%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT327+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 11:46:58 AM UTC 2026
% Result : Theorem 3.05s 1.89s
% Output : Refutation 7.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 9
% Syntax : Number of formulae : 101 ( 16 unt; 5 def)
% Number of atoms : 471 ( 0 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 644 ( 274 ~; 288 |; 58 &)
% ( 8 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 6 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-3 aty)
% Number of variables : 68 ( 0 sgn 62 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2318,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f2415,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> r3_lattices(X0,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r3_lattices) ).
fof(f2999,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_filter_2) ).
fof(f3000,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X1,k22_filter_2(X0,X1,X2))
& r2_hidden(X2,k22_filter_2(X0,X1,X2)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_filter_2) ).
fof(f3001,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X1,k22_filter_2(X0,X1,X2))
& r2_hidden(X2,k22_filter_2(X0,X1,X2)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3000]) ).
fof(f3039,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r2_hidden(X1,k22_filter_2(X0,X1,X2))
| ~ r2_hidden(X2,k22_filter_2(X0,X1,X2)) )
& r3_lattices(X0,X1,X2)
& m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f3001]) ).
fof(f3040,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r2_hidden(X1,k22_filter_2(X0,X1,X2))
| ~ r2_hidden(X2,k22_filter_2(X0,X1,X2)) )
& r3_lattices(X0,X1,X2)
& m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f3039]) ).
fof(f3182,plain,
! [X0,X1,X2] :
( r3_lattices(X0,X1,X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f2415]) ).
fof(f3183,plain,
! [X0,X1,X2] :
( r3_lattices(X0,X1,X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f3182]) ).
fof(f3192,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2999]) ).
fof(f3193,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3192]) ).
fof(f3996,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2318]) ).
fof(f3997,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3996]) ).
fof(f4054,plain,
( ( ~ r2_hidden(sK16,k22_filter_2(sK15,sK16,sK17))
| ~ r2_hidden(sK17,k22_filter_2(sK15,sK16,sK17)) )
& r3_lattices(sK15,sK16,sK17)
& m1_subset_1(sK17,u1_struct_0(sK15))
& m1_subset_1(sK16,u1_struct_0(sK15))
& ~ v3_struct_0(sK15)
& v10_lattices(sK15)
& l3_lattices(sK15) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17]),skolemize(X0,sK15),skolemize(X1,sK16),skolemize(X2,sK17)],[f3040]) ).
fof(f4137,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2) )
& ( ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) )
| ~ r2_hidden(X3,k22_filter_2(X0,X1,X2)) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f3193]) ).
fof(f4138,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2) )
& ( ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) )
| ~ r2_hidden(X3,k22_filter_2(X0,X1,X2)) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f4137]) ).
fof(f4414,plain,
l3_lattices(sK15),
inference(cnf_transformation,[],[f4054]) ).
fof(f4415,plain,
v10_lattices(sK15),
inference(cnf_transformation,[],[f4054]) ).
fof(f4416,plain,
~ v3_struct_0(sK15),
inference(cnf_transformation,[],[f4054]) ).
fof(f4417,plain,
m1_subset_1(sK16,u1_struct_0(sK15)),
inference(cnf_transformation,[],[f4054]) ).
fof(f4418,plain,
m1_subset_1(sK17,u1_struct_0(sK15)),
inference(cnf_transformation,[],[f4054]) ).
fof(f4419,plain,
r3_lattices(sK15,sK16,sK17),
inference(cnf_transformation,[],[f4054]) ).
fof(f4420,plain,
( ~ r2_hidden(sK16,k22_filter_2(sK15,sK16,sK17))
| ~ r2_hidden(sK17,k22_filter_2(sK15,sK16,sK17)) ),
inference(cnf_transformation,[],[f4054]) ).
fof(f4626,plain,
! [X2,X0,X1] :
( r3_lattices(X0,X1,X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f3183]) ).
fof(f4634,plain,
! [X2,X3,X0,X1] :
( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f4138]) ).
fof(f5832,plain,
! [X0] :
( v9_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3997]) ).
fof(f5833,plain,
! [X0] :
( v8_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3997]) ).
fof(f5835,plain,
! [X0] :
( v6_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3997]) ).
fof(f6250,definition,
( spl237_1
<=> r2_hidden(sK17,k22_filter_2(sK15,sK16,sK17)) ),
introduced(definition,[new_symbols(definition,[spl237_1])],[avatar_definition]) ).
fof(f6252,plain,
( ~ r2_hidden(sK17,k22_filter_2(sK15,sK16,sK17))
| spl237_1 ),
inference(avatar_component_clause,[],[f6250]) ).
fof(f6254,definition,
( spl237_2
<=> r2_hidden(sK16,k22_filter_2(sK15,sK16,sK17)) ),
introduced(definition,[new_symbols(definition,[spl237_2])],[avatar_definition]) ).
fof(f6256,plain,
( ~ r2_hidden(sK16,k22_filter_2(sK15,sK16,sK17))
| spl237_2 ),
inference(avatar_component_clause,[],[f6254]) ).
fof(f6257,plain,
( ~ spl237_1
| ~ spl237_2 ),
inference(avatar_split_clause,[],[f4420,f6254,f6250]) ).
fof(f6296,definition,
( spl237_6
<=> v9_lattices(sK15) ),
introduced(definition,[new_symbols(definition,[spl237_6])],[avatar_definition]) ).
fof(f6297,plain,
( v9_lattices(sK15)
| ~ spl237_6 ),
inference(avatar_component_clause,[],[f6296]) ).
fof(f6298,plain,
( ~ v9_lattices(sK15)
| spl237_6 ),
inference(avatar_component_clause,[],[f6296]) ).
fof(f6300,definition,
( spl237_7
<=> v8_lattices(sK15) ),
introduced(definition,[new_symbols(definition,[spl237_7])],[avatar_definition]) ).
fof(f6301,plain,
( v8_lattices(sK15)
| ~ spl237_7 ),
inference(avatar_component_clause,[],[f6300]) ).
fof(f6302,plain,
( ~ v8_lattices(sK15)
| spl237_7 ),
inference(avatar_component_clause,[],[f6300]) ).
fof(f6304,definition,
( spl237_8
<=> v6_lattices(sK15) ),
introduced(definition,[new_symbols(definition,[spl237_8])],[avatar_definition]) ).
fof(f6305,plain,
( v6_lattices(sK15)
| ~ spl237_8 ),
inference(avatar_component_clause,[],[f6304]) ).
fof(f6306,plain,
( ~ v6_lattices(sK15)
| spl237_8 ),
inference(avatar_component_clause,[],[f6304]) ).
fof(f6312,plain,
( v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_6 ),
inference(resolution,[],[f6298,f5832]) ).
fof(f6315,plain,
( ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_6 ),
inference(forward_subsumption_resolution,[],[f6312,f4416]) ).
fof(f6317,plain,
( ~ l3_lattices(sK15)
| spl237_6 ),
inference(forward_subsumption_resolution,[],[f6315,f4415]) ).
fof(f6320,plain,
( $false
| spl237_6 ),
inference(forward_subsumption_resolution,[],[f6317,f4414]) ).
fof(f6321,plain,
spl237_6,
inference(avatar_contradiction_clause,[],[f6320]) ).
fof(f6322,plain,
( ~ r3_lattices(sK15,sK16,sK17)
| ~ r3_lattices(sK15,sK17,sK17)
| ~ r3_lattices(sK15,sK16,sK17)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_1 ),
inference(resolution,[],[f6252,f4634]) ).
fof(f6324,plain,
( ~ r3_lattices(sK15,sK16,sK17)
| ~ r3_lattices(sK15,sK17,sK17)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_1 ),
inference(duplicate_literal_removal,[],[f6322]) ).
fof(f6342,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_1 ),
inference(forward_subsumption_resolution,[],[f6324,f4419]) ).
fof(f6343,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_1 ),
inference(forward_subsumption_resolution,[],[f6342,f4418]) ).
fof(f6344,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_1 ),
inference(forward_subsumption_resolution,[],[f6343,f4417]) ).
fof(f6345,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_1 ),
inference(forward_subsumption_resolution,[],[f6344,f4416]) ).
fof(f6346,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| ~ l3_lattices(sK15)
| spl237_1 ),
inference(forward_subsumption_resolution,[],[f6345,f4415]) ).
fof(f6347,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| spl237_1 ),
inference(forward_subsumption_resolution,[],[f6346,f4414]) ).
fof(f6350,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| ~ r3_lattices(sK15,sK16,sK17)
| ~ r3_lattices(sK15,sK16,sK17)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_2 ),
inference(resolution,[],[f6256,f4634]) ).
fof(f6352,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| ~ r3_lattices(sK15,sK16,sK17)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_2 ),
inference(duplicate_literal_removal,[],[f6350]) ).
fof(f6353,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_2 ),
inference(forward_subsumption_resolution,[],[f6352,f4419]) ).
fof(f6354,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_2 ),
inference(forward_subsumption_resolution,[],[f6353,f4417]) ).
fof(f6355,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_2 ),
inference(forward_subsumption_resolution,[],[f6354,f4418]) ).
fof(f6356,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_2 ),
inference(forward_subsumption_resolution,[],[f6355,f4416]) ).
fof(f6357,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| ~ l3_lattices(sK15)
| spl237_2 ),
inference(forward_subsumption_resolution,[],[f6356,f4415]) ).
fof(f6358,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| spl237_2 ),
inference(forward_subsumption_resolution,[],[f6357,f4414]) ).
fof(f6359,plain,
( v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_7 ),
inference(resolution,[],[f6302,f5833]) ).
fof(f6362,plain,
( ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_7 ),
inference(forward_subsumption_resolution,[],[f6359,f4416]) ).
fof(f6364,plain,
( ~ l3_lattices(sK15)
| spl237_7 ),
inference(forward_subsumption_resolution,[],[f6362,f4415]) ).
fof(f6367,plain,
( $false
| spl237_7 ),
inference(forward_subsumption_resolution,[],[f6364,f4414]) ).
fof(f6368,plain,
spl237_7,
inference(avatar_contradiction_clause,[],[f6367]) ).
fof(f6369,plain,
( v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_8 ),
inference(resolution,[],[f6306,f5835]) ).
fof(f6372,plain,
( ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl237_8 ),
inference(forward_subsumption_resolution,[],[f6369,f4416]) ).
fof(f6374,plain,
( ~ l3_lattices(sK15)
| spl237_8 ),
inference(forward_subsumption_resolution,[],[f6372,f4415]) ).
fof(f6377,plain,
( $false
| spl237_8 ),
inference(forward_subsumption_resolution,[],[f6374,f4414]) ).
fof(f6378,plain,
spl237_8,
inference(avatar_contradiction_clause,[],[f6377]) ).
fof(f6402,plain,
( ! [X0] :
( v3_struct_0(sK15)
| ~ v6_lattices(sK15)
| ~ v8_lattices(sK15)
| ~ v9_lattices(sK15)
| ~ l3_lattices(sK15)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_1 ),
inference(resolution,[],[f6347,f4626]) ).
fof(f6406,plain,
( ! [X0] :
( ~ v6_lattices(sK15)
| ~ v8_lattices(sK15)
| ~ v9_lattices(sK15)
| ~ l3_lattices(sK15)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_1 ),
inference(forward_subsumption_resolution,[],[f6402,f4416]) ).
fof(f6408,plain,
( ! [X0] :
( ~ v8_lattices(sK15)
| ~ v9_lattices(sK15)
| ~ l3_lattices(sK15)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_1
| ~ spl237_8 ),
inference(forward_subsumption_resolution,[],[f6406,f6305]) ).
fof(f6410,plain,
( ! [X0] :
( ~ v9_lattices(sK15)
| ~ l3_lattices(sK15)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_1
| ~ spl237_7
| ~ spl237_8 ),
inference(forward_subsumption_resolution,[],[f6408,f6301]) ).
fof(f6412,plain,
( ! [X0] :
( ~ l3_lattices(sK15)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_1
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(forward_subsumption_resolution,[],[f6410,f6297]) ).
fof(f6414,plain,
( ! [X0] :
( ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_1
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(forward_subsumption_resolution,[],[f6412,f4414]) ).
fof(f6416,plain,
( ! [X0] : ~ m1_subset_1(X0,u1_struct_0(sK15))
| spl237_1
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(forward_subsumption_resolution,[],[f6414,f4418]) ).
fof(f6417,plain,
( ! [X0] :
( v3_struct_0(sK15)
| ~ v6_lattices(sK15)
| ~ v8_lattices(sK15)
| ~ v9_lattices(sK15)
| ~ l3_lattices(sK15)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_2 ),
inference(resolution,[],[f6358,f4626]) ).
fof(f6431,plain,
( $false
| spl237_1
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(resolution,[],[f6416,f4417]) ).
fof(f6501,plain,
( spl237_1
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(avatar_contradiction_clause,[],[f6431]) ).
fof(f6638,plain,
( ! [X0] :
( ~ v6_lattices(sK15)
| ~ v8_lattices(sK15)
| ~ v9_lattices(sK15)
| ~ l3_lattices(sK15)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_2 ),
inference(forward_subsumption_resolution,[],[f6417,f4416]) ).
fof(f6640,plain,
( ! [X0] :
( ~ v8_lattices(sK15)
| ~ v9_lattices(sK15)
| ~ l3_lattices(sK15)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_2
| ~ spl237_8 ),
inference(forward_subsumption_resolution,[],[f6638,f6305]) ).
fof(f6642,plain,
( ! [X0] :
( ~ v9_lattices(sK15)
| ~ l3_lattices(sK15)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_2
| ~ spl237_7
| ~ spl237_8 ),
inference(forward_subsumption_resolution,[],[f6640,f6301]) ).
fof(f6644,plain,
( ! [X0] :
( ~ l3_lattices(sK15)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_2
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(forward_subsumption_resolution,[],[f6642,f6297]) ).
fof(f6646,plain,
( ! [X0] :
( ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl237_2
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(forward_subsumption_resolution,[],[f6644,f4414]) ).
fof(f6648,plain,
( ! [X0] : ~ m1_subset_1(X0,u1_struct_0(sK15))
| spl237_2
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(forward_subsumption_resolution,[],[f6646,f4417]) ).
fof(f6788,plain,
( $false
| spl237_2
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(resolution,[],[f6648,f4417]) ).
fof(f6858,plain,
( spl237_2
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(avatar_contradiction_clause,[],[f6788]) ).
cnf(s1,plain,
( ~ spl237_1
| ~ spl237_2 ),
inference(sat_conversion,[],[f6257]) ).
cnf(s7,plain,
spl237_6,
inference(sat_conversion,[],[f6321]) ).
cnf(s10,plain,
spl237_7,
inference(sat_conversion,[],[f6368]) ).
cnf(s12,plain,
spl237_8,
inference(sat_conversion,[],[f6378]) ).
cnf(s16,plain,
( spl237_1
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(sat_conversion,[],[f6501]) ).
cnf(s29,plain,
( spl237_2
| ~ spl237_6
| ~ spl237_7
| ~ spl237_8 ),
inference(sat_conversion,[],[f6858]) ).
cnf(s34,plain,
spl237_2,
inference(rat,[],[s29,s12,s10,s7]) ).
cnf(s35,plain,
spl237_1,
inference(rat,[],[s16,s12,s10,s7]) ).
cnf(s37,plain,
$false,
inference(rat,[],[s1,s34,s35]) ).
fof(f6962,plain,
$false,
inference(avatar_sat_refutation,[],[s37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT327+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 % Computer : n005.cluster.edu
% 0.11/0.40 % Model : x86_64 x86_64
% 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40 % Memory : 8046.5625MB
% 0.11/0.40 % OS : Linux 6.8.0-71-generic
% 0.11/0.40 % CPULimit : 300
% 0.11/0.40 % WCLimit : 300
% 0.11/0.40 % DateTime : Sun Sep 27 14:39:33 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.44 Running first-order theorem proving
% 0.11/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
% 3.05/1.89 % (4060118)Detected formulas, will run a generic FOF schedule.
% 3.05/1.89 % (4060127)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4240075218:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 3.05/1.89 % (4060125)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=7758992:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 3.05/1.89 % (4060124)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=4264443236:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 3.05/1.89 % (4060123)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=2308046965:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 3.05/1.89 % (4060127)Instruction limit reached!
% 3.05/1.89 % (4060127)------------------------------
% 3.05/1.89 % (4060127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.89 % (4060127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.89 % (4060127)CaDiCaL version: 2.1.3
% 3.05/1.89 % (4060127)Termination reason: Instruction limit
% 3.05/1.89 % (4060127)Termination phase: Saturation
% 3.05/1.89 % (4060127)Time elapsed: 0.044 s
% 3.05/1.89 % (4060127)Peak memory usage: 92 MB
% 3.05/1.89 % (4060127)Instructions burned: 121 (million)
% 3.05/1.89 % (4060126)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=808906106:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 3.05/1.89 % (4060129)dis-21_1_sil=8000:lcm=predicate:random_seed=65812246:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 3.05/1.89 % (4060128)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2940732679:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 3.05/1.89 % (4060126)Refutation not found, incomplete strategy
% 3.05/1.89 % (4060126)------------------------------
% 3.05/1.89 % (4060126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.89 % (4060126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.89 % (4060126)CaDiCaL version: 2.1.3
% 3.05/1.89 % (4060126)Termination reason: Refutation not found, incomplete strategy
% 3.05/1.89 % (4060126)Time elapsed: 0.015 s
% 3.05/1.89 % (4060126)Peak memory usage: 92 MB
% 3.05/1.89 % (4060126)Instructions burned: 18 (million)
% 3.05/1.89 % (4060134)lrs+10_1_sil=8000:sp=occurrence:random_seed=317173224:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.05/1.89 % (4060129)Instruction limit reached!
% 3.05/1.89 % (4060129)------------------------------
% 3.05/1.89 % (4060129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.89 % (4060129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.89 % (4060129)CaDiCaL version: 2.1.3
% 3.05/1.89 % (4060129)Termination reason: Instruction limit
% 3.05/1.89 % (4060129)Termination phase: Property scanning
% 3.05/1.89 % (4060129)Time elapsed: 0.082 s
% 3.05/1.89 % (4060129)Peak memory usage: 93 MB
% 3.05/1.89 % (4060129)Instructions burned: 131 (million)
% 3.05/1.89 % (4060128)Instruction limit reached!
% 3.05/1.89 % (4060128)------------------------------
% 3.05/1.89 % (4060128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.89 % (4060128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.89 % (4060128)CaDiCaL version: 2.1.3
% 3.05/1.89 % (4060128)Termination reason: Instruction limit
% 3.05/1.89 % (4060128)Termination phase: Clausification
% 3.05/1.89 % (4060128)Time elapsed: 0.089 s
% 3.05/1.89 % (4060128)Peak memory usage: 94 MB
% 3.05/1.89 % (4060128)Instructions burned: 139 (million)
% 3.05/1.89 % (4060134)Instruction limit reached!
% 3.05/1.89 % (4060134)------------------------------
% 3.05/1.89 % (4060134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.89 % (4060134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.89 % (4060134)CaDiCaL version: 2.1.3
% 3.05/1.89 % (4060134)Termination reason: Instruction limit
% 3.05/1.89 % (4060134)Termination phase: Saturation
% 3.05/1.89 % (4060134)Time elapsed: 0.089 s
% 3.05/1.89 % (4060134)Peak memory usage: 94 MB
% 3.05/1.89 % (4060134)Instructions burned: 286 (million)
% 3.05/1.89 % (4060139)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3076352305:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 3.05/1.89 % (4060140)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2354971578:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 3.05/1.89 % (4060139)Refutation not found, incomplete strategy
% 3.05/1.89 % (4060139)------------------------------
% 3.05/1.89 % (4060139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.89 % (4060139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.89 % (4060139)CaDiCaL version: 2.1.3
% 3.05/1.89 % (4060139)Termination reason: Refutation not found, incomplete strategy
% 3.05/1.89 % (4060139)Time elapsed: 0.028 s
% 3.05/1.89 % (4060139)Peak memory usage: 92 MB
% 3.05/1.89 % (4060139)Instructions burned: 49 (million)
% 3.05/1.89 % (4060126)------------------------------
% 3.05/1.89 % (4060126)------------------------------
% 3.05/1.89 % (4060141)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=2690554888:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 3.05/1.89 % (4060141)Instruction limit reached!
% 3.05/1.89 % (4060141)------------------------------
% 3.05/1.89 % (4060141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.89 % (4060141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.89 % (4060141)CaDiCaL version: 2.1.3
% 3.05/1.89 % (4060141)Termination reason: Instruction limit
% 3.05/1.89 % (4060141)Termination phase: Saturation
% 3.05/1.89 % (4060141)Time elapsed: 0.077 s
% 3.05/1.89 % (4060141)Peak memory usage: 98 MB
% 3.05/1.89 % (4060141)Instructions burned: 249 (million)
% 3.05/1.89 % (4060145)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2241566798:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 3.05/1.89 % (4060146)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=203709326:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 3.05/1.89 % (4060140)Instruction limit reached!
% 3.05/1.89 % (4060140)------------------------------
% 3.05/1.89 % (4060140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.89 % (4060140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.89 % (4060140)CaDiCaL version: 2.1.3
% 3.05/1.89 % (4060140)Termination reason: Instruction limit
% 3.05/1.89 % (4060140)Termination phase: Saturation
% 3.05/1.89 % (4060140)Time elapsed: 0.208 s
% 3.05/1.89 % (4060140)Peak memory usage: 94 MB
% 3.05/1.89 % (4060140)Instructions burned: 325 (million)
% 3.05/1.89 % (4060139)------------------------------
% 3.05/1.89 % (4060139)------------------------------
% 3.05/1.89 % (4060145)First to succeed.
% 3.05/1.89 % (4060145)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4060118"
% 3.05/1.89 % (4060149)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2492435491:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 3.05/1.89 % (4060150)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4047540523:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 3.05/1.89 % (4060149)Instruction limit reached!
% 3.05/1.89 % (4060149)------------------------------
% 3.05/1.89 % (4060149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.89 % (4060149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.89 % (4060149)CaDiCaL version: 2.1.3
% 3.05/1.89 % (4060149)Termination reason: Instruction limit
% 3.05/1.89 % (4060149)Termination phase: Saturation
% 3.05/1.89 % (4060149)Time elapsed: 0.066 s
% 3.05/1.89 % (4060149)Peak memory usage: 93 MB
% 3.05/1.89 % (4060149)Instructions burned: 114 (million)
% 3.05/1.89 % (4060150)Instruction limit reached!
% 3.05/1.89 % (4060150)------------------------------
% 3.05/1.89 % (4060150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.89 % (4060150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.89 % (4060150)CaDiCaL version: 2.1.3
% 3.05/1.89 % (4060150)Termination reason: Instruction limit
% 3.05/1.89 % (4060150)Termination phase: Property scanning
% 3.05/1.89 % (4060150)Time elapsed: 0.077 s
% 3.05/1.89 % (4060150)Peak memory usage: 94 MB
% 3.05/1.89 % (4060150)Instructions burned: 129 (million)
% 3.05/1.89 % (4060145)Refutation found. Thanks to Tanya!
% 3.05/1.89 % SZS status Theorem for theBenchmark
% 3.05/1.89 % SZS output start Proof for theBenchmark
% See solution above
% 7.09/2.08 % (4060145)------------------------------
% 7.09/2.08 % (4060145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.09/2.08 % (4060145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.09/2.08 % (4060145)CaDiCaL version: 2.1.3
% 7.09/2.08 % (4060145)Termination reason: Refutation
% 7.09/2.08 % (4060145)Time elapsed: 0.088 s
% 7.09/2.08 % (4060145)Peak memory usage: 95 MB
% 7.09/2.08 % (4060145)Instructions burned: 149 (million)
% 7.09/2.08 % (4060145)------------------------------
% 7.09/2.08 % (4060145)------------------------------
% 7.09/2.08 % (4060118)Success in time 1.011 s
% 7.09/2.08 % Vampire exiting
%------------------------------------------------------------------------------