%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : LAT323+1 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art06.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:03:47 EST 2010
% Result : Theorem 1.50s
% Output : CNFRefutation 1.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 16
% Syntax : Number of formulae : 165 ( 12 unt; 0 def)
% Number of atoms : 1184 ( 29 equ)
% Maximal formula atoms : 80 ( 7 avg)
% Number of connectives : 1619 ( 600 ~; 710 |; 241 &)
% ( 9 <=>; 59 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 254 ( 0 sgn 146 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(4,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/tmpbHIJHi/sel_LAT323+1.p_1',redefinition_m1_filter_2) ).
fof(7,axiom,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1)
& m1_subset_1(X2,u1_struct_0(X1)) )
=> m1_subset_1(k5_filter_2(X1,X2),u1_struct_0(k1_lattice2(X1))) ),
file('/tmp/tmpbHIJHi/sel_LAT323+1.p_1',dt_k5_filter_2) ).
fof(11,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> k7_lattices(k1_lattice2(X1),k5_filter_2(X1,X2)) = k7_lattices(X1,X2) ) ),
file('/tmp/tmpbHIJHi/sel_LAT323+1.p_1',l70_filter_2) ).
fof(14,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/tmpbHIJHi/sel_LAT323+1.p_1',dt_k15_filter_2) ).
fof(30,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/tmpbHIJHi/sel_LAT323+1.p_1',t33_filter_2) ).
fof(34,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/tmpbHIJHi/sel_LAT323+1.p_1',fc6_lattice2) ).
fof(45,conjecture,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( r2_filter_2(X1,X2)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( r2_hidden(X3,X2)
<=> ~ r2_hidden(k7_lattices(X1,X3),X2) ) ) ) ) ),
file('/tmp/tmpbHIJHi/sel_LAT323+1.p_1',t59_filter_2) ).
fof(46,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_filter_0(X2,X1)
=> ( v1_filter_0(X2,X1)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( r2_hidden(X3,X2)
<=> ~ r2_hidden(k7_lattices(X1,X3),X2) ) ) ) ) ),
file('/tmp/tmpbHIJHi/sel_LAT323+1.p_1',t59_filter_0) ).
fof(48,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/tmpbHIJHi/sel_LAT323+1.p_1',dt_m2_filter_2) ).
fof(53,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> k5_filter_2(X1,X2) = X2 ) ),
file('/tmp/tmpbHIJHi/sel_LAT323+1.p_1',d4_filter_2) ).
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/tmpbHIJHi/sel_LAT323+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/tmpbHIJHi/sel_LAT323+1.p_1',fc1_lattice2) ).
fof(68,axiom,
! [X1] :
( l3_lattices(X1)
=> ( v3_lattices(k1_lattice2(X1))
& l3_lattices(k1_lattice2(X1)) ) ),
file('/tmp/tmpbHIJHi/sel_LAT323+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/tmpbHIJHi/sel_LAT323+1.p_1',fc4_filter_2) ).
fof(89,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/tmpbHIJHi/sel_LAT323+1.p_1',d6_filter_2) ).
fof(92,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/tmpbHIJHi/sel_LAT323+1.p_1',dt_m2_lattice4) ).
fof(97,negated_conjecture,
~ ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( r2_filter_2(X1,X2)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( r2_hidden(X3,X2)
<=> ~ r2_hidden(k7_lattices(X1,X3),X2) ) ) ) ) ),
inference(assume_negation,[status(cth)],[45]) ).
fof(98,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)],[4,theory(equality)]) ).
fof(100,plain,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1)
& m1_subset_1(X2,u1_struct_0(X1)) )
=> m1_subset_1(k5_filter_2(X1,X2),u1_struct_0(k1_lattice2(X1))) ),
inference(fof_simplification,[status(thm)],[7,theory(equality)]) ).
fof(103,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> k7_lattices(k1_lattice2(X1),k5_filter_2(X1,X2)) = k7_lattices(X1,X2) ) ),
inference(fof_simplification,[status(thm)],[11,theory(equality)]) ).
fof(106,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)],[14,theory(equality)]) ).
fof(112,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)],[30,theory(equality)]) ).
fof(114,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)],[34,theory(equality)]) ).
fof(121,negated_conjecture,
~ ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m2_filter_2(X2,X1)
=> ( r2_filter_2(X1,X2)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( r2_hidden(X3,X2)
<=> ~ r2_hidden(k7_lattices(X1,X3),X2) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[97,theory(equality)]) ).
fof(122,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_filter_0(X2,X1)
=> ( v1_filter_0(X2,X1)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( r2_hidden(X3,X2)
<=> ~ r2_hidden(k7_lattices(X1,X3),X2) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[46,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)],[48,theory(equality)]) ).
fof(125,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> k5_filter_2(X1,X2) = X2 ) ),
inference(fof_simplification,[status(thm)],[53,theory(equality)]) ).
fof(131,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(133,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(139,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(145,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)],[89,theory(equality)]) ).
fof(146,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)],[92,theory(equality)]) ).
fof(159,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)],[98]) ).
fof(160,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)],[159]) ).
fof(161,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)],[160]) ).
fof(162,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)],[161]) ).
cnf(164,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)],[162]) ).
fof(186,plain,
! [X1,X2] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| m1_subset_1(k5_filter_2(X1,X2),u1_struct_0(k1_lattice2(X1))) ),
inference(fof_nnf,[status(thm)],[100]) ).
fof(187,plain,
! [X3,X4] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ~ m1_subset_1(X4,u1_struct_0(X3))
| m1_subset_1(k5_filter_2(X3,X4),u1_struct_0(k1_lattice2(X3))) ),
inference(variable_rename,[status(thm)],[186]) ).
cnf(188,plain,
( m1_subset_1(k5_filter_2(X1,X2),u1_struct_0(k1_lattice2(X1)))
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(split_conjunct,[status(thm)],[187]) ).
fof(201,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
| k7_lattices(k1_lattice2(X1),k5_filter_2(X1,X2)) = k7_lattices(X1,X2) ) ),
inference(fof_nnf,[status(thm)],[103]) ).
fof(202,plain,
! [X3] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ v17_lattices(X3)
| ~ l3_lattices(X3)
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X3))
| k7_lattices(k1_lattice2(X3),k5_filter_2(X3,X4)) = k7_lattices(X3,X4) ) ),
inference(variable_rename,[status(thm)],[201]) ).
fof(203,plain,
! [X3,X4] :
( ~ m1_subset_1(X4,u1_struct_0(X3))
| k7_lattices(k1_lattice2(X3),k5_filter_2(X3,X4)) = k7_lattices(X3,X4)
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ v17_lattices(X3)
| ~ l3_lattices(X3) ),
inference(shift_quantors,[status(thm)],[202]) ).
cnf(204,plain,
( v3_struct_0(X1)
| k7_lattices(k1_lattice2(X1),k5_filter_2(X1,X2)) = k7_lattices(X1,X2)
| ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(split_conjunct,[status(thm)],[203]) ).
fof(215,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)],[106]) ).
fof(216,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)],[215]) ).
cnf(217,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)],[216]) ).
fof(284,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)],[112]) ).
fof(285,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)],[284]) ).
fof(286,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)],[285]) ).
fof(287,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)],[286]) ).
cnf(289,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)],[287]) ).
fof(303,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)],[114]) ).
fof(304,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)],[303]) ).
fof(305,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)],[304]) ).
cnf(306,plain,
( v3_struct_0(X1)
| v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1) ),
inference(split_conjunct,[status(thm)],[305]) ).
fof(367,negated_conjecture,
? [X1] :
( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1)
& ? [X2] :
( m2_filter_2(X2,X1)
& r2_filter_2(X1,X2)
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
& ( ~ r2_hidden(X3,X2)
| r2_hidden(k7_lattices(X1,X3),X2) )
& ( r2_hidden(X3,X2)
| ~ r2_hidden(k7_lattices(X1,X3),X2) ) ) ) ),
inference(fof_nnf,[status(thm)],[121]) ).
fof(368,negated_conjecture,
? [X4] :
( ~ v3_struct_0(X4)
& v10_lattices(X4)
& v17_lattices(X4)
& l3_lattices(X4)
& ? [X5] :
( m2_filter_2(X5,X4)
& r2_filter_2(X4,X5)
& ? [X6] :
( m1_subset_1(X6,u1_struct_0(X4))
& ( ~ r2_hidden(X6,X5)
| r2_hidden(k7_lattices(X4,X6),X5) )
& ( r2_hidden(X6,X5)
| ~ r2_hidden(k7_lattices(X4,X6),X5) ) ) ) ),
inference(variable_rename,[status(thm)],[367]) ).
fof(369,negated_conjecture,
( ~ v3_struct_0(esk16_0)
& v10_lattices(esk16_0)
& v17_lattices(esk16_0)
& l3_lattices(esk16_0)
& m2_filter_2(esk17_0,esk16_0)
& r2_filter_2(esk16_0,esk17_0)
& m1_subset_1(esk18_0,u1_struct_0(esk16_0))
& ( ~ r2_hidden(esk18_0,esk17_0)
| r2_hidden(k7_lattices(esk16_0,esk18_0),esk17_0) )
& ( r2_hidden(esk18_0,esk17_0)
| ~ r2_hidden(k7_lattices(esk16_0,esk18_0),esk17_0) ) ),
inference(skolemize,[status(esa)],[368]) ).
cnf(370,negated_conjecture,
( r2_hidden(esk18_0,esk17_0)
| ~ r2_hidden(k7_lattices(esk16_0,esk18_0),esk17_0) ),
inference(split_conjunct,[status(thm)],[369]) ).
cnf(371,negated_conjecture,
( r2_hidden(k7_lattices(esk16_0,esk18_0),esk17_0)
| ~ r2_hidden(esk18_0,esk17_0) ),
inference(split_conjunct,[status(thm)],[369]) ).
cnf(372,negated_conjecture,
m1_subset_1(esk18_0,u1_struct_0(esk16_0)),
inference(split_conjunct,[status(thm)],[369]) ).
cnf(373,negated_conjecture,
r2_filter_2(esk16_0,esk17_0),
inference(split_conjunct,[status(thm)],[369]) ).
cnf(374,negated_conjecture,
m2_filter_2(esk17_0,esk16_0),
inference(split_conjunct,[status(thm)],[369]) ).
cnf(375,negated_conjecture,
l3_lattices(esk16_0),
inference(split_conjunct,[status(thm)],[369]) ).
cnf(376,negated_conjecture,
v17_lattices(esk16_0),
inference(split_conjunct,[status(thm)],[369]) ).
cnf(377,negated_conjecture,
v10_lattices(esk16_0),
inference(split_conjunct,[status(thm)],[369]) ).
cnf(378,negated_conjecture,
~ v3_struct_0(esk16_0),
inference(split_conjunct,[status(thm)],[369]) ).
fof(379,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1)
| ! [X2] :
( ~ m1_filter_0(X2,X1)
| ~ v1_filter_0(X2,X1)
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X1))
| ( ( ~ r2_hidden(X3,X2)
| ~ r2_hidden(k7_lattices(X1,X3),X2) )
& ( r2_hidden(k7_lattices(X1,X3),X2)
| r2_hidden(X3,X2) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[122]) ).
fof(380,plain,
! [X4] :
( v3_struct_0(X4)
| ~ v10_lattices(X4)
| ~ v17_lattices(X4)
| ~ l3_lattices(X4)
| ! [X5] :
( ~ m1_filter_0(X5,X4)
| ~ v1_filter_0(X5,X4)
| ! [X6] :
( ~ m1_subset_1(X6,u1_struct_0(X4))
| ( ( ~ r2_hidden(X6,X5)
| ~ r2_hidden(k7_lattices(X4,X6),X5) )
& ( r2_hidden(k7_lattices(X4,X6),X5)
| r2_hidden(X6,X5) ) ) ) ) ),
inference(variable_rename,[status(thm)],[379]) ).
fof(381,plain,
! [X4,X5,X6] :
( ~ m1_subset_1(X6,u1_struct_0(X4))
| ( ( ~ r2_hidden(X6,X5)
| ~ r2_hidden(k7_lattices(X4,X6),X5) )
& ( r2_hidden(k7_lattices(X4,X6),X5)
| r2_hidden(X6,X5) ) )
| ~ v1_filter_0(X5,X4)
| ~ m1_filter_0(X5,X4)
| v3_struct_0(X4)
| ~ v10_lattices(X4)
| ~ v17_lattices(X4)
| ~ l3_lattices(X4) ),
inference(shift_quantors,[status(thm)],[380]) ).
fof(382,plain,
! [X4,X5,X6] :
( ( ~ r2_hidden(X6,X5)
| ~ r2_hidden(k7_lattices(X4,X6),X5)
| ~ m1_subset_1(X6,u1_struct_0(X4))
| ~ v1_filter_0(X5,X4)
| ~ m1_filter_0(X5,X4)
| v3_struct_0(X4)
| ~ v10_lattices(X4)
| ~ v17_lattices(X4)
| ~ l3_lattices(X4) )
& ( r2_hidden(k7_lattices(X4,X6),X5)
| r2_hidden(X6,X5)
| ~ m1_subset_1(X6,u1_struct_0(X4))
| ~ v1_filter_0(X5,X4)
| ~ m1_filter_0(X5,X4)
| v3_struct_0(X4)
| ~ v10_lattices(X4)
| ~ v17_lattices(X4)
| ~ l3_lattices(X4) ) ),
inference(distribute,[status(thm)],[381]) ).
cnf(383,plain,
( v3_struct_0(X1)
| r2_hidden(X3,X2)
| r2_hidden(k7_lattices(X1,X3),X2)
| ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_filter_0(X2,X1)
| ~ v1_filter_0(X2,X1)
| ~ m1_subset_1(X3,u1_struct_0(X1)) ),
inference(split_conjunct,[status(thm)],[382]) ).
cnf(384,plain,
( v3_struct_0(X1)
| ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_filter_0(X2,X1)
| ~ v1_filter_0(X2,X1)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ r2_hidden(k7_lattices(X1,X3),X2)
| ~ r2_hidden(X3,X2) ),
inference(split_conjunct,[status(thm)],[382]) ).
fof(388,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(389,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)],[388]) ).
fof(390,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)],[389]) ).
fof(391,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)],[390]) ).
cnf(392,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)],[391]) ).
fof(408,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
| k5_filter_2(X1,X2) = X2 ) ),
inference(fof_nnf,[status(thm)],[125]) ).
fof(409,plain,
! [X3] :
( v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3)
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X3))
| k5_filter_2(X3,X4) = X4 ) ),
inference(variable_rename,[status(thm)],[408]) ).
fof(410,plain,
! [X3,X4] :
( ~ m1_subset_1(X4,u1_struct_0(X3))
| k5_filter_2(X3,X4) = X4
| v3_struct_0(X3)
| ~ v10_lattices(X3)
| ~ l3_lattices(X3) ),
inference(shift_quantors,[status(thm)],[409]) ).
cnf(411,plain,
( v3_struct_0(X1)
| k5_filter_2(X1,X2) = X2
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(split_conjunct,[status(thm)],[410]) ).
fof(462,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)],[131]) ).
fof(463,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)],[462]) ).
cnf(464,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)],[463]) ).
fof(473,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)],[133]) ).
fof(474,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)],[473]) ).
fof(475,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)],[474]) ).
cnf(477,plain,
( v3_struct_0(X1)
| ~ l3_lattices(X1)
| ~ v3_struct_0(k1_lattice2(X1)) ),
inference(split_conjunct,[status(thm)],[475]) ).
fof(478,plain,
! [X1] :
( ~ l3_lattices(X1)
| ( v3_lattices(k1_lattice2(X1))
& l3_lattices(k1_lattice2(X1)) ) ),
inference(fof_nnf,[status(thm)],[68]) ).
fof(479,plain,
! [X2] :
( ~ l3_lattices(X2)
| ( v3_lattices(k1_lattice2(X2))
& l3_lattices(k1_lattice2(X2)) ) ),
inference(variable_rename,[status(thm)],[478]) ).
fof(480,plain,
! [X2] :
( ( v3_lattices(k1_lattice2(X2))
| ~ l3_lattices(X2) )
& ( l3_lattices(k1_lattice2(X2))
| ~ l3_lattices(X2) ) ),
inference(distribute,[status(thm)],[479]) ).
cnf(481,plain,
( l3_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[480]) ).
fof(528,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)],[139]) ).
fof(529,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)],[528]) ).
fof(530,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)],[529]) ).
cnf(531,plain,
( v3_struct_0(X1)
| v17_lattices(k1_lattice2(X1))
| ~ l3_lattices(X1)
| ~ v17_lattices(X1)
| ~ v10_lattices(X1) ),
inference(split_conjunct,[status(thm)],[530]) ).
fof(604,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)],[145]) ).
fof(605,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)],[604]) ).
fof(606,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)],[605]) ).
cnf(607,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)],[606]) ).
fof(614,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)],[146]) ).
fof(615,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)],[614]) ).
fof(616,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)],[615]) ).
cnf(617,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)],[616]) ).
cnf(735,negated_conjecture,
( k5_filter_2(esk16_0,esk18_0) = esk18_0
| v3_struct_0(esk16_0)
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(spm,[status(thm)],[411,372,theory(equality)]) ).
cnf(738,negated_conjecture,
( k5_filter_2(esk16_0,esk18_0) = esk18_0
| v3_struct_0(esk16_0)
| $false
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[735,377,theory(equality)]) ).
cnf(739,negated_conjecture,
( k5_filter_2(esk16_0,esk18_0) = esk18_0
| v3_struct_0(esk16_0)
| $false
| $false ),
inference(rw,[status(thm)],[738,375,theory(equality)]) ).
cnf(740,negated_conjecture,
( k5_filter_2(esk16_0,esk18_0) = esk18_0
| v3_struct_0(esk16_0) ),
inference(cn,[status(thm)],[739,theory(equality)]) ).
cnf(741,negated_conjecture,
k5_filter_2(esk16_0,esk18_0) = esk18_0,
inference(sr,[status(thm)],[740,378,theory(equality)]) ).
cnf(773,plain,
( k7_filter_2(X1,X2) = X2
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_lattice4(X2,X1) ),
inference(spm,[status(thm)],[607,617,theory(equality)]) ).
cnf(776,plain,
( m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ m2_filter_2(X2,X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(spm,[status(thm)],[164,217,theory(equality)]) ).
cnf(829,plain,
( v1_filter_0(k7_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(X1)
| ~ r2_filter_2(X1,X2)
| ~ m2_filter_2(X2,X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(spm,[status(thm)],[289,464,theory(equality)]) ).
cnf(856,plain,
( r2_hidden(k7_lattices(X1,X2),X3)
| r2_hidden(k5_filter_2(X1,X2),X3)
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_0(X3,k1_lattice2(X1))
| ~ m1_subset_1(k5_filter_2(X1,X2),u1_struct_0(k1_lattice2(X1)))
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(X3,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v17_lattices(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(spm,[status(thm)],[383,204,theory(equality)]) ).
cnf(865,plain,
( v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_0(X2,k1_lattice2(X1))
| ~ m1_subset_1(k5_filter_2(X1,X3),u1_struct_0(k1_lattice2(X1)))
| ~ r2_hidden(k7_lattices(X1,X3),X2)
| ~ r2_hidden(k5_filter_2(X1,X3),X2)
| ~ v17_lattices(k1_lattice2(X1))
| ~ m1_filter_0(X2,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v17_lattices(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(spm,[status(thm)],[384,204,theory(equality)]) ).
cnf(1639,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)
| ~ v10_lattices(k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[776,481]) ).
cnf(1640,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)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[1639,306]) ).
cnf(1641,plain,
( m1_filter_0(k15_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[1640,477]) ).
cnf(1643,plain,
( m1_filter_0(k7_filter_2(X1,X2),k1_lattice2(X1))
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(spm,[status(thm)],[1641,464,theory(equality)]) ).
cnf(1767,plain,
( v1_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(X1)
| ~ r2_filter_2(X1,X2)
| ~ m2_filter_2(X2,X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_lattice4(X2,X1) ),
inference(spm,[status(thm)],[829,773,theory(equality)]) ).
cnf(2497,plain,
( r2_hidden(k7_lattices(X1,X2),X3)
| r2_hidden(k5_filter_2(X1,X2),X3)
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_0(X3,k1_lattice2(X1))
| ~ m1_subset_1(k5_filter_2(X1,X2),u1_struct_0(k1_lattice2(X1)))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v17_lattices(k1_lattice2(X1))
| ~ v17_lattices(X1)
| ~ m1_filter_0(X3,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[856,481]) ).
cnf(2498,plain,
( r2_hidden(k7_lattices(X1,X2),X3)
| r2_hidden(k5_filter_2(X1,X2),X3)
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_0(X3,k1_lattice2(X1))
| ~ m1_subset_1(k5_filter_2(X1,X2),u1_struct_0(k1_lattice2(X1)))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v17_lattices(k1_lattice2(X1))
| ~ v17_lattices(X1)
| ~ m1_filter_0(X3,k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[2497,306]) ).
cnf(2499,plain,
( r2_hidden(k7_lattices(X1,X2),X3)
| r2_hidden(k5_filter_2(X1,X2),X3)
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_0(X3,k1_lattice2(X1))
| ~ m1_subset_1(k5_filter_2(X1,X2),u1_struct_0(k1_lattice2(X1)))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v17_lattices(X1)
| ~ m1_filter_0(X3,k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[2498,531]) ).
cnf(2500,plain,
( r2_hidden(k7_lattices(X1,X2),X3)
| r2_hidden(k5_filter_2(X1,X2),X3)
| v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_0(X3,k1_lattice2(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v17_lattices(X1)
| ~ m1_filter_0(X3,k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[2499,188]) ).
cnf(2501,plain,
( r2_hidden(k7_lattices(X1,X2),X3)
| r2_hidden(k5_filter_2(X1,X2),X3)
| v3_struct_0(X1)
| ~ v1_filter_0(X3,k1_lattice2(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v17_lattices(X1)
| ~ m1_filter_0(X3,k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[2500,477]) ).
cnf(2502,negated_conjecture,
( r2_hidden(esk18_0,X1)
| r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| ~ m1_subset_1(esk18_0,u1_struct_0(esk16_0))
| ~ v17_lattices(esk16_0)
| ~ m1_filter_0(X1,k1_lattice2(esk16_0))
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(spm,[status(thm)],[2501,741,theory(equality)]) ).
cnf(2545,negated_conjecture,
( r2_hidden(esk18_0,X1)
| r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| ~ v17_lattices(esk16_0)
| ~ m1_filter_0(X1,k1_lattice2(esk16_0))
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[2502,372,theory(equality)]) ).
cnf(2546,negated_conjecture,
( r2_hidden(esk18_0,X1)
| r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| $false
| ~ m1_filter_0(X1,k1_lattice2(esk16_0))
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[2545,376,theory(equality)]) ).
cnf(2547,negated_conjecture,
( r2_hidden(esk18_0,X1)
| r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| $false
| ~ m1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[2546,377,theory(equality)]) ).
cnf(2548,negated_conjecture,
( r2_hidden(esk18_0,X1)
| r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| $false
| ~ m1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| $false ),
inference(rw,[status(thm)],[2547,375,theory(equality)]) ).
cnf(2549,negated_conjecture,
( r2_hidden(esk18_0,X1)
| r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| ~ m1_filter_0(X1,k1_lattice2(esk16_0)) ),
inference(cn,[status(thm)],[2548,theory(equality)]) ).
cnf(2550,negated_conjecture,
( r2_hidden(esk18_0,X1)
| r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| ~ m1_filter_0(X1,k1_lattice2(esk16_0)) ),
inference(sr,[status(thm)],[2549,378,theory(equality)]) ).
cnf(2697,plain,
( v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_0(X2,k1_lattice2(X1))
| ~ m1_subset_1(k5_filter_2(X1,X3),u1_struct_0(k1_lattice2(X1)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ r2_hidden(k7_lattices(X1,X3),X2)
| ~ r2_hidden(k5_filter_2(X1,X3),X2)
| ~ v17_lattices(k1_lattice2(X1))
| ~ v17_lattices(X1)
| ~ m1_filter_0(X2,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[865,481]) ).
cnf(2698,plain,
( v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_0(X2,k1_lattice2(X1))
| ~ m1_subset_1(k5_filter_2(X1,X3),u1_struct_0(k1_lattice2(X1)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ r2_hidden(k7_lattices(X1,X3),X2)
| ~ r2_hidden(k5_filter_2(X1,X3),X2)
| ~ v17_lattices(k1_lattice2(X1))
| ~ v17_lattices(X1)
| ~ m1_filter_0(X2,k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[2697,306]) ).
cnf(2699,plain,
( v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_0(X2,k1_lattice2(X1))
| ~ m1_subset_1(k5_filter_2(X1,X3),u1_struct_0(k1_lattice2(X1)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ r2_hidden(k7_lattices(X1,X3),X2)
| ~ r2_hidden(k5_filter_2(X1,X3),X2)
| ~ v17_lattices(X1)
| ~ m1_filter_0(X2,k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[2698,531]) ).
cnf(2700,plain,
( v3_struct_0(k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v1_filter_0(X2,k1_lattice2(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ r2_hidden(k7_lattices(X1,X3),X2)
| ~ r2_hidden(k5_filter_2(X1,X3),X2)
| ~ v17_lattices(X1)
| ~ m1_filter_0(X2,k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[2699,188]) ).
cnf(2701,plain,
( v3_struct_0(X1)
| ~ v1_filter_0(X2,k1_lattice2(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ r2_hidden(k7_lattices(X1,X3),X2)
| ~ r2_hidden(k5_filter_2(X1,X3),X2)
| ~ v17_lattices(X1)
| ~ m1_filter_0(X2,k1_lattice2(X1))
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[2700,477]) ).
cnf(2702,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| ~ m1_subset_1(esk18_0,u1_struct_0(esk16_0))
| ~ r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| ~ r2_hidden(esk18_0,X1)
| ~ v17_lattices(esk16_0)
| ~ m1_filter_0(X1,k1_lattice2(esk16_0))
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(spm,[status(thm)],[2701,741,theory(equality)]) ).
cnf(2721,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| ~ r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| ~ r2_hidden(esk18_0,X1)
| ~ v17_lattices(esk16_0)
| ~ m1_filter_0(X1,k1_lattice2(esk16_0))
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[2702,372,theory(equality)]) ).
cnf(2722,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| ~ r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| ~ r2_hidden(esk18_0,X1)
| $false
| ~ m1_filter_0(X1,k1_lattice2(esk16_0))
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[2721,376,theory(equality)]) ).
cnf(2723,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| ~ r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| ~ r2_hidden(esk18_0,X1)
| $false
| ~ m1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[2722,377,theory(equality)]) ).
cnf(2724,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| ~ r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| ~ r2_hidden(esk18_0,X1)
| $false
| ~ m1_filter_0(X1,k1_lattice2(esk16_0))
| $false
| $false ),
inference(rw,[status(thm)],[2723,375,theory(equality)]) ).
cnf(2725,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| ~ r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| ~ r2_hidden(esk18_0,X1)
| ~ m1_filter_0(X1,k1_lattice2(esk16_0)) ),
inference(cn,[status(thm)],[2724,theory(equality)]) ).
cnf(2726,negated_conjecture,
( ~ v1_filter_0(X1,k1_lattice2(esk16_0))
| ~ r2_hidden(k7_lattices(esk16_0,esk18_0),X1)
| ~ r2_hidden(esk18_0,X1)
| ~ m1_filter_0(X1,k1_lattice2(esk16_0)) ),
inference(sr,[status(thm)],[2725,378,theory(equality)]) ).
cnf(2994,negated_conjecture,
( r2_hidden(esk18_0,esk17_0)
| ~ v1_filter_0(esk17_0,k1_lattice2(esk16_0))
| ~ m1_filter_0(esk17_0,k1_lattice2(esk16_0)) ),
inference(spm,[status(thm)],[370,2550,theory(equality)]) ).
cnf(3059,negated_conjecture,
( ~ v1_filter_0(esk17_0,k1_lattice2(esk16_0))
| ~ r2_hidden(esk18_0,esk17_0)
| ~ m1_filter_0(esk17_0,k1_lattice2(esk16_0)) ),
inference(spm,[status(thm)],[2726,371,theory(equality)]) ).
cnf(3070,negated_conjecture,
( ~ v1_filter_0(esk17_0,k1_lattice2(esk16_0))
| ~ m1_filter_0(esk17_0,k1_lattice2(esk16_0)) ),
inference(csr,[status(thm)],[3059,2994]) ).
cnf(5276,plain,
( m1_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_lattice4(X2,X1) ),
inference(spm,[status(thm)],[1643,773,theory(equality)]) ).
cnf(5356,plain,
( m1_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(X1)
| ~ m2_filter_2(X2,X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[5276,392]) ).
cnf(10341,plain,
( v1_filter_0(X2,k1_lattice2(X1))
| v3_struct_0(X1)
| ~ r2_filter_2(X1,X2)
| ~ m2_filter_2(X2,X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[1767,392]) ).
cnf(10346,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ m1_filter_0(esk17_0,k1_lattice2(esk16_0))
| ~ r2_filter_2(esk16_0,esk17_0)
| ~ m2_filter_2(esk17_0,esk16_0)
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(spm,[status(thm)],[3070,10341,theory(equality)]) ).
cnf(10377,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ m1_filter_0(esk17_0,k1_lattice2(esk16_0))
| $false
| ~ m2_filter_2(esk17_0,esk16_0)
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[10346,373,theory(equality)]) ).
cnf(10378,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ m1_filter_0(esk17_0,k1_lattice2(esk16_0))
| $false
| $false
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[10377,374,theory(equality)]) ).
cnf(10379,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ m1_filter_0(esk17_0,k1_lattice2(esk16_0))
| $false
| $false
| $false
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[10378,377,theory(equality)]) ).
cnf(10380,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ m1_filter_0(esk17_0,k1_lattice2(esk16_0))
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[10379,375,theory(equality)]) ).
cnf(10381,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ m1_filter_0(esk17_0,k1_lattice2(esk16_0)) ),
inference(cn,[status(thm)],[10380,theory(equality)]) ).
cnf(10382,negated_conjecture,
~ m1_filter_0(esk17_0,k1_lattice2(esk16_0)),
inference(sr,[status(thm)],[10381,378,theory(equality)]) ).
cnf(10435,negated_conjecture,
( v3_struct_0(esk16_0)
| ~ m2_filter_2(esk17_0,esk16_0)
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(spm,[status(thm)],[10382,5356,theory(equality)]) ).
cnf(10436,negated_conjecture,
( v3_struct_0(esk16_0)
| $false
| ~ v10_lattices(esk16_0)
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[10435,374,theory(equality)]) ).
cnf(10437,negated_conjecture,
( v3_struct_0(esk16_0)
| $false
| $false
| ~ l3_lattices(esk16_0) ),
inference(rw,[status(thm)],[10436,377,theory(equality)]) ).
cnf(10438,negated_conjecture,
( v3_struct_0(esk16_0)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[10437,375,theory(equality)]) ).
cnf(10439,negated_conjecture,
v3_struct_0(esk16_0),
inference(cn,[status(thm)],[10438,theory(equality)]) ).
cnf(10440,negated_conjecture,
$false,
inference(sr,[status(thm)],[10439,378,theory(equality)]) ).
cnf(10441,negated_conjecture,
$false,
10440,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/LAT/LAT323+1.p
% --creating new selector for []
% -running prover on /tmp/tmpbHIJHi/sel_LAT323+1.p_1 with time limit 29
% -prover status Theorem
% Problem LAT323+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/LAT/LAT323+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/LAT/LAT323+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
%
%------------------------------------------------------------------------------