%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SEU347+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n012.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 : Tue Jul 19 14:36:28 EDT 2022
% Result : Theorem 123.72s 123.87s
% Output : Refutation 131.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 43
% Syntax : Number of clauses : 144 ( 34 unt; 67 nHn; 144 RR)
% Number of literals : 484 ( 0 equ; 278 neg)
% Maximal clause size : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
latt_str(skc13),
file('SEU347+1.p',unknown),
[] ).
cnf(2,axiom,
lattice(skc13),
file('SEU347+1.p',unknown),
[] ).
cnf(18,axiom,
~ empty_carrier(skc13),
file('SEU347+1.p',unknown),
[] ).
cnf(24,axiom,
element(skc14,the_carrier(skc13)),
file('SEU347+1.p',unknown),
[] ).
cnf(30,axiom,
( ~ latt_str(u)
| meet_semilatt_str(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(31,axiom,
( ~ latt_str(u)
| join_semilatt_str(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(39,axiom,
element(skf8(u,v,w),the_carrier(w)),
file('SEU347+1.p',unknown),
[] ).
cnf(40,axiom,
element(skf9(u,v,w),the_carrier(w)),
file('SEU347+1.p',unknown),
[] ).
cnf(52,axiom,
( ~ relation_of2_as_subset(u,v,w)
| relation_of2(u,v,w) ),
file('SEU347+1.p',unknown),
[] ).
cnf(56,axiom,
( ~ lattice(u)
| ~ latt_str(u)
| empty_carrier(u)
| join_commutative(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(57,axiom,
( ~ lattice(u)
| ~ latt_str(u)
| empty_carrier(u)
| join_associative(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ lattice(u)
| ~ latt_str(u)
| empty_carrier(u)
| meet_commutative(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ lattice(u)
| ~ latt_str(u)
| empty_carrier(u)
| meet_associative(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ lattice(u)
| ~ latt_str(u)
| empty_carrier(u)
| meet_absorbing(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(61,axiom,
( ~ lattice(u)
| ~ latt_str(u)
| empty_carrier(u)
| join_absorbing(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(63,axiom,
( latt_set_smaller(skc13,skc14,skc15)
| relstr_element_smaller(poset_of_lattice(skc13),skc15,cast_to_el_of_LattPOSet(skc13,skc14)) ),
file('SEU347+1.p',unknown),
[] ).
cnf(71,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| empty_carrier(u)
| rel_str(poset_of_lattice(u)) ),
file('SEU347+1.p',unknown),
[] ).
cnf(75,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| empty_carrier(u)
| strict_rel_str(poset_of_lattice(u)) ),
file('SEU347+1.p',unknown),
[] ).
cnf(76,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| empty_carrier(u)
| reflexive_relstr(poset_of_lattice(u)) ),
file('SEU347+1.p',unknown),
[] ).
cnf(77,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| empty_carrier(u)
| transitive_relstr(poset_of_lattice(u)) ),
file('SEU347+1.p',unknown),
[] ).
cnf(78,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| empty_carrier(u)
| antisymmetric_relstr(poset_of_lattice(u)) ),
file('SEU347+1.p',unknown),
[] ).
cnf(80,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| ~ empty_carrier(poset_of_lattice(u))
| empty_carrier(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(83,axiom,
( ~ latt_set_smaller(skc13,skc14,skc15)
| ~ relstr_element_smaller(poset_of_lattice(skc13),skc15,cast_to_el_of_LattPOSet(skc13,skc14)) ),
file('SEU347+1.p',unknown),
[] ).
cnf(84,axiom,
( ~ strict_rel_str(u)
| ~ rel_str(u)
| equal(rel_str_of(the_carrier(u),the_InternalRel(u)),u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(87,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| empty_carrier(u)
| relation_of2_as_subset(k2_lattice3(u),the_carrier(u),the_carrier(u)) ),
file('SEU347+1.p',unknown),
[] ).
cnf(92,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| empty_carrier(u)
| equal(rel_str_of(the_carrier(u),k2_lattice3(u)),poset_of_lattice(u)) ),
file('SEU347+1.p',unknown),
[] ).
cnf(93,axiom,
( ~ equal(rel_str_of(u,v),rel_str_of(w,x))
| ~ relation_of2(v,u,u)
| equal(u,w) ),
file('SEU347+1.p',unknown),
[] ).
cnf(96,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| ~ element(v,the_carrier(u))
| empty_carrier(u)
| equal(cast_to_el_of_LattPOSet(u,v),v) ),
file('SEU347+1.p',unknown),
[] ).
cnf(97,axiom,
( ~ rel_str(u)
| ~ element(v,the_carrier(u))
| in(skf9(v,w,u),w)
| relstr_element_smaller(u,w,v) ),
file('SEU347+1.p',unknown),
[] ).
cnf(98,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| ~ element(v,the_carrier(poset_of_lattice(u)))
| empty_carrier(u)
| equal(cast_to_el_of_lattice(u,v),v) ),
file('SEU347+1.p',unknown),
[] ).
cnf(100,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| ~ element(v,the_carrier(poset_of_lattice(u)))
| element(cast_to_el_of_lattice(u,v),the_carrier(u))
| empty_carrier(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(101,axiom,
( ~ latt_str(u)
| ~ lattice(u)
| ~ element(v,the_carrier(u))
| element(cast_to_el_of_LattPOSet(u,v),the_carrier(poset_of_lattice(u)))
| empty_carrier(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(102,axiom,
( ~ rel_str(u)
| ~ element(v,the_carrier(u))
| ~ related(u,v,skf9(v,w,u))
| relstr_element_smaller(u,w,v) ),
file('SEU347+1.p',unknown),
[] ).
cnf(103,axiom,
( ~ latt_str(u)
| ~ element(v,the_carrier(u))
| empty_carrier(u)
| in(skf8(v,w,u),w)
| latt_set_smaller(u,v,w) ),
file('SEU347+1.p',unknown),
[] ).
cnf(104,axiom,
( ~ latt_str(u)
| ~ element(v,the_carrier(u))
| ~ below(u,v,skf8(v,w,u))
| empty_carrier(u)
| latt_set_smaller(u,v,w) ),
file('SEU347+1.p',unknown),
[] ).
cnf(111,axiom,
( ~ rel_str(u)
| ~ in(v,w)
| ~ element(x,the_carrier(u))
| ~ element(v,the_carrier(u))
| ~ relstr_element_smaller(u,w,x)
| related(u,x,v) ),
file('SEU347+1.p',unknown),
[] ).
cnf(112,axiom,
( ~ rel_str(u)
| ~ reflexive_relstr(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ related(u,v,w)
| empty_carrier(u)
| related_reflexive(u,v,w) ),
file('SEU347+1.p',unknown),
[] ).
cnf(113,axiom,
( ~ rel_str(u)
| ~ reflexive_relstr(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ related_reflexive(u,v,w)
| empty_carrier(u)
| related(u,v,w) ),
file('SEU347+1.p',unknown),
[] ).
cnf(114,axiom,
( ~ latt_str(u)
| ~ in(v,w)
| ~ element(x,the_carrier(u))
| ~ element(v,the_carrier(u))
| ~ latt_set_smaller(u,x,w)
| empty_carrier(u)
| below(u,x,v) ),
file('SEU347+1.p',unknown),
[] ).
cnf(115,axiom,
( ~ lattice(u)
| ~ latt_str(u)
| ~ related_reflexive(poset_of_lattice(u),cast_to_el_of_LattPOSet(u,v),cast_to_el_of_LattPOSet(u,w))
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| below_refl(u,v,w)
| empty_carrier(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(116,axiom,
( ~ lattice(u)
| ~ latt_str(u)
| ~ below_refl(u,v,w)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| related_reflexive(poset_of_lattice(u),cast_to_el_of_LattPOSet(u,v),cast_to_el_of_LattPOSet(u,w))
| empty_carrier(u) ),
file('SEU347+1.p',unknown),
[] ).
cnf(117,axiom,
( ~ latt_str(u)
| ~ join_absorbing(u)
| ~ meet_absorbing(u)
| ~ meet_commutative(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ below(u,w,v)
| empty_carrier(u)
| below_refl(u,w,v) ),
file('SEU347+1.p',unknown),
[] ).
cnf(118,axiom,
( ~ latt_str(u)
| ~ join_absorbing(u)
| ~ meet_absorbing(u)
| ~ meet_commutative(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ below_refl(u,w,v)
| empty_carrier(u)
| below(u,w,v) ),
file('SEU347+1.p',unknown),
[] ).
cnf(120,plain,
( ~ lattice(u)
| ~ latt_str(u)
| ~ element(v,the_carrier(poset_of_lattice(u)))
| empty_carrier(u)
| element(v,the_carrier(u)) ),
inference(rew,[status(thm),theory(equality)],[98,100]),
[iquote('0:Rew:98.4,100.3')] ).
cnf(121,plain,
( ~ lattice(u)
| ~ latt_str(u)
| ~ element(v,the_carrier(u))
| empty_carrier(u)
| element(v,the_carrier(poset_of_lattice(u))) ),
inference(rew,[status(thm),theory(equality)],[96,101]),
[iquote('0:Rew:96.4,101.3')] ).
cnf(122,plain,
( ~ latt_str(u)
| ~ lattice(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ related_reflexive(poset_of_lattice(u),w,v)
| empty_carrier(u)
| below_refl(u,w,v) ),
inference(rew,[status(thm),theory(equality)],[96,115]),
[iquote('0:Rew:96.4,115.2,96.4,115.2')] ).
cnf(123,plain,
( ~ latt_str(u)
| ~ lattice(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ below_refl(u,w,v)
| empty_carrier(u)
| related_reflexive(poset_of_lattice(u),w,v) ),
inference(rew,[status(thm),theory(equality)],[96,116]),
[iquote('0:Rew:96.4,116.5,96.4,116.5')] ).
cnf(126,plain,
( ~ latt_str(skc13)
| ~ element(u,the_carrier(skc13))
| element(u,the_carrier(poset_of_lattice(skc13)))
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,121]),
[iquote('0:Res:2.0,121.1')] ).
cnf(127,plain,
( ~ latt_str(skc13)
| ~ element(u,the_carrier(poset_of_lattice(skc13)))
| element(u,the_carrier(skc13))
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,120]),
[iquote('0:Res:2.0,120.1')] ).
cnf(130,plain,
( ~ latt_str(skc13)
| empty_carrier(skc13)
| equal(rel_str_of(the_carrier(skc13),k2_lattice3(skc13)),poset_of_lattice(skc13)) ),
inference(res,[status(thm),theory(equality)],[2,92]),
[iquote('0:Res:2.0,92.0')] ).
cnf(132,plain,
( ~ latt_str(skc13)
| relation_of2_as_subset(k2_lattice3(skc13),the_carrier(skc13),the_carrier(skc13))
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,87]),
[iquote('0:Res:2.0,87.0')] ).
cnf(135,plain,
( ~ latt_str(skc13)
| ~ empty_carrier(poset_of_lattice(skc13))
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,80]),
[iquote('0:Res:2.0,80.0')] ).
cnf(139,plain,
( ~ latt_str(skc13)
| rel_str(poset_of_lattice(skc13))
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,71]),
[iquote('0:Res:2.0,71.0')] ).
cnf(140,plain,
( ~ latt_str(skc13)
| strict_rel_str(poset_of_lattice(skc13))
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,75]),
[iquote('0:Res:2.0,75.0')] ).
cnf(141,plain,
( ~ latt_str(skc13)
| reflexive_relstr(poset_of_lattice(skc13))
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,76]),
[iquote('0:Res:2.0,76.0')] ).
cnf(142,plain,
( ~ latt_str(skc13)
| transitive_relstr(poset_of_lattice(skc13))
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,77]),
[iquote('0:Res:2.0,77.0')] ).
cnf(143,plain,
( ~ latt_str(skc13)
| antisymmetric_relstr(poset_of_lattice(skc13))
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,78]),
[iquote('0:Res:2.0,78.0')] ).
cnf(144,plain,
( ~ latt_str(skc13)
| join_commutative(skc13)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,56]),
[iquote('0:Res:2.0,56.1')] ).
cnf(145,plain,
( ~ latt_str(skc13)
| join_associative(skc13)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,57]),
[iquote('0:Res:2.0,57.1')] ).
cnf(146,plain,
( ~ latt_str(skc13)
| meet_commutative(skc13)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,58]),
[iquote('0:Res:2.0,58.1')] ).
cnf(147,plain,
( ~ latt_str(skc13)
| meet_associative(skc13)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,59]),
[iquote('0:Res:2.0,59.1')] ).
cnf(148,plain,
( ~ latt_str(skc13)
| meet_absorbing(skc13)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,60]),
[iquote('0:Res:2.0,60.1')] ).
cnf(149,plain,
( ~ latt_str(skc13)
| join_absorbing(skc13)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[2,61]),
[iquote('0:Res:2.0,61.1')] ).
cnf(183,plain,
meet_semilatt_str(skc13),
inference(res,[status(thm),theory(equality)],[1,30]),
[iquote('0:Res:1.0,30.0')] ).
cnf(184,plain,
join_semilatt_str(skc13),
inference(res,[status(thm),theory(equality)],[1,31]),
[iquote('0:Res:1.0,31.0')] ).
cnf(223,plain,
( ~ meet_commutative(skc13)
| ~ meet_absorbing(skc13)
| ~ join_absorbing(skc13)
| ~ latt_str(skc13)
| ~ element(u,the_carrier(skc13))
| ~ below_refl(skc13,skc14,u)
| below(skc13,skc14,u)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[24,118]),
[iquote('0:Res:24.0,118.4')] ).
cnf(224,plain,
( ~ meet_commutative(skc13)
| ~ meet_absorbing(skc13)
| ~ join_absorbing(skc13)
| ~ latt_str(skc13)
| ~ element(u,the_carrier(skc13))
| ~ below(skc13,skc14,u)
| below_refl(skc13,skc14,u)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[24,117]),
[iquote('0:Res:24.0,117.4')] ).
cnf(225,plain,
( ~ lattice(skc13)
| ~ latt_str(skc13)
| ~ below_refl(skc13,skc14,u)
| ~ element(u,the_carrier(skc13))
| related_reflexive(poset_of_lattice(skc13),skc14,u)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[24,123]),
[iquote('0:Res:24.0,123.3')] ).
cnf(226,plain,
( ~ lattice(skc13)
| ~ latt_str(skc13)
| ~ related_reflexive(poset_of_lattice(skc13),skc14,u)
| ~ element(u,the_carrier(skc13))
| below_refl(skc13,skc14,u)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[24,122]),
[iquote('0:Res:24.0,122.3')] ).
cnf(232,plain,
( ~ latt_str(skc13)
| ~ below(skc13,skc14,skf8(skc14,u,skc13))
| latt_set_smaller(skc13,skc14,u)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[24,104]),
[iquote('0:Res:24.0,104.2')] ).
cnf(235,plain,
( ~ latt_str(skc13)
| ~ lattice(skc13)
| element(skc14,the_carrier(poset_of_lattice(skc13)))
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[24,121]),
[iquote('0:Res:24.0,121.2')] ).
cnf(236,plain,
( ~ lattice(skc13)
| ~ latt_str(skc13)
| empty_carrier(skc13)
| equal(cast_to_el_of_LattPOSet(skc13,skc14),skc14) ),
inference(res,[status(thm),theory(equality)],[24,96]),
[iquote('0:Res:24.0,96.2')] ).
cnf(239,plain,
( ~ latt_str(skc13)
| ~ element(u,the_carrier(skc13))
| ~ in(u,v)
| ~ latt_set_smaller(skc13,skc14,v)
| below(skc13,skc14,u)
| empty_carrier(skc13) ),
inference(res,[status(thm),theory(equality)],[24,114]),
[iquote('0:Res:24.0,114.4')] ).
cnf(248,plain,
join_commutative(skc13),
inference(mrr,[status(thm)],[144,1,18]),
[iquote('0:MRR:144.0,144.2,1.0,18.0')] ).
cnf(249,plain,
join_associative(skc13),
inference(mrr,[status(thm)],[145,1,18]),
[iquote('0:MRR:145.0,145.2,1.0,18.0')] ).
cnf(250,plain,
meet_commutative(skc13),
inference(mrr,[status(thm)],[146,1,18]),
[iquote('0:MRR:146.0,146.2,1.0,18.0')] ).
cnf(251,plain,
meet_associative(skc13),
inference(mrr,[status(thm)],[147,1,18]),
[iquote('0:MRR:147.0,147.2,1.0,18.0')] ).
cnf(252,plain,
meet_absorbing(skc13),
inference(mrr,[status(thm)],[148,1,18]),
[iquote('0:MRR:148.0,148.2,1.0,18.0')] ).
cnf(253,plain,
join_absorbing(skc13),
inference(mrr,[status(thm)],[149,1,18]),
[iquote('0:MRR:149.0,149.2,1.0,18.0')] ).
cnf(258,plain,
rel_str(poset_of_lattice(skc13)),
inference(mrr,[status(thm)],[139,1,18]),
[iquote('0:MRR:139.0,139.2,1.0,18.0')] ).
cnf(259,plain,
strict_rel_str(poset_of_lattice(skc13)),
inference(mrr,[status(thm)],[140,1,18]),
[iquote('0:MRR:140.0,140.2,1.0,18.0')] ).
cnf(260,plain,
reflexive_relstr(poset_of_lattice(skc13)),
inference(mrr,[status(thm)],[141,1,18]),
[iquote('0:MRR:141.0,141.2,1.0,18.0')] ).
cnf(261,plain,
transitive_relstr(poset_of_lattice(skc13)),
inference(mrr,[status(thm)],[142,1,18]),
[iquote('0:MRR:142.0,142.2,1.0,18.0')] ).
cnf(262,plain,
antisymmetric_relstr(poset_of_lattice(skc13)),
inference(mrr,[status(thm)],[143,1,18]),
[iquote('0:MRR:143.0,143.2,1.0,18.0')] ).
cnf(263,plain,
~ empty_carrier(poset_of_lattice(skc13)),
inference(mrr,[status(thm)],[135,1,18]),
[iquote('0:MRR:135.0,135.2,1.0,18.0')] ).
cnf(266,plain,
relation_of2_as_subset(k2_lattice3(skc13),the_carrier(skc13),the_carrier(skc13)),
inference(mrr,[status(thm)],[132,1,18]),
[iquote('0:MRR:132.0,132.2,1.0,18.0')] ).
cnf(268,plain,
equal(rel_str_of(the_carrier(skc13),k2_lattice3(skc13)),poset_of_lattice(skc13)),
inference(mrr,[status(thm)],[130,1,18]),
[iquote('0:MRR:130.0,130.1,1.0,18.0')] ).
cnf(269,plain,
element(skc14,the_carrier(poset_of_lattice(skc13))),
inference(mrr,[status(thm)],[235,1,2,18]),
[iquote('0:MRR:235.0,235.1,235.3,1.0,2.0,18.0')] ).
cnf(270,plain,
equal(cast_to_el_of_LattPOSet(skc13,skc14),skc14),
inference(mrr,[status(thm)],[236,2,1,18]),
[iquote('0:MRR:236.0,236.1,236.2,2.0,1.0,18.0')] ).
cnf(271,plain,
( ~ latt_set_smaller(skc13,skc14,skc15)
| ~ relstr_element_smaller(poset_of_lattice(skc13),skc15,skc14) ),
inference(rew,[status(thm),theory(equality)],[270,83]),
[iquote('0:Rew:270.0,83.1')] ).
cnf(272,plain,
( latt_set_smaller(skc13,skc14,skc15)
| relstr_element_smaller(poset_of_lattice(skc13),skc15,skc14) ),
inference(rew,[status(thm),theory(equality)],[270,63]),
[iquote('0:Rew:270.0,63.1')] ).
cnf(273,plain,
( ~ element(u,the_carrier(skc13))
| element(u,the_carrier(poset_of_lattice(skc13))) ),
inference(mrr,[status(thm)],[126,1,18]),
[iquote('0:MRR:126.0,126.3,1.0,18.0')] ).
cnf(274,plain,
( ~ element(u,the_carrier(poset_of_lattice(skc13)))
| element(u,the_carrier(skc13)) ),
inference(mrr,[status(thm)],[127,1,18]),
[iquote('0:MRR:127.0,127.3,1.0,18.0')] ).
cnf(279,plain,
( ~ below(skc13,skc14,skf8(skc14,u,skc13))
| latt_set_smaller(skc13,skc14,u) ),
inference(mrr,[status(thm)],[232,1,18]),
[iquote('0:MRR:232.0,232.3,1.0,18.0')] ).
cnf(289,plain,
( ~ in(u,v)
| ~ element(u,the_carrier(skc13))
| ~ latt_set_smaller(skc13,skc14,v)
| below(skc13,skc14,u) ),
inference(mrr,[status(thm)],[239,1,18]),
[iquote('0:MRR:239.0,239.5,1.0,18.0')] ).
cnf(291,plain,
( ~ element(u,the_carrier(skc13))
| ~ related_reflexive(poset_of_lattice(skc13),skc14,u)
| below_refl(skc13,skc14,u) ),
inference(mrr,[status(thm)],[226,2,1,18]),
[iquote('0:MRR:226.0,226.1,226.5,2.0,1.0,18.0')] ).
cnf(292,plain,
( ~ element(u,the_carrier(skc13))
| ~ below_refl(skc13,skc14,u)
| related_reflexive(poset_of_lattice(skc13),skc14,u) ),
inference(mrr,[status(thm)],[225,2,1,18]),
[iquote('0:MRR:225.0,225.1,225.5,2.0,1.0,18.0')] ).
cnf(298,plain,
( ~ element(u,the_carrier(skc13))
| ~ below(skc13,skc14,u)
| below_refl(skc13,skc14,u) ),
inference(mrr,[status(thm)],[224,250,252,253,1,18]),
[iquote('0:MRR:224.0,224.1,224.2,224.3,224.7,250.0,252.0,253.0,1.0,18.0')] ).
cnf(299,plain,
( ~ element(u,the_carrier(skc13))
| ~ below_refl(skc13,skc14,u)
| below(skc13,skc14,u) ),
inference(mrr,[status(thm)],[223,250,252,253,1,18]),
[iquote('0:MRR:223.0,223.1,223.2,223.3,223.7,250.0,252.0,253.0,1.0,18.0')] ).
cnf(331,plain,
latt_set_smaller(skc13,skc14,skc15),
inference(spt,[spt(split,[position(s1)])],[272]),
[iquote('1:Spt:272.0')] ).
cnf(332,plain,
~ relstr_element_smaller(poset_of_lattice(skc13),skc15,skc14),
inference(mrr,[status(thm)],[271,331]),
[iquote('1:MRR:271.0,331.0')] ).
cnf(376,plain,
relation_of2(k2_lattice3(skc13),the_carrier(skc13),the_carrier(skc13)),
inference(res,[status(thm),theory(equality)],[266,52]),
[iquote('0:Res:266.0,52.0')] ).
cnf(401,plain,
element(skf9(u,v,poset_of_lattice(skc13)),the_carrier(skc13)),
inference(res,[status(thm),theory(equality)],[40,274]),
[iquote('0:Res:40.0,274.0')] ).
cnf(774,plain,
( ~ equal(rel_str_of(u,v),poset_of_lattice(skc13))
| ~ relation_of2(k2_lattice3(skc13),the_carrier(skc13),the_carrier(skc13))
| equal(the_carrier(skc13),u) ),
inference(spl,[status(thm),theory(equality)],[268,93]),
[iquote('0:SpL:268.0,93.0')] ).
cnf(780,plain,
( ~ equal(rel_str_of(u,v),poset_of_lattice(skc13))
| equal(the_carrier(skc13),u) ),
inference(mrr,[status(thm)],[774,376]),
[iquote('0:MRR:774.1,376.0')] ).
cnf(1053,plain,
( ~ strict_rel_str(u)
| ~ rel_str(u)
| ~ equal(u,poset_of_lattice(skc13))
| equal(the_carrier(skc13),the_carrier(u)) ),
inference(spl,[status(thm),theory(equality)],[84,780]),
[iquote('0:SpL:84.2,780.0')] ).
cnf(1225,plain,
( ~ rel_str(poset_of_lattice(skc13))
| ~ in(u,v)
| ~ element(u,the_carrier(poset_of_lattice(skc13)))
| ~ relstr_element_smaller(poset_of_lattice(skc13),v,skc14)
| related(poset_of_lattice(skc13),skc14,u) ),
inference(res,[status(thm),theory(equality)],[269,111]),
[iquote('0:Res:269.0,111.2')] ).
cnf(1247,plain,
( ~ in(u,v)
| ~ element(u,the_carrier(poset_of_lattice(skc13)))
| ~ relstr_element_smaller(poset_of_lattice(skc13),v,skc14)
| related(poset_of_lattice(skc13),skc14,u) ),
inference(ssi,[status(thm)],[1225,259,262,261,260,258]),
[iquote('0:SSi:1225.0,259.0,262.0,261.0,260.0,258.0')] ).
cnf(1815,plain,
( ~ rel_str(poset_of_lattice(skc13))
| ~ reflexive_relstr(poset_of_lattice(skc13))
| ~ element(u,the_carrier(skc13))
| ~ below_refl(skc13,skc14,u)
| ~ element(skc14,the_carrier(poset_of_lattice(skc13)))
| ~ element(u,the_carrier(poset_of_lattice(skc13)))
| empty_carrier(poset_of_lattice(skc13))
| related(poset_of_lattice(skc13),skc14,u) ),
inference(res,[status(thm),theory(equality)],[292,113]),
[iquote('0:Res:292.2,113.4')] ).
cnf(1817,plain,
( ~ element(u,the_carrier(skc13))
| ~ below_refl(skc13,skc14,u)
| ~ element(skc14,the_carrier(poset_of_lattice(skc13)))
| ~ element(u,the_carrier(poset_of_lattice(skc13)))
| empty_carrier(poset_of_lattice(skc13))
| related(poset_of_lattice(skc13),skc14,u) ),
inference(ssi,[status(thm)],[1815,259,262,261,260,258]),
[iquote('0:SSi:1815.1,1815.0,259.0,262.0,261.0,260.0,258.0,259.0,262.0,261.0,260.0,258.0')] ).
cnf(1818,plain,
( ~ below_refl(skc13,skc14,u)
| ~ element(u,the_carrier(poset_of_lattice(skc13)))
| related(poset_of_lattice(skc13),skc14,u) ),
inference(mrr,[status(thm)],[1817,274,269,263]),
[iquote('0:MRR:1817.0,1817.2,1817.4,274.1,269.0,263.0')] ).
cnf(1877,plain,
( ~ rel_str(poset_of_lattice(skc13))
| ~ reflexive_relstr(poset_of_lattice(skc13))
| ~ element(skc14,the_carrier(poset_of_lattice(skc13)))
| ~ element(u,the_carrier(poset_of_lattice(skc13)))
| ~ related(poset_of_lattice(skc13),skc14,u)
| ~ element(u,the_carrier(skc13))
| empty_carrier(poset_of_lattice(skc13))
| below_refl(skc13,skc14,u) ),
inference(res,[status(thm),theory(equality)],[112,291]),
[iquote('0:Res:112.6,291.1')] ).
cnf(1881,plain,
( ~ element(skc14,the_carrier(poset_of_lattice(skc13)))
| ~ element(u,the_carrier(poset_of_lattice(skc13)))
| ~ related(poset_of_lattice(skc13),skc14,u)
| ~ element(u,the_carrier(skc13))
| empty_carrier(poset_of_lattice(skc13))
| below_refl(skc13,skc14,u) ),
inference(ssi,[status(thm)],[1877,259,262,261,260,258]),
[iquote('0:SSi:1877.1,1877.0,259.0,262.0,261.0,260.0,258.0,259.0,262.0,261.0,260.0,258.0')] ).
cnf(1882,plain,
( ~ related(poset_of_lattice(skc13),skc14,u)
| ~ element(u,the_carrier(skc13))
| below_refl(skc13,skc14,u) ),
inference(mrr,[status(thm)],[1881,269,273,263]),
[iquote('0:MRR:1881.0,1881.1,1881.4,269.0,273.1,263.0')] ).
cnf(2146,plain,
( ~ in(skf9(u,v,poset_of_lattice(skc13)),w)
| ~ latt_set_smaller(skc13,skc14,w)
| below(skc13,skc14,skf9(u,v,poset_of_lattice(skc13))) ),
inference(res,[status(thm),theory(equality)],[401,289]),
[iquote('0:Res:401.0,289.1')] ).
cnf(4134,plain,
( ~ rel_str(poset_of_lattice(skc13))
| ~ below_refl(skc13,skc14,skf9(skc14,u,poset_of_lattice(skc13)))
| ~ element(skf9(skc14,u,poset_of_lattice(skc13)),the_carrier(poset_of_lattice(skc13)))
| ~ element(skc14,the_carrier(poset_of_lattice(skc13)))
| relstr_element_smaller(poset_of_lattice(skc13),u,skc14) ),
inference(res,[status(thm),theory(equality)],[1818,102]),
[iquote('0:Res:1818.2,102.2')] ).
cnf(4138,plain,
( ~ below_refl(skc13,skc14,skf9(skc14,u,poset_of_lattice(skc13)))
| ~ element(skf9(skc14,u,poset_of_lattice(skc13)),the_carrier(poset_of_lattice(skc13)))
| ~ element(skc14,the_carrier(poset_of_lattice(skc13)))
| relstr_element_smaller(poset_of_lattice(skc13),u,skc14) ),
inference(ssi,[status(thm)],[4134,259,262,261,260,258]),
[iquote('0:SSi:4134.0,259.0,262.0,261.0,260.0,258.0')] ).
cnf(4139,plain,
( ~ below_refl(skc13,skc14,skf9(skc14,u,poset_of_lattice(skc13)))
| relstr_element_smaller(poset_of_lattice(skc13),u,skc14) ),
inference(mrr,[status(thm)],[4138,40,269]),
[iquote('0:MRR:4138.1,4138.2,40.0,269.0')] ).
cnf(4148,plain,
( ~ element(skf9(skc14,u,poset_of_lattice(skc13)),the_carrier(skc13))
| ~ below(skc13,skc14,skf9(skc14,u,poset_of_lattice(skc13)))
| relstr_element_smaller(poset_of_lattice(skc13),u,skc14) ),
inference(res,[status(thm),theory(equality)],[298,4139]),
[iquote('0:Res:298.2,4139.0')] ).
cnf(4151,plain,
( ~ below(skc13,skc14,skf9(skc14,u,poset_of_lattice(skc13)))
| relstr_element_smaller(poset_of_lattice(skc13),u,skc14) ),
inference(mrr,[status(thm)],[4148,401]),
[iquote('0:MRR:4148.0,401.0')] ).
cnf(8042,plain,
( ~ element(u,the_carrier(skc13))
| ~ in(u,v)
| ~ relstr_element_smaller(poset_of_lattice(skc13),v,skc14)
| related(poset_of_lattice(skc13),skc14,u) ),
inference(res,[status(thm),theory(equality)],[273,1247]),
[iquote('0:Res:273.1,1247.1')] ).
cnf(13704,plain,
( ~ strict_rel_str(poset_of_lattice(skc13))
| ~ rel_str(poset_of_lattice(skc13))
| equal(the_carrier(poset_of_lattice(skc13)),the_carrier(skc13)) ),
inference(eqr,[status(thm),theory(equality)],[1053]),
[iquote('0:EqR:1053.2')] ).
cnf(13705,plain,
equal(the_carrier(poset_of_lattice(skc13)),the_carrier(skc13)),
inference(ssi,[status(thm)],[13704,259,262,261,260,258]),
[iquote('0:SSi:13704.1,13704.0,259.0,262.0,261.0,260.0,258.0,259.0,262.0,261.0,260.0,258.0')] ).
cnf(18144,plain,
( ~ rel_str(poset_of_lattice(skc13))
| ~ element(u,the_carrier(poset_of_lattice(skc13)))
| ~ latt_set_smaller(skc13,skc14,v)
| relstr_element_smaller(poset_of_lattice(skc13),v,u)
| below(skc13,skc14,skf9(u,v,poset_of_lattice(skc13))) ),
inference(res,[status(thm),theory(equality)],[97,2146]),
[iquote('0:Res:97.2,2146.0')] ).
cnf(18146,plain,
( ~ rel_str(poset_of_lattice(skc13))
| ~ element(u,the_carrier(skc13))
| ~ latt_set_smaller(skc13,skc14,v)
| relstr_element_smaller(poset_of_lattice(skc13),v,u)
| below(skc13,skc14,skf9(u,v,poset_of_lattice(skc13))) ),
inference(rew,[status(thm),theory(equality)],[13705,18144]),
[iquote('0:Rew:13705.0,18144.1')] ).
cnf(18147,plain,
( ~ element(u,the_carrier(skc13))
| ~ latt_set_smaller(skc13,skc14,v)
| relstr_element_smaller(poset_of_lattice(skc13),v,u)
| below(skc13,skc14,skf9(u,v,poset_of_lattice(skc13))) ),
inference(ssi,[status(thm)],[18146,259,262,261,260,258]),
[iquote('0:SSi:18146.0,259.0,262.0,261.0,260.0,258.0')] ).
cnf(52981,plain,
( ~ element(skc14,the_carrier(skc13))
| ~ latt_set_smaller(skc13,skc14,u)
| relstr_element_smaller(poset_of_lattice(skc13),u,skc14)
| relstr_element_smaller(poset_of_lattice(skc13),u,skc14) ),
inference(res,[status(thm),theory(equality)],[18147,4151]),
[iquote('0:Res:18147.3,4151.0')] ).
cnf(52983,plain,
( ~ element(skc14,the_carrier(skc13))
| ~ latt_set_smaller(skc13,skc14,u)
| relstr_element_smaller(poset_of_lattice(skc13),u,skc14) ),
inference(obv,[status(thm),theory(equality)],[52981]),
[iquote('0:Obv:52981.2')] ).
cnf(52984,plain,
( ~ latt_set_smaller(skc13,skc14,u)
| relstr_element_smaller(poset_of_lattice(skc13),u,skc14) ),
inference(mrr,[status(thm)],[52983,24]),
[iquote('0:MRR:52983.0,24.0')] ).
cnf(52987,plain,
~ latt_set_smaller(skc13,skc14,skc15),
inference(res,[status(thm),theory(equality)],[52984,332]),
[iquote('1:Res:52984.1,332.0')] ).
cnf(53009,plain,
$false,
inference(mrr,[status(thm)],[52987,331]),
[iquote('1:MRR:52987.0,331.0')] ).
cnf(53010,plain,
~ latt_set_smaller(skc13,skc14,skc15),
inference(spt,[spt(split,[position(sa)])],[53009,331]),
[iquote('1:Spt:53009.0,272.0,331.0')] ).
cnf(53011,plain,
relstr_element_smaller(poset_of_lattice(skc13),skc15,skc14),
inference(spt,[spt(split,[position(s2)])],[272]),
[iquote('1:Spt:53009.0,272.1')] ).
cnf(53556,plain,
( ~ element(u,the_carrier(skc13))
| ~ in(u,skc15)
| related(poset_of_lattice(skc13),skc14,u) ),
inference(res,[status(thm),theory(equality)],[53011,8042]),
[iquote('1:Res:53011.0,8042.2')] ).
cnf(56969,plain,
( ~ element(u,the_carrier(skc13))
| ~ in(u,skc15)
| ~ element(u,the_carrier(skc13))
| below_refl(skc13,skc14,u) ),
inference(res,[status(thm),theory(equality)],[53556,1882]),
[iquote('1:Res:53556.2,1882.0')] ).
cnf(56972,plain,
( ~ in(u,skc15)
| ~ element(u,the_carrier(skc13))
| below_refl(skc13,skc14,u) ),
inference(obv,[status(thm),theory(equality)],[56969]),
[iquote('1:Obv:56969.0')] ).
cnf(56991,plain,
( ~ in(u,skc15)
| ~ element(u,the_carrier(skc13))
| ~ element(u,the_carrier(skc13))
| below(skc13,skc14,u) ),
inference(res,[status(thm),theory(equality)],[56972,299]),
[iquote('1:Res:56972.2,299.1')] ).
cnf(56998,plain,
( ~ in(u,skc15)
| ~ element(u,the_carrier(skc13))
| below(skc13,skc14,u) ),
inference(obv,[status(thm),theory(equality)],[56991]),
[iquote('1:Obv:56991.1')] ).
cnf(57134,plain,
( ~ in(skf8(skc14,u,skc13),skc15)
| ~ element(skf8(skc14,u,skc13),the_carrier(skc13))
| latt_set_smaller(skc13,skc14,u) ),
inference(res,[status(thm),theory(equality)],[56998,279]),
[iquote('1:Res:56998.2,279.0')] ).
cnf(57138,plain,
( ~ in(skf8(skc14,u,skc13),skc15)
| latt_set_smaller(skc13,skc14,u) ),
inference(mrr,[status(thm)],[57134,39]),
[iquote('1:MRR:57134.1,39.0')] ).
cnf(57148,plain,
( ~ latt_str(skc13)
| ~ element(skc14,the_carrier(skc13))
| empty_carrier(skc13)
| latt_set_smaller(skc13,skc14,skc15)
| latt_set_smaller(skc13,skc14,skc15) ),
inference(res,[status(thm),theory(equality)],[103,57138]),
[iquote('1:Res:103.3,57138.0')] ).
cnf(57173,plain,
( ~ latt_str(skc13)
| ~ element(skc14,the_carrier(skc13))
| empty_carrier(skc13)
| latt_set_smaller(skc13,skc14,skc15) ),
inference(obv,[status(thm),theory(equality)],[57148]),
[iquote('1:Obv:57148.3')] ).
cnf(57174,plain,
( ~ element(skc14,the_carrier(skc13))
| empty_carrier(skc13)
| latt_set_smaller(skc13,skc14,skc15) ),
inference(ssi,[status(thm)],[57173,2,1,251,249,248,184,183,253,252,250]),
[iquote('1:SSi:57173.0,2.0,1.0,251.0,249.0,248.0,184.0,183.0,253.0,252.0,250.0')] ).
cnf(57175,plain,
$false,
inference(mrr,[status(thm)],[57174,24,18,53010]),
[iquote('1:MRR:57174.0,57174.1,57174.2,24.0,18.0,53010.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU347+1 : TPTP v8.1.0. Released v3.3.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.14/0.34 % Computer : n012.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 : Mon Jun 20 05:20:37 EDT 2022
% 0.14/0.34 % CPUTime :
% 123.72/123.87
% 123.72/123.87 SPASS V 3.9
% 123.72/123.87 SPASS beiseite: Proof found.
% 123.72/123.87 % SZS status Theorem
% 123.72/123.87 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 123.72/123.87 SPASS derived 43465 clauses, backtracked 4418 clauses, performed 38 splits and kept 22002 clauses.
% 123.72/123.87 SPASS allocated 165433 KBytes.
% 123.72/123.87 SPASS spent 0:02:03.47 on the problem.
% 123.72/123.87 0:00:00.04 for the input.
% 123.72/123.87 0:00:00.04 for the FLOTTER CNF translation.
% 123.72/123.87 0:00:01.33 for inferences.
% 123.72/123.87 0:00:04.08 for the backtracking.
% 123.72/123.87 0:1:56.28 for the reduction.
% 123.72/123.87
% 123.72/123.87
% 123.72/123.87 Here is a proof with depth 8, length 144 :
% 123.72/123.87 % SZS output start Refutation
% See solution above
% 131.40/131.56 Formulae used in the proof : t28_lattice3 dt_l3_lattices d16_lattice3 existence_m1_subset_1 d8_lattice3 redefinition_m2_relset_1 cc1_lattices dt_k3_lattice3 fc4_lattice3 abstractness_v1_orders_2 dt_k2_lattice3 d2_lattice3 free_g1_orders_2 d3_lattice3 d4_lattice3 dt_k5_lattice3 dt_k4_lattice3 redefinition_r3_orders_2 t7_lattice3 redefinition_r3_lattices
% 131.40/131.56
%------------------------------------------------------------------------------