%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET660+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:10:23 PM UTC 2026
% Result : Theorem 1.14s 0.60s
% Output : CNFRefutation 1.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 108
% Syntax : Number of formulae : 509 ( 30 unt; 82 def)
% Number of atoms : 1681 ( 181 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 1965 ( 793 ~; 899 |; 90 &)
% ( 109 <=>; 72 =>; 0 <=; 2 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 89 ( 87 usr; 83 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 7 con; 0-3 aty)
% Number of variables : 583 ( 553 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [B] :
( ilf_type(B,binary_relation_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( member(C,range_of(B))
<=> ? [D] :
( member(ordered_pair(D,C),B)
& ilf_type(D,set_type) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,binary_relation_type)
=> ( member(ordered_pair(B,C),D)
=> ( member(C,range_of(D))
& member(B,domain_of(D)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( ! [D] :
( ilf_type(D,set_type)
=> ( member(D,B)
<=> member(D,C) ) )
=> B = C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,set_type)
=> ! [F] :
( ilf_type(F,set_type)
=> ( F = ordered_pair(D,E)
<=> F = unordered_pair(unordered_pair(D,E),singleton(D)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( ! [E] :
( ilf_type(E,relation_type(B,C))
=> ilf_type(E,subset_type(cross_product(B,C))) )
& ! [D] :
( ilf_type(D,subset_type(cross_product(B,C)))
=> ilf_type(D,relation_type(B,C)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( B = C
<=> ( subset(C,B)
& subset(B,C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> unordered_pair(B,C) = unordered_pair(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( ilf_type(B,binary_relation_type)
<=> ( ilf_type(B,set_type)
& relation_like(B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
? [B] : ilf_type(B,binary_relation_type),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( ilf_type(C,subset_type(B))
<=> ilf_type(C,member_type(power_set(B))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( B = C
<=> ! [D] :
( ilf_type(D,set_type)
=> ( member(D,B)
<=> member(D,C) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( subset(B,C)
<=> ! [D] :
( ilf_type(D,set_type)
=> ( member(D,B)
=> member(D,C) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( member(B,power_set(C))
<=> ! [D] :
( ilf_type(D,set_type)
=> ( member(D,B)
=> member(D,C) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( ilf_type(power_set(B),set_type)
& ~ empty(power_set(B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ( ilf_type(C,set_type)
& ~ empty(C) )
=> ( ilf_type(B,member_type(C))
<=> member(B,C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [B] :
( ( ilf_type(B,set_type)
& ~ empty(B) )
=> ? [C] : ilf_type(C,member_type(B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( relation_like(B)
<=> ! [C] :
( ilf_type(C,set_type)
=> ( member(C,B)
=> ? [D] :
( ? [E] :
( C = ordered_pair(D,E)
& ilf_type(E,set_type) )
& ilf_type(D,set_type) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,subset_type(cross_product(B,C)))
=> relation_like(D) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( empty(B)
<=> ! [C] :
( ilf_type(C,set_type)
=> ~ member(C,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [B] :
( ( ilf_type(B,set_type)
& empty(B) )
=> relation_like(B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> domain(B,C,D) = domain_of(D) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ilf_type(domain(B,C,D),subset_type(B)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> range(B,C,D) = range_of(D) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ilf_type(range(B,C,D),subset_type(C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [B] : ilf_type(B,set_type),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,conjecture,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ( ! [E] :
( ilf_type(E,set_type)
=> ( member(E,C)
=> ? [F] :
( member(ordered_pair(F,E),D)
& ilf_type(F,set_type) ) ) )
<=> range(B,C,D) = C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
~ ! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ( ! [E] :
( ilf_type(E,set_type)
=> ( member(E,C)
=> ? [F] :
( member(ordered_pair(F,E),D)
& ilf_type(F,set_type) ) ) )
<=> range(B,C,D) = C ) ) ) ),
inference(negated_conjecture,[status(cth)],[f35]) ).
fof(f37,plain,
! [B] :
( ! [C] :
( ( member(C,range_of(B))
<=> ? [D] :
( member(ordered_pair(D,C),B)
& ilf_type(D,set_type) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,binary_relation_type) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f38,plain,
! [B] :
( ! [C] :
( ( ( ! [D] :
( ~ member(ordered_pair(D,C),B)
| ~ ilf_type(D,set_type) )
| member(C,range_of(B)) )
& ( ? [D] :
( member(ordered_pair(D,C),B)
& ilf_type(D,set_type) )
| ~ member(C,range_of(B)) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,binary_relation_type) ),
inference(NNF_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
! [B] :
( ! [C] :
( ( ( ! [D] :
( ~ member(ordered_pair(D,C),B)
| ~ ilf_type(D,set_type) )
| member(C,range_of(B)) )
& ( ( member(ordered_pair(sK0_skl(C,B),C),B)
& ilf_type(sK0_skl(C,B),set_type) )
| ~ member(C,range_of(B)) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,binary_relation_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(D,sK0_skl(C,B))],[f38]) ).
fof(f41,plain,
! [X0,X1] :
( member(ordered_pair(sK0_skl(X1,X0),X1),X0)
| ~ member(X1,range_of(X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,binary_relation_type) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f42,plain,
! [X0,X1,X2] :
( ~ member(ordered_pair(X2,X1),X0)
| ~ ilf_type(X2,set_type)
| member(X1,range_of(X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,binary_relation_type) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f45,plain,
! [B] :
( ! [C] :
( ! [D] :
( ( member(C,range_of(D))
& member(B,domain_of(D)) )
| ~ member(ordered_pair(B,C),D)
| ~ ilf_type(D,binary_relation_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f46,plain,
! [X0,X1,X2] :
( member(X0,domain_of(X2))
| ~ member(ordered_pair(X0,X1),X2)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f48,plain,
! [B] :
( ! [C] :
( B = C
| ? [D] :
( ( member(D,B)
<~> member(D,C) )
& ilf_type(D,set_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f49,plain,
! [B] :
( ! [C] :
( B = C
| ? [D] :
( ( ~ member(D,C)
| ~ member(D,B) )
& ( member(D,C)
| member(D,B) )
& ilf_type(D,set_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
! [B] :
( ! [C] :
( B = C
| ( ( ~ member(sK1_skl(C,B),C)
| ~ member(sK1_skl(C,B),B) )
& ( member(sK1_skl(C,B),C)
| member(sK1_skl(C,B),B) )
& ilf_type(sK1_skl(C,B),set_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(C,B))],[f49]) ).
fof(f52,plain,
! [X0,X1] :
( X0 = X1
| member(sK1_skl(X1,X0),X1)
| member(sK1_skl(X1,X0),X0)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f54,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( ( F = ordered_pair(D,E)
<=> F = unordered_pair(unordered_pair(D,E),singleton(D)) )
| ~ ilf_type(F,set_type) )
| ~ ilf_type(E,set_type) )
| ~ ilf_type(D,set_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f55,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( ( ( F != unordered_pair(unordered_pair(D,E),singleton(D))
| F = ordered_pair(D,E) )
& ( F = unordered_pair(unordered_pair(D,E),singleton(D))
| F != ordered_pair(D,E) ) )
| ~ ilf_type(F,set_type) )
| ~ ilf_type(E,set_type) )
| ~ ilf_type(D,set_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
( ! [D] :
( ! [E] :
( ! [F] :
( ( ( F != unordered_pair(unordered_pair(D,E),singleton(D))
| F = ordered_pair(D,E) )
& ( F = unordered_pair(unordered_pair(D,E),singleton(D))
| F != ordered_pair(D,E) ) )
| ~ ilf_type(F,set_type) )
| ~ ilf_type(E,set_type) )
| ~ ilf_type(D,set_type) )
| ! [C] : ~ ilf_type(C,set_type)
| ! [B] : ~ ilf_type(B,set_type) ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f57,plain,
! [X0,X1,X2,X3,X4] :
( X4 = unordered_pair(unordered_pair(X2,X3),singleton(X2))
| X4 != ordered_pair(X2,X3)
| ~ ilf_type(X4,set_type)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f58,plain,
! [X0,X1,X2,X3,X4] :
( X4 != unordered_pair(unordered_pair(X2,X3),singleton(X2))
| X4 = ordered_pair(X2,X3)
| ~ ilf_type(X4,set_type)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f61,plain,
! [B] :
( ! [C] :
( ( ! [E] :
( ilf_type(E,subset_type(cross_product(B,C)))
| ~ ilf_type(E,relation_type(B,C)) )
& ! [D] :
( ilf_type(D,relation_type(B,C))
| ~ ilf_type(D,subset_type(cross_product(B,C))) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ilf_type(X2,subset_type(cross_product(X0,X1)))
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f67,plain,
! [B] :
( ! [C] :
( ( B = C
<=> ( subset(C,B)
& subset(B,C) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f68,plain,
! [B] :
( ! [C] :
( ( ( ~ subset(C,B)
| ~ subset(B,C)
| B = C )
& ( ( subset(C,B)
& subset(B,C) )
| B != C ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f67]) ).
fof(f71,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f80,plain,
! [B] :
( ! [C] :
( unordered_pair(B,C) = unordered_pair(C,B)
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f81,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = unordered_pair(X1,X0)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f82,plain,
! [B] :
( ( ilf_type(B,binary_relation_type)
<=> ( ilf_type(B,set_type)
& relation_like(B) ) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f83,plain,
! [B] :
( ( ( ~ ilf_type(B,set_type)
| ~ relation_like(B)
| ilf_type(B,binary_relation_type) )
& ( ( ilf_type(B,set_type)
& relation_like(B) )
| ~ ilf_type(B,binary_relation_type) ) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f82]) ).
fof(f84,plain,
! [X0] :
( relation_like(X0)
| ~ ilf_type(X0,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f86,plain,
! [X0] :
( ~ ilf_type(X0,set_type)
| ~ relation_like(X0)
| ilf_type(X0,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f87,plain,
ilf_type(sK3_skl,binary_relation_type),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(B,sK3_skl)],[f16]) ).
fof(f88,plain,
ilf_type(sK3_skl,binary_relation_type),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f89,plain,
! [B] :
( ! [C] :
( ( ilf_type(C,subset_type(B))
<=> ilf_type(C,member_type(power_set(B))) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f90,plain,
! [B] :
( ! [C] :
( ( ( ~ ilf_type(C,member_type(power_set(B)))
| ilf_type(C,subset_type(B)) )
& ( ilf_type(C,member_type(power_set(B)))
| ~ ilf_type(C,subset_type(B)) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f89]) ).
fof(f91,plain,
! [X0,X1] :
( ilf_type(X1,member_type(power_set(X0)))
| ~ ilf_type(X1,subset_type(X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f96,plain,
! [B] :
( ! [C] :
( ( B = C
<=> ! [D] :
( ( member(D,B)
<=> member(D,C) )
| ~ ilf_type(D,set_type) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f97,plain,
! [B] :
( ! [C] :
( ( ( ? [D] :
( ( member(D,C)
| member(D,B) )
& ( ~ member(D,C)
| ~ member(D,B) )
& ilf_type(D,set_type) )
| B = C )
& ( ! [D] :
( ( ( ~ member(D,C)
| member(D,B) )
& ( member(D,C)
| ~ member(D,B) ) )
| ~ ilf_type(D,set_type) )
| B != C ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f96]) ).
fof(f98,plain,
! [B] :
( ! [C] :
( ( ( ( ( member(sK5_skl(C,B),C)
| member(sK5_skl(C,B),B) )
& ( ~ member(sK5_skl(C,B),C)
| ~ member(sK5_skl(C,B),B) )
& ilf_type(sK5_skl(C,B),set_type) )
| B = C )
& ( ! [D] :
( ( ( ~ member(D,C)
| member(D,B) )
& ( member(D,C)
| ~ member(D,B) ) )
| ~ ilf_type(D,set_type) )
| B != C ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(D,sK5_skl(C,B))],[f97]) ).
fof(f103,plain,
! [X0,X1] :
( member(sK5_skl(X1,X0),X1)
| member(sK5_skl(X1,X0),X0)
| X0 = X1
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f104,plain,
! [B] :
( ! [C] :
( ( subset(B,C)
<=> ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f105,plain,
! [B] :
( ! [C] :
( ( ( ? [D] :
( ~ member(D,C)
& member(D,B)
& ilf_type(D,set_type) )
| subset(B,C) )
& ( ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) )
| ~ subset(B,C) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f104]) ).
fof(f106,plain,
! [B] :
( ! [C] :
( ( ( ( ~ member(sK6_skl(C,B),C)
& member(sK6_skl(C,B),B)
& ilf_type(sK6_skl(C,B),set_type) )
| subset(B,C) )
& ( ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) )
| ~ subset(B,C) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(D,sK6_skl(C,B))],[f105]) ).
fof(f109,plain,
! [X0,X1] :
( member(sK6_skl(X1,X0),X0)
| subset(X0,X1)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f110,plain,
! [X0,X1] :
( ~ member(sK6_skl(X1,X0),X1)
| subset(X0,X1)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f113,plain,
! [B] :
( ! [C] :
( ( member(B,power_set(C))
<=> ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f114,plain,
! [B] :
( ! [C] :
( ( ( ? [D] :
( ~ member(D,C)
& member(D,B)
& ilf_type(D,set_type) )
| member(B,power_set(C)) )
& ( ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) )
| ~ member(B,power_set(C)) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [B] :
( ! [C] :
( ( ( ( ~ member(sK7_skl(C,B),C)
& member(sK7_skl(C,B),B)
& ilf_type(sK7_skl(C,B),set_type) )
| member(B,power_set(C)) )
& ( ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) )
| ~ member(B,power_set(C)) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(D,sK7_skl(C,B))],[f114]) ).
fof(f116,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ ilf_type(X2,set_type)
| ~ member(X0,power_set(X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f120,plain,
! [B] :
( ( ilf_type(power_set(B),set_type)
& ~ empty(power_set(B)) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f121,plain,
! [X0] :
( ~ empty(power_set(X0))
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f123,plain,
! [B] :
( ! [C] :
( ( ilf_type(B,member_type(C))
<=> member(B,C) )
| ~ ilf_type(C,set_type)
| empty(C) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f124,plain,
! [B] :
( ! [C] :
( ( ( ~ member(B,C)
| ilf_type(B,member_type(C)) )
& ( member(B,C)
| ~ ilf_type(B,member_type(C)) ) )
| ~ ilf_type(C,set_type)
| empty(C) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [X0,X1] :
( member(X0,X1)
| ~ ilf_type(X0,member_type(X1))
| ~ ilf_type(X1,set_type)
| empty(X1)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f127,plain,
! [B] :
( ? [C] : ilf_type(C,member_type(B))
| ~ ilf_type(B,set_type)
| empty(B) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f128,plain,
! [B] :
( ilf_type(sK8_skl(B),member_type(B))
| ~ ilf_type(B,set_type)
| empty(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(C,sK8_skl(B))],[f127]) ).
fof(f129,plain,
! [X0] :
( ilf_type(sK8_skl(X0),member_type(X0))
| ~ ilf_type(X0,set_type)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [B] :
( ( relation_like(B)
<=> ! [C] :
( ? [D] :
( ? [E] :
( C = ordered_pair(D,E)
& ilf_type(E,set_type) )
& ilf_type(D,set_type) )
| ~ member(C,B)
| ~ ilf_type(C,set_type) ) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f131,plain,
! [B] :
( ( ( ? [C] :
( ! [D] :
( ! [E] :
( C != ordered_pair(D,E)
| ~ ilf_type(E,set_type) )
| ~ ilf_type(D,set_type) )
& member(C,B)
& ilf_type(C,set_type) )
| relation_like(B) )
& ( ! [C] :
( ? [D] :
( ? [E] :
( C = ordered_pair(D,E)
& ilf_type(E,set_type) )
& ilf_type(D,set_type) )
| ~ member(C,B)
| ~ ilf_type(C,set_type) )
| ~ relation_like(B) ) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f130]) ).
fof(f132,plain,
! [B] :
( ( ( ( ! [D] :
( ! [E] :
( sK11_skl(B) != ordered_pair(D,E)
| ~ ilf_type(E,set_type) )
| ~ ilf_type(D,set_type) )
& member(sK11_skl(B),B)
& ilf_type(sK11_skl(B),set_type) )
| relation_like(B) )
& ( ! [C] :
( ( C = ordered_pair(sK9_skl(C,B),sK10_skl(C,B))
& ilf_type(sK10_skl(C,B),set_type)
& ilf_type(sK9_skl(C,B),set_type) )
| ~ member(C,B)
| ~ ilf_type(C,set_type) )
| ~ relation_like(B) ) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl]),skolemize(D,sK9_skl(C,B)),skolemize(E,sK10_skl(C,B)),skolemize(C,sK11_skl(B))],[f131]) ).
fof(f135,plain,
! [X0,X1] :
( X1 = ordered_pair(sK9_skl(X1,X0),sK10_skl(X1,X0))
| ~ member(X1,X0)
| ~ ilf_type(X1,set_type)
| ~ relation_like(X0)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f137,plain,
! [X0] :
( member(sK11_skl(X0),X0)
| relation_like(X0)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f138,plain,
! [X0,X1,X2] :
( sK11_skl(X0) != ordered_pair(X1,X2)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| relation_like(X0)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f139,plain,
! [B] :
( ! [C] :
( ! [D] :
( relation_like(D)
| ~ ilf_type(D,subset_type(cross_product(B,C))) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f140,plain,
! [X0,X1,X2] :
( relation_like(X2)
| ~ ilf_type(X2,subset_type(cross_product(X0,X1)))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f141,plain,
! [B] :
( ( empty(B)
<=> ! [C] :
( ~ member(C,B)
| ~ ilf_type(C,set_type) ) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f142,plain,
! [B] :
( ( ( ? [C] :
( member(C,B)
& ilf_type(C,set_type) )
| empty(B) )
& ( ! [C] :
( ~ member(C,B)
| ~ ilf_type(C,set_type) )
| ~ empty(B) ) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f141]) ).
fof(f143,plain,
! [B] :
( ( ( ( member(sK12_skl(B),B)
& ilf_type(sK12_skl(B),set_type) )
| empty(B) )
& ( ! [C] :
( ~ member(C,B)
| ~ ilf_type(C,set_type) )
| ~ empty(B) ) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(C,sK12_skl(B))],[f142]) ).
fof(f144,plain,
! [X0,X1] :
( ~ member(X1,X0)
| ~ ilf_type(X1,set_type)
| ~ empty(X0)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f146,plain,
! [X0] :
( member(sK12_skl(X0),X0)
| empty(X0)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f147,plain,
! [B] :
( relation_like(B)
| ~ ilf_type(B,set_type)
| ~ empty(B) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f148,plain,
! [X0] :
( relation_like(X0)
| ~ ilf_type(X0,set_type)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f149,plain,
! [B] :
( ! [C] :
( ! [D] :
( domain(B,C,D) = domain_of(D)
| ~ ilf_type(D,relation_type(B,C)) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f150,plain,
! [X0,X1,X2] :
( domain(X0,X1,X2) = domain_of(X2)
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f151,plain,
! [B] :
( ! [C] :
( ! [D] :
( ilf_type(domain(B,C,D),subset_type(B))
| ~ ilf_type(D,relation_type(B,C)) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f152,plain,
! [X0,X1,X2] :
( ilf_type(domain(X0,X1,X2),subset_type(X0))
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
! [B] :
( ! [C] :
( ! [D] :
( range(B,C,D) = range_of(D)
| ~ ilf_type(D,relation_type(B,C)) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f154,plain,
! [X0,X1,X2] :
( range(X0,X1,X2) = range_of(X2)
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f155,plain,
! [B] :
( ! [C] :
( ! [D] :
( ilf_type(range(B,C,D),subset_type(C))
| ~ ilf_type(D,relation_type(B,C)) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f156,plain,
! [X0,X1,X2] :
( ilf_type(range(X0,X1,X2),subset_type(X1))
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f157,plain,
! [X0] : ilf_type(X0,set_type),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f158,plain,
? [B] :
( ? [C] :
( ? [D] :
( ( ! [E] :
( ? [F] :
( member(ordered_pair(F,E),D)
& ilf_type(F,set_type) )
| ~ member(E,C)
| ~ ilf_type(E,set_type) )
<~> range(B,C,D) = C )
& ilf_type(D,relation_type(B,C)) )
& ilf_type(C,set_type) )
& ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f159,plain,
? [B] :
( ? [C] :
( ? [D] :
( ( range(B,C,D) != C
| ? [E] :
( ! [F] :
( ~ member(ordered_pair(F,E),D)
| ~ ilf_type(F,set_type) )
& member(E,C)
& ilf_type(E,set_type) ) )
& ( range(B,C,D) = C
| ! [E] :
( ? [F] :
( member(ordered_pair(F,E),D)
& ilf_type(F,set_type) )
| ~ member(E,C)
| ~ ilf_type(E,set_type) ) )
& ilf_type(D,relation_type(B,C)) )
& ilf_type(C,set_type) )
& ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
( ( range(sK13_skl,sK14_skl,sK15_skl) != sK14_skl
| ( ! [F] :
( ~ member(ordered_pair(F,sK17_skl),sK15_skl)
| ~ ilf_type(F,set_type) )
& member(sK17_skl,sK14_skl)
& ilf_type(sK17_skl,set_type) ) )
& ( range(sK13_skl,sK14_skl,sK15_skl) = sK14_skl
| ! [E] :
( ( member(ordered_pair(sK16_skl(E),E),sK15_skl)
& ilf_type(sK16_skl(E),set_type) )
| ~ member(E,sK14_skl)
| ~ ilf_type(E,set_type) ) )
& ilf_type(sK15_skl,relation_type(sK13_skl,sK14_skl))
& ilf_type(sK14_skl,set_type)
& ilf_type(sK13_skl,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(B,sK13_skl),skolemize(C,sK14_skl),skolemize(D,sK15_skl),skolemize(F,sK16_skl(E)),skolemize(E,sK17_skl)],[f159]) ).
fof(f163,plain,
ilf_type(sK15_skl,relation_type(sK13_skl,sK14_skl)),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f165,plain,
! [X0] :
( range(sK13_skl,sK14_skl,sK15_skl) = sK14_skl
| member(ordered_pair(sK16_skl(X0),X0),sK15_skl)
| ~ member(X0,sK14_skl)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f167,plain,
( range(sK13_skl,sK14_skl,sK15_skl) != sK14_skl
| member(sK17_skl,sK14_skl) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f168,plain,
! [X0] :
( range(sK13_skl,sK14_skl,sK15_skl) != sK14_skl
| ~ member(ordered_pair(X0,sK17_skl),sK15_skl)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f169,definition,
! [X0] :
( sQ0_spl
<=> ~ ilf_type(X0,set_type) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f170,plain,
! [X0] :
( ~ sQ0_spl
| ~ ilf_type(X0,set_type) ),
inference(component_clause,[status(thm)],[f169]) ).
fof(f172,definition,
! [X2,X3,X4] :
( sQ1_spl
<=> ( X4 = unordered_pair(unordered_pair(X2,X3),singleton(X2))
| X4 != ordered_pair(X2,X3)
| ~ ilf_type(X4,set_type)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f173,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| X2 = unordered_pair(unordered_pair(X0,X1),singleton(X0))
| X2 != ordered_pair(X0,X1)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(component_clause,[status(thm)],[f172]) ).
fof(f175,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f57,f169,f172]) ).
fof(f176,definition,
! [X2,X3,X4] :
( sQ2_spl
<=> ( X4 != unordered_pair(unordered_pair(X2,X3),singleton(X2))
| X4 = ordered_pair(X2,X3)
| ~ ilf_type(X4,set_type)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f179,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f58,f169,f176]) ).
fof(f183,definition,
( sQ4_spl
<=> range(sK13_skl,sK14_skl,sK15_skl) = sK14_skl ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f184,plain,
( ~ sQ4_spl
| range(sK13_skl,sK14_skl,sK15_skl) = sK14_skl ),
inference(component_clause,[status(thm)],[f183]) ).
fof(f185,plain,
( sQ4_spl
| range(sK13_skl,sK14_skl,sK15_skl) != sK14_skl ),
inference(component_clause,[status(thm)],[f183]) ).
fof(f187,definition,
! [X0] :
( sQ5_spl
<=> ( member(ordered_pair(sK16_skl(X0),X0),sK15_skl)
| ~ member(X0,sK14_skl)
| ~ ilf_type(X0,set_type) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f188,plain,
! [X0] :
( ~ sQ5_spl
| member(ordered_pair(sK16_skl(X0),X0),sK15_skl)
| ~ member(X0,sK14_skl)
| ~ ilf_type(X0,set_type) ),
inference(component_clause,[status(thm)],[f187]) ).
fof(f190,plain,
( sQ4_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f165,f187,f183]) ).
fof(f195,definition,
( sQ7_spl
<=> member(sK17_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f198,plain,
( ~ sQ4_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f167,f195,f183]) ).
fof(f199,definition,
! [X0] :
( sQ8_spl
<=> ( ~ member(ordered_pair(X0,sK17_skl),sK15_skl)
| ~ ilf_type(X0,set_type) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f200,plain,
! [X0] :
( ~ sQ8_spl
| ~ member(ordered_pair(X0,sK17_skl),sK15_skl)
| ~ ilf_type(X0,set_type) ),
inference(component_clause,[status(thm)],[f199]) ).
fof(f202,plain,
( ~ sQ4_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f168,f199,f183]) ).
fof(f207,plain,
! [X0] :
( ~ relation_like(X0)
| ilf_type(X0,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(duplicate_literals_removal,[status(thm)],[f86]) ).
fof(f208,plain,
! [X0] :
( ~ sQ8_spl
| ~ member(ordered_pair(X0,sK17_skl),sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f200,f157]) ).
fof(f209,plain,
! [X0] :
( ~ sQ5_spl
| member(ordered_pair(sK16_skl(X0),X0),sK15_skl)
| ~ member(X0,sK14_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f188,f157]) ).
fof(f213,plain,
! [X0,X1,X2] :
( ilf_type(range(X2,X0,X1),subset_type(X0))
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f156,f157]) ).
fof(f214,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f170,f157]) ).
fof(f215,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f214]) ).
fof(f216,plain,
! [X0,X1] :
( ~ sQ1_spl
| ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0))
| ~ ilf_type(ordered_pair(X0,X1),set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(destructive_equality_resolution,[status(thm)],[f173]) ).
fof(f217,plain,
! [X0,X1] :
( ~ sQ1_spl
| ordered_pair(X1,X0) = unordered_pair(unordered_pair(X1,X0),singleton(X1))
| ~ ilf_type(ordered_pair(X1,X0),set_type)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f216,f157]) ).
fof(f221,plain,
! [X0] : ~ empty(power_set(X0)),
inference(forward_subsumption_resolution,[status(thm)],[f121,f157]) ).
fof(f223,definition,
( sQ9_spl
<=> ilf_type(sK14_skl,set_type) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f225,plain,
( sQ9_spl
| ~ ilf_type(sK14_skl,set_type) ),
inference(component_clause,[status(thm)],[f223]) ).
fof(f226,definition,
( sQ10_spl
<=> ilf_type(sK15_skl,relation_type(sK13_skl,sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f228,plain,
( sQ10_spl
| ~ ilf_type(sK15_skl,relation_type(sK13_skl,sK14_skl)) ),
inference(component_clause,[status(thm)],[f226]) ).
fof(f233,plain,
! [X0,X1] :
( member(ordered_pair(sK0_skl(X1,X0),X1),X0)
| ~ member(X1,range_of(X0))
| ~ ilf_type(X0,binary_relation_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f41,f157]) ).
fof(f234,plain,
! [X0,X1,X2] :
( ~ member(ordered_pair(X2,X1),X0)
| ~ ilf_type(X2,set_type)
| member(X1,range_of(X0))
| ~ ilf_type(X0,binary_relation_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f42,f157]) ).
fof(f235,plain,
! [X0,X1] :
( ~ sQ1_spl
| ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0))
| ~ ilf_type(ordered_pair(X0,X1),set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f217,f157]) ).
fof(f236,plain,
! [X0,X1] :
( ~ sQ1_spl
| ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)) ),
inference(resolution,[status(thm)],[f235,f157]) ).
fof(f443,plain,
! [X0] :
( relation_like(X0)
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f148,f157]) ).
fof(f444,plain,
! [X0] :
( relation_like(X0)
| ~ ilf_type(X0,binary_relation_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f84,f157]) ).
fof(f445,plain,
! [X0] :
( ~ relation_like(X0)
| ilf_type(X0,binary_relation_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f207,f157]) ).
fof(f447,plain,
! [X0] :
( member(sK11_skl(X0),X0)
| relation_like(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f137,f157]) ).
fof(f448,plain,
! [X0,X1,X2] :
( member(X2,domain_of(X1))
| ~ member(ordered_pair(X2,X0),X1)
| ~ ilf_type(X1,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f46,f157]) ).
fof(f1101,plain,
! [X0] :
( member(sK12_skl(X0),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f146,f157]) ).
fof(f1102,plain,
! [X0] :
( member(ordered_pair(sK0_skl(sK12_skl(range_of(X0)),X0),sK12_skl(range_of(X0))),X0)
| ~ ilf_type(X0,binary_relation_type)
| empty(range_of(X0)) ),
inference(resolution,[status(thm)],[f1101,f233]) ).
fof(f1103,plain,
! [X0] :
( ilf_type(sK8_skl(X0),member_type(X0))
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f129,f157]) ).
fof(f1104,plain,
! [X0,X1] :
( ~ member(X1,X0)
| ~ ilf_type(X1,set_type)
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f144,f157]) ).
fof(f1105,plain,
! [X0,X1] :
( unordered_pair(X1,X0) = unordered_pair(X0,X1)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f81,f157]) ).
fof(f1106,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(resolution,[status(thm)],[f1105,f157]) ).
fof(f1129,plain,
! [X0,X1] :
( ~ sQ1_spl
| ordered_pair(X0,X1) = unordered_pair(unordered_pair(X1,X0),singleton(X0)) ),
inference(paramodulation,[status(thm)],[f1106,f236]) ).
fof(f1149,plain,
! [X0,X1] :
( X1 = X0
| member(sK1_skl(X0,X1),X0)
| member(sK1_skl(X0,X1),X1)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f52,f157]) ).
fof(f1150,plain,
! [X0,X1] :
( X1 = X0
| member(sK1_skl(X0,X1),X0)
| member(sK1_skl(X0,X1),X1) ),
inference(resolution,[status(thm)],[f1149,f157]) ).
fof(f1161,plain,
! [X0,X1] :
( ~ sQ1_spl
| ordered_pair(singleton(X0),unordered_pair(X1,X0)) = unordered_pair(ordered_pair(X0,X1),singleton(singleton(X0))) ),
inference(paramodulation,[status(thm)],[f1129,f1129]) ).
fof(f1162,plain,
! [X0,X1] :
( ~ sQ1_spl
| ordered_pair(singleton(X0),unordered_pair(X0,X1)) = unordered_pair(ordered_pair(X0,X1),singleton(singleton(X0))) ),
inference(paramodulation,[status(thm)],[f236,f1129]) ).
fof(f1274,plain,
! [X0,X1] :
( member(ordered_pair(sK0_skl(sK1_skl(X0,range_of(X1)),X1),sK1_skl(X0,range_of(X1))),X1)
| ~ ilf_type(X1,binary_relation_type)
| range_of(X1) = X0
| member(sK1_skl(X0,range_of(X1)),X0) ),
inference(resolution,[status(thm)],[f1150,f233]) ).
fof(f1275,plain,
! [X0,X1] :
( ~ member(X1,range_of(X0))
| ~ ilf_type(X1,set_type)
| member(ordered_pair(sK0_skl(sK12_skl(range_of(X0)),X0),sK12_skl(range_of(X0))),X0)
| ~ ilf_type(X0,binary_relation_type) ),
inference(resolution,[status(thm)],[f1102,f1104]) ).
fof(f1276,plain,
! [X0] :
( relation_like(range_of(X0))
| member(ordered_pair(sK0_skl(sK12_skl(range_of(X0)),X0),sK12_skl(range_of(X0))),X0)
| ~ ilf_type(X0,binary_relation_type) ),
inference(resolution,[status(thm)],[f1102,f443]) ).
fof(f1277,plain,
! [X0,X1] :
( ~ member(X1,range_of(X0))
| member(ordered_pair(sK0_skl(sK12_skl(range_of(X0)),X0),sK12_skl(range_of(X0))),X0)
| ~ ilf_type(X0,binary_relation_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f1275,f157]) ).
fof(f1387,plain,
! [X0,X1] :
( ~ sQ1_spl
| ordered_pair(singleton(X0),unordered_pair(X0,X1)) = ordered_pair(singleton(X0),unordered_pair(X1,X0)) ),
inference(forward_demodulation,[status(thm)],[f1161,f1162]) ).
fof(f1410,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ member(ordered_pair(singleton(X1),unordered_pair(X2,X1)),X0)
| ~ ilf_type(singleton(X1),set_type)
| member(unordered_pair(X1,X2),range_of(X0))
| ~ ilf_type(X0,binary_relation_type) ),
inference(paramodulation,[status(thm)],[f1387,f234]) ).
fof(f1431,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ member(ordered_pair(singleton(X1),unordered_pair(X2,X1)),X0)
| member(unordered_pair(X1,X2),range_of(X0))
| ~ ilf_type(X0,binary_relation_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f1410,f157]) ).
fof(f2023,plain,
! [X0] :
( member(ordered_pair(sK0_skl(sK1_skl(X0,range_of(sK3_skl)),sK3_skl),sK1_skl(X0,range_of(sK3_skl))),sK3_skl)
| range_of(sK3_skl) = X0
| member(sK1_skl(X0,range_of(sK3_skl)),X0) ),
inference(resolution,[status(thm)],[f1274,f88]) ).
fof(f2044,definition,
( sQ15_spl
<=> ilf_type(range_of(sK3_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f2046,plain,
( sQ15_spl
| ~ ilf_type(range_of(sK3_skl),set_type) ),
inference(component_clause,[status(thm)],[f2044]) ).
fof(f2051,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2046,f157]) ).
fof(f2052,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f2051]) ).
fof(f2056,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| ~ subset(X1,X0)
| X1 = X0
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f71,f157]) ).
fof(f2057,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f2056,f157]) ).
fof(f2059,plain,
! [X0,X1,X2] :
( ilf_type(X1,subset_type(cross_product(X2,X0)))
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f63,f157]) ).
fof(f2060,plain,
! [X0,X1] :
( ilf_type(X0,member_type(power_set(X1)))
| ~ ilf_type(X0,subset_type(X1))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f91,f157]) ).
fof(f2064,definition,
( sQ17_spl
<=> ilf_type(sK12_skl(range_of(sK3_skl)),set_type) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f2066,plain,
( sQ17_spl
| ~ ilf_type(sK12_skl(range_of(sK3_skl)),set_type) ),
inference(component_clause,[status(thm)],[f2064]) ).
fof(f2067,definition,
( sQ18_spl
<=> ilf_type(sK3_skl,binary_relation_type) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f2069,plain,
( sQ18_spl
| ~ ilf_type(sK3_skl,binary_relation_type) ),
inference(component_clause,[status(thm)],[f2067]) ).
fof(f2077,definition,
( sQ21_spl
<=> ilf_type(sK0_skl(sK12_skl(range_of(sK3_skl)),sK3_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f2079,plain,
( sQ21_spl
| ~ ilf_type(sK0_skl(sK12_skl(range_of(sK3_skl)),sK3_skl),set_type) ),
inference(component_clause,[status(thm)],[f2077]) ).
fof(f2081,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2069,f88]) ).
fof(f2082,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f2081]) ).
fof(f2083,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2079,f157]) ).
fof(f2084,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f2083]) ).
fof(f2085,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2066,f157]) ).
fof(f2086,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f2085]) ).
fof(f2093,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ member(ordered_pair(singleton(X0),unordered_pair(X1,X0)),sK3_skl)
| member(unordered_pair(X0,X1),range_of(sK3_skl)) ),
inference(resolution,[status(thm)],[f1431,f88]) ).
fof(f2406,plain,
! [X0,X1] :
( member(sK6_skl(X0,X1),X1)
| subset(X1,X0)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f109,f157]) ).
fof(f2407,plain,
! [X0,X1] :
( member(sK6_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f2406,f157]) ).
fof(f2408,plain,
! [X0,X1] :
( member(ordered_pair(sK0_skl(sK6_skl(X1,range_of(X0)),X0),sK6_skl(X1,range_of(X0))),X0)
| ~ ilf_type(X0,binary_relation_type)
| subset(range_of(X0),X1) ),
inference(resolution,[status(thm)],[f2407,f233]) ).
fof(f2409,plain,
! [X0,X1] :
( ~ member(sK6_skl(X0,X1),X0)
| subset(X1,X0)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f110,f157]) ).
fof(f2410,plain,
! [X0,X1] :
( ~ member(sK6_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f2409,f157]) ).
fof(f2413,plain,
! [X0,X1,X2] :
( relation_like(X1)
| ~ ilf_type(X1,subset_type(cross_product(X2,X0)))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f140,f157]) ).
fof(f2420,plain,
! [X0,X1] :
( member(sK5_skl(X0,X1),X0)
| member(sK5_skl(X0,X1),X1)
| X1 = X0
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f103,f157]) ).
fof(f2421,plain,
! [X0,X1] :
( member(sK5_skl(X1,X0),X1)
| member(sK5_skl(X1,X0),X0)
| X0 = X1 ),
inference(resolution,[status(thm)],[f2420,f157]) ).
fof(f2433,plain,
! [X0,X1] :
( member(ordered_pair(sK0_skl(sK5_skl(range_of(X1),X0),X1),sK5_skl(range_of(X1),X0)),X1)
| ~ ilf_type(X1,binary_relation_type)
| member(sK5_skl(range_of(X1),X0),X0)
| X0 = range_of(X1) ),
inference(resolution,[status(thm)],[f2421,f233]) ).
fof(f2476,plain,
! [X0,X1] :
( ~ sQ1_spl
| member(ordered_pair(sK0_skl(unordered_pair(X0,X1),sK3_skl),unordered_pair(X0,X1)),sK3_skl)
| ~ ilf_type(sK3_skl,binary_relation_type)
| ~ member(ordered_pair(singleton(X0),unordered_pair(X1,X0)),sK3_skl) ),
inference(resolution,[status(thm)],[f2093,f233]) ).
fof(f2489,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ member(ordered_pair(singleton(X1),unordered_pair(X0,X1)),sK3_skl)
| member(unordered_pair(X0,X1),range_of(sK3_skl)) ),
inference(paramodulation,[status(thm)],[f1106,f2093]) ).
fof(f2491,definition,
! [X0,X1] :
( sQ22_spl
<=> ( member(ordered_pair(sK0_skl(unordered_pair(X0,X1),sK3_skl),unordered_pair(X0,X1)),sK3_skl)
| ~ member(ordered_pair(singleton(X0),unordered_pair(X1,X0)),sK3_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f2494,plain,
( ~ sQ1_spl
| ~ sQ18_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f2476,f2491,f2067,f172]) ).
fof(f2496,plain,
! [X0,X1] :
( ~ sQ1_spl
| member(ordered_pair(sK0_skl(unordered_pair(X1,X0),sK3_skl),unordered_pair(X1,X0)),sK3_skl)
| ~ ilf_type(sK3_skl,binary_relation_type)
| ~ member(ordered_pair(singleton(X0),unordered_pair(X1,X0)),sK3_skl) ),
inference(resolution,[status(thm)],[f2489,f233]) ).
fof(f2511,definition,
! [X0,X1] :
( sQ23_spl
<=> ( member(ordered_pair(sK0_skl(unordered_pair(X1,X0),sK3_skl),unordered_pair(X1,X0)),sK3_skl)
| ~ member(ordered_pair(singleton(X0),unordered_pair(X1,X0)),sK3_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f2514,plain,
( ~ sQ1_spl
| ~ sQ18_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f2496,f2511,f2067,f172]) ).
fof(f2529,plain,
! [X0,X1] :
( member(X1,X0)
| ~ ilf_type(X1,member_type(X0))
| ~ ilf_type(X0,set_type)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f125,f157]) ).
fof(f2530,plain,
! [X0,X1] :
( member(X1,X0)
| ~ ilf_type(X1,member_type(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f2529,f157]) ).
fof(f2531,plain,
! [X0] :
( empty(X0)
| member(sK8_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f2530,f1103]) ).
fof(f2532,plain,
! [X0,X1] :
( ~ ilf_type(X1,subset_type(X0))
| ~ ilf_type(X1,set_type)
| member(X1,power_set(X0))
| empty(power_set(X0)) ),
inference(resolution,[status(thm)],[f2530,f2060]) ).
fof(f2533,plain,
! [X0] :
( member(sK8_skl(X0),X0)
| empty(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2531]) ).
fof(f2534,plain,
! [X0,X1] :
( ~ ilf_type(X0,subset_type(X1))
| ~ ilf_type(X0,set_type)
| member(X0,power_set(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2532,f221]) ).
fof(f2536,plain,
! [X0,X1] :
( ~ ilf_type(X0,subset_type(X1))
| member(X0,power_set(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2534,f157]) ).
fof(f2539,plain,
! [X0,X1,X2] :
( ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| member(range(X0,X1,X2),power_set(X1)) ),
inference(resolution,[status(thm)],[f2536,f213]) ).
fof(f2542,plain,
! [X0,X1,X2] :
( ~ ilf_type(X2,relation_type(X0,X1))
| member(range(X0,X1,X2),power_set(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2539,f157]) ).
fof(f2551,plain,
! [X0,X1,X2] :
( member(X2,X0)
| ~ member(X2,X1)
| ~ ilf_type(X2,set_type)
| ~ member(X1,power_set(X0))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f116,f157]) ).
fof(f2552,plain,
! [X0,X1,X2] :
( member(X2,X0)
| ~ member(X2,X1)
| ~ member(X1,power_set(X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f2551,f157]) ).
fof(f2553,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ member(X0,power_set(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2552,f157]) ).
fof(f2560,plain,
! [X0,X1,X2] :
( subset(X2,X1)
| ~ member(sK6_skl(X1,X2),X0)
| ~ member(X0,power_set(X1)) ),
inference(resolution,[status(thm)],[f2553,f2410]) ).
fof(f2579,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f228,f163]) ).
fof(f2580,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f2579]) ).
fof(f2586,plain,
! [X0] :
( ~ sQ5_spl
| member(sK16_skl(X0),domain_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(X0,set_type)
| ~ member(X0,sK14_skl) ),
inference(resolution,[status(thm)],[f209,f448]) ).
fof(f2587,plain,
! [X0] :
( ~ sQ5_spl
| ~ ilf_type(sK16_skl(X0),set_type)
| member(X0,range_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ member(X0,sK14_skl) ),
inference(resolution,[status(thm)],[f209,f234]) ).
fof(f2588,definition,
! [X0] :
( sQ25_spl
<=> ( member(sK16_skl(X0),domain_of(sK15_skl))
| ~ ilf_type(X0,set_type)
| ~ member(X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f2589,plain,
! [X0] :
( ~ sQ25_spl
| member(sK16_skl(X0),domain_of(sK15_skl))
| ~ ilf_type(X0,set_type)
| ~ member(X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f2588]) ).
fof(f2591,definition,
( sQ26_spl
<=> ilf_type(sK15_skl,binary_relation_type) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f2592,plain,
( ~ sQ26_spl
| ilf_type(sK15_skl,binary_relation_type) ),
inference(component_clause,[status(thm)],[f2591]) ).
fof(f2593,plain,
( sQ26_spl
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(component_clause,[status(thm)],[f2591]) ).
fof(f2594,plain,
( ~ sQ5_spl
| ~ sQ26_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f2586,f2588,f2591,f187]) ).
fof(f2595,definition,
! [X0] :
( sQ27_spl
<=> ( ~ ilf_type(sK16_skl(X0),set_type)
| member(X0,range_of(sK15_skl))
| ~ member(X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f2596,plain,
! [X0] :
( ~ sQ27_spl
| ~ ilf_type(sK16_skl(X0),set_type)
| member(X0,range_of(sK15_skl))
| ~ member(X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f2595]) ).
fof(f2598,plain,
( ~ sQ5_spl
| ~ sQ26_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f2587,f2595,f2591,f187]) ).
fof(f2599,plain,
( sQ26_spl
| ~ relation_like(sK15_skl) ),
inference(resolution,[status(thm)],[f2593,f445]) ).
fof(f2602,plain,
! [X0,X1] :
( sQ26_spl
| ~ ilf_type(sK15_skl,subset_type(cross_product(X1,X0)))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f2599,f2413]) ).
fof(f2605,plain,
! [X0,X1] :
( sQ26_spl
| ~ ilf_type(sK15_skl,subset_type(cross_product(X0,X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2602,f157]) ).
fof(f2606,plain,
! [X0,X1] :
( sQ26_spl
| ~ ilf_type(sK15_skl,relation_type(X1,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f2605,f2059]) ).
fof(f2608,plain,
! [X0,X1] :
( sQ26_spl
| ~ ilf_type(sK15_skl,relation_type(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2606,f157]) ).
fof(f2609,definition,
( sQ28_spl
<=> ilf_type(sK15_skl,set_type) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f2611,plain,
( sQ28_spl
| ~ ilf_type(sK15_skl,set_type) ),
inference(component_clause,[status(thm)],[f2609]) ).
fof(f2616,plain,
! [X0] :
( ~ sQ25_spl
| member(sK16_skl(X0),domain_of(sK15_skl))
| ~ member(X0,sK14_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2589,f157]) ).
fof(f2617,plain,
! [X0] :
( ~ sQ27_spl
| member(X0,range_of(sK15_skl))
| ~ member(X0,sK14_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2596,f157]) ).
fof(f2618,plain,
( ~ sQ27_spl
| empty(sK14_skl)
| member(sK8_skl(sK14_skl),range_of(sK15_skl)) ),
inference(resolution,[status(thm)],[f2617,f2533]) ).
fof(f2621,plain,
! [X0] :
( ~ sQ27_spl
| subset(sK14_skl,X0)
| member(sK6_skl(X0,sK14_skl),range_of(sK15_skl)) ),
inference(resolution,[status(thm)],[f2617,f2407]) ).
fof(f2623,plain,
( ~ sQ27_spl
| empty(sK14_skl)
| member(sK12_skl(sK14_skl),range_of(sK15_skl)) ),
inference(resolution,[status(thm)],[f2617,f1101]) ).
fof(f2625,definition,
( sQ30_spl
<=> member(sK8_skl(sK14_skl),range_of(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f2626,plain,
( ~ sQ30_spl
| member(sK8_skl(sK14_skl),range_of(sK15_skl)) ),
inference(component_clause,[status(thm)],[f2625]) ).
fof(f2628,definition,
( sQ31_spl
<=> empty(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f2629,plain,
( ~ sQ31_spl
| empty(sK14_skl) ),
inference(component_clause,[status(thm)],[f2628]) ).
fof(f2631,plain,
( ~ sQ27_spl
| sQ31_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f2618,f2625,f2628,f2595]) ).
fof(f2632,definition,
( sQ32_spl
<=> member(sK12_skl(sK14_skl),range_of(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f2633,plain,
( ~ sQ32_spl
| member(sK12_skl(sK14_skl),range_of(sK15_skl)) ),
inference(component_clause,[status(thm)],[f2632]) ).
fof(f2635,plain,
( ~ sQ27_spl
| sQ31_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f2623,f2632,f2628,f2595]) ).
fof(f2636,plain,
! [X0] :
( ~ sQ31_spl
| ~ member(X0,sK14_skl)
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f2629,f1104]) ).
fof(f2638,plain,
! [X0] :
( ~ sQ31_spl
| ~ member(X0,sK14_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2636,f157]) ).
fof(f2643,plain,
! [X0] :
( ~ sQ31_spl
| sK14_skl = X0
| member(sK1_skl(X0,sK14_skl),X0) ),
inference(resolution,[status(thm)],[f2638,f1150]) ).
fof(f2648,plain,
! [X0,X1] :
( X1 = ordered_pair(sK9_skl(X1,X0),sK10_skl(X1,X0))
| ~ member(X1,X0)
| ~ ilf_type(X1,set_type)
| ~ relation_like(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f135,f157]) ).
fof(f2649,plain,
! [X0,X1] :
( X1 = ordered_pair(sK9_skl(X1,X0),sK10_skl(X1,X0))
| ~ member(X1,X0)
| ~ relation_like(X0) ),
inference(resolution,[status(thm)],[f2648,f157]) ).
fof(f2652,plain,
( ~ sQ32_spl
| member(ordered_pair(sK0_skl(sK12_skl(sK14_skl),sK15_skl),sK12_skl(sK14_skl)),sK15_skl)
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f2633,f233]) ).
fof(f2653,definition,
( sQ33_spl
<=> member(ordered_pair(sK0_skl(sK12_skl(sK14_skl),sK15_skl),sK12_skl(sK14_skl)),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f2654,plain,
( ~ sQ33_spl
| member(ordered_pair(sK0_skl(sK12_skl(sK14_skl),sK15_skl),sK12_skl(sK14_skl)),sK15_skl) ),
inference(component_clause,[status(thm)],[f2653]) ).
fof(f2656,plain,
( ~ sQ32_spl
| sQ33_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f2652,f2591,f2653,f2632]) ).
fof(f2657,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2611,f157]) ).
fof(f2658,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f2657]) ).
fof(f2664,plain,
( sQ26_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f163,f2608]) ).
fof(f2666,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f2664]) ).
fof(f2667,plain,
! [X0] :
( ~ sQ26_spl
| member(ordered_pair(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),sK5_skl(range_of(sK15_skl),X0)),sK15_skl)
| member(sK5_skl(range_of(sK15_skl),X0),X0)
| X0 = range_of(sK15_skl) ),
inference(resolution,[status(thm)],[f2592,f2433]) ).
fof(f2668,plain,
! [X0] :
( ~ sQ26_spl
| member(ordered_pair(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),sK6_skl(X0,range_of(sK15_skl))),sK15_skl)
| subset(range_of(sK15_skl),X0) ),
inference(resolution,[status(thm)],[f2592,f2408]) ).
fof(f2670,plain,
! [X0] :
( ~ sQ26_spl
| ~ member(X0,range_of(sK15_skl))
| member(ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))),sK15_skl) ),
inference(resolution,[status(thm)],[f2592,f1277]) ).
fof(f2671,plain,
! [X0] :
( ~ sQ26_spl
| member(ordered_pair(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),sK1_skl(X0,range_of(sK15_skl))),sK15_skl)
| range_of(sK15_skl) = X0
| member(sK1_skl(X0,range_of(sK15_skl)),X0) ),
inference(resolution,[status(thm)],[f2592,f1274]) ).
fof(f2672,definition,
( sQ34_spl
<=> member(ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f2673,plain,
( ~ sQ34_spl
| member(ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))),sK15_skl) ),
inference(component_clause,[status(thm)],[f2672]) ).
fof(f2675,definition,
! [X0] :
( sQ35_spl
<=> ~ member(X0,range_of(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f2676,plain,
! [X0] :
( ~ sQ35_spl
| ~ member(X0,range_of(sK15_skl)) ),
inference(component_clause,[status(thm)],[f2675]) ).
fof(f2678,plain,
( ~ sQ26_spl
| sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f2670,f2672,f2675,f2591]) ).
fof(f2687,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f225,f157]) ).
fof(f2688,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f2687]) ).
fof(f2693,plain,
! [X0,X1] :
( member(sK11_skl(X1),X1)
| X0 = ordered_pair(sK9_skl(X0,X1),sK10_skl(X0,X1))
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f2649,f447]) ).
fof(f2694,plain,
! [X0,X1] :
( ~ ilf_type(X1,binary_relation_type)
| X0 = ordered_pair(sK9_skl(X0,X1),sK10_skl(X0,X1))
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f2649,f444]) ).
fof(f2700,plain,
( ~ sQ30_spl
| member(ordered_pair(sK0_skl(sK8_skl(sK14_skl),sK15_skl),sK8_skl(sK14_skl)),sK15_skl)
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f2626,f233]) ).
fof(f2701,definition,
( sQ37_spl
<=> member(ordered_pair(sK0_skl(sK8_skl(sK14_skl),sK15_skl),sK8_skl(sK14_skl)),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f2702,plain,
( ~ sQ37_spl
| member(ordered_pair(sK0_skl(sK8_skl(sK14_skl),sK15_skl),sK8_skl(sK14_skl)),sK15_skl) ),
inference(component_clause,[status(thm)],[f2701]) ).
fof(f2704,plain,
( ~ sQ30_spl
| sQ37_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f2700,f2591,f2701,f2625]) ).
fof(f2745,plain,
! [X0,X1,X2] :
( sK11_skl(X0) != ordered_pair(X1,X2)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| relation_like(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f138,f157]) ).
fof(f2746,plain,
! [X0,X1,X2] :
( sK11_skl(X0) != ordered_pair(X1,X2)
| ~ ilf_type(X1,set_type)
| relation_like(X0) ),
inference(resolution,[status(thm)],[f2745,f157]) ).
fof(f2747,plain,
! [X0,X1,X2] :
( sK11_skl(X0) != ordered_pair(X1,X2)
| relation_like(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2746,f157]) ).
fof(f2748,plain,
! [X0,X1,X2] :
( domain(X2,X0,X1) = domain_of(X1)
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f150,f157]) ).
fof(f2749,plain,
! [X0,X1,X2] :
( domain(X1,X2,X0) = domain_of(X0)
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(resolution,[status(thm)],[f2748,f157]) ).
fof(f2750,plain,
! [X0,X1,X2] :
( ilf_type(domain(X2,X0,X1),subset_type(X2))
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f152,f157]) ).
fof(f2751,plain,
! [X0,X1,X2] :
( member(domain(X2,X0,X1),power_set(X2))
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f2750,f2536]) ).
fof(f2752,plain,
! [X0,X1,X2] :
( member(domain(X1,X2,X0),power_set(X1))
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2751,f157]) ).
fof(f2761,plain,
! [X0,X1,X2,X3] :
( X3 = ordered_pair(sK9_skl(X3,X0),sK10_skl(X3,X0))
| ~ member(X3,X0)
| sK11_skl(X0) != ordered_pair(X1,X2) ),
inference(resolution,[status(thm)],[f2747,f2649]) ).
fof(f2763,plain,
domain(sK13_skl,sK14_skl,sK15_skl) = domain_of(sK15_skl),
inference(resolution,[status(thm)],[f2749,f163]) ).
fof(f2768,plain,
( ilf_type(domain_of(sK15_skl),subset_type(sK13_skl))
| ~ ilf_type(sK15_skl,relation_type(sK13_skl,sK14_skl))
| ~ ilf_type(sK14_skl,set_type) ),
inference(paramodulation,[status(thm)],[f2763,f2750]) ).
fof(f2769,definition,
( sQ41_spl
<=> ilf_type(domain_of(sK15_skl),subset_type(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f2772,plain,
( sQ41_spl
| ~ sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f2768,f223,f226,f2769]) ).
fof(f2786,plain,
( ~ sQ27_spl
| subset(sK14_skl,range_of(sK15_skl))
| subset(sK14_skl,range_of(sK15_skl)) ),
inference(resolution,[status(thm)],[f2621,f2410]) ).
fof(f2788,definition,
( sQ43_spl
<=> subset(sK14_skl,range_of(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f2789,plain,
( ~ sQ43_spl
| subset(sK14_skl,range_of(sK15_skl)) ),
inference(component_clause,[status(thm)],[f2788]) ).
fof(f2791,plain,
( ~ sQ27_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f2786,f2788,f2595]) ).
fof(f2797,plain,
( ~ sQ43_spl
| ~ subset(range_of(sK15_skl),sK14_skl)
| range_of(sK15_skl) = sK14_skl ),
inference(resolution,[status(thm)],[f2789,f2057]) ).
fof(f2798,definition,
( sQ45_spl
<=> range_of(sK15_skl) = sK14_skl ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f2799,plain,
( ~ sQ45_spl
| range_of(sK15_skl) = sK14_skl ),
inference(component_clause,[status(thm)],[f2798]) ).
fof(f2800,plain,
( sQ45_spl
| range_of(sK15_skl) != sK14_skl ),
inference(component_clause,[status(thm)],[f2798]) ).
fof(f2801,definition,
( sQ46_spl
<=> subset(range_of(sK15_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f2803,plain,
( sQ46_spl
| ~ subset(range_of(sK15_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f2801]) ).
fof(f2804,plain,
( ~ sQ43_spl
| ~ sQ46_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f2797,f2798,f2801,f2788]) ).
fof(f2815,plain,
! [X0] :
( ~ sQ45_spl
| member(ordered_pair(sK0_skl(X0,sK15_skl),X0),sK15_skl)
| ~ member(X0,sK14_skl)
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(paramodulation,[status(thm)],[f2799,f233]) ).
fof(f2833,definition,
! [X0] :
( sQ51_spl
<=> ( member(ordered_pair(sK0_skl(X0,sK15_skl),X0),sK15_skl)
| ~ member(X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f2834,plain,
! [X0] :
( ~ sQ51_spl
| member(ordered_pair(sK0_skl(X0,sK15_skl),X0),sK15_skl)
| ~ member(X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f2833]) ).
fof(f2836,plain,
( ~ sQ45_spl
| sQ51_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f2815,f2591,f2833,f2798]) ).
fof(f2848,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ member(X1,X0)
| ~ member(X0,power_set(sK14_skl)) ),
inference(resolution,[status(thm)],[f2638,f2553]) ).
fof(f2851,plain,
! [X0,X1,X2] :
( range(X2,X0,X1) = range_of(X1)
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f154,f157]) ).
fof(f2852,plain,
! [X0,X1,X2] :
( range(X1,X2,X0) = range_of(X0)
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(resolution,[status(thm)],[f2851,f157]) ).
fof(f2853,plain,
range(sK13_skl,sK14_skl,sK15_skl) = range_of(sK15_skl),
inference(resolution,[status(thm)],[f2852,f163]) ).
fof(f2863,plain,
! [X0] :
( sQ46_spl
| ~ member(sK6_skl(sK14_skl,range_of(sK15_skl)),X0)
| ~ member(X0,power_set(sK14_skl)) ),
inference(resolution,[status(thm)],[f2803,f2560]) ).
fof(f2896,definition,
( sQ56_spl
<=> empty(power_set(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f2897,plain,
( ~ sQ56_spl
| empty(power_set(sK14_skl)) ),
inference(component_clause,[status(thm)],[f2896]) ).
fof(f2911,plain,
( ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2897,f221]) ).
fof(f2912,plain,
~ sQ56_spl,
inference(contradiction_clause,[status(thm)],[f2911]) ).
fof(f3035,plain,
! [X0] :
( ~ sQ26_spl
| X0 = ordered_pair(sK9_skl(X0,sK15_skl),sK10_skl(X0,sK15_skl))
| ~ member(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f2694,f2592]) ).
fof(f3223,plain,
( sQ4_spl
| range_of(sK15_skl) != sK14_skl ),
inference(backward_demodulation,[status(thm)],[f2853,f185]) ).
fof(f3224,plain,
( ~ ilf_type(sK15_skl,relation_type(sK13_skl,sK14_skl))
| member(range_of(sK15_skl),power_set(sK14_skl)) ),
inference(paramodulation,[status(thm)],[f2853,f2542]) ).
fof(f3225,plain,
( ilf_type(range_of(sK15_skl),subset_type(sK14_skl))
| ~ ilf_type(sK15_skl,relation_type(sK13_skl,sK14_skl))
| ~ ilf_type(sK14_skl,set_type) ),
inference(paramodulation,[status(thm)],[f2853,f213]) ).
fof(f3226,definition,
( sQ82_spl
<=> member(range_of(sK15_skl),power_set(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f3227,plain,
( ~ sQ82_spl
| member(range_of(sK15_skl),power_set(sK14_skl)) ),
inference(component_clause,[status(thm)],[f3226]) ).
fof(f3229,plain,
( ~ sQ10_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f3224,f3226,f226]) ).
fof(f3230,definition,
( sQ83_spl
<=> ilf_type(range_of(sK15_skl),subset_type(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f3233,plain,
( sQ83_spl
| ~ sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f3225,f223,f226,f3230]) ).
fof(f3241,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ82_spl
| ~ member(X0,range_of(sK15_skl)) ),
inference(resolution,[status(thm)],[f3227,f2848]) ).
fof(f3258,plain,
( ~ sQ31_spl
| ~ sQ82_spl
| sK14_skl = range_of(sK15_skl) ),
inference(resolution,[status(thm)],[f3241,f2643]) ).
fof(f3271,plain,
( ~ sQ31_spl
| ~ sQ82_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f3258,f2798,f3226,f2628]) ).
fof(f3272,plain,
( ~ sQ4_spl
| range_of(sK15_skl) = sK14_skl ),
inference(forward_demodulation,[status(thm)],[f2853,f184]) ).
fof(f3273,plain,
( ~ sQ4_spl
| sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3272,f2800]) ).
fof(f3274,plain,
( ~ sQ4_spl
| sQ45_spl ),
inference(contradiction_clause,[status(thm)],[f3273]) ).
fof(f3290,plain,
! [X0] :
( ~ sQ4_spl
| member(ordered_pair(sK0_skl(X0,sK15_skl),X0),sK15_skl)
| ~ member(X0,sK14_skl)
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(paramodulation,[status(thm)],[f3272,f233]) ).
fof(f3296,plain,
( ~ sQ4_spl
| sQ51_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f3290,f2591,f2833,f183]) ).
fof(f3351,plain,
! [X0] :
( member(sK0_skl(sK1_skl(X0,range_of(sK3_skl)),sK3_skl),domain_of(sK3_skl))
| ~ ilf_type(sK3_skl,binary_relation_type)
| ~ ilf_type(sK1_skl(X0,range_of(sK3_skl)),set_type)
| range_of(sK3_skl) = X0
| member(sK1_skl(X0,range_of(sK3_skl)),X0) ),
inference(resolution,[status(thm)],[f2023,f448]) ).
fof(f3352,plain,
! [X0] :
( ~ ilf_type(sK0_skl(sK1_skl(X0,range_of(sK3_skl)),sK3_skl),set_type)
| member(sK1_skl(X0,range_of(sK3_skl)),range_of(sK3_skl))
| ~ ilf_type(sK3_skl,binary_relation_type)
| range_of(sK3_skl) = X0
| member(sK1_skl(X0,range_of(sK3_skl)),X0) ),
inference(resolution,[status(thm)],[f2023,f234]) ).
fof(f3354,definition,
! [X0] :
( sQ90_spl
<=> ( member(sK0_skl(sK1_skl(X0,range_of(sK3_skl)),sK3_skl),domain_of(sK3_skl))
| ~ ilf_type(sK1_skl(X0,range_of(sK3_skl)),set_type)
| range_of(sK3_skl) = X0
| member(sK1_skl(X0,range_of(sK3_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f3357,plain,
( ~ sQ18_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f3351,f3354,f2067]) ).
fof(f3358,definition,
! [X0] :
( sQ91_spl
<=> ( ~ ilf_type(sK0_skl(sK1_skl(X0,range_of(sK3_skl)),sK3_skl),set_type)
| member(sK1_skl(X0,range_of(sK3_skl)),range_of(sK3_skl))
| range_of(sK3_skl) = X0
| member(sK1_skl(X0,range_of(sK3_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f3361,plain,
( ~ sQ18_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f3352,f3358,f2067]) ).
fof(f3381,plain,
( ~ sQ8_spl
| ~ sQ51_spl
| ~ member(sK17_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f2834,f208]) ).
fof(f3383,plain,
! [X0] :
( ~ sQ51_spl
| member(sK0_skl(X0,sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(X0,set_type)
| ~ member(X0,sK14_skl) ),
inference(resolution,[status(thm)],[f2834,f448]) ).
fof(f3384,plain,
! [X0] :
( ~ sQ51_spl
| ~ ilf_type(sK0_skl(X0,sK15_skl),set_type)
| member(X0,range_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ member(X0,sK14_skl) ),
inference(resolution,[status(thm)],[f2834,f234]) ).
fof(f3385,plain,
! [X0,X1,X2] :
( ~ sQ51_spl
| ordered_pair(sK0_skl(X0,sK15_skl),X0) = ordered_pair(sK9_skl(ordered_pair(sK0_skl(X0,sK15_skl),X0),sK15_skl),sK10_skl(ordered_pair(sK0_skl(X0,sK15_skl),X0),sK15_skl))
| sK11_skl(sK15_skl) != ordered_pair(X1,X2)
| ~ member(X0,sK14_skl) ),
inference(resolution,[status(thm)],[f2834,f2761]) ).
fof(f3386,plain,
( ~ sQ8_spl
| ~ sQ51_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f3381,f195,f2833,f199]) ).
fof(f3391,definition,
! [X0] :
( sQ94_spl
<=> ( member(sK0_skl(X0,sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(X0,set_type)
| ~ member(X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f3392,plain,
! [X0] :
( ~ sQ94_spl
| member(sK0_skl(X0,sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(X0,set_type)
| ~ member(X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f3391]) ).
fof(f3394,plain,
( ~ sQ51_spl
| ~ sQ26_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f3383,f3391,f2591,f2833]) ).
fof(f3395,definition,
! [X0] :
( sQ95_spl
<=> ( ~ ilf_type(sK0_skl(X0,sK15_skl),set_type)
| member(X0,range_of(sK15_skl))
| ~ member(X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f3398,plain,
( ~ sQ51_spl
| ~ sQ26_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f3384,f3395,f2591,f2833]) ).
fof(f3399,definition,
! [X0] :
( sQ96_spl
<=> ( ordered_pair(sK0_skl(X0,sK15_skl),X0) = ordered_pair(sK9_skl(ordered_pair(sK0_skl(X0,sK15_skl),X0),sK15_skl),sK10_skl(ordered_pair(sK0_skl(X0,sK15_skl),X0),sK15_skl))
| ~ member(X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f3402,definition,
! [X1,X2] :
( sQ97_spl
<=> sK11_skl(sK15_skl) != ordered_pair(X1,X2) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f3403,plain,
! [X0,X1] :
( ~ sQ97_spl
| sK11_skl(sK15_skl) != ordered_pair(X0,X1) ),
inference(component_clause,[status(thm)],[f3402]) ).
fof(f3405,plain,
( ~ sQ51_spl
| sQ97_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f3385,f3399,f3402,f2833]) ).
fof(f3406,plain,
! [X0] :
( ~ sQ94_spl
| member(sK0_skl(X0,sK15_skl),domain_of(sK15_skl))
| ~ member(X0,sK14_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3392,f157]) ).
fof(f3408,plain,
( sQ4_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f3223,f2798,f183]) ).
fof(f3434,plain,
! [X0,X1,X2] :
( ~ sQ25_spl
| sK16_skl(X0) = ordered_pair(sK9_skl(sK16_skl(X0),domain_of(sK15_skl)),sK10_skl(sK16_skl(X0),domain_of(sK15_skl)))
| sK11_skl(domain_of(sK15_skl)) != ordered_pair(X1,X2)
| ~ member(X0,sK14_skl) ),
inference(resolution,[status(thm)],[f2616,f2761]) ).
fof(f3435,definition,
! [X0] :
( sQ99_spl
<=> ( sK16_skl(X0) = ordered_pair(sK9_skl(sK16_skl(X0),domain_of(sK15_skl)),sK10_skl(sK16_skl(X0),domain_of(sK15_skl)))
| ~ member(X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f3438,definition,
! [X1,X2] :
( sQ100_spl
<=> sK11_skl(domain_of(sK15_skl)) != ordered_pair(X1,X2) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f3441,plain,
( ~ sQ25_spl
| sQ100_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f3434,f3435,f3438,f2588]) ).
fof(f3450,definition,
( sQ101_spl
<=> member(sK11_skl(sK14_skl),range_of(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f3451,plain,
( ~ sQ101_spl
| member(sK11_skl(sK14_skl),range_of(sK15_skl)) ),
inference(component_clause,[status(thm)],[f3450]) ).
fof(f3460,plain,
! [X0,X1] :
( ~ sQ30_spl
| sK8_skl(sK14_skl) = ordered_pair(sK9_skl(sK8_skl(sK14_skl),range_of(sK15_skl)),sK10_skl(sK8_skl(sK14_skl),range_of(sK15_skl)))
| sK11_skl(range_of(sK15_skl)) != ordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[f2626,f2761]) ).
fof(f3462,definition,
! [X0,X1] :
( sQ103_spl
<=> sK11_skl(range_of(sK15_skl)) != ordered_pair(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f3465,definition,
( sQ104_spl
<=> sK8_skl(sK14_skl) = ordered_pair(sK9_skl(sK8_skl(sK14_skl),range_of(sK15_skl)),sK10_skl(sK8_skl(sK14_skl),range_of(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f3468,plain,
( ~ sQ30_spl
| sQ104_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f3460,f3462,f3465,f2625]) ).
fof(f3470,plain,
! [X0,X1] :
( ~ sQ32_spl
| sK12_skl(sK14_skl) = ordered_pair(sK9_skl(sK12_skl(sK14_skl),range_of(sK15_skl)),sK10_skl(sK12_skl(sK14_skl),range_of(sK15_skl)))
| sK11_skl(range_of(sK15_skl)) != ordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[f2633,f2761]) ).
fof(f3472,definition,
( sQ105_spl
<=> sK12_skl(sK14_skl) = ordered_pair(sK9_skl(sK12_skl(sK14_skl),range_of(sK15_skl)),sK10_skl(sK12_skl(sK14_skl),range_of(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f3475,plain,
( ~ sQ32_spl
| sQ105_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f3470,f3462,f3472,f2632]) ).
fof(f3476,plain,
( ~ sQ101_spl
| member(ordered_pair(sK0_skl(sK11_skl(sK14_skl),sK15_skl),sK11_skl(sK14_skl)),sK15_skl)
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f3451,f233]) ).
fof(f3477,plain,
! [X0,X1] :
( ~ sQ101_spl
| sK11_skl(sK14_skl) = ordered_pair(sK9_skl(sK11_skl(sK14_skl),range_of(sK15_skl)),sK10_skl(sK11_skl(sK14_skl),range_of(sK15_skl)))
| sK11_skl(range_of(sK15_skl)) != ordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[f3451,f2761]) ).
fof(f3478,definition,
( sQ106_spl
<=> member(ordered_pair(sK0_skl(sK11_skl(sK14_skl),sK15_skl),sK11_skl(sK14_skl)),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f3481,plain,
( ~ sQ101_spl
| sQ106_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f3476,f2591,f3478,f3450]) ).
fof(f3482,definition,
( sQ107_spl
<=> sK11_skl(sK14_skl) = ordered_pair(sK9_skl(sK11_skl(sK14_skl),range_of(sK15_skl)),sK10_skl(sK11_skl(sK14_skl),range_of(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f3485,plain,
( ~ sQ101_spl
| sQ107_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f3477,f3462,f3482,f3450]) ).
fof(f3523,definition,
( sQ110_spl
<=> ilf_type(range_of(sK15_skl),binary_relation_type) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f3525,plain,
( sQ110_spl
| ~ ilf_type(range_of(sK15_skl),binary_relation_type) ),
inference(component_clause,[status(thm)],[f3523]) ).
fof(f3548,plain,
( sQ110_spl
| ~ relation_like(range_of(sK15_skl)) ),
inference(resolution,[status(thm)],[f3525,f445]) ).
fof(f3549,plain,
( sQ110_spl
| member(ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))),sK15_skl)
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f3548,f1276]) ).
fof(f3554,plain,
( sQ110_spl
| sQ34_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f3549,f2591,f2672,f3523]) ).
fof(f3724,plain,
! [X0,X1,X2] :
( ~ sQ94_spl
| sK0_skl(X0,sK15_skl) = ordered_pair(sK9_skl(sK0_skl(X0,sK15_skl),domain_of(sK15_skl)),sK10_skl(sK0_skl(X0,sK15_skl),domain_of(sK15_skl)))
| sK11_skl(domain_of(sK15_skl)) != ordered_pair(X1,X2)
| ~ member(X0,sK14_skl) ),
inference(resolution,[status(thm)],[f3406,f2761]) ).
fof(f3725,definition,
! [X0] :
( sQ129_spl
<=> ( sK0_skl(X0,sK15_skl) = ordered_pair(sK9_skl(sK0_skl(X0,sK15_skl),domain_of(sK15_skl)),sK10_skl(sK0_skl(X0,sK15_skl),domain_of(sK15_skl)))
| ~ member(X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f3728,plain,
( ~ sQ94_spl
| sQ100_spl
| sQ129_spl ),
inference(split_clause,[status(thm)],[f3724,f3725,f3438,f3391]) ).
fof(f3830,definition,
( sQ136_spl
<=> ilf_type(sK10_skl(sK17_skl,sK14_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f3832,plain,
( sQ136_spl
| ~ ilf_type(sK10_skl(sK17_skl,sK14_skl),set_type) ),
inference(component_clause,[status(thm)],[f3830]) ).
fof(f3852,definition,
( sQ139_spl
<=> ilf_type(sK9_skl(sK17_skl,sK14_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f3854,plain,
( sQ139_spl
| ~ ilf_type(sK9_skl(sK17_skl,sK14_skl),set_type) ),
inference(component_clause,[status(thm)],[f3852]) ).
fof(f3857,plain,
( sQ136_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3832,f157]) ).
fof(f3858,plain,
sQ136_spl,
inference(contradiction_clause,[status(thm)],[f3857]) ).
fof(f3859,plain,
( sQ139_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3854,f157]) ).
fof(f3860,plain,
sQ139_spl,
inference(contradiction_clause,[status(thm)],[f3859]) ).
fof(f3884,definition,
( sQ140_spl
<=> ilf_type(power_set(sK17_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f3886,plain,
( sQ140_spl
| ~ ilf_type(power_set(sK17_skl),set_type) ),
inference(component_clause,[status(thm)],[f3884]) ).
fof(f3891,plain,
( sQ140_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3886,f157]) ).
fof(f3892,plain,
sQ140_spl,
inference(contradiction_clause,[status(thm)],[f3891]) ).
fof(f3898,plain,
( ~ sQ33_spl
| member(sK0_skl(sK12_skl(sK14_skl),sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(sK12_skl(sK14_skl),set_type) ),
inference(resolution,[status(thm)],[f2654,f448]) ).
fof(f3899,plain,
( ~ sQ33_spl
| ~ ilf_type(sK0_skl(sK12_skl(sK14_skl),sK15_skl),set_type)
| member(sK12_skl(sK14_skl),range_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f2654,f234]) ).
fof(f3901,definition,
( sQ142_spl
<=> ilf_type(sK12_skl(sK14_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f3903,plain,
( sQ142_spl
| ~ ilf_type(sK12_skl(sK14_skl),set_type) ),
inference(component_clause,[status(thm)],[f3901]) ).
fof(f3904,definition,
( sQ143_spl
<=> member(sK0_skl(sK12_skl(sK14_skl),sK15_skl),domain_of(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f3905,plain,
( ~ sQ143_spl
| member(sK0_skl(sK12_skl(sK14_skl),sK15_skl),domain_of(sK15_skl)) ),
inference(component_clause,[status(thm)],[f3904]) ).
fof(f3907,plain,
( ~ sQ33_spl
| sQ143_spl
| ~ sQ26_spl
| ~ sQ142_spl ),
inference(split_clause,[status(thm)],[f3898,f3901,f2591,f3904,f2653]) ).
fof(f3908,definition,
( sQ144_spl
<=> ilf_type(sK0_skl(sK12_skl(sK14_skl),sK15_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f3910,plain,
( sQ144_spl
| ~ ilf_type(sK0_skl(sK12_skl(sK14_skl),sK15_skl),set_type) ),
inference(component_clause,[status(thm)],[f3908]) ).
fof(f3911,plain,
( ~ sQ33_spl
| ~ sQ144_spl
| sQ32_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f3899,f2591,f2632,f3908,f2653]) ).
fof(f3916,plain,
( sQ142_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3903,f157]) ).
fof(f3917,plain,
sQ142_spl,
inference(contradiction_clause,[status(thm)],[f3916]) ).
fof(f3918,plain,
( sQ144_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3910,f157]) ).
fof(f3919,plain,
sQ144_spl,
inference(contradiction_clause,[status(thm)],[f3918]) ).
fof(f3962,definition,
( sQ150_spl
<=> relation_like(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f3964,plain,
( sQ150_spl
| ~ relation_like(sK15_skl) ),
inference(component_clause,[status(thm)],[f3962]) ).
fof(f3969,plain,
( sQ150_spl
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f3964,f444]) ).
fof(f3971,plain,
( sQ150_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f3969,f2591,f3962]) ).
fof(f3979,plain,
( ~ sQ101_spl
| ~ sQ35_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3451,f2676]) ).
fof(f3996,plain,
( ~ sQ101_spl
| ~ sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f3979]) ).
fof(f4034,plain,
! [X0,X1] :
( ~ sQ143_spl
| sK0_skl(sK12_skl(sK14_skl),sK15_skl) = ordered_pair(sK9_skl(sK0_skl(sK12_skl(sK14_skl),sK15_skl),domain_of(sK15_skl)),sK10_skl(sK0_skl(sK12_skl(sK14_skl),sK15_skl),domain_of(sK15_skl)))
| sK11_skl(domain_of(sK15_skl)) != ordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[f3905,f2761]) ).
fof(f4035,definition,
( sQ151_spl
<=> sK0_skl(sK12_skl(sK14_skl),sK15_skl) = ordered_pair(sK9_skl(sK0_skl(sK12_skl(sK14_skl),sK15_skl),domain_of(sK15_skl)),sK10_skl(sK0_skl(sK12_skl(sK14_skl),sK15_skl),domain_of(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f4038,plain,
( ~ sQ143_spl
| sQ151_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f4034,f3438,f4035,f3904]) ).
fof(f4139,plain,
( member(domain_of(sK15_skl),power_set(sK13_skl))
| ~ ilf_type(sK15_skl,relation_type(sK13_skl,sK14_skl)) ),
inference(paramodulation,[status(thm)],[f2763,f2752]) ).
fof(f4141,definition,
( sQ153_spl
<=> member(domain_of(sK15_skl),power_set(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f4144,plain,
( sQ153_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f4139,f226,f4141]) ).
fof(f4145,plain,
( ~ sQ37_spl
| member(sK0_skl(sK8_skl(sK14_skl),sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(sK8_skl(sK14_skl),set_type) ),
inference(resolution,[status(thm)],[f2702,f448]) ).
fof(f4146,plain,
( ~ sQ37_spl
| ~ ilf_type(sK0_skl(sK8_skl(sK14_skl),sK15_skl),set_type)
| member(sK8_skl(sK14_skl),range_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f2702,f234]) ).
fof(f4148,definition,
( sQ154_spl
<=> ilf_type(sK8_skl(sK14_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f4150,plain,
( sQ154_spl
| ~ ilf_type(sK8_skl(sK14_skl),set_type) ),
inference(component_clause,[status(thm)],[f4148]) ).
fof(f4151,definition,
( sQ155_spl
<=> member(sK0_skl(sK8_skl(sK14_skl),sK15_skl),domain_of(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f4152,plain,
( ~ sQ155_spl
| member(sK0_skl(sK8_skl(sK14_skl),sK15_skl),domain_of(sK15_skl)) ),
inference(component_clause,[status(thm)],[f4151]) ).
fof(f4154,plain,
( ~ sQ37_spl
| sQ155_spl
| ~ sQ26_spl
| ~ sQ154_spl ),
inference(split_clause,[status(thm)],[f4145,f4148,f2591,f4151,f2701]) ).
fof(f4155,definition,
( sQ156_spl
<=> ilf_type(sK0_skl(sK8_skl(sK14_skl),sK15_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f4157,plain,
( sQ156_spl
| ~ ilf_type(sK0_skl(sK8_skl(sK14_skl),sK15_skl),set_type) ),
inference(component_clause,[status(thm)],[f4155]) ).
fof(f4158,plain,
( ~ sQ37_spl
| ~ sQ156_spl
| sQ30_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f4146,f2591,f2625,f4155,f2701]) ).
fof(f4163,plain,
( sQ154_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4150,f157]) ).
fof(f4164,plain,
sQ154_spl,
inference(contradiction_clause,[status(thm)],[f4163]) ).
fof(f4165,plain,
( sQ156_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4157,f157]) ).
fof(f4166,plain,
sQ156_spl,
inference(contradiction_clause,[status(thm)],[f4165]) ).
fof(f4167,plain,
! [X0,X1] :
( ~ sQ155_spl
| sK0_skl(sK8_skl(sK14_skl),sK15_skl) = ordered_pair(sK9_skl(sK0_skl(sK8_skl(sK14_skl),sK15_skl),domain_of(sK15_skl)),sK10_skl(sK0_skl(sK8_skl(sK14_skl),sK15_skl),domain_of(sK15_skl)))
| sK11_skl(domain_of(sK15_skl)) != ordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[f4152,f2761]) ).
fof(f4168,definition,
( sQ158_spl
<=> sK0_skl(sK8_skl(sK14_skl),sK15_skl) = ordered_pair(sK9_skl(sK0_skl(sK8_skl(sK14_skl),sK15_skl),domain_of(sK15_skl)),sK10_skl(sK0_skl(sK8_skl(sK14_skl),sK15_skl),domain_of(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f4171,plain,
( ~ sQ155_spl
| sQ158_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f4167,f3438,f4168,f4151]) ).
fof(f4175,plain,
! [X0] :
( ~ sQ26_spl
| X0 = ordered_pair(sK9_skl(X0,sK15_skl),sK10_skl(X0,sK15_skl))
| ~ member(X0,sK15_skl)
| sK11_skl(sK15_skl) = ordered_pair(sK9_skl(sK11_skl(sK15_skl),sK15_skl),sK10_skl(sK11_skl(sK15_skl),sK15_skl)) ),
inference(resolution,[status(thm)],[f3035,f2693]) ).
fof(f4183,definition,
( sQ159_spl
<=> sK11_skl(sK15_skl) = ordered_pair(sK9_skl(sK11_skl(sK15_skl),sK15_skl),sK10_skl(sK11_skl(sK15_skl),sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f4184,plain,
( ~ sQ159_spl
| sK11_skl(sK15_skl) = ordered_pair(sK9_skl(sK11_skl(sK15_skl),sK15_skl),sK10_skl(sK11_skl(sK15_skl),sK15_skl)) ),
inference(component_clause,[status(thm)],[f4183]) ).
fof(f4186,definition,
! [X0] :
( sQ160_spl
<=> ( X0 = ordered_pair(sK9_skl(X0,sK15_skl),sK10_skl(X0,sK15_skl))
| ~ member(X0,sK15_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f4189,plain,
( ~ sQ26_spl
| sQ160_spl
| sQ159_spl ),
inference(split_clause,[status(thm)],[f4175,f4183,f4186,f2591]) ).
fof(f4201,plain,
( ~ sQ159_spl
| ~ sQ97_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4184,f3403]) ).
fof(f4202,plain,
( ~ sQ159_spl
| ~ sQ97_spl ),
inference(contradiction_clause,[status(thm)],[f4201]) ).
fof(f4224,plain,
! [X0] :
( ~ sQ26_spl
| member(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(sK5_skl(range_of(sK15_skl),X0),set_type)
| member(sK5_skl(range_of(sK15_skl),X0),X0)
| X0 = range_of(sK15_skl) ),
inference(resolution,[status(thm)],[f2667,f448]) ).
fof(f4225,plain,
! [X0] :
( ~ sQ26_spl
| ~ ilf_type(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),set_type)
| member(sK5_skl(range_of(sK15_skl),X0),range_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| member(sK5_skl(range_of(sK15_skl),X0),X0)
| X0 = range_of(sK15_skl) ),
inference(resolution,[status(thm)],[f2667,f234]) ).
fof(f4226,plain,
! [X0,X1,X2] :
( ~ sQ26_spl
| ordered_pair(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),sK5_skl(range_of(sK15_skl),X0)) = ordered_pair(sK9_skl(ordered_pair(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),sK5_skl(range_of(sK15_skl),X0)),sK15_skl),sK10_skl(ordered_pair(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),sK5_skl(range_of(sK15_skl),X0)),sK15_skl))
| sK11_skl(sK15_skl) != ordered_pair(X1,X2)
| member(sK5_skl(range_of(sK15_skl),X0),X0)
| X0 = range_of(sK15_skl) ),
inference(resolution,[status(thm)],[f2667,f2761]) ).
fof(f4227,definition,
! [X0] :
( sQ164_spl
<=> ( member(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(sK5_skl(range_of(sK15_skl),X0),set_type)
| member(sK5_skl(range_of(sK15_skl),X0),X0)
| X0 = range_of(sK15_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f4230,plain,
( ~ sQ26_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f4224,f4227,f2591]) ).
fof(f4231,definition,
! [X0] :
( sQ165_spl
<=> ( ~ ilf_type(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),set_type)
| member(sK5_skl(range_of(sK15_skl),X0),range_of(sK15_skl))
| member(sK5_skl(range_of(sK15_skl),X0),X0)
| X0 = range_of(sK15_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f4234,plain,
( ~ sQ26_spl
| sQ165_spl ),
inference(split_clause,[status(thm)],[f4225,f4231,f2591]) ).
fof(f4235,definition,
! [X0] :
( sQ166_spl
<=> ( ordered_pair(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),sK5_skl(range_of(sK15_skl),X0)) = ordered_pair(sK9_skl(ordered_pair(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),sK5_skl(range_of(sK15_skl),X0)),sK15_skl),sK10_skl(ordered_pair(sK0_skl(sK5_skl(range_of(sK15_skl),X0),sK15_skl),sK5_skl(range_of(sK15_skl),X0)),sK15_skl))
| member(sK5_skl(range_of(sK15_skl),X0),X0)
| X0 = range_of(sK15_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f4238,plain,
( ~ sQ26_spl
| sQ97_spl
| sQ166_spl ),
inference(split_clause,[status(thm)],[f4226,f4235,f3402,f2591]) ).
fof(f4335,definition,
( sQ178_spl
<=> relation_like(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f4337,plain,
( sQ178_spl
| ~ relation_like(sK3_skl) ),
inference(component_clause,[status(thm)],[f4335]) ).
fof(f4360,plain,
( sQ178_spl
| ~ ilf_type(sK3_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f4337,f444]) ).
fof(f4362,plain,
( sQ178_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f4360,f2067,f4335]) ).
fof(f4418,plain,
! [X0] :
( ~ sQ26_spl
| member(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(sK6_skl(X0,range_of(sK15_skl)),set_type)
| subset(range_of(sK15_skl),X0) ),
inference(resolution,[status(thm)],[f2668,f448]) ).
fof(f4419,plain,
! [X0] :
( ~ sQ26_spl
| ~ ilf_type(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),set_type)
| member(sK6_skl(X0,range_of(sK15_skl)),range_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| subset(range_of(sK15_skl),X0) ),
inference(resolution,[status(thm)],[f2668,f234]) ).
fof(f4420,plain,
! [X0,X1,X2] :
( ~ sQ26_spl
| ordered_pair(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),sK6_skl(X0,range_of(sK15_skl))) = ordered_pair(sK9_skl(ordered_pair(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),sK6_skl(X0,range_of(sK15_skl))),sK15_skl),sK10_skl(ordered_pair(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),sK6_skl(X0,range_of(sK15_skl))),sK15_skl))
| sK11_skl(sK15_skl) != ordered_pair(X1,X2)
| subset(range_of(sK15_skl),X0) ),
inference(resolution,[status(thm)],[f2668,f2761]) ).
fof(f4421,definition,
! [X0] :
( sQ189_spl
<=> ( member(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(sK6_skl(X0,range_of(sK15_skl)),set_type)
| subset(range_of(sK15_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f4424,plain,
( ~ sQ26_spl
| sQ189_spl ),
inference(split_clause,[status(thm)],[f4418,f4421,f2591]) ).
fof(f4425,definition,
! [X0] :
( sQ190_spl
<=> ( ~ ilf_type(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),set_type)
| member(sK6_skl(X0,range_of(sK15_skl)),range_of(sK15_skl))
| subset(range_of(sK15_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f4428,plain,
( ~ sQ26_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f4419,f4425,f2591]) ).
fof(f4429,definition,
! [X0] :
( sQ191_spl
<=> ( ordered_pair(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),sK6_skl(X0,range_of(sK15_skl))) = ordered_pair(sK9_skl(ordered_pair(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),sK6_skl(X0,range_of(sK15_skl))),sK15_skl),sK10_skl(ordered_pair(sK0_skl(sK6_skl(X0,range_of(sK15_skl)),sK15_skl),sK6_skl(X0,range_of(sK15_skl))),sK15_skl))
| subset(range_of(sK15_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f4432,plain,
( ~ sQ26_spl
| sQ97_spl
| sQ191_spl ),
inference(split_clause,[status(thm)],[f4420,f4429,f3402,f2591]) ).
fof(f4434,plain,
! [X0] :
( ~ sQ26_spl
| member(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(sK1_skl(X0,range_of(sK15_skl)),set_type)
| range_of(sK15_skl) = X0
| member(sK1_skl(X0,range_of(sK15_skl)),X0) ),
inference(resolution,[status(thm)],[f2671,f448]) ).
fof(f4435,plain,
! [X0] :
( ~ sQ26_spl
| ~ ilf_type(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),set_type)
| member(sK1_skl(X0,range_of(sK15_skl)),range_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| range_of(sK15_skl) = X0
| member(sK1_skl(X0,range_of(sK15_skl)),X0) ),
inference(resolution,[status(thm)],[f2671,f234]) ).
fof(f4436,plain,
! [X0,X1,X2] :
( ~ sQ26_spl
| ordered_pair(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),sK1_skl(X0,range_of(sK15_skl))) = ordered_pair(sK9_skl(ordered_pair(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),sK1_skl(X0,range_of(sK15_skl))),sK15_skl),sK10_skl(ordered_pair(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),sK1_skl(X0,range_of(sK15_skl))),sK15_skl))
| sK11_skl(sK15_skl) != ordered_pair(X1,X2)
| range_of(sK15_skl) = X0
| member(sK1_skl(X0,range_of(sK15_skl)),X0) ),
inference(resolution,[status(thm)],[f2671,f2761]) ).
fof(f4437,definition,
! [X0] :
( sQ192_spl
<=> ( member(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(sK1_skl(X0,range_of(sK15_skl)),set_type)
| range_of(sK15_skl) = X0
| member(sK1_skl(X0,range_of(sK15_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f4440,plain,
( ~ sQ26_spl
| sQ192_spl ),
inference(split_clause,[status(thm)],[f4434,f4437,f2591]) ).
fof(f4441,definition,
! [X0] :
( sQ193_spl
<=> ( ~ ilf_type(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),set_type)
| member(sK1_skl(X0,range_of(sK15_skl)),range_of(sK15_skl))
| range_of(sK15_skl) = X0
| member(sK1_skl(X0,range_of(sK15_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f4444,plain,
( ~ sQ26_spl
| sQ193_spl ),
inference(split_clause,[status(thm)],[f4435,f4441,f2591]) ).
fof(f4445,definition,
! [X0] :
( sQ194_spl
<=> ( ordered_pair(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),sK1_skl(X0,range_of(sK15_skl))) = ordered_pair(sK9_skl(ordered_pair(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),sK1_skl(X0,range_of(sK15_skl))),sK15_skl),sK10_skl(ordered_pair(sK0_skl(sK1_skl(X0,range_of(sK15_skl)),sK15_skl),sK1_skl(X0,range_of(sK15_skl))),sK15_skl))
| range_of(sK15_skl) = X0
| member(sK1_skl(X0,range_of(sK15_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f4448,plain,
( ~ sQ26_spl
| sQ97_spl
| sQ194_spl ),
inference(split_clause,[status(thm)],[f4436,f4445,f3402,f2591]) ).
fof(f4495,plain,
( ~ sQ34_spl
| member(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(sK12_skl(range_of(sK15_skl)),set_type) ),
inference(resolution,[status(thm)],[f2673,f448]) ).
fof(f4496,plain,
( ~ sQ34_spl
| ~ ilf_type(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),set_type)
| member(sK12_skl(range_of(sK15_skl)),range_of(sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f2673,f234]) ).
fof(f4497,plain,
! [X0,X1] :
( ~ sQ34_spl
| ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))) = ordered_pair(sK9_skl(ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))),sK15_skl),sK10_skl(ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))),sK15_skl))
| sK11_skl(sK15_skl) != ordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[f2673,f2761]) ).
fof(f4498,definition,
( sQ203_spl
<=> ilf_type(sK12_skl(range_of(sK15_skl)),set_type) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f4500,plain,
( sQ203_spl
| ~ ilf_type(sK12_skl(range_of(sK15_skl)),set_type) ),
inference(component_clause,[status(thm)],[f4498]) ).
fof(f4501,definition,
( sQ204_spl
<=> member(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f4502,plain,
( ~ sQ204_spl
| member(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl)) ),
inference(component_clause,[status(thm)],[f4501]) ).
fof(f4504,plain,
( ~ sQ34_spl
| sQ204_spl
| ~ sQ26_spl
| ~ sQ203_spl ),
inference(split_clause,[status(thm)],[f4495,f4498,f2591,f4501,f2672]) ).
fof(f4505,definition,
( sQ205_spl
<=> member(sK12_skl(range_of(sK15_skl)),range_of(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f4506,plain,
( ~ sQ205_spl
| member(sK12_skl(range_of(sK15_skl)),range_of(sK15_skl)) ),
inference(component_clause,[status(thm)],[f4505]) ).
fof(f4508,definition,
( sQ206_spl
<=> ilf_type(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f4510,plain,
( sQ206_spl
| ~ ilf_type(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),set_type) ),
inference(component_clause,[status(thm)],[f4508]) ).
fof(f4511,plain,
( ~ sQ34_spl
| ~ sQ206_spl
| sQ205_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f4496,f2591,f4505,f4508,f2672]) ).
fof(f4512,definition,
( sQ207_spl
<=> ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))) = ordered_pair(sK9_skl(ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))),sK15_skl),sK10_skl(ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))),sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f4515,plain,
( ~ sQ34_spl
| sQ207_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f4497,f3402,f4512,f2672]) ).
fof(f4516,plain,
( sQ203_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4500,f157]) ).
fof(f4517,plain,
sQ203_spl,
inference(contradiction_clause,[status(thm)],[f4516]) ).
fof(f4518,plain,
( sQ206_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4510,f157]) ).
fof(f4519,plain,
sQ206_spl,
inference(contradiction_clause,[status(thm)],[f4518]) ).
fof(f4532,plain,
( ~ sQ205_spl
| member(ordered_pair(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),sK12_skl(range_of(sK15_skl))),sK15_skl)
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f4506,f233]) ).
fof(f4533,plain,
! [X0,X1] :
( ~ sQ205_spl
| sK12_skl(range_of(sK15_skl)) = ordered_pair(sK9_skl(sK12_skl(range_of(sK15_skl)),range_of(sK15_skl)),sK10_skl(sK12_skl(range_of(sK15_skl)),range_of(sK15_skl)))
| sK11_skl(range_of(sK15_skl)) != ordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[f4506,f2761]) ).
fof(f4534,plain,
( ~ sQ205_spl
| sQ34_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f4532,f2591,f2672,f4505]) ).
fof(f4535,definition,
( sQ210_spl
<=> sK12_skl(range_of(sK15_skl)) = ordered_pair(sK9_skl(sK12_skl(range_of(sK15_skl)),range_of(sK15_skl)),sK10_skl(sK12_skl(range_of(sK15_skl)),range_of(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f4538,plain,
( ~ sQ205_spl
| sQ210_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f4533,f3462,f4535,f4505]) ).
fof(f4544,plain,
! [X0,X1] :
( ~ sQ204_spl
| sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl) = ordered_pair(sK9_skl(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl)),sK10_skl(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl)))
| sK11_skl(domain_of(sK15_skl)) != ordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[f4502,f2761]) ).
fof(f4545,definition,
( sQ212_spl
<=> sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl) = ordered_pair(sK9_skl(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl)),sK10_skl(sK0_skl(sK12_skl(range_of(sK15_skl)),sK15_skl),domain_of(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f4548,plain,
( ~ sQ204_spl
| sQ212_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f4544,f3438,f4545,f4501]) ).
fof(f4592,plain,
( sQ46_spl
| subset(range_of(sK15_skl),sK14_skl)
| ~ member(range_of(sK15_skl),power_set(sK14_skl)) ),
inference(resolution,[status(thm)],[f2863,f2407]) ).
fof(f4597,plain,
( sQ46_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f4592,f3226,f2801]) ).
fof(f4602,plain,
$false,
inference(sat_refutation,[status(thm)],[f175,f179,f190,f198,f202,f215,f2052,f2082,f2084,f2086,f2494,f2514,f2580,f2594,f2598,f2631,f2635,f2656,f2658,f2666,f2678,f2688,f2704,f2772,f2791,f2804,f2836,f2912,f3229,f3233,f3271,f3274,f3296,f3357,f3361,f3386,f3394,f3398,f3405,f3408,f3441,f3468,f3475,f3481,f3485,f3554,f3728,f3858,f3860,f3892,f3907,f3911,f3917,f3919,f3971,f3996,f4038,f4144,f4154,f4158,f4164,f4166,f4171,f4189,f4202,f4230,f4234,f4238,f4362,f4424,f4428,f4432,f4440,f4444,f4448,f4504,f4511,f4515,f4517,f4519,f4534,f4538,f4548,f4597]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET660+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n018.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 05:33:44 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 1.14/0.60 % Refutation found
% 1.14/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.14/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.14/0.63 % Elapsed time: 0.250266 seconds
% 1.14/0.63 % CPU time: 1.682541 seconds
% 1.14/0.63 % Total memory used: 131.970 MB
% 1.14/0.63 % Net memory used: 129.533 MB
%------------------------------------------------------------------------------