%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT325+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:57 AM UTC 2026
% Result : Theorem 13.98s 5.51s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 65
% Syntax : Number of formulae : 473 ( 72 unt; 24 def)
% Number of atoms : 1767 ( 192 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 2202 ( 908 ~;1091 |; 109 &)
% ( 38 <=>; 56 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 43 ( 41 usr; 20 prp; 0-3 aty)
% Number of functors : 33 ( 33 usr; 8 con; 0-6 aty)
% Number of variables : 686 ( 1 sgn 675 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( v1_funct_1(k1_realset1(u2_lattices(X0),X1))
& v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(k1_realset1(u1_lattices(X0),X1))
& v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t61_filter_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( v1_funct_1(k1_realset1(u2_lattices(X0),X1))
& v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(k1_realset1(u1_lattices(X0),X1))
& v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f5,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f7,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f10,axiom,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f13,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( m2_lattice4(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(k4_lattices(X0,X2,X3),X1)
& r2_hidden(k3_lattices(X0,X2,X3),X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_lattice4) ).
fof(f14,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ! [X1,X2] : k1_binop_1(X0,X1,X2) = k1_funct_1(X0,k4_tarski(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_binop_1) ).
fof(f15,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> ( ( ( X1 = k1_xboole_0
=> X0 = k1_xboole_0 )
=> ( v1_funct_2(X2,X0,X1)
<=> X0 = k4_relset_1(X0,X1,X2) ) )
& ( X1 = k1_xboole_0
=> ( X0 = k1_xboole_0
| ( v1_funct_2(X2,X0,X1)
<=> X2 = k1_xboole_0 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_funct_2) ).
fof(f16,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_lattices) ).
fof(f17,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_lattices) ).
fof(f18,axiom,
! [X0] :
( v1_relat_1(X0)
=> ! [X1] : k1_realset1(X0,X1) = k7_relat_1(X0,k2_zfmisc_1(X1,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_realset1) ).
fof(f19,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f20,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ! [X1] :
( X1 = k2_relat_1(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ? [X3] :
( r2_hidden(X3,k1_relat_1(X0))
& X2 = k1_funct_1(X0,X3) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_funct_1) ).
fof(f21,axiom,
! [X0,X1] : k4_tarski(X0,X1) = k2_tarski(k2_tarski(X0,X1),k1_tarski(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f22,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(X1)) )
=> m1_subset_1(k12_mcart_1(X0,X1,X2,X3),k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k12_mcart_1) ).
fof(f41,axiom,
! [X0,X1] :
( v1_relat_1(X0)
=> v1_relat_1(k7_relat_1(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_relat_1) ).
fof(f44,axiom,
! [X0] :
( l2_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_lattices) ).
fof(f45,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f49,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/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f50,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f51,axiom,
! [X0] :
( l1_lattices(X0)
=> ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_lattices) ).
fof(f53,axiom,
! [X0] :
( l2_lattices(X0)
=> ( v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u2_lattices) ).
fof(f63,axiom,
! [X0,X1] :
( v1_relat_1(X0)
=> v1_relat_1(k1_realset1(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_realset1) ).
fof(f64,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f66,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f68,axiom,
! [X0,X1] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ( v1_relat_1(k1_realset1(X0,X1))
& v1_funct_1(k1_realset1(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_realset1) ).
fof(f73,axiom,
! [X0,X1] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ( v1_relat_1(k7_relat_1(X0,X1))
& v1_funct_1(k7_relat_1(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_funct_1) ).
fof(f89,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(X1)) )
=> k12_mcart_1(X0,X1,X2,X3) = k2_zfmisc_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k12_mcart_1) ).
fof(f91,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( ~ v1_xboole_0(X0)
& ~ v1_xboole_0(X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
& m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
& m1_subset_1(X4,X0)
& m1_subset_1(X5,X1) )
=> k2_binop_1(X0,X1,X2,X3,X4,X5) = k1_binop_1(X3,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_binop_1) ).
fof(f92,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& l2_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> k3_lattices(X0,X1,X2) = k1_lattices(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k3_lattices) ).
fof(f93,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& l1_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_lattices) ).
fof(f94,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> k4_relset_1(X0,X1,X2) = k1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_relset_1) ).
fof(f96,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f97,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f98,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( ( r1_tarski(k1_relat_1(X2),X0)
& r1_tarski(k2_relat_1(X2),X1) )
=> m2_relset_1(X2,X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_relset_1) ).
fof(f100,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f101,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f102,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f105,axiom,
! [X0,X1,X2] :
( ( v1_relat_1(X2)
& v1_funct_1(X2) )
=> ( r2_hidden(X1,k1_relat_1(k7_relat_1(X2,X0)))
=> k1_funct_1(k7_relat_1(X2,X0),X1) = k1_funct_1(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t70_funct_1) ).
fof(f106,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f108,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> ( r1_tarski(X0,k1_relat_1(X1))
=> k1_relat_1(k7_relat_1(X1,X0)) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t91_relat_1) ).
fof(f109,axiom,
! [X0,X1] :
( ~ v1_xboole_0(X1)
=> ! [X2] :
( ~ v1_xboole_0(X2)
=> ~ ( r2_hidden(X0,k2_zfmisc_1(X1,X2))
& ! [X3] :
( m1_subset_1(X3,X1)
=> ! [X4] :
( m1_subset_1(X4,X2)
=> X0 != k4_tarski(X3,X4) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_domain_1) ).
fof(f110,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f97]) ).
fof(f122,plain,
? [X0] :
( ? [X1] :
( ( ~ v1_funct_1(k1_realset1(u2_lattices(X0),X1))
| ~ v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(u1_lattices(X0),X1))
| ~ v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1) )
& ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f123,plain,
? [X0] :
( ? [X1] :
( ( ~ v1_funct_1(k1_realset1(u2_lattices(X0),X1))
| ~ v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(u1_lattices(X0),X1))
| ~ v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1) )
& ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f122]) ).
fof(f126,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f5]) ).
fof(f127,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f126]) ).
fof(f129,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f7]) ).
fof(f138,plain,
! [X0] :
( ! [X1] :
( ( m2_lattice4(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( r2_hidden(k4_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)) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f139,plain,
! [X0] :
( ! [X1] :
( ( m2_lattice4(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( r2_hidden(k4_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)) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f138]) ).
fof(f140,plain,
! [X0] :
( ! [X1,X2] : k1_binop_1(X0,X1,X2) = k1_funct_1(X0,k4_tarski(X1,X2))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f141,plain,
! [X0] :
( ! [X1,X2] : k1_binop_1(X0,X1,X2) = k1_funct_1(X0,k4_tarski(X1,X2))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f140]) ).
fof(f142,plain,
! [X0,X1,X2] :
( ( ( ( v1_funct_2(X2,X0,X1)
<=> X0 = k4_relset_1(X0,X1,X2) )
| ( k1_xboole_0 != X0
& X1 = k1_xboole_0 ) )
& ( X0 = k1_xboole_0
| ( v1_funct_2(X2,X0,X1)
<=> X2 = k1_xboole_0 )
| k1_xboole_0 != X1 ) )
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f15]) ).
fof(f143,plain,
! [X0,X1,X2] :
( ( ( ( v1_funct_2(X2,X0,X1)
<=> X0 = k4_relset_1(X0,X1,X2) )
| ( k1_xboole_0 != X0
& X1 = k1_xboole_0 ) )
& ( X0 = k1_xboole_0
| ( v1_funct_2(X2,X0,X1)
<=> X2 = k1_xboole_0 )
| k1_xboole_0 != X1 ) )
| ~ m2_relset_1(X2,X0,X1) ),
inference(flattening,[],[f142]) ).
fof(f144,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f145,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f144]) ).
fof(f146,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f147,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f146]) ).
fof(f148,plain,
! [X0] :
( ! [X1] : k1_realset1(X0,X1) = k7_relat_1(X0,k2_zfmisc_1(X1,X1))
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f149,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f150,plain,
! [X0] :
( ! [X1] :
( X1 = k2_relat_1(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ? [X3] :
( r2_hidden(X3,k1_relat_1(X0))
& X2 = k1_funct_1(X0,X3) ) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f151,plain,
! [X0] :
( ! [X1] :
( X1 = k2_relat_1(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ? [X3] :
( r2_hidden(X3,k1_relat_1(X0))
& X2 = k1_funct_1(X0,X3) ) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f150]) ).
fof(f152,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k12_mcart_1(X0,X1,X2,X3),k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1)) ),
inference(ennf_transformation,[],[f22]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k12_mcart_1(X0,X1,X2,X3),k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1)) ),
inference(flattening,[],[f152]) ).
fof(f167,plain,
! [X0,X1] :
( v1_relat_1(k7_relat_1(X0,X1))
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f169,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f170,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f45]) ).
fof(f173,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,[],[f49]) ).
fof(f174,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,[],[f173]) ).
fof(f175,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f50]) ).
fof(f176,plain,
! [X0] :
( ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f51]) ).
fof(f177,plain,
! [X0] :
( ( v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f182,plain,
! [X0,X1] :
( v1_relat_1(k1_realset1(X0,X1))
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f63]) ).
fof(f183,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f64]) ).
fof(f184,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f183]) ).
fof(f187,plain,
! [X0,X1] :
( ( v1_relat_1(k1_realset1(X0,X1))
& v1_funct_1(k1_realset1(X0,X1)) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f68]) ).
fof(f188,plain,
! [X0,X1] :
( ( v1_relat_1(k1_realset1(X0,X1))
& v1_funct_1(k1_realset1(X0,X1)) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f187]) ).
fof(f191,plain,
! [X0,X1] :
( ( v1_relat_1(k7_relat_1(X0,X1))
& v1_funct_1(k7_relat_1(X0,X1)) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f73]) ).
fof(f192,plain,
! [X0,X1] :
( ( v1_relat_1(k7_relat_1(X0,X1))
& v1_funct_1(k7_relat_1(X0,X1)) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f191]) ).
fof(f204,plain,
! [X0,X1,X2,X3] :
( k12_mcart_1(X0,X1,X2,X3) = k2_zfmisc_1(X2,X3)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1)) ),
inference(ennf_transformation,[],[f89]) ).
fof(f205,plain,
! [X0,X1,X2,X3] :
( k12_mcart_1(X0,X1,X2,X3) = k2_zfmisc_1(X2,X3)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1)) ),
inference(flattening,[],[f204]) ).
fof(f208,plain,
! [X0,X1,X2,X3,X4,X5] :
( k2_binop_1(X0,X1,X2,X3,X4,X5) = k1_binop_1(X3,X4,X5)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_subset_1(X4,X0)
| ~ m1_subset_1(X5,X1) ),
inference(ennf_transformation,[],[f91]) ).
fof(f209,plain,
! [X0,X1,X2,X3,X4,X5] :
( k2_binop_1(X0,X1,X2,X3,X4,X5) = k1_binop_1(X3,X4,X5)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_subset_1(X4,X0)
| ~ m1_subset_1(X5,X1) ),
inference(flattening,[],[f208]) ).
fof(f210,plain,
! [X0,X1,X2] :
( k3_lattices(X0,X1,X2) = k1_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f92]) ).
fof(f211,plain,
! [X0,X1,X2] :
( k3_lattices(X0,X1,X2) = k1_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f210]) ).
fof(f212,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f93]) ).
fof(f213,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f212]) ).
fof(f214,plain,
! [X0,X1,X2] :
( k4_relset_1(X0,X1,X2) = k1_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f94]) ).
fof(f217,plain,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
| ~ r1_tarski(k1_relat_1(X2),X0)
| ~ r1_tarski(k2_relat_1(X2),X1)
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f98]) ).
fof(f218,plain,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
| ~ r1_tarski(k1_relat_1(X2),X0)
| ~ r1_tarski(k2_relat_1(X2),X1)
| ~ v1_relat_1(X2) ),
inference(flattening,[],[f217]) ).
fof(f220,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f100]) ).
fof(f221,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f220]) ).
fof(f222,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f102]) ).
fof(f223,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f222]) ).
fof(f226,plain,
! [X0,X1,X2] :
( k1_funct_1(k7_relat_1(X2,X0),X1) = k1_funct_1(X2,X1)
| ~ r2_hidden(X1,k1_relat_1(k7_relat_1(X2,X0)))
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) ),
inference(ennf_transformation,[],[f105]) ).
fof(f227,plain,
! [X0,X1,X2] :
( k1_funct_1(k7_relat_1(X2,X0),X1) = k1_funct_1(X2,X1)
| ~ r2_hidden(X1,k1_relat_1(k7_relat_1(X2,X0)))
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) ),
inference(flattening,[],[f226]) ).
fof(f228,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f106]) ).
fof(f230,plain,
! [X0,X1] :
( k1_relat_1(k7_relat_1(X1,X0)) = X0
| ~ r1_tarski(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f108]) ).
fof(f231,plain,
! [X0,X1] :
( k1_relat_1(k7_relat_1(X1,X0)) = X0
| ~ r1_tarski(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1) ),
inference(flattening,[],[f230]) ).
fof(f232,plain,
! [X0,X1] :
( ! [X2] :
( ~ r2_hidden(X0,k2_zfmisc_1(X1,X2))
| ? [X3] :
( ? [X4] :
( k4_tarski(X3,X4) = X0
& m1_subset_1(X4,X2) )
& m1_subset_1(X3,X1) )
| v1_xboole_0(X2) )
| v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f109]) ).
fof(f233,plain,
! [X0,X1] :
( ! [X2] :
( ~ r2_hidden(X0,k2_zfmisc_1(X1,X2))
| ? [X3] :
( ? [X4] :
( k4_tarski(X3,X4) = X0
& m1_subset_1(X4,X2) )
& m1_subset_1(X3,X1) )
| v1_xboole_0(X2) )
| v1_xboole_0(X1) ),
inference(flattening,[],[f232]) ).
fof(f234,plain,
( ~ m2_relset_1(k1_realset1(u1_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(k1_realset1(u1_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK0),sK1))
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(k1_realset1(u2_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(k1_realset1(u2_lattices(sK0),sK1)) ),
inference(cnf_transformation,[],[f123]) ).
fof(f235,plain,
m2_lattice4(sK1,sK0),
inference(cnf_transformation,[],[f123]) ).
fof(f236,plain,
~ v1_xboole_0(sK1),
inference(cnf_transformation,[],[f123]) ).
fof(f237,plain,
l3_lattices(sK0),
inference(cnf_transformation,[],[f123]) ).
fof(f238,plain,
v10_lattices(sK0),
inference(cnf_transformation,[],[f123]) ).
fof(f239,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f123]) ).
fof(f245,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v6_lattices(X0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f247,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v4_lattices(X0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f249,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f129]) ).
fof(f251,plain,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
inference(cnf_transformation,[],[f10]) ).
fof(f254,plain,
! [X2,X3,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ m2_lattice4(X1,X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f255,plain,
! [X2,X3,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ m2_lattice4(X1,X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f261,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_relat_1(X0)
| k1_binop_1(X0,X1,X2) = k1_funct_1(X0,k4_tarski(X1,X2)) ),
inference(cnf_transformation,[],[f141]) ).
fof(f264,plain,
! [X2,X0,X1] :
( k4_relset_1(X0,X1,X2) != X0
| k1_xboole_0 = X1
| ~ m2_relset_1(X2,X0,X1)
| v1_funct_2(X2,X0,X1) ),
inference(cnf_transformation,[],[f143]) ).
fof(f265,plain,
! [X2,X0,X1] :
( k4_relset_1(X0,X1,X2) = X0
| k1_xboole_0 = X1
| ~ m2_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1) ),
inference(cnf_transformation,[],[f143]) ).
fof(f268,plain,
! [X2,X0,X1] :
( k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f269,plain,
! [X2,X0,X1] :
( k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f270,plain,
! [X0,X1] :
( k1_realset1(X0,X1) = k7_relat_1(X0,k2_zfmisc_1(X1,X1))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f272,plain,
! [X0,X1] :
( r2_hidden(sK4(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f149]) ).
fof(f273,plain,
! [X0,X1] :
( ~ r2_hidden(sK4(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f149]) ).
fof(f277,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_relat_1(X0)
| k1_funct_1(X0,sK6(X0,X2)) = X2
| ~ r2_hidden(X2,X1)
| k2_relat_1(X0) != X1 ),
inference(cnf_transformation,[],[f151]) ).
fof(f278,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_relat_1(X0)
| r2_hidden(sK6(X0,X2),k1_relat_1(X0))
| ~ r2_hidden(X2,X1)
| k2_relat_1(X0) != X1 ),
inference(cnf_transformation,[],[f151]) ).
fof(f280,plain,
! [X0,X1] : k4_tarski(X0,X1) = k2_tarski(k2_tarski(X0,X1),k1_tarski(X0)),
inference(cnf_transformation,[],[f21]) ).
fof(f281,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k12_mcart_1(X0,X1,X2,X3),k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f289,plain,
! [X0,X1] :
( v1_relat_1(k7_relat_1(X0,X1))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f167]) ).
fof(f291,plain,
! [X0] :
( ~ l2_lattices(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f292,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f293,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f295,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_lattice4(X1,X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f174]) ).
fof(f296,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f175]) ).
fof(f297,plain,
! [X0] :
( m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f176]) ).
fof(f298,plain,
! [X0] :
( v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f176]) ).
fof(f299,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f176]) ).
fof(f300,plain,
! [X0] :
( m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f301,plain,
! [X0] :
( v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f302,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f312,plain,
! [X0,X1] :
( v1_relat_1(k1_realset1(X0,X1))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f182]) ).
fof(f313,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f184]) ).
fof(f315,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f66]) ).
fof(f319,plain,
! [X0,X1] :
( v1_funct_1(k1_realset1(X0,X1))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[],[f188]) ).
fof(f320,plain,
! [X0,X1] :
( v1_relat_1(k1_realset1(X0,X1))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[],[f188]) ).
fof(f328,plain,
! [X0,X1] :
( v1_funct_1(k7_relat_1(X0,X1))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[],[f192]) ).
fof(f360,plain,
! [X2,X3,X0,X1] :
( k12_mcart_1(X0,X1,X2,X3) = k2_zfmisc_1(X2,X3)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f205]) ).
fof(f362,plain,
! [X2,X3,X0,X1,X4,X5] :
( k2_binop_1(X0,X1,X2,X3,X4,X5) = k1_binop_1(X3,X4,X5)
| ~ m1_subset_1(X4,X0)
| ~ m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X5,X1) ),
inference(cnf_transformation,[],[f209]) ).
fof(f363,plain,
! [X2,X0,X1] :
( k3_lattices(X0,X1,X2) = k1_lattices(X0,X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l2_lattices(X0)
| ~ v4_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f211]) ).
fof(f364,plain,
! [X2,X0,X1] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f213]) ).
fof(f365,plain,
! [X2,X0,X1] :
( k4_relset_1(X0,X1,X2) = k1_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f214]) ).
fof(f368,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f96]) ).
fof(f369,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f96]) ).
fof(f370,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f110]) ).
fof(f371,plain,
! [X2,X0,X1] :
( ~ r1_tarski(k1_relat_1(X2),X0)
| ~ r1_tarski(k2_relat_1(X2),X1)
| ~ v1_relat_1(X2)
| m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f218]) ).
fof(f373,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f221]) ).
fof(f375,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f376,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f223]) ).
fof(f379,plain,
! [X2,X0,X1] :
( k1_funct_1(k7_relat_1(X2,X0),X1) = k1_funct_1(X2,X1)
| ~ v1_relat_1(X2)
| ~ r2_hidden(X1,k1_relat_1(k7_relat_1(X2,X0)))
| ~ v1_funct_1(X2) ),
inference(cnf_transformation,[],[f227]) ).
fof(f380,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f228]) ).
fof(f382,plain,
! [X0,X1] :
( k1_relat_1(k7_relat_1(X1,X0)) = X0
| ~ r1_tarski(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f231]) ).
fof(f383,plain,
! [X2,X0,X1] :
( m1_subset_1(sK30(X0,X1,X2),X2)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) ),
inference(cnf_transformation,[],[f233]) ).
fof(f384,plain,
! [X2,X0,X1] :
( v1_xboole_0(X1)
| v1_xboole_0(X2)
| k4_tarski(sK29(X0,X1,X2),sK30(X0,X1,X2)) = X0
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) ),
inference(cnf_transformation,[],[f233]) ).
fof(f385,plain,
! [X2,X0,X1] :
( m1_subset_1(sK29(X0,X1,X2),X1)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) ),
inference(cnf_transformation,[],[f233]) ).
fof(f386,plain,
! [X2,X0,X1] :
( k1_binop_1(X0,X1,X2) = k1_funct_1(X0,k2_tarski(k2_tarski(X1,X2),k1_tarski(X1)))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(definition_unfolding,[],[f261,f280]) ).
fof(f388,plain,
! [X2,X0,X1] :
( k2_tarski(k2_tarski(sK29(X0,X1,X2),sK30(X0,X1,X2)),k1_tarski(sK29(X0,X1,X2))) = X0
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) ),
inference(definition_unfolding,[],[f384,f280]) ).
fof(f396,plain,
! [X2,X0] :
( r2_hidden(sK6(X0,X2),k1_relat_1(X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| ~ r2_hidden(X2,k2_relat_1(X0)) ),
inference(equality_resolution,[],[f278]) ).
fof(f397,plain,
! [X2,X0] :
( k1_funct_1(X0,sK6(X0,X2)) = X2
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| ~ r2_hidden(X2,k2_relat_1(X0)) ),
inference(equality_resolution,[],[f277]) ).
fof(f398,definition,
sF31 = u1_lattices(sK0),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f399,plain,
u1_lattices(sK0) = sF31,
inference(reorient_equations,[],[f398]) ).
fof(f400,definition,
sF32 = k1_realset1(sF31,sK1),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f401,plain,
k1_realset1(sF31,sK1) = sF32,
inference(reorient_equations,[],[f400]) ).
fof(f402,definition,
sF33 = k2_zfmisc_1(sK1,sK1),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f403,plain,
k2_zfmisc_1(sK1,sK1) = sF33,
inference(reorient_equations,[],[f402]) ).
fof(f404,definition,
sF34 = u2_lattices(sK0),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f405,plain,
u2_lattices(sK0) = sF34,
inference(reorient_equations,[],[f404]) ).
fof(f406,definition,
sF35 = k1_realset1(sF34,sK1),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f407,plain,
k1_realset1(sF34,sK1) = sF35,
inference(reorient_equations,[],[f406]) ).
fof(f408,plain,
( ~ m2_relset_1(sF32,sF33,sK1)
| ~ v1_funct_2(sF32,sF33,sK1)
| ~ v1_funct_1(sF32)
| ~ m2_relset_1(sF35,sF33,sK1)
| ~ v1_funct_2(sF35,sF33,sK1)
| ~ v1_funct_1(sF35) ),
inference(definition_folding,[],[f234,f407,f405,f403,f407,f405,f403,f407,f405,f401,f399,f403,f401,f399,f403,f401,f399]) ).
fof(f409,plain,
! [X2,X3,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ m2_lattice4(X1,X0) ),
inference(forward_subsumption_resolution,[],[f254,f376]) ).
fof(f410,plain,
! [X2,X3,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ m2_lattice4(X1,X0) ),
inference(forward_subsumption_resolution,[],[f255,f376]) ).
fof(f411,plain,
! [X2,X3,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ m2_lattice4(X1,X0) ),
inference(forward_subsumption_resolution,[],[f409,f376]) ).
fof(f412,plain,
! [X2,X3,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ m2_lattice4(X1,X0) ),
inference(forward_subsumption_resolution,[],[f410,f376]) ).
fof(f413,plain,
! [X2,X3,X0,X1] :
( r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0) ),
inference(forward_subsumption_resolution,[],[f411,f295]) ).
fof(f414,plain,
! [X2,X3,X0,X1] :
( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0) ),
inference(forward_subsumption_resolution,[],[f412,f295]) ).
fof(f415,plain,
( v1_funct_2(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ l1_lattices(sK0) ),
inference(superposition,[],[f298,f399]) ).
fof(f416,plain,
( m2_relset_1(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ l1_lattices(sK0) ),
inference(superposition,[],[f297,f399]) ).
fof(f417,plain,
( v1_funct_2(sF34,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(superposition,[],[f301,f405]) ).
fof(f418,plain,
( m2_relset_1(sF34,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(superposition,[],[f300,f405]) ).
fof(f419,plain,
! [X0] :
( k1_realset1(X0,sK1) = k7_relat_1(X0,sF33)
| ~ v1_relat_1(X0) ),
inference(superposition,[],[f270,f403]) ).
fof(f420,plain,
l2_lattices(sK0),
inference(resolution,[],[f292,f237]) ).
fof(f421,plain,
v1_funct_2(sF34,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(backward_subsumption_resolution,[],[f417,f420]) ).
fof(f422,plain,
m2_relset_1(sF34,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(backward_subsumption_resolution,[],[f418,f420]) ).
fof(f423,plain,
l1_lattices(sK0),
inference(resolution,[],[f293,f237]) ).
fof(f424,plain,
v1_funct_2(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(backward_subsumption_resolution,[],[f415,f423]) ).
fof(f425,plain,
m2_relset_1(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(backward_subsumption_resolution,[],[f416,f423]) ).
fof(f429,definition,
( spl36_1
<=> v1_funct_1(sF35) ),
introduced(definition,[new_symbols(definition,[spl36_1])],[avatar_definition]) ).
fof(f430,plain,
( ~ v1_funct_1(sF35)
| spl36_1 ),
inference(avatar_component_clause,[],[f429]) ).
fof(f432,definition,
( spl36_2
<=> v1_funct_2(sF35,sF33,sK1) ),
introduced(definition,[new_symbols(definition,[spl36_2])],[avatar_definition]) ).
fof(f435,definition,
( spl36_3
<=> m2_relset_1(sF35,sF33,sK1) ),
introduced(definition,[new_symbols(definition,[spl36_3])],[avatar_definition]) ).
fof(f436,plain,
( ~ m2_relset_1(sF35,sF33,sK1)
| spl36_3 ),
inference(avatar_component_clause,[],[f435]) ).
fof(f438,definition,
( spl36_4
<=> v1_funct_1(sF32) ),
introduced(definition,[new_symbols(definition,[spl36_4])],[avatar_definition]) ).
fof(f439,plain,
( ~ v1_funct_1(sF32)
| spl36_4 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,definition,
( spl36_5
<=> v1_funct_2(sF32,sF33,sK1) ),
introduced(definition,[new_symbols(definition,[spl36_5])],[avatar_definition]) ).
fof(f442,plain,
( ~ v1_funct_2(sF32,sF33,sK1)
| spl36_5 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f444,definition,
( spl36_6
<=> m2_relset_1(sF32,sF33,sK1) ),
introduced(definition,[new_symbols(definition,[spl36_6])],[avatar_definition]) ).
fof(f445,plain,
( ~ m2_relset_1(sF32,sF33,sK1)
| spl36_6 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f446,plain,
( ~ spl36_1
| ~ spl36_2
| ~ spl36_3
| ~ spl36_4
| ~ spl36_5
| ~ spl36_6 ),
inference(avatar_split_clause,[],[f408,f444,f441,f438,f435,f432,f429]) ).
fof(f447,plain,
( v1_funct_1(sF32)
| ~ v1_relat_1(sF31)
| ~ v1_funct_1(sF31) ),
inference(superposition,[],[f319,f401]) ).
fof(f448,plain,
( v1_funct_1(sF35)
| ~ v1_relat_1(sF34)
| ~ v1_funct_1(sF34) ),
inference(superposition,[],[f319,f407]) ).
fof(f449,plain,
( ~ v1_relat_1(sF34)
| ~ v1_funct_1(sF34)
| spl36_1 ),
inference(forward_subsumption_resolution,[],[f448,f430]) ).
fof(f450,plain,
( v1_funct_1(sF34)
| ~ l2_lattices(sK0) ),
inference(superposition,[],[f302,f405]) ).
fof(f451,plain,
v1_funct_1(sF34),
inference(forward_subsumption_resolution,[],[f450,f420]) ).
fof(f452,plain,
( ~ v1_relat_1(sF34)
| spl36_1 ),
inference(backward_subsumption_resolution,[],[f449,f451]) ).
fof(f453,plain,
( sF32 = k7_relat_1(sF31,sF33)
| ~ v1_relat_1(sF31) ),
inference(superposition,[],[f419,f401]) ).
fof(f454,plain,
( sF35 = k7_relat_1(sF34,sF33)
| ~ v1_relat_1(sF34) ),
inference(superposition,[],[f419,f407]) ).
fof(f464,plain,
! [X2,X0,X1] :
( k1_funct_1(X0,sK6(k7_relat_1(X0,X1),X2)) = X2
| ~ v1_relat_1(k7_relat_1(X0,X1))
| ~ v1_funct_1(k7_relat_1(X0,X1))
| ~ r2_hidden(X2,k2_relat_1(k7_relat_1(X0,X1)))
| ~ v1_relat_1(X0)
| ~ r2_hidden(sK6(k7_relat_1(X0,X1),X2),k1_relat_1(k7_relat_1(X0,X1)))
| ~ v1_funct_1(X0) ),
inference(superposition,[],[f397,f379]) ).
fof(f466,plain,
! [X2,X0,X1] :
( k1_funct_1(X0,sK6(k7_relat_1(X0,X1),X2)) = X2
| ~ v1_relat_1(k7_relat_1(X0,X1))
| ~ v1_funct_1(k7_relat_1(X0,X1))
| ~ r2_hidden(X2,k2_relat_1(k7_relat_1(X0,X1)))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(forward_subsumption_resolution,[],[f464,f396]) ).
fof(f468,plain,
! [X2,X0,X1] :
( k1_funct_1(X0,sK6(k7_relat_1(X0,X1),X2)) = X2
| ~ v1_funct_1(k7_relat_1(X0,X1))
| ~ r2_hidden(X2,k2_relat_1(k7_relat_1(X0,X1)))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(forward_subsumption_resolution,[],[f466,f289]) ).
fof(f470,plain,
! [X2,X0,X1] :
( k1_funct_1(X0,sK6(k7_relat_1(X0,X1),X2)) = X2
| ~ r2_hidden(X2,k2_relat_1(k7_relat_1(X0,X1)))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(forward_subsumption_resolution,[],[f468,f328]) ).
fof(f484,plain,
( v1_funct_1(sF31)
| ~ l1_lattices(sK0) ),
inference(superposition,[],[f299,f399]) ).
fof(f485,plain,
v1_funct_1(sF31),
inference(forward_subsumption_resolution,[],[f484,f423]) ).
fof(f487,plain,
( v1_funct_1(sF32)
| ~ v1_relat_1(sF31) ),
inference(backward_subsumption_resolution,[],[f447,f485]) ).
fof(f498,plain,
! [X2,X0,X1] :
( k2_tarski(k1_tarski(sK29(X0,X1,X2)),k2_tarski(sK29(X0,X1,X2),sK30(X0,X1,X2))) = X0
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) ),
inference(superposition,[],[f388,f251]) ).
fof(f499,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f296,f249]) ).
fof(f505,plain,
! [X2,X0,X1] :
( k1_binop_1(X2,X0,X1) = k1_funct_1(X2,k2_tarski(k1_tarski(X0),k2_tarski(X0,X1)))
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) ),
inference(superposition,[],[f386,f251]) ).
fof(f515,plain,
( v1_relat_1(sF32)
| ~ v1_relat_1(sF31)
| ~ v1_funct_1(sF31) ),
inference(superposition,[],[f320,f401]) ).
fof(f519,plain,
( v1_relat_1(sF32)
| ~ v1_relat_1(sF31) ),
inference(forward_subsumption_resolution,[],[f515,f485]) ).
fof(f520,plain,
l1_struct_0(sK0),
inference(resolution,[],[f291,f420]) ).
fof(f528,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v4_lattices(sK0) ),
inference(resolution,[],[f247,f237]) ).
fof(f529,plain,
( v3_struct_0(sK0)
| v4_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f528,f238]) ).
fof(f530,plain,
v4_lattices(sK0),
inference(forward_subsumption_resolution,[],[f529,f239]) ).
fof(f532,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v6_lattices(sK0) ),
inference(resolution,[],[f245,f237]) ).
fof(f533,plain,
( v3_struct_0(sK0)
| v6_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f532,f238]) ).
fof(f534,plain,
v6_lattices(sK0),
inference(forward_subsumption_resolution,[],[f533,f239]) ).
fof(f541,plain,
! [X2,X0,X1] :
( m1_subset_1(X0,u1_struct_0(X2))
| ~ r2_hidden(X0,X1)
| ~ v10_lattices(X2)
| v3_struct_0(X2)
| ~ m2_lattice4(X1,X2)
| ~ l3_lattices(X2) ),
inference(resolution,[],[f376,f295]) ).
fof(f545,plain,
( v1_relat_1(sF35)
| ~ v1_relat_1(sF34) ),
inference(superposition,[],[f312,f407]) ).
fof(f555,plain,
m1_relset_1(sF34,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(resolution,[],[f422,f369]) ).
fof(f556,plain,
v1_relat_1(sF34),
inference(resolution,[],[f422,f499]) ).
fof(f558,plain,
( $false
| spl36_1 ),
inference(forward_subsumption_resolution,[],[f556,f452]) ).
fof(f559,plain,
spl36_1,
inference(avatar_contradiction_clause,[],[f558]) ).
fof(f560,plain,
( v1_funct_1(sF35)
| ~ v1_relat_1(sF34) ),
inference(forward_subsumption_resolution,[],[f448,f451]) ).
fof(f563,plain,
v1_relat_1(sF35),
inference(backward_subsumption_resolution,[],[f545,f556]) ).
fof(f564,plain,
sF35 = k7_relat_1(sF34,sF33),
inference(backward_subsumption_resolution,[],[f454,f556]) ).
fof(f565,plain,
v1_funct_1(sF35),
inference(forward_subsumption_resolution,[],[f560,f556]) ).
fof(f579,plain,
( sF33 = k1_relat_1(sF35)
| ~ r1_tarski(sF33,k1_relat_1(sF34))
| ~ v1_relat_1(sF34) ),
inference(superposition,[],[f382,f564]) ).
fof(f580,plain,
( sF33 = k1_relat_1(sF35)
| ~ r1_tarski(sF33,k1_relat_1(sF34)) ),
inference(forward_subsumption_resolution,[],[f579,f556]) ).
fof(f581,plain,
m1_relset_1(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(resolution,[],[f425,f369]) ).
fof(f582,plain,
v1_relat_1(sF31),
inference(resolution,[],[f425,f499]) ).
fof(f583,plain,
v1_relat_1(sF32),
inference(backward_subsumption_resolution,[],[f519,f582]) ).
fof(f584,plain,
v1_funct_1(sF32),
inference(backward_subsumption_resolution,[],[f487,f582]) ).
fof(f586,plain,
sF32 = k7_relat_1(sF31,sF33),
inference(backward_subsumption_resolution,[],[f453,f582]) ).
fof(f598,plain,
( sF33 = k1_relat_1(sF32)
| ~ r1_tarski(sF33,k1_relat_1(sF31))
| ~ v1_relat_1(sF31) ),
inference(superposition,[],[f382,f586]) ).
fof(f599,plain,
( sF33 = k1_relat_1(sF32)
| ~ r1_tarski(sF33,k1_relat_1(sF31)) ),
inference(forward_subsumption_resolution,[],[f598,f582]) ).
fof(f607,definition,
( spl36_7
<=> r1_tarski(sF33,k1_relat_1(sF34)) ),
introduced(definition,[new_symbols(definition,[spl36_7])],[avatar_definition]) ).
fof(f608,plain,
( ~ r1_tarski(sF33,k1_relat_1(sF34))
| spl36_7 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f610,definition,
( spl36_8
<=> sF33 = k1_relat_1(sF35) ),
introduced(definition,[new_symbols(definition,[spl36_8])],[avatar_definition]) ).
fof(f611,plain,
( sF33 = k1_relat_1(sF35)
| ~ spl36_8 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f612,plain,
( ~ spl36_7
| spl36_8 ),
inference(avatar_split_clause,[],[f580,f610,f607]) ).
fof(f614,definition,
( spl36_9
<=> r1_tarski(sF33,k1_relat_1(sF31)) ),
introduced(definition,[new_symbols(definition,[spl36_9])],[avatar_definition]) ).
fof(f615,plain,
( ~ r1_tarski(sF33,k1_relat_1(sF31))
| spl36_9 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f617,definition,
( spl36_10
<=> sF33 = k1_relat_1(sF32) ),
introduced(definition,[new_symbols(definition,[spl36_10])],[avatar_definition]) ).
fof(f618,plain,
( sF33 = k1_relat_1(sF32)
| ~ spl36_10 ),
inference(avatar_component_clause,[],[f617]) ).
fof(f619,plain,
( ~ spl36_9
| spl36_10 ),
inference(avatar_split_clause,[],[f599,f617,f614]) ).
fof(f627,plain,
! [X2,X0,X1] :
( v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ r2_hidden(X2,k2_zfmisc_1(X1,X0))
| r2_hidden(sK30(X2,X1,X0),X0)
| v1_xboole_0(X0) ),
inference(resolution,[],[f383,f373]) ).
fof(f628,plain,
! [X2,X0,X1] :
( r2_hidden(sK30(X2,X1,X0),X0)
| v1_xboole_0(X1)
| ~ r2_hidden(X2,k2_zfmisc_1(X1,X0))
| v1_xboole_0(X0) ),
inference(duplicate_literal_removal,[],[f627]) ).
fof(f637,plain,
! [X2,X0,X1] :
( v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ r2_hidden(X2,k2_zfmisc_1(X1,X0))
| r2_hidden(sK29(X2,X1,X0),X1)
| v1_xboole_0(X1) ),
inference(resolution,[],[f385,f373]) ).
fof(f638,plain,
! [X2,X0,X1] :
( r2_hidden(sK29(X2,X1,X0),X1)
| v1_xboole_0(X1)
| ~ r2_hidden(X2,k2_zfmisc_1(X1,X0))
| v1_xboole_0(X0) ),
inference(duplicate_literal_removal,[],[f637]) ).
fof(f649,plain,
! [X0,X1] :
( m2_relset_1(X0,k1_relat_1(X0),X1)
| ~ v1_relat_1(X0)
| ~ r1_tarski(k2_relat_1(X0),X1) ),
inference(resolution,[],[f371,f370]) ).
fof(f739,plain,
! [X0,X1] :
( k1_lattices(sK0,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sF34,X0,X1)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(superposition,[],[f268,f405]) ).
fof(f740,plain,
! [X0,X1] :
( k1_lattices(sK0,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sF34,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f739,f239]) ).
fof(f741,plain,
! [X0,X1] :
( k1_lattices(sK0,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sF34,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f740,f420]) ).
fof(f803,plain,
! [X2,X0,X1] :
( k1_relat_1(X2) = X0
| ~ m1_relset_1(X2,X0,X1)
| k1_xboole_0 = X1
| ~ m2_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1) ),
inference(superposition,[],[f365,f265]) ).
fof(f804,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| k1_xboole_0 = X1
| k1_relat_1(X2) = X0
| ~ v1_funct_2(X2,X0,X1) ),
inference(forward_subsumption_resolution,[],[f803,f369]) ).
fof(f807,plain,
! [X0] :
( u1_struct_0(X0) = k1_xboole_0
| k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)) = k1_relat_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(resolution,[],[f804,f300]) ).
fof(f810,plain,
( k1_xboole_0 = u1_struct_0(sK0)
| k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)) = k1_relat_1(sF31)
| ~ v1_funct_2(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(resolution,[],[f804,f425]) ).
fof(f811,plain,
( k1_xboole_0 = u1_struct_0(sK0)
| k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)) = k1_relat_1(sF31) ),
inference(forward_subsumption_resolution,[],[f810,f424]) ).
fof(f814,plain,
! [X0] :
( k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)) = k1_relat_1(u2_lattices(X0))
| u1_struct_0(X0) = k1_xboole_0
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f807,f301]) ).
fof(f902,plain,
! [X0,X1] :
( k2_lattices(sK0,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sF31,X0,X1)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ l1_lattices(sK0) ),
inference(superposition,[],[f269,f399]) ).
fof(f903,plain,
! [X0,X1] :
( k2_lattices(sK0,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sF31,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ l1_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f902,f239]) ).
fof(f904,plain,
! [X0,X1] :
( k2_lattices(sK0,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sF31,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f903,f423]) ).
fof(f918,plain,
! [X0] :
( k1_funct_1(sF34,sK6(sF35,X0)) = X0
| ~ r2_hidden(X0,k2_relat_1(sF35))
| ~ v1_relat_1(sF34)
| ~ v1_funct_1(sF34) ),
inference(superposition,[],[f470,f564]) ).
fof(f919,plain,
! [X0] :
( k1_funct_1(sF31,sK6(sF32,X0)) = X0
| ~ r2_hidden(X0,k2_relat_1(sF32))
| ~ v1_relat_1(sF31)
| ~ v1_funct_1(sF31) ),
inference(superposition,[],[f470,f586]) ).
fof(f951,plain,
! [X0] :
( k1_funct_1(sF31,sK6(sF32,X0)) = X0
| ~ r2_hidden(X0,k2_relat_1(sF32))
| ~ v1_funct_1(sF31) ),
inference(forward_subsumption_resolution,[],[f919,f582]) ).
fof(f952,plain,
! [X0] :
( k1_funct_1(sF34,sK6(sF35,X0)) = X0
| ~ r2_hidden(X0,k2_relat_1(sF35))
| ~ v1_funct_1(sF34) ),
inference(forward_subsumption_resolution,[],[f918,f556]) ).
fof(f966,plain,
! [X0] :
( k1_funct_1(sF31,sK6(sF32,X0)) = X0
| ~ r2_hidden(X0,k2_relat_1(sF32)) ),
inference(forward_subsumption_resolution,[],[f951,f485]) ).
fof(f967,plain,
! [X0] :
( k1_funct_1(sF34,sK6(sF35,X0)) = X0
| ~ r2_hidden(X0,k2_relat_1(sF35)) ),
inference(forward_subsumption_resolution,[],[f952,f451]) ).
fof(f1034,plain,
! [X2,X0,X1] :
( k1_relat_1(X0) != X1
| k1_xboole_0 = X2
| ~ m2_relset_1(X0,X1,X2)
| v1_funct_2(X0,X1,X2)
| ~ m1_relset_1(X0,X1,X2) ),
inference(superposition,[],[f264,f365]) ).
fof(f1036,plain,
! [X2,X0,X1] :
( k1_relat_1(X0) != X1
| k1_xboole_0 = X2
| v1_funct_2(X0,X1,X2)
| ~ m1_relset_1(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1034,f368]) ).
fof(f1039,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,k1_relat_1(X1),X0)
| v1_funct_2(X1,k1_relat_1(X1),X0)
| k1_xboole_0 = X0 ),
inference(equality_resolution,[],[f1036]) ).
fof(f1106,definition,
( spl36_11
<=> k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)) = k1_relat_1(sF31) ),
introduced(definition,[new_symbols(definition,[spl36_11])],[avatar_definition]) ).
fof(f1107,plain,
( k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)) = k1_relat_1(sF31)
| ~ spl36_11 ),
inference(avatar_component_clause,[],[f1106]) ).
fof(f1109,definition,
( spl36_12
<=> k1_xboole_0 = u1_struct_0(sK0) ),
introduced(definition,[new_symbols(definition,[spl36_12])],[avatar_definition]) ).
fof(f1110,plain,
( k1_xboole_0 = u1_struct_0(sK0)
| ~ spl36_12 ),
inference(avatar_component_clause,[],[f1109]) ).
fof(f1111,plain,
( spl36_11
| spl36_12 ),
inference(avatar_split_clause,[],[f811,f1109,f1106]) ).
fof(f1121,plain,
( k1_relat_1(sF31) = k1_relat_1(u2_lattices(sK0))
| k1_xboole_0 = u1_struct_0(sK0)
| ~ l2_lattices(sK0)
| ~ spl36_11 ),
inference(superposition,[],[f814,f1107]) ).
fof(f1135,plain,
( k1_relat_1(sF31) = k1_relat_1(u2_lattices(sK0))
| k1_xboole_0 = u1_struct_0(sK0)
| ~ spl36_11 ),
inference(forward_subsumption_resolution,[],[f1121,f420]) ).
fof(f1139,plain,
( k1_relat_1(sF31) = k1_relat_1(sF34)
| k1_xboole_0 = u1_struct_0(sK0)
| ~ spl36_11 ),
inference(forward_demodulation,[],[f1135,f405]) ).
fof(f1142,definition,
( spl36_13
<=> k1_relat_1(sF31) = k1_relat_1(sF34) ),
introduced(definition,[new_symbols(definition,[spl36_13])],[avatar_definition]) ).
fof(f1143,plain,
( k1_relat_1(sF31) = k1_relat_1(sF34)
| ~ spl36_13 ),
inference(avatar_component_clause,[],[f1142]) ).
fof(f1144,plain,
( spl36_12
| spl36_13
| ~ spl36_11 ),
inference(avatar_split_clause,[],[f1139,f1106,f1142,f1109]) ).
fof(f1159,plain,
( ~ v1_xboole_0(k1_xboole_0)
| v3_struct_0(sK0)
| ~ l1_struct_0(sK0)
| ~ spl36_12 ),
inference(superposition,[],[f313,f1110]) ).
fof(f1168,plain,
( v3_struct_0(sK0)
| ~ l1_struct_0(sK0)
| ~ spl36_12 ),
inference(forward_subsumption_resolution,[],[f1159,f315]) ).
fof(f1185,plain,
( ~ l1_struct_0(sK0)
| ~ spl36_12 ),
inference(forward_subsumption_resolution,[],[f1168,f239]) ).
fof(f1194,plain,
( $false
| ~ spl36_12 ),
inference(forward_subsumption_resolution,[],[f1185,f520]) ).
fof(f1195,plain,
~ spl36_12,
inference(avatar_contradiction_clause,[],[f1194]) ).
fof(f1200,plain,
( ~ r1_tarski(sF33,k1_relat_1(sF31))
| spl36_7
| ~ spl36_13 ),
inference(superposition,[],[f608,f1143]) ).
fof(f1597,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k2_zfmisc_1(X0,X1),k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X3))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X3)) ),
inference(superposition,[],[f281,f360]) ).
fof(f1603,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k2_zfmisc_1(X0,X1),k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X3)) ),
inference(duplicate_literal_removal,[],[f1597]) ).
fof(f1618,plain,
! [X0,X1] :
( m1_subset_1(sF33,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(X0))
| ~ m1_subset_1(sK1,k1_zfmisc_1(X1)) ),
inference(superposition,[],[f1603,f403]) ).
fof(f1753,definition,
( spl36_29
<=> v1_xboole_0(u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl36_29])],[avatar_definition]) ).
fof(f1754,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ spl36_29 ),
inference(avatar_component_clause,[],[f1753]) ).
fof(f1760,plain,
( v3_struct_0(sK0)
| ~ l1_struct_0(sK0)
| ~ spl36_29 ),
inference(resolution,[],[f1754,f313]) ).
fof(f1763,plain,
( ~ l1_struct_0(sK0)
| ~ spl36_29 ),
inference(forward_subsumption_resolution,[],[f1760,f239]) ).
fof(f1764,plain,
( $false
| ~ spl36_29 ),
inference(forward_subsumption_resolution,[],[f1763,f520]) ).
fof(f1765,plain,
~ spl36_29,
inference(avatar_contradiction_clause,[],[f1764]) ).
fof(f1832,plain,
! [X2,X3,X0,X1] :
( k1_funct_1(X1,X0) = k1_binop_1(X1,sK29(X0,X2,X3),sK30(X0,X2,X3))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1)
| v1_xboole_0(X3)
| v1_xboole_0(X2)
| ~ r2_hidden(X0,k2_zfmisc_1(X2,X3)) ),
inference(superposition,[],[f505,f498]) ).
fof(f1959,plain,
! [X0,X1] :
( k1_binop_1(sF31,X0,X1) = k2_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_relset_1(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(sF31)
| v1_xboole_0(u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ),
inference(superposition,[],[f904,f362]) ).
fof(f1960,plain,
! [X0,X1] :
( k1_binop_1(sF34,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_relset_1(sF34,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(sF34,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(sF34)
| v1_xboole_0(u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ),
inference(superposition,[],[f741,f362]) ).
fof(f1963,plain,
! [X0,X1] :
( k1_binop_1(sF34,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_relset_1(sF34,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(sF34,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(sF34)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(duplicate_literal_removal,[],[f1960]) ).
fof(f1964,plain,
! [X0,X1] :
( k1_binop_1(sF31,X0,X1) = k2_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_relset_1(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(sF31)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(duplicate_literal_removal,[],[f1959]) ).
fof(f1971,plain,
! [X0,X1] :
( k1_binop_1(sF34,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ v1_funct_2(sF34,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(sF34)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1963,f555]) ).
fof(f1972,plain,
! [X0,X1] :
( k1_binop_1(sF31,X0,X1) = k2_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ v1_funct_2(sF31,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(sF31)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1964,f581]) ).
fof(f1979,plain,
! [X0,X1] :
( k1_binop_1(sF34,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ v1_funct_1(sF34)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1971,f421]) ).
fof(f1980,plain,
! [X0,X1] :
( k1_binop_1(sF31,X0,X1) = k2_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ v1_funct_1(sF31)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1972,f424]) ).
fof(f1987,plain,
! [X0,X1] :
( k1_binop_1(sF34,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1979,f451]) ).
fof(f1988,plain,
! [X0,X1] :
( k1_binop_1(sF31,X0,X1) = k2_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1980,f485]) ).
fof(f2113,plain,
( m1_subset_1(sF33,k1_zfmisc_1(k1_relat_1(sF31)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ spl36_11 ),
inference(superposition,[],[f1618,f1107]) ).
fof(f2114,plain,
( m1_subset_1(sF33,k1_zfmisc_1(k1_relat_1(sF31)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ spl36_11 ),
inference(duplicate_literal_removal,[],[f2113]) ).
fof(f2603,definition,
( spl36_37
<=> m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0))) ),
introduced(definition,[new_symbols(definition,[spl36_37])],[avatar_definition]) ).
fof(f2604,plain,
( ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0)))
| spl36_37 ),
inference(avatar_component_clause,[],[f2603]) ).
fof(f2606,definition,
( spl36_38
<=> m1_subset_1(sF33,k1_zfmisc_1(k1_relat_1(sF31))) ),
introduced(definition,[new_symbols(definition,[spl36_38])],[avatar_definition]) ).
fof(f2607,plain,
( m1_subset_1(sF33,k1_zfmisc_1(k1_relat_1(sF31)))
| ~ spl36_38 ),
inference(avatar_component_clause,[],[f2606]) ).
fof(f2608,plain,
( ~ spl36_37
| spl36_38
| ~ spl36_11 ),
inference(avatar_split_clause,[],[f2114,f1106,f2606,f2603]) ).
fof(f2610,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_lattice4(sK1,sK0)
| ~ l3_lattices(sK0)
| spl36_37 ),
inference(resolution,[],[f2604,f295]) ).
fof(f2613,plain,
( v3_struct_0(sK0)
| ~ m2_lattice4(sK1,sK0)
| ~ l3_lattices(sK0)
| spl36_37 ),
inference(forward_subsumption_resolution,[],[f2610,f238]) ).
fof(f2614,plain,
( ~ m2_lattice4(sK1,sK0)
| ~ l3_lattices(sK0)
| spl36_37 ),
inference(forward_subsumption_resolution,[],[f2613,f239]) ).
fof(f2615,plain,
( ~ l3_lattices(sK0)
| spl36_37 ),
inference(forward_subsumption_resolution,[],[f2614,f235]) ).
fof(f2616,plain,
( $false
| spl36_37 ),
inference(forward_subsumption_resolution,[],[f2615,f237]) ).
fof(f2617,plain,
spl36_37,
inference(avatar_contradiction_clause,[],[f2616]) ).
fof(f2622,plain,
( r1_tarski(sF33,k1_relat_1(sF31))
| ~ spl36_38 ),
inference(resolution,[],[f2607,f375]) ).
fof(f2626,plain,
( $false
| spl36_9
| ~ spl36_38 ),
inference(forward_subsumption_resolution,[],[f2622,f615]) ).
fof(f2627,plain,
( spl36_9
| ~ spl36_38 ),
inference(avatar_contradiction_clause,[],[f2626]) ).
fof(f2628,plain,
( $false
| spl36_7
| ~ spl36_13
| ~ spl36_38 ),
inference(forward_subsumption_resolution,[],[f2622,f1200]) ).
fof(f2629,plain,
( spl36_7
| ~ spl36_13
| ~ spl36_38 ),
inference(avatar_contradiction_clause,[],[f2628]) ).
fof(f2641,plain,
( ! [X0] :
( r2_hidden(sK6(sF35,X0),sF33)
| ~ v1_relat_1(sF35)
| ~ v1_funct_1(sF35)
| ~ r2_hidden(X0,k2_relat_1(sF35)) )
| ~ spl36_8 ),
inference(superposition,[],[f396,f611]) ).
fof(f2645,plain,
( ! [X0] :
( ~ m1_relset_1(sF35,sF33,X0)
| v1_funct_2(sF35,sF33,X0)
| k1_xboole_0 = X0 )
| ~ spl36_8 ),
inference(superposition,[],[f1039,f611]) ).
fof(f2650,plain,
( ! [X0] :
( r2_hidden(sK6(sF35,X0),sF33)
| ~ v1_funct_1(sF35)
| ~ r2_hidden(X0,k2_relat_1(sF35)) )
| ~ spl36_8 ),
inference(forward_subsumption_resolution,[],[f2641,f563]) ).
fof(f2654,plain,
( ! [X0] :
( r2_hidden(sK6(sF35,X0),sF33)
| ~ r2_hidden(X0,k2_relat_1(sF35)) )
| ~ spl36_8 ),
inference(forward_subsumption_resolution,[],[f2650,f565]) ).
fof(f2661,plain,
( ! [X0] :
( r2_hidden(sK6(sF32,X0),sF33)
| ~ v1_relat_1(sF32)
| ~ v1_funct_1(sF32)
| ~ r2_hidden(X0,k2_relat_1(sF32)) )
| ~ spl36_10 ),
inference(superposition,[],[f396,f618]) ).
fof(f2665,plain,
( ! [X0] :
( ~ m1_relset_1(sF32,sF33,X0)
| v1_funct_2(sF32,sF33,X0)
| k1_xboole_0 = X0 )
| ~ spl36_10 ),
inference(superposition,[],[f1039,f618]) ).
fof(f2670,plain,
( ! [X0] :
( r2_hidden(sK6(sF32,X0),sF33)
| ~ v1_funct_1(sF32)
| ~ r2_hidden(X0,k2_relat_1(sF32)) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f2661,f583]) ).
fof(f2674,plain,
( ! [X0] :
( r2_hidden(sK6(sF32,X0),sF33)
| ~ r2_hidden(X0,k2_relat_1(sF32)) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f2670,f584]) ).
fof(f3599,plain,
( ! [X0] :
( m2_relset_1(sF32,sF33,X0)
| ~ v1_relat_1(sF32)
| ~ r1_tarski(k2_relat_1(sF32),X0) )
| ~ spl36_10 ),
inference(superposition,[],[f649,f618]) ).
fof(f3601,plain,
( ! [X0] :
( m2_relset_1(sF35,sF33,X0)
| ~ v1_relat_1(sF35)
| ~ r1_tarski(k2_relat_1(sF35),X0) )
| ~ spl36_8 ),
inference(superposition,[],[f649,f611]) ).
fof(f3602,plain,
( ! [X0] :
( ~ r1_tarski(k2_relat_1(sF35),X0)
| m2_relset_1(sF35,sF33,X0) )
| ~ spl36_8 ),
inference(forward_subsumption_resolution,[],[f3601,f563]) ).
fof(f3603,plain,
( ! [X0] :
( ~ r1_tarski(k2_relat_1(sF32),X0)
| m2_relset_1(sF32,sF33,X0) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f3599,f583]) ).
fof(f4341,definition,
( spl36_45
<=> ! [X0,X1] :
( k1_binop_1(sF34,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl36_45])],[avatar_definition]) ).
fof(f4342,plain,
( ! [X0,X1] :
( k1_binop_1(sF34,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl36_45 ),
inference(avatar_component_clause,[],[f4341]) ).
fof(f4343,plain,
( spl36_29
| spl36_45 ),
inference(avatar_split_clause,[],[f1987,f4341,f1753]) ).
fof(f4345,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF34,X0) = k1_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ v1_relat_1(sF34)
| ~ v1_funct_1(sF34)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0)) )
| ~ spl36_45 ),
inference(superposition,[],[f1832,f4342]) ).
fof(f4346,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF34,X0) = k1_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ v1_funct_1(sF34)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4345,f556]) ).
fof(f4348,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF34,X0) = k1_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4346,f451]) ).
fof(f4355,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF34,X0) = k3_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| ~ v4_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0)) )
| ~ spl36_45 ),
inference(superposition,[],[f363,f4348]) ).
fof(f4356,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF34,X0) = k3_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| ~ v4_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_45 ),
inference(duplicate_literal_removal,[],[f4355]) ).
fof(f4362,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF34,X0) = k3_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| ~ v4_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4356,f420]) ).
fof(f4366,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF34,X0) = k3_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4362,f530]) ).
fof(f4370,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF34,X0) = k3_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4366,f239]) ).
fof(f4374,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k1_funct_1(sF34,X0),X3)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r2_hidden(sK30(X0,X1,X2),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ l3_lattices(sK0)
| ~ m2_lattice4(X3,sK0)
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_45 ),
inference(superposition,[],[f413,f4370]) ).
fof(f4376,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k1_funct_1(sF34,X0),X3)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r2_hidden(sK30(X0,X1,X2),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ l3_lattices(sK0)
| ~ m2_lattice4(X3,sK0)
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4374,f541]) ).
fof(f4378,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k1_funct_1(sF34,X0),X3)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r2_hidden(sK30(X0,X1,X2),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ l3_lattices(sK0)
| ~ m2_lattice4(X3,sK0)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4376,f541]) ).
fof(f4380,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k1_funct_1(sF34,X0),X3)
| v3_struct_0(sK0)
| ~ r2_hidden(sK30(X0,X1,X2),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ l3_lattices(sK0)
| ~ m2_lattice4(X3,sK0)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4378,f238]) ).
fof(f4382,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k1_funct_1(sF34,X0),X3)
| ~ r2_hidden(sK30(X0,X1,X2),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ l3_lattices(sK0)
| ~ m2_lattice4(X3,sK0)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4380,f239]) ).
fof(f4384,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(sK30(X0,X1,X2),X3)
| r2_hidden(k1_funct_1(sF34,X0),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ m2_lattice4(X3,sK0)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4382,f237]) ).
fof(f4386,plain,
( ! [X2,X0,X1] :
( r2_hidden(k1_funct_1(sF34,X0),X1)
| ~ r2_hidden(sK29(X0,X2,X1),X1)
| ~ m2_lattice4(X1,sK0)
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| ~ r2_hidden(X0,k2_zfmisc_1(X2,X1))
| v1_xboole_0(X2)
| ~ r2_hidden(X0,k2_zfmisc_1(X2,X1))
| v1_xboole_0(X1) )
| ~ spl36_45 ),
inference(resolution,[],[f4384,f628]) ).
fof(f4391,plain,
( ! [X2,X0,X1] :
( r2_hidden(k1_funct_1(sF34,X0),X1)
| ~ r2_hidden(sK29(X0,X2,X1),X1)
| ~ m2_lattice4(X1,sK0)
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| ~ r2_hidden(X0,k2_zfmisc_1(X2,X1)) )
| ~ spl36_45 ),
inference(duplicate_literal_removal,[],[f4386]) ).
fof(f4392,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(sK29(X0,X2,X1),X1)
| r2_hidden(k1_funct_1(sF34,X0),X1)
| ~ m2_lattice4(X1,sK0)
| v1_xboole_0(X2)
| ~ r2_hidden(X0,k2_zfmisc_1(X2,X1)) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f4391,f380]) ).
fof(f4400,plain,
( ! [X0,X1] :
( r2_hidden(k1_funct_1(sF34,X0),X1)
| ~ m2_lattice4(X1,sK0)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X1))
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X1))
| v1_xboole_0(X1) )
| ~ spl36_45 ),
inference(resolution,[],[f4392,f638]) ).
fof(f4405,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k2_zfmisc_1(X1,X1))
| ~ m2_lattice4(X1,sK0)
| v1_xboole_0(X1)
| r2_hidden(k1_funct_1(sF34,X0),X1) )
| ~ spl36_45 ),
inference(duplicate_literal_removal,[],[f4400]) ).
fof(f4767,definition,
( spl36_48
<=> ! [X0,X1] :
( k1_binop_1(sF31,X0,X1) = k2_lattices(sK0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl36_48])],[avatar_definition]) ).
fof(f4768,plain,
( ! [X0,X1] :
( k1_binop_1(sF31,X0,X1) = k2_lattices(sK0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl36_48 ),
inference(avatar_component_clause,[],[f4767]) ).
fof(f4769,plain,
( spl36_29
| spl36_48 ),
inference(avatar_split_clause,[],[f1988,f4767,f1753]) ).
fof(f4771,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF31,X0) = k2_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ v1_relat_1(sF31)
| ~ v1_funct_1(sF31)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0)) )
| ~ spl36_48 ),
inference(superposition,[],[f1832,f4768]) ).
fof(f4772,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF31,X0) = k2_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ v1_funct_1(sF31)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4771,f582]) ).
fof(f4774,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF31,X0) = k2_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4772,f485]) ).
fof(f4781,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF31,X0) = k4_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| ~ l1_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0)) )
| ~ spl36_48 ),
inference(superposition,[],[f364,f4774]) ).
fof(f4782,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF31,X0) = k4_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| ~ l1_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_48 ),
inference(duplicate_literal_removal,[],[f4781]) ).
fof(f4788,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF31,X0) = k4_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| ~ v6_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4782,f423]) ).
fof(f4793,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF31,X0) = k4_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4788,f534]) ).
fof(f4797,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF31,X0) = k4_lattices(sK0,sK29(X0,X1,X2),sK30(X0,X1,X2))
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4793,f239]) ).
fof(f4807,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k1_funct_1(sF31,X0),X3)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r2_hidden(sK30(X0,X1,X2),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ l3_lattices(sK0)
| ~ m2_lattice4(X3,sK0)
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_48 ),
inference(superposition,[],[f414,f4797]) ).
fof(f4809,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k1_funct_1(sF31,X0),X3)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r2_hidden(sK30(X0,X1,X2),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ l3_lattices(sK0)
| ~ m2_lattice4(X3,sK0)
| ~ m1_subset_1(sK29(X0,X1,X2),u1_struct_0(sK0))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4807,f541]) ).
fof(f4811,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k1_funct_1(sF31,X0),X3)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r2_hidden(sK30(X0,X1,X2),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ l3_lattices(sK0)
| ~ m2_lattice4(X3,sK0)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4809,f541]) ).
fof(f4813,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k1_funct_1(sF31,X0),X3)
| v3_struct_0(sK0)
| ~ r2_hidden(sK30(X0,X1,X2),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ l3_lattices(sK0)
| ~ m2_lattice4(X3,sK0)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4811,f238]) ).
fof(f4815,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(k1_funct_1(sF31,X0),X3)
| ~ r2_hidden(sK30(X0,X1,X2),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ l3_lattices(sK0)
| ~ m2_lattice4(X3,sK0)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4813,f239]) ).
fof(f4817,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(sK30(X0,X1,X2),X3)
| r2_hidden(k1_funct_1(sF31,X0),X3)
| ~ r2_hidden(sK29(X0,X1,X2),X3)
| ~ m2_lattice4(X3,sK0)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X2)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4815,f237]) ).
fof(f4819,plain,
( ! [X2,X0,X1] :
( r2_hidden(k1_funct_1(sF31,X0),X1)
| ~ r2_hidden(sK29(X0,X2,X1),X1)
| ~ m2_lattice4(X1,sK0)
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| ~ r2_hidden(X0,k2_zfmisc_1(X2,X1))
| v1_xboole_0(X2)
| ~ r2_hidden(X0,k2_zfmisc_1(X2,X1))
| v1_xboole_0(X1) )
| ~ spl36_48 ),
inference(resolution,[],[f4817,f628]) ).
fof(f4825,plain,
( ! [X2,X0,X1] :
( r2_hidden(k1_funct_1(sF31,X0),X1)
| ~ r2_hidden(sK29(X0,X2,X1),X1)
| ~ m2_lattice4(X1,sK0)
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| ~ r2_hidden(X0,k2_zfmisc_1(X2,X1)) )
| ~ spl36_48 ),
inference(duplicate_literal_removal,[],[f4819]) ).
fof(f4826,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(sK29(X0,X2,X1),X1)
| r2_hidden(k1_funct_1(sF31,X0),X1)
| ~ m2_lattice4(X1,sK0)
| v1_xboole_0(X2)
| ~ r2_hidden(X0,k2_zfmisc_1(X2,X1)) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f4825,f380]) ).
fof(f4835,plain,
( ! [X0,X1] :
( r2_hidden(k1_funct_1(sF31,X0),X1)
| ~ m2_lattice4(X1,sK0)
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X1))
| v1_xboole_0(X1)
| ~ r2_hidden(X0,k2_zfmisc_1(X1,X1))
| v1_xboole_0(X1) )
| ~ spl36_48 ),
inference(resolution,[],[f4826,f638]) ).
fof(f4841,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k2_zfmisc_1(X1,X1))
| ~ m2_lattice4(X1,sK0)
| v1_xboole_0(X1)
| r2_hidden(k1_funct_1(sF31,X0),X1) )
| ~ spl36_48 ),
inference(duplicate_literal_removal,[],[f4835]) ).
fof(f5694,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF33)
| ~ m2_lattice4(sK1,sK0)
| v1_xboole_0(sK1)
| r2_hidden(k1_funct_1(sF34,X0),sK1) )
| ~ spl36_45 ),
inference(superposition,[],[f4405,f403]) ).
fof(f5702,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF33)
| v1_xboole_0(sK1)
| r2_hidden(k1_funct_1(sF34,X0),sK1) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f5694,f235]) ).
fof(f5703,plain,
( ! [X0] :
( r2_hidden(k1_funct_1(sF34,X0),sK1)
| ~ r2_hidden(X0,sF33) )
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f5702,f236]) ).
fof(f5708,plain,
( ! [X0] :
( r2_hidden(X0,sK1)
| ~ r2_hidden(sK6(sF35,X0),sF33)
| ~ r2_hidden(X0,k2_relat_1(sF35)) )
| ~ spl36_45 ),
inference(superposition,[],[f5703,f967]) ).
fof(f5725,plain,
( ! [X0] :
( ~ r2_hidden(X0,k2_relat_1(sF35))
| r2_hidden(X0,sK1) )
| ~ spl36_8
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f5708,f2654]) ).
fof(f5744,plain,
( ! [X0] :
( r2_hidden(sK4(k2_relat_1(sF35),X0),sK1)
| r1_tarski(k2_relat_1(sF35),X0) )
| ~ spl36_8
| ~ spl36_45 ),
inference(resolution,[],[f5725,f272]) ).
fof(f5866,plain,
( r1_tarski(k2_relat_1(sF35),sK1)
| r1_tarski(k2_relat_1(sF35),sK1)
| ~ spl36_8
| ~ spl36_45 ),
inference(resolution,[],[f5744,f273]) ).
fof(f5871,plain,
( r1_tarski(k2_relat_1(sF35),sK1)
| ~ spl36_8
| ~ spl36_45 ),
inference(duplicate_literal_removal,[],[f5866]) ).
fof(f6157,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF33)
| ~ m2_lattice4(sK1,sK0)
| v1_xboole_0(sK1)
| r2_hidden(k1_funct_1(sF31,X0),sK1) )
| ~ spl36_48 ),
inference(superposition,[],[f4841,f403]) ).
fof(f6165,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF33)
| v1_xboole_0(sK1)
| r2_hidden(k1_funct_1(sF31,X0),sK1) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f6157,f235]) ).
fof(f6166,plain,
( ! [X0] :
( r2_hidden(k1_funct_1(sF31,X0),sK1)
| ~ r2_hidden(X0,sF33) )
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f6165,f236]) ).
fof(f6171,plain,
( ! [X0] :
( r2_hidden(X0,sK1)
| ~ r2_hidden(sK6(sF32,X0),sF33)
| ~ r2_hidden(X0,k2_relat_1(sF32)) )
| ~ spl36_48 ),
inference(superposition,[],[f6166,f966]) ).
fof(f6188,plain,
( ! [X0] :
( ~ r2_hidden(X0,k2_relat_1(sF32))
| r2_hidden(X0,sK1) )
| ~ spl36_10
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f6171,f2674]) ).
fof(f6207,plain,
( ! [X0] :
( r2_hidden(sK4(k2_relat_1(sF32),X0),sK1)
| r1_tarski(k2_relat_1(sF32),X0) )
| ~ spl36_10
| ~ spl36_48 ),
inference(resolution,[],[f6188,f272]) ).
fof(f6326,plain,
( $false
| spl36_4 ),
inference(forward_subsumption_resolution,[],[f439,f584]) ).
fof(f6327,plain,
spl36_4,
inference(avatar_contradiction_clause,[],[f6326]) ).
fof(f6336,plain,
( m2_relset_1(sF35,sF33,sK1)
| ~ spl36_8
| ~ spl36_45 ),
inference(resolution,[],[f5871,f3602]) ).
fof(f6342,plain,
( $false
| spl36_3
| ~ spl36_8
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f6336,f436]) ).
fof(f6343,plain,
( spl36_3
| ~ spl36_8
| ~ spl36_45 ),
inference(avatar_contradiction_clause,[],[f6342]) ).
fof(f6350,plain,
( m1_relset_1(sF35,sF33,sK1)
| ~ spl36_8
| ~ spl36_45 ),
inference(resolution,[],[f6336,f369]) ).
fof(f6353,plain,
( v1_funct_2(sF35,sF33,sK1)
| k1_xboole_0 = sK1
| ~ spl36_8
| ~ spl36_45 ),
inference(resolution,[],[f6350,f2645]) ).
fof(f6377,definition,
( spl36_58
<=> k1_xboole_0 = sK1 ),
introduced(definition,[new_symbols(definition,[spl36_58])],[avatar_definition]) ).
fof(f6378,plain,
( k1_xboole_0 = sK1
| ~ spl36_58 ),
inference(avatar_component_clause,[],[f6377]) ).
fof(f6380,plain,
( spl36_58
| spl36_2
| ~ spl36_8
| ~ spl36_45 ),
inference(avatar_split_clause,[],[f6353,f4341,f610,f432,f6377]) ).
fof(f6393,plain,
( r1_tarski(k2_relat_1(sF32),sK1)
| r1_tarski(k2_relat_1(sF32),sK1)
| ~ spl36_10
| ~ spl36_48 ),
inference(resolution,[],[f6207,f273]) ).
fof(f6397,plain,
( r1_tarski(k2_relat_1(sF32),sK1)
| ~ spl36_10
| ~ spl36_48 ),
inference(duplicate_literal_removal,[],[f6393]) ).
fof(f6400,plain,
( m2_relset_1(sF32,sF33,sK1)
| ~ spl36_10
| ~ spl36_48 ),
inference(resolution,[],[f6397,f3603]) ).
fof(f6406,plain,
( $false
| spl36_6
| ~ spl36_10
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f6400,f445]) ).
fof(f6407,plain,
( spl36_6
| ~ spl36_10
| ~ spl36_48 ),
inference(avatar_contradiction_clause,[],[f6406]) ).
fof(f6411,plain,
( m1_relset_1(sF32,sF33,sK1)
| ~ spl36_10
| ~ spl36_48 ),
inference(resolution,[],[f6400,f369]) ).
fof(f6413,plain,
( v1_funct_2(sF32,sF33,sK1)
| k1_xboole_0 = sK1
| ~ spl36_10
| ~ spl36_48 ),
inference(resolution,[],[f6411,f2665]) ).
fof(f6418,plain,
( k1_xboole_0 = sK1
| spl36_5
| ~ spl36_10
| ~ spl36_48 ),
inference(forward_subsumption_resolution,[],[f6413,f442]) ).
fof(f6419,plain,
( spl36_58
| spl36_5
| ~ spl36_10
| ~ spl36_48 ),
inference(avatar_split_clause,[],[f6418,f4767,f617,f441,f6377]) ).
fof(f6421,plain,
( ~ v1_xboole_0(k1_xboole_0)
| ~ spl36_58 ),
inference(superposition,[],[f236,f6378]) ).
fof(f6464,plain,
( $false
| ~ spl36_58 ),
inference(forward_subsumption_resolution,[],[f6421,f315]) ).
fof(f6465,plain,
~ spl36_58,
inference(avatar_contradiction_clause,[],[f6464]) ).
cnf(s167,plain,
( ~ spl36_1
| ~ spl36_2
| ~ spl36_3
| ~ spl36_4
| ~ spl36_5
| ~ spl36_6 ),
inference(sat_conversion,[],[f446]) ).
cnf(s214,plain,
spl36_1,
inference(sat_conversion,[],[f559]) ).
cnf(s236,plain,
( ~ spl36_7
| spl36_8 ),
inference(sat_conversion,[],[f612]) ).
cnf(s238,plain,
( ~ spl36_9
| spl36_10 ),
inference(sat_conversion,[],[f619]) ).
cnf(s472,plain,
( spl36_11
| spl36_12 ),
inference(sat_conversion,[],[f1111]) ).
cnf(s489,plain,
( ~ spl36_11
| spl36_12
| spl36_13 ),
inference(sat_conversion,[],[f1144]) ).
cnf(s501,plain,
~ spl36_12,
inference(sat_conversion,[],[f1195]) ).
cnf(s709,plain,
~ spl36_29,
inference(sat_conversion,[],[f1765]) ).
cnf(s1003,plain,
( ~ spl36_11
| ~ spl36_37
| spl36_38 ),
inference(sat_conversion,[],[f2608]) ).
cnf(s1007,plain,
spl36_37,
inference(sat_conversion,[],[f2617]) ).
cnf(s1010,plain,
( spl36_9
| ~ spl36_38 ),
inference(sat_conversion,[],[f2627]) ).
cnf(s1015,plain,
( spl36_7
| ~ spl36_13
| ~ spl36_38 ),
inference(sat_conversion,[],[f2629]) ).
cnf(s1637,plain,
( spl36_29
| spl36_45 ),
inference(sat_conversion,[],[f4343]) ).
cnf(s1752,plain,
( spl36_29
| spl36_48 ),
inference(sat_conversion,[],[f4769]) ).
cnf(s2199,plain,
spl36_4,
inference(sat_conversion,[],[f6327]) ).
cnf(s2219,plain,
( spl36_3
| ~ spl36_8
| ~ spl36_45 ),
inference(sat_conversion,[],[f6343]) ).
cnf(s2235,plain,
( spl36_2
| ~ spl36_8
| ~ spl36_45
| spl36_58 ),
inference(sat_conversion,[],[f6380]) ).
cnf(s2249,plain,
( spl36_6
| ~ spl36_10
| ~ spl36_48 ),
inference(sat_conversion,[],[f6407]) ).
cnf(s2255,plain,
( spl36_5
| ~ spl36_10
| ~ spl36_48
| spl36_58 ),
inference(sat_conversion,[],[f6419]) ).
cnf(s2299,plain,
~ spl36_58,
inference(sat_conversion,[],[f6465]) ).
cnf(s2301,plain,
( spl36_5
| ~ spl36_10
| ~ spl36_48 ),
inference(rat,[],[s2255,s2299]) ).
cnf(s2302,plain,
( spl36_2
| ~ spl36_8
| ~ spl36_45 ),
inference(rat,[],[s2235,s2299]) ).
cnf(s2305,plain,
( ~ spl36_11
| spl36_38 ),
inference(rat,[],[s1003,s1007]) ).
cnf(s2306,plain,
spl36_48,
inference(rat,[],[s1752,s709]) ).
cnf(s2307,plain,
spl36_45,
inference(rat,[],[s1637,s709]) ).
cnf(s2327,plain,
( ~ spl36_11
| spl36_13 ),
inference(rat,[],[s489,s501]) ).
cnf(s2328,plain,
spl36_11,
inference(rat,[],[s472,s501]) ).
cnf(s2330,plain,
spl36_38,
inference(rat,[],[s2305,s2328]) ).
cnf(s2332,plain,
spl36_13,
inference(rat,[],[s2327,s2328]) ).
cnf(s2333,plain,
spl36_9,
inference(rat,[],[s1010,s2330]) ).
cnf(s2334,plain,
spl36_7,
inference(rat,[],[s1015,s2330,s2332]) ).
cnf(s2335,plain,
spl36_10,
inference(rat,[],[s238,s2333]) ).
cnf(s2336,plain,
spl36_5,
inference(rat,[],[s2301,s2306,s2335]) ).
cnf(s2337,plain,
spl36_6,
inference(rat,[],[s2249,s2306,s2335]) ).
cnf(s2340,plain,
spl36_8,
inference(rat,[],[s236,s2334]) ).
cnf(s2341,plain,
spl36_2,
inference(rat,[],[s2302,s2307,s2340]) ).
cnf(s2342,plain,
spl36_3,
inference(rat,[],[s2219,s2307,s2340]) ).
cnf(s2345,plain,
$false,
inference(rat,[],[s167,s2337,s2336,s2199,s2342,s2341,s214]) ).
fof(f6466,plain,
$false,
inference(avatar_sat_refutation,[],[s2345]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT325+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 14:38:17 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.25/2.46 % (4058222)Detected formulas, will run a generic FOF schedule.
% 11.25/2.46 % (4058229)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=3193443952:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.25/2.46 % (4058228)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=3309808869:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.25/2.46 % (4058231)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=354010893:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.25/2.46 % (4058227)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=2468657315:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.25/2.46 % (4058230)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=961258488:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.25/2.46 % (4058230)Refutation not found, incomplete strategy
% 11.25/2.46 % (4058230)------------------------------
% 11.25/2.46 % (4058230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.25/2.46 % (4058230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.25/2.46 % (4058230)CaDiCaL version: 2.1.3
% 11.25/2.46 % (4058230)Termination reason: Refutation not found, incomplete strategy
% 11.25/2.46 % (4058230)Time elapsed: 0.003 s
% 11.25/2.46 % (4058230)Peak memory usage: 88 MB
% 11.25/2.46 % (4058230)Instructions burned: 2 (million)
% 11.25/2.46 % (4058232)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3832129389:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.25/2.46 % (4058233)dis-21_1_sil=8000:lcm=predicate:random_seed=3563428539:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.25/2.46 % (4058231)Instruction limit reached!
% 11.25/2.46 % (4058231)------------------------------
% 11.25/2.46 % (4058231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.25/2.46 % (4058231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.25/2.46 % (4058231)CaDiCaL version: 2.1.3
% 11.25/2.46 % (4058231)Termination reason: Instruction limit
% 11.25/2.46 % (4058231)Termination phase: Saturation
% 11.25/2.46 % (4058231)Time elapsed: 0.076 s
% 11.25/2.46 % (4058231)Peak memory usage: 88 MB
% 11.25/2.46 % (4058231)Instructions burned: 120 (million)
% 11.25/2.46 % (4058233)Instruction limit reached!
% 11.25/2.46 % (4058233)------------------------------
% 11.25/2.46 % (4058233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.25/2.46 % (4058233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.25/2.46 % (4058233)CaDiCaL version: 2.1.3
% 11.25/2.46 % (4058233)Termination reason: Instruction limit
% 11.25/2.46 % (4058233)Termination phase: Saturation
% 11.25/2.46 % (4058233)Time elapsed: 0.075 s
% 11.25/2.46 % (4058233)Peak memory usage: 91 MB
% 11.25/2.46 % (4058233)Instructions burned: 131 (million)
% 11.25/2.46 % (4058232)Instruction limit reached!
% 11.25/2.46 % (4058232)------------------------------
% 11.25/2.46 % (4058232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.25/2.46 % (4058232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.25/2.46 % (4058232)CaDiCaL version: 2.1.3
% 11.25/2.46 % (4058232)Termination reason: Instruction limit
% 11.25/2.46 % (4058232)Termination phase: Saturation
% 11.25/2.46 % (4058232)Time elapsed: 0.100 s
% 11.25/2.46 % (4058232)Peak memory usage: 90 MB
% 11.25/2.46 % (4058232)Instructions burned: 140 (million)
% 11.25/2.46 % (4058241)lrs+10_1_sil=8000:sp=occurrence:random_seed=2336269839:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.25/2.46 % (4058242)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2528866018:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.25/2.46 % (4058243)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2292266853:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 11.25/2.46 % (4058230)------------------------------
% 11.25/2.46 % (4058230)------------------------------
% 11.25/2.46 % (4058242)Instruction limit reached!
% 11.25/2.46 % (4058242)------------------------------
% 11.25/2.46 % (4058242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.73 % (4058242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.73 % (4058242)CaDiCaL version: 2.1.3
% 20.14/3.73 % (4058242)Termination reason: Instruction limit
% 20.14/3.73 % (4058242)Termination phase: Saturation
% 20.14/3.73 % (4058242)Time elapsed: 0.076 s
% 20.14/3.73 % (4058242)Peak memory usage: 91 MB
% 20.14/3.73 % (4058242)Instructions burned: 158 (million)
% 20.14/3.73 % (4058241)Instruction limit reached!
% 20.14/3.73 % (4058241)------------------------------
% 20.14/3.73 % (4058241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.73 % (4058241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.73 % (4058241)CaDiCaL version: 2.1.3
% 20.14/3.73 % (4058241)Termination reason: Instruction limit
% 20.14/3.73 % (4058241)Termination phase: Saturation
% 20.14/3.73 % (4058241)Time elapsed: 0.174 s
% 20.14/3.73 % (4058241)Peak memory usage: 92 MB
% 20.14/3.73 % (4058241)Instructions burned: 286 (million)
% 20.14/3.73 % (4058247)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=1784798877:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 20.14/3.73 % (4058248)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=487647064:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 20.14/3.73 % (4058248)Refutation not found, incomplete strategy
% 20.14/3.73 % (4058248)------------------------------
% 20.14/3.73 % (4058248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.73 % (4058248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.73 % (4058248)CaDiCaL version: 2.1.3
% 20.14/3.73 % (4058248)Termination reason: Refutation not found, incomplete strategy
% 20.14/3.73 % (4058248)Time elapsed: 0.006 s
% 20.14/3.73 % (4058248)Peak memory usage: 88 MB
% 20.14/3.73 % (4058248)Instructions burned: 8 (million)
% 20.14/3.73 % (4058243)Instruction limit reached!
% 20.14/3.73 % (4058243)------------------------------
% 20.14/3.73 % (4058243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.73 % (4058243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.73 % (4058243)CaDiCaL version: 2.1.3
% 20.14/3.73 % (4058243)Termination reason: Instruction limit
% 20.14/3.73 % (4058243)Termination phase: Saturation
% 20.14/3.73 % (4058243)Time elapsed: 0.202 s
% 20.14/3.73 % (4058243)Peak memory usage: 91 MB
% 20.14/3.73 % (4058243)Instructions burned: 326 (million)
% 20.14/3.73 % (4058250)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1085130451:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 20.14/3.73 % (4058247)Instruction limit reached!
% 20.14/3.73 % (4058247)------------------------------
% 20.14/3.73 % (4058247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.73 % (4058247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.73 % (4058247)CaDiCaL version: 2.1.3
% 20.14/3.73 % (4058247)Termination reason: Instruction limit
% 20.14/3.73 % (4058247)Termination phase: Saturation
% 20.14/3.73 % (4058247)Time elapsed: 0.146 s
% 20.14/3.73 % (4058247)Peak memory usage: 93 MB
% 20.14/3.73 % (4058247)Instructions burned: 249 (million)
% 20.14/3.73 % (4058252)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2468063348:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 20.14/3.73 % (4058252)Instruction limit reached!
% 20.14/3.73 % (4058252)------------------------------
% 20.14/3.73 % (4058252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.73 % (4058252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.73 % (4058252)CaDiCaL version: 2.1.3
% 20.14/3.73 % (4058252)Termination reason: Instruction limit
% 20.14/3.73 % (4058252)Termination phase: Saturation
% 20.14/3.73 % (4058252)Time elapsed: 0.077 s
% 20.14/3.73 % (4058252)Peak memory usage: 90 MB
% 20.14/3.73 % (4058252)Instructions burned: 113 (million)
% 20.14/3.73 % (4058248)------------------------------
% 20.14/3.73 % (4058248)------------------------------
% 20.14/3.73 % (4058254)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2653782356:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 20.14/3.73 % (4058254)Instruction limit reached!
% 20.14/3.73 % (4058254)------------------------------
% 20.14/3.73 % (4058254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.73 % (4058254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058254)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058254)Termination reason: Instruction limit
% 13.98/5.51 % (4058254)Termination phase: Saturation
% 13.98/5.51 % (4058254)Time elapsed: 0.069 s
% 13.98/5.51 % (4058254)Peak memory usage: 89 MB
% 13.98/5.51 % (4058254)Instructions burned: 127 (million)
% 13.98/5.51 % (4058256)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4035320241:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 13.98/5.51 % (4058258)lrs+10_1_sil=8000:sp=occurrence:random_seed=4243635627:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 13.98/5.51 % (4058256)Instruction limit reached!
% 13.98/5.51 % (4058256)------------------------------
% 13.98/5.51 % (4058256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058256)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058256)Termination reason: Instruction limit
% 13.98/5.51 % (4058256)Termination phase: Saturation
% 13.98/5.51 % (4058256)Time elapsed: 0.062 s
% 13.98/5.51 % (4058256)Peak memory usage: 90 MB
% 13.98/5.51 % (4058256)Instructions burned: 114 (million)
% 13.98/5.51 % (4058259)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=991112526:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 13.98/5.51 % (4058259)Refutation not found, incomplete strategy
% 13.98/5.51 % (4058259)------------------------------
% 13.98/5.51 % (4058259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058259)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058259)Termination reason: Refutation not found, incomplete strategy
% 13.98/5.51 % (4058259)Time elapsed: 0.007 s
% 13.98/5.51 % (4058259)Peak memory usage: 88 MB
% 13.98/5.51 % (4058259)Instructions burned: 9 (million)
% 13.98/5.51 % (4058262)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1897391925:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 13.98/5.51 % (4058259)------------------------------
% 13.98/5.51 % (4058259)------------------------------
% 13.98/5.51 % (4058265)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3725017391:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 13.98/5.51 % (4058258)Instruction limit reached!
% 13.98/5.51 % (4058258)------------------------------
% 13.98/5.51 % (4058258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058258)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058258)Termination reason: Instruction limit
% 13.98/5.51 % (4058258)Termination phase: Saturation
% 13.98/5.51 % (4058258)Time elapsed: 0.532 s
% 13.98/5.51 % (4058258)Peak memory usage: 100 MB
% 13.98/5.51 % (4058258)Instructions burned: 907 (million)
% 13.98/5.51 % (4058265)Instruction limit reached!
% 13.98/5.51 % (4058265)------------------------------
% 13.98/5.51 % (4058265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058265)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058265)Termination reason: Instruction limit
% 13.98/5.51 % (4058265)Termination phase: Saturation
% 13.98/5.51 % (4058265)Time elapsed: 0.073 s
% 13.98/5.51 % (4058265)Peak memory usage: 91 MB
% 13.98/5.51 % (4058265)Instructions burned: 135 (million)
% 13.98/5.51 % (4058267)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1282225020:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 13.98/5.51 % (4058267)Refutation not found, incomplete strategy
% 13.98/5.51 % (4058267)------------------------------
% 13.98/5.51 % (4058267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058267)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058267)Termination reason: Refutation not found, incomplete strategy
% 13.98/5.51 % (4058267)Time elapsed: 0.006 s
% 13.98/5.51 % (4058267)Peak memory usage: 88 MB
% 13.98/5.51 % (4058267)Instructions burned: 8 (million)
% 13.98/5.51 % (4058268)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2580290595:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 13.98/5.51 % (4058267)------------------------------
% 13.98/5.51 % (4058267)------------------------------
% 13.98/5.51 % (4058272)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=64185054:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 13.98/5.51 % (4058272)Instruction limit reached!
% 13.98/5.51 % (4058272)------------------------------
% 13.98/5.51 % (4058272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058272)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058272)Termination reason: Instruction limit
% 13.98/5.51 % (4058272)Termination phase: Saturation
% 13.98/5.51 % (4058272)Time elapsed: 0.075 s
% 13.98/5.51 % (4058272)Peak memory usage: 91 MB
% 13.98/5.51 % (4058272)Instructions burned: 125 (million)
% 13.98/5.51 % (4058274)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=917159102:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 13.98/5.51 % (4058250)Instruction limit reached!
% 13.98/5.51 % (4058250)------------------------------
% 13.98/5.51 % (4058250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058250)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058250)Termination reason: Instruction limit
% 13.98/5.51 % (4058250)Termination phase: Saturation
% 13.98/5.51 % (4058250)Time elapsed: 1.544 s
% 13.98/5.51 % (4058250)Peak memory usage: 142 MB
% 13.98/5.51 % (4058250)Instructions burned: 2351 (million)
% 13.98/5.51 % (4058274)Instruction limit reached!
% 13.98/5.51 % (4058274)------------------------------
% 13.98/5.51 % (4058274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058274)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058274)Termination reason: Instruction limit
% 13.98/5.51 % (4058274)Termination phase: Saturation
% 13.98/5.51 % (4058274)Time elapsed: 0.094 s
% 13.98/5.51 % (4058274)Peak memory usage: 90 MB
% 13.98/5.51 % (4058274)Instructions burned: 135 (million)
% 13.98/5.51 % (4058276)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2699598843:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 13.98/5.51 % (4058276)Refutation not found, incomplete strategy
% 13.98/5.51 % (4058276)------------------------------
% 13.98/5.51 % (4058276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058276)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058276)Termination reason: Refutation not found, incomplete strategy
% 13.98/5.51 % (4058276)Time elapsed: 0.004 s
% 13.98/5.51 % (4058276)Peak memory usage: 88 MB
% 13.98/5.51 % (4058276)Instructions burned: 5 (million)
% 13.98/5.51 % (4058277)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1687656554:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 13.98/5.51 % (4058276)------------------------------
% 13.98/5.51 % (4058276)------------------------------
% 13.98/5.51 % (4058277)Instruction limit reached!
% 13.98/5.51 % (4058277)------------------------------
% 13.98/5.51 % (4058277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058277)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058277)Termination reason: Instruction limit
% 13.98/5.51 % (4058277)Termination phase: Saturation
% 13.98/5.51 % (4058277)Time elapsed: 0.246 s
% 13.98/5.51 % (4058277)Peak memory usage: 95 MB
% 13.98/5.51 % (4058277)Instructions burned: 431 (million)
% 13.98/5.51 % (4058280)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=4079647787:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 13.98/5.51 % (4058281)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=880962386:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 13.98/5.51 % (4058281)Instruction limit reached!
% 13.98/5.51 % (4058281)------------------------------
% 13.98/5.51 % (4058281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058281)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058281)Termination reason: Instruction limit
% 13.98/5.51 % (4058281)Termination phase: Saturation
% 13.98/5.51 % (4058281)Time elapsed: 0.079 s
% 13.98/5.51 % (4058281)Peak memory usage: 91 MB
% 13.98/5.51 % (4058281)Instructions burned: 151 (million)
% 13.98/5.51 % (4058284)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1916929366:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 13.98/5.51 % (4058262)Instruction limit reached!
% 13.98/5.51 % (4058262)------------------------------
% 13.98/5.51 % (4058262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058262)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058262)Termination reason: Instruction limit
% 13.98/5.51 % (4058262)Termination phase: Saturation
% 13.98/5.51 % (4058262)Time elapsed: 3.149 s
% 13.98/5.51 % (4058262)Peak memory usage: 157 MB
% 13.98/5.51 % (4058262)Instructions burned: 5203 (million)
% 13.98/5.51 % (4058280)First to succeed.
% 13.98/5.51 % (4058280)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4058222"
% 13.98/5.51 % (4058286)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2896166830:i=667:av=off:fsr=off_2957 on theBenchmark for (2957ds/667Mi)
% 13.98/5.51 % (4058286)Refutation not found, incomplete strategy
% 13.98/5.51 % (4058286)------------------------------
% 13.98/5.51 % (4058286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.98/5.51 % (4058286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/5.51 % (4058286)CaDiCaL version: 2.1.3
% 13.98/5.51 % (4058286)Termination reason: Refutation not found, incomplete strategy
% 13.98/5.51 % (4058286)Time elapsed: 0.005 s
% 13.98/5.51 % (4058286)Peak memory usage: 88 MB
% 13.98/5.51 % (4058286)Instructions burned: 8 (million)
% 13.98/5.51 % (4058286)------------------------------
% 13.98/5.51 % (4058286)------------------------------
% 13.98/5.51 % (4058280)Refutation found. Thanks to Tanya!
% 13.98/5.51 % SZS status Theorem for theBenchmark
% 13.98/5.51 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/5.71 % (4058280)------------------------------
% 0.16/5.71 % (4058280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/5.71 % (4058280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/5.71 % (4058280)CaDiCaL version: 2.1.3
% 0.16/5.71 % (4058280)Termination reason: Refutation
% 0.16/5.71 % (4058280)Time elapsed: 1.651 s
% 0.16/5.71 % (4058280)Peak memory usage: 144 MB
% 0.16/5.71 % (4058280)Instructions burned: 2443 (million)
% 0.16/5.71 % (4058280)------------------------------
% 0.16/5.71 % (4058280)------------------------------
% 0.16/5.71 % (4058222)Success in time 4.663 s
% 0.16/5.71 % Vampire exiting
%------------------------------------------------------------------------------