%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT296+4 : 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 : n003.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:38 AM UTC 2026
% Result : Theorem 24.14s 9.49s
% Output : Refutation 48.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 41
% Syntax : Number of formulae : 337 ( 56 unt; 29 def)
% Number of atoms : 1607 ( 161 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 2185 ( 915 ~;1056 |; 143 &)
% ( 35 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 30 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-3 aty)
% Number of variables : 184 ( 0 sgn 169 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18128,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(f18150,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( v16_lattices(X0)
<=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& r2_lattices(X0,X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d19_lattices) ).
fof(f18197,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( X2 = k7_lattices(X0,X1)
<=> r2_lattices(X0,X2,X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d21_lattices) ).
fof(f18227,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_subset_1(k7_lattices(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_lattices) ).
fof(f22747,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(f22752,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(f22779,axiom,
! [X0] :
( l3_lattices(X0)
=> k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_lattice2) ).
fof(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22852,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(f34657,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_filter_2) ).
fof(f34661,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1)
& l3_lattices(X1) )
=> ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( X2 = X4
& X3 = X5
& r2_lattices(X0,X2,X3) )
=> r2_lattices(X1,X4,X5) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_filter_2) ).
fof(f34662,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( X2 = X3
=> k7_lattices(X0,X2) = k7_lattices(X1,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_filter_2) ).
fof(f34663,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( X2 = X3
=> k7_lattices(X0,X2) = k7_lattices(X1,X3) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34662]) ).
fof(f34694,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,[],[f22752]) ).
fof(f34807,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34657]) ).
fof(f34808,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34807]) ).
fof(f34815,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( r2_lattices(X1,X4,X5)
| X2 != X4
| X3 != X5
| ~ r2_lattices(X0,X2,X3)
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(X1)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v15_lattices(X1)
| ~ v16_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34661]) ).
fof(f34816,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( r2_lattices(X1,X4,X5)
| X2 != X4
| X3 != X5
| ~ r2_lattices(X0,X2,X3)
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(X1)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v15_lattices(X1)
| ~ v16_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34815]) ).
fof(f34817,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k7_lattices(X0,X2) != k7_lattices(X1,X3)
& X2 = X3
& m1_subset_1(X3,u1_struct_0(X1)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
& g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34663]) ).
fof(f34818,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k7_lattices(X0,X2) != k7_lattices(X1,X3)
& X2 = X3
& m1_subset_1(X3,u1_struct_0(X1)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
& g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f34817]) ).
fof(f34923,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f34944,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22780]) ).
fof(f34945,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34944]) ).
fof(f34946,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22779]) ).
fof(f34947,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,[],[f34694]) ).
fof(f34948,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,[],[f34947]) ).
fof(f34949,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22747]) ).
fof(f34950,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34949]) ).
fof(f35200,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,[],[f18128]) ).
fof(f35201,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,[],[f35200]) ).
fof(f35204,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k7_lattices(X0,X1)
<=> r2_lattices(X0,X2,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18197]) ).
fof(f35205,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k7_lattices(X0,X1)
<=> r2_lattices(X0,X2,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35204]) ).
fof(f35206,plain,
! [X0] :
( ( v16_lattices(X0)
<=> ! [X1] :
( ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& r2_lattices(X0,X2,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18150]) ).
fof(f35207,plain,
! [X0] :
( ( v16_lattices(X0)
<=> ! [X1] :
( ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& r2_lattices(X0,X2,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35206]) ).
fof(f35224,plain,
! [X0,X1] :
( m1_subset_1(k7_lattices(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f18227]) ).
fof(f35225,plain,
! [X0,X1] :
( m1_subset_1(k7_lattices(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f35224]) ).
fof(f35250,plain,
( k7_lattices(sK4,sK6) != k7_lattices(sK5,sK7)
& sK6 = sK7
& m1_subset_1(sK7,u1_struct_0(sK5))
& m1_subset_1(sK6,u1_struct_0(sK4))
& g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4)) = g3_lattices(u1_struct_0(sK5),u2_lattices(sK5),u1_lattices(sK5))
& ~ v3_struct_0(sK5)
& v10_lattices(sK5)
& v17_lattices(sK5)
& l3_lattices(sK5)
& ~ v3_struct_0(sK4)
& v10_lattices(sK4)
& v17_lattices(sK4)
& l3_lattices(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6,sK7]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6),skolemize(X3,sK7)],[f34818]) ).
fof(f35435,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k7_lattices(X0,X1)
| ~ r2_lattices(X0,X2,X1) )
& ( r2_lattices(X0,X2,X1)
| k7_lattices(X0,X1) != X2 ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35205]) ).
fof(f35436,plain,
! [X0] :
( ( ( v16_lattices(X0)
| ? [X1] :
( ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_lattices(X0,X2,X1) )
& m1_subset_1(X1,u1_struct_0(X0)) ) )
& ( ! [X1] :
( ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& r2_lattices(X0,X2,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v16_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35207]) ).
fof(f35437,plain,
! [X0] :
( ( ( v16_lattices(X0)
| ? [X1] :
( ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_lattices(X0,X2,X1) )
& m1_subset_1(X1,u1_struct_0(X0)) ) )
& ( ! [X3] :
( ? [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
& r2_lattices(X0,X4,X3) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v16_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f35436]) ).
fof(f35438,plain,
! [X0] :
( ( ( v16_lattices(X0)
| ( ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_lattices(X0,X2,sK114(X0)) )
& m1_subset_1(sK114(X0),u1_struct_0(X0)) ) )
& ( ! [X3] :
( ( m1_subset_1(sK115(X0,X3),u1_struct_0(X0))
& r2_lattices(X0,sK115(X0,X3),X3) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v16_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK114,sK115]),skolemize(X1,sK114(X0)),skolemize(X4,sK115(X0,X3))],[f35437]) ).
fof(f35513,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = k1_lattice2(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34808]) ).
fof(f35520,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_lattices(X1,X4,X5)
| X2 != X4
| X3 != X5
| ~ r2_lattices(X0,X2,X3)
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v15_lattices(X1)
| ~ v16_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34816]) ).
fof(f35521,plain,
l3_lattices(sK4),
inference(cnf_transformation,[],[f35250]) ).
fof(f35522,plain,
v17_lattices(sK4),
inference(cnf_transformation,[],[f35250]) ).
fof(f35523,plain,
v10_lattices(sK4),
inference(cnf_transformation,[],[f35250]) ).
fof(f35524,plain,
~ v3_struct_0(sK4),
inference(cnf_transformation,[],[f35250]) ).
fof(f35525,plain,
l3_lattices(sK5),
inference(cnf_transformation,[],[f35250]) ).
fof(f35526,plain,
v17_lattices(sK5),
inference(cnf_transformation,[],[f35250]) ).
fof(f35527,plain,
v10_lattices(sK5),
inference(cnf_transformation,[],[f35250]) ).
fof(f35528,plain,
~ v3_struct_0(sK5),
inference(cnf_transformation,[],[f35250]) ).
fof(f35529,plain,
g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4)) = g3_lattices(u1_struct_0(sK5),u2_lattices(sK5),u1_lattices(sK5)),
inference(cnf_transformation,[],[f35250]) ).
fof(f35530,plain,
m1_subset_1(sK6,u1_struct_0(sK4)),
inference(cnf_transformation,[],[f35250]) ).
fof(f35531,plain,
m1_subset_1(sK7,u1_struct_0(sK5)),
inference(cnf_transformation,[],[f35250]) ).
fof(f35532,plain,
sK6 = sK7,
inference(cnf_transformation,[],[f35250]) ).
fof(f35533,plain,
k7_lattices(sK4,sK6) != k7_lattices(sK5,sK7),
inference(cnf_transformation,[],[f35250]) ).
fof(f35672,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34923]) ).
fof(f35695,plain,
! [X0] :
( u1_lattices(X0) = u2_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34945]) ).
fof(f35696,plain,
! [X0] :
( u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34945]) ).
fof(f35697,plain,
! [X0] :
( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34945]) ).
fof(f35698,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34946]) ).
fof(f35699,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34948]) ).
fof(f35708,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34950]) ).
fof(f36090,plain,
! [X0] :
( v16_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35201]) ).
fof(f36091,plain,
! [X0] :
( v15_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35201]) ).
fof(f36094,plain,
! [X0] :
( v11_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35201]) ).
fof(f36113,plain,
! [X2,X0,X1] :
( k7_lattices(X0,X1) = X2
| ~ r2_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35435]) ).
fof(f36114,plain,
! [X3,X0] :
( r2_lattices(X0,sK115(X0,X3),X3)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ v16_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35438]) ).
fof(f36115,plain,
! [X3,X0] :
( m1_subset_1(sK115(X0,X3),u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ v16_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35438]) ).
fof(f36134,plain,
! [X0,X1] :
( m1_subset_1(k7_lattices(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f35225]) ).
fof(f36143,plain,
k7_lattices(sK5,sK7) != k7_lattices(sK4,sK7),
inference(definition_unfolding,[],[f35533,f35532]) ).
fof(f36144,plain,
m1_subset_1(sK7,u1_struct_0(sK4)),
inference(definition_unfolding,[],[f35530,f35532]) ).
fof(f36171,plain,
! [X3,X0,X1,X4,X5] :
( r2_lattices(X1,X4,X5)
| X3 != X5
| ~ r2_lattices(X0,X4,X3)
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v15_lattices(X1)
| ~ v16_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f35520]) ).
fof(f36172,plain,
! [X0,X1,X4,X5] :
( r2_lattices(X1,X4,X5)
| ~ r2_lattices(X0,X4,X5)
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v15_lattices(X1)
| ~ v16_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f36171]) ).
fof(f36266,plain,
! [X2,X0,X1] :
( k7_lattices(X0,X1) = X2
| ~ r2_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f36113]) ).
fof(f36271,definition,
( spl127_1
<=> v3_struct_0(sK4) ),
introduced(definition,[new_symbols(definition,[spl127_1])],[avatar_definition]) ).
fof(f36273,plain,
( ~ v3_struct_0(sK4)
| spl127_1 ),
inference(avatar_component_clause,[],[f36271]) ).
fof(f36274,plain,
~ spl127_1,
inference(avatar_split_clause,[],[f35524,f36271]) ).
fof(f36276,definition,
( spl127_2
<=> v3_struct_0(sK5) ),
introduced(definition,[new_symbols(definition,[spl127_2])],[avatar_definition]) ).
fof(f36278,plain,
( ~ v3_struct_0(sK5)
| spl127_2 ),
inference(avatar_component_clause,[],[f36276]) ).
fof(f36279,plain,
~ spl127_2,
inference(avatar_split_clause,[],[f35528,f36276]) ).
fof(f36281,definition,
( spl127_3
<=> v10_lattices(sK4) ),
introduced(definition,[new_symbols(definition,[spl127_3])],[avatar_definition]) ).
fof(f36283,plain,
( v10_lattices(sK4)
| ~ spl127_3 ),
inference(avatar_component_clause,[],[f36281]) ).
fof(f36284,plain,
spl127_3,
inference(avatar_split_clause,[],[f35523,f36281]) ).
fof(f36286,definition,
( spl127_4
<=> v10_lattices(sK5) ),
introduced(definition,[new_symbols(definition,[spl127_4])],[avatar_definition]) ).
fof(f36288,plain,
( v10_lattices(sK5)
| ~ spl127_4 ),
inference(avatar_component_clause,[],[f36286]) ).
fof(f36289,plain,
spl127_4,
inference(avatar_split_clause,[],[f35527,f36286]) ).
fof(f36340,plain,
( g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4)) = k1_lattice2(k1_lattice2(sK4))
| ~ v10_lattices(sK4)
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(resolution,[],[f36273,f35513]) ).
fof(f36450,plain,
( u1_lattices(sK4) = u2_lattices(k1_lattice2(sK4))
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(resolution,[],[f36273,f35695]) ).
fof(f36451,plain,
( u2_lattices(sK4) = u1_lattices(k1_lattice2(sK4))
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(resolution,[],[f36273,f35696]) ).
fof(f36452,plain,
( u1_struct_0(sK4) = u1_struct_0(k1_lattice2(sK4))
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(resolution,[],[f36273,f35697]) ).
fof(f36453,plain,
( v10_lattices(k1_lattice2(sK4))
| ~ v10_lattices(sK4)
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(resolution,[],[f36273,f35699]) ).
fof(f36462,plain,
( ~ v3_struct_0(k1_lattice2(sK4))
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(resolution,[],[f36273,f35708]) ).
fof(f36579,plain,
( v16_lattices(sK4)
| ~ v17_lattices(sK4)
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(resolution,[],[f36273,f36090]) ).
fof(f36580,plain,
( v15_lattices(sK4)
| ~ v17_lattices(sK4)
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(resolution,[],[f36273,f36091]) ).
fof(f36583,plain,
( v11_lattices(sK4)
| ~ v17_lattices(sK4)
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(resolution,[],[f36273,f36094]) ).
fof(f36755,plain,
( v11_lattices(sK4)
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(forward_subsumption_resolution,[],[f36583,f35522]) ).
fof(f36758,plain,
( v15_lattices(sK4)
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(forward_subsumption_resolution,[],[f36580,f35522]) ).
fof(f36759,plain,
( v16_lattices(sK4)
| ~ l3_lattices(sK4)
| spl127_1 ),
inference(forward_subsumption_resolution,[],[f36579,f35522]) ).
fof(f36873,plain,
( ~ v3_struct_0(k1_lattice2(sK4))
| spl127_1 ),
inference(forward_subsumption_resolution,[],[f36462,f35521]) ).
fof(f36880,plain,
( v10_lattices(k1_lattice2(sK4))
| ~ l3_lattices(sK4)
| spl127_1
| ~ spl127_3 ),
inference(forward_subsumption_resolution,[],[f36453,f36283]) ).
fof(f36881,plain,
( u1_struct_0(sK4) = u1_struct_0(k1_lattice2(sK4))
| spl127_1 ),
inference(forward_subsumption_resolution,[],[f36452,f35521]) ).
fof(f36882,plain,
( u2_lattices(sK4) = u1_lattices(k1_lattice2(sK4))
| spl127_1 ),
inference(forward_subsumption_resolution,[],[f36451,f35521]) ).
fof(f36883,plain,
( u1_lattices(sK4) = u2_lattices(k1_lattice2(sK4))
| spl127_1 ),
inference(forward_subsumption_resolution,[],[f36450,f35521]) ).
fof(f36993,plain,
( g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4)) = k1_lattice2(k1_lattice2(sK4))
| ~ l3_lattices(sK4)
| spl127_1
| ~ spl127_3 ),
inference(forward_subsumption_resolution,[],[f36340,f36283]) ).
fof(f37103,plain,
( v11_lattices(sK4)
| spl127_1 ),
inference(forward_subsumption_resolution,[],[f36755,f35521]) ).
fof(f37106,plain,
( v15_lattices(sK4)
| spl127_1 ),
inference(forward_subsumption_resolution,[],[f36758,f35521]) ).
fof(f37107,plain,
( v16_lattices(sK4)
| spl127_1 ),
inference(forward_subsumption_resolution,[],[f36759,f35521]) ).
fof(f37191,plain,
( v10_lattices(k1_lattice2(sK4))
| spl127_1
| ~ spl127_3 ),
inference(forward_subsumption_resolution,[],[f36880,f35521]) ).
fof(f37300,plain,
( g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4)) = k1_lattice2(k1_lattice2(sK4))
| spl127_1
| ~ spl127_3 ),
inference(forward_subsumption_resolution,[],[f36993,f35521]) ).
fof(f37528,definition,
( spl127_5
<=> l3_lattices(sK4) ),
introduced(definition,[new_symbols(definition,[spl127_5])],[avatar_definition]) ).
fof(f37530,plain,
( l3_lattices(sK4)
| ~ spl127_5 ),
inference(avatar_component_clause,[],[f37528]) ).
fof(f37531,plain,
spl127_5,
inference(avatar_split_clause,[],[f35521,f37528]) ).
fof(f37582,plain,
( g3_lattices(u1_struct_0(sK5),u2_lattices(sK5),u1_lattices(sK5)) = k1_lattice2(k1_lattice2(sK5))
| ~ v10_lattices(sK5)
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(resolution,[],[f36278,f35513]) ).
fof(f37692,plain,
( u1_lattices(sK5) = u2_lattices(k1_lattice2(sK5))
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(resolution,[],[f36278,f35695]) ).
fof(f37693,plain,
( u2_lattices(sK5) = u1_lattices(k1_lattice2(sK5))
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(resolution,[],[f36278,f35696]) ).
fof(f37694,plain,
( u1_struct_0(sK5) = u1_struct_0(k1_lattice2(sK5))
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(resolution,[],[f36278,f35697]) ).
fof(f37695,plain,
( v10_lattices(k1_lattice2(sK5))
| ~ v10_lattices(sK5)
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(resolution,[],[f36278,f35699]) ).
fof(f37704,plain,
( ~ v3_struct_0(k1_lattice2(sK5))
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(resolution,[],[f36278,f35708]) ).
fof(f37821,plain,
( v16_lattices(sK5)
| ~ v17_lattices(sK5)
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(resolution,[],[f36278,f36090]) ).
fof(f37822,plain,
( v15_lattices(sK5)
| ~ v17_lattices(sK5)
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(resolution,[],[f36278,f36091]) ).
fof(f37825,plain,
( v11_lattices(sK5)
| ~ v17_lattices(sK5)
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(resolution,[],[f36278,f36094]) ).
fof(f37997,plain,
( v11_lattices(sK5)
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(forward_subsumption_resolution,[],[f37825,f35526]) ).
fof(f38000,plain,
( v15_lattices(sK5)
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(forward_subsumption_resolution,[],[f37822,f35526]) ).
fof(f38001,plain,
( v16_lattices(sK5)
| ~ l3_lattices(sK5)
| spl127_2 ),
inference(forward_subsumption_resolution,[],[f37821,f35526]) ).
fof(f38115,plain,
( ~ v3_struct_0(k1_lattice2(sK5))
| spl127_2 ),
inference(forward_subsumption_resolution,[],[f37704,f35525]) ).
fof(f38122,plain,
( v10_lattices(k1_lattice2(sK5))
| ~ l3_lattices(sK5)
| spl127_2
| ~ spl127_4 ),
inference(forward_subsumption_resolution,[],[f37695,f36288]) ).
fof(f38123,plain,
( u1_struct_0(sK5) = u1_struct_0(k1_lattice2(sK5))
| spl127_2 ),
inference(forward_subsumption_resolution,[],[f37694,f35525]) ).
fof(f38124,plain,
( u2_lattices(sK5) = u1_lattices(k1_lattice2(sK5))
| spl127_2 ),
inference(forward_subsumption_resolution,[],[f37693,f35525]) ).
fof(f38125,plain,
( u1_lattices(sK5) = u2_lattices(k1_lattice2(sK5))
| spl127_2 ),
inference(forward_subsumption_resolution,[],[f37692,f35525]) ).
fof(f38235,plain,
( g3_lattices(u1_struct_0(sK5),u2_lattices(sK5),u1_lattices(sK5)) = k1_lattice2(k1_lattice2(sK5))
| ~ l3_lattices(sK5)
| spl127_2
| ~ spl127_4 ),
inference(forward_subsumption_resolution,[],[f37582,f36288]) ).
fof(f38361,plain,
( v11_lattices(sK5)
| spl127_2 ),
inference(forward_subsumption_resolution,[],[f37997,f35525]) ).
fof(f38364,plain,
( v15_lattices(sK5)
| spl127_2 ),
inference(forward_subsumption_resolution,[],[f38000,f35525]) ).
fof(f38365,plain,
( v16_lattices(sK5)
| spl127_2 ),
inference(forward_subsumption_resolution,[],[f38001,f35525]) ).
fof(f38449,plain,
( v10_lattices(k1_lattice2(sK5))
| spl127_2
| ~ spl127_4 ),
inference(forward_subsumption_resolution,[],[f38122,f35525]) ).
fof(f38558,plain,
( g3_lattices(u1_struct_0(sK5),u2_lattices(sK5),u1_lattices(sK5)) = k1_lattice2(k1_lattice2(sK5))
| spl127_2
| ~ spl127_4 ),
inference(forward_subsumption_resolution,[],[f38235,f35525]) ).
fof(f38808,definition,
( spl127_6
<=> l3_lattices(sK5) ),
introduced(definition,[new_symbols(definition,[spl127_6])],[avatar_definition]) ).
fof(f38810,plain,
( l3_lattices(sK5)
| ~ spl127_6 ),
inference(avatar_component_clause,[],[f38808]) ).
fof(f38811,plain,
spl127_6,
inference(avatar_split_clause,[],[f35525,f38808]) ).
fof(f39600,definition,
( spl127_8
<=> m1_subset_1(sK7,u1_struct_0(sK4)) ),
introduced(definition,[new_symbols(definition,[spl127_8])],[avatar_definition]) ).
fof(f39602,plain,
( m1_subset_1(sK7,u1_struct_0(sK4))
| ~ spl127_8 ),
inference(avatar_component_clause,[],[f39600]) ).
fof(f39603,plain,
spl127_8,
inference(avatar_split_clause,[],[f36144,f39600]) ).
fof(f39707,plain,
( r2_lattices(sK4,sK115(sK4,sK7),sK7)
| ~ v16_lattices(sK4)
| v3_struct_0(sK4)
| ~ l3_lattices(sK4)
| ~ spl127_8 ),
inference(resolution,[],[f39602,f36114]) ).
fof(f39708,plain,
( m1_subset_1(sK115(sK4,sK7),u1_struct_0(sK4))
| ~ v16_lattices(sK4)
| v3_struct_0(sK4)
| ~ l3_lattices(sK4)
| ~ spl127_8 ),
inference(resolution,[],[f39602,f36115]) ).
fof(f39734,plain,
( m1_subset_1(k7_lattices(sK4,sK7),u1_struct_0(sK4))
| v3_struct_0(sK4)
| ~ l3_lattices(sK4)
| ~ spl127_8 ),
inference(resolution,[],[f39602,f36134]) ).
fof(f39767,plain,
( ! [X0,X1] :
( r2_lattices(X0,X1,sK7)
| ~ r2_lattices(sK4,X1,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK4))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(sK4)
| ~ v10_lattices(sK4)
| ~ v15_lattices(sK4)
| ~ v16_lattices(sK4)
| ~ l3_lattices(sK4) )
| ~ spl127_8 ),
inference(resolution,[],[f39602,f36172]) ).
fof(f39807,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) = X0
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| v3_struct_0(sK4)
| ~ v10_lattices(sK4)
| ~ v11_lattices(sK4)
| ~ v16_lattices(sK4)
| ~ l3_lattices(sK4) )
| ~ spl127_8 ),
inference(resolution,[],[f39602,f36266]) ).
fof(f39939,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) = X0
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| ~ v10_lattices(sK4)
| ~ v11_lattices(sK4)
| ~ v16_lattices(sK4)
| ~ l3_lattices(sK4) )
| spl127_1
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f39807,f36273]) ).
fof(f39978,plain,
( ! [X0,X1] :
( r2_lattices(X0,X1,sK7)
| ~ r2_lattices(sK4,X1,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK4))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(sK4)
| ~ v15_lattices(sK4)
| ~ v16_lattices(sK4)
| ~ l3_lattices(sK4) )
| spl127_1
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f39767,f36273]) ).
fof(f40011,plain,
( m1_subset_1(k7_lattices(sK4,sK7),u1_struct_0(sK4))
| ~ l3_lattices(sK4)
| spl127_1
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f39734,f36273]) ).
fof(f40036,plain,
( m1_subset_1(sK115(sK4,sK7),u1_struct_0(sK4))
| v3_struct_0(sK4)
| ~ l3_lattices(sK4)
| spl127_1
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f39708,f37107]) ).
fof(f40037,plain,
( r2_lattices(sK4,sK115(sK4,sK7),sK7)
| v3_struct_0(sK4)
| ~ l3_lattices(sK4)
| spl127_1
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f39707,f37107]) ).
fof(f40140,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) = X0
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| ~ v11_lattices(sK4)
| ~ v16_lattices(sK4)
| ~ l3_lattices(sK4) )
| spl127_1
| ~ spl127_3
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f39939,f36283]) ).
fof(f40179,plain,
( ! [X0,X1] :
( r2_lattices(X0,X1,sK7)
| ~ r2_lattices(sK4,X1,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK4))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v15_lattices(sK4)
| ~ v16_lattices(sK4)
| ~ l3_lattices(sK4) )
| spl127_1
| ~ spl127_3
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f39978,f36283]) ).
fof(f40212,plain,
( m1_subset_1(k7_lattices(sK4,sK7),u1_struct_0(sK4))
| spl127_1
| ~ spl127_5
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40011,f37530]) ).
fof(f40237,plain,
( m1_subset_1(sK115(sK4,sK7),u1_struct_0(sK4))
| ~ l3_lattices(sK4)
| spl127_1
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40036,f36273]) ).
fof(f40238,plain,
( r2_lattices(sK4,sK115(sK4,sK7),sK7)
| ~ l3_lattices(sK4)
| spl127_1
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40037,f36273]) ).
fof(f40339,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) = X0
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| ~ v16_lattices(sK4)
| ~ l3_lattices(sK4) )
| spl127_1
| ~ spl127_3
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40140,f37103]) ).
fof(f40378,plain,
( ! [X0,X1] :
( r2_lattices(X0,X1,sK7)
| ~ r2_lattices(sK4,X1,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK4))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v16_lattices(sK4)
| ~ l3_lattices(sK4) )
| spl127_1
| ~ spl127_3
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40179,f37106]) ).
fof(f40425,plain,
( m1_subset_1(sK115(sK4,sK7),u1_struct_0(sK4))
| spl127_1
| ~ spl127_5
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40237,f37530]) ).
fof(f40426,plain,
( r2_lattices(sK4,sK115(sK4,sK7),sK7)
| spl127_1
| ~ spl127_5
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40238,f37530]) ).
fof(f40497,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) = X0
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| ~ l3_lattices(sK4) )
| spl127_1
| ~ spl127_3
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40339,f37107]) ).
fof(f40523,plain,
( ! [X0,X1] :
( r2_lattices(X0,X1,sK7)
| ~ r2_lattices(sK4,X1,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK4))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ l3_lattices(sK4) )
| spl127_1
| ~ spl127_3
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40378,f37107]) ).
fof(f40576,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) = X0
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) )
| spl127_1
| ~ spl127_3
| ~ spl127_5
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40497,f37530]) ).
fof(f40581,plain,
( ! [X0,X1] :
( r2_lattices(X0,X1,sK7)
| ~ r2_lattices(sK4,X1,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK4))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) )
| spl127_1
| ~ spl127_3
| ~ spl127_5
| ~ spl127_8 ),
inference(forward_subsumption_resolution,[],[f40523,f37530]) ).
fof(f40591,plain,
( ! [X0,X1] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k1_lattice2(k1_lattice2(sK4))
| r2_lattices(X0,X1,sK7)
| ~ r2_lattices(sK4,X1,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK4))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) )
| spl127_1
| ~ spl127_3
| ~ spl127_5
| ~ spl127_8 ),
inference(forward_demodulation,[],[f40581,f37300]) ).
fof(f40602,definition,
( spl127_10
<=> m1_subset_1(sK7,u1_struct_0(sK5)) ),
introduced(definition,[new_symbols(definition,[spl127_10])],[avatar_definition]) ).
fof(f40604,plain,
( m1_subset_1(sK7,u1_struct_0(sK5))
| ~ spl127_10 ),
inference(avatar_component_clause,[],[f40602]) ).
fof(f40605,plain,
spl127_10,
inference(avatar_split_clause,[],[f35531,f40602]) ).
fof(f41786,plain,
( l3_lattices(k1_lattice2(sK5))
| ~ spl127_6 ),
inference(resolution,[],[f38810,f35672]) ).
fof(f41801,plain,
( k1_lattice2(sK5) = g3_lattices(u1_struct_0(sK5),u1_lattices(sK5),u2_lattices(sK5))
| ~ spl127_6 ),
inference(resolution,[],[f38810,f35698]) ).
fof(f42320,plain,
( l3_lattices(k1_lattice2(sK4))
| ~ spl127_5 ),
inference(resolution,[],[f37530,f35672]) ).
fof(f42335,plain,
( k1_lattice2(sK4) = g3_lattices(u1_struct_0(sK4),u1_lattices(sK4),u2_lattices(sK4))
| ~ spl127_5 ),
inference(resolution,[],[f37530,f35698]) ).
fof(f42698,definition,
( spl127_11
<=> k7_lattices(sK5,sK7) = k7_lattices(sK4,sK7) ),
introduced(definition,[new_symbols(definition,[spl127_11])],[avatar_definition]) ).
fof(f42700,plain,
( k7_lattices(sK5,sK7) != k7_lattices(sK4,sK7)
| spl127_11 ),
inference(avatar_component_clause,[],[f42698]) ).
fof(f42701,plain,
~ spl127_11,
inference(avatar_split_clause,[],[f36143,f42698]) ).
fof(f42702,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) != X0
| ~ r2_lattices(sK5,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK5))
| v3_struct_0(sK5)
| ~ v10_lattices(sK5)
| ~ v11_lattices(sK5)
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5)
| ~ m1_subset_1(sK7,u1_struct_0(sK5)) )
| spl127_11 ),
inference(superposition,[],[f42700,f36266]) ).
fof(f42703,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) != X0
| ~ r2_lattices(sK5,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK5))
| ~ v10_lattices(sK5)
| ~ v11_lattices(sK5)
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5)
| ~ m1_subset_1(sK7,u1_struct_0(sK5)) )
| spl127_2
| spl127_11 ),
inference(forward_subsumption_resolution,[],[f42702,f36278]) ).
fof(f42704,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) != X0
| ~ r2_lattices(sK5,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK5))
| ~ v11_lattices(sK5)
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5)
| ~ m1_subset_1(sK7,u1_struct_0(sK5)) )
| spl127_2
| ~ spl127_4
| spl127_11 ),
inference(forward_subsumption_resolution,[],[f42703,f36288]) ).
fof(f42705,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) != X0
| ~ r2_lattices(sK5,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK5))
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5)
| ~ m1_subset_1(sK7,u1_struct_0(sK5)) )
| spl127_2
| ~ spl127_4
| spl127_11 ),
inference(forward_subsumption_resolution,[],[f42704,f38361]) ).
fof(f42706,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) != X0
| ~ r2_lattices(sK5,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK5))
| ~ l3_lattices(sK5)
| ~ m1_subset_1(sK7,u1_struct_0(sK5)) )
| spl127_2
| ~ spl127_4
| spl127_11 ),
inference(forward_subsumption_resolution,[],[f42705,f38365]) ).
fof(f42707,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) != X0
| ~ r2_lattices(sK5,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK5))
| ~ m1_subset_1(sK7,u1_struct_0(sK5)) )
| spl127_2
| ~ spl127_4
| ~ spl127_6
| spl127_11 ),
inference(forward_subsumption_resolution,[],[f42706,f38810]) ).
fof(f42708,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) != X0
| ~ r2_lattices(sK5,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK5)) )
| spl127_2
| ~ spl127_4
| ~ spl127_6
| ~ spl127_10
| spl127_11 ),
inference(forward_subsumption_resolution,[],[f42707,f40604]) ).
fof(f42710,definition,
( spl127_12
<=> g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4)) = g3_lattices(u1_struct_0(sK5),u2_lattices(sK5),u1_lattices(sK5)) ),
introduced(definition,[new_symbols(definition,[spl127_12])],[avatar_definition]) ).
fof(f42712,plain,
( g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4)) = g3_lattices(u1_struct_0(sK5),u2_lattices(sK5),u1_lattices(sK5))
| ~ spl127_12 ),
inference(avatar_component_clause,[],[f42710]) ).
fof(f42713,plain,
spl127_12,
inference(avatar_split_clause,[],[f35529,f42710]) ).
fof(f42714,plain,
( g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4)) = k1_lattice2(k1_lattice2(sK5))
| spl127_2
| ~ spl127_4
| ~ spl127_12 ),
inference(forward_demodulation,[],[f42712,f38558]) ).
fof(f42715,plain,
( k1_lattice2(k1_lattice2(sK4)) = k1_lattice2(k1_lattice2(sK5))
| spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_12 ),
inference(forward_demodulation,[],[f42714,f37300]) ).
fof(f42717,definition,
( spl127_13
<=> ! [X0] :
( k7_lattices(sK4,sK7) != X0
| ~ r2_lattices(sK5,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK5)) ) ),
introduced(definition,[new_symbols(definition,[spl127_13])],[avatar_definition]) ).
fof(f42718,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) != X0
| ~ r2_lattices(sK5,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK5)) )
| ~ spl127_13 ),
inference(avatar_component_clause,[],[f42717]) ).
fof(f42719,plain,
( spl127_13
| spl127_2
| ~ spl127_4
| ~ spl127_6
| ~ spl127_10
| spl127_11 ),
inference(avatar_split_clause,[],[f42708,f42698,f40602,f38808,f36286,f36276,f42717]) ).
fof(f42725,plain,
( ~ r2_lattices(sK5,k7_lattices(sK4,sK7),sK7)
| ~ m1_subset_1(k7_lattices(sK4,sK7),u1_struct_0(sK5))
| ~ spl127_13 ),
inference(equality_resolution,[],[f42718]) ).
fof(f42733,definition,
( spl127_15
<=> m1_subset_1(k7_lattices(sK4,sK7),u1_struct_0(sK5)) ),
introduced(definition,[new_symbols(definition,[spl127_15])],[avatar_definition]) ).
fof(f42735,plain,
( ~ m1_subset_1(k7_lattices(sK4,sK7),u1_struct_0(sK5))
| spl127_15 ),
inference(avatar_component_clause,[],[f42733]) ).
fof(f42737,definition,
( spl127_16
<=> r2_lattices(sK5,k7_lattices(sK4,sK7),sK7) ),
introduced(definition,[new_symbols(definition,[spl127_16])],[avatar_definition]) ).
fof(f42739,plain,
( ~ r2_lattices(sK5,k7_lattices(sK4,sK7),sK7)
| spl127_16 ),
inference(avatar_component_clause,[],[f42737]) ).
fof(f42740,plain,
( ~ spl127_15
| ~ spl127_16
| ~ spl127_13 ),
inference(avatar_split_clause,[],[f42725,f42717,f42737,f42733]) ).
fof(f42912,definition,
( spl127_22
<=> u2_lattices(sK5) = u1_lattices(k1_lattice2(sK5)) ),
introduced(definition,[new_symbols(definition,[spl127_22])],[avatar_definition]) ).
fof(f42914,plain,
( u2_lattices(sK5) = u1_lattices(k1_lattice2(sK5))
| ~ spl127_22 ),
inference(avatar_component_clause,[],[f42912]) ).
fof(f42915,plain,
( spl127_22
| spl127_2 ),
inference(avatar_split_clause,[],[f38124,f36276,f42912]) ).
fof(f42917,definition,
( spl127_23
<=> u2_lattices(sK4) = u1_lattices(k1_lattice2(sK4)) ),
introduced(definition,[new_symbols(definition,[spl127_23])],[avatar_definition]) ).
fof(f42919,plain,
( u2_lattices(sK4) = u1_lattices(k1_lattice2(sK4))
| ~ spl127_23 ),
inference(avatar_component_clause,[],[f42917]) ).
fof(f42920,plain,
( spl127_23
| spl127_1 ),
inference(avatar_split_clause,[],[f36882,f36271,f42917]) ).
fof(f43048,definition,
( spl127_25
<=> u1_struct_0(sK5) = u1_struct_0(k1_lattice2(sK5)) ),
introduced(definition,[new_symbols(definition,[spl127_25])],[avatar_definition]) ).
fof(f43050,plain,
( u1_struct_0(sK5) = u1_struct_0(k1_lattice2(sK5))
| ~ spl127_25 ),
inference(avatar_component_clause,[],[f43048]) ).
fof(f43051,plain,
( spl127_25
| spl127_2 ),
inference(avatar_split_clause,[],[f38123,f36276,f43048]) ).
fof(f43582,definition,
( spl127_27
<=> u1_struct_0(sK4) = u1_struct_0(k1_lattice2(sK4)) ),
introduced(definition,[new_symbols(definition,[spl127_27])],[avatar_definition]) ).
fof(f43584,plain,
( u1_struct_0(sK4) = u1_struct_0(k1_lattice2(sK4))
| ~ spl127_27 ),
inference(avatar_component_clause,[],[f43582]) ).
fof(f43585,plain,
( spl127_27
| spl127_1 ),
inference(avatar_split_clause,[],[f36881,f36271,f43582]) ).
fof(f43783,definition,
( spl127_29
<=> u1_lattices(sK5) = u2_lattices(k1_lattice2(sK5)) ),
introduced(definition,[new_symbols(definition,[spl127_29])],[avatar_definition]) ).
fof(f43785,plain,
( u1_lattices(sK5) = u2_lattices(k1_lattice2(sK5))
| ~ spl127_29 ),
inference(avatar_component_clause,[],[f43783]) ).
fof(f43786,plain,
( spl127_29
| spl127_2 ),
inference(avatar_split_clause,[],[f38125,f36276,f43783]) ).
fof(f44388,definition,
( spl127_31
<=> u1_lattices(sK4) = u2_lattices(k1_lattice2(sK4)) ),
introduced(definition,[new_symbols(definition,[spl127_31])],[avatar_definition]) ).
fof(f44390,plain,
( u1_lattices(sK4) = u2_lattices(k1_lattice2(sK4))
| ~ spl127_31 ),
inference(avatar_component_clause,[],[f44388]) ).
fof(f44391,plain,
( spl127_31
| spl127_1 ),
inference(avatar_split_clause,[],[f36883,f36271,f44388]) ).
fof(f44858,definition,
( spl127_36
<=> m1_subset_1(k7_lattices(sK4,sK7),u1_struct_0(sK4)) ),
introduced(definition,[new_symbols(definition,[spl127_36])],[avatar_definition]) ).
fof(f44860,plain,
( m1_subset_1(k7_lattices(sK4,sK7),u1_struct_0(sK4))
| ~ spl127_36 ),
inference(avatar_component_clause,[],[f44858]) ).
fof(f44861,plain,
( spl127_36
| spl127_1
| ~ spl127_5
| ~ spl127_8 ),
inference(avatar_split_clause,[],[f40212,f39600,f37528,f36271,f44858]) ).
fof(f47053,definition,
( spl127_42
<=> ! [X0] :
( k7_lattices(sK4,sK7) = X0
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) ) ),
introduced(definition,[new_symbols(definition,[spl127_42])],[avatar_definition]) ).
fof(f47054,plain,
( ! [X0] :
( k7_lattices(sK4,sK7) = X0
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) )
| ~ spl127_42 ),
inference(avatar_component_clause,[],[f47053]) ).
fof(f47055,plain,
( spl127_42
| spl127_1
| ~ spl127_3
| ~ spl127_5
| ~ spl127_8 ),
inference(avatar_split_clause,[],[f40576,f39600,f37528,f36281,f36271,f47053]) ).
fof(f47135,plain,
( g3_lattices(u1_struct_0(k1_lattice2(sK5)),u2_lattices(k1_lattice2(sK5)),u2_lattices(sK5)) = k1_lattice2(k1_lattice2(k1_lattice2(sK5)))
| v3_struct_0(k1_lattice2(sK5))
| ~ v10_lattices(k1_lattice2(sK5))
| ~ l3_lattices(k1_lattice2(sK5))
| ~ spl127_22 ),
inference(superposition,[],[f35513,f42914]) ).
fof(f47220,plain,
( g3_lattices(u1_struct_0(k1_lattice2(sK5)),u2_lattices(k1_lattice2(sK5)),u2_lattices(sK5)) = k1_lattice2(k1_lattice2(k1_lattice2(sK5)))
| ~ v10_lattices(k1_lattice2(sK5))
| ~ l3_lattices(k1_lattice2(sK5))
| spl127_2
| ~ spl127_22 ),
inference(forward_subsumption_resolution,[],[f47135,f38115]) ).
fof(f47264,plain,
( g3_lattices(u1_struct_0(k1_lattice2(sK5)),u2_lattices(k1_lattice2(sK5)),u2_lattices(sK5)) = k1_lattice2(k1_lattice2(k1_lattice2(sK5)))
| ~ l3_lattices(k1_lattice2(sK5))
| spl127_2
| ~ spl127_4
| ~ spl127_22 ),
inference(forward_subsumption_resolution,[],[f47220,f38449]) ).
fof(f47308,plain,
( g3_lattices(u1_struct_0(k1_lattice2(sK5)),u2_lattices(k1_lattice2(sK5)),u2_lattices(sK5)) = k1_lattice2(k1_lattice2(k1_lattice2(sK5)))
| spl127_2
| ~ spl127_4
| ~ spl127_6
| ~ spl127_22 ),
inference(forward_subsumption_resolution,[],[f47264,f41786]) ).
fof(f47351,plain,
( g3_lattices(u1_struct_0(k1_lattice2(sK5)),u2_lattices(k1_lattice2(sK5)),u2_lattices(sK5)) = k1_lattice2(k1_lattice2(k1_lattice2(sK4)))
| spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_6
| ~ spl127_12
| ~ spl127_22 ),
inference(forward_demodulation,[],[f47308,f42715]) ).
fof(f47389,plain,
( g3_lattices(u1_struct_0(k1_lattice2(sK5)),u1_lattices(sK5),u2_lattices(sK5)) = k1_lattice2(k1_lattice2(k1_lattice2(sK4)))
| spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_6
| ~ spl127_12
| ~ spl127_22
| ~ spl127_29 ),
inference(forward_demodulation,[],[f47351,f43785]) ).
fof(f47422,plain,
( g3_lattices(u1_struct_0(sK5),u1_lattices(sK5),u2_lattices(sK5)) = k1_lattice2(k1_lattice2(k1_lattice2(sK4)))
| spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_6
| ~ spl127_12
| ~ spl127_22
| ~ spl127_25
| ~ spl127_29 ),
inference(forward_demodulation,[],[f47389,f43050]) ).
fof(f47447,plain,
( k1_lattice2(sK5) = k1_lattice2(k1_lattice2(k1_lattice2(sK4)))
| spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_6
| ~ spl127_12
| ~ spl127_22
| ~ spl127_25
| ~ spl127_29 ),
inference(forward_demodulation,[],[f47422,f41801]) ).
fof(f47458,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK4))) = g3_lattices(u1_struct_0(k1_lattice2(sK4)),u2_lattices(k1_lattice2(sK4)),u2_lattices(sK4))
| v3_struct_0(k1_lattice2(sK4))
| ~ v10_lattices(k1_lattice2(sK4))
| ~ l3_lattices(k1_lattice2(sK4))
| ~ spl127_23 ),
inference(superposition,[],[f35513,f42919]) ).
fof(f47543,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK4))) = g3_lattices(u1_struct_0(k1_lattice2(sK4)),u2_lattices(k1_lattice2(sK4)),u2_lattices(sK4))
| ~ v10_lattices(k1_lattice2(sK4))
| ~ l3_lattices(k1_lattice2(sK4))
| spl127_1
| ~ spl127_23 ),
inference(forward_subsumption_resolution,[],[f47458,f36873]) ).
fof(f47587,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK4))) = g3_lattices(u1_struct_0(k1_lattice2(sK4)),u2_lattices(k1_lattice2(sK4)),u2_lattices(sK4))
| ~ l3_lattices(k1_lattice2(sK4))
| spl127_1
| ~ spl127_3
| ~ spl127_23 ),
inference(forward_subsumption_resolution,[],[f47543,f37191]) ).
fof(f47631,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK4))) = g3_lattices(u1_struct_0(k1_lattice2(sK4)),u2_lattices(k1_lattice2(sK4)),u2_lattices(sK4))
| spl127_1
| ~ spl127_3
| ~ spl127_5
| ~ spl127_23 ),
inference(forward_subsumption_resolution,[],[f47587,f42320]) ).
fof(f47672,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK4))) = g3_lattices(u1_struct_0(k1_lattice2(sK4)),u1_lattices(sK4),u2_lattices(sK4))
| spl127_1
| ~ spl127_3
| ~ spl127_5
| ~ spl127_23
| ~ spl127_31 ),
inference(forward_demodulation,[],[f47631,f44390]) ).
fof(f47710,plain,
( g3_lattices(u1_struct_0(sK4),u1_lattices(sK4),u2_lattices(sK4)) = k1_lattice2(k1_lattice2(k1_lattice2(sK4)))
| spl127_1
| ~ spl127_3
| ~ spl127_5
| ~ spl127_23
| ~ spl127_27
| ~ spl127_31 ),
inference(forward_demodulation,[],[f47672,f43584]) ).
fof(f47741,plain,
( k1_lattice2(sK5) = g3_lattices(u1_struct_0(sK4),u1_lattices(sK4),u2_lattices(sK4))
| spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_5
| ~ spl127_6
| ~ spl127_12
| ~ spl127_22
| ~ spl127_23
| ~ spl127_25
| ~ spl127_27
| ~ spl127_29
| ~ spl127_31 ),
inference(forward_demodulation,[],[f47710,f47447]) ).
fof(f47766,plain,
( k1_lattice2(sK4) = k1_lattice2(sK5)
| spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_5
| ~ spl127_6
| ~ spl127_12
| ~ spl127_22
| ~ spl127_23
| ~ spl127_25
| ~ spl127_27
| ~ spl127_29
| ~ spl127_31 ),
inference(forward_demodulation,[],[f47741,f42335]) ).
fof(f48558,definition,
( spl127_49
<=> v16_lattices(sK5) ),
introduced(definition,[new_symbols(definition,[spl127_49])],[avatar_definition]) ).
fof(f48560,plain,
( v16_lattices(sK5)
| ~ spl127_49 ),
inference(avatar_component_clause,[],[f48558]) ).
fof(f48561,plain,
( spl127_49
| spl127_2 ),
inference(avatar_split_clause,[],[f38365,f36276,f48558]) ).
fof(f55400,definition,
( spl127_70
<=> v15_lattices(sK5) ),
introduced(definition,[new_symbols(definition,[spl127_70])],[avatar_definition]) ).
fof(f55402,plain,
( v15_lattices(sK5)
| ~ spl127_70 ),
inference(avatar_component_clause,[],[f55400]) ).
fof(f55403,plain,
( spl127_70
| spl127_2 ),
inference(avatar_split_clause,[],[f38364,f36276,f55400]) ).
fof(f55448,plain,
( ! [X0] :
( ~ r2_lattices(sK5,X0,sK7)
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) )
| spl127_16
| ~ spl127_42 ),
inference(superposition,[],[f42739,f47054]) ).
fof(f70906,definition,
( spl127_157
<=> ! [X0] :
( ~ r2_lattices(sK5,X0,sK7)
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) ) ),
introduced(definition,[new_symbols(definition,[spl127_157])],[avatar_definition]) ).
fof(f70907,plain,
( ! [X0] :
( ~ r2_lattices(sK5,X0,sK7)
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) )
| ~ spl127_157 ),
inference(avatar_component_clause,[],[f70906]) ).
fof(f70908,plain,
( spl127_157
| spl127_16
| ~ spl127_42 ),
inference(avatar_split_clause,[],[f55448,f47053,f42737,f70906]) ).
fof(f72180,definition,
( spl127_172
<=> ! [X0,X1] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k1_lattice2(k1_lattice2(sK4))
| r2_lattices(X0,X1,sK7)
| ~ r2_lattices(sK4,X1,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK4))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ) ),
introduced(definition,[new_symbols(definition,[spl127_172])],[avatar_definition]) ).
fof(f72181,plain,
( ! [X0,X1] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k1_lattice2(k1_lattice2(sK4))
| r2_lattices(X0,X1,sK7)
| ~ r2_lattices(sK4,X1,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK4))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) )
| ~ spl127_172 ),
inference(avatar_component_clause,[],[f72180]) ).
fof(f72182,plain,
( spl127_172
| spl127_1
| ~ spl127_3
| ~ spl127_5
| ~ spl127_8 ),
inference(avatar_split_clause,[],[f40591,f39600,f37528,f36281,f36271,f72180]) ).
fof(f72667,definition,
( spl127_180
<=> r2_lattices(sK4,sK115(sK4,sK7),sK7) ),
introduced(definition,[new_symbols(definition,[spl127_180])],[avatar_definition]) ).
fof(f72669,plain,
( r2_lattices(sK4,sK115(sK4,sK7),sK7)
| ~ spl127_180 ),
inference(avatar_component_clause,[],[f72667]) ).
fof(f72670,plain,
( spl127_180
| spl127_1
| ~ spl127_5
| ~ spl127_8 ),
inference(avatar_split_clause,[],[f40426,f39600,f37528,f36271,f72667]) ).
fof(f82021,definition,
( spl127_260
<=> ! [X0] :
( ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) ) ),
introduced(definition,[new_symbols(definition,[spl127_260])],[avatar_definition]) ).
fof(f82022,plain,
( ! [X0] :
( ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) )
| ~ spl127_260 ),
inference(avatar_component_clause,[],[f82021]) ).
fof(f83598,definition,
( spl127_287
<=> k1_lattice2(sK4) = k1_lattice2(sK5) ),
introduced(definition,[new_symbols(definition,[spl127_287])],[avatar_definition]) ).
fof(f83600,plain,
( k1_lattice2(sK4) = k1_lattice2(sK5)
| ~ spl127_287 ),
inference(avatar_component_clause,[],[f83598]) ).
fof(f83601,plain,
( spl127_287
| spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_5
| ~ spl127_6
| ~ spl127_12
| ~ spl127_22
| ~ spl127_23
| ~ spl127_25
| ~ spl127_27
| ~ spl127_29
| ~ spl127_31 ),
inference(avatar_split_clause,[],[f47766,f44388,f43783,f43582,f43048,f42917,f42912,f42710,f38808,f37528,f36286,f36281,f36276,f36271,f83598]) ).
fof(f83604,plain,
( u1_struct_0(sK5) = u1_struct_0(k1_lattice2(sK4))
| ~ spl127_25
| ~ spl127_287 ),
inference(superposition,[],[f43050,f83600]) ).
fof(f83605,plain,
( u1_lattices(sK5) = u2_lattices(k1_lattice2(sK4))
| ~ spl127_29
| ~ spl127_287 ),
inference(superposition,[],[f43785,f83600]) ).
fof(f83606,plain,
( u2_lattices(sK5) = u1_lattices(k1_lattice2(sK4))
| ~ spl127_22
| ~ spl127_287 ),
inference(superposition,[],[f42914,f83600]) ).
fof(f83705,plain,
( u2_lattices(sK4) = u2_lattices(sK5)
| ~ spl127_22
| ~ spl127_23
| ~ spl127_287 ),
inference(forward_demodulation,[],[f83606,f42919]) ).
fof(f83706,plain,
( u1_lattices(sK4) = u1_lattices(sK5)
| ~ spl127_29
| ~ spl127_31
| ~ spl127_287 ),
inference(forward_demodulation,[],[f83605,f44390]) ).
fof(f83707,plain,
( u1_struct_0(sK5) = u1_struct_0(sK4)
| ~ spl127_25
| ~ spl127_27
| ~ spl127_287 ),
inference(forward_demodulation,[],[f83604,f43584]) ).
fof(f83779,definition,
( spl127_288
<=> u1_struct_0(sK5) = u1_struct_0(sK4) ),
introduced(definition,[new_symbols(definition,[spl127_288])],[avatar_definition]) ).
fof(f83781,plain,
( u1_struct_0(sK5) = u1_struct_0(sK4)
| ~ spl127_288 ),
inference(avatar_component_clause,[],[f83779]) ).
fof(f83782,plain,
( spl127_288
| ~ spl127_25
| ~ spl127_27
| ~ spl127_287 ),
inference(avatar_split_clause,[],[f83707,f83598,f43582,f43048,f83779]) ).
fof(f83785,plain,
( ~ m1_subset_1(k7_lattices(sK4,sK7),u1_struct_0(sK4))
| spl127_15
| ~ spl127_288 ),
inference(superposition,[],[f42735,f83781]) ).
fof(f84245,plain,
( ! [X0] :
( k1_lattice2(k1_lattice2(sK4)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK5),u1_lattices(sK5))
| r2_lattices(sK5,X0,sK7)
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(sK4))
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| v3_struct_0(sK5)
| ~ v10_lattices(sK5)
| ~ v15_lattices(sK5)
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5) )
| ~ spl127_172
| ~ spl127_288 ),
inference(superposition,[],[f72181,f83781]) ).
fof(f84268,plain,
( ! [X0] :
( k1_lattice2(k1_lattice2(sK4)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK5),u1_lattices(sK5))
| r2_lattices(sK5,X0,sK7)
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(sK4))
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| v3_struct_0(sK5)
| ~ v10_lattices(sK5)
| ~ v15_lattices(sK5)
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5) )
| ~ spl127_172
| ~ spl127_288 ),
inference(duplicate_literal_removal,[],[f84245]) ).
fof(f84288,plain,
( ! [X0] :
( k1_lattice2(k1_lattice2(sK4)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK5),u1_lattices(sK5))
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(sK7,u1_struct_0(sK4))
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| v3_struct_0(sK5)
| ~ v10_lattices(sK5)
| ~ v15_lattices(sK5)
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5) )
| ~ spl127_157
| ~ spl127_172
| ~ spl127_288 ),
inference(forward_subsumption_resolution,[],[f84268,f70907]) ).
fof(f84705,plain,
( $false
| spl127_15
| ~ spl127_36
| ~ spl127_288 ),
inference(forward_subsumption_resolution,[],[f83785,f44860]) ).
fof(f84706,plain,
( spl127_15
| ~ spl127_36
| ~ spl127_288 ),
inference(avatar_contradiction_clause,[],[f84705]) ).
fof(f84717,plain,
( ! [X0] :
( k1_lattice2(k1_lattice2(sK4)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK5),u1_lattices(sK5))
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| v3_struct_0(sK5)
| ~ v10_lattices(sK5)
| ~ v15_lattices(sK5)
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5) )
| ~ spl127_8
| ~ spl127_157
| ~ spl127_172
| ~ spl127_288 ),
inference(forward_subsumption_resolution,[],[f84288,f39602]) ).
fof(f85128,plain,
( ! [X0] :
( k1_lattice2(k1_lattice2(sK4)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK5),u1_lattices(sK5))
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| ~ v10_lattices(sK5)
| ~ v15_lattices(sK5)
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5) )
| spl127_2
| ~ spl127_8
| ~ spl127_157
| ~ spl127_172
| ~ spl127_288 ),
inference(forward_subsumption_resolution,[],[f84717,f36278]) ).
fof(f85492,plain,
( ! [X0] :
( k1_lattice2(k1_lattice2(sK4)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK5),u1_lattices(sK5))
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| ~ v15_lattices(sK5)
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5) )
| spl127_2
| ~ spl127_4
| ~ spl127_8
| ~ spl127_157
| ~ spl127_172
| ~ spl127_288 ),
inference(forward_subsumption_resolution,[],[f85128,f36288]) ).
fof(f85724,plain,
( ! [X0] :
( k1_lattice2(k1_lattice2(sK4)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK5),u1_lattices(sK5))
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| ~ v16_lattices(sK5)
| ~ l3_lattices(sK5) )
| spl127_2
| ~ spl127_4
| ~ spl127_8
| ~ spl127_70
| ~ spl127_157
| ~ spl127_172
| ~ spl127_288 ),
inference(forward_subsumption_resolution,[],[f85492,f55402]) ).
fof(f85877,plain,
( ! [X0] :
( k1_lattice2(k1_lattice2(sK4)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK5),u1_lattices(sK5))
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4))
| ~ l3_lattices(sK5) )
| spl127_2
| ~ spl127_4
| ~ spl127_8
| ~ spl127_49
| ~ spl127_70
| ~ spl127_157
| ~ spl127_172
| ~ spl127_288 ),
inference(forward_subsumption_resolution,[],[f85724,f48560]) ).
fof(f85937,plain,
( ! [X0] :
( k1_lattice2(k1_lattice2(sK4)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK5),u1_lattices(sK5))
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) )
| spl127_2
| ~ spl127_4
| ~ spl127_6
| ~ spl127_8
| ~ spl127_49
| ~ spl127_70
| ~ spl127_157
| ~ spl127_172
| ~ spl127_288 ),
inference(forward_subsumption_resolution,[],[f85877,f38810]) ).
fof(f85973,plain,
( ! [X0] :
( k1_lattice2(k1_lattice2(sK4)) != g3_lattices(u1_struct_0(sK4),u2_lattices(sK5),u1_lattices(sK4))
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) )
| spl127_2
| ~ spl127_4
| ~ spl127_6
| ~ spl127_8
| ~ spl127_29
| ~ spl127_31
| ~ spl127_49
| ~ spl127_70
| ~ spl127_157
| ~ spl127_172
| ~ spl127_287
| ~ spl127_288 ),
inference(forward_demodulation,[],[f85937,f83706]) ).
fof(f86000,plain,
( ! [X0] :
( g3_lattices(u1_struct_0(sK4),u2_lattices(sK4),u1_lattices(sK4)) != k1_lattice2(k1_lattice2(sK4))
| ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) )
| spl127_2
| ~ spl127_4
| ~ spl127_6
| ~ spl127_8
| ~ spl127_22
| ~ spl127_23
| ~ spl127_29
| ~ spl127_31
| ~ spl127_49
| ~ spl127_70
| ~ spl127_157
| ~ spl127_172
| ~ spl127_287
| ~ spl127_288 ),
inference(forward_demodulation,[],[f85973,f83705]) ).
fof(f86004,plain,
( ! [X0] :
( ~ r2_lattices(sK4,X0,sK7)
| ~ m1_subset_1(X0,u1_struct_0(sK4)) )
| spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_6
| ~ spl127_8
| ~ spl127_22
| ~ spl127_23
| ~ spl127_29
| ~ spl127_31
| ~ spl127_49
| ~ spl127_70
| ~ spl127_157
| ~ spl127_172
| ~ spl127_287
| ~ spl127_288 ),
inference(forward_subsumption_resolution,[],[f86000,f37300]) ).
fof(f87383,plain,
( spl127_260
| spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_6
| ~ spl127_8
| ~ spl127_22
| ~ spl127_23
| ~ spl127_29
| ~ spl127_31
| ~ spl127_49
| ~ spl127_70
| ~ spl127_157
| ~ spl127_172
| ~ spl127_287
| ~ spl127_288 ),
inference(avatar_split_clause,[],[f86004,f83779,f83598,f72180,f70906,f55400,f48558,f44388,f43783,f42917,f42912,f39600,f38808,f36286,f36281,f36276,f36271,f82021]) ).
fof(f87541,plain,
( ~ m1_subset_1(sK115(sK4,sK7),u1_struct_0(sK4))
| ~ spl127_180
| ~ spl127_260 ),
inference(resolution,[],[f82022,f72669]) ).
fof(f87559,plain,
( $false
| spl127_1
| ~ spl127_5
| ~ spl127_8
| ~ spl127_180
| ~ spl127_260 ),
inference(forward_subsumption_resolution,[],[f87541,f40425]) ).
fof(f87560,plain,
( spl127_1
| ~ spl127_5
| ~ spl127_8
| ~ spl127_180
| ~ spl127_260 ),
inference(avatar_contradiction_clause,[],[f87559]) ).
cnf(s1,plain,
~ spl127_1,
inference(sat_conversion,[],[f36274]) ).
cnf(s2,plain,
~ spl127_2,
inference(sat_conversion,[],[f36279]) ).
cnf(s3,plain,
spl127_3,
inference(sat_conversion,[],[f36284]) ).
cnf(s4,plain,
spl127_4,
inference(sat_conversion,[],[f36289]) ).
cnf(s5,plain,
spl127_5,
inference(sat_conversion,[],[f37531]) ).
cnf(s6,plain,
spl127_6,
inference(sat_conversion,[],[f38811]) ).
cnf(s8,plain,
spl127_8,
inference(sat_conversion,[],[f39603]) ).
cnf(s10,plain,
spl127_10,
inference(sat_conversion,[],[f40605]) ).
cnf(s11,plain,
~ spl127_11,
inference(sat_conversion,[],[f42701]) ).
cnf(s12,plain,
spl127_12,
inference(sat_conversion,[],[f42713]) ).
cnf(s13,plain,
( spl127_2
| ~ spl127_4
| ~ spl127_6
| ~ spl127_10
| spl127_11
| spl127_13 ),
inference(sat_conversion,[],[f42719]) ).
cnf(s15,plain,
( ~ spl127_13
| ~ spl127_15
| ~ spl127_16 ),
inference(sat_conversion,[],[f42740]) ).
cnf(s21,plain,
( spl127_2
| spl127_22 ),
inference(sat_conversion,[],[f42915]) ).
cnf(s22,plain,
( spl127_1
| spl127_23 ),
inference(sat_conversion,[],[f42920]) ).
cnf(s24,plain,
( spl127_2
| spl127_25 ),
inference(sat_conversion,[],[f43051]) ).
cnf(s26,plain,
( spl127_1
| spl127_27 ),
inference(sat_conversion,[],[f43585]) ).
cnf(s28,plain,
( spl127_2
| spl127_29 ),
inference(sat_conversion,[],[f43786]) ).
cnf(s30,plain,
( spl127_1
| spl127_31 ),
inference(sat_conversion,[],[f44391]) ).
cnf(s35,plain,
( spl127_1
| ~ spl127_5
| ~ spl127_8
| spl127_36 ),
inference(sat_conversion,[],[f44861]) ).
cnf(s41,plain,
( spl127_1
| ~ spl127_3
| ~ spl127_5
| ~ spl127_8
| spl127_42 ),
inference(sat_conversion,[],[f47055]) ).
cnf(s48,plain,
( spl127_2
| spl127_49 ),
inference(sat_conversion,[],[f48561]) ).
cnf(s68,plain,
( spl127_2
| spl127_70 ),
inference(sat_conversion,[],[f55403]) ).
cnf(s155,plain,
( spl127_16
| ~ spl127_42
| spl127_157 ),
inference(sat_conversion,[],[f70908]) ).
cnf(s169,plain,
( spl127_1
| ~ spl127_3
| ~ spl127_5
| ~ spl127_8
| spl127_172 ),
inference(sat_conversion,[],[f72182]) ).
cnf(s177,plain,
( spl127_1
| ~ spl127_5
| ~ spl127_8
| spl127_180 ),
inference(sat_conversion,[],[f72670]) ).
cnf(s303,plain,
( spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_5
| ~ spl127_6
| ~ spl127_12
| ~ spl127_22
| ~ spl127_23
| ~ spl127_25
| ~ spl127_27
| ~ spl127_29
| ~ spl127_31
| spl127_287 ),
inference(sat_conversion,[],[f83601]) ).
cnf(s304,plain,
( ~ spl127_25
| ~ spl127_27
| ~ spl127_287
| spl127_288 ),
inference(sat_conversion,[],[f83782]) ).
cnf(s307,plain,
( spl127_15
| ~ spl127_36
| ~ spl127_288 ),
inference(sat_conversion,[],[f84706]) ).
cnf(s317,plain,
( spl127_1
| spl127_2
| ~ spl127_3
| ~ spl127_4
| ~ spl127_6
| ~ spl127_8
| ~ spl127_22
| ~ spl127_23
| ~ spl127_29
| ~ spl127_31
| ~ spl127_49
| ~ spl127_70
| ~ spl127_157
| ~ spl127_172
| spl127_260
| ~ spl127_287
| ~ spl127_288 ),
inference(sat_conversion,[],[f87383]) ).
cnf(s320,plain,
( spl127_1
| ~ spl127_5
| ~ spl127_8
| ~ spl127_180
| ~ spl127_260 ),
inference(sat_conversion,[],[f87560]) ).
cnf(s390,plain,
spl127_70,
inference(rat,[],[s68,s2]) ).
cnf(s399,plain,
spl127_49,
inference(rat,[],[s48,s2]) ).
cnf(s408,plain,
spl127_29,
inference(rat,[],[s28,s2]) ).
cnf(s410,plain,
spl127_25,
inference(rat,[],[s24,s2]) ).
cnf(s411,plain,
spl127_22,
inference(rat,[],[s21,s2]) ).
cnf(s415,plain,
spl127_13,
inference(rat,[],[s13,s4,s11,s10,s6,s2]) ).
cnf(s473,plain,
spl127_180,
inference(rat,[],[s177,s5,s8,s1]) ).
cnf(s478,plain,
spl127_172,
inference(rat,[],[s169,s3,s8,s5,s1]) ).
cnf(s532,plain,
spl127_42,
inference(rat,[],[s41,s3,s8,s5,s1]) ).
cnf(s535,plain,
spl127_36,
inference(rat,[],[s35,s5,s8,s1]) ).
cnf(s537,plain,
spl127_31,
inference(rat,[],[s30,s1]) ).
cnf(s539,plain,
spl127_27,
inference(rat,[],[s26,s1]) ).
cnf(s541,plain,
spl127_23,
inference(rat,[],[s22,s1]) ).
cnf(s545,plain,
~ spl127_260,
inference(rat,[],[s320,s1,s5,s8,s473]) ).
cnf(s555,plain,
spl127_287,
inference(rat,[],[s303,s539,s537,s408,s1,s410,s411,s2,s12,s6,s5,s4,s3,s541]) ).
cnf(s569,plain,
spl127_288,
inference(rat,[],[s304,s539,s410,s555]) ).
cnf(s570,plain,
~ spl127_157,
inference(rat,[],[s317,s569,s541,s545,s478,s537,s390,s399,s1,s408,s411,s2,s8,s6,s4,s3,s555]) ).
cnf(s577,plain,
spl127_15,
inference(rat,[],[s307,s535,s569]) ).
cnf(s580,plain,
spl127_16,
inference(rat,[],[s155,s532,s570]) ).
cnf(s585,plain,
$false,
inference(rat,[],[s15,s415,s580,s577]) ).
fof(f87594,plain,
$false,
inference(avatar_sat_refutation,[],[s585]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT296+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n003.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 14:22:02 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/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
% 15.43/4.94 % (586070)Detected formulas, will run a generic FOF schedule.
% 15.43/4.94 % (586080)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3617965553:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 15.43/4.94 % (586079)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3229815762:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 15.43/4.94 % (586078)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=76606574:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 15.43/4.94 % (586076)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=3750213112:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 15.43/4.94 % (586077)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=36294618:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 15.43/4.94 % (586082)dis-21_1_sil=8000:lcm=predicate:random_seed=162748491:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 15.43/4.94 % (586081)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=459584861:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 15.43/4.94 % (586080)Instruction limit reached!
% 15.43/4.94 % (586080)------------------------------
% 15.43/4.94 % (586080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.43/4.94 % (586080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/4.94 % (586080)CaDiCaL version: 2.1.3
% 15.43/4.94 % (586080)Termination reason: Instruction limit
% 15.43/4.94 % (586080)Termination phase: SInE selection
% 15.43/4.94 % (586080)Time elapsed: 0.054 s
% 15.43/4.94 % (586080)Peak memory usage: 136 MB
% 15.43/4.94 % (586080)Instructions burned: 121 (million)
% 15.43/4.94 % (586081)Instruction limit reached!
% 15.43/4.94 % (586081)------------------------------
% 15.43/4.94 % (586081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.43/4.94 % (586081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/4.94 % (586081)CaDiCaL version: 2.1.3
% 15.43/4.94 % (586081)Termination reason: Instruction limit
% 15.43/4.94 % (586081)Termination phase: Property scanning
% 15.43/4.94 % (586081)Time elapsed: 0.062 s
% 15.43/4.94 % (586081)Peak memory usage: 136 MB
% 15.43/4.94 % (586081)Instructions burned: 140 (million)
% 15.43/4.94 % (586079)Instruction limit reached!
% 15.43/4.94 % (586079)------------------------------
% 15.43/4.94 % (586079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.43/4.94 % (586079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/4.94 % (586079)CaDiCaL version: 2.1.3
% 15.43/4.94 % (586079)Termination reason: Instruction limit
% 15.43/4.94 % (586079)Termination phase: SInE selection
% 15.43/4.94 % (586079)Time elapsed: 0.081 s
% 15.43/4.94 % (586079)Peak memory usage: 136 MB
% 15.43/4.94 % (586079)Instructions burned: 110 (million)
% 15.43/4.94 % (586082)Instruction limit reached!
% 15.43/4.94 % (586082)------------------------------
% 15.43/4.94 % (586082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.43/4.94 % (586082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/4.94 % (586082)CaDiCaL version: 2.1.3
% 15.43/4.94 % (586082)Termination reason: Instruction limit
% 15.43/4.94 % (586082)Termination phase: SInE selection
% 15.43/4.94 % (586082)Time elapsed: 0.093 s
% 15.43/4.94 % (586082)Peak memory usage: 136 MB
% 15.43/4.94 % (586082)Instructions burned: 130 (million)
% 15.43/4.94 % (586090)lrs+10_1_sil=8000:sp=occurrence:random_seed=2673678195:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 15.43/4.94 % (586091)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1303222668:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 15.43/4.94 % (586092)lrs+1011_1_sil=32000:sp=occurrence:random_seed=895411262:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 15.43/4.94 % (586093)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=70799144:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 15.43/4.94 % (586090)Instruction limit reached!
% 15.43/4.94 % (586090)------------------------------
% 25.08/6.20 % (586090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.08/6.20 % (586090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.08/6.20 % (586090)CaDiCaL version: 2.1.3
% 25.08/6.20 % (586090)Termination reason: Instruction limit
% 25.08/6.20 % (586090)Termination phase: Saturation
% 25.08/6.20 % (586090)Time elapsed: 0.131 s
% 25.08/6.20 % (586090)Peak memory usage: 141 MB
% 25.08/6.20 % (586090)Instructions burned: 287 (million)
% 25.08/6.20 % (586091)Instruction limit reached!
% 25.08/6.20 % (586091)------------------------------
% 25.08/6.20 % (586091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.08/6.20 % (586091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.08/6.20 % (586091)CaDiCaL version: 2.1.3
% 25.08/6.20 % (586091)Termination reason: Instruction limit
% 25.08/6.20 % (586091)Termination phase: Property scanning
% 25.08/6.20 % (586091)Time elapsed: 0.071 s
% 25.08/6.20 % (586091)Peak memory usage: 136 MB
% 25.08/6.20 % (586091)Instructions burned: 159 (million)
% 25.08/6.20 % (586093)Instruction limit reached!
% 25.08/6.20 % (586093)------------------------------
% 25.08/6.20 % (586093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.08/6.20 % (586093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.08/6.20 % (586093)CaDiCaL version: 2.1.3
% 25.08/6.20 % (586093)Termination reason: Instruction limit
% 25.08/6.20 % (586093)Termination phase: Property scanning
% 25.08/6.20 % (586093)Time elapsed: 0.106 s
% 25.08/6.20 % (586093)Peak memory usage: 136 MB
% 25.08/6.20 % (586093)Instructions burned: 248 (million)
% 25.08/6.20 % (586098)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4179650376:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 25.08/6.20 % (586099)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2909242298:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 25.08/6.20 % (586092)Instruction limit reached!
% 25.08/6.20 % (586092)------------------------------
% 25.08/6.20 % (586092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.08/6.20 % (586092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.08/6.20 % (586092)CaDiCaL version: 2.1.3
% 25.08/6.20 % (586092)Termination reason: Instruction limit
% 25.08/6.20 % (586092)Termination phase: Saturation
% 25.08/6.20 % (586092)Time elapsed: 0.260 s
% 25.08/6.20 % (586092)Peak memory usage: 142 MB
% 25.08/6.20 % (586092)Instructions burned: 326 (million)
% 25.08/6.20 % (586098)Instruction limit reached!
% 25.08/6.20 % (586098)------------------------------
% 25.08/6.20 % (586098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.08/6.20 % (586098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.08/6.20 % (586098)CaDiCaL version: 2.1.3
% 25.08/6.20 % (586098)Termination reason: Instruction limit
% 25.08/6.20 % (586098)Termination phase: SInE selection
% 25.08/6.20 % (586098)Time elapsed: 0.109 s
% 25.08/6.20 % (586098)Peak memory usage: 137 MB
% 25.08/6.20 % (586098)Instructions burned: 297 (million)
% 25.08/6.20 % (586100)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=694367648:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 25.08/6.20 % (586100)Instruction limit reached!
% 25.08/6.20 % (586100)------------------------------
% 25.08/6.20 % (586100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.08/6.20 % (586100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.08/6.20 % (586100)CaDiCaL version: 2.1.3
% 25.08/6.20 % (586100)Termination reason: Instruction limit
% 25.08/6.20 % (586100)Termination phase: SInE selection
% 25.08/6.20 % (586100)Time elapsed: 0.087 s
% 25.08/6.20 % (586100)Peak memory usage: 136 MB
% 25.08/6.20 % (586100)Instructions burned: 113 (million)
% 25.08/6.20 % (586105)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3288690597:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2971 on theBenchmark for (2971ds/114Mi)
% 25.08/6.20 % (586103)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1695373168:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 25.08/6.20 % (586105)Instruction limit reached!
% 25.08/6.20 % (586105)------------------------------
% 25.08/6.20 % (586105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.08/6.20 % (586105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586105)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586105)Termination reason: Instruction limit
% 24.14/9.49 % (586105)Termination phase: Property scanning
% 24.14/9.49 % (586105)Time elapsed: 0.029 s
% 24.14/9.49 % (586105)Peak memory usage: 136 MB
% 24.14/9.49 % (586105)Instructions burned: 119 (million)
% 24.14/9.49 % (586103)Instruction limit reached!
% 24.14/9.49 % (586103)------------------------------
% 24.14/9.49 % (586103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586103)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586103)Termination reason: Instruction limit
% 24.14/9.49 % (586103)Termination phase: Preprocessing 1
% 24.14/9.49 % (586103)Time elapsed: 0.096 s
% 24.14/9.49 % (586103)Peak memory usage: 137 MB
% 24.14/9.49 % (586103)Instructions burned: 128 (million)
% 24.14/9.49 % (586106)lrs+10_1_sil=8000:sp=occurrence:random_seed=1075124889:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2970 on theBenchmark for (2970ds/907Mi)
% 24.14/9.49 % (586109)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3031039575:i=437:sd=1:aac=none:ss=included_2969 on theBenchmark for (2969ds/437Mi)
% 24.14/9.49 % (586110)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=360560565:i=5202:ss=axioms:sgt=16_2969 on theBenchmark for (2969ds/5202Mi)
% 24.14/9.49 % (586109)Instruction limit reached!
% 24.14/9.49 % (586109)------------------------------
% 24.14/9.49 % (586109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586109)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586109)Termination reason: Instruction limit
% 24.14/9.49 % (586109)Termination phase: Saturation
% 24.14/9.49 % (586109)Time elapsed: 0.169 s
% 24.14/9.49 % (586109)Peak memory usage: 143 MB
% 24.14/9.49 % (586109)Instructions burned: 440 (million)
% 24.14/9.49 % (586114)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3777253305:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2966 on theBenchmark for (2966ds/134Mi)
% 24.14/9.49 % (586114)Instruction limit reached!
% 24.14/9.49 % (586114)------------------------------
% 24.14/9.49 % (586114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586114)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586114)Termination reason: Instruction limit
% 24.14/9.49 % (586114)Termination phase: SInE selection
% 24.14/9.49 % (586114)Time elapsed: 0.060 s
% 24.14/9.49 % (586114)Peak memory usage: 136 MB
% 24.14/9.49 % (586114)Instructions burned: 137 (million)
% 24.14/9.49 % (586116)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1869210402:st=8:i=592:sd=3:ep=RST:ss=axioms_2964 on theBenchmark for (2964ds/592Mi)
% 24.14/9.49 % (586106)Instruction limit reached!
% 24.14/9.49 % (586106)------------------------------
% 24.14/9.49 % (586106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586106)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586106)Termination reason: Instruction limit
% 24.14/9.49 % (586106)Termination phase: Function definition elimination
% 24.14/9.49 % (586106)Time elapsed: 0.576 s
% 24.14/9.49 % (586106)Peak memory usage: 155 MB
% 24.14/9.49 % (586106)Instructions burned: 907 (million)
% 24.14/9.49 % (586118)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1360641848:st=3:i=13193:sd=3:ss=axioms_2963 on theBenchmark for (2963ds/13193Mi)
% 24.14/9.49 % (586116)Instruction limit reached!
% 24.14/9.49 % (586116)------------------------------
% 24.14/9.49 % (586116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586116)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586116)Termination reason: Instruction limit
% 24.14/9.49 % (586116)Termination phase: Preprocessing 2
% 24.14/9.49 % (586116)Time elapsed: 0.267 s
% 24.14/9.49 % (586116)Peak memory usage: 154 MB
% 24.14/9.49 % (586116)Instructions burned: 592 (million)
% 24.14/9.49 % (586120)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=426059704:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/125Mi)
% 24.14/9.49 % (586120)Instruction limit reached!
% 24.14/9.49 % (586120)------------------------------
% 24.14/9.49 % (586120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586120)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586120)Termination reason: Instruction limit
% 24.14/9.49 % (586120)Termination phase: Property scanning
% 24.14/9.49 % (586120)Time elapsed: 0.031 s
% 24.14/9.49 % (586120)Peak memory usage: 136 MB
% 24.14/9.49 % (586120)Instructions burned: 127 (million)
% 24.14/9.49 % (586122)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2065606799:i=134:gtgl=5:slsql=off:gtg=exists_sym_2959 on theBenchmark for (2959ds/134Mi)
% 24.14/9.49 % (586122)Instruction limit reached!
% 24.14/9.49 % (586122)------------------------------
% 24.14/9.49 % (586122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586122)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586122)Termination reason: Instruction limit
% 24.14/9.49 % (586122)Termination phase: Property scanning
% 24.14/9.49 % (586122)Time elapsed: 0.032 s
% 24.14/9.49 % (586122)Peak memory usage: 136 MB
% 24.14/9.49 % (586122)Instructions burned: 136 (million)
% 24.14/9.49 % (586124)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2551451347:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2957 on theBenchmark for (2957ds/141Mi)
% 24.14/9.49 % (586099)Instruction limit reached!
% 24.14/9.49 % (586099)------------------------------
% 24.14/9.49 % (586099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586099)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586099)Termination reason: Instruction limit
% 24.14/9.49 % (586099)Termination phase: Property scanning
% 24.14/9.49 % (586099)Time elapsed: 1.565 s
% 24.14/9.49 % (586099)Peak memory usage: 233 MB
% 24.14/9.49 % (586099)Instructions burned: 2351 (million)
% 24.14/9.49 % (586124)Instruction limit reached!
% 24.14/9.49 % (586124)------------------------------
% 24.14/9.49 % (586124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586124)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586124)Termination reason: Instruction limit
% 24.14/9.49 % (586124)Termination phase: SInE selection
% 24.14/9.49 % (586124)Time elapsed: 0.061 s
% 24.14/9.49 % (586124)Peak memory usage: 136 MB
% 24.14/9.49 % (586124)Instructions burned: 143 (million)
% 24.14/9.49 % (586126)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1501358912:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2956 on theBenchmark for (2956ds/431Mi)
% 24.14/9.49 % (586127)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1599368231:i=6060:aac=none:ins=25_2955 on theBenchmark for (2955ds/6060Mi)
% 24.14/9.49 % (586126)Refutation not found, incomplete strategy
% 24.14/9.49 % (586126)------------------------------
% 24.14/9.49 % (586126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586126)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586126)Termination reason: Refutation not found, incomplete strategy
% 24.14/9.49 % (586126)Time elapsed: 0.204 s
% 24.14/9.49 % (586126)Peak memory usage: 142 MB
% 24.14/9.49 % (586126)Instructions burned: 248 (million)
% 24.14/9.49 % (586126)------------------------------
% 24.14/9.49 % (586126)------------------------------
% 24.14/9.49 % (586130)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=997263043:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2949 on theBenchmark for (2949ds/150Mi)
% 24.14/9.49 % (586130)Instruction limit reached!
% 24.14/9.49 % (586130)------------------------------
% 24.14/9.49 % (586130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586130)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586130)Termination reason: Instruction limit
% 24.14/9.49 % (586130)Termination phase: SInE selection
% 24.14/9.49 % (586130)Time elapsed: 0.115 s
% 24.14/9.49 % (586130)Peak memory usage: 136 MB
% 24.14/9.49 % (586130)Instructions burned: 151 (million)
% 24.14/9.49 % (586132)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1879069515:i=14155:bd=all_2946 on theBenchmark for (2946ds/14155Mi)
% 24.14/9.49 % (586110)Instruction limit reached!
% 24.14/9.49 % (586110)------------------------------
% 24.14/9.49 % (586110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586110)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586110)Termination reason: Instruction limit
% 24.14/9.49 % (586110)Termination phase: Saturation
% 24.14/9.49 % (586110)Time elapsed: 3.199 s
% 24.14/9.49 % (586110)Peak memory usage: 241 MB
% 24.14/9.49 % (586110)Instructions burned: 5203 (million)
% 24.14/9.49 % (586134)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1394211207:i=667:av=off:fsr=off_2935 on theBenchmark for (2935ds/667Mi)
% 24.14/9.49 % (586127)Instruction limit reached!
% 24.14/9.49 % (586127)------------------------------
% 24.14/9.49 % (586127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586127)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586127)Termination reason: Instruction limit
% 24.14/9.49 % (586127)Termination phase: Function definition elimination
% 24.14/9.49 % (586127)Time elapsed: 2.142 s
% 24.14/9.49 % (586127)Peak memory usage: 244 MB
% 24.14/9.49 % (586127)Instructions burned: 6066 (million)
% 24.14/9.49 % (586136)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1765961821:s2a=on:i=185:s2at=1.8:fdi=4_2932 on theBenchmark for (2932ds/185Mi)
% 24.14/9.49 % (586136)Instruction limit reached!
% 24.14/9.49 % (586136)------------------------------
% 24.14/9.49 % (586136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586136)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586136)Termination reason: Instruction limit
% 24.14/9.49 % (586136)Termination phase: SInE selection
% 24.14/9.49 % (586136)Time elapsed: 0.073 s
% 24.14/9.49 % (586136)Peak memory usage: 136 MB
% 24.14/9.49 % (586136)Instructions burned: 187 (million)
% 24.14/9.49 % (586138)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3822350997:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2930 on theBenchmark for (2930ds/193Mi)
% 24.14/9.49 % (586138)Instruction limit reached!
% 24.14/9.49 % (586138)------------------------------
% 24.14/9.49 % (586138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586138)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586138)Termination reason: Instruction limit
% 24.14/9.49 % (586138)Termination phase: SInE selection
% 24.14/9.49 % (586138)Time elapsed: 0.090 s
% 24.14/9.49 % (586138)Peak memory usage: 136 MB
% 24.14/9.49 % (586138)Instructions burned: 195 (million)
% 24.14/9.49 % (586134)Instruction limit reached!
% 24.14/9.49 % (586134)------------------------------
% 24.14/9.49 % (586134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.14/9.49 % (586134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.14/9.49 % (586134)CaDiCaL version: 2.1.3
% 24.14/9.49 % (586134)Termination reason: Instruction limit
% 24.14/9.49 % (586134)Termination phase: NewCNF
% 24.14/9.49 % (586134)Time elapsed: 0.532 s
% 24.14/9.49 % (586134)Peak memory usage: 185 MB
% 24.14/9.49 % (586134)Instructions burned: 667 (million)
% 24.14/9.49 % (586140)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4082059644:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2928 on theBenchmark for (2928ds/4850Mi)
% 24.14/9.49 % (586141)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3969804061:i=12111:sd=1:ss=included_2928 on theBenchmark for (2928ds/12111Mi)
% 24.14/9.49 % (586078)First to succeed.
% 24.14/9.49 % (586078)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-586070"
% 24.14/9.49 % (586078)Refutation found. Thanks to Tanya!
% 24.14/9.49 % SZS status Theorem for theBenchmark
% 24.14/9.49 % SZS output start Proof for theBenchmark
% See solution above
% 48.28/9.75 % (586078)------------------------------
% 48.28/9.75 % (586078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.28/9.75 % (586078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.28/9.75 % (586078)CaDiCaL version: 2.1.3
% 48.28/9.75 % (586078)Termination reason: Refutation
% 48.28/9.75 % (586078)Time elapsed: 5.901 s
% 48.28/9.75 % (586078)Peak memory usage: 248 MB
% 48.28/9.75 % (586078)Instructions burned: 9732 (million)
% 48.28/9.75 % (586078)------------------------------
% 48.28/9.75 % (586078)------------------------------
% 48.28/9.75 % (586070)Success in time 8.627 s
% 48.28/9.75 % Vampire exiting
%------------------------------------------------------------------------------