%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU094+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:19:12 PM UTC 2026
% Result : Theorem 0.12s 0.39s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 99
% Syntax : Number of formulae : 387 ( 81 unt; 61 def)
% Number of atoms : 888 ( 10 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 755 ( 254 ~; 272 |; 140 &)
% ( 65 <=>; 23 =>; 0 <=; 1 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 77 ( 75 usr; 62 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 14 con; 0-1 aty)
% Number of variables : 187 ( 168 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A] :
( ordinal(A)
=> ! [B] :
( element(B,A)
=> ( ordinal(B)
& epsilon_connected(B)
& epsilon_transitive(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] :
( empty(A)
=> finite(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( empty(A)
=> function(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( empty(A)
=> relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
( ( ordinal(A)
& empty(A) )
=> ( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( finite(A)
=> ! [B] :
( element(B,powerset(A))
=> finite(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A] :
( ( function(A)
& empty(A)
& relation(A) )
=> ( one_to_one(A)
& function(A)
& relation(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] :
( ( epsilon_connected(A)
& epsilon_transitive(A) )
=> ordinal(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A] :
( empty(A)
=> ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
( element(A,positive_rationals)
=> ( ordinal(A)
=> ( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,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(f20,axiom,
~ empty(positive_rationals),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( ( ! [B] :
( in(B,A)
=> finite(B) )
& finite(A) )
=> finite(union(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
? [A] :
( being_limit_ordinal(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A)
& element(A,positive_rationals) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A] :
? [B] :
( finite(B)
& natural(B)
& ordinal(B)
& epsilon_connected(B)
& epsilon_transitive(B)
& one_to_one(B)
& function(B)
& relation(B)
& empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,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(f37,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& element(A,positive_rationals) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [A] : subset(A,powerset(union(A))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A,B] :
( ( finite(B)
& subset(A,B) )
=> finite(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [A] :
( finite(A)
<=> finite(powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,conjecture,
! [A] :
( ( ! [B] :
( in(B,A)
=> finite(B) )
& finite(A) )
<=> finite(union(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,negated_conjecture,
~ ! [A] :
( ( ! [B] :
( in(B,A)
=> finite(B) )
& finite(A) )
<=> finite(union(A)) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f54,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,plain,
! [A] :
( ! [B] :
( ( ordinal(B)
& epsilon_connected(B)
& epsilon_transitive(B) )
| ~ element(B,A) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f66,plain,
! [X0,X1] :
( epsilon_connected(X1)
| ~ element(X1,X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f68,plain,
! [A] :
( finite(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f69,plain,
! [X0] :
( finite(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
! [A] :
( function(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f71,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f75,plain,
! [A] :
( relation(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f76,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f77,plain,
! [A] :
( ( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) )
| ~ ordinal(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f81,plain,
! [X0] :
( natural(X0)
| ~ ordinal(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f82,plain,
! [A] :
( ! [B] :
( finite(B)
| ~ element(B,powerset(A)) )
| ~ finite(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f83,plain,
! [X0,X1] :
( finite(X1)
| ~ element(X1,powerset(X0))
| ~ finite(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f84,plain,
! [A] :
( ( one_to_one(A)
& function(A)
& relation(A) )
| ~ function(A)
| ~ empty(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f87,plain,
! [X0] :
( one_to_one(X0)
| ~ function(X0)
| ~ empty(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f88,plain,
! [A] :
( ordinal(A)
| ~ epsilon_connected(A)
| ~ epsilon_transitive(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f89,plain,
! [X0] :
( ordinal(X0)
| ~ epsilon_connected(X0)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
! [A] :
( ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f91,plain,
! [X0] :
( epsilon_transitive(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
! [X0] :
( epsilon_connected(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f94,plain,
! [A] :
( ( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) )
| ~ ordinal(A)
| ~ element(A,positive_rationals) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f98,plain,
! [X0] :
( natural(X0)
| ~ ordinal(X0)
| ~ element(X0,positive_rationals) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f99,plain,
! [A] : element(sK0_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f13]) ).
fof(f100,plain,
! [X0] : element(sK0_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f101,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f108,plain,
function(empty_set),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f111,plain,
epsilon_transitive(empty_set),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f112,plain,
epsilon_connected(empty_set),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f113,plain,
ordinal(empty_set),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f120,plain,
~ empty(positive_rationals),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f121,plain,
! [A] :
( finite(union(A))
| ? [B] :
( ~ finite(B)
& in(B,A) )
| ~ finite(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f122,plain,
! [A] :
( finite(union(A))
| ( ~ finite(sK1_skl(A))
& in(sK1_skl(A),A) )
| ~ finite(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f121]) ).
fof(f123,plain,
! [X0] :
( finite(union(X0))
| in(sK1_skl(X0),X0)
| ~ finite(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f124,plain,
! [X0] :
( finite(union(X0))
| ~ finite(sK1_skl(X0))
| ~ finite(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f125,plain,
( natural(sK2_skl)
& ordinal(sK2_skl)
& epsilon_connected(sK2_skl)
& epsilon_transitive(sK2_skl)
& ~ empty(sK2_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f22]) ).
fof(f127,plain,
epsilon_transitive(sK2_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f128,plain,
epsilon_connected(sK2_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f141,plain,
( ordinal(sK6_skl)
& epsilon_connected(sK6_skl)
& epsilon_transitive(sK6_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f26]) ).
fof(f142,plain,
epsilon_transitive(sK6_skl),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f143,plain,
epsilon_connected(sK6_skl),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f145,plain,
( being_limit_ordinal(sK7_skl)
& ordinal(sK7_skl)
& epsilon_connected(sK7_skl)
& epsilon_transitive(sK7_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f27]) ).
fof(f146,plain,
epsilon_transitive(sK7_skl),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f147,plain,
epsilon_connected(sK7_skl),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f150,plain,
( relation(sK8_skl)
& empty(sK8_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f28]) ).
fof(f151,plain,
empty(sK8_skl),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f153,plain,
! [A] :
( ? [B] :
( ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f154,plain,
! [A] :
( ( ~ empty(sK9_skl(A))
& element(sK9_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(B,sK9_skl(A))],[f153]) ).
fof(f155,plain,
! [X0] :
( element(sK9_skl(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
! [X0] :
( ~ empty(sK9_skl(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f157,plain,
empty(sK10_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f30]) ).
fof(f158,plain,
empty(sK10_skl),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f159,plain,
( ordinal(sK11_skl)
& epsilon_connected(sK11_skl)
& epsilon_transitive(sK11_skl)
& ~ empty(sK11_skl)
& element(sK11_skl,positive_rationals) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f31]) ).
fof(f160,plain,
element(sK11_skl,positive_rationals),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f162,plain,
epsilon_transitive(sK11_skl),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f163,plain,
epsilon_connected(sK11_skl),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f165,plain,
! [A] :
( finite(sK12_skl(A))
& natural(sK12_skl(A))
& ordinal(sK12_skl(A))
& epsilon_connected(sK12_skl(A))
& epsilon_transitive(sK12_skl(A))
& one_to_one(sK12_skl(A))
& function(sK12_skl(A))
& relation(sK12_skl(A))
& empty(sK12_skl(A))
& element(sK12_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(B,sK12_skl(A))],[f32]) ).
fof(f166,plain,
! [X0] : element(sK12_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f167,plain,
! [X0] : empty(sK12_skl(X0)),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f176,plain,
( function(sK13_skl)
& empty(sK13_skl)
& relation(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f33]) ).
fof(f178,plain,
empty(sK13_skl),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f179,plain,
function(sK13_skl),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f180,plain,
( ordinal(sK14_skl)
& epsilon_connected(sK14_skl)
& epsilon_transitive(sK14_skl)
& empty(sK14_skl)
& one_to_one(sK14_skl)
& function(sK14_skl)
& relation(sK14_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f34]) ).
fof(f182,plain,
function(sK14_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f184,plain,
empty(sK14_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f185,plain,
epsilon_transitive(sK14_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f186,plain,
epsilon_connected(sK14_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f187,plain,
ordinal(sK14_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f196,plain,
! [A] :
( empty(sK17_skl(A))
& element(sK17_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(B,sK17_skl(A))],[f37]) ).
fof(f197,plain,
! [X0] : element(sK17_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f198,plain,
! [X0] : empty(sK17_skl(X0)),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f201,plain,
( natural(sK19_skl)
& ordinal(sK19_skl)
& epsilon_connected(sK19_skl)
& epsilon_transitive(sK19_skl)
& empty(sK19_skl)
& element(sK19_skl,positive_rationals) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(A,sK19_skl)],[f39]) ).
fof(f202,plain,
element(sK19_skl,positive_rationals),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f203,plain,
empty(sK19_skl),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f204,plain,
epsilon_transitive(sK19_skl),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f205,plain,
epsilon_connected(sK19_skl),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f206,plain,
ordinal(sK19_skl),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f217,plain,
( ordinal(sK22_skl)
& epsilon_connected(sK22_skl)
& epsilon_transitive(sK22_skl)
& ~ empty(sK22_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(A,sK22_skl)],[f42]) ).
fof(f219,plain,
epsilon_transitive(sK22_skl),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f220,plain,
epsilon_connected(sK22_skl),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f239,plain,
! [X0] : subset(X0,powerset(union(X0))),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f240,plain,
! [A,B] :
( finite(A)
| ~ finite(B)
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f241,plain,
! [A] :
( finite(A)
| ! [B] :
( ~ finite(B)
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f240]) ).
fof(f242,plain,
! [X0,X1] :
( finite(X0)
| ~ finite(X1)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f243,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f244,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f245,plain,
! [A] :
( ( ~ finite(powerset(A))
| finite(A) )
& ( finite(powerset(A))
| ~ finite(A) ) ),
inference(NNF_transformation,[status(thm)],[f51]) ).
fof(f246,plain,
( ! [A] :
( ~ finite(powerset(A))
| finite(A) )
& ! [A] :
( finite(powerset(A))
| ~ finite(A) ) ),
inference(miniscoping,[status(thm)],[f245]) ).
fof(f247,plain,
! [X0] :
( finite(powerset(X0))
| ~ finite(X0) ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f249,plain,
? [A] :
( ( ! [B] :
( finite(B)
| ~ in(B,A) )
& finite(A) )
<~> finite(union(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f250,plain,
? [A] :
( ( ~ finite(union(A))
| ? [B] :
( ~ finite(B)
& in(B,A) )
| ~ finite(A) )
& ( finite(union(A))
| ( ! [B] :
( finite(B)
| ~ in(B,A) )
& finite(A) ) ) ),
inference(NNF_transformation,[status(thm)],[f249]) ).
fof(f251,plain,
( ( ~ finite(union(sK27_skl))
| ( ~ finite(sK28_skl)
& in(sK28_skl,sK27_skl) )
| ~ finite(sK27_skl) )
& ( finite(union(sK27_skl))
| ( ! [B] :
( finite(B)
| ~ in(B,sK27_skl) )
& finite(sK27_skl) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl]),skolemize(A,sK27_skl),skolemize(B,sK28_skl)],[f250]) ).
fof(f252,plain,
( finite(union(sK27_skl))
| finite(sK27_skl) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f253,plain,
! [X0] :
( finite(union(sK27_skl))
| finite(X0)
| ~ in(X0,sK27_skl) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f254,plain,
( ~ finite(union(sK27_skl))
| in(sK28_skl,sK27_skl)
| ~ finite(sK27_skl) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f255,plain,
( ~ finite(union(sK27_skl))
| ~ finite(sK28_skl)
| ~ finite(sK27_skl) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f256,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f257,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f258,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(NNF_transformation,[status(thm)],[f55]) ).
fof(f259,plain,
( ! [A,B] :
( ~ subset(A,B)
| element(A,powerset(B)) )
& ! [A,B] :
( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(miniscoping,[status(thm)],[f258]) ).
fof(f261,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f262,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f263,plain,
! [A,C] :
( element(A,C)
| ! [B] :
( ~ element(B,powerset(C))
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f262]) ).
fof(f264,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f265,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f266,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f265]) ).
fof(f267,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f268,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f58]) ).
fof(f269,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f278,definition,
( sQ0_spl
<=> finite(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f281,definition,
( sQ1_spl
<=> finite(union(sK27_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f282,plain,
( ~ sQ1_spl
| finite(union(sK27_skl)) ),
inference(component_clause,[status(thm)],[f281]) ).
fof(f284,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f252,f278,f281]) ).
fof(f285,definition,
! [X0] :
( sQ2_spl
<=> ( finite(X0)
| ~ in(X0,sK27_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f286,plain,
! [X0] :
( ~ sQ2_spl
| finite(X0)
| ~ in(X0,sK27_skl) ),
inference(component_clause,[status(thm)],[f285]) ).
fof(f288,plain,
( sQ1_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f253,f285,f281]) ).
fof(f289,definition,
( sQ3_spl
<=> in(sK28_skl,sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f290,plain,
( ~ sQ3_spl
| in(sK28_skl,sK27_skl) ),
inference(component_clause,[status(thm)],[f289]) ).
fof(f292,plain,
( ~ sQ1_spl
| sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f254,f278,f289,f281]) ).
fof(f293,definition,
( sQ4_spl
<=> finite(sK28_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f295,plain,
( sQ4_spl
| ~ finite(sK28_skl) ),
inference(component_clause,[status(thm)],[f293]) ).
fof(f296,plain,
( ~ sQ1_spl
| ~ sQ4_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f255,f278,f293,f281]) ).
fof(f297,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| finite(sK28_skl) ),
inference(resolution,[status(thm)],[f286,f290]) ).
fof(f298,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f297,f295]) ).
fof(f299,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f298]) ).
fof(f312,plain,
function(sK8_skl),
inference(resolution,[status(thm)],[f151,f71]) ).
fof(f317,plain,
function(sK10_skl),
inference(resolution,[status(thm)],[f158,f71]) ).
fof(f329,plain,
( natural(sK14_skl)
| ~ empty(sK14_skl) ),
inference(resolution,[status(thm)],[f81,f187]) ).
fof(f334,plain,
( natural(empty_set)
| ~ empty(empty_set) ),
inference(resolution,[status(thm)],[f81,f113]) ).
fof(f336,definition,
( sQ5_spl
<=> empty(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f338,plain,
( sQ5_spl
| ~ empty(sK14_skl) ),
inference(component_clause,[status(thm)],[f336]) ).
fof(f339,definition,
( sQ6_spl
<=> natural(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f342,plain,
( sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f329,f336,f339]) ).
fof(f346,definition,
( sQ8_spl
<=> natural(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f371,definition,
( sQ15_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f373,plain,
( sQ15_spl
| ~ empty(empty_set) ),
inference(component_clause,[status(thm)],[f371]) ).
fof(f374,definition,
( sQ16_spl
<=> natural(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f377,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f334,f371,f374]) ).
fof(f378,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f373,f101]) ).
fof(f379,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f378]) ).
fof(f380,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f338,f184]) ).
fof(f381,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f380]) ).
fof(f382,plain,
! [X0] :
( one_to_one(X0)
| ~ function(X0)
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f87,f76]) ).
fof(f384,plain,
( one_to_one(sK14_skl)
| ~ empty(sK14_skl) ),
inference(resolution,[status(thm)],[f382,f182]) ).
fof(f385,plain,
( one_to_one(sK13_skl)
| ~ empty(sK13_skl) ),
inference(resolution,[status(thm)],[f382,f179]) ).
fof(f388,plain,
( one_to_one(empty_set)
| ~ empty(empty_set) ),
inference(resolution,[status(thm)],[f382,f108]) ).
fof(f396,definition,
( sQ19_spl
<=> one_to_one(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( sQ19_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f384,f336,f396]) ).
fof(f400,definition,
( sQ20_spl
<=> empty(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f402,plain,
( sQ20_spl
| ~ empty(sK13_skl) ),
inference(component_clause,[status(thm)],[f400]) ).
fof(f403,definition,
( sQ21_spl
<=> one_to_one(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f406,plain,
( sQ21_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f385,f400,f403]) ).
fof(f421,definition,
( sQ26_spl
<=> one_to_one(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f424,plain,
( sQ26_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f388,f371,f421]) ).
fof(f425,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f402,f178]) ).
fof(f426,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f425]) ).
fof(f428,plain,
function(sK19_skl),
inference(resolution,[status(thm)],[f203,f71]) ).
fof(f430,plain,
( natural(sK19_skl)
| ~ empty(sK19_skl) ),
inference(resolution,[status(thm)],[f206,f81]) ).
fof(f433,definition,
( sQ27_spl
<=> empty(sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f435,plain,
( sQ27_spl
| ~ empty(sK19_skl) ),
inference(component_clause,[status(thm)],[f433]) ).
fof(f436,definition,
( sQ28_spl
<=> natural(sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f430,f433,f436]) ).
fof(f440,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f435,f203]) ).
fof(f441,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f440]) ).
fof(f450,plain,
( ordinal(sK19_skl)
| ~ epsilon_transitive(sK19_skl) ),
inference(resolution,[status(thm)],[f89,f205]) ).
fof(f451,plain,
( ordinal(sK14_skl)
| ~ epsilon_transitive(sK14_skl) ),
inference(resolution,[status(thm)],[f89,f186]) ).
fof(f452,plain,
( ordinal(sK11_skl)
| ~ epsilon_transitive(sK11_skl) ),
inference(resolution,[status(thm)],[f89,f163]) ).
fof(f453,plain,
( ordinal(sK7_skl)
| ~ epsilon_transitive(sK7_skl) ),
inference(resolution,[status(thm)],[f89,f147]) ).
fof(f454,plain,
( ordinal(sK6_skl)
| ~ epsilon_transitive(sK6_skl) ),
inference(resolution,[status(thm)],[f89,f143]) ).
fof(f455,plain,
( ordinal(sK2_skl)
| ~ epsilon_transitive(sK2_skl) ),
inference(resolution,[status(thm)],[f89,f128]) ).
fof(f456,plain,
( ordinal(empty_set)
| ~ epsilon_transitive(empty_set) ),
inference(resolution,[status(thm)],[f89,f112]) ).
fof(f458,definition,
( sQ31_spl
<=> epsilon_transitive(sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( sQ31_spl
| ~ epsilon_transitive(sK19_skl) ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,definition,
( sQ32_spl
<=> ordinal(sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f464,plain,
( sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f450,f458,f461]) ).
fof(f465,definition,
( sQ33_spl
<=> epsilon_transitive(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( sQ33_spl
| ~ epsilon_transitive(sK14_skl) ),
inference(component_clause,[status(thm)],[f465]) ).
fof(f468,definition,
( sQ34_spl
<=> ordinal(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f451,f465,f468]) ).
fof(f472,definition,
( sQ35_spl
<=> epsilon_transitive(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( sQ35_spl
| ~ epsilon_transitive(sK11_skl) ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f475,definition,
( sQ36_spl
<=> ordinal(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f478,plain,
( sQ36_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f452,f472,f475]) ).
fof(f479,definition,
( sQ37_spl
<=> epsilon_transitive(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f481,plain,
( sQ37_spl
| ~ epsilon_transitive(sK7_skl) ),
inference(component_clause,[status(thm)],[f479]) ).
fof(f482,definition,
( sQ38_spl
<=> ordinal(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f485,plain,
( sQ38_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f453,f479,f482]) ).
fof(f486,definition,
( sQ39_spl
<=> epsilon_transitive(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( sQ39_spl
| ~ epsilon_transitive(sK6_skl) ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f489,definition,
( sQ40_spl
<=> ordinal(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f492,plain,
( sQ40_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f454,f486,f489]) ).
fof(f493,definition,
( sQ41_spl
<=> epsilon_transitive(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f495,plain,
( sQ41_spl
| ~ epsilon_transitive(sK2_skl) ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f496,definition,
( sQ42_spl
<=> ordinal(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f499,plain,
( sQ42_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f455,f493,f496]) ).
fof(f500,definition,
( sQ43_spl
<=> epsilon_transitive(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f502,plain,
( sQ43_spl
| ~ epsilon_transitive(empty_set) ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f503,definition,
( sQ44_spl
<=> ordinal(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f506,plain,
( sQ44_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f456,f500,f503]) ).
fof(f507,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f502,f111]) ).
fof(f508,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f507]) ).
fof(f509,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f495,f127]) ).
fof(f510,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f509]) ).
fof(f511,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f488,f142]) ).
fof(f512,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f511]) ).
fof(f513,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f481,f146]) ).
fof(f514,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f513]) ).
fof(f515,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f474,f162]) ).
fof(f516,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f515]) ).
fof(f517,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f467,f185]) ).
fof(f518,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f517]) ).
fof(f519,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f460,f204]) ).
fof(f520,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f519]) ).
fof(f523,plain,
epsilon_transitive(sK13_skl),
inference(resolution,[status(thm)],[f91,f178]) ).
fof(f524,plain,
epsilon_transitive(sK10_skl),
inference(resolution,[status(thm)],[f91,f158]) ).
fof(f525,plain,
epsilon_transitive(sK8_skl),
inference(resolution,[status(thm)],[f91,f151]) ).
fof(f527,plain,
( ordinal(sK22_skl)
| ~ epsilon_transitive(sK22_skl) ),
inference(resolution,[status(thm)],[f220,f89]) ).
fof(f528,definition,
( sQ45_spl
<=> epsilon_transitive(sK22_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f530,plain,
( sQ45_spl
| ~ epsilon_transitive(sK22_skl) ),
inference(component_clause,[status(thm)],[f528]) ).
fof(f531,definition,
( sQ46_spl
<=> ordinal(sK22_skl) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f534,plain,
( sQ46_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f527,f528,f531]) ).
fof(f535,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f530,f219]) ).
fof(f536,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f535]) ).
fof(f571,plain,
( one_to_one(sK8_skl)
| ~ empty(sK8_skl) ),
inference(resolution,[status(thm)],[f312,f382]) ).
fof(f572,definition,
( sQ55_spl
<=> empty(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f574,plain,
( sQ55_spl
| ~ empty(sK8_skl) ),
inference(component_clause,[status(thm)],[f572]) ).
fof(f575,definition,
( sQ56_spl
<=> one_to_one(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f578,plain,
( sQ56_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f571,f572,f575]) ).
fof(f579,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f574,f151]) ).
fof(f580,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f579]) ).
fof(f581,plain,
( one_to_one(sK10_skl)
| ~ empty(sK10_skl) ),
inference(resolution,[status(thm)],[f317,f382]) ).
fof(f582,definition,
( sQ57_spl
<=> empty(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f584,plain,
( sQ57_spl
| ~ empty(sK10_skl) ),
inference(component_clause,[status(thm)],[f582]) ).
fof(f585,definition,
( sQ58_spl
<=> one_to_one(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f588,plain,
( sQ58_spl
| ~ sQ57_spl ),
inference(split_clause,[status(thm)],[f581,f582,f585]) ).
fof(f589,plain,
( sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f584,f158]) ).
fof(f590,plain,
sQ57_spl,
inference(contradiction_clause,[status(thm)],[f589]) ).
fof(f593,plain,
epsilon_connected(sK13_skl),
inference(resolution,[status(thm)],[f92,f178]) ).
fof(f594,plain,
epsilon_connected(sK10_skl),
inference(resolution,[status(thm)],[f92,f158]) ).
fof(f595,plain,
epsilon_connected(sK8_skl),
inference(resolution,[status(thm)],[f92,f151]) ).
fof(f604,plain,
( one_to_one(sK19_skl)
| ~ empty(sK19_skl) ),
inference(resolution,[status(thm)],[f428,f382]) ).
fof(f605,definition,
( sQ59_spl
<=> one_to_one(sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f608,plain,
( sQ59_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f604,f433,f605]) ).
fof(f616,plain,
! [X0] :
( in(sK0_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f100,f257]) ).
fof(f624,plain,
( ordinal(sK13_skl)
| ~ epsilon_transitive(sK13_skl) ),
inference(resolution,[status(thm)],[f593,f89]) ).
fof(f625,definition,
( sQ62_spl
<=> epsilon_transitive(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f627,plain,
( sQ62_spl
| ~ epsilon_transitive(sK13_skl) ),
inference(component_clause,[status(thm)],[f625]) ).
fof(f628,definition,
( sQ63_spl
<=> ordinal(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f631,plain,
( sQ63_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f624,f625,f628]) ).
fof(f632,plain,
( sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f627,f523]) ).
fof(f633,plain,
sQ62_spl,
inference(contradiction_clause,[status(thm)],[f632]) ).
fof(f634,plain,
( ordinal(sK10_skl)
| ~ epsilon_transitive(sK10_skl) ),
inference(resolution,[status(thm)],[f594,f89]) ).
fof(f635,definition,
( sQ64_spl
<=> epsilon_transitive(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f637,plain,
( sQ64_spl
| ~ epsilon_transitive(sK10_skl) ),
inference(component_clause,[status(thm)],[f635]) ).
fof(f638,definition,
( sQ65_spl
<=> ordinal(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f641,plain,
( sQ65_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f634,f635,f638]) ).
fof(f642,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f637,f524]) ).
fof(f643,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f642]) ).
fof(f644,plain,
( ordinal(sK8_skl)
| ~ epsilon_transitive(sK8_skl) ),
inference(resolution,[status(thm)],[f595,f89]) ).
fof(f645,definition,
( sQ66_spl
<=> epsilon_transitive(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f647,plain,
( sQ66_spl
| ~ epsilon_transitive(sK8_skl) ),
inference(component_clause,[status(thm)],[f645]) ).
fof(f648,definition,
( sQ67_spl
<=> ordinal(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f651,plain,
( sQ67_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f644,f645,f648]) ).
fof(f652,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f647,f525]) ).
fof(f653,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f652]) ).
fof(f665,plain,
! [X0] : finite(sK12_skl(X0)),
inference(resolution,[status(thm)],[f167,f69]) ).
fof(f668,plain,
( ~ sQ2_spl
| finite(sK1_skl(sK27_skl))
| finite(union(sK27_skl))
| ~ finite(sK27_skl) ),
inference(resolution,[status(thm)],[f123,f286]) ).
fof(f672,definition,
( sQ68_spl
<=> finite(sK1_skl(sK27_skl)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f673,plain,
( ~ sQ68_spl
| finite(sK1_skl(sK27_skl)) ),
inference(component_clause,[status(thm)],[f672]) ).
fof(f675,plain,
( ~ sQ2_spl
| sQ68_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f668,f278,f281,f672,f285]) ).
fof(f678,plain,
! [X0,X1] :
( element(X1,X0)
| ~ in(X1,sK9_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f155,f264]) ).
fof(f703,plain,
( ~ sQ68_spl
| finite(union(sK27_skl))
| ~ finite(sK27_skl) ),
inference(resolution,[status(thm)],[f673,f124]) ).
fof(f704,plain,
( ~ sQ68_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f703,f278,f281,f672]) ).
fof(f752,definition,
( sQ76_spl
<=> finite(union(positive_rationals)) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f776,plain,
( natural(sK11_skl)
| ~ ordinal(sK11_skl) ),
inference(resolution,[status(thm)],[f160,f98]) ).
fof(f778,plain,
( epsilon_connected(sK11_skl)
| ~ ordinal(positive_rationals) ),
inference(resolution,[status(thm)],[f160,f66]) ).
fof(f780,plain,
( in(sK11_skl,positive_rationals)
| empty(positive_rationals) ),
inference(resolution,[status(thm)],[f160,f257]) ).
fof(f781,plain,
( sQ8_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f776,f475,f346]) ).
fof(f782,definition,
( sQ79_spl
<=> ordinal(positive_rationals) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f786,definition,
( sQ80_spl
<=> epsilon_connected(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f789,plain,
( sQ80_spl
| ~ sQ79_spl ),
inference(split_clause,[status(thm)],[f778,f782,f786]) ).
fof(f791,definition,
( sQ81_spl
<=> empty(positive_rationals) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f792,plain,
( ~ sQ81_spl
| empty(positive_rationals) ),
inference(component_clause,[status(thm)],[f791]) ).
fof(f794,definition,
( sQ82_spl
<=> in(sK11_skl,positive_rationals) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f795,plain,
( ~ sQ82_spl
| in(sK11_skl,positive_rationals) ),
inference(component_clause,[status(thm)],[f794]) ).
fof(f797,plain,
( sQ82_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f780,f791,f794]) ).
fof(f798,plain,
( ~ sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f792,f120]) ).
fof(f799,plain,
~ sQ81_spl,
inference(contradiction_clause,[status(thm)],[f798]) ).
fof(f802,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,sK12_skl(X1)) ),
inference(resolution,[status(thm)],[f166,f267]) ).
fof(f815,plain,
! [X0] :
( finite(union(sK12_skl(X0)))
| ~ finite(sK12_skl(X0))
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f802,f123]) ).
fof(f816,plain,
! [X0] :
( finite(union(sK12_skl(X0)))
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f815,f665]) ).
fof(f825,plain,
! [X0] :
( empty(sK9_skl(X0))
| element(sK0_skl(sK9_skl(X0)),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f678,f616]) ).
fof(f827,plain,
! [X0] :
( element(sK0_skl(sK9_skl(X0)),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f825,f156]) ).
fof(f852,plain,
( epsilon_connected(sK19_skl)
| ~ ordinal(positive_rationals) ),
inference(resolution,[status(thm)],[f202,f66]) ).
fof(f854,plain,
( in(sK19_skl,positive_rationals)
| empty(positive_rationals) ),
inference(resolution,[status(thm)],[f202,f257]) ).
fof(f857,definition,
( sQ86_spl
<=> epsilon_connected(sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f860,plain,
( sQ86_spl
| ~ sQ79_spl ),
inference(split_clause,[status(thm)],[f852,f782,f857]) ).
fof(f862,definition,
( sQ87_spl
<=> in(sK19_skl,positive_rationals) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f863,plain,
( ~ sQ87_spl
| in(sK19_skl,positive_rationals) ),
inference(component_clause,[status(thm)],[f862]) ).
fof(f865,plain,
( sQ87_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f854,f791,f862]) ).
fof(f866,plain,
! [X0] : sK17_skl(X0) = empty_set,
inference(resolution,[status(thm)],[f269,f198]) ).
fof(f868,plain,
! [X0] : sK12_skl(X0) = empty_set,
inference(resolution,[status(thm)],[f269,f167]) ).
fof(f869,plain,
sK19_skl = empty_set,
inference(resolution,[status(thm)],[f269,f203]) ).
fof(f870,plain,
sK14_skl = empty_set,
inference(resolution,[status(thm)],[f269,f184]) ).
fof(f886,plain,
sK19_skl = sK14_skl,
inference(backward_demodulation,[status(thm)],[f870,f869]) ).
fof(f933,plain,
! [X0] : sK17_skl(X0) = sK14_skl,
inference(forward_demodulation,[status(thm)],[f870,f866]) ).
fof(f934,plain,
! [X0] :
( finite(union(sK14_skl))
| ~ empty(X0) ),
inference(backward_demodulation,[status(thm)],[f949,f816]) ).
fof(f936,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,sK14_skl) ),
inference(backward_demodulation,[status(thm)],[f949,f802]) ).
fof(f949,plain,
! [X0] : sK12_skl(X0) = sK14_skl,
inference(forward_demodulation,[status(thm)],[f870,f868]) ).
fof(f950,definition,
! [X0] :
( sQ88_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f951,plain,
! [X0] :
( ~ sQ88_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f950]) ).
fof(f953,definition,
( sQ89_spl
<=> finite(union(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f956,plain,
( sQ89_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f934,f950,f953]) ).
fof(f957,definition,
! [X0] :
( sQ90_spl
<=> ~ in(X0,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f960,plain,
( sQ88_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f936,f957,f950]) ).
fof(f961,plain,
! [X0] : element(sK14_skl,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f933,f197]) ).
fof(f962,plain,
! [X0] :
( finite(sK14_skl)
| ~ finite(X0) ),
inference(resolution,[status(thm)],[f961,f83]) ).
fof(f969,definition,
! [X0] :
( sQ91_spl
<=> ~ finite(X0) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f970,plain,
! [X0] :
( ~ sQ91_spl
| ~ finite(X0) ),
inference(component_clause,[status(thm)],[f969]) ).
fof(f972,definition,
( sQ92_spl
<=> finite(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f975,plain,
( sQ92_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f962,f969,f972]) ).
fof(f981,definition,
( sQ94_spl
<=> epsilon_connected(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1004,plain,
( ~ sQ88_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f184,f951]) ).
fof(f1005,plain,
~ sQ88_spl,
inference(contradiction_clause,[status(thm)],[f1004]) ).
fof(f1008,plain,
( ~ sQ87_spl
| in(sK14_skl,positive_rationals) ),
inference(forward_demodulation,[status(thm)],[f886,f863]) ).
fof(f1009,plain,
( ~ sQ87_spl
| element(sK14_skl,positive_rationals) ),
inference(resolution,[status(thm)],[f1008,f244]) ).
fof(f1017,plain,
( ~ sQ87_spl
| epsilon_connected(sK14_skl)
| ~ ordinal(positive_rationals) ),
inference(resolution,[status(thm)],[f1009,f66]) ).
fof(f1021,plain,
( ~ sQ87_spl
| sQ94_spl
| ~ sQ79_spl ),
inference(split_clause,[status(thm)],[f1017,f782,f981,f862]) ).
fof(f1032,plain,
( ~ sQ87_spl
| in(sK14_skl,positive_rationals)
| empty(positive_rationals) ),
inference(resolution,[status(thm)],[f257,f1009]) ).
fof(f1038,definition,
( sQ95_spl
<=> in(sK14_skl,positive_rationals) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1041,plain,
( ~ sQ87_spl
| sQ95_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f1032,f791,f1038,f862]) ).
fof(f1044,plain,
! [X0] :
( ~ sQ91_spl
| ~ empty(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f69,f970]) ).
fof(f1052,plain,
( ~ sQ91_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f1044,f950,f969]) ).
fof(f1054,plain,
! [X0] :
( finite(X0)
| ~ finite(powerset(union(X0))) ),
inference(resolution,[status(thm)],[f242,f239]) ).
fof(f1086,plain,
! [X0,X1,X2] :
( element(X2,X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(resolution,[status(thm)],[f261,f264]) ).
fof(f1113,plain,
( natural(sK0_skl(sK9_skl(positive_rationals)))
| ~ ordinal(sK0_skl(sK9_skl(positive_rationals)))
| empty(positive_rationals) ),
inference(resolution,[status(thm)],[f827,f98]) ).
fof(f1121,definition,
( sQ96_spl
<=> ordinal(sK0_skl(sK9_skl(positive_rationals))) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1124,definition,
( sQ97_spl
<=> natural(sK0_skl(sK9_skl(positive_rationals))) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1127,plain,
( sQ97_spl
| ~ sQ96_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f1113,f791,f1121,f1124]) ).
fof(f1152,plain,
! [X0] :
( ~ finite(union(X0))
| finite(X0) ),
inference(resolution,[status(thm)],[f1054,f247]) ).
fof(f1154,plain,
( ~ sQ1_spl
| finite(sK27_skl) ),
inference(resolution,[status(thm)],[f1152,f282]) ).
fof(f1209,plain,
! [X0,X1] :
( element(X0,powerset(union(X1)))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f1086,f239]) ).
fof(f1216,plain,
! [X0,X1] :
( finite(X0)
| ~ finite(union(X1))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f1209,f83]) ).
fof(f1233,plain,
( ~ sQ82_spl
| finite(sK11_skl)
| ~ finite(union(positive_rationals)) ),
inference(resolution,[status(thm)],[f1216,f795]) ).
fof(f1234,plain,
( ~ sQ3_spl
| finite(sK28_skl)
| ~ finite(union(sK27_skl)) ),
inference(resolution,[status(thm)],[f1216,f290]) ).
fof(f1241,definition,
( sQ99_spl
<=> finite(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1244,plain,
( ~ sQ82_spl
| sQ99_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f1233,f752,f1241,f794]) ).
fof(f1245,plain,
( ~ sQ3_spl
| sQ4_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f1234,f281,f293,f289]) ).
fof(f1246,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1154,f278,f281]) ).
fof(f1247,plain,
$false,
inference(sat_refutation,[status(thm)],[f284,f288,f292,f296,f299,f342,f377,f379,f381,f399,f406,f424,f426,f439,f441,f464,f471,f478,f485,f492,f499,f506,f508,f510,f512,f514,f516,f518,f520,f534,f536,f578,f580,f588,f590,f608,f631,f633,f641,f643,f651,f653,f675,f704,f781,f789,f797,f799,f860,f865,f956,f960,f975,f1005,f1021,f1041,f1052,f1127,f1244,f1245,f1246]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU094+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 05:52:14 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.39 % Refutation found
% 0.12/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.41 % Elapsed time: 0.055260 seconds
% 0.12/0.41 % CPU time: 0.200622 seconds
% 0.12/0.41 % Total memory used: 86.163 MB
% 0.12/0.41 % Net memory used: 85.949 MB
%------------------------------------------------------------------------------