%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT301+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 11:46:41 AM UTC 2026
% Result : Theorem 7.22s 2.40s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 18
% Syntax : Number of formulae : 120 ( 22 unt; 9 def)
% Number of atoms : 484 ( 10 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 590 ( 226 ~; 254 |; 75 &)
% ( 18 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 10 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 72 ( 0 sgn 68 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8585,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> r2_hidden(k6_lattices(X0),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_filter_0) ).
fof(f9358,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f9363,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f9438,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_lattice2) ).
fof(f9453,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0) )
=> k5_lattices(X0) = k6_lattices(k1_lattice2(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t78_lattice2) ).
fof(f9463,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f13531,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f13600,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f13608,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v13_lattices(X0)
=> r2_hidden(k5_lattices(X0),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_filter_2) ).
fof(f13609,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v13_lattices(X0)
=> r2_hidden(k5_lattices(X0),X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f13608]) ).
fof(f13633,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
inference(pure_predicate_removal,[],[f9363]) ).
fof(f13694,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13531]) ).
fof(f13695,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13694]) ).
fof(f13819,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13600]) ).
fof(f13820,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13819]) ).
fof(f13835,plain,
? [X0] :
( ? [X1] :
( ~ r2_hidden(k5_lattices(X0),X1)
& v13_lattices(X0)
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f13609]) ).
fof(f13836,plain,
? [X0] :
( ? [X1] :
( ~ r2_hidden(k5_lattices(X0),X1)
& v13_lattices(X0)
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f13835]) ).
fof(f13943,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9438]) ).
fof(f13944,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13943]) ).
fof(f13964,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f13967,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13633]) ).
fof(f13968,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13967]) ).
fof(f13969,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9358]) ).
fof(f13970,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13969]) ).
fof(f14077,plain,
! [X0] :
( k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9453]) ).
fof(f14078,plain,
! [X0] :
( k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14077]) ).
fof(f14087,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8585]) ).
fof(f14088,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14087]) ).
fof(f14166,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0) )
& ( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13695]) ).
fof(f14186,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
| ~ m1_filter_2(X1,k1_lattice2(X0)) )
& ( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13820]) ).
fof(f14192,plain,
( ~ r2_hidden(k5_lattices(sK16),sK17)
& v13_lattices(sK16)
& m2_filter_2(sK17,sK16)
& ~ v3_struct_0(sK16)
& v10_lattices(sK16)
& l3_lattices(sK16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X0,sK16),skolemize(X1,sK17)],[f13836]) ).
fof(f14225,plain,
! [X0] :
( ( ( v13_lattices(X0)
| ~ v14_lattices(k1_lattice2(X0)) )
& ( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13944]) ).
fof(f14299,plain,
! [X0,X1] :
( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14166]) ).
fof(f14402,plain,
! [X0,X1] :
( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14186]) ).
fof(f14439,plain,
l3_lattices(sK16),
inference(cnf_transformation,[],[f14192]) ).
fof(f14440,plain,
v10_lattices(sK16),
inference(cnf_transformation,[],[f14192]) ).
fof(f14441,plain,
~ v3_struct_0(sK16),
inference(cnf_transformation,[],[f14192]) ).
fof(f14442,plain,
m2_filter_2(sK17,sK16),
inference(cnf_transformation,[],[f14192]) ).
fof(f14443,plain,
v13_lattices(sK16),
inference(cnf_transformation,[],[f14192]) ).
fof(f14444,plain,
~ r2_hidden(k5_lattices(sK16),sK17),
inference(cnf_transformation,[],[f14192]) ).
fof(f14554,plain,
! [X0] :
( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14225]) ).
fof(f14582,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13964]) ).
fof(f14585,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13968]) ).
fof(f14594,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13970]) ).
fof(f14730,plain,
! [X0] :
( k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14078]) ).
fof(f14737,plain,
! [X0,X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14088]) ).
fof(f15018,plain,
! [X0,X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(duplicate_literal_removal,[],[f14737]) ).
fof(f15032,definition,
( spl109_1
<=> v3_struct_0(sK16) ),
introduced(definition,[new_symbols(definition,[spl109_1])],[avatar_definition]) ).
fof(f15034,plain,
( ~ v3_struct_0(sK16)
| spl109_1 ),
inference(avatar_component_clause,[],[f15032]) ).
fof(f15035,plain,
~ spl109_1,
inference(avatar_split_clause,[],[f14441,f15032]) ).
fof(f15037,definition,
( spl109_2
<=> r2_hidden(k5_lattices(sK16),sK17) ),
introduced(definition,[new_symbols(definition,[spl109_2])],[avatar_definition]) ).
fof(f15039,plain,
( ~ r2_hidden(k5_lattices(sK16),sK17)
| spl109_2 ),
inference(avatar_component_clause,[],[f15037]) ).
fof(f15040,plain,
~ spl109_2,
inference(avatar_split_clause,[],[f14444,f15037]) ).
fof(f15093,definition,
( spl109_3
<=> v13_lattices(sK16) ),
introduced(definition,[new_symbols(definition,[spl109_3])],[avatar_definition]) ).
fof(f15095,plain,
( v13_lattices(sK16)
| ~ spl109_3 ),
inference(avatar_component_clause,[],[f15093]) ).
fof(f15096,plain,
spl109_3,
inference(avatar_split_clause,[],[f14443,f15093]) ).
fof(f15098,definition,
( spl109_4
<=> l3_lattices(sK16) ),
introduced(definition,[new_symbols(definition,[spl109_4])],[avatar_definition]) ).
fof(f15100,plain,
( l3_lattices(sK16)
| ~ spl109_4 ),
inference(avatar_component_clause,[],[f15098]) ).
fof(f15101,plain,
spl109_4,
inference(avatar_split_clause,[],[f14439,f15098]) ).
fof(f15289,plain,
( v14_lattices(k1_lattice2(sK16))
| ~ v13_lattices(sK16)
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_1 ),
inference(resolution,[],[f15034,f14554]) ).
fof(f15317,plain,
( v10_lattices(k1_lattice2(sK16))
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_1 ),
inference(resolution,[],[f15034,f14585]) ).
fof(f15326,plain,
( ~ v3_struct_0(k1_lattice2(sK16))
| ~ l3_lattices(sK16)
| spl109_1 ),
inference(resolution,[],[f15034,f14594]) ).
fof(f15386,plain,
( k5_lattices(sK16) = k6_lattices(k1_lattice2(sK16))
| ~ v10_lattices(sK16)
| ~ v13_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_1 ),
inference(resolution,[],[f15034,f14730]) ).
fof(f15767,plain,
( k5_lattices(sK16) = k6_lattices(k1_lattice2(sK16))
| ~ v13_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_1 ),
inference(forward_subsumption_resolution,[],[f15386,f14440]) ).
fof(f15814,plain,
( ~ v3_struct_0(k1_lattice2(sK16))
| spl109_1
| ~ spl109_4 ),
inference(forward_subsumption_resolution,[],[f15326,f15100]) ).
fof(f15821,plain,
( v10_lattices(k1_lattice2(sK16))
| ~ l3_lattices(sK16)
| spl109_1 ),
inference(forward_subsumption_resolution,[],[f15317,f14440]) ).
fof(f15848,plain,
( v14_lattices(k1_lattice2(sK16))
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_1
| ~ spl109_3 ),
inference(forward_subsumption_resolution,[],[f15289,f15095]) ).
fof(f16186,plain,
( k5_lattices(sK16) = k6_lattices(k1_lattice2(sK16))
| ~ l3_lattices(sK16)
| spl109_1
| ~ spl109_3 ),
inference(forward_subsumption_resolution,[],[f15767,f15095]) ).
fof(f16209,plain,
( v10_lattices(k1_lattice2(sK16))
| spl109_1
| ~ spl109_4 ),
inference(forward_subsumption_resolution,[],[f15821,f15100]) ).
fof(f16232,plain,
( v14_lattices(k1_lattice2(sK16))
| ~ l3_lattices(sK16)
| spl109_1
| ~ spl109_3 ),
inference(forward_subsumption_resolution,[],[f15848,f14440]) ).
fof(f16454,plain,
( k5_lattices(sK16) = k6_lattices(k1_lattice2(sK16))
| spl109_1
| ~ spl109_3
| ~ spl109_4 ),
inference(forward_subsumption_resolution,[],[f16186,f15100]) ).
fof(f16459,plain,
( v14_lattices(k1_lattice2(sK16))
| spl109_1
| ~ spl109_3
| ~ spl109_4 ),
inference(forward_subsumption_resolution,[],[f16232,f15100]) ).
fof(f16551,definition,
( spl109_5
<=> m2_filter_2(sK17,sK16) ),
introduced(definition,[new_symbols(definition,[spl109_5])],[avatar_definition]) ).
fof(f16553,plain,
( m2_filter_2(sK17,sK16)
| ~ spl109_5 ),
inference(avatar_component_clause,[],[f16551]) ).
fof(f16554,plain,
spl109_5,
inference(avatar_split_clause,[],[f14442,f16551]) ).
fof(f16567,plain,
( m1_filter_2(sK17,k1_lattice2(sK16))
| v3_struct_0(sK16)
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| ~ spl109_5 ),
inference(resolution,[],[f16553,f14402]) ).
fof(f16580,plain,
( m1_filter_2(sK17,k1_lattice2(sK16))
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_1
| ~ spl109_5 ),
inference(forward_subsumption_resolution,[],[f16567,f15034]) ).
fof(f16598,plain,
( m1_filter_2(sK17,k1_lattice2(sK16))
| ~ l3_lattices(sK16)
| spl109_1
| ~ spl109_5 ),
inference(forward_subsumption_resolution,[],[f16580,f14440]) ).
fof(f16616,plain,
( m1_filter_2(sK17,k1_lattice2(sK16))
| spl109_1
| ~ spl109_4
| ~ spl109_5 ),
inference(forward_subsumption_resolution,[],[f16598,f15100]) ).
fof(f17407,plain,
( l3_lattices(k1_lattice2(sK16))
| ~ spl109_4 ),
inference(resolution,[],[f15100,f14582]) ).
fof(f18028,definition,
( spl109_9
<=> k5_lattices(sK16) = k6_lattices(k1_lattice2(sK16)) ),
introduced(definition,[new_symbols(definition,[spl109_9])],[avatar_definition]) ).
fof(f18030,plain,
( k5_lattices(sK16) = k6_lattices(k1_lattice2(sK16))
| ~ spl109_9 ),
inference(avatar_component_clause,[],[f18028]) ).
fof(f18031,plain,
( spl109_9
| spl109_1
| ~ spl109_3
| ~ spl109_4 ),
inference(avatar_split_clause,[],[f16454,f15098,f15093,f15032,f18028]) ).
fof(f18051,plain,
( ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| v3_struct_0(k1_lattice2(sK16))
| ~ v10_lattices(k1_lattice2(sK16))
| ~ v14_lattices(k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16))
| ~ m1_filter_0(X0,k1_lattice2(sK16)) )
| ~ spl109_9 ),
inference(superposition,[],[f15018,f18030]) ).
fof(f18052,plain,
( ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| ~ v10_lattices(k1_lattice2(sK16))
| ~ v14_lattices(k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16))
| ~ m1_filter_0(X0,k1_lattice2(sK16)) )
| spl109_1
| ~ spl109_4
| ~ spl109_9 ),
inference(forward_subsumption_resolution,[],[f18051,f15814]) ).
fof(f18072,plain,
( ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| ~ v14_lattices(k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16))
| ~ m1_filter_0(X0,k1_lattice2(sK16)) )
| spl109_1
| ~ spl109_4
| ~ spl109_9 ),
inference(forward_subsumption_resolution,[],[f18052,f16209]) ).
fof(f18092,plain,
( ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| ~ l3_lattices(k1_lattice2(sK16))
| ~ m1_filter_0(X0,k1_lattice2(sK16)) )
| spl109_1
| ~ spl109_3
| ~ spl109_4
| ~ spl109_9 ),
inference(forward_subsumption_resolution,[],[f18072,f16459]) ).
fof(f18110,plain,
( ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK16)) )
| spl109_1
| ~ spl109_3
| ~ spl109_4
| ~ spl109_9 ),
inference(forward_subsumption_resolution,[],[f18092,f17407]) ).
fof(f18156,definition,
( spl109_10
<=> ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK16)) ) ),
introduced(definition,[new_symbols(definition,[spl109_10])],[avatar_definition]) ).
fof(f18157,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK16))
| r2_hidden(k5_lattices(sK16),X0) )
| ~ spl109_10 ),
inference(avatar_component_clause,[],[f18156]) ).
fof(f18158,plain,
( spl109_10
| spl109_1
| ~ spl109_3
| ~ spl109_4
| ~ spl109_9 ),
inference(avatar_split_clause,[],[f18110,f18028,f15098,f15093,f15032,f18156]) ).
fof(f18159,plain,
( ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| ~ m1_filter_2(X0,k1_lattice2(sK16))
| v3_struct_0(k1_lattice2(sK16))
| ~ v10_lattices(k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16)) )
| ~ spl109_10 ),
inference(resolution,[],[f18157,f14299]) ).
fof(f18240,plain,
( ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| ~ m1_filter_2(X0,k1_lattice2(sK16))
| ~ v10_lattices(k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16)) )
| spl109_1
| ~ spl109_4
| ~ spl109_10 ),
inference(forward_subsumption_resolution,[],[f18159,f15814]) ).
fof(f18281,plain,
( ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| ~ m1_filter_2(X0,k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16)) )
| spl109_1
| ~ spl109_4
| ~ spl109_10 ),
inference(forward_subsumption_resolution,[],[f18240,f16209]) ).
fof(f18320,plain,
( ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| ~ m1_filter_2(X0,k1_lattice2(sK16)) )
| spl109_1
| ~ spl109_4
| ~ spl109_10 ),
inference(forward_subsumption_resolution,[],[f18281,f17407]) ).
fof(f18392,definition,
( spl109_11
<=> m1_filter_2(sK17,k1_lattice2(sK16)) ),
introduced(definition,[new_symbols(definition,[spl109_11])],[avatar_definition]) ).
fof(f18394,plain,
( m1_filter_2(sK17,k1_lattice2(sK16))
| ~ spl109_11 ),
inference(avatar_component_clause,[],[f18392]) ).
fof(f18395,plain,
( spl109_11
| spl109_1
| ~ spl109_4
| ~ spl109_5 ),
inference(avatar_split_clause,[],[f16616,f16551,f15098,f15032,f18392]) ).
fof(f18463,definition,
( spl109_13
<=> ! [X0] :
( r2_hidden(k5_lattices(sK16),X0)
| ~ m1_filter_2(X0,k1_lattice2(sK16)) ) ),
introduced(definition,[new_symbols(definition,[spl109_13])],[avatar_definition]) ).
fof(f18464,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK16))
| r2_hidden(k5_lattices(sK16),X0) )
| ~ spl109_13 ),
inference(avatar_component_clause,[],[f18463]) ).
fof(f18465,plain,
( spl109_13
| spl109_1
| ~ spl109_4
| ~ spl109_10 ),
inference(avatar_split_clause,[],[f18320,f18156,f15098,f15032,f18463]) ).
fof(f18476,plain,
( r2_hidden(k5_lattices(sK16),sK17)
| ~ spl109_11
| ~ spl109_13 ),
inference(resolution,[],[f18464,f18394]) ).
fof(f18481,plain,
( $false
| spl109_2
| ~ spl109_11
| ~ spl109_13 ),
inference(forward_subsumption_resolution,[],[f18476,f15039]) ).
fof(f18482,plain,
( spl109_2
| ~ spl109_11
| ~ spl109_13 ),
inference(avatar_contradiction_clause,[],[f18481]) ).
cnf(s1,plain,
~ spl109_1,
inference(sat_conversion,[],[f15035]) ).
cnf(s2,plain,
~ spl109_2,
inference(sat_conversion,[],[f15040]) ).
cnf(s3,plain,
spl109_3,
inference(sat_conversion,[],[f15096]) ).
cnf(s4,plain,
spl109_4,
inference(sat_conversion,[],[f15101]) ).
cnf(s5,plain,
spl109_5,
inference(sat_conversion,[],[f16554]) ).
cnf(s9,plain,
( spl109_1
| ~ spl109_3
| ~ spl109_4
| spl109_9 ),
inference(sat_conversion,[],[f18031]) ).
cnf(s10,plain,
( spl109_1
| ~ spl109_3
| ~ spl109_4
| ~ spl109_9
| spl109_10 ),
inference(sat_conversion,[],[f18158]) ).
cnf(s11,plain,
( spl109_1
| ~ spl109_4
| ~ spl109_5
| spl109_11 ),
inference(sat_conversion,[],[f18395]) ).
cnf(s13,plain,
( spl109_1
| ~ spl109_4
| ~ spl109_10
| spl109_13 ),
inference(sat_conversion,[],[f18465]) ).
cnf(s14,plain,
( spl109_2
| ~ spl109_11
| ~ spl109_13 ),
inference(sat_conversion,[],[f18482]) ).
cnf(s16,plain,
spl109_11,
inference(rat,[],[s11,s4,s5,s1]) ).
cnf(s17,plain,
spl109_9,
inference(rat,[],[s9,s3,s4,s1]) ).
cnf(s19,plain,
~ spl109_13,
inference(rat,[],[s14,s2,s16]) ).
cnf(s20,plain,
spl109_10,
inference(rat,[],[s10,s1,s3,s4,s17]) ).
cnf(s22,plain,
$false,
inference(rat,[],[s13,s1,s4,s19,s20]) ).
fof(f18518,plain,
$false,
inference(avatar_sat_refutation,[],[s22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT301+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/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.39 % DateTime : Sun Sep 27 14:23:17 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.78/2.40 % (2081992)Detected formulas, will run a generic FOF schedule.
% 5.78/2.40 % (2081999)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=4005888423:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 5.78/2.40 % (2082003)dis-21_1_sil=8000:lcm=predicate:random_seed=3107886054: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)
% 5.78/2.40 % (2081997)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=693041862:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 5.78/2.40 % (2081998)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=1132205712:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 5.78/2.40 % (2082002)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1489318451:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 5.78/2.40 % (2082001)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3077838301:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 5.78/2.40 % (2082000)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2622899018:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 5.78/2.40 % (2082002)Instruction limit reached!
% 5.78/2.40 % (2082002)------------------------------
% 5.78/2.40 % (2082002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.78/2.40 % (2082002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.78/2.40 % (2082002)CaDiCaL version: 2.1.3
% 5.78/2.40 % (2082002)Termination reason: Instruction limit
% 5.78/2.40 % (2082002)Termination phase: Property scanning
% 5.78/2.40 % (2082002)Time elapsed: 0.059 s
% 5.78/2.40 % (2082002)Peak memory usage: 102 MB
% 5.78/2.40 % (2082002)Instructions burned: 139 (million)
% 5.78/2.40 % (2082000)Refutation not found, incomplete strategy
% 5.78/2.40 % (2082000)------------------------------
% 5.78/2.40 % (2082000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.78/2.40 % (2082000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.78/2.40 % (2082000)CaDiCaL version: 2.1.3
% 5.78/2.40 % (2082000)Termination reason: Refutation not found, incomplete strategy
% 5.78/2.40 % (2082000)Time elapsed: 0.066 s
% 5.78/2.40 % (2082000)Peak memory usage: 107 MB
% 5.78/2.40 % (2082000)Instructions burned: 85 (million)
% 5.78/2.40 % (2082001)Instruction limit reached!
% 5.78/2.40 % (2082001)------------------------------
% 5.78/2.40 % (2082001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.78/2.40 % (2082001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.78/2.40 % (2082001)CaDiCaL version: 2.1.3
% 5.78/2.40 % (2082001)Termination reason: Instruction limit
% 5.78/2.40 % (2082001)Termination phase: Property scanning
% 5.78/2.40 % (2082001)Time elapsed: 0.089 s
% 5.78/2.40 % (2082001)Peak memory usage: 106 MB
% 5.78/2.40 % (2082001)Instructions burned: 121 (million)
% 5.78/2.40 % (2082003)Instruction limit reached!
% 5.78/2.40 % (2082003)------------------------------
% 5.78/2.40 % (2082003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.78/2.40 % (2082003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.78/2.40 % (2082003)CaDiCaL version: 2.1.3
% 5.78/2.40 % (2082003)Termination reason: Instruction limit
% 5.78/2.40 % (2082003)Termination phase: Preprocessing 1
% 5.78/2.40 % (2082003)Time elapsed: 0.094 s
% 5.78/2.40 % (2082003)Peak memory usage: 103 MB
% 5.78/2.40 % (2082003)Instructions burned: 129 (million)
% 5.78/2.40 % (2082011)lrs+10_1_sil=8000:sp=occurrence:random_seed=2578370764:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 5.78/2.40 % (2082012)lrs+10_1_sil=32000:urr=on:br=off:random_seed=897018502:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 5.78/2.40 % (2082013)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1204257032:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 5.78/2.40 % (2082012)Instruction limit reached!
% 5.78/2.40 % (2082012)------------------------------
% 5.78/2.40 % (2082012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.78/2.40 % (2082012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.78/2.40 % (2082012)CaDiCaL version: 2.1.3
% 5.78/2.40 % (2082012)Termination reason: Instruction limit
% 5.78/2.40 % (2082012)Termination phase: Property scanning
% 5.78/2.40 % (2082012)Time elapsed: 0.067 s
% 5.78/2.40 % (2082012)Peak memory usage: 102 MB
% 5.78/2.40 % (2082012)Instructions burned: 158 (million)
% 5.78/2.40 % (2082000)------------------------------
% 5.78/2.40 % (2082000)------------------------------
% 5.78/2.40 % (2082011)Instruction limit reached!
% 5.78/2.40 % (2082011)------------------------------
% 5.78/2.40 % (2082011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.78/2.40 % (2082011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.78/2.40 % (2082011)CaDiCaL version: 2.1.3
% 5.78/2.40 % (2082011)Termination reason: Instruction limit
% 5.78/2.40 % (2082011)Termination phase: Saturation
% 5.78/2.40 % (2082011)Time elapsed: 0.187 s
% 5.78/2.40 % (2082011)Peak memory usage: 109 MB
% 5.78/2.40 % (2082011)Instructions burned: 286 (million)
% 5.78/2.40 % (2082017)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=1702483591:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 5.78/2.40 % (2082018)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2181927976:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 5.78/2.40 % (2082013)Instruction limit reached!
% 5.78/2.40 % (2082013)------------------------------
% 5.78/2.40 % (2082013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.78/2.40 % (2082013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.78/2.40 % (2082013)CaDiCaL version: 2.1.3
% 5.78/2.40 % (2082013)Termination reason: Instruction limit
% 5.78/2.40 % (2082013)Termination phase: Saturation
% 5.78/2.40 % (2082013)Time elapsed: 0.240 s
% 5.78/2.40 % (2082013)Peak memory usage: 109 MB
% 5.78/2.40 % (2082013)Instructions burned: 325 (million)
% 5.78/2.40 % (2082020)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2731448548:i=2350_2987 on theBenchmark for (2987ds/2350Mi)
% 5.78/2.40 % (2082017)Instruction limit reached!
% 5.78/2.40 % (2082017)------------------------------
% 5.78/2.40 % (2082017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/2.40 % (2082017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/2.40 % (2082017)CaDiCaL version: 2.1.3
% 7.22/2.40 % (2082017)Termination reason: Instruction limit
% 7.22/2.40 % (2082017)Termination phase: SInE selection
% 7.22/2.40 % (2082017)Time elapsed: 0.125 s
% 7.22/2.40 % (2082017)Peak memory usage: 103 MB
% 7.22/2.40 % (2082017)Instructions burned: 248 (million)
% 7.22/2.40 % (2081999)First to succeed.
% 7.22/2.40 % (2081999)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2081992"
% 7.22/2.40 % (2082018)Refutation not found, incomplete strategy
% 7.22/2.40 % (2082018)------------------------------
% 7.22/2.40 % (2082018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/2.40 % (2082018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/2.40 % (2082018)CaDiCaL version: 2.1.3
% 7.22/2.40 % (2082018)Termination reason: Refutation not found, incomplete strategy
% 7.22/2.40 % (2082018)Time elapsed: 0.156 s
% 7.22/2.40 % (2082018)Peak memory usage: 110 MB
% 7.22/2.40 % (2082018)Instructions burned: 238 (million)
% 7.22/2.40 % (2082023)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=692455152:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 7.22/2.40 % (2082025)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3547761569:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 7.22/2.40 % (2081999)Refutation found. Thanks to Tanya!
% 7.22/2.40 % SZS status Theorem for theBenchmark
% 7.22/2.40 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/2.60 % (2081999)------------------------------
% 0.15/2.60 % (2081999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/2.60 % (2081999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/2.60 % (2081999)CaDiCaL version: 2.1.3
% 0.15/2.60 % (2081999)Termination reason: Refutation
% 0.15/2.60 % (2081999)Time elapsed: 0.590 s
% 0.15/2.60 % (2081999)Peak memory usage: 156 MB
% 0.15/2.60 % (2081999)Instructions burned: 1697 (million)
% 0.15/2.60 % (2081999)------------------------------
% 0.15/2.60 % (2081999)------------------------------
% 0.15/2.60 % (2081992)Success in time 1.534 s
% 0.15/2.60 % Vampire exiting
%------------------------------------------------------------------------------