%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL033-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 : n020.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:54 PM UTC 2026
% Result : Unsatisfiable 244.11s 41.58s
% Output : CNFRefutation 244.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 103
% Number of leaves : 19
% Syntax : Number of clauses : 532 ( 532 unt; 0 nHn; 167 RR)
% Number of literals : 532 ( 531 equ; 7 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 : 15 ( 15 usr; 10 con; 0-2 aty)
% Number of variables : 593 ( 102 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t14,axiom,
sFlat0 = composition(sk2,sk3),
introduced(definition) ).
cnf(t63,plain,
composition(sk2,sk3) = sFlat0,
inference(orient,[status(thm)],[t14]) ).
cnf(t6,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t68,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t70,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t68,t23]) ).
cnf(t123363,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t70,t68]) ).
cnf(t85,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t123363]) ).
cnf(t15,axiom,
sFlat1 = meet(sk1,composition(sk2,sk3)),
introduced(definition) ).
cnf(t123361,plain,
sFlat1 = meet(sk1,sFlat0),
inference(step,[status(thm)],[t15,t63]) ).
cnf(t77,plain,
meet(sk1,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t123361]) ).
cnf(t87,plain,
meet(sk1,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t77]) ).
cnf(t123365,plain,
meet(sFlat0,sk1) = sFlat1,
inference(step,[status(thm)],[t87,t85]) ).
cnf(t89,plain,
meet(sFlat0,sk1) = sFlat1,
inference(orient,[status(thm)],[t123365]) ).
cnf(t16,axiom,
sFlat2 = meet(sk1,sk2),
introduced(definition) ).
cnf(t78,plain,
meet(sk1,sk2) = sFlat2,
inference(orient,[status(thm)],[t16]) ).
cnf(t86,plain,
meet(sk1,sk2) = sFlat2,
inference(rw,[status(thm)],[t78]) ).
cnf(t123364,plain,
meet(sk2,sk1) = sFlat2,
inference(step,[status(thm)],[t86,t85]) ).
cnf(t88,plain,
meet(sk2,sk1) = sFlat2,
inference(orient,[status(thm)],[t123364]) ).
cnf(t17,axiom,
sFlat3 = composition(meet(sk1,sk2),sk3),
introduced(definition) ).
cnf(t58,plain,
composition(meet(sk1,sk2),sk3) = sFlat3,
inference(orient,[status(thm)],[t17]) ).
cnf(t123362,plain,
composition(sFlat2,sk3) = sFlat3,
inference(step,[status(thm)],[t58,t78]) ).
cnf(t79,plain,
composition(sFlat2,sk3) = sFlat3,
inference(rw,[status(thm)],[t123362]) ).
cnf(t80,plain,
composition(sFlat2,sk3) = sFlat3,
inference(orient,[status(thm)],[t79]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t19,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)],[t18,t18]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t27,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t25,t23]) ).
cnf(t123372,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t27,t25]) ).
cnf(t179,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t123372]) ).
cnf(t123381,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)],[t19,t179]) ).
cnf(t123382,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)],[t123381,t23]) ).
cnf(t123383,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t123382,t68]) ).
cnf(t294,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t123383]) ).
cnf(t314,plain,
meet(X1,join(complement(X1),join(X2,meet(X1,X2)))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t68,t294]) ).
cnf(t72,plain,
meet(join(complement(X1),complement(X2)),X3) = complement(join(meet(X1,X2),complement(X3))),
inference(cp,[status(thm)],[t68,t68]) ).
cnf(t564,plain,
complement(join(meet(X1,X2),complement(X3))) = meet(join(complement(X1),complement(X2)),X3),
inference(orient,[status(thm)],[t72]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t69,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t68,t28]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t75,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t123366,plain,
zero = complement(top),
inference(step,[status(thm)],[t69,t75]) ).
cnf(t90,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t123366]) ).
cnf(t571,plain,
meet(join(complement(X1),complement(X2)),top) = complement(join(meet(X1,X2),zero)),
inference(cp,[status(thm)],[t564,t90]) ).
cnf(t123550,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(meet(X1,X2),zero)),
inference(step,[status(thm)],[t571,t85]) ).
cnf(t123551,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t123550,t23]) ).
cnf(t1718,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t123551]) ).
cnf(t24,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t18]) ).
cnf(t123495,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t24,t23]) ).
cnf(t123496,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t123495,t68]) ).
cnf(t123497,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t123496,t23]) ).
cnf(t1364,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t123497]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t123360,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t23]) ).
cnf(t33,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t123360]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t46,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t2,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t48,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t46,t22]) ).
cnf(t139,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t48]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t140,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t139,t21]) ).
cnf(t123369,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t140,t22]) ).
cnf(t154,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t123369]) ).
cnf(t9,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t41,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t42,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t41,t21]) ).
cnf(t99,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t42]) ).
cnf(t156,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t154,t99]) ).
cnf(t123371,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t156,t154]) ).
cnf(t172,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t123371]) ).
cnf(t175,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t33,t172]) ).
cnf(t155,plain,
one = converse(one),
inference(cp,[status(thm)],[t154,t21]) ).
cnf(t161,plain,
converse(one) = one,
inference(orient,[status(thm)],[t155]) ).
cnf(t123376,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t175,t161]) ).
cnf(t123377,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t123376,t172]) ).
cnf(t254,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t123377]) ).
cnf(t1380,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t1364,t254]) ).
cnf(t123501,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t1380,t23]) ).
cnf(t123502,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t123501,t75]) ).
cnf(t123503,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t123502,t23]) ).
cnf(t1424,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t123503]) ).
cnf(t263,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t68,t254]) ).
cnf(t267,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t263]) ).
cnf(t1430,plain,
complement(X1) = join(zero,complement(meet(X1,X1))),
inference(cp,[status(thm)],[t1424,t267]) ).
cnf(t1580,plain,
join(zero,complement(meet(X1,X1))) = complement(X1),
inference(orient,[status(thm)],[t1430]) ).
cnf(t1731,plain,
complement(join(zero,meet(X1,top))) = meet(top,join(complement(X1),zero)),
inference(cp,[status(thm)],[t1718,t90]) ).
cnf(t30,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t25,t28]) ).
cnf(t276,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t30]) ).
cnf(t280,plain,
join(top,complement(complement(X1))) = join(X1,top),
inference(cp,[status(thm)],[t276,t28]) ).
cnf(t279,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t276,t254]) ).
cnf(t123384,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t279,t28]) ).
cnf(t316,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t123384]) ).
cnf(t123385,plain,
top = join(X1,top),
inference(step,[status(thm)],[t280,t316]) ).
cnf(t320,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t123385]) ).
cnf(t1389,plain,
X1 = join(meet(X1,top),complement(top)),
inference(cp,[status(thm)],[t1364,t320]) ).
cnf(t123499,plain,
X1 = join(complement(top),meet(X1,top)),
inference(step,[status(thm)],[t1389,t23]) ).
cnf(t123500,plain,
X1 = join(zero,meet(X1,top)),
inference(step,[status(thm)],[t123499,t90]) ).
cnf(t1419,plain,
join(zero,meet(X1,top)) = X1,
inference(orient,[status(thm)],[t123500]) ).
cnf(t123552,plain,
complement(X1) = meet(top,join(complement(X1),zero)),
inference(step,[status(thm)],[t1731,t1419]) ).
cnf(t123553,plain,
complement(X1) = meet(top,join(zero,complement(X1))),
inference(step,[status(thm)],[t123552,t23]) ).
cnf(t1738,plain,
meet(top,join(zero,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t123553]) ).
cnf(t1741,plain,
complement(meet(X1,X1)) = meet(top,complement(X1)),
inference(cp,[status(thm)],[t1738,t1580]) ).
cnf(t93,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t68,t90]) ).
cnf(t238,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t93]) ).
cnf(t1432,plain,
meet(top,complement(X1)) = complement(X1),
inference(cp,[status(thm)],[t238,t1424]) ).
cnf(t1433,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1432]) ).
cnf(t123571,plain,
complement(meet(X1,X1)) = complement(X1),
inference(step,[status(thm)],[t1741,t1433]) ).
cnf(t1919,plain,
complement(meet(X1,X1)) = complement(X1),
inference(orient,[status(thm)],[t123571]) ).
cnf(t123572,plain,
join(zero,complement(X1)) = complement(X1),
inference(step,[status(thm)],[t1580,t1919]) ).
cnf(t1935,plain,
join(zero,complement(X1)) = complement(X1),
inference(rw,[status(thm)],[t123572]) ).
cnf(t1952,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1935]) ).
cnf(t1959,plain,
complement(join(complement(X1),complement(X2))) = join(zero,meet(X1,X2)),
inference(cp,[status(thm)],[t1952,t68]) ).
cnf(t123581,plain,
meet(X1,X2) = join(zero,meet(X1,X2)),
inference(step,[status(thm)],[t1959,t68]) ).
cnf(t1971,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t123581]) ).
cnf(t123582,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t1718,t1971]) ).
cnf(t1972,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t123582]) ).
cnf(t1367,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t1364,t75]) ).
cnf(t123498,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t1367,t68]) ).
cnf(t1411,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t123498]) ).
cnf(t123586,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t1411,t1971]) ).
cnf(t1976,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t123586]) ).
cnf(t1978,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1976]) ).
cnf(t1979,plain,
meet(X1,X1) = join(zero,X1),
inference(cp,[status(thm)],[t1971,t1978]) ).
cnf(t123594,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t1979,t1978]) ).
cnf(t2005,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t123594]) ).
cnf(t2009,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t2005,t23]) ).
cnf(t2028,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t2009]) ).
cnf(t2034,plain,
X1 = join(meet(X1,zero),complement(complement(X1))),
inference(cp,[status(thm)],[t1364,t2028]) ).
cnf(t91,plain,
zero = meet(top,zero),
inference(cp,[status(thm)],[t75,t90]) ).
cnf(t123367,plain,
zero = meet(zero,top),
inference(step,[status(thm)],[t91,t85]) ).
cnf(t96,plain,
meet(zero,top) = zero,
inference(orient,[status(thm)],[t123367]) ).
cnf(t1806,plain,
meet(zero,top) = zero,
inference(rw,[status(thm)],[t96]) ).
cnf(t1746,plain,
complement(complement(X1)) = meet(top,join(zero,meet(X1,X1))),
inference(cp,[status(thm)],[t1738,t267]) ).
cnf(t123556,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t1746,t1411]) ).
cnf(t1750,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t123556]) ).
cnf(t123557,plain,
meet(X1,X1) = meet(top,X1),
inference(step,[status(thm)],[t267,t1750]) ).
cnf(t1776,plain,
meet(X1,X1) = meet(top,X1),
inference(rw,[status(thm)],[t123557]) ).
cnf(t1779,plain,
meet(X1,X1) = meet(top,X1),
inference(orient,[status(thm)],[t1776]) ).
cnf(t1787,plain,
meet(X1,X1) = meet(X1,top),
inference(cp,[status(thm)],[t1779,t85]) ).
cnf(t1793,plain,
meet(X1,X1) = meet(X1,top),
inference(orient,[status(thm)],[t1787]) ).
cnf(t123562,plain,
meet(zero,zero) = zero,
inference(step,[status(thm)],[t1806,t1793]) ).
cnf(t1817,plain,
meet(zero,zero) = zero,
inference(orient,[status(thm)],[t123562]) ).
cnf(t1818,plain,
complement(zero) = join(zero,complement(zero)),
inference(cp,[status(thm)],[t1580,t1817]) ).
cnf(t123563,plain,
complement(zero) = top,
inference(step,[status(thm)],[t1818,t28]) ).
cnf(t1822,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t123563]) ).
cnf(t1826,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t68,t1822]) ).
cnf(t123568,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t1826,t320]) ).
cnf(t123569,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t123568,t90]) ).
cnf(t1899,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t123569]) ).
cnf(t123601,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t2034,t1899]) ).
cnf(t123602,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t123601,t1952]) ).
cnf(t123603,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t123602,t1750]) ).
cnf(t2040,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t123603]) ).
cnf(t123607,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t1972,t2040]) ).
cnf(t2047,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t123607]) ).
cnf(t2163,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t2047]) ).
cnf(t73,plain,
meet(X1,join(complement(X2),complement(X3))) = complement(join(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t68,t68]) ).
cnf(t588,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,join(complement(X2),complement(X3))),
inference(orient,[status(thm)],[t73]) ).
cnf(t2044,plain,
meet(X1,join(complement(top),complement(X2))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t588,t2040]) ).
cnf(t123620,plain,
meet(X1,join(zero,complement(X2))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t2044,t90]) ).
cnf(t123621,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t123620,t1952]) ).
cnf(t2124,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t123621]) ).
cnf(t2138,plain,
meet(X1,complement(X2)) = complement(join(X2,complement(X1))),
inference(cp,[status(thm)],[t2124,t23]) ).
cnf(t2177,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t2138]) ).
cnf(t2186,plain,
complement(meet(X1,join(X2,complement(X3)))) = join(complement(X1),meet(X3,complement(X2))),
inference(cp,[status(thm)],[t2163,t2177]) ).
cnf(t18889,plain,
complement(meet(X1,join(X2,complement(X3)))) = join(complement(X1),meet(X3,complement(X2))),
inference(orient,[status(thm)],[t2186]) ).
cnf(t1374,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t1364,t68]) ).
cnf(t123533,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t1374,t23]) ).
cnf(t1551,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t123533]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t37,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t40,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t25,t37]) ).
cnf(t460,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t40]) ).
cnf(t468,plain,
join(converse(join(X1,X2)),complement(converse(X2))) = join(converse(X1),top),
inference(cp,[status(thm)],[t460,t28]) ).
cnf(t123400,plain,
join(complement(converse(X2)),converse(join(X1,X2))) = join(converse(X1),top),
inference(step,[status(thm)],[t468,t23]) ).
cnf(t123401,plain,
join(complement(converse(X2)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t123400,t320]) ).
cnf(t627,plain,
join(complement(converse(X1)),converse(join(X2,X1))) = top,
inference(orient,[status(thm)],[t123401]) ).
cnf(t639,plain,
top = join(complement(converse(top)),converse(top)),
inference(cp,[status(thm)],[t627,t320]) ).
cnf(t38,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t37,t22]) ).
cnf(t109,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t38]) ).
cnf(t324,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t109,t320]) ).
cnf(t325,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t324]) ).
cnf(t123402,plain,
top = converse(top),
inference(step,[status(thm)],[t639,t325]) ).
cnf(t664,plain,
converse(top) = top,
inference(orient,[status(thm)],[t123402]) ).
cnf(t671,plain,
converse(join(top,X1)) = join(top,converse(X1)),
inference(cp,[status(thm)],[t37,t664]) ).
cnf(t727,plain,
converse(join(top,X1)) = join(top,converse(X1)),
inference(orient,[status(thm)],[t671]) ).
cnf(t739,plain,
join(top,converse(X1)) = converse(join(X1,top)),
inference(cp,[status(thm)],[t727,t23]) ).
cnf(t123412,plain,
join(top,converse(X1)) = converse(top),
inference(step,[status(thm)],[t739,t320]) ).
cnf(t123413,plain,
join(top,converse(X1)) = top,
inference(step,[status(thm)],[t123412,t664]) ).
cnf(t758,plain,
join(top,converse(X1)) = top,
inference(orient,[status(thm)],[t123413]) ).
cnf(t47,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t46,t22]) ).
cnf(t127,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t47]) ).
cnf(t763,plain,
top = join(top,composition(X1,converse(X2))),
inference(cp,[status(thm)],[t758,t127]) ).
cnf(t779,plain,
join(top,composition(X1,converse(X2))) = top,
inference(orient,[status(thm)],[t763]) ).
cnf(t785,plain,
top = join(top,composition(X1,one)),
inference(cp,[status(thm)],[t779,t161]) ).
cnf(t123421,plain,
top = join(top,X1),
inference(step,[status(thm)],[t785,t21]) ).
cnf(t852,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t123421]) ).
cnf(t123422,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t276,t852]) ).
cnf(t853,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t123422]) ).
cnf(t2174,plain,
top = join(X1,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t853,t2163]) ).
cnf(t2356,plain,
join(X1,complement(meet(X1,X2))) = top,
inference(orient,[status(thm)],[t2174]) ).
cnf(t2365,plain,
meet(X1,complement(complement(meet(complement(X1),X2)))) = complement(top),
inference(cp,[status(thm)],[t2124,t2356]) ).
cnf(t123604,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t1750,t2040]) ).
cnf(t2041,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t123604]) ).
cnf(t123674,plain,
meet(X1,meet(complement(X1),X2)) = complement(top),
inference(step,[status(thm)],[t2365,t2041]) ).
cnf(t123675,plain,
meet(X1,meet(complement(X1),X2)) = zero,
inference(step,[status(thm)],[t123674,t90]) ).
cnf(t2531,plain,
meet(X1,meet(complement(X1),X2)) = zero,
inference(orient,[status(thm)],[t123675]) ).
cnf(t2536,plain,
X1 = join(zero,meet(X1,complement(meet(complement(X1),X2)))),
inference(cp,[status(thm)],[t1551,t2531]) ).
cnf(t123717,plain,
X1 = meet(X1,complement(meet(complement(X1),X2))),
inference(step,[status(thm)],[t2536,t1971]) ).
cnf(t2166,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t2163,t2041]) ).
cnf(t2217,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t2166]) ).
cnf(t123718,plain,
X1 = meet(X1,join(X1,complement(X2))),
inference(step,[status(thm)],[t123717,t2217]) ).
cnf(t3363,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t123718]) ).
cnf(t3367,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t3363,t2041]) ).
cnf(t3371,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t3367]) ).
cnf(t18890,plain,
join(complement(X1),meet(X2,complement(X1))) = complement(X1),
inference(cp,[status(thm)],[t18889,t3371]) ).
cnf(t18980,plain,
join(complement(X1),meet(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t18890]) ).
cnf(t18996,plain,
complement(complement(X1)) = join(X1,meet(X2,complement(complement(X1)))),
inference(cp,[status(thm)],[t18980,t2041]) ).
cnf(t124172,plain,
X1 = join(X1,meet(X2,complement(complement(X1)))),
inference(step,[status(thm)],[t18996,t2041]) ).
cnf(t124173,plain,
X1 = join(X1,meet(X2,X1)),
inference(step,[status(thm)],[t124172,t2041]) ).
cnf(t19025,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t124173]) ).
cnf(t124415,plain,
meet(X1,join(complement(X1),X2)) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t314,t19025]) ).
cnf(t124416,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(step,[status(thm)],[t124415,t68]) ).
cnf(t25957,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t124416]) ).
cnf(t26002,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(complement(X1),X3))),
inference(cp,[status(thm)],[t25957,t179]) ).
cnf(t28736,plain,
meet(X1,join(X2,join(complement(X1),X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t26002]) ).
cnf(t28753,plain,
meet(X1,join(X2,complement(X3))) = meet(X1,join(X2,complement(meet(X1,X3)))),
inference(cp,[status(thm)],[t28736,t2163]) ).
cnf(t33736,plain,
meet(X1,join(X2,complement(meet(X1,X3)))) = meet(X1,join(X2,complement(X3))),
inference(orient,[status(thm)],[t28753]) ).
cnf(t2143,plain,
meet(X1,complement(join(X2,X3))) = complement(join(X2,join(complement(X1),X3))),
inference(cp,[status(thm)],[t2124,t179]) ).
cnf(t11457,plain,
complement(join(X1,join(complement(X2),X3))) = meet(X2,complement(join(X1,X3))),
inference(orient,[status(thm)],[t2143]) ).
cnf(t11474,plain,
meet(X1,complement(join(X2,complement(X3)))) = complement(join(X2,complement(meet(X1,X3)))),
inference(cp,[status(thm)],[t11457,t2163]) ).
cnf(t123989,plain,
meet(X1,meet(X3,complement(X2))) = complement(join(X2,complement(meet(X1,X3)))),
inference(step,[status(thm)],[t11474,t2177]) ).
cnf(t123990,plain,
meet(X1,meet(X3,complement(X2))) = meet(meet(X1,X3),complement(X2)),
inference(step,[status(thm)],[t123989,t2177]) ).
cnf(t11634,plain,
meet(meet(X1,X2),complement(X3)) = meet(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t123990]) ).
cnf(t11695,plain,
meet(sFlat0,meet(sk1,complement(X1))) = meet(sFlat1,complement(X1)),
inference(cp,[status(thm)],[t11634,t89]) ).
cnf(t11795,plain,
meet(sFlat0,meet(sk1,complement(X1))) = meet(sFlat1,complement(X1)),
inference(orient,[status(thm)],[t11695]) ).
cnf(t1557,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t1551,t85]) ).
cnf(t2630,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t1557]) ).
cnf(t36,plain,
join(complement(X1),join(composition(converse(X2),complement(composition(X2,X1))),X3)) = join(complement(X1),X3),
inference(cp,[status(thm)],[t25,t33]) ).
cnf(t3386,plain,
join(complement(X1),join(composition(converse(X2),complement(composition(X2,X1))),X3)) = join(complement(X1),X3),
inference(orient,[status(thm)],[t36]) ).
cnf(t3401,plain,
join(complement(X1),complement(composition(converse(X2),complement(composition(X2,X1))))) = join(complement(X1),top),
inference(cp,[status(thm)],[t3386,t28]) ).
cnf(t124139,plain,
complement(meet(X1,composition(converse(X2),complement(composition(X2,X1))))) = join(complement(X1),top),
inference(step,[status(thm)],[t3401,t2163]) ).
cnf(t124140,plain,
complement(meet(X1,composition(converse(X2),complement(composition(X2,X1))))) = top,
inference(step,[status(thm)],[t124139,t320]) ).
cnf(t17723,plain,
complement(meet(X1,composition(converse(X2),complement(composition(X2,X1))))) = top,
inference(orient,[status(thm)],[t124140]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t53,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t57,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t33,t53]) ).
cnf(t123451,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t57,t90]) ).
cnf(t123452,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t123451,t90]) ).
cnf(t1161,plain,
join(zero,composition(converse(sk1),complement(sk1))) = zero,
inference(orient,[status(thm)],[t123452]) ).
cnf(t123600,plain,
composition(converse(sk1),complement(sk1)) = zero,
inference(step,[status(thm)],[t1161,t2005]) ).
cnf(t2027,plain,
composition(converse(sk1),complement(sk1)) = zero,
inference(rw,[status(thm)],[t123600]) ).
cnf(t2094,plain,
composition(converse(sk1),complement(sk1)) = zero,
inference(orient,[status(thm)],[t2027]) ).
cnf(t2095,plain,
composition(converse(sk1),composition(complement(sk1),X1)) = composition(zero,X1),
inference(cp,[status(thm)],[t41,t2094]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t173,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t31,t172]) ).
cnf(t377,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t173]) ).
cnf(t380,plain,
join(X1,composition(converse(top),X1)) = composition(converse(top),X1),
inference(cp,[status(thm)],[t377,t325]) ).
cnf(t497,plain,
join(X1,composition(converse(top),X1)) = composition(converse(top),X1),
inference(orient,[status(thm)],[t380]) ).
cnf(t504,plain,
join(X1,converse(composition(converse(top),converse(X1)))) = converse(composition(converse(top),converse(X1))),
inference(cp,[status(thm)],[t109,t497]) ).
cnf(t123392,plain,
join(X1,composition(converse(converse(X1)),top)) = converse(composition(converse(top),converse(X1))),
inference(step,[status(thm)],[t504,t139]) ).
cnf(t123393,plain,
join(X1,composition(X1,top)) = converse(composition(converse(top),converse(X1))),
inference(step,[status(thm)],[t123392,t22]) ).
cnf(t123394,plain,
join(X1,composition(X1,top)) = composition(converse(converse(X1)),top),
inference(step,[status(thm)],[t123393,t139]) ).
cnf(t123395,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t123394,t22]) ).
cnf(t505,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t123395]) ).
cnf(t857,plain,
top = composition(top,top),
inference(cp,[status(thm)],[t852,t505]) ).
cnf(t860,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t857]) ).
cnf(t864,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t33,t860]) ).
cnf(t123428,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t864,t90]) ).
cnf(t123429,plain,
zero = composition(converse(top),complement(top)),
inference(step,[status(thm)],[t123428,t497]) ).
cnf(t123430,plain,
zero = composition(top,complement(top)),
inference(step,[status(thm)],[t123429,t664]) ).
cnf(t123431,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t123430,t90]) ).
cnf(t865,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t123431]) ).
cnf(t868,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t31,t865]) ).
cnf(t123434,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t868,t852]) ).
cnf(t123435,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t123434,t865]) ).
cnf(t887,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t123435]) ).
cnf(t123595,plain,
composition(X1,zero) = zero,
inference(step,[status(thm)],[t887,t2005]) ).
cnf(t2022,plain,
composition(X1,zero) = zero,
inference(rw,[status(thm)],[t123595]) ).
cnf(t2037,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t2022]) ).
cnf(t2039,plain,
composition(converse(zero),X1) = converse(zero),
inference(cp,[status(thm)],[t139,t2037]) ).
cnf(t39,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t37,t22]) ).
cnf(t118,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t39]) ).
cnf(t2015,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t118,t2005]) ).
cnf(t123609,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t2015,t22]) ).
cnf(t2052,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t123609]) ).
cnf(t2053,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t2052,t2028]) ).
cnf(t2074,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t2053]) ).
cnf(t123612,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t2039,t2074]) ).
cnf(t123613,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t123612,t2074]) ).
cnf(t2093,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t123613]) ).
cnf(t123741,plain,
composition(converse(sk1),composition(complement(sk1),X1)) = zero,
inference(step,[status(thm)],[t2095,t2093]) ).
cnf(t4075,plain,
composition(converse(sk1),composition(complement(sk1),X1)) = zero,
inference(orient,[status(thm)],[t123741]) ).
cnf(t17849,plain,
top = complement(meet(composition(complement(sk1),X1),composition(converse(converse(sk1)),complement(zero)))),
inference(cp,[status(thm)],[t17723,t4075]) ).
cnf(t124141,plain,
top = complement(meet(composition(complement(sk1),X1),composition(sk1,complement(zero)))),
inference(step,[status(thm)],[t17849,t22]) ).
cnf(t124142,plain,
top = complement(meet(composition(sk1,complement(zero)),composition(complement(sk1),X1))),
inference(step,[status(thm)],[t124141,t85]) ).
cnf(t124143,plain,
top = complement(meet(composition(sk1,top),composition(complement(sk1),X1))),
inference(step,[status(thm)],[t124142,t1822]) ).
cnf(t124144,plain,
top = complement(meet(sk1,composition(complement(sk1),X1))),
inference(step,[status(thm)],[t124143,t53]) ).
cnf(t17941,plain,
complement(meet(sk1,composition(complement(sk1),X1))) = top,
inference(orient,[status(thm)],[t124144]) ).
cnf(t17948,plain,
zero = meet(meet(sk1,composition(complement(sk1),X1)),top),
inference(cp,[status(thm)],[t75,t17941]) ).
cnf(t2043,plain,
X1 = meet(X1,top),
inference(cp,[status(thm)],[t2040,t85]) ).
cnf(t2048,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t2043]) ).
cnf(t124145,plain,
zero = meet(sk1,composition(complement(sk1),X1)),
inference(step,[status(thm)],[t17948,t2048]) ).
cnf(t17973,plain,
meet(sk1,composition(complement(sk1),X1)) = zero,
inference(orient,[status(thm)],[t124145]) ).
cnf(t17976,plain,
sk1 = join(zero,meet(complement(composition(complement(sk1),X1)),sk1)),
inference(cp,[status(thm)],[t2630,t17973]) ).
cnf(t124146,plain,
sk1 = meet(complement(composition(complement(sk1),X1)),sk1),
inference(step,[status(thm)],[t17976,t1971]) ).
cnf(t124147,plain,
sk1 = meet(sk1,complement(composition(complement(sk1),X1))),
inference(step,[status(thm)],[t124146,t85]) ).
cnf(t18004,plain,
meet(sk1,complement(composition(complement(sk1),X1))) = sk1,
inference(orient,[status(thm)],[t124147]) ).
cnf(t18007,plain,
meet(sFlat1,complement(composition(complement(sk1),X1))) = meet(sFlat0,sk1),
inference(cp,[status(thm)],[t11795,t18004]) ).
cnf(t124151,plain,
meet(sFlat1,complement(composition(complement(sk1),X1))) = sFlat1,
inference(step,[status(thm)],[t18007,t89]) ).
cnf(t18025,plain,
meet(sFlat1,complement(composition(complement(sk1),X1))) = sFlat1,
inference(orient,[status(thm)],[t124151]) ).
cnf(t33934,plain,
meet(sFlat1,join(X1,complement(complement(composition(complement(sk1),X2))))) = meet(sFlat1,join(X1,complement(sFlat1))),
inference(cp,[status(thm)],[t33736,t18025]) ).
cnf(t127031,plain,
meet(sFlat1,join(X1,composition(complement(sk1),X2))) = meet(sFlat1,join(X1,complement(sFlat1))),
inference(step,[status(thm)],[t33934,t2041]) ).
cnf(t25990,plain,
meet(X1,X2) = meet(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t25957,t23]) ).
cnf(t26041,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t25990]) ).
cnf(t127032,plain,
meet(sFlat1,join(X1,composition(complement(sk1),X2))) = meet(sFlat1,X1),
inference(step,[status(thm)],[t127031,t26041]) ).
cnf(t123093,plain,
meet(sFlat1,join(X1,composition(complement(sk1),X2))) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t127032]) ).
cnf(t65,plain,
composition(join(sk2,X1),sk3) = join(sFlat0,composition(X1,sk3)),
inference(cp,[status(thm)],[t31,t63]) ).
cnf(t219,plain,
composition(join(sk2,X1),sk3) = join(sFlat0,composition(X1,sk3)),
inference(orient,[status(thm)],[t65]) ).
cnf(t26035,plain,
join(complement(X1),meet(X2,complement(complement(X1)))) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t18889,t25957]) ).
cnf(t124439,plain,
join(complement(X1),meet(X2,X1)) = complement(meet(X1,complement(X2))),
inference(step,[status(thm)],[t26035,t2041]) ).
cnf(t2169,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t2163,t2041]) ).
cnf(t2234,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t2169]) ).
cnf(t124440,plain,
join(complement(X1),meet(X2,X1)) = join(complement(X1),X2),
inference(step,[status(thm)],[t124439,t2234]) ).
cnf(t26766,plain,
join(complement(X1),meet(X2,X1)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t124440]) ).
cnf(t26825,plain,
join(complement(sk1),sk2) = join(complement(sk1),sFlat2),
inference(cp,[status(thm)],[t26766,t88]) ).
cnf(t124444,plain,
join(sk2,complement(sk1)) = join(complement(sk1),sFlat2),
inference(step,[status(thm)],[t26825,t23]) ).
cnf(t124445,plain,
join(sk2,complement(sk1)) = join(sFlat2,complement(sk1)),
inference(step,[status(thm)],[t124444,t23]) ).
cnf(t26855,plain,
join(sk2,complement(sk1)) = join(sFlat2,complement(sk1)),
inference(orient,[status(thm)],[t124445]) ).
cnf(t26858,plain,
join(sFlat0,composition(complement(sk1),sk3)) = composition(join(sFlat2,complement(sk1)),sk3),
inference(cp,[status(thm)],[t219,t26855]) ).
cnf(t82,plain,
composition(join(sFlat2,X1),sk3) = join(sFlat3,composition(X1,sk3)),
inference(cp,[status(thm)],[t31,t80]) ).
cnf(t328,plain,
composition(join(sFlat2,X1),sk3) = join(sFlat3,composition(X1,sk3)),
inference(orient,[status(thm)],[t82]) ).
cnf(t124933,plain,
join(sFlat0,composition(complement(sk1),sk3)) = join(sFlat3,composition(complement(sk1),sk3)),
inference(step,[status(thm)],[t26858,t328]) ).
cnf(t39711,plain,
join(sFlat3,composition(complement(sk1),sk3)) = join(sFlat0,composition(complement(sk1),sk3)),
inference(orient,[status(thm)],[t124933]) ).
cnf(t123097,plain,
meet(sFlat1,sFlat3) = meet(sFlat1,join(sFlat0,composition(complement(sk1),sk3))),
inference(cp,[status(thm)],[t123093,t39711]) ).
cnf(t25968,plain,
meet(X1,complement(X2)) = meet(X1,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t25957,t2163]) ).
cnf(t26094,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t25968]) ).
cnf(t282,plain,
join(top,join(X1,X2)) = join(X3,join(X1,join(complement(X3),X2))),
inference(cp,[status(thm)],[t276,t179]) ).
cnf(t123736,plain,
top = join(X3,join(X1,join(complement(X3),X2))),
inference(step,[status(thm)],[t282,t852]) ).
cnf(t3967,plain,
join(X1,join(X2,join(complement(X1),X3))) = top,
inference(orient,[status(thm)],[t123736]) ).
cnf(t3997,plain,
meet(X1,complement(join(X2,join(complement(complement(X1)),X3)))) = complement(top),
inference(cp,[status(thm)],[t2124,t3967]) ).
cnf(t124161,plain,
meet(X1,complement(join(X2,join(X1,X3)))) = complement(top),
inference(step,[status(thm)],[t3997,t2041]) ).
cnf(t124162,plain,
meet(X1,complement(join(X2,join(X1,X3)))) = zero,
inference(step,[status(thm)],[t124161,t90]) ).
cnf(t18302,plain,
meet(X1,complement(join(X2,join(X1,X3)))) = zero,
inference(orient,[status(thm)],[t124162]) ).
cnf(t122,plain,
converse(composition(join(X1,converse(X2)),X3)) = composition(converse(X3),join(converse(X1),X2)),
inference(cp,[status(thm)],[t46,t118]) ).
cnf(t2869,plain,
converse(composition(join(X1,converse(X2)),X3)) = composition(converse(X3),join(converse(X1),X2)),
inference(orient,[status(thm)],[t122]) ).
cnf(t50,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t31,t46]) ).
cnf(t8888,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t50]) ).
cnf(t8967,plain,
composition(join(converse(sk3),X1),converse(sFlat2)) = join(converse(sFlat3),composition(X1,converse(sFlat2))),
inference(cp,[status(thm)],[t8888,t80]) ).
cnf(t9727,plain,
composition(join(converse(sk3),X1),converse(sFlat2)) = join(converse(sFlat3),composition(X1,converse(sFlat2))),
inference(orient,[status(thm)],[t8967]) ).
cnf(t9797,plain,
composition(converse(converse(sFlat2)),join(converse(converse(sk3)),X1)) = converse(join(converse(sFlat3),composition(converse(X1),converse(sFlat2)))),
inference(cp,[status(thm)],[t2869,t9727]) ).
cnf(t123947,plain,
composition(sFlat2,join(converse(converse(sk3)),X1)) = converse(join(converse(sFlat3),composition(converse(X1),converse(sFlat2)))),
inference(step,[status(thm)],[t9797,t22]) ).
cnf(t123948,plain,
composition(sFlat2,join(sk3,X1)) = converse(join(converse(sFlat3),composition(converse(X1),converse(sFlat2)))),
inference(step,[status(thm)],[t123947,t22]) ).
cnf(t123949,plain,
composition(sFlat2,join(sk3,X1)) = join(sFlat3,converse(composition(converse(X1),converse(sFlat2)))),
inference(step,[status(thm)],[t123948,t109]) ).
cnf(t123950,plain,
composition(sFlat2,join(sk3,X1)) = join(sFlat3,composition(converse(converse(sFlat2)),X1)),
inference(step,[status(thm)],[t123949,t139]) ).
cnf(t123951,plain,
composition(sFlat2,join(sk3,X1)) = join(sFlat3,composition(sFlat2,X1)),
inference(step,[status(thm)],[t123950,t22]) ).
cnf(t9810,plain,
composition(sFlat2,join(sk3,X1)) = join(sFlat3,composition(sFlat2,X1)),
inference(orient,[status(thm)],[t123951]) ).
cnf(t399,plain,
join(X1,converse(composition(X2,converse(X1)))) = converse(composition(join(one,X2),converse(X1))),
inference(cp,[status(thm)],[t109,t377]) ).
cnf(t123485,plain,
join(X1,composition(X1,converse(X2))) = converse(composition(join(one,X2),converse(X1))),
inference(step,[status(thm)],[t399,t127]) ).
cnf(t123486,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,converse(join(one,X2))),
inference(step,[status(thm)],[t123485,t127]) ).
cnf(t164,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t37,t161]) ).
cnf(t181,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t164]) ).
cnf(t123487,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(step,[status(thm)],[t123486,t181]) ).
cnf(t1243,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(orient,[status(thm)],[t123487]) ).
cnf(t1262,plain,
composition(X1,join(one,converse(converse(X2)))) = join(X1,composition(X1,X2)),
inference(cp,[status(thm)],[t1243,t22]) ).
cnf(t123490,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(step,[status(thm)],[t1262,t22]) ).
cnf(t1312,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(orient,[status(thm)],[t123490]) ).
cnf(t383,plain,
join(X1,composition(complement(one),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t377,t28]) ).
cnf(t455,plain,
join(X1,composition(complement(one),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t383]) ).
cnf(t1314,plain,
join(X1,composition(X1,composition(complement(one),one))) = composition(X1,composition(top,one)),
inference(cp,[status(thm)],[t1312,t455]) ).
cnf(t123540,plain,
join(X1,composition(X1,complement(one))) = composition(X1,composition(top,one)),
inference(step,[status(thm)],[t1314,t21]) ).
cnf(t123541,plain,
join(X1,composition(X1,complement(one))) = composition(X1,top),
inference(step,[status(thm)],[t123540,t21]) ).
cnf(t1594,plain,
join(X1,composition(X1,complement(one))) = composition(X1,top),
inference(orient,[status(thm)],[t123541]) ).
cnf(t1601,plain,
top = join(X1,composition(complement(X1),top)),
inference(cp,[status(thm)],[t853,t1594]) ).
cnf(t1646,plain,
join(X1,composition(complement(X1),top)) = top,
inference(orient,[status(thm)],[t1601]) ).
cnf(t9830,plain,
join(sFlat3,composition(sFlat2,composition(complement(sk3),top))) = composition(sFlat2,top),
inference(cp,[status(thm)],[t9810,t1646]) ).
cnf(t20598,plain,
join(sFlat3,composition(sFlat2,composition(complement(sk3),top))) = composition(sFlat2,top),
inference(orient,[status(thm)],[t9830]) ).
cnf(t20609,plain,
zero = meet(sFlat3,complement(join(X1,composition(sFlat2,top)))),
inference(cp,[status(thm)],[t18302,t20598]) ).
cnf(t20612,plain,
meet(sFlat3,complement(join(X1,composition(sFlat2,top)))) = zero,
inference(orient,[status(thm)],[t20609]) ).
cnf(t56,plain,
composition(join(X1,sk1),top) = join(composition(X1,top),sk1),
inference(cp,[status(thm)],[t31,t53]) ).
cnf(t123374,plain,
composition(join(X1,sk1),top) = join(sk1,composition(X1,top)),
inference(step,[status(thm)],[t56,t23]) ).
cnf(t213,plain,
composition(join(X1,sk1),top) = join(sk1,composition(X1,top)),
inference(orient,[status(thm)],[t123374]) ).
cnf(t281,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t276,t23]) ).
cnf(t365,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t281]) ).
cnf(t123424,plain,
join(X1,join(X2,complement(X1))) = top,
inference(step,[status(thm)],[t365,t852]) ).
cnf(t855,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t123424]) ).
cnf(t2136,plain,
meet(X1,complement(join(X2,complement(complement(X1))))) = complement(top),
inference(cp,[status(thm)],[t2124,t855]) ).
cnf(t123651,plain,
meet(X1,meet(complement(X1),complement(X2))) = complement(top),
inference(step,[status(thm)],[t2136,t2177]) ).
cnf(t2183,plain,
meet(complement(X1),complement(X2)) = complement(join(X2,X1)),
inference(cp,[status(thm)],[t2177,t2041]) ).
cnf(t2252,plain,
meet(complement(X1),complement(X2)) = complement(join(X2,X1)),
inference(orient,[status(thm)],[t2183]) ).
cnf(t123652,plain,
meet(X1,complement(join(X2,X1))) = complement(top),
inference(step,[status(thm)],[t123651,t2252]) ).
cnf(t123653,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(step,[status(thm)],[t123652,t90]) ).
cnf(t2292,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t123653]) ).
cnf(t2315,plain,
X1 = join(zero,meet(X1,complement(complement(join(X2,X1))))),
inference(cp,[status(thm)],[t1551,t2292]) ).
cnf(t123654,plain,
X1 = meet(X1,complement(complement(join(X2,X1)))),
inference(step,[status(thm)],[t2315,t1971]) ).
cnf(t123655,plain,
X1 = meet(X1,join(X2,X1)),
inference(step,[status(thm)],[t123654,t2041]) ).
cnf(t2317,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t123655]) ).
cnf(t2333,plain,
complement(X1) = meet(complement(X1),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t2317,t2163]) ).
cnf(t123728,plain,
complement(X1) = complement(join(meet(X2,X1),X1)),
inference(step,[status(thm)],[t2333,t2252]) ).
cnf(t123729,plain,
complement(X1) = complement(join(X1,meet(X2,X1))),
inference(step,[status(thm)],[t123728,t23]) ).
cnf(t3836,plain,
complement(join(X1,meet(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t123729]) ).
cnf(t568,plain,
meet(join(complement(sk2),complement(sk1)),X1) = complement(join(sFlat2,complement(X1))),
inference(cp,[status(thm)],[t564,t88]) ).
cnf(t1194,plain,
meet(join(complement(sk2),complement(sk1)),X1) = complement(join(sFlat2,complement(X1))),
inference(orient,[status(thm)],[t568]) ).
cnf(t1415,plain,
join(complement(sk2),complement(sk1)) = join(zero,complement(join(sFlat2,complement(join(complement(sk2),complement(sk1)))))),
inference(cp,[status(thm)],[t1411,t1194]) ).
cnf(t123518,plain,
join(complement(sk2),complement(sk1)) = join(zero,complement(join(sFlat2,meet(sk2,sk1)))),
inference(step,[status(thm)],[t1415,t68]) ).
cnf(t123519,plain,
join(complement(sk2),complement(sk1)) = join(zero,complement(join(sFlat2,sFlat2))),
inference(step,[status(thm)],[t123518,t88]) ).
cnf(t255,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t254,t68]) ).
cnf(t123477,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t255,t68]) ).
cnf(t123478,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t123477,t68]) ).
cnf(t1233,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t123478]) ).
cnf(t1235,plain,
meet(sk2,sk1) = join(sFlat2,meet(sk2,sk1)),
inference(cp,[status(thm)],[t1233,t88]) ).
cnf(t123481,plain,
sFlat2 = join(sFlat2,meet(sk2,sk1)),
inference(step,[status(thm)],[t1235,t88]) ).
cnf(t123482,plain,
sFlat2 = join(sFlat2,sFlat2),
inference(step,[status(thm)],[t123481,t88]) ).
cnf(t1239,plain,
join(sFlat2,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t123482]) ).
cnf(t123520,plain,
join(complement(sk2),complement(sk1)) = join(zero,complement(sFlat2)),
inference(step,[status(thm)],[t123519,t1239]) ).
cnf(t1473,plain,
join(complement(sk2),complement(sk1)) = join(zero,complement(sFlat2)),
inference(orient,[status(thm)],[t123520]) ).
cnf(t1475,plain,
top = join(sk1,join(zero,complement(sFlat2))),
inference(cp,[status(thm)],[t855,t1473]) ).
cnf(t123530,plain,
top = join(zero,join(sk1,complement(sFlat2))),
inference(step,[status(thm)],[t1475,t179]) ).
cnf(t1507,plain,
join(zero,join(sk1,complement(sFlat2))) = top,
inference(orient,[status(thm)],[t123530]) ).
cnf(t123599,plain,
join(sk1,complement(sFlat2)) = top,
inference(step,[status(thm)],[t1507,t2005]) ).
cnf(t2026,plain,
join(sk1,complement(sFlat2)) = top,
inference(rw,[status(thm)],[t123599]) ).
cnf(t2089,plain,
join(sk1,complement(sFlat2)) = top,
inference(orient,[status(thm)],[t2026]) ).
cnf(t2180,plain,
meet(sFlat2,complement(sk1)) = complement(top),
inference(cp,[status(thm)],[t2177,t2089]) ).
cnf(t123631,plain,
meet(sFlat2,complement(sk1)) = zero,
inference(step,[status(thm)],[t2180,t90]) ).
cnf(t2204,plain,
meet(sFlat2,complement(sk1)) = zero,
inference(orient,[status(thm)],[t123631]) ).
cnf(t2205,plain,
sFlat2 = join(zero,meet(sFlat2,complement(complement(sk1)))),
inference(cp,[status(thm)],[t1551,t2204]) ).
cnf(t123632,plain,
sFlat2 = meet(sFlat2,complement(complement(sk1))),
inference(step,[status(thm)],[t2205,t1971]) ).
cnf(t123633,plain,
sFlat2 = meet(sFlat2,sk1),
inference(step,[status(thm)],[t123632,t2041]) ).
cnf(t2207,plain,
meet(sFlat2,sk1) = sFlat2,
inference(orient,[status(thm)],[t123633]) ).
cnf(t3838,plain,
complement(sk1) = complement(join(sk1,sFlat2)),
inference(cp,[status(thm)],[t3836,t2207]) ).
cnf(t123730,plain,
complement(sk1) = complement(join(sFlat2,sk1)),
inference(step,[status(thm)],[t3838,t23]) ).
cnf(t3846,plain,
complement(join(sFlat2,sk1)) = complement(sk1),
inference(orient,[status(thm)],[t123730]) ).
cnf(t3854,plain,
join(sFlat2,sk1) = complement(complement(sk1)),
inference(cp,[status(thm)],[t2041,t3846]) ).
cnf(t123731,plain,
join(sFlat2,sk1) = sk1,
inference(step,[status(thm)],[t3854,t2041]) ).
cnf(t3870,plain,
join(sFlat2,sk1) = sk1,
inference(orient,[status(thm)],[t123731]) ).
cnf(t3872,plain,
join(sk1,composition(sFlat2,top)) = composition(sk1,top),
inference(cp,[status(thm)],[t213,t3870]) ).
cnf(t123754,plain,
join(sk1,composition(sFlat2,top)) = sk1,
inference(step,[status(thm)],[t3872,t53]) ).
cnf(t4513,plain,
join(sk1,composition(sFlat2,top)) = sk1,
inference(orient,[status(thm)],[t123754]) ).
cnf(t20616,plain,
zero = meet(sFlat3,complement(sk1)),
inference(cp,[status(thm)],[t20612,t4513]) ).
cnf(t20623,plain,
meet(sFlat3,complement(sk1)) = zero,
inference(orient,[status(thm)],[t20616]) ).
cnf(t20626,plain,
sFlat3 = join(zero,meet(complement(complement(sk1)),sFlat3)),
inference(cp,[status(thm)],[t2630,t20623]) ).
cnf(t124235,plain,
sFlat3 = meet(complement(complement(sk1)),sFlat3),
inference(step,[status(thm)],[t20626,t1971]) ).
cnf(t124236,plain,
sFlat3 = meet(sFlat3,complement(complement(sk1))),
inference(step,[status(thm)],[t124235,t85]) ).
cnf(t124237,plain,
sFlat3 = meet(sFlat3,sk1),
inference(step,[status(thm)],[t124236,t2041]) ).
cnf(t20635,plain,
meet(sFlat3,sk1) = sFlat3,
inference(orient,[status(thm)],[t124237]) ).
cnf(t20638,plain,
meet(sFlat3,meet(sk1,complement(X1))) = meet(sFlat3,complement(X1)),
inference(cp,[status(thm)],[t11634,t20635]) ).
cnf(t23505,plain,
meet(sFlat3,meet(sk1,complement(X1))) = meet(sFlat3,complement(X1)),
inference(orient,[status(thm)],[t20638]) ).
cnf(t26822,plain,
join(complement(sk1),sFlat0) = join(complement(sk1),sFlat1),
inference(cp,[status(thm)],[t26766,t89]) ).
cnf(t124442,plain,
join(sFlat0,complement(sk1)) = join(complement(sk1),sFlat1),
inference(step,[status(thm)],[t26822,t23]) ).
cnf(t124443,plain,
join(sFlat0,complement(sk1)) = join(sFlat1,complement(sk1)),
inference(step,[status(thm)],[t124442,t23]) ).
cnf(t26843,plain,
join(sFlat1,complement(sk1)) = join(sFlat0,complement(sk1)),
inference(orient,[status(thm)],[t124443]) ).
cnf(t26850,plain,
meet(sk1,complement(sFlat1)) = complement(join(sFlat0,complement(sk1))),
inference(cp,[status(thm)],[t2177,t26843]) ).
cnf(t124446,plain,
meet(sk1,complement(sFlat1)) = meet(sk1,complement(sFlat0)),
inference(step,[status(thm)],[t26850,t2177]) ).
cnf(t26871,plain,
meet(sk1,complement(sFlat1)) = meet(sk1,complement(sFlat0)),
inference(orient,[status(thm)],[t124446]) ).
cnf(t26878,plain,
meet(sFlat3,complement(sFlat1)) = meet(sFlat3,meet(sk1,complement(sFlat0))),
inference(cp,[status(thm)],[t23505,t26871]) ).
cnf(t124459,plain,
meet(sFlat3,complement(sFlat1)) = meet(sFlat3,complement(sFlat0)),
inference(step,[status(thm)],[t26878,t23505]) ).
cnf(t1981,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t1233,t1978]) ).
cnf(t123592,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t1981,t1978]) ).
cnf(t123593,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t123592,t1978]) ).
cnf(t1991,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t123593]) ).
cnf(t1993,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t1991,t179]) ).
cnf(t123641,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t1993,t25]) ).
cnf(t123642,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t123641,t1991]) ).
cnf(t2263,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t123642]) ).
cnf(t1556,plain,
sk2 = join(sFlat2,meet(sk2,complement(sk1))),
inference(cp,[status(thm)],[t1551,t88]) ).
cnf(t1574,plain,
join(sFlat2,meet(sk2,complement(sk1))) = sk2,
inference(orient,[status(thm)],[t1556]) ).
cnf(t2265,plain,
join(sFlat2,meet(sk2,complement(sk1))) = join(sFlat2,sk2),
inference(cp,[status(thm)],[t2263,t1574]) ).
cnf(t123643,plain,
sk2 = join(sFlat2,sk2),
inference(step,[status(thm)],[t2265,t1574]) ).
cnf(t2269,plain,
join(sFlat2,sk2) = sk2,
inference(orient,[status(thm)],[t123643]) ).
cnf(t2270,plain,
join(sFlat3,composition(sk2,sk3)) = composition(sk2,sk3),
inference(cp,[status(thm)],[t328,t2269]) ).
cnf(t123646,plain,
join(sFlat3,sFlat0) = composition(sk2,sk3),
inference(step,[status(thm)],[t2270,t63]) ).
cnf(t123647,plain,
join(sFlat0,sFlat3) = composition(sk2,sk3),
inference(step,[status(thm)],[t123646,t23]) ).
cnf(t123648,plain,
join(sFlat0,sFlat3) = sFlat0,
inference(step,[status(thm)],[t123647,t63]) ).
cnf(t2274,plain,
join(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t123648]) ).
cnf(t2305,plain,
zero = meet(sFlat3,complement(sFlat0)),
inference(cp,[status(thm)],[t2292,t2274]) ).
cnf(t2495,plain,
meet(sFlat3,complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t2305]) ).
cnf(t124460,plain,
meet(sFlat3,complement(sFlat1)) = zero,
inference(step,[status(thm)],[t124459,t2495]) ).
cnf(t26940,plain,
meet(sFlat3,complement(sFlat1)) = zero,
inference(orient,[status(thm)],[t124460]) ).
cnf(t26943,plain,
meet(sFlat3,complement(complement(sFlat1))) = meet(sFlat3,complement(zero)),
inference(cp,[status(thm)],[t26094,t26940]) ).
cnf(t124466,plain,
meet(sFlat3,sFlat1) = meet(sFlat3,complement(zero)),
inference(step,[status(thm)],[t26943,t2041]) ).
cnf(t124467,plain,
meet(sFlat1,sFlat3) = meet(sFlat3,complement(zero)),
inference(step,[status(thm)],[t124466,t85]) ).
cnf(t124468,plain,
meet(sFlat1,sFlat3) = meet(sFlat3,top),
inference(step,[status(thm)],[t124467,t1822]) ).
cnf(t124469,plain,
meet(sFlat1,sFlat3) = sFlat3,
inference(step,[status(thm)],[t124468,t2048]) ).
cnf(t26965,plain,
meet(sFlat1,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t124469]) ).
cnf(t127033,plain,
sFlat3 = meet(sFlat1,join(sFlat0,composition(complement(sk1),sk3))),
inference(step,[status(thm)],[t123097,t26965]) ).
cnf(t127034,plain,
sFlat3 = meet(sFlat1,sFlat0),
inference(step,[status(thm)],[t127033,t123093]) ).
cnf(t127035,plain,
sFlat3 = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t127034,t85]) ).
cnf(t594,plain,
meet(X1,join(complement(sFlat0),complement(sk1))) = complement(join(complement(X1),sFlat1)),
inference(cp,[status(thm)],[t588,t89]) ).
cnf(t123465,plain,
meet(X1,join(complement(sFlat0),complement(sk1))) = complement(join(sFlat1,complement(X1))),
inference(step,[status(thm)],[t594,t23]) ).
cnf(t1222,plain,
meet(X1,join(complement(sFlat0),complement(sk1))) = complement(join(sFlat1,complement(X1))),
inference(orient,[status(thm)],[t123465]) ).
cnf(t1412,plain,
join(complement(sFlat0),complement(sk1)) = join(zero,complement(join(sFlat1,complement(join(complement(sFlat0),complement(sk1)))))),
inference(cp,[status(thm)],[t1411,t1222]) ).
cnf(t123513,plain,
join(complement(sFlat0),complement(sk1)) = join(zero,complement(join(sFlat1,meet(sFlat0,sk1)))),
inference(step,[status(thm)],[t1412,t68]) ).
cnf(t123514,plain,
join(complement(sFlat0),complement(sk1)) = join(zero,complement(join(sFlat1,sFlat1))),
inference(step,[status(thm)],[t123513,t89]) ).
cnf(t1234,plain,
meet(sFlat0,sk1) = join(sFlat1,meet(sFlat0,sk1)),
inference(cp,[status(thm)],[t1233,t89]) ).
cnf(t123479,plain,
sFlat1 = join(sFlat1,meet(sFlat0,sk1)),
inference(step,[status(thm)],[t1234,t89]) ).
cnf(t123480,plain,
sFlat1 = join(sFlat1,sFlat1),
inference(step,[status(thm)],[t123479,t89]) ).
cnf(t1238,plain,
join(sFlat1,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t123480]) ).
cnf(t123515,plain,
join(complement(sFlat0),complement(sk1)) = join(zero,complement(sFlat1)),
inference(step,[status(thm)],[t123514,t1238]) ).
cnf(t1464,plain,
join(complement(sFlat0),complement(sk1)) = join(zero,complement(sFlat1)),
inference(orient,[status(thm)],[t123515]) ).
cnf(t1467,plain,
top = join(sFlat0,join(zero,complement(sFlat1))),
inference(cp,[status(thm)],[t853,t1464]) ).
cnf(t1592,plain,
join(sFlat0,join(zero,complement(sFlat1))) = top,
inference(orient,[status(thm)],[t1467]) ).
cnf(t123580,plain,
join(sFlat0,complement(sFlat1)) = top,
inference(step,[status(thm)],[t1592,t1952]) ).
cnf(t1965,plain,
join(sFlat0,complement(sFlat1)) = top,
inference(rw,[status(thm)],[t123580]) ).
cnf(t1966,plain,
join(sFlat0,complement(sFlat1)) = top,
inference(orient,[status(thm)],[t1965]) ).
cnf(t2181,plain,
meet(sFlat1,complement(sFlat0)) = complement(top),
inference(cp,[status(thm)],[t2177,t1966]) ).
cnf(t123637,plain,
meet(sFlat1,complement(sFlat0)) = zero,
inference(step,[status(thm)],[t2181,t90]) ).
cnf(t2212,plain,
meet(sFlat1,complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t123637]) ).
cnf(t2213,plain,
sFlat1 = join(zero,meet(sFlat1,complement(complement(sFlat0)))),
inference(cp,[status(thm)],[t1551,t2212]) ).
cnf(t123638,plain,
sFlat1 = meet(sFlat1,complement(complement(sFlat0))),
inference(step,[status(thm)],[t2213,t1971]) ).
cnf(t123639,plain,
sFlat1 = meet(sFlat1,sFlat0),
inference(step,[status(thm)],[t123638,t2041]) ).
cnf(t123640,plain,
sFlat1 = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t123639,t85]) ).
cnf(t2215,plain,
meet(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t123640]) ).
cnf(t127036,plain,
sFlat3 = sFlat1,
inference(step,[status(thm)],[t127035,t2215]) ).
cnf(t123127,plain,
sFlat3 = sFlat1,
inference(orient,[status(thm)],[t127036]) ).
cnf(t127037,plain,
composition(sFlat2,sk3) = sFlat1,
inference(step,[status(thm)],[t80,t123127]) ).
cnf(t123128,plain,
composition(sFlat2,sk3) = sFlat1,
inference(orient,[status(thm)],[t127037]) ).
cnf(goal_0,negated_conjecture,
meet(sk1,composition(sk2,sk3)) != composition(meet(sk1,sk2),sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(sk1,sFlat0) != composition(meet(sk1,sk2),sk3),
inference(rw,[status(thm)],[goal_0,t63]) ).
cnf(g0_1,plain,
meet(sFlat0,sk1) != composition(meet(sk1,sk2),sk3),
inference(rw,[status(thm)],[g0_0,t85]) ).
cnf(g0_2,plain,
sFlat1 != composition(meet(sk1,sk2),sk3),
inference(rw,[status(thm)],[g0_1,t89]) ).
cnf(g0_3,plain,
sFlat1 != composition(meet(sk2,sk1),sk3),
inference(rw,[status(thm)],[g0_2,t85]) ).
cnf(g0_4,plain,
sFlat1 != composition(sFlat2,sk3),
inference(rw,[status(thm)],[g0_3,t88]) ).
cnf(g0_5,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_4,t123128]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL033-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/10.37 % Computer : n020.cluster.edu
% 0.11/10.37 % Model : x86_64 x86_64
% 0.11/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.37 % Memory : 8046.5625MB
% 0.11/10.37 % OS : Linux 6.8.0-71-generic
% 0.11/10.37 % CPULimit : 300
% 0.11/10.37 % WCLimit : 300
% 0.11/10.37 % DateTime : Thu Sep 24 07:29:14 UTC 2026
% 0.11/10.37 % CPUTime :
% 0.11/10.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 244.11/41.58 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 244.11/41.58 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------