%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU340+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:20:13 PM UTC 2026
% Result : Theorem 0.17s 0.51s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 85
% Syntax : Number of formulae : 398 ( 40 unt; 64 def)
% Number of atoms : 1070 ( 44 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 1187 ( 515 ~; 520 |; 56 &)
% ( 71 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 75 ( 73 usr; 65 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-2 aty)
% Number of variables : 324 ( 308 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( rel_str(A)
=> ( transitive_relstr(A)
<=> is_transitive_in(the_InternalRel(A),the_carrier(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( relation(A)
=> ! [B] :
( is_transitive_in(A,B)
<=> ! [C,D,E] :
( ( in(ordered_pair(D,E),A)
& in(ordered_pair(C,D),A)
& in(E,B)
& in(D,B)
& in(C,B) )
=> in(ordered_pair(C,E),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( related(A,B,C)
<=> in(ordered_pair(B,C),the_InternalRel(A)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( rel_str(A)
=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A,B,C,D] :
( in(ordered_pair(A,B),cartesian_product2(C,D))
<=> ( in(B,D)
& in(A,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,conjecture,
! [A] :
( ( rel_str(A)
& transitive_relstr(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ( ( related(A,C,D)
& related(A,B,C) )
=> related(A,B,D) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& transitive_relstr(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ( ( related(A,C,D)
& related(A,B,C) )
=> related(A,B,D) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f39]) ).
fof(f41,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f49,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
! [A,B,C] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f51,plain,
! [C] :
( relation(C)
| ! [A,B] : ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(miniscoping,[status(thm)],[f50]) ).
fof(f52,plain,
! [X0,X1,X2] :
( relation(X0)
| ~ element(X0,powerset(cartesian_product2(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f54,plain,
! [A] :
( ( transitive_relstr(A)
<=> is_transitive_in(the_InternalRel(A),the_carrier(A)) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f55,plain,
! [A] :
( ( ( ~ is_transitive_in(the_InternalRel(A),the_carrier(A))
| transitive_relstr(A) )
& ( is_transitive_in(the_InternalRel(A),the_carrier(A))
| ~ transitive_relstr(A) ) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
! [X0] :
( is_transitive_in(the_InternalRel(X0),the_carrier(X0))
| ~ transitive_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f59,plain,
! [A] :
( ! [B] :
( is_transitive_in(A,B)
<=> ! [C,D,E] :
( in(ordered_pair(C,E),A)
| ~ in(ordered_pair(D,E),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(E,B)
| ~ in(D,B)
| ~ in(C,B) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f60,plain,
! [A] :
( ! [B] :
( ( ? [C,D,E] :
( ~ in(ordered_pair(C,E),A)
& in(ordered_pair(D,E),A)
& in(ordered_pair(C,D),A)
& in(E,B)
& in(D,B)
& in(C,B) )
| is_transitive_in(A,B) )
& ( ! [C,D,E] :
( in(ordered_pair(C,E),A)
| ~ in(ordered_pair(D,E),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(E,B)
| ~ in(D,B)
| ~ in(C,B) )
| ~ is_transitive_in(A,B) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [A] :
( ( ! [B] :
( ? [C,E] :
( ~ in(ordered_pair(C,E),A)
& ? [D] :
( in(ordered_pair(D,E),A)
& in(ordered_pair(C,D),A)
& in(E,B)
& in(D,B)
& in(C,B) ) )
| is_transitive_in(A,B) )
& ! [B] :
( ! [C,E] :
( in(ordered_pair(C,E),A)
| ! [D] :
( ~ in(ordered_pair(D,E),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(E,B)
| ~ in(D,B)
| ~ in(C,B) ) )
| ~ is_transitive_in(A,B) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f60]) ).
fof(f62,plain,
! [A] :
( ( ! [B] :
( ( ~ in(ordered_pair(sK0_skl(B,A),sK1_skl(B,A)),A)
& in(ordered_pair(sK2_skl(B,A),sK1_skl(B,A)),A)
& in(ordered_pair(sK0_skl(B,A),sK2_skl(B,A)),A)
& in(sK1_skl(B,A),B)
& in(sK2_skl(B,A),B)
& in(sK0_skl(B,A),B) )
| is_transitive_in(A,B) )
& ! [B] :
( ! [C,E] :
( in(ordered_pair(C,E),A)
| ! [D] :
( ~ in(ordered_pair(D,E),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(E,B)
| ~ in(D,B)
| ~ in(C,B) ) )
| ~ is_transitive_in(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(C,sK0_skl(B,A)),skolemize(E,sK1_skl(B,A)),skolemize(D,sK2_skl(B,A))],[f61]) ).
fof(f63,plain,
! [X0,X1,X2,X3,X4] :
( in(ordered_pair(X2,X4),X0)
| ~ in(ordered_pair(X3,X4),X0)
| ~ in(ordered_pair(X2,X3),X0)
| ~ in(X4,X1)
| ~ in(X3,X1)
| ~ in(X2,X1)
| ~ is_transitive_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f70,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( related(A,B,C)
<=> in(ordered_pair(B,C),the_InternalRel(A)) )
| ~ element(C,the_carrier(A)) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f71,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ in(ordered_pair(B,C),the_InternalRel(A))
| related(A,B,C) )
& ( in(ordered_pair(B,C),the_InternalRel(A))
| ~ related(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f70]) ).
fof(f72,plain,
! [X0,X1,X2] :
( in(ordered_pair(X1,X2),the_InternalRel(X0))
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),the_InternalRel(X0))
| related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f76,plain,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f77,plain,
! [X0,X1,X2] :
( element(X0,powerset(cartesian_product2(X1,X2)))
| ~ relation_of2_as_subset(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
! [A] :
( relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A))
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f79,plain,
! [X0] :
( relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f86,plain,
! [A] : element(sK6_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(B,sK6_skl(A))],[f24]) ).
fof(f87,plain,
! [X0] : element(sK6_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f90,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f96,plain,
! [A] :
( ? [B] :
( ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f97,plain,
! [A] :
( ( ~ empty(sK8_skl(A))
& element(sK8_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f96]) ).
fof(f98,plain,
! [X0] :
( element(sK8_skl(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f99,plain,
! [X0] :
( ~ empty(sK8_skl(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f100,plain,
empty(sK9_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f32]) ).
fof(f101,plain,
empty(sK9_skl),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f102,plain,
! [A] :
( empty(sK10_skl(A))
& element(sK10_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(B,sK10_skl(A))],[f33]) ).
fof(f103,plain,
! [X0] : element(sK10_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
! [X0] : empty(sK10_skl(X0)),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f105,plain,
~ empty(sK11_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f34]) ).
fof(f106,plain,
~ empty(sK11_skl),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f113,plain,
! [A,B,C,D] :
( ( ~ in(B,D)
| ~ in(A,C)
| in(ordered_pair(A,B),cartesian_product2(C,D)) )
& ( ( in(B,D)
& in(A,C) )
| ~ in(ordered_pair(A,B),cartesian_product2(C,D)) ) ),
inference(NNF_transformation,[status(thm)],[f37]) ).
fof(f114,plain,
( ! [A,B,C,D] :
( ~ in(B,D)
| ~ in(A,C)
| in(ordered_pair(A,B),cartesian_product2(C,D)) )
& ! [A,B,C,D] :
( ( in(B,D)
& in(A,C) )
| ~ in(ordered_pair(A,B),cartesian_product2(C,D)) ) ),
inference(miniscoping,[status(thm)],[f113]) ).
fof(f115,plain,
! [X0,X1,X2,X3] :
( in(X0,X2)
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f118,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f119,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ~ related(A,B,D)
& related(A,C,D)
& related(A,B,C)
& element(D,the_carrier(A)) )
& element(C,the_carrier(A)) )
& element(B,the_carrier(A)) )
& rel_str(A)
& transitive_relstr(A) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f121,plain,
( ~ related(sK12_skl,sK13_skl,sK15_skl)
& related(sK12_skl,sK14_skl,sK15_skl)
& related(sK12_skl,sK13_skl,sK14_skl)
& element(sK15_skl,the_carrier(sK12_skl))
& element(sK14_skl,the_carrier(sK12_skl))
& element(sK13_skl,the_carrier(sK12_skl))
& rel_str(sK12_skl)
& transitive_relstr(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl,sK15_skl]),skolemize(A,sK12_skl),skolemize(B,sK13_skl),skolemize(C,sK14_skl),skolemize(D,sK15_skl)],[f120]) ).
fof(f122,plain,
transitive_relstr(sK12_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
rel_str(sK12_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f124,plain,
element(sK13_skl,the_carrier(sK12_skl)),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f125,plain,
element(sK14_skl,the_carrier(sK12_skl)),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f126,plain,
element(sK15_skl,the_carrier(sK12_skl)),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f127,plain,
related(sK12_skl,sK13_skl,sK14_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f128,plain,
related(sK12_skl,sK14_skl,sK15_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f129,plain,
~ related(sK12_skl,sK13_skl,sK15_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f130,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f131,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f136,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f137,plain,
! [A,C] :
( element(A,C)
| ! [B] :
( ~ element(B,powerset(C))
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f136]) ).
fof(f138,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f140,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f139]) ).
fof(f141,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f142,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f143,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f144,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f145,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f146,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f152,plain,
! [X0] :
( in(X0,sK11_skl)
| ~ element(X0,sK11_skl) ),
inference(resolution,[status(thm)],[f106,f131]) ).
fof(f153,plain,
! [X0,X1] :
( in(X0,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(resolution,[status(thm)],[f90,f131]) ).
fof(f156,plain,
! [X0] : sK10_skl(X0) = empty_set,
inference(resolution,[status(thm)],[f143,f104]) ).
fof(f157,plain,
sK9_skl = empty_set,
inference(resolution,[status(thm)],[f143,f101]) ).
fof(f159,plain,
! [X0,X1] :
( in(X1,X0)
| ~ element(X1,X0)
| X0 = empty_set ),
inference(resolution,[status(thm)],[f143,f131]) ).
fof(f161,plain,
! [X0] : element(empty_set,powerset(X0)),
inference(backward_demodulation,[status(thm)],[f156,f103]) ).
fof(f162,plain,
! [X0] :
( X0 = sK9_skl
| ~ empty(X0) ),
inference(backward_demodulation,[status(thm)],[f157,f143]) ).
fof(f165,plain,
! [X0,X1] :
( in(X1,X0)
| ~ element(X1,X0)
| X0 = sK9_skl ),
inference(forward_demodulation,[status(thm)],[f157,f159]) ).
fof(f167,plain,
! [X0] : element(sK9_skl,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f157,f161]) ).
fof(f170,plain,
! [X0,X1,X2] :
( ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ empty(the_InternalRel(X0)) ),
inference(resolution,[status(thm)],[f146,f72]) ).
fof(f185,plain,
! [X0] :
( in(sK6_skl(X0),X0)
| X0 = sK9_skl ),
inference(resolution,[status(thm)],[f165,f87]) ).
fof(f186,plain,
( in(sK15_skl,the_carrier(sK12_skl))
| the_carrier(sK12_skl) = sK9_skl ),
inference(resolution,[status(thm)],[f165,f126]) ).
fof(f190,definition,
( sQ0_spl
<=> the_carrier(sK12_skl) = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( ~ sQ0_spl
| the_carrier(sK12_skl) = sK9_skl ),
inference(component_clause,[status(thm)],[f190]) ).
fof(f193,definition,
( sQ1_spl
<=> in(sK15_skl,the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f194,plain,
( ~ sQ1_spl
| in(sK15_skl,the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f193]) ).
fof(f196,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f186,f190,f193]) ).
fof(f197,definition,
( sQ2_spl
<=> in(sK14_skl,the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f198,plain,
( ~ sQ2_spl
| in(sK14_skl,the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f197]) ).
fof(f201,definition,
( sQ3_spl
<=> in(sK13_skl,the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f205,plain,
( ~ sQ0_spl
| element(sK15_skl,sK9_skl) ),
inference(backward_demodulation,[status(thm)],[f191,f126]) ).
fof(f206,plain,
( ~ sQ0_spl
| element(sK14_skl,sK9_skl) ),
inference(backward_demodulation,[status(thm)],[f191,f125]) ).
fof(f209,definition,
( sQ4_spl
<=> rel_str(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f211,plain,
( sQ4_spl
| ~ rel_str(sK12_skl) ),
inference(component_clause,[status(thm)],[f209]) ).
fof(f212,definition,
( sQ5_spl
<=> transitive_relstr(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f214,plain,
( sQ5_spl
| ~ transitive_relstr(sK12_skl) ),
inference(component_clause,[status(thm)],[f212]) ).
fof(f223,definition,
( sQ8_spl
<=> in(sK15_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f224,plain,
( ~ sQ8_spl
| in(sK15_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f223]) ).
fof(f228,definition,
( sQ9_spl
<=> in(sK14_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f229,plain,
( ~ sQ9_spl
| in(sK14_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f228]) ).
fof(f232,plain,
( ~ sQ8_spl
| ~ empty(sK9_skl) ),
inference(resolution,[status(thm)],[f224,f146]) ).
fof(f234,plain,
( ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f232,f101]) ).
fof(f235,plain,
~ sQ8_spl,
inference(contradiction_clause,[status(thm)],[f234]) ).
fof(f236,plain,
( ~ sQ9_spl
| ~ empty(sK9_skl) ),
inference(resolution,[status(thm)],[f229,f146]) ).
fof(f238,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f236,f101]) ).
fof(f239,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f238]) ).
fof(f240,plain,
( ~ sQ1_spl
| ~ empty(the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f194,f146]) ).
fof(f242,plain,
! [X0] :
( ~ sQ1_spl
| in(X0,the_carrier(sK12_skl))
| ~ element(X0,the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f240,f131]) ).
fof(f252,plain,
! [X0] :
( in(sK9_skl,powerset(X0))
| powerset(X0) = sK9_skl ),
inference(resolution,[status(thm)],[f167,f165]) ).
fof(f253,plain,
! [X0,X1] :
( in(X1,sK8_skl(X0))
| ~ element(X1,sK8_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f99,f131]) ).
fof(f259,plain,
! [X0] :
( ~ in(X0,sK6_skl(X0))
| X0 = sK9_skl ),
inference(resolution,[status(thm)],[f185,f49]) ).
fof(f260,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ element(X0,powerset(cartesian_product2(X5,X6)))
| in(ordered_pair(X2,X4),X0)
| ~ in(ordered_pair(X3,X4),X0)
| ~ in(ordered_pair(X2,X3),X0)
| ~ in(X4,X1)
| ~ in(X3,X1)
| ~ in(X2,X1)
| ~ is_transitive_in(X0,X1) ),
inference(resolution,[status(thm)],[f63,f52]) ).
fof(f261,plain,
! [X0] :
( ~ sQ1_spl
| ~ empty(the_carrier(sK12_skl))
| ~ element(X0,the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f242,f146]) ).
fof(f263,definition,
! [X0] :
( sQ10_spl
<=> ~ element(X0,the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f264,plain,
! [X0] :
( ~ sQ10_spl
| ~ element(X0,the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f263]) ).
fof(f266,definition,
( sQ11_spl
<=> empty(the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f269,plain,
( ~ sQ1_spl
| ~ sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f261,f263,f266,f193]) ).
fof(f270,plain,
( ~ sQ10_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f124,f264]) ).
fof(f282,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f270]) ).
fof(f310,plain,
! [X0,X1,X2,X3] :
( in(X3,the_InternalRel(X0))
| ~ element(X3,the_InternalRel(X0))
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(resolution,[status(thm)],[f170,f131]) ).
fof(f351,plain,
! [X0,X1] :
( ~ element(X1,powerset(sK9_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f141,f101]) ).
fof(f354,plain,
! [X0] : ~ in(X0,sK9_skl),
inference(resolution,[status(thm)],[f351,f167]) ).
fof(f357,plain,
! [X0,X1] :
( ~ in(X1,powerset(sK9_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f351,f119]) ).
fof(f410,plain,
! [X0] :
( powerset(sK9_skl) = sK9_skl
| ~ in(X0,sK9_skl) ),
inference(resolution,[status(thm)],[f357,f252]) ).
fof(f411,plain,
! [X0] :
( powerset(sK9_skl) = sK9_skl
| ~ in(X0,sK6_skl(powerset(sK9_skl))) ),
inference(resolution,[status(thm)],[f357,f185]) ).
fof(f413,definition,
! [X0] :
( sQ15_spl
<=> ~ in(X0,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f416,definition,
( sQ16_spl
<=> powerset(sK9_skl) = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f417,plain,
( ~ sQ16_spl
| powerset(sK9_skl) = sK9_skl ),
inference(component_clause,[status(thm)],[f416]) ).
fof(f419,plain,
( sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f410,f413,f416]) ).
fof(f420,definition,
! [X0] :
( sQ17_spl
<=> ~ in(X0,sK6_skl(powerset(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f421,plain,
! [X0] :
( ~ sQ17_spl
| ~ in(X0,sK6_skl(powerset(sK9_skl))) ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f423,plain,
( sQ16_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f411,f420,f416]) ).
fof(f427,plain,
! [X0] :
( in(sK6_skl(sK8_skl(X0)),sK8_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f253,f87]) ).
fof(f435,plain,
! [X0] :
( ~ sQ16_spl
| in(X0,sK9_skl)
| ~ element(X0,powerset(sK9_skl)) ),
inference(paramodulation,[status(thm)],[f417,f153]) ).
fof(f436,plain,
( ~ sQ16_spl
| element(sK9_skl,sK9_skl) ),
inference(paramodulation,[status(thm)],[f417,f167]) ).
fof(f447,plain,
! [X0] :
( ~ sQ16_spl
| in(X0,sK9_skl)
| ~ element(X0,sK9_skl) ),
inference(forward_demodulation,[status(thm)],[f417,f435]) ).
fof(f449,plain,
! [X0] :
( ~ sQ16_spl
| ~ element(X0,sK9_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f447,f354]) ).
fof(f450,plain,
( ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f436,f449]) ).
fof(f451,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f450]) ).
fof(f454,plain,
( ~ sQ17_spl
| sK6_skl(powerset(sK9_skl)) = sK9_skl ),
inference(resolution,[status(thm)],[f421,f185]) ).
fof(f456,plain,
( ~ sQ17_spl
| ~ in(powerset(sK9_skl),sK9_skl)
| powerset(sK9_skl) = sK9_skl ),
inference(paramodulation,[status(thm)],[f454,f259]) ).
fof(f457,plain,
( ~ sQ17_spl
| in(sK9_skl,powerset(sK9_skl))
| powerset(sK9_skl) = sK9_skl ),
inference(paramodulation,[status(thm)],[f454,f185]) ).
fof(f459,definition,
( sQ20_spl
<=> in(powerset(sK9_skl),sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f462,plain,
( ~ sQ17_spl
| ~ sQ20_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f456,f416,f459,f420]) ).
fof(f463,definition,
( sQ21_spl
<=> in(sK9_skl,powerset(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( ~ sQ17_spl
| sQ21_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f457,f416,f463,f420]) ).
fof(f572,plain,
( in(sK13_skl,the_carrier(sK12_skl))
| empty(the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f131,f124]) ).
fof(f573,plain,
( in(sK14_skl,the_carrier(sK12_skl))
| empty(the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f131,f125]) ).
fof(f577,plain,
! [X0] :
( in(sK6_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f131,f87]) ).
fof(f578,plain,
! [X0,X1,X2] :
( ~ relation_of2_as_subset(X2,X0,X1)
| in(X2,powerset(cartesian_product2(X0,X1)))
| empty(powerset(cartesian_product2(X0,X1))) ),
inference(resolution,[status(thm)],[f131,f77]) ).
fof(f581,plain,
( sQ3_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f572,f266,f201]) ).
fof(f582,plain,
( sQ2_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f573,f266,f197]) ).
fof(f586,plain,
! [X0,X1,X2] :
( ~ relation_of2_as_subset(X0,X1,X2)
| in(X0,powerset(cartesian_product2(X1,X2))) ),
inference(forward_subsumption_resolution,[status(thm)],[f578,f90]) ).
fof(f597,plain,
! [X0] :
( ~ element(X0,sK11_skl)
| ~ in(sK11_skl,X0) ),
inference(resolution,[status(thm)],[f49,f152]) ).
fof(f601,plain,
! [X0] :
( ~ in(X0,sK6_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f577,f49]) ).
fof(f603,definition,
( sQ26_spl
<=> empty(powerset(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( ~ sQ26_spl
| empty(powerset(sK9_skl)) ),
inference(component_clause,[status(thm)],[f603]) ).
fof(f722,plain,
! [X0,X1] :
( in(ordered_pair(X0,X1),the_InternalRel(sK12_skl))
| ~ related(sK12_skl,X0,X1)
| ~ element(X1,the_carrier(sK12_skl))
| ~ element(X0,the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f72,f123]) ).
fof(f740,plain,
! [X0,X1] :
( empty(X1)
| element(X0,X1)
| ~ in(X0,sK8_skl(X1)) ),
inference(resolution,[status(thm)],[f138,f98]) ).
fof(f745,plain,
! [X0,X1,X2] :
( ~ in(X1,powerset(X2))
| element(X0,X2)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f138,f119]) ).
fof(f747,plain,
( in(ordered_pair(sK14_skl,sK15_skl),the_InternalRel(sK12_skl))
| ~ element(sK15_skl,the_carrier(sK12_skl))
| ~ element(sK14_skl,the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f722,f128]) ).
fof(f748,plain,
( in(ordered_pair(sK13_skl,sK14_skl),the_InternalRel(sK12_skl))
| ~ element(sK14_skl,the_carrier(sK12_skl))
| ~ element(sK13_skl,the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f722,f127]) ).
fof(f749,definition,
( sQ29_spl
<=> element(sK14_skl,the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f751,plain,
( sQ29_spl
| ~ element(sK14_skl,the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f749]) ).
fof(f752,definition,
( sQ30_spl
<=> element(sK15_skl,the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f754,plain,
( sQ30_spl
| ~ element(sK15_skl,the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f752]) ).
fof(f755,definition,
( sQ31_spl
<=> in(ordered_pair(sK14_skl,sK15_skl),the_InternalRel(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f756,plain,
( ~ sQ31_spl
| in(ordered_pair(sK14_skl,sK15_skl),the_InternalRel(sK12_skl)) ),
inference(component_clause,[status(thm)],[f755]) ).
fof(f758,plain,
( sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f747,f749,f752,f755]) ).
fof(f759,definition,
( sQ32_spl
<=> element(sK13_skl,the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f761,plain,
( sQ32_spl
| ~ element(sK13_skl,the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f759]) ).
fof(f762,definition,
( sQ33_spl
<=> in(ordered_pair(sK13_skl,sK14_skl),the_InternalRel(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f763,plain,
( ~ sQ33_spl
| in(ordered_pair(sK13_skl,sK14_skl),the_InternalRel(sK12_skl)) ),
inference(component_clause,[status(thm)],[f762]) ).
fof(f765,plain,
( sQ33_spl
| ~ sQ29_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f748,f759,f749,f762]) ).
fof(f766,plain,
( ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f604,f90]) ).
fof(f767,plain,
~ sQ26_spl,
inference(contradiction_clause,[status(thm)],[f766]) ).
fof(f768,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f751,f125]) ).
fof(f769,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f768]) ).
fof(f770,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f754,f126]) ).
fof(f771,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f770]) ).
fof(f772,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f761,f124]) ).
fof(f773,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f772]) ).
fof(f774,plain,
( ~ sQ31_spl
| related(sK12_skl,sK14_skl,sK15_skl)
| ~ element(sK15_skl,the_carrier(sK12_skl))
| ~ element(sK14_skl,the_carrier(sK12_skl))
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f756,f73]) ).
fof(f776,definition,
( sQ34_spl
<=> related(sK12_skl,sK14_skl,sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f779,plain,
( ~ sQ31_spl
| sQ34_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f774,f209,f749,f752,f776,f755]) ).
fof(f780,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f211,f123]) ).
fof(f781,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f780]) ).
fof(f782,plain,
( ~ sQ33_spl
| related(sK12_skl,sK13_skl,sK14_skl)
| ~ element(sK14_skl,the_carrier(sK12_skl))
| ~ element(sK13_skl,the_carrier(sK12_skl))
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f763,f73]) ).
fof(f784,definition,
( sQ35_spl
<=> related(sK12_skl,sK13_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f787,plain,
( ~ sQ33_spl
| sQ35_spl
| ~ sQ29_spl
| ~ sQ32_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f782,f209,f759,f749,f784,f762]) ).
fof(f843,plain,
! [X0] :
( empty(X0)
| empty(X0)
| element(sK6_skl(sK8_skl(X0)),X0) ),
inference(resolution,[status(thm)],[f740,f427]) ).
fof(f846,plain,
! [X0] :
( empty(X0)
| element(sK6_skl(sK8_skl(X0)),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f843]) ).
fof(f857,plain,
( ~ in(sK11_skl,sK6_skl(sK8_skl(sK11_skl)))
| empty(sK11_skl) ),
inference(resolution,[status(thm)],[f846,f597]) ).
fof(f858,plain,
! [X0] :
( in(sK6_skl(sK8_skl(X0)),X0)
| X0 = sK9_skl
| empty(X0) ),
inference(resolution,[status(thm)],[f846,f165]) ).
fof(f859,plain,
! [X0] :
( in(sK6_skl(sK8_skl(X0)),X0)
| empty(X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f846,f131]) ).
fof(f869,definition,
! [X0] :
( sQ38_spl
<=> ~ in(X0,sK6_skl(sK8_skl(powerset(sK9_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f870,plain,
! [X0] :
( ~ sQ38_spl
| ~ in(X0,sK6_skl(sK8_skl(powerset(sK9_skl)))) ),
inference(component_clause,[status(thm)],[f869]) ).
fof(f876,definition,
( sQ39_spl
<=> empty(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f877,plain,
( ~ sQ39_spl
| empty(sK11_skl) ),
inference(component_clause,[status(thm)],[f876]) ).
fof(f879,definition,
( sQ40_spl
<=> in(sK11_skl,sK6_skl(sK8_skl(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f882,plain,
( ~ sQ40_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f857,f876,f879]) ).
fof(f883,plain,
! [X0] :
( in(sK6_skl(sK8_skl(X0)),X0)
| X0 = sK9_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f858,f162]) ).
fof(f884,plain,
! [X0] :
( in(sK6_skl(sK8_skl(X0)),X0)
| empty(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f859]) ).
fof(f885,plain,
( ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f877,f106]) ).
fof(f886,plain,
~ sQ39_spl,
inference(contradiction_clause,[status(thm)],[f885]) ).
fof(f889,plain,
! [X0] :
( ~ in(X0,sK6_skl(sK8_skl(powerset(sK9_skl))))
| powerset(sK9_skl) = sK9_skl ),
inference(resolution,[status(thm)],[f883,f357]) ).
fof(f894,plain,
( sQ38_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f889,f416,f869]) ).
fof(f895,plain,
! [X0] :
( empty(X0)
| element(sK6_skl(sK8_skl(sK8_skl(X0))),X0)
| empty(sK8_skl(X0)) ),
inference(resolution,[status(thm)],[f884,f740]) ).
fof(f902,plain,
! [X0] :
( empty(X0)
| element(sK6_skl(sK8_skl(sK8_skl(X0))),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f895,f99]) ).
fof(f905,plain,
( ~ sQ38_spl
| sK6_skl(sK8_skl(powerset(sK9_skl))) = sK9_skl ),
inference(resolution,[status(thm)],[f870,f883]) ).
fof(f913,plain,
( ~ sQ38_spl
| empty(powerset(sK9_skl))
| element(sK9_skl,powerset(sK9_skl)) ),
inference(paramodulation,[status(thm)],[f905,f846]) ).
fof(f914,plain,
( ~ sQ38_spl
| in(sK9_skl,sK8_skl(powerset(sK9_skl)))
| empty(powerset(sK9_skl)) ),
inference(paramodulation,[status(thm)],[f905,f427]) ).
fof(f916,plain,
( ~ sQ38_spl
| ~ in(sK8_skl(powerset(sK9_skl)),sK9_skl)
| empty(sK8_skl(powerset(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f905,f601]) ).
fof(f923,definition,
( sQ41_spl
<=> element(sK9_skl,powerset(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f926,plain,
( ~ sQ38_spl
| sQ26_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f913,f923,f603,f869]) ).
fof(f927,definition,
( sQ42_spl
<=> in(sK9_skl,sK8_skl(powerset(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f928,plain,
( ~ sQ42_spl
| in(sK9_skl,sK8_skl(powerset(sK9_skl))) ),
inference(component_clause,[status(thm)],[f927]) ).
fof(f930,plain,
( ~ sQ38_spl
| sQ42_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f914,f603,f927,f869]) ).
fof(f931,definition,
( sQ43_spl
<=> in(sK8_skl(powerset(sK9_skl)),sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f935,definition,
( sQ44_spl
<=> empty(sK8_skl(powerset(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f936,plain,
( ~ sQ44_spl
| empty(sK8_skl(powerset(sK9_skl))) ),
inference(component_clause,[status(thm)],[f935]) ).
fof(f938,plain,
( ~ sQ38_spl
| ~ sQ43_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f916,f935,f931,f869]) ).
fof(f940,definition,
( sQ45_spl
<=> sK8_skl(powerset(sK9_skl)) = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f941,plain,
( ~ sQ45_spl
| sK8_skl(powerset(sK9_skl)) = sK9_skl ),
inference(component_clause,[status(thm)],[f940]) ).
fof(f976,plain,
( ~ in(sK11_skl,sK6_skl(sK8_skl(sK8_skl(sK11_skl))))
| empty(sK11_skl) ),
inference(resolution,[status(thm)],[f902,f597]) ).
fof(f977,plain,
! [X0] :
( in(sK6_skl(sK8_skl(sK8_skl(X0))),X0)
| X0 = sK9_skl
| empty(X0) ),
inference(resolution,[status(thm)],[f902,f165]) ).
fof(f978,plain,
! [X0] :
( in(sK6_skl(sK8_skl(sK8_skl(X0))),X0)
| empty(X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f902,f131]) ).
fof(f988,definition,
! [X0] :
( sQ47_spl
<=> ~ in(X0,sK6_skl(sK8_skl(sK8_skl(powerset(sK9_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f989,plain,
! [X0] :
( ~ sQ47_spl
| ~ in(X0,sK6_skl(sK8_skl(sK8_skl(powerset(sK9_skl))))) ),
inference(component_clause,[status(thm)],[f988]) ).
fof(f995,definition,
( sQ48_spl
<=> in(sK11_skl,sK6_skl(sK8_skl(sK8_skl(sK11_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f998,plain,
( ~ sQ48_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f976,f876,f995]) ).
fof(f999,plain,
! [X0] :
( in(sK6_skl(sK8_skl(sK8_skl(X0))),X0)
| X0 = sK9_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f977,f162]) ).
fof(f1000,plain,
! [X0] :
( in(sK6_skl(sK8_skl(sK8_skl(X0))),X0)
| empty(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f978]) ).
fof(f1004,plain,
! [X0] :
( ~ in(X0,sK6_skl(sK8_skl(sK8_skl(powerset(sK9_skl)))))
| powerset(sK9_skl) = sK9_skl ),
inference(resolution,[status(thm)],[f999,f357]) ).
fof(f1009,plain,
( sQ47_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f1004,f416,f988]) ).
fof(f1010,plain,
! [X0] :
( empty(X0)
| element(sK6_skl(sK8_skl(sK8_skl(sK8_skl(X0)))),X0)
| empty(sK8_skl(X0)) ),
inference(resolution,[status(thm)],[f1000,f740]) ).
fof(f1017,plain,
! [X0] :
( empty(X0)
| element(sK6_skl(sK8_skl(sK8_skl(sK8_skl(X0)))),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1010,f99]) ).
fof(f1020,plain,
( ~ sQ47_spl
| sK6_skl(sK8_skl(sK8_skl(powerset(sK9_skl)))) = sK9_skl ),
inference(resolution,[status(thm)],[f989,f999]) ).
fof(f1036,plain,
( ~ sQ47_spl
| empty(sK8_skl(powerset(sK9_skl)))
| element(sK9_skl,sK8_skl(powerset(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f1020,f846]) ).
fof(f1037,plain,
( ~ sQ47_spl
| in(sK9_skl,sK8_skl(sK8_skl(powerset(sK9_skl))))
| empty(sK8_skl(powerset(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f1020,f427]) ).
fof(f1042,plain,
( ~ sQ47_spl
| ~ in(sK8_skl(sK8_skl(powerset(sK9_skl))),sK9_skl)
| sK8_skl(sK8_skl(powerset(sK9_skl))) = sK9_skl ),
inference(paramodulation,[status(thm)],[f1020,f259]) ).
fof(f1051,definition,
( sQ49_spl
<=> element(sK9_skl,sK8_skl(powerset(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1054,plain,
( ~ sQ47_spl
| sQ44_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1036,f1051,f935,f988]) ).
fof(f1055,definition,
( sQ50_spl
<=> in(sK9_skl,sK8_skl(sK8_skl(powerset(sK9_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1056,plain,
( ~ sQ50_spl
| in(sK9_skl,sK8_skl(sK8_skl(powerset(sK9_skl)))) ),
inference(component_clause,[status(thm)],[f1055]) ).
fof(f1058,plain,
( ~ sQ47_spl
| sQ50_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1037,f935,f1055,f988]) ).
fof(f1059,definition,
( sQ51_spl
<=> in(sK8_skl(sK8_skl(powerset(sK9_skl))),sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1063,definition,
( sQ52_spl
<=> empty(sK8_skl(sK8_skl(powerset(sK9_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1064,plain,
( ~ sQ52_spl
| empty(sK8_skl(sK8_skl(powerset(sK9_skl)))) ),
inference(component_clause,[status(thm)],[f1063]) ).
fof(f1068,definition,
( sQ53_spl
<=> sK8_skl(sK8_skl(powerset(sK9_skl))) = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1069,plain,
( ~ sQ53_spl
| sK8_skl(sK8_skl(powerset(sK9_skl))) = sK9_skl ),
inference(component_clause,[status(thm)],[f1068]) ).
fof(f1072,plain,
( ~ sQ47_spl
| ~ sQ51_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f1042,f1068,f1059,f988]) ).
fof(f1076,plain,
! [X0] :
( ~ sQ44_spl
| ~ in(X0,sK8_skl(powerset(sK9_skl))) ),
inference(resolution,[status(thm)],[f936,f146]) ).
fof(f1080,plain,
( ~ sQ42_spl
| ~ sQ44_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f928,f1076]) ).
fof(f1091,plain,
( ~ sQ42_spl
| ~ sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f1080]) ).
fof(f1251,plain,
! [X0,X1,X2,X3] :
( ~ sQ33_spl
| ~ element(the_InternalRel(sK12_skl),powerset(cartesian_product2(X2,X3)))
| in(ordered_pair(X1,sK14_skl),the_InternalRel(sK12_skl))
| ~ in(ordered_pair(X1,sK13_skl),the_InternalRel(sK12_skl))
| ~ in(sK14_skl,X0)
| ~ in(sK13_skl,X0)
| ~ in(X1,X0)
| ~ is_transitive_in(the_InternalRel(sK12_skl),X0) ),
inference(resolution,[status(thm)],[f260,f763]) ).
fof(f1252,plain,
! [X0,X1,X2,X3] :
( ~ sQ31_spl
| ~ element(the_InternalRel(sK12_skl),powerset(cartesian_product2(X2,X3)))
| in(ordered_pair(X1,sK15_skl),the_InternalRel(sK12_skl))
| ~ in(ordered_pair(X1,sK14_skl),the_InternalRel(sK12_skl))
| ~ in(sK15_skl,X0)
| ~ in(sK14_skl,X0)
| ~ in(X1,X0)
| ~ is_transitive_in(the_InternalRel(sK12_skl),X0) ),
inference(resolution,[status(thm)],[f260,f756]) ).
fof(f1256,definition,
! [X0,X1] :
( sQ54_spl
<=> ( in(ordered_pair(X1,sK14_skl),the_InternalRel(sK12_skl))
| ~ in(ordered_pair(X1,sK13_skl),the_InternalRel(sK12_skl))
| ~ in(sK14_skl,X0)
| ~ in(sK13_skl,X0)
| ~ in(X1,X0)
| ~ is_transitive_in(the_InternalRel(sK12_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1259,definition,
! [X2,X3] :
( sQ55_spl
<=> ~ element(the_InternalRel(sK12_skl),powerset(cartesian_product2(X2,X3))) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1260,plain,
! [X0,X1] :
( ~ sQ55_spl
| ~ element(the_InternalRel(sK12_skl),powerset(cartesian_product2(X0,X1))) ),
inference(component_clause,[status(thm)],[f1259]) ).
fof(f1262,plain,
( ~ sQ33_spl
| sQ55_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1251,f1256,f1259,f762]) ).
fof(f1263,definition,
! [X0,X1] :
( sQ56_spl
<=> ( in(ordered_pair(X1,sK15_skl),the_InternalRel(sK12_skl))
| ~ in(ordered_pair(X1,sK14_skl),the_InternalRel(sK12_skl))
| ~ in(sK15_skl,X0)
| ~ in(sK14_skl,X0)
| ~ in(X1,X0)
| ~ is_transitive_in(the_InternalRel(sK12_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1264,plain,
! [X0,X1] :
( ~ sQ56_spl
| in(ordered_pair(X1,sK15_skl),the_InternalRel(sK12_skl))
| ~ in(ordered_pair(X1,sK14_skl),the_InternalRel(sK12_skl))
| ~ in(sK15_skl,X0)
| ~ in(sK14_skl,X0)
| ~ in(X1,X0)
| ~ is_transitive_in(the_InternalRel(sK12_skl),X0) ),
inference(component_clause,[status(thm)],[f1263]) ).
fof(f1266,plain,
( ~ sQ31_spl
| sQ55_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1252,f1263,f1259,f755]) ).
fof(f1274,plain,
! [X0,X1] :
( ~ sQ55_spl
| ~ relation_of2_as_subset(the_InternalRel(sK12_skl),X0,X1) ),
inference(resolution,[status(thm)],[f1260,f77]) ).
fof(f1277,plain,
( ~ sQ55_spl
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f1274,f79]) ).
fof(f1279,plain,
( ~ sQ55_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1277,f209,f1259]) ).
fof(f1280,plain,
! [X0] :
( ~ sQ33_spl
| ~ sQ56_spl
| in(ordered_pair(sK13_skl,sK15_skl),the_InternalRel(sK12_skl))
| ~ in(sK15_skl,X0)
| ~ in(sK14_skl,X0)
| ~ in(sK13_skl,X0)
| ~ is_transitive_in(the_InternalRel(sK12_skl),X0) ),
inference(resolution,[status(thm)],[f1264,f763]) ).
fof(f1281,definition,
! [X0] :
( sQ59_spl
<=> ( ~ in(sK15_skl,X0)
| ~ in(sK14_skl,X0)
| ~ in(sK13_skl,X0)
| ~ is_transitive_in(the_InternalRel(sK12_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1282,plain,
! [X0] :
( ~ sQ59_spl
| ~ in(sK15_skl,X0)
| ~ in(sK14_skl,X0)
| ~ in(sK13_skl,X0)
| ~ is_transitive_in(the_InternalRel(sK12_skl),X0) ),
inference(component_clause,[status(thm)],[f1281]) ).
fof(f1284,definition,
( sQ60_spl
<=> in(ordered_pair(sK13_skl,sK15_skl),the_InternalRel(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1285,plain,
( ~ sQ60_spl
| in(ordered_pair(sK13_skl,sK15_skl),the_InternalRel(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1284]) ).
fof(f1287,plain,
( ~ sQ33_spl
| ~ sQ56_spl
| sQ60_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1280,f1281,f1284,f1263,f762]) ).
fof(f1288,plain,
( ~ sQ2_spl
| ~ sQ59_spl
| ~ in(sK15_skl,the_carrier(sK12_skl))
| ~ in(sK13_skl,the_carrier(sK12_skl))
| ~ is_transitive_in(the_InternalRel(sK12_skl),the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f1282,f198]) ).
fof(f1294,definition,
( sQ61_spl
<=> is_transitive_in(the_InternalRel(sK12_skl),the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1296,plain,
( sQ61_spl
| ~ is_transitive_in(the_InternalRel(sK12_skl),the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1294]) ).
fof(f1297,plain,
( ~ sQ2_spl
| ~ sQ59_spl
| ~ sQ1_spl
| ~ sQ3_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f1288,f1294,f201,f193,f1281,f197]) ).
fof(f1323,plain,
( ~ sQ42_spl
| ~ sQ45_spl
| in(sK9_skl,sK9_skl) ),
inference(backward_demodulation,[status(thm)],[f941,f928]) ).
fof(f1326,plain,
( ~ sQ42_spl
| ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1323,f354]) ).
fof(f1327,plain,
( ~ sQ42_spl
| ~ sQ45_spl ),
inference(contradiction_clause,[status(thm)],[f1326]) ).
fof(f1330,plain,
( sQ61_spl
| ~ transitive_relstr(sK12_skl)
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f1296,f56]) ).
fof(f1336,plain,
( sQ61_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1330,f209,f212,f1294]) ).
fof(f1337,definition,
( sQ68_spl
<=> relation(the_InternalRel(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1339,plain,
( sQ68_spl
| ~ relation(the_InternalRel(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1337]) ).
fof(f1360,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f214,f122]) ).
fof(f1361,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1360]) ).
fof(f1372,plain,
! [X0,X1] :
( sQ68_spl
| ~ element(the_InternalRel(sK12_skl),powerset(cartesian_product2(X0,X1))) ),
inference(resolution,[status(thm)],[f1339,f52]) ).
fof(f1373,plain,
( sQ68_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1372,f1259,f1337]) ).
fof(f1374,plain,
( ~ sQ0_spl
| relation_of2_as_subset(the_InternalRel(sK12_skl),the_carrier(sK12_skl),sK9_skl)
| ~ rel_str(sK12_skl) ),
inference(paramodulation,[status(thm)],[f191,f79]) ).
fof(f1377,definition,
( sQ74_spl
<=> relation_of2_as_subset(the_InternalRel(sK12_skl),the_carrier(sK12_skl),sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1378,plain,
( ~ sQ74_spl
| relation_of2_as_subset(the_InternalRel(sK12_skl),the_carrier(sK12_skl),sK9_skl) ),
inference(component_clause,[status(thm)],[f1377]) ).
fof(f1380,plain,
( ~ sQ0_spl
| sQ74_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1374,f209,f1377,f190]) ).
fof(f1386,plain,
( ~ sQ74_spl
| ~ sQ0_spl
| relation_of2_as_subset(the_InternalRel(sK12_skl),sK9_skl,sK9_skl) ),
inference(forward_demodulation,[status(thm)],[f191,f1378]) ).
fof(f1398,definition,
( sQ76_spl
<=> in(sK13_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1399,plain,
( ~ sQ76_spl
| in(sK13_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f1398]) ).
fof(f1403,plain,
( ~ sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1399,f354]) ).
fof(f1404,plain,
~ sQ76_spl,
inference(contradiction_clause,[status(thm)],[f1403]) ).
fof(f1407,definition,
( sQ77_spl
<=> element(sK14_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1409,plain,
( sQ77_spl
| ~ element(sK14_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f1407]) ).
fof(f1410,definition,
( sQ78_spl
<=> element(sK15_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1412,plain,
( sQ78_spl
| ~ element(sK15_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f1410]) ).
fof(f1418,plain,
( sQ77_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1409,f206]) ).
fof(f1419,plain,
( sQ77_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f1418]) ).
fof(f1421,plain,
! [X0,X1,X2] :
( in(X2,the_InternalRel(sK12_skl))
| ~ element(X2,the_InternalRel(sK12_skl))
| ~ related(sK12_skl,X0,X1)
| ~ element(X1,the_carrier(sK12_skl))
| ~ element(X0,the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f310,f123]) ).
fof(f1429,definition,
! [X0,X1] :
( sQ82_spl
<=> ( ~ related(sK12_skl,X0,X1)
| ~ element(X1,the_carrier(sK12_skl))
| ~ element(X0,the_carrier(sK12_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1430,plain,
! [X0,X1] :
( ~ sQ82_spl
| ~ related(sK12_skl,X0,X1)
| ~ element(X1,the_carrier(sK12_skl))
| ~ element(X0,the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1429]) ).
fof(f1432,definition,
! [X2] :
( sQ83_spl
<=> ( in(X2,the_InternalRel(sK12_skl))
| ~ element(X2,the_InternalRel(sK12_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1433,plain,
! [X0] :
( ~ sQ83_spl
| in(X0,the_InternalRel(sK12_skl))
| ~ element(X0,the_InternalRel(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1432]) ).
fof(f1435,plain,
( sQ83_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f1421,f1429,f1432]) ).
fof(f1436,plain,
! [X0,X1] :
( ~ sQ82_spl
| ~ sQ0_spl
| ~ related(sK12_skl,X0,X1)
| ~ element(X1,the_carrier(sK12_skl))
| ~ element(X0,sK9_skl) ),
inference(forward_demodulation,[status(thm)],[f191,f1430]) ).
fof(f1437,plain,
! [X0,X1] :
( ~ sQ82_spl
| ~ sQ0_spl
| ~ related(sK12_skl,X0,X1)
| ~ element(X1,sK9_skl)
| ~ element(X0,sK9_skl) ),
inference(forward_demodulation,[status(thm)],[f191,f1436]) ).
fof(f1474,plain,
( ~ sQ74_spl
| ~ sQ0_spl
| in(the_InternalRel(sK12_skl),powerset(cartesian_product2(sK9_skl,sK9_skl))) ),
inference(resolution,[status(thm)],[f1386,f586]) ).
fof(f1585,plain,
! [X0] :
( ~ sQ74_spl
| ~ sQ0_spl
| element(X0,cartesian_product2(sK9_skl,sK9_skl))
| ~ in(X0,the_InternalRel(sK12_skl)) ),
inference(resolution,[status(thm)],[f1474,f745]) ).
fof(f1587,plain,
( ~ sQ82_spl
| ~ sQ0_spl
| ~ element(sK15_skl,sK9_skl)
| ~ element(sK14_skl,sK9_skl) ),
inference(resolution,[status(thm)],[f1437,f128]) ).
fof(f1589,plain,
( ~ sQ82_spl
| ~ sQ0_spl
| ~ sQ78_spl
| ~ sQ77_spl ),
inference(split_clause,[status(thm)],[f1587,f1407,f1410,f190,f1429]) ).
fof(f1591,plain,
( sQ78_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1412,f205]) ).
fof(f1592,plain,
( sQ78_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f1591]) ).
fof(f1595,plain,
( ~ sQ83_spl
| empty(the_InternalRel(sK12_skl))
| in(sK6_skl(sK8_skl(sK8_skl(the_InternalRel(sK12_skl)))),the_InternalRel(sK12_skl)) ),
inference(resolution,[status(thm)],[f1433,f902]) ).
fof(f1596,plain,
( ~ sQ83_spl
| empty(the_InternalRel(sK12_skl))
| in(sK6_skl(sK8_skl(the_InternalRel(sK12_skl))),the_InternalRel(sK12_skl)) ),
inference(resolution,[status(thm)],[f1433,f846]) ).
fof(f1597,plain,
( ~ sQ83_spl
| in(sK6_skl(the_InternalRel(sK12_skl)),the_InternalRel(sK12_skl)) ),
inference(resolution,[status(thm)],[f1433,f87]) ).
fof(f1599,definition,
( sQ84_spl
<=> in(sK6_skl(sK8_skl(sK8_skl(the_InternalRel(sK12_skl)))),the_InternalRel(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1602,definition,
( sQ85_spl
<=> empty(the_InternalRel(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1603,plain,
( ~ sQ85_spl
| empty(the_InternalRel(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1602]) ).
fof(f1605,plain,
( ~ sQ83_spl
| sQ85_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1595,f1599,f1602,f1432]) ).
fof(f1606,definition,
( sQ86_spl
<=> in(sK6_skl(sK8_skl(the_InternalRel(sK12_skl))),the_InternalRel(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1609,plain,
( ~ sQ83_spl
| sQ85_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f1596,f1606,f1602,f1432]) ).
fof(f1613,plain,
! [X0] :
( ~ sQ85_spl
| ~ in(X0,the_InternalRel(sK12_skl)) ),
inference(resolution,[status(thm)],[f1603,f146]) ).
fof(f1618,plain,
( ~ sQ33_spl
| ~ sQ85_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f763,f1613]) ).
fof(f1640,plain,
( ~ sQ33_spl
| ~ sQ85_spl ),
inference(contradiction_clause,[status(thm)],[f1618]) ).
fof(f1714,plain,
( ~ sQ83_spl
| in(sK6_skl(sK8_skl(sK8_skl(sK8_skl(the_InternalRel(sK12_skl))))),the_InternalRel(sK12_skl))
| empty(the_InternalRel(sK12_skl)) ),
inference(resolution,[status(thm)],[f1017,f1433]) ).
fof(f1725,plain,
( ~ in(sK11_skl,sK6_skl(sK8_skl(sK8_skl(sK8_skl(sK11_skl)))))
| empty(sK11_skl) ),
inference(resolution,[status(thm)],[f1017,f597]) ).
fof(f1727,plain,
! [X0] :
( in(sK6_skl(sK8_skl(sK8_skl(sK8_skl(X0)))),X0)
| X0 = sK9_skl
| empty(X0) ),
inference(resolution,[status(thm)],[f1017,f165]) ).
fof(f1729,definition,
( sQ90_spl
<=> in(sK6_skl(sK8_skl(sK8_skl(sK8_skl(the_InternalRel(sK12_skl))))),the_InternalRel(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1732,plain,
( ~ sQ83_spl
| sQ90_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f1714,f1602,f1729,f1432]) ).
fof(f1739,definition,
! [X0] :
( sQ91_spl
<=> ~ in(X0,sK6_skl(sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1740,plain,
! [X0] :
( ~ sQ91_spl
| ~ in(X0,sK6_skl(sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl)))))) ),
inference(component_clause,[status(thm)],[f1739]) ).
fof(f1746,definition,
( sQ92_spl
<=> in(sK11_skl,sK6_skl(sK8_skl(sK8_skl(sK8_skl(sK11_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1749,plain,
( ~ sQ92_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f1725,f876,f1746]) ).
fof(f1751,plain,
! [X0] :
( in(sK6_skl(sK8_skl(sK8_skl(sK8_skl(X0)))),X0)
| X0 = sK9_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f1727,f162]) ).
fof(f1757,plain,
! [X0] :
( ~ in(X0,sK6_skl(sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl))))))
| powerset(sK9_skl) = sK9_skl ),
inference(resolution,[status(thm)],[f1751,f357]) ).
fof(f1763,plain,
( sQ91_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f1757,f416,f1739]) ).
fof(f1775,plain,
( ~ sQ91_spl
| sK6_skl(sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl))))) = sK9_skl ),
inference(resolution,[status(thm)],[f1740,f1751]) ).
fof(f1801,plain,
( ~ sQ91_spl
| empty(sK8_skl(sK8_skl(powerset(sK9_skl))))
| element(sK9_skl,sK8_skl(sK8_skl(powerset(sK9_skl)))) ),
inference(paramodulation,[status(thm)],[f1775,f846]) ).
fof(f1802,plain,
( ~ sQ91_spl
| in(sK9_skl,sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl)))))
| empty(sK8_skl(sK8_skl(powerset(sK9_skl)))) ),
inference(paramodulation,[status(thm)],[f1775,f427]) ).
fof(f1807,plain,
( ~ sQ91_spl
| ~ in(sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl)))),sK9_skl)
| sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl)))) = sK9_skl ),
inference(paramodulation,[status(thm)],[f1775,f259]) ).
fof(f1823,definition,
( sQ93_spl
<=> element(sK9_skl,sK8_skl(sK8_skl(powerset(sK9_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1826,plain,
( ~ sQ91_spl
| sQ52_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f1801,f1823,f1063,f1739]) ).
fof(f1827,definition,
( sQ94_spl
<=> in(sK9_skl,sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1828,plain,
( ~ sQ94_spl
| in(sK9_skl,sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl))))) ),
inference(component_clause,[status(thm)],[f1827]) ).
fof(f1830,plain,
( ~ sQ91_spl
| sQ94_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1802,f1063,f1827,f1739]) ).
fof(f1831,definition,
( sQ95_spl
<=> in(sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl)))),sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1840,definition,
( sQ97_spl
<=> sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl)))) = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1841,plain,
( ~ sQ97_spl
| sK8_skl(sK8_skl(sK8_skl(powerset(sK9_skl)))) = sK9_skl ),
inference(component_clause,[status(thm)],[f1840]) ).
fof(f1844,plain,
( ~ sQ91_spl
| ~ sQ95_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f1807,f1840,f1831,f1739]) ).
fof(f1847,plain,
( ~ sQ50_spl
| ~ sQ53_spl
| in(sK9_skl,sK9_skl) ),
inference(backward_demodulation,[status(thm)],[f1069,f1056]) ).
fof(f1858,plain,
( ~ sQ50_spl
| ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1847,f354]) ).
fof(f1859,plain,
( ~ sQ50_spl
| ~ sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f1858]) ).
fof(f1864,plain,
( ~ sQ94_spl
| ~ sQ97_spl
| in(sK9_skl,sK9_skl) ),
inference(forward_demodulation,[status(thm)],[f1841,f1828]) ).
fof(f1865,plain,
( ~ sQ94_spl
| ~ sQ97_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1864,f354]) ).
fof(f1866,plain,
( ~ sQ94_spl
| ~ sQ97_spl ),
inference(contradiction_clause,[status(thm)],[f1865]) ).
fof(f1956,plain,
! [X0] :
( ~ sQ74_spl
| ~ sQ0_spl
| in(X0,cartesian_product2(sK9_skl,sK9_skl))
| cartesian_product2(sK9_skl,sK9_skl) = sK9_skl
| ~ in(X0,the_InternalRel(sK12_skl)) ),
inference(resolution,[status(thm)],[f1585,f165]) ).
fof(f1958,definition,
! [X0] :
( sQ98_spl
<=> ( in(X0,cartesian_product2(sK9_skl,sK9_skl))
| ~ in(X0,the_InternalRel(sK12_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1959,plain,
! [X0] :
( ~ sQ98_spl
| in(X0,cartesian_product2(sK9_skl,sK9_skl))
| ~ in(X0,the_InternalRel(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1958]) ).
fof(f1966,definition,
( sQ100_spl
<=> cartesian_product2(sK9_skl,sK9_skl) = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1967,plain,
( ~ sQ100_spl
| cartesian_product2(sK9_skl,sK9_skl) = sK9_skl ),
inference(component_clause,[status(thm)],[f1966]) ).
fof(f1969,plain,
( ~ sQ74_spl
| ~ sQ0_spl
| sQ100_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1956,f1958,f1966,f190,f1377]) ).
fof(f1977,plain,
! [X0,X1] :
( ~ sQ98_spl
| in(X0,sK9_skl)
| ~ in(ordered_pair(X0,X1),the_InternalRel(sK12_skl)) ),
inference(resolution,[status(thm)],[f1959,f115]) ).
fof(f1989,plain,
( ~ sQ31_spl
| ~ sQ98_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f756,f1991]) ).
fof(f1991,plain,
! [X0,X1] :
( ~ sQ98_spl
| ~ in(ordered_pair(X0,X1),the_InternalRel(sK12_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1977,f354]) ).
fof(f1999,plain,
( ~ sQ31_spl
| ~ sQ98_spl ),
inference(contradiction_clause,[status(thm)],[f1989]) ).
fof(f2001,plain,
( ~ sQ74_spl
| ~ sQ0_spl
| ~ sQ100_spl
| in(the_InternalRel(sK12_skl),powerset(sK9_skl)) ),
inference(backward_demodulation,[status(thm)],[f1967,f1474]) ).
fof(f2045,plain,
( ~ sQ52_spl
| empty(sK8_skl(powerset(sK9_skl))) ),
inference(resolution,[status(thm)],[f1064,f99]) ).
fof(f2051,plain,
( ~ sQ52_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f2045,f935,f1063]) ).
fof(f2055,plain,
! [X0] :
( ~ sQ74_spl
| ~ sQ0_spl
| ~ sQ100_spl
| ~ in(X0,the_InternalRel(sK12_skl)) ),
inference(resolution,[status(thm)],[f2001,f357]) ).
fof(f2060,plain,
( ~ sQ83_spl
| ~ sQ74_spl
| ~ sQ0_spl
| ~ sQ100_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1597,f2055]) ).
fof(f2066,plain,
( ~ sQ83_spl
| ~ sQ74_spl
| ~ sQ0_spl
| ~ sQ100_spl ),
inference(contradiction_clause,[status(thm)],[f2060]) ).
fof(f2149,plain,
( ~ sQ60_spl
| related(sK12_skl,sK13_skl,sK15_skl)
| ~ element(sK15_skl,the_carrier(sK12_skl))
| ~ element(sK13_skl,the_carrier(sK12_skl))
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f1285,f73]) ).
fof(f2152,definition,
( sQ109_spl
<=> related(sK12_skl,sK13_skl,sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f2153,plain,
( ~ sQ109_spl
| related(sK12_skl,sK13_skl,sK15_skl) ),
inference(component_clause,[status(thm)],[f2152]) ).
fof(f2155,plain,
( ~ sQ60_spl
| sQ109_spl
| ~ sQ30_spl
| ~ sQ32_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2149,f209,f759,f752,f2152,f1284]) ).
fof(f2160,plain,
( ~ sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2153,f129]) ).
fof(f2161,plain,
~ sQ109_spl,
inference(contradiction_clause,[status(thm)],[f2160]) ).
fof(f2162,plain,
$false,
inference(sat_refutation,[status(thm)],[f196,f235,f239,f269,f282,f419,f423,f451,f462,f466,f581,f582,f758,f765,f767,f769,f771,f773,f779,f781,f787,f882,f886,f894,f926,f930,f938,f998,f1009,f1054,f1058,f1072,f1091,f1262,f1266,f1279,f1287,f1297,f1327,f1336,f1361,f1373,f1380,f1404,f1419,f1435,f1589,f1592,f1605,f1609,f1640,f1732,f1749,f1763,f1826,f1830,f1844,f1859,f1866,f1969,f1999,f2051,f2066,f2155,f2161]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU340+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.37 % Computer : n009.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Mon Sep 21 06:13:28 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 0.17/0.51 % Refutation found
% 0.17/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.17/0.57 % Elapsed time: 0.177680 seconds
% 0.17/0.57 % CPU time: 0.732042 seconds
% 0.17/0.57 % Total memory used: 112.833 MB
% 0.17/0.57 % Net memory used: 112.043 MB
%------------------------------------------------------------------------------