%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LAT339+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n017.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:51:04 EDT 2022
% Result : Theorem 2.74s 2.90s
% Output : Refutation 2.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 48
% Syntax : Number of clauses : 139 ( 40 unt; 65 nHn; 139 RR)
% Number of literals : 360 ( 0 equ; 160 neg)
% Maximal clause size : 12 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 36 ( 35 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 6 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
l2_conlat_1(skc14),
file('LAT339+1.p',unknown),
[] ).
cnf(4,axiom,
l1_struct_0(skc18),
file('LAT339+1.p',unknown),
[] ).
cnf(8,axiom,
v1_xboole_0(k1_xboole_0),
file('LAT339+1.p',unknown),
[] ).
cnf(36,axiom,
~ v3_conlat_1(skc14),
file('LAT339+1.p',unknown),
[] ).
cnf(38,axiom,
v1_xboole_0(skf36(u)),
file('LAT339+1.p',unknown),
[] ).
cnf(51,axiom,
( ~ l2_conlat_1(u)
| l1_conlat_1(u) ),
file('LAT339+1.p',unknown),
[] ).
cnf(52,axiom,
( ~ l2_lattices(u)
| l1_struct_0(u) ),
file('LAT339+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ l3_lattices(u)
| l2_lattices(u) ),
file('LAT339+1.p',unknown),
[] ).
cnf(56,axiom,
m1_subset_1(skf36(u),k1_zfmisc_1(u)),
file('LAT339+1.p',unknown),
[] ).
cnf(61,axiom,
( ~ l1_struct_0(u)
| v1_xboole_0(k1_pre_topc(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ l1_struct_0(u)
| v1_membered(k1_pre_topc(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(63,axiom,
( ~ l1_struct_0(u)
| v2_membered(k1_pre_topc(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ l1_struct_0(u)
| v3_membered(k1_pre_topc(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ l1_struct_0(u)
| v4_membered(k1_pre_topc(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(66,axiom,
( ~ l1_struct_0(u)
| v5_membered(k1_pre_topc(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(74,axiom,
( ~ v1_xboole_0(u)
| equal(u,k1_xboole_0) ),
file('LAT339+1.p',unknown),
[] ).
cnf(80,axiom,
m1_subset_1(skf41(u,v,w),u1_struct_0(w)),
file('LAT339+1.p',unknown),
[] ).
cnf(81,axiom,
( ~ v1_xboole_0(u)
| ~ r2_hidden(v,u) ),
file('LAT339+1.p',unknown),
[] ).
cnf(84,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| l3_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(93,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v13_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(94,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v14_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(95,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v15_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(105,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v3_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(106,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v4_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(107,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v5_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(108,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v6_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(109,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v7_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(110,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v8_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(111,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v9_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(112,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v10_lattices(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(113,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v4_lattice3(k11_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(116,axiom,
( ~ m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w)))
| v1_relat_1(u) ),
file('LAT339+1.p',unknown),
[] ).
cnf(133,axiom,
( ~ l2_conlat_1(u)
| ~ v3_struct_0(k11_conlat_1(u))
| v3_conlat_1(u) ),
file('LAT339+1.p',unknown),
[] ).
cnf(170,axiom,
( ~ l2_lattices(u)
| v3_struct_0(u)
| m1_subset_1(k6_lattices(u),u1_struct_0(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(187,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| equal(k5_lattices(k11_conlat_1(u)),k6_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(188,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| equal(k6_lattices(k11_conlat_1(u)),k5_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(210,axiom,
( ~ l2_conlat_1(u)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| v3_conlat_1(u)
| equal(k12_conlat_1(u,v),v) ),
file('LAT339+1.p',unknown),
[] ).
cnf(212,axiom,
( ~ l2_conlat_1(u)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| v9_conlat_1(k12_conlat_1(u,v),u)
| v3_conlat_1(u) ),
file('LAT339+1.p',unknown),
[] ).
cnf(213,axiom,
( ~ l2_conlat_1(u)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| l3_conlat_1(k12_conlat_1(u,v),u)
| v3_conlat_1(u) ),
file('LAT339+1.p',unknown),
[] ).
cnf(215,axiom,
( ~ l2_conlat_1(u)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| ~ v7_conlat_1(k12_conlat_1(u,v),u)
| v3_conlat_1(u) ),
file('LAT339+1.p',unknown),
[] ).
cnf(220,axiom,
( ~ l3_lattices(u)
| ~ v4_lattice3(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| equal(k15_lattice3(u,k1_xboole_0),k5_lattices(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(221,axiom,
( ~ equal(k2_conlat_2(skc14,k1_pre_topc(k11_conlat_1(skc14))),k5_conlat_1(skc14))
| ~ equal(k3_conlat_2(skc14,k1_pre_topc(k11_conlat_1(skc14))),k6_conlat_1(skc14)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(234,axiom,
( ~ l2_conlat_1(u)
| ~ m1_subset_1(v,k1_zfmisc_1(u1_struct_0(k11_conlat_1(u))))
| v3_conlat_1(u)
| equal(k15_lattice3(k11_conlat_1(u),v),k3_conlat_2(u,v)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(235,axiom,
( ~ l2_conlat_1(u)
| ~ m1_subset_1(v,k1_zfmisc_1(u1_struct_0(k11_conlat_1(u))))
| v3_conlat_1(u)
| equal(k16_lattice3(k11_conlat_1(u),v),k2_conlat_2(u,v)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(236,axiom,
( ~ l3_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| v3_struct_0(u)
| r2_hidden(skf21(v,w,u),w)
| r3_lattice3(u,v,w) ),
file('LAT339+1.p',unknown),
[] ).
cnf(239,axiom,
( ~ l2_conlat_1(u)
| ~ l3_conlat_1(v,u)
| ~ v9_conlat_1(v,u)
| v3_conlat_1(u)
| v7_conlat_1(v,u)
| r2_conlat_1(u,v,k5_conlat_1(u)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(254,axiom,
( ~ l2_conlat_1(u)
| ~ r2_conlat_1(u,k12_conlat_1(u,v),k12_conlat_1(u,w))
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| ~ m1_subset_1(w,u1_struct_0(k11_conlat_1(u)))
| r3_lattices(k11_conlat_1(u),v,w)
| v3_conlat_1(u) ),
file('LAT339+1.p',unknown),
[] ).
cnf(259,axiom,
( ~ l3_lattices(u)
| ~ v4_lattice3(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ r3_lattice3(u,v,w)
| ~ r3_lattices(u,skf41(v,w,u),v)
| v3_struct_0(u)
| equal(v,k16_lattice3(u,w)) ),
file('LAT339+1.p',unknown),
[] ).
cnf(268,plain,
( ~ l2_conlat_1(u)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| v3_conlat_1(u)
| l3_conlat_1(v,u) ),
inference(rew,[status(thm),theory(equality)],[210,213]),
[iquote('0:Rew:210.3,213.2')] ).
cnf(269,plain,
( ~ l2_conlat_1(u)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| v3_conlat_1(u)
| v9_conlat_1(v,u) ),
inference(rew,[status(thm),theory(equality)],[210,212]),
[iquote('0:Rew:210.3,212.2')] ).
cnf(271,plain,
( ~ l2_conlat_1(u)
| ~ v7_conlat_1(v,u)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| v3_conlat_1(u) ),
inference(rew,[status(thm),theory(equality)],[210,215]),
[iquote('0:Rew:210.3,215.2')] ).
cnf(273,plain,
( ~ l2_conlat_1(u)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| ~ m1_subset_1(w,u1_struct_0(k11_conlat_1(u)))
| ~ r2_conlat_1(u,w,v)
| v3_conlat_1(u)
| r3_lattices(k11_conlat_1(u),w,v) ),
inference(rew,[status(thm),theory(equality)],[210,254]),
[iquote('0:Rew:210.3,254.1,210.3,254.1')] ).
cnf(279,plain,
( ~ v9_conlat_1(u,skc14)
| ~ l3_conlat_1(u,skc14)
| r2_conlat_1(skc14,u,k5_conlat_1(skc14))
| v3_conlat_1(skc14)
| v7_conlat_1(u,skc14) ),
inference(res,[status(thm),theory(equality)],[1,239]),
[iquote('0:Res:1.0,239.0')] ).
cnf(282,plain,
( ~ m1_subset_1(u,k1_zfmisc_1(u1_struct_0(k11_conlat_1(skc14))))
| v3_conlat_1(skc14)
| equal(k15_lattice3(k11_conlat_1(skc14),u),k3_conlat_2(skc14,u)) ),
inference(res,[status(thm),theory(equality)],[1,234]),
[iquote('0:Res:1.0,234.0')] ).
cnf(285,plain,
( ~ m1_subset_1(u,u1_struct_0(k11_conlat_1(skc14)))
| ~ v7_conlat_1(u,skc14)
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,271]),
[iquote('0:Res:1.0,271.0')] ).
cnf(291,plain,
( ~ m1_subset_1(u,u1_struct_0(k11_conlat_1(skc14)))
| v9_conlat_1(u,skc14)
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,269]),
[iquote('0:Res:1.0,269.0')] ).
cnf(292,plain,
( ~ m1_subset_1(u,u1_struct_0(k11_conlat_1(skc14)))
| l3_conlat_1(u,skc14)
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,268]),
[iquote('0:Res:1.0,268.0')] ).
cnf(294,plain,
( equal(k5_lattices(k11_conlat_1(skc14)),k6_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,187]),
[iquote('0:Res:1.0,187.0')] ).
cnf(295,plain,
( equal(k6_lattices(k11_conlat_1(skc14)),k5_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,188]),
[iquote('0:Res:1.0,188.0')] ).
cnf(310,plain,
( ~ v3_struct_0(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,133]),
[iquote('0:Res:1.0,133.0')] ).
cnf(324,plain,
( l3_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,84]),
[iquote('0:Res:1.0,84.0')] ).
cnf(325,plain,
( v13_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,93]),
[iquote('0:Res:1.0,93.0')] ).
cnf(326,plain,
( v14_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,94]),
[iquote('0:Res:1.0,94.0')] ).
cnf(327,plain,
( v15_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,95]),
[iquote('0:Res:1.0,95.0')] ).
cnf(328,plain,
( v3_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,105]),
[iquote('0:Res:1.0,105.0')] ).
cnf(329,plain,
( v4_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,106]),
[iquote('0:Res:1.0,106.0')] ).
cnf(330,plain,
( v5_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,107]),
[iquote('0:Res:1.0,107.0')] ).
cnf(331,plain,
( v6_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,108]),
[iquote('0:Res:1.0,108.0')] ).
cnf(332,plain,
( v7_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,109]),
[iquote('0:Res:1.0,109.0')] ).
cnf(333,plain,
( v8_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,110]),
[iquote('0:Res:1.0,110.0')] ).
cnf(334,plain,
( v9_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,111]),
[iquote('0:Res:1.0,111.0')] ).
cnf(335,plain,
( v10_lattices(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,112]),
[iquote('0:Res:1.0,112.0')] ).
cnf(336,plain,
( v4_lattice3(k11_conlat_1(skc14))
| v3_conlat_1(skc14) ),
inference(res,[status(thm),theory(equality)],[1,113]),
[iquote('0:Res:1.0,113.0')] ).
cnf(337,plain,
l1_conlat_1(skc14),
inference(res,[status(thm),theory(equality)],[1,51]),
[iquote('0:Res:1.0,51.0')] ).
cnf(410,plain,
l3_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[324,36]),
[iquote('0:MRR:324.1,36.0')] ).
cnf(411,plain,
v13_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[325,36]),
[iquote('0:MRR:325.1,36.0')] ).
cnf(412,plain,
v14_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[326,36]),
[iquote('0:MRR:326.1,36.0')] ).
cnf(413,plain,
v15_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[327,36]),
[iquote('0:MRR:327.1,36.0')] ).
cnf(414,plain,
v3_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[328,36]),
[iquote('0:MRR:328.1,36.0')] ).
cnf(415,plain,
v4_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[329,36]),
[iquote('0:MRR:329.1,36.0')] ).
cnf(416,plain,
v5_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[330,36]),
[iquote('0:MRR:330.1,36.0')] ).
cnf(417,plain,
v6_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[331,36]),
[iquote('0:MRR:331.1,36.0')] ).
cnf(418,plain,
v7_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[332,36]),
[iquote('0:MRR:332.1,36.0')] ).
cnf(419,plain,
v8_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[333,36]),
[iquote('0:MRR:333.1,36.0')] ).
cnf(420,plain,
v9_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[334,36]),
[iquote('0:MRR:334.1,36.0')] ).
cnf(421,plain,
v10_lattices(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[335,36]),
[iquote('0:MRR:335.1,36.0')] ).
cnf(422,plain,
v4_lattice3(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[336,36]),
[iquote('0:MRR:336.1,36.0')] ).
cnf(431,plain,
~ v3_struct_0(k11_conlat_1(skc14)),
inference(mrr,[status(thm)],[310,36]),
[iquote('0:MRR:310.1,36.0')] ).
cnf(460,plain,
equal(k5_lattices(k11_conlat_1(skc14)),k6_conlat_1(skc14)),
inference(mrr,[status(thm)],[294,36]),
[iquote('0:MRR:294.1,36.0')] ).
cnf(461,plain,
equal(k6_lattices(k11_conlat_1(skc14)),k5_conlat_1(skc14)),
inference(mrr,[status(thm)],[295,36]),
[iquote('0:MRR:295.1,36.0')] ).
cnf(464,plain,
( ~ m1_subset_1(u,u1_struct_0(k11_conlat_1(skc14)))
| v9_conlat_1(u,skc14) ),
inference(mrr,[status(thm)],[291,36]),
[iquote('0:MRR:291.2,36.0')] ).
cnf(465,plain,
( ~ m1_subset_1(u,u1_struct_0(k11_conlat_1(skc14)))
| l3_conlat_1(u,skc14) ),
inference(mrr,[status(thm)],[292,36]),
[iquote('0:MRR:292.2,36.0')] ).
cnf(466,plain,
( ~ v7_conlat_1(u,skc14)
| ~ m1_subset_1(u,u1_struct_0(k11_conlat_1(skc14))) ),
inference(mrr,[status(thm)],[285,36]),
[iquote('0:MRR:285.2,36.0')] ).
cnf(475,plain,
( ~ m1_subset_1(u,k1_zfmisc_1(u1_struct_0(k11_conlat_1(skc14))))
| equal(k15_lattice3(k11_conlat_1(skc14),u),k3_conlat_2(skc14,u)) ),
inference(mrr,[status(thm)],[282,36]),
[iquote('0:MRR:282.1,36.0')] ).
cnf(476,plain,
( ~ l3_conlat_1(u,skc14)
| ~ v9_conlat_1(u,skc14)
| v7_conlat_1(u,skc14)
| r2_conlat_1(skc14,u,k5_conlat_1(skc14)) ),
inference(mrr,[status(thm)],[279,36]),
[iquote('0:MRR:279.3,36.0')] ).
cnf(484,plain,
equal(skf36(u),k1_xboole_0),
inference(ems,[status(thm)],[74,38]),
[iquote('0:EmS:74.0,38.0')] ).
cnf(489,plain,
m1_subset_1(k1_xboole_0,k1_zfmisc_1(u)),
inference(rew,[status(thm),theory(equality)],[484,56]),
[iquote('0:Rew:484.0,56.0')] ).
cnf(492,plain,
( ~ l1_struct_0(u)
| equal(k1_pre_topc(u),k1_xboole_0) ),
inference(ems,[status(thm)],[74,61]),
[iquote('0:EmS:74.0,61.1')] ).
cnf(493,plain,
( ~ l1_struct_0(u)
| v5_membered(k1_xboole_0) ),
inference(rew,[status(thm),theory(equality)],[492,66]),
[iquote('0:Rew:492.1,66.1')] ).
cnf(494,plain,
( ~ l1_struct_0(u)
| v4_membered(k1_xboole_0) ),
inference(rew,[status(thm),theory(equality)],[492,65]),
[iquote('0:Rew:492.1,65.1')] ).
cnf(495,plain,
( ~ l1_struct_0(u)
| v3_membered(k1_xboole_0) ),
inference(rew,[status(thm),theory(equality)],[492,64]),
[iquote('0:Rew:492.1,64.1')] ).
cnf(496,plain,
( ~ l1_struct_0(u)
| v2_membered(k1_xboole_0) ),
inference(rew,[status(thm),theory(equality)],[492,63]),
[iquote('0:Rew:492.1,63.1')] ).
cnf(497,plain,
( ~ l1_struct_0(u)
| v1_membered(k1_xboole_0) ),
inference(rew,[status(thm),theory(equality)],[492,62]),
[iquote('0:Rew:492.1,62.1')] ).
cnf(502,plain,
v5_membered(k1_xboole_0),
inference(ems,[status(thm)],[493,4]),
[iquote('0:EmS:493.0,4.0')] ).
cnf(506,plain,
v4_membered(k1_xboole_0),
inference(ems,[status(thm)],[494,4]),
[iquote('0:EmS:494.0,4.0')] ).
cnf(510,plain,
v3_membered(k1_xboole_0),
inference(ems,[status(thm)],[495,4]),
[iquote('0:EmS:495.0,4.0')] ).
cnf(514,plain,
v2_membered(k1_xboole_0),
inference(ems,[status(thm)],[496,4]),
[iquote('0:EmS:496.0,4.0')] ).
cnf(518,plain,
v1_membered(k1_xboole_0),
inference(ems,[status(thm)],[497,4]),
[iquote('0:EmS:497.0,4.0')] ).
cnf(535,plain,
v9_conlat_1(skf41(u,v,k11_conlat_1(skc14)),skc14),
inference(res,[status(thm),theory(equality)],[80,464]),
[iquote('0:Res:80.0,464.0')] ).
cnf(539,plain,
l3_conlat_1(skf41(u,v,k11_conlat_1(skc14)),skc14),
inference(res,[status(thm),theory(equality)],[80,465]),
[iquote('0:Res:80.0,465.0')] ).
cnf(544,plain,
v1_relat_1(k1_xboole_0),
inference(res,[status(thm),theory(equality)],[489,116]),
[iquote('0:Res:489.0,116.0')] ).
cnf(586,plain,
( ~ l2_lattices(k11_conlat_1(skc14))
| v3_struct_0(k11_conlat_1(skc14))
| m1_subset_1(k5_conlat_1(skc14),u1_struct_0(k11_conlat_1(skc14))) ),
inference(spr,[status(thm),theory(equality)],[461,170]),
[iquote('0:SpR:461.0,170.2')] ).
cnf(594,plain,
( v3_struct_0(k11_conlat_1(skc14))
| m1_subset_1(k5_conlat_1(skc14),u1_struct_0(k11_conlat_1(skc14))) ),
inference(ssi,[status(thm)],[586,54,412,413,411,422,414,420,419,418,416,415,417,421,410]),
[iquote('0:SSi:586.0,54.0,412.0,413.0,411.0,422.0,414.0,420.0,419.0,418.0,416.0,415.0,417.0,421.0,410.1')] ).
cnf(595,plain,
m1_subset_1(k5_conlat_1(skc14),u1_struct_0(k11_conlat_1(skc14))),
inference(mrr,[status(thm)],[594,431]),
[iquote('0:MRR:594.0,431.0')] ).
cnf(776,plain,
~ v7_conlat_1(skf41(u,v,k11_conlat_1(skc14)),skc14),
inference(res,[status(thm),theory(equality)],[80,466]),
[iquote('0:Res:80.0,466.1')] ).
cnf(1665,plain,
( ~ l1_struct_0(k11_conlat_1(skc14))
| ~ equal(k2_conlat_2(skc14,k1_xboole_0),k5_conlat_1(skc14))
| ~ equal(k3_conlat_2(skc14,k1_pre_topc(k11_conlat_1(skc14))),k6_conlat_1(skc14)) ),
inference(spl,[status(thm),theory(equality)],[492,221]),
[iquote('0:SpL:492.1,221.0')] ).
cnf(1666,plain,
( ~ l1_struct_0(k11_conlat_1(skc14))
| ~ equal(k2_conlat_2(skc14,k1_xboole_0),k5_conlat_1(skc14))
| ~ equal(k3_conlat_2(skc14,k1_xboole_0),k6_conlat_1(skc14)) ),
inference(rew,[status(thm),theory(equality)],[492,1665]),
[iquote('0:Rew:492.1,1665.2')] ).
cnf(1667,plain,
( ~ equal(k2_conlat_2(skc14,k1_xboole_0),k5_conlat_1(skc14))
| ~ equal(k3_conlat_2(skc14,k1_xboole_0),k6_conlat_1(skc14)) ),
inference(ssi,[status(thm)],[1666,54,52,412,413,411,422,414,420,419,418,416,415,417,421,410]),
[iquote('0:SSi:1666.0,54.0,52.0,412.0,413.0,411.0,422.0,414.0,420.0,419.0,418.0,416.0,415.0,417.0,421.1,410.1')] ).
cnf(1798,plain,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| equal(k16_lattice3(k11_conlat_1(u),k1_xboole_0),k2_conlat_2(u,k1_xboole_0)) ),
inference(res,[status(thm),theory(equality)],[489,235]),
[iquote('0:Res:489.0,235.1')] ).
cnf(1971,plain,
( ~ l3_lattices(u)
| ~ v1_xboole_0(v)
| ~ m1_subset_1(w,u1_struct_0(u))
| v3_struct_0(u)
| r3_lattice3(u,w,v) ),
inference(res,[status(thm),theory(equality)],[236,81]),
[iquote('0:Res:236.3,81.1')] ).
cnf(2684,plain,
( ~ l2_conlat_1(u)
| ~ l3_lattices(k11_conlat_1(u))
| ~ v4_lattice3(k11_conlat_1(u))
| ~ v10_lattices(k11_conlat_1(u))
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| ~ m1_subset_1(skf41(v,w,k11_conlat_1(u)),u1_struct_0(k11_conlat_1(u)))
| ~ r2_conlat_1(u,skf41(v,w,k11_conlat_1(u)),v)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| ~ r3_lattice3(k11_conlat_1(u),v,w)
| v3_conlat_1(u)
| v3_struct_0(k11_conlat_1(u))
| equal(v,k16_lattice3(k11_conlat_1(u),w)) ),
inference(res,[status(thm),theory(equality)],[273,259]),
[iquote('0:Res:273.5,259.5')] ).
cnf(2688,plain,
( ~ l2_conlat_1(u)
| ~ l3_lattices(k11_conlat_1(u))
| ~ v4_lattice3(k11_conlat_1(u))
| ~ v10_lattices(k11_conlat_1(u))
| ~ m1_subset_1(skf41(v,w,k11_conlat_1(u)),u1_struct_0(k11_conlat_1(u)))
| ~ r2_conlat_1(u,skf41(v,w,k11_conlat_1(u)),v)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| ~ r3_lattice3(k11_conlat_1(u),v,w)
| v3_conlat_1(u)
| v3_struct_0(k11_conlat_1(u))
| equal(v,k16_lattice3(k11_conlat_1(u),w)) ),
inference(obv,[status(thm),theory(equality)],[2684]),
[iquote('0:Obv:2684.4')] ).
cnf(2689,plain,
( ~ l2_conlat_1(u)
| ~ r2_conlat_1(u,skf41(v,w,k11_conlat_1(u)),v)
| ~ m1_subset_1(v,u1_struct_0(k11_conlat_1(u)))
| ~ r3_lattice3(k11_conlat_1(u),v,w)
| v3_conlat_1(u)
| equal(v,k16_lattice3(k11_conlat_1(u),w)) ),
inference(mrr,[status(thm)],[2688,84,113,112,80,133]),
[iquote('0:MRR:2688.1,2688.2,2688.3,2688.4,2688.9,84.2,113.2,112.2,80.0,133.1')] ).
cnf(4966,plain,
equal(k15_lattice3(k11_conlat_1(skc14),k1_xboole_0),k3_conlat_2(skc14,k1_xboole_0)),
inference(res,[status(thm),theory(equality)],[489,475]),
[iquote('0:Res:489.0,475.0')] ).
cnf(4972,plain,
( ~ l3_lattices(k11_conlat_1(skc14))
| ~ v4_lattice3(k11_conlat_1(skc14))
| ~ v10_lattices(k11_conlat_1(skc14))
| v3_struct_0(k11_conlat_1(skc14))
| equal(k3_conlat_2(skc14,k1_xboole_0),k5_lattices(k11_conlat_1(skc14))) ),
inference(spr,[status(thm),theory(equality)],[4966,220]),
[iquote('0:SpR:4966.0,220.4')] ).
cnf(4988,plain,
( ~ l3_lattices(k11_conlat_1(skc14))
| ~ v4_lattice3(k11_conlat_1(skc14))
| ~ v10_lattices(k11_conlat_1(skc14))
| v3_struct_0(k11_conlat_1(skc14))
| equal(k3_conlat_2(skc14,k1_xboole_0),k6_conlat_1(skc14)) ),
inference(rew,[status(thm),theory(equality)],[460,4972]),
[iquote('0:Rew:460.0,4972.4')] ).
cnf(4989,plain,
( v3_struct_0(k11_conlat_1(skc14))
| equal(k3_conlat_2(skc14,k1_xboole_0),k6_conlat_1(skc14)) ),
inference(ssi,[status(thm)],[4988,412,413,411,422,414,420,419,418,416,415,417,421,410]),
[iquote('0:SSi:4988.2,4988.1,4988.0,412.0,413.0,411.0,422.0,414.0,420.0,419.0,418.0,416.0,415.0,417.0,421.0,410.0,412.0,413.0,411.0,422.0,414.0,420.0,419.0,418.0,416.0,415.0,417.0,421.0,410.0,412.0,413.0,411.0,422.0,414.0,420.0,419.0,418.0,416.0,415.0,417.0,421.0,410.0')] ).
cnf(4990,plain,
equal(k3_conlat_2(skc14,k1_xboole_0),k6_conlat_1(skc14)),
inference(mrr,[status(thm)],[4989,431]),
[iquote('0:MRR:4989.0,431.0')] ).
cnf(4997,plain,
( ~ equal(k2_conlat_2(skc14,k1_xboole_0),k5_conlat_1(skc14))
| ~ equal(k6_conlat_1(skc14),k6_conlat_1(skc14)) ),
inference(rew,[status(thm),theory(equality)],[4990,1667]),
[iquote('0:Rew:4990.0,1667.1')] ).
cnf(5000,plain,
~ equal(k2_conlat_2(skc14,k1_xboole_0),k5_conlat_1(skc14)),
inference(obv,[status(thm),theory(equality)],[4997]),
[iquote('0:Obv:4997.1')] ).
cnf(9430,plain,
( ~ l2_conlat_1(skc14)
| ~ l3_conlat_1(skf41(k5_conlat_1(skc14),u,k11_conlat_1(skc14)),skc14)
| ~ v9_conlat_1(skf41(k5_conlat_1(skc14),u,k11_conlat_1(skc14)),skc14)
| ~ m1_subset_1(k5_conlat_1(skc14),u1_struct_0(k11_conlat_1(skc14)))
| ~ r3_lattice3(k11_conlat_1(skc14),k5_conlat_1(skc14),u)
| v7_conlat_1(skf41(k5_conlat_1(skc14),u,k11_conlat_1(skc14)),skc14)
| v3_conlat_1(skc14)
| equal(k16_lattice3(k11_conlat_1(skc14),u),k5_conlat_1(skc14)) ),
inference(res,[status(thm),theory(equality)],[476,2689]),
[iquote('0:Res:476.3,2689.1')] ).
cnf(9431,plain,
( ~ l3_conlat_1(skf41(k5_conlat_1(skc14),u,k11_conlat_1(skc14)),skc14)
| ~ v9_conlat_1(skf41(k5_conlat_1(skc14),u,k11_conlat_1(skc14)),skc14)
| ~ m1_subset_1(k5_conlat_1(skc14),u1_struct_0(k11_conlat_1(skc14)))
| ~ r3_lattice3(k11_conlat_1(skc14),k5_conlat_1(skc14),u)
| v7_conlat_1(skf41(k5_conlat_1(skc14),u,k11_conlat_1(skc14)),skc14)
| v3_conlat_1(skc14)
| equal(k16_lattice3(k11_conlat_1(skc14),u),k5_conlat_1(skc14)) ),
inference(ssi,[status(thm)],[9430,1,337]),
[iquote('0:SSi:9430.0,1.0,337.0')] ).
cnf(9432,plain,
( ~ r3_lattice3(k11_conlat_1(skc14),k5_conlat_1(skc14),u)
| equal(k16_lattice3(k11_conlat_1(skc14),u),k5_conlat_1(skc14)) ),
inference(mrr,[status(thm)],[9431,539,535,595,776,36]),
[iquote('0:MRR:9431.0,9431.1,9431.2,9431.4,9431.5,539.0,535.0,595.0,776.0,36.0')] ).
cnf(9436,plain,
( ~ l3_lattices(k11_conlat_1(skc14))
| ~ v1_xboole_0(u)
| ~ m1_subset_1(k5_conlat_1(skc14),u1_struct_0(k11_conlat_1(skc14)))
| v3_struct_0(k11_conlat_1(skc14))
| equal(k16_lattice3(k11_conlat_1(skc14),u),k5_conlat_1(skc14)) ),
inference(res,[status(thm),theory(equality)],[1971,9432]),
[iquote('0:Res:1971.4,9432.0')] ).
cnf(9437,plain,
( ~ v1_xboole_0(u)
| ~ m1_subset_1(k5_conlat_1(skc14),u1_struct_0(k11_conlat_1(skc14)))
| v3_struct_0(k11_conlat_1(skc14))
| equal(k16_lattice3(k11_conlat_1(skc14),u),k5_conlat_1(skc14)) ),
inference(ssi,[status(thm)],[9436,412,413,411,422,414,420,419,418,416,415,417,421,410]),
[iquote('0:SSi:9436.0,412.0,413.0,411.0,422.0,414.0,420.0,419.0,418.0,416.0,415.0,417.0,421.0,410.0')] ).
cnf(9438,plain,
( ~ v1_xboole_0(u)
| equal(k16_lattice3(k11_conlat_1(skc14),u),k5_conlat_1(skc14)) ),
inference(mrr,[status(thm)],[9437,595,431]),
[iquote('0:MRR:9437.1,9437.2,595.0,431.0')] ).
cnf(9456,plain,
( ~ v1_xboole_0(k1_xboole_0)
| ~ l2_conlat_1(skc14)
| v3_conlat_1(skc14)
| equal(k2_conlat_2(skc14,k1_xboole_0),k5_conlat_1(skc14)) ),
inference(spr,[status(thm),theory(equality)],[9438,1798]),
[iquote('0:SpR:9438.1,1798.2')] ).
cnf(9466,plain,
( v3_conlat_1(skc14)
| equal(k2_conlat_2(skc14,k1_xboole_0),k5_conlat_1(skc14)) ),
inference(ssi,[status(thm)],[9456,1,337,8,502,506,510,514,518,544]),
[iquote('0:SSi:9456.1,9456.0,1.0,337.0,8.0,502.0,506.0,510.0,514.0,518.0,544.0')] ).
cnf(9467,plain,
$false,
inference(mrr,[status(thm)],[9466,36,5000]),
[iquote('0:MRR:9466.0,9466.1,36.0,5000.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : LAT339+1 : TPTP v8.1.0. Released v3.4.0.
% 0.04/0.13 % Command : run_spass %d %s
% 0.14/0.34 % Computer : n017.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Thu Jun 30 05:05:38 EDT 2022
% 0.14/0.34 % CPUTime :
% 2.74/2.90
% 2.74/2.90 SPASS V 3.9
% 2.74/2.90 SPASS beiseite: Proof found.
% 2.74/2.90 % SZS status Theorem
% 2.74/2.90 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.74/2.90 SPASS derived 7385 clauses, backtracked 499 clauses, performed 8 splits and kept 4112 clauses.
% 2.74/2.90 SPASS allocated 106309 KBytes.
% 2.74/2.90 SPASS spent 0:00:02.55 on the problem.
% 2.74/2.90 0:00:00.04 for the input.
% 2.74/2.90 0:00:00.10 for the FLOTTER CNF translation.
% 2.74/2.90 0:00:00.14 for inferences.
% 2.74/2.90 0:00:00.03 for the backtracking.
% 2.74/2.90 0:00:02.13 for the reduction.
% 2.74/2.90
% 2.74/2.90
% 2.74/2.90 Here is a proof with depth 4, length 139 :
% 2.74/2.90 % SZS output start Refutation
% See solution above
% 2.74/2.90 Formulae used in the proof : t5_conlat_2 existence_l1_struct_0 fc1_xboole_0 rc2_subset_1 dt_l2_conlat_1 dt_l2_lattices dt_l3_lattices fc1_pre_topc t6_boole t34_lattice3 existence_m1_subset_1 t7_boole dt_k11_conlat_1 fc1_conlat_2 fc5_conlat_1 cc1_relset_1 dt_k6_lattices t1_conlat_2 d24_conlat_1 dt_k12_conlat_1 t50_lattice3 d3_conlat_2 d2_conlat_2 d16_lattice3 t34_conlat_1 t47_conlat_1
% 2.80/2.96
%------------------------------------------------------------------------------