%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET684+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 : n014.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:26 PM UTC 2026
% Result : Theorem 0.14s 5.45s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 62
% Syntax : Number of formulae : 291 ( 32 unt; 48 def)
% Number of atoms : 1002 ( 66 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 1223 ( 512 ~; 511 |; 84 &)
% ( 60 <=>; 55 =>; 0 <=; 1 <~>)
% Maximal formula depth : 24 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 54 ( 52 usr; 49 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 10 con; 0-5 aty)
% Number of variables : 423 ( 391 !; 32 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,binary_relation_type)
=> ! [E] :
( ilf_type(E,binary_relation_type)
=> ( member(ordered_pair(B,C),compose(D,E))
<=> ? [F] :
( member(ordered_pair(F,C),E)
& member(ordered_pair(B,F),D)
& ilf_type(F,set_type) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,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,relation_type(B,C))
=> ( member(ordered_pair(D,E),F)
=> ( member(E,C)
& member(D,B) ) ) ) ) ) ) ),
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,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(f5,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(f6,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ? [D] : ilf_type(D,relation_type(C,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,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(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(f18,axiom,
! [B] :
( ilf_type(B,set_type)
=> ? [C] : ilf_type(C,subset_type(B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,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(f26,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(f27,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ! [F] :
( ilf_type(F,relation_type(C,D))
=> compose5(B,C,D,E,F) = compose(E,F) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ! [F] :
( ilf_type(F,relation_type(C,D))
=> ilf_type(compose5(B,C,D,E,F),relation_type(B,D)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [B] : ilf_type(B,set_type),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,conjecture,
! [B] :
( ( ilf_type(B,set_type)
& ~ empty(B) )
=> ! [C] :
( ( ilf_type(C,set_type)
& ~ empty(C) )
=> ! [D] :
( ( ilf_type(D,set_type)
& ~ empty(D) )
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ! [F] :
( ilf_type(F,relation_type(C,D))
=> ! [G] :
( ilf_type(G,member_type(B))
=> ! [H] :
( ilf_type(H,member_type(D))
=> ( member(ordered_pair(G,H),compose5(B,C,D,E,F))
<=> ? [I] :
( member(ordered_pair(I,H),F)
& member(ordered_pair(G,I),E)
& ilf_type(I,member_type(C)) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
~ ! [B] :
( ( ilf_type(B,set_type)
& ~ empty(B) )
=> ! [C] :
( ( ilf_type(C,set_type)
& ~ empty(C) )
=> ! [D] :
( ( ilf_type(D,set_type)
& ~ empty(D) )
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ! [F] :
( ilf_type(F,relation_type(C,D))
=> ! [G] :
( ilf_type(G,member_type(B))
=> ! [H] :
( ilf_type(H,member_type(D))
=> ( member(ordered_pair(G,H),compose5(B,C,D,E,F))
<=> ? [I] :
( member(ordered_pair(I,H),F)
& member(ordered_pair(G,I),E)
& ilf_type(I,member_type(C)) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
fof(f32,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ( member(ordered_pair(B,C),compose(D,E))
<=> ? [F] :
( member(ordered_pair(F,C),E)
& member(ordered_pair(B,F),D)
& ilf_type(F,set_type) ) )
| ~ ilf_type(E,binary_relation_type) )
| ~ ilf_type(D,binary_relation_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f33,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ( ( ! [F] :
( ~ member(ordered_pair(F,C),E)
| ~ member(ordered_pair(B,F),D)
| ~ ilf_type(F,set_type) )
| member(ordered_pair(B,C),compose(D,E)) )
& ( ? [F] :
( member(ordered_pair(F,C),E)
& member(ordered_pair(B,F),D)
& ilf_type(F,set_type) )
| ~ member(ordered_pair(B,C),compose(D,E)) ) )
| ~ ilf_type(E,binary_relation_type) )
| ~ ilf_type(D,binary_relation_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f32]) ).
fof(f34,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ( ( ! [F] :
( ~ member(ordered_pair(F,C),E)
| ~ member(ordered_pair(B,F),D)
| ~ ilf_type(F,set_type) )
| member(ordered_pair(B,C),compose(D,E)) )
& ( ( member(ordered_pair(sK0_skl(E,D,C,B),C),E)
& member(ordered_pair(B,sK0_skl(E,D,C,B)),D)
& ilf_type(sK0_skl(E,D,C,B),set_type) )
| ~ member(ordered_pair(B,C),compose(D,E)) ) )
| ~ ilf_type(E,binary_relation_type) )
| ~ ilf_type(D,binary_relation_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(F,sK0_skl(E,D,C,B))],[f33]) ).
fof(f36,plain,
! [X0,X1,X2,X3] :
( member(ordered_pair(X0,sK0_skl(X3,X2,X1,X0)),X2)
| ~ member(ordered_pair(X0,X1),compose(X2,X3))
| ~ ilf_type(X3,binary_relation_type)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f37,plain,
! [X0,X1,X2,X3] :
( member(ordered_pair(sK0_skl(X3,X2,X1,X0),X1),X3)
| ~ member(ordered_pair(X0,X1),compose(X2,X3))
| ~ ilf_type(X3,binary_relation_type)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f38,plain,
! [X0,X1,X2,X3,X4] :
( ~ member(ordered_pair(X4,X1),X3)
| ~ member(ordered_pair(X0,X4),X2)
| ~ ilf_type(X4,set_type)
| member(ordered_pair(X0,X1),compose(X2,X3))
| ~ ilf_type(X3,binary_relation_type)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f39,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( ( member(E,C)
& member(D,B) )
| ~ member(ordered_pair(D,E),F)
| ~ ilf_type(F,relation_type(B,C)) )
| ~ 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)],[f2]) ).
fof(f40,plain,
! [X0,X1,X2,X3,X4] :
( member(X2,X0)
| ~ member(ordered_pair(X2,X3),X4)
| ~ ilf_type(X4,relation_type(X0,X1))
| ~ 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)],[f39]) ).
fof(f42,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)],[f3]) ).
fof(f43,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)],[f42]) ).
fof(f44,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)],[f43]) ).
fof(f45,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)],[f44]) ).
fof(f46,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)],[f44]) ).
fof(f49,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)],[f5]) ).
fof(f50,plain,
! [X0,X1,X2] :
( ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X2,subset_type(cross_product(X0,X1)))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,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)],[f49]) ).
fof(f52,plain,
! [B] :
( ! [C] :
( ? [D] : ilf_type(D,relation_type(C,B))
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f53,plain,
! [B] :
( ! [C] :
( ilf_type(sK1_skl(C,B),relation_type(C,B))
| ~ 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))],[f52]) ).
fof(f54,plain,
! [X0,X1] :
( ilf_type(sK1_skl(X1,X0),relation_type(X1,X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f55,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)],[f7]) ).
fof(f56,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)],[f55]) ).
fof(f57,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)],[f56]) ).
fof(f58,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)],[f56]) ).
fof(f78,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(f79,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)],[f78]) ).
fof(f82,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)],[f79]) ).
fof(f89,plain,
! [B] :
( ? [C] : ilf_type(C,subset_type(B))
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f90,plain,
! [B] :
( ilf_type(sK5_skl(B),subset_type(B))
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(C,sK5_skl(B))],[f89]) ).
fof(f91,plain,
! [X0] :
( ilf_type(sK5_skl(X0),subset_type(X0))
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f114,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)],[f24]) ).
fof(f115,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)],[f114]) ).
fof(f116,plain,
! [B] :
( ( ( ( ! [D] :
( ! [E] :
( sK10_skl(B) != ordered_pair(D,E)
| ~ ilf_type(E,set_type) )
| ~ ilf_type(D,set_type) )
& member(sK10_skl(B),B)
& ilf_type(sK10_skl(B),set_type) )
| relation_like(B) )
& ( ! [C] :
( ( C = ordered_pair(sK8_skl(C,B),sK9_skl(C,B))
& ilf_type(sK9_skl(C,B),set_type)
& ilf_type(sK8_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,[sK8_skl,sK9_skl,sK10_skl]),skolemize(D,sK8_skl(C,B)),skolemize(E,sK9_skl(C,B)),skolemize(C,sK10_skl(B))],[f115]) ).
fof(f119,plain,
! [X0,X1] :
( X1 = ordered_pair(sK8_skl(X1,X0),sK9_skl(X1,X0))
| ~ member(X1,X0)
| ~ ilf_type(X1,set_type)
| ~ relation_like(X0)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f122,plain,
! [X0,X1,X2] :
( sK10_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)],[f116]) ).
fof(f125,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)],[f26]) ).
fof(f126,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)],[f125]) ).
fof(f127,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( compose5(B,C,D,E,F) = compose(E,F)
| ~ ilf_type(F,relation_type(C,D)) )
| ~ ilf_type(E,relation_type(B,C)) )
| ~ ilf_type(D,set_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f128,plain,
! [X0,X1,X2,X3,X4] :
( compose5(X0,X1,X2,X3,X4) = compose(X3,X4)
| ~ ilf_type(X4,relation_type(X1,X2))
| ~ ilf_type(X3,relation_type(X0,X1))
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( ilf_type(compose5(B,C,D,E,F),relation_type(B,D))
| ~ ilf_type(F,relation_type(C,D)) )
| ~ ilf_type(E,relation_type(B,C)) )
| ~ ilf_type(D,set_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f130,plain,
! [X0,X1,X2,X3,X4] :
( ilf_type(compose5(X0,X1,X2,X3,X4),relation_type(X0,X2))
| ~ ilf_type(X4,relation_type(X1,X2))
| ~ ilf_type(X3,relation_type(X0,X1))
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f131,plain,
! [X0] : ilf_type(X0,set_type),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f132,plain,
? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ? [G] :
( ? [H] :
( ( member(ordered_pair(G,H),compose5(B,C,D,E,F))
<~> ? [I] :
( member(ordered_pair(I,H),F)
& member(ordered_pair(G,I),E)
& ilf_type(I,member_type(C)) ) )
& ilf_type(H,member_type(D)) )
& ilf_type(G,member_type(B)) )
& ilf_type(F,relation_type(C,D)) )
& ilf_type(E,relation_type(B,C)) )
& ilf_type(D,set_type)
& ~ empty(D) )
& ilf_type(C,set_type)
& ~ empty(C) )
& ilf_type(B,set_type)
& ~ empty(B) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f133,plain,
? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ? [G] :
( ? [H] :
( ( ! [I] :
( ~ member(ordered_pair(I,H),F)
| ~ member(ordered_pair(G,I),E)
| ~ ilf_type(I,member_type(C)) )
| ~ member(ordered_pair(G,H),compose5(B,C,D,E,F)) )
& ( ? [I] :
( member(ordered_pair(I,H),F)
& member(ordered_pair(G,I),E)
& ilf_type(I,member_type(C)) )
| member(ordered_pair(G,H),compose5(B,C,D,E,F)) )
& ilf_type(H,member_type(D)) )
& ilf_type(G,member_type(B)) )
& ilf_type(F,relation_type(C,D)) )
& ilf_type(E,relation_type(B,C)) )
& ilf_type(D,set_type)
& ~ empty(D) )
& ilf_type(C,set_type)
& ~ empty(C) )
& ilf_type(B,set_type)
& ~ empty(B) ),
inference(NNF_transformation,[status(thm)],[f132]) ).
fof(f134,plain,
( ( ! [I] :
( ~ member(ordered_pair(I,sK17_skl),sK15_skl)
| ~ member(ordered_pair(sK16_skl,I),sK14_skl)
| ~ ilf_type(I,member_type(sK12_skl)) )
| ~ member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl)) )
& ( ( member(ordered_pair(sK18_skl,sK17_skl),sK15_skl)
& member(ordered_pair(sK16_skl,sK18_skl),sK14_skl)
& ilf_type(sK18_skl,member_type(sK12_skl)) )
| member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl)) )
& ilf_type(sK17_skl,member_type(sK13_skl))
& ilf_type(sK16_skl,member_type(sK11_skl))
& ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))
& ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl))
& ilf_type(sK13_skl,set_type)
& ~ empty(sK13_skl)
& ilf_type(sK12_skl,set_type)
& ~ empty(sK12_skl)
& ilf_type(sK11_skl,set_type)
& ~ empty(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl]),skolemize(B,sK11_skl),skolemize(C,sK12_skl),skolemize(D,sK13_skl),skolemize(E,sK14_skl),skolemize(F,sK15_skl),skolemize(G,sK16_skl),skolemize(H,sK17_skl),skolemize(I,sK18_skl)],[f133]) ).
fof(f135,plain,
~ empty(sK11_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f137,plain,
~ empty(sK12_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f139,plain,
~ empty(sK13_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f141,plain,
ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl)),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f142,plain,
ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl)),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f143,plain,
ilf_type(sK16_skl,member_type(sK11_skl)),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f144,plain,
ilf_type(sK17_skl,member_type(sK13_skl)),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f146,plain,
( member(ordered_pair(sK16_skl,sK18_skl),sK14_skl)
| member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl)) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f147,plain,
( member(ordered_pair(sK18_skl,sK17_skl),sK15_skl)
| member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl)) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f148,plain,
! [X0] :
( ~ member(ordered_pair(X0,sK17_skl),sK15_skl)
| ~ member(ordered_pair(sK16_skl,X0),sK14_skl)
| ~ ilf_type(X0,member_type(sK12_skl))
| ~ member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl)) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f149,definition,
! [X0] :
( sQ0_spl
<=> ~ ilf_type(X0,set_type) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f150,plain,
! [X0] :
( ~ sQ0_spl
| ~ ilf_type(X0,set_type) ),
inference(component_clause,[status(thm)],[f149]) ).
fof(f152,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(f155,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f45,f149,f152]) ).
fof(f156,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(f159,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f46,f149,f156]) ).
fof(f160,definition,
( sQ3_spl
<=> member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f161,plain,
( ~ sQ3_spl
| member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f160]) ).
fof(f162,plain,
( sQ3_spl
| ~ member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f160]) ).
fof(f167,definition,
( sQ5_spl
<=> member(ordered_pair(sK16_skl,sK18_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f168,plain,
( ~ sQ5_spl
| member(ordered_pair(sK16_skl,sK18_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f167]) ).
fof(f170,plain,
( sQ5_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f146,f160,f167]) ).
fof(f171,definition,
( sQ6_spl
<=> member(ordered_pair(sK18_skl,sK17_skl),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f172,plain,
( ~ sQ6_spl
| member(ordered_pair(sK18_skl,sK17_skl),sK15_skl) ),
inference(component_clause,[status(thm)],[f171]) ).
fof(f174,plain,
( sQ6_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f147,f160,f171]) ).
fof(f175,definition,
! [X0] :
( sQ7_spl
<=> ( ~ member(ordered_pair(X0,sK17_skl),sK15_skl)
| ~ member(ordered_pair(sK16_skl,X0),sK14_skl)
| ~ ilf_type(X0,member_type(sK12_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f176,plain,
! [X0] :
( ~ sQ7_spl
| ~ member(ordered_pair(X0,sK17_skl),sK15_skl)
| ~ member(ordered_pair(sK16_skl,X0),sK14_skl)
| ~ ilf_type(X0,member_type(sK12_skl)) ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f178,plain,
( sQ7_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f148,f160,f175]) ).
fof(f179,plain,
! [X0] :
( ~ relation_like(X0)
| ilf_type(X0,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(duplicate_literals_removal,[status(thm)],[f82]) ).
fof(f180,plain,
! [X0,X1,X2,X3,X4] :
( member(X1,X4)
| ~ member(ordered_pair(X1,X2),X3)
| ~ ilf_type(X3,relation_type(X4,X0))
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f40,f131]) ).
fof(f182,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)],[f57,f131]) ).
fof(f183,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f150,f131]) ).
fof(f184,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f183]) ).
fof(f187,plain,
! [X0,X1,X2,X3] :
( member(ordered_pair(X3,sK0_skl(X2,X1,X0,X3)),X1)
| ~ member(ordered_pair(X3,X0),compose(X1,X2))
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f36,f131]) ).
fof(f188,plain,
! [X0,X1,X2,X3] :
( member(ordered_pair(sK0_skl(X2,X1,X0,X3),X0),X2)
| ~ member(ordered_pair(X3,X0),compose(X1,X2))
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f37,f131]) ).
fof(f189,plain,
! [X0,X1,X2,X3,X4] :
( ~ member(ordered_pair(X4,X0),X2)
| ~ member(ordered_pair(X3,X4),X1)
| ~ ilf_type(X4,set_type)
| member(ordered_pair(X3,X0),compose(X1,X2))
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f38,f131]) ).
fof(f190,plain,
! [X0,X1,X2] :
( ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X1,subset_type(cross_product(X2,X0)))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f50,f131]) ).
fof(f191,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)],[f51,f131]) ).
fof(f192,plain,
( ilf_type(sK14_skl,subset_type(cross_product(sK11_skl,sK12_skl)))
| ~ ilf_type(sK12_skl,set_type) ),
inference(resolution,[status(thm)],[f141,f191]) ).
fof(f193,definition,
( sQ8_spl
<=> ilf_type(sK12_skl,set_type) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f195,plain,
( sQ8_spl
| ~ ilf_type(sK12_skl,set_type) ),
inference(component_clause,[status(thm)],[f193]) ).
fof(f196,definition,
( sQ9_spl
<=> ilf_type(sK14_skl,subset_type(cross_product(sK11_skl,sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f197,plain,
( ~ sQ9_spl
| ilf_type(sK14_skl,subset_type(cross_product(sK11_skl,sK12_skl))) ),
inference(component_clause,[status(thm)],[f196]) ).
fof(f199,plain,
( sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f192,f193,f196]) ).
fof(f200,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f195,f131]) ).
fof(f201,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f200]) ).
fof(f202,plain,
( ilf_type(sK15_skl,subset_type(cross_product(sK12_skl,sK13_skl)))
| ~ ilf_type(sK13_skl,set_type) ),
inference(resolution,[status(thm)],[f142,f191]) ).
fof(f203,definition,
( sQ10_spl
<=> ilf_type(sK13_skl,set_type) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f205,plain,
( sQ10_spl
| ~ ilf_type(sK13_skl,set_type) ),
inference(component_clause,[status(thm)],[f203]) ).
fof(f206,definition,
( sQ11_spl
<=> ilf_type(sK15_skl,subset_type(cross_product(sK12_skl,sK13_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f207,plain,
( ~ sQ11_spl
| ilf_type(sK15_skl,subset_type(cross_product(sK12_skl,sK13_skl))) ),
inference(component_clause,[status(thm)],[f206]) ).
fof(f209,plain,
( sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f202,f203,f206]) ).
fof(f210,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f205,f131]) ).
fof(f211,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f210]) ).
fof(f212,plain,
( member(sK16_skl,sK11_skl)
| ~ ilf_type(sK11_skl,set_type)
| empty(sK11_skl) ),
inference(resolution,[status(thm)],[f143,f182]) ).
fof(f213,definition,
( sQ12_spl
<=> empty(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f214,plain,
( ~ sQ12_spl
| empty(sK11_skl) ),
inference(component_clause,[status(thm)],[f213]) ).
fof(f216,definition,
( sQ13_spl
<=> ilf_type(sK11_skl,set_type) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f218,plain,
( sQ13_spl
| ~ ilf_type(sK11_skl,set_type) ),
inference(component_clause,[status(thm)],[f216]) ).
fof(f219,definition,
( sQ14_spl
<=> member(sK16_skl,sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f220,plain,
( ~ sQ14_spl
| member(sK16_skl,sK11_skl) ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f222,plain,
( sQ14_spl
| ~ sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f212,f213,f216,f219]) ).
fof(f223,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)],[f58,f131]) ).
fof(f224,plain,
! [X0,X1] :
( ~ member(X1,X0)
| ilf_type(X1,member_type(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f223,f131]) ).
fof(f226,plain,
! [X0,X1,X2,X3,X4] :
( compose5(X3,X0,X1,X2,X4) = compose(X2,X4)
| ~ ilf_type(X4,relation_type(X0,X1))
| ~ ilf_type(X2,relation_type(X3,X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f128,f131]) ).
fof(f227,plain,
! [X0,X1,X2,X3,X4] :
( compose5(X2,X0,X4,X1,X3) = compose(X1,X3)
| ~ ilf_type(X3,relation_type(X0,X4))
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f226,f131]) ).
fof(f228,plain,
! [X0,X1,X2,X3,X4] :
( compose5(X1,X2,X4,X0,X3) = compose(X0,X3)
| ~ ilf_type(X3,relation_type(X2,X4))
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[f227,f131]) ).
fof(f229,plain,
! [X0,X1,X2,X3,X4] :
( ilf_type(compose5(X3,X0,X1,X2,X4),relation_type(X3,X1))
| ~ ilf_type(X4,relation_type(X0,X1))
| ~ ilf_type(X2,relation_type(X3,X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f130,f131]) ).
fof(f230,plain,
! [X0,X1,X2,X3,X4] :
( ilf_type(compose5(X3,X0,X1,X2,X4),subset_type(cross_product(X3,X1)))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X4,relation_type(X0,X1))
| ~ ilf_type(X2,relation_type(X3,X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f229,f191]) ).
fof(f231,plain,
! [X0,X1,X2,X3,X4] :
( ilf_type(compose5(X3,X0,X1,X2,X4),subset_type(cross_product(X3,X1)))
| ~ ilf_type(X4,relation_type(X0,X1))
| ~ ilf_type(X2,relation_type(X3,X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(duplicate_literals_removal,[status(thm)],[f230]) ).
fof(f232,plain,
! [X0,X1,X2,X3,X4] :
( ilf_type(compose5(X2,X3,X0,X1,X4),subset_type(cross_product(X2,X0)))
| ~ ilf_type(X4,relation_type(X3,X0))
| ~ ilf_type(X1,relation_type(X2,X3))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f231,f131]) ).
fof(f233,plain,
( member(sK17_skl,sK13_skl)
| ~ ilf_type(sK13_skl,set_type)
| empty(sK13_skl) ),
inference(resolution,[status(thm)],[f144,f182]) ).
fof(f234,definition,
( sQ15_spl
<=> empty(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f235,plain,
( ~ sQ15_spl
| empty(sK13_skl) ),
inference(component_clause,[status(thm)],[f234]) ).
fof(f237,definition,
( sQ16_spl
<=> member(sK17_skl,sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f238,plain,
( ~ sQ16_spl
| member(sK17_skl,sK13_skl) ),
inference(component_clause,[status(thm)],[f237]) ).
fof(f240,plain,
( sQ16_spl
| ~ sQ10_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f233,f234,f203,f237]) ).
fof(f241,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f235,f139]) ).
fof(f242,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f241]) ).
fof(f244,plain,
! [X0,X1] :
( ilf_type(sK1_skl(X0,X1),relation_type(X0,X1))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f54,f131]) ).
fof(f245,plain,
! [X0,X1] :
( ilf_type(sK1_skl(X0,X1),subset_type(cross_product(X0,X1)))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f244,f191]) ).
fof(f246,plain,
! [X0,X1] :
( ilf_type(sK1_skl(X1,X0),subset_type(cross_product(X1,X0)))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f245,f131]) ).
fof(f252,plain,
( ~ sQ9_spl
| ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl))
| ~ ilf_type(sK12_skl,set_type) ),
inference(resolution,[status(thm)],[f197,f190]) ).
fof(f253,definition,
( sQ17_spl
<=> ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f256,plain,
( ~ sQ9_spl
| sQ17_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f252,f193,f253,f196]) ).
fof(f260,definition,
( sQ18_spl
<=> ilf_type(sK17_skl,set_type) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f262,plain,
( sQ18_spl
| ~ ilf_type(sK17_skl,set_type) ),
inference(component_clause,[status(thm)],[f260]) ).
fof(f269,definition,
( sQ21_spl
<=> ilf_type(sK16_skl,set_type) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f271,plain,
( sQ21_spl
| ~ ilf_type(sK16_skl,set_type) ),
inference(component_clause,[status(thm)],[f269]) ).
fof(f281,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f262,f131]) ).
fof(f282,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f281]) ).
fof(f283,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f271,f131]) ).
fof(f284,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f283]) ).
fof(f287,plain,
( ~ sQ11_spl
| ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))
| ~ ilf_type(sK13_skl,set_type) ),
inference(resolution,[status(thm)],[f207,f190]) ).
fof(f288,definition,
( sQ24_spl
<=> ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f291,plain,
( ~ sQ11_spl
| sQ24_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f287,f203,f288,f206]) ).
fof(f297,plain,
! [X0,X1,X2,X3] :
( ~ ilf_type(X2,set_type)
| compose5(X1,X2,X3,X0,sK1_skl(X2,X3)) = compose(X0,sK1_skl(X2,X3))
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(resolution,[status(thm)],[f228,f244]) ).
fof(f299,plain,
! [X0,X1] :
( compose5(X1,sK12_skl,sK13_skl,X0,sK15_skl) = compose(X0,sK15_skl)
| ~ ilf_type(X0,relation_type(X1,sK12_skl)) ),
inference(resolution,[status(thm)],[f228,f142]) ).
fof(f300,plain,
! [X0,X1] :
( compose5(X1,sK11_skl,sK12_skl,X0,sK14_skl) = compose(X0,sK14_skl)
| ~ ilf_type(X0,relation_type(X1,sK11_skl)) ),
inference(resolution,[status(thm)],[f228,f141]) ).
fof(f301,plain,
! [X0,X1,X2,X3] :
( compose5(X1,X2,X3,X0,sK1_skl(X2,X3)) = compose(X0,sK1_skl(X2,X3))
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[f297,f131]) ).
fof(f306,plain,
! [X0] :
( ~ relation_like(X0)
| ilf_type(X0,binary_relation_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f179,f131]) ).
fof(f316,plain,
! [X0,X1,X2,X3,X4] :
( ilf_type(compose5(X1,X2,X4,X0,X3),subset_type(cross_product(X1,X4)))
| ~ ilf_type(X3,relation_type(X2,X4))
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[f232,f131]) ).
fof(f319,plain,
! [X0,X1] : ilf_type(sK1_skl(X0,X1),subset_type(cross_product(X0,X1))),
inference(forward_subsumption_resolution,[status(thm)],[f246,f131]) ).
fof(f320,plain,
! [X0,X1] :
( ilf_type(sK1_skl(X1,X0),relation_type(X1,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f319,f190]) ).
fof(f321,plain,
! [X0,X1] : ilf_type(sK1_skl(X0,X1),relation_type(X0,X1)),
inference(forward_subsumption_resolution,[status(thm)],[f320,f131]) ).
fof(f324,plain,
! [X0] : ilf_type(sK5_skl(X0),subset_type(X0)),
inference(forward_subsumption_resolution,[status(thm)],[f91,f131]) ).
fof(f325,plain,
! [X0,X1] :
( ilf_type(sK5_skl(cross_product(X1,X0)),relation_type(X1,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f324,f190]) ).
fof(f326,plain,
! [X0,X1] : ilf_type(sK5_skl(cross_product(X0,X1)),relation_type(X0,X1)),
inference(forward_subsumption_resolution,[status(thm)],[f325,f131]) ).
fof(f338,plain,
! [X0] : compose5(X0,sK12_skl,sK13_skl,sK5_skl(cross_product(X0,sK12_skl)),sK15_skl) = compose(sK5_skl(cross_product(X0,sK12_skl)),sK15_skl),
inference(resolution,[status(thm)],[f299,f326]) ).
fof(f339,plain,
! [X0] : compose5(X0,sK12_skl,sK13_skl,sK1_skl(X0,sK12_skl),sK15_skl) = compose(sK1_skl(X0,sK12_skl),sK15_skl),
inference(resolution,[status(thm)],[f299,f321]) ).
fof(f340,plain,
! [X0,X1,X2,X3] :
( ~ ilf_type(X3,relation_type(X1,sK12_skl))
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(sK12_skl,set_type)
| ~ ilf_type(X1,set_type)
| compose5(X0,sK12_skl,sK13_skl,compose5(X0,X1,sK12_skl,X2,X3),sK15_skl) = compose(compose5(X0,X1,sK12_skl,X2,X3),sK15_skl) ),
inference(resolution,[status(thm)],[f299,f229]) ).
fof(f341,plain,
compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl) = compose(sK14_skl,sK15_skl),
inference(resolution,[status(thm)],[f299,f141]) ).
fof(f342,definition,
! [X0,X1,X2,X3] :
( sQ25_spl
<=> ( ~ ilf_type(X3,relation_type(X1,sK12_skl))
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| compose5(X0,sK12_skl,sK13_skl,compose5(X0,X1,sK12_skl,X2,X3),sK15_skl) = compose(compose5(X0,X1,sK12_skl,X2,X3),sK15_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f345,plain,
( ~ sQ8_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f340,f342,f193]) ).
fof(f347,plain,
! [X0] : compose5(X0,sK11_skl,sK12_skl,sK5_skl(cross_product(X0,sK11_skl)),sK14_skl) = compose(sK5_skl(cross_product(X0,sK11_skl)),sK14_skl),
inference(resolution,[status(thm)],[f300,f326]) ).
fof(f348,plain,
! [X0] : compose5(X0,sK11_skl,sK12_skl,sK1_skl(X0,sK11_skl),sK14_skl) = compose(sK1_skl(X0,sK11_skl),sK14_skl),
inference(resolution,[status(thm)],[f300,f321]) ).
fof(f349,plain,
! [X0,X1,X2,X3] :
( ~ ilf_type(X3,relation_type(X1,sK11_skl))
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(sK11_skl,set_type)
| ~ ilf_type(X1,set_type)
| compose5(X0,sK11_skl,sK12_skl,compose5(X0,X1,sK11_skl,X2,X3),sK14_skl) = compose(compose5(X0,X1,sK11_skl,X2,X3),sK14_skl) ),
inference(resolution,[status(thm)],[f300,f229]) ).
fof(f350,definition,
! [X0,X1,X2,X3] :
( sQ26_spl
<=> ( ~ ilf_type(X3,relation_type(X1,sK11_skl))
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| compose5(X0,sK11_skl,sK12_skl,compose5(X0,X1,sK11_skl,X2,X3),sK14_skl) = compose(compose5(X0,X1,sK11_skl,X2,X3),sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f353,plain,
( ~ sQ13_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f349,f350,f216]) ).
fof(f354,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f218,f131]) ).
fof(f355,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f354]) ).
fof(f357,plain,
( ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f214,f135]) ).
fof(f358,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f357]) ).
fof(f372,plain,
! [X0] : compose5(sK12_skl,sK13_skl,X0,sK15_skl,sK1_skl(sK13_skl,X0)) = compose(sK15_skl,sK1_skl(sK13_skl,X0)),
inference(resolution,[status(thm)],[f301,f142]) ).
fof(f373,plain,
! [X0] : compose5(sK11_skl,sK12_skl,X0,sK14_skl,sK1_skl(sK12_skl,X0)) = compose(sK14_skl,sK1_skl(sK12_skl,X0)),
inference(resolution,[status(thm)],[f301,f141]) ).
fof(f410,plain,
! [X0,X1] :
( X1 = ordered_pair(sK8_skl(X1,X0),sK9_skl(X1,X0))
| ~ member(X1,X0)
| ~ ilf_type(X1,set_type)
| ~ relation_like(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f119,f131]) ).
fof(f411,plain,
! [X0,X1] :
( X1 = ordered_pair(sK8_skl(X1,X0),sK9_skl(X1,X0))
| ~ member(X1,X0)
| ~ relation_like(X0) ),
inference(resolution,[status(thm)],[f410,f131]) ).
fof(f412,plain,
! [X0,X1,X2] :
( sK10_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)],[f122,f131]) ).
fof(f416,plain,
( ~ sQ3_spl
| member(ordered_pair(sK16_skl,sK17_skl),compose(sK14_skl,sK15_skl)) ),
inference(backward_demodulation,[status(thm)],[f341,f161]) ).
fof(f417,plain,
( ilf_type(compose(sK14_skl,sK15_skl),subset_type(cross_product(sK11_skl,sK13_skl)))
| ~ ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))
| ~ ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl)) ),
inference(paramodulation,[status(thm)],[f341,f316]) ).
fof(f418,plain,
( ilf_type(compose(sK14_skl,sK15_skl),relation_type(sK11_skl,sK13_skl))
| ~ ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))
| ~ ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl))
| ~ ilf_type(sK13_skl,set_type)
| ~ ilf_type(sK12_skl,set_type) ),
inference(paramodulation,[status(thm)],[f341,f229]) ).
fof(f419,definition,
( sQ27_spl
<=> ilf_type(compose(sK14_skl,sK15_skl),subset_type(cross_product(sK11_skl,sK13_skl))) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f422,plain,
( sQ27_spl
| ~ sQ24_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f417,f253,f288,f419]) ).
fof(f423,definition,
( sQ28_spl
<=> ilf_type(compose(sK14_skl,sK15_skl),relation_type(sK11_skl,sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f426,plain,
( sQ28_spl
| ~ sQ24_spl
| ~ sQ17_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f418,f193,f203,f253,f288,f423]) ).
fof(f427,plain,
( ~ sQ3_spl
| member(ordered_pair(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK17_skl),sK15_skl)
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(sK14_skl,binary_relation_type)
| ~ ilf_type(sK17_skl,set_type) ),
inference(resolution,[status(thm)],[f416,f188]) ).
fof(f428,plain,
( ~ sQ3_spl
| member(ordered_pair(sK16_skl,sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl)),sK14_skl)
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(sK14_skl,binary_relation_type)
| ~ ilf_type(sK17_skl,set_type) ),
inference(resolution,[status(thm)],[f416,f187]) ).
fof(f432,definition,
( sQ29_spl
<=> ilf_type(sK14_skl,binary_relation_type) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f434,plain,
( sQ29_spl
| ~ ilf_type(sK14_skl,binary_relation_type) ),
inference(component_clause,[status(thm)],[f432]) ).
fof(f435,definition,
( sQ30_spl
<=> ilf_type(sK15_skl,binary_relation_type) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f437,plain,
( sQ30_spl
| ~ ilf_type(sK15_skl,binary_relation_type) ),
inference(component_clause,[status(thm)],[f435]) ).
fof(f438,definition,
( sQ31_spl
<=> member(ordered_pair(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK17_skl),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( ~ sQ31_spl
| member(ordered_pair(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK17_skl),sK15_skl) ),
inference(component_clause,[status(thm)],[f438]) ).
fof(f441,plain,
( ~ sQ3_spl
| sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f427,f260,f432,f435,f438,f160]) ).
fof(f442,definition,
( sQ32_spl
<=> member(ordered_pair(sK16_skl,sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl)),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f443,plain,
( ~ sQ32_spl
| member(ordered_pair(sK16_skl,sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl)),sK14_skl) ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f445,plain,
( ~ sQ3_spl
| sQ32_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f428,f260,f432,f435,f442,f160]) ).
fof(f461,plain,
( sQ3_spl
| ~ member(ordered_pair(sK16_skl,sK17_skl),compose(sK14_skl,sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f341,f162]) ).
fof(f463,definition,
( sQ37_spl
<=> empty(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f464,plain,
( ~ sQ37_spl
| empty(sK12_skl) ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f470,plain,
( ~ sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f464,f137]) ).
fof(f471,plain,
~ sQ37_spl,
inference(contradiction_clause,[status(thm)],[f470]) ).
fof(f475,definition,
( sQ39_spl
<=> ilf_type(sK18_skl,set_type) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( sQ39_spl
| ~ ilf_type(sK18_skl,set_type) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f490,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f477,f131]) ).
fof(f491,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f490]) ).
fof(f494,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ member(ordered_pair(X1,sK18_skl),X0)
| ~ ilf_type(sK18_skl,set_type)
| member(ordered_pair(X1,sK17_skl),compose(X0,sK15_skl))
| ~ ilf_type(sK15_skl,binary_relation_type)
| ~ ilf_type(X0,binary_relation_type)
| ~ ilf_type(sK17_skl,set_type) ),
inference(resolution,[status(thm)],[f172,f189]) ).
fof(f497,definition,
! [X0,X1] :
( sQ43_spl
<=> ( ~ member(ordered_pair(X1,sK18_skl),X0)
| member(ordered_pair(X1,sK17_skl),compose(X0,sK15_skl))
| ~ ilf_type(X0,binary_relation_type) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f498,plain,
! [X0,X1] :
( ~ sQ43_spl
| ~ member(ordered_pair(X1,sK18_skl),X0)
| member(ordered_pair(X1,sK17_skl),compose(X0,sK15_skl))
| ~ ilf_type(X0,binary_relation_type) ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f500,plain,
( ~ sQ6_spl
| ~ sQ39_spl
| ~ sQ30_spl
| sQ43_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f494,f260,f497,f435,f475,f171]) ).
fof(f514,plain,
! [X0,X1,X2,X3] :
( sK10_skl(X1) != ordered_pair(X2,X3)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| X0 = ordered_pair(sK8_skl(X0,X1),sK9_skl(X0,X1))
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f411,f412]) ).
fof(f518,plain,
! [X0,X1,X2,X3] :
( sK10_skl(X1) != ordered_pair(X3,X2)
| ~ ilf_type(X2,set_type)
| X0 = ordered_pair(sK8_skl(X0,X1),sK9_skl(X0,X1))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f514,f131]) ).
fof(f519,plain,
( sQ29_spl
| ~ relation_like(sK14_skl) ),
inference(resolution,[status(thm)],[f434,f306]) ).
fof(f525,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)],[f126,f131]) ).
fof(f526,plain,
! [X0,X1,X2] :
( relation_like(X0)
| ~ ilf_type(X0,subset_type(cross_product(X1,X2))) ),
inference(resolution,[status(thm)],[f525,f131]) ).
fof(f529,plain,
( sQ30_spl
| ~ relation_like(sK15_skl) ),
inference(resolution,[status(thm)],[f437,f306]) ).
fof(f537,plain,
! [X0] :
( ilf_type(compose(sK5_skl(cross_product(X0,sK12_skl)),sK15_skl),subset_type(cross_product(X0,sK13_skl)))
| ~ ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))
| ~ ilf_type(sK5_skl(cross_product(X0,sK12_skl)),relation_type(X0,sK12_skl)) ),
inference(paramodulation,[status(thm)],[f338,f316]) ).
fof(f538,plain,
! [X0] :
( ilf_type(compose(sK5_skl(cross_product(X0,sK12_skl)),sK15_skl),relation_type(X0,sK13_skl))
| ~ ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))
| ~ ilf_type(sK5_skl(cross_product(X0,sK12_skl)),relation_type(X0,sK12_skl))
| ~ ilf_type(sK13_skl,set_type)
| ~ ilf_type(sK12_skl,set_type) ),
inference(paramodulation,[status(thm)],[f338,f229]) ).
fof(f539,definition,
! [X0] :
( sQ46_spl
<=> ( ilf_type(compose(sK5_skl(cross_product(X0,sK12_skl)),sK15_skl),subset_type(cross_product(X0,sK13_skl)))
| ~ ilf_type(sK5_skl(cross_product(X0,sK12_skl)),relation_type(X0,sK12_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( ~ sQ24_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f537,f539,f288]) ).
fof(f543,definition,
! [X0] :
( sQ47_spl
<=> ( ilf_type(compose(sK5_skl(cross_product(X0,sK12_skl)),sK15_skl),relation_type(X0,sK13_skl))
| ~ ilf_type(sK5_skl(cross_product(X0,sK12_skl)),relation_type(X0,sK12_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f546,plain,
( ~ sQ24_spl
| sQ47_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f538,f193,f203,f543,f288]) ).
fof(f549,plain,
! [X0] :
( ilf_type(compose(sK1_skl(X0,sK12_skl),sK15_skl),subset_type(cross_product(X0,sK13_skl)))
| ~ ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))
| ~ ilf_type(sK1_skl(X0,sK12_skl),relation_type(X0,sK12_skl)) ),
inference(paramodulation,[status(thm)],[f339,f316]) ).
fof(f550,plain,
! [X0] :
( ilf_type(compose(sK1_skl(X0,sK12_skl),sK15_skl),relation_type(X0,sK13_skl))
| ~ ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))
| ~ ilf_type(sK1_skl(X0,sK12_skl),relation_type(X0,sK12_skl))
| ~ ilf_type(sK13_skl,set_type)
| ~ ilf_type(sK12_skl,set_type) ),
inference(paramodulation,[status(thm)],[f339,f229]) ).
fof(f551,definition,
! [X0] :
( sQ48_spl
<=> ( ilf_type(compose(sK1_skl(X0,sK12_skl),sK15_skl),subset_type(cross_product(X0,sK13_skl)))
| ~ ilf_type(sK1_skl(X0,sK12_skl),relation_type(X0,sK12_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( ~ sQ24_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f549,f551,f288]) ).
fof(f555,definition,
! [X0] :
( sQ49_spl
<=> ( ilf_type(compose(sK1_skl(X0,sK12_skl),sK15_skl),relation_type(X0,sK13_skl))
| ~ ilf_type(sK1_skl(X0,sK12_skl),relation_type(X0,sK12_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f558,plain,
( ~ sQ24_spl
| sQ49_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f550,f193,f203,f555,f288]) ).
fof(f568,plain,
! [X0,X1] :
( sQ30_spl
| ~ ilf_type(sK15_skl,subset_type(cross_product(X0,X1))) ),
inference(resolution,[status(thm)],[f526,f529]) ).
fof(f569,plain,
! [X0,X1] :
( sQ29_spl
| ~ ilf_type(sK14_skl,subset_type(cross_product(X0,X1))) ),
inference(resolution,[status(thm)],[f526,f519]) ).
fof(f591,plain,
( ~ sQ11_spl
| sQ30_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f207,f568]) ).
fof(f593,plain,
( ~ sQ11_spl
| sQ30_spl ),
inference(contradiction_clause,[status(thm)],[f591]) ).
fof(f612,plain,
( ~ sQ9_spl
| sQ29_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f197,f569]) ).
fof(f614,plain,
( ~ sQ9_spl
| sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f612]) ).
fof(f637,plain,
( ~ sQ5_spl
| ~ sQ43_spl
| member(ordered_pair(sK16_skl,sK17_skl),compose(sK14_skl,sK15_skl))
| ~ ilf_type(sK14_skl,binary_relation_type) ),
inference(resolution,[status(thm)],[f498,f168]) ).
fof(f640,definition,
( sQ50_spl
<=> member(ordered_pair(sK16_skl,sK17_skl),compose(sK14_skl,sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f641,plain,
( ~ sQ50_spl
| member(ordered_pair(sK16_skl,sK17_skl),compose(sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f640]) ).
fof(f643,plain,
( ~ sQ5_spl
| ~ sQ43_spl
| sQ50_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f637,f432,f640,f497,f167]) ).
fof(f644,plain,
( ~ sQ50_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f641,f461]) ).
fof(f645,plain,
( ~ sQ50_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f644]) ).
fof(f673,plain,
! [X0,X1] :
( ~ sQ31_spl
| member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),X1)
| ~ ilf_type(sK15_skl,relation_type(X1,X0))
| ~ ilf_type(sK17_skl,set_type)
| ~ ilf_type(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),set_type)
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f439,f180]) ).
fof(f677,definition,
( sQ52_spl
<=> ilf_type(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f679,plain,
( sQ52_spl
| ~ ilf_type(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),set_type) ),
inference(component_clause,[status(thm)],[f677]) ).
fof(f682,definition,
! [X0,X1] :
( sQ53_spl
<=> ( member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),X1)
| ~ ilf_type(sK15_skl,relation_type(X1,X0))
| ~ ilf_type(X0,set_type) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f683,plain,
! [X0,X1] :
( ~ sQ53_spl
| member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),X1)
| ~ ilf_type(sK15_skl,relation_type(X1,X0))
| ~ ilf_type(X0,set_type) ),
inference(component_clause,[status(thm)],[f682]) ).
fof(f685,plain,
( ~ sQ31_spl
| ~ sQ18_spl
| ~ sQ52_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f673,f682,f677,f260,f438]) ).
fof(f686,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f679,f131]) ).
fof(f687,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f686]) ).
fof(f688,plain,
! [X0,X1] :
( ~ sQ53_spl
| member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),X0)
| ~ ilf_type(sK15_skl,relation_type(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f683,f131]) ).
fof(f689,plain,
( ~ sQ7_spl
| ~ sQ32_spl
| ~ member(ordered_pair(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK17_skl),sK15_skl)
| ~ ilf_type(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),member_type(sK12_skl)) ),
inference(resolution,[status(thm)],[f443,f176]) ).
fof(f693,definition,
( sQ54_spl
<=> ilf_type(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),member_type(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f695,plain,
( sQ54_spl
| ~ ilf_type(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),member_type(sK12_skl)) ),
inference(component_clause,[status(thm)],[f693]) ).
fof(f696,plain,
( ~ sQ7_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f689,f693,f438,f442,f175]) ).
fof(f722,plain,
! [X0,X1,X2,X3] :
( sK10_skl(X1) != ordered_pair(X2,X3)
| X0 = ordered_pair(sK8_skl(X0,X1),sK9_skl(X0,X1))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f518,f131]) ).
fof(f732,plain,
! [X0,X1] :
( ~ sQ16_spl
| sK10_skl(sK13_skl) != ordered_pair(X0,X1)
| sK17_skl = ordered_pair(sK8_skl(sK17_skl,sK13_skl),sK9_skl(sK17_skl,sK13_skl)) ),
inference(resolution,[status(thm)],[f722,f238]) ).
fof(f733,plain,
! [X0,X1] :
( ~ sQ14_spl
| sK10_skl(sK11_skl) != ordered_pair(X0,X1)
| sK16_skl = ordered_pair(sK8_skl(sK16_skl,sK11_skl),sK9_skl(sK16_skl,sK11_skl)) ),
inference(resolution,[status(thm)],[f722,f220]) ).
fof(f765,definition,
( sQ65_spl
<=> sK17_skl = ordered_pair(sK8_skl(sK17_skl,sK13_skl),sK9_skl(sK17_skl,sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f768,definition,
! [X0,X1] :
( sQ66_spl
<=> sK10_skl(sK13_skl) != ordered_pair(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f771,plain,
( ~ sQ16_spl
| sQ66_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f732,f765,f768,f237]) ).
fof(f772,definition,
( sQ67_spl
<=> sK16_skl = ordered_pair(sK8_skl(sK16_skl,sK11_skl),sK9_skl(sK16_skl,sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f775,definition,
! [X0,X1] :
( sQ68_spl
<=> sK10_skl(sK11_skl) != ordered_pair(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f778,plain,
( ~ sQ14_spl
| sQ68_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f733,f772,f775,f219]) ).
fof(f848,plain,
( ~ sQ53_spl
| member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f688,f142]) ).
fof(f849,plain,
( sQ54_spl
| ~ member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK12_skl)
| empty(sK12_skl) ),
inference(resolution,[status(thm)],[f695,f224]) ).
fof(f850,definition,
( sQ75_spl
<=> member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f852,plain,
( sQ75_spl
| ~ member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK12_skl) ),
inference(component_clause,[status(thm)],[f850]) ).
fof(f853,plain,
( sQ54_spl
| ~ sQ75_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f849,f463,f850,f693]) ).
fof(f867,plain,
! [X0] :
( ilf_type(compose(sK5_skl(cross_product(X0,sK11_skl)),sK14_skl),subset_type(cross_product(X0,sK12_skl)))
| ~ ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl))
| ~ ilf_type(sK5_skl(cross_product(X0,sK11_skl)),relation_type(X0,sK11_skl)) ),
inference(paramodulation,[status(thm)],[f347,f316]) ).
fof(f868,definition,
! [X0] :
( sQ76_spl
<=> ( ilf_type(compose(sK5_skl(cross_product(X0,sK11_skl)),sK14_skl),subset_type(cross_product(X0,sK12_skl)))
| ~ ilf_type(sK5_skl(cross_product(X0,sK11_skl)),relation_type(X0,sK11_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f871,plain,
( ~ sQ17_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f867,f868,f253]) ).
fof(f873,plain,
! [X0] :
( ilf_type(compose(sK1_skl(X0,sK11_skl),sK14_skl),subset_type(cross_product(X0,sK12_skl)))
| ~ ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl))
| ~ ilf_type(sK1_skl(X0,sK11_skl),relation_type(X0,sK11_skl)) ),
inference(paramodulation,[status(thm)],[f348,f316]) ).
fof(f874,definition,
! [X0] :
( sQ77_spl
<=> ( ilf_type(compose(sK1_skl(X0,sK11_skl),sK14_skl),subset_type(cross_product(X0,sK12_skl)))
| ~ ilf_type(sK1_skl(X0,sK11_skl),relation_type(X0,sK11_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f877,plain,
( ~ sQ17_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f873,f874,f253]) ).
fof(f936,plain,
! [X0] :
( ilf_type(compose(sK15_skl,sK1_skl(sK13_skl,X0)),subset_type(cross_product(sK12_skl,X0)))
| ~ ilf_type(sK1_skl(sK13_skl,X0),relation_type(sK13_skl,X0))
| ~ ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl)) ),
inference(paramodulation,[status(thm)],[f372,f316]) ).
fof(f937,definition,
! [X0] :
( sQ83_spl
<=> ( ilf_type(compose(sK15_skl,sK1_skl(sK13_skl,X0)),subset_type(cross_product(sK12_skl,X0)))
| ~ ilf_type(sK1_skl(sK13_skl,X0),relation_type(sK13_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f940,plain,
( sQ83_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f936,f288,f937]) ).
fof(f942,plain,
! [X0] :
( ilf_type(compose(sK14_skl,sK1_skl(sK12_skl,X0)),subset_type(cross_product(sK11_skl,X0)))
| ~ ilf_type(sK1_skl(sK12_skl,X0),relation_type(sK12_skl,X0))
| ~ ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl)) ),
inference(paramodulation,[status(thm)],[f373,f316]) ).
fof(f943,definition,
! [X0] :
( sQ84_spl
<=> ( ilf_type(compose(sK14_skl,sK1_skl(sK12_skl,X0)),subset_type(cross_product(sK11_skl,X0)))
| ~ ilf_type(sK1_skl(sK12_skl,X0),relation_type(sK12_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f946,plain,
( sQ84_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f942,f253,f943]) ).
fof(f1219,plain,
( sQ75_spl
| ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f852,f848]) ).
fof(f1220,plain,
( sQ75_spl
| ~ sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f1219]) ).
fof(f1221,plain,
$false,
inference(sat_refutation,[status(thm)],[f155,f159,f170,f174,f178,f184,f199,f201,f209,f211,f222,f240,f242,f256,f282,f284,f291,f345,f353,f355,f358,f422,f426,f441,f445,f471,f491,f500,f542,f546,f554,f558,f593,f614,f643,f645,f685,f687,f696,f771,f778,f853,f871,f877,f940,f946,f1220]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET684+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.37 % Computer : n014.cluster.edu
% 0.08/5.37 % Model : x86_64 x86_64
% 0.08/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.37 % Memory : 8046.5625MB
% 0.08/5.37 % OS : Linux 6.8.0-71-generic
% 0.08/5.37 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Mon Sep 21 05:32:40 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.08/5.38 % Drodi V4.1.1
% 0.14/5.45 % Refutation found
% 0.14/5.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/5.49 % Elapsed time: 0.101860 seconds
% 0.14/5.49 % CPU time: 0.548855 seconds
% 0.14/5.49 % Total memory used: 95.180 MB
% 0.14/5.49 % Net memory used: 94.488 MB
%------------------------------------------------------------------------------