%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU301+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:52:47 PM UTC 2026
% Result : Theorem 9.32s 4.21s
% Output : Refutation 9.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 18
% Syntax : Number of formulae : 224 ( 26 unt; 8 def)
% Number of atoms : 1412 ( 283 equ)
% Maximal formula atoms : 49 ( 6 avg)
% Number of connectives : 1994 ( 806 ~; 786 |; 285 &)
% ( 0 <=>; 117 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 2 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 9 con; 0-2 aty)
% Number of variables : 481 ( 407 !; 74 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ( in(empty_set,omega)
=> ! [X0] :
( element(X0,powerset(powerset(empty_set)))
=> ~ ( X0 != empty_set
& ! [X1] :
~ ( in(X1,X0)
& ! [X2] :
( ( in(X2,X0)
& subset(X1,X2) )
=> X2 = X1 ) ) ) ) )
& ! [X3] :
( ordinal(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 ) ) ) ) )
=> ( in(succ(X3),omega)
=> ! [X7] :
( element(X7,powerset(powerset(succ(X3))))
=> ~ ( X7 != empty_set
& ! [X8] :
~ ( in(X8,X7)
& ! [X9] :
( ( in(X9,X7)
& subset(X8,X9) )
=> X9 = X8 ) ) ) ) ) ) )
& ! [X3] :
( ordinal(X3)
=> ( ( being_limit_ordinal(X3)
& ! [X10] :
( ordinal(X10)
=> ( in(X10,X3)
=> ( in(X10,omega)
=> ! [X11] :
( element(X11,powerset(powerset(X10)))
=> ~ ( X11 != empty_set
& ! [X12] :
~ ( in(X12,X11)
& ! [X13] :
( ( in(X13,X11)
& subset(X12,X13) )
=> X13 = X12 ) ) ) ) ) ) ) )
=> ( X3 = empty_set
| ( in(X3,omega)
=> ! [X14] :
( element(X14,powerset(powerset(X3)))
=> ~ ( X14 != empty_set
& ! [X15] :
~ ( in(X15,X14)
& ! [X16] :
( ( in(X16,X14)
& subset(X15,X16) )
=> X16 = X15 ) ) ) ) ) ) ) ) )
=> ! [X3] :
( ordinal(X3)
=> ( in(X3,omega)
=> ! [X17] :
( element(X17,powerset(powerset(X3)))
=> ~ ( X17 != empty_set
& ! [X18] :
~ ( in(X18,X17)
& ! [X19] :
( ( in(X19,X17)
& subset(X18,X19) )
=> X19 = X18 ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_ordinal2__e18_27__finset_1) ).
fof(f2,negated_conjecture,
~ ( ( ( in(empty_set,omega)
=> ! [X0] :
( element(X0,powerset(powerset(empty_set)))
=> ~ ( X0 != empty_set
& ! [X1] :
~ ( in(X1,X0)
& ! [X2] :
( ( in(X2,X0)
& subset(X1,X2) )
=> X2 = X1 ) ) ) ) )
& ! [X3] :
( ordinal(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 ) ) ) ) )
=> ( in(succ(X3),omega)
=> ! [X7] :
( element(X7,powerset(powerset(succ(X3))))
=> ~ ( X7 != empty_set
& ! [X8] :
~ ( in(X8,X7)
& ! [X9] :
( ( in(X9,X7)
& subset(X8,X9) )
=> X9 = X8 ) ) ) ) ) ) )
& ! [X3] :
( ordinal(X3)
=> ( ( being_limit_ordinal(X3)
& ! [X10] :
( ordinal(X10)
=> ( in(X10,X3)
=> ( in(X10,omega)
=> ! [X11] :
( element(X11,powerset(powerset(X10)))
=> ~ ( X11 != empty_set
& ! [X12] :
~ ( in(X12,X11)
& ! [X13] :
( ( in(X13,X11)
& subset(X12,X13) )
=> X13 = X12 ) ) ) ) ) ) ) )
=> ( X3 = empty_set
| ( in(X3,omega)
=> ! [X14] :
( element(X14,powerset(powerset(X3)))
=> ~ ( X14 != empty_set
& ! [X15] :
~ ( in(X15,X14)
& ! [X16] :
( ( in(X16,X14)
& subset(X15,X16) )
=> X16 = X15 ) ) ) ) ) ) ) ) )
=> ! [X3] :
( ordinal(X3)
=> ( in(X3,omega)
=> ! [X17] :
( element(X17,powerset(powerset(X3)))
=> ~ ( X17 != empty_set
& ! [X18] :
~ ( in(X18,X17)
& ! [X19] :
( ( in(X19,X17)
& subset(X18,X19) )
=> X19 = X18 ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f41,axiom,
! [X0] :
( ordinal(X0)
=> ! [X1] :
( element(X1,X0)
=> ( epsilon_transitive(X1)
& epsilon_connected(X1)
& ordinal(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_arytm_3) ).
fof(f42,axiom,
! [X0] :
( element(X0,omega)
=> ( epsilon_transitive(X0)
& epsilon_connected(X0)
& ordinal(X0)
& natural(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc3_arytm_3) ).
fof(f49,axiom,
( ! [X0] :
( ordinal(X0)
=> ( ! [X1] :
( ordinal(X1)
=> ( in(X1,X0)
=> ( in(X1,omega)
=> ! [X2] :
( element(X2,powerset(powerset(X1)))
=> ~ ( X2 != empty_set
& ! [X3] :
~ ( in(X3,X2)
& ! [X4] :
( ( in(X4,X2)
& subset(X3,X4) )
=> X4 = X3 ) ) ) ) ) ) )
=> ( in(X0,omega)
=> ! [X5] :
( element(X5,powerset(powerset(X0)))
=> ~ ( X5 != empty_set
& ! [X6] :
~ ( in(X6,X5)
& ! [X7] :
( ( in(X7,X5)
& subset(X6,X7) )
=> X7 = X6 ) ) ) ) ) ) )
=> ! [X0] :
( ordinal(X0)
=> ( in(X0,omega)
=> ! [X8] :
( element(X8,powerset(powerset(X0)))
=> ~ ( X8 != empty_set
& ! [X9] :
~ ( in(X9,X8)
& ! [X10] :
( ( in(X10,X8)
& subset(X9,X10) )
=> X10 = X9 ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s2_ordinal1__e18_27__finset_1__1) ).
fof(f51,axiom,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_ordinal1) ).
fof(f59,axiom,
! [X0] : in(X0,succ(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_ordinal1) ).
fof(f61,axiom,
! [X0,X1] :
( in(X0,X1)
=> element(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f62,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( empty(X1)
| in(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f63,axiom,
! [X0] :
( ordinal(X0)
=> ( ~ ( ~ being_limit_ordinal(X0)
& ! [X1] :
( ordinal(X1)
=> X0 != succ(X1) ) )
& ~ ( ? [X1] :
( ordinal(X1)
& X0 = succ(X1) )
& being_limit_ordinal(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t42_ordinal1) ).
fof(f65,axiom,
! [X0,X1] :
~ ( in(X0,X1)
& empty(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f67,plain,
~ ( ( ( in(empty_set,omega)
=> ! [X0] :
( element(X0,powerset(powerset(empty_set)))
=> ~ ( X0 != empty_set
& ! [X1] :
~ ( in(X1,X0)
& ! [X2] :
( ( in(X2,X0)
& subset(X1,X2) )
=> X2 = X1 ) ) ) ) )
& ! [X3] :
( ordinal(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 ) ) ) ) )
=> ( in(succ(X3),omega)
=> ! [X7] :
( element(X7,powerset(powerset(succ(X3))))
=> ~ ( X7 != empty_set
& ! [X8] :
~ ( in(X8,X7)
& ! [X9] :
( ( in(X9,X7)
& subset(X8,X9) )
=> X9 = X8 ) ) ) ) ) ) )
& ! [X10] :
( ordinal(X10)
=> ( ( being_limit_ordinal(X10)
& ! [X11] :
( ordinal(X11)
=> ( in(X11,X10)
=> ( in(X11,omega)
=> ! [X12] :
( element(X12,powerset(powerset(X11)))
=> ~ ( empty_set != X12
& ! [X13] :
~ ( in(X13,X12)
& ! [X14] :
( ( in(X14,X12)
& subset(X13,X14) )
=> X13 = X14 ) ) ) ) ) ) ) )
=> ( empty_set = X10
| ( in(X10,omega)
=> ! [X15] :
( element(X15,powerset(powerset(X10)))
=> ~ ( empty_set != X15
& ! [X16] :
~ ( in(X16,X15)
& ! [X17] :
( ( in(X17,X15)
& subset(X16,X17) )
=> X16 = X17 ) ) ) ) ) ) ) ) )
=> ! [X18] :
( ordinal(X18)
=> ( in(X18,omega)
=> ! [X19] :
( element(X19,powerset(powerset(X18)))
=> ~ ( empty_set != X19
& ! [X20] :
~ ( in(X20,X19)
& ! [X21] :
( ( in(X21,X19)
& subset(X20,X21) )
=> X20 = X21 ) ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f69,plain,
( ! [X0] :
( ordinal(X0)
=> ( ! [X1] :
( ordinal(X1)
=> ( in(X1,X0)
=> ( in(X1,omega)
=> ! [X2] :
( element(X2,powerset(powerset(X1)))
=> ~ ( X2 != empty_set
& ! [X3] :
~ ( in(X3,X2)
& ! [X4] :
( ( in(X4,X2)
& subset(X3,X4) )
=> X4 = X3 ) ) ) ) ) ) )
=> ( in(X0,omega)
=> ! [X5] :
( element(X5,powerset(powerset(X0)))
=> ~ ( X5 != empty_set
& ! [X6] :
~ ( in(X6,X5)
& ! [X7] :
( ( in(X7,X5)
& subset(X6,X7) )
=> X7 = X6 ) ) ) ) ) ) )
=> ! [X8] :
( ordinal(X8)
=> ( in(X8,omega)
=> ! [X9] :
( element(X9,powerset(powerset(X8)))
=> ~ ( empty_set != X9
& ! [X10] :
~ ( in(X10,X9)
& ! [X11] :
( ( in(X11,X9)
& subset(X10,X11) )
=> X10 = X11 ) ) ) ) ) ) ),
inference(rectify,[],[f49]) ).
fof(f71,plain,
! [X0] :
( ordinal(X0)
=> ( ~ ( ~ being_limit_ordinal(X0)
& ! [X1] :
( ordinal(X1)
=> X0 != succ(X1) ) )
& ~ ( ? [X2] :
( ordinal(X2)
& succ(X2) = X0 )
& being_limit_ordinal(X0) ) ) ),
inference(rectify,[],[f63]) ).
fof(f81,plain,
( ? [X18] :
( ? [X19] :
( empty_set != X19
& ! [X20] :
( ~ in(X20,X19)
| ? [X21] :
( X20 != X21
& in(X21,X19)
& subset(X20,X21) ) )
& element(X19,powerset(powerset(X18))) )
& in(X18,omega)
& ordinal(X18) )
& ( ! [X0] :
( empty_set = X0
| ? [X1] :
( in(X1,X0)
& ! [X2] :
( X2 = X1
| ~ in(X2,X0)
| ~ subset(X1,X2) ) )
| ~ element(X0,powerset(powerset(empty_set))) )
| ~ in(empty_set,omega) )
& ! [X3] :
( ! [X7] :
( empty_set = X7
| ? [X8] :
( in(X8,X7)
& ! [X9] :
( X9 = X8
| ~ in(X9,X7)
| ~ subset(X8,X9) ) )
| ~ element(X7,powerset(powerset(succ(X3)))) )
| ~ in(succ(X3),omega)
| ( ? [X4] :
( X4 != empty_set
& ! [X5] :
( ~ in(X5,X4)
| ? [X6] :
( X5 != X6
& in(X6,X4)
& subset(X5,X6) ) )
& element(X4,powerset(powerset(X3))) )
& in(X3,omega) )
| ~ ordinal(X3) )
& ! [X10] :
( empty_set = X10
| ! [X15] :
( empty_set = X15
| ? [X16] :
( in(X16,X15)
& ! [X17] :
( X16 = X17
| ~ in(X17,X15)
| ~ subset(X16,X17) ) )
| ~ element(X15,powerset(powerset(X10))) )
| ~ in(X10,omega)
| ~ being_limit_ordinal(X10)
| ? [X11] :
( ? [X12] :
( empty_set != X12
& ! [X13] :
( ~ in(X13,X12)
| ? [X14] :
( X13 != X14
& in(X14,X12)
& subset(X13,X14) ) )
& element(X12,powerset(powerset(X11))) )
& in(X11,omega)
& in(X11,X10)
& ordinal(X11) )
| ~ ordinal(X10) ) ),
inference(ennf_transformation,[],[f67]) ).
fof(f82,plain,
( ? [X18] :
( ? [X19] :
( empty_set != X19
& ! [X20] :
( ~ in(X20,X19)
| ? [X21] :
( X20 != X21
& in(X21,X19)
& subset(X20,X21) ) )
& element(X19,powerset(powerset(X18))) )
& in(X18,omega)
& ordinal(X18) )
& ( ! [X0] :
( empty_set = X0
| ? [X1] :
( in(X1,X0)
& ! [X2] :
( X2 = X1
| ~ in(X2,X0)
| ~ subset(X1,X2) ) )
| ~ element(X0,powerset(powerset(empty_set))) )
| ~ in(empty_set,omega) )
& ! [X3] :
( ! [X7] :
( empty_set = X7
| ? [X8] :
( in(X8,X7)
& ! [X9] :
( X9 = X8
| ~ in(X9,X7)
| ~ subset(X8,X9) ) )
| ~ element(X7,powerset(powerset(succ(X3)))) )
| ~ in(succ(X3),omega)
| ( ? [X4] :
( X4 != empty_set
& ! [X5] :
( ~ in(X5,X4)
| ? [X6] :
( X5 != X6
& in(X6,X4)
& subset(X5,X6) ) )
& element(X4,powerset(powerset(X3))) )
& in(X3,omega) )
| ~ ordinal(X3) )
& ! [X10] :
( empty_set = X10
| ! [X15] :
( empty_set = X15
| ? [X16] :
( in(X16,X15)
& ! [X17] :
( X16 = X17
| ~ in(X17,X15)
| ~ subset(X16,X17) ) )
| ~ element(X15,powerset(powerset(X10))) )
| ~ in(X10,omega)
| ~ being_limit_ordinal(X10)
| ? [X11] :
( ? [X12] :
( empty_set != X12
& ! [X13] :
( ~ in(X13,X12)
| ? [X14] :
( X13 != X14
& in(X14,X12)
& subset(X13,X14) ) )
& element(X12,powerset(powerset(X11))) )
& in(X11,omega)
& in(X11,X10)
& ordinal(X11) )
| ~ ordinal(X10) ) ),
inference(flattening,[],[f81]) ).
fof(f99,plain,
! [X0] :
( ! [X1] :
( ( epsilon_transitive(X1)
& epsilon_connected(X1)
& ordinal(X1) )
| ~ element(X1,X0) )
| ~ ordinal(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f100,plain,
! [X0] :
( ( epsilon_transitive(X0)
& epsilon_connected(X0)
& ordinal(X0)
& natural(X0) )
| ~ element(X0,omega) ),
inference(ennf_transformation,[],[f42]) ).
fof(f103,plain,
( ! [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)
| ~ ordinal(X8) )
| ? [X0] :
( ? [X5] :
( X5 != empty_set
& ! [X6] :
( ~ in(X6,X5)
| ? [X7] :
( X6 != X7
& in(X7,X5)
& subset(X6,X7) ) )
& element(X5,powerset(powerset(X0))) )
& in(X0,omega)
& ! [X1] :
( ! [X2] :
( empty_set = X2
| ? [X3] :
( in(X3,X2)
& ! [X4] :
( X4 = X3
| ~ in(X4,X2)
| ~ subset(X3,X4) ) )
| ~ element(X2,powerset(powerset(X1))) )
| ~ in(X1,omega)
| ~ in(X1,X0)
| ~ ordinal(X1) )
& ordinal(X0) ) ),
inference(ennf_transformation,[],[f69]) ).
fof(f104,plain,
( ! [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)
| ~ ordinal(X8) )
| ? [X0] :
( ? [X5] :
( X5 != empty_set
& ! [X6] :
( ~ in(X6,X5)
| ? [X7] :
( X6 != X7
& in(X7,X5)
& subset(X6,X7) ) )
& element(X5,powerset(powerset(X0))) )
& in(X0,omega)
& ! [X1] :
( ! [X2] :
( empty_set = X2
| ? [X3] :
( in(X3,X2)
& ! [X4] :
( X4 = X3
| ~ in(X4,X2)
| ~ subset(X3,X4) ) )
| ~ element(X2,powerset(powerset(X1))) )
| ~ in(X1,omega)
| ~ in(X1,X0)
| ~ ordinal(X1) )
& ordinal(X0) ) ),
inference(flattening,[],[f103]) ).
fof(f107,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f61]) ).
fof(f108,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(ennf_transformation,[],[f62]) ).
fof(f109,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0] :
( ( ( being_limit_ordinal(X0)
| ? [X1] :
( succ(X1) = X0
& ordinal(X1) ) )
& ( ! [X2] :
( ~ ordinal(X2)
| succ(X2) != X0 )
| ~ being_limit_ordinal(X0) ) )
| ~ ordinal(X0) ),
inference(ennf_transformation,[],[f71]) ).
fof(f112,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(ennf_transformation,[],[f65]) ).
fof(f114,definition,
! [X10] :
( ? [X11] :
( ? [X12] :
( empty_set != X12
& ! [X13] :
( ~ in(X13,X12)
| ? [X14] :
( X13 != X14
& in(X14,X12)
& subset(X13,X14) ) )
& element(X12,powerset(powerset(X11))) )
& in(X11,omega)
& in(X11,X10)
& ordinal(X11) )
| ~ sP0(X10) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f115,definition,
! [X3] :
( ( ? [X4] :
( X4 != empty_set
& ! [X5] :
( ~ in(X5,X4)
| ? [X6] :
( X5 != X6
& in(X6,X4)
& subset(X5,X6) ) )
& element(X4,powerset(powerset(X3))) )
& in(X3,omega) )
| ~ sP1(X3) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f116,plain,
( ? [X18] :
( ? [X19] :
( empty_set != X19
& ! [X20] :
( ~ in(X20,X19)
| ? [X21] :
( X20 != X21
& in(X21,X19)
& subset(X20,X21) ) )
& element(X19,powerset(powerset(X18))) )
& in(X18,omega)
& ordinal(X18) )
& ( ! [X0] :
( empty_set = X0
| ? [X1] :
( in(X1,X0)
& ! [X2] :
( X2 = X1
| ~ in(X2,X0)
| ~ subset(X1,X2) ) )
| ~ element(X0,powerset(powerset(empty_set))) )
| ~ in(empty_set,omega) )
& ! [X3] :
( ! [X7] :
( empty_set = X7
| ? [X8] :
( in(X8,X7)
& ! [X9] :
( X9 = X8
| ~ in(X9,X7)
| ~ subset(X8,X9) ) )
| ~ element(X7,powerset(powerset(succ(X3)))) )
| ~ in(succ(X3),omega)
| sP1(X3)
| ~ ordinal(X3) )
& ! [X10] :
( empty_set = X10
| ! [X15] :
( empty_set = X15
| ? [X16] :
( in(X16,X15)
& ! [X17] :
( X16 = X17
| ~ in(X17,X15)
| ~ subset(X16,X17) ) )
| ~ element(X15,powerset(powerset(X10))) )
| ~ in(X10,omega)
| ~ being_limit_ordinal(X10)
| sP0(X10)
| ~ ordinal(X10) ) ),
inference(definition_folding,[],[f82,f115,f114]) ).
fof(f117,definition,
! [X0] :
( ? [X5] :
( X5 != empty_set
& ! [X6] :
( ~ in(X6,X5)
| ? [X7] :
( X6 != X7
& in(X7,X5)
& subset(X6,X7) ) )
& element(X5,powerset(powerset(X0))) )
| ~ sP2(X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f118,definition,
( ? [X0] :
( sP2(X0)
& in(X0,omega)
& ! [X1] :
( ! [X2] :
( empty_set = X2
| ? [X3] :
( in(X3,X2)
& ! [X4] :
( X4 = X3
| ~ in(X4,X2)
| ~ subset(X3,X4) ) )
| ~ element(X2,powerset(powerset(X1))) )
| ~ in(X1,omega)
| ~ in(X1,X0)
| ~ ordinal(X1) )
& ordinal(X0) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f119,plain,
( ! [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)
| ~ ordinal(X8) )
| sP3 ),
inference(definition_folding,[],[f104,f118,f117]) ).
fof(f120,plain,
! [X3] :
( ( ? [X4] :
( X4 != empty_set
& ! [X5] :
( ~ in(X5,X4)
| ? [X6] :
( X5 != X6
& in(X6,X4)
& subset(X5,X6) ) )
& element(X4,powerset(powerset(X3))) )
& in(X3,omega) )
| ~ sP1(X3) ),
inference(nnf_transformation,[],[f115]) ).
fof(f121,plain,
! [X0] :
( ( ? [X1] :
( empty_set != X1
& ! [X2] :
( ~ in(X2,X1)
| ? [X3] :
( X2 != X3
& in(X3,X1)
& subset(X2,X3) ) )
& element(X1,powerset(powerset(X0))) )
& in(X0,omega) )
| ~ sP1(X0) ),
inference(rectify,[],[f120]) ).
fof(f122,plain,
! [X0] :
( ( empty_set != sK4(X0)
& ! [X2] :
( ~ in(X2,sK4(X0))
| ( sK5(X0,X2) != X2
& in(sK5(X0,X2),sK4(X0))
& subset(X2,sK5(X0,X2)) ) )
& element(sK4(X0),powerset(powerset(X0)))
& in(X0,omega) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X1,sK4(X0)),skolemize(X3,sK5(X0,X2))],[f121]) ).
fof(f123,plain,
! [X10] :
( ? [X11] :
( ? [X12] :
( empty_set != X12
& ! [X13] :
( ~ in(X13,X12)
| ? [X14] :
( X13 != X14
& in(X14,X12)
& subset(X13,X14) ) )
& element(X12,powerset(powerset(X11))) )
& in(X11,omega)
& in(X11,X10)
& ordinal(X11) )
| ~ sP0(X10) ),
inference(nnf_transformation,[],[f114]) ).
fof(f124,plain,
! [X0] :
( ? [X1] :
( ? [X2] :
( empty_set != X2
& ! [X3] :
( ~ in(X3,X2)
| ? [X4] :
( X3 != X4
& in(X4,X2)
& subset(X3,X4) ) )
& element(X2,powerset(powerset(X1))) )
& in(X1,omega)
& in(X1,X0)
& ordinal(X1) )
| ~ sP0(X0) ),
inference(rectify,[],[f123]) ).
fof(f125,plain,
! [X0] :
( ( empty_set != sK7(X0)
& ! [X3] :
( ~ in(X3,sK7(X0))
| ( sK8(X0,X3) != X3
& in(sK8(X0,X3),sK7(X0))
& subset(X3,sK8(X0,X3)) ) )
& element(sK7(X0),powerset(powerset(sK6(X0))))
& in(sK6(X0),omega)
& in(sK6(X0),X0)
& ordinal(sK6(X0)) )
| ~ sP0(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(f126,plain,
( ? [X0] :
( ? [X1] :
( empty_set != X1
& ! [X2] :
( ~ in(X2,X1)
| ? [X3] :
( X2 != X3
& in(X3,X1)
& subset(X2,X3) ) )
& element(X1,powerset(powerset(X0))) )
& in(X0,omega)
& ordinal(X0) )
& ( ! [X4] :
( empty_set = X4
| ? [X5] :
( in(X5,X4)
& ! [X6] :
( X5 = X6
| ~ in(X6,X4)
| ~ subset(X5,X6) ) )
| ~ element(X4,powerset(powerset(empty_set))) )
| ~ in(empty_set,omega) )
& ! [X7] :
( ! [X8] :
( empty_set = X8
| ? [X9] :
( in(X9,X8)
& ! [X10] :
( X9 = X10
| ~ in(X10,X8)
| ~ subset(X9,X10) ) )
| ~ element(X8,powerset(powerset(succ(X7)))) )
| ~ in(succ(X7),omega)
| sP1(X7)
| ~ ordinal(X7) )
& ! [X11] :
( empty_set = X11
| ! [X12] :
( empty_set = X12
| ? [X13] :
( in(X13,X12)
& ! [X14] :
( X13 = X14
| ~ in(X14,X12)
| ~ subset(X13,X14) ) )
| ~ element(X12,powerset(powerset(X11))) )
| ~ in(X11,omega)
| ~ being_limit_ordinal(X11)
| sP0(X11)
| ~ ordinal(X11) ) ),
inference(rectify,[],[f116]) ).
fof(f127,plain,
( empty_set != sK10
& ! [X2] :
( ~ in(X2,sK10)
| ( sK11(X2) != X2
& in(sK11(X2),sK10)
& subset(X2,sK11(X2)) ) )
& element(sK10,powerset(powerset(sK9)))
& in(sK9,omega)
& ordinal(sK9)
& ( ! [X4] :
( empty_set = X4
| ( in(sK12(X4),X4)
& ! [X6] :
( sK12(X4) = X6
| ~ in(X6,X4)
| ~ subset(sK12(X4),X6) ) )
| ~ element(X4,powerset(powerset(empty_set))) )
| ~ in(empty_set,omega) )
& ! [X7] :
( ! [X8] :
( empty_set = X8
| ( in(sK13(X8),X8)
& ! [X10] :
( sK13(X8) = X10
| ~ in(X10,X8)
| ~ subset(sK13(X8),X10) ) )
| ~ element(X8,powerset(powerset(succ(X7)))) )
| ~ in(succ(X7),omega)
| sP1(X7)
| ~ ordinal(X7) )
& ! [X11] :
( empty_set = X11
| ! [X12] :
( empty_set = X12
| ( in(sK14(X12),X12)
& ! [X14] :
( sK14(X12) = X14
| ~ in(X14,X12)
| ~ subset(sK14(X12),X14) ) )
| ~ element(X12,powerset(powerset(X11))) )
| ~ in(X11,omega)
| ~ being_limit_ordinal(X11)
| sP0(X11)
| ~ ordinal(X11) ) ),
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(f147,plain,
( ? [X0] :
( sP2(X0)
& in(X0,omega)
& ! [X1] :
( ! [X2] :
( empty_set = X2
| ? [X3] :
( in(X3,X2)
& ! [X4] :
( X4 = X3
| ~ in(X4,X2)
| ~ subset(X3,X4) ) )
| ~ element(X2,powerset(powerset(X1))) )
| ~ in(X1,omega)
| ~ in(X1,X0)
| ~ ordinal(X1) )
& ordinal(X0) )
| ~ sP3 ),
inference(nnf_transformation,[],[f118]) ).
fof(f148,plain,
( ( sP2(sK34)
& in(sK34,omega)
& ! [X1] :
( ! [X2] :
( empty_set = X2
| ( in(sK35(X2),X2)
& ! [X4] :
( sK35(X2) = X4
| ~ in(X4,X2)
| ~ subset(sK35(X2),X4) ) )
| ~ element(X2,powerset(powerset(X1))) )
| ~ in(X1,omega)
| ~ in(X1,sK34)
| ~ ordinal(X1) )
& ordinal(sK34) )
| ~ sP3 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34,sK35]),skolemize(X0,sK34),skolemize(X3,sK35(X2))],[f147]) ).
fof(f149,plain,
! [X0] :
( ? [X5] :
( X5 != empty_set
& ! [X6] :
( ~ in(X6,X5)
| ? [X7] :
( X6 != X7
& in(X7,X5)
& subset(X6,X7) ) )
& element(X5,powerset(powerset(X0))) )
| ~ sP2(X0) ),
inference(nnf_transformation,[],[f117]) ).
fof(f150,plain,
! [X0] :
( ? [X1] :
( empty_set != X1
& ! [X2] :
( ~ in(X2,X1)
| ? [X3] :
( X2 != X3
& in(X3,X1)
& subset(X2,X3) ) )
& element(X1,powerset(powerset(X0))) )
| ~ sP2(X0) ),
inference(rectify,[],[f149]) ).
fof(f151,plain,
! [X0] :
( ( empty_set != sK36(X0)
& ! [X2] :
( ~ in(X2,sK36(X0))
| ( sK37(X0,X2) != X2
& in(sK37(X0,X2),sK36(X0))
& subset(X2,sK37(X0,X2)) ) )
& element(sK36(X0),powerset(powerset(X0))) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36,sK37]),skolemize(X1,sK36(X0)),skolemize(X3,sK37(X0,X2))],[f150]) ).
fof(f152,plain,
( ! [X0] :
( ! [X1] :
( empty_set = X1
| ? [X2] :
( in(X2,X1)
& ! [X3] :
( X2 = X3
| ~ in(X3,X1)
| ~ subset(X2,X3) ) )
| ~ element(X1,powerset(powerset(X0))) )
| ~ in(X0,omega)
| ~ ordinal(X0) )
| sP3 ),
inference(rectify,[],[f119]) ).
fof(f153,plain,
( ! [X0] :
( ! [X1] :
( empty_set = X1
| ( in(sK38(X1),X1)
& ! [X3] :
( sK38(X1) = X3
| ~ in(X3,X1)
| ~ subset(sK38(X1),X3) ) )
| ~ element(X1,powerset(powerset(X0))) )
| ~ in(X0,omega)
| ~ ordinal(X0) )
| sP3 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(X2,sK38(X1))],[f152]) ).
fof(f155,plain,
! [X0] :
( ( ( being_limit_ordinal(X0)
| ( succ(sK40(X0)) = X0
& ordinal(sK40(X0)) ) )
& ( ! [X2] :
( ~ ordinal(X2)
| succ(X2) != X0 )
| ~ being_limit_ordinal(X0) ) )
| ~ ordinal(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(X1,sK40(X0))],[f110]) ).
fof(f156,plain,
! [X0] :
( in(X0,omega)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f157,plain,
! [X0] :
( element(sK4(X0),powerset(powerset(X0)))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f158,plain,
! [X2,X0] :
( subset(X2,sK5(X0,X2))
| ~ in(X2,sK4(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f159,plain,
! [X2,X0] :
( in(sK5(X0,X2),sK4(X0))
| ~ in(X2,sK4(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f160,plain,
! [X2,X0] :
( sK5(X0,X2) != X2
| ~ in(X2,sK4(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f161,plain,
! [X0] :
( empty_set != sK4(X0)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f162,plain,
! [X0] :
( ordinal(sK6(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f163,plain,
! [X0] :
( in(sK6(X0),X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f164,plain,
! [X0] :
( in(sK6(X0),omega)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f165,plain,
! [X0] :
( element(sK7(X0),powerset(powerset(sK6(X0))))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f166,plain,
! [X3,X0] :
( subset(X3,sK8(X0,X3))
| ~ in(X3,sK7(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f167,plain,
! [X3,X0] :
( in(sK8(X0,X3),sK7(X0))
| ~ in(X3,sK7(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f168,plain,
! [X3,X0] :
( sK8(X0,X3) != X3
| ~ in(X3,sK7(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f169,plain,
! [X0] :
( empty_set != sK7(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f170,plain,
! [X11,X14,X12] :
( ~ element(X12,powerset(powerset(X11)))
| empty_set = X12
| sK14(X12) = X14
| ~ in(X14,X12)
| ~ subset(sK14(X12),X14)
| empty_set = X11
| ~ in(X11,omega)
| ~ being_limit_ordinal(X11)
| sP0(X11)
| ~ ordinal(X11) ),
inference(cnf_transformation,[],[f127]) ).
fof(f171,plain,
! [X11,X12] :
( ~ element(X12,powerset(powerset(X11)))
| empty_set = X12
| in(sK14(X12),X12)
| empty_set = X11
| ~ in(X11,omega)
| ~ being_limit_ordinal(X11)
| sP0(X11)
| ~ ordinal(X11) ),
inference(cnf_transformation,[],[f127]) ).
fof(f172,plain,
! [X10,X8,X7] :
( empty_set = X8
| sK13(X8) = X10
| ~ in(X10,X8)
| ~ subset(sK13(X8),X10)
| ~ element(X8,powerset(powerset(succ(X7))))
| ~ in(succ(X7),omega)
| sP1(X7)
| ~ ordinal(X7) ),
inference(cnf_transformation,[],[f127]) ).
fof(f173,plain,
! [X8,X7] :
( empty_set = X8
| in(sK13(X8),X8)
| ~ element(X8,powerset(powerset(succ(X7))))
| ~ in(succ(X7),omega)
| sP1(X7)
| ~ ordinal(X7) ),
inference(cnf_transformation,[],[f127]) ).
fof(f174,plain,
! [X6,X4] :
( empty_set = X4
| sK12(X4) = X6
| ~ in(X6,X4)
| ~ subset(sK12(X4),X6)
| ~ element(X4,powerset(powerset(empty_set)))
| ~ in(empty_set,omega) ),
inference(cnf_transformation,[],[f127]) ).
fof(f175,plain,
! [X4] :
( empty_set = X4
| in(sK12(X4),X4)
| ~ element(X4,powerset(powerset(empty_set)))
| ~ in(empty_set,omega) ),
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(f268,plain,
! [X0,X1] :
( ~ element(X1,X0)
| ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f272,plain,
! [X0] :
( ~ element(X0,omega)
| ordinal(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f290,plain,
( ordinal(sK34)
| ~ sP3 ),
inference(cnf_transformation,[],[f148]) ).
fof(f291,plain,
! [X2,X1,X4] :
( ~ element(X2,powerset(powerset(X1)))
| sK35(X2) = X4
| ~ in(X4,X2)
| ~ subset(sK35(X2),X4)
| empty_set = X2
| ~ in(X1,omega)
| ~ in(X1,sK34)
| ~ ordinal(X1)
| ~ sP3 ),
inference(cnf_transformation,[],[f148]) ).
fof(f292,plain,
! [X2,X1] :
( ~ element(X2,powerset(powerset(X1)))
| in(sK35(X2),X2)
| empty_set = X2
| ~ in(X1,omega)
| ~ in(X1,sK34)
| ~ ordinal(X1)
| ~ sP3 ),
inference(cnf_transformation,[],[f148]) ).
fof(f293,plain,
( in(sK34,omega)
| ~ sP3 ),
inference(cnf_transformation,[],[f148]) ).
fof(f294,plain,
( sP2(sK34)
| ~ sP3 ),
inference(cnf_transformation,[],[f148]) ).
fof(f295,plain,
! [X0] :
( element(sK36(X0),powerset(powerset(X0)))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f296,plain,
! [X2,X0] :
( subset(X2,sK37(X0,X2))
| ~ in(X2,sK36(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f297,plain,
! [X2,X0] :
( in(sK37(X0,X2),sK36(X0))
| ~ in(X2,sK36(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f298,plain,
! [X2,X0] :
( sK37(X0,X2) != X2
| ~ in(X2,sK36(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f299,plain,
! [X0] :
( empty_set != sK36(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f300,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| sK38(X1) = X3
| ~ in(X3,X1)
| ~ subset(sK38(X1),X3)
| empty_set = X1
| ~ in(X0,omega)
| ~ ordinal(X0)
| sP3 ),
inference(cnf_transformation,[],[f153]) ).
fof(f301,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| in(sK38(X1),X1)
| empty_set = X1
| ~ in(X0,omega)
| ~ ordinal(X0)
| sP3 ),
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] :
( being_limit_ordinal(X0)
| succ(sK40(X0)) = X0
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f317,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f319,plain,
! [X8,X7] :
( ~ element(X8,powerset(powerset(set_union2(X7,singleton(X7)))))
| in(sK13(X8),X8)
| empty_set = X8
| ~ in(set_union2(X7,singleton(X7)),omega)
| sP1(X7)
| ~ ordinal(X7) ),
inference(definition_unfolding,[],[f173,f303,f303]) ).
fof(f320,plain,
! [X10,X8,X7] :
( ~ element(X8,powerset(powerset(set_union2(X7,singleton(X7)))))
| sK13(X8) = X10
| ~ in(X10,X8)
| ~ subset(sK13(X8),X10)
| empty_set = X8
| ~ in(set_union2(X7,singleton(X7)),omega)
| sP1(X7)
| ~ ordinal(X7) ),
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]) ).
fof(f335,definition,
sF41 = powerset(sK9),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
fof(f336,plain,
powerset(sK9) = sF41,
inference(reorient_equations,[],[f335]) ).
fof(f337,definition,
sF42 = powerset(sF41),
introduced(definition,[new_symbols(definition,[sF42])],[function_definition]) ).
fof(f338,plain,
powerset(sF41) = sF42,
inference(reorient_equations,[],[f337]) ).
fof(f339,plain,
element(sK10,sF42),
inference(definition_folding,[],[f178,f338,f336]) ).
fof(f340,definition,
sF43 = powerset(empty_set),
introduced(definition,[new_symbols(definition,[sF43])],[function_definition]) ).
fof(f341,plain,
powerset(empty_set) = sF43,
inference(reorient_equations,[],[f340]) ).
fof(f342,definition,
sF44 = powerset(sF43),
introduced(definition,[new_symbols(definition,[sF44])],[function_definition]) ).
fof(f343,plain,
powerset(sF43) = sF44,
inference(reorient_equations,[],[f342]) ).
fof(f344,plain,
! [X4] :
( in(sK12(X4),X4)
| empty_set = X4
| ~ element(X4,sF44)
| ~ in(empty_set,omega) ),
inference(definition_folding,[],[f175,f343,f341]) ).
fof(f345,plain,
! [X6,X4] :
( ~ subset(sK12(X4),X6)
| sK12(X4) = X6
| ~ in(X6,X4)
| empty_set = X4
| ~ element(X4,sF44)
| ~ in(empty_set,omega) ),
inference(definition_folding,[],[f174,f343,f341]) ).
fof(f531,plain,
! [X0] :
( element(X0,omega)
| ~ sP1(X0) ),
inference(resolution,[],[f311,f156]) ).
fof(f544,plain,
! [X0] : element(X0,set_union2(X0,singleton(X0))),
inference(resolution,[],[f331,f311]) ).
fof(f697,plain,
! [X0,X1] :
( ~ sP2(X0)
| empty_set = sK36(X0)
| sK14(sK36(X0)) = X1
| ~ in(X1,sK36(X0))
| ~ subset(sK14(sK36(X0)),X1)
| empty_set = X0
| ~ in(X0,omega)
| ~ being_limit_ordinal(X0)
| sP0(X0)
| ~ ordinal(X0) ),
inference(resolution,[],[f295,f170]) ).
fof(f698,plain,
! [X0] :
( ~ sP2(X0)
| empty_set = sK36(X0)
| in(sK14(sK36(X0)),sK36(X0))
| empty_set = X0
| ~ in(X0,omega)
| ~ being_limit_ordinal(X0)
| sP0(X0)
| ~ ordinal(X0) ),
inference(resolution,[],[f295,f171]) ).
fof(f699,plain,
! [X0,X1] :
( ~ sP2(set_union2(X0,singleton(X0)))
| sK13(sK36(set_union2(X0,singleton(X0)))) = X1
| ~ in(X1,sK36(set_union2(X0,singleton(X0))))
| ~ subset(sK13(sK36(set_union2(X0,singleton(X0)))),X1)
| empty_set = sK36(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| sP1(X0)
| ~ ordinal(X0) ),
inference(resolution,[],[f295,f320]) ).
fof(f700,plain,
! [X0] :
( ~ sP2(set_union2(X0,singleton(X0)))
| in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(set_union2(X0,singleton(X0))))
| empty_set = sK36(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| sP1(X0)
| ~ ordinal(X0) ),
inference(resolution,[],[f295,f319]) ).
fof(f705,plain,
( element(sK36(empty_set),powerset(sF43))
| ~ sP2(empty_set) ),
inference(superposition,[],[f295,f341]) ).
fof(f710,plain,
( element(sK36(empty_set),sF44)
| ~ sP2(empty_set) ),
inference(forward_demodulation,[],[f705,f343]) ).
fof(f711,plain,
! [X0] :
( in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(set_union2(X0,singleton(X0))))
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| sP1(X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[],[f700,f299]) ).
fof(f712,plain,
! [X0,X1] :
( ~ subset(sK13(sK36(set_union2(X0,singleton(X0)))),X1)
| sK13(sK36(set_union2(X0,singleton(X0)))) = X1
| ~ in(X1,sK36(set_union2(X0,singleton(X0))))
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| sP1(X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[],[f699,f299]) ).
fof(f713,plain,
! [X0] :
( in(sK14(sK36(X0)),sK36(X0))
| ~ sP2(X0)
| empty_set = X0
| ~ in(X0,omega)
| ~ being_limit_ordinal(X0)
| sP0(X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[],[f698,f299]) ).
fof(f714,plain,
! [X0,X1] :
( ~ subset(sK14(sK36(X0)),X1)
| sK14(sK36(X0)) = X1
| ~ in(X1,sK36(X0))
| ~ sP2(X0)
| empty_set = X0
| ~ in(X0,omega)
| ~ being_limit_ordinal(X0)
| sP0(X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[],[f697,f299]) ).
fof(f764,plain,
! [X0,X1] :
( ~ in(sK12(X0),sK36(X1))
| ~ sP2(X1)
| sK12(X0) = sK37(X1,sK12(X0))
| ~ in(sK37(X1,sK12(X0)),X0)
| empty_set = X0
| ~ element(X0,sF44)
| ~ in(empty_set,omega) ),
inference(resolution,[],[f296,f345]) ).
fof(f766,plain,
! [X0,X1] :
( ~ in(sK37(X1,sK12(X0)),X0)
| ~ sP2(X1)
| ~ in(sK12(X0),sK36(X1))
| empty_set = X0
| ~ element(X0,sF44)
| ~ in(empty_set,omega) ),
inference(forward_subsumption_resolution,[],[f764,f298]) ).
fof(f802,plain,
( being_limit_ordinal(sK34)
| sK34 = set_union2(sK40(sK34),singleton(sK40(sK34)))
| ~ sP3 ),
inference(resolution,[],[f332,f290]) ).
fof(f825,plain,
! [X0] :
( ~ element(X0,powerset(sF41))
| in(sK38(X0),X0)
| empty_set = X0
| ~ in(sK9,omega)
| ~ ordinal(sK9)
| sP3 ),
inference(superposition,[],[f301,f336]) ).
fof(f828,plain,
! [X0] :
( ~ element(X0,powerset(sF41))
| in(sK38(X0),X0)
| empty_set = X0
| ~ ordinal(sK9)
| sP3 ),
inference(forward_subsumption_resolution,[],[f825,f177]) ).
fof(f835,plain,
! [X0] :
( ~ element(X0,powerset(sF41))
| in(sK38(X0),X0)
| empty_set = X0
| sP3 ),
inference(forward_subsumption_resolution,[],[f828,f176]) ).
fof(f839,plain,
! [X0] :
( in(sK38(X0),X0)
| ~ element(X0,sF42)
| empty_set = X0
| sP3 ),
inference(forward_demodulation,[],[f835,f338]) ).
fof(f853,plain,
! [X0] :
( in(sK35(sK4(X0)),sK4(X0))
| empty_set = sK4(X0)
| ~ in(X0,omega)
| ~ in(X0,sK34)
| ~ ordinal(X0)
| ~ sP3
| ~ sP1(X0) ),
inference(resolution,[],[f292,f157]) ).
fof(f854,plain,
! [X0] :
( in(sK35(sK7(X0)),sK7(X0))
| empty_set = sK7(X0)
| ~ in(sK6(X0),omega)
| ~ in(sK6(X0),sK34)
| ~ ordinal(sK6(X0))
| ~ sP3
| ~ sP0(X0) ),
inference(resolution,[],[f292,f165]) ).
fof(f871,plain,
! [X0] :
( in(sK35(sK7(X0)),sK7(X0))
| ~ in(sK6(X0),omega)
| ~ in(sK6(X0),sK34)
| ~ ordinal(sK6(X0))
| ~ sP3
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f854,f169]) ).
fof(f872,plain,
! [X0] :
( in(sK35(sK4(X0)),sK4(X0))
| ~ in(X0,omega)
| ~ in(X0,sK34)
| ~ ordinal(X0)
| ~ sP3
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f853,f161]) ).
fof(f875,plain,
! [X0] :
( in(sK35(sK7(X0)),sK7(X0))
| ~ in(sK6(X0),sK34)
| ~ ordinal(sK6(X0))
| ~ sP3
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f871,f164]) ).
fof(f876,plain,
! [X0] :
( in(sK35(sK4(X0)),sK4(X0))
| ~ in(X0,sK34)
| ~ ordinal(X0)
| ~ sP3
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f872,f156]) ).
fof(f878,plain,
! [X0] :
( in(sK35(sK7(X0)),sK7(X0))
| ~ in(sK6(X0),sK34)
| ~ sP3
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f875,f162]) ).
fof(f892,plain,
! [X0,X1] :
( ~ element(X0,powerset(sF41))
| sK38(X0) = X1
| ~ in(X1,X0)
| ~ subset(sK38(X0),X1)
| empty_set = X0
| ~ in(sK9,omega)
| ~ ordinal(sK9)
| sP3 ),
inference(superposition,[],[f300,f336]) ).
fof(f895,plain,
! [X0,X1] :
( ~ element(X0,powerset(sF41))
| sK38(X0) = X1
| ~ in(X1,X0)
| ~ subset(sK38(X0),X1)
| empty_set = X0
| ~ ordinal(sK9)
| sP3 ),
inference(forward_subsumption_resolution,[],[f892,f177]) ).
fof(f902,plain,
! [X0,X1] :
( ~ element(X0,powerset(sF41))
| sK38(X0) = X1
| ~ in(X1,X0)
| ~ subset(sK38(X0),X1)
| empty_set = X0
| sP3 ),
inference(forward_subsumption_resolution,[],[f895,f176]) ).
fof(f906,plain,
! [X0,X1] :
( ~ subset(sK38(X0),X1)
| sK38(X0) = X1
| ~ in(X1,X0)
| ~ element(X0,sF42)
| empty_set = X0
| sP3 ),
inference(forward_demodulation,[],[f902,f338]) ).
fof(f909,plain,
! [X0,X1] :
( sK35(sK4(X0)) = X1
| ~ in(X1,sK4(X0))
| ~ subset(sK35(sK4(X0)),X1)
| empty_set = sK4(X0)
| ~ in(X0,omega)
| ~ in(X0,sK34)
| ~ ordinal(X0)
| ~ sP3
| ~ sP1(X0) ),
inference(resolution,[],[f291,f157]) ).
fof(f910,plain,
! [X0,X1] :
( sK35(sK7(X0)) = X1
| ~ in(X1,sK7(X0))
| ~ subset(sK35(sK7(X0)),X1)
| empty_set = sK7(X0)
| ~ in(sK6(X0),omega)
| ~ in(sK6(X0),sK34)
| ~ ordinal(sK6(X0))
| ~ sP3
| ~ sP0(X0) ),
inference(resolution,[],[f291,f165]) ).
fof(f927,plain,
! [X0,X1] :
( sK35(sK7(X0)) = X1
| ~ in(X1,sK7(X0))
| ~ subset(sK35(sK7(X0)),X1)
| ~ in(sK6(X0),omega)
| ~ in(sK6(X0),sK34)
| ~ ordinal(sK6(X0))
| ~ sP3
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f910,f169]) ).
fof(f928,plain,
! [X0,X1] :
( sK35(sK4(X0)) = X1
| ~ in(X1,sK4(X0))
| ~ subset(sK35(sK4(X0)),X1)
| ~ in(X0,omega)
| ~ in(X0,sK34)
| ~ ordinal(X0)
| ~ sP3
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f909,f161]) ).
fof(f931,plain,
! [X0,X1] :
( sK35(sK7(X0)) = X1
| ~ in(X1,sK7(X0))
| ~ subset(sK35(sK7(X0)),X1)
| ~ in(sK6(X0),sK34)
| ~ ordinal(sK6(X0))
| ~ sP3
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f927,f164]) ).
fof(f932,plain,
! [X0,X1] :
( ~ subset(sK35(sK4(X0)),X1)
| ~ in(X1,sK4(X0))
| sK35(sK4(X0)) = X1
| ~ in(X0,sK34)
| ~ ordinal(X0)
| ~ sP3
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f928,f156]) ).
fof(f934,plain,
! [X0,X1] :
( ~ subset(sK35(sK7(X0)),X1)
| ~ in(X1,sK7(X0))
| sK35(sK7(X0)) = X1
| ~ in(sK6(X0),sK34)
| ~ sP3
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f931,f162]) ).
fof(f957,plain,
! [X0] :
( sK38(X0) = sK11(sK38(X0))
| ~ in(sK11(sK38(X0)),X0)
| ~ element(X0,sF42)
| empty_set = X0
| sP3
| ~ in(sK38(X0),sK10) ),
inference(resolution,[],[f906,f179]) ).
fof(f960,plain,
! [X0] :
( ~ in(sK11(sK38(X0)),X0)
| ~ element(X0,sF42)
| empty_set = X0
| sP3
| ~ in(sK38(X0),sK10) ),
inference(forward_subsumption_resolution,[],[f957,f181]) ).
fof(f1012,plain,
! [X0] :
( ~ sP2(X0)
| ~ in(sK12(sK36(X0)),sK36(X0))
| empty_set = sK36(X0)
| ~ element(sK36(X0),sF44)
| ~ in(empty_set,omega)
| ~ in(sK12(sK36(X0)),sK36(X0))
| ~ sP2(X0) ),
inference(resolution,[],[f766,f297]) ).
fof(f1014,plain,
! [X0] :
( ~ sP2(X0)
| ~ in(sK12(sK36(X0)),sK36(X0))
| empty_set = sK36(X0)
| ~ element(sK36(X0),sF44)
| ~ in(empty_set,omega) ),
inference(duplicate_literal_removal,[],[f1012]) ).
fof(f1015,plain,
! [X0] :
( ~ sP2(X0)
| empty_set = sK36(X0)
| ~ element(sK36(X0),sF44)
| ~ in(empty_set,omega) ),
inference(forward_subsumption_resolution,[],[f1014,f344]) ).
fof(f1016,plain,
! [X0] :
( ~ element(sK36(X0),sF44)
| ~ sP2(X0)
| ~ in(empty_set,omega) ),
inference(forward_subsumption_resolution,[],[f1015,f299]) ).
fof(f1080,plain,
! [X0,X1] :
( sK14(sK36(X0)) = sK37(X1,sK14(sK36(X0)))
| ~ in(sK37(X1,sK14(sK36(X0))),sK36(X0))
| ~ sP2(X0)
| empty_set = X0
| ~ in(X0,omega)
| ~ being_limit_ordinal(X0)
| sP0(X0)
| ~ ordinal(X0)
| ~ in(sK14(sK36(X0)),sK36(X1))
| ~ sP2(X1) ),
inference(resolution,[],[f714,f296]) ).
fof(f1081,plain,
! [X0,X1] :
( ~ in(sK37(X1,sK14(sK36(X0))),sK36(X0))
| ~ sP2(X0)
| empty_set = X0
| ~ in(X0,omega)
| ~ being_limit_ordinal(X0)
| sP0(X0)
| ~ ordinal(X0)
| ~ in(sK14(sK36(X0)),sK36(X1))
| ~ sP2(X1) ),
inference(forward_subsumption_resolution,[],[f1080,f298]) ).
fof(f1276,plain,
( ~ element(sK10,sF42)
| empty_set = sK10
| sP3
| ~ in(sK38(sK10),sK10)
| ~ in(sK38(sK10),sK10) ),
inference(resolution,[],[f960,f180]) ).
fof(f1278,plain,
( ~ element(sK10,sF42)
| empty_set = sK10
| sP3
| ~ in(sK38(sK10),sK10) ),
inference(duplicate_literal_removal,[],[f1276]) ).
fof(f1279,plain,
( ~ element(sK10,sF42)
| empty_set = sK10
| sP3 ),
inference(forward_subsumption_resolution,[],[f1278,f839]) ).
fof(f1280,plain,
( empty_set = sK10
| sP3 ),
inference(forward_subsumption_resolution,[],[f1279,f339]) ).
fof(f1281,plain,
sP3,
inference(forward_subsumption_resolution,[],[f1280,f182]) ).
fof(f1301,plain,
! [X0,X1] :
( sK13(sK36(set_union2(X0,singleton(X0)))) = sK37(X1,sK13(sK36(set_union2(X0,singleton(X0)))))
| ~ in(sK37(X1,sK13(sK36(set_union2(X0,singleton(X0))))),sK36(set_union2(X0,singleton(X0))))
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| sP1(X0)
| ~ ordinal(X0)
| ~ in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(X1))
| ~ sP2(X1) ),
inference(resolution,[],[f712,f296]) ).
fof(f1302,plain,
! [X0,X1] :
( ~ in(sK37(X1,sK13(sK36(set_union2(X0,singleton(X0))))),sK36(set_union2(X0,singleton(X0))))
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| sP1(X0)
| ~ ordinal(X0)
| ~ in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(X1))
| ~ sP2(X1) ),
inference(forward_subsumption_resolution,[],[f1301,f298]) ).
fof(f1537,plain,
! [X0] :
( ~ sP1(X0)
| ordinal(X0) ),
inference(resolution,[],[f531,f272]) ).
fof(f1750,plain,
( ~ sP2(empty_set)
| ~ sP2(empty_set)
| ~ in(empty_set,omega) ),
inference(resolution,[],[f710,f1016]) ).
fof(f1758,plain,
( ~ in(empty_set,omega)
| ~ sP2(empty_set) ),
inference(duplicate_literal_removal,[],[f1750]) ).
fof(f2041,plain,
! [X0] :
( ~ in(sK6(X0),sK34)
| ~ sP3
| ~ sP0(X0)
| element(sK35(sK7(X0)),sK7(X0)) ),
inference(resolution,[],[f878,f311]) ).
fof(f2043,plain,
! [X0] :
( ~ in(sK6(X0),sK34)
| ~ sP3
| ~ sP0(X0)
| ~ empty(sK7(X0)) ),
inference(resolution,[],[f878,f317]) ).
fof(f2044,plain,
! [X0] :
( ~ in(sK6(X0),sK34)
| ~ sP0(X0)
| ~ empty(sK7(X0)) ),
inference(forward_subsumption_resolution,[],[f2043,f1281]) ).
fof(f2046,plain,
! [X0] :
( element(sK35(sK7(X0)),sK7(X0))
| ~ sP0(X0)
| ~ in(sK6(X0),sK34) ),
inference(forward_subsumption_resolution,[],[f2041,f1281]) ).
fof(f2058,plain,
! [X0] :
( ~ in(X0,sK34)
| ~ ordinal(X0)
| ~ sP3
| ~ sP1(X0)
| element(sK35(sK4(X0)),sK4(X0)) ),
inference(resolution,[],[f876,f311]) ).
fof(f2060,plain,
! [X0] :
( ~ in(X0,sK34)
| ~ ordinal(X0)
| ~ sP3
| ~ sP1(X0)
| ~ empty(sK4(X0)) ),
inference(resolution,[],[f876,f317]) ).
fof(f2061,plain,
! [X0] :
( ~ in(X0,sK34)
| ~ ordinal(X0)
| ~ sP1(X0)
| ~ empty(sK4(X0)) ),
inference(forward_subsumption_resolution,[],[f2060,f1281]) ).
fof(f2063,plain,
! [X0] :
( ~ in(X0,sK34)
| ~ ordinal(X0)
| ~ sP1(X0)
| element(sK35(sK4(X0)),sK4(X0)) ),
inference(forward_subsumption_resolution,[],[f2058,f1281]) ).
fof(f2064,plain,
! [X0] :
( ~ empty(sK4(X0))
| ~ sP1(X0)
| ~ in(X0,sK34) ),
inference(forward_subsumption_resolution,[],[f2061,f1537]) ).
fof(f2066,plain,
! [X0] :
( element(sK35(sK4(X0)),sK4(X0))
| ~ sP1(X0)
| ~ in(X0,sK34) ),
inference(forward_subsumption_resolution,[],[f2063,f1537]) ).
fof(f2079,plain,
! [X0] :
( ~ sP1(X0)
| ~ in(X0,sK34)
| in(sK35(sK4(X0)),sK4(X0))
| empty(sK4(X0)) ),
inference(resolution,[],[f2066,f312]) ).
fof(f2083,plain,
! [X0] :
( in(sK35(sK4(X0)),sK4(X0))
| ~ in(X0,sK34)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f2079,f2064]) ).
fof(f2105,plain,
! [X0] :
( ~ sP0(X0)
| ~ in(sK6(X0),sK34)
| in(sK35(sK7(X0)),sK7(X0))
| empty(sK7(X0)) ),
inference(resolution,[],[f2046,f312]) ).
fof(f2109,plain,
! [X0] :
( in(sK35(sK7(X0)),sK7(X0))
| ~ in(sK6(X0),sK34)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f2105,f2044]) ).
fof(f2200,plain,
! [X0,X1] :
( ~ in(sK8(X0,sK35(sK7(X1))),sK7(X1))
| sK35(sK7(X1)) = sK8(X0,sK35(sK7(X1)))
| ~ in(sK6(X1),sK34)
| ~ sP3
| ~ sP0(X1)
| ~ in(sK35(sK7(X1)),sK7(X0))
| ~ sP0(X0) ),
inference(resolution,[],[f934,f166]) ).
fof(f2205,plain,
! [X0,X1] :
( ~ in(sK8(X0,sK35(sK7(X1))),sK7(X1))
| ~ in(sK6(X1),sK34)
| ~ sP3
| ~ sP0(X1)
| ~ in(sK35(sK7(X1)),sK7(X0))
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f2200,f168]) ).
fof(f2209,plain,
! [X0,X1] :
( ~ in(sK8(X0,sK35(sK7(X1))),sK7(X1))
| ~ in(sK6(X1),sK34)
| ~ sP0(X1)
| ~ in(sK35(sK7(X1)),sK7(X0))
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f2205,f1281]) ).
fof(f2256,plain,
! [X0,X1] :
( ~ in(sK5(X0,sK35(sK4(X1))),sK4(X1))
| sK35(sK4(X1)) = sK5(X0,sK35(sK4(X1)))
| ~ in(X1,sK34)
| ~ ordinal(X1)
| ~ sP3
| ~ sP1(X1)
| ~ in(sK35(sK4(X1)),sK4(X0))
| ~ sP1(X0) ),
inference(resolution,[],[f932,f158]) ).
fof(f2263,plain,
! [X0,X1] :
( ~ in(sK5(X0,sK35(sK4(X1))),sK4(X1))
| ~ in(X1,sK34)
| ~ ordinal(X1)
| ~ sP3
| ~ sP1(X1)
| ~ in(sK35(sK4(X1)),sK4(X0))
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f2256,f160]) ).
fof(f2267,plain,
! [X0,X1] :
( ~ in(sK5(X0,sK35(sK4(X1))),sK4(X1))
| ~ in(X1,sK34)
| ~ ordinal(X1)
| ~ sP1(X1)
| ~ in(sK35(sK4(X1)),sK4(X0))
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f2263,f1281]) ).
fof(f2271,plain,
! [X0,X1] :
( ~ in(sK5(X0,sK35(sK4(X1))),sK4(X1))
| ~ in(X1,sK34)
| ~ sP1(X1)
| ~ in(sK35(sK4(X1)),sK4(X0))
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f2267,f1537]) ).
fof(f2619,plain,
! [X0] :
( ~ in(X0,sK34)
| ~ sP1(X0)
| ~ in(sK35(sK4(X0)),sK4(X0))
| ~ sP1(X0)
| ~ in(sK35(sK4(X0)),sK4(X0))
| ~ sP1(X0) ),
inference(resolution,[],[f2271,f159]) ).
fof(f2620,plain,
! [X0] :
( ~ in(X0,sK34)
| ~ sP1(X0)
| ~ in(sK35(sK4(X0)),sK4(X0)) ),
inference(duplicate_literal_removal,[],[f2619]) ).
fof(f2621,plain,
! [X0] :
( ~ in(X0,sK34)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f2620,f2083]) ).
fof(f2676,plain,
! [X0] :
( ~ in(sK6(X0),sK34)
| ~ sP0(X0)
| ~ in(sK35(sK7(X0)),sK7(X0))
| ~ sP0(X0)
| ~ in(sK35(sK7(X0)),sK7(X0))
| ~ sP0(X0) ),
inference(resolution,[],[f2209,f167]) ).
fof(f2677,plain,
! [X0] :
( ~ in(sK6(X0),sK34)
| ~ sP0(X0)
| ~ in(sK35(sK7(X0)),sK7(X0)) ),
inference(duplicate_literal_removal,[],[f2676]) ).
fof(f2678,plain,
! [X0] :
( ~ in(sK6(X0),sK34)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f2677,f2109]) ).
fof(f2679,plain,
( ~ sP0(sK34)
| ~ sP0(sK34) ),
inference(resolution,[],[f2678,f163]) ).
fof(f2680,plain,
~ sP0(sK34),
inference(duplicate_literal_removal,[],[f2679]) ).
fof(f3074,plain,
! [X0] :
( ~ sP2(X0)
| empty_set = X0
| ~ in(X0,omega)
| ~ being_limit_ordinal(X0)
| sP0(X0)
| ~ ordinal(X0)
| ~ in(sK14(sK36(X0)),sK36(X0))
| ~ sP2(X0)
| ~ in(sK14(sK36(X0)),sK36(X0))
| ~ sP2(X0) ),
inference(resolution,[],[f1081,f297]) ).
fof(f3075,plain,
! [X0] :
( ~ sP2(X0)
| empty_set = X0
| ~ in(X0,omega)
| ~ being_limit_ordinal(X0)
| sP0(X0)
| ~ ordinal(X0)
| ~ in(sK14(sK36(X0)),sK36(X0)) ),
inference(duplicate_literal_removal,[],[f3074]) ).
fof(f3076,plain,
! [X0] :
( ~ in(X0,omega)
| empty_set = X0
| ~ sP2(X0)
| ~ being_limit_ordinal(X0)
| sP0(X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[],[f3075,f713]) ).
fof(f3083,plain,
( empty_set = sK34
| ~ sP2(sK34)
| ~ being_limit_ordinal(sK34)
| sP0(sK34)
| ~ ordinal(sK34)
| ~ sP3 ),
inference(resolution,[],[f3076,f293]) ).
fof(f3095,plain,
( empty_set = sK34
| ~ being_limit_ordinal(sK34)
| sP0(sK34)
| ~ ordinal(sK34)
| ~ sP3 ),
inference(forward_subsumption_resolution,[],[f3083,f294]) ).
fof(f3099,plain,
( empty_set = sK34
| ~ being_limit_ordinal(sK34)
| ~ ordinal(sK34)
| ~ sP3 ),
inference(forward_subsumption_resolution,[],[f3095,f2680]) ).
fof(f3100,plain,
( empty_set = sK34
| ~ being_limit_ordinal(sK34)
| ~ sP3 ),
inference(forward_subsumption_resolution,[],[f3099,f290]) ).
fof(f3101,plain,
( ~ being_limit_ordinal(sK34)
| empty_set = sK34 ),
inference(forward_subsumption_resolution,[],[f3100,f1281]) ).
fof(f3102,plain,
( empty_set = sK34
| sK34 = set_union2(sK40(sK34),singleton(sK40(sK34)))
| ~ sP3 ),
inference(resolution,[],[f3101,f802]) ).
fof(f3103,plain,
( sK34 = set_union2(sK40(sK34),singleton(sK40(sK34)))
| empty_set = sK34 ),
inference(forward_subsumption_resolution,[],[f3102,f1281]) ).
fof(f3112,plain,
( in(sK40(sK34),sK34)
| empty_set = sK34 ),
inference(superposition,[],[f331,f3103]) ).
fof(f3120,plain,
( element(sK40(sK34),sK34)
| empty_set = sK34 ),
inference(superposition,[],[f544,f3103]) ).
fof(f3142,plain,
( ~ sP1(sK40(sK34))
| empty_set = sK34 ),
inference(resolution,[],[f3112,f2621]) ).
fof(f3167,plain,
( ordinal(sK40(sK34))
| empty_set = sK34
| ~ ordinal(sK34) ),
inference(resolution,[],[f3120,f268]) ).
fof(f3686,plain,
! [X0] :
( ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| sP1(X0)
| ~ ordinal(X0)
| ~ in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(set_union2(X0,singleton(X0))))
| ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(set_union2(X0,singleton(X0))))
| ~ sP2(set_union2(X0,singleton(X0))) ),
inference(resolution,[],[f1302,f297]) ).
fof(f3689,plain,
! [X0] :
( ~ sP2(set_union2(X0,singleton(X0)))
| ~ in(set_union2(X0,singleton(X0)),omega)
| sP1(X0)
| ~ ordinal(X0)
| ~ in(sK13(sK36(set_union2(X0,singleton(X0)))),sK36(set_union2(X0,singleton(X0)))) ),
inference(duplicate_literal_removal,[],[f3686]) ).
fof(f3691,plain,
! [X0] :
( ~ in(set_union2(X0,singleton(X0)),omega)
| ~ sP2(set_union2(X0,singleton(X0)))
| sP1(X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[],[f3689,f711]) ).
fof(f3694,plain,
( ~ in(sK34,omega)
| ~ sP2(sK34)
| sP1(sK40(sK34))
| ~ ordinal(sK40(sK34))
| empty_set = sK34 ),
inference(superposition,[],[f3691,f3103]) ).
fof(f3695,plain,
( ~ ordinal(sK40(sK34))
| ~ sP2(sK34)
| ~ in(sK34,omega)
| empty_set = sK34 ),
inference(forward_subsumption_resolution,[],[f3694,f3142]) ).
fof(f3703,plain,
( ~ sP2(sK34)
| ~ in(sK34,omega)
| empty_set = sK34
| empty_set = sK34
| ~ ordinal(sK34) ),
inference(resolution,[],[f3695,f3167]) ).
fof(f3705,plain,
( ~ in(sK34,omega)
| ~ sP2(sK34)
| empty_set = sK34
| ~ ordinal(sK34) ),
inference(duplicate_literal_removal,[],[f3703]) ).
fof(f3732,plain,
( ~ sP2(sK34)
| empty_set = sK34
| ~ ordinal(sK34)
| ~ sP3 ),
inference(resolution,[],[f3705,f293]) ).
fof(f3734,plain,
( empty_set = sK34
| ~ ordinal(sK34)
| ~ sP3 ),
inference(forward_subsumption_resolution,[],[f3732,f294]) ).
fof(f3735,plain,
( empty_set = sK34
| ~ sP3 ),
inference(forward_subsumption_resolution,[],[f3734,f290]) ).
fof(f3736,plain,
empty_set = sK34,
inference(forward_subsumption_resolution,[],[f3735,f1281]) ).
fof(f3741,plain,
( in(empty_set,omega)
| ~ sP3 ),
inference(superposition,[],[f293,f3736]) ).
fof(f3742,plain,
( sP2(empty_set)
| ~ sP3 ),
inference(superposition,[],[f294,f3736]) ).
fof(f3770,plain,
sP2(empty_set),
inference(forward_subsumption_resolution,[],[f3742,f1281]) ).
fof(f3771,plain,
in(empty_set,omega),
inference(forward_subsumption_resolution,[],[f3741,f1281]) ).
fof(f3793,plain,
~ sP2(empty_set),
inference(resolution,[],[f3771,f1758]) ).
fof(f3798,plain,
$false,
inference(forward_subsumption_resolution,[],[f3793,f3770]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU301+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n019.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 28 04:34:48 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.44/3.37 % (3660943)Will run a generic schedule for satisfiability detection.
% 20.44/3.37 % (3660951)dis+10_1_sil=32000:sp=arity:random_seed=3867192477:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 20.44/3.37 % (3660949)% WARNING: option uhcvi not known.
% 20.44/3.37 % (3660948)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3353334499_2999 on theBenchmark for (2999ds/0Mi)
% 20.44/3.37 % (3660950)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3856110494:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 20.44/3.37 % (3660952)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1885853975:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 20.44/3.37 % (3660953)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=267059174:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 20.44/3.37 % (3660954)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=749319435:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 20.44/3.37 % (3660949)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1723649172:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 20.44/3.37 % TRYING [1]
% 20.44/3.37 % TRYING [2]
% 20.44/3.37 % TRYING [3]
% 20.44/3.37 % TRYING [4]
% 20.44/3.37 % (3660951)Instruction limit reached!
% 20.44/3.37 % (3660951)------------------------------
% 20.44/3.37 % (3660951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.44/3.37 % (3660951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.37 % (3660951)CaDiCaL version: 2.1.3
% 20.44/3.37 % (3660951)Termination reason: Instruction limit
% 20.44/3.37 % (3660951)Termination phase: Saturation
% 20.44/3.37 % (3660951)Time elapsed: 0.038 s
% 20.44/3.37 % (3660951)Peak memory usage: 13 MB
% 20.44/3.37 % (3660951)Instructions burned: 104 (million)
% 20.44/3.37 % TRYING [5]
% 20.44/3.37 % (3660962)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4030373984:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 20.44/3.37 % TRYING [1]
% 20.44/3.37 % TRYING [2]
% 20.44/3.37 % TRYING [3]
% 20.44/3.37 % TRYING [4]
% 20.44/3.37 % TRYING [5]
% 20.44/3.37 % (3660952)Instruction limit reached!
% 20.44/3.37 % (3660952)------------------------------
% 20.44/3.37 % (3660952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.44/3.37 % (3660952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.37 % (3660952)CaDiCaL version: 2.1.3
% 20.44/3.37 % (3660952)Termination reason: Instruction limit
% 20.44/3.37 % (3660952)Termination phase: Saturation
% 20.44/3.37 % (3660952)Time elapsed: 0.066 s
% 20.44/3.37 % (3660952)Peak memory usage: 13 MB
% 20.44/3.37 % (3660952)Instructions burned: 117 (million)
% 20.44/3.37 % (3660953)Instruction limit reached!
% 20.44/3.37 % (3660953)------------------------------
% 20.44/3.37 % (3660953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.44/3.37 % (3660953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.37 % (3660953)CaDiCaL version: 2.1.3
% 20.44/3.37 % (3660953)Termination reason: Instruction limit
% 20.44/3.37 % (3660953)Termination phase: Saturation
% 20.44/3.37 % (3660953)Time elapsed: 0.085 s
% 20.44/3.37 % (3660953)Peak memory usage: 13 MB
% 20.44/3.37 % (3660953)Instructions burned: 132 (million)
% 20.44/3.37 % (3660964)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=172553801:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 20.44/3.37 % (3660954)Instruction limit reached!
% 20.44/3.37 % (3660954)------------------------------
% 20.44/3.37 % (3660954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.44/3.37 % (3660954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.37 % (3660954)CaDiCaL version: 2.1.3
% 20.44/3.37 % (3660954)Termination reason: Instruction limit
% 20.44/3.37 % (3660954)Termination phase: Saturation
% 20.44/3.37 % (3660954)Time elapsed: 0.089 s
% 20.44/3.37 % (3660954)Peak memory usage: 14 MB
% 20.44/3.37 % (3660954)Instructions burned: 164 (million)
% 20.44/3.37 % (3660965)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3694562340:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 20.44/3.37 % (3660967)ott-21_1_sil=16000:fs=off:random_seed=1290114001:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 20.44/3.37 % (3660964)Instruction limit reached!
% 20.44/3.37 % (3660964)------------------------------
% 20.44/3.37 % (3660964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660964)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660964)Termination reason: Instruction limit
% 9.32/4.21 % (3660964)Termination phase: Saturation
% 9.32/4.21 % (3660964)Time elapsed: 0.088 s
% 9.32/4.21 % (3660964)Peak memory usage: 14 MB
% 9.32/4.21 % (3660964)Instructions burned: 132 (million)
% 9.32/4.21 % (3660970)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1676246653:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 9.32/4.21 % (3660967)Instruction limit reached!
% 9.32/4.21 % (3660967)------------------------------
% 9.32/4.21 % (3660967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660967)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660967)Termination reason: Instruction limit
% 9.32/4.21 % (3660967)Termination phase: Saturation
% 9.32/4.21 % (3660967)Time elapsed: 0.097 s
% 9.32/4.21 % (3660967)Peak memory usage: 13 MB
% 9.32/4.21 % (3660967)Instructions burned: 180 (million)
% 9.32/4.21 % (3660972)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1265203413:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 9.32/4.21 % TRYING [1]
% 9.32/4.21 % TRYING [2]
% 9.32/4.21 % TRYING [3]
% 9.32/4.21 % (3660962)Instruction limit reached!
% 9.32/4.21 % (3660962)------------------------------
% 9.32/4.21 % (3660962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660962)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660962)Termination reason: Instruction limit
% 9.32/4.21 % (3660962)Termination phase: Finite model building SAT solving
% 9.32/4.21 % (3660962)Time elapsed: 0.202 s
% 9.32/4.21 % (3660962)Peak memory usage: 16 MB
% 9.32/4.21 % (3660962)Instructions burned: 717 (million)
% 9.32/4.21 % TRYING [4]
% 9.32/4.21 % (3660974)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3363647688:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 9.32/4.21 % TRYING [5]
% 9.32/4.21 % TRYING [6]
% 9.32/4.21 % (3660965)Instruction limit reached!
% 9.32/4.21 % (3660965)------------------------------
% 9.32/4.21 % (3660965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660965)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660965)Termination reason: Instruction limit
% 9.32/4.21 % (3660965)Termination phase: Saturation
% 9.32/4.21 % (3660965)Time elapsed: 0.340 s
% 9.32/4.21 % (3660965)Peak memory usage: 18 MB
% 9.32/4.21 % (3660965)Instructions burned: 684 (million)
% 9.32/4.21 % TRYING [6]
% 9.32/4.21 % (3660976)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1293464582:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 9.32/4.21 % TRYING [14]
% 9.32/4.21 % (3660970)Instruction limit reached!
% 9.32/4.21 % (3660970)------------------------------
% 9.32/4.21 % (3660970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660970)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660970)Termination reason: Instruction limit
% 9.32/4.21 % (3660970)Termination phase: Saturation
% 9.32/4.21 % (3660970)Time elapsed: 0.305 s
% 9.32/4.21 % (3660970)Peak memory usage: 15 MB
% 9.32/4.21 % (3660970)Instructions burned: 477 (million)
% 9.32/4.21 % (3660978)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2885137051:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 9.32/4.21 % (3660974)Instruction limit reached!
% 9.32/4.21 % (3660974)------------------------------
% 9.32/4.21 % (3660974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660974)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660974)Termination reason: Instruction limit
% 9.32/4.21 % (3660974)Termination phase: Saturation
% 9.32/4.21 % (3660974)Time elapsed: 0.364 s
% 9.32/4.21 % (3660974)Peak memory usage: 27 MB
% 9.32/4.21 % (3660974)Instructions burned: 1179 (million)
% 9.32/4.21 % (3660980)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3649927910:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 9.32/4.21 % (3660972)Instruction limit reached!
% 9.32/4.21 % (3660972)------------------------------
% 9.32/4.21 % (3660972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660972)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660972)Termination reason: Instruction limit
% 9.32/4.21 % (3660972)Termination phase: Finite model building SAT solving
% 9.32/4.21 % (3660972)Time elapsed: 0.474 s
% 9.32/4.21 % (3660972)Peak memory usage: 15 MB
% 9.32/4.21 % (3660972)Instructions burned: 865 (million)
% 9.32/4.21 % (3660982)fmb+10_1_sil=64000:random_seed=2576872881:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 9.32/4.21 % TRYING [1]
% 9.32/4.21 % TRYING [2]
% 9.32/4.21 % TRYING [3]
% 9.32/4.21 % TRYING [4]
% 9.32/4.21 % TRYING [5]
% 9.32/4.21 % (3660976)Instruction limit reached!
% 9.32/4.21 % (3660976)------------------------------
% 9.32/4.21 % (3660976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660976)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660976)Termination reason: Instruction limit
% 9.32/4.21 % (3660976)Termination phase: Finite model building SAT solving
% 9.32/4.21 % (3660976)Time elapsed: 0.369 s
% 9.32/4.21 % (3660976)Peak memory usage: 49 MB
% 9.32/4.21 % (3660976)Instructions burned: 890 (million)
% 9.32/4.21 % (3660984)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=917577812:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 9.32/4.21 % TRYING [20]
% 9.32/4.21 % (3660980)Instruction limit reached!
% 9.32/4.21 % (3660980)------------------------------
% 9.32/4.21 % (3660980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660980)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660980)Termination reason: Instruction limit
% 9.32/4.21 % (3660980)Termination phase: Saturation
% 9.32/4.21 % (3660980)Time elapsed: 0.256 s
% 9.32/4.21 % (3660980)Peak memory usage: 19 MB
% 9.32/4.21 % (3660980)Instructions burned: 880 (million)
% 9.32/4.21 % (3660986)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2930944034:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 9.32/4.21 % TRYING [8]
% 9.32/4.21 % (3660978)Instruction limit reached!
% 9.32/4.21 % (3660978)------------------------------
% 9.32/4.21 % (3660978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660978)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660978)Termination reason: Instruction limit
% 9.32/4.21 % (3660978)Termination phase: Saturation
% 9.32/4.21 % (3660978)Time elapsed: 0.423 s
% 9.32/4.21 % (3660978)Peak memory usage: 20 MB
% 9.32/4.21 % (3660978)Instructions burned: 692 (million)
% 9.32/4.21 % (3660988)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1057153242:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 9.32/4.21 % TRYING [6]
% 9.32/4.21 % (3660986)Instruction limit reached!
% 9.32/4.21 % (3660986)------------------------------
% 9.32/4.21 % (3660986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660986)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660986)Termination reason: Instruction limit
% 9.32/4.21 % (3660986)Termination phase: Finite model building SAT solving
% 9.32/4.21 % (3660986)Time elapsed: 0.254 s
% 9.32/4.21 % (3660986)Peak memory usage: 27 MB
% 9.32/4.21 % (3660986)Instructions burned: 924 (million)
% 9.32/4.21 % (3660990)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1128279150:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 9.32/4.21 % (3660990)Instruction limit reached!
% 9.32/4.21 % (3660990)------------------------------
% 9.32/4.21 % (3660990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660990)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660990)Termination reason: Instruction limit
% 9.32/4.21 % (3660990)Termination phase: Saturation
% 9.32/4.21 % (3660990)Time elapsed: 0.529 s
% 9.32/4.21 % (3660990)Peak memory usage: 26 MB
% 9.32/4.21 % (3660990)Instructions burned: 1473 (million)
% 9.32/4.21 % (3660992)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=546779623:i=6324_2982 on theBenchmark for (2982ds/6324Mi)
% 9.32/4.21 % TRYING [77]
% 9.32/4.21 % (3660992)Instruction limit reached!
% 9.32/4.21 % (3660992)------------------------------
% 9.32/4.21 % (3660992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660992)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660992)Termination reason: Instruction limit
% 9.32/4.21 % (3660992)Termination phase: Finite model building constraint generation
% 9.32/4.21 % (3660992)Time elapsed: 1.202 s
% 9.32/4.21 % (3660992)Peak memory usage: 421 MB
% 9.32/4.21 % (3660992)Instructions burned: 6328 (million)
% 9.32/4.21 % (3660994)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3276542526:fmbsr=2.30978:i=2174_2970 on theBenchmark for (2970ds/2174Mi)
% 9.32/4.21 % TRYING [16]
% 9.32/4.21 % (3660994)Instruction limit reached!
% 9.32/4.21 % (3660994)------------------------------
% 9.32/4.21 % (3660994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660994)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660994)Termination reason: Instruction limit
% 9.32/4.21 % (3660994)Termination phase: Finite model building constraint generation
% 9.32/4.21 % (3660994)Time elapsed: 0.452 s
% 9.32/4.21 % (3660994)Peak memory usage: 168 MB
% 9.32/4.21 % (3660994)Instructions burned: 2177 (million)
% 9.32/4.21 % (3660996)ott-2_1_sil=16000:newcnf=on:random_seed=1157137188:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2965 on theBenchmark for (2965ds/869Mi)
% 9.32/4.21 % (3660988)Instruction limit reached!
% 9.32/4.21 % (3660988)------------------------------
% 9.32/4.21 % (3660988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660988)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660988)Termination reason: Instruction limit
% 9.32/4.21 % (3660988)Termination phase: Saturation
% 9.32/4.21 % (3660988)Time elapsed: 2.602 s
% 9.32/4.21 % (3660988)Peak memory usage: 20 MB
% 9.32/4.21 % (3660988)Instructions burned: 5132 (million)
% 9.32/4.21 % (3660998)ott+10_1_sil=32000:tgt=ground:random_seed=5747926:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi)
% 9.32/4.21 % (3660996)Instruction limit reached!
% 9.32/4.21 % (3660996)------------------------------
% 9.32/4.21 % (3660996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.21 % (3660996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.21 % (3660996)CaDiCaL version: 2.1.3
% 9.32/4.21 % (3660996)Termination reason: Instruction limit
% 9.32/4.21 % (3660996)Termination phase: Saturation
% 9.32/4.21 % (3660996)Time elapsed: 0.228 s
% 9.32/4.21 % (3660996)Peak memory usage: 15 MB
% 9.32/4.21 % (3660996)Instructions burned: 869 (million)
% 9.32/4.21 % (3661000)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=316969978:i=54282_2962 on theBenchmark for (2962ds/54282Mi)
% 9.32/4.21 % TRYING [1]
% 9.32/4.21 % TRYING [2]
% 9.32/4.21 % TRYING [3]
% 9.32/4.21 % TRYING [4]
% 9.32/4.21 % TRYING [5]
% 9.32/4.21 % (3660998) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3660943-3660998"...
% 9.32/4.21 % (3660998)...printing done.
% 9.32/4.21 % (3660998)Refutation found. Thanks to Tanya!
% 9.32/4.21 % SZS status Theorem for theBenchmark
% 9.32/4.21 % SZS output start Proof for theBenchmark
% See solution above
% 9.32/4.22 % (3660998)------------------------------
% 9.32/4.22 % (3660998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.32/4.22 % (3660998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.32/4.22 % (3660998)CaDiCaL version: 2.1.3
% 9.32/4.22 % (3660998)Termination reason: Refutation
% 9.32/4.22 % (3660998)Time elapsed: 0.144 s
% 9.32/4.22 % (3660998)Peak memory usage: 14 MB
% 9.32/4.22 % (3660998)Instructions burned: 232 (million)
% 9.32/4.22 % (3660943)Success in time 3.803 s
% 9.32/4.22 % Vampire exiting
%------------------------------------------------------------------------------