%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LAT288+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 : art05.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:27:20 EST 2010
% Result : Theorem 1.40s
% Output : Solution 1.40s
% 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/SystemOnTPTP19688/LAT288+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP19688/LAT288+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP19688/LAT288+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 19784
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.022 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(6, axiom,![X1]:(((((~(v3_struct_0(X1))&v10_lattices(X1))&v17_lattices(X1))&~(v3_realset2(X1)))&l3_lattices(X1))=>k7_lopclset(X1)=a_1_1_lopclset(X1)),file('/tmp/SRASS.s.p', d5_lopclset)).
% fof(9, axiom,![X1]:![X2]:![X3]:((((((~(v3_struct_0(X2))&v10_lattices(X2))&v17_lattices(X2))&~(v3_realset2(X2)))&l3_lattices(X2))&m1_subset_1(X3,u1_struct_0(X2)))=>(r2_hidden(X1,a_2_0_lopclset(X2,X3))<=>?[X4]:(((m1_filter_0(X4,X2)&X1=X4)&v1_filter_0(X4,X2))&r2_hidden(X3,X4)))),file('/tmp/SRASS.s.p', fraenkel_a_2_0_lopclset)).
% fof(11, axiom,![X1]:![X2]:(r1_tarski(X1,X2)<=>![X3]:(r2_hidden(X3,X1)=>r2_hidden(X3,X2))),file('/tmp/SRASS.s.p', d3_tarski)).
% fof(17, axiom,![X1]:![X2]:(((((~(v3_struct_0(X2))&v10_lattices(X2))&v17_lattices(X2))&~(v3_realset2(X2)))&l3_lattices(X2))=>(r2_hidden(X1,a_1_1_lopclset(X2))<=>?[X3]:((m1_filter_0(X3,X2)&X1=X3)&v1_filter_0(X3,X2)))),file('/tmp/SRASS.s.p', fraenkel_a_1_1_lopclset)).
% fof(69, conjecture,![X1]:(((((~(v3_struct_0(X1))&v10_lattices(X1))&v17_lattices(X1))&~(v3_realset2(X1)))&l3_lattices(X1))=>![X2]:(m1_subset_1(X2,u1_struct_0(X1))=>r1_tarski(a_2_0_lopclset(X1,X2),k7_lopclset(X1)))),file('/tmp/SRASS.s.p', t19_lopclset)).
% fof(70, negated_conjecture,~(![X1]:(((((~(v3_struct_0(X1))&v10_lattices(X1))&v17_lattices(X1))&~(v3_realset2(X1)))&l3_lattices(X1))=>![X2]:(m1_subset_1(X2,u1_struct_0(X1))=>r1_tarski(a_2_0_lopclset(X1,X2),k7_lopclset(X1))))),inference(assume_negation,[status(cth)],[69])).
% fof(73, plain,![X1]:(((((~(v3_struct_0(X1))&v10_lattices(X1))&v17_lattices(X1))&~(v3_realset2(X1)))&l3_lattices(X1))=>k7_lopclset(X1)=a_1_1_lopclset(X1)),inference(fof_simplification,[status(thm)],[6,theory(equality)])).
% fof(75, plain,![X1]:![X2]:![X3]:((((((~(v3_struct_0(X2))&v10_lattices(X2))&v17_lattices(X2))&~(v3_realset2(X2)))&l3_lattices(X2))&m1_subset_1(X3,u1_struct_0(X2)))=>(r2_hidden(X1,a_2_0_lopclset(X2,X3))<=>?[X4]:(((m1_filter_0(X4,X2)&X1=X4)&v1_filter_0(X4,X2))&r2_hidden(X3,X4)))),inference(fof_simplification,[status(thm)],[9,theory(equality)])).
% fof(80, plain,![X1]:![X2]:(((((~(v3_struct_0(X2))&v10_lattices(X2))&v17_lattices(X2))&~(v3_realset2(X2)))&l3_lattices(X2))=>(r2_hidden(X1,a_1_1_lopclset(X2))<=>?[X3]:((m1_filter_0(X3,X2)&X1=X3)&v1_filter_0(X3,X2)))),inference(fof_simplification,[status(thm)],[17,theory(equality)])).
% fof(95, negated_conjecture,~(![X1]:(((((~(v3_struct_0(X1))&v10_lattices(X1))&v17_lattices(X1))&~(v3_realset2(X1)))&l3_lattices(X1))=>![X2]:(m1_subset_1(X2,u1_struct_0(X1))=>r1_tarski(a_2_0_lopclset(X1,X2),k7_lopclset(X1))))),inference(fof_simplification,[status(thm)],[70,theory(equality)])).
% fof(110, plain,![X1]:(((((v3_struct_0(X1)|~(v10_lattices(X1)))|~(v17_lattices(X1)))|v3_realset2(X1))|~(l3_lattices(X1)))|k7_lopclset(X1)=a_1_1_lopclset(X1)),inference(fof_nnf,[status(thm)],[73])).
% fof(111, plain,![X2]:(((((v3_struct_0(X2)|~(v10_lattices(X2)))|~(v17_lattices(X2)))|v3_realset2(X2))|~(l3_lattices(X2)))|k7_lopclset(X2)=a_1_1_lopclset(X2)),inference(variable_rename,[status(thm)],[110])).
% cnf(112,plain,(k7_lopclset(X1)=a_1_1_lopclset(X1)|v3_realset2(X1)|v3_struct_0(X1)|~l3_lattices(X1)|~v17_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[111])).
% fof(121, plain,![X1]:![X2]:![X3]:((((((v3_struct_0(X2)|~(v10_lattices(X2)))|~(v17_lattices(X2)))|v3_realset2(X2))|~(l3_lattices(X2)))|~(m1_subset_1(X3,u1_struct_0(X2))))|((~(r2_hidden(X1,a_2_0_lopclset(X2,X3)))|?[X4]:(((m1_filter_0(X4,X2)&X1=X4)&v1_filter_0(X4,X2))&r2_hidden(X3,X4)))&(![X4]:(((~(m1_filter_0(X4,X2))|~(X1=X4))|~(v1_filter_0(X4,X2)))|~(r2_hidden(X3,X4)))|r2_hidden(X1,a_2_0_lopclset(X2,X3))))),inference(fof_nnf,[status(thm)],[75])).
% fof(122, plain,![X5]:![X6]:![X7]:((((((v3_struct_0(X6)|~(v10_lattices(X6)))|~(v17_lattices(X6)))|v3_realset2(X6))|~(l3_lattices(X6)))|~(m1_subset_1(X7,u1_struct_0(X6))))|((~(r2_hidden(X5,a_2_0_lopclset(X6,X7)))|?[X8]:(((m1_filter_0(X8,X6)&X5=X8)&v1_filter_0(X8,X6))&r2_hidden(X7,X8)))&(![X9]:(((~(m1_filter_0(X9,X6))|~(X5=X9))|~(v1_filter_0(X9,X6)))|~(r2_hidden(X7,X9)))|r2_hidden(X5,a_2_0_lopclset(X6,X7))))),inference(variable_rename,[status(thm)],[121])).
% fof(123, plain,![X5]:![X6]:![X7]:((((((v3_struct_0(X6)|~(v10_lattices(X6)))|~(v17_lattices(X6)))|v3_realset2(X6))|~(l3_lattices(X6)))|~(m1_subset_1(X7,u1_struct_0(X6))))|((~(r2_hidden(X5,a_2_0_lopclset(X6,X7)))|(((m1_filter_0(esk4_3(X5,X6,X7),X6)&X5=esk4_3(X5,X6,X7))&v1_filter_0(esk4_3(X5,X6,X7),X6))&r2_hidden(X7,esk4_3(X5,X6,X7))))&(![X9]:(((~(m1_filter_0(X9,X6))|~(X5=X9))|~(v1_filter_0(X9,X6)))|~(r2_hidden(X7,X9)))|r2_hidden(X5,a_2_0_lopclset(X6,X7))))),inference(skolemize,[status(esa)],[122])).
% fof(124, plain,![X5]:![X6]:![X7]:![X9]:((((((~(m1_filter_0(X9,X6))|~(X5=X9))|~(v1_filter_0(X9,X6)))|~(r2_hidden(X7,X9)))|r2_hidden(X5,a_2_0_lopclset(X6,X7)))&(~(r2_hidden(X5,a_2_0_lopclset(X6,X7)))|(((m1_filter_0(esk4_3(X5,X6,X7),X6)&X5=esk4_3(X5,X6,X7))&v1_filter_0(esk4_3(X5,X6,X7),X6))&r2_hidden(X7,esk4_3(X5,X6,X7)))))|(((((v3_struct_0(X6)|~(v10_lattices(X6)))|~(v17_lattices(X6)))|v3_realset2(X6))|~(l3_lattices(X6)))|~(m1_subset_1(X7,u1_struct_0(X6))))),inference(shift_quantors,[status(thm)],[123])).
% fof(125, plain,![X5]:![X6]:![X7]:![X9]:((((((~(m1_filter_0(X9,X6))|~(X5=X9))|~(v1_filter_0(X9,X6)))|~(r2_hidden(X7,X9)))|r2_hidden(X5,a_2_0_lopclset(X6,X7)))|(((((v3_struct_0(X6)|~(v10_lattices(X6)))|~(v17_lattices(X6)))|v3_realset2(X6))|~(l3_lattices(X6)))|~(m1_subset_1(X7,u1_struct_0(X6)))))&(((((m1_filter_0(esk4_3(X5,X6,X7),X6)|~(r2_hidden(X5,a_2_0_lopclset(X6,X7))))|(((((v3_struct_0(X6)|~(v10_lattices(X6)))|~(v17_lattices(X6)))|v3_realset2(X6))|~(l3_lattices(X6)))|~(m1_subset_1(X7,u1_struct_0(X6)))))&((X5=esk4_3(X5,X6,X7)|~(r2_hidden(X5,a_2_0_lopclset(X6,X7))))|(((((v3_struct_0(X6)|~(v10_lattices(X6)))|~(v17_lattices(X6)))|v3_realset2(X6))|~(l3_lattices(X6)))|~(m1_subset_1(X7,u1_struct_0(X6))))))&((v1_filter_0(esk4_3(X5,X6,X7),X6)|~(r2_hidden(X5,a_2_0_lopclset(X6,X7))))|(((((v3_struct_0(X6)|~(v10_lattices(X6)))|~(v17_lattices(X6)))|v3_realset2(X6))|~(l3_lattices(X6)))|~(m1_subset_1(X7,u1_struct_0(X6))))))&((r2_hidden(X7,esk4_3(X5,X6,X7))|~(r2_hidden(X5,a_2_0_lopclset(X6,X7))))|(((((v3_struct_0(X6)|~(v10_lattices(X6)))|~(v17_lattices(X6)))|v3_realset2(X6))|~(l3_lattices(X6)))|~(m1_subset_1(X7,u1_struct_0(X6))))))),inference(distribute,[status(thm)],[124])).
% cnf(127,plain,(v3_realset2(X2)|v3_struct_0(X2)|v1_filter_0(esk4_3(X3,X2,X1),X2)|~m1_subset_1(X1,u1_struct_0(X2))|~l3_lattices(X2)|~v17_lattices(X2)|~v10_lattices(X2)|~r2_hidden(X3,a_2_0_lopclset(X2,X1))),inference(split_conjunct,[status(thm)],[125])).
% cnf(128,plain,(v3_realset2(X2)|v3_struct_0(X2)|X3=esk4_3(X3,X2,X1)|~m1_subset_1(X1,u1_struct_0(X2))|~l3_lattices(X2)|~v17_lattices(X2)|~v10_lattices(X2)|~r2_hidden(X3,a_2_0_lopclset(X2,X1))),inference(split_conjunct,[status(thm)],[125])).
% cnf(129,plain,(v3_realset2(X2)|v3_struct_0(X2)|m1_filter_0(esk4_3(X3,X2,X1),X2)|~m1_subset_1(X1,u1_struct_0(X2))|~l3_lattices(X2)|~v17_lattices(X2)|~v10_lattices(X2)|~r2_hidden(X3,a_2_0_lopclset(X2,X1))),inference(split_conjunct,[status(thm)],[125])).
% fof(137, plain,![X1]:![X2]:((~(r1_tarski(X1,X2))|![X3]:(~(r2_hidden(X3,X1))|r2_hidden(X3,X2)))&(?[X3]:(r2_hidden(X3,X1)&~(r2_hidden(X3,X2)))|r1_tarski(X1,X2))),inference(fof_nnf,[status(thm)],[11])).
% fof(138, plain,![X4]:![X5]:((~(r1_tarski(X4,X5))|![X6]:(~(r2_hidden(X6,X4))|r2_hidden(X6,X5)))&(?[X7]:(r2_hidden(X7,X4)&~(r2_hidden(X7,X5)))|r1_tarski(X4,X5))),inference(variable_rename,[status(thm)],[137])).
% fof(139, plain,![X4]:![X5]:((~(r1_tarski(X4,X5))|![X6]:(~(r2_hidden(X6,X4))|r2_hidden(X6,X5)))&((r2_hidden(esk5_2(X4,X5),X4)&~(r2_hidden(esk5_2(X4,X5),X5)))|r1_tarski(X4,X5))),inference(skolemize,[status(esa)],[138])).
% fof(140, plain,![X4]:![X5]:![X6]:(((~(r2_hidden(X6,X4))|r2_hidden(X6,X5))|~(r1_tarski(X4,X5)))&((r2_hidden(esk5_2(X4,X5),X4)&~(r2_hidden(esk5_2(X4,X5),X5)))|r1_tarski(X4,X5))),inference(shift_quantors,[status(thm)],[139])).
% fof(141, plain,![X4]:![X5]:![X6]:(((~(r2_hidden(X6,X4))|r2_hidden(X6,X5))|~(r1_tarski(X4,X5)))&((r2_hidden(esk5_2(X4,X5),X4)|r1_tarski(X4,X5))&(~(r2_hidden(esk5_2(X4,X5),X5))|r1_tarski(X4,X5)))),inference(distribute,[status(thm)],[140])).
% cnf(142,plain,(r1_tarski(X1,X2)|~r2_hidden(esk5_2(X1,X2),X2)),inference(split_conjunct,[status(thm)],[141])).
% cnf(143,plain,(r1_tarski(X1,X2)|r2_hidden(esk5_2(X1,X2),X1)),inference(split_conjunct,[status(thm)],[141])).
% fof(166, plain,![X1]:![X2]:(((((v3_struct_0(X2)|~(v10_lattices(X2)))|~(v17_lattices(X2)))|v3_realset2(X2))|~(l3_lattices(X2)))|((~(r2_hidden(X1,a_1_1_lopclset(X2)))|?[X3]:((m1_filter_0(X3,X2)&X1=X3)&v1_filter_0(X3,X2)))&(![X3]:((~(m1_filter_0(X3,X2))|~(X1=X3))|~(v1_filter_0(X3,X2)))|r2_hidden(X1,a_1_1_lopclset(X2))))),inference(fof_nnf,[status(thm)],[80])).
% fof(167, plain,![X4]:![X5]:(((((v3_struct_0(X5)|~(v10_lattices(X5)))|~(v17_lattices(X5)))|v3_realset2(X5))|~(l3_lattices(X5)))|((~(r2_hidden(X4,a_1_1_lopclset(X5)))|?[X6]:((m1_filter_0(X6,X5)&X4=X6)&v1_filter_0(X6,X5)))&(![X7]:((~(m1_filter_0(X7,X5))|~(X4=X7))|~(v1_filter_0(X7,X5)))|r2_hidden(X4,a_1_1_lopclset(X5))))),inference(variable_rename,[status(thm)],[166])).
% fof(168, plain,![X4]:![X5]:(((((v3_struct_0(X5)|~(v10_lattices(X5)))|~(v17_lattices(X5)))|v3_realset2(X5))|~(l3_lattices(X5)))|((~(r2_hidden(X4,a_1_1_lopclset(X5)))|((m1_filter_0(esk9_2(X4,X5),X5)&X4=esk9_2(X4,X5))&v1_filter_0(esk9_2(X4,X5),X5)))&(![X7]:((~(m1_filter_0(X7,X5))|~(X4=X7))|~(v1_filter_0(X7,X5)))|r2_hidden(X4,a_1_1_lopclset(X5))))),inference(skolemize,[status(esa)],[167])).
% fof(169, plain,![X4]:![X5]:![X7]:(((((~(m1_filter_0(X7,X5))|~(X4=X7))|~(v1_filter_0(X7,X5)))|r2_hidden(X4,a_1_1_lopclset(X5)))&(~(r2_hidden(X4,a_1_1_lopclset(X5)))|((m1_filter_0(esk9_2(X4,X5),X5)&X4=esk9_2(X4,X5))&v1_filter_0(esk9_2(X4,X5),X5))))|((((v3_struct_0(X5)|~(v10_lattices(X5)))|~(v17_lattices(X5)))|v3_realset2(X5))|~(l3_lattices(X5)))),inference(shift_quantors,[status(thm)],[168])).
% fof(170, plain,![X4]:![X5]:![X7]:(((((~(m1_filter_0(X7,X5))|~(X4=X7))|~(v1_filter_0(X7,X5)))|r2_hidden(X4,a_1_1_lopclset(X5)))|((((v3_struct_0(X5)|~(v10_lattices(X5)))|~(v17_lattices(X5)))|v3_realset2(X5))|~(l3_lattices(X5))))&((((m1_filter_0(esk9_2(X4,X5),X5)|~(r2_hidden(X4,a_1_1_lopclset(X5))))|((((v3_struct_0(X5)|~(v10_lattices(X5)))|~(v17_lattices(X5)))|v3_realset2(X5))|~(l3_lattices(X5))))&((X4=esk9_2(X4,X5)|~(r2_hidden(X4,a_1_1_lopclset(X5))))|((((v3_struct_0(X5)|~(v10_lattices(X5)))|~(v17_lattices(X5)))|v3_realset2(X5))|~(l3_lattices(X5)))))&((v1_filter_0(esk9_2(X4,X5),X5)|~(r2_hidden(X4,a_1_1_lopclset(X5))))|((((v3_struct_0(X5)|~(v10_lattices(X5)))|~(v17_lattices(X5)))|v3_realset2(X5))|~(l3_lattices(X5)))))),inference(distribute,[status(thm)],[169])).
% cnf(174,plain,(v3_realset2(X1)|v3_struct_0(X1)|r2_hidden(X2,a_1_1_lopclset(X1))|~l3_lattices(X1)|~v17_lattices(X1)|~v10_lattices(X1)|~v1_filter_0(X3,X1)|X2!=X3|~m1_filter_0(X3,X1)),inference(split_conjunct,[status(thm)],[170])).
% fof(433, negated_conjecture,?[X1]:(((((~(v3_struct_0(X1))&v10_lattices(X1))&v17_lattices(X1))&~(v3_realset2(X1)))&l3_lattices(X1))&?[X2]:(m1_subset_1(X2,u1_struct_0(X1))&~(r1_tarski(a_2_0_lopclset(X1,X2),k7_lopclset(X1))))),inference(fof_nnf,[status(thm)],[95])).
% fof(434, negated_conjecture,?[X3]:(((((~(v3_struct_0(X3))&v10_lattices(X3))&v17_lattices(X3))&~(v3_realset2(X3)))&l3_lattices(X3))&?[X4]:(m1_subset_1(X4,u1_struct_0(X3))&~(r1_tarski(a_2_0_lopclset(X3,X4),k7_lopclset(X3))))),inference(variable_rename,[status(thm)],[433])).
% fof(435, negated_conjecture,(((((~(v3_struct_0(esk18_0))&v10_lattices(esk18_0))&v17_lattices(esk18_0))&~(v3_realset2(esk18_0)))&l3_lattices(esk18_0))&(m1_subset_1(esk19_0,u1_struct_0(esk18_0))&~(r1_tarski(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0))))),inference(skolemize,[status(esa)],[434])).
% cnf(436,negated_conjecture,(~r1_tarski(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0))),inference(split_conjunct,[status(thm)],[435])).
% cnf(437,negated_conjecture,(m1_subset_1(esk19_0,u1_struct_0(esk18_0))),inference(split_conjunct,[status(thm)],[435])).
% cnf(438,negated_conjecture,(l3_lattices(esk18_0)),inference(split_conjunct,[status(thm)],[435])).
% cnf(439,negated_conjecture,(~v3_realset2(esk18_0)),inference(split_conjunct,[status(thm)],[435])).
% cnf(440,negated_conjecture,(v17_lattices(esk18_0)),inference(split_conjunct,[status(thm)],[435])).
% cnf(441,negated_conjecture,(v10_lattices(esk18_0)),inference(split_conjunct,[status(thm)],[435])).
% cnf(442,negated_conjecture,(~v3_struct_0(esk18_0)),inference(split_conjunct,[status(thm)],[435])).
% cnf(449,plain,(r2_hidden(X1,a_1_1_lopclset(X2))|v3_realset2(X2)|v3_struct_0(X2)|~v1_filter_0(X1,X2)|~m1_filter_0(X1,X2)|~v17_lattices(X2)|~v10_lattices(X2)|~l3_lattices(X2)),inference(er,[status(thm)],[174,theory(equality)])).
% cnf(625,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),a_2_0_lopclset(esk18_0,esk19_0))),inference(spm,[status(thm)],[436,143,theory(equality)])).
% cnf(666,negated_conjecture,(v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~r1_tarski(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0))|~v17_lattices(esk18_0)|~v10_lattices(esk18_0)|~l3_lattices(esk18_0)),inference(spm,[status(thm)],[436,112,theory(equality)])).
% cnf(667,negated_conjecture,(v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~r1_tarski(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0))|$false|~v10_lattices(esk18_0)|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[666,440,theory(equality)])).
% cnf(668,negated_conjecture,(v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~r1_tarski(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0))|$false|$false|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[667,441,theory(equality)])).
% cnf(669,negated_conjecture,(v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~r1_tarski(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0))|$false|$false|$false),inference(rw,[status(thm)],[668,438,theory(equality)])).
% cnf(670,negated_conjecture,(v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~r1_tarski(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0))),inference(cn,[status(thm)],[669,theory(equality)])).
% cnf(671,negated_conjecture,(v3_struct_0(esk18_0)|~r1_tarski(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0))),inference(sr,[status(thm)],[670,439,theory(equality)])).
% cnf(672,negated_conjecture,(~r1_tarski(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0))),inference(sr,[status(thm)],[671,442,theory(equality)])).
% cnf(942,negated_conjecture,(~r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))),inference(spm,[status(thm)],[672,142,theory(equality)])).
% cnf(994,negated_conjecture,(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0)=esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~v17_lattices(esk18_0)|~v10_lattices(esk18_0)|~m1_subset_1(esk19_0,u1_struct_0(esk18_0))|~l3_lattices(esk18_0)),inference(spm,[status(thm)],[128,625,theory(equality)])).
% cnf(995,negated_conjecture,(m1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~v17_lattices(esk18_0)|~v10_lattices(esk18_0)|~m1_subset_1(esk19_0,u1_struct_0(esk18_0))|~l3_lattices(esk18_0)),inference(spm,[status(thm)],[129,625,theory(equality)])).
% cnf(996,negated_conjecture,(v1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~v17_lattices(esk18_0)|~v10_lattices(esk18_0)|~m1_subset_1(esk19_0,u1_struct_0(esk18_0))|~l3_lattices(esk18_0)),inference(spm,[status(thm)],[127,625,theory(equality)])).
% cnf(999,negated_conjecture,(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0)=esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|~v10_lattices(esk18_0)|~m1_subset_1(esk19_0,u1_struct_0(esk18_0))|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[994,440,theory(equality)])).
% cnf(1000,negated_conjecture,(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0)=esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|~m1_subset_1(esk19_0,u1_struct_0(esk18_0))|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[999,441,theory(equality)])).
% cnf(1001,negated_conjecture,(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0)=esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|$false|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[1000,437,theory(equality)])).
% cnf(1002,negated_conjecture,(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0)=esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|$false|$false),inference(rw,[status(thm)],[1001,438,theory(equality)])).
% cnf(1003,negated_conjecture,(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0)=esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)),inference(cn,[status(thm)],[1002,theory(equality)])).
% cnf(1004,negated_conjecture,(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0)=esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0))|v3_struct_0(esk18_0)),inference(sr,[status(thm)],[1003,439,theory(equality)])).
% cnf(1005,negated_conjecture,(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0)=esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0))),inference(sr,[status(thm)],[1004,442,theory(equality)])).
% cnf(1006,negated_conjecture,(m1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|~v10_lattices(esk18_0)|~m1_subset_1(esk19_0,u1_struct_0(esk18_0))|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[995,440,theory(equality)])).
% cnf(1007,negated_conjecture,(m1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|~m1_subset_1(esk19_0,u1_struct_0(esk18_0))|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[1006,441,theory(equality)])).
% cnf(1008,negated_conjecture,(m1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|$false|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[1007,437,theory(equality)])).
% cnf(1009,negated_conjecture,(m1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|$false|$false),inference(rw,[status(thm)],[1008,438,theory(equality)])).
% cnf(1010,negated_conjecture,(m1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)),inference(cn,[status(thm)],[1009,theory(equality)])).
% cnf(1011,negated_conjecture,(m1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_struct_0(esk18_0)),inference(sr,[status(thm)],[1010,439,theory(equality)])).
% cnf(1012,negated_conjecture,(m1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)),inference(sr,[status(thm)],[1011,442,theory(equality)])).
% cnf(1013,negated_conjecture,(v1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|~v10_lattices(esk18_0)|~m1_subset_1(esk19_0,u1_struct_0(esk18_0))|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[996,440,theory(equality)])).
% cnf(1014,negated_conjecture,(v1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|~m1_subset_1(esk19_0,u1_struct_0(esk18_0))|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[1013,441,theory(equality)])).
% cnf(1015,negated_conjecture,(v1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|$false|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[1014,437,theory(equality)])).
% cnf(1016,negated_conjecture,(v1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|$false|$false),inference(rw,[status(thm)],[1015,438,theory(equality)])).
% cnf(1017,negated_conjecture,(v1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_realset2(esk18_0)|v3_struct_0(esk18_0)),inference(cn,[status(thm)],[1016,theory(equality)])).
% cnf(1018,negated_conjecture,(v1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)|v3_struct_0(esk18_0)),inference(sr,[status(thm)],[1017,439,theory(equality)])).
% cnf(1019,negated_conjecture,(v1_filter_0(esk4_3(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0,esk19_0),esk18_0)),inference(sr,[status(thm)],[1018,442,theory(equality)])).
% cnf(1140,negated_conjecture,(v1_filter_0(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0)),inference(rw,[status(thm)],[1019,1005,theory(equality)])).
% cnf(1141,negated_conjecture,(m1_filter_0(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0)),inference(rw,[status(thm)],[1012,1005,theory(equality)])).
% cnf(1158,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~m1_filter_0(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0)|~v17_lattices(esk18_0)|~v10_lattices(esk18_0)|~l3_lattices(esk18_0)),inference(spm,[status(thm)],[449,1140,theory(equality)])).
% cnf(1161,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~m1_filter_0(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0)|$false|~v10_lattices(esk18_0)|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[1158,440,theory(equality)])).
% cnf(1162,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~m1_filter_0(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0)|$false|$false|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[1161,441,theory(equality)])).
% cnf(1163,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~m1_filter_0(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0)|$false|$false|$false),inference(rw,[status(thm)],[1162,438,theory(equality)])).
% cnf(1164,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~m1_filter_0(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0)),inference(cn,[status(thm)],[1163,theory(equality)])).
% cnf(1165,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_struct_0(esk18_0)|~m1_filter_0(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0)),inference(sr,[status(thm)],[1164,439,theory(equality)])).
% cnf(1166,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|~m1_filter_0(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),esk18_0)),inference(sr,[status(thm)],[1165,442,theory(equality)])).
% cnf(6123,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|$false),inference(rw,[status(thm)],[1166,1141,theory(equality)])).
% cnf(6124,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),k7_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))),inference(cn,[status(thm)],[6123,theory(equality)])).
% cnf(6147,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|~v17_lattices(esk18_0)|~v10_lattices(esk18_0)|~l3_lattices(esk18_0)),inference(spm,[status(thm)],[6124,112,theory(equality)])).
% cnf(6167,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|~v10_lattices(esk18_0)|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[6147,440,theory(equality)])).
% cnf(6168,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|~l3_lattices(esk18_0)),inference(rw,[status(thm)],[6167,441,theory(equality)])).
% cnf(6169,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)|$false|$false|$false),inference(rw,[status(thm)],[6168,438,theory(equality)])).
% cnf(6170,negated_conjecture,(r2_hidden(esk5_2(a_2_0_lopclset(esk18_0,esk19_0),a_1_1_lopclset(esk18_0)),a_1_1_lopclset(esk18_0))|v3_realset2(esk18_0)|v3_struct_0(esk18_0)),inference(cn,[status(thm)],[6169,theory(equality)])).
% cnf(6171,negated_conjecture,(v3_realset2(esk18_0)|v3_struct_0(esk18_0)),inference(sr,[status(thm)],[6170,942,theory(equality)])).
% cnf(6172,negated_conjecture,(v3_struct_0(esk18_0)),inference(sr,[status(thm)],[6171,439,theory(equality)])).
% cnf(6173,negated_conjecture,($false),inference(sr,[status(thm)],[6172,442,theory(equality)])).
% cnf(6174,negated_conjecture,($false),6173,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2034
% # ...of these trivial : 12
% # ...subsumed : 868
% # ...remaining for further processing: 1154
% # Other redundant clauses eliminated : 2
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 22
% # Backward-rewritten : 15
% # Generated clauses : 4223
% # ...of the previous two non-trivial : 4030
% # Contextual simplify-reflections : 156
% # Paramodulations : 4213
% # Factorizations : 2
% # Equation resolutions : 2
% # Current number of processed clauses: 957
% # Positive orientable unit clauses: 102
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 50
% # Non-unit-clauses : 805
% # Current number of unprocessed clauses: 2098
% # ...number of literals in the above : 8975
% # Clause-clause subsumption calls (NU) : 81313
% # Rec. Clause-clause subsumption calls : 66294
% # Unit Clause-clause subsumption calls : 908
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 21
% # Indexed BW rewrite successes : 7
% # Backwards rewriting index: 526 leaves, 1.17+/-0.556 terms/leaf
% # Paramod-from index: 259 leaves, 1.05+/-0.258 terms/leaf
% # Paramod-into index: 423 leaves, 1.15+/-0.500 terms/leaf
% # -------------------------------------------------
% # User time : 0.268 s
% # System time : 0.012 s
% # Total time : 0.280 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.43 CPU 0.52 WC
% FINAL PrfWatch: 0.43 CPU 0.52 WC
% SZS output end Solution for /tmp/SystemOnTPTP19688/LAT288+1.tptp
%
%------------------------------------------------------------------------------