%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU206+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 : n012.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:40 PM UTC 2026
% Result : Theorem 0.07s 5.74s
% Output : CNFRefutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 113
% Syntax : Number of formulae : 505 ( 39 unt; 86 def)
% Number of atoms : 1424 ( 213 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 1538 ( 619 ~; 729 |; 71 &)
% ( 102 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 93 ( 91 usr; 87 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 5 con; 0-4 aty)
% Number of variables : 519 ( 485 !; 34 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = relation_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,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(f8,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(f19,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_dom(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_rng(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( empty(A)
=> ( relation(relation_dom(A))
& empty(relation_dom(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( empty(A)
=> ( relation(relation_rng(A))
& empty(relation_rng(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A,B] :
( relation(B)
=> subset(relation_image(B,A),relation_rng(B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,conjecture,
! [A] :
( relation(A)
=> relation_image(A,relation_dom(A)) = relation_rng(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
~ ! [A] :
( relation(A)
=> relation_image(A,relation_dom(A)) = relation_rng(A) ),
inference(negated_conjecture,[status(cth)],[f38]) ).
fof(f40,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [A,B] :
~ ( empty(B)
& A != B
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f49,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f53,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f54,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)],[f53]) ).
fof(f55,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f57,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f58,plain,
! [A] :
( ! [B,C] :
( C = relation_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) ) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f59,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C = relation_image(A,B) )
& ( ! [D] :
( ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| in(D,C) )
& ( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [A] :
( ( ! [B,C] :
( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C = relation_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| in(D,C) )
& ! [D] :
( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f61,plain,
! [A] :
( ( ! [B,C] :
( ( ( ( in(sK2_skl(C,B,A),B)
& in(ordered_pair(sK2_skl(C,B,A),sK1_skl(C,B,A)),A) )
| in(sK1_skl(C,B,A),C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,sK1_skl(C,B,A)),A) )
| ~ in(sK1_skl(C,B,A),C) ) )
| C = relation_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| in(D,C) )
& ! [D] :
( ( in(sK0_skl(D,C,B,A),B)
& in(ordered_pair(sK0_skl(D,C,B,A),D),A) )
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(E,sK0_skl(D,C,B,A)),skolemize(D,sK1_skl(C,B,A)),skolemize(E,sK2_skl(C,B,A))],[f60]) ).
fof(f62,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(sK0_skl(X3,X1,X2,X0),X3),X0)
| ~ in(X3,X1)
| X1 != relation_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [X0,X1,X2,X3] :
( in(sK0_skl(X3,X1,X2,X0),X2)
| ~ in(X3,X1)
| X1 != relation_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f64,plain,
! [X0,X1,X2,X3,X4] :
( ~ in(X4,X2)
| ~ in(ordered_pair(X4,X3),X0)
| in(X3,X1)
| X1 != relation_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f68,plain,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,B)
| ~ in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f69,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)],[f68]) ).
fof(f70,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)],[f69]) ).
fof(f71,plain,
( ! [A,B] :
( ( ~ in(sK3_skl(B,A),B)
& in(sK3_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,[sK3_skl]),skolemize(C,sK3_skl(B,A))],[f70]) ).
fof(f72,plain,
! [X0,X1,X2] :
( in(X2,X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [X0,X1] :
( in(sK3_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f74,plain,
! [X0,X1] :
( ~ in(sK3_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f75,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)],[f7]) ).
fof(f76,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)],[f75]) ).
fof(f77,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)],[f76]) ).
fof(f78,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK5_skl(B,A),sK6_skl(B,A)),A)
| in(sK5_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(sK5_skl(B,A),D),A)
| ~ in(sK5_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,sK4_skl(C,B,A)),A)
| ~ in(C,B) ) )
| B != relation_dom(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))],[f77]) ).
fof(f79,plain,
! [X0,X1,X2] :
( in(ordered_pair(X2,sK4_skl(X2,X1,X0)),X0)
| ~ in(X2,X1)
| X1 != relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f80,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)],[f78]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(sK5_skl(X1,X0),X2),X0)
| ~ in(sK5_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f82,plain,
! [X0,X1] :
( in(ordered_pair(sK5_skl(X1,X0),sK6_skl(X1,X0)),X0)
| in(sK5_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f83,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)],[f8]) ).
fof(f84,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)],[f83]) ).
fof(f85,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)],[f84]) ).
fof(f86,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK9_skl(B,A),sK8_skl(B,A)),A)
| in(sK8_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(D,sK8_skl(B,A)),A)
| ~ in(sK8_skl(B,A),B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(sK7_skl(C,B,A),C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl]),skolemize(D,sK7_skl(C,B,A)),skolemize(C,sK8_skl(B,A)),skolemize(D,sK9_skl(B,A))],[f85]) ).
fof(f87,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK7_skl(X2,X1,X0),X2),X0)
| ~ in(X2,X1)
| X1 != relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f88,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)],[f86]) ).
fof(f89,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X2,sK8_skl(X1,X0)),X0)
| ~ in(sK8_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f90,plain,
! [X0,X1] :
( in(ordered_pair(sK9_skl(X1,X0),sK8_skl(X1,X0)),X0)
| in(sK8_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f92,plain,
! [A] : element(sK10_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(B,sK10_skl(A))],[f19]) ).
fof(f93,plain,
! [X0] : element(sK10_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f94,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f101,plain,
! [A] :
( ~ empty(relation_dom(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f102,plain,
! [X0] :
( ~ empty(relation_dom(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
! [A] :
( ~ empty(relation_rng(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f104,plain,
! [X0] :
( ~ empty(relation_rng(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [A] :
( ( relation(relation_dom(A))
& empty(relation_dom(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f106,plain,
! [X0] :
( empty(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f108,plain,
! [A] :
( ( relation(relation_rng(A))
& empty(relation_rng(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f109,plain,
! [X0] :
( empty(relation_rng(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f110,plain,
! [X0] :
( relation(relation_rng(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f111,plain,
( relation(sK11_skl)
& empty(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f30]) ).
fof(f112,plain,
empty(sK11_skl),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
relation(sK11_skl),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f114,plain,
! [A] :
( ? [B] :
( ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f115,plain,
! [A] :
( ( ~ empty(sK12_skl(A))
& element(sK12_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(B,sK12_skl(A))],[f114]) ).
fof(f116,plain,
! [X0] :
( element(sK12_skl(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f117,plain,
! [X0] :
( ~ empty(sK12_skl(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f118,plain,
empty(sK13_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f32]) ).
fof(f119,plain,
empty(sK13_skl),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
( relation(sK14_skl)
& ~ empty(sK14_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f33]) ).
fof(f121,plain,
~ empty(sK14_skl),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f122,plain,
relation(sK14_skl),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f123,plain,
! [A] :
( empty(sK15_skl(A))
& element(sK15_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(B,sK15_skl(A))],[f34]) ).
fof(f124,plain,
! [X0] : element(sK15_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [X0] : empty(sK15_skl(X0)),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f130,plain,
! [A,B] :
( subset(relation_image(B,A),relation_rng(B))
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f131,plain,
! [B] :
( ! [A] : subset(relation_image(B,A),relation_rng(B))
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f132,plain,
! [X0,X1] :
( subset(relation_image(X0,X1),relation_rng(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
? [A] :
( relation_image(A,relation_dom(A)) != relation_rng(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f134,plain,
( relation_image(sK17_skl,relation_dom(sK17_skl)) != relation_rng(sK17_skl)
& relation(sK17_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(A,sK17_skl)],[f133]) ).
fof(f135,plain,
relation(sK17_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
relation_image(sK17_skl,relation_dom(sK17_skl)) != relation_rng(sK17_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f137,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f138,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f140,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f141,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f142,plain,
( ! [A,B] :
( ~ subset(A,B)
| element(A,powerset(B)) )
& ! [A,B] :
( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(miniscoping,[status(thm)],[f141]) ).
fof(f143,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f144,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f145,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f146,plain,
! [A,C] :
( element(A,C)
| ! [B] :
( ~ element(B,powerset(C))
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f145]) ).
fof(f147,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f149,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f148]) ).
fof(f150,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f151,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f152,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f154,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f153]) ).
fof(f155,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f157,plain,
! [B] :
( ~ empty(B)
| ! [A] :
( A = B
| ~ empty(A) ) ),
inference(miniscoping,[status(thm)],[f156]) ).
fof(f158,plain,
! [X0,X1] :
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f159,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f55]) ).
fof(f161,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK0_skl(X1,relation_image(X0,X2),X2,X0),X1),X0)
| ~ in(X1,relation_image(X0,X2))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f62]) ).
fof(f162,plain,
! [X0,X1,X2] :
( in(sK0_skl(X1,relation_image(X0,X2),X2,X0),X2)
| ~ in(X1,relation_image(X0,X2))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f63]) ).
fof(f163,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,X2)
| ~ in(ordered_pair(X3,X1),X0)
| in(X1,relation_image(X0,X2))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f64]) ).
fof(f164,plain,
! [X0,X1] :
( in(ordered_pair(X1,sK4_skl(X1,relation_dom(X0),X0)),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f79]) ).
fof(f165,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),X0)
| in(X1,relation_dom(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f80]) ).
fof(f166,plain,
! [X0,X1] :
( in(ordered_pair(sK7_skl(X1,relation_rng(X0),X0),X1),X0)
| ~ in(X1,relation_rng(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f87]) ).
fof(f167,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X2,X1),X0)
| in(X1,relation_rng(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f88]) ).
fof(f172,plain,
( ~ empty(relation_rng(sK14_skl))
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f121,f104]) ).
fof(f173,plain,
( ~ empty(relation_dom(sK14_skl))
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f121,f102]) ).
fof(f174,definition,
( sQ0_spl
<=> relation(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f176,plain,
( sQ0_spl
| ~ relation(sK14_skl) ),
inference(component_clause,[status(thm)],[f174]) ).
fof(f177,definition,
( sQ1_spl
<=> empty(relation_rng(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f180,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f172,f174,f177]) ).
fof(f181,definition,
( sQ2_spl
<=> empty(relation_dom(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f184,plain,
( ~ sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f173,f174,f181]) ).
fof(f185,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f176,f122]) ).
fof(f186,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f185]) ).
fof(f211,plain,
! [X0] : sK15_skl(X0) = empty_set,
inference(resolution,[status(thm)],[f152,f125]) ).
fof(f212,plain,
sK13_skl = empty_set,
inference(resolution,[status(thm)],[f152,f119]) ).
fof(f213,plain,
sK11_skl = empty_set,
inference(resolution,[status(thm)],[f152,f112]) ).
fof(f215,plain,
! [X0] :
( ~ empty(X0)
| relation_rng(X0) = empty_set ),
inference(resolution,[status(thm)],[f152,f109]) ).
fof(f216,plain,
! [X0] :
( ~ empty(X0)
| relation_dom(X0) = empty_set ),
inference(resolution,[status(thm)],[f152,f106]) ).
fof(f217,plain,
! [X0] :
( ~ empty(relation_rng(X0))
| ~ relation(X0)
| X0 = empty_set ),
inference(resolution,[status(thm)],[f152,f104]) ).
fof(f220,plain,
! [X0] : element(empty_set,powerset(X0)),
inference(backward_demodulation,[status(thm)],[f211,f124]) ).
fof(f221,plain,
! [X0] :
( X0 = sK13_skl
| ~ empty(X0) ),
inference(backward_demodulation,[status(thm)],[f212,f152]) ).
fof(f225,plain,
sK13_skl = sK11_skl,
inference(backward_demodulation,[status(thm)],[f213,f212]) ).
fof(f226,plain,
! [X0] :
( ~ empty(X0)
| relation_rng(X0) = sK11_skl ),
inference(forward_demodulation,[status(thm)],[f213,f215]) ).
fof(f227,plain,
! [X0] :
( ~ empty(X0)
| relation_dom(X0) = sK11_skl ),
inference(forward_demodulation,[status(thm)],[f213,f216]) ).
fof(f228,plain,
! [X0] :
( ~ empty(relation_rng(X0))
| ~ relation(X0)
| X0 = sK11_skl ),
inference(forward_demodulation,[status(thm)],[f213,f217]) ).
fof(f231,plain,
! [X0] : element(sK11_skl,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f213,f220]) ).
fof(f235,plain,
! [X0] :
( X0 = sK11_skl
| ~ empty(X0) ),
inference(backward_demodulation,[status(thm)],[f225,f221]) ).
fof(f236,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ subset(relation_rng(X0),relation_image(X0,X1))
| relation_rng(X0) = relation_image(X0,X1) ),
inference(resolution,[status(thm)],[f57,f132]) ).
fof(f270,plain,
relation_rng(sK11_skl) = sK11_skl,
inference(resolution,[status(thm)],[f226,f112]) ).
fof(f274,plain,
! [X0] :
( ~ empty(relation_dom(X0))
| ~ relation(X0)
| relation_rng(X0) = sK11_skl ),
inference(resolution,[status(thm)],[f226,f102]) ).
fof(f276,plain,
! [X0] :
( subset(relation_image(sK11_skl,X0),sK11_skl)
| ~ relation(sK11_skl) ),
inference(paramodulation,[status(thm)],[f270,f132]) ).
fof(f277,plain,
( relation(sK11_skl)
| ~ empty(sK11_skl) ),
inference(paramodulation,[status(thm)],[f270,f110]) ).
fof(f279,definition,
( sQ12_spl
<=> relation(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f282,definition,
! [X0] :
( sQ13_spl
<=> subset(relation_image(sK11_skl,X0),sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f283,plain,
! [X0] :
( ~ sQ13_spl
| subset(relation_image(sK11_skl,X0),sK11_skl) ),
inference(component_clause,[status(thm)],[f282]) ).
fof(f285,plain,
( sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f276,f279,f282]) ).
fof(f286,definition,
( sQ14_spl
<=> empty(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f288,plain,
( sQ14_spl
| ~ empty(sK11_skl) ),
inference(component_clause,[status(thm)],[f286]) ).
fof(f289,plain,
( sQ12_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f277,f286,f279]) ).
fof(f291,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f288,f112]) ).
fof(f292,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f291]) ).
fof(f293,plain,
relation_dom(sK11_skl) = sK11_skl,
inference(resolution,[status(thm)],[f227,f112]) ).
fof(f296,plain,
! [X0] :
( ~ empty(relation_rng(X0))
| ~ relation(X0)
| relation_dom(X0) = sK11_skl ),
inference(resolution,[status(thm)],[f227,f104]) ).
fof(f330,plain,
( ~ empty(sK11_skl)
| ~ relation(sK11_skl)
| sK11_skl = sK11_skl ),
inference(paramodulation,[status(thm)],[f270,f228]) ).
fof(f331,definition,
( sQ15_spl
<=> sK11_skl = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( ~ sQ14_spl
| ~ sQ12_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f330,f331,f279,f286]) ).
fof(f352,plain,
! [X0,X1] :
( ~ empty(relation_rng(X1))
| ~ relation(X1)
| X0 = X1
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f158,f104]) ).
fof(f354,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| X1 = X0
| ~ element(X0,powerset(X1)) ),
inference(resolution,[status(thm)],[f143,f57]) ).
fof(f467,plain,
( ~ empty(sK11_skl)
| ~ relation(sK11_skl)
| relation_rng(sK11_skl) = sK11_skl ),
inference(paramodulation,[status(thm)],[f293,f274]) ).
fof(f468,definition,
( sQ16_spl
<=> relation_rng(sK11_skl) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( ~ sQ14_spl
| ~ sQ12_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f467,f468,f279,f286]) ).
fof(f475,plain,
( ~ empty(sK11_skl)
| ~ relation(sK11_skl)
| relation_dom(sK11_skl) = sK11_skl ),
inference(paramodulation,[status(thm)],[f270,f296]) ).
fof(f476,definition,
( sQ17_spl
<=> relation_dom(sK11_skl) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f479,plain,
( ~ sQ14_spl
| ~ sQ12_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f475,f476,f279,f286]) ).
fof(f486,plain,
! [X0] :
( in(sK10_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f140,f93]) ).
fof(f487,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| in(X1,powerset(X0))
| empty(powerset(X0)) ),
inference(resolution,[status(thm)],[f140,f144]) ).
fof(f491,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| in(X0,powerset(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f487,f94]) ).
fof(f497,plain,
! [X0] :
( ~ in(X0,sK10_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f486,f49]) ).
fof(f499,plain,
! [X0,X1] :
( ~ relation(X0)
| in(relation_image(X0,X1),powerset(relation_rng(X0))) ),
inference(resolution,[status(thm)],[f491,f132]) ).
fof(f500,plain,
! [X0,X1] :
( in(sK3_skl(X1,X0),X0)
| in(X0,powerset(X1)) ),
inference(resolution,[status(thm)],[f491,f73]) ).
fof(f501,plain,
! [X0,X1] :
( ~ element(X0,powerset(X1))
| in(X0,powerset(X1)) ),
inference(resolution,[status(thm)],[f491,f143]) ).
fof(f502,plain,
! [X0] : in(X0,powerset(X0)),
inference(resolution,[status(thm)],[f491,f159]) ).
fof(f507,plain,
! [X0] : ~ in(powerset(X0),X0),
inference(resolution,[status(thm)],[f502,f49]) ).
fof(f513,plain,
! [X0,X1,X2] :
( ~ relation(X1)
| in(X0,relation_rng(X1))
| ~ in(X0,relation_image(X1,X2)) ),
inference(resolution,[status(thm)],[f72,f132]) ).
fof(f518,plain,
! [X0] :
( ~ subset(X0,sK11_skl)
| X0 = sK11_skl ),
inference(resolution,[status(thm)],[f354,f231]) ).
fof(f522,plain,
! [X0] :
( ~ sQ13_spl
| relation_image(sK11_skl,X0) = sK11_skl ),
inference(resolution,[status(thm)],[f518,f283]) ).
fof(f523,plain,
! [X0] :
( in(sK3_skl(sK11_skl,X0),X0)
| X0 = sK11_skl ),
inference(resolution,[status(thm)],[f518,f73]) ).
fof(f524,plain,
! [X0] :
( ~ element(X0,powerset(sK11_skl))
| X0 = sK11_skl ),
inference(resolution,[status(thm)],[f518,f143]) ).
fof(f541,plain,
! [X0] :
( in(ordered_pair(X0,sK4_skl(X0,relation_dom(sK11_skl),sK11_skl)),sK11_skl)
| ~ in(X0,sK11_skl)
| ~ relation(sK11_skl) ),
inference(paramodulation,[status(thm)],[f293,f164]) ).
fof(f542,definition,
! [X0] :
( sQ20_spl
<=> ( in(ordered_pair(X0,sK4_skl(X0,relation_dom(sK11_skl),sK11_skl)),sK11_skl)
| ~ in(X0,sK11_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f545,plain,
( sQ20_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f541,f279,f542]) ).
fof(f548,plain,
! [X0] :
( in(ordered_pair(sK5_skl(X0,sK11_skl),sK6_skl(X0,sK11_skl)),sK11_skl)
| in(sK5_skl(X0,sK11_skl),X0)
| X0 = relation_dom(sK11_skl) ),
inference(resolution,[status(thm)],[f82,f113]) ).
fof(f551,plain,
! [X0] :
( in(ordered_pair(sK5_skl(X0,sK17_skl),sK6_skl(X0,sK17_skl)),sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(resolution,[status(thm)],[f82,f135]) ).
fof(f553,plain,
! [X0] :
( in(ordered_pair(sK5_skl(X0,sK11_skl),sK6_skl(X0,sK11_skl)),sK11_skl)
| in(sK5_skl(X0,sK11_skl),X0)
| X0 = sK11_skl ),
inference(forward_demodulation,[status(thm)],[f293,f548]) ).
fof(f555,plain,
! [X0] :
( in(sK6_skl(X0,sK17_skl),relation_rng(sK17_skl))
| ~ relation(sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(resolution,[status(thm)],[f551,f167]) ).
fof(f556,plain,
! [X0] :
( in(sK5_skl(X0,sK17_skl),relation_dom(sK17_skl))
| ~ relation(sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(resolution,[status(thm)],[f551,f165]) ).
fof(f557,plain,
! [X0,X1] :
( ~ in(sK5_skl(X0,sK17_skl),X1)
| in(sK6_skl(X0,sK17_skl),relation_image(sK17_skl,X1))
| ~ relation(sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(resolution,[status(thm)],[f551,f163]) ).
fof(f560,definition,
! [X0] :
( sQ21_spl
<=> ( in(sK6_skl(X0,sK17_skl),relation_rng(sK17_skl))
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f561,plain,
! [X0] :
( ~ sQ21_spl
| in(sK6_skl(X0,sK17_skl),relation_rng(sK17_skl))
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(component_clause,[status(thm)],[f560]) ).
fof(f563,definition,
( sQ22_spl
<=> relation(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f565,plain,
( sQ22_spl
| ~ relation(sK17_skl) ),
inference(component_clause,[status(thm)],[f563]) ).
fof(f566,plain,
( ~ sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f555,f560,f563]) ).
fof(f567,definition,
! [X0] :
( sQ23_spl
<=> ( in(sK5_skl(X0,sK17_skl),relation_dom(sK17_skl))
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f568,plain,
! [X0] :
( ~ sQ23_spl
| in(sK5_skl(X0,sK17_skl),relation_dom(sK17_skl))
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(component_clause,[status(thm)],[f567]) ).
fof(f570,plain,
( ~ sQ22_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f556,f567,f563]) ).
fof(f571,definition,
! [X0,X1] :
( sQ24_spl
<=> ( ~ in(sK5_skl(X0,sK17_skl),X1)
| in(sK6_skl(X0,sK17_skl),relation_image(sK17_skl,X1))
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f572,plain,
! [X0,X1] :
( ~ sQ24_spl
| ~ in(sK5_skl(X0,sK17_skl),X1)
| in(sK6_skl(X0,sK17_skl),relation_image(sK17_skl,X1))
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(component_clause,[status(thm)],[f571]) ).
fof(f574,plain,
( ~ sQ22_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f557,f571,f563]) ).
fof(f582,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f565,f135]) ).
fof(f583,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f582]) ).
fof(f645,plain,
! [X0,X1] :
( ~ sQ13_spl
| in(sK0_skl(X0,relation_image(sK11_skl,X1),X1,sK11_skl),X1)
| ~ in(X0,sK11_skl)
| ~ relation(sK11_skl) ),
inference(paramodulation,[status(thm)],[f522,f162]) ).
fof(f646,plain,
! [X0,X1] :
( ~ sQ13_spl
| in(ordered_pair(sK0_skl(X0,relation_image(sK11_skl,X1),X1,sK11_skl),X0),sK11_skl)
| ~ in(X0,sK11_skl)
| ~ relation(sK11_skl) ),
inference(paramodulation,[status(thm)],[f522,f161]) ).
fof(f647,plain,
( ~ sQ13_spl
| subset(sK11_skl,relation_rng(sK11_skl))
| ~ relation(sK11_skl) ),
inference(paramodulation,[status(thm)],[f522,f132]) ).
fof(f648,definition,
! [X0,X1] :
( sQ36_spl
<=> ( in(sK0_skl(X0,relation_image(sK11_skl,X1),X1,sK11_skl),X1)
| ~ in(X0,sK11_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f651,plain,
( ~ sQ13_spl
| sQ36_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f645,f279,f648,f282]) ).
fof(f652,definition,
! [X0,X1] :
( sQ37_spl
<=> ( in(ordered_pair(sK0_skl(X0,relation_image(sK11_skl,X1),X1,sK11_skl),X0),sK11_skl)
| ~ in(X0,sK11_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f655,plain,
( ~ sQ13_spl
| sQ37_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f646,f279,f652,f282]) ).
fof(f656,definition,
( sQ38_spl
<=> subset(sK11_skl,relation_rng(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f659,plain,
( ~ sQ13_spl
| sQ38_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f647,f279,f656,f282]) ).
fof(f699,plain,
! [X0] :
( ~ empty(sK11_skl)
| ~ relation(sK11_skl)
| X0 = sK11_skl
| ~ empty(X0) ),
inference(paramodulation,[status(thm)],[f270,f352]) ).
fof(f700,definition,
! [X0] :
( sQ39_spl
<=> ( X0 = sK11_skl
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f703,plain,
( ~ sQ14_spl
| ~ sQ12_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f699,f700,f279,f286]) ).
fof(f714,plain,
! [X0] :
( ~ relation(sK11_skl)
| ~ subset(sK11_skl,relation_image(sK11_skl,X0))
| relation_rng(sK11_skl) = relation_image(sK11_skl,X0) ),
inference(paramodulation,[status(thm)],[f270,f236]) ).
fof(f716,definition,
! [X0] :
( sQ40_spl
<=> ( ~ subset(sK11_skl,relation_image(sK11_skl,X0))
| relation_rng(sK11_skl) = relation_image(sK11_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f719,plain,
( ~ sQ12_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f714,f716,f279]) ).
fof(f732,plain,
sK10_skl(powerset(sK11_skl)) = sK11_skl,
inference(resolution,[status(thm)],[f524,f93]) ).
fof(f734,plain,
! [X0] :
( ~ in(X0,powerset(sK11_skl))
| X0 = sK11_skl ),
inference(resolution,[status(thm)],[f524,f138]) ).
fof(f739,plain,
( ~ in(powerset(sK11_skl),sK11_skl)
| empty(powerset(sK11_skl)) ),
inference(paramodulation,[status(thm)],[f732,f497]) ).
fof(f740,plain,
( in(sK11_skl,powerset(sK11_skl))
| empty(powerset(sK11_skl)) ),
inference(paramodulation,[status(thm)],[f732,f486]) ).
fof(f742,definition,
( sQ44_spl
<=> empty(powerset(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f743,plain,
( ~ sQ44_spl
| empty(powerset(sK11_skl)) ),
inference(component_clause,[status(thm)],[f742]) ).
fof(f745,definition,
( sQ45_spl
<=> in(powerset(sK11_skl),sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f748,plain,
( ~ sQ45_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f739,f742,f745]) ).
fof(f749,definition,
( sQ46_spl
<=> in(sK11_skl,powerset(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f752,plain,
( sQ46_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f740,f742,f749]) ).
fof(f753,plain,
( ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f743,f94]) ).
fof(f754,plain,
~ sQ44_spl,
inference(contradiction_clause,[status(thm)],[f753]) ).
fof(f756,plain,
( empty(powerset(sK11_skl))
| sK10_skl(powerset(sK11_skl)) = sK11_skl ),
inference(resolution,[status(thm)],[f734,f486]) ).
fof(f762,definition,
( sQ47_spl
<=> sK10_skl(powerset(sK11_skl)) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f765,plain,
( sQ44_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f756,f762,f742]) ).
fof(f767,plain,
( sK3_skl(sK11_skl,powerset(sK11_skl)) = sK11_skl
| powerset(sK11_skl) = sK11_skl ),
inference(resolution,[status(thm)],[f523,f734]) ).
fof(f774,definition,
( sQ48_spl
<=> powerset(sK11_skl) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f775,plain,
( ~ sQ48_spl
| powerset(sK11_skl) = sK11_skl ),
inference(component_clause,[status(thm)],[f774]) ).
fof(f776,plain,
( sQ48_spl
| powerset(sK11_skl) != sK11_skl ),
inference(component_clause,[status(thm)],[f774]) ).
fof(f777,definition,
( sQ49_spl
<=> sK3_skl(sK11_skl,powerset(sK11_skl)) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f778,plain,
( ~ sQ49_spl
| sK3_skl(sK11_skl,powerset(sK11_skl)) = sK11_skl ),
inference(component_clause,[status(thm)],[f777]) ).
fof(f780,plain,
( sQ49_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f767,f774,f777]) ).
fof(f794,plain,
( ~ sQ48_spl
| ~ in(sK11_skl,sK11_skl) ),
inference(paramodulation,[status(thm)],[f775,f507]) ).
fof(f795,plain,
( ~ sQ48_spl
| in(sK11_skl,sK11_skl) ),
inference(paramodulation,[status(thm)],[f775,f502]) ).
fof(f812,plain,
( ~ sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f795,f794]) ).
fof(f813,plain,
~ sQ48_spl,
inference(contradiction_clause,[status(thm)],[f812]) ).
fof(f820,plain,
( ~ sQ49_spl
| ~ in(sK11_skl,sK11_skl)
| subset(powerset(sK11_skl),sK11_skl) ),
inference(paramodulation,[status(thm)],[f778,f74]) ).
fof(f822,definition,
( sQ52_spl
<=> subset(powerset(sK11_skl),sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f823,plain,
( ~ sQ52_spl
| subset(powerset(sK11_skl),sK11_skl) ),
inference(component_clause,[status(thm)],[f822]) ).
fof(f824,plain,
( sQ52_spl
| ~ subset(powerset(sK11_skl),sK11_skl) ),
inference(component_clause,[status(thm)],[f822]) ).
fof(f825,definition,
( sQ53_spl
<=> in(sK11_skl,sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f828,plain,
( ~ sQ49_spl
| ~ sQ53_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f820,f822,f825,f777]) ).
fof(f829,plain,
( ~ sQ52_spl
| powerset(sK11_skl) = sK11_skl ),
inference(resolution,[status(thm)],[f823,f518]) ).
fof(f833,plain,
( ~ sQ52_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f829,f774,f822]) ).
fof(f839,plain,
( sQ52_spl
| ~ element(powerset(sK11_skl),powerset(sK11_skl)) ),
inference(resolution,[status(thm)],[f824,f143]) ).
fof(f858,plain,
( sQ52_spl
| ~ in(powerset(sK11_skl),powerset(sK11_skl)) ),
inference(resolution,[status(thm)],[f839,f138]) ).
fof(f863,plain,
! [X0] :
( in(ordered_pair(sK7_skl(X0,relation_rng(sK11_skl),sK11_skl),X0),sK11_skl)
| ~ in(X0,sK11_skl)
| ~ relation(sK11_skl) ),
inference(paramodulation,[status(thm)],[f270,f166]) ).
fof(f864,definition,
! [X0] :
( sQ55_spl
<=> ( in(ordered_pair(sK7_skl(X0,relation_rng(sK11_skl),sK11_skl),X0),sK11_skl)
| ~ in(X0,sK11_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f867,plain,
( sQ55_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f863,f279,f864]) ).
fof(f870,plain,
! [X0] :
( in(ordered_pair(sK9_skl(X0,sK11_skl),sK8_skl(X0,sK11_skl)),sK11_skl)
| in(sK8_skl(X0,sK11_skl),X0)
| X0 = relation_rng(sK11_skl) ),
inference(resolution,[status(thm)],[f90,f113]) ).
fof(f873,plain,
! [X0] :
( in(ordered_pair(sK9_skl(X0,sK17_skl),sK8_skl(X0,sK17_skl)),sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f90,f135]) ).
fof(f875,plain,
! [X0] :
( in(ordered_pair(sK9_skl(X0,sK11_skl),sK8_skl(X0,sK11_skl)),sK11_skl)
| in(sK8_skl(X0,sK11_skl),X0)
| X0 = sK11_skl ),
inference(forward_demodulation,[status(thm)],[f270,f870]) ).
fof(f877,plain,
! [X0] :
( ~ sQ21_spl
| in(ordered_pair(sK7_skl(sK6_skl(X0,sK17_skl),relation_rng(sK17_skl),sK17_skl),sK6_skl(X0,sK17_skl)),sK17_skl)
| ~ relation(sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(resolution,[status(thm)],[f561,f166]) ).
fof(f880,definition,
! [X0] :
( sQ56_spl
<=> ( in(ordered_pair(sK7_skl(sK6_skl(X0,sK17_skl),relation_rng(sK17_skl),sK17_skl),sK6_skl(X0,sK17_skl)),sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f883,plain,
( ~ sQ21_spl
| ~ sQ22_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f877,f880,f563,f560]) ).
fof(f1078,plain,
! [X0] :
( ~ sQ13_spl
| ~ relation(sK11_skl)
| in(X0,relation_rng(sK11_skl))
| ~ in(X0,sK11_skl) ),
inference(paramodulation,[status(thm)],[f522,f513]) ).
fof(f1079,definition,
! [X0] :
( sQ57_spl
<=> ( in(X0,relation_rng(sK11_skl))
| ~ in(X0,sK11_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1082,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1078,f1079,f279,f282]) ).
fof(f1087,plain,
! [X0] : in(sK10_skl(powerset(X0)),powerset(X0)),
inference(resolution,[status(thm)],[f501,f93]) ).
fof(f1107,plain,
! [X0,X1] :
( ~ element(X1,powerset(sK11_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f150,f112]) ).
fof(f1111,plain,
! [X0,X1,X2] :
( ~ empty(relation_dom(X2))
| ~ relation(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f150,f102]) ).
fof(f1113,plain,
! [X0] : ~ in(X0,sK11_skl),
inference(resolution,[status(thm)],[f1107,f231]) ).
fof(f1115,plain,
! [X0,X1] :
( ~ subset(X1,sK11_skl)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f1107,f144]) ).
fof(f1116,plain,
! [X0,X1] :
( ~ in(X1,powerset(sK11_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f1107,f138]) ).
fof(f1121,plain,
! [X0] :
( in(sK8_skl(X0,sK11_skl),X0)
| X0 = sK11_skl ),
inference(backward_subsumption_resolution,[status(thm)],[f875,f1113]) ).
fof(f1122,plain,
! [X0] :
( in(sK5_skl(X0,sK11_skl),X0)
| X0 = sK11_skl ),
inference(backward_subsumption_resolution,[status(thm)],[f553,f1113]) ).
fof(f1128,plain,
! [X0,X1] :
( in(sK3_skl(sK11_skl,X1),X1)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f1115,f73]) ).
fof(f1131,plain,
! [X0] :
( powerset(sK11_skl) = sK11_skl
| ~ in(X0,sK3_skl(sK11_skl,powerset(sK11_skl))) ),
inference(resolution,[status(thm)],[f1116,f523]) ).
fof(f1134,plain,
! [X0] :
( empty(powerset(sK11_skl))
| ~ in(X0,sK10_skl(powerset(sK11_skl))) ),
inference(resolution,[status(thm)],[f1116,f486]) ).
fof(f1139,definition,
! [X0] :
( sQ59_spl
<=> ~ in(X0,sK3_skl(sK11_skl,powerset(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1142,plain,
( sQ48_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1131,f1139,f774]) ).
fof(f1145,definition,
! [X0] :
( sQ60_spl
<=> ~ in(X0,sK10_skl(powerset(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1148,plain,
( sQ44_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1134,f1145,f742]) ).
fof(f1151,plain,
! [X0,X1] :
( ~ in(ordered_pair(X1,sK8_skl(X0,sK11_skl)),sK11_skl)
| X0 = relation_rng(sK11_skl)
| ~ relation(sK11_skl)
| X0 = sK11_skl ),
inference(resolution,[status(thm)],[f1121,f89]) ).
fof(f1154,plain,
! [X0] :
( ~ in(X0,sK8_skl(powerset(sK11_skl),sK11_skl))
| powerset(sK11_skl) = sK11_skl ),
inference(resolution,[status(thm)],[f1121,f1116]) ).
fof(f1155,plain,
( sK8_skl(powerset(sK11_skl),sK11_skl) = sK11_skl
| powerset(sK11_skl) = sK11_skl ),
inference(resolution,[status(thm)],[f1121,f734]) ).
fof(f1162,definition,
! [X0,X1] :
( sQ61_spl
<=> ( ~ in(ordered_pair(X1,sK8_skl(X0,sK11_skl)),sK11_skl)
| X0 = relation_rng(sK11_skl)
| X0 = sK11_skl ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1165,plain,
( ~ sQ12_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1151,f1162,f279]) ).
fof(f1166,definition,
! [X0] :
( sQ62_spl
<=> ~ in(X0,sK8_skl(powerset(sK11_skl),sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1169,plain,
( sQ62_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1154,f774,f1166]) ).
fof(f1170,definition,
( sQ63_spl
<=> sK8_skl(powerset(sK11_skl),sK11_skl) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1171,plain,
( ~ sQ63_spl
| sK8_skl(powerset(sK11_skl),sK11_skl) = sK11_skl ),
inference(component_clause,[status(thm)],[f1170]) ).
fof(f1173,plain,
( sQ63_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1155,f774,f1170]) ).
fof(f1178,plain,
! [X0] :
( ~ sQ63_spl
| ~ in(ordered_pair(X0,sK8_skl(powerset(sK11_skl),sK11_skl)),sK11_skl)
| ~ in(sK11_skl,powerset(sK11_skl))
| powerset(sK11_skl) = relation_rng(sK11_skl)
| ~ relation(sK11_skl) ),
inference(paramodulation,[status(thm)],[f1171,f89]) ).
fof(f1180,definition,
( sQ64_spl
<=> powerset(sK11_skl) = relation_rng(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1181,plain,
( ~ sQ64_spl
| powerset(sK11_skl) = relation_rng(sK11_skl) ),
inference(component_clause,[status(thm)],[f1180]) ).
fof(f1183,definition,
! [X0] :
( sQ65_spl
<=> ~ in(ordered_pair(X0,sK8_skl(powerset(sK11_skl),sK11_skl)),sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1186,plain,
( ~ sQ63_spl
| sQ65_spl
| ~ sQ46_spl
| sQ64_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1178,f279,f1180,f749,f1183,f1170]) ).
fof(f1187,plain,
( ~ sQ64_spl
| powerset(sK11_skl) = sK11_skl ),
inference(forward_demodulation,[status(thm)],[f270,f1181]) ).
fof(f1188,plain,
( ~ sQ64_spl
| sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1187,f776]) ).
fof(f1189,plain,
( ~ sQ64_spl
| sQ48_spl ),
inference(contradiction_clause,[status(thm)],[f1188]) ).
fof(f1192,plain,
! [X0,X1] :
( ~ in(ordered_pair(sK5_skl(X0,sK11_skl),X1),sK11_skl)
| X0 = relation_dom(sK11_skl)
| ~ relation(sK11_skl)
| X0 = sK11_skl ),
inference(resolution,[status(thm)],[f1122,f81]) ).
fof(f1195,plain,
! [X0] :
( ~ in(X0,sK5_skl(powerset(sK11_skl),sK11_skl))
| powerset(sK11_skl) = sK11_skl ),
inference(resolution,[status(thm)],[f1122,f1116]) ).
fof(f1196,plain,
( sK5_skl(powerset(sK11_skl),sK11_skl) = sK11_skl
| powerset(sK11_skl) = sK11_skl ),
inference(resolution,[status(thm)],[f1122,f734]) ).
fof(f1203,definition,
! [X0,X1] :
( sQ66_spl
<=> ( ~ in(ordered_pair(sK5_skl(X0,sK11_skl),X1),sK11_skl)
| X0 = relation_dom(sK11_skl)
| X0 = sK11_skl ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1206,plain,
( ~ sQ12_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f1192,f1203,f279]) ).
fof(f1207,definition,
! [X0] :
( sQ67_spl
<=> ~ in(X0,sK5_skl(powerset(sK11_skl),sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1210,plain,
( sQ67_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1195,f774,f1207]) ).
fof(f1211,definition,
( sQ68_spl
<=> sK5_skl(powerset(sK11_skl),sK11_skl) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1212,plain,
( ~ sQ68_spl
| sK5_skl(powerset(sK11_skl),sK11_skl) = sK11_skl ),
inference(component_clause,[status(thm)],[f1211]) ).
fof(f1214,plain,
( sQ68_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1196,f774,f1211]) ).
fof(f1219,plain,
! [X0] :
( ~ sQ68_spl
| ~ in(ordered_pair(sK5_skl(powerset(sK11_skl),sK11_skl),X0),sK11_skl)
| ~ in(sK11_skl,powerset(sK11_skl))
| powerset(sK11_skl) = relation_dom(sK11_skl)
| ~ relation(sK11_skl) ),
inference(paramodulation,[status(thm)],[f1212,f81]) ).
fof(f1221,definition,
( sQ69_spl
<=> powerset(sK11_skl) = relation_dom(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1222,plain,
( ~ sQ69_spl
| powerset(sK11_skl) = relation_dom(sK11_skl) ),
inference(component_clause,[status(thm)],[f1221]) ).
fof(f1224,definition,
! [X0] :
( sQ70_spl
<=> ~ in(ordered_pair(sK5_skl(powerset(sK11_skl),sK11_skl),X0),sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1227,plain,
( ~ sQ68_spl
| sQ70_spl
| ~ sQ46_spl
| sQ69_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1219,f279,f1221,f749,f1224,f1211]) ).
fof(f1228,plain,
( ~ sQ69_spl
| powerset(sK11_skl) = sK11_skl ),
inference(forward_demodulation,[status(thm)],[f293,f1222]) ).
fof(f1229,plain,
( ~ sQ69_spl
| sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1228,f776]) ).
fof(f1230,plain,
( ~ sQ69_spl
| sQ48_spl ),
inference(contradiction_clause,[status(thm)],[f1229]) ).
fof(f1233,plain,
! [X0,X1] :
( empty(X1)
| element(X0,X1)
| ~ in(X0,sK12_skl(X1)) ),
inference(resolution,[status(thm)],[f147,f116]) ).
fof(f1248,plain,
! [X0] :
( ~ sQ23_spl
| in(ordered_pair(sK5_skl(X0,sK17_skl),sK4_skl(sK5_skl(X0,sK17_skl),relation_dom(sK17_skl),sK17_skl)),sK17_skl)
| ~ relation(sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(resolution,[status(thm)],[f568,f164]) ).
fof(f1261,definition,
! [X0] :
( sQ74_spl
<=> ( in(ordered_pair(sK5_skl(X0,sK17_skl),sK4_skl(sK5_skl(X0,sK17_skl),relation_dom(sK17_skl),sK17_skl)),sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1264,plain,
( ~ sQ23_spl
| ~ sQ22_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f1248,f1261,f563,f567]) ).
fof(f1377,plain,
! [X0,X1] :
( ~ in(X1,sK3_skl(sK11_skl,X1))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f1128,f49]) ).
fof(f1383,definition,
! [X0] :
( sQ76_spl
<=> ~ in(X0,powerset(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1384,plain,
! [X0] :
( ~ sQ76_spl
| ~ in(X0,powerset(sK11_skl)) ),
inference(component_clause,[status(thm)],[f1383]) ).
fof(f1394,plain,
( ~ sQ76_spl
| $false ),
inference(resolution,[status(thm)],[f1384,f1087]) ).
fof(f1403,plain,
~ sQ76_spl,
inference(contradiction_clause,[status(thm)],[f1394]) ).
fof(f1461,plain,
! [X0,X1] :
( ~ empty(X0)
| in(X0,powerset(X1)) ),
inference(resolution,[status(thm)],[f500,f155]) ).
fof(f1464,definition,
( sQ77_spl
<=> in(powerset(sK11_skl),powerset(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1465,plain,
( ~ sQ77_spl
| in(powerset(sK11_skl),powerset(sK11_skl)) ),
inference(component_clause,[status(thm)],[f1464]) ).
fof(f1469,plain,
! [X0,X1] :
( ~ empty(X0)
| in(relation_rng(X0),powerset(X1)) ),
inference(resolution,[status(thm)],[f1461,f109]) ).
fof(f1475,plain,
! [X0,X1] :
( ~ empty(powerset(X1))
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1469,f155]) ).
fof(f1477,plain,
! [X0] :
( ~ empty(sK11_skl)
| in(sK11_skl,powerset(X0)) ),
inference(paramodulation,[status(thm)],[f270,f1469]) ).
fof(f1480,definition,
! [X0] :
( sQ78_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1481,plain,
! [X0] :
( ~ sQ78_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f1480]) ).
fof(f1483,definition,
! [X1] :
( sQ79_spl
<=> ~ empty(powerset(X1)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1486,plain,
( sQ79_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f1475,f1480,f1483]) ).
fof(f1487,definition,
! [X0] :
( sQ80_spl
<=> in(sK11_skl,powerset(X0)) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1490,plain,
( ~ sQ14_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f1477,f1487,f286]) ).
fof(f1497,plain,
( ~ sQ78_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f112,f1481]) ).
fof(f1506,plain,
~ sQ78_spl,
inference(contradiction_clause,[status(thm)],[f1497]) ).
fof(f1520,plain,
! [X0] :
( in(sK8_skl(X0,sK17_skl),relation_rng(sK17_skl))
| ~ relation(sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f873,f167]) ).
fof(f1521,plain,
! [X0] :
( in(sK9_skl(X0,sK17_skl),relation_dom(sK17_skl))
| ~ relation(sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f873,f165]) ).
fof(f1522,plain,
! [X0,X1] :
( ~ in(sK9_skl(X0,sK17_skl),X1)
| in(sK8_skl(X0,sK17_skl),relation_image(sK17_skl,X1))
| ~ relation(sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f873,f163]) ).
fof(f1524,definition,
! [X0] :
( sQ82_spl
<=> ( in(sK8_skl(X0,sK17_skl),relation_rng(sK17_skl))
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1525,plain,
! [X0] :
( ~ sQ82_spl
| in(sK8_skl(X0,sK17_skl),relation_rng(sK17_skl))
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(component_clause,[status(thm)],[f1524]) ).
fof(f1527,plain,
( ~ sQ22_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f1520,f1524,f563]) ).
fof(f1528,definition,
! [X0] :
( sQ83_spl
<=> ( in(sK9_skl(X0,sK17_skl),relation_dom(sK17_skl))
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1529,plain,
! [X0] :
( ~ sQ83_spl
| in(sK9_skl(X0,sK17_skl),relation_dom(sK17_skl))
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(component_clause,[status(thm)],[f1528]) ).
fof(f1531,plain,
( ~ sQ22_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f1521,f1528,f563]) ).
fof(f1532,definition,
! [X0,X1] :
( sQ84_spl
<=> ( ~ in(sK9_skl(X0,sK17_skl),X1)
| in(sK8_skl(X0,sK17_skl),relation_image(sK17_skl,X1))
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1533,plain,
! [X0,X1] :
( ~ sQ84_spl
| ~ in(sK9_skl(X0,sK17_skl),X1)
| in(sK8_skl(X0,sK17_skl),relation_image(sK17_skl,X1))
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(component_clause,[status(thm)],[f1532]) ).
fof(f1535,plain,
( ~ sQ22_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1522,f1532,f563]) ).
fof(f1536,plain,
! [X0] :
( ~ sQ23_spl
| ~ sQ24_spl
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl)
| in(sK6_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)))
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(resolution,[status(thm)],[f572,f568]) ).
fof(f1538,plain,
! [X0] :
( ~ sQ23_spl
| ~ sQ24_spl
| in(sK6_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)))
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1536]) ).
fof(f1601,plain,
! [X0] :
( ~ sQ82_spl
| in(ordered_pair(sK7_skl(sK8_skl(X0,sK17_skl),relation_rng(sK17_skl),sK17_skl),sK8_skl(X0,sK17_skl)),sK17_skl)
| ~ relation(sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f1525,f166]) ).
fof(f1613,definition,
! [X0] :
( sQ88_spl
<=> ( in(ordered_pair(sK7_skl(sK8_skl(X0,sK17_skl),relation_rng(sK17_skl),sK17_skl),sK8_skl(X0,sK17_skl)),sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1616,plain,
( ~ sQ82_spl
| ~ sQ22_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f1601,f1613,f563,f1524]) ).
fof(f1627,plain,
! [X0] :
( ~ sQ83_spl
| in(ordered_pair(sK9_skl(X0,sK17_skl),sK4_skl(sK9_skl(X0,sK17_skl),relation_dom(sK17_skl),sK17_skl)),sK17_skl)
| ~ relation(sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f1529,f164]) ).
fof(f1629,definition,
! [X0] :
( sQ90_spl
<=> ( in(ordered_pair(sK9_skl(X0,sK17_skl),sK4_skl(sK9_skl(X0,sK17_skl),relation_dom(sK17_skl),sK17_skl)),sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1632,plain,
( ~ sQ83_spl
| ~ sQ22_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f1627,f1629,f563,f1528]) ).
fof(f1708,plain,
! [X0] :
( ~ sQ23_spl
| ~ sQ24_spl
| in(sK0_skl(sK6_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),relation_dom(sK17_skl))
| ~ relation(sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(resolution,[status(thm)],[f1538,f162]) ).
fof(f1709,plain,
! [X0] :
( ~ sQ23_spl
| ~ sQ24_spl
| in(ordered_pair(sK0_skl(sK6_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),sK6_skl(X0,sK17_skl)),sK17_skl)
| ~ relation(sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ),
inference(resolution,[status(thm)],[f1538,f161]) ).
fof(f1712,definition,
! [X0] :
( sQ91_spl
<=> ( in(sK0_skl(sK6_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),relation_dom(sK17_skl))
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1715,plain,
( ~ sQ23_spl
| ~ sQ24_spl
| ~ sQ22_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f1708,f1712,f563,f571,f567]) ).
fof(f1716,definition,
! [X0] :
( sQ92_spl
<=> ( in(ordered_pair(sK0_skl(sK6_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),sK6_skl(X0,sK17_skl)),sK17_skl)
| in(sK5_skl(X0,sK17_skl),X0)
| X0 = relation_dom(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1719,plain,
( ~ sQ23_spl
| ~ sQ24_spl
| ~ sQ22_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f1709,f1716,f563,f571,f567]) ).
fof(f1743,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ84_spl
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl)
| in(sK8_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)))
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f1533,f1529]) ).
fof(f1745,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ84_spl
| in(sK8_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)))
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1743]) ).
fof(f1755,plain,
( ~ sQ13_spl
| ~ relation(sK11_skl)
| in(sK11_skl,powerset(relation_rng(sK11_skl))) ),
inference(paramodulation,[status(thm)],[f522,f499]) ).
fof(f1756,plain,
! [X0] :
( ~ relation(sK11_skl)
| in(relation_image(sK11_skl,X0),powerset(sK11_skl)) ),
inference(paramodulation,[status(thm)],[f270,f499]) ).
fof(f1757,definition,
( sQ96_spl
<=> in(sK11_skl,powerset(relation_rng(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1760,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f1755,f1757,f279,f282]) ).
fof(f1761,definition,
! [X0] :
( sQ97_spl
<=> in(relation_image(sK11_skl,X0),powerset(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1764,plain,
( ~ sQ12_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f1756,f1761,f279]) ).
fof(f1790,plain,
! [X0,X1] :
( ~ empty(sK11_skl)
| ~ relation(sK11_skl)
| ~ element(X1,powerset(sK11_skl))
| ~ in(X0,X1) ),
inference(paramodulation,[status(thm)],[f293,f1111]) ).
fof(f1791,definition,
! [X0,X1] :
( sQ98_spl
<=> ( ~ element(X1,powerset(sK11_skl))
| ~ in(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1794,plain,
( ~ sQ14_spl
| ~ sQ12_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1790,f1791,f279,f286]) ).
fof(f1815,plain,
( sQ52_spl
| empty(powerset(sK11_skl))
| ~ in(powerset(sK11_skl),sK12_skl(powerset(sK11_skl))) ),
inference(resolution,[status(thm)],[f1233,f839]) ).
fof(f1816,plain,
! [X0,X1] :
( ~ in(X1,X0)
| empty(powerset(sK11_skl))
| ~ in(X0,sK12_skl(powerset(sK11_skl))) ),
inference(resolution,[status(thm)],[f1233,f1107]) ).
fof(f1817,plain,
! [X0] :
( X0 = sK11_skl
| empty(powerset(sK11_skl))
| ~ in(X0,sK12_skl(powerset(sK11_skl))) ),
inference(resolution,[status(thm)],[f1233,f524]) ).
fof(f1821,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| empty(X1)
| ~ in(X0,sK12_skl(X1)) ),
inference(resolution,[status(thm)],[f1233,f140]) ).
fof(f1822,definition,
( sQ99_spl
<=> in(powerset(sK11_skl),sK12_skl(powerset(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1825,plain,
( sQ52_spl
| sQ44_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f1815,f1822,f742,f822]) ).
fof(f1826,definition,
! [X0,X1] :
( sQ100_spl
<=> ( ~ in(X1,X0)
| ~ in(X0,sK12_skl(powerset(sK11_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1829,plain,
( sQ44_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f1816,f1826,f742]) ).
fof(f1830,definition,
! [X0] :
( sQ101_spl
<=> ( X0 = sK11_skl
| ~ in(X0,sK12_skl(powerset(sK11_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1831,plain,
! [X0] :
( ~ sQ101_spl
| X0 = sK11_skl
| ~ in(X0,sK12_skl(powerset(sK11_skl))) ),
inference(component_clause,[status(thm)],[f1830]) ).
fof(f1833,plain,
( sQ44_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f1817,f1830,f742]) ).
fof(f1837,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ in(X0,sK12_skl(X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f1821]) ).
fof(f1838,plain,
( ~ sQ101_spl
| empty(sK12_skl(powerset(sK11_skl)))
| sK10_skl(sK12_skl(powerset(sK11_skl))) = sK11_skl ),
inference(resolution,[status(thm)],[f1831,f486]) ).
fof(f1839,plain,
( ~ sQ101_spl
| sK12_skl(powerset(sK11_skl)) = sK11_skl
| sK5_skl(sK12_skl(powerset(sK11_skl)),sK11_skl) = sK11_skl ),
inference(resolution,[status(thm)],[f1831,f1122]) ).
fof(f1840,plain,
( ~ sQ101_spl
| sK12_skl(powerset(sK11_skl)) = sK11_skl
| sK8_skl(sK12_skl(powerset(sK11_skl)),sK11_skl) = sK11_skl ),
inference(resolution,[status(thm)],[f1831,f1121]) ).
fof(f1841,plain,
! [X0] :
( ~ sQ101_spl
| ~ in(X0,sK12_skl(powerset(sK11_skl)))
| sK3_skl(sK11_skl,sK12_skl(powerset(sK11_skl))) = sK11_skl ),
inference(resolution,[status(thm)],[f1831,f1128]) ).
fof(f1846,definition,
( sQ102_spl
<=> sK10_skl(sK12_skl(powerset(sK11_skl))) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1847,plain,
( ~ sQ102_spl
| sK10_skl(sK12_skl(powerset(sK11_skl))) = sK11_skl ),
inference(component_clause,[status(thm)],[f1846]) ).
fof(f1849,definition,
( sQ103_spl
<=> empty(sK12_skl(powerset(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1850,plain,
( ~ sQ103_spl
| empty(sK12_skl(powerset(sK11_skl))) ),
inference(component_clause,[status(thm)],[f1849]) ).
fof(f1852,plain,
( ~ sQ101_spl
| sQ103_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f1838,f1846,f1849,f1830]) ).
fof(f1853,definition,
( sQ104_spl
<=> sK5_skl(sK12_skl(powerset(sK11_skl)),sK11_skl) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1854,plain,
( ~ sQ104_spl
| sK5_skl(sK12_skl(powerset(sK11_skl)),sK11_skl) = sK11_skl ),
inference(component_clause,[status(thm)],[f1853]) ).
fof(f1856,definition,
( sQ105_spl
<=> sK12_skl(powerset(sK11_skl)) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1857,plain,
( ~ sQ105_spl
| sK12_skl(powerset(sK11_skl)) = sK11_skl ),
inference(component_clause,[status(thm)],[f1856]) ).
fof(f1858,plain,
( sQ105_spl
| sK12_skl(powerset(sK11_skl)) != sK11_skl ),
inference(component_clause,[status(thm)],[f1856]) ).
fof(f1859,plain,
( ~ sQ101_spl
| sQ105_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f1839,f1853,f1856,f1830]) ).
fof(f1860,definition,
( sQ106_spl
<=> sK8_skl(sK12_skl(powerset(sK11_skl)),sK11_skl) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1861,plain,
( ~ sQ106_spl
| sK8_skl(sK12_skl(powerset(sK11_skl)),sK11_skl) = sK11_skl ),
inference(component_clause,[status(thm)],[f1860]) ).
fof(f1863,plain,
( ~ sQ101_spl
| sQ105_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f1840,f1860,f1856,f1830]) ).
fof(f1864,definition,
( sQ107_spl
<=> sK3_skl(sK11_skl,sK12_skl(powerset(sK11_skl))) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1865,plain,
( ~ sQ107_spl
| sK3_skl(sK11_skl,sK12_skl(powerset(sK11_skl))) = sK11_skl ),
inference(component_clause,[status(thm)],[f1864]) ).
fof(f1867,definition,
! [X0] :
( sQ108_spl
<=> ~ in(X0,sK12_skl(powerset(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1868,plain,
! [X0] :
( ~ sQ108_spl
| ~ in(X0,sK12_skl(powerset(sK11_skl))) ),
inference(component_clause,[status(thm)],[f1867]) ).
fof(f1870,plain,
( ~ sQ101_spl
| sQ108_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f1841,f1864,f1867,f1830]) ).
fof(f1897,plain,
( ~ sQ105_spl
| ~ empty(sK11_skl)
| empty(powerset(sK11_skl)) ),
inference(paramodulation,[status(thm)],[f1857,f117]) ).
fof(f1915,plain,
( ~ sQ105_spl
| ~ sQ14_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1897,f742,f286,f1856]) ).
fof(f1920,plain,
( ~ sQ102_spl
| in(sK11_skl,sK12_skl(powerset(sK11_skl)))
| empty(sK12_skl(powerset(sK11_skl))) ),
inference(paramodulation,[status(thm)],[f1847,f486]) ).
fof(f1923,definition,
( sQ114_spl
<=> in(sK11_skl,sK12_skl(powerset(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1924,plain,
( ~ sQ114_spl
| in(sK11_skl,sK12_skl(powerset(sK11_skl))) ),
inference(component_clause,[status(thm)],[f1923]) ).
fof(f1926,plain,
( ~ sQ102_spl
| sQ114_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f1920,f1849,f1923,f1846]) ).
fof(f1927,definition,
( sQ115_spl
<=> in(sK12_skl(powerset(sK11_skl)),sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1960,plain,
( ~ sQ103_spl
| sK12_skl(powerset(sK11_skl)) = sK11_skl ),
inference(resolution,[status(thm)],[f1850,f235]) ).
fof(f1986,plain,
( ~ sQ103_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f1960,f1856,f1849]) ).
fof(f2033,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ84_spl
| ~ in(ordered_pair(X0,sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl)),sK17_skl)
| relation_image(sK17_skl,relation_dom(sK17_skl)) = relation_rng(sK17_skl)
| ~ relation(sK17_skl)
| in(sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)))
| relation_image(sK17_skl,relation_dom(sK17_skl)) = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f1745,f89]) ).
fof(f2035,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ84_spl
| in(sK0_skl(sK8_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),relation_dom(sK17_skl))
| ~ relation(sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f1745,f162]) ).
fof(f2036,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ84_spl
| in(ordered_pair(sK0_skl(sK8_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),sK8_skl(X0,sK17_skl)),sK17_skl)
| ~ relation(sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f1745,f161]) ).
fof(f2038,definition,
( sQ117_spl
<=> relation_image(sK17_skl,relation_dom(sK17_skl)) = relation_rng(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f2039,plain,
( ~ sQ117_spl
| relation_image(sK17_skl,relation_dom(sK17_skl)) = relation_rng(sK17_skl) ),
inference(component_clause,[status(thm)],[f2038]) ).
fof(f2041,definition,
( sQ118_spl
<=> in(sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl))) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f2042,plain,
( ~ sQ118_spl
| in(sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl))) ),
inference(component_clause,[status(thm)],[f2041]) ).
fof(f2044,definition,
! [X0] :
( sQ119_spl
<=> ~ in(ordered_pair(X0,sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl)),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f2045,plain,
! [X0] :
( ~ sQ119_spl
| ~ in(ordered_pair(X0,sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl)),sK17_skl) ),
inference(component_clause,[status(thm)],[f2044]) ).
fof(f2047,plain,
( ~ sQ83_spl
| ~ sQ84_spl
| sQ119_spl
| ~ sQ22_spl
| sQ118_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f2033,f2038,f2041,f563,f2044,f1532,f1528]) ).
fof(f2049,definition,
! [X0] :
( sQ120_spl
<=> ( in(sK0_skl(sK8_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),relation_dom(sK17_skl))
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f2052,plain,
( ~ sQ83_spl
| ~ sQ84_spl
| ~ sQ22_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f2035,f2049,f563,f1532,f1528]) ).
fof(f2053,definition,
! [X0] :
( sQ121_spl
<=> ( in(ordered_pair(sK0_skl(sK8_skl(X0,sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),sK8_skl(X0,sK17_skl)),sK17_skl)
| in(sK8_skl(X0,sK17_skl),X0)
| X0 = relation_rng(sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f2056,plain,
( ~ sQ83_spl
| ~ sQ84_spl
| ~ sQ22_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f2036,f2053,f563,f1532,f1528]) ).
fof(f2057,plain,
( ~ sQ77_spl
| sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1465,f858]) ).
fof(f2058,plain,
( ~ sQ77_spl
| sQ52_spl ),
inference(contradiction_clause,[status(thm)],[f2057]) ).
fof(f2059,plain,
( ~ sQ119_spl
| in(sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)))
| relation_image(sK17_skl,relation_dom(sK17_skl)) = relation_rng(sK17_skl) ),
inference(resolution,[status(thm)],[f2045,f873]) ).
fof(f2060,plain,
( ~ sQ119_spl
| sQ118_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f2059,f2038,f2041,f2044]) ).
fof(f2068,plain,
! [X0] :
( ~ sQ104_spl
| ~ in(ordered_pair(sK5_skl(sK12_skl(powerset(sK11_skl)),sK11_skl),X0),sK11_skl)
| ~ in(sK11_skl,sK12_skl(powerset(sK11_skl)))
| sK12_skl(powerset(sK11_skl)) = relation_dom(sK11_skl)
| ~ relation(sK11_skl) ),
inference(paramodulation,[status(thm)],[f1854,f81]) ).
fof(f2071,definition,
( sQ122_spl
<=> sK12_skl(powerset(sK11_skl)) = relation_dom(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f2072,plain,
( ~ sQ122_spl
| sK12_skl(powerset(sK11_skl)) = relation_dom(sK11_skl) ),
inference(component_clause,[status(thm)],[f2071]) ).
fof(f2074,definition,
! [X0] :
( sQ123_spl
<=> ~ in(ordered_pair(sK5_skl(sK12_skl(powerset(sK11_skl)),sK11_skl),X0),sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f2077,plain,
( ~ sQ104_spl
| sQ123_spl
| ~ sQ114_spl
| sQ122_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f2068,f279,f2071,f1923,f2074,f1853]) ).
fof(f2078,plain,
( ~ sQ122_spl
| sK12_skl(powerset(sK11_skl)) = sK11_skl ),
inference(forward_demodulation,[status(thm)],[f293,f2072]) ).
fof(f2079,plain,
( ~ sQ122_spl
| sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2078,f1858]) ).
fof(f2080,plain,
( ~ sQ122_spl
| sQ105_spl ),
inference(contradiction_clause,[status(thm)],[f2079]) ).
fof(f2085,plain,
! [X0] :
( ~ sQ106_spl
| ~ in(ordered_pair(X0,sK8_skl(sK12_skl(powerset(sK11_skl)),sK11_skl)),sK11_skl)
| ~ in(sK11_skl,sK12_skl(powerset(sK11_skl)))
| sK12_skl(powerset(sK11_skl)) = relation_rng(sK11_skl)
| ~ relation(sK11_skl) ),
inference(paramodulation,[status(thm)],[f1861,f89]) ).
fof(f2088,definition,
( sQ124_spl
<=> sK12_skl(powerset(sK11_skl)) = relation_rng(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f2089,plain,
( ~ sQ124_spl
| sK12_skl(powerset(sK11_skl)) = relation_rng(sK11_skl) ),
inference(component_clause,[status(thm)],[f2088]) ).
fof(f2091,definition,
! [X0] :
( sQ125_spl
<=> ~ in(ordered_pair(X0,sK8_skl(sK12_skl(powerset(sK11_skl)),sK11_skl)),sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f2094,plain,
( ~ sQ106_spl
| sQ125_spl
| ~ sQ114_spl
| sQ124_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f2085,f279,f2088,f1923,f2091,f1860]) ).
fof(f2095,plain,
( ~ sQ124_spl
| sK12_skl(powerset(sK11_skl)) = sK11_skl ),
inference(forward_demodulation,[status(thm)],[f270,f2089]) ).
fof(f2096,plain,
( ~ sQ124_spl
| sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2095,f1858]) ).
fof(f2097,plain,
( ~ sQ124_spl
| sQ105_spl ),
inference(contradiction_clause,[status(thm)],[f2096]) ).
fof(f2138,plain,
! [X0] :
( ~ sQ107_spl
| ~ in(sK12_skl(powerset(sK11_skl)),sK11_skl)
| ~ in(X0,sK12_skl(powerset(sK11_skl))) ),
inference(paramodulation,[status(thm)],[f1865,f1377]) ).
fof(f2145,plain,
( ~ sQ107_spl
| ~ sQ115_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f2138,f1867,f1927,f1864]) ).
fof(f2149,definition,
( sQ126_spl
<=> in(sK12_skl(powerset(sK11_skl)),powerset(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f2150,plain,
( ~ sQ126_spl
| in(sK12_skl(powerset(sK11_skl)),powerset(sK11_skl)) ),
inference(component_clause,[status(thm)],[f2149]) ).
fof(f2158,plain,
( ~ sQ114_spl
| ~ sQ108_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1924,f1868]) ).
fof(f2159,plain,
( ~ sQ114_spl
| ~ sQ108_spl ),
inference(contradiction_clause,[status(thm)],[f2158]) ).
fof(f2162,plain,
( ~ sQ126_spl
| sK12_skl(powerset(sK11_skl)) = sK11_skl ),
inference(resolution,[status(thm)],[f2150,f734]) ).
fof(f2165,plain,
( ~ sQ126_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f2162,f1856,f2149]) ).
fof(f2182,plain,
! [X0] :
( empty(sK12_skl(X0))
| in(sK10_skl(sK12_skl(X0)),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f1837,f486]) ).
fof(f2191,plain,
! [X0] :
( in(sK10_skl(sK12_skl(X0)),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2182,f117]) ).
fof(f2193,plain,
( ~ sQ101_spl
| sK10_skl(sK12_skl(sK12_skl(powerset(sK11_skl)))) = sK11_skl
| empty(sK12_skl(powerset(sK11_skl))) ),
inference(resolution,[status(thm)],[f2191,f1831]) ).
fof(f2195,plain,
! [X0] :
( ~ in(X0,sK10_skl(sK12_skl(powerset(sK11_skl))))
| empty(powerset(sK11_skl)) ),
inference(resolution,[status(thm)],[f2191,f1116]) ).
fof(f2205,definition,
( sQ128_spl
<=> sK10_skl(sK12_skl(sK12_skl(powerset(sK11_skl)))) = sK11_skl ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f2206,plain,
( ~ sQ128_spl
| sK10_skl(sK12_skl(sK12_skl(powerset(sK11_skl)))) = sK11_skl ),
inference(component_clause,[status(thm)],[f2205]) ).
fof(f2208,plain,
( ~ sQ101_spl
| sQ128_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f2193,f1849,f2205,f1830]) ).
fof(f2210,definition,
! [X0] :
( sQ129_spl
<=> ~ in(X0,sK10_skl(sK12_skl(powerset(sK11_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f2213,plain,
( sQ129_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f2195,f742,f2210]) ).
fof(f2221,plain,
( ~ sQ128_spl
| in(sK11_skl,sK12_skl(sK12_skl(powerset(sK11_skl))))
| empty(sK12_skl(sK12_skl(powerset(sK11_skl)))) ),
inference(paramodulation,[status(thm)],[f2206,f486]) ).
fof(f2222,plain,
( ~ sQ128_spl
| ~ in(sK12_skl(sK12_skl(powerset(sK11_skl))),sK11_skl)
| empty(sK12_skl(sK12_skl(powerset(sK11_skl)))) ),
inference(paramodulation,[status(thm)],[f2206,f497]) ).
fof(f2226,definition,
( sQ130_spl
<=> empty(sK12_skl(sK12_skl(powerset(sK11_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f2227,plain,
( ~ sQ130_spl
| empty(sK12_skl(sK12_skl(powerset(sK11_skl)))) ),
inference(component_clause,[status(thm)],[f2226]) ).
fof(f2229,definition,
( sQ131_spl
<=> in(sK11_skl,sK12_skl(sK12_skl(powerset(sK11_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f2232,plain,
( ~ sQ128_spl
| sQ131_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f2221,f2226,f2229,f2205]) ).
fof(f2233,definition,
( sQ132_spl
<=> in(sK12_skl(sK12_skl(powerset(sK11_skl))),sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f2236,plain,
( ~ sQ128_spl
| ~ sQ132_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f2222,f2226,f2233,f2205]) ).
fof(f2237,plain,
( ~ sQ130_spl
| empty(sK12_skl(powerset(sK11_skl))) ),
inference(resolution,[status(thm)],[f2227,f117]) ).
fof(f2284,plain,
( ~ sQ130_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f2237,f1849,f2226]) ).
fof(f2402,plain,
! [X0] :
( ~ sQ118_spl
| ~ in(ordered_pair(X0,sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl)),sK17_skl)
| relation_image(sK17_skl,relation_dom(sK17_skl)) = relation_rng(sK17_skl)
| ~ relation(sK17_skl) ),
inference(resolution,[status(thm)],[f2042,f89]) ).
fof(f2405,plain,
( ~ sQ118_spl
| in(ordered_pair(sK0_skl(sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl)),sK17_skl)
| ~ relation(sK17_skl) ),
inference(resolution,[status(thm)],[f2042,f161]) ).
fof(f2407,plain,
( ~ sQ118_spl
| sQ119_spl
| sQ117_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f2402,f563,f2038,f2044,f2041]) ).
fof(f2416,definition,
( sQ137_spl
<=> in(ordered_pair(sK0_skl(sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl)),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f2417,plain,
( ~ sQ137_spl
| in(ordered_pair(sK0_skl(sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl),relation_image(sK17_skl,relation_dom(sK17_skl)),relation_dom(sK17_skl),sK17_skl),sK8_skl(relation_image(sK17_skl,relation_dom(sK17_skl)),sK17_skl)),sK17_skl) ),
inference(component_clause,[status(thm)],[f2416]) ).
fof(f2419,plain,
( ~ sQ118_spl
| sQ137_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f2405,f563,f2416,f2041]) ).
fof(f2420,plain,
( ~ sQ117_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2039,f136]) ).
fof(f2421,plain,
~ sQ117_spl,
inference(contradiction_clause,[status(thm)],[f2420]) ).
fof(f2422,plain,
( ~ sQ137_spl
| ~ sQ119_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2417,f2045]) ).
fof(f2423,plain,
( ~ sQ137_spl
| ~ sQ119_spl ),
inference(contradiction_clause,[status(thm)],[f2422]) ).
fof(f2424,plain,
$false,
inference(sat_refutation,[status(thm)],[f180,f184,f186,f285,f289,f292,f334,f471,f479,f545,f566,f570,f574,f583,f651,f655,f659,f703,f719,f748,f752,f754,f765,f780,f813,f828,f833,f867,f883,f1082,f1142,f1148,f1165,f1169,f1173,f1186,f1189,f1206,f1210,f1214,f1227,f1230,f1264,f1403,f1486,f1490,f1506,f1527,f1531,f1535,f1616,f1632,f1715,f1719,f1760,f1764,f1794,f1825,f1829,f1833,f1852,f1859,f1863,f1870,f1915,f1926,f1986,f2047,f2052,f2056,f2058,f2060,f2077,f2080,f2094,f2097,f2145,f2159,f2165,f2208,f2213,f2232,f2236,f2284,f2407,f2419,f2421,f2423]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU206+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/5.52 % Computer : n012.cluster.edu
% 0.03/5.52 % Model : x86_64 x86_64
% 0.03/5.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/5.52 % Memory : 8046.5625MB
% 0.03/5.52 % OS : Linux 6.8.0-71-generic
% 0.03/5.52 % CPULimit : 300
% 0.03/5.52 % WCLimit : 300
% 0.03/5.52 % DateTime : Mon Sep 21 05:57:29 UTC 2026
% 0.03/5.52 % CPUTime :
% 0.03/5.53 % Drodi V4.1.1
% 0.07/5.74 % Refutation found
% 0.07/5.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.07/5.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.07/5.77 % Elapsed time: 0.234998 seconds
% 0.07/5.77 % CPU time: 1.705527 seconds
% 0.07/5.77 % Total memory used: 148.399 MB
% 0.07/5.77 % Net memory used: 141.022 MB
%------------------------------------------------------------------------------