%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL029+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.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:30 PM UTC 2026
% Result : Theorem 169.51s 25.01s
% Output : Proof 169.51s
% 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(t451205,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)],[t451205]) ).
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(t451202,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)],[t451202]) ).
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(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(t193,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t192,t18]) ).
cnf(t451211,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t193,t22]) ).
cnf(t205,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t451211]) ).
cnf(t206,plain,
one = converse(one),
inference(cp,[status(thm)],[t205,t18]) ).
cnf(t215,plain,
converse(one) = one,
inference(orient,[status(thm)],[t206]) ).
cnf(t451212,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t205,t215]) ).
cnf(t225,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t451212]) ).
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(t451216,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t229,t215]) ).
cnf(t451217,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t451216,t226]) ).
cnf(t263,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t451217]) ).
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(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]) ).
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(t451885,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t46,t44]) ).
cnf(t451886,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t451885,t88]) ).
cnf(t451887,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t451886,t44]) ).
cnf(t11678,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t451887]) ).
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(t11679,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t11678,t95]) ).
cnf(t451959,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)],[t451959]) ).
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(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]) ).
cnf(t451203,plain,
zero = complement(top),
inference(step,[status(thm)],[t89,t95]) ).
cnf(t100,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t451203]) ).
cnf(t267,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t263,t100]) ).
cnf(t451218,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t267,t100]) ).
cnf(t451219,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t451218,t100]) ).
cnf(t274,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t451219]) ).
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(t12223,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t308,t12218]) ).
cnf(t451961,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t12223,t12218]) ).
cnf(t12235,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t451961]) ).
cnf(t451966,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t12218,t12235]) ).
cnf(t12283,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t451966]) ).
cnf(t12327,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t12283]) ).
cnf(t451997,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)],[t451997]) ).
cnf(t13215,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t12358]) ).
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(t451274,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t264,t88]) ).
cnf(t451275,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t451274,t88]) ).
cnf(t672,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t451275]) ).
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(t12328,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t693,t12327]) ).
cnf(t452013,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t12328,t12327]) ).
cnf(t452014,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t452013,t12327]) ).
cnf(t12392,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t452014]) ).
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(t452016,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t12475,t11678]) ).
cnf(t452017,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t452016,t44]) ).
cnf(t12485,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t452017]) ).
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(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(t452041,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)],[t452041]) ).
cnf(t26189,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t13298]) ).
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(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(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(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]) ).
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(t451463,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(t451464,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)],[t451463,t18]) ).
cnf(t451465,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)],[t451464,t215]) ).
cnf(t451466,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)],[t451465,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)],[t451466]) ).
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(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(t451230,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t397,t52]) ).
cnf(t412,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t451230]) ).
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(t451233,plain,
top = join(X1,top),
inference(step,[status(thm)],[t395,t432]) ).
cnf(t437,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t451233]) ).
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(t451256,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)],[t451256]) ).
cnf(t4039,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t4033,t517]) ).
cnf(t451594,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)],[t451594]) ).
cnf(t4164,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t4117,t61]) ).
cnf(t451595,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t4164,t22]) ).
cnf(t451596,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t451595,t22]) ).
cnf(t4178,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t451596]) ).
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(t451352,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)],[t451352]) ).
cnf(t4255,plain,
top = join(complement(composition(top,zero)),complement(one)),
inference(cp,[status(thm)],[t4242,t1881]) ).
cnf(t451597,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)],[t451597]) ).
cnf(t4335,plain,
meet(one,composition(top,zero)) = complement(top),
inference(cp,[status(thm)],[t88,t4333]) ).
cnf(t451598,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)],[t451598]) ).
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(t451599,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(t451600,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)],[t451599,t215]) ).
cnf(t451601,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)],[t451600,t226]) ).
cnf(t451602,plain,
composition(zero,zero) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t451601,t4341]) ).
cnf(t451603,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t451602,t4341]) ).
cnf(t451604,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(one,composition(top,zero))))),
inference(step,[status(thm)],[t451603,t215]) ).
cnf(t451605,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(top,zero)))),
inference(step,[status(thm)],[t451604,t226]) ).
cnf(t451606,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t451605,t4341]) ).
cnf(t4349,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t451606]) ).
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(t451629,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)],[t451629]) ).
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(t451697,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t7185,t465]) ).
cnf(t451698,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t451697,t465]) ).
cnf(t451699,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t451698,t443]) ).
cnf(t451700,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t451699,t453]) ).
cnf(t7315,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t451700]) ).
cnf(t7331,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t7315,t215]) ).
cnf(t451701,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t7331,t18]) ).
cnf(t451702,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t451701,t437]) ).
cnf(t7344,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t451702]) ).
cnf(t7349,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t55,t7344]) ).
cnf(t451711,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t7349,t100]) ).
cnf(t451712,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t451711,t100]) ).
cnf(t451713,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t451712,t453]) ).
cnf(t451714,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t451713,t100]) ).
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(t451357,plain,
join(zero,join(X1,join(zero,X2))) = join(join(zero,X1),X2),
inference(step,[status(thm)],[t314,t47]) ).
cnf(t451358,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(step,[status(thm)],[t451357,t47]) ).
cnf(t2137,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(orient,[status(thm)],[t451358]) ).
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,X2] :
( ( join(X1,one) = one
& join(X0,one) = one )
=> meet(composition(X0,X2),composition(X1,X2)) = composition(meet(X0,X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0,X1,X2] :
( ( join(X1,one) = one
& join(X0,one) = one )
=> meet(composition(X0,X2),composition(X1,X2)) = composition(meet(X0,X1),X2) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0,X1,X2] :
( meet(composition(X0,X2),composition(X1,X2)) != composition(meet(X0,X1),X2)
& join(X1,one) = one
& join(X0,one) = one ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( meet(composition(sk0,sk2),composition(sk1,sk2)) != composition(meet(sk0,sk1),sk2)
& join(sk1,one) = one
& join(sk0,one) = one ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[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(t451213,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)],[t451213]) ).
cnf(t451249,plain,
join(one,converse(complement(sk0))) = join(one,converse(top)),
inference(step,[status(thm)],[t428,t243]) ).
cnf(t451250,plain,
join(one,converse(complement(sk0))) = join(one,top),
inference(step,[status(thm)],[t451249,t453]) ).
cnf(t451251,plain,
join(one,converse(complement(sk0))) = top,
inference(step,[status(thm)],[t451250,t437]) ).
cnf(t493,plain,
join(one,converse(complement(sk0))) = top,
inference(orient,[status(thm)],[t451251]) ).
cnf(t494,plain,
join(one,join(converse(complement(sk0)),X1)) = join(top,X1),
inference(cp,[status(thm)],[t47,t493]) ).
cnf(t451258,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)],[t451258]) ).
cnf(t951,plain,
top = join(join(converse(complement(sk0)),X1),join(one,complement(top))),
inference(cp,[status(thm)],[t899,t542]) ).
cnf(t451441,plain,
top = join(converse(complement(sk0)),join(X1,join(one,complement(top)))),
inference(step,[status(thm)],[t951,t47]) ).
cnf(t451442,plain,
top = join(converse(complement(sk0)),join(X1,join(one,zero))),
inference(step,[status(thm)],[t451441,t100]) ).
cnf(t451443,plain,
top = join(converse(complement(sk0)),join(X1,join(zero,one))),
inference(step,[status(thm)],[t451442,t44]) ).
cnf(t3107,plain,
join(converse(complement(sk0)),join(X1,join(zero,one))) = top,
inference(orient,[status(thm)],[t451443]) ).
cnf(t3112,plain,
top = join(converse(complement(sk0)),join(join(zero,one),X1)),
inference(cp,[status(thm)],[t3107,t44]) ).
cnf(t451540,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)],[t451540]) ).
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(t451204,plain,
top = join(zero,top),
inference(step,[status(thm)],[t102,t44]) ).
cnf(t107,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t451204]) ).
cnf(t451564,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)],[t451564]) ).
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(t451630,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)],[t451630]) ).
cnf(t451715,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t451714,t5206]) ).
cnf(t7456,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t451715]) ).
cnf(t7458,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t25,t7456]) ).
cnf(t451723,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t7458,t443]) ).
cnf(t451724,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t451723,t7456]) ).
cnf(t7521,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t451724]) ).
cnf(t451727,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)],[t451727]) ).
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(t451751,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t7633,t47]) ).
cnf(t451752,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t451751,t7521]) ).
cnf(t7901,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t451752]) ).
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(t451843,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)],[t451843]) ).
cnf(t9763,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t9751,t226]) ).
cnf(t451845,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t9763,t437]) ).
cnf(t451846,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t451845,t7344]) ).
cnf(t9943,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t451846]) ).
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(t451849,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t9988,t453]) ).
cnf(t451850,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t451849,t453]) ).
cnf(t10027,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t451850]) ).
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(t451869,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t10058,t453]) ).
cnf(t451870,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t451869,t44]) ).
cnf(t451871,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t451870,t100]) ).
cnf(t451872,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t451871,t7456]) ).
cnf(t10857,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t451872]) ).
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]) ).
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(t451899,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t11867,t11920]) ).
cnf(t451900,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t451899,t11920]) ).
cnf(t11984,plain,
composition(zero,X1) = zero,
inference(rw,[status(thm)],[t451900]) ).
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(t451926,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t12018,t11920]) ).
cnf(t451927,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t451926,t12007]) ).
cnf(t451928,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t451927,t44]) ).
cnf(t12045,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t451928]) ).
cnf(t451941,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)],[t451941]) ).
cnf(t12150,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t12105]) ).
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(t451946,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t12111,t437]) ).
cnf(t451947,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t451946,t100]) ).
cnf(t12144,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t451947]) ).
cnf(t452000,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t12319,t12144]) ).
cnf(t452001,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t452000,t12045]) ).
cnf(t452002,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t452001,t12150]) ).
cnf(t12361,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t452002]) ).
cnf(t452003,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t12150,t12361]) ).
cnf(t12362,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t452003]) ).
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(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(t452399,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t30194,t12362]) ).
cnf(t452400,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t452399,t88]) ).
cnf(t30220,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t452400]) ).
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(t27007,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t18688,t26949]) ).
cnf(t456250,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(step,[status(thm)],[t27007,t18688]) ).
cnf(t293789,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t456250]) ).
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(t451998,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)],[t451998]) ).
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(t293818,plain,
join(X1,X2) = join(X1,meet(X2,join(X3,complement(X1)))),
inference(cp,[status(thm)],[t293789,t14339]) ).
cnf(t413343,plain,
join(X1,meet(X2,join(X3,complement(X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t293818]) ).
cnf(t413558,plain,
meet(X1,meet(X2,join(X3,complement(complement(X1))))) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t30301,t413343]) ).
cnf(t457258,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t413558,t12362]) ).
cnf(t457259,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(step,[status(thm)],[t457258,t30301]) ).
cnf(t414790,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t457259]) ).
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(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(t451710,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)],[t451710]) ).
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(t451657,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)],[t451657]) ).
cnf(t5822,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t88,t5807]) ).
cnf(t451658,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)],[t451658]) ).
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(t451999,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)],[t451999]) ).
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(t452081,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(t452082,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)],[t452081,t12007]) ).
cnf(t452083,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)],[t452082,t109]) ).
cnf(t452084,plain,
zero = join(meet(converse(complement(X1)),converse(X1)),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t452083,t226]) ).
cnf(t452085,plain,
zero = join(meet(converse(X1),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t452084,t109]) ).
cnf(t452086,plain,
zero = join(meet(converse(X1),converse(complement(X1))),zero),
inference(step,[status(thm)],[t452085,t12007]) ).
cnf(t452087,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(step,[status(thm)],[t452086,t12307]) ).
cnf(t15008,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t452087]) ).
cnf(t30942,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t30886,t15008]) ).
cnf(t452448,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t30942,t44]) ).
cnf(t452449,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t452448,t12307]) ).
cnf(t34958,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t452449]) ).
cnf(t34963,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t34958,t12362]) ).
cnf(t451244,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)],[t451244]) ).
cnf(t13254,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t13215,t456]) ).
cnf(t452344,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)],[t452344]) ).
cnf(t27576,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t27561,t26171]) ).
cnf(t452394,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t27576,t12362]) ).
cnf(t452395,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t452394,t12307]) ).
cnf(t29259,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t452395]) ).
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(t452450,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)],[t452450]) ).
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(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(t451962,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)],[t451962]) ).
cnf(t452009,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)],[t452009]) ).
cnf(t14183,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t12389]) ).
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(t452507,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t36708,t13215]) ).
cnf(t452508,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t452507,t35008]) ).
cnf(t452509,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t452508,t12362]) ).
cnf(t36738,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t452509]) ).
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(t451215,plain,
join(one,converse(sk0)) = one,
inference(step,[status(thm)],[t245,t215]) ).
cnf(t260,plain,
join(one,converse(sk0)) = one,
inference(orient,[status(thm)],[t451215]) ).
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(t451271,plain,
join(one,join(sk0,X1)) = converse(join(one,converse(X1))),
inference(step,[status(thm)],[t650,t22]) ).
cnf(t451272,plain,
join(one,join(sk0,X1)) = join(one,converse(converse(X1))),
inference(step,[status(thm)],[t451271,t232]) ).
cnf(t451273,plain,
join(one,join(sk0,X1)) = join(one,X1),
inference(step,[status(thm)],[t451272,t22]) ).
cnf(t653,plain,
join(one,join(sk0,X1)) = join(one,X1),
inference(orient,[status(thm)],[t451273]) ).
cnf(t12492,plain,
join(one,meet(sk0,X1)) = join(one,sk0),
inference(cp,[status(thm)],[t653,t12485]) ).
cnf(t452019,plain,
join(one,meet(sk0,X1)) = join(sk0,one),
inference(step,[status(thm)],[t12492,t44]) ).
cnf(t452020,plain,
join(one,meet(sk0,X1)) = one,
inference(step,[status(thm)],[t452019,t84]) ).
cnf(t12743,plain,
join(one,meet(sk0,X1)) = one,
inference(orient,[status(thm)],[t452020]) ).
cnf(t83262,plain,
join(X1,composition(meet(sk0,X2),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t83099,t12743]) ).
cnf(t453535,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)],[t453535]) ).
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(t452042,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)],[t452042]) ).
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(t452225,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)],[t452225]) ).
cnf(t14285,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t12521,t14278]) ).
cnf(t452051,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)],[t452051]) ).
cnf(t14435,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t12362,t14374]) ).
cnf(t452052,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)],[t452052]) ).
cnf(t14462,plain,
meet(X1,X2) = meet(meet(X1,X2),X2),
inference(cp,[status(thm)],[t14459,t12521]) ).
cnf(t452056,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)],[t452056]) ).
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(t452691,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)],[t452691]) ).
cnf(t27623,plain,
meet(X1,complement(meet(complement(complement(X1)),X2))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t13215,t27561]) ).
cnf(t452405,plain,
meet(X1,join(complement(X1),complement(X2))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t27623,t14339]) ).
cnf(t452406,plain,
meet(X1,complement(meet(X1,X2))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t452405,t14183]) ).
cnf(t452407,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t452406,t13215]) ).
cnf(t31035,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t452407]) ).
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(t451784,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(t451785,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)],[t451784,t18]) ).
cnf(t451786,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)],[t451785,t109]) ).
cnf(t451787,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)],[t451786,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)],[t451787]) ).
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(t451214,plain,
join(one,converse(sk1)) = one,
inference(step,[status(thm)],[t244,t215]) ).
cnf(t257,plain,
join(one,converse(sk1)) = one,
inference(orient,[status(thm)],[t451214]) ).
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(t452032,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)],[t452032]) ).
cnf(t13309,plain,
zero = meet(converse(meet(X1,sk1)),complement(one)),
inference(cp,[status(thm)],[t13299,t13073]) ).
cnf(t452118,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)],[t452118]) ).
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(t452548,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(t452549,plain,
zero = join(meet(one,composition(complement(one),meet(X1,sk1))),composition(zero,meet(meet(X1,sk1),converse(complement(one))))),
inference(step,[status(thm)],[t452548,t12007]) ).
cnf(t452550,plain,
zero = join(meet(one,composition(complement(one),meet(X1,sk1))),zero),
inference(step,[status(thm)],[t452549,t12007]) ).
cnf(t452551,plain,
zero = meet(one,composition(complement(one),meet(X1,sk1))),
inference(step,[status(thm)],[t452550,t12307]) ).
cnf(t40500,plain,
meet(one,composition(complement(one),meet(X1,sk1))) = zero,
inference(orient,[status(thm)],[t452551]) ).
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(t452554,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(t452555,plain,
meet(one,complement(composition(complement(one),sk1))) = one,
inference(step,[status(thm)],[t452554,t12433]) ).
cnf(t40545,plain,
meet(one,complement(composition(complement(one),sk1))) = one,
inference(orient,[status(thm)],[t452555]) ).
cnf(t44297,plain,
zero = meet(complement(complement(composition(complement(one),sk1))),meet(X1,one)),
inference(cp,[status(thm)],[t44169,t40545]) ).
cnf(t453169,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)],[t453169]) ).
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(t453170,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)],[t453170]) ).
cnf(t65095,plain,
sk0 = join(zero,meet(complement(composition(complement(one),sk1)),sk0)),
inference(cp,[status(thm)],[t51849,t65090]) ).
cnf(t453179,plain,
sk0 = meet(complement(composition(complement(one),sk1)),sk0),
inference(step,[status(thm)],[t65095,t12235]) ).
cnf(t453180,plain,
sk0 = meet(sk0,complement(composition(complement(one),sk1))),
inference(step,[status(thm)],[t453179,t109]) ).
cnf(t65138,plain,
meet(sk0,complement(composition(complement(one),sk1))) = sk0,
inference(orient,[status(thm)],[t453180]) ).
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(t87127,plain,
join(X1,converse(composition(sk0,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t324,t87044]) ).
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(t452213,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(t452214,plain,
composition(sk0,meet(one,converse(sk0))) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t452213,t18]) ).
cnf(t14495,plain,
converse(sk0) = meet(converse(sk0),one),
inference(cp,[status(thm)],[t14459,t260]) ).
cnf(t452054,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)],[t452054]) ).
cnf(t452215,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t452214,t14545]) ).
cnf(t452216,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t452215,t14621]) ).
cnf(t452217,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,meet(one,converse(sk0)))),
inference(step,[status(thm)],[t452216,t18]) ).
cnf(t452218,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,converse(sk0))),
inference(step,[status(thm)],[t452217,t14545]) ).
cnf(t17603,plain,
join(sk0,composition(sk0,converse(sk0))) = composition(sk0,converse(sk0)),
inference(orient,[status(thm)],[t452218]) ).
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(t452717,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)],[t452717]) ).
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(t453254,plain,
sk0 = meet(sk0,converse(sk0)),
inference(step,[status(thm)],[t68312,t226]) ).
cnf(t68413,plain,
meet(sk0,converse(sk0)) = sk0,
inference(orient,[status(thm)],[t453254]) ).
cnf(t68478,plain,
meet(sk0,converse(sk0)) = converse(sk0),
inference(cp,[status(thm)],[t36853,t68413]) ).
cnf(t453255,plain,
sk0 = converse(sk0),
inference(step,[status(thm)],[t68478,t68413]) ).
cnf(t68503,plain,
converse(sk0) = sk0,
inference(orient,[status(thm)],[t453255]) ).
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(t453565,plain,
join(X1,composition(converse(converse(X1)),sk0)) = converse(converse(X1)),
inference(step,[status(thm)],[t87127,t69344]) ).
cnf(t453566,plain,
join(X1,composition(X1,sk0)) = converse(converse(X1)),
inference(step,[status(thm)],[t453565,t22]) ).
cnf(t453567,plain,
join(X1,composition(X1,sk0)) = X1,
inference(step,[status(thm)],[t453566,t22]) ).
cnf(t87210,plain,
join(X1,composition(X1,sk0)) = X1,
inference(orient,[status(thm)],[t453567]) ).
cnf(t87240,plain,
join(X1,join(composition(X1,sk0),X2)) = join(X1,X2),
inference(cp,[status(thm)],[t47,t87210]) ).
cnf(t102363,plain,
join(X1,join(composition(X1,sk0),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t87240]) ).
cnf(t102385,plain,
join(X1,composition(X2,sk0)) = join(X1,composition(join(X1,X2),sk0)),
inference(cp,[status(thm)],[t102363,t25]) ).
cnf(t235378,plain,
join(X1,composition(join(X1,X2),sk0)) = join(X1,composition(X2,sk0)),
inference(orient,[status(thm)],[t102385]) ).
cnf(t235546,plain,
join(X1,composition(complement(X1),sk0)) = join(X1,composition(top,sk0)),
inference(cp,[status(thm)],[t235378,t52]) ).
cnf(t236027,plain,
join(X1,composition(complement(X1),sk0)) = join(X1,composition(top,sk0)),
inference(orient,[status(thm)],[t235546]) ).
cnf(t236151,plain,
meet(X1,composition(complement(complement(X1)),sk0)) = meet(X1,join(complement(X1),composition(top,sk0))),
inference(cp,[status(thm)],[t30301,t236027]) ).
cnf(t455650,plain,
meet(X1,composition(X1,sk0)) = meet(X1,join(complement(X1),composition(top,sk0))),
inference(step,[status(thm)],[t236151,t12362]) ).
cnf(t87238,plain,
composition(X1,sk0) = meet(composition(X1,sk0),X1),
inference(cp,[status(thm)],[t14459,t87210]) ).
cnf(t453569,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)],[t453569]) ).
cnf(t455651,plain,
composition(X1,sk0) = meet(X1,join(complement(X1),composition(top,sk0))),
inference(step,[status(thm)],[t455650,t87549]) ).
cnf(t455652,plain,
composition(X1,sk0) = meet(X1,composition(top,sk0)),
inference(step,[status(thm)],[t455651,t30301]) ).
cnf(t236212,plain,
meet(X1,composition(top,sk0)) = composition(X1,sk0),
inference(orient,[status(thm)],[t455652]) ).
cnf(t236335,plain,
meet(X1,converse(composition(top,sk0))) = converse(composition(converse(X1),sk0)),
inference(cp,[status(thm)],[t36738,t236212]) ).
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(t455653,plain,
meet(X1,composition(converse(sk0),top)) = converse(composition(converse(X1),sk0)),
inference(step,[status(thm)],[t236335,t479]) ).
cnf(t455654,plain,
meet(X1,composition(sk0,top)) = converse(composition(converse(X1),sk0)),
inference(step,[status(thm)],[t455653,t68503]) ).
cnf(t455655,plain,
meet(X1,composition(sk0,top)) = composition(converse(sk0),X1),
inference(step,[status(thm)],[t455654,t192]) ).
cnf(t455656,plain,
meet(X1,composition(sk0,top)) = composition(sk0,X1),
inference(step,[status(thm)],[t455655,t68503]) ).
cnf(t236752,plain,
meet(X1,composition(sk0,top)) = composition(sk0,X1),
inference(orient,[status(thm)],[t455656]) ).
cnf(t236755,plain,
composition(sk0,X1) = meet(composition(sk0,top),X1),
inference(cp,[status(thm)],[t236752,t109]) ).
cnf(t237077,plain,
meet(composition(sk0,top),X1) = composition(sk0,X1),
inference(orient,[status(thm)],[t236755]) ).
cnf(t414873,plain,
meet(X1,composition(sk0,top)) = meet(X1,composition(sk0,join(X2,X1))),
inference(cp,[status(thm)],[t414790,t237077]) ).
cnf(t457260,plain,
composition(sk0,X1) = meet(X1,composition(sk0,join(X2,X1))),
inference(step,[status(thm)],[t414873,t236752]) ).
cnf(t416610,plain,
meet(X1,composition(sk0,join(X2,X1))) = composition(sk0,X1),
inference(orient,[status(thm)],[t457260]) ).
cnf(t634,plain,
join(one,converse(converse(join(sk1,X1)))) = converse(join(one,converse(X1))),
inference(cp,[status(thm)],[t232,t632]) ).
cnf(t451268,plain,
join(one,join(sk1,X1)) = converse(join(one,converse(X1))),
inference(step,[status(thm)],[t634,t22]) ).
cnf(t451269,plain,
join(one,join(sk1,X1)) = join(one,converse(converse(X1))),
inference(step,[status(thm)],[t451268,t232]) ).
cnf(t451270,plain,
join(one,join(sk1,X1)) = join(one,X1),
inference(step,[status(thm)],[t451269,t22]) ).
cnf(t637,plain,
join(one,join(sk1,X1)) = join(one,X1),
inference(orient,[status(thm)],[t451270]) ).
cnf(t12493,plain,
join(one,meet(sk1,X1)) = join(one,sk1),
inference(cp,[status(thm)],[t637,t12485]) ).
cnf(t452021,plain,
join(one,meet(sk1,X1)) = join(sk1,one),
inference(step,[status(thm)],[t12493,t44]) ).
cnf(t452022,plain,
join(one,meet(sk1,X1)) = one,
inference(step,[status(thm)],[t452021,t86]) ).
cnf(t12792,plain,
join(one,meet(sk1,X1)) = one,
inference(orient,[status(thm)],[t452022]) ).
cnf(t83261,plain,
join(X1,composition(meet(sk1,X2),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t83099,t12792]) ).
cnf(t453451,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)],[t453451]) ).
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(t65073,plain,
zero = meet(composition(complement(one),sk1),sk1),
inference(cp,[status(thm)],[t65068,t14608]) ).
cnf(t453171,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)],[t453171]) ).
cnf(t65111,plain,
sk1 = join(zero,meet(complement(composition(complement(one),sk1)),sk1)),
inference(cp,[status(thm)],[t51849,t65106]) ).
cnf(t453191,plain,
sk1 = meet(complement(composition(complement(one),sk1)),sk1),
inference(step,[status(thm)],[t65111,t12235]) ).
cnf(t453192,plain,
sk1 = meet(sk1,complement(composition(complement(one),sk1))),
inference(step,[status(thm)],[t453191,t109]) ).
cnf(t65372,plain,
meet(sk1,complement(composition(complement(one),sk1))) = sk1,
inference(orient,[status(thm)],[t453192]) ).
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(t416730,plain,
composition(sk0,composition(sk1,X1)) = meet(composition(sk1,X1),composition(sk0,X1)),
inference(cp,[status(thm)],[t416610,t84977]) ).
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(t452206,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(t452207,plain,
composition(sk1,meet(one,converse(sk1))) = join(sk1,composition(meet(sk1,one),meet(one,composition(converse(sk1),one)))),
inference(step,[status(thm)],[t452206,t18]) ).
cnf(t14494,plain,
converse(sk1) = meet(converse(sk1),one),
inference(cp,[status(thm)],[t14459,t257]) ).
cnf(t452053,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)],[t452053]) ).
cnf(t452208,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(meet(sk1,one),meet(one,composition(converse(sk1),one)))),
inference(step,[status(thm)],[t452207,t14532]) ).
cnf(t452209,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(sk1,meet(one,composition(converse(sk1),one)))),
inference(step,[status(thm)],[t452208,t14608]) ).
cnf(t452210,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(sk1,meet(one,converse(sk1)))),
inference(step,[status(thm)],[t452209,t18]) ).
cnf(t452211,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(sk1,converse(sk1))),
inference(step,[status(thm)],[t452210,t14532]) ).
cnf(t17555,plain,
join(sk1,composition(sk1,converse(sk1))) = composition(sk1,converse(sk1)),
inference(orient,[status(thm)],[t452211]) ).
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(t452747,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)],[t452747]) ).
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(t453300,plain,
sk1 = meet(sk1,converse(sk1)),
inference(step,[status(thm)],[t72502,t226]) ).
cnf(t72603,plain,
meet(sk1,converse(sk1)) = sk1,
inference(orient,[status(thm)],[t453300]) ).
cnf(t72668,plain,
meet(sk1,converse(sk1)) = converse(sk1),
inference(cp,[status(thm)],[t36853,t72603]) ).
cnf(t453301,plain,
sk1 = converse(sk1),
inference(step,[status(thm)],[t72668,t72603]) ).
cnf(t72693,plain,
converse(sk1) = sk1,
inference(orient,[status(thm)],[t453301]) ).
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(t87073,plain,
composition(sk0,X1) = meet(composition(sk0,X1),X1),
inference(cp,[status(thm)],[t14459,t87044]) ).
cnf(t453568,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)],[t453568]) ).
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(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(t453636,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(t453637,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)],[t453636,t226]) ).
cnf(t453638,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)],[t453637,t215]) ).
cnf(t453639,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)],[t453638,t226]) ).
cnf(t83319,plain,
join(X1,composition(meet(one,X2),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t83099,t12485]) ).
cnf(t453581,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)],[t453581]) ).
cnf(t453640,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = meet(X2,X1),
inference(step,[status(thm)],[t453639,t88435]) ).
cnf(t91799,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t453640]) ).
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(t87572,plain,
meet(X1,composition(X1,sk0)) = meet(join(X2,X1),composition(X1,sk0)),
inference(cp,[status(thm)],[t22054,t87549]) ).
cnf(t453804,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)],[t453804]) ).
cnf(t17961,plain,
join(X1,meet(meet(X1,X2),X3)) = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t17925,t12485]) ).
cnf(t452224,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)],[t452224]) ).
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(t452683,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)],[t452683]) ).
cnf(t12544,plain,
join(one,converse(meet(X1,sk0))) = join(one,converse(sk0)),
inference(cp,[status(thm)],[t648,t12521]) ).
cnf(t452031,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)],[t452031]) ).
cnf(t13311,plain,
zero = meet(converse(meet(X1,sk0)),complement(one)),
inference(cp,[status(thm)],[t13299,t13049]) ).
cnf(t452120,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)],[t452120]) ).
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(t451645,plain,
join(complement(one),composition(top,zero)) = join(zero,complement(one)),
inference(step,[status(thm)],[t5444,t44]) ).
cnf(t451646,plain,
complement(one) = join(zero,complement(one)),
inference(step,[status(thm)],[t451645,t1881]) ).
cnf(t5466,plain,
join(zero,complement(one)) = complement(one),
inference(orient,[status(thm)],[t451646]) ).
cnf(t5479,plain,
meet(top,one) = complement(complement(one)),
inference(cp,[status(thm)],[t131,t5466]) ).
cnf(t451647,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)],[t451647]) ).
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(t452011,plain,
meet(one,composition(converse(complement(one)),one)) = zero,
inference(step,[status(thm)],[t6302,t12361]) ).
cnf(t452012,plain,
meet(one,converse(complement(one))) = zero,
inference(step,[status(thm)],[t452011,t18]) ).
cnf(t12391,plain,
meet(one,converse(complement(one))) = zero,
inference(rw,[status(thm)],[t452012]) ).
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(t452352,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)],[t452352]) ).
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(t452359,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(t452354,plain,
complement(one) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(step,[status(thm)],[t26777,t22]) ).
cnf(t452355,plain,
complement(one) = meet(converse(complement(one)),converse(converse(complement(one)))),
inference(step,[status(thm)],[t452354,t109]) ).
cnf(t452356,plain,
complement(one) = meet(converse(complement(one)),complement(one)),
inference(step,[status(thm)],[t452355,t22]) ).
cnf(t452357,plain,
complement(one) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t452356,t109]) ).
cnf(t26790,plain,
meet(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t452357]) ).
cnf(t452360,plain,
converse(complement(one)) = complement(one),
inference(step,[status(thm)],[t452359,t26790]) ).
cnf(t27048,plain,
converse(complement(one)) = complement(one),
inference(orient,[status(thm)],[t452360]) ).
cnf(t452577,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(t452578,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)],[t452577,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(t452047,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)],[t452047]) ).
cnf(t452579,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)],[t452578,t14028]) ).
cnf(t452580,plain,
zero = join(meet(one,composition(meet(X1,sk0),complement(one))),composition(meet(meet(X1,sk0),converse(complement(one))),zero)),
inference(step,[status(thm)],[t452579,t12007]) ).
cnf(t452581,plain,
zero = join(meet(one,composition(meet(X1,sk0),complement(one))),zero),
inference(step,[status(thm)],[t452580,t11831]) ).
cnf(t452582,plain,
zero = meet(one,composition(meet(X1,sk0),complement(one))),
inference(step,[status(thm)],[t452581,t12307]) ).
cnf(t40813,plain,
meet(one,composition(meet(X1,sk0),complement(one))) = zero,
inference(orient,[status(thm)],[t452582]) ).
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(t452585,plain,
meet(one,complement(composition(sk0,complement(one)))) = meet(one,top),
inference(step,[status(thm)],[t40837,t12106]) ).
cnf(t452586,plain,
meet(one,complement(composition(sk0,complement(one)))) = one,
inference(step,[status(thm)],[t452585,t12433]) ).
cnf(t40858,plain,
meet(one,complement(composition(sk0,complement(one)))) = one,
inference(orient,[status(thm)],[t452586]) ).
cnf(t43966,plain,
zero = meet(complement(complement(composition(sk0,complement(one)))),meet(one,X1)),
inference(cp,[status(thm)],[t43838,t40858]) ).
cnf(t452936,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)],[t452936]) ).
cnf(t59153,plain,
zero = meet(composition(sk0,complement(one)),converse(sk1)),
inference(cp,[status(thm)],[t59116,t14532]) ).
cnf(t452938,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)],[t452938]) ).
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(t452966,plain,
meet(sk1,composition(complement(one),converse(sk0))) = converse(zero),
inference(step,[status(thm)],[t59216,t27304]) ).
cnf(t452967,plain,
meet(sk1,composition(complement(one),converse(sk0))) = zero,
inference(step,[status(thm)],[t452966,t11920]) ).
cnf(t59497,plain,
meet(sk1,composition(complement(one),converse(sk0))) = zero,
inference(orient,[status(thm)],[t452967]) ).
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(t452968,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(t452969,plain,
zero = join(meet(composition(sk1,sk0),complement(one)),composition(zero,meet(sk0,composition(converse(sk1),complement(one))))),
inference(step,[status(thm)],[t452968,t12007]) ).
cnf(t452970,plain,
zero = join(meet(complement(one),composition(sk1,sk0)),composition(zero,meet(sk0,composition(converse(sk1),complement(one))))),
inference(step,[status(thm)],[t452969,t109]) ).
cnf(t452971,plain,
zero = join(meet(complement(one),composition(sk1,sk0)),zero),
inference(step,[status(thm)],[t452970,t12007]) ).
cnf(t452972,plain,
zero = meet(complement(one),composition(sk1,sk0)),
inference(step,[status(thm)],[t452971,t12307]) ).
cnf(t59518,plain,
meet(complement(one),composition(sk1,sk0)) = zero,
inference(orient,[status(thm)],[t452972]) ).
cnf(t59519,plain,
join(complement(complement(one)),composition(sk1,sk0)) = join(complement(complement(one)),zero),
inference(cp,[status(thm)],[t30886,t59518]) ).
cnf(t452973,plain,
join(composition(sk1,sk0),complement(complement(one))) = join(complement(complement(one)),zero),
inference(step,[status(thm)],[t59519,t44]) ).
cnf(t452974,plain,
join(composition(sk1,sk0),one) = join(complement(complement(one)),zero),
inference(step,[status(thm)],[t452973,t12362]) ).
cnf(t452975,plain,
join(one,composition(sk1,sk0)) = join(complement(complement(one)),zero),
inference(step,[status(thm)],[t452974,t44]) ).
cnf(t452976,plain,
join(one,composition(sk1,sk0)) = complement(complement(one)),
inference(step,[status(thm)],[t452975,t12307]) ).
cnf(t452977,plain,
join(one,composition(sk1,sk0)) = one,
inference(step,[status(thm)],[t452976,t12362]) ).
cnf(t59538,plain,
join(one,composition(sk1,sk0)) = one,
inference(orient,[status(thm)],[t452977]) ).
cnf(t83151,plain,
join(X1,composition(composition(sk1,sk0),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t83099,t59538]) ).
cnf(t453443,plain,
join(X1,composition(sk1,composition(sk0,X1))) = composition(one,X1),
inference(step,[status(thm)],[t83151,t23]) ).
cnf(t453444,plain,
join(X1,composition(sk1,composition(sk0,X1))) = X1,
inference(step,[status(thm)],[t453443,t226]) ).
cnf(t84427,plain,
join(X1,composition(sk1,composition(sk0,X1))) = X1,
inference(orient,[status(thm)],[t453444]) ).
cnf(t84458,plain,
composition(sk1,composition(sk0,X1)) = meet(composition(sk1,composition(sk0,X1)),X1),
inference(cp,[status(thm)],[t14459,t84427]) ).
cnf(t455421,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)],[t455421]) ).
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(t455422,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(t455423,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)],[t455422,t215]) ).
cnf(t455424,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)],[t455423,t226]) ).
cnf(t455425,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)],[t455424,t109]) ).
cnf(t455426,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)],[t455425,t72693]) ).
cnf(t455427,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)],[t455426,t18]) ).
cnf(t14478,plain,
meet(sk1,X1) = meet(meet(sk1,X1),one),
inference(cp,[status(thm)],[t14459,t12792]) ).
cnf(t452057,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)],[t452057]) ).
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(t453831,plain,
meet(sk1,X1) = composition(meet(one,composition(meet(sk1,X1),converse(one))),meet(sk1,X1)),
inference(step,[status(thm)],[t92034,t14740]) ).
cnf(t453832,plain,
meet(sk1,X1) = composition(meet(one,composition(meet(sk1,X1),one)),meet(sk1,X1)),
inference(step,[status(thm)],[t453831,t215]) ).
cnf(t453833,plain,
meet(sk1,X1) = composition(meet(one,meet(sk1,X1)),meet(sk1,X1)),
inference(step,[status(thm)],[t453832,t18]) ).
cnf(t453834,plain,
meet(sk1,X1) = composition(meet(sk1,X1),meet(sk1,X1)),
inference(step,[status(thm)],[t453833,t14740]) ).
cnf(t106271,plain,
composition(meet(sk1,X1),meet(sk1,X1)) = meet(sk1,X1),
inference(orient,[status(thm)],[t453834]) ).
cnf(t455428,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)],[t455427,t106271]) ).
cnf(t455429,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)],[t455428,t18]) ).
cnf(t455430,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)],[t455429,t69344]) ).
cnf(t455431,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,composition(one,sk0)),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t455430,t215]) ).
cnf(t455432,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,sk0),meet(composition(sk0,one),converse(sk1)))),
inference(step,[status(thm)],[t455431,t226]) ).
cnf(t455433,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,sk0),meet(converse(sk1),composition(sk0,one)))),
inference(step,[status(thm)],[t455432,t109]) ).
cnf(t455434,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,sk0),meet(sk1,composition(sk0,one)))),
inference(step,[status(thm)],[t455433,t72693]) ).
cnf(t455435,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),composition(meet(sk1,sk0),meet(sk1,sk0))),
inference(step,[status(thm)],[t455434,t18]) ).
cnf(t455436,plain,
meet(sk1,sk0) = join(composition(sk1,sk0),meet(sk1,sk0)),
inference(step,[status(thm)],[t455435,t106271]) ).
cnf(t455437,plain,
meet(sk1,sk0) = join(meet(sk1,sk0),composition(sk1,sk0)),
inference(step,[status(thm)],[t455436,t44]) ).
cnf(t205605,plain,
join(meet(sk1,sk0),composition(sk1,sk0)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t455437]) ).
cnf(t205607,plain,
composition(composition(sk1,sk0),sk0) = meet(meet(sk1,sk0),composition(composition(sk1,sk0),sk0)),
inference(cp,[status(thm)],[t105399,t205605]) ).
cnf(t455438,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(t452187,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(t452188,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)],[t452187,t28]) ).
cnf(t452189,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)],[t452188,t18]) ).
cnf(t452190,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)],[t452189,t14545]) ).
cnf(t452191,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),composition(meet(one,converse(sk0)),meet(one,composition(converse(one),converse(sk0))))),
inference(step,[status(thm)],[t452190,t28]) ).
cnf(t452192,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),composition(converse(sk0),meet(one,composition(converse(one),converse(sk0))))),
inference(step,[status(thm)],[t452191,t14545]) ).
cnf(t452193,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),composition(converse(sk0),meet(one,converse(composition(sk0,one))))),
inference(step,[status(thm)],[t452192,t28]) ).
cnf(t452194,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),composition(converse(sk0),meet(one,converse(sk0)))),
inference(step,[status(thm)],[t452193,t18]) ).
cnf(t452195,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),composition(converse(sk0),converse(sk0))),
inference(step,[status(thm)],[t452194,t14545]) ).
cnf(t452196,plain,
converse(composition(sk0,sk0)) = join(converse(sk0),converse(composition(sk0,sk0))),
inference(step,[status(thm)],[t452195,t28]) ).
cnf(t452197,plain,
converse(composition(sk0,sk0)) = converse(join(sk0,composition(sk0,sk0))),
inference(step,[status(thm)],[t452196,t61]) ).
cnf(t16827,plain,
converse(join(sk0,composition(sk0,sk0))) = converse(composition(sk0,sk0)),
inference(orient,[status(thm)],[t452197]) ).
cnf(t16828,plain,
join(sk0,composition(sk0,sk0)) = converse(converse(composition(sk0,sk0))),
inference(cp,[status(thm)],[t22,t16827]) ).
cnf(t452198,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)],[t452198]) ).
cnf(t453537,plain,
sk0 = composition(sk0,sk0),
inference(step,[status(thm)],[t16888,t87044]) ).
cnf(t87141,plain,
sk0 = composition(sk0,sk0),
inference(rw,[status(thm)],[t453537]) ).
cnf(t87142,plain,
composition(sk0,sk0) = sk0,
inference(orient,[status(thm)],[t87141]) ).
cnf(t455439,plain,
composition(sk1,sk0) = meet(meet(sk1,sk0),composition(composition(sk1,sk0),sk0)),
inference(step,[status(thm)],[t455438,t87142]) ).
cnf(t455440,plain,
composition(sk1,sk0) = meet(meet(sk1,sk0),composition(sk1,composition(sk0,sk0))),
inference(step,[status(thm)],[t455439,t23]) ).
cnf(t455441,plain,
composition(sk1,sk0) = meet(meet(sk1,sk0),composition(sk1,sk0)),
inference(step,[status(thm)],[t455440,t87142]) ).
cnf(t205661,plain,
meet(meet(sk1,sk0),composition(sk1,sk0)) = composition(sk1,sk0),
inference(orient,[status(thm)],[t455441]) ).
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(t455442,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(t455443,plain,
composition(sk1,sk0) = composition(meet(one,composition(sk1,composition(sk0,converse(meet(sk1,sk0))))),composition(sk1,sk0)),
inference(step,[status(thm)],[t455442,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(t455444,plain,
composition(sk1,sk0) = composition(meet(one,composition(sk1,composition(sk0,meet(sk1,converse(sk0))))),composition(sk1,sk0)),
inference(step,[status(thm)],[t455443,t72909]) ).
cnf(t455445,plain,
composition(sk1,sk0) = composition(meet(one,composition(sk1,composition(sk0,meet(sk1,sk0)))),composition(sk1,sk0)),
inference(step,[status(thm)],[t455444,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(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(t452201,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)],[t452201]) ).
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(t451238,plain,
join(one,complement(sk1)) = top,
inference(step,[status(thm)],[t422,t443]) ).
cnf(t446,plain,
join(one,complement(sk1)) = top,
inference(orient,[status(thm)],[t451238]) ).
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(t453415,plain,
join(X1,composition(converse(converse(X1)),complement(sk1))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t83623,t76388]) ).
cnf(t453416,plain,
join(X1,composition(X1,complement(sk1))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t453415,t22]) ).
cnf(t453417,plain,
join(X1,composition(X1,complement(sk1))) = composition(converse(converse(X1)),top),
inference(step,[status(thm)],[t453416,t479]) ).
cnf(t453418,plain,
join(X1,composition(X1,complement(sk1))) = composition(X1,top),
inference(step,[status(thm)],[t453417,t22]) ).
cnf(t84054,plain,
join(X1,composition(X1,complement(sk1))) = composition(X1,top),
inference(orient,[status(thm)],[t453418]) ).
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(t453773,plain,
meet(composition(sk0,top),complement(complement(sk1))) = meet(complement(complement(sk1)),join(sk0,complement(sk1))),
inference(step,[status(thm)],[t101820,t109]) ).
cnf(t453774,plain,
meet(composition(sk0,top),sk1) = meet(complement(complement(sk1)),join(sk0,complement(sk1))),
inference(step,[status(thm)],[t453773,t12362]) ).
cnf(t453775,plain,
meet(sk1,composition(sk0,top)) = meet(complement(complement(sk1)),join(sk0,complement(sk1))),
inference(step,[status(thm)],[t453774,t109]) ).
cnf(t30193,plain,
meet(complement(X1),join(X2,X1)) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t14125,t29926]) ).
cnf(t452419,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)],[t452419]) ).
cnf(t453776,plain,
meet(sk1,composition(sk0,top)) = meet(complement(complement(sk1)),sk0),
inference(step,[status(thm)],[t453775,t31267]) ).
cnf(t453777,plain,
meet(sk1,composition(sk0,top)) = meet(sk0,complement(complement(sk1))),
inference(step,[status(thm)],[t453776,t109]) ).
cnf(t453778,plain,
meet(sk1,composition(sk0,top)) = meet(sk0,sk1),
inference(step,[status(thm)],[t453777,t12362]) ).
cnf(t453779,plain,
meet(sk1,composition(sk0,top)) = meet(sk1,sk0),
inference(step,[status(thm)],[t453778,t109]) ).
cnf(t101861,plain,
meet(sk1,composition(sk0,top)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t453779]) ).
cnf(t101862,plain,
meet(sk1,converse(composition(sk0,top))) = converse(meet(sk1,sk0)),
inference(cp,[status(thm)],[t72909,t101861]) ).
cnf(t453780,plain,
meet(sk1,composition(converse(top),sk0)) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t101862,t69344]) ).
cnf(t453781,plain,
meet(sk1,composition(top,sk0)) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t453780,t453]) ).
cnf(t453782,plain,
meet(sk1,composition(top,sk0)) = meet(sk1,converse(sk0)),
inference(step,[status(thm)],[t453781,t72909]) ).
cnf(t453783,plain,
meet(sk1,composition(top,sk0)) = meet(sk1,sk0),
inference(step,[status(thm)],[t453782,t68503]) ).
cnf(t101918,plain,
meet(sk1,composition(top,sk0)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t453783]) ).
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(t453858,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(t453859,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)],[t453858,t23]) ).
cnf(t453860,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)],[t453859,t68503]) ).
cnf(t453861,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)],[t453860,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(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(t451240,plain,
join(one,complement(sk0)) = top,
inference(step,[status(thm)],[t427,t443]) ).
cnf(t448,plain,
join(one,complement(sk0)) = top,
inference(orient,[status(thm)],[t451240]) ).
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(t453427,plain,
join(X1,composition(converse(converse(X1)),complement(sk0))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t83762,t71300]) ).
cnf(t453428,plain,
join(X1,composition(X1,complement(sk0))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t453427,t22]) ).
cnf(t453429,plain,
join(X1,composition(X1,complement(sk0))) = composition(converse(converse(X1)),top),
inference(step,[status(thm)],[t453428,t479]) ).
cnf(t453430,plain,
join(X1,composition(X1,complement(sk0))) = composition(X1,top),
inference(step,[status(thm)],[t453429,t22]) ).
cnf(t84204,plain,
join(X1,composition(X1,complement(sk0))) = composition(X1,top),
inference(orient,[status(thm)],[t453430]) ).
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(t453732,plain,
meet(composition(sk1,top),complement(complement(sk0))) = meet(complement(complement(sk0)),join(sk1,complement(sk0))),
inference(step,[status(thm)],[t97730,t109]) ).
cnf(t453733,plain,
meet(composition(sk1,top),sk0) = meet(complement(complement(sk0)),join(sk1,complement(sk0))),
inference(step,[status(thm)],[t453732,t12362]) ).
cnf(t453734,plain,
meet(sk0,composition(sk1,top)) = meet(complement(complement(sk0)),join(sk1,complement(sk0))),
inference(step,[status(thm)],[t453733,t109]) ).
cnf(t453735,plain,
meet(sk0,composition(sk1,top)) = meet(complement(complement(sk0)),sk1),
inference(step,[status(thm)],[t453734,t31267]) ).
cnf(t453736,plain,
meet(sk0,composition(sk1,top)) = meet(sk1,complement(complement(sk0))),
inference(step,[status(thm)],[t453735,t109]) ).
cnf(t453737,plain,
meet(sk0,composition(sk1,top)) = meet(sk1,sk0),
inference(step,[status(thm)],[t453736,t12362]) ).
cnf(t97771,plain,
meet(sk0,composition(sk1,top)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t453737]) ).
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(t453738,plain,
meet(sk0,composition(converse(top),sk1)) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t97772,t73582]) ).
cnf(t453739,plain,
meet(sk0,composition(top,sk1)) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t453738,t453]) ).
cnf(t453740,plain,
meet(sk0,composition(top,sk1)) = meet(sk1,converse(sk0)),
inference(step,[status(thm)],[t453739,t72909]) ).
cnf(t453741,plain,
meet(sk0,composition(top,sk1)) = meet(sk1,sk0),
inference(step,[status(thm)],[t453740,t68503]) ).
cnf(t97828,plain,
meet(sk0,composition(top,sk1)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t453741]) ).
cnf(t453862,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)],[t453861,t97828]) ).
cnf(t453863,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)],[t453862,t12361]) ).
cnf(t453864,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)],[t453863,t23]) ).
cnf(t453865,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)],[t453864,t68503]) ).
cnf(t453866,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)],[t453865,t453]) ).
cnf(t453867,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = join(meet(sk1,sk0),composition(sk1,composition(sk0,meet(sk1,sk0)))),
inference(step,[status(thm)],[t453866,t97828]) ).
cnf(t453868,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = meet(sk1,sk0),
inference(step,[status(thm)],[t453867,t84427]) ).
cnf(t106771,plain,
composition(sk1,composition(sk0,meet(sk1,sk0))) = meet(sk1,sk0),
inference(orient,[status(thm)],[t453868]) ).
cnf(t455446,plain,
composition(sk1,sk0) = composition(meet(one,meet(sk1,sk0)),composition(sk1,sk0)),
inference(step,[status(thm)],[t455445,t106771]) ).
cnf(t455447,plain,
composition(sk1,sk0) = composition(meet(sk1,sk0),composition(sk1,sk0)),
inference(step,[status(thm)],[t455446,t14740]) ).
cnf(t205753,plain,
composition(meet(sk1,sk0),composition(sk1,sk0)) = composition(sk1,sk0),
inference(orient,[status(thm)],[t455447]) ).
cnf(t205762,plain,
composition(sk0,converse(composition(meet(sk1,sk0),sk1))) = converse(composition(sk1,sk0)),
inference(cp,[status(thm)],[t154245,t205753]) ).
cnf(t455448,plain,
composition(sk0,composition(sk1,converse(meet(sk1,sk0)))) = converse(composition(sk1,sk0)),
inference(step,[status(thm)],[t205762,t73471]) ).
cnf(t455449,plain,
composition(sk0,composition(sk1,meet(sk1,converse(sk0)))) = converse(composition(sk1,sk0)),
inference(step,[status(thm)],[t455448,t72909]) ).
cnf(t455450,plain,
composition(sk0,composition(sk1,meet(sk1,sk0))) = converse(composition(sk1,sk0)),
inference(step,[status(thm)],[t455449,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(t452169,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(t452170,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)],[t452169,t28]) ).
cnf(t452171,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)],[t452170,t18]) ).
cnf(t452172,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)],[t452171,t14532]) ).
cnf(t452173,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t452172,t28]) ).
cnf(t452174,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t452173,t14532]) ).
cnf(t452175,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),meet(one,converse(composition(sk1,one))))),
inference(step,[status(thm)],[t452174,t28]) ).
cnf(t452176,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t452175,t18]) ).
cnf(t452177,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),converse(sk1))),
inference(step,[status(thm)],[t452176,t14532]) ).
cnf(t452178,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),converse(composition(sk1,sk1))),
inference(step,[status(thm)],[t452177,t28]) ).
cnf(t452179,plain,
converse(composition(sk1,sk1)) = converse(join(sk1,composition(sk1,sk1))),
inference(step,[status(thm)],[t452178,t61]) ).
cnf(t16472,plain,
converse(join(sk1,composition(sk1,sk1))) = converse(composition(sk1,sk1)),
inference(orient,[status(thm)],[t452179]) ).
cnf(t16473,plain,
join(sk1,composition(sk1,sk1)) = converse(converse(composition(sk1,sk1))),
inference(cp,[status(thm)],[t22,t16472]) ).
cnf(t452180,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)],[t452180]) ).
cnf(t453452,plain,
sk1 = composition(sk1,sk1),
inference(step,[status(thm)],[t16533,t84977]) ).
cnf(t85076,plain,
sk1 = composition(sk1,sk1),
inference(rw,[status(thm)],[t453452]) ).
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(t453869,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)],[t453869]) ).
cnf(t455451,plain,
composition(sk0,meet(sk1,sk0)) = converse(composition(sk1,sk0)),
inference(step,[status(thm)],[t455450,t106840]) ).
cnf(t455452,plain,
composition(sk0,meet(sk1,sk0)) = composition(converse(sk0),sk1),
inference(step,[status(thm)],[t455451,t73582]) ).
cnf(t455453,plain,
composition(sk0,meet(sk1,sk0)) = composition(sk0,sk1),
inference(step,[status(thm)],[t455452,t68503]) ).
cnf(t205828,plain,
composition(sk0,meet(sk1,sk0)) = composition(sk0,sk1),
inference(orient,[status(thm)],[t455453]) ).
cnf(t205840,plain,
composition(sk0,meet(sk1,sk0)) = meet(meet(sk1,sk0),composition(sk0,sk1)),
inference(cp,[status(thm)],[t87295,t205828]) ).
cnf(t455455,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(t453479,plain,
join(X1,composition(converse(converse(X1)),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t85062,t73582]) ).
cnf(t453480,plain,
join(X1,composition(X1,sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t453479,t22]) ).
cnf(t453481,plain,
join(X1,composition(X1,sk1)) = X1,
inference(step,[status(thm)],[t453480,t22]) ).
cnf(t85178,plain,
join(X1,composition(X1,sk1)) = X1,
inference(orient,[status(thm)],[t453481]) ).
cnf(t85205,plain,
composition(X1,sk1) = meet(composition(X1,sk1),X1),
inference(cp,[status(thm)],[t14459,t85178]) ).
cnf(t453486,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)],[t453486]) ).
cnf(t85632,plain,
meet(X1,composition(X1,sk1)) = meet(composition(X1,sk1),join(X1,X2)),
inference(cp,[status(thm)],[t21240,t85606]) ).
cnf(t453762,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)],[t453762]) ).
cnf(t83263,plain,
join(X1,composition(meet(X2,sk0),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t83099,t12768]) ).
cnf(t453579,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)],[t453579]) ).
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(t453849,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(t453850,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)],[t453849,t97771]) ).
cnf(t453851,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)],[t453850,t12361]) ).
cnf(t453852,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)],[t453851,t68503]) ).
cnf(t453853,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)],[t453852,t453]) ).
cnf(t453854,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)],[t453853,t97771]) ).
cnf(t453855,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = join(meet(sk1,sk0),composition(meet(sk1,sk0),composition(converse(sk0),sk1))),
inference(step,[status(thm)],[t453854,t12361]) ).
cnf(t453856,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = join(meet(sk1,sk0),composition(meet(sk1,sk0),composition(sk0,sk1))),
inference(step,[status(thm)],[t453855,t68503]) ).
cnf(t84516,plain,
join(X1,converse(composition(sk1,composition(sk0,converse(X1))))) = converse(converse(X1)),
inference(cp,[status(thm)],[t324,t84427]) ).
cnf(t453583,plain,
join(X1,composition(converse(composition(sk0,converse(X1))),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t84516,t73582]) ).
cnf(t453584,plain,
join(X1,composition(composition(converse(converse(X1)),sk0),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t453583,t69344]) ).
cnf(t453585,plain,
join(X1,composition(converse(converse(X1)),composition(sk0,sk1))) = converse(converse(X1)),
inference(step,[status(thm)],[t453584,t23]) ).
cnf(t453586,plain,
join(X1,composition(X1,composition(sk0,sk1))) = converse(converse(X1)),
inference(step,[status(thm)],[t453585,t22]) ).
cnf(t453587,plain,
join(X1,composition(X1,composition(sk0,sk1))) = X1,
inference(step,[status(thm)],[t453586,t22]) ).
cnf(t88807,plain,
join(X1,composition(X1,composition(sk0,sk1))) = X1,
inference(orient,[status(thm)],[t453587]) ).
cnf(t453857,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = meet(sk1,sk0),
inference(step,[status(thm)],[t453856,t88807]) ).
cnf(t106712,plain,
composition(meet(sk1,sk0),composition(sk0,sk1)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t453857]) ).
cnf(t106721,plain,
composition(sk0,sk1) = join(composition(sk0,sk1),meet(sk1,sk0)),
inference(cp,[status(thm)],[t88243,t106712]) ).
cnf(t453876,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)],[t453876]) ).
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(t453870,plain,
composition(meet(sk1,converse(sk0)),sk1) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t106846,t72909]) ).
cnf(t453871,plain,
composition(meet(sk1,sk0),sk1) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t453870,t68503]) ).
cnf(t453872,plain,
composition(meet(sk1,sk0),sk1) = meet(sk1,converse(sk0)),
inference(step,[status(thm)],[t453871,t72909]) ).
cnf(t453873,plain,
composition(meet(sk1,sk0),sk1) = meet(sk1,sk0),
inference(step,[status(thm)],[t453872,t68503]) ).
cnf(t106890,plain,
composition(meet(sk1,sk0),sk1) = meet(sk1,sk0),
inference(orient,[status(thm)],[t453873]) ).
cnf(t453877,plain,
meet(sk1,sk0) = meet(composition(meet(sk1,sk0),sk1),composition(sk0,sk1)),
inference(step,[status(thm)],[t107859,t106890]) ).
cnf(t453878,plain,
meet(sk1,sk0) = meet(composition(sk0,sk1),composition(meet(sk1,sk0),sk1)),
inference(step,[status(thm)],[t453877,t109]) ).
cnf(t453879,plain,
meet(sk1,sk0) = meet(composition(sk0,sk1),meet(sk1,sk0)),
inference(step,[status(thm)],[t453878,t106890]) ).
cnf(t453880,plain,
meet(sk1,sk0) = meet(meet(sk1,sk0),composition(sk0,sk1)),
inference(step,[status(thm)],[t453879,t109]) ).
cnf(t107901,plain,
meet(meet(sk1,sk0),composition(sk0,sk1)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t453880]) ).
cnf(t455456,plain,
composition(sk0,sk1) = meet(sk1,sk0),
inference(step,[status(thm)],[t455455,t107901]) ).
cnf(t205925,plain,
composition(sk0,sk1) = meet(sk1,sk0),
inference(orient,[status(thm)],[t455456]) ).
cnf(t205933,plain,
composition(sk1,converse(sk0)) = converse(meet(sk1,sk0)),
inference(cp,[status(thm)],[t73471,t205925]) ).
cnf(t455465,plain,
composition(sk1,sk0) = converse(meet(sk1,sk0)),
inference(step,[status(thm)],[t205933,t68503]) ).
cnf(t455466,plain,
composition(sk1,sk0) = meet(sk1,converse(sk0)),
inference(step,[status(thm)],[t455465,t72909]) ).
cnf(t455467,plain,
composition(sk1,sk0) = meet(sk1,sk0),
inference(step,[status(thm)],[t455466,t68503]) ).
cnf(t205987,plain,
composition(sk1,sk0) = meet(sk1,sk0),
inference(orient,[status(thm)],[t455467]) ).
cnf(t205992,plain,
composition(sk1,composition(sk0,X1)) = composition(meet(sk1,sk0),X1),
inference(cp,[status(thm)],[t23,t205987]) ).
cnf(t205937,plain,
composition(sk0,composition(sk1,X1)) = composition(meet(sk1,sk0),X1),
inference(cp,[status(thm)],[t23,t205925]) ).
cnf(t206101,plain,
composition(meet(sk1,sk0),X1) = composition(sk0,composition(sk1,X1)),
inference(orient,[status(thm)],[t205937]) ).
cnf(t455476,plain,
composition(sk1,composition(sk0,X1)) = composition(sk0,composition(sk1,X1)),
inference(step,[status(thm)],[t205992,t206101]) ).
cnf(t206343,plain,
composition(sk0,composition(sk1,X1)) = composition(sk1,composition(sk0,X1)),
inference(orient,[status(thm)],[t455476]) ).
cnf(t457555,plain,
composition(sk1,composition(sk0,X1)) = meet(composition(sk1,X1),composition(sk0,X1)),
inference(step,[status(thm)],[t416730,t206343]) ).
cnf(t450957,plain,
meet(composition(sk1,X1),composition(sk0,X1)) = composition(sk1,composition(sk0,X1)),
inference(orient,[status(thm)],[t457555]) ).
cnf(t455477,plain,
composition(meet(sk1,sk0),X1) = composition(sk1,composition(sk0,X1)),
inference(step,[status(thm)],[t206101,t206343]) ).
cnf(t206344,plain,
composition(meet(sk1,sk0),X1) = composition(sk1,composition(sk0,X1)),
inference(orient,[status(thm)],[t455477]) ).
cnf(c18,plain,
meet(composition(sk0,sk2),composition(sk1,sk2)) != composition(meet(sk0,sk1),sk2),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
meet(composition(sk0,sk2),composition(sk1,sk2)) != composition(meet(sk0,sk1),sk2),
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(g0_0,plain,
meet(composition(sk1,sk2),composition(sk0,sk2)) != composition(meet(sk0,sk1),sk2),
inference(rw,[status(thm)],[goal_0,t109]) ).
cnf(g0_1,plain,
composition(sk1,composition(sk0,sk2)) != composition(meet(sk0,sk1),sk2),
inference(rw,[status(thm)],[g0_0,t450957]) ).
cnf(g0_2,plain,
composition(sk1,composition(sk0,sk2)) != composition(meet(sk1,sk0),sk2),
inference(rw,[status(thm)],[g0_1,t109]) ).
cnf(g0_3,plain,
composition(sk1,composition(sk0,sk2)) != composition(sk1,composition(sk0,sk2)),
inference(rw,[status(thm)],[g0_2,t206344]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL029+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 07:24:34 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 169.51/25.01 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 169.51/25.01 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------