%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU299+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:14 PM UTC 2026
% Result : Theorem 2.21s 1.31s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 31
% Syntax : Number of formulae : 264 ( 8 unt; 29 def)
% Number of atoms : 1378 ( 237 equ)
% Maximal formula atoms : 34 ( 5 avg)
% Number of connectives : 1802 ( 688 ~; 846 |; 199 &)
% ( 34 <=>; 32 =>; 0 <=; 3 <~>)
% Maximal formula depth : 24 ( 7 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 35 ( 33 usr; 26 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 7 con; 0-2 aty)
% Number of variables : 461 ( 0 sgn 376 !; 85 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ordinal(X0)
=> ? [X1] :
! [X2] :
( in(X2,X1)
<=> ( in(X2,succ(X0))
& ? [X3] :
( ordinal(X3)
& X2 = X3
& ( in(X3,omega)
=> ! [X4] :
( element(X4,powerset(powerset(X3)))
=> ~ ( X4 != empty_set
& ! [X5] :
~ ( in(X5,X4)
& ! [X6] :
( ( in(X6,X4)
& subset(X5,X6) )
=> X6 = X5 ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_xboole_0__e18_27__finset_1__1) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ordinal(X0)
=> ? [X1] :
! [X2] :
( in(X2,X1)
<=> ( in(X2,succ(X0))
& ? [X3] :
( ordinal(X3)
& X2 = X3
& ( in(X3,omega)
=> ! [X4] :
( element(X4,powerset(powerset(X3)))
=> ~ ( X4 != empty_set
& ! [X5] :
~ ( in(X5,X4)
& ! [X6] :
( ( in(X6,X4)
& subset(X5,X6) )
=> X6 = X5 ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f48,axiom,
! [X0] :
( ordinal(X0)
=> ( ! [X1,X2,X3] :
( ( X1 = X2
& ? [X4] :
( ordinal(X4)
& X2 = X4
& ( in(X4,omega)
=> ! [X5] :
( element(X5,powerset(powerset(X4)))
=> ~ ( X5 != empty_set
& ! [X6] :
~ ( in(X6,X5)
& ! [X7] :
( ( in(X7,X5)
& subset(X6,X7) )
=> X7 = X6 ) ) ) ) ) )
& X1 = X3
& ? [X8] :
( ordinal(X8)
& X3 = X8
& ( in(X8,omega)
=> ! [X9] :
( element(X9,powerset(powerset(X8)))
=> ~ ( X9 != empty_set
& ! [X10] :
~ ( in(X10,X9)
& ! [X11] :
( ( in(X11,X9)
& subset(X10,X11) )
=> X11 = X10 ) ) ) ) ) ) )
=> X2 = X3 )
=> ? [X1] :
! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,succ(X0))
& X3 = X2
& ? [X12] :
( ordinal(X12)
& X2 = X12
& ( in(X12,omega)
=> ! [X13] :
( element(X13,powerset(powerset(X12)))
=> ~ ( X13 != empty_set
& ! [X14] :
~ ( in(X14,X13)
& ! [X15] :
( ( in(X15,X13)
& subset(X14,X15) )
=> X15 = X14 ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_tarski__e18_27__finset_1__1) ).
fof(f50,plain,
! [X0] :
( ordinal(X0)
=> ( ! [X1,X2,X3] :
( ( X1 = X2
& ? [X4] :
( ordinal(X4)
& X2 = X4
& ( in(X4,omega)
=> ! [X5] :
( element(X5,powerset(powerset(X4)))
=> ~ ( X5 != empty_set
& ! [X6] :
~ ( in(X6,X5)
& ! [X7] :
( ( in(X7,X5)
& subset(X6,X7) )
=> X7 = X6 ) ) ) ) ) )
& X1 = X3
& ? [X8] :
( ordinal(X8)
& X3 = X8
& ( in(X8,omega)
=> ! [X9] :
( element(X9,powerset(powerset(X8)))
=> ~ ( X9 != empty_set
& ! [X10] :
~ ( in(X10,X9)
& ! [X11] :
( ( in(X11,X9)
& subset(X10,X11) )
=> X11 = X10 ) ) ) ) ) ) )
=> X2 = X3 )
=> ? [X12] :
! [X13] :
( in(X13,X12)
<=> ? [X14] :
( in(X14,succ(X0))
& X13 = X14
& ? [X15] :
( ordinal(X15)
& X13 = X15
& ( in(X15,omega)
=> ! [X16] :
( element(X16,powerset(powerset(X15)))
=> ~ ( empty_set != X16
& ! [X17] :
~ ( in(X17,X16)
& ! [X18] :
( ( in(X18,X16)
& subset(X17,X18) )
=> X17 = X18 ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f48]) ).
fof(f60,plain,
? [X0] :
( ! [X1] :
? [X2] :
( in(X2,X1)
<~> ( in(X2,succ(X0))
& ? [X3] :
( ordinal(X3)
& X2 = X3
& ( ! [X4] :
( empty_set = X4
| ? [X5] :
( in(X5,X4)
& ! [X6] :
( X6 = X5
| ~ in(X6,X4)
| ~ subset(X5,X6) ) )
| ~ element(X4,powerset(powerset(X3))) )
| ~ in(X3,omega) ) ) ) )
& ordinal(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f61,plain,
? [X0] :
( ! [X1] :
? [X2] :
( in(X2,X1)
<~> ( in(X2,succ(X0))
& ? [X3] :
( ordinal(X3)
& X2 = X3
& ( ! [X4] :
( empty_set = X4
| ? [X5] :
( in(X5,X4)
& ! [X6] :
( X6 = X5
| ~ in(X6,X4)
| ~ subset(X5,X6) ) )
| ~ element(X4,powerset(powerset(X3))) )
| ~ in(X3,omega) ) ) ) )
& ordinal(X0) ),
inference(flattening,[],[f60]) ).
fof(f82,plain,
! [X0] :
( ? [X12] :
! [X13] :
( in(X13,X12)
<=> ? [X14] :
( in(X14,succ(X0))
& X13 = X14
& ? [X15] :
( ordinal(X15)
& X13 = X15
& ( ! [X16] :
( empty_set = X16
| ? [X17] :
( in(X17,X16)
& ! [X18] :
( X17 = X18
| ~ in(X18,X16)
| ~ subset(X17,X18) ) )
| ~ element(X16,powerset(powerset(X15))) )
| ~ in(X15,omega) ) ) ) )
| ? [X1,X2,X3] :
( X2 != X3
& X1 = X2
& ? [X4] :
( ordinal(X4)
& X2 = X4
& ( ! [X5] :
( empty_set = X5
| ? [X6] :
( in(X6,X5)
& ! [X7] :
( X7 = X6
| ~ in(X7,X5)
| ~ subset(X6,X7) ) )
| ~ element(X5,powerset(powerset(X4))) )
| ~ in(X4,omega) ) )
& X1 = X3
& ? [X8] :
( ordinal(X8)
& X3 = X8
& ( ! [X9] :
( empty_set = X9
| ? [X10] :
( in(X10,X9)
& ! [X11] :
( X11 = X10
| ~ in(X11,X9)
| ~ subset(X10,X11) ) )
| ~ element(X9,powerset(powerset(X8))) )
| ~ in(X8,omega) ) ) )
| ~ ordinal(X0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f83,plain,
! [X0] :
( ? [X12] :
! [X13] :
( in(X13,X12)
<=> ? [X14] :
( in(X14,succ(X0))
& X13 = X14
& ? [X15] :
( ordinal(X15)
& X13 = X15
& ( ! [X16] :
( empty_set = X16
| ? [X17] :
( in(X17,X16)
& ! [X18] :
( X17 = X18
| ~ in(X18,X16)
| ~ subset(X17,X18) ) )
| ~ element(X16,powerset(powerset(X15))) )
| ~ in(X15,omega) ) ) ) )
| ? [X1,X2,X3] :
( X2 != X3
& X1 = X2
& ? [X4] :
( ordinal(X4)
& X2 = X4
& ( ! [X5] :
( empty_set = X5
| ? [X6] :
( in(X6,X5)
& ! [X7] :
( X7 = X6
| ~ in(X7,X5)
| ~ subset(X6,X7) ) )
| ~ element(X5,powerset(powerset(X4))) )
| ~ in(X4,omega) ) )
& X1 = X3
& ? [X8] :
( ordinal(X8)
& X3 = X8
& ( ! [X9] :
( empty_set = X9
| ? [X10] :
( in(X10,X9)
& ! [X11] :
( X11 = X10
| ~ in(X11,X9)
| ~ subset(X10,X11) ) )
| ~ element(X9,powerset(powerset(X8))) )
| ~ in(X8,omega) ) ) )
| ~ ordinal(X0) ),
inference(flattening,[],[f82]) ).
fof(f84,definition,
! [X0,X2] :
( sP0(X0,X2)
<=> ( in(X2,succ(X0))
& ? [X3] :
( ordinal(X3)
& X2 = X3
& ( ! [X4] :
( empty_set = X4
| ? [X5] :
( in(X5,X4)
& ! [X6] :
( X6 = X5
| ~ in(X6,X4)
| ~ subset(X5,X6) ) )
| ~ element(X4,powerset(powerset(X3))) )
| ~ in(X3,omega) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f85,plain,
? [X0] :
( ! [X1] :
? [X2] :
( in(X2,X1)
<~> sP0(X0,X2) )
& ordinal(X0) ),
inference(definition_folding,[],[f61,f84]) ).
fof(f86,definition,
! [X3] :
( ? [X8] :
( ordinal(X8)
& X3 = X8
& ( ! [X9] :
( empty_set = X9
| ? [X10] :
( in(X10,X9)
& ! [X11] :
( X11 = X10
| ~ in(X11,X9)
| ~ subset(X10,X11) ) )
| ~ element(X9,powerset(powerset(X8))) )
| ~ in(X8,omega) ) )
| ~ sP1(X3) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f87,definition,
! [X0,X13] :
( sP2(X0,X13)
<=> ? [X14] :
( in(X14,succ(X0))
& X13 = X14
& ? [X15] :
( ordinal(X15)
& X13 = X15
& ( ! [X16] :
( empty_set = X16
| ? [X17] :
( in(X17,X16)
& ! [X18] :
( X17 = X18
| ~ in(X18,X16)
| ~ subset(X17,X18) ) )
| ~ element(X16,powerset(powerset(X15))) )
| ~ in(X15,omega) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f88,definition,
! [X0] :
( ? [X12] :
! [X13] :
( in(X13,X12)
<=> sP2(X0,X13) )
| ~ sP3(X0) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f89,plain,
! [X0] :
( sP3(X0)
| ? [X1,X2,X3] :
( X2 != X3
& X1 = X2
& ? [X4] :
( ordinal(X4)
& X2 = X4
& ( ! [X5] :
( empty_set = X5
| ? [X6] :
( in(X6,X5)
& ! [X7] :
( X7 = X6
| ~ in(X7,X5)
| ~ subset(X6,X7) ) )
| ~ element(X5,powerset(powerset(X4))) )
| ~ in(X4,omega) ) )
& X1 = X3
& sP1(X3) )
| ~ ordinal(X0) ),
inference(definition_folding,[],[f83,f88,f87,f86]) ).
fof(f90,plain,
! [X0,X2] :
( ( sP0(X0,X2)
| ~ in(X2,succ(X0))
| ! [X3] :
( ~ ordinal(X3)
| X2 != X3
| ( ? [X4] :
( empty_set != X4
& ! [X5] :
( ~ in(X5,X4)
| ? [X6] :
( X5 != X6
& in(X6,X4)
& subset(X5,X6) ) )
& element(X4,powerset(powerset(X3))) )
& in(X3,omega) ) ) )
& ( ( in(X2,succ(X0))
& ? [X3] :
( ordinal(X3)
& X2 = X3
& ( ! [X4] :
( empty_set = X4
| ? [X5] :
( in(X5,X4)
& ! [X6] :
( X6 = X5
| ~ in(X6,X4)
| ~ subset(X5,X6) ) )
| ~ element(X4,powerset(powerset(X3))) )
| ~ in(X3,omega) ) ) )
| ~ sP0(X0,X2) ) ),
inference(nnf_transformation,[],[f84]) ).
fof(f91,plain,
! [X0,X2] :
( ( sP0(X0,X2)
| ~ in(X2,succ(X0))
| ! [X3] :
( ~ ordinal(X3)
| X2 != X3
| ( ? [X4] :
( empty_set != X4
& ! [X5] :
( ~ in(X5,X4)
| ? [X6] :
( X5 != X6
& in(X6,X4)
& subset(X5,X6) ) )
& element(X4,powerset(powerset(X3))) )
& in(X3,omega) ) ) )
& ( ( in(X2,succ(X0))
& ? [X3] :
( ordinal(X3)
& X2 = X3
& ( ! [X4] :
( empty_set = X4
| ? [X5] :
( in(X5,X4)
& ! [X6] :
( X6 = X5
| ~ in(X6,X4)
| ~ subset(X5,X6) ) )
| ~ element(X4,powerset(powerset(X3))) )
| ~ in(X3,omega) ) ) )
| ~ sP0(X0,X2) ) ),
inference(flattening,[],[f90]) ).
fof(f92,plain,
! [X0,X1] :
( ( sP0(X0,X1)
| ~ in(X1,succ(X0))
| ! [X2] :
( ~ ordinal(X2)
| X1 != X2
| ( ? [X3] :
( empty_set != X3
& ! [X4] :
( ~ in(X4,X3)
| ? [X5] :
( X4 != X5
& in(X5,X3)
& subset(X4,X5) ) )
& element(X3,powerset(powerset(X2))) )
& in(X2,omega) ) ) )
& ( ( in(X1,succ(X0))
& ? [X6] :
( ordinal(X6)
& X1 = X6
& ( ! [X7] :
( empty_set = X7
| ? [X8] :
( in(X8,X7)
& ! [X9] :
( X8 = X9
| ~ in(X9,X7)
| ~ subset(X8,X9) ) )
| ~ element(X7,powerset(powerset(X6))) )
| ~ in(X6,omega) ) ) )
| ~ sP0(X0,X1) ) ),
inference(rectify,[],[f91]) ).
fof(f93,plain,
! [X0,X1] :
( ( sP0(X0,X1)
| ~ in(X1,succ(X0))
| ! [X2] :
( ~ ordinal(X2)
| X1 != X2
| ( empty_set != sK4(X2)
& ! [X4] :
( ~ in(X4,sK4(X2))
| ( sK5(X2,X4) != X4
& in(sK5(X2,X4),sK4(X2))
& subset(X4,sK5(X2,X4)) ) )
& element(sK4(X2),powerset(powerset(X2)))
& in(X2,omega) ) ) )
& ( ( in(X1,succ(X0))
& ordinal(sK6(X1))
& sK6(X1) = X1
& ( ! [X7] :
( empty_set = X7
| ( in(sK7(X7),X7)
& ! [X9] :
( sK7(X7) = X9
| ~ in(X9,X7)
| ~ subset(sK7(X7),X9) ) )
| ~ element(X7,powerset(powerset(sK6(X1)))) )
| ~ in(sK6(X1),omega) ) )
| ~ sP0(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6,sK7]),skolemize(X3,sK4(X2)),skolemize(X5,sK5(X2,X4)),skolemize(X6,sK6(X1)),skolemize(X8,sK7(X7))],[f92]) ).
fof(f94,plain,
? [X0] :
( ! [X1] :
? [X2] :
( ( ~ sP0(X0,X2)
| ~ in(X2,X1) )
& ( sP0(X0,X2)
| in(X2,X1) ) )
& ordinal(X0) ),
inference(nnf_transformation,[],[f85]) ).
fof(f95,plain,
( ! [X1] :
( ( ~ sP0(sK8,sK9(X1))
| ~ in(sK9(X1),X1) )
& ( sP0(sK8,sK9(X1))
| in(sK9(X1),X1) ) )
& ordinal(sK8) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X0,sK8),skolemize(X2,sK9(X1))],[f94]) ).
fof(f114,plain,
! [X0] :
( ? [X12] :
! [X13] :
( ( in(X13,X12)
| ~ sP2(X0,X13) )
& ( sP2(X0,X13)
| ~ in(X13,X12) ) )
| ~ sP3(X0) ),
inference(nnf_transformation,[],[f88]) ).
fof(f115,plain,
! [X0] :
( ? [X1] :
! [X2] :
( ( in(X2,X1)
| ~ sP2(X0,X2) )
& ( sP2(X0,X2)
| ~ in(X2,X1) ) )
| ~ sP3(X0) ),
inference(rectify,[],[f114]) ).
fof(f116,plain,
! [X0] :
( ! [X2] :
( ( in(X2,sK28(X0))
| ~ sP2(X0,X2) )
& ( sP2(X0,X2)
| ~ in(X2,sK28(X0)) ) )
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(X1,sK28(X0))],[f115]) ).
fof(f117,plain,
! [X0,X13] :
( ( sP2(X0,X13)
| ! [X14] :
( ~ in(X14,succ(X0))
| X13 != X14
| ! [X15] :
( ~ ordinal(X15)
| X13 != X15
| ( ? [X16] :
( empty_set != X16
& ! [X17] :
( ~ in(X17,X16)
| ? [X18] :
( X17 != X18
& in(X18,X16)
& subset(X17,X18) ) )
& element(X16,powerset(powerset(X15))) )
& in(X15,omega) ) ) ) )
& ( ? [X14] :
( in(X14,succ(X0))
& X13 = X14
& ? [X15] :
( ordinal(X15)
& X13 = X15
& ( ! [X16] :
( empty_set = X16
| ? [X17] :
( in(X17,X16)
& ! [X18] :
( X17 = X18
| ~ in(X18,X16)
| ~ subset(X17,X18) ) )
| ~ element(X16,powerset(powerset(X15))) )
| ~ in(X15,omega) ) ) )
| ~ sP2(X0,X13) ) ),
inference(nnf_transformation,[],[f87]) ).
fof(f118,plain,
! [X0,X1] :
( ( sP2(X0,X1)
| ! [X2] :
( ~ in(X2,succ(X0))
| X1 != X2
| ! [X3] :
( ~ ordinal(X3)
| X1 != X3
| ( ? [X4] :
( empty_set != X4
& ! [X5] :
( ~ in(X5,X4)
| ? [X6] :
( X5 != X6
& in(X6,X4)
& subset(X5,X6) ) )
& element(X4,powerset(powerset(X3))) )
& in(X3,omega) ) ) ) )
& ( ? [X7] :
( in(X7,succ(X0))
& X1 = X7
& ? [X8] :
( ordinal(X8)
& X1 = X8
& ( ! [X9] :
( empty_set = X9
| ? [X10] :
( in(X10,X9)
& ! [X11] :
( X10 = X11
| ~ in(X11,X9)
| ~ subset(X10,X11) ) )
| ~ element(X9,powerset(powerset(X8))) )
| ~ in(X8,omega) ) ) )
| ~ sP2(X0,X1) ) ),
inference(rectify,[],[f117]) ).
fof(f119,plain,
! [X0,X1] :
( ( sP2(X0,X1)
| ! [X2] :
( ~ in(X2,succ(X0))
| X1 != X2
| ! [X3] :
( ~ ordinal(X3)
| X1 != X3
| ( empty_set != sK29(X3)
& ! [X5] :
( ~ in(X5,sK29(X3))
| ( sK30(X3,X5) != X5
& in(sK30(X3,X5),sK29(X3))
& subset(X5,sK30(X3,X5)) ) )
& element(sK29(X3),powerset(powerset(X3)))
& in(X3,omega) ) ) ) )
& ( ( in(sK31(X0,X1),succ(X0))
& sK31(X0,X1) = X1
& ordinal(sK32(X1))
& sK32(X1) = X1
& ( ! [X9] :
( empty_set = X9
| ( in(sK33(X9),X9)
& ! [X11] :
( sK33(X9) = X11
| ~ in(X11,X9)
| ~ subset(sK33(X9),X11) ) )
| ~ element(X9,powerset(powerset(sK32(X1)))) )
| ~ in(sK32(X1),omega) ) )
| ~ sP2(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29,sK30,sK31,sK32,sK33]),skolemize(X4,sK29(X3)),skolemize(X6,sK30(X3,X5)),skolemize(X7,sK31(X0,X1)),skolemize(X8,sK32(X1)),skolemize(X10,sK33(X9))],[f118]) ).
fof(f123,plain,
! [X0] :
( sP3(X0)
| ( sK37 != sK38
& sK36 = sK37
& ordinal(sK39)
& sK37 = sK39
& ( ! [X5] :
( empty_set = X5
| ( in(sK40(X5),X5)
& ! [X7] :
( sK40(X5) = X7
| ~ in(X7,X5)
| ~ subset(sK40(X5),X7) ) )
| ~ element(X5,powerset(powerset(sK39))) )
| ~ in(sK39,omega) )
& sK36 = sK38
& sP1(sK38) )
| ~ ordinal(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36,sK37,sK38,sK39,sK40]),skolemize(X1,sK36),skolemize(X2,sK37),skolemize(X3,sK38),skolemize(X4,sK39),skolemize(X6,sK40(X5))],[f89]) ).
fof(f124,plain,
! [X0,X1,X9,X7] :
( ~ in(sK6(X1),omega)
| sK7(X7) = X9
| ~ in(X9,X7)
| ~ subset(sK7(X7),X9)
| ~ element(X7,powerset(powerset(sK6(X1))))
| empty_set = X7
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f93]) ).
fof(f125,plain,
! [X0,X1,X7] :
( ~ in(sK6(X1),omega)
| in(sK7(X7),X7)
| ~ element(X7,powerset(powerset(sK6(X1))))
| empty_set = X7
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f93]) ).
fof(f126,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| sK6(X1) = X1 ),
inference(cnf_transformation,[],[f93]) ).
fof(f127,plain,
! [X0,X1] :
( ordinal(sK6(X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f93]) ).
fof(f128,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| in(X1,succ(X0)) ),
inference(cnf_transformation,[],[f93]) ).
fof(f129,plain,
! [X2,X0,X1] :
( sP0(X0,X1)
| ~ in(X1,succ(X0))
| ~ ordinal(X2)
| X1 != X2
| in(X2,omega) ),
inference(cnf_transformation,[],[f93]) ).
fof(f130,plain,
! [X2,X0,X1] :
( sP0(X0,X1)
| ~ in(X1,succ(X0))
| ~ ordinal(X2)
| X1 != X2
| element(sK4(X2),powerset(powerset(X2))) ),
inference(cnf_transformation,[],[f93]) ).
fof(f131,plain,
! [X2,X0,X1,X4] :
( sP0(X0,X1)
| ~ in(X1,succ(X0))
| ~ ordinal(X2)
| X1 != X2
| ~ in(X4,sK4(X2))
| subset(X4,sK5(X2,X4)) ),
inference(cnf_transformation,[],[f93]) ).
fof(f132,plain,
! [X2,X0,X1,X4] :
( sP0(X0,X1)
| ~ in(X1,succ(X0))
| ~ ordinal(X2)
| X1 != X2
| ~ in(X4,sK4(X2))
| in(sK5(X2,X4),sK4(X2)) ),
inference(cnf_transformation,[],[f93]) ).
fof(f133,plain,
! [X2,X0,X1,X4] :
( sP0(X0,X1)
| ~ in(X1,succ(X0))
| ~ ordinal(X2)
| X1 != X2
| ~ in(X4,sK4(X2))
| sK5(X2,X4) != X4 ),
inference(cnf_transformation,[],[f93]) ).
fof(f134,plain,
! [X2,X0,X1] :
( sP0(X0,X1)
| ~ in(X1,succ(X0))
| ~ ordinal(X2)
| X1 != X2
| empty_set != sK4(X2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f135,plain,
ordinal(sK8),
inference(cnf_transformation,[],[f95]) ).
fof(f136,plain,
! [X1] :
( sP0(sK8,sK9(X1))
| in(sK9(X1),X1) ),
inference(cnf_transformation,[],[f95]) ).
fof(f137,plain,
! [X1] :
( ~ in(sK9(X1),X1)
| ~ sP0(sK8,sK9(X1)) ),
inference(cnf_transformation,[],[f95]) ).
fof(f241,plain,
! [X2,X0] :
( ~ in(X2,sK28(X0))
| sP2(X0,X2)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f242,plain,
! [X2,X0] :
( ~ sP2(X0,X2)
| in(X2,sK28(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f243,plain,
! [X0,X11,X1,X9] :
( ~ in(sK32(X1),omega)
| sK33(X9) = X11
| ~ in(X11,X9)
| ~ subset(sK33(X9),X11)
| ~ element(X9,powerset(powerset(sK32(X1))))
| empty_set = X9
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f244,plain,
! [X0,X1,X9] :
( ~ in(sK32(X1),omega)
| in(sK33(X9),X9)
| ~ element(X9,powerset(powerset(sK32(X1))))
| empty_set = X9
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f245,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| sK32(X1) = X1 ),
inference(cnf_transformation,[],[f119]) ).
fof(f246,plain,
! [X0,X1] :
( ordinal(sK32(X1))
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f247,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| sK31(X0,X1) = X1 ),
inference(cnf_transformation,[],[f119]) ).
fof(f248,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| in(sK31(X0,X1),succ(X0)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f249,plain,
! [X2,X3,X0,X1] :
( sP2(X0,X1)
| ~ in(X2,succ(X0))
| X1 != X2
| ~ ordinal(X3)
| X1 != X3
| in(X3,omega) ),
inference(cnf_transformation,[],[f119]) ).
fof(f250,plain,
! [X2,X3,X0,X1] :
( sP2(X0,X1)
| ~ in(X2,succ(X0))
| X1 != X2
| ~ ordinal(X3)
| X1 != X3
| element(sK29(X3),powerset(powerset(X3))) ),
inference(cnf_transformation,[],[f119]) ).
fof(f251,plain,
! [X2,X3,X0,X1,X5] :
( sP2(X0,X1)
| ~ in(X2,succ(X0))
| X1 != X2
| ~ ordinal(X3)
| X1 != X3
| ~ in(X5,sK29(X3))
| subset(X5,sK30(X3,X5)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f252,plain,
! [X2,X3,X0,X1,X5] :
( sP2(X0,X1)
| ~ in(X2,succ(X0))
| X1 != X2
| ~ ordinal(X3)
| X1 != X3
| ~ in(X5,sK29(X3))
| in(sK30(X3,X5),sK29(X3)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f253,plain,
! [X2,X3,X0,X1,X5] :
( sP2(X0,X1)
| ~ in(X2,succ(X0))
| X1 != X2
| ~ ordinal(X3)
| X1 != X3
| ~ in(X5,sK29(X3))
| sK30(X3,X5) != X5 ),
inference(cnf_transformation,[],[f119]) ).
fof(f254,plain,
! [X2,X3,X0,X1] :
( sP2(X0,X1)
| ~ in(X2,succ(X0))
| X1 != X2
| ~ ordinal(X3)
| X1 != X3
| empty_set != sK29(X3) ),
inference(cnf_transformation,[],[f119]) ).
fof(f260,plain,
! [X0] :
( sP3(X0)
| sK36 = sK38
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f265,plain,
! [X0] :
( sP3(X0)
| sK36 = sK37
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f266,plain,
! [X0] :
( sP3(X0)
| sK37 != sK38
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f267,plain,
! [X2,X0] :
( empty_set != sK4(X2)
| ~ in(X2,succ(X0))
| ~ ordinal(X2)
| sP0(X0,X2) ),
inference(equality_resolution,[],[f134]) ).
fof(f268,plain,
! [X2,X0,X4] :
( ~ in(X4,sK4(X2))
| ~ in(X2,succ(X0))
| ~ ordinal(X2)
| sP0(X0,X2)
| sK5(X2,X4) != X4 ),
inference(equality_resolution,[],[f133]) ).
fof(f269,plain,
! [X2,X0,X4] :
( ~ in(X4,sK4(X2))
| ~ in(X2,succ(X0))
| ~ ordinal(X2)
| sP0(X0,X2)
| in(sK5(X2,X4),sK4(X2)) ),
inference(equality_resolution,[],[f132]) ).
fof(f270,plain,
! [X2,X0,X4] :
( subset(X4,sK5(X2,X4))
| ~ in(X2,succ(X0))
| ~ ordinal(X2)
| ~ in(X4,sK4(X2))
| sP0(X0,X2) ),
inference(equality_resolution,[],[f131]) ).
fof(f271,plain,
! [X2,X0] :
( element(sK4(X2),powerset(powerset(X2)))
| ~ in(X2,succ(X0))
| ~ ordinal(X2)
| sP0(X0,X2) ),
inference(equality_resolution,[],[f130]) ).
fof(f272,plain,
! [X2,X0] :
( ~ in(X2,succ(X0))
| sP0(X0,X2)
| ~ ordinal(X2)
| in(X2,omega) ),
inference(equality_resolution,[],[f129]) ).
fof(f273,plain,
! [X2,X3,X0] :
( sP2(X0,X2)
| ~ in(X2,succ(X0))
| ~ ordinal(X3)
| X2 != X3
| empty_set != sK29(X3) ),
inference(equality_resolution,[],[f254]) ).
fof(f274,plain,
! [X3,X0] :
( empty_set != sK29(X3)
| ~ in(X3,succ(X0))
| ~ ordinal(X3)
| sP2(X0,X3) ),
inference(equality_resolution,[],[f273]) ).
fof(f275,plain,
! [X2,X3,X0,X5] :
( sP2(X0,X2)
| ~ in(X2,succ(X0))
| ~ ordinal(X3)
| X2 != X3
| ~ in(X5,sK29(X3))
| sK30(X3,X5) != X5 ),
inference(equality_resolution,[],[f253]) ).
fof(f276,plain,
! [X3,X0,X5] :
( ~ in(X5,sK29(X3))
| ~ in(X3,succ(X0))
| ~ ordinal(X3)
| sP2(X0,X3)
| sK30(X3,X5) != X5 ),
inference(equality_resolution,[],[f275]) ).
fof(f277,plain,
! [X2,X3,X0,X5] :
( sP2(X0,X2)
| ~ in(X2,succ(X0))
| ~ ordinal(X3)
| X2 != X3
| ~ in(X5,sK29(X3))
| in(sK30(X3,X5),sK29(X3)) ),
inference(equality_resolution,[],[f252]) ).
fof(f278,plain,
! [X3,X0,X5] :
( ~ in(X5,sK29(X3))
| ~ in(X3,succ(X0))
| ~ ordinal(X3)
| sP2(X0,X3)
| in(sK30(X3,X5),sK29(X3)) ),
inference(equality_resolution,[],[f277]) ).
fof(f279,plain,
! [X2,X3,X0,X5] :
( sP2(X0,X2)
| ~ in(X2,succ(X0))
| ~ ordinal(X3)
| X2 != X3
| ~ in(X5,sK29(X3))
| subset(X5,sK30(X3,X5)) ),
inference(equality_resolution,[],[f251]) ).
fof(f280,plain,
! [X3,X0,X5] :
( subset(X5,sK30(X3,X5))
| ~ in(X3,succ(X0))
| ~ ordinal(X3)
| ~ in(X5,sK29(X3))
| sP2(X0,X3) ),
inference(equality_resolution,[],[f279]) ).
fof(f281,plain,
! [X2,X3,X0] :
( sP2(X0,X2)
| ~ in(X2,succ(X0))
| ~ ordinal(X3)
| X2 != X3
| element(sK29(X3),powerset(powerset(X3))) ),
inference(equality_resolution,[],[f250]) ).
fof(f282,plain,
! [X3,X0] :
( element(sK29(X3),powerset(powerset(X3)))
| ~ in(X3,succ(X0))
| ~ ordinal(X3)
| sP2(X0,X3) ),
inference(equality_resolution,[],[f281]) ).
fof(f283,plain,
! [X2,X3,X0] :
( sP2(X0,X2)
| ~ in(X2,succ(X0))
| ~ ordinal(X3)
| X2 != X3
| in(X3,omega) ),
inference(equality_resolution,[],[f249]) ).
fof(f284,plain,
! [X3,X0] :
( ~ in(X3,succ(X0))
| sP2(X0,X3)
| ~ ordinal(X3)
| in(X3,omega) ),
inference(equality_resolution,[],[f283]) ).
fof(f290,definition,
( spl41_2
<=> ! [X0] :
( sP3(X0)
| ~ ordinal(X0) ) ),
introduced(definition,[new_symbols(definition,[spl41_2])],[avatar_definition]) ).
fof(f291,plain,
( ! [X0] :
( sP3(X0)
| ~ ordinal(X0) )
| ~ spl41_2 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f294,definition,
( spl41_3
<=> sK36 = sK38 ),
introduced(definition,[new_symbols(definition,[spl41_3])],[avatar_definition]) ).
fof(f296,plain,
( sK36 = sK38
| ~ spl41_3 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f297,plain,
( spl41_3
| spl41_2 ),
inference(avatar_split_clause,[],[f260,f290,f294]) ).
fof(f321,definition,
( spl41_9
<=> sK36 = sK37 ),
introduced(definition,[new_symbols(definition,[spl41_9])],[avatar_definition]) ).
fof(f323,plain,
( sK36 = sK37
| ~ spl41_9 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f324,plain,
( spl41_9
| spl41_2 ),
inference(avatar_split_clause,[],[f265,f290,f321]) ).
fof(f326,definition,
( spl41_10
<=> sK37 = sK38 ),
introduced(definition,[new_symbols(definition,[spl41_10])],[avatar_definition]) ).
fof(f329,plain,
( ~ spl41_10
| spl41_2 ),
inference(avatar_split_clause,[],[f266,f290,f326]) ).
fof(f332,plain,
! [X0] :
( sK9(X0) = sK6(sK9(X0))
| in(sK9(X0),X0) ),
inference(resolution,[],[f126,f136]) ).
fof(f333,plain,
! [X0] :
( in(sK9(X0),succ(sK8))
| in(sK9(X0),X0) ),
inference(resolution,[],[f128,f136]) ).
fof(f340,plain,
! [X0,X1] :
( ordinal(sK9(X0))
| ~ sP0(X1,sK9(X0))
| in(sK9(X0),X0) ),
inference(superposition,[],[f127,f332]) ).
fof(f365,plain,
! [X0] :
( in(sK9(X0),omega)
| ~ ordinal(sK9(X0))
| sP2(sK8,sK9(X0))
| in(sK9(X0),X0) ),
inference(resolution,[],[f284,f333]) ).
fof(f388,plain,
! [X2,X0,X1] :
( ~ sP0(X2,sK9(X0))
| in(sK7(X1),X1)
| ~ element(X1,powerset(powerset(sK9(X0))))
| empty_set = X1
| ~ in(sK9(X0),omega)
| in(sK9(X0),X0) ),
inference(superposition,[],[f125,f332]) ).
fof(f389,plain,
! [X0,X1] :
( in(sK7(X0),X0)
| ~ element(X0,powerset(powerset(sK9(X1))))
| empty_set = X0
| ~ in(sK9(X1),omega)
| in(sK9(X1),X1)
| in(sK9(X1),X1) ),
inference(resolution,[],[f388,f136]) ).
fof(f390,plain,
! [X0,X1] :
( ~ in(sK9(X1),omega)
| ~ element(X0,powerset(powerset(sK9(X1))))
| empty_set = X0
| in(sK7(X0),X0)
| in(sK9(X1),X1) ),
inference(duplicate_literal_removal,[],[f389]) ).
fof(f400,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(sK9(X1))))
| empty_set = X0
| in(sK7(X0),X0)
| in(sK9(X1),X1)
| ~ ordinal(sK9(X1))
| sP2(sK8,sK9(X1))
| in(sK9(X1),X1) ),
inference(resolution,[],[f390,f365]) ).
fof(f402,plain,
! [X0,X1] :
( sP2(sK8,sK9(X1))
| empty_set = X0
| in(sK7(X0),X0)
| in(sK9(X1),X1)
| ~ ordinal(sK9(X1))
| ~ element(X0,powerset(powerset(sK9(X1)))) ),
inference(duplicate_literal_removal,[],[f400]) ).
fof(f404,plain,
! [X2,X3,X0,X1] :
( ~ sP0(X3,sK9(X0))
| sK7(X1) = X2
| ~ in(X2,X1)
| ~ subset(sK7(X1),X2)
| ~ element(X1,powerset(powerset(sK9(X0))))
| empty_set = X1
| ~ in(sK9(X0),omega)
| in(sK9(X0),X0) ),
inference(superposition,[],[f124,f332]) ).
fof(f410,plain,
! [X0,X1] :
( empty_set = X0
| in(sK7(X0),X0)
| in(sK9(X1),X1)
| ~ ordinal(sK9(X1))
| ~ element(X0,powerset(powerset(sK9(X1))))
| in(sK9(X1),sK28(sK8))
| ~ sP3(sK8) ),
inference(resolution,[],[f402,f242]) ).
fof(f414,definition,
( spl41_20
<=> sP3(sK8) ),
introduced(definition,[new_symbols(definition,[spl41_20])],[avatar_definition]) ).
fof(f415,plain,
( sP3(sK8)
| ~ spl41_20 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f416,plain,
( ~ sP3(sK8)
| spl41_20 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f418,definition,
( spl41_21
<=> ! [X0,X1] :
( empty_set = X0
| in(sK9(X1),sK28(sK8))
| ~ element(X0,powerset(powerset(sK9(X1))))
| in(sK9(X1),X1)
| ~ ordinal(sK9(X1))
| in(sK7(X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl41_21])],[avatar_definition]) ).
fof(f419,plain,
( ! [X0,X1] :
( in(sK9(X1),sK28(sK8))
| empty_set = X0
| ~ element(X0,powerset(powerset(sK9(X1))))
| in(sK9(X1),X1)
| ~ ordinal(sK9(X1))
| in(sK7(X0),X0) )
| ~ spl41_21 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f420,plain,
( ~ spl41_20
| spl41_21 ),
inference(avatar_split_clause,[],[f410,f418,f414]) ).
fof(f426,plain,
( ~ ordinal(sK8)
| ~ spl41_2
| spl41_20 ),
inference(resolution,[],[f416,f291]) ).
fof(f427,plain,
( $false
| ~ spl41_2
| spl41_20 ),
inference(forward_subsumption_resolution,[],[f426,f135]) ).
fof(f428,plain,
( ~ spl41_2
| spl41_20 ),
inference(avatar_contradiction_clause,[],[f427]) ).
fof(f455,definition,
( spl41_23
<=> sP0(sK8,sK9(sK28(sK8))) ),
introduced(definition,[new_symbols(definition,[spl41_23])],[avatar_definition]) ).
fof(f457,plain,
( ~ sP0(sK8,sK9(sK28(sK8)))
| spl41_23 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f459,definition,
( spl41_24
<=> ! [X0] :
( empty_set = X0
| in(sK7(X0),X0)
| ~ element(X0,powerset(powerset(sK9(sK28(sK8))))) ) ),
introduced(definition,[new_symbols(definition,[spl41_24])],[avatar_definition]) ).
fof(f460,plain,
( ! [X0] :
( ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| in(sK7(X0),X0)
| empty_set = X0 )
| ~ spl41_24 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f462,plain,
( in(sK9(sK28(sK8)),sK28(sK8))
| spl41_23 ),
inference(resolution,[],[f457,f136]) ).
fof(f465,plain,
( sP2(sK8,sK9(sK28(sK8)))
| ~ sP3(sK8)
| spl41_23 ),
inference(resolution,[],[f462,f241]) ).
fof(f467,plain,
( sP2(sK8,sK9(sK28(sK8)))
| ~ spl41_20
| spl41_23 ),
inference(forward_subsumption_resolution,[],[f465,f415]) ).
fof(f471,plain,
( sK9(sK28(sK8)) = sK32(sK9(sK28(sK8)))
| ~ spl41_20
| spl41_23 ),
inference(resolution,[],[f467,f245]) ).
fof(f472,plain,
! [X2,X0,X1] :
( sK7(X0) = X1
| ~ in(X1,X0)
| ~ subset(sK7(X0),X1)
| ~ element(X0,powerset(powerset(sK9(X2))))
| empty_set = X0
| ~ in(sK9(X2),omega)
| in(sK9(X2),X2)
| in(sK9(X2),X2) ),
inference(resolution,[],[f404,f136]) ).
fof(f473,plain,
! [X2,X0,X1] :
( ~ in(sK9(X2),omega)
| ~ in(X1,X0)
| ~ subset(sK7(X0),X1)
| ~ element(X0,powerset(powerset(sK9(X2))))
| empty_set = X0
| sK7(X0) = X1
| in(sK9(X2),X2) ),
inference(duplicate_literal_removal,[],[f472]) ).
fof(f495,plain,
! [X2,X0,X1] :
( ~ in(X0,X1)
| ~ subset(sK7(X1),X0)
| ~ element(X1,powerset(powerset(sK9(X2))))
| empty_set = X1
| sK7(X1) = X0
| in(sK9(X2),X2)
| ~ ordinal(sK9(X2))
| sP2(sK8,sK9(X2))
| in(sK9(X2),X2) ),
inference(resolution,[],[f473,f365]) ).
fof(f498,plain,
! [X2,X0,X1] :
( ~ subset(sK7(X1),X0)
| ~ in(X0,X1)
| ~ element(X1,powerset(powerset(sK9(X2))))
| empty_set = X1
| sK7(X1) = X0
| in(sK9(X2),X2)
| ~ ordinal(sK9(X2))
| sP2(sK8,sK9(X2)) ),
inference(duplicate_literal_removal,[],[f495]) ).
fof(f514,plain,
! [X2,X3,X0,X1] :
( ~ in(sK30(X0,sK7(X1)),X1)
| ~ element(X1,powerset(powerset(sK9(X2))))
| empty_set = X1
| sK7(X1) = sK30(X0,sK7(X1))
| in(sK9(X2),X2)
| ~ ordinal(sK9(X2))
| sP2(sK8,sK9(X2))
| ~ in(X0,succ(X3))
| ~ ordinal(X0)
| ~ in(sK7(X1),sK29(X0))
| sP2(X3,X0) ),
inference(resolution,[],[f498,f280]) ).
fof(f515,plain,
! [X2,X3,X0,X1] :
( ~ in(sK7(X1),sK29(X0))
| ~ element(X1,powerset(powerset(sK9(X2))))
| empty_set = X1
| in(sK9(X2),X2)
| ~ ordinal(sK9(X2))
| sP2(sK8,sK9(X2))
| ~ in(X0,succ(X3))
| ~ ordinal(X0)
| ~ in(sK30(X0,sK7(X1)),X1)
| sP2(X3,X0) ),
inference(forward_subsumption_resolution,[],[f514,f276]) ).
fof(f530,plain,
( ! [X2,X0,X1] :
( ~ in(sK9(sK28(sK8)),omega)
| sK33(X0) = X1
| ~ in(X1,X0)
| ~ subset(sK33(X0),X1)
| ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| empty_set = X0
| ~ sP2(X2,sK9(sK28(sK8))) )
| ~ spl41_20
| spl41_23 ),
inference(superposition,[],[f243,f471]) ).
fof(f532,plain,
( ! [X0] :
( ordinal(sK9(sK28(sK8)))
| ~ sP2(X0,sK9(sK28(sK8))) )
| ~ spl41_20
| spl41_23 ),
inference(superposition,[],[f246,f471]) ).
fof(f534,definition,
( spl41_31
<=> ! [X0] : ~ sP2(X0,sK9(sK28(sK8))) ),
introduced(definition,[new_symbols(definition,[spl41_31])],[avatar_definition]) ).
fof(f535,plain,
( ! [X0] : ~ sP2(X0,sK9(sK28(sK8)))
| ~ spl41_31 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f537,definition,
( spl41_32
<=> ordinal(sK9(sK28(sK8))) ),
introduced(definition,[new_symbols(definition,[spl41_32])],[avatar_definition]) ).
fof(f538,plain,
( ~ ordinal(sK9(sK28(sK8)))
| spl41_32 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f539,plain,
( ordinal(sK9(sK28(sK8)))
| ~ spl41_32 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f540,plain,
( spl41_31
| spl41_32
| ~ spl41_20
| spl41_23 ),
inference(avatar_split_clause,[],[f532,f455,f414,f537,f534]) ).
fof(f542,definition,
( spl41_33
<=> ! [X0] :
( in(sK33(X0),X0)
| empty_set = X0
| ~ element(X0,powerset(powerset(sK9(sK28(sK8))))) ) ),
introduced(definition,[new_symbols(definition,[spl41_33])],[avatar_definition]) ).
fof(f543,plain,
( ! [X0] :
( ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| empty_set = X0
| in(sK33(X0),X0) )
| ~ spl41_33 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f545,definition,
( spl41_34
<=> in(sK9(sK28(sK8)),omega) ),
introduced(definition,[new_symbols(definition,[spl41_34])],[avatar_definition]) ).
fof(f550,definition,
( spl41_35
<=> ! [X0,X1] :
( sK33(X0) = X1
| empty_set = X0
| ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| ~ subset(sK33(X0),X1)
| ~ in(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl41_35])],[avatar_definition]) ).
fof(f551,plain,
( ! [X0,X1] :
( ~ subset(sK33(X0),X1)
| empty_set = X0
| ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| sK33(X0) = X1
| ~ in(X1,X0) )
| ~ spl41_35 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f552,plain,
( spl41_31
| spl41_35
| ~ spl41_34
| ~ spl41_20
| spl41_23 ),
inference(avatar_split_clause,[],[f530,f455,f414,f545,f550,f534]) ).
fof(f579,definition,
( spl41_39
<=> sP2(sK8,sK9(sK28(sK8))) ),
introduced(definition,[new_symbols(definition,[spl41_39])],[avatar_definition]) ).
fof(f580,plain,
( ~ sP2(sK8,sK9(sK28(sK8)))
| spl41_39 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f581,plain,
( sP2(sK8,sK9(sK28(sK8)))
| ~ spl41_39 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f597,definition,
( spl41_42
<=> in(sK9(sK28(sK8)),sK28(sK8)) ),
introduced(definition,[new_symbols(definition,[spl41_42])],[avatar_definition]) ).
fof(f598,plain,
( ~ in(sK9(sK28(sK8)),sK28(sK8))
| spl41_42 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f599,plain,
( in(sK9(sK28(sK8)),sK28(sK8))
| ~ spl41_42 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f601,definition,
( spl41_43
<=> ! [X0] : ~ sP0(X0,sK9(sK28(sK8))) ),
introduced(definition,[new_symbols(definition,[spl41_43])],[avatar_definition]) ).
fof(f602,plain,
( ! [X0] : ~ sP0(X0,sK9(sK28(sK8)))
| ~ spl41_43 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f604,plain,
( spl41_39
| ~ spl41_20
| spl41_23 ),
inference(avatar_split_clause,[],[f467,f455,f414,f579]) ).
fof(f612,definition,
( spl41_44
<=> sK9(sK28(sK8)) = sK32(sK9(sK28(sK8))) ),
introduced(definition,[new_symbols(definition,[spl41_44])],[avatar_definition]) ).
fof(f614,plain,
( sK9(sK28(sK8)) = sK32(sK9(sK28(sK8)))
| ~ spl41_44 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f617,definition,
( spl41_45
<=> sK9(sK28(sK8)) = sK31(sK8,sK9(sK28(sK8))) ),
introduced(definition,[new_symbols(definition,[spl41_45])],[avatar_definition]) ).
fof(f619,plain,
( sK9(sK28(sK8)) = sK31(sK8,sK9(sK28(sK8)))
| ~ spl41_45 ),
inference(avatar_component_clause,[],[f617]) ).
fof(f670,definition,
( spl41_54
<=> ! [X0] :
( ~ in(sK9(sK28(sK8)),succ(X0))
| sP2(X0,sK9(sK28(sK8))) ) ),
introduced(definition,[new_symbols(definition,[spl41_54])],[avatar_definition]) ).
fof(f671,plain,
( ! [X0] :
( ~ in(sK9(sK28(sK8)),succ(X0))
| sP2(X0,sK9(sK28(sK8))) )
| ~ spl41_54 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f673,definition,
( spl41_55
<=> in(sK7(sK29(sK9(sK28(sK8)))),sK29(sK9(sK28(sK8)))) ),
introduced(definition,[new_symbols(definition,[spl41_55])],[avatar_definition]) ).
fof(f675,plain,
( in(sK7(sK29(sK9(sK28(sK8)))),sK29(sK9(sK28(sK8))))
| ~ spl41_55 ),
inference(avatar_component_clause,[],[f673]) ).
fof(f678,definition,
( spl41_56
<=> ! [X0] :
( ~ in(sK9(sK28(sK8)),succ(X0))
| sP0(X0,sK9(sK28(sK8))) ) ),
introduced(definition,[new_symbols(definition,[spl41_56])],[avatar_definition]) ).
fof(f679,plain,
( ! [X0] :
( ~ in(sK9(sK28(sK8)),succ(X0))
| sP0(X0,sK9(sK28(sK8))) )
| ~ spl41_56 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f688,plain,
( in(sK9(sK28(sK8)),sK28(sK8))
| ~ sP3(sK8)
| ~ spl41_39 ),
inference(resolution,[],[f581,f242]) ).
fof(f689,plain,
( sK9(sK28(sK8)) = sK31(sK8,sK9(sK28(sK8)))
| ~ spl41_39 ),
inference(resolution,[],[f581,f247]) ).
fof(f690,plain,
( sK9(sK28(sK8)) = sK32(sK9(sK28(sK8)))
| ~ spl41_39 ),
inference(resolution,[],[f581,f245]) ).
fof(f691,plain,
( spl41_44
| ~ spl41_39 ),
inference(avatar_split_clause,[],[f690,f579,f612]) ).
fof(f692,plain,
( spl41_45
| ~ spl41_39 ),
inference(avatar_split_clause,[],[f689,f579,f617]) ).
fof(f693,plain,
( in(sK9(sK28(sK8)),sK28(sK8))
| ~ spl41_20
| ~ spl41_39 ),
inference(forward_subsumption_resolution,[],[f688,f415]) ).
fof(f694,plain,
( spl41_42
| ~ spl41_20
| ~ spl41_39 ),
inference(avatar_split_clause,[],[f693,f579,f414,f597]) ).
fof(f711,plain,
( ~ sP0(sK8,sK9(sK28(sK8)))
| ~ spl41_42 ),
inference(resolution,[],[f599,f137]) ).
fof(f714,plain,
( ~ spl41_23
| ~ spl41_42 ),
inference(avatar_split_clause,[],[f711,f597,f455]) ).
fof(f718,plain,
( ! [X0] :
( ~ sP0(X0,sK9(sK28(sK8)))
| in(sK9(sK28(sK8)),sK28(sK8)) )
| spl41_32 ),
inference(resolution,[],[f538,f340]) ).
fof(f723,plain,
( spl41_42
| spl41_43
| spl41_32 ),
inference(avatar_split_clause,[],[f718,f537,f601,f597]) ).
fof(f732,plain,
( $false
| ~ spl41_20
| spl41_23
| ~ spl41_31 ),
inference(forward_subsumption_resolution,[],[f467,f535]) ).
fof(f733,plain,
( ~ spl41_20
| spl41_23
| ~ spl41_31 ),
inference(avatar_contradiction_clause,[],[f732]) ).
fof(f743,plain,
( sK37 = sK38
| ~ spl41_3
| ~ spl41_9 ),
inference(superposition,[],[f296,f323]) ).
fof(f744,plain,
( spl41_10
| ~ spl41_3
| ~ spl41_9 ),
inference(avatar_split_clause,[],[f743,f321,f294,f326]) ).
fof(f747,plain,
( in(sK31(sK8,sK9(sK28(sK8))),succ(sK8))
| ~ spl41_39 ),
inference(resolution,[],[f581,f248]) ).
fof(f755,plain,
( in(sK9(sK28(sK8)),sK28(sK8))
| ~ spl41_43 ),
inference(resolution,[],[f602,f136]) ).
fof(f756,plain,
( spl41_42
| ~ spl41_43 ),
inference(avatar_split_clause,[],[f755,f601,f597]) ).
fof(f794,plain,
( sP0(sK8,sK31(sK8,sK9(sK28(sK8))))
| ~ ordinal(sK31(sK8,sK9(sK28(sK8))))
| in(sK31(sK8,sK9(sK28(sK8))),omega)
| ~ spl41_39 ),
inference(resolution,[],[f747,f272]) ).
fof(f796,plain,
( ! [X0] :
( empty_set = X0
| ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| in(sK9(sK28(sK8)),sK28(sK8))
| ~ ordinal(sK9(sK28(sK8)))
| in(sK7(X0),X0)
| ~ sP0(sK8,sK9(sK28(sK8))) )
| ~ spl41_21 ),
inference(resolution,[],[f419,f137]) ).
fof(f799,plain,
( ! [X0] :
( empty_set = X0
| ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| in(sK9(sK28(sK8)),sK28(sK8))
| in(sK7(X0),X0)
| ~ sP0(sK8,sK9(sK28(sK8))) )
| ~ spl41_21 ),
inference(forward_subsumption_resolution,[],[f796,f340]) ).
fof(f802,plain,
( ! [X0,X1] :
( ~ in(sK9(sK28(sK8)),omega)
| in(sK33(X0),X0)
| ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| empty_set = X0
| ~ sP2(X1,sK9(sK28(sK8))) )
| ~ spl41_44 ),
inference(superposition,[],[f244,f614]) ).
fof(f809,plain,
( in(sK9(sK28(sK8)),succ(sK8))
| ~ spl41_39
| ~ spl41_45 ),
inference(superposition,[],[f747,f619]) ).
fof(f819,plain,
( sP0(sK8,sK9(sK28(sK8)))
| ~ ordinal(sK31(sK8,sK9(sK28(sK8))))
| in(sK31(sK8,sK9(sK28(sK8))),omega)
| ~ spl41_39
| ~ spl41_45 ),
inference(forward_demodulation,[],[f794,f619]) ).
fof(f825,plain,
( ~ ordinal(sK31(sK8,sK9(sK28(sK8))))
| in(sK31(sK8,sK9(sK28(sK8))),omega)
| spl41_23
| ~ spl41_39
| ~ spl41_45 ),
inference(forward_subsumption_resolution,[],[f819,f457]) ).
fof(f826,plain,
( ~ ordinal(sK9(sK28(sK8)))
| in(sK31(sK8,sK9(sK28(sK8))),omega)
| spl41_23
| ~ spl41_39
| ~ spl41_45 ),
inference(forward_demodulation,[],[f825,f619]) ).
fof(f827,plain,
( in(sK31(sK8,sK9(sK28(sK8))),omega)
| spl41_23
| ~ spl41_32
| ~ spl41_39
| ~ spl41_45 ),
inference(forward_subsumption_resolution,[],[f826,f539]) ).
fof(f828,plain,
( in(sK9(sK28(sK8)),omega)
| spl41_23
| ~ spl41_32
| ~ spl41_39
| ~ spl41_45 ),
inference(forward_demodulation,[],[f827,f619]) ).
fof(f832,plain,
( spl41_31
| spl41_33
| ~ spl41_34
| ~ spl41_44 ),
inference(avatar_split_clause,[],[f802,f612,f545,f542,f534]) ).
fof(f836,plain,
( spl41_34
| spl41_23
| ~ spl41_32
| ~ spl41_39
| ~ spl41_45 ),
inference(avatar_split_clause,[],[f828,f617,f579,f537,f455,f545]) ).
fof(f866,plain,
( ! [X0] :
( empty_set = sK4(sK9(sK28(sK8)))
| in(sK33(sK4(sK9(sK28(sK8)))),sK4(sK9(sK28(sK8))))
| ~ in(sK9(sK28(sK8)),succ(X0))
| ~ ordinal(sK9(sK28(sK8)))
| sP0(X0,sK9(sK28(sK8))) )
| ~ spl41_33 ),
inference(resolution,[],[f543,f271]) ).
fof(f885,plain,
( ! [X0] :
( in(sK33(sK4(sK9(sK28(sK8)))),sK4(sK9(sK28(sK8))))
| ~ in(sK9(sK28(sK8)),succ(X0))
| ~ ordinal(sK9(sK28(sK8)))
| sP0(X0,sK9(sK28(sK8))) )
| ~ spl41_33 ),
inference(forward_subsumption_resolution,[],[f866,f267]) ).
fof(f897,plain,
( ! [X0] :
( in(sK33(sK4(sK9(sK28(sK8)))),sK4(sK9(sK28(sK8))))
| ~ in(sK9(sK28(sK8)),succ(X0))
| sP0(X0,sK9(sK28(sK8))) )
| ~ spl41_32
| ~ spl41_33 ),
inference(forward_subsumption_resolution,[],[f885,f539]) ).
fof(f908,definition,
( spl41_71
<=> in(sK33(sK4(sK9(sK28(sK8)))),sK4(sK9(sK28(sK8)))) ),
introduced(definition,[new_symbols(definition,[spl41_71])],[avatar_definition]) ).
fof(f910,plain,
( in(sK33(sK4(sK9(sK28(sK8)))),sK4(sK9(sK28(sK8))))
| ~ spl41_71 ),
inference(avatar_component_clause,[],[f908]) ).
fof(f966,definition,
( spl41_75
<=> in(sK5(sK9(sK28(sK8)),sK33(sK4(sK9(sK28(sK8))))),sK4(sK9(sK28(sK8)))) ),
introduced(definition,[new_symbols(definition,[spl41_75])],[avatar_definition]) ).
fof(f1077,plain,
( ! [X2,X0,X1] :
( empty_set = X0
| ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| sK33(X0) = sK5(X1,sK33(X0))
| ~ in(sK5(X1,sK33(X0)),X0)
| ~ in(X1,succ(X2))
| ~ ordinal(X1)
| ~ in(sK33(X0),sK4(X1))
| sP0(X2,X1) )
| ~ spl41_35 ),
inference(resolution,[],[f551,f270]) ).
fof(f1080,plain,
( ! [X2,X0,X1] :
( ~ in(sK33(X0),sK4(X1))
| ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| ~ in(sK5(X1,sK33(X0)),X0)
| ~ in(X1,succ(X2))
| ~ ordinal(X1)
| empty_set = X0
| sP0(X2,X1) )
| ~ spl41_35 ),
inference(forward_subsumption_resolution,[],[f1077,f268]) ).
fof(f1176,plain,
( sP2(sK8,sK9(sK28(sK8)))
| in(sK9(sK28(sK8)),sK28(sK8))
| ~ spl41_54 ),
inference(resolution,[],[f671,f333]) ).
fof(f1189,plain,
( sP0(sK8,sK9(sK28(sK8)))
| ~ spl41_39
| ~ spl41_45
| ~ spl41_56 ),
inference(resolution,[],[f679,f809]) ).
fof(f1191,plain,
( $false
| spl41_23
| ~ spl41_39
| ~ spl41_45
| ~ spl41_56 ),
inference(forward_subsumption_resolution,[],[f1189,f457]) ).
fof(f1192,plain,
( spl41_23
| ~ spl41_39
| ~ spl41_45
| ~ spl41_56 ),
inference(avatar_contradiction_clause,[],[f1191]) ).
fof(f1193,plain,
( spl41_56
| spl41_71
| ~ spl41_32
| ~ spl41_33 ),
inference(avatar_split_clause,[],[f897,f542,f537,f908,f678]) ).
fof(f1194,plain,
( ! [X0] :
( ~ element(sK4(sK9(sK28(sK8))),powerset(powerset(sK9(sK28(sK8)))))
| ~ in(sK5(sK9(sK28(sK8)),sK33(sK4(sK9(sK28(sK8))))),sK4(sK9(sK28(sK8))))
| ~ in(sK9(sK28(sK8)),succ(X0))
| ~ ordinal(sK9(sK28(sK8)))
| empty_set = sK4(sK9(sK28(sK8)))
| sP0(X0,sK9(sK28(sK8))) )
| ~ spl41_35
| ~ spl41_71 ),
inference(resolution,[],[f910,f1080]) ).
fof(f1195,plain,
( ! [X0] :
( ~ in(sK9(sK28(sK8)),succ(X0))
| ~ ordinal(sK9(sK28(sK8)))
| sP0(X0,sK9(sK28(sK8)))
| in(sK5(sK9(sK28(sK8)),sK33(sK4(sK9(sK28(sK8))))),sK4(sK9(sK28(sK8)))) )
| ~ spl41_71 ),
inference(resolution,[],[f910,f269]) ).
fof(f1198,plain,
( ! [X0] :
( ~ in(sK9(sK28(sK8)),succ(X0))
| sP0(X0,sK9(sK28(sK8)))
| in(sK5(sK9(sK28(sK8)),sK33(sK4(sK9(sK28(sK8))))),sK4(sK9(sK28(sK8)))) )
| ~ spl41_32
| ~ spl41_71 ),
inference(forward_subsumption_resolution,[],[f1195,f539]) ).
fof(f1199,plain,
( ! [X0] :
( ~ in(sK5(sK9(sK28(sK8)),sK33(sK4(sK9(sK28(sK8))))),sK4(sK9(sK28(sK8))))
| ~ in(sK9(sK28(sK8)),succ(X0))
| ~ ordinal(sK9(sK28(sK8)))
| empty_set = sK4(sK9(sK28(sK8)))
| sP0(X0,sK9(sK28(sK8))) )
| ~ spl41_35
| ~ spl41_71 ),
inference(forward_subsumption_resolution,[],[f1194,f271]) ).
fof(f1200,plain,
( spl41_75
| spl41_56
| ~ spl41_32
| ~ spl41_71 ),
inference(avatar_split_clause,[],[f1198,f908,f537,f678,f966]) ).
fof(f1201,plain,
( ! [X0] :
( ~ in(sK5(sK9(sK28(sK8)),sK33(sK4(sK9(sK28(sK8))))),sK4(sK9(sK28(sK8))))
| ~ in(sK9(sK28(sK8)),succ(X0))
| ~ ordinal(sK9(sK28(sK8)))
| sP0(X0,sK9(sK28(sK8))) )
| ~ spl41_35
| ~ spl41_71 ),
inference(forward_subsumption_resolution,[],[f1199,f267]) ).
fof(f1202,plain,
( ! [X0] :
( ~ in(sK5(sK9(sK28(sK8)),sK33(sK4(sK9(sK28(sK8))))),sK4(sK9(sK28(sK8))))
| ~ in(sK9(sK28(sK8)),succ(X0))
| sP0(X0,sK9(sK28(sK8))) )
| ~ spl41_32
| ~ spl41_35
| ~ spl41_71 ),
inference(forward_subsumption_resolution,[],[f1201,f539]) ).
fof(f1203,plain,
( spl41_56
| ~ spl41_75
| ~ spl41_32
| ~ spl41_35
| ~ spl41_71 ),
inference(avatar_split_clause,[],[f1202,f908,f550,f537,f966,f678]) ).
fof(f1204,plain,
( ! [X0] :
( empty_set = X0
| ~ element(X0,powerset(powerset(sK9(sK28(sK8)))))
| in(sK7(X0),X0)
| ~ sP0(sK8,sK9(sK28(sK8))) )
| ~ spl41_21 ),
inference(forward_subsumption_resolution,[],[f799,f137]) ).
fof(f1207,plain,
( spl41_42
| spl41_39
| ~ spl41_54 ),
inference(avatar_split_clause,[],[f1176,f670,f579,f597]) ).
fof(f1208,plain,
( ~ spl41_23
| spl41_24
| ~ spl41_21 ),
inference(avatar_split_clause,[],[f1204,f418,f459,f455]) ).
fof(f1219,plain,
( ! [X0] :
( in(sK7(sK29(sK9(sK28(sK8)))),sK29(sK9(sK28(sK8))))
| empty_set = sK29(sK9(sK28(sK8)))
| ~ in(sK9(sK28(sK8)),succ(X0))
| ~ ordinal(sK9(sK28(sK8)))
| sP2(X0,sK9(sK28(sK8))) )
| ~ spl41_24 ),
inference(resolution,[],[f460,f282]) ).
fof(f1228,plain,
( ! [X0] :
( in(sK7(sK29(sK9(sK28(sK8)))),sK29(sK9(sK28(sK8))))
| ~ in(sK9(sK28(sK8)),succ(X0))
| ~ ordinal(sK9(sK28(sK8)))
| sP2(X0,sK9(sK28(sK8))) )
| ~ spl41_24 ),
inference(forward_subsumption_resolution,[],[f1219,f274]) ).
fof(f1232,plain,
( ! [X0] :
( in(sK7(sK29(sK9(sK28(sK8)))),sK29(sK9(sK28(sK8))))
| ~ in(sK9(sK28(sK8)),succ(X0))
| sP2(X0,sK9(sK28(sK8))) )
| ~ spl41_24
| ~ spl41_32 ),
inference(forward_subsumption_resolution,[],[f1228,f539]) ).
fof(f1234,plain,
( spl41_54
| spl41_55
| ~ spl41_24
| ~ spl41_32 ),
inference(avatar_split_clause,[],[f1232,f537,f459,f673,f670]) ).
fof(f1272,plain,
( ! [X0,X1] :
( ~ element(sK29(sK9(sK28(sK8))),powerset(powerset(sK9(X0))))
| empty_set = sK29(sK9(sK28(sK8)))
| in(sK9(X0),X0)
| ~ ordinal(sK9(X0))
| sP2(sK8,sK9(X0))
| ~ in(sK9(sK28(sK8)),succ(X1))
| ~ ordinal(sK9(sK28(sK8)))
| ~ in(sK30(sK9(sK28(sK8)),sK7(sK29(sK9(sK28(sK8))))),sK29(sK9(sK28(sK8))))
| sP2(X1,sK9(sK28(sK8))) )
| ~ spl41_55 ),
inference(resolution,[],[f675,f515]) ).
fof(f1273,plain,
( ! [X0] :
( ~ in(sK9(sK28(sK8)),succ(X0))
| ~ ordinal(sK9(sK28(sK8)))
| sP2(X0,sK9(sK28(sK8)))
| in(sK30(sK9(sK28(sK8)),sK7(sK29(sK9(sK28(sK8))))),sK29(sK9(sK28(sK8)))) )
| ~ spl41_55 ),
inference(resolution,[],[f675,f278]) ).
fof(f1277,plain,
( ! [X0] :
( ~ in(sK9(sK28(sK8)),succ(X0))
| sP2(X0,sK9(sK28(sK8)))
| in(sK30(sK9(sK28(sK8)),sK7(sK29(sK9(sK28(sK8))))),sK29(sK9(sK28(sK8)))) )
| ~ spl41_32
| ~ spl41_55 ),
inference(forward_subsumption_resolution,[],[f1273,f539]) ).
fof(f1278,plain,
( ! [X0,X1] :
( ~ element(sK29(sK9(sK28(sK8))),powerset(powerset(sK9(X0))))
| in(sK9(X0),X0)
| ~ ordinal(sK9(X0))
| sP2(sK8,sK9(X0))
| ~ in(sK9(sK28(sK8)),succ(X1))
| ~ ordinal(sK9(sK28(sK8)))
| ~ in(sK30(sK9(sK28(sK8)),sK7(sK29(sK9(sK28(sK8))))),sK29(sK9(sK28(sK8))))
| sP2(X1,sK9(sK28(sK8))) )
| ~ spl41_55 ),
inference(forward_subsumption_resolution,[],[f1272,f274]) ).
fof(f1281,plain,
( ! [X0,X1] :
( ~ element(sK29(sK9(sK28(sK8))),powerset(powerset(sK9(X0))))
| in(sK9(X0),X0)
| ~ ordinal(sK9(X0))
| sP2(sK8,sK9(X0))
| ~ in(sK9(sK28(sK8)),succ(X1))
| ~ in(sK30(sK9(sK28(sK8)),sK7(sK29(sK9(sK28(sK8))))),sK29(sK9(sK28(sK8))))
| sP2(X1,sK9(sK28(sK8))) )
| ~ spl41_32
| ~ spl41_55 ),
inference(forward_subsumption_resolution,[],[f1278,f539]) ).
fof(f1288,definition,
( spl41_95
<=> in(sK30(sK9(sK28(sK8)),sK7(sK29(sK9(sK28(sK8))))),sK29(sK9(sK28(sK8)))) ),
introduced(definition,[new_symbols(definition,[spl41_95])],[avatar_definition]) ).
fof(f1294,definition,
( spl41_96
<=> ! [X0] :
( ~ element(sK29(sK9(sK28(sK8))),powerset(powerset(sK9(X0))))
| sP2(sK8,sK9(X0))
| ~ ordinal(sK9(X0))
| in(sK9(X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl41_96])],[avatar_definition]) ).
fof(f1295,plain,
( ! [X0] :
( ~ element(sK29(sK9(sK28(sK8))),powerset(powerset(sK9(X0))))
| sP2(sK8,sK9(X0))
| ~ ordinal(sK9(X0))
| in(sK9(X0),X0) )
| ~ spl41_96 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1321,plain,
( ! [X0] :
( sP2(sK8,sK9(sK28(sK8)))
| ~ ordinal(sK9(sK28(sK8)))
| in(sK9(sK28(sK8)),sK28(sK8))
| ~ in(sK9(sK28(sK8)),succ(X0))
| ~ ordinal(sK9(sK28(sK8)))
| sP2(X0,sK9(sK28(sK8))) )
| ~ spl41_96 ),
inference(resolution,[],[f1295,f282]) ).
fof(f1322,plain,
( ! [X0] :
( sP2(sK8,sK9(sK28(sK8)))
| ~ ordinal(sK9(sK28(sK8)))
| in(sK9(sK28(sK8)),sK28(sK8))
| ~ in(sK9(sK28(sK8)),succ(X0))
| sP2(X0,sK9(sK28(sK8))) )
| ~ spl41_96 ),
inference(duplicate_literal_removal,[],[f1321]) ).
fof(f1323,plain,
( ! [X0] :
( ~ ordinal(sK9(sK28(sK8)))
| in(sK9(sK28(sK8)),sK28(sK8))
| ~ in(sK9(sK28(sK8)),succ(X0))
| sP2(X0,sK9(sK28(sK8))) )
| spl41_39
| ~ spl41_96 ),
inference(forward_subsumption_resolution,[],[f1322,f580]) ).
fof(f1324,plain,
( ! [X0] :
( in(sK9(sK28(sK8)),sK28(sK8))
| ~ in(sK9(sK28(sK8)),succ(X0))
| sP2(X0,sK9(sK28(sK8))) )
| ~ spl41_32
| spl41_39
| ~ spl41_96 ),
inference(forward_subsumption_resolution,[],[f1323,f539]) ).
fof(f1325,plain,
( ! [X0] :
( ~ in(sK9(sK28(sK8)),succ(X0))
| sP2(X0,sK9(sK28(sK8))) )
| ~ spl41_32
| spl41_39
| spl41_42
| ~ spl41_96 ),
inference(forward_subsumption_resolution,[],[f1324,f598]) ).
fof(f1332,plain,
( spl41_95
| spl41_54
| ~ spl41_32
| ~ spl41_55 ),
inference(avatar_split_clause,[],[f1277,f673,f537,f670,f1288]) ).
fof(f1333,plain,
( ~ spl41_95
| spl41_54
| spl41_96
| ~ spl41_32
| ~ spl41_55 ),
inference(avatar_split_clause,[],[f1281,f673,f537,f1294,f670,f1288]) ).
fof(f1335,plain,
( spl41_54
| ~ spl41_32
| spl41_39
| spl41_42
| ~ spl41_96 ),
inference(avatar_split_clause,[],[f1325,f1294,f597,f579,f537,f670]) ).
cnf(s2,plain,
( spl41_2
| spl41_3 ),
inference(sat_conversion,[],[f297]) ).
cnf(s7,plain,
( spl41_2
| spl41_9 ),
inference(sat_conversion,[],[f324]) ).
cnf(s8,plain,
( spl41_2
| ~ spl41_10 ),
inference(sat_conversion,[],[f329]) ).
cnf(s14,plain,
( ~ spl41_20
| spl41_21 ),
inference(sat_conversion,[],[f420]) ).
cnf(s16,plain,
( ~ spl41_2
| spl41_20 ),
inference(sat_conversion,[],[f428]) ).
cnf(s22,plain,
( ~ spl41_20
| spl41_23
| spl41_31
| spl41_32 ),
inference(sat_conversion,[],[f540]) ).
cnf(s24,plain,
( ~ spl41_20
| spl41_23
| spl41_31
| ~ spl41_34
| spl41_35 ),
inference(sat_conversion,[],[f552]) ).
cnf(s29,plain,
( ~ spl41_20
| spl41_23
| spl41_39 ),
inference(sat_conversion,[],[f604]) ).
cnf(s40,plain,
( ~ spl41_39
| spl41_44 ),
inference(sat_conversion,[],[f691]) ).
cnf(s41,plain,
( ~ spl41_39
| spl41_45 ),
inference(sat_conversion,[],[f692]) ).
cnf(s42,plain,
( ~ spl41_20
| ~ spl41_39
| spl41_42 ),
inference(sat_conversion,[],[f694]) ).
cnf(s47,plain,
( ~ spl41_23
| ~ spl41_42 ),
inference(sat_conversion,[],[f714]) ).
cnf(s51,plain,
( spl41_32
| spl41_42
| spl41_43 ),
inference(sat_conversion,[],[f723]) ).
cnf(s53,plain,
( ~ spl41_20
| spl41_23
| ~ spl41_31 ),
inference(sat_conversion,[],[f733]) ).
cnf(s61,plain,
( ~ spl41_3
| ~ spl41_9
| spl41_10 ),
inference(sat_conversion,[],[f744]) ).
cnf(s67,plain,
( spl41_42
| ~ spl41_43 ),
inference(sat_conversion,[],[f756]) ).
cnf(s76,plain,
( spl41_31
| spl41_33
| ~ spl41_34
| ~ spl41_44 ),
inference(sat_conversion,[],[f832]) ).
cnf(s80,plain,
( spl41_23
| ~ spl41_32
| spl41_34
| ~ spl41_39
| ~ spl41_45 ),
inference(sat_conversion,[],[f836]) ).
cnf(s116,plain,
( spl41_23
| ~ spl41_39
| ~ spl41_45
| ~ spl41_56 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s117,plain,
( ~ spl41_32
| ~ spl41_33
| spl41_56
| spl41_71 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s118,plain,
( ~ spl41_32
| spl41_56
| ~ spl41_71
| spl41_75 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s119,plain,
( ~ spl41_32
| ~ spl41_35
| spl41_56
| ~ spl41_71
| ~ spl41_75 ),
inference(sat_conversion,[],[f1203]) ).
cnf(s122,plain,
( spl41_39
| spl41_42
| ~ spl41_54 ),
inference(sat_conversion,[],[f1207]) ).
cnf(s123,plain,
( ~ spl41_21
| ~ spl41_23
| spl41_24 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s129,plain,
( ~ spl41_24
| ~ spl41_32
| spl41_54
| spl41_55 ),
inference(sat_conversion,[],[f1234]) ).
cnf(s143,plain,
( ~ spl41_32
| spl41_54
| ~ spl41_55
| spl41_95 ),
inference(sat_conversion,[],[f1332]) ).
cnf(s144,plain,
( ~ spl41_32
| spl41_54
| ~ spl41_55
| ~ spl41_95
| spl41_96 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s145,plain,
( ~ spl41_32
| spl41_39
| spl41_42
| spl41_54
| ~ spl41_96 ),
inference(sat_conversion,[],[f1335]) ).
cnf(s153,plain,
( spl41_23
| ~ spl41_20 ),
inference(rat,[],[s119,s118,s117,s76,s24,s80,s116,s22,s40,s41,s53,s29]) ).
cnf(s154,plain,
( ~ spl41_55
| spl41_96
| ~ spl41_32
| spl41_54 ),
inference(rat,[],[s143,s144]) ).
cnf(s155,plain,
~ spl41_20,
inference(rat,[],[s154,s129,s145,s122,s51,s42,s67,s47,s123,s153,s14]) ).
cnf(s156,plain,
~ spl41_2,
inference(rat,[],[s16,s155]) ).
cnf(s157,plain,
~ spl41_10,
inference(rat,[],[s8,s156]) ).
cnf(s158,plain,
spl41_9,
inference(rat,[],[s7,s156]) ).
cnf(s161,plain,
spl41_3,
inference(rat,[],[s2,s156]) ).
cnf(s163,plain,
$false,
inference(rat,[],[s61,s161,s157,s158]) ).
fof(f1336,plain,
$false,
inference(avatar_sat_refutation,[],[s163]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU299+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n009.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 04:34:15 UTC 2026
% 0.15/0.38 % CPUTime :
% 0.15/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 Running first-order theorem proving
% 0.15/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.21/1.31 % (2660948)Detected formulas, will run a generic FOF schedule.
% 2.21/1.31 % (2660957)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1690596974:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.21/1.31 % (2660959)dis-21_1_sil=8000:lcm=predicate:random_seed=4192918506:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.21/1.31 % (2660954)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2413490835:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.21/1.31 % (2660953)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2895051178:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.21/1.31 % (2660955)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=190477106:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.21/1.31 % (2660956)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4129120657:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.21/1.31 % (2660958)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=789372673:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.21/1.31 % (2660957)Instruction limit reached!
% 2.21/1.31 % (2660957)------------------------------
% 2.21/1.31 % (2660957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.21/1.31 % (2660957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/1.31 % (2660957)CaDiCaL version: 2.1.3
% 2.21/1.31 % (2660957)Termination reason: Instruction limit
% 2.21/1.31 % (2660957)Termination phase: Saturation
% 2.21/1.31 % (2660957)Time elapsed: 0.039 s
% 2.21/1.31 % (2660957)Peak memory usage: 88 MB
% 2.21/1.31 % (2660957)Instructions burned: 119 (million)
% 2.21/1.31 % (2660956)Refutation not found, incomplete strategy
% 2.21/1.31 % (2660956)------------------------------
% 2.21/1.31 % (2660956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.21/1.31 % (2660956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/1.31 % (2660956)CaDiCaL version: 2.1.3
% 2.21/1.31 % (2660956)Termination reason: Refutation not found, incomplete strategy
% 2.21/1.31 % (2660956)Time elapsed: 0.041 s
% 2.21/1.31 % (2660956)Peak memory usage: 89 MB
% 2.21/1.31 % (2660956)Instructions burned: 72 (million)
% 2.21/1.31 % (2660958)First to succeed.
% 2.21/1.31 % (2660958)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2660948"
% 2.21/1.31 % (2660959)Instruction limit reached!
% 2.21/1.31 % (2660959)------------------------------
% 2.21/1.31 % (2660959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.21/1.31 % (2660959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/1.31 % (2660959)CaDiCaL version: 2.1.3
% 2.21/1.31 % (2660959)Termination reason: Instruction limit
% 2.21/1.31 % (2660959)Termination phase: Saturation
% 2.21/1.31 % (2660959)Time elapsed: 0.077 s
% 2.21/1.31 % (2660959)Peak memory usage: 89 MB
% 2.21/1.31 % (2660959)Instructions burned: 130 (million)
% 2.21/1.31 % (2660967)lrs+10_1_sil=8000:sp=occurrence:random_seed=910664652:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.21/1.31 % (2660968)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1315975020:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.21/1.31 % (2660967)Instruction limit reached!
% 2.21/1.31 % (2660967)------------------------------
% 2.21/1.31 % (2660967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.21/1.31 % (2660967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/1.31 % (2660967)CaDiCaL version: 2.1.3
% 2.21/1.31 % (2660967)Termination reason: Instruction limit
% 2.21/1.31 % (2660967)Termination phase: Saturation
% 2.21/1.31 % (2660967)Time elapsed: 0.096 s
% 2.21/1.31 % (2660967)Peak memory usage: 93 MB
% 2.21/1.31 % (2660967)Instructions burned: 288 (million)
% 2.21/1.31 % (2660968)Instruction limit reached!
% 2.21/1.31 % (2660968)------------------------------
% 2.21/1.31 % (2660968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.21/1.31 % (2660968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/1.31 % (2660968)CaDiCaL version: 2.1.3
% 2.21/1.31 % (2660968)Termination reason: Instruction limit
% 2.21/1.31 % (2660968)Termination phase: Saturation
% 2.21/1.31 % (2660968)Time elapsed: 0.073 s
% 2.21/1.31 % (2660968)Peak memory usage: 90 MB
% 2.21/1.31 % (2660968)Instructions burned: 157 (million)
% 2.21/1.31 % (2660956)------------------------------
% 2.21/1.31 % (2660956)------------------------------
% 2.21/1.31 % (2660971)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3134567379:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 2.21/1.31 % (2660958)Refutation found. Thanks to Tanya!
% 2.21/1.31 % SZS status Theorem for theBenchmark
% 2.21/1.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/1.50 % (2660958)------------------------------
% 0.17/1.50 % (2660958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/1.50 % (2660958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/1.50 % (2660958)CaDiCaL version: 2.1.3
% 0.17/1.50 % (2660958)Termination reason: Refutation
% 0.17/1.50 % (2660958)Time elapsed: 0.046 s
% 0.17/1.50 % (2660958)Peak memory usage: 90 MB
% 0.17/1.50 % (2660958)Instructions burned: 65 (million)
% 0.17/1.50 % (2660958)------------------------------
% 0.17/1.50 % (2660958)------------------------------
% 0.17/1.50 % (2660948)Success in time 0.449 s
% 0.17/1.50 % Vampire exiting
%------------------------------------------------------------------------------