%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LAT343+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n003.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:08 EDT 2022
% Result : Theorem 4.87s 5.05s
% Output : Refutation 5.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 58
% Syntax : Number of clauses : 261 ( 78 unt; 108 nHn; 261 RR)
% Number of literals : 719 ( 0 equ; 378 neg)
% Maximal clause size : 11 ( 2 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 34 ( 33 usr; 1 prp; 0-3 aty)
% Number of functors : 28 ( 28 usr; 9 con; 0-4 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
l2_conlat_1(skc16),
file('LAT343+1.p',unknown),
[] ).
cnf(36,axiom,
~ v3_conlat_1(skc16),
file('LAT343+1.p',unknown),
[] ).
cnf(44,axiom,
m1_subset_1(skc18,u2_conlat_1(skc16)),
file('LAT343+1.p',unknown),
[] ).
cnf(45,axiom,
m1_subset_1(skc17,u1_conlat_1(skc16)),
file('LAT343+1.p',unknown),
[] ).
cnf(46,axiom,
m1_subset_1(skf18(u),u),
file('LAT343+1.p',unknown),
[] ).
cnf(53,axiom,
( ~ l2_conlat_1(u)
| l1_conlat_1(u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ l2_lattices(u)
| l1_struct_0(u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(56,axiom,
( ~ l3_lattices(u)
| l2_lattices(u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(57,axiom,
m1_subset_1(skf22(u),k1_zfmisc_1(u)),
file('LAT343+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ v1_xboole_0(skf22(u))
| v1_xboole_0(u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ v1_xboole_0(u)
| ~ r2_hidden(v,u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(75,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v1_funct_1(k10_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(77,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| l3_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(78,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v1_funct_1(k4_conlat_2(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v1_funct_1(k5_conlat_2(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(80,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v1_funct_1(k9_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(89,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v13_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(90,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v14_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(91,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v15_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(101,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v3_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(102,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v4_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(103,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v5_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(104,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v6_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(105,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v7_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(106,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v8_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(107,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v9_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(108,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v10_lattices(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(109,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v4_lattice3(k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(112,axiom,
( ~ m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w)))
| v1_relat_1(u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(115,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| m1_conlat_1(k8_conlat_1(u),u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(116,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| m1_conlat_1(skf16(u),u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(117,axiom,
( ~ l1_conlat_1(u)
| ~ v1_xboole_0(u2_conlat_1(u))
| v3_conlat_1(u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(119,axiom,
( ~ l1_struct_0(u)
| ~ v1_xboole_0(u1_struct_0(u))
| v3_struct_0(u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(120,axiom,
( ~ l1_conlat_1(u)
| ~ v1_xboole_0(u1_conlat_1(u))
| v3_conlat_1(u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(124,axiom,
( ~ l2_conlat_1(u)
| ~ v3_struct_0(k11_conlat_1(u))
| v3_conlat_1(u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(130,axiom,
( ~ m2_relset_1(u,v,w)
| m1_relset_1(u,v,w) ),
file('LAT343+1.p',unknown),
[] ).
cnf(132,axiom,
( ~ m1_subset_1(u,v)
| v1_xboole_0(v)
| r2_hidden(u,v) ),
file('LAT343+1.p',unknown),
[] ).
cnf(144,axiom,
( ~ m2_relset_1(u,v,w)
| m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w))) ),
file('LAT343+1.p',unknown),
[] ).
cnf(153,axiom,
( ~ v1_xboole_0(u)
| ~ l2_conlat_1(v)
| ~ m1_conlat_1(u,v)
| v3_conlat_1(v) ),
file('LAT343+1.p',unknown),
[] ).
cnf(154,axiom,
( ~ r2_hidden(u,v)
| ~ m1_subset_1(v,k1_zfmisc_1(w))
| m1_subset_1(u,w) ),
file('LAT343+1.p',unknown),
[] ).
cnf(158,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v1_funct_2(k4_conlat_2(u),u1_conlat_1(u),u1_struct_0(k11_conlat_1(u))) ),
file('LAT343+1.p',unknown),
[] ).
cnf(159,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| m2_relset_1(k4_conlat_2(u),u1_conlat_1(u),u1_struct_0(k11_conlat_1(u))) ),
file('LAT343+1.p',unknown),
[] ).
cnf(160,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v1_funct_2(k5_conlat_2(u),u2_conlat_1(u),u1_struct_0(k11_conlat_1(u))) ),
file('LAT343+1.p',unknown),
[] ).
cnf(161,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| m2_relset_1(k5_conlat_2(u),u2_conlat_1(u),u1_struct_0(k11_conlat_1(u))) ),
file('LAT343+1.p',unknown),
[] ).
cnf(170,axiom,
( ~ v3_lattices(u)
| ~ l3_lattices(u)
| equal(g3_lattices(u1_struct_0(u),u2_lattices(u),u1_lattices(u)),u) ),
file('LAT343+1.p',unknown),
[] ).
cnf(172,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| equal(g3_lattices(k8_conlat_1(u),k10_conlat_1(u),k9_conlat_1(u)),k11_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(173,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v1_funct_2(k10_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(174,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| m2_relset_1(k10_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(175,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| v1_funct_2(k9_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(176,axiom,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| m2_relset_1(k9_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(178,axiom,
( ~ l2_conlat_1(u)
| ~ r2_hidden(v,w)
| ~ m1_conlat_1(w,u)
| v9_conlat_1(v,u)
| v3_conlat_1(u)
| v1_xboole_0(w) ),
file('LAT343+1.p',unknown),
[] ).
cnf(179,axiom,
( ~ l2_conlat_1(u)
| ~ r2_hidden(v,w)
| ~ m1_conlat_1(w,u)
| l3_conlat_1(v,u)
| v3_conlat_1(u)
| v1_xboole_0(w) ),
file('LAT343+1.p',unknown),
[] ).
cnf(188,axiom,
( ~ v1_funct_1(u)
| ~ m1_relset_1(u,v,w)
| ~ v1_funct_2(u,v,w)
| v1_xboole_0(w)
| v1_partfun1(u,v,w) ),
file('LAT343+1.p',unknown),
[] ).
cnf(189,axiom,
( ~ l2_conlat_1(u)
| ~ m1_conlat_1(v,u)
| ~ r2_hidden(w,v)
| ~ v7_conlat_1(w,u)
| v3_conlat_1(u)
| v1_xboole_0(v) ),
file('LAT343+1.p',unknown),
[] ).
cnf(193,axiom,
( ~ v1_funct_1(u)
| ~ m1_relset_1(u,v,w)
| ~ v1_funct_2(u,v,w)
| ~ m1_subset_1(x,v)
| m1_subset_1(k8_funct_2(v,w,u,x),w)
| v1_xboole_0(v) ),
file('LAT343+1.p',unknown),
[] ).
cnf(195,axiom,
( ~ v1_funct_1(u)
| ~ m1_subset_1(v,w)
| ~ v1_funct_2(u,w,x)
| ~ m1_relset_1(u,w,x)
| v1_xboole_0(w)
| equal(k8_funct_2(w,x,u,v),k1_funct_1(u,v)) ),
file('LAT343+1.p',unknown),
[] ).
cnf(202,axiom,
( ~ v1_funct_1(u)
| ~ v1_funct_1(v)
| ~ equal(g3_lattices(w,v,u),g3_lattices(x,y,z))
| ~ m1_relset_1(v,k2_zfmisc_1(w,w),w)
| ~ v1_funct_2(v,k2_zfmisc_1(w,w),w)
| ~ m1_relset_1(u,k2_zfmisc_1(w,w),w)
| ~ v1_funct_2(u,k2_zfmisc_1(w,w),w)
| equal(w,x) ),
file('LAT343+1.p',unknown),
[] ).
cnf(203,axiom,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v7_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16) ),
file('LAT343+1.p',unknown),
[] ).
cnf(205,plain,
( ~ l2_conlat_1(u)
| ~ m1_conlat_1(v,u)
| ~ r2_hidden(w,v)
| v3_conlat_1(u)
| l3_conlat_1(w,u) ),
inference(mrr,[status(thm)],[179,153]),
[iquote('0:MRR:179.5,153.1')] ).
cnf(206,plain,
( ~ l2_conlat_1(u)
| ~ m1_conlat_1(v,u)
| ~ r2_hidden(w,v)
| v3_conlat_1(u)
| v9_conlat_1(w,u) ),
inference(mrr,[status(thm)],[178,153]),
[iquote('0:MRR:178.5,153.1')] ).
cnf(207,plain,
( ~ l2_conlat_1(u)
| ~ v7_conlat_1(v,u)
| ~ r2_hidden(v,w)
| ~ m1_conlat_1(w,u)
| v3_conlat_1(u) ),
inference(mrr,[status(thm)],[189,153]),
[iquote('0:MRR:189.5,153.1')] ).
cnf(208,plain,
( ~ v1_funct_1(u)
| ~ m1_subset_1(v,w)
| ~ v1_funct_2(u,w,x)
| ~ m1_relset_1(u,w,x)
| v1_xboole_0(w)
| m1_subset_1(k1_funct_1(u,v),x) ),
inference(rew,[status(thm),theory(equality)],[195,193]),
[iquote('0:Rew:195.4,193.4')] ).
cnf(211,plain,
( ~ r2_hidden(u,v)
| ~ m1_conlat_1(v,skc16)
| v9_conlat_1(u,skc16)
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,206]),
[iquote('0:Res:1.0,206.0')] ).
cnf(212,plain,
( ~ r2_hidden(u,v)
| ~ m1_conlat_1(v,skc16)
| l3_conlat_1(u,skc16)
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,205]),
[iquote('0:Res:1.0,205.0')] ).
cnf(214,plain,
( v3_conlat_1(skc16)
| equal(g3_lattices(k8_conlat_1(skc16),k10_conlat_1(skc16),k9_conlat_1(skc16)),k11_conlat_1(skc16)) ),
inference(res,[status(thm),theory(equality)],[1,172]),
[iquote('0:Res:1.0,172.0')] ).
cnf(215,plain,
( v1_funct_2(k10_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,173]),
[iquote('0:Res:1.0,173.0')] ).
cnf(216,plain,
( m2_relset_1(k10_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,174]),
[iquote('0:Res:1.0,174.0')] ).
cnf(217,plain,
( v1_funct_2(k9_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,175]),
[iquote('0:Res:1.0,175.0')] ).
cnf(218,plain,
( m2_relset_1(k9_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,176]),
[iquote('0:Res:1.0,176.0')] ).
cnf(219,plain,
( v1_funct_2(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,158]),
[iquote('0:Res:1.0,158.0')] ).
cnf(220,plain,
( m2_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,159]),
[iquote('0:Res:1.0,159.0')] ).
cnf(221,plain,
( v1_funct_2(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,160]),
[iquote('0:Res:1.0,160.0')] ).
cnf(222,plain,
( m2_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,161]),
[iquote('0:Res:1.0,161.0')] ).
cnf(223,plain,
( ~ v1_xboole_0(u)
| ~ m1_conlat_1(u,skc16)
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,153]),
[iquote('0:Res:1.0,153.0')] ).
cnf(227,plain,
( v3_conlat_1(skc16)
| m1_conlat_1(k8_conlat_1(skc16),skc16) ),
inference(res,[status(thm),theory(equality)],[1,115]),
[iquote('0:Res:1.0,115.0')] ).
cnf(228,plain,
( v3_conlat_1(skc16)
| m1_conlat_1(skf16(skc16),skc16) ),
inference(res,[status(thm),theory(equality)],[1,116]),
[iquote('0:Res:1.0,116.0')] ).
cnf(229,plain,
( ~ v3_struct_0(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,124]),
[iquote('0:Res:1.0,124.0')] ).
cnf(232,plain,
( v1_funct_1(k10_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,75]),
[iquote('0:Res:1.0,75.0')] ).
cnf(233,plain,
( l3_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,77]),
[iquote('0:Res:1.0,77.0')] ).
cnf(234,plain,
( v1_funct_1(k4_conlat_2(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,78]),
[iquote('0:Res:1.0,78.0')] ).
cnf(235,plain,
( v1_funct_1(k5_conlat_2(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,79]),
[iquote('0:Res:1.0,79.0')] ).
cnf(236,plain,
( v1_funct_1(k9_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,80]),
[iquote('0:Res:1.0,80.0')] ).
cnf(237,plain,
( v13_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,89]),
[iquote('0:Res:1.0,89.0')] ).
cnf(238,plain,
( v14_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,90]),
[iquote('0:Res:1.0,90.0')] ).
cnf(239,plain,
( v15_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,91]),
[iquote('0:Res:1.0,91.0')] ).
cnf(240,plain,
( v3_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,101]),
[iquote('0:Res:1.0,101.0')] ).
cnf(241,plain,
( v4_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,102]),
[iquote('0:Res:1.0,102.0')] ).
cnf(242,plain,
( v5_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,103]),
[iquote('0:Res:1.0,103.0')] ).
cnf(243,plain,
( v6_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,104]),
[iquote('0:Res:1.0,104.0')] ).
cnf(244,plain,
( v7_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,105]),
[iquote('0:Res:1.0,105.0')] ).
cnf(245,plain,
( v8_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,106]),
[iquote('0:Res:1.0,106.0')] ).
cnf(246,plain,
( v9_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,107]),
[iquote('0:Res:1.0,107.0')] ).
cnf(247,plain,
( v10_lattices(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,108]),
[iquote('0:Res:1.0,108.0')] ).
cnf(248,plain,
( v4_lattice3(k11_conlat_1(skc16))
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[1,109]),
[iquote('0:Res:1.0,109.0')] ).
cnf(249,plain,
l1_conlat_1(skc16),
inference(res,[status(thm),theory(equality)],[1,53]),
[iquote('0:Res:1.0,53.0')] ).
cnf(270,plain,
( ~ l1_conlat_1(skc16)
| ~ v1_xboole_0(u2_conlat_1(skc16)) ),
inference(res,[status(thm),theory(equality)],[117,36]),
[iquote('0:Res:117.2,36.0')] ).
cnf(271,plain,
( ~ l1_conlat_1(skc16)
| ~ v1_xboole_0(u1_conlat_1(skc16)) ),
inference(res,[status(thm),theory(equality)],[120,36]),
[iquote('0:Res:120.2,36.0')] ).
cnf(294,plain,
( r2_hidden(skc17,u1_conlat_1(skc16))
| v1_xboole_0(u1_conlat_1(skc16)) ),
inference(res,[status(thm),theory(equality)],[45,132]),
[iquote('0:Res:45.0,132.0')] ).
cnf(297,plain,
( r2_hidden(skc18,u2_conlat_1(skc16))
| v1_xboole_0(u2_conlat_1(skc16)) ),
inference(res,[status(thm),theory(equality)],[44,132]),
[iquote('0:Res:44.0,132.0')] ).
cnf(300,plain,
v1_funct_1(k10_conlat_1(skc16)),
inference(mrr,[status(thm)],[232,36]),
[iquote('0:MRR:232.1,36.0')] ).
cnf(301,plain,
l3_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[233,36]),
[iquote('0:MRR:233.1,36.0')] ).
cnf(302,plain,
v1_funct_1(k4_conlat_2(skc16)),
inference(mrr,[status(thm)],[234,36]),
[iquote('0:MRR:234.1,36.0')] ).
cnf(303,plain,
v1_funct_1(k5_conlat_2(skc16)),
inference(mrr,[status(thm)],[235,36]),
[iquote('0:MRR:235.1,36.0')] ).
cnf(304,plain,
v1_funct_1(k9_conlat_1(skc16)),
inference(mrr,[status(thm)],[236,36]),
[iquote('0:MRR:236.1,36.0')] ).
cnf(305,plain,
v13_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[237,36]),
[iquote('0:MRR:237.1,36.0')] ).
cnf(306,plain,
v14_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[238,36]),
[iquote('0:MRR:238.1,36.0')] ).
cnf(307,plain,
v15_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[239,36]),
[iquote('0:MRR:239.1,36.0')] ).
cnf(308,plain,
v3_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[240,36]),
[iquote('0:MRR:240.1,36.0')] ).
cnf(309,plain,
v4_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[241,36]),
[iquote('0:MRR:241.1,36.0')] ).
cnf(310,plain,
v5_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[242,36]),
[iquote('0:MRR:242.1,36.0')] ).
cnf(311,plain,
v6_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[243,36]),
[iquote('0:MRR:243.1,36.0')] ).
cnf(312,plain,
v7_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[244,36]),
[iquote('0:MRR:244.1,36.0')] ).
cnf(313,plain,
v8_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[245,36]),
[iquote('0:MRR:245.1,36.0')] ).
cnf(314,plain,
v9_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[246,36]),
[iquote('0:MRR:246.1,36.0')] ).
cnf(315,plain,
v10_lattices(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[247,36]),
[iquote('0:MRR:247.1,36.0')] ).
cnf(316,plain,
v4_lattice3(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[248,36]),
[iquote('0:MRR:248.1,36.0')] ).
cnf(318,plain,
m1_conlat_1(k8_conlat_1(skc16),skc16),
inference(mrr,[status(thm)],[227,36]),
[iquote('0:MRR:227.0,36.0')] ).
cnf(319,plain,
m1_conlat_1(skf16(skc16),skc16),
inference(mrr,[status(thm)],[228,36]),
[iquote('0:MRR:228.0,36.0')] ).
cnf(320,plain,
~ v3_struct_0(k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[229,36]),
[iquote('0:MRR:229.1,36.0')] ).
cnf(325,plain,
~ v1_xboole_0(u2_conlat_1(skc16)),
inference(mrr,[status(thm)],[270,249]),
[iquote('0:MRR:270.0,249.0')] ).
cnf(326,plain,
~ v1_xboole_0(u1_conlat_1(skc16)),
inference(mrr,[status(thm)],[271,249]),
[iquote('0:MRR:271.0,249.0')] ).
cnf(329,plain,
r2_hidden(skc17,u1_conlat_1(skc16)),
inference(mrr,[status(thm)],[294,326]),
[iquote('0:MRR:294.1,326.0')] ).
cnf(330,plain,
r2_hidden(skc18,u2_conlat_1(skc16)),
inference(mrr,[status(thm)],[297,325]),
[iquote('0:MRR:297.1,325.0')] ).
cnf(331,plain,
( ~ v1_xboole_0(u)
| ~ m1_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[223,36]),
[iquote('0:MRR:223.2,36.0')] ).
cnf(332,plain,
v1_funct_2(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16))),
inference(mrr,[status(thm)],[219,36]),
[iquote('0:MRR:219.1,36.0')] ).
cnf(333,plain,
m2_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16))),
inference(mrr,[status(thm)],[220,36]),
[iquote('0:MRR:220.1,36.0')] ).
cnf(334,plain,
v1_funct_2(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16))),
inference(mrr,[status(thm)],[221,36]),
[iquote('0:MRR:221.1,36.0')] ).
cnf(335,plain,
m2_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16))),
inference(mrr,[status(thm)],[222,36]),
[iquote('0:MRR:222.1,36.0')] ).
cnf(337,plain,
equal(g3_lattices(k8_conlat_1(skc16),k10_conlat_1(skc16),k9_conlat_1(skc16)),k11_conlat_1(skc16)),
inference(mrr,[status(thm)],[214,36]),
[iquote('0:MRR:214.0,36.0')] ).
cnf(338,plain,
v1_funct_2(k10_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16)),
inference(mrr,[status(thm)],[215,36]),
[iquote('0:MRR:215.1,36.0')] ).
cnf(339,plain,
m2_relset_1(k10_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16)),
inference(mrr,[status(thm)],[216,36]),
[iquote('0:MRR:216.1,36.0')] ).
cnf(340,plain,
v1_funct_2(k9_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16)),
inference(mrr,[status(thm)],[217,36]),
[iquote('0:MRR:217.1,36.0')] ).
cnf(341,plain,
m2_relset_1(k9_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16)),
inference(mrr,[status(thm)],[218,36]),
[iquote('0:MRR:218.1,36.0')] ).
cnf(342,plain,
( ~ r2_hidden(u,v)
| ~ m1_conlat_1(v,skc16)
| v9_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[211,36]),
[iquote('0:MRR:211.3,36.0')] ).
cnf(343,plain,
( ~ r2_hidden(u,v)
| ~ m1_conlat_1(v,skc16)
| l3_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[212,36]),
[iquote('0:MRR:212.3,36.0')] ).
cnf(357,plain,
~ v1_xboole_0(skf16(skc16)),
inference(res,[status(thm),theory(equality)],[319,331]),
[iquote('0:Res:319.0,331.1')] ).
cnf(358,plain,
~ v1_xboole_0(k8_conlat_1(skc16)),
inference(res,[status(thm),theory(equality)],[318,331]),
[iquote('0:Res:318.0,331.1')] ).
cnf(359,plain,
~ v1_xboole_0(u2_conlat_1(skc16)),
inference(res,[status(thm),theory(equality)],[330,73]),
[iquote('0:Res:330.0,73.1')] ).
cnf(360,plain,
~ v1_xboole_0(u1_conlat_1(skc16)),
inference(res,[status(thm),theory(equality)],[329,73]),
[iquote('0:Res:329.0,73.1')] ).
cnf(390,plain,
m1_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16))),
inference(res,[status(thm),theory(equality)],[335,130]),
[iquote('0:Res:335.0,130.0')] ).
cnf(391,plain,
m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16))),
inference(res,[status(thm),theory(equality)],[333,130]),
[iquote('0:Res:333.0,130.0')] ).
cnf(392,plain,
m1_relset_1(k9_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16)),
inference(res,[status(thm),theory(equality)],[341,130]),
[iquote('0:Res:341.0,130.0')] ).
cnf(395,plain,
m1_relset_1(k10_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16)),
inference(res,[status(thm),theory(equality)],[339,130]),
[iquote('0:Res:339.0,130.0')] ).
cnf(473,plain,
( ~ m2_relset_1(u,v,w)
| v1_relat_1(u) ),
inference(res,[status(thm),theory(equality)],[144,112]),
[iquote('0:Res:144.1,112.0')] ).
cnf(476,plain,
v1_relat_1(k5_conlat_2(skc16)),
inference(res,[status(thm),theory(equality)],[335,473]),
[iquote('0:Res:335.0,473.0')] ).
cnf(477,plain,
v1_relat_1(k4_conlat_2(skc16)),
inference(res,[status(thm),theory(equality)],[333,473]),
[iquote('0:Res:333.0,473.0')] ).
cnf(478,plain,
v1_relat_1(k9_conlat_1(skc16)),
inference(res,[status(thm),theory(equality)],[341,473]),
[iquote('0:Res:341.0,473.0')] ).
cnf(479,plain,
v1_relat_1(k10_conlat_1(skc16)),
inference(res,[status(thm),theory(equality)],[339,473]),
[iquote('0:Res:339.0,473.0')] ).
cnf(511,plain,
( ~ r2_hidden(u,skf22(v))
| m1_subset_1(u,v) ),
inference(res,[status(thm),theory(equality)],[57,154]),
[iquote('0:Res:57.0,154.1')] ).
cnf(520,plain,
( ~ m1_subset_1(u,skf22(v))
| v1_xboole_0(skf22(v))
| m1_subset_1(u,v) ),
inference(res,[status(thm),theory(equality)],[132,511]),
[iquote('0:Res:132.2,511.0')] ).
cnf(600,plain,
( v1_xboole_0(skf22(u))
| m1_subset_1(skf18(skf22(u)),u) ),
inference(res,[status(thm),theory(equality)],[46,520]),
[iquote('0:Res:46.0,520.0')] ).
cnf(727,plain,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| m1_relset_1(k9_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u)) ),
inference(res,[status(thm),theory(equality)],[176,130]),
[iquote('0:Res:176.2,130.0')] ).
cnf(729,plain,
( ~ l2_conlat_1(u)
| v3_conlat_1(u)
| m1_relset_1(k10_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u)) ),
inference(res,[status(thm),theory(equality)],[174,130]),
[iquote('0:Res:174.2,130.0')] ).
cnf(885,plain,
( ~ l2_conlat_1(skc16)
| ~ r2_hidden(u,skf16(skc16))
| v3_conlat_1(skc16)
| v9_conlat_1(u,skc16) ),
inference(res,[status(thm),theory(equality)],[319,206]),
[iquote('0:Res:319.0,206.1')] ).
cnf(886,plain,
( ~ l2_conlat_1(skc16)
| ~ r2_hidden(u,k8_conlat_1(skc16))
| v3_conlat_1(skc16)
| v9_conlat_1(u,skc16) ),
inference(res,[status(thm),theory(equality)],[318,206]),
[iquote('0:Res:318.0,206.1')] ).
cnf(891,plain,
( ~ r2_hidden(u,skf16(skc16))
| v3_conlat_1(skc16)
| v9_conlat_1(u,skc16) ),
inference(ssi,[status(thm)],[885,1,249]),
[iquote('0:SSi:885.0,1.0,249.0')] ).
cnf(892,plain,
( ~ r2_hidden(u,skf16(skc16))
| v9_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[891,36]),
[iquote('0:MRR:891.1,36.0')] ).
cnf(893,plain,
( ~ r2_hidden(u,k8_conlat_1(skc16))
| v3_conlat_1(skc16)
| v9_conlat_1(u,skc16) ),
inference(ssi,[status(thm)],[886,1,249]),
[iquote('0:SSi:886.0,1.0,249.0')] ).
cnf(894,plain,
( ~ r2_hidden(u,k8_conlat_1(skc16))
| v9_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[893,36]),
[iquote('0:MRR:893.1,36.0')] ).
cnf(900,plain,
( ~ m1_subset_1(u,skf16(skc16))
| v1_xboole_0(skf16(skc16))
| v9_conlat_1(u,skc16) ),
inference(res,[status(thm),theory(equality)],[132,892]),
[iquote('0:Res:132.2,892.0')] ).
cnf(902,plain,
( ~ m1_subset_1(u,skf16(skc16))
| v9_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[900,357]),
[iquote('0:MRR:900.1,357.0')] ).
cnf(905,plain,
( ~ m1_subset_1(u,k8_conlat_1(skc16))
| v1_xboole_0(k8_conlat_1(skc16))
| v9_conlat_1(u,skc16) ),
inference(res,[status(thm),theory(equality)],[132,894]),
[iquote('0:Res:132.2,894.0')] ).
cnf(907,plain,
( ~ m1_subset_1(u,k8_conlat_1(skc16))
| v9_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[905,358]),
[iquote('0:MRR:905.1,358.0')] ).
cnf(910,plain,
( v1_xboole_0(skf22(skf16(skc16)))
| v9_conlat_1(skf18(skf22(skf16(skc16))),skc16) ),
inference(res,[status(thm),theory(equality)],[600,902]),
[iquote('0:Res:600.1,902.0')] ).
cnf(917,plain,
( ~ l2_conlat_1(skc16)
| ~ r2_hidden(u,k8_conlat_1(skc16))
| v3_conlat_1(skc16)
| l3_conlat_1(u,skc16) ),
inference(res,[status(thm),theory(equality)],[318,205]),
[iquote('0:Res:318.0,205.1')] ).
cnf(924,plain,
( ~ r2_hidden(u,k8_conlat_1(skc16))
| v3_conlat_1(skc16)
| l3_conlat_1(u,skc16) ),
inference(ssi,[status(thm)],[917,1,249]),
[iquote('0:SSi:917.0,1.0,249.0')] ).
cnf(925,plain,
( ~ r2_hidden(u,k8_conlat_1(skc16))
| l3_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[924,36]),
[iquote('0:MRR:924.1,36.0')] ).
cnf(931,plain,
( v1_xboole_0(skf22(k8_conlat_1(skc16)))
| v9_conlat_1(skf18(skf22(k8_conlat_1(skc16))),skc16) ),
inference(res,[status(thm),theory(equality)],[600,907]),
[iquote('0:Res:600.1,907.0')] ).
cnf(943,plain,
( ~ m1_subset_1(u,k8_conlat_1(skc16))
| v1_xboole_0(k8_conlat_1(skc16))
| l3_conlat_1(u,skc16) ),
inference(res,[status(thm),theory(equality)],[132,925]),
[iquote('0:Res:132.2,925.0')] ).
cnf(945,plain,
( ~ m1_subset_1(u,k8_conlat_1(skc16))
| l3_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[943,358]),
[iquote('0:MRR:943.1,358.0')] ).
cnf(961,plain,
v1_xboole_0(skf22(skf16(skc16))),
inference(spt,[spt(split,[position(s1)])],[910]),
[iquote('1:Spt:910.0')] ).
cnf(966,plain,
v1_xboole_0(skf16(skc16)),
inference(res,[status(thm),theory(equality)],[961,65]),
[iquote('1:Res:961.0,65.0')] ).
cnf(967,plain,
$false,
inference(mrr,[status(thm)],[966,357]),
[iquote('1:MRR:966.0,357.0')] ).
cnf(971,plain,
~ v1_xboole_0(skf22(skf16(skc16))),
inference(spt,[spt(split,[position(sa)])],[967,961]),
[iquote('1:Spt:967.0,910.0,961.0')] ).
cnf(972,plain,
v9_conlat_1(skf18(skf22(skf16(skc16))),skc16),
inference(spt,[spt(split,[position(s2)])],[910]),
[iquote('1:Spt:967.0,910.1')] ).
cnf(1003,plain,
v1_xboole_0(skf22(k8_conlat_1(skc16))),
inference(spt,[spt(split,[position(s2s1)])],[931]),
[iquote('2:Spt:931.0')] ).
cnf(1008,plain,
v1_xboole_0(k8_conlat_1(skc16)),
inference(res,[status(thm),theory(equality)],[1003,65]),
[iquote('2:Res:1003.0,65.0')] ).
cnf(1009,plain,
$false,
inference(mrr,[status(thm)],[1008,358]),
[iquote('2:MRR:1008.0,358.0')] ).
cnf(1013,plain,
~ v1_xboole_0(skf22(k8_conlat_1(skc16))),
inference(spt,[spt(split,[position(s2sa)])],[1009,1003]),
[iquote('2:Spt:1009.0,931.0,1003.0')] ).
cnf(1014,plain,
v9_conlat_1(skf18(skf22(k8_conlat_1(skc16))),skc16),
inference(spt,[spt(split,[position(s2s2)])],[931]),
[iquote('2:Spt:1009.0,931.1')] ).
cnf(1058,plain,
( ~ v1_funct_1(k4_conlat_2(skc16))
| ~ m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v1_xboole_0(u1_struct_0(k11_conlat_1(skc16)))
| v1_partfun1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16))) ),
inference(res,[status(thm),theory(equality)],[332,188]),
[iquote('0:Res:332.0,188.2')] ).
cnf(1069,plain,
( ~ m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v1_xboole_0(u1_struct_0(k11_conlat_1(skc16)))
| v1_partfun1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16))) ),
inference(ssi,[status(thm)],[1058,302,477]),
[iquote('0:SSi:1058.0,302.0,477.0')] ).
cnf(1070,plain,
( v1_xboole_0(u1_struct_0(k11_conlat_1(skc16)))
| v1_partfun1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16))) ),
inference(mrr,[status(thm)],[1069,391]),
[iquote('0:MRR:1069.0,391.0')] ).
cnf(1131,plain,
( ~ v1_funct_1(k5_conlat_2(skc16))
| ~ m1_subset_1(u,u2_conlat_1(skc16))
| ~ m1_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v1_xboole_0(u2_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k5_conlat_2(skc16),u),u1_struct_0(k11_conlat_1(skc16))) ),
inference(res,[status(thm),theory(equality)],[334,208]),
[iquote('0:Res:334.0,208.2')] ).
cnf(1132,plain,
( ~ v1_funct_1(k4_conlat_2(skc16))
| ~ m1_subset_1(u,u1_conlat_1(skc16))
| ~ m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v1_xboole_0(u1_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k4_conlat_2(skc16),u),u1_struct_0(k11_conlat_1(skc16))) ),
inference(res,[status(thm),theory(equality)],[332,208]),
[iquote('0:Res:332.0,208.2')] ).
cnf(1143,plain,
( ~ m1_subset_1(u,u1_conlat_1(skc16))
| ~ m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v1_xboole_0(u1_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k4_conlat_2(skc16),u),u1_struct_0(k11_conlat_1(skc16))) ),
inference(ssi,[status(thm)],[1132,302,477]),
[iquote('0:SSi:1132.0,302.0,477.0')] ).
cnf(1144,plain,
( ~ m1_subset_1(u,u1_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k4_conlat_2(skc16),u),u1_struct_0(k11_conlat_1(skc16))) ),
inference(mrr,[status(thm)],[1143,391,360]),
[iquote('0:MRR:1143.1,1143.2,391.0,360.0')] ).
cnf(1145,plain,
( ~ m1_subset_1(u,u2_conlat_1(skc16))
| ~ m1_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v1_xboole_0(u2_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k5_conlat_2(skc16),u),u1_struct_0(k11_conlat_1(skc16))) ),
inference(ssi,[status(thm)],[1131,303,476]),
[iquote('0:SSi:1131.0,303.0,476.0')] ).
cnf(1146,plain,
( ~ m1_subset_1(u,u2_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k5_conlat_2(skc16),u),u1_struct_0(k11_conlat_1(skc16))) ),
inference(mrr,[status(thm)],[1145,390,359]),
[iquote('0:MRR:1145.1,1145.2,390.0,359.0')] ).
cnf(1238,plain,
( ~ v1_funct_1(k9_conlat_1(skc16))
| ~ v1_funct_1(k10_conlat_1(skc16))
| ~ equal(g3_lattices(u,v,w),k11_conlat_1(skc16))
| ~ m1_relset_1(k10_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| ~ v1_funct_2(k10_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| ~ m1_relset_1(k9_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| ~ v1_funct_2(k9_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| equal(k8_conlat_1(skc16),u) ),
inference(spl,[status(thm),theory(equality)],[337,202]),
[iquote('0:SpL:337.0,202.2')] ).
cnf(1239,plain,
( ~ l2_conlat_1(u)
| ~ v1_funct_1(k9_conlat_1(u))
| ~ v1_funct_1(k10_conlat_1(u))
| ~ equal(k11_conlat_1(u),g3_lattices(v,w,x))
| ~ m1_relset_1(k10_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u))
| ~ v1_funct_2(k10_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u))
| ~ m1_relset_1(k9_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u))
| ~ v1_funct_2(k9_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u))
| v3_conlat_1(u)
| equal(k8_conlat_1(u),v) ),
inference(spl,[status(thm),theory(equality)],[172,202]),
[iquote('0:SpL:172.2,202.2')] ).
cnf(1244,plain,
( ~ equal(g3_lattices(u,v,w),k11_conlat_1(skc16))
| ~ m1_relset_1(k10_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| ~ v1_funct_2(k10_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| ~ m1_relset_1(k9_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| ~ v1_funct_2(k9_conlat_1(skc16),k2_zfmisc_1(k8_conlat_1(skc16),k8_conlat_1(skc16)),k8_conlat_1(skc16))
| equal(k8_conlat_1(skc16),u) ),
inference(ssi,[status(thm)],[1238,300,479,304,478]),
[iquote('0:SSi:1238.1,1238.0,300.0,479.0,304.0,478.0')] ).
cnf(1245,plain,
( ~ equal(g3_lattices(u,v,w),k11_conlat_1(skc16))
| equal(k8_conlat_1(skc16),u) ),
inference(mrr,[status(thm)],[1244,395,338,392,340]),
[iquote('0:MRR:1244.1,1244.2,1244.3,1244.4,395.0,338.0,392.0,340.0')] ).
cnf(1247,plain,
( ~ l2_conlat_1(u)
| ~ equal(k11_conlat_1(u),g3_lattices(v,w,x))
| ~ m1_relset_1(k10_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u))
| ~ m1_relset_1(k9_conlat_1(u),k2_zfmisc_1(k8_conlat_1(u),k8_conlat_1(u)),k8_conlat_1(u))
| v3_conlat_1(u)
| equal(k8_conlat_1(u),v) ),
inference(mrr,[status(thm)],[1239,80,75,173,175]),
[iquote('0:MRR:1239.1,1239.2,1239.5,1239.7,80.2,75.2,173.2,175.2')] ).
cnf(1248,plain,
( ~ l2_conlat_1(u)
| ~ equal(k11_conlat_1(u),g3_lattices(v,w,x))
| v3_conlat_1(u)
| equal(k8_conlat_1(u),v) ),
inference(mrr,[status(thm)],[1247,729,727]),
[iquote('0:MRR:1247.2,1247.3,729.2,727.2')] ).
cnf(1273,plain,
v1_xboole_0(u1_struct_0(k11_conlat_1(skc16))),
inference(spt,[spt(split,[position(s2s2s1)])],[1070]),
[iquote('3:Spt:1070.0')] ).
cnf(1278,plain,
( ~ l1_struct_0(k11_conlat_1(skc16))
| v3_struct_0(k11_conlat_1(skc16)) ),
inference(res,[status(thm),theory(equality)],[1273,119]),
[iquote('3:Res:1273.0,119.1')] ).
cnf(1289,plain,
v3_struct_0(k11_conlat_1(skc16)),
inference(ssi,[status(thm)],[1278,56,54,316,306,305,314,313,307,308,312,311,310,309,315,301]),
[iquote('3:SSi:1278.0,56.0,54.0,316.0,306.0,305.0,314.0,313.0,307.0,308.0,312.0,311.0,310.0,309.0,315.1,301.1')] ).
cnf(1290,plain,
$false,
inference(mrr,[status(thm)],[1289,320]),
[iquote('3:MRR:1289.0,320.0')] ).
cnf(1294,plain,
~ v1_xboole_0(u1_struct_0(k11_conlat_1(skc16))),
inference(spt,[spt(split,[position(s2s2sa)])],[1290,1273]),
[iquote('3:Spt:1290.0,1070.0,1273.0')] ).
cnf(1295,plain,
v1_partfun1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16))),
inference(spt,[spt(split,[position(s2s2s2)])],[1070]),
[iquote('3:Spt:1290.0,1070.1')] ).
cnf(1299,plain,
( ~ v1_funct_1(k5_conlat_2(skc16))
| ~ m1_subset_1(skc18,u2_conlat_1(skc16))
| ~ v1_funct_2(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ l3_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v1_xboole_0(u2_conlat_1(skc16))
| v7_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16) ),
inference(spr,[status(thm),theory(equality)],[195,203]),
[iquote('0:SpR:195.5,203.4')] ).
cnf(1300,plain,
( ~ l2_conlat_1(skc16)
| ~ l3_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16)
| v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[203,207]),
[iquote('0:Res:203.4,207.1')] ).
cnf(1301,plain,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16)
| v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v3_conlat_1(skc16) ),
inference(ssi,[status(thm)],[1300,1,249]),
[iquote('0:SSi:1300.0,1.0,249.0')] ).
cnf(1302,plain,
( ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16)
| v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16) ),
inference(mrr,[status(thm)],[1301,343,342,36]),
[iquote('0:MRR:1301.0,1301.1,1301.7,343.2,342.2,36.0')] ).
cnf(1303,plain,
( ~ v1_funct_1(k5_conlat_2(skc16))
| ~ m1_subset_1(skc18,u2_conlat_1(skc16))
| ~ v1_funct_2(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ l3_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v1_xboole_0(u2_conlat_1(skc16))
| v7_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16) ),
inference(rew,[status(thm),theory(equality)],[195,1299]),
[iquote('0:Rew:195.5,1299.5,195.5,1299.4')] ).
cnf(1304,plain,
( ~ m1_subset_1(skc18,u2_conlat_1(skc16))
| ~ v1_funct_2(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ l3_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v1_xboole_0(u2_conlat_1(skc16))
| v7_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16) ),
inference(ssi,[status(thm)],[1303,303,476]),
[iquote('0:SSi:1303.0,303.0,476.0')] ).
cnf(1305,plain,
( ~ v1_funct_2(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ l3_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v7_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16) ),
inference(mrr,[status(thm)],[1304,44,359]),
[iquote('0:MRR:1304.0,1304.7,44.0,359.0')] ).
cnf(1306,plain,
( ~ l3_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v7_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16) ),
inference(mrr,[status(thm)],[1305,334,390]),
[iquote('0:MRR:1305.0,1305.1,334.0,390.0')] ).
cnf(1336,plain,
( ~ v3_lattices(u)
| ~ l3_lattices(u)
| ~ equal(u,k11_conlat_1(skc16))
| equal(k8_conlat_1(skc16),u1_struct_0(u)) ),
inference(spl,[status(thm),theory(equality)],[170,1245]),
[iquote('0:SpL:170.2,1245.0')] ).
cnf(1900,plain,
( ~ v3_lattices(u)
| ~ l3_lattices(u)
| ~ l2_conlat_1(v)
| ~ equal(k11_conlat_1(v),u)
| v3_conlat_1(v)
| equal(k8_conlat_1(v),u1_struct_0(u)) ),
inference(spl,[status(thm),theory(equality)],[170,1248]),
[iquote('0:SpL:170.2,1248.1')] ).
cnf(2635,plain,
v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16),
inference(spt,[spt(split,[position(s2s2s2s1)])],[1306]),
[iquote('4:Spt:1306.5')] ).
cnf(2636,plain,
( ~ v1_funct_1(k4_conlat_2(skc16))
| ~ m1_subset_1(skc17,u1_conlat_1(skc16))
| ~ v1_funct_2(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v1_xboole_0(u1_conlat_1(skc16))
| v7_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16) ),
inference(spr,[status(thm),theory(equality)],[195,2635]),
[iquote('4:SpR:195.5,2635.0')] ).
cnf(2640,plain,
( ~ m1_subset_1(skc17,u1_conlat_1(skc16))
| ~ v1_funct_2(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| v1_xboole_0(u1_conlat_1(skc16))
| v7_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16) ),
inference(ssi,[status(thm)],[2636,302,477]),
[iquote('4:SSi:2636.0,302.0,477.0')] ).
cnf(2641,plain,
v7_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16),
inference(mrr,[status(thm)],[2640,45,332,391,360]),
[iquote('4:MRR:2640.0,2640.1,2640.2,2640.3,45.0,332.0,391.0,360.0')] ).
cnf(2642,plain,
( ~ l2_conlat_1(skc16)
| ~ r2_hidden(k1_funct_1(k4_conlat_2(skc16),skc17),u)
| ~ m1_conlat_1(u,skc16)
| v3_conlat_1(skc16) ),
inference(res,[status(thm),theory(equality)],[2641,207]),
[iquote('4:Res:2641.0,207.1')] ).
cnf(2643,plain,
( ~ r2_hidden(k1_funct_1(k4_conlat_2(skc16),skc17),u)
| ~ m1_conlat_1(u,skc16)
| v3_conlat_1(skc16) ),
inference(ssi,[status(thm)],[2642,1,249]),
[iquote('4:SSi:2642.0,1.0,249.0')] ).
cnf(2644,plain,
( ~ r2_hidden(k1_funct_1(k4_conlat_2(skc16),skc17),u)
| ~ m1_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[2643,36]),
[iquote('4:MRR:2643.2,36.0')] ).
cnf(2645,plain,
( ~ m1_subset_1(k1_funct_1(k4_conlat_2(skc16),skc17),u)
| ~ m1_conlat_1(u,skc16)
| v1_xboole_0(u) ),
inference(res,[status(thm),theory(equality)],[132,2644]),
[iquote('4:Res:132.2,2644.0')] ).
cnf(2646,plain,
( ~ m1_subset_1(k1_funct_1(k4_conlat_2(skc16),skc17),u)
| ~ m1_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[2645,331]),
[iquote('4:MRR:2645.2,331.0')] ).
cnf(2654,plain,
( ~ m1_subset_1(skc17,u1_conlat_1(skc16))
| ~ m1_conlat_1(u1_struct_0(k11_conlat_1(skc16)),skc16) ),
inference(res,[status(thm),theory(equality)],[1144,2646]),
[iquote('4:Res:1144.1,2646.0')] ).
cnf(2656,plain,
~ m1_conlat_1(u1_struct_0(k11_conlat_1(skc16)),skc16),
inference(mrr,[status(thm)],[2654,45]),
[iquote('4:MRR:2654.0,45.0')] ).
cnf(4965,plain,
( ~ v3_lattices(u)
| ~ l3_lattices(u)
| ~ l2_conlat_1(skc16)
| ~ equal(k11_conlat_1(skc16),u)
| v3_conlat_1(skc16)
| m1_conlat_1(u1_struct_0(u),skc16) ),
inference(spr,[status(thm),theory(equality)],[1900,318]),
[iquote('0:SpR:1900.5,318.0')] ).
cnf(5164,plain,
( ~ v3_lattices(u)
| ~ l3_lattices(u)
| ~ equal(k11_conlat_1(skc16),u)
| v3_conlat_1(skc16)
| m1_conlat_1(u1_struct_0(u),skc16) ),
inference(ssi,[status(thm)],[4965,1,249]),
[iquote('0:SSi:4965.2,1.0,249.0')] ).
cnf(5165,plain,
( ~ v3_lattices(u)
| ~ l3_lattices(u)
| ~ equal(k11_conlat_1(skc16),u)
| m1_conlat_1(u1_struct_0(u),skc16) ),
inference(mrr,[status(thm)],[5164,36]),
[iquote('0:MRR:5164.3,36.0')] ).
cnf(5441,plain,
( ~ v3_lattices(k11_conlat_1(skc16))
| ~ l3_lattices(k11_conlat_1(skc16))
| ~ equal(k11_conlat_1(skc16),k11_conlat_1(skc16)) ),
inference(res,[status(thm),theory(equality)],[5165,2656]),
[iquote('4:Res:5165.3,2656.0')] ).
cnf(5445,plain,
( ~ v3_lattices(k11_conlat_1(skc16))
| ~ l3_lattices(k11_conlat_1(skc16)) ),
inference(obv,[status(thm),theory(equality)],[5441]),
[iquote('4:Obv:5441.2')] ).
cnf(5446,plain,
$false,
inference(ssi,[status(thm)],[5445,316,306,305,314,313,307,308,312,311,310,309,315,301]),
[iquote('4:SSi:5445.1,5445.0,316.0,306.0,305.0,314.0,313.0,307.0,308.0,312.0,311.0,310.0,309.0,315.0,301.0,316.0,306.0,305.0,314.0,313.0,307.0,308.0,312.0,311.0,310.0,309.0,315.0,301.0')] ).
cnf(5449,plain,
~ v7_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16),
inference(spt,[spt(split,[position(s2s2s2sa)])],[5446,2635]),
[iquote('4:Spt:5446.0,1306.5,2635.0')] ).
cnf(5450,plain,
( ~ l3_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v7_conlat_1(k1_funct_1(k5_conlat_2(skc16),skc18),skc16) ),
inference(spt,[spt(split,[position(s2s2s2s2)])],[1306]),
[iquote('4:Spt:5446.0,1306.0,1306.1,1306.2,1306.3,1306.4')] ).
cnf(5451,plain,
( ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[1302,5449]),
[iquote('4:MRR:1302.4,5449.0')] ).
cnf(5452,plain,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v7_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16) ),
inference(mrr,[status(thm)],[203,5449]),
[iquote('4:MRR:203.5,5449.0')] ).
cnf(5484,plain,
~ l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16),
inference(spt,[spt(split,[position(s2s2s2s2s1)])],[5452]),
[iquote('5:Spt:5452.2')] ).
cnf(5487,plain,
( ~ v1_funct_1(k4_conlat_2(skc16))
| ~ m1_subset_1(skc17,u1_conlat_1(skc16))
| ~ v1_funct_2(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ l3_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16)
| v1_xboole_0(u1_conlat_1(skc16)) ),
inference(spl,[status(thm),theory(equality)],[195,5484]),
[iquote('5:SpL:195.5,5484.0')] ).
cnf(5489,plain,
( ~ m1_subset_1(skc17,u1_conlat_1(skc16))
| ~ v1_funct_2(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ l3_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16)
| v1_xboole_0(u1_conlat_1(skc16)) ),
inference(ssi,[status(thm)],[5487,302,477]),
[iquote('5:SSi:5487.0,302.0,477.0')] ).
cnf(5490,plain,
~ l3_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16),
inference(mrr,[status(thm)],[5489,45,332,391,360]),
[iquote('5:MRR:5489.0,5489.1,5489.2,5489.4,45.0,332.0,391.0,360.0')] ).
cnf(9012,plain,
( ~ v3_lattices(k11_conlat_1(skc16))
| ~ l3_lattices(k11_conlat_1(skc16))
| ~ equal(k11_conlat_1(skc16),k11_conlat_1(skc16))
| ~ m1_subset_1(u,u2_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k5_conlat_2(skc16),u),k8_conlat_1(skc16)) ),
inference(spr,[status(thm),theory(equality)],[1336,1146]),
[iquote('0:SpR:1336.3,1146.1')] ).
cnf(9013,plain,
( ~ v3_lattices(k11_conlat_1(skc16))
| ~ l3_lattices(k11_conlat_1(skc16))
| ~ equal(k11_conlat_1(skc16),k11_conlat_1(skc16))
| ~ m1_subset_1(u,u1_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k4_conlat_2(skc16),u),k8_conlat_1(skc16)) ),
inference(spr,[status(thm),theory(equality)],[1336,1144]),
[iquote('0:SpR:1336.3,1144.1')] ).
cnf(9141,plain,
( ~ v3_lattices(k11_conlat_1(skc16))
| ~ l3_lattices(k11_conlat_1(skc16))
| ~ m1_subset_1(u,u1_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k4_conlat_2(skc16),u),k8_conlat_1(skc16)) ),
inference(obv,[status(thm),theory(equality)],[9013]),
[iquote('0:Obv:9013.2')] ).
cnf(9142,plain,
( ~ m1_subset_1(u,u1_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k4_conlat_2(skc16),u),k8_conlat_1(skc16)) ),
inference(ssi,[status(thm)],[9141,316,306,305,314,313,307,308,312,311,310,309,315,301]),
[iquote('0:SSi:9141.1,9141.0,316.0,306.0,305.0,314.0,313.0,307.0,308.0,312.0,311.0,310.0,309.0,315.0,301.0,316.0,306.0,305.0,314.0,313.0,307.0,308.0,312.0,311.0,310.0,309.0,315.0,301.0')] ).
cnf(9143,plain,
( ~ v3_lattices(k11_conlat_1(skc16))
| ~ l3_lattices(k11_conlat_1(skc16))
| ~ m1_subset_1(u,u2_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k5_conlat_2(skc16),u),k8_conlat_1(skc16)) ),
inference(obv,[status(thm),theory(equality)],[9012]),
[iquote('0:Obv:9012.2')] ).
cnf(9144,plain,
( ~ m1_subset_1(u,u2_conlat_1(skc16))
| m1_subset_1(k1_funct_1(k5_conlat_2(skc16),u),k8_conlat_1(skc16)) ),
inference(ssi,[status(thm)],[9143,316,306,305,314,313,307,308,312,311,310,309,315,301]),
[iquote('0:SSi:9143.1,9143.0,316.0,306.0,305.0,314.0,313.0,307.0,308.0,312.0,311.0,310.0,309.0,315.0,301.0,316.0,306.0,305.0,314.0,313.0,307.0,308.0,312.0,311.0,310.0,309.0,315.0,301.0')] ).
cnf(9329,plain,
( ~ m1_subset_1(u,u1_conlat_1(skc16))
| l3_conlat_1(k1_funct_1(k4_conlat_2(skc16),u),skc16) ),
inference(res,[status(thm),theory(equality)],[9142,945]),
[iquote('0:Res:9142.1,945.0')] ).
cnf(9330,plain,
( ~ m1_subset_1(u,u1_conlat_1(skc16))
| v9_conlat_1(k1_funct_1(k4_conlat_2(skc16),u),skc16) ),
inference(res,[status(thm),theory(equality)],[9142,907]),
[iquote('0:Res:9142.1,907.0')] ).
cnf(9340,plain,
~ m1_subset_1(skc17,u1_conlat_1(skc16)),
inference(res,[status(thm),theory(equality)],[9329,5490]),
[iquote('5:Res:9329.1,5490.0')] ).
cnf(9341,plain,
$false,
inference(mrr,[status(thm)],[9340,45]),
[iquote('5:MRR:9340.0,45.0')] ).
cnf(9342,plain,
l3_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16),
inference(spt,[spt(split,[position(s2s2s2s2sa)])],[9341,5484]),
[iquote('5:Spt:9341.0,5452.2,5484.0')] ).
cnf(9343,plain,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| v7_conlat_1(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),skc16) ),
inference(spt,[spt(split,[position(s2s2s2s2s2)])],[5452]),
[iquote('5:Spt:9341.0,5452.0,5452.1,5452.3,5452.4')] ).
cnf(9350,plain,
( ~ v9_conlat_1(k8_funct_2(u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[5451,9342]),
[iquote('5:MRR:5451.0,9342.0')] ).
cnf(9379,plain,
( ~ v1_funct_1(k4_conlat_2(skc16))
| ~ m1_subset_1(skc17,u1_conlat_1(skc16))
| ~ v1_funct_2(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ v9_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16)
| v1_xboole_0(u1_conlat_1(skc16)) ),
inference(spl,[status(thm),theory(equality)],[195,9350]),
[iquote('5:SpL:195.5,9350.0')] ).
cnf(9383,plain,
( ~ m1_subset_1(skc17,u1_conlat_1(skc16))
| ~ v1_funct_2(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k4_conlat_2(skc16),u1_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ v9_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16)
| v1_xboole_0(u1_conlat_1(skc16)) ),
inference(ssi,[status(thm)],[9379,302,477]),
[iquote('5:SSi:9379.0,302.0,477.0')] ).
cnf(9384,plain,
( ~ v9_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k8_funct_2(u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)),k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[9383,45,332,391,360]),
[iquote('5:MRR:9383.0,9383.1,9383.2,9383.6,45.0,332.0,391.0,360.0')] ).
cnf(10531,plain,
( ~ v1_funct_1(k5_conlat_2(skc16))
| ~ m1_subset_1(skc18,u2_conlat_1(skc16))
| ~ v1_funct_2(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ v9_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k1_funct_1(k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16)
| v1_xboole_0(u2_conlat_1(skc16)) ),
inference(spl,[status(thm),theory(equality)],[195,9384]),
[iquote('5:SpL:195.5,9384.1')] ).
cnf(10537,plain,
( ~ m1_subset_1(skc18,u2_conlat_1(skc16))
| ~ v1_funct_2(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ m1_relset_1(k5_conlat_2(skc16),u2_conlat_1(skc16),u1_struct_0(k11_conlat_1(skc16)))
| ~ v9_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k1_funct_1(k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16)
| v1_xboole_0(u2_conlat_1(skc16)) ),
inference(ssi,[status(thm)],[10531,303,476]),
[iquote('5:SSi:10531.0,303.0,476.0')] ).
cnf(10538,plain,
( ~ v9_conlat_1(k1_funct_1(k4_conlat_2(skc16),skc17),skc16)
| ~ r2_hidden(k1_funct_1(k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[10537,44,334,390,359]),
[iquote('5:MRR:10537.0,10537.1,10537.2,10537.6,44.0,334.0,390.0,359.0')] ).
cnf(13739,plain,
( ~ m1_subset_1(skc17,u1_conlat_1(skc16))
| ~ r2_hidden(k1_funct_1(k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16) ),
inference(res,[status(thm),theory(equality)],[9330,10538]),
[iquote('5:Res:9330.1,10538.0')] ).
cnf(13741,plain,
( ~ r2_hidden(k1_funct_1(k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[13739,45]),
[iquote('5:MRR:13739.0,45.0')] ).
cnf(13742,plain,
( ~ m1_subset_1(k1_funct_1(k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16)
| v1_xboole_0(u) ),
inference(res,[status(thm),theory(equality)],[132,13741]),
[iquote('5:Res:132.2,13741.0')] ).
cnf(13743,plain,
( ~ m1_subset_1(k1_funct_1(k5_conlat_2(skc16),skc18),u)
| ~ m1_conlat_1(u,skc16) ),
inference(mrr,[status(thm)],[13742,331]),
[iquote('5:MRR:13742.2,331.0')] ).
cnf(13760,plain,
( ~ m1_subset_1(skc18,u2_conlat_1(skc16))
| ~ m1_conlat_1(k8_conlat_1(skc16),skc16) ),
inference(res,[status(thm),theory(equality)],[9144,13743]),
[iquote('5:Res:9144.1,13743.0')] ).
cnf(13762,plain,
$false,
inference(mrr,[status(thm)],[13760,44,318]),
[iquote('5:MRR:13760.0,13760.1,44.0,318.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : LAT343+1 : TPTP v8.1.0. Released v3.4.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.13/0.33 % Computer : n003.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Thu Jun 30 05:32:36 EDT 2022
% 0.13/0.33 % CPUTime :
% 4.87/5.05
% 4.87/5.05 SPASS V 3.9
% 4.87/5.05 SPASS beiseite: Proof found.
% 4.87/5.05 % SZS status Theorem
% 4.87/5.05 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.87/5.05 SPASS derived 9898 clauses, backtracked 476 clauses, performed 49 splits and kept 5952 clauses.
% 4.87/5.05 SPASS allocated 110759 KBytes.
% 4.87/5.05 SPASS spent 0:00:04.70 on the problem.
% 4.87/5.05 0:00:00.04 for the input.
% 4.87/5.05 0:00:00.06 for the FLOTTER CNF translation.
% 4.87/5.05 0:00:00.20 for inferences.
% 4.87/5.05 0:00:00.23 for the backtracking.
% 4.87/5.05 0:00:04.01 for the reduction.
% 4.87/5.05
% 4.87/5.05
% 4.87/5.05 Here is a proof with depth 8, length 261 :
% 4.87/5.05 % SZS output start Refutation
% See solution above
% 5.45/5.61 Formulae used in the proof : t11_conlat_2 existence_m1_subset_1 dt_l2_conlat_1 dt_l2_lattices dt_l3_lattices rc1_subset_1 t7_boole dt_k10_conlat_1 dt_k11_conlat_1 dt_k4_conlat_2 dt_k5_conlat_2 dt_k9_conlat_1 fc1_conlat_2 fc5_conlat_1 cc1_relset_1 dt_k8_conlat_1 existence_m1_conlat_1 fc1_conlat_1 fc1_struct_0 fc2_conlat_1 redefinition_m2_relset_1 t2_subset dt_m2_relset_1 dt_m1_conlat_1 t4_subset abstractness_v3_lattices d23_conlat_1 d18_conlat_1 cc5_funct_2 dt_k8_funct_2 redefinition_k8_funct_2 free_g3_lattices
% 5.45/5.61
%------------------------------------------------------------------------------