%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL027+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 : n004.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:06 PM UTC 2026
% Result : Theorem 60.36s 8.15s
% Output : Proof 60.36s
% 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(t6,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t85,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
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(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t43,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t87,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t85,t43]) ).
cnf(t86446,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t87,t85]) ).
cnf(t106,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t86446]) ).
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(t12,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t86443,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t43]) ).
cnf(t54,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t86443]) ).
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(t7,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t27,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
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(t21,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t29,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t169,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t29]) ).
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(t17,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t170,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t169,t17]) ).
cnf(t86450,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t170,t21]) ).
cnf(t182,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t86450]) ).
cnf(t183,plain,
one = converse(one),
inference(cp,[status(thm)],[t182,t17]) ).
cnf(t192,plain,
converse(one) = one,
inference(orient,[status(thm)],[t183]) ).
cnf(t86451,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t182,t192]) ).
cnf(t202,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t86451]) ).
cnf(t203,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t202]) ).
cnf(t206,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t54,t203]) ).
cnf(t86454,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t206,t192]) ).
cnf(t86455,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t86454,t203]) ).
cnf(t236,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t86455]) ).
cnf(t246,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t85,t236]) ).
cnf(t256,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t246]) ).
cnf(t266,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t85,t256]) ).
cnf(t1388,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t266]) ).
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(t13,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t18,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t45,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t18]) ).
cnf(t87066,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t45,t43]) ).
cnf(t87067,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t87066,t85]) ).
cnf(t87068,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t87067,t43]) ).
cnf(t14257,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t87068]) ).
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(t4,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t92,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t14258,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t14257,t92]) ).
cnf(t87177,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t14258,t85]) ).
cnf(t14877,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t87177]) ).
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(t10,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t46,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
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(t3,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t51,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t86,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t85,t51]) ).
cnf(t86444,plain,
zero = complement(top),
inference(step,[status(thm)],[t86,t92]) ).
cnf(t97,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t86444]) ).
cnf(t240,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t236,t97]) ).
cnf(t86456,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t240,t97]) ).
cnf(t86457,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t86456,t97]) ).
cnf(t247,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t86457]) ).
cnf(t248,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t46,t247]) ).
cnf(t269,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t248]) ).
cnf(t14882,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t269,t14877]) ).
cnf(t87179,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t14882,t14877]) ).
cnf(t14893,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t87179]) ).
cnf(t87184,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t14877,t14893]) ).
cnf(t14928,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t87184]) ).
cnf(t14961,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t14928]) ).
cnf(t87208,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1388,t14961]) ).
cnf(t14992,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t87208]) ).
cnf(t15554,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t14992]) ).
cnf(t237,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t236,t85]) ).
cnf(t86493,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t237,t85]) ).
cnf(t86494,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t86493,t85]) ).
cnf(t544,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t86494]) ).
cnf(t545,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t544,t106]) ).
cnf(t565,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t545]) ).
cnf(t14962,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t565,t14961]) ).
cnf(t87224,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t14962,t14961]) ).
cnf(t87225,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t87224,t14961]) ).
cnf(t15026,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t87225]) ).
cnf(t15032,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t46,t15026]) ).
cnf(t15073,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t15032]) ).
cnf(t15092,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t15073,t14257]) ).
cnf(t87227,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t15092,t14257]) ).
cnf(t87228,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t87227,t43]) ).
cnf(t15101,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t87228]) ).
cnf(t15103,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t15101,t106]) ).
cnf(t15129,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t15103]) ).
cnf(t15136,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t46,t15129]) ).
cnf(t19528,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t15136]) ).
cnf(t87244,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t14257,t15554]) ).
cnf(t15642,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t87244]) ).
cnf(t26034,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t15642]) ).
cnf(t26111,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t19528,t26034]) ).
cnf(t26302,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t26111]) ).
cnf(t26322,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t26302,t106]) ).
cnf(t26876,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t26322]) ).
cnf(t100,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t85,t97]) ).
cnf(t123,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t100]) ).
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(t8,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t60,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t63,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t60,t21]) ).
cnf(t311,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t63]) ).
cnf(t53,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t46,t51]) ).
cnf(t353,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t53]) ).
cnf(t264,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t51,t256]) ).
cnf(t280,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t264]) ).
cnf(t358,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t353,t280]) ).
cnf(t360,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t353,t236]) ).
cnf(t86465,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t360,t51]) ).
cnf(t373,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t86465]) ).
cnf(t374,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t373,t85]) ).
cnf(t386,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t374]) ).
cnf(t86467,plain,
top = join(X1,top),
inference(step,[status(thm)],[t358,t386]) ).
cnf(t391,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t86467]) ).
cnf(t392,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t391,t43]) ).
cnf(t397,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t392]) ).
cnf(t62,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t60,t21]) ).
cnf(t294,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t62]) ).
cnf(t296,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t294,t51]) ).
cnf(t335,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t296]) ).
cnf(t402,plain,
top = converse(top),
inference(cp,[status(thm)],[t397,t335]) ).
cnf(t405,plain,
converse(top) = top,
inference(orient,[status(thm)],[t402]) ).
cnf(t410,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t27,t405]) ).
cnf(t417,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t410]) ).
cnf(t423,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t311,t417]) ).
cnf(t12010,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t423]) ).
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(t11,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t24,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t30,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t24,t27]) ).
cnf(t1261,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t30]) ).
cnf(t12012,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t12010,t1261]) ).
cnf(t87015,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t12012,t21]) ).
cnf(t28,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t159,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t28]) ).
cnf(t87016,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t87015,t159]) ).
cnf(t87017,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t87016,t294]) ).
cnf(t87018,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t87017,t405]) ).
cnf(t87019,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t87018,t391]) ).
cnf(t12092,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t87019]) ).
cnf(t411,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t27,t405]) ).
cnf(t431,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t411]) ).
cnf(t419,plain,
converse(join(composition(X1,top),X2)) = join(composition(top,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t60,t417]) ).
cnf(t5391,plain,
join(composition(top,converse(X1)),converse(X2)) = converse(join(composition(X1,top),X2)),
inference(orient,[status(thm)],[t419]) ).
cnf(t5404,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(cp,[status(thm)],[t5391,t405]) ).
cnf(t5439,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(orient,[status(thm)],[t5404]) ).
cnf(t5443,plain,
join(composition(top,top),converse(composition(X1,top))) = converse(composition(join(top,X1),top)),
inference(cp,[status(thm)],[t5439,t24]) ).
cnf(t86780,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t5443,t417]) ).
cnf(t86781,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t86780,t417]) ).
cnf(t86782,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t86781,t397]) ).
cnf(t86783,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t86782,t405]) ).
cnf(t5565,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t86783]) ).
cnf(t5581,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t5565,t192]) ).
cnf(t86784,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t5581,t17]) ).
cnf(t86785,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t86784,t391]) ).
cnf(t5594,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t86785]) ).
cnf(t5599,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t5594]) ).
cnf(t86793,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t5599,t97]) ).
cnf(t86794,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t86793,t97]) ).
cnf(t86795,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t86794,t405]) ).
cnf(t86796,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t86795,t97]) ).
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(t16,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(t33,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)],[t16]) ).
cnf(t64,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t46,t60]) ).
cnf(t2656,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t64]) ).
cnf(t363,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t353,t43]) ).
cnf(t86483,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t363,t397]) ).
cnf(t456,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t86483]) ).
cnf(t2661,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t2656,t456]) ).
cnf(t86674,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t2661,t43]) ).
cnf(t2725,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t86674]) ).
cnf(t2765,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t2725,t60]) ).
cnf(t86675,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t2765,t21]) ).
cnf(t86676,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t86675,t21]) ).
cnf(t2778,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t86676]) ).
cnf(t2815,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t2778,t43]) ).
cnf(t2825,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t2815]) ).
cnf(t56,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t54,t17]) ).
cnf(t1465,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t56]) ).
cnf(t1475,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t1465,t21]) ).
cnf(t1493,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t1475]) ).
cnf(t2836,plain,
top = join(complement(composition(X1,complement(converse(X1)))),complement(one)),
inference(cp,[status(thm)],[t2825,t1493]) ).
cnf(t86690,plain,
top = join(complement(one),complement(composition(X1,complement(converse(X1))))),
inference(step,[status(thm)],[t2836,t43]) ).
cnf(t3322,plain,
join(complement(one),complement(composition(X1,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t86690]) ).
cnf(t3337,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t85,t3322]) ).
cnf(t86691,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t3337,t97]) ).
cnf(t3343,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t86691]) ).
cnf(t3364,plain,
composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(cp,[status(thm)],[t33,t3343]) ).
cnf(t86692,plain,
composition(meet(X1,composition(complement(X1),converse(one))),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t3364,t21]) ).
cnf(t86693,plain,
composition(meet(X1,composition(complement(X1),one)),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t86692,t192]) ).
cnf(t86694,plain,
composition(meet(X1,complement(X1)),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t86693,t17]) ).
cnf(t86695,plain,
composition(zero,meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t86694,t92]) ).
cnf(t86696,plain,
composition(zero,zero) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t86695,t3343]) ).
cnf(t86697,plain,
composition(zero,zero) = join(meet(X1,complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t86696,t17]) ).
cnf(t86698,plain,
composition(zero,zero) = join(meet(X1,complement(X1)),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t86697,t21]) ).
cnf(t86699,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t86698,t92]) ).
cnf(t86700,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),converse(one))),zero)),
inference(step,[status(thm)],[t86699,t21]) ).
cnf(t86701,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),one)),zero)),
inference(step,[status(thm)],[t86700,t192]) ).
cnf(t86702,plain,
composition(zero,zero) = join(zero,composition(meet(X1,complement(X1)),zero)),
inference(step,[status(thm)],[t86701,t17]) ).
cnf(t86703,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t86702,t92]) ).
cnf(t3365,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t86703]) ).
cnf(t3368,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(cp,[status(thm)],[t46,t3365]) ).
cnf(t3524,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(orient,[status(thm)],[t3368]) ).
cnf(t3532,plain,
join(composition(zero,zero),composition(X1,zero)) = join(zero,composition(join(zero,X1),zero)),
inference(cp,[status(thm)],[t3524,t24]) ).
cnf(t86716,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(zero,X1),zero)),
inference(step,[status(thm)],[t3532,t24]) ).
cnf(t3610,plain,
join(zero,composition(join(zero,X1),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t86716]) ).
cnf(t271,plain,
join(zero,X1) = join(zero,join(X1,zero)),
inference(cp,[status(thm)],[t269,t43]) ).
cnf(t272,plain,
join(zero,join(X1,zero)) = join(zero,X1),
inference(orient,[status(thm)],[t271]) ).
cnf(t275,plain,
join(zero,join(join(X1,zero),X2)) = join(join(zero,X1),X2),
inference(cp,[status(thm)],[t46,t272]) ).
cnf(t86546,plain,
join(zero,join(X1,join(zero,X2))) = join(join(zero,X1),X2),
inference(step,[status(thm)],[t275,t46]) ).
cnf(t86547,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(step,[status(thm)],[t86546,t46]) ).
cnf(t1597,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(orient,[status(thm)],[t86547]) ).
cnf(t52,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t51,t46]) ).
cnf(t577,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t52]) ).
cnf(t606,plain,
top = join(X1,join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t577,t43]) ).
cnf(t734,plain,
join(X1,join(X2,complement(join(X2,X1)))) = top,
inference(orient,[status(thm)],[t606]) ).
cnf(t193,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t60,t192]) ).
cnf(t209,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t193]) ).
fof(f16,conjecture,
! [X0] :
( join(X0,one) = one
=> meet(complement(composition(X0,top)),one) = meet(complement(X0),one) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0] :
( join(X0,one) = one
=> meet(complement(composition(X0,top)),one) = meet(complement(X0),one) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0] :
( meet(complement(composition(X0,top)),one) != meet(complement(X0),one)
& join(X0,one) = one ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( meet(complement(composition(sk0,top)),one) != meet(complement(sk0),one)
& join(sk0,one) = one ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[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(t83,plain,
join(sk0,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t84,plain,
join(sk0,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t46,t83]) ).
cnf(t118,plain,
join(sk0,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t84]) ).
cnf(t120,plain,
join(one,X1) = join(sk0,join(X1,one)),
inference(cp,[status(thm)],[t118,t43]) ).
cnf(t142,plain,
join(sk0,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t120]) ).
cnf(t356,plain,
join(top,one) = join(one,complement(sk0)),
inference(cp,[status(thm)],[t353,t142]) ).
cnf(t382,plain,
join(one,complement(sk0)) = join(top,one),
inference(orient,[status(thm)],[t356]) ).
cnf(t383,plain,
join(one,converse(complement(sk0))) = converse(join(top,one)),
inference(cp,[status(thm)],[t209,t382]) ).
cnf(t194,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t60,t192]) ).
cnf(t86452,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t194,t43]) ).
cnf(t220,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t86452]) ).
cnf(t86478,plain,
join(one,converse(complement(sk0))) = join(one,converse(top)),
inference(step,[status(thm)],[t383,t220]) ).
cnf(t86479,plain,
join(one,converse(complement(sk0))) = join(one,top),
inference(step,[status(thm)],[t86478,t405]) ).
cnf(t86480,plain,
join(one,converse(complement(sk0))) = top,
inference(step,[status(thm)],[t86479,t391]) ).
cnf(t443,plain,
join(one,converse(complement(sk0))) = top,
inference(orient,[status(thm)],[t86480]) ).
cnf(t444,plain,
join(one,join(converse(complement(sk0)),X1)) = join(top,X1),
inference(cp,[status(thm)],[t46,t443]) ).
cnf(t86484,plain,
join(one,join(converse(complement(sk0)),X1)) = top,
inference(step,[status(thm)],[t444,t397]) ).
cnf(t471,plain,
join(one,join(converse(complement(sk0)),X1)) = top,
inference(orient,[status(thm)],[t86484]) ).
cnf(t765,plain,
top = join(join(converse(complement(sk0)),X1),join(one,complement(top))),
inference(cp,[status(thm)],[t734,t471]) ).
cnf(t86595,plain,
top = join(converse(complement(sk0)),join(X1,join(one,complement(top)))),
inference(step,[status(thm)],[t765,t46]) ).
cnf(t86596,plain,
top = join(converse(complement(sk0)),join(X1,join(one,zero))),
inference(step,[status(thm)],[t86595,t97]) ).
cnf(t86597,plain,
top = join(converse(complement(sk0)),join(X1,join(zero,one))),
inference(step,[status(thm)],[t86596,t43]) ).
cnf(t2215,plain,
join(converse(complement(sk0)),join(X1,join(zero,one))) = top,
inference(orient,[status(thm)],[t86597]) ).
cnf(t2219,plain,
top = join(converse(complement(sk0)),join(join(zero,one),X1)),
inference(cp,[status(thm)],[t2215,t43]) ).
cnf(t86637,plain,
top = join(converse(complement(sk0)),join(zero,join(one,X1))),
inference(step,[status(thm)],[t2219,t46]) ).
cnf(t2464,plain,
join(converse(complement(sk0)),join(zero,join(one,X1))) = top,
inference(orient,[status(thm)],[t86637]) ).
cnf(t2468,plain,
join(zero,join(converse(complement(sk0)),join(one,X1))) = join(zero,top),
inference(cp,[status(thm)],[t1597,t2464]) ).
cnf(t99,plain,
top = join(top,zero),
inference(cp,[status(thm)],[t51,t97]) ).
cnf(t86445,plain,
top = join(zero,top),
inference(step,[status(thm)],[t99,t43]) ).
cnf(t104,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t86445]) ).
cnf(t86649,plain,
join(zero,join(converse(complement(sk0)),join(one,X1))) = top,
inference(step,[status(thm)],[t2468,t104]) ).
cnf(t2519,plain,
join(zero,join(converse(complement(sk0)),join(one,X1))) = top,
inference(orient,[status(thm)],[t86649]) ).
cnf(t3613,plain,
composition(join(zero,join(converse(complement(sk0)),join(one,X1))),zero) = join(zero,composition(top,zero)),
inference(cp,[status(thm)],[t3610,t2519]) ).
cnf(t86717,plain,
composition(top,zero) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t3613,t2519]) ).
cnf(t3644,plain,
join(zero,composition(top,zero)) = composition(top,zero),
inference(orient,[status(thm)],[t86717]) ).
cnf(t86797,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t86796,t3644]) ).
cnf(t5611,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t86797]) ).
cnf(t5612,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t431,t5611]) ).
cnf(t5635,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t5612]) ).
cnf(t12144,plain,
composition(converse(zero),top) = join(composition(converse(zero),X1),converse(zero)),
inference(cp,[status(thm)],[t12092,t5635]) ).
cnf(t87046,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t12144,t5635]) ).
cnf(t87047,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t87046,t43]) ).
cnf(t13339,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t87047]) ).
cnf(t3633,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(X1,zero),zero)),
inference(cp,[status(thm)],[t3610,t43]) ).
cnf(t3699,plain,
join(zero,composition(join(X1,zero),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t3633]) ).
cnf(t5613,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t24,t5611]) ).
cnf(t86804,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t5613,t397]) ).
cnf(t86805,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t86804,t5611]) ).
cnf(t5660,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t86805]) ).
cnf(t86808,plain,
zero = composition(join(zero,X1),zero),
inference(step,[status(thm)],[t3699,t5660]) ).
cnf(t5679,plain,
zero = composition(join(zero,X1),zero),
inference(rw,[status(thm)],[t86808]) ).
cnf(t5724,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t5679]) ).
cnf(t5727,plain,
zero = composition(join(X1,zero),zero),
inference(cp,[status(thm)],[t5724,t43]) ).
cnf(t5747,plain,
composition(join(X1,zero),zero) = zero,
inference(orient,[status(thm)],[t5727]) ).
cnf(t5749,plain,
composition(join(join(X1,zero),X2),zero) = join(zero,composition(X2,zero)),
inference(cp,[status(thm)],[t24,t5747]) ).
cnf(t86831,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t5749,t46]) ).
cnf(t86832,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t86831,t5660]) ).
cnf(t5958,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t86832]) ).
cnf(t215,plain,
composition(converse(X1),join(one,X2)) = converse(composition(join(one,converse(X2)),X1)),
inference(cp,[status(thm)],[t169,t209]) ).
cnf(t5136,plain,
converse(composition(join(one,converse(X1)),X2)) = composition(converse(X2),join(one,X1)),
inference(orient,[status(thm)],[t215]) ).
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(t9,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t22,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t26,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t24,t22]) ).
cnf(t674,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t5597,plain,
composition(join(X1,composition(X2,top)),top) = join(composition(X1,top),composition(X2,top)),
inference(cp,[status(thm)],[t674,t5594]) ).
cnf(t86923,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(step,[status(thm)],[t5597,t24]) ).
cnf(t7819,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(orient,[status(thm)],[t86923]) ).
cnf(t7831,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t7819,t203]) ).
cnf(t86924,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t7831,t391]) ).
cnf(t86925,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t86924,t5594]) ).
cnf(t7860,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t86925]) ).
cnf(t7862,plain,
top = composition(join(one,X1),top),
inference(cp,[status(thm)],[t7860,t43]) ).
cnf(t7889,plain,
composition(join(one,X1),top) = top,
inference(orient,[status(thm)],[t7862]) ).
cnf(t7901,plain,
composition(converse(top),join(one,X1)) = converse(top),
inference(cp,[status(thm)],[t5136,t7889]) ).
cnf(t86928,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t7901,t405]) ).
cnf(t86929,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t86928,t405]) ).
cnf(t7935,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t86929]) ).
cnf(t7936,plain,
top = composition(top,join(X1,one)),
inference(cp,[status(thm)],[t7935,t43]) ).
cnf(t7956,plain,
composition(top,join(X1,one)) = top,
inference(orient,[status(thm)],[t7936]) ).
cnf(t7963,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t7956]) ).
cnf(t86948,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t7963,t405]) ).
cnf(t86949,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t86948,t43]) ).
cnf(t86950,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t86949,t97]) ).
cnf(t86951,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t86950,t5611]) ).
cnf(t8643,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t86951]) ).
cnf(t8652,plain,
zero = composition(join(X1,complement(join(X2,one))),zero),
inference(cp,[status(thm)],[t5958,t8643]) ).
cnf(t8943,plain,
composition(join(X1,complement(join(X2,one))),zero) = zero,
inference(orient,[status(thm)],[t8652]) ).
cnf(t14451,plain,
zero = composition(X1,zero),
inference(cp,[status(thm)],[t8943,t14257]) ).
cnf(t14456,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t14451]) ).
cnf(t14463,plain,
converse(zero) = join(converse(zero),zero),
inference(cp,[status(thm)],[t13339,t14456]) ).
cnf(t87111,plain,
converse(zero) = join(zero,converse(zero)),
inference(step,[status(thm)],[t14463,t43]) ).
cnf(t14611,plain,
join(zero,converse(zero)) = converse(zero),
inference(orient,[status(thm)],[t87111]) ).
cnf(t14618,plain,
join(converse(zero),zero) = converse(converse(zero)),
inference(cp,[status(thm)],[t311,t14611]) ).
cnf(t87112,plain,
join(zero,converse(zero)) = converse(converse(zero)),
inference(step,[status(thm)],[t14618,t43]) ).
cnf(t87113,plain,
converse(zero) = converse(converse(zero)),
inference(step,[status(thm)],[t87112,t14611]) ).
cnf(t87114,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t87113,t21]) ).
cnf(t14621,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t87114]) ).
cnf(t14624,plain,
converse(composition(X1,zero)) = composition(zero,converse(X1)),
inference(cp,[status(thm)],[t27,t14621]) ).
cnf(t87148,plain,
converse(zero) = composition(zero,converse(X1)),
inference(step,[status(thm)],[t14624,t14456]) ).
cnf(t87149,plain,
zero = composition(zero,converse(X1)),
inference(step,[status(thm)],[t87148,t14621]) ).
cnf(t14706,plain,
composition(zero,converse(X1)) = zero,
inference(orient,[status(thm)],[t87149]) ).
cnf(t14723,plain,
zero = composition(zero,X1),
inference(cp,[status(thm)],[t14706,t21]) ).
cnf(t14744,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t14723]) ).
cnf(t14755,plain,
complement(X1) = join(complement(X1),composition(converse(zero),complement(zero))),
inference(cp,[status(thm)],[t54,t14744]) ).
cnf(t87150,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t14755,t14621]) ).
cnf(t87151,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t87150,t14744]) ).
cnf(t87152,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t87151,t43]) ).
cnf(t14757,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t87152]) ).
cnf(t87165,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t123,t14757]) ).
cnf(t14800,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t87165]) ).
cnf(t14801,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t14800]) ).
cnf(t14899,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t14893,t43]) ).
cnf(t14946,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t14899]) ).
cnf(t14955,plain,
X1 = join(meet(X1,zero),complement(complement(X1))),
inference(cp,[status(thm)],[t14257,t14946]) ).
cnf(t2877,plain,
join(complement(X1),join(join(X2,X1),X3)) = join(top,X3),
inference(cp,[status(thm)],[t46,t2825]) ).
cnf(t86685,plain,
join(complement(X1),join(X2,join(X1,X3))) = join(top,X3),
inference(step,[status(thm)],[t2877,t46]) ).
cnf(t86686,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(step,[status(thm)],[t86685,t397]) ).
cnf(t3178,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(orient,[status(thm)],[t86686]) ).
cnf(t8653,plain,
top = join(complement(zero),join(X1,complement(join(X2,one)))),
inference(cp,[status(thm)],[t3178,t8643]) ).
cnf(t11047,plain,
join(complement(zero),join(X1,complement(join(X2,one)))) = top,
inference(orient,[status(thm)],[t8653]) ).
cnf(t14450,plain,
top = join(complement(zero),X1),
inference(cp,[status(thm)],[t11047,t14257]) ).
cnf(t14513,plain,
join(complement(zero),X1) = top,
inference(orient,[status(thm)],[t14450]) ).
cnf(t14514,plain,
top = complement(zero),
inference(cp,[status(thm)],[t14513,t54]) ).
cnf(t14553,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t14514]) ).
cnf(t14558,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t85,t14553]) ).
cnf(t87108,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t14558,t391]) ).
cnf(t87109,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t87108,t97]) ).
cnf(t14600,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t87109]) ).
cnf(t87211,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t14955,t14600]) ).
cnf(t87212,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t87211,t14757]) ).
cnf(t87213,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t87212,t14801]) ).
cnf(t14995,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t87213]) ).
cnf(t87214,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t14801,t14995]) ).
cnf(t14996,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t87214]) ).
cnf(t26899,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t26876,t14996]) ).
cnf(t28391,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t26899]) ).
cnf(t39,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)],[t33,t21]) ).
cnf(t86955,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)],[t39,t21]) ).
cnf(t9032,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)],[t86955]) ).
cnf(t3353,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t3343,t21]) ).
cnf(t3378,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t3353]) ).
cnf(t3397,plain,
zero = meet(one,composition(converse(complement(X1)),meet(X1,X1))),
inference(cp,[status(thm)],[t3378,t256]) ).
cnf(t4326,plain,
meet(one,composition(converse(complement(X1)),meet(X1,X1))) = zero,
inference(orient,[status(thm)],[t3397]) ).
cnf(t87210,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(step,[status(thm)],[t4326,t14961]) ).
cnf(t14994,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(rw,[status(thm)],[t87210]) ).
cnf(t16927,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t14994]) ).
cnf(t16942,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)],[t9032,t16927]) ).
cnf(t87265,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)],[t16942,t16927]) ).
cnf(t87266,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)],[t87265,t14744]) ).
cnf(t87267,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)],[t87266,t106]) ).
cnf(t87268,plain,
zero = join(meet(converse(complement(X1)),converse(X1)),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t87267,t203]) ).
cnf(t87269,plain,
zero = join(meet(converse(X1),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t87268,t106]) ).
cnf(t87270,plain,
zero = join(meet(converse(X1),converse(complement(X1))),zero),
inference(step,[status(thm)],[t87269,t14744]) ).
cnf(t87271,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(step,[status(thm)],[t87270,t14946]) ).
cnf(t16973,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t87271]) ).
cnf(t28466,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t28391,t16973]) ).
cnf(t87506,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t28466,t43]) ).
cnf(t87507,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t87506,t14946]) ).
cnf(t29844,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t87507]) ).
cnf(t29849,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t29844,t14996]) ).
cnf(t86476,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t335,t405]) ).
cnf(t408,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t86476]) ).
cnf(t15595,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t15554,t408]) ).
cnf(t87453,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(step,[status(thm)],[t15595,t97]) ).
cnf(t26018,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(orient,[status(thm)],[t87453]) ).
cnf(t26884,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t26876,t26018]) ).
cnf(t87474,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t26884,t14996]) ).
cnf(t87475,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t87474,t14946]) ).
cnf(t27421,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t87475]) ).
cnf(t27440,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t27421,t21]) ).
cnf(t29451,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t27440]) ).
cnf(t87508,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t29849,t29451]) ).
cnf(t29895,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t87508]) ).
cnf(t29900,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t29895,t14996]) ).
cnf(t29962,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t29900]) ).
cnf(t29976,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(cp,[status(thm)],[t29962,t294]) ).
cnf(t30874,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(orient,[status(thm)],[t29976]) ).
cnf(t125,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t123,t85]) ).
cnf(t4591,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t125]) ).
cnf(t87180,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t4591,t14893]) ).
cnf(t14894,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t87180]) ).
cnf(t87220,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t14894,t14995]) ).
cnf(t15023,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t87220]) ).
cnf(t16309,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t15023]) ).
cnf(t29989,plain,
complement(meet(converse(X1),X2)) = join(converse(complement(X1)),complement(X2)),
inference(cp,[status(thm)],[t16309,t29962]) ).
cnf(t31445,plain,
join(converse(complement(X1)),complement(X2)) = complement(meet(converse(X1),X2)),
inference(orient,[status(thm)],[t29989]) ).
cnf(t31492,plain,
complement(join(complement(X1),converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(cp,[status(thm)],[t30874,t31445]) ).
cnf(t87553,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t31492,t15554]) ).
cnf(t87554,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t87553,t29895]) ).
cnf(t87555,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t87554,t14996]) ).
cnf(t31513,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t87555]) ).
cnf(t31526,plain,
meet(X1,converse(X2)) = converse(meet(X2,converse(X1))),
inference(cp,[status(thm)],[t31513,t106]) ).
cnf(t31631,plain,
converse(meet(X1,converse(X2))) = meet(X2,converse(X1)),
inference(orient,[status(thm)],[t31526]) ).
cnf(t15599,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t15554,t14996]) ).
cnf(t16371,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t15599]) ).
cnf(t16378,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t15129,t16371]) ).
cnf(t87253,plain,
complement(X1) = complement(meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t16378,t16309]) ).
cnf(t16475,plain,
complement(meet(X1,join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t87253]) ).
cnf(t16522,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t14996,t16475]) ).
cnf(t87254,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t16522,t14996]) ).
cnf(t16552,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t87254]) ).
cnf(t16590,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t16552,t43]) ).
cnf(t16622,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t16590]) ).
cnf(t47,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t46,t43]) ).
cnf(t15758,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t47]) ).
cnf(t16652,plain,
X1 = meet(X1,join(X2,join(X1,X3))),
inference(cp,[status(thm)],[t16622,t15758]) ).
cnf(t17553,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t16652]) ).
cnf(t19615,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(cp,[status(thm)],[t17553,t19528]) ).
cnf(t22093,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t19615]) ).
cnf(t34,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)],[t33,t17]) ).
cnf(t86708,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)],[t34,t192]) ).
cnf(t86709,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)],[t86708,t17]) ).
cnf(t86710,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)],[t86709,t192]) ).
cnf(t86711,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)],[t86710,t17]) ).
cnf(t3445,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)],[t86711]) ).
cnf(t16638,plain,
sk0 = meet(sk0,one),
inference(cp,[status(thm)],[t16622,t83]) ).
cnf(t16669,plain,
meet(sk0,one) = sk0,
inference(orient,[status(thm)],[t16638]) ).
cnf(t16680,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)],[t3445,t16669]) ).
cnf(t87335,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)],[t16680,t16669]) ).
cnf(t87336,plain,
composition(sk0,meet(one,converse(sk0))) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t87335,t17]) ).
cnf(t221,plain,
join(one,converse(sk0)) = converse(one),
inference(cp,[status(thm)],[t220,t83]) ).
cnf(t86453,plain,
join(one,converse(sk0)) = one,
inference(step,[status(thm)],[t221,t192]) ).
cnf(t233,plain,
join(one,converse(sk0)) = one,
inference(orient,[status(thm)],[t86453]) ).
cnf(t16577,plain,
converse(sk0) = meet(converse(sk0),one),
inference(cp,[status(thm)],[t16552,t233]) ).
cnf(t87255,plain,
converse(sk0) = meet(one,converse(sk0)),
inference(step,[status(thm)],[t16577,t106]) ).
cnf(t16609,plain,
meet(one,converse(sk0)) = converse(sk0),
inference(orient,[status(thm)],[t87255]) ).
cnf(t87337,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t87336,t16609]) ).
cnf(t87338,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t87337,t16669]) ).
cnf(t87339,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,meet(one,converse(sk0)))),
inference(step,[status(thm)],[t87338,t17]) ).
cnf(t87340,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,converse(sk0))),
inference(step,[status(thm)],[t87339,t16609]) ).
cnf(t18589,plain,
join(sk0,composition(sk0,converse(sk0))) = composition(sk0,converse(sk0)),
inference(orient,[status(thm)],[t87340]) ).
cnf(t18590,plain,
sk0 = meet(sk0,composition(sk0,converse(sk0))),
inference(cp,[status(thm)],[t16622,t18589]) ).
cnf(t18604,plain,
meet(sk0,composition(sk0,converse(sk0))) = sk0,
inference(orient,[status(thm)],[t18590]) ).
cnf(t22112,plain,
meet(sk0,composition(sk0,converse(sk0))) = meet(sk0,join(composition(sk0,converse(sk0)),X1)),
inference(cp,[status(thm)],[t22093,t18604]) ).
cnf(t87666,plain,
sk0 = meet(sk0,join(composition(sk0,converse(sk0)),X1)),
inference(step,[status(thm)],[t22112,t18604]) ).
cnf(t38372,plain,
meet(sk0,join(composition(sk0,converse(sk0)),X1)) = sk0,
inference(orient,[status(thm)],[t87666]) ).
cnf(t38375,plain,
sk0 = meet(sk0,composition(join(sk0,X1),converse(sk0))),
inference(cp,[status(thm)],[t38372,t24]) ).
cnf(t46857,plain,
meet(sk0,composition(join(sk0,X1),converse(sk0))) = sk0,
inference(orient,[status(thm)],[t38375]) ).
cnf(t46860,plain,
sk0 = meet(sk0,composition(one,converse(sk0))),
inference(cp,[status(thm)],[t46857,t83]) ).
cnf(t87842,plain,
sk0 = meet(sk0,converse(sk0)),
inference(step,[status(thm)],[t46860,t203]) ).
cnf(t46960,plain,
meet(sk0,converse(sk0)) = sk0,
inference(orient,[status(thm)],[t87842]) ).
cnf(t47025,plain,
meet(sk0,converse(sk0)) = converse(sk0),
inference(cp,[status(thm)],[t31631,t46960]) ).
cnf(t87843,plain,
sk0 = converse(sk0),
inference(step,[status(thm)],[t47025,t46960]) ).
cnf(t47049,plain,
converse(sk0) = sk0,
inference(orient,[status(thm)],[t87843]) ).
cnf(t47057,plain,
converse(composition(X1,sk0)) = composition(sk0,converse(X1)),
inference(cp,[status(thm)],[t27,t47049]) ).
cnf(t47707,plain,
converse(composition(X1,sk0)) = composition(sk0,converse(X1)),
inference(orient,[status(thm)],[t47057]) ).
cnf(t26082,plain,
X1 = join(meet(X2,X1),meet(X1,complement(X2))),
inference(cp,[status(thm)],[t26034,t106]) ).
cnf(t41289,plain,
join(meet(X1,X2),meet(X2,complement(X1))) = X2,
inference(orient,[status(thm)],[t26082]) ).
cnf(t41485,plain,
X1 = join(meet(X2,X1),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t41289,t106]) ).
cnf(t51037,plain,
join(meet(X1,X2),meet(complement(X1),X2)) = X2,
inference(orient,[status(thm)],[t41485]) ).
cnf(t15557,plain,
meet(X1,complement(join(X2,X1))) = complement(top),
inference(cp,[status(thm)],[t15554,t2825]) ).
cnf(t87246,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(step,[status(thm)],[t15557,t97]) ).
cnf(t15653,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t87246]) ).
cnf(t15109,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t46,t15101]) ).
cnf(t19043,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t15109]) ).
cnf(t19069,plain,
join(X1,meet(X2,meet(X1,X3))) = join(X1,meet(X1,X3)),
inference(cp,[status(thm)],[t19043,t15129]) ).
cnf(t87348,plain,
join(X1,meet(X2,meet(X1,X3))) = X1,
inference(step,[status(thm)],[t19069,t15101]) ).
cnf(t19180,plain,
join(X1,meet(X2,meet(X1,X3))) = X1,
inference(orient,[status(thm)],[t87348]) ).
cnf(t16555,plain,
meet(X1,X2) = meet(meet(X1,X2),X2),
inference(cp,[status(thm)],[t16552,t15129]) ).
cnf(t87257,plain,
meet(X1,X2) = meet(X2,meet(X1,X2)),
inference(step,[status(thm)],[t16555,t106]) ).
cnf(t16787,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t87257]) ).
cnf(t19182,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t19180,t16787]) ).
cnf(t19331,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t19182]) ).
cnf(t19372,plain,
zero = meet(meet(X1,meet(X2,X3)),complement(X3)),
inference(cp,[status(thm)],[t15653,t19331]) ).
cnf(t87644,plain,
zero = meet(complement(X3),meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t19372,t106]) ).
cnf(t35989,plain,
meet(complement(X1),meet(X2,meet(X3,X1))) = zero,
inference(orient,[status(thm)],[t87644]) ).
cnf(t41,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)],[t33,t17]) ).
cnf(t86997,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)],[t41,t203]) ).
cnf(t86998,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)],[t86997,t17]) ).
cnf(t86999,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)],[t86998,t106]) ).
cnf(t87000,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)],[t86999,t203]) ).
cnf(t10173,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)],[t87000]) ).
cnf(t16998,plain,
composition(meet(complement(X1),converse(converse(X1))),meet(converse(X1),converse(complement(X1)))) = join(meet(one,composition(complement(X1),converse(X1))),composition(meet(complement(X1),converse(converse(X1))),zero)),
inference(cp,[status(thm)],[t10173,t16973]) ).
cnf(t87303,plain,
composition(meet(complement(X1),X1),meet(converse(X1),converse(complement(X1)))) = join(meet(one,composition(complement(X1),converse(X1))),composition(meet(complement(X1),converse(converse(X1))),zero)),
inference(step,[status(thm)],[t16998,t21]) ).
cnf(t87304,plain,
composition(meet(X1,complement(X1)),meet(converse(X1),converse(complement(X1)))) = join(meet(one,composition(complement(X1),converse(X1))),composition(meet(complement(X1),converse(converse(X1))),zero)),
inference(step,[status(thm)],[t87303,t106]) ).
cnf(t87305,plain,
composition(zero,meet(converse(X1),converse(complement(X1)))) = join(meet(one,composition(complement(X1),converse(X1))),composition(meet(complement(X1),converse(converse(X1))),zero)),
inference(step,[status(thm)],[t87304,t92]) ).
cnf(t87306,plain,
zero = join(meet(one,composition(complement(X1),converse(X1))),composition(meet(complement(X1),converse(converse(X1))),zero)),
inference(step,[status(thm)],[t87305,t14744]) ).
cnf(t87307,plain,
zero = join(meet(one,composition(complement(X1),converse(X1))),zero),
inference(step,[status(thm)],[t87306,t14456]) ).
cnf(t87308,plain,
zero = meet(one,composition(complement(X1),converse(X1))),
inference(step,[status(thm)],[t87307,t14946]) ).
cnf(t17788,plain,
meet(one,composition(complement(X1),converse(X1))) = zero,
inference(orient,[status(thm)],[t87308]) ).
cnf(t26074,plain,
one = join(zero,meet(one,complement(composition(complement(X1),converse(X1))))),
inference(cp,[status(thm)],[t26034,t17788]) ).
cnf(t87676,plain,
one = meet(one,complement(composition(complement(X1),converse(X1)))),
inference(step,[status(thm)],[t26074,t14893]) ).
cnf(t41120,plain,
meet(one,complement(composition(complement(X1),converse(X1)))) = one,
inference(orient,[status(thm)],[t87676]) ).
cnf(t47096,plain,
one = meet(one,complement(composition(complement(sk0),sk0))),
inference(cp,[status(thm)],[t41120,t47049]) ).
cnf(t49719,plain,
meet(one,complement(composition(complement(sk0),sk0))) = one,
inference(orient,[status(thm)],[t47096]) ).
cnf(t49770,plain,
zero = meet(complement(complement(composition(complement(sk0),sk0))),meet(X1,one)),
inference(cp,[status(thm)],[t35989,t49719]) ).
cnf(t87979,plain,
zero = meet(composition(complement(sk0),sk0),meet(X1,one)),
inference(step,[status(thm)],[t49770,t14996]) ).
cnf(t54926,plain,
meet(composition(complement(sk0),sk0),meet(X1,one)) = zero,
inference(orient,[status(thm)],[t87979]) ).
cnf(t54928,plain,
zero = meet(meet(X1,one),composition(complement(sk0),sk0)),
inference(cp,[status(thm)],[t54926,t106]) ).
cnf(t56736,plain,
meet(meet(X1,one),composition(complement(sk0),sk0)) = zero,
inference(orient,[status(thm)],[t54928]) ).
cnf(t56747,plain,
composition(meet(meet(X1,one),composition(complement(sk0),sk0)),meet(converse(sk0),composition(converse(meet(X1,one)),complement(sk0)))) = join(meet(composition(meet(X1,one),converse(sk0)),complement(sk0)),composition(zero,meet(converse(sk0),composition(converse(meet(X1,one)),complement(sk0))))),
inference(cp,[status(thm)],[t9032,t56736]) ).
cnf(t88169,plain,
composition(zero,meet(converse(sk0),composition(converse(meet(X1,one)),complement(sk0)))) = join(meet(composition(meet(X1,one),converse(sk0)),complement(sk0)),composition(zero,meet(converse(sk0),composition(converse(meet(X1,one)),complement(sk0))))),
inference(step,[status(thm)],[t56747,t56736]) ).
cnf(t88170,plain,
zero = join(meet(composition(meet(X1,one),converse(sk0)),complement(sk0)),composition(zero,meet(converse(sk0),composition(converse(meet(X1,one)),complement(sk0))))),
inference(step,[status(thm)],[t88169,t14744]) ).
cnf(t88171,plain,
zero = join(meet(complement(sk0),composition(meet(X1,one),converse(sk0))),composition(zero,meet(converse(sk0),composition(converse(meet(X1,one)),complement(sk0))))),
inference(step,[status(thm)],[t88170,t106]) ).
cnf(t88172,plain,
zero = join(meet(complement(sk0),composition(meet(X1,one),sk0)),composition(zero,meet(converse(sk0),composition(converse(meet(X1,one)),complement(sk0))))),
inference(step,[status(thm)],[t88171,t47049]) ).
cnf(t88173,plain,
zero = join(meet(complement(sk0),composition(meet(X1,one),sk0)),zero),
inference(step,[status(thm)],[t88172,t14744]) ).
cnf(t88174,plain,
zero = meet(complement(sk0),composition(meet(X1,one),sk0)),
inference(step,[status(thm)],[t88173,t14946]) ).
cnf(t57524,plain,
meet(complement(sk0),composition(meet(X1,one),sk0)) = zero,
inference(orient,[status(thm)],[t88174]) ).
cnf(t57533,plain,
composition(meet(X1,one),sk0) = join(zero,meet(complement(complement(sk0)),composition(meet(X1,one),sk0))),
inference(cp,[status(thm)],[t51037,t57524]) ).
cnf(t88542,plain,
composition(meet(X1,one),sk0) = meet(complement(complement(sk0)),composition(meet(X1,one),sk0)),
inference(step,[status(thm)],[t57533,t14893]) ).
cnf(t88543,plain,
composition(meet(X1,one),sk0) = meet(sk0,composition(meet(X1,one),sk0)),
inference(step,[status(thm)],[t88542,t14996]) ).
cnf(t85920,plain,
meet(sk0,composition(meet(X1,one),sk0)) = composition(meet(X1,one),sk0),
inference(orient,[status(thm)],[t88543]) ).
cnf(t26321,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t26302,t16371]) ).
cnf(t27674,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t26321]) ).
cnf(t27870,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t15554,t27674]) ).
cnf(t87478,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t27870,t14996]) ).
cnf(t87479,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t87478,t85]) ).
cnf(t27891,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t87479]) ).
cnf(t27917,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t27891,t43]) ).
cnf(t27960,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t27917]) ).
cnf(t19068,plain,
join(X1,meet(meet(X1,X2),X3)) = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t19043,t15101]) ).
cnf(t87347,plain,
join(X1,meet(meet(X1,X2),X3)) = X1,
inference(step,[status(thm)],[t19068,t15101]) ).
cnf(t19135,plain,
join(X1,meet(meet(X1,X2),X3)) = X1,
inference(orient,[status(thm)],[t87347]) ).
cnf(t27978,plain,
meet(X1,meet(meet(complement(X1),X2),X3)) = meet(X1,complement(X1)),
inference(cp,[status(thm)],[t27960,t19135]) ).
cnf(t87685,plain,
meet(X1,meet(meet(complement(X1),X2),X3)) = zero,
inference(step,[status(thm)],[t27978,t92]) ).
cnf(t42107,plain,
meet(X1,meet(meet(complement(X1),X2),X3)) = zero,
inference(orient,[status(thm)],[t87685]) ).
cnf(t28001,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X1,X2)),
inference(cp,[status(thm)],[t27960,t14996]) ).
cnf(t28877,plain,
meet(complement(X1),join(X1,X2)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t28001]) ).
cnf(t472,plain,
top = join(one,converse(join(complement(sk0),X1))),
inference(cp,[status(thm)],[t471,t60]) ).
cnf(t487,plain,
join(one,converse(join(complement(sk0),X1))) = top,
inference(orient,[status(thm)],[t472]) ).
cnf(t489,plain,
join(one,converse(converse(join(complement(sk0),X1)))) = converse(top),
inference(cp,[status(thm)],[t209,t487]) ).
cnf(t86488,plain,
join(one,join(complement(sk0),X1)) = converse(top),
inference(step,[status(thm)],[t489,t21]) ).
cnf(t86489,plain,
join(one,join(complement(sk0),X1)) = top,
inference(step,[status(thm)],[t86488,t405]) ).
cnf(t492,plain,
join(one,join(complement(sk0),X1)) = top,
inference(orient,[status(thm)],[t86489]) ).
cnf(t27791,plain,
join(join(complement(sk0),X1),complement(one)) = join(join(complement(sk0),X1),complement(top)),
inference(cp,[status(thm)],[t27674,t492]) ).
cnf(t88270,plain,
join(complement(sk0),join(X1,complement(one))) = join(join(complement(sk0),X1),complement(top)),
inference(step,[status(thm)],[t27791,t46]) ).
cnf(t88271,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),join(X1,complement(top))),
inference(step,[status(thm)],[t88270,t46]) ).
cnf(t88272,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(top),join(complement(sk0),X1)),
inference(step,[status(thm)],[t88271,t15758]) ).
cnf(t88273,plain,
join(complement(sk0),join(X1,complement(one))) = join(zero,join(complement(sk0),X1)),
inference(step,[status(thm)],[t88272,t97]) ).
cnf(t88274,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),X1),
inference(step,[status(thm)],[t88273,t14893]) ).
cnf(t59707,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),X1),
inference(orient,[status(thm)],[t88274]) ).
cnf(t59716,plain,
meet(complement(complement(sk0)),join(X1,complement(one))) = meet(complement(complement(sk0)),join(complement(sk0),X1)),
inference(cp,[status(thm)],[t28877,t59707]) ).
cnf(t88275,plain,
meet(sk0,join(X1,complement(one))) = meet(complement(complement(sk0)),join(complement(sk0),X1)),
inference(step,[status(thm)],[t59716,t14996]) ).
cnf(t88276,plain,
meet(sk0,join(X1,complement(one))) = meet(complement(complement(sk0)),X1),
inference(step,[status(thm)],[t88275,t28877]) ).
cnf(t88277,plain,
meet(sk0,join(X1,complement(one))) = meet(sk0,X1),
inference(step,[status(thm)],[t88276,t14996]) ).
cnf(t59756,plain,
meet(sk0,join(X1,complement(one))) = meet(sk0,X1),
inference(orient,[status(thm)],[t88277]) ).
cnf(t59760,plain,
meet(sk0,X1) = meet(sk0,join(complement(one),X1)),
inference(cp,[status(thm)],[t59756,t43]) ).
cnf(t59812,plain,
meet(sk0,join(complement(one),X1)) = meet(sk0,X1),
inference(orient,[status(thm)],[t59760]) ).
cnf(t59813,plain,
meet(sk0,composition(converse(X1),complement(X1))) = meet(sk0,complement(one)),
inference(cp,[status(thm)],[t59812,t1465]) ).
cnf(t15558,plain,
meet(X1,complement(join(X1,X2))) = complement(top),
inference(cp,[status(thm)],[t15554,t2778]) ).
cnf(t87247,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(step,[status(thm)],[t15558,t97]) ).
cnf(t15703,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(orient,[status(thm)],[t87247]) ).
cnf(t15718,plain,
zero = meet(sk0,complement(one)),
inference(cp,[status(thm)],[t15703,t83]) ).
cnf(t15738,plain,
meet(sk0,complement(one)) = zero,
inference(orient,[status(thm)],[t15718]) ).
cnf(t88280,plain,
meet(sk0,composition(converse(X1),complement(X1))) = zero,
inference(step,[status(thm)],[t59813,t15738]) ).
cnf(t60035,plain,
meet(sk0,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t88280]) ).
cnf(t60129,plain,
composition(meet(X1,composition(complement(X1),converse(sk0))),meet(sk0,composition(converse(X1),complement(X1)))) = join(meet(composition(X1,sk0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(cp,[status(thm)],[t33,t60035]) ).
cnf(t88281,plain,
composition(meet(X1,composition(complement(X1),sk0)),meet(sk0,composition(converse(X1),complement(X1)))) = join(meet(composition(X1,sk0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(step,[status(thm)],[t60129,t47049]) ).
cnf(t88282,plain,
composition(meet(X1,composition(complement(X1),sk0)),zero) = join(meet(composition(X1,sk0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(step,[status(thm)],[t88281,t60035]) ).
cnf(t88283,plain,
zero = join(meet(composition(X1,sk0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(step,[status(thm)],[t88282,t14456]) ).
cnf(t88284,plain,
zero = join(meet(complement(X1),composition(X1,sk0)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(step,[status(thm)],[t88283,t106]) ).
cnf(t88285,plain,
zero = join(meet(complement(X1),composition(X1,sk0)),zero),
inference(step,[status(thm)],[t88284,t14456]) ).
cnf(t88286,plain,
zero = meet(complement(X1),composition(X1,sk0)),
inference(step,[status(thm)],[t88285,t14946]) ).
cnf(t60137,plain,
meet(complement(X1),composition(X1,sk0)) = zero,
inference(orient,[status(thm)],[t88286]) ).
cnf(t60171,plain,
composition(X1,sk0) = join(zero,meet(complement(complement(X1)),composition(X1,sk0))),
inference(cp,[status(thm)],[t51037,t60137]) ).
cnf(t88295,plain,
composition(X1,sk0) = meet(complement(complement(X1)),composition(X1,sk0)),
inference(step,[status(thm)],[t60171,t14893]) ).
cnf(t88296,plain,
composition(X1,sk0) = meet(composition(X1,sk0),complement(complement(X1))),
inference(step,[status(thm)],[t88295,t106]) ).
cnf(t88297,plain,
composition(X1,sk0) = meet(composition(X1,sk0),X1),
inference(step,[status(thm)],[t88296,t14996]) ).
cnf(t88298,plain,
composition(X1,sk0) = meet(X1,composition(X1,sk0)),
inference(step,[status(thm)],[t88297,t106]) ).
cnf(t60317,plain,
meet(X1,composition(X1,sk0)) = composition(X1,sk0),
inference(orient,[status(thm)],[t88298]) ).
cnf(t60440,plain,
zero = meet(X1,composition(meet(complement(X1),X2),sk0)),
inference(cp,[status(thm)],[t42107,t60317]) ).
cnf(t71052,plain,
meet(X1,composition(meet(complement(X1),X2),sk0)) = zero,
inference(orient,[status(thm)],[t60440]) ).
cnf(t85922,plain,
composition(meet(complement(sk0),one),sk0) = zero,
inference(cp,[status(thm)],[t85920,t71052]) ).
cnf(t88544,plain,
composition(meet(one,complement(sk0)),sk0) = zero,
inference(step,[status(thm)],[t85922,t106]) ).
cnf(t86052,plain,
composition(meet(one,complement(sk0)),sk0) = zero,
inference(orient,[status(thm)],[t88544]) ).
cnf(t86053,plain,
composition(sk0,converse(meet(one,complement(sk0)))) = converse(zero),
inference(cp,[status(thm)],[t47707,t86052]) ).
cnf(t15602,plain,
join(complement(X1),X2) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t14996,t15554]) ).
cnf(t16388,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t15602]) ).
cnf(t3646,plain,
join(zero,join(composition(top,zero),X1)) = join(composition(top,zero),X1),
inference(cp,[status(thm)],[t46,t3644]) ).
cnf(t3715,plain,
join(zero,join(composition(top,zero),X1)) = join(composition(top,zero),X1),
inference(orient,[status(thm)],[t3646]) ).
cnf(t3723,plain,
join(composition(top,zero),X1) = join(zero,join(X1,composition(top,zero))),
inference(cp,[status(thm)],[t3715,t43]) ).
cnf(t3812,plain,
join(zero,join(X1,composition(top,zero))) = join(composition(top,zero),X1),
inference(orient,[status(thm)],[t3723]) ).
cnf(t1470,plain,
complement(one) = join(complement(one),composition(top,complement(top))),
inference(cp,[status(thm)],[t1465,t405]) ).
cnf(t86543,plain,
complement(one) = join(complement(one),composition(top,zero)),
inference(step,[status(thm)],[t1470,t97]) ).
cnf(t1490,plain,
join(complement(one),composition(top,zero)) = complement(one),
inference(orient,[status(thm)],[t86543]) ).
cnf(t3816,plain,
join(composition(top,zero),complement(one)) = join(zero,complement(one)),
inference(cp,[status(thm)],[t3812,t1490]) ).
cnf(t86729,plain,
join(complement(one),composition(top,zero)) = join(zero,complement(one)),
inference(step,[status(thm)],[t3816,t43]) ).
cnf(t86730,plain,
complement(one) = join(zero,complement(one)),
inference(step,[status(thm)],[t86729,t1490]) ).
cnf(t3835,plain,
join(zero,complement(one)) = complement(one),
inference(orient,[status(thm)],[t86730]) ).
cnf(t3848,plain,
meet(top,one) = complement(complement(one)),
inference(cp,[status(thm)],[t123,t3835]) ).
cnf(t86731,plain,
meet(top,one) = meet(one,one),
inference(step,[status(thm)],[t3848,t256]) ).
cnf(t3851,plain,
meet(one,one) = meet(top,one),
inference(orient,[status(thm)],[t86731]) ).
cnf(t4337,plain,
zero = meet(one,composition(converse(complement(one)),meet(top,one))),
inference(cp,[status(thm)],[t4326,t3851]) ).
cnf(t4551,plain,
meet(one,composition(converse(complement(one)),meet(top,one))) = zero,
inference(orient,[status(thm)],[t4337]) ).
cnf(t87222,plain,
meet(one,composition(converse(complement(one)),one)) = zero,
inference(step,[status(thm)],[t4551,t14995]) ).
cnf(t87223,plain,
meet(one,converse(complement(one))) = zero,
inference(step,[status(thm)],[t87222,t17]) ).
cnf(t15025,plain,
meet(one,converse(complement(one))) = zero,
inference(rw,[status(thm)],[t87223]) ).
cnf(t15067,plain,
meet(one,converse(complement(one))) = zero,
inference(orient,[status(thm)],[t15025]) ).
cnf(t26078,plain,
one = join(zero,meet(one,complement(converse(complement(one))))),
inference(cp,[status(thm)],[t26034,t15067]) ).
cnf(t87454,plain,
one = meet(one,complement(converse(complement(one)))),
inference(step,[status(thm)],[t26078,t14893]) ).
cnf(t26129,plain,
meet(one,complement(converse(complement(one)))) = one,
inference(orient,[status(thm)],[t87454]) ).
cnf(t26158,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(cp,[status(thm)],[t16388,t26129]) ).
cnf(t26165,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t26158]) ).
cnf(t26173,plain,
converse(complement(one)) = meet(converse(complement(one)),complement(one)),
inference(cp,[status(thm)],[t16552,t26165]) ).
cnf(t87460,plain,
converse(complement(one)) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t26173,t106]) ).
cnf(t16583,plain,
converse(X1) = meet(converse(X1),converse(join(X2,X1))),
inference(cp,[status(thm)],[t16552,t60]) ).
cnf(t18864,plain,
meet(converse(X1),converse(join(X2,X1))) = converse(X1),
inference(orient,[status(thm)],[t16583]) ).
cnf(t26177,plain,
converse(converse(complement(one))) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(cp,[status(thm)],[t18864,t26165]) ).
cnf(t87455,plain,
complement(one) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(step,[status(thm)],[t26177,t21]) ).
cnf(t87456,plain,
complement(one) = meet(converse(complement(one)),converse(converse(complement(one)))),
inference(step,[status(thm)],[t87455,t106]) ).
cnf(t87457,plain,
complement(one) = meet(converse(complement(one)),complement(one)),
inference(step,[status(thm)],[t87456,t21]) ).
cnf(t87458,plain,
complement(one) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t87457,t106]) ).
cnf(t26191,plain,
meet(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t87458]) ).
cnf(t87461,plain,
converse(complement(one)) = complement(one),
inference(step,[status(thm)],[t87460,t26191]) ).
cnf(t26380,plain,
converse(complement(one)) = complement(one),
inference(orient,[status(thm)],[t87461]) ).
cnf(t26382,plain,
converse(join(X1,complement(one))) = join(converse(X1),complement(one)),
inference(cp,[status(thm)],[t60,t26380]) ).
cnf(t26571,plain,
converse(join(X1,complement(one))) = join(converse(X1),complement(one)),
inference(orient,[status(thm)],[t26382]) ).
cnf(t29965,plain,
converse(complement(join(X1,complement(one)))) = complement(join(converse(X1),complement(one))),
inference(cp,[status(thm)],[t29962,t26571]) ).
cnf(t265,plain,
meet(complement(X1),X2) = complement(join(meet(X1,X1),complement(X2))),
inference(cp,[status(thm)],[t85,t256]) ).
cnf(t1338,plain,
complement(join(meet(X1,X1),complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t265]) ).
cnf(t87209,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(step,[status(thm)],[t1338,t14961]) ).
cnf(t14993,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(rw,[status(thm)],[t87209]) ).
cnf(t16258,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t14993]) ).
cnf(t87535,plain,
converse(meet(complement(X1),one)) = complement(join(converse(X1),complement(one))),
inference(step,[status(thm)],[t29965,t16258]) ).
cnf(t87536,plain,
converse(meet(one,complement(X1))) = complement(join(converse(X1),complement(one))),
inference(step,[status(thm)],[t87535,t106]) ).
cnf(t87537,plain,
converse(meet(one,complement(X1))) = meet(complement(converse(X1)),one),
inference(step,[status(thm)],[t87536,t16258]) ).
cnf(t87538,plain,
converse(meet(one,complement(X1))) = meet(one,complement(converse(X1))),
inference(step,[status(thm)],[t87537,t106]) ).
cnf(t87539,plain,
converse(meet(one,complement(X1))) = meet(one,converse(complement(X1))),
inference(step,[status(thm)],[t87538,t29962]) ).
cnf(t30040,plain,
converse(meet(one,complement(X1))) = meet(one,converse(complement(X1))),
inference(orient,[status(thm)],[t87539]) ).
cnf(t88545,plain,
composition(sk0,meet(one,converse(complement(sk0)))) = converse(zero),
inference(step,[status(thm)],[t86053,t30040]) ).
cnf(t47054,plain,
converse(complement(sk0)) = complement(sk0),
inference(cp,[status(thm)],[t29962,t47049]) ).
cnf(t47146,plain,
converse(complement(sk0)) = complement(sk0),
inference(orient,[status(thm)],[t47054]) ).
cnf(t88546,plain,
composition(sk0,meet(one,complement(sk0))) = converse(zero),
inference(step,[status(thm)],[t88545,t47146]) ).
cnf(t88547,plain,
composition(sk0,meet(one,complement(sk0))) = zero,
inference(step,[status(thm)],[t88546,t14621]) ).
cnf(t86087,plain,
composition(sk0,meet(one,complement(sk0))) = zero,
inference(orient,[status(thm)],[t88547]) ).
cnf(t86100,plain,
complement(meet(one,complement(sk0))) = join(complement(meet(one,complement(sk0))),composition(converse(sk0),complement(zero))),
inference(cp,[status(thm)],[t54,t86087]) ).
cnf(t88548,plain,
join(complement(one),sk0) = join(complement(meet(one,complement(sk0))),composition(converse(sk0),complement(zero))),
inference(step,[status(thm)],[t86100,t16388]) ).
cnf(t88549,plain,
join(sk0,complement(one)) = join(complement(meet(one,complement(sk0))),composition(converse(sk0),complement(zero))),
inference(step,[status(thm)],[t88548,t43]) ).
cnf(t88550,plain,
join(sk0,complement(one)) = join(composition(converse(sk0),complement(zero)),complement(meet(one,complement(sk0)))),
inference(step,[status(thm)],[t88549,t43]) ).
cnf(t88551,plain,
join(sk0,complement(one)) = join(composition(sk0,complement(zero)),complement(meet(one,complement(sk0)))),
inference(step,[status(thm)],[t88550,t47049]) ).
cnf(t88552,plain,
join(sk0,complement(one)) = join(composition(sk0,top),complement(meet(one,complement(sk0)))),
inference(step,[status(thm)],[t88551,t14553]) ).
cnf(t88553,plain,
join(sk0,complement(one)) = join(composition(sk0,top),join(complement(one),sk0)),
inference(step,[status(thm)],[t88552,t16388]) ).
cnf(t88554,plain,
join(sk0,complement(one)) = join(composition(sk0,top),join(sk0,complement(one))),
inference(step,[status(thm)],[t88553,t43]) ).
cnf(t50,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t46,t43]) ).
cnf(t87396,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t50,t46]) ).
cnf(t21413,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t87396]) ).
cnf(t88555,plain,
join(sk0,complement(one)) = join(sk0,join(composition(sk0,top),complement(one))),
inference(step,[status(thm)],[t88554,t21413]) ).
cnf(t12096,plain,
composition(X1,top) = join(X1,composition(X1,top)),
inference(cp,[status(thm)],[t12092,t17]) ).
cnf(t12200,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t12096]) ).
cnf(t12211,plain,
join(X1,join(composition(X1,top),X2)) = join(composition(X1,top),X2),
inference(cp,[status(thm)],[t46,t12200]) ).
cnf(t75882,plain,
join(X1,join(composition(X1,top),X2)) = join(composition(X1,top),X2),
inference(orient,[status(thm)],[t12211]) ).
cnf(t88556,plain,
join(sk0,complement(one)) = join(composition(sk0,top),complement(one)),
inference(step,[status(thm)],[t88555,t75882]) ).
cnf(t88557,plain,
join(sk0,complement(one)) = join(complement(one),composition(sk0,top)),
inference(step,[status(thm)],[t88556,t43]) ).
cnf(t86118,plain,
join(complement(one),composition(sk0,top)) = join(sk0,complement(one)),
inference(orient,[status(thm)],[t88557]) ).
cnf(t86160,plain,
meet(one,complement(composition(sk0,top))) = complement(join(sk0,complement(one))),
inference(cp,[status(thm)],[t15554,t86118]) ).
cnf(t88573,plain,
meet(one,complement(composition(sk0,top))) = meet(complement(sk0),one),
inference(step,[status(thm)],[t86160,t16258]) ).
cnf(t88574,plain,
meet(one,complement(composition(sk0,top))) = meet(one,complement(sk0)),
inference(step,[status(thm)],[t88573,t106]) ).
cnf(t86357,plain,
meet(one,complement(composition(sk0,top))) = meet(one,complement(sk0)),
inference(orient,[status(thm)],[t88574]) ).
cnf(c17,plain,
meet(complement(composition(sk0,top)),one) != meet(complement(sk0),one),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
meet(complement(composition(sk0,top)),one) != meet(complement(sk0),one),
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(g0_0,plain,
meet(one,complement(composition(sk0,top))) != meet(complement(sk0),one),
inference(rw,[status(thm)],[goal_0,t106]) ).
cnf(g0_1,plain,
meet(one,complement(sk0)) != meet(complement(sk0),one),
inference(rw,[status(thm)],[g0_0,t86357]) ).
cnf(g0_2,plain,
meet(one,complement(sk0)) != meet(one,complement(sk0)),
inference(rw,[status(thm)],[g0_1,t106]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL027+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.19/0.45 % Computer : n004.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Thu Sep 24 07:22:51 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.45 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 60.36/8.15 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 60.36/8.15 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------