%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : REL010+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n004.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 : Mon Jul 18 20:01:36 EDT 2022
% Result : Theorem 1.74s 1.93s
% Output : Refutation 1.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 15
% Syntax : Number of clauses : 117 ( 117 unt; 0 nHn; 117 RR)
% Number of literals : 117 ( 0 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(composition(u,one),u),
file('REL010+2.p',unknown),
[] ).
cnf(2,axiom,
equal(converse(converse(u)),u),
file('REL010+2.p',unknown),
[] ).
cnf(3,axiom,
equal(join(u,complement(u)),top),
file('REL010+2.p',unknown),
[] ).
cnf(4,axiom,
equal(meet(u,complement(u)),zero),
file('REL010+2.p',unknown),
[] ).
cnf(5,axiom,
equal(meet(composition(skc3,skc4),skc5),zero),
file('REL010+2.p',unknown),
[] ).
cnf(6,axiom,
equal(join(u,v),join(v,u)),
file('REL010+2.p',unknown),
[] ).
cnf(7,axiom,
~ equal(meet(skc4,composition(converse(skc3),skc5)),zero),
file('REL010+2.p',unknown),
[] ).
cnf(8,axiom,
equal(complement(join(complement(u),complement(v))),meet(u,v)),
file('REL010+2.p',unknown),
[] ).
cnf(9,axiom,
equal(join(converse(u),converse(v)),converse(join(u,v))),
file('REL010+2.p',unknown),
[] ).
cnf(10,axiom,
equal(composition(converse(u),converse(v)),converse(composition(v,u))),
file('REL010+2.p',unknown),
[] ).
cnf(11,axiom,
equal(join(join(u,v),w),join(u,join(v,w))),
file('REL010+2.p',unknown),
[] ).
cnf(13,axiom,
equal(join(composition(u,v),composition(w,v)),composition(join(u,w),v)),
file('REL010+2.p',unknown),
[] ).
cnf(14,axiom,
equal(join(composition(converse(u),complement(composition(u,v))),complement(v)),complement(v)),
file('REL010+2.p',unknown),
[] ).
cnf(15,axiom,
equal(join(complement(join(complement(u),complement(v))),complement(join(complement(u),v))),u),
file('REL010+2.p',unknown),
[] ).
cnf(17,axiom,
equal(join(meet(composition(u,v),w),meet(composition(u,meet(v,composition(converse(u),w))),w)),meet(composition(u,meet(v,composition(converse(u),w))),w)),
file('REL010+2.p',unknown),
[] ).
cnf(19,plain,
equal(join(complement(u),composition(converse(v),complement(composition(v,u)))),complement(u)),
inference(rew,[status(thm),theory(equality)],[6,14]),
[iquote('0:Rew:6.0,14.0')] ).
cnf(20,plain,
equal(join(meet(u,v),complement(join(complement(u),v))),u),
inference(rew,[status(thm),theory(equality)],[8,15]),
[iquote('0:Rew:8.0,15.0')] ).
cnf(32,plain,
equal(converse(composition(converse(u),v)),composition(converse(v),u)),
inference(spr,[status(thm),theory(equality)],[2,10]),
[iquote('0:SpR:2.0,10.0')] ).
cnf(38,plain,
equal(converse(join(converse(u),v)),join(u,converse(v))),
inference(spr,[status(thm),theory(equality)],[2,9]),
[iquote('0:SpR:2.0,9.0')] ).
cnf(46,plain,
equal(meet(u,complement(u)),complement(top)),
inference(spr,[status(thm),theory(equality)],[3,8]),
[iquote('0:SpR:3.0,8.0')] ).
cnf(47,plain,
equal(complement(join(complement(u),complement(v))),meet(v,u)),
inference(spr,[status(thm),theory(equality)],[6,8]),
[iquote('0:SpR:6.0,8.0')] ).
cnf(49,plain,
equal(complement(top),zero),
inference(rew,[status(thm),theory(equality)],[4,46]),
[iquote('0:Rew:4.0,46.0')] ).
cnf(50,plain,
equal(meet(u,v),meet(v,u)),
inference(rew,[status(thm),theory(equality)],[8,47]),
[iquote('0:Rew:8.0,47.0')] ).
cnf(51,plain,
equal(meet(skc5,composition(skc3,skc4)),zero),
inference(rew,[status(thm),theory(equality)],[50,5]),
[iquote('0:Rew:50.0,5.0')] ).
cnf(52,plain,
equal(join(meet(composition(u,v),w),meet(w,composition(u,meet(v,composition(converse(u),w))))),meet(w,composition(u,meet(v,composition(converse(u),w))))),
inference(rew,[status(thm),theory(equality)],[50,17]),
[iquote('0:Rew:50.0,17.0')] ).
cnf(59,plain,
equal(meet(top,zero),zero),
inference(spr,[status(thm),theory(equality)],[49,4]),
[iquote('0:SpR:49.0,4.0')] ).
cnf(61,plain,
equal(complement(join(zero,complement(u))),meet(top,u)),
inference(spr,[status(thm),theory(equality)],[49,8]),
[iquote('0:SpR:49.0,8.0')] ).
cnf(64,plain,
equal(meet(zero,top),zero),
inference(rew,[status(thm),theory(equality)],[50,59]),
[iquote('0:Rew:50.0,59.0')] ).
cnf(73,plain,
equal(join(meet(top,u),complement(join(zero,u))),top),
inference(spr,[status(thm),theory(equality)],[49,20]),
[iquote('0:SpR:49.0,20.0')] ).
cnf(74,plain,
equal(join(meet(u,complement(complement(u))),complement(top)),u),
inference(spr,[status(thm),theory(equality)],[3,20]),
[iquote('0:SpR:3.0,20.0')] ).
cnf(77,plain,
equal(join(meet(u,complement(v)),meet(u,v)),u),
inference(spr,[status(thm),theory(equality)],[8,20]),
[iquote('0:SpR:8.0,20.0')] ).
cnf(78,plain,
equal(join(zero,complement(join(complement(u),complement(u)))),u),
inference(spr,[status(thm),theory(equality)],[4,20]),
[iquote('0:SpR:4.0,20.0')] ).
cnf(80,plain,
equal(join(zero,complement(join(complement(zero),top))),zero),
inference(spr,[status(thm),theory(equality)],[64,20]),
[iquote('0:SpR:64.0,20.0')] ).
cnf(81,plain,
equal(join(zero,complement(join(top,complement(zero)))),zero),
inference(rew,[status(thm),theory(equality)],[6,80]),
[iquote('0:Rew:6.0,80.0')] ).
cnf(82,plain,
equal(join(zero,meet(u,complement(complement(u)))),u),
inference(rew,[status(thm),theory(equality)],[6,74,49]),
[iquote('0:Rew:6.0,74.0,49.0,74.0')] ).
cnf(83,plain,
equal(join(meet(u,v),meet(u,complement(v))),u),
inference(rew,[status(thm),theory(equality)],[6,77]),
[iquote('0:Rew:6.0,77.0')] ).
cnf(84,plain,
equal(join(zero,meet(u,u)),u),
inference(rew,[status(thm),theory(equality)],[8,78]),
[iquote('0:Rew:8.0,78.0')] ).
cnf(97,plain,
equal(meet(join(zero,complement(u)),meet(top,u)),zero),
inference(spr,[status(thm),theory(equality)],[61,4]),
[iquote('0:SpR:61.0,4.0')] ).
cnf(105,plain,
equal(complement(join(zero,zero)),meet(top,top)),
inference(spr,[status(thm),theory(equality)],[49,61]),
[iquote('0:SpR:49.0,61.0')] ).
cnf(109,plain,
equal(meet(meet(top,u),join(zero,complement(u))),zero),
inference(rew,[status(thm),theory(equality)],[50,97]),
[iquote('0:Rew:50.0,97.0')] ).
cnf(121,plain,
equal(meet(join(zero,zero),meet(top,top)),zero),
inference(spr,[status(thm),theory(equality)],[105,4]),
[iquote('0:SpR:105.0,4.0')] ).
cnf(130,plain,
equal(meet(meet(top,top),join(zero,zero)),zero),
inference(rew,[status(thm),theory(equality)],[50,121]),
[iquote('0:Rew:50.0,121.0')] ).
cnf(145,plain,
equal(join(zero,complement(join(complement(meet(top,top)),join(zero,zero)))),meet(top,top)),
inference(spr,[status(thm),theory(equality)],[130,20]),
[iquote('0:SpR:130.0,20.0')] ).
cnf(151,plain,
equal(join(zero,complement(join(join(zero,zero),complement(meet(top,top))))),meet(top,top)),
inference(rew,[status(thm),theory(equality)],[6,145]),
[iquote('0:Rew:6.0,145.0')] ).
cnf(152,plain,
equal(join(zero,complement(join(zero,join(zero,complement(meet(top,top)))))),meet(top,top)),
inference(rew,[status(thm),theory(equality)],[11,151]),
[iquote('0:Rew:11.0,151.0')] ).
cnf(153,plain,
equal(join(u,join(v,complement(join(u,v)))),top),
inference(spr,[status(thm),theory(equality)],[11,3]),
[iquote('0:SpR:11.0,3.0')] ).
cnf(158,plain,
equal(join(u,join(complement(u),v)),join(top,v)),
inference(spr,[status(thm),theory(equality)],[3,11]),
[iquote('0:SpR:3.0,11.0')] ).
cnf(159,plain,
equal(join(join(u,v),w),join(v,join(u,w))),
inference(spr,[status(thm),theory(equality)],[6,11]),
[iquote('0:SpR:6.0,11.0')] ).
cnf(165,plain,
equal(join(zero,join(complement(join(top,complement(zero))),u)),join(zero,u)),
inference(spr,[status(thm),theory(equality)],[81,11]),
[iquote('0:SpR:81.0,11.0')] ).
cnf(174,plain,
equal(join(u,join(v,w)),join(v,join(u,w))),
inference(rew,[status(thm),theory(equality)],[11,159]),
[iquote('0:Rew:11.0,159.0')] ).
cnf(214,plain,
equal(join(zero,composition(converse(u),complement(composition(u,top)))),zero),
inference(spr,[status(thm),theory(equality)],[49,19]),
[iquote('0:SpR:49.0,19.0')] ).
cnf(343,plain,
equal(join(meet(composition(converse(u),v),w),meet(w,composition(converse(u),meet(v,composition(u,w))))),meet(w,composition(converse(u),meet(v,composition(u,w))))),
inference(spr,[status(thm),theory(equality)],[2,52]),
[iquote('0:SpR:2.0,52.0')] ).
cnf(373,plain,
equal(meet(meet(u,top),join(zero,complement(u))),zero),
inference(spr,[status(thm),theory(equality)],[50,109]),
[iquote('0:SpR:50.0,109.0')] ).
cnf(514,plain,
equal(join(zero,complement(join(complement(meet(u,top)),join(zero,complement(u))))),meet(u,top)),
inference(spr,[status(thm),theory(equality)],[373,20]),
[iquote('0:SpR:373.0,20.0')] ).
cnf(537,plain,
equal(join(zero,complement(join(zero,join(complement(meet(u,top)),complement(u))))),meet(u,top)),
inference(rew,[status(thm),theory(equality)],[174,514]),
[iquote('0:Rew:174.0,514.0')] ).
cnf(538,plain,
equal(join(zero,complement(join(zero,join(complement(u),complement(meet(u,top)))))),meet(u,top)),
inference(rew,[status(thm),theory(equality)],[6,537]),
[iquote('0:Rew:6.0,537.0')] ).
cnf(640,plain,
equal(composition(converse(one),u),converse(converse(u))),
inference(spr,[status(thm),theory(equality)],[1,32]),
[iquote('0:SpR:1.0,32.0')] ).
cnf(643,plain,
equal(composition(converse(one),u),u),
inference(rew,[status(thm),theory(equality)],[2,640]),
[iquote('0:Rew:2.0,640.0')] ).
cnf(654,plain,
equal(converse(one),one),
inference(spr,[status(thm),theory(equality)],[643,1]),
[iquote('0:SpR:643.0,1.0')] ).
cnf(665,plain,
equal(join(complement(u),complement(composition(one,u))),complement(u)),
inference(spr,[status(thm),theory(equality)],[643,19]),
[iquote('0:SpR:643.0,19.0')] ).
cnf(672,plain,
equal(composition(one,u),u),
inference(rew,[status(thm),theory(equality)],[654,643]),
[iquote('0:Rew:654.0,643.0')] ).
cnf(687,plain,
equal(join(complement(u),complement(u)),complement(u)),
inference(rew,[status(thm),theory(equality)],[672,665]),
[iquote('0:Rew:672.0,665.0')] ).
cnf(760,plain,
equal(meet(u,u),complement(complement(u))),
inference(spr,[status(thm),theory(equality)],[687,8]),
[iquote('0:SpR:687.0,8.0')] ).
cnf(766,plain,
equal(join(zero,zero),zero),
inference(spr,[status(thm),theory(equality)],[49,687]),
[iquote('0:SpR:49.0,687.0')] ).
cnf(771,plain,
equal(meet(top,top),complement(zero)),
inference(rew,[status(thm),theory(equality)],[766,105]),
[iquote('0:Rew:766.0,105.0')] ).
cnf(785,plain,
equal(join(zero,complement(join(zero,join(zero,complement(complement(zero)))))),complement(zero)),
inference(rew,[status(thm),theory(equality)],[771,152]),
[iquote('0:Rew:771.0,152.0')] ).
cnf(787,plain,
equal(join(zero,complement(complement(u))),u),
inference(rew,[status(thm),theory(equality)],[760,84]),
[iquote('0:Rew:760.0,84.0')] ).
cnf(814,plain,
equal(join(zero,complement(zero)),complement(zero)),
inference(rew,[status(thm),theory(equality)],[766,785,787]),
[iquote('0:Rew:766.0,785.0,787.0,785.0')] ).
cnf(815,plain,
equal(complement(zero),top),
inference(rew,[status(thm),theory(equality)],[3,814]),
[iquote('0:Rew:3.0,814.0')] ).
cnf(823,plain,
equal(join(zero,join(complement(join(top,top)),u)),join(zero,u)),
inference(rew,[status(thm),theory(equality)],[815,165]),
[iquote('0:Rew:815.0,165.0')] ).
cnf(844,plain,
equal(meet(top,complement(u)),complement(u)),
inference(spr,[status(thm),theory(equality)],[787,61]),
[iquote('0:SpR:787.0,61.0')] ).
cnf(848,plain,
equal(join(zero,complement(meet(u,v))),join(complement(u),complement(v))),
inference(spr,[status(thm),theory(equality)],[8,787]),
[iquote('0:SpR:8.0,787.0')] ).
cnf(868,plain,
equal(complement(join(top,complement(u))),meet(zero,u)),
inference(spr,[status(thm),theory(equality)],[815,8]),
[iquote('0:SpR:815.0,8.0')] ).
cnf(869,plain,
equal(join(meet(zero,u),complement(join(top,u))),zero),
inference(spr,[status(thm),theory(equality)],[815,20]),
[iquote('0:SpR:815.0,20.0')] ).
cnf(878,plain,
equal(join(top,top),top),
inference(spr,[status(thm),theory(equality)],[815,687]),
[iquote('0:SpR:815.0,687.0')] ).
cnf(887,plain,
equal(join(zero,join(complement(top),u)),join(zero,u)),
inference(rew,[status(thm),theory(equality)],[878,823]),
[iquote('0:Rew:878.0,823.0')] ).
cnf(911,plain,
equal(join(zero,join(zero,u)),join(zero,u)),
inference(rew,[status(thm),theory(equality)],[49,887]),
[iquote('0:Rew:49.0,887.0')] ).
cnf(943,plain,
equal(join(complement(u),complement(join(zero,complement(u)))),top),
inference(spr,[status(thm),theory(equality)],[844,73]),
[iquote('0:SpR:844.0,73.0')] ).
cnf(956,plain,
equal(join(complement(u),meet(top,u)),top),
inference(rew,[status(thm),theory(equality)],[61,943]),
[iquote('0:Rew:61.0,943.0')] ).
cnf(1039,plain,
equal(join(complement(u),meet(u,top)),top),
inference(spr,[status(thm),theory(equality)],[50,956]),
[iquote('0:SpR:50.0,956.0')] ).
cnf(1060,plain,
equal(join(meet(u,meet(u,top)),complement(top)),u),
inference(spr,[status(thm),theory(equality)],[1039,20]),
[iquote('0:SpR:1039.0,20.0')] ).
cnf(1074,plain,
equal(join(zero,meet(u,meet(u,top))),u),
inference(rew,[status(thm),theory(equality)],[6,1060,49]),
[iquote('0:Rew:6.0,1060.0,49.0,1060.0')] ).
cnf(1162,plain,
equal(meet(top,join(top,complement(u))),complement(join(zero,meet(zero,u)))),
inference(spr,[status(thm),theory(equality)],[868,61]),
[iquote('0:SpR:868.0,61.0')] ).
cnf(1176,plain,
equal(meet(zero,join(zero,complement(u))),complement(join(top,meet(top,u)))),
inference(spr,[status(thm),theory(equality)],[61,868]),
[iquote('0:SpR:61.0,868.0')] ).
cnf(1207,plain,
equal(join(zero,u),u),
inference(spr,[status(thm),theory(equality)],[82,911]),
[iquote('0:SpR:82.0,911.0')] ).
cnf(1212,plain,
equal(complement(complement(u)),u),
inference(rew,[status(thm),theory(equality)],[1207,787]),
[iquote('0:Rew:1207.0,787.0')] ).
cnf(1213,plain,
equal(meet(top,u),complement(complement(u))),
inference(rew,[status(thm),theory(equality)],[1207,61]),
[iquote('0:Rew:1207.0,61.0')] ).
cnf(1220,plain,
equal(join(zero,complement(join(complement(u),complement(meet(u,top))))),meet(u,top)),
inference(rew,[status(thm),theory(equality)],[1207,538]),
[iquote('0:Rew:1207.0,538.0')] ).
cnf(1222,plain,
equal(composition(converse(u),complement(composition(u,top))),zero),
inference(rew,[status(thm),theory(equality)],[1207,214]),
[iquote('0:Rew:1207.0,214.0')] ).
cnf(1224,plain,
equal(join(complement(u),complement(v)),complement(meet(u,v))),
inference(rew,[status(thm),theory(equality)],[1207,848]),
[iquote('0:Rew:1207.0,848.0')] ).
cnf(1231,plain,
equal(complement(join(top,meet(top,u))),meet(zero,complement(u))),
inference(rew,[status(thm),theory(equality)],[1207,1176]),
[iquote('0:Rew:1207.0,1176.0')] ).
cnf(1235,plain,
equal(meet(u,meet(u,top)),u),
inference(rew,[status(thm),theory(equality)],[1207,1074]),
[iquote('0:Rew:1207.0,1074.0')] ).
cnf(1238,plain,
equal(meet(top,join(top,complement(u))),complement(meet(zero,u))),
inference(rew,[status(thm),theory(equality)],[1207,1162]),
[iquote('0:Rew:1207.0,1162.0')] ).
cnf(1251,plain,
equal(meet(top,u),u),
inference(rew,[status(thm),theory(equality)],[1212,1213]),
[iquote('0:Rew:1212.0,1213.0')] ).
cnf(1281,plain,
equal(meet(zero,complement(u)),complement(join(top,u))),
inference(rew,[status(thm),theory(equality)],[1251,1231]),
[iquote('0:Rew:1251.0,1231.0')] ).
cnf(1282,plain,
equal(join(top,complement(u)),complement(meet(zero,u))),
inference(rew,[status(thm),theory(equality)],[1251,1238]),
[iquote('0:Rew:1251.0,1238.0')] ).
cnf(1308,plain,
equal(meet(u,top),u),
inference(rew,[status(thm),theory(equality)],[1207,1220,1212,1235,1224]),
[iquote('0:Rew:1207.0,1220.0,1212.0,1220.0,1235.0,1220.0,1224.0,1220.0')] ).
cnf(1612,plain,
equal(join(u,complement(meet(zero,join(u,top)))),top),
inference(spr,[status(thm),theory(equality)],[1282,153]),
[iquote('0:SpR:1282.0,153.0')] ).
cnf(1911,plain,
equal(join(u,meet(u,complement(top))),u),
inference(spr,[status(thm),theory(equality)],[1308,83]),
[iquote('0:SpR:1308.0,83.0')] ).
cnf(1920,plain,
equal(join(u,meet(u,zero)),u),
inference(rew,[status(thm),theory(equality)],[49,1911]),
[iquote('0:Rew:49.0,1911.0')] ).
cnf(1939,plain,
equal(join(u,complement(u)),join(top,meet(complement(u),zero))),
inference(spr,[status(thm),theory(equality)],[1920,158]),
[iquote('0:SpR:1920.0,158.0')] ).
cnf(1949,plain,
equal(complement(meet(zero,join(top,u))),top),
inference(rew,[status(thm),theory(equality)],[3,1939,1282,1281,50]),
[iquote('0:Rew:3.0,1939.0,1282.0,1939.0,1281.0,1939.0,50.0,1939.0')] ).
cnf(2042,plain,
equal(complement(meet(zero,join(u,top))),top),
inference(spr,[status(thm),theory(equality)],[6,1949]),
[iquote('0:SpR:6.0,1949.0')] ).
cnf(2065,plain,
equal(join(u,top),top),
inference(rew,[status(thm),theory(equality)],[2042,1612]),
[iquote('0:Rew:2042.0,1612.0')] ).
cnf(2088,plain,
equal(join(top,u),top),
inference(spr,[status(thm),theory(equality)],[2065,6]),
[iquote('0:SpR:2065.0,6.0')] ).
cnf(2095,plain,
equal(join(u,converse(top)),converse(top)),
inference(spr,[status(thm),theory(equality)],[2065,38]),
[iquote('0:SpR:2065.0,38.0')] ).
cnf(2111,plain,
equal(join(meet(zero,u),complement(top)),zero),
inference(rew,[status(thm),theory(equality)],[2088,869]),
[iquote('0:Rew:2088.0,869.0')] ).
cnf(2125,plain,
equal(meet(zero,u),zero),
inference(rew,[status(thm),theory(equality)],[1207,2111,6,49]),
[iquote('0:Rew:1207.0,2111.0,6.0,2111.0,49.0,2111.0')] ).
cnf(2280,plain,
equal(converse(top),top),
inference(spr,[status(thm),theory(equality)],[2095,2088]),
[iquote('0:SpR:2095.0,2088.0')] ).
cnf(2310,plain,
equal(composition(top,complement(composition(top,top))),zero),
inference(spr,[status(thm),theory(equality)],[2280,1222]),
[iquote('0:SpR:2280.0,1222.0')] ).
cnf(2345,plain,
equal(join(zero,composition(u,complement(composition(top,top)))),composition(join(top,u),complement(composition(top,top)))),
inference(spr,[status(thm),theory(equality)],[2310,13]),
[iquote('0:SpR:2310.0,13.0')] ).
cnf(2352,plain,
equal(composition(u,complement(composition(top,top))),zero),
inference(rew,[status(thm),theory(equality)],[1207,2345,2310,2088]),
[iquote('0:Rew:1207.0,2345.0,2310.0,2345.0,2088.0,2345.0')] ).
cnf(2475,plain,
equal(complement(composition(top,top)),zero),
inference(spr,[status(thm),theory(equality)],[2352,672]),
[iquote('0:SpR:2352.0,672.0')] ).
cnf(2477,plain,
equal(composition(u,zero),zero),
inference(rew,[status(thm),theory(equality)],[2475,2352]),
[iquote('0:Rew:2475.0,2352.0')] ).
cnf(10692,plain,
equal(join(meet(composition(converse(skc3),skc5),skc4),meet(skc4,composition(converse(skc3),zero))),meet(skc4,composition(converse(skc3),zero))),
inference(spr,[status(thm),theory(equality)],[51,343]),
[iquote('0:SpR:51.0,343.0')] ).
cnf(10750,plain,
equal(meet(skc4,composition(converse(skc3),skc5)),zero),
inference(rew,[status(thm),theory(equality)],[1207,10692,6,50,2125,2477]),
[iquote('0:Rew:1207.0,10692.0,6.0,10692.0,50.0,10692.0,2125.0,10692.0,50.0,10692.0,2477.0,10692.0')] ).
cnf(10751,plain,
$false,
inference(mrr,[status(thm)],[10750,7]),
[iquote('0:MRR:10750.0,7.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : REL010+2 : TPTP v8.1.0. Released v4.0.0.
% 0.00/0.07 % Command : run_spass %d %s
% 0.06/0.26 % Computer : n004.cluster.edu
% 0.06/0.26 % Model : x86_64 x86_64
% 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.26 % Memory : 8042.1875MB
% 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.26 % CPULimit : 300
% 0.06/0.26 % WCLimit : 600
% 0.06/0.26 % DateTime : Fri Jul 8 14:19:52 EDT 2022
% 0.06/0.26 % CPUTime :
% 1.74/1.93
% 1.74/1.93 SPASS V 3.9
% 1.74/1.93 SPASS beiseite: Proof found.
% 1.74/1.93 % SZS status Theorem
% 1.74/1.93 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.74/1.93 SPASS derived 6642 clauses, backtracked 0 clauses, performed 0 splits and kept 1584 clauses.
% 1.74/1.93 SPASS allocated 97886 KBytes.
% 1.74/1.93 SPASS spent 0:00:01.66 on the problem.
% 1.74/1.93 0:00:00.02 for the input.
% 1.74/1.93 0:00:00.02 for the FLOTTER CNF translation.
% 1.74/1.93 0:00:00.06 for inferences.
% 1.74/1.93 0:00:00.00 for the backtracking.
% 1.74/1.93 0:00:01.55 for the reduction.
% 1.74/1.93
% 1.74/1.93
% 1.74/1.93 Here is a proof with depth 13, length 117 :
% 1.74/1.93 % SZS output start Refutation
% See solution above
% 1.81/1.99 Formulae used in the proof : composition_identity converse_idempotence def_top def_zero goals maddux1_join_commutativity maddux4_definiton_of_meet converse_additivity converse_multiplicativity maddux2_join_associativity composition_distributivity converse_cancellativity maddux3_a_kind_of_de_Morgan modular_law_1
% 1.81/1.99
%------------------------------------------------------------------------------