%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LAT303+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 10:04:53 EST 2010
% Result : Theorem 2.75s
% Output : Solution 2.75s
% 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/SystemOnTPTP18284/LAT303+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP18284/LAT303+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP18284/LAT303+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 18416
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.024 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(2, axiom,![X1]:?[X2]:m1_subset_1(X2,X1),file('/tmp/SRASS.s.p', existence_m1_subset_1)).
% fof(4, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m1_subset_1(X2,u1_struct_0(X1))=>(m1_filter_0(k6_domain_1(u1_struct_0(X1),X2),X1)=>v14_lattices(X1)))),file('/tmp/SRASS.s.p', t14_filter_0)).
% fof(7, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>?[X2]:m1_filter_2(X2,X1)),file('/tmp/SRASS.s.p', existence_m1_filter_2)).
% fof(9, 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(10, 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(12, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m2_filter_2(X2,X1)<=>m1_filter_2(X2,k1_lattice2(X1)))),file('/tmp/SRASS.s.p', t21_filter_2)).
% fof(13, 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(14, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m1_filter_0(X2,X1)=>(~(v1_xboole_0(X2))&m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))))),file('/tmp/SRASS.s.p', dt_m1_filter_0)).
% fof(20, 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(31, axiom,![X1]:![X2]:((~(v1_xboole_0(X1))&m1_subset_1(X2,X1))=>k6_domain_1(X1,X2)=k1_tarski(X2)),file('/tmp/SRASS.s.p', redefinition_k6_domain_1)).
% 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(35, axiom,![X1]:![X2]:![X3]:~(((r2_hidden(X1,X2)&m1_subset_1(X2,k1_zfmisc_1(X3)))&v1_xboole_0(X3))),file('/tmp/SRASS.s.p', t5_subset)).
% fof(41, axiom,![X1]:(l3_lattices(X1)=>(v3_lattices(k1_lattice2(X1))&l3_lattices(k1_lattice2(X1)))),file('/tmp/SRASS.s.p', dt_k1_lattice2)).
% fof(44, axiom,![X1]:![X2]:(m1_subset_1(X1,X2)=>(v1_xboole_0(X2)|r2_hidden(X1,X2))),file('/tmp/SRASS.s.p', t2_subset)).
% fof(60, 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(91, conjecture,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m1_subset_1(X2,u1_struct_0(X1))=>(m2_filter_2(k6_domain_1(u1_struct_0(X1),X2),X1)=>v13_lattices(X1)))),file('/tmp/SRASS.s.p', t27_filter_2)).
% fof(92, negated_conjecture,~(![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m1_subset_1(X2,u1_struct_0(X1))=>(m2_filter_2(k6_domain_1(u1_struct_0(X1),X2),X1)=>v13_lattices(X1))))),inference(assume_negation,[status(cth)],[91])).
% fof(94, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m1_subset_1(X2,u1_struct_0(X1))=>(m1_filter_0(k6_domain_1(u1_struct_0(X1),X2),X1)=>v14_lattices(X1)))),inference(fof_simplification,[status(thm)],[4,theory(equality)])).
% fof(97, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>?[X2]:m1_filter_2(X2,X1)),inference(fof_simplification,[status(thm)],[7,theory(equality)])).
% fof(99, 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)],[9,theory(equality)])).
% fof(100, plain,![X1]:![X2]:((((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))&m1_subset_1(X2,u1_struct_0(X1)))=>m1_subset_1(k5_filter_2(X1,X2),u1_struct_0(k1_lattice2(X1)))),inference(fof_simplification,[status(thm)],[10,theory(equality)])).
% fof(102, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m2_filter_2(X2,X1)<=>m1_filter_2(X2,k1_lattice2(X1)))),inference(fof_simplification,[status(thm)],[12,theory(equality)])).
% fof(103, 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)],[13,theory(equality)])).
% fof(104, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m1_filter_0(X2,X1)=>(~(v1_xboole_0(X2))&m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))))),inference(fof_simplification,[status(thm)],[14,theory(equality)])).
% fof(110, 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)],[20,theory(equality)])).
% fof(117, plain,![X1]:![X2]:((~(v1_xboole_0(X1))&m1_subset_1(X2,X1))=>k6_domain_1(X1,X2)=k1_tarski(X2)),inference(fof_simplification,[status(thm)],[31,theory(equality)])).
% fof(118, 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(127, 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)],[60,theory(equality)])).
% fof(137, negated_conjecture,~(![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m1_subset_1(X2,u1_struct_0(X1))=>(m2_filter_2(k6_domain_1(u1_struct_0(X1),X2),X1)=>v13_lattices(X1))))),inference(fof_simplification,[status(thm)],[92,theory(equality)])).
% fof(141, plain,![X3]:?[X4]:m1_subset_1(X4,X3),inference(variable_rename,[status(thm)],[2])).
% fof(142, plain,![X3]:m1_subset_1(esk2_1(X3),X3),inference(skolemize,[status(esa)],[141])).
% cnf(143,plain,(m1_subset_1(esk2_1(X1),X1)),inference(split_conjunct,[status(thm)],[142])).
% fof(148, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|![X2]:(~(m1_subset_1(X2,u1_struct_0(X1)))|(~(m1_filter_0(k6_domain_1(u1_struct_0(X1),X2),X1))|v14_lattices(X1)))),inference(fof_nnf,[status(thm)],[94])).
% fof(149, plain,![X3]:(((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))|![X4]:(~(m1_subset_1(X4,u1_struct_0(X3)))|(~(m1_filter_0(k6_domain_1(u1_struct_0(X3),X4),X3))|v14_lattices(X3)))),inference(variable_rename,[status(thm)],[148])).
% fof(150, plain,![X3]:![X4]:((~(m1_subset_1(X4,u1_struct_0(X3)))|(~(m1_filter_0(k6_domain_1(u1_struct_0(X3),X4),X3))|v14_lattices(X3)))|((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))),inference(shift_quantors,[status(thm)],[149])).
% cnf(151,plain,(v3_struct_0(X1)|v14_lattices(X1)|~l3_lattices(X1)|~v10_lattices(X1)|~m1_filter_0(k6_domain_1(u1_struct_0(X1),X2),X1)|~m1_subset_1(X2,u1_struct_0(X1))),inference(split_conjunct,[status(thm)],[150])).
% fof(160, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|?[X2]:m1_filter_2(X2,X1)),inference(fof_nnf,[status(thm)],[97])).
% fof(161, plain,![X3]:(((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))|?[X4]:m1_filter_2(X4,X3)),inference(variable_rename,[status(thm)],[160])).
% fof(162, plain,![X3]:(((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))|m1_filter_2(esk6_1(X3),X3)),inference(skolemize,[status(esa)],[161])).
% cnf(163,plain,(m1_filter_2(esk6_1(X1),X1)|v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[162])).
% fof(168, 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)],[99])).
% fof(169, 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)],[168])).
% fof(170, 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)],[169])).
% cnf(171,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)],[170])).
% fof(172, plain,![X1]:![X2]:((((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|~(m1_subset_1(X2,u1_struct_0(X1))))|m1_subset_1(k5_filter_2(X1,X2),u1_struct_0(k1_lattice2(X1)))),inference(fof_nnf,[status(thm)],[100])).
% fof(173, 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)],[172])).
% cnf(174,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)],[173])).
% fof(181, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|![X2]:((~(m2_filter_2(X2,X1))|m1_filter_2(X2,k1_lattice2(X1)))&(~(m1_filter_2(X2,k1_lattice2(X1)))|m2_filter_2(X2,X1)))),inference(fof_nnf,[status(thm)],[102])).
% fof(182, plain,![X3]:(((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))|![X4]:((~(m2_filter_2(X4,X3))|m1_filter_2(X4,k1_lattice2(X3)))&(~(m1_filter_2(X4,k1_lattice2(X3)))|m2_filter_2(X4,X3)))),inference(variable_rename,[status(thm)],[181])).
% fof(183, plain,![X3]:![X4]:(((~(m2_filter_2(X4,X3))|m1_filter_2(X4,k1_lattice2(X3)))&(~(m1_filter_2(X4,k1_lattice2(X3)))|m2_filter_2(X4,X3)))|((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))),inference(shift_quantors,[status(thm)],[182])).
% fof(184, plain,![X3]:![X4]:(((~(m2_filter_2(X4,X3))|m1_filter_2(X4,k1_lattice2(X3)))|((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3))))&((~(m1_filter_2(X4,k1_lattice2(X3)))|m2_filter_2(X4,X3))|((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3))))),inference(distribute,[status(thm)],[183])).
% cnf(186,plain,(v3_struct_0(X1)|m1_filter_2(X2,k1_lattice2(X1))|~l3_lattices(X1)|~v10_lattices(X1)|~m2_filter_2(X2,X1)),inference(split_conjunct,[status(thm)],[184])).
% fof(187, 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)],[103])).
% fof(188, 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)],[187])).
% fof(189, 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)],[188])).
% cnf(190,plain,(v3_struct_0(X1)|v13_lattices(X1)|~l3_lattices(X1)|~v10_lattices(X1)|~v14_lattices(k1_lattice2(X1))),inference(split_conjunct,[status(thm)],[189])).
% fof(192, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|![X2]:(~(m1_filter_0(X2,X1))|(~(v1_xboole_0(X2))&m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))))),inference(fof_nnf,[status(thm)],[104])).
% fof(193, plain,![X3]:(((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))|![X4]:(~(m1_filter_0(X4,X3))|(~(v1_xboole_0(X4))&m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3)))))),inference(variable_rename,[status(thm)],[192])).
% fof(194, plain,![X3]:![X4]:((~(m1_filter_0(X4,X3))|(~(v1_xboole_0(X4))&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)],[193])).
% fof(195, plain,![X3]:![X4]:(((~(v1_xboole_0(X4))|~(m1_filter_0(X4,X3)))|((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3))))&((m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3)))|~(m1_filter_0(X4,X3)))|((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3))))),inference(distribute,[status(thm)],[194])).
% cnf(196,plain,(v3_struct_0(X1)|m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|~l3_lattices(X1)|~v10_lattices(X1)|~m1_filter_0(X2,X1)),inference(split_conjunct,[status(thm)],[195])).
% cnf(197,plain,(v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)|~m1_filter_0(X2,X1)|~v1_xboole_0(X2)),inference(split_conjunct,[status(thm)],[195])).
% fof(223, 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)],[110])).
% fof(224, 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)],[223])).
% fof(225, 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)],[224])).
% fof(226, 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)],[225])).
% cnf(228,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)],[226])).
% fof(266, plain,![X1]:![X2]:((v1_xboole_0(X1)|~(m1_subset_1(X2,X1)))|k6_domain_1(X1,X2)=k1_tarski(X2)),inference(fof_nnf,[status(thm)],[117])).
% fof(267, plain,![X3]:![X4]:((v1_xboole_0(X3)|~(m1_subset_1(X4,X3)))|k6_domain_1(X3,X4)=k1_tarski(X4)),inference(variable_rename,[status(thm)],[266])).
% cnf(268,plain,(k6_domain_1(X1,X2)=k1_tarski(X2)|v1_xboole_0(X1)|~m1_subset_1(X2,X1)),inference(split_conjunct,[status(thm)],[267])).
% fof(269, 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)],[118])).
% fof(270, 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)],[269])).
% fof(271, 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)],[270])).
% cnf(273,plain,(v3_struct_0(X1)|~l3_lattices(X1)|~v3_struct_0(k1_lattice2(X1))),inference(split_conjunct,[status(thm)],[271])).
% fof(284, plain,![X1]:![X2]:![X3]:((~(r2_hidden(X1,X2))|~(m1_subset_1(X2,k1_zfmisc_1(X3))))|~(v1_xboole_0(X3))),inference(fof_nnf,[status(thm)],[35])).
% fof(285, plain,![X4]:![X5]:![X6]:((~(r2_hidden(X4,X5))|~(m1_subset_1(X5,k1_zfmisc_1(X6))))|~(v1_xboole_0(X6))),inference(variable_rename,[status(thm)],[284])).
% cnf(286,plain,(~v1_xboole_0(X1)|~m1_subset_1(X2,k1_zfmisc_1(X1))|~r2_hidden(X3,X2)),inference(split_conjunct,[status(thm)],[285])).
% fof(301, plain,![X1]:(~(l3_lattices(X1))|(v3_lattices(k1_lattice2(X1))&l3_lattices(k1_lattice2(X1)))),inference(fof_nnf,[status(thm)],[41])).
% fof(302, plain,![X2]:(~(l3_lattices(X2))|(v3_lattices(k1_lattice2(X2))&l3_lattices(k1_lattice2(X2)))),inference(variable_rename,[status(thm)],[301])).
% fof(303, plain,![X2]:((v3_lattices(k1_lattice2(X2))|~(l3_lattices(X2)))&(l3_lattices(k1_lattice2(X2))|~(l3_lattices(X2)))),inference(distribute,[status(thm)],[302])).
% cnf(304,plain,(l3_lattices(k1_lattice2(X1))|~l3_lattices(X1)),inference(split_conjunct,[status(thm)],[303])).
% fof(313, plain,![X1]:![X2]:(~(m1_subset_1(X1,X2))|(v1_xboole_0(X2)|r2_hidden(X1,X2))),inference(fof_nnf,[status(thm)],[44])).
% fof(314, plain,![X3]:![X4]:(~(m1_subset_1(X3,X4))|(v1_xboole_0(X4)|r2_hidden(X3,X4))),inference(variable_rename,[status(thm)],[313])).
% cnf(315,plain,(r2_hidden(X1,X2)|v1_xboole_0(X2)|~m1_subset_1(X1,X2)),inference(split_conjunct,[status(thm)],[314])).
% fof(394, 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)],[127])).
% fof(395, 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)],[394])).
% fof(396, 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)],[395])).
% cnf(397,plain,(v3_struct_0(X1)|v10_lattices(k1_lattice2(X1))|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[396])).
% fof(522, negated_conjecture,?[X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))&?[X2]:(m1_subset_1(X2,u1_struct_0(X1))&(m2_filter_2(k6_domain_1(u1_struct_0(X1),X2),X1)&~(v13_lattices(X1))))),inference(fof_nnf,[status(thm)],[137])).
% fof(523, negated_conjecture,?[X3]:(((~(v3_struct_0(X3))&v10_lattices(X3))&l3_lattices(X3))&?[X4]:(m1_subset_1(X4,u1_struct_0(X3))&(m2_filter_2(k6_domain_1(u1_struct_0(X3),X4),X3)&~(v13_lattices(X3))))),inference(variable_rename,[status(thm)],[522])).
% fof(524, negated_conjecture,(((~(v3_struct_0(esk28_0))&v10_lattices(esk28_0))&l3_lattices(esk28_0))&(m1_subset_1(esk29_0,u1_struct_0(esk28_0))&(m2_filter_2(k6_domain_1(u1_struct_0(esk28_0),esk29_0),esk28_0)&~(v13_lattices(esk28_0))))),inference(skolemize,[status(esa)],[523])).
% cnf(525,negated_conjecture,(~v13_lattices(esk28_0)),inference(split_conjunct,[status(thm)],[524])).
% cnf(526,negated_conjecture,(m2_filter_2(k6_domain_1(u1_struct_0(esk28_0),esk29_0),esk28_0)),inference(split_conjunct,[status(thm)],[524])).
% cnf(527,negated_conjecture,(m1_subset_1(esk29_0,u1_struct_0(esk28_0))),inference(split_conjunct,[status(thm)],[524])).
% cnf(528,negated_conjecture,(l3_lattices(esk28_0)),inference(split_conjunct,[status(thm)],[524])).
% cnf(529,negated_conjecture,(v10_lattices(esk28_0)),inference(split_conjunct,[status(thm)],[524])).
% cnf(530,negated_conjecture,(~v3_struct_0(esk28_0)),inference(split_conjunct,[status(thm)],[524])).
% cnf(745,negated_conjecture,(m2_filter_2(k1_tarski(esk29_0),esk28_0)|v1_xboole_0(u1_struct_0(esk28_0))|~m1_subset_1(esk29_0,u1_struct_0(esk28_0))),inference(spm,[status(thm)],[526,268,theory(equality)])).
% cnf(747,negated_conjecture,(m2_filter_2(k1_tarski(esk29_0),esk28_0)|v1_xboole_0(u1_struct_0(esk28_0))|$false),inference(rw,[status(thm)],[745,527,theory(equality)])).
% cnf(748,negated_conjecture,(m2_filter_2(k1_tarski(esk29_0),esk28_0)|v1_xboole_0(u1_struct_0(esk28_0))),inference(cn,[status(thm)],[747,theory(equality)])).
% cnf(798,plain,(m1_filter_0(esk6_1(X1),X1)|v3_struct_0(X1)|~v10_lattices(X1)|~l3_lattices(X1)),inference(spm,[status(thm)],[228,163,theory(equality)])).
% cnf(803,negated_conjecture,(k5_filter_2(esk28_0,esk29_0)=esk29_0|v3_struct_0(esk28_0)|~v10_lattices(esk28_0)|~l3_lattices(esk28_0)),inference(spm,[status(thm)],[171,527,theory(equality)])).
% cnf(805,negated_conjecture,(k5_filter_2(esk28_0,esk29_0)=esk29_0|v3_struct_0(esk28_0)|$false|~l3_lattices(esk28_0)),inference(rw,[status(thm)],[803,529,theory(equality)])).
% cnf(806,negated_conjecture,(k5_filter_2(esk28_0,esk29_0)=esk29_0|v3_struct_0(esk28_0)|$false|$false),inference(rw,[status(thm)],[805,528,theory(equality)])).
% cnf(807,negated_conjecture,(k5_filter_2(esk28_0,esk29_0)=esk29_0|v3_struct_0(esk28_0)),inference(cn,[status(thm)],[806,theory(equality)])).
% cnf(808,negated_conjecture,(k5_filter_2(esk28_0,esk29_0)=esk29_0),inference(sr,[status(thm)],[807,530,theory(equality)])).
% cnf(817,plain,(m1_filter_0(X1,k1_lattice2(X2))|v3_struct_0(k1_lattice2(X2))|v3_struct_0(X2)|~v10_lattices(k1_lattice2(X2))|~l3_lattices(k1_lattice2(X2))|~m2_filter_2(X1,X2)|~v10_lattices(X2)|~l3_lattices(X2)),inference(spm,[status(thm)],[228,186,theory(equality)])).
% cnf(847,plain,(v3_struct_0(X3)|~r2_hidden(X1,X2)|~v1_xboole_0(u1_struct_0(X3))|~m1_filter_0(X2,X3)|~v10_lattices(X3)|~l3_lattices(X3)),inference(spm,[status(thm)],[286,196,theory(equality)])).
% cnf(866,negated_conjecture,(v3_struct_0(esk28_0)|m1_subset_1(esk29_0,u1_struct_0(k1_lattice2(esk28_0)))|~v10_lattices(esk28_0)|~m1_subset_1(esk29_0,u1_struct_0(esk28_0))|~l3_lattices(esk28_0)),inference(spm,[status(thm)],[174,808,theory(equality)])).
% cnf(867,negated_conjecture,(v3_struct_0(esk28_0)|m1_subset_1(esk29_0,u1_struct_0(k1_lattice2(esk28_0)))|$false|~m1_subset_1(esk29_0,u1_struct_0(esk28_0))|~l3_lattices(esk28_0)),inference(rw,[status(thm)],[866,529,theory(equality)])).
% cnf(868,negated_conjecture,(v3_struct_0(esk28_0)|m1_subset_1(esk29_0,u1_struct_0(k1_lattice2(esk28_0)))|$false|$false|~l3_lattices(esk28_0)),inference(rw,[status(thm)],[867,527,theory(equality)])).
% cnf(869,negated_conjecture,(v3_struct_0(esk28_0)|m1_subset_1(esk29_0,u1_struct_0(k1_lattice2(esk28_0)))|$false|$false|$false),inference(rw,[status(thm)],[868,528,theory(equality)])).
% cnf(870,negated_conjecture,(v3_struct_0(esk28_0)|m1_subset_1(esk29_0,u1_struct_0(k1_lattice2(esk28_0)))),inference(cn,[status(thm)],[869,theory(equality)])).
% cnf(871,negated_conjecture,(m1_subset_1(esk29_0,u1_struct_0(k1_lattice2(esk28_0)))),inference(sr,[status(thm)],[870,530,theory(equality)])).
% cnf(921,plain,(v14_lattices(X1)|v3_struct_0(X1)|v1_xboole_0(u1_struct_0(X1))|~m1_filter_0(k1_tarski(X2),X1)|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~l3_lattices(X1)),inference(spm,[status(thm)],[151,268,theory(equality)])).
% cnf(1023,plain,(v3_struct_0(X1)|v1_xboole_0(X3)|~v1_xboole_0(u1_struct_0(X1))|~m1_filter_0(X3,X1)|~v10_lattices(X1)|~l3_lattices(X1)|~m1_subset_1(X2,X3)),inference(spm,[status(thm)],[847,315,theory(equality)])).
% cnf(1334,plain,(m1_filter_0(X1,k1_lattice2(X2))|v3_struct_0(k1_lattice2(X2))|v3_struct_0(X2)|~m2_filter_2(X1,X2)|~v10_lattices(k1_lattice2(X2))|~v10_lattices(X2)|~l3_lattices(X2)),inference(csr,[status(thm)],[817,304])).
% cnf(1335,plain,(m1_filter_0(X1,k1_lattice2(X2))|v3_struct_0(k1_lattice2(X2))|v3_struct_0(X2)|~m2_filter_2(X1,X2)|~v10_lattices(X2)|~l3_lattices(X2)),inference(csr,[status(thm)],[1334,397])).
% cnf(1336,plain,(m1_filter_0(X1,k1_lattice2(X2))|v3_struct_0(X2)|~m2_filter_2(X1,X2)|~v10_lattices(X2)|~l3_lattices(X2)),inference(csr,[status(thm)],[1335,273])).
% cnf(1340,plain,(v3_struct_0(X1)|~v1_xboole_0(u1_struct_0(X1))|~m1_filter_0(X3,X1)|~v10_lattices(X1)|~m1_subset_1(X2,X3)|~l3_lattices(X1)),inference(csr,[status(thm)],[1023,197])).
% cnf(1341,plain,(v3_struct_0(X1)|~v1_xboole_0(u1_struct_0(X1))|~v10_lattices(X1)|~m1_subset_1(X2,esk6_1(X1))|~l3_lattices(X1)),inference(spm,[status(thm)],[1340,798,theory(equality)])).
% cnf(1352,plain,(v3_struct_0(X1)|~v1_xboole_0(u1_struct_0(X1))|~v10_lattices(X1)|~l3_lattices(X1)),inference(spm,[status(thm)],[1341,143,theory(equality)])).
% cnf(1873,plain,(v14_lattices(X1)|v3_struct_0(X1)|~m1_filter_0(k1_tarski(X2),X1)|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~l3_lattices(X1)),inference(csr,[status(thm)],[921,1352])).
% cnf(1874,plain,(v14_lattices(k1_lattice2(X1))|v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|~v10_lattices(k1_lattice2(X1))|~m1_subset_1(X2,u1_struct_0(k1_lattice2(X1)))|~l3_lattices(k1_lattice2(X1))|~m2_filter_2(k1_tarski(X2),X1)|~v10_lattices(X1)|~l3_lattices(X1)),inference(spm,[status(thm)],[1873,1336,theory(equality)])).
% cnf(27145,plain,(v14_lattices(k1_lattice2(X1))|v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|~m2_filter_2(k1_tarski(X2),X1)|~v10_lattices(k1_lattice2(X1))|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(k1_lattice2(X1)))|~l3_lattices(X1)),inference(csr,[status(thm)],[1874,304])).
% cnf(27146,plain,(v14_lattices(k1_lattice2(X1))|v3_struct_0(k1_lattice2(X1))|v3_struct_0(X1)|~m2_filter_2(k1_tarski(X2),X1)|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(k1_lattice2(X1)))|~l3_lattices(X1)),inference(csr,[status(thm)],[27145,397])).
% cnf(27147,plain,(v14_lattices(k1_lattice2(X1))|v3_struct_0(X1)|~m2_filter_2(k1_tarski(X2),X1)|~v10_lattices(X1)|~m1_subset_1(X2,u1_struct_0(k1_lattice2(X1)))|~l3_lattices(X1)),inference(csr,[status(thm)],[27146,273])).
% cnf(27148,negated_conjecture,(v14_lattices(k1_lattice2(esk28_0))|v3_struct_0(esk28_0)|~m2_filter_2(k1_tarski(esk29_0),esk28_0)|~v10_lattices(esk28_0)|~l3_lattices(esk28_0)),inference(spm,[status(thm)],[27147,871,theory(equality)])).
% cnf(27330,negated_conjecture,(v14_lattices(k1_lattice2(esk28_0))|v3_struct_0(esk28_0)|~m2_filter_2(k1_tarski(esk29_0),esk28_0)|$false|~l3_lattices(esk28_0)),inference(rw,[status(thm)],[27148,529,theory(equality)])).
% cnf(27331,negated_conjecture,(v14_lattices(k1_lattice2(esk28_0))|v3_struct_0(esk28_0)|~m2_filter_2(k1_tarski(esk29_0),esk28_0)|$false|$false),inference(rw,[status(thm)],[27330,528,theory(equality)])).
% cnf(27332,negated_conjecture,(v14_lattices(k1_lattice2(esk28_0))|v3_struct_0(esk28_0)|~m2_filter_2(k1_tarski(esk29_0),esk28_0)),inference(cn,[status(thm)],[27331,theory(equality)])).
% cnf(27333,negated_conjecture,(v14_lattices(k1_lattice2(esk28_0))|~m2_filter_2(k1_tarski(esk29_0),esk28_0)),inference(sr,[status(thm)],[27332,530,theory(equality)])).
% cnf(27470,negated_conjecture,(v14_lattices(k1_lattice2(esk28_0))|v1_xboole_0(u1_struct_0(esk28_0))),inference(spm,[status(thm)],[27333,748,theory(equality)])).
% cnf(27484,negated_conjecture,(v3_struct_0(esk28_0)|v14_lattices(k1_lattice2(esk28_0))|~v10_lattices(esk28_0)|~l3_lattices(esk28_0)),inference(spm,[status(thm)],[1352,27470,theory(equality)])).
% cnf(27486,negated_conjecture,(v3_struct_0(esk28_0)|v14_lattices(k1_lattice2(esk28_0))|$false|~l3_lattices(esk28_0)),inference(rw,[status(thm)],[27484,529,theory(equality)])).
% cnf(27487,negated_conjecture,(v3_struct_0(esk28_0)|v14_lattices(k1_lattice2(esk28_0))|$false|$false),inference(rw,[status(thm)],[27486,528,theory(equality)])).
% cnf(27488,negated_conjecture,(v3_struct_0(esk28_0)|v14_lattices(k1_lattice2(esk28_0))),inference(cn,[status(thm)],[27487,theory(equality)])).
% cnf(27489,negated_conjecture,(v14_lattices(k1_lattice2(esk28_0))),inference(sr,[status(thm)],[27488,530,theory(equality)])).
% cnf(27490,negated_conjecture,(v13_lattices(esk28_0)|v3_struct_0(esk28_0)|~v10_lattices(esk28_0)|~l3_lattices(esk28_0)),inference(spm,[status(thm)],[190,27489,theory(equality)])).
% cnf(27493,negated_conjecture,(v13_lattices(esk28_0)|v3_struct_0(esk28_0)|$false|~l3_lattices(esk28_0)),inference(rw,[status(thm)],[27490,529,theory(equality)])).
% cnf(27494,negated_conjecture,(v13_lattices(esk28_0)|v3_struct_0(esk28_0)|$false|$false),inference(rw,[status(thm)],[27493,528,theory(equality)])).
% cnf(27495,negated_conjecture,(v13_lattices(esk28_0)|v3_struct_0(esk28_0)),inference(cn,[status(thm)],[27494,theory(equality)])).
% cnf(27496,negated_conjecture,(v3_struct_0(esk28_0)),inference(sr,[status(thm)],[27495,525,theory(equality)])).
% cnf(27497,negated_conjecture,($false),inference(sr,[status(thm)],[27496,530,theory(equality)])).
% cnf(27498,negated_conjecture,($false),27497,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2703
% # ...of these trivial : 25
% # ...subsumed : 1315
% # ...remaining for further processing: 1363
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 51
% # Backward-rewritten : 34
% # Generated clauses : 19285
% # ...of the previous two non-trivial : 18195
% # Contextual simplify-reflections : 956
% # Paramodulations : 19267
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 1272
% # Positive orientable unit clauses: 187
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 23
% # Non-unit-clauses : 1062
% # Current number of unprocessed clauses: 15211
% # ...number of literals in the above : 70857
% # Clause-clause subsumption calls (NU) : 135440
% # Rec. Clause-clause subsumption calls : 70423
% # Unit Clause-clause subsumption calls : 3844
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 2081
% # Indexed BW rewrite successes : 20
% # Backwards rewriting index: 766 leaves, 2.49+/-6.995 terms/leaf
% # Paramod-from index: 267 leaves, 2.34+/-6.142 terms/leaf
% # Paramod-into index: 680 leaves, 2.45+/-7.034 terms/leaf
% # -------------------------------------------------
% # User time : 1.030 s
% # System time : 0.033 s
% # Total time : 1.063 s
% # Maximum resident set size: 0 pages
% PrfWatch: 1.48 CPU 1.56 WC
% FINAL PrfWatch: 1.48 CPU 1.56 WC
% SZS output end Solution for /tmp/SystemOnTPTP18284/LAT303+1.tptp
%
%------------------------------------------------------------------------------