%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT346+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:47:09 AM UTC 2026
% Result : Theorem 2.43s 1.79s
% Output : Refutation 5.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 23
% Syntax : Number of formulae : 179 ( 22 unt; 12 def)
% Number of atoms : 723 ( 0 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 875 ( 331 ~; 356 |; 147 &)
% ( 15 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 29 ( 28 usr; 13 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% Number of variables : 87 ( 0 sgn 80 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4151,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f4156,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/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f4256,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f4342,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ( r1_filter_1(X0,X1)
=> r1_filter_1(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_r1_filter_1) ).
fof(f4514,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ( r1_filter_1(X0,X1)
<=> ? [X2] :
( m1_lattice4(X2,X0,X1)
& v3_lattice4(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_lattice4) ).
fof(f5266,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_conlat_1) ).
fof(f5331,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_conlat_1) ).
fof(f5460,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& l2_conlat_1(k7_conlat_2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_conlat_2) ).
fof(f5464,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> m1_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k10_conlat_2) ).
fof(f5500,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> v3_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_conlat_2) ).
fof(f5501,conjecture,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> r1_filter_1(k11_conlat_1(k7_conlat_2(X0)),k1_lattice2(k11_conlat_1(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t22_conlat_2) ).
fof(f5502,negated_conjecture,
~ ! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> r1_filter_1(k11_conlat_1(k7_conlat_2(X0)),k1_lattice2(k11_conlat_1(X0))) ),
inference(negated_conjecture,[status(cth)],[f5501]) ).
fof(f5504,plain,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f5266]) ).
fof(f5506,plain,
! [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))
& v10_lattices(k1_lattice2(X0)) ) ),
inference(pure_predicate_removal,[],[f4156]) ).
fof(f5509,plain,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f5504]) ).
fof(f5510,plain,
! [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))
& v10_lattices(k1_lattice2(X0)) ) ),
inference(pure_predicate_removal,[],[f5506]) ).
fof(f5513,plain,
! [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))
& v10_lattices(k1_lattice2(X0)) ) ),
inference(pure_predicate_removal,[],[f5510]) ).
fof(f5514,plain,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f5509]) ).
fof(f5518,plain,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f5514]) ).
fof(f5519,plain,
! [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))
& v10_lattices(k1_lattice2(X0)) ) ),
inference(pure_predicate_removal,[],[f5513]) ).
fof(f5521,plain,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f5518]) ).
fof(f5523,plain,
! [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))
& v10_lattices(k1_lattice2(X0)) ) ),
inference(pure_predicate_removal,[],[f5519]) ).
fof(f5525,plain,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f5521]) ).
fof(f5527,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
inference(pure_predicate_removal,[],[f5523]) ).
fof(f5529,plain,
? [X0] :
( ~ r1_filter_1(k11_conlat_1(k7_conlat_2(X0)),k1_lattice2(k11_conlat_1(X0)))
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f5502]) ).
fof(f5530,plain,
? [X0] :
( ~ r1_filter_1(k11_conlat_1(k7_conlat_2(X0)),k1_lattice2(k11_conlat_1(X0)))
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(flattening,[],[f5529]) ).
fof(f5537,plain,
! [X0] :
( ! [X1] :
( ( r1_filter_1(X0,X1)
<=> ? [X2] :
( m1_lattice4(X2,X0,X1)
& v3_lattice4(X2,X0,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4514]) ).
fof(f5538,plain,
! [X0] :
( ! [X1] :
( ( r1_filter_1(X0,X1)
<=> ? [X2] :
( m1_lattice4(X2,X0,X1)
& v3_lattice4(X2,X0,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5537]) ).
fof(f5541,plain,
! [X0,X1] :
( r1_filter_1(X1,X0)
| ~ r1_filter_1(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(ennf_transformation,[],[f4342]) ).
fof(f5542,plain,
! [X0,X1] :
( r1_filter_1(X1,X0)
| ~ r1_filter_1(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(flattening,[],[f5541]) ).
fof(f5549,plain,
! [X0] :
( v3_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f5500]) ).
fof(f5550,plain,
! [X0] :
( v3_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f5549]) ).
fof(f5555,plain,
! [X0] :
( m1_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f5464]) ).
fof(f5556,plain,
! [X0] :
( m1_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f5555]) ).
fof(f5563,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4256]) ).
fof(f5587,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f5527]) ).
fof(f5588,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5587]) ).
fof(f5589,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4151]) ).
fof(f5590,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5589]) ).
fof(f5595,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f5331]) ).
fof(f5596,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f5595]) ).
fof(f5599,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f5525]) ).
fof(f5600,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f5599]) ).
fof(f5619,plain,
! [X0] :
( ( ~ v3_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& l2_conlat_1(k7_conlat_2(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f5460]) ).
fof(f5620,plain,
! [X0] :
( ( ~ v3_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& l2_conlat_1(k7_conlat_2(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f5619]) ).
fof(f5623,plain,
( ~ r1_filter_1(k11_conlat_1(k7_conlat_2(sK1)),k1_lattice2(k11_conlat_1(sK1)))
& ~ v3_conlat_1(sK1)
& l2_conlat_1(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X0,sK1)],[f5530]) ).
fof(f5634,plain,
! [X0] :
( ! [X1] :
( ( ( r1_filter_1(X0,X1)
| ! [X2] :
( ~ m1_lattice4(X2,X0,X1)
| ~ v3_lattice4(X2,X0,X1) ) )
& ( ? [X2] :
( m1_lattice4(X2,X0,X1)
& v3_lattice4(X2,X0,X1) )
| ~ r1_filter_1(X0,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f5538]) ).
fof(f5635,plain,
! [X0] :
( ! [X1] :
( ( ( r1_filter_1(X0,X1)
| ! [X2] :
( ~ m1_lattice4(X2,X0,X1)
| ~ v3_lattice4(X2,X0,X1) ) )
& ( ? [X3] :
( m1_lattice4(X3,X0,X1)
& v3_lattice4(X3,X0,X1) )
| ~ r1_filter_1(X0,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f5634]) ).
fof(f5636,plain,
! [X0] :
( ! [X1] :
( ( ( r1_filter_1(X0,X1)
| ! [X2] :
( ~ m1_lattice4(X2,X0,X1)
| ~ v3_lattice4(X2,X0,X1) ) )
& ( ( m1_lattice4(sK7(X0,X1),X0,X1)
& v3_lattice4(sK7(X0,X1),X0,X1) )
| ~ r1_filter_1(X0,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X3,sK7(X0,X1))],[f5635]) ).
fof(f5650,plain,
l2_conlat_1(sK1),
inference(cnf_transformation,[],[f5623]) ).
fof(f5651,plain,
~ v3_conlat_1(sK1),
inference(cnf_transformation,[],[f5623]) ).
fof(f5652,plain,
~ r1_filter_1(k11_conlat_1(k7_conlat_2(sK1)),k1_lattice2(k11_conlat_1(sK1))),
inference(cnf_transformation,[],[f5623]) ).
fof(f5676,plain,
! [X2,X0,X1] :
( r1_filter_1(X0,X1)
| ~ m1_lattice4(X2,X0,X1)
| ~ v3_lattice4(X2,X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5636]) ).
fof(f5678,plain,
! [X0,X1] :
( r1_filter_1(X1,X0)
| ~ r1_filter_1(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f5542]) ).
fof(f5684,plain,
! [X0] :
( v3_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5550]) ).
fof(f5695,plain,
! [X0] :
( m1_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5556]) ).
fof(f5701,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5563]) ).
fof(f5728,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5588]) ).
fof(f5732,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5590]) ).
fof(f5740,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5596]) ).
fof(f5747,plain,
! [X0] :
( v10_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5600]) ).
fof(f5749,plain,
! [X0] :
( ~ v3_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5600]) ).
fof(f5767,plain,
! [X0] :
( l2_conlat_1(k7_conlat_2(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5620]) ).
fof(f5769,plain,
! [X0] :
( ~ v3_conlat_1(k7_conlat_2(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5620]) ).
fof(f5829,definition,
( spl10_3
<=> l3_lattices(k1_lattice2(k11_conlat_1(sK1))) ),
introduced(definition,[new_symbols(definition,[spl10_3])],[avatar_definition]) ).
fof(f5830,plain,
( l3_lattices(k1_lattice2(k11_conlat_1(sK1)))
| ~ spl10_3 ),
inference(avatar_component_clause,[],[f5829]) ).
fof(f5831,plain,
( ~ l3_lattices(k1_lattice2(k11_conlat_1(sK1)))
| spl10_3 ),
inference(avatar_component_clause,[],[f5829]) ).
fof(f5833,definition,
( spl10_4
<=> v10_lattices(k1_lattice2(k11_conlat_1(sK1))) ),
introduced(definition,[new_symbols(definition,[spl10_4])],[avatar_definition]) ).
fof(f5834,plain,
( v10_lattices(k1_lattice2(k11_conlat_1(sK1)))
| ~ spl10_4 ),
inference(avatar_component_clause,[],[f5833]) ).
fof(f5835,plain,
( ~ v10_lattices(k1_lattice2(k11_conlat_1(sK1)))
| spl10_4 ),
inference(avatar_component_clause,[],[f5833]) ).
fof(f5837,definition,
( spl10_5
<=> v3_struct_0(k1_lattice2(k11_conlat_1(sK1))) ),
introduced(definition,[new_symbols(definition,[spl10_5])],[avatar_definition]) ).
fof(f5838,plain,
( ~ v3_struct_0(k1_lattice2(k11_conlat_1(sK1)))
| spl10_5 ),
inference(avatar_component_clause,[],[f5837]) ).
fof(f5839,plain,
( v3_struct_0(k1_lattice2(k11_conlat_1(sK1)))
| ~ spl10_5 ),
inference(avatar_component_clause,[],[f5837]) ).
fof(f5850,definition,
( spl10_8
<=> v3_struct_0(k11_conlat_1(sK1)) ),
introduced(definition,[new_symbols(definition,[spl10_8])],[avatar_definition]) ).
fof(f5851,plain,
( v3_struct_0(k11_conlat_1(sK1))
| ~ spl10_8 ),
inference(avatar_component_clause,[],[f5850]) ).
fof(f5852,plain,
( ~ v3_struct_0(k11_conlat_1(sK1))
| spl10_8 ),
inference(avatar_component_clause,[],[f5850]) ).
fof(f5860,definition,
( spl10_10
<=> v10_lattices(k11_conlat_1(sK1)) ),
introduced(definition,[new_symbols(definition,[spl10_10])],[avatar_definition]) ).
fof(f5861,plain,
( ~ v10_lattices(k11_conlat_1(sK1))
| spl10_10 ),
inference(avatar_component_clause,[],[f5860]) ).
fof(f5908,definition,
( spl10_20
<=> l3_lattices(k11_conlat_1(sK1)) ),
introduced(definition,[new_symbols(definition,[spl10_20])],[avatar_definition]) ).
fof(f5909,plain,
( ~ l3_lattices(k11_conlat_1(sK1))
| spl10_20 ),
inference(avatar_component_clause,[],[f5908]) ).
fof(f5910,plain,
( l3_lattices(k11_conlat_1(sK1))
| ~ spl10_20 ),
inference(avatar_component_clause,[],[f5908]) ).
fof(f5932,plain,
( ~ l3_lattices(k11_conlat_1(sK1))
| spl10_3 ),
inference(resolution,[],[f5831,f5701]) ).
fof(f5933,plain,
( ~ spl10_20
| spl10_3 ),
inference(avatar_split_clause,[],[f5932,f5829,f5908]) ).
fof(f5934,plain,
( v3_conlat_1(sK1)
| ~ l2_conlat_1(sK1)
| spl10_20 ),
inference(resolution,[],[f5909,f5740]) ).
fof(f5935,plain,
( ~ l2_conlat_1(sK1)
| spl10_20 ),
inference(forward_subsumption_resolution,[],[f5934,f5651]) ).
fof(f5936,plain,
( $false
| spl10_20 ),
inference(forward_subsumption_resolution,[],[f5935,f5650]) ).
fof(f5937,plain,
spl10_20,
inference(avatar_contradiction_clause,[],[f5936]) ).
fof(f5943,plain,
( v3_struct_0(k11_conlat_1(sK1))
| ~ l3_lattices(k11_conlat_1(sK1))
| ~ spl10_5 ),
inference(resolution,[],[f5839,f5732]) ).
fof(f5944,plain,
( v3_struct_0(k11_conlat_1(sK1))
| ~ spl10_5
| ~ spl10_20 ),
inference(forward_subsumption_resolution,[],[f5943,f5910]) ).
fof(f5945,plain,
( spl10_8
| ~ spl10_5
| ~ spl10_20 ),
inference(avatar_split_clause,[],[f5944,f5908,f5837,f5850]) ).
fof(f5946,plain,
( v3_conlat_1(sK1)
| ~ l2_conlat_1(sK1)
| ~ spl10_8 ),
inference(resolution,[],[f5851,f5749]) ).
fof(f5947,plain,
( ~ l2_conlat_1(sK1)
| ~ spl10_8 ),
inference(forward_subsumption_resolution,[],[f5946,f5651]) ).
fof(f5948,plain,
( $false
| ~ spl10_8 ),
inference(forward_subsumption_resolution,[],[f5947,f5650]) ).
fof(f5949,plain,
~ spl10_8,
inference(avatar_contradiction_clause,[],[f5948]) ).
fof(f5951,plain,
( v3_struct_0(k11_conlat_1(sK1))
| ~ v10_lattices(k11_conlat_1(sK1))
| ~ l3_lattices(k11_conlat_1(sK1))
| spl10_4 ),
inference(resolution,[],[f5835,f5728]) ).
fof(f5952,plain,
( ~ v10_lattices(k11_conlat_1(sK1))
| ~ l3_lattices(k11_conlat_1(sK1))
| spl10_4
| spl10_8 ),
inference(forward_subsumption_resolution,[],[f5951,f5852]) ).
fof(f5953,plain,
( ~ v10_lattices(k11_conlat_1(sK1))
| spl10_4
| spl10_8
| ~ spl10_20 ),
inference(forward_subsumption_resolution,[],[f5952,f5910]) ).
fof(f5954,plain,
( ~ spl10_10
| spl10_4
| spl10_8
| ~ spl10_20 ),
inference(avatar_split_clause,[],[f5953,f5908,f5850,f5833,f5860]) ).
fof(f5955,plain,
( v3_conlat_1(sK1)
| ~ l2_conlat_1(sK1)
| spl10_10 ),
inference(resolution,[],[f5861,f5747]) ).
fof(f5956,plain,
( ~ l2_conlat_1(sK1)
| spl10_10 ),
inference(forward_subsumption_resolution,[],[f5955,f5651]) ).
fof(f5957,plain,
( $false
| spl10_10 ),
inference(forward_subsumption_resolution,[],[f5956,f5650]) ).
fof(f5958,plain,
spl10_10,
inference(avatar_contradiction_clause,[],[f5957]) ).
fof(f5987,plain,
( ~ r1_filter_1(k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK1)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK1)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK1)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK1)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK1))) ),
inference(resolution,[],[f5678,f5652]) ).
fof(f5988,plain,
( ~ r1_filter_1(k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK1)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK1)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK1)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| spl10_5 ),
inference(forward_subsumption_resolution,[],[f5987,f5838]) ).
fof(f5989,plain,
( ~ r1_filter_1(k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK1)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK1)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| ~ spl10_4
| spl10_5 ),
inference(forward_subsumption_resolution,[],[f5988,f5834]) ).
fof(f5990,plain,
( ~ r1_filter_1(k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK1)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| ~ spl10_3
| ~ spl10_4
| spl10_5 ),
inference(forward_subsumption_resolution,[],[f5989,f5830]) ).
fof(f5992,definition,
( spl10_25
<=> l3_lattices(k11_conlat_1(k7_conlat_2(sK1))) ),
introduced(definition,[new_symbols(definition,[spl10_25])],[avatar_definition]) ).
fof(f5993,plain,
( l3_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| ~ spl10_25 ),
inference(avatar_component_clause,[],[f5992]) ).
fof(f5994,plain,
( ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| spl10_25 ),
inference(avatar_component_clause,[],[f5992]) ).
fof(f5996,definition,
( spl10_26
<=> v10_lattices(k11_conlat_1(k7_conlat_2(sK1))) ),
introduced(definition,[new_symbols(definition,[spl10_26])],[avatar_definition]) ).
fof(f5997,plain,
( v10_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| ~ spl10_26 ),
inference(avatar_component_clause,[],[f5996]) ).
fof(f5998,plain,
( ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| spl10_26 ),
inference(avatar_component_clause,[],[f5996]) ).
fof(f6000,definition,
( spl10_27
<=> v3_struct_0(k11_conlat_1(k7_conlat_2(sK1))) ),
introduced(definition,[new_symbols(definition,[spl10_27])],[avatar_definition]) ).
fof(f6001,plain,
( ~ v3_struct_0(k11_conlat_1(k7_conlat_2(sK1)))
| spl10_27 ),
inference(avatar_component_clause,[],[f6000]) ).
fof(f6002,plain,
( v3_struct_0(k11_conlat_1(k7_conlat_2(sK1)))
| ~ spl10_27 ),
inference(avatar_component_clause,[],[f6000]) ).
fof(f6004,definition,
( spl10_28
<=> r1_filter_1(k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1))) ),
introduced(definition,[new_symbols(definition,[spl10_28])],[avatar_definition]) ).
fof(f6006,plain,
( ~ r1_filter_1(k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| spl10_28 ),
inference(avatar_component_clause,[],[f6004]) ).
fof(f6007,plain,
( ~ spl10_25
| ~ spl10_26
| spl10_27
| ~ spl10_28
| ~ spl10_3
| ~ spl10_4
| spl10_5 ),
inference(avatar_split_clause,[],[f5990,f5837,f5833,f5829,f6004,f6000,f5996,f5992]) ).
fof(f6009,plain,
( v3_conlat_1(k7_conlat_2(sK1))
| ~ l2_conlat_1(k7_conlat_2(sK1))
| spl10_25 ),
inference(resolution,[],[f5994,f5740]) ).
fof(f6011,definition,
( spl10_29
<=> l2_conlat_1(k7_conlat_2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl10_29])],[avatar_definition]) ).
fof(f6012,plain,
( l2_conlat_1(k7_conlat_2(sK1))
| ~ spl10_29 ),
inference(avatar_component_clause,[],[f6011]) ).
fof(f6013,plain,
( ~ l2_conlat_1(k7_conlat_2(sK1))
| spl10_29 ),
inference(avatar_component_clause,[],[f6011]) ).
fof(f6015,definition,
( spl10_30
<=> v3_conlat_1(k7_conlat_2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl10_30])],[avatar_definition]) ).
fof(f6016,plain,
( ~ v3_conlat_1(k7_conlat_2(sK1))
| spl10_30 ),
inference(avatar_component_clause,[],[f6015]) ).
fof(f6017,plain,
( v3_conlat_1(k7_conlat_2(sK1))
| ~ spl10_30 ),
inference(avatar_component_clause,[],[f6015]) ).
fof(f6018,plain,
( ~ spl10_29
| spl10_30
| spl10_25 ),
inference(avatar_split_clause,[],[f6009,f5992,f6015,f6011]) ).
fof(f6019,plain,
( v3_conlat_1(sK1)
| ~ l2_conlat_1(sK1)
| spl10_29 ),
inference(resolution,[],[f6013,f5767]) ).
fof(f6020,plain,
( ~ l2_conlat_1(sK1)
| spl10_29 ),
inference(forward_subsumption_resolution,[],[f6019,f5651]) ).
fof(f6021,plain,
( $false
| spl10_29 ),
inference(forward_subsumption_resolution,[],[f6020,f5650]) ).
fof(f6022,plain,
spl10_29,
inference(avatar_contradiction_clause,[],[f6021]) ).
fof(f6037,plain,
( v3_conlat_1(sK1)
| ~ l2_conlat_1(sK1)
| ~ spl10_30 ),
inference(resolution,[],[f6017,f5769]) ).
fof(f6038,plain,
( ~ l2_conlat_1(sK1)
| ~ spl10_30 ),
inference(forward_subsumption_resolution,[],[f6037,f5651]) ).
fof(f6039,plain,
( $false
| ~ spl10_30 ),
inference(forward_subsumption_resolution,[],[f6038,f5650]) ).
fof(f6040,plain,
~ spl10_30,
inference(avatar_contradiction_clause,[],[f6039]) ).
fof(f6044,plain,
( v3_conlat_1(k7_conlat_2(sK1))
| ~ l2_conlat_1(k7_conlat_2(sK1))
| ~ spl10_27 ),
inference(resolution,[],[f6002,f5749]) ).
fof(f6045,plain,
( ~ l2_conlat_1(k7_conlat_2(sK1))
| ~ spl10_27
| spl10_30 ),
inference(forward_subsumption_resolution,[],[f6044,f6016]) ).
fof(f6046,plain,
( $false
| ~ spl10_27
| ~ spl10_29
| spl10_30 ),
inference(forward_subsumption_resolution,[],[f6045,f6012]) ).
fof(f6047,plain,
( ~ spl10_27
| ~ spl10_29
| spl10_30 ),
inference(avatar_contradiction_clause,[],[f6046]) ).
fof(f6122,plain,
( v3_conlat_1(k7_conlat_2(sK1))
| ~ l2_conlat_1(k7_conlat_2(sK1))
| spl10_26 ),
inference(resolution,[],[f5998,f5747]) ).
fof(f6123,plain,
( ~ l2_conlat_1(k7_conlat_2(sK1))
| spl10_26
| spl10_30 ),
inference(forward_subsumption_resolution,[],[f6122,f6016]) ).
fof(f6124,plain,
( $false
| spl10_26
| ~ spl10_29
| spl10_30 ),
inference(forward_subsumption_resolution,[],[f6123,f6012]) ).
fof(f6125,plain,
( spl10_26
| ~ spl10_29
| spl10_30 ),
inference(avatar_contradiction_clause,[],[f6124]) ).
fof(f6141,plain,
( ! [X0] :
( ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK1)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK1)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK1)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK1))) )
| spl10_28 ),
inference(resolution,[],[f6006,f5676]) ).
fof(f6143,plain,
( ! [X0] :
( ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK1)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK1)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK1))) )
| spl10_27
| spl10_28 ),
inference(forward_subsumption_resolution,[],[f6141,f6001]) ).
fof(f6144,plain,
( ! [X0] :
( ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK1)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK1)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK1)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK1))) )
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(forward_subsumption_resolution,[],[f6143,f5997]) ).
fof(f6145,plain,
( ! [X0] :
( ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK1)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK1)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK1))) )
| ~ spl10_25
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(forward_subsumption_resolution,[],[f6144,f5993]) ).
fof(f6146,plain,
( ! [X0] :
( ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK1)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK1))) )
| spl10_5
| ~ spl10_25
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(forward_subsumption_resolution,[],[f6145,f5838]) ).
fof(f6147,plain,
( ! [X0] :
( ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK1))) )
| ~ spl10_4
| spl10_5
| ~ spl10_25
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(forward_subsumption_resolution,[],[f6146,f5834]) ).
fof(f6148,plain,
( ! [X0] :
( ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1))) )
| ~ spl10_3
| ~ spl10_4
| spl10_5
| ~ spl10_25
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(forward_subsumption_resolution,[],[f6147,f5830]) ).
fof(f7085,plain,
( ~ m1_lattice4(k10_conlat_2(sK1),k1_lattice2(k11_conlat_1(sK1)),k11_conlat_1(k7_conlat_2(sK1)))
| v3_conlat_1(sK1)
| ~ l2_conlat_1(sK1)
| ~ spl10_3
| ~ spl10_4
| spl10_5
| ~ spl10_25
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(resolution,[],[f6148,f5684]) ).
fof(f7087,plain,
( v3_conlat_1(sK1)
| ~ l2_conlat_1(sK1)
| ~ spl10_3
| ~ spl10_4
| spl10_5
| ~ spl10_25
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(forward_subsumption_resolution,[],[f7085,f5695]) ).
fof(f7088,plain,
( ~ l2_conlat_1(sK1)
| ~ spl10_3
| ~ spl10_4
| spl10_5
| ~ spl10_25
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(forward_subsumption_resolution,[],[f7087,f5651]) ).
fof(f7089,plain,
( $false
| ~ spl10_3
| ~ spl10_4
| spl10_5
| ~ spl10_25
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(forward_subsumption_resolution,[],[f7088,f5650]) ).
fof(f7090,plain,
( ~ spl10_3
| ~ spl10_4
| spl10_5
| ~ spl10_25
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(avatar_contradiction_clause,[],[f7089]) ).
cnf(s16,plain,
( spl10_3
| ~ spl10_20 ),
inference(sat_conversion,[],[f5933]) ).
cnf(s17,plain,
spl10_20,
inference(sat_conversion,[],[f5937]) ).
cnf(s18,plain,
( ~ spl10_5
| spl10_8
| ~ spl10_20 ),
inference(sat_conversion,[],[f5945]) ).
cnf(s19,plain,
~ spl10_8,
inference(sat_conversion,[],[f5949]) ).
cnf(s20,plain,
( spl10_4
| spl10_8
| ~ spl10_10
| ~ spl10_20 ),
inference(sat_conversion,[],[f5954]) ).
cnf(s21,plain,
spl10_10,
inference(sat_conversion,[],[f5958]) ).
cnf(s26,plain,
( ~ spl10_3
| ~ spl10_4
| spl10_5
| ~ spl10_25
| ~ spl10_26
| spl10_27
| ~ spl10_28 ),
inference(sat_conversion,[],[f6007]) ).
cnf(s27,plain,
( spl10_25
| ~ spl10_29
| spl10_30 ),
inference(sat_conversion,[],[f6018]) ).
cnf(s28,plain,
spl10_29,
inference(sat_conversion,[],[f6022]) ).
cnf(s31,plain,
~ spl10_30,
inference(sat_conversion,[],[f6040]) ).
cnf(s33,plain,
( ~ spl10_27
| ~ spl10_29
| spl10_30 ),
inference(sat_conversion,[],[f6047]) ).
cnf(s40,plain,
( spl10_26
| ~ spl10_29
| spl10_30 ),
inference(sat_conversion,[],[f6125]) ).
cnf(s102,plain,
( ~ spl10_3
| ~ spl10_4
| spl10_5
| ~ spl10_25
| ~ spl10_26
| spl10_27
| spl10_28 ),
inference(sat_conversion,[],[f7090]) ).
cnf(s108,plain,
spl10_26,
inference(rat,[],[s40,s31,s28]) ).
cnf(s109,plain,
~ spl10_27,
inference(rat,[],[s33,s31,s28]) ).
cnf(s129,plain,
spl10_25,
inference(rat,[],[s27,s31,s28]) ).
cnf(s137,plain,
( ~ spl10_3
| ~ spl10_4
| spl10_5
| ~ spl10_28 ),
inference(rat,[],[s26,s109,s108,s129]) ).
cnf(s138,plain,
( spl10_4
| spl10_8
| ~ spl10_20 ),
inference(rat,[],[s20,s21]) ).
cnf(s139,plain,
( ~ spl10_5
| ~ spl10_20 ),
inference(rat,[],[s18,s19]) ).
cnf(s141,plain,
spl10_4,
inference(rat,[],[s138,s19,s17]) ).
cnf(s142,plain,
~ spl10_5,
inference(rat,[],[s139,s17]) ).
cnf(s143,plain,
spl10_3,
inference(rat,[],[s16,s17]) ).
cnf(s144,plain,
spl10_28,
inference(rat,[],[s102,s141,s109,s108,s129,s142,s143]) ).
cnf(s146,plain,
$false,
inference(rat,[],[s137,s141,s142,s144,s143]) ).
fof(f7091,plain,
$false,
inference(avatar_sat_refutation,[],[s146]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT346+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n017.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 14:47:36 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/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
% 2.43/1.79 % (2647548)Detected formulas, will run a generic FOF schedule.
% 2.43/1.79 % (2647558)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=533912331:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 2.43/1.79 % (2647559)dis-21_1_sil=8000:lcm=predicate:random_seed=3627722303:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 2.43/1.79 % (2647553)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=2336900277:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 2.43/1.79 % (2647557)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2085047223:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 2.43/1.79 % (2647554)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=56133500:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 2.43/1.79 % (2647555)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=2004445736:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 2.43/1.79 % (2647556)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=377857011:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 2.43/1.79 % (2647558)Instruction limit reached!
% 2.43/1.79 % (2647558)------------------------------
% 2.43/1.79 % (2647558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.43/1.79 % (2647558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.43/1.79 % (2647558)CaDiCaL version: 2.1.3
% 2.43/1.79 % (2647558)Termination reason: Instruction limit
% 2.43/1.79 % (2647558)Termination phase: Preprocessing 2
% 2.43/1.79 % (2647558)Time elapsed: 0.052 s
% 2.43/1.79 % (2647558)Peak memory usage: 93 MB
% 2.43/1.79 % (2647558)Instructions burned: 141 (million)
% 2.43/1.79 % (2647556)Refutation not found, incomplete strategy
% 2.43/1.79 % (2647556)------------------------------
% 2.43/1.79 % (2647556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.43/1.79 % (2647556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.43/1.79 % (2647556)CaDiCaL version: 2.1.3
% 2.43/1.79 % (2647556)Termination reason: Refutation not found, incomplete strategy
% 2.43/1.79 % (2647556)Time elapsed: 0.025 s
% 2.43/1.79 % (2647556)Peak memory usage: 95 MB
% 2.43/1.79 % (2647556)Instructions burned: 31 (million)
% 2.43/1.79 % (2647557)Instruction limit reached!
% 2.43/1.79 % (2647557)------------------------------
% 2.43/1.79 % (2647557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.43/1.79 % (2647557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.43/1.79 % (2647557)CaDiCaL version: 2.1.3
% 2.43/1.79 % (2647557)Termination reason: Instruction limit
% 2.43/1.79 % (2647557)Termination phase: Saturation
% 2.43/1.79 % (2647557)Time elapsed: 0.075 s
% 2.43/1.79 % (2647557)Peak memory usage: 95 MB
% 2.43/1.79 % (2647557)Instructions burned: 119 (million)
% 2.43/1.79 % (2647559)Instruction limit reached!
% 2.43/1.79 % (2647559)------------------------------
% 2.43/1.79 % (2647559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.43/1.79 % (2647559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.43/1.79 % (2647559)CaDiCaL version: 2.1.3
% 2.43/1.79 % (2647559)Termination reason: Instruction limit
% 2.43/1.79 % (2647559)Termination phase: Preprocessing 3
% 2.43/1.79 % (2647559)Time elapsed: 0.099 s
% 2.43/1.79 % (2647559)Peak memory usage: 96 MB
% 2.43/1.79 % (2647559)Instructions burned: 130 (million)
% 2.43/1.79 % (2647567)lrs+10_1_sil=8000:sp=occurrence:random_seed=175952994:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 2.43/1.79 % (2647568)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2174649516:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 2.43/1.79 % (2647567)Instruction limit reached!
% 2.43/1.79 % (2647567)------------------------------
% 2.43/1.79 % (2647567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.43/1.79 % (2647567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.43/1.79 % (2647567)CaDiCaL version: 2.1.3
% 2.43/1.79 % (2647567)Termination reason: Instruction limit
% 2.43/1.79 % (2647567)Termination phase: Saturation
% 2.43/1.79 % (2647567)Time elapsed: 0.101 s
% 2.43/1.79 % (2647567)Peak memory usage: 98 MB
% 2.43/1.79 % (2647567)Instructions burned: 285 (million)
% 2.43/1.79 % (2647570)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1790392971:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 2.43/1.79 % (2647556)------------------------------
% 2.43/1.79 % (2647556)------------------------------
% 2.43/1.79 % (2647570)First to succeed.
% 2.43/1.79 % (2647570)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2647548"
% 2.43/1.79 % (2647568)Instruction limit reached!
% 2.43/1.79 % (2647568)------------------------------
% 2.43/1.79 % (2647568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.43/1.79 % (2647568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.43/1.79 % (2647568)CaDiCaL version: 2.1.3
% 2.43/1.79 % (2647568)Termination reason: Instruction limit
% 2.43/1.79 % (2647568)Termination phase: Saturation
% 2.43/1.79 % (2647568)Time elapsed: 0.087 s
% 2.43/1.79 % (2647568)Peak memory usage: 95 MB
% 2.43/1.79 % (2647568)Instructions burned: 158 (million)
% 2.43/1.79 % (2647572)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=3601801367:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 2.43/1.79 % (2647572)Instruction limit reached!
% 2.43/1.79 % (2647572)------------------------------
% 2.43/1.79 % (2647572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.43/1.79 % (2647572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.43/1.79 % (2647572)CaDiCaL version: 2.1.3
% 2.43/1.79 % (2647572)Termination reason: Instruction limit
% 2.43/1.79 % (2647572)Termination phase: Preprocessing 3
% 2.43/1.79 % (2647572)Time elapsed: 0.090 s
% 2.43/1.79 % (2647572)Peak memory usage: 100 MB
% 2.43/1.79 % (2647572)Instructions burned: 248 (million)
% 2.43/1.79 % (2647574)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=303072118:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 2.43/1.79 % (2647576)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3015276556:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 2.43/1.79 % (2647577)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3970005017:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 2.43/1.79 % (2647577)Instruction limit reached!
% 2.43/1.79 % (2647577)------------------------------
% 2.43/1.79 % (2647577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.43/1.79 % (2647577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.43/1.79 % (2647577)CaDiCaL version: 2.1.3
% 2.43/1.79 % (2647577)Termination reason: Instruction limit
% 2.43/1.79 % (2647577)Termination phase: Property scanning
% 2.43/1.79 % (2647577)Time elapsed: 0.043 s
% 2.43/1.79 % (2647577)Peak memory usage: 95 MB
% 2.43/1.79 % (2647577)Instructions burned: 117 (million)
% 2.43/1.79 % (2647570)Refutation found. Thanks to Tanya!
% 2.43/1.79 % SZS status Theorem for theBenchmark
% 2.43/1.79 % SZS output start Proof for theBenchmark
% See solution above
% 5.60/1.88 % (2647570)------------------------------
% 5.60/1.88 % (2647570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.88 % (2647570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.88 % (2647570)CaDiCaL version: 2.1.3
% 5.60/1.88 % (2647570)Termination reason: Refutation
% 5.60/1.88 % (2647570)Time elapsed: 0.059 s
% 5.60/1.88 % (2647570)Peak memory usage: 97 MB
% 5.60/1.88 % (2647570)Instructions burned: 80 (million)
% 5.60/1.88 % (2647570)------------------------------
% 5.60/1.88 % (2647570)------------------------------
% 5.60/1.88 % (2647548)Success in time 0.921 s
% 5.60/1.88 % Vampire exiting
%------------------------------------------------------------------------------