%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT328+4 : 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:59 AM UTC 2026
% Result : Theorem 26.01s 10.00s
% Output : Refutation 59.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 39
% Syntax : Number of formulae : 309 ( 29 unt; 12 def)
% Number of atoms : 1407 ( 102 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 1824 ( 726 ~; 849 |; 171 &)
% ( 35 <=>; 43 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 12 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-3 aty)
% Number of variables : 356 ( 0 sgn 347 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1,X2] :
( X2 = k2_tarski(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( X3 = X0
| X3 = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_tarski) ).
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(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f678,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f2300,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_domain_1) ).
fof(f2301,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> k6_domain_1(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_domain_1) ).
fof(f18210,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f18225,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_lattices(X0) )
=> m1_subset_1(k5_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattices) ).
fof(f21515,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f21600,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f22747,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f22752,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22852,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f31985,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f33202,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r1_boolealg(X0,X1,X2)
<=> ( r3_lattices(X0,X1,X2)
& r3_lattices(X0,X2,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_boolealg) ).
fof(f33294,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( r1_boolealg(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_boolealg) ).
fof(f34611,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(f34646,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(f34689,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_filter_2) ).
fof(f34691,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_filter_2) ).
fof(f34733,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_filter_2) ).
fof(f34734,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X1,k22_filter_2(X0,X1,X2))
& r2_hidden(X2,k22_filter_2(X0,X1,X2)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_filter_2) ).
fof(f34735,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r1_filter_2(u1_struct_0(X0),k22_filter_2(X0,X1,X1),k6_domain_1(u1_struct_0(X0),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_filter_2) ).
fof(f34736,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r1_filter_2(u1_struct_0(X0),k22_filter_2(X0,X1,X1),k6_domain_1(u1_struct_0(X0),X1)) ) ),
inference(negated_conjecture,[status(cth)],[f34735]) ).
fof(f35079,plain,
? [X0] :
( ? [X1] :
( ~ r1_filter_2(u1_struct_0(X0),k22_filter_2(X0,X1,X1),k6_domain_1(u1_struct_0(X0),X1))
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34736]) ).
fof(f35080,plain,
? [X0] :
( ? [X1] :
( ~ r1_filter_2(u1_struct_0(X0),k22_filter_2(X0,X1,X1),k6_domain_1(u1_struct_0(X0),X1))
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f35079]) ).
fof(f35083,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f35084,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f35113,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f2301]) ).
fof(f35114,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f35113]) ).
fof(f35115,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f2300]) ).
fof(f35116,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f35115]) ).
fof(f35136,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,[],[f34611]) ).
fof(f35137,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,[],[f35136]) ).
fof(f35142,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k22_filter_2(X0,X1,X2))
& r2_hidden(X2,k22_filter_2(X0,X1,X2)) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34734]) ).
fof(f35143,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k22_filter_2(X0,X1,X2))
& r2_hidden(X2,k22_filter_2(X0,X1,X2)) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35142]) ).
fof(f35144,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34733]) ).
fof(f35145,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35144]) ).
fof(f35146,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f34646]) ).
fof(f35147,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f35146]) ).
fof(f35155,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f678]) ).
fof(f35156,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f35155]) ).
fof(f35169,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f35281,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f18225]) ).
fof(f35282,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f35281]) ).
fof(f36680,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21600]) ).
fof(f36681,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36680]) ).
fof(f36682,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21515]) ).
fof(f36683,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36682]) ).
fof(f37092,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34691]) ).
fof(f37093,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f37092]) ).
fof(f37096,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34689]) ).
fof(f37097,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f37096]) ).
fof(f37163,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_boolealg(X0,X1,X2)
<=> ( r3_lattices(X0,X1,X2)
& r3_lattices(X0,X2,X1) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f33202]) ).
fof(f37164,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_boolealg(X0,X1,X2)
<=> ( r3_lattices(X0,X1,X2)
& r3_lattices(X0,X2,X1) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f37163]) ).
fof(f37201,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f31985]) ).
fof(f37202,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,[],[f37201]) ).
fof(f37252,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22780]) ).
fof(f37253,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,[],[f37252]) ).
fof(f37280,plain,
! [X0,X1,X2] :
( ( r1_boolealg(X0,X1,X2)
<=> X1 = X2 )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f33294]) ).
fof(f37281,plain,
! [X0,X1,X2] :
( ( r1_boolealg(X0,X1,X2)
<=> X1 = X2 )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f37280]) ).
fof(f37463,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f37470,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,[],[f22752]) ).
fof(f37471,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,[],[f37470]) ).
fof(f37472,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22747]) ).
fof(f37473,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f37472]) ).
fof(f37836,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18210]) ).
fof(f45145,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)) )
| ~ sP40(X0) ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f45146,plain,
! [X0] :
( sP40(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f37471,f45145]) ).
fof(f45498,plain,
( ~ r1_filter_2(u1_struct_0(sK282),k22_filter_2(sK282,sK283,sK283),k6_domain_1(u1_struct_0(sK282),sK283))
& m1_subset_1(sK283,u1_struct_0(sK282))
& ~ v3_struct_0(sK282)
& v10_lattices(sK282)
& l3_lattices(sK282) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK282,sK283]),skolemize(X0,sK282),skolemize(X1,sK283)],[f35080]) ).
fof(f45500,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f35084]) ).
fof(f45515,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,[],[f35137]) ).
fof(f45516,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2) )
& ( ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) )
| ~ r2_hidden(X3,k22_filter_2(X0,X1,X2)) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35145]) ).
fof(f45517,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2) )
& ( ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) )
| ~ r2_hidden(X3,k22_filter_2(X0,X1,X2)) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f45516]) ).
fof(f45535,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,[],[f35169]) ).
fof(f45536,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,[],[f45535]) ).
fof(f45537,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK298(X0,X1),X1)
& r2_hidden(sK298(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK298]),skolemize(X2,sK298(X0,X1))],[f45536]) ).
fof(f46092,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r2_hidden(X1,k18_filter_2(X0,X2))
| ~ r3_lattices(X0,X1,X2) )
& ( r3_lattices(X0,X1,X2)
| ~ r2_hidden(X1,k18_filter_2(X0,X2)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f37097]) ).
fof(f46096,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(f46097,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,[],[f46096]) ).
fof(f46115,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r1_boolealg(X0,X1,X2)
| ~ r3_lattices(X0,X1,X2)
| ~ r3_lattices(X0,X2,X1) )
& ( ( r3_lattices(X0,X1,X2)
& r3_lattices(X0,X2,X1) )
| ~ r1_boolealg(X0,X1,X2) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f37164]) ).
fof(f46116,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r1_boolealg(X0,X1,X2)
| ~ r3_lattices(X0,X1,X2)
| ~ r3_lattices(X0,X2,X1) )
& ( ( r3_lattices(X0,X1,X2)
& r3_lattices(X0,X2,X1) )
| ~ r1_boolealg(X0,X1,X2) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f46115]) ).
fof(f46130,plain,
! [X0,X1,X2] :
( ( ( r1_boolealg(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_boolealg(X0,X1,X2) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(nnf_transformation,[],[f37281]) ).
fof(f46175,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)) )
| ~ sP40(X0) ),
inference(nnf_transformation,[],[f45145]) ).
fof(f47391,plain,
! [X0,X1,X2] :
( ( X2 = k2_tarski(X0,X1)
| ? [X3] :
( ( ( X0 != X3
& X1 != X3 )
| ~ r2_hidden(X3,X2) )
& ( X3 = X0
| X3 = X1
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ( X0 != X3
& X1 != X3 ) )
& ( X3 = X0
| X3 = X1
| ~ r2_hidden(X3,X2) ) )
| k2_tarski(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f47392,plain,
! [X0,X1,X2] :
( ( X2 = k2_tarski(X0,X1)
| ? [X3] :
( ( ( X0 != X3
& X1 != X3 )
| ~ r2_hidden(X3,X2) )
& ( X3 = X0
| X3 = X1
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ( X0 != X3
& X1 != X3 ) )
& ( X3 = X0
| X3 = X1
| ~ r2_hidden(X3,X2) ) )
| k2_tarski(X0,X1) != X2 ) ),
inference(flattening,[],[f47391]) ).
fof(f47393,plain,
! [X0,X1,X2] :
( ( X2 = k2_tarski(X0,X1)
| ? [X3] :
( ( ( X0 != X3
& X1 != X3 )
| ~ r2_hidden(X3,X2) )
& ( X3 = X0
| X3 = X1
| r2_hidden(X3,X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ( X0 != X4
& X1 != X4 ) )
& ( X0 = X4
| X1 = X4
| ~ r2_hidden(X4,X2) ) )
| k2_tarski(X0,X1) != X2 ) ),
inference(rectify,[],[f47392]) ).
fof(f47394,plain,
! [X0,X1,X2] :
( ( X2 = k2_tarski(X0,X1)
| ( ( ( sK1359(X0,X1,X2) != X0
& sK1359(X0,X1,X2) != X1 )
| ~ r2_hidden(sK1359(X0,X1,X2),X2) )
& ( sK1359(X0,X1,X2) = X0
| sK1359(X0,X1,X2) = X1
| r2_hidden(sK1359(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ( X0 != X4
& X1 != X4 ) )
& ( X0 = X4
| X1 = X4
| ~ r2_hidden(X4,X2) ) )
| k2_tarski(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1359]),skolemize(X3,sK1359(X0,X1,X2))],[f47393]) ).
fof(f48646,plain,
l3_lattices(sK282),
inference(cnf_transformation,[],[f45498]) ).
fof(f48647,plain,
v10_lattices(sK282),
inference(cnf_transformation,[],[f45498]) ).
fof(f48648,plain,
~ v3_struct_0(sK282),
inference(cnf_transformation,[],[f45498]) ).
fof(f48649,plain,
m1_subset_1(sK283,u1_struct_0(sK282)),
inference(cnf_transformation,[],[f45498]) ).
fof(f48650,plain,
~ r1_filter_2(u1_struct_0(sK282),k22_filter_2(sK282,sK283,sK283),k6_domain_1(u1_struct_0(sK282),sK283)),
inference(cnf_transformation,[],[f45498]) ).
fof(f48652,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f35083]) ).
fof(f48656,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| r2_hidden(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f45500]) ).
fof(f48683,plain,
! [X0,X1] :
( k1_tarski(X1) = k6_domain_1(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(cnf_transformation,[],[f35114]) ).
fof(f48684,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(cnf_transformation,[],[f35116]) ).
fof(f48709,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,[],[f45515]) ).
fof(f48712,plain,
! [X2,X0,X1] :
( r2_hidden(X2,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35143]) ).
fof(f48714,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X3,k22_filter_2(X0,X1,X2))
| r3_lattices(X0,X3,X2)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f45517]) ).
fof(f48715,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X3,k22_filter_2(X0,X1,X2))
| r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f45517]) ).
fof(f48717,plain,
! [X2,X0,X1] :
( m2_lattice4(k22_filter_2(X0,X1,X2),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f35147]) ).
fof(f48718,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f35147]) ).
fof(f48730,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f35156]) ).
fof(f48752,plain,
! [X0,X1] :
( r2_hidden(sK298(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f45537]) ).
fof(f48753,plain,
! [X0,X1] :
( ~ r2_hidden(sK298(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f45537]) ).
fof(f48909,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f35282]) ).
fof(f51012,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36681]) ).
fof(f51013,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36683]) ).
fof(f51383,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| r2_hidden(X1,k18_filter_2(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37093]) ).
fof(f51386,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X1,k18_filter_2(X0,X2))
| r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f46092]) ).
fof(f51416,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f46097]) ).
fof(f51472,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X0,X2,X1)
| ~ r3_lattices(X0,X1,X2)
| r1_boolealg(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f46116]) ).
fof(f51515,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,[],[f37202]) ).
fof(f51566,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f37253]) ).
fof(f51601,plain,
! [X2,X0,X1] :
( ~ r1_boolealg(X0,X1,X2)
| X1 = X2
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f46130]) ).
fof(f51806,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37463]) ).
fof(f51813,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f46175]) ).
fof(f51822,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP40(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f45146]) ).
fof(f51824,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37473]) ).
fof(f52529,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f37836]) ).
fof(f57641,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f57646,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| X1 != X4
| k2_tarski(X0,X1) != X2 ),
inference(cnf_transformation,[],[f47394]) ).
fof(f63033,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0)
| k6_domain_1(X0,X1) = k2_tarski(X1,X1) ),
inference(definition_unfolding,[],[f48683,f57641]) ).
fof(f65014,plain,
! [X2,X0] :
( r1_filter_2(X0,X2,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(equality_resolution,[],[f48709]) ).
fof(f65672,plain,
! [X2,X0,X4] :
( r2_hidden(X4,X2)
| k2_tarski(X0,X4) != X2 ),
inference(equality_resolution,[],[f57646]) ).
fof(f65673,plain,
! [X0,X4] : r2_hidden(X4,k2_tarski(X0,X4)),
inference(equality_resolution,[],[f65672]) ).
fof(f66281,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| r1_filter_2(X0,X2,X2) ),
inference(duplicate_literal_removal,[],[f65014]) ).
fof(f68829,plain,
! [X0,X1] :
( v1_xboole_0(X0)
| r1_filter_2(X0,k6_domain_1(X0,X1),k6_domain_1(X0,X1))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(resolution,[],[f66281,f48684]) ).
fof(f68832,plain,
! [X0,X1] :
( r1_filter_2(X0,k6_domain_1(X0,X1),k6_domain_1(X0,X1))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(duplicate_literal_removal,[],[f68829]) ).
fof(f68890,plain,
! [X0] :
( r2_hidden(X0,k18_filter_2(sK282,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282) ),
inference(resolution,[],[f51383,f48649]) ).
fof(f68891,plain,
! [X0] :
( r2_hidden(X0,k18_filter_2(sK282,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK282))
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282) ),
inference(forward_subsumption_resolution,[],[f68890,f48648]) ).
fof(f68892,plain,
! [X0] :
( r2_hidden(X0,k18_filter_2(sK282,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK282))
| ~ l3_lattices(sK282) ),
inference(forward_subsumption_resolution,[],[f68891,f48647]) ).
fof(f68893,plain,
! [X0] :
( r2_hidden(X0,k18_filter_2(sK282,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK282)) ),
inference(forward_subsumption_resolution,[],[f68892,f48646]) ).
fof(f68899,plain,
( v3_struct_0(sK282)
| u1_struct_0(sK282) = u1_struct_0(k1_lattice2(sK282)) ),
inference(resolution,[],[f51566,f48646]) ).
fof(f68901,plain,
u1_struct_0(sK282) = u1_struct_0(k1_lattice2(sK282)),
inference(forward_subsumption_resolution,[],[f68899,f48648]) ).
fof(f68914,definition,
( spl2127_52
<=> l3_lattices(k1_lattice2(sK282)) ),
introduced(definition,[new_symbols(definition,[spl2127_52])],[avatar_definition]) ).
fof(f68915,plain,
( l3_lattices(k1_lattice2(sK282))
| ~ spl2127_52 ),
inference(avatar_component_clause,[],[f68914]) ).
fof(f68916,plain,
( ~ l3_lattices(k1_lattice2(sK282))
| spl2127_52 ),
inference(avatar_component_clause,[],[f68914]) ).
fof(f68918,definition,
( spl2127_53
<=> v10_lattices(k1_lattice2(sK282)) ),
introduced(definition,[new_symbols(definition,[spl2127_53])],[avatar_definition]) ).
fof(f68919,plain,
( v10_lattices(k1_lattice2(sK282))
| ~ spl2127_53 ),
inference(avatar_component_clause,[],[f68918]) ).
fof(f68920,plain,
( ~ v10_lattices(k1_lattice2(sK282))
| spl2127_53 ),
inference(avatar_component_clause,[],[f68918]) ).
fof(f68922,definition,
( spl2127_54
<=> v3_struct_0(k1_lattice2(sK282)) ),
introduced(definition,[new_symbols(definition,[spl2127_54])],[avatar_definition]) ).
fof(f68923,plain,
( ~ v3_struct_0(k1_lattice2(sK282))
| spl2127_54 ),
inference(avatar_component_clause,[],[f68922]) ).
fof(f68924,plain,
( v3_struct_0(k1_lattice2(sK282))
| ~ spl2127_54 ),
inference(avatar_component_clause,[],[f68922]) ).
fof(f68980,plain,
( ~ l3_lattices(sK282)
| spl2127_52 ),
inference(resolution,[],[f68916,f51806]) ).
fof(f68981,plain,
( $false
| spl2127_52 ),
inference(forward_subsumption_resolution,[],[f68980,f48646]) ).
fof(f68982,plain,
spl2127_52,
inference(avatar_contradiction_clause,[],[f68981]) ).
fof(f68991,plain,
( v3_struct_0(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_54 ),
inference(resolution,[],[f68924,f51824]) ).
fof(f68992,plain,
( ~ l3_lattices(sK282)
| ~ spl2127_54 ),
inference(forward_subsumption_resolution,[],[f68991,f48648]) ).
fof(f68993,plain,
( $false
| ~ spl2127_54 ),
inference(forward_subsumption_resolution,[],[f68992,f48646]) ).
fof(f68994,plain,
~ spl2127_54,
inference(avatar_contradiction_clause,[],[f68993]) ).
fof(f68995,plain,
( ~ sP40(sK282)
| spl2127_53 ),
inference(resolution,[],[f68920,f51813]) ).
fof(f68997,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f51012,f51013]) ).
fof(f68998,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f68997]) ).
fof(f68999,plain,
( ~ v1_xboole_0(u1_struct_0(sK282))
| v3_struct_0(k1_lattice2(sK282))
| ~ v10_lattices(k1_lattice2(sK282))
| ~ l3_lattices(k1_lattice2(sK282)) ),
inference(superposition,[],[f68998,f68901]) ).
fof(f69018,plain,
( v3_struct_0(sK282)
| sP40(sK282)
| ~ l3_lattices(sK282) ),
inference(resolution,[],[f51822,f48647]) ).
fof(f69023,plain,
( sP40(sK282)
| ~ l3_lattices(sK282) ),
inference(forward_subsumption_resolution,[],[f69018,f48648]) ).
fof(f69024,plain,
( ~ l3_lattices(sK282)
| spl2127_53 ),
inference(forward_subsumption_resolution,[],[f69023,f68995]) ).
fof(f69025,plain,
( $false
| spl2127_53 ),
inference(forward_subsumption_resolution,[],[f69024,f48646]) ).
fof(f69026,plain,
spl2127_53,
inference(avatar_contradiction_clause,[],[f69025]) ).
fof(f69027,plain,
( ~ v1_xboole_0(u1_struct_0(sK282))
| ~ v10_lattices(k1_lattice2(sK282))
| ~ l3_lattices(k1_lattice2(sK282))
| spl2127_54 ),
inference(forward_subsumption_resolution,[],[f68999,f68923]) ).
fof(f69030,plain,
( ~ v1_xboole_0(u1_struct_0(sK282))
| ~ l3_lattices(k1_lattice2(sK282))
| ~ spl2127_53
| spl2127_54 ),
inference(forward_subsumption_resolution,[],[f69027,f68919]) ).
fof(f69032,plain,
( ~ v1_xboole_0(u1_struct_0(sK282))
| ~ spl2127_52
| ~ spl2127_53
| spl2127_54 ),
inference(forward_subsumption_resolution,[],[f69030,f68915]) ).
fof(f69090,plain,
( v1_xboole_0(u1_struct_0(sK282))
| k6_domain_1(u1_struct_0(sK282),sK283) = k2_tarski(sK283,sK283) ),
inference(resolution,[],[f63033,f48649]) ).
fof(f69097,plain,
( k6_domain_1(u1_struct_0(sK282),sK283) = k2_tarski(sK283,sK283)
| ~ spl2127_52
| ~ spl2127_53
| spl2127_54 ),
inference(forward_subsumption_resolution,[],[f69090,f69032]) ).
fof(f69099,plain,
( r1_filter_2(u1_struct_0(sK282),k2_tarski(sK283,sK283),k2_tarski(sK283,sK283))
| v1_xboole_0(u1_struct_0(sK282))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ spl2127_52
| ~ spl2127_53
| spl2127_54 ),
inference(superposition,[],[f68832,f69097]) ).
fof(f69102,plain,
( r1_filter_2(u1_struct_0(sK282),k2_tarski(sK283,sK283),k2_tarski(sK283,sK283))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ spl2127_52
| ~ spl2127_53
| spl2127_54 ),
inference(forward_subsumption_resolution,[],[f69099,f69032]) ).
fof(f69104,plain,
( r1_filter_2(u1_struct_0(sK282),k2_tarski(sK283,sK283),k2_tarski(sK283,sK283))
| ~ spl2127_52
| ~ spl2127_53
| spl2127_54 ),
inference(forward_subsumption_resolution,[],[f69102,f48649]) ).
fof(f69161,plain,
! [X0] :
( r3_lattices(sK282,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK282))
| ~ m1_subset_1(X0,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ m1_subset_1(X0,u1_struct_0(sK282)) ),
inference(resolution,[],[f51386,f68893]) ).
fof(f69162,plain,
! [X0] :
( r3_lattices(sK282,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282) ),
inference(duplicate_literal_removal,[],[f69161]) ).
fof(f69163,plain,
! [X0] :
( r3_lattices(sK282,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK282))
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282) ),
inference(forward_subsumption_resolution,[],[f69162,f48648]) ).
fof(f69164,plain,
! [X0] :
( r3_lattices(sK282,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK282))
| ~ l3_lattices(sK282) ),
inference(forward_subsumption_resolution,[],[f69163,f48647]) ).
fof(f69165,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK282))
| r3_lattices(sK282,X0,X0) ),
inference(forward_subsumption_resolution,[],[f69164,f48646]) ).
fof(f69166,plain,
r3_lattices(sK282,sK283,sK283),
inference(resolution,[],[f69165,f48649]) ).
fof(f69253,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(sK298(k22_filter_2(X0,X1,X2),X3),u1_struct_0(X0))
| r3_lattices(X0,X1,sK298(k22_filter_2(X0,X1,X2),X3))
| ~ r3_lattices(X0,X1,X2)
| r1_tarski(k22_filter_2(X0,X1,X2),X3)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f48752,f48715]) ).
fof(f69254,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(sK298(k22_filter_2(X0,X1,X2),X3),u1_struct_0(X0))
| r3_lattices(X0,sK298(k22_filter_2(X0,X1,X2),X3),X2)
| ~ r3_lattices(X0,X1,X2)
| r1_tarski(k22_filter_2(X0,X1,X2),X3)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f48752,f48714]) ).
fof(f69265,plain,
! [X2,X0,X1] :
( ~ m2_lattice4(X1,X2)
| m1_subset_1(X0,u1_struct_0(X2))
| ~ r2_hidden(X0,X1)
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) ),
inference(resolution,[],[f48730,f51515]) ).
fof(f69282,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(X0,u1_struct_0(X1))
| ~ r2_hidden(X0,k22_filter_2(X1,X2,X3))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1)) ),
inference(resolution,[],[f69265,f48717]) ).
fof(f69285,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X0,k22_filter_2(X1,X2,X3))
| m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1)) ),
inference(duplicate_literal_removal,[],[f69282]) ).
fof(f69593,plain,
! [X2,X0,X1] :
( m1_subset_1(X0,k22_filter_2(X1,X2,X0))
| ~ r3_lattices(X1,X2,X0)
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f48652,f48712]) ).
fof(f69603,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(k22_filter_2(X0,X1,X2))
| k2_tarski(X2,X2) = k6_domain_1(k22_filter_2(X0,X1,X2),X2) ),
inference(resolution,[],[f69593,f63033]) ).
fof(f69604,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k2_tarski(X2,X2) = k6_domain_1(k22_filter_2(X0,X1,X2),X2) ),
inference(forward_subsumption_resolution,[],[f69603,f48718]) ).
fof(f69666,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(sK298(k22_filter_2(X0,X1,X2),X3),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| r1_tarski(k22_filter_2(X0,X1,X2),X3) ),
inference(resolution,[],[f69285,f48752]) ).
fof(f69758,plain,
( ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| k2_tarski(sK283,sK283) = k6_domain_1(k22_filter_2(sK282,sK283,sK283),sK283) ),
inference(resolution,[],[f69604,f69166]) ).
fof(f69763,plain,
( ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| k2_tarski(sK283,sK283) = k6_domain_1(k22_filter_2(sK282,sK283,sK283),sK283) ),
inference(duplicate_literal_removal,[],[f69758]) ).
fof(f69766,plain,
( v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| k2_tarski(sK283,sK283) = k6_domain_1(k22_filter_2(sK282,sK283,sK283),sK283) ),
inference(forward_subsumption_resolution,[],[f69763,f48649]) ).
fof(f69767,plain,
( ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| k2_tarski(sK283,sK283) = k6_domain_1(k22_filter_2(sK282,sK283,sK283),sK283) ),
inference(forward_subsumption_resolution,[],[f69766,f48648]) ).
fof(f69768,plain,
( ~ l3_lattices(sK282)
| k2_tarski(sK283,sK283) = k6_domain_1(k22_filter_2(sK282,sK283,sK283),sK283) ),
inference(forward_subsumption_resolution,[],[f69767,f48647]) ).
fof(f69769,plain,
k2_tarski(sK283,sK283) = k6_domain_1(k22_filter_2(sK282,sK283,sK283),sK283),
inference(forward_subsumption_resolution,[],[f69768,f48646]) ).
fof(f69771,plain,
( m1_subset_1(k2_tarski(sK283,sK283),k1_zfmisc_1(k22_filter_2(sK282,sK283,sK283)))
| v1_xboole_0(k22_filter_2(sK282,sK283,sK283))
| ~ m1_subset_1(sK283,k22_filter_2(sK282,sK283,sK283)) ),
inference(superposition,[],[f48684,f69769]) ).
fof(f69773,definition,
( spl2127_110
<=> m1_subset_1(sK283,k22_filter_2(sK282,sK283,sK283)) ),
introduced(definition,[new_symbols(definition,[spl2127_110])],[avatar_definition]) ).
fof(f69775,plain,
( ~ m1_subset_1(sK283,k22_filter_2(sK282,sK283,sK283))
| spl2127_110 ),
inference(avatar_component_clause,[],[f69773]) ).
fof(f69777,definition,
( spl2127_111
<=> v1_xboole_0(k22_filter_2(sK282,sK283,sK283)) ),
introduced(definition,[new_symbols(definition,[spl2127_111])],[avatar_definition]) ).
fof(f69778,plain,
( ~ v1_xboole_0(k22_filter_2(sK282,sK283,sK283))
| spl2127_111 ),
inference(avatar_component_clause,[],[f69777]) ).
fof(f69779,plain,
( v1_xboole_0(k22_filter_2(sK282,sK283,sK283))
| ~ spl2127_111 ),
inference(avatar_component_clause,[],[f69777]) ).
fof(f69781,definition,
( spl2127_112
<=> m1_subset_1(k2_tarski(sK283,sK283),k1_zfmisc_1(k22_filter_2(sK282,sK283,sK283))) ),
introduced(definition,[new_symbols(definition,[spl2127_112])],[avatar_definition]) ).
fof(f69783,plain,
( m1_subset_1(k2_tarski(sK283,sK283),k1_zfmisc_1(k22_filter_2(sK282,sK283,sK283)))
| ~ spl2127_112 ),
inference(avatar_component_clause,[],[f69781]) ).
fof(f69784,plain,
( ~ spl2127_110
| spl2127_111
| spl2127_112 ),
inference(avatar_split_clause,[],[f69771,f69781,f69777,f69773]) ).
fof(f69790,plain,
( ~ r3_lattices(sK282,sK283,sK283)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_110 ),
inference(resolution,[],[f69775,f69593]) ).
fof(f69793,plain,
( ~ r3_lattices(sK282,sK283,sK283)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_110 ),
inference(duplicate_literal_removal,[],[f69790]) ).
fof(f69795,plain,
( ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_110 ),
inference(forward_subsumption_resolution,[],[f69793,f69165]) ).
fof(f69797,plain,
( v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_110 ),
inference(forward_subsumption_resolution,[],[f69795,f48649]) ).
fof(f69799,plain,
( ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_110 ),
inference(forward_subsumption_resolution,[],[f69797,f48648]) ).
fof(f69801,plain,
( ~ l3_lattices(sK282)
| spl2127_110 ),
inference(forward_subsumption_resolution,[],[f69799,f48647]) ).
fof(f69804,plain,
( $false
| spl2127_110 ),
inference(forward_subsumption_resolution,[],[f69801,f48646]) ).
fof(f69805,plain,
spl2127_110,
inference(avatar_contradiction_clause,[],[f69804]) ).
fof(f69806,plain,
( v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ spl2127_111 ),
inference(resolution,[],[f69779,f48718]) ).
fof(f69807,plain,
( v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ spl2127_111 ),
inference(duplicate_literal_removal,[],[f69806]) ).
fof(f69808,plain,
( ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ spl2127_111 ),
inference(forward_subsumption_resolution,[],[f69807,f48648]) ).
fof(f69809,plain,
( ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ spl2127_111 ),
inference(forward_subsumption_resolution,[],[f69808,f48647]) ).
fof(f69810,plain,
( ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ spl2127_111 ),
inference(forward_subsumption_resolution,[],[f69809,f48646]) ).
fof(f69811,plain,
( $false
| ~ spl2127_111 ),
inference(forward_subsumption_resolution,[],[f69810,f48649]) ).
fof(f69812,plain,
~ spl2127_111,
inference(avatar_contradiction_clause,[],[f69811]) ).
fof(f69817,plain,
( ! [X0] :
( m1_subset_1(X0,k22_filter_2(sK282,sK283,sK283))
| ~ r2_hidden(X0,k2_tarski(sK283,sK283)) )
| ~ spl2127_112 ),
inference(resolution,[],[f69783,f48730]) ).
fof(f70963,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ l1_lattices(X0)
| r2_hidden(X1,k18_filter_2(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f48909,f51383]) ).
fof(f70987,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ l1_lattices(X0)
| r2_hidden(X1,k18_filter_2(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f70963]) ).
fof(f71008,plain,
! [X0,X1] :
( r2_hidden(X1,k18_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f70987,f52529]) ).
fof(f71089,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| r3_lattices(X0,X1,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f71008,f51386]) ).
fof(f71094,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| r3_lattices(X0,X1,X1) ),
inference(duplicate_literal_removal,[],[f71089]) ).
fof(f72398,plain,
( ! [X0] :
( ~ r2_hidden(X0,k2_tarski(sK283,sK283))
| r2_hidden(X0,k22_filter_2(sK282,sK283,sK283))
| v1_xboole_0(k22_filter_2(sK282,sK283,sK283)) )
| ~ spl2127_112 ),
inference(resolution,[],[f69817,f48656]) ).
fof(f72401,plain,
( ! [X0] :
( r2_hidden(X0,k22_filter_2(sK282,sK283,sK283))
| ~ r2_hidden(X0,k2_tarski(sK283,sK283)) )
| spl2127_111
| ~ spl2127_112 ),
inference(forward_subsumption_resolution,[],[f72398,f69778]) ).
fof(f73743,plain,
( ! [X0] :
( ~ r2_hidden(sK298(X0,k22_filter_2(sK282,sK283,sK283)),k2_tarski(sK283,sK283))
| r1_tarski(X0,k22_filter_2(sK282,sK283,sK283)) )
| spl2127_111
| ~ spl2127_112 ),
inference(resolution,[],[f72401,f48753]) ).
fof(f73760,plain,
( r1_tarski(k2_tarski(sK283,sK283),k22_filter_2(sK282,sK283,sK283))
| r1_tarski(k2_tarski(sK283,sK283),k22_filter_2(sK282,sK283,sK283))
| spl2127_111
| ~ spl2127_112 ),
inference(resolution,[],[f73743,f48752]) ).
fof(f73761,plain,
( r1_tarski(k2_tarski(sK283,sK283),k22_filter_2(sK282,sK283,sK283))
| spl2127_111
| ~ spl2127_112 ),
inference(duplicate_literal_removal,[],[f73760]) ).
fof(f73764,plain,
( ~ r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| k22_filter_2(sK282,sK283,sK283) = k2_tarski(sK283,sK283)
| spl2127_111
| ~ spl2127_112 ),
inference(resolution,[],[f73761,f51416]) ).
fof(f73768,definition,
( spl2127_179
<=> k22_filter_2(sK282,sK283,sK283) = k2_tarski(sK283,sK283) ),
introduced(definition,[new_symbols(definition,[spl2127_179])],[avatar_definition]) ).
fof(f73770,plain,
( k22_filter_2(sK282,sK283,sK283) = k2_tarski(sK283,sK283)
| ~ spl2127_179 ),
inference(avatar_component_clause,[],[f73768]) ).
fof(f73772,definition,
( spl2127_180
<=> r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)) ),
introduced(definition,[new_symbols(definition,[spl2127_180])],[avatar_definition]) ).
fof(f73774,plain,
( ~ r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| spl2127_180 ),
inference(avatar_component_clause,[],[f73772]) ).
fof(f73775,plain,
( spl2127_179
| ~ spl2127_180
| spl2127_111
| ~ spl2127_112 ),
inference(avatar_split_clause,[],[f73764,f69781,f69777,f73772,f73768]) ).
fof(f73785,plain,
( ~ r1_filter_2(u1_struct_0(sK282),k2_tarski(sK283,sK283),k6_domain_1(u1_struct_0(sK282),sK283))
| ~ spl2127_179 ),
inference(superposition,[],[f48650,f73770]) ).
fof(f73907,plain,
( ~ r1_filter_2(u1_struct_0(sK282),k2_tarski(sK283,sK283),k2_tarski(sK283,sK283))
| ~ spl2127_52
| ~ spl2127_53
| spl2127_54
| ~ spl2127_179 ),
inference(forward_demodulation,[],[f73785,f69097]) ).
fof(f73934,plain,
( $false
| ~ spl2127_52
| ~ spl2127_53
| spl2127_54
| ~ spl2127_179 ),
inference(forward_subsumption_resolution,[],[f73907,f69104]) ).
fof(f73935,plain,
( ~ spl2127_52
| ~ spl2127_53
| spl2127_54
| ~ spl2127_179 ),
inference(avatar_contradiction_clause,[],[f73934]) ).
fof(f77750,definition,
( spl2127_287
<=> m1_subset_1(sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),u1_struct_0(sK282)) ),
introduced(definition,[new_symbols(definition,[spl2127_287])],[avatar_definition]) ).
fof(f77751,plain,
( m1_subset_1(sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),u1_struct_0(sK282))
| ~ spl2127_287 ),
inference(avatar_component_clause,[],[f77750]) ).
fof(f77752,plain,
( ~ m1_subset_1(sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),u1_struct_0(sK282))
| spl2127_287 ),
inference(avatar_component_clause,[],[f77750]) ).
fof(f77758,plain,
( v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| spl2127_287 ),
inference(resolution,[],[f77752,f69666]) ).
fof(f77759,plain,
( v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| spl2127_287 ),
inference(duplicate_literal_removal,[],[f77758]) ).
fof(f77760,plain,
( ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77759,f48648]) ).
fof(f77761,plain,
( ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77760,f48647]) ).
fof(f77762,plain,
( ~ m1_subset_1(sK283,u1_struct_0(sK282))
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77761,f48646]) ).
fof(f77763,plain,
( r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77762,f48649]) ).
fof(f77764,plain,
( $false
| spl2127_180
| spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77763,f73774]) ).
fof(f77765,plain,
( spl2127_180
| spl2127_287 ),
inference(avatar_contradiction_clause,[],[f77764]) ).
fof(f77766,plain,
( r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ r3_lattices(sK282,sK283,sK283)
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_287 ),
inference(resolution,[],[f77751,f69253]) ).
fof(f77767,plain,
( r3_lattices(sK282,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),sK283)
| ~ r3_lattices(sK282,sK283,sK283)
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_287 ),
inference(resolution,[],[f77751,f69254]) ).
fof(f77807,plain,
( r3_lattices(sK282,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),sK283)
| ~ r3_lattices(sK282,sK283,sK283)
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_287 ),
inference(duplicate_literal_removal,[],[f77767]) ).
fof(f77808,plain,
( r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ r3_lattices(sK282,sK283,sK283)
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_287 ),
inference(duplicate_literal_removal,[],[f77766]) ).
fof(f77823,plain,
( r3_lattices(sK282,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),sK283)
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77807,f71094]) ).
fof(f77824,plain,
( r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77808,f71094]) ).
fof(f77835,definition,
( spl2127_289
<=> r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))) ),
introduced(definition,[new_symbols(definition,[spl2127_289])],[avatar_definition]) ).
fof(f77837,plain,
( r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ spl2127_289 ),
inference(avatar_component_clause,[],[f77835]) ).
fof(f77844,definition,
( spl2127_291
<=> r3_lattices(sK282,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),sK283) ),
introduced(definition,[new_symbols(definition,[spl2127_291])],[avatar_definition]) ).
fof(f77846,plain,
( r3_lattices(sK282,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),sK283)
| ~ spl2127_291 ),
inference(avatar_component_clause,[],[f77844]) ).
fof(f77848,plain,
( r3_lattices(sK282,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),sK283)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_180
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77823,f73774]) ).
fof(f77849,plain,
( r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_180
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77824,f73774]) ).
fof(f77858,plain,
( r3_lattices(sK282,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),sK283)
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_180
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77848,f48649]) ).
fof(f77859,plain,
( r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_180
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77849,f48649]) ).
fof(f77863,plain,
( r3_lattices(sK282,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),sK283)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_180
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77858,f48648]) ).
fof(f77864,plain,
( r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| spl2127_180
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77859,f48648]) ).
fof(f77866,plain,
( r3_lattices(sK282,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),sK283)
| ~ l3_lattices(sK282)
| spl2127_180
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77863,f48647]) ).
fof(f77867,plain,
( r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ l3_lattices(sK282)
| spl2127_180
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77864,f48647]) ).
fof(f77868,plain,
( r3_lattices(sK282,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),sK283)
| spl2127_180
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77866,f48646]) ).
fof(f77869,plain,
( r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| spl2127_180
| ~ spl2127_287 ),
inference(forward_subsumption_resolution,[],[f77867,f48646]) ).
fof(f77870,plain,
( spl2127_291
| spl2127_180
| ~ spl2127_287 ),
inference(avatar_split_clause,[],[f77868,f77750,f73772,f77844]) ).
fof(f77871,plain,
( spl2127_289
| spl2127_180
| ~ spl2127_287 ),
inference(avatar_split_clause,[],[f77869,f77750,f73772,f77835]) ).
fof(f77876,plain,
( ~ r3_lattices(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| r1_boolealg(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ m1_subset_1(sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),u1_struct_0(sK282))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_291 ),
inference(resolution,[],[f77846,f51472]) ).
fof(f77892,plain,
( r1_boolealg(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ m1_subset_1(sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),u1_struct_0(sK282))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77876,f77837]) ).
fof(f77899,plain,
( r1_boolealg(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77892,f77751]) ).
fof(f77906,plain,
( r1_boolealg(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77899,f48649]) ).
fof(f77913,plain,
( r1_boolealg(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77906,f48648]) ).
fof(f77920,plain,
( r1_boolealg(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ l3_lattices(sK282)
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77913,f48647]) ).
fof(f77926,plain,
( r1_boolealg(sK282,sK283,sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)))
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77920,f48646]) ).
fof(f77984,plain,
( sK283 = sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| v3_struct_0(sK282)
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ m1_subset_1(sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),u1_struct_0(sK282))
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(resolution,[],[f77926,f51601]) ).
fof(f77985,plain,
( sK283 = sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ v10_lattices(sK282)
| ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ m1_subset_1(sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),u1_struct_0(sK282))
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77984,f48648]) ).
fof(f77986,plain,
( sK283 = sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ l3_lattices(sK282)
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ m1_subset_1(sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),u1_struct_0(sK282))
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77985,f48647]) ).
fof(f77987,plain,
( sK283 = sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ m1_subset_1(sK283,u1_struct_0(sK282))
| ~ m1_subset_1(sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),u1_struct_0(sK282))
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77986,f48646]) ).
fof(f77988,plain,
( sK283 = sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ m1_subset_1(sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283)),u1_struct_0(sK282))
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77987,f48649]) ).
fof(f77989,plain,
( sK283 = sK298(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f77988,f77751]) ).
fof(f78023,plain,
( ~ r2_hidden(sK283,k2_tarski(sK283,sK283))
| r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(superposition,[],[f48753,f77989]) ).
fof(f78041,plain,
( r1_tarski(k22_filter_2(sK282,sK283,sK283),k2_tarski(sK283,sK283))
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f78023,f65673]) ).
fof(f78044,plain,
( $false
| spl2127_180
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(forward_subsumption_resolution,[],[f78041,f73774]) ).
fof(f78045,plain,
( spl2127_180
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(avatar_contradiction_clause,[],[f78044]) ).
cnf(s45,plain,
spl2127_52,
inference(sat_conversion,[],[f68982]) ).
cnf(s47,plain,
~ spl2127_54,
inference(sat_conversion,[],[f68994]) ).
cnf(s48,plain,
spl2127_53,
inference(sat_conversion,[],[f69026]) ).
cnf(s83,plain,
( ~ spl2127_110
| spl2127_111
| spl2127_112 ),
inference(sat_conversion,[],[f69784]) ).
cnf(s86,plain,
spl2127_110,
inference(sat_conversion,[],[f69805]) ).
cnf(s87,plain,
~ spl2127_111,
inference(sat_conversion,[],[f69812]) ).
cnf(s143,plain,
( spl2127_111
| ~ spl2127_112
| spl2127_179
| ~ spl2127_180 ),
inference(sat_conversion,[],[f73775]) ).
cnf(s146,plain,
( ~ spl2127_52
| ~ spl2127_53
| spl2127_54
| ~ spl2127_179 ),
inference(sat_conversion,[],[f73935]) ).
cnf(s232,plain,
( spl2127_180
| spl2127_287 ),
inference(sat_conversion,[],[f77765]) ).
cnf(s235,plain,
( spl2127_180
| ~ spl2127_287
| spl2127_291 ),
inference(sat_conversion,[],[f77870]) ).
cnf(s236,plain,
( spl2127_180
| ~ spl2127_287
| spl2127_289 ),
inference(sat_conversion,[],[f77871]) ).
cnf(s237,plain,
( spl2127_180
| ~ spl2127_287
| ~ spl2127_289
| ~ spl2127_291 ),
inference(sat_conversion,[],[f78045]) ).
cnf(s247,plain,
spl2127_112,
inference(rat,[],[s83,s87,s86]) ).
cnf(s254,plain,
~ spl2127_179,
inference(rat,[],[s146,s47,s48,s45]) ).
cnf(s270,plain,
~ spl2127_180,
inference(rat,[],[s143,s247,s87,s254]) ).
cnf(s296,plain,
spl2127_287,
inference(rat,[],[s232,s270]) ).
cnf(s299,plain,
spl2127_289,
inference(rat,[],[s236,s270,s296]) ).
cnf(s300,plain,
spl2127_291,
inference(rat,[],[s235,s270,s296]) ).
cnf(s302,plain,
$false,
inference(rat,[],[s237,s296,s270,s300,s299]) ).
fof(f78046,plain,
$false,
inference(avatar_sat_refutation,[],[s302]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT328+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.58 % Computer : n011.cluster.edu
% 0.11/0.58 % Model : x86_64 x86_64
% 0.11/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.58 % Memory : 8046.5625MB
% 0.11/0.58 % OS : Linux 6.8.0-71-generic
% 0.11/0.58 % CPULimit : 300
% 0.11/0.58 % WCLimit : 300
% 0.11/0.58 % DateTime : Sun Sep 27 14:40:47 UTC 2026
% 0.11/0.58 % CPUTime :
% 0.11/0.58 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.62 Running first-order theorem proving
% 0.11/0.62 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
% 13.61/3.59 % (2498326)Detected formulas, will run a generic FOF schedule.
% 13.61/3.59 % (2498333)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=1231351672:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2991 on theBenchmark for (2991ds/134677Mi)
% 13.61/3.59 % (2498337)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3033442507:s2a=on:i=139:gtg=position_2991 on theBenchmark for (2991ds/139Mi)
% 13.61/3.59 % (2498332)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=3397728066:i=141193_2991 on theBenchmark for (2991ds/141193Mi)
% 13.61/3.59 % (2498336)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2994282818:i=119:av=off:ss=axioms_2991 on theBenchmark for (2991ds/119Mi)
% 13.61/3.59 % (2498334)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=552967388:i=141695:sd=1:nm=32:gsp=on:ss=included_2991 on theBenchmark for (2991ds/141695Mi)
% 13.61/3.59 % (2498335)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=379621776:i=109:sd=1:ins=1:gsp=on:ss=axioms_2991 on theBenchmark for (2991ds/109Mi)
% 13.61/3.59 % (2498338)dis-21_1_sil=8000:lcm=predicate:random_seed=2845841953:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2991 on theBenchmark for (2991ds/129Mi)
% 13.61/3.59 % (2498337)Instruction limit reached!
% 13.61/3.59 % (2498337)------------------------------
% 13.61/3.59 % (2498337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.61/3.59 % (2498337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/3.59 % (2498337)CaDiCaL version: 2.1.3
% 13.61/3.59 % (2498337)Termination reason: Instruction limit
% 13.61/3.59 % (2498337)Termination phase: Property scanning
% 13.61/3.59 % (2498337)Time elapsed: 0.059 s
% 13.61/3.59 % (2498337)Peak memory usage: 136 MB
% 13.61/3.59 % (2498337)Instructions burned: 139 (million)
% 13.61/3.59 % (2498335)Instruction limit reached!
% 13.61/3.59 % (2498335)------------------------------
% 13.61/3.59 % (2498335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.61/3.59 % (2498335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/3.59 % (2498335)CaDiCaL version: 2.1.3
% 13.61/3.59 % (2498335)Termination reason: Instruction limit
% 13.61/3.59 % (2498335)Termination phase: SInE selection
% 13.61/3.59 % (2498335)Time elapsed: 0.082 s
% 13.61/3.59 % (2498335)Peak memory usage: 136 MB
% 13.61/3.59 % (2498335)Instructions burned: 110 (million)
% 13.61/3.59 % (2498336)Instruction limit reached!
% 13.61/3.59 % (2498336)------------------------------
% 13.61/3.59 % (2498336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.61/3.59 % (2498336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/3.59 % (2498336)CaDiCaL version: 2.1.3
% 13.61/3.59 % (2498336)Termination reason: Instruction limit
% 13.61/3.59 % (2498336)Termination phase: SInE selection
% 13.61/3.59 % (2498336)Time elapsed: 0.087 s
% 13.61/3.59 % (2498336)Peak memory usage: 136 MB
% 13.61/3.59 % (2498336)Instructions burned: 119 (million)
% 13.61/3.59 % (2498338)Instruction limit reached!
% 13.61/3.59 % (2498338)------------------------------
% 13.61/3.59 % (2498338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.61/3.59 % (2498338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/3.59 % (2498338)CaDiCaL version: 2.1.3
% 13.61/3.59 % (2498338)Termination reason: Instruction limit
% 13.61/3.59 % (2498338)Termination phase: SInE selection
% 13.61/3.59 % (2498338)Time elapsed: 0.084 s
% 13.61/3.59 % (2498338)Peak memory usage: 136 MB
% 13.61/3.59 % (2498338)Instructions burned: 129 (million)
% 13.61/3.59 % (2498346)lrs+10_1_sil=8000:sp=occurrence:random_seed=201042798:i=285:sd=3:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/285Mi)
% 13.61/3.59 % (2498349)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=2580078187:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 13.61/3.59 % (2498347)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3624717859:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/157Mi)
% 13.61/3.59 % (2498348)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1222207645:i=325:sd=1:ss=axioms:sgt=32_2988 on theBenchmark for (2988ds/325Mi)
% 13.61/3.59 % (2498349)Instruction limit reached!
% 22.17/4.77 % (2498349)------------------------------
% 22.17/4.77 % (2498349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.17/4.77 % (2498349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.17/4.77 % (2498349)CaDiCaL version: 2.1.3
% 22.17/4.77 % (2498349)Termination reason: Instruction limit
% 22.17/4.77 % (2498349)Termination phase: Property scanning
% 22.17/4.77 % (2498349)Time elapsed: 0.058 s
% 22.17/4.77 % (2498349)Peak memory usage: 136 MB
% 22.17/4.77 % (2498349)Instructions burned: 252 (million)
% 22.17/4.77 % (2498347)Instruction limit reached!
% 22.17/4.77 % (2498347)------------------------------
% 22.17/4.77 % (2498347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.17/4.77 % (2498347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.17/4.77 % (2498347)CaDiCaL version: 2.1.3
% 22.17/4.77 % (2498347)Termination reason: Instruction limit
% 22.17/4.77 % (2498347)Termination phase: Property scanning
% 22.17/4.77 % (2498347)Time elapsed: 0.069 s
% 22.17/4.77 % (2498347)Peak memory usage: 136 MB
% 22.17/4.77 % (2498347)Instructions burned: 158 (million)
% 22.17/4.77 % (2498346)Instruction limit reached!
% 22.17/4.77 % (2498346)------------------------------
% 22.17/4.77 % (2498346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.17/4.77 % (2498346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.17/4.77 % (2498346)CaDiCaL version: 2.1.3
% 22.17/4.77 % (2498346)Termination reason: Instruction limit
% 22.17/4.77 % (2498346)Termination phase: Saturation
% 22.17/4.77 % (2498346)Time elapsed: 0.220 s
% 22.17/4.77 % (2498346)Peak memory usage: 142 MB
% 22.17/4.77 % (2498346)Instructions burned: 285 (million)
% 22.17/4.77 % (2498354)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1566795935:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2986 on theBenchmark for (2986ds/294Mi)
% 22.17/4.77 % (2498355)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=190991349:i=2350_2986 on theBenchmark for (2986ds/2350Mi)
% 22.17/4.77 % (2498348)Instruction limit reached!
% 22.17/4.77 % (2498348)------------------------------
% 22.17/4.77 % (2498348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.17/4.77 % (2498348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.17/4.77 % (2498348)CaDiCaL version: 2.1.3
% 22.17/4.77 % (2498348)Termination reason: Instruction limit
% 22.17/4.77 % (2498348)Termination phase: Saturation
% 22.17/4.77 % (2498348)Time elapsed: 0.255 s
% 22.17/4.77 % (2498348)Peak memory usage: 142 MB
% 22.17/4.77 % (2498348)Instructions burned: 325 (million)
% 22.17/4.77 % (2498354)Instruction limit reached!
% 22.17/4.77 % (2498354)------------------------------
% 22.17/4.77 % (2498354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.17/4.77 % (2498354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.17/4.77 % (2498354)CaDiCaL version: 2.1.3
% 22.17/4.77 % (2498354)Termination reason: Instruction limit
% 22.17/4.77 % (2498354)Termination phase: SInE selection
% 22.17/4.77 % (2498354)Time elapsed: 0.104 s
% 22.17/4.77 % (2498354)Peak memory usage: 137 MB
% 22.17/4.77 % (2498354)Instructions burned: 295 (million)
% 22.17/4.77 % (2498356)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1707894816:cts=off:i=113:fsr=off:ss=included:sgt=4_2985 on theBenchmark for (2985ds/113Mi)
% 22.17/4.77 % (2498359)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=265553417:i=127:av=off:fsr=off:sup=off_2984 on theBenchmark for (2984ds/127Mi)
% 22.17/4.77 % (2498360)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3585972945:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 22.17/4.77 % (2498356)Instruction limit reached!
% 22.17/4.77 % (2498356)------------------------------
% 22.17/4.77 % (2498356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.17/4.77 % (2498356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.17/4.77 % (2498356)CaDiCaL version: 2.1.3
% 22.17/4.77 % (2498356)Termination reason: Instruction limit
% 22.17/4.77 % (2498356)Termination phase: SInE selection
% 22.17/4.77 % (2498356)Time elapsed: 0.087 s
% 22.17/4.77 % (2498356)Peak memory usage: 136 MB
% 22.17/4.77 % (2498356)Instructions burned: 114 (million)
% 22.17/4.77 % (2498360)Instruction limit reached!
% 22.17/4.77 % (2498360)------------------------------
% 22.17/4.77 % (2498360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.59/8.42 % (2498360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.59/8.42 % (2498360)CaDiCaL version: 2.1.3
% 48.59/8.42 % (2498360)Termination reason: Instruction limit
% 48.59/8.42 % (2498360)Termination phase: Property scanning
% 48.59/8.42 % (2498360)Time elapsed: 0.028 s
% 48.59/8.42 % (2498360)Peak memory usage: 136 MB
% 48.59/8.42 % (2498360)Instructions burned: 114 (million)
% 48.59/8.42 % (2498359)Instruction limit reached!
% 48.59/8.42 % (2498359)------------------------------
% 48.59/8.42 % (2498359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.59/8.42 % (2498359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.59/8.42 % (2498359)CaDiCaL version: 2.1.3
% 48.59/8.42 % (2498359)Termination reason: Instruction limit
% 48.59/8.42 % (2498359)Termination phase: Preprocessing 1
% 48.59/8.42 % (2498359)Time elapsed: 0.097 s
% 48.59/8.42 % (2498359)Peak memory usage: 137 MB
% 48.59/8.42 % (2498359)Instructions burned: 128 (million)
% 48.59/8.42 % (2498365)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4080261095:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 48.59/8.42 % (2498364)lrs+10_1_sil=8000:sp=occurrence:random_seed=2331587080:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 48.59/8.42 % (2498366)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4098621186:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 48.59/8.42 % (2498365)Instruction limit reached!
% 48.59/8.42 % (2498365)------------------------------
% 48.59/8.42 % (2498365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.59/8.42 % (2498365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.59/8.42 % (2498365)CaDiCaL version: 2.1.3
% 48.59/8.42 % (2498365)Termination reason: Instruction limit
% 48.59/8.42 % (2498365)Termination phase: Saturation
% 48.59/8.42 % (2498365)Time elapsed: 0.175 s
% 48.59/8.42 % (2498365)Peak memory usage: 144 MB
% 48.59/8.42 % (2498365)Instructions burned: 439 (million)
% 48.59/8.42 % (2498370)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=971431997:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi)
% 48.59/8.42 % (2498370)Instruction limit reached!
% 48.59/8.42 % (2498370)------------------------------
% 48.59/8.42 % (2498370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.59/8.42 % (2498370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.59/8.42 % (2498370)CaDiCaL version: 2.1.3
% 48.59/8.42 % (2498370)Termination reason: Instruction limit
% 48.59/8.42 % (2498370)Termination phase: SInE selection
% 48.59/8.42 % (2498370)Time elapsed: 0.058 s
% 48.59/8.42 % (2498370)Peak memory usage: 136 MB
% 48.59/8.42 % (2498370)Instructions burned: 137 (million)
% 48.59/8.42 % (2498372)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3208612037:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 48.59/8.42 % (2498364)Instruction limit reached!
% 48.59/8.42 % (2498364)------------------------------
% 48.59/8.42 % (2498364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.59/8.42 % (2498364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.59/8.42 % (2498364)CaDiCaL version: 2.1.3
% 48.59/8.42 % (2498364)Termination reason: Instruction limit
% 48.59/8.42 % (2498364)Termination phase: Function definition elimination
% 48.59/8.42 % (2498364)Time elapsed: 0.579 s
% 48.59/8.42 % (2498364)Peak memory usage: 156 MB
% 48.59/8.42 % (2498364)Instructions burned: 908 (million)
% 48.59/8.42 % (2498374)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2477017655:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 48.59/8.42 % (2498372)Instruction limit reached!
% 48.59/8.42 % (2498372)------------------------------
% 48.59/8.42 % (2498372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.59/8.42 % (2498372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.59/8.42 % (2498372)CaDiCaL version: 2.1.3
% 48.59/8.42 % (2498372)Termination reason: Instruction limit
% 48.59/8.42 % (2498372)Termination phase: Preprocessing 2
% 48.59/8.42 % (2498372)Time elapsed: 0.270 s
% 48.59/8.42 % (2498372)Peak memory usage: 143 MB
% 48.59/8.42 % (2498372)Instructions burned: 593 (million)
% 48.59/8.42 % (2498376)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=3666833532:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 26.01/10.00 % (2498376)Instruction limit reached!
% 26.01/10.00 % (2498376)------------------------------
% 26.01/10.00 % (2498376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498376)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498376)Termination reason: Instruction limit
% 26.01/10.00 % (2498376)Termination phase: Property scanning
% 26.01/10.00 % (2498376)Time elapsed: 0.031 s
% 26.01/10.00 % (2498376)Peak memory usage: 136 MB
% 26.01/10.00 % (2498376)Instructions burned: 126 (million)
% 26.01/10.00 % (2498378)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=447200589:i=134:gtgl=5:slsql=off:gtg=exists_sym_2971 on theBenchmark for (2971ds/134Mi)
% 26.01/10.00 % (2498378)Instruction limit reached!
% 26.01/10.00 % (2498378)------------------------------
% 26.01/10.00 % (2498378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498378)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498378)Termination reason: Instruction limit
% 26.01/10.00 % (2498378)Termination phase: Property scanning
% 26.01/10.00 % (2498378)Time elapsed: 0.034 s
% 26.01/10.00 % (2498378)Peak memory usage: 136 MB
% 26.01/10.00 % (2498378)Instructions burned: 139 (million)
% 26.01/10.00 % (2498355)Instruction limit reached!
% 26.01/10.00 % (2498355)------------------------------
% 26.01/10.00 % (2498355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498355)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498355)Termination reason: Instruction limit
% 26.01/10.00 % (2498355)Termination phase: Property scanning
% 26.01/10.00 % (2498355)Time elapsed: 1.512 s
% 26.01/10.00 % (2498355)Peak memory usage: 233 MB
% 26.01/10.00 % (2498355)Instructions burned: 2351 (million)
% 26.01/10.00 % (2498380)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2600653896:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/141Mi)
% 26.01/10.00 % (2498380)Instruction limit reached!
% 26.01/10.00 % (2498380)------------------------------
% 26.01/10.00 % (2498380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498380)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498380)Termination reason: Instruction limit
% 26.01/10.00 % (2498380)Termination phase: SInE selection
% 26.01/10.00 % (2498380)Time elapsed: 0.061 s
% 26.01/10.00 % (2498380)Peak memory usage: 136 MB
% 26.01/10.00 % (2498380)Instructions burned: 142 (million)
% 26.01/10.00 % (2498381)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=655263444:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2969 on theBenchmark for (2969ds/431Mi)
% 26.01/10.00 % (2498383)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=2977493087:i=6060:aac=none:ins=25_2968 on theBenchmark for (2968ds/6060Mi)
% 26.01/10.00 % (2498381)Refutation not found, incomplete strategy
% 26.01/10.00 % (2498381)------------------------------
% 26.01/10.00 % (2498381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498381)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498381)Termination reason: Refutation not found, incomplete strategy
% 26.01/10.00 % (2498381)Time elapsed: 0.204 s
% 26.01/10.00 % (2498381)Peak memory usage: 142 MB
% 26.01/10.00 % (2498381)Instructions burned: 245 (million)
% 26.01/10.00 % (2498381)------------------------------
% 26.01/10.00 % (2498381)------------------------------
% 26.01/10.00 % (2498386)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=1147845953:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2963 on theBenchmark for (2963ds/150Mi)
% 26.01/10.00 % (2498386)Instruction limit reached!
% 26.01/10.00 % (2498386)------------------------------
% 26.01/10.00 % (2498386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498386)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498386)Termination reason: Instruction limit
% 26.01/10.00 % (2498386)Termination phase: SInE selection
% 26.01/10.00 % (2498386)Time elapsed: 0.116 s
% 26.01/10.00 % (2498386)Peak memory usage: 136 MB
% 26.01/10.00 % (2498386)Instructions burned: 150 (million)
% 26.01/10.00 % (2498388)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3939520378:i=14155:bd=all_2960 on theBenchmark for (2960ds/14155Mi)
% 26.01/10.00 % (2498383)Instruction limit reached!
% 26.01/10.00 % (2498383)------------------------------
% 26.01/10.00 % (2498383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498383)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498383)Termination reason: Instruction limit
% 26.01/10.00 % (2498383)Termination phase: Function definition elimination
% 26.01/10.00 % (2498383)Time elapsed: 2.112 s
% 26.01/10.00 % (2498383)Peak memory usage: 245 MB
% 26.01/10.00 % (2498383)Instructions burned: 6063 (million)
% 26.01/10.00 % (2498390)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2711859900:i=667:av=off:fsr=off_2945 on theBenchmark for (2945ds/667Mi)
% 26.01/10.00 % (2498366)Instruction limit reached!
% 26.01/10.00 % (2498366)------------------------------
% 26.01/10.00 % (2498366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498366)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498366)Termination reason: Instruction limit
% 26.01/10.00 % (2498366)Termination phase: Saturation
% 26.01/10.00 % (2498366)Time elapsed: 3.894 s
% 26.01/10.00 % (2498366)Peak memory usage: 586 MB
% 26.01/10.00 % (2498366)Instructions burned: 5205 (million)
% 26.01/10.00 % (2498390)Instruction limit reached!
% 26.01/10.00 % (2498390)------------------------------
% 26.01/10.00 % (2498390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498390)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498390)Termination reason: Instruction limit
% 26.01/10.00 % (2498390)Termination phase: NewCNF
% 26.01/10.00 % (2498390)Time elapsed: 0.324 s
% 26.01/10.00 % (2498390)Peak memory usage: 186 MB
% 26.01/10.00 % (2498390)Instructions burned: 670 (million)
% 26.01/10.00 % (2498392)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=2799041011:s2a=on:i=185:s2at=1.8:fdi=4_2941 on theBenchmark for (2941ds/185Mi)
% 26.01/10.00 % (2498393)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4038407431:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2941 on theBenchmark for (2941ds/193Mi)
% 26.01/10.00 % (2498392)Instruction limit reached!
% 26.01/10.00 % (2498392)------------------------------
% 26.01/10.00 % (2498392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498392)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498392)Termination reason: Instruction limit
% 26.01/10.00 % (2498392)Termination phase: SInE selection
% 26.01/10.00 % (2498392)Time elapsed: 0.074 s
% 26.01/10.00 % (2498392)Peak memory usage: 136 MB
% 26.01/10.00 % (2498392)Instructions burned: 187 (million)
% 26.01/10.00 % (2498396)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1325259489:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2939 on theBenchmark for (2939ds/4850Mi)
% 26.01/10.00 % (2498393)Instruction limit reached!
% 26.01/10.00 % (2498393)------------------------------
% 26.01/10.00 % (2498393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498393)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498393)Termination reason: Instruction limit
% 26.01/10.00 % (2498393)Termination phase: SInE selection
% 26.01/10.00 % (2498393)Time elapsed: 0.153 s
% 26.01/10.00 % (2498393)Peak memory usage: 137 MB
% 26.01/10.00 % (2498393)Instructions burned: 193 (million)
% 26.01/10.00 % (2498398)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1022583788:i=12111:sd=1:ss=included_2937 on theBenchmark for (2937ds/12111Mi)
% 26.01/10.00 % (2498396)Instruction limit reached!
% 26.01/10.00 % (2498396)------------------------------
% 26.01/10.00 % (2498396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498396)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498396)Termination reason: Instruction limit
% 26.01/10.00 % (2498396)Termination phase: Property scanning
% 26.01/10.00 % (2498396)Time elapsed: 1.416 s
% 26.01/10.00 % (2498396)Peak memory usage: 220 MB
% 26.01/10.00 % (2498396)Instructions burned: 4860 (million)
% 26.01/10.00 % (2498400)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2779680595:i=319:kws=precedence:fsr=off_2923 on theBenchmark for (2923ds/319Mi)
% 26.01/10.00 % (2498400)Instruction limit reached!
% 26.01/10.00 % (2498400)------------------------------
% 26.01/10.00 % (2498400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498400)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498400)Termination reason: Instruction limit
% 26.01/10.00 % (2498400)Termination phase: Unused predicate definition removal
% 26.01/10.00 % (2498400)Time elapsed: 0.148 s
% 26.01/10.00 % (2498400)Peak memory usage: 142 MB
% 26.01/10.00 % (2498400)Instructions burned: 319 (million)
% 26.01/10.00 % (2498402)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2781620812:i=2064:ep=RST_2920 on theBenchmark for (2920ds/2064Mi)
% 26.01/10.00 % (2498374)First to succeed.
% 26.01/10.00 % (2498374)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2498326"
% 26.01/10.00 % (2498402)Instruction limit reached!
% 26.01/10.00 % (2498402)------------------------------
% 26.01/10.00 % (2498402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/10.00 % (2498402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/10.00 % (2498402)CaDiCaL version: 2.1.3
% 26.01/10.00 % (2498402)Termination reason: Instruction limit
% 26.01/10.00 % (2498402)Termination phase: Property scanning
% 26.01/10.00 % (2498402)Time elapsed: 0.761 s
% 26.01/10.00 % (2498402)Peak memory usage: 233 MB
% 26.01/10.00 % (2498402)Instructions burned: 2065 (million)
% 26.01/10.00 % (2498404)dis-1011_128_sil=32000:random_seed=637832192:i=3706:ep=RST:av=off_2911 on theBenchmark for (2911ds/3706Mi)
% 26.01/10.00 % (2498374)Refutation found. Thanks to Tanya!
% 26.01/10.00 % SZS status Theorem for theBenchmark
% 26.01/10.00 % SZS output start Proof for theBenchmark
% See solution above
% 59.30/10.10 % (2498374)------------------------------
% 59.30/10.10 % (2498374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.30/10.10 % (2498374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.30/10.10 % (2498374)CaDiCaL version: 2.1.3
% 59.30/10.10 % (2498374)Termination reason: Refutation
% 59.30/10.10 % (2498374)Time elapsed: 6.102 s
% 59.30/10.10 % (2498374)Peak memory usage: 350 MB
% 59.30/10.10 % (2498374)Instructions burned: 9921 (million)
% 59.30/10.10 % (2498374)------------------------------
% 59.30/10.10 % (2498374)------------------------------
% 59.30/10.10 % (2498326)Success in time 9.184 s
% 59.30/10.11 % Vampire exiting
%------------------------------------------------------------------------------