%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU311+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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:17 PM UTC 2026
% Result : Theorem 6.20s 1.82s
% Output : Refutation 8.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 13
% Syntax : Number of formulae : 108 ( 23 unt; 8 def)
% Number of atoms : 348 ( 10 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 420 ( 180 ~; 180 |; 42 &)
% ( 8 <=>; 8 =>; 0 <=; 2 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 4 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-2 aty)
% Number of variables : 134 ( 0 sgn 114 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f192,axiom,
! [X0] : ~ empty(powerset(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f258,axiom,
! [X0,X1] :
( ! [X2] :
( in(X2,X0)
=> in(X2,X1) )
=> element(X0,powerset(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l71_subset_1) ).
fof(f320,axiom,
! [X0,X1] :
( ( topological_space(X0)
& top_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(X3,powerset(the_carrier(X0)))
& in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e2_37_1_1__pre_topc__1) ).
fof(f330,conjecture,
! [X0,X1] :
( ( topological_space(X0)
& top_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ? [X2] :
( element(X2,powerset(powerset(the_carrier(X0))))
& ! [X3] :
( element(X3,powerset(the_carrier(X0)))
=> ( in(X3,X2)
<=> in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s3_subset_1__e2_37_1_1__pre_topc) ).
fof(f331,negated_conjecture,
~ ! [X0,X1] :
( ( topological_space(X0)
& top_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ? [X2] :
( element(X2,powerset(powerset(the_carrier(X0))))
& ! [X3] :
( element(X3,powerset(the_carrier(X0)))
=> ( in(X3,X2)
<=> in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f330]) ).
fof(f407,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( empty(X1)
| in(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f779,plain,
! [X0,X1] :
( element(X0,powerset(X1))
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) ),
inference(ennf_transformation,[],[f258]) ).
fof(f838,plain,
! [X0,X1] :
( ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(X3,powerset(the_carrier(X0)))
& in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) )
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(ennf_transformation,[],[f320]) ).
fof(f839,plain,
! [X0,X1] :
( ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(X3,powerset(the_carrier(X0)))
& in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) )
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(flattening,[],[f838]) ).
fof(f854,plain,
? [X0,X1] :
( ! [X2] :
( ~ element(X2,powerset(powerset(the_carrier(X0))))
| ? [X3] :
( ( in(X3,X2)
<~> in(set_difference(cast_as_carrier_subset(X0),X3),X1) )
& element(X3,powerset(the_carrier(X0))) ) )
& topological_space(X0)
& top_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(ennf_transformation,[],[f331]) ).
fof(f855,plain,
? [X0,X1] :
( ! [X2] :
( ~ element(X2,powerset(powerset(the_carrier(X0))))
| ? [X3] :
( ( in(X3,X2)
<~> in(set_difference(cast_as_carrier_subset(X0),X3),X1) )
& element(X3,powerset(the_carrier(X0))) ) )
& topological_space(X0)
& top_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(flattening,[],[f854]) ).
fof(f953,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(ennf_transformation,[],[f407]) ).
fof(f954,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(flattening,[],[f953]) ).
fof(f1322,plain,
! [X0,X1] :
( element(X0,powerset(X1))
| ( ~ in(sK147(X0,X1),X1)
& in(sK147(X0,X1),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK147]),skolemize(X2,sK147(X0,X1))],[f779]) ).
fof(f1489,plain,
! [X0,X1] :
( ? [X2] :
! [X3] :
( ( in(X3,X2)
| ~ in(X3,powerset(the_carrier(X0)))
| ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1) )
& ( ( in(X3,powerset(the_carrier(X0)))
& in(set_difference(cast_as_carrier_subset(X0),X3),X1) )
| ~ in(X3,X2) ) )
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(nnf_transformation,[],[f839]) ).
fof(f1490,plain,
! [X0,X1] :
( ? [X2] :
! [X3] :
( ( in(X3,X2)
| ~ in(X3,powerset(the_carrier(X0)))
| ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1) )
& ( ( in(X3,powerset(the_carrier(X0)))
& in(set_difference(cast_as_carrier_subset(X0),X3),X1) )
| ~ in(X3,X2) ) )
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(flattening,[],[f1489]) ).
fof(f1491,plain,
! [X0,X1] :
( ! [X3] :
( ( in(X3,sK307(X0,X1))
| ~ in(X3,powerset(the_carrier(X0)))
| ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1) )
& ( ( in(X3,powerset(the_carrier(X0)))
& in(set_difference(cast_as_carrier_subset(X0),X3),X1) )
| ~ in(X3,sK307(X0,X1)) ) )
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK307]),skolemize(X2,sK307(X0,X1))],[f1490]) ).
fof(f1529,plain,
? [X0,X1] :
( ! [X2] :
( ~ element(X2,powerset(powerset(the_carrier(X0))))
| ? [X3] :
( ( ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| ~ in(X3,X2) )
& ( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| in(X3,X2) )
& element(X3,powerset(the_carrier(X0))) ) )
& topological_space(X0)
& top_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(nnf_transformation,[],[f855]) ).
fof(f1530,plain,
? [X0,X1] :
( ! [X2] :
( ~ element(X2,powerset(powerset(the_carrier(X0))))
| ? [X3] :
( ( ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| ~ in(X3,X2) )
& ( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| in(X3,X2) )
& element(X3,powerset(the_carrier(X0))) ) )
& topological_space(X0)
& top_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(flattening,[],[f1529]) ).
fof(f1531,plain,
( ! [X2] :
( ~ element(X2,powerset(powerset(the_carrier(sK337))))
| ( ( ~ in(set_difference(cast_as_carrier_subset(sK337),sK339(X2)),sK338)
| ~ in(sK339(X2),X2) )
& ( in(set_difference(cast_as_carrier_subset(sK337),sK339(X2)),sK338)
| in(sK339(X2),X2) )
& element(sK339(X2),powerset(the_carrier(sK337))) ) )
& topological_space(sK337)
& top_str(sK337)
& element(sK338,powerset(powerset(the_carrier(sK337)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK337,sK338,sK339]),skolemize(X0,sK337),skolemize(X1,sK338),skolemize(X3,sK339(X2))],[f1530]) ).
fof(f2050,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[],[f192]) ).
fof(f2194,plain,
! [X0,X1] :
( in(sK147(X0,X1),X0)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f1322]) ).
fof(f2195,plain,
! [X0,X1] :
( ~ in(sK147(X0,X1),X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f1322]) ).
fof(f2555,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ in(X3,sK307(X0,X1))
| ~ topological_space(X0)
| ~ top_str(X0)
| in(set_difference(cast_as_carrier_subset(X0),X3),X1) ),
inference(cnf_transformation,[],[f1491]) ).
fof(f2556,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ in(X3,sK307(X0,X1))
| ~ topological_space(X0)
| ~ top_str(X0)
| in(X3,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f1491]) ).
fof(f2557,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ in(X3,powerset(the_carrier(X0)))
| ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| in(X3,sK307(X0,X1)) ),
inference(cnf_transformation,[],[f1491]) ).
fof(f2622,plain,
element(sK338,powerset(powerset(the_carrier(sK337)))),
inference(cnf_transformation,[],[f1531]) ).
fof(f2623,plain,
top_str(sK337),
inference(cnf_transformation,[],[f1531]) ).
fof(f2624,plain,
topological_space(sK337),
inference(cnf_transformation,[],[f1531]) ).
fof(f2625,plain,
! [X2] :
( ~ element(X2,powerset(powerset(the_carrier(sK337))))
| element(sK339(X2),powerset(the_carrier(sK337))) ),
inference(cnf_transformation,[],[f1531]) ).
fof(f2626,plain,
! [X2] :
( ~ element(X2,powerset(powerset(the_carrier(sK337))))
| in(set_difference(cast_as_carrier_subset(sK337),sK339(X2)),sK338)
| in(sK339(X2),X2) ),
inference(cnf_transformation,[],[f1531]) ).
fof(f2627,plain,
! [X2] :
( ~ element(X2,powerset(powerset(the_carrier(sK337))))
| ~ in(set_difference(cast_as_carrier_subset(sK337),sK339(X2)),sK338)
| ~ in(sK339(X2),X2) ),
inference(cnf_transformation,[],[f1531]) ).
fof(f2738,plain,
! [X0,X1] :
( ~ element(X0,X1)
| in(X0,X1)
| empty(X1) ),
inference(cnf_transformation,[],[f954]) ).
fof(f3456,definition,
sF367 = the_carrier(sK337),
introduced(definition,[new_symbols(definition,[sF367])],[function_definition]) ).
fof(f3457,plain,
the_carrier(sK337) = sF367,
inference(reorient_equations,[],[f3456]) ).
fof(f3458,definition,
sF368 = powerset(sF367),
introduced(definition,[new_symbols(definition,[sF368])],[function_definition]) ).
fof(f3459,plain,
powerset(sF367) = sF368,
inference(reorient_equations,[],[f3458]) ).
fof(f3460,definition,
sF369 = powerset(sF368),
introduced(definition,[new_symbols(definition,[sF369])],[function_definition]) ).
fof(f3461,plain,
powerset(sF368) = sF369,
inference(reorient_equations,[],[f3460]) ).
fof(f3462,definition,
sF370 = cast_as_carrier_subset(sK337),
introduced(definition,[new_symbols(definition,[sF370])],[function_definition]) ).
fof(f3463,plain,
cast_as_carrier_subset(sK337) = sF370,
inference(reorient_equations,[],[f3462]) ).
fof(f3464,definition,
! [X2] : sF371(X2) = set_difference(sF370,sK339(X2)),
introduced(definition,[new_symbols(definition,[sF371])],[function_definition]) ).
fof(f3465,plain,
! [X2] : set_difference(sF370,sK339(X2)) = sF371(X2),
inference(reorient_equations,[],[f3464]) ).
fof(f3466,plain,
! [X2] :
( ~ in(sF371(X2),sK338)
| ~ element(X2,sF369)
| ~ in(sK339(X2),X2) ),
inference(definition_folding,[],[f2627,f3465,f3463,f3461,f3459,f3457]) ).
fof(f3467,plain,
! [X2] :
( in(sF371(X2),sK338)
| in(sK339(X2),X2)
| ~ element(X2,sF369) ),
inference(definition_folding,[],[f2626,f3465,f3463,f3461,f3459,f3457]) ).
fof(f3468,plain,
! [X2] :
( element(sK339(X2),sF368)
| ~ element(X2,sF369) ),
inference(definition_folding,[],[f2625,f3459,f3457,f3461,f3459,f3457]) ).
fof(f3469,plain,
element(sK338,sF369),
inference(definition_folding,[],[f2622,f3461,f3459,f3457]) ).
fof(f3791,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(sF367)))
| ~ in(X1,powerset(sF367))
| ~ in(set_difference(cast_as_carrier_subset(sK337),X1),X0)
| ~ topological_space(sK337)
| ~ top_str(sK337)
| in(X1,sK307(sK337,X0)) ),
inference(superposition,[],[f2557,f3457]) ).
fof(f3792,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(sF367)))
| ~ in(X1,powerset(sF367))
| ~ in(set_difference(cast_as_carrier_subset(sK337),X1),X0)
| ~ top_str(sK337)
| in(X1,sK307(sK337,X0)) ),
inference(forward_subsumption_resolution,[],[f3791,f2624]) ).
fof(f3793,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(sF367)))
| ~ in(X1,powerset(sF367))
| ~ in(set_difference(cast_as_carrier_subset(sK337),X1),X0)
| in(X1,sK307(sK337,X0)) ),
inference(forward_subsumption_resolution,[],[f3792,f2623]) ).
fof(f3794,plain,
! [X0,X1] :
( ~ element(X0,powerset(sF368))
| ~ in(X1,powerset(sF367))
| ~ in(set_difference(cast_as_carrier_subset(sK337),X1),X0)
| in(X1,sK307(sK337,X0)) ),
inference(forward_demodulation,[],[f3793,f3459]) ).
fof(f3795,plain,
! [X0,X1] :
( ~ element(X0,sF369)
| ~ in(X1,powerset(sF367))
| ~ in(set_difference(cast_as_carrier_subset(sK337),X1),X0)
| in(X1,sK307(sK337,X0)) ),
inference(forward_demodulation,[],[f3794,f3461]) ).
fof(f3796,plain,
! [X0,X1] :
( ~ in(X1,sF368)
| ~ element(X0,sF369)
| ~ in(set_difference(cast_as_carrier_subset(sK337),X1),X0)
| in(X1,sK307(sK337,X0)) ),
inference(forward_demodulation,[],[f3795,f3459]) ).
fof(f3797,plain,
! [X0,X1] :
( ~ in(set_difference(sF370,X1),X0)
| ~ in(X1,sF368)
| ~ element(X0,sF369)
| in(X1,sK307(sK337,X0)) ),
inference(forward_demodulation,[],[f3796,f3463]) ).
fof(f3798,plain,
! [X0,X1] :
( in(sK339(X0),sK307(sK337,X1))
| ~ in(sK339(X0),sF368)
| ~ element(X1,sF369)
| ~ in(sF371(X0),X1) ),
inference(superposition,[],[f3797,f3465]) ).
fof(f3807,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(sF367)))
| ~ in(X1,sK307(sK337,X0))
| ~ topological_space(sK337)
| ~ top_str(sK337)
| in(set_difference(cast_as_carrier_subset(sK337),X1),X0) ),
inference(superposition,[],[f2555,f3457]) ).
fof(f3808,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(sF367)))
| ~ in(X1,sK307(sK337,X0))
| ~ top_str(sK337)
| in(set_difference(cast_as_carrier_subset(sK337),X1),X0) ),
inference(forward_subsumption_resolution,[],[f3807,f2624]) ).
fof(f3809,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(sF367)))
| ~ in(X1,sK307(sK337,X0))
| in(set_difference(cast_as_carrier_subset(sK337),X1),X0) ),
inference(forward_subsumption_resolution,[],[f3808,f2623]) ).
fof(f3810,plain,
! [X0,X1] :
( ~ element(X0,powerset(sF368))
| ~ in(X1,sK307(sK337,X0))
| in(set_difference(cast_as_carrier_subset(sK337),X1),X0) ),
inference(forward_demodulation,[],[f3809,f3459]) ).
fof(f3811,plain,
! [X0,X1] :
( ~ element(X0,sF369)
| ~ in(X1,sK307(sK337,X0))
| in(set_difference(cast_as_carrier_subset(sK337),X1),X0) ),
inference(forward_demodulation,[],[f3810,f3461]) ).
fof(f3812,plain,
! [X0,X1] :
( ~ in(X1,sK307(sK337,X0))
| ~ element(X0,sF369)
| in(set_difference(sF370,X1),X0) ),
inference(forward_demodulation,[],[f3811,f3463]) ).
fof(f3814,plain,
! [X0] :
( ~ element(X0,sF369)
| in(set_difference(sF370,sK339(sK307(sK337,X0))),X0)
| in(sF371(sK307(sK337,X0)),sK338)
| ~ element(sK307(sK337,X0),sF369) ),
inference(resolution,[],[f3812,f3467]) ).
fof(f3815,plain,
! [X0] :
( in(sF371(sK307(sK337,X0)),sK338)
| in(sF371(sK307(sK337,X0)),X0)
| ~ element(X0,sF369)
| ~ element(sK307(sK337,X0),sF369) ),
inference(forward_demodulation,[],[f3814,f3465]) ).
fof(f3818,plain,
( in(sF371(sK307(sK337,sK338)),sK338)
| ~ element(sK338,sF369)
| ~ element(sK307(sK337,sK338),sF369) ),
inference(factoring,[],[f3815]) ).
fof(f3820,plain,
( in(sF371(sK307(sK337,sK338)),sK338)
| ~ element(sK307(sK337,sK338),sF369) ),
inference(forward_subsumption_resolution,[],[f3818,f3469]) ).
fof(f3822,definition,
( spl372_57
<=> element(sK307(sK337,sK338),sF369) ),
introduced(definition,[new_symbols(definition,[spl372_57])],[avatar_definition]) ).
fof(f3823,plain,
( element(sK307(sK337,sK338),sF369)
| ~ spl372_57 ),
inference(avatar_component_clause,[],[f3822]) ).
fof(f3824,plain,
( ~ element(sK307(sK337,sK338),sF369)
| spl372_57 ),
inference(avatar_component_clause,[],[f3822]) ).
fof(f3826,definition,
( spl372_58
<=> in(sF371(sK307(sK337,sK338)),sK338) ),
introduced(definition,[new_symbols(definition,[spl372_58])],[avatar_definition]) ).
fof(f3828,plain,
( in(sF371(sK307(sK337,sK338)),sK338)
| ~ spl372_58 ),
inference(avatar_component_clause,[],[f3826]) ).
fof(f3829,plain,
( ~ spl372_57
| spl372_58 ),
inference(avatar_split_clause,[],[f3820,f3826,f3822]) ).
fof(f3883,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(sF367)))
| ~ in(X1,sK307(sK337,X0))
| ~ topological_space(sK337)
| ~ top_str(sK337)
| in(X1,powerset(sF367)) ),
inference(superposition,[],[f2556,f3457]) ).
fof(f3884,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(sF367)))
| ~ in(X1,sK307(sK337,X0))
| ~ top_str(sK337)
| in(X1,powerset(sF367)) ),
inference(forward_subsumption_resolution,[],[f3883,f2624]) ).
fof(f3885,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(sF367)))
| ~ in(X1,sK307(sK337,X0))
| in(X1,powerset(sF367)) ),
inference(forward_subsumption_resolution,[],[f3884,f2623]) ).
fof(f3886,plain,
! [X0,X1] :
( ~ element(X0,powerset(sF368))
| ~ in(X1,sK307(sK337,X0))
| in(X1,powerset(sF367)) ),
inference(forward_demodulation,[],[f3885,f3459]) ).
fof(f3887,plain,
! [X0,X1] :
( ~ element(X0,sF369)
| ~ in(X1,sK307(sK337,X0))
| in(X1,powerset(sF367)) ),
inference(forward_demodulation,[],[f3886,f3461]) ).
fof(f3888,plain,
! [X0,X1] :
( ~ in(X1,sK307(sK337,X0))
| ~ element(X0,sF369)
| in(X1,sF368) ),
inference(forward_demodulation,[],[f3887,f3459]) ).
fof(f3889,plain,
! [X0,X1] :
( in(sK147(sK307(sK337,X0),X1),sF368)
| ~ element(X0,sF369)
| element(sK307(sK337,X0),powerset(X1)) ),
inference(resolution,[],[f3888,f2194]) ).
fof(f3931,plain,
~ empty(sF368),
inference(superposition,[],[f2050,f3459]) ).
fof(f4058,plain,
! [X0] :
( ~ element(X0,sF369)
| element(sK307(sK337,X0),powerset(sF368))
| element(sK307(sK337,X0),powerset(sF368)) ),
inference(resolution,[],[f3889,f2195]) ).
fof(f4060,plain,
! [X0] :
( ~ element(X0,sF369)
| element(sK307(sK337,X0),powerset(sF368)) ),
inference(duplicate_literal_removal,[],[f4058]) ).
fof(f4061,plain,
! [X0] :
( element(sK307(sK337,X0),sF369)
| ~ element(X0,sF369) ),
inference(forward_demodulation,[],[f4060,f3461]) ).
fof(f4062,plain,
( ~ element(sK338,sF369)
| spl372_57 ),
inference(resolution,[],[f4061,f3824]) ).
fof(f4069,plain,
( $false
| spl372_57 ),
inference(forward_subsumption_resolution,[],[f4062,f3469]) ).
fof(f4070,plain,
spl372_57,
inference(avatar_contradiction_clause,[],[f4069]) ).
fof(f4071,plain,
( ~ element(sK307(sK337,sK338),sF369)
| ~ in(sK339(sK307(sK337,sK338)),sK307(sK337,sK338))
| ~ spl372_58 ),
inference(resolution,[],[f3828,f3466]) ).
fof(f4073,plain,
( ~ in(sK339(sK307(sK337,sK338)),sK307(sK337,sK338))
| ~ spl372_57
| ~ spl372_58 ),
inference(forward_subsumption_resolution,[],[f4071,f3823]) ).
fof(f4074,plain,
( ~ in(sK339(sK307(sK337,sK338)),sF368)
| ~ element(sK338,sF369)
| ~ in(sF371(sK307(sK337,sK338)),sK338)
| ~ spl372_57
| ~ spl372_58 ),
inference(resolution,[],[f4073,f3798]) ).
fof(f4076,plain,
( ~ in(sK339(sK307(sK337,sK338)),sF368)
| ~ in(sF371(sK307(sK337,sK338)),sK338)
| ~ spl372_57
| ~ spl372_58 ),
inference(forward_subsumption_resolution,[],[f4074,f3469]) ).
fof(f4077,plain,
( ~ in(sK339(sK307(sK337,sK338)),sF368)
| ~ spl372_57
| ~ spl372_58 ),
inference(forward_subsumption_resolution,[],[f4076,f3828]) ).
fof(f4092,definition,
( spl372_66
<=> element(sK339(sK307(sK337,sK338)),sF368) ),
introduced(definition,[new_symbols(definition,[spl372_66])],[avatar_definition]) ).
fof(f4093,plain,
( element(sK339(sK307(sK337,sK338)),sF368)
| ~ spl372_66 ),
inference(avatar_component_clause,[],[f4092]) ).
fof(f4094,plain,
( ~ element(sK339(sK307(sK337,sK338)),sF368)
| spl372_66 ),
inference(avatar_component_clause,[],[f4092]) ).
fof(f4096,plain,
( ~ element(sK307(sK337,sK338),sF369)
| spl372_66 ),
inference(resolution,[],[f4094,f3468]) ).
fof(f4097,plain,
( $false
| ~ spl372_57
| spl372_66 ),
inference(forward_subsumption_resolution,[],[f4096,f3823]) ).
fof(f4098,plain,
( ~ spl372_57
| spl372_66 ),
inference(avatar_contradiction_clause,[],[f4097]) ).
fof(f4290,plain,
( in(sK339(sK307(sK337,sK338)),sF368)
| empty(sF368)
| ~ spl372_66 ),
inference(resolution,[],[f2738,f4093]) ).
fof(f4300,plain,
( empty(sF368)
| ~ spl372_57
| ~ spl372_58
| ~ spl372_66 ),
inference(forward_subsumption_resolution,[],[f4290,f4077]) ).
fof(f4313,plain,
( $false
| ~ spl372_57
| ~ spl372_58
| ~ spl372_66 ),
inference(forward_subsumption_resolution,[],[f4300,f3931]) ).
fof(f4314,plain,
( ~ spl372_57
| ~ spl372_58
| ~ spl372_66 ),
inference(avatar_contradiction_clause,[],[f4313]) ).
cnf(s49,plain,
( ~ spl372_57
| spl372_58 ),
inference(sat_conversion,[],[f3829]) ).
cnf(s53,plain,
spl372_57,
inference(sat_conversion,[],[f4070]) ).
cnf(s55,plain,
( ~ spl372_57
| spl372_66 ),
inference(sat_conversion,[],[f4098]) ).
cnf(s65,plain,
( ~ spl372_57
| ~ spl372_58
| ~ spl372_66 ),
inference(sat_conversion,[],[f4314]) ).
cnf(s66,plain,
spl372_66,
inference(rat,[],[s55,s53]) ).
cnf(s67,plain,
~ spl372_58,
inference(rat,[],[s65,s53,s66]) ).
cnf(s70,plain,
$false,
inference(rat,[],[s49,s67,s53]) ).
fof(f4315,plain,
$false,
inference(avatar_sat_refutation,[],[s70]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU311+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 : n017.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.14/0.38 % CPULimit : 300
% 0.14/0.38 % WCLimit : 300
% 0.14/0.38 % DateTime : Mon Sep 28 04:33:51 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.14/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.44 Running first-order theorem proving
% 0.14/0.44 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
% 6.20/1.82 % (3204673)Detected formulas, will run a generic FOF schedule.
% 6.20/1.82 % (3204687)dis-21_1_sil=8000:lcm=predicate:random_seed=835456606: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)
% 6.20/1.82 % (3204687)Instruction limit reached!
% 6.20/1.82 % (3204687)------------------------------
% 6.20/1.82 % (3204687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204687)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204687)Termination reason: Instruction limit
% 6.20/1.82 % (3204687)Termination phase: Saturation
% 6.20/1.82 % (3204687)Time elapsed: 0.036 s
% 6.20/1.82 % (3204687)Peak memory usage: 91 MB
% 6.20/1.82 % (3204687)Instructions burned: 132 (million)
% 6.20/1.82 % (3204681)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=2347003655:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.20/1.82 % (3204682)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=3705161394:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.20/1.82 % (3204685)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1076149648:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.20/1.82 % (3204683)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=3151882119:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.20/1.82 % (3204684)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3236649258:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.20/1.82 % (3204686)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=113420659:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.20/1.82 % (3204684)Instruction limit reached!
% 6.20/1.82 % (3204684)------------------------------
% 6.20/1.82 % (3204684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204684)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204684)Termination reason: Instruction limit
% 6.20/1.82 % (3204684)Termination phase: Saturation
% 6.20/1.82 % (3204684)Time elapsed: 0.063 s
% 6.20/1.82 % (3204684)Peak memory usage: 91 MB
% 6.20/1.82 % (3204684)Instructions burned: 109 (million)
% 6.20/1.82 % (3204685)Instruction limit reached!
% 6.20/1.82 % (3204685)------------------------------
% 6.20/1.82 % (3204685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204685)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204685)Termination reason: Instruction limit
% 6.20/1.82 % (3204685)Termination phase: Saturation
% 6.20/1.82 % (3204685)Time elapsed: 0.078 s
% 6.20/1.82 % (3204685)Peak memory usage: 90 MB
% 6.20/1.82 % (3204685)Instructions burned: 121 (million)
% 6.20/1.82 % (3204695)lrs+10_1_sil=8000:sp=occurrence:random_seed=4014841076:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 6.20/1.82 % (3204686)Instruction limit reached!
% 6.20/1.82 % (3204686)------------------------------
% 6.20/1.82 % (3204686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204686)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204686)Termination reason: Instruction limit
% 6.20/1.82 % (3204686)Termination phase: Saturation
% 6.20/1.82 % (3204686)Time elapsed: 0.097 s
% 6.20/1.82 % (3204686)Peak memory usage: 91 MB
% 6.20/1.82 % (3204686)Instructions burned: 139 (million)
% 6.20/1.82 % (3204695)Instruction limit reached!
% 6.20/1.82 % (3204695)------------------------------
% 6.20/1.82 % (3204695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204695)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204695)Termination reason: Instruction limit
% 6.20/1.82 % (3204695)Termination phase: Saturation
% 6.20/1.82 % (3204695)Time elapsed: 0.105 s
% 6.20/1.82 % (3204695)Peak memory usage: 94 MB
% 6.20/1.82 % (3204695)Instructions burned: 287 (million)
% 6.20/1.82 % (3204697)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3493641981:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 6.20/1.82 % (3204698)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2194499318:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 6.20/1.82 % (3204700)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=2799666972:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 6.20/1.82 % (3204702)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4257919994:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 6.20/1.82 % (3204697)Instruction limit reached!
% 6.20/1.82 % (3204697)------------------------------
% 6.20/1.82 % (3204697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204697)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204697)Termination reason: Instruction limit
% 6.20/1.82 % (3204697)Termination phase: Saturation
% 6.20/1.82 % (3204697)Time elapsed: 0.103 s
% 6.20/1.82 % (3204697)Peak memory usage: 91 MB
% 6.20/1.82 % (3204697)Instructions burned: 158 (million)
% 6.20/1.82 % (3204700)Instruction limit reached!
% 6.20/1.82 % (3204700)------------------------------
% 6.20/1.82 % (3204700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204700)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204700)Termination reason: Instruction limit
% 6.20/1.82 % (3204700)Termination phase: Saturation
% 6.20/1.82 % (3204700)Time elapsed: 0.156 s
% 6.20/1.82 % (3204700)Peak memory usage: 93 MB
% 6.20/1.82 % (3204700)Instructions burned: 248 (million)
% 6.20/1.82 % (3204702)Instruction limit reached!
% 6.20/1.82 % (3204702)------------------------------
% 6.20/1.82 % (3204702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204702)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204702)Termination reason: Instruction limit
% 6.20/1.82 % (3204702)Termination phase: Saturation
% 6.20/1.82 % (3204702)Time elapsed: 0.103 s
% 6.20/1.82 % (3204702)Peak memory usage: 92 MB
% 6.20/1.82 % (3204702)Instructions burned: 296 (million)
% 6.20/1.82 % (3204745)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=606375561:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 6.20/1.82 % (3204698)Instruction limit reached!
% 6.20/1.82 % (3204698)------------------------------
% 6.20/1.82 % (3204698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204698)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204698)Termination reason: Instruction limit
% 6.20/1.82 % (3204698)Termination phase: Saturation
% 6.20/1.82 % (3204698)Time elapsed: 0.229 s
% 6.20/1.82 % (3204698)Peak memory usage: 94 MB
% 6.20/1.82 % (3204698)Instructions burned: 325 (million)
% 6.20/1.82 % (3204774)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4164780073:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 6.20/1.82 % (3204777)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=782683315:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 6.20/1.82 % (3204790)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=785326416:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 6.20/1.82 % (3204774)Instruction limit reached!
% 6.20/1.82 % (3204774)------------------------------
% 6.20/1.82 % (3204774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204774)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204774)Termination reason: Instruction limit
% 6.20/1.82 % (3204774)Termination phase: Saturation
% 6.20/1.82 % (3204774)Time elapsed: 0.070 s
% 6.20/1.82 % (3204774)Peak memory usage: 91 MB
% 6.20/1.82 % (3204774)Instructions burned: 113 (million)
% 6.20/1.82 % (3204777)Instruction limit reached!
% 6.20/1.82 % (3204777)------------------------------
% 6.20/1.82 % (3204777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204777)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204777)Termination reason: Instruction limit
% 6.20/1.82 % (3204777)Termination phase: Saturation
% 6.20/1.82 % (3204777)Time elapsed: 0.069 s
% 6.20/1.82 % (3204777)Peak memory usage: 91 MB
% 6.20/1.82 % (3204777)Instructions burned: 128 (million)
% 6.20/1.82 % (3204790)Instruction limit reached!
% 6.20/1.82 % (3204790)------------------------------
% 6.20/1.82 % (3204790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.20/1.82 % (3204790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.82 % (3204790)CaDiCaL version: 2.1.3
% 6.20/1.82 % (3204790)Termination reason: Instruction limit
% 6.20/1.82 % (3204790)Termination phase: Saturation
% 6.20/1.82 % (3204790)Time elapsed: 0.058 s
% 6.20/1.82 % (3204790)Peak memory usage: 90 MB
% 6.20/1.82 % (3204790)Instructions burned: 116 (million)
% 6.20/1.82 % (3204819)lrs+10_1_sil=8000:sp=occurrence:random_seed=3173860747:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 6.20/1.82 % (3204820)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=323826022:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 6.20/1.82 % (3204821)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=357425446:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 6.20/1.82 % (3204681)First to succeed.
% 6.20/1.82 % (3204681)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3204673"
% 6.20/1.82 % (3204681)Refutation found. Thanks to Tanya!
% 6.20/1.82 % SZS status Theorem for theBenchmark
% 6.20/1.82 % SZS output start Proof for theBenchmark
% See solution above
% 8.06/2.01 % (3204681)------------------------------
% 8.06/2.01 % (3204681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.01 % (3204681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.01 % (3204681)CaDiCaL version: 2.1.3
% 8.06/2.01 % (3204681)Termination reason: Refutation
% 8.06/2.01 % (3204681)Time elapsed: 0.785 s
% 8.06/2.01 % (3204681)Peak memory usage: 146 MB
% 8.06/2.01 % (3204681)Instructions burned: 1538 (million)
% 8.06/2.01 % (3204681)------------------------------
% 8.06/2.01 % (3204681)------------------------------
% 8.06/2.01 % (3204673)Success in time 1.08 s
% 8.06/2.01 % Vampire exiting
%------------------------------------------------------------------------------