%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT319+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:48:23 AM UTC 2026
% Result : Theorem 0.16s 0.48s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 26
% Syntax : Number of formulae : 224 ( 22 unt; 17 def)
% Number of atoms : 1164 ( 0 equ)
% Maximal formula atoms : 19 ( 5 avg)
% Number of connectives : 1522 ( 582 ~; 674 |; 227 &)
% ( 24 <=>; 13 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 34 ( 33 usr; 15 prp; 0-1 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 64 ( 0 sgn 60 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_filter_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f10,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v13_lattices(X0)
& v14_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v15_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc3_lattices) ).
fof(f12,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc5_lattices) ).
fof(f13,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v17_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc6_lattices) ).
fof(f18,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(f39,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(f49,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(f73,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t53_filter_2) ).
fof(f75,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_lattice2) ).
fof(f93,plain,
? [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<~> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f94,plain,
? [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<~> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f93]) ).
fof(f106,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v15_lattices(X0) )
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f107,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v15_lattices(X0) )
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f106]) ).
fof(f110,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f111,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f110]) ).
fof(f112,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f113,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f112]) ).
fof(f121,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f128,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f129,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f128]) ).
fof(f144,plain,
! [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)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f49]) ).
fof(f145,plain,
! [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)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f144]) ).
fof(f157,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f73]) ).
fof(f158,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f157]) ).
fof(f160,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f75]) ).
fof(f161,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f160]) ).
fof(f165,definition,
! [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)) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f166,plain,
! [X0] :
( sP0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f145,f165]) ).
fof(f167,definition,
! [X0] :
( sP1(X0)
<=> ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f168,definition,
! [X0] :
( ( sP1(X0)
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| ~ sP2(X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f169,plain,
! [X0] :
( sP2(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f158,f168,f167]) ).
fof(f170,plain,
? [X0] :
( ( v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(nnf_transformation,[],[f94]) ).
fof(f171,plain,
? [X0] :
( ( v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f170]) ).
fof(f172,plain,
( ( v3_struct_0(k1_lattice2(sK3))
| ~ v10_lattices(k1_lattice2(sK3))
| ~ v17_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| v3_struct_0(sK3)
| ~ v10_lattices(sK3)
| ~ v17_lattices(sK3)
| ~ l3_lattices(sK3) )
& ( ( ~ v3_struct_0(k1_lattice2(sK3))
& v10_lattices(k1_lattice2(sK3))
& v17_lattices(k1_lattice2(sK3))
& l3_lattices(k1_lattice2(sK3)) )
| ( ~ v3_struct_0(sK3)
& v10_lattices(sK3)
& v17_lattices(sK3)
& l3_lattices(sK3) ) )
& ~ v3_struct_0(sK3)
& v10_lattices(sK3)
& l3_lattices(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3)],[f171]) ).
fof(f182,plain,
! [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)) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f165]) ).
fof(f200,plain,
! [X0] :
( ( ( sP1(X0)
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ sP1(X0) ) )
| ~ sP2(X0) ),
inference(nnf_transformation,[],[f168]) ).
fof(f201,plain,
! [X0] :
( ( ( sP1(X0)
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ sP1(X0) ) )
| ~ sP2(X0) ),
inference(flattening,[],[f200]) ).
fof(f202,plain,
! [X0] :
( ( sP1(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) )
& ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
| ~ sP1(X0) ) ),
inference(nnf_transformation,[],[f167]) ).
fof(f203,plain,
! [X0] :
( ( sP1(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) )
& ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
| ~ sP1(X0) ) ),
inference(flattening,[],[f202]) ).
fof(f204,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f161]) ).
fof(f205,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f204]) ).
fof(f206,plain,
l3_lattices(sK3),
inference(cnf_transformation,[],[f172]) ).
fof(f207,plain,
v10_lattices(sK3),
inference(cnf_transformation,[],[f172]) ).
fof(f208,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f172]) ).
fof(f214,plain,
( v17_lattices(k1_lattice2(sK3))
| v17_lattices(sK3) ),
inference(cnf_transformation,[],[f172]) ).
fof(f225,plain,
( v3_struct_0(k1_lattice2(sK3))
| ~ v10_lattices(k1_lattice2(sK3))
| ~ v17_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| v3_struct_0(sK3)
| ~ v10_lattices(sK3)
| ~ v17_lattices(sK3)
| ~ l3_lattices(sK3) ),
inference(cnf_transformation,[],[f172]) ).
fof(f241,plain,
! [X0] :
( ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| v15_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f107]) ).
fof(f246,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f247,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| v15_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f248,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f249,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f250,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f252,plain,
! [X0] :
( ~ v16_lattices(X0)
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f269,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f121]) ).
fof(f290,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f309,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f182]) ).
fof(f318,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f166]) ).
fof(f418,plain,
! [X0] :
( v16_lattices(k1_lattice2(X0))
| ~ sP1(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f201]) ).
fof(f419,plain,
! [X0] :
( v15_lattices(k1_lattice2(X0))
| ~ sP1(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f201]) ).
fof(f422,plain,
! [X0] :
( ~ v16_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| sP1(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f201]) ).
fof(f424,plain,
! [X0] :
( ~ sP1(X0)
| v16_lattices(X0) ),
inference(cnf_transformation,[],[f203]) ).
fof(f425,plain,
! [X0] :
( ~ sP1(X0)
| v15_lattices(X0) ),
inference(cnf_transformation,[],[f203]) ).
fof(f428,plain,
! [X0] :
( ~ v16_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| sP1(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f203]) ).
fof(f429,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| sP2(X0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f432,plain,
! [X0] :
( v11_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f205]) ).
fof(f436,plain,
! [X0] :
( v11_lattices(X0)
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f205]) ).
fof(f443,plain,
! [X0] :
( v11_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f432]) ).
fof(f447,definition,
( spl27_1
<=> l3_lattices(sK3) ),
introduced(definition,[new_symbols(definition,[spl27_1])],[avatar_definition]) ).
fof(f449,plain,
( l3_lattices(sK3)
| ~ spl27_1 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f451,definition,
( spl27_2
<=> l3_lattices(k1_lattice2(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_2])],[avatar_definition]) ).
fof(f452,plain,
( ~ l3_lattices(k1_lattice2(sK3))
| spl27_2 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f453,plain,
( l3_lattices(k1_lattice2(sK3))
| ~ spl27_2 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f456,definition,
( spl27_3
<=> v17_lattices(sK3) ),
introduced(definition,[new_symbols(definition,[spl27_3])],[avatar_definition]) ).
fof(f457,plain,
( ~ v17_lattices(sK3)
| spl27_3 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f458,plain,
( v17_lattices(sK3)
| ~ spl27_3 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f461,definition,
( spl27_4
<=> v10_lattices(sK3) ),
introduced(definition,[new_symbols(definition,[spl27_4])],[avatar_definition]) ).
fof(f463,plain,
( v10_lattices(sK3)
| ~ spl27_4 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f466,definition,
( spl27_5
<=> v3_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl27_5])],[avatar_definition]) ).
fof(f468,plain,
( ~ v3_struct_0(sK3)
| spl27_5 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f471,definition,
( spl27_6
<=> v17_lattices(k1_lattice2(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_6])],[avatar_definition]) ).
fof(f472,plain,
( ~ v17_lattices(k1_lattice2(sK3))
| spl27_6 ),
inference(avatar_component_clause,[],[f471]) ).
fof(f473,plain,
( v17_lattices(k1_lattice2(sK3))
| ~ spl27_6 ),
inference(avatar_component_clause,[],[f471]) ).
fof(f475,plain,
( spl27_3
| spl27_6 ),
inference(avatar_split_clause,[],[f214,f471,f456]) ).
fof(f479,definition,
( spl27_7
<=> v10_lattices(k1_lattice2(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_7])],[avatar_definition]) ).
fof(f480,plain,
( ~ v10_lattices(k1_lattice2(sK3))
| spl27_7 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f481,plain,
( v10_lattices(k1_lattice2(sK3))
| ~ spl27_7 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f487,definition,
( spl27_8
<=> v3_struct_0(k1_lattice2(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_8])],[avatar_definition]) ).
fof(f488,plain,
( v3_struct_0(k1_lattice2(sK3))
| ~ spl27_8 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f489,plain,
( ~ v3_struct_0(k1_lattice2(sK3))
| spl27_8 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f494,plain,
( ~ spl27_1
| ~ spl27_3
| ~ spl27_4
| spl27_5
| ~ spl27_2
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(avatar_split_clause,[],[f225,f487,f479,f471,f451,f466,f461,f456,f447]) ).
fof(f495,plain,
spl27_1,
inference(avatar_split_clause,[],[f206,f447]) ).
fof(f496,plain,
spl27_4,
inference(avatar_split_clause,[],[f207,f461]) ).
fof(f497,plain,
~ spl27_5,
inference(avatar_split_clause,[],[f208,f466]) ).
fof(f796,plain,
( v3_struct_0(k1_lattice2(sK3))
| v16_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| ~ spl27_6 ),
inference(resolution,[],[f246,f473]) ).
fof(f798,plain,
( v16_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| ~ spl27_6
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f796,f489]) ).
fof(f799,plain,
( v16_lattices(k1_lattice2(sK3))
| ~ spl27_2
| ~ spl27_6
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f798,f453]) ).
fof(f800,plain,
( v3_struct_0(k1_lattice2(sK3))
| v15_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| ~ spl27_6 ),
inference(resolution,[],[f247,f473]) ).
fof(f802,plain,
( v15_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| ~ spl27_6
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f800,f489]) ).
fof(f803,plain,
( v15_lattices(k1_lattice2(sK3))
| ~ spl27_2
| ~ spl27_6
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f802,f453]) ).
fof(f812,plain,
( v3_struct_0(k1_lattice2(sK3))
| v11_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| ~ spl27_6 ),
inference(resolution,[],[f250,f473]) ).
fof(f814,plain,
( v11_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| ~ spl27_6
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f812,f489]) ).
fof(f815,plain,
( v11_lattices(k1_lattice2(sK3))
| ~ spl27_2
| ~ spl27_6
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f814,f453]) ).
fof(f825,plain,
( v3_struct_0(sK3)
| ~ v10_lattices(sK3)
| sP0(sK3)
| ~ spl27_1 ),
inference(resolution,[],[f318,f449]) ).
fof(f850,plain,
( ~ v10_lattices(sK3)
| sP0(sK3)
| ~ spl27_1
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f825,f468]) ).
fof(f863,plain,
( sP0(sK3)
| ~ spl27_1
| ~ spl27_4
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f850,f463]) ).
fof(f878,plain,
( v3_struct_0(sK3)
| ~ v10_lattices(sK3)
| sP2(sK3)
| ~ spl27_1 ),
inference(resolution,[],[f429,f449]) ).
fof(f898,plain,
( ~ v10_lattices(sK3)
| sP2(sK3)
| ~ spl27_1
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f878,f468]) ).
fof(f911,plain,
( sP2(sK3)
| ~ spl27_1
| ~ spl27_4
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f898,f463]) ).
fof(f1072,plain,
( v3_struct_0(k1_lattice2(sK3))
| ~ v10_lattices(k1_lattice2(sK3))
| ~ v15_lattices(k1_lattice2(sK3))
| sP1(sK3)
| ~ l3_lattices(k1_lattice2(sK3))
| ~ sP2(sK3)
| ~ spl27_2
| ~ spl27_6
| spl27_8 ),
inference(resolution,[],[f422,f799]) ).
fof(f1074,plain,
( ~ v10_lattices(k1_lattice2(sK3))
| ~ v15_lattices(k1_lattice2(sK3))
| sP1(sK3)
| ~ l3_lattices(k1_lattice2(sK3))
| ~ sP2(sK3)
| ~ spl27_2
| ~ spl27_6
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1072,f489]) ).
fof(f1075,plain,
( ~ v15_lattices(k1_lattice2(sK3))
| sP1(sK3)
| ~ l3_lattices(k1_lattice2(sK3))
| ~ sP2(sK3)
| ~ spl27_2
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1074,f481]) ).
fof(f1076,plain,
( sP1(sK3)
| ~ l3_lattices(k1_lattice2(sK3))
| ~ sP2(sK3)
| ~ spl27_2
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1075,f803]) ).
fof(f1077,plain,
( sP1(sK3)
| ~ sP2(sK3)
| ~ spl27_2
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1076,f453]) ).
fof(f1078,plain,
( sP1(sK3)
| ~ spl27_1
| ~ spl27_2
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1077,f911]) ).
fof(f1081,plain,
( v15_lattices(sK3)
| ~ spl27_1
| ~ spl27_2
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(resolution,[],[f1078,f425]) ).
fof(f1082,plain,
( v16_lattices(sK3)
| ~ spl27_1
| ~ spl27_2
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(resolution,[],[f1078,f424]) ).
fof(f1084,plain,
! [X0] :
( v11_lattices(X0)
| ~ v10_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f436,f290]) ).
fof(f1085,plain,
! [X0] :
( ~ v11_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v11_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f1084,f269]) ).
fof(f1092,plain,
( ~ v10_lattices(k1_lattice2(sK3))
| v11_lattices(sK3)
| v3_struct_0(sK3)
| ~ v10_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_2
| ~ spl27_6
| spl27_8 ),
inference(resolution,[],[f1085,f815]) ).
fof(f1095,plain,
( v11_lattices(sK3)
| v3_struct_0(sK3)
| ~ v10_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_2
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1092,f481]) ).
fof(f1096,plain,
( v11_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_2
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1095,f468]) ).
fof(f1097,plain,
( v11_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_2
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1096,f463]) ).
fof(f1098,plain,
( v11_lattices(sK3)
| ~ spl27_1
| ~ spl27_2
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1097,f449]) ).
fof(f1101,plain,
( v3_struct_0(sK3)
| ~ v11_lattices(sK3)
| ~ v15_lattices(sK3)
| v17_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_2
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(resolution,[],[f1082,f252]) ).
fof(f1102,plain,
( ~ v11_lattices(sK3)
| ~ v15_lattices(sK3)
| v17_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_2
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1101,f468]) ).
fof(f1103,plain,
( ~ v15_lattices(sK3)
| v17_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_2
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1102,f1098]) ).
fof(f1104,plain,
( v17_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_2
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1103,f1081]) ).
fof(f1105,plain,
( ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1104,f457]) ).
fof(f1106,plain,
( $false
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1105,f449]) ).
fof(f1107,plain,
( ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(avatar_contradiction_clause,[],[f1106]) ).
fof(f1152,definition,
( spl27_47
<=> v16_lattices(k1_lattice2(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_47])],[avatar_definition]) ).
fof(f1153,plain,
( ~ v16_lattices(k1_lattice2(sK3))
| spl27_47 ),
inference(avatar_component_clause,[],[f1152]) ).
fof(f1154,plain,
( v16_lattices(k1_lattice2(sK3))
| ~ spl27_47 ),
inference(avatar_component_clause,[],[f1152]) ).
fof(f1157,definition,
( spl27_48
<=> v15_lattices(k1_lattice2(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_48])],[avatar_definition]) ).
fof(f1158,plain,
( ~ v15_lattices(k1_lattice2(sK3))
| spl27_48 ),
inference(avatar_component_clause,[],[f1157]) ).
fof(f1159,plain,
( v15_lattices(k1_lattice2(sK3))
| ~ spl27_48 ),
inference(avatar_component_clause,[],[f1157]) ).
fof(f1172,definition,
( spl27_51
<=> v11_lattices(k1_lattice2(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_51])],[avatar_definition]) ).
fof(f1173,plain,
( ~ v11_lattices(k1_lattice2(sK3))
| spl27_51 ),
inference(avatar_component_clause,[],[f1172]) ).
fof(f1186,plain,
( v3_struct_0(sK3)
| v11_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_3 ),
inference(resolution,[],[f458,f250]) ).
fof(f1187,plain,
( v3_struct_0(sK3)
| v13_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_3 ),
inference(resolution,[],[f458,f249]) ).
fof(f1188,plain,
( v3_struct_0(sK3)
| v14_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_3 ),
inference(resolution,[],[f458,f248]) ).
fof(f1190,plain,
( v3_struct_0(sK3)
| v16_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_3 ),
inference(resolution,[],[f458,f246]) ).
fof(f1191,plain,
( v16_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1190,f468]) ).
fof(f1193,plain,
( v14_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1188,f468]) ).
fof(f1194,plain,
( v13_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1187,f468]) ).
fof(f1195,plain,
( v11_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1186,f468]) ).
fof(f1196,plain,
( v16_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1191,f449]) ).
fof(f1198,plain,
( v14_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1193,f449]) ).
fof(f1199,plain,
( v13_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1194,f449]) ).
fof(f1200,plain,
( v11_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1195,f449]) ).
fof(f1201,plain,
( v3_struct_0(sK3)
| ~ v10_lattices(sK3)
| ~ v15_lattices(sK3)
| sP1(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(resolution,[],[f1196,f428]) ).
fof(f1203,plain,
( ~ v10_lattices(sK3)
| ~ v15_lattices(sK3)
| sP1(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1201,f468]) ).
fof(f1204,plain,
( ~ v15_lattices(sK3)
| sP1(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| ~ spl27_4
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1203,f463]) ).
fof(f1205,plain,
( ~ v15_lattices(sK3)
| sP1(sK3)
| ~ spl27_1
| ~ spl27_3
| ~ spl27_4
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1204,f449]) ).
fof(f1207,definition,
( spl27_54
<=> sP1(sK3) ),
introduced(definition,[new_symbols(definition,[spl27_54])],[avatar_definition]) ).
fof(f1209,plain,
( sP1(sK3)
| ~ spl27_54 ),
inference(avatar_component_clause,[],[f1207]) ).
fof(f1211,definition,
( spl27_55
<=> v15_lattices(sK3) ),
introduced(definition,[new_symbols(definition,[spl27_55])],[avatar_definition]) ).
fof(f1214,plain,
( spl27_54
| ~ spl27_55
| ~ spl27_1
| ~ spl27_3
| ~ spl27_4
| spl27_5 ),
inference(avatar_split_clause,[],[f1205,f466,f461,f456,f447,f1211,f1207]) ).
fof(f1216,plain,
( v3_struct_0(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_8 ),
inference(resolution,[],[f488,f290]) ).
fof(f1220,plain,
( ~ l3_lattices(sK3)
| spl27_5
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f1216,f468]) ).
fof(f1222,plain,
( $false
| ~ spl27_1
| spl27_5
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f1220,f449]) ).
fof(f1223,plain,
( ~ spl27_1
| spl27_5
| ~ spl27_8 ),
inference(avatar_contradiction_clause,[],[f1222]) ).
fof(f1241,plain,
( ~ sP0(sK3)
| spl27_7 ),
inference(resolution,[],[f480,f309]) ).
fof(f1242,plain,
( $false
| ~ spl27_1
| ~ spl27_4
| spl27_5
| spl27_7 ),
inference(forward_subsumption_resolution,[],[f1241,f863]) ).
fof(f1243,plain,
( ~ spl27_1
| ~ spl27_4
| spl27_5
| spl27_7 ),
inference(avatar_contradiction_clause,[],[f1242]) ).
fof(f1257,plain,
( v3_struct_0(sK3)
| ~ v13_lattices(sK3)
| v15_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(resolution,[],[f1198,f241]) ).
fof(f1258,plain,
( ~ v13_lattices(sK3)
| v15_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1257,f468]) ).
fof(f1259,plain,
( ~ v13_lattices(sK3)
| v15_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1258,f449]) ).
fof(f1261,definition,
( spl27_56
<=> v13_lattices(sK3) ),
introduced(definition,[new_symbols(definition,[spl27_56])],[avatar_definition]) ).
fof(f1264,plain,
( spl27_55
| ~ spl27_56
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(avatar_split_clause,[],[f1259,f466,f456,f447,f1261,f1211]) ).
fof(f1265,plain,
( spl27_56
| ~ spl27_1
| ~ spl27_3
| spl27_5 ),
inference(avatar_split_clause,[],[f1199,f466,f456,f447,f1261]) ).
fof(f1382,plain,
( ~ sP1(sK3)
| ~ sP2(sK3)
| spl27_48 ),
inference(resolution,[],[f1158,f419]) ).
fof(f1383,plain,
( ~ sP2(sK3)
| spl27_48
| ~ spl27_54 ),
inference(forward_subsumption_resolution,[],[f1382,f1209]) ).
fof(f1384,plain,
( $false
| ~ spl27_1
| ~ spl27_4
| spl27_5
| spl27_48
| ~ spl27_54 ),
inference(forward_subsumption_resolution,[],[f1383,f911]) ).
fof(f1385,plain,
( ~ spl27_1
| ~ spl27_4
| spl27_5
| spl27_48
| ~ spl27_54 ),
inference(avatar_contradiction_clause,[],[f1384]) ).
fof(f1386,plain,
( ~ sP1(sK3)
| ~ sP2(sK3)
| spl27_47 ),
inference(resolution,[],[f1153,f418]) ).
fof(f1387,plain,
( ~ sP2(sK3)
| spl27_47
| ~ spl27_54 ),
inference(forward_subsumption_resolution,[],[f1386,f1209]) ).
fof(f1388,plain,
( $false
| ~ spl27_1
| ~ spl27_4
| spl27_5
| spl27_47
| ~ spl27_54 ),
inference(forward_subsumption_resolution,[],[f1387,f911]) ).
fof(f1389,plain,
( ~ spl27_1
| ~ spl27_4
| spl27_5
| spl27_47
| ~ spl27_54 ),
inference(avatar_contradiction_clause,[],[f1388]) ).
fof(f1392,plain,
( v3_struct_0(k1_lattice2(sK3))
| ~ v11_lattices(k1_lattice2(sK3))
| ~ v15_lattices(k1_lattice2(sK3))
| v17_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| ~ spl27_47 ),
inference(resolution,[],[f1154,f252]) ).
fof(f1393,plain,
( ~ v11_lattices(k1_lattice2(sK3))
| ~ v15_lattices(k1_lattice2(sK3))
| v17_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| spl27_8
| ~ spl27_47 ),
inference(forward_subsumption_resolution,[],[f1392,f489]) ).
fof(f1395,plain,
( ~ v11_lattices(k1_lattice2(sK3))
| ~ v15_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| spl27_6
| spl27_8
| ~ spl27_47 ),
inference(forward_subsumption_resolution,[],[f1393,f472]) ).
fof(f1410,plain,
( v3_struct_0(sK3)
| ~ v10_lattices(sK3)
| ~ v11_lattices(sK3)
| ~ l3_lattices(sK3)
| spl27_51 ),
inference(resolution,[],[f1173,f443]) ).
fof(f1411,plain,
( ~ v10_lattices(sK3)
| ~ v11_lattices(sK3)
| ~ l3_lattices(sK3)
| spl27_5
| spl27_51 ),
inference(forward_subsumption_resolution,[],[f1410,f468]) ).
fof(f1412,plain,
( ~ v11_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ spl27_4
| spl27_5
| spl27_51 ),
inference(forward_subsumption_resolution,[],[f1411,f463]) ).
fof(f1413,plain,
( ~ l3_lattices(sK3)
| ~ spl27_1
| ~ spl27_3
| ~ spl27_4
| spl27_5
| spl27_51 ),
inference(forward_subsumption_resolution,[],[f1412,f1200]) ).
fof(f1414,plain,
( $false
| ~ spl27_1
| ~ spl27_3
| ~ spl27_4
| spl27_5
| spl27_51 ),
inference(forward_subsumption_resolution,[],[f1413,f449]) ).
fof(f1415,plain,
( ~ spl27_1
| ~ spl27_3
| ~ spl27_4
| spl27_5
| spl27_51 ),
inference(avatar_contradiction_clause,[],[f1414]) ).
fof(f1416,plain,
( ~ v11_lattices(k1_lattice2(sK3))
| ~ l3_lattices(k1_lattice2(sK3))
| spl27_6
| spl27_8
| ~ spl27_47
| ~ spl27_48 ),
inference(forward_subsumption_resolution,[],[f1395,f1159]) ).
fof(f1418,plain,
( ~ spl27_2
| ~ spl27_51
| spl27_6
| spl27_8
| ~ spl27_47
| ~ spl27_48 ),
inference(avatar_split_clause,[],[f1416,f1157,f1152,f487,f471,f1172,f451]) ).
fof(f1421,plain,
( ~ l3_lattices(sK3)
| spl27_2 ),
inference(resolution,[],[f452,f269]) ).
fof(f1422,plain,
( $false
| ~ spl27_1
| spl27_2 ),
inference(forward_subsumption_resolution,[],[f1421,f449]) ).
fof(f1423,plain,
( ~ spl27_1
| spl27_2 ),
inference(avatar_contradiction_clause,[],[f1422]) ).
cnf(s6,plain,
( spl27_3
| spl27_6 ),
inference(sat_conversion,[],[f475]) ).
cnf(s17,plain,
( ~ spl27_1
| ~ spl27_2
| ~ spl27_3
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(sat_conversion,[],[f494]) ).
cnf(s18,plain,
spl27_1,
inference(sat_conversion,[],[f495]) ).
cnf(s19,plain,
spl27_4,
inference(sat_conversion,[],[f496]) ).
cnf(s20,plain,
~ spl27_5,
inference(sat_conversion,[],[f497]) ).
cnf(s50,plain,
( ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_5
| ~ spl27_6
| ~ spl27_7
| spl27_8 ),
inference(sat_conversion,[],[f1107]) ).
cnf(s64,plain,
( ~ spl27_1
| ~ spl27_3
| ~ spl27_4
| spl27_5
| spl27_54
| ~ spl27_55 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s66,plain,
( ~ spl27_1
| spl27_5
| ~ spl27_8 ),
inference(sat_conversion,[],[f1223]) ).
cnf(s82,plain,
( ~ spl27_1
| ~ spl27_4
| spl27_5
| spl27_7 ),
inference(sat_conversion,[],[f1243]) ).
cnf(s92,plain,
( ~ spl27_1
| ~ spl27_3
| spl27_5
| spl27_55
| ~ spl27_56 ),
inference(sat_conversion,[],[f1264]) ).
cnf(s93,plain,
( ~ spl27_1
| ~ spl27_3
| spl27_5
| spl27_56 ),
inference(sat_conversion,[],[f1265]) ).
cnf(s104,plain,
( ~ spl27_1
| ~ spl27_4
| spl27_5
| spl27_48
| ~ spl27_54 ),
inference(sat_conversion,[],[f1385]) ).
cnf(s105,plain,
( ~ spl27_1
| ~ spl27_4
| spl27_5
| spl27_47
| ~ spl27_54 ),
inference(sat_conversion,[],[f1389]) ).
cnf(s110,plain,
( ~ spl27_1
| ~ spl27_3
| ~ spl27_4
| spl27_5
| spl27_51 ),
inference(sat_conversion,[],[f1415]) ).
cnf(s111,plain,
( ~ spl27_2
| spl27_6
| spl27_8
| ~ spl27_47
| ~ spl27_48
| ~ spl27_51 ),
inference(sat_conversion,[],[f1418]) ).
cnf(s113,plain,
( ~ spl27_1
| spl27_2 ),
inference(sat_conversion,[],[f1423]) ).
cnf(s116,plain,
spl27_2,
inference(rat,[],[s113,s18]) ).
cnf(s117,plain,
spl27_7,
inference(rat,[],[s82,s19,s20,s18]) ).
cnf(s118,plain,
~ spl27_8,
inference(rat,[],[s66,s20,s18]) ).
cnf(s127,plain,
( ~ spl27_3
| ~ spl27_6 ),
inference(rat,[],[s17,s118,s117,s20,s19,s116,s18]) ).
cnf(s128,plain,
spl27_3,
inference(rat,[],[s6,s50,s18,s19,s20,s116,s117,s118]) ).
cnf(s129,plain,
spl27_51,
inference(rat,[],[s110,s18,s20,s19,s128]) ).
cnf(s130,plain,
spl27_56,
inference(rat,[],[s93,s18,s20,s128]) ).
cnf(s131,plain,
spl27_55,
inference(rat,[],[s92,s130,s18,s20,s128]) ).
cnf(s132,plain,
~ spl27_6,
inference(rat,[],[s127,s128]) ).
cnf(s133,plain,
spl27_54,
inference(rat,[],[s64,s128,s18,s20,s19,s131]) ).
cnf(s134,plain,
spl27_47,
inference(rat,[],[s105,s18,s19,s20,s133]) ).
cnf(s135,plain,
spl27_48,
inference(rat,[],[s104,s18,s19,s20,s133]) ).
cnf(s136,plain,
$false,
inference(rat,[],[s111,s129,s132,s116,s118,s135,s134]) ).
fof(f1427,plain,
$false,
inference(avatar_sat_refutation,[],[s136]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT319+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n011.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 14:35:45 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.48 % (2493615)Will run a generic schedule for satisfiability detection.
% 0.16/0.48 % (2493620)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=771244592_2999 on theBenchmark for (2999ds/0Mi)
% 0.16/0.48 % (2493621)% WARNING: option uhcvi not known.
% 0.16/0.48 % TRYING [1]
% 0.16/0.48 % TRYING [2]
% 0.16/0.48 % (2493621)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3802714483:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.16/0.48 % (2493623)dis+10_1_sil=32000:sp=arity:random_seed=3440300193:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.16/0.48 % (2493622)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4034055530:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.16/0.48 % TRYING [3]
% 0.16/0.48 % (2493624)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3776776193:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.16/0.48 % (2493626)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=214015071:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.16/0.48 % (2493625)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4026881279:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.16/0.48 % TRYING [4]
% 0.16/0.48 % TRYING [5]
% 0.16/0.48 % (2493623) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2493615-2493623"...
% 0.16/0.48 % (2493625) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2493615-2493625"...
% 0.16/0.48 % (2493623)...printing done.
% 0.16/0.48 % (2493625)...printing done.
% 0.16/0.48 % (2493623)Refutation found. Thanks to Tanya!
% 0.16/0.48 % SZS status Theorem for theBenchmark
% 0.16/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/0.48 % (2493623)------------------------------
% 0.16/0.48 % (2493623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.16/0.48 % (2493623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/0.48 % (2493623)CaDiCaL version: 2.1.3
% 0.16/0.48 % (2493623)Termination reason: Refutation
% 0.16/0.48 % (2493623)Time elapsed: 0.022 s
% 0.16/0.48 % (2493623)Peak memory usage: 13 MB
% 0.16/0.48 % (2493623)Instructions burned: 30 (million)
% 0.16/0.48 % (2493615)Success in time 0.064 s
% 0.16/0.48 % Vampire exiting
%------------------------------------------------------------------------------