%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LAT332+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 : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Wed Dec 29 11:15:24 EST 2010
% Result : Theorem 2.09s
% Output : Solution 2.09s
% 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/SystemOnTPTP5757/LAT332+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP5757/LAT332+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP5757/LAT332+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 5889
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.025 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>k17_filter_2(X1)=u1_struct_0(X1)),file('/tmp/SRASS.s.p', d8_filter_2)).
% fof(4, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>k1_filter_0(X1)=u1_struct_0(X1)),file('/tmp/SRASS.s.p', d2_filter_0)).
% fof(5, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>k1_filter_2(X1)=k1_filter_0(X1)),file('/tmp/SRASS.s.p', redefinition_k1_filter_2)).
% fof(6, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>m2_filter_2(k17_filter_2(X1),X1)),file('/tmp/SRASS.s.p', dt_k17_filter_2)).
% fof(17, axiom,![X1]:![X2]:(((((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))&~(v1_xboole_0(X2)))&m2_lattice4(X2,X1))=>m2_nat_lat(k23_filter_2(X1,X2),X1)),file('/tmp/SRASS.s.p', dt_k23_filter_2)).
% fof(29, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:((~(v1_xboole_0(X2))&m2_lattice4(X2,X1))=>![X3]:(m2_nat_lat(X3,X1)=>(X3=k23_filter_2(X1,X2)<=>?[X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2))&?[X5]:(((((v1_funct_1(X5)&v1_funct_2(X5,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X5,k2_zfmisc_1(X2,X2),X2))&X4=k1_realset1(u2_lattices(X1),X2))&X5=k1_realset1(u1_lattices(X1),X2))&X3=g3_lattices(X2,X4,X5))))))),file('/tmp/SRASS.s.p', d16_filter_2)).
% fof(33, 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(35, axiom,![X1]:(l1_lattices(X1)=>((v1_funct_1(u1_lattices(X1))&v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),file('/tmp/SRASS.s.p', dt_u1_lattices)).
% fof(36, axiom,![X1]:(l2_lattices(X1)=>((v1_funct_1(u2_lattices(X1))&v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),file('/tmp/SRASS.s.p', dt_u2_lattices)).
% fof(51, axiom,![X1]:![X2]:(m1_subset_1(X1,k1_zfmisc_1(X2))<=>r1_tarski(X1,X2)),file('/tmp/SRASS.s.p', t3_subset)).
% fof(55, axiom,![X1]:(v1_relat_1(X1)=>![X2]:k1_realset1(X1,X2)=k7_relat_1(X1,k2_zfmisc_1(X2,X2))),file('/tmp/SRASS.s.p', d3_realset1)).
% fof(60, axiom,![X1]:(l3_lattices(X1)=>(l1_lattices(X1)&l2_lattices(X1))),file('/tmp/SRASS.s.p', dt_l3_lattices)).
% fof(63, axiom,![X1]:![X2]:![X3]:(m2_relset_1(X3,X1,X2)=>m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))),file('/tmp/SRASS.s.p', dt_m2_relset_1)).
% fof(64, axiom,![X1]:![X2]:![X3]:(m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))=>v1_relat_1(X3)),file('/tmp/SRASS.s.p', cc1_relset_1)).
% fof(68, axiom,![X1]:![X2]:![X3]:(m2_relset_1(X3,X1,X2)<=>m1_relset_1(X3,X1,X2)),file('/tmp/SRASS.s.p', redefinition_m2_relset_1)).
% fof(72, axiom,![X1]:![X2]:![X3]:(m1_relset_1(X3,X1,X2)=>m1_subset_1(k4_relset_1(X1,X2,X3),k1_zfmisc_1(X1))),file('/tmp/SRASS.s.p', dt_k4_relset_1)).
% fof(87, axiom,![X1]:![X2]:(v1_relat_1(X2)=>(r1_tarski(k1_relat_1(X2),X1)=>k7_relat_1(X2,X1)=X2)),file('/tmp/SRASS.s.p', t97_relat_1)).
% fof(88, axiom,![X1]:![X2]:![X3]:(m1_relset_1(X3,X1,X2)=>k4_relset_1(X1,X2,X3)=k1_relat_1(X3)),file('/tmp/SRASS.s.p', redefinition_k4_relset_1)).
% fof(99, conjecture,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>(k23_filter_2(X1,k17_filter_2(X1))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))&k23_filter_2(X1,k1_filter_2(X1))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)))),file('/tmp/SRASS.s.p', t72_filter_2)).
% fof(100, negated_conjecture,~(![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>(k23_filter_2(X1,k17_filter_2(X1))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))&k23_filter_2(X1,k1_filter_2(X1))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))))),inference(assume_negation,[status(cth)],[99])).
% fof(101, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>k17_filter_2(X1)=u1_struct_0(X1)),inference(fof_simplification,[status(thm)],[1,theory(equality)])).
% fof(102, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>k1_filter_0(X1)=u1_struct_0(X1)),inference(fof_simplification,[status(thm)],[4,theory(equality)])).
% fof(103, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>k1_filter_2(X1)=k1_filter_0(X1)),inference(fof_simplification,[status(thm)],[5,theory(equality)])).
% fof(104, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>m2_filter_2(k17_filter_2(X1),X1)),inference(fof_simplification,[status(thm)],[6,theory(equality)])).
% fof(114, plain,![X1]:![X2]:(((((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))&~(v1_xboole_0(X2)))&m2_lattice4(X2,X1))=>m2_nat_lat(k23_filter_2(X1,X2),X1)),inference(fof_simplification,[status(thm)],[17,theory(equality)])).
% fof(120, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:((~(v1_xboole_0(X2))&m2_lattice4(X2,X1))=>![X3]:(m2_nat_lat(X3,X1)=>(X3=k23_filter_2(X1,X2)<=>?[X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2))&?[X5]:(((((v1_funct_1(X5)&v1_funct_2(X5,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X5,k2_zfmisc_1(X2,X2),X2))&X4=k1_realset1(u2_lattices(X1),X2))&X5=k1_realset1(u1_lattices(X1),X2))&X3=g3_lattices(X2,X4,X5))))))),inference(fof_simplification,[status(thm)],[29,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)],[33,theory(equality)])).
% fof(143, negated_conjecture,~(![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>(k23_filter_2(X1,k17_filter_2(X1))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))&k23_filter_2(X1,k1_filter_2(X1))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))))),inference(fof_simplification,[status(thm)],[100,theory(equality)])).
% fof(144, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|k17_filter_2(X1)=u1_struct_0(X1)),inference(fof_nnf,[status(thm)],[101])).
% fof(145, plain,![X2]:(((v3_struct_0(X2)|~(v10_lattices(X2)))|~(l3_lattices(X2)))|k17_filter_2(X2)=u1_struct_0(X2)),inference(variable_rename,[status(thm)],[144])).
% cnf(146,plain,(k17_filter_2(X1)=u1_struct_0(X1)|v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[145])).
% fof(153, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|k1_filter_0(X1)=u1_struct_0(X1)),inference(fof_nnf,[status(thm)],[102])).
% fof(154, plain,![X2]:(((v3_struct_0(X2)|~(v10_lattices(X2)))|~(l3_lattices(X2)))|k1_filter_0(X2)=u1_struct_0(X2)),inference(variable_rename,[status(thm)],[153])).
% cnf(155,plain,(k1_filter_0(X1)=u1_struct_0(X1)|v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[154])).
% fof(156, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|k1_filter_2(X1)=k1_filter_0(X1)),inference(fof_nnf,[status(thm)],[103])).
% fof(157, plain,![X2]:(((v3_struct_0(X2)|~(v10_lattices(X2)))|~(l3_lattices(X2)))|k1_filter_2(X2)=k1_filter_0(X2)),inference(variable_rename,[status(thm)],[156])).
% cnf(158,plain,(k1_filter_2(X1)=k1_filter_0(X1)|v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[157])).
% fof(159, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|m2_filter_2(k17_filter_2(X1),X1)),inference(fof_nnf,[status(thm)],[104])).
% fof(160, plain,![X2]:(((v3_struct_0(X2)|~(v10_lattices(X2)))|~(l3_lattices(X2)))|m2_filter_2(k17_filter_2(X2),X2)),inference(variable_rename,[status(thm)],[159])).
% cnf(161,plain,(m2_filter_2(k17_filter_2(X1),X1)|v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[160])).
% fof(206, plain,![X1]:![X2]:(((((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|v1_xboole_0(X2))|~(m2_lattice4(X2,X1)))|m2_nat_lat(k23_filter_2(X1,X2),X1)),inference(fof_nnf,[status(thm)],[114])).
% fof(207, plain,![X3]:![X4]:(((((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))|v1_xboole_0(X4))|~(m2_lattice4(X4,X3)))|m2_nat_lat(k23_filter_2(X3,X4),X3)),inference(variable_rename,[status(thm)],[206])).
% cnf(208,plain,(m2_nat_lat(k23_filter_2(X1,X2),X1)|v1_xboole_0(X2)|v3_struct_0(X1)|~m2_lattice4(X2,X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[207])).
% fof(247, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|![X2]:((v1_xboole_0(X2)|~(m2_lattice4(X2,X1)))|![X3]:(~(m2_nat_lat(X3,X1))|((~(X3=k23_filter_2(X1,X2))|?[X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2))&?[X5]:(((((v1_funct_1(X5)&v1_funct_2(X5,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X5,k2_zfmisc_1(X2,X2),X2))&X4=k1_realset1(u2_lattices(X1),X2))&X5=k1_realset1(u1_lattices(X1),X2))&X3=g3_lattices(X2,X4,X5))))&(![X4]:(((~(v1_funct_1(X4))|~(v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)))|~(m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)))|![X5]:(((((~(v1_funct_1(X5))|~(v1_funct_2(X5,k2_zfmisc_1(X2,X2),X2)))|~(m2_relset_1(X5,k2_zfmisc_1(X2,X2),X2)))|~(X4=k1_realset1(u2_lattices(X1),X2)))|~(X5=k1_realset1(u1_lattices(X1),X2)))|~(X3=g3_lattices(X2,X4,X5))))|X3=k23_filter_2(X1,X2)))))),inference(fof_nnf,[status(thm)],[120])).
% fof(248, plain,![X6]:(((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6)))|![X7]:((v1_xboole_0(X7)|~(m2_lattice4(X7,X6)))|![X8]:(~(m2_nat_lat(X8,X6))|((~(X8=k23_filter_2(X6,X7))|?[X9]:(((v1_funct_1(X9)&v1_funct_2(X9,k2_zfmisc_1(X7,X7),X7))&m2_relset_1(X9,k2_zfmisc_1(X7,X7),X7))&?[X10]:(((((v1_funct_1(X10)&v1_funct_2(X10,k2_zfmisc_1(X7,X7),X7))&m2_relset_1(X10,k2_zfmisc_1(X7,X7),X7))&X9=k1_realset1(u2_lattices(X6),X7))&X10=k1_realset1(u1_lattices(X6),X7))&X8=g3_lattices(X7,X9,X10))))&(![X11]:(((~(v1_funct_1(X11))|~(v1_funct_2(X11,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X11,k2_zfmisc_1(X7,X7),X7)))|![X12]:(((((~(v1_funct_1(X12))|~(v1_funct_2(X12,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X12,k2_zfmisc_1(X7,X7),X7)))|~(X11=k1_realset1(u2_lattices(X6),X7)))|~(X12=k1_realset1(u1_lattices(X6),X7)))|~(X8=g3_lattices(X7,X11,X12))))|X8=k23_filter_2(X6,X7)))))),inference(variable_rename,[status(thm)],[247])).
% fof(249, plain,![X6]:(((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6)))|![X7]:((v1_xboole_0(X7)|~(m2_lattice4(X7,X6)))|![X8]:(~(m2_nat_lat(X8,X6))|((~(X8=k23_filter_2(X6,X7))|(((v1_funct_1(esk15_3(X6,X7,X8))&v1_funct_2(esk15_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7))&m2_relset_1(esk15_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7))&(((((v1_funct_1(esk16_3(X6,X7,X8))&v1_funct_2(esk16_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7))&m2_relset_1(esk16_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7))&esk15_3(X6,X7,X8)=k1_realset1(u2_lattices(X6),X7))&esk16_3(X6,X7,X8)=k1_realset1(u1_lattices(X6),X7))&X8=g3_lattices(X7,esk15_3(X6,X7,X8),esk16_3(X6,X7,X8)))))&(![X11]:(((~(v1_funct_1(X11))|~(v1_funct_2(X11,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X11,k2_zfmisc_1(X7,X7),X7)))|![X12]:(((((~(v1_funct_1(X12))|~(v1_funct_2(X12,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X12,k2_zfmisc_1(X7,X7),X7)))|~(X11=k1_realset1(u2_lattices(X6),X7)))|~(X12=k1_realset1(u1_lattices(X6),X7)))|~(X8=g3_lattices(X7,X11,X12))))|X8=k23_filter_2(X6,X7)))))),inference(skolemize,[status(esa)],[248])).
% fof(250, plain,![X6]:![X7]:![X8]:![X11]:![X12]:(((((((((((~(v1_funct_1(X12))|~(v1_funct_2(X12,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X12,k2_zfmisc_1(X7,X7),X7)))|~(X11=k1_realset1(u2_lattices(X6),X7)))|~(X12=k1_realset1(u1_lattices(X6),X7)))|~(X8=g3_lattices(X7,X11,X12)))|((~(v1_funct_1(X11))|~(v1_funct_2(X11,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X11,k2_zfmisc_1(X7,X7),X7))))|X8=k23_filter_2(X6,X7))&(~(X8=k23_filter_2(X6,X7))|(((v1_funct_1(esk15_3(X6,X7,X8))&v1_funct_2(esk15_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7))&m2_relset_1(esk15_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7))&(((((v1_funct_1(esk16_3(X6,X7,X8))&v1_funct_2(esk16_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7))&m2_relset_1(esk16_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7))&esk15_3(X6,X7,X8)=k1_realset1(u2_lattices(X6),X7))&esk16_3(X6,X7,X8)=k1_realset1(u1_lattices(X6),X7))&X8=g3_lattices(X7,esk15_3(X6,X7,X8),esk16_3(X6,X7,X8))))))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6)))),inference(shift_quantors,[status(thm)],[249])).
% fof(251, plain,![X6]:![X7]:![X8]:![X11]:![X12]:(((((((((((~(v1_funct_1(X12))|~(v1_funct_2(X12,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X12,k2_zfmisc_1(X7,X7),X7)))|~(X11=k1_realset1(u2_lattices(X6),X7)))|~(X12=k1_realset1(u1_lattices(X6),X7)))|~(X8=g3_lattices(X7,X11,X12)))|((~(v1_funct_1(X11))|~(v1_funct_2(X11,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X11,k2_zfmisc_1(X7,X7),X7))))|X8=k23_filter_2(X6,X7))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6))))&(((((((v1_funct_1(esk15_3(X6,X7,X8))|~(X8=k23_filter_2(X6,X7)))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6))))&((((v1_funct_2(esk15_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7)|~(X8=k23_filter_2(X6,X7)))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6)))))&((((m2_relset_1(esk15_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7)|~(X8=k23_filter_2(X6,X7)))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6)))))&(((((((((v1_funct_1(esk16_3(X6,X7,X8))|~(X8=k23_filter_2(X6,X7)))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6))))&((((v1_funct_2(esk16_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7)|~(X8=k23_filter_2(X6,X7)))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6)))))&((((m2_relset_1(esk16_3(X6,X7,X8),k2_zfmisc_1(X7,X7),X7)|~(X8=k23_filter_2(X6,X7)))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6)))))&((((esk15_3(X6,X7,X8)=k1_realset1(u2_lattices(X6),X7)|~(X8=k23_filter_2(X6,X7)))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6)))))&((((esk16_3(X6,X7,X8)=k1_realset1(u1_lattices(X6),X7)|~(X8=k23_filter_2(X6,X7)))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6)))))&((((X8=g3_lattices(X7,esk15_3(X6,X7,X8),esk16_3(X6,X7,X8))|~(X8=k23_filter_2(X6,X7)))|~(m2_nat_lat(X8,X6)))|(v1_xboole_0(X7)|~(m2_lattice4(X7,X6))))|((v3_struct_0(X6)|~(v10_lattices(X6)))|~(l3_lattices(X6))))))),inference(distribute,[status(thm)],[250])).
% cnf(252,plain,(v3_struct_0(X1)|v1_xboole_0(X2)|X3=g3_lattices(X2,esk15_3(X1,X2,X3),esk16_3(X1,X2,X3))|~l3_lattices(X1)|~v10_lattices(X1)|~m2_lattice4(X2,X1)|~m2_nat_lat(X3,X1)|X3!=k23_filter_2(X1,X2)),inference(split_conjunct,[status(thm)],[251])).
% cnf(253,plain,(v3_struct_0(X1)|v1_xboole_0(X2)|esk16_3(X1,X2,X3)=k1_realset1(u1_lattices(X1),X2)|~l3_lattices(X1)|~v10_lattices(X1)|~m2_lattice4(X2,X1)|~m2_nat_lat(X3,X1)|X3!=k23_filter_2(X1,X2)),inference(split_conjunct,[status(thm)],[251])).
% cnf(254,plain,(v3_struct_0(X1)|v1_xboole_0(X2)|esk15_3(X1,X2,X3)=k1_realset1(u2_lattices(X1),X2)|~l3_lattices(X1)|~v10_lattices(X1)|~m2_lattice4(X2,X1)|~m2_nat_lat(X3,X1)|X3!=k23_filter_2(X1,X2)),inference(split_conjunct,[status(thm)],[251])).
% fof(277, 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(278, 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)],[277])).
% fof(279, 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)],[278])).
% fof(280, 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)],[279])).
% cnf(281,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)],[280])).
% cnf(282,plain,(v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)|~m2_filter_2(X2,X1)|~v1_xboole_0(X2)),inference(split_conjunct,[status(thm)],[280])).
% fof(287, plain,![X1]:(~(l1_lattices(X1))|((v1_funct_1(u1_lattices(X1))&v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[35])).
% fof(288, plain,![X2]:(~(l1_lattices(X2))|((v1_funct_1(u1_lattices(X2))&v1_funct_2(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))&m2_relset_1(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))),inference(variable_rename,[status(thm)],[287])).
% fof(289, plain,![X2]:(((v1_funct_1(u1_lattices(X2))|~(l1_lattices(X2)))&(v1_funct_2(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|~(l1_lattices(X2))))&(m2_relset_1(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|~(l1_lattices(X2)))),inference(distribute,[status(thm)],[288])).
% cnf(290,plain,(m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))|~l1_lattices(X1)),inference(split_conjunct,[status(thm)],[289])).
% fof(293, plain,![X1]:(~(l2_lattices(X1))|((v1_funct_1(u2_lattices(X1))&v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[36])).
% fof(294, plain,![X2]:(~(l2_lattices(X2))|((v1_funct_1(u2_lattices(X2))&v1_funct_2(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))&m2_relset_1(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))),inference(variable_rename,[status(thm)],[293])).
% fof(295, plain,![X2]:(((v1_funct_1(u2_lattices(X2))|~(l2_lattices(X2)))&(v1_funct_2(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|~(l2_lattices(X2))))&(m2_relset_1(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|~(l2_lattices(X2)))),inference(distribute,[status(thm)],[294])).
% cnf(296,plain,(m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))|~l2_lattices(X1)),inference(split_conjunct,[status(thm)],[295])).
% fof(359, plain,![X1]:![X2]:((~(m1_subset_1(X1,k1_zfmisc_1(X2)))|r1_tarski(X1,X2))&(~(r1_tarski(X1,X2))|m1_subset_1(X1,k1_zfmisc_1(X2)))),inference(fof_nnf,[status(thm)],[51])).
% fof(360, plain,![X3]:![X4]:((~(m1_subset_1(X3,k1_zfmisc_1(X4)))|r1_tarski(X3,X4))&(~(r1_tarski(X3,X4))|m1_subset_1(X3,k1_zfmisc_1(X4)))),inference(variable_rename,[status(thm)],[359])).
% cnf(362,plain,(r1_tarski(X1,X2)|~m1_subset_1(X1,k1_zfmisc_1(X2))),inference(split_conjunct,[status(thm)],[360])).
% fof(372, plain,![X1]:(~(v1_relat_1(X1))|![X2]:k1_realset1(X1,X2)=k7_relat_1(X1,k2_zfmisc_1(X2,X2))),inference(fof_nnf,[status(thm)],[55])).
% fof(373, plain,![X3]:(~(v1_relat_1(X3))|![X4]:k1_realset1(X3,X4)=k7_relat_1(X3,k2_zfmisc_1(X4,X4))),inference(variable_rename,[status(thm)],[372])).
% fof(374, plain,![X3]:![X4]:(k1_realset1(X3,X4)=k7_relat_1(X3,k2_zfmisc_1(X4,X4))|~(v1_relat_1(X3))),inference(shift_quantors,[status(thm)],[373])).
% cnf(375,plain,(k1_realset1(X1,X2)=k7_relat_1(X1,k2_zfmisc_1(X2,X2))|~v1_relat_1(X1)),inference(split_conjunct,[status(thm)],[374])).
% fof(405, plain,![X1]:(~(l3_lattices(X1))|(l1_lattices(X1)&l2_lattices(X1))),inference(fof_nnf,[status(thm)],[60])).
% fof(406, plain,![X2]:(~(l3_lattices(X2))|(l1_lattices(X2)&l2_lattices(X2))),inference(variable_rename,[status(thm)],[405])).
% fof(407, plain,![X2]:((l1_lattices(X2)|~(l3_lattices(X2)))&(l2_lattices(X2)|~(l3_lattices(X2)))),inference(distribute,[status(thm)],[406])).
% cnf(408,plain,(l2_lattices(X1)|~l3_lattices(X1)),inference(split_conjunct,[status(thm)],[407])).
% cnf(409,plain,(l1_lattices(X1)|~l3_lattices(X1)),inference(split_conjunct,[status(thm)],[407])).
% fof(415, plain,![X1]:![X2]:![X3]:(~(m2_relset_1(X3,X1,X2))|m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))),inference(fof_nnf,[status(thm)],[63])).
% fof(416, plain,![X4]:![X5]:![X6]:(~(m2_relset_1(X6,X4,X5))|m1_subset_1(X6,k1_zfmisc_1(k2_zfmisc_1(X4,X5)))),inference(variable_rename,[status(thm)],[415])).
% cnf(417,plain,(m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))|~m2_relset_1(X1,X2,X3)),inference(split_conjunct,[status(thm)],[416])).
% fof(418, plain,![X1]:![X2]:![X3]:(~(m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2))))|v1_relat_1(X3)),inference(fof_nnf,[status(thm)],[64])).
% fof(419, plain,![X4]:![X5]:![X6]:(~(m1_subset_1(X6,k1_zfmisc_1(k2_zfmisc_1(X4,X5))))|v1_relat_1(X6)),inference(variable_rename,[status(thm)],[418])).
% cnf(420,plain,(v1_relat_1(X1)|~m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))),inference(split_conjunct,[status(thm)],[419])).
% fof(431, plain,![X1]:![X2]:![X3]:((~(m2_relset_1(X3,X1,X2))|m1_relset_1(X3,X1,X2))&(~(m1_relset_1(X3,X1,X2))|m2_relset_1(X3,X1,X2))),inference(fof_nnf,[status(thm)],[68])).
% fof(432, plain,![X4]:![X5]:![X6]:((~(m2_relset_1(X6,X4,X5))|m1_relset_1(X6,X4,X5))&(~(m1_relset_1(X6,X4,X5))|m2_relset_1(X6,X4,X5))),inference(variable_rename,[status(thm)],[431])).
% cnf(434,plain,(m1_relset_1(X1,X2,X3)|~m2_relset_1(X1,X2,X3)),inference(split_conjunct,[status(thm)],[432])).
% fof(444, plain,![X1]:![X2]:![X3]:(~(m1_relset_1(X3,X1,X2))|m1_subset_1(k4_relset_1(X1,X2,X3),k1_zfmisc_1(X1))),inference(fof_nnf,[status(thm)],[72])).
% fof(445, plain,![X4]:![X5]:![X6]:(~(m1_relset_1(X6,X4,X5))|m1_subset_1(k4_relset_1(X4,X5,X6),k1_zfmisc_1(X4))),inference(variable_rename,[status(thm)],[444])).
% cnf(446,plain,(m1_subset_1(k4_relset_1(X1,X2,X3),k1_zfmisc_1(X1))|~m1_relset_1(X3,X1,X2)),inference(split_conjunct,[status(thm)],[445])).
% fof(543, plain,![X1]:![X2]:(~(v1_relat_1(X2))|(~(r1_tarski(k1_relat_1(X2),X1))|k7_relat_1(X2,X1)=X2)),inference(fof_nnf,[status(thm)],[87])).
% fof(544, plain,![X3]:![X4]:(~(v1_relat_1(X4))|(~(r1_tarski(k1_relat_1(X4),X3))|k7_relat_1(X4,X3)=X4)),inference(variable_rename,[status(thm)],[543])).
% cnf(545,plain,(k7_relat_1(X1,X2)=X1|~r1_tarski(k1_relat_1(X1),X2)|~v1_relat_1(X1)),inference(split_conjunct,[status(thm)],[544])).
% fof(546, plain,![X1]:![X2]:![X3]:(~(m1_relset_1(X3,X1,X2))|k4_relset_1(X1,X2,X3)=k1_relat_1(X3)),inference(fof_nnf,[status(thm)],[88])).
% fof(547, plain,![X4]:![X5]:![X6]:(~(m1_relset_1(X6,X4,X5))|k4_relset_1(X4,X5,X6)=k1_relat_1(X6)),inference(variable_rename,[status(thm)],[546])).
% cnf(548,plain,(k4_relset_1(X1,X2,X3)=k1_relat_1(X3)|~m1_relset_1(X3,X1,X2)),inference(split_conjunct,[status(thm)],[547])).
% fof(561, negated_conjecture,?[X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))&(~(k23_filter_2(X1,k17_filter_2(X1))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)))|~(k23_filter_2(X1,k1_filter_2(X1))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))))),inference(fof_nnf,[status(thm)],[143])).
% fof(562, negated_conjecture,?[X2]:(((~(v3_struct_0(X2))&v10_lattices(X2))&l3_lattices(X2))&(~(k23_filter_2(X2,k17_filter_2(X2))=g3_lattices(u1_struct_0(X2),u2_lattices(X2),u1_lattices(X2)))|~(k23_filter_2(X2,k1_filter_2(X2))=g3_lattices(u1_struct_0(X2),u2_lattices(X2),u1_lattices(X2))))),inference(variable_rename,[status(thm)],[561])).
% fof(563, negated_conjecture,(((~(v3_struct_0(esk29_0))&v10_lattices(esk29_0))&l3_lattices(esk29_0))&(~(k23_filter_2(esk29_0,k17_filter_2(esk29_0))=g3_lattices(u1_struct_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0)))|~(k23_filter_2(esk29_0,k1_filter_2(esk29_0))=g3_lattices(u1_struct_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))))),inference(skolemize,[status(esa)],[562])).
% cnf(564,negated_conjecture,(k23_filter_2(esk29_0,k1_filter_2(esk29_0))!=g3_lattices(u1_struct_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=g3_lattices(u1_struct_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))),inference(split_conjunct,[status(thm)],[563])).
% cnf(565,negated_conjecture,(l3_lattices(esk29_0)),inference(split_conjunct,[status(thm)],[563])).
% cnf(566,negated_conjecture,(v10_lattices(esk29_0)),inference(split_conjunct,[status(thm)],[563])).
% cnf(567,negated_conjecture,(~v3_struct_0(esk29_0)),inference(split_conjunct,[status(thm)],[563])).
% cnf(589,negated_conjecture,(l1_lattices(esk29_0)),inference(spm,[status(thm)],[409,565,theory(equality)])).
% cnf(594,negated_conjecture,(l2_lattices(esk29_0)),inference(spm,[status(thm)],[408,565,theory(equality)])).
% cnf(650,negated_conjecture,(u1_struct_0(esk29_0)=k1_filter_0(esk29_0)|v3_struct_0(esk29_0)|~l3_lattices(esk29_0)),inference(spm,[status(thm)],[155,566,theory(equality)])).
% cnf(652,negated_conjecture,(u1_struct_0(esk29_0)=k1_filter_0(esk29_0)|v3_struct_0(esk29_0)|$false),inference(rw,[status(thm)],[650,565,theory(equality)])).
% cnf(653,negated_conjecture,(u1_struct_0(esk29_0)=k1_filter_0(esk29_0)|v3_struct_0(esk29_0)),inference(cn,[status(thm)],[652,theory(equality)])).
% cnf(654,negated_conjecture,(u1_struct_0(esk29_0)=k1_filter_0(esk29_0)),inference(sr,[status(thm)],[653,567,theory(equality)])).
% cnf(665,plain,(m2_filter_2(u1_struct_0(X1),X1)|v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(spm,[status(thm)],[161,146,theory(equality)])).
% cnf(684,plain,(v3_struct_0(X1)|~v1_xboole_0(k17_filter_2(X1))|~l3_lattices(X1)|~v10_lattices(X1)),inference(spm,[status(thm)],[282,161,theory(equality)])).
% cnf(725,plain,(v1_relat_1(X1)|~m2_relset_1(X1,X2,X3)),inference(spm,[status(thm)],[420,417,theory(equality)])).
% cnf(741,plain,(r1_tarski(k4_relset_1(X1,X2,X3),X1)|~m1_relset_1(X3,X1,X2)),inference(spm,[status(thm)],[362,446,theory(equality)])).
% cnf(780,plain,(g3_lattices(X1,esk15_3(X2,X1,X3),k1_realset1(u1_lattices(X2),X1))=X3|v1_xboole_0(X1)|v3_struct_0(X2)|k23_filter_2(X2,X1)!=X3|~m2_lattice4(X1,X2)|~m2_nat_lat(X3,X2)|~l3_lattices(X2)|~v10_lattices(X2)),inference(spm,[status(thm)],[252,253,theory(equality)])).
% cnf(816,negated_conjecture,(m2_relset_1(u2_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)),k1_filter_0(esk29_0))|~l2_lattices(esk29_0)),inference(spm,[status(thm)],[296,654,theory(equality)])).
% cnf(817,negated_conjecture,(m2_relset_1(u1_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)),k1_filter_0(esk29_0))|~l1_lattices(esk29_0)),inference(spm,[status(thm)],[290,654,theory(equality)])).
% cnf(826,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))!=k23_filter_2(esk29_0,k17_filter_2(esk29_0))|g3_lattices(u1_struct_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))!=k23_filter_2(esk29_0,k1_filter_2(esk29_0))),inference(rw,[status(thm)],[564,654,theory(equality)])).
% cnf(827,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))!=k23_filter_2(esk29_0,k17_filter_2(esk29_0))|g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))!=k23_filter_2(esk29_0,k1_filter_2(esk29_0))),inference(rw,[status(thm)],[826,654,theory(equality)])).
% cnf(848,negated_conjecture,(m2_relset_1(u2_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)),k1_filter_0(esk29_0))|$false),inference(rw,[status(thm)],[816,594,theory(equality)])).
% cnf(849,negated_conjecture,(m2_relset_1(u2_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)),k1_filter_0(esk29_0))),inference(cn,[status(thm)],[848,theory(equality)])).
% cnf(850,negated_conjecture,(m2_relset_1(u1_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)),k1_filter_0(esk29_0))|$false),inference(rw,[status(thm)],[817,589,theory(equality)])).
% cnf(851,negated_conjecture,(m2_relset_1(u1_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)),k1_filter_0(esk29_0))),inference(cn,[status(thm)],[850,theory(equality)])).
% cnf(1010,plain,(v3_struct_0(X1)|~v1_xboole_0(u1_struct_0(X1))|~l3_lattices(X1)|~v10_lattices(X1)),inference(spm,[status(thm)],[684,146,theory(equality)])).
% cnf(1012,negated_conjecture,(v3_struct_0(esk29_0)|~v1_xboole_0(k1_filter_0(esk29_0))|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(spm,[status(thm)],[1010,654,theory(equality)])).
% cnf(1014,negated_conjecture,(v3_struct_0(esk29_0)|~v1_xboole_0(k1_filter_0(esk29_0))|$false|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[1012,565,theory(equality)])).
% cnf(1015,negated_conjecture,(v3_struct_0(esk29_0)|~v1_xboole_0(k1_filter_0(esk29_0))|$false|$false),inference(rw,[status(thm)],[1014,566,theory(equality)])).
% cnf(1016,negated_conjecture,(v3_struct_0(esk29_0)|~v1_xboole_0(k1_filter_0(esk29_0))),inference(cn,[status(thm)],[1015,theory(equality)])).
% cnf(1017,negated_conjecture,(~v1_xboole_0(k1_filter_0(esk29_0))),inference(sr,[status(thm)],[1016,567,theory(equality)])).
% cnf(1030,negated_conjecture,(m2_filter_2(k1_filter_0(esk29_0),esk29_0)|v3_struct_0(esk29_0)|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(spm,[status(thm)],[665,654,theory(equality)])).
% cnf(1032,negated_conjecture,(m2_filter_2(k1_filter_0(esk29_0),esk29_0)|v3_struct_0(esk29_0)|$false|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[1030,565,theory(equality)])).
% cnf(1033,negated_conjecture,(m2_filter_2(k1_filter_0(esk29_0),esk29_0)|v3_struct_0(esk29_0)|$false|$false),inference(rw,[status(thm)],[1032,566,theory(equality)])).
% cnf(1034,negated_conjecture,(m2_filter_2(k1_filter_0(esk29_0),esk29_0)|v3_struct_0(esk29_0)),inference(cn,[status(thm)],[1033,theory(equality)])).
% cnf(1035,negated_conjecture,(m2_filter_2(k1_filter_0(esk29_0),esk29_0)),inference(sr,[status(thm)],[1034,567,theory(equality)])).
% cnf(1041,negated_conjecture,(m2_lattice4(k1_filter_0(esk29_0),esk29_0)|v3_struct_0(esk29_0)|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(spm,[status(thm)],[281,1035,theory(equality)])).
% cnf(1046,negated_conjecture,(m2_lattice4(k1_filter_0(esk29_0),esk29_0)|v3_struct_0(esk29_0)|$false|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[1041,565,theory(equality)])).
% cnf(1047,negated_conjecture,(m2_lattice4(k1_filter_0(esk29_0),esk29_0)|v3_struct_0(esk29_0)|$false|$false),inference(rw,[status(thm)],[1046,566,theory(equality)])).
% cnf(1048,negated_conjecture,(m2_lattice4(k1_filter_0(esk29_0),esk29_0)|v3_struct_0(esk29_0)),inference(cn,[status(thm)],[1047,theory(equality)])).
% cnf(1049,negated_conjecture,(m2_lattice4(k1_filter_0(esk29_0),esk29_0)),inference(sr,[status(thm)],[1048,567,theory(equality)])).
% cnf(1221,negated_conjecture,(m1_relset_1(u2_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)),k1_filter_0(esk29_0))),inference(spm,[status(thm)],[434,849,theory(equality)])).
% cnf(1222,negated_conjecture,(v1_relat_1(u2_lattices(esk29_0))),inference(spm,[status(thm)],[725,849,theory(equality)])).
% cnf(1238,negated_conjecture,(m1_relset_1(u1_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)),k1_filter_0(esk29_0))),inference(spm,[status(thm)],[434,851,theory(equality)])).
% cnf(1239,negated_conjecture,(v1_relat_1(u1_lattices(esk29_0))),inference(spm,[status(thm)],[725,851,theory(equality)])).
% cnf(1527,plain,(r1_tarski(k1_relat_1(X3),X1)|~m1_relset_1(X3,X1,X2)),inference(spm,[status(thm)],[741,548,theory(equality)])).
% cnf(1534,negated_conjecture,(r1_tarski(k1_relat_1(u1_lattices(esk29_0)),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)))),inference(spm,[status(thm)],[1527,1238,theory(equality)])).
% cnf(1536,negated_conjecture,(r1_tarski(k1_relat_1(u2_lattices(esk29_0)),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)))),inference(spm,[status(thm)],[1527,1221,theory(equality)])).
% cnf(1552,negated_conjecture,(k7_relat_1(u1_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)))=u1_lattices(esk29_0)|~v1_relat_1(u1_lattices(esk29_0))),inference(spm,[status(thm)],[545,1534,theory(equality)])).
% cnf(1553,negated_conjecture,(k7_relat_1(u1_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)))=u1_lattices(esk29_0)|$false),inference(rw,[status(thm)],[1552,1239,theory(equality)])).
% cnf(1554,negated_conjecture,(k7_relat_1(u1_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)))=u1_lattices(esk29_0)),inference(cn,[status(thm)],[1553,theory(equality)])).
% cnf(1557,negated_conjecture,(u1_lattices(esk29_0)=k1_realset1(u1_lattices(esk29_0),k1_filter_0(esk29_0))|~v1_relat_1(u1_lattices(esk29_0))),inference(spm,[status(thm)],[375,1554,theory(equality)])).
% cnf(1563,negated_conjecture,(u1_lattices(esk29_0)=k1_realset1(u1_lattices(esk29_0),k1_filter_0(esk29_0))|$false),inference(rw,[status(thm)],[1557,1239,theory(equality)])).
% cnf(1564,negated_conjecture,(u1_lattices(esk29_0)=k1_realset1(u1_lattices(esk29_0),k1_filter_0(esk29_0))),inference(cn,[status(thm)],[1563,theory(equality)])).
% cnf(1596,negated_conjecture,(k7_relat_1(u2_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)))=u2_lattices(esk29_0)|~v1_relat_1(u2_lattices(esk29_0))),inference(spm,[status(thm)],[545,1536,theory(equality)])).
% cnf(1597,negated_conjecture,(k7_relat_1(u2_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)))=u2_lattices(esk29_0)|$false),inference(rw,[status(thm)],[1596,1222,theory(equality)])).
% cnf(1598,negated_conjecture,(k7_relat_1(u2_lattices(esk29_0),k2_zfmisc_1(k1_filter_0(esk29_0),k1_filter_0(esk29_0)))=u2_lattices(esk29_0)),inference(cn,[status(thm)],[1597,theory(equality)])).
% cnf(1601,negated_conjecture,(u2_lattices(esk29_0)=k1_realset1(u2_lattices(esk29_0),k1_filter_0(esk29_0))|~v1_relat_1(u2_lattices(esk29_0))),inference(spm,[status(thm)],[375,1598,theory(equality)])).
% cnf(1607,negated_conjecture,(u2_lattices(esk29_0)=k1_realset1(u2_lattices(esk29_0),k1_filter_0(esk29_0))|$false),inference(rw,[status(thm)],[1601,1222,theory(equality)])).
% cnf(1608,negated_conjecture,(u2_lattices(esk29_0)=k1_realset1(u2_lattices(esk29_0),k1_filter_0(esk29_0))),inference(cn,[status(thm)],[1607,theory(equality)])).
% cnf(3135,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),esk15_3(esk29_0,k1_filter_0(esk29_0),X1),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_lattice4(k1_filter_0(esk29_0),esk29_0)|~m2_nat_lat(X1,esk29_0)|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(spm,[status(thm)],[780,1564,theory(equality)])).
% cnf(3149,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),esk15_3(esk29_0,k1_filter_0(esk29_0),X1),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|$false|~m2_nat_lat(X1,esk29_0)|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[3135,1049,theory(equality)])).
% cnf(3150,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),esk15_3(esk29_0,k1_filter_0(esk29_0),X1),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|$false|~m2_nat_lat(X1,esk29_0)|$false|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[3149,565,theory(equality)])).
% cnf(3151,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),esk15_3(esk29_0,k1_filter_0(esk29_0),X1),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|$false|~m2_nat_lat(X1,esk29_0)|$false|$false),inference(rw,[status(thm)],[3150,566,theory(equality)])).
% cnf(3152,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),esk15_3(esk29_0,k1_filter_0(esk29_0),X1),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)),inference(cn,[status(thm)],[3151,theory(equality)])).
% cnf(3153,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),esk15_3(esk29_0,k1_filter_0(esk29_0),X1),u1_lattices(esk29_0))=X1|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)),inference(sr,[status(thm)],[3152,1017,theory(equality)])).
% cnf(3154,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),esk15_3(esk29_0,k1_filter_0(esk29_0),X1),u1_lattices(esk29_0))=X1|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)),inference(sr,[status(thm)],[3153,567,theory(equality)])).
% cnf(13634,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),k1_realset1(u2_lattices(esk29_0),k1_filter_0(esk29_0)),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)|~m2_lattice4(k1_filter_0(esk29_0),esk29_0)|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(spm,[status(thm)],[3154,254,theory(equality)])).
% cnf(13635,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)|~m2_lattice4(k1_filter_0(esk29_0),esk29_0)|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[13634,1608,theory(equality)])).
% cnf(13636,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)|$false|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[13635,1049,theory(equality)])).
% cnf(13637,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)|$false|$false|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[13636,565,theory(equality)])).
% cnf(13638,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)|$false|$false|$false),inference(rw,[status(thm)],[13637,566,theory(equality)])).
% cnf(13639,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))=X1|v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)),inference(cn,[status(thm)],[13638,theory(equality)])).
% cnf(13640,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))=X1|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)),inference(sr,[status(thm)],[13639,1017,theory(equality)])).
% cnf(13641,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))=X1|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=X1|~m2_nat_lat(X1,esk29_0)),inference(sr,[status(thm)],[13640,567,theory(equality)])).
% cnf(13642,negated_conjecture,(g3_lattices(k1_filter_0(esk29_0),u2_lattices(esk29_0),u1_lattices(esk29_0))=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|~m2_nat_lat(k23_filter_2(esk29_0,k1_filter_0(esk29_0)),esk29_0)),inference(er,[status(thm)],[13641,theory(equality)])).
% cnf(13644,negated_conjecture,(k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=k23_filter_2(esk29_0,k17_filter_2(esk29_0))|k23_filter_2(esk29_0,k1_filter_0(esk29_0))!=k23_filter_2(esk29_0,k1_filter_2(esk29_0))|~m2_nat_lat(k23_filter_2(esk29_0,k1_filter_0(esk29_0)),esk29_0)),inference(spm,[status(thm)],[827,13642,theory(equality)])).
% cnf(13750,negated_conjecture,(v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|k23_filter_2(esk29_0,k1_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|~m2_lattice4(k1_filter_0(esk29_0),esk29_0)|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(spm,[status(thm)],[13644,208,theory(equality)])).
% cnf(13751,negated_conjecture,(v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|k23_filter_2(esk29_0,k1_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|$false|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[13750,1049,theory(equality)])).
% cnf(13752,negated_conjecture,(v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|k23_filter_2(esk29_0,k1_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|$false|$false|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[13751,565,theory(equality)])).
% cnf(13753,negated_conjecture,(v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|k23_filter_2(esk29_0,k1_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|$false|$false|$false),inference(rw,[status(thm)],[13752,566,theory(equality)])).
% cnf(13754,negated_conjecture,(v1_xboole_0(k1_filter_0(esk29_0))|v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|k23_filter_2(esk29_0,k1_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))),inference(cn,[status(thm)],[13753,theory(equality)])).
% cnf(13755,negated_conjecture,(v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|k23_filter_2(esk29_0,k1_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))),inference(sr,[status(thm)],[13754,1017,theory(equality)])).
% cnf(13756,negated_conjecture,(k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|k23_filter_2(esk29_0,k1_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))),inference(sr,[status(thm)],[13755,567,theory(equality)])).
% cnf(13757,negated_conjecture,(v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(spm,[status(thm)],[13756,158,theory(equality)])).
% cnf(13758,negated_conjecture,(v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|$false|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[13757,565,theory(equality)])).
% cnf(13759,negated_conjecture,(v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|$false|$false),inference(rw,[status(thm)],[13758,566,theory(equality)])).
% cnf(13760,negated_conjecture,(v3_struct_0(esk29_0)|k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))),inference(cn,[status(thm)],[13759,theory(equality)])).
% cnf(13761,negated_conjecture,(k23_filter_2(esk29_0,k17_filter_2(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))),inference(sr,[status(thm)],[13760,567,theory(equality)])).
% cnf(13762,negated_conjecture,(v3_struct_0(esk29_0)|k23_filter_2(esk29_0,u1_struct_0(esk29_0))!=k23_filter_2(esk29_0,k1_filter_0(esk29_0))|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(spm,[status(thm)],[13761,146,theory(equality)])).
% cnf(13763,negated_conjecture,(v3_struct_0(esk29_0)|$false|~l3_lattices(esk29_0)|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[13762,654,theory(equality)])).
% cnf(13764,negated_conjecture,(v3_struct_0(esk29_0)|$false|$false|~v10_lattices(esk29_0)),inference(rw,[status(thm)],[13763,565,theory(equality)])).
% cnf(13765,negated_conjecture,(v3_struct_0(esk29_0)|$false|$false|$false),inference(rw,[status(thm)],[13764,566,theory(equality)])).
% cnf(13766,negated_conjecture,(v3_struct_0(esk29_0)),inference(cn,[status(thm)],[13765,theory(equality)])).
% cnf(13767,negated_conjecture,($false),inference(sr,[status(thm)],[13766,567,theory(equality)])).
% cnf(13768,negated_conjecture,($false),13767,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2208
% # ...of these trivial : 53
% # ...subsumed : 861
% # ...remaining for further processing: 1294
% # Other redundant clauses eliminated : 3
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 27
% # Backward-rewritten : 9
% # Generated clauses : 6657
% # ...of the previous two non-trivial : 5453
% # Contextual simplify-reflections : 672
% # Paramodulations : 6622
% # Factorizations : 0
% # Equation resolutions : 32
% # Current number of processed clauses: 1081
% # Positive orientable unit clauses: 213
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 27
% # Non-unit-clauses : 841
% # Current number of unprocessed clauses: 3484
% # ...number of literals in the above : 21170
% # Clause-clause subsumption calls (NU) : 52727
% # Rec. Clause-clause subsumption calls : 13180
% # Unit Clause-clause subsumption calls : 1448
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 179
% # Indexed BW rewrite successes : 5
% # Backwards rewriting index: 953 leaves, 1.47+/-1.281 terms/leaf
% # Paramod-from index: 473 leaves, 1.32+/-1.105 terms/leaf
% # Paramod-into index: 822 leaves, 1.39+/-1.053 terms/leaf
% # -------------------------------------------------
% # User time : 0.479 s
% # System time : 0.015 s
% # Total time : 0.494 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.78 CPU 0.85 WC
% FINAL PrfWatch: 0.78 CPU 0.85 WC
% SZS output end Solution for /tmp/SystemOnTPTP5757/LAT332+1.tptp
%
%------------------------------------------------------------------------------