%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL030+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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:42 PM UTC 2026
% Result : Theorem 76.65s 10.23s
% Output : Proof 76.65s
% 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/sandbox/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(f10,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/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]) ).
fof(f0,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/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(t192418,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)],[t192418]) ).
fof(f9,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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(t192425,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t170,t21]) ).
cnf(t182,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t192425]) ).
cnf(t183,plain,
one = converse(one),
inference(cp,[status(thm)],[t182,t17]) ).
cnf(t192,plain,
converse(one) = one,
inference(orient,[status(thm)],[t183]) ).
cnf(t192426,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t182,t192]) ).
cnf(t202,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t192426]) ).
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(t192429,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t206,t192]) ).
cnf(t192430,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t192429,t203]) ).
cnf(t236,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t192430]) ).
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/sandbox/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(t193041,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t45,t43]) ).
cnf(t193042,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t193041,t85]) ).
cnf(t193043,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t193042,t43]) ).
cnf(t14257,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t193043]) ).
fof(f12,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/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(t193152,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)],[t193152]) ).
fof(f1,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/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/sandbox/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(t192419,plain,
zero = complement(top),
inference(step,[status(thm)],[t86,t92]) ).
cnf(t97,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t192419]) ).
cnf(t240,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t236,t97]) ).
cnf(t192431,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t240,t97]) ).
cnf(t192432,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t192431,t97]) ).
cnf(t247,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t192432]) ).
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(t193154,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t14882,t14877]) ).
cnf(t14893,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t193154]) ).
cnf(t193159,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t14877,t14893]) ).
cnf(t14928,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t193159]) ).
cnf(t14961,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t14928]) ).
cnf(t193183,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)],[t193183]) ).
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(t192468,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t237,t85]) ).
cnf(t192469,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t192468,t85]) ).
cnf(t544,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t192469]) ).
cnf(t87,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t85,t43]) ).
cnf(t192421,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)],[t192421]) ).
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(t193199,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t14962,t14961]) ).
cnf(t193200,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t193199,t14961]) ).
cnf(t15026,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t193200]) ).
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(t193202,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t15092,t14257]) ).
cnf(t193203,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t193202,t43]) ).
cnf(t15101,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t193203]) ).
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(t193219,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)],[t193219]) ).
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(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/sandbox/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(t192440,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t360,t51]) ).
cnf(t373,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t192440]) ).
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(t192442,plain,
top = join(X1,top),
inference(step,[status(thm)],[t358,t386]) ).
cnf(t391,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t192442]) ).
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/sandbox/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(t192990,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(t192991,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t192990,t159]) ).
cnf(t192992,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t192991,t294]) ).
cnf(t192993,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t192992,t405]) ).
cnf(t192994,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t192993,t391]) ).
cnf(t12092,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t192994]) ).
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(t192755,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t5443,t417]) ).
cnf(t192756,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t192755,t417]) ).
cnf(t192757,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t192756,t397]) ).
cnf(t192758,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t192757,t405]) ).
cnf(t5565,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t192758]) ).
cnf(t5581,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t5565,t192]) ).
cnf(t192759,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t5581,t17]) ).
cnf(t192760,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t192759,t391]) ).
cnf(t5594,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t192760]) ).
cnf(t5599,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t5594]) ).
cnf(t192768,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t5599,t97]) ).
cnf(t192769,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t192768,t97]) ).
cnf(t192770,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t192769,t405]) ).
cnf(t192771,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t192770,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/sandbox/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(t192458,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)],[t192458]) ).
cnf(t2661,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t2656,t456]) ).
cnf(t192649,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)],[t192649]) ).
cnf(t2765,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t2725,t60]) ).
cnf(t192650,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t2765,t21]) ).
cnf(t192651,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t192650,t21]) ).
cnf(t2778,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t192651]) ).
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(t192665,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)],[t192665]) ).
cnf(t3337,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t85,t3322]) ).
cnf(t192666,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)],[t192666]) ).
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(t192667,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(t192668,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)],[t192667,t192]) ).
cnf(t192669,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)],[t192668,t17]) ).
cnf(t192670,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)],[t192669,t92]) ).
cnf(t192671,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)],[t192670,t3343]) ).
cnf(t192672,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)],[t192671,t17]) ).
cnf(t192673,plain,
composition(zero,zero) = join(meet(X1,complement(X1)),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t192672,t21]) ).
cnf(t192674,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t192673,t92]) ).
cnf(t192675,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),converse(one))),zero)),
inference(step,[status(thm)],[t192674,t21]) ).
cnf(t192676,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),one)),zero)),
inference(step,[status(thm)],[t192675,t192]) ).
cnf(t192677,plain,
composition(zero,zero) = join(zero,composition(meet(X1,complement(X1)),zero)),
inference(step,[status(thm)],[t192676,t17]) ).
cnf(t192678,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t192677,t92]) ).
cnf(t3365,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t192678]) ).
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(t192691,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)],[t192691]) ).
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(t192521,plain,
join(zero,join(X1,join(zero,X2))) = join(join(zero,X1),X2),
inference(step,[status(thm)],[t275,t46]) ).
cnf(t192522,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(step,[status(thm)],[t192521,t46]) ).
cnf(t1597,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(orient,[status(thm)],[t192522]) ).
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,X1,X2] :
( join(X0,one) = one
=> meet(composition(X0,X1),complement(X2)) = meet(composition(X0,X1),complement(composition(X0,X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0,X1,X2] :
( join(X0,one) = one
=> meet(composition(X0,X1),complement(X2)) = meet(composition(X0,X1),complement(composition(X0,X2))) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0,X1,X2] :
( meet(composition(X0,X1),complement(X2)) != meet(composition(X0,X1),complement(composition(X0,X2)))
& join(X0,one) = one ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( meet(composition(sk0,sk1),complement(sk2)) != meet(composition(sk0,sk1),complement(composition(sk0,sk2)))
& join(sk0,one) = one ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f16_nnf]) ).
cnf(c16,plain,
join(sk0,one) = one,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t2,plain,
join(sk0,one) = one,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(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(t192427,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)],[t192427]) ).
cnf(t192453,plain,
join(one,converse(complement(sk0))) = join(one,converse(top)),
inference(step,[status(thm)],[t383,t220]) ).
cnf(t192454,plain,
join(one,converse(complement(sk0))) = join(one,top),
inference(step,[status(thm)],[t192453,t405]) ).
cnf(t192455,plain,
join(one,converse(complement(sk0))) = top,
inference(step,[status(thm)],[t192454,t391]) ).
cnf(t443,plain,
join(one,converse(complement(sk0))) = top,
inference(orient,[status(thm)],[t192455]) ).
cnf(t444,plain,
join(one,join(converse(complement(sk0)),X1)) = join(top,X1),
inference(cp,[status(thm)],[t46,t443]) ).
cnf(t192459,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)],[t192459]) ).
cnf(t765,plain,
top = join(join(converse(complement(sk0)),X1),join(one,complement(top))),
inference(cp,[status(thm)],[t734,t471]) ).
cnf(t192570,plain,
top = join(converse(complement(sk0)),join(X1,join(one,complement(top)))),
inference(step,[status(thm)],[t765,t46]) ).
cnf(t192571,plain,
top = join(converse(complement(sk0)),join(X1,join(one,zero))),
inference(step,[status(thm)],[t192570,t97]) ).
cnf(t192572,plain,
top = join(converse(complement(sk0)),join(X1,join(zero,one))),
inference(step,[status(thm)],[t192571,t43]) ).
cnf(t2215,plain,
join(converse(complement(sk0)),join(X1,join(zero,one))) = top,
inference(orient,[status(thm)],[t192572]) ).
cnf(t2219,plain,
top = join(converse(complement(sk0)),join(join(zero,one),X1)),
inference(cp,[status(thm)],[t2215,t43]) ).
cnf(t192612,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)],[t192612]) ).
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(t192420,plain,
top = join(zero,top),
inference(step,[status(thm)],[t99,t43]) ).
cnf(t104,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t192420]) ).
cnf(t192624,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)],[t192624]) ).
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(t192692,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)],[t192692]) ).
cnf(t192772,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t192771,t3644]) ).
cnf(t5611,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t192772]) ).
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(t193021,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t12144,t5635]) ).
cnf(t193022,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t193021,t43]) ).
cnf(t13339,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t193022]) ).
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(t192779,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t5613,t397]) ).
cnf(t192780,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t192779,t5611]) ).
cnf(t5660,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t192780]) ).
cnf(t192783,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)],[t192783]) ).
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(t192806,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t5749,t46]) ).
cnf(t192807,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t192806,t5660]) ).
cnf(t5958,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t192807]) ).
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/sandbox/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(t192898,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)],[t192898]) ).
cnf(t7831,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t7819,t203]) ).
cnf(t192899,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t7831,t391]) ).
cnf(t192900,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t192899,t5594]) ).
cnf(t7860,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t192900]) ).
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(t192903,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t7901,t405]) ).
cnf(t192904,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t192903,t405]) ).
cnf(t7935,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t192904]) ).
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(t192923,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t7963,t405]) ).
cnf(t192924,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t192923,t43]) ).
cnf(t192925,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t192924,t97]) ).
cnf(t192926,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t192925,t5611]) ).
cnf(t8643,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t192926]) ).
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(t193086,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)],[t193086]) ).
cnf(t14618,plain,
join(converse(zero),zero) = converse(converse(zero)),
inference(cp,[status(thm)],[t311,t14611]) ).
cnf(t193087,plain,
join(zero,converse(zero)) = converse(converse(zero)),
inference(step,[status(thm)],[t14618,t43]) ).
cnf(t193088,plain,
converse(zero) = converse(converse(zero)),
inference(step,[status(thm)],[t193087,t14611]) ).
cnf(t193089,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t193088,t21]) ).
cnf(t14621,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t193089]) ).
cnf(t14624,plain,
converse(composition(X1,zero)) = composition(zero,converse(X1)),
inference(cp,[status(thm)],[t27,t14621]) ).
cnf(t193123,plain,
converse(zero) = composition(zero,converse(X1)),
inference(step,[status(thm)],[t14624,t14456]) ).
cnf(t193124,plain,
zero = composition(zero,converse(X1)),
inference(step,[status(thm)],[t193123,t14621]) ).
cnf(t14706,plain,
composition(zero,converse(X1)) = zero,
inference(orient,[status(thm)],[t193124]) ).
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(t193125,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t14755,t14621]) ).
cnf(t193126,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t193125,t14744]) ).
cnf(t193127,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t193126,t43]) ).
cnf(t14757,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t193127]) ).
cnf(t193140,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)],[t193140]) ).
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(t192660,plain,
join(complement(X1),join(X2,join(X1,X3))) = join(top,X3),
inference(step,[status(thm)],[t2877,t46]) ).
cnf(t192661,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(step,[status(thm)],[t192660,t397]) ).
cnf(t3178,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(orient,[status(thm)],[t192661]) ).
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(t193083,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t14558,t391]) ).
cnf(t193084,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t193083,t97]) ).
cnf(t14600,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t193084]) ).
cnf(t193186,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t14955,t14600]) ).
cnf(t193187,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t193186,t14757]) ).
cnf(t193188,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t193187,t14801]) ).
cnf(t14995,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t193188]) ).
cnf(t193189,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t14801,t14995]) ).
cnf(t14996,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t193189]) ).
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(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(t193453,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t27870,t14996]) ).
cnf(t193454,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t193453,t85]) ).
cnf(t27891,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t193454]) ).
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(t26347,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t19528,t26302]) ).
cnf(t195066,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(step,[status(thm)],[t26347,t19528]) ).
cnf(t121440,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t195066]) ).
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(t193184,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)],[t193184]) ).
cnf(t16258,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t14993]) ).
cnf(t16271,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t14996,t16258]) ).
cnf(t16434,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t16271]) ).
cnf(t121460,plain,
join(X1,X2) = join(X1,meet(X2,join(X3,complement(X1)))),
inference(cp,[status(thm)],[t121440,t16434]) ).
cnf(t165055,plain,
join(X1,meet(X2,join(X3,complement(X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t121460]) ).
cnf(t165175,plain,
meet(X1,meet(X2,join(X3,complement(complement(X1))))) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t27960,t165055]) ).
cnf(t195573,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t165175,t14996]) ).
cnf(t195574,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(step,[status(thm)],[t195573,t27960]) ).
cnf(t165345,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t195574]) ).
cnf(t165516,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X3,X1)),
inference(cp,[status(thm)],[t165345,t15101]) ).
cnf(t171815,plain,
meet(meet(X1,X2),meet(X3,X1)) = meet(meet(X1,X2),X3),
inference(orient,[status(thm)],[t165516]) ).
cnf(t171838,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t171815,t106]) ).
cnf(t165414,plain,
meet(X1,X2) = meet(X1,meet(join(X3,X1),X2)),
inference(cp,[status(thm)],[t165345,t106]) ).
cnf(t167051,plain,
meet(X1,meet(join(X2,X1),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t165414]) ).
cnf(t167272,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X2,X3)),
inference(cp,[status(thm)],[t167051,t15129]) ).
cnf(t188048,plain,
meet(meet(X1,X2),meet(X2,X3)) = meet(meet(X1,X2),X3),
inference(orient,[status(thm)],[t167272]) ).
cnf(t195734,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),X2),
inference(step,[status(thm)],[t171838,t188048]) ).
cnf(t189663,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),X2),
inference(orient,[status(thm)],[t195734]) ).
cnf(t189685,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(cp,[status(thm)],[t189663,t106]) ).
cnf(t191234,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t189685]) ).
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(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(t192930,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)],[t192930]) ).
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(t193185,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)],[t193185]) ).
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(t193240,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(t193241,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)],[t193240,t14744]) ).
cnf(t193242,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)],[t193241,t106]) ).
cnf(t193243,plain,
zero = join(meet(converse(complement(X1)),converse(X1)),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t193242,t203]) ).
cnf(t193244,plain,
zero = join(meet(converse(X1),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t193243,t106]) ).
cnf(t193245,plain,
zero = join(meet(converse(X1),converse(complement(X1))),zero),
inference(step,[status(thm)],[t193244,t14744]) ).
cnf(t193246,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(step,[status(thm)],[t193245,t14946]) ).
cnf(t16973,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t193246]) ).
cnf(t28466,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t28391,t16973]) ).
cnf(t193481,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t28466,t43]) ).
cnf(t193482,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t193481,t14946]) ).
cnf(t29844,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t193482]) ).
cnf(t29849,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t29844,t14996]) ).
cnf(t192451,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)],[t192451]) ).
cnf(t15595,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t15554,t408]) ).
cnf(t193428,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)],[t193428]) ).
cnf(t26884,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t26876,t26018]) ).
cnf(t193449,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t26884,t14996]) ).
cnf(t193450,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t193449,t14946]) ).
cnf(t27421,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t193450]) ).
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(t193483,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)],[t193483]) ).
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(t193155,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)],[t193155]) ).
cnf(t193195,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)],[t193195]) ).
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(t193528,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t31492,t15554]) ).
cnf(t193529,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t193528,t29895]) ).
cnf(t193530,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t193529,t14996]) ).
cnf(t31513,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t193530]) ).
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(t192463,plain,
join(one,join(complement(sk0),X1)) = converse(top),
inference(step,[status(thm)],[t489,t21]) ).
cnf(t192464,plain,
join(one,join(complement(sk0),X1)) = top,
inference(step,[status(thm)],[t192463,t405]) ).
cnf(t492,plain,
join(one,join(complement(sk0),X1)) = top,
inference(orient,[status(thm)],[t192464]) ).
cnf(t27791,plain,
join(join(complement(sk0),X1),complement(one)) = join(join(complement(sk0),X1),complement(top)),
inference(cp,[status(thm)],[t27674,t492]) ).
cnf(t194245,plain,
join(complement(sk0),join(X1,complement(one))) = join(join(complement(sk0),X1),complement(top)),
inference(step,[status(thm)],[t27791,t46]) ).
cnf(t194246,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),join(X1,complement(top))),
inference(step,[status(thm)],[t194245,t46]) ).
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(t194247,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(top),join(complement(sk0),X1)),
inference(step,[status(thm)],[t194246,t15758]) ).
cnf(t194248,plain,
join(complement(sk0),join(X1,complement(one))) = join(zero,join(complement(sk0),X1)),
inference(step,[status(thm)],[t194247,t97]) ).
cnf(t194249,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),X1),
inference(step,[status(thm)],[t194248,t14893]) ).
cnf(t59707,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),X1),
inference(orient,[status(thm)],[t194249]) ).
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(t194250,plain,
meet(sk0,join(X1,complement(one))) = meet(complement(complement(sk0)),join(complement(sk0),X1)),
inference(step,[status(thm)],[t59716,t14996]) ).
cnf(t194251,plain,
meet(sk0,join(X1,complement(one))) = meet(complement(complement(sk0)),X1),
inference(step,[status(thm)],[t194250,t28877]) ).
cnf(t194252,plain,
meet(sk0,join(X1,complement(one))) = meet(sk0,X1),
inference(step,[status(thm)],[t194251,t14996]) ).
cnf(t59756,plain,
meet(sk0,join(X1,complement(one))) = meet(sk0,X1),
inference(orient,[status(thm)],[t194252]) ).
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(t193222,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)],[t193222]) ).
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(t194255,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)],[t194255]) ).
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(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(t16378,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t15129,t16371]) ).
cnf(t193228,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)],[t193228]) ).
cnf(t16522,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t14996,t16475]) ).
cnf(t193229,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)],[t193229]) ).
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(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(t192683,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(t192684,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)],[t192683,t17]) ).
cnf(t192685,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)],[t192684,t192]) ).
cnf(t192686,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)],[t192685,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)],[t192686]) ).
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(t193310,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(t193311,plain,
composition(sk0,meet(one,converse(sk0))) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t193310,t17]) ).
cnf(t221,plain,
join(one,converse(sk0)) = converse(one),
inference(cp,[status(thm)],[t220,t83]) ).
cnf(t192428,plain,
join(one,converse(sk0)) = one,
inference(step,[status(thm)],[t221,t192]) ).
cnf(t233,plain,
join(one,converse(sk0)) = one,
inference(orient,[status(thm)],[t192428]) ).
cnf(t16577,plain,
converse(sk0) = meet(converse(sk0),one),
inference(cp,[status(thm)],[t16552,t233]) ).
cnf(t193230,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)],[t193230]) ).
cnf(t193312,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t193311,t16609]) ).
cnf(t193313,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t193312,t16669]) ).
cnf(t193314,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,meet(one,converse(sk0)))),
inference(step,[status(thm)],[t193313,t17]) ).
cnf(t193315,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,converse(sk0))),
inference(step,[status(thm)],[t193314,t16609]) ).
cnf(t18589,plain,
join(sk0,composition(sk0,converse(sk0))) = composition(sk0,converse(sk0)),
inference(orient,[status(thm)],[t193315]) ).
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(t193641,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)],[t193641]) ).
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(t193817,plain,
sk0 = meet(sk0,converse(sk0)),
inference(step,[status(thm)],[t46860,t203]) ).
cnf(t46960,plain,
meet(sk0,converse(sk0)) = sk0,
inference(orient,[status(thm)],[t193817]) ).
cnf(t47025,plain,
meet(sk0,converse(sk0)) = converse(sk0),
inference(cp,[status(thm)],[t31631,t46960]) ).
cnf(t193818,plain,
sk0 = converse(sk0),
inference(step,[status(thm)],[t47025,t46960]) ).
cnf(t47049,plain,
converse(sk0) = sk0,
inference(orient,[status(thm)],[t193818]) ).
cnf(t194256,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(t194257,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)],[t194256,t60035]) ).
cnf(t194258,plain,
zero = join(meet(composition(X1,sk0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(step,[status(thm)],[t194257,t14456]) ).
cnf(t194259,plain,
zero = join(meet(complement(X1),composition(X1,sk0)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(step,[status(thm)],[t194258,t106]) ).
cnf(t194260,plain,
zero = join(meet(complement(X1),composition(X1,sk0)),zero),
inference(step,[status(thm)],[t194259,t14456]) ).
cnf(t194261,plain,
zero = meet(complement(X1),composition(X1,sk0)),
inference(step,[status(thm)],[t194260,t14946]) ).
cnf(t60137,plain,
meet(complement(X1),composition(X1,sk0)) = zero,
inference(orient,[status(thm)],[t194261]) ).
cnf(t60167,plain,
join(complement(complement(X1)),composition(X1,sk0)) = join(complement(complement(X1)),zero),
inference(cp,[status(thm)],[t28391,t60137]) ).
cnf(t194262,plain,
join(composition(X1,sk0),complement(complement(X1))) = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t60167,t43]) ).
cnf(t194263,plain,
join(composition(X1,sk0),X1) = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t194262,t14996]) ).
cnf(t194264,plain,
join(X1,composition(X1,sk0)) = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t194263,t43]) ).
cnf(t194265,plain,
join(X1,composition(X1,sk0)) = complement(complement(X1)),
inference(step,[status(thm)],[t194264,t14946]) ).
cnf(t194266,plain,
join(X1,composition(X1,sk0)) = X1,
inference(step,[status(thm)],[t194265,t14996]) ).
cnf(t60194,plain,
join(X1,composition(X1,sk0)) = X1,
inference(orient,[status(thm)],[t194266]) ).
cnf(t60215,plain,
join(X1,join(composition(X1,sk0),X2)) = join(X1,X2),
inference(cp,[status(thm)],[t46,t60194]) ).
cnf(t63401,plain,
join(X1,join(composition(X1,sk0),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t60215]) ).
cnf(t63414,plain,
join(X1,composition(X2,sk0)) = join(X1,composition(join(X1,X2),sk0)),
inference(cp,[status(thm)],[t63401,t24]) ).
cnf(t92073,plain,
join(X1,composition(join(X1,X2),sk0)) = join(X1,composition(X2,sk0)),
inference(orient,[status(thm)],[t63414]) ).
cnf(t92149,plain,
join(X1,composition(complement(X1),sk0)) = join(X1,composition(top,sk0)),
inference(cp,[status(thm)],[t92073,t51]) ).
cnf(t92411,plain,
join(X1,composition(complement(X1),sk0)) = join(X1,composition(top,sk0)),
inference(orient,[status(thm)],[t92149]) ).
cnf(t92488,plain,
meet(X1,composition(complement(complement(X1)),sk0)) = meet(X1,join(complement(X1),composition(top,sk0))),
inference(cp,[status(thm)],[t27960,t92411]) ).
cnf(t194641,plain,
meet(X1,composition(X1,sk0)) = meet(X1,join(complement(X1),composition(top,sk0))),
inference(step,[status(thm)],[t92488,t14996]) ).
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(t60171,plain,
composition(X1,sk0) = join(zero,meet(complement(complement(X1)),composition(X1,sk0))),
inference(cp,[status(thm)],[t51037,t60137]) ).
cnf(t194270,plain,
composition(X1,sk0) = meet(complement(complement(X1)),composition(X1,sk0)),
inference(step,[status(thm)],[t60171,t14893]) ).
cnf(t194271,plain,
composition(X1,sk0) = meet(composition(X1,sk0),complement(complement(X1))),
inference(step,[status(thm)],[t194270,t106]) ).
cnf(t194272,plain,
composition(X1,sk0) = meet(composition(X1,sk0),X1),
inference(step,[status(thm)],[t194271,t14996]) ).
cnf(t194273,plain,
composition(X1,sk0) = meet(X1,composition(X1,sk0)),
inference(step,[status(thm)],[t194272,t106]) ).
cnf(t60317,plain,
meet(X1,composition(X1,sk0)) = composition(X1,sk0),
inference(orient,[status(thm)],[t194273]) ).
cnf(t194642,plain,
composition(X1,sk0) = meet(X1,join(complement(X1),composition(top,sk0))),
inference(step,[status(thm)],[t194641,t60317]) ).
cnf(t194643,plain,
composition(X1,sk0) = meet(X1,composition(top,sk0)),
inference(step,[status(thm)],[t194642,t27960]) ).
cnf(t92527,plain,
meet(X1,composition(top,sk0)) = composition(X1,sk0),
inference(orient,[status(thm)],[t194643]) ).
cnf(t92609,plain,
meet(X1,converse(composition(top,sk0))) = converse(composition(converse(X1),sk0)),
inference(cp,[status(thm)],[t31513,t92527]) ).
cnf(t194644,plain,
meet(X1,composition(converse(sk0),top)) = converse(composition(converse(X1),sk0)),
inference(step,[status(thm)],[t92609,t431]) ).
cnf(t194645,plain,
meet(X1,composition(sk0,top)) = converse(composition(converse(X1),sk0)),
inference(step,[status(thm)],[t194644,t47049]) ).
cnf(t194646,plain,
meet(X1,composition(sk0,top)) = composition(converse(sk0),X1),
inference(step,[status(thm)],[t194645,t169]) ).
cnf(t194647,plain,
meet(X1,composition(sk0,top)) = composition(sk0,X1),
inference(step,[status(thm)],[t194646,t47049]) ).
cnf(t92929,plain,
meet(X1,composition(sk0,top)) = composition(sk0,X1),
inference(orient,[status(thm)],[t194647]) ).
cnf(t191416,plain,
meet(X1,meet(composition(sk0,top),X2)) = meet(composition(sk0,X1),X2),
inference(cp,[status(thm)],[t191234,t92929]) ).
cnf(t92932,plain,
composition(sk0,X1) = meet(composition(sk0,top),X1),
inference(cp,[status(thm)],[t92929,t106]) ).
cnf(t93170,plain,
meet(composition(sk0,top),X1) = composition(sk0,X1),
inference(orient,[status(thm)],[t92932]) ).
cnf(t195756,plain,
meet(X1,composition(sk0,X2)) = meet(composition(sk0,X1),X2),
inference(step,[status(thm)],[t191416,t93170]) ).
cnf(t192030,plain,
meet(composition(sk0,X1),X2) = meet(X1,composition(sk0,X2)),
inference(orient,[status(thm)],[t195756]) ).
cnf(t26355,plain,
meet(X1,complement(meet(X2,complement(complement(X1))))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t15554,t26302]) ).
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(t193455,plain,
meet(X1,join(complement(X2),complement(X1))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t26355,t16388]) ).
cnf(t193456,plain,
meet(X1,complement(meet(X2,X1))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t193455,t16309]) ).
cnf(t193457,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t193456,t15554]) ).
cnf(t28036,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t193457]) ).
cnf(t93198,plain,
composition(sk0,complement(meet(X1,composition(sk0,top)))) = meet(composition(sk0,top),complement(X1)),
inference(cp,[status(thm)],[t93170,t28036]) ).
cnf(t194663,plain,
composition(sk0,complement(composition(sk0,X1))) = meet(composition(sk0,top),complement(X1)),
inference(step,[status(thm)],[t93198,t92929]) ).
cnf(t194664,plain,
composition(sk0,complement(composition(sk0,X1))) = composition(sk0,complement(X1)),
inference(step,[status(thm)],[t194663,t93170]) ).
cnf(t93818,plain,
composition(sk0,complement(composition(sk0,X1))) = composition(sk0,complement(X1)),
inference(orient,[status(thm)],[t194664]) ).
cnf(c17,plain,
meet(composition(sk0,sk1),complement(sk2)) != meet(composition(sk0,sk1),complement(composition(sk0,sk2))),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
meet(composition(sk0,sk1),complement(composition(sk0,sk2))) != meet(composition(sk0,sk1),complement(sk2)),
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(g0_0,plain,
meet(sk1,composition(sk0,complement(composition(sk0,sk2)))) != meet(composition(sk0,sk1),complement(sk2)),
inference(rw,[status(thm)],[goal_0,t192030]) ).
cnf(g0_1,plain,
meet(sk1,composition(sk0,complement(sk2))) != meet(composition(sk0,sk1),complement(sk2)),
inference(rw,[status(thm)],[g0_0,t93818]) ).
cnf(g0_2,plain,
meet(sk1,composition(sk0,complement(sk2))) != meet(sk1,composition(sk0,complement(sk2))),
inference(rw,[status(thm)],[g0_1,t192030]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL030+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n004.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 07:25:35 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 76.65/10.23 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 76.65/10.23 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------