%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU301+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n017.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 : Fri Sep 25 02:56:33 PM UTC 2026
% Result : Theorem 112.13s 18.24s
% Output : CNFRefutation 112.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 23
% Syntax : Number of formulae : 311 ( 34 unt; 4 def)
% Number of atoms : 1695 ( 368 equ)
% Maximal formula atoms : 49 ( 5 avg)
% Number of connectives : 2293 ( 909 ~; 974 |; 290 &)
% ( 0 <=>; 120 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 7 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 14 usr; 2 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 6 con; 0-2 aty)
% Number of variables : 618 ( 0 sgn 541 !; 77 ?; 233 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ! [X3] :
( ordinal(X3)
=> ( ( ! [X10] :
( ordinal(X10)
=> ( in(X10,X3)
=> ( in(X10,omega)
=> ! [X11] :
( element(X11,powerset(powerset(X10)))
=> ~ ( ! [X12] :
~ ( ! [X13] :
( ( subset(X12,X13)
& in(X13,X11) )
=> X13 = X12 )
& in(X12,X11) )
& X11 != empty_set ) ) ) ) )
& being_limit_ordinal(X3) )
=> ( ( in(X3,omega)
=> ! [X14] :
( element(X14,powerset(powerset(X3)))
=> ~ ( ! [X15] :
~ ( ! [X16] :
( ( subset(X15,X16)
& in(X16,X14) )
=> X16 = X15 )
& in(X15,X14) )
& X14 != empty_set ) ) )
| X3 = empty_set ) ) )
& ! [X3] :
( ordinal(X3)
=> ( ( in(X3,omega)
=> ! [X4] :
( element(X4,powerset(powerset(X3)))
=> ~ ( ! [X5] :
~ ( ! [X6] :
( ( subset(X5,X6)
& in(X6,X4) )
=> X6 = X5 )
& in(X5,X4) )
& X4 != empty_set ) ) )
=> ( in(succ(X3),omega)
=> ! [X7] :
( element(X7,powerset(powerset(succ(X3))))
=> ~ ( ! [X8] :
~ ( ! [X9] :
( ( subset(X8,X9)
& in(X9,X7) )
=> X9 = X8 )
& in(X8,X7) )
& X7 != empty_set ) ) ) ) )
& ( in(empty_set,omega)
=> ! [X0] :
( element(X0,powerset(powerset(empty_set)))
=> ~ ( ! [X1] :
~ ( ! [X2] :
( ( subset(X1,X2)
& in(X2,X0) )
=> X2 = X1 )
& in(X1,X0) )
& X0 != empty_set ) ) ) )
=> ! [X3] :
( ordinal(X3)
=> ( in(X3,omega)
=> ! [X17] :
( element(X17,powerset(powerset(X3)))
=> ~ ( ! [X18] :
~ ( ! [X19] :
( ( subset(X18,X19)
& in(X19,X17) )
=> X19 = X18 )
& in(X18,X17) )
& X17 != empty_set ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_ordinal2__e18_27__finset_1) ).
fof(f2,negated_conjecture,
~ ( ( ! [X3] :
( ordinal(X3)
=> ( ( ! [X10] :
( ordinal(X10)
=> ( in(X10,X3)
=> ( in(X10,omega)
=> ! [X11] :
( element(X11,powerset(powerset(X10)))
=> ~ ( ! [X12] :
~ ( ! [X13] :
( ( subset(X12,X13)
& in(X13,X11) )
=> X13 = X12 )
& in(X12,X11) )
& X11 != empty_set ) ) ) ) )
& being_limit_ordinal(X3) )
=> ( ( in(X3,omega)
=> ! [X14] :
( element(X14,powerset(powerset(X3)))
=> ~ ( ! [X15] :
~ ( ! [X16] :
( ( subset(X15,X16)
& in(X16,X14) )
=> X16 = X15 )
& in(X15,X14) )
& X14 != empty_set ) ) )
| X3 = empty_set ) ) )
& ! [X3] :
( ordinal(X3)
=> ( ( in(X3,omega)
=> ! [X4] :
( element(X4,powerset(powerset(X3)))
=> ~ ( ! [X5] :
~ ( ! [X6] :
( ( subset(X5,X6)
& in(X6,X4) )
=> X6 = X5 )
& in(X5,X4) )
& X4 != empty_set ) ) )
=> ( in(succ(X3),omega)
=> ! [X7] :
( element(X7,powerset(powerset(succ(X3))))
=> ~ ( ! [X8] :
~ ( ! [X9] :
( ( subset(X8,X9)
& in(X9,X7) )
=> X9 = X8 )
& in(X8,X7) )
& X7 != empty_set ) ) ) ) )
& ( in(empty_set,omega)
=> ! [X0] :
( element(X0,powerset(powerset(empty_set)))
=> ~ ( ! [X1] :
~ ( ! [X2] :
( ( subset(X1,X2)
& in(X2,X0) )
=> X2 = X1 )
& in(X1,X0) )
& X0 != empty_set ) ) ) )
=> ! [X3] :
( ordinal(X3)
=> ( in(X3,omega)
=> ! [X17] :
( element(X17,powerset(powerset(X3)))
=> ~ ( ! [X18] :
~ ( ! [X19] :
( ( subset(X18,X19)
& in(X19,X17) )
=> X19 = X18 )
& in(X18,X17) )
& X17 != empty_set ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f15,axiom,
? [X0] :
( relation(X0)
& empty(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_relat_1) ).
fof(f22,axiom,
! [X0] :
( ( epsilon_connected(X0)
& epsilon_transitive(X0) )
=> ordinal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_ordinal1) ).
fof(f27,axiom,
! [X0] :
( ~ empty(X0)
=> ? [X1] :
( ~ empty(X1)
& element(X1,powerset(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_subset_1) ).
fof(f41,axiom,
! [X0] :
( ordinal(X0)
=> ! [X1] :
( element(X1,X0)
=> ( ordinal(X1)
& epsilon_connected(X1)
& epsilon_transitive(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_arytm_3) ).
fof(f42,axiom,
! [X0] :
( element(X0,omega)
=> ( natural(X0)
& ordinal(X0)
& epsilon_connected(X0)
& epsilon_transitive(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc3_arytm_3) ).
fof(f47,axiom,
! [X0] : ~ empty(powerset(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f48,axiom,
empty(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f49,axiom,
( ! [X0] :
( ordinal(X0)
=> ( ! [X1] :
( ordinal(X1)
=> ( in(X1,X0)
=> ( in(X1,omega)
=> ! [X2] :
( element(X2,powerset(powerset(X1)))
=> ~ ( ! [X3] :
~ ( ! [X4] :
( ( subset(X3,X4)
& in(X4,X2) )
=> X4 = X3 )
& in(X3,X2) )
& X2 != empty_set ) ) ) ) )
=> ( in(X0,omega)
=> ! [X5] :
( element(X5,powerset(powerset(X0)))
=> ~ ( ! [X6] :
~ ( ! [X7] :
( ( subset(X6,X7)
& in(X7,X5) )
=> X7 = X6 )
& in(X6,X5) )
& X5 != empty_set ) ) ) ) )
=> ! [X0] :
( ordinal(X0)
=> ( in(X0,omega)
=> ! [X8] :
( element(X8,powerset(powerset(X0)))
=> ~ ( ! [X9] :
~ ( ! [X10] :
( ( subset(X9,X10)
& in(X10,X8) )
=> X10 = X9 )
& in(X9,X8) )
& X8 != empty_set ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_ordinal1__e18_27__finset_1__1) ).
fof(f51,axiom,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_ordinal1) ).
fof(f59,axiom,
! [X0] : in(X0,succ(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_ordinal1) ).
fof(f61,axiom,
! [X0,X1] :
( in(X0,X1)
=> element(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f62,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( in(X0,X1)
| empty(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f63,axiom,
! [X0] :
( ordinal(X0)
=> ( ~ ( being_limit_ordinal(X0)
& ? [X1] :
( X0 = succ(X1)
& ordinal(X1) ) )
& ~ ( ! [X1] :
( ordinal(X1)
=> X0 != succ(X1) )
& ~ being_limit_ordinal(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t42_ordinal1) ).
fof(f64,axiom,
! [X0] :
( empty(X0)
=> X0 = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(f67,plain,
~ ( ( ! [X10] :
( ordinal(X10)
=> ( ( ! [X11] :
( ordinal(X11)
=> ( in(X11,X10)
=> ( in(X11,omega)
=> ! [X12] :
( element(X12,powerset(powerset(X11)))
=> ~ ( ! [X13] :
~ ( ! [X14] :
( ( subset(X13,X14)
& in(X14,X12) )
=> X13 = X14 )
& in(X13,X12) )
& empty_set != X12 ) ) ) ) )
& being_limit_ordinal(X10) )
=> ( ( in(X10,omega)
=> ! [X15] :
( element(X15,powerset(powerset(X10)))
=> ~ ( ! [X16] :
~ ( ! [X17] :
( ( subset(X16,X17)
& in(X17,X15) )
=> X16 = X17 )
& in(X16,X15) )
& empty_set != X15 ) ) )
| empty_set = X10 ) ) )
& ! [X3] :
( ordinal(X3)
=> ( ( in(X3,omega)
=> ! [X4] :
( element(X4,powerset(powerset(X3)))
=> ~ ( ! [X5] :
~ ( ! [X6] :
( ( subset(X5,X6)
& in(X6,X4) )
=> X6 = X5 )
& in(X5,X4) )
& X4 != empty_set ) ) )
=> ( in(succ(X3),omega)
=> ! [X7] :
( element(X7,powerset(powerset(succ(X3))))
=> ~ ( ! [X8] :
~ ( ! [X9] :
( ( subset(X8,X9)
& in(X9,X7) )
=> X9 = X8 )
& in(X8,X7) )
& X7 != empty_set ) ) ) ) )
& ( in(empty_set,omega)
=> ! [X0] :
( element(X0,powerset(powerset(empty_set)))
=> ~ ( ! [X1] :
~ ( ! [X2] :
( ( subset(X1,X2)
& in(X2,X0) )
=> X2 = X1 )
& in(X1,X0) )
& X0 != empty_set ) ) ) )
=> ! [X18] :
( ordinal(X18)
=> ( in(X18,omega)
=> ! [X19] :
( element(X19,powerset(powerset(X18)))
=> ~ ( ! [X20] :
~ ( ! [X21] :
( ( subset(X20,X21)
& in(X21,X19) )
=> X20 = X21 )
& in(X20,X19) )
& empty_set != X19 ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f69,plain,
( ! [X0] :
( ordinal(X0)
=> ( ! [X1] :
( ordinal(X1)
=> ( in(X1,X0)
=> ( in(X1,omega)
=> ! [X2] :
( element(X2,powerset(powerset(X1)))
=> ~ ( ! [X3] :
~ ( ! [X4] :
( ( subset(X3,X4)
& in(X4,X2) )
=> X4 = X3 )
& in(X3,X2) )
& X2 != empty_set ) ) ) ) )
=> ( in(X0,omega)
=> ! [X5] :
( element(X5,powerset(powerset(X0)))
=> ~ ( ! [X6] :
~ ( ! [X7] :
( ( subset(X6,X7)
& in(X7,X5) )
=> X7 = X6 )
& in(X6,X5) )
& X5 != empty_set ) ) ) ) )
=> ! [X8] :
( ordinal(X8)
=> ( in(X8,omega)
=> ! [X9] :
( element(X9,powerset(powerset(X8)))
=> ~ ( ! [X10] :
~ ( ! [X11] :
( ( subset(X10,X11)
& in(X11,X9) )
=> X10 = X11 )
& in(X10,X9) )
& empty_set != X9 ) ) ) ) ),
inference(rectify,[],[f49]) ).
fof(f71,plain,
! [X0] :
( ordinal(X0)
=> ( ~ ( being_limit_ordinal(X0)
& ? [X2] :
( succ(X2) = X0
& ordinal(X2) ) )
& ~ ( ! [X1] :
( ordinal(X1)
=> X0 != succ(X1) )
& ~ being_limit_ordinal(X0) ) ) ),
inference(rectify,[],[f63]) ).
fof(f81,plain,
( ! [X10] :
( ~ ordinal(X10)
| ? [X11] :
( ordinal(X11)
& in(X11,X10)
& in(X11,omega)
& ? [X12] :
( element(X12,powerset(powerset(X11)))
& ! [X13] :
( ? [X14] :
( subset(X13,X14)
& in(X14,X12)
& X13 != X14 )
| ~ in(X13,X12) )
& empty_set != X12 ) )
| ~ being_limit_ordinal(X10)
| ~ in(X10,omega)
| ! [X15] :
( ~ element(X15,powerset(powerset(X10)))
| ? [X16] :
( ! [X17] :
( ~ subset(X16,X17)
| ~ in(X17,X15)
| X16 = X17 )
& in(X16,X15) )
| empty_set = X15 )
| empty_set = X10 )
& ! [X3] :
( ~ ordinal(X3)
| ( in(X3,omega)
& ? [X4] :
( element(X4,powerset(powerset(X3)))
& ! [X5] :
( ? [X6] :
( subset(X5,X6)
& in(X6,X4)
& X5 != X6 )
| ~ in(X5,X4) )
& X4 != empty_set ) )
| ~ in(succ(X3),omega)
| ! [X7] :
( ~ element(X7,powerset(powerset(succ(X3))))
| ? [X8] :
( ! [X9] :
( ~ subset(X8,X9)
| ~ in(X9,X7)
| X9 = X8 )
& in(X8,X7) )
| empty_set = X7 ) )
& ( ~ in(empty_set,omega)
| ! [X0] :
( ~ element(X0,powerset(powerset(empty_set)))
| ? [X1] :
( ! [X2] :
( ~ subset(X1,X2)
| ~ in(X2,X0)
| X2 = X1 )
& in(X1,X0) )
| empty_set = X0 ) )
& ? [X18] :
( ordinal(X18)
& in(X18,omega)
& ? [X19] :
( element(X19,powerset(powerset(X18)))
& ! [X20] :
( ? [X21] :
( subset(X20,X21)
& in(X21,X19)
& X20 != X21 )
| ~ in(X20,X19) )
& empty_set != X19 ) ) ),
inference(ennf_transformation,[],[f67]) ).
fof(f82,plain,
( ! [X10] :
( ~ ordinal(X10)
| ? [X11] :
( ordinal(X11)
& in(X11,X10)
& in(X11,omega)
& ? [X12] :
( element(X12,powerset(powerset(X11)))
& ! [X13] :
( ? [X14] :
( subset(X13,X14)
& in(X14,X12)
& X13 != X14 )
| ~ in(X13,X12) )
& empty_set != X12 ) )
| ~ being_limit_ordinal(X10)
| ~ in(X10,omega)
| ! [X15] :
( ~ element(X15,powerset(powerset(X10)))
| ? [X16] :
( ! [X17] :
( ~ subset(X16,X17)
| ~ in(X17,X15)
| X16 = X17 )
& in(X16,X15) )
| empty_set = X15 )
| empty_set = X10 )
& ! [X3] :
( ~ ordinal(X3)
| ( in(X3,omega)
& ? [X4] :
( element(X4,powerset(powerset(X3)))
& ! [X5] :
( ? [X6] :
( subset(X5,X6)
& in(X6,X4)
& X5 != X6 )
| ~ in(X5,X4) )
& X4 != empty_set ) )
| ~ in(succ(X3),omega)
| ! [X7] :
( ~ element(X7,powerset(powerset(succ(X3))))
| ? [X8] :
( ! [X9] :
( ~ subset(X8,X9)
| ~ in(X9,X7)
| X9 = X8 )
& in(X8,X7) )
| empty_set = X7 ) )
& ( ~ in(empty_set,omega)
| ! [X0] :
( ~ element(X0,powerset(powerset(empty_set)))
| ? [X1] :
( ! [X2] :
( ~ subset(X1,X2)
| ~ in(X2,X0)
| X2 = X1 )
& in(X1,X0) )
| empty_set = X0 ) )
& ? [X18] :
( ordinal(X18)
& in(X18,omega)
& ? [X19] :
( element(X19,powerset(powerset(X18)))
& ! [X20] :
( ? [X21] :
( subset(X20,X21)
& in(X21,X19)
& X20 != X21 )
| ~ in(X20,X19) )
& empty_set != X19 ) ) ),
inference(flattening,[],[f81]) ).
fof(f94,plain,
! [X0] :
( ~ epsilon_connected(X0)
| ~ epsilon_transitive(X0)
| ordinal(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f95,plain,
! [X0] :
( ~ epsilon_connected(X0)
| ~ epsilon_transitive(X0)
| ordinal(X0) ),
inference(flattening,[],[f94]) ).
fof(f97,plain,
! [X0] :
( empty(X0)
| ? [X1] :
( ~ empty(X1)
& element(X1,powerset(X0)) ) ),
inference(ennf_transformation,[],[f27]) ).
fof(f99,plain,
! [X0] :
( ~ ordinal(X0)
| ! [X1] :
( ~ element(X1,X0)
| ( ordinal(X1)
& epsilon_connected(X1)
& epsilon_transitive(X1) ) ) ),
inference(ennf_transformation,[],[f41]) ).
fof(f100,plain,
! [X0] :
( ~ element(X0,omega)
| ( natural(X0)
& ordinal(X0)
& epsilon_connected(X0)
& epsilon_transitive(X0) ) ),
inference(ennf_transformation,[],[f42]) ).
fof(f103,plain,
( ? [X0] :
( ordinal(X0)
& ! [X1] :
( ~ ordinal(X1)
| ~ in(X1,X0)
| ~ in(X1,omega)
| ! [X2] :
( ~ element(X2,powerset(powerset(X1)))
| ? [X3] :
( ! [X4] :
( ~ subset(X3,X4)
| ~ in(X4,X2)
| X4 = X3 )
& in(X3,X2) )
| empty_set = X2 ) )
& in(X0,omega)
& ? [X5] :
( element(X5,powerset(powerset(X0)))
& ! [X6] :
( ? [X7] :
( subset(X6,X7)
& in(X7,X5)
& X6 != X7 )
| ~ in(X6,X5) )
& X5 != empty_set ) )
| ! [X8] :
( ~ ordinal(X8)
| ~ in(X8,omega)
| ! [X9] :
( ~ element(X9,powerset(powerset(X8)))
| ? [X10] :
( ! [X11] :
( ~ subset(X10,X11)
| ~ in(X11,X9)
| X10 = X11 )
& in(X10,X9) )
| empty_set = X9 ) ) ),
inference(ennf_transformation,[],[f69]) ).
fof(f104,plain,
( ? [X0] :
( ordinal(X0)
& ! [X1] :
( ~ ordinal(X1)
| ~ in(X1,X0)
| ~ in(X1,omega)
| ! [X2] :
( ~ element(X2,powerset(powerset(X1)))
| ? [X3] :
( ! [X4] :
( ~ subset(X3,X4)
| ~ in(X4,X2)
| X4 = X3 )
& in(X3,X2) )
| empty_set = X2 ) )
& in(X0,omega)
& ? [X5] :
( element(X5,powerset(powerset(X0)))
& ! [X6] :
( ? [X7] :
( subset(X6,X7)
& in(X7,X5)
& X6 != X7 )
| ~ in(X6,X5) )
& X5 != empty_set ) )
| ! [X8] :
( ~ ordinal(X8)
| ~ in(X8,omega)
| ! [X9] :
( ~ element(X9,powerset(powerset(X8)))
| ? [X10] :
( ! [X11] :
( ~ subset(X10,X11)
| ~ in(X11,X9)
| X10 = X11 )
& in(X10,X9) )
| empty_set = X9 ) ) ),
inference(flattening,[],[f103]) ).
fof(f107,plain,
! [X0,X1] :
( ~ in(X0,X1)
| element(X0,X1) ),
inference(ennf_transformation,[],[f61]) ).
fof(f108,plain,
! [X0,X1] :
( ~ element(X0,X1)
| in(X0,X1)
| empty(X1) ),
inference(ennf_transformation,[],[f62]) ).
fof(f109,plain,
! [X0,X1] :
( ~ element(X0,X1)
| in(X0,X1)
| empty(X1) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0] :
( ~ ordinal(X0)
| ( ( ~ being_limit_ordinal(X0)
| ! [X2] :
( succ(X2) != X0
| ~ ordinal(X2) ) )
& ( ? [X1] :
( ordinal(X1)
& succ(X1) = X0 )
| being_limit_ordinal(X0) ) ) ),
inference(ennf_transformation,[],[f71]) ).
fof(f111,plain,
! [X0] :
( ~ empty(X0)
| X0 = empty_set ),
inference(ennf_transformation,[],[f64]) ).
fof(f120,plain,
! [X3] :
( ~ sP1(X3)
| ( in(X3,omega)
& ? [X4] :
( element(X4,powerset(powerset(X3)))
& ! [X5] :
( ? [X6] :
( subset(X5,X6)
& in(X6,X4)
& X5 != X6 )
| ~ in(X5,X4) )
& X4 != empty_set ) ) ),
inference(nnf_transformation,[],[f115]) ).
fof(f121,plain,
! [X0] :
( ~ sP1(X0)
| ( in(X0,omega)
& ? [X1] :
( element(X1,powerset(powerset(X0)))
& ! [X2] :
( ? [X3] :
( subset(X2,X3)
& in(X3,X1)
& X2 != X3 )
| ~ in(X2,X1) )
& empty_set != X1 ) ) ),
inference(rectify,[],[f120]) ).
fof(f122,plain,
! [X0] :
( ~ sP1(X0)
| ( in(X0,omega)
& element(sK4(X0),powerset(powerset(X0)))
& ! [X2] :
( ( subset(X2,sK5(X0,X2))
& in(sK5(X0,X2),sK4(X0))
& sK5(X0,X2) != X2 )
| ~ in(X2,sK4(X0)) )
& empty_set != sK4(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X1,sK4(X0)),skolemize(X3,sK5(X0,X2))],[f121]) ).
fof(f126,plain,
( ! [X11] :
( ~ ordinal(X11)
| sP0(X11)
| ~ being_limit_ordinal(X11)
| ~ in(X11,omega)
| ! [X12] :
( ~ element(X12,powerset(powerset(X11)))
| ? [X13] :
( ! [X14] :
( ~ subset(X13,X14)
| ~ in(X14,X12)
| X13 = X14 )
& in(X13,X12) )
| empty_set = X12 )
| empty_set = X11 )
& ! [X7] :
( ~ ordinal(X7)
| sP1(X7)
| ~ in(succ(X7),omega)
| ! [X8] :
( ~ element(X8,powerset(powerset(succ(X7))))
| ? [X9] :
( ! [X10] :
( ~ subset(X9,X10)
| ~ in(X10,X8)
| X9 = X10 )
& in(X9,X8) )
| empty_set = X8 ) )
& ( ~ in(empty_set,omega)
| ! [X4] :
( ~ element(X4,powerset(powerset(empty_set)))
| ? [X5] :
( ! [X6] :
( ~ subset(X5,X6)
| ~ in(X6,X4)
| X5 = X6 )
& in(X5,X4) )
| empty_set = X4 ) )
& ? [X0] :
( ordinal(X0)
& in(X0,omega)
& ? [X1] :
( element(X1,powerset(powerset(X0)))
& ! [X2] :
( ? [X3] :
( subset(X2,X3)
& in(X3,X1)
& X2 != X3 )
| ~ in(X2,X1) )
& empty_set != X1 ) ) ),
inference(rectify,[],[f116]) ).
fof(f127,plain,
( ! [X11] :
( ~ ordinal(X11)
| sP0(X11)
| ~ being_limit_ordinal(X11)
| ~ in(X11,omega)
| ! [X12] :
( ~ element(X12,powerset(powerset(X11)))
| ( ! [X14] :
( ~ subset(sK14(X12),X14)
| ~ in(X14,X12)
| sK14(X12) = X14 )
& in(sK14(X12),X12) )
| empty_set = X12 )
| empty_set = X11 )
& ! [X7] :
( ~ ordinal(X7)
| sP1(X7)
| ~ in(succ(X7),omega)
| ! [X8] :
( ~ element(X8,powerset(powerset(succ(X7))))
| ( ! [X10] :
( ~ subset(sK13(X8),X10)
| ~ in(X10,X8)
| sK13(X8) = X10 )
& in(sK13(X8),X8) )
| empty_set = X8 ) )
& ( ~ in(empty_set,omega)
| ! [X4] :
( ~ element(X4,powerset(powerset(empty_set)))
| ( ! [X6] :
( ~ subset(sK12(X4),X6)
| ~ in(X6,X4)
| sK12(X4) = X6 )
& in(sK12(X4),X4) )
| empty_set = X4 ) )
& ordinal(sK9)
& in(sK9,omega)
& element(sK10,powerset(powerset(sK9)))
& ! [X2] :
( ( subset(X2,sK11(X2))
& in(sK11(X2),sK10)
& sK11(X2) != X2 )
| ~ in(X2,sK10) )
& empty_set != sK10 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11,sK12,sK13,sK14]),skolemize(X0,sK9),skolemize(X1,sK10),skolemize(X3,sK11(X2)),skolemize(X5,sK12(X4)),skolemize(X9,sK13(X8)),skolemize(X13,sK14(X12))],[f126]) ).
fof(f136,plain,
( relation(sK23)
& empty(sK23) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(X0,sK23)],[f15]) ).
fof(f143,plain,
! [X0] :
( empty(X0)
| ( ~ empty(sK30(X0))
& element(sK30(X0),powerset(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(X1,sK30(X0))],[f97]) ).
fof(f147,plain,
( ~ sP3
| ? [X0] :
( ordinal(X0)
& ! [X1] :
( ~ ordinal(X1)
| ~ in(X1,X0)
| ~ in(X1,omega)
| ! [X2] :
( ~ element(X2,powerset(powerset(X1)))
| ? [X3] :
( ! [X4] :
( ~ subset(X3,X4)
| ~ in(X4,X2)
| X4 = X3 )
& in(X3,X2) )
| empty_set = X2 ) )
& in(X0,omega)
& sP2(X0) ) ),
inference(nnf_transformation,[],[f118]) ).
fof(f148,plain,
( ~ sP3
| ( ordinal(sK34)
& ! [X1] :
( ~ ordinal(X1)
| ~ in(X1,sK34)
| ~ in(X1,omega)
| ! [X2] :
( ~ element(X2,powerset(powerset(X1)))
| ( ! [X4] :
( ~ subset(sK35(X2),X4)
| ~ in(X4,X2)
| sK35(X2) = X4 )
& in(sK35(X2),X2) )
| empty_set = X2 ) )
& in(sK34,omega)
& sP2(sK34) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34,sK35]),skolemize(X0,sK34),skolemize(X3,sK35(X2))],[f147]) ).
fof(f152,plain,
( sP3
| ! [X0] :
( ~ ordinal(X0)
| ~ in(X0,omega)
| ! [X1] :
( ~ element(X1,powerset(powerset(X0)))
| ? [X2] :
( ! [X3] :
( ~ subset(X2,X3)
| ~ in(X3,X1)
| X2 = X3 )
& in(X2,X1) )
| empty_set = X1 ) ) ),
inference(rectify,[],[f119]) ).
fof(f153,plain,
( sP3
| ! [X0] :
( ~ ordinal(X0)
| ~ in(X0,omega)
| ! [X1] :
( ~ element(X1,powerset(powerset(X0)))
| ( ! [X3] :
( ~ subset(sK38(X1),X3)
| ~ in(X3,X1)
| sK38(X1) = X3 )
& in(sK38(X1),X1) )
| empty_set = X1 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(X2,sK38(X1))],[f152]) ).
fof(f155,plain,
! [X0] :
( ~ ordinal(X0)
| ( ( ~ being_limit_ordinal(X0)
| ! [X2] :
( succ(X2) != X0
| ~ ordinal(X2) ) )
& ( ( ordinal(sK40(X0))
& succ(sK40(X0)) = X0 )
| being_limit_ordinal(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(X1,sK40(X0))],[f110]) ).
fof(f156,plain,
! [X0] :
( ~ sP1(X0)
| in(X0,omega) ),
inference(cnf_transformation,[],[f122]) ).
fof(f157,plain,
! [X0] :
( ~ sP1(X0)
| element(sK4(X0),powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f122]) ).
fof(f158,plain,
! [X2,X0] :
( ~ sP1(X0)
| subset(X2,sK5(X0,X2))
| ~ in(X2,sK4(X0)) ),
inference(cnf_transformation,[],[f122]) ).
fof(f159,plain,
! [X2,X0] :
( ~ sP1(X0)
| in(sK5(X0,X2),sK4(X0))
| ~ in(X2,sK4(X0)) ),
inference(cnf_transformation,[],[f122]) ).
fof(f160,plain,
! [X2,X0] :
( ~ sP1(X0)
| sK5(X0,X2) != X2
| ~ in(X2,sK4(X0)) ),
inference(cnf_transformation,[],[f122]) ).
fof(f161,plain,
! [X0] :
( ~ sP1(X0)
| empty_set != sK4(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f170,plain,
! [X11,X14,X12] :
( ~ ordinal(X11)
| sP0(X11)
| ~ being_limit_ordinal(X11)
| ~ in(X11,omega)
| ~ element(X12,powerset(powerset(X11)))
| ~ subset(sK14(X12),X14)
| ~ in(X14,X12)
| sK14(X12) = X14
| empty_set = X12
| empty_set = X11 ),
inference(cnf_transformation,[],[f127]) ).
fof(f171,plain,
! [X11,X12] :
( ~ ordinal(X11)
| sP0(X11)
| ~ being_limit_ordinal(X11)
| ~ in(X11,omega)
| ~ element(X12,powerset(powerset(X11)))
| in(sK14(X12),X12)
| empty_set = X12
| empty_set = X11 ),
inference(cnf_transformation,[],[f127]) ).
fof(f172,plain,
! [X10,X8,X7] :
( ~ ordinal(X7)
| sP1(X7)
| ~ in(succ(X7),omega)
| ~ element(X8,powerset(powerset(succ(X7))))
| ~ subset(sK13(X8),X10)
| ~ in(X10,X8)
| sK13(X8) = X10
| empty_set = X8 ),
inference(cnf_transformation,[],[f127]) ).
fof(f173,plain,
! [X8,X7] :
( ~ ordinal(X7)
| sP1(X7)
| ~ in(succ(X7),omega)
| ~ element(X8,powerset(powerset(succ(X7))))
| in(sK13(X8),X8)
| empty_set = X8 ),
inference(cnf_transformation,[],[f127]) ).
fof(f174,plain,
! [X6,X4] :
( ~ in(empty_set,omega)
| ~ element(X4,powerset(powerset(empty_set)))
| ~ subset(sK12(X4),X6)
| ~ in(X6,X4)
| sK12(X4) = X6
| empty_set = X4 ),
inference(cnf_transformation,[],[f127]) ).
fof(f175,plain,
! [X4] :
( ~ in(empty_set,omega)
| ~ element(X4,powerset(powerset(empty_set)))
| in(sK12(X4),X4)
| empty_set = X4 ),
inference(cnf_transformation,[],[f127]) ).
fof(f176,plain,
ordinal(sK9),
inference(cnf_transformation,[],[f127]) ).
fof(f177,plain,
in(sK9,omega),
inference(cnf_transformation,[],[f127]) ).
fof(f178,plain,
element(sK10,powerset(powerset(sK9))),
inference(cnf_transformation,[],[f127]) ).
fof(f179,plain,
! [X2] :
( subset(X2,sK11(X2))
| ~ in(X2,sK10) ),
inference(cnf_transformation,[],[f127]) ).
fof(f180,plain,
! [X2] :
( in(sK11(X2),sK10)
| ~ in(X2,sK10) ),
inference(cnf_transformation,[],[f127]) ).
fof(f181,plain,
! [X2] :
( sK11(X2) != X2
| ~ in(X2,sK10) ),
inference(cnf_transformation,[],[f127]) ).
fof(f182,plain,
empty_set != sK10,
inference(cnf_transformation,[],[f127]) ).
fof(f216,plain,
empty(sK23),
inference(cnf_transformation,[],[f136]) ).
fof(f235,plain,
! [X0] :
( ~ epsilon_connected(X0)
| ~ epsilon_transitive(X0)
| ordinal(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f252,plain,
! [X0] :
( empty(X0)
| ~ empty(sK30(X0)) ),
inference(cnf_transformation,[],[f143]) ).
fof(f253,plain,
! [X0] :
( empty(X0)
| element(sK30(X0),powerset(X0)) ),
inference(cnf_transformation,[],[f143]) ).
fof(f268,plain,
! [X0,X1] :
( ~ ordinal(X0)
| ~ element(X1,X0)
| ordinal(X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f270,plain,
! [X0,X1] :
( ~ ordinal(X0)
| ~ element(X1,X0)
| epsilon_transitive(X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f272,plain,
! [X0] :
( ~ element(X0,omega)
| ordinal(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f288,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[],[f47]) ).
fof(f289,plain,
empty(empty_set),
inference(cnf_transformation,[],[f48]) ).
fof(f290,plain,
( ~ sP3
| ordinal(sK34) ),
inference(cnf_transformation,[],[f148]) ).
fof(f291,plain,
! [X2,X1,X4] :
( ~ sP3
| ~ ordinal(X1)
| ~ in(X1,sK34)
| ~ in(X1,omega)
| ~ element(X2,powerset(powerset(X1)))
| ~ subset(sK35(X2),X4)
| ~ in(X4,X2)
| sK35(X2) = X4
| empty_set = X2 ),
inference(cnf_transformation,[],[f148]) ).
fof(f292,plain,
! [X2,X1] :
( ~ sP3
| ~ ordinal(X1)
| ~ in(X1,sK34)
| ~ in(X1,omega)
| ~ element(X2,powerset(powerset(X1)))
| in(sK35(X2),X2)
| empty_set = X2 ),
inference(cnf_transformation,[],[f148]) ).
fof(f293,plain,
( ~ sP3
| in(sK34,omega) ),
inference(cnf_transformation,[],[f148]) ).
fof(f294,plain,
( ~ sP3
| sP2(sK34) ),
inference(cnf_transformation,[],[f148]) ).
fof(f300,plain,
! [X3,X0,X1] :
( sP3
| ~ ordinal(X0)
| ~ in(X0,omega)
| ~ element(X1,powerset(powerset(X0)))
| ~ subset(sK38(X1),X3)
| ~ in(X3,X1)
| sK38(X1) = X3
| empty_set = X1 ),
inference(cnf_transformation,[],[f153]) ).
fof(f301,plain,
! [X0,X1] :
( sP3
| ~ ordinal(X0)
| ~ in(X0,omega)
| ~ element(X1,powerset(powerset(X0)))
| in(sK38(X1),X1)
| empty_set = X1 ),
inference(cnf_transformation,[],[f153]) ).
fof(f303,plain,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
inference(cnf_transformation,[],[f51]) ).
fof(f309,plain,
! [X0] : in(X0,succ(X0)),
inference(cnf_transformation,[],[f59]) ).
fof(f311,plain,
! [X0,X1] :
( ~ in(X0,X1)
| element(X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f312,plain,
! [X0,X1] :
( ~ element(X0,X1)
| in(X0,X1)
| empty(X1) ),
inference(cnf_transformation,[],[f109]) ).
fof(f315,plain,
! [X0] :
( ~ ordinal(X0)
| succ(sK40(X0)) = X0
| being_limit_ordinal(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f316,plain,
! [X0] :
( ~ empty(X0)
| empty_set = X0 ),
inference(cnf_transformation,[],[f111]) ).
fof(f319,plain,
! [X8,X7] :
( ~ ordinal(X7)
| sP1(X7)
| ~ in(set_union2(X7,singleton(X7)),omega)
| ~ element(X8,powerset(powerset(set_union2(X7,singleton(X7)))))
| in(sK13(X8),X8)
| empty_set = X8 ),
inference(definition_unfolding,[],[f173,f303,f303]) ).
fof(f320,plain,
! [X10,X8,X7] :
( ~ ordinal(X7)
| sP1(X7)
| ~ in(set_union2(X7,singleton(X7)),omega)
| ~ element(X8,powerset(powerset(set_union2(X7,singleton(X7)))))
| ~ subset(sK13(X8),X10)
| ~ in(X10,X8)
| sK13(X8) = X10
| empty_set = X8 ),
inference(definition_unfolding,[],[f172,f303,f303]) ).
fof(f331,plain,
! [X0] : in(X0,set_union2(X0,singleton(X0))),
inference(definition_unfolding,[],[f309,f303]) ).
fof(f332,plain,
! [X0] :
( ~ ordinal(X0)
| set_union2(sK40(X0),singleton(sK40(X0))) = X0
| being_limit_ordinal(X0) ),
inference(definition_unfolding,[],[f315,f303]) ).
tcf(c_49,plain,
! [X0: $i] :
( ~ sP1(X0)
| ( sK4(X0) != empty_set ) ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i] :
( ~ sP1(X0)
| ~ in(X1,sK4(X0))
| ( sK5(X0,X1) != X1 ) ),
inference(cnf_transformation,[],[f160]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i] :
( in(sK5(X1,X0),sK4(X1))
| ~ sP1(X1)
| ~ in(X0,sK4(X1)) ),
inference(cnf_transformation,[],[f159]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( subset(X0,sK5(X1,X0))
| ~ sP1(X1)
| ~ in(X0,sK4(X1)) ),
inference(cnf_transformation,[],[f158]) ).
tcf(c_53,plain,
! [X0: $i] :
( element(sK4(X0),powerset(powerset(X0)))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f157]) ).
tcf(c_54,plain,
! [X0: $i] :
( in(X0,omega)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f156]) ).
tcf(c_63,negated_conjecture,
empty_set != sK10,
inference(cnf_transformation,[],[f182]) ).
tcf(c_64,negated_conjecture,
! [X0: $i] :
( ~ in(X0,sK10)
| ( sK11(X0) != X0 ) ),
inference(cnf_transformation,[],[f181]) ).
tcf(c_65,negated_conjecture,
! [X0: $i] :
( in(sK11(X0),sK10)
| ~ in(X0,sK10) ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_66,negated_conjecture,
! [X0: $i] :
( subset(X0,sK11(X0))
| ~ in(X0,sK10) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_67,negated_conjecture,
element(sK10,powerset(powerset(sK9))),
inference(cnf_transformation,[],[f178]) ).
tcf(c_68,negated_conjecture,
in(sK9,omega),
inference(cnf_transformation,[],[f177]) ).
tcf(c_69,negated_conjecture,
ordinal(sK9),
inference(cnf_transformation,[],[f176]) ).
tcf(c_70,negated_conjecture,
! [X0: $i] :
( in(sK12(X0),X0)
| ( X0 = empty_set )
| ~ in(empty_set,omega)
| ~ element(X0,powerset(powerset(empty_set))) ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_71,negated_conjecture,
! [X0: $i,X1: $i] :
( ( X0 = empty_set )
| ( sK12(X0) = X1 )
| ~ in(empty_set,omega)
| ~ in(X1,X0)
| ~ subset(sK12(X0),X1)
| ~ element(X0,powerset(powerset(empty_set))) ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_72,negated_conjecture,
! [X0: $i,X1: $i] :
( sP1(X1)
| in(sK13(X0),X0)
| ( X0 = empty_set )
| ~ ordinal(X1)
| ~ in(set_union2(X1,singleton(X1)),omega)
| ~ element(X0,powerset(powerset(set_union2(X1,singleton(X1))))) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_73,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1)
| ( X0 = empty_set )
| ( sK13(X0) = X2 )
| ~ ordinal(X1)
| ~ in(X2,X0)
| ~ subset(sK13(X0),X2)
| ~ in(set_union2(X1,singleton(X1)),omega)
| ~ element(X0,powerset(powerset(set_union2(X1,singleton(X1))))) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_74,negated_conjecture,
! [X0: $i,X1: $i] :
( sP0(X1)
| in(sK14(X0),X0)
| ( X1 = empty_set )
| ( X0 = empty_set )
| ~ being_limit_ordinal(X1)
| ~ ordinal(X1)
| ~ in(X1,omega)
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[],[f171]) ).
tcf(c_75,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X1)
| ( X1 = empty_set )
| ( X0 = empty_set )
| ( sK14(X0) = X2 )
| ~ being_limit_ordinal(X1)
| ~ ordinal(X1)
| ~ in(X1,omega)
| ~ in(X2,X0)
| ~ subset(sK14(X0),X2)
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[],[f170]) ).
tcf(c_106,plain,
empty(sK23),
inference(cnf_transformation,[],[f216]) ).
tcf(c_125,plain,
! [X0: $i] :
( ordinal(X0)
| ~ epsilon_connected(X0)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_142,plain,
! [X0: $i] :
( empty(X0)
| element(sK30(X0),powerset(X0)) ),
inference(cnf_transformation,[],[f253]) ).
tcf(c_143,plain,
! [X0: $i] :
( empty(X0)
| ~ empty(sK30(X0)) ),
inference(cnf_transformation,[],[f252]) ).
tcf(c_158,plain,
! [X0: $i,X1: $i] :
( epsilon_transitive(X0)
| ~ ordinal(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[],[f270]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i] :
( ordinal(X0)
| ~ ordinal(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[],[f268]) ).
tcf(c_163,plain,
! [X0: $i] :
( ordinal(X0)
| ~ element(X0,omega) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_178,plain,
! [X0: $i] : ~ empty(powerset(X0)),
inference(cnf_transformation,[],[f288]) ).
tcf(c_179,plain,
empty(empty_set),
inference(cnf_transformation,[],[f289]) ).
tcf(c_180,plain,
( sP2(sK34)
| ~ sP3 ),
inference(cnf_transformation,[],[f294]) ).
tcf(c_181,plain,
( in(sK34,omega)
| ~ sP3 ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i] :
( in(sK35(X0),X0)
| ( X0 = empty_set )
| ~ sP3
| ~ ordinal(X1)
| ~ in(X1,sK34)
| ~ in(X1,omega)
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_183,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = empty_set )
| ( sK35(X0) = X2 )
| ~ sP3
| ~ ordinal(X1)
| ~ in(X1,sK34)
| ~ in(X1,omega)
| ~ in(X2,X0)
| ~ subset(sK35(X0),X2)
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_184,plain,
( ordinal(sK34)
| ~ sP3 ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_190,plain,
! [X0: $i,X1: $i] :
( sP3
| in(sK38(X0),X0)
| ( X0 = empty_set )
| ~ ordinal(X1)
| ~ in(X1,omega)
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[],[f301]) ).
tcf(c_191,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP3
| ( X0 = empty_set )
| ( sK38(X0) = X2 )
| ~ ordinal(X1)
| ~ in(X1,omega)
| ~ in(X2,X0)
| ~ subset(sK38(X0),X2)
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_198,plain,
! [X0: $i] : in(X0,set_union2(X0,singleton(X0))),
inference(cnf_transformation,[],[f331]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_202,plain,
! [X0: $i] :
( being_limit_ordinal(X0)
| ( set_union2(sK40(X0),singleton(sK40(X0))) = X0 )
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f332]) ).
tcf(c_205,plain,
! [X0: $i] :
( ( X0 = empty_set )
| ~ empty(X0) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_231,plain,
( ( empty_set = empty_set )
| ~ empty(empty_set) ),
inference(instantiation,[status(thm)],[c_205]) ).
tcf(c_325,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_327,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_336,plain,
! [X0: $i,X1: $i] :
( empty(X0)
| ~ empty(X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_339,plain,
! [X0: $i,X1: $i] :
( sP2(X0)
| ~ sP2(X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_479,plain,
! [X0: $i] :
( ( empty_set = sK10 )
| ( sK10 != X0 )
| ( empty_set != X0 ) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_480,plain,
( ( empty_set = sK10 )
| ( sK10 != empty_set )
| ( empty_set != empty_set ) ),
inference(instantiation,[status(thm)],[c_479]) ).
tcf(c_594,plain,
! [X0: $i] :
( sP3
| in(sK38(sK10),sK10)
| ( sK10 = empty_set )
| ~ ordinal(X0)
| ~ in(X0,omega)
| ~ element(sK10,powerset(powerset(X0))) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_1108,plain,
! [X0: $i] :
( element(X0,omega)
| ~ sP1(X0) ),
inference(superposition,[status(thm)],[c_54,c_200]) ).
tcf(c_1111,plain,
! [X0: $i] : element(X0,set_union2(X0,singleton(X0))),
inference(superposition,[status(thm)],[c_198,c_200]) ).
tcf(c_1266,plain,
! [X0: $i] :
( empty(powerset(X0))
| ~ empty(sK30(powerset(X0))) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_1519,plain,
empty_set = sK23,
inference(superposition,[status(thm)],[c_106,c_205]) ).
tcf(c_1548,plain,
! [X0: $i,X1: $i] :
( ( X0 = empty_set )
| ( sK12(X0) = X1 )
| ~ in(empty_set,omega)
| ~ in(X1,X0)
| ~ subset(sK12(X0),X1)
| ~ element(X0,powerset(powerset(sK23))) ),
inference(superposition,[status(thm)],[c_1519,c_71]) ).
tcf(c_1549,plain,
! [X0: $i] :
( in(sK12(X0),X0)
| ( X0 = empty_set )
| ~ in(empty_set,omega)
| ~ element(X0,powerset(powerset(sK23))) ),
inference(superposition,[status(thm)],[c_1519,c_70]) ).
tcf(c_1553,plain,
! [X0: $i] :
( in(sK12(X0),X0)
| ( X0 = sK23 )
| ~ in(sK23,omega)
| ~ element(X0,powerset(powerset(sK23))) ),
inference(demodulation,[status(thm)],[c_1549,c_1519]) ).
tcf(c_1558,plain,
! [X0: $i,X1: $i] :
( ( X0 = sK23 )
| ( sK12(X0) = X1 )
| ~ in(sK23,omega)
| ~ in(X1,X0)
| ~ subset(sK12(X0),X1)
| ~ element(X0,powerset(powerset(sK23))) ),
inference(demodulation,[status(thm)],[c_1548,c_1519]) ).
tcf(c_1959,plain,
( sP3
| in(sK38(sK10),sK10)
| ( sK10 = empty_set )
| ~ ordinal(sK9)
| ~ in(sK9,omega)
| ~ element(sK10,powerset(powerset(sK9))) ),
inference(instantiation,[status(thm)],[c_594]) ).
tcf(c_2299,plain,
! [X0: $i] :
( ordinal(X0)
| ~ sP1(X0) ),
inference(superposition,[status(thm)],[c_1108,c_163]) ).
tcf(c_2330,plain,
! [X0: $i] :
( ordinal(X0)
| ~ ordinal(set_union2(X0,singleton(X0))) ),
inference(superposition,[status(thm)],[c_1111,c_160]) ).
tcf(c_3926,plain,
! [X0: $i] :
( ordinal(X0)
| ~ in(X0,omega) ),
inference(resolution,[status(thm)],[c_200,c_163]) ).
tcf(c_4471,plain,
! [X0: $i] :
( sP2(X0)
| ~ sP2(sK34)
| ( X0 != sK34 ) ),
inference(instantiation,[status(thm)],[c_339]) ).
tcf(c_4690,plain,
! [X0: $i,X1: $i] :
( sP3
| in(sK38(X0),X0)
| ( X0 = empty_set )
| ~ in(X1,omega)
| ~ element(X0,powerset(powerset(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_190,c_3926]) ).
tcf(c_4691,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP3
| ( X0 = empty_set )
| ( sK38(X0) = X2 )
| ~ in(X1,omega)
| ~ in(X2,X0)
| ~ subset(sK38(X0),X2)
| ~ element(X0,powerset(powerset(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_191,c_3926]) ).
tcf(c_4693,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = empty_set )
| ( sK35(X0) = X2 )
| ~ sP3
| ~ in(X1,sK34)
| ~ in(X1,omega)
| ~ in(X2,X0)
| ~ subset(sK35(X0),X2)
| ~ element(X0,powerset(powerset(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_183,c_3926]) ).
tcf(c_8541,plain,
( subset(sK38(sK10),sK11(sK38(sK10)))
| ~ in(sK38(sK10),sK10) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_8543,plain,
( in(sK11(sK38(sK10)),sK10)
| ~ in(sK38(sK10),sK10) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_12901,plain,
( sP2(set_union2(sK40(sK34),singleton(sK40(sK34))))
| ~ sP2(sK34)
| ( set_union2(sK40(sK34),singleton(sK40(sK34))) != sK34 ) ),
inference(instantiation,[status(thm)],[c_4471]) ).
tcf(c_13300,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_327,c_325]) ).
tcf(c_13391,plain,
! [X0: $i,X1: $i] :
( sP3
| in(sK38(X0),X0)
| ( X0 = sK23 )
| ~ ordinal(X1)
| ~ in(X1,omega)
| ~ element(X0,powerset(powerset(X1))) ),
inference(demodulation,[status(thm)],[c_190,c_1519]) ).
tcf(c_13392,plain,
! [X0: $i] :
( sP3
| in(sK38(sK4(X0)),sK4(X0))
| ( sK4(X0) = sK23 )
| ~ ordinal(X0)
| ~ sP1(X0)
| ~ in(X0,omega) ),
inference(superposition,[status(thm)],[c_53,c_13391]) ).
tcf(c_13394,plain,
( sP3
| in(sK38(sK10),sK10)
| ( sK10 = sK23 )
| ~ ordinal(sK9)
| ~ in(sK9,omega) ),
inference(superposition,[status(thm)],[c_67,c_13391]) ).
tcf(c_13396,plain,
( sP3
| in(sK38(sK10),sK10) ),
inference(global_subsumption_just,[status(thm)],[c_13394,c_69,c_179,c_68,c_67,c_63,c_231,c_480,c_1959]) ).
tcf(c_17716,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP3
| ( X0 = sK23 )
| ( sK38(X0) = X2 )
| ~ ordinal(X1)
| ~ in(X1,omega)
| ~ in(X2,X0)
| ~ subset(sK38(X0),X2)
| ~ element(X0,powerset(powerset(X1))) ),
inference(demodulation,[status(thm)],[c_191,c_1519]) ).
tcf(c_17717,plain,
! [X0: $i,X1: $i] :
( sP3
| ( sK4(X0) = sK23 )
| ( sK38(sK4(X0)) = X1 )
| ~ ordinal(X0)
| ~ sP1(X0)
| ~ in(X0,omega)
| ~ in(X1,sK4(X0))
| ~ subset(sK38(sK4(X0)),X1) ),
inference(superposition,[status(thm)],[c_53,c_17716]) ).
tcf(c_17732,plain,
! [X0: $i,X1: $i] :
( sP3
| ( sK4(X0) = sK23 )
| ( sK38(sK4(X0)) = X1 )
| ~ in(X1,sK4(X0))
| ~ subset(sK38(sK4(X0)),X1)
| ~ sP1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_17717,c_54,c_2299,c_17717]) ).
tcf(c_17733,plain,
! [X0: $i,X1: $i] :
( sP3
| ( sK4(X0) = sK23 )
| ( sK38(sK4(X0)) = X1 )
| ~ sP1(X0)
| ~ in(X1,sK4(X0))
| ~ subset(sK38(sK4(X0)),X1) ),
inference(renaming,[status(thm)],[c_17732]) ).
tcf(c_22626,plain,
! [X0: $i,X1: $i] :
( sP3
| ( sK4(X1) = sK23 )
| ( sK5(X0,sK38(sK4(X1))) = sK38(sK4(X1)) )
| ~ sP1(X1)
| ~ sP1(X0)
| ~ in(sK38(sK4(X1)),sK4(X0))
| ~ in(sK5(X0,sK38(sK4(X1))),sK4(X1)) ),
inference(superposition,[status(thm)],[c_52,c_17733]) ).
tcf(c_22699,plain,
! [X0: $i,X1: $i] :
( sP3
| ( sK4(X1) = sK23 )
| ~ sP1(X1)
| ~ sP1(X0)
| ~ in(sK38(sK4(X1)),sK4(X0))
| ~ in(sK5(X0,sK38(sK4(X1))),sK4(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_22626,c_50]) ).
tcf(c_34196,plain,
! [X0: $i,X1: $i] :
( empty(sK30(powerset(X0)))
| ~ empty(X1)
| ( sK30(powerset(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_35511,plain,
! [X0: $i] :
( sP3
| ( sK4(X0) = sK23 )
| ~ sP1(X0)
| ~ in(sK38(sK4(X0)),sK4(X0)) ),
inference(superposition,[status(thm)],[c_51,c_22699]) ).
tcf(c_35513,plain,
! [X0: $i] :
( sP3
| ( sK4(X0) = sK23 )
| ~ sP1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_35511,c_54,c_2299,c_13392,c_35511]) ).
tcf(c_54052,plain,
! [X0: $i] :
( sP3
| empty(powerset(X0))
| in(sK38(sK30(powerset(X0))),sK30(powerset(X0)))
| ( sK30(powerset(X0)) = sK23 )
| ~ ordinal(X0)
| ~ in(X0,omega) ),
inference(superposition,[status(thm)],[c_142,c_13391]) ).
tcf(c_54088,plain,
! [X0: $i] :
( sP3
| ~ in(X0,omega)
| ( sK30(powerset(X0)) = sK23 )
| in(sK38(sK30(powerset(X0))),sK30(powerset(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_54052,c_178,c_3926,c_54052]) ).
tcf(c_54089,plain,
! [X0: $i] :
( sP3
| in(sK38(sK30(powerset(X0))),sK30(powerset(X0)))
| ( sK30(powerset(X0)) = sK23 )
| ~ in(X0,omega) ),
inference(renaming,[status(thm)],[c_54088]) ).
tcf(c_56546,plain,
! [X0: $i] :
( empty(sK30(powerset(X0)))
| ~ empty(empty_set)
| ( sK30(powerset(X0)) != empty_set ) ),
inference(instantiation,[status(thm)],[c_34196]) ).
tcf(c_57028,plain,
! [X0: $i] :
( sP3
| element(sK38(sK30(powerset(X0))),sK30(powerset(X0)))
| ( sK30(powerset(X0)) = sK23 )
| ~ in(X0,omega) ),
inference(superposition,[status(thm)],[c_54089,c_200]) ).
tcf(c_59569,plain,
! [X0: $i] :
( sP3
| empty(powerset(X0))
| in(sK38(sK30(powerset(X0))),sK30(powerset(X0)))
| ( sK30(powerset(X0)) = empty_set )
| ~ in(X0,omega) ),
inference(resolution,[status(thm)],[c_4690,c_142]) ).
tcf(c_64946,plain,
! [X0: $i] :
( sP3
| empty(sK30(powerset(X0)))
| in(sK38(sK30(powerset(X0))),sK30(powerset(X0)))
| ( sK30(powerset(X0)) = sK23 )
| ~ in(X0,omega) ),
inference(superposition,[status(thm)],[c_57028,c_201]) ).
tcf(c_64967,plain,
! [X0: $i] :
( sP3
| ~ in(X0,omega)
| in(sK38(sK30(powerset(X0))),sK30(powerset(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_64946,c_179,c_178,c_1266,c_56546,c_59569]) ).
tcf(c_64968,plain,
! [X0: $i] :
( sP3
| in(sK38(sK30(powerset(X0))),sK30(powerset(X0)))
| ~ in(X0,omega) ),
inference(renaming,[status(thm)],[c_64967]) ).
tcf(c_65251,plain,
! [X0: $i,X1: $i] :
( in(sK35(X0),X0)
| ( X0 = sK23 )
| ~ sP3
| ~ ordinal(X1)
| ~ in(X1,sK34)
| ~ in(X1,omega)
| ~ element(X0,powerset(powerset(X1))) ),
inference(demodulation,[status(thm)],[c_182,c_1519]) ).
tcf(c_65252,plain,
! [X0: $i] :
( in(sK35(sK4(X0)),sK4(X0))
| ( sK4(X0) = sK23 )
| ~ sP3
| ~ ordinal(X0)
| ~ sP1(X0)
| ~ in(X0,sK34)
| ~ in(X0,omega) ),
inference(superposition,[status(thm)],[c_53,c_65251]) ).
tcf(c_65275,plain,
! [X0: $i] :
( in(sK35(sK4(X0)),sK4(X0))
| ( sK4(X0) = sK23 )
| ~ sP1(X0)
| ~ in(X0,sK34) ),
inference(global_subsumption_just,[status(thm)],[c_65252,c_54,c_2299,c_35513,c_65252]) ).
tcf(c_66291,plain,
! [X0: $i] :
( sP3
| element(sK38(sK30(powerset(X0))),sK30(powerset(X0)))
| ~ in(X0,omega) ),
inference(superposition,[status(thm)],[c_64968,c_200]) ).
tcf(c_67771,plain,
! [X0: $i] :
( sP3
| epsilon_transitive(sK38(sK30(powerset(X0))))
| ~ in(X0,omega)
| ~ ordinal(sK30(powerset(X0))) ),
inference(superposition,[status(thm)],[c_66291,c_158]) ).
tcf(c_69266,plain,
! [X0: $i] :
( sP3
| ( sK10 = empty_set )
| ( sK38(sK10) = X0 )
| ~ in(sK9,omega)
| ~ in(X0,sK10)
| ~ subset(sK38(sK10),X0) ),
inference(resolution,[status(thm)],[c_4691,c_67]) ).
tcf(c_69675,plain,
! [X0: $i] :
( sP3
| ~ in(X0,sK10)
| ~ subset(sK38(sK10),X0)
| ( sK38(sK10) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_69266,c_179,c_68,c_63,c_231,c_480,c_69266]) ).
tcf(c_69676,plain,
! [X0: $i] :
( sP3
| ( sK38(sK10) = X0 )
| ~ in(X0,sK10)
| ~ subset(sK38(sK10),X0) ),
inference(renaming,[status(thm)],[c_69675]) ).
tcf(c_69830,plain,
! [X0: $i] :
( sP3
| ( X0 = sK38(sK10) )
| ~ in(X0,sK10)
| ~ subset(sK38(sK10),X0) ),
inference(resolution,[status(thm)],[c_69676,c_13300]) ).
tcf(c_70357,plain,
( sP3
| ~ in(sK38(sK10),sK10)
| ~ in(sK11(sK38(sK10)),sK10)
| ~ subset(sK38(sK10),sK11(sK38(sK10))) ),
inference(resolution,[status(thm)],[c_69830,c_64]) ).
tcf(c_70556,plain,
! [X0: $i] :
( sP3
| ordinal(sK38(sK30(powerset(X0))))
| ~ in(X0,omega)
| ~ ordinal(sK30(powerset(X0)))
| ~ epsilon_connected(sK38(sK30(powerset(X0)))) ),
inference(superposition,[status(thm)],[c_67771,c_125]) ).
tcf(c_70557,plain,
sP3,
inference(global_subsumption_just,[status(thm)],[c_70556,c_8543,c_8541,c_13396,c_70357]) ).
tcf(c_70583,plain,
ordinal(sK34),
inference(backward_subsumption_resolution,[status(thm)],[c_184,c_70557]) ).
tcf(c_70584,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = empty_set )
| ( sK35(X0) = X2 )
| ~ ordinal(X1)
| ~ in(X1,sK34)
| ~ in(X1,omega)
| ~ in(X2,X0)
| ~ subset(sK35(X0),X2)
| ~ element(X0,powerset(powerset(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_183,c_70557]) ).
tcf(c_70585,plain,
in(sK34,omega),
inference(backward_subsumption_resolution,[status(thm)],[c_181,c_70557]) ).
tcf(c_70586,plain,
sP2(sK34),
inference(backward_subsumption_resolution,[status(thm)],[c_180,c_70557]) ).
tcf(c_70785,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = empty_set )
| ( sK35(X0) = X2 )
| ~ element(X0,powerset(powerset(X1)))
| ~ subset(sK35(X0),X2)
| ~ in(X2,X0)
| ~ in(X1,omega)
| ~ in(X1,sK34) ),
inference(global_subsumption_just,[status(thm)],[c_70584,c_4693,c_8543,c_8541,c_13396,c_70357]) ).
tcf(c_70786,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = empty_set )
| ( sK35(X0) = X2 )
| ~ in(X1,sK34)
| ~ in(X1,omega)
| ~ in(X2,X0)
| ~ subset(sK35(X0),X2)
| ~ element(X0,powerset(powerset(X1))) ),
inference(renaming,[status(thm)],[c_70785]) ).
tcf(c_70794,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sK23 )
| ( sK35(X0) = X2 )
| ~ in(X1,sK34)
| ~ in(X1,omega)
| ~ in(X2,X0)
| ~ subset(sK35(X0),X2)
| ~ element(X0,powerset(powerset(X1))) ),
inference(light_normalisation,[status(thm)],[c_70786,c_1519]) ).
tcf(c_73537,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0) = sK23 )
| ( sK35(sK4(X0)) = X1 )
| ~ sP1(X0)
| ~ in(X0,sK34)
| ~ in(X0,omega)
| ~ in(X1,sK4(X0))
| ~ subset(sK35(sK4(X0)),X1) ),
inference(superposition,[status(thm)],[c_53,c_70794]) ).
tcf(c_73566,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0) = sK23 )
| ( sK35(sK4(X0)) = X1 )
| ~ sP1(X0)
| ~ in(X0,sK34)
| ~ subset(sK35(sK4(X0)),X1)
| ~ in(X1,sK4(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_73537,c_54,c_73537]) ).
tcf(c_73567,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0) = sK23 )
| ( sK35(sK4(X0)) = X1 )
| ~ sP1(X0)
| ~ in(X0,sK34)
| ~ in(X1,sK4(X0))
| ~ subset(sK35(sK4(X0)),X1) ),
inference(renaming,[status(thm)],[c_73566]) ).
tcf(c_77536,plain,
! [X0: $i,X1: $i] :
( ( sK4(X1) = sK23 )
| ( sK5(X0,sK35(sK4(X1))) = sK35(sK4(X1)) )
| ~ sP1(X1)
| ~ sP1(X0)
| ~ in(X1,sK34)
| ~ in(sK35(sK4(X1)),sK4(X0))
| ~ in(sK5(X0,sK35(sK4(X1))),sK4(X1)) ),
inference(superposition,[status(thm)],[c_52,c_73567]) ).
tcf(c_77609,plain,
! [X0: $i,X1: $i] :
( ( sK4(X1) = sK23 )
| ~ sP1(X1)
| ~ sP1(X0)
| ~ in(X1,sK34)
| ~ in(sK35(sK4(X1)),sK4(X0))
| ~ in(sK5(X0,sK35(sK4(X1))),sK4(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_77536,c_50]) ).
tcf(c_79796,plain,
! [X0: $i] :
( ( sK4(X0) = sK23 )
| ~ sP1(X0)
| ~ in(X0,sK34)
| ~ in(sK35(sK4(X0)),sK4(X0)) ),
inference(superposition,[status(thm)],[c_51,c_77609]) ).
tcf(c_79798,plain,
! [X0: $i] :
( ( sK4(X0) = sK23 )
| ~ sP1(X0)
| ~ in(X0,sK34) ),
inference(global_subsumption_just,[status(thm)],[c_79796,c_65275,c_79796]) ).
tcf(c_80326,plain,
( being_limit_ordinal(sK34)
| ( set_union2(sK40(sK34),singleton(sK40(sK34))) = sK34 ) ),
inference(superposition,[status(thm)],[c_70583,c_202]) ).
fof(f114,definition,
! [X10] :
( ~ sP0(X10)
| ? [X11] :
( ordinal(X11)
& in(X11,X10)
& in(X11,omega)
& ? [X12] :
( element(X12,powerset(powerset(X11)))
& ! [X13] :
( ? [X14] :
( subset(X13,X14)
& in(X14,X12)
& X13 != X14 )
| ~ in(X13,X12) )
& empty_set != X12 ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f115,definition,
! [X3] :
( ~ sP1(X3)
| ( in(X3,omega)
& ? [X4] :
( element(X4,powerset(powerset(X3)))
& ! [X5] :
( ? [X6] :
( subset(X5,X6)
& in(X6,X4)
& X5 != X6 )
| ~ in(X5,X4) )
& X4 != empty_set ) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f116,plain,
( ! [X10] :
( ~ ordinal(X10)
| sP0(X10)
| ~ being_limit_ordinal(X10)
| ~ in(X10,omega)
| ! [X15] :
( ~ element(X15,powerset(powerset(X10)))
| ? [X16] :
( ! [X17] :
( ~ subset(X16,X17)
| ~ in(X17,X15)
| X16 = X17 )
& in(X16,X15) )
| empty_set = X15 )
| empty_set = X10 )
& ! [X3] :
( ~ ordinal(X3)
| sP1(X3)
| ~ in(succ(X3),omega)
| ! [X7] :
( ~ element(X7,powerset(powerset(succ(X3))))
| ? [X8] :
( ! [X9] :
( ~ subset(X8,X9)
| ~ in(X9,X7)
| X9 = X8 )
& in(X8,X7) )
| empty_set = X7 ) )
& ( ~ in(empty_set,omega)
| ! [X0] :
( ~ element(X0,powerset(powerset(empty_set)))
| ? [X1] :
( ! [X2] :
( ~ subset(X1,X2)
| ~ in(X2,X0)
| X2 = X1 )
& in(X1,X0) )
| empty_set = X0 ) )
& ? [X18] :
( ordinal(X18)
& in(X18,omega)
& ? [X19] :
( element(X19,powerset(powerset(X18)))
& ! [X20] :
( ? [X21] :
( subset(X20,X21)
& in(X21,X19)
& X20 != X21 )
| ~ in(X20,X19) )
& empty_set != X19 ) ) ),
inference(definition_folding,[],[f82,f115,f114]) ).
fof(f117,definition,
! [X0] :
( ~ sP2(X0)
| ? [X5] :
( element(X5,powerset(powerset(X0)))
& ! [X6] :
( ? [X7] :
( subset(X6,X7)
& in(X7,X5)
& X6 != X7 )
| ~ in(X6,X5) )
& X5 != empty_set ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f118,definition,
( ~ sP3
| ? [X0] :
( ordinal(X0)
& ! [X1] :
( ~ ordinal(X1)
| ~ in(X1,X0)
| ~ in(X1,omega)
| ! [X2] :
( ~ element(X2,powerset(powerset(X1)))
| ? [X3] :
( ! [X4] :
( ~ subset(X3,X4)
| ~ in(X4,X2)
| X4 = X3 )
& in(X3,X2) )
| empty_set = X2 ) )
& in(X0,omega)
& sP2(X0) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f119,plain,
( sP3
| ! [X8] :
( ~ ordinal(X8)
| ~ in(X8,omega)
| ! [X9] :
( ~ element(X9,powerset(powerset(X8)))
| ? [X10] :
( ! [X11] :
( ~ subset(X10,X11)
| ~ in(X11,X9)
| X10 = X11 )
& in(X10,X9) )
| empty_set = X9 ) ) ),
inference(definition_folding,[],[f104,f118,f117]) ).
fof(f123,plain,
! [X10] :
( ~ sP0(X10)
| ? [X11] :
( ordinal(X11)
& in(X11,X10)
& in(X11,omega)
& ? [X12] :
( element(X12,powerset(powerset(X11)))
& ! [X13] :
( ? [X14] :
( subset(X13,X14)
& in(X14,X12)
& X13 != X14 )
| ~ in(X13,X12) )
& empty_set != X12 ) ) ),
inference(nnf_transformation,[],[f114]) ).
fof(f124,plain,
! [X0] :
( ~ sP0(X0)
| ? [X1] :
( ordinal(X1)
& in(X1,X0)
& in(X1,omega)
& ? [X2] :
( element(X2,powerset(powerset(X1)))
& ! [X3] :
( ? [X4] :
( subset(X3,X4)
& in(X4,X2)
& X3 != X4 )
| ~ in(X3,X2) )
& empty_set != X2 ) ) ),
inference(rectify,[],[f123]) ).
fof(f125,plain,
! [X0] :
( ~ sP0(X0)
| ( ordinal(sK6(X0))
& in(sK6(X0),X0)
& in(sK6(X0),omega)
& element(sK7(X0),powerset(powerset(sK6(X0))))
& ! [X3] :
( ( subset(X3,sK8(X0,X3))
& in(sK8(X0,X3),sK7(X0))
& sK8(X0,X3) != X3 )
| ~ in(X3,sK7(X0)) )
& empty_set != sK7(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8]),skolemize(X1,sK6(X0)),skolemize(X2,sK7(X0)),skolemize(X4,sK8(X0,X3))],[f124]) ).
fof(f149,plain,
! [X0] :
( ~ sP2(X0)
| ? [X5] :
( element(X5,powerset(powerset(X0)))
& ! [X6] :
( ? [X7] :
( subset(X6,X7)
& in(X7,X5)
& X6 != X7 )
| ~ in(X6,X5) )
& X5 != empty_set ) ),
inference(nnf_transformation,[],[f117]) ).
fof(f150,plain,
! [X0] :
( ~ sP2(X0)
| ? [X1] :
( element(X1,powerset(powerset(X0)))
& ! [X2] :
( ? [X3] :
( subset(X2,X3)
& in(X3,X1)
& X2 != X3 )
| ~ in(X2,X1) )
& empty_set != X1 ) ),
inference(rectify,[],[f149]) ).
fof(f151,plain,
! [X0] :
( ~ sP2(X0)
| ( element(sK36(X0),powerset(powerset(X0)))
& ! [X2] :
( ( subset(X2,sK37(X0,X2))
& in(sK37(X0,X2),sK36(X0))
& sK37(X0,X2) != X2 )
| ~ in(X2,sK36(X0)) )
& empty_set != sK36(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36,sK37]),skolemize(X1,sK36(X0)),skolemize(X3,sK37(X0,X2))],[f150]) ).
fof(f162,plain,
! [X0] :
( ~ sP0(X0)
| ordinal(sK6(X0)) ),
inference(cnf_transformation,[],[f125]) ).
fof(f163,plain,
! [X0] :
( ~ sP0(X0)
| in(sK6(X0),X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f164,plain,
! [X0] :
( ~ sP0(X0)
| in(sK6(X0),omega) ),
inference(cnf_transformation,[],[f125]) ).
fof(f165,plain,
! [X0] :
( ~ sP0(X0)
| element(sK7(X0),powerset(powerset(sK6(X0)))) ),
inference(cnf_transformation,[],[f125]) ).
fof(f166,plain,
! [X3,X0] :
( ~ sP0(X0)
| subset(X3,sK8(X0,X3))
| ~ in(X3,sK7(X0)) ),
inference(cnf_transformation,[],[f125]) ).
fof(f167,plain,
! [X3,X0] :
( ~ sP0(X0)
| in(sK8(X0,X3),sK7(X0))
| ~ in(X3,sK7(X0)) ),
inference(cnf_transformation,[],[f125]) ).
fof(f168,plain,
! [X3,X0] :
( ~ sP0(X0)
| sK8(X0,X3) != X3
| ~ in(X3,sK7(X0)) ),
inference(cnf_transformation,[],[f125]) ).
fof(f169,plain,
! [X0] :
( ~ sP0(X0)
| empty_set != sK7(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f295,plain,
! [X0] :
( ~ sP2(X0)
| element(sK36(X0),powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f151]) ).
fof(f296,plain,
! [X2,X0] :
( ~ sP2(X0)
| subset(X2,sK37(X0,X2))
| ~ in(X2,sK36(X0)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f297,plain,
! [X2,X0] :
( ~ sP2(X0)
| in(sK37(X0,X2),sK36(X0))
| ~ in(X2,sK36(X0)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f298,plain,
! [X2,X0] :
( ~ sP2(X0)
| sK37(X0,X2) != X2
| ~ in(X2,sK36(X0)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f299,plain,
! [X0] :
( ~ sP2(X0)
| empty_set != sK36(X0) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_55,plain,
! [X0: $i] :
( ~ sP0(X0)
| ( sK7(X0) != empty_set ) ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X0)
| ~ in(X1,sK7(X0))
| ( sK8(X0,X1) != X1 ) ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] :
( in(sK8(X1,X0),sK7(X1))
| ~ sP0(X1)
| ~ in(X0,sK7(X1)) ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( subset(X0,sK8(X1,X0))
| ~ sP0(X1)
| ~ in(X0,sK7(X1)) ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_59,plain,
! [X0: $i] :
( element(sK7(X0),powerset(powerset(sK6(X0))))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_60,plain,
! [X0: $i] :
( in(sK6(X0),omega)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_61,plain,
! [X0: $i] :
( in(sK6(X0),X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_62,plain,
! [X0: $i] :
( ordinal(sK6(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f162]) ).
tcf(c_185,plain,
! [X0: $i] :
( ~ sP2(X0)
| ( sK36(X0) != empty_set ) ),
inference(cnf_transformation,[],[f299]) ).
tcf(c_186,plain,
! [X0: $i,X1: $i] :
( ~ sP2(X0)
| ~ in(X1,sK36(X0))
| ( sK37(X0,X1) != X1 ) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_187,plain,
! [X0: $i,X1: $i] :
( in(sK37(X1,X0),sK36(X1))
| ~ sP2(X1)
| ~ in(X0,sK36(X1)) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_188,plain,
! [X0: $i,X1: $i] :
( subset(X0,sK37(X1,X0))
| ~ sP2(X1)
| ~ in(X0,sK36(X1)) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_189,plain,
! [X0: $i] :
( element(sK36(X0),powerset(powerset(X0)))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_5964,plain,
! [X0: $i] :
( ~ sP0(X0)
| ( sK7(X0) != sK23 ) ),
inference(demodulation,[status(thm)],[c_55,c_1519]) ).
tcf(c_13393,plain,
! [X0: $i] :
( sP3
| in(sK38(sK7(X0)),sK7(X0))
| ( sK7(X0) = sK23 )
| ~ sP0(X0)
| ~ ordinal(sK6(X0))
| ~ in(sK6(X0),omega) ),
inference(superposition,[status(thm)],[c_59,c_13391]) ).
tcf(c_17718,plain,
! [X0: $i,X1: $i] :
( sP3
| ( sK7(X0) = sK23 )
| ( sK38(sK7(X0)) = X1 )
| ~ sP0(X0)
| ~ ordinal(sK6(X0))
| ~ in(sK6(X0),omega)
| ~ in(X1,sK7(X0))
| ~ subset(sK38(sK7(X0)),X1) ),
inference(superposition,[status(thm)],[c_59,c_17716]) ).
tcf(c_17742,plain,
! [X0: $i,X1: $i] :
( sP3
| ~ subset(sK38(sK7(X0)),X1)
| ~ in(X1,sK7(X0))
| ~ sP0(X0)
| ( sK38(sK7(X0)) = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_17718,c_62,c_60,c_5964,c_17718]) ).
tcf(c_17743,plain,
! [X0: $i,X1: $i] :
( sP3
| ( sK38(sK7(X0)) = X1 )
| ~ sP0(X0)
| ~ in(X1,sK7(X0))
| ~ subset(sK38(sK7(X0)),X1) ),
inference(renaming,[status(thm)],[c_17742]) ).
tcf(c_22043,plain,
! [X0: $i] :
( ~ sP2(X0)
| ( sK36(X0) != sK23 ) ),
inference(demodulation,[status(thm)],[c_185,c_1519]) ).
tcf(c_23309,plain,
! [X0: $i,X1: $i] :
( sP3
| ( sK8(X0,sK38(sK7(X1))) = sK38(sK7(X1)) )
| ~ sP0(X1)
| ~ sP0(X0)
| ~ in(sK38(sK7(X1)),sK7(X0))
| ~ in(sK8(X0,sK38(sK7(X1))),sK7(X1)) ),
inference(superposition,[status(thm)],[c_58,c_17743]) ).
tcf(c_23353,plain,
! [X0: $i,X1: $i] :
( sP3
| ~ sP0(X1)
| ~ sP0(X0)
| ~ in(sK38(sK7(X1)),sK7(X0))
| ~ in(sK8(X0,sK38(sK7(X1))),sK7(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23309,c_56]) ).
tcf(c_25973,plain,
! [X0: $i,X1: $i] :
( sP1(X0)
| ( sK36(set_union2(X0,singleton(X0))) = empty_set )
| ( sK13(sK36(set_union2(X0,singleton(X0)))) = X1 )
| ~ ordinal(X0)
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| ~ in(X1,sK36(set_union2(X0,singleton(X0))))
| ~ subset(sK13(sK36(set_union2(X0,singleton(X0)))),X1) ),
inference(superposition,[status(thm)],[c_189,c_73]) ).
tcf(c_25974,plain,
! [X0: $i] :
( sP1(X0)
| in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(set_union2(X0,singleton(X0))))
| ( sK36(set_union2(X0,singleton(X0))) = empty_set )
| ~ ordinal(X0)
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega) ),
inference(superposition,[status(thm)],[c_189,c_72]) ).
tcf(c_25977,plain,
! [X0: $i,X1: $i] :
( sP0(X0)
| ( X0 = empty_set )
| ( sK36(X0) = empty_set )
| ( sK14(sK36(X0)) = X1 )
| ~ sP2(X0)
| ~ being_limit_ordinal(X0)
| ~ ordinal(X0)
| ~ in(X0,omega)
| ~ in(X1,sK36(X0))
| ~ subset(sK14(sK36(X0)),X1) ),
inference(superposition,[status(thm)],[c_189,c_75]) ).
tcf(c_25978,plain,
! [X0: $i] :
( sP0(X0)
| in(sK14(sK36(X0)),sK36(X0))
| ( X0 = empty_set )
| ( sK36(X0) = empty_set )
| ~ sP2(X0)
| ~ being_limit_ordinal(X0)
| ~ ordinal(X0)
| ~ in(X0,omega) ),
inference(superposition,[status(thm)],[c_189,c_74]) ).
tcf(c_25983,plain,
! [X0: $i] :
( ( sK36(sK23) = sK23 )
| ( sK12(sK36(sK23)) = X0 )
| ~ sP2(sK23)
| ~ in(sK23,omega)
| ~ in(X0,sK36(sK23))
| ~ subset(sK12(sK36(sK23)),X0) ),
inference(superposition,[status(thm)],[c_189,c_1558]) ).
tcf(c_25984,plain,
( in(sK12(sK36(sK23)),sK36(sK23))
| ( sK36(sK23) = sK23 )
| ~ sP2(sK23)
| ~ in(sK23,omega) ),
inference(superposition,[status(thm)],[c_189,c_1553]) ).
tcf(c_26009,plain,
( in(sK12(sK36(sK23)),sK36(sK23))
| ~ sP2(sK23)
| ~ in(sK23,omega) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25984,c_22043]) ).
tcf(c_26051,plain,
! [X0: $i] :
( ( sK12(sK36(sK23)) = X0 )
| ~ sP2(sK23)
| ~ in(sK23,omega)
| ~ in(X0,sK36(sK23))
| ~ subset(sK12(sK36(sK23)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25983,c_22043]) ).
tcf(c_26077,plain,
! [X0: $i] :
( sP0(X0)
| in(sK14(sK36(X0)),sK36(X0))
| ( X0 = empty_set )
| ~ in(X0,omega)
| ~ being_limit_ordinal(X0)
| ~ sP2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_25978,c_185,c_3926,c_25978]) ).
tcf(c_26078,plain,
! [X0: $i] :
( sP0(X0)
| in(sK14(sK36(X0)),sK36(X0))
| ( X0 = empty_set )
| ~ sP2(X0)
| ~ being_limit_ordinal(X0)
| ~ in(X0,omega) ),
inference(renaming,[status(thm)],[c_26077]) ).
tcf(c_26085,plain,
! [X0: $i] :
( sP0(X0)
| in(sK14(sK36(X0)),sK36(X0))
| ( X0 = sK23 )
| ~ sP2(X0)
| ~ being_limit_ordinal(X0)
| ~ in(X0,omega) ),
inference(light_normalisation,[status(thm)],[c_26078,c_1519]) ).
tcf(c_26127,plain,
! [X0: $i] :
( sP1(X0)
| in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(set_union2(X0,singleton(X0))))
| ( sK36(set_union2(X0,singleton(X0))) = sK23 )
| ~ ordinal(X0)
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega) ),
inference(light_normalisation,[status(thm)],[c_25974,c_1519]) ).
tcf(c_26134,plain,
! [X0: $i] :
( sP1(X0)
| in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(set_union2(X0,singleton(X0))))
| ~ ordinal(X0)
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26127,c_22043]) ).
tcf(c_26145,plain,
! [X0: $i,X1: $i] :
( sP0(X0)
| ( X0 = empty_set )
| ~ in(X0,omega)
| ~ in(X1,sK36(X0))
| ~ subset(sK14(sK36(X0)),X1)
| ~ being_limit_ordinal(X0)
| ~ sP2(X0)
| ( sK14(sK36(X0)) = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_25977,c_185,c_3926,c_25977]) ).
tcf(c_26146,plain,
! [X0: $i,X1: $i] :
( sP0(X0)
| ( X0 = empty_set )
| ( sK14(sK36(X0)) = X1 )
| ~ sP2(X0)
| ~ being_limit_ordinal(X0)
| ~ in(X0,omega)
| ~ in(X1,sK36(X0))
| ~ subset(sK14(sK36(X0)),X1) ),
inference(renaming,[status(thm)],[c_26145]) ).
tcf(c_26155,plain,
! [X0: $i,X1: $i] :
( sP0(X0)
| ( X0 = sK23 )
| ( sK14(sK36(X0)) = X1 )
| ~ sP2(X0)
| ~ being_limit_ordinal(X0)
| ~ in(X0,omega)
| ~ in(X1,sK36(X0))
| ~ subset(sK14(sK36(X0)),X1) ),
inference(light_normalisation,[status(thm)],[c_26146,c_1519]) ).
tcf(c_26173,plain,
! [X0: $i,X1: $i] :
( sP1(X0)
| ( sK36(set_union2(X0,singleton(X0))) = sK23 )
| ( sK13(sK36(set_union2(X0,singleton(X0)))) = X1 )
| ~ ordinal(X0)
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| ~ in(X1,sK36(set_union2(X0,singleton(X0))))
| ~ subset(sK13(sK36(set_union2(X0,singleton(X0)))),X1) ),
inference(light_normalisation,[status(thm)],[c_25973,c_1519]) ).
tcf(c_26182,plain,
! [X0: $i,X1: $i] :
( sP1(X0)
| ( sK13(sK36(set_union2(X0,singleton(X0)))) = X1 )
| ~ ordinal(X0)
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| ~ in(X1,sK36(set_union2(X0,singleton(X0))))
| ~ subset(sK13(sK36(set_union2(X0,singleton(X0)))),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26173,c_22043]) ).
tcf(c_28546,plain,
! [X0: $i,X1: $i] :
( sP0(X1)
| ( X1 = sK23 )
| ( sK37(X0,sK14(sK36(X1))) = sK14(sK36(X1)) )
| ~ sP2(X1)
| ~ sP2(X0)
| ~ being_limit_ordinal(X1)
| ~ in(X1,omega)
| ~ in(sK14(sK36(X1)),sK36(X0))
| ~ in(sK37(X0,sK14(sK36(X1))),sK36(X1)) ),
inference(superposition,[status(thm)],[c_188,c_26155]) ).
tcf(c_28579,plain,
! [X0: $i,X1: $i] :
( sP0(X1)
| ( X1 = sK23 )
| ~ sP2(X1)
| ~ sP2(X0)
| ~ being_limit_ordinal(X1)
| ~ in(X1,omega)
| ~ in(sK14(sK36(X1)),sK36(X0))
| ~ in(sK37(X0,sK14(sK36(X1))),sK36(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_28546,c_186]) ).
tcf(c_29619,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| ( sK37(X0,sK13(sK36(set_union2(X1,singleton(X1))))) = sK13(sK36(set_union2(X1,singleton(X1)))) )
| ~ sP2(X0)
| ~ ordinal(X1)
| ~ sP2(set_union2(X1,singleton(X1)))
| ~ in(set_union2(X1,singleton(X1)),omega)
| ~ in(sK13(sK36(set_union2(X1,singleton(X1)))),sK36(X0))
| ~ in(sK37(X0,sK13(sK36(set_union2(X1,singleton(X1))))),sK36(set_union2(X1,singleton(X1)))) ),
inference(superposition,[status(thm)],[c_188,c_26182]) ).
tcf(c_29661,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| ~ sP2(X0)
| ~ ordinal(X1)
| ~ sP2(set_union2(X1,singleton(X1)))
| ~ in(set_union2(X1,singleton(X1)),omega)
| ~ in(sK13(sK36(set_union2(X1,singleton(X1)))),sK36(X0))
| ~ in(sK37(X0,sK13(sK36(set_union2(X1,singleton(X1))))),sK36(set_union2(X1,singleton(X1)))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_29619,c_186]) ).
tcf(c_36806,plain,
! [X0: $i] :
( ( sK37(X0,sK12(sK36(sK23))) = sK12(sK36(sK23)) )
| ~ sP2(sK23)
| ~ sP2(X0)
| ~ in(sK23,omega)
| ~ in(sK12(sK36(sK23)),sK36(X0))
| ~ in(sK37(X0,sK12(sK36(sK23))),sK36(sK23)) ),
inference(superposition,[status(thm)],[c_188,c_26051]) ).
tcf(c_36828,plain,
! [X0: $i] :
( ~ sP2(sK23)
| ~ sP2(X0)
| ~ in(sK23,omega)
| ~ in(sK12(sK36(sK23)),sK36(X0))
| ~ in(sK37(X0,sK12(sK36(sK23))),sK36(sK23)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_36806,c_186]) ).
tcf(c_37234,plain,
! [X0: $i] :
( sP0(X0)
| ( X0 = sK23 )
| ~ sP2(X0)
| ~ being_limit_ordinal(X0)
| ~ in(X0,omega)
| ~ in(sK14(sK36(X0)),sK36(X0)) ),
inference(superposition,[status(thm)],[c_187,c_28579]) ).
tcf(c_37235,plain,
! [X0: $i] :
( sP0(X0)
| ( X0 = sK23 )
| ~ sP2(X0)
| ~ being_limit_ordinal(X0)
| ~ in(X0,omega) ),
inference(global_subsumption_just,[status(thm)],[c_37234,c_26085,c_37234]) ).
tcf(c_38295,plain,
! [X0: $i] :
( sP3
| ~ sP0(X0)
| ~ in(sK38(sK7(X0)),sK7(X0)) ),
inference(superposition,[status(thm)],[c_57,c_23353]) ).
tcf(c_38297,plain,
! [X0: $i] :
( sP3
| ~ sP0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_38295,c_62,c_60,c_5964,c_13393,c_38295]) ).
tcf(c_38639,plain,
! [X0: $i] :
( sP1(X0)
| ~ ordinal(X0)
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| ~ in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(set_union2(X0,singleton(X0)))) ),
inference(superposition,[status(thm)],[c_187,c_29661]) ).
tcf(c_38643,plain,
! [X0: $i] :
( sP1(X0)
| ~ ordinal(X0)
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega) ),
inference(global_subsumption_just,[status(thm)],[c_38639,c_26134,c_38639]) ).
tcf(c_39145,plain,
( sP0(sK34)
| ( sK23 = sK34 )
| ~ sP3
| ~ sP2(sK34)
| ~ being_limit_ordinal(sK34) ),
inference(superposition,[status(thm)],[c_181,c_37235]) ).
tcf(c_39150,plain,
( sP0(sK34)
| ( sK23 = sK34 )
| ~ sP3
| ~ being_limit_ordinal(sK34) ),
inference(global_subsumption_just,[status(thm)],[c_39145,c_180,c_39145]) ).
tcf(c_39520,plain,
( ~ sP2(sK23)
| ~ in(sK23,omega)
| ~ in(sK12(sK36(sK23)),sK36(sK23)) ),
inference(superposition,[status(thm)],[c_187,c_36828]) ).
tcf(c_39521,plain,
( ~ sP2(sK23)
| ~ in(sK23,omega) ),
inference(global_subsumption_just,[status(thm)],[c_39520,c_26009,c_39520]) ).
tcf(c_65253,plain,
! [X0: $i] :
( in(sK35(sK7(X0)),sK7(X0))
| ( sK7(X0) = sK23 )
| ~ sP3
| ~ sP0(X0)
| ~ ordinal(sK6(X0))
| ~ in(sK6(X0),sK34)
| ~ in(sK6(X0),omega) ),
inference(superposition,[status(thm)],[c_59,c_65251]) ).
tcf(c_65310,plain,
! [X0: $i] :
( in(sK35(sK7(X0)),sK7(X0))
| ~ sP0(X0)
| ~ in(sK6(X0),sK34) ),
inference(global_subsumption_just,[status(thm)],[c_65253,c_62,c_60,c_5964,c_38297,c_65253]) ).
tcf(c_70578,plain,
( sP0(sK34)
| ( sK23 = sK34 )
| ~ being_limit_ordinal(sK34) ),
inference(backward_subsumption_resolution,[status(thm)],[c_39150,c_70557]) ).
tcf(c_73538,plain,
! [X0: $i,X1: $i] :
( ( sK7(X0) = sK23 )
| ( sK35(sK7(X0)) = X1 )
| ~ sP0(X0)
| ~ in(sK6(X0),sK34)
| ~ in(sK6(X0),omega)
| ~ in(X1,sK7(X0))
| ~ subset(sK35(sK7(X0)),X1) ),
inference(superposition,[status(thm)],[c_59,c_70794]) ).
tcf(c_73576,plain,
! [X0: $i,X1: $i] :
( ~ in(X1,sK7(X0))
| ~ subset(sK35(sK7(X0)),X1)
| ~ in(sK6(X0),sK34)
| ~ sP0(X0)
| ( sK35(sK7(X0)) = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_73538,c_60,c_5964,c_73538]) ).
tcf(c_73577,plain,
! [X0: $i,X1: $i] :
( ( sK35(sK7(X0)) = X1 )
| ~ sP0(X0)
| ~ in(sK6(X0),sK34)
| ~ in(X1,sK7(X0))
| ~ subset(sK35(sK7(X0)),X1) ),
inference(renaming,[status(thm)],[c_73576]) ).
tcf(c_77883,plain,
! [X0: $i,X1: $i] :
( ( sK8(X0,sK35(sK7(X1))) = sK35(sK7(X1)) )
| ~ sP0(X1)
| ~ sP0(X0)
| ~ in(sK6(X1),sK34)
| ~ in(sK35(sK7(X1)),sK7(X0))
| ~ in(sK8(X0,sK35(sK7(X1))),sK7(X1)) ),
inference(superposition,[status(thm)],[c_58,c_73577]) ).
tcf(c_77927,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X1)
| ~ sP0(X0)
| ~ in(sK6(X1),sK34)
| ~ in(sK35(sK7(X1)),sK7(X0))
| ~ in(sK8(X0,sK35(sK7(X1))),sK7(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_77883,c_56]) ).
tcf(c_79874,plain,
! [X0: $i] :
( ~ sP0(X0)
| ~ in(sK6(X0),sK34)
| ~ in(sK35(sK7(X0)),sK7(X0)) ),
inference(superposition,[status(thm)],[c_57,c_77927]) ).
tcf(c_79876,plain,
! [X0: $i] :
( ~ sP0(X0)
| ~ in(sK6(X0),sK34) ),
inference(global_subsumption_just,[status(thm)],[c_79874,c_65310,c_79874]) ).
tcf(c_80195,plain,
~ sP0(sK34),
inference(superposition,[status(thm)],[c_61,c_79876]) ).
tcf(c_80196,plain,
( ( sK23 = sK34 )
| ~ being_limit_ordinal(sK34) ),
inference(backward_subsumption_resolution,[status(thm)],[c_70578,c_80195]) ).
tcf(c_90329,plain,
( ( sK23 = sK34 )
| ( set_union2(sK40(sK34),singleton(sK40(sK34))) = sK34 ) ),
inference(superposition,[status(thm)],[c_80326,c_80196]) ).
tcf(c_90414,plain,
( sP1(sK40(sK34))
| ( sK23 = sK34 )
| ~ ordinal(sK40(sK34))
| ~ in(sK34,omega)
| ~ sP2(set_union2(sK40(sK34),singleton(sK40(sK34)))) ),
inference(superposition,[status(thm)],[c_90329,c_38643]) ).
tcf(c_90452,plain,
( ordinal(sK40(sK34))
| ( sK23 = sK34 )
| ~ ordinal(sK34) ),
inference(superposition,[status(thm)],[c_90329,c_2330]) ).
tcf(c_90456,plain,
( in(sK40(sK34),sK34)
| ( sK23 = sK34 ) ),
inference(superposition,[status(thm)],[c_90329,c_198]) ).
tcf(c_90500,plain,
( sP1(sK40(sK34))
| ( sK23 = sK34 ) ),
inference(global_subsumption_just,[status(thm)],[c_90414,c_184,c_180,c_181,c_8543,c_8541,c_12901,c_13396,c_70357,c_90329,c_90452,c_90414]) ).
tcf(c_91398,plain,
( ( sK23 = sK34 )
| ( sK4(sK40(sK34)) = sK23 )
| ~ sP1(sK40(sK34)) ),
inference(superposition,[status(thm)],[c_90456,c_79798]) ).
tcf(c_91403,plain,
( ( sK23 = sK34 )
| ( sK4(sK40(sK34)) = sK23 ) ),
inference(global_subsumption_just,[status(thm)],[c_91398,c_90500,c_91398]) ).
tcf(c_91479,plain,
( ( sK23 = sK34 )
| ~ sP1(sK40(sK34))
| ( empty_set != sK23 ) ),
inference(superposition,[status(thm)],[c_91403,c_49]) ).
tcf(c_91489,plain,
sK23 = sK34,
inference(global_subsumption_just,[status(thm)],[c_91479,c_1519,c_90500,c_91479]) ).
tcf(c_91688,plain,
sP2(sK23),
inference(superposition,[status(thm)],[c_91489,c_70586]) ).
tcf(c_91689,plain,
in(sK23,omega),
inference(superposition,[status(thm)],[c_91489,c_70585]) ).
tcf(c_91699,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_91689,c_91688,c_39521]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU301+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.20/0.45 % Computer : n017.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Thu Sep 24 13:31:46 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.45 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.23/0.51 Running first-order theorem proving
% 0.23/0.51 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.23/0.52
% 0.23/0.52 % ======== iProver multi-core TPTP/SMT =========
% 0.23/0.52
% 0.23/0.52 % Detected problem language: tptp
% 0.23/0.54 % Proving...
% 112.13/18.24 % SZS status Started for theBenchmark.p
% 112.13/18.24 % SZS status Theorem for theBenchmark.p
% 112.13/18.24
% 112.13/18.24 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 112.13/18.24
% 112.13/18.24 % ------ iProver source info
% 112.13/18.24
% 112.13/18.24 % git: date: 2026-07-19 20:42:38 +0200
% 112.13/18.24 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 112.13/18.24 % git: non_committed_changes: false
% 112.13/18.24
% 112.13/18.24 % ------ Parsing...
% 112.13/18.24 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 112.13/18.24
% 112.13/18.24 % ------ Preprocessing... sf_s rm: 34 0s sf_e sf_s rm: 5 0s sf_e %
% 112.13/18.24
% 112.13/18.24 % ------ Preprocessing...%
% 112.13/18.24
% 112.13/18.24 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 112.13/18.24 % ------ Proving...
% 112.13/18.24 % ------ Problem Properties
% 112.13/18.24
% 112.13/18.24 %
% 112.13/18.24 % clauses 118
% 112.13/18.24 % conjectures 13
% 112.13/18.24 % EPR 59
% 112.13/18.24 % Horn 103
% 112.13/18.24 % unary 53
% 112.13/18.24 % binary 38
% 112.13/18.24 % lits 252
% 112.13/18.24 % lits eq 31
% 112.13/18.24 % fd_pure 0
% 112.13/18.24 % fd_pseudo 0
% 112.13/18.24 % fd_cond 6
% 112.13/18.24 % fd_pseudo_cond 6
% 112.13/18.24 % AC symbols 0
% 112.13/18.24
% 112.13/18.24 % ------ Input Options Time Limit: Unbounded
% 112.13/18.24
% 112.13/18.24
% 112.13/18.24 % ------
% 112.13/18.24 % Current options:
% 112.13/18.24 % ------
% 112.13/18.24
% 112.13/18.24
% 112.13/18.24 %
% 112.13/18.24
% 112.13/18.24 % ------ Proving...
% 112.13/18.24 %
% 112.13/18.24
% 112.13/18.24 % SZS status Theorem for theBenchmark.p
% 112.13/18.24
% 112.13/18.24 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 112.13/18.25
% 112.13/18.25
%------------------------------------------------------------------------------