%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU344+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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:26 PM UTC 2026
% Result : Theorem 6.35s 1.85s
% Output : Refutation 7.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 20
% Syntax : Number of formulae : 149 ( 20 unt; 12 def)
% Number of atoms : 508 ( 46 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 611 ( 252 ~; 281 |; 45 &)
% ( 21 <=>; 11 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 13 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 122 ( 0 sgn 108 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f88,axiom,
! [X0,X1,X2] :
( X2 = set_union2(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X0)
| in(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_xboole_0) ).
fof(f91,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& join_semilatt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( below(X0,X1,X2)
<=> join(X0,X1,X2) = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_lattices) ).
fof(f95,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f141,axiom,
! [X0] :
( strict_latt_str(boole_lattice(X0))
& latt_str(boole_lattice(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice3) ).
fof(f195,axiom,
! [X0] :
( latt_str(X0)
=> ( meet_semilatt_str(X0)
& join_semilatt_str(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f226,axiom,
! [X0] :
( ~ empty_carrier(boole_lattice(X0))
& strict_latt_str(boole_lattice(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice3) ).
fof(f455,axiom,
! [X0,X1] :
( element(X1,the_carrier(boole_lattice(X0)))
=> ! [X2] :
( element(X2,the_carrier(boole_lattice(X0)))
=> ( join(boole_lattice(X0),X1,X2) = set_union2(X1,X2)
& meet(boole_lattice(X0),X1,X2) = set_intersection2(X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_lattice3) ).
fof(f490,conjecture,
! [X0,X1] :
( element(X1,the_carrier(boole_lattice(X0)))
=> ! [X2] :
( element(X2,the_carrier(boole_lattice(X0)))
=> ( below(boole_lattice(X0),X1,X2)
<=> subset(X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_lattice3) ).
fof(f491,negated_conjecture,
~ ! [X0,X1] :
( element(X1,the_carrier(boole_lattice(X0)))
=> ! [X2] :
( element(X2,the_carrier(boole_lattice(X0)))
=> ( below(boole_lattice(X0),X1,X2)
<=> subset(X1,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f490]) ).
fof(f757,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( below(X0,X1,X2)
<=> join(X0,X1,X2) = X2 )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ join_semilatt_str(X0) ),
inference(ennf_transformation,[],[f91]) ).
fof(f758,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( below(X0,X1,X2)
<=> join(X0,X1,X2) = X2 )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ join_semilatt_str(X0) ),
inference(flattening,[],[f757]) ).
fof(f762,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f95]) ).
fof(f850,plain,
! [X0] :
( ( meet_semilatt_str(X0)
& join_semilatt_str(X0) )
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f195]) ).
fof(f1149,plain,
! [X0,X1] :
( ! [X2] :
( ( join(boole_lattice(X0),X1,X2) = set_union2(X1,X2)
& meet(boole_lattice(X0),X1,X2) = set_intersection2(X1,X2) )
| ~ element(X2,the_carrier(boole_lattice(X0))) )
| ~ element(X1,the_carrier(boole_lattice(X0))) ),
inference(ennf_transformation,[],[f455]) ).
fof(f1202,plain,
? [X0,X1] :
( ? [X2] :
( ( below(boole_lattice(X0),X1,X2)
<~> subset(X1,X2) )
& element(X2,the_carrier(boole_lattice(X0))) )
& element(X1,the_carrier(boole_lattice(X0))) ),
inference(ennf_transformation,[],[f491]) ).
fof(f1480,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X0)
& ~ in(X3,X1) ) )
& ( in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f88]) ).
fof(f1481,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X0)
& ~ in(X3,X1) ) )
& ( in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(flattening,[],[f1480]) ).
fof(f1482,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( ~ in(X4,X0)
& ~ in(X4,X1) ) )
& ( in(X4,X0)
| in(X4,X1)
| ~ in(X4,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(rectify,[],[f1481]) ).
fof(f1483,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ( ( ( ~ in(sK73(X0,X1,X2),X0)
& ~ in(sK73(X0,X1,X2),X1) )
| ~ in(sK73(X0,X1,X2),X2) )
& ( in(sK73(X0,X1,X2),X0)
| in(sK73(X0,X1,X2),X1)
| in(sK73(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( ~ in(X4,X0)
& ~ in(X4,X1) ) )
& ( in(X4,X0)
| in(X4,X1)
| ~ in(X4,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK73]),skolemize(X3,sK73(X0,X1,X2))],[f1482]) ).
fof(f1490,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( below(X0,X1,X2)
| join(X0,X1,X2) != X2 )
& ( join(X0,X1,X2) = X2
| ~ below(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ join_semilatt_str(X0) ),
inference(nnf_transformation,[],[f758]) ).
fof(f1497,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) )
| ~ subset(X0,X1) ) ),
inference(nnf_transformation,[],[f762]) ).
fof(f1498,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(rectify,[],[f1497]) ).
fof(f1499,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK85(X0,X1),X1)
& in(sK85(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK85]),skolemize(X2,sK85(X0,X1))],[f1498]) ).
fof(f1854,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ subset(X1,X2)
| ~ below(boole_lattice(X0),X1,X2) )
& ( subset(X1,X2)
| below(boole_lattice(X0),X1,X2) )
& element(X2,the_carrier(boole_lattice(X0))) )
& element(X1,the_carrier(boole_lattice(X0))) ),
inference(nnf_transformation,[],[f1202]) ).
fof(f1855,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ subset(X1,X2)
| ~ below(boole_lattice(X0),X1,X2) )
& ( subset(X1,X2)
| below(boole_lattice(X0),X1,X2) )
& element(X2,the_carrier(boole_lattice(X0))) )
& element(X1,the_carrier(boole_lattice(X0))) ),
inference(flattening,[],[f1854]) ).
fof(f1856,plain,
( ( ~ subset(sK433,sK434)
| ~ below(boole_lattice(sK432),sK433,sK434) )
& ( subset(sK433,sK434)
| below(boole_lattice(sK432),sK433,sK434) )
& element(sK434,the_carrier(boole_lattice(sK432)))
& element(sK433,the_carrier(boole_lattice(sK432))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK432,sK433,sK434]),skolemize(X0,sK432),skolemize(X1,sK433),skolemize(X2,sK434)],[f1855]) ).
fof(f2190,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,X0)
| set_union2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f1483]) ).
fof(f2191,plain,
! [X2,X0,X1] :
( set_union2(X0,X1) = X2
| in(sK73(X0,X1,X2),X0)
| in(sK73(X0,X1,X2),X1)
| in(sK73(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f1483]) ).
fof(f2192,plain,
! [X2,X0,X1] :
( set_union2(X0,X1) = X2
| ~ in(sK73(X0,X1,X2),X1)
| ~ in(sK73(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f1483]) ).
fof(f2210,plain,
! [X2,X0,X1] :
( join(X0,X1,X2) = X2
| ~ below(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ join_semilatt_str(X0) ),
inference(cnf_transformation,[],[f1490]) ).
fof(f2211,plain,
! [X2,X0,X1] :
( below(X0,X1,X2)
| join(X0,X1,X2) != X2
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ join_semilatt_str(X0) ),
inference(cnf_transformation,[],[f1490]) ).
fof(f2222,plain,
! [X3,X0,X1] :
( in(X3,X1)
| ~ in(X3,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f1499]) ).
fof(f2223,plain,
! [X0,X1] :
( subset(X0,X1)
| in(sK85(X0,X1),X0) ),
inference(cnf_transformation,[],[f1499]) ).
fof(f2224,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ in(sK85(X0,X1),X1) ),
inference(cnf_transformation,[],[f1499]) ).
fof(f2378,plain,
! [X0] : latt_str(boole_lattice(X0)),
inference(cnf_transformation,[],[f141]) ).
fof(f2413,plain,
! [X0] :
( join_semilatt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f850]) ).
fof(f2457,plain,
! [X0] : ~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[],[f226]) ).
fof(f3457,plain,
! [X2,X0,X1] :
( set_union2(X1,X2) = join(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0))) ),
inference(cnf_transformation,[],[f1149]) ).
fof(f3511,plain,
element(sK433,the_carrier(boole_lattice(sK432))),
inference(cnf_transformation,[],[f1856]) ).
fof(f3512,plain,
element(sK434,the_carrier(boole_lattice(sK432))),
inference(cnf_transformation,[],[f1856]) ).
fof(f3513,plain,
( subset(sK433,sK434)
| below(boole_lattice(sK432),sK433,sK434) ),
inference(cnf_transformation,[],[f1856]) ).
fof(f3514,plain,
( ~ subset(sK433,sK434)
| ~ below(boole_lattice(sK432),sK433,sK434) ),
inference(cnf_transformation,[],[f1856]) ).
fof(f4238,plain,
! [X0,X1,X4] :
( in(X4,set_union2(X0,X1))
| ~ in(X4,X0) ),
inference(equality_resolution,[],[f2190]) ).
fof(f4975,definition,
( spl573_1
<=> below(boole_lattice(sK432),sK433,sK434) ),
introduced(definition,[new_symbols(definition,[spl573_1])],[avatar_definition]) ).
fof(f4976,plain,
( ~ below(boole_lattice(sK432),sK433,sK434)
| spl573_1 ),
inference(avatar_component_clause,[],[f4975]) ).
fof(f4977,plain,
( below(boole_lattice(sK432),sK433,sK434)
| ~ spl573_1 ),
inference(avatar_component_clause,[],[f4975]) ).
fof(f4979,definition,
( spl573_2
<=> subset(sK433,sK434) ),
introduced(definition,[new_symbols(definition,[spl573_2])],[avatar_definition]) ).
fof(f4980,plain,
( ~ subset(sK433,sK434)
| spl573_2 ),
inference(avatar_component_clause,[],[f4979]) ).
fof(f4981,plain,
( subset(sK433,sK434)
| ~ spl573_2 ),
inference(avatar_component_clause,[],[f4979]) ).
fof(f4982,plain,
( spl573_1
| spl573_2 ),
inference(avatar_split_clause,[],[f3513,f4979,f4975]) ).
fof(f4983,plain,
( ~ below(boole_lattice(sK432),sK433,sK434)
| ~ spl573_2 ),
inference(backward_subsumption_resolution,[],[f3514,f4981]) ).
fof(f4984,plain,
( ~ spl573_1
| ~ spl573_2 ),
inference(avatar_split_clause,[],[f4983,f4979,f4975]) ).
fof(f4988,plain,
( ! [X0] :
( in(X0,sK434)
| ~ in(X0,sK433) )
| ~ spl573_2 ),
inference(resolution,[],[f4981,f2222]) ).
fof(f5000,plain,
( sK434 != join(boole_lattice(sK432),sK433,sK434)
| ~ element(sK434,the_carrier(boole_lattice(sK432)))
| ~ element(sK433,the_carrier(boole_lattice(sK432)))
| empty_carrier(boole_lattice(sK432))
| ~ join_semilatt_str(boole_lattice(sK432))
| spl573_1 ),
inference(resolution,[],[f4976,f2211]) ).
fof(f5004,plain,
( sK434 != join(boole_lattice(sK432),sK433,sK434)
| ~ element(sK433,the_carrier(boole_lattice(sK432)))
| empty_carrier(boole_lattice(sK432))
| ~ join_semilatt_str(boole_lattice(sK432))
| spl573_1 ),
inference(forward_subsumption_resolution,[],[f5000,f3512]) ).
fof(f5006,plain,
( sK434 != join(boole_lattice(sK432),sK433,sK434)
| empty_carrier(boole_lattice(sK432))
| ~ join_semilatt_str(boole_lattice(sK432))
| spl573_1 ),
inference(forward_subsumption_resolution,[],[f5004,f3511]) ).
fof(f5008,plain,
( sK434 != join(boole_lattice(sK432),sK433,sK434)
| ~ join_semilatt_str(boole_lattice(sK432))
| spl573_1 ),
inference(forward_subsumption_resolution,[],[f5006,f2457]) ).
fof(f5012,definition,
( spl573_3
<=> element(sK433,the_carrier(boole_lattice(sK432))) ),
introduced(definition,[new_symbols(definition,[spl573_3])],[avatar_definition]) ).
fof(f5014,plain,
( element(sK433,the_carrier(boole_lattice(sK432)))
| ~ spl573_3 ),
inference(avatar_component_clause,[],[f5012]) ).
fof(f5015,plain,
spl573_3,
inference(avatar_split_clause,[],[f3511,f5012]) ).
fof(f5122,definition,
( spl573_4
<=> element(sK434,the_carrier(boole_lattice(sK432))) ),
introduced(definition,[new_symbols(definition,[spl573_4])],[avatar_definition]) ).
fof(f5124,plain,
( element(sK434,the_carrier(boole_lattice(sK432)))
| ~ spl573_4 ),
inference(avatar_component_clause,[],[f5122]) ).
fof(f5125,plain,
spl573_4,
inference(avatar_split_clause,[],[f3512,f5122]) ).
fof(f5242,definition,
( spl573_7
<=> ! [X0] :
( in(X0,sK434)
| ~ in(X0,sK433) ) ),
introduced(definition,[new_symbols(definition,[spl573_7])],[avatar_definition]) ).
fof(f5243,plain,
( ! [X0] :
( ~ in(X0,sK433)
| in(X0,sK434) )
| ~ spl573_7 ),
inference(avatar_component_clause,[],[f5242]) ).
fof(f5244,plain,
( spl573_7
| ~ spl573_2 ),
inference(avatar_split_clause,[],[f4988,f4979,f5242]) ).
fof(f5500,definition,
( spl573_8
<=> join_semilatt_str(boole_lattice(sK432)) ),
introduced(definition,[new_symbols(definition,[spl573_8])],[avatar_definition]) ).
fof(f5501,plain,
( join_semilatt_str(boole_lattice(sK432))
| ~ spl573_8 ),
inference(avatar_component_clause,[],[f5500]) ).
fof(f5502,plain,
( ~ join_semilatt_str(boole_lattice(sK432))
| spl573_8 ),
inference(avatar_component_clause,[],[f5500]) ).
fof(f5504,definition,
( spl573_9
<=> sK434 = join(boole_lattice(sK432),sK433,sK434) ),
introduced(definition,[new_symbols(definition,[spl573_9])],[avatar_definition]) ).
fof(f5505,plain,
( sK434 = join(boole_lattice(sK432),sK433,sK434)
| ~ spl573_9 ),
inference(avatar_component_clause,[],[f5504]) ).
fof(f5506,plain,
( sK434 != join(boole_lattice(sK432),sK433,sK434)
| spl573_9 ),
inference(avatar_component_clause,[],[f5504]) ).
fof(f5507,plain,
( ~ spl573_8
| ~ spl573_9
| spl573_1 ),
inference(avatar_split_clause,[],[f5008,f4975,f5504,f5500]) ).
fof(f5508,plain,
( ~ latt_str(boole_lattice(sK432))
| spl573_8 ),
inference(resolution,[],[f5502,f2413]) ).
fof(f5515,plain,
( $false
| spl573_8 ),
inference(forward_subsumption_resolution,[],[f5508,f2378]) ).
fof(f5516,plain,
spl573_8,
inference(avatar_contradiction_clause,[],[f5515]) ).
fof(f5546,plain,
( sK434 != sK434
| ~ below(boole_lattice(sK432),sK433,sK434)
| ~ element(sK434,the_carrier(boole_lattice(sK432)))
| ~ element(sK433,the_carrier(boole_lattice(sK432)))
| empty_carrier(boole_lattice(sK432))
| ~ join_semilatt_str(boole_lattice(sK432))
| spl573_9 ),
inference(superposition,[],[f5506,f2210]) ).
fof(f5547,plain,
( ~ below(boole_lattice(sK432),sK433,sK434)
| ~ element(sK434,the_carrier(boole_lattice(sK432)))
| ~ element(sK433,the_carrier(boole_lattice(sK432)))
| empty_carrier(boole_lattice(sK432))
| ~ join_semilatt_str(boole_lattice(sK432))
| spl573_9 ),
inference(trivial_inequality_removal,[],[f5546]) ).
fof(f5886,definition,
( spl573_20
<=> ! [X2,X0,X1] :
( set_union2(X1,X2) = join(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0))) ) ),
introduced(definition,[new_symbols(definition,[spl573_20])],[avatar_definition]) ).
fof(f5887,plain,
( ! [X2,X0,X1] :
( set_union2(X1,X2) = join(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0))) )
| ~ spl573_20 ),
inference(avatar_component_clause,[],[f5886]) ).
fof(f5888,plain,
spl573_20,
inference(avatar_split_clause,[],[f3457,f5886]) ).
fof(f5898,plain,
( sK434 != set_union2(sK433,sK434)
| ~ element(sK434,the_carrier(boole_lattice(sK432)))
| ~ element(sK433,the_carrier(boole_lattice(sK432)))
| spl573_9
| ~ spl573_20 ),
inference(superposition,[],[f5506,f5887]) ).
fof(f5943,plain,
( sK434 != set_union2(sK433,sK434)
| ~ element(sK433,the_carrier(boole_lattice(sK432)))
| ~ spl573_4
| spl573_9
| ~ spl573_20 ),
inference(forward_subsumption_resolution,[],[f5898,f5124]) ).
fof(f5952,plain,
( sK434 != set_union2(sK433,sK434)
| ~ spl573_3
| ~ spl573_4
| spl573_9
| ~ spl573_20 ),
inference(forward_subsumption_resolution,[],[f5943,f5014]) ).
fof(f5959,definition,
( spl573_21
<=> sK434 = set_union2(sK433,sK434) ),
introduced(definition,[new_symbols(definition,[spl573_21])],[avatar_definition]) ).
fof(f5960,plain,
( sK434 = set_union2(sK433,sK434)
| ~ spl573_21 ),
inference(avatar_component_clause,[],[f5959]) ).
fof(f5961,plain,
( sK434 != set_union2(sK433,sK434)
| spl573_21 ),
inference(avatar_component_clause,[],[f5959]) ).
fof(f5962,plain,
( ~ spl573_21
| ~ spl573_3
| ~ spl573_4
| spl573_9
| ~ spl573_20 ),
inference(avatar_split_clause,[],[f5952,f5886,f5504,f5122,f5012,f5959]) ).
fof(f5964,plain,
( ! [X0] :
( sK434 != X0
| ~ in(sK73(sK433,sK434,X0),sK434)
| ~ in(sK73(sK433,sK434,X0),X0) )
| spl573_21 ),
inference(superposition,[],[f5961,f2192]) ).
fof(f6046,definition,
( spl573_28
<=> ! [X0] :
( sK434 != X0
| ~ in(sK73(sK433,sK434,X0),sK434)
| ~ in(sK73(sK433,sK434,X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl573_28])],[avatar_definition]) ).
fof(f6047,plain,
( ! [X0] :
( sK434 != X0
| ~ in(sK73(sK433,sK434,X0),sK434)
| ~ in(sK73(sK433,sK434,X0),X0) )
| ~ spl573_28 ),
inference(avatar_component_clause,[],[f6046]) ).
fof(f6048,plain,
( spl573_28
| spl573_21 ),
inference(avatar_split_clause,[],[f5964,f5959,f6046]) ).
fof(f6049,plain,
( ~ in(sK73(sK433,sK434,sK434),sK434)
| ~ in(sK73(sK433,sK434,sK434),sK434)
| ~ spl573_28 ),
inference(equality_resolution,[],[f6047]) ).
fof(f6050,plain,
( ~ in(sK73(sK433,sK434,sK434),sK434)
| ~ spl573_28 ),
inference(duplicate_literal_removal,[],[f6049]) ).
fof(f6052,definition,
( spl573_29
<=> in(sK73(sK433,sK434,sK434),sK434) ),
introduced(definition,[new_symbols(definition,[spl573_29])],[avatar_definition]) ).
fof(f6054,plain,
( ~ in(sK73(sK433,sK434,sK434),sK434)
| spl573_29 ),
inference(avatar_component_clause,[],[f6052]) ).
fof(f6055,plain,
( ~ spl573_29
| ~ spl573_28 ),
inference(avatar_split_clause,[],[f6050,f6046,f6052]) ).
fof(f6056,plain,
( sK434 = set_union2(sK433,sK434)
| in(sK73(sK433,sK434,sK434),sK433)
| in(sK73(sK433,sK434,sK434),sK434)
| spl573_29 ),
inference(resolution,[],[f6054,f2191]) ).
fof(f6069,plain,
( sK434 = set_union2(sK433,sK434)
| in(sK73(sK433,sK434,sK434),sK434)
| ~ spl573_7
| spl573_29 ),
inference(forward_subsumption_resolution,[],[f6056,f5243]) ).
fof(f6071,plain,
( in(sK73(sK433,sK434,sK434),sK434)
| ~ spl573_7
| spl573_21
| spl573_29 ),
inference(forward_subsumption_resolution,[],[f6069,f5961]) ).
fof(f6074,plain,
( $false
| ~ spl573_7
| spl573_21
| spl573_29 ),
inference(forward_subsumption_resolution,[],[f6071,f6054]) ).
fof(f6075,plain,
( ~ spl573_7
| spl573_21
| spl573_29 ),
inference(avatar_contradiction_clause,[],[f6074]) ).
fof(f6078,plain,
( ~ element(sK434,the_carrier(boole_lattice(sK432)))
| ~ element(sK433,the_carrier(boole_lattice(sK432)))
| empty_carrier(boole_lattice(sK432))
| ~ join_semilatt_str(boole_lattice(sK432))
| ~ spl573_1
| spl573_9 ),
inference(forward_subsumption_resolution,[],[f5547,f4977]) ).
fof(f6083,plain,
( ~ element(sK433,the_carrier(boole_lattice(sK432)))
| empty_carrier(boole_lattice(sK432))
| ~ join_semilatt_str(boole_lattice(sK432))
| ~ spl573_1
| ~ spl573_4
| spl573_9 ),
inference(forward_subsumption_resolution,[],[f6078,f5124]) ).
fof(f6088,plain,
( empty_carrier(boole_lattice(sK432))
| ~ join_semilatt_str(boole_lattice(sK432))
| ~ spl573_1
| ~ spl573_3
| ~ spl573_4
| spl573_9 ),
inference(forward_subsumption_resolution,[],[f6083,f5014]) ).
fof(f6089,plain,
( ~ join_semilatt_str(boole_lattice(sK432))
| ~ spl573_1
| ~ spl573_3
| ~ spl573_4
| spl573_9 ),
inference(forward_subsumption_resolution,[],[f6088,f2457]) ).
fof(f6090,plain,
( $false
| ~ spl573_1
| ~ spl573_3
| ~ spl573_4
| ~ spl573_8
| spl573_9 ),
inference(forward_subsumption_resolution,[],[f6089,f5501]) ).
fof(f6091,plain,
( ~ spl573_1
| ~ spl573_3
| ~ spl573_4
| ~ spl573_8
| spl573_9 ),
inference(avatar_contradiction_clause,[],[f6090]) ).
fof(f6104,plain,
( sK434 = set_union2(sK433,sK434)
| ~ element(sK434,the_carrier(boole_lattice(sK432)))
| ~ element(sK433,the_carrier(boole_lattice(sK432)))
| ~ spl573_9
| ~ spl573_20 ),
inference(superposition,[],[f5505,f5887]) ).
fof(f6114,plain,
( ~ element(sK434,the_carrier(boole_lattice(sK432)))
| ~ element(sK433,the_carrier(boole_lattice(sK432)))
| ~ spl573_9
| ~ spl573_20
| spl573_21 ),
inference(forward_subsumption_resolution,[],[f6104,f5961]) ).
fof(f6116,plain,
( ~ element(sK433,the_carrier(boole_lattice(sK432)))
| ~ spl573_4
| ~ spl573_9
| ~ spl573_20
| spl573_21 ),
inference(forward_subsumption_resolution,[],[f6114,f5124]) ).
fof(f6119,plain,
( $false
| ~ spl573_3
| ~ spl573_4
| ~ spl573_9
| ~ spl573_20
| spl573_21 ),
inference(forward_subsumption_resolution,[],[f6116,f5014]) ).
fof(f6120,plain,
( ~ spl573_3
| ~ spl573_4
| ~ spl573_9
| ~ spl573_20
| spl573_21 ),
inference(avatar_contradiction_clause,[],[f6119]) ).
fof(f6133,plain,
( ! [X0] :
( in(X0,sK434)
| ~ in(X0,sK433) )
| ~ spl573_21 ),
inference(superposition,[],[f4238,f5960]) ).
fof(f6142,plain,
( spl573_7
| ~ spl573_21 ),
inference(avatar_split_clause,[],[f6133,f5959,f5242]) ).
fof(f6315,plain,
( in(sK85(sK433,sK434),sK433)
| spl573_2 ),
inference(resolution,[],[f4980,f2223]) ).
fof(f6316,plain,
( ~ in(sK85(sK433,sK434),sK434)
| spl573_2 ),
inference(resolution,[],[f4980,f2224]) ).
fof(f6322,definition,
( spl573_30
<=> in(sK85(sK433,sK434),sK433) ),
introduced(definition,[new_symbols(definition,[spl573_30])],[avatar_definition]) ).
fof(f6324,plain,
( in(sK85(sK433,sK434),sK433)
| ~ spl573_30 ),
inference(avatar_component_clause,[],[f6322]) ).
fof(f6325,plain,
( spl573_30
| spl573_2 ),
inference(avatar_split_clause,[],[f6315,f4979,f6322]) ).
fof(f6326,plain,
( in(sK85(sK433,sK434),sK434)
| ~ spl573_7
| ~ spl573_30 ),
inference(resolution,[],[f6324,f5243]) ).
fof(f6394,plain,
( $false
| spl573_2
| ~ spl573_7
| ~ spl573_30 ),
inference(forward_subsumption_resolution,[],[f6326,f6316]) ).
fof(f6395,plain,
( spl573_2
| ~ spl573_7
| ~ spl573_30 ),
inference(avatar_contradiction_clause,[],[f6394]) ).
cnf(s1,plain,
( spl573_1
| spl573_2 ),
inference(sat_conversion,[],[f4982]) ).
cnf(s2,plain,
( ~ spl573_1
| ~ spl573_2 ),
inference(sat_conversion,[],[f4984]) ).
cnf(s3,plain,
spl573_3,
inference(sat_conversion,[],[f5015]) ).
cnf(s4,plain,
spl573_4,
inference(sat_conversion,[],[f5125]) ).
cnf(s7,plain,
( ~ spl573_2
| spl573_7 ),
inference(sat_conversion,[],[f5244]) ).
cnf(s8,plain,
( spl573_1
| ~ spl573_8
| ~ spl573_9 ),
inference(sat_conversion,[],[f5507]) ).
cnf(s9,plain,
spl573_8,
inference(sat_conversion,[],[f5516]) ).
cnf(s20,plain,
spl573_20,
inference(sat_conversion,[],[f5888]) ).
cnf(s21,plain,
( ~ spl573_3
| ~ spl573_4
| spl573_9
| ~ spl573_20
| ~ spl573_21 ),
inference(sat_conversion,[],[f5962]) ).
cnf(s28,plain,
( spl573_21
| spl573_28 ),
inference(sat_conversion,[],[f6048]) ).
cnf(s29,plain,
( ~ spl573_28
| ~ spl573_29 ),
inference(sat_conversion,[],[f6055]) ).
cnf(s31,plain,
( ~ spl573_7
| spl573_21
| spl573_29 ),
inference(sat_conversion,[],[f6075]) ).
cnf(s34,plain,
( ~ spl573_1
| ~ spl573_3
| ~ spl573_4
| ~ spl573_8
| spl573_9 ),
inference(sat_conversion,[],[f6091]) ).
cnf(s36,plain,
( ~ spl573_3
| ~ spl573_4
| ~ spl573_9
| ~ spl573_20
| spl573_21 ),
inference(sat_conversion,[],[f6120]) ).
cnf(s37,plain,
( spl573_7
| ~ spl573_21 ),
inference(sat_conversion,[],[f6142]) ).
cnf(s38,plain,
( spl573_2
| spl573_30 ),
inference(sat_conversion,[],[f6325]) ).
cnf(s39,plain,
( spl573_2
| ~ spl573_7
| ~ spl573_30 ),
inference(sat_conversion,[],[f6395]) ).
cnf(s41,plain,
( spl573_1
| ~ spl573_9 ),
inference(rat,[],[s8,s9]) ).
cnf(s59,plain,
spl573_1,
inference(rat,[],[s29,s31,s28,s7,s21,s1,s41,s4,s20,s3]) ).
cnf(s60,plain,
spl573_9,
inference(rat,[],[s34,s3,s9,s4,s59]) ).
cnf(s61,plain,
~ spl573_2,
inference(rat,[],[s2,s59]) ).
cnf(s62,plain,
spl573_21,
inference(rat,[],[s36,s3,s20,s4,s60]) ).
cnf(s63,plain,
spl573_30,
inference(rat,[],[s38,s61]) ).
cnf(s64,plain,
~ spl573_7,
inference(rat,[],[s39,s63,s61]) ).
cnf(s65,plain,
$false,
inference(rat,[],[s37,s62,s64]) ).
fof(f6399,plain,
$false,
inference(avatar_sat_refutation,[],[s65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU344+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n009.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 04:49:15 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/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
% 6.35/1.85 % (2667755)Detected formulas, will run a generic FOF schedule.
% 6.35/1.85 % (2667762)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=473437214:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.35/1.85 % (2667766)dis-21_1_sil=8000:lcm=predicate:random_seed=294031671: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.35/1.85 % (2667761)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=212398167:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.35/1.85 % (2667764)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1578169079:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.35/1.85 % (2667760)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=3139527930:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.35/1.85 % (2667763)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=381159803:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.35/1.85 % (2667765)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1304407744:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.35/1.85 % (2667763)Instruction limit reached!
% 6.35/1.85 % (2667763)------------------------------
% 6.35/1.85 % (2667763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667763)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667763)Termination reason: Instruction limit
% 6.35/1.85 % (2667763)Termination phase: Saturation
% 6.35/1.85 % (2667763)Time elapsed: 0.058 s
% 6.35/1.85 % (2667763)Peak memory usage: 91 MB
% 6.35/1.85 % (2667763)Instructions burned: 109 (million)
% 6.35/1.85 % (2667766)Instruction limit reached!
% 6.35/1.85 % (2667766)------------------------------
% 6.35/1.85 % (2667766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667766)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667766)Termination reason: Instruction limit
% 6.35/1.85 % (2667766)Termination phase: Saturation
% 6.35/1.85 % (2667766)Time elapsed: 0.065 s
% 6.35/1.85 % (2667766)Peak memory usage: 91 MB
% 6.35/1.85 % (2667766)Instructions burned: 130 (million)
% 6.35/1.85 % (2667764)Instruction limit reached!
% 6.35/1.85 % (2667764)------------------------------
% 6.35/1.85 % (2667764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667764)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667764)Termination reason: Instruction limit
% 6.35/1.85 % (2667764)Termination phase: Saturation
% 6.35/1.85 % (2667764)Time elapsed: 0.075 s
% 6.35/1.85 % (2667764)Peak memory usage: 91 MB
% 6.35/1.85 % (2667764)Instructions burned: 120 (million)
% 6.35/1.85 % (2667765)Instruction limit reached!
% 6.35/1.85 % (2667765)------------------------------
% 6.35/1.85 % (2667765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667765)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667765)Termination reason: Instruction limit
% 6.35/1.85 % (2667765)Termination phase: Saturation
% 6.35/1.85 % (2667765)Time elapsed: 0.090 s
% 6.35/1.85 % (2667765)Peak memory usage: 92 MB
% 6.35/1.85 % (2667765)Instructions burned: 140 (million)
% 6.35/1.85 % (2667774)lrs+10_1_sil=8000:sp=occurrence:random_seed=2694214860:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 6.35/1.85 % (2667776)lrs+1011_1_sil=32000:sp=occurrence:random_seed=765660021:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 6.35/1.85 % (2667775)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1367552615:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 6.35/1.85 % (2667777)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=3763057014:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 6.35/1.85 % (2667775)Instruction limit reached!
% 6.35/1.85 % (2667775)------------------------------
% 6.35/1.85 % (2667775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667775)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667775)Termination reason: Instruction limit
% 6.35/1.85 % (2667775)Termination phase: Saturation
% 6.35/1.85 % (2667775)Time elapsed: 0.079 s
% 6.35/1.85 % (2667775)Peak memory usage: 91 MB
% 6.35/1.85 % (2667775)Instructions burned: 158 (million)
% 6.35/1.85 % (2667774)Instruction limit reached!
% 6.35/1.85 % (2667774)------------------------------
% 6.35/1.85 % (2667774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667774)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667774)Termination reason: Instruction limit
% 6.35/1.85 % (2667774)Termination phase: Saturation
% 6.35/1.85 % (2667774)Time elapsed: 0.182 s
% 6.35/1.85 % (2667774)Peak memory usage: 95 MB
% 6.35/1.85 % (2667774)Instructions burned: 285 (million)
% 6.35/1.85 % (2667777)Instruction limit reached!
% 6.35/1.85 % (2667777)------------------------------
% 6.35/1.85 % (2667777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667777)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667777)Termination reason: Instruction limit
% 6.35/1.85 % (2667777)Termination phase: Saturation
% 6.35/1.85 % (2667777)Time elapsed: 0.147 s
% 6.35/1.85 % (2667777)Peak memory usage: 94 MB
% 6.35/1.85 % (2667777)Instructions burned: 250 (million)
% 6.35/1.85 % (2667776)Instruction limit reached!
% 6.35/1.85 % (2667776)------------------------------
% 6.35/1.85 % (2667776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667776)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667776)Termination reason: Instruction limit
% 6.35/1.85 % (2667776)Termination phase: Saturation
% 6.35/1.85 % (2667776)Time elapsed: 0.223 s
% 6.35/1.85 % (2667776)Peak memory usage: 94 MB
% 6.35/1.85 % (2667776)Instructions burned: 325 (million)
% 6.35/1.85 % (2667782)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1420711552:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 6.35/1.85 % (2667783)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1431576113:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 6.35/1.85 % (2667784)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3979993287:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 6.35/1.85 % (2667785)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2817962029:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 6.35/1.85 % (2667762)First to succeed.
% 6.35/1.85 % (2667762)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2667755"
% 6.35/1.85 % (2667784)Instruction limit reached!
% 6.35/1.85 % (2667784)------------------------------
% 6.35/1.85 % (2667784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667784)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667784)Termination reason: Instruction limit
% 6.35/1.85 % (2667784)Termination phase: Saturation
% 6.35/1.85 % (2667784)Time elapsed: 0.066 s
% 6.35/1.85 % (2667784)Peak memory usage: 92 MB
% 6.35/1.85 % (2667784)Instructions burned: 113 (million)
% 6.35/1.85 % (2667782)Instruction limit reached!
% 6.35/1.85 % (2667782)------------------------------
% 6.35/1.85 % (2667782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667782)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667782)Termination reason: Instruction limit
% 6.35/1.85 % (2667782)Termination phase: Saturation
% 6.35/1.85 % (2667782)Time elapsed: 0.186 s
% 6.35/1.85 % (2667782)Peak memory usage: 93 MB
% 6.35/1.85 % (2667782)Instructions burned: 295 (million)
% 6.35/1.85 % (2667785)Instruction limit reached!
% 6.35/1.85 % (2667785)------------------------------
% 6.35/1.85 % (2667785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.85 % (2667785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.85 % (2667785)CaDiCaL version: 2.1.3
% 6.35/1.85 % (2667785)Termination reason: Instruction limit
% 6.35/1.85 % (2667785)Termination phase: Saturation
% 6.35/1.85 % (2667785)Time elapsed: 0.072 s
% 6.35/1.85 % (2667785)Peak memory usage: 91 MB
% 6.35/1.85 % (2667785)Instructions burned: 129 (million)
% 6.35/1.85 % (2667762)Refutation found. Thanks to Tanya!
% 6.35/1.85 % SZS status Theorem for theBenchmark
% 6.35/1.85 % SZS output start Proof for theBenchmark
% See solution above
% 7.36/2.03 % (2667762)------------------------------
% 7.36/2.03 % (2667762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.36/2.03 % (2667762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.36/2.03 % (2667762)CaDiCaL version: 2.1.3
% 7.36/2.03 % (2667762)Termination reason: Refutation
% 7.36/2.03 % (2667762)Time elapsed: 0.681 s
% 7.36/2.03 % (2667762)Peak memory usage: 152 MB
% 7.36/2.03 % (2667762)Instructions burned: 1880 (million)
% 7.36/2.03 % (2667762)------------------------------
% 7.36/2.03 % (2667762)------------------------------
% 7.36/2.03 % (2667755)Success in time 0.994 s
% 7.36/2.03 % Vampire exiting
%------------------------------------------------------------------------------