%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU298+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 : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:20:04 PM UTC 2026
% Result : Theorem 0.10s 0.41s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 73
% Syntax : Number of formulae : 318 ( 53 unt; 52 def)
% Number of atoms : 1087 ( 132 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 1223 ( 454 ~; 535 |; 164 &)
% ( 57 <=>; 12 =>; 0 <=; 1 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 65 ( 63 usr; 52 prp; 0-5 aty)
% Number of functors : 29 ( 29 usr; 11 con; 0-5 aty)
% Number of variables : 321 ( 257 !; 64 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A,B] :
( ( element(B,powerset(powerset(succ(A))))
& ordinal(A) )
=> ? [C] :
! [D] :
( in(D,C)
<=> ( ? [E] :
( D = set_difference(E,singleton(A))
& in(E,B) )
& in(D,powerset(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A,B] :
( ( element(B,powerset(powerset(succ(A))))
& ordinal(A) )
=> ? [C] :
! [D] :
( in(D,C)
<=> ( ? [E] :
( D = set_difference(E,singleton(A))
& in(E,B) )
& in(D,powerset(A)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,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/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,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(f6,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( ( function(A)
& empty(A)
& relation(A) )
=> ( one_to_one(A)
& function(A)
& relation(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] :
( ( epsilon_connected(A)
& epsilon_transitive(A) )
=> ordinal(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A] :
( empty(A)
=> ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A] :
( ordinal(A)
=> ( epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A,B] :
( ( element(B,powerset(powerset(succ(A))))
& ordinal(A) )
=> ( ! [C,D,E] :
( ( ? [G] :
( E = set_difference(G,singleton(A))
& in(G,B) )
& C = E
& ? [F] :
( D = set_difference(F,singleton(A))
& in(F,B) )
& C = D )
=> D = E )
=> ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( ? [H] :
( D = set_difference(H,singleton(A))
& in(H,B) )
& E = D
& in(E,powerset(A)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,plain,
? [A,B] :
( ! [C] :
? [D] :
( in(D,C)
<~> ( ? [E] :
( D = set_difference(E,singleton(A))
& in(E,B) )
& in(D,powerset(A)) ) )
& element(B,powerset(powerset(succ(A))))
& ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f45,plain,
? [A,B] :
( ! [C] :
? [D] :
( ( ! [E] :
( D != set_difference(E,singleton(A))
| ~ in(E,B) )
| ~ in(D,powerset(A))
| ~ in(D,C) )
& ( ( ? [E] :
( D = set_difference(E,singleton(A))
& in(E,B) )
& in(D,powerset(A)) )
| in(D,C) ) )
& element(B,powerset(powerset(succ(A))))
& ordinal(A) ),
inference(NNF_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
( ! [C] :
( ( ! [E] :
( sK2_skl(C) != set_difference(E,singleton(sK0_skl))
| ~ in(E,sK1_skl) )
| ~ in(sK2_skl(C),powerset(sK0_skl))
| ~ in(sK2_skl(C),C) )
& ( ( sK2_skl(C) = set_difference(sK3_skl(C),singleton(sK0_skl))
& in(sK3_skl(C),sK1_skl)
& in(sK2_skl(C),powerset(sK0_skl)) )
| in(sK2_skl(C),C) ) )
& element(sK1_skl,powerset(powerset(succ(sK0_skl))))
& ordinal(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(D,sK2_skl(C)),skolemize(E,sK3_skl(C))],[f45]) ).
fof(f47,plain,
ordinal(sK0_skl),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f48,plain,
element(sK1_skl,powerset(powerset(succ(sK0_skl)))),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f49,plain,
! [X0] :
( in(sK2_skl(X0),powerset(sK0_skl))
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f50,plain,
! [X0] :
( in(sK3_skl(X0),sK1_skl)
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f51,plain,
! [X0] :
( sK2_skl(X0) = set_difference(sK3_skl(X0),singleton(sK0_skl))
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f52,plain,
! [X0,X1] :
( sK2_skl(X0) != set_difference(X1,singleton(sK0_skl))
| ~ in(X1,sK1_skl)
| ~ in(sK2_skl(X0),powerset(sK0_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f53,plain,
! [A] :
( finite(sK4_skl(A))
& natural(sK4_skl(A))
& ordinal(sK4_skl(A))
& epsilon_connected(sK4_skl(A))
& epsilon_transitive(sK4_skl(A))
& one_to_one(sK4_skl(A))
& function(sK4_skl(A))
& relation(sK4_skl(A))
& empty(sK4_skl(A))
& element(sK4_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f3]) ).
fof(f54,plain,
! [X0] : element(sK4_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f64,plain,
( one_to_one(sK5_skl)
& function(sK5_skl)
& relation(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f4]) ).
fof(f65,plain,
relation(sK5_skl),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f68,plain,
( ordinal(sK6_skl)
& epsilon_connected(sK6_skl)
& epsilon_transitive(sK6_skl)
& empty(sK6_skl)
& one_to_one(sK6_skl)
& function(sK6_skl)
& relation(sK6_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f5]) ).
fof(f69,plain,
relation(sK6_skl),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
function(sK6_skl),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f72,plain,
empty(sK6_skl),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f73,plain,
epsilon_transitive(sK6_skl),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f74,plain,
epsilon_connected(sK6_skl),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f76,plain,
( function(sK7_skl)
& relation(sK7_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f6]) ).
fof(f77,plain,
relation(sK7_skl),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f79,plain,
( function(sK8_skl)
& empty(sK8_skl)
& relation(sK8_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f7]) ).
fof(f80,plain,
relation(sK8_skl),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f81,plain,
empty(sK8_skl),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f82,plain,
function(sK8_skl),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f83,plain,
! [A] :
( ( one_to_one(A)
& function(A)
& relation(A) )
| ~ function(A)
| ~ empty(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f86,plain,
! [X0] :
( one_to_one(X0)
| ~ function(X0)
| ~ empty(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f87,plain,
( relation(sK9_skl)
& empty(sK9_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f9]) ).
fof(f88,plain,
empty(sK9_skl),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f95,plain,
( natural(sK11_skl)
& ordinal(sK11_skl)
& epsilon_connected(sK11_skl)
& epsilon_transitive(sK11_skl)
& ~ empty(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f12]) ).
fof(f97,plain,
epsilon_transitive(sK11_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f98,plain,
epsilon_connected(sK11_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f112,plain,
! [A] :
( ? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f113,plain,
! [A] :
( ( finite(sK13_skl(A))
& ~ empty(sK13_skl(A))
& element(sK13_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(B,sK13_skl(A))],[f112]) ).
fof(f114,plain,
! [X0] :
( element(sK13_skl(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f131,plain,
! [A] :
( ordinal(A)
| ~ epsilon_connected(A)
| ~ epsilon_transitive(A) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f132,plain,
! [X0] :
( ordinal(X0)
| ~ epsilon_connected(X0)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
( ordinal(sK14_skl)
& epsilon_connected(sK14_skl)
& epsilon_transitive(sK14_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f23]) ).
fof(f134,plain,
epsilon_transitive(sK14_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
epsilon_connected(sK14_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f137,plain,
! [A] :
( ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f138,plain,
! [X0] :
( epsilon_transitive(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
! [X0] :
( epsilon_connected(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f141,plain,
( ordinal(sK15_skl)
& epsilon_connected(sK15_skl)
& epsilon_transitive(sK15_skl)
& ~ empty(sK15_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f25]) ).
fof(f143,plain,
epsilon_transitive(sK15_skl),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f144,plain,
epsilon_connected(sK15_skl),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f146,plain,
! [A] :
( ? [B] :
( ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f147,plain,
! [A] :
( ( ~ empty(sK16_skl(A))
& element(sK16_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(B,sK16_skl(A))],[f146]) ).
fof(f148,plain,
! [X0] :
( element(sK16_skl(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f150,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))],[f27]) ).
fof(f151,plain,
! [X0] : element(sK17_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f153,plain,
empty(sK18_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f28]) ).
fof(f154,plain,
empty(sK18_skl),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f157,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f158,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f167,plain,
! [A] :
( ( epsilon_connected(A)
& epsilon_transitive(A) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f168,plain,
! [X0] :
( epsilon_transitive(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,plain,
! [X0] :
( epsilon_connected(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f175,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f177,plain,
! [A,B] :
( ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( ? [H] :
( D = set_difference(H,singleton(A))
& in(H,B) )
& E = D
& in(E,powerset(A)) ) )
| ? [C,D,E] :
( D != E
& ? [G] :
( E = set_difference(G,singleton(A))
& in(G,B) )
& C = E
& ? [F] :
( D = set_difference(F,singleton(A))
& in(F,B) )
& C = D )
| ~ element(B,powerset(powerset(succ(A))))
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f178,definition,
! [A,B,C,D,E] :
( sP0_prd(E,D,C,B,A)
<=> ( D != E
& ? [G] :
( E = set_difference(G,singleton(A))
& in(G,B) )
& C = E
& ? [F] :
( D = set_difference(F,singleton(A))
& in(F,B) )
& C = D ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f179,plain,
! [A,B] :
( ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( ? [H] :
( D = set_difference(H,singleton(A))
& in(H,B) )
& E = D
& in(E,powerset(A)) ) )
| ? [C,D,E] : sP0_prd(E,D,C,B,A)
| ~ element(B,powerset(powerset(succ(A))))
| ~ ordinal(A) ),
inference(formula_renaming,[status(thm)],[f177,f178]) ).
fof(f180,plain,
! [A,B] :
( ? [C] :
! [D] :
( ( ! [E] :
( ! [H] :
( D != set_difference(H,singleton(A))
| ~ in(H,B) )
| E != D
| ~ in(E,powerset(A)) )
| in(D,C) )
& ( ? [E] :
( ? [H] :
( D = set_difference(H,singleton(A))
& in(H,B) )
& E = D
& in(E,powerset(A)) )
| ~ in(D,C) ) )
| ? [C,D,E] : sP0_prd(E,D,C,B,A)
| ~ element(B,powerset(powerset(succ(A))))
| ~ ordinal(A) ),
inference(NNF_transformation,[status(thm)],[f179]) ).
fof(f181,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ! [H] :
( D != set_difference(H,singleton(A))
| ~ in(H,B) )
| ! [E] :
( E != D
| ~ in(E,powerset(A)) )
| in(D,C) )
& ! [D] :
( ( ? [H] :
( D = set_difference(H,singleton(A))
& in(H,B) )
& ? [E] :
( E = D
& in(E,powerset(A)) ) )
| ~ in(D,C) ) )
| ? [C,D,E] : sP0_prd(E,D,C,B,A)
| ~ element(B,powerset(powerset(succ(A))))
| ~ ordinal(A) ),
inference(miniscoping,[status(thm)],[f180]) ).
fof(f182,plain,
! [A,B] :
( ( ! [D] :
( ! [H] :
( D != set_difference(H,singleton(A))
| ~ in(H,B) )
| ! [E] :
( E != D
| ~ in(E,powerset(A)) )
| in(D,sK23_skl(B,A)) )
& ! [D] :
( ( D = set_difference(sK25_skl(D,B,A),singleton(A))
& in(sK25_skl(D,B,A),B)
& sK24_skl(D,B,A) = D
& in(sK24_skl(D,B,A),powerset(A)) )
| ~ in(D,sK23_skl(B,A)) ) )
| sP0_prd(sK22_skl(B,A),sK21_skl(B,A),sK20_skl(B,A),B,A)
| ~ element(B,powerset(powerset(succ(A))))
| ~ ordinal(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl]),skolemize(C,sK20_skl(B,A)),skolemize(D,sK21_skl(B,A)),skolemize(E,sK22_skl(B,A)),skolemize(C,sK23_skl(B,A)),skolemize(E,sK24_skl(D,B,A)),skolemize(H,sK25_skl(D,B,A))],[f181]) ).
fof(f183,plain,
! [X0,X1,X2] :
( in(sK24_skl(X2,X1,X0),powerset(X0))
| ~ in(X2,sK23_skl(X1,X0))
| sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f184,plain,
! [X0,X1,X2] :
( sK24_skl(X2,X1,X0) = X2
| ~ in(X2,sK23_skl(X1,X0))
| sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f185,plain,
! [X0,X1,X2] :
( in(sK25_skl(X2,X1,X0),X1)
| ~ in(X2,sK23_skl(X1,X0))
| sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f186,plain,
! [X0,X1,X2] :
( X2 = set_difference(sK25_skl(X2,X1,X0),singleton(X0))
| ~ in(X2,sK23_skl(X1,X0))
| sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f187,plain,
! [X0,X1,X2,X3,X4] :
( X2 != set_difference(X4,singleton(X0))
| ~ in(X4,X1)
| X3 != X2
| ~ in(X3,powerset(X0))
| in(X2,sK23_skl(X1,X0))
| sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f188,plain,
! [A,B,C,D,E] :
( ( D = E
| ! [G] :
( E != set_difference(G,singleton(A))
| ~ in(G,B) )
| C != E
| ! [F] :
( D != set_difference(F,singleton(A))
| ~ in(F,B) )
| C != D
| sP0_prd(E,D,C,B,A) )
& ( ( D != E
& ? [G] :
( E = set_difference(G,singleton(A))
& in(G,B) )
& C = E
& ? [F] :
( D = set_difference(F,singleton(A))
& in(F,B) )
& C = D )
| ~ sP0_prd(E,D,C,B,A) ) ),
inference(NNF_transformation,[status(thm)],[f178]) ).
fof(f189,plain,
( ! [A,B,C,D,E] :
( D = E
| ! [G] :
( E != set_difference(G,singleton(A))
| ~ in(G,B) )
| C != E
| ! [F] :
( D != set_difference(F,singleton(A))
| ~ in(F,B) )
| C != D
| sP0_prd(E,D,C,B,A) )
& ! [A,B,C,D,E] :
( ( D != E
& ? [G] :
( E = set_difference(G,singleton(A))
& in(G,B) )
& C = E
& ? [F] :
( D = set_difference(F,singleton(A))
& in(F,B) )
& C = D )
| ~ sP0_prd(E,D,C,B,A) ) ),
inference(miniscoping,[status(thm)],[f188]) ).
fof(f190,plain,
( ! [A,B,C,D,E] :
( D = E
| ! [G] :
( E != set_difference(G,singleton(A))
| ~ in(G,B) )
| C != E
| ! [F] :
( D != set_difference(F,singleton(A))
| ~ in(F,B) )
| C != D
| sP0_prd(E,D,C,B,A) )
& ! [A,B,C,D,E] :
( ( D != E
& E = set_difference(sK27_skl(E,D,C,B,A),singleton(A))
& in(sK27_skl(E,D,C,B,A),B)
& C = E
& D = set_difference(sK26_skl(E,D,C,B,A),singleton(A))
& in(sK26_skl(E,D,C,B,A),B)
& C = D )
| ~ sP0_prd(E,D,C,B,A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl]),skolemize(F,sK26_skl(E,D,C,B,A)),skolemize(G,sK27_skl(E,D,C,B,A))],[f189]) ).
fof(f191,plain,
! [X0,X1,X2,X3,X4] :
( X2 = X1
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f194,plain,
! [X0,X1,X2,X3,X4] :
( X2 = X0
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f197,plain,
! [X0,X1,X2,X3,X4] :
( X1 != X0
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f199,plain,
! [X0,X1,X2] :
( ~ in(X2,X1)
| ~ in(set_difference(X2,singleton(X0)),powerset(X0))
| in(set_difference(X2,singleton(X0)),sK23_skl(X1,X0))
| sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f187]) ).
fof(f200,plain,
! [X0,X1,X2,X3] : ~ sP0_prd(X0,X0,X1,X2,X3),
inference(destructive_equality_resolution,[status(thm)],[f197]) ).
fof(f238,plain,
( one_to_one(sK8_skl)
| ~ empty(sK8_skl)
| ~ relation(sK8_skl) ),
inference(resolution,[status(thm)],[f86,f82]) ).
fof(f240,plain,
( one_to_one(sK6_skl)
| ~ empty(sK6_skl)
| ~ relation(sK6_skl) ),
inference(resolution,[status(thm)],[f86,f70]) ).
fof(f242,definition,
( sQ4_spl
<=> relation(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f244,plain,
( sQ4_spl
| ~ relation(sK8_skl) ),
inference(component_clause,[status(thm)],[f242]) ).
fof(f245,definition,
( sQ5_spl
<=> empty(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f247,plain,
( sQ5_spl
| ~ empty(sK8_skl) ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f248,definition,
( sQ6_spl
<=> one_to_one(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f251,plain,
( sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f238,f242,f245,f248]) ).
fof(f252,definition,
( sQ7_spl
<=> relation(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f254,plain,
( sQ7_spl
| ~ relation(sK7_skl) ),
inference(component_clause,[status(thm)],[f252]) ).
fof(f262,definition,
( sQ10_spl
<=> relation(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f264,plain,
( sQ10_spl
| ~ relation(sK6_skl) ),
inference(component_clause,[status(thm)],[f262]) ).
fof(f265,definition,
( sQ11_spl
<=> empty(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f267,plain,
( sQ11_spl
| ~ empty(sK6_skl) ),
inference(component_clause,[status(thm)],[f265]) ).
fof(f268,definition,
( sQ12_spl
<=> one_to_one(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f271,plain,
( sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f240,f262,f265,f268]) ).
fof(f272,definition,
( sQ13_spl
<=> relation(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f274,plain,
( sQ13_spl
| ~ relation(sK5_skl) ),
inference(component_clause,[status(thm)],[f272]) ).
fof(f282,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f274,f65]) ).
fof(f283,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f282]) ).
fof(f284,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f267,f72]) ).
fof(f285,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f284]) ).
fof(f286,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f264,f69]) ).
fof(f287,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f286]) ).
fof(f288,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f254,f77]) ).
fof(f289,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f288]) ).
fof(f304,plain,
epsilon_transitive(sK18_skl),
inference(resolution,[status(thm)],[f138,f154]) ).
fof(f306,plain,
epsilon_transitive(sK9_skl),
inference(resolution,[status(thm)],[f138,f88]) ).
fof(f307,plain,
epsilon_transitive(sK8_skl),
inference(resolution,[status(thm)],[f138,f81]) ).
fof(f310,plain,
epsilon_connected(sK18_skl),
inference(resolution,[status(thm)],[f139,f154]) ).
fof(f312,plain,
epsilon_connected(sK9_skl),
inference(resolution,[status(thm)],[f139,f88]) ).
fof(f313,plain,
epsilon_connected(sK8_skl),
inference(resolution,[status(thm)],[f139,f81]) ).
fof(f325,plain,
epsilon_transitive(sK0_skl),
inference(resolution,[status(thm)],[f168,f47]) ).
fof(f336,plain,
epsilon_connected(sK0_skl),
inference(resolution,[status(thm)],[f169,f47]) ).
fof(f359,plain,
( ordinal(sK0_skl)
| ~ epsilon_transitive(sK0_skl) ),
inference(resolution,[status(thm)],[f132,f336]) ).
fof(f361,plain,
( ordinal(sK8_skl)
| ~ epsilon_transitive(sK8_skl) ),
inference(resolution,[status(thm)],[f132,f313]) ).
fof(f362,plain,
( ordinal(sK9_skl)
| ~ epsilon_transitive(sK9_skl) ),
inference(resolution,[status(thm)],[f132,f312]) ).
fof(f363,plain,
( ordinal(sK18_skl)
| ~ epsilon_transitive(sK18_skl) ),
inference(resolution,[status(thm)],[f132,f310]) ).
fof(f366,plain,
( ordinal(sK15_skl)
| ~ epsilon_transitive(sK15_skl) ),
inference(resolution,[status(thm)],[f132,f144]) ).
fof(f367,plain,
( ordinal(sK14_skl)
| ~ epsilon_transitive(sK14_skl) ),
inference(resolution,[status(thm)],[f132,f135]) ).
fof(f368,plain,
( ordinal(sK11_skl)
| ~ epsilon_transitive(sK11_skl) ),
inference(resolution,[status(thm)],[f132,f98]) ).
fof(f369,plain,
( ordinal(sK6_skl)
| ~ epsilon_transitive(sK6_skl) ),
inference(resolution,[status(thm)],[f132,f74]) ).
fof(f370,definition,
( sQ18_spl
<=> epsilon_transitive(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f372,plain,
( sQ18_spl
| ~ epsilon_transitive(sK0_skl) ),
inference(component_clause,[status(thm)],[f370]) ).
fof(f373,definition,
( sQ19_spl
<=> ordinal(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f376,plain,
( sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f359,f370,f373]) ).
fof(f377,definition,
( sQ20_spl
<=> epsilon_transitive(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f379,plain,
( sQ20_spl
| ~ epsilon_transitive(sK8_skl) ),
inference(component_clause,[status(thm)],[f377]) ).
fof(f380,definition,
( sQ21_spl
<=> ordinal(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f383,plain,
( sQ21_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f361,f377,f380]) ).
fof(f384,definition,
( sQ22_spl
<=> epsilon_transitive(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f386,plain,
( sQ22_spl
| ~ epsilon_transitive(sK9_skl) ),
inference(component_clause,[status(thm)],[f384]) ).
fof(f387,definition,
( sQ23_spl
<=> ordinal(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f390,plain,
( sQ23_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f362,f384,f387]) ).
fof(f391,definition,
( sQ24_spl
<=> epsilon_transitive(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( sQ24_spl
| ~ epsilon_transitive(sK18_skl) ),
inference(component_clause,[status(thm)],[f391]) ).
fof(f394,definition,
( sQ25_spl
<=> ordinal(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f397,plain,
( sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f363,f391,f394]) ).
fof(f398,definition,
( sQ26_spl
<=> epsilon_transitive(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f400,plain,
( sQ26_spl
| ~ epsilon_transitive(sK15_skl) ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f401,definition,
( sQ27_spl
<=> ordinal(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f404,plain,
( sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f366,f398,f401]) ).
fof(f405,definition,
( sQ28_spl
<=> epsilon_transitive(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f407,plain,
( sQ28_spl
| ~ epsilon_transitive(sK14_skl) ),
inference(component_clause,[status(thm)],[f405]) ).
fof(f408,definition,
( sQ29_spl
<=> ordinal(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f411,plain,
( sQ29_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f367,f405,f408]) ).
fof(f412,definition,
( sQ30_spl
<=> epsilon_transitive(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f414,plain,
( sQ30_spl
| ~ epsilon_transitive(sK11_skl) ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f415,definition,
( sQ31_spl
<=> ordinal(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f418,plain,
( sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f368,f412,f415]) ).
fof(f419,definition,
( sQ32_spl
<=> epsilon_transitive(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f421,plain,
( sQ32_spl
| ~ epsilon_transitive(sK6_skl) ),
inference(component_clause,[status(thm)],[f419]) ).
fof(f422,definition,
( sQ33_spl
<=> ordinal(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f425,plain,
( sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f369,f419,f422]) ).
fof(f426,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f421,f73]) ).
fof(f427,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f426]) ).
fof(f428,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f414,f97]) ).
fof(f429,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f428]) ).
fof(f430,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f407,f134]) ).
fof(f431,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f430]) ).
fof(f432,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f400,f143]) ).
fof(f433,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f432]) ).
fof(f434,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f393,f304]) ).
fof(f435,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f434]) ).
fof(f436,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f386,f306]) ).
fof(f437,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f436]) ).
fof(f438,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f379,f307]) ).
fof(f439,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f438]) ).
fof(f440,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f372,f325]) ).
fof(f441,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f440]) ).
fof(f479,plain,
! [X0,X1,X2] :
( sK20_skl(X1,X0) = sK22_skl(X1,X0)
| in(sK24_skl(X2,X1,X0),powerset(X0))
| ~ in(X2,sK23_skl(X1,X0))
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f183,f194]) ).
fof(f481,plain,
! [X0,X1,X2] :
( sK20_skl(X1,X0) = sK22_skl(X1,X0)
| sK24_skl(X2,X1,X0) = X2
| ~ in(X2,sK23_skl(X1,X0))
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f184,f194]) ).
fof(f483,plain,
! [X0,X1,X2] :
( sK20_skl(X1,X0) = sK22_skl(X1,X0)
| in(sK25_skl(X2,X1,X0),X1)
| ~ in(X2,sK23_skl(X1,X0))
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f185,f194]) ).
fof(f493,plain,
! [X0] :
( sK20_skl(sK1_skl,sK0_skl) = sK22_skl(sK1_skl,sK0_skl)
| sK24_skl(X0,sK1_skl,sK0_skl) = X0
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl))
| ~ ordinal(sK0_skl) ),
inference(resolution,[status(thm)],[f481,f48]) ).
fof(f496,definition,
! [X0] :
( sQ36_spl
<=> ( sK24_skl(X0,sK1_skl,sK0_skl) = X0
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f497,plain,
! [X0] :
( ~ sQ36_spl
| sK24_skl(X0,sK1_skl,sK0_skl) = X0
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,definition,
( sQ37_spl
<=> sK20_skl(sK1_skl,sK0_skl) = sK22_skl(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f500,plain,
( ~ sQ37_spl
| sK20_skl(sK1_skl,sK0_skl) = sK22_skl(sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f502,plain,
( sQ37_spl
| sQ36_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f493,f373,f496,f499]) ).
fof(f503,plain,
! [X0] :
( ~ sQ37_spl
| in(sK25_skl(X0,sK1_skl,sK0_skl),sK1_skl)
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl))
| sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(paramodulation,[status(thm)],[f500,f185]) ).
fof(f504,plain,
! [X0] :
( ~ sQ37_spl
| sK24_skl(X0,sK1_skl,sK0_skl) = X0
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl))
| sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(paramodulation,[status(thm)],[f500,f184]) ).
fof(f505,plain,
! [X0] :
( ~ sQ37_spl
| in(sK24_skl(X0,sK1_skl,sK0_skl),powerset(sK0_skl))
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl))
| sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(paramodulation,[status(thm)],[f500,f183]) ).
fof(f506,definition,
( sQ38_spl
<=> element(sK1_skl,powerset(powerset(succ(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( sQ38_spl
| ~ element(sK1_skl,powerset(powerset(succ(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f506]) ).
fof(f509,definition,
( sQ39_spl
<=> sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f510,plain,
( ~ sQ39_spl
| sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f509]) ).
fof(f512,definition,
! [X0] :
( sQ40_spl
<=> ( in(sK25_skl(X0,sK1_skl,sK0_skl),sK1_skl)
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f513,plain,
! [X0] :
( ~ sQ40_spl
| in(sK25_skl(X0,sK1_skl,sK0_skl),sK1_skl)
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f512]) ).
fof(f515,plain,
( ~ sQ37_spl
| sQ40_spl
| sQ39_spl
| ~ sQ38_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f503,f373,f506,f509,f512,f499]) ).
fof(f516,plain,
( ~ sQ37_spl
| sQ36_spl
| sQ39_spl
| ~ sQ38_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f504,f373,f506,f509,f496,f499]) ).
fof(f517,definition,
! [X0] :
( sQ41_spl
<=> ( in(sK24_skl(X0,sK1_skl,sK0_skl),powerset(sK0_skl))
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f518,plain,
! [X0] :
( ~ sQ41_spl
| in(sK24_skl(X0,sK1_skl,sK0_skl),powerset(sK0_skl))
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f517]) ).
fof(f520,plain,
( ~ sQ37_spl
| sQ41_spl
| sQ39_spl
| ~ sQ38_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f505,f373,f506,f509,f517,f499]) ).
fof(f521,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f508,f48]) ).
fof(f522,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f521]) ).
fof(f553,definition,
( sQ47_spl
<=> in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( ~ sQ47_spl
| in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f555,plain,
( sQ47_spl
| ~ in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,definition,
( sQ48_spl
<=> in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f566,plain,
( ~ sQ39_spl
| sK20_skl(sK1_skl,sK0_skl) = sK21_skl(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f510,f191]) ).
fof(f567,plain,
( ~ sQ39_spl
| sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f566,f510]) ).
fof(f571,plain,
( ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f567,f200]) ).
fof(f572,plain,
~ sQ39_spl,
inference(contradiction_clause,[status(thm)],[f571]) ).
fof(f607,plain,
! [X0] :
( sK20_skl(sK1_skl,sK0_skl) = sK22_skl(sK1_skl,sK0_skl)
| in(sK25_skl(X0,sK1_skl,sK0_skl),sK1_skl)
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl))
| ~ ordinal(sK0_skl) ),
inference(resolution,[status(thm)],[f483,f48]) ).
fof(f610,plain,
( sQ37_spl
| sQ40_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f607,f373,f512,f499]) ).
fof(f611,plain,
! [X0,X1,X2] :
( sK20_skl(X1,X0) = sK22_skl(X1,X0)
| X2 = set_difference(sK25_skl(X2,X1,X0),singleton(X0))
| ~ in(X2,sK23_skl(X1,X0))
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f186,f194]) ).
fof(f612,plain,
! [X0,X1,X2] :
( sK20_skl(X1,X0) = sK21_skl(X1,X0)
| X2 = set_difference(sK25_skl(X2,X1,X0),singleton(X0))
| ~ in(X2,sK23_skl(X1,X0))
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f186,f191]) ).
fof(f613,plain,
! [X0,X1,X2] :
( sK20_skl(X1,X0) = sK22_skl(X1,X0)
| ~ in(X2,X1)
| ~ in(set_difference(X2,singleton(X0)),powerset(X0))
| in(set_difference(X2,singleton(X0)),sK23_skl(X1,X0))
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f199,f194]) ).
fof(f614,plain,
! [X0,X1,X2] :
( sK20_skl(X1,X0) = sK21_skl(X1,X0)
| ~ in(X2,X1)
| ~ in(set_difference(X2,singleton(X0)),powerset(X0))
| in(set_difference(X2,singleton(X0)),sK23_skl(X1,X0))
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f199,f191]) ).
fof(f627,plain,
! [X0,X1] :
( ~ in(sK25_skl(sK2_skl(X1),X0,sK0_skl),sK1_skl)
| ~ in(sK2_skl(X1),powerset(sK0_skl))
| ~ in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(resolution,[status(thm)],[f611,f52]) ).
fof(f628,definition,
! [X0,X1] :
( sQ51_spl
<=> ( ~ in(sK25_skl(sK2_skl(X1),X0,sK0_skl),sK1_skl)
| ~ in(sK2_skl(X1),powerset(sK0_skl))
| ~ in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f629,plain,
! [X0,X1] :
( ~ sQ51_spl
| ~ in(sK25_skl(sK2_skl(X1),X0,sK0_skl),sK1_skl)
| ~ in(sK2_skl(X1),powerset(sK0_skl))
| ~ in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f628]) ).
fof(f631,plain,
( sQ51_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f627,f373,f628]) ).
fof(f632,plain,
! [X0] :
( ~ sQ40_spl
| ~ sQ51_spl
| ~ in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl))
| ~ in(sK2_skl(X0),powerset(sK0_skl))
| ~ in(sK2_skl(X0),X0)
| sK20_skl(sK1_skl,sK0_skl) = sK22_skl(sK1_skl,sK0_skl)
| ~ in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl))
| ~ element(sK1_skl,powerset(powerset(succ(sK0_skl)))) ),
inference(resolution,[status(thm)],[f629,f513]) ).
fof(f633,definition,
! [X0] :
( sQ52_spl
<=> ( ~ in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl))
| ~ in(sK2_skl(X0),powerset(sK0_skl))
| ~ in(sK2_skl(X0),X0)
| ~ in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f634,plain,
! [X0] :
( ~ sQ52_spl
| ~ in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl))
| ~ in(sK2_skl(X0),powerset(sK0_skl))
| ~ in(sK2_skl(X0),X0)
| ~ in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f636,plain,
( ~ sQ40_spl
| ~ sQ51_spl
| sQ37_spl
| sQ52_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f632,f506,f633,f499,f628,f512]) ).
fof(f637,plain,
! [X0] :
( ~ sQ52_spl
| ~ in(sK2_skl(X0),powerset(sK0_skl))
| ~ in(sK2_skl(X0),X0)
| ~ in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f634]) ).
fof(f640,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f247,f81]) ).
fof(f641,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f640]) ).
fof(f642,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f244,f80]) ).
fof(f643,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f642]) ).
fof(f644,plain,
! [X0] :
( ~ sQ37_spl
| ~ in(X0,sK1_skl)
| ~ in(set_difference(X0,singleton(sK0_skl)),powerset(sK0_skl))
| in(set_difference(X0,singleton(sK0_skl)),sK23_skl(sK1_skl,sK0_skl))
| sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(paramodulation,[status(thm)],[f500,f199]) ).
fof(f645,plain,
! [X0] :
( ~ sQ37_spl
| X0 = set_difference(sK25_skl(X0,sK1_skl,sK0_skl),singleton(sK0_skl))
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl))
| sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(paramodulation,[status(thm)],[f500,f186]) ).
fof(f649,definition,
! [X0] :
( sQ53_spl
<=> ( ~ in(X0,sK1_skl)
| ~ in(set_difference(X0,singleton(sK0_skl)),powerset(sK0_skl))
| in(set_difference(X0,singleton(sK0_skl)),sK23_skl(sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f650,plain,
! [X0] :
( ~ sQ53_spl
| ~ in(X0,sK1_skl)
| ~ in(set_difference(X0,singleton(sK0_skl)),powerset(sK0_skl))
| in(set_difference(X0,singleton(sK0_skl)),sK23_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f649]) ).
fof(f652,plain,
( ~ sQ37_spl
| sQ53_spl
| sQ39_spl
| ~ sQ38_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f644,f373,f506,f509,f649,f499]) ).
fof(f653,definition,
! [X0] :
( sQ54_spl
<=> ( X0 = set_difference(sK25_skl(X0,sK1_skl,sK0_skl),singleton(sK0_skl))
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f654,plain,
! [X0] :
( ~ sQ54_spl
| X0 = set_difference(sK25_skl(X0,sK1_skl,sK0_skl),singleton(sK0_skl))
| ~ in(X0,sK23_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f653]) ).
fof(f656,plain,
( ~ sQ37_spl
| sQ54_spl
| sQ39_spl
| ~ sQ38_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f645,f373,f506,f509,f653,f499]) ).
fof(f662,plain,
! [X0] :
( ~ sQ54_spl
| ~ in(sK25_skl(sK2_skl(X0),sK1_skl,sK0_skl),sK1_skl)
| ~ in(sK2_skl(X0),powerset(sK0_skl))
| ~ in(sK2_skl(X0),X0)
| ~ in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f654,f52]) ).
fof(f663,plain,
! [X0] :
( ~ sQ54_spl
| ~ sQ40_spl
| ~ in(sK2_skl(X0),powerset(sK0_skl))
| ~ in(sK2_skl(X0),X0)
| ~ in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f662,f513]) ).
fof(f672,plain,
! [X0] :
( ~ sQ53_spl
| in(sK2_skl(X0),X0)
| ~ in(sK3_skl(X0),sK1_skl)
| ~ in(set_difference(sK3_skl(X0),singleton(sK0_skl)),powerset(sK0_skl))
| in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f51,f650]) ).
fof(f673,plain,
! [X0] :
( ~ sQ53_spl
| in(sK2_skl(X0),X0)
| ~ in(set_difference(sK3_skl(X0),singleton(sK0_skl)),powerset(sK0_skl))
| in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f672,f50]) ).
fof(f674,plain,
! [X0] :
( ~ sQ53_spl
| in(sK2_skl(X0),X0)
| in(sK2_skl(X0),X0)
| ~ in(sK2_skl(X0),powerset(sK0_skl))
| in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f51,f673]) ).
fof(f675,plain,
! [X0] :
( ~ sQ53_spl
| in(sK2_skl(X0),X0)
| ~ in(sK2_skl(X0),powerset(sK0_skl))
| in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f674]) ).
fof(f676,plain,
! [X0] :
( ~ sQ53_spl
| in(sK2_skl(X0),X0)
| in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f675,f49]) ).
fof(f677,plain,
( sQ47_spl
| ~ sQ53_spl
| in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f676,f555]) ).
fof(f681,plain,
( sQ47_spl
| ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f677,f555]) ).
fof(f682,plain,
( sQ47_spl
| ~ sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f681]) ).
fof(f684,plain,
( ~ sQ54_spl
| ~ sQ40_spl
| ~ sQ47_spl
| ~ in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))
| ~ in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f554,f663]) ).
fof(f685,plain,
( ~ sQ36_spl
| ~ sQ47_spl
| sK24_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK23_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f554,f497]) ).
fof(f687,plain,
( ~ sQ54_spl
| ~ sQ40_spl
| ~ sQ48_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f684,f553,f556,f512,f653]) ).
fof(f689,plain,
( ~ sQ36_spl
| ~ sQ47_spl
| ~ sQ41_spl
| in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))
| ~ in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f685,f518]) ).
fof(f693,plain,
( ~ sQ36_spl
| ~ sQ47_spl
| sK20_skl(sK1_skl,sK0_skl) = sK22_skl(sK1_skl,sK0_skl)
| in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))
| ~ in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl))
| ~ element(sK1_skl,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(paramodulation,[status(thm)],[f685,f479]) ).
fof(f698,plain,
( ~ sQ36_spl
| ~ sQ41_spl
| sQ48_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f689,f553,f556,f517,f496]) ).
fof(f702,plain,
( ~ sQ36_spl
| sQ37_spl
| sQ48_spl
| ~ sQ47_spl
| ~ sQ38_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f693,f373,f506,f553,f556,f499,f496]) ).
fof(f705,plain,
! [X0,X1] :
( ~ in(sK25_skl(sK2_skl(X1),X0,sK0_skl),sK1_skl)
| ~ in(sK2_skl(X1),powerset(sK0_skl))
| ~ in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK21_skl(X0,sK0_skl)
| ~ in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(resolution,[status(thm)],[f612,f52]) ).
fof(f706,definition,
! [X0,X1] :
( sQ56_spl
<=> ( ~ in(sK25_skl(sK2_skl(X1),X0,sK0_skl),sK1_skl)
| ~ in(sK2_skl(X1),powerset(sK0_skl))
| ~ in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK21_skl(X0,sK0_skl)
| ~ in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f709,plain,
( sQ56_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f705,f373,f706]) ).
fof(f711,plain,
! [X0,X1,X2] :
( ~ in(sK23_skl(X1,X0),set_difference(X2,singleton(X0)))
| sK20_skl(X1,X0) = sK22_skl(X1,X0)
| ~ in(X2,X1)
| ~ in(set_difference(X2,singleton(X0)),powerset(X0))
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f613,f158]) ).
fof(f712,plain,
! [X0,X1] :
( in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(set_difference(sK3_skl(X1),singleton(sK0_skl)),powerset(sK0_skl))
| in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(paramodulation,[status(thm)],[f51,f613]) ).
fof(f717,definition,
! [X0,X1] :
( sQ58_spl
<=> ( in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(set_difference(sK3_skl(X1),singleton(sK0_skl)),powerset(sK0_skl))
| in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f718,plain,
! [X0,X1] :
( ~ sQ58_spl
| in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(set_difference(sK3_skl(X1),singleton(sK0_skl)),powerset(sK0_skl))
| in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f717]) ).
fof(f720,plain,
( sQ58_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f712,f373,f717]) ).
fof(f722,plain,
! [X0,X1,X2] :
( ~ in(sK23_skl(X1,X0),set_difference(X2,singleton(X0)))
| sK20_skl(X1,X0) = sK21_skl(X1,X0)
| ~ in(X2,X1)
| ~ in(set_difference(X2,singleton(X0)),powerset(X0))
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f614,f158]) ).
fof(f723,plain,
! [X0,X1] :
( in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK21_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(set_difference(sK3_skl(X1),singleton(sK0_skl)),powerset(sK0_skl))
| in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(paramodulation,[status(thm)],[f51,f614]) ).
fof(f725,definition,
! [X0,X1] :
( sQ59_spl
<=> ( in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK21_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(set_difference(sK3_skl(X1),singleton(sK0_skl)),powerset(sK0_skl))
| in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f728,plain,
( sQ59_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f723,f373,f725]) ).
fof(f754,plain,
! [X0,X1] :
( in(sK2_skl(X1),X1)
| ~ in(sK23_skl(X0,sK0_skl),sK2_skl(X1))
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(set_difference(sK3_skl(X1),singleton(sK0_skl)),powerset(sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(paramodulation,[status(thm)],[f51,f711]) ).
fof(f755,definition,
! [X0,X1] :
( sQ62_spl
<=> ( in(sK2_skl(X1),X1)
| ~ in(sK23_skl(X0,sK0_skl),sK2_skl(X1))
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(set_difference(sK3_skl(X1),singleton(sK0_skl)),powerset(sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( sQ62_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f754,f373,f755]) ).
fof(f759,plain,
! [X0,X1] :
( in(sK2_skl(X1),X1)
| ~ in(sK23_skl(X0,sK0_skl),sK2_skl(X1))
| sK20_skl(X0,sK0_skl) = sK21_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(set_difference(sK3_skl(X1),singleton(sK0_skl)),powerset(sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl))))
| ~ ordinal(sK0_skl) ),
inference(paramodulation,[status(thm)],[f51,f722]) ).
fof(f760,definition,
! [X0,X1] :
( sQ63_spl
<=> ( in(sK2_skl(X1),X1)
| ~ in(sK23_skl(X0,sK0_skl),sK2_skl(X1))
| sK20_skl(X0,sK0_skl) = sK21_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(set_difference(sK3_skl(X1),singleton(sK0_skl)),powerset(sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f763,plain,
( sQ63_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f759,f373,f760]) ).
fof(f764,plain,
! [X0,X1] :
( ~ sQ58_spl
| in(sK2_skl(X1),X1)
| in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(sK2_skl(X1),powerset(sK0_skl))
| in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ),
inference(paramodulation,[status(thm)],[f51,f718]) ).
fof(f765,plain,
! [X0,X1] :
( ~ sQ58_spl
| in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| ~ in(sK2_skl(X1),powerset(sK0_skl))
| in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ),
inference(duplicate_literals_removal,[status(thm)],[f764]) ).
fof(f766,plain,
! [X0,X1] :
( ~ sQ58_spl
| in(sK2_skl(X1),X1)
| sK20_skl(X0,sK0_skl) = sK22_skl(X0,sK0_skl)
| ~ in(sK3_skl(X1),X0)
| in(sK2_skl(X1),sK23_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(succ(sK0_skl)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f765,f49]) ).
fof(f767,plain,
! [X0] :
( ~ sQ58_spl
| empty(powerset(succ(sK0_skl)))
| in(sK2_skl(X0),X0)
| sK20_skl(sK16_skl(powerset(succ(sK0_skl))),sK0_skl) = sK22_skl(sK16_skl(powerset(succ(sK0_skl))),sK0_skl)
| ~ in(sK3_skl(X0),sK16_skl(powerset(succ(sK0_skl))))
| in(sK2_skl(X0),sK23_skl(sK16_skl(powerset(succ(sK0_skl))),sK0_skl)) ),
inference(resolution,[status(thm)],[f766,f148]) ).
fof(f768,plain,
! [X0] :
( ~ sQ58_spl
| empty(powerset(succ(sK0_skl)))
| in(sK2_skl(X0),X0)
| sK20_skl(sK13_skl(powerset(succ(sK0_skl))),sK0_skl) = sK22_skl(sK13_skl(powerset(succ(sK0_skl))),sK0_skl)
| ~ in(sK3_skl(X0),sK13_skl(powerset(succ(sK0_skl))))
| in(sK2_skl(X0),sK23_skl(sK13_skl(powerset(succ(sK0_skl))),sK0_skl)) ),
inference(resolution,[status(thm)],[f766,f114]) ).
fof(f769,plain,
! [X0] :
( ~ sQ58_spl
| in(sK2_skl(X0),X0)
| sK20_skl(sK17_skl(powerset(succ(sK0_skl))),sK0_skl) = sK22_skl(sK17_skl(powerset(succ(sK0_skl))),sK0_skl)
| ~ in(sK3_skl(X0),sK17_skl(powerset(succ(sK0_skl))))
| in(sK2_skl(X0),sK23_skl(sK17_skl(powerset(succ(sK0_skl))),sK0_skl)) ),
inference(resolution,[status(thm)],[f766,f151]) ).
fof(f770,plain,
! [X0] :
( ~ sQ58_spl
| in(sK2_skl(X0),X0)
| sK20_skl(sK4_skl(powerset(succ(sK0_skl))),sK0_skl) = sK22_skl(sK4_skl(powerset(succ(sK0_skl))),sK0_skl)
| ~ in(sK3_skl(X0),sK4_skl(powerset(succ(sK0_skl))))
| in(sK2_skl(X0),sK23_skl(sK4_skl(powerset(succ(sK0_skl))),sK0_skl)) ),
inference(resolution,[status(thm)],[f766,f54]) ).
fof(f771,plain,
! [X0] :
( ~ sQ58_spl
| in(sK2_skl(X0),X0)
| sK20_skl(sK1_skl,sK0_skl) = sK22_skl(sK1_skl,sK0_skl)
| ~ in(sK3_skl(X0),sK1_skl)
| in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f766,f48]) ).
fof(f772,definition,
! [X0] :
( sQ64_spl
<=> ( in(sK2_skl(X0),X0)
| ~ in(sK3_skl(X0),sK16_skl(powerset(succ(sK0_skl))))
| in(sK2_skl(X0),sK23_skl(sK16_skl(powerset(succ(sK0_skl))),sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f775,definition,
( sQ65_spl
<=> sK20_skl(sK16_skl(powerset(succ(sK0_skl))),sK0_skl) = sK22_skl(sK16_skl(powerset(succ(sK0_skl))),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f778,definition,
( sQ66_spl
<=> empty(powerset(succ(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f779,plain,
( ~ sQ66_spl
| empty(powerset(succ(sK0_skl))) ),
inference(component_clause,[status(thm)],[f778]) ).
fof(f781,plain,
( ~ sQ58_spl
| sQ66_spl
| sQ65_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f767,f772,f775,f778,f717]) ).
fof(f782,definition,
! [X0] :
( sQ67_spl
<=> ( in(sK2_skl(X0),X0)
| ~ in(sK3_skl(X0),sK13_skl(powerset(succ(sK0_skl))))
| in(sK2_skl(X0),sK23_skl(sK13_skl(powerset(succ(sK0_skl))),sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f785,definition,
( sQ68_spl
<=> sK20_skl(sK13_skl(powerset(succ(sK0_skl))),sK0_skl) = sK22_skl(sK13_skl(powerset(succ(sK0_skl))),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f788,plain,
( ~ sQ58_spl
| sQ66_spl
| sQ68_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f768,f782,f785,f778,f717]) ).
fof(f789,definition,
! [X0] :
( sQ69_spl
<=> ( in(sK2_skl(X0),X0)
| ~ in(sK3_skl(X0),sK17_skl(powerset(succ(sK0_skl))))
| in(sK2_skl(X0),sK23_skl(sK17_skl(powerset(succ(sK0_skl))),sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f792,definition,
( sQ70_spl
<=> sK20_skl(sK17_skl(powerset(succ(sK0_skl))),sK0_skl) = sK22_skl(sK17_skl(powerset(succ(sK0_skl))),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f795,plain,
( ~ sQ58_spl
| sQ70_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f769,f789,f792,f717]) ).
fof(f796,definition,
! [X0] :
( sQ71_spl
<=> ( in(sK2_skl(X0),X0)
| ~ in(sK3_skl(X0),sK4_skl(powerset(succ(sK0_skl))))
| in(sK2_skl(X0),sK23_skl(sK4_skl(powerset(succ(sK0_skl))),sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f799,definition,
( sQ72_spl
<=> sK20_skl(sK4_skl(powerset(succ(sK0_skl))),sK0_skl) = sK22_skl(sK4_skl(powerset(succ(sK0_skl))),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f802,plain,
( ~ sQ58_spl
| sQ72_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f770,f796,f799,f717]) ).
fof(f803,definition,
! [X0] :
( sQ73_spl
<=> ( in(sK2_skl(X0),X0)
| ~ in(sK3_skl(X0),sK1_skl)
| in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f804,plain,
! [X0] :
( ~ sQ73_spl
| in(sK2_skl(X0),X0)
| ~ in(sK3_skl(X0),sK1_skl)
| in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f803]) ).
fof(f806,plain,
( ~ sQ58_spl
| sQ37_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f771,f803,f499,f717]) ).
fof(f807,plain,
( ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f779,f175]) ).
fof(f808,plain,
~ sQ66_spl,
inference(contradiction_clause,[status(thm)],[f807]) ).
fof(f809,plain,
! [X0] :
( ~ sQ73_spl
| in(sK2_skl(X0),X0)
| in(sK2_skl(X0),sK23_skl(sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f804,f50]) ).
fof(f810,plain,
( sQ47_spl
| ~ sQ73_spl
| in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f809,f555]) ).
fof(f814,plain,
( ~ sQ73_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f810,f553,f803]) ).
fof(f816,plain,
( ~ sQ52_spl
| ~ sQ47_spl
| ~ in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))
| ~ in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f554,f637]) ).
fof(f819,plain,
( ~ sQ52_spl
| ~ sQ48_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f816,f553,f556,f633]) ).
fof(f820,plain,
$false,
inference(sat_refutation,[status(thm)],[f251,f271,f283,f285,f287,f289,f376,f383,f390,f397,f404,f411,f418,f425,f427,f429,f431,f433,f435,f437,f439,f441,f502,f515,f516,f520,f522,f572,f610,f631,f636,f641,f643,f652,f656,f682,f687,f698,f702,f709,f720,f728,f758,f763,f781,f788,f795,f802,f806,f808,f814,f819]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU298+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.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:09:05 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.41 % Refutation found
% 0.10/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.44 % Elapsed time: 0.069673 seconds
% 0.10/0.44 % CPU time: 0.268727 seconds
% 0.10/0.44 % Total memory used: 88.365 MB
% 0.10/0.44 % Net memory used: 88.167 MB
%------------------------------------------------------------------------------