%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL040-3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:36:00 PM UTC 2026
% Result : Unsatisfiable 266.21s 34.99s
% Output : CNFRefutation 266.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 174
% Number of leaves : 22
% Syntax : Number of clauses : 773 ( 773 unt; 0 nHn; 290 RR)
% Number of literals : 773 ( 772 equ; 9 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 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 : 775 ( 164 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t114,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t63,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t116,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t114,t63]) ).
cnf(t288804,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t116,t114]) ).
cnf(t146,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t288804]) ).
cnf(t18,axiom,
sFlat1 = composition(sk1,sk3),
introduced(definition) ).
cnf(t58,plain,
composition(sk1,sk3) = sFlat1,
inference(orient,[status(thm)],[t18]) ).
cnf(t17,axiom,
sFlat0 = composition(sk1,sk2),
introduced(definition) ).
cnf(t53,plain,
composition(sk1,sk2) = sFlat0,
inference(orient,[status(thm)],[t17]) ).
cnf(t19,axiom,
sFlat2 = meet(composition(sk1,sk2),composition(sk1,sk3)),
introduced(definition) ).
cnf(t288799,plain,
sFlat2 = meet(sFlat0,composition(sk1,sk3)),
inference(step,[status(thm)],[t19,t53]) ).
cnf(t288800,plain,
sFlat2 = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t288799,t58]) ).
cnf(t126,plain,
meet(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t288800]) ).
cnf(t20,axiom,
sFlat3 = meet(sk2,sk3),
introduced(definition) ).
cnf(t127,plain,
meet(sk2,sk3) = sFlat3,
inference(orient,[status(thm)],[t20]) ).
cnf(t151,plain,
meet(sk2,sk3) = sFlat3,
inference(rw,[status(thm)],[t127]) ).
cnf(t288806,plain,
meet(sk3,sk2) = sFlat3,
inference(step,[status(thm)],[t151,t146]) ).
cnf(t155,plain,
meet(sk3,sk2) = sFlat3,
inference(orient,[status(thm)],[t288806]) ).
cnf(t21,axiom,
sFlat4 = composition(sk1,meet(sk2,sk3)),
introduced(definition) ).
cnf(t48,plain,
composition(sk1,meet(sk2,sk3)) = sFlat4,
inference(orient,[status(thm)],[t21]) ).
cnf(t288801,plain,
composition(sk1,sFlat3) = sFlat4,
inference(step,[status(thm)],[t48,t127]) ).
cnf(t128,plain,
composition(sk1,sFlat3) = sFlat4,
inference(rw,[status(thm)],[t288801]) ).
cnf(t129,plain,
composition(sk1,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t128]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t109,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t39,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t41,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t39,t26]) ).
cnf(t208,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t41]) ).
cnf(t212,plain,
converse(join(composition(converse(X1),X2),X3)) = join(composition(converse(X2),X1),converse(X3)),
inference(cp,[status(thm)],[t109,t208]) ).
cnf(t86608,plain,
converse(join(composition(converse(X1),X2),X3)) = join(composition(converse(X2),X1),converse(X3)),
inference(orient,[status(thm)],[t212]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t43,plain,
composition(join(X1,converse(X2)),converse(X3)) = join(composition(X1,converse(X3)),converse(composition(X3,X2))),
inference(cp,[status(thm)],[t29,t39]) ).
cnf(t7413,plain,
join(composition(X1,converse(X2)),converse(composition(X2,X3))) = composition(join(X1,converse(X3)),converse(X2)),
inference(orient,[status(thm)],[t43]) ).
cnf(t86616,plain,
join(composition(converse(converse(X1)),X2),converse(converse(composition(X1,X3)))) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(cp,[status(thm)],[t86608,t7413]) ).
cnf(t293225,plain,
join(composition(X1,X2),converse(converse(composition(X1,X3)))) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t86616,t26]) ).
cnf(t293226,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t293225,t26]) ).
cnf(t111,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t109,t26]) ).
cnf(t338,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t111]) ).
cnf(t348,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t39,t338]) ).
cnf(t181899,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t348]) ).
cnf(t293227,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(converse(converse(X1)),join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t293226,t181899]) ).
cnf(t293228,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t293227,t26]) ).
cnf(t293229,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t293228,t26]) ).
cnf(t237316,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t293229]) ).
cnf(t237531,plain,
composition(sk1,join(sFlat3,X1)) = join(sFlat4,composition(sk1,X1)),
inference(cp,[status(thm)],[t237316,t129]) ).
cnf(t237864,plain,
composition(sk1,join(sFlat3,X1)) = join(sFlat4,composition(sk1,X1)),
inference(orient,[status(thm)],[t237531]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t66,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t288797,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t63]) ).
cnf(t74,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t288797]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t209,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t208,t22]) ).
cnf(t288807,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t209,t26]) ).
cnf(t221,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t288807]) ).
cnf(t222,plain,
one = converse(one),
inference(cp,[status(thm)],[t221,t22]) ).
cnf(t231,plain,
converse(one) = one,
inference(orient,[status(thm)],[t222]) ).
cnf(t288808,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t221,t231]) ).
cnf(t241,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t288808]) ).
cnf(t242,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t241]) ).
cnf(t245,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t74,t242]) ).
cnf(t288810,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t245,t231]) ).
cnf(t288811,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t288810,t242]) ).
cnf(t271,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t288811]) ).
cnf(t272,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t271,t114]) ).
cnf(t288836,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t272,t114]) ).
cnf(t288837,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t288836,t114]) ).
cnf(t596,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t288837]) ).
cnf(t599,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t596,t146]) ).
cnf(t635,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t599]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t65,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t23]) ).
cnf(t289468,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t65,t63]) ).
cnf(t289469,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t289468,t114]) ).
cnf(t289470,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t289469,t63]) ).
cnf(t15525,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t289470]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t121,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t15526,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t15525,t121]) ).
cnf(t289584,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t15526,t114]) ).
cnf(t16182,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t289584]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t71,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t115,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t114,t71]) ).
cnf(t288802,plain,
zero = complement(top),
inference(step,[status(thm)],[t115,t121]) ).
cnf(t137,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t288802]) ).
cnf(t275,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t271,t137]) ).
cnf(t288812,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t275,t137]) ).
cnf(t288813,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t288812,t137]) ).
cnf(t282,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t288813]) ).
cnf(t283,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t66,t282]) ).
cnf(t301,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t283]) ).
cnf(t16187,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t301,t16182]) ).
cnf(t289586,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t16187,t16182]) ).
cnf(t16197,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t289586]) ).
cnf(t289591,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t16182,t16197]) ).
cnf(t16236,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t289591]) ).
cnf(t16266,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t16236]) ).
cnf(t16267,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t635,t16266]) ).
cnf(t289626,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t16267,t16266]) ).
cnf(t289627,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t289626,t16266]) ).
cnf(t16333,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t289627]) ).
cnf(t16337,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t66,t16333]) ).
cnf(t16384,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t16337]) ).
cnf(t16403,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t16384,t15525]) ).
cnf(t289629,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t16403,t15525]) ).
cnf(t289630,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t289629,t63]) ).
cnf(t16413,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t289630]) ).
cnf(t16417,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t16413,t146]) ).
cnf(t16473,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t16417]) ).
cnf(t16483,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t66,t16473]) ).
cnf(t26289,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t16483]) ).
cnf(t281,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t114,t271]) ).
cnf(t288,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t281]) ).
cnf(t299,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t114,t288]) ).
cnf(t1328,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t299]) ).
cnf(t289610,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1328,t16266]) ).
cnf(t16299,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t289610]) ).
cnf(t17826,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t16299]) ).
cnf(t289690,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t15525,t17826]) ).
cnf(t17911,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t289690]) ).
cnf(t51653,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t17911]) ).
cnf(t51817,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t26289,t51653]) ).
cnf(t52763,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t51817]) ).
cnf(t52828,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t52763,t146]) ).
cnf(t53580,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t52828]) ).
cnf(t140,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t114,t137]) ).
cnf(t175,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t140]) ).
cnf(t112,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t109,t26]) ).
cnf(t355,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t112]) ).
cnf(t73,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t66,t71]) ).
cnf(t448,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t73]) ).
cnf(t296,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t71,t288]) ).
cnf(t333,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t296]) ).
cnf(t452,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t448,t333]) ).
cnf(t454,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t448,t271]) ).
cnf(t288821,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t454,t71]) ).
cnf(t468,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t288821]) ).
cnf(t469,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t468,t114]) ).
cnf(t476,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t469]) ).
cnf(t288825,plain,
top = join(X1,top),
inference(step,[status(thm)],[t452,t476]) ).
cnf(t489,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t288825]) ).
cnf(t490,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t489,t63]) ).
cnf(t498,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t490]) ).
cnf(t340,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t338,t71]) ).
cnf(t374,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t340]) ).
cnf(t501,plain,
top = converse(top),
inference(cp,[status(thm)],[t498,t374]) ).
cnf(t507,plain,
converse(top) = top,
inference(orient,[status(thm)],[t501]) ).
cnf(t512,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t39,t507]) ).
cnf(t519,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t512]) ).
cnf(t525,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t355,t519]) ).
cnf(t12901,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t525]) ).
cnf(t42,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t29,t39]) ).
cnf(t6534,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t42]) ).
cnf(t12902,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t12901,t6534]) ).
cnf(t289382,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t12902,t26]) ).
cnf(t40,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t39,t26]) ).
cnf(t198,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t40]) ).
cnf(t289383,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t289382,t198]) ).
cnf(t289384,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t289383,t338]) ).
cnf(t289385,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t289384,t507]) ).
cnf(t289386,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t289385,t489]) ).
cnf(t12986,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t289386]) ).
cnf(t513,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t39,t507]) ).
cnf(t533,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t513]) ).
cnf(t521,plain,
converse(join(composition(X1,top),X2)) = join(composition(top,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t109,t519]) ).
cnf(t5750,plain,
join(composition(top,converse(X1)),converse(X2)) = converse(join(composition(X1,top),X2)),
inference(orient,[status(thm)],[t521]) ).
cnf(t5762,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(cp,[status(thm)],[t5750,t507]) ).
cnf(t5796,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(orient,[status(thm)],[t5762]) ).
cnf(t5800,plain,
join(composition(top,top),converse(composition(X1,top))) = converse(composition(join(top,X1),top)),
inference(cp,[status(thm)],[t5796,t29]) ).
cnf(t289112,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t5800,t519]) ).
cnf(t289113,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t289112,t519]) ).
cnf(t289114,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t289113,t498]) ).
cnf(t289115,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t289114,t507]) ).
cnf(t5932,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t289115]) ).
cnf(t5948,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t5932,t231]) ).
cnf(t289116,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t5948,t22]) ).
cnf(t289117,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t289116,t489]) ).
cnf(t5961,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t289117]) ).
cnf(t5966,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t74,t5961]) ).
cnf(t289125,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t5966,t137]) ).
cnf(t289126,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t289125,t137]) ).
cnf(t289127,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t289126,t507]) ).
cnf(t289128,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t289127,t137]) ).
cnf(t16,axiom,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t32,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t16]) ).
cnf(t33,plain,
composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t32,t22]) ).
cnf(t288873,plain,
composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t33,t231]) ).
cnf(t288874,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t288873,t22]) ).
cnf(t288875,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t288874,t231]) ).
cnf(t288876,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t288875,t22]) ).
cnf(t1499,plain,
join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))) = composition(meet(X1,X2),meet(one,composition(converse(X1),X2))),
inference(orient,[status(thm)],[t288876]) ).
cnf(t113,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t66,t109]) ).
cnf(t2787,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t113]) ).
cnf(t457,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t448,t63]) ).
cnf(t288834,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t457,t498]) ).
cnf(t557,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t288834]) ).
cnf(t2791,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t2787,t557]) ).
cnf(t289006,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t2791,t63]) ).
cnf(t2841,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t289006]) ).
cnf(t2887,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t2841,t109]) ).
cnf(t289007,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t2887,t26]) ).
cnf(t289008,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t289007,t26]) ).
cnf(t2901,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t289008]) ).
cnf(t2939,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t2901,t63]) ).
cnf(t2944,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t2939]) ).
cnf(t76,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t74,t22]) ).
cnf(t1401,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t76]) ).
cnf(t1406,plain,
complement(one) = join(complement(one),composition(top,complement(top))),
inference(cp,[status(thm)],[t1401,t507]) ).
cnf(t288870,plain,
complement(one) = join(complement(one),composition(top,zero)),
inference(step,[status(thm)],[t1406,t137]) ).
cnf(t1426,plain,
join(complement(one),composition(top,zero)) = complement(one),
inference(orient,[status(thm)],[t288870]) ).
cnf(t2959,plain,
top = join(complement(composition(top,zero)),complement(one)),
inference(cp,[status(thm)],[t2944,t1426]) ).
cnf(t289009,plain,
top = join(complement(one),complement(composition(top,zero))),
inference(step,[status(thm)],[t2959,t63]) ).
cnf(t3022,plain,
join(complement(one),complement(composition(top,zero))) = top,
inference(orient,[status(thm)],[t289009]) ).
cnf(t3027,plain,
meet(one,composition(top,zero)) = complement(top),
inference(cp,[status(thm)],[t114,t3022]) ).
cnf(t289010,plain,
meet(one,composition(top,zero)) = zero,
inference(step,[status(thm)],[t3027,t137]) ).
cnf(t3030,plain,
meet(one,composition(top,zero)) = zero,
inference(orient,[status(thm)],[t289010]) ).
cnf(t3036,plain,
composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(cp,[status(thm)],[t1499,t3030]) ).
cnf(t289011,plain,
composition(zero,meet(one,composition(converse(one),composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t3036,t3030]) ).
cnf(t289012,plain,
composition(zero,meet(one,composition(one,composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t289011,t231]) ).
cnf(t289013,plain,
composition(zero,meet(one,composition(top,zero))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t289012,t242]) ).
cnf(t289014,plain,
composition(zero,zero) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t289013,t3030]) ).
cnf(t289015,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t289014,t3030]) ).
cnf(t289016,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(one,composition(top,zero))))),
inference(step,[status(thm)],[t289015,t231]) ).
cnf(t289017,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(top,zero)))),
inference(step,[status(thm)],[t289016,t242]) ).
cnf(t289018,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t289017,t3030]) ).
cnf(t3038,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t289018]) ).
cnf(t3041,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(cp,[status(thm)],[t66,t3038]) ).
cnf(t3667,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(orient,[status(thm)],[t3041]) ).
cnf(t3675,plain,
join(composition(zero,zero),composition(X1,zero)) = join(zero,composition(join(zero,X1),zero)),
inference(cp,[status(thm)],[t3667,t29]) ).
cnf(t289036,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(zero,X1),zero)),
inference(step,[status(thm)],[t3675,t29]) ).
cnf(t3746,plain,
join(zero,composition(join(zero,X1),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t289036]) ).
cnf(t72,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t71,t66]) ).
cnf(t651,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t72]) ).
cnf(t673,plain,
top = join(X1,join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t651,t63]) ).
cnf(t800,plain,
join(X1,join(X2,complement(join(X2,X1)))) = top,
inference(orient,[status(thm)],[t673]) ).
cnf(t812,plain,
top = join(complement(X1),join(X1,complement(top))),
inference(cp,[status(thm)],[t800,t71]) ).
cnf(t288849,plain,
top = join(complement(X1),join(X1,zero)),
inference(step,[status(thm)],[t812,t137]) ).
cnf(t839,plain,
join(complement(X1),join(X1,zero)) = top,
inference(orient,[status(thm)],[t288849]) ).
cnf(t846,plain,
top = join(complement(X1),join(zero,X1)),
inference(cp,[status(thm)],[t839,t63]) ).
cnf(t848,plain,
join(complement(X1),join(zero,X1)) = top,
inference(orient,[status(thm)],[t846]) ).
cnf(t142,plain,
complement(top) = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(cp,[status(thm)],[t74,t137]) ).
cnf(t288910,plain,
zero = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(step,[status(thm)],[t142,t137]) ).
cnf(t2134,plain,
join(zero,composition(converse(X1),complement(composition(X1,top)))) = zero,
inference(orient,[status(thm)],[t288910]) ).
cnf(t2139,plain,
zero = join(zero,composition(top,complement(composition(top,top)))),
inference(cp,[status(thm)],[t2134,t507]) ).
cnf(t2156,plain,
join(zero,composition(top,complement(composition(top,top)))) = zero,
inference(orient,[status(thm)],[t2139]) ).
cnf(t2158,plain,
top = join(complement(composition(top,complement(composition(top,top)))),zero),
inference(cp,[status(thm)],[t848,t2156]) ).
cnf(t288957,plain,
top = join(zero,complement(composition(top,complement(composition(top,top))))),
inference(step,[status(thm)],[t2158,t63]) ).
cnf(t2482,plain,
join(zero,complement(composition(top,complement(composition(top,top))))) = top,
inference(orient,[status(thm)],[t288957]) ).
cnf(t3749,plain,
composition(join(zero,complement(composition(top,complement(composition(top,top))))),zero) = join(zero,composition(top,zero)),
inference(cp,[status(thm)],[t3746,t2482]) ).
cnf(t289037,plain,
composition(top,zero) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t3749,t2482]) ).
cnf(t3775,plain,
join(zero,composition(top,zero)) = composition(top,zero),
inference(orient,[status(thm)],[t289037]) ).
cnf(t289129,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t289128,t3775]) ).
cnf(t5981,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t289129]) ).
cnf(t5982,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t533,t5981]) ).
cnf(t6005,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t5982]) ).
cnf(t13057,plain,
composition(converse(zero),top) = join(composition(converse(zero),X1),converse(zero)),
inference(cp,[status(thm)],[t12986,t6005]) ).
cnf(t289441,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t13057,t6005]) ).
cnf(t289442,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t289441,t63]) ).
cnf(t14692,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t289442]) ).
cnf(t3765,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(X1,zero),zero)),
inference(cp,[status(thm)],[t3746,t63]) ).
cnf(t3826,plain,
join(zero,composition(join(X1,zero),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t3765]) ).
cnf(t5983,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t29,t5981]) ).
cnf(t289135,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t5983,t498]) ).
cnf(t289136,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t289135,t5981]) ).
cnf(t6033,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t289136]) ).
cnf(t289139,plain,
zero = composition(join(zero,X1),zero),
inference(step,[status(thm)],[t3826,t6033]) ).
cnf(t6051,plain,
zero = composition(join(zero,X1),zero),
inference(rw,[status(thm)],[t289139]) ).
cnf(t6097,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t6051]) ).
cnf(t6100,plain,
zero = composition(join(X1,zero),zero),
inference(cp,[status(thm)],[t6097,t63]) ).
cnf(t6121,plain,
composition(join(X1,zero),zero) = zero,
inference(orient,[status(thm)],[t6100]) ).
cnf(t6123,plain,
composition(join(join(X1,zero),X2),zero) = join(zero,composition(X2,zero)),
inference(cp,[status(thm)],[t29,t6121]) ).
cnf(t289161,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t6123,t66]) ).
cnf(t289162,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t289161,t6033]) ).
cnf(t6340,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t289162]) ).
cnf(t232,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t109,t231]) ).
cnf(t248,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t232]) ).
cnf(t254,plain,
composition(converse(X1),join(one,X2)) = converse(composition(join(one,converse(X2)),X1)),
inference(cp,[status(thm)],[t208,t248]) ).
cnf(t5484,plain,
converse(composition(join(one,converse(X1)),X2)) = composition(converse(X2),join(one,X1)),
inference(orient,[status(thm)],[t254]) ).
cnf(t9,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t31,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t29,t27]) ).
cnf(t717,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t31]) ).
cnf(t5964,plain,
composition(join(X1,composition(X2,top)),top) = join(composition(X1,top),composition(X2,top)),
inference(cp,[status(thm)],[t717,t5961]) ).
cnf(t289242,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(step,[status(thm)],[t5964,t29]) ).
cnf(t8020,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(orient,[status(thm)],[t289242]) ).
cnf(t8035,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t8020,t242]) ).
cnf(t289243,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t8035,t489]) ).
cnf(t289244,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t289243,t5961]) ).
cnf(t8061,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t289244]) ).
cnf(t8063,plain,
top = composition(join(one,X1),top),
inference(cp,[status(thm)],[t8061,t63]) ).
cnf(t8087,plain,
composition(join(one,X1),top) = top,
inference(orient,[status(thm)],[t8063]) ).
cnf(t8099,plain,
composition(converse(top),join(one,X1)) = converse(top),
inference(cp,[status(thm)],[t5484,t8087]) ).
cnf(t289247,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t8099,t507]) ).
cnf(t289248,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t289247,t507]) ).
cnf(t8127,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t289248]) ).
cnf(t8128,plain,
top = composition(top,join(X1,one)),
inference(cp,[status(thm)],[t8127,t63]) ).
cnf(t8145,plain,
composition(top,join(X1,one)) = top,
inference(orient,[status(thm)],[t8128]) ).
cnf(t8152,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t74,t8145]) ).
cnf(t289271,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t8152,t507]) ).
cnf(t289272,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t289271,t63]) ).
cnf(t289273,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t289272,t137]) ).
cnf(t289274,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t289273,t5981]) ).
cnf(t9006,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t289274]) ).
cnf(t9015,plain,
zero = composition(join(X1,complement(join(X2,one))),zero),
inference(cp,[status(thm)],[t6340,t9006]) ).
cnf(t9744,plain,
composition(join(X1,complement(join(X2,one))),zero) = zero,
inference(orient,[status(thm)],[t9015]) ).
cnf(t15751,plain,
zero = composition(X1,zero),
inference(cp,[status(thm)],[t9744,t15525]) ).
cnf(t15756,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t15751]) ).
cnf(t15766,plain,
converse(zero) = join(converse(zero),zero),
inference(cp,[status(thm)],[t14692,t15756]) ).
cnf(t289512,plain,
converse(zero) = join(zero,converse(zero)),
inference(step,[status(thm)],[t15766,t63]) ).
cnf(t15920,plain,
join(zero,converse(zero)) = converse(zero),
inference(orient,[status(thm)],[t289512]) ).
cnf(t15927,plain,
join(converse(zero),zero) = converse(converse(zero)),
inference(cp,[status(thm)],[t355,t15920]) ).
cnf(t289513,plain,
join(zero,converse(zero)) = converse(converse(zero)),
inference(step,[status(thm)],[t15927,t63]) ).
cnf(t289514,plain,
converse(zero) = converse(converse(zero)),
inference(step,[status(thm)],[t289513,t15920]) ).
cnf(t289515,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t289514,t26]) ).
cnf(t15930,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t289515]) ).
cnf(t15933,plain,
converse(composition(X1,zero)) = composition(zero,converse(X1)),
inference(cp,[status(thm)],[t39,t15930]) ).
cnf(t289555,plain,
converse(zero) = composition(zero,converse(X1)),
inference(step,[status(thm)],[t15933,t15756]) ).
cnf(t289556,plain,
zero = composition(zero,converse(X1)),
inference(step,[status(thm)],[t289555,t15930]) ).
cnf(t16017,plain,
composition(zero,converse(X1)) = zero,
inference(orient,[status(thm)],[t289556]) ).
cnf(t16034,plain,
zero = composition(zero,X1),
inference(cp,[status(thm)],[t16017,t26]) ).
cnf(t16055,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t16034]) ).
cnf(t16066,plain,
complement(X1) = join(complement(X1),composition(converse(zero),complement(zero))),
inference(cp,[status(thm)],[t74,t16055]) ).
cnf(t289557,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t16066,t15930]) ).
cnf(t289558,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t289557,t16055]) ).
cnf(t289559,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t289558,t63]) ).
cnf(t16068,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t289559]) ).
cnf(t289572,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t175,t16068]) ).
cnf(t16109,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t289572]) ).
cnf(t16110,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t16109]) ).
cnf(t16203,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t16197,t63]) ).
cnf(t16248,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t16203]) ).
cnf(t16257,plain,
X1 = join(meet(X1,zero),complement(complement(X1))),
inference(cp,[status(thm)],[t15525,t16248]) ).
cnf(t3017,plain,
join(complement(X1),join(join(X2,X1),X3)) = join(top,X3),
inference(cp,[status(thm)],[t66,t2944]) ).
cnf(t289024,plain,
join(complement(X1),join(X2,join(X1,X3))) = join(top,X3),
inference(step,[status(thm)],[t3017,t66]) ).
cnf(t289025,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(step,[status(thm)],[t289024,t498]) ).
cnf(t3363,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(orient,[status(thm)],[t289025]) ).
cnf(t9016,plain,
top = join(complement(zero),join(X1,complement(join(X2,one)))),
inference(cp,[status(thm)],[t3363,t9006]) ).
cnf(t12044,plain,
join(complement(zero),join(X1,complement(join(X2,one)))) = top,
inference(orient,[status(thm)],[t9016]) ).
cnf(t15750,plain,
top = join(complement(zero),X1),
inference(cp,[status(thm)],[t12044,t15525]) ).
cnf(t15817,plain,
join(complement(zero),X1) = top,
inference(orient,[status(thm)],[t15750]) ).
cnf(t15818,plain,
top = complement(zero),
inference(cp,[status(thm)],[t15817,t74]) ).
cnf(t15862,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t15818]) ).
cnf(t15884,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t114,t15862]) ).
cnf(t289509,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t15884,t489]) ).
cnf(t289510,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t289509,t137]) ).
cnf(t15909,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t289510]) ).
cnf(t289613,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t16257,t15909]) ).
cnf(t289614,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t289613,t16068]) ).
cnf(t289615,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t289614,t16110]) ).
cnf(t16302,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t289615]) ).
cnf(t289616,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t16110,t16302]) ).
cnf(t16303,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t289616]) ).
cnf(t17880,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t17826,t16303]) ).
cnf(t18721,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t17880]) ).
cnf(t53605,plain,
join(X1,complement(X2)) = join(X1,complement(join(X1,X2))),
inference(cp,[status(thm)],[t53580,t18721]) ).
cnf(t55946,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t53605]) ).
cnf(t597,plain,
meet(sk3,sk2) = join(sFlat3,meet(sk3,sk2)),
inference(cp,[status(thm)],[t596,t155]) ).
cnf(t288838,plain,
sFlat3 = join(sFlat3,meet(sk3,sk2)),
inference(step,[status(thm)],[t597,t155]) ).
cnf(t288839,plain,
sFlat3 = join(sFlat3,sFlat3),
inference(step,[status(thm)],[t288838,t155]) ).
cnf(t606,plain,
join(sFlat3,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t288839]) ).
cnf(t607,plain,
join(sFlat3,join(sFlat3,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t66,t606]) ).
cnf(t610,plain,
join(sFlat3,join(sFlat3,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t607]) ).
cnf(t611,plain,
join(sFlat3,X1) = join(sFlat3,join(X1,sFlat3)),
inference(cp,[status(thm)],[t610,t63]) ).
cnf(t614,plain,
join(sFlat3,join(X1,sFlat3)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t611]) ).
cnf(t616,plain,
join(sFlat3,join(join(X1,sFlat3),X2)) = join(join(sFlat3,X1),X2),
inference(cp,[status(thm)],[t66,t614]) ).
cnf(t288897,plain,
join(sFlat3,join(X1,join(sFlat3,X2))) = join(join(sFlat3,X1),X2),
inference(step,[status(thm)],[t616,t66]) ).
cnf(t288898,plain,
join(sFlat3,join(X1,join(sFlat3,X2))) = join(sFlat3,join(X1,X2)),
inference(step,[status(thm)],[t288897,t66]) ).
cnf(t1793,plain,
join(sFlat3,join(X1,join(sFlat3,X2))) = join(sFlat3,join(X1,X2)),
inference(orient,[status(thm)],[t288898]) ).
cnf(t117,plain,
top = join(join(complement(X1),complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t71,t114]) ).
cnf(t288904,plain,
top = join(complement(X1),join(complement(X2),meet(X1,X2))),
inference(step,[status(thm)],[t117,t66]) ).
cnf(t1970,plain,
join(complement(X1),join(complement(X2),meet(X1,X2))) = top,
inference(orient,[status(thm)],[t288904]) ).
cnf(t1989,plain,
top = join(complement(sk3),join(complement(sk2),sFlat3)),
inference(cp,[status(thm)],[t1970,t155]) ).
cnf(t288905,plain,
top = join(complement(sk3),join(sFlat3,complement(sk2))),
inference(step,[status(thm)],[t1989,t63]) ).
cnf(t1995,plain,
join(complement(sk3),join(sFlat3,complement(sk2))) = top,
inference(orient,[status(thm)],[t288905]) ).
cnf(t1997,plain,
join(sFlat3,join(complement(sk3),complement(sk2))) = join(sFlat3,top),
inference(cp,[status(thm)],[t1793,t1995]) ).
cnf(t479,plain,
top = join(top,sFlat3),
inference(cp,[status(thm)],[t476,t155]) ).
cnf(t288823,plain,
top = join(sFlat3,top),
inference(step,[status(thm)],[t479,t63]) ).
cnf(t483,plain,
join(sFlat3,top) = top,
inference(orient,[status(thm)],[t288823]) ).
cnf(t288907,plain,
join(sFlat3,join(complement(sk3),complement(sk2))) = top,
inference(step,[status(thm)],[t1997,t483]) ).
cnf(t2005,plain,
join(sFlat3,join(complement(sk3),complement(sk2))) = top,
inference(orient,[status(thm)],[t288907]) ).
cnf(t2006,plain,
join(sFlat3,join(join(complement(sk3),complement(sk2)),X1)) = join(top,X1),
inference(cp,[status(thm)],[t66,t2005]) ).
cnf(t288945,plain,
join(sFlat3,join(complement(sk3),join(complement(sk2),X1))) = join(top,X1),
inference(step,[status(thm)],[t2006,t66]) ).
cnf(t288946,plain,
join(sFlat3,join(complement(sk3),join(complement(sk2),X1))) = top,
inference(step,[status(thm)],[t288945,t498]) ).
cnf(t2397,plain,
join(sFlat3,join(complement(sk3),join(complement(sk2),X1))) = top,
inference(orient,[status(thm)],[t288946]) ).
cnf(t2398,plain,
top = join(sFlat3,join(complement(sk3),join(X1,complement(sk2)))),
inference(cp,[status(thm)],[t2397,t63]) ).
cnf(t2641,plain,
join(sFlat3,join(complement(sk3),join(X1,complement(sk2)))) = top,
inference(orient,[status(thm)],[t2398]) ).
cnf(t177,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t175,t114]) ).
cnf(t4980,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t177]) ).
cnf(t289587,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t4980,t16197]) ).
cnf(t16198,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t289587]) ).
cnf(t289622,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t16198,t16302]) ).
cnf(t16330,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t289622]) ).
cnf(t18611,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t16330]) ).
cnf(t18632,plain,
top = join(sFlat3,join(complement(sk3),complement(meet(X1,sk2)))),
inference(cp,[status(thm)],[t2641,t18611]) ).
cnf(t290403,plain,
top = join(sFlat3,complement(meet(sk3,meet(X1,sk2)))),
inference(step,[status(thm)],[t18632,t18611]) ).
cnf(t66236,plain,
join(sFlat3,complement(meet(sk3,meet(X1,sk2)))) = top,
inference(orient,[status(thm)],[t290403]) ).
cnf(t66244,plain,
join(sFlat3,complement(complement(meet(sk3,meet(X1,sk2))))) = join(sFlat3,complement(top)),
inference(cp,[status(thm)],[t55946,t66236]) ).
cnf(t290404,plain,
join(sFlat3,meet(sk3,meet(X1,sk2))) = join(sFlat3,complement(top)),
inference(step,[status(thm)],[t66244,t16303]) ).
cnf(t290405,plain,
join(sFlat3,meet(sk3,meet(X1,sk2))) = join(sFlat3,zero),
inference(step,[status(thm)],[t290404,t137]) ).
cnf(t290406,plain,
join(sFlat3,meet(sk3,meet(X1,sk2))) = sFlat3,
inference(step,[status(thm)],[t290405,t16248]) ).
cnf(t66252,plain,
join(sFlat3,meet(sk3,meet(X1,sk2))) = sFlat3,
inference(orient,[status(thm)],[t290406]) ).
cnf(t66253,plain,
sFlat3 = join(sFlat3,meet(sk3,meet(sk2,X1))),
inference(cp,[status(thm)],[t66252,t146]) ).
cnf(t66281,plain,
join(sFlat3,meet(sk3,meet(sk2,X1))) = sFlat3,
inference(orient,[status(thm)],[t66253]) ).
cnf(t51776,plain,
X1 = join(meet(X2,X1),meet(X1,complement(X2))),
inference(cp,[status(thm)],[t51653,t146]) ).
cnf(t89348,plain,
join(meet(X1,X2),meet(X2,complement(X1))) = X2,
inference(orient,[status(thm)],[t51776]) ).
cnf(t89920,plain,
X1 = join(meet(X2,X1),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t89348,t146]) ).
cnf(t104335,plain,
join(meet(X1,X2),meet(complement(X1),X2)) = X2,
inference(orient,[status(thm)],[t89920]) ).
cnf(t38,plain,
composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(converse(converse(X1)),X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))),
inference(cp,[status(thm)],[t32,t26]) ).
cnf(t289107,plain,
composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))),
inference(step,[status(thm)],[t38,t26]) ).
cnf(t4856,plain,
join(meet(composition(converse(X1),X2),X3),composition(meet(converse(X1),composition(X3,converse(X2))),meet(X2,composition(X1,X3)))) = composition(meet(converse(X1),composition(X3,converse(X2))),meet(X2,composition(X1,X3))),
inference(orient,[status(thm)],[t289107]) ).
cnf(t17871,plain,
meet(X1,complement(join(X2,complement(complement(X1))))) = complement(top),
inference(cp,[status(thm)],[t17826,t557]) ).
cnf(t289701,plain,
meet(X1,complement(join(X2,X1))) = complement(top),
inference(step,[status(thm)],[t17871,t16303]) ).
cnf(t289702,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(step,[status(thm)],[t289701,t137]) ).
cnf(t17982,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t289702]) ).
cnf(t17986,plain,
zero = meet(meet(X1,X2),complement(X2)),
inference(cp,[status(thm)],[t17982,t16473]) ).
cnf(t289705,plain,
zero = meet(complement(X2),meet(X1,X2)),
inference(step,[status(thm)],[t17986,t146]) ).
cnf(t18255,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t289705]) ).
cnf(t18728,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t16473,t18721]) ).
cnf(t289774,plain,
complement(X1) = complement(meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t18728,t18611]) ).
cnf(t18979,plain,
complement(meet(X1,join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t289774]) ).
cnf(t19045,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t16303,t18979]) ).
cnf(t289779,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t19045,t16303]) ).
cnf(t19169,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t289779]) ).
cnf(t19226,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t19169,t63]) ).
cnf(t19250,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t19226]) ).
cnf(t67,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t66,t63]) ).
cnf(t16970,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t67]) ).
cnf(t19313,plain,
X1 = meet(X1,join(X2,join(X1,X3))),
inference(cp,[status(thm)],[t19250,t16970]) ).
cnf(t21081,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t19313]) ).
cnf(t26478,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(cp,[status(thm)],[t21081,t26289]) ).
cnf(t34571,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t26478]) ).
cnf(t34897,plain,
zero = meet(complement(join(X1,X2)),meet(X3,X1)),
inference(cp,[status(thm)],[t18255,t34571]) ).
cnf(t79520,plain,
meet(complement(join(X1,X2)),meet(X3,X1)) = zero,
inference(orient,[status(thm)],[t34897]) ).
cnf(t79636,plain,
zero = meet(complement(complement(meet(X1,X2))),meet(X3,complement(X1))),
inference(cp,[status(thm)],[t79520,t18611]) ).
cnf(t291044,plain,
zero = meet(meet(X1,X2),meet(X3,complement(X1))),
inference(step,[status(thm)],[t79636,t16303]) ).
cnf(t103469,plain,
meet(meet(X1,X2),meet(X3,complement(X1))) = zero,
inference(orient,[status(thm)],[t291044]) ).
cnf(t51784,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t51653,t146]) ).
cnf(t89978,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t51784]) ).
cnf(t243,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t29,t242]) ).
cnf(t105047,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t243]) ).
cnf(t5,axiom,
join(composition(converse(sk1),sk1),one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t288798,plain,
join(one,composition(converse(sk1),sk1)) = one,
inference(step,[status(thm)],[t5,t63]) ).
cnf(t83,plain,
join(one,composition(converse(sk1),sk1)) = one,
inference(orient,[status(thm)],[t288798]) ).
cnf(t105065,plain,
join(X1,composition(composition(converse(sk1),sk1),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t105047,t83]) ).
cnf(t291113,plain,
join(X1,composition(converse(sk1),composition(sk1,X1))) = composition(one,X1),
inference(step,[status(thm)],[t105065,t27]) ).
cnf(t291114,plain,
join(X1,composition(converse(sk1),composition(sk1,X1))) = X1,
inference(step,[status(thm)],[t291113,t242]) ).
cnf(t109373,plain,
join(X1,composition(converse(sk1),composition(sk1,X1))) = X1,
inference(orient,[status(thm)],[t291114]) ).
cnf(t109380,plain,
sk2 = join(sk2,composition(converse(sk1),sFlat0)),
inference(cp,[status(thm)],[t109373,t53]) ).
cnf(t109571,plain,
join(sk2,composition(converse(sk1),sFlat0)) = sk2,
inference(orient,[status(thm)],[t109380]) ).
cnf(t109599,plain,
zero = meet(composition(converse(sk1),sFlat0),complement(sk2)),
inference(cp,[status(thm)],[t17982,t109571]) ).
cnf(t291140,plain,
zero = meet(complement(sk2),composition(converse(sk1),sFlat0)),
inference(step,[status(thm)],[t109599,t146]) ).
cnf(t109831,plain,
meet(complement(sk2),composition(converse(sk1),sFlat0)) = zero,
inference(orient,[status(thm)],[t291140]) ).
cnf(t109845,plain,
composition(meet(sk1,composition(sFlat0,converse(complement(sk2)))),meet(complement(sk2),composition(converse(sk1),sFlat0))) = join(meet(composition(sk1,complement(sk2)),sFlat0),composition(meet(sk1,composition(sFlat0,converse(complement(sk2)))),zero)),
inference(cp,[status(thm)],[t32,t109831]) ).
cnf(t291141,plain,
composition(meet(sk1,composition(sFlat0,converse(complement(sk2)))),zero) = join(meet(composition(sk1,complement(sk2)),sFlat0),composition(meet(sk1,composition(sFlat0,converse(complement(sk2)))),zero)),
inference(step,[status(thm)],[t109845,t109831]) ).
cnf(t291142,plain,
zero = join(meet(composition(sk1,complement(sk2)),sFlat0),composition(meet(sk1,composition(sFlat0,converse(complement(sk2)))),zero)),
inference(step,[status(thm)],[t291141,t15756]) ).
cnf(t291143,plain,
zero = join(meet(sFlat0,composition(sk1,complement(sk2))),composition(meet(sk1,composition(sFlat0,converse(complement(sk2)))),zero)),
inference(step,[status(thm)],[t291142,t146]) ).
cnf(t291144,plain,
zero = join(meet(sFlat0,composition(sk1,complement(sk2))),zero),
inference(step,[status(thm)],[t291143,t15756]) ).
cnf(t291145,plain,
zero = meet(sFlat0,composition(sk1,complement(sk2))),
inference(step,[status(thm)],[t291144,t16248]) ).
cnf(t109852,plain,
meet(sFlat0,composition(sk1,complement(sk2))) = zero,
inference(orient,[status(thm)],[t291145]) ).
cnf(t109858,plain,
sFlat0 = join(zero,meet(complement(composition(sk1,complement(sk2))),sFlat0)),
inference(cp,[status(thm)],[t89978,t109852]) ).
cnf(t291176,plain,
sFlat0 = meet(complement(composition(sk1,complement(sk2))),sFlat0),
inference(step,[status(thm)],[t109858,t16197]) ).
cnf(t291177,plain,
sFlat0 = meet(sFlat0,complement(composition(sk1,complement(sk2)))),
inference(step,[status(thm)],[t291176,t146]) ).
cnf(t110166,plain,
meet(sFlat0,complement(composition(sk1,complement(sk2)))) = sFlat0,
inference(orient,[status(thm)],[t291177]) ).
cnf(t110199,plain,
zero = meet(meet(composition(sk1,complement(sk2)),X1),sFlat0),
inference(cp,[status(thm)],[t103469,t110166]) ).
cnf(t291373,plain,
zero = meet(sFlat0,meet(composition(sk1,complement(sk2)),X1)),
inference(step,[status(thm)],[t110199,t146]) ).
cnf(t117976,plain,
meet(sFlat0,meet(composition(sk1,complement(sk2)),X1)) = zero,
inference(orient,[status(thm)],[t291373]) ).
cnf(t16416,plain,
sFlat0 = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t16413,t126]) ).
cnf(t16456,plain,
join(sFlat0,sFlat2) = sFlat0,
inference(orient,[status(thm)],[t16416]) ).
cnf(t16459,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat0,X1),
inference(cp,[status(thm)],[t66,t16456]) ).
cnf(t16709,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat0,X1),
inference(orient,[status(thm)],[t16459]) ).
cnf(t16716,plain,
join(sFlat0,meet(X1,sFlat2)) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t16709,t16473]) ).
cnf(t289641,plain,
join(sFlat0,meet(X1,sFlat2)) = sFlat0,
inference(step,[status(thm)],[t16716,t16456]) ).
cnf(t16746,plain,
join(sFlat0,meet(X1,sFlat2)) = sFlat0,
inference(orient,[status(thm)],[t289641]) ).
cnf(t19189,plain,
meet(X1,sFlat2) = meet(meet(X1,sFlat2),sFlat0),
inference(cp,[status(thm)],[t19169,t16746]) ).
cnf(t289783,plain,
meet(X1,sFlat2) = meet(sFlat0,meet(X1,sFlat2)),
inference(step,[status(thm)],[t19189,t146]) ).
cnf(t19744,plain,
meet(sFlat0,meet(X1,sFlat2)) = meet(X1,sFlat2),
inference(orient,[status(thm)],[t289783]) ).
cnf(t117977,plain,
zero = meet(composition(sk1,complement(sk2)),sFlat2),
inference(cp,[status(thm)],[t117976,t19744]) ).
cnf(t291374,plain,
zero = meet(sFlat2,composition(sk1,complement(sk2))),
inference(step,[status(thm)],[t117977,t146]) ).
cnf(t117995,plain,
meet(sFlat2,composition(sk1,complement(sk2))) = zero,
inference(orient,[status(thm)],[t291374]) ).
cnf(t118012,plain,
composition(meet(converse(sk1),composition(complement(sk2),converse(sFlat2))),meet(sFlat2,composition(sk1,complement(sk2)))) = join(meet(composition(converse(sk1),sFlat2),complement(sk2)),composition(meet(converse(sk1),composition(complement(sk2),converse(sFlat2))),zero)),
inference(cp,[status(thm)],[t4856,t117995]) ).
cnf(t291377,plain,
composition(meet(converse(sk1),composition(complement(sk2),converse(sFlat2))),zero) = join(meet(composition(converse(sk1),sFlat2),complement(sk2)),composition(meet(converse(sk1),composition(complement(sk2),converse(sFlat2))),zero)),
inference(step,[status(thm)],[t118012,t117995]) ).
cnf(t291378,plain,
zero = join(meet(composition(converse(sk1),sFlat2),complement(sk2)),composition(meet(converse(sk1),composition(complement(sk2),converse(sFlat2))),zero)),
inference(step,[status(thm)],[t291377,t15756]) ).
cnf(t291379,plain,
zero = join(meet(complement(sk2),composition(converse(sk1),sFlat2)),composition(meet(converse(sk1),composition(complement(sk2),converse(sFlat2))),zero)),
inference(step,[status(thm)],[t291378,t146]) ).
cnf(t291380,plain,
zero = join(meet(complement(sk2),composition(converse(sk1),sFlat2)),zero),
inference(step,[status(thm)],[t291379,t15756]) ).
cnf(t291381,plain,
zero = meet(complement(sk2),composition(converse(sk1),sFlat2)),
inference(step,[status(thm)],[t291380,t16248]) ).
cnf(t118137,plain,
meet(complement(sk2),composition(converse(sk1),sFlat2)) = zero,
inference(orient,[status(thm)],[t291381]) ).
cnf(t118142,plain,
composition(converse(sk1),sFlat2) = join(zero,meet(complement(complement(sk2)),composition(converse(sk1),sFlat2))),
inference(cp,[status(thm)],[t104335,t118137]) ).
cnf(t291391,plain,
composition(converse(sk1),sFlat2) = meet(complement(complement(sk2)),composition(converse(sk1),sFlat2)),
inference(step,[status(thm)],[t118142,t16197]) ).
cnf(t291392,plain,
composition(converse(sk1),sFlat2) = meet(sk2,composition(converse(sk1),sFlat2)),
inference(step,[status(thm)],[t291391,t16303]) ).
cnf(t118235,plain,
meet(sk2,composition(converse(sk1),sFlat2)) = composition(converse(sk1),sFlat2),
inference(orient,[status(thm)],[t291392]) ).
cnf(t118289,plain,
sFlat3 = join(sFlat3,meet(sk3,composition(converse(sk1),sFlat2))),
inference(cp,[status(thm)],[t66281,t118235]) ).
cnf(t109379,plain,
sk3 = join(sk3,composition(converse(sk1),sFlat1)),
inference(cp,[status(thm)],[t109373,t58]) ).
cnf(t109532,plain,
join(sk3,composition(converse(sk1),sFlat1)) = sk3,
inference(orient,[status(thm)],[t109379]) ).
cnf(t109560,plain,
zero = meet(composition(converse(sk1),sFlat1),complement(sk3)),
inference(cp,[status(thm)],[t17982,t109532]) ).
cnf(t291133,plain,
zero = meet(complement(sk3),composition(converse(sk1),sFlat1)),
inference(step,[status(thm)],[t109560,t146]) ).
cnf(t109781,plain,
meet(complement(sk3),composition(converse(sk1),sFlat1)) = zero,
inference(orient,[status(thm)],[t291133]) ).
cnf(t109795,plain,
composition(meet(sk1,composition(sFlat1,converse(complement(sk3)))),meet(complement(sk3),composition(converse(sk1),sFlat1))) = join(meet(composition(sk1,complement(sk3)),sFlat1),composition(meet(sk1,composition(sFlat1,converse(complement(sk3)))),zero)),
inference(cp,[status(thm)],[t32,t109781]) ).
cnf(t291134,plain,
composition(meet(sk1,composition(sFlat1,converse(complement(sk3)))),zero) = join(meet(composition(sk1,complement(sk3)),sFlat1),composition(meet(sk1,composition(sFlat1,converse(complement(sk3)))),zero)),
inference(step,[status(thm)],[t109795,t109781]) ).
cnf(t291135,plain,
zero = join(meet(composition(sk1,complement(sk3)),sFlat1),composition(meet(sk1,composition(sFlat1,converse(complement(sk3)))),zero)),
inference(step,[status(thm)],[t291134,t15756]) ).
cnf(t291136,plain,
zero = join(meet(sFlat1,composition(sk1,complement(sk3))),composition(meet(sk1,composition(sFlat1,converse(complement(sk3)))),zero)),
inference(step,[status(thm)],[t291135,t146]) ).
cnf(t291137,plain,
zero = join(meet(sFlat1,composition(sk1,complement(sk3))),zero),
inference(step,[status(thm)],[t291136,t15756]) ).
cnf(t291138,plain,
zero = meet(sFlat1,composition(sk1,complement(sk3))),
inference(step,[status(thm)],[t291137,t16248]) ).
cnf(t109802,plain,
meet(sFlat1,composition(sk1,complement(sk3))) = zero,
inference(orient,[status(thm)],[t291138]) ).
cnf(t109808,plain,
sFlat1 = join(zero,meet(complement(composition(sk1,complement(sk3))),sFlat1)),
inference(cp,[status(thm)],[t89978,t109802]) ).
cnf(t291169,plain,
sFlat1 = meet(complement(composition(sk1,complement(sk3))),sFlat1),
inference(step,[status(thm)],[t109808,t16197]) ).
cnf(t291170,plain,
sFlat1 = meet(sFlat1,complement(composition(sk1,complement(sk3)))),
inference(step,[status(thm)],[t291169,t146]) ).
cnf(t110055,plain,
meet(sFlat1,complement(composition(sk1,complement(sk3)))) = sFlat1,
inference(orient,[status(thm)],[t291170]) ).
cnf(t110088,plain,
zero = meet(meet(composition(sk1,complement(sk3)),X1),sFlat1),
inference(cp,[status(thm)],[t103469,t110055]) ).
cnf(t291338,plain,
zero = meet(sFlat1,meet(composition(sk1,complement(sk3)),X1)),
inference(step,[status(thm)],[t110088,t146]) ).
cnf(t116921,plain,
meet(sFlat1,meet(composition(sk1,complement(sk3)),X1)) = zero,
inference(orient,[status(thm)],[t291338]) ).
cnf(t16476,plain,
sFlat1 = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t16473,t126]) ).
cnf(t16515,plain,
join(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t16476]) ).
cnf(t16518,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t66,t16515]) ).
cnf(t16776,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t16518]) ).
cnf(t16783,plain,
join(sFlat1,meet(X1,sFlat2)) = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t16776,t16473]) ).
cnf(t289643,plain,
join(sFlat1,meet(X1,sFlat2)) = sFlat1,
inference(step,[status(thm)],[t16783,t16515]) ).
cnf(t16813,plain,
join(sFlat1,meet(X1,sFlat2)) = sFlat1,
inference(orient,[status(thm)],[t289643]) ).
cnf(t19198,plain,
meet(X1,sFlat2) = meet(meet(X1,sFlat2),sFlat1),
inference(cp,[status(thm)],[t19169,t16813]) ).
cnf(t289785,plain,
meet(X1,sFlat2) = meet(sFlat1,meet(X1,sFlat2)),
inference(step,[status(thm)],[t19198,t146]) ).
cnf(t19768,plain,
meet(sFlat1,meet(X1,sFlat2)) = meet(X1,sFlat2),
inference(orient,[status(thm)],[t289785]) ).
cnf(t116922,plain,
zero = meet(composition(sk1,complement(sk3)),sFlat2),
inference(cp,[status(thm)],[t116921,t19768]) ).
cnf(t291339,plain,
zero = meet(sFlat2,composition(sk1,complement(sk3))),
inference(step,[status(thm)],[t116922,t146]) ).
cnf(t116940,plain,
meet(sFlat2,composition(sk1,complement(sk3))) = zero,
inference(orient,[status(thm)],[t291339]) ).
cnf(t116957,plain,
composition(meet(converse(sk1),composition(complement(sk3),converse(sFlat2))),meet(sFlat2,composition(sk1,complement(sk3)))) = join(meet(composition(converse(sk1),sFlat2),complement(sk3)),composition(meet(converse(sk1),composition(complement(sk3),converse(sFlat2))),zero)),
inference(cp,[status(thm)],[t4856,t116940]) ).
cnf(t291342,plain,
composition(meet(converse(sk1),composition(complement(sk3),converse(sFlat2))),zero) = join(meet(composition(converse(sk1),sFlat2),complement(sk3)),composition(meet(converse(sk1),composition(complement(sk3),converse(sFlat2))),zero)),
inference(step,[status(thm)],[t116957,t116940]) ).
cnf(t291343,plain,
zero = join(meet(composition(converse(sk1),sFlat2),complement(sk3)),composition(meet(converse(sk1),composition(complement(sk3),converse(sFlat2))),zero)),
inference(step,[status(thm)],[t291342,t15756]) ).
cnf(t291344,plain,
zero = join(meet(complement(sk3),composition(converse(sk1),sFlat2)),composition(meet(converse(sk1),composition(complement(sk3),converse(sFlat2))),zero)),
inference(step,[status(thm)],[t291343,t146]) ).
cnf(t291345,plain,
zero = join(meet(complement(sk3),composition(converse(sk1),sFlat2)),zero),
inference(step,[status(thm)],[t291344,t15756]) ).
cnf(t291346,plain,
zero = meet(complement(sk3),composition(converse(sk1),sFlat2)),
inference(step,[status(thm)],[t291345,t16248]) ).
cnf(t117082,plain,
meet(complement(sk3),composition(converse(sk1),sFlat2)) = zero,
inference(orient,[status(thm)],[t291346]) ).
cnf(t117087,plain,
composition(converse(sk1),sFlat2) = join(zero,meet(complement(complement(sk3)),composition(converse(sk1),sFlat2))),
inference(cp,[status(thm)],[t104335,t117082]) ).
cnf(t291357,plain,
composition(converse(sk1),sFlat2) = meet(complement(complement(sk3)),composition(converse(sk1),sFlat2)),
inference(step,[status(thm)],[t117087,t16197]) ).
cnf(t291358,plain,
composition(converse(sk1),sFlat2) = meet(sk3,composition(converse(sk1),sFlat2)),
inference(step,[status(thm)],[t291357,t16303]) ).
cnf(t117628,plain,
meet(sk3,composition(converse(sk1),sFlat2)) = composition(converse(sk1),sFlat2),
inference(orient,[status(thm)],[t291358]) ).
cnf(t291393,plain,
sFlat3 = join(sFlat3,composition(converse(sk1),sFlat2)),
inference(step,[status(thm)],[t118289,t117628]) ).
cnf(t118318,plain,
join(sFlat3,composition(converse(sk1),sFlat2)) = sFlat3,
inference(orient,[status(thm)],[t291393]) ).
cnf(t237893,plain,
join(sFlat4,composition(sk1,composition(converse(sk1),sFlat2))) = composition(sk1,sFlat3),
inference(cp,[status(thm)],[t237864,t118318]) ).
cnf(t293271,plain,
join(sFlat4,composition(sk1,composition(converse(sk1),sFlat2))) = sFlat4,
inference(step,[status(thm)],[t237893,t129]) ).
cnf(t243997,plain,
join(sFlat4,composition(sk1,composition(converse(sk1),sFlat2))) = sFlat4,
inference(orient,[status(thm)],[t293271]) ).
cnf(t16424,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t66,t16413]) ).
cnf(t24769,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t16424]) ).
cnf(t298,plain,
meet(complement(X1),X2) = complement(join(meet(X1,X1),complement(X2))),
inference(cp,[status(thm)],[t114,t288]) ).
cnf(t1278,plain,
complement(join(meet(X1,X1),complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t298]) ).
cnf(t289611,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(step,[status(thm)],[t1278,t16266]) ).
cnf(t16300,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(rw,[status(thm)],[t289611]) ).
cnf(t18541,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t16300]) ).
cnf(t52796,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t52763,t18721]) ).
cnf(t54906,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t52796]) ).
cnf(t55276,plain,
meet(complement(X1),join(X2,X1)) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t18541,t54906]) ).
cnf(t290173,plain,
meet(complement(X1),join(X2,X1)) = meet(complement(X1),X2),
inference(step,[status(thm)],[t55276,t18541]) ).
cnf(t57082,plain,
meet(complement(X1),join(X2,X1)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t290173]) ).
cnf(t70,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t66,t63]) ).
cnf(t289815,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t70,t66]) ).
cnf(t20159,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t289815]) ).
cnf(t20188,plain,
join(X1,join(X2,meet(X3,X1))) = join(X2,X1),
inference(cp,[status(thm)],[t20159,t16473]) ).
cnf(t28450,plain,
join(X1,join(X2,meet(X3,X1))) = join(X2,X1),
inference(orient,[status(thm)],[t20188]) ).
cnf(t51775,plain,
sFlat0 = join(sFlat2,meet(sFlat0,complement(sFlat1))),
inference(cp,[status(thm)],[t51653,t126]) ).
cnf(t52259,plain,
join(sFlat2,meet(sFlat0,complement(sFlat1))) = sFlat0,
inference(orient,[status(thm)],[t51775]) ).
cnf(t52278,plain,
join(sFlat2,complement(sFlat1)) = join(complement(sFlat1),sFlat0),
inference(cp,[status(thm)],[t28450,t52259]) ).
cnf(t290115,plain,
join(sFlat2,complement(sFlat1)) = join(sFlat0,complement(sFlat1)),
inference(step,[status(thm)],[t52278,t63]) ).
cnf(t52295,plain,
join(sFlat2,complement(sFlat1)) = join(sFlat0,complement(sFlat1)),
inference(orient,[status(thm)],[t290115]) ).
cnf(t52302,plain,
meet(complement(sFlat2),sFlat1) = complement(join(sFlat0,complement(sFlat1))),
inference(cp,[status(thm)],[t18541,t52295]) ).
cnf(t290116,plain,
meet(sFlat1,complement(sFlat2)) = complement(join(sFlat0,complement(sFlat1))),
inference(step,[status(thm)],[t52302,t146]) ).
cnf(t290117,plain,
meet(sFlat1,complement(sFlat2)) = meet(complement(sFlat0),sFlat1),
inference(step,[status(thm)],[t290116,t18541]) ).
cnf(t290118,plain,
meet(sFlat1,complement(sFlat2)) = meet(sFlat1,complement(sFlat0)),
inference(step,[status(thm)],[t290117,t146]) ).
cnf(t52313,plain,
meet(sFlat1,complement(sFlat2)) = meet(sFlat1,complement(sFlat0)),
inference(orient,[status(thm)],[t290118]) ).
cnf(t52332,plain,
sFlat1 = join(meet(sFlat1,complement(sFlat0)),meet(sFlat1,complement(complement(sFlat2)))),
inference(cp,[status(thm)],[t51653,t52313]) ).
cnf(t290120,plain,
sFlat1 = join(meet(sFlat1,complement(sFlat0)),meet(sFlat1,sFlat2)),
inference(step,[status(thm)],[t52332,t16303]) ).
cnf(t19010,plain,
complement(sFlat2) = complement(meet(sFlat2,sFlat1)),
inference(cp,[status(thm)],[t18979,t16515]) ).
cnf(t289777,plain,
complement(sFlat2) = complement(meet(sFlat1,sFlat2)),
inference(step,[status(thm)],[t19010,t146]) ).
cnf(t19121,plain,
complement(meet(sFlat1,sFlat2)) = complement(sFlat2),
inference(orient,[status(thm)],[t289777]) ).
cnf(t19128,plain,
meet(sFlat1,sFlat2) = complement(complement(sFlat2)),
inference(cp,[status(thm)],[t16303,t19121]) ).
cnf(t289778,plain,
meet(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t19128,t16303]) ).
cnf(t19156,plain,
meet(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t289778]) ).
cnf(t290121,plain,
sFlat1 = join(meet(sFlat1,complement(sFlat0)),sFlat2),
inference(step,[status(thm)],[t290120,t19156]) ).
cnf(t290122,plain,
sFlat1 = join(sFlat2,meet(sFlat1,complement(sFlat0))),
inference(step,[status(thm)],[t290121,t63]) ).
cnf(t52351,plain,
join(sFlat2,meet(sFlat1,complement(sFlat0))) = sFlat1,
inference(orient,[status(thm)],[t290122]) ).
cnf(t52370,plain,
join(sFlat2,complement(sFlat0)) = join(complement(sFlat0),sFlat1),
inference(cp,[status(thm)],[t28450,t52351]) ).
cnf(t290123,plain,
join(sFlat2,complement(sFlat0)) = join(sFlat1,complement(sFlat0)),
inference(step,[status(thm)],[t52370,t63]) ).
cnf(t52387,plain,
join(sFlat2,complement(sFlat0)) = join(sFlat1,complement(sFlat0)),
inference(orient,[status(thm)],[t290123]) ).
cnf(t52393,plain,
join(sFlat2,join(complement(sFlat0),X1)) = join(join(sFlat1,complement(sFlat0)),X1),
inference(cp,[status(thm)],[t66,t52387]) ).
cnf(t291646,plain,
join(sFlat2,join(complement(sFlat0),X1)) = join(sFlat1,join(complement(sFlat0),X1)),
inference(step,[status(thm)],[t52393,t66]) ).
cnf(t127330,plain,
join(sFlat2,join(complement(sFlat0),X1)) = join(sFlat1,join(complement(sFlat0),X1)),
inference(orient,[status(thm)],[t291646]) ).
cnf(t127337,plain,
join(sFlat1,join(complement(sFlat0),complement(X1))) = join(sFlat2,complement(meet(sFlat0,X1))),
inference(cp,[status(thm)],[t127330,t18611]) ).
cnf(t291697,plain,
join(sFlat1,complement(meet(sFlat0,X1))) = join(sFlat2,complement(meet(sFlat0,X1))),
inference(step,[status(thm)],[t127337,t18611]) ).
cnf(t128946,plain,
join(sFlat2,complement(meet(sFlat0,X1))) = join(sFlat1,complement(meet(sFlat0,X1))),
inference(orient,[status(thm)],[t291697]) ).
cnf(t128954,plain,
meet(complement(complement(meet(sFlat0,X1))),sFlat2) = meet(complement(complement(meet(sFlat0,X1))),join(sFlat1,complement(meet(sFlat0,X1)))),
inference(cp,[status(thm)],[t57082,t128946]) ).
cnf(t291698,plain,
meet(sFlat2,complement(complement(meet(sFlat0,X1)))) = meet(complement(complement(meet(sFlat0,X1))),join(sFlat1,complement(meet(sFlat0,X1)))),
inference(step,[status(thm)],[t128954,t146]) ).
cnf(t291699,plain,
meet(sFlat2,meet(sFlat0,X1)) = meet(complement(complement(meet(sFlat0,X1))),join(sFlat1,complement(meet(sFlat0,X1)))),
inference(step,[status(thm)],[t291698,t16303]) ).
cnf(t291700,plain,
meet(sFlat2,meet(sFlat0,X1)) = meet(complement(complement(meet(sFlat0,X1))),sFlat1),
inference(step,[status(thm)],[t291699,t57082]) ).
cnf(t291701,plain,
meet(sFlat2,meet(sFlat0,X1)) = meet(sFlat1,complement(complement(meet(sFlat0,X1)))),
inference(step,[status(thm)],[t291700,t146]) ).
cnf(t291702,plain,
meet(sFlat2,meet(sFlat0,X1)) = meet(sFlat1,meet(sFlat0,X1)),
inference(step,[status(thm)],[t291701,t16303]) ).
cnf(t128971,plain,
meet(sFlat2,meet(sFlat0,X1)) = meet(sFlat1,meet(sFlat0,X1)),
inference(orient,[status(thm)],[t291702]) ).
cnf(t55277,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t17826,t54906]) ).
cnf(t290159,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t55277,t16303]) ).
cnf(t290160,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t290159,t114]) ).
cnf(t55296,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t290160]) ).
cnf(t55347,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t55296,t63]) ).
cnf(t55402,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t55347]) ).
cnf(t55451,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X1,X2)),
inference(cp,[status(thm)],[t55402,t16303]) ).
cnf(t57477,plain,
meet(complement(X1),join(X1,X2)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t55451]) ).
cnf(t16475,plain,
sk2 = join(sk2,sFlat3),
inference(cp,[status(thm)],[t16473,t155]) ).
cnf(t289634,plain,
sk2 = join(sFlat3,sk2),
inference(step,[status(thm)],[t16475,t63]) ).
cnf(t16506,plain,
join(sFlat3,sk2) = sk2,
inference(orient,[status(thm)],[t289634]) ).
cnf(t16510,plain,
top = join(complement(sFlat3),join(X1,sk2)),
inference(cp,[status(thm)],[t3363,t16506]) ).
cnf(t289664,plain,
top = join(sk2,join(complement(sFlat3),X1)),
inference(step,[status(thm)],[t16510,t16970]) ).
cnf(t17618,plain,
join(sk2,join(complement(sFlat3),X1)) = top,
inference(orient,[status(thm)],[t289664]) ).
cnf(t55010,plain,
join(join(complement(sFlat3),X1),complement(sk2)) = join(join(complement(sFlat3),X1),complement(top)),
inference(cp,[status(thm)],[t54906,t17618]) ).
cnf(t291778,plain,
join(complement(sFlat3),join(X1,complement(sk2))) = join(join(complement(sFlat3),X1),complement(top)),
inference(step,[status(thm)],[t55010,t66]) ).
cnf(t291779,plain,
join(complement(sFlat3),join(X1,complement(sk2))) = join(complement(sFlat3),join(X1,complement(top))),
inference(step,[status(thm)],[t291778,t66]) ).
cnf(t291780,plain,
join(complement(sFlat3),join(X1,complement(sk2))) = join(complement(sFlat3),join(X1,zero)),
inference(step,[status(thm)],[t291779,t137]) ).
cnf(t291781,plain,
join(complement(sFlat3),join(X1,complement(sk2))) = join(complement(sFlat3),X1),
inference(step,[status(thm)],[t291780,t16248]) ).
cnf(t132798,plain,
join(complement(sFlat3),join(X1,complement(sk2))) = join(complement(sFlat3),X1),
inference(orient,[status(thm)],[t291781]) ).
cnf(t132808,plain,
meet(complement(complement(sFlat3)),join(X1,complement(sk2))) = meet(complement(complement(sFlat3)),join(complement(sFlat3),X1)),
inference(cp,[status(thm)],[t57477,t132798]) ).
cnf(t291782,plain,
meet(sFlat3,join(X1,complement(sk2))) = meet(complement(complement(sFlat3)),join(complement(sFlat3),X1)),
inference(step,[status(thm)],[t132808,t16303]) ).
cnf(t291783,plain,
meet(sFlat3,join(X1,complement(sk2))) = meet(complement(complement(sFlat3)),X1),
inference(step,[status(thm)],[t291782,t57477]) ).
cnf(t291784,plain,
meet(sFlat3,join(X1,complement(sk2))) = meet(sFlat3,X1),
inference(step,[status(thm)],[t291783,t16303]) ).
cnf(t132851,plain,
meet(sFlat3,join(X1,complement(sk2))) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t291784]) ).
cnf(t132855,plain,
meet(sFlat3,X1) = meet(sFlat3,join(complement(sk2),X1)),
inference(cp,[status(thm)],[t132851,t63]) ).
cnf(t132907,plain,
meet(sFlat3,join(complement(sk2),X1)) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t132855]) ).
cnf(t79,plain,
complement(sk2) = join(complement(sk2),composition(converse(sk1),complement(sFlat0))),
inference(cp,[status(thm)],[t74,t53]) ).
cnf(t1432,plain,
join(complement(sk2),composition(converse(sk1),complement(sFlat0))) = complement(sk2),
inference(orient,[status(thm)],[t79]) ).
cnf(t132908,plain,
meet(sFlat3,composition(converse(sk1),complement(sFlat0))) = meet(sFlat3,complement(sk2)),
inference(cp,[status(thm)],[t132907,t1432]) ).
cnf(t18261,plain,
zero = meet(complement(sk2),sFlat3),
inference(cp,[status(thm)],[t18255,t155]) ).
cnf(t289706,plain,
zero = meet(sFlat3,complement(sk2)),
inference(step,[status(thm)],[t18261,t146]) ).
cnf(t18267,plain,
meet(sFlat3,complement(sk2)) = zero,
inference(orient,[status(thm)],[t289706]) ).
cnf(t291791,plain,
meet(sFlat3,composition(converse(sk1),complement(sFlat0))) = zero,
inference(step,[status(thm)],[t132908,t18267]) ).
cnf(t133148,plain,
meet(sFlat3,composition(converse(sk1),complement(sFlat0))) = zero,
inference(orient,[status(thm)],[t291791]) ).
cnf(t133165,plain,
composition(meet(sk1,composition(complement(sFlat0),converse(sFlat3))),meet(sFlat3,composition(converse(sk1),complement(sFlat0)))) = join(meet(composition(sk1,sFlat3),complement(sFlat0)),composition(meet(sk1,composition(complement(sFlat0),converse(sFlat3))),zero)),
inference(cp,[status(thm)],[t32,t133148]) ).
cnf(t291792,plain,
composition(meet(sk1,composition(complement(sFlat0),converse(sFlat3))),zero) = join(meet(composition(sk1,sFlat3),complement(sFlat0)),composition(meet(sk1,composition(complement(sFlat0),converse(sFlat3))),zero)),
inference(step,[status(thm)],[t133165,t133148]) ).
cnf(t291793,plain,
zero = join(meet(composition(sk1,sFlat3),complement(sFlat0)),composition(meet(sk1,composition(complement(sFlat0),converse(sFlat3))),zero)),
inference(step,[status(thm)],[t291792,t15756]) ).
cnf(t291794,plain,
zero = join(meet(complement(sFlat0),composition(sk1,sFlat3)),composition(meet(sk1,composition(complement(sFlat0),converse(sFlat3))),zero)),
inference(step,[status(thm)],[t291793,t146]) ).
cnf(t291795,plain,
zero = join(meet(complement(sFlat0),sFlat4),composition(meet(sk1,composition(complement(sFlat0),converse(sFlat3))),zero)),
inference(step,[status(thm)],[t291794,t129]) ).
cnf(t291796,plain,
zero = join(meet(sFlat4,complement(sFlat0)),composition(meet(sk1,composition(complement(sFlat0),converse(sFlat3))),zero)),
inference(step,[status(thm)],[t291795,t146]) ).
cnf(t291797,plain,
zero = join(meet(sFlat4,complement(sFlat0)),zero),
inference(step,[status(thm)],[t291796,t15756]) ).
cnf(t291798,plain,
zero = meet(sFlat4,complement(sFlat0)),
inference(step,[status(thm)],[t291797,t16248]) ).
cnf(t133173,plain,
meet(sFlat4,complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t291798]) ).
cnf(t133179,plain,
sFlat4 = join(zero,meet(complement(complement(sFlat0)),sFlat4)),
inference(cp,[status(thm)],[t89978,t133173]) ).
cnf(t291804,plain,
sFlat4 = meet(complement(complement(sFlat0)),sFlat4),
inference(step,[status(thm)],[t133179,t16197]) ).
cnf(t291805,plain,
sFlat4 = meet(sFlat4,complement(complement(sFlat0))),
inference(step,[status(thm)],[t291804,t146]) ).
cnf(t291806,plain,
sFlat4 = meet(sFlat4,sFlat0),
inference(step,[status(thm)],[t291805,t16303]) ).
cnf(t291807,plain,
sFlat4 = meet(sFlat0,sFlat4),
inference(step,[status(thm)],[t291806,t146]) ).
cnf(t133237,plain,
meet(sFlat0,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t291807]) ).
cnf(t133239,plain,
meet(sFlat1,meet(sFlat0,sFlat4)) = meet(sFlat2,sFlat4),
inference(cp,[status(thm)],[t128971,t133237]) ).
cnf(t291808,plain,
meet(sFlat1,sFlat4) = meet(sFlat2,sFlat4),
inference(step,[status(thm)],[t133239,t133237]) ).
cnf(t133334,plain,
meet(sFlat2,sFlat4) = meet(sFlat1,sFlat4),
inference(orient,[status(thm)],[t291808]) ).
cnf(t133425,plain,
join(sFlat2,X1) = join(sFlat2,join(meet(sFlat1,sFlat4),X1)),
inference(cp,[status(thm)],[t24769,t133334]) ).
cnf(t141365,plain,
join(sFlat2,join(meet(sFlat1,sFlat4),X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t133425]) ).
cnf(t16415,plain,
sk3 = join(sk3,sFlat3),
inference(cp,[status(thm)],[t16413,t155]) ).
cnf(t289631,plain,
sk3 = join(sFlat3,sk3),
inference(step,[status(thm)],[t16415,t63]) ).
cnf(t16447,plain,
join(sFlat3,sk3) = sk3,
inference(orient,[status(thm)],[t289631]) ).
cnf(t16451,plain,
top = join(complement(sFlat3),join(X1,sk3)),
inference(cp,[status(thm)],[t3363,t16447]) ).
cnf(t289659,plain,
top = join(sk3,join(complement(sFlat3),X1)),
inference(step,[status(thm)],[t16451,t16970]) ).
cnf(t17572,plain,
join(sk3,join(complement(sFlat3),X1)) = top,
inference(orient,[status(thm)],[t289659]) ).
cnf(t55026,plain,
join(join(complement(sFlat3),X1),complement(sk3)) = join(join(complement(sFlat3),X1),complement(top)),
inference(cp,[status(thm)],[t54906,t17572]) ).
cnf(t292191,plain,
join(complement(sFlat3),join(X1,complement(sk3))) = join(join(complement(sFlat3),X1),complement(top)),
inference(step,[status(thm)],[t55026,t66]) ).
cnf(t292192,plain,
join(complement(sFlat3),join(X1,complement(sk3))) = join(complement(sFlat3),join(X1,complement(top))),
inference(step,[status(thm)],[t292191,t66]) ).
cnf(t292193,plain,
join(complement(sFlat3),join(X1,complement(sk3))) = join(complement(sFlat3),join(X1,zero)),
inference(step,[status(thm)],[t292192,t137]) ).
cnf(t292194,plain,
join(complement(sFlat3),join(X1,complement(sk3))) = join(complement(sFlat3),X1),
inference(step,[status(thm)],[t292193,t16248]) ).
cnf(t157790,plain,
join(complement(sFlat3),join(X1,complement(sk3))) = join(complement(sFlat3),X1),
inference(orient,[status(thm)],[t292194]) ).
cnf(t157800,plain,
meet(complement(complement(sFlat3)),join(X1,complement(sk3))) = meet(complement(complement(sFlat3)),join(complement(sFlat3),X1)),
inference(cp,[status(thm)],[t57477,t157790]) ).
cnf(t292195,plain,
meet(sFlat3,join(X1,complement(sk3))) = meet(complement(complement(sFlat3)),join(complement(sFlat3),X1)),
inference(step,[status(thm)],[t157800,t16303]) ).
cnf(t292196,plain,
meet(sFlat3,join(X1,complement(sk3))) = meet(complement(complement(sFlat3)),X1),
inference(step,[status(thm)],[t292195,t57477]) ).
cnf(t292197,plain,
meet(sFlat3,join(X1,complement(sk3))) = meet(sFlat3,X1),
inference(step,[status(thm)],[t292196,t16303]) ).
cnf(t157844,plain,
meet(sFlat3,join(X1,complement(sk3))) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t292197]) ).
cnf(t157848,plain,
meet(sFlat3,X1) = meet(sFlat3,join(complement(sk3),X1)),
inference(cp,[status(thm)],[t157844,t63]) ).
cnf(t157910,plain,
meet(sFlat3,join(complement(sk3),X1)) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t157848]) ).
cnf(t77,plain,
complement(sk3) = join(complement(sk3),composition(converse(sk1),complement(sFlat1))),
inference(cp,[status(thm)],[t74,t58]) ).
cnf(t1429,plain,
join(complement(sk3),composition(converse(sk1),complement(sFlat1))) = complement(sk3),
inference(orient,[status(thm)],[t77]) ).
cnf(t157911,plain,
meet(sFlat3,composition(converse(sk1),complement(sFlat1))) = meet(sFlat3,complement(sk3)),
inference(cp,[status(thm)],[t157910,t1429]) ).
cnf(t17985,plain,
zero = meet(meet(X1,X2),complement(X1)),
inference(cp,[status(thm)],[t17982,t16413]) ).
cnf(t289703,plain,
zero = meet(complement(X1),meet(X1,X2)),
inference(step,[status(thm)],[t17985,t146]) ).
cnf(t18237,plain,
meet(complement(X1),meet(X1,X2)) = zero,
inference(orient,[status(thm)],[t289703]) ).
cnf(t18244,plain,
zero = meet(complement(sk3),sFlat3),
inference(cp,[status(thm)],[t18237,t155]) ).
cnf(t289704,plain,
zero = meet(sFlat3,complement(sk3)),
inference(step,[status(thm)],[t18244,t146]) ).
cnf(t18251,plain,
meet(sFlat3,complement(sk3)) = zero,
inference(orient,[status(thm)],[t289704]) ).
cnf(t292204,plain,
meet(sFlat3,composition(converse(sk1),complement(sFlat1))) = zero,
inference(step,[status(thm)],[t157911,t18251]) ).
cnf(t158174,plain,
meet(sFlat3,composition(converse(sk1),complement(sFlat1))) = zero,
inference(orient,[status(thm)],[t292204]) ).
cnf(t158191,plain,
composition(meet(sk1,composition(complement(sFlat1),converse(sFlat3))),meet(sFlat3,composition(converse(sk1),complement(sFlat1)))) = join(meet(composition(sk1,sFlat3),complement(sFlat1)),composition(meet(sk1,composition(complement(sFlat1),converse(sFlat3))),zero)),
inference(cp,[status(thm)],[t32,t158174]) ).
cnf(t292205,plain,
composition(meet(sk1,composition(complement(sFlat1),converse(sFlat3))),zero) = join(meet(composition(sk1,sFlat3),complement(sFlat1)),composition(meet(sk1,composition(complement(sFlat1),converse(sFlat3))),zero)),
inference(step,[status(thm)],[t158191,t158174]) ).
cnf(t292206,plain,
zero = join(meet(composition(sk1,sFlat3),complement(sFlat1)),composition(meet(sk1,composition(complement(sFlat1),converse(sFlat3))),zero)),
inference(step,[status(thm)],[t292205,t15756]) ).
cnf(t292207,plain,
zero = join(meet(complement(sFlat1),composition(sk1,sFlat3)),composition(meet(sk1,composition(complement(sFlat1),converse(sFlat3))),zero)),
inference(step,[status(thm)],[t292206,t146]) ).
cnf(t292208,plain,
zero = join(meet(complement(sFlat1),sFlat4),composition(meet(sk1,composition(complement(sFlat1),converse(sFlat3))),zero)),
inference(step,[status(thm)],[t292207,t129]) ).
cnf(t292209,plain,
zero = join(meet(sFlat4,complement(sFlat1)),composition(meet(sk1,composition(complement(sFlat1),converse(sFlat3))),zero)),
inference(step,[status(thm)],[t292208,t146]) ).
cnf(t292210,plain,
zero = join(meet(sFlat4,complement(sFlat1)),zero),
inference(step,[status(thm)],[t292209,t15756]) ).
cnf(t292211,plain,
zero = meet(sFlat4,complement(sFlat1)),
inference(step,[status(thm)],[t292210,t16248]) ).
cnf(t158199,plain,
meet(sFlat4,complement(sFlat1)) = zero,
inference(orient,[status(thm)],[t292211]) ).
cnf(t158208,plain,
sFlat4 = join(zero,meet(complement(complement(sFlat1)),sFlat4)),
inference(cp,[status(thm)],[t89978,t158199]) ).
cnf(t292221,plain,
sFlat4 = meet(complement(complement(sFlat1)),sFlat4),
inference(step,[status(thm)],[t158208,t16197]) ).
cnf(t292222,plain,
sFlat4 = meet(sFlat4,complement(complement(sFlat1))),
inference(step,[status(thm)],[t292221,t146]) ).
cnf(t292223,plain,
sFlat4 = meet(sFlat4,sFlat1),
inference(step,[status(thm)],[t292222,t16303]) ).
cnf(t292224,plain,
sFlat4 = meet(sFlat1,sFlat4),
inference(step,[status(thm)],[t292223,t146]) ).
cnf(t158270,plain,
meet(sFlat1,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t292224]) ).
cnf(t292255,plain,
join(sFlat2,join(sFlat4,X1)) = join(sFlat2,X1),
inference(step,[status(thm)],[t141365,t158270]) ).
cnf(t158412,plain,
join(sFlat2,join(sFlat4,X1)) = join(sFlat2,X1),
inference(rw,[status(thm)],[t292255]) ).
cnf(t160289,plain,
join(sFlat2,join(sFlat4,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t158412]) ).
cnf(t237948,plain,
join(sFlat4,composition(sk1,meet(sFlat3,X1))) = composition(sk1,sFlat3),
inference(cp,[status(thm)],[t237864,t16413]) ).
cnf(t293234,plain,
join(sFlat4,composition(sk1,meet(sFlat3,X1))) = sFlat4,
inference(step,[status(thm)],[t237948,t129]) ).
cnf(t240873,plain,
join(sFlat4,composition(sk1,meet(sFlat3,X1))) = sFlat4,
inference(orient,[status(thm)],[t293234]) ).
cnf(t240889,plain,
join(sFlat2,composition(sk1,meet(sFlat3,X1))) = join(sFlat2,sFlat4),
inference(cp,[status(thm)],[t160289,t240873]) ).
cnf(t51813,plain,
join(meet(X1,X2),complement(X2)) = join(complement(X2),X1),
inference(cp,[status(thm)],[t28450,t51653]) ).
cnf(t290157,plain,
join(complement(X2),meet(X1,X2)) = join(complement(X2),X1),
inference(step,[status(thm)],[t51813,t63]) ).
cnf(t54588,plain,
join(complement(X1),meet(X2,X1)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t290157]) ).
cnf(t128966,plain,
meet(complement(sFlat2),meet(sFlat0,X1)) = complement(join(sFlat1,complement(meet(sFlat0,X1)))),
inference(cp,[status(thm)],[t18541,t128946]) ).
cnf(t291729,plain,
meet(complement(sFlat2),meet(sFlat0,X1)) = meet(complement(sFlat1),meet(sFlat0,X1)),
inference(step,[status(thm)],[t128966,t18541]) ).
cnf(t130838,plain,
meet(complement(sFlat2),meet(sFlat0,X1)) = meet(complement(sFlat1),meet(sFlat0,X1)),
inference(orient,[status(thm)],[t291729]) ).
cnf(t133238,plain,
meet(complement(sFlat1),meet(sFlat0,sFlat4)) = meet(complement(sFlat2),sFlat4),
inference(cp,[status(thm)],[t130838,t133237]) ).
cnf(t291815,plain,
meet(complement(sFlat1),sFlat4) = meet(complement(sFlat2),sFlat4),
inference(step,[status(thm)],[t133238,t133237]) ).
cnf(t291816,plain,
meet(sFlat4,complement(sFlat1)) = meet(complement(sFlat2),sFlat4),
inference(step,[status(thm)],[t291815,t146]) ).
cnf(t291817,plain,
meet(sFlat4,complement(sFlat1)) = meet(sFlat4,complement(sFlat2)),
inference(step,[status(thm)],[t291816,t146]) ).
cnf(t134179,plain,
meet(sFlat4,complement(sFlat2)) = meet(sFlat4,complement(sFlat1)),
inference(orient,[status(thm)],[t291817]) ).
cnf(t134181,plain,
join(complement(complement(sFlat2)),sFlat4) = join(complement(complement(sFlat2)),meet(sFlat4,complement(sFlat1))),
inference(cp,[status(thm)],[t54588,t134179]) ).
cnf(t291829,plain,
join(sFlat4,complement(complement(sFlat2))) = join(complement(complement(sFlat2)),meet(sFlat4,complement(sFlat1))),
inference(step,[status(thm)],[t134181,t63]) ).
cnf(t291830,plain,
join(sFlat4,sFlat2) = join(complement(complement(sFlat2)),meet(sFlat4,complement(sFlat1))),
inference(step,[status(thm)],[t291829,t16303]) ).
cnf(t291831,plain,
join(sFlat2,sFlat4) = join(complement(complement(sFlat2)),meet(sFlat4,complement(sFlat1))),
inference(step,[status(thm)],[t291830,t63]) ).
cnf(t291832,plain,
join(sFlat2,sFlat4) = join(sFlat2,meet(sFlat4,complement(sFlat1))),
inference(step,[status(thm)],[t291831,t16303]) ).
cnf(t135456,plain,
join(sFlat2,meet(sFlat4,complement(sFlat1))) = join(sFlat2,sFlat4),
inference(orient,[status(thm)],[t291832]) ).
cnf(t292214,plain,
join(sFlat2,zero) = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t135456,t158199]) ).
cnf(t292215,plain,
sFlat2 = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t292214,t16248]) ).
cnf(t158221,plain,
sFlat2 = join(sFlat2,sFlat4),
inference(rw,[status(thm)],[t292215]) ).
cnf(t158422,plain,
join(sFlat2,sFlat4) = sFlat2,
inference(orient,[status(thm)],[t158221]) ).
cnf(t293244,plain,
join(sFlat2,composition(sk1,meet(sFlat3,X1))) = sFlat2,
inference(step,[status(thm)],[t240889,t158422]) ).
cnf(t241508,plain,
join(sFlat2,composition(sk1,meet(sFlat3,X1))) = sFlat2,
inference(orient,[status(thm)],[t293244]) ).
cnf(t241535,plain,
composition(sk1,meet(sFlat3,X1)) = meet(composition(sk1,meet(sFlat3,X1)),sFlat2),
inference(cp,[status(thm)],[t19169,t241508]) ).
cnf(t293713,plain,
composition(sk1,meet(sFlat3,X1)) = meet(sFlat2,composition(sk1,meet(sFlat3,X1))),
inference(step,[status(thm)],[t241535,t146]) ).
cnf(t288323,plain,
meet(sFlat2,composition(sk1,meet(sFlat3,X1))) = composition(sk1,meet(sFlat3,X1)),
inference(orient,[status(thm)],[t293713]) ).
cnf(t118329,plain,
composition(converse(sk1),sFlat2) = meet(composition(converse(sk1),sFlat2),sFlat3),
inference(cp,[status(thm)],[t19169,t118318]) ).
cnf(t291408,plain,
composition(converse(sk1),sFlat2) = meet(sFlat3,composition(converse(sk1),sFlat2)),
inference(step,[status(thm)],[t118329,t146]) ).
cnf(t118554,plain,
meet(sFlat3,composition(converse(sk1),sFlat2)) = composition(converse(sk1),sFlat2),
inference(orient,[status(thm)],[t291408]) ).
cnf(t288324,plain,
composition(sk1,meet(sFlat3,composition(converse(sk1),sFlat2))) = meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2))),
inference(cp,[status(thm)],[t288323,t118554]) ).
cnf(t293714,plain,
composition(sk1,composition(converse(sk1),sFlat2)) = meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2))),
inference(step,[status(thm)],[t288324,t118554]) ).
cnf(t14,axiom,
join(meet(composition(X1,X2),X3),meet(composition(X1,meet(X2,composition(converse(X1),X3))),X3)) = meet(composition(X1,meet(X2,composition(converse(X1),X3))),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t85,plain,
join(meet(composition(X1,X2),X3),meet(composition(X1,meet(X2,composition(converse(X1),X3))),X3)) = meet(composition(X1,meet(X2,composition(converse(X1),X3))),X3),
inference(orient,[status(thm)],[t14]) ).
cnf(t152,plain,
join(meet(composition(X1,X2),X3),meet(composition(X1,meet(X2,composition(converse(X1),X3))),X3)) = meet(composition(X1,meet(X2,composition(converse(X1),X3))),X3),
inference(rw,[status(thm)],[t85]) ).
cnf(t289959,plain,
join(meet(composition(X1,X2),X3),meet(X3,composition(X1,meet(X2,composition(converse(X1),X3))))) = meet(composition(X1,meet(X2,composition(converse(X1),X3))),X3),
inference(step,[status(thm)],[t152,t146]) ).
cnf(t289960,plain,
join(meet(composition(X1,X2),X3),meet(X3,composition(X1,meet(X2,composition(converse(X1),X3))))) = meet(X3,composition(X1,meet(X2,composition(converse(X1),X3)))),
inference(step,[status(thm)],[t289959,t146]) ).
cnf(t42971,plain,
join(meet(composition(X1,X2),X3),meet(X3,composition(X1,meet(X2,composition(converse(X1),X3))))) = meet(X3,composition(X1,meet(X2,composition(converse(X1),X3)))),
inference(orient,[status(thm)],[t289960]) ).
cnf(t117709,plain,
meet(sFlat2,composition(sk1,meet(sk3,composition(converse(sk1),sFlat2)))) = join(meet(composition(sk1,sk3),sFlat2),meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2)))),
inference(cp,[status(thm)],[t42971,t117628]) ).
cnf(t291572,plain,
meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2))) = join(meet(composition(sk1,sk3),sFlat2),meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2)))),
inference(step,[status(thm)],[t117709,t117628]) ).
cnf(t291573,plain,
meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2))) = join(meet(sFlat2,composition(sk1,sk3)),meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2)))),
inference(step,[status(thm)],[t291572,t146]) ).
cnf(t291574,plain,
meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2))) = join(meet(sFlat2,sFlat1),meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2)))),
inference(step,[status(thm)],[t291573,t58]) ).
cnf(t291575,plain,
meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2))) = join(meet(sFlat1,sFlat2),meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2)))),
inference(step,[status(thm)],[t291574,t146]) ).
cnf(t291576,plain,
meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2))) = join(sFlat2,meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2)))),
inference(step,[status(thm)],[t291575,t19156]) ).
cnf(t291577,plain,
meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2))) = sFlat2,
inference(step,[status(thm)],[t291576,t16413]) ).
cnf(t124270,plain,
meet(sFlat2,composition(sk1,composition(converse(sk1),sFlat2))) = sFlat2,
inference(orient,[status(thm)],[t291577]) ).
cnf(t293715,plain,
composition(sk1,composition(converse(sk1),sFlat2)) = sFlat2,
inference(step,[status(thm)],[t293714,t124270]) ).
cnf(t288511,plain,
composition(sk1,composition(converse(sk1),sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t293715]) ).
cnf(t293716,plain,
join(sFlat4,sFlat2) = sFlat4,
inference(step,[status(thm)],[t243997,t288511]) ).
cnf(t288591,plain,
join(sFlat4,sFlat2) = sFlat4,
inference(rw,[status(thm)],[t293716]) ).
cnf(t293717,plain,
join(sFlat2,sFlat4) = sFlat4,
inference(step,[status(thm)],[t288591,t63]) ).
cnf(t293718,plain,
sFlat2 = sFlat4,
inference(step,[status(thm)],[t293717,t158422]) ).
cnf(t288592,plain,
sFlat4 = sFlat2,
inference(orient,[status(thm)],[t293718]) ).
cnf(t293719,plain,
composition(sk1,sFlat3) = sFlat2,
inference(step,[status(thm)],[t129,t288592]) ).
cnf(t288593,plain,
composition(sk1,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t293719]) ).
cnf(goal_0,negated_conjecture,
meet(composition(sk1,sk2),composition(sk1,sk3)) != composition(sk1,meet(sk2,sk3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(composition(sk1,sk3),composition(sk1,sk2)) != composition(sk1,meet(sk2,sk3)),
inference(rw,[status(thm)],[goal_0,t146]) ).
cnf(g0_1,plain,
meet(sFlat1,composition(sk1,sk2)) != composition(sk1,meet(sk2,sk3)),
inference(rw,[status(thm)],[g0_0,t58]) ).
cnf(g0_2,plain,
meet(sFlat1,sFlat0) != composition(sk1,meet(sk2,sk3)),
inference(rw,[status(thm)],[g0_1,t53]) ).
cnf(g0_3,plain,
meet(sFlat0,sFlat1) != composition(sk1,meet(sk2,sk3)),
inference(rw,[status(thm)],[g0_2,t146]) ).
cnf(g0_4,plain,
sFlat2 != composition(sk1,meet(sk2,sk3)),
inference(rw,[status(thm)],[g0_3,t126]) ).
cnf(g0_5,plain,
sFlat2 != composition(sk1,meet(sk3,sk2)),
inference(rw,[status(thm)],[g0_4,t146]) ).
cnf(g0_6,plain,
sFlat2 != composition(sk1,sFlat3),
inference(rw,[status(thm)],[g0_5,t155]) ).
cnf(g0_7,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_6,t288593]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL040-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n002.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 07:36:34 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 266.21/34.99 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 266.21/34.99 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------