%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU257+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:19:55 PM UTC 2026
% Result : Theorem 15.00s 2.37s
% Output : CNFRefutation 15.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 132
% Syntax : Number of formulae : 575 ( 135 unt; 88 def)
% Number of atoms : 1411 ( 124 equ)
% Maximal formula atoms : 20 ( 2 avg)
% Number of connectives : 1366 ( 530 ~; 506 |; 187 &)
% ( 112 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 107 ( 105 usr; 89 prp; 0-2 aty)
% Number of functors : 50 ( 50 usr; 13 con; 0-4 aty)
% Number of variables : 463 ( 416 !; 47 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] :
( empty(A)
=> function(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = relation_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A] : succ(A) = set_union2(A,singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A,B] :
( ( A = empty_set
=> ( B = set_meet(A)
<=> B = empty_set ) )
& ( A != empty_set
=> ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(D,A)
=> in(C,D) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [A,B] :
( B = union(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( in(D,A)
& in(C,D) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [A] :
( relation(A)
=> ( well_ordering(A)
<=> ( well_founded_relation(A)
& connected(A)
& antisymmetric(A)
& transitive(A)
& reflexive(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A] :
( relation(A)
=> ! [B] : relation_restriction(A,B) = set_intersection2(A,cartesian_product2(B,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [A,B] :
( relation(A)
=> relation(relation_restriction(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [A] :
( relation(A)
=> relation(relation_inverse(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f117,axiom,
( ordinal(empty_set)
& epsilon_connected(empty_set)
& epsilon_transitive(empty_set)
& empty(empty_set)
& one_to_one(empty_set)
& function(empty_set)
& relation_empty_yielding(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f143,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f160,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f162,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f165,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f166,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f171,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,axiom,
? [A] :
( relation_empty_yielding(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,axiom,
? [A] :
( function(A)
& relation_empty_yielding(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,lemma,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_restriction(C,B))
<=> ( in(A,cartesian_product2(B,B))
& in(A,C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f208,lemma,
! [A,B] : subset(set_intersection2(A,B),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f210,lemma,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_field(relation_restriction(C,B)))
=> ( in(A,B)
& in(A,relation_field(C)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f212,axiom,
! [A] : set_union2(A,empty_set) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f217,lemma,
! [A,B] :
( relation(B)
=> ( subset(relation_field(relation_restriction(B,A)),A)
& subset(relation_field(relation_restriction(B,A)),relation_field(B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f223,lemma,
! [A,B] :
( relation(B)
=> ( reflexive(B)
=> reflexive(relation_restriction(B,A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f226,lemma,
! [A,B] :
( relation(B)
=> ( connected(B)
=> connected(relation_restriction(B,A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f228,lemma,
! [A,B] :
( relation(B)
=> ( transitive(B)
=> transitive(relation_restriction(B,A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f230,lemma,
! [A,B] :
( relation(B)
=> ( antisymmetric(B)
=> antisymmetric(relation_restriction(B,A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f236,lemma,
! [A] : subset(empty_set,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f239,lemma,
! [A,B] :
( relation(B)
=> ( well_founded_relation(B)
=> well_founded_relation(relation_restriction(B,A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f241,conjecture,
! [A,B] :
( relation(B)
=> ( well_ordering(B)
=> well_ordering(relation_restriction(B,A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f242,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> ( well_ordering(B)
=> well_ordering(relation_restriction(B,A)) ) ),
inference(negated_conjecture,[status(cth)],[f241]) ).
fof(f259,lemma,
! [A] :
( subset(A,empty_set)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f285,lemma,
( relation_rng(empty_set) = empty_set
& relation_dom(empty_set) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f286,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f318,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f319,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f322,plain,
! [A] :
( function(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f323,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f340,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f354,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f14]) ).
fof(f355,plain,
( ! [A,B] :
( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ! [A,B] :
( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(miniscoping,[status(thm)],[f354]) ).
fof(f358,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f403,plain,
! [A] :
( ! [B,C] :
( C = relation_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) ) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f404,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C = relation_image(A,B) )
& ( ! [D] :
( ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| in(D,C) )
& ( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f403]) ).
fof(f405,plain,
! [A] :
( ( ! [B,C] :
( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C = relation_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| in(D,C) )
& ! [D] :
( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f404]) ).
fof(f406,plain,
! [A] :
( ( ! [B,C] :
( ( ( ( in(sK12_skl(C,B,A),B)
& in(ordered_pair(sK12_skl(C,B,A),sK11_skl(C,B,A)),A) )
| in(sK11_skl(C,B,A),C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,sK11_skl(C,B,A)),A) )
| ~ in(sK11_skl(C,B,A),C) ) )
| C = relation_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| in(D,C) )
& ! [D] :
( ( in(sK10_skl(D,C,B,A),B)
& in(ordered_pair(sK10_skl(D,C,B,A),D),A) )
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(E,sK10_skl(D,C,B,A)),skolemize(D,sK11_skl(C,B,A)),skolemize(E,sK12_skl(C,B,A))],[f405]) ).
fof(f408,plain,
! [X0,X1,X2,X3] :
( in(sK10_skl(X3,X1,X2,X0),X2)
| ~ in(X3,X1)
| X1 != relation_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f406]) ).
fof(f413,plain,
! [A] :
( ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) ) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f414,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ( ! [D] :
( ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| in(D,C) )
& ( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f413]) ).
fof(f415,plain,
! [A] :
( ( ! [B,C] :
( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| in(D,C) )
& ! [D] :
( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f414]) ).
fof(f416,plain,
! [A] :
( ( ! [B,C] :
( ( ( ( in(sK15_skl(C,B,A),B)
& in(ordered_pair(sK14_skl(C,B,A),sK15_skl(C,B,A)),A) )
| in(sK14_skl(C,B,A),C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(sK14_skl(C,B,A),E),A) )
| ~ in(sK14_skl(C,B,A),C) ) )
| C = relation_inverse_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| in(D,C) )
& ! [D] :
( ( in(sK13_skl(D,C,B,A),B)
& in(ordered_pair(D,sK13_skl(D,C,B,A)),A) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(E,sK13_skl(D,C,B,A)),skolemize(D,sK14_skl(C,B,A)),skolemize(E,sK15_skl(C,B,A))],[f415]) ).
fof(f418,plain,
! [X0,X1,X2,X3] :
( in(sK13_skl(X3,X1,X2,X0),X2)
| ~ in(X3,X1)
| X1 != relation_inverse_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f441,plain,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f456,plain,
! [A,B] :
( ( ( B = set_meet(A)
<=> B = empty_set )
| A != empty_set )
& ( ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(C,D)
| ~ in(D,A) ) ) )
| A = empty_set ) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f457,plain,
! [A,B] :
( ( ( ( B != empty_set
| B = set_meet(A) )
& ( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ( ( ( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ( ! [C] :
( ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(NNF_transformation,[status(thm)],[f456]) ).
fof(f458,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(miniscoping,[status(thm)],[f457]) ).
fof(f459,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ( ( ! [D] :
( in(sK22_skl(B,A),D)
| ~ in(D,A) )
| in(sK22_skl(B,A),B) )
& ( ( ~ in(sK22_skl(B,A),sK23_skl(B,A))
& in(sK23_skl(B,A),A) )
| ~ in(sK22_skl(B,A),B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ( ~ in(C,sK21_skl(C,B,A))
& in(sK21_skl(C,B,A),A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl]),skolemize(D,sK21_skl(C,B,A)),skolemize(C,sK22_skl(B,A)),skolemize(D,sK23_skl(B,A))],[f458]) ).
fof(f466,plain,
! [X0,X1] :
( X1 = empty_set
| X1 != set_meet(X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f459]) ).
fof(f485,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f31]) ).
fof(f486,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f485]) ).
fof(f487,plain,
( ! [A] :
( in(sK26_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(B,sK26_skl(A))],[f486]) ).
fof(f488,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f487]) ).
fof(f489,plain,
! [X0] :
( in(sK26_skl(X0),X0)
| X0 = empty_set ),
inference(cnf_transformation,[status(thm)],[f487]) ).
fof(f626,plain,
! [A,B] :
( ( ? [C] :
( ( ? [D] :
( in(D,A)
& in(C,D) )
| in(C,B) )
& ( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| ~ in(C,B) ) )
| B = union(A) )
& ( ! [C] :
( ( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| in(C,B) )
& ( ? [D] :
( in(D,A)
& in(C,D) )
| ~ in(C,B) ) )
| B != union(A) ) ),
inference(NNF_transformation,[status(thm)],[f50]) ).
fof(f627,plain,
( ! [A,B] :
( ? [C] :
( ( ? [D] :
( in(D,A)
& in(C,D) )
| in(C,B) )
& ( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| ~ in(C,B) ) )
| B = union(A) )
& ! [A,B] :
( ( ! [C] :
( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| in(C,B) )
& ! [C] :
( ? [D] :
( in(D,A)
& in(C,D) )
| ~ in(C,B) ) )
| B != union(A) ) ),
inference(miniscoping,[status(thm)],[f626]) ).
fof(f628,plain,
( ! [A,B] :
( ( ( ( in(sK55_skl(B,A),A)
& in(sK54_skl(B,A),sK55_skl(B,A)) )
| in(sK54_skl(B,A),B) )
& ( ! [D] :
( ~ in(D,A)
| ~ in(sK54_skl(B,A),D) )
| ~ in(sK54_skl(B,A),B) ) )
| B = union(A) )
& ! [A,B] :
( ( ! [C] :
( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| in(C,B) )
& ! [C] :
( ( in(sK53_skl(C,B,A),A)
& in(C,sK53_skl(C,B,A)) )
| ~ in(C,B) ) )
| B != union(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53_skl,sK54_skl,sK55_skl]),skolemize(D,sK53_skl(C,B,A)),skolemize(C,sK54_skl(B,A)),skolemize(D,sK55_skl(B,A))],[f627]) ).
fof(f630,plain,
! [X0,X1,X2] :
( in(sK53_skl(X2,X0,X1),X1)
| ~ in(X2,X0)
| X0 != union(X1) ),
inference(cnf_transformation,[status(thm)],[f628]) ).
fof(f635,plain,
! [A] :
( ( well_ordering(A)
<=> ( well_founded_relation(A)
& connected(A)
& antisymmetric(A)
& transitive(A)
& reflexive(A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f636,plain,
! [A] :
( ( ( ~ well_founded_relation(A)
| ~ connected(A)
| ~ antisymmetric(A)
| ~ transitive(A)
| ~ reflexive(A)
| well_ordering(A) )
& ( ( well_founded_relation(A)
& connected(A)
& antisymmetric(A)
& transitive(A)
& reflexive(A) )
| ~ well_ordering(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f635]) ).
fof(f637,plain,
! [X0] :
( reflexive(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f638,plain,
! [X0] :
( transitive(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f639,plain,
! [X0] :
( antisymmetric(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f640,plain,
! [X0] :
( connected(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f641,plain,
! [X0] :
( well_founded_relation(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f642,plain,
! [X0] :
( ~ well_founded_relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f643,plain,
! [A,B,C] :
( ( ? [D] :
( ( ( ~ in(D,B)
& in(D,A) )
| in(D,C) )
& ( in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_difference(A,B) )
& ( ! [D] :
( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f52]) ).
fof(f644,plain,
( ! [A,B,C] :
( ? [D] :
( ( ( ~ in(D,B)
& in(D,A) )
| in(D,C) )
& ( in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_difference(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(miniscoping,[status(thm)],[f643]) ).
fof(f645,plain,
( ! [A,B,C] :
( ( ( ( ~ in(sK56_skl(C,B,A),B)
& in(sK56_skl(C,B,A),A) )
| in(sK56_skl(C,B,A),C) )
& ( in(sK56_skl(C,B,A),B)
| ~ in(sK56_skl(C,B,A),A)
| ~ in(sK56_skl(C,B,A),C) ) )
| C = set_difference(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56_skl]),skolemize(D,sK56_skl(C,B,A))],[f644]) ).
fof(f647,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,X2)
| ~ in(X3,X0)
| X0 != set_difference(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f645]) ).
fof(f698,plain,
! [A] :
( ! [B] : relation_restriction(A,B) = set_intersection2(A,cartesian_product2(B,B))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f699,plain,
! [X0,X1] :
( relation_restriction(X0,X1) = set_intersection2(X0,cartesian_product2(X1,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f698]) ).
fof(f764,plain,
! [A,B] :
( relation(relation_restriction(A,B))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f765,plain,
! [A] :
( ! [B] : relation(relation_restriction(A,B))
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f764]) ).
fof(f766,plain,
! [X0,X1] :
( relation(relation_restriction(X0,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f765]) ).
fof(f769,plain,
! [A] :
( relation(relation_inverse(A))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f770,plain,
! [X0] :
( relation(relation_inverse(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f769]) ).
fof(f796,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f797,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f817,plain,
function(empty_set),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f820,plain,
epsilon_transitive(empty_set),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f822,plain,
ordinal(empty_set),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f832,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f122]) ).
fof(f836,plain,
! [X0] :
( ordinal(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f832]) ).
fof(f890,plain,
! [X0] : singleton(X0) != empty_set,
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f959,plain,
( function(sK87_skl)
& relation(sK87_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87_skl]),skolemize(A,sK87_skl)],[f160]) ).
fof(f960,plain,
relation(sK87_skl),
inference(cnf_transformation,[status(thm)],[f959]) ).
fof(f961,plain,
function(sK87_skl),
inference(cnf_transformation,[status(thm)],[f959]) ).
fof(f962,plain,
( ordinal(sK88_skl)
& epsilon_connected(sK88_skl)
& epsilon_transitive(sK88_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK88_skl]),skolemize(A,sK88_skl)],[f161]) ).
fof(f963,plain,
epsilon_transitive(sK88_skl),
inference(cnf_transformation,[status(thm)],[f962]) ).
fof(f966,plain,
( relation(sK89_skl)
& empty(sK89_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK89_skl]),skolemize(A,sK89_skl)],[f162]) ).
fof(f967,plain,
empty(sK89_skl),
inference(cnf_transformation,[status(thm)],[f966]) ).
fof(f975,plain,
( function(sK92_skl)
& empty(sK92_skl)
& relation(sK92_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK92_skl]),skolemize(A,sK92_skl)],[f165]) ).
fof(f977,plain,
empty(sK92_skl),
inference(cnf_transformation,[status(thm)],[f975]) ).
fof(f978,plain,
function(sK92_skl),
inference(cnf_transformation,[status(thm)],[f975]) ).
fof(f979,plain,
( ordinal(sK93_skl)
& epsilon_connected(sK93_skl)
& epsilon_transitive(sK93_skl)
& empty(sK93_skl)
& one_to_one(sK93_skl)
& function(sK93_skl)
& relation(sK93_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK93_skl]),skolemize(A,sK93_skl)],[f166]) ).
fof(f981,plain,
function(sK93_skl),
inference(cnf_transformation,[status(thm)],[f979]) ).
fof(f983,plain,
empty(sK93_skl),
inference(cnf_transformation,[status(thm)],[f979]) ).
fof(f984,plain,
epsilon_transitive(sK93_skl),
inference(cnf_transformation,[status(thm)],[f979]) ).
fof(f987,plain,
( relation(sK94_skl)
& ~ empty(sK94_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK94_skl]),skolemize(A,sK94_skl)],[f167]) ).
fof(f988,plain,
~ empty(sK94_skl),
inference(cnf_transformation,[status(thm)],[f987]) ).
fof(f989,plain,
relation(sK94_skl),
inference(cnf_transformation,[status(thm)],[f987]) ).
fof(f995,plain,
( one_to_one(sK97_skl)
& function(sK97_skl)
& relation(sK97_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK97_skl]),skolemize(A,sK97_skl)],[f170]) ).
fof(f996,plain,
relation(sK97_skl),
inference(cnf_transformation,[status(thm)],[f995]) ).
fof(f997,plain,
function(sK97_skl),
inference(cnf_transformation,[status(thm)],[f995]) ).
fof(f999,plain,
( ordinal(sK98_skl)
& epsilon_connected(sK98_skl)
& epsilon_transitive(sK98_skl)
& ~ empty(sK98_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK98_skl]),skolemize(A,sK98_skl)],[f171]) ).
fof(f1001,plain,
epsilon_transitive(sK98_skl),
inference(cnf_transformation,[status(thm)],[f999]) ).
fof(f1004,plain,
( relation_empty_yielding(sK99_skl)
& relation(sK99_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK99_skl]),skolemize(A,sK99_skl)],[f172]) ).
fof(f1005,plain,
relation(sK99_skl),
inference(cnf_transformation,[status(thm)],[f1004]) ).
fof(f1007,plain,
( function(sK100_skl)
& relation_empty_yielding(sK100_skl)
& relation(sK100_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK100_skl]),skolemize(A,sK100_skl)],[f173]) ).
fof(f1008,plain,
relation(sK100_skl),
inference(cnf_transformation,[status(thm)],[f1007]) ).
fof(f1010,plain,
function(sK100_skl),
inference(cnf_transformation,[status(thm)],[f1007]) ).
fof(f1111,plain,
! [A,B,C] :
( ( in(A,relation_restriction(C,B))
<=> ( in(A,cartesian_product2(B,B))
& in(A,C) ) )
| ~ relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f204]) ).
fof(f1112,plain,
! [A,B,C] :
( ( ( ~ in(A,cartesian_product2(B,B))
| ~ in(A,C)
| in(A,relation_restriction(C,B)) )
& ( ( in(A,cartesian_product2(B,B))
& in(A,C) )
| ~ in(A,relation_restriction(C,B)) ) )
| ~ relation(C) ),
inference(NNF_transformation,[status(thm)],[f1111]) ).
fof(f1113,plain,
! [C] :
( ( ! [A,B] :
( ~ in(A,cartesian_product2(B,B))
| ~ in(A,C)
| in(A,relation_restriction(C,B)) )
& ! [A,B] :
( ( in(A,cartesian_product2(B,B))
& in(A,C) )
| ~ in(A,relation_restriction(C,B)) ) )
| ~ relation(C) ),
inference(miniscoping,[status(thm)],[f1112]) ).
fof(f1114,plain,
! [X0,X1,X2] :
( in(X1,X0)
| ~ in(X1,relation_restriction(X0,X2))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1113]) ).
fof(f1126,plain,
! [X0,X1] : subset(set_intersection2(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f1130,plain,
! [A,B,C] :
( ( in(A,B)
& in(A,relation_field(C)) )
| ~ in(A,relation_field(relation_restriction(C,B)))
| ~ relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f210]) ).
fof(f1131,plain,
! [C] :
( ! [A,B] :
( ( in(A,B)
& in(A,relation_field(C)) )
| ~ in(A,relation_field(relation_restriction(C,B))) )
| ~ relation(C) ),
inference(miniscoping,[status(thm)],[f1130]) ).
fof(f1132,plain,
! [X0,X1,X2] :
( in(X1,relation_field(X0))
| ~ in(X1,relation_field(relation_restriction(X0,X2)))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1131]) ).
fof(f1136,plain,
! [X0] : set_union2(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f1147,plain,
! [A,B] :
( ( subset(relation_field(relation_restriction(B,A)),A)
& subset(relation_field(relation_restriction(B,A)),relation_field(B)) )
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f217]) ).
fof(f1148,plain,
! [B] :
( ( ! [A] : subset(relation_field(relation_restriction(B,A)),A)
& ! [A] : subset(relation_field(relation_restriction(B,A)),relation_field(B)) )
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f1147]) ).
fof(f1150,plain,
! [X0,X1] :
( subset(relation_field(relation_restriction(X0,X1)),X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1148]) ).
fof(f1167,plain,
! [A,B] :
( reflexive(relation_restriction(B,A))
| ~ reflexive(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f223]) ).
fof(f1168,plain,
! [B] :
( ! [A] : reflexive(relation_restriction(B,A))
| ~ reflexive(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f1167]) ).
fof(f1169,plain,
! [X0,X1] :
( reflexive(relation_restriction(X0,X1))
| ~ reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1168]) ).
fof(f1176,plain,
! [A,B] :
( connected(relation_restriction(B,A))
| ~ connected(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f226]) ).
fof(f1177,plain,
! [B] :
( ! [A] : connected(relation_restriction(B,A))
| ~ connected(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f1176]) ).
fof(f1178,plain,
! [X0,X1] :
( connected(relation_restriction(X0,X1))
| ~ connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1177]) ).
fof(f1181,plain,
! [A,B] :
( transitive(relation_restriction(B,A))
| ~ transitive(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f228]) ).
fof(f1182,plain,
! [B] :
( ! [A] : transitive(relation_restriction(B,A))
| ~ transitive(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f1181]) ).
fof(f1183,plain,
! [X0,X1] :
( transitive(relation_restriction(X0,X1))
| ~ transitive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1182]) ).
fof(f1187,plain,
! [A,B] :
( antisymmetric(relation_restriction(B,A))
| ~ antisymmetric(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f230]) ).
fof(f1188,plain,
! [B] :
( ! [A] : antisymmetric(relation_restriction(B,A))
| ~ antisymmetric(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f1187]) ).
fof(f1189,plain,
! [X0,X1] :
( antisymmetric(relation_restriction(X0,X1))
| ~ antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1188]) ).
fof(f1203,plain,
! [X0] : subset(empty_set,X0),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f1212,plain,
! [A,B] :
( well_founded_relation(relation_restriction(B,A))
| ~ well_founded_relation(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f239]) ).
fof(f1213,plain,
! [B] :
( ! [A] : well_founded_relation(relation_restriction(B,A))
| ~ well_founded_relation(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f1212]) ).
fof(f1214,plain,
! [X0,X1] :
( well_founded_relation(relation_restriction(X0,X1))
| ~ well_founded_relation(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1213]) ).
fof(f1221,plain,
? [A,B] :
( ~ well_ordering(relation_restriction(B,A))
& well_ordering(B)
& relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f242]) ).
fof(f1222,plain,
? [B] :
( ? [A] : ~ well_ordering(relation_restriction(B,A))
& well_ordering(B)
& relation(B) ),
inference(miniscoping,[status(thm)],[f1221]) ).
fof(f1223,plain,
( ~ well_ordering(relation_restriction(sK107_skl,sK108_skl))
& well_ordering(sK107_skl)
& relation(sK107_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK107_skl,sK108_skl]),skolemize(B,sK107_skl),skolemize(A,sK108_skl)],[f1222]) ).
fof(f1224,plain,
relation(sK107_skl),
inference(cnf_transformation,[status(thm)],[f1223]) ).
fof(f1225,plain,
well_ordering(sK107_skl),
inference(cnf_transformation,[status(thm)],[f1223]) ).
fof(f1226,plain,
~ well_ordering(relation_restriction(sK107_skl,sK108_skl)),
inference(cnf_transformation,[status(thm)],[f1223]) ).
fof(f1284,plain,
! [A] :
( A = empty_set
| ~ subset(A,empty_set) ),
inference(pre_NNF_transformation,[status(thm)],[f259]) ).
fof(f1285,plain,
! [X0] :
( X0 = empty_set
| ~ subset(X0,empty_set) ),
inference(cnf_transformation,[status(thm)],[f1284]) ).
fof(f1367,plain,
relation_rng(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f1368,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f286]) ).
fof(f1369,plain,
! [X0,X1] :
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1368]) ).
fof(f1526,plain,
! [X0,X1,X2] :
( in(sK10_skl(X1,relation_image(X0,X2),X2,X0),X2)
| ~ in(X1,relation_image(X0,X2))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f408]) ).
fof(f1529,plain,
! [X0,X1,X2] :
( in(sK13_skl(X1,relation_inverse_image(X0,X2),X2,X0),X2)
| ~ in(X1,relation_inverse_image(X0,X2))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f418]) ).
fof(f1536,plain,
set_meet(empty_set) = empty_set,
inference(destructive_equality_resolution,[status(thm)],[f466]) ).
fof(f1543,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f488]) ).
fof(f1563,plain,
! [X0,X1] :
( in(sK53_skl(X0,union(X1),X1),X1)
| ~ in(X0,union(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f630]) ).
fof(f1566,plain,
! [X0,X1,X2] :
( ~ in(X0,X2)
| ~ in(X0,set_difference(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f647]) ).
fof(f1605,plain,
( transitive(sK107_skl)
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f638,f1225]) ).
fof(f1606,definition,
( sQ2_spl
<=> relation(sK107_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1608,plain,
( sQ2_spl
| ~ relation(sK107_skl) ),
inference(component_clause,[status(thm)],[f1606]) ).
fof(f1609,definition,
( sQ3_spl
<=> transitive(sK107_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1612,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1605,f1606,f1609]) ).
fof(f1613,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1608,f1224]) ).
fof(f1614,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f1613]) ).
fof(f1615,plain,
( antisymmetric(sK107_skl)
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f639,f1225]) ).
fof(f1616,definition,
( sQ4_spl
<=> antisymmetric(sK107_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1619,plain,
( sQ4_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1615,f1606,f1616]) ).
fof(f1620,plain,
( connected(sK107_skl)
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f640,f1225]) ).
fof(f1621,definition,
( sQ5_spl
<=> connected(sK107_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1624,plain,
( sQ5_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1620,f1606,f1621]) ).
fof(f1625,plain,
( well_founded_relation(sK107_skl)
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f641,f1225]) ).
fof(f1626,definition,
( sQ6_spl
<=> well_founded_relation(sK107_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1629,plain,
( sQ6_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1625,f1606,f1626]) ).
fof(f1630,plain,
! [X0] : relation_restriction(empty_set,X0) = set_intersection2(empty_set,cartesian_product2(X0,X0)),
inference(resolution,[status(thm)],[f699,f797]) ).
fof(f1633,plain,
! [X0,X1,X2] :
( ~ relation(X0)
| subset(relation_field(relation_restriction(relation_restriction(X0,X1),X2)),X2) ),
inference(resolution,[status(thm)],[f1150,f766]) ).
fof(f1637,plain,
! [X0,X1] :
( in(X0,empty_set)
| ~ in(X0,relation_restriction(empty_set,X1)) ),
inference(resolution,[status(thm)],[f1114,f797]) ).
fof(f1638,plain,
! [X0,X1] :
( in(X0,sK107_skl)
| ~ in(X0,relation_restriction(sK107_skl,X1)) ),
inference(resolution,[status(thm)],[f1114,f1224]) ).
fof(f1646,plain,
! [X0,X1] :
( ~ in(sK107_skl,X0)
| ~ in(X0,relation_restriction(sK107_skl,X1)) ),
inference(resolution,[status(thm)],[f1638,f319]) ).
fof(f1648,plain,
! [X0,X1] :
( ~ in(empty_set,X0)
| ~ in(X0,relation_restriction(empty_set,X1)) ),
inference(resolution,[status(thm)],[f1637,f319]) ).
fof(f1650,plain,
! [X0,X1] :
( ~ in(sK107_skl,relation_restriction(sK107_skl,X1))
| ~ in(sK107_skl,relation_restriction(sK107_skl,X0)) ),
inference(resolution,[status(thm)],[f1646,f1638]) ).
fof(f1658,definition,
! [X0] :
( sQ9_spl
<=> ~ in(sK107_skl,relation_restriction(sK107_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1661,plain,
sQ9_spl,
inference(split_clause,[status(thm)],[f1650,f1658]) ).
fof(f1673,definition,
( sQ10_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1675,plain,
( sQ10_spl
| ~ empty(empty_set) ),
inference(component_clause,[status(thm)],[f1673]) ).
fof(f1681,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1675,f796]) ).
fof(f1682,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1681]) ).
fof(f1685,definition,
( sQ12_spl
<=> epsilon_transitive(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1687,plain,
( sQ12_spl
| ~ epsilon_transitive(empty_set) ),
inference(component_clause,[status(thm)],[f1685]) ).
fof(f1692,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1687,f820]) ).
fof(f1693,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1692]) ).
fof(f1695,plain,
! [X0,X1] :
( ~ in(empty_set,relation_restriction(empty_set,X1))
| ~ in(empty_set,relation_restriction(empty_set,X0)) ),
inference(resolution,[status(thm)],[f1648,f1637]) ).
fof(f1697,definition,
! [X0] :
( sQ14_spl
<=> ~ in(empty_set,relation_restriction(empty_set,X0)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f1700,plain,
sQ14_spl,
inference(split_clause,[status(thm)],[f1695,f1697]) ).
fof(f1708,plain,
! [X0,X1] :
( in(X0,relation_field(sK107_skl))
| ~ in(X0,relation_field(relation_restriction(sK107_skl,X1))) ),
inference(resolution,[status(thm)],[f1132,f1224]) ).
fof(f1727,definition,
( sQ17_spl
<=> epsilon_transitive(sK88_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1729,plain,
( sQ17_spl
| ~ epsilon_transitive(sK88_skl) ),
inference(component_clause,[status(thm)],[f1727]) ).
fof(f1734,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1729,f963]) ).
fof(f1735,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f1734]) ).
fof(f1744,plain,
! [X0,X1] :
( ~ in(relation_field(sK107_skl),X0)
| ~ in(X0,relation_field(relation_restriction(sK107_skl,X1))) ),
inference(resolution,[status(thm)],[f1708,f319]) ).
fof(f1786,definition,
( sQ23_spl
<=> empty(sK92_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f1788,plain,
( sQ23_spl
| ~ empty(sK92_skl) ),
inference(component_clause,[status(thm)],[f1786]) ).
fof(f1793,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1788,f977]) ).
fof(f1794,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f1793]) ).
fof(f1821,plain,
! [X0,X1] : subset(relation_field(relation_restriction(relation_restriction(empty_set,X0),X1)),X1),
inference(resolution,[status(thm)],[f1633,f797]) ).
fof(f1836,definition,
( sQ25_spl
<=> empty(sK93_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f1838,plain,
( sQ25_spl
| ~ empty(sK93_skl) ),
inference(component_clause,[status(thm)],[f1836]) ).
fof(f1845,definition,
( sQ27_spl
<=> epsilon_transitive(sK93_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1847,plain,
( sQ27_spl
| ~ epsilon_transitive(sK93_skl) ),
inference(component_clause,[status(thm)],[f1845]) ).
fof(f1852,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1847,f984]) ).
fof(f1853,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f1852]) ).
fof(f1857,plain,
! [X0,X1] :
( ~ in(relation_field(sK107_skl),relation_field(relation_restriction(sK107_skl,X1)))
| ~ in(relation_field(sK107_skl),relation_field(relation_restriction(sK107_skl,X0))) ),
inference(resolution,[status(thm)],[f1744,f1708]) ).
fof(f1860,definition,
! [X0] :
( sQ29_spl
<=> ~ in(relation_field(sK107_skl),relation_field(relation_restriction(sK107_skl,X0))) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1863,plain,
sQ29_spl,
inference(split_clause,[status(thm)],[f1857,f1860]) ).
fof(f1970,definition,
( sQ38_spl
<=> epsilon_transitive(sK98_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1972,plain,
( sQ38_spl
| ~ epsilon_transitive(sK98_skl) ),
inference(component_clause,[status(thm)],[f1970]) ).
fof(f1977,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1972,f1001]) ).
fof(f1978,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f1977]) ).
fof(f2142,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1838,f983]) ).
fof(f2143,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f2142]) ).
fof(f2168,definition,
( sQ48_spl
<=> function(sK100_skl) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f2170,plain,
( sQ48_spl
| ~ function(sK100_skl) ),
inference(component_clause,[status(thm)],[f2168]) ).
fof(f2182,definition,
( sQ52_spl
<=> function(sK97_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f2184,plain,
( sQ52_spl
| ~ function(sK97_skl) ),
inference(component_clause,[status(thm)],[f2182]) ).
fof(f2196,definition,
( sQ56_spl
<=> function(sK93_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f2198,plain,
( sQ56_spl
| ~ function(sK93_skl) ),
inference(component_clause,[status(thm)],[f2196]) ).
fof(f2203,definition,
( sQ58_spl
<=> function(sK92_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f2205,plain,
( sQ58_spl
| ~ function(sK92_skl) ),
inference(component_clause,[status(thm)],[f2203]) ).
fof(f2210,definition,
( sQ60_spl
<=> function(sK89_skl) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f2212,plain,
( sQ60_spl
| ~ function(sK89_skl) ),
inference(component_clause,[status(thm)],[f2210]) ).
fof(f2217,definition,
( sQ62_spl
<=> function(sK87_skl) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f2219,plain,
( sQ62_spl
| ~ function(sK87_skl) ),
inference(component_clause,[status(thm)],[f2217]) ).
fof(f2224,definition,
( sQ64_spl
<=> function(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f2226,plain,
( sQ64_spl
| ~ function(empty_set) ),
inference(component_clause,[status(thm)],[f2224]) ).
fof(f2239,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2226,f817]) ).
fof(f2240,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f2239]) ).
fof(f2241,plain,
( sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2219,f961]) ).
fof(f2242,plain,
sQ62_spl,
inference(contradiction_clause,[status(thm)],[f2241]) ).
fof(f2243,plain,
( sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2205,f978]) ).
fof(f2244,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f2243]) ).
fof(f2245,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2198,f981]) ).
fof(f2246,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f2245]) ).
fof(f2247,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2184,f997]) ).
fof(f2248,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f2247]) ).
fof(f2249,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2170,f1010]) ).
fof(f2250,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f2249]) ).
fof(f2329,plain,
( sQ60_spl
| ~ empty(sK89_skl) ),
inference(resolution,[status(thm)],[f2212,f323]) ).
fof(f2330,plain,
( sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2329,f967]) ).
fof(f2331,plain,
sQ60_spl,
inference(contradiction_clause,[status(thm)],[f2330]) ).
fof(f2335,definition,
( sQ78_spl
<=> empty(sK89_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f2337,plain,
( sQ78_spl
| ~ empty(sK89_skl) ),
inference(component_clause,[status(thm)],[f2335]) ).
fof(f2342,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2337,f967]) ).
fof(f2343,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f2342]) ).
fof(f2834,definition,
( sQ132_spl
<=> subset(empty_set,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f2836,plain,
( sQ132_spl
| ~ subset(empty_set,empty_set) ),
inference(component_clause,[status(thm)],[f2834]) ).
fof(f2965,plain,
! [X0] : set_union2(empty_set,X0) = X0,
inference(paramodulation,[status(thm)],[f340,f1136]) ).
fof(f3041,definition,
( sQ162_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f3043,plain,
( sQ162_spl
| ~ relation(empty_set) ),
inference(component_clause,[status(thm)],[f3041]) ).
fof(f3052,plain,
( sQ162_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3043,f797]) ).
fof(f3053,plain,
sQ162_spl,
inference(contradiction_clause,[status(thm)],[f3052]) ).
fof(f3159,plain,
! [X0,X1] :
( in(sK10_skl(X0,relation_image(sK107_skl,X1),X1,sK107_skl),X1)
| ~ in(X0,relation_image(sK107_skl,X1)) ),
inference(resolution,[status(thm)],[f1526,f1224]) ).
fof(f3240,plain,
! [X0] : ~ in(X0,relation_image(sK107_skl,empty_set)),
inference(resolution,[status(thm)],[f3159,f1543]) ).
fof(f3293,plain,
! [X0,X1] :
( in(sK13_skl(X0,relation_inverse_image(sK107_skl,X1),X1,sK107_skl),X1)
| ~ in(X0,relation_inverse_image(sK107_skl,X1)) ),
inference(resolution,[status(thm)],[f1529,f1224]) ).
fof(f3466,plain,
! [X0] : subset(relation_restriction(empty_set,X0),empty_set),
inference(paramodulation,[status(thm)],[f1630,f1126]) ).
fof(f3530,plain,
! [X0] :
( ~ subset(empty_set,relation_restriction(empty_set,X0))
| empty_set = relation_restriction(empty_set,X0) ),
inference(resolution,[status(thm)],[f3466,f358]) ).
fof(f3531,plain,
! [X0] : empty_set = relation_restriction(empty_set,X0),
inference(forward_subsumption_resolution,[status(thm)],[f3530,f1203]) ).
fof(f3536,plain,
! [X0] : subset(relation_field(relation_restriction(empty_set,X0)),X0),
inference(backward_demodulation,[status(thm)],[f3531,f1821]) ).
fof(f3546,plain,
! [X0] : subset(relation_field(empty_set),X0),
inference(forward_demodulation,[status(thm)],[f3531,f3536]) ).
fof(f3646,plain,
succ(empty_set) = singleton(empty_set),
inference(paramodulation,[status(thm)],[f2965,f441]) ).
fof(f3678,definition,
( sQ183_spl
<=> relation(sK87_skl) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f3680,plain,
( sQ183_spl
| ~ relation(sK87_skl) ),
inference(component_clause,[status(thm)],[f3678]) ).
fof(f3685,definition,
( sQ185_spl
<=> relation(relation_field(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f3687,plain,
( sQ185_spl
| ~ relation(relation_field(empty_set)) ),
inference(component_clause,[status(thm)],[f3685]) ).
fof(f3688,definition,
! [X0] :
( sQ186_spl
<=> in(sK19_skl(relation_field(empty_set)),X0) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f3689,plain,
! [X0] :
( ~ sQ186_spl
| in(sK19_skl(relation_field(empty_set)),X0) ),
inference(component_clause,[status(thm)],[f3688]) ).
fof(f3794,plain,
! [X0] : ~ in(X0,relation_inverse_image(sK107_skl,empty_set)),
inference(resolution,[status(thm)],[f3293,f1543]) ).
fof(f4180,definition,
( sQ227_spl
<=> relation_inverse_image(sK107_skl,empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f4182,plain,
( sQ227_spl
| relation_inverse_image(sK107_skl,empty_set) != empty_set ),
inference(component_clause,[status(thm)],[f4180]) ).
fof(f4183,definition,
! [X0] :
( sQ228_spl
<=> in(X0,set_meet(relation_inverse_image(sK107_skl,empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f4184,plain,
! [X0] :
( ~ sQ228_spl
| in(X0,set_meet(relation_inverse_image(sK107_skl,empty_set))) ),
inference(component_clause,[status(thm)],[f4183]) ).
fof(f4190,definition,
! [X0] :
( sQ230_spl
<=> in(X0,set_meet(relation_image(sK107_skl,relation_image(sK107_skl,empty_set)))) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f4191,plain,
! [X0] :
( ~ sQ230_spl
| in(X0,set_meet(relation_image(sK107_skl,relation_image(sK107_skl,empty_set)))) ),
inference(component_clause,[status(thm)],[f4190]) ).
fof(f4194,definition,
( sQ231_spl
<=> relation_image(sK107_skl,empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f4196,plain,
( sQ231_spl
| relation_image(sK107_skl,empty_set) != empty_set ),
inference(component_clause,[status(thm)],[f4194]) ).
fof(f4197,definition,
! [X0] :
( sQ232_spl
<=> in(X0,set_meet(relation_image(sK107_skl,empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f4198,plain,
! [X0] :
( ~ sQ232_spl
| in(X0,set_meet(relation_image(sK107_skl,empty_set))) ),
inference(component_clause,[status(thm)],[f4197]) ).
fof(f4208,definition,
! [X0] :
( sQ235_spl
<=> in(X0,set_meet(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f4209,plain,
! [X0] :
( ~ sQ235_spl
| in(X0,set_meet(empty_set)) ),
inference(component_clause,[status(thm)],[f4208]) ).
fof(f4212,definition,
( sQ236_spl
<=> relation_field(empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f4214,plain,
( sQ236_spl
| relation_field(empty_set) != empty_set ),
inference(component_clause,[status(thm)],[f4212]) ).
fof(f4226,definition,
! [X0] :
( sQ240_spl
<=> ( in(sK21_skl(X0,empty_set,empty_set),empty_set)
| in(X0,set_meet(empty_set)) ) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f4227,plain,
! [X0] :
( ~ sQ240_spl
| in(sK21_skl(X0,empty_set,empty_set),empty_set)
| in(X0,set_meet(empty_set)) ),
inference(component_clause,[status(thm)],[f4226]) ).
fof(f5613,plain,
relation_inverse_image(sK107_skl,empty_set) = empty_set,
inference(resolution,[status(thm)],[f3794,f489]) ).
fof(f5621,plain,
( sQ227_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5613,f4182]) ).
fof(f5622,plain,
sQ227_spl,
inference(contradiction_clause,[status(thm)],[f5621]) ).
fof(f5690,plain,
relation_image(sK107_skl,empty_set) = empty_set,
inference(resolution,[status(thm)],[f3240,f489]) ).
fof(f5698,plain,
( sQ231_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5690,f4196]) ).
fof(f5699,plain,
sQ231_spl,
inference(contradiction_clause,[status(thm)],[f5698]) ).
fof(f5776,plain,
relation_field(empty_set) = empty_set,
inference(resolution,[status(thm)],[f1285,f3546]) ).
fof(f5783,plain,
( sQ236_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5776,f4214]) ).
fof(f5784,plain,
sQ236_spl,
inference(contradiction_clause,[status(thm)],[f5783]) ).
fof(f5871,plain,
( sQ185_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f5776,f3687]) ).
fof(f5872,plain,
( sQ185_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5871,f797]) ).
fof(f5873,plain,
sQ185_spl,
inference(contradiction_clause,[status(thm)],[f5872]) ).
fof(f6291,plain,
! [X0] : ~ proper_subset(X0,empty_set),
inference(resolution,[status(thm)],[f1369,f1203]) ).
fof(f6481,definition,
( sQ287_spl
<=> relation(sK99_skl) ),
introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition]) ).
fof(f6483,plain,
( sQ287_spl
| ~ relation(sK99_skl) ),
inference(component_clause,[status(thm)],[f6481]) ).
fof(f6766,plain,
succ(empty_set) != empty_set,
inference(paramodulation,[status(thm)],[f3646,f890]) ).
fof(f6890,definition,
( sQ310_spl
<=> well_ordering(sK107_skl) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f6892,plain,
( sQ310_spl
| ~ well_ordering(sK107_skl) ),
inference(component_clause,[status(thm)],[f6890]) ).
fof(f6899,plain,
( sQ310_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6892,f1225]) ).
fof(f6900,plain,
sQ310_spl,
inference(contradiction_clause,[status(thm)],[f6899]) ).
fof(f7033,definition,
( sQ315_spl
<=> subset(empty_set,sK33_skl(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition]) ).
fof(f7035,plain,
( sQ315_spl
| ~ subset(empty_set,sK33_skl(empty_set)) ),
inference(component_clause,[status(thm)],[f7033]) ).
fof(f7037,plain,
( sQ315_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7035,f1203]) ).
fof(f7038,plain,
sQ315_spl,
inference(contradiction_clause,[status(thm)],[f7037]) ).
fof(f7108,definition,
( sQ325_spl
<=> relation(sK100_skl) ),
introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition]) ).
fof(f7110,plain,
( sQ325_spl
| ~ relation(sK100_skl) ),
inference(component_clause,[status(thm)],[f7108]) ).
fof(f7448,plain,
( sQ325_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7110,f1008]) ).
fof(f7449,plain,
sQ325_spl,
inference(contradiction_clause,[status(thm)],[f7448]) ).
fof(f7679,definition,
( sQ347_spl
<=> ordinal(succ(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ347_spl])],[split_symbol_definition]) ).
fof(f7681,plain,
( sQ347_spl
| ~ ordinal(succ(empty_set)) ),
inference(component_clause,[status(thm)],[f7679]) ).
fof(f7688,plain,
( sQ347_spl
| ~ ordinal(empty_set) ),
inference(resolution,[status(thm)],[f7681,f836]) ).
fof(f7690,plain,
( sQ347_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7688,f822]) ).
fof(f7691,plain,
sQ347_spl,
inference(contradiction_clause,[status(thm)],[f7690]) ).
fof(f8186,definition,
( sQ383_spl
<=> succ(empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition]) ).
fof(f8187,plain,
( ~ sQ383_spl
| succ(empty_set) = empty_set ),
inference(component_clause,[status(thm)],[f8186]) ).
fof(f8193,plain,
( ~ sQ383_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8187,f6766]) ).
fof(f8194,plain,
~ sQ383_spl,
inference(contradiction_clause,[status(thm)],[f8193]) ).
fof(f8682,plain,
( reflexive(sK107_skl)
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f637,f1225]) ).
fof(f8683,definition,
( sQ434_spl
<=> reflexive(sK107_skl) ),
introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition]) ).
fof(f8686,plain,
( sQ434_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f8682,f1606,f8683]) ).
fof(f8999,plain,
( sQ287_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6483,f1005]) ).
fof(f9000,plain,
sQ287_spl,
inference(contradiction_clause,[status(thm)],[f8999]) ).
fof(f9558,plain,
! [X0] : ~ in(X0,union(empty_set)),
inference(resolution,[status(thm)],[f1563,f1543]) ).
fof(f9660,plain,
union(empty_set) = empty_set,
inference(resolution,[status(thm)],[f9558,f489]) ).
fof(f9677,definition,
! [X0] :
( sQ501_spl
<=> in(X0,set_meet(union(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ501_spl])],[split_symbol_definition]) ).
fof(f9678,plain,
! [X0] :
( ~ sQ501_spl
| in(X0,set_meet(union(empty_set))) ),
inference(component_clause,[status(thm)],[f9677]) ).
fof(f9683,definition,
( sQ502_spl
<=> epsilon_transitive(union(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ502_spl])],[split_symbol_definition]) ).
fof(f9685,plain,
( sQ502_spl
| ~ epsilon_transitive(union(empty_set)) ),
inference(component_clause,[status(thm)],[f9683]) ).
fof(f9877,plain,
( sQ502_spl
| ~ epsilon_transitive(empty_set) ),
inference(forward_demodulation,[status(thm)],[f9660,f9685]) ).
fof(f9878,plain,
( sQ502_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9877,f820]) ).
fof(f9879,plain,
sQ502_spl,
inference(contradiction_clause,[status(thm)],[f9878]) ).
fof(f9937,plain,
( ~ well_founded_relation(relation_restriction(sK107_skl,sK108_skl))
| ~ connected(relation_restriction(sK107_skl,sK108_skl))
| ~ antisymmetric(relation_restriction(sK107_skl,sK108_skl))
| ~ transitive(relation_restriction(sK107_skl,sK108_skl))
| ~ reflexive(relation_restriction(sK107_skl,sK108_skl))
| ~ relation(relation_restriction(sK107_skl,sK108_skl)) ),
inference(resolution,[status(thm)],[f642,f1226]) ).
fof(f9983,definition,
( sQ518_spl
<=> relation(relation_restriction(sK107_skl,sK108_skl)) ),
introduced(definition,[new_symbols(definition,[sQ518_spl])],[split_symbol_definition]) ).
fof(f9985,plain,
( sQ518_spl
| ~ relation(relation_restriction(sK107_skl,sK108_skl)) ),
inference(component_clause,[status(thm)],[f9983]) ).
fof(f9986,definition,
( sQ519_spl
<=> reflexive(relation_restriction(sK107_skl,sK108_skl)) ),
introduced(definition,[new_symbols(definition,[sQ519_spl])],[split_symbol_definition]) ).
fof(f9988,plain,
( sQ519_spl
| ~ reflexive(relation_restriction(sK107_skl,sK108_skl)) ),
inference(component_clause,[status(thm)],[f9986]) ).
fof(f9989,definition,
( sQ520_spl
<=> transitive(relation_restriction(sK107_skl,sK108_skl)) ),
introduced(definition,[new_symbols(definition,[sQ520_spl])],[split_symbol_definition]) ).
fof(f9991,plain,
( sQ520_spl
| ~ transitive(relation_restriction(sK107_skl,sK108_skl)) ),
inference(component_clause,[status(thm)],[f9989]) ).
fof(f9992,definition,
( sQ521_spl
<=> antisymmetric(relation_restriction(sK107_skl,sK108_skl)) ),
introduced(definition,[new_symbols(definition,[sQ521_spl])],[split_symbol_definition]) ).
fof(f9994,plain,
( sQ521_spl
| ~ antisymmetric(relation_restriction(sK107_skl,sK108_skl)) ),
inference(component_clause,[status(thm)],[f9992]) ).
fof(f9995,definition,
( sQ522_spl
<=> connected(relation_restriction(sK107_skl,sK108_skl)) ),
introduced(definition,[new_symbols(definition,[sQ522_spl])],[split_symbol_definition]) ).
fof(f9997,plain,
( sQ522_spl
| ~ connected(relation_restriction(sK107_skl,sK108_skl)) ),
inference(component_clause,[status(thm)],[f9995]) ).
fof(f9998,definition,
( sQ523_spl
<=> well_founded_relation(relation_restriction(sK107_skl,sK108_skl)) ),
introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition]) ).
fof(f10000,plain,
( sQ523_spl
| ~ well_founded_relation(relation_restriction(sK107_skl,sK108_skl)) ),
inference(component_clause,[status(thm)],[f9998]) ).
fof(f10001,plain,
( ~ sQ523_spl
| ~ sQ522_spl
| ~ sQ521_spl
| ~ sQ520_spl
| ~ sQ519_spl
| ~ sQ518_spl ),
inference(split_clause,[status(thm)],[f9937,f9983,f9986,f9989,f9992,f9995,f9998]) ).
fof(f10876,definition,
( sQ577_spl
<=> in(empty_set,relation_rng(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ577_spl])],[split_symbol_definition]) ).
fof(f10877,plain,
( ~ sQ577_spl
| in(empty_set,relation_rng(empty_set)) ),
inference(component_clause,[status(thm)],[f10876]) ).
fof(f10891,plain,
( ~ sQ577_spl
| in(empty_set,empty_set) ),
inference(forward_demodulation,[status(thm)],[f1367,f10877]) ).
fof(f10892,plain,
( ~ sQ577_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10891,f1543]) ).
fof(f10893,plain,
~ sQ577_spl,
inference(contradiction_clause,[status(thm)],[f10892]) ).
fof(f11158,plain,
( sQ518_spl
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f9985,f766]) ).
fof(f11160,plain,
( sQ518_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f11158,f1606,f9983]) ).
fof(f11351,definition,
( sQ608_spl
<=> relation(relation_inverse(sK97_skl)) ),
introduced(definition,[new_symbols(definition,[sQ608_spl])],[split_symbol_definition]) ).
fof(f11353,plain,
( sQ608_spl
| ~ relation(relation_inverse(sK97_skl)) ),
inference(component_clause,[status(thm)],[f11351]) ).
fof(f11495,plain,
( sQ608_spl
| ~ relation(sK97_skl) ),
inference(resolution,[status(thm)],[f11353,f770]) ).
fof(f11497,plain,
( sQ608_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11495,f996]) ).
fof(f11498,plain,
sQ608_spl,
inference(contradiction_clause,[status(thm)],[f11497]) ).
fof(f11644,definition,
( sQ627_spl
<=> empty(sK94_skl) ),
introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition]) ).
fof(f11645,plain,
( ~ sQ627_spl
| empty(sK94_skl) ),
inference(component_clause,[status(thm)],[f11644]) ).
fof(f11648,definition,
( sQ628_spl
<=> relation(relation_inverse(sK94_skl)) ),
introduced(definition,[new_symbols(definition,[sQ628_spl])],[split_symbol_definition]) ).
fof(f11650,plain,
( sQ628_spl
| ~ relation(relation_inverse(sK94_skl)) ),
inference(component_clause,[status(thm)],[f11648]) ).
fof(f11652,plain,
( ~ sQ627_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11645,f988]) ).
fof(f11653,plain,
~ sQ627_spl,
inference(contradiction_clause,[status(thm)],[f11652]) ).
fof(f11658,plain,
( sQ628_spl
| ~ relation(sK94_skl) ),
inference(resolution,[status(thm)],[f11650,f770]) ).
fof(f11660,plain,
( sQ628_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11658,f989]) ).
fof(f11661,plain,
sQ628_spl,
inference(contradiction_clause,[status(thm)],[f11660]) ).
fof(f12305,plain,
! [X0] :
( ~ sQ501_spl
| in(X0,set_meet(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f9660,f9678]) ).
fof(f12306,plain,
! [X0] :
( ~ sQ501_spl
| in(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f1536,f12305]) ).
fof(f12307,plain,
( ~ sQ501_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12306,f1543]) ).
fof(f12308,plain,
~ sQ501_spl,
inference(contradiction_clause,[status(thm)],[f12307]) ).
fof(f12314,plain,
! [X0] :
( ~ sQ186_spl
| in(sK19_skl(empty_set),X0) ),
inference(forward_demodulation,[status(thm)],[f5776,f3689]) ).
fof(f12325,plain,
! [X0] :
( ~ sQ232_spl
| in(X0,set_meet(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f5690,f4198]) ).
fof(f12326,plain,
! [X0] :
( ~ sQ232_spl
| in(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f1536,f12325]) ).
fof(f12327,plain,
( ~ sQ232_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12326,f1543]) ).
fof(f12328,plain,
~ sQ232_spl,
inference(contradiction_clause,[status(thm)],[f12327]) ).
fof(f12329,plain,
! [X0] :
( ~ sQ228_spl
| in(X0,set_meet(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f5613,f4184]) ).
fof(f12330,plain,
! [X0] :
( ~ sQ228_spl
| in(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f1536,f12329]) ).
fof(f12331,plain,
( ~ sQ228_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12330,f1543]) ).
fof(f12332,plain,
~ sQ228_spl,
inference(contradiction_clause,[status(thm)],[f12331]) ).
fof(f12336,plain,
! [X0] :
( ~ sQ240_spl
| in(sK21_skl(X0,empty_set,empty_set),empty_set)
| in(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f1536,f4227]) ).
fof(f12337,plain,
! [X0] :
( ~ sQ240_spl
| in(sK21_skl(X0,empty_set,empty_set),empty_set) ),
inference(forward_subsumption_resolution,[status(thm)],[f12336,f1543]) ).
fof(f12338,plain,
! [X0] :
( ~ sQ235_spl
| in(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f1536,f4209]) ).
fof(f12339,plain,
( ~ sQ235_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12338,f1543]) ).
fof(f12340,plain,
~ sQ235_spl,
inference(contradiction_clause,[status(thm)],[f12339]) ).
fof(f12341,plain,
! [X0] :
( ~ sQ230_spl
| in(X0,set_meet(relation_image(sK107_skl,empty_set))) ),
inference(forward_demodulation,[status(thm)],[f5690,f4191]) ).
fof(f12342,plain,
! [X0] :
( ~ sQ230_spl
| in(X0,set_meet(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f5690,f12341]) ).
fof(f12343,plain,
! [X0] :
( ~ sQ230_spl
| in(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f1536,f12342]) ).
fof(f12344,plain,
( ~ sQ230_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12343,f1543]) ).
fof(f12345,plain,
~ sQ230_spl,
inference(contradiction_clause,[status(thm)],[f12344]) ).
fof(f12355,plain,
( sQ132_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2836,f1203]) ).
fof(f12356,plain,
sQ132_spl,
inference(contradiction_clause,[status(thm)],[f12355]) ).
fof(f12477,plain,
! [X0] :
( ~ sQ186_spl
| ~ in(sK19_skl(empty_set),X0) ),
inference(resolution,[status(thm)],[f12314,f1566]) ).
fof(f12502,plain,
( ~ sQ186_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12477,f12314]) ).
fof(f12503,plain,
~ sQ186_spl,
inference(contradiction_clause,[status(thm)],[f12502]) ).
fof(f13237,plain,
( sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3680,f960]) ).
fof(f13238,plain,
sQ183_spl,
inference(contradiction_clause,[status(thm)],[f13237]) ).
fof(f13348,definition,
( sQ721_spl
<=> in(sK67_skl(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ721_spl])],[split_symbol_definition]) ).
fof(f13349,plain,
( ~ sQ721_spl
| in(sK67_skl(empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f13348]) ).
fof(f13356,definition,
( sQ722_spl
<=> in(sK68_skl(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition]) ).
fof(f13357,plain,
( ~ sQ722_spl
| in(sK68_skl(empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f13356]) ).
fof(f13374,definition,
( sQ724_spl
<=> subset(empty_set,sK33_skl(sK87_skl)) ),
introduced(definition,[new_symbols(definition,[sQ724_spl])],[split_symbol_definition]) ).
fof(f13376,plain,
( sQ724_spl
| ~ subset(empty_set,sK33_skl(sK87_skl)) ),
inference(component_clause,[status(thm)],[f13374]) ).
fof(f13378,plain,
( sQ724_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13376,f1203]) ).
fof(f13379,plain,
sQ724_spl,
inference(contradiction_clause,[status(thm)],[f13378]) ).
fof(f14060,definition,
( sQ750_spl
<=> relation(relation_restriction(sK94_skl,empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ750_spl])],[split_symbol_definition]) ).
fof(f14062,plain,
( sQ750_spl
| ~ relation(relation_restriction(sK94_skl,empty_set)) ),
inference(component_clause,[status(thm)],[f14060]) ).
fof(f14329,plain,
( sQ750_spl
| ~ relation(sK94_skl) ),
inference(resolution,[status(thm)],[f14062,f766]) ).
fof(f14331,plain,
( sQ750_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14329,f989]) ).
fof(f14332,plain,
sQ750_spl,
inference(contradiction_clause,[status(thm)],[f14331]) ).
fof(f14343,definition,
( sQ780_spl
<=> subset(empty_set,sK33_skl(sK94_skl)) ),
introduced(definition,[new_symbols(definition,[sQ780_spl])],[split_symbol_definition]) ).
fof(f14345,plain,
( sQ780_spl
| ~ subset(empty_set,sK33_skl(sK94_skl)) ),
inference(component_clause,[status(thm)],[f14343]) ).
fof(f14347,plain,
( sQ780_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14345,f1203]) ).
fof(f14348,plain,
sQ780_spl,
inference(contradiction_clause,[status(thm)],[f14347]) ).
fof(f15494,definition,
( sQ856_spl
<=> relation(relation_restriction(sK97_skl,empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ856_spl])],[split_symbol_definition]) ).
fof(f15496,plain,
( sQ856_spl
| ~ relation(relation_restriction(sK97_skl,empty_set)) ),
inference(component_clause,[status(thm)],[f15494]) ).
fof(f15976,plain,
( sQ856_spl
| ~ relation(sK97_skl) ),
inference(resolution,[status(thm)],[f15496,f766]) ).
fof(f15978,plain,
( sQ856_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15976,f996]) ).
fof(f15979,plain,
sQ856_spl,
inference(contradiction_clause,[status(thm)],[f15978]) ).
fof(f17780,definition,
! [X0] :
( sQ977_spl
<=> ( ~ relation(X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ977_spl])],[split_symbol_definition]) ).
fof(f17781,plain,
! [X0] :
( ~ sQ977_spl
| ~ relation(X0)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f17780]) ).
fof(f17830,definition,
( sQ982_spl
<=> in(sK78_skl(sK97_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ982_spl])],[split_symbol_definition]) ).
fof(f17831,plain,
( ~ sQ982_spl
| in(sK78_skl(sK97_skl),empty_set) ),
inference(component_clause,[status(thm)],[f17830]) ).
fof(f17834,definition,
( sQ983_spl
<=> in(sK78_skl(sK94_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ983_spl])],[split_symbol_definition]) ).
fof(f17835,plain,
( ~ sQ983_spl
| in(sK78_skl(sK94_skl),empty_set) ),
inference(component_clause,[status(thm)],[f17834]) ).
fof(f17838,definition,
( sQ984_spl
<=> in(sK78_skl(sK87_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ984_spl])],[split_symbol_definition]) ).
fof(f17839,plain,
( ~ sQ984_spl
| in(sK78_skl(sK87_skl),empty_set) ),
inference(component_clause,[status(thm)],[f17838]) ).
fof(f17843,definition,
( sQ985_spl
<=> in(sK78_skl(sK99_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ985_spl])],[split_symbol_definition]) ).
fof(f17844,plain,
( ~ sQ985_spl
| in(sK78_skl(sK99_skl),empty_set) ),
inference(component_clause,[status(thm)],[f17843]) ).
fof(f17847,definition,
( sQ986_spl
<=> in(sK78_skl(sK100_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ986_spl])],[split_symbol_definition]) ).
fof(f17848,plain,
( ~ sQ986_spl
| in(sK78_skl(sK100_skl),empty_set) ),
inference(component_clause,[status(thm)],[f17847]) ).
fof(f17851,definition,
( sQ987_spl
<=> in(sK78_skl(relation_restriction(sK97_skl,empty_set)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ987_spl])],[split_symbol_definition]) ).
fof(f17852,plain,
( ~ sQ987_spl
| in(sK78_skl(relation_restriction(sK97_skl,empty_set)),empty_set) ),
inference(component_clause,[status(thm)],[f17851]) ).
fof(f17859,definition,
( sQ988_spl
<=> in(sK78_skl(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ988_spl])],[split_symbol_definition]) ).
fof(f17860,plain,
( ~ sQ988_spl
| in(sK78_skl(empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f17859]) ).
fof(f17863,plain,
( ~ sQ983_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17835,f1543]) ).
fof(f17864,plain,
~ sQ983_spl,
inference(contradiction_clause,[status(thm)],[f17863]) ).
fof(f17865,plain,
( ~ sQ986_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17848,f1543]) ).
fof(f17866,plain,
~ sQ986_spl,
inference(contradiction_clause,[status(thm)],[f17865]) ).
fof(f17867,plain,
( ~ sQ985_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17844,f1543]) ).
fof(f17868,plain,
~ sQ985_spl,
inference(contradiction_clause,[status(thm)],[f17867]) ).
fof(f17869,plain,
( ~ sQ984_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17839,f1543]) ).
fof(f17870,plain,
~ sQ984_spl,
inference(contradiction_clause,[status(thm)],[f17869]) ).
fof(f18814,plain,
( ~ sQ988_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17860,f1543]) ).
fof(f18815,plain,
~ sQ988_spl,
inference(contradiction_clause,[status(thm)],[f18814]) ).
fof(f18816,plain,
( ~ sQ987_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17852,f1543]) ).
fof(f18817,plain,
~ sQ987_spl,
inference(contradiction_clause,[status(thm)],[f18816]) ).
fof(f18818,plain,
( ~ sQ982_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17831,f1543]) ).
fof(f18819,plain,
~ sQ982_spl,
inference(contradiction_clause,[status(thm)],[f18818]) ).
fof(f18820,plain,
! [X0] :
( ~ sQ977_spl
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f17781]) ).
fof(f18830,plain,
( ~ sQ722_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13357,f1543]) ).
fof(f18831,plain,
~ sQ722_spl,
inference(contradiction_clause,[status(thm)],[f18830]) ).
fof(f18832,plain,
( ~ sQ721_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13349,f1543]) ).
fof(f18833,plain,
~ sQ721_spl,
inference(contradiction_clause,[status(thm)],[f18832]) ).
fof(f18837,plain,
( ~ sQ240_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12337,f1543]) ).
fof(f18838,plain,
~ sQ240_spl,
inference(contradiction_clause,[status(thm)],[f18837]) ).
fof(f18943,plain,
( ~ sQ977_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1224,f18820]) ).
fof(f18966,plain,
~ sQ977_spl,
inference(contradiction_clause,[status(thm)],[f18943]) ).
fof(f19340,definition,
( sQ1069_spl
<=> in(sK84_skl(sK97_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1069_spl])],[split_symbol_definition]) ).
fof(f19341,plain,
( ~ sQ1069_spl
| in(sK84_skl(sK97_skl),empty_set) ),
inference(component_clause,[status(thm)],[f19340]) ).
fof(f19344,definition,
( sQ1070_spl
<=> in(sK84_skl(sK94_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1070_spl])],[split_symbol_definition]) ).
fof(f19345,plain,
( ~ sQ1070_spl
| in(sK84_skl(sK94_skl),empty_set) ),
inference(component_clause,[status(thm)],[f19344]) ).
fof(f19348,definition,
( sQ1071_spl
<=> in(sK84_skl(sK87_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1071_spl])],[split_symbol_definition]) ).
fof(f19349,plain,
( ~ sQ1071_spl
| in(sK84_skl(sK87_skl),empty_set) ),
inference(component_clause,[status(thm)],[f19348]) ).
fof(f19353,definition,
( sQ1072_spl
<=> in(sK84_skl(sK99_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1072_spl])],[split_symbol_definition]) ).
fof(f19354,plain,
( ~ sQ1072_spl
| in(sK84_skl(sK99_skl),empty_set) ),
inference(component_clause,[status(thm)],[f19353]) ).
fof(f19357,definition,
( sQ1073_spl
<=> in(sK84_skl(sK100_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1073_spl])],[split_symbol_definition]) ).
fof(f19358,plain,
( ~ sQ1073_spl
| in(sK84_skl(sK100_skl),empty_set) ),
inference(component_clause,[status(thm)],[f19357]) ).
fof(f19361,definition,
( sQ1074_spl
<=> in(sK84_skl(relation_restriction(sK97_skl,empty_set)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1074_spl])],[split_symbol_definition]) ).
fof(f19362,plain,
( ~ sQ1074_spl
| in(sK84_skl(relation_restriction(sK97_skl,empty_set)),empty_set) ),
inference(component_clause,[status(thm)],[f19361]) ).
fof(f19369,definition,
( sQ1075_spl
<=> in(sK84_skl(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1075_spl])],[split_symbol_definition]) ).
fof(f19370,plain,
( ~ sQ1075_spl
| in(sK84_skl(empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f19369]) ).
fof(f19373,plain,
( ~ sQ1075_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19370,f1543]) ).
fof(f19374,plain,
~ sQ1075_spl,
inference(contradiction_clause,[status(thm)],[f19373]) ).
fof(f19375,plain,
( ~ sQ1074_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19362,f1543]) ).
fof(f19376,plain,
~ sQ1074_spl,
inference(contradiction_clause,[status(thm)],[f19375]) ).
fof(f19377,plain,
( ~ sQ1073_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19358,f1543]) ).
fof(f19378,plain,
~ sQ1073_spl,
inference(contradiction_clause,[status(thm)],[f19377]) ).
fof(f19379,plain,
( ~ sQ1072_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19354,f1543]) ).
fof(f19380,plain,
~ sQ1072_spl,
inference(contradiction_clause,[status(thm)],[f19379]) ).
fof(f19381,plain,
( ~ sQ1071_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19349,f1543]) ).
fof(f19382,plain,
~ sQ1071_spl,
inference(contradiction_clause,[status(thm)],[f19381]) ).
fof(f19383,plain,
( ~ sQ1070_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19345,f1543]) ).
fof(f19384,plain,
~ sQ1070_spl,
inference(contradiction_clause,[status(thm)],[f19383]) ).
fof(f19385,plain,
( ~ sQ1069_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19341,f1543]) ).
fof(f19386,plain,
~ sQ1069_spl,
inference(contradiction_clause,[status(thm)],[f19385]) ).
fof(f19404,definition,
( sQ1076_spl
<=> in(sK85_skl(sK97_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1076_spl])],[split_symbol_definition]) ).
fof(f19405,plain,
( ~ sQ1076_spl
| in(sK85_skl(sK97_skl),empty_set) ),
inference(component_clause,[status(thm)],[f19404]) ).
fof(f19408,definition,
( sQ1077_spl
<=> in(sK85_skl(sK94_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1077_spl])],[split_symbol_definition]) ).
fof(f19409,plain,
( ~ sQ1077_spl
| in(sK85_skl(sK94_skl),empty_set) ),
inference(component_clause,[status(thm)],[f19408]) ).
fof(f19412,definition,
( sQ1078_spl
<=> in(sK85_skl(sK87_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1078_spl])],[split_symbol_definition]) ).
fof(f19413,plain,
( ~ sQ1078_spl
| in(sK85_skl(sK87_skl),empty_set) ),
inference(component_clause,[status(thm)],[f19412]) ).
fof(f19417,definition,
( sQ1079_spl
<=> in(sK85_skl(sK99_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1079_spl])],[split_symbol_definition]) ).
fof(f19418,plain,
( ~ sQ1079_spl
| in(sK85_skl(sK99_skl),empty_set) ),
inference(component_clause,[status(thm)],[f19417]) ).
fof(f19421,definition,
( sQ1080_spl
<=> in(sK85_skl(sK100_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1080_spl])],[split_symbol_definition]) ).
fof(f19422,plain,
( ~ sQ1080_spl
| in(sK85_skl(sK100_skl),empty_set) ),
inference(component_clause,[status(thm)],[f19421]) ).
fof(f19425,definition,
( sQ1081_spl
<=> in(sK85_skl(relation_restriction(sK97_skl,empty_set)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1081_spl])],[split_symbol_definition]) ).
fof(f19426,plain,
( ~ sQ1081_spl
| in(sK85_skl(relation_restriction(sK97_skl,empty_set)),empty_set) ),
inference(component_clause,[status(thm)],[f19425]) ).
fof(f19433,definition,
( sQ1082_spl
<=> in(sK85_skl(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1082_spl])],[split_symbol_definition]) ).
fof(f19434,plain,
( ~ sQ1082_spl
| in(sK85_skl(empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f19433]) ).
fof(f19437,plain,
( ~ sQ1082_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19434,f1543]) ).
fof(f19438,plain,
~ sQ1082_spl,
inference(contradiction_clause,[status(thm)],[f19437]) ).
fof(f19439,plain,
( ~ sQ1081_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19426,f1543]) ).
fof(f19440,plain,
~ sQ1081_spl,
inference(contradiction_clause,[status(thm)],[f19439]) ).
fof(f19441,plain,
( ~ sQ1080_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19422,f1543]) ).
fof(f19442,plain,
~ sQ1080_spl,
inference(contradiction_clause,[status(thm)],[f19441]) ).
fof(f19443,plain,
( ~ sQ1079_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19418,f1543]) ).
fof(f19444,plain,
~ sQ1079_spl,
inference(contradiction_clause,[status(thm)],[f19443]) ).
fof(f19445,plain,
( ~ sQ1078_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19413,f1543]) ).
fof(f19446,plain,
~ sQ1078_spl,
inference(contradiction_clause,[status(thm)],[f19445]) ).
fof(f19447,plain,
( ~ sQ1077_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19409,f1543]) ).
fof(f19448,plain,
~ sQ1077_spl,
inference(contradiction_clause,[status(thm)],[f19447]) ).
fof(f19449,plain,
( ~ sQ1076_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19405,f1543]) ).
fof(f19450,plain,
~ sQ1076_spl,
inference(contradiction_clause,[status(thm)],[f19449]) ).
fof(f19639,definition,
! [X0] :
( sQ1096_spl
<=> empty_set = singleton(X0) ),
introduced(definition,[new_symbols(definition,[sQ1096_spl])],[split_symbol_definition]) ).
fof(f19640,plain,
! [X0] :
( ~ sQ1096_spl
| empty_set = singleton(X0) ),
inference(component_clause,[status(thm)],[f19639]) ).
fof(f19644,plain,
( ~ sQ1096_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19640,f890]) ).
fof(f19645,plain,
~ sQ1096_spl,
inference(contradiction_clause,[status(thm)],[f19644]) ).
fof(f20376,definition,
( sQ1145_spl
<=> proper_subset(sK33_skl(sK99_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1145_spl])],[split_symbol_definition]) ).
fof(f20377,plain,
( ~ sQ1145_spl
| proper_subset(sK33_skl(sK99_skl),empty_set) ),
inference(component_clause,[status(thm)],[f20376]) ).
fof(f20383,definition,
( sQ1147_spl
<=> subset(empty_set,sK33_skl(sK99_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1147_spl])],[split_symbol_definition]) ).
fof(f20385,plain,
( sQ1147_spl
| ~ subset(empty_set,sK33_skl(sK99_skl)) ),
inference(component_clause,[status(thm)],[f20383]) ).
fof(f20387,plain,
( sQ1147_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20385,f1203]) ).
fof(f20388,plain,
sQ1147_spl,
inference(contradiction_clause,[status(thm)],[f20387]) ).
fof(f20389,plain,
( ~ sQ1145_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20377,f6291]) ).
fof(f20390,plain,
~ sQ1145_spl,
inference(contradiction_clause,[status(thm)],[f20389]) ).
fof(f20397,definition,
( sQ1148_spl
<=> proper_subset(sK33_skl(sK100_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1148_spl])],[split_symbol_definition]) ).
fof(f20398,plain,
( ~ sQ1148_spl
| proper_subset(sK33_skl(sK100_skl),empty_set) ),
inference(component_clause,[status(thm)],[f20397]) ).
fof(f20404,definition,
( sQ1150_spl
<=> subset(empty_set,sK33_skl(sK100_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1150_spl])],[split_symbol_definition]) ).
fof(f20406,plain,
( sQ1150_spl
| ~ subset(empty_set,sK33_skl(sK100_skl)) ),
inference(component_clause,[status(thm)],[f20404]) ).
fof(f20408,plain,
( sQ1150_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20406,f1203]) ).
fof(f20409,plain,
sQ1150_spl,
inference(contradiction_clause,[status(thm)],[f20408]) ).
fof(f20410,plain,
( ~ sQ1148_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20398,f6291]) ).
fof(f20411,plain,
~ sQ1148_spl,
inference(contradiction_clause,[status(thm)],[f20410]) ).
fof(f23076,plain,
( sQ519_spl
| ~ reflexive(sK107_skl)
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f1169,f9988]) ).
fof(f23081,plain,
( sQ519_spl
| ~ sQ434_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f23076,f1606,f8683,f9986]) ).
fof(f23260,plain,
( sQ522_spl
| ~ connected(sK107_skl)
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f9997,f1178]) ).
fof(f23262,plain,
( sQ522_spl
| ~ sQ5_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f23260,f1606,f1621,f9995]) ).
fof(f23400,plain,
( sQ521_spl
| ~ antisymmetric(sK107_skl)
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f1189,f9994]) ).
fof(f23405,plain,
( sQ521_spl
| ~ sQ4_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f23400,f1606,f1616,f9992]) ).
fof(f23537,plain,
( sQ520_spl
| ~ transitive(sK107_skl)
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f9991,f1183]) ).
fof(f23539,plain,
( sQ520_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f23537,f1606,f1609,f9989]) ).
fof(f23680,plain,
( sQ523_spl
| ~ well_founded_relation(sK107_skl)
| ~ relation(sK107_skl) ),
inference(resolution,[status(thm)],[f1214,f10000]) ).
fof(f23682,plain,
( sQ523_spl
| ~ sQ6_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f23680,f1606,f1626,f9998]) ).
fof(f23684,plain,
$false,
inference(sat_refutation,[status(thm)],[f1612,f1614,f1619,f1624,f1629,f1661,f1682,f1693,f1700,f1735,f1794,f1853,f1863,f1978,f2143,f2240,f2242,f2244,f2246,f2248,f2250,f2331,f2343,f3053,f5622,f5699,f5784,f5873,f6900,f7038,f7449,f7691,f8194,f8686,f9000,f9879,f10001,f10893,f11160,f11498,f11653,f11661,f12308,f12328,f12332,f12340,f12345,f12356,f12503,f13238,f13379,f14332,f14348,f15979,f17864,f17866,f17868,f17870,f18815,f18817,f18819,f18831,f18833,f18838,f18966,f19374,f19376,f19378,f19380,f19382,f19384,f19386,f19438,f19440,f19442,f19444,f19446,f19448,f19450,f19645,f20388,f20390,f20409,f20411,f23081,f23262,f23405,f23539,f23682]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU257+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:07:36 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.40 % Drodi V4.1.1
% 15.00/2.37 % Refutation found
% 15.00/2.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.00/2.37 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.20/2.43 % Elapsed time: 2.052642 seconds
% 3.20/2.43 % CPU time: 15.800351 seconds
% 3.20/2.43 % Total memory used: 245.736 MB
% 3.20/2.43 % Net memory used: 232.208 MB
%------------------------------------------------------------------------------