%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL028+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:35:17 PM UTC 2026
% Result : Theorem 111.30s 31.64s
% Output : Proof 111.30s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet) ).
fof(f3_nnf,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t7,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t88,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t7]) ).
fof(f0,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity) ).
fof(f0_nnf,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t6,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t44,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t90,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t88,t44]) ).
cnf(t205990,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t90,t88]) ).
cnf(t109,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t205990]) ).
fof(f11,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top) ).
fof(f11_nnf,plain,
! [X0] : top = join(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X0] : top = join(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
top = join(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t4,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t52,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t89,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t88,t52]) ).
fof(f12,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero) ).
fof(f12_nnf,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t5,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t95,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t205988,plain,
zero = complement(top),
inference(step,[status(thm)],[t89,t95]) ).
cnf(t100,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t205988]) ).
cnf(t103,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t88,t100]) ).
cnf(t131,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t103]) ).
fof(f10,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity) ).
fof(f10_nnf,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t13,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t205987,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t13,t44]) ).
cnf(t55,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t205987]) ).
fof(f9,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity) ).
fof(f9_nnf,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t8,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t28,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t8]) ).
fof(f7,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence) ).
fof(f7_nnf,plain,
! [X0] : converse(converse(X0)) = X0,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X0] : converse(converse(X0)) = X0,
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
converse(converse(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t1,plain,
converse(converse(X1)) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t22,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t30,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t28,t22]) ).
cnf(t192,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t30]) ).
fof(f6,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity) ).
fof(f6_nnf,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t12,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t25,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
fof(f1,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity) ).
fof(f1_nnf,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t11,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t47,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
fof(f13,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dedekind_law) ).
fof(f13_nnf,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t17,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t34,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t17]) ).
fof(f5,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity) ).
fof(f5_nnf,plain,
! [X0] : composition(X0,one) = X0,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X0] : composition(X0,one) = X0,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
composition(X0,one) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t0,plain,
composition(X1,one) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t18,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t35,plain,
composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t34,t18]) ).
cnf(t193,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t192,t18]) ).
cnf(t205996,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t193,t22]) ).
cnf(t205,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t205996]) ).
cnf(t206,plain,
one = converse(one),
inference(cp,[status(thm)],[t205,t18]) ).
cnf(t215,plain,
converse(one) = one,
inference(orient,[status(thm)],[t206]) ).
cnf(t206248,plain,
composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t35,t215]) ).
cnf(t206249,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t206248,t18]) ).
cnf(t206250,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t206249,t215]) ).
cnf(t206251,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t206250,t18]) ).
cnf(t3225,plain,
join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))) = composition(meet(X1,X2),meet(one,composition(converse(X1),X2))),
inference(orient,[status(thm)],[t206251]) ).
fof(f8,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity) ).
fof(f8_nnf,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t9,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t61,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t65,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t47,t61]) ).
cnf(t4033,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t65]) ).
cnf(t54,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t47,t52]) ).
cnf(t389,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t54]) ).
cnf(t400,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t389,t44]) ).
cnf(t205997,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t205,t215]) ).
cnf(t225,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t205997]) ).
cnf(t226,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t225]) ).
cnf(t229,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t55,t226]) ).
cnf(t206001,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t229,t215]) ).
cnf(t206002,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t206001,t226]) ).
cnf(t263,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t206002]) ).
cnf(t273,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t88,t263]) ).
cnf(t295,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t273]) ).
cnf(t303,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t52,t295]) ).
cnf(t319,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t303]) ).
cnf(t395,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t389,t319]) ).
cnf(t397,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t389,t263]) ).
cnf(t206015,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t397,t52]) ).
cnf(t412,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t206015]) ).
cnf(t413,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t412,t88]) ).
cnf(t432,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t413]) ).
cnf(t206018,plain,
top = join(X1,top),
inference(step,[status(thm)],[t395,t432]) ).
cnf(t437,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t206018]) ).
cnf(t438,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t437,t44]) ).
cnf(t443,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t438]) ).
cnf(t206041,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t400,t443]) ).
cnf(t517,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t206041]) ).
cnf(t4039,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t4033,t517]) ).
cnf(t206379,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t4039,t44]) ).
cnf(t4117,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t206379]) ).
cnf(t4164,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t4117,t61]) ).
cnf(t206380,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t4164,t22]) ).
cnf(t206381,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t206380,t22]) ).
cnf(t4178,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t206381]) ).
cnf(t4223,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t4178,t44]) ).
cnf(t4242,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t4223]) ).
cnf(t57,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t55,t18]) ).
cnf(t1856,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t57]) ).
cnf(t63,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t61,t22]) ).
cnf(t324,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t63]) ).
cnf(t326,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t324,t52]) ).
cnf(t370,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t326]) ).
cnf(t450,plain,
top = converse(top),
inference(cp,[status(thm)],[t443,t370]) ).
cnf(t453,plain,
converse(top) = top,
inference(orient,[status(thm)],[t450]) ).
cnf(t1861,plain,
complement(one) = join(complement(one),composition(top,complement(top))),
inference(cp,[status(thm)],[t1856,t453]) ).
cnf(t206137,plain,
complement(one) = join(complement(one),composition(top,zero)),
inference(step,[status(thm)],[t1861,t100]) ).
cnf(t1881,plain,
join(complement(one),composition(top,zero)) = complement(one),
inference(orient,[status(thm)],[t206137]) ).
cnf(t4255,plain,
top = join(complement(composition(top,zero)),complement(one)),
inference(cp,[status(thm)],[t4242,t1881]) ).
cnf(t206382,plain,
top = join(complement(one),complement(composition(top,zero))),
inference(step,[status(thm)],[t4255,t44]) ).
cnf(t4333,plain,
join(complement(one),complement(composition(top,zero))) = top,
inference(orient,[status(thm)],[t206382]) ).
cnf(t4335,plain,
meet(one,composition(top,zero)) = complement(top),
inference(cp,[status(thm)],[t88,t4333]) ).
cnf(t206383,plain,
meet(one,composition(top,zero)) = zero,
inference(step,[status(thm)],[t4335,t100]) ).
cnf(t4341,plain,
meet(one,composition(top,zero)) = zero,
inference(orient,[status(thm)],[t206383]) ).
cnf(t4347,plain,
composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(cp,[status(thm)],[t3225,t4341]) ).
cnf(t206384,plain,
composition(zero,meet(one,composition(converse(one),composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t4347,t4341]) ).
cnf(t206385,plain,
composition(zero,meet(one,composition(one,composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t206384,t215]) ).
cnf(t206386,plain,
composition(zero,meet(one,composition(top,zero))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t206385,t226]) ).
cnf(t206387,plain,
composition(zero,zero) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t206386,t4341]) ).
cnf(t206388,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t206387,t4341]) ).
cnf(t206389,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(one,composition(top,zero))))),
inference(step,[status(thm)],[t206388,t215]) ).
cnf(t206390,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(top,zero)))),
inference(step,[status(thm)],[t206389,t226]) ).
cnf(t206391,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t206390,t4341]) ).
cnf(t4349,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t206391]) ).
cnf(t4352,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(cp,[status(thm)],[t47,t4349]) ).
cnf(t5066,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(orient,[status(thm)],[t4352]) ).
cnf(t5074,plain,
join(composition(zero,zero),composition(X1,zero)) = join(zero,composition(join(zero,X1),zero)),
inference(cp,[status(thm)],[t5066,t25]) ).
cnf(t206414,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(zero,X1),zero)),
inference(step,[status(thm)],[t5074,t25]) ).
cnf(t5167,plain,
join(zero,composition(join(zero,X1),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t206414]) ).
cnf(t5194,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(X1,zero),zero)),
inference(cp,[status(thm)],[t5167,t44]) ).
cnf(t5311,plain,
join(zero,composition(join(X1,zero),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t5194]) ).
cnf(t458,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t28,t453]) ).
cnf(t465,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t458]) ).
cnf(t467,plain,
converse(join(composition(X1,top),X2)) = join(composition(top,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t61,t465]) ).
cnf(t7132,plain,
join(composition(top,converse(X1)),converse(X2)) = converse(join(composition(X1,top),X2)),
inference(orient,[status(thm)],[t467]) ).
cnf(t7145,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(cp,[status(thm)],[t7132,t453]) ).
cnf(t7181,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(orient,[status(thm)],[t7145]) ).
cnf(t7185,plain,
join(composition(top,top),converse(composition(X1,top))) = converse(composition(join(top,X1),top)),
inference(cp,[status(thm)],[t7181,t25]) ).
cnf(t206482,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t7185,t465]) ).
cnf(t206483,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t206482,t465]) ).
cnf(t206484,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t206483,t443]) ).
cnf(t206485,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t206484,t453]) ).
cnf(t7315,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t206485]) ).
cnf(t7331,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t7315,t215]) ).
cnf(t206486,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t7331,t18]) ).
cnf(t206487,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t206486,t437]) ).
cnf(t7344,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t206487]) ).
cnf(t7349,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t55,t7344]) ).
cnf(t206496,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t7349,t100]) ).
cnf(t206497,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t206496,t100]) ).
cnf(t206498,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t206497,t453]) ).
cnf(t206499,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t206498,t100]) ).
cnf(t267,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t263,t100]) ).
cnf(t206003,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t267,t100]) ).
cnf(t206004,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t206003,t100]) ).
cnf(t274,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t206004]) ).
cnf(t275,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t47,t274]) ).
cnf(t308,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t275]) ).
cnf(t310,plain,
join(zero,X1) = join(zero,join(X1,zero)),
inference(cp,[status(thm)],[t308,t44]) ).
cnf(t311,plain,
join(zero,join(X1,zero)) = join(zero,X1),
inference(orient,[status(thm)],[t310]) ).
cnf(t314,plain,
join(zero,join(join(X1,zero),X2)) = join(join(zero,X1),X2),
inference(cp,[status(thm)],[t47,t311]) ).
cnf(t206142,plain,
join(zero,join(X1,join(zero,X2))) = join(join(zero,X1),X2),
inference(step,[status(thm)],[t314,t47]) ).
cnf(t206143,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(step,[status(thm)],[t206142,t47]) ).
cnf(t2137,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(orient,[status(thm)],[t206143]) ).
cnf(t53,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t52,t47]) ).
cnf(t705,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t53]) ).
cnf(t747,plain,
top = join(X1,join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t705,t44]) ).
cnf(t899,plain,
join(X1,join(X2,complement(join(X2,X1)))) = top,
inference(orient,[status(thm)],[t747]) ).
cnf(t216,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t61,t215]) ).
cnf(t232,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t216]) ).
fof(f16,conjecture,
! [X0,X1] :
( ( join(X1,one) = one
& join(X0,one) = one )
=> composition(X0,X1) = meet(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0,X1] :
( ( join(X1,one) = one
& join(X0,one) = one )
=> composition(X0,X1) = meet(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0,X1] :
( composition(X0,X1) != meet(X0,X1)
& join(X1,one) = one
& join(X0,one) = one ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( composition(sk0,sk1) != meet(sk0,sk1)
& join(sk1,one) = one
& join(sk0,one) = one ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f16_nnf]) ).
cnf(c16,plain,
join(sk0,one) = one,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t2,plain,
join(sk0,one) = one,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t84,plain,
join(sk0,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t85,plain,
join(sk0,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t47,t84]) ).
cnf(t121,plain,
join(sk0,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t85]) ).
cnf(t123,plain,
join(one,X1) = join(sk0,join(X1,one)),
inference(cp,[status(thm)],[t121,t44]) ).
cnf(t150,plain,
join(sk0,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t123]) ).
cnf(t393,plain,
join(top,one) = join(one,complement(sk0)),
inference(cp,[status(thm)],[t389,t150]) ).
cnf(t427,plain,
join(one,complement(sk0)) = join(top,one),
inference(orient,[status(thm)],[t393]) ).
cnf(t428,plain,
join(one,converse(complement(sk0))) = converse(join(top,one)),
inference(cp,[status(thm)],[t232,t427]) ).
cnf(t217,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t61,t215]) ).
cnf(t205998,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t217,t44]) ).
cnf(t243,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t205998]) ).
cnf(t206034,plain,
join(one,converse(complement(sk0))) = join(one,converse(top)),
inference(step,[status(thm)],[t428,t243]) ).
cnf(t206035,plain,
join(one,converse(complement(sk0))) = join(one,top),
inference(step,[status(thm)],[t206034,t453]) ).
cnf(t206036,plain,
join(one,converse(complement(sk0))) = top,
inference(step,[status(thm)],[t206035,t437]) ).
cnf(t493,plain,
join(one,converse(complement(sk0))) = top,
inference(orient,[status(thm)],[t206036]) ).
cnf(t494,plain,
join(one,join(converse(complement(sk0)),X1)) = join(top,X1),
inference(cp,[status(thm)],[t47,t493]) ).
cnf(t206043,plain,
join(one,join(converse(complement(sk0)),X1)) = top,
inference(step,[status(thm)],[t494,t443]) ).
cnf(t542,plain,
join(one,join(converse(complement(sk0)),X1)) = top,
inference(orient,[status(thm)],[t206043]) ).
cnf(t951,plain,
top = join(join(converse(complement(sk0)),X1),join(one,complement(top))),
inference(cp,[status(thm)],[t899,t542]) ).
cnf(t206226,plain,
top = join(converse(complement(sk0)),join(X1,join(one,complement(top)))),
inference(step,[status(thm)],[t951,t47]) ).
cnf(t206227,plain,
top = join(converse(complement(sk0)),join(X1,join(one,zero))),
inference(step,[status(thm)],[t206226,t100]) ).
cnf(t206228,plain,
top = join(converse(complement(sk0)),join(X1,join(zero,one))),
inference(step,[status(thm)],[t206227,t44]) ).
cnf(t3107,plain,
join(converse(complement(sk0)),join(X1,join(zero,one))) = top,
inference(orient,[status(thm)],[t206228]) ).
cnf(t3112,plain,
top = join(converse(complement(sk0)),join(join(zero,one),X1)),
inference(cp,[status(thm)],[t3107,t44]) ).
cnf(t206325,plain,
top = join(converse(complement(sk0)),join(zero,join(one,X1))),
inference(step,[status(thm)],[t3112,t47]) ).
cnf(t3706,plain,
join(converse(complement(sk0)),join(zero,join(one,X1))) = top,
inference(orient,[status(thm)],[t206325]) ).
cnf(t3711,plain,
join(zero,join(converse(complement(sk0)),join(one,X1))) = join(zero,top),
inference(cp,[status(thm)],[t2137,t3706]) ).
cnf(t102,plain,
top = join(top,zero),
inference(cp,[status(thm)],[t52,t100]) ).
cnf(t205989,plain,
top = join(zero,top),
inference(step,[status(thm)],[t102,t44]) ).
cnf(t107,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t205989]) ).
cnf(t206349,plain,
join(zero,join(converse(complement(sk0)),join(one,X1))) = top,
inference(step,[status(thm)],[t3711,t107]) ).
cnf(t3877,plain,
join(zero,join(converse(complement(sk0)),join(one,X1))) = top,
inference(orient,[status(thm)],[t206349]) ).
cnf(t5170,plain,
composition(join(zero,join(converse(complement(sk0)),join(one,X1))),zero) = join(zero,composition(top,zero)),
inference(cp,[status(thm)],[t5167,t3877]) ).
cnf(t206415,plain,
composition(top,zero) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t5170,t3877]) ).
cnf(t5206,plain,
join(zero,composition(top,zero)) = composition(top,zero),
inference(orient,[status(thm)],[t206415]) ).
cnf(t206500,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t206499,t5206]) ).
cnf(t7456,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t206500]) ).
cnf(t7458,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t25,t7456]) ).
cnf(t206508,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t7458,t443]) ).
cnf(t206509,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t206508,t7456]) ).
cnf(t7521,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t206509]) ).
cnf(t206512,plain,
zero = composition(join(zero,X1),zero),
inference(step,[status(thm)],[t5311,t7521]) ).
cnf(t7541,plain,
zero = composition(join(zero,X1),zero),
inference(rw,[status(thm)],[t206512]) ).
cnf(t7601,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t7541]) ).
cnf(t7604,plain,
zero = composition(join(X1,zero),zero),
inference(cp,[status(thm)],[t7601,t44]) ).
cnf(t7631,plain,
composition(join(X1,zero),zero) = zero,
inference(orient,[status(thm)],[t7604]) ).
cnf(t7633,plain,
composition(join(join(X1,zero),X2),zero) = join(zero,composition(X2,zero)),
inference(cp,[status(thm)],[t25,t7631]) ).
cnf(t206536,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t7633,t47]) ).
cnf(t206537,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t206536,t7521]) ).
cnf(t7901,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t206537]) ).
cnf(t238,plain,
composition(converse(X1),join(one,X2)) = converse(composition(join(one,converse(X2)),X1)),
inference(cp,[status(thm)],[t192,t232]) ).
cnf(t6850,plain,
converse(composition(join(one,converse(X1)),X2)) = composition(converse(X2),join(one,X1)),
inference(orient,[status(thm)],[t238]) ).
fof(f4,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_associativity) ).
fof(f4_nnf,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t10,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t23,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t27,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t25,t23]) ).
cnf(t585,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t27]) ).
cnf(t7347,plain,
composition(join(X1,composition(X2,top)),top) = join(composition(X1,top),composition(X2,top)),
inference(cp,[status(thm)],[t585,t7344]) ).
cnf(t206628,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(step,[status(thm)],[t7347,t25]) ).
cnf(t9751,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(orient,[status(thm)],[t206628]) ).
cnf(t9763,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t9751,t226]) ).
cnf(t206630,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t9763,t437]) ).
cnf(t206631,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t206630,t7344]) ).
cnf(t9943,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t206631]) ).
cnf(t9945,plain,
top = composition(join(one,X1),top),
inference(cp,[status(thm)],[t9943,t44]) ).
cnf(t9975,plain,
composition(join(one,X1),top) = top,
inference(orient,[status(thm)],[t9945]) ).
cnf(t9988,plain,
composition(converse(top),join(one,X1)) = converse(top),
inference(cp,[status(thm)],[t6850,t9975]) ).
cnf(t206634,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t9988,t453]) ).
cnf(t206635,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t206634,t453]) ).
cnf(t10027,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t206635]) ).
cnf(t10028,plain,
top = composition(top,join(X1,one)),
inference(cp,[status(thm)],[t10027,t44]) ).
cnf(t10051,plain,
composition(top,join(X1,one)) = top,
inference(orient,[status(thm)],[t10028]) ).
cnf(t10058,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t55,t10051]) ).
cnf(t206654,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t10058,t453]) ).
cnf(t206655,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t206654,t44]) ).
cnf(t206656,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t206655,t100]) ).
cnf(t206657,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t206656,t7456]) ).
cnf(t10857,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t206657]) ).
cnf(t10866,plain,
zero = composition(join(X1,complement(join(X2,one))),zero),
inference(cp,[status(thm)],[t7901,t10857]) ).
cnf(t11188,plain,
composition(join(X1,complement(join(X2,one))),zero) = zero,
inference(orient,[status(thm)],[t10866]) ).
fof(f2,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan) ).
fof(f2_nnf,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t14,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t19,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t46,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t19]) ).
cnf(t206670,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t46,t44]) ).
cnf(t206671,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t206670,t88]) ).
cnf(t206672,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t206671,t44]) ).
cnf(t11678,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t206672]) ).
cnf(t11826,plain,
zero = composition(X1,zero),
inference(cp,[status(thm)],[t11188,t11678]) ).
cnf(t11831,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t11826]) ).
cnf(t11835,plain,
composition(converse(zero),X1) = converse(zero),
inference(cp,[status(thm)],[t192,t11831]) ).
cnf(t11867,plain,
composition(converse(zero),X1) = converse(zero),
inference(orient,[status(thm)],[t11835]) ).
cnf(t11868,plain,
converse(zero) = zero,
inference(cp,[status(thm)],[t11867,t11831]) ).
cnf(t11920,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t11868]) ).
cnf(t206684,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t11867,t11920]) ).
cnf(t206685,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t206684,t11920]) ).
cnf(t11984,plain,
composition(zero,X1) = zero,
inference(rw,[status(thm)],[t206685]) ).
cnf(t12007,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t11984]) ).
cnf(t12018,plain,
complement(X1) = join(complement(X1),composition(converse(zero),complement(zero))),
inference(cp,[status(thm)],[t55,t12007]) ).
cnf(t206711,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t12018,t11920]) ).
cnf(t206712,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t206711,t12007]) ).
cnf(t206713,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t206712,t44]) ).
cnf(t12045,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t206713]) ).
cnf(t206726,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t131,t12045]) ).
cnf(t12105,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t206726]) ).
cnf(t12150,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t12105]) ).
cnf(t11679,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t11678,t95]) ).
cnf(t206744,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t11679,t88]) ).
cnf(t12218,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t206744]) ).
cnf(t12223,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t308,t12218]) ).
cnf(t206746,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t12223,t12218]) ).
cnf(t12235,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t206746]) ).
cnf(t12241,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t12235,t44]) ).
cnf(t12307,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t12241]) ).
cnf(t12319,plain,
X1 = join(meet(X1,zero),complement(complement(X1))),
inference(cp,[status(thm)],[t11678,t12307]) ).
cnf(t12054,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t12045,t52]) ).
cnf(t12106,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t12054]) ).
cnf(t12111,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t88,t12106]) ).
cnf(t206731,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t12111,t437]) ).
cnf(t206732,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t206731,t100]) ).
cnf(t12144,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t206732]) ).
cnf(t206785,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t12319,t12144]) ).
cnf(t206786,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t206785,t12045]) ).
cnf(t206787,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t206786,t12150]) ).
cnf(t12361,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t206787]) ).
cnf(t206788,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t12150,t12361]) ).
cnf(t12362,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t206788]) ).
cnf(t264,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t263,t88]) ).
cnf(t206059,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t264,t88]) ).
cnf(t206060,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t206059,t88]) ).
cnf(t672,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t206060]) ).
cnf(t673,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t672,t109]) ).
cnf(t693,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t673]) ).
cnf(t206751,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t12218,t12235]) ).
cnf(t12283,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t206751]) ).
cnf(t12327,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t12283]) ).
cnf(t12328,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t693,t12327]) ).
cnf(t206798,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t12328,t12327]) ).
cnf(t206799,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t206798,t12327]) ).
cnf(t12392,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t206799]) ).
cnf(t12400,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t47,t12392]) ).
cnf(t12449,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t12400]) ).
cnf(t12475,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t12449,t11678]) ).
cnf(t206801,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t12475,t11678]) ).
cnf(t206802,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t206801,t44]) ).
cnf(t12485,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t206802]) ).
cnf(t12487,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t12485,t109]) ).
cnf(t12521,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t12487]) ).
cnf(t305,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t88,t295]) ).
cnf(t1772,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t305]) ).
cnf(t206782,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1772,t12327]) ).
cnf(t12358,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t206782]) ).
cnf(t13215,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t12358]) ).
cnf(t13258,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t13215,t12362]) ).
cnf(t14278,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t13258]) ).
cnf(t14285,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t12521,t14278]) ).
cnf(t133,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t131,t88]) ).
cnf(t6311,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t133]) ).
cnf(t206747,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t6311,t12235]) ).
cnf(t12236,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t206747]) ).
cnf(t206794,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t12236,t12361]) ).
cnf(t12389,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t206794]) ).
cnf(t14183,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t12389]) ).
cnf(t206836,plain,
complement(X1) = complement(meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t14285,t14183]) ).
cnf(t14374,plain,
complement(meet(X1,join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t206836]) ).
cnf(t14435,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t12362,t14374]) ).
cnf(t206837,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t14435,t12362]) ).
cnf(t14459,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t206837]) ).
cnf(t227,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t25,t226]) ).
cnf(t83099,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t227]) ).
cnf(t245,plain,
join(one,converse(sk0)) = converse(one),
inference(cp,[status(thm)],[t243,t84]) ).
cnf(t206000,plain,
join(one,converse(sk0)) = one,
inference(step,[status(thm)],[t245,t215]) ).
cnf(t260,plain,
join(one,converse(sk0)) = one,
inference(orient,[status(thm)],[t206000]) ).
cnf(t262,plain,
join(one,join(converse(sk0),X1)) = join(one,X1),
inference(cp,[status(thm)],[t47,t260]) ).
cnf(t506,plain,
join(one,join(converse(sk0),X1)) = join(one,X1),
inference(orient,[status(thm)],[t262]) ).
cnf(t507,plain,
join(one,converse(X1)) = join(one,converse(join(sk0,X1))),
inference(cp,[status(thm)],[t506,t61]) ).
cnf(t648,plain,
join(one,converse(join(sk0,X1))) = join(one,converse(X1)),
inference(orient,[status(thm)],[t507]) ).
cnf(t650,plain,
join(one,converse(converse(join(sk0,X1)))) = converse(join(one,converse(X1))),
inference(cp,[status(thm)],[t232,t648]) ).
cnf(t206056,plain,
join(one,join(sk0,X1)) = converse(join(one,converse(X1))),
inference(step,[status(thm)],[t650,t22]) ).
cnf(t206057,plain,
join(one,join(sk0,X1)) = join(one,converse(converse(X1))),
inference(step,[status(thm)],[t206056,t232]) ).
cnf(t206058,plain,
join(one,join(sk0,X1)) = join(one,X1),
inference(step,[status(thm)],[t206057,t22]) ).
cnf(t653,plain,
join(one,join(sk0,X1)) = join(one,X1),
inference(orient,[status(thm)],[t206058]) ).
cnf(t12492,plain,
join(one,meet(sk0,X1)) = join(one,sk0),
inference(cp,[status(thm)],[t653,t12485]) ).
cnf(t206804,plain,
join(one,meet(sk0,X1)) = join(sk0,one),
inference(step,[status(thm)],[t12492,t44]) ).
cnf(t206805,plain,
join(one,meet(sk0,X1)) = one,
inference(step,[status(thm)],[t206804,t84]) ).
cnf(t12743,plain,
join(one,meet(sk0,X1)) = one,
inference(orient,[status(thm)],[t206805]) ).
cnf(t83262,plain,
join(X1,composition(meet(sk0,X2),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t83099,t12743]) ).
cnf(t208320,plain,
join(X1,composition(meet(sk0,X2),X1)) = X1,
inference(step,[status(thm)],[t83262,t226]) ).
cnf(t86692,plain,
join(X1,composition(meet(sk0,X2),X1)) = X1,
inference(orient,[status(thm)],[t208320]) ).
cnf(t206826,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t11678,t13215]) ).
cnf(t13298,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t206826]) ).
cnf(t26189,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t13298]) ).
cnf(t26276,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t26189,t109]) ).
cnf(t51849,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t26276]) ).
cnf(t13216,plain,
meet(X1,complement(join(X2,X1))) = complement(top),
inference(cp,[status(thm)],[t13215,t4242]) ).
cnf(t206827,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(step,[status(thm)],[t13216,t100]) ).
cnf(t13299,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t206827]) ).
cnf(t12495,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t47,t12485]) ).
cnf(t17925,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t12495]) ).
cnf(t17962,plain,
join(X1,meet(X2,meet(X1,X3))) = join(X1,meet(X1,X3)),
inference(cp,[status(thm)],[t17925,t12521]) ).
cnf(t207010,plain,
join(X1,meet(X2,meet(X1,X3))) = X1,
inference(step,[status(thm)],[t17962,t12485]) ).
cnf(t18098,plain,
join(X1,meet(X2,meet(X1,X3))) = X1,
inference(orient,[status(thm)],[t207010]) ).
cnf(t14462,plain,
meet(X1,X2) = meet(meet(X1,X2),X2),
inference(cp,[status(thm)],[t14459,t12521]) ).
cnf(t206841,plain,
meet(X1,X2) = meet(X2,meet(X1,X2)),
inference(step,[status(thm)],[t14462,t109]) ).
cnf(t14712,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t206841]) ).
cnf(t18100,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t18098,t14712]) ).
cnf(t18344,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t18100]) ).
cnf(t18398,plain,
zero = meet(meet(X1,meet(X2,X3)),complement(X3)),
inference(cp,[status(thm)],[t13299,t18344]) ).
cnf(t207476,plain,
zero = meet(complement(X3),meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t18398,t109]) ).
cnf(t44169,plain,
meet(complement(X1),meet(X2,meet(X3,X1))) = zero,
inference(orient,[status(thm)],[t207476]) ).
cnf(t12530,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t47,t12521]) ).
cnf(t18688,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t12530]) ).
cnf(t26303,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t18688,t26189]) ).
cnf(t26949,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t26303]) ).
cnf(t26976,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t26949,t109]) ).
cnf(t27561,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t26976]) ).
cnf(t27623,plain,
meet(X1,complement(meet(complement(complement(X1)),X2))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t13215,t27561]) ).
cnf(t304,plain,
meet(complement(X1),X2) = complement(join(meet(X1,X1),complement(X2))),
inference(cp,[status(thm)],[t88,t295]) ).
cnf(t1722,plain,
complement(join(meet(X1,X1),complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t304]) ).
cnf(t206783,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(step,[status(thm)],[t1722,t12327]) ).
cnf(t12359,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(rw,[status(thm)],[t206783]) ).
cnf(t14125,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t12359]) ).
cnf(t14144,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t12362,t14125]) ).
cnf(t14339,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t14144]) ).
cnf(t207190,plain,
meet(X1,join(complement(X1),complement(X2))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t27623,t14339]) ).
cnf(t207191,plain,
meet(X1,complement(meet(X1,X2))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t207190,t14183]) ).
cnf(t207192,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t207191,t13215]) ).
cnf(t31035,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t207192]) ).
cnf(t42,plain,
composition(meet(X1,composition(one,converse(X2))),meet(X2,composition(converse(X1),one))) = join(meet(composition(X1,X2),one),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(cp,[status(thm)],[t34,t18]) ).
cnf(t206569,plain,
composition(meet(X1,converse(X2)),meet(X2,composition(converse(X1),one))) = join(meet(composition(X1,X2),one),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t42,t226]) ).
cnf(t206570,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(composition(X1,X2),one),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t206569,t18]) ).
cnf(t206571,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(one,composition(X1,X2)),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t206570,t109]) ).
cnf(t206572,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(one,composition(X1,X2)),composition(meet(X1,converse(X2)),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t206571,t226]) ).
cnf(t8502,plain,
join(meet(one,composition(X1,X2)),composition(meet(X1,converse(X2)),meet(X2,converse(X1)))) = composition(meet(X1,converse(X2)),meet(X2,converse(X1))),
inference(orient,[status(thm)],[t206572]) ).
cnf(c17,plain,
join(sk1,one) = one,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t3,plain,
join(sk1,one) = one,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t86,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t244,plain,
join(one,converse(sk1)) = converse(one),
inference(cp,[status(thm)],[t243,t86]) ).
cnf(t205999,plain,
join(one,converse(sk1)) = one,
inference(step,[status(thm)],[t244,t215]) ).
cnf(t257,plain,
join(one,converse(sk1)) = one,
inference(orient,[status(thm)],[t205999]) ).
cnf(t259,plain,
join(one,join(converse(sk1),X1)) = join(one,X1),
inference(cp,[status(thm)],[t47,t257]) ).
cnf(t495,plain,
join(one,join(converse(sk1),X1)) = join(one,X1),
inference(orient,[status(thm)],[t259]) ).
cnf(t496,plain,
join(one,converse(X1)) = join(one,converse(join(sk1,X1))),
inference(cp,[status(thm)],[t495,t61]) ).
cnf(t632,plain,
join(one,converse(join(sk1,X1))) = join(one,converse(X1)),
inference(orient,[status(thm)],[t496]) ).
cnf(t12545,plain,
join(one,converse(meet(X1,sk1))) = join(one,converse(sk1)),
inference(cp,[status(thm)],[t632,t12521]) ).
cnf(t206817,plain,
join(one,converse(meet(X1,sk1))) = one,
inference(step,[status(thm)],[t12545,t257]) ).
cnf(t13073,plain,
join(one,converse(meet(X1,sk1))) = one,
inference(orient,[status(thm)],[t206817]) ).
cnf(t13309,plain,
zero = meet(converse(meet(X1,sk1)),complement(one)),
inference(cp,[status(thm)],[t13299,t13073]) ).
cnf(t206903,plain,
zero = meet(complement(one),converse(meet(X1,sk1))),
inference(step,[status(thm)],[t13309,t109]) ).
cnf(t15527,plain,
meet(complement(one),converse(meet(X1,sk1))) = zero,
inference(orient,[status(thm)],[t206903]) ).
cnf(t15534,plain,
composition(meet(complement(one),converse(meet(X1,sk1))),meet(meet(X1,sk1),converse(complement(one)))) = join(meet(one,composition(complement(one),meet(X1,sk1))),composition(zero,meet(meet(X1,sk1),converse(complement(one))))),
inference(cp,[status(thm)],[t8502,t15527]) ).
cnf(t207333,plain,
composition(zero,meet(meet(X1,sk1),converse(complement(one)))) = join(meet(one,composition(complement(one),meet(X1,sk1))),composition(zero,meet(meet(X1,sk1),converse(complement(one))))),
inference(step,[status(thm)],[t15534,t15527]) ).
cnf(t207334,plain,
zero = join(meet(one,composition(complement(one),meet(X1,sk1))),composition(zero,meet(meet(X1,sk1),converse(complement(one))))),
inference(step,[status(thm)],[t207333,t12007]) ).
cnf(t207335,plain,
zero = join(meet(one,composition(complement(one),meet(X1,sk1))),zero),
inference(step,[status(thm)],[t207334,t12007]) ).
cnf(t207336,plain,
zero = meet(one,composition(complement(one),meet(X1,sk1))),
inference(step,[status(thm)],[t207335,t12307]) ).
cnf(t40500,plain,
meet(one,composition(complement(one),meet(X1,sk1))) = zero,
inference(orient,[status(thm)],[t207336]) ).
cnf(t40501,plain,
zero = meet(one,composition(complement(one),sk1)),
inference(cp,[status(thm)],[t40500,t12327]) ).
cnf(t40517,plain,
meet(one,composition(complement(one),sk1)) = zero,
inference(orient,[status(thm)],[t40501]) ).
cnf(t40524,plain,
meet(one,complement(composition(complement(one),sk1))) = meet(one,complement(zero)),
inference(cp,[status(thm)],[t31035,t40517]) ).
cnf(t207339,plain,
meet(one,complement(composition(complement(one),sk1))) = meet(one,top),
inference(step,[status(thm)],[t40524,t12106]) ).
cnf(t12364,plain,
X1 = meet(X1,top),
inference(cp,[status(thm)],[t12361,t109]) ).
cnf(t12433,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t12364]) ).
cnf(t207340,plain,
meet(one,complement(composition(complement(one),sk1))) = one,
inference(step,[status(thm)],[t207339,t12433]) ).
cnf(t40545,plain,
meet(one,complement(composition(complement(one),sk1))) = one,
inference(orient,[status(thm)],[t207340]) ).
cnf(t44297,plain,
zero = meet(complement(complement(composition(complement(one),sk1))),meet(X1,one)),
inference(cp,[status(thm)],[t44169,t40545]) ).
cnf(t207954,plain,
zero = meet(composition(complement(one),sk1),meet(X1,one)),
inference(step,[status(thm)],[t44297,t12362]) ).
cnf(t65068,plain,
meet(composition(complement(one),sk1),meet(X1,one)) = zero,
inference(orient,[status(thm)],[t207954]) ).
cnf(t14511,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t14459,t44]) ).
cnf(t14558,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t14511]) ).
cnf(t14576,plain,
sk0 = meet(sk0,one),
inference(cp,[status(thm)],[t14558,t84]) ).
cnf(t14621,plain,
meet(sk0,one) = sk0,
inference(orient,[status(thm)],[t14576]) ).
cnf(t65072,plain,
zero = meet(composition(complement(one),sk1),sk0),
inference(cp,[status(thm)],[t65068,t14621]) ).
cnf(t207955,plain,
zero = meet(sk0,composition(complement(one),sk1)),
inference(step,[status(thm)],[t65072,t109]) ).
cnf(t65090,plain,
meet(sk0,composition(complement(one),sk1)) = zero,
inference(orient,[status(thm)],[t207955]) ).
cnf(t65095,plain,
sk0 = join(zero,meet(complement(composition(complement(one),sk1)),sk0)),
inference(cp,[status(thm)],[t51849,t65090]) ).
cnf(t207964,plain,
sk0 = meet(complement(composition(complement(one),sk1)),sk0),
inference(step,[status(thm)],[t65095,t12235]) ).
cnf(t207965,plain,
sk0 = meet(sk0,complement(composition(complement(one),sk1))),
inference(step,[status(thm)],[t207964,t109]) ).
cnf(t65138,plain,
meet(sk0,complement(composition(complement(one),sk1))) = sk0,
inference(orient,[status(thm)],[t207965]) ).
cnf(t86694,plain,
X1 = join(X1,composition(sk0,X1)),
inference(cp,[status(thm)],[t86692,t65138]) ).
cnf(t87044,plain,
join(X1,composition(sk0,X1)) = X1,
inference(orient,[status(thm)],[t86694]) ).
cnf(t87073,plain,
composition(sk0,X1) = meet(composition(sk0,X1),X1),
inference(cp,[status(thm)],[t14459,t87044]) ).
cnf(t208353,plain,
composition(sk0,X1) = meet(X1,composition(sk0,X1)),
inference(step,[status(thm)],[t87073,t109]) ).
cnf(t87295,plain,
meet(X1,composition(sk0,X1)) = composition(sk0,X1),
inference(orient,[status(thm)],[t208353]) ).
cnf(t29,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t28,t22]) ).
cnf(t182,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t29]) ).
cnf(t183,plain,
composition(X1,converse(composition(X2,X3))) = converse(composition(X2,composition(X3,converse(X1)))),
inference(cp,[status(thm)],[t182,t23]) ).
cnf(t6503,plain,
converse(composition(X1,composition(X2,converse(X3)))) = composition(X3,converse(composition(X1,X2))),
inference(orient,[status(thm)],[t183]) ).
cnf(t27588,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t27561,t12362]) ).
cnf(t30886,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t27588]) ).
cnf(t40,plain,
composition(meet(X1,composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(X1),X2))) = join(meet(composition(X1,converse(X3)),X2),composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t34,t22]) ).
cnf(t206495,plain,
composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2))) = join(meet(composition(X1,converse(X3)),X2),composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2)))),
inference(step,[status(thm)],[t40,t22]) ).
cnf(t7367,plain,
join(meet(composition(X1,converse(X2)),X3),composition(meet(X1,composition(X3,X2)),meet(converse(X2),composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,X2)),meet(converse(X2),composition(converse(X1),X3))),
inference(orient,[status(thm)],[t206495]) ).
cnf(t1866,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t1856,t22]) ).
cnf(t1884,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t1866]) ).
cnf(t4253,plain,
top = join(complement(composition(X1,complement(converse(X1)))),complement(one)),
inference(cp,[status(thm)],[t4242,t1884]) ).
cnf(t206442,plain,
top = join(complement(one),complement(composition(X1,complement(converse(X1))))),
inference(step,[status(thm)],[t4253,t44]) ).
cnf(t5807,plain,
join(complement(one),complement(composition(X1,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t206442]) ).
cnf(t5822,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t88,t5807]) ).
cnf(t206443,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t5822,t100]) ).
cnf(t5827,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t206443]) ).
cnf(t5837,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t5827,t22]) ).
cnf(t5848,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t5837]) ).
cnf(t5869,plain,
zero = meet(one,composition(converse(complement(X1)),meet(X1,X1))),
inference(cp,[status(thm)],[t5848,t295]) ).
cnf(t6222,plain,
meet(one,composition(converse(complement(X1)),meet(X1,X1))) = zero,
inference(orient,[status(thm)],[t5869]) ).
cnf(t206784,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(step,[status(thm)],[t6222,t12327]) ).
cnf(t12360,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(rw,[status(thm)],[t206784]) ).
cnf(t14964,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t12360]) ).
cnf(t14978,plain,
composition(meet(one,composition(converse(complement(X1)),X1)),meet(converse(X1),composition(converse(one),converse(complement(X1))))) = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(cp,[status(thm)],[t7367,t14964]) ).
cnf(t206866,plain,
composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1))))) = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t14978,t14964]) ).
cnf(t206867,plain,
zero = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t206866,t12007]) ).
cnf(t206868,plain,
zero = join(meet(converse(complement(X1)),composition(one,converse(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t206867,t109]) ).
cnf(t206869,plain,
zero = join(meet(converse(complement(X1)),converse(X1)),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t206868,t226]) ).
cnf(t206870,plain,
zero = join(meet(converse(X1),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t206869,t109]) ).
cnf(t206871,plain,
zero = join(meet(converse(X1),converse(complement(X1))),zero),
inference(step,[status(thm)],[t206870,t12007]) ).
cnf(t206872,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(step,[status(thm)],[t206871,t12307]) ).
cnf(t15008,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t206872]) ).
cnf(t30942,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t30886,t15008]) ).
cnf(t207233,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t30942,t44]) ).
cnf(t207234,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t207233,t12307]) ).
cnf(t34958,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t207234]) ).
cnf(t34963,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t34958,t12362]) ).
cnf(t206029,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t370,t453]) ).
cnf(t456,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t206029]) ).
cnf(t13254,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t13215,t456]) ).
cnf(t207129,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(step,[status(thm)],[t13254,t100]) ).
cnf(t26171,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(orient,[status(thm)],[t207129]) ).
cnf(t27576,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t27561,t26171]) ).
cnf(t207179,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t27576,t12362]) ).
cnf(t207180,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t207179,t12307]) ).
cnf(t29259,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t207180]) ).
cnf(t29277,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t29259,t22]) ).
cnf(t32451,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t29277]) ).
cnf(t207235,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t34963,t32451]) ).
cnf(t35008,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t207235]) ).
cnf(t35013,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t35008,t12362]) ).
cnf(t35072,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t35013]) ).
cnf(t35085,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(cp,[status(thm)],[t35072,t324]) ).
cnf(t36108,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(orient,[status(thm)],[t35085]) ).
cnf(t35100,plain,
complement(meet(converse(X1),X2)) = join(converse(complement(X1)),complement(X2)),
inference(cp,[status(thm)],[t14183,t35072]) ).
cnf(t36662,plain,
join(converse(complement(X1)),complement(X2)) = complement(meet(converse(X1),X2)),
inference(orient,[status(thm)],[t35100]) ).
cnf(t36708,plain,
complement(join(complement(X1),converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(cp,[status(thm)],[t36108,t36662]) ).
cnf(t207292,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t36708,t13215]) ).
cnf(t207293,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t207292,t35008]) ).
cnf(t207294,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t207293,t12362]) ).
cnf(t36738,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t207294]) ).
cnf(t36751,plain,
meet(X1,converse(X2)) = converse(meet(X2,converse(X1))),
inference(cp,[status(thm)],[t36738,t109]) ).
cnf(t36853,plain,
converse(meet(X1,converse(X2))) = meet(X2,converse(X1)),
inference(orient,[status(thm)],[t36751]) ).
cnf(t48,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t47,t44]) ).
cnf(t13369,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t48]) ).
cnf(t14589,plain,
X1 = meet(X1,join(X2,join(X1,X3))),
inference(cp,[status(thm)],[t14558,t13369]) ).
cnf(t15862,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t14589]) ).
cnf(t18795,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(cp,[status(thm)],[t15862,t18688]) ).
cnf(t21770,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t18795]) ).
cnf(t14632,plain,
composition(meet(sk0,one),meet(one,composition(converse(sk0),one))) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(cp,[status(thm)],[t3225,t14621]) ).
cnf(t206998,plain,
composition(sk0,meet(one,composition(converse(sk0),one))) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t14632,t14621]) ).
cnf(t206999,plain,
composition(sk0,meet(one,converse(sk0))) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t206998,t18]) ).
cnf(t14495,plain,
converse(sk0) = meet(converse(sk0),one),
inference(cp,[status(thm)],[t14459,t260]) ).
cnf(t206839,plain,
converse(sk0) = meet(one,converse(sk0)),
inference(step,[status(thm)],[t14495,t109]) ).
cnf(t14545,plain,
meet(one,converse(sk0)) = converse(sk0),
inference(orient,[status(thm)],[t206839]) ).
cnf(t207000,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t206999,t14545]) ).
cnf(t207001,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t207000,t14621]) ).
cnf(t207002,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,meet(one,converse(sk0)))),
inference(step,[status(thm)],[t207001,t18]) ).
cnf(t207003,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,converse(sk0))),
inference(step,[status(thm)],[t207002,t14545]) ).
cnf(t17603,plain,
join(sk0,composition(sk0,converse(sk0))) = composition(sk0,converse(sk0)),
inference(orient,[status(thm)],[t207003]) ).
cnf(t17604,plain,
sk0 = meet(sk0,composition(sk0,converse(sk0))),
inference(cp,[status(thm)],[t14558,t17603]) ).
cnf(t17617,plain,
meet(sk0,composition(sk0,converse(sk0))) = sk0,
inference(orient,[status(thm)],[t17604]) ).
cnf(t21787,plain,
meet(sk0,composition(sk0,converse(sk0))) = meet(sk0,join(composition(sk0,converse(sk0)),X1)),
inference(cp,[status(thm)],[t21770,t17617]) ).
cnf(t207502,plain,
sk0 = meet(sk0,join(composition(sk0,converse(sk0)),X1)),
inference(step,[status(thm)],[t21787,t17617]) ).
cnf(t47391,plain,
meet(sk0,join(composition(sk0,converse(sk0)),X1)) = sk0,
inference(orient,[status(thm)],[t207502]) ).
cnf(t47394,plain,
sk0 = meet(sk0,composition(join(sk0,X1),converse(sk0))),
inference(cp,[status(thm)],[t47391,t25]) ).
cnf(t68309,plain,
meet(sk0,composition(join(sk0,X1),converse(sk0))) = sk0,
inference(orient,[status(thm)],[t47394]) ).
cnf(t68312,plain,
sk0 = meet(sk0,composition(one,converse(sk0))),
inference(cp,[status(thm)],[t68309,t84]) ).
cnf(t208039,plain,
sk0 = meet(sk0,converse(sk0)),
inference(step,[status(thm)],[t68312,t226]) ).
cnf(t68413,plain,
meet(sk0,converse(sk0)) = sk0,
inference(orient,[status(thm)],[t208039]) ).
cnf(t68478,plain,
meet(sk0,converse(sk0)) = converse(sk0),
inference(cp,[status(thm)],[t36853,t68413]) ).
cnf(t208040,plain,
sk0 = converse(sk0),
inference(step,[status(thm)],[t68478,t68413]) ).
cnf(t68503,plain,
converse(sk0) = sk0,
inference(orient,[status(thm)],[t208040]) ).
cnf(t68567,plain,
composition(sk0,converse(composition(X1,X2))) = converse(composition(X1,composition(X2,sk0))),
inference(cp,[status(thm)],[t6503,t68503]) ).
cnf(t154245,plain,
converse(composition(X1,composition(X2,sk0))) = composition(sk0,converse(composition(X1,X2))),
inference(orient,[status(thm)],[t68567]) ).
cnf(t230,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(converse(one),X1))) = join(meet(X2,X1),composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(converse(one),X1)))),
inference(cp,[status(thm)],[t34,t226]) ).
cnf(t208421,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(one,X1))) = join(meet(X2,X1),composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(converse(one),X1)))),
inference(step,[status(thm)],[t230,t215]) ).
cnf(t208422,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = join(meet(X2,X1),composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(converse(one),X1)))),
inference(step,[status(thm)],[t208421,t226]) ).
cnf(t208423,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = join(meet(X2,X1),composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(one,X1)))),
inference(step,[status(thm)],[t208422,t215]) ).
cnf(t208424,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = join(meet(X2,X1),composition(meet(one,composition(X1,converse(X2))),meet(X2,X1))),
inference(step,[status(thm)],[t208423,t226]) ).
cnf(t83319,plain,
join(X1,composition(meet(one,X2),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t83099,t12485]) ).
cnf(t208366,plain,
join(X1,composition(meet(one,X2),X1)) = X1,
inference(step,[status(thm)],[t83319,t226]) ).
cnf(t88435,plain,
join(X1,composition(meet(one,X2),X1)) = X1,
inference(orient,[status(thm)],[t208366]) ).
cnf(t208425,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = meet(X2,X1),
inference(step,[status(thm)],[t208424,t88435]) ).
cnf(t91799,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t208425]) ).
cnf(t14507,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t14459,t47]) ).
cnf(t15637,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t14507]) ).
cnf(t15654,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(cp,[status(thm)],[t15637,t12485]) ).
cnf(t19846,plain,
meet(meet(X1,X2),join(X3,X1)) = meet(X1,X2),
inference(orient,[status(thm)],[t15654]) ).
cnf(t19847,plain,
meet(X1,X2) = meet(join(X3,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t19846,t109]) ).
cnf(t22054,plain,
meet(join(X1,X2),meet(X2,X3)) = meet(X2,X3),
inference(orient,[status(thm)],[t19847]) ).
cnf(t87127,plain,
join(X1,converse(composition(sk0,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t324,t87044]) ).
cnf(t68512,plain,
converse(composition(sk0,X1)) = composition(converse(X1),sk0),
inference(cp,[status(thm)],[t28,t68503]) ).
cnf(t69344,plain,
converse(composition(sk0,X1)) = composition(converse(X1),sk0),
inference(orient,[status(thm)],[t68512]) ).
cnf(t208350,plain,
join(X1,composition(converse(converse(X1)),sk0)) = converse(converse(X1)),
inference(step,[status(thm)],[t87127,t69344]) ).
cnf(t208351,plain,
join(X1,composition(X1,sk0)) = converse(converse(X1)),
inference(step,[status(thm)],[t208350,t22]) ).
cnf(t208352,plain,
join(X1,composition(X1,sk0)) = X1,
inference(step,[status(thm)],[t208351,t22]) ).
cnf(t87210,plain,
join(X1,composition(X1,sk0)) = X1,
inference(orient,[status(thm)],[t208352]) ).
cnf(t87238,plain,
composition(X1,sk0) = meet(composition(X1,sk0),X1),
inference(cp,[status(thm)],[t14459,t87210]) ).
cnf(t208354,plain,
composition(X1,sk0) = meet(X1,composition(X1,sk0)),
inference(step,[status(thm)],[t87238,t109]) ).
cnf(t87549,plain,
meet(X1,composition(X1,sk0)) = composition(X1,sk0),
inference(orient,[status(thm)],[t208354]) ).
cnf(t87572,plain,
meet(X1,composition(X1,sk0)) = meet(join(X2,X1),composition(X1,sk0)),
inference(cp,[status(thm)],[t22054,t87549]) ).
cnf(t208589,plain,
composition(X1,sk0) = meet(join(X2,X1),composition(X1,sk0)),
inference(step,[status(thm)],[t87572,t87549]) ).
cnf(t105399,plain,
meet(join(X1,X2),composition(X2,sk0)) = composition(X2,sk0),
inference(orient,[status(thm)],[t208589]) ).
cnf(t17961,plain,
join(X1,meet(meet(X1,X2),X3)) = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t17925,t12485]) ).
cnf(t207009,plain,
join(X1,meet(meet(X1,X2),X3)) = X1,
inference(step,[status(thm)],[t17961,t12485]) ).
cnf(t18040,plain,
join(X1,meet(meet(X1,X2),X3)) = X1,
inference(orient,[status(thm)],[t207009]) ).
cnf(t18044,plain,
X1 = join(X1,meet(meet(X2,X1),X3)),
inference(cp,[status(thm)],[t18040,t14712]) ).
cnf(t18154,plain,
join(X1,meet(meet(X2,X1),X3)) = X1,
inference(orient,[status(thm)],[t18044]) ).
cnf(t18210,plain,
zero = meet(meet(meet(X1,X2),X3),complement(X2)),
inference(cp,[status(thm)],[t13299,t18154]) ).
cnf(t207468,plain,
zero = meet(complement(X2),meet(meet(X1,X2),X3)),
inference(step,[status(thm)],[t18210,t109]) ).
cnf(t43838,plain,
meet(complement(X1),meet(meet(X2,X1),X3)) = zero,
inference(orient,[status(thm)],[t207468]) ).
cnf(t12544,plain,
join(one,converse(meet(X1,sk0))) = join(one,converse(sk0)),
inference(cp,[status(thm)],[t648,t12521]) ).
cnf(t206816,plain,
join(one,converse(meet(X1,sk0))) = one,
inference(step,[status(thm)],[t12544,t260]) ).
cnf(t13049,plain,
join(one,converse(meet(X1,sk0))) = one,
inference(orient,[status(thm)],[t206816]) ).
cnf(t13311,plain,
zero = meet(converse(meet(X1,sk0)),complement(one)),
inference(cp,[status(thm)],[t13299,t13049]) ).
cnf(t206905,plain,
zero = meet(complement(one),converse(meet(X1,sk0))),
inference(step,[status(thm)],[t13311,t109]) ).
cnf(t15549,plain,
meet(complement(one),converse(meet(X1,sk0))) = zero,
inference(orient,[status(thm)],[t206905]) ).
cnf(t15557,plain,
composition(meet(meet(X1,sk0),converse(complement(one))),meet(complement(one),converse(meet(X1,sk0)))) = join(meet(one,composition(meet(X1,sk0),complement(one))),composition(meet(meet(X1,sk0),converse(complement(one))),zero)),
inference(cp,[status(thm)],[t8502,t15549]) ).
cnf(t13261,plain,
join(complement(X1),X2) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t12362,t13215]) ).
cnf(t14295,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t13261]) ).
cnf(t5208,plain,
join(zero,join(composition(top,zero),X1)) = join(composition(top,zero),X1),
inference(cp,[status(thm)],[t47,t5206]) ).
cnf(t5328,plain,
join(zero,join(composition(top,zero),X1)) = join(composition(top,zero),X1),
inference(orient,[status(thm)],[t5208]) ).
cnf(t5336,plain,
join(composition(top,zero),X1) = join(zero,join(X1,composition(top,zero))),
inference(cp,[status(thm)],[t5328,t44]) ).
cnf(t5441,plain,
join(zero,join(X1,composition(top,zero))) = join(composition(top,zero),X1),
inference(orient,[status(thm)],[t5336]) ).
cnf(t5444,plain,
join(composition(top,zero),complement(one)) = join(zero,complement(one)),
inference(cp,[status(thm)],[t5441,t1881]) ).
cnf(t206430,plain,
join(complement(one),composition(top,zero)) = join(zero,complement(one)),
inference(step,[status(thm)],[t5444,t44]) ).
cnf(t206431,plain,
complement(one) = join(zero,complement(one)),
inference(step,[status(thm)],[t206430,t1881]) ).
cnf(t5466,plain,
join(zero,complement(one)) = complement(one),
inference(orient,[status(thm)],[t206431]) ).
cnf(t5479,plain,
meet(top,one) = complement(complement(one)),
inference(cp,[status(thm)],[t131,t5466]) ).
cnf(t206432,plain,
meet(top,one) = meet(one,one),
inference(step,[status(thm)],[t5479,t295]) ).
cnf(t5482,plain,
meet(one,one) = meet(top,one),
inference(orient,[status(thm)],[t206432]) ).
cnf(t6233,plain,
zero = meet(one,composition(converse(complement(one)),meet(top,one))),
inference(cp,[status(thm)],[t6222,t5482]) ).
cnf(t6302,plain,
meet(one,composition(converse(complement(one)),meet(top,one))) = zero,
inference(orient,[status(thm)],[t6233]) ).
cnf(t206796,plain,
meet(one,composition(converse(complement(one)),one)) = zero,
inference(step,[status(thm)],[t6302,t12361]) ).
cnf(t206797,plain,
meet(one,converse(complement(one))) = zero,
inference(step,[status(thm)],[t206796,t18]) ).
cnf(t12391,plain,
meet(one,converse(complement(one))) = zero,
inference(rw,[status(thm)],[t206797]) ).
cnf(t12443,plain,
meet(one,converse(complement(one))) = zero,
inference(orient,[status(thm)],[t12391]) ).
cnf(t26265,plain,
one = join(zero,meet(one,complement(converse(complement(one))))),
inference(cp,[status(thm)],[t26189,t12443]) ).
cnf(t207137,plain,
one = meet(one,complement(converse(complement(one)))),
inference(step,[status(thm)],[t26265,t12235]) ).
cnf(t26633,plain,
meet(one,complement(converse(complement(one)))) = one,
inference(orient,[status(thm)],[t207137]) ).
cnf(t26655,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(cp,[status(thm)],[t14295,t26633]) ).
cnf(t26767,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t26655]) ).
cnf(t26775,plain,
converse(complement(one)) = meet(converse(complement(one)),complement(one)),
inference(cp,[status(thm)],[t14459,t26767]) ).
cnf(t207144,plain,
converse(complement(one)) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t26775,t109]) ).
cnf(t14503,plain,
converse(X1) = meet(converse(X1),converse(join(X2,X1))),
inference(cp,[status(thm)],[t14459,t61]) ).
cnf(t17651,plain,
meet(converse(X1),converse(join(X2,X1))) = converse(X1),
inference(orient,[status(thm)],[t14503]) ).
cnf(t26777,plain,
converse(converse(complement(one))) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(cp,[status(thm)],[t17651,t26767]) ).
cnf(t207139,plain,
complement(one) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(step,[status(thm)],[t26777,t22]) ).
cnf(t207140,plain,
complement(one) = meet(converse(complement(one)),converse(converse(complement(one)))),
inference(step,[status(thm)],[t207139,t109]) ).
cnf(t207141,plain,
complement(one) = meet(converse(complement(one)),complement(one)),
inference(step,[status(thm)],[t207140,t22]) ).
cnf(t207142,plain,
complement(one) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t207141,t109]) ).
cnf(t26790,plain,
meet(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t207142]) ).
cnf(t207145,plain,
converse(complement(one)) = complement(one),
inference(step,[status(thm)],[t207144,t26790]) ).
cnf(t27048,plain,
converse(complement(one)) = complement(one),
inference(orient,[status(thm)],[t207145]) ).
cnf(t207362,plain,
composition(meet(meet(X1,sk0),complement(one)),meet(complement(one),converse(meet(X1,sk0)))) = join(meet(one,composition(meet(X1,sk0),complement(one))),composition(meet(meet(X1,sk0),converse(complement(one))),zero)),
inference(step,[status(thm)],[t15557,t27048]) ).
cnf(t207363,plain,
composition(meet(complement(one),meet(X1,sk0)),meet(complement(one),converse(meet(X1,sk0)))) = join(meet(one,composition(meet(X1,sk0),complement(one))),composition(meet(meet(X1,sk0),converse(complement(one))),zero)),
inference(step,[status(thm)],[t207362,t109]) ).
cnf(t12746,plain,
one = join(one,meet(X1,sk0)),
inference(cp,[status(thm)],[t12743,t109]) ).
cnf(t12768,plain,
join(one,meet(X1,sk0)) = one,
inference(orient,[status(thm)],[t12746]) ).
cnf(t13319,plain,
zero = meet(meet(X1,sk0),complement(one)),
inference(cp,[status(thm)],[t13299,t12768]) ).
cnf(t206832,plain,
zero = meet(complement(one),meet(X1,sk0)),
inference(step,[status(thm)],[t13319,t109]) ).
cnf(t14028,plain,
meet(complement(one),meet(X1,sk0)) = zero,
inference(orient,[status(thm)],[t206832]) ).
cnf(t207364,plain,
composition(zero,meet(complement(one),converse(meet(X1,sk0)))) = join(meet(one,composition(meet(X1,sk0),complement(one))),composition(meet(meet(X1,sk0),converse(complement(one))),zero)),
inference(step,[status(thm)],[t207363,t14028]) ).
cnf(t207365,plain,
zero = join(meet(one,composition(meet(X1,sk0),complement(one))),composition(meet(meet(X1,sk0),converse(complement(one))),zero)),
inference(step,[status(thm)],[t207364,t12007]) ).
cnf(t207366,plain,
zero = join(meet(one,composition(meet(X1,sk0),complement(one))),zero),
inference(step,[status(thm)],[t207365,t11831]) ).
cnf(t207367,plain,
zero = meet(one,composition(meet(X1,sk0),complement(one))),
inference(step,[status(thm)],[t207366,t12307]) ).
cnf(t40813,plain,
meet(one,composition(meet(X1,sk0),complement(one))) = zero,
inference(orient,[status(thm)],[t207367]) ).
cnf(t40814,plain,
zero = meet(one,composition(sk0,complement(one))),
inference(cp,[status(thm)],[t40813,t12327]) ).
cnf(t40830,plain,
meet(one,composition(sk0,complement(one))) = zero,
inference(orient,[status(thm)],[t40814]) ).
cnf(t40837,plain,
meet(one,complement(composition(sk0,complement(one)))) = meet(one,complement(zero)),
inference(cp,[status(thm)],[t31035,t40830]) ).
cnf(t207370,plain,
meet(one,complement(composition(sk0,complement(one)))) = meet(one,top),
inference(step,[status(thm)],[t40837,t12106]) ).
cnf(t207371,plain,
meet(one,complement(composition(sk0,complement(one)))) = one,
inference(step,[status(thm)],[t207370,t12433]) ).
cnf(t40858,plain,
meet(one,complement(composition(sk0,complement(one)))) = one,
inference(orient,[status(thm)],[t207371]) ).
cnf(t43966,plain,
zero = meet(complement(complement(composition(sk0,complement(one)))),meet(one,X1)),
inference(cp,[status(thm)],[t43838,t40858]) ).
cnf(t207721,plain,
zero = meet(composition(sk0,complement(one)),meet(one,X1)),
inference(step,[status(thm)],[t43966,t12362]) ).
cnf(t59116,plain,
meet(composition(sk0,complement(one)),meet(one,X1)) = zero,
inference(orient,[status(thm)],[t207721]) ).
cnf(t14494,plain,
converse(sk1) = meet(converse(sk1),one),
inference(cp,[status(thm)],[t14459,t257]) ).
cnf(t206838,plain,
converse(sk1) = meet(one,converse(sk1)),
inference(step,[status(thm)],[t14494,t109]) ).
cnf(t14532,plain,
meet(one,converse(sk1)) = converse(sk1),
inference(orient,[status(thm)],[t206838]) ).
cnf(t59153,plain,
zero = meet(composition(sk0,complement(one)),converse(sk1)),
inference(cp,[status(thm)],[t59116,t14532]) ).
cnf(t207723,plain,
zero = meet(converse(sk1),composition(sk0,complement(one))),
inference(step,[status(thm)],[t59153,t109]) ).
cnf(t59208,plain,
meet(converse(sk1),composition(sk0,complement(one))) = zero,
inference(orient,[status(thm)],[t207723]) ).
cnf(t59216,plain,
meet(sk1,converse(composition(sk0,complement(one)))) = converse(zero),
inference(cp,[status(thm)],[t36738,t59208]) ).
cnf(t27051,plain,
converse(composition(X1,complement(one))) = composition(complement(one),converse(X1)),
inference(cp,[status(thm)],[t28,t27048]) ).
cnf(t27304,plain,
converse(composition(X1,complement(one))) = composition(complement(one),converse(X1)),
inference(orient,[status(thm)],[t27051]) ).
cnf(t207751,plain,
meet(sk1,composition(complement(one),converse(sk0))) = converse(zero),
inference(step,[status(thm)],[t59216,t27304]) ).
cnf(t207752,plain,
meet(sk1,composition(complement(one),converse(sk0))) = zero,
inference(step,[status(thm)],[t207751,t11920]) ).
cnf(t59497,plain,
meet(sk1,composition(complement(one),converse(sk0))) = zero,
inference(orient,[status(thm)],[t207752]) ).
cnf(t59511,plain,
composition(meet(sk1,composition(complement(one),converse(sk0))),meet(sk0,composition(converse(sk1),complement(one)))) = join(meet(composition(sk1,sk0),complement(one)),composition(zero,meet(sk0,composition(converse(sk1),complement(one))))),
inference(cp,[status(thm)],[t34,t59497]) ).
cnf(t207753,plain,
composition(zero,meet(sk0,composition(converse(sk1),complement(one)))) = join(meet(composition(sk1,sk0),complement(one)),composition(zero,meet(sk0,composition(converse(sk1),complement(one))))),
inference(step,[status(thm)],[t59511,t59497]) ).
cnf(t207754,plain,
zero = join(meet(composition(sk1,sk0),complement(one)),composition(zero,meet(sk0,composition(converse(sk1),complement(one))))),
inference(step,[status(thm)],[t207753,t12007]) ).
cnf(t207755,plain,
zero = join(meet(complement(one),composition(sk1,sk0)),composition(zero,meet(sk0,composition(converse(sk1),complement(one))))),
inference(step,[status(thm)],[t207754,t109]) ).
cnf(t207756,plain,
zero = join(meet(complement(one),composition(sk1,sk0)),zero),
inference(step,[status(thm)],[t207755,t12007]) ).
cnf(t207757,plain,
zero = meet(complement(one),composition(sk1,sk0)),
inference(step,[status(thm)],[t207756,t12307]) ).
cnf(t59518,plain,
meet(complement(one),composition(sk1,sk0)) = zero,
inference(orient,[status(thm)],[t207757]) ).
cnf(t59519,plain,
join(complement(complement(one)),composition(sk1,sk0)) = join(complement(complement(one)),zero),
inference(cp,[status(thm)],[t30886,t59518]) ).
cnf(t207758,plain,
join(composition(sk1,sk0),complement(complement(one))) = join(complement(complement(one)),zero),
inference(step,[status(thm)],[t59519,t44]) ).
cnf(t207759,plain,
join(composition(sk1,sk0),one) = join(complement(complement(one)),zero),
inference(step,[status(thm)],[t207758,t12362]) ).
cnf(t207760,plain,
join(one,composition(sk1,sk0)) = join(complement(complement(one)),zero),
inference(step,[status(thm)],[t207759,t44]) ).
cnf(t207761,plain,
join(one,composition(sk1,sk0)) = complement(complement(one)),
inference(step,[status(thm)],[t207760,t12307]) ).
cnf(t207762,plain,
join(one,composition(sk1,sk0)) = one,
inference(step,[status(thm)],[t207761,t12362]) ).
cnf(t59538,plain,
join(one,composition(sk1,sk0)) = one,
inference(orient,[status(thm)],[t207762]) ).
cnf(t83151,plain,
join(X1,composition(composition(sk1,sk0),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t83099,t59538]) ).
cnf(t208228,plain,
join(X1,composition(sk1,composition(sk0,X1))) = composition(one,X1),
inference(step,[status(thm)],[t83151,t23]) ).
cnf(t208229,plain,
join(X1,composition(sk1,composition(sk0,X1))) = X1,
inference(step,[status(thm)],[t208228,t226]) ).
cnf(t84427,plain,
join(X1,composition(sk1,composition(sk0,X1))) = X1,
inference(orient,[status(thm)],[t208229]) ).
cnf(t84458,plain,
composition(sk1,composition(sk0,X1)) = meet(composition(sk1,composition(sk0,X1)),X1),
inference(cp,[status(thm)],[t14459,t84427]) ).
cnf(t210206,plain,
composition(sk1,composition(sk0,X1)) = meet(X1,composition(sk1,composition(sk0,X1))),
inference(step,[status(thm)],[t84458,t109]) ).
cnf(t205250,plain,
meet(X1,composition(sk1,composition(sk0,X1))) = composition(sk1,composition(sk0,X1)),
inference(orient,[status(thm)],[t210206]) ).
cnf(t205572,plain,
composition(meet(sk1,converse(composition(sk0,one))),meet(composition(sk0,one),converse(sk1))) = join(composition(sk1,composition(sk0,one)),composition(meet(sk1,converse(composition(sk0,one))),meet(composition(sk0,one),converse(sk1)))),
inference(cp,[status(thm)],[t8502,t205250]) ).
cnf(t210207,plain,
composition(meet(sk1,composition(converse(one),sk0)),meet(composition(sk0,one),converse(sk1))) = join(composition(sk1,composition(sk0,one)),composition(meet(sk1,converse(composition(sk0,one))),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t205572,t69344]) ).
cnf(t210208,plain,
composition(meet(sk1,composition(one,sk0)),meet(composition(sk0,one),converse(sk1))) = join(composition(sk1,composition(sk0,one)),composition(meet(sk1,converse(composition(sk0,one))),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t210207,t215]) ).
cnf(t210209,plain,
composition(meet(sk1,sk0),meet(composition(sk0,one),converse(sk1))) = join(composition(sk1,composition(sk0,one)),composition(meet(sk1,converse(composition(sk0,one))),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t210208,t226]) ).
cnf(t210210,plain,
composition(meet(sk1,sk0),meet(converse(sk1),composition(sk0,one))) = join(composition(sk1,composition(sk0,one)),composition(meet(sk1,converse(composition(sk0,one))),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t210209,t109]) ).
cnf(t14571,plain,
sk1 = meet(sk1,one),
inference(cp,[status(thm)],[t14558,t86]) ).
cnf(t14608,plain,
meet(sk1,one) = sk1,
inference(orient,[status(thm)],[t14571]) ).
cnf(t14619,plain,
composition(meet(sk1,one),meet(one,composition(converse(sk1),one))) = join(sk1,composition(meet(sk1,one),meet(one,composition(converse(sk1),one)))),
inference(cp,[status(thm)],[t3225,t14608]) ).
cnf(t206991,plain,
composition(sk1,meet(one,composition(converse(sk1),one))) = join(sk1,composition(meet(sk1,one),meet(one,composition(converse(sk1),one)))),
inference(step,[status(thm)],[t14619,t14608]) ).
cnf(t206992,plain,
composition(sk1,meet(one,converse(sk1))) = join(sk1,composition(meet(sk1,one),meet(one,composition(converse(sk1),one)))),
inference(step,[status(thm)],[t206991,t18]) ).
cnf(t206993,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(meet(sk1,one),meet(one,composition(converse(sk1),one)))),
inference(step,[status(thm)],[t206992,t14532]) ).
cnf(t206994,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(sk1,meet(one,composition(converse(sk1),one)))),
inference(step,[status(thm)],[t206993,t14608]) ).
cnf(t206995,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(sk1,meet(one,converse(sk1)))),
inference(step,[status(thm)],[t206994,t18]) ).
cnf(t206996,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(sk1,converse(sk1))),
inference(step,[status(thm)],[t206995,t14532]) ).
cnf(t17555,plain,
join(sk1,composition(sk1,converse(sk1))) = composition(sk1,converse(sk1)),
inference(orient,[status(thm)],[t206996]) ).
cnf(t17556,plain,
sk1 = meet(sk1,composition(sk1,converse(sk1))),
inference(cp,[status(thm)],[t14558,t17555]) ).
cnf(t17569,plain,
meet(sk1,composition(sk1,converse(sk1))) = sk1,
inference(orient,[status(thm)],[t17556]) ).
cnf(t21797,plain,
meet(sk1,composition(sk1,converse(sk1))) = meet(sk1,join(composition(sk1,converse(sk1)),X1)),
inference(cp,[status(thm)],[t21770,t17569]) ).
cnf(t207532,plain,
sk1 = meet(sk1,join(composition(sk1,converse(sk1)),X1)),
inference(step,[status(thm)],[t21797,t17569]) ).
cnf(t47878,plain,
meet(sk1,join(composition(sk1,converse(sk1)),X1)) = sk1,
inference(orient,[status(thm)],[t207532]) ).
cnf(t47881,plain,
sk1 = meet(sk1,composition(join(sk1,X1),converse(sk1))),
inference(cp,[status(thm)],[t47878,t25]) ).
cnf(t72499,plain,
meet(sk1,composition(join(sk1,X1),converse(sk1))) = sk1,
inference(orient,[status(thm)],[t47881]) ).
cnf(t72502,plain,
sk1 = meet(sk1,composition(one,converse(sk1))),
inference(cp,[status(thm)],[t72499,t86]) ).
cnf(t208085,plain,
sk1 = meet(sk1,converse(sk1)),
inference(step,[status(thm)],[t72502,t226]) ).
cnf(t72603,plain,
meet(sk1,converse(sk1)) = sk1,
inference(orient,[status(thm)],[t208085]) ).
cnf(t72668,plain,
meet(sk1,converse(sk1)) = converse(sk1),
inference(cp,[status(thm)],[t36853,t72603]) ).
cnf(t208086,plain,
sk1 = converse(sk1),
inference(step,[status(thm)],[t72668,t72603]) ).
cnf(t72693,plain,
converse(sk1) = sk1,
inference(orient,[status(thm)],[t208086]) ).
cnf(t210211,plain,
composition(meet(sk1,sk0),meet(sk1,composition(sk0,one))) = join(composition(sk1,composition(sk0,one)),composition(meet(sk1,converse(composition(sk0,one))),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t210210,t72693]) ).
cnf(t210212,plain,
composition(meet(sk1,sk0),meet(sk1,sk0)) = join(composition(sk1,composition(sk0,one)),composition(meet(sk1,converse(composition(sk0,one))),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t210211,t18]) ).
cnf(t634,plain,
join(one,converse(converse(join(sk1,X1)))) = converse(join(one,converse(X1))),
inference(cp,[status(thm)],[t232,t632]) ).
cnf(t206053,plain,
join(one,join(sk1,X1)) = converse(join(one,converse(X1))),
inference(step,[status(thm)],[t634,t22]) ).
cnf(t206054,plain,
join(one,join(sk1,X1)) = join(one,converse(converse(X1))),
inference(step,[status(thm)],[t206053,t232]) ).
cnf(t206055,plain,
join(one,join(sk1,X1)) = join(one,X1),
inference(step,[status(thm)],[t206054,t22]) ).
cnf(t637,plain,
join(one,join(sk1,X1)) = join(one,X1),
inference(orient,[status(thm)],[t206055]) ).
cnf(t12493,plain,
join(one,meet(sk1,X1)) = join(one,sk1),
inference(cp,[status(thm)],[t637,t12485]) ).
cnf(t206806,plain,
join(one,meet(sk1,X1)) = join(sk1,one),
inference(step,[status(thm)],[t12493,t44]) ).
cnf(t206807,plain,
join(one,meet(sk1,X1)) = one,
inference(step,[status(thm)],[t206806,t86]) ).
cnf(t12792,plain,
join(one,meet(sk1,X1)) = one,
inference(orient,[status(thm)],[t206807]) ).
cnf(t14478,plain,
meet(sk1,X1) = meet(meet(sk1,X1),one),
inference(cp,[status(thm)],[t14459,t12792]) ).
cnf(t206842,plain,
meet(sk1,X1) = meet(one,meet(sk1,X1)),
inference(step,[status(thm)],[t14478,t109]) ).
cnf(t14740,plain,
meet(one,meet(sk1,X1)) = meet(sk1,X1),
inference(orient,[status(thm)],[t206842]) ).
cnf(t92034,plain,
meet(one,meet(sk1,X1)) = composition(meet(one,composition(meet(sk1,X1),converse(one))),meet(sk1,X1)),
inference(cp,[status(thm)],[t91799,t14740]) ).
cnf(t208616,plain,
meet(sk1,X1) = composition(meet(one,composition(meet(sk1,X1),converse(one))),meet(sk1,X1)),
inference(step,[status(thm)],[t92034,t14740]) ).
cnf(t208617,plain,
meet(sk1,X1) = composition(meet(one,composition(meet(sk1,X1),one)),meet(sk1,X1)),
inference(step,[status(thm)],[t208616,t215]) ).
cnf(t208618,plain,
meet(sk1,X1) = composition(meet(one,meet(sk1,X1)),meet(sk1,X1)),
inference(step,[status(thm)],[t208617,t18]) ).
cnf(t208619,plain,
meet(sk1,X1) = composition(meet(sk1,X1),meet(sk1,X1)),
inference(step,[status(thm)],[t208618,t14740]) ).
cnf(t106271,plain,
composition(meet(sk1,X1),meet(sk1,X1)) = meet(sk1,X1),
inference(orient,[status(thm)],[t208619]) ).
cnf(t210213,plain,
meet(sk1,sk0) = join(composition(sk1,composition(sk0,one)),composition(meet(sk1,converse(composition(sk0,one))),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t210212,t106271]) ).
cnf(t210214,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,converse(composition(sk0,one))),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t210213,t18]) ).
cnf(t210215,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,composition(converse(one),sk0)),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t210214,t69344]) ).
cnf(t210216,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,composition(one,sk0)),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t210215,t215]) ).
cnf(t210217,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,sk0),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t210216,t226]) ).
cnf(t210218,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,sk0),meet(converse(sk1),composition(sk0,one)))),
inference(step,[status(thm)],[t210217,t109]) ).
cnf(t210219,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,sk0),meet(sk1,composition(sk0,one)))),
inference(step,[status(thm)],[t210218,t72693]) ).
cnf(t210220,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,sk0),meet(sk1,sk0))),
inference(step,[status(thm)],[t210219,t18]) ).
cnf(t210221,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),meet(sk1,sk0)),
inference(step,[status(thm)],[t210220,t106271]) ).
cnf(t210222,plain,
meet(sk1,sk0) = join(meet(sk1,sk0),composition(sk1,sk0)),
inference(step,[status(thm)],[t210221,t44]) ).
cnf(t205605,plain,
join(meet(sk1,sk0),composition(sk1,sk0)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t210222]) ).
cnf(t205607,plain,
composition(composition(sk1,sk0),sk0) = meet(meet(sk1,sk0),composition(composition(sk1,sk0),sk0)),
inference(cp,[status(thm)],[t105399,t205605]) ).
cnf(t210223,plain,
composition(sk1,composition(sk0,sk0)) = meet(meet(sk1,sk0),composition(composition(sk1,sk0),sk0)),
inference(step,[status(thm)],[t205607,t23]) ).
cnf(t14556,plain,
composition(meet(one,converse(sk0)),meet(one,composition(converse(one),converse(sk0)))) = join(converse(sk0),composition(meet(one,converse(sk0)),meet(one,composition(converse(one),converse(sk0))))),
inference(cp,[status(thm)],[t3225,t14545]) ).
cnf(t206972,plain,
composition(converse(sk0),meet(one,composition(converse(one),converse(sk0)))) = join(converse(sk0),composition(meet(one,converse(sk0)),meet(one,composition(converse(one),converse(sk0))))),
inference(step,[status(thm)],[t14556,t14545]) ).
cnf(t206973,plain,
composition(converse(sk0),meet(one,converse(composition(sk0,one)))) = join(converse(sk0),composition(meet(one,converse(sk0)),meet(one,composition(converse(one),converse(sk0))))),
inference(step,[status(thm)],[t206972,t28]) ).
cnf(t206974,plain,
composition(converse(sk0),meet(one,converse(sk0))) = join(converse(sk0),composition(meet(one,converse(sk0)),meet(one,composition(converse(one),converse(sk0))))),
inference(step,[status(thm)],[t206973,t18]) ).
cnf(t206975,plain,
composition(converse(sk0),converse(sk0)) = join(converse(sk0),composition(meet(one,converse(sk0)),meet(one,composition(converse(one),converse(sk0))))),
inference(step,[status(thm)],[t206974,t14545]) ).
cnf(t206976,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),composition(meet(one,converse(sk0)),meet(one,composition(converse(one),converse(sk0))))),
inference(step,[status(thm)],[t206975,t28]) ).
cnf(t206977,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),composition(converse(sk0),meet(one,composition(converse(one),converse(sk0))))),
inference(step,[status(thm)],[t206976,t14545]) ).
cnf(t206978,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),composition(converse(sk0),meet(one,converse(composition(sk0,one))))),
inference(step,[status(thm)],[t206977,t28]) ).
cnf(t206979,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),composition(converse(sk0),meet(one,converse(sk0)))),
inference(step,[status(thm)],[t206978,t18]) ).
cnf(t206980,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),composition(converse(sk0),converse(sk0))),
inference(step,[status(thm)],[t206979,t14545]) ).
cnf(t206981,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),converse(composition(sk0,sk0))),
inference(step,[status(thm)],[t206980,t28]) ).
cnf(t206982,plain,
converse(composition(sk0,sk0)) = converse(join(sk0,composition(sk0,sk0))),
inference(step,[status(thm)],[t206981,t61]) ).
cnf(t16827,plain,
converse(join(sk0,composition(sk0,sk0))) = converse(composition(sk0,sk0)),
inference(orient,[status(thm)],[t206982]) ).
cnf(t16828,plain,
join(sk0,composition(sk0,sk0)) = converse(converse(composition(sk0,sk0))),
inference(cp,[status(thm)],[t22,t16827]) ).
cnf(t206983,plain,
join(sk0,composition(sk0,sk0)) = composition(sk0,sk0),
inference(step,[status(thm)],[t16828,t22]) ).
cnf(t16888,plain,
join(sk0,composition(sk0,sk0)) = composition(sk0,sk0),
inference(orient,[status(thm)],[t206983]) ).
cnf(t208322,plain,
sk0 = composition(sk0,sk0),
inference(step,[status(thm)],[t16888,t87044]) ).
cnf(t87141,plain,
sk0 = composition(sk0,sk0),
inference(rw,[status(thm)],[t208322]) ).
cnf(t87142,plain,
composition(sk0,sk0) = sk0,
inference(orient,[status(thm)],[t87141]) ).
cnf(t210224,plain,
composition(sk1,sk0) = meet(meet(sk1,sk0),composition(composition(sk1,sk0),sk0)),
inference(step,[status(thm)],[t210223,t87142]) ).
cnf(t210225,plain,
composition(sk1,sk0) = meet(meet(sk1,sk0),composition(sk1,composition(sk0,sk0))),
inference(step,[status(thm)],[t210224,t23]) ).
cnf(t210226,plain,
composition(sk1,sk0) = meet(meet(sk1,sk0),composition(sk1,sk0)),
inference(step,[status(thm)],[t210225,t87142]) ).
cnf(t205661,plain,
meet(meet(sk1,sk0),composition(sk1,sk0)) = composition(sk1,sk0),
inference(orient,[status(thm)],[t210226]) ).
cnf(t205743,plain,
meet(meet(sk1,sk0),composition(sk1,sk0)) = composition(meet(one,composition(composition(sk1,sk0),converse(meet(sk1,sk0)))),composition(sk1,sk0)),
inference(cp,[status(thm)],[t91799,t205661]) ).
cnf(t210227,plain,
composition(sk1,sk0) = composition(meet(one,composition(composition(sk1,sk0),converse(meet(sk1,sk0)))),composition(sk1,sk0)),
inference(step,[status(thm)],[t205743,t205661]) ).
cnf(t210228,plain,
composition(sk1,sk0) = composition(meet(one,composition(sk1,composition(sk0,converse(meet(sk1,sk0))))),composition(sk1,sk0)),
inference(step,[status(thm)],[t210227,t23]) ).
cnf(t36775,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(cp,[status(thm)],[t36738,t22]) ).
cnf(t36985,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(orient,[status(thm)],[t36775]) ).
cnf(t72696,plain,
converse(meet(sk1,X1)) = meet(sk1,converse(X1)),
inference(cp,[status(thm)],[t36985,t72693]) ).
cnf(t72909,plain,
converse(meet(sk1,X1)) = meet(sk1,converse(X1)),
inference(orient,[status(thm)],[t72696]) ).
cnf(t210229,plain,
composition(sk1,sk0) = composition(meet(one,composition(sk1,composition(sk0,meet(sk1,converse(sk0))))),composition(sk1,sk0)),
inference(step,[status(thm)],[t210228,t72909]) ).
cnf(t210230,plain,
composition(sk1,sk0) = composition(meet(one,composition(sk1,composition(sk0,meet(sk1,sk0)))),composition(sk1,sk0)),
inference(step,[status(thm)],[t210229,t68503]) ).
cnf(t110,plain,
composition(meet(X1,composition(X2,converse(X3))),meet(X3,composition(converse(X1),X2))) = join(meet(X2,composition(X1,X3)),composition(meet(X1,composition(X2,converse(X3))),meet(X3,composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t34,t109]) ).
cnf(t31813,plain,
join(meet(X1,composition(X2,X3)),composition(meet(X2,composition(X1,converse(X3))),meet(X3,composition(converse(X2),X1)))) = composition(meet(X2,composition(X1,converse(X3))),meet(X3,composition(converse(X2),X1))),
inference(orient,[status(thm)],[t110]) ).
cnf(t26975,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t26949,t14278]) ).
cnf(t29926,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t26975]) ).
cnf(t30194,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t13215,t29926]) ).
cnf(t207184,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t30194,t12362]) ).
cnf(t207185,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t207184,t88]) ).
cnf(t30220,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t207185]) ).
cnf(t30264,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t30220,t44]) ).
cnf(t30301,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t30264]) ).
cnf(t30348,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X1,X2)),
inference(cp,[status(thm)],[t30301,t12362]) ).
cnf(t31544,plain,
meet(complement(X1),join(X1,X2)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t30348]) ).
cnf(t51,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t47,t44]) ).
cnf(t206986,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t51,t47]) ).
cnf(t17003,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t206986]) ).
cnf(t87138,plain,
join(X1,join(X2,composition(sk0,X1))) = join(X2,X1),
inference(cp,[status(thm)],[t17003,t87044]) ).
cnf(t101482,plain,
join(X1,join(X2,composition(sk0,X1))) = join(X2,X1),
inference(orient,[status(thm)],[t87138]) ).
cnf(t87,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t47,t86]) ).
cnf(t126,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t87]) ).
cnf(t128,plain,
join(one,X1) = join(sk1,join(X1,one)),
inference(cp,[status(thm)],[t126,t44]) ).
cnf(t161,plain,
join(sk1,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t128]) ).
cnf(t392,plain,
join(top,one) = join(one,complement(sk1)),
inference(cp,[status(thm)],[t389,t161]) ).
cnf(t422,plain,
join(one,complement(sk1)) = join(top,one),
inference(orient,[status(thm)],[t392]) ).
cnf(t206023,plain,
join(one,complement(sk1)) = top,
inference(step,[status(thm)],[t422,t443]) ).
cnf(t446,plain,
join(one,complement(sk1)) = top,
inference(orient,[status(thm)],[t206023]) ).
cnf(t83287,plain,
join(X1,composition(complement(sk1),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t83099,t446]) ).
cnf(t83559,plain,
join(X1,composition(complement(sk1),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t83287]) ).
cnf(t83623,plain,
join(X1,converse(composition(complement(sk1),converse(X1)))) = converse(composition(top,converse(X1))),
inference(cp,[status(thm)],[t324,t83559]) ).
cnf(t72698,plain,
converse(complement(sk1)) = complement(sk1),
inference(cp,[status(thm)],[t35072,t72693]) ).
cnf(t72812,plain,
converse(complement(sk1)) = complement(sk1),
inference(orient,[status(thm)],[t72698]) ).
cnf(t72818,plain,
converse(composition(complement(sk1),X1)) = composition(converse(X1),complement(sk1)),
inference(cp,[status(thm)],[t28,t72812]) ).
cnf(t76388,plain,
converse(composition(complement(sk1),X1)) = composition(converse(X1),complement(sk1)),
inference(orient,[status(thm)],[t72818]) ).
cnf(t208200,plain,
join(X1,composition(converse(converse(X1)),complement(sk1))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t83623,t76388]) ).
cnf(t208201,plain,
join(X1,composition(X1,complement(sk1))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t208200,t22]) ).
cnf(t459,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t28,t453]) ).
cnf(t479,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t459]) ).
cnf(t208202,plain,
join(X1,composition(X1,complement(sk1))) = composition(converse(converse(X1)),top),
inference(step,[status(thm)],[t208201,t479]) ).
cnf(t208203,plain,
join(X1,composition(X1,complement(sk1))) = composition(X1,top),
inference(step,[status(thm)],[t208202,t22]) ).
cnf(t84054,plain,
join(X1,composition(X1,complement(sk1))) = composition(X1,top),
inference(orient,[status(thm)],[t208203]) ).
cnf(t101528,plain,
join(sk0,complement(sk1)) = join(complement(sk1),composition(sk0,top)),
inference(cp,[status(thm)],[t101482,t84054]) ).
cnf(t101814,plain,
join(complement(sk1),composition(sk0,top)) = join(sk0,complement(sk1)),
inference(orient,[status(thm)],[t101528]) ).
cnf(t101820,plain,
meet(complement(complement(sk1)),composition(sk0,top)) = meet(complement(complement(sk1)),join(sk0,complement(sk1))),
inference(cp,[status(thm)],[t31544,t101814]) ).
cnf(t208558,plain,
meet(composition(sk0,top),complement(complement(sk1))) = meet(complement(complement(sk1)),join(sk0,complement(sk1))),
inference(step,[status(thm)],[t101820,t109]) ).
cnf(t208559,plain,
meet(composition(sk0,top),sk1) = meet(complement(complement(sk1)),join(sk0,complement(sk1))),
inference(step,[status(thm)],[t208558,t12362]) ).
cnf(t208560,plain,
meet(sk1,composition(sk0,top)) = meet(complement(complement(sk1)),join(sk0,complement(sk1))),
inference(step,[status(thm)],[t208559,t109]) ).
cnf(t30193,plain,
meet(complement(X1),join(X2,X1)) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t14125,t29926]) ).
cnf(t207204,plain,
meet(complement(X1),join(X2,X1)) = meet(complement(X1),X2),
inference(step,[status(thm)],[t30193,t14125]) ).
cnf(t31267,plain,
meet(complement(X1),join(X2,X1)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t207204]) ).
cnf(t208561,plain,
meet(sk1,composition(sk0,top)) = meet(complement(complement(sk1)),sk0),
inference(step,[status(thm)],[t208560,t31267]) ).
cnf(t208562,plain,
meet(sk1,composition(sk0,top)) = meet(sk0,complement(complement(sk1))),
inference(step,[status(thm)],[t208561,t109]) ).
cnf(t208563,plain,
meet(sk1,composition(sk0,top)) = meet(sk0,sk1),
inference(step,[status(thm)],[t208562,t12362]) ).
cnf(t208564,plain,
meet(sk1,composition(sk0,top)) = meet(sk1,sk0),
inference(step,[status(thm)],[t208563,t109]) ).
cnf(t101861,plain,
meet(sk1,composition(sk0,top)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t208564]) ).
cnf(t101862,plain,
meet(sk1,converse(composition(sk0,top))) = converse(meet(sk1,sk0)),
inference(cp,[status(thm)],[t72909,t101861]) ).
cnf(t208565,plain,
meet(sk1,composition(converse(top),sk0)) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t101862,t69344]) ).
cnf(t208566,plain,
meet(sk1,composition(top,sk0)) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t208565,t453]) ).
cnf(t208567,plain,
meet(sk1,composition(top,sk0)) = meet(sk1,converse(sk0)),
inference(step,[status(thm)],[t208566,t72909]) ).
cnf(t208568,plain,
meet(sk1,composition(top,sk0)) = meet(sk1,sk0),
inference(step,[status(thm)],[t208567,t68503]) ).
cnf(t101918,plain,
meet(sk1,composition(top,sk0)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t208568]) ).
cnf(t101970,plain,
composition(meet(top,composition(sk1,converse(sk0))),meet(sk0,composition(converse(top),sk1))) = join(meet(sk1,sk0),composition(meet(top,composition(sk1,converse(sk0))),meet(sk0,composition(converse(top),sk1)))),
inference(cp,[status(thm)],[t31813,t101918]) ).
cnf(t208643,plain,
composition(composition(sk1,converse(sk0)),meet(sk0,composition(converse(top),sk1))) = join(meet(sk1,sk0),composition(meet(top,composition(sk1,converse(sk0))),meet(sk0,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t101970,t12361]) ).
cnf(t208644,plain,
composition(sk1,composition(converse(sk0),meet(sk0,composition(converse(top),sk1)))) = join(meet(sk1,sk0),composition(meet(top,composition(sk1,converse(sk0))),meet(sk0,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t208643,t23]) ).
cnf(t208645,plain,
composition(sk1,composition(sk0,meet(sk0,composition(converse(top),sk1)))) = join(meet(sk1,sk0),composition(meet(top,composition(sk1,converse(sk0))),meet(sk0,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t208644,t68503]) ).
cnf(t208646,plain,
composition(sk1,composition(sk0,meet(sk0,composition(top,sk1)))) = join(meet(sk1,sk0),composition(meet(top,composition(sk1,converse(sk0))),meet(sk0,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t208645,t453]) ).
cnf(t68506,plain,
converse(meet(sk0,X1)) = meet(sk0,converse(X1)),
inference(cp,[status(thm)],[t36985,t68503]) ).
cnf(t68704,plain,
converse(meet(sk0,X1)) = meet(sk0,converse(X1)),
inference(orient,[status(thm)],[t68506]) ).
cnf(t83261,plain,
join(X1,composition(meet(sk1,X2),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t83099,t12792]) ).
cnf(t208236,plain,
join(X1,composition(meet(sk1,X2),X1)) = X1,
inference(step,[status(thm)],[t83261,t226]) ).
cnf(t84841,plain,
join(X1,composition(meet(sk1,X2),X1)) = X1,
inference(orient,[status(thm)],[t208236]) ).
cnf(t65073,plain,
zero = meet(composition(complement(one),sk1),sk1),
inference(cp,[status(thm)],[t65068,t14608]) ).
cnf(t207956,plain,
zero = meet(sk1,composition(complement(one),sk1)),
inference(step,[status(thm)],[t65073,t109]) ).
cnf(t65106,plain,
meet(sk1,composition(complement(one),sk1)) = zero,
inference(orient,[status(thm)],[t207956]) ).
cnf(t65111,plain,
sk1 = join(zero,meet(complement(composition(complement(one),sk1)),sk1)),
inference(cp,[status(thm)],[t51849,t65106]) ).
cnf(t207976,plain,
sk1 = meet(complement(composition(complement(one),sk1)),sk1),
inference(step,[status(thm)],[t65111,t12235]) ).
cnf(t207977,plain,
sk1 = meet(sk1,complement(composition(complement(one),sk1))),
inference(step,[status(thm)],[t207976,t109]) ).
cnf(t65372,plain,
meet(sk1,complement(composition(complement(one),sk1))) = sk1,
inference(orient,[status(thm)],[t207977]) ).
cnf(t84843,plain,
X1 = join(X1,composition(sk1,X1)),
inference(cp,[status(thm)],[t84841,t65372]) ).
cnf(t84977,plain,
join(X1,composition(sk1,X1)) = X1,
inference(orient,[status(thm)],[t84843]) ).
cnf(t85073,plain,
join(X1,join(X2,composition(sk1,X1))) = join(X2,X1),
inference(cp,[status(thm)],[t17003,t84977]) ).
cnf(t97075,plain,
join(X1,join(X2,composition(sk1,X1))) = join(X2,X1),
inference(orient,[status(thm)],[t85073]) ).
cnf(t206025,plain,
join(one,complement(sk0)) = top,
inference(step,[status(thm)],[t427,t443]) ).
cnf(t448,plain,
join(one,complement(sk0)) = top,
inference(orient,[status(thm)],[t206025]) ).
cnf(t83288,plain,
join(X1,composition(complement(sk0),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t83099,t448]) ).
cnf(t83698,plain,
join(X1,composition(complement(sk0),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t83288]) ).
cnf(t83762,plain,
join(X1,converse(composition(complement(sk0),converse(X1)))) = converse(composition(top,converse(X1))),
inference(cp,[status(thm)],[t324,t83698]) ).
cnf(t68508,plain,
converse(complement(sk0)) = complement(sk0),
inference(cp,[status(thm)],[t35072,t68503]) ).
cnf(t68613,plain,
converse(complement(sk0)) = complement(sk0),
inference(orient,[status(thm)],[t68508]) ).
cnf(t68619,plain,
converse(composition(complement(sk0),X1)) = composition(converse(X1),complement(sk0)),
inference(cp,[status(thm)],[t28,t68613]) ).
cnf(t71300,plain,
converse(composition(complement(sk0),X1)) = composition(converse(X1),complement(sk0)),
inference(orient,[status(thm)],[t68619]) ).
cnf(t208212,plain,
join(X1,composition(converse(converse(X1)),complement(sk0))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t83762,t71300]) ).
cnf(t208213,plain,
join(X1,composition(X1,complement(sk0))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t208212,t22]) ).
cnf(t208214,plain,
join(X1,composition(X1,complement(sk0))) = composition(converse(converse(X1)),top),
inference(step,[status(thm)],[t208213,t479]) ).
cnf(t208215,plain,
join(X1,composition(X1,complement(sk0))) = composition(X1,top),
inference(step,[status(thm)],[t208214,t22]) ).
cnf(t84204,plain,
join(X1,composition(X1,complement(sk0))) = composition(X1,top),
inference(orient,[status(thm)],[t208215]) ).
cnf(t97118,plain,
join(sk1,complement(sk0)) = join(complement(sk0),composition(sk1,top)),
inference(cp,[status(thm)],[t97075,t84204]) ).
cnf(t97728,plain,
join(complement(sk0),composition(sk1,top)) = join(sk1,complement(sk0)),
inference(orient,[status(thm)],[t97118]) ).
cnf(t97730,plain,
meet(complement(complement(sk0)),composition(sk1,top)) = meet(complement(complement(sk0)),join(sk1,complement(sk0))),
inference(cp,[status(thm)],[t31544,t97728]) ).
cnf(t208517,plain,
meet(composition(sk1,top),complement(complement(sk0))) = meet(complement(complement(sk0)),join(sk1,complement(sk0))),
inference(step,[status(thm)],[t97730,t109]) ).
cnf(t208518,plain,
meet(composition(sk1,top),sk0) = meet(complement(complement(sk0)),join(sk1,complement(sk0))),
inference(step,[status(thm)],[t208517,t12362]) ).
cnf(t208519,plain,
meet(sk0,composition(sk1,top)) = meet(complement(complement(sk0)),join(sk1,complement(sk0))),
inference(step,[status(thm)],[t208518,t109]) ).
cnf(t208520,plain,
meet(sk0,composition(sk1,top)) = meet(complement(complement(sk0)),sk1),
inference(step,[status(thm)],[t208519,t31267]) ).
cnf(t208521,plain,
meet(sk0,composition(sk1,top)) = meet(sk1,complement(complement(sk0))),
inference(step,[status(thm)],[t208520,t109]) ).
cnf(t208522,plain,
meet(sk0,composition(sk1,top)) = meet(sk1,sk0),
inference(step,[status(thm)],[t208521,t12362]) ).
cnf(t97771,plain,
meet(sk0,composition(sk1,top)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t208522]) ).
cnf(t97772,plain,
meet(sk0,converse(composition(sk1,top))) = converse(meet(sk1,sk0)),
inference(cp,[status(thm)],[t68704,t97771]) ).
cnf(t72702,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sk1),
inference(cp,[status(thm)],[t28,t72693]) ).
cnf(t73582,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sk1),
inference(orient,[status(thm)],[t72702]) ).
cnf(t208523,plain,
meet(sk0,composition(converse(top),sk1)) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t97772,t73582]) ).
cnf(t208524,plain,
meet(sk0,composition(top,sk1)) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t208523,t453]) ).
cnf(t208525,plain,
meet(sk0,composition(top,sk1)) = meet(sk1,converse(sk0)),
inference(step,[status(thm)],[t208524,t72909]) ).
cnf(t208526,plain,
meet(sk0,composition(top,sk1)) = meet(sk1,sk0),
inference(step,[status(thm)],[t208525,t68503]) ).
cnf(t97828,plain,
meet(sk0,composition(top,sk1)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t208526]) ).
cnf(t208647,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = join(meet(sk1,sk0),composition(meet(top,composition(sk1,converse(sk0))),meet(sk0,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t208646,t97828]) ).
cnf(t208648,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = join(meet(sk1,sk0),composition(composition(sk1,converse(sk0)),meet(sk0,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t208647,t12361]) ).
cnf(t208649,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = join(meet(sk1,sk0),composition(sk1,composition(converse(sk0),meet(sk0,composition(converse(top),sk1))))),
inference(step,[status(thm)],[t208648,t23]) ).
cnf(t208650,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = join(meet(sk1,sk0),composition(sk1,composition(sk0,meet(sk0,composition(converse(top),sk1))))),
inference(step,[status(thm)],[t208649,t68503]) ).
cnf(t208651,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = join(meet(sk1,sk0),composition(sk1,composition(sk0,meet(sk0,composition(top,sk1))))),
inference(step,[status(thm)],[t208650,t453]) ).
cnf(t208652,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = join(meet(sk1,sk0),composition(sk1,composition(sk0,meet(sk1,sk0)))),
inference(step,[status(thm)],[t208651,t97828]) ).
cnf(t208653,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = meet(sk1,sk0),
inference(step,[status(thm)],[t208652,t84427]) ).
cnf(t106771,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = meet(sk1,sk0),
inference(orient,[status(thm)],[t208653]) ).
cnf(t210231,plain,
composition(sk1,sk0) = composition(meet(one,meet(sk1,sk0)),composition(sk1,sk0)),
inference(step,[status(thm)],[t210230,t106771]) ).
cnf(t210232,plain,
composition(sk1,sk0) = composition(meet(sk1,sk0),composition(sk1,sk0)),
inference(step,[status(thm)],[t210231,t14740]) ).
cnf(t205753,plain,
composition(meet(sk1,sk0),composition(sk1,sk0)) = composition(sk1,sk0),
inference(orient,[status(thm)],[t210232]) ).
cnf(t205762,plain,
composition(sk0,converse(composition(meet(sk1,sk0),sk1))) = converse(composition(sk1,sk0)),
inference(cp,[status(thm)],[t154245,t205753]) ).
cnf(t72701,plain,
converse(composition(X1,sk1)) = composition(sk1,converse(X1)),
inference(cp,[status(thm)],[t28,t72693]) ).
cnf(t73471,plain,
converse(composition(X1,sk1)) = composition(sk1,converse(X1)),
inference(orient,[status(thm)],[t72701]) ).
cnf(t210233,plain,
composition(sk0,composition(sk1,converse(meet(sk1,sk0)))) = converse(composition(sk1,sk0)),
inference(step,[status(thm)],[t205762,t73471]) ).
cnf(t210234,plain,
composition(sk0,composition(sk1,meet(sk1,converse(sk0)))) = converse(composition(sk1,sk0)),
inference(step,[status(thm)],[t210233,t72909]) ).
cnf(t210235,plain,
composition(sk0,composition(sk1,meet(sk1,sk0))) = converse(composition(sk1,sk0)),
inference(step,[status(thm)],[t210234,t68503]) ).
cnf(t14543,plain,
composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1)))) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(cp,[status(thm)],[t3225,t14532]) ).
cnf(t206954,plain,
composition(converse(sk1),meet(one,composition(converse(one),converse(sk1)))) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t14543,t14532]) ).
cnf(t206955,plain,
composition(converse(sk1),meet(one,converse(composition(sk1,one)))) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t206954,t28]) ).
cnf(t206956,plain,
composition(converse(sk1),meet(one,converse(sk1))) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t206955,t18]) ).
cnf(t206957,plain,
composition(converse(sk1),converse(sk1)) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t206956,t14532]) ).
cnf(t206958,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t206957,t28]) ).
cnf(t206959,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t206958,t14532]) ).
cnf(t206960,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),meet(one,converse(composition(sk1,one))))),
inference(step,[status(thm)],[t206959,t28]) ).
cnf(t206961,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t206960,t18]) ).
cnf(t206962,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),converse(sk1))),
inference(step,[status(thm)],[t206961,t14532]) ).
cnf(t206963,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),converse(composition(sk1,sk1))),
inference(step,[status(thm)],[t206962,t28]) ).
cnf(t206964,plain,
converse(composition(sk1,sk1)) = converse(join(sk1,composition(sk1,sk1))),
inference(step,[status(thm)],[t206963,t61]) ).
cnf(t16472,plain,
converse(join(sk1,composition(sk1,sk1))) = converse(composition(sk1,sk1)),
inference(orient,[status(thm)],[t206964]) ).
cnf(t16473,plain,
join(sk1,composition(sk1,sk1)) = converse(converse(composition(sk1,sk1))),
inference(cp,[status(thm)],[t22,t16472]) ).
cnf(t206965,plain,
join(sk1,composition(sk1,sk1)) = composition(sk1,sk1),
inference(step,[status(thm)],[t16473,t22]) ).
cnf(t16533,plain,
join(sk1,composition(sk1,sk1)) = composition(sk1,sk1),
inference(orient,[status(thm)],[t206965]) ).
cnf(t208237,plain,
sk1 = composition(sk1,sk1),
inference(step,[status(thm)],[t16533,t84977]) ).
cnf(t85076,plain,
sk1 = composition(sk1,sk1),
inference(rw,[status(thm)],[t208237]) ).
cnf(t85077,plain,
composition(sk1,sk1) = sk1,
inference(orient,[status(thm)],[t85076]) ).
cnf(t85083,plain,
composition(sk1,composition(sk1,X1)) = composition(sk1,X1),
inference(cp,[status(thm)],[t23,t85077]) ).
cnf(t85559,plain,
composition(sk1,composition(sk1,X1)) = composition(sk1,X1),
inference(orient,[status(thm)],[t85083]) ).
cnf(t106781,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = composition(sk1,meet(sk1,sk0)),
inference(cp,[status(thm)],[t85559,t106771]) ).
cnf(t208654,plain,
meet(sk1,sk0) = composition(sk1,meet(sk1,sk0)),
inference(step,[status(thm)],[t106781,t106771]) ).
cnf(t106840,plain,
composition(sk1,meet(sk1,sk0)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t208654]) ).
cnf(t210236,plain,
composition(sk0,meet(sk1,sk0)) = converse(composition(sk1,sk0)),
inference(step,[status(thm)],[t210235,t106840]) ).
cnf(t210237,plain,
composition(sk0,meet(sk1,sk0)) = composition(converse(sk0),sk1),
inference(step,[status(thm)],[t210236,t73582]) ).
cnf(t210238,plain,
composition(sk0,meet(sk1,sk0)) = composition(sk0,sk1),
inference(step,[status(thm)],[t210237,t68503]) ).
cnf(t205828,plain,
composition(sk0,meet(sk1,sk0)) = composition(sk0,sk1),
inference(orient,[status(thm)],[t210238]) ).
cnf(t205840,plain,
composition(sk0,meet(sk1,sk0)) = meet(meet(sk1,sk0),composition(sk0,sk1)),
inference(cp,[status(thm)],[t87295,t205828]) ).
cnf(t210240,plain,
composition(sk0,sk1) = meet(meet(sk1,sk0),composition(sk0,sk1)),
inference(step,[status(thm)],[t205840,t205828]) ).
cnf(t18002,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t15862,t17925]) ).
cnf(t21240,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t18002]) ).
cnf(t85062,plain,
join(X1,converse(composition(sk1,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t324,t84977]) ).
cnf(t208264,plain,
join(X1,composition(converse(converse(X1)),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t85062,t73582]) ).
cnf(t208265,plain,
join(X1,composition(X1,sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t208264,t22]) ).
cnf(t208266,plain,
join(X1,composition(X1,sk1)) = X1,
inference(step,[status(thm)],[t208265,t22]) ).
cnf(t85178,plain,
join(X1,composition(X1,sk1)) = X1,
inference(orient,[status(thm)],[t208266]) ).
cnf(t85205,plain,
composition(X1,sk1) = meet(composition(X1,sk1),X1),
inference(cp,[status(thm)],[t14459,t85178]) ).
cnf(t208271,plain,
composition(X1,sk1) = meet(X1,composition(X1,sk1)),
inference(step,[status(thm)],[t85205,t109]) ).
cnf(t85606,plain,
meet(X1,composition(X1,sk1)) = composition(X1,sk1),
inference(orient,[status(thm)],[t208271]) ).
cnf(t85632,plain,
meet(X1,composition(X1,sk1)) = meet(composition(X1,sk1),join(X1,X2)),
inference(cp,[status(thm)],[t21240,t85606]) ).
cnf(t208547,plain,
composition(X1,sk1) = meet(composition(X1,sk1),join(X1,X2)),
inference(step,[status(thm)],[t85632,t85606]) ).
cnf(t100562,plain,
meet(composition(X1,sk1),join(X1,X2)) = composition(X1,sk1),
inference(orient,[status(thm)],[t208547]) ).
cnf(t83263,plain,
join(X1,composition(meet(X2,sk0),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t83099,t12768]) ).
cnf(t208364,plain,
join(X1,composition(meet(X2,sk0),X1)) = X1,
inference(step,[status(thm)],[t83263,t226]) ).
cnf(t88243,plain,
join(X1,composition(meet(X2,sk0),X1)) = X1,
inference(orient,[status(thm)],[t208364]) ).
cnf(t101913,plain,
composition(meet(sk0,composition(sk1,converse(top))),meet(top,composition(converse(sk0),sk1))) = join(meet(sk1,sk0),composition(meet(sk0,composition(sk1,converse(top))),meet(top,composition(converse(sk0),sk1)))),
inference(cp,[status(thm)],[t31813,t101861]) ).
cnf(t208634,plain,
composition(meet(sk0,composition(sk1,top)),meet(top,composition(converse(sk0),sk1))) = join(meet(sk1,sk0),composition(meet(sk0,composition(sk1,converse(top))),meet(top,composition(converse(sk0),sk1)))),
inference(step,[status(thm)],[t101913,t453]) ).
cnf(t208635,plain,
composition(meet(sk1,sk0),meet(top,composition(converse(sk0),sk1))) = join(meet(sk1,sk0),composition(meet(sk0,composition(sk1,converse(top))),meet(top,composition(converse(sk0),sk1)))),
inference(step,[status(thm)],[t208634,t97771]) ).
cnf(t208636,plain,
composition(meet(sk1,sk0),composition(converse(sk0),sk1)) = join(meet(sk1,sk0),composition(meet(sk0,composition(sk1,converse(top))),meet(top,composition(converse(sk0),sk1)))),
inference(step,[status(thm)],[t208635,t12361]) ).
cnf(t208637,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = join(meet(sk1,sk0),composition(meet(sk0,composition(sk1,converse(top))),meet(top,composition(converse(sk0),sk1)))),
inference(step,[status(thm)],[t208636,t68503]) ).
cnf(t208638,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = join(meet(sk1,sk0),composition(meet(sk0,composition(sk1,top)),meet(top,composition(converse(sk0),sk1)))),
inference(step,[status(thm)],[t208637,t453]) ).
cnf(t208639,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = join(meet(sk1,sk0),composition(meet(sk1,sk0),meet(top,composition(converse(sk0),sk1)))),
inference(step,[status(thm)],[t208638,t97771]) ).
cnf(t208640,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = join(meet(sk1,sk0),composition(meet(sk1,sk0),composition(converse(sk0),sk1))),
inference(step,[status(thm)],[t208639,t12361]) ).
cnf(t208641,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = join(meet(sk1,sk0),composition(meet(sk1,sk0),composition(sk0,sk1))),
inference(step,[status(thm)],[t208640,t68503]) ).
cnf(t84516,plain,
join(X1,converse(composition(sk1,composition(sk0,converse(X1))))) = converse(converse(X1)),
inference(cp,[status(thm)],[t324,t84427]) ).
cnf(t208368,plain,
join(X1,composition(converse(composition(sk0,converse(X1))),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t84516,t73582]) ).
cnf(t208369,plain,
join(X1,composition(composition(converse(converse(X1)),sk0),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t208368,t69344]) ).
cnf(t208370,plain,
join(X1,composition(converse(converse(X1)),composition(sk0,sk1))) = converse(converse(X1)),
inference(step,[status(thm)],[t208369,t23]) ).
cnf(t208371,plain,
join(X1,composition(X1,composition(sk0,sk1))) = converse(converse(X1)),
inference(step,[status(thm)],[t208370,t22]) ).
cnf(t208372,plain,
join(X1,composition(X1,composition(sk0,sk1))) = X1,
inference(step,[status(thm)],[t208371,t22]) ).
cnf(t88807,plain,
join(X1,composition(X1,composition(sk0,sk1))) = X1,
inference(orient,[status(thm)],[t208372]) ).
cnf(t208642,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = meet(sk1,sk0),
inference(step,[status(thm)],[t208641,t88807]) ).
cnf(t106712,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t208642]) ).
cnf(t106721,plain,
composition(sk0,sk1) = join(composition(sk0,sk1),meet(sk1,sk0)),
inference(cp,[status(thm)],[t88243,t106712]) ).
cnf(t208661,plain,
composition(sk0,sk1) = join(meet(sk1,sk0),composition(sk0,sk1)),
inference(step,[status(thm)],[t106721,t44]) ).
cnf(t107853,plain,
join(meet(sk1,sk0),composition(sk0,sk1)) = composition(sk0,sk1),
inference(orient,[status(thm)],[t208661]) ).
cnf(t107859,plain,
composition(meet(sk1,sk0),sk1) = meet(composition(meet(sk1,sk0),sk1),composition(sk0,sk1)),
inference(cp,[status(thm)],[t100562,t107853]) ).
cnf(t106846,plain,
composition(converse(meet(sk1,sk0)),sk1) = converse(meet(sk1,sk0)),
inference(cp,[status(thm)],[t73582,t106840]) ).
cnf(t208655,plain,
composition(meet(sk1,converse(sk0)),sk1) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t106846,t72909]) ).
cnf(t208656,plain,
composition(meet(sk1,sk0),sk1) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t208655,t68503]) ).
cnf(t208657,plain,
composition(meet(sk1,sk0),sk1) = meet(sk1,converse(sk0)),
inference(step,[status(thm)],[t208656,t72909]) ).
cnf(t208658,plain,
composition(meet(sk1,sk0),sk1) = meet(sk1,sk0),
inference(step,[status(thm)],[t208657,t68503]) ).
cnf(t106890,plain,
composition(meet(sk1,sk0),sk1) = meet(sk1,sk0),
inference(orient,[status(thm)],[t208658]) ).
cnf(t208662,plain,
meet(sk1,sk0) = meet(composition(meet(sk1,sk0),sk1),composition(sk0,sk1)),
inference(step,[status(thm)],[t107859,t106890]) ).
cnf(t208663,plain,
meet(sk1,sk0) = meet(composition(sk0,sk1),composition(meet(sk1,sk0),sk1)),
inference(step,[status(thm)],[t208662,t109]) ).
cnf(t208664,plain,
meet(sk1,sk0) = meet(composition(sk0,sk1),meet(sk1,sk0)),
inference(step,[status(thm)],[t208663,t106890]) ).
cnf(t208665,plain,
meet(sk1,sk0) = meet(meet(sk1,sk0),composition(sk0,sk1)),
inference(step,[status(thm)],[t208664,t109]) ).
cnf(t107901,plain,
meet(meet(sk1,sk0),composition(sk0,sk1)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t208665]) ).
cnf(t210241,plain,
composition(sk0,sk1) = meet(sk1,sk0),
inference(step,[status(thm)],[t210240,t107901]) ).
cnf(t205925,plain,
composition(sk0,sk1) = meet(sk1,sk0),
inference(orient,[status(thm)],[t210241]) ).
cnf(c18,plain,
composition(sk0,sk1) != meet(sk0,sk1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
meet(sk0,sk1) != composition(sk0,sk1),
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(g0_0,plain,
meet(sk1,sk0) != composition(sk0,sk1),
inference(rw,[status(thm)],[goal_0,t109]) ).
cnf(g0_1,plain,
meet(sk1,sk0) != meet(sk1,sk0),
inference(rw,[status(thm)],[g0_0,t205925]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL028+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.18/15.47 % Computer : n006.cluster.edu
% 0.18/15.47 % Model : x86_64 x86_64
% 0.18/15.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/15.47 % Memory : 8046.5625MB
% 0.18/15.47 % OS : Linux 6.8.0-71-generic
% 0.18/15.47 % CPULimit : 300
% 0.18/15.47 % WCLimit : 300
% 0.18/15.47 % DateTime : Thu Sep 24 07:23:13 UTC 2026
% 0.18/15.47 % CPUTime :
% 0.18/15.47 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 111.30/31.64 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 111.30/31.64 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------