%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : GRP653+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 : art07.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 07:12:14 EST 2010
% Result : Theorem 1.31s
% Output : Solution 1.31s
% 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/SystemOnTPTP10382/GRP653+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP10382/GRP653+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP10382/GRP653+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 10478
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.021 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:((((~(v3_struct_0(X1))&v3_group_1(X1))&v4_group_1(X1))&l1_group_1(X1))=>![X2]:((((~(v3_struct_0(X2))&v3_group_1(X2))&v4_group_1(X2))&l1_group_1(X2))=>![X3]:((((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&v1_group_6(X3,X1,X2))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v2_funct_1(X3)=>m3_vectsp_8(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2)))))),file('/tmp/SRASS.s.p', t36_latsubgr)).
% fof(5, axiom,![X1]:((((~(v3_struct_0(X1))&v3_group_1(X1))&v4_group_1(X1))&l1_group_1(X1))=>![X2]:((((~(v3_struct_0(X2))&v3_group_1(X2))&v4_group_1(X2))&l1_group_1(X2))=>![X3]:((((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&v1_group_6(X3,X1,X2))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>m4_vectsp_8(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2))))),file('/tmp/SRASS.s.p', t37_latsubgr)).
% fof(7, axiom,![X1]:((((~(v3_struct_0(X1))&v3_group_1(X1))&v4_group_1(X1))&l1_group_1(X1))=>(((~(v3_struct_0(k11_group_4(X1)))&v3_lattices(k11_group_4(X1)))&v10_lattices(k11_group_4(X1)))&l3_lattices(k11_group_4(X1)))),file('/tmp/SRASS.s.p', dt_k11_group_4)).
% fof(8, axiom,![X1]:![X2]:((((((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))&~(v3_struct_0(X2)))&v10_lattices(X2))&l3_lattices(X2))=>![X3]:(m3_vectsp_8(X3,X1,X2)=>((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))),file('/tmp/SRASS.s.p', dt_m3_vectsp_8)).
% fof(10, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(((~(v3_struct_0(X2))&v10_lattices(X2))&l3_lattices(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(m1_lattice4(X3,X1,X2)<=>(m4_vectsp_8(X3,X1,X2)&m3_vectsp_8(X3,X1,X2)))))),file('/tmp/SRASS.s.p', t11_vectsp_8)).
% fof(66, conjecture,![X1]:((((~(v3_struct_0(X1))&v3_group_1(X1))&v4_group_1(X1))&l1_group_1(X1))=>![X2]:((((~(v3_struct_0(X2))&v3_group_1(X2))&v4_group_1(X2))&l1_group_1(X2))=>![X3]:((((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&v1_group_6(X3,X1,X2))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v2_funct_1(X3)=>m1_lattice4(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2)))))),file('/tmp/SRASS.s.p', t38_latsubgr)).
% fof(67, negated_conjecture,~(![X1]:((((~(v3_struct_0(X1))&v3_group_1(X1))&v4_group_1(X1))&l1_group_1(X1))=>![X2]:((((~(v3_struct_0(X2))&v3_group_1(X2))&v4_group_1(X2))&l1_group_1(X2))=>![X3]:((((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&v1_group_6(X3,X1,X2))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v2_funct_1(X3)=>m1_lattice4(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2))))))),inference(assume_negation,[status(cth)],[66])).
% fof(68, plain,![X1]:((((~(v3_struct_0(X1))&v3_group_1(X1))&v4_group_1(X1))&l1_group_1(X1))=>![X2]:((((~(v3_struct_0(X2))&v3_group_1(X2))&v4_group_1(X2))&l1_group_1(X2))=>![X3]:((((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&v1_group_6(X3,X1,X2))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v2_funct_1(X3)=>m3_vectsp_8(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2)))))),inference(fof_simplification,[status(thm)],[3,theory(equality)])).
% fof(70, plain,![X1]:((((~(v3_struct_0(X1))&v3_group_1(X1))&v4_group_1(X1))&l1_group_1(X1))=>![X2]:((((~(v3_struct_0(X2))&v3_group_1(X2))&v4_group_1(X2))&l1_group_1(X2))=>![X3]:((((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&v1_group_6(X3,X1,X2))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>m4_vectsp_8(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2))))),inference(fof_simplification,[status(thm)],[5,theory(equality)])).
% fof(72, plain,![X1]:((((~(v3_struct_0(X1))&v3_group_1(X1))&v4_group_1(X1))&l1_group_1(X1))=>(((~(v3_struct_0(k11_group_4(X1)))&v3_lattices(k11_group_4(X1)))&v10_lattices(k11_group_4(X1)))&l3_lattices(k11_group_4(X1)))),inference(fof_simplification,[status(thm)],[7,theory(equality)])).
% fof(73, plain,![X1]:![X2]:((((((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))&~(v3_struct_0(X2)))&v10_lattices(X2))&l3_lattices(X2))=>![X3]:(m3_vectsp_8(X3,X1,X2)=>((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))),inference(fof_simplification,[status(thm)],[8,theory(equality)])).
% fof(75, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(((~(v3_struct_0(X2))&v10_lattices(X2))&l3_lattices(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(m1_lattice4(X3,X1,X2)<=>(m4_vectsp_8(X3,X1,X2)&m3_vectsp_8(X3,X1,X2)))))),inference(fof_simplification,[status(thm)],[10,theory(equality)])).
% fof(90, negated_conjecture,~(![X1]:((((~(v3_struct_0(X1))&v3_group_1(X1))&v4_group_1(X1))&l1_group_1(X1))=>![X2]:((((~(v3_struct_0(X2))&v3_group_1(X2))&v4_group_1(X2))&l1_group_1(X2))=>![X3]:((((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&v1_group_6(X3,X1,X2))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v2_funct_1(X3)=>m1_lattice4(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2))))))),inference(fof_simplification,[status(thm)],[67,theory(equality)])).
% fof(97, plain,![X1]:((((v3_struct_0(X1)|~(v3_group_1(X1)))|~(v4_group_1(X1)))|~(l1_group_1(X1)))|![X2]:((((v3_struct_0(X2)|~(v3_group_1(X2)))|~(v4_group_1(X2)))|~(l1_group_1(X2)))|![X3]:((((~(v1_funct_1(X3))|~(v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))))|~(v1_group_6(X3,X1,X2)))|~(m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))|(~(v2_funct_1(X3))|m3_vectsp_8(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2)))))),inference(fof_nnf,[status(thm)],[68])).
% fof(98, plain,![X4]:((((v3_struct_0(X4)|~(v3_group_1(X4)))|~(v4_group_1(X4)))|~(l1_group_1(X4)))|![X5]:((((v3_struct_0(X5)|~(v3_group_1(X5)))|~(v4_group_1(X5)))|~(l1_group_1(X5)))|![X6]:((((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(v1_group_6(X6,X4,X5)))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|(~(v2_funct_1(X6))|m3_vectsp_8(k3_latsubgr(X4,X5,X6),k11_group_4(X4),k11_group_4(X5)))))),inference(variable_rename,[status(thm)],[97])).
% fof(99, plain,![X4]:![X5]:![X6]:((((((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(v1_group_6(X6,X4,X5)))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|(~(v2_funct_1(X6))|m3_vectsp_8(k3_latsubgr(X4,X5,X6),k11_group_4(X4),k11_group_4(X5))))|(((v3_struct_0(X5)|~(v3_group_1(X5)))|~(v4_group_1(X5)))|~(l1_group_1(X5))))|(((v3_struct_0(X4)|~(v3_group_1(X4)))|~(v4_group_1(X4)))|~(l1_group_1(X4)))),inference(shift_quantors,[status(thm)],[98])).
% cnf(100,plain,(v3_struct_0(X1)|v3_struct_0(X2)|m3_vectsp_8(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2))|~l1_group_1(X1)|~v4_group_1(X1)|~v3_group_1(X1)|~l1_group_1(X2)|~v4_group_1(X2)|~v3_group_1(X2)|~v2_funct_1(X3)|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_group_6(X3,X1,X2)|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_1(X3)),inference(split_conjunct,[status(thm)],[99])).
% fof(107, plain,![X1]:((((v3_struct_0(X1)|~(v3_group_1(X1)))|~(v4_group_1(X1)))|~(l1_group_1(X1)))|![X2]:((((v3_struct_0(X2)|~(v3_group_1(X2)))|~(v4_group_1(X2)))|~(l1_group_1(X2)))|![X3]:((((~(v1_funct_1(X3))|~(v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))))|~(v1_group_6(X3,X1,X2)))|~(m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))|m4_vectsp_8(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2))))),inference(fof_nnf,[status(thm)],[70])).
% fof(108, plain,![X4]:((((v3_struct_0(X4)|~(v3_group_1(X4)))|~(v4_group_1(X4)))|~(l1_group_1(X4)))|![X5]:((((v3_struct_0(X5)|~(v3_group_1(X5)))|~(v4_group_1(X5)))|~(l1_group_1(X5)))|![X6]:((((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(v1_group_6(X6,X4,X5)))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|m4_vectsp_8(k3_latsubgr(X4,X5,X6),k11_group_4(X4),k11_group_4(X5))))),inference(variable_rename,[status(thm)],[107])).
% fof(109, plain,![X4]:![X5]:![X6]:((((((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(v1_group_6(X6,X4,X5)))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|m4_vectsp_8(k3_latsubgr(X4,X5,X6),k11_group_4(X4),k11_group_4(X5)))|(((v3_struct_0(X5)|~(v3_group_1(X5)))|~(v4_group_1(X5)))|~(l1_group_1(X5))))|(((v3_struct_0(X4)|~(v3_group_1(X4)))|~(v4_group_1(X4)))|~(l1_group_1(X4)))),inference(shift_quantors,[status(thm)],[108])).
% cnf(110,plain,(v3_struct_0(X1)|v3_struct_0(X2)|m4_vectsp_8(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2))|~l1_group_1(X1)|~v4_group_1(X1)|~v3_group_1(X1)|~l1_group_1(X2)|~v4_group_1(X2)|~v3_group_1(X2)|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_group_6(X3,X1,X2)|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_1(X3)),inference(split_conjunct,[status(thm)],[109])).
% fof(118, plain,![X1]:((((v3_struct_0(X1)|~(v3_group_1(X1)))|~(v4_group_1(X1)))|~(l1_group_1(X1)))|(((~(v3_struct_0(k11_group_4(X1)))&v3_lattices(k11_group_4(X1)))&v10_lattices(k11_group_4(X1)))&l3_lattices(k11_group_4(X1)))),inference(fof_nnf,[status(thm)],[72])).
% fof(119, plain,![X2]:((((v3_struct_0(X2)|~(v3_group_1(X2)))|~(v4_group_1(X2)))|~(l1_group_1(X2)))|(((~(v3_struct_0(k11_group_4(X2)))&v3_lattices(k11_group_4(X2)))&v10_lattices(k11_group_4(X2)))&l3_lattices(k11_group_4(X2)))),inference(variable_rename,[status(thm)],[118])).
% fof(120, plain,![X2]:((((~(v3_struct_0(k11_group_4(X2)))|(((v3_struct_0(X2)|~(v3_group_1(X2)))|~(v4_group_1(X2)))|~(l1_group_1(X2))))&(v3_lattices(k11_group_4(X2))|(((v3_struct_0(X2)|~(v3_group_1(X2)))|~(v4_group_1(X2)))|~(l1_group_1(X2)))))&(v10_lattices(k11_group_4(X2))|(((v3_struct_0(X2)|~(v3_group_1(X2)))|~(v4_group_1(X2)))|~(l1_group_1(X2)))))&(l3_lattices(k11_group_4(X2))|(((v3_struct_0(X2)|~(v3_group_1(X2)))|~(v4_group_1(X2)))|~(l1_group_1(X2))))),inference(distribute,[status(thm)],[119])).
% cnf(121,plain,(v3_struct_0(X1)|l3_lattices(k11_group_4(X1))|~l1_group_1(X1)|~v4_group_1(X1)|~v3_group_1(X1)),inference(split_conjunct,[status(thm)],[120])).
% cnf(122,plain,(v3_struct_0(X1)|v10_lattices(k11_group_4(X1))|~l1_group_1(X1)|~v4_group_1(X1)|~v3_group_1(X1)),inference(split_conjunct,[status(thm)],[120])).
% cnf(124,plain,(v3_struct_0(X1)|~l1_group_1(X1)|~v4_group_1(X1)|~v3_group_1(X1)|~v3_struct_0(k11_group_4(X1))),inference(split_conjunct,[status(thm)],[120])).
% fof(125, plain,![X1]:![X2]:((((((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|v3_struct_0(X2))|~(v10_lattices(X2)))|~(l3_lattices(X2)))|![X3]:(~(m3_vectsp_8(X3,X1,X2))|((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))),inference(fof_nnf,[status(thm)],[73])).
% fof(126, plain,![X4]:![X5]:((((((v3_struct_0(X4)|~(v10_lattices(X4)))|~(l3_lattices(X4)))|v3_struct_0(X5))|~(v10_lattices(X5)))|~(l3_lattices(X5)))|![X6]:(~(m3_vectsp_8(X6,X4,X5))|((v1_funct_1(X6)&v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5)))&m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))),inference(variable_rename,[status(thm)],[125])).
% fof(127, plain,![X4]:![X5]:![X6]:((~(m3_vectsp_8(X6,X4,X5))|((v1_funct_1(X6)&v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5)))&m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|(((((v3_struct_0(X4)|~(v10_lattices(X4)))|~(l3_lattices(X4)))|v3_struct_0(X5))|~(v10_lattices(X5)))|~(l3_lattices(X5)))),inference(shift_quantors,[status(thm)],[126])).
% fof(128, plain,![X4]:![X5]:![X6]:((((v1_funct_1(X6)|~(m3_vectsp_8(X6,X4,X5)))|(((((v3_struct_0(X4)|~(v10_lattices(X4)))|~(l3_lattices(X4)))|v3_struct_0(X5))|~(v10_lattices(X5)))|~(l3_lattices(X5))))&((v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))|~(m3_vectsp_8(X6,X4,X5)))|(((((v3_struct_0(X4)|~(v10_lattices(X4)))|~(l3_lattices(X4)))|v3_struct_0(X5))|~(v10_lattices(X5)))|~(l3_lattices(X5)))))&((m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))|~(m3_vectsp_8(X6,X4,X5)))|(((((v3_struct_0(X4)|~(v10_lattices(X4)))|~(l3_lattices(X4)))|v3_struct_0(X5))|~(v10_lattices(X5)))|~(l3_lattices(X5))))),inference(distribute,[status(thm)],[127])).
% cnf(129,plain,(v3_struct_0(X1)|v3_struct_0(X2)|m2_relset_1(X3,u1_struct_0(X2),u1_struct_0(X1))|~l3_lattices(X1)|~v10_lattices(X1)|~l3_lattices(X2)|~v10_lattices(X2)|~m3_vectsp_8(X3,X2,X1)),inference(split_conjunct,[status(thm)],[128])).
% cnf(130,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v1_funct_2(X3,u1_struct_0(X2),u1_struct_0(X1))|~l3_lattices(X1)|~v10_lattices(X1)|~l3_lattices(X2)|~v10_lattices(X2)|~m3_vectsp_8(X3,X2,X1)),inference(split_conjunct,[status(thm)],[128])).
% cnf(131,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v1_funct_1(X3)|~l3_lattices(X1)|~v10_lattices(X1)|~l3_lattices(X2)|~v10_lattices(X2)|~m3_vectsp_8(X3,X2,X1)),inference(split_conjunct,[status(thm)],[128])).
% fof(139, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|![X2]:(((v3_struct_0(X2)|~(v10_lattices(X2)))|~(l3_lattices(X2)))|![X3]:(((~(v1_funct_1(X3))|~(v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))))|~(m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))|((~(m1_lattice4(X3,X1,X2))|(m4_vectsp_8(X3,X1,X2)&m3_vectsp_8(X3,X1,X2)))&((~(m4_vectsp_8(X3,X1,X2))|~(m3_vectsp_8(X3,X1,X2)))|m1_lattice4(X3,X1,X2)))))),inference(fof_nnf,[status(thm)],[75])).
% fof(140, plain,![X4]:(((v3_struct_0(X4)|~(v10_lattices(X4)))|~(l3_lattices(X4)))|![X5]:(((v3_struct_0(X5)|~(v10_lattices(X5)))|~(l3_lattices(X5)))|![X6]:(((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|((~(m1_lattice4(X6,X4,X5))|(m4_vectsp_8(X6,X4,X5)&m3_vectsp_8(X6,X4,X5)))&((~(m4_vectsp_8(X6,X4,X5))|~(m3_vectsp_8(X6,X4,X5)))|m1_lattice4(X6,X4,X5)))))),inference(variable_rename,[status(thm)],[139])).
% fof(141, plain,![X4]:![X5]:![X6]:(((((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|((~(m1_lattice4(X6,X4,X5))|(m4_vectsp_8(X6,X4,X5)&m3_vectsp_8(X6,X4,X5)))&((~(m4_vectsp_8(X6,X4,X5))|~(m3_vectsp_8(X6,X4,X5)))|m1_lattice4(X6,X4,X5))))|((v3_struct_0(X5)|~(v10_lattices(X5)))|~(l3_lattices(X5))))|((v3_struct_0(X4)|~(v10_lattices(X4)))|~(l3_lattices(X4)))),inference(shift_quantors,[status(thm)],[140])).
% fof(142, plain,![X4]:![X5]:![X6]:((((((m4_vectsp_8(X6,X4,X5)|~(m1_lattice4(X6,X4,X5)))|((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))))|((v3_struct_0(X5)|~(v10_lattices(X5)))|~(l3_lattices(X5))))|((v3_struct_0(X4)|~(v10_lattices(X4)))|~(l3_lattices(X4))))&((((m3_vectsp_8(X6,X4,X5)|~(m1_lattice4(X6,X4,X5)))|((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))))|((v3_struct_0(X5)|~(v10_lattices(X5)))|~(l3_lattices(X5))))|((v3_struct_0(X4)|~(v10_lattices(X4)))|~(l3_lattices(X4)))))&(((((~(m4_vectsp_8(X6,X4,X5))|~(m3_vectsp_8(X6,X4,X5)))|m1_lattice4(X6,X4,X5))|((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))))|((v3_struct_0(X5)|~(v10_lattices(X5)))|~(l3_lattices(X5))))|((v3_struct_0(X4)|~(v10_lattices(X4)))|~(l3_lattices(X4))))),inference(distribute,[status(thm)],[141])).
% cnf(143,plain,(v3_struct_0(X1)|v3_struct_0(X2)|m1_lattice4(X3,X1,X2)|~l3_lattices(X1)|~v10_lattices(X1)|~l3_lattices(X2)|~v10_lattices(X2)|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_1(X3)|~m3_vectsp_8(X3,X1,X2)|~m4_vectsp_8(X3,X1,X2)),inference(split_conjunct,[status(thm)],[142])).
% fof(351, negated_conjecture,?[X1]:((((~(v3_struct_0(X1))&v3_group_1(X1))&v4_group_1(X1))&l1_group_1(X1))&?[X2]:((((~(v3_struct_0(X2))&v3_group_1(X2))&v4_group_1(X2))&l1_group_1(X2))&?[X3]:((((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&v1_group_6(X3,X1,X2))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))&(v2_funct_1(X3)&~(m1_lattice4(k3_latsubgr(X1,X2,X3),k11_group_4(X1),k11_group_4(X2))))))),inference(fof_nnf,[status(thm)],[90])).
% fof(352, negated_conjecture,?[X4]:((((~(v3_struct_0(X4))&v3_group_1(X4))&v4_group_1(X4))&l1_group_1(X4))&?[X5]:((((~(v3_struct_0(X5))&v3_group_1(X5))&v4_group_1(X5))&l1_group_1(X5))&?[X6]:((((v1_funct_1(X6)&v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5)))&v1_group_6(X6,X4,X5))&m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))&(v2_funct_1(X6)&~(m1_lattice4(k3_latsubgr(X4,X5,X6),k11_group_4(X4),k11_group_4(X5))))))),inference(variable_rename,[status(thm)],[351])).
% fof(353, negated_conjecture,((((~(v3_struct_0(esk21_0))&v3_group_1(esk21_0))&v4_group_1(esk21_0))&l1_group_1(esk21_0))&((((~(v3_struct_0(esk22_0))&v3_group_1(esk22_0))&v4_group_1(esk22_0))&l1_group_1(esk22_0))&((((v1_funct_1(esk23_0)&v1_funct_2(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0)))&v1_group_6(esk23_0,esk21_0,esk22_0))&m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0)))&(v2_funct_1(esk23_0)&~(m1_lattice4(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))))))),inference(skolemize,[status(esa)],[352])).
% cnf(354,negated_conjecture,(~m1_lattice4(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))),inference(split_conjunct,[status(thm)],[353])).
% cnf(355,negated_conjecture,(v2_funct_1(esk23_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(356,negated_conjecture,(m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))),inference(split_conjunct,[status(thm)],[353])).
% cnf(357,negated_conjecture,(v1_group_6(esk23_0,esk21_0,esk22_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(358,negated_conjecture,(v1_funct_2(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))),inference(split_conjunct,[status(thm)],[353])).
% cnf(359,negated_conjecture,(v1_funct_1(esk23_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(360,negated_conjecture,(l1_group_1(esk22_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(361,negated_conjecture,(v4_group_1(esk22_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(362,negated_conjecture,(v3_group_1(esk22_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(363,negated_conjecture,(~v3_struct_0(esk22_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(364,negated_conjecture,(l1_group_1(esk21_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(365,negated_conjecture,(v4_group_1(esk21_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(366,negated_conjecture,(v3_group_1(esk21_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(367,negated_conjecture,(~v3_struct_0(esk21_0)),inference(split_conjunct,[status(thm)],[353])).
% cnf(945,plain,(m1_lattice4(X3,X1,X2)|v3_struct_0(X2)|v3_struct_0(X1)|~l3_lattices(X2)|~l3_lattices(X1)|~v10_lattices(X2)|~v10_lattices(X1)|~m4_vectsp_8(X3,X1,X2)|~m3_vectsp_8(X3,X1,X2)|~v1_funct_1(X3)|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))),inference(csr,[status(thm)],[143,130])).
% cnf(946,plain,(m1_lattice4(X3,X1,X2)|v3_struct_0(X2)|v3_struct_0(X1)|~l3_lattices(X2)|~l3_lattices(X1)|~v10_lattices(X2)|~v10_lattices(X1)|~m4_vectsp_8(X3,X1,X2)|~m3_vectsp_8(X3,X1,X2)|~v1_funct_1(X3)),inference(csr,[status(thm)],[945,129])).
% cnf(947,plain,(m1_lattice4(X3,X1,X2)|v3_struct_0(X2)|v3_struct_0(X1)|~l3_lattices(X2)|~l3_lattices(X1)|~v10_lattices(X2)|~v10_lattices(X1)|~m4_vectsp_8(X3,X1,X2)|~m3_vectsp_8(X3,X1,X2)),inference(csr,[status(thm)],[946,131])).
% cnf(948,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m4_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))),inference(spm,[status(thm)],[354,947,theory(equality)])).
% cnf(4194,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|~v1_group_6(esk23_0,esk21_0,esk22_0)|~v1_funct_2(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~v1_funct_1(esk23_0)|~v4_group_1(esk22_0)|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(spm,[status(thm)],[948,110,theory(equality)])).
% cnf(4195,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|$false|~v1_funct_2(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~v1_funct_1(esk23_0)|~v4_group_1(esk22_0)|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4194,357,theory(equality)])).
% cnf(4196,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|$false|$false|~v1_funct_1(esk23_0)|~v4_group_1(esk22_0)|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4195,358,theory(equality)])).
% cnf(4197,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|$false|$false|$false|~v4_group_1(esk22_0)|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4196,359,theory(equality)])).
% cnf(4198,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|$false|$false|$false|$false|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4197,361,theory(equality)])).
% cnf(4199,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|$false|$false|$false|$false|$false|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4198,365,theory(equality)])).
% cnf(4200,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|$false|$false|$false|$false|$false|$false|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4199,362,theory(equality)])).
% cnf(4201,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|$false|$false|$false|$false|$false|$false|$false|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4200,366,theory(equality)])).
% cnf(4202,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|$false|$false|$false|$false|$false|$false|$false|$false|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4201,356,theory(equality)])).
% cnf(4203,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4202,360,theory(equality)])).
% cnf(4204,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[4203,364,theory(equality)])).
% cnf(4205,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))),inference(cn,[status(thm)],[4204,theory(equality)])).
% cnf(4206,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))),inference(sr,[status(thm)],[4205,367,theory(equality)])).
% cnf(4207,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~m3_vectsp_8(k3_latsubgr(esk21_0,esk22_0,esk23_0),k11_group_4(esk21_0),k11_group_4(esk22_0))),inference(sr,[status(thm)],[4206,363,theory(equality)])).
% cnf(4251,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|~v2_funct_1(esk23_0)|~v1_group_6(esk23_0,esk21_0,esk22_0)|~v1_funct_2(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~v1_funct_1(esk23_0)|~v4_group_1(esk22_0)|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(spm,[status(thm)],[4207,100,theory(equality)])).
% cnf(4252,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|~v1_group_6(esk23_0,esk21_0,esk22_0)|~v1_funct_2(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~v1_funct_1(esk23_0)|~v4_group_1(esk22_0)|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4251,355,theory(equality)])).
% cnf(4253,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|~v1_funct_2(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~v1_funct_1(esk23_0)|~v4_group_1(esk22_0)|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4252,357,theory(equality)])).
% cnf(4254,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|$false|~v1_funct_1(esk23_0)|~v4_group_1(esk22_0)|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4253,358,theory(equality)])).
% cnf(4255,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|$false|$false|~v4_group_1(esk22_0)|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4254,359,theory(equality)])).
% cnf(4256,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|$false|$false|$false|~v4_group_1(esk21_0)|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4255,361,theory(equality)])).
% cnf(4257,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|$false|$false|$false|$false|~v3_group_1(esk22_0)|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4256,365,theory(equality)])).
% cnf(4258,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|$false|$false|$false|$false|$false|~v3_group_1(esk21_0)|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4257,362,theory(equality)])).
% cnf(4259,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|$false|$false|$false|$false|$false|$false|~m2_relset_1(esk23_0,u1_struct_0(esk21_0),u1_struct_0(esk22_0))|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4258,366,theory(equality)])).
% cnf(4260,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|~l1_group_1(esk22_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4259,356,theory(equality)])).
% cnf(4261,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4260,360,theory(equality)])).
% cnf(4262,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[4261,364,theory(equality)])).
% cnf(4263,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))),inference(cn,[status(thm)],[4262,theory(equality)])).
% cnf(4264,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))),inference(sr,[status(thm)],[4263,367,theory(equality)])).
% cnf(4265,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk22_0))|~v10_lattices(k11_group_4(esk21_0))),inference(sr,[status(thm)],[4264,363,theory(equality)])).
% cnf(4266,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk21_0))|~v4_group_1(esk22_0)|~v3_group_1(esk22_0)|~l1_group_1(esk22_0)),inference(spm,[status(thm)],[4265,122,theory(equality)])).
% cnf(4267,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk21_0))|$false|~v3_group_1(esk22_0)|~l1_group_1(esk22_0)),inference(rw,[status(thm)],[4266,361,theory(equality)])).
% cnf(4268,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|~l1_group_1(esk22_0)),inference(rw,[status(thm)],[4267,362,theory(equality)])).
% cnf(4269,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk21_0))|$false|$false|$false),inference(rw,[status(thm)],[4268,360,theory(equality)])).
% cnf(4270,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk21_0))),inference(cn,[status(thm)],[4269,theory(equality)])).
% cnf(4271,negated_conjecture,(v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(k11_group_4(esk21_0))|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v10_lattices(k11_group_4(esk21_0))),inference(sr,[status(thm)],[4270,363,theory(equality)])).
% cnf(4288,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|~v4_group_1(esk21_0)|~v3_group_1(esk21_0)|~l1_group_1(esk21_0)),inference(spm,[status(thm)],[4271,122,theory(equality)])).
% cnf(4289,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|$false|~v3_group_1(esk21_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4288,365,theory(equality)])).
% cnf(4290,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|$false|$false|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4289,366,theory(equality)])).
% cnf(4291,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))|$false|$false|$false),inference(rw,[status(thm)],[4290,364,theory(equality)])).
% cnf(4292,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|v3_struct_0(esk21_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(cn,[status(thm)],[4291,theory(equality)])).
% cnf(4293,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|v3_struct_0(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(sr,[status(thm)],[4292,367,theory(equality)])).
% cnf(4294,negated_conjecture,(v3_struct_0(esk22_0)|v3_struct_0(k11_group_4(esk21_0))|~v4_group_1(esk22_0)|~v3_group_1(esk22_0)|~l1_group_1(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(spm,[status(thm)],[124,4293,theory(equality)])).
% cnf(4295,negated_conjecture,(v3_struct_0(esk22_0)|v3_struct_0(k11_group_4(esk21_0))|$false|~v3_group_1(esk22_0)|~l1_group_1(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(rw,[status(thm)],[4294,361,theory(equality)])).
% cnf(4296,negated_conjecture,(v3_struct_0(esk22_0)|v3_struct_0(k11_group_4(esk21_0))|$false|$false|~l1_group_1(esk22_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(rw,[status(thm)],[4295,362,theory(equality)])).
% cnf(4297,negated_conjecture,(v3_struct_0(esk22_0)|v3_struct_0(k11_group_4(esk21_0))|$false|$false|$false|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(rw,[status(thm)],[4296,360,theory(equality)])).
% cnf(4298,negated_conjecture,(v3_struct_0(esk22_0)|v3_struct_0(k11_group_4(esk21_0))|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(cn,[status(thm)],[4297,theory(equality)])).
% cnf(4299,negated_conjecture,(v3_struct_0(k11_group_4(esk21_0))|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(sr,[status(thm)],[4298,363,theory(equality)])).
% cnf(4300,negated_conjecture,(v3_struct_0(esk21_0)|~v4_group_1(esk21_0)|~v3_group_1(esk21_0)|~l1_group_1(esk21_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(spm,[status(thm)],[124,4299,theory(equality)])).
% cnf(4301,negated_conjecture,(v3_struct_0(esk21_0)|$false|~v3_group_1(esk21_0)|~l1_group_1(esk21_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(rw,[status(thm)],[4300,365,theory(equality)])).
% cnf(4302,negated_conjecture,(v3_struct_0(esk21_0)|$false|$false|~l1_group_1(esk21_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(rw,[status(thm)],[4301,366,theory(equality)])).
% cnf(4303,negated_conjecture,(v3_struct_0(esk21_0)|$false|$false|$false|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(rw,[status(thm)],[4302,364,theory(equality)])).
% cnf(4304,negated_conjecture,(v3_struct_0(esk21_0)|~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(cn,[status(thm)],[4303,theory(equality)])).
% cnf(4305,negated_conjecture,(~l3_lattices(k11_group_4(esk22_0))|~l3_lattices(k11_group_4(esk21_0))),inference(sr,[status(thm)],[4304,367,theory(equality)])).
% cnf(4306,negated_conjecture,(v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk21_0))|~v4_group_1(esk22_0)|~v3_group_1(esk22_0)|~l1_group_1(esk22_0)),inference(spm,[status(thm)],[4305,121,theory(equality)])).
% cnf(4307,negated_conjecture,(v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk21_0))|$false|~v3_group_1(esk22_0)|~l1_group_1(esk22_0)),inference(rw,[status(thm)],[4306,361,theory(equality)])).
% cnf(4308,negated_conjecture,(v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk21_0))|$false|$false|~l1_group_1(esk22_0)),inference(rw,[status(thm)],[4307,362,theory(equality)])).
% cnf(4309,negated_conjecture,(v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk21_0))|$false|$false|$false),inference(rw,[status(thm)],[4308,360,theory(equality)])).
% cnf(4310,negated_conjecture,(v3_struct_0(esk22_0)|~l3_lattices(k11_group_4(esk21_0))),inference(cn,[status(thm)],[4309,theory(equality)])).
% cnf(4311,negated_conjecture,(~l3_lattices(k11_group_4(esk21_0))),inference(sr,[status(thm)],[4310,363,theory(equality)])).
% cnf(4317,negated_conjecture,(v3_struct_0(esk21_0)|~v4_group_1(esk21_0)|~v3_group_1(esk21_0)|~l1_group_1(esk21_0)),inference(spm,[status(thm)],[4311,121,theory(equality)])).
% cnf(4318,negated_conjecture,(v3_struct_0(esk21_0)|$false|~v3_group_1(esk21_0)|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4317,365,theory(equality)])).
% cnf(4319,negated_conjecture,(v3_struct_0(esk21_0)|$false|$false|~l1_group_1(esk21_0)),inference(rw,[status(thm)],[4318,366,theory(equality)])).
% cnf(4320,negated_conjecture,(v3_struct_0(esk21_0)|$false|$false|$false),inference(rw,[status(thm)],[4319,364,theory(equality)])).
% cnf(4321,negated_conjecture,(v3_struct_0(esk21_0)),inference(cn,[status(thm)],[4320,theory(equality)])).
% cnf(4322,negated_conjecture,($false),inference(sr,[status(thm)],[4321,367,theory(equality)])).
% cnf(4323,negated_conjecture,($false),4322,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 1052
% # ...of these trivial : 5
% # ...subsumed : 522
% # ...remaining for further processing: 525
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 19
% # Backward-rewritten : 14
% # Generated clauses : 1881
% # ...of the previous two non-trivial : 1680
% # Contextual simplify-reflections : 644
% # Paramodulations : 1866
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 486
% # Positive orientable unit clauses: 63
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 15
% # Non-unit-clauses : 408
% # Current number of unprocessed clauses: 680
% # ...number of literals in the above : 4902
% # Clause-clause subsumption calls (NU) : 18853
% # Rec. Clause-clause subsumption calls : 8243
% # Unit Clause-clause subsumption calls : 347
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 34
% # Indexed BW rewrite successes : 9
% # Backwards rewriting index: 407 leaves, 1.67+/-1.916 terms/leaf
% # Paramod-from index: 185 leaves, 1.22+/-1.184 terms/leaf
% # Paramod-into index: 357 leaves, 1.46+/-1.798 terms/leaf
% # -------------------------------------------------
% # User time : 0.214 s
% # System time : 0.006 s
% # Total time : 0.220 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.37 CPU 0.46 WC
% FINAL PrfWatch: 0.37 CPU 0.46 WC
% SZS output end Solution for /tmp/SystemOnTPTP10382/GRP653+1.tptp
%
%------------------------------------------------------------------------------