%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL012-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 : n017.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:34:43 PM UTC 2026
% Result : Unsatisfiable 110.76s 14.97s
% Output : CNFRefutation 110.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 106
% Number of leaves : 19
% Syntax : Number of clauses : 514 ( 514 unt; 0 nHn; 163 RR)
% Number of literals : 514 ( 513 equ; 10 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 : 544 ( 30 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t68,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t17,axiom,
sFlat4 = complement(sk1),
introduced(definition) ).
cnf(t40,plain,
complement(sk1) = sFlat4,
inference(orient,[status(thm)],[t17]) ).
cnf(t13,axiom,
sFlat0 = composition(sk1,sk2),
introduced(definition) ).
cnf(t62,plain,
composition(sk1,sk2) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sFlat1 = complement(composition(sk1,sk2)),
introduced(definition) ).
cnf(t27,plain,
complement(composition(sk1,sk2)) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t47596,plain,
complement(sFlat0) = sFlat1,
inference(step,[status(thm)],[t27,t62]) ).
cnf(t67,plain,
complement(sFlat0) = sFlat1,
inference(rw,[status(thm)],[t47596]) ).
cnf(t98,plain,
complement(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t67]) ).
cnf(t15,axiom,
sFlat2 = converse(sk2),
introduced(definition) ).
cnf(t87,plain,
converse(sk2) = sFlat2,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sFlat3 = composition(complement(composition(sk1,sk2)),converse(sk2)),
introduced(definition) ).
cnf(t47595,plain,
sFlat3 = composition(sFlat1,converse(sk2)),
inference(step,[status(thm)],[t16,t27]) ).
cnf(t47,plain,
composition(sFlat1,converse(sk2)) = sFlat3,
inference(orient,[status(thm)],[t47595]) ).
cnf(t47600,plain,
composition(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t47,t87]) ).
cnf(t93,plain,
composition(sFlat1,sFlat2) = sFlat3,
inference(rw,[status(thm)],[t47600]) ).
cnf(t110,plain,
composition(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t93]) ).
cnf(t18,axiom,
sFlat5 = join(composition(complement(composition(sk1,sk2)),converse(sk2)),complement(sk1)),
introduced(definition) ).
cnf(t47597,plain,
sFlat5 = join(complement(sk1),composition(complement(composition(sk1,sk2)),converse(sk2))),
inference(step,[status(thm)],[t18,t68]) ).
cnf(t47598,plain,
sFlat5 = join(sFlat4,composition(complement(composition(sk1,sk2)),converse(sk2))),
inference(step,[status(thm)],[t47597,t40]) ).
cnf(t47599,plain,
sFlat5 = join(sFlat4,composition(complement(sFlat0),converse(sk2))),
inference(step,[status(thm)],[t47598,t62]) ).
cnf(t81,plain,
join(sFlat4,composition(complement(sFlat0),converse(sk2))) = sFlat5,
inference(orient,[status(thm)],[t47599]) ).
cnf(t47601,plain,
join(sFlat4,composition(complement(sFlat0),sFlat2)) = sFlat5,
inference(step,[status(thm)],[t81,t87]) ).
cnf(t94,plain,
join(sFlat4,composition(complement(sFlat0),sFlat2)) = sFlat5,
inference(rw,[status(thm)],[t47601]) ).
cnf(t47625,plain,
join(sFlat4,composition(sFlat1,sFlat2)) = sFlat5,
inference(step,[status(thm)],[t94,t98]) ).
cnf(t47626,plain,
join(sFlat4,sFlat3) = sFlat5,
inference(step,[status(thm)],[t47625,t110]) ).
cnf(t47627,plain,
join(sFlat3,sFlat4) = sFlat5,
inference(step,[status(thm)],[t47626,t68]) ).
cnf(t468,plain,
join(sFlat3,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t47627]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t25,plain,
complement(X1) = join(composition(X2,complement(composition(converse(X2),X1))),complement(X1)),
inference(cp,[status(thm)],[t24,t23]) ).
cnf(t47669,plain,
complement(X1) = join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))),
inference(step,[status(thm)],[t25,t68]) ).
cnf(t1401,plain,
join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))) = complement(X1),
inference(orient,[status(thm)],[t47669]) ).
cnf(t1454,plain,
complement(X1) = join(complement(X1),composition(sk2,complement(composition(sFlat2,X1)))),
inference(cp,[status(thm)],[t1401,t87]) ).
cnf(t25256,plain,
join(complement(X1),composition(sk2,complement(composition(sFlat2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t1454]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t36,plain,
meet(join(complement(X1),complement(X2)),X3) = complement(join(meet(X1,X2),complement(X3))),
inference(cp,[status(thm)],[t33,t33]) ).
cnf(t1301,plain,
complement(join(meet(X1,X2),complement(X3))) = meet(join(complement(X1),complement(X2)),X3),
inference(orient,[status(thm)],[t36]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t71,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t74,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t33,t71]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t95,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t47605,plain,
zero = complement(top),
inference(step,[status(thm)],[t74,t95]) ).
cnf(t121,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t47605]) ).
cnf(t1315,plain,
meet(join(complement(X1),complement(X2)),top) = complement(join(meet(X1,X2),zero)),
inference(cp,[status(thm)],[t1301,t121]) ).
cnf(t69,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t33,t68]) ).
cnf(t47603,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t69,t33]) ).
cnf(t115,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t47603]) ).
cnf(t47880,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(meet(X1,X2),zero)),
inference(step,[status(thm)],[t1315,t115]) ).
cnf(t47881,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t47880,t68]) ).
cnf(t5764,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t47881]) ).
cnf(t5811,plain,
complement(join(zero,meet(X1,top))) = meet(top,join(complement(X1),zero)),
inference(cp,[status(thm)],[t5764,t121]) ).
cnf(t12,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)],[t12]) ).
cnf(t47594,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t20,t33]) ).
cnf(t39,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t47594]) ).
cnf(t2790,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t39]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t75,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t76,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t75,t71]) ).
cnf(t673,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t76]) ).
cnf(t78,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t75,t71]) ).
cnf(t470,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t78]) ).
cnf(t474,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t470,t68]) ).
cnf(t564,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t474]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t55,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t57,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t55,t23]) ).
cnf(t249,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t57]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t250,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t249,t19]) ).
cnf(t47618,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t250,t23]) ).
cnf(t287,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t47618]) ).
cnf(t288,plain,
one = converse(one),
inference(cp,[status(thm)],[t287,t19]) ).
cnf(t292,plain,
converse(one) = one,
inference(orient,[status(thm)],[t288]) ).
cnf(t1441,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t1401,t292]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t44,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t45,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t44,t19]) ).
cnf(t195,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t45]) ).
cnf(t289,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t287,t195]) ).
cnf(t47620,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t289,t287]) ).
cnf(t300,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t47620]) ).
cnf(t47670,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t1441,t300]) ).
cnf(t47671,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t47670,t300]) ).
cnf(t1458,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t47671]) ).
cnf(t1500,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t564,t1458]) ).
cnf(t47691,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t1500,t71]) ).
cnf(t1556,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t47691]) ).
cnf(t1572,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t673,t1556]) ).
cnf(t1577,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t1572]) ).
cnf(t2819,plain,
X1 = join(meet(X1,top),complement(top)),
inference(cp,[status(thm)],[t2790,t1577]) ).
cnf(t47831,plain,
X1 = join(complement(top),meet(X1,top)),
inference(step,[status(thm)],[t2819,t68]) ).
cnf(t47832,plain,
X1 = join(zero,meet(X1,top)),
inference(step,[status(thm)],[t47831,t121]) ).
cnf(t2882,plain,
join(zero,meet(X1,top)) = X1,
inference(orient,[status(thm)],[t47832]) ).
cnf(t47882,plain,
complement(X1) = meet(top,join(complement(X1),zero)),
inference(step,[status(thm)],[t5811,t2882]) ).
cnf(t47883,plain,
complement(X1) = meet(top,join(zero,complement(X1))),
inference(step,[status(thm)],[t47882,t68]) ).
cnf(t5824,plain,
meet(top,join(zero,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t47883]) ).
cnf(t1499,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t33,t1458]) ).
cnf(t1530,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t1499]) ).
cnf(t5851,plain,
complement(complement(X1)) = meet(top,join(zero,meet(X1,X1))),
inference(cp,[status(thm)],[t5824,t1530]) ).
cnf(t2791,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t2790,t95]) ).
cnf(t47829,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t2791,t33]) ).
cnf(t2857,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t47829]) ).
cnf(t47886,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t5851,t2857]) ).
cnf(t5856,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t47886]) ).
cnf(t2806,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t2790,t1458]) ).
cnf(t47843,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t2806,t68]) ).
cnf(t47844,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t47843,t95]) ).
cnf(t47845,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t47844,t68]) ).
cnf(t2913,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t47845]) ).
cnf(t47888,plain,
join(zero,meet(top,X1)) = X1,
inference(step,[status(thm)],[t2913,t5856]) ).
cnf(t5913,plain,
join(zero,meet(top,X1)) = X1,
inference(rw,[status(thm)],[t47888]) ).
cnf(t6060,plain,
join(zero,meet(top,X1)) = X1,
inference(orient,[status(thm)],[t5913]) ).
cnf(t124,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t33,t121]) ).
cnf(t439,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t124]) ).
cnf(t1544,plain,
meet(top,complement(X1)) = complement(join(zero,meet(X1,X1))),
inference(cp,[status(thm)],[t439,t1530]) ).
cnf(t1643,plain,
complement(join(zero,meet(X1,X1))) = meet(top,complement(X1)),
inference(orient,[status(thm)],[t1544]) ).
cnf(t47830,plain,
complement(X1) = meet(top,complement(X1)),
inference(step,[status(thm)],[t1643,t2857]) ).
cnf(t2860,plain,
complement(X1) = meet(top,complement(X1)),
inference(rw,[status(thm)],[t47830]) ).
cnf(t2861,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t2860]) ).
cnf(t5880,plain,
complement(complement(X1)) = meet(top,meet(top,X1)),
inference(cp,[status(thm)],[t2861,t5856]) ).
cnf(t47916,plain,
meet(top,X1) = meet(top,meet(top,X1)),
inference(step,[status(thm)],[t5880,t5856]) ).
cnf(t6269,plain,
meet(top,meet(top,X1)) = meet(top,X1),
inference(orient,[status(thm)],[t47916]) ).
cnf(t6272,plain,
meet(top,X1) = join(zero,meet(top,X1)),
inference(cp,[status(thm)],[t6060,t6269]) ).
cnf(t47917,plain,
meet(top,X1) = X1,
inference(step,[status(thm)],[t6272,t6060]) ).
cnf(t6274,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t47917]) ).
cnf(t47922,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t5856,t6274]) ).
cnf(t6279,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t47922]) ).
cnf(t2845,plain,
join(zero,complement(X1)) = join(meet(join(zero,complement(X1)),X2),complement(join(meet(top,X1),X2))),
inference(cp,[status(thm)],[t2790,t439]) ).
cnf(t47926,plain,
join(zero,X1) = X1,
inference(step,[status(thm)],[t6060,t6274]) ).
cnf(t6294,plain,
join(zero,X1) = X1,
inference(rw,[status(thm)],[t47926]) ).
cnf(t6430,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t6294]) ).
cnf(t49532,plain,
complement(X1) = join(meet(join(zero,complement(X1)),X2),complement(join(meet(top,X1),X2))),
inference(step,[status(thm)],[t2845,t6430]) ).
cnf(t49533,plain,
complement(X1) = join(meet(complement(X1),X2),complement(join(meet(top,X1),X2))),
inference(step,[status(thm)],[t49532,t6430]) ).
cnf(t49534,plain,
complement(X1) = join(meet(complement(X1),X2),complement(join(X1,X2))),
inference(step,[status(thm)],[t49533,t6274]) ).
cnf(t46930,plain,
join(meet(complement(X1),X2),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t49534]) ).
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(t47615,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(join(complement(X1),X2),complement(join(complement(X1),complement(X2)))))),
inference(step,[status(thm)],[t21,t68]) ).
cnf(t47616,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)],[t47615,t75]) ).
cnf(t47617,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t47616,t33]) ).
cnf(t263,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t47617]) ).
cnf(t285,plain,
join(complement(X1),join(complement(join(complement(X1),join(X2,meet(X1,X2)))),X3)) = join(join(complement(X1),complement(X2)),X3),
inference(cp,[status(thm)],[t75,t263]) ).
cnf(t37,plain,
meet(X1,join(complement(X2),complement(X3))) = complement(join(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t33,t33]) ).
cnf(t1340,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,join(complement(X2),complement(X3))),
inference(orient,[status(thm)],[t37]) ).
cnf(t47887,plain,
meet(X1,X1) = meet(top,X1),
inference(step,[status(thm)],[t1530,t5856]) ).
cnf(t5912,plain,
meet(X1,X1) = meet(top,X1),
inference(rw,[status(thm)],[t47887]) ).
cnf(t5915,plain,
meet(X1,X1) = meet(top,X1),
inference(orient,[status(thm)],[t5912]) ).
cnf(t47924,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t5915,t6274]) ).
cnf(t6292,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t47924]) ).
cnf(t6357,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t6292]) ).
cnf(t6371,plain,
meet(X1,join(complement(X2),complement(X2))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t1340,t6357]) ).
cnf(t48001,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t6371,t1458]) ).
cnf(t7343,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t48001]) ).
cnf(t49131,plain,
join(complement(X1),join(meet(X1,complement(join(X2,meet(X1,X2)))),X3)) = join(join(complement(X1),complement(X2)),X3),
inference(step,[status(thm)],[t285,t7343]) ).
cnf(t49132,plain,
join(complement(X1),join(meet(X1,complement(join(X2,meet(X1,X2)))),X3)) = join(complement(X1),join(complement(X2),X3)),
inference(step,[status(thm)],[t49131,t75]) ).
cnf(t34281,plain,
join(complement(X1),join(meet(X1,complement(join(X2,meet(X1,X2)))),X3)) = join(complement(X1),join(complement(X2),X3)),
inference(orient,[status(thm)],[t49132]) ).
cnf(t2801,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t2790,t33]) ).
cnf(t47846,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t2801,t68]) ).
cnf(t2931,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t47846]) ).
cnf(t6365,plain,
X1 = join(X1,meet(X1,complement(X1))),
inference(cp,[status(thm)],[t2931,t6357]) ).
cnf(t47956,plain,
X1 = join(X1,zero),
inference(step,[status(thm)],[t6365,t95]) ).
cnf(t6463,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t47956]) ).
cnf(t34352,plain,
join(complement(X1),join(complement(X2),zero)) = join(complement(X1),meet(X1,complement(join(X2,meet(X1,X2))))),
inference(cp,[status(thm)],[t34281,t6463]) ).
cnf(t77,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t75,t68]) ).
cnf(t362,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t77]) ).
cnf(t49359,plain,
join(zero,join(complement(X1),complement(X2))) = join(complement(X1),meet(X1,complement(join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t34352,t362]) ).
cnf(t49360,plain,
join(complement(X1),complement(X2)) = join(complement(X1),meet(X1,complement(join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t49359,t6430]) ).
cnf(t47929,plain,
join(complement(X1),complement(X2)) = complement(join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t5764,t6274]) ).
cnf(t6297,plain,
join(complement(X1),complement(X2)) = complement(join(zero,meet(X1,X2))),
inference(rw,[status(thm)],[t47929]) ).
cnf(t48083,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t6297,t6430]) ).
cnf(t7871,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t48083]) ).
cnf(t49361,plain,
complement(meet(X1,X2)) = join(complement(X1),meet(X1,complement(join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t49360,t7871]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t83,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t86,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t75,t83]) ).
cnf(t946,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t86]) ).
cnf(t947,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = join(top,converse(X2)),
inference(cp,[status(thm)],[t946,t564]) ).
cnf(t48658,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = join(top,converse(X2)),
inference(step,[status(thm)],[t947,t68]) ).
cnf(t85,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t83,t23]) ).
cnf(t330,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t85]) ).
cnf(t331,plain,
join(converse(join(X1,X2)),X3) = converse(join(X1,join(X2,converse(X3)))),
inference(cp,[status(thm)],[t330,t75]) ).
cnf(t2097,plain,
converse(join(X1,join(X2,converse(X3)))) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t331]) ).
cnf(t84,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t83,t23]) ).
cnf(t303,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t84]) ).
cnf(t306,plain,
join(one,converse(X1)) = converse(join(one,X1)),
inference(cp,[status(thm)],[t303,t292]) ).
cnf(t322,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t306]) ).
cnf(t323,plain,
join(one,converse(complement(one))) = converse(top),
inference(cp,[status(thm)],[t322,t71]) ).
cnf(t518,plain,
join(one,converse(complement(one))) = converse(top),
inference(orient,[status(thm)],[t323]) ).
cnf(t2100,plain,
join(converse(join(X1,one)),complement(one)) = converse(join(X1,converse(top))),
inference(cp,[status(thm)],[t2097,t518]) ).
cnf(t47760,plain,
join(complement(one),converse(join(X1,one))) = converse(join(X1,converse(top))),
inference(step,[status(thm)],[t2100,t68]) ).
cnf(t334,plain,
join(converse(X1),one) = converse(join(X1,one)),
inference(cp,[status(thm)],[t330,t292]) ).
cnf(t47621,plain,
join(one,converse(X1)) = converse(join(X1,one)),
inference(step,[status(thm)],[t334,t68]) ).
cnf(t352,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t47621]) ).
cnf(t47761,plain,
join(complement(one),join(one,converse(X1))) = converse(join(X1,converse(top))),
inference(step,[status(thm)],[t47760,t352]) ).
cnf(t80,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t75,t68]) ).
cnf(t47622,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t80,t75]) ).
cnf(t372,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t47622]) ).
cnf(t47762,plain,
join(one,join(complement(one),converse(X1))) = converse(join(X1,converse(top))),
inference(step,[status(thm)],[t47761,t372]) ).
cnf(t47763,plain,
join(top,converse(X1)) = converse(join(X1,converse(top))),
inference(step,[status(thm)],[t47762,t470]) ).
cnf(t47764,plain,
join(top,converse(X1)) = join(converse(X1),top),
inference(step,[status(thm)],[t47763,t330]) ).
cnf(t47765,plain,
join(top,converse(X1)) = top,
inference(step,[status(thm)],[t47764,t1577]) ).
cnf(t2147,plain,
join(top,converse(X1)) = top,
inference(orient,[status(thm)],[t47765]) ).
cnf(t48659,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t48658,t2147]) ).
cnf(t22451,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t48659]) ).
cnf(t22557,plain,
meet(converse(X1),complement(converse(join(X1,X2)))) = complement(top),
inference(cp,[status(thm)],[t7343,t22451]) ).
cnf(t48948,plain,
meet(converse(X1),complement(converse(join(X1,X2)))) = zero,
inference(step,[status(thm)],[t22557,t121]) ).
cnf(t29100,plain,
meet(converse(X1),complement(converse(join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t48948]) ).
cnf(t29225,plain,
converse(X1) = join(zero,meet(converse(X1),complement(complement(converse(join(X1,X2)))))),
inference(cp,[status(thm)],[t2931,t29100]) ).
cnf(t48949,plain,
converse(X1) = meet(converse(X1),complement(complement(converse(join(X1,X2))))),
inference(step,[status(thm)],[t29225,t6430]) ).
cnf(t48950,plain,
converse(X1) = meet(converse(X1),converse(join(X1,X2))),
inference(step,[status(thm)],[t48949,t6279]) ).
cnf(t29227,plain,
meet(converse(X1),converse(join(X1,X2))) = converse(X1),
inference(orient,[status(thm)],[t48950]) ).
cnf(t1475,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t1458,t33]) ).
cnf(t47735,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t1475,t33]) ).
cnf(t47736,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t47735,t33]) ).
cnf(t1642,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t47736]) ).
cnf(t6282,plain,
meet(top,X1) = join(X1,meet(top,X1)),
inference(cp,[status(thm)],[t1642,t6274]) ).
cnf(t47937,plain,
X1 = join(X1,meet(top,X1)),
inference(step,[status(thm)],[t6282,t6274]) ).
cnf(t47938,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t47937,t6274]) ).
cnf(t6332,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t47938]) ).
cnf(t6354,plain,
join(converse(join(join(X1,converse(X2)),X1)),X2) = converse(join(X1,converse(X2))),
inference(cp,[status(thm)],[t2097,t6332]) ).
cnf(t48057,plain,
join(converse(join(X1,join(converse(X2),X1))),X2) = converse(join(X1,converse(X2))),
inference(step,[status(thm)],[t6354,t75]) ).
cnf(t366,plain,
join(X1,converse(join(X2,X3))) = converse(join(X3,join(converse(X1),X2))),
inference(cp,[status(thm)],[t303,t362]) ).
cnf(t2328,plain,
converse(join(X1,join(converse(X2),X3))) = join(X2,converse(join(X3,X1))),
inference(orient,[status(thm)],[t366]) ).
cnf(t48058,plain,
join(join(X2,converse(join(X1,X1))),X2) = converse(join(X1,converse(X2))),
inference(step,[status(thm)],[t48057,t2328]) ).
cnf(t48059,plain,
join(X2,join(converse(join(X1,X1)),X2)) = converse(join(X1,converse(X2))),
inference(step,[status(thm)],[t48058,t75]) ).
cnf(t48060,plain,
join(X2,join(converse(X1),X2)) = converse(join(X1,converse(X2))),
inference(step,[status(thm)],[t48059,t6332]) ).
cnf(t48061,plain,
join(X2,join(converse(X1),X2)) = join(converse(X1),X2),
inference(step,[status(thm)],[t48060,t330]) ).
cnf(t7706,plain,
join(X1,join(converse(X2),X1)) = join(converse(X2),X1),
inference(orient,[status(thm)],[t48061]) ).
cnf(t29312,plain,
converse(X1) = meet(converse(X1),converse(join(converse(X2),X1))),
inference(cp,[status(thm)],[t29227,t7706]) ).
cnf(t49206,plain,
converse(X1) = meet(converse(X1),join(X2,converse(X1))),
inference(step,[status(thm)],[t29312,t303]) ).
cnf(t36945,plain,
meet(converse(X1),join(X2,converse(X1))) = converse(X1),
inference(orient,[status(thm)],[t49206]) ).
cnf(t37015,plain,
converse(converse(X1)) = meet(X1,join(X2,converse(converse(X1)))),
inference(cp,[status(thm)],[t36945,t23]) ).
cnf(t49207,plain,
X1 = meet(X1,join(X2,converse(converse(X1)))),
inference(step,[status(thm)],[t37015,t23]) ).
cnf(t49208,plain,
X1 = meet(X1,join(X2,X1)),
inference(step,[status(thm)],[t49207,t23]) ).
cnf(t37100,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t49208]) ).
cnf(t37184,plain,
complement(X1) = meet(complement(X1),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t37100,t7871]) ).
cnf(t7384,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t7343,t6279]) ).
cnf(t15321,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t7384]) ).
cnf(t49212,plain,
complement(X1) = complement(join(X1,meet(X2,X1))),
inference(step,[status(thm)],[t37184,t15321]) ).
cnf(t37288,plain,
complement(join(X1,meet(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t49212]) ).
cnf(t49362,plain,
complement(meet(X1,X2)) = join(complement(X1),meet(X1,complement(X2))),
inference(step,[status(thm)],[t49361,t37288]) ).
cnf(t40764,plain,
join(complement(X1),meet(X1,complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t49362]) ).
cnf(t40800,plain,
complement(meet(complement(X1),X2)) = join(X1,meet(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t40764,t6279]) ).
cnf(t7889,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t7871,t6279]) ).
cnf(t7917,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t7889]) ).
cnf(t49363,plain,
join(X1,complement(X2)) = join(X1,meet(complement(X1),complement(X2))),
inference(step,[status(thm)],[t40800,t7917]) ).
cnf(t49364,plain,
join(X1,complement(X2)) = join(X1,complement(join(X1,X2))),
inference(step,[status(thm)],[t49363,t15321]) ).
cnf(t40872,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t49364]) ).
cnf(t6372,plain,
meet(join(complement(X1),complement(X1)),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t1301,t6357]) ).
cnf(t48005,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(step,[status(thm)],[t6372,t1458]) ).
cnf(t7411,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t48005]) ).
cnf(t40881,plain,
join(X1,complement(complement(X2))) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t40872,t7411]) ).
cnf(t49385,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(step,[status(thm)],[t40881,t6279]) ).
cnf(t41514,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t49385]) ).
cnf(t41531,plain,
join(X1,X2) = join(X1,meet(X2,complement(X1))),
inference(cp,[status(thm)],[t41514,t115]) ).
cnf(t43352,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t41531]) ).
cnf(t43410,plain,
join(complement(X1),X2) = join(complement(X1),meet(X2,X1)),
inference(cp,[status(thm)],[t43352,t6279]) ).
cnf(t44158,plain,
join(complement(X1),meet(X2,X1)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t43410]) ).
cnf(t22,plain,
join(complement(X1),complement(X2)) = join(complement(join(complement(join(complement(X1),complement(X2))),complement(complement(join(complement(X1),X2))))),complement(X1)),
inference(cp,[status(thm)],[t20,t20]) ).
cnf(t47640,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(join(complement(X1),complement(X2))),complement(complement(join(complement(X1),X2)))))),
inference(step,[status(thm)],[t22,t68]) ).
cnf(t47641,plain,
join(complement(X1),complement(X2)) = join(complement(X1),meet(join(complement(X1),complement(X2)),complement(join(complement(X1),X2)))),
inference(step,[status(thm)],[t47640,t33]) ).
cnf(t735,plain,
join(complement(X1),meet(join(complement(X1),complement(X2)),complement(join(complement(X1),X2)))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t47641]) ).
cnf(t41,plain,
meet(sk1,X1) = complement(join(sFlat4,complement(X1))),
inference(cp,[status(thm)],[t33,t40]) ).
cnf(t202,plain,
complement(join(sFlat4,complement(X1))) = meet(sk1,X1),
inference(orient,[status(thm)],[t41]) ).
cnf(t203,plain,
meet(sk1,top) = complement(join(sFlat4,zero)),
inference(cp,[status(thm)],[t202,t121]) ).
cnf(t47612,plain,
meet(top,sk1) = complement(join(sFlat4,zero)),
inference(step,[status(thm)],[t203,t115]) ).
cnf(t212,plain,
complement(join(sFlat4,zero)) = meet(top,sk1),
inference(orient,[status(thm)],[t47612]) ).
cnf(t779,plain,
join(complement(X1),complement(join(sFlat4,zero))) = join(complement(X1),meet(join(complement(X1),meet(top,sk1)),complement(join(complement(X1),join(sFlat4,zero))))),
inference(cp,[status(thm)],[t735,t212]) ).
cnf(t49230,plain,
complement(meet(X1,join(sFlat4,zero))) = join(complement(X1),meet(join(complement(X1),meet(top,sk1)),complement(join(complement(X1),join(sFlat4,zero))))),
inference(step,[status(thm)],[t779,t7871]) ).
cnf(t205,plain,
meet(sk1,sk1) = complement(join(sFlat4,sFlat4)),
inference(cp,[status(thm)],[t202,t40]) ).
cnf(t224,plain,
complement(join(sFlat4,sFlat4)) = meet(sk1,sk1),
inference(orient,[status(thm)],[t205]) ).
cnf(t1474,plain,
complement(sk1) = join(sFlat4,complement(sk1)),
inference(cp,[status(thm)],[t1458,t40]) ).
cnf(t47678,plain,
sFlat4 = join(sFlat4,complement(sk1)),
inference(step,[status(thm)],[t1474,t40]) ).
cnf(t47679,plain,
sFlat4 = join(sFlat4,sFlat4),
inference(step,[status(thm)],[t47678,t40]) ).
cnf(t1513,plain,
join(sFlat4,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t47679]) ).
cnf(t47680,plain,
complement(sFlat4) = meet(sk1,sk1),
inference(step,[status(thm)],[t224,t1513]) ).
cnf(t1515,plain,
complement(sFlat4) = meet(sk1,sk1),
inference(rw,[status(thm)],[t47680]) ).
cnf(t1528,plain,
meet(sk1,sk1) = complement(sFlat4),
inference(orient,[status(thm)],[t1515]) ).
cnf(t1529,plain,
join(complement(sk1),complement(sk1)) = join(complement(sk1),complement(join(complement(sk1),join(sk1,complement(sFlat4))))),
inference(cp,[status(thm)],[t263,t1528]) ).
cnf(t47715,plain,
complement(sk1) = join(complement(sk1),complement(join(complement(sk1),join(sk1,complement(sFlat4))))),
inference(step,[status(thm)],[t1529,t1458]) ).
cnf(t47716,plain,
sFlat4 = join(complement(sk1),complement(join(complement(sk1),join(sk1,complement(sFlat4))))),
inference(step,[status(thm)],[t47715,t40]) ).
cnf(t47717,plain,
sFlat4 = join(sFlat4,complement(join(complement(sk1),join(sk1,complement(sFlat4))))),
inference(step,[status(thm)],[t47716,t40]) ).
cnf(t47718,plain,
sFlat4 = join(sFlat4,complement(join(sk1,join(complement(sk1),complement(sFlat4))))),
inference(step,[status(thm)],[t47717,t372]) ).
cnf(t47719,plain,
sFlat4 = join(sFlat4,complement(join(top,complement(sFlat4)))),
inference(step,[status(thm)],[t47718,t470]) ).
cnf(t47720,plain,
sFlat4 = join(sFlat4,complement(top)),
inference(step,[status(thm)],[t47719,t1556]) ).
cnf(t47721,plain,
sFlat4 = join(sFlat4,zero),
inference(step,[status(thm)],[t47720,t121]) ).
cnf(t1631,plain,
join(sFlat4,zero) = sFlat4,
inference(orient,[status(thm)],[t47721]) ).
cnf(t49231,plain,
complement(meet(X1,sFlat4)) = join(complement(X1),meet(join(complement(X1),meet(top,sk1)),complement(join(complement(X1),join(sFlat4,zero))))),
inference(step,[status(thm)],[t49230,t1631]) ).
cnf(t47731,plain,
complement(sFlat4) = meet(top,sk1),
inference(step,[status(thm)],[t212,t1631]) ).
cnf(t1637,plain,
complement(sFlat4) = meet(top,sk1),
inference(rw,[status(thm)],[t47731]) ).
cnf(t1638,plain,
meet(top,sk1) = complement(sFlat4),
inference(orient,[status(thm)],[t1637]) ).
cnf(t47925,plain,
sk1 = complement(sFlat4),
inference(step,[status(thm)],[t1638,t6274]) ).
cnf(t6293,plain,
sk1 = complement(sFlat4),
inference(rw,[status(thm)],[t47925]) ).
cnf(t6301,plain,
complement(sFlat4) = sk1,
inference(orient,[status(thm)],[t6293]) ).
cnf(t6304,plain,
meet(sFlat4,X1) = complement(join(sk1,complement(X1))),
inference(cp,[status(thm)],[t33,t6301]) ).
cnf(t7058,plain,
complement(join(sk1,complement(X1))) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t6304]) ).
cnf(t7072,plain,
join(sk1,complement(X1)) = complement(meet(sFlat4,X1)),
inference(cp,[status(thm)],[t6279,t7058]) ).
cnf(t7181,plain,
complement(meet(sFlat4,X1)) = join(sk1,complement(X1)),
inference(orient,[status(thm)],[t7072]) ).
cnf(t7182,plain,
join(sk1,complement(X1)) = complement(meet(X1,sFlat4)),
inference(cp,[status(thm)],[t7181,t115]) ).
cnf(t7494,plain,
complement(meet(X1,sFlat4)) = join(sk1,complement(X1)),
inference(orient,[status(thm)],[t7182]) ).
cnf(t49232,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(join(complement(X1),meet(top,sk1)),complement(join(complement(X1),join(sFlat4,zero))))),
inference(step,[status(thm)],[t49231,t7494]) ).
cnf(t49233,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(join(complement(X1),sk1),complement(join(complement(X1),join(sFlat4,zero))))),
inference(step,[status(thm)],[t49232,t6274]) ).
cnf(t49234,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(join(sk1,complement(X1)),complement(join(complement(X1),join(sFlat4,zero))))),
inference(step,[status(thm)],[t49233,t68]) ).
cnf(t49235,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(join(sk1,complement(X1)),meet(X1,complement(join(sFlat4,zero))))),
inference(step,[status(thm)],[t49234,t7343]) ).
cnf(t1546,plain,
meet(sk1,complement(X1)) = complement(join(sFlat4,meet(X1,X1))),
inference(cp,[status(thm)],[t202,t1530]) ).
cnf(t1682,plain,
complement(join(sFlat4,meet(X1,X1))) = meet(sk1,complement(X1)),
inference(orient,[status(thm)],[t1546]) ).
cnf(t47946,plain,
complement(join(sFlat4,X1)) = meet(sk1,complement(X1)),
inference(step,[status(thm)],[t1682,t6357]) ).
cnf(t6383,plain,
complement(join(sFlat4,X1)) = meet(sk1,complement(X1)),
inference(rw,[status(thm)],[t47946]) ).
cnf(t6590,plain,
complement(join(sFlat4,X1)) = meet(sk1,complement(X1)),
inference(orient,[status(thm)],[t6383]) ).
cnf(t49236,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(join(sk1,complement(X1)),meet(X1,meet(sk1,complement(zero))))),
inference(step,[status(thm)],[t49235,t6590]) ).
cnf(t1535,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t71,t1530]) ).
cnf(t1623,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t1535]) ).
cnf(t2808,plain,
X1 = join(meet(X1,meet(X1,X1)),complement(top)),
inference(cp,[status(thm)],[t2790,t1623]) ).
cnf(t47839,plain,
X1 = join(complement(top),meet(X1,meet(X1,X1))),
inference(step,[status(thm)],[t2808,t68]) ).
cnf(t47840,plain,
X1 = join(zero,meet(X1,meet(X1,X1))),
inference(step,[status(thm)],[t47839,t121]) ).
cnf(t2887,plain,
join(zero,meet(X1,meet(X1,X1))) = X1,
inference(orient,[status(thm)],[t47840]) ).
cnf(t6061,plain,
meet(top,top) = top,
inference(cp,[status(thm)],[t6060,t2887]) ).
cnf(t445,plain,
meet(top,top) = complement(join(zero,zero)),
inference(cp,[status(thm)],[t439,t121]) ).
cnf(t458,plain,
complement(join(zero,zero)) = meet(top,top),
inference(orient,[status(thm)],[t445]) ).
cnf(t1472,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t1458,t121]) ).
cnf(t47672,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t1472,t121]) ).
cnf(t47673,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t47672,t121]) ).
cnf(t1505,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t47673]) ).
cnf(t47674,plain,
complement(zero) = meet(top,top),
inference(step,[status(thm)],[t458,t1505]) ).
cnf(t1506,plain,
complement(zero) = meet(top,top),
inference(rw,[status(thm)],[t47674]) ).
cnf(t1524,plain,
meet(top,top) = complement(zero),
inference(orient,[status(thm)],[t1506]) ).
cnf(t47896,plain,
complement(zero) = top,
inference(step,[status(thm)],[t6061,t1524]) ).
cnf(t6228,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t47896]) ).
cnf(t49237,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(join(sk1,complement(X1)),meet(X1,meet(sk1,top)))),
inference(step,[status(thm)],[t49236,t6228]) ).
cnf(t6281,plain,
X1 = meet(X1,top),
inference(cp,[status(thm)],[t6274,t115]) ).
cnf(t6412,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t6281]) ).
cnf(t49238,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(join(sk1,complement(X1)),meet(X1,sk1))),
inference(step,[status(thm)],[t49237,t6412]) ).
cnf(t49239,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(meet(X1,sk1),join(sk1,complement(X1)))),
inference(step,[status(thm)],[t49238,t115]) ).
cnf(t5786,plain,
complement(join(zero,meet(sk1,X1))) = meet(top,join(sFlat4,complement(X1))),
inference(cp,[status(thm)],[t5764,t40]) ).
cnf(t48076,plain,
complement(meet(sk1,X1)) = meet(top,join(sFlat4,complement(X1))),
inference(step,[status(thm)],[t5786,t6430]) ).
cnf(t48077,plain,
complement(meet(sk1,X1)) = join(sFlat4,complement(X1)),
inference(step,[status(thm)],[t48076,t6274]) ).
cnf(t7805,plain,
complement(meet(sk1,X1)) = join(sFlat4,complement(X1)),
inference(orient,[status(thm)],[t48077]) ).
cnf(t7809,plain,
meet(meet(sk1,X1),complement(X2)) = complement(join(join(sFlat4,complement(X1)),X2)),
inference(cp,[status(thm)],[t7343,t7805]) ).
cnf(t48730,plain,
meet(meet(sk1,X1),complement(X2)) = complement(join(sFlat4,join(complement(X1),X2))),
inference(step,[status(thm)],[t7809,t75]) ).
cnf(t48731,plain,
meet(meet(sk1,X1),complement(X2)) = meet(sk1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t48730,t6590]) ).
cnf(t48732,plain,
meet(meet(sk1,X1),complement(X2)) = meet(sk1,meet(X1,complement(X2))),
inference(step,[status(thm)],[t48731,t7343]) ).
cnf(t24221,plain,
meet(meet(sk1,X1),complement(X2)) = meet(sk1,meet(X1,complement(X2))),
inference(orient,[status(thm)],[t48732]) ).
cnf(t24292,plain,
meet(sk1,meet(X1,complement(complement(X2)))) = meet(meet(sk1,X1),X2),
inference(cp,[status(thm)],[t24221,t6279]) ).
cnf(t48733,plain,
meet(sk1,meet(X1,X2)) = meet(meet(sk1,X1),X2),
inference(step,[status(thm)],[t24292,t6279]) ).
cnf(t24305,plain,
meet(meet(sk1,X1),X2) = meet(sk1,meet(X1,X2)),
inference(orient,[status(thm)],[t48733]) ).
cnf(t24355,plain,
meet(sk1,meet(X1,X2)) = meet(meet(X1,sk1),X2),
inference(cp,[status(thm)],[t24305,t115]) ).
cnf(t24469,plain,
meet(meet(X1,sk1),X2) = meet(sk1,meet(X1,X2)),
inference(orient,[status(thm)],[t24355]) ).
cnf(t49240,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(sk1,meet(X1,join(sk1,complement(X1))))),
inference(step,[status(thm)],[t49239,t24469]) ).
cnf(t6334,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t6332,t372]) ).
cnf(t47981,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t6334,t75]) ).
cnf(t47982,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t47981,t6332]) ).
cnf(t6818,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t47982]) ).
cnf(t2851,plain,
sk1 = join(meet(sk1,X1),complement(join(sFlat4,X1))),
inference(cp,[status(thm)],[t2790,t40]) ).
cnf(t3078,plain,
join(meet(sk1,X1),complement(join(sFlat4,X1))) = sk1,
inference(orient,[status(thm)],[t2851]) ).
cnf(t3079,plain,
sk1 = join(meet(X1,sk1),complement(join(sFlat4,X1))),
inference(cp,[status(thm)],[t3078,t115]) ).
cnf(t48265,plain,
sk1 = join(meet(X1,sk1),meet(sk1,complement(X1))),
inference(step,[status(thm)],[t3079,t6590]) ).
cnf(t11954,plain,
join(meet(X1,sk1),meet(sk1,complement(X1))) = sk1,
inference(orient,[status(thm)],[t48265]) ).
cnf(t11983,plain,
join(meet(X1,sk1),meet(sk1,complement(X1))) = join(meet(X1,sk1),sk1),
inference(cp,[status(thm)],[t6818,t11954]) ).
cnf(t48266,plain,
sk1 = join(meet(X1,sk1),sk1),
inference(step,[status(thm)],[t11983,t11954]) ).
cnf(t48267,plain,
sk1 = join(sk1,meet(X1,sk1)),
inference(step,[status(thm)],[t48266,t68]) ).
cnf(t11985,plain,
join(sk1,meet(X1,sk1)) = sk1,
inference(orient,[status(thm)],[t48267]) ).
cnf(t34394,plain,
join(complement(X1),join(complement(sk1),X2)) = join(complement(X1),join(meet(X1,complement(sk1)),X2)),
inference(cp,[status(thm)],[t34281,t11985]) ).
cnf(t49139,plain,
join(complement(X1),join(sFlat4,X2)) = join(complement(X1),join(meet(X1,complement(sk1)),X2)),
inference(step,[status(thm)],[t34394,t40]) ).
cnf(t49140,plain,
join(sFlat4,join(complement(X1),X2)) = join(complement(X1),join(meet(X1,complement(sk1)),X2)),
inference(step,[status(thm)],[t49139,t372]) ).
cnf(t49141,plain,
join(sFlat4,join(complement(X1),X2)) = join(complement(X1),join(meet(X1,sFlat4),X2)),
inference(step,[status(thm)],[t49140,t40]) ).
cnf(t34694,plain,
join(complement(X1),join(meet(X1,sFlat4),X2)) = join(sFlat4,join(complement(X1),X2)),
inference(orient,[status(thm)],[t49141]) ).
cnf(t34752,plain,
join(sFlat4,join(complement(X1),zero)) = join(complement(X1),meet(X1,sFlat4)),
inference(cp,[status(thm)],[t34694,t6463]) ).
cnf(t49142,plain,
join(sFlat4,complement(X1)) = join(complement(X1),meet(X1,sFlat4)),
inference(step,[status(thm)],[t34752,t6463]) ).
cnf(t34809,plain,
join(complement(X1),meet(X1,sFlat4)) = join(sFlat4,complement(X1)),
inference(orient,[status(thm)],[t49142]) ).
cnf(t34840,plain,
meet(X1,complement(meet(X1,sFlat4))) = complement(join(sFlat4,complement(X1))),
inference(cp,[status(thm)],[t7343,t34809]) ).
cnf(t49150,plain,
meet(X1,join(sk1,complement(X1))) = complement(join(sFlat4,complement(X1))),
inference(step,[status(thm)],[t34840,t7494]) ).
cnf(t49151,plain,
meet(X1,join(sk1,complement(X1))) = meet(sk1,X1),
inference(step,[status(thm)],[t49150,t202]) ).
cnf(t34862,plain,
meet(X1,join(sk1,complement(X1))) = meet(sk1,X1),
inference(orient,[status(thm)],[t49151]) ).
cnf(t49241,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(sk1,meet(sk1,X1))),
inference(step,[status(thm)],[t49240,t34862]) ).
cnf(t7910,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t6818,t7871]) ).
cnf(t48104,plain,
complement(meet(X1,X2)) = join(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t7910,t7871]) ).
cnf(t48105,plain,
complement(meet(X1,X2)) = complement(meet(X1,meet(X1,X2))),
inference(step,[status(thm)],[t48104,t7871]) ).
cnf(t8286,plain,
complement(meet(X1,meet(X1,X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t48105]) ).
cnf(t8296,plain,
meet(X1,meet(X1,X2)) = complement(complement(meet(X1,X2))),
inference(cp,[status(thm)],[t6279,t8286]) ).
cnf(t48112,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t8296,t6279]) ).
cnf(t8318,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t48112]) ).
cnf(t49242,plain,
join(sk1,complement(X1)) = join(complement(X1),meet(sk1,X1)),
inference(step,[status(thm)],[t49241,t8318]) ).
cnf(t37647,plain,
join(complement(X1),meet(sk1,X1)) = join(sk1,complement(X1)),
inference(orient,[status(thm)],[t49242]) ).
cnf(t304,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t303,t71]) ).
cnf(t538,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t304]) ).
cnf(t1592,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t303,t1577]) ).
cnf(t1599,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t1592]) ).
cnf(t2149,plain,
top = converse(top),
inference(cp,[status(thm)],[t2147,t1599]) ).
cnf(t2171,plain,
converse(top) = top,
inference(orient,[status(thm)],[t2149]) ).
cnf(t47773,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t538,t2171]) ).
cnf(t2178,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t47773]) ).
cnf(t6600,plain,
meet(sk1,complement(converse(complement(converse(sFlat4))))) = complement(top),
inference(cp,[status(thm)],[t6590,t2178]) ).
cnf(t48148,plain,
meet(sk1,complement(converse(complement(converse(sFlat4))))) = zero,
inference(step,[status(thm)],[t6600,t121]) ).
cnf(t10025,plain,
meet(sk1,complement(converse(complement(converse(sFlat4))))) = zero,
inference(orient,[status(thm)],[t48148]) ).
cnf(t37680,plain,
join(sk1,complement(complement(converse(complement(converse(sFlat4)))))) = join(complement(complement(converse(complement(converse(sFlat4))))),zero),
inference(cp,[status(thm)],[t37647,t10025]) ).
cnf(t49388,plain,
join(sk1,converse(complement(converse(sFlat4)))) = join(complement(complement(converse(complement(converse(sFlat4))))),zero),
inference(step,[status(thm)],[t37680,t6279]) ).
cnf(t49389,plain,
join(sk1,converse(complement(converse(sFlat4)))) = complement(complement(converse(complement(converse(sFlat4))))),
inference(step,[status(thm)],[t49388,t6463]) ).
cnf(t49390,plain,
join(sk1,converse(complement(converse(sFlat4)))) = converse(complement(converse(sFlat4))),
inference(step,[status(thm)],[t49389,t6279]) ).
cnf(t41791,plain,
join(sk1,converse(complement(converse(sFlat4)))) = converse(complement(converse(sFlat4))),
inference(orient,[status(thm)],[t49390]) ).
cnf(t41799,plain,
top = join(complement(converse(sk1)),converse(converse(complement(converse(sFlat4))))),
inference(cp,[status(thm)],[t22451,t41791]) ).
cnf(t49391,plain,
top = join(complement(converse(sk1)),complement(converse(sFlat4))),
inference(step,[status(thm)],[t41799,t23]) ).
cnf(t49392,plain,
top = complement(meet(converse(sk1),converse(sFlat4))),
inference(step,[status(thm)],[t49391,t7871]) ).
cnf(t49393,plain,
top = complement(meet(converse(sFlat4),converse(sk1))),
inference(step,[status(thm)],[t49392,t115]) ).
cnf(t41808,plain,
complement(meet(converse(sFlat4),converse(sk1))) = top,
inference(orient,[status(thm)],[t49393]) ).
cnf(t41820,plain,
meet(converse(sFlat4),converse(sk1)) = complement(top),
inference(cp,[status(thm)],[t6279,t41808]) ).
cnf(t49394,plain,
meet(converse(sFlat4),converse(sk1)) = zero,
inference(step,[status(thm)],[t41820,t121]) ).
cnf(t41851,plain,
meet(converse(sFlat4),converse(sk1)) = zero,
inference(orient,[status(thm)],[t49394]) ).
cnf(t44230,plain,
join(complement(converse(sk1)),converse(sFlat4)) = join(complement(converse(sk1)),zero),
inference(cp,[status(thm)],[t44158,t41851]) ).
cnf(t49519,plain,
join(converse(sFlat4),complement(converse(sk1))) = join(complement(converse(sk1)),zero),
inference(step,[status(thm)],[t44230,t68]) ).
cnf(t49520,plain,
join(converse(sFlat4),complement(converse(sk1))) = complement(converse(sk1)),
inference(step,[status(thm)],[t49519,t6463]) ).
cnf(t46384,plain,
join(converse(sFlat4),complement(converse(sk1))) = complement(converse(sk1)),
inference(orient,[status(thm)],[t49520]) ).
cnf(t47040,plain,
complement(converse(sFlat4)) = join(meet(complement(converse(sFlat4)),complement(converse(sk1))),complement(complement(converse(sk1)))),
inference(cp,[status(thm)],[t46930,t46384]) ).
cnf(t49549,plain,
complement(converse(sFlat4)) = join(complement(join(converse(sFlat4),converse(sk1))),complement(complement(converse(sk1)))),
inference(step,[status(thm)],[t47040,t15321]) ).
cnf(t49550,plain,
complement(converse(sFlat4)) = complement(meet(join(converse(sFlat4),converse(sk1)),complement(converse(sk1)))),
inference(step,[status(thm)],[t49549,t7871]) ).
cnf(t7908,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t7871,t6279]) ).
cnf(t7950,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t7908]) ).
cnf(t49551,plain,
complement(converse(sFlat4)) = join(complement(join(converse(sFlat4),converse(sk1))),converse(sk1)),
inference(step,[status(thm)],[t49550,t7950]) ).
cnf(t49552,plain,
complement(converse(sFlat4)) = join(complement(converse(join(sFlat4,sk1))),converse(sk1)),
inference(step,[status(thm)],[t49551,t83]) ).
cnf(t72,plain,
top = join(sk1,sFlat4),
inference(cp,[status(thm)],[t71,t40]) ).
cnf(t47602,plain,
top = join(sFlat4,sk1),
inference(step,[status(thm)],[t72,t68]) ).
cnf(t108,plain,
join(sFlat4,sk1) = top,
inference(orient,[status(thm)],[t47602]) ).
cnf(t49553,plain,
complement(converse(sFlat4)) = join(complement(converse(top)),converse(sk1)),
inference(step,[status(thm)],[t49552,t108]) ).
cnf(t49554,plain,
complement(converse(sFlat4)) = join(complement(top),converse(sk1)),
inference(step,[status(thm)],[t49553,t2171]) ).
cnf(t49555,plain,
complement(converse(sFlat4)) = join(zero,converse(sk1)),
inference(step,[status(thm)],[t49554,t121]) ).
cnf(t49556,plain,
complement(converse(sFlat4)) = converse(sk1),
inference(step,[status(thm)],[t49555,t6430]) ).
cnf(t47212,plain,
complement(converse(sFlat4)) = converse(sk1),
inference(orient,[status(thm)],[t49556]) ).
cnf(t47223,plain,
converse(sFlat4) = complement(converse(sk1)),
inference(cp,[status(thm)],[t6279,t47212]) ).
cnf(t47278,plain,
complement(converse(sk1)) = converse(sFlat4),
inference(orient,[status(thm)],[t47223]) ).
cnf(t47332,plain,
complement(converse(sk1)) = join(converse(sFlat4),composition(sk2,complement(composition(sFlat2,converse(sk1))))),
inference(cp,[status(thm)],[t25256,t47278]) ).
cnf(t49566,plain,
converse(sFlat4) = join(converse(sFlat4),composition(sk2,complement(composition(sFlat2,converse(sk1))))),
inference(step,[status(thm)],[t47332,t47278]) ).
cnf(t91,plain,
converse(composition(X1,sk2)) = composition(sFlat2,converse(X1)),
inference(cp,[status(thm)],[t55,t87]) ).
cnf(t143,plain,
converse(composition(X1,sk2)) = composition(sFlat2,converse(X1)),
inference(orient,[status(thm)],[t91]) ).
cnf(t144,plain,
composition(sFlat2,converse(sk1)) = converse(sFlat0),
inference(cp,[status(thm)],[t143,t62]) ).
cnf(t162,plain,
composition(sFlat2,converse(sk1)) = converse(sFlat0),
inference(orient,[status(thm)],[t144]) ).
cnf(t49567,plain,
converse(sFlat4) = join(converse(sFlat4),composition(sk2,complement(converse(sFlat0)))),
inference(step,[status(thm)],[t49566,t162]) ).
cnf(t29,plain,
X1 = join(complement(join(complement(X1),sFlat1)),complement(join(complement(X1),composition(sk1,sk2)))),
inference(cp,[status(thm)],[t20,t27]) ).
cnf(t47818,plain,
X1 = join(complement(join(sFlat1,complement(X1))),complement(join(complement(X1),composition(sk1,sk2)))),
inference(step,[status(thm)],[t29,t68]) ).
cnf(t34,plain,
meet(composition(sk1,sk2),X1) = complement(join(sFlat1,complement(X1))),
inference(cp,[status(thm)],[t33,t27]) ).
cnf(t47623,plain,
meet(sFlat0,X1) = complement(join(sFlat1,complement(X1))),
inference(step,[status(thm)],[t34,t62]) ).
cnf(t379,plain,
complement(join(sFlat1,complement(X1))) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t47623]) ).
cnf(t47819,plain,
X1 = join(meet(sFlat0,X1),complement(join(complement(X1),composition(sk1,sk2)))),
inference(step,[status(thm)],[t47818,t379]) ).
cnf(t47820,plain,
X1 = join(meet(sFlat0,X1),complement(join(complement(X1),sFlat0))),
inference(step,[status(thm)],[t47819,t62]) ).
cnf(t47821,plain,
X1 = join(meet(sFlat0,X1),complement(join(sFlat0,complement(X1)))),
inference(step,[status(thm)],[t47820,t68]) ).
cnf(t2720,plain,
join(meet(sFlat0,X1),complement(join(sFlat0,complement(X1)))) = X1,
inference(orient,[status(thm)],[t47821]) ).
cnf(t6823,plain,
join(meet(sFlat0,X1),complement(join(sFlat0,complement(X1)))) = join(meet(sFlat0,X1),X1),
inference(cp,[status(thm)],[t6818,t2720]) ).
cnf(t47989,plain,
X1 = join(meet(sFlat0,X1),X1),
inference(step,[status(thm)],[t6823,t2720]) ).
cnf(t47990,plain,
X1 = join(X1,meet(sFlat0,X1)),
inference(step,[status(thm)],[t47989,t68]) ).
cnf(t7030,plain,
join(X1,meet(sFlat0,X1)) = X1,
inference(orient,[status(thm)],[t47990]) ).
cnf(t7051,plain,
join(X1,converse(meet(sFlat0,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t303,t7030]) ).
cnf(t48563,plain,
join(X1,converse(meet(sFlat0,converse(X1)))) = X1,
inference(step,[status(thm)],[t7051,t23]) ).
cnf(t20303,plain,
join(X1,converse(meet(sFlat0,converse(X1)))) = X1,
inference(orient,[status(thm)],[t48563]) ).
cnf(t1545,plain,
meet(sFlat0,complement(X1)) = complement(join(sFlat1,meet(X1,X1))),
inference(cp,[status(thm)],[t379,t1530]) ).
cnf(t1663,plain,
complement(join(sFlat1,meet(X1,X1))) = meet(sFlat0,complement(X1)),
inference(orient,[status(thm)],[t1545]) ).
cnf(t47947,plain,
complement(join(sFlat1,X1)) = meet(sFlat0,complement(X1)),
inference(step,[status(thm)],[t1663,t6357]) ).
cnf(t6384,plain,
complement(join(sFlat1,X1)) = meet(sFlat0,complement(X1)),
inference(rw,[status(thm)],[t47947]) ).
cnf(t6641,plain,
complement(join(sFlat1,X1)) = meet(sFlat0,complement(X1)),
inference(orient,[status(thm)],[t6384]) ).
cnf(t6650,plain,
meet(sFlat0,complement(converse(complement(converse(sFlat1))))) = complement(top),
inference(cp,[status(thm)],[t6641,t2178]) ).
cnf(t48151,plain,
meet(sFlat0,complement(converse(complement(converse(sFlat1))))) = zero,
inference(step,[status(thm)],[t6650,t121]) ).
cnf(t10032,plain,
meet(sFlat0,complement(converse(complement(converse(sFlat1))))) = zero,
inference(orient,[status(thm)],[t48151]) ).
cnf(t10035,plain,
sFlat0 = join(zero,meet(sFlat0,complement(complement(converse(complement(converse(sFlat1))))))),
inference(cp,[status(thm)],[t2931,t10032]) ).
cnf(t48152,plain,
sFlat0 = meet(sFlat0,complement(complement(converse(complement(converse(sFlat1)))))),
inference(step,[status(thm)],[t10035,t6430]) ).
cnf(t48153,plain,
sFlat0 = meet(sFlat0,converse(complement(converse(sFlat1)))),
inference(step,[status(thm)],[t48152,t6279]) ).
cnf(t10037,plain,
meet(sFlat0,converse(complement(converse(sFlat1)))) = sFlat0,
inference(orient,[status(thm)],[t48153]) ).
cnf(t20305,plain,
complement(converse(sFlat1)) = join(complement(converse(sFlat1)),converse(sFlat0)),
inference(cp,[status(thm)],[t20303,t10037]) ).
cnf(t48881,plain,
complement(converse(sFlat1)) = join(converse(sFlat0),complement(converse(sFlat1))),
inference(step,[status(thm)],[t20305,t68]) ).
cnf(t26984,plain,
join(converse(sFlat0),complement(converse(sFlat1))) = complement(converse(sFlat1)),
inference(orient,[status(thm)],[t48881]) ).
cnf(t47078,plain,
complement(converse(sFlat0)) = join(meet(complement(converse(sFlat0)),complement(converse(sFlat1))),complement(complement(converse(sFlat1)))),
inference(cp,[status(thm)],[t46930,t26984]) ).
cnf(t49535,plain,
complement(converse(sFlat0)) = join(complement(join(converse(sFlat0),converse(sFlat1))),complement(complement(converse(sFlat1)))),
inference(step,[status(thm)],[t47078,t15321]) ).
cnf(t49536,plain,
complement(converse(sFlat0)) = complement(meet(join(converse(sFlat0),converse(sFlat1)),complement(converse(sFlat1)))),
inference(step,[status(thm)],[t49535,t7871]) ).
cnf(t49537,plain,
complement(converse(sFlat0)) = join(complement(join(converse(sFlat0),converse(sFlat1))),converse(sFlat1)),
inference(step,[status(thm)],[t49536,t7950]) ).
cnf(t49538,plain,
complement(converse(sFlat0)) = join(complement(converse(join(sFlat0,sFlat1))),converse(sFlat1)),
inference(step,[status(thm)],[t49537,t83]) ).
cnf(t100,plain,
top = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t71,t98]) ).
cnf(t118,plain,
join(sFlat0,sFlat1) = top,
inference(orient,[status(thm)],[t100]) ).
cnf(t49539,plain,
complement(converse(sFlat0)) = join(complement(converse(top)),converse(sFlat1)),
inference(step,[status(thm)],[t49538,t118]) ).
cnf(t49540,plain,
complement(converse(sFlat0)) = join(complement(top),converse(sFlat1)),
inference(step,[status(thm)],[t49539,t2171]) ).
cnf(t49541,plain,
complement(converse(sFlat0)) = join(zero,converse(sFlat1)),
inference(step,[status(thm)],[t49540,t121]) ).
cnf(t49542,plain,
complement(converse(sFlat0)) = converse(sFlat1),
inference(step,[status(thm)],[t49541,t6430]) ).
cnf(t47147,plain,
complement(converse(sFlat0)) = converse(sFlat1),
inference(orient,[status(thm)],[t49542]) ).
cnf(t49568,plain,
converse(sFlat4) = join(converse(sFlat4),composition(sk2,converse(sFlat1))),
inference(step,[status(thm)],[t49567,t47147]) ).
cnf(t88,plain,
sk2 = converse(sFlat2),
inference(cp,[status(thm)],[t23,t87]) ).
cnf(t103,plain,
converse(sFlat2) = sk2,
inference(orient,[status(thm)],[t88]) ).
cnf(t106,plain,
converse(composition(X1,sFlat2)) = composition(sk2,converse(X1)),
inference(cp,[status(thm)],[t55,t103]) ).
cnf(t178,plain,
converse(composition(X1,sFlat2)) = composition(sk2,converse(X1)),
inference(orient,[status(thm)],[t106]) ).
cnf(t179,plain,
composition(sk2,converse(sFlat1)) = converse(sFlat3),
inference(cp,[status(thm)],[t178,t110]) ).
cnf(t198,plain,
composition(sk2,converse(sFlat1)) = converse(sFlat3),
inference(orient,[status(thm)],[t179]) ).
cnf(t49569,plain,
converse(sFlat4) = join(converse(sFlat4),converse(sFlat3)),
inference(step,[status(thm)],[t49568,t198]) ).
cnf(t49570,plain,
converse(sFlat4) = converse(join(sFlat4,sFlat3)),
inference(step,[status(thm)],[t49569,t83]) ).
cnf(t49571,plain,
converse(sFlat4) = converse(join(sFlat3,sFlat4)),
inference(step,[status(thm)],[t49570,t68]) ).
cnf(t49572,plain,
converse(sFlat4) = converse(sFlat5),
inference(step,[status(thm)],[t49571,t468]) ).
cnf(t47402,plain,
converse(sFlat5) = converse(sFlat4),
inference(orient,[status(thm)],[t49572]) ).
cnf(t47403,plain,
sFlat5 = converse(converse(sFlat4)),
inference(cp,[status(thm)],[t23,t47402]) ).
cnf(t49577,plain,
sFlat5 = sFlat4,
inference(step,[status(thm)],[t47403,t23]) ).
cnf(t47543,plain,
sFlat5 = sFlat4,
inference(orient,[status(thm)],[t49577]) ).
cnf(t49578,plain,
join(sFlat3,sFlat4) = sFlat4,
inference(step,[status(thm)],[t468,t47543]) ).
cnf(t47544,plain,
join(sFlat3,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t49578]) ).
cnf(goal_0,negated_conjecture,
join(composition(complement(composition(sk1,sk2)),converse(sk2)),complement(sk1)) != complement(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(complement(sk1),composition(complement(composition(sk1,sk2)),converse(sk2))) != complement(sk1),
inference(rw,[status(thm)],[goal_0,t68]) ).
cnf(g0_1,plain,
join(sFlat4,composition(complement(composition(sk1,sk2)),converse(sk2))) != complement(sk1),
inference(rw,[status(thm)],[g0_0,t40]) ).
cnf(g0_2,plain,
join(sFlat4,composition(complement(sFlat0),converse(sk2))) != complement(sk1),
inference(rw,[status(thm)],[g0_1,t62]) ).
cnf(g0_3,plain,
join(sFlat4,composition(sFlat1,converse(sk2))) != complement(sk1),
inference(rw,[status(thm)],[g0_2,t98]) ).
cnf(g0_4,plain,
join(sFlat4,composition(sFlat1,sFlat2)) != complement(sk1),
inference(rw,[status(thm)],[g0_3,t87]) ).
cnf(g0_5,plain,
join(sFlat4,sFlat3) != complement(sk1),
inference(rw,[status(thm)],[g0_4,t110]) ).
cnf(g0_6,plain,
join(sFlat3,sFlat4) != complement(sk1),
inference(rw,[status(thm)],[g0_5,t68]) ).
cnf(g0_7,plain,
sFlat4 != complement(sk1),
inference(rw,[status(thm)],[g0_6,t47544]) ).
cnf(g0_8,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_7,t40]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL012-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.39 % Computer : n017.cluster.edu
% 0.09/0.39 % Model : x86_64 x86_64
% 0.09/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.39 % Memory : 8046.5625MB
% 0.09/0.39 % OS : Linux 6.8.0-71-generic
% 0.09/0.39 % CPULimit : 300
% 0.09/0.39 % WCLimit : 300
% 0.09/0.39 % DateTime : Thu Sep 24 07:06:16 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 110.76/14.97 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 110.76/14.97 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------