%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : LAT337+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:04:59 PM UTC 2026
% Result : Theorem 32.28s 13.09s
% Output : CNFRefutation 32.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 31
% Syntax : Number of formulae : 195 ( 44 unt; 0 def)
% Number of atoms : 1179 ( 24 equ)
% Maximal formula atoms : 65 ( 6 avg)
% Number of connectives : 1514 ( 530 ~; 541 |; 304 &)
% ( 4 <=>; 135 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 3 con; 0-3 aty)
% Number of variables : 254 ( 1 sgn 179 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t87_filter_2,conjecture,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( ( r3_lattices(X1,X2,X3)
& l3_lattices(X1)
& v17_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( l3_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v17_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v10_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& ~ v3_struct_0(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t87_filter_2) ).
fof(dt_k2_filter_0,axiom,
! [X1,X2] :
( ( m1_subset_1(X2,u1_struct_0(X1))
& l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> m1_filter_0(k2_filter_0(X1,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+242.ax',dt_k2_filter_0) ).
fof(t12_filter_0,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_filter_0(X2,X1)
=> ( ( l3_lattices(X1)
& v14_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> r2_hidden(k6_lattices(X1),X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+242.ax',t12_filter_0) ).
fof(dt_k18_filter_2,axiom,
! [X1,X2] :
( ( m1_subset_1(X2,u1_struct_0(X1))
& l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> m2_filter_2(k18_filter_2(X1,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k18_filter_2) ).
fof(t11_lattice4,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_filter_0(X2,X1)
=> m2_lattice4(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+375.ax',t11_lattice4) ).
fof(dt_m1_filter_0,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_filter_0(X2,X1)
=> ( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& ~ v1_xboole_0(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+242.ax',dt_m1_filter_0) ).
fof(dt_m2_filter_2,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( m2_lattice4(X2,X1)
& ~ v1_xboole_0(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(t25_filter_2,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( v13_lattices(X1)
=> r2_hidden(k5_lattices(X1),X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_filter_2) ).
fof(dt_k23_filter_2,axiom,
! [X1,X2] :
( ( m2_lattice4(X2,X1)
& ~ v1_xboole_0(X2)
& l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> m2_nat_lat(k23_filter_2(X1,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k23_filter_2) ).
fof(t73_filter_2,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_lattice4(X2,X1)
& ~ v1_xboole_0(X2) )
=> ( u1_lattices(k23_filter_2(X1,X2)) = k1_realset1(u1_lattices(X1),X2)
& u2_lattices(k23_filter_2(X1,X2)) = k1_realset1(u2_lattices(X1),X2)
& u1_struct_0(k23_filter_2(X1,X2)) = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t73_filter_2) ).
fof(cc5_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( v17_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v16_lattices(X1)
& v15_lattices(X1)
& v14_lattices(X1)
& v13_lattices(X1)
& v11_lattices(X1)
& ~ v3_struct_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+205.ax',cc5_lattices) ).
fof(t15_filter_0,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> m1_filter_0(u1_struct_0(X1),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+242.ax',t15_filter_0) ).
fof(d2_subset_1,axiom,
! [X1,X2] :
( ( v1_xboole_0(X1)
=> ( m1_subset_1(X2,X1)
<=> v1_xboole_0(X2) ) )
& ( ~ v1_xboole_0(X1)
=> ( m1_subset_1(X2,X1)
<=> r2_hidden(X2,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+7.ax',d2_subset_1) ).
fof(t69_filter_2,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m2_nat_lat(X2,X1)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X2))
=> m1_subset_1(X3,u1_struct_0(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_filter_2) ).
fof(t1_subset,axiom,
! [X1,X2] :
( r2_hidden(X1,X2)
=> m1_subset_1(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+9.ax',t1_subset) ).
fof(t13_filter_0,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( ( l3_lattices(X1)
& v14_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> m1_filter_0(k6_domain_1(u1_struct_0(X1),k6_lattices(X1)),X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+242.ax',t13_filter_0) ).
fof(redefinition_k6_domain_1,axiom,
! [X1,X2] :
( ( m1_subset_1(X2,X1)
& ~ v1_xboole_0(X1) )
=> k6_domain_1(X1,X2) = k1_tarski(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+22.ax',redefinition_k6_domain_1) ).
fof(t7_boole,axiom,
! [X1,X2] :
~ ( v1_xboole_0(X2)
& r2_hidden(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+3.ax',t7_boole) ).
fof(t26_filter_2,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v13_lattices(X1)
=> m2_filter_2(k6_domain_1(u1_struct_0(X1),k5_lattices(X1)),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t26_filter_2) ).
fof(t14_filter_0,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( m1_filter_0(k6_domain_1(u1_struct_0(X1),X2),X1)
=> v14_lattices(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+242.ax',t14_filter_0) ).
fof(t27_filter_2,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( m2_filter_2(k6_domain_1(u1_struct_0(X1),X2),X1)
=> v13_lattices(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t27_filter_2) ).
fof(dt_k22_filter_2,axiom,
! [X1,X2,X3] :
( ( m1_subset_1(X3,u1_struct_0(X1))
& m1_subset_1(X2,u1_struct_0(X1))
& l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( m2_lattice4(k22_filter_2(X1,X2,X3),X1)
& ~ v1_xboole_0(k22_filter_2(X1,X2,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(t86_filter_2,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( ( r3_lattices(X1,X2,X3)
& v12_lattices(X1)
& l3_lattices(X1)
& v16_lattices(X1)
& v15_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( l3_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v16_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v15_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v10_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& ~ v3_struct_0(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t86_filter_2) ).
fof(cc3_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( v14_lattices(X1)
& v13_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v15_lattices(X1)
& ~ v3_struct_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+205.ax',cc3_lattices) ).
fof(t64_filter_2,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( r3_lattices(X1,X2,X3)
=> ( r2_hidden(X3,k22_filter_2(X1,X2,X3))
& r2_hidden(X2,k22_filter_2(X1,X2,X3)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_filter_2) ).
fof(cc7_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( v11_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v12_lattices(X1)
& v10_lattices(X1)
& v9_lattices(X1)
& v8_lattices(X1)
& v7_lattices(X1)
& v6_lattices(X1)
& v5_lattices(X1)
& v4_lattices(X1)
& ~ v3_struct_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+205.ax',cc7_lattices) ).
fof(t78_filter_2,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_lattice4(X2,X1)
& ~ v1_xboole_0(X2) )
=> ( v11_lattices(X1)
=> v11_lattices(k23_filter_2(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t78_filter_2) ).
fof(fc5_filter_2,axiom,
! [X1,X2] :
( ( m2_lattice4(X2,X1)
& ~ v1_xboole_0(X2)
& l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v10_lattices(k23_filter_2(X1,X2))
& v9_lattices(k23_filter_2(X1,X2))
& v8_lattices(k23_filter_2(X1,X2))
& v7_lattices(k23_filter_2(X1,X2))
& v6_lattices(k23_filter_2(X1,X2))
& v5_lattices(k23_filter_2(X1,X2))
& v4_lattices(k23_filter_2(X1,X2))
& v3_lattices(k23_filter_2(X1,X2))
& ~ v3_struct_0(k23_filter_2(X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_filter_2) ).
fof(dt_m2_nat_lat,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m2_nat_lat(X2,X1)
=> ( l3_lattices(X2)
& v10_lattices(X2)
& ~ v3_struct_0(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+297.ax',dt_m2_nat_lat) ).
fof(t84_filter_2,axiom,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( r3_lattices(X1,X2,X3)
=> ( k5_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) = X2
& k6_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) = X3
& v15_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t84_filter_2) ).
fof(cc6_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( v16_lattices(X1)
& v15_lattices(X1)
& v11_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v17_lattices(X1)
& ~ v3_struct_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+205.ax',cc6_lattices) ).
fof(c_0_31,negated_conjecture,
~ ! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( ( r3_lattices(X1,X2,X3)
& l3_lattices(X1)
& v17_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( l3_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v17_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v10_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& ~ v3_struct_0(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) ) ) ) ) ),
inference(assume_negation,[status(cth)],[t87_filter_2]) ).
fof(c_0_32,plain,
! [X1,X2] :
( ( m1_subset_1(X2,u1_struct_0(X1))
& l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> m1_filter_0(k2_filter_0(X1,X2),X1) ),
inference(fof_simplification,[status(thm)],[dt_k2_filter_0]) ).
fof(c_0_33,negated_conjecture,
~ ! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( ( r3_lattices(X1,X2,X3)
& l3_lattices(X1)
& v17_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( l3_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v17_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v10_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& ~ v3_struct_0(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[c_0_31]) ).
fof(c_0_34,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_filter_0(X2,X1)
=> ( ( l3_lattices(X1)
& v14_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> r2_hidden(k6_lattices(X1),X2) ) ) ),
inference(fof_simplification,[status(thm)],[t12_filter_0]) ).
fof(c_0_35,plain,
! [X1,X2] :
( ( m1_subset_1(X2,u1_struct_0(X1))
& l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> m2_filter_2(k18_filter_2(X1,X2),X1) ),
inference(fof_simplification,[status(thm)],[dt_k18_filter_2]) ).
fof(c_0_36,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_filter_0(X2,X1)
=> m2_lattice4(X2,X1) ) ),
inference(fof_simplification,[status(thm)],[t11_lattice4]) ).
fof(c_0_37,plain,
! [X1889,X1890] :
( m1_filter_0(k2_filter_0(X1889,X1890),X1889)
| ~ m1_subset_1(X1890,u1_struct_0(X1889))
| ~ l3_lattices(X1889)
| ~ v10_lattices(X1889)
| v3_struct_0(X1889) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_32])])]) ).
fof(c_0_38,negated_conjecture,
( ( ~ l3_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0)))
| ~ v17_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0)))
| ~ v10_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0)))
| v3_struct_0(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))) )
& r3_lattices(esk1_0,esk2_0,esk3_0)
& l3_lattices(esk1_0)
& v17_lattices(esk1_0)
& v10_lattices(esk1_0)
& ~ v3_struct_0(esk1_0)
& m1_subset_1(esk3_0,u1_struct_0(esk1_0))
& m1_subset_1(esk2_0,u1_struct_0(esk1_0))
& l3_lattices(esk1_0)
& v10_lattices(esk1_0)
& ~ v3_struct_0(esk1_0) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_33])])])]) ).
fof(c_0_39,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_filter_0(X2,X1)
=> ( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& ~ v1_xboole_0(X2) ) ) ),
inference(fof_simplification,[status(thm)],[dt_m1_filter_0]) ).
fof(c_0_40,plain,
! [X499,X500] :
( r2_hidden(k6_lattices(X499),X500)
| ~ l3_lattices(X499)
| ~ v14_lattices(X499)
| ~ v10_lattices(X499)
| v3_struct_0(X499)
| ~ m1_filter_0(X500,X499)
| ~ l3_lattices(X499)
| ~ v10_lattices(X499)
| v3_struct_0(X499) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_34])])])]) ).
fof(c_0_41,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( m2_lattice4(X2,X1)
& ~ v1_xboole_0(X2) ) ) ),
inference(fof_simplification,[status(thm)],[dt_m2_filter_2]) ).
fof(c_0_42,plain,
! [X508,X509] :
( m2_filter_2(k18_filter_2(X508,X509),X508)
| ~ m1_subset_1(X509,u1_struct_0(X508))
| ~ l3_lattices(X508)
| ~ v10_lattices(X508)
| v3_struct_0(X508) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_35])])]) ).
fof(c_0_43,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( v13_lattices(X1)
=> r2_hidden(k5_lattices(X1),X2) ) ) ),
inference(fof_simplification,[status(thm)],[t25_filter_2]) ).
fof(c_0_44,plain,
! [X1,X2] :
( ( m2_lattice4(X2,X1)
& ~ v1_xboole_0(X2)
& l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> m2_nat_lat(k23_filter_2(X1,X2),X1) ),
inference(fof_simplification,[status(thm)],[dt_k23_filter_2]) ).
fof(c_0_45,plain,
! [X193,X194] :
( m2_lattice4(X194,X193)
| ~ m1_filter_0(X194,X193)
| ~ l3_lattices(X193)
| ~ v10_lattices(X193)
| v3_struct_0(X193) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_36])])])]) ).
cnf(c_0_46,plain,
( ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| m1_filter_0(k2_filter_0(X1,X2),X1)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
cnf(c_0_47,negated_conjecture,
m1_subset_1(esk3_0,u1_struct_0(esk1_0)),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_48,negated_conjecture,
v10_lattices(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_49,negated_conjecture,
l3_lattices(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_50,negated_conjecture,
~ v3_struct_0(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
fof(c_0_51,plain,
! [X661,X662] :
( ( ~ l3_lattices(X661)
| ~ v10_lattices(X661)
| v3_struct_0(X661)
| ~ m1_filter_0(X662,X661)
| m1_subset_1(X662,k1_zfmisc_1(u1_struct_0(X661))) )
& ( ~ l3_lattices(X661)
| ~ v10_lattices(X661)
| v3_struct_0(X661)
| ~ m1_filter_0(X662,X661)
| ~ v1_xboole_0(X662) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_39])])])])]) ).
fof(c_0_52,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_lattice4(X2,X1)
& ~ v1_xboole_0(X2) )
=> ( u1_lattices(k23_filter_2(X1,X2)) = k1_realset1(u1_lattices(X1),X2)
& u2_lattices(k23_filter_2(X1,X2)) = k1_realset1(u2_lattices(X1),X2)
& u1_struct_0(k23_filter_2(X1,X2)) = X2 ) ) ),
inference(fof_simplification,[status(thm)],[t73_filter_2]) ).
cnf(c_0_53,plain,
( ~ l3_lattices(X1)
| ~ v14_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_filter_0(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| r2_hidden(k6_lattices(X1),X2)
| v3_struct_0(X1)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
fof(c_0_54,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( v17_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v16_lattices(X1)
& v15_lattices(X1)
& v14_lattices(X1)
& v13_lattices(X1)
& v11_lattices(X1)
& ~ v3_struct_0(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc5_lattices]) ).
fof(c_0_55,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> m1_filter_0(u1_struct_0(X1),X1) ),
inference(fof_simplification,[status(thm)],[t15_filter_0]) ).
fof(c_0_56,plain,
! [X1,X2] :
( ( v1_xboole_0(X1)
=> ( m1_subset_1(X2,X1)
<=> v1_xboole_0(X2) ) )
& ( ~ v1_xboole_0(X1)
=> ( m1_subset_1(X2,X1)
<=> r2_hidden(X2,X1) ) ) ),
inference(fof_simplification,[status(thm)],[d2_subset_1]) ).
fof(c_0_57,plain,
! [X199,X200] :
( ( ~ l3_lattices(X199)
| ~ v10_lattices(X199)
| v3_struct_0(X199)
| ~ m2_filter_2(X200,X199)
| m2_lattice4(X200,X199) )
& ( ~ l3_lattices(X199)
| ~ v10_lattices(X199)
| v3_struct_0(X199)
| ~ m2_filter_2(X200,X199)
| ~ v1_xboole_0(X200) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_41])])])])]) ).
cnf(c_0_58,plain,
( ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| m2_filter_2(k18_filter_2(X1,X2),X1)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
fof(c_0_59,plain,
! [X460,X461] :
( r2_hidden(k5_lattices(X460),X461)
| ~ v13_lattices(X460)
| ~ m2_filter_2(X461,X460)
| ~ l3_lattices(X460)
| ~ v10_lattices(X460)
| v3_struct_0(X460) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_43])])])]) ).
fof(c_0_60,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m2_nat_lat(X2,X1)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X2))
=> m1_subset_1(X3,u1_struct_0(X1)) ) ) ),
inference(fof_simplification,[status(thm)],[t69_filter_2]) ).
fof(c_0_61,plain,
! [X56,X57] :
( m2_nat_lat(k23_filter_2(X56,X57),X56)
| ~ m2_lattice4(X57,X56)
| v1_xboole_0(X57)
| ~ l3_lattices(X56)
| ~ v10_lattices(X56)
| v3_struct_0(X56) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_44])])]) ).
cnf(c_0_62,plain,
( ~ m1_filter_0(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| m2_lattice4(X2,X1)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
cnf(c_0_63,negated_conjecture,
m1_filter_0(k2_filter_0(esk1_0,esk3_0),esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_47]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_64,plain,
( ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| ~ m1_filter_0(X1,X2)
| ~ v1_xboole_0(X1)
| v3_struct_0(X2) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
fof(c_0_65,plain,
! [X67,X68] :
( ( ~ l3_lattices(X67)
| ~ v10_lattices(X67)
| v3_struct_0(X67)
| ~ m2_lattice4(X68,X67)
| v1_xboole_0(X68)
| u1_lattices(k23_filter_2(X67,X68)) = k1_realset1(u1_lattices(X67),X68) )
& ( ~ l3_lattices(X67)
| ~ v10_lattices(X67)
| v3_struct_0(X67)
| ~ m2_lattice4(X68,X67)
| v1_xboole_0(X68)
| u2_lattices(k23_filter_2(X67,X68)) = k1_realset1(u2_lattices(X67),X68) )
& ( ~ l3_lattices(X67)
| ~ v10_lattices(X67)
| v3_struct_0(X67)
| ~ m2_lattice4(X68,X67)
| v1_xboole_0(X68)
| u1_struct_0(k23_filter_2(X67,X68)) = X68 ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_52])])])])]) ).
cnf(c_0_66,plain,
( ~ m1_filter_0(X2,X1)
| ~ v14_lattices(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| r2_hidden(k6_lattices(X1),X2)
| v3_struct_0(X1) ),
inference(cn,[status(thm)],[c_0_53]) ).
fof(c_0_67,plain,
! [X565] :
( ( ~ l3_lattices(X565)
| ~ v17_lattices(X565)
| v3_struct_0(X565)
| v16_lattices(X565) )
& ( ~ l3_lattices(X565)
| ~ v17_lattices(X565)
| v3_struct_0(X565)
| v15_lattices(X565) )
& ( ~ l3_lattices(X565)
| ~ v17_lattices(X565)
| v3_struct_0(X565)
| v14_lattices(X565) )
& ( ~ l3_lattices(X565)
| ~ v17_lattices(X565)
| v3_struct_0(X565)
| v13_lattices(X565) )
& ( ~ l3_lattices(X565)
| ~ v17_lattices(X565)
| v3_struct_0(X565)
| v11_lattices(X565) )
& ( ~ l3_lattices(X565)
| ~ v17_lattices(X565)
| v3_struct_0(X565)
| ~ v3_struct_0(X565) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_54])])])]) ).
fof(c_0_68,plain,
! [X660] :
( m1_filter_0(u1_struct_0(X660),X660)
| ~ l3_lattices(X660)
| ~ v10_lattices(X660)
| v3_struct_0(X660) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_55])])]) ).
fof(c_0_69,plain,
! [X228,X229] :
( ( ~ v1_xboole_0(X228)
| m1_subset_1(X229,X228)
| ~ v1_xboole_0(X229) )
& ( ~ v1_xboole_0(X228)
| v1_xboole_0(X229)
| ~ m1_subset_1(X229,X228) )
& ( v1_xboole_0(X228)
| m1_subset_1(X229,X228)
| ~ r2_hidden(X229,X228) )
& ( v1_xboole_0(X228)
| r2_hidden(X229,X228)
| ~ m1_subset_1(X229,X228) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_56])])])]) ).
cnf(c_0_70,plain,
( ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| ~ m2_filter_2(X1,X2)
| v3_struct_0(X2)
| m2_lattice4(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
cnf(c_0_71,negated_conjecture,
m2_filter_2(k18_filter_2(esk1_0,esk3_0),esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58,c_0_47]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_72,plain,
( ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| ~ m2_filter_2(X1,X2)
| ~ v1_xboole_0(X1)
| v3_struct_0(X2) ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
cnf(c_0_73,plain,
( ~ v13_lattices(X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| r2_hidden(k5_lattices(X1),X2)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
fof(c_0_74,plain,
! [X181,X182,X183] :
( m1_subset_1(X183,u1_struct_0(X181))
| ~ m1_subset_1(X183,u1_struct_0(X182))
| ~ m2_nat_lat(X182,X181)
| ~ l3_lattices(X181)
| ~ v10_lattices(X181)
| v3_struct_0(X181) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_60])])])]) ).
cnf(c_0_75,plain,
( ~ m2_lattice4(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| m2_nat_lat(k23_filter_2(X1,X2),X1)
| v1_xboole_0(X2)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
cnf(c_0_76,negated_conjecture,
m2_lattice4(k2_filter_0(esk1_0,esk3_0),esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_63]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_77,negated_conjecture,
~ v1_xboole_0(k2_filter_0(esk1_0,esk3_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64,c_0_63]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_78,plain,
( ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_lattice4(X2,X1)
| v3_struct_0(X1)
| v1_xboole_0(X2)
| u1_struct_0(k23_filter_2(X1,X2)) = X2 ),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
fof(c_0_79,plain,
! [X598,X599] :
( m1_subset_1(X598,X599)
| ~ r2_hidden(X598,X599) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t1_subset])])]) ).
cnf(c_0_80,negated_conjecture,
( ~ v14_lattices(esk1_0)
| r2_hidden(k6_lattices(esk1_0),k2_filter_0(esk1_0,esk3_0)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_63]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_81,plain,
( ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| v3_struct_0(X1)
| v14_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_82,negated_conjecture,
v17_lattices(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_83,plain,
( ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| m1_filter_0(u1_struct_0(X1),X1)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
cnf(c_0_84,plain,
( ~ m1_subset_1(X1,X2)
| v1_xboole_0(X2)
| r2_hidden(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_69]) ).
cnf(c_0_85,negated_conjecture,
m2_lattice4(k18_filter_2(esk1_0,esk3_0),esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70,c_0_71]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_86,negated_conjecture,
~ v1_xboole_0(k18_filter_2(esk1_0,esk3_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_71]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_87,negated_conjecture,
( ~ v13_lattices(esk1_0)
| r2_hidden(k5_lattices(esk1_0),k18_filter_2(esk1_0,esk3_0)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_71]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_88,plain,
( ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| v3_struct_0(X1)
| v13_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
fof(c_0_89,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( ( l3_lattices(X1)
& v14_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> m1_filter_0(k6_domain_1(u1_struct_0(X1),k6_lattices(X1)),X1) ) ),
inference(fof_simplification,[status(thm)],[t13_filter_0]) ).
fof(c_0_90,plain,
! [X1,X2] :
( ( m1_subset_1(X2,X1)
& ~ v1_xboole_0(X1) )
=> k6_domain_1(X1,X2) = k1_tarski(X2) ),
inference(fof_simplification,[status(thm)],[redefinition_k6_domain_1]) ).
cnf(c_0_91,plain,
( ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m2_nat_lat(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| m1_subset_1(X3,u1_struct_0(X1))
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_74]) ).
cnf(c_0_92,negated_conjecture,
m2_nat_lat(k23_filter_2(esk1_0,k2_filter_0(esk1_0,esk3_0)),esk1_0),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_76]),c_0_48]),c_0_49])]),c_0_50]),c_0_77]) ).
cnf(c_0_93,negated_conjecture,
u1_struct_0(k23_filter_2(esk1_0,k2_filter_0(esk1_0,esk3_0))) = k2_filter_0(esk1_0,esk3_0),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_78,c_0_76]),c_0_48]),c_0_49])]),c_0_50]),c_0_77]) ).
cnf(c_0_94,plain,
( ~ r2_hidden(X1,X2)
| m1_subset_1(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_79]) ).
cnf(c_0_95,negated_conjecture,
r2_hidden(k6_lattices(esk1_0),k2_filter_0(esk1_0,esk3_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80,c_0_81]),c_0_82]),c_0_49])]),c_0_50]) ).
fof(c_0_96,plain,
! [X219,X220] :
( ~ v1_xboole_0(X220)
| ~ r2_hidden(X219,X220) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t7_boole])])]) ).
cnf(c_0_97,plain,
( ~ v1_xboole_0(u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v3_struct_0(X1) ),
inference(spm,[status(thm)],[c_0_64,c_0_83]) ).
cnf(c_0_98,negated_conjecture,
( r2_hidden(esk3_0,u1_struct_0(esk1_0))
| v1_xboole_0(u1_struct_0(esk1_0)) ),
inference(spm,[status(thm)],[c_0_84,c_0_47]) ).
cnf(c_0_99,negated_conjecture,
m2_nat_lat(k23_filter_2(esk1_0,k18_filter_2(esk1_0,esk3_0)),esk1_0),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_85]),c_0_48]),c_0_49])]),c_0_50]),c_0_86]) ).
cnf(c_0_100,negated_conjecture,
u1_struct_0(k23_filter_2(esk1_0,k18_filter_2(esk1_0,esk3_0))) = k18_filter_2(esk1_0,esk3_0),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_78,c_0_85]),c_0_48]),c_0_49])]),c_0_50]),c_0_86]) ).
cnf(c_0_101,negated_conjecture,
r2_hidden(k5_lattices(esk1_0),k18_filter_2(esk1_0,esk3_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87,c_0_88]),c_0_82]),c_0_49])]),c_0_50]) ).
fof(c_0_102,plain,
! [X501] :
( m1_filter_0(k6_domain_1(u1_struct_0(X501),k6_lattices(X501)),X501)
| ~ l3_lattices(X501)
| ~ v14_lattices(X501)
| ~ v10_lattices(X501)
| v3_struct_0(X501)
| ~ l3_lattices(X501)
| ~ v10_lattices(X501)
| v3_struct_0(X501) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_89])])]) ).
fof(c_0_103,plain,
! [X645,X646] :
( k6_domain_1(X645,X646) = k1_tarski(X646)
| ~ m1_subset_1(X646,X645)
| v1_xboole_0(X645) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_90])])]) ).
cnf(c_0_104,negated_conjecture,
( ~ m1_subset_1(X1,k2_filter_0(esk1_0,esk3_0))
| m1_subset_1(X1,u1_struct_0(esk1_0)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91,c_0_92]),c_0_48]),c_0_49]),c_0_93])]),c_0_50]) ).
cnf(c_0_105,negated_conjecture,
m1_subset_1(k6_lattices(esk1_0),k2_filter_0(esk1_0,esk3_0)),
inference(spm,[status(thm)],[c_0_94,c_0_95]) ).
cnf(c_0_106,plain,
( ~ v1_xboole_0(X2)
| ~ r2_hidden(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_96]) ).
cnf(c_0_107,negated_conjecture,
r2_hidden(esk3_0,u1_struct_0(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_98]),c_0_48]),c_0_49])]),c_0_50]) ).
fof(c_0_108,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v13_lattices(X1)
=> m2_filter_2(k6_domain_1(u1_struct_0(X1),k5_lattices(X1)),X1) ) ),
inference(fof_simplification,[status(thm)],[t26_filter_2]) ).
cnf(c_0_109,negated_conjecture,
( ~ m1_subset_1(X1,k18_filter_2(esk1_0,esk3_0))
| m1_subset_1(X1,u1_struct_0(esk1_0)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91,c_0_99]),c_0_48]),c_0_49]),c_0_100])]),c_0_50]) ).
cnf(c_0_110,negated_conjecture,
m1_subset_1(k5_lattices(esk1_0),k18_filter_2(esk1_0,esk3_0)),
inference(spm,[status(thm)],[c_0_94,c_0_101]) ).
fof(c_0_111,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( m1_filter_0(k6_domain_1(u1_struct_0(X1),X2),X1)
=> v14_lattices(X1) ) ) ),
inference(fof_simplification,[status(thm)],[t14_filter_0]) ).
cnf(c_0_112,plain,
( ~ l3_lattices(X1)
| ~ v14_lattices(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| m1_filter_0(k6_domain_1(u1_struct_0(X1),k6_lattices(X1)),X1)
| v3_struct_0(X1)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_102]) ).
cnf(c_0_113,plain,
( ~ m1_subset_1(X2,X1)
| k6_domain_1(X1,X2) = k1_tarski(X2)
| v1_xboole_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_103]) ).
cnf(c_0_114,negated_conjecture,
m1_subset_1(k6_lattices(esk1_0),u1_struct_0(esk1_0)),
inference(spm,[status(thm)],[c_0_104,c_0_105]) ).
cnf(c_0_115,negated_conjecture,
~ v1_xboole_0(u1_struct_0(esk1_0)),
inference(spm,[status(thm)],[c_0_106,c_0_107]) ).
fof(c_0_116,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( m2_filter_2(k6_domain_1(u1_struct_0(X1),X2),X1)
=> v13_lattices(X1) ) ) ),
inference(fof_simplification,[status(thm)],[t27_filter_2]) ).
fof(c_0_117,plain,
! [X462] :
( m2_filter_2(k6_domain_1(u1_struct_0(X462),k5_lattices(X462)),X462)
| ~ v13_lattices(X462)
| ~ l3_lattices(X462)
| ~ v10_lattices(X462)
| v3_struct_0(X462) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_108])])]) ).
cnf(c_0_118,negated_conjecture,
m1_subset_1(k5_lattices(esk1_0),u1_struct_0(esk1_0)),
inference(spm,[status(thm)],[c_0_109,c_0_110]) ).
fof(c_0_119,plain,
! [X502,X503] :
( v14_lattices(X502)
| ~ m1_filter_0(k6_domain_1(u1_struct_0(X502),X503),X502)
| ~ m1_subset_1(X503,u1_struct_0(X502))
| ~ l3_lattices(X502)
| ~ v10_lattices(X502)
| v3_struct_0(X502) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_111])])])]) ).
cnf(c_0_120,plain,
( ~ v14_lattices(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| m1_filter_0(k6_domain_1(u1_struct_0(X1),k6_lattices(X1)),X1)
| v3_struct_0(X1) ),
inference(cn,[status(thm)],[c_0_112]) ).
cnf(c_0_121,negated_conjecture,
k6_domain_1(u1_struct_0(esk1_0),k6_lattices(esk1_0)) = k1_tarski(k6_lattices(esk1_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_113,c_0_114]),c_0_115]) ).
fof(c_0_122,plain,
! [X463,X464] :
( v13_lattices(X463)
| ~ m2_filter_2(k6_domain_1(u1_struct_0(X463),X464),X463)
| ~ m1_subset_1(X464,u1_struct_0(X463))
| ~ l3_lattices(X463)
| ~ v10_lattices(X463)
| v3_struct_0(X463) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_116])])])]) ).
cnf(c_0_123,plain,
( ~ v13_lattices(X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| m2_filter_2(k6_domain_1(u1_struct_0(X1),k5_lattices(X1)),X1)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_117]) ).
cnf(c_0_124,negated_conjecture,
k6_domain_1(u1_struct_0(esk1_0),k5_lattices(esk1_0)) = k1_tarski(k5_lattices(esk1_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_113,c_0_118]),c_0_115]) ).
fof(c_0_125,plain,
! [X1,X2,X3] :
( ( m1_subset_1(X3,u1_struct_0(X1))
& m1_subset_1(X2,u1_struct_0(X1))
& l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( m2_lattice4(k22_filter_2(X1,X2,X3),X1)
& ~ v1_xboole_0(k22_filter_2(X1,X2,X3)) ) ),
inference(fof_simplification,[status(thm)],[dt_k22_filter_2]) ).
fof(c_0_126,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( ( r3_lattices(X1,X2,X3)
& v12_lattices(X1)
& l3_lattices(X1)
& v16_lattices(X1)
& v15_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( l3_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v16_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v15_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& v10_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
& ~ v3_struct_0(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[t86_filter_2]) ).
fof(c_0_127,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( v14_lattices(X1)
& v13_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v15_lattices(X1)
& ~ v3_struct_0(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc3_lattices]) ).
cnf(c_0_128,plain,
( ~ m1_filter_0(k6_domain_1(u1_struct_0(X1),X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v14_lattices(X1)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_119]) ).
cnf(c_0_129,negated_conjecture,
( ~ v14_lattices(esk1_0)
| m1_filter_0(k1_tarski(k6_lattices(esk1_0)),esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120,c_0_121]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_130,plain,
( ~ m2_filter_2(k6_domain_1(u1_struct_0(X1),X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v13_lattices(X1)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_122]) ).
cnf(c_0_131,negated_conjecture,
( ~ v13_lattices(esk1_0)
| m2_filter_2(k1_tarski(k5_lattices(esk1_0)),esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123,c_0_124]),c_0_48]),c_0_49])]),c_0_50]) ).
fof(c_0_132,plain,
! [X97,X98,X99] :
( ( ~ m1_subset_1(X99,u1_struct_0(X97))
| ~ m1_subset_1(X98,u1_struct_0(X97))
| ~ l3_lattices(X97)
| ~ v10_lattices(X97)
| v3_struct_0(X97)
| m2_lattice4(k22_filter_2(X97,X98,X99),X97) )
& ( ~ m1_subset_1(X99,u1_struct_0(X97))
| ~ m1_subset_1(X98,u1_struct_0(X97))
| ~ l3_lattices(X97)
| ~ v10_lattices(X97)
| v3_struct_0(X97)
| ~ v1_xboole_0(k22_filter_2(X97,X98,X99)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_125])])])]) ).
fof(c_0_133,plain,
! [X117,X118,X119] :
( ( ~ l3_lattices(X117)
| ~ v10_lattices(X117)
| v3_struct_0(X117)
| ~ m1_subset_1(X118,u1_struct_0(X117))
| ~ m1_subset_1(X119,u1_struct_0(X117))
| ~ r3_lattices(X117,X118,X119)
| ~ v12_lattices(X117)
| ~ l3_lattices(X117)
| ~ v16_lattices(X117)
| ~ v15_lattices(X117)
| ~ v10_lattices(X117)
| v3_struct_0(X117)
| l3_lattices(k23_filter_2(X117,k22_filter_2(X117,X118,X119))) )
& ( ~ l3_lattices(X117)
| ~ v10_lattices(X117)
| v3_struct_0(X117)
| ~ m1_subset_1(X118,u1_struct_0(X117))
| ~ m1_subset_1(X119,u1_struct_0(X117))
| ~ r3_lattices(X117,X118,X119)
| ~ v12_lattices(X117)
| ~ l3_lattices(X117)
| ~ v16_lattices(X117)
| ~ v15_lattices(X117)
| ~ v10_lattices(X117)
| v3_struct_0(X117)
| v16_lattices(k23_filter_2(X117,k22_filter_2(X117,X118,X119))) )
& ( ~ l3_lattices(X117)
| ~ v10_lattices(X117)
| v3_struct_0(X117)
| ~ m1_subset_1(X118,u1_struct_0(X117))
| ~ m1_subset_1(X119,u1_struct_0(X117))
| ~ r3_lattices(X117,X118,X119)
| ~ v12_lattices(X117)
| ~ l3_lattices(X117)
| ~ v16_lattices(X117)
| ~ v15_lattices(X117)
| ~ v10_lattices(X117)
| v3_struct_0(X117)
| v15_lattices(k23_filter_2(X117,k22_filter_2(X117,X118,X119))) )
& ( ~ l3_lattices(X117)
| ~ v10_lattices(X117)
| v3_struct_0(X117)
| ~ m1_subset_1(X118,u1_struct_0(X117))
| ~ m1_subset_1(X119,u1_struct_0(X117))
| ~ r3_lattices(X117,X118,X119)
| ~ v12_lattices(X117)
| ~ l3_lattices(X117)
| ~ v16_lattices(X117)
| ~ v15_lattices(X117)
| ~ v10_lattices(X117)
| v3_struct_0(X117)
| v10_lattices(k23_filter_2(X117,k22_filter_2(X117,X118,X119))) )
& ( ~ l3_lattices(X117)
| ~ v10_lattices(X117)
| v3_struct_0(X117)
| ~ m1_subset_1(X118,u1_struct_0(X117))
| ~ m1_subset_1(X119,u1_struct_0(X117))
| ~ r3_lattices(X117,X118,X119)
| ~ v12_lattices(X117)
| ~ l3_lattices(X117)
| ~ v16_lattices(X117)
| ~ v15_lattices(X117)
| ~ v10_lattices(X117)
| v3_struct_0(X117)
| ~ v3_struct_0(k23_filter_2(X117,k22_filter_2(X117,X118,X119))) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_126])])])])]) ).
fof(c_0_134,plain,
! [X561] :
( ( ~ l3_lattices(X561)
| ~ v14_lattices(X561)
| ~ v13_lattices(X561)
| v3_struct_0(X561)
| v15_lattices(X561) )
& ( ~ l3_lattices(X561)
| ~ v14_lattices(X561)
| ~ v13_lattices(X561)
| v3_struct_0(X561)
| ~ v3_struct_0(X561) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_127])])])]) ).
cnf(c_0_135,negated_conjecture,
( ~ m1_filter_0(k1_tarski(k6_lattices(esk1_0)),esk1_0)
| v14_lattices(esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_128,c_0_121]),c_0_48]),c_0_49]),c_0_114])]),c_0_50]) ).
cnf(c_0_136,negated_conjecture,
m1_filter_0(k1_tarski(k6_lattices(esk1_0)),esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_129,c_0_81]),c_0_82]),c_0_49])]),c_0_50]) ).
cnf(c_0_137,negated_conjecture,
( ~ m2_filter_2(k1_tarski(k5_lattices(esk1_0)),esk1_0)
| v13_lattices(esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_124]),c_0_48]),c_0_49]),c_0_118])]),c_0_50]) ).
cnf(c_0_138,negated_conjecture,
m2_filter_2(k1_tarski(k5_lattices(esk1_0)),esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_131,c_0_88]),c_0_82]),c_0_49])]),c_0_50]) ).
fof(c_0_139,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( r3_lattices(X1,X2,X3)
=> ( r2_hidden(X3,k22_filter_2(X1,X2,X3))
& r2_hidden(X2,k22_filter_2(X1,X2,X3)) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[t64_filter_2]) ).
cnf(c_0_140,plain,
( ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v3_struct_0(X1)
| m2_lattice4(k22_filter_2(X1,X2,X3),X1) ),
inference(split_conjunct,[status(thm)],[c_0_132]) ).
cnf(c_0_141,plain,
( ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ r3_lattices(X1,X2,X3)
| ~ v12_lattices(X1)
| ~ l3_lattices(X1)
| ~ v16_lattices(X1)
| ~ v15_lattices(X1)
| ~ v10_lattices(X1)
| v3_struct_0(X1)
| v3_struct_0(X1)
| v16_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) ),
inference(split_conjunct,[status(thm)],[c_0_133]) ).
cnf(c_0_142,plain,
( ~ l3_lattices(X1)
| ~ v14_lattices(X1)
| ~ v13_lattices(X1)
| v3_struct_0(X1)
| v15_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_134]) ).
cnf(c_0_143,negated_conjecture,
v14_lattices(esk1_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_135,c_0_136])]) ).
cnf(c_0_144,negated_conjecture,
v13_lattices(esk1_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_137,c_0_138])]) ).
fof(c_0_145,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( v11_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v12_lattices(X1)
& v10_lattices(X1)
& v9_lattices(X1)
& v8_lattices(X1)
& v7_lattices(X1)
& v6_lattices(X1)
& v5_lattices(X1)
& v4_lattices(X1)
& ~ v3_struct_0(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc7_lattices]) ).
fof(c_0_146,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_lattice4(X2,X1)
& ~ v1_xboole_0(X2) )
=> ( v11_lattices(X1)
=> v11_lattices(k23_filter_2(X1,X2)) ) ) ),
inference(fof_simplification,[status(thm)],[t78_filter_2]) ).
fof(c_0_147,plain,
! [X104,X105,X106] :
( ( ~ l3_lattices(X104)
| ~ v10_lattices(X104)
| v3_struct_0(X104)
| ~ m1_subset_1(X105,u1_struct_0(X104))
| ~ m1_subset_1(X106,u1_struct_0(X104))
| ~ r3_lattices(X104,X105,X106)
| r2_hidden(X106,k22_filter_2(X104,X105,X106)) )
& ( ~ l3_lattices(X104)
| ~ v10_lattices(X104)
| v3_struct_0(X104)
| ~ m1_subset_1(X105,u1_struct_0(X104))
| ~ m1_subset_1(X106,u1_struct_0(X104))
| ~ r3_lattices(X104,X105,X106)
| r2_hidden(X105,k22_filter_2(X104,X105,X106)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_139])])])])]) ).
fof(c_0_148,plain,
! [X1,X2] :
( ( m2_lattice4(X2,X1)
& ~ v1_xboole_0(X2)
& l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v10_lattices(k23_filter_2(X1,X2))
& v9_lattices(k23_filter_2(X1,X2))
& v8_lattices(k23_filter_2(X1,X2))
& v7_lattices(k23_filter_2(X1,X2))
& v6_lattices(k23_filter_2(X1,X2))
& v5_lattices(k23_filter_2(X1,X2))
& v4_lattices(k23_filter_2(X1,X2))
& v3_lattices(k23_filter_2(X1,X2))
& ~ v3_struct_0(k23_filter_2(X1,X2)) ) ),
inference(fof_simplification,[status(thm)],[fc5_filter_2]) ).
fof(c_0_149,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m2_nat_lat(X2,X1)
=> ( l3_lattices(X2)
& v10_lattices(X2)
& ~ v3_struct_0(X2) ) ) ),
inference(fof_simplification,[status(thm)],[dt_m2_nat_lat]) ).
cnf(c_0_150,negated_conjecture,
( ~ m1_subset_1(X1,u1_struct_0(esk1_0))
| m2_lattice4(k22_filter_2(esk1_0,X1,esk3_0),esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_140,c_0_47]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_151,negated_conjecture,
m1_subset_1(esk2_0,u1_struct_0(esk1_0)),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_152,plain,
( ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ r3_lattices(X1,X2,X3)
| ~ v16_lattices(X1)
| ~ v15_lattices(X1)
| ~ v12_lattices(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v16_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3)))
| v3_struct_0(X1) ),
inference(cn,[status(thm)],[c_0_141]) ).
cnf(c_0_153,negated_conjecture,
r3_lattices(esk1_0,esk2_0,esk3_0),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_154,negated_conjecture,
v15_lattices(esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_142,c_0_143]),c_0_144]),c_0_49])]),c_0_50]) ).
fof(c_0_155,plain,
! [X467] :
( ( ~ l3_lattices(X467)
| ~ v11_lattices(X467)
| ~ v10_lattices(X467)
| v3_struct_0(X467)
| v12_lattices(X467) )
& ( ~ l3_lattices(X467)
| ~ v11_lattices(X467)
| ~ v10_lattices(X467)
| v3_struct_0(X467)
| v10_lattices(X467) )
& ( ~ l3_lattices(X467)
| ~ v11_lattices(X467)
| ~ v10_lattices(X467)
| v3_struct_0(X467)
| v9_lattices(X467) )
& ( ~ l3_lattices(X467)
| ~ v11_lattices(X467)
| ~ v10_lattices(X467)
| v3_struct_0(X467)
| v8_lattices(X467) )
& ( ~ l3_lattices(X467)
| ~ v11_lattices(X467)
| ~ v10_lattices(X467)
| v3_struct_0(X467)
| v7_lattices(X467) )
& ( ~ l3_lattices(X467)
| ~ v11_lattices(X467)
| ~ v10_lattices(X467)
| v3_struct_0(X467)
| v6_lattices(X467) )
& ( ~ l3_lattices(X467)
| ~ v11_lattices(X467)
| ~ v10_lattices(X467)
| v3_struct_0(X467)
| v5_lattices(X467) )
& ( ~ l3_lattices(X467)
| ~ v11_lattices(X467)
| ~ v10_lattices(X467)
| v3_struct_0(X467)
| v4_lattices(X467) )
& ( ~ l3_lattices(X467)
| ~ v11_lattices(X467)
| ~ v10_lattices(X467)
| v3_struct_0(X467)
| ~ v3_struct_0(X467) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_145])])])]) ).
fof(c_0_156,plain,
! [X85,X86] :
( v11_lattices(k23_filter_2(X85,X86))
| ~ v11_lattices(X85)
| ~ m2_lattice4(X86,X85)
| v1_xboole_0(X86)
| ~ l3_lattices(X85)
| ~ v10_lattices(X85)
| v3_struct_0(X85) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_146])])])]) ).
cnf(c_0_157,plain,
( ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ r3_lattices(X2,X3,X1)
| v3_struct_0(X2)
| r2_hidden(X1,k22_filter_2(X2,X3,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_147]) ).
fof(c_0_158,plain,
! [X65,X66] :
( ( ~ m2_lattice4(X66,X65)
| v1_xboole_0(X66)
| ~ l3_lattices(X65)
| ~ v10_lattices(X65)
| v3_struct_0(X65)
| v10_lattices(k23_filter_2(X65,X66)) )
& ( ~ m2_lattice4(X66,X65)
| v1_xboole_0(X66)
| ~ l3_lattices(X65)
| ~ v10_lattices(X65)
| v3_struct_0(X65)
| v9_lattices(k23_filter_2(X65,X66)) )
& ( ~ m2_lattice4(X66,X65)
| v1_xboole_0(X66)
| ~ l3_lattices(X65)
| ~ v10_lattices(X65)
| v3_struct_0(X65)
| v8_lattices(k23_filter_2(X65,X66)) )
& ( ~ m2_lattice4(X66,X65)
| v1_xboole_0(X66)
| ~ l3_lattices(X65)
| ~ v10_lattices(X65)
| v3_struct_0(X65)
| v7_lattices(k23_filter_2(X65,X66)) )
& ( ~ m2_lattice4(X66,X65)
| v1_xboole_0(X66)
| ~ l3_lattices(X65)
| ~ v10_lattices(X65)
| v3_struct_0(X65)
| v6_lattices(k23_filter_2(X65,X66)) )
& ( ~ m2_lattice4(X66,X65)
| v1_xboole_0(X66)
| ~ l3_lattices(X65)
| ~ v10_lattices(X65)
| v3_struct_0(X65)
| v5_lattices(k23_filter_2(X65,X66)) )
& ( ~ m2_lattice4(X66,X65)
| v1_xboole_0(X66)
| ~ l3_lattices(X65)
| ~ v10_lattices(X65)
| v3_struct_0(X65)
| v4_lattices(k23_filter_2(X65,X66)) )
& ( ~ m2_lattice4(X66,X65)
| v1_xboole_0(X66)
| ~ l3_lattices(X65)
| ~ v10_lattices(X65)
| v3_struct_0(X65)
| v3_lattices(k23_filter_2(X65,X66)) )
& ( ~ m2_lattice4(X66,X65)
| v1_xboole_0(X66)
| ~ l3_lattices(X65)
| ~ v10_lattices(X65)
| v3_struct_0(X65)
| ~ v3_struct_0(k23_filter_2(X65,X66)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_148])])])]) ).
fof(c_0_159,plain,
! [X167,X168] :
( ( ~ l3_lattices(X167)
| ~ v10_lattices(X167)
| v3_struct_0(X167)
| ~ m2_nat_lat(X168,X167)
| l3_lattices(X168) )
& ( ~ l3_lattices(X167)
| ~ v10_lattices(X167)
| v3_struct_0(X167)
| ~ m2_nat_lat(X168,X167)
| v10_lattices(X168) )
& ( ~ l3_lattices(X167)
| ~ v10_lattices(X167)
| v3_struct_0(X167)
| ~ m2_nat_lat(X168,X167)
| ~ v3_struct_0(X168) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_149])])])])]) ).
cnf(c_0_160,negated_conjecture,
m2_lattice4(k22_filter_2(esk1_0,esk2_0,esk3_0),esk1_0),
inference(spm,[status(thm)],[c_0_150,c_0_151]) ).
cnf(c_0_161,negated_conjecture,
( ~ v12_lattices(esk1_0)
| ~ v16_lattices(esk1_0)
| v16_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_152,c_0_153]),c_0_154]),c_0_48]),c_0_49]),c_0_47]),c_0_151])]),c_0_50]) ).
cnf(c_0_162,plain,
( ~ l3_lattices(X1)
| ~ v11_lattices(X1)
| ~ v10_lattices(X1)
| v3_struct_0(X1)
| v12_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_155]) ).
fof(c_0_163,plain,
! [X1] :
( ( l3_lattices(X1)
& v10_lattices(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( r3_lattices(X1,X2,X3)
=> ( k5_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) = X2
& k6_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) = X3
& v15_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[t84_filter_2]) ).
cnf(c_0_164,plain,
( ~ v11_lattices(X1)
| ~ m2_lattice4(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v11_lattices(k23_filter_2(X1,X2))
| v1_xboole_0(X2)
| v3_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_156]) ).
cnf(c_0_165,negated_conjecture,
r2_hidden(esk3_0,k22_filter_2(esk1_0,esk2_0,esk3_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_157,c_0_153]),c_0_48]),c_0_49]),c_0_151]),c_0_47])]),c_0_50]) ).
cnf(c_0_166,plain,
( ~ m2_lattice4(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v1_xboole_0(X2)
| v3_struct_0(X1)
| v10_lattices(k23_filter_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_158]) ).
cnf(c_0_167,plain,
( ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| ~ m2_nat_lat(X1,X2)
| v3_struct_0(X2)
| l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_159]) ).
cnf(c_0_168,negated_conjecture,
( v1_xboole_0(k22_filter_2(esk1_0,esk2_0,esk3_0))
| m2_nat_lat(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0)),esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_160]),c_0_48]),c_0_49])]),c_0_50]) ).
fof(c_0_169,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( v16_lattices(X1)
& v15_lattices(X1)
& v11_lattices(X1)
& ~ v3_struct_0(X1) )
=> ( v17_lattices(X1)
& ~ v3_struct_0(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc6_lattices]) ).
cnf(c_0_170,negated_conjecture,
( ~ v11_lattices(esk1_0)
| ~ v16_lattices(esk1_0)
| v16_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_161,c_0_162]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_171,plain,
( ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| v3_struct_0(X1)
| v16_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
fof(c_0_172,plain,
! [X114,X115,X116] :
( ( ~ l3_lattices(X114)
| ~ v10_lattices(X114)
| v3_struct_0(X114)
| ~ m1_subset_1(X115,u1_struct_0(X114))
| ~ m1_subset_1(X116,u1_struct_0(X114))
| ~ r3_lattices(X114,X115,X116)
| k5_lattices(k23_filter_2(X114,k22_filter_2(X114,X115,X116))) = X115 )
& ( ~ l3_lattices(X114)
| ~ v10_lattices(X114)
| v3_struct_0(X114)
| ~ m1_subset_1(X115,u1_struct_0(X114))
| ~ m1_subset_1(X116,u1_struct_0(X114))
| ~ r3_lattices(X114,X115,X116)
| k6_lattices(k23_filter_2(X114,k22_filter_2(X114,X115,X116))) = X116 )
& ( ~ l3_lattices(X114)
| ~ v10_lattices(X114)
| v3_struct_0(X114)
| ~ m1_subset_1(X115,u1_struct_0(X114))
| ~ m1_subset_1(X116,u1_struct_0(X114))
| ~ r3_lattices(X114,X115,X116)
| v15_lattices(k23_filter_2(X114,k22_filter_2(X114,X115,X116))) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_163])])])])]) ).
cnf(c_0_173,negated_conjecture,
( ~ v11_lattices(esk1_0)
| v1_xboole_0(k22_filter_2(esk1_0,esk2_0,esk3_0))
| v11_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_164,c_0_160]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_174,plain,
( ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| v3_struct_0(X1)
| v11_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_175,negated_conjecture,
~ v1_xboole_0(k22_filter_2(esk1_0,esk2_0,esk3_0)),
inference(spm,[status(thm)],[c_0_106,c_0_165]) ).
cnf(c_0_176,negated_conjecture,
( v1_xboole_0(k22_filter_2(esk1_0,esk2_0,esk3_0))
| v10_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_166,c_0_160]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_177,negated_conjecture,
( v1_xboole_0(k22_filter_2(esk1_0,esk2_0,esk3_0))
| l3_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_167,c_0_168]),c_0_48]),c_0_49])]),c_0_50]) ).
fof(c_0_178,plain,
! [X566] :
( ( ~ l3_lattices(X566)
| ~ v16_lattices(X566)
| ~ v15_lattices(X566)
| ~ v11_lattices(X566)
| v3_struct_0(X566)
| v17_lattices(X566) )
& ( ~ l3_lattices(X566)
| ~ v16_lattices(X566)
| ~ v15_lattices(X566)
| ~ v11_lattices(X566)
| v3_struct_0(X566)
| ~ v3_struct_0(X566) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_169])])])]) ).
cnf(c_0_179,negated_conjecture,
( ~ v11_lattices(esk1_0)
| v16_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_170,c_0_171]),c_0_82]),c_0_49])]),c_0_50]) ).
cnf(c_0_180,plain,
( ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ r3_lattices(X1,X2,X3)
| v3_struct_0(X1)
| v15_lattices(k23_filter_2(X1,k22_filter_2(X1,X2,X3))) ),
inference(split_conjunct,[status(thm)],[c_0_172]) ).
cnf(c_0_181,negated_conjecture,
( v1_xboole_0(k22_filter_2(esk1_0,esk2_0,esk3_0))
| v11_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_173,c_0_174]),c_0_82]),c_0_49])]),c_0_50]) ).
cnf(c_0_182,plain,
( ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| ~ m2_nat_lat(X1,X2)
| ~ v3_struct_0(X1)
| v3_struct_0(X2) ),
inference(split_conjunct,[status(thm)],[c_0_159]) ).
cnf(c_0_183,negated_conjecture,
m2_nat_lat(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0)),esk1_0),
inference(sr,[status(thm)],[c_0_168,c_0_175]) ).
cnf(c_0_184,negated_conjecture,
( ~ l3_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0)))
| ~ v17_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0)))
| ~ v10_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0)))
| v3_struct_0(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_185,negated_conjecture,
v10_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))),
inference(sr,[status(thm)],[c_0_176,c_0_175]) ).
cnf(c_0_186,negated_conjecture,
l3_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))),
inference(sr,[status(thm)],[c_0_177,c_0_175]) ).
cnf(c_0_187,plain,
( ~ l3_lattices(X1)
| ~ v16_lattices(X1)
| ~ v15_lattices(X1)
| ~ v11_lattices(X1)
| v3_struct_0(X1)
| v17_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_178]) ).
cnf(c_0_188,negated_conjecture,
v16_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_179,c_0_174]),c_0_82]),c_0_49])]),c_0_50]) ).
cnf(c_0_189,negated_conjecture,
v15_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_180,c_0_153]),c_0_48]),c_0_49]),c_0_47]),c_0_151])]),c_0_50]) ).
cnf(c_0_190,negated_conjecture,
v11_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))),
inference(sr,[status(thm)],[c_0_181,c_0_175]) ).
cnf(c_0_191,negated_conjecture,
~ v3_struct_0(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_182,c_0_183]),c_0_48]),c_0_49])]),c_0_50]) ).
cnf(c_0_192,negated_conjecture,
( ~ v17_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0)))
| v3_struct_0(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_184,c_0_185])]),c_0_186])]) ).
cnf(c_0_193,negated_conjecture,
v17_lattices(k23_filter_2(esk1_0,k22_filter_2(esk1_0,esk2_0,esk3_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_187,c_0_188]),c_0_189]),c_0_190]),c_0_186])]),c_0_191]) ).
cnf(c_0_194,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_192,c_0_193])]),c_0_191]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT337+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/5.45 % Computer : n005.cluster.edu
% 0.17/5.45 % Model : x86_64 x86_64
% 0.17/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.45 % Memory : 8046.5625MB
% 0.17/5.45 % OS : Linux 6.8.0-71-generic
% 0.17/5.45 % CPULimit : 300
% 0.17/5.45 % WCLimit : 300
% 0.17/5.45 % DateTime : Sun Sep 20 23:42:22 UTC 2026
% 0.17/5.45 % CPUTime :
% 0.17/5.45 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/5.52 Running first-order theorem proving
% 0.22/5.52 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.28/13.09 % Version: 3.5.1
% 32.28/13.09 % Preprocessing class: FMLLMLLLSSSNFFN.
% 32.28/13.09 % Scheduled 4 strats onto 8 cores with 297 seconds (2376 total)
% 32.28/13.09 % Starting new_bool_3 with 891s (3) cores
% 32.28/13.09 % Starting new_bool_1 with 891s (3) cores
% 32.28/13.09 % Starting sh5l with 297s (1) cores
% 32.28/13.09 % Starting G-E--_207_C01_F1_SE_CS_SP_PI_S5PRR_S0Y with 297s (1) cores
% 32.28/13.09 % new_bool_1 with pid 2030447 completed with status 0
% 32.28/13.09 % Result found by new_bool_1
% 32.28/13.09 % Preprocessing class: FMLLMLLLSSSNFFN.
% 32.28/13.09 % Scheduled 4 strats onto 8 cores with 297 seconds (2376 total)
% 32.28/13.09 % Starting new_bool_3 with 891s (3) cores
% 32.28/13.09 % Starting new_bool_1 with 891s (3) cores
% 32.28/13.09 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 32.28/13.09 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 32.28/13.09 % Search class: FGHSM-SMLM32-MFFFFFNN
% 32.28/13.09 % Scheduled 13 strats onto 3 cores with 891 seconds (891 total)
% 32.28/13.09 % Starting SubtermCWHack with 81s (1) cores
% 32.28/13.09 % Starting new_bool_1 with 90s (1) cores
% 32.28/13.09 % Starting C12_02_nc_SAT001_MinMin_p005000_rr with 67s (1) cores
% 32.28/13.09 % new_bool_1 with pid 2030452 completed with status 0
% 32.28/13.09 % Result found by new_bool_1
% 32.28/13.09 % Preprocessing class: FMLLMLLLSSSNFFN.
% 32.28/13.09 % Scheduled 4 strats onto 8 cores with 297 seconds (2376 total)
% 32.28/13.09 % Starting new_bool_3 with 891s (3) cores
% 32.28/13.09 % Starting new_bool_1 with 891s (3) cores
% 32.28/13.09 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 32.28/13.09 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 32.28/13.09 % Search class: FGHSM-SMLM32-MFFFFFNN
% 32.28/13.09 % Scheduled 13 strats onto 3 cores with 891 seconds (891 total)
% 32.28/13.09 % Starting SubtermCWHack with 81s (1) cores
% 32.28/13.09 % Starting new_bool_1 with 90s (1) cores
% 32.28/13.09 % Preprocessing time : 0.087 s
% 32.28/13.09 % Presaturation interreduction done
% 32.28/13.09
% 32.28/13.09 % Proof found!
% 32.28/13.09 % SZS status Theorem
% 32.28/13.09 % SZS output start CNFRefutation
% See solution above
% 32.28/13.09 % Parsed axioms : 34760
% 32.28/13.09 % Removed by relevancy pruning/SinE : 33874
% 32.28/13.09 % Initial clauses : 2347
% 32.28/13.09 % Removed in clause preprocessing : 97
% 32.28/13.09 % Initial clauses in saturation : 2250
% 32.28/13.09 % Processed clauses : 14428
% 32.28/13.09 % ...of these trivial : 130
% 32.28/13.09 % ...subsumed : 6329
% 32.28/13.09 % ...remaining for further processing : 7969
% 32.28/13.09 % Other redundant clauses eliminated : 645
% 32.28/13.09 % Clauses deleted for lack of memory : 0
% 32.28/13.09 % Backward-subsumed : 139
% 32.28/13.09 % Backward-rewritten : 259
% 32.28/13.09 % Generated clauses : 103383
% 32.28/13.09 % ...of the previous two non-redundant : 99922
% 32.28/13.09 % ...aggressively subsumed : 0
% 32.28/13.09 % Contextual simplify-reflections : 269
% 32.28/13.09 % Paramodulations : 102729
% 32.28/13.09 % Factorizations : 3
% 32.28/13.09 % NegExts : 0
% 32.28/13.09 % Equation resolutions : 657
% 32.28/13.09 % Disequality decompositions : 0
% 32.28/13.09 % Total rewrite steps : 36750
% 32.28/13.09 % ...of those cached : 35562
% 32.28/13.09 % Propositional unsat checks : 1
% 32.28/13.09 % Propositional check models : 0
% 32.28/13.09 % Propositional check unsatisfiable : 0
% 32.28/13.09 % Propositional clauses : 0
% 32.28/13.09 % Propositional clauses after purity: 0
% 32.28/13.09 % Propositional unsat core size : 0
% 32.28/13.09 % Propositional preprocessing time : 0.000
% 32.28/13.09 % Propositional encoding time : 0.045
% 32.28/13.09 % Propositional solver time : 0.033
% 32.28/13.09 % Success case prop preproc time : 0.000
% 32.28/13.09 % Success case prop encoding time : 0.000
% 32.28/13.09 % Success case prop solver time : 0.000
% 32.28/13.09 % Current number of processed clauses : 5353
% 32.28/13.09 % Positive orientable unit clauses : 1298
% 32.28/13.09 % Positive unorientable unit clauses: 0
% 32.28/13.09 % Negative unit clauses : 791
% 32.28/13.09 % Non-unit-clauses : 3264
% 32.28/13.09 % Current number of unprocessed clauses: 89515
% 32.28/13.09 % ...number of literals in the above : 301571
% 32.28/13.09 % Current number of archived formulas : 0
% 32.28/13.09 % Current number of archived clauses : 2417
% 32.28/13.09 % Clause-clause subsumption calls (NU) : 3548161
% 32.28/13.09 % Rec. Clause-clause subsumption calls : 657641
% 32.28/13.09 % Non-unit clause-clause subsumptions : 2066
% 32.28/13.09 % Unit Clause-clause subsumption calls : 290615
% 32.28/13.09 % Rewrite failures with RHS unbound : 0
% 32.28/13.09 % BW rewrite match attempts : 1216
% 32.28/13.09 % BW rewrite match successes : 126
% 32.28/13.09 % Condensation attempts : 0
% 32.28/13.09 % Condensation successes : 0
% 32.28/13.09 % Termbank termtop insertions : 3157624
% 32.28/13.09 % Search garbage collected termcells : 378774
% 32.28/13.09
% 32.28/13.09 % -------------------------------------------------
% 32.28/13.09 % User time : 4.149 s
% 32.28/13.09 % System time : 0.275 s
% 32.28/13.09 % Total time : 4.424 s
% 32.28/13.09 % Maximum resident set size: 70468 pages
% 32.28/13.09
% 32.28/13.09 % -------------------------------------------------
% 32.28/13.09 % User time : 14.224 s
% 32.28/13.09 % System time : 0.739 s
% 32.28/13.09 % Total time : 14.963 s
% 32.28/13.09 % Maximum resident set size: 57088 pages
% 32.28/13.09 % E exiting
%------------------------------------------------------------------------------