%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT315+3 : 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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:50 AM UTC 2026
% Result : Theorem 65.07s 14.42s
% Output : Refutation 89.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 77
% Syntax : Number of formulae : 646 ( 123 unt; 38 def)
% Number of atoms : 2311 ( 300 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 2789 (1124 ~;1406 |; 177 &)
% ( 37 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 47 ( 45 usr; 28 prp; 0-3 aty)
% Number of functors : 38 ( 38 usr; 16 con; 0-3 aty)
% Number of variables : 567 ( 0 sgn 556 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,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(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f66,axiom,
! [X0] : k5_xboole_0(X0,k1_xboole_0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_boole) ).
fof(f68,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f70,axiom,
! [X0,X1,X2] :
( ( r1_tarski(X0,X1)
& r1_tarski(X1,X2) )
=> r1_tarski(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f79,axiom,
! [X0,X1,X2] :
( r1_tarski(X0,X1)
=> r1_tarski(X0,k2_xboole_0(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_xboole_1) ).
fof(f81,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
=> k2_xboole_0(X0,X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_xboole_1) ).
fof(f90,axiom,
! [X0,X1] : k3_xboole_0(X0,k2_xboole_0(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_xboole_1) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f160,axiom,
! [X0,X1,X2] : k5_xboole_0(k5_xboole_0(X0,X1),X2) = k5_xboole_0(X0,k5_xboole_0(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t91_xboole_1) ).
fof(f161,axiom,
! [X0] : k5_xboole_0(X0,X0) = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t92_xboole_1) ).
fof(f163,axiom,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(k5_xboole_0(X0,X1),k3_xboole_0(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t94_xboole_1) ).
fof(f418,axiom,
! [X0,X1] : k3_tarski(k2_tarski(X0,X1)) = k2_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t93_zfmisc_1) ).
fof(f567,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_subset_1) ).
fof(f568,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k4_subset_1) ).
fof(f570,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_subset_1) ).
fof(f572,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k5_subset_1) ).
fof(f574,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f602,axiom,
! [X0,X1] : k1_setfam_1(k2_tarski(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_setfam_1) ).
fof(f677,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(f3551,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_card_1) ).
fof(f8626,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),k3_filter_0(X0,X1),X2))
& k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,k3_filter_0(X0,X2))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t47_filter_0) ).
fof(f9358,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f9363,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f9391,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f9463,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f10273,axiom,
k5_nat_lat = np__0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_nat_lat) ).
fof(f10607,axiom,
! [X0] : k1_pcomps_1(X0) = k1_zfmisc_1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_pcomps_1) ).
fof(f12317,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(f13532,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f13536,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f13542,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> k3_filter_2(X0,X1) = k3_filter_0(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k3_filter_2) ).
fof(f13567,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m2_filter_2(k19_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k19_filter_2) ).
fof(f13601,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f13611,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_filter_2(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_filter_2) ).
fof(f13623,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( m2_filter_2(X2,X0)
=> ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( m2_filter_2(X3,X0)
=> ( r1_tarski(X1,X3)
=> r1_tarski(X2,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_filter_2) ).
fof(f13625,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t37_filter_2) ).
fof(f13627,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X3] :
( ( ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( ( r1_tarski(X2,X3)
=> r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3)) )
& r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t39_filter_2) ).
fof(f13641,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),k19_filter_2(X0,X1),X2)))
& r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,k19_filter_2(X0,X2)))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t49_filter_2) ).
fof(f13642,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),k19_filter_2(X0,X1),X2)))
& r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,k19_filter_2(X0,X2)))) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13641]) ).
fof(f13972,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f13995,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f13997,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f13998,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(flattening,[],[f13997]) ).
fof(f14003,plain,
! [X0,X1,X2] :
( r1_tarski(X0,k2_xboole_0(X2,X1))
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f79]) ).
fof(f14005,plain,
! [X0,X1] :
( k2_xboole_0(X0,X1) = X1
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f81]) ).
fof(f14280,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f567]) ).
fof(f14281,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f14280]) ).
fof(f14282,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f568]) ).
fof(f14283,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f14282]) ).
fof(f14286,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f570]) ).
fof(f14287,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f14286]) ).
fof(f14290,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f572]) ).
fof(f14291,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f14290]) ).
fof(f14294,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f574]) ).
fof(f14295,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f14294]) ).
fof(f24089,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),k3_filter_0(X0,X1),X2))
& k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,k3_filter_0(X0,X2))) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8626]) ).
fof(f24090,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),k3_filter_0(X0,X1),X2))
& k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,k3_filter_0(X0,X2))) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f24089]) ).
fof(f25363,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9358]) ).
fof(f25364,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f25363]) ).
fof(f25373,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9363]) ).
fof(f25374,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f25373]) ).
fof(f25414,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9391]) ).
fof(f25415,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f25414]) ).
fof(f25550,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f30156,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,[],[f12317]) ).
fof(f30157,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,[],[f30156]) ).
fof(f32344,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13532]) ).
fof(f32345,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f32344]) ).
fof(f32352,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f13536]) ).
fof(f32353,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f32352]) ).
fof(f32364,plain,
! [X0,X1] :
( k3_filter_2(X0,X1) = k3_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f13542]) ).
fof(f32365,plain,
! [X0,X1] :
( k3_filter_2(X0,X1) = k3_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f32364]) ).
fof(f32414,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f13567]) ).
fof(f32415,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f32414]) ).
fof(f32479,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13601]) ).
fof(f32480,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f32479]) ).
fof(f32499,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13611]) ).
fof(f32500,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f32499]) ).
fof(f32523,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13623]) ).
fof(f32524,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f32523]) ).
fof(f32527,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13625]) ).
fof(f32528,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f32527]) ).
fof(f32531,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3))
| ~ r1_tarski(X2,X3) )
& r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) )
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13627]) ).
fof(f32532,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3))
| ~ r1_tarski(X2,X3) )
& r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) )
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f32531]) ).
fof(f32559,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),k19_filter_2(X0,X1),X2)))
| ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,k19_filter_2(X0,X2)))) )
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f13642]) ).
fof(f32560,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),k19_filter_2(X0,X1),X2)))
| ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,k19_filter_2(X0,X2)))) )
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f32559]) ).
fof(f33173,definition,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP387(X0) ),
introduced(definition,[new_symbols(definition,[sP387])],[predicate_definition_introduction]) ).
fof(f33174,plain,
! [X0] :
( sP387(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f25374,f33173]) ).
fof(f33572,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f13972]) ).
fof(f33573,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f33572]) ).
fof(f33574,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK629(X0,X1),X1)
& r2_hidden(sK629(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK629]),skolemize(X2,sK629(X0,X1))],[f33573]) ).
fof(f33616,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f33617,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f33616]) ).
fof(f33822,plain,
! [X0,X1] :
( ( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) )
& ( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f677]) ).
fof(f38432,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP387(X0) ),
inference(nnf_transformation,[],[f33173]) ).
fof(f41219,plain,
! [X0,X1,X2] :
( ( ( r1_filter_2(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_filter_2(X0,X1,X2) ) )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f32353]) ).
fof(f41254,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f32524]) ).
fof(f41255,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f41254]) ).
fof(f41256,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f41255]) ).
fof(f41257,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ( ~ r1_tarski(X2,sK4865(X0,X1,X2))
& r1_tarski(X1,sK4865(X0,X1,X2))
& m2_filter_2(sK4865(X0,X1,X2),X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4865]),skolemize(X3,sK4865(X0,X1,X2))],[f41256]) ).
fof(f41264,plain,
( ( ~ r1_filter_2(u1_struct_0(sK4870),k19_filter_2(sK4870,k4_subset_1(u1_struct_0(sK4870),sK4871,sK4872)),k19_filter_2(sK4870,k4_subset_1(u1_struct_0(sK4870),k19_filter_2(sK4870,sK4871),sK4872)))
| ~ r1_filter_2(u1_struct_0(sK4870),k19_filter_2(sK4870,k4_subset_1(u1_struct_0(sK4870),sK4871,sK4872)),k19_filter_2(sK4870,k4_subset_1(u1_struct_0(sK4870),sK4871,k19_filter_2(sK4870,sK4872)))) )
& ~ v1_xboole_0(sK4872)
& m1_subset_1(sK4872,k1_zfmisc_1(u1_struct_0(sK4870)))
& ~ v1_xboole_0(sK4871)
& m1_subset_1(sK4871,k1_zfmisc_1(u1_struct_0(sK4870)))
& ~ v3_struct_0(sK4870)
& v10_lattices(sK4870)
& l3_lattices(sK4870) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4870,sK4871,sK4872]),skolemize(X0,sK4870),skolemize(X1,sK4871),skolemize(X2,sK4872)],[f32560]) ).
fof(f41279,plain,
! [X0,X1] :
( r2_hidden(sK629(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f33574]) ).
fof(f41356,plain,
! [X0,X1] :
( r1_tarski(X1,X0)
| X0 != X1 ),
inference(cnf_transformation,[],[f33617]) ).
fof(f41358,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f33617]) ).
fof(f41401,plain,
! [X0] : k5_xboole_0(X0,k1_xboole_0) = X0,
inference(cnf_transformation,[],[f66]) ).
fof(f41403,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f13995]) ).
fof(f41405,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X1,X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(X0,X2) ),
inference(cnf_transformation,[],[f13998]) ).
fof(f41414,plain,
! [X2,X0,X1] :
( r1_tarski(X0,k2_xboole_0(X2,X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f14003]) ).
fof(f41416,plain,
! [X0,X1] :
( k2_xboole_0(X0,X1) = X1
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f14005]) ).
fof(f41429,plain,
! [X0,X1] : k3_xboole_0(X0,k2_xboole_0(X0,X1)) = X0,
inference(cnf_transformation,[],[f90]) ).
fof(f41457,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f41504,plain,
! [X2,X0,X1] : k5_xboole_0(k5_xboole_0(X0,X1),X2) = k5_xboole_0(X0,k5_xboole_0(X1,X2)),
inference(cnf_transformation,[],[f160]) ).
fof(f41505,plain,
! [X0] : k1_xboole_0 = k5_xboole_0(X0,X0),
inference(cnf_transformation,[],[f161]) ).
fof(f41507,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(k5_xboole_0(X0,X1),k3_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f163]) ).
fof(f41821,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k3_tarski(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f418]) ).
fof(f42046,plain,
! [X2,X0,X1] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f14281]) ).
fof(f42047,plain,
! [X2,X0,X1] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f14283]) ).
fof(f42049,plain,
! [X2,X0,X1] :
( k2_xboole_0(X1,X2) = k4_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f14287]) ).
fof(f42051,plain,
! [X2,X0,X1] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f14291]) ).
fof(f42053,plain,
! [X2,X0,X1] :
( k3_xboole_0(X1,X2) = k5_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f14295]) ).
fof(f42092,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k1_setfam_1(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f602]) ).
fof(f42190,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f33822]) ).
fof(f42191,plain,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f33822]) ).
fof(f47925,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f3551]) ).
fof(f57916,plain,
! [X2,X0,X1] :
( k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),k3_filter_0(X0,X1),X2))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f24090]) ).
fof(f59195,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f25364]) ).
fof(f59216,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP387(X0) ),
inference(cnf_transformation,[],[f38432]) ).
fof(f59225,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP387(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f33174]) ).
fof(f59342,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f25415]) ).
fof(f59463,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f25550]) ).
fof(f60826,plain,
np__0 = k5_nat_lat,
inference(cnf_transformation,[],[f10273]) ).
fof(f61560,plain,
! [X0] : k1_zfmisc_1(X0) = k1_pcomps_1(X0),
inference(cnf_transformation,[],[f10607]) ).
fof(f65894,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(cnf_transformation,[],[f30157]) ).
fof(f69551,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f32345]) ).
fof(f69552,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f32345]) ).
fof(f69557,plain,
! [X2,X0,X1] :
( r1_filter_2(X0,X1,X2)
| X1 != X2
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f41219]) ).
fof(f69563,plain,
! [X0,X1] :
( k3_filter_0(X0,X1) = k3_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f32365]) ).
fof(f69590,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f32415]) ).
fof(f69664,plain,
! [X0,X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f32480]) ).
fof(f69688,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f32500]) ).
fof(f69715,plain,
! [X2,X0,X1] :
( r1_tarski(X1,X2)
| k19_filter_2(X0,X1) != X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f41257]) ).
fof(f69717,plain,
! [X2,X0,X1] :
( k19_filter_2(X0,X1) = X2
| ~ r1_tarski(X1,X2)
| r1_tarski(X1,sK4865(X0,X1,X2))
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f41257]) ).
fof(f69718,plain,
! [X2,X0,X1] :
( k19_filter_2(X0,X1) = X2
| ~ r1_tarski(X1,X2)
| ~ r1_tarski(X2,sK4865(X0,X1,X2))
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f41257]) ).
fof(f69724,plain,
! [X2,X0,X1] :
( k19_filter_2(X0,X1) = k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f32528]) ).
fof(f69727,plain,
! [X2,X3,X0,X1] :
( r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3))
| ~ r1_tarski(X2,X3)
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f32532]) ).
fof(f69759,plain,
l3_lattices(sK4870),
inference(cnf_transformation,[],[f41264]) ).
fof(f69760,plain,
v10_lattices(sK4870),
inference(cnf_transformation,[],[f41264]) ).
fof(f69761,plain,
~ v3_struct_0(sK4870),
inference(cnf_transformation,[],[f41264]) ).
fof(f69762,plain,
m1_subset_1(sK4871,k1_zfmisc_1(u1_struct_0(sK4870))),
inference(cnf_transformation,[],[f41264]) ).
fof(f69763,plain,
~ v1_xboole_0(sK4871),
inference(cnf_transformation,[],[f41264]) ).
fof(f69764,plain,
m1_subset_1(sK4872,k1_zfmisc_1(u1_struct_0(sK4870))),
inference(cnf_transformation,[],[f41264]) ).
fof(f69765,plain,
~ v1_xboole_0(sK4872),
inference(cnf_transformation,[],[f41264]) ).
fof(f69766,plain,
( ~ r1_filter_2(u1_struct_0(sK4870),k19_filter_2(sK4870,k4_subset_1(u1_struct_0(sK4870),sK4871,sK4872)),k19_filter_2(sK4870,k4_subset_1(u1_struct_0(sK4870),k19_filter_2(sK4870,sK4871),sK4872)))
| ~ r1_filter_2(u1_struct_0(sK4870),k19_filter_2(sK4870,k4_subset_1(u1_struct_0(sK4870),sK4871,sK4872)),k19_filter_2(sK4870,k4_subset_1(u1_struct_0(sK4870),sK4871,k19_filter_2(sK4870,sK4872)))) ),
inference(cnf_transformation,[],[f41264]) ).
fof(f69767,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),
inference(definition_unfolding,[],[f41507,f41457]) ).
fof(f69769,plain,
k1_xboole_0 = k5_nat_lat,
inference(definition_unfolding,[],[f47925,f60826]) ).
fof(f69855,plain,
! [X0] : k5_xboole_0(X0,k5_nat_lat) = X0,
inference(definition_unfolding,[],[f41401,f69769]) ).
fof(f69865,plain,
! [X2,X0,X1] :
( r1_tarski(X0,k5_xboole_0(k5_xboole_0(X2,X1),k4_xboole_0(X2,k4_xboole_0(X2,X1))))
| ~ r1_tarski(X0,X1) ),
inference(definition_unfolding,[],[f41414,f69767]) ).
fof(f69867,plain,
! [X0,X1] :
( k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))) = X1
| ~ r1_tarski(X0,X1) ),
inference(definition_unfolding,[],[f41416,f69767]) ).
fof(f69880,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))))) = X0,
inference(definition_unfolding,[],[f41429,f41457,f69767]) ).
fof(f69931,plain,
! [X0] : k5_xboole_0(X0,X0) = k5_nat_lat,
inference(definition_unfolding,[],[f41505,f69769]) ).
fof(f70148,plain,
! [X0,X1] : k3_tarski(k2_tarski(X0,X1)) = k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),
inference(definition_unfolding,[],[f41821,f69767]) ).
fof(f70333,plain,
! [X2,X0,X1] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_pcomps_1(X0))
| ~ m1_subset_1(X1,k1_pcomps_1(X0))
| ~ m1_subset_1(X2,k1_pcomps_1(X0)) ),
inference(definition_unfolding,[],[f42046,f61560,f61560,f61560]) ).
fof(f70334,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_pcomps_1(X0))
| ~ m1_subset_1(X1,k1_pcomps_1(X0))
| k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1) ),
inference(definition_unfolding,[],[f42047,f61560,f61560]) ).
fof(f70336,plain,
! [X2,X0,X1] :
( k4_subset_1(X0,X1,X2) = k5_xboole_0(k5_xboole_0(X1,X2),k4_xboole_0(X1,k4_xboole_0(X1,X2)))
| ~ m1_subset_1(X1,k1_pcomps_1(X0))
| ~ m1_subset_1(X2,k1_pcomps_1(X0)) ),
inference(definition_unfolding,[],[f42049,f69767,f61560,f61560]) ).
fof(f70338,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_pcomps_1(X0))
| ~ m1_subset_1(X1,k1_pcomps_1(X0))
| k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1) ),
inference(definition_unfolding,[],[f42051,f61560,f61560]) ).
fof(f70340,plain,
! [X2,X0,X1] :
( k5_subset_1(X0,X1,X2) = k4_xboole_0(X1,k4_xboole_0(X1,X2))
| ~ m1_subset_1(X1,k1_pcomps_1(X0))
| ~ m1_subset_1(X2,k1_pcomps_1(X0)) ),
inference(definition_unfolding,[],[f42053,f41457,f61560,f61560]) ).
fof(f70365,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k1_setfam_1(k2_tarski(X0,X1)),
inference(definition_unfolding,[],[f42092,f41457]) ).
fof(f70421,plain,
! [X0,X1] :
( m1_subset_1(X0,k1_pcomps_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(definition_unfolding,[],[f42191,f61560]) ).
fof(f70422,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(X1))
| r1_tarski(X0,X1) ),
inference(definition_unfolding,[],[f42190,f61560]) ).
fof(f76569,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_pcomps_1(u1_struct_0(X0)))
| v1_xboole_0(X2)
| k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),k3_filter_0(X0,X1),X2))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_unfolding,[],[f57916,f61560,f61560]) ).
fof(f78642,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_unfolding,[],[f65894,f61560]) ).
fof(f79669,plain,
! [X2,X0,X1] :
( r1_filter_2(X0,X1,X2)
| X1 != X2
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_pcomps_1(X0))
| ~ m1_subset_1(X2,k1_pcomps_1(X0)) ),
inference(definition_unfolding,[],[f69557,f61560,f61560]) ).
fof(f79672,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| k3_filter_0(X0,X1) = k3_filter_2(X0,X1) ),
inference(definition_unfolding,[],[f69563,f61560]) ).
fof(f79675,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| m2_filter_2(k19_filter_2(X0,X1),X0) ),
inference(definition_unfolding,[],[f69590,f61560]) ).
fof(f79707,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| k7_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_unfolding,[],[f69664,f61560]) ).
fof(f79718,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X2,sK4865(X0,X1,X2))
| ~ r1_tarski(X1,X2)
| k19_filter_2(X0,X1) = X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_unfolding,[],[f69718,f61560]) ).
fof(f79719,plain,
! [X2,X0,X1] :
( r1_tarski(X1,sK4865(X0,X1,X2))
| ~ r1_tarski(X1,X2)
| k19_filter_2(X0,X1) = X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_unfolding,[],[f69717,f61560]) ).
fof(f79721,plain,
! [X2,X0,X1] :
( r1_tarski(X1,X2)
| k19_filter_2(X0,X1) != X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_unfolding,[],[f69715,f61560]) ).
fof(f79725,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_pcomps_1(u1_struct_0(k1_lattice2(X0))))
| v1_xboole_0(X2)
| k19_filter_2(X0,X1) = k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_unfolding,[],[f69724,f61560,f61560]) ).
fof(f79729,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,k1_pcomps_1(u1_struct_0(X0)))
| ~ r1_tarski(X2,X3)
| v1_xboole_0(X3)
| r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_pcomps_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_unfolding,[],[f69727,f61560,f61560,f61560]) ).
fof(f79750,plain,
m1_subset_1(sK4872,k1_pcomps_1(u1_struct_0(sK4870))),
inference(definition_unfolding,[],[f69764,f61560]) ).
fof(f79751,plain,
m1_subset_1(sK4871,k1_pcomps_1(u1_struct_0(sK4870))),
inference(definition_unfolding,[],[f69762,f61560]) ).
fof(f79778,plain,
! [X1] : r1_tarski(X1,X1),
inference(equality_resolution,[],[f41356]) ).
fof(f82325,plain,
! [X2,X0] :
( r1_filter_2(X0,X2,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X2,k1_pcomps_1(X0))
| ~ m1_subset_1(X2,k1_pcomps_1(X0)) ),
inference(equality_resolution,[],[f79669]) ).
fof(f82355,plain,
! [X0,X1] :
( ~ m2_filter_2(k19_filter_2(X0,X1),X0)
| r1_tarski(X1,k19_filter_2(X0,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f79721]) ).
fof(f82361,definition,
sF4873 = u1_struct_0(sK4870),
introduced(definition,[new_symbols(definition,[sF4873])],[function_definition]) ).
fof(f82362,plain,
u1_struct_0(sK4870) = sF4873,
inference(reorient_equations,[],[f82361]) ).
fof(f82363,definition,
sF4874 = k4_subset_1(sF4873,sK4871,sK4872),
introduced(definition,[new_symbols(definition,[sF4874])],[function_definition]) ).
fof(f82364,plain,
k4_subset_1(sF4873,sK4871,sK4872) = sF4874,
inference(reorient_equations,[],[f82363]) ).
fof(f82365,definition,
sF4875 = k19_filter_2(sK4870,sF4874),
introduced(definition,[new_symbols(definition,[sF4875])],[function_definition]) ).
fof(f82366,plain,
k19_filter_2(sK4870,sF4874) = sF4875,
inference(reorient_equations,[],[f82365]) ).
fof(f82367,definition,
sF4876 = k19_filter_2(sK4870,sK4871),
introduced(definition,[new_symbols(definition,[sF4876])],[function_definition]) ).
fof(f82368,plain,
k19_filter_2(sK4870,sK4871) = sF4876,
inference(reorient_equations,[],[f82367]) ).
fof(f82369,definition,
sF4877 = k4_subset_1(sF4873,sF4876,sK4872),
introduced(definition,[new_symbols(definition,[sF4877])],[function_definition]) ).
fof(f82370,plain,
k4_subset_1(sF4873,sF4876,sK4872) = sF4877,
inference(reorient_equations,[],[f82369]) ).
fof(f82371,definition,
sF4878 = k19_filter_2(sK4870,sF4877),
introduced(definition,[new_symbols(definition,[sF4878])],[function_definition]) ).
fof(f82372,plain,
k19_filter_2(sK4870,sF4877) = sF4878,
inference(reorient_equations,[],[f82371]) ).
fof(f82373,definition,
sF4879 = k19_filter_2(sK4870,sK4872),
introduced(definition,[new_symbols(definition,[sF4879])],[function_definition]) ).
fof(f82374,plain,
k19_filter_2(sK4870,sK4872) = sF4879,
inference(reorient_equations,[],[f82373]) ).
fof(f82375,definition,
sF4880 = k4_subset_1(sF4873,sK4871,sF4879),
introduced(definition,[new_symbols(definition,[sF4880])],[function_definition]) ).
fof(f82376,plain,
k4_subset_1(sF4873,sK4871,sF4879) = sF4880,
inference(reorient_equations,[],[f82375]) ).
fof(f82377,definition,
sF4881 = k19_filter_2(sK4870,sF4880),
introduced(definition,[new_symbols(definition,[sF4881])],[function_definition]) ).
fof(f82378,plain,
k19_filter_2(sK4870,sF4880) = sF4881,
inference(reorient_equations,[],[f82377]) ).
fof(f82379,plain,
( ~ r1_filter_2(sF4873,sF4875,sF4878)
| ~ r1_filter_2(sF4873,sF4875,sF4881) ),
inference(definition_folding,[],[f69766,f82378,f82376,f82374,f82362,f82366,f82364,f82362,f82362,f82372,f82370,f82368,f82362,f82366,f82364,f82362,f82362]) ).
fof(f82380,definition,
sF4882 = k1_pcomps_1(sF4873),
introduced(definition,[new_symbols(definition,[sF4882])],[function_definition]) ).
fof(f82381,plain,
k1_pcomps_1(sF4873) = sF4882,
inference(reorient_equations,[],[f82380]) ).
fof(f82382,plain,
m1_subset_1(sK4872,sF4882),
inference(definition_folding,[],[f79750,f82381,f82362]) ).
fof(f82383,plain,
m1_subset_1(sK4871,sF4882),
inference(definition_folding,[],[f79751,f82381,f82362]) ).
fof(f82387,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,k1_pcomps_1(X0))
| v1_xboole_0(X0)
| r1_filter_2(X0,X2,X2) ),
inference(duplicate_literal_removal,[],[f82325]) ).
fof(f82599,definition,
( spl4883_1
<=> r1_filter_2(sF4873,sF4875,sF4881) ),
introduced(definition,[new_symbols(definition,[spl4883_1])],[avatar_definition]) ).
fof(f82601,plain,
( ~ r1_filter_2(sF4873,sF4875,sF4881)
| spl4883_1 ),
inference(avatar_component_clause,[],[f82599]) ).
fof(f82603,definition,
( spl4883_2
<=> r1_filter_2(sF4873,sF4875,sF4878) ),
introduced(definition,[new_symbols(definition,[spl4883_2])],[avatar_definition]) ).
fof(f82604,plain,
( r1_filter_2(sF4873,sF4875,sF4878)
| ~ spl4883_2 ),
inference(avatar_component_clause,[],[f82603]) ).
fof(f82605,plain,
( ~ r1_filter_2(sF4873,sF4875,sF4878)
| spl4883_2 ),
inference(avatar_component_clause,[],[f82603]) ).
fof(f82606,plain,
( ~ spl4883_1
| ~ spl4883_2 ),
inference(avatar_split_clause,[],[f82379,f82603,f82599]) ).
fof(f88932,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_pcomps_1(X0))
| ~ m1_subset_1(X1,k1_pcomps_1(X0))
| k5_subset_1(X0,X1,X2) = k1_setfam_1(k2_tarski(X1,X2)) ),
inference(forward_demodulation,[],[f70340,f70365]) ).
fof(f88933,plain,
! [X2,X0,X1] :
( k4_subset_1(X0,X1,X2) = k5_xboole_0(k5_xboole_0(X1,X2),k1_setfam_1(k2_tarski(X1,X2)))
| ~ m1_subset_1(X1,k1_pcomps_1(X0))
| ~ m1_subset_1(X2,k1_pcomps_1(X0)) ),
inference(forward_demodulation,[],[f70336,f70365]) ).
fof(f89016,plain,
! [X0,X1] : k3_tarski(k2_tarski(X0,X1)) = k5_xboole_0(k5_xboole_0(X0,X1),k1_setfam_1(k2_tarski(X0,X1))),
inference(forward_demodulation,[],[f70148,f70365]) ).
fof(f89194,plain,
! [X0,X1] : k1_setfam_1(k2_tarski(X0,k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))))) = X0,
inference(forward_demodulation,[],[f69880,f70365]) ).
fof(f89205,plain,
! [X0,X1] :
( k5_xboole_0(X0,k5_xboole_0(X1,k4_xboole_0(X0,k4_xboole_0(X0,X1)))) = X1
| ~ r1_tarski(X0,X1) ),
inference(forward_demodulation,[],[f69867,f41504]) ).
fof(f89207,plain,
! [X2,X0,X1] :
( r1_tarski(X0,k5_xboole_0(X2,k5_xboole_0(X1,k4_xboole_0(X2,k4_xboole_0(X2,X1)))))
| ~ r1_tarski(X0,X1) ),
inference(forward_demodulation,[],[f69865,f41504]) ).
fof(f89930,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_pcomps_1(X0))
| ~ m1_subset_1(X1,k1_pcomps_1(X0))
| k4_subset_1(X0,X1,X2) = k5_xboole_0(X1,k5_xboole_0(X2,k1_setfam_1(k2_tarski(X1,X2)))) ),
inference(forward_demodulation,[],[f88933,f41504]) ).
fof(f89960,plain,
! [X0,X1] : k3_tarski(k2_tarski(X0,X1)) = k5_xboole_0(X0,k5_xboole_0(X1,k1_setfam_1(k2_tarski(X0,X1)))),
inference(forward_demodulation,[],[f89016,f41504]) ).
fof(f90116,plain,
! [X0,X1] : k1_setfam_1(k2_tarski(X0,k5_xboole_0(X0,k5_xboole_0(X1,k4_xboole_0(X0,k4_xboole_0(X0,X1)))))) = X0,
inference(forward_demodulation,[],[f89194,f41504]) ).
fof(f90123,plain,
! [X0,X1] :
( k5_xboole_0(X0,k5_xboole_0(X1,k1_setfam_1(k2_tarski(X0,X1)))) = X1
| ~ r1_tarski(X0,X1) ),
inference(forward_demodulation,[],[f89205,f70365]) ).
fof(f90125,plain,
! [X2,X0,X1] :
( r1_tarski(X0,k5_xboole_0(X2,k5_xboole_0(X1,k1_setfam_1(k2_tarski(X2,X1)))))
| ~ r1_tarski(X0,X1) ),
inference(forward_demodulation,[],[f89207,f70365]) ).
fof(f90729,plain,
! [X0,X1] : k1_setfam_1(k2_tarski(X0,k5_xboole_0(X0,k5_xboole_0(X1,k1_setfam_1(k2_tarski(X0,X1)))))) = X0,
inference(forward_demodulation,[],[f90116,f70365]) ).
fof(f90736,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| k3_tarski(k2_tarski(X0,X1)) = X1 ),
inference(forward_demodulation,[],[f90123,f89960]) ).
fof(f90738,plain,
! [X2,X0,X1] :
( r1_tarski(X0,k3_tarski(k2_tarski(X2,X1)))
| ~ r1_tarski(X0,X1) ),
inference(forward_demodulation,[],[f90125,f89960]) ).
fof(f91174,plain,
! [X0,X1] : k1_setfam_1(k2_tarski(X0,k3_tarski(k2_tarski(X0,X1)))) = X0,
inference(forward_demodulation,[],[f90729,f89960]) ).
fof(f94195,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870)
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK4870,X0),sK4870) ),
inference(superposition,[],[f79675,f82362]) ).
fof(f94196,plain,
( ~ m2_filter_2(sF4876,sK4870)
| r1_tarski(sK4871,sF4876)
| v1_xboole_0(sK4871)
| ~ m1_subset_1(sK4871,k1_pcomps_1(u1_struct_0(sK4870)))
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(superposition,[],[f82355,f82368]) ).
fof(f94207,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF4882)
| ~ m1_subset_1(X1,sF4882)
| k5_xboole_0(X1,k5_xboole_0(X0,k1_setfam_1(k2_tarski(X1,X0)))) = k4_subset_1(sF4873,X1,X0) ),
inference(superposition,[],[f89930,f82381]) ).
fof(f94208,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF4882)
| ~ m1_subset_1(X0,sF4882)
| k3_tarski(k2_tarski(X1,X0)) = k4_subset_1(sF4873,X1,X0) ),
inference(forward_demodulation,[],[f94207,f89960]) ).
fof(f94213,plain,
( m1_subset_1(sF4880,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sK4871,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sF4879,k1_pcomps_1(sF4873)) ),
inference(superposition,[],[f70333,f82376]) ).
fof(f94214,plain,
( m1_subset_1(sF4874,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sK4871,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sK4872,k1_pcomps_1(sF4873)) ),
inference(superposition,[],[f70333,f82364]) ).
fof(f94215,plain,
( m1_subset_1(sF4877,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sF4876,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sK4872,k1_pcomps_1(sF4873)) ),
inference(superposition,[],[f70333,f82370]) ).
fof(f94217,plain,
( m1_subset_1(sF4877,sF4882)
| ~ m1_subset_1(sF4876,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sK4872,k1_pcomps_1(sF4873)) ),
inference(forward_demodulation,[],[f94215,f82381]) ).
fof(f94218,plain,
( m1_subset_1(sF4874,sF4882)
| ~ m1_subset_1(sK4871,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sK4872,k1_pcomps_1(sF4873)) ),
inference(forward_demodulation,[],[f94214,f82381]) ).
fof(f94219,plain,
( m1_subset_1(sF4880,sF4882)
| ~ m1_subset_1(sK4871,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sF4879,k1_pcomps_1(sF4873)) ),
inference(forward_demodulation,[],[f94213,f82381]) ).
fof(f94221,plain,
( ~ m1_subset_1(sF4876,sF4882)
| m1_subset_1(sF4877,sF4882)
| ~ m1_subset_1(sK4872,k1_pcomps_1(sF4873)) ),
inference(forward_demodulation,[],[f94217,f82381]) ).
fof(f94222,plain,
( ~ m1_subset_1(sK4871,sF4882)
| m1_subset_1(sF4874,sF4882)
| ~ m1_subset_1(sK4872,k1_pcomps_1(sF4873)) ),
inference(forward_demodulation,[],[f94218,f82381]) ).
fof(f94223,plain,
( ~ m1_subset_1(sK4871,sF4882)
| m1_subset_1(sF4880,sF4882)
| ~ m1_subset_1(sF4879,k1_pcomps_1(sF4873)) ),
inference(forward_demodulation,[],[f94219,f82381]) ).
fof(f94224,plain,
( ~ m1_subset_1(sK4872,sF4882)
| ~ m1_subset_1(sF4876,sF4882)
| m1_subset_1(sF4877,sF4882) ),
inference(forward_demodulation,[],[f94221,f82381]) ).
fof(f94225,plain,
( m1_subset_1(sF4874,sF4882)
| ~ m1_subset_1(sK4872,k1_pcomps_1(sF4873)) ),
inference(forward_subsumption_resolution,[],[f94222,f82383]) ).
fof(f94226,plain,
( m1_subset_1(sF4880,sF4882)
| ~ m1_subset_1(sF4879,k1_pcomps_1(sF4873)) ),
inference(forward_subsumption_resolution,[],[f94223,f82383]) ).
fof(f94227,plain,
( ~ m1_subset_1(sF4876,sF4882)
| m1_subset_1(sF4877,sF4882) ),
inference(forward_subsumption_resolution,[],[f94224,f82382]) ).
fof(f94228,plain,
( ~ m1_subset_1(sK4872,sF4882)
| m1_subset_1(sF4874,sF4882) ),
inference(forward_demodulation,[],[f94225,f82381]) ).
fof(f94229,plain,
( ~ m1_subset_1(sF4879,sF4882)
| m1_subset_1(sF4880,sF4882) ),
inference(forward_demodulation,[],[f94226,f82381]) ).
fof(f94231,definition,
( spl4883_1163
<=> m1_subset_1(sF4877,sF4882) ),
introduced(definition,[new_symbols(definition,[spl4883_1163])],[avatar_definition]) ).
fof(f94233,plain,
( m1_subset_1(sF4877,sF4882)
| ~ spl4883_1163 ),
inference(avatar_component_clause,[],[f94231]) ).
fof(f94235,definition,
( spl4883_1164
<=> m1_subset_1(sF4876,sF4882) ),
introduced(definition,[new_symbols(definition,[spl4883_1164])],[avatar_definition]) ).
fof(f94236,plain,
( m1_subset_1(sF4876,sF4882)
| ~ spl4883_1164 ),
inference(avatar_component_clause,[],[f94235]) ).
fof(f94237,plain,
( ~ m1_subset_1(sF4876,sF4882)
| spl4883_1164 ),
inference(avatar_component_clause,[],[f94235]) ).
fof(f94238,plain,
( spl4883_1163
| ~ spl4883_1164 ),
inference(avatar_split_clause,[],[f94227,f94235,f94231]) ).
fof(f94239,plain,
m1_subset_1(sF4874,sF4882),
inference(forward_subsumption_resolution,[],[f94228,f82382]) ).
fof(f94241,definition,
( spl4883_1165
<=> m1_subset_1(sF4880,sF4882) ),
introduced(definition,[new_symbols(definition,[spl4883_1165])],[avatar_definition]) ).
fof(f94243,plain,
( m1_subset_1(sF4880,sF4882)
| ~ spl4883_1165 ),
inference(avatar_component_clause,[],[f94241]) ).
fof(f94245,definition,
( spl4883_1166
<=> m1_subset_1(sF4879,sF4882) ),
introduced(definition,[new_symbols(definition,[spl4883_1166])],[avatar_definition]) ).
fof(f94246,plain,
( m1_subset_1(sF4879,sF4882)
| ~ spl4883_1166 ),
inference(avatar_component_clause,[],[f94245]) ).
fof(f94247,plain,
( ~ m1_subset_1(sF4879,sF4882)
| spl4883_1166 ),
inference(avatar_component_clause,[],[f94245]) ).
fof(f94248,plain,
( spl4883_1165
| ~ spl4883_1166 ),
inference(avatar_split_clause,[],[f94229,f94245,f94241]) ).
fof(f94250,plain,
! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k3_tarski(k2_tarski(sK4872,X0)) = k4_subset_1(sF4873,sK4872,X0) ),
inference(resolution,[],[f94208,f82382]) ).
fof(f94257,plain,
k3_tarski(k2_tarski(sK4872,sK4871)) = k4_subset_1(sF4873,sK4872,sK4871),
inference(resolution,[],[f94250,f82383]) ).
fof(f94262,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF4882)
| ~ m1_subset_1(X0,sF4882)
| k4_subset_1(sF4873,X1,X0) = k4_subset_1(sF4873,X0,X1) ),
inference(superposition,[],[f70334,f82381]) ).
fof(f94269,plain,
( m1_subset_1(k3_tarski(k2_tarski(sK4872,sK4871)),k1_pcomps_1(sF4873))
| ~ m1_subset_1(sK4872,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sK4871,k1_pcomps_1(sF4873)) ),
inference(superposition,[],[f70333,f94257]) ).
fof(f94270,plain,
( m1_subset_1(k3_tarski(k2_tarski(sK4872,sK4871)),sF4882)
| ~ m1_subset_1(sK4872,k1_pcomps_1(sF4873))
| ~ m1_subset_1(sK4871,k1_pcomps_1(sF4873)) ),
inference(forward_demodulation,[],[f94269,f82381]) ).
fof(f94271,plain,
( ~ m1_subset_1(sK4872,sF4882)
| m1_subset_1(k3_tarski(k2_tarski(sK4872,sK4871)),sF4882)
| ~ m1_subset_1(sK4871,k1_pcomps_1(sF4873)) ),
inference(forward_demodulation,[],[f94270,f82381]) ).
fof(f94272,plain,
( m1_subset_1(k3_tarski(k2_tarski(sK4872,sK4871)),sF4882)
| ~ m1_subset_1(sK4871,k1_pcomps_1(sF4873)) ),
inference(forward_subsumption_resolution,[],[f94271,f82382]) ).
fof(f94273,plain,
( ~ m1_subset_1(sK4871,sF4882)
| m1_subset_1(k3_tarski(k2_tarski(sK4872,sK4871)),sF4882) ),
inference(forward_demodulation,[],[f94272,f82381]) ).
fof(f94274,plain,
m1_subset_1(k3_tarski(k2_tarski(sK4872,sK4871)),sF4882),
inference(forward_subsumption_resolution,[],[f94273,f82383]) ).
fof(f94281,plain,
! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k4_subset_1(sF4873,sK4871,X0) = k4_subset_1(sF4873,X0,sK4871) ),
inference(resolution,[],[f94262,f82383]) ).
fof(f94282,plain,
! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k4_subset_1(sF4873,sK4872,X0) = k4_subset_1(sF4873,X0,sK4872) ),
inference(resolution,[],[f94262,f82382]) ).
fof(f94285,plain,
k4_subset_1(sF4873,sK4871,sK4872) = k4_subset_1(sF4873,sK4872,sK4871),
inference(resolution,[],[f94281,f82382]) ).
fof(f94288,plain,
k4_subset_1(sF4873,sK4871,sK4872) = k3_tarski(k2_tarski(sK4872,sK4871)),
inference(forward_demodulation,[],[f94285,f94257]) ).
fof(f94289,plain,
sF4874 = k3_tarski(k2_tarski(sK4872,sK4871)),
inference(forward_demodulation,[],[f94288,f82364]) ).
fof(f94313,plain,
! [X0] :
( m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ m2_lattice4(X0,sK4870)
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(superposition,[],[f78642,f82362]) ).
fof(f94319,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| k7_filter_2(sK4870,X0) = X0
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(superposition,[],[f79707,f82362]) ).
fof(f94322,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_pcomps_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_pcomps_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f79719,f79718]) ).
fof(f94323,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_pcomps_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(duplicate_literal_removal,[],[f94322]) ).
fof(f94324,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| ~ m1_subset_1(X0,k1_pcomps_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f94323,f69552]) ).
fof(f94332,plain,
( m2_filter_2(sF4873,sK4870)
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(superposition,[],[f69688,f82362]) ).
fof(f94456,plain,
( v3_struct_0(sK4870)
| sP387(sK4870)
| ~ l3_lattices(sK4870) ),
inference(resolution,[],[f59225,f69760]) ).
fof(f94457,plain,
( sP387(sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f94456,f69761]) ).
fof(f94458,plain,
sP387(sK4870),
inference(forward_subsumption_resolution,[],[f94457,f69759]) ).
fof(f94513,plain,
! [X0,X1] :
( r1_filter_2(X1,X0,X0)
| v1_xboole_0(X1)
| ~ r1_tarski(X0,X1) ),
inference(resolution,[],[f70421,f82387]) ).
fof(f94517,plain,
! [X0] :
( ~ r1_tarski(X0,sF4873)
| m1_subset_1(X0,sF4882) ),
inference(superposition,[],[f70421,f82381]) ).
fof(f94540,plain,
( v3_struct_0(sK4870)
| u1_struct_0(sK4870) = u1_struct_0(k1_lattice2(sK4870)) ),
inference(resolution,[],[f59342,f69759]) ).
fof(f94542,plain,
u1_struct_0(sK4870) = u1_struct_0(k1_lattice2(sK4870)),
inference(forward_subsumption_resolution,[],[f94540,f69761]) ).
fof(f94543,plain,
sF4873 = u1_struct_0(k1_lattice2(sK4870)),
inference(forward_demodulation,[],[f94542,f82362]) ).
fof(f94544,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v1_xboole_0(X0)
| k19_filter_2(sK4870,X1) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(sK4870)))
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(superposition,[],[f79725,f94543]) ).
fof(f94553,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v3_struct_0(k1_lattice2(sK4870))
| ~ v10_lattices(k1_lattice2(sK4870))
| ~ l3_lattices(k1_lattice2(sK4870))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),X0) = k3_filter_2(k1_lattice2(sK4870),X0) ),
inference(superposition,[],[f79672,f94543]) ).
fof(f94565,definition,
( spl4883_1168
<=> v3_struct_0(k1_lattice2(sK4870)) ),
introduced(definition,[new_symbols(definition,[spl4883_1168])],[avatar_definition]) ).
fof(f94566,plain,
( ~ v3_struct_0(k1_lattice2(sK4870))
| spl4883_1168 ),
inference(avatar_component_clause,[],[f94565]) ).
fof(f94567,plain,
( v3_struct_0(k1_lattice2(sK4870))
| ~ spl4883_1168 ),
inference(avatar_component_clause,[],[f94565]) ).
fof(f94633,plain,
! [X0] :
( ~ m1_subset_1(X0,sF4882)
| r1_tarski(X0,sF4873) ),
inference(superposition,[],[f70422,f82381]) ).
fof(f94741,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ r1_tarski(X1,X0)
| v1_xboole_0(X0)
| r1_tarski(k19_filter_2(sK4870,X1),k19_filter_2(sK4870,X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(sF4873))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_pcomps_1(sF4873))
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(superposition,[],[f79729,f82362]) ).
fof(f94830,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,X1,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,k3_filter_0(k1_lattice2(sK4870),X1),X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(sF4873))
| v3_struct_0(k1_lattice2(sK4870))
| ~ v10_lattices(k1_lattice2(sK4870))
| ~ l3_lattices(k1_lattice2(sK4870)) ),
inference(superposition,[],[f76569,f94543]) ).
fof(f94886,definition,
( spl4883_1169
<=> m1_subset_1(sF4873,sF4882) ),
introduced(definition,[new_symbols(definition,[spl4883_1169])],[avatar_definition]) ).
fof(f94887,plain,
( m1_subset_1(sF4873,sF4882)
| ~ spl4883_1169 ),
inference(avatar_component_clause,[],[f94886]) ).
fof(f94888,plain,
( ~ m1_subset_1(sF4873,sF4882)
| spl4883_1169 ),
inference(avatar_component_clause,[],[f94886]) ).
fof(f95071,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF4882)
| ~ m1_subset_1(X0,sF4882)
| k5_subset_1(sF4873,X0,X1) = k5_subset_1(sF4873,X1,X0) ),
inference(superposition,[],[f70338,f82381]) ).
fof(f95075,plain,
! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k5_subset_1(sF4873,X0,sK4872) = k5_subset_1(sF4873,sK4872,X0) ),
inference(resolution,[],[f95071,f82382]) ).
fof(f95090,plain,
k5_subset_1(sF4873,sF4874,sK4872) = k5_subset_1(sF4873,sK4872,sF4874),
inference(resolution,[],[f95075,f94239]) ).
fof(f95094,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ v1_xboole_0(X0) ),
inference(resolution,[],[f41403,f41279]) ).
fof(f95189,plain,
m1_subset_1(sF4873,sF4882),
inference(resolution,[],[f94517,f79778]) ).
fof(f95193,plain,
( $false
| spl4883_1169 ),
inference(forward_subsumption_resolution,[],[f95189,f94888]) ).
fof(f95194,plain,
spl4883_1169,
inference(avatar_contradiction_clause,[],[f95193]) ).
fof(f95282,plain,
! [X0] :
( m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ m2_lattice4(X0,sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f94313,f69761]) ).
fof(f95285,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| k7_filter_2(sK4870,X0) = X0
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f94319,f69761]) ).
fof(f95287,plain,
( m2_filter_2(sF4873,sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f94332,f69761]) ).
fof(f95303,definition,
( spl4883_1184
<=> l3_lattices(k1_lattice2(sK4870)) ),
introduced(definition,[new_symbols(definition,[spl4883_1184])],[avatar_definition]) ).
fof(f95304,plain,
( l3_lattices(k1_lattice2(sK4870))
| ~ spl4883_1184 ),
inference(avatar_component_clause,[],[f95303]) ).
fof(f95305,plain,
( ~ l3_lattices(k1_lattice2(sK4870))
| spl4883_1184 ),
inference(avatar_component_clause,[],[f95303]) ).
fof(f95307,definition,
( spl4883_1185
<=> v10_lattices(k1_lattice2(sK4870)) ),
introduced(definition,[new_symbols(definition,[spl4883_1185])],[avatar_definition]) ).
fof(f95308,plain,
( v10_lattices(k1_lattice2(sK4870))
| ~ spl4883_1185 ),
inference(avatar_component_clause,[],[f95307]) ).
fof(f95309,plain,
( ~ v10_lattices(k1_lattice2(sK4870))
| spl4883_1185 ),
inference(avatar_component_clause,[],[f95307]) ).
fof(f95416,plain,
! [X0] :
( m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ m2_lattice4(X0,sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f95282,f69760]) ).
fof(f95418,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| k7_filter_2(sK4870,X0) = X0
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f95285,f69760]) ).
fof(f95419,plain,
( m2_filter_2(sF4873,sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f95287,f69760]) ).
fof(f95482,plain,
! [X0] :
( m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ m2_lattice4(X0,sK4870) ),
inference(forward_subsumption_resolution,[],[f95416,f69759]) ).
fof(f95484,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| k7_filter_2(sK4870,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f95418,f69759]) ).
fof(f95485,plain,
m2_filter_2(sF4873,sK4870),
inference(forward_subsumption_resolution,[],[f95419,f69759]) ).
fof(f95536,plain,
! [X0] :
( ~ m2_lattice4(X0,sK4870)
| m1_subset_1(X0,sF4882) ),
inference(forward_demodulation,[],[f95482,f82381]) ).
fof(f95537,plain,
! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k7_filter_2(sK4870,X0) = X0 ),
inference(forward_demodulation,[],[f95484,f82381]) ).
fof(f95689,plain,
( ~ m2_filter_2(sF4876,sK4870)
| r1_tarski(sK4871,sF4876)
| ~ m1_subset_1(sK4871,k1_pcomps_1(u1_struct_0(sK4870)))
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f94196,f69763]) ).
fof(f95691,definition,
( spl4883_1230
<=> v1_xboole_0(sF4873) ),
introduced(definition,[new_symbols(definition,[spl4883_1230])],[avatar_definition]) ).
fof(f95692,plain,
( ~ v1_xboole_0(sF4873)
| spl4883_1230 ),
inference(avatar_component_clause,[],[f95691]) ).
fof(f95693,plain,
( v1_xboole_0(sF4873)
| ~ spl4883_1230 ),
inference(avatar_component_clause,[],[f95691]) ).
fof(f95850,definition,
( spl4883_1256
<=> v1_xboole_0(sF4874) ),
introduced(definition,[new_symbols(definition,[spl4883_1256])],[avatar_definition]) ).
fof(f95851,plain,
( ~ v1_xboole_0(sF4874)
| spl4883_1256 ),
inference(avatar_component_clause,[],[f95850]) ).
fof(f95852,plain,
( v1_xboole_0(sF4874)
| ~ spl4883_1256 ),
inference(avatar_component_clause,[],[f95850]) ).
fof(f95894,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870)
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK4870,X0),sK4870) ),
inference(forward_subsumption_resolution,[],[f94195,f69761]) ).
fof(f95896,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(u1_struct_0(X1)))
| ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f94324,f79778]) ).
fof(f95900,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v1_xboole_0(X0)
| k19_filter_2(sK4870,X1) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(sK4870)))
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f94544,f69761]) ).
fof(f95906,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ r1_tarski(X1,X0)
| v1_xboole_0(X0)
| r1_tarski(k19_filter_2(sK4870,X1),k19_filter_2(sK4870,X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(sF4873))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_pcomps_1(sF4873))
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f94741,f69761]) ).
fof(f95941,plain,
( ~ m2_filter_2(sF4876,sK4870)
| r1_tarski(sK4871,sF4876)
| ~ m1_subset_1(sK4871,k1_pcomps_1(u1_struct_0(sK4870)))
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f95689,f69761]) ).
fof(f95992,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ l3_lattices(sK4870)
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK4870,X0),sK4870) ),
inference(forward_subsumption_resolution,[],[f95894,f69760]) ).
fof(f95995,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v1_xboole_0(X0)
| k19_filter_2(sK4870,X1) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(sK4870)))
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f95900,f69760]) ).
fof(f95998,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ r1_tarski(X1,X0)
| v1_xboole_0(X0)
| r1_tarski(k19_filter_2(sK4870,X1),k19_filter_2(sK4870,X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(sF4873))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_pcomps_1(sF4873))
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f95906,f69760]) ).
fof(f96014,plain,
( ~ m2_filter_2(sF4876,sK4870)
| r1_tarski(sK4871,sF4876)
| ~ m1_subset_1(sK4871,k1_pcomps_1(u1_struct_0(sK4870)))
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f95941,f69760]) ).
fof(f96046,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK4870,X0),sK4870) ),
inference(forward_subsumption_resolution,[],[f95992,f69759]) ).
fof(f96049,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v1_xboole_0(X0)
| k19_filter_2(sK4870,X1) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(sK4870))) ),
inference(forward_subsumption_resolution,[],[f95995,f69759]) ).
fof(f96052,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ r1_tarski(X1,X0)
| v1_xboole_0(X0)
| r1_tarski(k19_filter_2(sK4870,X1),k19_filter_2(sK4870,X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(sF4873))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_pcomps_1(sF4873)) ),
inference(forward_subsumption_resolution,[],[f95998,f69759]) ).
fof(f96067,plain,
( ~ m2_filter_2(sF4876,sK4870)
| r1_tarski(sK4871,sF4876)
| ~ m1_subset_1(sK4871,k1_pcomps_1(u1_struct_0(sK4870))) ),
inference(forward_subsumption_resolution,[],[f96014,f69759]) ).
fof(f96089,plain,
! [X0] :
( m2_filter_2(k19_filter_2(sK4870,X0),sK4870)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF4882) ),
inference(forward_demodulation,[],[f96046,f82381]) ).
fof(f96092,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0)
| k19_filter_2(sK4870,X1) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(u1_struct_0(sK4870))) ),
inference(forward_demodulation,[],[f96049,f82381]) ).
fof(f96095,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF4882)
| ~ r1_tarski(X1,X0)
| v1_xboole_0(X0)
| r1_tarski(k19_filter_2(sK4870,X1),k19_filter_2(sK4870,X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(sF4873))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_pcomps_1(sF4873)) ),
inference(forward_demodulation,[],[f96052,f82381]) ).
fof(f96105,plain,
( ~ m1_subset_1(sK4871,k1_pcomps_1(sF4873))
| ~ m2_filter_2(sF4876,sK4870)
| r1_tarski(sK4871,sF4876) ),
inference(forward_demodulation,[],[f96067,f82362]) ).
fof(f96124,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_pcomps_1(sF4873))
| ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0)
| k19_filter_2(sK4870,X1) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,X1))
| v1_xboole_0(X1) ),
inference(forward_demodulation,[],[f96092,f82362]) ).
fof(f96126,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,sF4882)
| ~ m1_subset_1(X0,sF4882)
| ~ r1_tarski(X1,X0)
| v1_xboole_0(X0)
| r1_tarski(k19_filter_2(sK4870,X1),k19_filter_2(sK4870,X0))
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_pcomps_1(sF4873)) ),
inference(forward_demodulation,[],[f96095,f82381]) ).
fof(f96136,plain,
( ~ m1_subset_1(sK4871,sF4882)
| ~ m2_filter_2(sF4876,sK4870)
| r1_tarski(sK4871,sF4876) ),
inference(forward_demodulation,[],[f96105,f82381]) ).
fof(f96138,definition,
( spl4883_1263
<=> v1_xboole_0(sF4880) ),
introduced(definition,[new_symbols(definition,[spl4883_1263])],[avatar_definition]) ).
fof(f96139,plain,
( ~ v1_xboole_0(sF4880)
| spl4883_1263 ),
inference(avatar_component_clause,[],[f96138]) ).
fof(f96140,plain,
( v1_xboole_0(sF4880)
| ~ spl4883_1263 ),
inference(avatar_component_clause,[],[f96138]) ).
fof(f96150,definition,
( spl4883_1266
<=> v1_xboole_0(sF4877) ),
introduced(definition,[new_symbols(definition,[spl4883_1266])],[avatar_definition]) ).
fof(f96151,plain,
( ~ v1_xboole_0(sF4877)
| spl4883_1266 ),
inference(avatar_component_clause,[],[f96150]) ).
fof(f96152,plain,
( v1_xboole_0(sF4877)
| ~ spl4883_1266 ),
inference(avatar_component_clause,[],[f96150]) ).
fof(f96175,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF4882)
| ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0)
| k19_filter_2(sK4870,X1) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,X1))
| v1_xboole_0(X1) ),
inference(forward_demodulation,[],[f96124,f82381]) ).
fof(f96177,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,sF4882)
| ~ m1_subset_1(X1,sF4882)
| ~ m1_subset_1(X0,sF4882)
| ~ r1_tarski(X1,X0)
| v1_xboole_0(X0)
| r1_tarski(k19_filter_2(sK4870,X1),k19_filter_2(sK4870,X0))
| v1_xboole_0(X1)
| v1_xboole_0(X2) ),
inference(forward_demodulation,[],[f96126,f82381]) ).
fof(f96192,plain,
( ~ m2_filter_2(sF4876,sK4870)
| r1_tarski(sK4871,sF4876) ),
inference(forward_subsumption_resolution,[],[f96136,f82383]) ).
fof(f96215,definition,
( spl4883_1273
<=> ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4883_1273])],[avatar_definition]) ).
fof(f96216,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0) )
| ~ spl4883_1273 ),
inference(avatar_component_clause,[],[f96215]) ).
fof(f96218,definition,
( spl4883_1274
<=> ! [X1] :
( ~ m1_subset_1(X1,sF4882)
| v1_xboole_0(X1)
| k19_filter_2(sK4870,X1) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl4883_1274])],[avatar_definition]) ).
fof(f96219,plain,
( ! [X1] :
( ~ m1_subset_1(X1,sF4882)
| v1_xboole_0(X1)
| k19_filter_2(sK4870,X1) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,X1)) )
| ~ spl4883_1274 ),
inference(avatar_component_clause,[],[f96218]) ).
fof(f96220,plain,
( spl4883_1273
| spl4883_1274 ),
inference(avatar_split_clause,[],[f96175,f96218,f96215]) ).
fof(f96226,definition,
( spl4883_1276
<=> ! [X0,X1] :
( ~ m1_subset_1(X1,sF4882)
| v1_xboole_0(X1)
| r1_tarski(k19_filter_2(sK4870,X1),k19_filter_2(sK4870,X0))
| v1_xboole_0(X0)
| ~ r1_tarski(X1,X0)
| ~ m1_subset_1(X0,sF4882) ) ),
introduced(definition,[new_symbols(definition,[spl4883_1276])],[avatar_definition]) ).
fof(f96227,plain,
( ! [X0,X1] :
( r1_tarski(k19_filter_2(sK4870,X1),k19_filter_2(sK4870,X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,sF4882)
| v1_xboole_0(X0)
| ~ r1_tarski(X1,X0)
| ~ m1_subset_1(X0,sF4882) )
| ~ spl4883_1276 ),
inference(avatar_component_clause,[],[f96226]) ).
fof(f96228,plain,
( spl4883_1276
| spl4883_1273 ),
inference(avatar_split_clause,[],[f96177,f96215,f96226]) ).
fof(f96243,definition,
( spl4883_1280
<=> m2_filter_2(sF4879,sK4870) ),
introduced(definition,[new_symbols(definition,[spl4883_1280])],[avatar_definition]) ).
fof(f96244,plain,
( m2_filter_2(sF4879,sK4870)
| ~ spl4883_1280 ),
inference(avatar_component_clause,[],[f96243]) ).
fof(f96245,plain,
( ~ m2_filter_2(sF4879,sK4870)
| spl4883_1280 ),
inference(avatar_component_clause,[],[f96243]) ).
fof(f96248,definition,
( spl4883_1281
<=> r1_tarski(sK4871,sF4876) ),
introduced(definition,[new_symbols(definition,[spl4883_1281])],[avatar_definition]) ).
fof(f96250,plain,
( r1_tarski(sK4871,sF4876)
| ~ spl4883_1281 ),
inference(avatar_component_clause,[],[f96248]) ).
fof(f96252,definition,
( spl4883_1282
<=> m2_filter_2(sF4876,sK4870) ),
introduced(definition,[new_symbols(definition,[spl4883_1282])],[avatar_definition]) ).
fof(f96253,plain,
( m2_filter_2(sF4876,sK4870)
| ~ spl4883_1282 ),
inference(avatar_component_clause,[],[f96252]) ).
fof(f96254,plain,
( ~ m2_filter_2(sF4876,sK4870)
| spl4883_1282 ),
inference(avatar_component_clause,[],[f96252]) ).
fof(f96255,plain,
( spl4883_1281
| ~ spl4883_1282 ),
inference(avatar_split_clause,[],[f96192,f96252,f96248]) ).
fof(f96311,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ m2_filter_2(X0,sK4870)
| k19_filter_2(sK4870,X0) = X0
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(superposition,[],[f95896,f82362]) ).
fof(f96318,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ m2_filter_2(X0,sK4870)
| k19_filter_2(sK4870,X0) = X0
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f96311,f69761]) ).
fof(f96323,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ m2_filter_2(X0,sK4870)
| k19_filter_2(sK4870,X0) = X0
| ~ l3_lattices(sK4870) ),
inference(forward_subsumption_resolution,[],[f96318,f69760]) ).
fof(f96325,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ m2_filter_2(X0,sK4870)
| k19_filter_2(sK4870,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f96323,f69759]) ).
fof(f96326,plain,
! [X0] :
( ~ m2_filter_2(X0,sK4870)
| ~ m1_subset_1(X0,sF4882)
| k19_filter_2(sK4870,X0) = X0 ),
inference(forward_demodulation,[],[f96325,f82381]) ).
fof(f96329,plain,
sK4871 = k7_filter_2(sK4870,sK4871),
inference(resolution,[],[f95537,f82383]) ).
fof(f96330,plain,
sK4872 = k7_filter_2(sK4870,sK4872),
inference(resolution,[],[f95537,f82382]) ).
fof(f96332,plain,
sF4874 = k7_filter_2(sK4870,sF4874),
inference(resolution,[],[f95537,f94239]) ).
fof(f96340,plain,
( m2_filter_2(sF4876,sK4870)
| v1_xboole_0(sK4871)
| ~ m1_subset_1(sK4871,sF4882) ),
inference(superposition,[],[f96089,f82368]) ).
fof(f96341,plain,
( m2_filter_2(sF4879,sK4870)
| v1_xboole_0(sK4872)
| ~ m1_subset_1(sK4872,sF4882) ),
inference(superposition,[],[f96089,f82374]) ).
fof(f96352,plain,
( ~ v1_xboole_0(sF4873)
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870) ),
inference(resolution,[],[f95485,f69552]) ).
fof(f96353,plain,
( v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1230 ),
inference(forward_subsumption_resolution,[],[f96352,f95693]) ).
fof(f96355,plain,
( ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1230 ),
inference(forward_subsumption_resolution,[],[f96353,f69761]) ).
fof(f96357,plain,
( ~ l3_lattices(sK4870)
| ~ spl4883_1230 ),
inference(forward_subsumption_resolution,[],[f96355,f69760]) ).
fof(f96359,plain,
( $false
| ~ spl4883_1230 ),
inference(forward_subsumption_resolution,[],[f96357,f69759]) ).
fof(f96360,plain,
~ spl4883_1230,
inference(avatar_contradiction_clause,[],[f96359]) ).
fof(f96380,plain,
( v1_xboole_0(sK4871)
| ~ spl4883_1273 ),
inference(resolution,[],[f96216,f82383]) ).
fof(f96390,plain,
( $false
| ~ spl4883_1273 ),
inference(forward_subsumption_resolution,[],[f96380,f69763]) ).
fof(f96391,plain,
~ spl4883_1273,
inference(avatar_contradiction_clause,[],[f96390]) ).
fof(f96394,plain,
( v1_xboole_0(sK4872)
| ~ m1_subset_1(sK4872,sF4882)
| spl4883_1280 ),
inference(forward_subsumption_resolution,[],[f96341,f96245]) ).
fof(f96395,plain,
( v1_xboole_0(sK4871)
| ~ m1_subset_1(sK4871,sF4882)
| spl4883_1282 ),
inference(forward_subsumption_resolution,[],[f96340,f96254]) ).
fof(f96403,plain,
( ~ m1_subset_1(sK4872,sF4882)
| spl4883_1280 ),
inference(forward_subsumption_resolution,[],[f96394,f69765]) ).
fof(f96404,plain,
( ~ m1_subset_1(sK4871,sF4882)
| spl4883_1282 ),
inference(forward_subsumption_resolution,[],[f96395,f69763]) ).
fof(f96412,plain,
( $false
| spl4883_1280 ),
inference(forward_subsumption_resolution,[],[f96403,f82382]) ).
fof(f96413,plain,
spl4883_1280,
inference(avatar_contradiction_clause,[],[f96412]) ).
fof(f96414,plain,
( $false
| spl4883_1282 ),
inference(forward_subsumption_resolution,[],[f96404,f82383]) ).
fof(f96415,plain,
spl4883_1282,
inference(avatar_contradiction_clause,[],[f96414]) ).
fof(f96458,plain,
( m2_lattice4(sF4879,sK4870)
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1280 ),
inference(resolution,[],[f96244,f69551]) ).
fof(f96461,plain,
( m2_lattice4(sF4879,sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1280 ),
inference(forward_subsumption_resolution,[],[f96458,f69761]) ).
fof(f96463,plain,
( m2_lattice4(sF4879,sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1280 ),
inference(forward_subsumption_resolution,[],[f96461,f69760]) ).
fof(f96465,plain,
( m2_lattice4(sF4879,sK4870)
| ~ spl4883_1280 ),
inference(forward_subsumption_resolution,[],[f96463,f69759]) ).
fof(f96466,plain,
( m2_lattice4(sF4876,sK4870)
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1282 ),
inference(resolution,[],[f96253,f69551]) ).
fof(f96467,plain,
( ~ v1_xboole_0(sF4876)
| v3_struct_0(sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1282 ),
inference(resolution,[],[f96253,f69552]) ).
fof(f96468,plain,
( ~ v1_xboole_0(sF4876)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1282 ),
inference(forward_subsumption_resolution,[],[f96467,f69761]) ).
fof(f96469,plain,
( m2_lattice4(sF4876,sK4870)
| ~ v10_lattices(sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1282 ),
inference(forward_subsumption_resolution,[],[f96466,f69761]) ).
fof(f96470,plain,
( ~ v1_xboole_0(sF4876)
| ~ l3_lattices(sK4870)
| ~ spl4883_1282 ),
inference(forward_subsumption_resolution,[],[f96468,f69760]) ).
fof(f96471,plain,
( m2_lattice4(sF4876,sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1282 ),
inference(forward_subsumption_resolution,[],[f96469,f69760]) ).
fof(f96472,plain,
( ~ v1_xboole_0(sF4876)
| ~ spl4883_1282 ),
inference(forward_subsumption_resolution,[],[f96470,f69759]) ).
fof(f96473,plain,
( m2_lattice4(sF4876,sK4870)
| ~ spl4883_1282 ),
inference(forward_subsumption_resolution,[],[f96471,f69759]) ).
fof(f96476,plain,
( v1_xboole_0(sK4871)
| k19_filter_2(sK4870,sK4871) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,sK4871))
| ~ spl4883_1274 ),
inference(resolution,[],[f96219,f82383]) ).
fof(f96477,plain,
( v1_xboole_0(sK4872)
| k19_filter_2(sK4870,sK4872) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,sK4872))
| ~ spl4883_1274 ),
inference(resolution,[],[f96219,f82382]) ).
fof(f96479,plain,
( v1_xboole_0(sF4874)
| k19_filter_2(sK4870,sF4874) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,sF4874))
| ~ spl4883_1274 ),
inference(resolution,[],[f96219,f94239]) ).
fof(f96483,plain,
( k19_filter_2(sK4870,sK4872) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,sK4872))
| ~ spl4883_1274 ),
inference(forward_subsumption_resolution,[],[f96477,f69765]) ).
fof(f96484,plain,
( k19_filter_2(sK4870,sK4871) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,sK4871))
| ~ spl4883_1274 ),
inference(forward_subsumption_resolution,[],[f96476,f69763]) ).
fof(f96487,plain,
( k19_filter_2(sK4870,sK4872) = k3_filter_2(k1_lattice2(sK4870),sK4872)
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f96483,f96330]) ).
fof(f96488,plain,
( k19_filter_2(sK4870,sK4871) = k3_filter_2(k1_lattice2(sK4870),sK4871)
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f96484,f96329]) ).
fof(f96489,plain,
( sF4879 = k3_filter_2(k1_lattice2(sK4870),sK4872)
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f96487,f82374]) ).
fof(f96490,plain,
( sF4876 = k3_filter_2(k1_lattice2(sK4870),sK4871)
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f96488,f82368]) ).
fof(f96500,definition,
( spl4883_1292
<=> r1_tarski(sK4872,sF4876) ),
introduced(definition,[new_symbols(definition,[spl4883_1292])],[avatar_definition]) ).
fof(f96501,plain,
( r1_tarski(sK4872,sF4876)
| ~ spl4883_1292 ),
inference(avatar_component_clause,[],[f96500]) ).
fof(f96502,plain,
( ~ r1_tarski(sK4872,sF4876)
| spl4883_1292 ),
inference(avatar_component_clause,[],[f96500]) ).
fof(f96550,plain,
( ~ m1_subset_1(sF4873,sF4882)
| sF4873 = k19_filter_2(sK4870,sF4873) ),
inference(resolution,[],[f96326,f95485]) ).
fof(f96557,plain,
( sF4873 = k19_filter_2(sK4870,sF4873)
| ~ spl4883_1169 ),
inference(forward_subsumption_resolution,[],[f96550,f94887]) ).
fof(f96614,plain,
( m1_subset_1(sF4876,sF4882)
| ~ spl4883_1282 ),
inference(resolution,[],[f96473,f95536]) ).
fof(f96617,plain,
( $false
| spl4883_1164
| ~ spl4883_1282 ),
inference(forward_subsumption_resolution,[],[f96614,f94237]) ).
fof(f96618,plain,
( spl4883_1164
| ~ spl4883_1282 ),
inference(avatar_contradiction_clause,[],[f96617]) ).
fof(f96635,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k3_tarski(k2_tarski(sF4876,X0)) = k4_subset_1(sF4873,sF4876,X0) )
| ~ spl4883_1164 ),
inference(resolution,[],[f94236,f94208]) ).
fof(f96637,plain,
( k3_tarski(k2_tarski(sK4872,sF4876)) = k4_subset_1(sF4873,sK4872,sF4876)
| ~ spl4883_1164 ),
inference(resolution,[],[f94236,f94250]) ).
fof(f96641,plain,
( k4_subset_1(sF4873,sF4876,sK4872) = k4_subset_1(sF4873,sK4872,sF4876)
| ~ spl4883_1164 ),
inference(resolution,[],[f94236,f94282]) ).
fof(f96665,plain,
( sF4877 = k4_subset_1(sF4873,sK4872,sF4876)
| ~ spl4883_1164 ),
inference(forward_demodulation,[],[f96641,f82370]) ).
fof(f96668,plain,
( sF4877 = k3_tarski(k2_tarski(sK4872,sF4876))
| ~ spl4883_1164 ),
inference(forward_demodulation,[],[f96665,f96637]) ).
fof(f96690,plain,
( sF4877 = k7_filter_2(sK4870,sF4877)
| ~ spl4883_1163 ),
inference(resolution,[],[f94233,f95537]) ).
fof(f96692,plain,
( v1_xboole_0(sF4877)
| k19_filter_2(sK4870,sF4877) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,sF4877))
| ~ spl4883_1163
| ~ spl4883_1274 ),
inference(resolution,[],[f94233,f96219]) ).
fof(f96698,plain,
( m1_subset_1(sF4879,sF4882)
| ~ spl4883_1280 ),
inference(resolution,[],[f96465,f95536]) ).
fof(f96701,plain,
( $false
| spl4883_1166
| ~ spl4883_1280 ),
inference(forward_subsumption_resolution,[],[f96698,f94247]) ).
fof(f96702,plain,
( spl4883_1166
| ~ spl4883_1280 ),
inference(avatar_contradiction_clause,[],[f96701]) ).
fof(f96719,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k3_tarski(k2_tarski(sF4879,X0)) = k4_subset_1(sF4873,sF4879,X0) )
| ~ spl4883_1166 ),
inference(resolution,[],[f94246,f94208]) ).
fof(f96724,plain,
( k4_subset_1(sF4873,sK4871,sF4879) = k4_subset_1(sF4873,sF4879,sK4871)
| ~ spl4883_1166 ),
inference(resolution,[],[f94246,f94281]) ).
fof(f96747,plain,
( sF4880 = k4_subset_1(sF4873,sF4879,sK4871)
| ~ spl4883_1166 ),
inference(forward_demodulation,[],[f96724,f82376]) ).
fof(f96772,plain,
( sF4880 = k7_filter_2(sK4870,sF4880)
| ~ spl4883_1165 ),
inference(resolution,[],[f94243,f95537]) ).
fof(f96774,plain,
( v1_xboole_0(sF4880)
| k19_filter_2(sK4870,sF4880) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,sF4880))
| ~ spl4883_1165
| ~ spl4883_1274 ),
inference(resolution,[],[f94243,f96219]) ).
fof(f96997,plain,
( k4_subset_1(sF4873,sF4879,sK4871) = k3_tarski(k2_tarski(sF4879,sK4871))
| ~ spl4883_1166 ),
inference(resolution,[],[f96719,f82383]) ).
fof(f97009,plain,
( sF4880 = k3_tarski(k2_tarski(sF4879,sK4871))
| ~ spl4883_1166 ),
inference(forward_demodulation,[],[f96997,f96747]) ).
fof(f97016,plain,
( ~ sP387(sK4870)
| spl4883_1185 ),
inference(resolution,[],[f95309,f59216]) ).
fof(f97017,plain,
( $false
| spl4883_1185 ),
inference(forward_subsumption_resolution,[],[f97016,f94458]) ).
fof(f97018,plain,
spl4883_1185,
inference(avatar_contradiction_clause,[],[f97017]) ).
fof(f97028,plain,
( ~ l3_lattices(sK4870)
| spl4883_1184 ),
inference(resolution,[],[f95305,f59463]) ).
fof(f97029,plain,
( $false
| spl4883_1184 ),
inference(forward_subsumption_resolution,[],[f97028,f69759]) ).
fof(f97030,plain,
spl4883_1184,
inference(avatar_contradiction_clause,[],[f97029]) ).
fof(f97035,plain,
( v3_struct_0(sK4870)
| ~ l3_lattices(sK4870)
| ~ spl4883_1168 ),
inference(resolution,[],[f94567,f59195]) ).
fof(f97036,plain,
( ~ l3_lattices(sK4870)
| ~ spl4883_1168 ),
inference(forward_subsumption_resolution,[],[f97035,f69761]) ).
fof(f97038,plain,
( $false
| ~ spl4883_1168 ),
inference(forward_subsumption_resolution,[],[f97036,f69759]) ).
fof(f97039,plain,
~ spl4883_1168,
inference(avatar_contradiction_clause,[],[f97038]) ).
fof(f97045,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ v10_lattices(k1_lattice2(sK4870))
| ~ l3_lattices(k1_lattice2(sK4870))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),X0) = k3_filter_2(k1_lattice2(sK4870),X0) )
| spl4883_1168 ),
inference(forward_subsumption_resolution,[],[f94553,f94566]) ).
fof(f97051,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,X1,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,k3_filter_0(k1_lattice2(sK4870),X1),X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(sF4873))
| ~ v10_lattices(k1_lattice2(sK4870))
| ~ l3_lattices(k1_lattice2(sK4870)) )
| spl4883_1168 ),
inference(forward_subsumption_resolution,[],[f94830,f94566]) ).
fof(f97070,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| ~ l3_lattices(k1_lattice2(sK4870))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),X0) = k3_filter_2(k1_lattice2(sK4870),X0) )
| spl4883_1168
| ~ spl4883_1185 ),
inference(forward_subsumption_resolution,[],[f97045,f95308]) ).
fof(f97076,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,X1,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,k3_filter_0(k1_lattice2(sK4870),X1),X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(sF4873))
| ~ l3_lattices(k1_lattice2(sK4870)) )
| spl4883_1168
| ~ spl4883_1185 ),
inference(forward_subsumption_resolution,[],[f97051,f95308]) ).
fof(f97095,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),X0) = k3_filter_2(k1_lattice2(sK4870),X0) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(forward_subsumption_resolution,[],[f97070,f95304]) ).
fof(f97101,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_pcomps_1(sF4873))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,X1,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,k3_filter_0(k1_lattice2(sK4870),X1),X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(sF4873)) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(forward_subsumption_resolution,[],[f97076,f95304]) ).
fof(f97111,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),X0) = k3_filter_2(k1_lattice2(sK4870),X0) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(forward_demodulation,[],[f97095,f82381]) ).
fof(f97116,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,X1,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,k3_filter_0(k1_lattice2(sK4870),X1),X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_pcomps_1(sF4873)) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(forward_demodulation,[],[f97101,f82381]) ).
fof(f97125,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF4882)
| ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,X1,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,k3_filter_0(k1_lattice2(sK4870),X1),X0))
| v1_xboole_0(X1) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(forward_demodulation,[],[f97116,f82381]) ).
fof(f97141,plain,
( v1_xboole_0(sK4871)
| k3_filter_2(k1_lattice2(sK4870),sK4871) = k3_filter_0(k1_lattice2(sK4870),sK4871)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(resolution,[],[f97111,f82383]) ).
fof(f97142,plain,
( v1_xboole_0(sK4872)
| k3_filter_2(k1_lattice2(sK4870),sK4872) = k3_filter_0(k1_lattice2(sK4870),sK4872)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(resolution,[],[f97111,f82382]) ).
fof(f97144,plain,
( v1_xboole_0(sF4874)
| k3_filter_0(k1_lattice2(sK4870),sF4874) = k3_filter_2(k1_lattice2(sK4870),sF4874)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(resolution,[],[f97111,f94239]) ).
fof(f97146,plain,
( v1_xboole_0(sF4877)
| k3_filter_0(k1_lattice2(sK4870),sF4877) = k3_filter_2(k1_lattice2(sK4870),sF4877)
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(resolution,[],[f97111,f94233]) ).
fof(f97148,plain,
( v1_xboole_0(sF4880)
| k3_filter_0(k1_lattice2(sK4870),sF4880) = k3_filter_2(k1_lattice2(sK4870),sF4880)
| ~ spl4883_1165
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(resolution,[],[f97111,f94243]) ).
fof(f97154,plain,
( k3_filter_2(k1_lattice2(sK4870),sK4872) = k3_filter_0(k1_lattice2(sK4870),sK4872)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(forward_subsumption_resolution,[],[f97142,f69765]) ).
fof(f97155,plain,
( k3_filter_2(k1_lattice2(sK4870),sK4871) = k3_filter_0(k1_lattice2(sK4870),sK4871)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(forward_subsumption_resolution,[],[f97141,f69763]) ).
fof(f97160,plain,
( sF4879 = k3_filter_0(k1_lattice2(sK4870),sK4872)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f97154,f96489]) ).
fof(f97161,plain,
( sF4876 = k3_filter_0(k1_lattice2(sK4870),sK4871)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f97155,f96490]) ).
fof(f97200,plain,
( k4_subset_1(sF4873,sF4876,sK4872) = k3_tarski(k2_tarski(sF4876,sK4872))
| ~ spl4883_1164 ),
inference(resolution,[],[f96635,f82382]) ).
fof(f97210,plain,
( sF4877 = k3_tarski(k2_tarski(sF4876,sK4872))
| ~ spl4883_1164 ),
inference(forward_demodulation,[],[f97200,f82370]) ).
fof(f97254,definition,
( spl4883_1311
<=> r1_tarski(sK4872,sK4871) ),
introduced(definition,[new_symbols(definition,[spl4883_1311])],[avatar_definition]) ).
fof(f97255,plain,
( r1_tarski(sK4872,sK4871)
| ~ spl4883_1311 ),
inference(avatar_component_clause,[],[f97254]) ).
fof(f97256,plain,
( ~ r1_tarski(sK4872,sK4871)
| spl4883_1311 ),
inference(avatar_component_clause,[],[f97254]) ).
fof(f97957,plain,
( ! [X0] :
( r1_tarski(k19_filter_2(sK4870,X0),sF4873)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(sF4873)
| ~ r1_tarski(X0,sF4873)
| ~ m1_subset_1(sF4873,sF4882) )
| ~ spl4883_1169
| ~ spl4883_1276 ),
inference(superposition,[],[f96227,f96557]) ).
fof(f97981,plain,
( ! [X0] :
( r1_tarski(k19_filter_2(sK4870,X0),sF4873)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(sF4873)
| ~ m1_subset_1(sF4873,sF4882) )
| ~ spl4883_1169
| ~ spl4883_1276 ),
inference(forward_subsumption_resolution,[],[f97957,f94633]) ).
fof(f97988,plain,
( ! [X0] :
( r1_tarski(k19_filter_2(sK4870,X0),sF4873)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF4882)
| ~ m1_subset_1(sF4873,sF4882) )
| ~ spl4883_1169
| spl4883_1230
| ~ spl4883_1276 ),
inference(forward_subsumption_resolution,[],[f97981,f95692]) ).
fof(f97992,plain,
( ! [X0] :
( r1_tarski(k19_filter_2(sK4870,X0),sF4873)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF4882) )
| ~ spl4883_1169
| spl4883_1230
| ~ spl4883_1276 ),
inference(forward_subsumption_resolution,[],[f97988,f94887]) ).
fof(f101115,plain,
( r1_tarski(sF4875,sF4873)
| v1_xboole_0(sF4874)
| ~ m1_subset_1(sF4874,sF4882)
| ~ spl4883_1169
| spl4883_1230
| ~ spl4883_1276 ),
inference(superposition,[],[f97992,f82366]) ).
fof(f102104,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF4882)
| ~ m1_subset_1(X0,sF4882)
| k1_setfam_1(k2_tarski(X1,X0)) = k5_subset_1(sF4873,X1,X0) ),
inference(superposition,[],[f88932,f82381]) ).
fof(f102113,plain,
! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k5_subset_1(sF4873,sK4872,X0) = k1_setfam_1(k2_tarski(sK4872,X0)) ),
inference(resolution,[],[f102104,f82382]) ).
fof(f102115,plain,
! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k5_subset_1(sF4873,sF4874,X0) = k1_setfam_1(k2_tarski(sF4874,X0)) ),
inference(resolution,[],[f102104,f94239]) ).
fof(f102150,plain,
k5_subset_1(sF4873,sK4872,k3_tarski(k2_tarski(sK4872,sK4871))) = k1_setfam_1(k2_tarski(sK4872,k3_tarski(k2_tarski(sK4872,sK4871)))),
inference(resolution,[],[f102113,f94274]) ).
fof(f102174,plain,
sK4872 = k5_subset_1(sF4873,sK4872,k3_tarski(k2_tarski(sK4872,sK4871))),
inference(forward_demodulation,[],[f102150,f91174]) ).
fof(f102175,plain,
sK4872 = k5_subset_1(sF4873,sK4872,sF4874),
inference(forward_demodulation,[],[f102174,f94289]) ).
fof(f102176,plain,
sK4872 = k5_subset_1(sF4873,sF4874,sK4872),
inference(forward_demodulation,[],[f102175,f95090]) ).
fof(f102233,plain,
k5_subset_1(sF4873,sF4874,sK4872) = k1_setfam_1(k2_tarski(sF4874,sK4872)),
inference(resolution,[],[f102115,f82382]) ).
fof(f102243,plain,
sK4872 = k1_setfam_1(k2_tarski(sF4874,sK4872)),
inference(forward_demodulation,[],[f102233,f102176]) ).
fof(f104280,plain,
( k19_filter_2(sK4870,sF4874) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,sF4874))
| spl4883_1256
| ~ spl4883_1274 ),
inference(forward_subsumption_resolution,[],[f96479,f95851]) ).
fof(f104291,plain,
( k3_filter_0(k1_lattice2(sK4870),sF4874) = k3_filter_2(k1_lattice2(sK4870),sF4874)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256 ),
inference(forward_subsumption_resolution,[],[f97144,f95851]) ).
fof(f104365,plain,
( r1_tarski(sF4875,sF4873)
| ~ m1_subset_1(sF4874,sF4882)
| ~ spl4883_1169
| spl4883_1230
| spl4883_1256
| ~ spl4883_1276 ),
inference(forward_subsumption_resolution,[],[f101115,f95851]) ).
fof(f104398,plain,
( k19_filter_2(sK4870,sF4874) = k3_filter_2(k1_lattice2(sK4870),sF4874)
| spl4883_1256
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f104280,f96332]) ).
fof(f104467,plain,
( r1_tarski(sF4875,sF4873)
| ~ spl4883_1169
| spl4883_1230
| spl4883_1256
| ~ spl4883_1276 ),
inference(forward_subsumption_resolution,[],[f104365,f94239]) ).
fof(f104491,plain,
( k19_filter_2(sK4870,sF4874) = k3_filter_0(k1_lattice2(sK4870),sF4874)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f104398,f104291]) ).
fof(f104566,plain,
( sF4875 = k3_filter_0(k1_lattice2(sK4870),sF4874)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f104491,f82366]) ).
fof(f105656,plain,
( k19_filter_2(sK4870,sF4880) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,sF4880))
| ~ spl4883_1165
| spl4883_1263
| ~ spl4883_1274 ),
inference(forward_subsumption_resolution,[],[f96774,f96139]) ).
fof(f105662,plain,
( k3_filter_0(k1_lattice2(sK4870),sF4880) = k3_filter_2(k1_lattice2(sK4870),sF4880)
| ~ spl4883_1165
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1263 ),
inference(forward_subsumption_resolution,[],[f97148,f96139]) ).
fof(f105801,plain,
( k19_filter_2(sK4870,sF4877) = k3_filter_2(k1_lattice2(sK4870),k7_filter_2(sK4870,sF4877))
| ~ spl4883_1163
| spl4883_1266
| ~ spl4883_1274 ),
inference(forward_subsumption_resolution,[],[f96692,f96151]) ).
fof(f105807,plain,
( k3_filter_0(k1_lattice2(sK4870),sF4877) = k3_filter_2(k1_lattice2(sK4870),sF4877)
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1266 ),
inference(forward_subsumption_resolution,[],[f97146,f96151]) ).
fof(f105868,plain,
( k19_filter_2(sK4870,sF4880) = k3_filter_2(k1_lattice2(sK4870),sF4880)
| ~ spl4883_1165
| spl4883_1263
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f105656,f96772]) ).
fof(f105952,plain,
( k19_filter_2(sK4870,sF4877) = k3_filter_2(k1_lattice2(sK4870),sF4877)
| ~ spl4883_1163
| spl4883_1266
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f105801,f96690]) ).
fof(f106012,plain,
( k19_filter_2(sK4870,sF4880) = k3_filter_0(k1_lattice2(sK4870),sF4880)
| ~ spl4883_1165
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1263
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f105868,f105662]) ).
fof(f106055,plain,
( k19_filter_2(sK4870,sF4877) = k3_filter_0(k1_lattice2(sK4870),sF4877)
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1266
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f105952,f105807]) ).
fof(f106096,plain,
( sF4881 = k3_filter_0(k1_lattice2(sK4870),sF4880)
| ~ spl4883_1165
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1263
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f106012,f82378]) ).
fof(f106114,plain,
( sF4878 = k3_filter_0(k1_lattice2(sK4870),sF4877)
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1266
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f106055,f82372]) ).
fof(f106640,definition,
( spl4883_1453
<=> r1_tarski(sF4877,sK4871) ),
introduced(definition,[new_symbols(definition,[spl4883_1453])],[avatar_definition]) ).
fof(f106641,plain,
( r1_tarski(sF4877,sK4871)
| ~ spl4883_1453 ),
inference(avatar_component_clause,[],[f106640]) ).
fof(f106642,plain,
( ~ r1_tarski(sF4877,sK4871)
| spl4883_1453 ),
inference(avatar_component_clause,[],[f106640]) ).
fof(f108975,plain,
k3_tarski(k2_tarski(sF4874,sK4872)) = k5_xboole_0(sF4874,k5_xboole_0(sK4872,sK4872)),
inference(superposition,[],[f89960,f102243]) ).
fof(f108981,plain,
k3_tarski(k2_tarski(sF4874,sK4872)) = k5_xboole_0(sF4874,k5_nat_lat),
inference(forward_demodulation,[],[f108975,f69931]) ).
fof(f108986,plain,
sF4874 = k3_tarski(k2_tarski(sF4874,sK4872)),
inference(forward_demodulation,[],[f108981,f69855]) ).
fof(f110535,plain,
( ! [X0] :
( ~ r1_tarski(X0,sK4871)
| r1_tarski(X0,sF4876) )
| ~ spl4883_1281 ),
inference(resolution,[],[f41405,f96250]) ).
fof(f111236,plain,
( ~ v1_xboole_0(sF4877)
| spl4883_1453 ),
inference(resolution,[],[f95094,f106642]) ).
fof(f111251,plain,
( $false
| ~ spl4883_1266
| spl4883_1453 ),
inference(forward_subsumption_resolution,[],[f111236,f96152]) ).
fof(f111252,plain,
( ~ spl4883_1266
| spl4883_1453 ),
inference(avatar_contradiction_clause,[],[f111251]) ).
fof(f112450,plain,
( ! [X0] :
( ~ r1_tarski(X0,sF4877)
| r1_tarski(X0,sK4871) )
| ~ spl4883_1453 ),
inference(resolution,[],[f106641,f41405]) ).
fof(f113951,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4871,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,k3_filter_0(k1_lattice2(sK4870),sK4871),X0))
| v1_xboole_0(sK4871) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(resolution,[],[f97125,f82383]) ).
fof(f113952,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4872,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,k3_filter_0(k1_lattice2(sK4870),sK4872),X0))
| v1_xboole_0(sK4872) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(resolution,[],[f97125,f82382]) ).
fof(f113967,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4872,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,k3_filter_0(k1_lattice2(sK4870),sK4872),X0)) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(forward_subsumption_resolution,[],[f113952,f69765]) ).
fof(f113968,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4871,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,k3_filter_0(k1_lattice2(sK4870),sK4871),X0)) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185 ),
inference(forward_subsumption_resolution,[],[f113951,f69763]) ).
fof(f113973,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4872,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sF4879,X0))
| v1_xboole_0(X0) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f113967,f97160]) ).
fof(f113974,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF4882)
| k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4871,X0)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sF4876,X0))
| v1_xboole_0(X0) )
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f113968,f97161]) ).
fof(f113984,plain,
( k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4871,sK4872)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sF4876,sK4872))
| v1_xboole_0(sK4872)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(resolution,[],[f113974,f82382]) ).
fof(f113999,plain,
( k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4871,sK4872)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sF4876,sK4872))
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_subsumption_resolution,[],[f113984,f69765]) ).
fof(f114010,plain,
( k3_filter_0(k1_lattice2(sK4870),sF4877) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4871,sK4872))
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f113999,f82370]) ).
fof(f114018,plain,
( k3_filter_0(k1_lattice2(sK4870),sF4874) = k3_filter_0(k1_lattice2(sK4870),sF4877)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f114010,f82364]) ).
fof(f114414,definition,
( spl4883_1570
<=> r1_tarski(sK4871,sF4880) ),
introduced(definition,[new_symbols(definition,[spl4883_1570])],[avatar_definition]) ).
fof(f114415,plain,
( r1_tarski(sK4871,sF4880)
| ~ spl4883_1570 ),
inference(avatar_component_clause,[],[f114414]) ).
fof(f114416,plain,
( ~ r1_tarski(sK4871,sF4880)
| spl4883_1570 ),
inference(avatar_component_clause,[],[f114414]) ).
fof(f114447,definition,
( spl4883_1576
<=> r1_tarski(sF4880,sK4871) ),
introduced(definition,[new_symbols(definition,[spl4883_1576])],[avatar_definition]) ).
fof(f114448,plain,
( r1_tarski(sF4880,sK4871)
| ~ spl4883_1576 ),
inference(avatar_component_clause,[],[f114447]) ).
fof(f114449,plain,
( ~ r1_tarski(sF4880,sK4871)
| spl4883_1576 ),
inference(avatar_component_clause,[],[f114447]) ).
fof(f114523,definition,
( spl4883_1581
<=> r1_tarski(sK4872,sF4877) ),
introduced(definition,[new_symbols(definition,[spl4883_1581])],[avatar_definition]) ).
fof(f114524,plain,
( r1_tarski(sK4872,sF4877)
| ~ spl4883_1581 ),
inference(avatar_component_clause,[],[f114523]) ).
fof(f114525,plain,
( ~ r1_tarski(sK4872,sF4877)
| spl4883_1581 ),
inference(avatar_component_clause,[],[f114523]) ).
fof(f114744,plain,
( r1_tarski(sK4872,sF4876)
| ~ spl4883_1281
| ~ spl4883_1311 ),
inference(resolution,[],[f97255,f110535]) ).
fof(f114827,definition,
( spl4883_1590
<=> r1_tarski(sF4874,sK4872) ),
introduced(definition,[new_symbols(definition,[spl4883_1590])],[avatar_definition]) ).
fof(f114828,plain,
( r1_tarski(sF4874,sK4872)
| ~ spl4883_1590 ),
inference(avatar_component_clause,[],[f114827]) ).
fof(f114829,plain,
( ~ r1_tarski(sF4874,sK4872)
| spl4883_1590 ),
inference(avatar_component_clause,[],[f114827]) ).
fof(f114851,plain,
( k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4872,sK4871)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sF4879,sK4871))
| v1_xboole_0(sK4871)
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(resolution,[],[f113973,f82383]) ).
fof(f114867,plain,
( k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4872,sK4871)) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sF4879,sK4871))
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_subsumption_resolution,[],[f114851,f69763]) ).
fof(f114877,plain,
( k3_filter_0(k1_lattice2(sK4870),sF4880) = k3_filter_0(k1_lattice2(sK4870),k4_subset_1(sF4873,sK4872,sK4871))
| ~ spl4883_1166
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f114867,f96747]) ).
fof(f114884,plain,
( k3_filter_0(k1_lattice2(sK4870),k3_tarski(k2_tarski(sK4872,sK4871))) = k3_filter_0(k1_lattice2(sK4870),sF4880)
| ~ spl4883_1166
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f114877,f94257]) ).
fof(f114890,plain,
( k3_filter_0(k1_lattice2(sK4870),sF4874) = k3_filter_0(k1_lattice2(sK4870),sF4880)
| ~ spl4883_1166
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f114884,f94289]) ).
fof(f115059,plain,
( ~ v1_xboole_0(sF4874)
| spl4883_1590 ),
inference(resolution,[],[f114829,f95094]) ).
fof(f115207,plain,
( ~ v1_xboole_0(sF4880)
| spl4883_1576 ),
inference(resolution,[],[f114449,f95094]) ).
fof(f115208,plain,
( $false
| ~ spl4883_1263
| spl4883_1576 ),
inference(forward_subsumption_resolution,[],[f115207,f96140]) ).
fof(f115209,plain,
( ~ spl4883_1263
| spl4883_1576 ),
inference(avatar_contradiction_clause,[],[f115208]) ).
fof(f115508,plain,
( sF4875 = k3_filter_0(k1_lattice2(sK4870),sF4880)
| ~ spl4883_1166
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f114890,f104566]) ).
fof(f115517,plain,
( sF4875 = sF4881
| ~ spl4883_1165
| ~ spl4883_1166
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| spl4883_1263
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f115508,f106096]) ).
fof(f117643,plain,
( $false
| ~ spl4883_1256
| spl4883_1590 ),
inference(forward_subsumption_resolution,[],[f115059,f95852]) ).
fof(f117644,plain,
( ~ spl4883_1256
| spl4883_1590 ),
inference(avatar_contradiction_clause,[],[f117643]) ).
fof(f118143,plain,
( $false
| ~ spl4883_1281
| spl4883_1292
| ~ spl4883_1311 ),
inference(forward_subsumption_resolution,[],[f114744,f96502]) ).
fof(f118144,plain,
( ~ spl4883_1281
| spl4883_1292
| ~ spl4883_1311 ),
inference(avatar_contradiction_clause,[],[f118143]) ).
fof(f137206,plain,
( sK4872 = k3_tarski(k2_tarski(sF4874,sK4872))
| ~ spl4883_1590 ),
inference(resolution,[],[f90736,f114828]) ).
fof(f137250,plain,
( sK4872 = sF4874
| ~ spl4883_1590 ),
inference(forward_demodulation,[],[f137206,f108986]) ).
fof(f137441,plain,
( ~ v1_xboole_0(sF4874)
| ~ spl4883_1590 ),
inference(superposition,[],[f69765,f137250]) ).
fof(f151153,plain,
( ! [X0] :
( ~ r1_tarski(X0,sK4872)
| r1_tarski(X0,sF4877) )
| ~ spl4883_1164 ),
inference(superposition,[],[f90738,f97210]) ).
fof(f151169,plain,
( ! [X0] :
( ~ r1_tarski(X0,sK4871)
| r1_tarski(X0,sF4880) )
| ~ spl4883_1166 ),
inference(superposition,[],[f90738,f97009]) ).
fof(f153256,plain,
( r1_tarski(sK4872,sF4877)
| ~ spl4883_1164 ),
inference(resolution,[],[f151153,f79778]) ).
fof(f153265,plain,
( $false
| ~ spl4883_1164
| spl4883_1581 ),
inference(forward_subsumption_resolution,[],[f153256,f114525]) ).
fof(f153266,plain,
( ~ spl4883_1164
| spl4883_1581 ),
inference(avatar_contradiction_clause,[],[f153265]) ).
fof(f154196,plain,
( r1_tarski(sK4872,sK4871)
| ~ spl4883_1453
| ~ spl4883_1581 ),
inference(resolution,[],[f114524,f112450]) ).
fof(f154209,plain,
( $false
| spl4883_1311
| ~ spl4883_1453
| ~ spl4883_1581 ),
inference(forward_subsumption_resolution,[],[f154196,f97256]) ).
fof(f154210,plain,
( spl4883_1311
| ~ spl4883_1453
| ~ spl4883_1581 ),
inference(avatar_contradiction_clause,[],[f154209]) ).
fof(f154438,plain,
( sF4878 = k3_filter_0(k1_lattice2(sK4870),sF4874)
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1266
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f106114,f114018]) ).
fof(f156490,plain,
( sF4876 = k3_tarski(k2_tarski(sK4872,sF4876))
| ~ spl4883_1292 ),
inference(resolution,[],[f96501,f90736]) ).
fof(f156494,plain,
( sF4876 = sF4877
| ~ spl4883_1164
| ~ spl4883_1292 ),
inference(forward_demodulation,[],[f156490,f96668]) ).
fof(f156578,plain,
( v1_xboole_0(sF4876)
| ~ spl4883_1164
| ~ spl4883_1266
| ~ spl4883_1292 ),
inference(superposition,[],[f96152,f156494]) ).
fof(f156677,plain,
( $false
| ~ spl4883_1164
| ~ spl4883_1266
| ~ spl4883_1282
| ~ spl4883_1292 ),
inference(forward_subsumption_resolution,[],[f156578,f96472]) ).
fof(f156678,plain,
( ~ spl4883_1164
| ~ spl4883_1266
| ~ spl4883_1282
| ~ spl4883_1292 ),
inference(avatar_contradiction_clause,[],[f156677]) ).
fof(f156737,plain,
( sF4875 = sF4878
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| spl4883_1266
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f154438,f104566]) ).
fof(f171105,plain,
( ~ r1_filter_2(sF4873,sF4875,sF4875)
| spl4883_2
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| spl4883_1266
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f82605,f156737]) ).
fof(f171956,plain,
( v1_xboole_0(sF4873)
| ~ r1_tarski(sF4875,sF4873)
| spl4883_2
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| spl4883_1266
| ~ spl4883_1274 ),
inference(resolution,[],[f171105,f94513]) ).
fof(f171963,plain,
( ~ r1_tarski(sF4875,sF4873)
| spl4883_2
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1230
| spl4883_1256
| spl4883_1266
| ~ spl4883_1274 ),
inference(forward_subsumption_resolution,[],[f171956,f95692]) ).
fof(f171976,plain,
( $false
| spl4883_2
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1169
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1230
| spl4883_1256
| spl4883_1266
| ~ spl4883_1274
| ~ spl4883_1276 ),
inference(forward_subsumption_resolution,[],[f171963,f104467]) ).
fof(f171977,plain,
( spl4883_2
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1169
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1230
| spl4883_1256
| spl4883_1266
| ~ spl4883_1274
| ~ spl4883_1276 ),
inference(avatar_contradiction_clause,[],[f171976]) ).
fof(f171984,plain,
( r1_filter_2(sF4873,sF4875,sF4875)
| ~ spl4883_2
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| spl4883_1266
| ~ spl4883_1274 ),
inference(forward_demodulation,[],[f82604,f156737]) ).
fof(f172606,plain,
( ~ r1_tarski(sF4880,sK4871)
| sK4871 = sF4880
| ~ spl4883_1570 ),
inference(resolution,[],[f114415,f41358]) ).
fof(f172607,plain,
( sK4871 = sF4880
| ~ spl4883_1570
| ~ spl4883_1576 ),
inference(forward_subsumption_resolution,[],[f172606,f114448]) ).
fof(f173325,plain,
( ~ v1_xboole_0(sF4880)
| ~ spl4883_1570
| ~ spl4883_1576 ),
inference(superposition,[],[f69763,f172607]) ).
fof(f173682,plain,
( $false
| ~ spl4883_1263
| ~ spl4883_1570
| ~ spl4883_1576 ),
inference(forward_subsumption_resolution,[],[f173325,f96140]) ).
fof(f173683,plain,
( ~ spl4883_1263
| ~ spl4883_1570
| ~ spl4883_1576 ),
inference(avatar_contradiction_clause,[],[f173682]) ).
fof(f174148,plain,
( r1_tarski(sK4871,sF4880)
| ~ spl4883_1166 ),
inference(resolution,[],[f151169,f79778]) ).
fof(f174157,plain,
( $false
| ~ spl4883_1166
| spl4883_1570 ),
inference(forward_subsumption_resolution,[],[f174148,f114416]) ).
fof(f174158,plain,
( ~ spl4883_1166
| spl4883_1570 ),
inference(avatar_contradiction_clause,[],[f174157]) ).
fof(f174887,plain,
( ~ r1_filter_2(sF4873,sF4875,sF4875)
| spl4883_1
| ~ spl4883_1165
| ~ spl4883_1166
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| spl4883_1263
| ~ spl4883_1274 ),
inference(superposition,[],[f82601,f115517]) ).
fof(f174921,plain,
( $false
| spl4883_1
| ~ spl4883_2
| ~ spl4883_1163
| ~ spl4883_1165
| ~ spl4883_1166
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| spl4883_1263
| spl4883_1266
| ~ spl4883_1274 ),
inference(forward_subsumption_resolution,[],[f174887,f171984]) ).
fof(f174922,plain,
( spl4883_1
| ~ spl4883_2
| ~ spl4883_1163
| ~ spl4883_1165
| ~ spl4883_1166
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| spl4883_1263
| spl4883_1266
| ~ spl4883_1274 ),
inference(avatar_contradiction_clause,[],[f174921]) ).
fof(f174935,plain,
( $false
| ~ spl4883_1256
| ~ spl4883_1590 ),
inference(forward_subsumption_resolution,[],[f137441,f95852]) ).
fof(f174936,plain,
( ~ spl4883_1256
| ~ spl4883_1590 ),
inference(avatar_contradiction_clause,[],[f174935]) ).
cnf(s1,plain,
( ~ spl4883_1
| ~ spl4883_2 ),
inference(sat_conversion,[],[f82606]) ).
cnf(s988,plain,
( spl4883_1163
| ~ spl4883_1164 ),
inference(sat_conversion,[],[f94238]) ).
cnf(s989,plain,
( spl4883_1165
| ~ spl4883_1166 ),
inference(sat_conversion,[],[f94248]) ).
cnf(s999,plain,
spl4883_1169,
inference(sat_conversion,[],[f95194]) ).
cnf(s1076,plain,
( spl4883_1273
| spl4883_1274 ),
inference(sat_conversion,[],[f96220]) ).
cnf(s1079,plain,
( spl4883_1273
| spl4883_1276 ),
inference(sat_conversion,[],[f96228]) ).
cnf(s1083,plain,
( spl4883_1281
| ~ spl4883_1282 ),
inference(sat_conversion,[],[f96255]) ).
cnf(s1089,plain,
~ spl4883_1230,
inference(sat_conversion,[],[f96360]) ).
cnf(s1093,plain,
~ spl4883_1273,
inference(sat_conversion,[],[f96391]) ).
cnf(s1095,plain,
spl4883_1280,
inference(sat_conversion,[],[f96413]) ).
cnf(s1096,plain,
spl4883_1282,
inference(sat_conversion,[],[f96415]) ).
cnf(s1101,plain,
( spl4883_1164
| ~ spl4883_1282 ),
inference(sat_conversion,[],[f96618]) ).
cnf(s1104,plain,
( spl4883_1166
| ~ spl4883_1280 ),
inference(sat_conversion,[],[f96702]) ).
cnf(s1115,plain,
spl4883_1185,
inference(sat_conversion,[],[f97018]) ).
cnf(s1116,plain,
spl4883_1184,
inference(sat_conversion,[],[f97030]) ).
cnf(s1117,plain,
~ spl4883_1168,
inference(sat_conversion,[],[f97039]) ).
cnf(s1392,plain,
( ~ spl4883_1266
| spl4883_1453 ),
inference(sat_conversion,[],[f111252]) ).
cnf(s1503,plain,
( ~ spl4883_1263
| spl4883_1576 ),
inference(sat_conversion,[],[f115209]) ).
cnf(s1573,plain,
( ~ spl4883_1256
| spl4883_1590 ),
inference(sat_conversion,[],[f117644]) ).
cnf(s1642,plain,
( ~ spl4883_1281
| spl4883_1292
| ~ spl4883_1311 ),
inference(sat_conversion,[],[f118144]) ).
cnf(s3674,plain,
( ~ spl4883_1164
| spl4883_1581 ),
inference(sat_conversion,[],[f153266]) ).
cnf(s3678,plain,
( spl4883_1311
| ~ spl4883_1453
| ~ spl4883_1581 ),
inference(sat_conversion,[],[f154210]) ).
cnf(s3890,plain,
( ~ spl4883_1164
| ~ spl4883_1266
| ~ spl4883_1282
| ~ spl4883_1292 ),
inference(sat_conversion,[],[f156678]) ).
cnf(s4756,plain,
( spl4883_2
| ~ spl4883_1163
| spl4883_1168
| ~ spl4883_1169
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1230
| spl4883_1256
| spl4883_1266
| ~ spl4883_1274
| ~ spl4883_1276 ),
inference(sat_conversion,[],[f171977]) ).
cnf(s4782,plain,
( ~ spl4883_1263
| ~ spl4883_1570
| ~ spl4883_1576 ),
inference(sat_conversion,[],[f173683]) ).
cnf(s4788,plain,
( ~ spl4883_1166
| spl4883_1570 ),
inference(sat_conversion,[],[f174158]) ).
cnf(s4805,plain,
( spl4883_1
| ~ spl4883_2
| ~ spl4883_1163
| ~ spl4883_1165
| ~ spl4883_1166
| spl4883_1168
| ~ spl4883_1184
| ~ spl4883_1185
| spl4883_1256
| spl4883_1263
| spl4883_1266
| ~ spl4883_1274 ),
inference(sat_conversion,[],[f174922]) ).
cnf(s4812,plain,
( ~ spl4883_1256
| ~ spl4883_1590 ),
inference(sat_conversion,[],[f174936]) ).
cnf(s4910,plain,
spl4883_1164,
inference(rat,[],[s1101,s1096]) ).
cnf(s4911,plain,
spl4883_1581,
inference(rat,[],[s3674,s4910]) ).
cnf(s4913,plain,
spl4883_1166,
inference(rat,[],[s1104,s1095]) ).
cnf(s4914,plain,
spl4883_1570,
inference(rat,[],[s4788,s4913]) ).
cnf(s4936,plain,
spl4883_1281,
inference(rat,[],[s1083,s1096]) ).
cnf(s4950,plain,
spl4883_1276,
inference(rat,[],[s1079,s1093]) ).
cnf(s4952,plain,
spl4883_1274,
inference(rat,[],[s1076,s1093]) ).
cnf(s5002,plain,
spl4883_1165,
inference(rat,[],[s989,s4913]) ).
cnf(s5006,plain,
spl4883_1163,
inference(rat,[],[s988,s4910]) ).
cnf(s5037,plain,
~ spl4883_1266,
inference(rat,[],[s3678,s1642,s1392,s3890,s4911,s4936,s1096,s4910]) ).
cnf(s5055,plain,
~ spl4883_1256,
inference(rat,[],[s1573,s4812]) ).
cnf(s5098,plain,
spl4883_2,
inference(rat,[],[s4756,s4950,s4952,s5037,s5006,s1089,s1115,s1116,s999,s1117,s5055]) ).
cnf(s5158,plain,
~ spl4883_1263,
inference(rat,[],[s1503,s4782,s4914]) ).
cnf(s5159,plain,
~ spl4883_1,
inference(rat,[],[s1,s5098]) ).
cnf(s5196,plain,
$false,
inference(rat,[],[s4805,s4952,s5037,s5055,s5098,s1115,s1116,s1117,s4913,s5002,s5006,s5159,s5158]) ).
fof(f175421,plain,
$false,
inference(avatar_sat_refutation,[],[s5196]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT315+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 % Computer : n011.cluster.edu
% 0.13/0.41 % Model : x86_64 x86_64
% 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.41 % Memory : 8046.5625MB
% 0.13/0.41 % OS : Linux 6.8.0-71-generic
% 0.13/0.41 % CPULimit : 300
% 0.13/0.41 % WCLimit : 300
% 0.13/0.41 % DateTime : Sun Sep 27 14:32:17 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.46 Running first-order theorem proving
% 0.13/0.46 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
% 26.40/5.56 % (2483413)Detected formulas, will run a generic FOF schedule.
% 26.40/5.56 % (2483418)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=1597242712:i=141193_2990 on theBenchmark for (2990ds/141193Mi)
% 26.40/5.56 % (2483424)dis-21_1_sil=8000:lcm=predicate:random_seed=1480366687:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2990 on theBenchmark for (2990ds/129Mi)
% 26.40/5.56 % (2483422)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2404700465:i=119:av=off:ss=axioms_2990 on theBenchmark for (2990ds/119Mi)
% 26.40/5.56 % (2483421)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=994734356:i=109:sd=1:ins=1:gsp=on:ss=axioms_2990 on theBenchmark for (2990ds/109Mi)
% 26.40/5.56 % (2483420)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=1279319531:i=141695:sd=1:nm=32:gsp=on:ss=included_2990 on theBenchmark for (2990ds/141695Mi)
% 26.40/5.56 % (2483423)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3757159402:s2a=on:i=139:gtg=position_2990 on theBenchmark for (2990ds/139Mi)
% 26.40/5.56 % (2483419)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=4275204215:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2990 on theBenchmark for (2990ds/134677Mi)
% 26.40/5.56 % (2483424)Instruction limit reached!
% 26.40/5.56 % (2483424)------------------------------
% 26.40/5.56 % (2483424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.40/5.56 % (2483424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.40/5.56 % (2483424)CaDiCaL version: 2.1.3
% 26.40/5.56 % (2483424)Termination reason: Instruction limit
% 26.40/5.56 % (2483424)Termination phase: Preprocessing 1
% 26.40/5.56 % (2483424)Time elapsed: 0.142 s
% 26.40/5.56 % (2483424)Peak memory usage: 104 MB
% 26.40/5.56 % (2483424)Instructions burned: 129 (million)
% 26.40/5.56 % (2483421)Refutation not found, incomplete strategy
% 26.40/5.56 % (2483421)------------------------------
% 26.40/5.56 % (2483421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.40/5.56 % (2483421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.40/5.56 % (2483421)CaDiCaL version: 2.1.3
% 26.40/5.56 % (2483421)Termination reason: Refutation not found, incomplete strategy
% 26.40/5.56 % (2483421)Time elapsed: 0.105 s
% 26.40/5.56 % (2483421)Peak memory usage: 107 MB
% 26.40/5.56 % (2483421)Instructions burned: 90 (million)
% 26.40/5.56 % (2483423)Instruction limit reached!
% 26.40/5.56 % (2483423)------------------------------
% 26.40/5.56 % (2483423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.40/5.56 % (2483423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.40/5.56 % (2483423)CaDiCaL version: 2.1.3
% 26.40/5.56 % (2483423)Termination reason: Instruction limit
% 26.40/5.56 % (2483423)Termination phase: Property scanning
% 26.40/5.56 % (2483423)Time elapsed: 0.116 s
% 26.40/5.56 % (2483423)Peak memory usage: 102 MB
% 26.40/5.56 % (2483423)Instructions burned: 139 (million)
% 26.40/5.56 % (2483422)Instruction limit reached!
% 26.40/5.56 % (2483422)------------------------------
% 26.40/5.56 % (2483422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.40/5.56 % (2483422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.40/5.56 % (2483422)CaDiCaL version: 2.1.3
% 26.40/5.56 % (2483422)Termination reason: Instruction limit
% 26.40/5.56 % (2483422)Termination phase: Function definition elimination
% 26.40/5.56 % (2483422)Time elapsed: 0.138 s
% 26.40/5.56 % (2483422)Peak memory usage: 105 MB
% 26.40/5.56 % (2483422)Instructions burned: 120 (million)
% 26.40/5.56 % (2483433)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4013259343:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/157Mi)
% 26.40/5.56 % (2483432)lrs+10_1_sil=8000:sp=occurrence:random_seed=2954396640:i=285:sd=3:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/285Mi)
% 26.40/5.56 % (2483434)lrs+1011_1_sil=32000:sp=occurrence:random_seed=472362285:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 26.40/5.56 % (2483433)Instruction limit reached!
% 26.40/5.56 % (2483433)------------------------------
% 26.40/5.56 % (2483433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.40/5.56 % (2483433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.04/7.18 % (2483433)CaDiCaL version: 2.1.3
% 38.04/7.18 % (2483433)Termination reason: Instruction limit
% 38.04/7.18 % (2483433)Termination phase: Property scanning
% 38.04/7.18 % (2483433)Time elapsed: 0.131 s
% 38.04/7.18 % (2483433)Peak memory usage: 102 MB
% 38.04/7.18 % (2483433)Instructions burned: 157 (million)
% 38.04/7.18 % (2483421)------------------------------
% 38.04/7.18 % (2483421)------------------------------
% 38.04/7.18 % (2483432)Instruction limit reached!
% 38.04/7.18 % (2483432)------------------------------
% 38.04/7.18 % (2483432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.04/7.18 % (2483432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.04/7.18 % (2483432)CaDiCaL version: 2.1.3
% 38.04/7.18 % (2483432)Termination reason: Instruction limit
% 38.04/7.18 % (2483432)Termination phase: Saturation
% 38.04/7.18 % (2483432)Time elapsed: 0.320 s
% 38.04/7.18 % (2483432)Peak memory usage: 110 MB
% 38.04/7.18 % (2483432)Instructions burned: 285 (million)
% 38.04/7.18 % (2483438)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=2928158789:s2a=on:i=248:s2at=1.23:gtg=position_2983 on theBenchmark for (2983ds/248Mi)
% 38.04/7.18 % (2483439)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1885001645:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2983 on theBenchmark for (2983ds/294Mi)
% 38.04/7.18 % (2483434)Instruction limit reached!
% 38.04/7.18 % (2483434)------------------------------
% 38.04/7.18 % (2483434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.04/7.18 % (2483434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.04/7.18 % (2483434)CaDiCaL version: 2.1.3
% 38.04/7.18 % (2483434)Termination reason: Instruction limit
% 38.04/7.18 % (2483434)Termination phase: Saturation
% 38.04/7.18 % (2483434)Time elapsed: 0.353 s
% 38.04/7.18 % (2483434)Peak memory usage: 109 MB
% 38.04/7.18 % (2483434)Instructions burned: 325 (million)
% 38.04/7.18 % (2483438)Instruction limit reached!
% 38.04/7.18 % (2483438)------------------------------
% 38.04/7.18 % (2483438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.04/7.18 % (2483438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.04/7.18 % (2483438)CaDiCaL version: 2.1.3
% 38.04/7.18 % (2483438)Termination reason: Instruction limit
% 38.04/7.18 % (2483438)Termination phase: SInE selection
% 38.04/7.18 % (2483438)Time elapsed: 0.224 s
% 38.04/7.18 % (2483438)Peak memory usage: 103 MB
% 38.04/7.18 % (2483438)Instructions burned: 248 (million)
% 38.04/7.18 % (2483440)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=267280309:i=2350_2981 on theBenchmark for (2981ds/2350Mi)
% 38.04/7.18 % (2483439)Instruction limit reached!
% 38.04/7.18 % (2483439)------------------------------
% 38.04/7.18 % (2483439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.04/7.18 % (2483439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.04/7.18 % (2483439)CaDiCaL version: 2.1.3
% 38.04/7.18 % (2483439)Termination reason: Instruction limit
% 38.04/7.18 % (2483439)Termination phase: Saturation
% 38.04/7.18 % (2483439)Time elapsed: 0.303 s
% 38.04/7.18 % (2483439)Peak memory usage: 111 MB
% 38.04/7.18 % (2483439)Instructions burned: 294 (million)
% 38.04/7.18 % (2483443)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1575051605:cts=off:i=113:fsr=off:ss=included:sgt=4_2980 on theBenchmark for (2980ds/113Mi)
% 38.04/7.18 % (2483445)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3109852382:i=127:av=off:fsr=off:sup=off_2978 on theBenchmark for (2978ds/127Mi)
% 38.04/7.18 % (2483443)Instruction limit reached!
% 38.04/7.18 % (2483443)------------------------------
% 38.04/7.18 % (2483443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.04/7.18 % (2483443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.04/7.18 % (2483443)CaDiCaL version: 2.1.3
% 38.04/7.18 % (2483443)Termination reason: Instruction limit
% 38.04/7.18 % (2483443)Termination phase: Preprocessing 3
% 38.04/7.18 % (2483443)Time elapsed: 0.146 s
% 38.04/7.18 % (2483443)Peak memory usage: 106 MB
% 38.04/7.18 % (2483443)Instructions burned: 116 (million)
% 38.04/7.18 % (2483446)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2640918997:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2977 on theBenchmark for (2977ds/114Mi)
% 38.04/7.18 % (2483445)Instruction limit reached!
% 38.04/7.18 % (2483445)------------------------------
% 87.68/14.17 % (2483445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.68/14.17 % (2483445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.68/14.17 % (2483445)CaDiCaL version: 2.1.3
% 87.68/14.17 % (2483445)Termination reason: Instruction limit
% 87.68/14.17 % (2483445)Termination phase: Preprocessing 2
% 87.68/14.17 % (2483445)Time elapsed: 0.156 s
% 87.68/14.17 % (2483445)Peak memory usage: 106 MB
% 87.68/14.17 % (2483445)Instructions burned: 127 (million)
% 87.68/14.17 % (2483449)lrs+10_1_sil=8000:sp=occurrence:random_seed=2394733453:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2976 on theBenchmark for (2976ds/907Mi)
% 87.68/14.17 % (2483446)Instruction limit reached!
% 87.68/14.17 % (2483446)------------------------------
% 87.68/14.17 % (2483446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.68/14.17 % (2483446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.68/14.17 % (2483446)CaDiCaL version: 2.1.3
% 87.68/14.17 % (2483446)Termination reason: Instruction limit
% 87.68/14.17 % (2483446)Termination phase: Property scanning
% 87.68/14.17 % (2483446)Time elapsed: 0.095 s
% 87.68/14.17 % (2483446)Peak memory usage: 102 MB
% 87.68/14.17 % (2483446)Instructions burned: 114 (million)
% 87.68/14.17 % (2483451)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2866673091:i=437:sd=1:aac=none:ss=included_2974 on theBenchmark for (2974ds/437Mi)
% 87.68/14.17 % (2483453)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=216380658:i=5202:ss=axioms:sgt=16_2973 on theBenchmark for (2973ds/5202Mi)
% 87.68/14.17 % (2483451)Instruction limit reached!
% 87.68/14.17 % (2483451)------------------------------
% 87.68/14.17 % (2483451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.68/14.17 % (2483451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.68/14.17 % (2483451)CaDiCaL version: 2.1.3
% 87.68/14.17 % (2483451)Termination reason: Instruction limit
% 87.68/14.17 % (2483451)Termination phase: Saturation
% 87.68/14.17 % (2483451)Time elapsed: 0.428 s
% 87.68/14.17 % (2483451)Peak memory usage: 111 MB
% 87.68/14.17 % (2483451)Instructions burned: 437 (million)
% 87.68/14.17 % (2483449)Instruction limit reached!
% 87.68/14.17 % (2483449)------------------------------
% 87.68/14.17 % (2483449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.68/14.17 % (2483449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.68/14.17 % (2483449)CaDiCaL version: 2.1.3
% 87.68/14.17 % (2483449)Termination reason: Instruction limit
% 87.68/14.17 % (2483449)Termination phase: Saturation
% 87.68/14.17 % (2483449)Time elapsed: 0.861 s
% 87.68/14.17 % (2483449)Peak memory usage: 121 MB
% 87.68/14.17 % (2483449)Instructions burned: 907 (million)
% 87.68/14.17 % (2483456)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=791180407:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2967 on theBenchmark for (2967ds/134Mi)
% 87.68/14.17 % (2483456)Instruction limit reached!
% 87.68/14.17 % (2483456)------------------------------
% 87.68/14.17 % (2483456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.68/14.17 % (2483456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.68/14.17 % (2483456)CaDiCaL version: 2.1.3
% 87.68/14.17 % (2483456)Termination reason: Instruction limit
% 87.68/14.17 % (2483456)Termination phase: Property scanning
% 87.68/14.18 % (2483456)Time elapsed: 0.153 s
% 87.68/14.18 % (2483456)Peak memory usage: 106 MB
% 87.68/14.18 % (2483456)Instructions burned: 134 (million)
% 87.68/14.18 % (2483457)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2441538879:st=8:i=592:sd=3:ep=RST:ss=axioms_2965 on theBenchmark for (2965ds/592Mi)
% 87.68/14.18 % (2483459)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=990901897:st=3:i=13193:sd=3:ss=axioms_2963 on theBenchmark for (2963ds/13193Mi)
% 87.68/14.18 % (2483457)Instruction limit reached!
% 87.68/14.18 % (2483457)------------------------------
% 87.68/14.18 % (2483457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.68/14.18 % (2483457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.68/14.18 % (2483457)CaDiCaL version: 2.1.3
% 87.68/14.18 % (2483457)Termination reason: Instruction limit
% 87.68/14.18 % (2483457)Termination phase: Property scanning
% 87.68/14.18 % (2483457)Time elapsed: 0.626 s
% 87.68/14.18 % (2483457)Peak memory usage: 124 MB
% 87.68/14.18 % (2483457)Instructions burned: 593 (million)
% 87.68/14.18 % (2483440)Instruction limit reached!
% 87.68/14.18 % (2483440)------------------------------
% 65.07/14.42 % (2483440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483440)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483440)Termination reason: Instruction limit
% 65.07/14.42 % (2483440)Termination phase: Saturation
% 65.07/14.42 % (2483440)Time elapsed: 2.405 s
% 65.07/14.42 % (2483440)Peak memory usage: 240 MB
% 65.07/14.42 % (2483440)Instructions burned: 2350 (million)
% 65.07/14.42 % (2483462)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=763176126:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/125Mi)
% 65.07/14.42 % (2483462)Instruction limit reached!
% 65.07/14.42 % (2483462)------------------------------
% 65.07/14.42 % (2483462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483462)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483462)Termination reason: Instruction limit
% 65.07/14.42 % (2483462)Termination phase: Property scanning
% 65.07/14.42 % (2483462)Time elapsed: 0.097 s
% 65.07/14.42 % (2483462)Peak memory usage: 102 MB
% 65.07/14.42 % (2483462)Instructions burned: 125 (million)
% 65.07/14.42 % (2483464)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3531128974:i=134:gtgl=5:slsql=off:gtg=exists_sym_2954 on theBenchmark for (2954ds/134Mi)
% 65.07/14.42 % (2483465)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1687902420:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/141Mi)
% 65.07/14.42 % (2483464)Instruction limit reached!
% 65.07/14.42 % (2483464)------------------------------
% 65.07/14.42 % (2483464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483464)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483464)Termination reason: Instruction limit
% 65.07/14.42 % (2483464)Termination phase: Property scanning
% 65.07/14.42 % (2483464)Time elapsed: 0.113 s
% 65.07/14.42 % (2483464)Peak memory usage: 102 MB
% 65.07/14.42 % (2483464)Instructions burned: 134 (million)
% 65.07/14.42 % (2483465)Instruction limit reached!
% 65.07/14.42 % (2483465)------------------------------
% 65.07/14.42 % (2483465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483465)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483465)Termination reason: Instruction limit
% 65.07/14.42 % (2483465)Termination phase: Saturation
% 65.07/14.42 % (2483465)Time elapsed: 0.158 s
% 65.07/14.42 % (2483465)Peak memory usage: 108 MB
% 65.07/14.42 % (2483465)Instructions burned: 142 (million)
% 65.07/14.42 % (2483468)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2835856853:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2950 on theBenchmark for (2950ds/431Mi)
% 65.07/14.42 % (2483469)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=2416553737:i=6060:aac=none:ins=25_2949 on theBenchmark for (2949ds/6060Mi)
% 65.07/14.42 % (2483468)Instruction limit reached!
% 65.07/14.42 % (2483468)------------------------------
% 65.07/14.42 % (2483468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483468)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483468)Termination reason: Instruction limit
% 65.07/14.42 % (2483468)Termination phase: Saturation
% 65.07/14.42 % (2483468)Time elapsed: 0.434 s
% 65.07/14.42 % (2483468)Peak memory usage: 111 MB
% 65.07/14.42 % (2483468)Instructions burned: 431 (million)
% 65.07/14.42 % (2483472)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=1019863244:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2943 on theBenchmark for (2943ds/150Mi)
% 65.07/14.42 % (2483472)Instruction limit reached!
% 65.07/14.42 % (2483472)------------------------------
% 65.07/14.42 % (2483472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483472)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483472)Termination reason: Instruction limit
% 65.07/14.42 % (2483472)Termination phase: Preprocessing 1
% 65.07/14.42 % (2483472)Time elapsed: 0.182 s
% 65.07/14.42 % (2483472)Peak memory usage: 103 MB
% 65.07/14.42 % (2483472)Instructions burned: 150 (million)
% 65.07/14.42 % (2483474)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1834099780:i=14155:bd=all_2938 on theBenchmark for (2938ds/14155Mi)
% 65.07/14.42 % (2483453)Instruction limit reached!
% 65.07/14.42 % (2483453)------------------------------
% 65.07/14.42 % (2483453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483453)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483453)Termination reason: Instruction limit
% 65.07/14.42 % (2483453)Termination phase: Saturation
% 65.07/14.42 % (2483453)Time elapsed: 5.644 s
% 65.07/14.42 % (2483453)Peak memory usage: 411 MB
% 65.07/14.42 % (2483453)Instructions burned: 5203 (million)
% 65.07/14.42 % (2483478)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=168656922:i=667:av=off:fsr=off_2913 on theBenchmark for (2913ds/667Mi)
% 65.07/14.42 % (2483478)Instruction limit reached!
% 65.07/14.42 % (2483478)------------------------------
% 65.07/14.42 % (2483478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483478)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483478)Termination reason: Instruction limit
% 65.07/14.42 % (2483478)Termination phase: NewCNF
% 65.07/14.42 % (2483478)Time elapsed: 0.730 s
% 65.07/14.42 % (2483478)Peak memory usage: 135 MB
% 65.07/14.42 % (2483478)Instructions burned: 667 (million)
% 65.07/14.42 % (2483480)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3647083559:s2a=on:i=185:s2at=1.8:fdi=4_2903 on theBenchmark for (2903ds/185Mi)
% 65.07/14.42 % (2483480)Instruction limit reached!
% 65.07/14.42 % (2483480)------------------------------
% 65.07/14.42 % (2483480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483480)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483480)Termination reason: Instruction limit
% 65.07/14.42 % (2483480)Termination phase: Preprocessing 1
% 65.07/14.42 % (2483480)Time elapsed: 0.213 s
% 65.07/14.42 % (2483480)Peak memory usage: 103 MB
% 65.07/14.42 % (2483480)Instructions burned: 185 (million)
% 65.07/14.42 % (2483482)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=553259865:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2899 on theBenchmark for (2899ds/193Mi)
% 65.07/14.42 % (2483482)Instruction limit reached!
% 65.07/14.42 % (2483482)------------------------------
% 65.07/14.42 % (2483482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483482)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483482)Termination reason: Instruction limit
% 65.07/14.42 % (2483482)Termination phase: Equality resolution with deletion
% 65.07/14.42 % (2483482)Time elapsed: 0.197 s
% 65.07/14.42 % (2483482)Peak memory usage: 106 MB
% 65.07/14.42 % (2483482)Instructions burned: 194 (million)
% 65.07/14.42 % (2483484)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1869822744:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2895 on theBenchmark for (2895ds/4850Mi)
% 65.07/14.42 % (2483469)Instruction limit reached!
% 65.07/14.42 % (2483469)------------------------------
% 65.07/14.42 % (2483469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.07/14.42 % (2483469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/14.42 % (2483469)CaDiCaL version: 2.1.3
% 65.07/14.42 % (2483469)Termination reason: Instruction limit
% 65.07/14.42 % (2483469)Termination phase: Saturation
% 65.07/14.42 % (2483469)Time elapsed: 6.294 s
% 65.07/14.42 % (2483469)Peak memory usage: 518 MB
% 65.07/14.42 % (2483469)Instructions burned: 6060 (million)
% 65.07/14.42 % (2483639)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2197728770:i=12111:sd=1:ss=included_2883 on theBenchmark for (2883ds/12111Mi)
% 65.07/14.42 % (2483418)First to succeed.
% 65.07/14.42 % (2483418)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2483413"
% 65.07/14.42 % (2483418)Refutation found. Thanks to Tanya!
% 65.07/14.42 % SZS status Theorem for theBenchmark
% 65.07/14.42 % SZS output start Proof for theBenchmark
% See solution above
% 89.75/14.63 % (2483418)------------------------------
% 89.75/14.63 % (2483418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.75/14.63 % (2483418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.75/14.63 % (2483418)CaDiCaL version: 2.1.3
% 89.75/14.63 % (2483418)Termination reason: Refutation
% 89.75/14.63 % (2483418)Time elapsed: 12.044 s
% 89.75/14.63 % (2483418)Peak memory usage: 534 MB
% 89.75/14.63 % (2483418)Instructions burned: 24940 (million)
% 89.75/14.63 % (2483418)------------------------------
% 89.75/14.63 % (2483418)------------------------------
% 89.75/14.63 % (2483413)Success in time 13.371 s
% 89.75/14.63 % Vampire exiting
%------------------------------------------------------------------------------