%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT299+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 : n001.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:40 AM UTC 2026
% Result : Theorem 23.95s 12.12s
% Output : Refutation 66.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 51
% Syntax : Number of formulae : 361 ( 78 unt; 41 def)
% Number of atoms : 1990 ( 144 equ)
% Maximal formula atoms : 23 ( 5 avg)
% Number of connectives : 2807 (1178 ~;1447 |; 109 &)
% ( 40 <=>; 31 =>; 0 <=; 2 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 43 ( 41 usr; 34 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 11 con; 0-3 aty)
% Number of variables : 263 ( 0 sgn 243 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f68,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
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(f22816,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
=> ( ( X1 = X3
& X2 = X4 )
=> ( k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),X3,X4)
& k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),X3,X4) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t52_lattice2) ).
fof(f31985,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f34607,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f34656,axiom,
! [X0] :
( l3_lattices(X0)
=> ! [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))
=> k1_lattice2(X0) = k1_lattice2(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_filter_2) ).
fof(f34666,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( m2_filter_2(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k3_lattices(X0,X2,X3),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_filter_2) ).
fof(f34667,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k3_lattices(X0,X2,X3),X1) ) ) )
=> m2_filter_2(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_filter_2) ).
fof(f34669,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_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] :
( m2_filter_2(X2,X0)
=> m2_filter_2(X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_filter_2) ).
fof(f34670,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_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] :
( m2_filter_2(X2,X0)
=> m2_filter_2(X2,X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34669]) ).
fof(f34716,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34607]) ).
fof(f34717,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34716]) ).
fof(f34813,plain,
! [X0] :
( ! [X1] :
( k1_lattice2(X0) = k1_lattice2(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))
| ~ l3_lattices(X1) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34656]) ).
fof(f34814,plain,
! [X0] :
( ! [X1] :
( k1_lattice2(X0) = k1_lattice2(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))
| ~ l3_lattices(X1) )
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34813]) ).
fof(f34831,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k3_lattices(X0,X2,X3),X1) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34666]) ).
fof(f34832,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k3_lattices(X0,X2,X3),X1) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34831]) ).
fof(f34833,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<~> r2_hidden(k3_lattices(X0,X2,X3),X1) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34667]) ).
fof(f34834,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<~> r2_hidden(k3_lattices(X0,X2,X3),X1) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34833]) ).
fof(f34837,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m2_filter_2(X2,X1)
& m2_filter_2(X2,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)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34670]) ).
fof(f34838,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m2_filter_2(X2,X1)
& m2_filter_2(X2,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)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f34837]) ).
fof(f34845,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f34848,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f31985]) ).
fof(f34849,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34848]) ).
fof(f34960,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),X3,X4)
& k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),X3,X4) )
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22816]) ).
fof(f34961,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),X3,X4)
& k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),X3,X4) )
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34960]) ).
fof(f34964,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(f34965,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,[],[f34964]) ).
fof(f35309,plain,
! [X0] :
( ! [X1] :
( ( ( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k3_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
| ~ r2_hidden(k3_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m2_filter_2(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f34832]) ).
fof(f35310,plain,
! [X0] :
( ! [X1] :
( ( ( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k3_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
| ~ r2_hidden(k3_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m2_filter_2(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35309]) ).
fof(f35311,plain,
! [X0] :
( ! [X1] :
( ( ( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k3_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( ( ( r2_hidden(X4,X1)
& r2_hidden(X5,X1) )
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1) )
& ( r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1) ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m2_filter_2(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f35310]) ).
fof(f35312,plain,
! [X0] :
( ! [X1] :
( ( ( m2_filter_2(X1,X0)
| ( ( ~ r2_hidden(k3_lattices(X0,sK15(X0,X1),sK16(X0,X1)),X1)
| ~ r2_hidden(sK15(X0,X1),X1)
| ~ r2_hidden(sK16(X0,X1),X1) )
& ( r2_hidden(k3_lattices(X0,sK15(X0,X1),sK16(X0,X1)),X1)
| ( r2_hidden(sK15(X0,X1),X1)
& r2_hidden(sK16(X0,X1),X1) ) )
& m1_subset_1(sK16(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK15(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( ( ( r2_hidden(X4,X1)
& r2_hidden(X5,X1) )
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1) )
& ( r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1) ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m2_filter_2(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X2,sK15(X0,X1)),skolemize(X3,sK16(X0,X1))],[f35311]) ).
fof(f35313,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k3_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f34834]) ).
fof(f35314,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k3_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35313]) ).
fof(f35315,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
| ( ( ~ r2_hidden(k3_lattices(X0,sK17(X0,X1),sK18(X0,X1)),X1)
| ~ r2_hidden(sK17(X0,X1),X1)
| ~ r2_hidden(sK18(X0,X1),X1) )
& ( r2_hidden(k3_lattices(X0,sK17(X0,X1),sK18(X0,X1)),X1)
| ( r2_hidden(sK17(X0,X1),X1)
& r2_hidden(sK18(X0,X1),X1) ) )
& m1_subset_1(sK18(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK17(X0,X1),u1_struct_0(X0)) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18]),skolemize(X2,sK17(X0,X1)),skolemize(X3,sK18(X0,X1))],[f35314]) ).
fof(f35316,plain,
( ~ m2_filter_2(sK21,sK20)
& m2_filter_2(sK21,sK19)
& g3_lattices(u1_struct_0(sK19),u2_lattices(sK19),u1_lattices(sK19)) = g3_lattices(u1_struct_0(sK20),u2_lattices(sK20),u1_lattices(sK20))
& ~ v3_struct_0(sK20)
& v10_lattices(sK20)
& l3_lattices(sK20)
& ~ v3_struct_0(sK19)
& v10_lattices(sK19)
& l3_lattices(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20,sK21]),skolemize(X0,sK19),skolemize(X1,sK20),skolemize(X2,sK21)],[f34838]) ).
fof(f35527,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34717]) ).
fof(f35528,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34717]) ).
fof(f35591,plain,
! [X0,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))
| k1_lattice2(X0) = k1_lattice2(X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34814]) ).
fof(f35611,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35312]) ).
fof(f35612,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35312]) ).
fof(f35613,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X4,X1)
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35312]) ).
fof(f35619,plain,
! [X0,X1] :
( m1_subset_1(sK17(X0,X1),u1_struct_0(X0))
| m2_filter_2(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35315]) ).
fof(f35620,plain,
! [X0,X1] :
( m1_subset_1(sK18(X0,X1),u1_struct_0(X0))
| m2_filter_2(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35315]) ).
fof(f35621,plain,
! [X0,X1] :
( r2_hidden(sK18(X0,X1),X1)
| r2_hidden(k3_lattices(X0,sK17(X0,X1),sK18(X0,X1)),X1)
| m2_filter_2(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35315]) ).
fof(f35622,plain,
! [X0,X1] :
( r2_hidden(sK17(X0,X1),X1)
| r2_hidden(k3_lattices(X0,sK17(X0,X1),sK18(X0,X1)),X1)
| m2_filter_2(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35315]) ).
fof(f35623,plain,
! [X0,X1] :
( m2_filter_2(X1,X0)
| ~ r2_hidden(k3_lattices(X0,sK17(X0,X1),sK18(X0,X1)),X1)
| ~ r2_hidden(sK17(X0,X1),X1)
| ~ r2_hidden(sK18(X0,X1),X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35315]) ).
fof(f35625,plain,
l3_lattices(sK19),
inference(cnf_transformation,[],[f35316]) ).
fof(f35626,plain,
v10_lattices(sK19),
inference(cnf_transformation,[],[f35316]) ).
fof(f35627,plain,
~ v3_struct_0(sK19),
inference(cnf_transformation,[],[f35316]) ).
fof(f35628,plain,
l3_lattices(sK20),
inference(cnf_transformation,[],[f35316]) ).
fof(f35629,plain,
v10_lattices(sK20),
inference(cnf_transformation,[],[f35316]) ).
fof(f35630,plain,
~ v3_struct_0(sK20),
inference(cnf_transformation,[],[f35316]) ).
fof(f35631,plain,
g3_lattices(u1_struct_0(sK19),u2_lattices(sK19),u1_lattices(sK19)) = g3_lattices(u1_struct_0(sK20),u2_lattices(sK20),u1_lattices(sK20)),
inference(cnf_transformation,[],[f35316]) ).
fof(f35632,plain,
m2_filter_2(sK21,sK19),
inference(cnf_transformation,[],[f35316]) ).
fof(f35633,plain,
~ m2_filter_2(sK21,sK20),
inference(cnf_transformation,[],[f35316]) ).
fof(f35642,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f34845]) ).
fof(f35647,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34849]) ).
fof(f35778,plain,
! [X2,X3,X0,X1,X4] :
( k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),X3,X4)
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34961]) ).
fof(f35783,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f34965]) ).
fof(f36292,plain,
! [X2,X3,X0,X4] :
( k3_lattices(X0,X3,X2) = k4_lattices(k1_lattice2(X0),X3,X4)
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f35778]) ).
fof(f36293,plain,
! [X3,X0,X4] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| v3_struct_0(X0)
| k4_lattices(k1_lattice2(X0),X3,X4) = k3_lattices(X0,X3,X4)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f36292]) ).
fof(f36311,definition,
sF136 = u1_struct_0(sK19),
introduced(definition,[new_symbols(definition,[sF136])],[function_definition]) ).
fof(f36312,plain,
u1_struct_0(sK19) = sF136,
inference(reorient_equations,[],[f36311]) ).
fof(f36313,definition,
sF137 = u2_lattices(sK19),
introduced(definition,[new_symbols(definition,[sF137])],[function_definition]) ).
fof(f36314,plain,
u2_lattices(sK19) = sF137,
inference(reorient_equations,[],[f36313]) ).
fof(f36315,definition,
sF138 = u1_lattices(sK19),
introduced(definition,[new_symbols(definition,[sF138])],[function_definition]) ).
fof(f36316,plain,
u1_lattices(sK19) = sF138,
inference(reorient_equations,[],[f36315]) ).
fof(f36317,definition,
sF139 = g3_lattices(sF136,sF137,sF138),
introduced(definition,[new_symbols(definition,[sF139])],[function_definition]) ).
fof(f36318,plain,
g3_lattices(sF136,sF137,sF138) = sF139,
inference(reorient_equations,[],[f36317]) ).
fof(f36319,definition,
sF140 = u1_struct_0(sK20),
introduced(definition,[new_symbols(definition,[sF140])],[function_definition]) ).
fof(f36320,plain,
u1_struct_0(sK20) = sF140,
inference(reorient_equations,[],[f36319]) ).
fof(f36321,definition,
sF141 = u2_lattices(sK20),
introduced(definition,[new_symbols(definition,[sF141])],[function_definition]) ).
fof(f36322,plain,
u2_lattices(sK20) = sF141,
inference(reorient_equations,[],[f36321]) ).
fof(f36323,definition,
sF142 = u1_lattices(sK20),
introduced(definition,[new_symbols(definition,[sF142])],[function_definition]) ).
fof(f36324,plain,
u1_lattices(sK20) = sF142,
inference(reorient_equations,[],[f36323]) ).
fof(f36325,definition,
sF143 = g3_lattices(sF140,sF141,sF142),
introduced(definition,[new_symbols(definition,[sF143])],[function_definition]) ).
fof(f36326,plain,
g3_lattices(sF140,sF141,sF142) = sF143,
inference(reorient_equations,[],[f36325]) ).
fof(f36327,plain,
sF139 = sF143,
inference(definition_folding,[],[f35631,f36326,f36324,f36322,f36320,f36318,f36316,f36314,f36312]) ).
fof(f36676,definition,
( spl144_65
<=> l3_lattices(sK19) ),
introduced(definition,[new_symbols(definition,[spl144_65])],[avatar_definition]) ).
fof(f36678,plain,
( l3_lattices(sK19)
| ~ spl144_65 ),
inference(avatar_component_clause,[],[f36676]) ).
fof(f36679,plain,
spl144_65,
inference(avatar_split_clause,[],[f35625,f36676]) ).
fof(f36681,definition,
( spl144_66
<=> v10_lattices(sK19) ),
introduced(definition,[new_symbols(definition,[spl144_66])],[avatar_definition]) ).
fof(f36683,plain,
( v10_lattices(sK19)
| ~ spl144_66 ),
inference(avatar_component_clause,[],[f36681]) ).
fof(f36684,plain,
spl144_66,
inference(avatar_split_clause,[],[f35626,f36681]) ).
fof(f36686,definition,
( spl144_67
<=> v3_struct_0(sK19) ),
introduced(definition,[new_symbols(definition,[spl144_67])],[avatar_definition]) ).
fof(f36688,plain,
( ~ v3_struct_0(sK19)
| spl144_67 ),
inference(avatar_component_clause,[],[f36686]) ).
fof(f36689,plain,
~ spl144_67,
inference(avatar_split_clause,[],[f35627,f36686]) ).
fof(f36691,definition,
( spl144_68
<=> l3_lattices(sK20) ),
introduced(definition,[new_symbols(definition,[spl144_68])],[avatar_definition]) ).
fof(f36693,plain,
( l3_lattices(sK20)
| ~ spl144_68 ),
inference(avatar_component_clause,[],[f36691]) ).
fof(f36694,plain,
spl144_68,
inference(avatar_split_clause,[],[f35628,f36691]) ).
fof(f36696,definition,
( spl144_69
<=> v10_lattices(sK20) ),
introduced(definition,[new_symbols(definition,[spl144_69])],[avatar_definition]) ).
fof(f36698,plain,
( v10_lattices(sK20)
| ~ spl144_69 ),
inference(avatar_component_clause,[],[f36696]) ).
fof(f36699,plain,
spl144_69,
inference(avatar_split_clause,[],[f35629,f36696]) ).
fof(f36701,definition,
( spl144_70
<=> v3_struct_0(sK20) ),
introduced(definition,[new_symbols(definition,[spl144_70])],[avatar_definition]) ).
fof(f36703,plain,
( ~ v3_struct_0(sK20)
| spl144_70 ),
inference(avatar_component_clause,[],[f36701]) ).
fof(f36704,plain,
~ spl144_70,
inference(avatar_split_clause,[],[f35630,f36701]) ).
fof(f36706,definition,
( spl144_71
<=> sF139 = sF143 ),
introduced(definition,[new_symbols(definition,[spl144_71])],[avatar_definition]) ).
fof(f36708,plain,
( sF139 = sF143
| ~ spl144_71 ),
inference(avatar_component_clause,[],[f36706]) ).
fof(f36709,plain,
spl144_71,
inference(avatar_split_clause,[],[f36327,f36706]) ).
fof(f36711,definition,
( spl144_72
<=> m2_filter_2(sK21,sK19) ),
introduced(definition,[new_symbols(definition,[spl144_72])],[avatar_definition]) ).
fof(f36713,plain,
( m2_filter_2(sK21,sK19)
| ~ spl144_72 ),
inference(avatar_component_clause,[],[f36711]) ).
fof(f36714,plain,
spl144_72,
inference(avatar_split_clause,[],[f35632,f36711]) ).
fof(f36716,definition,
( spl144_73
<=> m2_filter_2(sK21,sK20) ),
introduced(definition,[new_symbols(definition,[spl144_73])],[avatar_definition]) ).
fof(f36718,plain,
( ~ m2_filter_2(sK21,sK20)
| spl144_73 ),
inference(avatar_component_clause,[],[f36716]) ).
fof(f36719,plain,
~ spl144_73,
inference(avatar_split_clause,[],[f35633,f36716]) ).
fof(f36720,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ r2_hidden(k3_lattices(X0,sK17(X0,X1),sK18(X0,X1)),X1)
| ~ r2_hidden(sK17(X0,X1),X1)
| ~ r2_hidden(sK18(X0,X1),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| m2_filter_2(X1,X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f35623,f35642]) ).
fof(f36721,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f35611,f35642]) ).
fof(f36722,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f35612,f35642]) ).
fof(f36723,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X4,X1)
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f35613,f35642]) ).
fof(f36732,definition,
( spl144_74
<=> u1_struct_0(sK19) = sF136 ),
introduced(definition,[new_symbols(definition,[spl144_74])],[avatar_definition]) ).
fof(f36734,plain,
( u1_struct_0(sK19) = sF136
| ~ spl144_74 ),
inference(avatar_component_clause,[],[f36732]) ).
fof(f36735,plain,
spl144_74,
inference(avatar_split_clause,[],[f36312,f36732]) ).
fof(f36737,definition,
( spl144_75
<=> u2_lattices(sK19) = sF137 ),
introduced(definition,[new_symbols(definition,[spl144_75])],[avatar_definition]) ).
fof(f36739,plain,
( u2_lattices(sK19) = sF137
| ~ spl144_75 ),
inference(avatar_component_clause,[],[f36737]) ).
fof(f36740,plain,
spl144_75,
inference(avatar_split_clause,[],[f36314,f36737]) ).
fof(f36742,definition,
( spl144_76
<=> u1_lattices(sK19) = sF138 ),
introduced(definition,[new_symbols(definition,[spl144_76])],[avatar_definition]) ).
fof(f36744,plain,
( u1_lattices(sK19) = sF138
| ~ spl144_76 ),
inference(avatar_component_clause,[],[f36742]) ).
fof(f36745,plain,
spl144_76,
inference(avatar_split_clause,[],[f36316,f36742]) ).
fof(f36747,definition,
( spl144_77
<=> g3_lattices(sF136,sF137,sF138) = sF139 ),
introduced(definition,[new_symbols(definition,[spl144_77])],[avatar_definition]) ).
fof(f36749,plain,
( g3_lattices(sF136,sF137,sF138) = sF139
| ~ spl144_77 ),
inference(avatar_component_clause,[],[f36747]) ).
fof(f36750,plain,
spl144_77,
inference(avatar_split_clause,[],[f36318,f36747]) ).
fof(f36752,definition,
( spl144_78
<=> u1_struct_0(sK20) = sF140 ),
introduced(definition,[new_symbols(definition,[spl144_78])],[avatar_definition]) ).
fof(f36754,plain,
( u1_struct_0(sK20) = sF140
| ~ spl144_78 ),
inference(avatar_component_clause,[],[f36752]) ).
fof(f36755,plain,
spl144_78,
inference(avatar_split_clause,[],[f36320,f36752]) ).
fof(f36757,definition,
( spl144_79
<=> u2_lattices(sK20) = sF141 ),
introduced(definition,[new_symbols(definition,[spl144_79])],[avatar_definition]) ).
fof(f36759,plain,
( u2_lattices(sK20) = sF141
| ~ spl144_79 ),
inference(avatar_component_clause,[],[f36757]) ).
fof(f36760,plain,
spl144_79,
inference(avatar_split_clause,[],[f36322,f36757]) ).
fof(f36762,definition,
( spl144_80
<=> u1_lattices(sK20) = sF142 ),
introduced(definition,[new_symbols(definition,[spl144_80])],[avatar_definition]) ).
fof(f36764,plain,
( u1_lattices(sK20) = sF142
| ~ spl144_80 ),
inference(avatar_component_clause,[],[f36762]) ).
fof(f36765,plain,
spl144_80,
inference(avatar_split_clause,[],[f36324,f36762]) ).
fof(f36767,definition,
( spl144_81
<=> g3_lattices(sF140,sF141,sF142) = sF143 ),
introduced(definition,[new_symbols(definition,[spl144_81])],[avatar_definition]) ).
fof(f36769,plain,
( g3_lattices(sF140,sF141,sF142) = sF143
| ~ spl144_81 ),
inference(avatar_component_clause,[],[f36767]) ).
fof(f36770,plain,
spl144_81,
inference(avatar_split_clause,[],[f36326,f36767]) ).
fof(f36776,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f36721,f35527]) ).
fof(f36777,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f36722,f35527]) ).
fof(f36778,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X4,X1)
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f36723,f35527]) ).
fof(f36788,plain,
( sF139 = g3_lattices(sF140,sF141,sF142)
| ~ spl144_71
| ~ spl144_81 ),
inference(forward_demodulation,[],[f36769,f36708]) ).
fof(f36790,definition,
( spl144_82
<=> sF139 = g3_lattices(sF140,sF141,sF142) ),
introduced(definition,[new_symbols(definition,[spl144_82])],[avatar_definition]) ).
fof(f36792,plain,
( sF139 = g3_lattices(sF140,sF141,sF142)
| ~ spl144_82 ),
inference(avatar_component_clause,[],[f36790]) ).
fof(f36793,plain,
( spl144_82
| ~ spl144_71
| ~ spl144_81 ),
inference(avatar_split_clause,[],[f36788,f36767,f36706,f36790]) ).
fof(f36854,plain,
( m2_lattice4(sK21,sK19)
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72 ),
inference(unit_resulting_resolution,[],[f35527,f36678,f36683,f36688,f36713]) ).
fof(f36858,definition,
( spl144_87
<=> m2_lattice4(sK21,sK19) ),
introduced(definition,[new_symbols(definition,[spl144_87])],[avatar_definition]) ).
fof(f36860,plain,
( m2_lattice4(sK21,sK19)
| ~ spl144_87 ),
inference(avatar_component_clause,[],[f36858]) ).
fof(f36861,plain,
( spl144_87
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72 ),
inference(avatar_split_clause,[],[f36854,f36711,f36686,f36681,f36676,f36858]) ).
fof(f36864,plain,
( m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK19)))
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_87 ),
inference(unit_resulting_resolution,[],[f35647,f36678,f36683,f36688,f36860]) ).
fof(f36867,plain,
( m1_subset_1(sK21,k1_zfmisc_1(sF136))
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_74
| ~ spl144_87 ),
inference(forward_demodulation,[],[f36864,f36734]) ).
fof(f36870,definition,
( spl144_88
<=> m1_subset_1(sK21,k1_zfmisc_1(sF136)) ),
introduced(definition,[new_symbols(definition,[spl144_88])],[avatar_definition]) ).
fof(f36872,plain,
( m1_subset_1(sK21,k1_zfmisc_1(sF136))
| ~ spl144_88 ),
inference(avatar_component_clause,[],[f36870]) ).
fof(f36873,plain,
( spl144_88
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_74
| ~ spl144_87 ),
inference(avatar_split_clause,[],[f36867,f36858,f36732,f36686,f36681,f36676,f36870]) ).
fof(f36922,plain,
( ! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK19),u2_lattices(sK19),u1_lattices(sK19))
| k1_lattice2(X0) = k1_lattice2(sK19)
| ~ l3_lattices(X0) )
| ~ spl144_65 ),
inference(resolution,[],[f35591,f36678]) ).
fof(f36925,plain,
( ! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK19),u2_lattices(sK19),sF138)
| k1_lattice2(X0) = k1_lattice2(sK19)
| ~ l3_lattices(X0) )
| ~ spl144_65
| ~ spl144_76 ),
inference(forward_demodulation,[],[f36922,f36744]) ).
fof(f36927,plain,
( ! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK19),sF137,sF138)
| k1_lattice2(X0) = k1_lattice2(sK19)
| ~ l3_lattices(X0) )
| ~ spl144_65
| ~ spl144_75
| ~ spl144_76 ),
inference(forward_demodulation,[],[f36925,f36739]) ).
fof(f36929,plain,
( ! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(sF136,sF137,sF138)
| k1_lattice2(X0) = k1_lattice2(sK19)
| ~ l3_lattices(X0) )
| ~ spl144_65
| ~ spl144_74
| ~ spl144_75
| ~ spl144_76 ),
inference(forward_demodulation,[],[f36927,f36734]) ).
fof(f36931,plain,
( ! [X0] :
( ~ l3_lattices(X0)
| k1_lattice2(X0) = k1_lattice2(sK19)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != sF139 )
| ~ spl144_65
| ~ spl144_74
| ~ spl144_75
| ~ spl144_76
| ~ spl144_77 ),
inference(forward_demodulation,[],[f36929,f36749]) ).
fof(f36933,plain,
( k1_lattice2(sK19) = k1_lattice2(sK20)
| g3_lattices(u1_struct_0(sK20),u2_lattices(sK20),u1_lattices(sK20)) != sF139
| ~ spl144_65
| ~ spl144_68
| ~ spl144_74
| ~ spl144_75
| ~ spl144_76
| ~ spl144_77 ),
inference(resolution,[],[f36931,f36693]) ).
fof(f36934,plain,
( sF139 != g3_lattices(u1_struct_0(sK20),u2_lattices(sK20),sF142)
| k1_lattice2(sK19) = k1_lattice2(sK20)
| ~ spl144_65
| ~ spl144_68
| ~ spl144_74
| ~ spl144_75
| ~ spl144_76
| ~ spl144_77
| ~ spl144_80 ),
inference(forward_demodulation,[],[f36933,f36764]) ).
fof(f36935,plain,
( sF139 != g3_lattices(u1_struct_0(sK20),sF141,sF142)
| k1_lattice2(sK19) = k1_lattice2(sK20)
| ~ spl144_65
| ~ spl144_68
| ~ spl144_74
| ~ spl144_75
| ~ spl144_76
| ~ spl144_77
| ~ spl144_79
| ~ spl144_80 ),
inference(forward_demodulation,[],[f36934,f36759]) ).
fof(f36936,plain,
( sF139 != g3_lattices(sF140,sF141,sF142)
| k1_lattice2(sK19) = k1_lattice2(sK20)
| ~ spl144_65
| ~ spl144_68
| ~ spl144_74
| ~ spl144_75
| ~ spl144_76
| ~ spl144_77
| ~ spl144_78
| ~ spl144_79
| ~ spl144_80 ),
inference(forward_demodulation,[],[f36935,f36754]) ).
fof(f36937,plain,
( k1_lattice2(sK19) = k1_lattice2(sK20)
| ~ spl144_65
| ~ spl144_68
| ~ spl144_74
| ~ spl144_75
| ~ spl144_76
| ~ spl144_77
| ~ spl144_78
| ~ spl144_79
| ~ spl144_80
| ~ spl144_82 ),
inference(forward_subsumption_resolution,[],[f36936,f36792]) ).
fof(f36939,definition,
( spl144_93
<=> k1_lattice2(sK19) = k1_lattice2(sK20) ),
introduced(definition,[new_symbols(definition,[spl144_93])],[avatar_definition]) ).
fof(f36941,plain,
( k1_lattice2(sK19) = k1_lattice2(sK20)
| ~ spl144_93 ),
inference(avatar_component_clause,[],[f36939]) ).
fof(f36942,plain,
( spl144_93
| ~ spl144_65
| ~ spl144_68
| ~ spl144_74
| ~ spl144_75
| ~ spl144_76
| ~ spl144_77
| ~ spl144_78
| ~ spl144_79
| ~ spl144_80
| ~ spl144_82 ),
inference(avatar_split_clause,[],[f36937,f36790,f36762,f36757,f36752,f36747,f36742,f36737,f36732,f36691,f36676,f36939]) ).
fof(f36946,plain,
( ~ v1_xboole_0(sK21)
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72 ),
inference(unit_resulting_resolution,[],[f35528,f36678,f36683,f36688,f36713]) ).
fof(f36948,definition,
( spl144_94
<=> v1_xboole_0(sK21) ),
introduced(definition,[new_symbols(definition,[spl144_94])],[avatar_definition]) ).
fof(f36950,plain,
( ~ v1_xboole_0(sK21)
| spl144_94 ),
inference(avatar_component_clause,[],[f36948]) ).
fof(f36951,plain,
( ~ spl144_94
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72 ),
inference(avatar_split_clause,[],[f36946,f36711,f36686,f36681,f36676,f36948]) ).
fof(f37079,plain,
( ! [X0] :
( m1_subset_1(sK17(sK20,X0),sF140)
| m2_filter_2(X0,sK20)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF140))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) )
| ~ spl144_78 ),
inference(superposition,[],[f35619,f36754]) ).
fof(f37080,plain,
( ! [X0] :
( m1_subset_1(sK17(sK20,X0),sF140)
| m2_filter_2(X0,sK20)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF140))
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) )
| spl144_70
| ~ spl144_78 ),
inference(forward_subsumption_resolution,[],[f37079,f36703]) ).
fof(f37082,plain,
( ! [X0] :
( m1_subset_1(sK17(sK20,X0),sF140)
| m2_filter_2(X0,sK20)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF140))
| ~ l3_lattices(sK20) )
| ~ spl144_69
| spl144_70
| ~ spl144_78 ),
inference(forward_subsumption_resolution,[],[f37080,f36698]) ).
fof(f37084,plain,
( ! [X0] :
( m1_subset_1(sK17(sK20,X0),sF140)
| m2_filter_2(X0,sK20)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF140)) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78 ),
inference(forward_subsumption_resolution,[],[f37082,f36693]) ).
fof(f37087,plain,
( ! [X0] :
( m1_subset_1(sK18(sK20,X0),sF140)
| m2_filter_2(X0,sK20)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF140))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) )
| ~ spl144_78 ),
inference(superposition,[],[f35620,f36754]) ).
fof(f37088,plain,
( ! [X0] :
( m1_subset_1(sK18(sK20,X0),sF140)
| m2_filter_2(X0,sK20)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF140))
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) )
| spl144_70
| ~ spl144_78 ),
inference(forward_subsumption_resolution,[],[f37087,f36703]) ).
fof(f37090,plain,
( ! [X0] :
( m1_subset_1(sK18(sK20,X0),sF140)
| m2_filter_2(X0,sK20)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF140))
| ~ l3_lattices(sK20) )
| ~ spl144_69
| spl144_70
| ~ spl144_78 ),
inference(forward_subsumption_resolution,[],[f37088,f36698]) ).
fof(f37092,plain,
( ! [X0] :
( m1_subset_1(sK18(sK20,X0),sF140)
| m2_filter_2(X0,sK20)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF140)) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78 ),
inference(forward_subsumption_resolution,[],[f37090,f36693]) ).
fof(f37223,plain,
( u1_struct_0(sK19) = u1_struct_0(k1_lattice2(sK19))
| ~ spl144_65
| spl144_67 ),
inference(unit_resulting_resolution,[],[f35783,f36678,f36688]) ).
fof(f37224,plain,
( u1_struct_0(sK20) = u1_struct_0(k1_lattice2(sK20))
| ~ spl144_68
| spl144_70 ),
inference(unit_resulting_resolution,[],[f35783,f36693,f36703]) ).
fof(f37229,plain,
( sF136 = u1_struct_0(k1_lattice2(sK19))
| ~ spl144_65
| spl144_67
| ~ spl144_74 ),
inference(forward_demodulation,[],[f37223,f36734]) ).
fof(f37230,plain,
( u1_struct_0(sK20) = u1_struct_0(k1_lattice2(sK19))
| ~ spl144_68
| spl144_70
| ~ spl144_93 ),
inference(forward_demodulation,[],[f37224,f36941]) ).
fof(f37234,definition,
( spl144_118
<=> sF136 = u1_struct_0(k1_lattice2(sK19)) ),
introduced(definition,[new_symbols(definition,[spl144_118])],[avatar_definition]) ).
fof(f37236,plain,
( sF136 = u1_struct_0(k1_lattice2(sK19))
| ~ spl144_118 ),
inference(avatar_component_clause,[],[f37234]) ).
fof(f37237,plain,
( spl144_118
| ~ spl144_65
| spl144_67
| ~ spl144_74 ),
inference(avatar_split_clause,[],[f37229,f36732,f36686,f36676,f37234]) ).
fof(f37238,plain,
( sF140 = u1_struct_0(k1_lattice2(sK19))
| ~ spl144_68
| spl144_70
| ~ spl144_78
| ~ spl144_93 ),
inference(forward_demodulation,[],[f37230,f36754]) ).
fof(f37241,definition,
( spl144_119
<=> sF140 = u1_struct_0(k1_lattice2(sK19)) ),
introduced(definition,[new_symbols(definition,[spl144_119])],[avatar_definition]) ).
fof(f37243,plain,
( sF140 = u1_struct_0(k1_lattice2(sK19))
| ~ spl144_119 ),
inference(avatar_component_clause,[],[f37241]) ).
fof(f37244,plain,
( spl144_119
| ~ spl144_68
| spl144_70
| ~ spl144_78
| ~ spl144_93 ),
inference(avatar_split_clause,[],[f37238,f36939,f36752,f36701,f36691,f37241]) ).
fof(f37245,plain,
( sF136 = sF140
| ~ spl144_118
| ~ spl144_119 ),
inference(forward_demodulation,[],[f37243,f37236]) ).
fof(f37247,definition,
( spl144_120
<=> sF136 = sF140 ),
introduced(definition,[new_symbols(definition,[spl144_120])],[avatar_definition]) ).
fof(f37249,plain,
( sF136 = sF140
| ~ spl144_120 ),
inference(avatar_component_clause,[],[f37247]) ).
fof(f37250,plain,
( spl144_120
| ~ spl144_118
| ~ spl144_119 ),
inference(avatar_split_clause,[],[f37245,f37241,f37234,f37247]) ).
fof(f37259,plain,
( ! [X0] :
( m1_subset_1(sK17(sK20,X0),sF136)
| m2_filter_2(X0,sK20)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF136)) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_120 ),
inference(superposition,[],[f37084,f37249]) ).
fof(f37260,plain,
( ! [X0] :
( m1_subset_1(sK18(sK20,X0),sF136)
| m2_filter_2(X0,sK20)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF136)) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_120 ),
inference(superposition,[],[f37092,f37249]) ).
fof(f37349,plain,
( m1_subset_1(sK17(sK20,sK21),sF136)
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120 ),
inference(unit_resulting_resolution,[],[f37259,f36950,f36718,f36872]) ).
fof(f37351,definition,
( spl144_133
<=> m1_subset_1(sK17(sK20,sK21),sF136) ),
introduced(definition,[new_symbols(definition,[spl144_133])],[avatar_definition]) ).
fof(f37353,plain,
( m1_subset_1(sK17(sK20,sK21),sF136)
| ~ spl144_133 ),
inference(avatar_component_clause,[],[f37351]) ).
fof(f37354,plain,
( spl144_133
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120 ),
inference(avatar_split_clause,[],[f37349,f37247,f36948,f36870,f36752,f36716,f36701,f36696,f36691,f37351]) ).
fof(f37355,plain,
( m1_subset_1(sK18(sK20,sK21),sF136)
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120 ),
inference(unit_resulting_resolution,[],[f37260,f36950,f36718,f36872]) ).
fof(f37357,definition,
( spl144_134
<=> m1_subset_1(sK18(sK20,sK21),sF136) ),
introduced(definition,[new_symbols(definition,[spl144_134])],[avatar_definition]) ).
fof(f37359,plain,
( m1_subset_1(sK18(sK20,sK21),sF136)
| ~ spl144_134 ),
inference(avatar_component_clause,[],[f37357]) ).
fof(f37360,plain,
( spl144_134
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120 ),
inference(avatar_split_clause,[],[f37355,f37247,f36948,f36870,f36752,f36716,f36701,f36696,f36691,f37357]) ).
fof(f38391,plain,
( ! [X0] :
( ~ r2_hidden(k3_lattices(sK20,sK17(sK20,X0),sK18(sK20,X0)),X0)
| ~ r2_hidden(sK17(sK20,X0),X0)
| ~ r2_hidden(sK18(sK20,X0),X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK20)))
| m2_filter_2(X0,sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) )
| spl144_70 ),
inference(resolution,[],[f36720,f36703]) ).
fof(f38394,plain,
( ! [X0] :
( ~ r2_hidden(k3_lattices(sK20,sK17(sK20,X0),sK18(sK20,X0)),X0)
| ~ r2_hidden(sK17(sK20,X0),X0)
| ~ r2_hidden(sK18(sK20,X0),X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK20)))
| m2_filter_2(X0,sK20)
| ~ l3_lattices(sK20) )
| ~ spl144_69
| spl144_70 ),
inference(forward_subsumption_resolution,[],[f38391,f36698]) ).
fof(f38397,plain,
( ! [X0] :
( ~ r2_hidden(k3_lattices(sK20,sK17(sK20,X0),sK18(sK20,X0)),X0)
| ~ r2_hidden(sK17(sK20,X0),X0)
| ~ r2_hidden(sK18(sK20,X0),X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK20)))
| m2_filter_2(X0,sK20) )
| ~ spl144_68
| ~ spl144_69
| spl144_70 ),
inference(forward_subsumption_resolution,[],[f38394,f36693]) ).
fof(f38400,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF140))
| ~ r2_hidden(k3_lattices(sK20,sK17(sK20,X0),sK18(sK20,X0)),X0)
| ~ r2_hidden(sK17(sK20,X0),X0)
| ~ r2_hidden(sK18(sK20,X0),X0)
| m2_filter_2(X0,sK20) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78 ),
inference(forward_demodulation,[],[f38397,f36754]) ).
fof(f38402,plain,
( ! [X0] :
( m2_filter_2(X0,sK20)
| ~ r2_hidden(k3_lattices(sK20,sK17(sK20,X0),sK18(sK20,X0)),X0)
| ~ r2_hidden(sK17(sK20,X0),X0)
| ~ r2_hidden(sK18(sK20,X0),X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF136)) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_120 ),
inference(forward_demodulation,[],[f38400,f37249]) ).
fof(f38404,plain,
( ~ r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ r2_hidden(sK18(sK20,sK21),sK21)
| ~ m1_subset_1(sK21,k1_zfmisc_1(sF136))
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_120 ),
inference(resolution,[],[f38402,f36718]) ).
fof(f38405,plain,
( ~ r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ r2_hidden(sK18(sK20,sK21),sK21)
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| ~ spl144_120 ),
inference(forward_subsumption_resolution,[],[f38404,f36872]) ).
fof(f38408,definition,
( spl144_189
<=> r2_hidden(sK18(sK20,sK21),sK21) ),
introduced(definition,[new_symbols(definition,[spl144_189])],[avatar_definition]) ).
fof(f38409,plain,
( r2_hidden(sK18(sK20,sK21),sK21)
| ~ spl144_189 ),
inference(avatar_component_clause,[],[f38408]) ).
fof(f38410,plain,
( ~ r2_hidden(sK18(sK20,sK21),sK21)
| spl144_189 ),
inference(avatar_component_clause,[],[f38408]) ).
fof(f38412,definition,
( spl144_190
<=> r2_hidden(sK17(sK20,sK21),sK21) ),
introduced(definition,[new_symbols(definition,[spl144_190])],[avatar_definition]) ).
fof(f38414,plain,
( ~ r2_hidden(sK17(sK20,sK21),sK21)
| spl144_190 ),
inference(avatar_component_clause,[],[f38412]) ).
fof(f38416,definition,
( spl144_191
<=> r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21) ),
introduced(definition,[new_symbols(definition,[spl144_191])],[avatar_definition]) ).
fof(f38418,plain,
( ~ r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| spl144_191 ),
inference(avatar_component_clause,[],[f38416]) ).
fof(f38419,plain,
( ~ spl144_189
| ~ spl144_190
| ~ spl144_191
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| ~ spl144_120 ),
inference(avatar_split_clause,[],[f38405,f37247,f36870,f36752,f36716,f36701,f36696,f36691,f38416,f38412,f38408]) ).
fof(f38422,plain,
( r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| m2_filter_2(sK21,sK20)
| v1_xboole_0(sK21)
| ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| spl144_189 ),
inference(resolution,[],[f38410,f35621]) ).
fof(f38425,plain,
( r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| v1_xboole_0(sK21)
| ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| spl144_73
| spl144_189 ),
inference(forward_subsumption_resolution,[],[f38422,f36718]) ).
fof(f38426,plain,
( r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| spl144_73
| spl144_94
| spl144_189 ),
inference(forward_subsumption_resolution,[],[f38425,f36950]) ).
fof(f38427,plain,
( r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| spl144_70
| spl144_73
| spl144_94
| spl144_189 ),
inference(forward_subsumption_resolution,[],[f38426,f36703]) ).
fof(f38428,plain,
( r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| ~ l3_lattices(sK20)
| ~ spl144_69
| spl144_70
| spl144_73
| spl144_94
| spl144_189 ),
inference(forward_subsumption_resolution,[],[f38427,f36698]) ).
fof(f38429,plain,
( r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| spl144_94
| spl144_189 ),
inference(forward_subsumption_resolution,[],[f38428,f36693]) ).
fof(f38430,plain,
( ~ m1_subset_1(sK21,k1_zfmisc_1(sF140))
| r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| spl144_94
| spl144_189 ),
inference(forward_demodulation,[],[f38429,f36754]) ).
fof(f38431,plain,
( ~ m1_subset_1(sK21,k1_zfmisc_1(sF136))
| r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| spl144_94
| ~ spl144_120
| spl144_189 ),
inference(forward_demodulation,[],[f38430,f37249]) ).
fof(f38432,plain,
( r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120
| spl144_189 ),
inference(forward_subsumption_resolution,[],[f38431,f36872]) ).
fof(f38433,plain,
( spl144_191
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120
| spl144_189 ),
inference(avatar_split_clause,[],[f38432,f38408,f37247,f36948,f36870,f36752,f36716,f36701,f36696,f36691,f38416]) ).
fof(f39578,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK19)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK19)))
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ m1_subset_1(X1,u1_struct_0(sK19))
| v3_struct_0(sK19)
| k4_lattices(k1_lattice2(sK19),X1,X0) = k3_lattices(sK19,X1,X0)
| ~ l3_lattices(sK19) )
| ~ spl144_66 ),
inference(resolution,[],[f36293,f36683]) ).
fof(f39579,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK20)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK20)))
| ~ m1_subset_1(X0,u1_struct_0(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| v3_struct_0(sK20)
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0)
| ~ l3_lattices(sK20) )
| ~ spl144_69 ),
inference(resolution,[],[f36293,f36698]) ).
fof(f39582,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK20)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK20)))
| ~ m1_subset_1(X0,u1_struct_0(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0)
| ~ l3_lattices(sK20) )
| ~ spl144_69
| spl144_70 ),
inference(forward_subsumption_resolution,[],[f39579,f36703]) ).
fof(f39583,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK19)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK19)))
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ m1_subset_1(X1,u1_struct_0(sK19))
| k4_lattices(k1_lattice2(sK19),X1,X0) = k3_lattices(sK19,X1,X0)
| ~ l3_lattices(sK19) )
| ~ spl144_66
| spl144_67 ),
inference(forward_subsumption_resolution,[],[f39578,f36688]) ).
fof(f39586,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK20)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK20)))
| ~ m1_subset_1(X0,u1_struct_0(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70 ),
inference(forward_subsumption_resolution,[],[f39582,f36693]) ).
fof(f39587,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK19)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK19)))
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ m1_subset_1(X1,u1_struct_0(sK19))
| k4_lattices(k1_lattice2(sK19),X1,X0) = k3_lattices(sK19,X1,X0) )
| ~ spl144_65
| ~ spl144_66
| spl144_67 ),
inference(forward_subsumption_resolution,[],[f39583,f36678]) ).
fof(f39590,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK19)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK20)))
| ~ m1_subset_1(X0,u1_struct_0(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_93 ),
inference(forward_demodulation,[],[f39586,f36941]) ).
fof(f39591,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK19)))
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ m1_subset_1(X1,u1_struct_0(sK19))
| k4_lattices(k1_lattice2(sK19),X1,X0) = k3_lattices(sK19,X1,X0) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_118 ),
inference(forward_demodulation,[],[f39587,f37236]) ).
fof(f39594,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK20)))
| ~ m1_subset_1(X0,u1_struct_0(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_93
| ~ spl144_118 ),
inference(forward_demodulation,[],[f39590,f37236]) ).
fof(f39595,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ m1_subset_1(X1,u1_struct_0(sK19))
| k4_lattices(k1_lattice2(sK19),X1,X0) = k3_lattices(sK19,X1,X0) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_118 ),
inference(forward_demodulation,[],[f39591,f37236]) ).
fof(f39598,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK19)))
| ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X0,u1_struct_0(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_93
| ~ spl144_118 ),
inference(forward_demodulation,[],[f39594,f36941]) ).
fof(f39599,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,u1_struct_0(sK19))
| k4_lattices(k1_lattice2(sK19),X1,X0) = k3_lattices(sK19,X1,X0) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_74
| ~ spl144_118 ),
inference(forward_demodulation,[],[f39595,f36734]) ).
fof(f39600,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X1,u1_struct_0(sK19))
| k4_lattices(k1_lattice2(sK19),X1,X0) = k3_lattices(sK19,X1,X0) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_74
| ~ spl144_118 ),
inference(duplicate_literal_removal,[],[f39599]) ).
fof(f39603,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X0,u1_struct_0(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_93
| ~ spl144_118 ),
inference(forward_demodulation,[],[f39598,f37236]) ).
fof(f39604,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,sF136)
| k4_lattices(k1_lattice2(sK19),X1,X0) = k3_lattices(sK19,X1,X0) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_74
| ~ spl144_118 ),
inference(forward_demodulation,[],[f39600,f36734]) ).
fof(f39605,plain,
( ! [X0,X1] :
( k4_lattices(k1_lattice2(sK19),X1,X0) = k3_lattices(sK19,X1,X0)
| ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,sF136) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_74
| ~ spl144_118 ),
inference(duplicate_literal_removal,[],[f39604]) ).
fof(f39609,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF140)
| ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118 ),
inference(forward_demodulation,[],[f39603,f36754]) ).
fof(f39614,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118
| ~ spl144_120 ),
inference(forward_demodulation,[],[f39609,f37249]) ).
fof(f39615,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118
| ~ spl144_120 ),
inference(duplicate_literal_removal,[],[f39614]) ).
fof(f39619,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF140)
| ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,sF136)
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118
| ~ spl144_120 ),
inference(forward_demodulation,[],[f39615,f36754]) ).
fof(f39621,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(X1,sF136)
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118
| ~ spl144_120 ),
inference(forward_demodulation,[],[f39619,f37249]) ).
fof(f39622,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X0,sF136)
| k4_lattices(k1_lattice2(sK20),X1,X0) = k3_lattices(sK20,X1,X0) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118
| ~ spl144_120 ),
inference(duplicate_literal_removal,[],[f39621]) ).
fof(f39623,plain,
( ! [X0,X1] :
( k4_lattices(k1_lattice2(sK19),X1,X0) = k3_lattices(sK20,X1,X0)
| ~ m1_subset_1(X1,sF136)
| ~ m1_subset_1(X0,sF136) )
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118
| ~ spl144_120 ),
inference(forward_demodulation,[],[f39622,f36941]) ).
fof(f39626,plain,
( k4_lattices(k1_lattice2(sK19),sK17(sK20,sK21),sK18(sK20,sK21)) = k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21))
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_74
| ~ spl144_118
| ~ spl144_133
| ~ spl144_134 ),
inference(unit_resulting_resolution,[],[f39605,f37353,f37359]) ).
fof(f39639,definition,
( spl144_309
<=> k4_lattices(k1_lattice2(sK19),sK17(sK20,sK21),sK18(sK20,sK21)) = k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21)) ),
introduced(definition,[new_symbols(definition,[spl144_309])],[avatar_definition]) ).
fof(f39641,plain,
( k4_lattices(k1_lattice2(sK19),sK17(sK20,sK21),sK18(sK20,sK21)) = k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21))
| ~ spl144_309 ),
inference(avatar_component_clause,[],[f39639]) ).
fof(f39642,plain,
( spl144_309
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_74
| ~ spl144_118
| ~ spl144_133
| ~ spl144_134 ),
inference(avatar_split_clause,[],[f39626,f37357,f37351,f37234,f36732,f36686,f36681,f36676,f39639]) ).
fof(f39649,plain,
( k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)) = k4_lattices(k1_lattice2(sK19),sK17(sK20,sK21),sK18(sK20,sK21))
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118
| ~ spl144_120
| ~ spl144_133
| ~ spl144_134 ),
inference(unit_resulting_resolution,[],[f39623,f37359,f37353]) ).
fof(f39657,plain,
( k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)) = k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21))
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118
| ~ spl144_120
| ~ spl144_133
| ~ spl144_134
| ~ spl144_309 ),
inference(forward_demodulation,[],[f39649,f39641]) ).
fof(f39666,definition,
( spl144_312
<=> k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)) = k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21)) ),
introduced(definition,[new_symbols(definition,[spl144_312])],[avatar_definition]) ).
fof(f39668,plain,
( k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)) = k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21))
| ~ spl144_312 ),
inference(avatar_component_clause,[],[f39666]) ).
fof(f39669,plain,
( spl144_312
| ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118
| ~ spl144_120
| ~ spl144_133
| ~ spl144_134
| ~ spl144_309 ),
inference(avatar_split_clause,[],[f39657,f39639,f37357,f37351,f37247,f37234,f36939,f36752,f36701,f36696,f36691,f39666]) ).
fof(f39708,plain,
( ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| spl144_191
| ~ spl144_312 ),
inference(superposition,[],[f38418,f39668]) ).
fof(f39712,definition,
( spl144_315
<=> r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21)),sK21) ),
introduced(definition,[new_symbols(definition,[spl144_315])],[avatar_definition]) ).
fof(f39713,plain,
( r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ spl144_315 ),
inference(avatar_component_clause,[],[f39712]) ).
fof(f39714,plain,
( ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| spl144_315 ),
inference(avatar_component_clause,[],[f39712]) ).
fof(f39715,plain,
( ~ spl144_315
| spl144_191
| ~ spl144_312 ),
inference(avatar_split_clause,[],[f39708,f39666,f38416,f39712]) ).
fof(f39734,plain,
( ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ r2_hidden(sK18(sK20,sK21),sK21)
| ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(sK19))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ m2_filter_2(sK21,sK19)
| v3_struct_0(sK19)
| ~ v10_lattices(sK19)
| ~ l3_lattices(sK19)
| spl144_315 ),
inference(resolution,[],[f39714,f36776]) ).
fof(f39737,plain,
( ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(sK19))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ m2_filter_2(sK21,sK19)
| v3_struct_0(sK19)
| ~ v10_lattices(sK19)
| ~ l3_lattices(sK19)
| ~ spl144_189
| spl144_315 ),
inference(forward_subsumption_resolution,[],[f39734,f38409]) ).
fof(f39738,plain,
( ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(sK19))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| v3_struct_0(sK19)
| ~ v10_lattices(sK19)
| ~ l3_lattices(sK19)
| ~ spl144_72
| ~ spl144_189
| spl144_315 ),
inference(forward_subsumption_resolution,[],[f39737,f36713]) ).
fof(f39739,plain,
( ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(sK19))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ v10_lattices(sK19)
| ~ l3_lattices(sK19)
| spl144_67
| ~ spl144_72
| ~ spl144_189
| spl144_315 ),
inference(forward_subsumption_resolution,[],[f39738,f36688]) ).
fof(f39740,plain,
( ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(sK19))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ l3_lattices(sK19)
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_189
| spl144_315 ),
inference(forward_subsumption_resolution,[],[f39739,f36683]) ).
fof(f39741,plain,
( ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(sK19))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_189
| spl144_315 ),
inference(forward_subsumption_resolution,[],[f39740,f36678]) ).
fof(f39742,plain,
( ~ m1_subset_1(sK18(sK20,sK21),sF136)
| ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_189
| spl144_315 ),
inference(forward_demodulation,[],[f39741,f36734]) ).
fof(f39743,plain,
( ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_134
| ~ spl144_189
| spl144_315 ),
inference(forward_subsumption_resolution,[],[f39742,f37359]) ).
fof(f39744,plain,
( ~ m1_subset_1(sK17(sK20,sK21),sF136)
| ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_134
| ~ spl144_189
| spl144_315 ),
inference(forward_demodulation,[],[f39743,f36734]) ).
fof(f39745,plain,
( ~ r2_hidden(sK17(sK20,sK21),sK21)
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| ~ spl144_189
| spl144_315 ),
inference(forward_subsumption_resolution,[],[f39744,f37353]) ).
fof(f39746,plain,
( ~ spl144_190
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| ~ spl144_189
| spl144_315 ),
inference(avatar_split_clause,[],[f39745,f39712,f38408,f37357,f37351,f36732,f36711,f36686,f36681,f36676,f38412]) ).
fof(f39748,plain,
( r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| m2_filter_2(sK21,sK20)
| v1_xboole_0(sK21)
| ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| spl144_190 ),
inference(resolution,[],[f38414,f35622]) ).
fof(f39749,plain,
( ! [X0,X1] :
( ~ m2_filter_2(sK21,X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(X0))
| ~ r2_hidden(k3_lattices(X0,sK17(sK20,sK21),X1),sK21)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) )
| spl144_190 ),
inference(resolution,[],[f38414,f36778]) ).
fof(f39751,plain,
( m2_filter_2(sK21,sK20)
| v1_xboole_0(sK21)
| ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| spl144_190
| spl144_191 ),
inference(forward_subsumption_resolution,[],[f39748,f38418]) ).
fof(f39753,plain,
( v1_xboole_0(sK21)
| ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| spl144_73
| spl144_190
| spl144_191 ),
inference(forward_subsumption_resolution,[],[f39751,f36718]) ).
fof(f39755,plain,
( ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| spl144_73
| spl144_94
| spl144_190
| spl144_191 ),
inference(forward_subsumption_resolution,[],[f39753,f36950]) ).
fof(f39758,plain,
( ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| spl144_70
| spl144_73
| spl144_94
| spl144_190
| spl144_191 ),
inference(forward_subsumption_resolution,[],[f39755,f36703]) ).
fof(f39759,plain,
( ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| ~ l3_lattices(sK20)
| ~ spl144_69
| spl144_70
| spl144_73
| spl144_94
| spl144_190
| spl144_191 ),
inference(forward_subsumption_resolution,[],[f39758,f36698]) ).
fof(f39760,plain,
( ~ m1_subset_1(sK21,k1_zfmisc_1(u1_struct_0(sK20)))
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| spl144_94
| spl144_190
| spl144_191 ),
inference(forward_subsumption_resolution,[],[f39759,f36693]) ).
fof(f39761,plain,
( ~ m1_subset_1(sK21,k1_zfmisc_1(sF140))
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| spl144_94
| spl144_190
| spl144_191 ),
inference(forward_demodulation,[],[f39760,f36754]) ).
fof(f39762,plain,
( ~ m1_subset_1(sK21,k1_zfmisc_1(sF136))
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| spl144_94
| ~ spl144_120
| spl144_190
| spl144_191 ),
inference(forward_demodulation,[],[f39761,f37249]) ).
fof(f39763,plain,
( $false
| ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120
| spl144_190
| spl144_191 ),
inference(forward_subsumption_resolution,[],[f39762,f36872]) ).
fof(f39764,plain,
( ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120
| spl144_190
| spl144_191 ),
inference(avatar_contradiction_clause,[],[f39763]) ).
fof(f39765,plain,
( k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)) != k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21))
| r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ r2_hidden(k3_lattices(sK20,sK17(sK20,sK21),sK18(sK20,sK21)),sK21) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f39817,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),X0),sK21)
| v3_struct_0(sK19)
| ~ v10_lattices(sK19)
| ~ l3_lattices(sK19) )
| ~ spl144_72
| spl144_190 ),
inference(resolution,[],[f39749,f36713]) ).
fof(f39824,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),X0),sK21)
| ~ v10_lattices(sK19)
| ~ l3_lattices(sK19) )
| spl144_67
| ~ spl144_72
| spl144_190 ),
inference(forward_subsumption_resolution,[],[f39817,f36688]) ).
fof(f39826,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),X0),sK21)
| ~ l3_lattices(sK19) )
| ~ spl144_66
| spl144_67
| ~ spl144_72
| spl144_190 ),
inference(forward_subsumption_resolution,[],[f39824,f36683]) ).
fof(f39828,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),X0),sK21) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| spl144_190 ),
inference(forward_subsumption_resolution,[],[f39826,f36678]) ).
fof(f39830,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF136)
| ~ m1_subset_1(sK17(sK20,sK21),u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),X0),sK21) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| spl144_190 ),
inference(forward_demodulation,[],[f39828,f36734]) ).
fof(f39832,plain,
( ! [X0] :
( ~ m1_subset_1(sK17(sK20,sK21),sF136)
| ~ m1_subset_1(X0,sF136)
| ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),X0),sK21) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| spl144_190 ),
inference(forward_demodulation,[],[f39830,f36734]) ).
fof(f39834,plain,
( ! [X0] :
( ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),X0),sK21)
| ~ m1_subset_1(X0,sF136) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| spl144_190 ),
inference(forward_subsumption_resolution,[],[f39832,f37353]) ).
fof(f39837,plain,
( ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| spl144_190 ),
inference(unit_resulting_resolution,[],[f39834,f37359]) ).
fof(f39842,plain,
( $false
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| spl144_190
| ~ spl144_315 ),
inference(forward_subsumption_resolution,[],[f39837,f39713]) ).
fof(f39843,plain,
( ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| spl144_190
| ~ spl144_315 ),
inference(avatar_contradiction_clause,[],[f39842]) ).
fof(f39852,plain,
( ! [X0,X1] :
( ~ m2_filter_2(sK21,X0)
| ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r2_hidden(k3_lattices(X0,X1,sK18(sK20,sK21)),sK21)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) )
| spl144_189 ),
inference(resolution,[],[f38410,f36777]) ).
fof(f39859,plain,
( ! [X0] :
( ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(sK19))
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,X0,sK18(sK20,sK21)),sK21)
| v3_struct_0(sK19)
| ~ v10_lattices(sK19)
| ~ l3_lattices(sK19) )
| ~ spl144_72
| spl144_189 ),
inference(resolution,[],[f39852,f36713]) ).
fof(f39866,plain,
( ! [X0] :
( ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(sK19))
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,X0,sK18(sK20,sK21)),sK21)
| ~ v10_lattices(sK19)
| ~ l3_lattices(sK19) )
| spl144_67
| ~ spl144_72
| spl144_189 ),
inference(forward_subsumption_resolution,[],[f39859,f36688]) ).
fof(f39868,plain,
( ! [X0] :
( ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(sK19))
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,X0,sK18(sK20,sK21)),sK21)
| ~ l3_lattices(sK19) )
| ~ spl144_66
| spl144_67
| ~ spl144_72
| spl144_189 ),
inference(forward_subsumption_resolution,[],[f39866,f36683]) ).
fof(f39870,plain,
( ! [X0] :
( ~ m1_subset_1(sK18(sK20,sK21),u1_struct_0(sK19))
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,X0,sK18(sK20,sK21)),sK21) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| spl144_189 ),
inference(forward_subsumption_resolution,[],[f39868,f36678]) ).
fof(f39872,plain,
( ! [X0] :
( ~ m1_subset_1(sK18(sK20,sK21),sF136)
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,X0,sK18(sK20,sK21)),sK21) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| spl144_189 ),
inference(forward_demodulation,[],[f39870,f36734]) ).
fof(f39874,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ r2_hidden(k3_lattices(sK19,X0,sK18(sK20,sK21)),sK21) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_134
| spl144_189 ),
inference(forward_subsumption_resolution,[],[f39872,f37359]) ).
fof(f39876,plain,
( ! [X0] :
( ~ r2_hidden(k3_lattices(sK19,X0,sK18(sK20,sK21)),sK21)
| ~ m1_subset_1(X0,sF136) )
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_134
| spl144_189 ),
inference(forward_demodulation,[],[f39874,f36734]) ).
fof(f39878,plain,
( ~ r2_hidden(k3_lattices(sK19,sK17(sK20,sK21),sK18(sK20,sK21)),sK21)
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| spl144_189 ),
inference(unit_resulting_resolution,[],[f39876,f37353]) ).
fof(f39884,plain,
( $false
| ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| spl144_189
| ~ spl144_315 ),
inference(forward_subsumption_resolution,[],[f39878,f39713]) ).
fof(f39885,plain,
( ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| spl144_189
| ~ spl144_315 ),
inference(avatar_contradiction_clause,[],[f39884]) ).
cnf(s65,plain,
spl144_65,
inference(sat_conversion,[],[f36679]) ).
cnf(s66,plain,
spl144_66,
inference(sat_conversion,[],[f36684]) ).
cnf(s67,plain,
~ spl144_67,
inference(sat_conversion,[],[f36689]) ).
cnf(s68,plain,
spl144_68,
inference(sat_conversion,[],[f36694]) ).
cnf(s69,plain,
spl144_69,
inference(sat_conversion,[],[f36699]) ).
cnf(s70,plain,
~ spl144_70,
inference(sat_conversion,[],[f36704]) ).
cnf(s71,plain,
spl144_71,
inference(sat_conversion,[],[f36709]) ).
cnf(s72,plain,
spl144_72,
inference(sat_conversion,[],[f36714]) ).
cnf(s73,plain,
~ spl144_73,
inference(sat_conversion,[],[f36719]) ).
cnf(s74,plain,
spl144_74,
inference(sat_conversion,[],[f36735]) ).
cnf(s75,plain,
spl144_75,
inference(sat_conversion,[],[f36740]) ).
cnf(s76,plain,
spl144_76,
inference(sat_conversion,[],[f36745]) ).
cnf(s77,plain,
spl144_77,
inference(sat_conversion,[],[f36750]) ).
cnf(s78,plain,
spl144_78,
inference(sat_conversion,[],[f36755]) ).
cnf(s79,plain,
spl144_79,
inference(sat_conversion,[],[f36760]) ).
cnf(s80,plain,
spl144_80,
inference(sat_conversion,[],[f36765]) ).
cnf(s81,plain,
spl144_81,
inference(sat_conversion,[],[f36770]) ).
cnf(s82,plain,
( ~ spl144_71
| ~ spl144_81
| spl144_82 ),
inference(sat_conversion,[],[f36793]) ).
cnf(s91,plain,
( ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| spl144_87 ),
inference(sat_conversion,[],[f36861]) ).
cnf(s93,plain,
( ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_74
| ~ spl144_87
| spl144_88 ),
inference(sat_conversion,[],[f36873]) ).
cnf(s103,plain,
( ~ spl144_65
| ~ spl144_68
| ~ spl144_74
| ~ spl144_75
| ~ spl144_76
| ~ spl144_77
| ~ spl144_78
| ~ spl144_79
| ~ spl144_80
| ~ spl144_82
| spl144_93 ),
inference(sat_conversion,[],[f36942]) ).
cnf(s104,plain,
( ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_94 ),
inference(sat_conversion,[],[f36951]) ).
cnf(s137,plain,
( ~ spl144_65
| spl144_67
| ~ spl144_74
| spl144_118 ),
inference(sat_conversion,[],[f37237]) ).
cnf(s139,plain,
( ~ spl144_68
| spl144_70
| ~ spl144_78
| ~ spl144_93
| spl144_119 ),
inference(sat_conversion,[],[f37244]) ).
cnf(s141,plain,
( ~ spl144_118
| ~ spl144_119
| spl144_120 ),
inference(sat_conversion,[],[f37250]) ).
cnf(s152,plain,
( ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120
| spl144_133 ),
inference(sat_conversion,[],[f37354]) ).
cnf(s153,plain,
( ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120
| spl144_134 ),
inference(sat_conversion,[],[f37360]) ).
cnf(s261,plain,
( ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| ~ spl144_120
| ~ spl144_189
| ~ spl144_190
| ~ spl144_191 ),
inference(sat_conversion,[],[f38419]) ).
cnf(s262,plain,
( ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120
| spl144_189
| spl144_191 ),
inference(sat_conversion,[],[f38433]) ).
cnf(s410,plain,
( ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_74
| ~ spl144_118
| ~ spl144_133
| ~ spl144_134
| spl144_309 ),
inference(sat_conversion,[],[f39642]) ).
cnf(s413,plain,
( ~ spl144_68
| ~ spl144_69
| spl144_70
| ~ spl144_78
| ~ spl144_93
| ~ spl144_118
| ~ spl144_120
| ~ spl144_133
| ~ spl144_134
| ~ spl144_309
| spl144_312 ),
inference(sat_conversion,[],[f39669]) ).
cnf(s416,plain,
( spl144_191
| ~ spl144_312
| ~ spl144_315 ),
inference(sat_conversion,[],[f39715]) ).
cnf(s419,plain,
( ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| ~ spl144_189
| ~ spl144_190
| spl144_315 ),
inference(sat_conversion,[],[f39746]) ).
cnf(s421,plain,
( ~ spl144_68
| ~ spl144_69
| spl144_70
| spl144_73
| ~ spl144_78
| ~ spl144_88
| spl144_94
| ~ spl144_120
| spl144_190
| spl144_191 ),
inference(sat_conversion,[],[f39764]) ).
cnf(s422,plain,
( ~ spl144_191
| ~ spl144_312
| spl144_315 ),
inference(sat_conversion,[],[f39765]) ).
cnf(s427,plain,
( ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| spl144_190
| ~ spl144_315 ),
inference(sat_conversion,[],[f39843]) ).
cnf(s429,plain,
( ~ spl144_65
| ~ spl144_66
| spl144_67
| ~ spl144_72
| ~ spl144_74
| ~ spl144_133
| ~ spl144_134
| spl144_189
| ~ spl144_315 ),
inference(sat_conversion,[],[f39885]) ).
cnf(s431,plain,
spl144_82,
inference(rat,[],[s82,s81,s71]) ).
cnf(s452,plain,
spl144_118,
inference(rat,[],[s137,s67,s74,s65]) ).
cnf(s459,plain,
~ spl144_94,
inference(rat,[],[s104,s66,s72,s67,s65]) ).
cnf(s460,plain,
spl144_93,
inference(rat,[],[s103,s68,s431,s80,s79,s78,s77,s76,s75,s74,s65]) ).
cnf(s462,plain,
spl144_87,
inference(rat,[],[s91,s66,s72,s67,s65]) ).
cnf(s475,plain,
spl144_119,
inference(rat,[],[s139,s68,s70,s78,s460]) ).
cnf(s482,plain,
spl144_88,
inference(rat,[],[s93,s65,s66,s74,s67,s462]) ).
cnf(s495,plain,
spl144_120,
inference(rat,[],[s141,s452,s475]) ).
cnf(s523,plain,
spl144_134,
inference(rat,[],[s153,s482,s459,s68,s69,s78,s73,s70,s495]) ).
cnf(s524,plain,
spl144_133,
inference(rat,[],[s152,s482,s459,s68,s69,s78,s73,s70,s495]) ).
cnf(s533,plain,
spl144_309,
inference(rat,[],[s410,s523,s452,s65,s66,s74,s67,s524]) ).
cnf(s569,plain,
spl144_312,
inference(rat,[],[s413,s524,s523,s495,s460,s452,s68,s69,s78,s70,s533]) ).
cnf(s575,plain,
spl144_189,
inference(rat,[],[s422,s429,s262,s569,s67,s72,s74,s66,s65,s523,s524,s70,s73,s78,s69,s68,s459,s482,s495]) ).
cnf(s577,plain,
spl144_190,
inference(rat,[],[s422,s427,s421,s569,s67,s72,s74,s66,s65,s523,s524,s70,s73,s78,s69,s68,s459,s482,s495]) ).
cnf(s579,plain,
~ spl144_191,
inference(rat,[],[s261,s575,s495,s482,s68,s69,s78,s73,s70,s577]) ).
cnf(s580,plain,
spl144_315,
inference(rat,[],[s419,s575,s524,s523,s65,s66,s74,s72,s67,s577]) ).
cnf(s581,plain,
$false,
inference(rat,[],[s416,s569,s580,s579]) ).
fof(f39891,plain,
$false,
inference(avatar_sat_refutation,[],[s581]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT299+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.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 14:28:19 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 18.53/5.33 % (3621941)Detected formulas, will run a generic FOF schedule.
% 18.53/5.33 % (3621946)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=1723460328:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 18.53/5.33 % (3621948)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=3810115344:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 18.53/5.33 % (3621947)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=4274607958:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 18.53/5.33 % (3621949)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4240331662:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 18.53/5.33 % (3621952)dis-21_1_sil=8000:lcm=predicate:random_seed=3773608564: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)
% 18.53/5.33 % (3621951)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4182425780:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 18.53/5.33 % (3621950)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2179898860:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 18.53/5.33 % (3621951)Instruction limit reached!
% 18.53/5.33 % (3621951)------------------------------
% 18.53/5.33 % (3621951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/5.33 % (3621951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/5.33 % (3621951)CaDiCaL version: 2.1.3
% 18.53/5.33 % (3621951)Termination reason: Instruction limit
% 18.53/5.33 % (3621951)Termination phase: Property scanning
% 18.53/5.33 % (3621951)Time elapsed: 0.061 s
% 18.53/5.33 % (3621951)Peak memory usage: 136 MB
% 18.53/5.33 % (3621951)Instructions burned: 139 (million)
% 18.53/5.33 % (3621949)Instruction limit reached!
% 18.53/5.33 % (3621949)------------------------------
% 18.53/5.33 % (3621949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/5.33 % (3621949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/5.33 % (3621949)CaDiCaL version: 2.1.3
% 18.53/5.33 % (3621949)Termination reason: Instruction limit
% 18.53/5.33 % (3621949)Termination phase: SInE selection
% 18.53/5.33 % (3621949)Time elapsed: 0.084 s
% 18.53/5.33 % (3621949)Peak memory usage: 136 MB
% 18.53/5.33 % (3621949)Instructions burned: 110 (million)
% 18.53/5.33 % (3621950)Instruction limit reached!
% 18.53/5.33 % (3621950)------------------------------
% 18.53/5.33 % (3621950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/5.33 % (3621950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/5.33 % (3621950)CaDiCaL version: 2.1.3
% 18.53/5.33 % (3621950)Termination reason: Instruction limit
% 18.53/5.33 % (3621950)Termination phase: SInE selection
% 18.53/5.33 % (3621950)Time elapsed: 0.083 s
% 18.53/5.33 % (3621950)Peak memory usage: 136 MB
% 18.53/5.33 % (3621950)Instructions burned: 119 (million)
% 18.53/5.33 % (3621952)Instruction limit reached!
% 18.53/5.33 % (3621952)------------------------------
% 18.53/5.33 % (3621952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/5.33 % (3621952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/5.33 % (3621952)CaDiCaL version: 2.1.3
% 18.53/5.33 % (3621952)Termination reason: Instruction limit
% 18.53/5.33 % (3621952)Termination phase: SInE selection
% 18.53/5.33 % (3621952)Time elapsed: 0.086 s
% 18.53/5.33 % (3621952)Peak memory usage: 136 MB
% 18.53/5.33 % (3621952)Instructions burned: 129 (million)
% 18.53/5.33 % (3621960)lrs+10_1_sil=8000:sp=occurrence:random_seed=3807698499:i=285:sd=3:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/285Mi)
% 18.53/5.33 % (3621961)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2822784713:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 18.53/5.33 % (3621962)lrs+1011_1_sil=32000:sp=occurrence:random_seed=16733986:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 18.53/5.33 % (3621963)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=4078980431:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 18.53/5.33 % (3621961)Instruction limit reached!
% 26.81/6.57 % (3621961)------------------------------
% 26.81/6.57 % (3621961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.57 % (3621961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.57 % (3621961)CaDiCaL version: 2.1.3
% 26.81/6.57 % (3621961)Termination reason: Instruction limit
% 26.81/6.57 % (3621961)Termination phase: Property scanning
% 26.81/6.57 % (3621961)Time elapsed: 0.070 s
% 26.81/6.57 % (3621961)Peak memory usage: 136 MB
% 26.81/6.57 % (3621961)Instructions burned: 158 (million)
% 26.81/6.57 % (3621963)Instruction limit reached!
% 26.81/6.57 % (3621963)------------------------------
% 26.81/6.57 % (3621963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.57 % (3621963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.57 % (3621963)CaDiCaL version: 2.1.3
% 26.81/6.57 % (3621963)Termination reason: Instruction limit
% 26.81/6.57 % (3621963)Termination phase: Property scanning
% 26.81/6.57 % (3621963)Time elapsed: 0.110 s
% 26.81/6.57 % (3621963)Peak memory usage: 136 MB
% 26.81/6.57 % (3621963)Instructions burned: 251 (million)
% 26.81/6.57 % (3621962)Refutation not found, incomplete strategy
% 26.81/6.57 % (3621962)------------------------------
% 26.81/6.57 % (3621962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.57 % (3621962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.57 % (3621962)CaDiCaL version: 2.1.3
% 26.81/6.57 % (3621962)Termination reason: Refutation not found, incomplete strategy
% 26.81/6.57 % (3621962)Time elapsed: 0.193 s
% 26.81/6.57 % (3621962)Peak memory usage: 142 MB
% 26.81/6.57 % (3621962)Instructions burned: 243 (million)
% 26.81/6.57 % (3621960)Instruction limit reached!
% 26.81/6.57 % (3621960)------------------------------
% 26.81/6.57 % (3621960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.57 % (3621960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.57 % (3621960)CaDiCaL version: 2.1.3
% 26.81/6.57 % (3621960)Termination reason: Instruction limit
% 26.81/6.57 % (3621960)Termination phase: Saturation
% 26.81/6.57 % (3621960)Time elapsed: 0.228 s
% 26.81/6.57 % (3621960)Peak memory usage: 141 MB
% 26.81/6.57 % (3621960)Instructions burned: 286 (million)
% 26.81/6.57 % (3621968)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=239595710:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 26.81/6.57 % (3621969)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1165692991:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 26.81/6.57 % (3621970)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=157796210:cts=off:i=113:fsr=off:ss=included:sgt=4_2971 on theBenchmark for (2971ds/113Mi)
% 26.81/6.57 % (3621968)Instruction limit reached!
% 26.81/6.57 % (3621968)------------------------------
% 26.81/6.57 % (3621968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.57 % (3621968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.57 % (3621968)CaDiCaL version: 2.1.3
% 26.81/6.57 % (3621968)Termination reason: Instruction limit
% 26.81/6.57 % (3621968)Termination phase: SInE selection
% 26.81/6.57 % (3621968)Time elapsed: 0.191 s
% 26.81/6.57 % (3621968)Peak memory usage: 137 MB
% 26.81/6.57 % (3621968)Instructions burned: 295 (million)
% 26.81/6.57 % (3621962)------------------------------
% 26.81/6.57 % (3621962)------------------------------
% 26.81/6.57 % (3621970)Instruction limit reached!
% 26.81/6.57 % (3621970)------------------------------
% 26.81/6.57 % (3621970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.57 % (3621970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.57 % (3621970)CaDiCaL version: 2.1.3
% 26.81/6.57 % (3621970)Termination reason: Instruction limit
% 26.81/6.57 % (3621970)Termination phase: SInE selection
% 26.81/6.57 % (3621970)Time elapsed: 0.087 s
% 26.81/6.57 % (3621970)Peak memory usage: 136 MB
% 26.81/6.57 % (3621970)Instructions burned: 113 (million)
% 26.81/6.57 % (3621974)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=530995642:i=127:av=off:fsr=off:sup=off_2969 on theBenchmark for (2969ds/127Mi)
% 26.81/6.57 % (3621975)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2808633011:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2969 on theBenchmark for (2969ds/114Mi)
% 26.81/6.57 % (3621976)lrs+10_1_sil=8000:sp=occurrence:random_seed=1012116976:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2968 on theBenchmark for (2968ds/907Mi)
% 52.15/10.09 % (3621975)Instruction limit reached!
% 52.15/10.09 % (3621975)------------------------------
% 52.15/10.09 % (3621975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.15/10.09 % (3621975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.15/10.09 % (3621975)CaDiCaL version: 2.1.3
% 52.15/10.09 % (3621975)Termination reason: Instruction limit
% 52.15/10.09 % (3621975)Termination phase: Property scanning
% 52.15/10.09 % (3621975)Time elapsed: 0.052 s
% 52.15/10.09 % (3621975)Peak memory usage: 136 MB
% 52.15/10.09 % (3621975)Instructions burned: 116 (million)
% 52.15/10.09 % (3621974)Instruction limit reached!
% 52.15/10.09 % (3621974)------------------------------
% 52.15/10.09 % (3621974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.15/10.09 % (3621974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.15/10.09 % (3621974)CaDiCaL version: 2.1.3
% 52.15/10.09 % (3621974)Termination reason: Instruction limit
% 52.15/10.09 % (3621974)Termination phase: Preprocessing 1
% 52.15/10.09 % (3621974)Time elapsed: 0.096 s
% 52.15/10.09 % (3621974)Peak memory usage: 137 MB
% 52.15/10.09 % (3621974)Instructions burned: 128 (million)
% 52.15/10.09 % (3621980)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1774907119:i=437:sd=1:aac=none:ss=included_2966 on theBenchmark for (2966ds/437Mi)
% 52.15/10.09 % (3621981)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1355526096:i=5202:ss=axioms:sgt=16_2966 on theBenchmark for (2966ds/5202Mi)
% 52.15/10.09 % (3621980)Instruction limit reached!
% 52.15/10.09 % (3621980)------------------------------
% 52.15/10.09 % (3621980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.15/10.09 % (3621980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.15/10.09 % (3621980)CaDiCaL version: 2.1.3
% 52.15/10.09 % (3621980)Termination reason: Instruction limit
% 52.15/10.09 % (3621980)Termination phase: Saturation
% 52.15/10.09 % (3621980)Time elapsed: 0.300 s
% 52.15/10.09 % (3621980)Peak memory usage: 143 MB
% 52.15/10.09 % (3621980)Instructions burned: 437 (million)
% 52.15/10.09 % (3621976)Instruction limit reached!
% 52.15/10.09 % (3621976)------------------------------
% 52.15/10.09 % (3621976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.15/10.09 % (3621976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.15/10.09 % (3621976)CaDiCaL version: 2.1.3
% 52.15/10.09 % (3621976)Termination reason: Instruction limit
% 52.15/10.09 % (3621976)Termination phase: Property scanning
% 52.15/10.09 % (3621976)Time elapsed: 0.559 s
% 52.15/10.09 % (3621976)Peak memory usage: 153 MB
% 52.15/10.09 % (3621976)Instructions burned: 909 (million)
% 52.15/10.09 % (3621984)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=913164763:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2962 on theBenchmark for (2962ds/134Mi)
% 52.15/10.09 % (3621985)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=860720331:st=8:i=592:sd=3:ep=RST:ss=axioms_2961 on theBenchmark for (2961ds/592Mi)
% 52.15/10.09 % (3621984)Instruction limit reached!
% 52.15/10.09 % (3621984)------------------------------
% 52.15/10.09 % (3621984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.15/10.09 % (3621984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.15/10.09 % (3621984)CaDiCaL version: 2.1.3
% 52.15/10.09 % (3621984)Termination reason: Instruction limit
% 52.15/10.09 % (3621984)Termination phase: SInE selection
% 52.15/10.09 % (3621984)Time elapsed: 0.100 s
% 52.15/10.09 % (3621984)Peak memory usage: 136 MB
% 52.15/10.09 % (3621984)Instructions burned: 137 (million)
% 52.15/10.09 % (3621988)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=954988474:st=3:i=13193:sd=3:ss=axioms_2959 on theBenchmark for (2959ds/13193Mi)
% 52.15/10.09 % (3621985)Instruction limit reached!
% 52.15/10.09 % (3621985)------------------------------
% 52.15/10.09 % (3621985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.15/10.09 % (3621985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.15/10.09 % (3621985)CaDiCaL version: 2.1.3
% 52.15/10.09 % (3621985)Termination reason: Instruction limit
% 52.15/10.09 % (3621985)Termination phase: Naming
% 52.15/10.09 % (3621985)Time elapsed: 0.450 s
% 52.15/10.09 % (3621985)Peak memory usage: 154 MB
% 52.15/10.09 % (3621985)Instructions burned: 594 (million)
% 52.15/10.09 % (3621969)Instruction limit reached!
% 52.15/10.09 % (3621969)------------------------------
% 23.95/12.12 % (3621969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3621969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3621969)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3621969)Termination reason: Instruction limit
% 23.95/12.12 % (3621969)Termination phase: Property scanning
% 23.95/12.12 % (3621969)Time elapsed: 1.555 s
% 23.95/12.12 % (3621969)Peak memory usage: 233 MB
% 23.95/12.12 % (3621969)Instructions burned: 2353 (million)
% 23.95/12.12 % (3621990)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=1891055987:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/125Mi)
% 23.95/12.12 % (3621991)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2727452954:i=134:gtgl=5:slsql=off:gtg=exists_sym_2955 on theBenchmark for (2955ds/134Mi)
% 23.95/12.12 % (3621990)Instruction limit reached!
% 23.95/12.12 % (3621990)------------------------------
% 23.95/12.12 % (3621990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3621990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3621990)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3621990)Termination reason: Instruction limit
% 23.95/12.12 % (3621990)Termination phase: Property scanning
% 23.95/12.12 % (3621990)Time elapsed: 0.057 s
% 23.95/12.12 % (3621990)Peak memory usage: 136 MB
% 23.95/12.12 % (3621990)Instructions burned: 127 (million)
% 23.95/12.12 % (3621991)Instruction limit reached!
% 23.95/12.12 % (3621991)------------------------------
% 23.95/12.12 % (3621991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3621991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3621991)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3621991)Termination reason: Instruction limit
% 23.95/12.12 % (3621991)Termination phase: Property scanning
% 23.95/12.12 % (3621991)Time elapsed: 0.060 s
% 23.95/12.12 % (3621991)Peak memory usage: 136 MB
% 23.95/12.12 % (3621991)Instructions burned: 134 (million)
% 23.95/12.12 % (3621994)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=615993508:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/141Mi)
% 23.95/12.12 % (3621995)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=256224639:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2952 on theBenchmark for (2952ds/431Mi)
% 23.95/12.12 % (3621994)Instruction limit reached!
% 23.95/12.12 % (3621994)------------------------------
% 23.95/12.12 % (3621994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3621994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3621994)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3621994)Termination reason: Instruction limit
% 23.95/12.12 % (3621994)Termination phase: SInE selection
% 23.95/12.12 % (3621994)Time elapsed: 0.106 s
% 23.95/12.12 % (3621994)Peak memory usage: 136 MB
% 23.95/12.12 % (3621994)Instructions burned: 142 (million)
% 23.95/12.12 % (3621995)Refutation not found, incomplete strategy
% 23.95/12.12 % (3621995)------------------------------
% 23.95/12.12 % (3621995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3621995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3621995)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3621995)Termination reason: Refutation not found, incomplete strategy
% 23.95/12.12 % (3621995)Time elapsed: 0.209 s
% 23.95/12.12 % (3621995)Peak memory usage: 142 MB
% 23.95/12.12 % (3621995)Instructions burned: 248 (million)
% 23.95/12.12 % (3621998)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=4039007660:i=6060:aac=none:ins=25_2950 on theBenchmark for (2950ds/6060Mi)
% 23.95/12.12 % (3621995)------------------------------
% 23.95/12.12 % (3621995)------------------------------
% 23.95/12.12 % (3622000)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=1402458028:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2945 on theBenchmark for (2945ds/150Mi)
% 23.95/12.12 % (3622000)Instruction limit reached!
% 23.95/12.12 % (3622000)------------------------------
% 23.95/12.12 % (3622000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3622000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3622000)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3622000)Termination reason: Instruction limit
% 23.95/12.12 % (3622000)Termination phase: SInE selection
% 23.95/12.12 % (3622000)Time elapsed: 0.123 s
% 23.95/12.12 % (3622000)Peak memory usage: 136 MB
% 23.95/12.12 % (3622000)Instructions burned: 150 (million)
% 23.95/12.12 % (3622002)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3772283489:i=14155:bd=all_2942 on theBenchmark for (2942ds/14155Mi)
% 23.95/12.12 % (3621981)Instruction limit reached!
% 23.95/12.12 % (3621981)------------------------------
% 23.95/12.12 % (3621981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3621981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3621981)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3621981)Termination reason: Instruction limit
% 23.95/12.12 % (3621981)Termination phase: Saturation
% 23.95/12.12 % (3621981)Time elapsed: 3.862 s
% 23.95/12.12 % (3621981)Peak memory usage: 524 MB
% 23.95/12.12 % (3621981)Instructions burned: 5205 (million)
% 23.95/12.12 % (3622004)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3412433272:i=667:av=off:fsr=off_2926 on theBenchmark for (2926ds/667Mi)
% 23.95/12.12 % (3622004)Instruction limit reached!
% 23.95/12.12 % (3622004)------------------------------
% 23.95/12.12 % (3622004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3622004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3622004)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3622004)Termination reason: Instruction limit
% 23.95/12.12 % (3622004)Termination phase: NewCNF
% 23.95/12.12 % (3622004)Time elapsed: 0.545 s
% 23.95/12.12 % (3622004)Peak memory usage: 185 MB
% 23.95/12.12 % (3622004)Instructions burned: 667 (million)
% 23.95/12.12 % (3622006)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=94359852:s2a=on:i=185:s2at=1.8:fdi=4_2918 on theBenchmark for (2918ds/185Mi)
% 23.95/12.12 % (3622006)Instruction limit reached!
% 23.95/12.12 % (3622006)------------------------------
% 23.95/12.12 % (3622006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3622006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3622006)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3622006)Termination reason: Instruction limit
% 23.95/12.12 % (3622006)Termination phase: SInE selection
% 23.95/12.12 % (3622006)Time elapsed: 0.134 s
% 23.95/12.12 % (3622006)Peak memory usage: 136 MB
% 23.95/12.12 % (3622006)Instructions burned: 185 (million)
% 23.95/12.12 % (3622008)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2236722709:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2915 on theBenchmark for (2915ds/193Mi)
% 23.95/12.12 % (3622008)Instruction limit reached!
% 23.95/12.12 % (3622008)------------------------------
% 23.95/12.12 % (3622008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3622008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3622008)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3622008)Termination reason: Instruction limit
% 23.95/12.12 % (3622008)Termination phase: SInE selection
% 23.95/12.12 % (3622008)Time elapsed: 0.154 s
% 23.95/12.12 % (3622008)Peak memory usage: 136 MB
% 23.95/12.12 % (3622008)Instructions burned: 194 (million)
% 23.95/12.12 % (3622010)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1850928684:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2911 on theBenchmark for (2911ds/4850Mi)
% 23.95/12.12 % (3621998)Instruction limit reached!
% 23.95/12.12 % (3621998)------------------------------
% 23.95/12.12 % (3621998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/12.12 % (3621998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/12.12 % (3621998)CaDiCaL version: 2.1.3
% 23.95/12.12 % (3621998)Termination reason: Instruction limit
% 23.95/12.12 % (3621998)Termination phase: Function definition elimination
% 23.95/12.12 % (3621998)Time elapsed: 3.892 s
% 23.95/12.12 % (3621998)Peak memory usage: 244 MB
% 23.95/12.12 % (3621998)Instructions burned: 6061 (million)
% 23.95/12.12 % (3622012)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1494192289:i=12111:sd=1:ss=included_2909 on theBenchmark for (2909ds/12111Mi)
% 23.95/12.12 % (3622012)First to succeed.
% 23.95/12.12 % (3622012)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3621941"
% 23.95/12.12 % (3622012)Refutation found. Thanks to Tanya!
% 23.95/12.12 % SZS status Theorem for theBenchmark
% 23.95/12.12 % SZS output start Proof for theBenchmark
% See solution above
% 66.42/12.37 % (3622012)------------------------------
% 66.42/12.37 % (3622012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.42/12.37 % (3622012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.42/12.37 % (3622012)CaDiCaL version: 2.1.3
% 66.42/12.37 % (3622012)Termination reason: Refutation
% 66.42/12.37 % (3622012)Time elapsed: 1.577 s
% 66.42/12.37 % (3622012)Peak memory usage: 208 MB
% 66.42/12.37 % (3622012)Instructions burned: 2256 (million)
% 66.42/12.37 % (3622012)------------------------------
% 66.42/12.37 % (3622012)------------------------------
% 66.42/12.37 % (3621941)Success in time 11.26 s
% 66.42/12.37 % Vampire exiting
%------------------------------------------------------------------------------