%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU236+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:19:50 PM UTC 2026
% Result : Theorem 0.69s 0.56s
% Output : CNFRefutation 0.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 88
% Syntax : Number of formulae : 379 ( 67 unt; 59 def)
% Number of atoms : 889 ( 37 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 828 ( 318 ~; 332 |; 90 &)
% ( 69 <=>; 18 =>; 0 <=; 1 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 72 ( 70 usr; 60 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 194 ( 178 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A] :
( empty(A)
=> function(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] :
( ordinal(A)
=> ( epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( empty(A)
=> relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] :
( ( function(A)
& empty(A)
& relation(A) )
=> ( one_to_one(A)
& function(A)
& relation(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( ( epsilon_connected(A)
& epsilon_transitive(A) )
=> ordinal(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
( empty(A)
=> ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] : succ(A) = set_union2(A,singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
( epsilon_transitive(A)
<=> ! [B] :
( in(B,A)
=> subset(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,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/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A,B] :
( ( relation(B)
& relation(A) )
=> relation(set_union2(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A,B] :
( ~ empty(A)
=> ~ empty(set_union2(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A,B] :
( ( ordinal(B)
& ordinal(A) )
=> ( ordinal_subset(A,B)
<=> subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A] : in(A,succ(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [A] : set_union2(A,empty_set) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,conjecture,
! [A] :
( ordinal(A)
=> ! [B] :
( ordinal(B)
=> ( in(A,B)
<=> ordinal_subset(succ(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,negated_conjecture,
~ ! [A] :
( ordinal(A)
=> ! [B] :
( ordinal(B)
=> ( in(A,B)
<=> ordinal_subset(succ(A),B) ) ) ),
inference(negated_conjecture,[status(cth)],[f50]) ).
fof(f55,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [A,B,C] :
( ( subset(C,B)
& subset(A,B) )
=> subset(set_union2(A,C),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,plain,
! [A] :
( function(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f62,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [A] :
( ( epsilon_connected(A)
& epsilon_transitive(A) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f64,plain,
! [X0] :
( epsilon_transitive(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [X0] :
( epsilon_connected(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f66,plain,
! [A] :
( relation(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f67,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [A] :
( ( one_to_one(A)
& function(A)
& relation(A) )
| ~ function(A)
| ~ empty(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f71,plain,
! [X0] :
( one_to_one(X0)
| ~ function(X0)
| ~ empty(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f72,plain,
! [A] :
( ordinal(A)
| ~ epsilon_connected(A)
| ~ epsilon_transitive(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f73,plain,
! [X0] :
( ordinal(X0)
| ~ epsilon_connected(X0)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f74,plain,
! [A] :
( ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f77,plain,
! [X0] :
( ordinal(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f78,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f81,plain,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f82,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ( ! [C] :
( ( C != A
| in(C,B) )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f83,plain,
( ! [A,B] :
( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(miniscoping,[status(thm)],[f82]) ).
fof(f84,plain,
( ! [A,B] :
( ( ( sK0_skl(B,A) = A
| in(sK0_skl(B,A),B) )
& ( sK0_skl(B,A) != A
| ~ in(sK0_skl(B,A),B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f89,plain,
! [A] :
( epsilon_transitive(A)
<=> ! [B] :
( subset(B,A)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f90,plain,
! [A] :
( ( ? [B] :
( ~ subset(B,A)
& in(B,A) )
| epsilon_transitive(A) )
& ( ! [B] :
( subset(B,A)
| ~ in(B,A) )
| ~ epsilon_transitive(A) ) ),
inference(NNF_transformation,[status(thm)],[f89]) ).
fof(f91,plain,
( ! [A] :
( ? [B] :
( ~ subset(B,A)
& in(B,A) )
| epsilon_transitive(A) )
& ! [A] :
( ! [B] :
( subset(B,A)
| ~ in(B,A) )
| ~ epsilon_transitive(A) ) ),
inference(miniscoping,[status(thm)],[f90]) ).
fof(f92,plain,
( ! [A] :
( ( ~ subset(sK1_skl(A),A)
& in(sK1_skl(A),A) )
| epsilon_transitive(A) )
& ! [A] :
( ! [B] :
( subset(B,A)
| ~ in(B,A) )
| ~ epsilon_transitive(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f91]) ).
fof(f93,plain,
! [X0,X1] :
( subset(X1,X0)
| ~ in(X1,X0)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f96,plain,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,B)
| ~ in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f97,plain,
! [A,B] :
( ( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f96]) ).
fof(f98,plain,
( ! [A,B] :
( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f97]) ).
fof(f99,plain,
( ! [A,B] :
( ( ~ in(sK2_skl(B,A),B)
& in(sK2_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( in(X2,X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f101,plain,
! [X0,X1] :
( in(sK2_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f102,plain,
! [X0,X1] :
( ~ in(sK2_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f105,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f112,plain,
function(empty_set),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f115,plain,
epsilon_transitive(empty_set),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f116,plain,
epsilon_connected(empty_set),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f118,plain,
! [A,B] :
( relation(set_union2(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f119,plain,
! [X0,X1] :
( relation(set_union2(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
! [A,B] :
( ~ empty(set_union2(A,B))
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f121,plain,
! [A] :
( ! [B] : ~ empty(set_union2(A,B))
| empty(A) ),
inference(miniscoping,[status(thm)],[f120]) ).
fof(f122,plain,
! [X0,X1] :
( ~ empty(set_union2(X0,X1))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f125,plain,
! [X0] :
( epsilon_transitive(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f126,plain,
! [X0] :
( epsilon_connected(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f127,plain,
! [X0] :
( ordinal(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f138,plain,
( ordinal(sK5_skl)
& epsilon_connected(sK5_skl)
& epsilon_transitive(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f32]) ).
fof(f139,plain,
epsilon_transitive(sK5_skl),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f140,plain,
epsilon_connected(sK5_skl),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f142,plain,
( relation(sK6_skl)
& empty(sK6_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f33]) ).
fof(f143,plain,
empty(sK6_skl),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f145,plain,
empty(sK7_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f34]) ).
fof(f146,plain,
empty(sK7_skl),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f147,plain,
( function(sK8_skl)
& empty(sK8_skl)
& relation(sK8_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f35]) ).
fof(f149,plain,
empty(sK8_skl),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f150,plain,
function(sK8_skl),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f151,plain,
( ordinal(sK9_skl)
& epsilon_connected(sK9_skl)
& epsilon_transitive(sK9_skl)
& empty(sK9_skl)
& one_to_one(sK9_skl)
& function(sK9_skl)
& relation(sK9_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f36]) ).
fof(f152,plain,
relation(sK9_skl),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
function(sK9_skl),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f155,plain,
empty(sK9_skl),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f156,plain,
epsilon_transitive(sK9_skl),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f157,plain,
epsilon_connected(sK9_skl),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f168,plain,
( ordinal(sK13_skl)
& epsilon_connected(sK13_skl)
& epsilon_transitive(sK13_skl)
& ~ empty(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f40]) ).
fof(f170,plain,
epsilon_transitive(sK13_skl),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f171,plain,
epsilon_connected(sK13_skl),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f180,plain,
! [A,B] :
( ( ordinal_subset(A,B)
<=> subset(A,B) )
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f181,plain,
! [A,B] :
( ( ( ~ subset(A,B)
| ordinal_subset(A,B) )
& ( subset(A,B)
| ~ ordinal_subset(A,B) ) )
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(NNF_transformation,[status(thm)],[f180]) ).
fof(f182,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f183,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f189,plain,
! [X0] : in(X0,succ(X0)),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f190,plain,
! [X0] : set_union2(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f195,plain,
? [A] :
( ? [B] :
( ( in(A,B)
<~> ordinal_subset(succ(A),B) )
& ordinal(B) )
& ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f196,plain,
? [A] :
( ? [B] :
( ( ~ ordinal_subset(succ(A),B)
| ~ in(A,B) )
& ( ordinal_subset(succ(A),B)
| in(A,B) )
& ordinal(B) )
& ordinal(A) ),
inference(NNF_transformation,[status(thm)],[f195]) ).
fof(f197,plain,
( ( ~ ordinal_subset(succ(sK16_skl),sK17_skl)
| ~ in(sK16_skl,sK17_skl) )
& ( ordinal_subset(succ(sK16_skl),sK17_skl)
| in(sK16_skl,sK17_skl) )
& ordinal(sK17_skl)
& ordinal(sK16_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl]),skolemize(A,sK16_skl),skolemize(B,sK17_skl)],[f196]) ).
fof(f198,plain,
ordinal(sK16_skl),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f199,plain,
ordinal(sK17_skl),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f200,plain,
( ordinal_subset(succ(sK16_skl),sK17_skl)
| in(sK16_skl,sK17_skl) ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f201,plain,
( ~ ordinal_subset(succ(sK16_skl),sK17_skl)
| ~ in(sK16_skl,sK17_skl) ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f212,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f213,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f214,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f215,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f214]) ).
fof(f216,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f220,plain,
! [A,B,C] :
( subset(set_union2(A,C),B)
| ~ subset(C,B)
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f58]) ).
fof(f221,plain,
! [X0,X1,X2] :
( subset(set_union2(X0,X2),X1)
| ~ subset(X2,X1)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f229,definition,
( sQ2_spl
<=> in(sK16_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f230,plain,
( ~ sQ2_spl
| in(sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f229]) ).
fof(f232,definition,
( sQ3_spl
<=> ordinal_subset(succ(sK16_skl),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f233,plain,
( ~ sQ3_spl
| ordinal_subset(succ(sK16_skl),sK17_skl) ),
inference(component_clause,[status(thm)],[f232]) ).
fof(f235,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f200,f229,f232]) ).
fof(f236,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f201,f229,f232]) ).
fof(f237,plain,
! [X0] :
( one_to_one(X0)
| ~ function(X0)
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f71,f67]) ).
fof(f238,plain,
! [X0,X1] :
( X0 = X1
| ~ in(X0,singleton(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f85]) ).
fof(f242,plain,
( ~ sQ3_spl
| subset(succ(sK16_skl),sK17_skl)
| ~ ordinal(sK17_skl)
| ~ ordinal(succ(sK16_skl)) ),
inference(resolution,[status(thm)],[f182,f233]) ).
fof(f245,definition,
( sQ4_spl
<=> ordinal(succ(sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f247,plain,
( sQ4_spl
| ~ ordinal(succ(sK16_skl)) ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f248,definition,
( sQ5_spl
<=> ordinal(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f250,plain,
( sQ5_spl
| ~ ordinal(sK17_skl) ),
inference(component_clause,[status(thm)],[f248]) ).
fof(f251,definition,
( sQ6_spl
<=> subset(succ(sK16_skl),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f252,plain,
( ~ sQ6_spl
| subset(succ(sK16_skl),sK17_skl) ),
inference(component_clause,[status(thm)],[f251]) ).
fof(f254,plain,
( ~ sQ3_spl
| sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f242,f245,f248,f251,f232]) ).
fof(f259,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f250,f199]) ).
fof(f260,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f259]) ).
fof(f271,plain,
ordinal(sK6_skl),
inference(resolution,[status(thm)],[f143,f77]) ).
fof(f272,plain,
ordinal(sK7_skl),
inference(resolution,[status(thm)],[f146,f77]) ).
fof(f273,plain,
ordinal(sK8_skl),
inference(resolution,[status(thm)],[f149,f77]) ).
fof(f275,plain,
function(sK7_skl),
inference(resolution,[status(thm)],[f62,f146]) ).
fof(f276,plain,
function(sK6_skl),
inference(resolution,[status(thm)],[f62,f143]) ).
fof(f281,plain,
epsilon_transitive(sK17_skl),
inference(resolution,[status(thm)],[f64,f199]) ).
fof(f282,plain,
epsilon_transitive(sK16_skl),
inference(resolution,[status(thm)],[f64,f198]) ).
fof(f287,plain,
epsilon_connected(sK16_skl),
inference(resolution,[status(thm)],[f65,f198]) ).
fof(f288,plain,
( sQ4_spl
| ~ ordinal(sK16_skl) ),
inference(resolution,[status(thm)],[f247,f127]) ).
fof(f289,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f288,f198]) ).
fof(f290,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f289]) ).
fof(f293,plain,
epsilon_connected(sK6_skl),
inference(resolution,[status(thm)],[f271,f65]) ).
fof(f294,plain,
epsilon_transitive(sK6_skl),
inference(resolution,[status(thm)],[f271,f64]) ).
fof(f295,plain,
epsilon_connected(sK7_skl),
inference(resolution,[status(thm)],[f272,f65]) ).
fof(f296,plain,
epsilon_transitive(sK7_skl),
inference(resolution,[status(thm)],[f272,f64]) ).
fof(f297,plain,
epsilon_connected(sK8_skl),
inference(resolution,[status(thm)],[f273,f65]) ).
fof(f298,plain,
epsilon_transitive(sK8_skl),
inference(resolution,[status(thm)],[f273,f64]) ).
fof(f323,plain,
( one_to_one(sK9_skl)
| ~ function(sK9_skl) ),
inference(resolution,[status(thm)],[f237,f155]) ).
fof(f324,plain,
( one_to_one(sK8_skl)
| ~ function(sK8_skl) ),
inference(resolution,[status(thm)],[f237,f149]) ).
fof(f325,plain,
( one_to_one(sK7_skl)
| ~ function(sK7_skl) ),
inference(resolution,[status(thm)],[f237,f146]) ).
fof(f326,plain,
( one_to_one(sK6_skl)
| ~ function(sK6_skl) ),
inference(resolution,[status(thm)],[f237,f143]) ).
fof(f327,plain,
( one_to_one(empty_set)
| ~ function(empty_set) ),
inference(resolution,[status(thm)],[f237,f105]) ).
fof(f328,definition,
( sQ9_spl
<=> function(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f330,plain,
( sQ9_spl
| ~ function(sK9_skl) ),
inference(component_clause,[status(thm)],[f328]) ).
fof(f331,definition,
( sQ10_spl
<=> one_to_one(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f323,f328,f331]) ).
fof(f335,definition,
( sQ11_spl
<=> function(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f337,plain,
( sQ11_spl
| ~ function(sK8_skl) ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f338,definition,
( sQ12_spl
<=> one_to_one(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f341,plain,
( sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f324,f335,f338]) ).
fof(f342,definition,
( sQ13_spl
<=> function(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f344,plain,
( sQ13_spl
| ~ function(sK7_skl) ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f345,definition,
( sQ14_spl
<=> one_to_one(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f348,plain,
( sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f325,f342,f345]) ).
fof(f349,definition,
( sQ15_spl
<=> function(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f351,plain,
( sQ15_spl
| ~ function(sK6_skl) ),
inference(component_clause,[status(thm)],[f349]) ).
fof(f352,definition,
( sQ16_spl
<=> one_to_one(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f355,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f326,f349,f352]) ).
fof(f356,definition,
( sQ17_spl
<=> function(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f358,plain,
( sQ17_spl
| ~ function(empty_set) ),
inference(component_clause,[status(thm)],[f356]) ).
fof(f359,definition,
( sQ18_spl
<=> one_to_one(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f362,plain,
( sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f327,f356,f359]) ).
fof(f363,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f358,f112]) ).
fof(f364,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f363]) ).
fof(f365,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f351,f276]) ).
fof(f366,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f365]) ).
fof(f367,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f344,f275]) ).
fof(f368,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f367]) ).
fof(f369,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f337,f150]) ).
fof(f370,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f369]) ).
fof(f371,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f330,f153]) ).
fof(f372,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f371]) ).
fof(f373,plain,
( ordinal(sK13_skl)
| ~ epsilon_connected(sK13_skl) ),
inference(resolution,[status(thm)],[f73,f170]) ).
fof(f374,plain,
( ordinal(sK9_skl)
| ~ epsilon_connected(sK9_skl) ),
inference(resolution,[status(thm)],[f73,f156]) ).
fof(f375,plain,
( ordinal(sK8_skl)
| ~ epsilon_connected(sK8_skl) ),
inference(resolution,[status(thm)],[f73,f298]) ).
fof(f376,plain,
( ordinal(sK7_skl)
| ~ epsilon_connected(sK7_skl) ),
inference(resolution,[status(thm)],[f73,f296]) ).
fof(f377,plain,
( ordinal(sK6_skl)
| ~ epsilon_connected(sK6_skl) ),
inference(resolution,[status(thm)],[f73,f294]) ).
fof(f378,plain,
( ordinal(sK16_skl)
| ~ epsilon_connected(sK16_skl) ),
inference(resolution,[status(thm)],[f73,f282]) ).
fof(f380,plain,
( ordinal(sK5_skl)
| ~ epsilon_connected(sK5_skl) ),
inference(resolution,[status(thm)],[f73,f139]) ).
fof(f381,plain,
( ordinal(empty_set)
| ~ epsilon_connected(empty_set) ),
inference(resolution,[status(thm)],[f73,f115]) ).
fof(f383,definition,
( sQ19_spl
<=> epsilon_connected(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f385,plain,
( sQ19_spl
| ~ epsilon_connected(sK13_skl) ),
inference(component_clause,[status(thm)],[f383]) ).
fof(f386,definition,
( sQ20_spl
<=> ordinal(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f373,f383,f386]) ).
fof(f390,definition,
( sQ21_spl
<=> epsilon_connected(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f392,plain,
( sQ21_spl
| ~ epsilon_connected(sK9_skl) ),
inference(component_clause,[status(thm)],[f390]) ).
fof(f393,definition,
( sQ22_spl
<=> ordinal(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f396,plain,
( sQ22_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f374,f390,f393]) ).
fof(f397,definition,
( sQ23_spl
<=> epsilon_connected(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( sQ23_spl
| ~ epsilon_connected(sK8_skl) ),
inference(component_clause,[status(thm)],[f397]) ).
fof(f400,definition,
( sQ24_spl
<=> ordinal(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f403,plain,
( sQ24_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f375,f397,f400]) ).
fof(f404,definition,
( sQ25_spl
<=> epsilon_connected(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f406,plain,
( sQ25_spl
| ~ epsilon_connected(sK7_skl) ),
inference(component_clause,[status(thm)],[f404]) ).
fof(f407,definition,
( sQ26_spl
<=> ordinal(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f410,plain,
( sQ26_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f376,f404,f407]) ).
fof(f411,definition,
( sQ27_spl
<=> epsilon_connected(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f413,plain,
( sQ27_spl
| ~ epsilon_connected(sK6_skl) ),
inference(component_clause,[status(thm)],[f411]) ).
fof(f414,definition,
( sQ28_spl
<=> ordinal(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f417,plain,
( sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f377,f411,f414]) ).
fof(f418,definition,
( sQ29_spl
<=> epsilon_connected(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f420,plain,
( sQ29_spl
| ~ epsilon_connected(sK16_skl) ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f421,definition,
( sQ30_spl
<=> ordinal(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f424,plain,
( sQ30_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f378,f418,f421]) ).
fof(f429,definition,
( sQ32_spl
<=> epsilon_connected(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f431,plain,
( sQ32_spl
| ~ epsilon_connected(sK5_skl) ),
inference(component_clause,[status(thm)],[f429]) ).
fof(f432,definition,
( sQ33_spl
<=> ordinal(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f435,plain,
( sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f380,f429,f432]) ).
fof(f436,definition,
( sQ34_spl
<=> epsilon_connected(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f438,plain,
( sQ34_spl
| ~ epsilon_connected(empty_set) ),
inference(component_clause,[status(thm)],[f436]) ).
fof(f439,definition,
( sQ35_spl
<=> ordinal(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f442,plain,
( sQ35_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f381,f436,f439]) ).
fof(f443,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f438,f116]) ).
fof(f444,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f443]) ).
fof(f445,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f140]) ).
fof(f446,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f445]) ).
fof(f447,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f420,f287]) ).
fof(f448,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f447]) ).
fof(f449,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f413,f293]) ).
fof(f450,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f449]) ).
fof(f451,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f406,f295]) ).
fof(f452,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f451]) ).
fof(f453,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f399,f297]) ).
fof(f454,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f453]) ).
fof(f455,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f392,f157]) ).
fof(f456,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f455]) ).
fof(f457,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f385,f171]) ).
fof(f458,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f457]) ).
fof(f488,plain,
! [X0] : set_union2(empty_set,X0) = X0,
inference(paramodulation,[status(thm)],[f78,f190]) ).
fof(f494,plain,
sK9_skl = empty_set,
inference(resolution,[status(thm)],[f213,f155]) ).
fof(f509,plain,
! [X0] : set_union2(sK9_skl,X0) = X0,
inference(backward_demodulation,[status(thm)],[f494,f488]) ).
fof(f553,plain,
succ(sK9_skl) = singleton(sK9_skl),
inference(paramodulation,[status(thm)],[f509,f81]) ).
fof(f563,plain,
( epsilon_connected(singleton(sK9_skl))
| ~ ordinal(sK9_skl) ),
inference(paramodulation,[status(thm)],[f553,f126]) ).
fof(f564,plain,
( ordinal(singleton(sK9_skl))
| ~ ordinal(sK9_skl) ),
inference(paramodulation,[status(thm)],[f553,f127]) ).
fof(f565,plain,
( epsilon_transitive(singleton(sK9_skl))
| ~ ordinal(sK9_skl) ),
inference(paramodulation,[status(thm)],[f553,f125]) ).
fof(f569,definition,
( sQ37_spl
<=> epsilon_connected(singleton(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f572,plain,
( sQ37_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f563,f393,f569]) ).
fof(f573,definition,
( sQ38_spl
<=> ordinal(singleton(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f574,plain,
( ~ sQ38_spl
| ordinal(singleton(sK9_skl)) ),
inference(component_clause,[status(thm)],[f573]) ).
fof(f576,plain,
( sQ38_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f564,f393,f573]) ).
fof(f577,definition,
( sQ39_spl
<=> epsilon_transitive(singleton(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f578,plain,
( ~ sQ39_spl
| epsilon_transitive(singleton(sK9_skl)) ),
inference(component_clause,[status(thm)],[f577]) ).
fof(f580,plain,
( sQ39_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f565,f393,f577]) ).
fof(f590,plain,
! [X0] :
( ~ empty(X0)
| empty(sK9_skl) ),
inference(paramodulation,[status(thm)],[f509,f122]) ).
fof(f596,definition,
( sQ40_spl
<=> empty(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f599,definition,
! [X0] :
( sQ41_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f600,plain,
! [X0] :
( ~ sQ41_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f599]) ).
fof(f602,plain,
( sQ41_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f590,f596,f599]) ).
fof(f618,plain,
( ~ sQ2_spl
| subset(sK16_skl,sK17_skl)
| ~ epsilon_transitive(sK17_skl) ),
inference(resolution,[status(thm)],[f93,f230]) ).
fof(f620,plain,
! [X0] :
( subset(X0,succ(X0))
| ~ epsilon_transitive(succ(X0)) ),
inference(resolution,[status(thm)],[f93,f189]) ).
fof(f621,definition,
( sQ42_spl
<=> epsilon_transitive(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( sQ42_spl
| ~ epsilon_transitive(sK17_skl) ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f624,definition,
( sQ43_spl
<=> subset(sK16_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f625,plain,
( ~ sQ43_spl
| subset(sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f624]) ).
fof(f627,plain,
( ~ sQ2_spl
| sQ43_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f618,f621,f624,f229]) ).
fof(f628,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f623,f281]) ).
fof(f629,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f628]) ).
fof(f630,plain,
! [X0] :
( ordinal_subset(X0,succ(X0))
| ~ ordinal(succ(X0))
| ~ ordinal(X0)
| ~ epsilon_transitive(succ(X0)) ),
inference(resolution,[status(thm)],[f620,f183]) ).
fof(f631,plain,
( subset(sK9_skl,singleton(sK9_skl))
| ~ epsilon_transitive(succ(sK9_skl)) ),
inference(paramodulation,[status(thm)],[f553,f620]) ).
fof(f632,plain,
! [X0] :
( ordinal_subset(X0,succ(X0))
| ~ ordinal(succ(X0))
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f630,f64]) ).
fof(f633,definition,
( sQ44_spl
<=> epsilon_transitive(succ(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f635,plain,
( sQ44_spl
| ~ epsilon_transitive(succ(sK9_skl)) ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f636,definition,
( sQ45_spl
<=> subset(sK9_skl,singleton(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f639,plain,
( sQ45_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f631,f633,f636]) ).
fof(f640,plain,
( sQ44_spl
| ~ epsilon_transitive(singleton(sK9_skl)) ),
inference(forward_demodulation,[status(thm)],[f553,f635]) ).
fof(f641,plain,
( sQ44_spl
| ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f640,f578]) ).
fof(f642,plain,
( sQ44_spl
| ~ sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f641]) ).
fof(f644,plain,
( ~ sQ43_spl
| ordinal_subset(sK16_skl,sK17_skl)
| ~ ordinal(sK17_skl)
| ~ ordinal(sK16_skl) ),
inference(resolution,[status(thm)],[f625,f183]) ).
fof(f645,definition,
( sQ46_spl
<=> ordinal_subset(sK16_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f646,plain,
( ~ sQ46_spl
| ordinal_subset(sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f645]) ).
fof(f648,plain,
( ~ sQ43_spl
| sQ46_spl
| ~ sQ5_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f644,f421,f248,f645,f624]) ).
fof(f649,plain,
( ~ sQ46_spl
| subset(sK16_skl,sK17_skl)
| ~ ordinal(sK17_skl)
| ~ ordinal(sK16_skl) ),
inference(resolution,[status(thm)],[f646,f182]) ).
fof(f650,plain,
( ~ sQ46_spl
| sQ43_spl
| ~ sQ5_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f649,f421,f248,f624,f645]) ).
fof(f673,definition,
( sQ49_spl
<=> ordinal_subset(sK9_skl,singleton(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f685,plain,
! [X0,X1] :
( sK2_skl(X1,singleton(X0)) = X0
| subset(singleton(X0),X1) ),
inference(resolution,[status(thm)],[f101,f238]) ).
fof(f699,plain,
! [X0,X1] :
( in(X0,X1)
| ~ subset(succ(X0),X1) ),
inference(resolution,[status(thm)],[f100,f189]) ).
fof(f702,plain,
! [X0] :
( relation(X0)
| ~ relation(X0)
| ~ relation(sK9_skl) ),
inference(paramodulation,[status(thm)],[f509,f119]) ).
fof(f708,definition,
( sQ50_spl
<=> relation(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f710,plain,
( sQ50_spl
| ~ relation(sK9_skl) ),
inference(component_clause,[status(thm)],[f708]) ).
fof(f711,definition,
! [X0] :
( sQ51_spl
<=> ( relation(X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f714,plain,
( sQ51_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f702,f708,f711]) ).
fof(f716,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f710,f152]) ).
fof(f717,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f716]) ).
fof(f726,definition,
( sQ53_spl
<=> epsilon_transitive(succ(sK17_skl)) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f727,plain,
( ~ sQ53_spl
| epsilon_transitive(succ(sK17_skl)) ),
inference(component_clause,[status(thm)],[f726]) ).
fof(f728,plain,
( sQ53_spl
| ~ epsilon_transitive(succ(sK17_skl)) ),
inference(component_clause,[status(thm)],[f726]) ).
fof(f730,definition,
! [X0] :
( sQ54_spl
<=> in(sK16_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f731,plain,
! [X0] :
( ~ sQ54_spl
| in(sK16_skl,X0) ),
inference(component_clause,[status(thm)],[f730]) ).
fof(f747,plain,
! [X0] :
( ~ sQ54_spl
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f731,f216]) ).
fof(f749,plain,
( ~ sQ54_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f155,f747]) ).
fof(f751,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f749]) ).
fof(f785,plain,
( sQ53_spl
| ~ ordinal(sK17_skl) ),
inference(resolution,[status(thm)],[f728,f125]) ).
fof(f786,plain,
( sQ53_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f785,f248,f726]) ).
fof(f787,plain,
( ~ sQ53_spl
| ordinal(succ(sK17_skl))
| ~ epsilon_connected(succ(sK17_skl)) ),
inference(resolution,[status(thm)],[f727,f73]) ).
fof(f788,definition,
( sQ58_spl
<=> epsilon_connected(succ(sK17_skl)) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f790,plain,
( sQ58_spl
| ~ epsilon_connected(succ(sK17_skl)) ),
inference(component_clause,[status(thm)],[f788]) ).
fof(f791,definition,
( sQ59_spl
<=> ordinal(succ(sK17_skl)) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f792,plain,
( ~ sQ59_spl
| ordinal(succ(sK17_skl)) ),
inference(component_clause,[status(thm)],[f791]) ).
fof(f794,plain,
( ~ sQ53_spl
| sQ59_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f787,f788,f791,f726]) ).
fof(f795,plain,
( sQ58_spl
| ~ ordinal(sK17_skl) ),
inference(resolution,[status(thm)],[f790,f126]) ).
fof(f796,plain,
( sQ58_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f795,f248,f788]) ).
fof(f827,plain,
! [X0,X1,X2] :
( ordinal_subset(set_union2(X0,X2),X1)
| ~ ordinal(X1)
| ~ ordinal(set_union2(X0,X2))
| ~ subset(X2,X1)
| ~ subset(X0,X1) ),
inference(resolution,[status(thm)],[f221,f183]) ).
fof(f852,plain,
( ~ sQ6_spl
| in(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f699,f252]) ).
fof(f858,plain,
( ~ sQ6_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f852,f229,f251]) ).
fof(f902,definition,
( sQ65_spl
<=> epsilon_transitive(succ(succ(sK17_skl))) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f903,plain,
( ~ sQ65_spl
| epsilon_transitive(succ(succ(sK17_skl))) ),
inference(component_clause,[status(thm)],[f902]) ).
fof(f904,plain,
( sQ65_spl
| ~ epsilon_transitive(succ(succ(sK17_skl))) ),
inference(component_clause,[status(thm)],[f902]) ).
fof(f923,plain,
( sQ65_spl
| ~ ordinal(succ(sK17_skl)) ),
inference(resolution,[status(thm)],[f904,f125]) ).
fof(f924,plain,
( sQ65_spl
| ~ sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f923,f792]) ).
fof(f925,plain,
( sQ65_spl
| ~ sQ59_spl ),
inference(contradiction_clause,[status(thm)],[f924]) ).
fof(f928,plain,
! [X0,X1] :
( ordinal_subset(succ(X0),X1)
| ~ ordinal(X1)
| ~ ordinal(set_union2(X0,singleton(X0)))
| ~ subset(singleton(X0),X1)
| ~ subset(X0,X1) ),
inference(paramodulation,[status(thm)],[f81,f827]) ).
fof(f935,plain,
! [X0,X1] :
( ordinal_subset(succ(X0),X1)
| ~ ordinal(X1)
| ~ ordinal(succ(X0))
| ~ subset(singleton(X0),X1)
| ~ subset(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f81,f928]) ).
fof(f939,plain,
! [X0] :
( subset(X0,succ(X0))
| ~ ordinal(succ(X0))
| ~ ordinal(X0)
| ~ ordinal(succ(X0))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f632,f182]) ).
fof(f940,plain,
( ordinal_subset(sK9_skl,singleton(sK9_skl))
| ~ ordinal(succ(sK9_skl))
| ~ ordinal(sK9_skl) ),
inference(paramodulation,[status(thm)],[f553,f632]) ).
fof(f941,plain,
! [X0] :
( subset(X0,succ(X0))
| ~ ordinal(succ(X0))
| ~ ordinal(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f939]) ).
fof(f942,plain,
! [X0] :
( subset(X0,succ(X0))
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f941,f127]) ).
fof(f943,definition,
( sQ69_spl
<=> ordinal(succ(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f945,plain,
( sQ69_spl
| ~ ordinal(succ(sK9_skl)) ),
inference(component_clause,[status(thm)],[f943]) ).
fof(f946,plain,
( sQ49_spl
| ~ sQ69_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f940,f393,f943,f673]) ).
fof(f947,plain,
( ~ sQ65_spl
| ordinal(succ(succ(sK17_skl)))
| ~ epsilon_connected(succ(succ(sK17_skl))) ),
inference(resolution,[status(thm)],[f903,f73]) ).
fof(f948,definition,
( sQ70_spl
<=> epsilon_connected(succ(succ(sK17_skl))) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f950,plain,
( sQ70_spl
| ~ epsilon_connected(succ(succ(sK17_skl))) ),
inference(component_clause,[status(thm)],[f948]) ).
fof(f951,definition,
( sQ71_spl
<=> ordinal(succ(succ(sK17_skl))) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f954,plain,
( ~ sQ65_spl
| sQ71_spl
| ~ sQ70_spl ),
inference(split_clause,[status(thm)],[f947,f948,f951,f902]) ).
fof(f955,plain,
( sQ70_spl
| ~ ordinal(succ(sK17_skl)) ),
inference(resolution,[status(thm)],[f950,f126]) ).
fof(f956,plain,
( sQ70_spl
| ~ sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f955,f792]) ).
fof(f957,plain,
( sQ70_spl
| ~ sQ59_spl ),
inference(contradiction_clause,[status(thm)],[f956]) ).
fof(f969,plain,
! [X0] :
( in(X0,succ(succ(X0)))
| ~ ordinal(succ(X0)) ),
inference(resolution,[status(thm)],[f942,f699]) ).
fof(f1136,plain,
( in(sK9_skl,succ(singleton(sK9_skl)))
| ~ ordinal(succ(sK9_skl)) ),
inference(paramodulation,[status(thm)],[f553,f969]) ).
fof(f1138,definition,
( sQ83_spl
<=> in(sK9_skl,succ(singleton(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1139,plain,
( ~ sQ83_spl
| in(sK9_skl,succ(singleton(sK9_skl))) ),
inference(component_clause,[status(thm)],[f1138]) ).
fof(f1141,plain,
( sQ83_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f1136,f943,f1138]) ).
fof(f1142,plain,
( sQ69_spl
| ~ ordinal(singleton(sK9_skl)) ),
inference(forward_demodulation,[status(thm)],[f553,f945]) ).
fof(f1143,plain,
( sQ69_spl
| ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1142,f574]) ).
fof(f1144,plain,
( sQ69_spl
| ~ sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f1143]) ).
fof(f1148,plain,
( ~ sQ83_spl
| subset(sK9_skl,succ(singleton(sK9_skl)))
| ~ epsilon_transitive(succ(singleton(sK9_skl))) ),
inference(resolution,[status(thm)],[f1139,f93]) ).
fof(f1151,definition,
( sQ84_spl
<=> epsilon_transitive(succ(singleton(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1152,plain,
( ~ sQ84_spl
| epsilon_transitive(succ(singleton(sK9_skl))) ),
inference(component_clause,[status(thm)],[f1151]) ).
fof(f1153,plain,
( sQ84_spl
| ~ epsilon_transitive(succ(singleton(sK9_skl))) ),
inference(component_clause,[status(thm)],[f1151]) ).
fof(f1154,definition,
( sQ85_spl
<=> subset(sK9_skl,succ(singleton(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1155,plain,
( ~ sQ85_spl
| subset(sK9_skl,succ(singleton(sK9_skl))) ),
inference(component_clause,[status(thm)],[f1154]) ).
fof(f1157,plain,
( ~ sQ83_spl
| sQ85_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f1148,f1151,f1154,f1138]) ).
fof(f1158,plain,
( sQ84_spl
| ~ ordinal(singleton(sK9_skl)) ),
inference(resolution,[status(thm)],[f1153,f125]) ).
fof(f1159,plain,
( sQ84_spl
| ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1158,f574]) ).
fof(f1160,plain,
( sQ84_spl
| ~ sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f1159]) ).
fof(f1161,plain,
( ~ sQ84_spl
| ordinal(succ(singleton(sK9_skl)))
| ~ epsilon_connected(succ(singleton(sK9_skl))) ),
inference(resolution,[status(thm)],[f1152,f73]) ).
fof(f1162,definition,
( sQ86_spl
<=> epsilon_connected(succ(singleton(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1164,plain,
( sQ86_spl
| ~ epsilon_connected(succ(singleton(sK9_skl))) ),
inference(component_clause,[status(thm)],[f1162]) ).
fof(f1165,definition,
( sQ87_spl
<=> ordinal(succ(singleton(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1168,plain,
( ~ sQ84_spl
| sQ87_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f1161,f1162,f1165,f1151]) ).
fof(f1169,plain,
( sQ86_spl
| ~ ordinal(singleton(sK9_skl)) ),
inference(resolution,[status(thm)],[f1164,f126]) ).
fof(f1170,plain,
( sQ86_spl
| ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1169,f574]) ).
fof(f1171,plain,
( sQ86_spl
| ~ sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f1170]) ).
fof(f1226,plain,
( ~ sQ85_spl
| ordinal_subset(sK9_skl,succ(singleton(sK9_skl)))
| ~ ordinal(succ(singleton(sK9_skl)))
| ~ ordinal(sK9_skl) ),
inference(resolution,[status(thm)],[f1155,f183]) ).
fof(f1227,definition,
( sQ94_spl
<=> ordinal_subset(sK9_skl,succ(singleton(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1230,plain,
( ~ sQ85_spl
| sQ94_spl
| ~ sQ87_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f1226,f393,f1165,f1227,f1154]) ).
fof(f1264,plain,
! [X0,X1] :
( subset(singleton(X0),X1)
| ~ in(X0,X1)
| subset(singleton(X0),X1) ),
inference(paramodulation,[status(thm)],[f685,f102]) ).
fof(f1268,plain,
! [X0,X1] :
( ~ in(X0,X1)
| subset(singleton(X0),X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1264]) ).
fof(f1275,definition,
( sQ96_spl
<=> subset(singleton(sK16_skl),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1276,plain,
( ~ sQ96_spl
| subset(singleton(sK16_skl),sK17_skl) ),
inference(component_clause,[status(thm)],[f1275]) ).
fof(f1277,plain,
( sQ96_spl
| ~ subset(singleton(sK16_skl),sK17_skl) ),
inference(component_clause,[status(thm)],[f1275]) ).
fof(f1292,plain,
( ~ sQ96_spl
| ordinal_subset(succ(sK16_skl),sK17_skl)
| ~ ordinal(sK17_skl)
| ~ ordinal(succ(sK16_skl))
| ~ subset(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f1276,f935]) ).
fof(f1295,plain,
( ~ sQ96_spl
| sQ3_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1292,f624,f245,f248,f232,f1275]) ).
fof(f1345,plain,
( ~ sQ41_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f155,f600]) ).
fof(f1349,plain,
~ sQ41_spl,
inference(contradiction_clause,[status(thm)],[f1345]) ).
fof(f1430,plain,
( sQ96_spl
| ~ in(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f1268,f1277]) ).
fof(f1435,plain,
( sQ96_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1430,f229,f1275]) ).
fof(f1436,plain,
$false,
inference(sat_refutation,[status(thm)],[f235,f236,f254,f260,f290,f334,f341,f348,f355,f362,f364,f366,f368,f370,f372,f389,f396,f403,f410,f417,f424,f435,f442,f444,f446,f448,f450,f452,f454,f456,f458,f572,f576,f580,f602,f627,f629,f639,f642,f648,f650,f714,f717,f751,f786,f794,f796,f858,f925,f946,f954,f957,f1141,f1144,f1157,f1160,f1168,f1171,f1230,f1295,f1349,f1435]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU236+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 06:01:57 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.69/0.56 % Refutation found
% 0.69/0.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.69/0.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.69/0.57 % Elapsed time: 0.198351 seconds
% 0.69/0.57 % CPU time: 1.266658 seconds
% 0.69/0.57 % Total memory used: 125.389 MB
% 0.69/0.57 % Net memory used: 123.201 MB
%------------------------------------------------------------------------------