%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT327+3 : 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 : n016.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 6.85s 2.59s
% Output : Refutation 8.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 10
% Syntax : Number of formulae : 109 ( 16 unt; 5 def)
% Number of atoms : 505 ( 0 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 690 ( 294 ~; 312 |; 59 &)
% ( 8 <=>; 17 =>; 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 : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 76 ( 0 sgn 70 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6650,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(f6747,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(f11649,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_lattice3) ).
fof(f13658,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(f13659,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(f13660,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)],[f13659]) ).
fof(f13721,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,[],[f13660]) ).
fof(f13722,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,[],[f13721]) ).
fof(f13820,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,[],[f6747]) ).
fof(f13821,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,[],[f13820]) ).
fof(f13830,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,[],[f13658]) ).
fof(f13831,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,[],[f13830]) ).
fof(f14242,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f11649]) ).
fof(f14243,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14242]) ).
fof(f14491,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,[],[f6650]) ).
fof(f14492,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,[],[f14491]) ).
fof(f14588,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)],[f13722]) ).
fof(f14649,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,[],[f13831]) ).
fof(f14650,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,[],[f14649]) ).
fof(f14896,plain,
l3_lattices(sK15),
inference(cnf_transformation,[],[f14588]) ).
fof(f14897,plain,
v10_lattices(sK15),
inference(cnf_transformation,[],[f14588]) ).
fof(f14898,plain,
~ v3_struct_0(sK15),
inference(cnf_transformation,[],[f14588]) ).
fof(f14899,plain,
m1_subset_1(sK16,u1_struct_0(sK15)),
inference(cnf_transformation,[],[f14588]) ).
fof(f14900,plain,
m1_subset_1(sK17,u1_struct_0(sK15)),
inference(cnf_transformation,[],[f14588]) ).
fof(f14901,plain,
r3_lattices(sK15,sK16,sK17),
inference(cnf_transformation,[],[f14588]) ).
fof(f14902,plain,
( ~ r2_hidden(sK16,k22_filter_2(sK15,sK16,sK17))
| ~ r2_hidden(sK17,k22_filter_2(sK15,sK16,sK17)) ),
inference(cnf_transformation,[],[f14588]) ).
fof(f15057,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,[],[f13821]) ).
fof(f15065,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,[],[f14650]) ).
fof(f15639,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14243]) ).
fof(f16128,plain,
! [X0] :
( v9_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14492]) ).
fof(f16129,plain,
! [X0] :
( v8_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14492]) ).
fof(f16131,plain,
! [X0] :
( v6_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14492]) ).
fof(f16517,definition,
( spl217_1
<=> r2_hidden(sK17,k22_filter_2(sK15,sK16,sK17)) ),
introduced(definition,[new_symbols(definition,[spl217_1])],[avatar_definition]) ).
fof(f16519,plain,
( ~ r2_hidden(sK17,k22_filter_2(sK15,sK16,sK17))
| spl217_1 ),
inference(avatar_component_clause,[],[f16517]) ).
fof(f16521,definition,
( spl217_2
<=> r2_hidden(sK16,k22_filter_2(sK15,sK16,sK17)) ),
introduced(definition,[new_symbols(definition,[spl217_2])],[avatar_definition]) ).
fof(f16523,plain,
( ~ r2_hidden(sK16,k22_filter_2(sK15,sK16,sK17))
| spl217_2 ),
inference(avatar_component_clause,[],[f16521]) ).
fof(f16524,plain,
( ~ spl217_1
| ~ spl217_2 ),
inference(avatar_split_clause,[],[f14902,f16521,f16517]) ).
fof(f16560,definition,
( spl217_6
<=> v9_lattices(sK15) ),
introduced(definition,[new_symbols(definition,[spl217_6])],[avatar_definition]) ).
fof(f16561,plain,
( v9_lattices(sK15)
| ~ spl217_6 ),
inference(avatar_component_clause,[],[f16560]) ).
fof(f16562,plain,
( ~ v9_lattices(sK15)
| spl217_6 ),
inference(avatar_component_clause,[],[f16560]) ).
fof(f16564,definition,
( spl217_7
<=> v8_lattices(sK15) ),
introduced(definition,[new_symbols(definition,[spl217_7])],[avatar_definition]) ).
fof(f16565,plain,
( v8_lattices(sK15)
| ~ spl217_7 ),
inference(avatar_component_clause,[],[f16564]) ).
fof(f16566,plain,
( ~ v8_lattices(sK15)
| spl217_7 ),
inference(avatar_component_clause,[],[f16564]) ).
fof(f16568,definition,
( spl217_8
<=> v6_lattices(sK15) ),
introduced(definition,[new_symbols(definition,[spl217_8])],[avatar_definition]) ).
fof(f16569,plain,
( v6_lattices(sK15)
| ~ spl217_8 ),
inference(avatar_component_clause,[],[f16568]) ).
fof(f16570,plain,
( ~ v6_lattices(sK15)
| spl217_8 ),
inference(avatar_component_clause,[],[f16568]) ).
fof(f16576,plain,
( v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_6 ),
inference(resolution,[],[f16562,f16128]) ).
fof(f16579,plain,
( ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_6 ),
inference(forward_subsumption_resolution,[],[f16576,f14898]) ).
fof(f16581,plain,
( ~ l3_lattices(sK15)
| spl217_6 ),
inference(forward_subsumption_resolution,[],[f16579,f14897]) ).
fof(f16584,plain,
( $false
| spl217_6 ),
inference(forward_subsumption_resolution,[],[f16581,f14896]) ).
fof(f16585,plain,
spl217_6,
inference(avatar_contradiction_clause,[],[f16584]) ).
fof(f16586,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)
| spl217_1 ),
inference(resolution,[],[f16519,f15065]) ).
fof(f16587,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)
| spl217_1 ),
inference(duplicate_literal_removal,[],[f16586]) ).
fof(f16588,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)
| spl217_1 ),
inference(forward_subsumption_resolution,[],[f16587,f14901]) ).
fof(f16589,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_1 ),
inference(forward_subsumption_resolution,[],[f16588,f14900]) ).
fof(f16590,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_1 ),
inference(forward_subsumption_resolution,[],[f16589,f14899]) ).
fof(f16591,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_1 ),
inference(forward_subsumption_resolution,[],[f16590,f14898]) ).
fof(f16592,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| ~ l3_lattices(sK15)
| spl217_1 ),
inference(forward_subsumption_resolution,[],[f16591,f14897]) ).
fof(f16593,plain,
( ~ r3_lattices(sK15,sK17,sK17)
| spl217_1 ),
inference(forward_subsumption_resolution,[],[f16592,f14896]) ).
fof(f16596,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)
| spl217_2 ),
inference(resolution,[],[f16523,f15065]) ).
fof(f16597,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)
| spl217_2 ),
inference(duplicate_literal_removal,[],[f16596]) ).
fof(f16598,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)
| spl217_2 ),
inference(forward_subsumption_resolution,[],[f16597,f14901]) ).
fof(f16599,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_2 ),
inference(forward_subsumption_resolution,[],[f16598,f14899]) ).
fof(f16600,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_2 ),
inference(forward_subsumption_resolution,[],[f16599,f14900]) ).
fof(f16601,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_2 ),
inference(forward_subsumption_resolution,[],[f16600,f14898]) ).
fof(f16602,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| ~ l3_lattices(sK15)
| spl217_2 ),
inference(forward_subsumption_resolution,[],[f16601,f14897]) ).
fof(f16603,plain,
( ~ r3_lattices(sK15,sK16,sK16)
| spl217_2 ),
inference(forward_subsumption_resolution,[],[f16602,f14896]) ).
fof(f16604,plain,
( v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_7 ),
inference(resolution,[],[f16566,f16129]) ).
fof(f16607,plain,
( ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_7 ),
inference(forward_subsumption_resolution,[],[f16604,f14898]) ).
fof(f16609,plain,
( ~ l3_lattices(sK15)
| spl217_7 ),
inference(forward_subsumption_resolution,[],[f16607,f14897]) ).
fof(f16612,plain,
( $false
| spl217_7 ),
inference(forward_subsumption_resolution,[],[f16609,f14896]) ).
fof(f16613,plain,
spl217_7,
inference(avatar_contradiction_clause,[],[f16612]) ).
fof(f16614,plain,
( v3_struct_0(sK15)
| ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_8 ),
inference(resolution,[],[f16570,f16131]) ).
fof(f16617,plain,
( ~ v10_lattices(sK15)
| ~ l3_lattices(sK15)
| spl217_8 ),
inference(forward_subsumption_resolution,[],[f16614,f14898]) ).
fof(f16619,plain,
( ~ l3_lattices(sK15)
| spl217_8 ),
inference(forward_subsumption_resolution,[],[f16617,f14897]) ).
fof(f16622,plain,
( $false
| spl217_8 ),
inference(forward_subsumption_resolution,[],[f16619,f14896]) ).
fof(f16623,plain,
spl217_8,
inference(avatar_contradiction_clause,[],[f16622]) ).
fof(f16636,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)) )
| spl217_1 ),
inference(resolution,[],[f16593,f15057]) ).
fof(f16640,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)) )
| spl217_1 ),
inference(forward_subsumption_resolution,[],[f16636,f14898]) ).
fof(f16642,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)) )
| spl217_1
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16640,f16569]) ).
fof(f16644,plain,
( ! [X0] :
( ~ v9_lattices(sK15)
| ~ l3_lattices(sK15)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl217_1
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16642,f16565]) ).
fof(f16646,plain,
( ! [X0] :
( ~ l3_lattices(sK15)
| ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl217_1
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16644,f16561]) ).
fof(f16648,plain,
( ! [X0] :
( ~ m1_subset_1(sK17,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl217_1
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16646,f14896]) ).
fof(f16650,plain,
( ! [X0] : ~ m1_subset_1(X0,u1_struct_0(sK15))
| spl217_1
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16648,f14900]) ).
fof(f16651,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)) )
| spl217_2 ),
inference(resolution,[],[f16603,f15057]) ).
fof(f16661,plain,
( v3_struct_0(sK15)
| ~ l3_lattices(sK15)
| spl217_1
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(resolution,[],[f16650,f15639]) ).
fof(f16780,plain,
( ~ l3_lattices(sK15)
| spl217_1
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16661,f14898]) ).
fof(f16816,plain,
( $false
| spl217_1
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16780,f14896]) ).
fof(f16817,plain,
( spl217_1
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(avatar_contradiction_clause,[],[f16816]) ).
fof(f16867,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)) )
| spl217_2 ),
inference(forward_subsumption_resolution,[],[f16651,f14898]) ).
fof(f16869,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)) )
| spl217_2
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16867,f16569]) ).
fof(f16871,plain,
( ! [X0] :
( ~ v9_lattices(sK15)
| ~ l3_lattices(sK15)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl217_2
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16869,f16565]) ).
fof(f16873,plain,
( ! [X0] :
( ~ l3_lattices(sK15)
| ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl217_2
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16871,f16561]) ).
fof(f16875,plain,
( ! [X0] :
( ~ m1_subset_1(sK16,u1_struct_0(sK15))
| ~ m1_subset_1(X0,u1_struct_0(sK15)) )
| spl217_2
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16873,f14896]) ).
fof(f16877,plain,
( ! [X0] : ~ m1_subset_1(X0,u1_struct_0(sK15))
| spl217_2
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16875,f14899]) ).
fof(f16895,plain,
( v3_struct_0(sK15)
| ~ l3_lattices(sK15)
| spl217_2
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(resolution,[],[f16877,f15639]) ).
fof(f17009,plain,
( ~ l3_lattices(sK15)
| spl217_2
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f16895,f14898]) ).
fof(f17040,plain,
( $false
| spl217_2
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(forward_subsumption_resolution,[],[f17009,f14896]) ).
fof(f17041,plain,
( spl217_2
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(avatar_contradiction_clause,[],[f17040]) ).
cnf(s1,plain,
( ~ spl217_1
| ~ spl217_2 ),
inference(sat_conversion,[],[f16524]) ).
cnf(s7,plain,
spl217_6,
inference(sat_conversion,[],[f16585]) ).
cnf(s9,plain,
spl217_7,
inference(sat_conversion,[],[f16613]) ).
cnf(s11,plain,
spl217_8,
inference(sat_conversion,[],[f16623]) ).
cnf(s15,plain,
( spl217_1
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(sat_conversion,[],[f16817]) ).
cnf(s23,plain,
( spl217_2
| ~ spl217_6
| ~ spl217_7
| ~ spl217_8 ),
inference(sat_conversion,[],[f17041]) ).
cnf(s24,plain,
spl217_2,
inference(rat,[],[s23,s11,s9,s7]) ).
cnf(s25,plain,
spl217_1,
inference(rat,[],[s15,s11,s9,s7]) ).
cnf(s27,plain,
$false,
inference(rat,[],[s1,s24,s25]) ).
fof(f17071,plain,
$false,
inference(avatar_sat_refutation,[],[s27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT327+3 : 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.38 % Computer : n016.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 14:44:34 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.85/2.59 % (2711169)Detected formulas, will run a generic FOF schedule.
% 6.85/2.59 % (2711179)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=938924770:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 6.85/2.59 % (2711179)Instruction limit reached!
% 6.85/2.59 % (2711179)------------------------------
% 6.85/2.59 % (2711179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711179)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711179)Termination reason: Instruction limit
% 6.85/2.59 % (2711179)Termination phase: Property scanning
% 6.85/2.59 % (2711179)Time elapsed: 0.033 s
% 6.85/2.59 % (2711179)Peak memory usage: 102 MB
% 6.85/2.59 % (2711179)Instructions burned: 140 (million)
% 6.85/2.59 % (2711176)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=2738064735:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 6.85/2.59 % (2711175)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=1497801131:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 6.85/2.59 % (2711174)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=2753044758:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 6.85/2.59 % (2711177)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=782638475:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 6.85/2.59 % (2711178)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2628709636:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 6.85/2.59 % (2711180)dis-21_1_sil=8000:lcm=predicate:random_seed=284879483:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 6.85/2.59 % (2711177)Refutation not found, incomplete strategy
% 6.85/2.59 % (2711177)------------------------------
% 6.85/2.59 % (2711177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711177)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711177)Termination reason: Refutation not found, incomplete strategy
% 6.85/2.59 % (2711177)Time elapsed: 0.069 s
% 6.85/2.59 % (2711177)Peak memory usage: 107 MB
% 6.85/2.59 % (2711177)Instructions burned: 80 (million)
% 6.85/2.59 % (2711178)Instruction limit reached!
% 6.85/2.59 % (2711178)------------------------------
% 6.85/2.59 % (2711178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711178)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711178)Termination reason: Instruction limit
% 6.85/2.59 % (2711178)Termination phase: Equality resolution with deletion
% 6.85/2.59 % (2711178)Time elapsed: 0.094 s
% 6.85/2.59 % (2711178)Peak memory usage: 105 MB
% 6.85/2.59 % (2711178)Instructions burned: 121 (million)
% 6.85/2.59 % (2711180)Instruction limit reached!
% 6.85/2.59 % (2711180)------------------------------
% 6.85/2.59 % (2711180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711180)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711180)Termination reason: Instruction limit
% 6.85/2.59 % (2711180)Termination phase: Preprocessing 1
% 6.85/2.59 % (2711180)Time elapsed: 0.097 s
% 6.85/2.59 % (2711180)Peak memory usage: 103 MB
% 6.85/2.59 % (2711180)Instructions burned: 129 (million)
% 6.85/2.59 % (2711182)lrs+10_1_sil=8000:sp=occurrence:random_seed=85927860:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 6.85/2.59 % (2711182)Instruction limit reached!
% 6.85/2.59 % (2711182)------------------------------
% 6.85/2.59 % (2711182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711182)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711182)Termination reason: Instruction limit
% 6.85/2.59 % (2711182)Termination phase: Saturation
% 6.85/2.59 % (2711182)Time elapsed: 0.091 s
% 6.85/2.59 % (2711182)Peak memory usage: 108 MB
% 6.85/2.59 % (2711182)Instructions burned: 286 (million)
% 6.85/2.59 % (2711189)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1150838242:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 6.85/2.59 % (2711190)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4061791720:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 6.85/2.59 % (2711177)------------------------------
% 6.85/2.59 % (2711177)------------------------------
% 6.85/2.59 % (2711192)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=434577115:s2a=on:i=248:s2at=1.23:gtg=position_2989 on theBenchmark for (2989ds/248Mi)
% 6.85/2.59 % (2711189)Instruction limit reached!
% 6.85/2.59 % (2711189)------------------------------
% 6.85/2.59 % (2711189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711189)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711189)Termination reason: Instruction limit
% 6.85/2.59 % (2711189)Termination phase: Property scanning
% 6.85/2.59 % (2711189)Time elapsed: 0.068 s
% 6.85/2.59 % (2711189)Peak memory usage: 102 MB
% 6.85/2.59 % (2711189)Instructions burned: 158 (million)
% 6.85/2.59 % (2711192)Instruction limit reached!
% 6.85/2.59 % (2711192)------------------------------
% 6.85/2.59 % (2711192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711192)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711192)Termination reason: Instruction limit
% 6.85/2.59 % (2711192)Termination phase: SInE selection
% 6.85/2.59 % (2711192)Time elapsed: 0.071 s
% 6.85/2.59 % (2711192)Peak memory usage: 103 MB
% 6.85/2.59 % (2711192)Instructions burned: 248 (million)
% 6.85/2.59 % (2711190)Instruction limit reached!
% 6.85/2.59 % (2711190)------------------------------
% 6.85/2.59 % (2711190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711190)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711190)Termination reason: Instruction limit
% 6.85/2.59 % (2711190)Termination phase: Saturation
% 6.85/2.59 % (2711190)Time elapsed: 0.169 s
% 6.85/2.59 % (2711190)Peak memory usage: 107 MB
% 6.85/2.59 % (2711190)Instructions burned: 326 (million)
% 6.85/2.59 % (2711195)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1877377346:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 6.85/2.59 % (2711197)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3094308100:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 6.85/2.59 % (2711198)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1241880398:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 6.85/2.59 % (2711198)Instruction limit reached!
% 6.85/2.59 % (2711198)------------------------------
% 6.85/2.59 % (2711198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711198)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711198)Termination reason: Instruction limit
% 6.85/2.59 % (2711198)Termination phase: Preprocessing 3
% 6.85/2.59 % (2711198)Time elapsed: 0.054 s
% 6.85/2.59 % (2711198)Peak memory usage: 105 MB
% 6.85/2.59 % (2711198)Instructions burned: 114 (million)
% 6.85/2.59 % (2711199)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=36962398:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 6.85/2.59 % (2711195)First to succeed.
% 6.85/2.59 % (2711195)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2711169"
% 6.85/2.59 % (2711199)Instruction limit reached!
% 6.85/2.59 % (2711199)------------------------------
% 6.85/2.59 % (2711199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711199)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711199)Termination reason: Instruction limit
% 6.85/2.59 % (2711199)Termination phase: Preprocessing 2
% 6.85/2.59 % (2711199)Time elapsed: 0.103 s
% 6.85/2.59 % (2711199)Peak memory usage: 106 MB
% 6.85/2.59 % (2711199)Instructions burned: 128 (million)
% 6.85/2.59 % (2711203)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2153337724:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 6.85/2.59 % (2711203)Instruction limit reached!
% 6.85/2.59 % (2711203)------------------------------
% 6.85/2.59 % (2711203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.59 % (2711203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.59 % (2711203)CaDiCaL version: 2.1.3
% 6.85/2.59 % (2711203)Termination reason: Instruction limit
% 6.85/2.59 % (2711203)Termination phase: Property scanning
% 6.85/2.59 % (2711203)Time elapsed: 0.027 s
% 6.85/2.59 % (2711203)Peak memory usage: 102 MB
% 6.85/2.59 % (2711203)Instructions burned: 116 (million)
% 6.85/2.59 % (2711206)lrs+10_1_sil=8000:sp=occurrence:random_seed=2555546785:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 6.85/2.59 % (2711207)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2877652469:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 6.85/2.59 % (2711195)Refutation found. Thanks to Tanya!
% 6.85/2.59 % SZS status Theorem for theBenchmark
% 6.85/2.59 % SZS output start Proof for theBenchmark
% See solution above
% 8.69/2.74 % (2711195)------------------------------
% 8.69/2.74 % (2711195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.74 % (2711195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.74 % (2711195)CaDiCaL version: 2.1.3
% 8.69/2.74 % (2711195)Termination reason: Refutation
% 8.69/2.74 % (2711195)Time elapsed: 0.142 s
% 8.69/2.74 % (2711195)Peak memory usage: 110 MB
% 8.69/2.74 % (2711195)Instructions burned: 205 (million)
% 8.69/2.74 % (2711195)------------------------------
% 8.69/2.74 % (2711195)------------------------------
% 8.69/2.74 % (2711169)Success in time 1.734 s
% 8.69/2.74 % Vampire exiting
%------------------------------------------------------------------------------