%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SEU343+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n015.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:26 EDT 2022
% Result : Theorem 148.87s 149.11s
% Output : Refutation 165.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 33
% Syntax : Number of clauses : 79 ( 17 unt; 26 nHn; 79 RR)
% Number of literals : 325 ( 0 equ; 207 neg)
% Maximal clause size : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 10 con; 0-6 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(13,axiom,
latt_str(boole_lattice(u)),
file('SEU343+1.p',unknown),
[] ).
cnf(14,axiom,
strict_latt_str(boole_lattice(u)),
file('SEU343+1.p',unknown),
[] ).
cnf(15,axiom,
empty(skf14(u)),
file('SEU343+1.p',unknown),
[] ).
cnf(21,axiom,
~ empty_carrier(boole_lattice(u)),
file('SEU343+1.p',unknown),
[] ).
cnf(22,axiom,
~ empty(powerset(u)),
file('SEU343+1.p',unknown),
[] ).
cnf(24,axiom,
element(skc14,the_carrier(boole_lattice(skc12))),
file('SEU343+1.p',unknown),
[] ).
cnf(25,axiom,
element(skc13,the_carrier(boole_lattice(skc12))),
file('SEU343+1.p',unknown),
[] ).
cnf(28,axiom,
( ~ latt_str(u)
| meet_semilatt_str(u) ),
file('SEU343+1.p',unknown),
[] ).
cnf(29,axiom,
( ~ latt_str(u)
| join_semilatt_str(u) ),
file('SEU343+1.p',unknown),
[] ).
cnf(34,axiom,
element(skf14(u),powerset(u)),
file('SEU343+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ meet_semilatt_str(u)
| function(the_L_meet(u)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ join_semilatt_str(u)
| function(the_L_join(u)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ empty(u)
| equal(u,empty_set) ),
file('SEU343+1.p',unknown),
[] ).
cnf(52,axiom,
( ~ empty(u)
| ~ in(v,u) ),
file('SEU343+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ element(u,powerset(v))
| subset(u,v) ),
file('SEU343+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ subset(u,v)
| element(u,powerset(v)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(56,axiom,
( ~ element(u,powerset(cartesian_product2(v,w)))
| relation(u) ),
file('SEU343+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ relation_of2_as_subset(u,v,w)
| relation_of2(u,v,w) ),
file('SEU343+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ element(u,v)
| empty(v)
| in(u,v) ),
file('SEU343+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ relation_of2_as_subset(u,v,w)
| element(u,powerset(cartesian_product2(v,w))) ),
file('SEU343+1.p',unknown),
[] ).
cnf(70,axiom,
( ~ meet_semilatt_str(u)
| quasi_total(the_L_meet(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(71,axiom,
( ~ meet_semilatt_str(u)
| relation_of2_as_subset(the_L_meet(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(72,axiom,
( ~ join_semilatt_str(u)
| quasi_total(the_L_join(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ join_semilatt_str(u)
| relation_of2_as_subset(the_L_join(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(76,axiom,
( ~ strict_latt_str(u)
| ~ latt_str(u)
| ~ equal(u,boole_lattice(v))
| equal(the_carrier(u),powerset(v)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ element(u,powerset(v))
| ~ element(w,powerset(v))
| equal(subset_union2(v,w,u),set_union2(w,u)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(80,axiom,
( ~ element(u,powerset(v))
| ~ element(w,powerset(v))
| equal(subset_intersection2(v,w,u),set_intersection2(w,u)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(83,axiom,
( ~ equal(meet(boole_lattice(skc12),skc13,skc14),set_intersection2(skc13,skc14))
| ~ equal(join(boole_lattice(skc12),skc13,skc14),set_union2(skc13,skc14)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(86,axiom,
( ~ meet_semilatt_str(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty_carrier(u)
| equal(apply_binary_as_element(the_carrier(u),the_carrier(u),the_carrier(u),the_L_meet(u),w,v),meet(u,w,v)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(87,axiom,
( ~ join_semilatt_str(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty_carrier(u)
| equal(apply_binary_as_element(the_carrier(u),the_carrier(u),the_carrier(u),the_L_join(u),w,v),join(u,w,v)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(88,axiom,
( ~ latt_str(u)
| ~ strict_latt_str(u)
| ~ equal(u,boole_lattice(v))
| ~ element(w,powerset(v))
| ~ element(x,powerset(v))
| equal(apply_binary(the_L_meet(u),w,x),subset_intersection2(v,w,x)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(89,axiom,
( ~ latt_str(u)
| ~ strict_latt_str(u)
| ~ equal(u,boole_lattice(v))
| ~ element(w,powerset(v))
| ~ element(x,powerset(v))
| equal(apply_binary(the_L_join(u),w,x),subset_union2(v,w,x)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(93,axiom,
( ~ function(u)
| ~ element(v,w)
| ~ element(x,y)
| ~ quasi_total(u,cartesian_product2(w,y),z)
| ~ relation_of2(u,cartesian_product2(w,y),z)
| empty(y)
| empty(w)
| equal(apply_binary_as_element(w,y,z,u,v,x),apply_binary(u,v,x)) ),
file('SEU343+1.p',unknown),
[] ).
cnf(105,plain,
( ~ strict_latt_str(u)
| ~ latt_str(u)
| ~ element(v,powerset(w))
| ~ element(x,powerset(w))
| ~ equal(u,boole_lattice(w))
| equal(apply_binary(the_L_meet(u),x,v),set_intersection2(x,v)) ),
inference(rew,[status(thm),theory(equality)],[80,88]),
[iquote('0:Rew:80.2,88.5')] ).
cnf(106,plain,
( ~ strict_latt_str(u)
| ~ latt_str(u)
| ~ element(v,powerset(w))
| ~ element(x,powerset(w))
| ~ equal(u,boole_lattice(w))
| equal(apply_binary(the_L_join(u),x,v),set_union2(x,v)) ),
inference(rew,[status(thm),theory(equality)],[79,89]),
[iquote('0:Rew:79.2,89.5')] ).
cnf(164,plain,
equal(skf14(u),empty_set),
inference(ems,[status(thm)],[45,15]),
[iquote('0:EmS:45.0,15.0')] ).
cnf(169,plain,
element(empty_set,powerset(u)),
inference(rew,[status(thm),theory(equality)],[164,34]),
[iquote('0:Rew:164.0,34.0')] ).
cnf(310,plain,
( empty(powerset(u))
| in(empty_set,powerset(u)) ),
inference(res,[status(thm),theory(equality)],[169,62]),
[iquote('0:Res:169.0,62.0')] ).
cnf(323,plain,
in(empty_set,powerset(u)),
inference(mrr,[status(thm)],[310,22]),
[iquote('0:MRR:310.0,22.0')] ).
cnf(334,plain,
~ empty(powerset(u)),
inference(res,[status(thm),theory(equality)],[323,52]),
[iquote('0:Res:323.0,52.1')] ).
cnf(381,plain,
( ~ relation_of2_as_subset(u,v,w)
| relation(u) ),
inference(res,[status(thm),theory(equality)],[65,56]),
[iquote('0:Res:65.1,56.0')] ).
cnf(443,plain,
( ~ join_semilatt_str(u)
| relation(the_L_join(u)) ),
inference(res,[status(thm),theory(equality)],[73,381]),
[iquote('0:Res:73.1,381.0')] ).
cnf(444,plain,
( ~ join_semilatt_str(u)
| relation_of2(the_L_join(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u)) ),
inference(res,[status(thm),theory(equality)],[73,60]),
[iquote('0:Res:73.1,60.0')] ).
cnf(449,plain,
( ~ meet_semilatt_str(u)
| relation(the_L_meet(u)) ),
inference(res,[status(thm),theory(equality)],[71,381]),
[iquote('0:Res:71.1,381.0')] ).
cnf(450,plain,
( ~ meet_semilatt_str(u)
| relation_of2(the_L_meet(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u)) ),
inference(res,[status(thm),theory(equality)],[71,60]),
[iquote('0:Res:71.1,60.0')] ).
cnf(503,plain,
( ~ strict_latt_str(boole_lattice(u))
| ~ latt_str(boole_lattice(u))
| equal(the_carrier(boole_lattice(u)),powerset(u)) ),
inference(eqr,[status(thm),theory(equality)],[76]),
[iquote('0:EqR:76.2')] ).
cnf(504,plain,
equal(the_carrier(boole_lattice(u)),powerset(u)),
inference(ssi,[status(thm)],[503,14,13]),
[iquote('0:SSi:503.1,503.0,14.0,13.0,14.0,13.0')] ).
cnf(506,plain,
element(skc14,powerset(skc12)),
inference(rew,[status(thm),theory(equality)],[504,24]),
[iquote('0:Rew:504.0,24.0')] ).
cnf(507,plain,
element(skc13,powerset(skc12)),
inference(rew,[status(thm),theory(equality)],[504,25]),
[iquote('0:Rew:504.0,25.0')] ).
cnf(556,plain,
subset(skc14,skc12),
inference(res,[status(thm),theory(equality)],[506,54]),
[iquote('0:Res:506.0,54.0')] ).
cnf(792,plain,
( ~ strict_latt_str(u)
| ~ latt_str(u)
| ~ subset(v,w)
| ~ element(x,powerset(w))
| ~ equal(u,boole_lattice(w))
| equal(apply_binary(the_L_join(u),x,v),set_union2(x,v)) ),
inference(res,[status(thm),theory(equality)],[55,106]),
[iquote('0:Res:55.1,106.2')] ).
cnf(818,plain,
( ~ strict_latt_str(u)
| ~ latt_str(u)
| ~ subset(v,w)
| ~ element(x,powerset(w))
| ~ equal(u,boole_lattice(w))
| equal(apply_binary(the_L_meet(u),x,v),set_intersection2(x,v)) ),
inference(res,[status(thm),theory(equality)],[55,105]),
[iquote('0:Res:55.1,105.2')] ).
cnf(953,plain,
( ~ function(the_L_join(u))
| ~ join_semilatt_str(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ quasi_total(the_L_join(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ relation_of2(the_L_join(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ element(v,the_carrier(u))
| empty(the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(apply_binary(the_L_join(u),v,w),join(u,v,w)) ),
inference(spr,[status(thm),theory(equality)],[93,87]),
[iquote('0:SpR:93.7,87.4')] ).
cnf(954,plain,
( ~ function(the_L_meet(u))
| ~ meet_semilatt_str(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ quasi_total(the_L_meet(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ relation_of2(the_L_meet(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ element(v,the_carrier(u))
| empty(the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(apply_binary(the_L_meet(u),v,w),meet(u,v,w)) ),
inference(spr,[status(thm),theory(equality)],[93,86]),
[iquote('0:SpR:93.7,86.4')] ).
cnf(956,plain,
( ~ function(the_L_meet(u))
| ~ meet_semilatt_str(u)
| ~ quasi_total(the_L_meet(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ relation_of2(the_L_meet(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(apply_binary(the_L_meet(u),w,v),meet(u,w,v)) ),
inference(obv,[status(thm),theory(equality)],[954]),
[iquote('0:Obv:954.8')] ).
cnf(957,plain,
( ~ meet_semilatt_str(u)
| ~ quasi_total(the_L_meet(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ relation_of2(the_L_meet(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(apply_binary(the_L_meet(u),w,v),meet(u,w,v)) ),
inference(ssi,[status(thm)],[956,39,449]),
[iquote('0:SSi:956.0,39.1,449.1')] ).
cnf(958,plain,
( ~ meet_semilatt_str(u)
| ~ relation_of2(the_L_meet(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(apply_binary(the_L_meet(u),w,v),meet(u,w,v)) ),
inference(mrr,[status(thm)],[957,70]),
[iquote('0:MRR:957.1,70.1')] ).
cnf(959,plain,
( ~ meet_semilatt_str(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(apply_binary(the_L_meet(u),w,v),meet(u,w,v)) ),
inference(mrr,[status(thm)],[958,450]),
[iquote('0:MRR:958.1,450.1')] ).
cnf(960,plain,
( ~ function(the_L_join(u))
| ~ join_semilatt_str(u)
| ~ quasi_total(the_L_join(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ relation_of2(the_L_join(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(apply_binary(the_L_join(u),w,v),join(u,w,v)) ),
inference(obv,[status(thm),theory(equality)],[953]),
[iquote('0:Obv:953.8')] ).
cnf(961,plain,
( ~ join_semilatt_str(u)
| ~ quasi_total(the_L_join(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ relation_of2(the_L_join(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(apply_binary(the_L_join(u),w,v),join(u,w,v)) ),
inference(ssi,[status(thm)],[960,40,443]),
[iquote('0:SSi:960.0,40.1,443.1')] ).
cnf(962,plain,
( ~ join_semilatt_str(u)
| ~ relation_of2(the_L_join(u),cartesian_product2(the_carrier(u),the_carrier(u)),the_carrier(u))
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(apply_binary(the_L_join(u),w,v),join(u,w,v)) ),
inference(mrr,[status(thm)],[961,72]),
[iquote('0:MRR:961.1,72.1')] ).
cnf(963,plain,
( ~ join_semilatt_str(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(apply_binary(the_L_join(u),w,v),join(u,w,v)) ),
inference(mrr,[status(thm)],[962,444]),
[iquote('0:MRR:962.1,444.1')] ).
cnf(2647,plain,
( ~ strict_latt_str(u)
| ~ latt_str(u)
| ~ subset(v,w)
| ~ subset(x,w)
| ~ equal(u,boole_lattice(w))
| equal(apply_binary(the_L_join(u),v,x),set_union2(v,x)) ),
inference(res,[status(thm),theory(equality)],[55,792]),
[iquote('0:Res:55.1,792.3')] ).
cnf(5457,plain,
( ~ strict_latt_str(u)
| ~ latt_str(u)
| ~ subset(v,skc12)
| ~ equal(u,boole_lattice(skc12))
| equal(apply_binary(the_L_meet(u),skc13,v),set_intersection2(skc13,v)) ),
inference(res,[status(thm),theory(equality)],[507,818]),
[iquote('0:Res:507.0,818.3')] ).
cnf(8531,plain,
( ~ strict_latt_str(u)
| ~ latt_str(u)
| ~ meet_semilatt_str(u)
| ~ subset(v,skc12)
| ~ equal(u,boole_lattice(skc12))
| ~ element(v,the_carrier(u))
| ~ element(skc13,the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(meet(u,skc13,v),set_intersection2(skc13,v)) ),
inference(spr,[status(thm),theory(equality)],[5457,959]),
[iquote('0:SpR:5457.4,959.5')] ).
cnf(8539,plain,
( ~ strict_latt_str(u)
| ~ latt_str(u)
| ~ subset(v,skc12)
| ~ equal(u,boole_lattice(skc12))
| ~ element(v,the_carrier(u))
| ~ element(skc13,the_carrier(u))
| empty(the_carrier(u))
| empty_carrier(u)
| equal(meet(u,skc13,v),set_intersection2(skc13,v)) ),
inference(ssi,[status(thm)],[8531,28]),
[iquote('0:SSi:8531.2,28.1')] ).
cnf(10155,plain,
( ~ strict_latt_str(boole_lattice(u))
| ~ latt_str(boole_lattice(u))
| ~ subset(v,u)
| ~ subset(w,u)
| equal(apply_binary(the_L_join(boole_lattice(u)),v,w),set_union2(v,w)) ),
inference(eqr,[status(thm),theory(equality)],[2647]),
[iquote('0:EqR:2647.4')] ).
cnf(10156,plain,
( ~ subset(u,v)
| ~ subset(w,v)
| equal(apply_binary(the_L_join(boole_lattice(v)),u,w),set_union2(u,w)) ),
inference(ssi,[status(thm)],[10155,14,13]),
[iquote('0:SSi:10155.1,10155.0,14.0,13.0,14.0,13.0')] ).
cnf(35306,plain,
( ~ join_semilatt_str(boole_lattice(u))
| ~ subset(v,u)
| ~ subset(w,u)
| ~ element(w,the_carrier(boole_lattice(u)))
| ~ element(v,the_carrier(boole_lattice(u)))
| empty(the_carrier(boole_lattice(u)))
| empty_carrier(boole_lattice(u))
| equal(join(boole_lattice(u),v,w),set_union2(v,w)) ),
inference(spr,[status(thm),theory(equality)],[10156,963]),
[iquote('0:SpR:10156.2,963.5')] ).
cnf(35393,plain,
( ~ join_semilatt_str(boole_lattice(u))
| ~ subset(v,u)
| ~ subset(w,u)
| ~ element(w,powerset(u))
| ~ element(v,powerset(u))
| empty(powerset(u))
| empty_carrier(boole_lattice(u))
| equal(join(boole_lattice(u),v,w),set_union2(v,w)) ),
inference(rew,[status(thm),theory(equality)],[504,35306]),
[iquote('0:Rew:504.0,35306.5,504.0,35306.4,504.0,35306.3')] ).
cnf(35394,plain,
( ~ subset(u,v)
| ~ subset(w,v)
| ~ element(w,powerset(v))
| ~ element(u,powerset(v))
| empty(powerset(v))
| empty_carrier(boole_lattice(v))
| equal(join(boole_lattice(v),u,w),set_union2(u,w)) ),
inference(ssi,[status(thm)],[35393,29,14,13]),
[iquote('0:SSi:35393.0,29.0,14.0,13.1')] ).
cnf(35395,plain,
( ~ element(u,powerset(v))
| ~ element(w,powerset(v))
| equal(join(boole_lattice(v),w,u),set_union2(w,u)) ),
inference(mrr,[status(thm)],[35394,54,334,21]),
[iquote('0:MRR:35394.0,35394.1,35394.4,35394.5,54.1,54.1,334.0,21.0')] ).
cnf(82172,plain,
( ~ strict_latt_str(boole_lattice(skc12))
| ~ latt_str(boole_lattice(skc12))
| ~ subset(skc14,skc12)
| ~ equal(boole_lattice(skc12),boole_lattice(skc12))
| ~ element(skc14,the_carrier(boole_lattice(skc12)))
| ~ element(skc13,the_carrier(boole_lattice(skc12)))
| ~ equal(set_intersection2(skc13,skc14),set_intersection2(skc13,skc14))
| ~ equal(join(boole_lattice(skc12),skc13,skc14),set_union2(skc13,skc14))
| empty(the_carrier(boole_lattice(skc12)))
| empty_carrier(boole_lattice(skc12)) ),
inference(spl,[status(thm),theory(equality)],[8539,83]),
[iquote('0:SpL:8539.8,83.0')] ).
cnf(82173,plain,
( ~ strict_latt_str(boole_lattice(skc12))
| ~ latt_str(boole_lattice(skc12))
| ~ subset(skc14,skc12)
| ~ element(skc14,the_carrier(boole_lattice(skc12)))
| ~ element(skc13,the_carrier(boole_lattice(skc12)))
| ~ equal(join(boole_lattice(skc12),skc13,skc14),set_union2(skc13,skc14))
| empty(the_carrier(boole_lattice(skc12)))
| empty_carrier(boole_lattice(skc12)) ),
inference(obv,[status(thm),theory(equality)],[82172]),
[iquote('0:Obv:82172.6')] ).
cnf(82174,plain,
( ~ strict_latt_str(boole_lattice(skc12))
| ~ latt_str(boole_lattice(skc12))
| ~ subset(skc14,skc12)
| ~ element(skc14,powerset(skc12))
| ~ element(skc13,powerset(skc12))
| ~ equal(join(boole_lattice(skc12),skc13,skc14),set_union2(skc13,skc14))
| empty(powerset(skc12))
| empty_carrier(boole_lattice(skc12)) ),
inference(rew,[status(thm),theory(equality)],[504,82173]),
[iquote('0:Rew:504.0,82173.6,504.0,82173.4,504.0,82173.3')] ).
cnf(82175,plain,
( ~ strict_latt_str(boole_lattice(skc12))
| ~ latt_str(boole_lattice(skc12))
| ~ subset(skc14,skc12)
| ~ element(skc14,powerset(skc12))
| ~ element(skc13,powerset(skc12))
| ~ equal(set_union2(skc13,skc14),set_union2(skc13,skc14))
| empty(powerset(skc12))
| empty_carrier(boole_lattice(skc12)) ),
inference(rew,[status(thm),theory(equality)],[35395,82174]),
[iquote('0:Rew:35395.2,82174.5')] ).
cnf(82176,plain,
( ~ strict_latt_str(boole_lattice(skc12))
| ~ latt_str(boole_lattice(skc12))
| ~ subset(skc14,skc12)
| ~ element(skc14,powerset(skc12))
| ~ element(skc13,powerset(skc12))
| empty(powerset(skc12))
| empty_carrier(boole_lattice(skc12)) ),
inference(obv,[status(thm),theory(equality)],[82175]),
[iquote('0:Obv:82175.5')] ).
cnf(82177,plain,
( ~ subset(skc14,skc12)
| ~ element(skc14,powerset(skc12))
| ~ element(skc13,powerset(skc12))
| empty(powerset(skc12))
| empty_carrier(boole_lattice(skc12)) ),
inference(ssi,[status(thm)],[82176,14,13]),
[iquote('0:SSi:82176.1,82176.0,14.0,13.0,14.0,13.0')] ).
cnf(82178,plain,
$false,
inference(mrr,[status(thm)],[82177,556,506,507,334,21]),
[iquote('0:MRR:82177.0,82177.1,82177.2,82177.3,82177.4,556.0,506.0,507.0,334.0,21.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU343+1 : TPTP v8.1.0. Released v3.3.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Mon Jun 20 04:56:30 EDT 2022
% 0.12/0.33 % CPUTime :
% 148.87/149.11
% 148.87/149.11 SPASS V 3.9
% 148.87/149.11 SPASS beiseite: Proof found.
% 148.87/149.11 % SZS status Theorem
% 148.87/149.11 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 148.87/149.11 SPASS derived 62512 clauses, backtracked 5333 clauses, performed 58 splits and kept 27717 clauses.
% 148.87/149.11 SPASS allocated 196917 KBytes.
% 148.87/149.11 SPASS spent 0:2:28.68 on the problem.
% 148.87/149.11 0:00:00.04 for the input.
% 148.87/149.11 0:00:00.05 for the FLOTTER CNF translation.
% 148.87/149.11 0:00:01.87 for inferences.
% 148.87/149.11 0:00:01.74 for the backtracking.
% 148.87/149.11 0:2:23.18 for the reduction.
% 148.87/149.11
% 148.87/149.11
% 148.87/149.11 Here is a proof with depth 4, length 79 :
% 148.87/149.11 % SZS output start Refutation
% See solution above
% 165.31/165.57 Formulae used in the proof : dt_k1_lattice3 fc1_lattice3 rc2_subset_1 fc1_subset_1 t1_lattice3 dt_l3_lattices dt_u1_lattices dt_u2_lattices t6_boole t7_boole t3_subset cc1_relset_1 redefinition_m2_relset_1 t2_subset dt_m2_relset_1 d1_lattice3 existence_m1_subset_1 redefinition_k4_subset_1 redefinition_k5_subset_1 d2_lattices d1_lattices redefinition_k2_binop_1
% 165.31/165.57
%------------------------------------------------------------------------------