%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU297+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:13 PM UTC 2026
% Result : Theorem 5.44s 1.75s
% Output : Refutation 6.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 11
% Syntax : Number of formulae : 106 ( 14 unt; 9 def)
% Number of atoms : 417 ( 53 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 495 ( 184 ~; 204 |; 82 &)
% ( 15 <=>; 8 =>; 0 <=; 2 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 9 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-3 aty)
% Number of variables : 175 ( 0 sgn 128 !; 47 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f232,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(powerset(X0)))
& relation(X2)
& function(X2) )
=> ( ! [X3,X4,X5] :
( ( X3 = X4
& in(relation_image(X2,X4),X1)
& X3 = X5
& in(relation_image(X2,X5),X1) )
=> X4 = X5 )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ? [X5] :
( in(X5,powerset(relation_dom(X2)))
& X5 = X4
& in(relation_image(X2,X4),X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e6_27__finset_1__1) ).
fof(f238,conjecture,
! [X0,X1,X2] :
( ( element(X1,powerset(powerset(X0)))
& relation(X2)
& function(X2) )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ( in(X4,powerset(relation_dom(X2)))
& in(relation_image(X2,X4),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e6_27__finset_1) ).
fof(f239,negated_conjecture,
~ ! [X0,X1,X2] :
( ( element(X1,powerset(powerset(X0)))
& relation(X2)
& function(X2) )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ( in(X4,powerset(relation_dom(X2)))
& in(relation_image(X2,X4),X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f238]) ).
fof(f424,plain,
! [X0,X1,X2] :
( ( element(X1,powerset(powerset(X0)))
& relation(X2)
& function(X2) )
=> ( ! [X3,X4,X5] :
( ( X3 = X4
& in(relation_image(X2,X4),X1)
& X3 = X5
& in(relation_image(X2,X5),X1) )
=> X4 = X5 )
=> ? [X6] :
! [X7] :
( in(X7,X6)
<=> ? [X8] :
( in(X8,powerset(relation_dom(X2)))
& X7 = X8
& in(relation_image(X2,X7),X1) ) ) ) ),
inference(rectify,[],[f232]) ).
fof(f620,plain,
! [X0,X1,X2] :
( ? [X6] :
! [X7] :
( in(X7,X6)
<=> ? [X8] :
( in(X8,powerset(relation_dom(X2)))
& X7 = X8
& in(relation_image(X2,X7),X1) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& in(relation_image(X2,X4),X1)
& X3 = X5
& in(relation_image(X2,X5),X1) )
| ~ element(X1,powerset(powerset(X0)))
| ~ relation(X2)
| ~ function(X2) ),
inference(ennf_transformation,[],[f424]) ).
fof(f621,plain,
! [X0,X1,X2] :
( ? [X6] :
! [X7] :
( in(X7,X6)
<=> ? [X8] :
( in(X8,powerset(relation_dom(X2)))
& X7 = X8
& in(relation_image(X2,X7),X1) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& in(relation_image(X2,X4),X1)
& X3 = X5
& in(relation_image(X2,X5),X1) )
| ~ element(X1,powerset(powerset(X0)))
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f620]) ).
fof(f628,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,powerset(relation_dom(X2)))
& in(relation_image(X2,X4),X1) ) )
& element(X1,powerset(powerset(X0)))
& relation(X2)
& function(X2) ),
inference(ennf_transformation,[],[f239]) ).
fof(f629,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,powerset(relation_dom(X2)))
& in(relation_image(X2,X4),X1) ) )
& element(X1,powerset(powerset(X0)))
& relation(X2)
& function(X2) ),
inference(flattening,[],[f628]) ).
fof(f850,definition,
! [X1,X2] :
( ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& in(relation_image(X2,X4),X1)
& X3 = X5
& in(relation_image(X2,X5),X1) )
| ~ sP8(X1,X2) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f851,plain,
! [X0,X1,X2] :
( ? [X6] :
! [X7] :
( in(X7,X6)
<=> ? [X8] :
( in(X8,powerset(relation_dom(X2)))
& X7 = X8
& in(relation_image(X2,X7),X1) ) )
| sP8(X1,X2)
| ~ element(X1,powerset(powerset(X0)))
| ~ relation(X2)
| ~ function(X2) ),
inference(definition_folding,[],[f621,f850]) ).
fof(f1126,plain,
! [X1,X2] :
( ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& in(relation_image(X2,X4),X1)
& X3 = X5
& in(relation_image(X2,X5),X1) )
| ~ sP8(X1,X2) ),
inference(nnf_transformation,[],[f850]) ).
fof(f1127,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& in(relation_image(X1,X3),X0)
& X2 = X4
& in(relation_image(X1,X4),X0) )
| ~ sP8(X0,X1) ),
inference(rectify,[],[f1126]) ).
fof(f1128,plain,
! [X0,X1] :
( ( sK208(X0,X1) != sK209(X0,X1)
& sK207(X0,X1) = sK208(X0,X1)
& in(relation_image(X1,sK208(X0,X1)),X0)
& sK207(X0,X1) = sK209(X0,X1)
& in(relation_image(X1,sK209(X0,X1)),X0) )
| ~ sP8(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK207,sK208,sK209]),skolemize(X2,sK207(X0,X1)),skolemize(X3,sK208(X0,X1)),skolemize(X4,sK209(X0,X1))],[f1127]) ).
fof(f1129,plain,
! [X0,X1,X2] :
( ? [X6] :
! [X7] :
( ( in(X7,X6)
| ! [X8] :
( ~ in(X8,powerset(relation_dom(X2)))
| X7 != X8
| ~ in(relation_image(X2,X7),X1) ) )
& ( ? [X8] :
( in(X8,powerset(relation_dom(X2)))
& X7 = X8
& in(relation_image(X2,X7),X1) )
| ~ in(X7,X6) ) )
| sP8(X1,X2)
| ~ element(X1,powerset(powerset(X0)))
| ~ relation(X2)
| ~ function(X2) ),
inference(nnf_transformation,[],[f851]) ).
fof(f1130,plain,
! [X0,X1,X2] :
( ? [X3] :
! [X4] :
( ( in(X4,X3)
| ! [X5] :
( ~ in(X5,powerset(relation_dom(X2)))
| X4 != X5
| ~ in(relation_image(X2,X4),X1) ) )
& ( ? [X6] :
( in(X6,powerset(relation_dom(X2)))
& X4 = X6
& in(relation_image(X2,X4),X1) )
| ~ in(X4,X3) ) )
| sP8(X1,X2)
| ~ element(X1,powerset(powerset(X0)))
| ~ relation(X2)
| ~ function(X2) ),
inference(rectify,[],[f1129]) ).
fof(f1131,plain,
! [X0,X1,X2] :
( ! [X4] :
( ( in(X4,sK210(X1,X2))
| ! [X5] :
( ~ in(X5,powerset(relation_dom(X2)))
| X4 != X5
| ~ in(relation_image(X2,X4),X1) ) )
& ( ( in(sK211(X1,X2,X4),powerset(relation_dom(X2)))
& sK211(X1,X2,X4) = X4
& in(relation_image(X2,X4),X1) )
| ~ in(X4,sK210(X1,X2)) ) )
| sP8(X1,X2)
| ~ element(X1,powerset(powerset(X0)))
| ~ relation(X2)
| ~ function(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK210,sK211]),skolemize(X3,sK210(X1,X2)),skolemize(X6,sK211(X1,X2,X4))],[f1130]) ).
fof(f1153,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( ( ~ in(X4,powerset(relation_dom(X2)))
| ~ in(relation_image(X2,X4),X1)
| ~ in(X4,X3) )
& ( ( in(X4,powerset(relation_dom(X2)))
& in(relation_image(X2,X4),X1) )
| in(X4,X3) ) )
& element(X1,powerset(powerset(X0)))
& relation(X2)
& function(X2) ),
inference(nnf_transformation,[],[f629]) ).
fof(f1154,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( ( ~ in(X4,powerset(relation_dom(X2)))
| ~ in(relation_image(X2,X4),X1)
| ~ in(X4,X3) )
& ( ( in(X4,powerset(relation_dom(X2)))
& in(relation_image(X2,X4),X1) )
| in(X4,X3) ) )
& element(X1,powerset(powerset(X0)))
& relation(X2)
& function(X2) ),
inference(flattening,[],[f1153]) ).
fof(f1155,plain,
( ! [X3] :
( ( ~ in(sK235(X3),powerset(relation_dom(sK234)))
| ~ in(relation_image(sK234,sK235(X3)),sK233)
| ~ in(sK235(X3),X3) )
& ( ( in(sK235(X3),powerset(relation_dom(sK234)))
& in(relation_image(sK234,sK235(X3)),sK233) )
| in(sK235(X3),X3) ) )
& element(sK233,powerset(powerset(sK232)))
& relation(sK234)
& function(sK234) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK232,sK233,sK234,sK235]),skolemize(X0,sK232),skolemize(X1,sK233),skolemize(X2,sK234),skolemize(X4,sK235(X3))],[f1154]) ).
fof(f1905,plain,
! [X0,X1] :
( ~ sP8(X0,X1)
| sK207(X0,X1) = sK209(X0,X1) ),
inference(cnf_transformation,[],[f1128]) ).
fof(f1907,plain,
! [X0,X1] :
( ~ sP8(X0,X1)
| sK207(X0,X1) = sK208(X0,X1) ),
inference(cnf_transformation,[],[f1128]) ).
fof(f1908,plain,
! [X0,X1] :
( sK208(X0,X1) != sK209(X0,X1)
| ~ sP8(X0,X1) ),
inference(cnf_transformation,[],[f1128]) ).
fof(f1909,plain,
! [X2,X0,X1,X4] :
( ~ relation(X2)
| ~ in(X4,sK210(X1,X2))
| sP8(X1,X2)
| ~ element(X1,powerset(powerset(X0)))
| in(relation_image(X2,X4),X1)
| ~ function(X2) ),
inference(cnf_transformation,[],[f1131]) ).
fof(f1910,plain,
! [X2,X0,X1,X4] :
( ~ relation(X2)
| ~ in(X4,sK210(X1,X2))
| sP8(X1,X2)
| ~ element(X1,powerset(powerset(X0)))
| sK211(X1,X2,X4) = X4
| ~ function(X2) ),
inference(cnf_transformation,[],[f1131]) ).
fof(f1911,plain,
! [X2,X0,X1,X4] :
( ~ relation(X2)
| ~ in(X4,sK210(X1,X2))
| sP8(X1,X2)
| ~ element(X1,powerset(powerset(X0)))
| in(sK211(X1,X2,X4),powerset(relation_dom(X2)))
| ~ function(X2) ),
inference(cnf_transformation,[],[f1131]) ).
fof(f1912,plain,
! [X2,X0,X1,X4,X5] :
( in(X4,sK210(X1,X2))
| ~ in(X5,powerset(relation_dom(X2)))
| X4 != X5
| ~ in(relation_image(X2,X4),X1)
| sP8(X1,X2)
| ~ element(X1,powerset(powerset(X0)))
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f1131]) ).
fof(f1948,plain,
function(sK234),
inference(cnf_transformation,[],[f1155]) ).
fof(f1949,plain,
relation(sK234),
inference(cnf_transformation,[],[f1155]) ).
fof(f1950,plain,
element(sK233,powerset(powerset(sK232))),
inference(cnf_transformation,[],[f1155]) ).
fof(f1951,plain,
! [X3] :
( in(relation_image(sK234,sK235(X3)),sK233)
| in(sK235(X3),X3) ),
inference(cnf_transformation,[],[f1155]) ).
fof(f1952,plain,
! [X3] :
( in(sK235(X3),powerset(relation_dom(sK234)))
| in(sK235(X3),X3) ),
inference(cnf_transformation,[],[f1155]) ).
fof(f1953,plain,
! [X3] :
( ~ in(sK235(X3),powerset(relation_dom(sK234)))
| ~ in(relation_image(sK234,sK235(X3)),sK233)
| ~ in(sK235(X3),X3) ),
inference(cnf_transformation,[],[f1155]) ).
fof(f2686,plain,
! [X2,X0,X1,X5] :
( ~ relation(X2)
| ~ in(X5,powerset(relation_dom(X2)))
| ~ in(relation_image(X2,X5),X1)
| sP8(X1,X2)
| ~ element(X1,powerset(powerset(X0)))
| in(X5,sK210(X1,X2))
| ~ function(X2) ),
inference(equality_resolution,[],[f1912]) ).
fof(f2842,plain,
! [X2,X0,X1] :
( ~ in(X0,sK210(X1,sK234))
| sP8(X1,sK234)
| ~ element(X1,powerset(powerset(X2)))
| in(relation_image(sK234,X0),X1)
| ~ function(sK234) ),
inference(resolution,[],[f1909,f1949]) ).
fof(f2843,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(powerset(X2)))
| sP8(X1,sK234)
| ~ in(X0,sK210(X1,sK234))
| in(relation_image(sK234,X0),X1) ),
inference(forward_subsumption_resolution,[],[f2842,f1948]) ).
fof(f2844,plain,
! [X0] :
( sP8(sK233,sK234)
| ~ in(X0,sK210(sK233,sK234))
| in(relation_image(sK234,X0),sK233) ),
inference(resolution,[],[f2843,f1950]) ).
fof(f2846,definition,
( spl279_13
<=> ! [X0] :
( ~ in(X0,sK210(sK233,sK234))
| in(relation_image(sK234,X0),sK233) ) ),
introduced(definition,[new_symbols(definition,[spl279_13])],[avatar_definition]) ).
fof(f2847,plain,
( ! [X0] :
( in(relation_image(sK234,X0),sK233)
| ~ in(X0,sK210(sK233,sK234)) )
| ~ spl279_13 ),
inference(avatar_component_clause,[],[f2846]) ).
fof(f2849,definition,
( spl279_14
<=> sP8(sK233,sK234) ),
introduced(definition,[new_symbols(definition,[spl279_14])],[avatar_definition]) ).
fof(f2850,plain,
( sP8(sK233,sK234)
| ~ spl279_14 ),
inference(avatar_component_clause,[],[f2849]) ).
fof(f2851,plain,
( spl279_13
| spl279_14 ),
inference(avatar_split_clause,[],[f2844,f2849,f2846]) ).
fof(f2860,plain,
! [X2,X0,X1] :
( ~ in(X0,powerset(relation_dom(sK234)))
| ~ in(relation_image(sK234,X0),X1)
| sP8(X1,sK234)
| ~ element(X1,powerset(powerset(X2)))
| in(X0,sK210(X1,sK234))
| ~ function(sK234) ),
inference(resolution,[],[f2686,f1949]) ).
fof(f2861,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(powerset(X2)))
| ~ in(relation_image(sK234,X0),X1)
| sP8(X1,sK234)
| ~ in(X0,powerset(relation_dom(sK234)))
| in(X0,sK210(X1,sK234)) ),
inference(forward_subsumption_resolution,[],[f2860,f1948]) ).
fof(f2862,plain,
! [X0] :
( ~ in(relation_image(sK234,X0),sK233)
| sP8(sK233,sK234)
| ~ in(X0,powerset(relation_dom(sK234)))
| in(X0,sK210(sK233,sK234)) ),
inference(resolution,[],[f2861,f1950]) ).
fof(f2864,definition,
( spl279_17
<=> ! [X0] :
( ~ in(relation_image(sK234,X0),sK233)
| in(X0,sK210(sK233,sK234))
| ~ in(X0,powerset(relation_dom(sK234))) ) ),
introduced(definition,[new_symbols(definition,[spl279_17])],[avatar_definition]) ).
fof(f2865,plain,
( ! [X0] :
( ~ in(relation_image(sK234,X0),sK233)
| in(X0,sK210(sK233,sK234))
| ~ in(X0,powerset(relation_dom(sK234))) )
| ~ spl279_17 ),
inference(avatar_component_clause,[],[f2864]) ).
fof(f2866,plain,
( spl279_14
| spl279_17 ),
inference(avatar_split_clause,[],[f2862,f2864,f2849]) ).
fof(f2869,plain,
! [X2,X0,X1] :
( ~ in(X0,sK210(X1,sK234))
| sP8(X1,sK234)
| ~ element(X1,powerset(powerset(X2)))
| in(sK211(X1,sK234,X0),powerset(relation_dom(sK234)))
| ~ function(sK234) ),
inference(resolution,[],[f1911,f1949]) ).
fof(f2870,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(powerset(X2)))
| sP8(X1,sK234)
| ~ in(X0,sK210(X1,sK234))
| in(sK211(X1,sK234,X0),powerset(relation_dom(sK234))) ),
inference(forward_subsumption_resolution,[],[f2869,f1948]) ).
fof(f2871,plain,
! [X0] :
( sP8(sK233,sK234)
| ~ in(X0,sK210(sK233,sK234))
| in(sK211(sK233,sK234,X0),powerset(relation_dom(sK234))) ),
inference(resolution,[],[f2870,f1950]) ).
fof(f2874,plain,
! [X2,X0,X1] :
( ~ in(X0,sK210(X1,sK234))
| sP8(X1,sK234)
| ~ element(X1,powerset(powerset(X2)))
| sK211(X1,sK234,X0) = X0
| ~ function(sK234) ),
inference(resolution,[],[f1910,f1949]) ).
fof(f2875,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(powerset(X2)))
| sP8(X1,sK234)
| ~ in(X0,sK210(X1,sK234))
| sK211(X1,sK234,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f2874,f1948]) ).
fof(f2876,plain,
! [X0] :
( sP8(sK233,sK234)
| ~ in(X0,sK210(sK233,sK234))
| sK211(sK233,sK234,X0) = X0 ),
inference(resolution,[],[f2875,f1950]) ).
fof(f3455,plain,
( sK207(sK233,sK234) = sK208(sK233,sK234)
| ~ spl279_14 ),
inference(resolution,[],[f1907,f2850]) ).
fof(f3490,plain,
( sK207(sK233,sK234) = sK209(sK233,sK234)
| ~ spl279_14 ),
inference(resolution,[],[f1905,f2850]) ).
fof(f3493,plain,
( sK208(sK233,sK234) = sK209(sK233,sK234)
| ~ spl279_14 ),
inference(forward_demodulation,[],[f3490,f3455]) ).
fof(f3496,plain,
( sK208(sK233,sK234) != sK208(sK233,sK234)
| ~ sP8(sK233,sK234)
| ~ spl279_14 ),
inference(superposition,[],[f1908,f3493]) ).
fof(f3497,plain,
( ~ sP8(sK233,sK234)
| ~ spl279_14 ),
inference(trivial_inequality_removal,[],[f3496]) ).
fof(f3499,plain,
( $false
| ~ spl279_14 ),
inference(forward_subsumption_resolution,[],[f3497,f2850]) ).
fof(f3500,plain,
~ spl279_14,
inference(avatar_contradiction_clause,[],[f3499]) ).
fof(f3502,definition,
( spl279_70
<=> ! [X0] :
( ~ in(X0,sK210(sK233,sK234))
| in(sK211(sK233,sK234,X0),powerset(relation_dom(sK234))) ) ),
introduced(definition,[new_symbols(definition,[spl279_70])],[avatar_definition]) ).
fof(f3503,plain,
( ! [X0] :
( in(sK211(sK233,sK234,X0),powerset(relation_dom(sK234)))
| ~ in(X0,sK210(sK233,sK234)) )
| ~ spl279_70 ),
inference(avatar_component_clause,[],[f3502]) ).
fof(f3504,plain,
( spl279_70
| spl279_14 ),
inference(avatar_split_clause,[],[f2871,f2849,f3502]) ).
fof(f3506,definition,
( spl279_71
<=> ! [X0] :
( ~ in(X0,sK210(sK233,sK234))
| sK211(sK233,sK234,X0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl279_71])],[avatar_definition]) ).
fof(f3507,plain,
( ! [X0] :
( ~ in(X0,sK210(sK233,sK234))
| sK211(sK233,sK234,X0) = X0 )
| ~ spl279_71 ),
inference(avatar_component_clause,[],[f3506]) ).
fof(f3508,plain,
( spl279_71
| spl279_14 ),
inference(avatar_split_clause,[],[f2876,f2849,f3506]) ).
fof(f3511,plain,
( sK235(sK210(sK233,sK234)) = sK211(sK233,sK234,sK235(sK210(sK233,sK234)))
| in(sK235(sK210(sK233,sK234)),powerset(relation_dom(sK234)))
| ~ spl279_71 ),
inference(resolution,[],[f3507,f1952]) ).
fof(f3512,plain,
( sK235(sK210(sK233,sK234)) = sK211(sK233,sK234,sK235(sK210(sK233,sK234)))
| in(relation_image(sK234,sK235(sK210(sK233,sK234))),sK233)
| ~ spl279_71 ),
inference(resolution,[],[f3507,f1951]) ).
fof(f3515,definition,
( spl279_72
<=> in(relation_image(sK234,sK235(sK210(sK233,sK234))),sK233) ),
introduced(definition,[new_symbols(definition,[spl279_72])],[avatar_definition]) ).
fof(f3516,plain,
( in(relation_image(sK234,sK235(sK210(sK233,sK234))),sK233)
| ~ spl279_72 ),
inference(avatar_component_clause,[],[f3515]) ).
fof(f3518,definition,
( spl279_73
<=> sK235(sK210(sK233,sK234)) = sK211(sK233,sK234,sK235(sK210(sK233,sK234))) ),
introduced(definition,[new_symbols(definition,[spl279_73])],[avatar_definition]) ).
fof(f3519,plain,
( sK235(sK210(sK233,sK234)) = sK211(sK233,sK234,sK235(sK210(sK233,sK234)))
| ~ spl279_73 ),
inference(avatar_component_clause,[],[f3518]) ).
fof(f3520,plain,
( spl279_72
| spl279_73
| ~ spl279_71 ),
inference(avatar_split_clause,[],[f3512,f3506,f3518,f3515]) ).
fof(f3522,definition,
( spl279_74
<=> in(sK235(sK210(sK233,sK234)),powerset(relation_dom(sK234))) ),
introduced(definition,[new_symbols(definition,[spl279_74])],[avatar_definition]) ).
fof(f3523,plain,
( in(sK235(sK210(sK233,sK234)),powerset(relation_dom(sK234)))
| ~ spl279_74 ),
inference(avatar_component_clause,[],[f3522]) ).
fof(f3524,plain,
( spl279_74
| spl279_73
| ~ spl279_71 ),
inference(avatar_split_clause,[],[f3511,f3506,f3518,f3522]) ).
fof(f3548,plain,
( in(sK235(sK210(sK233,sK234)),powerset(relation_dom(sK234)))
| ~ in(sK235(sK210(sK233,sK234)),sK210(sK233,sK234))
| ~ spl279_70
| ~ spl279_73 ),
inference(superposition,[],[f3503,f3519]) ).
fof(f3549,plain,
( in(sK235(sK210(sK233,sK234)),powerset(relation_dom(sK234)))
| ~ spl279_70
| ~ spl279_73 ),
inference(forward_subsumption_resolution,[],[f3548,f1952]) ).
fof(f3550,plain,
( spl279_74
| ~ spl279_70
| ~ spl279_73 ),
inference(avatar_split_clause,[],[f3549,f3518,f3502,f3522]) ).
fof(f3551,plain,
( ~ in(relation_image(sK234,sK235(sK210(sK233,sK234))),sK233)
| ~ in(sK235(sK210(sK233,sK234)),sK210(sK233,sK234))
| ~ spl279_74 ),
inference(resolution,[],[f3523,f1953]) ).
fof(f3553,plain,
( ~ in(sK235(sK210(sK233,sK234)),sK210(sK233,sK234))
| ~ spl279_13
| ~ spl279_74 ),
inference(forward_subsumption_resolution,[],[f3551,f2847]) ).
fof(f3555,plain,
( in(relation_image(sK234,sK235(sK210(sK233,sK234))),sK233)
| ~ spl279_13
| ~ spl279_74 ),
inference(resolution,[],[f3553,f1951]) ).
fof(f3556,plain,
( spl279_72
| ~ spl279_13
| ~ spl279_74 ),
inference(avatar_split_clause,[],[f3555,f3522,f2846,f3515]) ).
fof(f3558,plain,
( in(sK235(sK210(sK233,sK234)),sK210(sK233,sK234))
| ~ in(sK235(sK210(sK233,sK234)),powerset(relation_dom(sK234)))
| ~ spl279_17
| ~ spl279_72 ),
inference(resolution,[],[f3516,f2865]) ).
fof(f3563,plain,
( ~ in(sK235(sK210(sK233,sK234)),powerset(relation_dom(sK234)))
| ~ spl279_13
| ~ spl279_17
| ~ spl279_72
| ~ spl279_74 ),
inference(forward_subsumption_resolution,[],[f3558,f3553]) ).
fof(f3564,plain,
( $false
| ~ spl279_13
| ~ spl279_17
| ~ spl279_72
| ~ spl279_74 ),
inference(forward_subsumption_resolution,[],[f3563,f3523]) ).
fof(f3565,plain,
( ~ spl279_13
| ~ spl279_17
| ~ spl279_72
| ~ spl279_74 ),
inference(avatar_contradiction_clause,[],[f3564]) ).
cnf(s11,plain,
( spl279_13
| spl279_14 ),
inference(sat_conversion,[],[f2851]) ).
cnf(s13,plain,
( spl279_14
| spl279_17 ),
inference(sat_conversion,[],[f2866]) ).
cnf(s47,plain,
~ spl279_14,
inference(sat_conversion,[],[f3500]) ).
cnf(s48,plain,
( spl279_14
| spl279_70 ),
inference(sat_conversion,[],[f3504]) ).
cnf(s49,plain,
( spl279_14
| spl279_71 ),
inference(sat_conversion,[],[f3508]) ).
cnf(s50,plain,
( ~ spl279_71
| spl279_72
| spl279_73 ),
inference(sat_conversion,[],[f3520]) ).
cnf(s51,plain,
( ~ spl279_71
| spl279_73
| spl279_74 ),
inference(sat_conversion,[],[f3524]) ).
cnf(s53,plain,
( ~ spl279_70
| ~ spl279_73
| spl279_74 ),
inference(sat_conversion,[],[f3550]) ).
cnf(s54,plain,
( ~ spl279_13
| spl279_72
| ~ spl279_74 ),
inference(sat_conversion,[],[f3556]) ).
cnf(s56,plain,
( ~ spl279_13
| ~ spl279_17
| ~ spl279_72
| ~ spl279_74 ),
inference(sat_conversion,[],[f3565]) ).
cnf(s57,plain,
spl279_71,
inference(rat,[],[s49,s47]) ).
cnf(s58,plain,
spl279_70,
inference(rat,[],[s48,s47]) ).
cnf(s60,plain,
spl279_17,
inference(rat,[],[s13,s47]) ).
cnf(s61,plain,
spl279_13,
inference(rat,[],[s11,s47]) ).
cnf(s62,plain,
spl279_72,
inference(rat,[],[s53,s50,s54,s58,s57,s61]) ).
cnf(s63,plain,
~ spl279_74,
inference(rat,[],[s56,s61,s60,s62]) ).
cnf(s64,plain,
spl279_73,
inference(rat,[],[s51,s57,s63]) ).
cnf(s65,plain,
$false,
inference(rat,[],[s53,s58,s63,s64]) ).
fof(f3566,plain,
$false,
inference(avatar_sat_refutation,[],[s65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU297+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n013.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 04:33:51 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.44/1.75 % (802942)Detected formulas, will run a generic FOF schedule.
% 5.44/1.75 % (802948)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1599510036:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.44/1.75 % (802951)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1233088231:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.44/1.75 % (802953)dis-21_1_sil=8000:lcm=predicate:random_seed=739003612:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.44/1.75 % (802949)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=554146458:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.44/1.75 % (802947)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4073835020:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.44/1.75 % (802952)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3819543336:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.44/1.75 % (802950)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3947283460:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.44/1.75 % (802950)Instruction limit reached!
% 5.44/1.75 % (802950)------------------------------
% 5.44/1.75 % (802950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802950)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802950)Termination reason: Instruction limit
% 5.44/1.75 % (802950)Termination phase: Saturation
% 5.44/1.75 % (802950)Time elapsed: 0.063 s
% 5.44/1.75 % (802950)Peak memory usage: 91 MB
% 5.44/1.75 % (802950)Instructions burned: 109 (million)
% 5.44/1.75 % (802953)Instruction limit reached!
% 5.44/1.75 % (802953)------------------------------
% 5.44/1.75 % (802953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802953)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802953)Termination reason: Instruction limit
% 5.44/1.75 % (802953)Termination phase: Saturation
% 5.44/1.75 % (802953)Time elapsed: 0.064 s
% 5.44/1.75 % (802953)Peak memory usage: 90 MB
% 5.44/1.75 % (802953)Instructions burned: 131 (million)
% 5.44/1.75 % (802951)Instruction limit reached!
% 5.44/1.75 % (802951)------------------------------
% 5.44/1.75 % (802951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802951)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802951)Termination reason: Instruction limit
% 5.44/1.75 % (802951)Termination phase: Saturation
% 5.44/1.75 % (802951)Time elapsed: 0.075 s
% 5.44/1.75 % (802951)Peak memory usage: 90 MB
% 5.44/1.75 % (802951)Instructions burned: 119 (million)
% 5.44/1.75 % (802952)Instruction limit reached!
% 5.44/1.75 % (802952)------------------------------
% 5.44/1.75 % (802952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802952)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802952)Termination reason: Instruction limit
% 5.44/1.75 % (802952)Termination phase: Saturation
% 5.44/1.75 % (802952)Time elapsed: 0.094 s
% 5.44/1.75 % (802952)Peak memory usage: 91 MB
% 5.44/1.75 % (802952)Instructions burned: 139 (million)
% 5.44/1.75 % (802962)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1904174274:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.44/1.75 % (802961)lrs+10_1_sil=8000:sp=occurrence:random_seed=2486738074:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.44/1.75 % (802963)lrs+1011_1_sil=32000:sp=occurrence:random_seed=234279930:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.44/1.75 % (802964)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=648275314:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.44/1.75 % (802962)Instruction limit reached!
% 5.44/1.75 % (802962)------------------------------
% 5.44/1.75 % (802962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802962)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802962)Termination reason: Instruction limit
% 5.44/1.75 % (802962)Termination phase: Saturation
% 5.44/1.75 % (802962)Time elapsed: 0.088 s
% 5.44/1.75 % (802962)Peak memory usage: 90 MB
% 5.44/1.75 % (802962)Instructions burned: 157 (million)
% 5.44/1.75 % (802964)Instruction limit reached!
% 5.44/1.75 % (802964)------------------------------
% 5.44/1.75 % (802964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802964)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802964)Termination reason: Instruction limit
% 5.44/1.75 % (802964)Termination phase: Saturation
% 5.44/1.75 % (802964)Time elapsed: 0.142 s
% 5.44/1.75 % (802964)Peak memory usage: 93 MB
% 5.44/1.75 % (802964)Instructions burned: 249 (million)
% 5.44/1.75 % (802961)Instruction limit reached!
% 5.44/1.75 % (802961)------------------------------
% 5.44/1.75 % (802961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802961)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802961)Termination reason: Instruction limit
% 5.44/1.75 % (802961)Termination phase: Saturation
% 5.44/1.75 % (802961)Time elapsed: 0.184 s
% 5.44/1.75 % (802961)Peak memory usage: 94 MB
% 5.44/1.75 % (802961)Instructions burned: 285 (million)
% 5.44/1.75 % (802963)Instruction limit reached!
% 5.44/1.75 % (802963)------------------------------
% 5.44/1.75 % (802963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802963)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802963)Termination reason: Instruction limit
% 5.44/1.75 % (802963)Termination phase: Saturation
% 5.44/1.75 % (802963)Time elapsed: 0.226 s
% 5.44/1.75 % (802963)Peak memory usage: 94 MB
% 5.44/1.75 % (802963)Instructions burned: 326 (million)
% 5.44/1.75 % (802969)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=692561179:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 5.44/1.75 % (802948)First to succeed.
% 5.44/1.75 % (802948)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-802942"
% 5.44/1.75 % (802970)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2591540474:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 5.44/1.75 % (802971)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2697300821:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 5.44/1.75 % (802972)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2399134927:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 5.44/1.75 % (802971)Instruction limit reached!
% 5.44/1.75 % (802971)------------------------------
% 5.44/1.75 % (802971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802971)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802971)Termination reason: Instruction limit
% 5.44/1.75 % (802971)Termination phase: Saturation
% 5.44/1.75 % (802971)Time elapsed: 0.072 s
% 5.44/1.75 % (802971)Peak memory usage: 91 MB
% 5.44/1.75 % (802971)Instructions burned: 114 (million)
% 5.44/1.75 % (802969)Instruction limit reached!
% 5.44/1.75 % (802969)------------------------------
% 5.44/1.75 % (802969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802969)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802969)Termination reason: Instruction limit
% 5.44/1.75 % (802969)Termination phase: Saturation
% 5.44/1.75 % (802969)Time elapsed: 0.193 s
% 5.44/1.75 % (802969)Peak memory usage: 92 MB
% 5.44/1.75 % (802969)Instructions burned: 295 (million)
% 5.44/1.75 % (802972)Instruction limit reached!
% 5.44/1.75 % (802972)------------------------------
% 5.44/1.75 % (802972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.75 % (802972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.75 % (802972)CaDiCaL version: 2.1.3
% 5.44/1.75 % (802972)Termination reason: Instruction limit
% 5.44/1.75 % (802972)Termination phase: Saturation
% 5.44/1.75 % (802972)Time elapsed: 0.068 s
% 5.44/1.75 % (802972)Peak memory usage: 90 MB
% 5.44/1.75 % (802972)Instructions burned: 127 (million)
% 5.44/1.75 % (802948)Refutation found. Thanks to Tanya!
% 5.44/1.75 % SZS status Theorem for theBenchmark
% 5.44/1.75 % SZS output start Proof for theBenchmark
% See solution above
% 6.76/1.94 % (802948)------------------------------
% 6.76/1.94 % (802948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/1.94 % (802948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.94 % (802948)CaDiCaL version: 2.1.3
% 6.76/1.94 % (802948)Termination reason: Refutation
% 6.76/1.94 % (802948)Time elapsed: 0.576 s
% 6.76/1.94 % (802948)Peak memory usage: 143 MB
% 6.76/1.94 % (802948)Instructions burned: 1512 (million)
% 6.76/1.94 % (802948)------------------------------
% 6.76/1.94 % (802948)------------------------------
% 6.76/1.94 % (802942)Success in time 0.882 s
% 6.76/1.94 % Vampire exiting
%------------------------------------------------------------------------------