%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : LAT322+1 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art02.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 15:00:47 EST 2010
% Result : Theorem 7.55s
% Output : CNFRefutation 7.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 29
% Syntax : Number of formulae : 368 ( 15 unt; 0 def)
% Number of atoms : 2231 ( 296 equ)
% Maximal formula atoms : 80 ( 6 avg)
% Number of connectives : 3041 (1178 ~;1472 |; 318 &)
% ( 13 <=>; 60 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 2 con; 0-3 aty)
% Number of variables : 442 ( 23 sgn 233 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> k1_filter_0(X1) = u1_struct_0(X1) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',d2_filter_0) ).
fof(2,axiom,
! [X1] :
( l3_lattices(X1)
=> ( l1_lattices(X1)
& l2_lattices(X1) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',dt_l3_lattices) ).
fof(5,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_filter_2(X2,X1)
<=> m1_filter_0(X2,X1) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',redefinition_m1_filter_2) ).
fof(13,axiom,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1)
& m2_filter_2(X2,X1) )
=> m1_filter_2(k15_filter_2(X1,X2),k1_lattice2(X1)) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',dt_k15_filter_2) ).
fof(14,axiom,
! [X1] :
? [X2] : m1_subset_1(X2,X1),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',existence_m1_subset_1) ).
fof(21,axiom,
! [X1] :
( l1_lattices(X1)
=> ( v1_funct_1(u1_lattices(X1))
& v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',dt_u1_lattices) ).
fof(24,axiom,
! [X1,X2,X3] :
( m2_relset_1(X3,X1,X2)
<=> m1_relset_1(X3,X1,X2) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',redefinition_m2_relset_1) ).
fof(25,axiom,
! [X1] :
( l3_lattices(X1)
=> k1_lattice2(X1) = g3_lattices(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1)) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',d2_lattice2) ).
fof(29,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( r2_filter_2(X1,X2)
<=> v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1)) ) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',t33_filter_2) ).
fof(33,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ( ~ v3_struct_0(k1_lattice2(X1))
& v3_lattices(k1_lattice2(X1))
& v4_lattices(k1_lattice2(X1))
& v5_lattices(k1_lattice2(X1))
& v6_lattices(k1_lattice2(X1))
& v7_lattices(k1_lattice2(X1))
& v8_lattices(k1_lattice2(X1))
& v9_lattices(k1_lattice2(X1))
& v10_lattices(k1_lattice2(X1)) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',fc6_lattice2) ).
fof(41,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> k17_filter_2(X1) = u1_struct_0(X1) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',d8_filter_2) ).
fof(45,axiom,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
=> m1_subset_1(k7_filter_2(X1,X2),k1_zfmisc_1(u1_struct_0(k1_lattice2(X1)))) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',dt_k7_filter_2) ).
fof(46,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( ~ v1_xboole_0(X2)
& m2_lattice4(X2,X1) ) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',dt_m2_filter_2) ).
fof(48,axiom,
! [X1,X2,X3] :
~ ( r2_hidden(X1,X2)
& m1_subset_1(X2,k1_zfmisc_1(X3))
& v1_xboole_0(X3) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',t5_subset) ).
fof(50,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( v1_filter_2(X2,X1)
<=> v2_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1)) ) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',t44_filter_2) ).
fof(51,axiom,
! [X1,X2,X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) )
=> ! [X4,X5,X6] :
( g3_lattices(X1,X2,X3) = g3_lattices(X4,X5,X6)
=> ( X1 = X4
& X2 = X5
& X3 = X6 ) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',free_g3_lattices) ).
fof(55,axiom,
! [X1,X2] :
( m1_subset_1(X1,k1_zfmisc_1(X2))
<=> r1_tarski(X1,X2) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',t3_subset) ).
fof(64,axiom,
! [X1] :
( l3_lattices(X1)
=> ( v3_lattices(X1)
=> X1 = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',abstractness_v3_lattices) ).
fof(65,axiom,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1)
& m2_filter_2(X2,X1) )
=> k15_filter_2(X1,X2) = k7_filter_2(X1,X2) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',redefinition_k15_filter_2) ).
fof(67,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& l3_lattices(X1) )
=> ( ~ v3_struct_0(k1_lattice2(X1))
& v3_lattices(k1_lattice2(X1)) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',fc1_lattice2) ).
fof(68,axiom,
! [X1] :
( l3_lattices(X1)
=> ( v3_lattices(k1_lattice2(X1))
& l3_lattices(k1_lattice2(X1)) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',dt_k1_lattice2) ).
fof(75,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ( ~ v3_struct_0(k1_lattice2(X1))
& v3_lattices(k1_lattice2(X1))
& v4_lattices(k1_lattice2(X1))
& v5_lattices(k1_lattice2(X1))
& v6_lattices(k1_lattice2(X1))
& v7_lattices(k1_lattice2(X1))
& v8_lattices(k1_lattice2(X1))
& v9_lattices(k1_lattice2(X1))
& v10_lattices(k1_lattice2(X1))
& v11_lattices(k1_lattice2(X1))
& v12_lattices(k1_lattice2(X1))
& v13_lattices(k1_lattice2(X1))
& v14_lattices(k1_lattice2(X1))
& v15_lattices(k1_lattice2(X1))
& v16_lattices(k1_lattice2(X1))
& v17_lattices(k1_lattice2(X1)) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',fc4_filter_2) ).
fof(77,axiom,
! [X1] :
( l2_lattices(X1)
=> ( v1_funct_1(u2_lattices(X1))
& v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',dt_u2_lattices) ).
fof(90,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> k7_filter_2(X1,X2) = X2 ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',d6_filter_2) ).
fof(91,axiom,
! [X1,X2] :
( m1_subset_1(X1,X2)
=> ( v1_xboole_0(X2)
| r2_hidden(X1,X2) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',t2_subset) ).
fof(93,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_lattice4(X2,X1)
=> m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',dt_m2_lattice4) ).
fof(94,axiom,
! [X1,X2,X3] :
( ( ~ v1_xboole_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) )
=> ( ~ v3_struct_0(g3_lattices(X1,X2,X3))
& v3_lattices(g3_lattices(X1,X2,X3)) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',fc3_lattices) ).
fof(95,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_filter_0(X2,X1)
=> ( ( X2 != k1_filter_0(X1)
& v2_filter_0(X2,X1) )
<=> v1_filter_0(X2,X1) ) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',t58_filter_0) ).
fof(96,conjecture,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( ( X2 != k17_filter_2(X1)
& v1_filter_2(X2,X1) )
<=> r2_filter_2(X1,X2) ) ) ),
file('/tmp/tmpe1_y5v/sel_LAT322+1.p_1',t58_filter_2) ).
fof(100,negated_conjecture,
~ ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( ( X2 != k17_filter_2(X1)
& v1_filter_2(X2,X1) )
<=> r2_filter_2(X1,X2) ) ) ),
inference(assume_negation,[status(cth)],[96]) ).
fof(101,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> k1_filter_0(X1) = u1_struct_0(X1) ),
inference(fof_simplification,[status(thm)],[1,theory(equality)]) ).
fof(102,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_filter_2(X2,X1)
<=> m1_filter_0(X2,X1) ) ),
inference(fof_simplification,[status(thm)],[5,theory(equality)]) ).
fof(108,plain,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1)
& m2_filter_2(X2,X1) )
=> m1_filter_2(k15_filter_2(X1,X2),k1_lattice2(X1)) ),
inference(fof_simplification,[status(thm)],[13,theory(equality)]) ).
fof(113,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( r2_filter_2(X1,X2)
<=> v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1)) ) ) ),
inference(fof_simplification,[status(thm)],[29,theory(equality)]) ).
fof(115,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ( ~ v3_struct_0(k1_lattice2(X1))
& v3_lattices(k1_lattice2(X1))
& v4_lattices(k1_lattice2(X1))
& v5_lattices(k1_lattice2(X1))
& v6_lattices(k1_lattice2(X1))
& v7_lattices(k1_lattice2(X1))
& v8_lattices(k1_lattice2(X1))
& v9_lattices(k1_lattice2(X1))
& v10_lattices(k1_lattice2(X1)) ) ),
inference(fof_simplification,[status(thm)],[33,theory(equality)]) ).
fof(120,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> k17_filter_2(X1) = u1_struct_0(X1) ),
inference(fof_simplification,[status(thm)],[41,theory(equality)]) ).
fof(123,plain,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
=> m1_subset_1(k7_filter_2(X1,X2),k1_zfmisc_1(u1_struct_0(k1_lattice2(X1)))) ),
inference(fof_simplification,[status(thm)],[45,theory(equality)]) ).
fof(124,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( ~ v1_xboole_0(X2)
& m2_lattice4(X2,X1) ) ) ),
inference(fof_simplification,[status(thm)],[46,theory(equality)]) ).
fof(125,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( v1_filter_2(X2,X1)
<=> v2_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1)) ) ) ),
inference(fof_simplification,[status(thm)],[50,theory(equality)]) ).
fof(133,plain,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1)
& m2_filter_2(X2,X1) )
=> k15_filter_2(X1,X2) = k7_filter_2(X1,X2) ),
inference(fof_simplification,[status(thm)],[65,theory(equality)]) ).
fof(135,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& l3_lattices(X1) )
=> ( ~ v3_struct_0(k1_lattice2(X1))
& v3_lattices(k1_lattice2(X1)) ) ),
inference(fof_simplification,[status(thm)],[67,theory(equality)]) ).
fof(141,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ( ~ v3_struct_0(k1_lattice2(X1))
& v3_lattices(k1_lattice2(X1))
& v4_lattices(k1_lattice2(X1))
& v5_lattices(k1_lattice2(X1))
& v6_lattices(k1_lattice2(X1))
& v7_lattices(k1_lattice2(X1))
& v8_lattices(k1_lattice2(X1))
& v9_lattices(k1_lattice2(X1))
& v10_lattices(k1_lattice2(X1))
& v11_lattices(k1_lattice2(X1))
& v12_lattices(k1_lattice2(X1))
& v13_lattices(k1_lattice2(X1))
& v14_lattices(k1_lattice2(X1))
& v15_lattices(k1_lattice2(X1))
& v16_lattices(k1_lattice2(X1))
& v17_lattices(k1_lattice2(X1)) ) ),
inference(fof_simplification,[status(thm)],[75,theory(equality)]) ).
fof(149,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> k7_filter_2(X1,X2) = X2 ) ),
inference(fof_simplification,[status(thm)],[90,theory(equality)]) ).
fof(150,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_lattice4(X2,X1)
=> m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ) ),
inference(fof_simplification,[status(thm)],[93,theory(equality)]) ).
fof(151,plain,
! [X1,X2,X3] :
( ( ~ v1_xboole_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) )
=> ( ~ v3_struct_0(g3_lattices(X1,X2,X3))
& v3_lattices(g3_lattices(X1,X2,X3)) ) ),
inference(fof_simplification,[status(thm)],[94,theory(equality)]) ).
fof(152,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_filter_0(X2,X1)
=> ( ( X2 != k1_filter_0(X1)
& v2_filter_0(X2,X1) )
<=> v1_filter_0(X2,X1) ) ) ),
inference(fof_simplification,[status(thm)],[95,theory(equality)]) ).
fof(153,negated_conjecture,
~ ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( ( X2 != k17_filter_2(X1)
& v1_filter_2(X2,X1) )
<=> r2_filter_2(X1,X2) ) ) ),
inference(fof_simplification,[status(thm)],[100,theory(equality)]) ).
fof(155,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| k1_filter_0(X1) = u1_struct_0(X1) ),
inference(fof_nnf,[status(thm)],[101]) ).
fof(156,plain,
! [X2] :
( v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| k1_filter_0(X2) = u1_struct_0(X2) ),
inference(variable_rename,[status(thm)],[155]) ).
cnf(157,plain,
( k1_filter_0(X1) = u1_struct_0(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(split_conjunct,[status(thm)],[156]) ).
fof(158,plain,
! [X1] :
( ~ l3_lattices(X1)
| ( l1_lattices(X1)
& l2_lattices(X1) ) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(159,plain,
! [X2] :
( ~ l3_lattices(X2)
| ( l1_lattices(X2)
& l2_lattices(X2) ) ),
inference(variable_rename,[status(thm)],[158]) ).
fof(160,plain,
! [X2] :
( ( l1_lattices(X2)
| ~ l3_lattices(X2) )
& ( l2_lattices(X2)
| ~ l3_lattices(X2) ) ),
inference(distribute,[status(thm)],[159]) ).
cnf(161,plain,
( l2_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[160]) ).
cnf(162,plain,
( l1_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[160]) ).
fof(168,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ! [X2] :
( ( ~ m1_filter_2(X2,X1)
| m1_filter_0(X2,X1) )
& ( ~ m1_filter_0(X2,X1)
| m1_filter_2(X2,X1) ) ) ),
inference(fof_nnf,[status(thm)],[102]) ).
fof(169,plain,
! [X3] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ! [X4] :
( ( ~ m1_filter_2(X4,X3)
| m1_filter_0(X4,X3) )
& ( ~ m1_filter_0(X4,X3)
| m1_filter_2(X4,X3) ) ) ),
inference(variable_rename,[status(thm)],[168]) ).
fof(170,plain,
! [X3,X4] :
( ( ( ~ m1_filter_2(X4,X3)
| m1_filter_0(X4,X3) )
& ( ~ m1_filter_0(X4,X3)
| m1_filter_2(X4,X3) ) )
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ),
inference(shift_quantors,[status(thm)],[169]) ).
fof(171,plain,
! [X3,X4] :
( ( ~ m1_filter_2(X4,X3)
| m1_filter_0(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) )
& ( ~ m1_filter_0(X4,X3)
| m1_filter_2(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ) ),
inference(distribute,[status(thm)],[170]) ).
cnf(173,plain,
( v3_struct_0(X1)
| m1_filter_0(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_filter_2(X2,X1) ),
inference(split_conjunct,[status(thm)],[171]) ).
fof(217,plain,
! [X1,X2] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_filter_2(X2,X1)
| m1_filter_2(k15_filter_2(X1,X2),k1_lattice2(X1)) ),
inference(fof_nnf,[status(thm)],[108]) ).
fof(218,plain,
! [X3,X4] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ~ m2_filter_2(X4,X3)
| m1_filter_2(k15_filter_2(X3,X4),k1_lattice2(X3)) ),
inference(variable_rename,[status(thm)],[217]) ).
cnf(219,plain,
( m1_filter_2(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(split_conjunct,[status(thm)],[218]) ).
fof(220,plain,
! [X3] :
? [X4] : m1_subset_1(X4,X3),
inference(variable_rename,[status(thm)],[14]) ).
fof(221,plain,
! [X3] : m1_subset_1(esk5_1(X3),X3),
inference(skolemize,[status(esa)],[220]) ).
cnf(222,plain,
m1_subset_1(esk5_1(X1),X1),
inference(split_conjunct,[status(thm)],[221]) ).
fof(255,plain,
! [X1] :
( ~ l1_lattices(X1)
| ( v1_funct_1(u1_lattices(X1))
& v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
inference(fof_nnf,[status(thm)],[21]) ).
fof(256,plain,
! [X2] :
( ~ l1_lattices(X2)
| ( v1_funct_1(u1_lattices(X2))
& v1_funct_2(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))
& m2_relset_1(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)) ) ),
inference(variable_rename,[status(thm)],[255]) ).
fof(257,plain,
! [X2] :
( ( v1_funct_1(u1_lattices(X2))
| ~ l1_lattices(X2) )
& ( v1_funct_2(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))
| ~ l1_lattices(X2) )
& ( m2_relset_1(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))
| ~ l1_lattices(X2) ) ),
inference(distribute,[status(thm)],[256]) ).
cnf(258,plain,
( m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[257]) ).
cnf(259,plain,
( v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[257]) ).
cnf(260,plain,
( v1_funct_1(u1_lattices(X1))
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[257]) ).
fof(269,plain,
! [X1,X2,X3] :
( ( ~ m2_relset_1(X3,X1,X2)
| m1_relset_1(X3,X1,X2) )
& ( ~ m1_relset_1(X3,X1,X2)
| m2_relset_1(X3,X1,X2) ) ),
inference(fof_nnf,[status(thm)],[24]) ).
fof(270,plain,
! [X4,X5,X6] :
( ( ~ m2_relset_1(X6,X4,X5)
| m1_relset_1(X6,X4,X5) )
& ( ~ m1_relset_1(X6,X4,X5)
| m2_relset_1(X6,X4,X5) ) ),
inference(variable_rename,[status(thm)],[269]) ).
cnf(272,plain,
( m1_relset_1(X1,X2,X3)
| ~ m2_relset_1(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[270]) ).
fof(273,plain,
! [X1] :
( ~ l3_lattices(X1)
| k1_lattice2(X1) = g3_lattices(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1)) ),
inference(fof_nnf,[status(thm)],[25]) ).
fof(274,plain,
! [X2] :
( ~ l3_lattices(X2)
| k1_lattice2(X2) = g3_lattices(u1_struct_0(X2),u1_lattices(X2),u2_lattices(X2)) ),
inference(variable_rename,[status(thm)],[273]) ).
cnf(275,plain,
( k1_lattice2(X1) = g3_lattices(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1))
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[274]) ).
fof(286,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ! [X2] :
( ~ m2_filter_2(X2,X1)
| ( ( ~ r2_filter_2(X1,X2)
| v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1)) )
& ( ~ v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| r2_filter_2(X1,X2) ) ) ) ),
inference(fof_nnf,[status(thm)],[113]) ).
fof(287,plain,
! [X3] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ! [X4] :
( ~ m2_filter_2(X4,X3)
| ( ( ~ r2_filter_2(X3,X4)
| v1_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3)) )
& ( ~ v1_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3))
| r2_filter_2(X3,X4) ) ) ) ),
inference(variable_rename,[status(thm)],[286]) ).
fof(288,plain,
! [X3,X4] :
( ~ m2_filter_2(X4,X3)
| ( ( ~ r2_filter_2(X3,X4)
| v1_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3)) )
& ( ~ v1_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3))
| r2_filter_2(X3,X4) ) )
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ),
inference(shift_quantors,[status(thm)],[287]) ).
fof(289,plain,
! [X3,X4] :
( ( ~ r2_filter_2(X3,X4)
| v1_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3))
| ~ m2_filter_2(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) )
& ( ~ v1_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3))
| r2_filter_2(X3,X4)
| ~ m2_filter_2(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ) ),
inference(distribute,[status(thm)],[288]) ).
cnf(290,plain,
( v3_struct_0(X1)
| r2_filter_2(X1,X2)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_filter_2(X2,X1)
| ~ v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1)) ),
inference(split_conjunct,[status(thm)],[289]) ).
cnf(291,plain,
( v3_struct_0(X1)
| v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_filter_2(X2,X1)
| ~ r2_filter_2(X1,X2) ),
inference(split_conjunct,[status(thm)],[289]) ).
fof(305,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ( ~ v3_struct_0(k1_lattice2(X1))
& v3_lattices(k1_lattice2(X1))
& v4_lattices(k1_lattice2(X1))
& v5_lattices(k1_lattice2(X1))
& v6_lattices(k1_lattice2(X1))
& v7_lattices(k1_lattice2(X1))
& v8_lattices(k1_lattice2(X1))
& v9_lattices(k1_lattice2(X1))
& v10_lattices(k1_lattice2(X1)) ) ),
inference(fof_nnf,[status(thm)],[115]) ).
fof(306,plain,
! [X2] :
( v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| ( ~ v3_struct_0(k1_lattice2(X2))
& v3_lattices(k1_lattice2(X2))
& v4_lattices(k1_lattice2(X2))
& v5_lattices(k1_lattice2(X2))
& v6_lattices(k1_lattice2(X2))
& v7_lattices(k1_lattice2(X2))
& v8_lattices(k1_lattice2(X2))
& v9_lattices(k1_lattice2(X2))
& v10_lattices(k1_lattice2(X2)) ) ),
inference(variable_rename,[status(thm)],[305]) ).
fof(307,plain,
! [X2] :
( ( ~ v3_struct_0(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
& ( v3_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
& ( v4_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
& ( v5_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
& ( v6_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
& ( v7_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
& ( v8_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
& ( v9_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
& ( v10_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) ) ),
inference(distribute,[status(thm)],[306]) ).
cnf(308,plain,
( v3_struct_0(X1)
| v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(split_conjunct,[status(thm)],[307]) ).
fof(348,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| k17_filter_2(X1) = u1_struct_0(X1) ),
inference(fof_nnf,[status(thm)],[120]) ).
fof(349,plain,
! [X2] :
( v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| k17_filter_2(X2) = u1_struct_0(X2) ),
inference(variable_rename,[status(thm)],[348]) ).
cnf(350,plain,
( k17_filter_2(X1) = u1_struct_0(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(split_conjunct,[status(thm)],[349]) ).
fof(372,plain,
! [X1,X2] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| m1_subset_1(k7_filter_2(X1,X2),k1_zfmisc_1(u1_struct_0(k1_lattice2(X1)))) ),
inference(fof_nnf,[status(thm)],[123]) ).
fof(373,plain,
! [X3,X4] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3)))
| m1_subset_1(k7_filter_2(X3,X4),k1_zfmisc_1(u1_struct_0(k1_lattice2(X3)))) ),
inference(variable_rename,[status(thm)],[372]) ).
cnf(374,plain,
( m1_subset_1(k7_filter_2(X1,X2),k1_zfmisc_1(u1_struct_0(k1_lattice2(X1))))
| v3_struct_0(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(split_conjunct,[status(thm)],[373]) ).
fof(375,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ! [X2] :
( ~ m2_filter_2(X2,X1)
| ( ~ v1_xboole_0(X2)
& m2_lattice4(X2,X1) ) ) ),
inference(fof_nnf,[status(thm)],[124]) ).
fof(376,plain,
! [X3] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ! [X4] :
( ~ m2_filter_2(X4,X3)
| ( ~ v1_xboole_0(X4)
& m2_lattice4(X4,X3) ) ) ),
inference(variable_rename,[status(thm)],[375]) ).
fof(377,plain,
! [X3,X4] :
( ~ m2_filter_2(X4,X3)
| ( ~ v1_xboole_0(X4)
& m2_lattice4(X4,X3) )
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ),
inference(shift_quantors,[status(thm)],[376]) ).
fof(378,plain,
! [X3,X4] :
( ( ~ v1_xboole_0(X4)
| ~ m2_filter_2(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) )
& ( m2_lattice4(X4,X3)
| ~ m2_filter_2(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ) ),
inference(distribute,[status(thm)],[377]) ).
cnf(379,plain,
( v3_struct_0(X1)
| m2_lattice4(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_filter_2(X2,X1) ),
inference(split_conjunct,[status(thm)],[378]) ).
cnf(380,plain,
( v3_struct_0(X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_filter_2(X2,X1)
| ~ v1_xboole_0(X2) ),
inference(split_conjunct,[status(thm)],[378]) ).
fof(384,plain,
! [X1,X2,X3] :
( ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X3))
| ~ v1_xboole_0(X3) ),
inference(fof_nnf,[status(thm)],[48]) ).
fof(385,plain,
! [X4,X5,X6] :
( ~ r2_hidden(X4,X5)
| ~ m1_subset_1(X5,k1_zfmisc_1(X6))
| ~ v1_xboole_0(X6) ),
inference(variable_rename,[status(thm)],[384]) ).
cnf(386,plain,
( ~ v1_xboole_0(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ r2_hidden(X3,X2) ),
inference(split_conjunct,[status(thm)],[385]) ).
fof(388,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ! [X2] :
( ~ m2_filter_2(X2,X1)
| ( ( ~ v1_filter_2(X2,X1)
| v2_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1)) )
& ( ~ v2_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v1_filter_2(X2,X1) ) ) ) ),
inference(fof_nnf,[status(thm)],[125]) ).
fof(389,plain,
! [X3] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ! [X4] :
( ~ m2_filter_2(X4,X3)
| ( ( ~ v1_filter_2(X4,X3)
| v2_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3)) )
& ( ~ v2_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3))
| v1_filter_2(X4,X3) ) ) ) ),
inference(variable_rename,[status(thm)],[388]) ).
fof(390,plain,
! [X3,X4] :
( ~ m2_filter_2(X4,X3)
| ( ( ~ v1_filter_2(X4,X3)
| v2_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3)) )
& ( ~ v2_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3))
| v1_filter_2(X4,X3) ) )
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ),
inference(shift_quantors,[status(thm)],[389]) ).
fof(391,plain,
! [X3,X4] :
( ( ~ v1_filter_2(X4,X3)
| v2_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3))
| ~ m2_filter_2(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) )
& ( ~ v2_filter_0(k15_filter_2(X3,X4),k1_lattice2(X3))
| v1_filter_2(X4,X3)
| ~ m2_filter_2(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ) ),
inference(distribute,[status(thm)],[390]) ).
cnf(392,plain,
( v3_struct_0(X1)
| v1_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_filter_2(X2,X1)
| ~ v2_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1)) ),
inference(split_conjunct,[status(thm)],[391]) ).
cnf(393,plain,
( v3_struct_0(X1)
| v2_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_filter_2(X2,X1)
| ~ v1_filter_2(X2,X1) ),
inference(split_conjunct,[status(thm)],[391]) ).
fof(394,plain,
! [X1,X2,X3] :
( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ! [X4,X5,X6] :
( g3_lattices(X1,X2,X3) != g3_lattices(X4,X5,X6)
| ( X1 = X4
& X2 = X5
& X3 = X6 ) ) ),
inference(fof_nnf,[status(thm)],[51]) ).
fof(395,plain,
! [X7,X8,X9] :
( ~ v1_funct_1(X8)
| ~ v1_funct_2(X8,k2_zfmisc_1(X7,X7),X7)
| ~ m1_relset_1(X8,k2_zfmisc_1(X7,X7),X7)
| ~ v1_funct_1(X9)
| ~ v1_funct_2(X9,k2_zfmisc_1(X7,X7),X7)
| ~ m1_relset_1(X9,k2_zfmisc_1(X7,X7),X7)
| ! [X10,X11,X12] :
( g3_lattices(X7,X8,X9) != g3_lattices(X10,X11,X12)
| ( X7 = X10
& X8 = X11
& X9 = X12 ) ) ),
inference(variable_rename,[status(thm)],[394]) ).
fof(396,plain,
! [X7,X8,X9,X10,X11,X12] :
( g3_lattices(X7,X8,X9) != g3_lattices(X10,X11,X12)
| ( X7 = X10
& X8 = X11
& X9 = X12 )
| ~ v1_funct_1(X8)
| ~ v1_funct_2(X8,k2_zfmisc_1(X7,X7),X7)
| ~ m1_relset_1(X8,k2_zfmisc_1(X7,X7),X7)
| ~ v1_funct_1(X9)
| ~ v1_funct_2(X9,k2_zfmisc_1(X7,X7),X7)
| ~ m1_relset_1(X9,k2_zfmisc_1(X7,X7),X7) ),
inference(shift_quantors,[status(thm)],[395]) ).
fof(397,plain,
! [X7,X8,X9,X10,X11,X12] :
( ( X7 = X10
| g3_lattices(X7,X8,X9) != g3_lattices(X10,X11,X12)
| ~ v1_funct_1(X8)
| ~ v1_funct_2(X8,k2_zfmisc_1(X7,X7),X7)
| ~ m1_relset_1(X8,k2_zfmisc_1(X7,X7),X7)
| ~ v1_funct_1(X9)
| ~ v1_funct_2(X9,k2_zfmisc_1(X7,X7),X7)
| ~ m1_relset_1(X9,k2_zfmisc_1(X7,X7),X7) )
& ( X8 = X11
| g3_lattices(X7,X8,X9) != g3_lattices(X10,X11,X12)
| ~ v1_funct_1(X8)
| ~ v1_funct_2(X8,k2_zfmisc_1(X7,X7),X7)
| ~ m1_relset_1(X8,k2_zfmisc_1(X7,X7),X7)
| ~ v1_funct_1(X9)
| ~ v1_funct_2(X9,k2_zfmisc_1(X7,X7),X7)
| ~ m1_relset_1(X9,k2_zfmisc_1(X7,X7),X7) )
& ( X9 = X12
| g3_lattices(X7,X8,X9) != g3_lattices(X10,X11,X12)
| ~ v1_funct_1(X8)
| ~ v1_funct_2(X8,k2_zfmisc_1(X7,X7),X7)
| ~ m1_relset_1(X8,k2_zfmisc_1(X7,X7),X7)
| ~ v1_funct_1(X9)
| ~ v1_funct_2(X9,k2_zfmisc_1(X7,X7),X7)
| ~ m1_relset_1(X9,k2_zfmisc_1(X7,X7),X7) ) ),
inference(distribute,[status(thm)],[396]) ).
cnf(400,plain,
( X2 = X4
| ~ m1_relset_1(X1,k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_2(X1,k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(X3)
| g3_lattices(X2,X3,X1) != g3_lattices(X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[397]) ).
fof(410,plain,
! [X1,X2] :
( ( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| r1_tarski(X1,X2) )
& ( ~ r1_tarski(X1,X2)
| m1_subset_1(X1,k1_zfmisc_1(X2)) ) ),
inference(fof_nnf,[status(thm)],[55]) ).
fof(411,plain,
! [X3,X4] :
( ( ~ m1_subset_1(X3,k1_zfmisc_1(X4))
| r1_tarski(X3,X4) )
& ( ~ r1_tarski(X3,X4)
| m1_subset_1(X3,k1_zfmisc_1(X4)) ) ),
inference(variable_rename,[status(thm)],[410]) ).
cnf(412,plain,
( m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r1_tarski(X1,X2) ),
inference(split_conjunct,[status(thm)],[411]) ).
cnf(413,plain,
( r1_tarski(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(split_conjunct,[status(thm)],[411]) ).
fof(454,plain,
! [X1] :
( ~ l3_lattices(X1)
| ~ v3_lattices(X1)
| X1 = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) ),
inference(fof_nnf,[status(thm)],[64]) ).
fof(455,plain,
! [X2] :
( ~ l3_lattices(X2)
| ~ v3_lattices(X2)
| X2 = g3_lattices(u1_struct_0(X2),u2_lattices(X2),u1_lattices(X2)) ),
inference(variable_rename,[status(thm)],[454]) ).
cnf(456,plain,
( X1 = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ v3_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[455]) ).
fof(457,plain,
! [X1,X2] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_filter_2(X2,X1)
| k15_filter_2(X1,X2) = k7_filter_2(X1,X2) ),
inference(fof_nnf,[status(thm)],[133]) ).
fof(458,plain,
! [X3,X4] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ~ m2_filter_2(X4,X3)
| k15_filter_2(X3,X4) = k7_filter_2(X3,X4) ),
inference(variable_rename,[status(thm)],[457]) ).
cnf(459,plain,
( k15_filter_2(X1,X2) = k7_filter_2(X1,X2)
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(split_conjunct,[status(thm)],[458]) ).
fof(468,plain,
! [X1] :
( v3_struct_0(X1)
| ~ l3_lattices(X1)
| ( ~ v3_struct_0(k1_lattice2(X1))
& v3_lattices(k1_lattice2(X1)) ) ),
inference(fof_nnf,[status(thm)],[135]) ).
fof(469,plain,
! [X2] :
( v3_struct_0(X2)
| ~ l3_lattices(X2)
| ( ~ v3_struct_0(k1_lattice2(X2))
& v3_lattices(k1_lattice2(X2)) ) ),
inference(variable_rename,[status(thm)],[468]) ).
fof(470,plain,
! [X2] :
( ( ~ v3_struct_0(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ l3_lattices(X2) )
& ( v3_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ l3_lattices(X2) ) ),
inference(distribute,[status(thm)],[469]) ).
cnf(472,plain,
( v3_struct_0(X1)
| ~ l3_lattices(X1)
| ~ v3_struct_0(k1_lattice2(X1)) ),
inference(split_conjunct,[status(thm)],[470]) ).
fof(473,plain,
! [X1] :
( ~ l3_lattices(X1)
| ( v3_lattices(k1_lattice2(X1))
& l3_lattices(k1_lattice2(X1)) ) ),
inference(fof_nnf,[status(thm)],[68]) ).
fof(474,plain,
! [X2] :
( ~ l3_lattices(X2)
| ( v3_lattices(k1_lattice2(X2))
& l3_lattices(k1_lattice2(X2)) ) ),
inference(variable_rename,[status(thm)],[473]) ).
fof(475,plain,
! [X2] :
( ( v3_lattices(k1_lattice2(X2))
| ~ l3_lattices(X2) )
& ( l3_lattices(k1_lattice2(X2))
| ~ l3_lattices(X2) ) ),
inference(distribute,[status(thm)],[474]) ).
cnf(476,plain,
( l3_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[475]) ).
cnf(477,plain,
( v3_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[475]) ).
fof(523,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1)
| ( ~ v3_struct_0(k1_lattice2(X1))
& v3_lattices(k1_lattice2(X1))
& v4_lattices(k1_lattice2(X1))
& v5_lattices(k1_lattice2(X1))
& v6_lattices(k1_lattice2(X1))
& v7_lattices(k1_lattice2(X1))
& v8_lattices(k1_lattice2(X1))
& v9_lattices(k1_lattice2(X1))
& v10_lattices(k1_lattice2(X1))
& v11_lattices(k1_lattice2(X1))
& v12_lattices(k1_lattice2(X1))
& v13_lattices(k1_lattice2(X1))
& v14_lattices(k1_lattice2(X1))
& v15_lattices(k1_lattice2(X1))
& v16_lattices(k1_lattice2(X1))
& v17_lattices(k1_lattice2(X1)) ) ),
inference(fof_nnf,[status(thm)],[141]) ).
fof(524,plain,
! [X2] :
( v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2)
| ( ~ v3_struct_0(k1_lattice2(X2))
& v3_lattices(k1_lattice2(X2))
& v4_lattices(k1_lattice2(X2))
& v5_lattices(k1_lattice2(X2))
& v6_lattices(k1_lattice2(X2))
& v7_lattices(k1_lattice2(X2))
& v8_lattices(k1_lattice2(X2))
& v9_lattices(k1_lattice2(X2))
& v10_lattices(k1_lattice2(X2))
& v11_lattices(k1_lattice2(X2))
& v12_lattices(k1_lattice2(X2))
& v13_lattices(k1_lattice2(X2))
& v14_lattices(k1_lattice2(X2))
& v15_lattices(k1_lattice2(X2))
& v16_lattices(k1_lattice2(X2))
& v17_lattices(k1_lattice2(X2)) ) ),
inference(variable_rename,[status(thm)],[523]) ).
fof(525,plain,
! [X2] :
( ( ~ v3_struct_0(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v3_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v4_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v5_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v6_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v7_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v8_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v9_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v10_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v11_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v12_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v13_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v14_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v15_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v16_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) )
& ( v17_lattices(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ v17_lattices(X2)
| ~ l3_lattices(X2) ) ),
inference(distribute,[status(thm)],[524]) ).
cnf(526,plain,
( v3_struct_0(X1)
| v17_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| ~ v10_lattices(X1) ),
inference(split_conjunct,[status(thm)],[525]) ).
fof(543,plain,
! [X1] :
( ~ l2_lattices(X1)
| ( v1_funct_1(u2_lattices(X1))
& v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
inference(fof_nnf,[status(thm)],[77]) ).
fof(544,plain,
! [X2] :
( ~ l2_lattices(X2)
| ( v1_funct_1(u2_lattices(X2))
& v1_funct_2(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))
& m2_relset_1(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)) ) ),
inference(variable_rename,[status(thm)],[543]) ).
fof(545,plain,
! [X2] :
( ( v1_funct_1(u2_lattices(X2))
| ~ l2_lattices(X2) )
& ( v1_funct_2(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))
| ~ l2_lattices(X2) )
& ( m2_relset_1(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))
| ~ l2_lattices(X2) ) ),
inference(distribute,[status(thm)],[544]) ).
cnf(546,plain,
( m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[545]) ).
cnf(547,plain,
( v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[545]) ).
cnf(548,plain,
( v1_funct_1(u2_lattices(X1))
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[545]) ).
fof(602,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| k7_filter_2(X1,X2) = X2 ) ),
inference(fof_nnf,[status(thm)],[149]) ).
fof(603,plain,
! [X3] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3)))
| k7_filter_2(X3,X4) = X4 ) ),
inference(variable_rename,[status(thm)],[602]) ).
fof(604,plain,
! [X3,X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3)))
| k7_filter_2(X3,X4) = X4
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ),
inference(shift_quantors,[status(thm)],[603]) ).
cnf(605,plain,
( v3_struct_0(X1)
| k7_filter_2(X1,X2) = X2
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(split_conjunct,[status(thm)],[604]) ).
fof(606,plain,
! [X1,X2] :
( ~ m1_subset_1(X1,X2)
| v1_xboole_0(X2)
| r2_hidden(X1,X2) ),
inference(fof_nnf,[status(thm)],[91]) ).
fof(607,plain,
! [X3,X4] :
( ~ m1_subset_1(X3,X4)
| v1_xboole_0(X4)
| r2_hidden(X3,X4) ),
inference(variable_rename,[status(thm)],[606]) ).
cnf(608,plain,
( r2_hidden(X1,X2)
| v1_xboole_0(X2)
| ~ m1_subset_1(X1,X2) ),
inference(split_conjunct,[status(thm)],[607]) ).
fof(612,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ! [X2] :
( ~ m2_lattice4(X2,X1)
| m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ) ),
inference(fof_nnf,[status(thm)],[150]) ).
fof(613,plain,
! [X3] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ! [X4] :
( ~ m2_lattice4(X4,X3)
| m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3))) ) ),
inference(variable_rename,[status(thm)],[612]) ).
fof(614,plain,
! [X3,X4] :
( ~ m2_lattice4(X4,X3)
| m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3)))
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ),
inference(shift_quantors,[status(thm)],[613]) ).
cnf(615,plain,
( v3_struct_0(X1)
| m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_lattice4(X2,X1) ),
inference(split_conjunct,[status(thm)],[614]) ).
fof(616,plain,
! [X1,X2,X3] :
( v1_xboole_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ( ~ v3_struct_0(g3_lattices(X1,X2,X3))
& v3_lattices(g3_lattices(X1,X2,X3)) ) ),
inference(fof_nnf,[status(thm)],[151]) ).
fof(617,plain,
! [X4,X5,X6] :
( v1_xboole_0(X4)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X4,X4),X4)
| ~ m1_relset_1(X5,k2_zfmisc_1(X4,X4),X4)
| ~ v1_funct_1(X6)
| ~ v1_funct_2(X6,k2_zfmisc_1(X4,X4),X4)
| ~ m1_relset_1(X6,k2_zfmisc_1(X4,X4),X4)
| ( ~ v3_struct_0(g3_lattices(X4,X5,X6))
& v3_lattices(g3_lattices(X4,X5,X6)) ) ),
inference(variable_rename,[status(thm)],[616]) ).
fof(618,plain,
! [X4,X5,X6] :
( ( ~ v3_struct_0(g3_lattices(X4,X5,X6))
| v1_xboole_0(X4)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X4,X4),X4)
| ~ m1_relset_1(X5,k2_zfmisc_1(X4,X4),X4)
| ~ v1_funct_1(X6)
| ~ v1_funct_2(X6,k2_zfmisc_1(X4,X4),X4)
| ~ m1_relset_1(X6,k2_zfmisc_1(X4,X4),X4) )
& ( v3_lattices(g3_lattices(X4,X5,X6))
| v1_xboole_0(X4)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X4,X4),X4)
| ~ m1_relset_1(X5,k2_zfmisc_1(X4,X4),X4)
| ~ v1_funct_1(X6)
| ~ v1_funct_2(X6,k2_zfmisc_1(X4,X4),X4)
| ~ m1_relset_1(X6,k2_zfmisc_1(X4,X4),X4) ) ),
inference(distribute,[status(thm)],[617]) ).
cnf(620,plain,
( v1_xboole_0(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_2(X1,k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(X3)
| ~ v3_struct_0(g3_lattices(X2,X3,X1)) ),
inference(split_conjunct,[status(thm)],[618]) ).
fof(621,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1)
| ! [X2] :
( ~ m1_filter_0(X2,X1)
| ( ( X2 = k1_filter_0(X1)
| ~ v2_filter_0(X2,X1)
| v1_filter_0(X2,X1) )
& ( ~ v1_filter_0(X2,X1)
| ( X2 != k1_filter_0(X1)
& v2_filter_0(X2,X1) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[152]) ).
fof(622,plain,
! [X3] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ v17_lattices(X3)
| ~ l3_lattices(X3)
| ! [X4] :
( ~ m1_filter_0(X4,X3)
| ( ( X4 = k1_filter_0(X3)
| ~ v2_filter_0(X4,X3)
| v1_filter_0(X4,X3) )
& ( ~ v1_filter_0(X4,X3)
| ( X4 != k1_filter_0(X3)
& v2_filter_0(X4,X3) ) ) ) ) ),
inference(variable_rename,[status(thm)],[621]) ).
fof(623,plain,
! [X3,X4] :
( ~ m1_filter_0(X4,X3)
| ( ( X4 = k1_filter_0(X3)
| ~ v2_filter_0(X4,X3)
| v1_filter_0(X4,X3) )
& ( ~ v1_filter_0(X4,X3)
| ( X4 != k1_filter_0(X3)
& v2_filter_0(X4,X3) ) ) )
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ v17_lattices(X3)
| ~ l3_lattices(X3) ),
inference(shift_quantors,[status(thm)],[622]) ).
fof(624,plain,
! [X3,X4] :
( ( X4 = k1_filter_0(X3)
| ~ v2_filter_0(X4,X3)
| v1_filter_0(X4,X3)
| ~ m1_filter_0(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ v17_lattices(X3)
| ~ l3_lattices(X3) )
& ( X4 != k1_filter_0(X3)
| ~ v1_filter_0(X4,X3)
| ~ m1_filter_0(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ v17_lattices(X3)
| ~ l3_lattices(X3) )
& ( v2_filter_0(X4,X3)
| ~ v1_filter_0(X4,X3)
| ~ m1_filter_0(X4,X3)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ v17_lattices(X3)
| ~ l3_lattices(X3) ) ),
inference(distribute,[status(thm)],[623]) ).
cnf(625,plain,
( v3_struct_0(X1)
| v2_filter_0(X2,X1)
| ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_filter_0(X2,X1)
| ~ v1_filter_0(X2,X1) ),
inference(split_conjunct,[status(thm)],[624]) ).
cnf(626,plain,
( v3_struct_0(X1)
| ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_filter_0(X2,X1)
| ~ v1_filter_0(X2,X1)
| X2 != k1_filter_0(X1) ),
inference(split_conjunct,[status(thm)],[624]) ).
cnf(627,plain,
( v3_struct_0(X1)
| v1_filter_0(X2,X1)
| X2 = k1_filter_0(X1)
| ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_filter_0(X2,X1)
| ~ v2_filter_0(X2,X1) ),
inference(split_conjunct,[status(thm)],[624]) ).
fof(628,negated_conjecture,
? [X1] :
( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1)
& ? [X2] :
( m2_filter_2(X2,X1)
& ( X2 = k17_filter_2(X1)
| ~ v1_filter_2(X2,X1)
| ~ r2_filter_2(X1,X2) )
& ( ( X2 != k17_filter_2(X1)
& v1_filter_2(X2,X1) )
| r2_filter_2(X1,X2) ) ) ),
inference(fof_nnf,[status(thm)],[153]) ).
fof(629,negated_conjecture,
? [X3] :
( ~ v3_struct_0(X3)
& v10_lattices(X3)
& v17_lattices(X3)
& l3_lattices(X3)
& ? [X4] :
( m2_filter_2(X4,X3)
& ( X4 = k17_filter_2(X3)
| ~ v1_filter_2(X4,X3)
| ~ r2_filter_2(X3,X4) )
& ( ( X4 != k17_filter_2(X3)
& v1_filter_2(X4,X3) )
| r2_filter_2(X3,X4) ) ) ),
inference(variable_rename,[status(thm)],[628]) ).
fof(630,negated_conjecture,
( ~ v3_struct_0(esk27_0)
& v10_lattices(esk27_0)
& v17_lattices(esk27_0)
& l3_lattices(esk27_0)
& m2_filter_2(esk28_0,esk27_0)
& ( esk28_0 = k17_filter_2(esk27_0)
| ~ v1_filter_2(esk28_0,esk27_0)
| ~ r2_filter_2(esk27_0,esk28_0) )
& ( ( esk28_0 != k17_filter_2(esk27_0)
& v1_filter_2(esk28_0,esk27_0) )
| r2_filter_2(esk27_0,esk28_0) ) ),
inference(skolemize,[status(esa)],[629]) ).
fof(631,negated_conjecture,
( ~ v3_struct_0(esk27_0)
& v10_lattices(esk27_0)
& v17_lattices(esk27_0)
& l3_lattices(esk27_0)
& m2_filter_2(esk28_0,esk27_0)
& ( esk28_0 = k17_filter_2(esk27_0)
| ~ v1_filter_2(esk28_0,esk27_0)
| ~ r2_filter_2(esk27_0,esk28_0) )
& ( esk28_0 != k17_filter_2(esk27_0)
| r2_filter_2(esk27_0,esk28_0) )
& ( v1_filter_2(esk28_0,esk27_0)
| r2_filter_2(esk27_0,esk28_0) ) ),
inference(distribute,[status(thm)],[630]) ).
cnf(632,negated_conjecture,
( r2_filter_2(esk27_0,esk28_0)
| v1_filter_2(esk28_0,esk27_0) ),
inference(split_conjunct,[status(thm)],[631]) ).
cnf(633,negated_conjecture,
( r2_filter_2(esk27_0,esk28_0)
| esk28_0 != k17_filter_2(esk27_0) ),
inference(split_conjunct,[status(thm)],[631]) ).
cnf(634,negated_conjecture,
( esk28_0 = k17_filter_2(esk27_0)
| ~ r2_filter_2(esk27_0,esk28_0)
| ~ v1_filter_2(esk28_0,esk27_0) ),
inference(split_conjunct,[status(thm)],[631]) ).
cnf(635,negated_conjecture,
m2_filter_2(esk28_0,esk27_0),
inference(split_conjunct,[status(thm)],[631]) ).
cnf(636,negated_conjecture,
l3_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[631]) ).
cnf(637,negated_conjecture,
v17_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[631]) ).
cnf(638,negated_conjecture,
v10_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[631]) ).
cnf(639,negated_conjecture,
~ v3_struct_0(esk27_0),
inference(split_conjunct,[status(thm)],[631]) ).
cnf(670,negated_conjecture,
( v3_struct_0(esk27_0)
| ~ v1_xboole_0(esk28_0)
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[380,635,theory(equality)]) ).
cnf(673,negated_conjecture,
( v3_struct_0(esk27_0)
| ~ v1_xboole_0(esk28_0)
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[670,636,theory(equality)]) ).
cnf(674,negated_conjecture,
( v3_struct_0(esk27_0)
| ~ v1_xboole_0(esk28_0)
| $false
| $false ),
inference(rw,[status(thm)],[673,638,theory(equality)]) ).
cnf(675,negated_conjecture,
( v3_struct_0(esk27_0)
| ~ v1_xboole_0(esk28_0) ),
inference(cn,[status(thm)],[674,theory(equality)]) ).
cnf(676,negated_conjecture,
~ v1_xboole_0(esk28_0),
inference(sr,[status(thm)],[675,639,theory(equality)]) ).
cnf(749,plain,
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X3,X2)
| ~ r1_tarski(X2,X1) ),
inference(spm,[status(thm)],[386,412,theory(equality)]) ).
cnf(775,plain,
( m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ l3_lattices(k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(spm,[status(thm)],[173,219,theory(equality)]) ).
cnf(788,plain,
( k7_filter_2(X1,X2) = X2
| v3_struct_0(X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_lattice4(X2,X1) ),
inference(spm,[status(thm)],[605,615,theory(equality)]) ).
cnf(789,plain,
( m1_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
inference(spm,[status(thm)],[272,258,theory(equality)]) ).
cnf(837,plain,
( v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| k1_filter_0(k1_lattice2(X1)) != k15_filter_2(X1,X2)
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ r2_filter_2(X1,X2)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(spm,[status(thm)],[626,291,theory(equality)]) ).
cnf(839,plain,
( v1_filter_2(X1,X2)
| v3_struct_0(X2)
| v3_struct_0(k1_lattice2(X2))
| ~ m2_filter_2(X1,X2)
| ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| ~ v1_filter_0(k15_filter_2(X2,X1),k1_lattice2(X2))
| ~ v17_lattices(k1_lattice2(X2))
| ~ m1_filter_0(k15_filter_2(X2,X1),k1_lattice2(X2))
| ~ l3_lattices(k1_lattice2(X2))
| ~ v10_lattices(k1_lattice2(X2)) ),
inference(spm,[status(thm)],[392,625,theory(equality)]) ).
cnf(841,plain,
( m1_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
inference(spm,[status(thm)],[272,546,theory(equality)]) ).
cnf(845,plain,
( k1_filter_0(k1_lattice2(X1)) = k15_filter_2(X1,X2)
| v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(spm,[status(thm)],[627,393,theory(equality)]) ).
cnf(863,plain,
( m1_subset_1(k15_filter_2(X1,X2),k1_zfmisc_1(u1_struct_0(k1_lattice2(X1))))
| v3_struct_0(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_filter_2(X2,X1) ),
inference(spm,[status(thm)],[374,459,theory(equality)]) ).
cnf(890,plain,
( v1_xboole_0(X3)
| ~ v1_xboole_0(X1)
| ~ r1_tarski(X3,X1)
| ~ m1_subset_1(X2,X3) ),
inference(spm,[status(thm)],[749,608,theory(equality)]) ).
cnf(984,plain,
( v1_xboole_0(X1)
| ~ v1_xboole_0(X2)
| ~ r1_tarski(X1,X2) ),
inference(spm,[status(thm)],[890,222,theory(equality)]) ).
cnf(1185,plain,
( X2 = k15_filter_2(X1,X2)
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_lattice4(X2,X1) ),
inference(spm,[status(thm)],[459,788,theory(equality)]) ).
cnf(1207,plain,
( k15_filter_2(X1,X2) = X2
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[1185,379]) ).
cnf(1210,plain,
( v2_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(spm,[status(thm)],[393,1207,theory(equality)]) ).
cnf(1211,plain,
( r2_filter_2(X1,X2)
| v3_struct_0(X1)
| ~ v1_filter_0(X2,k1_lattice2(X1))
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(spm,[status(thm)],[290,1207,theory(equality)]) ).
cnf(1225,plain,
( m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[775,308]) ).
cnf(1226,plain,
( m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[1225,476]) ).
cnf(1227,plain,
( m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[1226,472]) ).
cnf(1229,plain,
( m1_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(spm,[status(thm)],[1227,1207,theory(equality)]) ).
cnf(1261,plain,
( k1_filter_0(k1_lattice2(X1)) = X2
| v1_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(X2,k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(spm,[status(thm)],[627,1210,theory(equality)]) ).
cnf(1323,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_2(X2,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_1(u1_lattices(X1))
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v3_struct_0(g3_lattices(u1_struct_0(X1),u1_lattices(X1),X2))
| ~ l1_lattices(X1) ),
inference(spm,[status(thm)],[620,789,theory(equality)]) ).
cnf(1325,plain,
( u1_struct_0(X1) = X2
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),X3) != g3_lattices(X2,X4,X5)
| ~ v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_2(X3,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_1(u1_lattices(X1))
| ~ v1_funct_1(X3)
| ~ m1_relset_1(X3,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
inference(spm,[status(thm)],[400,789,theory(equality)]) ).
cnf(1355,plain,
( v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| k1_filter_0(k1_lattice2(X1)) != k15_filter_2(X1,X2)
| ~ r2_filter_2(X1,X2)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[837,308]) ).
cnf(1356,plain,
( v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| k1_filter_0(k1_lattice2(X1)) != k15_filter_2(X1,X2)
| ~ r2_filter_2(X1,X2)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[1355,476]) ).
cnf(1357,plain,
( v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| k1_filter_0(k1_lattice2(X1)) != k15_filter_2(X1,X2)
| ~ r2_filter_2(X1,X2)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[1356,1227]) ).
cnf(1358,plain,
( v3_struct_0(X1)
| k1_filter_0(k1_lattice2(X1)) != k15_filter_2(X1,X2)
| ~ r2_filter_2(X1,X2)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[1357,472]) ).
cnf(1359,negated_conjecture,
( v3_struct_0(esk27_0)
| k1_filter_0(k1_lattice2(esk27_0)) != k15_filter_2(esk27_0,esk28_0)
| ~ m2_filter_2(esk28_0,esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0)
| k17_filter_2(esk27_0) != esk28_0 ),
inference(spm,[status(thm)],[1358,633,theory(equality)]) ).
cnf(1360,negated_conjecture,
( v3_struct_0(esk27_0)
| k1_filter_0(k1_lattice2(esk27_0)) != k15_filter_2(esk27_0,esk28_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0)
| k17_filter_2(esk27_0) != esk28_0 ),
inference(rw,[status(thm)],[1359,635,theory(equality)]) ).
cnf(1361,negated_conjecture,
( v3_struct_0(esk27_0)
| k1_filter_0(k1_lattice2(esk27_0)) != k15_filter_2(esk27_0,esk28_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| ~ v10_lattices(esk27_0)
| k17_filter_2(esk27_0) != esk28_0 ),
inference(rw,[status(thm)],[1360,636,theory(equality)]) ).
cnf(1362,negated_conjecture,
( v3_struct_0(esk27_0)
| k1_filter_0(k1_lattice2(esk27_0)) != k15_filter_2(esk27_0,esk28_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| $false
| k17_filter_2(esk27_0) != esk28_0 ),
inference(rw,[status(thm)],[1361,638,theory(equality)]) ).
cnf(1363,negated_conjecture,
( v3_struct_0(esk27_0)
| k1_filter_0(k1_lattice2(esk27_0)) != k15_filter_2(esk27_0,esk28_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| k17_filter_2(esk27_0) != esk28_0 ),
inference(cn,[status(thm)],[1362,theory(equality)]) ).
cnf(1364,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) != k15_filter_2(esk27_0,esk28_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| k17_filter_2(esk27_0) != esk28_0 ),
inference(sr,[status(thm)],[1363,639,theory(equality)]) ).
cnf(1365,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| u1_struct_0(k1_lattice2(esk27_0)) != k15_filter_2(esk27_0,esk28_0)
| k17_filter_2(esk27_0) != esk28_0
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(spm,[status(thm)],[1364,157,theory(equality)]) ).
cnf(1378,plain,
( v1_filter_2(X1,X2)
| v3_struct_0(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v1_filter_0(k15_filter_2(X2,X1),k1_lattice2(X2))
| ~ m2_filter_2(X1,X2)
| ~ v17_lattices(k1_lattice2(X2))
| ~ m1_filter_0(k15_filter_2(X2,X1),k1_lattice2(X2))
| ~ l3_lattices(k1_lattice2(X2))
| ~ l3_lattices(X2)
| ~ v10_lattices(X2) ),
inference(csr,[status(thm)],[839,308]) ).
cnf(1379,plain,
( v1_filter_2(X1,X2)
| v3_struct_0(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v1_filter_0(k15_filter_2(X2,X1),k1_lattice2(X2))
| ~ m2_filter_2(X1,X2)
| ~ v17_lattices(k1_lattice2(X2))
| ~ m1_filter_0(k15_filter_2(X2,X1),k1_lattice2(X2))
| ~ l3_lattices(X2)
| ~ v10_lattices(X2) ),
inference(csr,[status(thm)],[1378,476]) ).
cnf(1380,plain,
( v1_filter_2(X1,X2)
| v3_struct_0(k1_lattice2(X2))
| v3_struct_0(X2)
| ~ v1_filter_0(k15_filter_2(X2,X1),k1_lattice2(X2))
| ~ m2_filter_2(X1,X2)
| ~ v17_lattices(k1_lattice2(X2))
| ~ l3_lattices(X2)
| ~ v10_lattices(X2) ),
inference(csr,[status(thm)],[1379,1227]) ).
cnf(1381,plain,
( v1_filter_2(X1,X2)
| v3_struct_0(X2)
| ~ v1_filter_0(k15_filter_2(X2,X1),k1_lattice2(X2))
| ~ m2_filter_2(X1,X2)
| ~ v17_lattices(k1_lattice2(X2))
| ~ l3_lattices(X2)
| ~ v10_lattices(X2) ),
inference(csr,[status(thm)],[1380,472]) ).
cnf(1382,plain,
( v1_filter_2(X1,X2)
| v3_struct_0(X2)
| ~ m2_filter_2(X1,X2)
| ~ v17_lattices(k1_lattice2(X2))
| ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| ~ r2_filter_2(X2,X1) ),
inference(spm,[status(thm)],[1381,291,theory(equality)]) ).
cnf(1389,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ r2_filter_2(esk27_0,esk28_0)
| ~ m2_filter_2(esk28_0,esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[634,1382,theory(equality)]) ).
cnf(1390,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ r2_filter_2(esk27_0,esk28_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[1389,635,theory(equality)]) ).
cnf(1391,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ r2_filter_2(esk27_0,esk28_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[1390,636,theory(equality)]) ).
cnf(1392,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ r2_filter_2(esk27_0,esk28_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| $false ),
inference(rw,[status(thm)],[1391,638,theory(equality)]) ).
cnf(1393,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ r2_filter_2(esk27_0,esk28_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[1392,theory(equality)]) ).
cnf(1394,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ r2_filter_2(esk27_0,esk28_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[1393,639,theory(equality)]) ).
cnf(1411,plain,
( k1_filter_0(k1_lattice2(X1)) = k15_filter_2(X1,X2)
| v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[845,308]) ).
cnf(1412,plain,
( k1_filter_0(k1_lattice2(X1)) = k15_filter_2(X1,X2)
| v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[1411,476]) ).
cnf(1413,plain,
( k1_filter_0(k1_lattice2(X1)) = k15_filter_2(X1,X2)
| v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[1412,1227]) ).
cnf(1414,plain,
( k1_filter_0(k1_lattice2(X1)) = k15_filter_2(X1,X2)
| v1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[1413,472]) ).
cnf(1416,plain,
( r2_filter_2(X1,X2)
| v3_struct_0(X1)
| k1_filter_0(k1_lattice2(X1)) = k15_filter_2(X1,X2)
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ v1_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1)) ),
inference(spm,[status(thm)],[290,1414,theory(equality)]) ).
cnf(2012,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| esk28_0 != u1_struct_0(k1_lattice2(esk27_0))
| k17_filter_2(esk27_0) != esk28_0
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| ~ m2_filter_2(esk28_0,esk27_0)
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[1365,1207,theory(equality)]) ).
cnf(2013,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| esk28_0 != u1_struct_0(k1_lattice2(esk27_0))
| k17_filter_2(esk27_0) != esk28_0
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[2012,635,theory(equality)]) ).
cnf(2014,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| esk28_0 != u1_struct_0(k1_lattice2(esk27_0))
| k17_filter_2(esk27_0) != esk28_0
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[2013,636,theory(equality)]) ).
cnf(2015,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| esk28_0 != u1_struct_0(k1_lattice2(esk27_0))
| k17_filter_2(esk27_0) != esk28_0
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[2014,638,theory(equality)]) ).
cnf(2016,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| esk28_0 != u1_struct_0(k1_lattice2(esk27_0))
| k17_filter_2(esk27_0) != esk28_0
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[2015,theory(equality)]) ).
cnf(2017,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| u1_struct_0(k1_lattice2(esk27_0)) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[2016,639,theory(equality)]) ).
cnf(2018,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| u1_struct_0(k1_lattice2(esk27_0)) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| ~ v17_lattices(esk27_0)
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[2017,526,theory(equality)]) ).
cnf(2019,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| u1_struct_0(k1_lattice2(esk27_0)) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[2018,637,theory(equality)]) ).
cnf(2020,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| u1_struct_0(k1_lattice2(esk27_0)) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[2019,636,theory(equality)]) ).
cnf(2021,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| u1_struct_0(k1_lattice2(esk27_0)) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[2020,638,theory(equality)]) ).
cnf(2022,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| u1_struct_0(k1_lattice2(esk27_0)) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[2021,theory(equality)]) ).
cnf(2023,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| u1_struct_0(k1_lattice2(esk27_0)) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[2022,639,theory(equality)]) ).
cnf(2341,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = k15_filter_2(esk27_0,esk28_0)
| r2_filter_2(esk27_0,esk28_0)
| v3_struct_0(esk27_0)
| ~ m2_filter_2(esk28_0,esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[1416,632,theory(equality)]) ).
cnf(2344,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = k15_filter_2(esk27_0,esk28_0)
| r2_filter_2(esk27_0,esk28_0)
| v3_struct_0(esk27_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[2341,635,theory(equality)]) ).
cnf(2345,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = k15_filter_2(esk27_0,esk28_0)
| r2_filter_2(esk27_0,esk28_0)
| v3_struct_0(esk27_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[2344,636,theory(equality)]) ).
cnf(2346,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = k15_filter_2(esk27_0,esk28_0)
| r2_filter_2(esk27_0,esk28_0)
| v3_struct_0(esk27_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| $false ),
inference(rw,[status(thm)],[2345,638,theory(equality)]) ).
cnf(2347,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = k15_filter_2(esk27_0,esk28_0)
| r2_filter_2(esk27_0,esk28_0)
| v3_struct_0(esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[2346,theory(equality)]) ).
cnf(2348,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = k15_filter_2(esk27_0,esk28_0)
| r2_filter_2(esk27_0,esk28_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[2347,639,theory(equality)]) ).
cnf(2350,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| k1_filter_0(k1_lattice2(esk27_0)) = k15_filter_2(esk27_0,esk28_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(spm,[status(thm)],[1394,2348,theory(equality)]) ).
cnf(2358,negated_conjecture,
( k15_filter_2(esk27_0,esk28_0) = u1_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(k1_lattice2(esk27_0))
| k17_filter_2(esk27_0) = esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(spm,[status(thm)],[157,2350,theory(equality)]) ).
cnf(2377,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| v3_struct_0(esk27_0)
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| ~ m2_filter_2(esk28_0,esk27_0)
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(spm,[status(thm)],[1207,2358,theory(equality)]) ).
cnf(2414,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| v3_struct_0(esk27_0)
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| $false
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(rw,[status(thm)],[2377,635,theory(equality)]) ).
cnf(2415,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| v3_struct_0(esk27_0)
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| $false
| $false
| ~ v10_lattices(esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(rw,[status(thm)],[2414,636,theory(equality)]) ).
cnf(2416,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| v3_struct_0(esk27_0)
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| $false
| $false
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(rw,[status(thm)],[2415,638,theory(equality)]) ).
cnf(2417,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| v3_struct_0(esk27_0)
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[2416,theory(equality)]) ).
cnf(2418,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[2417,639,theory(equality)]) ).
cnf(2464,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| ~ v17_lattices(esk27_0)
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[2418,526,theory(equality)]) ).
cnf(2465,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[2464,637,theory(equality)]) ).
cnf(2466,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[2465,636,theory(equality)]) ).
cnf(2467,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[2466,638,theory(equality)]) ).
cnf(2468,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[2467,theory(equality)]) ).
cnf(2469,negated_conjecture,
( u1_struct_0(k1_lattice2(esk27_0)) = esk28_0
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[2468,639,theory(equality)]) ).
cnf(3286,plain,
( k1_filter_0(k1_lattice2(X1)) = X2
| v1_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(X2,k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[1261,308]) ).
cnf(3287,plain,
( k1_filter_0(k1_lattice2(X1)) = X2
| v1_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(X2,k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[3286,476]) ).
cnf(3288,plain,
( k1_filter_0(k1_lattice2(X1)) = X2
| v1_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[3287,1229]) ).
cnf(3289,plain,
( k1_filter_0(k1_lattice2(X1)) = X2
| v1_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_2(X2,X1)
| ~ m2_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(csr,[status(thm)],[3288,472]) ).
cnf(3292,plain,
( r2_filter_2(X1,X2)
| v3_struct_0(X1)
| k1_filter_0(k1_lattice2(X1)) = X2
| ~ m2_filter_2(X2,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ v1_filter_2(X2,X1)
| ~ v17_lattices(k1_lattice2(X1)) ),
inference(spm,[status(thm)],[1211,3289,theory(equality)]) ).
cnf(3321,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = esk28_0
| r2_filter_2(esk27_0,esk28_0)
| v3_struct_0(esk27_0)
| ~ m2_filter_2(esk28_0,esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[3292,632,theory(equality)]) ).
cnf(3324,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = esk28_0
| r2_filter_2(esk27_0,esk28_0)
| v3_struct_0(esk27_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[3321,635,theory(equality)]) ).
cnf(3325,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = esk28_0
| r2_filter_2(esk27_0,esk28_0)
| v3_struct_0(esk27_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[3324,636,theory(equality)]) ).
cnf(3326,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = esk28_0
| r2_filter_2(esk27_0,esk28_0)
| v3_struct_0(esk27_0)
| $false
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| $false ),
inference(rw,[status(thm)],[3325,638,theory(equality)]) ).
cnf(3327,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = esk28_0
| r2_filter_2(esk27_0,esk28_0)
| v3_struct_0(esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[3326,theory(equality)]) ).
cnf(3328,negated_conjecture,
( k1_filter_0(k1_lattice2(esk27_0)) = esk28_0
| r2_filter_2(esk27_0,esk28_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[3327,639,theory(equality)]) ).
cnf(3330,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| k1_filter_0(k1_lattice2(esk27_0)) = esk28_0
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(spm,[status(thm)],[1394,3328,theory(equality)]) ).
cnf(3346,negated_conjecture,
( esk28_0 = k15_filter_2(esk27_0,esk28_0)
| k17_filter_2(esk27_0) = esk28_0
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(spm,[status(thm)],[2350,3330,theory(equality)]) ).
cnf(3362,negated_conjecture,
( m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(k1_lattice2(esk27_0))))
| v3_struct_0(esk27_0)
| k17_filter_2(esk27_0) = esk28_0
| ~ m2_filter_2(esk28_0,esk27_0)
| ~ m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk27_0)))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(spm,[status(thm)],[863,3346,theory(equality)]) ).
cnf(3417,negated_conjecture,
( m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(k1_lattice2(esk27_0))))
| v3_struct_0(esk27_0)
| k17_filter_2(esk27_0) = esk28_0
| $false
| ~ m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk27_0)))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(rw,[status(thm)],[3362,635,theory(equality)]) ).
cnf(3418,negated_conjecture,
( m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(k1_lattice2(esk27_0))))
| v3_struct_0(esk27_0)
| k17_filter_2(esk27_0) = esk28_0
| $false
| ~ m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk27_0)))
| $false
| ~ v10_lattices(esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(rw,[status(thm)],[3417,636,theory(equality)]) ).
cnf(3419,negated_conjecture,
( m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(k1_lattice2(esk27_0))))
| v3_struct_0(esk27_0)
| k17_filter_2(esk27_0) = esk28_0
| $false
| ~ m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk27_0)))
| $false
| $false
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(rw,[status(thm)],[3418,638,theory(equality)]) ).
cnf(3420,negated_conjecture,
( m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(k1_lattice2(esk27_0))))
| v3_struct_0(esk27_0)
| k17_filter_2(esk27_0) = esk28_0
| ~ m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk27_0)))
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[3419,theory(equality)]) ).
cnf(3421,negated_conjecture,
( m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(k1_lattice2(esk27_0))))
| k17_filter_2(esk27_0) = esk28_0
| ~ m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk27_0)))
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[3420,639,theory(equality)]) ).
cnf(4212,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_2(X2,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1)
| ~ v3_struct_0(g3_lattices(u1_struct_0(X1),u1_lattices(X1),X2)) ),
inference(csr,[status(thm)],[1323,260]) ).
cnf(4213,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ v1_funct_2(X2,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1)
| ~ v3_struct_0(g3_lattices(u1_struct_0(X1),u1_lattices(X1),X2)) ),
inference(csr,[status(thm)],[4212,259]) ).
cnf(4217,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_1(u2_lattices(X1))
| ~ l1_lattices(X1)
| ~ v3_struct_0(g3_lattices(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1)))
| ~ l2_lattices(X1) ),
inference(spm,[status(thm)],[4213,841,theory(equality)]) ).
cnf(4279,plain,
( u1_struct_0(X1) = X2
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),X3) != g3_lattices(X2,X4,X5)
| ~ v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_2(X3,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ m1_relset_1(X3,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
inference(csr,[status(thm)],[1325,260]) ).
cnf(4280,plain,
( u1_struct_0(X1) = X2
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),X3) != g3_lattices(X2,X4,X5)
| ~ v1_funct_2(X3,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ m1_relset_1(X3,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
inference(csr,[status(thm)],[4279,259]) ).
cnf(4284,plain,
( u1_struct_0(X1) = X2
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1)) != g3_lattices(X2,X3,X4)
| ~ v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_1(u2_lattices(X1))
| ~ l1_lattices(X1)
| ~ l2_lattices(X1) ),
inference(spm,[status(thm)],[4280,841,theory(equality)]) ).
cnf(5536,negated_conjecture,
( r1_tarski(esk28_0,u1_struct_0(k1_lattice2(esk27_0)))
| k17_filter_2(esk27_0) = esk28_0
| ~ m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk27_0)))
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(spm,[status(thm)],[413,3421,theory(equality)]) ).
cnf(5546,negated_conjecture,
( v1_xboole_0(esk28_0)
| k17_filter_2(esk27_0) = esk28_0
| ~ v1_xboole_0(u1_struct_0(k1_lattice2(esk27_0)))
| ~ m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk27_0)))
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(spm,[status(thm)],[984,5536,theory(equality)]) ).
cnf(5551,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ v1_xboole_0(u1_struct_0(k1_lattice2(esk27_0)))
| ~ m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk27_0)))
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[5546,676,theory(equality)]) ).
cnf(5557,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(k1_lattice2(esk27_0)))
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ m2_lattice4(esk28_0,esk27_0)
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[5551,615,theory(equality)]) ).
cnf(5562,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(k1_lattice2(esk27_0)))
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ m2_lattice4(esk28_0,esk27_0)
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[5557,636,theory(equality)]) ).
cnf(5563,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(k1_lattice2(esk27_0)))
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ m2_lattice4(esk28_0,esk27_0)
| $false
| $false ),
inference(rw,[status(thm)],[5562,638,theory(equality)]) ).
cnf(5564,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(k1_lattice2(esk27_0)))
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ m2_lattice4(esk28_0,esk27_0) ),
inference(cn,[status(thm)],[5563,theory(equality)]) ).
cnf(5565,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ v1_xboole_0(u1_struct_0(k1_lattice2(esk27_0)))
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ m2_lattice4(esk28_0,esk27_0) ),
inference(sr,[status(thm)],[5564,639,theory(equality)]) ).
cnf(36793,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1)
| ~ l1_lattices(X1)
| ~ v3_struct_0(g3_lattices(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1))) ),
inference(csr,[status(thm)],[4217,548]) ).
cnf(36794,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ l2_lattices(X1)
| ~ l1_lattices(X1)
| ~ v3_struct_0(g3_lattices(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1))) ),
inference(csr,[status(thm)],[36793,547]) ).
cnf(36795,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ l2_lattices(X1)
| ~ l1_lattices(X1)
| ~ v3_struct_0(k1_lattice2(X1))
| ~ l3_lattices(X1) ),
inference(spm,[status(thm)],[36794,275,theory(equality)]) ).
cnf(36812,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ l2_lattices(X1)
| ~ l3_lattices(X1)
| ~ v3_struct_0(k1_lattice2(X1)) ),
inference(csr,[status(thm)],[36795,162]) ).
cnf(36813,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ v3_struct_0(k1_lattice2(X1)) ),
inference(csr,[status(thm)],[36812,161]) ).
cnf(37175,plain,
( u1_struct_0(X1) = X2
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1)) != g3_lattices(X2,X3,X4)
| ~ v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1)
| ~ l1_lattices(X1) ),
inference(csr,[status(thm)],[4284,548]) ).
cnf(37176,plain,
( u1_struct_0(X1) = X2
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1)) != g3_lattices(X2,X3,X4)
| ~ l2_lattices(X1)
| ~ l1_lattices(X1) ),
inference(csr,[status(thm)],[37175,547]) ).
cnf(37178,plain,
( u1_struct_0(X1) = X2
| k1_lattice2(X1) != g3_lattices(X2,X3,X4)
| ~ l2_lattices(X1)
| ~ l1_lattices(X1)
| ~ l3_lattices(X1) ),
inference(spm,[status(thm)],[37176,275,theory(equality)]) ).
cnf(37192,plain,
( u1_struct_0(X1) = X2
| k1_lattice2(X1) != g3_lattices(X2,X3,X4)
| ~ l2_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[37178,162]) ).
cnf(37193,plain,
( u1_struct_0(X1) = X2
| k1_lattice2(X1) != g3_lattices(X2,X3,X4)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[37192,161]) ).
cnf(37195,plain,
( u1_struct_0(X1) = u1_struct_0(X2)
| k1_lattice2(X1) != X2
| ~ l3_lattices(X1)
| ~ v3_lattices(X2)
| ~ l3_lattices(X2) ),
inference(spm,[status(thm)],[37193,456,theory(equality)]) ).
cnf(37201,plain,
( u1_struct_0(X1) = u1_struct_0(k1_lattice2(X1))
| ~ v3_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ l3_lattices(k1_lattice2(X1)) ),
inference(er,[status(thm)],[37195,theory(equality)]) ).
cnf(37202,plain,
( u1_struct_0(k1_lattice2(X1)) = u1_struct_0(X1)
| ~ v3_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[37201,476]) ).
cnf(37203,plain,
( u1_struct_0(k1_lattice2(X1)) = u1_struct_0(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[37202,477]) ).
cnf(37266,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0) ),
inference(spm,[status(thm)],[2023,37203,theory(equality)]) ).
cnf(37273,negated_conjecture,
( u1_struct_0(esk27_0) = esk28_0
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0) ),
inference(spm,[status(thm)],[2469,37203,theory(equality)]) ).
cnf(37354,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| ~ m2_lattice4(esk28_0,esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0) ),
inference(spm,[status(thm)],[5565,37203,theory(equality)]) ).
cnf(38128,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false ),
inference(rw,[status(thm)],[37266,636,theory(equality)]) ).
cnf(38129,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[38128,theory(equality)]) ).
cnf(38130,negated_conjecture,
( u1_struct_0(esk27_0) = esk28_0
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0))
| $false ),
inference(rw,[status(thm)],[37273,636,theory(equality)]) ).
cnf(38131,negated_conjecture,
( u1_struct_0(esk27_0) = esk28_0
| k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[38130,theory(equality)]) ).
cnf(38150,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| ~ m2_lattice4(esk28_0,esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false ),
inference(rw,[status(thm)],[37354,636,theory(equality)]) ).
cnf(38151,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| ~ m2_lattice4(esk28_0,esk27_0)
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[38150,theory(equality)]) ).
cnf(38316,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| ~ v17_lattices(k1_lattice2(esk27_0))
| ~ m2_filter_2(esk28_0,esk27_0)
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[38151,379,theory(equality)]) ).
cnf(38318,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[38316,635,theory(equality)]) ).
cnf(38319,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[38318,636,theory(equality)]) ).
cnf(38320,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| ~ v17_lattices(k1_lattice2(esk27_0))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[38319,638,theory(equality)]) ).
cnf(38321,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[38320,theory(equality)]) ).
cnf(38322,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| ~ v17_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[38321,639,theory(equality)]) ).
cnf(38327,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| ~ v17_lattices(esk27_0)
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[38322,526,theory(equality)]) ).
cnf(38328,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| $false
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[38327,637,theory(equality)]) ).
cnf(38329,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| $false
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[38328,636,theory(equality)]) ).
cnf(38330,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(esk27_0))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[38329,638,theory(equality)]) ).
cnf(38331,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ v1_xboole_0(u1_struct_0(esk27_0)) ),
inference(cn,[status(thm)],[38330,theory(equality)]) ).
cnf(38332,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ v1_xboole_0(u1_struct_0(esk27_0)) ),
inference(sr,[status(thm)],[38331,639,theory(equality)]) ).
cnf(38333,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ l3_lattices(esk27_0)
| ~ v3_struct_0(k1_lattice2(esk27_0)) ),
inference(spm,[status(thm)],[38332,36813,theory(equality)]) ).
cnf(38334,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| $false
| ~ v3_struct_0(k1_lattice2(esk27_0)) ),
inference(rw,[status(thm)],[38333,636,theory(equality)]) ).
cnf(38335,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ v3_struct_0(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[38334,theory(equality)]) ).
cnf(38336,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[38129,308,theory(equality)]) ).
cnf(38337,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[38336,636,theory(equality)]) ).
cnf(38338,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| $false
| $false ),
inference(rw,[status(thm)],[38337,638,theory(equality)]) ).
cnf(38339,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| v3_struct_0(esk27_0)
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[38338,theory(equality)]) ).
cnf(38340,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[38339,639,theory(equality)]) ).
cnf(38343,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| ~ l3_lattices(esk27_0) ),
inference(spm,[status(thm)],[38340,476,theory(equality)]) ).
cnf(38344,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0
| $false ),
inference(rw,[status(thm)],[38343,636,theory(equality)]) ).
cnf(38345,negated_conjecture,
( v3_struct_0(k1_lattice2(esk27_0))
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0 ),
inference(cn,[status(thm)],[38344,theory(equality)]) ).
cnf(38346,negated_conjecture,
( v3_struct_0(esk27_0)
| ~ l3_lattices(esk27_0)
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0 ),
inference(spm,[status(thm)],[472,38345,theory(equality)]) ).
cnf(38357,negated_conjecture,
( v3_struct_0(esk27_0)
| $false
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0 ),
inference(rw,[status(thm)],[38346,636,theory(equality)]) ).
cnf(38358,negated_conjecture,
( v3_struct_0(esk27_0)
| u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0 ),
inference(cn,[status(thm)],[38357,theory(equality)]) ).
cnf(38359,negated_conjecture,
( u1_struct_0(esk27_0) != esk28_0
| k17_filter_2(esk27_0) != esk28_0 ),
inference(sr,[status(thm)],[38358,639,theory(equality)]) ).
cnf(38378,negated_conjecture,
( v3_struct_0(esk27_0)
| u1_struct_0(esk27_0) != esk28_0
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[38359,350,theory(equality)]) ).
cnf(38379,negated_conjecture,
( v3_struct_0(esk27_0)
| u1_struct_0(esk27_0) != esk28_0
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[38378,636,theory(equality)]) ).
cnf(38380,negated_conjecture,
( v3_struct_0(esk27_0)
| u1_struct_0(esk27_0) != esk28_0
| $false
| $false ),
inference(rw,[status(thm)],[38379,638,theory(equality)]) ).
cnf(38381,negated_conjecture,
( v3_struct_0(esk27_0)
| u1_struct_0(esk27_0) != esk28_0 ),
inference(cn,[status(thm)],[38380,theory(equality)]) ).
cnf(38382,negated_conjecture,
u1_struct_0(esk27_0) != esk28_0,
inference(sr,[status(thm)],[38381,639,theory(equality)]) ).
cnf(38383,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(k1_lattice2(esk27_0))
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[38131,38382,theory(equality)]) ).
cnf(38384,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ v10_lattices(k1_lattice2(esk27_0)) ),
inference(csr,[status(thm)],[38383,38335]) ).
cnf(38385,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ l3_lattices(k1_lattice2(esk27_0))
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[38384,308,theory(equality)]) ).
cnf(38386,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ l3_lattices(k1_lattice2(esk27_0))
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[38385,636,theory(equality)]) ).
cnf(38387,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ l3_lattices(k1_lattice2(esk27_0))
| $false
| $false ),
inference(rw,[status(thm)],[38386,638,theory(equality)]) ).
cnf(38388,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| v3_struct_0(esk27_0)
| ~ l3_lattices(k1_lattice2(esk27_0)) ),
inference(cn,[status(thm)],[38387,theory(equality)]) ).
cnf(38389,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ l3_lattices(k1_lattice2(esk27_0)) ),
inference(sr,[status(thm)],[38388,639,theory(equality)]) ).
cnf(38390,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| ~ l3_lattices(esk27_0) ),
inference(spm,[status(thm)],[38389,476,theory(equality)]) ).
cnf(38391,negated_conjecture,
( k17_filter_2(esk27_0) = esk28_0
| $false ),
inference(rw,[status(thm)],[38390,636,theory(equality)]) ).
cnf(38392,negated_conjecture,
k17_filter_2(esk27_0) = esk28_0,
inference(cn,[status(thm)],[38391,theory(equality)]) ).
cnf(38394,negated_conjecture,
( esk28_0 = u1_struct_0(esk27_0)
| v3_struct_0(esk27_0)
| ~ l3_lattices(esk27_0)
| ~ v10_lattices(esk27_0) ),
inference(spm,[status(thm)],[350,38392,theory(equality)]) ).
cnf(38513,negated_conjecture,
( esk28_0 = u1_struct_0(esk27_0)
| v3_struct_0(esk27_0)
| $false
| ~ v10_lattices(esk27_0) ),
inference(rw,[status(thm)],[38394,636,theory(equality)]) ).
cnf(38514,negated_conjecture,
( esk28_0 = u1_struct_0(esk27_0)
| v3_struct_0(esk27_0)
| $false
| $false ),
inference(rw,[status(thm)],[38513,638,theory(equality)]) ).
cnf(38515,negated_conjecture,
( esk28_0 = u1_struct_0(esk27_0)
| v3_struct_0(esk27_0) ),
inference(cn,[status(thm)],[38514,theory(equality)]) ).
cnf(38516,negated_conjecture,
v3_struct_0(esk27_0),
inference(sr,[status(thm)],[38515,38382,theory(equality)]) ).
cnf(38517,negated_conjecture,
$false,
inference(sr,[status(thm)],[38516,639,theory(equality)]) ).
cnf(38518,negated_conjecture,
$false,
38517,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/LAT/LAT322+1.p
% --creating new selector for []
% -running prover on /tmp/tmpe1_y5v/sel_LAT322+1.p_1 with time limit 29
% -prover status Theorem
% Problem LAT322+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/LAT/LAT322+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/LAT/LAT322+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------