%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU298+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:46 PM UTC 2026
% Result : Theorem 0.18s 0.50s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 15
% Syntax : Number of formulae : 138 ( 12 unt; 13 def)
% Number of atoms : 553 ( 113 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 659 ( 244 ~; 277 |; 109 &)
% ( 19 <=>; 8 =>; 0 <=; 2 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 18 ( 16 usr; 13 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-3 aty)
% Number of variables : 189 ( 0 sgn 115 !; 74 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1] :
( ( ordinal(X0)
& element(X1,powerset(powerset(succ(X0)))) )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(X3,powerset(X0))
& ? [X4] :
( in(X4,X1)
& X3 = set_difference(X4,singleton(X0)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e4_27_3_1__finset_1) ).
fof(f2,negated_conjecture,
~ ! [X0,X1] :
( ( ordinal(X0)
& element(X1,powerset(powerset(succ(X0)))) )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(X3,powerset(X0))
& ? [X4] :
( in(X4,X1)
& X3 = set_difference(X4,singleton(X0)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f43,axiom,
! [X0,X1] :
( ( ordinal(X0)
& element(X1,powerset(powerset(succ(X0)))) )
=> ( ! [X2,X3,X4] :
( ( X2 = X3
& ? [X5] :
( in(X5,X1)
& X3 = set_difference(X5,singleton(X0)) )
& X2 = X4
& ? [X6] :
( in(X6,X1)
& X4 = set_difference(X6,singleton(X0)) ) )
=> X3 = X4 )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ? [X4] :
( in(X4,powerset(X0))
& X4 = X3
& ? [X7] :
( in(X7,X1)
& X3 = set_difference(X7,singleton(X0)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e4_27_3_1__finset_1__1) ).
fof(f44,plain,
! [X0,X1] :
( ( ordinal(X0)
& element(X1,powerset(powerset(succ(X0)))) )
=> ( ! [X2,X3,X4] :
( ( X2 = X3
& ? [X5] :
( in(X5,X1)
& X3 = set_difference(X5,singleton(X0)) )
& X2 = X4
& ? [X6] :
( in(X6,X1)
& X4 = set_difference(X6,singleton(X0)) ) )
=> X3 = X4 )
=> ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,powerset(X0))
& X8 = X9
& ? [X10] :
( in(X10,X1)
& set_difference(X10,singleton(X0)) = X8 ) ) ) ) ),
inference(rectify,[],[f43]) ).
fof(f49,plain,
? [X0,X1] :
( ! [X2] :
? [X3] :
( in(X3,X2)
<~> ( in(X3,powerset(X0))
& ? [X4] :
( in(X4,X1)
& X3 = set_difference(X4,singleton(X0)) ) ) )
& ordinal(X0)
& element(X1,powerset(powerset(succ(X0)))) ),
inference(ennf_transformation,[],[f2]) ).
fof(f50,plain,
? [X0,X1] :
( ! [X2] :
? [X3] :
( in(X3,X2)
<~> ( in(X3,powerset(X0))
& ? [X4] :
( in(X4,X1)
& X3 = set_difference(X4,singleton(X0)) ) ) )
& ordinal(X0)
& element(X1,powerset(powerset(succ(X0)))) ),
inference(flattening,[],[f49]) ).
fof(f73,plain,
! [X0,X1] :
( ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,powerset(X0))
& X8 = X9
& ? [X10] :
( in(X10,X1)
& set_difference(X10,singleton(X0)) = X8 ) ) )
| ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5] :
( in(X5,X1)
& X3 = set_difference(X5,singleton(X0)) )
& X2 = X4
& ? [X6] :
( in(X6,X1)
& X4 = set_difference(X6,singleton(X0)) ) )
| ~ ordinal(X0)
| ~ element(X1,powerset(powerset(succ(X0)))) ),
inference(ennf_transformation,[],[f44]) ).
fof(f74,plain,
! [X0,X1] :
( ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,powerset(X0))
& X8 = X9
& ? [X10] :
( in(X10,X1)
& set_difference(X10,singleton(X0)) = X8 ) ) )
| ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5] :
( in(X5,X1)
& X3 = set_difference(X5,singleton(X0)) )
& X2 = X4
& ? [X6] :
( in(X6,X1)
& X4 = set_difference(X6,singleton(X0)) ) )
| ~ ordinal(X0)
| ~ element(X1,powerset(powerset(succ(X0)))) ),
inference(flattening,[],[f73]) ).
fof(f75,definition,
! [X1,X0] :
( ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5] :
( in(X5,X1)
& X3 = set_difference(X5,singleton(X0)) )
& X2 = X4
& ? [X6] :
( in(X6,X1)
& X4 = set_difference(X6,singleton(X0)) ) )
| ~ sP0(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f76,plain,
! [X0,X1] :
( ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,powerset(X0))
& X8 = X9
& ? [X10] :
( in(X10,X1)
& set_difference(X10,singleton(X0)) = X8 ) ) )
| sP0(X1,X0)
| ~ ordinal(X0)
| ~ element(X1,powerset(powerset(succ(X0)))) ),
inference(definition_folding,[],[f74,f75]) ).
fof(f77,plain,
? [X0,X1] :
( ! [X2] :
? [X3] :
( ( ~ in(X3,powerset(X0))
| ! [X4] :
( ~ in(X4,X1)
| set_difference(X4,singleton(X0)) != X3 )
| ~ in(X3,X2) )
& ( ( in(X3,powerset(X0))
& ? [X4] :
( in(X4,X1)
& X3 = set_difference(X4,singleton(X0)) ) )
| in(X3,X2) ) )
& ordinal(X0)
& element(X1,powerset(powerset(succ(X0)))) ),
inference(nnf_transformation,[],[f50]) ).
fof(f78,plain,
? [X0,X1] :
( ! [X2] :
? [X3] :
( ( ~ in(X3,powerset(X0))
| ! [X4] :
( ~ in(X4,X1)
| set_difference(X4,singleton(X0)) != X3 )
| ~ in(X3,X2) )
& ( ( in(X3,powerset(X0))
& ? [X4] :
( in(X4,X1)
& X3 = set_difference(X4,singleton(X0)) ) )
| in(X3,X2) ) )
& ordinal(X0)
& element(X1,powerset(powerset(succ(X0)))) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
? [X0,X1] :
( ! [X2] :
? [X3] :
( ( ~ in(X3,powerset(X0))
| ! [X4] :
( ~ in(X4,X1)
| set_difference(X4,singleton(X0)) != X3 )
| ~ in(X3,X2) )
& ( ( in(X3,powerset(X0))
& ? [X5] :
( in(X5,X1)
& set_difference(X5,singleton(X0)) = X3 ) )
| in(X3,X2) ) )
& ordinal(X0)
& element(X1,powerset(powerset(succ(X0)))) ),
inference(rectify,[],[f78]) ).
fof(f80,plain,
( ! [X2] :
( ( ~ in(sK3(X2),powerset(sK1))
| ! [X4] :
( ~ in(X4,sK2)
| sK3(X2) != set_difference(X4,singleton(sK1)) )
| ~ in(sK3(X2),X2) )
& ( ( in(sK3(X2),powerset(sK1))
& in(sK4(X2),sK2)
& sK3(X2) = set_difference(sK4(X2),singleton(sK1)) )
| in(sK3(X2),X2) ) )
& ordinal(sK1)
& element(sK2,powerset(powerset(succ(sK1)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X3,sK3(X2)),skolemize(X5,sK4(X2))],[f79]) ).
fof(f97,plain,
! [X1,X0] :
( ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5] :
( in(X5,X1)
& X3 = set_difference(X5,singleton(X0)) )
& X2 = X4
& ? [X6] :
( in(X6,X1)
& X4 = set_difference(X6,singleton(X0)) ) )
| ~ sP0(X1,X0) ),
inference(nnf_transformation,[],[f75]) ).
fof(f98,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5] :
( in(X5,X0)
& set_difference(X5,singleton(X1)) = X3 )
& X2 = X4
& ? [X6] :
( in(X6,X0)
& set_difference(X6,singleton(X1)) = X4 ) )
| ~ sP0(X0,X1) ),
inference(rectify,[],[f97]) ).
fof(f99,plain,
! [X0,X1] :
( ( sK22(X0,X1) != sK23(X0,X1)
& sK21(X0,X1) = sK22(X0,X1)
& in(sK24(X0,X1),X0)
& sK22(X0,X1) = set_difference(sK24(X0,X1),singleton(X1))
& sK21(X0,X1) = sK23(X0,X1)
& in(sK25(X0,X1),X0)
& sK23(X0,X1) = set_difference(sK25(X0,X1),singleton(X1)) )
| ~ sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22,sK23,sK24,sK25]),skolemize(X2,sK21(X0,X1)),skolemize(X3,sK22(X0,X1)),skolemize(X4,sK23(X0,X1)),skolemize(X5,sK24(X0,X1)),skolemize(X6,sK25(X0,X1))],[f98]) ).
fof(f100,plain,
! [X0,X1] :
( ? [X7] :
! [X8] :
( ( in(X8,X7)
| ! [X9] :
( ~ in(X9,powerset(X0))
| X8 != X9
| ! [X10] :
( ~ in(X10,X1)
| set_difference(X10,singleton(X0)) != X8 ) ) )
& ( ? [X9] :
( in(X9,powerset(X0))
& X8 = X9
& ? [X10] :
( in(X10,X1)
& set_difference(X10,singleton(X0)) = X8 ) )
| ~ in(X8,X7) ) )
| sP0(X1,X0)
| ~ ordinal(X0)
| ~ element(X1,powerset(powerset(succ(X0)))) ),
inference(nnf_transformation,[],[f76]) ).
fof(f101,plain,
! [X0,X1] :
( ? [X2] :
! [X3] :
( ( in(X3,X2)
| ! [X4] :
( ~ in(X4,powerset(X0))
| X3 != X4
| ! [X5] :
( ~ in(X5,X1)
| set_difference(X5,singleton(X0)) != X3 ) ) )
& ( ? [X6] :
( in(X6,powerset(X0))
& X3 = X6
& ? [X7] :
( in(X7,X1)
& set_difference(X7,singleton(X0)) = X3 ) )
| ~ in(X3,X2) ) )
| sP0(X1,X0)
| ~ ordinal(X0)
| ~ element(X1,powerset(powerset(succ(X0)))) ),
inference(rectify,[],[f100]) ).
fof(f102,plain,
! [X0,X1] :
( ! [X3] :
( ( in(X3,sK26(X0,X1))
| ! [X4] :
( ~ in(X4,powerset(X0))
| X3 != X4
| ! [X5] :
( ~ in(X5,X1)
| set_difference(X5,singleton(X0)) != X3 ) ) )
& ( ( in(sK27(X0,X1,X3),powerset(X0))
& sK27(X0,X1,X3) = X3
& in(sK28(X0,X1,X3),X1)
& set_difference(sK28(X0,X1,X3),singleton(X0)) = X3 )
| ~ in(X3,sK26(X0,X1)) ) )
| sP0(X1,X0)
| ~ ordinal(X0)
| ~ element(X1,powerset(powerset(succ(X0)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26,sK27,sK28]),skolemize(X2,sK26(X0,X1)),skolemize(X6,sK27(X0,X1,X3)),skolemize(X7,sK28(X0,X1,X3))],[f101]) ).
fof(f103,plain,
element(sK2,powerset(powerset(succ(sK1)))),
inference(cnf_transformation,[],[f80]) ).
fof(f104,plain,
ordinal(sK1),
inference(cnf_transformation,[],[f80]) ).
fof(f105,plain,
! [X2] :
( in(sK3(X2),X2)
| sK3(X2) = set_difference(sK4(X2),singleton(sK1)) ),
inference(cnf_transformation,[],[f80]) ).
fof(f106,plain,
! [X2] :
( in(sK4(X2),sK2)
| in(sK3(X2),X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f107,plain,
! [X2] :
( in(sK3(X2),powerset(sK1))
| in(sK3(X2),X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f108,plain,
! [X2,X4] :
( sK3(X2) != set_difference(X4,singleton(sK1))
| ~ in(X4,sK2)
| ~ in(sK3(X2),powerset(sK1))
| ~ in(sK3(X2),X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f196,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| sK21(X0,X1) = sK23(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f199,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| sK21(X0,X1) = sK22(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f200,plain,
! [X0,X1] :
( sK22(X0,X1) != sK23(X0,X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f201,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ in(X3,sK26(X0,X1))
| sP0(X1,X0)
| ~ ordinal(X0)
| set_difference(sK28(X0,X1,X3),singleton(X0)) = X3 ),
inference(cnf_transformation,[],[f102]) ).
fof(f202,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ in(X3,sK26(X0,X1))
| sP0(X1,X0)
| ~ ordinal(X0)
| in(sK28(X0,X1,X3),X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f203,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ in(X3,sK26(X0,X1))
| sP0(X1,X0)
| ~ ordinal(X0)
| sK27(X0,X1,X3) = X3 ),
inference(cnf_transformation,[],[f102]) ).
fof(f204,plain,
! [X3,X0,X1] :
( in(sK27(X0,X1,X3),powerset(X0))
| ~ in(X3,sK26(X0,X1))
| sP0(X1,X0)
| ~ ordinal(X0)
| ~ element(X1,powerset(powerset(succ(X0)))) ),
inference(cnf_transformation,[],[f102]) ).
fof(f205,plain,
! [X3,X0,X1,X4,X5] :
( in(X3,sK26(X0,X1))
| ~ in(X4,powerset(X0))
| X3 != X4
| ~ in(X5,X1)
| set_difference(X5,singleton(X0)) != X3
| sP0(X1,X0)
| ~ ordinal(X0)
| ~ element(X1,powerset(powerset(succ(X0)))) ),
inference(cnf_transformation,[],[f102]) ).
fof(f206,plain,
! [X0,X1,X4,X5] :
( in(X4,sK26(X0,X1))
| ~ in(X4,powerset(X0))
| ~ in(X5,X1)
| set_difference(X5,singleton(X0)) != X4
| sP0(X1,X0)
| ~ ordinal(X0)
| ~ element(X1,powerset(powerset(succ(X0)))) ),
inference(equality_resolution,[],[f205]) ).
fof(f207,plain,
! [X0,X1,X5] :
( in(set_difference(X5,singleton(X0)),sK26(X0,X1))
| ~ in(set_difference(X5,singleton(X0)),powerset(X0))
| ~ in(X5,X1)
| sP0(X1,X0)
| ~ ordinal(X0)
| ~ element(X1,powerset(powerset(succ(X0)))) ),
inference(equality_resolution,[],[f206]) ).
fof(f331,plain,
! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| sP0(sK2,sK1)
| ~ ordinal(sK1)
| in(sK28(sK1,sK2,X0),sK2) ),
inference(resolution,[],[f202,f103]) ).
fof(f338,plain,
! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| sP0(sK2,sK1)
| in(sK28(sK1,sK2,X0),sK2) ),
inference(forward_subsumption_resolution,[],[f331,f104]) ).
fof(f340,definition,
( spl29_5
<=> sP0(sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f341,plain,
( ~ sP0(sK2,sK1)
| spl29_5 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f342,plain,
( sP0(sK2,sK1)
| ~ spl29_5 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f344,definition,
( spl29_6
<=> ! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| in(sK28(sK1,sK2,X0),sK2) ) ),
introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).
fof(f345,plain,
( ! [X0] :
( in(sK28(sK1,sK2,X0),sK2)
| ~ in(X0,sK26(sK1,sK2)) )
| ~ spl29_6 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f346,plain,
( spl29_5
| spl29_6 ),
inference(avatar_split_clause,[],[f338,f344,f340]) ).
fof(f349,plain,
( sK22(sK2,sK1) = sK21(sK2,sK1)
| ~ spl29_5 ),
inference(resolution,[],[f342,f199]) ).
fof(f350,plain,
( sK23(sK2,sK1) = sK21(sK2,sK1)
| ~ spl29_5 ),
inference(resolution,[],[f342,f196]) ).
fof(f351,plain,
! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| sP0(sK2,sK1)
| ~ ordinal(sK1)
| sK27(sK1,sK2,X0) = X0 ),
inference(resolution,[],[f203,f103]) ).
fof(f359,plain,
( sK22(sK2,sK1) != sK21(sK2,sK1)
| ~ sP0(sK2,sK1)
| ~ spl29_5 ),
inference(superposition,[],[f200,f350]) ).
fof(f360,plain,
( ~ sP0(sK2,sK1)
| ~ spl29_5 ),
inference(forward_subsumption_resolution,[],[f359,f349]) ).
fof(f361,plain,
( $false
| ~ spl29_5 ),
inference(forward_subsumption_resolution,[],[f360,f342]) ).
fof(f362,plain,
~ spl29_5,
inference(avatar_contradiction_clause,[],[f361]) ).
fof(f363,plain,
! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| sP0(sK2,sK1)
| sK27(sK1,sK2,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f351,f104]) ).
fof(f365,definition,
( spl29_7
<=> ! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| sK27(sK1,sK2,X0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).
fof(f366,plain,
( ! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| sK27(sK1,sK2,X0) = X0 )
| ~ spl29_7 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f367,plain,
( spl29_5
| spl29_7 ),
inference(avatar_split_clause,[],[f363,f365,f340]) ).
fof(f368,plain,
! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| sP0(sK2,sK1)
| ~ ordinal(sK1)
| set_difference(sK28(sK1,sK2,X0),singleton(sK1)) = X0 ),
inference(resolution,[],[f201,f103]) ).
fof(f375,plain,
! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| sP0(sK2,sK1)
| set_difference(sK28(sK1,sK2,X0),singleton(sK1)) = X0 ),
inference(forward_subsumption_resolution,[],[f368,f104]) ).
fof(f377,definition,
( spl29_8
<=> ! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| set_difference(sK28(sK1,sK2,X0),singleton(sK1)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl29_8])],[avatar_definition]) ).
fof(f378,plain,
( ! [X0] :
( ~ in(X0,sK26(sK1,sK2))
| set_difference(sK28(sK1,sK2,X0),singleton(sK1)) = X0 )
| ~ spl29_8 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f379,plain,
( spl29_5
| spl29_8 ),
inference(avatar_split_clause,[],[f375,f377,f340]) ).
fof(f384,plain,
( sK3(sK26(sK1,sK2)) = sK27(sK1,sK2,sK3(sK26(sK1,sK2)))
| in(sK3(sK26(sK1,sK2)),powerset(sK1))
| ~ spl29_7 ),
inference(resolution,[],[f366,f107]) ).
fof(f385,plain,
( sK3(sK26(sK1,sK2)) = sK27(sK1,sK2,sK3(sK26(sK1,sK2)))
| in(sK4(sK26(sK1,sK2)),sK2)
| ~ spl29_7 ),
inference(resolution,[],[f366,f106]) ).
fof(f389,definition,
( spl29_9
<=> in(sK4(sK26(sK1,sK2)),sK2) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
fof(f391,plain,
( in(sK4(sK26(sK1,sK2)),sK2)
| ~ spl29_9 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f393,definition,
( spl29_10
<=> sK3(sK26(sK1,sK2)) = sK27(sK1,sK2,sK3(sK26(sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl29_10])],[avatar_definition]) ).
fof(f395,plain,
( sK3(sK26(sK1,sK2)) = sK27(sK1,sK2,sK3(sK26(sK1,sK2)))
| ~ spl29_10 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f396,plain,
( spl29_9
| spl29_10
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f385,f365,f393,f389]) ).
fof(f398,definition,
( spl29_11
<=> in(sK3(sK26(sK1,sK2)),powerset(sK1)) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f400,plain,
( in(sK3(sK26(sK1,sK2)),powerset(sK1))
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f401,plain,
( spl29_11
| spl29_10
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f384,f365,f393,f398]) ).
fof(f403,definition,
( spl29_12
<=> sK3(sK26(sK1,sK2)) = set_difference(sK4(sK26(sK1,sK2)),singleton(sK1)) ),
introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).
fof(f404,plain,
( sK3(sK26(sK1,sK2)) != set_difference(sK4(sK26(sK1,sK2)),singleton(sK1))
| spl29_12 ),
inference(avatar_component_clause,[],[f403]) ).
fof(f405,plain,
( sK3(sK26(sK1,sK2)) = set_difference(sK4(sK26(sK1,sK2)),singleton(sK1))
| ~ spl29_12 ),
inference(avatar_component_clause,[],[f403]) ).
fof(f411,plain,
( sK3(sK26(sK1,sK2)) = set_difference(sK28(sK1,sK2,sK3(sK26(sK1,sK2))),singleton(sK1))
| sK3(sK26(sK1,sK2)) = set_difference(sK4(sK26(sK1,sK2)),singleton(sK1))
| ~ spl29_8 ),
inference(resolution,[],[f378,f105]) ).
fof(f413,plain,
( sK3(sK26(sK1,sK2)) = set_difference(sK28(sK1,sK2,sK3(sK26(sK1,sK2))),singleton(sK1))
| in(sK4(sK26(sK1,sK2)),sK2)
| ~ spl29_8 ),
inference(resolution,[],[f378,f106]) ).
fof(f417,definition,
( spl29_13
<=> sK3(sK26(sK1,sK2)) = set_difference(sK28(sK1,sK2,sK3(sK26(sK1,sK2))),singleton(sK1)) ),
introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).
fof(f419,plain,
( sK3(sK26(sK1,sK2)) = set_difference(sK28(sK1,sK2,sK3(sK26(sK1,sK2))),singleton(sK1))
| ~ spl29_13 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f420,plain,
( spl29_9
| spl29_13
| ~ spl29_8 ),
inference(avatar_split_clause,[],[f413,f377,f417,f389]) ).
fof(f422,plain,
( spl29_12
| spl29_13
| ~ spl29_8 ),
inference(avatar_split_clause,[],[f411,f377,f417,f403]) ).
fof(f428,plain,
( in(sK3(sK26(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK26(sK1,sK2)),sK26(sK1,sK2))
| sP0(sK2,sK1)
| ~ ordinal(sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ spl29_10 ),
inference(superposition,[],[f204,f395]) ).
fof(f429,plain,
( in(sK3(sK26(sK1,sK2)),powerset(sK1))
| sP0(sK2,sK1)
| ~ ordinal(sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ spl29_10 ),
inference(forward_subsumption_resolution,[],[f428,f107]) ).
fof(f430,plain,
( ! [X0] :
( sK3(X0) != sK3(sK26(sK1,sK2))
| ~ in(sK4(sK26(sK1,sK2)),sK2)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK3(X0),X0) )
| ~ spl29_12 ),
inference(superposition,[],[f108,f405]) ).
fof(f431,plain,
( ! [X0] :
( in(sK3(sK26(sK1,sK2)),sK26(sK1,X0))
| ~ in(sK3(sK26(sK1,sK2)),powerset(sK1))
| ~ in(sK4(sK26(sK1,sK2)),X0)
| sP0(X0,sK1)
| ~ ordinal(sK1)
| ~ element(X0,powerset(powerset(succ(sK1)))) )
| ~ spl29_12 ),
inference(superposition,[],[f207,f405]) ).
fof(f456,plain,
( ! [X0] :
( in(sK3(sK26(sK1,sK2)),sK26(sK1,X0))
| ~ in(sK4(sK26(sK1,sK2)),X0)
| sP0(X0,sK1)
| ~ ordinal(sK1)
| ~ element(X0,powerset(powerset(succ(sK1)))) )
| ~ spl29_11
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f431,f400]) ).
fof(f457,plain,
( ! [X0] :
( sK3(X0) != sK3(sK26(sK1,sK2))
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK3(X0),X0) )
| ~ spl29_9
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f430,f391]) ).
fof(f458,plain,
( ! [X0] :
( in(sK3(sK26(sK1,sK2)),sK26(sK1,X0))
| ~ in(sK4(sK26(sK1,sK2)),X0)
| sP0(X0,sK1)
| ~ element(X0,powerset(powerset(succ(sK1)))) )
| ~ spl29_11
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f456,f104]) ).
fof(f459,plain,
( ~ in(sK3(sK26(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK26(sK1,sK2)),sK26(sK1,sK2))
| ~ spl29_9
| ~ spl29_12 ),
inference(equality_resolution,[],[f457]) ).
fof(f460,plain,
( ~ in(sK3(sK26(sK1,sK2)),sK26(sK1,sK2))
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f459,f400]) ).
fof(f465,plain,
( ~ in(sK4(sK26(sK1,sK2)),sK2)
| sP0(sK2,sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12 ),
inference(resolution,[],[f458,f460]) ).
fof(f470,plain,
( sP0(sK2,sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f465,f391]) ).
fof(f472,plain,
( ~ element(sK2,powerset(powerset(succ(sK1))))
| spl29_5
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f470,f341]) ).
fof(f474,plain,
( $false
| spl29_5
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f472,f103]) ).
fof(f475,plain,
( spl29_5
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12 ),
inference(avatar_contradiction_clause,[],[f474]) ).
fof(f477,plain,
( in(sK3(sK26(sK1,sK2)),powerset(sK1))
| ~ ordinal(sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| spl29_5
| ~ spl29_10 ),
inference(forward_subsumption_resolution,[],[f429,f341]) ).
fof(f480,definition,
( spl29_19
<=> in(sK3(sK26(sK1,sK2)),sK26(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl29_19])],[avatar_definition]) ).
fof(f482,plain,
( ~ in(sK3(sK26(sK1,sK2)),sK26(sK1,sK2))
| spl29_19 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f484,plain,
( in(sK3(sK26(sK1,sK2)),powerset(sK1))
| ~ element(sK2,powerset(powerset(succ(sK1))))
| spl29_5
| ~ spl29_10 ),
inference(forward_subsumption_resolution,[],[f477,f104]) ).
fof(f489,plain,
( in(sK3(sK26(sK1,sK2)),powerset(sK1))
| spl29_5
| ~ spl29_10 ),
inference(forward_subsumption_resolution,[],[f484,f103]) ).
fof(f490,plain,
( spl29_11
| spl29_5
| ~ spl29_10 ),
inference(avatar_split_clause,[],[f489,f393,f340,f398]) ).
fof(f528,plain,
( ! [X0] :
( sK3(X0) != sK3(sK26(sK1,sK2))
| ~ in(sK28(sK1,sK2,sK3(sK26(sK1,sK2))),sK2)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK3(X0),X0) )
| ~ spl29_13 ),
inference(superposition,[],[f108,f419]) ).
fof(f544,definition,
( spl29_23
<=> in(sK28(sK1,sK2,sK3(sK26(sK1,sK2))),sK2) ),
introduced(definition,[new_symbols(definition,[spl29_23])],[avatar_definition]) ).
fof(f546,plain,
( ~ in(sK28(sK1,sK2,sK3(sK26(sK1,sK2))),sK2)
| spl29_23 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f548,definition,
( spl29_24
<=> ! [X0] :
( sK3(X0) != sK3(sK26(sK1,sK2))
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1)) ) ),
introduced(definition,[new_symbols(definition,[spl29_24])],[avatar_definition]) ).
fof(f549,plain,
( ! [X0] :
( sK3(X0) != sK3(sK26(sK1,sK2))
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1)) )
| ~ spl29_24 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f550,plain,
( ~ spl29_23
| spl29_24
| ~ spl29_13 ),
inference(avatar_split_clause,[],[f528,f417,f548,f544]) ).
fof(f555,plain,
( ~ in(sK3(sK26(sK1,sK2)),sK26(sK1,sK2))
| ~ spl29_6
| spl29_23 ),
inference(resolution,[],[f546,f345]) ).
fof(f556,plain,
( ~ spl29_19
| ~ spl29_6
| spl29_23 ),
inference(avatar_split_clause,[],[f555,f544,f344,f480]) ).
fof(f558,plain,
( sK3(sK26(sK1,sK2)) = set_difference(sK4(sK26(sK1,sK2)),singleton(sK1))
| spl29_19 ),
inference(resolution,[],[f482,f105]) ).
fof(f560,plain,
( in(sK4(sK26(sK1,sK2)),sK2)
| spl29_19 ),
inference(resolution,[],[f482,f106]) ).
fof(f561,plain,
( $false
| spl29_12
| spl29_19 ),
inference(forward_subsumption_resolution,[],[f558,f404]) ).
fof(f562,plain,
( spl29_12
| spl29_19 ),
inference(avatar_contradiction_clause,[],[f561]) ).
fof(f600,plain,
( ~ in(sK3(sK26(sK1,sK2)),sK26(sK1,sK2))
| ~ in(sK3(sK26(sK1,sK2)),powerset(sK1))
| ~ spl29_24 ),
inference(equality_resolution,[],[f549]) ).
fof(f604,plain,
( spl29_9
| spl29_19 ),
inference(avatar_split_clause,[],[f560,f480,f389]) ).
fof(f605,plain,
( ~ in(sK3(sK26(sK1,sK2)),sK26(sK1,sK2))
| ~ spl29_11
| ~ spl29_24 ),
inference(forward_subsumption_resolution,[],[f600,f400]) ).
fof(f606,plain,
( ~ spl29_19
| ~ spl29_11
| ~ spl29_24 ),
inference(avatar_split_clause,[],[f605,f548,f398,f480]) ).
cnf(s3,plain,
( spl29_5
| spl29_6 ),
inference(sat_conversion,[],[f346]) ).
cnf(s4,plain,
~ spl29_5,
inference(sat_conversion,[],[f362]) ).
cnf(s5,plain,
( spl29_5
| spl29_7 ),
inference(sat_conversion,[],[f367]) ).
cnf(s6,plain,
( spl29_5
| spl29_8 ),
inference(sat_conversion,[],[f379]) ).
cnf(s7,plain,
( ~ spl29_7
| spl29_9
| spl29_10 ),
inference(sat_conversion,[],[f396]) ).
cnf(s8,plain,
( ~ spl29_7
| spl29_10
| spl29_11 ),
inference(sat_conversion,[],[f401]) ).
cnf(s10,plain,
( ~ spl29_8
| spl29_9
| spl29_13 ),
inference(sat_conversion,[],[f420]) ).
cnf(s12,plain,
( ~ spl29_8
| spl29_12
| spl29_13 ),
inference(sat_conversion,[],[f422]) ).
cnf(s15,plain,
( spl29_5
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12 ),
inference(sat_conversion,[],[f475]) ).
cnf(s19,plain,
( spl29_5
| ~ spl29_10
| spl29_11 ),
inference(sat_conversion,[],[f490]) ).
cnf(s22,plain,
( ~ spl29_13
| ~ spl29_23
| spl29_24 ),
inference(sat_conversion,[],[f550]) ).
cnf(s23,plain,
( ~ spl29_6
| ~ spl29_19
| spl29_23 ),
inference(sat_conversion,[],[f556]) ).
cnf(s24,plain,
( spl29_12
| spl29_19 ),
inference(sat_conversion,[],[f562]) ).
cnf(s26,plain,
( spl29_9
| spl29_19 ),
inference(sat_conversion,[],[f604]) ).
cnf(s27,plain,
( ~ spl29_11
| ~ spl29_19
| ~ spl29_24 ),
inference(sat_conversion,[],[f606]) ).
cnf(s28,plain,
spl29_8,
inference(rat,[],[s6,s4]) ).
cnf(s29,plain,
spl29_7,
inference(rat,[],[s5,s4]) ).
cnf(s30,plain,
spl29_6,
inference(rat,[],[s3,s4]) ).
cnf(s31,plain,
spl29_9,
inference(rat,[],[s27,s22,s19,s23,s7,s10,s26,s4,s30,s29,s28]) ).
cnf(s32,plain,
~ spl29_11,
inference(rat,[],[s22,s27,s23,s12,s24,s15,s30,s28,s4,s31]) ).
cnf(s34,plain,
~ spl29_10,
inference(rat,[],[s19,s4,s32]) ).
cnf(s35,plain,
$false,
inference(rat,[],[s8,s29,s32,s34]) ).
fof(f607,plain,
$false,
inference(avatar_sat_refutation,[],[s35]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU298+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n002.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 04:36:52 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.50 % (4148420)Will run a generic schedule for satisfiability detection.
% 0.18/0.50 % (4148430)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1241423418:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.50 % (4148426)% WARNING: option uhcvi not known.
% 0.18/0.50 % (4148425)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3036797311_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.50 % (4148426)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3479875968:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.50 % (4148429)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=493304516:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.50 % (4148427)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3712125435:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.50 % (4148428)dis+10_1_sil=32000:sp=arity:random_seed=4204658946:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.50 % (4148431)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3697290560:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.50 % TRYING [1]
% 0.18/0.50 % TRYING [2]
% 0.18/0.50 % TRYING [3]
% 0.18/0.50 % (4148428) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4148420-4148428"...
% 0.18/0.50 % (4148428)...printing done.
% 0.18/0.50 % (4148428)Refutation found. Thanks to Tanya!
% 0.18/0.50 % SZS status Theorem for theBenchmark
% 0.18/0.50 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.50 % (4148428)------------------------------
% 0.18/0.50 % (4148428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.50 % (4148428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.50 % (4148428)CaDiCaL version: 2.1.3
% 0.18/0.50 % (4148428)Termination reason: Refutation
% 0.18/0.50 % (4148428)Time elapsed: 0.017 s
% 0.18/0.50 % (4148428)Peak memory usage: 13 MB
% 0.18/0.50 % (4148428)Instructions burned: 24 (million)
% 0.18/0.50 % (4148420)Success in time 0.058 s
% 0.18/0.50 % Vampire exiting
%------------------------------------------------------------------------------