%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU194+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:37 PM UTC 2026
% Result : Theorem 76.48s 10.42s
% Output : CNFRefutation 72.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 207
% Syntax : Number of formulae : 915 ( 133 unt; 159 def)
% Number of atoms : 2835 ( 517 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 3272 (1352 ~;1436 |; 236 &)
% ( 215 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 166 ( 164 usr; 160 prp; 0-2 aty)
% Number of functors : 51 ( 51 usr; 4 con; 0-5 aty)
% Number of variables : 1081 (1010 !; 71 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( relation(B)
=> ( B = identity_relation(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> ( C = D
& in(C,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] :
( ( A = empty_set
=> ( B = set_meet(A)
<=> B = empty_set ) )
& ( A != empty_set
=> ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(D,A)
=> in(C,D) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B] :
( B = powerset(A)
<=> ! [C] :
( in(C,B)
<=> subset(C,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B] :
( ( empty(A)
=> ( element(B,A)
<=> empty(B) ) )
& ( ~ empty(A)
=> ( element(B,A)
<=> in(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A,B,C] :
( C = unordered_pair(A,B)
<=> ! [D] :
( in(D,C)
<=> ( D = B
| D = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A,B,C] :
( C = set_union2(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(D,B)
| in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( subset(A,B)
<=> ! [C,D] :
( in(ordered_pair(C,D),A)
=> in(ordered_pair(C,D),B) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B,C] :
( C = set_intersection2(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( B = relation_inverse(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> in(ordered_pair(D,C),A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( relation(C)
=> ( C = relation_composition(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A,B] :
( relation(A)
=> relation(relation_dom_restriction(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
empty(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
( relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_dom(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [A,B] : set_intersection2(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,lemma,
! [A,B] :
( subset(A,singleton(B))
<=> ( A = singleton(B)
| A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,lemma,
! [A,B] :
( ! [C] :
( in(C,A)
=> in(C,B) )
=> element(A,powerset(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,lemma,
! [A,B,C,D] :
~ ( A != D
& A != C
& unordered_pair(A,B) = unordered_pair(C,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,lemma,
! [A,B,C] :
( ( subset(A,C)
& subset(A,B) )
=> subset(A,set_intersection2(B,C)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f115,axiom,
! [A] : set_union2(A,empty_set) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f121,lemma,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( subset(A,B)
=> ( subset(relation_rng(A),relation_rng(B))
& subset(relation_dom(A),relation_dom(B)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,axiom,
! [A] : set_intersection2(A,empty_set) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,lemma,
! [A] : subset(empty_set,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f153,lemma,
! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f159,lemma,
! [A] :
( relation(A)
=> ( ! [B,C] : ~ in(ordered_pair(B,C),A)
=> A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,lemma,
( relation_rng(empty_set) = empty_set
& relation_dom(empty_set) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f166,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,lemma,
! [A] : unordered_pair(A,A) = singleton(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,lemma,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_dom(relation_dom_restriction(C,B)))
<=> ( in(A,relation_dom(C))
& in(A,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,conjecture,
! [A,B] :
( relation(B)
=> relation_dom(relation_dom_restriction(B,A)) = set_intersection2(relation_dom(B),A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f181,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> relation_dom(relation_dom_restriction(B,A)) = set_intersection2(relation_dom(B),A) ),
inference(negated_conjecture,[status(cth)],[f180]) ).
fof(f186,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f187,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f192,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f194,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f195,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)],[f7]) ).
fof(f196,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)],[f195]) ).
fof(f197,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)],[f196]) ).
fof(f198,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))],[f197]) ).
fof(f203,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)],[f198]) ).
fof(f204,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)],[f198]) ).
fof(f205,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f206,plain,
( ! [A,B] :
( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ! [A,B] :
( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(miniscoping,[status(thm)],[f205]) ).
fof(f207,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f209,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f210,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)],[f9]) ).
fof(f211,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)],[f210]) ).
fof(f212,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)],[f211]) ).
fof(f213,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))],[f212]) ).
fof(f218,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)],[f213]) ).
fof(f219,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)],[f213]) ).
fof(f227,plain,
! [A,B] :
( ( ( B = set_meet(A)
<=> B = empty_set )
| A != empty_set )
& ( ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(C,D)
| ~ in(D,A) ) ) )
| A = empty_set ) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f228,plain,
! [A,B] :
( ( ( ( B != empty_set
| B = set_meet(A) )
& ( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ( ( ( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ( ! [C] :
( ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(NNF_transformation,[status(thm)],[f227]) ).
fof(f229,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(miniscoping,[status(thm)],[f228]) ).
fof(f230,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ( ( ! [D] :
( in(sK8_skl(B,A),D)
| ~ in(D,A) )
| in(sK8_skl(B,A),B) )
& ( ( ~ in(sK8_skl(B,A),sK9_skl(B,A))
& in(sK9_skl(B,A),A) )
| ~ in(sK8_skl(B,A),B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ( ~ in(C,sK7_skl(C,B,A))
& in(sK7_skl(C,B,A),A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl]),skolemize(D,sK7_skl(C,B,A)),skolemize(C,sK8_skl(B,A)),skolemize(D,sK9_skl(B,A))],[f229]) ).
fof(f232,plain,
! [X0,X1,X2] :
( in(sK7_skl(X2,X1,X0),X0)
| in(X2,X1)
| X1 != set_meet(X0)
| X0 = empty_set ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f234,plain,
! [X0,X1] :
( in(sK9_skl(X1,X0),X0)
| ~ in(sK8_skl(X1,X0),X1)
| X1 = set_meet(X0)
| X0 = empty_set ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f237,plain,
! [X0,X1] :
( X1 = empty_set
| X1 != set_meet(X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f239,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)],[f12]) ).
fof(f240,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)],[f239]) ).
fof(f241,plain,
( ! [A,B] :
( ( ( sK10_skl(B,A) = A
| in(sK10_skl(B,A),B) )
& ( sK10_skl(B,A) != A
| ~ in(sK10_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,[sK10_skl]),skolemize(C,sK10_skl(B,A))],[f240]) ).
fof(f242,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f243,plain,
! [X0,X1,X2] :
( X2 != X1
| in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f246,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f247,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f246]) ).
fof(f248,plain,
( ! [A] :
( in(sK11_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(B,sK11_skl(A))],[f247]) ).
fof(f249,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f251,plain,
! [A,B] :
( ( ? [C] :
( ( subset(C,A)
| in(C,B) )
& ( ~ subset(C,A)
| ~ in(C,B) ) )
| B = powerset(A) )
& ( ! [C] :
( ( ~ subset(C,A)
| in(C,B) )
& ( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(NNF_transformation,[status(thm)],[f14]) ).
fof(f252,plain,
( ! [A,B] :
( ? [C] :
( ( subset(C,A)
| in(C,B) )
& ( ~ subset(C,A)
| ~ in(C,B) ) )
| B = powerset(A) )
& ! [A,B] :
( ( ! [C] :
( ~ subset(C,A)
| in(C,B) )
& ! [C] :
( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(miniscoping,[status(thm)],[f251]) ).
fof(f253,plain,
( ! [A,B] :
( ( ( subset(sK12_skl(B,A),A)
| in(sK12_skl(B,A),B) )
& ( ~ subset(sK12_skl(B,A),A)
| ~ in(sK12_skl(B,A),B) ) )
| B = powerset(A) )
& ! [A,B] :
( ( ! [C] :
( ~ subset(C,A)
| in(C,B) )
& ! [C] :
( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(C,sK12_skl(B,A))],[f252]) ).
fof(f254,plain,
! [X0,X1,X2] :
( subset(X2,X1)
| ~ in(X2,X0)
| X0 != powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f255,plain,
! [X0,X1,X2] :
( ~ subset(X2,X1)
| in(X2,X0)
| X0 != powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f258,plain,
! [A,B] :
( ( ( element(B,A)
<=> empty(B) )
| ~ empty(A) )
& ( ( element(B,A)
<=> in(B,A) )
| empty(A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f259,plain,
! [A,B] :
( ( ( ( ~ empty(B)
| element(B,A) )
& ( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ( ( ( ~ in(B,A)
| element(B,A) )
& ( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(NNF_transformation,[status(thm)],[f258]) ).
fof(f260,plain,
( ! [A] :
( ( ! [B] :
( ~ empty(B)
| element(B,A) )
& ! [B] :
( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ! [A] :
( ( ! [B] :
( ~ in(B,A)
| element(B,A) )
& ! [B] :
( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(miniscoping,[status(thm)],[f259]) ).
fof(f261,plain,
! [X0,X1] :
( in(X1,X0)
| ~ element(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f264,plain,
! [X0,X1] :
( ~ empty(X1)
| element(X1,X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f265,plain,
! [A,B,C] :
( ( ? [D] :
( ( D = B
| D = A
| in(D,C) )
& ( ( D != B
& D != A )
| ~ in(D,C) ) )
| C = unordered_pair(A,B) )
& ( ! [D] :
( ( ( D != B
& D != A )
| in(D,C) )
& ( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f16]) ).
fof(f266,plain,
( ! [A,B,C] :
( ? [D] :
( ( D = B
| D = A
| in(D,C) )
& ( ( D != B
& D != A )
| ~ in(D,C) ) )
| C = unordered_pair(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( D != B
& D != A )
| in(D,C) )
& ! [D] :
( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(miniscoping,[status(thm)],[f265]) ).
fof(f267,plain,
( ! [A,B,C] :
( ( ( sK13_skl(C,B,A) = B
| sK13_skl(C,B,A) = A
| in(sK13_skl(C,B,A),C) )
& ( ( sK13_skl(C,B,A) != B
& sK13_skl(C,B,A) != A )
| ~ in(sK13_skl(C,B,A),C) ) )
| C = unordered_pair(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( D != B
& D != A )
| in(D,C) )
& ! [D] :
( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(D,sK13_skl(C,B,A))],[f266]) ).
fof(f268,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| X3 = X1
| ~ in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f270,plain,
! [X0,X1,X2,X3] :
( X3 != X2
| in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f271,plain,
! [X0,X1,X2] :
( sK13_skl(X0,X2,X1) != X1
| ~ in(sK13_skl(X0,X2,X1),X0)
| X0 = unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f272,plain,
! [X0,X1,X2] :
( sK13_skl(X0,X2,X1) != X2
| ~ in(sK13_skl(X0,X2,X1),X0)
| X0 = unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f274,plain,
! [A,B,C] :
( ( ? [D] :
( ( in(D,B)
| in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& ~ in(D,A) )
| ~ in(D,C) ) )
| C = set_union2(A,B) )
& ( ! [D] :
( ( ( ~ in(D,B)
& ~ in(D,A) )
| in(D,C) )
& ( in(D,B)
| in(D,A)
| ~ in(D,C) ) )
| C != set_union2(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f17]) ).
fof(f275,plain,
( ! [A,B,C] :
( ? [D] :
( ( in(D,B)
| in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& ~ in(D,A) )
| ~ in(D,C) ) )
| C = set_union2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( ~ in(D,B)
& ~ in(D,A) )
| in(D,C) )
& ! [D] :
( in(D,B)
| in(D,A)
| ~ in(D,C) ) )
| C != set_union2(A,B) ) ),
inference(miniscoping,[status(thm)],[f274]) ).
fof(f276,plain,
( ! [A,B,C] :
( ( ( in(sK14_skl(C,B,A),B)
| in(sK14_skl(C,B,A),A)
| in(sK14_skl(C,B,A),C) )
& ( ( ~ in(sK14_skl(C,B,A),B)
& ~ in(sK14_skl(C,B,A),A) )
| ~ in(sK14_skl(C,B,A),C) ) )
| C = set_union2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( ~ in(D,B)
& ~ in(D,A) )
| in(D,C) )
& ! [D] :
( in(D,B)
| in(D,A)
| ~ in(D,C) ) )
| C != set_union2(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(D,sK14_skl(C,B,A))],[f275]) ).
fof(f277,plain,
! [X0,X1,X2,X3] :
( in(X3,X2)
| in(X3,X1)
| ~ in(X3,X0)
| X0 != set_union2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f292,plain,
! [A] :
( ! [B] :
( ( subset(A,B)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f293,plain,
! [A] :
( ! [B] :
( ( ( ? [C,D] :
( ~ in(ordered_pair(C,D),B)
& in(ordered_pair(C,D),A) )
| subset(A,B) )
& ( ! [C,D] :
( in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) )
| ~ subset(A,B) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f292]) ).
fof(f294,plain,
! [A] :
( ! [B] :
( ( ( ( ~ in(ordered_pair(sK20_skl(B,A),sK21_skl(B,A)),B)
& in(ordered_pair(sK20_skl(B,A),sK21_skl(B,A)),A) )
| subset(A,B) )
& ( ! [C,D] :
( in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) )
| ~ subset(A,B) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl]),skolemize(C,sK20_skl(B,A)),skolemize(D,sK21_skl(B,A))],[f293]) ).
fof(f296,plain,
! [X0,X1] :
( in(ordered_pair(sK20_skl(X1,X0),sK21_skl(X1,X0)),X0)
| subset(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f298,plain,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,B)
| ~ in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f299,plain,
! [A,B] :
( ( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f298]) ).
fof(f300,plain,
( ! [A,B] :
( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f299]) ).
fof(f301,plain,
( ! [A,B] :
( ( ~ in(sK22_skl(B,A),B)
& in(sK22_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(C,sK22_skl(B,A))],[f300]) ).
fof(f304,plain,
! [X0,X1] :
( ~ in(sK22_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f305,plain,
! [A,B,C] :
( ( ? [D] :
( ( ( in(D,B)
& in(D,A) )
| in(D,C) )
& ( ~ in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_intersection2(A,B) )
& ( ! [D] :
( ( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f21]) ).
fof(f306,plain,
( ! [A,B,C] :
( ? [D] :
( ( ( in(D,B)
& in(D,A) )
| in(D,C) )
& ( ~ in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_intersection2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(miniscoping,[status(thm)],[f305]) ).
fof(f307,plain,
( ! [A,B,C] :
( ( ( ( in(sK23_skl(C,B,A),B)
& in(sK23_skl(C,B,A),A) )
| in(sK23_skl(C,B,A),C) )
& ( ~ in(sK23_skl(C,B,A),B)
| ~ in(sK23_skl(C,B,A),A)
| ~ in(sK23_skl(C,B,A),C) ) )
| C = set_intersection2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(D,sK23_skl(C,B,A))],[f306]) ).
fof(f308,plain,
! [X0,X1,X2,X3] :
( in(X3,X1)
| ~ in(X3,X0)
| X0 != set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f309,plain,
! [X0,X1,X2,X3] :
( in(X3,X2)
| ~ in(X3,X0)
| X0 != set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f310,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,X2)
| ~ in(X3,X1)
| in(X3,X0)
| X0 != set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f311,plain,
! [X0,X1,X2] :
( ~ in(sK23_skl(X0,X2,X1),X2)
| ~ in(sK23_skl(X0,X2,X1),X1)
| ~ in(sK23_skl(X0,X2,X1),X0)
| X0 = set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f312,plain,
! [X0,X1,X2] :
( in(sK23_skl(X0,X2,X1),X1)
| in(sK23_skl(X0,X2,X1),X0)
| X0 = set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f313,plain,
! [X0,X1,X2] :
( in(sK23_skl(X0,X2,X1),X2)
| in(sK23_skl(X0,X2,X1),X0)
| X0 = set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f314,plain,
! [A] :
( ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f315,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] : in(ordered_pair(C,D),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B = relation_dom(A) )
& ( ! [C] :
( ( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ( ? [D] : in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f314]) ).
fof(f316,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ( ? [D] : in(ordered_pair(C,D),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B = relation_dom(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ! [C] :
( ? [D] : in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f315]) ).
fof(f317,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK25_skl(B,A),sK26_skl(B,A)),A)
| in(sK25_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(sK25_skl(B,A),D),A)
| ~ in(sK25_skl(B,A),B) ) )
| B = relation_dom(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(C,sK24_skl(C,B,A)),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl,sK25_skl,sK26_skl]),skolemize(D,sK24_skl(C,B,A)),skolemize(C,sK25_skl(B,A)),skolemize(D,sK26_skl(B,A))],[f316]) ).
fof(f319,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(X2,X3),X0)
| in(X2,X1)
| X1 != relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f321,plain,
! [X0,X1] :
( in(ordered_pair(sK25_skl(X1,X0),sK26_skl(X1,X0)),X0)
| in(sK25_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f332,plain,
! [A,B,C] :
( ( ? [D] :
( ( ( ~ in(D,B)
& in(D,A) )
| in(D,C) )
& ( in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_difference(A,B) )
& ( ! [D] :
( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f25]) ).
fof(f333,plain,
( ! [A,B,C] :
( ? [D] :
( ( ( ~ in(D,B)
& in(D,A) )
| in(D,C) )
& ( in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_difference(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(miniscoping,[status(thm)],[f332]) ).
fof(f334,plain,
( ! [A,B,C] :
( ( ( ( ~ in(sK30_skl(C,B,A),B)
& in(sK30_skl(C,B,A),A) )
| in(sK30_skl(C,B,A),C) )
& ( in(sK30_skl(C,B,A),B)
| ~ in(sK30_skl(C,B,A),A)
| ~ in(sK30_skl(C,B,A),C) ) )
| C = set_difference(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl]),skolemize(D,sK30_skl(C,B,A))],[f333]) ).
fof(f337,plain,
! [X0,X1,X2,X3] :
( in(X3,X2)
| ~ in(X3,X1)
| in(X3,X0)
| X0 != set_difference(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f341,plain,
! [A] :
( ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f342,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] : in(ordered_pair(D,C),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ( ! [C] :
( ( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ( ? [D] : in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f341]) ).
fof(f343,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ( ? [D] : in(ordered_pair(D,C),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( ? [D] : in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f342]) ).
fof(f344,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK33_skl(B,A),sK32_skl(B,A)),A)
| in(sK32_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(D,sK32_skl(B,A)),A)
| ~ in(sK32_skl(B,A),B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(sK31_skl(C,B,A),C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl,sK32_skl,sK33_skl]),skolemize(D,sK31_skl(C,B,A)),skolemize(C,sK32_skl(B,A)),skolemize(D,sK33_skl(B,A))],[f343]) ).
fof(f348,plain,
! [X0,X1] :
( in(ordered_pair(sK33_skl(X1,X0),sK32_skl(X1,X0)),X0)
| in(sK32_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f354,plain,
! [A] :
( ! [B] :
( ( B = relation_inverse(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> in(ordered_pair(D,C),A) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f355,plain,
! [A] :
( ! [B] :
( ( ( ? [C,D] :
( ( in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),B) )
& ( ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),B) ) )
| B = relation_inverse(A) )
& ( ! [C,D] :
( ( ~ in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),B) )
& ( in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),B) ) )
| B != relation_inverse(A) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f354]) ).
fof(f356,plain,
! [A] :
( ! [B] :
( ( ( ? [C,D] :
( ( in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),B) )
& ( ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),B) ) )
| B = relation_inverse(A) )
& ( ( ! [C,D] :
( ~ in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),B) )
& ! [C,D] :
( in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),B) ) )
| B != relation_inverse(A) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f355]) ).
fof(f357,plain,
! [A] :
( ! [B] :
( ( ( ( ( in(ordered_pair(sK35_skl(B,A),sK34_skl(B,A)),A)
| in(ordered_pair(sK34_skl(B,A),sK35_skl(B,A)),B) )
& ( ~ in(ordered_pair(sK35_skl(B,A),sK34_skl(B,A)),A)
| ~ in(ordered_pair(sK34_skl(B,A),sK35_skl(B,A)),B) ) )
| B = relation_inverse(A) )
& ( ( ! [C,D] :
( ~ in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),B) )
& ! [C,D] :
( in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),B) ) )
| B != relation_inverse(A) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl,sK35_skl]),skolemize(C,sK34_skl(B,A)),skolemize(D,sK35_skl(B,A))],[f356]) ).
fof(f361,plain,
! [X0,X1] :
( in(ordered_pair(sK35_skl(X1,X0),sK34_skl(X1,X0)),X0)
| in(ordered_pair(sK34_skl(X1,X0),sK35_skl(X1,X0)),X1)
| X1 = relation_inverse(X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f357]) ).
fof(f366,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( C = relation_composition(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) ) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f367,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D,E] :
( ( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_composition(A,B) )
& ( ! [D,E] :
( ( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_composition(A,B) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f366]) ).
fof(f368,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D,E] :
( ( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_composition(A,B) )
& ( ( ! [D,E] :
( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_composition(A,B) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f367]) ).
fof(f369,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ( ( ( in(ordered_pair(sK39_skl(C,B,A),sK38_skl(C,B,A)),B)
& in(ordered_pair(sK37_skl(C,B,A),sK39_skl(C,B,A)),A) )
| in(ordered_pair(sK37_skl(C,B,A),sK38_skl(C,B,A)),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,sK38_skl(C,B,A)),B)
| ~ in(ordered_pair(sK37_skl(C,B,A),F),A) )
| ~ in(ordered_pair(sK37_skl(C,B,A),sK38_skl(C,B,A)),C) ) )
| C = relation_composition(A,B) )
& ( ( ! [D,E] :
( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(sK36_skl(E,D,C,B,A),E),B)
& in(ordered_pair(D,sK36_skl(E,D,C,B,A)),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_composition(A,B) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl,sK38_skl,sK39_skl]),skolemize(F,sK36_skl(E,D,C,B,A)),skolemize(D,sK37_skl(C,B,A)),skolemize(E,sK38_skl(C,B,A)),skolemize(F,sK39_skl(C,B,A))],[f368]) ).
fof(f374,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK37_skl(X2,X1,X0),sK39_skl(X2,X1,X0)),X0)
| in(ordered_pair(sK37_skl(X2,X1,X0),sK38_skl(X2,X1,X0)),X2)
| X2 = relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f375,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK39_skl(X2,X1,X0),sK38_skl(X2,X1,X0)),X1)
| in(ordered_pair(sK37_skl(X2,X1,X0),sK38_skl(X2,X1,X0)),X2)
| X2 = relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f398,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f403,plain,
! [A,B] :
( relation(relation_dom_restriction(A,B))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f404,plain,
! [A] :
( ! [B] : relation(relation_dom_restriction(A,B))
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f403]) ).
fof(f405,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f415,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f416,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f420,plain,
! [X0] : ~ empty(singleton(X0)),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f424,plain,
! [X0,X1] : ~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f429,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f432,plain,
! [A] :
( ~ empty(relation_dom(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f433,plain,
! [X0] :
( ~ empty(relation_dom(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f432]) ).
fof(f447,plain,
! [A] : set_intersection2(A,A) = A,
inference(miniscoping,[status(thm)],[f79]) ).
fof(f448,plain,
! [X0] : set_intersection2(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f447]) ).
fof(f457,plain,
! [X0] : singleton(X0) != empty_set,
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f477,plain,
! [A,B] :
( ( ( A != singleton(B)
& A != empty_set )
| subset(A,singleton(B)) )
& ( A = singleton(B)
| A = empty_set
| ~ subset(A,singleton(B)) ) ),
inference(NNF_transformation,[status(thm)],[f92]) ).
fof(f478,plain,
( ! [A,B] :
( ( A != singleton(B)
& A != empty_set )
| subset(A,singleton(B)) )
& ! [A,B] :
( A = singleton(B)
| A = empty_set
| ~ subset(A,singleton(B)) ) ),
inference(miniscoping,[status(thm)],[f477]) ).
fof(f479,plain,
! [X0,X1] :
( X0 = singleton(X1)
| X0 = empty_set
| ~ subset(X0,singleton(X1)) ),
inference(cnf_transformation,[status(thm)],[f478]) ).
fof(f489,plain,
! [A,B] :
( element(A,powerset(B))
| ? [C] :
( ~ in(C,B)
& in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f490,plain,
! [A,B] :
( element(A,powerset(B))
| ( ~ in(sK42_skl(B,A),B)
& in(sK42_skl(B,A),A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42_skl]),skolemize(C,sK42_skl(B,A))],[f489]) ).
fof(f491,plain,
! [X0,X1] :
( element(X1,powerset(X0))
| in(sK42_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f490]) ).
fof(f502,plain,
( relation(sK46_skl)
& ~ empty(sK46_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46_skl]),skolemize(A,sK46_skl)],[f99]) ).
fof(f503,plain,
~ empty(sK46_skl),
inference(cnf_transformation,[status(thm)],[f502]) ).
fof(f504,plain,
relation(sK46_skl),
inference(cnf_transformation,[status(thm)],[f502]) ).
fof(f505,plain,
! [A] :
( empty(sK47_skl(A))
& element(sK47_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl]),skolemize(B,sK47_skl(A))],[f100]) ).
fof(f507,plain,
! [X0] : empty(sK47_skl(X0)),
inference(cnf_transformation,[status(thm)],[f505]) ).
fof(f525,plain,
! [A,B,C,D] :
( A = D
| A = C
| unordered_pair(A,B) != unordered_pair(C,D) ),
inference(pre_NNF_transformation,[status(thm)],[f108]) ).
fof(f526,plain,
! [A,D] :
( A = D
| ! [C] :
( A = C
| ! [B] : unordered_pair(A,B) != unordered_pair(C,D) ) ),
inference(miniscoping,[status(thm)],[f525]) ).
fof(f527,plain,
! [X0,X1,X2,X3] :
( X0 = X3
| X0 = X2
| unordered_pair(X0,X1) != unordered_pair(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f526]) ).
fof(f544,plain,
! [A,B,C] :
( subset(A,set_intersection2(B,C))
| ~ subset(A,C)
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f114]) ).
fof(f545,plain,
! [X0,X1,X2] :
( subset(X0,set_intersection2(X1,X2))
| ~ subset(X0,X2)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f544]) ).
fof(f546,plain,
! [X0] : set_union2(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f559,plain,
! [A] :
( ! [B] :
( ( subset(relation_rng(A),relation_rng(B))
& subset(relation_dom(A),relation_dom(B)) )
| ~ subset(A,B)
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f121]) ).
fof(f560,plain,
! [X0,X1] :
( subset(relation_dom(X0),relation_dom(X1))
| ~ subset(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f559]) ).
fof(f567,plain,
! [X0] : set_intersection2(X0,empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f575,plain,
! [X0] : subset(empty_set,X0),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f645,plain,
! [X0,X1] : set_difference(X0,set_difference(X0,X1)) = set_intersection2(X0,X1),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f660,plain,
! [A] :
( A = empty_set
| ? [B,C] : in(ordered_pair(B,C),A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f159]) ).
fof(f661,plain,
! [A] :
( A = empty_set
| in(ordered_pair(sK53_skl(A),sK54_skl(A)),A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53_skl,sK54_skl]),skolemize(B,sK53_skl(A)),skolemize(C,sK54_skl(A))],[f660]) ).
fof(f662,plain,
! [X0] :
( X0 = empty_set
| in(ordered_pair(sK53_skl(X0),sK54_skl(X0)),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f661]) ).
fof(f666,plain,
relation_dom(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f667,plain,
relation_rng(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f680,plain,
! [A,B] :
( ( in(B,A)
| set_difference(A,singleton(B)) = A )
& ( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(NNF_transformation,[status(thm)],[f166]) ).
fof(f681,plain,
( ! [A,B] :
( in(B,A)
| set_difference(A,singleton(B)) = A )
& ! [A,B] :
( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(miniscoping,[status(thm)],[f680]) ).
fof(f683,plain,
! [X0,X1] :
( in(X1,X0)
| set_difference(X0,singleton(X1)) = X0 ),
inference(cnf_transformation,[status(thm)],[f681]) ).
fof(f684,plain,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f706,plain,
! [A,B,C] :
( ( in(A,relation_dom(relation_dom_restriction(C,B)))
<=> ( in(A,relation_dom(C))
& in(A,B) ) )
| ~ relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f175]) ).
fof(f707,plain,
! [A,B,C] :
( ( ( ~ in(A,relation_dom(C))
| ~ in(A,B)
| in(A,relation_dom(relation_dom_restriction(C,B))) )
& ( ( in(A,relation_dom(C))
& in(A,B) )
| ~ in(A,relation_dom(relation_dom_restriction(C,B))) ) )
| ~ relation(C) ),
inference(NNF_transformation,[status(thm)],[f706]) ).
fof(f708,plain,
! [C] :
( ( ! [A,B] :
( ~ in(A,relation_dom(C))
| ~ in(A,B)
| in(A,relation_dom(relation_dom_restriction(C,B))) )
& ! [A,B] :
( ( in(A,relation_dom(C))
& in(A,B) )
| ~ in(A,relation_dom(relation_dom_restriction(C,B))) ) )
| ~ relation(C) ),
inference(miniscoping,[status(thm)],[f707]) ).
fof(f709,plain,
! [X0,X1,X2] :
( in(X1,X2)
| ~ in(X1,relation_dom(relation_dom_restriction(X0,X2)))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f708]) ).
fof(f710,plain,
! [X0,X1,X2] :
( in(X1,relation_dom(X0))
| ~ in(X1,relation_dom(relation_dom_restriction(X0,X2)))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f708]) ).
fof(f711,plain,
! [X0,X1,X2] :
( ~ in(X1,relation_dom(X0))
| ~ in(X1,X2)
| in(X1,relation_dom(relation_dom_restriction(X0,X2)))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f708]) ).
fof(f723,plain,
? [A,B] :
( relation_dom(relation_dom_restriction(B,A)) != set_intersection2(relation_dom(B),A)
& relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f181]) ).
fof(f724,plain,
? [B] :
( ? [A] : relation_dom(relation_dom_restriction(B,A)) != set_intersection2(relation_dom(B),A)
& relation(B) ),
inference(miniscoping,[status(thm)],[f723]) ).
fof(f725,plain,
( relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) != set_intersection2(relation_dom(sK55_skl),sK56_skl)
& relation(sK55_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55_skl,sK56_skl]),skolemize(B,sK55_skl),skolemize(A,sK56_skl)],[f724]) ).
fof(f726,plain,
relation(sK55_skl),
inference(cnf_transformation,[status(thm)],[f725]) ).
fof(f727,plain,
relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) != set_intersection2(relation_dom(sK55_skl),sK56_skl),
inference(cnf_transformation,[status(thm)],[f725]) ).
fof(f751,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f207]) ).
fof(f757,plain,
! [X0,X1] :
( in(sK7_skl(X1,set_meet(X0),X0),X0)
| in(X1,set_meet(X0))
| X0 = empty_set ),
inference(destructive_equality_resolution,[status(thm)],[f232]) ).
fof(f759,plain,
set_meet(empty_set) = empty_set,
inference(destructive_equality_resolution,[status(thm)],[f237]) ).
fof(f761,plain,
! [X0,X1] :
( X0 = X1
| ~ in(X0,singleton(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f242]) ).
fof(f762,plain,
! [X0] : in(X0,singleton(X0)),
inference(destructive_equality_resolution,[status(thm)],[f243]) ).
fof(f763,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f249]) ).
fof(f764,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ in(X0,powerset(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f254]) ).
fof(f765,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| in(X0,powerset(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f255]) ).
fof(f766,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ in(X0,unordered_pair(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f268]) ).
fof(f768,plain,
! [X0,X1] : in(X0,unordered_pair(X1,X0)),
inference(destructive_equality_resolution,[status(thm)],[f270]) ).
fof(f769,plain,
! [X0,X1,X2] :
( in(X0,X2)
| in(X0,X1)
| ~ in(X0,set_union2(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f277]) ).
fof(f774,plain,
! [X0,X1,X2] :
( in(X0,X1)
| ~ in(X0,set_intersection2(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f308]) ).
fof(f775,plain,
! [X0,X1,X2] :
( in(X0,X2)
| ~ in(X0,set_intersection2(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f309]) ).
fof(f776,plain,
! [X0,X1,X2] :
( ~ in(X0,X2)
| ~ in(X0,X1)
| in(X0,set_intersection2(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f310]) ).
fof(f778,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),X0)
| in(X1,relation_dom(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f319]) ).
fof(f784,plain,
! [X0,X1,X2] :
( in(X0,X2)
| ~ in(X0,X1)
| in(X0,set_difference(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f337]) ).
fof(f821,plain,
relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) != set_intersection2(sK56_skl,relation_dom(sK55_skl)),
inference(paramodulation,[status(thm)],[f194,f727]) ).
fof(f823,plain,
! [X0,X1] : ~ in(X0,set_intersection2(X0,X1)),
inference(resolution,[status(thm)],[f187,f774]) ).
fof(f837,plain,
! [X0,X1] :
( ~ in(X0,ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)))
| sK0_skl(X1,X0) = sK1_skl(X1,X0)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f204,f187]) ).
fof(f841,plain,
! [X0,X1,X2] :
( ~ in(X1,ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)))
| 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)],[f219,f187]) ).
fof(f847,plain,
! [X0] :
( relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) = X0
| ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)) ),
inference(resolution,[status(thm)],[f766,f727]) ).
fof(f848,plain,
! [X0] :
( set_intersection2(relation_dom(sK55_skl),sK56_skl) = X0
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0)) ),
inference(resolution,[status(thm)],[f766,f727]) ).
fof(f884,plain,
! [X0,X1] :
( set_intersection2(relation_dom(sK55_skl),sK56_skl) = X1
| unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) != unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X1) ),
inference(resolution,[status(thm)],[f527,f727]) ).
fof(f940,plain,
! [X0,X1] :
( relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) = X1
| unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0) != unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X1) ),
inference(resolution,[status(thm)],[f821,f527]) ).
fof(f941,plain,
! [X0] :
( relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) = X0
| ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0)) ),
inference(resolution,[status(thm)],[f821,f766]) ).
fof(f942,plain,
! [X0,X1] :
( set_intersection2(sK56_skl,relation_dom(sK55_skl)) = X1
| unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0) != unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X1) ),
inference(resolution,[status(thm)],[f821,f527]) ).
fof(f943,plain,
! [X0] :
( set_intersection2(sK56_skl,relation_dom(sK55_skl)) = X0
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0)) ),
inference(resolution,[status(thm)],[f821,f766]) ).
fof(f944,plain,
~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl)))),
inference(resolution,[status(thm)],[f847,f821]) ).
fof(f945,plain,
~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(relation_dom(sK55_skl),sK56_skl))),
inference(resolution,[status(thm)],[f847,f727]) ).
fof(f946,plain,
~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl))),
inference(forward_demodulation,[status(thm)],[f684,f945]) ).
fof(f950,plain,
! [X0] : set_intersection2(empty_set,X0) = empty_set,
inference(paramodulation,[status(thm)],[f194,f567]) ).
fof(f985,plain,
! [X0,X1] :
( ~ in(X1,ordered_pair(sK34_skl(X1,X0),sK35_skl(X1,X0)))
| in(ordered_pair(sK35_skl(X1,X0),sK34_skl(X1,X0)),X0)
| X1 = relation_inverse(X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f361,f187]) ).
fof(f987,plain,
! [X0,X1,X2] :
( ~ in(X2,ordered_pair(sK37_skl(X2,X1,X0),sK38_skl(X2,X1,X0)))
| in(ordered_pair(sK37_skl(X2,X1,X0),sK39_skl(X2,X1,X0)),X0)
| X2 = relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f374,f187]) ).
fof(f989,plain,
! [X0,X1,X2] :
( ~ in(X2,ordered_pair(sK37_skl(X2,X1,X0),sK38_skl(X2,X1,X0)))
| in(ordered_pair(sK39_skl(X2,X1,X0),sK38_skl(X2,X1,X0)),X1)
| X2 = relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f375,f187]) ).
fof(f1045,plain,
~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))),
inference(resolution,[status(thm)],[f848,f727]) ).
fof(f1048,plain,
~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))),
inference(forward_demodulation,[status(thm)],[f684,f1045]) ).
fof(f1052,plain,
! [X0] : unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) != unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),
inference(resolution,[status(thm)],[f884,f727]) ).
fof(f1055,plain,
! [X0] : unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) != singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),
inference(forward_demodulation,[status(thm)],[f684,f1052]) ).
fof(f1056,plain,
! [X0] : unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0) != unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(sK56_skl,relation_dom(sK55_skl))),
inference(resolution,[status(thm)],[f940,f821]) ).
fof(f1058,plain,
! [X0] : unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0) != singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),
inference(forward_demodulation,[status(thm)],[f684,f1056]) ).
fof(f1059,plain,
~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(sK56_skl,relation_dom(sK55_skl)))),
inference(resolution,[status(thm)],[f941,f821]) ).
fof(f1060,plain,
~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl))),
inference(resolution,[status(thm)],[f941,f727]) ).
fof(f1061,plain,
~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))),
inference(forward_demodulation,[status(thm)],[f684,f1059]) ).
fof(f1062,plain,
! [X0] : unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0) != unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),
inference(resolution,[status(thm)],[f942,f821]) ).
fof(f1063,plain,
! [X0] : unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0) != singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),
inference(forward_demodulation,[status(thm)],[f684,f1062]) ).
fof(f1064,plain,
~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))),
inference(resolution,[status(thm)],[f943,f821]) ).
fof(f1065,plain,
~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))),
inference(forward_demodulation,[status(thm)],[f684,f1064]) ).
fof(f1067,plain,
! [X0] : ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(X0,unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl))))),
inference(resolution,[status(thm)],[f944,f775]) ).
fof(f1070,plain,
set_difference(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) = unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl))),
inference(resolution,[status(thm)],[f944,f683]) ).
fof(f1071,plain,
( ~ element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl))))
| empty(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
inference(resolution,[status(thm)],[f944,f261]) ).
fof(f1077,definition,
( sQ0_spl
<=> empty(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1078,plain,
( ~ sQ0_spl
| empty(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
inference(component_clause,[status(thm)],[f1077]) ).
fof(f1080,definition,
( sQ1_spl
<=> element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1083,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1071,f1077,f1080]) ).
fof(f1086,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1078,f424]) ).
fof(f1087,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f1086]) ).
fof(f1092,plain,
set_difference(singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) = singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl)),
inference(resolution,[status(thm)],[f946,f683]) ).
fof(f1093,plain,
( ~ element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl)))
| empty(singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
inference(resolution,[status(thm)],[f946,f261]) ).
fof(f1097,definition,
( sQ2_spl
<=> empty(singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1098,plain,
( ~ sQ2_spl
| empty(singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
inference(component_clause,[status(thm)],[f1097]) ).
fof(f1100,definition,
( sQ3_spl
<=> element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1103,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1093,f1097,f1100]) ).
fof(f1104,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1098,f420]) ).
fof(f1105,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f1104]) ).
fof(f1107,plain,
! [X0] : ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(X0,singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))),
inference(resolution,[status(thm)],[f1048,f775]) ).
fof(f1108,plain,
! [X0] :
( in(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_union2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
inference(resolution,[status(thm)],[f1048,f769]) ).
fof(f1111,plain,
( ~ element(set_intersection2(relation_dom(sK55_skl),sK56_skl),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| empty(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f1048,f261]) ).
fof(f1112,plain,
! [X0] : ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)),
inference(resolution,[status(thm)],[f1048,f774]) ).
fof(f1115,definition,
( sQ4_spl
<=> empty(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1116,plain,
( ~ sQ4_spl
| empty(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(component_clause,[status(thm)],[f1115]) ).
fof(f1118,definition,
( sQ5_spl
<=> element(set_intersection2(relation_dom(sK55_skl),sK56_skl),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1121,plain,
( ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1111,f1115,f1118]) ).
fof(f1122,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1116,f420]) ).
fof(f1123,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1122]) ).
fof(f1130,plain,
! [X0,X1] :
( ~ in(ordered_pair(X0,X1),empty_set)
| in(X0,empty_set)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f666,f778]) ).
fof(f1131,definition,
( sQ6_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1133,plain,
( sQ6_spl
| ~ relation(empty_set) ),
inference(component_clause,[status(thm)],[f1131]) ).
fof(f1134,definition,
! [X0,X1] :
( sQ7_spl
<=> ( ~ in(ordered_pair(X0,X1),empty_set)
| in(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1137,plain,
( sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1130,f1131,f1134]) ).
fof(f1138,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1133,f429]) ).
fof(f1139,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1138]) ).
fof(f1141,plain,
( ~ subset(set_intersection2(sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))
| ~ subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(sK56_skl,relation_dom(sK55_skl))) ),
inference(resolution,[status(thm)],[f209,f821]) ).
fof(f1142,plain,
( ~ subset(set_intersection2(relation_dom(sK55_skl),sK56_skl),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))
| ~ subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f209,f727]) ).
fof(f1145,definition,
( sQ8_spl
<=> subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(sK56_skl,relation_dom(sK55_skl))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1147,plain,
( sQ8_spl
| ~ subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(sK56_skl,relation_dom(sK55_skl))) ),
inference(component_clause,[status(thm)],[f1145]) ).
fof(f1148,definition,
( sQ9_spl
<=> subset(set_intersection2(sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1150,plain,
( sQ9_spl
| ~ subset(set_intersection2(sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(component_clause,[status(thm)],[f1148]) ).
fof(f1151,plain,
( ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1141,f1145,f1148]) ).
fof(f1152,definition,
( sQ10_spl
<=> subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1153,plain,
( ~ sQ10_spl
| subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(component_clause,[status(thm)],[f1152]) ).
fof(f1154,plain,
( sQ10_spl
| ~ subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(component_clause,[status(thm)],[f1152]) ).
fof(f1155,definition,
( sQ11_spl
<=> subset(set_intersection2(relation_dom(sK55_skl),sK56_skl),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1156,plain,
( ~ sQ11_spl
| subset(set_intersection2(relation_dom(sK55_skl),sK56_skl),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(component_clause,[status(thm)],[f1155]) ).
fof(f1157,plain,
( sQ11_spl
| ~ subset(set_intersection2(relation_dom(sK55_skl),sK56_skl),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(component_clause,[status(thm)],[f1155]) ).
fof(f1158,plain,
( ~ sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1142,f1152,f1155]) ).
fof(f1162,plain,
( sQ10_spl
| ~ subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(sK56_skl,relation_dom(sK55_skl))) ),
inference(paramodulation,[status(thm)],[f194,f1154]) ).
fof(f1167,plain,
set_difference(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) = singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),
inference(resolution,[status(thm)],[f1061,f683]) ).
fof(f1168,plain,
( ~ element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))))
| empty(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
inference(resolution,[status(thm)],[f1061,f261]) ).
fof(f1169,plain,
! [X0] : ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),X0)),
inference(resolution,[status(thm)],[f1061,f774]) ).
fof(f1170,definition,
( sQ12_spl
<=> empty(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1171,plain,
( ~ sQ12_spl
| empty(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
inference(component_clause,[status(thm)],[f1170]) ).
fof(f1173,definition,
( sQ13_spl
<=> element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1176,plain,
( ~ sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f1168,f1170,f1173]) ).
fof(f1177,plain,
( ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1171,f420]) ).
fof(f1178,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1177]) ).
fof(f1184,plain,
( ~ element(set_intersection2(sK56_skl,relation_dom(sK55_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| empty(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f1065,f261]) ).
fof(f1186,definition,
( sQ14_spl
<=> element(set_intersection2(sK56_skl,relation_dom(sK55_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f1189,plain,
( ~ sQ14_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1184,f1115,f1186]) ).
fof(f1213,plain,
! [X0] :
( unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) = empty_set
| ~ subset(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f1055,f479]) ).
fof(f1216,plain,
! [X0,X1] :
( unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) = X1
| ~ in(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),unordered_pair(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X1)) ),
inference(resolution,[status(thm)],[f1055,f766]) ).
fof(f1220,plain,
! [X0] : unordered_pair(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) != singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),
inference(paramodulation,[status(thm)],[f192,f1055]) ).
fof(f1285,plain,
( ~ element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)))
| empty(unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
inference(resolution,[status(thm)],[f1060,f261]) ).
fof(f1289,definition,
( sQ15_spl
<=> empty(unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f1290,plain,
( ~ sQ15_spl
| empty(unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
inference(component_clause,[status(thm)],[f1289]) ).
fof(f1292,definition,
( sQ16_spl
<=> element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1295,plain,
( ~ sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f1285,f1289,f1292]) ).
fof(f1298,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1290,f424]) ).
fof(f1299,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f1298]) ).
fof(f1300,plain,
! [X0] :
( ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl))))
| ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0) ),
inference(resolution,[status(thm)],[f1067,f776]) ).
fof(f1307,plain,
! [X0,X1] : ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(set_intersection2(X0,unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl)))),X1)),
inference(resolution,[status(thm)],[f1067,f774]) ).
fof(f1315,definition,
! [X0] :
( sQ17_spl
<=> ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1316,plain,
! [X0] :
( ~ sQ17_spl
| ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0) ),
inference(component_clause,[status(thm)],[f1315]) ).
fof(f1318,definition,
( sQ18_spl
<=> in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1321,plain,
( ~ sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f1300,f1315,f1318]) ).
fof(f1326,plain,
set_difference(unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) = unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl))),
inference(paramodulation,[status(thm)],[f194,f1070]) ).
fof(f1332,plain,
set_difference(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) = unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl))),
inference(forward_demodulation,[status(thm)],[f684,f1326]) ).
fof(f1346,plain,
singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))) = unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl))),
inference(forward_demodulation,[status(thm)],[f1167,f1332]) ).
fof(f1357,plain,
set_difference(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) = singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl)),
inference(paramodulation,[status(thm)],[f194,f1092]) ).
fof(f1379,plain,
singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))) = singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl)),
inference(forward_demodulation,[status(thm)],[f1167,f1357]) ).
fof(f1455,plain,
! [X0] : ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(X0,singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))))),
inference(forward_demodulation,[status(thm)],[f1346,f1067]) ).
fof(f1464,plain,
! [X0,X1] : ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(set_intersection2(X0,singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))),X1)),
inference(forward_demodulation,[status(thm)],[f1346,f1307]) ).
fof(f1477,plain,
! [X0] :
( ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) ),
inference(resolution,[status(thm)],[f1107,f776]) ).
fof(f1484,plain,
! [X0,X1] : ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(set_intersection2(X0,singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))),X1)),
inference(resolution,[status(thm)],[f1107,f774]) ).
fof(f1490,definition,
! [X0] :
( sQ21_spl
<=> ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f1491,plain,
! [X0] :
( ~ sQ21_spl
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) ),
inference(component_clause,[status(thm)],[f1490]) ).
fof(f1493,definition,
( sQ22_spl
<=> in(set_intersection2(relation_dom(sK55_skl),sK56_skl),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1496,plain,
( ~ sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f1477,f1490,f1493]) ).
fof(f1518,plain,
! [X0] : ~ in(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),unordered_pair(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))),
inference(resolution,[status(thm)],[f1216,f1055]) ).
fof(f1519,plain,
~ in(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(relation_dom(sK55_skl),sK56_skl)),unordered_pair(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))),
inference(resolution,[status(thm)],[f1216,f1220]) ).
fof(f1524,plain,
! [X0] : ~ in(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))),
inference(forward_demodulation,[status(thm)],[f684,f1518]) ).
fof(f1525,plain,
~ in(singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl)),unordered_pair(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))),
inference(forward_demodulation,[status(thm)],[f684,f1519]) ).
fof(f1526,plain,
~ in(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),unordered_pair(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))),
inference(forward_demodulation,[status(thm)],[f1379,f1525]) ).
fof(f1527,plain,
~ in(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))),
inference(forward_demodulation,[status(thm)],[f684,f1526]) ).
fof(f1545,definition,
( sQ23_spl
<=> in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f1569,plain,
! [X0] :
( ~ sQ21_spl
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0) ),
inference(paramodulation,[status(thm)],[f194,f1491]) ).
fof(f1596,plain,
! [X0] : ~ in(X0,X0),
inference(paramodulation,[status(thm)],[f448,f823]) ).
fof(f1616,definition,
! [X0] :
( sQ25_spl
<=> ~ relation(X0) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f1617,plain,
! [X0] :
( ~ sQ25_spl
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f1616]) ).
fof(f1620,plain,
( ~ empty(relation_dom(sK46_skl))
| ~ relation(sK46_skl) ),
inference(resolution,[status(thm)],[f433,f503]) ).
fof(f1621,definition,
( sQ26_spl
<=> relation(sK46_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f1623,plain,
( sQ26_spl
| ~ relation(sK46_skl) ),
inference(component_clause,[status(thm)],[f1621]) ).
fof(f1624,definition,
( sQ27_spl
<=> empty(relation_dom(sK46_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1627,plain,
( ~ sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f1620,f1621,f1624]) ).
fof(f1628,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1623,f504]) ).
fof(f1629,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f1628]) ).
fof(f1648,definition,
( sQ30_spl
<=> empty_set = empty_set ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1679,plain,
! [X0] : ~ in(unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))),
inference(resolution,[status(thm)],[f761,f1063]) ).
fof(f1681,plain,
! [X0] : ~ in(unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0),singleton(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))))),
inference(resolution,[status(thm)],[f761,f1058]) ).
fof(f1683,plain,
! [X0] : ~ in(unordered_pair(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))),
inference(resolution,[status(thm)],[f761,f1220]) ).
fof(f1687,plain,
! [X0] : ~ in(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0))),
inference(resolution,[status(thm)],[f761,f1055]) ).
fof(f1716,plain,
! [X0,X1] :
( ~ sQ21_spl
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X1)
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0) ),
inference(resolution,[status(thm)],[f1569,f776]) ).
fof(f1728,definition,
! [X0] :
( sQ39_spl
<=> ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1729,plain,
! [X0] :
( ~ sQ39_spl
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0) ),
inference(component_clause,[status(thm)],[f1728]) ).
fof(f1731,plain,
( ~ sQ21_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f1716,f1728,f1490]) ).
fof(f1743,plain,
! [X0,X1] : ~ in(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),set_intersection2(X0,singleton(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1)))),
inference(resolution,[status(thm)],[f1687,f775]) ).
fof(f1798,plain,
~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_union2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))),
inference(resolution,[status(thm)],[f1108,f1596]) ).
fof(f1808,plain,
! [X0,X1] : ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(X0,set_intersection2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X1))),
inference(resolution,[status(thm)],[f1112,f775]) ).
fof(f1815,plain,
! [X0] : ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)),
inference(paramodulation,[status(thm)],[f194,f1112]) ).
fof(f2017,definition,
( sQ46_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f2019,plain,
( sQ46_spl
| ~ empty(empty_set) ),
inference(component_clause,[status(thm)],[f2017]) ).
fof(f2049,plain,
! [X0] : element(empty_set,powerset(X0)),
inference(resolution,[status(thm)],[f763,f491]) ).
fof(f2060,plain,
! [X0,X1] :
( ~ in(X1,ordered_pair(sK37_skl(X1,empty_set,X0),sK38_skl(X1,empty_set,X0)))
| X1 = relation_composition(X0,empty_set)
| ~ relation(X1)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f763,f989]) ).
fof(f2061,plain,
! [X0] :
( ~ in(X0,ordered_pair(sK34_skl(X0,empty_set),sK35_skl(X0,empty_set)))
| X0 = relation_inverse(empty_set)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f763,f985]) ).
fof(f2062,plain,
! [X0,X1] :
( ~ in(X1,ordered_pair(sK37_skl(X1,X0,empty_set),sK38_skl(X1,X0,empty_set)))
| X1 = relation_composition(empty_set,X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f763,f987]) ).
fof(f2063,plain,
! [X0,X1] :
( in(ordered_pair(sK39_skl(empty_set,X1,X0),sK38_skl(empty_set,X1,X0)),X1)
| empty_set = relation_composition(X0,X1)
| ~ relation(empty_set)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f763,f375]) ).
fof(f2064,plain,
! [X0,X1] :
( in(ordered_pair(sK37_skl(empty_set,X1,X0),sK39_skl(empty_set,X1,X0)),X0)
| empty_set = relation_composition(X0,X1)
| ~ relation(empty_set)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f763,f374]) ).
fof(f2065,plain,
! [X0] :
( in(ordered_pair(sK35_skl(empty_set,X0),sK34_skl(empty_set,X0)),X0)
| empty_set = relation_inverse(X0)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f763,f361]) ).
fof(f2066,plain,
! [X0] :
( in(sK32_skl(X0,empty_set),X0)
| X0 = relation_rng(empty_set)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f763,f348]) ).
fof(f2067,plain,
( empty_set = empty_set
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f763,f662]) ).
fof(f2068,plain,
! [X0] :
( in(sK25_skl(X0,empty_set),X0)
| X0 = relation_dom(empty_set)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f763,f321]) ).
fof(f2069,plain,
! [X0] :
( subset(empty_set,X0)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f763,f296]) ).
fof(f2070,plain,
! [X0,X1] :
( ~ in(X0,ordered_pair(sK2_skl(X1,X0,empty_set),sK3_skl(X1,X0,empty_set)))
| X0 = relation_dom_restriction(empty_set,X1)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f763,f841]) ).
fof(f2071,plain,
! [X0,X1] :
( in(ordered_pair(sK2_skl(X1,empty_set,X0),sK3_skl(X1,empty_set,X0)),X0)
| empty_set = relation_dom_restriction(X0,X1)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f763,f219]) ).
fof(f2072,plain,
! [X0,X1] :
( in(sK2_skl(X1,empty_set,X0),X1)
| empty_set = relation_dom_restriction(X0,X1)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f763,f218]) ).
fof(f2073,plain,
! [X0] :
( sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f763,f204]) ).
fof(f2074,plain,
! [X0] :
( in(sK0_skl(X0,empty_set),X0)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f763,f203]) ).
fof(f2097,definition,
! [X0] :
( sQ48_spl
<=> in(X0,set_meet(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f2098,plain,
! [X0] :
( ~ sQ48_spl
| in(X0,set_meet(empty_set)) ),
inference(component_clause,[status(thm)],[f2097]) ).
fof(f2102,definition,
! [X0,X1] :
( sQ49_spl
<=> ( ~ in(X1,ordered_pair(sK37_skl(X1,empty_set,X0),sK38_skl(X1,empty_set,X0)))
| X1 = relation_composition(X0,empty_set)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f2105,plain,
( ~ sQ6_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f2060,f2102,f1131]) ).
fof(f2106,definition,
! [X0] :
( sQ50_spl
<=> ( ~ in(X0,ordered_pair(sK34_skl(X0,empty_set),sK35_skl(X0,empty_set)))
| X0 = relation_inverse(empty_set)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f2109,plain,
( sQ50_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2061,f1131,f2106]) ).
fof(f2110,definition,
! [X0,X1] :
( sQ51_spl
<=> ( ~ in(X1,ordered_pair(sK37_skl(X1,X0,empty_set),sK38_skl(X1,X0,empty_set)))
| X1 = relation_composition(empty_set,X0)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f2113,plain,
( sQ51_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2062,f1131,f2110]) ).
fof(f2114,definition,
! [X0,X1] :
( sQ52_spl
<=> ( in(ordered_pair(sK39_skl(empty_set,X1,X0),sK38_skl(empty_set,X1,X0)),X1)
| empty_set = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f2115,plain,
! [X0,X1] :
( ~ sQ52_spl
| in(ordered_pair(sK39_skl(empty_set,X1,X0),sK38_skl(empty_set,X1,X0)),X1)
| empty_set = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f2114]) ).
fof(f2117,plain,
( ~ sQ6_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f2063,f2114,f1131]) ).
fof(f2118,definition,
! [X0,X1] :
( sQ53_spl
<=> ( in(ordered_pair(sK37_skl(empty_set,X1,X0),sK39_skl(empty_set,X1,X0)),X0)
| empty_set = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f2119,plain,
! [X0,X1] :
( ~ sQ53_spl
| in(ordered_pair(sK37_skl(empty_set,X1,X0),sK39_skl(empty_set,X1,X0)),X0)
| empty_set = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f2118]) ).
fof(f2121,plain,
( ~ sQ6_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f2064,f2118,f1131]) ).
fof(f2122,definition,
! [X0] :
( sQ54_spl
<=> ( in(ordered_pair(sK35_skl(empty_set,X0),sK34_skl(empty_set,X0)),X0)
| empty_set = relation_inverse(X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f2123,plain,
! [X0] :
( ~ sQ54_spl
| in(ordered_pair(sK35_skl(empty_set,X0),sK34_skl(empty_set,X0)),X0)
| empty_set = relation_inverse(X0)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f2122]) ).
fof(f2125,plain,
( ~ sQ6_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f2065,f2122,f1131]) ).
fof(f2126,definition,
! [X0] :
( sQ55_spl
<=> ( in(sK32_skl(X0,empty_set),X0)
| X0 = relation_rng(empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f2127,plain,
! [X0] :
( ~ sQ55_spl
| in(sK32_skl(X0,empty_set),X0)
| X0 = relation_rng(empty_set) ),
inference(component_clause,[status(thm)],[f2126]) ).
fof(f2129,plain,
( sQ55_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2066,f1131,f2126]) ).
fof(f2130,plain,
( sQ30_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2067,f1131,f1648]) ).
fof(f2131,definition,
! [X0] :
( sQ56_spl
<=> ( in(sK25_skl(X0,empty_set),X0)
| X0 = relation_dom(empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f2134,plain,
( sQ56_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2068,f1131,f2131]) ).
fof(f2135,definition,
! [X0] :
( sQ57_spl
<=> ( subset(empty_set,X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f2138,plain,
( sQ57_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2069,f1131,f2135]) ).
fof(f2139,definition,
! [X0,X1] :
( sQ58_spl
<=> ( ~ in(X0,ordered_pair(sK2_skl(X1,X0,empty_set),sK3_skl(X1,X0,empty_set)))
| X0 = relation_dom_restriction(empty_set,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f2142,plain,
( sQ58_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2070,f1131,f2139]) ).
fof(f2143,definition,
! [X0,X1] :
( sQ59_spl
<=> ( in(ordered_pair(sK2_skl(X1,empty_set,X0),sK3_skl(X1,empty_set,X0)),X0)
| empty_set = relation_dom_restriction(X0,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f2144,plain,
! [X0,X1] :
( ~ sQ59_spl
| in(ordered_pair(sK2_skl(X1,empty_set,X0),sK3_skl(X1,empty_set,X0)),X0)
| empty_set = relation_dom_restriction(X0,X1)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f2143]) ).
fof(f2146,plain,
( ~ sQ6_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f2071,f2143,f1131]) ).
fof(f2147,definition,
! [X0,X1] :
( sQ60_spl
<=> ( in(sK2_skl(X1,empty_set,X0),X1)
| empty_set = relation_dom_restriction(X0,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f2150,plain,
( ~ sQ6_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f2072,f2147,f1131]) ).
fof(f2151,definition,
! [X0] :
( sQ61_spl
<=> ( sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f2152,plain,
! [X0] :
( ~ sQ61_spl
| sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| empty_set = identity_relation(X0) ),
inference(component_clause,[status(thm)],[f2151]) ).
fof(f2154,plain,
( sQ61_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2073,f1131,f2151]) ).
fof(f2155,definition,
! [X0] :
( sQ62_spl
<=> ( in(sK0_skl(X0,empty_set),X0)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f2156,plain,
! [X0] :
( ~ sQ62_spl
| in(sK0_skl(X0,empty_set),X0)
| empty_set = identity_relation(X0) ),
inference(component_clause,[status(thm)],[f2155]) ).
fof(f2158,plain,
( sQ62_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2074,f1131,f2155]) ).
fof(f2161,definition,
! [X0] :
( sQ63_spl
<=> ~ element(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f2162,plain,
! [X0] :
( ~ sQ63_spl
| ~ element(X0,empty_set) ),
inference(component_clause,[status(thm)],[f2161]) ).
fof(f2166,plain,
! [X0] :
( ~ sQ55_spl
| in(sK32_skl(X0,empty_set),X0)
| X0 = empty_set ),
inference(forward_demodulation,[status(thm)],[f667,f2127]) ).
fof(f2172,plain,
( ~ sQ39_spl
| $false ),
inference(resolution,[status(thm)],[f762,f1729]) ).
fof(f2175,plain,
in(set_intersection2(relation_dom(sK55_skl),sK56_skl),singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))),
inference(paramodulation,[status(thm)],[f1379,f762]) ).
fof(f2176,plain,
~ sQ39_spl,
inference(contradiction_clause,[status(thm)],[f2172]) ).
fof(f2187,plain,
( sQ10_spl
| ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),powerset(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
inference(resolution,[status(thm)],[f764,f1154]) ).
fof(f2210,plain,
( ~ sQ62_spl
| empty_set = identity_relation(empty_set) ),
inference(resolution,[status(thm)],[f2156,f763]) ).
fof(f2214,plain,
! [X0] :
( ~ sQ61_spl
| empty_set = identity_relation(X0)
| ~ in(empty_set,ordered_pair(sK0_skl(X0,empty_set),sK1_skl(X0,empty_set)))
| sK0_skl(X0,empty_set) = sK0_skl(X0,empty_set)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f2152,f837]) ).
fof(f2215,plain,
! [X0] :
( ~ sQ61_spl
| empty_set = identity_relation(X0)
| sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| in(ordered_pair(sK0_skl(X0,empty_set),sK0_skl(X0,empty_set)),empty_set)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f2152,f204]) ).
fof(f2216,plain,
! [X0] :
( ~ sQ61_spl
| empty_set = identity_relation(X0)
| in(sK0_skl(X0,empty_set),X0)
| in(ordered_pair(sK0_skl(X0,empty_set),sK0_skl(X0,empty_set)),empty_set)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f2152,f203]) ).
fof(f2217,definition,
! [X0] :
( sQ64_spl
<=> ( empty_set = identity_relation(X0)
| ~ in(empty_set,ordered_pair(sK0_skl(X0,empty_set),sK1_skl(X0,empty_set)))
| sK0_skl(X0,empty_set) = sK0_skl(X0,empty_set)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f2220,plain,
( ~ sQ61_spl
| sQ64_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2214,f1131,f2217,f2151]) ).
fof(f2221,definition,
! [X0] :
( sQ65_spl
<=> ( empty_set = identity_relation(X0)
| sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| in(ordered_pair(sK0_skl(X0,empty_set),sK0_skl(X0,empty_set)),empty_set)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f2224,plain,
( ~ sQ61_spl
| sQ65_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2215,f1131,f2221,f2151]) ).
fof(f2225,definition,
! [X0] :
( sQ66_spl
<=> ( empty_set = identity_relation(X0)
| in(sK0_skl(X0,empty_set),X0)
| in(ordered_pair(sK0_skl(X0,empty_set),sK0_skl(X0,empty_set)),empty_set)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f2228,plain,
( ~ sQ61_spl
| sQ66_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2216,f1131,f2225,f2151]) ).
fof(f2290,plain,
! [X0] :
( ~ sQ52_spl
| empty_set = relation_composition(X0,empty_set)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f2115,f763]) ).
fof(f2293,definition,
! [X0] :
( sQ71_spl
<=> ( empty_set = relation_composition(X0,empty_set)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f2296,plain,
( ~ sQ52_spl
| ~ sQ6_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f2290,f2293,f1131,f2114]) ).
fof(f2297,plain,
! [X0] :
( ~ sQ53_spl
| empty_set = relation_composition(empty_set,X0)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f2119,f763]) ).
fof(f2300,definition,
! [X0] :
( sQ72_spl
<=> ( empty_set = relation_composition(empty_set,X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f2303,plain,
( ~ sQ53_spl
| sQ72_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2297,f1131,f2300,f2118]) ).
fof(f2304,plain,
( ~ sQ54_spl
| empty_set = relation_inverse(empty_set)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f2123,f763]) ).
fof(f2307,definition,
( sQ73_spl
<=> empty_set = relation_inverse(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f2308,plain,
( ~ sQ73_spl
| empty_set = relation_inverse(empty_set) ),
inference(component_clause,[status(thm)],[f2307]) ).
fof(f2310,plain,
( ~ sQ54_spl
| sQ73_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2304,f1131,f2307,f2122]) ).
fof(f2330,plain,
! [X0] :
( ~ sQ59_spl
| empty_set = relation_dom_restriction(empty_set,X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f2144,f763]) ).
fof(f2333,definition,
! [X0] :
( sQ75_spl
<=> empty_set = relation_dom_restriction(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f2334,plain,
! [X0] :
( ~ sQ75_spl
| empty_set = relation_dom_restriction(empty_set,X0) ),
inference(component_clause,[status(thm)],[f2333]) ).
fof(f2336,plain,
( ~ sQ59_spl
| sQ75_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2330,f1131,f2333,f2143]) ).
fof(f2346,plain,
~ in(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl)),
inference(resolution,[status(thm)],[f2175,f187]) ).
fof(f2365,definition,
( sQ76_spl
<=> empty(powerset(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f2366,plain,
( ~ sQ76_spl
| empty(powerset(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
inference(component_clause,[status(thm)],[f2365]) ).
fof(f2368,definition,
( sQ77_spl
<=> element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),powerset(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f2372,plain,
( sQ9_spl
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f1150,f764]) ).
fof(f2373,plain,
( sQ10_spl
| ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),powerset(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
inference(resolution,[status(thm)],[f1162,f764]) ).
fof(f2381,plain,
( sQ10_spl
| ~ element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),powerset(set_intersection2(relation_dom(sK55_skl),sK56_skl)))
| empty(powerset(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
inference(resolution,[status(thm)],[f2187,f261]) ).
fof(f2385,definition,
( sQ78_spl
<=> empty(powerset(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f2386,plain,
( ~ sQ78_spl
| empty(powerset(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
inference(component_clause,[status(thm)],[f2385]) ).
fof(f2388,definition,
( sQ79_spl
<=> element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),powerset(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f2391,plain,
( sQ10_spl
| ~ sQ79_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f2381,f2385,f2388,f1152]) ).
fof(f2392,plain,
( ~ sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2386,f415]) ).
fof(f2393,plain,
~ sQ78_spl,
inference(contradiction_clause,[status(thm)],[f2392]) ).
fof(f2394,plain,
( sQ11_spl
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f1157,f764]) ).
fof(f2398,plain,
! [X0] :
( sQ11_spl
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(X0,powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
inference(resolution,[status(thm)],[f2394,f775]) ).
fof(f2402,plain,
( sQ11_spl
| ~ element(set_intersection2(relation_dom(sK55_skl),sK56_skl),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| empty(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f2394,f261]) ).
fof(f2403,plain,
! [X0] :
( sQ11_spl
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
inference(resolution,[status(thm)],[f2394,f774]) ).
fof(f2407,definition,
( sQ80_spl
<=> empty(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f2408,plain,
( ~ sQ80_spl
| empty(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(component_clause,[status(thm)],[f2407]) ).
fof(f2410,definition,
( sQ81_spl
<=> element(set_intersection2(relation_dom(sK55_skl),sK56_skl),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f2412,plain,
( sQ81_spl
| ~ element(set_intersection2(relation_dom(sK55_skl),sK56_skl),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(component_clause,[status(thm)],[f2410]) ).
fof(f2413,plain,
( sQ11_spl
| ~ sQ81_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f2402,f2407,f2410,f1155]) ).
fof(f2414,plain,
( ~ sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2408,f415]) ).
fof(f2415,plain,
~ sQ80_spl,
inference(contradiction_clause,[status(thm)],[f2414]) ).
fof(f2448,plain,
! [X0] :
( sQ9_spl
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(X0,powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
inference(resolution,[status(thm)],[f2372,f775]) ).
fof(f2454,definition,
( sQ82_spl
<=> element(set_intersection2(sK56_skl,relation_dom(sK55_skl)),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f2458,plain,
( ~ sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2366,f415]) ).
fof(f2459,plain,
~ sQ76_spl,
inference(contradiction_clause,[status(thm)],[f2458]) ).
fof(f2469,plain,
( sQ10_spl
| ~ element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),powerset(set_intersection2(sK56_skl,relation_dom(sK55_skl))))
| empty(powerset(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
inference(resolution,[status(thm)],[f2373,f261]) ).
fof(f2471,plain,
( sQ10_spl
| ~ sQ77_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f2469,f2365,f2368,f1152]) ).
fof(f2478,plain,
( ~ element(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))
| empty(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f2346,f261]) ).
fof(f2489,definition,
( sQ85_spl
<=> empty(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f2490,plain,
( ~ sQ85_spl
| empty(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(component_clause,[status(thm)],[f2489]) ).
fof(f2492,definition,
( sQ86_spl
<=> element(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f2495,plain,
( ~ sQ86_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f2478,f2489,f2492]) ).
fof(f2518,plain,
( sQ10_spl
| ~ subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),relation_dom(sK55_skl))
| ~ subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl) ),
inference(resolution,[status(thm)],[f545,f1162]) ).
fof(f2525,definition,
( sQ87_spl
<=> subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f2527,plain,
( sQ87_spl
| ~ subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl) ),
inference(component_clause,[status(thm)],[f2525]) ).
fof(f2528,definition,
( sQ88_spl
<=> subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),relation_dom(sK55_skl)) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f2530,plain,
( sQ88_spl
| ~ subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),relation_dom(sK55_skl)) ),
inference(component_clause,[status(thm)],[f2528]) ).
fof(f2531,plain,
( sQ10_spl
| ~ sQ88_spl
| ~ sQ87_spl ),
inference(split_clause,[status(thm)],[f2518,f2525,f2528,f1152]) ).
fof(f2533,plain,
! [X0] :
( subset(empty_set,relation_dom(X0))
| ~ subset(empty_set,X0)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f666,f560]) ).
fof(f2534,plain,
! [X0] :
( subset(relation_dom(X0),empty_set)
| ~ subset(X0,empty_set)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f666,f560]) ).
fof(f2535,definition,
! [X0] :
( sQ89_spl
<=> ( subset(empty_set,relation_dom(X0))
| ~ subset(empty_set,X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2538,plain,
( sQ89_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2533,f1131,f2535]) ).
fof(f2539,definition,
! [X0] :
( sQ90_spl
<=> ( subset(relation_dom(X0),empty_set)
| ~ subset(X0,empty_set)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2542,plain,
( ~ sQ6_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f2534,f2539,f1131]) ).
fof(f2570,definition,
! [X0] :
( sQ91_spl
<=> ~ subset(empty_set,singleton(X0)) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f2571,plain,
! [X0] :
( ~ sQ91_spl
| ~ subset(empty_set,singleton(X0)) ),
inference(component_clause,[status(thm)],[f2570]) ).
fof(f2594,definition,
( sQ92_spl
<=> relation(sK55_skl) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f2596,plain,
( sQ92_spl
| ~ relation(sK55_skl) ),
inference(component_clause,[status(thm)],[f2594]) ).
fof(f2608,plain,
( sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2596,f726]) ).
fof(f2609,plain,
sQ92_spl,
inference(contradiction_clause,[status(thm)],[f2608]) ).
fof(f2610,plain,
( ~ sQ10_spl
| subset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(sK56_skl,relation_dom(sK55_skl))) ),
inference(paramodulation,[status(thm)],[f194,f1153]) ).
fof(f2612,plain,
( ~ sQ10_spl
| sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2610,f1147]) ).
fof(f2613,plain,
( ~ sQ10_spl
| sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f2612]) ).
fof(f2614,plain,
( sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1162,f1145,f1152]) ).
fof(f2667,plain,
( sQ11_spl
| set_difference(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(set_intersection2(relation_dom(sK55_skl),sK56_skl))) = powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(resolution,[status(thm)],[f2394,f683]) ).
fof(f2672,plain,
( sQ11_spl
| set_difference(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) = powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(forward_demodulation,[status(thm)],[f1379,f2667]) ).
fof(f2684,plain,
! [X0] :
( sQ11_spl
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) ),
inference(resolution,[status(thm)],[f2398,f776]) ).
fof(f2698,definition,
( sQ101_spl
<=> in(set_intersection2(relation_dom(sK55_skl),sK56_skl),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f2700,plain,
( sQ101_spl
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(component_clause,[status(thm)],[f2698]) ).
fof(f2701,plain,
( sQ11_spl
| ~ sQ101_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f2684,f1490,f2698,f1155]) ).
fof(f2730,plain,
! [X0] :
( sQ11_spl
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
inference(paramodulation,[status(thm)],[f194,f2403]) ).
fof(f2767,definition,
! [X0] :
( sQ102_spl
<=> ~ in(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),X0) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2768,plain,
! [X0] :
( ~ sQ102_spl
| ~ in(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),X0) ),
inference(component_clause,[status(thm)],[f2767]) ).
fof(f3025,definition,
! [X0] :
( sQ103_spl
<=> ~ subset(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f3026,plain,
! [X0] :
( ~ sQ103_spl
| ~ subset(empty_set,X0) ),
inference(component_clause,[status(thm)],[f3025]) ).
fof(f3029,plain,
( ~ sQ103_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3026,f575]) ).
fof(f3030,plain,
~ sQ103_spl,
inference(contradiction_clause,[status(thm)],[f3029]) ).
fof(f3041,plain,
! [X0] :
( ~ sQ63_spl
| ~ empty(X0)
| ~ empty(empty_set) ),
inference(resolution,[status(thm)],[f264,f2162]) ).
fof(f3043,definition,
! [X0] :
( sQ104_spl
<=> ~ empty(set_intersection2(relation_dom(sK55_skl),X0)) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f3044,plain,
! [X0] :
( ~ sQ104_spl
| ~ empty(set_intersection2(relation_dom(sK55_skl),X0)) ),
inference(component_clause,[status(thm)],[f3043]) ).
fof(f3047,definition,
! [X0] :
( sQ105_spl
<=> ~ empty(set_intersection2(X0,relation_dom(sK55_skl))) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f3048,plain,
! [X0] :
( ~ sQ105_spl
| ~ empty(set_intersection2(X0,relation_dom(sK55_skl))) ),
inference(component_clause,[status(thm)],[f3047]) ).
fof(f3059,definition,
( sQ107_spl
<=> empty(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f3064,definition,
! [X0] :
( sQ108_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f3065,plain,
! [X0] :
( ~ sQ108_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f3064]) ).
fof(f3067,plain,
( ~ sQ63_spl
| sQ108_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f3041,f2017,f3064,f2161]) ).
fof(f3070,plain,
( ~ sQ108_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f507,f3065]) ).
fof(f3089,plain,
~ sQ108_spl,
inference(contradiction_clause,[status(thm)],[f3070]) ).
fof(f3090,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f416,f2019]) ).
fof(f3091,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f3090]) ).
fof(f3092,plain,
( ~ sQ85_spl
| ~ sQ104_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2490,f3044]) ).
fof(f3094,plain,
( ~ sQ85_spl
| ~ sQ104_spl ),
inference(contradiction_clause,[status(thm)],[f3092]) ).
fof(f3163,plain,
( singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))) = empty_set
| ~ subset(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(paramodulation,[status(thm)],[f1346,f1213]) ).
fof(f3164,plain,
singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))) != singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),
inference(paramodulation,[status(thm)],[f1346,f1055]) ).
fof(f3243,definition,
( sQ114_spl
<=> subset(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f3250,definition,
( sQ116_spl
<=> subset(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f3253,definition,
( sQ117_spl
<=> singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f3254,plain,
( ~ sQ117_spl
| singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))) = empty_set ),
inference(component_clause,[status(thm)],[f3253]) ).
fof(f3256,plain,
( sQ117_spl
| ~ sQ116_spl ),
inference(split_clause,[status(thm)],[f3163,f3250,f3253]) ).
fof(f3275,plain,
( ~ sQ117_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3254,f457]) ).
fof(f3276,plain,
~ sQ117_spl,
inference(contradiction_clause,[status(thm)],[f3275]) ).
fof(f3284,plain,
( ~ sQ105_spl
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f950,f3048]) ).
fof(f3288,plain,
( ~ sQ105_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f3284,f2017,f3047]) ).
fof(f3295,plain,
( singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))) = empty_set
| ~ subset(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f3164,f479]) ).
fof(f3307,plain,
( singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) = empty_set
| ~ subset(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
inference(resolution,[status(thm)],[f3164,f479]) ).
fof(f3321,plain,
( sQ117_spl
| ~ sQ114_spl ),
inference(split_clause,[status(thm)],[f3295,f3243,f3253]) ).
fof(f3322,definition,
( sQ120_spl
<=> subset(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f3335,definition,
( sQ123_spl
<=> singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f3336,plain,
( ~ sQ123_spl
| singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) = empty_set ),
inference(component_clause,[status(thm)],[f3335]) ).
fof(f3338,plain,
( sQ123_spl
| ~ sQ120_spl ),
inference(split_clause,[status(thm)],[f3307,f3322,f3335]) ).
fof(f3340,plain,
( ~ sQ123_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3336,f457]) ).
fof(f3341,plain,
~ sQ123_spl,
inference(contradiction_clause,[status(thm)],[f3340]) ).
fof(f3366,plain,
( ~ sQ102_spl
| $false ),
inference(resolution,[status(thm)],[f2768,f768]) ).
fof(f3383,plain,
~ sQ102_spl,
inference(contradiction_clause,[status(thm)],[f3366]) ).
fof(f3631,plain,
! [X0] :
( ~ element(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))))
| empty(singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
inference(resolution,[status(thm)],[f1524,f261]) ).
fof(f3643,definition,
( sQ126_spl
<=> empty(singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f3644,plain,
( ~ sQ126_spl
| empty(singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
inference(component_clause,[status(thm)],[f3643]) ).
fof(f3646,definition,
! [X0] :
( sQ127_spl
<=> ~ element(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f3649,plain,
( sQ127_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f3631,f3643,f3646]) ).
fof(f3650,plain,
( ~ sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3644,f420]) ).
fof(f3651,plain,
~ sQ126_spl,
inference(contradiction_clause,[status(thm)],[f3650]) ).
fof(f3819,plain,
! [X0,X1,X2] :
( in(X0,set_difference(X1,X2))
| ~ in(X0,X1)
| in(X0,set_intersection2(X1,X2)) ),
inference(paramodulation,[status(thm)],[f645,f784]) ).
fof(f3832,plain,
! [X0] :
( sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) != set_intersection2(relation_dom(sK55_skl),sK56_skl)
| ~ in(sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f271,f1055]) ).
fof(f3849,plain,
! [X0] :
( sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) != X0
| ~ in(sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f272,f1055]) ).
fof(f3887,plain,
! [X0,X1,X2] :
( in(X0,set_difference(X2,X1))
| ~ in(X0,X2)
| in(X0,set_intersection2(X1,X2)) ),
inference(paramodulation,[status(thm)],[f194,f3819]) ).
fof(f3890,definition,
! [X0] :
( sQ128_spl
<=> in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_difference(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f3891,plain,
! [X0] :
( ~ sQ128_spl
| in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_difference(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
inference(component_clause,[status(thm)],[f3890]) ).
fof(f3894,definition,
! [X0] :
( sQ129_spl
<=> in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_difference(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f3895,plain,
! [X0] :
( ~ sQ129_spl
| in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_difference(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
inference(component_clause,[status(thm)],[f3894]) ).
fof(f3904,plain,
! [X0] :
( in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_difference(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),X0))
| ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))) ),
inference(resolution,[status(thm)],[f3887,f1455]) ).
fof(f3927,definition,
! [X0] :
( sQ131_spl
<=> in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_difference(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),X0)) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f3928,plain,
! [X0] :
( ~ sQ131_spl
| in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_difference(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),X0)) ),
inference(component_clause,[status(thm)],[f3927]) ).
fof(f3930,plain,
( sQ131_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f3904,f1545,f3927]) ).
fof(f3952,plain,
! [X0] :
( ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0)
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f1815,f776]) ).
fof(f3964,definition,
( sQ132_spl
<=> in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f3967,definition,
! [X0] :
( sQ133_spl
<=> in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_difference(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f3968,plain,
! [X0] :
( ~ sQ133_spl
| in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_difference(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
inference(component_clause,[status(thm)],[f3967]) ).
fof(f3971,plain,
( sQ39_spl
| ~ sQ132_spl ),
inference(split_clause,[status(thm)],[f3952,f3964,f1728]) ).
fof(f3973,plain,
! [X0] :
( ~ element(sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| empty(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) != set_intersection2(relation_dom(sK55_skl),sK56_skl) ),
inference(resolution,[status(thm)],[f3832,f261]) ).
fof(f3982,definition,
! [X0] :
( sQ134_spl
<=> ( ~ element(sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) != set_intersection2(relation_dom(sK55_skl),sK56_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f3985,plain,
( sQ4_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f3973,f3982,f1115]) ).
fof(f3987,plain,
! [X0] :
( ~ element(sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| empty(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) != X0 ),
inference(resolution,[status(thm)],[f3849,f261]) ).
fof(f3996,definition,
! [X0] :
( sQ135_spl
<=> ( ~ element(sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| sK13_skl(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) != X0 ) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f3999,plain,
( sQ4_spl
| sQ135_spl ),
inference(split_clause,[status(thm)],[f3987,f3996,f1115]) ).
fof(f4019,plain,
! [X0] :
( ~ element(unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))))
| empty(singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
inference(resolution,[status(thm)],[f1679,f261]) ).
fof(f4028,definition,
! [X0] :
( sQ136_spl
<=> ~ element(unordered_pair(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f4031,plain,
( sQ136_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f4019,f3643,f4028]) ).
fof(f4050,plain,
! [X0] :
( sQ9_spl
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0) ),
inference(resolution,[status(thm)],[f2448,f776]) ).
fof(f4062,definition,
( sQ137_spl
<=> in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f4064,plain,
( sQ137_spl
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(component_clause,[status(thm)],[f4062]) ).
fof(f4065,definition,
! [X0] :
( sQ138_spl
<=> in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_difference(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f4066,plain,
! [X0] :
( ~ sQ138_spl
| in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_difference(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
inference(component_clause,[status(thm)],[f4065]) ).
fof(f4069,plain,
( sQ9_spl
| ~ sQ137_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f4050,f1728,f4062,f1148]) ).
fof(f4170,plain,
! [X0] :
( ~ element(unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0),singleton(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl)))))
| empty(singleton(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))))) ),
inference(resolution,[status(thm)],[f1681,f261]) ).
fof(f4179,definition,
( sQ139_spl
<=> empty(singleton(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f4180,plain,
( ~ sQ139_spl
| empty(singleton(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))))) ),
inference(component_clause,[status(thm)],[f4179]) ).
fof(f4182,definition,
! [X0] :
( sQ140_spl
<=> ~ element(unordered_pair(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X0),singleton(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f4185,plain,
( sQ140_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f4170,f4179,f4182]) ).
fof(f4186,plain,
( ~ sQ139_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4180,f420]) ).
fof(f4187,plain,
~ sQ139_spl,
inference(contradiction_clause,[status(thm)],[f4186]) ).
fof(f4188,plain,
! [X0] :
( ~ element(unordered_pair(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))))
| empty(singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
inference(resolution,[status(thm)],[f1683,f261]) ).
fof(f4199,definition,
! [X0] :
( sQ141_spl
<=> ~ element(unordered_pair(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f4202,plain,
( sQ141_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f4188,f3643,f4199]) ).
fof(f4248,plain,
! [X0,X1] :
( ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1)
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(X0,singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
inference(resolution,[status(thm)],[f1484,f776]) ).
fof(f4266,definition,
! [X0] :
( sQ142_spl
<=> ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(X0,singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f4269,plain,
( sQ21_spl
| sQ142_spl ),
inference(split_clause,[status(thm)],[f4248,f4266,f1490]) ).
fof(f4284,plain,
! [X0] :
( ~ sQ129_spl
| in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
inference(paramodulation,[status(thm)],[f645,f3895]) ).
fof(f4285,plain,
( ~ sQ129_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4284,f1112]) ).
fof(f4286,plain,
~ sQ129_spl,
inference(contradiction_clause,[status(thm)],[f4285]) ).
fof(f4291,plain,
! [X0] :
( ~ sQ128_spl
| in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
inference(paramodulation,[status(thm)],[f645,f3891]) ).
fof(f4292,plain,
( ~ sQ128_spl
| sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4291,f2403]) ).
fof(f4293,plain,
( ~ sQ128_spl
| sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f4292]) ).
fof(f4294,plain,
( sQ87_spl
| ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),powerset(sK56_skl)) ),
inference(resolution,[status(thm)],[f2527,f764]) ).
fof(f4296,plain,
( sQ87_spl
| ~ element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),powerset(sK56_skl))
| empty(powerset(sK56_skl)) ),
inference(resolution,[status(thm)],[f4294,f261]) ).
fof(f4303,definition,
( sQ143_spl
<=> empty(powerset(sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f4304,plain,
( ~ sQ143_spl
| empty(powerset(sK56_skl)) ),
inference(component_clause,[status(thm)],[f4303]) ).
fof(f4306,definition,
( sQ144_spl
<=> element(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),powerset(sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f4309,plain,
( sQ87_spl
| ~ sQ144_spl
| sQ143_spl ),
inference(split_clause,[status(thm)],[f4296,f4303,f4306,f2525]) ).
fof(f4310,plain,
( ~ sQ143_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4304,f415]) ).
fof(f4311,plain,
~ sQ143_spl,
inference(contradiction_clause,[status(thm)],[f4310]) ).
fof(f4312,plain,
( sQ88_spl
| ~ subset(relation_dom_restriction(sK55_skl,sK56_skl),sK55_skl)
| ~ relation(sK55_skl)
| ~ relation(relation_dom_restriction(sK55_skl,sK56_skl)) ),
inference(resolution,[status(thm)],[f2530,f560]) ).
fof(f4314,definition,
( sQ145_spl
<=> relation(relation_dom_restriction(sK55_skl,sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f4316,plain,
( sQ145_spl
| ~ relation(relation_dom_restriction(sK55_skl,sK56_skl)) ),
inference(component_clause,[status(thm)],[f4314]) ).
fof(f4317,definition,
( sQ146_spl
<=> subset(relation_dom_restriction(sK55_skl,sK56_skl),sK55_skl) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f4319,plain,
( sQ146_spl
| ~ subset(relation_dom_restriction(sK55_skl,sK56_skl),sK55_skl) ),
inference(component_clause,[status(thm)],[f4317]) ).
fof(f4320,plain,
( sQ88_spl
| ~ sQ146_spl
| ~ sQ92_spl
| ~ sQ145_spl ),
inference(split_clause,[status(thm)],[f4312,f4314,f2594,f4317,f2528]) ).
fof(f4321,plain,
( sQ145_spl
| ~ relation(sK55_skl) ),
inference(resolution,[status(thm)],[f4316,f405]) ).
fof(f4323,plain,
( sQ145_spl
| ~ sQ92_spl ),
inference(split_clause,[status(thm)],[f4321,f2594,f4314]) ).
fof(f4324,plain,
( sQ146_spl
| ~ in(relation_dom_restriction(sK55_skl,sK56_skl),powerset(sK55_skl)) ),
inference(resolution,[status(thm)],[f4319,f764]) ).
fof(f4327,plain,
( sQ146_spl
| ~ element(relation_dom_restriction(sK55_skl,sK56_skl),powerset(sK55_skl))
| empty(powerset(sK55_skl)) ),
inference(resolution,[status(thm)],[f4324,f261]) ).
fof(f4334,definition,
( sQ147_spl
<=> empty(powerset(sK55_skl)) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f4335,plain,
( ~ sQ147_spl
| empty(powerset(sK55_skl)) ),
inference(component_clause,[status(thm)],[f4334]) ).
fof(f4337,definition,
( sQ148_spl
<=> element(relation_dom_restriction(sK55_skl,sK56_skl),powerset(sK55_skl)) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f4340,plain,
( sQ146_spl
| ~ sQ148_spl
| sQ147_spl ),
inference(split_clause,[status(thm)],[f4327,f4334,f4337,f4317]) ).
fof(f4341,plain,
( ~ sQ147_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4335,f415]) ).
fof(f4342,plain,
~ sQ147_spl,
inference(contradiction_clause,[status(thm)],[f4341]) ).
fof(f4344,plain,
( ~ sQ11_spl
| subset(set_intersection2(sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(paramodulation,[status(thm)],[f194,f1156]) ).
fof(f4507,plain,
! [X0,X1] :
( in(X0,empty_set)
| ~ in(X0,relation_dom(relation_dom_restriction(empty_set,X1)))
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f666,f710]) ).
fof(f4512,definition,
! [X0,X1] :
( sQ150_spl
<=> ( in(X0,empty_set)
| ~ in(X0,relation_dom(relation_dom_restriction(empty_set,X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f4515,plain,
( sQ150_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f4507,f1131,f4512]) ).
fof(f4611,plain,
( sQ101_spl
| ~ element(set_intersection2(relation_dom(sK55_skl),sK56_skl),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| empty(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f2700,f261]) ).
fof(f4621,plain,
( sQ101_spl
| ~ sQ81_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f4611,f2407,f2410,f2698]) ).
fof(f4623,plain,
( sQ137_spl
| ~ subset(set_intersection2(sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(resolution,[status(thm)],[f4064,f765]) ).
fof(f4625,plain,
( sQ137_spl
| ~ element(set_intersection2(sK56_skl,relation_dom(sK55_skl)),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))
| empty(powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f4064,f261]) ).
fof(f4632,plain,
( sQ137_spl
| ~ sQ82_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f4625,f2407,f2454,f4062]) ).
fof(f4704,plain,
! [X0,X1] :
( ~ in(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1)))
| ~ in(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0) ),
inference(resolution,[status(thm)],[f1743,f776]) ).
fof(f4722,definition,
! [X0] :
( sQ151_spl
<=> ~ in(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f4723,plain,
! [X0] :
( ~ sQ151_spl
| ~ in(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0) ),
inference(component_clause,[status(thm)],[f4722]) ).
fof(f4725,definition,
! [X1] :
( sQ152_spl
<=> ~ in(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),singleton(unordered_pair(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1))) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f4728,plain,
( sQ152_spl
| sQ151_spl ),
inference(split_clause,[status(thm)],[f4704,f4722,f4725]) ).
fof(f4765,plain,
! [X0,X1] :
( ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X1))
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) ),
inference(resolution,[status(thm)],[f1808,f776]) ).
fof(f4784,definition,
! [X1] :
( sQ153_spl
<=> ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_intersection2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X1)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f4787,plain,
( sQ153_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f4765,f1490,f4784]) ).
fof(f4813,plain,
( ~ sQ151_spl
| $false ),
inference(resolution,[status(thm)],[f4723,f768]) ).
fof(f4834,plain,
~ sQ151_spl,
inference(contradiction_clause,[status(thm)],[f4813]) ).
fof(f4849,plain,
! [X0] :
( ~ sQ131_spl
| in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),X0)) ),
inference(paramodulation,[status(thm)],[f645,f3928]) ).
fof(f4850,plain,
( ~ sQ131_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4849,f1169]) ).
fof(f4851,plain,
~ sQ131_spl,
inference(contradiction_clause,[status(thm)],[f4850]) ).
fof(f4854,plain,
! [X0] :
( ~ sQ133_spl
| in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),set_intersection2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),X0)) ),
inference(paramodulation,[status(thm)],[f645,f3968]) ).
fof(f4855,plain,
( ~ sQ133_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4854,f1815]) ).
fof(f4856,plain,
~ sQ133_spl,
inference(contradiction_clause,[status(thm)],[f4855]) ).
fof(f4859,plain,
( sQ11_spl
| ~ sQ138_spl
| in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(paramodulation,[status(thm)],[f2672,f4066]) ).
fof(f4861,plain,
( sQ11_spl
| ~ sQ138_spl
| sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4859,f4064]) ).
fof(f4862,plain,
( sQ11_spl
| ~ sQ138_spl
| sQ137_spl ),
inference(contradiction_clause,[status(thm)],[f4861]) ).
fof(f4865,plain,
! [X0] :
( sQ11_spl
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),X0)
| ~ in(set_intersection2(sK56_skl,relation_dom(sK55_skl)),powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(resolution,[status(thm)],[f2730,f776]) ).
fof(f4879,plain,
( sQ11_spl
| sQ39_spl
| ~ sQ137_spl ),
inference(split_clause,[status(thm)],[f4865,f4062,f1728,f1155]) ).
fof(f4942,plain,
( ~ element(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))))
| empty(singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
inference(resolution,[status(thm)],[f1527,f261]) ).
fof(f4949,definition,
( sQ154_spl
<=> element(singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))),singleton(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f4952,plain,
( ~ sQ154_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f4942,f3643,f4949]) ).
fof(f5017,plain,
! [X0,X1] :
( ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),X1)
| ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(X0,singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))))) ),
inference(resolution,[status(thm)],[f1464,f776]) ).
fof(f5034,definition,
! [X0] :
( sQ155_spl
<=> ~ in(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(X0,singleton(set_intersection2(sK56_skl,relation_dom(sK55_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f5037,plain,
( sQ17_spl
| sQ155_spl ),
inference(split_clause,[status(thm)],[f5017,f5034,f1315]) ).
fof(f5072,plain,
( ~ element(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_union2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl)))
| empty(set_union2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
inference(resolution,[status(thm)],[f1798,f261]) ).
fof(f5085,definition,
( sQ156_spl
<=> empty(set_union2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f5086,plain,
( ~ sQ156_spl
| empty(set_union2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
inference(component_clause,[status(thm)],[f5085]) ).
fof(f5088,definition,
( sQ157_spl
<=> element(set_intersection2(relation_dom(sK55_skl),sK56_skl),set_union2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f5091,plain,
( ~ sQ157_spl
| sQ156_spl ),
inference(split_clause,[status(thm)],[f5072,f5085,f5088]) ).
fof(f5140,plain,
( ~ sQ17_spl
| $false ),
inference(resolution,[status(thm)],[f1316,f768]) ).
fof(f5161,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f5140]) ).
fof(f5244,definition,
! [X0] :
( sQ158_spl
<=> ~ in(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f5245,plain,
! [X0] :
( ~ sQ158_spl
| ~ in(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(component_clause,[status(thm)],[f5244]) ).
fof(f5277,plain,
( ~ sQ55_spl
| ~ sQ158_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = empty_set ),
inference(resolution,[status(thm)],[f5245,f2166]) ).
fof(f5324,plain,
! [X0] :
( ~ sQ158_spl
| ~ in(sK8_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| X0 = set_meet(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = empty_set ),
inference(resolution,[status(thm)],[f5245,f234]) ).
fof(f5325,plain,
! [X0] :
( ~ sQ158_spl
| in(X0,set_meet(set_intersection2(relation_dom(sK55_skl),sK56_skl)))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = empty_set ),
inference(resolution,[status(thm)],[f5245,f757]) ).
fof(f5329,plain,
! [X0] :
( ~ sQ52_spl
| ~ sQ158_spl
| empty_set = relation_composition(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f5245,f2115]) ).
fof(f5330,plain,
! [X0,X1] :
( ~ sQ158_spl
| ~ in(X1,ordered_pair(sK37_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),sK38_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)))
| X1 = relation_composition(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X1)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f5245,f989]) ).
fof(f5331,plain,
( ~ sQ54_spl
| ~ sQ158_spl
| empty_set = relation_inverse(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f2123]) ).
fof(f5332,plain,
! [X0] :
( ~ sQ158_spl
| ~ in(X0,ordered_pair(sK34_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK35_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))))
| X0 = relation_inverse(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f985]) ).
fof(f5333,plain,
! [X0] :
( ~ sQ53_spl
| ~ sQ158_spl
| empty_set = relation_composition(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)
| ~ relation(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f2119]) ).
fof(f5334,plain,
! [X0,X1] :
( ~ sQ158_spl
| ~ in(X1,ordered_pair(sK37_skl(X1,X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK38_skl(X1,X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))))
| X1 = relation_composition(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f987]) ).
fof(f5335,plain,
! [X0,X1] :
( ~ sQ158_spl
| in(ordered_pair(sK39_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0),sK38_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0)),X1)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_composition(X0,X1)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f5245,f375]) ).
fof(f5336,plain,
! [X0,X1] :
( ~ sQ158_spl
| in(ordered_pair(sK37_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0),sK39_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_composition(X0,X1)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f5245,f374]) ).
fof(f5337,plain,
! [X0] :
( ~ sQ158_spl
| in(ordered_pair(sK35_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),sK34_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_inverse(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f5245,f361]) ).
fof(f5338,plain,
! [X0] :
( ~ sQ158_spl
| in(sK32_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| X0 = relation_rng(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f348]) ).
fof(f5340,plain,
! [X0] :
( ~ sQ158_spl
| in(sK25_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| X0 = relation_dom(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f321]) ).
fof(f5341,plain,
! [X0] :
( ~ sQ158_spl
| subset(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)
| ~ relation(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f296]) ).
fof(f5342,plain,
! [X0] :
( ~ sQ59_spl
| ~ sQ158_spl
| empty_set = relation_dom_restriction(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f2144]) ).
fof(f5343,plain,
! [X0,X1] :
( ~ sQ158_spl
| ~ in(X0,ordered_pair(sK2_skl(X1,X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK3_skl(X1,X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))))
| X0 = relation_dom_restriction(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1)
| ~ relation(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f841]) ).
fof(f5344,plain,
! [X0,X1] :
( ~ sQ158_spl
| in(ordered_pair(sK2_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),sK3_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_dom_restriction(X0,X1)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f5245,f219]) ).
fof(f5345,plain,
! [X0,X1] :
( ~ sQ158_spl
| in(sK2_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),X1)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_dom_restriction(X0,X1)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f5245,f218]) ).
fof(f5346,plain,
! [X0] :
( ~ sQ158_spl
| sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) = sK1_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f204]) ).
fof(f5347,plain,
! [X0] :
( ~ sQ158_spl
| in(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f203]) ).
fof(f5354,plain,
! [X0] :
( ~ sQ158_spl
| ~ element(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| empty(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5245,f261]) ).
fof(f5366,plain,
( ~ sQ156_spl
| ~ sQ55_spl
| ~ sQ158_spl
| empty(set_union2(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))),empty_set)) ),
inference(backward_demodulation,[status(thm)],[f5277,f5086]) ).
fof(f5894,definition,
( sQ160_spl
<=> set_intersection2(relation_dom(sK55_skl),sK56_skl) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f5895,plain,
( ~ sQ160_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = empty_set ),
inference(component_clause,[status(thm)],[f5894]) ).
fof(f5896,plain,
( sQ160_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) != empty_set ),
inference(component_clause,[status(thm)],[f5894]) ).
fof(f5897,definition,
! [X0] :
( sQ161_spl
<=> ( ~ in(sK8_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| X0 = set_meet(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f5900,plain,
( ~ sQ158_spl
| sQ161_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f5324,f5894,f5897,f5244]) ).
fof(f5901,definition,
! [X0] :
( sQ162_spl
<=> in(X0,set_meet(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f5902,plain,
! [X0] :
( ~ sQ162_spl
| in(X0,set_meet(set_intersection2(relation_dom(sK55_skl),sK56_skl))) ),
inference(component_clause,[status(thm)],[f5901]) ).
fof(f5904,plain,
( ~ sQ158_spl
| sQ162_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f5325,f5894,f5901,f5244]) ).
fof(f5908,definition,
! [X0] :
( sQ163_spl
<=> ( empty_set = relation_composition(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f5911,definition,
( sQ164_spl
<=> relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f5913,plain,
( sQ164_spl
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(component_clause,[status(thm)],[f5911]) ).
fof(f5914,plain,
( ~ sQ52_spl
| ~ sQ158_spl
| ~ sQ164_spl
| sQ163_spl ),
inference(split_clause,[status(thm)],[f5329,f5908,f5911,f5244,f2114]) ).
fof(f5915,definition,
! [X0,X1] :
( sQ165_spl
<=> ( ~ in(X1,ordered_pair(sK37_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),sK38_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)))
| X1 = relation_composition(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f5918,plain,
( ~ sQ158_spl
| ~ sQ164_spl
| sQ165_spl ),
inference(split_clause,[status(thm)],[f5330,f5915,f5911,f5244]) ).
fof(f5919,definition,
( sQ166_spl
<=> empty_set = relation_inverse(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f5922,plain,
( ~ sQ54_spl
| ~ sQ158_spl
| sQ166_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5331,f5911,f5919,f5244,f2122]) ).
fof(f5923,definition,
! [X0] :
( sQ167_spl
<=> ( ~ in(X0,ordered_pair(sK34_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK35_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))))
| X0 = relation_inverse(set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f5926,plain,
( ~ sQ158_spl
| sQ167_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5332,f5911,f5923,f5244]) ).
fof(f5927,definition,
! [X0] :
( sQ168_spl
<=> ( empty_set = relation_composition(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f5930,plain,
( ~ sQ53_spl
| ~ sQ158_spl
| sQ168_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5333,f5911,f5927,f5244,f2118]) ).
fof(f5931,definition,
! [X0,X1] :
( sQ169_spl
<=> ( ~ in(X1,ordered_pair(sK37_skl(X1,X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK38_skl(X1,X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))))
| X1 = relation_composition(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f5934,plain,
( ~ sQ158_spl
| sQ169_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5334,f5911,f5931,f5244]) ).
fof(f5935,definition,
! [X0,X1] :
( sQ170_spl
<=> ( in(ordered_pair(sK39_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0),sK38_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0)),X1)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f5936,plain,
! [X0,X1] :
( ~ sQ170_spl
| in(ordered_pair(sK39_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0),sK38_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0)),X1)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f5935]) ).
fof(f5938,plain,
( ~ sQ158_spl
| ~ sQ164_spl
| sQ170_spl ),
inference(split_clause,[status(thm)],[f5335,f5935,f5911,f5244]) ).
fof(f5939,definition,
! [X0,X1] :
( sQ171_spl
<=> ( in(ordered_pair(sK37_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0),sK39_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f5940,plain,
! [X0,X1] :
( ~ sQ171_spl
| in(ordered_pair(sK37_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0),sK39_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1,X0)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f5939]) ).
fof(f5942,plain,
( ~ sQ158_spl
| ~ sQ164_spl
| sQ171_spl ),
inference(split_clause,[status(thm)],[f5336,f5939,f5911,f5244]) ).
fof(f5943,definition,
! [X0] :
( sQ172_spl
<=> ( in(ordered_pair(sK35_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),sK34_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_inverse(X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f5944,plain,
! [X0] :
( ~ sQ172_spl
| in(ordered_pair(sK35_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),sK34_skl(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_inverse(X0)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f5943]) ).
fof(f5946,plain,
( ~ sQ158_spl
| ~ sQ164_spl
| sQ172_spl ),
inference(split_clause,[status(thm)],[f5337,f5943,f5911,f5244]) ).
fof(f5947,definition,
! [X0] :
( sQ173_spl
<=> ( in(sK32_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| X0 = relation_rng(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f5950,plain,
( ~ sQ158_spl
| sQ173_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5338,f5911,f5947,f5244]) ).
fof(f5952,definition,
! [X0] :
( sQ174_spl
<=> ( in(sK25_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| X0 = relation_dom(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f5953,plain,
! [X0] :
( ~ sQ174_spl
| in(sK25_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| X0 = relation_dom(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(component_clause,[status(thm)],[f5952]) ).
fof(f5955,plain,
( ~ sQ158_spl
| sQ174_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5340,f5911,f5952,f5244]) ).
fof(f5956,definition,
! [X0] :
( sQ175_spl
<=> ( subset(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f5959,plain,
( ~ sQ158_spl
| sQ175_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5341,f5911,f5956,f5244]) ).
fof(f5960,definition,
! [X0] :
( sQ176_spl
<=> empty_set = relation_dom_restriction(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f5961,plain,
! [X0] :
( ~ sQ176_spl
| empty_set = relation_dom_restriction(set_intersection2(relation_dom(sK55_skl),sK56_skl),X0) ),
inference(component_clause,[status(thm)],[f5960]) ).
fof(f5963,plain,
( ~ sQ59_spl
| ~ sQ158_spl
| sQ176_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5342,f5911,f5960,f5244,f2143]) ).
fof(f5964,definition,
! [X0,X1] :
( sQ177_spl
<=> ( ~ in(X0,ordered_pair(sK2_skl(X1,X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK3_skl(X1,X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))))
| X0 = relation_dom_restriction(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f5967,plain,
( ~ sQ158_spl
| sQ177_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5343,f5911,f5964,f5244]) ).
fof(f5968,definition,
! [X0,X1] :
( sQ178_spl
<=> ( in(ordered_pair(sK2_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),sK3_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_dom_restriction(X0,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f5969,plain,
! [X0,X1] :
( ~ sQ178_spl
| in(ordered_pair(sK2_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),sK3_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_dom_restriction(X0,X1)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f5968]) ).
fof(f5971,plain,
( ~ sQ158_spl
| ~ sQ164_spl
| sQ178_spl ),
inference(split_clause,[status(thm)],[f5344,f5968,f5911,f5244]) ).
fof(f5972,definition,
! [X0,X1] :
( sQ179_spl
<=> ( in(sK2_skl(X1,set_intersection2(relation_dom(sK55_skl),sK56_skl),X0),X1)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_dom_restriction(X0,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f5975,plain,
( ~ sQ158_spl
| ~ sQ164_spl
| sQ179_spl ),
inference(split_clause,[status(thm)],[f5345,f5972,f5911,f5244]) ).
fof(f5976,definition,
! [X0] :
( sQ180_spl
<=> ( sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) = sK1_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f5977,plain,
! [X0] :
( ~ sQ180_spl
| sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) = sK1_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0) ),
inference(component_clause,[status(thm)],[f5976]) ).
fof(f5979,plain,
( ~ sQ158_spl
| sQ180_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5346,f5911,f5976,f5244]) ).
fof(f5980,definition,
! [X0] :
( sQ181_spl
<=> ( in(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f5981,plain,
! [X0] :
( ~ sQ181_spl
| in(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0) ),
inference(component_clause,[status(thm)],[f5980]) ).
fof(f5983,plain,
( ~ sQ158_spl
| sQ181_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f5347,f5911,f5980,f5244]) ).
fof(f5986,definition,
! [X0] :
( sQ182_spl
<=> ~ element(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f5987,plain,
! [X0] :
( ~ sQ182_spl
| ~ element(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(component_clause,[status(thm)],[f5986]) ).
fof(f5989,plain,
( ~ sQ158_spl
| sQ182_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f5354,f2489,f5986,f5244]) ).
fof(f6000,plain,
( ~ sQ156_spl
| ~ sQ55_spl
| ~ sQ158_spl
| empty(singleton(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(forward_demodulation,[status(thm)],[f546,f5366]) ).
fof(f6001,plain,
( ~ sQ156_spl
| ~ sQ55_spl
| ~ sQ158_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6000,f420]) ).
fof(f6002,plain,
( ~ sQ156_spl
| ~ sQ55_spl
| ~ sQ158_spl ),
inference(contradiction_clause,[status(thm)],[f6001]) ).
fof(f6003,plain,
( sQ164_spl
| ~ sQ160_spl
| ~ relation(empty_set) ),
inference(backward_demodulation,[status(thm)],[f5895,f5913]) ).
fof(f6004,plain,
! [X0] :
( ~ sQ182_spl
| ~ sQ160_spl
| ~ element(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f5895,f5987]) ).
fof(f6049,plain,
! [X0] :
( ~ sQ162_spl
| ~ sQ160_spl
| in(X0,set_meet(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f5895,f5902]) ).
fof(f6050,plain,
! [X0] :
( ~ sQ162_spl
| ~ sQ160_spl
| in(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f759,f6049]) ).
fof(f6051,plain,
( ~ sQ162_spl
| ~ sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6050,f763]) ).
fof(f6052,plain,
( ~ sQ162_spl
| ~ sQ160_spl ),
inference(contradiction_clause,[status(thm)],[f6051]) ).
fof(f6073,plain,
( ~ sQ174_spl
| empty_set = relation_dom(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(resolution,[status(thm)],[f5953,f763]) ).
fof(f6094,plain,
! [X0] :
( ~ sQ170_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_composition(X0,empty_set)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f5936,f763]) ).
fof(f6101,definition,
! [X0] :
( sQ183_spl
<=> ( set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_composition(X0,empty_set)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f6104,plain,
( ~ sQ170_spl
| ~ sQ6_spl
| sQ183_spl ),
inference(split_clause,[status(thm)],[f6094,f6101,f1131,f5935]) ).
fof(f6105,plain,
! [X0] :
( ~ sQ171_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_composition(empty_set,X0)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f5940,f763]) ).
fof(f6112,definition,
! [X0] :
( sQ184_spl
<=> ( set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_composition(empty_set,X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f6115,plain,
( ~ sQ171_spl
| sQ184_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f6105,f1131,f6112,f5939]) ).
fof(f6116,plain,
( ~ sQ172_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_inverse(empty_set)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f5944,f763]) ).
fof(f6123,definition,
( sQ185_spl
<=> set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_inverse(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f6124,plain,
( ~ sQ185_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_inverse(empty_set) ),
inference(component_clause,[status(thm)],[f6123]) ).
fof(f6125,plain,
( sQ185_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) != relation_inverse(empty_set) ),
inference(component_clause,[status(thm)],[f6123]) ).
fof(f6126,plain,
( ~ sQ172_spl
| sQ185_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f6116,f1131,f6123,f5943]) ).
fof(f6127,plain,
( ~ sQ185_spl
| ~ sQ73_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = empty_set ),
inference(forward_demodulation,[status(thm)],[f2308,f6124]) ).
fof(f6128,plain,
( ~ sQ185_spl
| ~ sQ73_spl
| sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6127,f5896]) ).
fof(f6129,plain,
( ~ sQ185_spl
| ~ sQ73_spl
| sQ160_spl ),
inference(contradiction_clause,[status(thm)],[f6128]) ).
fof(f6573,plain,
( sQ81_spl
| ~ sQ185_spl
| ~ sQ73_spl
| ~ element(empty_set,powerset(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))) ),
inference(backward_demodulation,[status(thm)],[f6127,f2412]) ).
fof(f6620,plain,
( sQ164_spl
| ~ sQ160_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f6003,f1131,f5894,f5911]) ).
fof(f6621,plain,
( ~ sQ182_spl
| ~ sQ160_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f6004,f2161,f5894,f5986]) ).
fof(f7413,plain,
( sQ81_spl
| ~ sQ185_spl
| ~ sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6573,f2049]) ).
fof(f7414,plain,
( sQ81_spl
| ~ sQ185_spl
| ~ sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f7413]) ).
fof(f7415,plain,
( sQ185_spl
| ~ sQ73_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) != empty_set ),
inference(forward_demodulation,[status(thm)],[f2308,f6125]) ).
fof(f7427,plain,
( ~ sQ181_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(empty_set) ),
inference(resolution,[status(thm)],[f5981,f763]) ).
fof(f7432,plain,
( ~ sQ181_spl
| ~ sQ62_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = empty_set ),
inference(forward_demodulation,[status(thm)],[f2210,f7427]) ).
fof(f7433,plain,
( ~ sQ181_spl
| ~ sQ62_spl
| sQ185_spl
| ~ sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7432,f7415]) ).
fof(f7434,plain,
( ~ sQ181_spl
| ~ sQ62_spl
| sQ185_spl
| ~ sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f7433]) ).
fof(f7445,plain,
! [X0] :
( ~ sQ180_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),ordered_pair(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK1_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))))
| sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) = sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(paramodulation,[status(thm)],[f5977,f837]) ).
fof(f7446,plain,
! [X0] :
( ~ sQ180_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) = sK1_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| in(ordered_pair(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(paramodulation,[status(thm)],[f5977,f204]) ).
fof(f7447,plain,
! [X0] :
( ~ sQ180_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| in(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| in(ordered_pair(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(paramodulation,[status(thm)],[f5977,f203]) ).
fof(f7448,definition,
! [X0] :
( sQ186_spl
<=> ( set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),ordered_pair(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK1_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))))
| sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) = sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f7451,plain,
( ~ sQ180_spl
| sQ186_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f7445,f5911,f7448,f5976]) ).
fof(f7452,definition,
! [X0] :
( sQ187_spl
<=> ( set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)) = sK1_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| in(ordered_pair(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f7455,plain,
( ~ sQ180_spl
| sQ187_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f7446,f5911,f7452,f5976]) ).
fof(f7456,definition,
! [X0] :
( sQ188_spl
<=> ( set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| in(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| in(ordered_pair(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f7457,plain,
! [X0] :
( ~ sQ188_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0)
| in(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| in(ordered_pair(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0) ),
inference(component_clause,[status(thm)],[f7456]) ).
fof(f7459,plain,
( ~ sQ180_spl
| sQ188_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f7447,f5911,f7456,f5976]) ).
fof(f7460,plain,
! [X0] :
( ~ sQ188_spl
| in(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| in(ordered_pair(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))),set_intersection2(relation_dom(sK55_skl),sK56_skl))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f7457]) ).
fof(f7462,plain,
! [X0] :
( ~ sQ178_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_dom_restriction(empty_set,X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f5969,f763]) ).
fof(f7469,definition,
! [X0] :
( sQ189_spl
<=> set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_dom_restriction(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f7470,plain,
! [X0] :
( ~ sQ189_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = relation_dom_restriction(empty_set,X0) ),
inference(component_clause,[status(thm)],[f7469]) ).
fof(f7472,plain,
( ~ sQ178_spl
| sQ189_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f7462,f1131,f7469,f5968]) ).
fof(f7473,plain,
( ~ sQ189_spl
| ~ sQ75_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = empty_set ),
inference(forward_demodulation,[status(thm)],[f2334,f7470]) ).
fof(f7474,plain,
( ~ sQ189_spl
| ~ sQ75_spl
| sQ185_spl
| ~ sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7473,f7415]) ).
fof(f7475,plain,
( ~ sQ189_spl
| ~ sQ75_spl
| sQ185_spl
| ~ sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f7474]) ).
fof(f7476,plain,
! [X0] :
( ~ sQ188_spl
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),ordered_pair(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl))))
| in(sK0_skl(X0,set_intersection2(relation_dom(sK55_skl),sK56_skl)),X0)
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(X0) ),
inference(resolution,[status(thm)],[f7460,f187]) ).
fof(f7484,plain,
( ~ sQ188_spl
| ~ in(set_intersection2(relation_dom(sK55_skl),sK56_skl),ordered_pair(sK0_skl(empty_set,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK0_skl(empty_set,set_intersection2(relation_dom(sK55_skl),sK56_skl))))
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(empty_set) ),
inference(resolution,[status(thm)],[f7476,f763]) ).
fof(f7489,definition,
( sQ190_spl
<=> set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f7490,plain,
( ~ sQ190_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = identity_relation(empty_set) ),
inference(component_clause,[status(thm)],[f7489]) ).
fof(f7492,definition,
( sQ191_spl
<=> in(set_intersection2(relation_dom(sK55_skl),sK56_skl),ordered_pair(sK0_skl(empty_set,set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK0_skl(empty_set,set_intersection2(relation_dom(sK55_skl),sK56_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f7495,plain,
( ~ sQ188_spl
| ~ sQ191_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f7484,f7489,f7492,f7456]) ).
fof(f7496,plain,
( ~ sQ190_spl
| ~ sQ62_spl
| set_intersection2(relation_dom(sK55_skl),sK56_skl) = empty_set ),
inference(forward_demodulation,[status(thm)],[f2210,f7490]) ).
fof(f7497,plain,
( ~ sQ190_spl
| ~ sQ62_spl
| sQ185_spl
| ~ sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7496,f7415]) ).
fof(f7498,plain,
( ~ sQ190_spl
| ~ sQ62_spl
| sQ185_spl
| ~ sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f7497]) ).
fof(f7499,plain,
( ~ sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2571,f575]) ).
fof(f7500,plain,
~ sQ91_spl,
inference(contradiction_clause,[status(thm)],[f7499]) ).
fof(f7501,plain,
! [X0] :
( ~ sQ48_spl
| in(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f759,f2098]) ).
fof(f7502,plain,
( ~ sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7501,f763]) ).
fof(f7503,plain,
~ sQ48_spl,
inference(contradiction_clause,[status(thm)],[f7502]) ).
fof(f7507,plain,
( ~ sQ25_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f398,f1617]) ).
fof(f7525,plain,
~ sQ25_spl,
inference(contradiction_clause,[status(thm)],[f7507]) ).
fof(f7643,plain,
( ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),sK56_skl)
| ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(sK55_skl))
| ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(resolution,[status(thm)],[f311,f727]) ).
fof(f7650,definition,
( sQ192_spl
<=> in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f7651,plain,
( ~ sQ192_spl
| in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(component_clause,[status(thm)],[f7650]) ).
fof(f7652,plain,
( sQ192_spl
| ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(component_clause,[status(thm)],[f7650]) ).
fof(f7653,definition,
( sQ193_spl
<=> in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(sK55_skl)) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f7655,plain,
( sQ193_spl
| ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(sK55_skl)) ),
inference(component_clause,[status(thm)],[f7653]) ).
fof(f7656,definition,
( sQ194_spl
<=> in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f7658,plain,
( sQ194_spl
| ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),sK56_skl) ),
inference(component_clause,[status(thm)],[f7656]) ).
fof(f7659,plain,
( ~ sQ194_spl
| ~ sQ193_spl
| ~ sQ192_spl ),
inference(split_clause,[status(thm)],[f7643,f7650,f7653,f7656]) ).
fof(f7779,plain,
( sQ11_spl
| ~ in(sK22_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(resolution,[status(thm)],[f1157,f304]) ).
fof(f7799,definition,
( sQ198_spl
<=> relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) = set_intersection2(relation_dom(sK55_skl),sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f7800,plain,
( ~ sQ198_spl
| relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) = set_intersection2(relation_dom(sK55_skl),sK56_skl) ),
inference(component_clause,[status(thm)],[f7799]) ).
fof(f7810,plain,
( ~ sQ198_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7800,f727]) ).
fof(f7811,plain,
~ sQ198_spl,
inference(contradiction_clause,[status(thm)],[f7810]) ).
fof(f7827,plain,
( sQ192_spl
| in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(sK55_skl))
| relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) = set_intersection2(relation_dom(sK55_skl),sK56_skl) ),
inference(resolution,[status(thm)],[f7652,f312]) ).
fof(f7828,plain,
( sQ192_spl
| ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(sK55_skl))
| ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),sK56_skl)
| ~ relation(sK55_skl) ),
inference(resolution,[status(thm)],[f7652,f711]) ).
fof(f7830,plain,
( sQ192_spl
| ~ element(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))
| empty(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(resolution,[status(thm)],[f7652,f261]) ).
fof(f7838,plain,
( sQ192_spl
| sQ193_spl
| sQ198_spl ),
inference(split_clause,[status(thm)],[f7827,f7799,f7653,f7650]) ).
fof(f7839,plain,
( sQ192_spl
| ~ sQ193_spl
| ~ sQ194_spl
| ~ sQ92_spl ),
inference(split_clause,[status(thm)],[f7828,f2594,f7656,f7653,f7650]) ).
fof(f7840,definition,
( sQ202_spl
<=> element(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f7843,plain,
( sQ192_spl
| ~ sQ202_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f7830,f3059,f7840,f7650]) ).
fof(f7879,plain,
! [X0] :
( sQ193_spl
| ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,X0)))
| ~ relation(sK55_skl) ),
inference(resolution,[status(thm)],[f710,f7655]) ).
fof(f7888,definition,
! [X0] :
( sQ203_spl
<=> ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,X0))) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f7889,plain,
! [X0] :
( ~ sQ203_spl
| ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(sK55_skl,X0))) ),
inference(component_clause,[status(thm)],[f7888]) ).
fof(f7891,plain,
( sQ193_spl
| sQ203_spl
| ~ sQ92_spl ),
inference(split_clause,[status(thm)],[f7879,f2594,f7888,f7653]) ).
fof(f7893,plain,
( ~ sQ192_spl
| ~ sQ203_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f7651,f7889]) ).
fof(f7894,plain,
( ~ sQ192_spl
| ~ sQ203_spl ),
inference(contradiction_clause,[status(thm)],[f7893]) ).
fof(f7933,plain,
( sQ185_spl
| ~ sQ73_spl
| ~ subset(empty_set,set_intersection2(relation_dom(sK55_skl),sK56_skl))
| ~ subset(set_intersection2(relation_dom(sK55_skl),sK56_skl),empty_set) ),
inference(resolution,[status(thm)],[f7415,f209]) ).
fof(f7941,plain,
( sQ185_spl
| ~ sQ73_spl
| set_intersection2(sK56_skl,relation_dom(sK55_skl)) != empty_set ),
inference(paramodulation,[status(thm)],[f194,f7415]) ).
fof(f7944,definition,
( sQ204_spl
<=> subset(set_intersection2(relation_dom(sK55_skl),sK56_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f7947,definition,
( sQ205_spl
<=> subset(empty_set,set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f7949,plain,
( sQ205_spl
| ~ subset(empty_set,set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(component_clause,[status(thm)],[f7947]) ).
fof(f7950,plain,
( sQ185_spl
| ~ sQ73_spl
| ~ sQ205_spl
| ~ sQ204_spl ),
inference(split_clause,[status(thm)],[f7933,f7944,f7947,f2307,f6123]) ).
fof(f7963,plain,
( sQ205_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7949,f575]) ).
fof(f7964,plain,
sQ205_spl,
inference(contradiction_clause,[status(thm)],[f7963]) ).
fof(f7970,plain,
! [X0] :
( sQ194_spl
| ~ in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),relation_dom(relation_dom_restriction(X0,sK56_skl)))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f7658,f709]) ).
fof(f7990,plain,
( sQ185_spl
| ~ sQ73_spl
| ~ subset(empty_set,set_intersection2(sK56_skl,relation_dom(sK55_skl)))
| ~ subset(set_intersection2(sK56_skl,relation_dom(sK55_skl)),empty_set) ),
inference(resolution,[status(thm)],[f7941,f209]) ).
fof(f7999,definition,
( sQ209_spl
<=> subset(set_intersection2(sK56_skl,relation_dom(sK55_skl)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f8002,definition,
( sQ210_spl
<=> subset(empty_set,set_intersection2(sK56_skl,relation_dom(sK55_skl))) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f8004,plain,
( sQ210_spl
| ~ subset(empty_set,set_intersection2(sK56_skl,relation_dom(sK55_skl))) ),
inference(component_clause,[status(thm)],[f8002]) ).
fof(f8005,plain,
( sQ185_spl
| ~ sQ73_spl
| ~ sQ210_spl
| ~ sQ209_spl ),
inference(split_clause,[status(thm)],[f7990,f7999,f8002,f2307,f6123]) ).
fof(f8017,plain,
( sQ210_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8004,f575]) ).
fof(f8018,plain,
sQ210_spl,
inference(contradiction_clause,[status(thm)],[f8017]) ).
fof(f8021,plain,
! [X0,X1] :
( ~ sQ174_spl
| in(X0,empty_set)
| ~ in(X0,relation_dom(relation_dom_restriction(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1)))
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(paramodulation,[status(thm)],[f6073,f710]) ).
fof(f8023,definition,
! [X0,X1] :
( sQ214_spl
<=> ( in(X0,empty_set)
| ~ in(X0,relation_dom(relation_dom_restriction(set_intersection2(relation_dom(sK55_skl),sK56_skl),X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f8026,plain,
( ~ sQ174_spl
| sQ214_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f8021,f5911,f8023,f5952]) ).
fof(f8050,definition,
( sQ215_spl
<=> relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) = set_intersection2(sK56_skl,relation_dom(sK55_skl)) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f8051,plain,
( ~ sQ215_spl
| relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) = set_intersection2(sK56_skl,relation_dom(sK55_skl)) ),
inference(component_clause,[status(thm)],[f8050]) ).
fof(f8065,plain,
( ~ sQ215_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8051,f821]) ).
fof(f8066,plain,
~ sQ215_spl,
inference(contradiction_clause,[status(thm)],[f8065]) ).
fof(f8082,plain,
( sQ11_spl
| ~ in(sK22_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)),relation_dom(sK55_skl))
| ~ in(sK22_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK56_skl)
| ~ relation(sK55_skl) ),
inference(resolution,[status(thm)],[f7779,f711]) ).
fof(f8083,plain,
! [X0] :
( sQ11_spl
| ~ in(sK22_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)),relation_dom(relation_dom_restriction(relation_dom_restriction(sK55_skl,sK56_skl),X0)))
| ~ relation(relation_dom_restriction(sK55_skl,sK56_skl)) ),
inference(resolution,[status(thm)],[f7779,f710]) ).
fof(f8086,plain,
( sQ11_spl
| ~ element(sK22_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)))
| empty(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
inference(resolution,[status(thm)],[f7779,f261]) ).
fof(f8095,definition,
( sQ220_spl
<=> in(sK22_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)),sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f8098,definition,
( sQ221_spl
<=> in(sK22_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)),relation_dom(sK55_skl)) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f8101,plain,
( sQ11_spl
| ~ sQ221_spl
| ~ sQ220_spl
| ~ sQ92_spl ),
inference(split_clause,[status(thm)],[f8082,f2594,f8095,f8098,f1155]) ).
fof(f8102,definition,
! [X0] :
( sQ222_spl
<=> ~ in(sK22_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)),relation_dom(relation_dom_restriction(relation_dom_restriction(sK55_skl,sK56_skl),X0))) ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f8105,plain,
( sQ11_spl
| sQ222_spl
| ~ sQ145_spl ),
inference(split_clause,[status(thm)],[f8083,f4314,f8102,f1155]) ).
fof(f8106,definition,
( sQ223_spl
<=> element(sK22_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),set_intersection2(relation_dom(sK55_skl),sK56_skl)),relation_dom(relation_dom_restriction(sK55_skl,sK56_skl))) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f8109,plain,
( sQ11_spl
| ~ sQ223_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f8086,f3059,f8106,f1155]) ).
fof(f8160,definition,
( sQ226_spl
<=> subset(sK56_skl,sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f8162,plain,
( sQ226_spl
| ~ subset(sK56_skl,sK56_skl) ),
inference(component_clause,[status(thm)],[f8160]) ).
fof(f8170,plain,
( sQ226_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8162,f751]) ).
fof(f8171,plain,
sQ226_spl,
inference(contradiction_clause,[status(thm)],[f8170]) ).
fof(f8172,plain,
( ~ sQ11_spl
| sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4344,f4623]) ).
fof(f8173,plain,
( ~ sQ11_spl
| sQ137_spl ),
inference(contradiction_clause,[status(thm)],[f8172]) ).
fof(f8218,plain,
! [X0,X1] :
( ~ sQ176_spl
| ~ in(X0,relation_dom(set_intersection2(relation_dom(sK55_skl),sK56_skl)))
| ~ in(X0,X1)
| in(X0,relation_dom(empty_set))
| ~ relation(set_intersection2(relation_dom(sK55_skl),sK56_skl)) ),
inference(paramodulation,[status(thm)],[f5961,f711]) ).
fof(f8220,definition,
! [X0,X1] :
( sQ230_spl
<=> ( ~ in(X0,relation_dom(set_intersection2(relation_dom(sK55_skl),sK56_skl)))
| ~ in(X0,X1)
| in(X0,relation_dom(empty_set)) ) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f8223,plain,
( ~ sQ176_spl
| sQ230_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f8218,f5911,f8220,f5960]) ).
fof(f8380,plain,
( sQ194_spl
| in(sK23_skl(relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)),sK56_skl,relation_dom(sK55_skl)),sK56_skl)
| relation_dom(relation_dom_restriction(sK55_skl,sK56_skl)) = set_intersection2(relation_dom(sK55_skl),sK56_skl)
| ~ relation(sK55_skl) ),
inference(resolution,[status(thm)],[f7970,f313]) ).
fof(f8394,plain,
( sQ194_spl
| sQ198_spl
| ~ sQ92_spl ),
inference(split_clause,[status(thm)],[f8380,f2594,f7799,f7656]) ).
fof(f8401,plain,
$false,
inference(sat_refutation,[status(thm)],[f1083,f1087,f1103,f1105,f1121,f1123,f1137,f1139,f1151,f1158,f1176,f1178,f1189,f1295,f1299,f1321,f1496,f1627,f1629,f1731,f2105,f2109,f2113,f2117,f2121,f2125,f2129,f2130,f2134,f2138,f2142,f2146,f2150,f2154,f2158,f2176,f2220,f2224,f2228,f2296,f2303,f2310,f2336,f2391,f2393,f2413,f2415,f2459,f2471,f2495,f2531,f2538,f2542,f2609,f2613,f2614,f2701,f3030,f3067,f3089,f3091,f3094,f3256,f3276,f3288,f3321,f3338,f3341,f3383,f3649,f3651,f3930,f3971,f3985,f3999,f4031,f4069,f4185,f4187,f4202,f4269,f4286,f4293,f4309,f4311,f4320,f4323,f4340,f4342,f4515,f4621,f4632,f4728,f4787,f4834,f4851,f4856,f4862,f4879,f4952,f5037,f5091,f5161,f5900,f5904,f5914,f5918,f5922,f5926,f5930,f5934,f5938,f5942,f5946,f5950,f5955,f5959,f5963,f5967,f5971,f5975,f5979,f5983,f5989,f6002,f6052,f6104,f6115,f6126,f6129,f6620,f6621,f7414,f7434,f7451,f7455,f7459,f7472,f7475,f7495,f7498,f7500,f7503,f7525,f7659,f7811,f7838,f7839,f7843,f7891,f7894,f7950,f7964,f8005,f8018,f8026,f8066,f8101,f8105,f8109,f8171,f8173,f8223,f8394]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU194+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.60 % Computer : n020.cluster.edu
% 0.14/0.60 % Model : x86_64 x86_64
% 0.14/0.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.60 % Memory : 8046.5625MB
% 0.14/0.60 % OS : Linux 6.8.0-71-generic
% 0.14/0.61 % CPULimit : 300
% 0.14/0.61 % WCLimit : 300
% 0.14/0.61 % DateTime : Mon Sep 21 05:57:35 UTC 2026
% 0.16/0.61 % CPUTime :
% 0.16/0.64 % Drodi V4.1.1
% 76.48/10.42 % Refutation found
% 76.48/10.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 76.48/10.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.00/10.59 % Elapsed time: 9.957731 seconds
% 7.00/10.59 % CPU time: 77.837153 seconds
% 7.00/10.59 % Total memory used: 436.179 MB
% 7.00/10.59 % Net memory used: 373.800 MB
%------------------------------------------------------------------------------