%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LAT323+1 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %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 : Wed Dec 29 10:49:29 EST 2010
% Result : Theorem 1.47s
% Output : Solution 1.47s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP10424/LAT323+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP10424/LAT323+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP10424/LAT323+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 10520
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.029 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(7, 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/SRASS.s.p', t59_filter_0)).
% fof(10, 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/SRASS.s.p', dt_m2_lattice4)).
% fof(14, 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/SRASS.s.p', l70_filter_2)).
% fof(15, 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/SRASS.s.p', d4_filter_2)).
% fof(16, 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/SRASS.s.p', dt_k5_filter_2)).
% fof(17, 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/SRASS.s.p', dt_m2_filter_2)).
% fof(20, 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/SRASS.s.p', t33_filter_2)).
% fof(21, 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/SRASS.s.p', d6_filter_2)).
% fof(31, 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/SRASS.s.p', dt_k15_filter_2)).
% fof(32, 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/SRASS.s.p', redefinition_k15_filter_2)).
% fof(37, 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/SRASS.s.p', redefinition_m1_filter_2)).
% fof(39, axiom,![X1]:((~(v3_struct_0(X1))&l3_lattices(X1))=>(~(v3_struct_0(k1_lattice2(X1)))&v3_lattices(k1_lattice2(X1)))),file('/tmp/SRASS.s.p', fc1_lattice2)).
% fof(46, axiom,![X1]:(l3_lattices(X1)=>(v3_lattices(k1_lattice2(X1))&l3_lattices(k1_lattice2(X1)))),file('/tmp/SRASS.s.p', 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/SRASS.s.p', fc4_filter_2)).
% fof(79, 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/SRASS.s.p', fc6_lattice2)).
% fof(96, 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/SRASS.s.p', t59_filter_2)).
% 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)],[96])).
% fof(101, 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)],[7,theory(equality)])).
% fof(102, 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)],[10,theory(equality)])).
% fof(106, 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)],[14,theory(equality)])).
% fof(107, 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)],[15,theory(equality)])).
% fof(108, 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)],[16,theory(equality)])).
% fof(109, 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)],[17,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)],[20,theory(equality)])).
% fof(113, 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)],[21,theory(equality)])).
% fof(119, 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)],[31,theory(equality)])).
% fof(120, 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)],[32,theory(equality)])).
% fof(124, 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)],[37,theory(equality)])).
% fof(126, 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)],[39,theory(equality)])).
% fof(140, 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(142, 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)],[79,theory(equality)])).
% fof(148, 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(168, 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)],[101])).
% fof(169, 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)],[168])).
% fof(170, 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)],[169])).
% fof(171, 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)],[170])).
% cnf(172,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)],[171])).
% cnf(173,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)],[171])).
% fof(180, 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)],[102])).
% fof(181, 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)],[180])).
% fof(182, 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)],[181])).
% cnf(183,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)],[182])).
% fof(196, 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)],[106])).
% fof(197, 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)],[196])).
% fof(198, 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)],[197])).
% cnf(199,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)],[198])).
% fof(200, 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)],[107])).
% fof(201, 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)],[200])).
% fof(202, 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)],[201])).
% cnf(203,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)],[202])).
% fof(204, 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)],[108])).
% fof(205, 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)],[204])).
% cnf(206,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)],[205])).
% fof(207, 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)],[109])).
% fof(208, 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)],[207])).
% fof(209, 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)],[208])).
% fof(210, 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)],[209])).
% cnf(211,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)],[210])).
% fof(222, 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(223, 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)],[222])).
% fof(224, 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)],[223])).
% fof(225, 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)],[224])).
% cnf(227,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)],[225])).
% fof(228, 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)],[113])).
% fof(229, 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)],[228])).
% fof(230, 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)],[229])).
% cnf(231,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)],[230])).
% fof(263, 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)],[119])).
% fof(264, 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)],[263])).
% cnf(265,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)],[264])).
% fof(266, 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)],[120])).
% fof(267, 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)],[266])).
% cnf(268,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)],[267])).
% fof(287, 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)],[124])).
% fof(288, 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)],[287])).
% fof(289, 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)],[288])).
% fof(290, 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)],[289])).
% cnf(292,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)],[290])).
% fof(297, 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)],[126])).
% fof(298, 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)],[297])).
% fof(299, 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)],[298])).
% cnf(301,plain,(v3_struct_0(X1)|~l3_lattices(X1)|~v3_struct_0(k1_lattice2(X1))),inference(split_conjunct,[status(thm)],[299])).
% fof(323, plain,![X1]:(~(l3_lattices(X1))|(v3_lattices(k1_lattice2(X1))&l3_lattices(k1_lattice2(X1)))),inference(fof_nnf,[status(thm)],[46])).
% fof(324, plain,![X2]:(~(l3_lattices(X2))|(v3_lattices(k1_lattice2(X2))&l3_lattices(k1_lattice2(X2)))),inference(variable_rename,[status(thm)],[323])).
% fof(325, plain,![X2]:((v3_lattices(k1_lattice2(X2))|~(l3_lattices(X2)))&(l3_lattices(k1_lattice2(X2))|~(l3_lattices(X2)))),inference(distribute,[status(thm)],[324])).
% cnf(326,plain,(l3_lattices(k1_lattice2(X1))|~l3_lattices(X1)),inference(split_conjunct,[status(thm)],[325])).
% fof(498, 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)],[140])).
% fof(499, 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)],[498])).
% fof(500, 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)],[499])).
% cnf(501,plain,(v3_struct_0(X1)|v17_lattices(k1_lattice2(X1))|~l3_lattices(X1)|~v17_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[500])).
% fof(544, 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)],[142])).
% fof(545, 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)],[544])).
% fof(546, 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)],[545])).
% cnf(547,plain,(v3_struct_0(X1)|v10_lattices(k1_lattice2(X1))|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[546])).
% fof(624, 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)],[148])).
% fof(625, 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)],[624])).
% fof(626, negated_conjecture,((((~(v3_struct_0(esk29_0))&v10_lattices(esk29_0))&v17_lattices(esk29_0))&l3_lattices(esk29_0))&(m2_filter_2(esk30_0,esk29_0)&(r2_filter_2(esk29_0,esk30_0)&(m1_subset_1(esk31_0,u1_struct_0(esk29_0))&((~(r2_hidden(esk31_0,esk30_0))|r2_hidden(k7_lattices(esk29_0,esk31_0),esk30_0))&(r2_hidden(esk31_0,esk30_0)|~(r2_hidden(k7_lattices(esk29_0,esk31_0),esk30_0)))))))),inference(skolemize,[status(esa)],[625])).
% cnf(627,negated_conjecture,(r2_hidden(esk31_0,esk30_0)|~r2_hidden(k7_lattices(esk29_0,esk31_0),esk30_0)),inference(split_conjunct,[status(thm)],[626])).
% cnf(628,negated_conjecture,(r2_hidden(k7_lattices(esk29_0,esk31_0),esk30_0)|~r2_hidden(esk31_0,esk30_0)),inference(split_conjunct,[status(thm)],[626])).
% cnf(629,negated_conjecture,(m1_subset_1(esk31_0,u1_struct_0(esk29_0))),inference(split_conjunct,[status(thm)],[626])).
% cnf(630,negated_conjecture,(r2_filter_2(esk29_0,esk30_0)),inference(split_conjunct,[status(thm)],[626])).
% cnf(631,negated_conjecture,(m2_filter_2(esk30_0,esk29_0)),inference(split_conjunct,[status(thm)],[626])).
% cnf(632,negated_conjecture,(l3_lattices(esk29_0)),inference(split_conjunct,[status(thm)],[626])).
% cnf(633,negated_conjecture,(v17_lattices(esk29_0)),inference(split_conjunct,[status(thm)],[626])).
% cnf(634,negated_conjecture,(v10_lattices(esk29_0)),inference(split_conjunct,[status(thm)],[626])).
% cnf(635,negated_conjecture,(~v3_struct_0(esk29_0)),inference(split_conjunct,[status(thm)],[626])).
% cnf(761,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)],[231,183,theory(equality)])).
% cnf(812,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)],[292,265,theory(equality)])).
% cnf(813,plain,(m1_subset_1(X2,u1_struct_0(k1_lattice2(X1)))|v3_struct_0(X1)|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~l3_lattices(X1)),inference(spm,[status(thm)],[206,203,theory(equality)])).
% cnf(816,plain,(k7_lattices(k1_lattice2(X1),X2)=k7_lattices(X1,X2)|v3_struct_0(X1)|~v17_lattices(X1)|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~l3_lattices(X1)),inference(spm,[status(thm)],[199,203,theory(equality)])).
% cnf(818,plain,(v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|~v1_filter_0(X2,k1_lattice2(X1))|~m1_filter_0(X2,k1_lattice2(X1))|~v17_lattices(k1_lattice2(X1))|~v10_lattices(k1_lattice2(X1))|~m1_subset_1(k5_filter_2(X1,X3),u1_struct_0(k1_lattice2(X1)))|~l3_lattices(k1_lattice2(X1))|~r2_hidden(k7_lattices(X1,X3),X2)|~r2_hidden(k5_filter_2(X1,X3),X2)|~v17_lattices(X1)|~v10_lattices(X1)|~m1_subset_1(X3,u1_struct_0(X1))|~l3_lattices(X1)),inference(spm,[status(thm)],[173,199,theory(equality)])).
% cnf(996,plain,(X2=k15_filter_2(X1,X2)|v3_struct_0(X1)|~m2_filter_2(X2,X1)|~v10_lattices(X1)|~l3_lattices(X1)|~m2_lattice4(X2,X1)),inference(spm,[status(thm)],[268,761,theory(equality)])).
% cnf(1033,plain,(k15_filter_2(X1,X2)=X2|v3_struct_0(X1)|~m2_filter_2(X2,X1)|~v10_lattices(X1)|~l3_lattices(X1)),inference(csr,[status(thm)],[996,211])).
% cnf(1035,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(spm,[status(thm)],[227,1033,theory(equality)])).
% cnf(1130,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)],[812,326])).
% cnf(1131,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)],[1130,547])).
% cnf(1132,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)],[1131,301])).
% cnf(1135,plain,(m1_filter_0(X2,k1_lattice2(X1))|v3_struct_0(X1)|~m2_filter_2(X2,X1)|~v10_lattices(X1)|~l3_lattices(X1)),inference(spm,[status(thm)],[1132,1033,theory(equality)])).
% cnf(1174,plain,(v3_struct_0(k1_lattice2(X1))|r2_hidden(k7_lattices(X1,X2),X3)|r2_hidden(X2,X3)|v3_struct_0(X1)|~v1_filter_0(X3,k1_lattice2(X1))|~m1_filter_0(X3,k1_lattice2(X1))|~v17_lattices(k1_lattice2(X1))|~v10_lattices(k1_lattice2(X1))|~m1_subset_1(X2,u1_struct_0(k1_lattice2(X1)))|~l3_lattices(k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~l3_lattices(X1)),inference(spm,[status(thm)],[172,816,theory(equality)])).
% cnf(1195,plain,(v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|~v1_filter_0(X2,k1_lattice2(X1))|~m1_filter_0(X2,k1_lattice2(X1))|~v17_lattices(k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(k1_lattice2(X1))|~v10_lattices(X1)|~m1_subset_1(k5_filter_2(X1,X3),u1_struct_0(k1_lattice2(X1)))|~m1_subset_1(X3,u1_struct_0(X1))|~l3_lattices(X1)|~r2_hidden(k7_lattices(X1,X3),X2)|~r2_hidden(k5_filter_2(X1,X3),X2)),inference(csr,[status(thm)],[818,326])).
% cnf(1196,plain,(v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|~v1_filter_0(X2,k1_lattice2(X1))|~m1_filter_0(X2,k1_lattice2(X1))|~v17_lattices(k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(k1_lattice2(X1))|~v10_lattices(X1)|~m1_subset_1(X3,u1_struct_0(X1))|~l3_lattices(X1)|~r2_hidden(k7_lattices(X1,X3),X2)|~r2_hidden(k5_filter_2(X1,X3),X2)),inference(csr,[status(thm)],[1195,206])).
% cnf(1197,plain,(v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|~v1_filter_0(X2,k1_lattice2(X1))|~m1_filter_0(X2,k1_lattice2(X1))|~v17_lattices(k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(X1)|~m1_subset_1(X3,u1_struct_0(X1))|~l3_lattices(X1)|~r2_hidden(k7_lattices(X1,X3),X2)|~r2_hidden(k5_filter_2(X1,X3),X2)),inference(csr,[status(thm)],[1196,547])).
% cnf(1198,plain,(v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|~v1_filter_0(X2,k1_lattice2(X1))|~m1_filter_0(X2,k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(X1)|~m1_subset_1(X3,u1_struct_0(X1))|~l3_lattices(X1)|~r2_hidden(k7_lattices(X1,X3),X2)|~r2_hidden(k5_filter_2(X1,X3),X2)),inference(csr,[status(thm)],[1197,501])).
% cnf(1199,plain,(v3_struct_0(X1)|~v1_filter_0(X2,k1_lattice2(X1))|~m1_filter_0(X2,k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(X1)|~m1_subset_1(X3,u1_struct_0(X1))|~l3_lattices(X1)|~r2_hidden(k7_lattices(X1,X3),X2)|~r2_hidden(k5_filter_2(X1,X3),X2)),inference(csr,[status(thm)],[1198,301])).
% cnf(1200,plain,(v3_struct_0(X1)|~v1_filter_0(X2,k1_lattice2(X1))|~m1_filter_0(X2,k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(X1)|~m1_subset_1(X3,u1_struct_0(X1))|~l3_lattices(X1)|~r2_hidden(k7_lattices(X1,X3),X2)|~r2_hidden(X3,X2)),inference(spm,[status(thm)],[1199,203,theory(equality)])).
% cnf(2062,negated_conjecture,(v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~v17_lattices(esk29_0)|~v10_lattices(esk29_0)|~m1_subset_1(esk31_0,u1_struct_0(esk29_0))|~l3_lattices(esk29_0)|~r2_hidden(esk31_0,esk30_0)),inference(spm,[status(thm)],[1200,628,theory(equality)])).
% cnf(2064,negated_conjecture,(v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|~v10_lattices(esk29_0)|~m1_subset_1(esk31_0,u1_struct_0(esk29_0))|~l3_lattices(esk29_0)|~r2_hidden(esk31_0,esk30_0)),inference(rw,[status(thm)],[2062,633,theory(equality)])).
% cnf(2065,negated_conjecture,(v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|$false|~m1_subset_1(esk31_0,u1_struct_0(esk29_0))|~l3_lattices(esk29_0)|~r2_hidden(esk31_0,esk30_0)),inference(rw,[status(thm)],[2064,634,theory(equality)])).
% cnf(2066,negated_conjecture,(v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|$false|$false|~l3_lattices(esk29_0)|~r2_hidden(esk31_0,esk30_0)),inference(rw,[status(thm)],[2065,629,theory(equality)])).
% cnf(2067,negated_conjecture,(v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|$false|$false|$false|~r2_hidden(esk31_0,esk30_0)),inference(rw,[status(thm)],[2066,632,theory(equality)])).
% cnf(2068,negated_conjecture,(v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~r2_hidden(esk31_0,esk30_0)),inference(cn,[status(thm)],[2067,theory(equality)])).
% cnf(2069,negated_conjecture,(~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~r2_hidden(esk31_0,esk30_0)),inference(sr,[status(thm)],[2068,635,theory(equality)])).
% cnf(2070,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~r2_hidden(esk31_0,esk30_0)|~r2_filter_2(esk29_0,esk30_0)|~m2_filter_2(esk30_0,esk29_0)|~v10_lattices(esk29_0)|~l3_lattices(esk29_0)),inference(spm,[status(thm)],[2069,1035,theory(equality)])).
% cnf(2071,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~r2_hidden(esk31_0,esk30_0)|$false|~m2_filter_2(esk30_0,esk29_0)|~v10_lattices(esk29_0)|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[2070,630,theory(equality)])).
% cnf(2072,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~r2_hidden(esk31_0,esk30_0)|$false|$false|~v10_lattices(esk29_0)|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[2071,631,theory(equality)])).
% cnf(2073,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~r2_hidden(esk31_0,esk30_0)|$false|$false|$false|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[2072,634,theory(equality)])).
% cnf(2074,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~r2_hidden(esk31_0,esk30_0)|$false|$false|$false|$false),inference(rw,[status(thm)],[2073,632,theory(equality)])).
% cnf(2075,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~r2_hidden(esk31_0,esk30_0)),inference(cn,[status(thm)],[2074,theory(equality)])).
% cnf(2076,negated_conjecture,(~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~r2_hidden(esk31_0,esk30_0)),inference(sr,[status(thm)],[2075,635,theory(equality)])).
% cnf(2077,negated_conjecture,(v3_struct_0(esk29_0)|~r2_hidden(esk31_0,esk30_0)|~m2_filter_2(esk30_0,esk29_0)|~v10_lattices(esk29_0)|~l3_lattices(esk29_0)),inference(spm,[status(thm)],[2076,1135,theory(equality)])).
% cnf(2078,negated_conjecture,(v3_struct_0(esk29_0)|~r2_hidden(esk31_0,esk30_0)|$false|~v10_lattices(esk29_0)|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[2077,631,theory(equality)])).
% cnf(2079,negated_conjecture,(v3_struct_0(esk29_0)|~r2_hidden(esk31_0,esk30_0)|$false|$false|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[2078,634,theory(equality)])).
% cnf(2080,negated_conjecture,(v3_struct_0(esk29_0)|~r2_hidden(esk31_0,esk30_0)|$false|$false|$false),inference(rw,[status(thm)],[2079,632,theory(equality)])).
% cnf(2081,negated_conjecture,(v3_struct_0(esk29_0)|~r2_hidden(esk31_0,esk30_0)),inference(cn,[status(thm)],[2080,theory(equality)])).
% cnf(2082,negated_conjecture,(~r2_hidden(esk31_0,esk30_0)),inference(sr,[status(thm)],[2081,635,theory(equality)])).
% cnf(2991,plain,(v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|r2_hidden(k7_lattices(X1,X2),X3)|r2_hidden(X2,X3)|~v1_filter_0(X3,k1_lattice2(X1))|~m1_filter_0(X3,k1_lattice2(X1))|~v17_lattices(k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(k1_lattice2(X1))|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(k1_lattice2(X1)))|~m1_subset_1(X2,u1_struct_0(X1))|~l3_lattices(X1)),inference(csr,[status(thm)],[1174,326])).
% cnf(2992,plain,(v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|r2_hidden(k7_lattices(X1,X2),X3)|r2_hidden(X2,X3)|~v1_filter_0(X3,k1_lattice2(X1))|~m1_filter_0(X3,k1_lattice2(X1))|~v17_lattices(k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(k1_lattice2(X1))|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~l3_lattices(X1)),inference(csr,[status(thm)],[2991,813])).
% cnf(2993,plain,(v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|r2_hidden(k7_lattices(X1,X2),X3)|r2_hidden(X2,X3)|~v1_filter_0(X3,k1_lattice2(X1))|~m1_filter_0(X3,k1_lattice2(X1))|~v17_lattices(k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~l3_lattices(X1)),inference(csr,[status(thm)],[2992,547])).
% cnf(2994,plain,(v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|r2_hidden(k7_lattices(X1,X2),X3)|r2_hidden(X2,X3)|~v1_filter_0(X3,k1_lattice2(X1))|~m1_filter_0(X3,k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~l3_lattices(X1)),inference(csr,[status(thm)],[2993,501])).
% cnf(2995,plain,(v3_struct_0(X1)|r2_hidden(k7_lattices(X1,X2),X3)|r2_hidden(X2,X3)|~v1_filter_0(X3,k1_lattice2(X1))|~m1_filter_0(X3,k1_lattice2(X1))|~v17_lattices(X1)|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~l3_lattices(X1)),inference(csr,[status(thm)],[2994,301])).
% cnf(3033,negated_conjecture,(r2_hidden(esk31_0,esk30_0)|v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~v17_lattices(esk29_0)|~v10_lattices(esk29_0)|~m1_subset_1(esk31_0,u1_struct_0(esk29_0))|~l3_lattices(esk29_0)),inference(spm,[status(thm)],[627,2995,theory(equality)])).
% cnf(3040,negated_conjecture,(r2_hidden(esk31_0,esk30_0)|v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|~v10_lattices(esk29_0)|~m1_subset_1(esk31_0,u1_struct_0(esk29_0))|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[3033,633,theory(equality)])).
% cnf(3041,negated_conjecture,(r2_hidden(esk31_0,esk30_0)|v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|$false|~m1_subset_1(esk31_0,u1_struct_0(esk29_0))|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[3040,634,theory(equality)])).
% cnf(3042,negated_conjecture,(r2_hidden(esk31_0,esk30_0)|v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|$false|$false|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[3041,629,theory(equality)])).
% cnf(3043,negated_conjecture,(r2_hidden(esk31_0,esk30_0)|v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|$false|$false|$false),inference(rw,[status(thm)],[3042,632,theory(equality)])).
% cnf(3044,negated_conjecture,(r2_hidden(esk31_0,esk30_0)|v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))),inference(cn,[status(thm)],[3043,theory(equality)])).
% cnf(3045,negated_conjecture,(v3_struct_0(esk29_0)|~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))),inference(sr,[status(thm)],[3044,2082,theory(equality)])).
% cnf(3046,negated_conjecture,(~v1_filter_0(esk30_0,k1_lattice2(esk29_0))|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))),inference(sr,[status(thm)],[3045,635,theory(equality)])).
% cnf(3047,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|~r2_filter_2(esk29_0,esk30_0)|~m2_filter_2(esk30_0,esk29_0)|~v10_lattices(esk29_0)|~l3_lattices(esk29_0)),inference(spm,[status(thm)],[3046,1035,theory(equality)])).
% cnf(3048,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|~m2_filter_2(esk30_0,esk29_0)|~v10_lattices(esk29_0)|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[3047,630,theory(equality)])).
% cnf(3049,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|$false|~v10_lattices(esk29_0)|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[3048,631,theory(equality)])).
% cnf(3050,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|$false|$false|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[3049,634,theory(equality)])).
% cnf(3051,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))|$false|$false|$false|$false),inference(rw,[status(thm)],[3050,632,theory(equality)])).
% cnf(3052,negated_conjecture,(v3_struct_0(esk29_0)|~m1_filter_0(esk30_0,k1_lattice2(esk29_0))),inference(cn,[status(thm)],[3051,theory(equality)])).
% cnf(3053,negated_conjecture,(~m1_filter_0(esk30_0,k1_lattice2(esk29_0))),inference(sr,[status(thm)],[3052,635,theory(equality)])).
% cnf(3054,negated_conjecture,(v3_struct_0(esk29_0)|~m2_filter_2(esk30_0,esk29_0)|~v10_lattices(esk29_0)|~l3_lattices(esk29_0)),inference(spm,[status(thm)],[3053,1135,theory(equality)])).
% cnf(3055,negated_conjecture,(v3_struct_0(esk29_0)|$false|~v10_lattices(esk29_0)|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[3054,631,theory(equality)])).
% cnf(3056,negated_conjecture,(v3_struct_0(esk29_0)|$false|$false|~l3_lattices(esk29_0)),inference(rw,[status(thm)],[3055,634,theory(equality)])).
% cnf(3057,negated_conjecture,(v3_struct_0(esk29_0)|$false|$false|$false),inference(rw,[status(thm)],[3056,632,theory(equality)])).
% cnf(3058,negated_conjecture,(v3_struct_0(esk29_0)),inference(cn,[status(thm)],[3057,theory(equality)])).
% cnf(3059,negated_conjecture,($false),inference(sr,[status(thm)],[3058,635,theory(equality)])).
% cnf(3060,negated_conjecture,($false),3059,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 884
% # ...of these trivial : 0
% # ...subsumed : 263
% # ...remaining for further processing: 621
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 24
% # Backward-rewritten : 10
% # Generated clauses : 1587
% # ...of the previous two non-trivial : 1500
% # Contextual simplify-reflections : 353
% # Paramodulations : 1584
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 586
% # Positive orientable unit clauses: 105
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 23
% # Non-unit-clauses : 458
% # Current number of unprocessed clauses: 765
% # ...number of literals in the above : 5531
% # Clause-clause subsumption calls (NU) : 26315
% # Rec. Clause-clause subsumption calls : 6832
% # Unit Clause-clause subsumption calls : 306
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 20
% # Indexed BW rewrite successes : 4
% # Backwards rewriting index: 551 leaves, 1.50+/-1.157 terms/leaf
% # Paramod-from index: 243 leaves, 1.07+/-0.425 terms/leaf
% # Paramod-into index: 472 leaves, 1.35+/-0.996 terms/leaf
% # -------------------------------------------------
% # User time : 0.212 s
% # System time : 0.009 s
% # Total time : 0.221 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.35 CPU 0.45 WC
% FINAL PrfWatch: 0.35 CPU 0.45 WC
% SZS output end Solution for /tmp/SystemOnTPTP10424/LAT323+1.tptp
%
%------------------------------------------------------------------------------