%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LAT301+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 : art03.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 09:56:47 EST 2010
% Result : Theorem 1.29s
% Output : Solution 1.29s
% 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/SystemOnTPTP27074/LAT301+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP27074/LAT301+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP27074/LAT301+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 27170
% 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(7, 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(8, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>(v13_lattices(X1)<=>v14_lattices(k1_lattice2(X1)))),file('/tmp/SRASS.s.p', t63_lattice2)).
% fof(9, axiom,![X1]:((((~(v3_struct_0(X1))&v10_lattices(X1))&v13_lattices(X1))&l3_lattices(X1))=>k5_lattices(X1)=k6_lattices(k1_lattice2(X1))),file('/tmp/SRASS.s.p', t78_lattice2)).
% fof(16, 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(22, 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(23, 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(24, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m1_filter_0(X2,X1)=>((((~(v3_struct_0(X1))&v10_lattices(X1))&v14_lattices(X1))&l3_lattices(X1))=>r2_hidden(k6_lattices(X1),X2)))),file('/tmp/SRASS.s.p', t12_filter_0)).
% fof(30, 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(32, 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(37, axiom,![X1]:(l3_lattices(X1)=>(v3_lattices(k1_lattice2(X1))&l3_lattices(k1_lattice2(X1)))),file('/tmp/SRASS.s.p', dt_k1_lattice2)).
% fof(41, 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(47, axiom,![X1]:(l3_lattices(X1)=>(((((((~(v3_struct_0(X1))&v4_lattices(X1))&v5_lattices(X1))&v6_lattices(X1))&v7_lattices(X1))&v8_lattices(X1))&v9_lattices(X1))=>(~(v3_struct_0(X1))&v10_lattices(X1)))),file('/tmp/SRASS.s.p', cc2_lattices)).
% fof(62, 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(88, conjecture,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m2_filter_2(X2,X1)=>(v13_lattices(X1)=>r2_hidden(k5_lattices(X1),X2)))),file('/tmp/SRASS.s.p', t25_filter_2)).
% fof(89, negated_conjecture,~(![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m2_filter_2(X2,X1)=>(v13_lattices(X1)=>r2_hidden(k5_lattices(X1),X2))))),inference(assume_negation,[status(cth)],[88])).
% fof(95, 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)],[7,theory(equality)])).
% fof(96, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>(v13_lattices(X1)<=>v14_lattices(k1_lattice2(X1)))),inference(fof_simplification,[status(thm)],[8,theory(equality)])).
% fof(97, plain,![X1]:((((~(v3_struct_0(X1))&v10_lattices(X1))&v13_lattices(X1))&l3_lattices(X1))=>k5_lattices(X1)=k6_lattices(k1_lattice2(X1))),inference(fof_simplification,[status(thm)],[9,theory(equality)])).
% fof(102, 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)],[16,theory(equality)])).
% fof(104, 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)],[22,theory(equality)])).
% fof(105, 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)],[23,theory(equality)])).
% fof(106, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m1_filter_0(X2,X1)=>((((~(v3_struct_0(X1))&v10_lattices(X1))&v14_lattices(X1))&l3_lattices(X1))=>r2_hidden(k6_lattices(X1),X2)))),inference(fof_simplification,[status(thm)],[24,theory(equality)])).
% fof(110, 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)],[30,theory(equality)])).
% fof(111, 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)],[32,theory(equality)])).
% fof(116, 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)],[41,theory(equality)])).
% fof(119, plain,![X1]:(l3_lattices(X1)=>(((((((~(v3_struct_0(X1))&v4_lattices(X1))&v5_lattices(X1))&v6_lattices(X1))&v7_lattices(X1))&v8_lattices(X1))&v9_lattices(X1))=>(~(v3_struct_0(X1))&v10_lattices(X1)))),inference(fof_simplification,[status(thm)],[47,theory(equality)])).
% fof(126, 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)],[62,theory(equality)])).
% fof(132, negated_conjecture,~(![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m2_filter_2(X2,X1)=>(v13_lattices(X1)=>r2_hidden(k5_lattices(X1),X2))))),inference(fof_simplification,[status(thm)],[89,theory(equality)])).
% fof(155, 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)],[95])).
% fof(156, 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)],[155])).
% fof(157, 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)],[156])).
% fof(158, 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)],[157])).
% cnf(159,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)],[158])).
% fof(161, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|((~(v13_lattices(X1))|v14_lattices(k1_lattice2(X1)))&(~(v14_lattices(k1_lattice2(X1)))|v13_lattices(X1)))),inference(fof_nnf,[status(thm)],[96])).
% fof(162, plain,![X2]:(((v3_struct_0(X2)|~(v10_lattices(X2)))|~(l3_lattices(X2)))|((~(v13_lattices(X2))|v14_lattices(k1_lattice2(X2)))&(~(v14_lattices(k1_lattice2(X2)))|v13_lattices(X2)))),inference(variable_rename,[status(thm)],[161])).
% fof(163, plain,![X2]:(((~(v13_lattices(X2))|v14_lattices(k1_lattice2(X2)))|((v3_struct_0(X2)|~(v10_lattices(X2)))|~(l3_lattices(X2))))&((~(v14_lattices(k1_lattice2(X2)))|v13_lattices(X2))|((v3_struct_0(X2)|~(v10_lattices(X2)))|~(l3_lattices(X2))))),inference(distribute,[status(thm)],[162])).
% cnf(165,plain,(v3_struct_0(X1)|v14_lattices(k1_lattice2(X1))|~l3_lattices(X1)|~v10_lattices(X1)|~v13_lattices(X1)),inference(split_conjunct,[status(thm)],[163])).
% fof(166, plain,![X1]:((((v3_struct_0(X1)|~(v10_lattices(X1)))|~(v13_lattices(X1)))|~(l3_lattices(X1)))|k5_lattices(X1)=k6_lattices(k1_lattice2(X1))),inference(fof_nnf,[status(thm)],[97])).
% fof(167, plain,![X2]:((((v3_struct_0(X2)|~(v10_lattices(X2)))|~(v13_lattices(X2)))|~(l3_lattices(X2)))|k5_lattices(X2)=k6_lattices(k1_lattice2(X2))),inference(variable_rename,[status(thm)],[166])).
% cnf(168,plain,(k5_lattices(X1)=k6_lattices(k1_lattice2(X1))|v3_struct_0(X1)|~l3_lattices(X1)|~v13_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[167])).
% fof(197, 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)],[102])).
% fof(198, 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)],[197])).
% cnf(199,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)],[198])).
% fof(215, 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)],[104])).
% fof(216, 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)],[215])).
% cnf(217,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)],[216])).
% fof(218, 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)],[105])).
% fof(219, 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)],[218])).
% fof(220, 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)],[219])).
% fof(221, 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)],[220])).
% cnf(223,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)],[221])).
% fof(224, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|![X2]:(~(m1_filter_0(X2,X1))|((((v3_struct_0(X1)|~(v10_lattices(X1)))|~(v14_lattices(X1)))|~(l3_lattices(X1)))|r2_hidden(k6_lattices(X1),X2)))),inference(fof_nnf,[status(thm)],[106])).
% fof(225, plain,![X3]:(((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))|![X4]:(~(m1_filter_0(X4,X3))|((((v3_struct_0(X3)|~(v10_lattices(X3)))|~(v14_lattices(X3)))|~(l3_lattices(X3)))|r2_hidden(k6_lattices(X3),X4)))),inference(variable_rename,[status(thm)],[224])).
% fof(226, plain,![X3]:![X4]:((~(m1_filter_0(X4,X3))|((((v3_struct_0(X3)|~(v10_lattices(X3)))|~(v14_lattices(X3)))|~(l3_lattices(X3)))|r2_hidden(k6_lattices(X3),X4)))|((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))),inference(shift_quantors,[status(thm)],[225])).
% cnf(227,plain,(v3_struct_0(X1)|r2_hidden(k6_lattices(X1),X2)|v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)|~l3_lattices(X1)|~v14_lattices(X1)|~v10_lattices(X1)|~m1_filter_0(X2,X1)),inference(split_conjunct,[status(thm)],[226])).
% fof(248, 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)],[110])).
% fof(249, 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)],[248])).
% fof(250, 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)],[249])).
% cnf(251,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)],[250])).
% fof(255, 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)],[111])).
% fof(256, 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)],[255])).
% fof(257, 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)],[256])).
% cnf(259,plain,(v3_struct_0(X1)|~l3_lattices(X1)|~v3_struct_0(k1_lattice2(X1))),inference(split_conjunct,[status(thm)],[257])).
% fof(276, plain,![X1]:(~(l3_lattices(X1))|(v3_lattices(k1_lattice2(X1))&l3_lattices(k1_lattice2(X1)))),inference(fof_nnf,[status(thm)],[37])).
% fof(277, plain,![X2]:(~(l3_lattices(X2))|(v3_lattices(k1_lattice2(X2))&l3_lattices(k1_lattice2(X2)))),inference(variable_rename,[status(thm)],[276])).
% fof(278, plain,![X2]:((v3_lattices(k1_lattice2(X2))|~(l3_lattices(X2)))&(l3_lattices(k1_lattice2(X2))|~(l3_lattices(X2)))),inference(distribute,[status(thm)],[277])).
% cnf(279,plain,(l3_lattices(k1_lattice2(X1))|~l3_lattices(X1)),inference(split_conjunct,[status(thm)],[278])).
% fof(293, 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)],[116])).
% fof(294, 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)],[293])).
% fof(295, 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)],[294])).
% cnf(296,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)],[295])).
% fof(319, plain,![X1]:(~(l3_lattices(X1))|(((((((v3_struct_0(X1)|~(v4_lattices(X1)))|~(v5_lattices(X1)))|~(v6_lattices(X1)))|~(v7_lattices(X1)))|~(v8_lattices(X1)))|~(v9_lattices(X1)))|(~(v3_struct_0(X1))&v10_lattices(X1)))),inference(fof_nnf,[status(thm)],[119])).
% fof(320, plain,![X2]:(~(l3_lattices(X2))|(((((((v3_struct_0(X2)|~(v4_lattices(X2)))|~(v5_lattices(X2)))|~(v6_lattices(X2)))|~(v7_lattices(X2)))|~(v8_lattices(X2)))|~(v9_lattices(X2)))|(~(v3_struct_0(X2))&v10_lattices(X2)))),inference(variable_rename,[status(thm)],[319])).
% fof(321, plain,![X2]:(((~(v3_struct_0(X2))|((((((v3_struct_0(X2)|~(v4_lattices(X2)))|~(v5_lattices(X2)))|~(v6_lattices(X2)))|~(v7_lattices(X2)))|~(v8_lattices(X2)))|~(v9_lattices(X2))))|~(l3_lattices(X2)))&((v10_lattices(X2)|((((((v3_struct_0(X2)|~(v4_lattices(X2)))|~(v5_lattices(X2)))|~(v6_lattices(X2)))|~(v7_lattices(X2)))|~(v8_lattices(X2)))|~(v9_lattices(X2))))|~(l3_lattices(X2)))),inference(distribute,[status(thm)],[320])).
% cnf(322,plain,(v3_struct_0(X1)|v10_lattices(X1)|~l3_lattices(X1)|~v9_lattices(X1)|~v8_lattices(X1)|~v7_lattices(X1)|~v6_lattices(X1)|~v5_lattices(X1)|~v4_lattices(X1)),inference(split_conjunct,[status(thm)],[321])).
% fof(386, 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)],[126])).
% fof(387, 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)],[386])).
% fof(388, 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)],[387])).
% cnf(390,plain,(v3_struct_0(X1)|v9_lattices(k1_lattice2(X1))|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[388])).
% cnf(391,plain,(v3_struct_0(X1)|v8_lattices(k1_lattice2(X1))|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[388])).
% cnf(392,plain,(v3_struct_0(X1)|v7_lattices(k1_lattice2(X1))|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[388])).
% cnf(393,plain,(v3_struct_0(X1)|v6_lattices(k1_lattice2(X1))|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[388])).
% cnf(394,plain,(v3_struct_0(X1)|v5_lattices(k1_lattice2(X1))|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[388])).
% cnf(395,plain,(v3_struct_0(X1)|v4_lattices(k1_lattice2(X1))|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[388])).
% fof(505, negated_conjecture,?[X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))&?[X2]:(m2_filter_2(X2,X1)&(v13_lattices(X1)&~(r2_hidden(k5_lattices(X1),X2))))),inference(fof_nnf,[status(thm)],[132])).
% fof(506, negated_conjecture,?[X3]:(((~(v3_struct_0(X3))&v10_lattices(X3))&l3_lattices(X3))&?[X4]:(m2_filter_2(X4,X3)&(v13_lattices(X3)&~(r2_hidden(k5_lattices(X3),X4))))),inference(variable_rename,[status(thm)],[505])).
% fof(507, negated_conjecture,(((~(v3_struct_0(esk26_0))&v10_lattices(esk26_0))&l3_lattices(esk26_0))&(m2_filter_2(esk27_0,esk26_0)&(v13_lattices(esk26_0)&~(r2_hidden(k5_lattices(esk26_0),esk27_0))))),inference(skolemize,[status(esa)],[506])).
% cnf(508,negated_conjecture,(~r2_hidden(k5_lattices(esk26_0),esk27_0)),inference(split_conjunct,[status(thm)],[507])).
% cnf(509,negated_conjecture,(v13_lattices(esk26_0)),inference(split_conjunct,[status(thm)],[507])).
% cnf(510,negated_conjecture,(m2_filter_2(esk27_0,esk26_0)),inference(split_conjunct,[status(thm)],[507])).
% cnf(511,negated_conjecture,(l3_lattices(esk26_0)),inference(split_conjunct,[status(thm)],[507])).
% cnf(512,negated_conjecture,(v10_lattices(esk26_0)),inference(split_conjunct,[status(thm)],[507])).
% cnf(513,negated_conjecture,(~v3_struct_0(esk26_0)),inference(split_conjunct,[status(thm)],[507])).
% cnf(557,negated_conjecture,(v3_struct_0(esk26_0)|~v3_struct_0(k1_lattice2(esk26_0))),inference(spm,[status(thm)],[259,511,theory(equality)])).
% cnf(564,negated_conjecture,(~v3_struct_0(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[557,513,theory(equality)])).
% cnf(669,negated_conjecture,(v4_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[395,512,theory(equality)])).
% cnf(673,negated_conjecture,(v4_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|$false),inference(rw,[status(thm)],[669,511,theory(equality)])).
% cnf(674,negated_conjecture,(v4_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[673,theory(equality)])).
% cnf(675,negated_conjecture,(v4_lattices(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[674,513,theory(equality)])).
% cnf(693,negated_conjecture,(v5_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[394,512,theory(equality)])).
% cnf(697,negated_conjecture,(v5_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|$false),inference(rw,[status(thm)],[693,511,theory(equality)])).
% cnf(698,negated_conjecture,(v5_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[697,theory(equality)])).
% cnf(699,negated_conjecture,(v5_lattices(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[698,513,theory(equality)])).
% cnf(706,negated_conjecture,(v6_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[393,512,theory(equality)])).
% cnf(710,negated_conjecture,(v6_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|$false),inference(rw,[status(thm)],[706,511,theory(equality)])).
% cnf(711,negated_conjecture,(v6_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[710,theory(equality)])).
% cnf(712,negated_conjecture,(v6_lattices(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[711,513,theory(equality)])).
% cnf(719,negated_conjecture,(v7_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[392,512,theory(equality)])).
% cnf(723,negated_conjecture,(v7_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|$false),inference(rw,[status(thm)],[719,511,theory(equality)])).
% cnf(724,negated_conjecture,(v7_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[723,theory(equality)])).
% cnf(725,negated_conjecture,(v7_lattices(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[724,513,theory(equality)])).
% cnf(732,negated_conjecture,(v8_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[391,512,theory(equality)])).
% cnf(736,negated_conjecture,(v8_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|$false),inference(rw,[status(thm)],[732,511,theory(equality)])).
% cnf(737,negated_conjecture,(v8_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[736,theory(equality)])).
% cnf(738,negated_conjecture,(v8_lattices(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[737,513,theory(equality)])).
% cnf(745,negated_conjecture,(v9_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[390,512,theory(equality)])).
% cnf(749,negated_conjecture,(v9_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|$false),inference(rw,[status(thm)],[745,511,theory(equality)])).
% cnf(750,negated_conjecture,(v9_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[749,theory(equality)])).
% cnf(751,negated_conjecture,(v9_lattices(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[750,513,theory(equality)])).
% cnf(849,negated_conjecture,(v14_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|~v10_lattices(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[165,509,theory(equality)])).
% cnf(852,negated_conjecture,(v14_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|$false|~l3_lattices(esk26_0)),inference(rw,[status(thm)],[849,512,theory(equality)])).
% cnf(853,negated_conjecture,(v14_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|$false|$false),inference(rw,[status(thm)],[852,511,theory(equality)])).
% cnf(854,negated_conjecture,(v14_lattices(k1_lattice2(esk26_0))|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[853,theory(equality)])).
% cnf(855,negated_conjecture,(v14_lattices(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[854,513,theory(equality)])).
% cnf(862,negated_conjecture,(m2_lattice4(esk27_0,esk26_0)|v3_struct_0(esk26_0)|~v10_lattices(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[159,510,theory(equality)])).
% cnf(864,negated_conjecture,(m2_lattice4(esk27_0,esk26_0)|v3_struct_0(esk26_0)|$false|~l3_lattices(esk26_0)),inference(rw,[status(thm)],[862,512,theory(equality)])).
% cnf(865,negated_conjecture,(m2_lattice4(esk27_0,esk26_0)|v3_struct_0(esk26_0)|$false|$false),inference(rw,[status(thm)],[864,511,theory(equality)])).
% cnf(866,negated_conjecture,(m2_lattice4(esk27_0,esk26_0)|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[865,theory(equality)])).
% cnf(867,negated_conjecture,(m2_lattice4(esk27_0,esk26_0)),inference(sr,[status(thm)],[866,513,theory(equality)])).
% cnf(868,negated_conjecture,(v3_struct_0(esk26_0)|~r2_hidden(k6_lattices(k1_lattice2(esk26_0)),esk27_0)|~v13_lattices(esk26_0)|~v10_lattices(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[508,168,theory(equality)])).
% cnf(869,negated_conjecture,(v3_struct_0(esk26_0)|~r2_hidden(k6_lattices(k1_lattice2(esk26_0)),esk27_0)|$false|~v10_lattices(esk26_0)|~l3_lattices(esk26_0)),inference(rw,[status(thm)],[868,509,theory(equality)])).
% cnf(870,negated_conjecture,(v3_struct_0(esk26_0)|~r2_hidden(k6_lattices(k1_lattice2(esk26_0)),esk27_0)|$false|$false|~l3_lattices(esk26_0)),inference(rw,[status(thm)],[869,512,theory(equality)])).
% cnf(871,negated_conjecture,(v3_struct_0(esk26_0)|~r2_hidden(k6_lattices(k1_lattice2(esk26_0)),esk27_0)|$false|$false|$false),inference(rw,[status(thm)],[870,511,theory(equality)])).
% cnf(872,negated_conjecture,(v3_struct_0(esk26_0)|~r2_hidden(k6_lattices(k1_lattice2(esk26_0)),esk27_0)),inference(cn,[status(thm)],[871,theory(equality)])).
% cnf(873,negated_conjecture,(~r2_hidden(k6_lattices(k1_lattice2(esk26_0)),esk27_0)),inference(sr,[status(thm)],[872,513,theory(equality)])).
% cnf(913,negated_conjecture,(k15_filter_2(esk26_0,esk27_0)=k7_filter_2(esk26_0,esk27_0)|v3_struct_0(esk26_0)|~v10_lattices(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[217,510,theory(equality)])).
% cnf(915,negated_conjecture,(k15_filter_2(esk26_0,esk27_0)=k7_filter_2(esk26_0,esk27_0)|v3_struct_0(esk26_0)|$false|~l3_lattices(esk26_0)),inference(rw,[status(thm)],[913,512,theory(equality)])).
% cnf(916,negated_conjecture,(k15_filter_2(esk26_0,esk27_0)=k7_filter_2(esk26_0,esk27_0)|v3_struct_0(esk26_0)|$false|$false),inference(rw,[status(thm)],[915,511,theory(equality)])).
% cnf(917,negated_conjecture,(k15_filter_2(esk26_0,esk27_0)=k7_filter_2(esk26_0,esk27_0)|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[916,theory(equality)])).
% cnf(918,negated_conjecture,(k15_filter_2(esk26_0,esk27_0)=k7_filter_2(esk26_0,esk27_0)),inference(sr,[status(thm)],[917,513,theory(equality)])).
% cnf(1020,negated_conjecture,(m1_filter_2(k15_filter_2(esk26_0,esk27_0),k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|~v10_lattices(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[199,510,theory(equality)])).
% cnf(1022,negated_conjecture,(m1_filter_2(k15_filter_2(esk26_0,esk27_0),k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|$false|~l3_lattices(esk26_0)),inference(rw,[status(thm)],[1020,512,theory(equality)])).
% cnf(1023,negated_conjecture,(m1_filter_2(k15_filter_2(esk26_0,esk27_0),k1_lattice2(esk26_0))|v3_struct_0(esk26_0)|$false|$false),inference(rw,[status(thm)],[1022,511,theory(equality)])).
% cnf(1024,negated_conjecture,(m1_filter_2(k15_filter_2(esk26_0,esk27_0),k1_lattice2(esk26_0))|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[1023,theory(equality)])).
% cnf(1025,negated_conjecture,(m1_filter_2(k15_filter_2(esk26_0,esk27_0),k1_lattice2(esk26_0))),inference(sr,[status(thm)],[1024,513,theory(equality)])).
% cnf(1050,negated_conjecture,(k7_filter_2(esk26_0,X1)=X1|v3_struct_0(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[296,512,theory(equality)])).
% cnf(1055,negated_conjecture,(k7_filter_2(esk26_0,X1)=X1|v3_struct_0(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false),inference(rw,[status(thm)],[1050,511,theory(equality)])).
% cnf(1056,negated_conjecture,(k7_filter_2(esk26_0,X1)=X1|v3_struct_0(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(cn,[status(thm)],[1055,theory(equality)])).
% cnf(1057,negated_conjecture,(k7_filter_2(esk26_0,X1)=X1|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(sr,[status(thm)],[1056,513,theory(equality)])).
% cnf(1148,negated_conjecture,(m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|v3_struct_0(esk26_0)|~v10_lattices(esk26_0)|~l3_lattices(esk26_0)),inference(spm,[status(thm)],[251,867,theory(equality)])).
% cnf(1149,negated_conjecture,(m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|v3_struct_0(esk26_0)|$false|~l3_lattices(esk26_0)),inference(rw,[status(thm)],[1148,512,theory(equality)])).
% cnf(1150,negated_conjecture,(m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|v3_struct_0(esk26_0)|$false|$false),inference(rw,[status(thm)],[1149,511,theory(equality)])).
% cnf(1151,negated_conjecture,(m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|v3_struct_0(esk26_0)),inference(cn,[status(thm)],[1150,theory(equality)])).
% cnf(1152,negated_conjecture,(m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(sr,[status(thm)],[1151,513,theory(equality)])).
% cnf(1496,negated_conjecture,(m1_filter_2(k7_filter_2(esk26_0,esk27_0),k1_lattice2(esk26_0))),inference(rw,[status(thm)],[1025,918,theory(equality)])).
% cnf(1554,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|~v14_lattices(k1_lattice2(esk26_0))|~m1_filter_0(esk27_0,k1_lattice2(esk26_0))|~v10_lattices(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))),inference(spm,[status(thm)],[873,227,theory(equality)])).
% cnf(1556,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|$false|~m1_filter_0(esk27_0,k1_lattice2(esk26_0))|~v10_lattices(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))),inference(rw,[status(thm)],[1554,855,theory(equality)])).
% cnf(1557,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|~m1_filter_0(esk27_0,k1_lattice2(esk26_0))|~v10_lattices(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))),inference(cn,[status(thm)],[1556,theory(equality)])).
% cnf(1558,negated_conjecture,(~m1_filter_0(esk27_0,k1_lattice2(esk26_0))|~v10_lattices(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[1557,564,theory(equality)])).
% cnf(2227,negated_conjecture,(m1_filter_2(esk27_0,k1_lattice2(esk26_0))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(spm,[status(thm)],[1496,1057,theory(equality)])).
% cnf(2231,negated_conjecture,(m1_filter_2(esk27_0,k1_lattice2(esk26_0))|$false),inference(rw,[status(thm)],[2227,1152,theory(equality)])).
% cnf(2232,negated_conjecture,(m1_filter_2(esk27_0,k1_lattice2(esk26_0))),inference(cn,[status(thm)],[2231,theory(equality)])).
% cnf(2234,negated_conjecture,(m1_filter_0(esk27_0,k1_lattice2(esk26_0))|v3_struct_0(k1_lattice2(esk26_0))|~v10_lattices(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))),inference(spm,[status(thm)],[223,2232,theory(equality)])).
% cnf(2236,negated_conjecture,(m1_filter_0(esk27_0,k1_lattice2(esk26_0))|~v10_lattices(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[2234,564,theory(equality)])).
% cnf(2367,negated_conjecture,(~v10_lattices(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))),inference(csr,[status(thm)],[2236,1558])).
% cnf(2368,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))|~v9_lattices(k1_lattice2(esk26_0))|~v8_lattices(k1_lattice2(esk26_0))|~v7_lattices(k1_lattice2(esk26_0))|~v6_lattices(k1_lattice2(esk26_0))|~v5_lattices(k1_lattice2(esk26_0))|~v4_lattices(k1_lattice2(esk26_0))),inference(spm,[status(thm)],[2367,322,theory(equality)])).
% cnf(2370,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))|$false|~v8_lattices(k1_lattice2(esk26_0))|~v7_lattices(k1_lattice2(esk26_0))|~v6_lattices(k1_lattice2(esk26_0))|~v5_lattices(k1_lattice2(esk26_0))|~v4_lattices(k1_lattice2(esk26_0))),inference(rw,[status(thm)],[2368,751,theory(equality)])).
% cnf(2371,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))|$false|$false|~v7_lattices(k1_lattice2(esk26_0))|~v6_lattices(k1_lattice2(esk26_0))|~v5_lattices(k1_lattice2(esk26_0))|~v4_lattices(k1_lattice2(esk26_0))),inference(rw,[status(thm)],[2370,738,theory(equality)])).
% cnf(2372,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))|$false|$false|$false|~v6_lattices(k1_lattice2(esk26_0))|~v5_lattices(k1_lattice2(esk26_0))|~v4_lattices(k1_lattice2(esk26_0))),inference(rw,[status(thm)],[2371,725,theory(equality)])).
% cnf(2373,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))|$false|$false|$false|$false|~v5_lattices(k1_lattice2(esk26_0))|~v4_lattices(k1_lattice2(esk26_0))),inference(rw,[status(thm)],[2372,712,theory(equality)])).
% cnf(2374,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))|$false|$false|$false|$false|$false|~v4_lattices(k1_lattice2(esk26_0))),inference(rw,[status(thm)],[2373,699,theory(equality)])).
% cnf(2375,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[2374,675,theory(equality)])).
% cnf(2376,negated_conjecture,(v3_struct_0(k1_lattice2(esk26_0))|~l3_lattices(k1_lattice2(esk26_0))),inference(cn,[status(thm)],[2375,theory(equality)])).
% cnf(2377,negated_conjecture,(~l3_lattices(k1_lattice2(esk26_0))),inference(sr,[status(thm)],[2376,564,theory(equality)])).
% cnf(2382,negated_conjecture,(~l3_lattices(esk26_0)),inference(spm,[status(thm)],[2377,279,theory(equality)])).
% cnf(2383,negated_conjecture,($false),inference(rw,[status(thm)],[2382,511,theory(equality)])).
% cnf(2384,negated_conjecture,($false),inference(cn,[status(thm)],[2383,theory(equality)])).
% cnf(2385,negated_conjecture,($false),2384,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 732
% # ...of these trivial : 8
% # ...subsumed : 56
% # ...remaining for further processing: 668
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 2
% # Backward-rewritten : 7
% # Generated clauses : 916
% # ...of the previous two non-trivial : 861
% # Contextual simplify-reflections : 57
% # Paramodulations : 910
% # Factorizations : 0
% # Equation resolutions : 3
% # Current number of processed clauses: 502
% # Positive orientable unit clauses: 255
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 46
% # Non-unit-clauses : 201
% # Current number of unprocessed clauses: 445
% # ...number of literals in the above : 1952
% # Clause-clause subsumption calls (NU) : 3930
% # Rec. Clause-clause subsumption calls : 1983
% # Unit Clause-clause subsumption calls : 748
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 512
% # Indexed BW rewrite successes : 4
% # Backwards rewriting index: 553 leaves, 1.25+/-1.550 terms/leaf
% # Paramod-from index: 238 leaves, 1.24+/-1.727 terms/leaf
% # Paramod-into index: 452 leaves, 1.21+/-1.416 terms/leaf
% # -------------------------------------------------
% # User time : 0.098 s
% # System time : 0.006 s
% # Total time : 0.104 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.21 CPU 0.31 WC
% FINAL PrfWatch: 0.21 CPU 0.31 WC
% SZS output end Solution for /tmp/SystemOnTPTP27074/LAT301+1.tptp
%
%------------------------------------------------------------------------------