%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU181+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:34 PM UTC 2026
% Result : Theorem 22.96s 3.56s
% Output : CNFRefutation 20.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 166
% Syntax : Number of formulae : 647 ( 9 unt; 156 def)
% Number of atoms : 2074 ( 117 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 2729 (1302 ~;1204 |; 42 &)
% ( 171 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 163 ( 161 usr; 157 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 1 con; 0-3 aty)
% Number of variables : 630 ( 607 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,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/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( relation(A)
=> relation(relation_inverse(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,conjecture,
! [A] :
( relation(A)
=> ( relation_dom(A) = relation_rng(relation_inverse(A))
& relation_rng(A) = relation_dom(relation_inverse(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( relation_dom(A) = relation_rng(relation_inverse(A))
& relation_rng(A) = relation_dom(relation_inverse(A)) ) ),
inference(negated_conjecture,[status(cth)],[f33]) ).
fof(f41,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f42,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f44,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f45,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)],[f44]) ).
fof(f46,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f48,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f49,plain,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,B)
| ~ in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f50,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)],[f49]) ).
fof(f51,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)],[f50]) ).
fof(f52,plain,
( ! [A,B] :
( ( ~ in(sK0_skl(B,A),B)
& in(sK0_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f51]) ).
fof(f53,plain,
! [X0,X1,X2] :
( in(X2,X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f54,plain,
! [X0,X1] :
( in(sK0_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f55,plain,
! [X0,X1] :
( ~ in(sK0_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f56,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)],[f5]) ).
fof(f57,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)],[f56]) ).
fof(f58,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)],[f57]) ).
fof(f59,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK2_skl(B,A),sK3_skl(B,A)),A)
| in(sK2_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(sK2_skl(B,A),D),A)
| ~ in(sK2_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,sK1_skl(C,B,A)),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl]),skolemize(D,sK1_skl(C,B,A)),skolemize(C,sK2_skl(B,A)),skolemize(D,sK3_skl(B,A))],[f58]) ).
fof(f60,plain,
! [X0,X1,X2] :
( in(ordered_pair(X2,sK1_skl(X2,X1,X0)),X0)
| ~ in(X2,X1)
| X1 != relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,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)],[f59]) ).
fof(f62,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(sK2_skl(X1,X0),X2),X0)
| ~ in(sK2_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f63,plain,
! [X0,X1] :
( in(ordered_pair(sK2_skl(X1,X0),sK3_skl(X1,X0)),X0)
| in(sK2_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f64,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)],[f6]) ).
fof(f65,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)],[f64]) ).
fof(f66,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)],[f65]) ).
fof(f67,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK6_skl(B,A),sK5_skl(B,A)),A)
| in(sK5_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(D,sK5_skl(B,A)),A)
| ~ in(sK5_skl(B,A),B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(sK4_skl(C,B,A),C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(D,sK4_skl(C,B,A)),skolemize(C,sK5_skl(B,A)),skolemize(D,sK6_skl(B,A))],[f66]) ).
fof(f68,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK4_skl(X2,X1,X0),X2),X0)
| ~ in(X2,X1)
| X1 != relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(X3,X2),X0)
| in(X2,X1)
| X1 != relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f70,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X2,sK5_skl(X1,X0)),X0)
| ~ in(sK5_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f71,plain,
! [X0,X1] :
( in(ordered_pair(sK6_skl(X1,X0),sK5_skl(X1,X0)),X0)
| in(sK5_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f73,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)],[f8]) ).
fof(f74,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)],[f73]) ).
fof(f75,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)],[f74]) ).
fof(f76,plain,
! [A] :
( ! [B] :
( ( ( ( ( in(ordered_pair(sK8_skl(B,A),sK7_skl(B,A)),A)
| in(ordered_pair(sK7_skl(B,A),sK8_skl(B,A)),B) )
& ( ~ in(ordered_pair(sK8_skl(B,A),sK7_skl(B,A)),A)
| ~ in(ordered_pair(sK7_skl(B,A),sK8_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,[sK7_skl,sK8_skl]),skolemize(C,sK7_skl(B,A)),skolemize(D,sK8_skl(B,A))],[f75]) ).
fof(f77,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(X3,X2),X0)
| ~ in(ordered_pair(X2,X3),X1)
| X1 != relation_inverse(X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(X3,X2),X0)
| in(ordered_pair(X2,X3),X1)
| X1 != relation_inverse(X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f80,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(X1,X0),sK7_skl(X1,X0)),X0)
| in(ordered_pair(sK7_skl(X1,X0),sK8_skl(X1,X0)),X1)
| X1 = relation_inverse(X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f81,plain,
! [A] :
( relation(relation_inverse(A))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f82,plain,
! [X0] :
( relation(relation_inverse(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f87,plain,
! [X0,X1] : ~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f110,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f111,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f112,plain,
? [A] :
( ( relation_dom(A) != relation_rng(relation_inverse(A))
| relation_rng(A) != relation_dom(relation_inverse(A)) )
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f113,plain,
( ( relation_dom(sK15_skl) != relation_rng(relation_inverse(sK15_skl))
| relation_rng(sK15_skl) != relation_dom(relation_inverse(sK15_skl)) )
& relation(sK15_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f112]) ).
fof(f114,plain,
relation(sK15_skl),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
( relation_dom(sK15_skl) != relation_rng(relation_inverse(sK15_skl))
| relation_rng(sK15_skl) != relation_dom(relation_inverse(sK15_skl)) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f134,definition,
( sQ0_spl
<=> relation_rng(sK15_skl) = relation_dom(relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f135,plain,
( ~ sQ0_spl
| relation_rng(sK15_skl) = relation_dom(relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f134]) ).
fof(f136,plain,
( sQ0_spl
| relation_rng(sK15_skl) != relation_dom(relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f134]) ).
fof(f137,definition,
( sQ1_spl
<=> relation_dom(sK15_skl) = relation_rng(relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f138,plain,
( ~ sQ1_spl
| relation_dom(sK15_skl) = relation_rng(relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f137]) ).
fof(f139,plain,
( sQ1_spl
| relation_dom(sK15_skl) != relation_rng(relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f137]) ).
fof(f140,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f115,f134,f137]) ).
fof(f141,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f46]) ).
fof(f143,plain,
! [X0,X1] :
( in(ordered_pair(X1,sK1_skl(X1,relation_dom(X0),X0)),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f60]) ).
fof(f144,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),X0)
| in(X1,relation_dom(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f61]) ).
fof(f145,plain,
! [X0,X1] :
( in(ordered_pair(sK4_skl(X1,relation_rng(X0),X0),X1),X0)
| ~ in(X1,relation_rng(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f68]) ).
fof(f146,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X2,X1),X0)
| in(X1,relation_rng(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f69]) ).
fof(f147,plain,
! [X0,X1,X2] :
( in(ordered_pair(X2,X1),X0)
| ~ in(ordered_pair(X1,X2),relation_inverse(X0))
| ~ relation(relation_inverse(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f77]) ).
fof(f148,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X2,X1),X0)
| in(ordered_pair(X1,X2),relation_inverse(X0))
| ~ relation(relation_inverse(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f78]) ).
fof(f149,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X2,X1),X0)
| in(ordered_pair(X1,X2),relation_inverse(X0))
| ~ relation(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f148,f82]) ).
fof(f150,plain,
! [X0,X1,X2] :
( in(ordered_pair(X2,X1),X0)
| ~ in(ordered_pair(X1,X2),relation_inverse(X0))
| ~ relation(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f147,f82]) ).
fof(f151,plain,
! [X0,X1] :
( ~ in(ordered_pair(X1,relation_rng(X0)),X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f42,f146]) ).
fof(f152,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X2,X1),X0)
| ~ relation(X0)
| ~ in(relation_rng(X0),X1) ),
inference(resolution,[status(thm)],[f42,f146]) ).
fof(f153,plain,
! [X0,X1] :
( ~ in(ordered_pair(relation_dom(X0),X1),X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f42,f144]) ).
fof(f154,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),X0)
| ~ relation(X0)
| ~ in(relation_dom(X0),X1) ),
inference(resolution,[status(thm)],[f42,f144]) ).
fof(f161,plain,
( sQ0_spl
| ~ subset(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))
| ~ subset(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f48,f136]) ).
fof(f163,definition,
( sQ2_spl
<=> subset(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f165,plain,
( sQ2_spl
| ~ subset(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f163]) ).
fof(f166,definition,
( sQ3_spl
<=> subset(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f168,plain,
( sQ3_spl
| ~ subset(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)) ),
inference(component_clause,[status(thm)],[f166]) ).
fof(f169,plain,
( sQ0_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f161,f163,f166,f134]) ).
fof(f177,plain,
! [X0,X1] :
( ~ in(X0,ordered_pair(sK2_skl(X1,X0),sK3_skl(X1,X0)))
| in(sK2_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f63,f42]) ).
fof(f179,plain,
! [X0,X1] :
( ~ in(X0,ordered_pair(sK6_skl(X1,X0),sK5_skl(X1,X0)))
| in(sK5_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f71,f42]) ).
fof(f181,plain,
! [X0,X1] :
( ~ in(X1,ordered_pair(sK7_skl(X1,X0),sK8_skl(X1,X0)))
| in(ordered_pair(sK8_skl(X1,X0),sK7_skl(X1,X0)),X0)
| X1 = relation_inverse(X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f80,f42]) ).
fof(f189,plain,
( sQ1_spl
| ~ subset(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl))
| ~ subset(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f139,f48]) ).
fof(f191,definition,
( sQ4_spl
<=> subset(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f193,plain,
( sQ4_spl
| ~ subset(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,definition,
( sQ5_spl
<=> subset(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f195,plain,
( ~ sQ5_spl
| subset(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
inference(component_clause,[status(thm)],[f194]) ).
fof(f196,plain,
( sQ5_spl
| ~ subset(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
inference(component_clause,[status(thm)],[f194]) ).
fof(f197,plain,
( sQ1_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f189,f191,f194,f137]) ).
fof(f203,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,ordered_pair(X2,relation_rng(relation_rng(X0)))),X0)
| ~ relation(X0)
| ~ relation(relation_rng(X0)) ),
inference(resolution,[status(thm)],[f151,f146]) ).
fof(f204,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(ordered_pair(X1,relation_rng(relation_dom(X0))),X2),X0)
| ~ relation(X0)
| ~ relation(relation_dom(X0)) ),
inference(resolution,[status(thm)],[f151,f144]) ).
fof(f206,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,ordered_pair(relation_dom(relation_rng(X0)),X2)),X0)
| ~ relation(X0)
| ~ relation(relation_rng(X0)) ),
inference(resolution,[status(thm)],[f153,f146]) ).
fof(f207,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(ordered_pair(relation_dom(relation_dom(X0)),X1),X2),X0)
| ~ relation(X0)
| ~ relation(relation_dom(X0)) ),
inference(resolution,[status(thm)],[f153,f144]) ).
fof(f209,plain,
! [X0,X1] :
( ~ relation(relation_inverse(X0))
| ~ in(ordered_pair(X1,relation_dom(relation_inverse(X0))),X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f149,f153]) ).
fof(f210,plain,
! [X0,X1] :
( ~ relation(relation_inverse(X0))
| ~ in(ordered_pair(relation_rng(relation_inverse(X0)),X1),X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f149,f151]) ).
fof(f213,plain,
! [X0,X1] :
( ~ in(ordered_pair(X1,relation_dom(relation_inverse(X0))),X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f209,f82]) ).
fof(f214,plain,
! [X0,X1] :
( ~ in(ordered_pair(relation_rng(relation_inverse(X0)),X1),X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f210,f82]) ).
fof(f216,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ in(ordered_pair(relation_rng(X0),X1),relation_inverse(X0))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f150,f151]) ).
fof(f218,plain,
! [X0,X1,X2] :
( ~ in(X0,ordered_pair(X2,X1))
| ~ in(ordered_pair(X1,X2),relation_inverse(X0))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f150,f42]) ).
fof(f222,plain,
! [X0,X1] :
( ~ in(ordered_pair(relation_rng(X0),X1),relation_inverse(X0))
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f216]) ).
fof(f224,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(X0,X1),sK7_skl(X0,X1)),X1)
| X0 = relation_inverse(X1)
| ~ relation(X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ in(relation_rng(X0),sK8_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f152,f80]) ).
fof(f225,plain,
! [X0,X1] :
( in(sK5_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0)
| ~ relation(X0)
| ~ in(relation_rng(X0),sK5_skl(X1,X0)) ),
inference(resolution,[status(thm)],[f152,f71]) ).
fof(f226,plain,
! [X0,X1] :
( in(sK2_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0)
| ~ relation(X0)
| ~ in(relation_rng(X0),sK3_skl(X1,X0)) ),
inference(resolution,[status(thm)],[f152,f63]) ).
fof(f227,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),X0)
| ~ relation(X0)
| ~ relation(relation_inverse(X0))
| ~ in(relation_rng(relation_inverse(X0)),X1) ),
inference(resolution,[status(thm)],[f152,f149]) ).
fof(f228,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),relation_inverse(X0))
| ~ relation(X0)
| ~ relation(X0)
| ~ in(relation_rng(X0),X1) ),
inference(resolution,[status(thm)],[f152,f150]) ).
fof(f229,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(X2,ordered_pair(X3,X1)),X0)
| ~ relation(X0)
| ~ relation(relation_rng(X0))
| ~ in(relation_rng(relation_rng(X0)),X1) ),
inference(resolution,[status(thm)],[f152,f146]) ).
fof(f230,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(ordered_pair(X2,X1),X3),X0)
| ~ relation(X0)
| ~ relation(relation_dom(X0))
| ~ in(relation_rng(relation_dom(X0)),X1) ),
inference(resolution,[status(thm)],[f152,f144]) ).
fof(f233,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(X0,X1),sK7_skl(X0,X1)),X1)
| X0 = relation_inverse(X1)
| ~ relation(X1)
| ~ relation(X0)
| ~ in(relation_rng(X0),sK8_skl(X0,X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f224]) ).
fof(f234,plain,
! [X0,X1] :
( in(sK5_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0)
| ~ in(relation_rng(X0),sK5_skl(X1,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f225]) ).
fof(f235,plain,
! [X0,X1] :
( in(sK2_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0)
| ~ in(relation_rng(X0),sK3_skl(X1,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f226]) ).
fof(f236,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),X0)
| ~ relation(X0)
| ~ in(relation_rng(relation_inverse(X0)),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f227,f82]) ).
fof(f237,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),relation_inverse(X0))
| ~ relation(X0)
| ~ in(relation_rng(X0),X1) ),
inference(duplicate_literals_removal,[status(thm)],[f228]) ).
fof(f248,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(X0,X1),sK7_skl(X0,X1)),X1)
| X0 = relation_inverse(X1)
| ~ relation(X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ in(relation_dom(X0),sK7_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f154,f80]) ).
fof(f249,plain,
! [X0,X1] :
( in(sK5_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0)
| ~ relation(X0)
| ~ in(relation_dom(X0),sK6_skl(X1,X0)) ),
inference(resolution,[status(thm)],[f154,f71]) ).
fof(f250,plain,
! [X0,X1] :
( in(sK2_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0)
| ~ relation(X0)
| ~ in(relation_dom(X0),sK2_skl(X1,X0)) ),
inference(resolution,[status(thm)],[f154,f63]) ).
fof(f258,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(X0,X1),sK7_skl(X0,X1)),X1)
| X0 = relation_inverse(X1)
| ~ relation(X1)
| ~ relation(X0)
| ~ in(relation_dom(X0),sK7_skl(X0,X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f248]) ).
fof(f259,plain,
! [X0,X1] :
( in(sK5_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0)
| ~ in(relation_dom(X0),sK6_skl(X1,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f249]) ).
fof(f260,plain,
! [X0,X1] :
( in(sK2_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0)
| ~ in(relation_dom(X0),sK2_skl(X1,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f250]) ).
fof(f273,plain,
! [X0,X1] :
( ~ in(ordered_pair(relation_dom(relation_inverse(relation_inverse(X0))),X1),X0)
| ~ relation(X0)
| ~ relation(relation_inverse(X0)) ),
inference(resolution,[status(thm)],[f213,f149]) ).
fof(f278,plain,
! [X0,X1] :
( ~ in(ordered_pair(relation_dom(relation_inverse(relation_inverse(X0))),X1),X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f273,f82]) ).
fof(f280,plain,
! [X0,X1] :
( ~ in(ordered_pair(X1,relation_rng(relation_inverse(relation_inverse(X0)))),X0)
| ~ relation(X0)
| ~ relation(relation_inverse(X0)) ),
inference(resolution,[status(thm)],[f214,f149]) ).
fof(f281,plain,
! [X0,X1] :
( ~ in(ordered_pair(X1,relation_rng(relation_inverse(X0))),relation_inverse(X0))
| ~ relation(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f214,f150]) ).
fof(f285,plain,
! [X0,X1] :
( ~ in(ordered_pair(X1,relation_rng(relation_inverse(relation_inverse(X0)))),X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f280,f82]) ).
fof(f286,plain,
! [X0,X1] :
( ~ in(ordered_pair(X1,relation_rng(relation_inverse(X0))),relation_inverse(X0))
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f281]) ).
fof(f293,plain,
! [X0,X1] :
( ~ in(ordered_pair(X1,relation_rng(X0)),relation_inverse(relation_inverse(X0)))
| ~ relation(relation_inverse(X0))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f222,f150]) ).
fof(f296,plain,
! [X0,X1] :
( ~ in(ordered_pair(X1,relation_rng(X0)),relation_inverse(relation_inverse(X0)))
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f293,f82]) ).
fof(f332,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(relation_inverse(X0),X1),sK7_skl(relation_inverse(X0),X1)),X1)
| relation_inverse(X0) = relation_inverse(X1)
| ~ relation(relation_inverse(X0))
| ~ relation(X1)
| ~ in(X0,ordered_pair(sK8_skl(relation_inverse(X0),X1),sK7_skl(relation_inverse(X0),X1)))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f218,f80]) ).
fof(f341,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(relation_inverse(X0),X1),sK7_skl(relation_inverse(X0),X1)),X1)
| relation_inverse(X0) = relation_inverse(X1)
| ~ relation(X1)
| ~ in(X0,ordered_pair(sK8_skl(relation_inverse(X0),X1),sK7_skl(relation_inverse(X0),X1)))
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f332,f82]) ).
fof(f393,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(X0,X1),sK7_skl(X0,X1)),X1)
| X0 = relation_inverse(X1)
| ~ relation(X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ in(relation_rng(relation_inverse(X0)),sK7_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f236,f80]) ).
fof(f394,plain,
! [X0,X1] :
( in(sK5_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0)
| ~ relation(X0)
| ~ in(relation_rng(relation_inverse(X0)),sK6_skl(X1,X0)) ),
inference(resolution,[status(thm)],[f236,f71]) ).
fof(f395,plain,
! [X0,X1] :
( in(sK2_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0)
| ~ relation(X0)
| ~ in(relation_rng(relation_inverse(X0)),sK2_skl(X1,X0)) ),
inference(resolution,[status(thm)],[f236,f63]) ).
fof(f405,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(X0,X1),sK7_skl(X0,X1)),X1)
| X0 = relation_inverse(X1)
| ~ relation(X1)
| ~ relation(X0)
| ~ in(relation_rng(relation_inverse(X0)),sK7_skl(X0,X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f393]) ).
fof(f406,plain,
! [X0,X1] :
( in(sK5_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0)
| ~ in(relation_rng(relation_inverse(X0)),sK6_skl(X1,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f394]) ).
fof(f407,plain,
! [X0,X1] :
( in(sK2_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0)
| ~ in(relation_rng(relation_inverse(X0)),sK2_skl(X1,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f395]) ).
fof(f417,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(relation_inverse(X0),X1),sK7_skl(relation_inverse(X0),X1)),X1)
| relation_inverse(X0) = relation_inverse(X1)
| ~ relation(relation_inverse(X0))
| ~ relation(X1)
| ~ relation(X0)
| ~ in(relation_rng(X0),sK7_skl(relation_inverse(X0),X1)) ),
inference(resolution,[status(thm)],[f237,f80]) ).
fof(f427,plain,
! [X0,X1] :
( in(ordered_pair(sK8_skl(relation_inverse(X0),X1),sK7_skl(relation_inverse(X0),X1)),X1)
| relation_inverse(X0) = relation_inverse(X1)
| ~ relation(X1)
| ~ relation(X0)
| ~ in(relation_rng(X0),sK7_skl(relation_inverse(X0),X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f417,f82]) ).
fof(f498,plain,
( sQ5_spl
| ~ in(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f55,f196]) ).
fof(f499,plain,
( sQ2_spl
| ~ in(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),relation_dom(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f55,f165]) ).
fof(f508,plain,
! [X0] :
( ~ relation(X0)
| ~ in(relation_dom(X0),relation_dom(X0))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f143,f153]) ).
fof(f523,plain,
! [X0] :
( ~ in(relation_dom(X0),relation_dom(X0))
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f508]) ).
fof(f561,plain,
! [X0] :
( sQ5_spl
| ~ in(ordered_pair(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),X0),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f498,f144]) ).
fof(f563,plain,
( sQ5_spl
| empty(relation_dom(sK15_skl))
| ~ element(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f498,f111]) ).
fof(f564,definition,
( sQ10_spl
<=> relation(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f566,plain,
( sQ10_spl
| ~ relation(sK15_skl) ),
inference(component_clause,[status(thm)],[f564]) ).
fof(f567,definition,
! [X0] :
( sQ11_spl
<=> ~ in(ordered_pair(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),X0),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f568,plain,
! [X0] :
( ~ sQ11_spl
| ~ in(ordered_pair(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),X0),sK15_skl) ),
inference(component_clause,[status(thm)],[f567]) ).
fof(f570,plain,
( sQ5_spl
| sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f561,f564,f567,f194]) ).
fof(f571,definition,
( sQ12_spl
<=> element(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f574,definition,
( sQ13_spl
<=> empty(relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f577,plain,
( sQ5_spl
| sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f563,f571,f574,f194]) ).
fof(f578,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f566,f114]) ).
fof(f579,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f578]) ).
fof(f580,plain,
( sQ4_spl
| ~ in(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f193,f55]) ).
fof(f581,plain,
( ~ sQ11_spl
| ~ in(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),relation_dom(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f568,f143]) ).
fof(f582,plain,
! [X0] :
( ~ sQ11_spl
| ~ in(ordered_pair(X0,sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl)))),relation_inverse(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f568,f150]) ).
fof(f584,plain,
! [X0] :
( ~ sQ11_spl
| empty(sK15_skl)
| ~ element(ordered_pair(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),X0),sK15_skl) ),
inference(resolution,[status(thm)],[f568,f111]) ).
fof(f585,definition,
( sQ14_spl
<=> in(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f586,plain,
( ~ sQ14_spl
| in(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),relation_dom(sK15_skl)) ),
inference(component_clause,[status(thm)],[f585]) ).
fof(f587,plain,
( sQ14_spl
| ~ in(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),relation_dom(sK15_skl)) ),
inference(component_clause,[status(thm)],[f585]) ).
fof(f588,plain,
( ~ sQ11_spl
| ~ sQ14_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f581,f564,f585,f567]) ).
fof(f589,definition,
! [X0] :
( sQ15_spl
<=> ~ in(ordered_pair(X0,sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl)))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f590,plain,
! [X0] :
( ~ sQ15_spl
| ~ in(ordered_pair(X0,sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl)))),relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f589]) ).
fof(f592,plain,
( ~ sQ11_spl
| sQ15_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f582,f564,f589,f567]) ).
fof(f593,definition,
! [X0] :
( sQ16_spl
<=> ~ element(ordered_pair(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),X0),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f596,definition,
( sQ17_spl
<=> empty(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f599,plain,
( ~ sQ11_spl
| sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f584,f593,f596,f567]) ).
fof(f600,plain,
! [X0] :
( sQ14_spl
| ~ in(ordered_pair(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),X0),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f587,f144]) ).
fof(f602,plain,
( sQ14_spl
| empty(relation_dom(sK15_skl))
| ~ element(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f587,f111]) ).
fof(f603,plain,
( sQ14_spl
| sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f600,f564,f567,f585]) ).
fof(f604,plain,
( sQ14_spl
| sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f602,f571,f574,f585]) ).
fof(f605,plain,
! [X0] :
( sQ2_spl
| ~ in(ordered_pair(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),X0),relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f499,f144]) ).
fof(f606,plain,
! [X0] :
( sQ2_spl
| ~ in(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),X0)
| ~ subset(X0,relation_dom(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f499,f53]) ).
fof(f607,plain,
( sQ2_spl
| empty(relation_dom(relation_inverse(sK15_skl)))
| ~ element(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),relation_dom(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f499,f111]) ).
fof(f608,definition,
( sQ18_spl
<=> relation(relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f610,plain,
( sQ18_spl
| ~ relation(relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f608]) ).
fof(f611,definition,
! [X0] :
( sQ19_spl
<=> ~ in(ordered_pair(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),X0),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f612,plain,
! [X0] :
( ~ sQ19_spl
| ~ in(ordered_pair(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),X0),relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f611]) ).
fof(f614,plain,
( sQ2_spl
| sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f605,f608,f611,f163]) ).
fof(f615,definition,
( sQ20_spl
<=> element(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),relation_dom(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f618,definition,
( sQ21_spl
<=> empty(relation_dom(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f621,plain,
( sQ2_spl
| sQ21_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f607,f615,f618,f163]) ).
fof(f622,plain,
( sQ18_spl
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f610,f82]) ).
fof(f623,plain,
( sQ18_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f622,f564,f608]) ).
fof(f624,plain,
! [X0] :
( sQ4_spl
| ~ in(ordered_pair(X0,sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl))),relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f580,f146]) ).
fof(f626,plain,
( sQ4_spl
| empty(relation_rng(relation_inverse(sK15_skl)))
| ~ element(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f580,f111]) ).
fof(f627,definition,
! [X0] :
( sQ22_spl
<=> ~ in(ordered_pair(X0,sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f628,plain,
! [X0] :
( ~ sQ22_spl
| ~ in(ordered_pair(X0,sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl))),relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f627]) ).
fof(f630,plain,
( sQ4_spl
| sQ22_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f624,f608,f627,f191]) ).
fof(f631,definition,
( sQ23_spl
<=> element(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f634,definition,
( sQ24_spl
<=> empty(relation_rng(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f637,plain,
( sQ4_spl
| sQ24_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f626,f631,f634,f191]) ).
fof(f638,plain,
( sQ3_spl
| ~ in(sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))),relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f168,f55]) ).
fof(f640,plain,
! [X0] :
( sQ3_spl
| ~ in(ordered_pair(X0,sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl)))),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f638,f146]) ).
fof(f642,plain,
( sQ3_spl
| empty(relation_rng(sK15_skl))
| ~ element(sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))),relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f638,f111]) ).
fof(f643,definition,
! [X0] :
( sQ25_spl
<=> ~ in(ordered_pair(X0,sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl)))),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f644,plain,
! [X0] :
( ~ sQ25_spl
| ~ in(ordered_pair(X0,sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl)))),sK15_skl) ),
inference(component_clause,[status(thm)],[f643]) ).
fof(f646,plain,
( sQ3_spl
| sQ25_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f640,f564,f643,f166]) ).
fof(f647,definition,
( sQ26_spl
<=> element(sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f650,definition,
( sQ27_spl
<=> empty(relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f653,plain,
( sQ3_spl
| sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f642,f647,f650,f166]) ).
fof(f657,plain,
! [X0,X1] :
( sQ2_spl
| ~ in(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),X1)
| ~ subset(X1,X0)
| ~ subset(X0,relation_dom(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f606,f53]) ).
fof(f660,plain,
! [X0] :
( ~ sQ25_spl
| ~ in(ordered_pair(sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))),X0),relation_inverse(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f644,f150]) ).
fof(f662,plain,
! [X0] :
( ~ sQ25_spl
| empty(sK15_skl)
| ~ element(ordered_pair(X0,sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl)))),sK15_skl) ),
inference(resolution,[status(thm)],[f644,f111]) ).
fof(f663,definition,
! [X0] :
( sQ28_spl
<=> ~ in(ordered_pair(sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))),X0),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f666,plain,
( ~ sQ25_spl
| sQ28_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f660,f564,f663,f643]) ).
fof(f667,definition,
! [X0] :
( sQ29_spl
<=> ~ element(ordered_pair(X0,sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl)))),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f670,plain,
( ~ sQ25_spl
| sQ17_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f662,f667,f596,f643]) ).
fof(f671,plain,
! [X0] :
( ~ sQ15_spl
| ~ in(ordered_pair(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),X0),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f590,f149]) ).
fof(f672,plain,
! [X0] :
( ~ sQ15_spl
| ~ in(ordered_pair(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),X0),relation_inverse(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f590,f150]) ).
fof(f674,plain,
! [X0] :
( ~ sQ15_spl
| empty(relation_inverse(sK15_skl))
| ~ element(ordered_pair(X0,sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl)))),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f590,f111]) ).
fof(f675,plain,
( ~ sQ15_spl
| sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f671,f564,f567,f589]) ).
fof(f676,definition,
! [X0] :
( sQ30_spl
<=> ~ in(ordered_pair(sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl))),X0),relation_inverse(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f679,plain,
( ~ sQ15_spl
| sQ30_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f672,f608,f676,f589]) ).
fof(f680,definition,
! [X0] :
( sQ31_spl
<=> ~ element(ordered_pair(X0,sK0_skl(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl)))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f683,definition,
( sQ32_spl
<=> empty(relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f686,plain,
( ~ sQ15_spl
| sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f674,f680,f683,f589]) ).
fof(f693,plain,
( ~ sQ19_spl
| ~ in(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),relation_dom(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f612,f143]) ).
fof(f694,plain,
! [X0] :
( ~ sQ19_spl
| ~ in(ordered_pair(X0,sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f612,f149]) ).
fof(f695,plain,
! [X0] :
( ~ sQ19_spl
| ~ in(ordered_pair(X0,sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))),relation_inverse(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f612,f150]) ).
fof(f697,plain,
! [X0] :
( ~ sQ19_spl
| empty(relation_inverse(sK15_skl))
| ~ element(ordered_pair(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),X0),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f612,f111]) ).
fof(f698,definition,
( sQ33_spl
<=> in(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),relation_dom(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f701,plain,
( ~ sQ19_spl
| ~ sQ33_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f693,f608,f698,f611]) ).
fof(f702,definition,
! [X0] :
( sQ34_spl
<=> ~ in(ordered_pair(X0,sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f705,plain,
( ~ sQ19_spl
| sQ34_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f694,f564,f702,f611]) ).
fof(f706,definition,
! [X0] :
( sQ35_spl
<=> ~ in(ordered_pair(X0,sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))),relation_inverse(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f709,plain,
( ~ sQ19_spl
| sQ35_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f695,f608,f706,f611]) ).
fof(f710,definition,
! [X0] :
( sQ36_spl
<=> ~ element(ordered_pair(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),X0),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f713,plain,
( ~ sQ19_spl
| sQ32_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f697,f710,f683,f611]) ).
fof(f714,plain,
! [X0] :
( ~ sQ22_spl
| ~ in(ordered_pair(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),X0),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f628,f149]) ).
fof(f715,plain,
! [X0] :
( ~ sQ22_spl
| ~ in(ordered_pair(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),X0),relation_inverse(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f628,f150]) ).
fof(f717,plain,
! [X0] :
( ~ sQ22_spl
| empty(relation_inverse(sK15_skl))
| ~ element(ordered_pair(X0,sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl))),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f628,f111]) ).
fof(f718,definition,
! [X0] :
( sQ37_spl
<=> ~ in(ordered_pair(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),X0),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f721,plain,
( ~ sQ22_spl
| sQ37_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f714,f564,f718,f627]) ).
fof(f722,definition,
! [X0] :
( sQ38_spl
<=> ~ in(ordered_pair(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),X0),relation_inverse(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f725,plain,
( ~ sQ22_spl
| sQ38_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f715,f608,f722,f627]) ).
fof(f726,definition,
! [X0] :
( sQ39_spl
<=> ~ element(ordered_pair(X0,sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f729,plain,
( ~ sQ22_spl
| sQ32_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f717,f726,f683,f627]) ).
fof(f758,plain,
( ~ sQ5_spl
| sQ2_spl
| ~ in(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),relation_rng(relation_inverse(sK15_skl)))
| ~ subset(relation_dom(sK15_skl),relation_dom(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f657,f195]) ).
fof(f761,plain,
! [X0] :
( sQ2_spl
| subset(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl)))
| ~ subset(relation_rng(sK15_skl),X0)
| ~ subset(X0,relation_dom(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f657,f54]) ).
fof(f770,definition,
( sQ41_spl
<=> subset(relation_dom(sK15_skl),relation_dom(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f773,definition,
( sQ42_spl
<=> in(sK0_skl(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f776,plain,
( ~ sQ5_spl
| sQ2_spl
| ~ sQ42_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f758,f770,f773,f163,f194]) ).
fof(f777,definition,
! [X0] :
( sQ43_spl
<=> ( ~ subset(relation_rng(sK15_skl),X0)
| ~ subset(X0,relation_dom(relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f780,plain,
( sQ2_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f761,f777,f163]) ).
fof(f818,plain,
! [X0] :
( sQ0_spl
| ~ in(ordered_pair(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),X0),relation_inverse(sK15_skl))
| ~ in(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),relation_rng(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f62,f136]) ).
fof(f819,definition,
( sQ45_spl
<=> in(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f821,plain,
( sQ45_spl
| ~ in(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),relation_rng(sK15_skl)) ),
inference(component_clause,[status(thm)],[f819]) ).
fof(f822,definition,
! [X0] :
( sQ46_spl
<=> ~ in(ordered_pair(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),X0),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f823,plain,
! [X0] :
( ~ sQ46_spl
| ~ in(ordered_pair(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),X0),relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f822]) ).
fof(f825,plain,
( sQ0_spl
| sQ46_spl
| ~ sQ45_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f818,f608,f819,f822,f134]) ).
fof(f826,plain,
( ~ sQ22_spl
| ~ in(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f145,f628]) ).
fof(f827,plain,
( ~ sQ25_spl
| ~ in(sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))),relation_rng(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f145,f644]) ).
fof(f845,definition,
( sQ47_spl
<=> in(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f846,plain,
( ~ sQ47_spl
| in(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f845]) ).
fof(f847,plain,
( sQ47_spl
| ~ in(sK0_skl(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f845]) ).
fof(f848,plain,
( ~ sQ22_spl
| ~ sQ47_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f826,f608,f845,f627]) ).
fof(f849,definition,
( sQ48_spl
<=> in(sK0_skl(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f852,plain,
( ~ sQ25_spl
| ~ sQ48_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f827,f564,f849,f643]) ).
fof(f866,plain,
! [X0] :
( sQ0_spl
| ~ in(ordered_pair(X0,sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl)),sK15_skl)
| ~ in(sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl),relation_dom(relation_inverse(sK15_skl)))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f70,f136]) ).
fof(f867,definition,
( sQ49_spl
<=> in(sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl),relation_dom(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f869,plain,
( sQ49_spl
| ~ in(sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl),relation_dom(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f867]) ).
fof(f870,definition,
! [X0] :
( sQ50_spl
<=> ~ in(ordered_pair(X0,sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl)),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f873,plain,
( sQ0_spl
| sQ50_spl
| ~ sQ49_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f866,f564,f867,f870,f134]) ).
fof(f878,plain,
( sQ49_spl
| ~ sQ0_spl
| ~ in(sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl),relation_rng(sK15_skl)) ),
inference(backward_demodulation,[status(thm)],[f135,f869]) ).
fof(f890,plain,
( sQ49_spl
| ~ sQ0_spl
| ~ in(sK5_skl(relation_rng(sK15_skl),sK15_skl),relation_rng(sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f135,f878]) ).
fof(f894,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ in(ordered_pair(sK2_skl(X0,relation_inverse(sK15_skl)),X1),relation_inverse(sK15_skl))
| ~ in(sK2_skl(X0,relation_inverse(sK15_skl)),X0)
| X0 = relation_rng(sK15_skl)
| ~ relation(relation_inverse(sK15_skl)) ),
inference(paramodulation,[status(thm)],[f135,f62]) ).
fof(f895,plain,
( ~ sQ0_spl
| ~ in(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(paramodulation,[status(thm)],[f135,f523]) ).
fof(f897,plain,
! [X0] :
( ~ sQ0_spl
| in(ordered_pair(X0,sK1_skl(X0,relation_rng(sK15_skl),relation_inverse(sK15_skl))),relation_inverse(sK15_skl))
| ~ in(X0,relation_dom(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(paramodulation,[status(thm)],[f135,f143]) ).
fof(f903,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ in(ordered_pair(X0,X1),relation_inverse(sK15_skl))
| in(X0,relation_rng(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(paramodulation,[status(thm)],[f135,f144]) ).
fof(f904,definition,
! [X0] :
( sQ51_spl
<=> ~ in(ordered_pair(relation_rng(sK15_skl),X0),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f905,plain,
! [X0] :
( ~ sQ51_spl
| ~ in(ordered_pair(relation_rng(sK15_skl),X0),relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f904]) ).
fof(f908,definition,
! [X0] :
( sQ52_spl
<=> ~ in(ordered_pair(X0,relation_rng(sK15_skl)),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f909,plain,
! [X0] :
( ~ sQ52_spl
| ~ in(ordered_pair(X0,relation_rng(sK15_skl)),sK15_skl) ),
inference(component_clause,[status(thm)],[f908]) ).
fof(f912,definition,
! [X0,X1] :
( sQ53_spl
<=> ( ~ in(ordered_pair(sK2_skl(X0,relation_inverse(sK15_skl)),X1),relation_inverse(sK15_skl))
| ~ in(sK2_skl(X0,relation_inverse(sK15_skl)),X0)
| X0 = relation_rng(sK15_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f915,plain,
( ~ sQ0_spl
| sQ53_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f894,f608,f912,f134]) ).
fof(f916,definition,
( sQ54_spl
<=> in(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f919,plain,
( ~ sQ0_spl
| ~ sQ54_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f895,f608,f916,f134]) ).
fof(f920,definition,
( sQ55_spl
<=> in(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f924,definition,
! [X0] :
( sQ56_spl
<=> ( in(ordered_pair(X0,sK1_skl(X0,relation_rng(sK15_skl),relation_inverse(sK15_skl))),relation_inverse(sK15_skl))
| ~ in(X0,relation_dom(relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f925,plain,
! [X0] :
( ~ sQ56_spl
| in(ordered_pair(X0,sK1_skl(X0,relation_rng(sK15_skl),relation_inverse(sK15_skl))),relation_inverse(sK15_skl))
| ~ in(X0,relation_dom(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f924]) ).
fof(f927,plain,
( ~ sQ0_spl
| sQ56_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f897,f608,f924,f134]) ).
fof(f939,definition,
! [X0] :
( sQ60_spl
<=> ~ in(ordered_pair(relation_rng(sK15_skl),X0),relation_inverse(relation_inverse(relation_inverse(sK15_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f943,definition,
! [X0] :
( sQ61_spl
<=> ~ in(ordered_pair(X0,relation_rng(sK15_skl)),relation_inverse(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f944,plain,
! [X0] :
( ~ sQ61_spl
| ~ in(ordered_pair(X0,relation_rng(sK15_skl)),relation_inverse(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f943]) ).
fof(f948,definition,
! [X0,X1] :
( sQ62_spl
<=> ( ~ in(ordered_pair(X0,X1),relation_inverse(sK15_skl))
| in(X0,relation_rng(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f949,plain,
! [X0,X1] :
( ~ sQ62_spl
| ~ in(ordered_pair(X0,X1),relation_inverse(sK15_skl))
| in(X0,relation_rng(sK15_skl)) ),
inference(component_clause,[status(thm)],[f948]) ).
fof(f951,plain,
( ~ sQ0_spl
| sQ62_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f903,f608,f948,f134]) ).
fof(f955,plain,
! [X0] :
( ~ sQ56_spl
| ~ sQ0_spl
| in(ordered_pair(X0,sK1_skl(X0,relation_rng(sK15_skl),relation_inverse(sK15_skl))),relation_inverse(sK15_skl))
| ~ in(X0,relation_rng(sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f135,f925]) ).
fof(f956,plain,
! [X0] :
( sQ1_spl
| ~ in(ordered_pair(X0,sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl))),relation_inverse(sK15_skl))
| ~ in(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_dom(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f139,f70]) ).
fof(f958,plain,
! [X0] :
( sQ1_spl
| ~ in(ordered_pair(sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl),X0),sK15_skl)
| ~ in(sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl),relation_rng(relation_inverse(sK15_skl)))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f139,f62]) ).
fof(f960,definition,
( sQ63_spl
<=> in(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f962,plain,
( sQ63_spl
| ~ in(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
inference(component_clause,[status(thm)],[f960]) ).
fof(f963,definition,
! [X0] :
( sQ64_spl
<=> ~ in(ordered_pair(X0,sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f964,plain,
! [X0] :
( ~ sQ64_spl
| ~ in(ordered_pair(X0,sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl))),relation_inverse(sK15_skl)) ),
inference(component_clause,[status(thm)],[f963]) ).
fof(f966,plain,
( sQ1_spl
| sQ64_spl
| ~ sQ63_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f956,f608,f960,f963,f137]) ).
fof(f968,definition,
( sQ65_spl
<=> in(sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl),relation_rng(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f970,plain,
( sQ65_spl
| ~ in(sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl),relation_rng(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f968]) ).
fof(f971,definition,
! [X0] :
( sQ66_spl
<=> ~ in(ordered_pair(sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl),X0),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f972,plain,
! [X0] :
( ~ sQ66_spl
| ~ in(ordered_pair(sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl),X0),sK15_skl) ),
inference(component_clause,[status(thm)],[f971]) ).
fof(f974,plain,
( sQ1_spl
| sQ66_spl
| ~ sQ65_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f958,f564,f968,f971,f137]) ).
fof(f980,plain,
! [X0] :
( sQ49_spl
| ~ sQ0_spl
| ~ in(ordered_pair(X0,sK5_skl(relation_rng(sK15_skl),sK15_skl)),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f890,f146]) ).
fof(f1002,definition,
! [X0] :
( sQ72_spl
<=> ~ in(ordered_pair(X0,sK5_skl(relation_rng(sK15_skl),sK15_skl)),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1005,plain,
( sQ49_spl
| ~ sQ0_spl
| sQ72_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f980,f564,f1002,f134,f867]) ).
fof(f1015,plain,
( ~ sQ56_spl
| ~ sQ0_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(relation_inverse(relation_inverse(sK15_skl))),relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f955,f214]) ).
fof(f1017,plain,
( ~ sQ56_spl
| ~ sQ0_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_dom(relation_inverse(relation_inverse(relation_inverse(sK15_skl)))),relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f955,f278]) ).
fof(f1020,plain,
! [X0] :
( ~ sQ56_spl
| ~ sQ0_spl
| ~ relation(sK15_skl)
| ~ in(relation_rng(sK15_skl),X0)
| ~ in(X0,relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f955,f237]) ).
fof(f1021,plain,
! [X0] :
( ~ sQ56_spl
| ~ sQ0_spl
| ~ in(sK15_skl,ordered_pair(sK1_skl(X0,relation_rng(sK15_skl),relation_inverse(sK15_skl)),X0))
| ~ relation(sK15_skl)
| ~ in(X0,relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f955,f218]) ).
fof(f1022,plain,
! [X0] :
( ~ sQ56_spl
| ~ sQ0_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(relation_inverse(relation_inverse(sK15_skl))),X0)
| ~ in(X0,relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f955,f236]) ).
fof(f1023,plain,
! [X0] :
( ~ sQ56_spl
| ~ sQ0_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_dom(relation_inverse(sK15_skl)),X0)
| ~ in(X0,relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f955,f154]) ).
fof(f1024,plain,
! [X0] :
( ~ sQ56_spl
| ~ sQ0_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(relation_inverse(sK15_skl)),sK1_skl(X0,relation_rng(sK15_skl),relation_inverse(sK15_skl)))
| ~ in(X0,relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f955,f152]) ).
fof(f1039,definition,
( sQ77_spl
<=> in(relation_rng(relation_inverse(relation_inverse(sK15_skl))),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1041,plain,
( sQ77_spl
| ~ in(relation_rng(relation_inverse(relation_inverse(sK15_skl))),relation_rng(sK15_skl)) ),
inference(component_clause,[status(thm)],[f1039]) ).
fof(f1042,plain,
( ~ sQ56_spl
| ~ sQ0_spl
| ~ sQ18_spl
| ~ sQ77_spl ),
inference(split_clause,[status(thm)],[f1015,f1039,f608,f134,f924]) ).
fof(f1043,definition,
( sQ78_spl
<=> in(relation_rng(sK15_skl),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1044,plain,
( ~ sQ78_spl
| in(relation_rng(sK15_skl),relation_rng(sK15_skl)) ),
inference(component_clause,[status(thm)],[f1043]) ).
fof(f1045,plain,
( sQ78_spl
| ~ in(relation_rng(sK15_skl),relation_rng(sK15_skl)) ),
inference(component_clause,[status(thm)],[f1043]) ).
fof(f1047,definition,
( sQ79_spl
<=> in(relation_dom(relation_inverse(relation_inverse(relation_inverse(sK15_skl)))),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1050,plain,
( ~ sQ56_spl
| ~ sQ0_spl
| ~ sQ18_spl
| ~ sQ79_spl ),
inference(split_clause,[status(thm)],[f1017,f1047,f608,f134,f924]) ).
fof(f1053,definition,
! [X0] :
( sQ80_spl
<=> ( ~ in(relation_rng(sK15_skl),X0)
| ~ in(X0,relation_rng(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1056,plain,
( ~ sQ56_spl
| ~ sQ0_spl
| ~ sQ10_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f1020,f1053,f564,f134,f924]) ).
fof(f1057,definition,
! [X0] :
( sQ81_spl
<=> ( ~ in(sK15_skl,ordered_pair(sK1_skl(X0,relation_rng(sK15_skl),relation_inverse(sK15_skl)),X0))
| ~ in(X0,relation_rng(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1060,plain,
( ~ sQ56_spl
| ~ sQ0_spl
| ~ sQ10_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f1021,f1057,f564,f134,f924]) ).
fof(f1061,definition,
! [X0] :
( sQ82_spl
<=> ( ~ in(relation_rng(relation_inverse(relation_inverse(sK15_skl))),X0)
| ~ in(X0,relation_rng(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1064,plain,
( ~ sQ56_spl
| ~ sQ0_spl
| ~ sQ18_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f1022,f1061,f608,f134,f924]) ).
fof(f1065,definition,
! [X0] :
( sQ83_spl
<=> ( ~ in(relation_dom(relation_inverse(sK15_skl)),X0)
| ~ in(X0,relation_rng(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1068,plain,
( ~ sQ56_spl
| ~ sQ0_spl
| ~ sQ18_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f1023,f1065,f608,f134,f924]) ).
fof(f1069,definition,
! [X0] :
( sQ84_spl
<=> ( ~ in(relation_rng(relation_inverse(sK15_skl)),sK1_skl(X0,relation_rng(sK15_skl),relation_inverse(sK15_skl)))
| ~ in(X0,relation_rng(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1072,plain,
( ~ sQ56_spl
| ~ sQ0_spl
| ~ sQ18_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1024,f1069,f608,f134,f924]) ).
fof(f1092,plain,
! [X0,X1] :
( ~ sQ62_spl
| ~ in(relation_rng(sK15_skl),X0)
| ~ in(ordered_pair(X0,X1),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f949,f42]) ).
fof(f1170,definition,
( sQ103_spl
<=> element(relation_rng(sK15_skl),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1175,plain,
! [X0] :
( ~ sQ52_spl
| ~ in(ordered_pair(relation_rng(sK15_skl),X0),relation_inverse(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f909,f150]) ).
fof(f1177,plain,
! [X0] :
( ~ sQ52_spl
| empty(sK15_skl)
| ~ element(ordered_pair(X0,relation_rng(sK15_skl)),sK15_skl) ),
inference(resolution,[status(thm)],[f909,f111]) ).
fof(f1179,plain,
( ~ sQ52_spl
| sQ51_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1175,f564,f904,f908]) ).
fof(f1180,definition,
! [X0] :
( sQ104_spl
<=> ~ element(ordered_pair(X0,relation_rng(sK15_skl)),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1183,plain,
( ~ sQ52_spl
| sQ17_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f1177,f1180,f596,f908]) ).
fof(f1185,plain,
( ~ sQ51_spl
| ~ in(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f905,f143]) ).
fof(f1187,plain,
! [X0] :
( ~ sQ51_spl
| ~ in(ordered_pair(X0,relation_rng(sK15_skl)),relation_inverse(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f905,f150]) ).
fof(f1189,plain,
! [X0] :
( ~ sQ51_spl
| empty(relation_inverse(sK15_skl))
| ~ element(ordered_pair(relation_rng(sK15_skl),X0),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f905,f111]) ).
fof(f1190,plain,
( ~ sQ51_spl
| ~ sQ55_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1185,f608,f920,f904]) ).
fof(f1192,plain,
( ~ sQ51_spl
| sQ61_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1187,f608,f943,f904]) ).
fof(f1193,definition,
! [X0] :
( sQ105_spl
<=> ~ element(ordered_pair(relation_rng(sK15_skl),X0),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1196,plain,
( ~ sQ51_spl
| sQ32_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f1189,f1193,f683,f904]) ).
fof(f1200,plain,
! [X0] :
( sQ77_spl
| ~ in(ordered_pair(X0,relation_rng(relation_inverse(relation_inverse(sK15_skl)))),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f1041,f146]) ).
fof(f1202,plain,
( sQ77_spl
| empty(relation_rng(sK15_skl))
| ~ element(relation_rng(relation_inverse(relation_inverse(sK15_skl))),relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f1041,f111]) ).
fof(f1203,definition,
! [X0] :
( sQ106_spl
<=> ~ in(ordered_pair(X0,relation_rng(relation_inverse(relation_inverse(sK15_skl)))),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1206,plain,
( sQ77_spl
| sQ106_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1200,f564,f1203,f1039]) ).
fof(f1207,definition,
( sQ107_spl
<=> element(relation_rng(relation_inverse(relation_inverse(sK15_skl))),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1210,plain,
( sQ77_spl
| sQ27_spl
| ~ sQ107_spl ),
inference(split_clause,[status(thm)],[f1202,f1207,f650,f1039]) ).
fof(f1217,plain,
! [X0] :
( sQ63_spl
| ~ in(ordered_pair(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f962,f144]) ).
fof(f1219,plain,
( sQ63_spl
| empty(relation_dom(sK15_skl))
| ~ element(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f962,f111]) ).
fof(f1244,definition,
! [X0] :
( sQ114_spl
<=> ~ in(ordered_pair(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1245,plain,
! [X0] :
( ~ sQ114_spl
| ~ in(ordered_pair(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),sK15_skl) ),
inference(component_clause,[status(thm)],[f1244]) ).
fof(f1247,plain,
( sQ63_spl
| sQ114_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1217,f564,f1244,f960]) ).
fof(f1248,definition,
( sQ115_spl
<=> element(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1251,plain,
( sQ63_spl
| sQ13_spl
| ~ sQ115_spl ),
inference(split_clause,[status(thm)],[f1219,f1248,f574,f960]) ).
fof(f1253,plain,
( sQ65_spl
| relation_rng(relation_inverse(sK15_skl)) = relation_dom(sK15_skl)
| ~ relation(sK15_skl)
| ~ in(relation_rng(relation_inverse(sK15_skl)),sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl)) ),
inference(resolution,[status(thm)],[f970,f407]) ).
fof(f1254,plain,
( sQ65_spl
| relation_rng(relation_inverse(sK15_skl)) = relation_dom(sK15_skl)
| ~ relation(sK15_skl)
| ~ in(relation_dom(sK15_skl),sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl)) ),
inference(resolution,[status(thm)],[f970,f260]) ).
fof(f1255,plain,
( sQ65_spl
| relation_rng(relation_inverse(sK15_skl)) = relation_dom(sK15_skl)
| ~ relation(sK15_skl)
| ~ in(relation_rng(sK15_skl),sK3_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl)) ),
inference(resolution,[status(thm)],[f970,f235]) ).
fof(f1256,plain,
( sQ65_spl
| ~ in(sK15_skl,ordered_pair(sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl),sK3_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl)))
| relation_rng(relation_inverse(sK15_skl)) = relation_dom(sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f970,f177]) ).
fof(f1257,plain,
! [X0] :
( sQ65_spl
| ~ in(ordered_pair(X0,sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl)),relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f970,f146]) ).
fof(f1259,plain,
( sQ65_spl
| empty(relation_rng(relation_inverse(sK15_skl)))
| ~ element(sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl),relation_rng(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f970,f111]) ).
fof(f1260,definition,
( sQ116_spl
<=> in(relation_rng(relation_inverse(sK15_skl)),sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1263,plain,
( sQ65_spl
| sQ1_spl
| ~ sQ10_spl
| ~ sQ116_spl ),
inference(split_clause,[status(thm)],[f1253,f1260,f564,f137,f968]) ).
fof(f1264,definition,
( sQ117_spl
<=> in(relation_dom(sK15_skl),sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1267,plain,
( sQ65_spl
| sQ1_spl
| ~ sQ10_spl
| ~ sQ117_spl ),
inference(split_clause,[status(thm)],[f1254,f1264,f564,f137,f968]) ).
fof(f1268,definition,
( sQ118_spl
<=> in(relation_rng(sK15_skl),sK3_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1271,plain,
( sQ65_spl
| sQ1_spl
| ~ sQ10_spl
| ~ sQ118_spl ),
inference(split_clause,[status(thm)],[f1255,f1268,f564,f137,f968]) ).
fof(f1272,definition,
( sQ119_spl
<=> in(sK15_skl,ordered_pair(sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl),sK3_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1275,plain,
( sQ65_spl
| ~ sQ119_spl
| sQ1_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1256,f564,f137,f1272,f968]) ).
fof(f1276,definition,
! [X0] :
( sQ120_spl
<=> ~ in(ordered_pair(X0,sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl)),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1279,plain,
( sQ65_spl
| sQ120_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1257,f608,f1276,f968]) ).
fof(f1280,definition,
( sQ121_spl
<=> element(sK2_skl(relation_rng(relation_inverse(sK15_skl)),sK15_skl),relation_rng(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1283,plain,
( sQ65_spl
| sQ24_spl
| ~ sQ121_spl ),
inference(split_clause,[status(thm)],[f1259,f1280,f634,f968]) ).
fof(f1292,plain,
! [X0] :
( ~ sQ62_spl
| ~ in(X0,relation_rng(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(sK15_skl),sK4_skl(X0,relation_rng(relation_inverse(sK15_skl)),relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f1092,f145]) ).
fof(f1293,plain,
! [X0] :
( ~ sQ62_spl
| relation_inverse(X0) = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ in(relation_rng(X0),sK7_skl(relation_inverse(X0),relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),sK8_skl(relation_inverse(X0),relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f1092,f427]) ).
fof(f1294,plain,
! [X0] :
( ~ sQ62_spl
| relation_inverse(X0) = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl))
| ~ in(X0,ordered_pair(sK8_skl(relation_inverse(X0),relation_inverse(sK15_skl)),sK7_skl(relation_inverse(X0),relation_inverse(sK15_skl))))
| ~ relation(X0)
| ~ in(relation_rng(sK15_skl),sK8_skl(relation_inverse(X0),relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f1092,f341]) ).
fof(f1295,plain,
! [X0] :
( ~ sQ62_spl
| X0 = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ in(relation_rng(relation_inverse(X0)),sK7_skl(X0,relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),sK8_skl(X0,relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f1092,f405]) ).
fof(f1296,plain,
! [X0] :
( ~ sQ62_spl
| X0 = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ in(relation_dom(X0),sK7_skl(X0,relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),sK8_skl(X0,relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f1092,f258]) ).
fof(f1297,plain,
! [X0] :
( ~ sQ62_spl
| X0 = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ in(relation_rng(X0),sK8_skl(X0,relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),sK8_skl(X0,relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f1092,f233]) ).
fof(f1298,plain,
! [X0] :
( ~ sQ62_spl
| ~ in(X0,ordered_pair(sK7_skl(X0,relation_inverse(sK15_skl)),sK8_skl(X0,relation_inverse(sK15_skl))))
| X0 = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(sK15_skl),sK8_skl(X0,relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f1092,f181]) ).
fof(f1299,plain,
! [X0] :
( ~ sQ62_spl
| in(ordered_pair(sK8_skl(relation_inverse(sK15_skl),X0),sK7_skl(relation_inverse(sK15_skl),X0)),X0)
| relation_inverse(sK15_skl) = relation_inverse(X0)
| ~ relation(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ in(relation_rng(sK15_skl),sK7_skl(relation_inverse(sK15_skl),X0)) ),
inference(resolution,[status(thm)],[f1092,f80]) ).
fof(f1300,plain,
! [X0] :
( ~ sQ62_spl
| in(sK5_skl(X0,relation_inverse(sK15_skl)),X0)
| X0 = relation_rng(relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(sK15_skl),sK6_skl(X0,relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f1092,f71]) ).
fof(f1301,plain,
! [X0] :
( ~ sQ62_spl
| in(sK2_skl(X0,relation_inverse(sK15_skl)),X0)
| X0 = relation_dom(relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(sK15_skl),sK2_skl(X0,relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f1092,f63]) ).
fof(f1303,plain,
! [X0] :
( ~ sQ62_spl
| ~ in(X0,relation_dom(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(sK15_skl),X0) ),
inference(resolution,[status(thm)],[f1092,f143]) ).
fof(f1304,plain,
! [X0,X1] :
( ~ sQ62_spl
| ~ in(ordered_pair(X1,X0),sK15_skl)
| ~ relation(sK15_skl)
| ~ in(relation_rng(sK15_skl),X0) ),
inference(resolution,[status(thm)],[f1092,f149]) ).
fof(f1305,plain,
! [X0,X1] :
( ~ sQ62_spl
| ~ in(ordered_pair(X1,X0),relation_inverse(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(sK15_skl),X0) ),
inference(resolution,[status(thm)],[f1092,f150]) ).
fof(f1308,definition,
! [X0] :
( sQ122_spl
<=> ( ~ in(X0,relation_rng(relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),sK4_skl(X0,relation_rng(relation_inverse(sK15_skl)),relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1311,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f1292,f1308,f608,f948]) ).
fof(f1312,definition,
! [X0] :
( sQ123_spl
<=> ( relation_inverse(X0) = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ in(relation_rng(X0),sK7_skl(relation_inverse(X0),relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),sK8_skl(relation_inverse(X0),relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1315,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f1293,f1312,f608,f948]) ).
fof(f1316,definition,
! [X0] :
( sQ124_spl
<=> ( relation_inverse(X0) = relation_inverse(relation_inverse(sK15_skl))
| ~ in(X0,ordered_pair(sK8_skl(relation_inverse(X0),relation_inverse(sK15_skl)),sK7_skl(relation_inverse(X0),relation_inverse(sK15_skl))))
| ~ relation(X0)
| ~ in(relation_rng(sK15_skl),sK8_skl(relation_inverse(X0),relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1319,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ124_spl ),
inference(split_clause,[status(thm)],[f1294,f1316,f608,f948]) ).
fof(f1320,definition,
! [X0] :
( sQ125_spl
<=> ( X0 = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ in(relation_rng(relation_inverse(X0)),sK7_skl(X0,relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),sK8_skl(X0,relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1323,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f1295,f1320,f608,f948]) ).
fof(f1324,definition,
! [X0] :
( sQ126_spl
<=> ( X0 = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ in(relation_dom(X0),sK7_skl(X0,relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),sK8_skl(X0,relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1327,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f1296,f1324,f608,f948]) ).
fof(f1328,definition,
! [X0] :
( sQ127_spl
<=> ( X0 = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ in(relation_rng(X0),sK8_skl(X0,relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),sK8_skl(X0,relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1331,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f1297,f1328,f608,f948]) ).
fof(f1332,definition,
! [X0] :
( sQ128_spl
<=> ( ~ in(X0,ordered_pair(sK7_skl(X0,relation_inverse(sK15_skl)),sK8_skl(X0,relation_inverse(sK15_skl))))
| X0 = relation_inverse(relation_inverse(sK15_skl))
| ~ relation(X0)
| ~ in(relation_rng(sK15_skl),sK8_skl(X0,relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1335,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f1298,f1332,f608,f948]) ).
fof(f1336,definition,
! [X0] :
( sQ129_spl
<=> ( in(ordered_pair(sK8_skl(relation_inverse(sK15_skl),X0),sK7_skl(relation_inverse(sK15_skl),X0)),X0)
| relation_inverse(sK15_skl) = relation_inverse(X0)
| ~ relation(X0)
| ~ in(relation_rng(sK15_skl),sK7_skl(relation_inverse(sK15_skl),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1339,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ129_spl ),
inference(split_clause,[status(thm)],[f1299,f1336,f608,f948]) ).
fof(f1340,definition,
! [X0] :
( sQ130_spl
<=> ( in(sK5_skl(X0,relation_inverse(sK15_skl)),X0)
| X0 = relation_rng(relation_inverse(sK15_skl))
| ~ in(relation_rng(sK15_skl),sK6_skl(X0,relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f1343,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f1300,f1340,f608,f948]) ).
fof(f1344,definition,
! [X0] :
( sQ131_spl
<=> ( in(sK2_skl(X0,relation_inverse(sK15_skl)),X0)
| X0 = relation_dom(relation_inverse(sK15_skl))
| ~ in(relation_rng(sK15_skl),sK2_skl(X0,relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1347,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ131_spl ),
inference(split_clause,[status(thm)],[f1301,f1344,f608,f948]) ).
fof(f1348,definition,
! [X0] :
( sQ132_spl
<=> ( ~ in(X0,relation_dom(relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1351,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f1303,f1348,f608,f948]) ).
fof(f1352,definition,
! [X0,X1] :
( sQ133_spl
<=> ( ~ in(ordered_pair(X1,X0),sK15_skl)
| ~ in(relation_rng(sK15_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1355,plain,
( ~ sQ62_spl
| ~ sQ10_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f1304,f1352,f564,f948]) ).
fof(f1356,definition,
! [X0,X1] :
( sQ134_spl
<=> ( ~ in(ordered_pair(X1,X0),relation_inverse(relation_inverse(sK15_skl)))
| ~ in(relation_rng(sK15_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1359,plain,
( ~ sQ62_spl
| ~ sQ18_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f1305,f1356,f608,f948]) ).
fof(f1404,plain,
( ~ sQ61_spl
| ~ in(relation_rng(sK15_skl),relation_rng(relation_inverse(relation_inverse(sK15_skl))))
| ~ relation(relation_inverse(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f944,f145]) ).
fof(f1406,plain,
! [X0] :
( ~ sQ61_spl
| ~ in(ordered_pair(relation_rng(sK15_skl),X0),relation_inverse(relation_inverse(relation_inverse(sK15_skl))))
| ~ relation(relation_inverse(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f944,f150]) ).
fof(f1408,plain,
! [X0] :
( ~ sQ61_spl
| empty(relation_inverse(relation_inverse(sK15_skl)))
| ~ element(ordered_pair(X0,relation_rng(sK15_skl)),relation_inverse(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f944,f111]) ).
fof(f1409,definition,
( sQ141_spl
<=> relation(relation_inverse(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1411,plain,
( sQ141_spl
| ~ relation(relation_inverse(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f1409]) ).
fof(f1412,definition,
( sQ142_spl
<=> in(relation_rng(sK15_skl),relation_rng(relation_inverse(relation_inverse(sK15_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1415,plain,
( ~ sQ61_spl
| ~ sQ142_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f1404,f1409,f1412,f943]) ).
fof(f1417,plain,
( ~ sQ61_spl
| sQ60_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f1406,f1409,f939,f943]) ).
fof(f1418,definition,
! [X0] :
( sQ143_spl
<=> ~ element(ordered_pair(X0,relation_rng(sK15_skl)),relation_inverse(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1421,definition,
( sQ144_spl
<=> empty(relation_inverse(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1424,plain,
( ~ sQ61_spl
| sQ144_spl
| sQ143_spl ),
inference(split_clause,[status(thm)],[f1408,f1418,f1421,f943]) ).
fof(f1425,plain,
( sQ141_spl
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1411,f82]) ).
fof(f1426,plain,
( sQ141_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1425,f608,f1409]) ).
fof(f1428,plain,
( ~ sQ14_spl
| ~ sQ1_spl
| in(sK0_skl(relation_dom(sK15_skl),relation_dom(sK15_skl)),relation_dom(sK15_skl)) ),
inference(backward_demodulation,[status(thm)],[f138,f586]) ).
fof(f1437,plain,
( sQ47_spl
| ~ sQ1_spl
| ~ in(sK0_skl(relation_dom(sK15_skl),relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
inference(forward_demodulation,[status(thm)],[f138,f847]) ).
fof(f1438,plain,
( sQ47_spl
| ~ sQ1_spl
| ~ in(sK0_skl(relation_dom(sK15_skl),relation_dom(sK15_skl)),relation_dom(sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f138,f1437]) ).
fof(f1439,plain,
( ~ sQ14_spl
| ~ sQ1_spl
| sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1428,f1438]) ).
fof(f1440,plain,
( ~ sQ14_spl
| ~ sQ1_spl
| sQ47_spl ),
inference(contradiction_clause,[status(thm)],[f1439]) ).
fof(f1463,plain,
! [X0] :
( sQ45_spl
| ~ in(ordered_pair(X0,sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl))),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f821,f146]) ).
fof(f1490,definition,
! [X0] :
( sQ151_spl
<=> ~ in(ordered_pair(X0,sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl))),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1491,plain,
! [X0] :
( ~ sQ151_spl
| ~ in(ordered_pair(X0,sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl))),sK15_skl) ),
inference(component_clause,[status(thm)],[f1490]) ).
fof(f1493,plain,
( sQ45_spl
| sQ151_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1463,f564,f1490,f819]) ).
fof(f1498,plain,
( sQ49_spl
| relation_dom(relation_inverse(sK15_skl)) = relation_rng(sK15_skl)
| ~ relation(sK15_skl)
| ~ in(relation_rng(relation_inverse(sK15_skl)),sK6_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl)) ),
inference(resolution,[status(thm)],[f869,f406]) ).
fof(f1499,plain,
( sQ49_spl
| relation_dom(relation_inverse(sK15_skl)) = relation_rng(sK15_skl)
| ~ relation(sK15_skl)
| ~ in(relation_dom(sK15_skl),sK6_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl)) ),
inference(resolution,[status(thm)],[f869,f259]) ).
fof(f1500,plain,
( sQ49_spl
| relation_dom(relation_inverse(sK15_skl)) = relation_rng(sK15_skl)
| ~ relation(sK15_skl)
| ~ in(relation_rng(sK15_skl),sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl)) ),
inference(resolution,[status(thm)],[f869,f234]) ).
fof(f1501,plain,
( sQ49_spl
| ~ in(sK15_skl,ordered_pair(sK6_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl),sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl)))
| relation_dom(relation_inverse(sK15_skl)) = relation_rng(sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f869,f179]) ).
fof(f1502,plain,
! [X0] :
( sQ49_spl
| ~ in(ordered_pair(sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl),X0),relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f869,f144]) ).
fof(f1504,plain,
( sQ49_spl
| empty(relation_dom(relation_inverse(sK15_skl)))
| ~ element(sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl),relation_dom(relation_inverse(sK15_skl))) ),
inference(resolution,[status(thm)],[f869,f111]) ).
fof(f1505,definition,
( sQ153_spl
<=> in(relation_rng(relation_inverse(sK15_skl)),sK6_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1508,plain,
( sQ49_spl
| sQ0_spl
| ~ sQ10_spl
| ~ sQ153_spl ),
inference(split_clause,[status(thm)],[f1498,f1505,f564,f134,f867]) ).
fof(f1509,definition,
( sQ154_spl
<=> in(relation_dom(sK15_skl),sK6_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f1512,plain,
( sQ49_spl
| sQ0_spl
| ~ sQ10_spl
| ~ sQ154_spl ),
inference(split_clause,[status(thm)],[f1499,f1509,f564,f134,f867]) ).
fof(f1513,definition,
( sQ155_spl
<=> in(relation_rng(sK15_skl),sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1516,plain,
( sQ49_spl
| sQ0_spl
| ~ sQ10_spl
| ~ sQ155_spl ),
inference(split_clause,[status(thm)],[f1500,f1513,f564,f134,f867]) ).
fof(f1517,definition,
( sQ156_spl
<=> in(sK15_skl,ordered_pair(sK6_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl),sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f1520,plain,
( sQ49_spl
| ~ sQ156_spl
| sQ0_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1501,f564,f134,f1517,f867]) ).
fof(f1521,definition,
! [X0] :
( sQ157_spl
<=> ~ in(ordered_pair(sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl),X0),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f1524,plain,
( sQ49_spl
| sQ157_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1502,f608,f1521,f867]) ).
fof(f1525,definition,
( sQ158_spl
<=> element(sK5_skl(relation_dom(relation_inverse(sK15_skl)),sK15_skl),relation_dom(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f1528,plain,
( sQ49_spl
| sQ21_spl
| ~ sQ158_spl ),
inference(split_clause,[status(thm)],[f1504,f1525,f618,f867]) ).
fof(f1570,plain,
( ~ sQ114_spl
| ~ in(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_dom(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f1245,f143]) ).
fof(f1571,plain,
! [X0] :
( ~ sQ114_spl
| ~ in(ordered_pair(X0,sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl))),relation_inverse(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f1245,f150]) ).
fof(f1573,plain,
! [X0] :
( ~ sQ114_spl
| empty(sK15_skl)
| ~ element(ordered_pair(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),sK15_skl) ),
inference(resolution,[status(thm)],[f1245,f111]) ).
fof(f1574,plain,
( ~ sQ114_spl
| ~ sQ63_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1570,f564,f960,f1244]) ).
fof(f1575,plain,
( ~ sQ114_spl
| sQ64_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1571,f564,f963,f1244]) ).
fof(f1576,definition,
! [X0] :
( sQ161_spl
<=> ~ element(ordered_pair(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f1579,plain,
( ~ sQ114_spl
| sQ17_spl
| sQ161_spl ),
inference(split_clause,[status(thm)],[f1573,f1576,f596,f1244]) ).
fof(f1580,plain,
( ~ sQ64_spl
| ~ in(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_rng(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f964,f145]) ).
fof(f1581,plain,
( ~ sQ64_spl
| in(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_dom(sK15_skl))
| relation_dom(sK15_skl) = relation_rng(relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f964,f71]) ).
fof(f1582,plain,
! [X0] :
( ~ sQ64_spl
| ~ in(ordered_pair(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f964,f149]) ).
fof(f1583,plain,
! [X0] :
( ~ sQ64_spl
| ~ in(ordered_pair(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),relation_inverse(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f964,f150]) ).
fof(f1585,plain,
! [X0] :
( ~ sQ64_spl
| empty(relation_inverse(sK15_skl))
| ~ element(ordered_pair(X0,sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl))),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f964,f111]) ).
fof(f1586,definition,
( sQ162_spl
<=> in(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f1588,plain,
( sQ162_spl
| ~ in(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f1586]) ).
fof(f1589,plain,
( ~ sQ64_spl
| ~ sQ162_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1580,f608,f1586,f963]) ).
fof(f1590,plain,
( ~ sQ64_spl
| sQ63_spl
| sQ1_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1581,f608,f137,f960,f963]) ).
fof(f1591,plain,
( ~ sQ64_spl
| sQ114_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1582,f564,f1244,f963]) ).
fof(f1592,definition,
! [X0] :
( sQ163_spl
<=> ~ in(ordered_pair(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),relation_inverse(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f1595,plain,
( ~ sQ64_spl
| sQ163_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1583,f608,f1592,f963]) ).
fof(f1596,definition,
! [X0] :
( sQ164_spl
<=> ~ element(ordered_pair(X0,sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f1599,plain,
( ~ sQ64_spl
| sQ32_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f1585,f1596,f683,f963]) ).
fof(f1602,plain,
! [X0] :
( ~ sQ66_spl
| ~ sQ1_spl
| ~ in(ordered_pair(sK2_skl(relation_dom(sK15_skl),sK15_skl),X0),sK15_skl) ),
inference(backward_demodulation,[status(thm)],[f138,f972]) ).
fof(f1604,plain,
( sQ162_spl
| ~ sQ1_spl
| ~ in(sK5_skl(relation_dom(sK15_skl),relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
inference(backward_demodulation,[status(thm)],[f138,f1588]) ).
fof(f1625,plain,
( sQ14_spl
| ~ sQ1_spl
| ~ in(sK0_skl(relation_dom(sK15_skl),relation_dom(sK15_skl)),relation_dom(sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f138,f587]) ).
fof(f1631,plain,
( sQ162_spl
| ~ sQ1_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f1604,f960,f137,f1586]) ).
fof(f1635,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ in(ordered_pair(X0,X1),sK15_skl)
| ~ relation(sK15_skl)
| ~ in(relation_dom(sK15_skl),X0) ),
inference(paramodulation,[status(thm)],[f138,f236]) ).
fof(f1636,plain,
! [X0] :
( ~ sQ1_spl
| ~ in(ordered_pair(X0,relation_dom(sK15_skl)),relation_inverse(sK15_skl))
| ~ relation(sK15_skl) ),
inference(paramodulation,[status(thm)],[f138,f286]) ).
fof(f1637,plain,
! [X0] :
( ~ sQ1_spl
| ~ in(ordered_pair(relation_dom(sK15_skl),X0),sK15_skl)
| ~ relation(sK15_skl) ),
inference(paramodulation,[status(thm)],[f138,f214]) ).
fof(f1638,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ in(ordered_pair(X1,sK5_skl(X0,relation_inverse(sK15_skl))),relation_inverse(sK15_skl))
| ~ in(sK5_skl(X0,relation_inverse(sK15_skl)),X0)
| X0 = relation_dom(sK15_skl)
| ~ relation(relation_inverse(sK15_skl)) ),
inference(paramodulation,[status(thm)],[f138,f70]) ).
fof(f1639,plain,
! [X0] :
( ~ sQ1_spl
| in(ordered_pair(sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),relation_inverse(sK15_skl))
| ~ in(X0,relation_rng(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(paramodulation,[status(thm)],[f138,f145]) ).
fof(f1640,plain,
! [X0] :
( ~ sQ1_spl
| ~ in(ordered_pair(X0,relation_dom(sK15_skl)),relation_inverse(relation_inverse(relation_inverse(sK15_skl))))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(paramodulation,[status(thm)],[f138,f296]) ).
fof(f1641,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ in(ordered_pair(X0,ordered_pair(relation_dom(relation_dom(sK15_skl)),X1)),relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl))
| ~ relation(relation_rng(relation_inverse(sK15_skl))) ),
inference(paramodulation,[status(thm)],[f138,f206]) ).
fof(f1642,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ in(ordered_pair(X0,ordered_pair(X1,relation_rng(relation_dom(sK15_skl)))),relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl))
| ~ relation(relation_rng(relation_inverse(sK15_skl))) ),
inference(paramodulation,[status(thm)],[f138,f203]) ).
fof(f1643,plain,
! [X0] :
( ~ sQ1_spl
| ~ in(ordered_pair(relation_dom(sK15_skl),X0),relation_inverse(relation_inverse(sK15_skl)))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(paramodulation,[status(thm)],[f138,f222]) ).
fof(f1645,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ in(ordered_pair(X1,X0),relation_inverse(sK15_skl))
| in(X0,relation_dom(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(paramodulation,[status(thm)],[f138,f146]) ).
fof(f1646,definition,
! [X0,X1] :
( sQ165_spl
<=> ( ~ in(ordered_pair(X0,X1),sK15_skl)
| ~ in(relation_dom(sK15_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f1649,plain,
( ~ sQ1_spl
| ~ sQ10_spl
| sQ165_spl ),
inference(split_clause,[status(thm)],[f1635,f1646,f564,f137]) ).
fof(f1650,definition,
! [X0] :
( sQ166_spl
<=> ~ in(ordered_pair(X0,relation_dom(sK15_skl)),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f1653,plain,
( ~ sQ1_spl
| sQ166_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1636,f564,f1650,f137]) ).
fof(f1654,definition,
! [X0] :
( sQ167_spl
<=> ~ in(ordered_pair(relation_dom(sK15_skl),X0),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f1655,plain,
! [X0] :
( ~ sQ167_spl
| ~ in(ordered_pair(relation_dom(sK15_skl),X0),sK15_skl) ),
inference(component_clause,[status(thm)],[f1654]) ).
fof(f1657,plain,
( ~ sQ1_spl
| sQ167_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1637,f564,f1654,f137]) ).
fof(f1658,definition,
! [X0,X1] :
( sQ168_spl
<=> ( ~ in(ordered_pair(X1,sK5_skl(X0,relation_inverse(sK15_skl))),relation_inverse(sK15_skl))
| ~ in(sK5_skl(X0,relation_inverse(sK15_skl)),X0)
| X0 = relation_dom(sK15_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f1661,plain,
( ~ sQ1_spl
| sQ168_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1638,f608,f1658,f137]) ).
fof(f1662,definition,
! [X0] :
( sQ169_spl
<=> ( in(ordered_pair(sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),relation_inverse(sK15_skl))
| ~ in(X0,relation_rng(relation_inverse(sK15_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f1663,plain,
! [X0] :
( ~ sQ169_spl
| in(ordered_pair(sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),relation_inverse(sK15_skl))
| ~ in(X0,relation_rng(relation_inverse(sK15_skl))) ),
inference(component_clause,[status(thm)],[f1662]) ).
fof(f1665,plain,
( ~ sQ1_spl
| sQ169_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1639,f608,f1662,f137]) ).
fof(f1666,definition,
! [X0] :
( sQ170_spl
<=> ~ in(ordered_pair(X0,relation_dom(sK15_skl)),relation_inverse(relation_inverse(relation_inverse(sK15_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f1669,plain,
( ~ sQ1_spl
| sQ170_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1640,f608,f1666,f137]) ).
fof(f1670,definition,
( sQ171_spl
<=> relation(relation_rng(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f1673,definition,
! [X0,X1] :
( sQ172_spl
<=> ~ in(ordered_pair(X0,ordered_pair(relation_dom(relation_dom(sK15_skl)),X1)),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f1676,plain,
( ~ sQ1_spl
| sQ172_spl
| ~ sQ18_spl
| ~ sQ171_spl ),
inference(split_clause,[status(thm)],[f1641,f1670,f608,f1673,f137]) ).
fof(f1677,definition,
! [X0,X1] :
( sQ173_spl
<=> ~ in(ordered_pair(X0,ordered_pair(X1,relation_rng(relation_dom(sK15_skl)))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f1680,plain,
( ~ sQ1_spl
| sQ173_spl
| ~ sQ18_spl
| ~ sQ171_spl ),
inference(split_clause,[status(thm)],[f1642,f1670,f608,f1677,f137]) ).
fof(f1681,definition,
! [X0] :
( sQ174_spl
<=> ~ in(ordered_pair(relation_dom(sK15_skl),X0),relation_inverse(relation_inverse(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f1684,plain,
( ~ sQ1_spl
| sQ174_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1643,f608,f1681,f137]) ).
fof(f1686,definition,
! [X0,X1] :
( sQ175_spl
<=> ( ~ in(ordered_pair(X1,X0),relation_inverse(sK15_skl))
| in(X0,relation_dom(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f1687,plain,
! [X0,X1] :
( ~ sQ175_spl
| ~ in(ordered_pair(X1,X0),relation_inverse(sK15_skl))
| in(X0,relation_dom(sK15_skl)) ),
inference(component_clause,[status(thm)],[f1686]) ).
fof(f1689,plain,
( ~ sQ1_spl
| sQ175_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1645,f608,f1686,f137]) ).
fof(f1691,plain,
! [X0] :
( ~ sQ169_spl
| ~ sQ1_spl
| in(ordered_pair(sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl)),X0),relation_inverse(sK15_skl))
| ~ in(X0,relation_dom(sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f138,f1663]) ).
fof(f1694,plain,
( ~ sQ66_spl
| ~ sQ1_spl
| in(sK2_skl(relation_dom(sK15_skl),sK15_skl),relation_dom(sK15_skl))
| relation_dom(sK15_skl) = relation_dom(sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f1602,f63]) ).
fof(f1695,plain,
( ~ sQ66_spl
| ~ sQ1_spl
| ~ in(sK2_skl(relation_dom(sK15_skl),sK15_skl),relation_dom(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f1602,f143]) ).
fof(f1696,plain,
! [X0] :
( ~ sQ66_spl
| ~ sQ1_spl
| ~ in(ordered_pair(X0,sK2_skl(relation_dom(sK15_skl),sK15_skl)),relation_inverse(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f1602,f150]) ).
fof(f1698,plain,
! [X0] :
( ~ sQ66_spl
| ~ sQ1_spl
| empty(sK15_skl)
| ~ element(ordered_pair(sK2_skl(relation_dom(sK15_skl),sK15_skl),X0),sK15_skl) ),
inference(resolution,[status(thm)],[f1602,f111]) ).
fof(f1699,definition,
( sQ176_spl
<=> relation_dom(sK15_skl) = relation_dom(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f1702,definition,
( sQ177_spl
<=> in(sK2_skl(relation_dom(sK15_skl),sK15_skl),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f1705,plain,
( ~ sQ66_spl
| ~ sQ1_spl
| sQ177_spl
| sQ176_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1694,f564,f1699,f1702,f137,f971]) ).
fof(f1706,plain,
( ~ sQ66_spl
| ~ sQ1_spl
| ~ sQ177_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1695,f564,f1702,f137,f971]) ).
fof(f1707,definition,
! [X0] :
( sQ178_spl
<=> ~ in(ordered_pair(X0,sK2_skl(relation_dom(sK15_skl),sK15_skl)),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f1710,plain,
( ~ sQ66_spl
| ~ sQ1_spl
| sQ178_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1696,f564,f1707,f137,f971]) ).
fof(f1711,definition,
! [X0] :
( sQ179_spl
<=> ~ element(ordered_pair(sK2_skl(relation_dom(sK15_skl),sK15_skl),X0),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1714,plain,
( ~ sQ66_spl
| ~ sQ1_spl
| sQ17_spl
| sQ179_spl ),
inference(split_clause,[status(thm)],[f1698,f1711,f596,f137,f971]) ).
fof(f1767,plain,
! [X0] :
( ~ sQ169_spl
| ~ sQ1_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ relation(relation_rng(relation_inverse(sK15_skl)))
| ~ in(ordered_pair(relation_dom(relation_rng(relation_inverse(sK15_skl))),X0),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f206]) ).
fof(f1768,plain,
! [X0] :
( ~ sQ169_spl
| ~ sQ1_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ relation(relation_rng(relation_inverse(sK15_skl)))
| ~ in(ordered_pair(X0,relation_rng(relation_rng(relation_inverse(sK15_skl)))),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f203]) ).
fof(f1769,plain,
! [X0,X1] :
( ~ sQ169_spl
| ~ sQ1_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ relation(relation_rng(relation_inverse(sK15_skl)))
| ~ in(relation_rng(relation_rng(relation_inverse(sK15_skl))),X1)
| ~ in(ordered_pair(X0,X1),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f229]) ).
fof(f1770,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_dom(relation_inverse(relation_inverse(sK15_skl))),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f213]) ).
fof(f1772,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(relation_inverse(relation_inverse(relation_inverse(sK15_skl)))),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f285]) ).
fof(f1773,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ relation(sK15_skl)
| ~ in(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f286]) ).
fof(f1775,plain,
! [X0] :
( ~ sQ169_spl
| ~ sQ1_spl
| ~ relation(sK15_skl)
| ~ in(relation_rng(sK15_skl),sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl)))
| ~ in(X0,relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f237]) ).
fof(f1776,plain,
! [X0] :
( ~ sQ169_spl
| ~ sQ1_spl
| ~ in(sK15_skl,ordered_pair(X0,sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl))))
| ~ relation(sK15_skl)
| ~ in(X0,relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f218]) ).
fof(f1777,plain,
! [X0] :
( ~ sQ169_spl
| ~ sQ1_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(relation_inverse(relation_inverse(sK15_skl))),sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl)))
| ~ in(X0,relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f236]) ).
fof(f1778,plain,
! [X0] :
( ~ sQ169_spl
| ~ sQ1_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_dom(relation_inverse(sK15_skl)),sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl)))
| ~ in(X0,relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f154]) ).
fof(f1779,plain,
! [X0] :
( ~ sQ169_spl
| ~ sQ1_spl
| ~ relation(relation_inverse(sK15_skl))
| ~ in(relation_rng(relation_inverse(sK15_skl)),X0)
| ~ in(X0,relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1691,f152]) ).
fof(f1782,definition,
! [X0] :
( sQ180_spl
<=> ~ in(ordered_pair(relation_dom(relation_rng(relation_inverse(sK15_skl))),X0),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f1785,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ18_spl
| ~ sQ171_spl
| sQ180_spl ),
inference(split_clause,[status(thm)],[f1767,f1782,f1670,f608,f137,f1662]) ).
fof(f1786,definition,
! [X0] :
( sQ181_spl
<=> ~ in(ordered_pair(X0,relation_rng(relation_rng(relation_inverse(sK15_skl)))),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f1789,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ18_spl
| ~ sQ171_spl
| sQ181_spl ),
inference(split_clause,[status(thm)],[f1768,f1786,f1670,f608,f137,f1662]) ).
fof(f1790,definition,
! [X0,X1] :
( sQ182_spl
<=> ( ~ in(relation_rng(relation_rng(relation_inverse(sK15_skl))),X1)
| ~ in(ordered_pair(X0,X1),relation_dom(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f1793,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ18_spl
| ~ sQ171_spl
| sQ182_spl ),
inference(split_clause,[status(thm)],[f1769,f1790,f1670,f608,f137,f1662]) ).
fof(f1794,definition,
( sQ183_spl
<=> in(relation_dom(relation_inverse(relation_inverse(sK15_skl))),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f1797,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ18_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f1770,f1794,f608,f137,f1662]) ).
fof(f1798,definition,
( sQ184_spl
<=> in(relation_dom(sK15_skl),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f1802,definition,
( sQ185_spl
<=> in(relation_rng(relation_inverse(relation_inverse(relation_inverse(sK15_skl)))),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f1805,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ18_spl
| ~ sQ185_spl ),
inference(split_clause,[status(thm)],[f1772,f1802,f608,f137,f1662]) ).
fof(f1806,definition,
( sQ186_spl
<=> in(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f1808,plain,
( sQ186_spl
| ~ in(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl)) ),
inference(component_clause,[status(thm)],[f1806]) ).
fof(f1809,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ10_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f1773,f1806,f564,f137,f1662]) ).
fof(f1811,definition,
! [X0] :
( sQ187_spl
<=> ( ~ in(relation_rng(sK15_skl),sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl)))
| ~ in(X0,relation_dom(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f1814,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ187_spl ),
inference(split_clause,[status(thm)],[f1775,f1811,f564,f137,f1662]) ).
fof(f1815,definition,
! [X0] :
( sQ188_spl
<=> ( ~ in(sK15_skl,ordered_pair(X0,sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl))))
| ~ in(X0,relation_dom(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f1818,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ188_spl ),
inference(split_clause,[status(thm)],[f1776,f1815,f564,f137,f1662]) ).
fof(f1819,definition,
! [X0] :
( sQ189_spl
<=> ( ~ in(relation_rng(relation_inverse(relation_inverse(sK15_skl))),sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl)))
| ~ in(X0,relation_dom(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f1822,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ18_spl
| sQ189_spl ),
inference(split_clause,[status(thm)],[f1777,f1819,f608,f137,f1662]) ).
fof(f1823,definition,
! [X0] :
( sQ190_spl
<=> ( ~ in(relation_dom(relation_inverse(sK15_skl)),sK4_skl(X0,relation_dom(sK15_skl),relation_inverse(sK15_skl)))
| ~ in(X0,relation_dom(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f1826,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ18_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f1778,f1823,f608,f137,f1662]) ).
fof(f1827,definition,
! [X0] :
( sQ191_spl
<=> ( ~ in(relation_rng(relation_inverse(sK15_skl)),X0)
| ~ in(X0,relation_dom(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f1830,plain,
( ~ sQ169_spl
| ~ sQ1_spl
| ~ sQ18_spl
| sQ191_spl ),
inference(split_clause,[status(thm)],[f1779,f1827,f608,f137,f1662]) ).
fof(f1831,plain,
( sQ186_spl
| ~ sQ1_spl
| ~ in(relation_dom(sK15_skl),relation_dom(sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f138,f1808]) ).
fof(f1836,plain,
! [X0] :
( sQ78_spl
| ~ in(ordered_pair(X0,relation_rng(sK15_skl)),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f1045,f146]) ).
fof(f1838,plain,
( sQ78_spl
| empty(relation_rng(sK15_skl))
| ~ element(relation_rng(sK15_skl),relation_rng(sK15_skl)) ),
inference(resolution,[status(thm)],[f1045,f111]) ).
fof(f1839,plain,
( sQ78_spl
| sQ52_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1836,f564,f908,f1043]) ).
fof(f1840,plain,
( sQ78_spl
| sQ27_spl
| ~ sQ103_spl ),
inference(split_clause,[status(thm)],[f1838,f1170,f650,f1043]) ).
fof(f1843,plain,
( sQ186_spl
| ~ sQ1_spl
| empty(relation_dom(sK15_skl))
| ~ element(relation_dom(sK15_skl),relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f1831,f111]) ).
fof(f1845,definition,
( sQ192_spl
<=> element(relation_dom(sK15_skl),relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f1848,plain,
( sQ186_spl
| ~ sQ1_spl
| sQ13_spl
| ~ sQ192_spl ),
inference(split_clause,[status(thm)],[f1843,f1845,f574,f137,f1806]) ).
fof(f1849,plain,
( ~ sQ78_spl
| $false ),
inference(resolution,[status(thm)],[f1044,f42]) ).
fof(f1853,plain,
~ sQ78_spl,
inference(contradiction_clause,[status(thm)],[f1849]) ).
fof(f1860,plain,
( ~ sQ47_spl
| ~ sQ1_spl
| in(sK0_skl(relation_dom(sK15_skl),relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl))) ),
inference(forward_demodulation,[status(thm)],[f138,f846]) ).
fof(f1861,plain,
( ~ sQ47_spl
| ~ sQ1_spl
| in(sK0_skl(relation_dom(sK15_skl),relation_dom(sK15_skl)),relation_dom(sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f138,f1860]) ).
fof(f1862,plain,
( ~ sQ47_spl
| ~ sQ1_spl
| sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1861,f1625]) ).
fof(f1863,plain,
( ~ sQ47_spl
| ~ sQ1_spl
| sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f1862]) ).
fof(f1876,plain,
( ~ sQ167_spl
| ~ in(relation_dom(sK15_skl),relation_dom(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f1655,f143]) ).
fof(f1879,plain,
! [X0] :
( ~ sQ167_spl
| empty(sK15_skl)
| ~ element(ordered_pair(relation_dom(sK15_skl),X0),sK15_skl) ),
inference(resolution,[status(thm)],[f1655,f111]) ).
fof(f1880,plain,
( ~ sQ167_spl
| ~ sQ184_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1876,f564,f1798,f1654]) ).
fof(f1882,definition,
! [X0] :
( sQ193_spl
<=> ~ element(ordered_pair(relation_dom(sK15_skl),X0),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f1885,plain,
( ~ sQ167_spl
| sQ17_spl
| sQ193_spl ),
inference(split_clause,[status(thm)],[f1879,f1882,f596,f1654]) ).
fof(f1890,plain,
! [X0,X1,X2] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ relation(relation_dom(relation_dom(sK15_skl)))
| ~ in(ordered_pair(X0,ordered_pair(ordered_pair(relation_dom(relation_dom(relation_dom(sK15_skl))),X1),X2)),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f207]) ).
fof(f1891,plain,
! [X0,X1,X2] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ relation(relation_dom(relation_dom(sK15_skl)))
| ~ in(ordered_pair(X0,ordered_pair(ordered_pair(X1,relation_rng(relation_dom(relation_dom(sK15_skl)))),X2)),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f204]) ).
fof(f1892,plain,
! [X0,X1,X2,X3] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ relation(relation_dom(relation_dom(sK15_skl)))
| ~ in(relation_rng(relation_dom(relation_dom(sK15_skl))),X2)
| ~ in(ordered_pair(X0,ordered_pair(ordered_pair(X1,X2),X3)),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f230]) ).
fof(f1893,plain,
! [X0,X1] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ in(ordered_pair(X0,ordered_pair(relation_rng(relation_inverse(relation_dom(sK15_skl))),X1)),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f214]) ).
fof(f1894,plain,
! [X0,X1] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ in(ordered_pair(X0,ordered_pair(relation_dom(relation_inverse(relation_inverse(relation_dom(sK15_skl)))),X1)),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f278]) ).
fof(f1895,plain,
! [X0,X1] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ in(ordered_pair(X0,ordered_pair(relation_dom(relation_dom(sK15_skl)),X1)),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f153]) ).
fof(f1896,plain,
! [X0,X1,X2] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ relation(relation_rng(relation_dom(sK15_skl)))
| ~ in(ordered_pair(X0,ordered_pair(X1,ordered_pair(relation_dom(relation_rng(relation_dom(sK15_skl))),X2))),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f206]) ).
fof(f1897,plain,
! [X0,X1,X2] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ relation(relation_rng(relation_dom(sK15_skl)))
| ~ in(ordered_pair(X0,ordered_pair(X1,ordered_pair(X2,relation_rng(relation_rng(relation_dom(sK15_skl)))))),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f203]) ).
fof(f1898,plain,
! [X0,X1,X2,X3] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ relation(relation_rng(relation_dom(sK15_skl)))
| ~ in(relation_rng(relation_rng(relation_dom(sK15_skl))),X3)
| ~ in(ordered_pair(X0,ordered_pair(X1,ordered_pair(X2,X3))),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f229]) ).
fof(f1899,plain,
! [X0,X1] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ in(ordered_pair(X0,ordered_pair(X1,relation_dom(relation_inverse(relation_dom(sK15_skl))))),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f213]) ).
fof(f1900,plain,
! [X0,X1] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ in(ordered_pair(X0,ordered_pair(X1,relation_rng(relation_inverse(relation_inverse(relation_dom(sK15_skl)))))),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f285]) ).
fof(f1901,plain,
! [X0,X1] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ in(ordered_pair(X0,ordered_pair(X1,relation_rng(relation_dom(sK15_skl)))),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f151]) ).
fof(f1902,plain,
! [X0,X1,X2] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ in(relation_rng(relation_inverse(relation_dom(sK15_skl))),X1)
| ~ in(ordered_pair(X0,ordered_pair(X1,X2)),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f236]) ).
fof(f1903,plain,
! [X0,X1,X2] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ in(relation_dom(relation_dom(sK15_skl)),X1)
| ~ in(ordered_pair(X0,ordered_pair(X1,X2)),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f154]) ).
fof(f1904,plain,
! [X0,X1,X2] :
( ~ sQ175_spl
| ~ relation(relation_dom(sK15_skl))
| ~ in(relation_rng(relation_dom(sK15_skl)),X2)
| ~ in(ordered_pair(X0,ordered_pair(X1,X2)),relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f1687,f152]) ).
fof(f1910,definition,
! [X0,X1,X2] :
( sQ194_spl
<=> ~ in(ordered_pair(X0,ordered_pair(ordered_pair(relation_dom(relation_dom(relation_dom(sK15_skl))),X1),X2)),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f1913,definition,
( sQ195_spl
<=> relation(relation_dom(relation_dom(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f1916,definition,
( sQ196_spl
<=> relation(relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f1919,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| ~ sQ195_spl
| sQ194_spl ),
inference(split_clause,[status(thm)],[f1890,f1910,f1913,f1916,f1686]) ).
fof(f1920,definition,
! [X0,X1,X2] :
( sQ197_spl
<=> ~ in(ordered_pair(X0,ordered_pair(ordered_pair(X1,relation_rng(relation_dom(relation_dom(sK15_skl)))),X2)),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f1923,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| ~ sQ195_spl
| sQ197_spl ),
inference(split_clause,[status(thm)],[f1891,f1920,f1913,f1916,f1686]) ).
fof(f1924,definition,
! [X0,X1,X2,X3] :
( sQ198_spl
<=> ( ~ in(relation_rng(relation_dom(relation_dom(sK15_skl))),X2)
| ~ in(ordered_pair(X0,ordered_pair(ordered_pair(X1,X2),X3)),relation_inverse(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f1927,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| ~ sQ195_spl
| sQ198_spl ),
inference(split_clause,[status(thm)],[f1892,f1924,f1913,f1916,f1686]) ).
fof(f1928,definition,
! [X0,X1] :
( sQ199_spl
<=> ~ in(ordered_pair(X0,ordered_pair(relation_rng(relation_inverse(relation_dom(sK15_skl))),X1)),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f1931,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| sQ199_spl ),
inference(split_clause,[status(thm)],[f1893,f1928,f1916,f1686]) ).
fof(f1932,definition,
! [X0,X1] :
( sQ200_spl
<=> ~ in(ordered_pair(X0,ordered_pair(relation_dom(relation_inverse(relation_inverse(relation_dom(sK15_skl)))),X1)),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f1935,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| sQ200_spl ),
inference(split_clause,[status(thm)],[f1894,f1932,f1916,f1686]) ).
fof(f1936,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| sQ172_spl ),
inference(split_clause,[status(thm)],[f1895,f1673,f1916,f1686]) ).
fof(f1937,definition,
! [X0,X1,X2] :
( sQ201_spl
<=> ~ in(ordered_pair(X0,ordered_pair(X1,ordered_pair(relation_dom(relation_rng(relation_dom(sK15_skl))),X2))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f1940,definition,
( sQ202_spl
<=> relation(relation_rng(relation_dom(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f1943,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| ~ sQ202_spl
| sQ201_spl ),
inference(split_clause,[status(thm)],[f1896,f1937,f1940,f1916,f1686]) ).
fof(f1944,definition,
! [X0,X1,X2] :
( sQ203_spl
<=> ~ in(ordered_pair(X0,ordered_pair(X1,ordered_pair(X2,relation_rng(relation_rng(relation_dom(sK15_skl)))))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f1947,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| ~ sQ202_spl
| sQ203_spl ),
inference(split_clause,[status(thm)],[f1897,f1944,f1940,f1916,f1686]) ).
fof(f1948,definition,
! [X0,X1,X2,X3] :
( sQ204_spl
<=> ( ~ in(relation_rng(relation_rng(relation_dom(sK15_skl))),X3)
| ~ in(ordered_pair(X0,ordered_pair(X1,ordered_pair(X2,X3))),relation_inverse(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f1951,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| ~ sQ202_spl
| sQ204_spl ),
inference(split_clause,[status(thm)],[f1898,f1948,f1940,f1916,f1686]) ).
fof(f1952,definition,
! [X0,X1] :
( sQ205_spl
<=> ~ in(ordered_pair(X0,ordered_pair(X1,relation_dom(relation_inverse(relation_dom(sK15_skl))))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f1955,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f1899,f1952,f1916,f1686]) ).
fof(f1956,definition,
! [X0,X1] :
( sQ206_spl
<=> ~ in(ordered_pair(X0,ordered_pair(X1,relation_rng(relation_inverse(relation_inverse(relation_dom(sK15_skl)))))),relation_inverse(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f1959,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| sQ206_spl ),
inference(split_clause,[status(thm)],[f1900,f1956,f1916,f1686]) ).
fof(f1960,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| sQ173_spl ),
inference(split_clause,[status(thm)],[f1901,f1677,f1916,f1686]) ).
fof(f1961,definition,
! [X0,X1,X2] :
( sQ207_spl
<=> ( ~ in(relation_rng(relation_inverse(relation_dom(sK15_skl))),X1)
| ~ in(ordered_pair(X0,ordered_pair(X1,X2)),relation_inverse(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f1964,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| sQ207_spl ),
inference(split_clause,[status(thm)],[f1902,f1961,f1916,f1686]) ).
fof(f1965,definition,
! [X0,X1,X2] :
( sQ208_spl
<=> ( ~ in(relation_dom(relation_dom(sK15_skl)),X1)
| ~ in(ordered_pair(X0,ordered_pair(X1,X2)),relation_inverse(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f1968,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f1903,f1965,f1916,f1686]) ).
fof(f1969,definition,
! [X0,X1,X2] :
( sQ209_spl
<=> ( ~ in(relation_rng(relation_dom(sK15_skl)),X2)
| ~ in(ordered_pair(X0,ordered_pair(X1,X2)),relation_inverse(sK15_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f1972,plain,
( ~ sQ175_spl
| ~ sQ196_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f1904,f1969,f1916,f1686]) ).
fof(f1993,definition,
( sQ212_spl
<=> subset(relation_rng(sK15_skl),relation_rng(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f1995,plain,
( sQ212_spl
| ~ subset(relation_rng(sK15_skl),relation_rng(sK15_skl)) ),
inference(component_clause,[status(thm)],[f1993]) ).
fof(f2009,plain,
( sQ212_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1995,f141]) ).
fof(f2010,plain,
sQ212_spl,
inference(contradiction_clause,[status(thm)],[f2009]) ).
fof(f2016,definition,
( sQ216_spl
<=> empty(ordered_pair(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),sK3_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f2017,plain,
( ~ sQ216_spl
| empty(ordered_pair(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),sK3_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)))) ),
inference(component_clause,[status(thm)],[f2016]) ).
fof(f2020,plain,
( ~ sQ216_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2017,f87]) ).
fof(f2021,plain,
~ sQ216_spl,
inference(contradiction_clause,[status(thm)],[f2020]) ).
fof(f2022,plain,
( ~ sQ151_spl
| ~ in(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),relation_rng(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f1491,f145]) ).
fof(f2023,plain,
! [X0] :
( ~ sQ151_spl
| ~ in(ordered_pair(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),X0),relation_inverse(sK15_skl))
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f1491,f150]) ).
fof(f2025,plain,
! [X0] :
( ~ sQ151_spl
| empty(sK15_skl)
| ~ element(ordered_pair(X0,sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl))),sK15_skl) ),
inference(resolution,[status(thm)],[f1491,f111]) ).
fof(f2026,plain,
( ~ sQ151_spl
| ~ sQ45_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f2022,f564,f819,f1490]) ).
fof(f2027,plain,
( ~ sQ151_spl
| sQ46_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f2023,f564,f822,f1490]) ).
fof(f2028,definition,
! [X0] :
( sQ217_spl
<=> ~ element(ordered_pair(X0,sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl))),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f2031,plain,
( ~ sQ151_spl
| sQ17_spl
| sQ217_spl ),
inference(split_clause,[status(thm)],[f2025,f2028,f596,f1490]) ).
fof(f2032,plain,
( ~ sQ46_spl
| in(sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl)),relation_rng(sK15_skl))
| relation_rng(sK15_skl) = relation_dom(relation_inverse(sK15_skl))
| ~ relation(relation_inverse(sK15_skl)) ),
inference(resolution,[status(thm)],[f823,f63]) ).
fof(f2034,plain,
! [X0] :
( ~ sQ46_spl
| ~ in(ordered_pair(X0,sK2_skl(relation_rng(sK15_skl),relation_inverse(sK15_skl))),sK15_skl)
| ~ relation(sK15_skl) ),
inference(resolution,[status(thm)],[f823,f149]) ).
fof(f2038,plain,
( ~ sQ46_spl
| sQ45_spl
| sQ0_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f2032,f608,f134,f819,f822]) ).
fof(f2043,plain,
( ~ sQ46_spl
| sQ151_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f2034,f564,f1490,f822]) ).
fof(f2052,plain,
$false,
inference(sat_refutation,[status(thm)],[f140,f169,f197,f570,f577,f579,f588,f592,f599,f603,f604,f614,f621,f623,f630,f637,f646,f653,f666,f670,f675,f679,f686,f701,f705,f709,f713,f721,f725,f729,f776,f780,f825,f848,f852,f873,f915,f919,f927,f951,f966,f974,f1005,f1042,f1050,f1056,f1060,f1064,f1068,f1072,f1179,f1183,f1190,f1192,f1196,f1206,f1210,f1247,f1251,f1263,f1267,f1271,f1275,f1279,f1283,f1311,f1315,f1319,f1323,f1327,f1331,f1335,f1339,f1343,f1347,f1351,f1355,f1359,f1415,f1417,f1424,f1426,f1440,f1493,f1508,f1512,f1516,f1520,f1524,f1528,f1574,f1575,f1579,f1589,f1590,f1591,f1595,f1599,f1631,f1649,f1653,f1657,f1661,f1665,f1669,f1676,f1680,f1684,f1689,f1705,f1706,f1710,f1714,f1785,f1789,f1793,f1797,f1805,f1809,f1814,f1818,f1822,f1826,f1830,f1839,f1840,f1848,f1853,f1863,f1880,f1885,f1919,f1923,f1927,f1931,f1935,f1936,f1943,f1947,f1951,f1955,f1959,f1960,f1964,f1968,f1972,f2010,f2021,f2026,f2027,f2031,f2038,f2043]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU181+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.48 % Computer : n015.cluster.edu
% 0.18/0.48 % Model : x86_64 x86_64
% 0.18/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.48 % Memory : 8046.5625MB
% 0.18/0.48 % OS : Linux 6.8.0-71-generic
% 0.18/0.48 % CPULimit : 300
% 0.18/0.48 % WCLimit : 300
% 0.18/0.48 % DateTime : Mon Sep 21 05:59:06 UTC 2026
% 0.18/0.49 % CPUTime :
% 0.18/0.52 % Drodi V4.1.1
% 22.96/3.56 % Refutation found
% 22.96/3.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 22.96/3.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 20.69/3.62 % Elapsed time: 3.104734 seconds
% 20.69/3.62 % CPU time: 23.942224 seconds
% 20.69/3.62 % Total memory used: 255.304 MB
% 20.69/3.62 % Net memory used: 243.992 MB
%------------------------------------------------------------------------------