%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LAT323+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sun Jul 17 06:50:48 EDT 2022
% Result : Theorem 0.79s 0.97s
% Output : Refutation 0.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 54
% Syntax : Number of clauses : 155 ( 51 unt; 81 nHn; 155 RR)
% Number of literals : 519 ( 0 equ; 283 neg)
% Maximal clause size : 14 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 29 ( 28 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
v10_lattices(skc20),
file('LAT323+1.p',unknown),
[] ).
cnf(2,axiom,
v17_lattices(skc20),
file('LAT323+1.p',unknown),
[] ).
cnf(3,axiom,
l3_lattices(skc20),
file('LAT323+1.p',unknown),
[] ).
cnf(85,axiom,
m2_filter_2(skc21,skc20),
file('LAT323+1.p',unknown),
[] ).
cnf(86,axiom,
~ v3_struct_0(skc20),
file('LAT323+1.p',unknown),
[] ).
cnf(87,axiom,
r2_filter_2(skc20,skc21),
file('LAT323+1.p',unknown),
[] ).
cnf(98,axiom,
m1_subset_1(skc22,u1_struct_0(skc20)),
file('LAT323+1.p',unknown),
[] ).
cnf(105,axiom,
( ~ l3_lattices(u)
| l1_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(106,axiom,
( ~ l3_lattices(u)
| l2_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(109,axiom,
( ~ l3_lattices(u)
| v3_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(110,axiom,
( ~ l3_lattices(u)
| l3_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(124,axiom,
( ~ r2_hidden(k7_lattices(skc20,skc22),skc21)
| r2_hidden(skc22,skc21) ),
file('LAT323+1.p',unknown),
[] ).
cnf(125,axiom,
( ~ r2_hidden(skc22,skc21)
| r2_hidden(k7_lattices(skc20,skc22),skc21) ),
file('LAT323+1.p',unknown),
[] ).
cnf(127,axiom,
( ~ l3_lattices(u)
| ~ v3_struct_0(k1_lattice2(u))
| v3_struct_0(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(135,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v4_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(136,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v5_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(137,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v6_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(138,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v7_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(139,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v8_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(140,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v9_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(143,axiom,
( ~ v17_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v11_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(144,axiom,
( ~ v17_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v13_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(145,axiom,
( ~ v17_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v14_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(146,axiom,
( ~ v17_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v15_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(147,axiom,
( ~ v17_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v16_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(159,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v4_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(160,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v5_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(161,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v6_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(162,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v7_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(163,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v8_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(164,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v9_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(165,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v10_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(172,axiom,
( ~ r2_hidden(u,v)
| ~ m1_subset_1(v,k1_zfmisc_1(w))
| m1_subset_1(u,w) ),
file('LAT323+1.p',unknown),
[] ).
cnf(181,axiom,
( ~ v11_lattices(u)
| ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v12_lattices(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(199,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v11_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(200,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v12_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(201,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v13_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(202,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v14_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(203,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v15_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(204,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v16_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(205,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v17_lattices(k1_lattice2(u)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(211,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m2_filter_2(v,u)
| v3_struct_0(u)
| m2_lattice4(v,u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(213,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_filter_2(v,u)
| v3_struct_0(u)
| m1_filter_0(v,u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(217,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_filter_0(v,u)
| v3_struct_0(u)
| m1_subset_1(v,k1_zfmisc_1(u1_struct_0(u))) ),
file('LAT323+1.p',unknown),
[] ).
cnf(218,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m2_lattice4(v,u)
| v3_struct_0(u)
| m1_subset_1(v,k1_zfmisc_1(u1_struct_0(u))) ),
file('LAT323+1.p',unknown),
[] ).
cnf(219,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| v3_struct_0(u)
| equal(k5_filter_2(u,v),v) ),
file('LAT323+1.p',unknown),
[] ).
cnf(220,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m2_filter_2(v,u)
| m1_filter_2(k15_filter_2(u,v),k1_lattice2(u))
| v3_struct_0(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(229,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,k1_zfmisc_1(u1_struct_0(u)))
| v3_struct_0(u)
| equal(k7_filter_2(u,v),v) ),
file('LAT323+1.p',unknown),
[] ).
cnf(230,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| ~ m2_filter_2(v,u)
| v3_struct_0(u)
| equal(k15_filter_2(u,v),k7_filter_2(u,v)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(231,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| m1_subset_1(k5_filter_2(u,v),u1_struct_0(k1_lattice2(u)))
| v3_struct_0(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(234,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| ~ r2_filter_2(u,v)
| ~ m2_filter_2(v,u)
| v1_filter_0(k15_filter_2(u,v),k1_lattice2(u))
| v3_struct_0(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(237,axiom,
( ~ v10_lattices(u)
| ~ v17_lattices(u)
| ~ l3_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| v3_struct_0(u)
| equal(k7_lattices(k1_lattice2(u),k5_filter_2(u,v)),k7_lattices(u,v)) ),
file('LAT323+1.p',unknown),
[] ).
cnf(238,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ v1_filter_0(v,u)
| ~ m1_filter_0(v,u)
| ~ m1_subset_1(w,u1_struct_0(u))
| v3_struct_0(u)
| r2_hidden(w,v)
| r2_hidden(k7_lattices(u,w),v) ),
file('LAT323+1.p',unknown),
[] ).
cnf(239,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ v1_filter_0(v,u)
| ~ m1_filter_0(v,u)
| ~ r2_hidden(w,v)
| ~ m1_subset_1(w,u1_struct_0(u))
| ~ r2_hidden(k7_lattices(u,w),v)
| v3_struct_0(u) ),
file('LAT323+1.p',unknown),
[] ).
cnf(248,plain,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| ~ m2_filter_2(v,u)
| v3_struct_0(u)
| m1_filter_2(k7_filter_2(u,v),k1_lattice2(u)) ),
inference(rew,[status(thm),theory(equality)],[230,220]),
[iquote('0:Rew:230.3,220.3')] ).
cnf(249,plain,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| v3_struct_0(u)
| m1_subset_1(v,u1_struct_0(k1_lattice2(u))) ),
inference(rew,[status(thm),theory(equality)],[219,231]),
[iquote('0:Rew:219.4,231.3')] ).
cnf(252,plain,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m2_filter_2(v,u)
| ~ r2_filter_2(u,v)
| v3_struct_0(u)
| v1_filter_0(k7_filter_2(u,v),k1_lattice2(u)) ),
inference(rew,[status(thm),theory(equality)],[230,234]),
[iquote('0:Rew:230.3,234.4')] ).
cnf(254,plain,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| v3_struct_0(u)
| equal(k7_lattices(k1_lattice2(u),v),k7_lattices(u,v)) ),
inference(rew,[status(thm),theory(equality)],[219,237]),
[iquote('0:Rew:219.4,237.5')] ).
cnf(263,plain,
( ~ v10_lattices(skc20)
| ~ m1_subset_1(u,k1_zfmisc_1(u1_struct_0(skc20)))
| v3_struct_0(skc20)
| equal(k7_filter_2(skc20,u),u) ),
inference(res,[status(thm),theory(equality)],[3,229]),
[iquote('0:Res:3.0,229.1')] ).
cnf(268,plain,
( ~ v10_lattices(skc20)
| ~ m2_lattice4(u,skc20)
| v3_struct_0(skc20)
| m1_subset_1(u,k1_zfmisc_1(u1_struct_0(skc20))) ),
inference(res,[status(thm),theory(equality)],[3,218]),
[iquote('0:Res:3.0,218.1')] ).
cnf(276,plain,
( ~ v10_lattices(skc20)
| ~ v17_lattices(skc20)
| v11_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,199]),
[iquote('0:Res:3.0,199.2')] ).
cnf(277,plain,
( ~ v10_lattices(skc20)
| ~ v17_lattices(skc20)
| v12_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,200]),
[iquote('0:Res:3.0,200.2')] ).
cnf(278,plain,
( ~ v10_lattices(skc20)
| ~ v17_lattices(skc20)
| v13_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,201]),
[iquote('0:Res:3.0,201.2')] ).
cnf(279,plain,
( ~ v10_lattices(skc20)
| ~ v17_lattices(skc20)
| v14_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,202]),
[iquote('0:Res:3.0,202.2')] ).
cnf(280,plain,
( ~ v10_lattices(skc20)
| ~ v17_lattices(skc20)
| v15_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,203]),
[iquote('0:Res:3.0,203.2')] ).
cnf(281,plain,
( ~ v10_lattices(skc20)
| ~ v17_lattices(skc20)
| v16_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,204]),
[iquote('0:Res:3.0,204.2')] ).
cnf(282,plain,
( ~ v10_lattices(skc20)
| ~ v17_lattices(skc20)
| v17_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,205]),
[iquote('0:Res:3.0,205.2')] ).
cnf(284,plain,
( ~ v10_lattices(skc20)
| ~ v11_lattices(skc20)
| v12_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,181]),
[iquote('0:Res:3.0,181.0')] ).
cnf(291,plain,
( ~ v10_lattices(skc20)
| v4_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,159]),
[iquote('0:Res:3.0,159.1')] ).
cnf(292,plain,
( ~ v10_lattices(skc20)
| v5_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,160]),
[iquote('0:Res:3.0,160.1')] ).
cnf(293,plain,
( ~ v10_lattices(skc20)
| v6_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,161]),
[iquote('0:Res:3.0,161.1')] ).
cnf(294,plain,
( ~ v10_lattices(skc20)
| v7_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,162]),
[iquote('0:Res:3.0,162.1')] ).
cnf(295,plain,
( ~ v10_lattices(skc20)
| v8_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,163]),
[iquote('0:Res:3.0,163.1')] ).
cnf(296,plain,
( ~ v10_lattices(skc20)
| v9_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,164]),
[iquote('0:Res:3.0,164.1')] ).
cnf(297,plain,
( ~ v10_lattices(skc20)
| v10_lattices(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,165]),
[iquote('0:Res:3.0,165.1')] ).
cnf(298,plain,
( ~ v10_lattices(skc20)
| v4_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,135]),
[iquote('0:Res:3.0,135.0')] ).
cnf(299,plain,
( ~ v10_lattices(skc20)
| v5_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,136]),
[iquote('0:Res:3.0,136.0')] ).
cnf(300,plain,
( ~ v10_lattices(skc20)
| v6_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,137]),
[iquote('0:Res:3.0,137.0')] ).
cnf(301,plain,
( ~ v10_lattices(skc20)
| v7_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,138]),
[iquote('0:Res:3.0,138.0')] ).
cnf(302,plain,
( ~ v10_lattices(skc20)
| v8_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,139]),
[iquote('0:Res:3.0,139.0')] ).
cnf(303,plain,
( ~ v10_lattices(skc20)
| v9_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,140]),
[iquote('0:Res:3.0,140.0')] ).
cnf(306,plain,
( ~ v17_lattices(skc20)
| v11_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,143]),
[iquote('0:Res:3.0,143.0')] ).
cnf(307,plain,
( ~ v17_lattices(skc20)
| v13_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,144]),
[iquote('0:Res:3.0,144.0')] ).
cnf(308,plain,
( ~ v17_lattices(skc20)
| v14_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,145]),
[iquote('0:Res:3.0,145.0')] ).
cnf(309,plain,
( ~ v17_lattices(skc20)
| v15_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,146]),
[iquote('0:Res:3.0,146.0')] ).
cnf(310,plain,
( ~ v17_lattices(skc20)
| v16_lattices(skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,147]),
[iquote('0:Res:3.0,147.0')] ).
cnf(311,plain,
( ~ v3_struct_0(k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3,127]),
[iquote('0:Res:3.0,127.0')] ).
cnf(312,plain,
v3_lattices(k1_lattice2(skc20)),
inference(res,[status(thm),theory(equality)],[3,109]),
[iquote('0:Res:3.0,109.0')] ).
cnf(313,plain,
l3_lattices(k1_lattice2(skc20)),
inference(res,[status(thm),theory(equality)],[3,110]),
[iquote('0:Res:3.0,110.0')] ).
cnf(314,plain,
l1_lattices(skc20),
inference(res,[status(thm),theory(equality)],[3,105]),
[iquote('0:Res:3.0,105.0')] ).
cnf(315,plain,
l2_lattices(skc20),
inference(res,[status(thm),theory(equality)],[3,106]),
[iquote('0:Res:3.0,106.0')] ).
cnf(380,plain,
( ~ v10_lattices(skc20)
| ~ l3_lattices(skc20)
| ~ m2_filter_2(skc21,skc20)
| v1_filter_0(k7_filter_2(skc20,skc21),k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[87,252]),
[iquote('0:Res:87.0,252.2')] ).
cnf(455,plain,
( ~ l3_lattices(skc20)
| ~ v10_lattices(skc20)
| m1_filter_2(k7_filter_2(skc20,skc21),k1_lattice2(skc20))
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[85,248]),
[iquote('0:Res:85.0,248.2')] ).
cnf(457,plain,
( ~ v10_lattices(skc20)
| ~ l3_lattices(skc20)
| m2_lattice4(skc21,skc20)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[85,211]),
[iquote('0:Res:85.0,211.2')] ).
cnf(466,plain,
~ v3_struct_0(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[311,86]),
[iquote('0:MRR:311.1,86.0')] ).
cnf(467,plain,
v4_lattices(skc20),
inference(mrr,[status(thm)],[298,1,86]),
[iquote('0:MRR:298.0,298.2,1.0,86.0')] ).
cnf(468,plain,
v5_lattices(skc20),
inference(mrr,[status(thm)],[299,1,86]),
[iquote('0:MRR:299.0,299.2,1.0,86.0')] ).
cnf(469,plain,
v6_lattices(skc20),
inference(mrr,[status(thm)],[300,1,86]),
[iquote('0:MRR:300.0,300.2,1.0,86.0')] ).
cnf(470,plain,
v7_lattices(skc20),
inference(mrr,[status(thm)],[301,1,86]),
[iquote('0:MRR:301.0,301.2,1.0,86.0')] ).
cnf(471,plain,
v8_lattices(skc20),
inference(mrr,[status(thm)],[302,1,86]),
[iquote('0:MRR:302.0,302.2,1.0,86.0')] ).
cnf(472,plain,
v9_lattices(skc20),
inference(mrr,[status(thm)],[303,1,86]),
[iquote('0:MRR:303.0,303.2,1.0,86.0')] ).
cnf(475,plain,
v11_lattices(skc20),
inference(mrr,[status(thm)],[306,2,86]),
[iquote('0:MRR:306.0,306.2,2.0,86.0')] ).
cnf(476,plain,
v13_lattices(skc20),
inference(mrr,[status(thm)],[307,2,86]),
[iquote('0:MRR:307.0,307.2,2.0,86.0')] ).
cnf(477,plain,
v14_lattices(skc20),
inference(mrr,[status(thm)],[308,2,86]),
[iquote('0:MRR:308.0,308.2,2.0,86.0')] ).
cnf(478,plain,
v15_lattices(skc20),
inference(mrr,[status(thm)],[309,2,86]),
[iquote('0:MRR:309.0,309.2,2.0,86.0')] ).
cnf(479,plain,
v16_lattices(skc20),
inference(mrr,[status(thm)],[310,2,86]),
[iquote('0:MRR:310.0,310.2,2.0,86.0')] ).
cnf(480,plain,
v4_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[291,1,86]),
[iquote('0:MRR:291.0,291.2,1.0,86.0')] ).
cnf(481,plain,
v5_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[292,1,86]),
[iquote('0:MRR:292.0,292.2,1.0,86.0')] ).
cnf(482,plain,
v6_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[293,1,86]),
[iquote('0:MRR:293.0,293.2,1.0,86.0')] ).
cnf(483,plain,
v7_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[294,1,86]),
[iquote('0:MRR:294.0,294.2,1.0,86.0')] ).
cnf(484,plain,
v8_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[295,1,86]),
[iquote('0:MRR:295.0,295.2,1.0,86.0')] ).
cnf(485,plain,
v9_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[296,1,86]),
[iquote('0:MRR:296.0,296.2,1.0,86.0')] ).
cnf(486,plain,
v10_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[297,1,86]),
[iquote('0:MRR:297.0,297.2,1.0,86.0')] ).
cnf(494,plain,
v12_lattices(skc20),
inference(mrr,[status(thm)],[284,1,475,86]),
[iquote('0:MRR:284.0,284.1,284.3,1.0,475.0,86.0')] ).
cnf(495,plain,
v11_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[276,1,2,86]),
[iquote('0:MRR:276.0,276.1,276.3,1.0,2.0,86.0')] ).
cnf(496,plain,
v12_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[277,1,2,86]),
[iquote('0:MRR:277.0,277.1,277.3,1.0,2.0,86.0')] ).
cnf(497,plain,
v13_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[278,1,2,86]),
[iquote('0:MRR:278.0,278.1,278.3,1.0,2.0,86.0')] ).
cnf(498,plain,
v14_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[279,1,2,86]),
[iquote('0:MRR:279.0,279.1,279.3,1.0,2.0,86.0')] ).
cnf(499,plain,
v15_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[280,1,2,86]),
[iquote('0:MRR:280.0,280.1,280.3,1.0,2.0,86.0')] ).
cnf(500,plain,
v16_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[281,1,2,86]),
[iquote('0:MRR:281.0,281.1,281.3,1.0,2.0,86.0')] ).
cnf(501,plain,
v17_lattices(k1_lattice2(skc20)),
inference(mrr,[status(thm)],[282,1,2,86]),
[iquote('0:MRR:282.0,282.1,282.3,1.0,2.0,86.0')] ).
cnf(506,plain,
m2_lattice4(skc21,skc20),
inference(mrr,[status(thm)],[457,1,3,86]),
[iquote('0:MRR:457.0,457.1,457.3,1.0,3.0,86.0')] ).
cnf(520,plain,
( ~ m2_lattice4(u,skc20)
| m1_subset_1(u,k1_zfmisc_1(u1_struct_0(skc20))) ),
inference(mrr,[status(thm)],[268,1,86]),
[iquote('0:MRR:268.0,268.2,1.0,86.0')] ).
cnf(521,plain,
m1_filter_2(k7_filter_2(skc20,skc21),k1_lattice2(skc20)),
inference(mrr,[status(thm)],[455,3,1,86]),
[iquote('0:MRR:455.0,455.1,455.3,3.0,1.0,86.0')] ).
cnf(526,plain,
( ~ m1_subset_1(u,k1_zfmisc_1(u1_struct_0(skc20)))
| equal(k7_filter_2(skc20,u),u) ),
inference(mrr,[status(thm)],[263,1,86]),
[iquote('0:MRR:263.0,263.2,1.0,86.0')] ).
cnf(531,plain,
v1_filter_0(k7_filter_2(skc20,skc21),k1_lattice2(skc20)),
inference(mrr,[status(thm)],[380,1,3,85,86]),
[iquote('0:MRR:380.0,380.1,380.2,380.4,1.0,3.0,85.0,86.0')] ).
cnf(587,plain,
~ r2_hidden(skc22,skc21),
inference(spt,[spt(split,[position(s1)])],[125]),
[iquote('1:Spt:125.0')] ).
cnf(588,plain,
~ r2_hidden(k7_lattices(skc20,skc22),skc21),
inference(mrr,[status(thm)],[124,587]),
[iquote('1:MRR:124.1,587.0')] ).
cnf(627,plain,
( ~ m2_lattice4(u,skc20)
| equal(k7_filter_2(skc20,u),u) ),
inference(res,[status(thm),theory(equality)],[520,526]),
[iquote('0:Res:520.1,526.0')] ).
cnf(641,plain,
( ~ m2_lattice4(skc21,skc20)
| v1_filter_0(skc21,k1_lattice2(skc20)) ),
inference(spr,[status(thm),theory(equality)],[627,531]),
[iquote('0:SpR:627.1,531.0')] ).
cnf(642,plain,
( ~ m2_lattice4(skc21,skc20)
| m1_filter_2(skc21,k1_lattice2(skc20)) ),
inference(spr,[status(thm),theory(equality)],[627,521]),
[iquote('0:SpR:627.1,521.0')] ).
cnf(649,plain,
v1_filter_0(skc21,k1_lattice2(skc20)),
inference(mrr,[status(thm)],[641,506]),
[iquote('0:MRR:641.0,506.0')] ).
cnf(650,plain,
m1_filter_2(skc21,k1_lattice2(skc20)),
inference(mrr,[status(thm)],[642,506]),
[iquote('0:MRR:642.0,506.0')] ).
cnf(1393,plain,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_filter_0(v,u)
| ~ r2_hidden(w,v)
| v3_struct_0(u)
| m1_subset_1(w,u1_struct_0(u)) ),
inference(res,[status(thm),theory(equality)],[217,172]),
[iquote('0:Res:217.4,172.1')] ).
cnf(1397,plain,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ v1_filter_0(v,u)
| ~ m1_filter_0(v,u)
| ~ r2_hidden(w,v)
| ~ r2_hidden(k7_lattices(u,w),v)
| v3_struct_0(u) ),
inference(mrr,[status(thm)],[239,1393]),
[iquote('0:MRR:239.6,1393.5')] ).
cnf(1832,plain,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ l3_lattices(k1_lattice2(u))
| ~ v17_lattices(k1_lattice2(u))
| ~ v10_lattices(k1_lattice2(u))
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ v1_filter_0(w,k1_lattice2(u))
| ~ m1_filter_0(w,k1_lattice2(u))
| ~ r2_hidden(v,w)
| ~ r2_hidden(k7_lattices(u,v),w)
| v3_struct_0(u)
| v3_struct_0(k1_lattice2(u)) ),
inference(spl,[status(thm),theory(equality)],[254,1397]),
[iquote('0:SpL:254.5,1397.6')] ).
cnf(1837,plain,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ v17_lattices(k1_lattice2(u))
| ~ v10_lattices(k1_lattice2(u))
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ v1_filter_0(w,k1_lattice2(u))
| ~ m1_filter_0(w,k1_lattice2(u))
| ~ r2_hidden(v,w)
| ~ r2_hidden(k7_lattices(u,v),w)
| v3_struct_0(u)
| v3_struct_0(k1_lattice2(u)) ),
inference(ssi,[status(thm)],[1832,109,110]),
[iquote('0:SSi:1832.3,109.1,110.1')] ).
cnf(1838,plain,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ v1_filter_0(w,k1_lattice2(u))
| ~ m1_filter_0(w,k1_lattice2(u))
| ~ r2_hidden(v,w)
| ~ r2_hidden(k7_lattices(u,v),w)
| v3_struct_0(u) ),
inference(mrr,[status(thm)],[1837,205,165,127]),
[iquote('0:MRR:1837.3,1837.4,1837.11,205.4,165.3,127.1')] ).
cnf(1864,plain,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ l3_lattices(k1_lattice2(u))
| ~ v17_lattices(k1_lattice2(u))
| ~ v10_lattices(k1_lattice2(u))
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ v1_filter_0(w,k1_lattice2(u))
| ~ m1_filter_0(w,k1_lattice2(u))
| ~ m1_subset_1(v,u1_struct_0(k1_lattice2(u)))
| v3_struct_0(u)
| v3_struct_0(k1_lattice2(u))
| r2_hidden(v,w)
| r2_hidden(k7_lattices(u,v),w) ),
inference(spr,[status(thm),theory(equality)],[254,238]),
[iquote('0:SpR:254.5,238.8')] ).
cnf(1888,plain,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ v17_lattices(k1_lattice2(u))
| ~ v10_lattices(k1_lattice2(u))
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ v1_filter_0(w,k1_lattice2(u))
| ~ m1_filter_0(w,k1_lattice2(u))
| ~ m1_subset_1(v,u1_struct_0(k1_lattice2(u)))
| v3_struct_0(u)
| v3_struct_0(k1_lattice2(u))
| r2_hidden(v,w)
| r2_hidden(k7_lattices(u,v),w) ),
inference(ssi,[status(thm)],[1864,109,110]),
[iquote('0:SSi:1864.3,109.1,110.1')] ).
cnf(1889,plain,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ v1_filter_0(w,k1_lattice2(u))
| ~ m1_filter_0(w,k1_lattice2(u))
| v3_struct_0(u)
| r2_hidden(v,w)
| r2_hidden(k7_lattices(u,v),w) ),
inference(mrr,[status(thm)],[1888,205,165,249,127]),
[iquote('0:MRR:1888.3,1888.4,1888.8,1888.10,205.4,165.3,249.4,127.1')] ).
cnf(3733,plain,
( ~ l3_lattices(skc20)
| ~ v17_lattices(skc20)
| ~ v10_lattices(skc20)
| ~ m1_subset_1(skc22,u1_struct_0(skc20))
| ~ v1_filter_0(skc21,k1_lattice2(skc20))
| ~ m1_filter_0(skc21,k1_lattice2(skc20))
| v3_struct_0(skc20)
| r2_hidden(skc22,skc21) ),
inference(res,[status(thm),theory(equality)],[1889,588]),
[iquote('1:Res:1889.8,588.0')] ).
cnf(3736,plain,
( ~ m1_subset_1(skc22,u1_struct_0(skc20))
| ~ v1_filter_0(skc21,k1_lattice2(skc20))
| ~ m1_filter_0(skc21,k1_lattice2(skc20))
| v3_struct_0(skc20)
| r2_hidden(skc22,skc21) ),
inference(ssi,[status(thm)],[3733,2,1,3,494,479,475,477,476,472,471,478,470,469,468,467,315,314]),
[iquote('1:SSi:3733.2,3733.1,3733.0,2.0,1.0,3.0,494.0,479.0,475.0,477.0,476.0,472.0,471.0,478.0,470.0,469.0,468.0,467.0,315.0,314.0,2.0,1.0,3.0,494.0,479.0,475.0,477.0,476.0,472.0,471.0,478.0,470.0,469.0,468.0,467.0,315.0,314.0,2.0,1.0,3.0,494.0,479.0,475.0,477.0,476.0,472.0,471.0,478.0,470.0,469.0,468.0,467.0,315.0,314.0')] ).
cnf(3737,plain,
~ m1_filter_0(skc21,k1_lattice2(skc20)),
inference(mrr,[status(thm)],[3736,98,649,86,587]),
[iquote('1:MRR:3736.0,3736.1,3736.3,3736.4,98.0,649.0,86.0,587.0')] ).
cnf(3738,plain,
( ~ l3_lattices(k1_lattice2(skc20))
| ~ v10_lattices(k1_lattice2(skc20))
| ~ m1_filter_2(skc21,k1_lattice2(skc20))
| v3_struct_0(k1_lattice2(skc20)) ),
inference(res,[status(thm),theory(equality)],[213,3737]),
[iquote('1:Res:213.4,3737.0')] ).
cnf(3739,plain,
( ~ m1_filter_2(skc21,k1_lattice2(skc20))
| v3_struct_0(k1_lattice2(skc20)) ),
inference(ssi,[status(thm)],[3738,496,500,495,498,497,485,484,499,312,483,482,481,480,501,486,313]),
[iquote('1:SSi:3738.1,3738.0,496.0,500.0,495.0,498.0,497.0,485.0,484.0,499.0,312.0,483.0,482.0,481.0,480.0,501.0,486.0,313.0,496.0,500.0,495.0,498.0,497.0,485.0,484.0,499.0,312.0,483.0,482.0,481.0,480.0,501.0,486.0,313.0')] ).
cnf(3740,plain,
$false,
inference(mrr,[status(thm)],[3739,650,466]),
[iquote('1:MRR:3739.0,3739.1,650.0,466.0')] ).
cnf(3741,plain,
r2_hidden(skc22,skc21),
inference(spt,[spt(split,[position(sa)])],[3740,587]),
[iquote('1:Spt:3740.0,125.0,587.0')] ).
cnf(3742,plain,
r2_hidden(k7_lattices(skc20,skc22),skc21),
inference(spt,[spt(split,[position(s2)])],[125]),
[iquote('1:Spt:3740.0,125.1')] ).
cnf(3862,plain,
( ~ l3_lattices(skc20)
| ~ v17_lattices(skc20)
| ~ v10_lattices(skc20)
| ~ m1_subset_1(skc22,u1_struct_0(skc20))
| ~ v1_filter_0(skc21,k1_lattice2(skc20))
| ~ m1_filter_0(skc21,k1_lattice2(skc20))
| ~ r2_hidden(skc22,skc21)
| v3_struct_0(skc20) ),
inference(res,[status(thm),theory(equality)],[3742,1838]),
[iquote('1:Res:3742.0,1838.7')] ).
cnf(3864,plain,
( ~ m1_subset_1(skc22,u1_struct_0(skc20))
| ~ v1_filter_0(skc21,k1_lattice2(skc20))
| ~ m1_filter_0(skc21,k1_lattice2(skc20))
| ~ r2_hidden(skc22,skc21)
| v3_struct_0(skc20) ),
inference(ssi,[status(thm)],[3862,2,1,3,494,479,475,477,476,472,471,478,470,469,468,467,315,314]),
[iquote('1:SSi:3862.2,3862.1,3862.0,2.0,1.0,3.0,494.0,479.0,475.0,477.0,476.0,472.0,471.0,478.0,470.0,469.0,468.0,467.0,315.0,314.0,2.0,1.0,3.0,494.0,479.0,475.0,477.0,476.0,472.0,471.0,478.0,470.0,469.0,468.0,467.0,315.0,314.0,2.0,1.0,3.0,494.0,479.0,475.0,477.0,476.0,472.0,471.0,478.0,470.0,469.0,468.0,467.0,315.0,314.0')] ).
cnf(3865,plain,
~ m1_filter_0(skc21,k1_lattice2(skc20)),
inference(mrr,[status(thm)],[3864,98,649,3741,86]),
[iquote('1:MRR:3864.0,3864.1,3864.3,3864.4,98.0,649.0,3741.0,86.0')] ).
cnf(3872,plain,
( ~ l3_lattices(k1_lattice2(skc20))
| ~ v10_lattices(k1_lattice2(skc20))
| ~ m1_filter_2(skc21,k1_lattice2(skc20))
| v3_struct_0(k1_lattice2(skc20)) ),
inference(res,[status(thm),theory(equality)],[213,3865]),
[iquote('1:Res:213.4,3865.0')] ).
cnf(3873,plain,
( ~ m1_filter_2(skc21,k1_lattice2(skc20))
| v3_struct_0(k1_lattice2(skc20)) ),
inference(ssi,[status(thm)],[3872,496,500,495,498,497,485,484,499,312,483,482,481,480,501,486,313]),
[iquote('1:SSi:3872.1,3872.0,496.0,500.0,495.0,498.0,497.0,485.0,484.0,499.0,312.0,483.0,482.0,481.0,480.0,501.0,486.0,313.0,496.0,500.0,495.0,498.0,497.0,485.0,484.0,499.0,312.0,483.0,482.0,481.0,480.0,501.0,486.0,313.0')] ).
cnf(3874,plain,
$false,
inference(mrr,[status(thm)],[3873,650,466]),
[iquote('1:MRR:3873.0,3873.1,650.0,466.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : LAT323+1 : TPTP v8.1.0. Released v3.4.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.32 % Computer : n006.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 600
% 0.12/0.32 % DateTime : Wed Jun 29 04:47:53 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.79/0.97
% 0.79/0.97 SPASS V 3.9
% 0.79/0.97 SPASS beiseite: Proof found.
% 0.79/0.97 % SZS status Theorem
% 0.79/0.97 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.79/0.97 SPASS derived 2748 clauses, backtracked 215 clauses, performed 14 splits and kept 1616 clauses.
% 0.79/0.97 SPASS allocated 101332 KBytes.
% 0.79/0.97 SPASS spent 0:00:00.63 on the problem.
% 0.79/0.97 0:00:00.04 for the input.
% 0.79/0.97 0:00:00.05 for the FLOTTER CNF translation.
% 0.79/0.97 0:00:00.05 for inferences.
% 0.79/0.97 0:00:00.01 for the backtracking.
% 0.79/0.97 0:00:00.42 for the reduction.
% 0.79/0.97
% 0.79/0.97
% 0.79/0.97 Here is a proof with depth 3, length 155 :
% 0.79/0.97 % SZS output start Refutation
% See solution above
% 0.79/0.99 Formulae used in the proof : t59_filter_2 dt_l3_lattices dt_k1_lattice2 fc1_lattice2 cc1_lattices cc5_lattices fc6_lattice2 t4_subset cc7_lattices fc4_filter_2 dt_m2_filter_2 redefinition_m1_filter_2 dt_m1_filter_0 dt_m2_lattice4 d4_filter_2 dt_k15_filter_2 d6_filter_2 redefinition_k15_filter_2 dt_k5_filter_2 t33_filter_2 l70_filter_2 t59_filter_0
% 0.79/0.99
%------------------------------------------------------------------------------