%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL029-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:35:30 PM UTC 2026
% Result : Unsatisfiable 101.90s 13.55s
% Output : CNFRefutation 101.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 87
% Number of leaves : 21
% Syntax : Number of clauses : 505 ( 505 unt; 0 nHn; 159 RR)
% Number of literals : 505 ( 504 equ; 9 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 11 con; 0-2 aty)
% Number of variables : 581 ( 45 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t7,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t74,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t7]) ).
cnf(t6,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t76,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t74,t25]) ).
cnf(t41027,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t76,t74]) ).
cnf(t91,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t41027]) ).
cnf(t16,axiom,
sFlat1 = composition(sk2,sk3),
introduced(definition) ).
cnf(t64,plain,
composition(sk2,sk3) = sFlat1,
inference(orient,[status(thm)],[t16]) ).
cnf(t15,axiom,
sFlat0 = composition(sk1,sk3),
introduced(definition) ).
cnf(t59,plain,
composition(sk1,sk3) = sFlat0,
inference(orient,[status(thm)],[t15]) ).
cnf(t17,axiom,
sFlat2 = meet(composition(sk1,sk3),composition(sk2,sk3)),
introduced(definition) ).
cnf(t41024,plain,
sFlat2 = meet(sFlat0,composition(sk2,sk3)),
inference(step,[status(thm)],[t17,t59]) ).
cnf(t41025,plain,
sFlat2 = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t41024,t64]) ).
cnf(t83,plain,
meet(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t41025]) ).
cnf(t18,axiom,
sFlat3 = meet(sk1,sk2),
introduced(definition) ).
cnf(t84,plain,
meet(sk1,sk2) = sFlat3,
inference(orient,[status(thm)],[t18]) ).
cnf(t92,plain,
meet(sk1,sk2) = sFlat3,
inference(rw,[status(thm)],[t84]) ).
cnf(t41028,plain,
meet(sk2,sk1) = sFlat3,
inference(step,[status(thm)],[t92,t91]) ).
cnf(t93,plain,
meet(sk2,sk1) = sFlat3,
inference(orient,[status(thm)],[t41028]) ).
cnf(t19,axiom,
sFlat4 = composition(meet(sk1,sk2),sk3),
introduced(definition) ).
cnf(t69,plain,
composition(meet(sk1,sk2),sk3) = sFlat4,
inference(orient,[status(thm)],[t19]) ).
cnf(t41026,plain,
composition(sFlat3,sk3) = sFlat4,
inference(step,[status(thm)],[t69,t84]) ).
cnf(t85,plain,
composition(sFlat3,sk3) = sFlat4,
inference(rw,[status(thm)],[t41026]) ).
cnf(t86,plain,
composition(sFlat3,sk3) = sFlat4,
inference(orient,[status(thm)],[t85]) ).
cnf(t14,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t26,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t20]) ).
cnf(t41165,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t26,t25]) ).
cnf(t41166,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t41165,t74]) ).
cnf(t41167,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t41166,t25]) ).
cnf(t1053,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t41167]) ).
cnf(t13,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t41023,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t13,t25]) ).
cnf(t35,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t41023]) ).
cnf(t8,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t52,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t54,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t52,t24]) ).
cnf(t153,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t54]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t154,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t153,t23]) ).
cnf(t41036,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t154,t24]) ).
cnf(t168,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t41036]) ).
cnf(t10,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t47,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t48,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t47,t23]) ).
cnf(t103,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t48]) ).
cnf(t170,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t168,t103]) ).
cnf(t41038,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t170,t168]) ).
cnf(t186,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t41038]) ).
cnf(t189,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t35,t186]) ).
cnf(t169,plain,
one = converse(one),
inference(cp,[status(thm)],[t168,t23]) ).
cnf(t175,plain,
converse(one) = one,
inference(orient,[status(thm)],[t169]) ).
cnf(t41052,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t189,t175]) ).
cnf(t41053,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t41052,t186]) ).
cnf(t302,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t41053]) ).
cnf(t1066,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t1053,t302]) ).
cnf(t41169,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t1066,t25]) ).
cnf(t5,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t81,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t41170,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t41169,t81]) ).
cnf(t41171,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t41170,t25]) ).
cnf(t1106,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t41171]) ).
cnf(t21,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(join(complement(X1),complement(X2))),join(complement(X1),X2)))),
inference(cp,[status(thm)],[t20,t20]) ).
cnf(t11,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t29,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t27,t25]) ).
cnf(t41039,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t29,t27]) ).
cnf(t193,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t41039]) ).
cnf(t41048,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(complement(join(complement(X1),complement(X2))),X2)))),
inference(step,[status(thm)],[t21,t193]) ).
cnf(t41049,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,complement(join(complement(X1),complement(X2))))))),
inference(step,[status(thm)],[t41048,t25]) ).
cnf(t41050,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t41049,t74]) ).
cnf(t253,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t41050]) ).
cnf(t4,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t75,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t74,t30]) ).
cnf(t41029,plain,
zero = complement(top),
inference(step,[status(thm)],[t75,t81]) ).
cnf(t94,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t41029]) ).
cnf(t97,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t74,t94]) ).
cnf(t278,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t97]) ).
cnf(t1114,plain,
meet(top,complement(X1)) = complement(X1),
inference(cp,[status(thm)],[t278,t1106]) ).
cnf(t1115,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1114]) ).
cnf(t1123,plain,
join(complement(top),complement(complement(X1))) = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(cp,[status(thm)],[t253,t1115]) ).
cnf(t41174,plain,
join(zero,complement(complement(X1))) = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t1123,t94]) ).
cnf(t41175,plain,
X1 = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t41174,t1106]) ).
cnf(t41176,plain,
X1 = join(zero,complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t41175,t94]) ).
cnf(t41177,plain,
X1 = join(zero,complement(join(zero,join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t41176,t94]) ).
cnf(t41178,plain,
X1 = join(zero,complement(join(zero,complement(X1)))),
inference(step,[status(thm)],[t41177,t302]) ).
cnf(t41179,plain,
X1 = join(zero,meet(top,X1)),
inference(step,[status(thm)],[t41178,t278]) ).
cnf(t1127,plain,
join(zero,meet(top,X1)) = X1,
inference(orient,[status(thm)],[t41179]) ).
cnf(t1128,plain,
complement(X1) = join(zero,complement(X1)),
inference(cp,[status(thm)],[t1127,t1115]) ).
cnf(t1132,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1128]) ).
cnf(t41181,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t1106,t1132]) ).
cnf(t1139,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t41181]) ).
cnf(t1153,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1139]) ).
cnf(t1163,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t74,t1153]) ).
cnf(t1330,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t1163]) ).
cnf(t1334,plain,
meet(complement(join(X1,X2)),X3) = complement(join(X1,join(X2,complement(X3)))),
inference(cp,[status(thm)],[t1330,t27]) ).
cnf(t5619,plain,
complement(join(X1,join(X2,complement(X3)))) = meet(complement(join(X1,X2)),X3),
inference(orient,[status(thm)],[t1334]) ).
cnf(t1164,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t74,t1153]) ).
cnf(t1358,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t1164]) ).
cnf(t5620,plain,
meet(complement(join(complement(X1),X2)),X3) = meet(X1,complement(join(X2,complement(X3)))),
inference(cp,[status(thm)],[t5619,t1358]) ).
cnf(t41527,plain,
meet(meet(X1,complement(X2)),X3) = meet(X1,complement(join(X2,complement(X3)))),
inference(step,[status(thm)],[t5620,t1358]) ).
cnf(t41528,plain,
meet(meet(X1,complement(X2)),X3) = meet(X1,meet(complement(X2),X3)),
inference(step,[status(thm)],[t41527,t1330]) ).
cnf(t5981,plain,
meet(meet(X1,complement(X2)),X3) = meet(X1,meet(complement(X2),X3)),
inference(orient,[status(thm)],[t41528]) ).
cnf(t6032,plain,
meet(X1,meet(complement(complement(X2)),X3)) = meet(meet(X1,X2),X3),
inference(cp,[status(thm)],[t5981,t1153]) ).
cnf(t41529,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t6032,t1153]) ).
cnf(t6061,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t41529]) ).
cnf(t1161,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t302,t1153]) ).
cnf(t41187,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1161,t1153]) ).
cnf(t41188,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t41187,t1153]) ).
cnf(t1180,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t41188]) ).
cnf(t1182,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t1180,t193]) ).
cnf(t41208,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t1182,t27]) ).
cnf(t41209,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t41208,t1180]) ).
cnf(t1306,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t41209]) ).
cnf(t1059,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t1053,t74]) ).
cnf(t41237,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t1059,t25]) ).
cnf(t1415,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t41237]) ).
cnf(t1420,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t1306,t1415]) ).
cnf(t41238,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t1420,t1415]) ).
cnf(t41239,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t41238,t25]) ).
cnf(t1422,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t41239]) ).
cnf(t1429,plain,
meet(X1,complement(meet(complement(X1),X2))) = complement(complement(X1)),
inference(cp,[status(thm)],[t1358,t1422]) ).
cnf(t1155,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t1153,t74]) ).
cnf(t1310,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t1155]) ).
cnf(t1315,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t1310,t1153]) ).
cnf(t3814,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t1315]) ).
cnf(t41420,plain,
meet(X1,join(X1,complement(X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t1429,t3814]) ).
cnf(t41421,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t41420,t1153]) ).
cnf(t4204,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t41421]) ).
cnf(t4208,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t4204,t1153]) ).
cnf(t4212,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t4208]) ).
cnf(t12,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t66,plain,
composition(join(sk2,X1),sk3) = join(sFlat1,composition(X1,sk3)),
inference(cp,[status(thm)],[t33,t64]) ).
cnf(t241,plain,
composition(join(sk2,X1),sk3) = join(sFlat1,composition(X1,sk3)),
inference(orient,[status(thm)],[t66]) ).
cnf(t3,axiom,
join(sk2,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t45,plain,
join(sk2,one) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t242,plain,
join(sFlat1,composition(one,sk3)) = composition(one,sk3),
inference(cp,[status(thm)],[t241,t45]) ).
cnf(t41046,plain,
join(sFlat1,sk3) = composition(one,sk3),
inference(step,[status(thm)],[t242,t186]) ).
cnf(t41047,plain,
join(sFlat1,sk3) = sk3,
inference(step,[status(thm)],[t41046,t186]) ).
cnf(t252,plain,
join(sFlat1,sk3) = sk3,
inference(orient,[status(thm)],[t41047]) ).
cnf(t4217,plain,
sFlat1 = meet(sFlat1,sk3),
inference(cp,[status(thm)],[t4212,t252]) ).
cnf(t4236,plain,
meet(sFlat1,sk3) = sFlat1,
inference(orient,[status(thm)],[t4217]) ).
cnf(t6119,plain,
meet(sFlat1,meet(sk3,X1)) = meet(sFlat1,X1),
inference(cp,[status(thm)],[t6061,t4236]) ).
cnf(t10091,plain,
meet(sFlat1,meet(sk3,X1)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t6119]) ).
cnf(t266,plain,
meet(X1,join(complement(X1),join(X2,meet(X1,X2)))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t74,t253]) ).
cnf(t42854,plain,
meet(X1,join(complement(X1),join(X2,meet(X1,X2)))) = meet(X1,X2),
inference(step,[status(thm)],[t266,t74]) ).
cnf(t37704,plain,
meet(X1,join(complement(X1),join(X2,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t42854]) ).
cnf(t1335,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t1330,t1153]) ).
cnf(t3866,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t1335]) ).
cnf(t37773,plain,
meet(complement(X1),complement(X2)) = meet(complement(X1),join(complement(complement(X1)),join(complement(X2),complement(join(X1,X2))))),
inference(cp,[status(thm)],[t37704,t3866]) ).
cnf(t42857,plain,
complement(join(X1,X2)) = meet(complement(X1),join(complement(complement(X1)),join(complement(X2),complement(join(X1,X2))))),
inference(step,[status(thm)],[t37773,t3866]) ).
cnf(t42858,plain,
complement(join(X1,X2)) = meet(complement(X1),join(X1,join(complement(X2),complement(join(X1,X2))))),
inference(step,[status(thm)],[t42857,t1153]) ).
cnf(t42859,plain,
complement(join(X1,X2)) = meet(complement(X1),join(X1,complement(meet(X2,join(X1,X2))))),
inference(step,[status(thm)],[t42858,t1310]) ).
cnf(t1417,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t1415,t91]) ).
cnf(t2117,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t1417]) ).
cnf(t9,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t39,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t42,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t27,t39]) ).
cnf(t650,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t42]) ).
cnf(t32,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t27,t30]) ).
cnf(t330,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t32]) ).
cnf(t338,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t330,t25]) ).
cnf(t412,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t338]) ).
cnf(t651,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = join(top,converse(X2)),
inference(cp,[status(thm)],[t650,t412]) ).
cnf(t41706,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = join(top,converse(X2)),
inference(step,[status(thm)],[t651,t25]) ).
cnf(t28,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t27,t25]) ).
cnf(t190,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t28]) ).
cnf(t46,plain,
join(sk2,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t27,t45]) ).
cnf(t110,plain,
join(sk2,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t46]) ).
cnf(t111,plain,
join(one,complement(one)) = join(sk2,top),
inference(cp,[status(thm)],[t110,t30]) ).
cnf(t41034,plain,
top = join(sk2,top),
inference(step,[status(thm)],[t111,t30]) ).
cnf(t41035,plain,
top = join(top,sk2),
inference(step,[status(thm)],[t41034,t25]) ).
cnf(t113,plain,
join(top,sk2) = top,
inference(orient,[status(thm)],[t41035]) ).
cnf(t114,plain,
join(top,join(sk2,X1)) = join(top,X1),
inference(cp,[status(thm)],[t27,t113]) ).
cnf(t394,plain,
join(top,join(sk2,X1)) = join(top,X1),
inference(orient,[status(thm)],[t114]) ).
cnf(t40,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t39,t24]) ).
cnf(t123,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t40]) ).
cnf(t124,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t123,t30]) ).
cnf(t395,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t124]) ).
cnf(t404,plain,
join(top,converse(complement(converse(sk2)))) = join(top,converse(top)),
inference(cp,[status(thm)],[t394,t395]) ).
cnf(t337,plain,
join(top,complement(complement(X1))) = join(X1,top),
inference(cp,[status(thm)],[t330,t30]) ).
cnf(t336,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t330,t302]) ).
cnf(t41057,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t336,t30]) ).
cnf(t352,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t41057]) ).
cnf(t41058,plain,
top = join(X1,top),
inference(step,[status(thm)],[t337,t352]) ).
cnf(t358,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t41058]) ).
cnf(t360,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t123,t358]) ).
cnf(t361,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t360]) ).
cnf(t41097,plain,
join(top,converse(complement(converse(sk2)))) = converse(top),
inference(step,[status(thm)],[t404,t361]) ).
cnf(t692,plain,
join(top,converse(complement(converse(sk2)))) = converse(top),
inference(orient,[status(thm)],[t41097]) ).
cnf(t695,plain,
join(converse(complement(converse(sk2))),join(X1,top)) = join(X1,converse(top)),
inference(cp,[status(thm)],[t190,t692]) ).
cnf(t41098,plain,
join(converse(complement(converse(sk2))),top) = join(X1,converse(top)),
inference(step,[status(thm)],[t695,t358]) ).
cnf(t41099,plain,
top = join(X1,converse(top)),
inference(step,[status(thm)],[t41098,t358]) ).
cnf(t41100,plain,
top = converse(top),
inference(step,[status(thm)],[t41099,t361]) ).
cnf(t696,plain,
converse(top) = top,
inference(orient,[status(thm)],[t41100]) ).
cnf(t709,plain,
converse(join(top,X1)) = join(top,converse(X1)),
inference(cp,[status(thm)],[t39,t696]) ).
cnf(t750,plain,
converse(join(top,X1)) = join(top,converse(X1)),
inference(orient,[status(thm)],[t709]) ).
cnf(t764,plain,
join(top,converse(X1)) = converse(join(X1,top)),
inference(cp,[status(thm)],[t750,t25]) ).
cnf(t41112,plain,
join(top,converse(X1)) = converse(top),
inference(step,[status(thm)],[t764,t358]) ).
cnf(t41113,plain,
join(top,converse(X1)) = top,
inference(step,[status(thm)],[t41112,t696]) ).
cnf(t779,plain,
join(top,converse(X1)) = top,
inference(orient,[status(thm)],[t41113]) ).
cnf(t41707,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t41706,t779]) ).
cnf(t9330,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t41707]) ).
cnf(t9396,plain,
meet(converse(X1),complement(converse(join(X1,X2)))) = complement(top),
inference(cp,[status(thm)],[t1358,t9330]) ).
cnf(t42101,plain,
meet(converse(X1),complement(converse(join(X1,X2)))) = zero,
inference(step,[status(thm)],[t9396,t94]) ).
cnf(t16564,plain,
meet(converse(X1),complement(converse(join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t42101]) ).
cnf(t16635,plain,
converse(X1) = join(zero,meet(complement(complement(converse(join(X1,X2)))),converse(X1))),
inference(cp,[status(thm)],[t2117,t16564]) ).
cnf(t1054,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t1053,t81]) ).
cnf(t41168,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t1054,t74]) ).
cnf(t1102,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t41168]) ).
cnf(t1185,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t74,t1180]) ).
cnf(t41189,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t1185,t1153]) ).
cnf(t1187,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t41189]) ).
cnf(t41191,plain,
join(zero,X1) = X1,
inference(step,[status(thm)],[t1102,t1187]) ).
cnf(t1192,plain,
join(zero,X1) = X1,
inference(rw,[status(thm)],[t41191]) ).
cnf(t1203,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t1192]) ).
cnf(t42102,plain,
converse(X1) = meet(complement(complement(converse(join(X1,X2)))),converse(X1)),
inference(step,[status(thm)],[t16635,t1203]) ).
cnf(t42103,plain,
converse(X1) = meet(converse(X1),complement(complement(converse(join(X1,X2))))),
inference(step,[status(thm)],[t42102,t91]) ).
cnf(t42104,plain,
converse(X1) = meet(converse(X1),converse(join(X1,X2))),
inference(step,[status(thm)],[t42103,t1153]) ).
cnf(t16638,plain,
meet(converse(X1),converse(join(X1,X2))) = converse(X1),
inference(orient,[status(thm)],[t42104]) ).
cnf(t191,plain,
join(X1,converse(join(X2,X3))) = converse(join(X3,join(converse(X1),X2))),
inference(cp,[status(thm)],[t123,t190]) ).
cnf(t1728,plain,
converse(join(X1,join(converse(X2),X3))) = join(X2,converse(join(X3,X1))),
inference(orient,[status(thm)],[t191]) ).
cnf(t188,plain,
composition(join(X1,one),X2) = join(composition(X1,X2),X2),
inference(cp,[status(thm)],[t33,t186]) ).
cnf(t41067,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(step,[status(thm)],[t188,t25]) ).
cnf(t448,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t41067]) ).
cnf(t450,plain,
join(X1,composition(sk2,X1)) = composition(one,X1),
inference(cp,[status(thm)],[t448,t45]) ).
cnf(t41068,plain,
join(X1,composition(sk2,X1)) = X1,
inference(step,[status(thm)],[t450,t186]) ).
cnf(t463,plain,
join(X1,composition(sk2,X1)) = X1,
inference(orient,[status(thm)],[t41068]) ).
cnf(t468,plain,
join(X1,converse(composition(sk2,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t123,t463]) ).
cnf(t53,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t52,t24]) ).
cnf(t141,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t53]) ).
cnf(t41093,plain,
join(X1,composition(X1,converse(sk2))) = converse(converse(X1)),
inference(step,[status(thm)],[t468,t141]) ).
cnf(t41094,plain,
join(X1,composition(X1,converse(sk2))) = X1,
inference(step,[status(thm)],[t41093,t24]) ).
cnf(t632,plain,
join(X1,composition(X1,converse(sk2))) = X1,
inference(orient,[status(thm)],[t41094]) ).
cnf(t1735,plain,
join(X1,converse(join(composition(converse(X1),converse(sk2)),X2))) = converse(join(X2,converse(X1))),
inference(cp,[status(thm)],[t1728,t632]) ).
cnf(t161,plain,
converse(join(composition(converse(X1),X2),X3)) = join(composition(converse(X2),X1),converse(X3)),
inference(cp,[status(thm)],[t39,t153]) ).
cnf(t2677,plain,
converse(join(composition(converse(X1),X2),X3)) = join(composition(converse(X2),X1),converse(X3)),
inference(orient,[status(thm)],[t161]) ).
cnf(t42222,plain,
join(X1,join(composition(converse(converse(sk2)),X1),converse(X2))) = converse(join(X2,converse(X1))),
inference(step,[status(thm)],[t1735,t2677]) ).
cnf(t42223,plain,
join(X1,join(composition(sk2,X1),converse(X2))) = converse(join(X2,converse(X1))),
inference(step,[status(thm)],[t42222,t24]) ).
cnf(t41,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t39,t24]) ).
cnf(t132,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t41]) ).
cnf(t42224,plain,
join(X1,join(composition(sk2,X1),converse(X2))) = join(converse(X2),X1),
inference(step,[status(thm)],[t42223,t132]) ).
cnf(t19725,plain,
join(X1,join(composition(sk2,X1),converse(X2))) = join(converse(X2),X1),
inference(orient,[status(thm)],[t42224]) ).
cnf(t19782,plain,
converse(X1) = meet(converse(X1),converse(join(converse(X2),X1))),
inference(cp,[status(thm)],[t16638,t19725]) ).
cnf(t42339,plain,
converse(X1) = meet(converse(X1),join(X2,converse(X1))),
inference(step,[status(thm)],[t19782,t123]) ).
cnf(t22999,plain,
meet(converse(X1),join(X2,converse(X1))) = converse(X1),
inference(orient,[status(thm)],[t42339]) ).
cnf(t23021,plain,
converse(converse(X1)) = meet(X1,join(X2,converse(converse(X1)))),
inference(cp,[status(thm)],[t22999,t24]) ).
cnf(t42340,plain,
X1 = meet(X1,join(X2,converse(converse(X1)))),
inference(step,[status(thm)],[t23021,t24]) ).
cnf(t42341,plain,
X1 = meet(X1,join(X2,X1)),
inference(step,[status(thm)],[t42340,t24]) ).
cnf(t23073,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t42341]) ).
cnf(t42860,plain,
complement(join(X1,X2)) = meet(complement(X1),join(X1,complement(X2))),
inference(step,[status(thm)],[t42859,t23073]) ).
cnf(t38106,plain,
meet(complement(X1),join(X1,complement(X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t42860]) ).
cnf(t38124,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),join(X1,X2)),
inference(cp,[status(thm)],[t38106,t1153]) ).
cnf(t42886,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t38124,t1330]) ).
cnf(t38448,plain,
meet(complement(X1),join(X1,X2)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t42886]) ).
cnf(t2,axiom,
join(sk1,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t43,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t451,plain,
join(X1,composition(sk1,X1)) = composition(one,X1),
inference(cp,[status(thm)],[t448,t43]) ).
cnf(t41069,plain,
join(X1,composition(sk1,X1)) = X1,
inference(step,[status(thm)],[t451,t186]) ).
cnf(t469,plain,
join(X1,composition(sk1,X1)) = X1,
inference(orient,[status(thm)],[t41069]) ).
cnf(t474,plain,
join(X1,converse(composition(sk1,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t123,t469]) ).
cnf(t41095,plain,
join(X1,composition(X1,converse(sk1))) = converse(converse(X1)),
inference(step,[status(thm)],[t474,t141]) ).
cnf(t41096,plain,
join(X1,composition(X1,converse(sk1))) = X1,
inference(step,[status(thm)],[t41095,t24]) ).
cnf(t641,plain,
join(X1,composition(X1,converse(sk1))) = X1,
inference(orient,[status(thm)],[t41096]) ).
cnf(t1736,plain,
join(X1,converse(join(composition(converse(X1),converse(sk1)),X2))) = converse(join(X2,converse(X1))),
inference(cp,[status(thm)],[t1728,t641]) ).
cnf(t41682,plain,
join(X1,join(composition(converse(converse(sk1)),X1),converse(X2))) = converse(join(X2,converse(X1))),
inference(step,[status(thm)],[t1736,t2677]) ).
cnf(t41683,plain,
join(X1,join(composition(sk1,X1),converse(X2))) = converse(join(X2,converse(X1))),
inference(step,[status(thm)],[t41682,t24]) ).
cnf(t41684,plain,
join(X1,join(composition(sk1,X1),converse(X2))) = join(converse(X2),X1),
inference(step,[status(thm)],[t41683,t132]) ).
cnf(t8630,plain,
join(X1,join(composition(sk1,X1),converse(X2))) = join(converse(X2),X1),
inference(orient,[status(thm)],[t41684]) ).
cnf(t8664,plain,
join(converse(converse(X1)),X2) = join(X2,join(composition(sk1,X2),X1)),
inference(cp,[status(thm)],[t8630,t24]) ).
cnf(t41689,plain,
join(X1,X2) = join(X2,join(composition(sk1,X2),X1)),
inference(step,[status(thm)],[t8664,t24]) ).
cnf(t8874,plain,
join(X1,join(composition(sk1,X1),X2)) = join(X2,X1),
inference(orient,[status(thm)],[t41689]) ).
cnf(t8931,plain,
join(X1,X2) = join(X2,join(X1,composition(sk1,X2))),
inference(cp,[status(thm)],[t8874,t25]) ).
cnf(t9037,plain,
join(X1,join(X2,composition(sk1,X1))) = join(X2,X1),
inference(orient,[status(thm)],[t8931]) ).
cnf(t162,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t39,t153]) ).
cnf(t2747,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t162]) ).
cnf(t56,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t33,t52]) ).
cnf(t6912,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t56]) ).
cnf(t6994,plain,
join(converse(converse(composition(X1,X2))),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(cp,[status(thm)],[t2747,t6912]) ).
cnf(t41579,plain,
join(composition(X1,X2),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t6994,t24]) ).
cnf(t41580,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t41579,t24]) ).
cnf(t128,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t52,t123]) ).
cnf(t2184,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t128]) ).
cnf(t41581,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(converse(converse(X1)),join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t41580,t2184]) ).
cnf(t41582,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t41581,t24]) ).
cnf(t41583,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t41582,t24]) ).
cnf(t7002,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t41583]) ).
cnf(t7050,plain,
composition(sk1,join(sk3,X1)) = join(sFlat0,composition(sk1,X1)),
inference(cp,[status(thm)],[t7002,t59]) ).
cnf(t7263,plain,
composition(sk1,join(sk3,X1)) = join(sFlat0,composition(sk1,X1)),
inference(orient,[status(thm)],[t7050]) ).
cnf(t7304,plain,
join(sFlat0,composition(sk1,complement(sk3))) = composition(sk1,top),
inference(cp,[status(thm)],[t7263,t30]) ).
cnf(t7543,plain,
join(sFlat0,composition(sk1,complement(sk3))) = composition(sk1,top),
inference(orient,[status(thm)],[t7304]) ).
cnf(t9047,plain,
join(sFlat0,complement(sk3)) = join(complement(sk3),composition(sk1,top)),
inference(cp,[status(thm)],[t9037,t7543]) ).
cnf(t9323,plain,
join(complement(sk3),composition(sk1,top)) = join(sFlat0,complement(sk3)),
inference(orient,[status(thm)],[t9047]) ).
cnf(t38615,plain,
meet(complement(complement(sk3)),composition(sk1,top)) = meet(complement(complement(sk3)),join(sFlat0,complement(sk3))),
inference(cp,[status(thm)],[t38448,t9323]) ).
cnf(t42898,plain,
meet(composition(sk1,top),complement(complement(sk3))) = meet(complement(complement(sk3)),join(sFlat0,complement(sk3))),
inference(step,[status(thm)],[t38615,t91]) ).
cnf(t42899,plain,
meet(composition(sk1,top),sk3) = meet(complement(complement(sk3)),join(sFlat0,complement(sk3))),
inference(step,[status(thm)],[t42898,t1153]) ).
cnf(t42900,plain,
meet(sk3,composition(sk1,top)) = meet(complement(complement(sk3)),join(sFlat0,complement(sk3))),
inference(step,[status(thm)],[t42899,t91]) ).
cnf(t42901,plain,
meet(sk3,composition(sk1,top)) = meet(sk3,join(sFlat0,complement(sk3))),
inference(step,[status(thm)],[t42900,t1153]) ).
cnf(t1342,plain,
meet(complement(X1),join(X2,complement(X3))) = complement(join(X1,meet(complement(X2),X3))),
inference(cp,[status(thm)],[t1330,t1330]) ).
cnf(t12565,plain,
complement(join(X1,meet(complement(X2),X3))) = meet(complement(X1),join(X2,complement(X3))),
inference(orient,[status(thm)],[t1342]) ).
cnf(t12569,plain,
meet(complement(meet(complement(X1),X2)),join(X1,complement(complement(X2)))) = complement(complement(X1)),
inference(cp,[status(thm)],[t12565,t1415]) ).
cnf(t41820,plain,
meet(join(X1,complement(complement(X2))),complement(meet(complement(X1),X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t12569,t91]) ).
cnf(t41821,plain,
meet(join(X1,X2),complement(meet(complement(X1),X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t41820,t1153]) ).
cnf(t41822,plain,
meet(join(X1,X2),join(X1,complement(X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t41821,t3814]) ).
cnf(t41823,plain,
meet(join(X1,X2),join(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t41822,t1153]) ).
cnf(t12666,plain,
meet(join(X1,X2),join(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t41823]) ).
cnf(t61,plain,
composition(join(sk1,X1),sk3) = join(sFlat0,composition(X1,sk3)),
inference(cp,[status(thm)],[t33,t59]) ).
cnf(t222,plain,
composition(join(sk1,X1),sk3) = join(sFlat0,composition(X1,sk3)),
inference(orient,[status(thm)],[t61]) ).
cnf(t223,plain,
join(sFlat0,composition(one,sk3)) = composition(one,sk3),
inference(cp,[status(thm)],[t222,t43]) ).
cnf(t41043,plain,
join(sFlat0,sk3) = composition(one,sk3),
inference(step,[status(thm)],[t223,t186]) ).
cnf(t41044,plain,
join(sFlat0,sk3) = sk3,
inference(step,[status(thm)],[t41043,t186]) ).
cnf(t233,plain,
join(sFlat0,sk3) = sk3,
inference(orient,[status(thm)],[t41044]) ).
cnf(t12745,plain,
sFlat0 = meet(sk3,join(sFlat0,complement(sk3))),
inference(cp,[status(thm)],[t12666,t233]) ).
cnf(t12864,plain,
meet(sk3,join(sFlat0,complement(sk3))) = sFlat0,
inference(orient,[status(thm)],[t12745]) ).
cnf(t42902,plain,
meet(sk3,composition(sk1,top)) = sFlat0,
inference(step,[status(thm)],[t42901,t12864]) ).
cnf(t38886,plain,
meet(sk3,composition(sk1,top)) = sFlat0,
inference(orient,[status(thm)],[t42902]) ).
cnf(t38887,plain,
meet(sFlat1,composition(sk1,top)) = meet(sFlat1,sFlat0),
inference(cp,[status(thm)],[t10091,t38886]) ).
cnf(t42955,plain,
meet(sFlat1,composition(sk1,top)) = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t38887,t91]) ).
cnf(t42956,plain,
meet(sFlat1,composition(sk1,top)) = sFlat2,
inference(step,[status(thm)],[t42955,t83]) ).
cnf(t40011,plain,
meet(sFlat1,composition(sk1,top)) = sFlat2,
inference(orient,[status(thm)],[t42956]) ).
cnf(t8877,plain,
join(composition(sk1,X1),X2) = join(X2,composition(sk1,join(X2,X1))),
inference(cp,[status(thm)],[t8874,t7002]) ).
cnf(t14214,plain,
join(X1,composition(sk1,join(X1,X2))) = join(composition(sk1,X2),X1),
inference(orient,[status(thm)],[t8877]) ).
cnf(t14273,plain,
join(composition(sk1,complement(X1)),X1) = join(X1,composition(sk1,top)),
inference(cp,[status(thm)],[t14214,t30]) ).
cnf(t41984,plain,
join(X1,composition(sk1,complement(X1))) = join(X1,composition(sk1,top)),
inference(step,[status(thm)],[t14273,t25]) ).
cnf(t14681,plain,
join(X1,composition(sk1,complement(X1))) = join(X1,composition(sk1,top)),
inference(orient,[status(thm)],[t41984]) ).
cnf(t14687,plain,
join(complement(X1),composition(sk1,top)) = join(complement(X1),composition(sk1,X1)),
inference(cp,[status(thm)],[t14681,t1153]) ).
cnf(t40778,plain,
join(complement(X1),composition(sk1,top)) = join(complement(X1),composition(sk1,X1)),
inference(orient,[status(thm)],[t14687]) ).
cnf(t40780,plain,
meet(complement(complement(X1)),composition(sk1,top)) = meet(complement(complement(X1)),join(complement(X1),composition(sk1,X1))),
inference(cp,[status(thm)],[t38448,t40778]) ).
cnf(t42984,plain,
meet(X1,composition(sk1,top)) = meet(complement(complement(X1)),join(complement(X1),composition(sk1,X1))),
inference(step,[status(thm)],[t40780,t1153]) ).
cnf(t42985,plain,
meet(X1,composition(sk1,top)) = meet(complement(complement(X1)),composition(sk1,X1)),
inference(step,[status(thm)],[t42984,t38448]) ).
cnf(t42986,plain,
meet(X1,composition(sk1,top)) = meet(X1,composition(sk1,X1)),
inference(step,[status(thm)],[t42985,t1153]) ).
cnf(t5626,plain,
meet(complement(join(X1,X2)),X2) = complement(join(X1,top)),
inference(cp,[status(thm)],[t5619,t30]) ).
cnf(t41490,plain,
meet(X2,complement(join(X1,X2))) = complement(join(X1,top)),
inference(step,[status(thm)],[t5626,t91]) ).
cnf(t41491,plain,
meet(X2,complement(join(X1,X2))) = complement(top),
inference(step,[status(thm)],[t41490,t358]) ).
cnf(t41492,plain,
meet(X2,complement(join(X1,X2))) = zero,
inference(step,[status(thm)],[t41491,t94]) ).
cnf(t5718,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t41492]) ).
cnf(t5744,plain,
zero = meet(composition(sk1,X1),complement(X1)),
inference(cp,[status(thm)],[t5718,t469]) ).
cnf(t41511,plain,
zero = meet(complement(X1),composition(sk1,X1)),
inference(step,[status(thm)],[t5744,t91]) ).
cnf(t5888,plain,
meet(complement(X1),composition(sk1,X1)) = zero,
inference(orient,[status(thm)],[t41511]) ).
cnf(t5900,plain,
composition(sk1,X1) = join(meet(composition(sk1,X1),X1),zero),
inference(cp,[status(thm)],[t2117,t5888]) ).
cnf(t1216,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t1203,t25]) ).
cnf(t1233,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t1216]) ).
cnf(t41512,plain,
composition(sk1,X1) = meet(composition(sk1,X1),X1),
inference(step,[status(thm)],[t5900,t1233]) ).
cnf(t41513,plain,
composition(sk1,X1) = meet(X1,composition(sk1,X1)),
inference(step,[status(thm)],[t41512,t91]) ).
cnf(t5902,plain,
meet(X1,composition(sk1,X1)) = composition(sk1,X1),
inference(orient,[status(thm)],[t41513]) ).
cnf(t42987,plain,
meet(X1,composition(sk1,top)) = composition(sk1,X1),
inference(step,[status(thm)],[t42986,t5902]) ).
cnf(t40834,plain,
meet(X1,composition(sk1,top)) = composition(sk1,X1),
inference(orient,[status(thm)],[t42987]) ).
cnf(t42988,plain,
composition(sk1,sFlat1) = sFlat2,
inference(step,[status(thm)],[t40011,t40834]) ).
cnf(t31,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t30,t27]) ).
cnf(t490,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t31]) ).
cnf(t12695,plain,
X1 = meet(top,join(X1,complement(join(X2,complement(join(X1,X2)))))),
inference(cp,[status(thm)],[t12666,t490]) ).
cnf(t1158,plain,
complement(complement(X1)) = meet(top,X1),
inference(cp,[status(thm)],[t1115,t1153]) ).
cnf(t41195,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t1158,t1153]) ).
cnf(t1196,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t41195]) ).
cnf(t42477,plain,
X1 = join(X1,complement(join(X2,complement(join(X1,X2))))),
inference(step,[status(thm)],[t12695,t1196]) ).
cnf(t42478,plain,
X1 = join(X1,meet(complement(X2),join(X1,X2))),
inference(step,[status(thm)],[t42477,t1330]) ).
cnf(t27616,plain,
join(X1,meet(complement(X2),join(X1,X2))) = X1,
inference(orient,[status(thm)],[t42478]) ).
cnf(t9049,plain,
join(composition(sk1,X1),X2) = join(X2,composition(sk1,join(X1,X2))),
inference(cp,[status(thm)],[t9037,t7002]) ).
cnf(t31740,plain,
join(X1,composition(sk1,join(X2,X1))) = join(composition(sk1,X2),X1),
inference(orient,[status(thm)],[t9049]) ).
cnf(t1318,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t1310,t1153]) ).
cnf(t3840,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t1318]) ).
cnf(t88,plain,
composition(join(sFlat3,X1),sk3) = join(sFlat4,composition(X1,sk3)),
inference(cp,[status(thm)],[t33,t86]) ).
cnf(t374,plain,
composition(join(sFlat3,X1),sk3) = join(sFlat4,composition(X1,sk3)),
inference(orient,[status(thm)],[t88]) ).
cnf(t1424,plain,
sk2 = join(sk2,sFlat3),
inference(cp,[status(thm)],[t1422,t93]) ).
cnf(t41240,plain,
sk2 = join(sFlat3,sk2),
inference(step,[status(thm)],[t1424,t25]) ).
cnf(t1434,plain,
join(sFlat3,sk2) = sk2,
inference(orient,[status(thm)],[t41240]) ).
cnf(t1435,plain,
join(sFlat4,composition(sk2,sk3)) = composition(sk2,sk3),
inference(cp,[status(thm)],[t374,t1434]) ).
cnf(t41241,plain,
join(sFlat4,sFlat1) = composition(sk2,sk3),
inference(step,[status(thm)],[t1435,t64]) ).
cnf(t41242,plain,
join(sFlat1,sFlat4) = composition(sk2,sk3),
inference(step,[status(thm)],[t41241,t25]) ).
cnf(t41243,plain,
join(sFlat1,sFlat4) = sFlat1,
inference(step,[status(thm)],[t41242,t64]) ).
cnf(t1437,plain,
join(sFlat1,sFlat4) = sFlat1,
inference(orient,[status(thm)],[t41243]) ).
cnf(t5762,plain,
zero = meet(sFlat4,complement(sFlat1)),
inference(cp,[status(thm)],[t5718,t1437]) ).
cnf(t5809,plain,
meet(sFlat4,complement(sFlat1)) = zero,
inference(orient,[status(thm)],[t5762]) ).
cnf(t5810,plain,
join(complement(sFlat4),sFlat1) = complement(zero),
inference(cp,[status(thm)],[t3840,t5809]) ).
cnf(t41503,plain,
join(sFlat1,complement(sFlat4)) = complement(zero),
inference(step,[status(thm)],[t5810,t25]) ).
cnf(t1133,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t1132,t30]) ).
cnf(t1141,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t1133]) ).
cnf(t41504,plain,
join(sFlat1,complement(sFlat4)) = top,
inference(step,[status(thm)],[t41503,t1141]) ).
cnf(t5826,plain,
join(sFlat1,complement(sFlat4)) = top,
inference(orient,[status(thm)],[t41504]) ).
cnf(t31897,plain,
join(composition(sk1,sFlat1),complement(sFlat4)) = join(complement(sFlat4),composition(sk1,top)),
inference(cp,[status(thm)],[t31740,t5826]) ).
cnf(t42828,plain,
join(complement(sFlat4),composition(sk1,sFlat1)) = join(complement(sFlat4),composition(sk1,top)),
inference(step,[status(thm)],[t31897,t25]) ).
cnf(t1323,plain,
join(top,complement(X1)) = join(X2,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t412,t1310]) ).
cnf(t41345,plain,
top = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t1323,t352]) ).
cnf(t2950,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t41345]) ).
cnf(t178,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t39,t175]) ).
cnf(t195,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t178]) ).
cnf(t133,plain,
join(converse(join(X1,X2)),X3) = converse(join(X1,join(X2,converse(X3)))),
inference(cp,[status(thm)],[t132,t27]) ).
cnf(t1443,plain,
converse(join(X1,join(X2,converse(X3)))) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t133]) ).
cnf(t1451,plain,
join(converse(join(X1,X2)),one) = converse(join(X1,join(X2,one))),
inference(cp,[status(thm)],[t1443,t175]) ).
cnf(t41248,plain,
join(one,converse(join(X1,X2))) = converse(join(X1,join(X2,one))),
inference(step,[status(thm)],[t1451,t25]) ).
cnf(t1480,plain,
converse(join(X1,join(X2,one))) = join(one,converse(join(X1,X2))),
inference(orient,[status(thm)],[t41248]) ).
cnf(t1484,plain,
join(one,converse(join(X1,sk2))) = converse(join(X1,one)),
inference(cp,[status(thm)],[t1480,t45]) ).
cnf(t179,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t39,t175]) ).
cnf(t41040,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t179,t25]) ).
cnf(t208,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t41040]) ).
cnf(t41287,plain,
join(one,converse(join(X1,sk2))) = join(one,converse(X1)),
inference(step,[status(thm)],[t1484,t208]) ).
cnf(t1666,plain,
join(one,converse(join(X1,sk2))) = join(one,converse(X1)),
inference(orient,[status(thm)],[t41287]) ).
cnf(t1667,plain,
join(one,converse(sFlat3)) = join(one,converse(sk2)),
inference(cp,[status(thm)],[t1666,t1434]) ).
cnf(t209,plain,
join(one,converse(sk2)) = converse(one),
inference(cp,[status(thm)],[t208,t45]) ).
cnf(t41041,plain,
join(one,converse(sk2)) = one,
inference(step,[status(thm)],[t209,t175]) ).
cnf(t220,plain,
join(one,converse(sk2)) = one,
inference(orient,[status(thm)],[t41041]) ).
cnf(t41288,plain,
join(one,converse(sFlat3)) = one,
inference(step,[status(thm)],[t1667,t220]) ).
cnf(t1672,plain,
join(one,converse(sFlat3)) = one,
inference(orient,[status(thm)],[t41288]) ).
cnf(t1673,plain,
join(one,converse(converse(sFlat3))) = converse(one),
inference(cp,[status(thm)],[t195,t1672]) ).
cnf(t41289,plain,
join(one,sFlat3) = converse(one),
inference(step,[status(thm)],[t1673,t24]) ).
cnf(t41290,plain,
join(sFlat3,one) = converse(one),
inference(step,[status(thm)],[t41289,t25]) ).
cnf(t41291,plain,
join(sFlat3,one) = one,
inference(step,[status(thm)],[t41290,t175]) ).
cnf(t1678,plain,
join(sFlat3,one) = one,
inference(orient,[status(thm)],[t41291]) ).
cnf(t1679,plain,
join(sFlat4,composition(one,sk3)) = composition(one,sk3),
inference(cp,[status(thm)],[t374,t1678]) ).
cnf(t41292,plain,
join(sFlat4,sk3) = composition(one,sk3),
inference(step,[status(thm)],[t1679,t186]) ).
cnf(t41293,plain,
join(sFlat4,sk3) = sk3,
inference(step,[status(thm)],[t41292,t186]) ).
cnf(t1682,plain,
join(sFlat4,sk3) = sk3,
inference(orient,[status(thm)],[t41293]) ).
cnf(t4213,plain,
sFlat4 = meet(sFlat4,sk3),
inference(cp,[status(thm)],[t4212,t1682]) ).
cnf(t4343,plain,
meet(sFlat4,sk3) = sFlat4,
inference(orient,[status(thm)],[t4213]) ).
cnf(t4344,plain,
top = join(sk3,complement(sFlat4)),
inference(cp,[status(thm)],[t2950,t4343]) ).
cnf(t4700,plain,
join(sk3,complement(sFlat4)) = top,
inference(orient,[status(thm)],[t4344]) ).
cnf(t7274,plain,
join(sFlat0,composition(sk1,complement(sFlat4))) = composition(sk1,top),
inference(cp,[status(thm)],[t7263,t4700]) ).
cnf(t7538,plain,
join(sFlat0,composition(sk1,complement(sFlat4))) = composition(sk1,top),
inference(orient,[status(thm)],[t7274]) ).
cnf(t9046,plain,
join(sFlat0,complement(sFlat4)) = join(complement(sFlat4),composition(sk1,top)),
inference(cp,[status(thm)],[t9037,t7538]) ).
cnf(t9316,plain,
join(complement(sFlat4),composition(sk1,top)) = join(sFlat0,complement(sFlat4)),
inference(orient,[status(thm)],[t9046]) ).
cnf(t2953,plain,
top = join(sk1,complement(sFlat3)),
inference(cp,[status(thm)],[t2950,t93]) ).
cnf(t2974,plain,
join(sk1,complement(sFlat3)) = top,
inference(orient,[status(thm)],[t2953]) ).
cnf(t12782,plain,
sk1 = meet(top,join(sk1,complement(complement(sFlat3)))),
inference(cp,[status(thm)],[t12666,t2974]) ).
cnf(t41824,plain,
sk1 = join(sk1,complement(complement(sFlat3))),
inference(step,[status(thm)],[t12782,t1196]) ).
cnf(t41825,plain,
sk1 = join(sk1,sFlat3),
inference(step,[status(thm)],[t41824,t1153]) ).
cnf(t41826,plain,
sk1 = join(sFlat3,sk1),
inference(step,[status(thm)],[t41825,t25]) ).
cnf(t12814,plain,
join(sFlat3,sk1) = sk1,
inference(orient,[status(thm)],[t41826]) ).
cnf(t12815,plain,
join(sFlat4,composition(sk1,sk3)) = composition(sk1,sk3),
inference(cp,[status(thm)],[t374,t12814]) ).
cnf(t41829,plain,
join(sFlat4,sFlat0) = composition(sk1,sk3),
inference(step,[status(thm)],[t12815,t59]) ).
cnf(t41830,plain,
join(sFlat0,sFlat4) = composition(sk1,sk3),
inference(step,[status(thm)],[t41829,t25]) ).
cnf(t41831,plain,
join(sFlat0,sFlat4) = sFlat0,
inference(step,[status(thm)],[t41830,t59]) ).
cnf(t12822,plain,
join(sFlat0,sFlat4) = sFlat0,
inference(orient,[status(thm)],[t41831]) ).
cnf(t12823,plain,
zero = meet(sFlat4,complement(sFlat0)),
inference(cp,[status(thm)],[t5718,t12822]) ).
cnf(t12826,plain,
meet(sFlat4,complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t12823]) ).
cnf(t12827,plain,
join(complement(sFlat4),sFlat0) = complement(zero),
inference(cp,[status(thm)],[t3840,t12826]) ).
cnf(t41838,plain,
join(sFlat0,complement(sFlat4)) = complement(zero),
inference(step,[status(thm)],[t12827,t25]) ).
cnf(t41839,plain,
join(sFlat0,complement(sFlat4)) = top,
inference(step,[status(thm)],[t41838,t1141]) ).
cnf(t12844,plain,
join(sFlat0,complement(sFlat4)) = top,
inference(orient,[status(thm)],[t41839]) ).
cnf(t41840,plain,
join(complement(sFlat4),composition(sk1,top)) = top,
inference(step,[status(thm)],[t9316,t12844]) ).
cnf(t12845,plain,
join(complement(sFlat4),composition(sk1,top)) = top,
inference(orient,[status(thm)],[t41840]) ).
cnf(t42829,plain,
join(complement(sFlat4),composition(sk1,sFlat1)) = top,
inference(step,[status(thm)],[t42828,t12845]) ).
cnf(t37105,plain,
join(complement(sFlat4),composition(sk1,sFlat1)) = top,
inference(orient,[status(thm)],[t42829]) ).
cnf(t37108,plain,
complement(sFlat4) = join(complement(sFlat4),meet(complement(composition(sk1,sFlat1)),top)),
inference(cp,[status(thm)],[t27616,t37105]) ).
cnf(t1197,plain,
X1 = meet(X1,top),
inference(cp,[status(thm)],[t1196,t91]) ).
cnf(t1229,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t1197]) ).
cnf(t42830,plain,
complement(sFlat4) = join(complement(sFlat4),complement(composition(sk1,sFlat1))),
inference(step,[status(thm)],[t37108,t1229]) ).
cnf(t42831,plain,
complement(sFlat4) = complement(meet(sFlat4,composition(sk1,sFlat1))),
inference(step,[status(thm)],[t42830,t1310]) ).
cnf(t1425,plain,
join(sFlat4,composition(meet(sFlat3,X1),sk3)) = composition(sFlat3,sk3),
inference(cp,[status(thm)],[t374,t1422]) ).
cnf(t41749,plain,
join(sFlat4,composition(meet(sFlat3,X1),sk3)) = sFlat4,
inference(step,[status(thm)],[t1425,t86]) ).
cnf(t10125,plain,
join(sFlat4,composition(meet(sFlat3,X1),sk3)) = sFlat4,
inference(orient,[status(thm)],[t41749]) ).
cnf(t6144,plain,
meet(sk2,meet(sk1,X1)) = meet(sFlat3,X1),
inference(cp,[status(thm)],[t6061,t93]) ).
cnf(t6200,plain,
meet(sk2,meet(sk1,X1)) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t6144]) ).
cnf(t187,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t33,t186]) ).
cnf(t424,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t187]) ).
cnf(t428,plain,
join(X1,composition(converse(sk2),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t424,t220]) ).
cnf(t41085,plain,
join(X1,composition(converse(sk2),X1)) = X1,
inference(step,[status(thm)],[t428,t186]) ).
cnf(t586,plain,
join(X1,composition(converse(sk2),X1)) = X1,
inference(orient,[status(thm)],[t41085]) ).
cnf(t592,plain,
join(X1,converse(composition(converse(sk2),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t123,t586]) ).
cnf(t41086,plain,
join(X1,composition(converse(converse(X1)),sk2)) = converse(converse(X1)),
inference(step,[status(thm)],[t592,t153]) ).
cnf(t41087,plain,
join(X1,composition(X1,sk2)) = converse(converse(X1)),
inference(step,[status(thm)],[t41086,t24]) ).
cnf(t41088,plain,
join(X1,composition(X1,sk2)) = X1,
inference(step,[status(thm)],[t41087,t24]) ).
cnf(t595,plain,
join(X1,composition(X1,sk2)) = X1,
inference(orient,[status(thm)],[t41088]) ).
cnf(t5737,plain,
zero = meet(composition(X1,sk2),complement(X1)),
inference(cp,[status(thm)],[t5718,t595]) ).
cnf(t41505,plain,
zero = meet(complement(X1),composition(X1,sk2)),
inference(step,[status(thm)],[t5737,t91]) ).
cnf(t5828,plain,
meet(complement(X1),composition(X1,sk2)) = zero,
inference(orient,[status(thm)],[t41505]) ).
cnf(t5843,plain,
composition(X1,sk2) = join(meet(composition(X1,sk2),X1),zero),
inference(cp,[status(thm)],[t2117,t5828]) ).
cnf(t41506,plain,
composition(X1,sk2) = meet(composition(X1,sk2),X1),
inference(step,[status(thm)],[t5843,t1233]) ).
cnf(t41507,plain,
composition(X1,sk2) = meet(X1,composition(X1,sk2)),
inference(step,[status(thm)],[t41506,t91]) ).
cnf(t5845,plain,
meet(X1,composition(X1,sk2)) = composition(X1,sk2),
inference(orient,[status(thm)],[t41507]) ).
cnf(t6219,plain,
meet(sFlat3,composition(sk1,sk2)) = meet(sk2,composition(sk1,sk2)),
inference(cp,[status(thm)],[t6200,t5845]) ).
cnf(t41614,plain,
meet(sFlat3,composition(sk1,sk2)) = composition(sk1,sk2),
inference(step,[status(thm)],[t6219,t5902]) ).
cnf(t7870,plain,
meet(sFlat3,composition(sk1,sk2)) = composition(sk1,sk2),
inference(orient,[status(thm)],[t41614]) ).
cnf(t10126,plain,
sFlat4 = join(sFlat4,composition(composition(sk1,sk2),sk3)),
inference(cp,[status(thm)],[t10125,t7870]) ).
cnf(t41750,plain,
sFlat4 = join(sFlat4,composition(sk1,composition(sk2,sk3))),
inference(step,[status(thm)],[t10126,t47]) ).
cnf(t41751,plain,
sFlat4 = join(sFlat4,composition(sk1,sFlat1)),
inference(step,[status(thm)],[t41750,t64]) ).
cnf(t10133,plain,
join(sFlat4,composition(sk1,sFlat1)) = sFlat4,
inference(orient,[status(thm)],[t41751]) ).
cnf(t23197,plain,
composition(sk1,sFlat1) = meet(composition(sk1,sFlat1),sFlat4),
inference(cp,[status(thm)],[t23073,t10133]) ).
cnf(t42355,plain,
composition(sk1,sFlat1) = meet(sFlat4,composition(sk1,sFlat1)),
inference(step,[status(thm)],[t23197,t91]) ).
cnf(t23544,plain,
meet(sFlat4,composition(sk1,sFlat1)) = composition(sk1,sFlat1),
inference(orient,[status(thm)],[t42355]) ).
cnf(t42832,plain,
complement(sFlat4) = complement(composition(sk1,sFlat1)),
inference(step,[status(thm)],[t42831,t23544]) ).
cnf(t37114,plain,
complement(composition(sk1,sFlat1)) = complement(sFlat4),
inference(orient,[status(thm)],[t42832]) ).
cnf(t37127,plain,
composition(sk1,sFlat1) = complement(complement(sFlat4)),
inference(cp,[status(thm)],[t1153,t37114]) ).
cnf(t42833,plain,
composition(sk1,sFlat1) = sFlat4,
inference(step,[status(thm)],[t37127,t1153]) ).
cnf(t37207,plain,
composition(sk1,sFlat1) = sFlat4,
inference(orient,[status(thm)],[t42833]) ).
cnf(t42989,plain,
sFlat4 = sFlat2,
inference(step,[status(thm)],[t42988,t37207]) ).
cnf(t40880,plain,
sFlat4 = sFlat2,
inference(rw,[status(thm)],[t42989]) ).
cnf(t40887,plain,
sFlat4 = sFlat2,
inference(orient,[status(thm)],[t40880]) ).
cnf(t42996,plain,
composition(sFlat3,sk3) = sFlat2,
inference(step,[status(thm)],[t86,t40887]) ).
cnf(t40888,plain,
composition(sFlat3,sk3) = sFlat2,
inference(orient,[status(thm)],[t42996]) ).
cnf(goal_0,negated_conjecture,
meet(composition(sk1,sk3),composition(sk2,sk3)) != composition(meet(sk1,sk2),sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(composition(sk2,sk3),composition(sk1,sk3)) != composition(meet(sk1,sk2),sk3),
inference(rw,[status(thm)],[goal_0,t91]) ).
cnf(g0_1,plain,
meet(sFlat1,composition(sk1,sk3)) != composition(meet(sk1,sk2),sk3),
inference(rw,[status(thm)],[g0_0,t64]) ).
cnf(g0_2,plain,
meet(sFlat1,sFlat0) != composition(meet(sk1,sk2),sk3),
inference(rw,[status(thm)],[g0_1,t59]) ).
cnf(g0_3,plain,
meet(sFlat0,sFlat1) != composition(meet(sk1,sk2),sk3),
inference(rw,[status(thm)],[g0_2,t91]) ).
cnf(g0_4,plain,
sFlat2 != composition(meet(sk1,sk2),sk3),
inference(rw,[status(thm)],[g0_3,t83]) ).
cnf(g0_5,plain,
sFlat2 != composition(meet(sk2,sk1),sk3),
inference(rw,[status(thm)],[g0_4,t91]) ).
cnf(g0_6,plain,
sFlat2 != composition(sFlat3,sk3),
inference(rw,[status(thm)],[g0_5,t93]) ).
cnf(g0_7,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_6,t40888]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL029-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n002.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 07:26:53 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 101.90/13.55 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 101.90/13.55 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------