%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL030-3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:35:52 PM UTC 2026
% Result : Unsatisfiable 124.87s 16.41s
% Output : CNFRefutation 81.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 126
% Number of leaves : 23
% Syntax : Number of clauses : 708 ( 708 unt; 0 nHn; 265 RR)
% Number of literals : 708 ( 707 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 12 con; 0-2 aty)
% Number of variables : 715 ( 78 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t17,axiom,
sFlat0 = composition(sk1,sk2),
introduced(definition) ).
cnf(t54,plain,
composition(sk1,sk2) = sFlat0,
inference(orient,[status(thm)],[t17]) ).
cnf(t18,axiom,
sFlat1 = composition(sk1,sk3),
introduced(definition) ).
cnf(t49,plain,
composition(sk1,sk3) = sFlat1,
inference(orient,[status(thm)],[t18]) ).
cnf(t19,axiom,
sFlat2 = complement(composition(sk1,sk3)),
introduced(definition) ).
cnf(t44596,plain,
sFlat2 = complement(sFlat1),
inference(step,[status(thm)],[t19,t49]) ).
cnf(t119,plain,
complement(sFlat1) = sFlat2,
inference(orient,[status(thm)],[t44596]) ).
cnf(t20,axiom,
sFlat3 = meet(composition(sk1,sk2),complement(composition(sk1,sk3))),
introduced(definition) ).
cnf(t44593,plain,
sFlat3 = meet(sFlat0,complement(composition(sk1,sk3))),
inference(step,[status(thm)],[t20,t54]) ).
cnf(t44594,plain,
sFlat3 = meet(sFlat0,complement(sFlat1)),
inference(step,[status(thm)],[t44593,t49]) ).
cnf(t117,plain,
meet(sFlat0,complement(sFlat1)) = sFlat3,
inference(orient,[status(thm)],[t44594]) ).
cnf(t44597,plain,
meet(sFlat0,sFlat2) = sFlat3,
inference(step,[status(thm)],[t117,t119]) ).
cnf(t125,plain,
meet(sFlat0,sFlat2) = sFlat3,
inference(rw,[status(thm)],[t44597]) ).
cnf(t136,plain,
meet(sFlat0,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t125]) ).
cnf(t6,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t105,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t59,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t107,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t105,t59]) ).
cnf(t44600,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t107,t105]) ).
cnf(t141,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t44600]) ).
cnf(t21,axiom,
sFlat4 = complement(sk3),
introduced(definition) ).
cnf(t126,plain,
complement(sk3) = sFlat4,
inference(orient,[status(thm)],[t21]) ).
cnf(t22,axiom,
sFlat5 = meet(composition(sk1,sk2),complement(sk3)),
introduced(definition) ).
cnf(t44595,plain,
sFlat5 = meet(sFlat0,complement(sk3)),
inference(step,[status(thm)],[t22,t54]) ).
cnf(t118,plain,
meet(sFlat0,complement(sk3)) = sFlat5,
inference(orient,[status(thm)],[t44595]) ).
cnf(t44598,plain,
meet(sFlat0,sFlat4) = sFlat5,
inference(step,[status(thm)],[t118,t126]) ).
cnf(t132,plain,
meet(sFlat0,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t44598]) ).
cnf(t140,plain,
meet(sFlat0,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t132]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t60,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t24]) ).
cnf(t45636,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t60,t59]) ).
cnf(t45637,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t45636,t105]) ).
cnf(t45638,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t45637,t59]) ).
cnf(t24414,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t45638]) ).
cnf(t24471,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t24414,t105]) ).
cnf(t45834,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t24471,t59]) ).
cnf(t26941,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t45834]) ).
cnf(t109,plain,
meet(join(complement(X1),complement(X2)),X3) = complement(join(meet(X1,X2),complement(X3))),
inference(cp,[status(thm)],[t105,t105]) ).
cnf(t1371,plain,
complement(join(meet(X1,X2),complement(X3))) = meet(join(complement(X1),complement(X2)),X3),
inference(orient,[status(thm)],[t109]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t112,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t24429,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t24414,t112]) ).
cnf(t25,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(join(complement(X1),complement(X2))),join(complement(X1),X2)))),
inference(cp,[status(thm)],[t24,t24]) ).
cnf(t44611,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(join(complement(X1),X2),complement(join(complement(X1),complement(X2)))))),
inference(step,[status(thm)],[t25,t59]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t61,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t44612,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,complement(join(complement(X1),complement(X2))))))),
inference(step,[status(thm)],[t44611,t61]) ).
cnf(t44613,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t44612,t105]) ).
cnf(t290,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t44613]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t44592,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t59]) ).
cnf(t69,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t44592]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t70,plain,
complement(X1) = join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))),
inference(cp,[status(thm)],[t69,t27]) ).
cnf(t12153,plain,
join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))) = complement(X1),
inference(orient,[status(thm)],[t70]) ).
cnf(t62,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t61,t59]) ).
cnf(t382,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t62]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t66,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t128,plain,
top = join(sk3,sFlat4),
inference(cp,[status(thm)],[t66,t126]) ).
cnf(t44599,plain,
top = join(sFlat4,sk3),
inference(step,[status(thm)],[t128,t59]) ).
cnf(t138,plain,
join(sFlat4,sk3) = top,
inference(orient,[status(thm)],[t44599]) ).
cnf(t139,plain,
join(sFlat4,join(sk3,X1)) = join(top,X1),
inference(cp,[status(thm)],[t61,t138]) ).
cnf(t437,plain,
join(sFlat4,join(sk3,X1)) = join(top,X1),
inference(orient,[status(thm)],[t139]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t99,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t100,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t99,t27]) ).
cnf(t322,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t100]) ).
cnf(t323,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t322,t66]) ).
cnf(t592,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t323]) ).
cnf(t601,plain,
join(top,converse(complement(converse(sk3)))) = join(sFlat4,converse(top)),
inference(cp,[status(thm)],[t437,t592]) ).
cnf(t68,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t61,t66]) ).
cnf(t535,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t68]) ).
cnf(t541,plain,
join(top,complement(complement(X1))) = join(X1,top),
inference(cp,[status(thm)],[t535,t66]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t42,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t40,t27]) ).
cnf(t250,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t42]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t251,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t250,t23]) ).
cnf(t44608,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t251,t27]) ).
cnf(t263,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t44608]) ).
cnf(t9,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t29,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t28,t23]) ).
cnf(t158,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t29]) ).
cnf(t265,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t263,t158]) ).
cnf(t44610,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t265,t263]) ).
cnf(t284,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t44610]) ).
cnf(t287,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t69,t284]) ).
cnf(t264,plain,
one = converse(one),
inference(cp,[status(thm)],[t263,t23]) ).
cnf(t273,plain,
converse(one) = one,
inference(orient,[status(thm)],[t264]) ).
cnf(t44623,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t287,t273]) ).
cnf(t44624,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t44623,t284]) ).
cnf(t472,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t44624]) ).
cnf(t540,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t535,t472]) ).
cnf(t44636,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t540,t66]) ).
cnf(t561,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t44636]) ).
cnf(t44643,plain,
top = join(X1,top),
inference(step,[status(thm)],[t541,t561]) ).
cnf(t583,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t44643]) ).
cnf(t585,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t322,t583]) ).
cnf(t586,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t585]) ).
cnf(t44661,plain,
join(top,converse(complement(converse(sk3)))) = converse(top),
inference(step,[status(thm)],[t601,t586]) ).
cnf(t768,plain,
join(top,converse(complement(converse(sk3)))) = converse(top),
inference(orient,[status(thm)],[t44661]) ).
cnf(t770,plain,
join(converse(complement(converse(sk3))),join(X1,top)) = join(X1,converse(top)),
inference(cp,[status(thm)],[t382,t768]) ).
cnf(t44662,plain,
join(converse(complement(converse(sk3))),top) = join(X1,converse(top)),
inference(step,[status(thm)],[t770,t583]) ).
cnf(t44663,plain,
top = join(X1,converse(top)),
inference(step,[status(thm)],[t44662,t583]) ).
cnf(t44664,plain,
top = converse(top),
inference(step,[status(thm)],[t44663,t586]) ).
cnf(t771,plain,
converse(top) = top,
inference(orient,[status(thm)],[t44664]) ).
cnf(t12237,plain,
complement(X1) = join(complement(X1),composition(top,complement(composition(top,X1)))),
inference(cp,[status(thm)],[t12153,t771]) ).
cnf(t780,plain,
converse(join(top,X1)) = join(top,converse(X1)),
inference(cp,[status(thm)],[t99,t771]) ).
cnf(t791,plain,
converse(join(top,X1)) = join(top,converse(X1)),
inference(orient,[status(thm)],[t780]) ).
cnf(t804,plain,
join(top,converse(X1)) = converse(join(X1,top)),
inference(cp,[status(thm)],[t791,t59]) ).
cnf(t44674,plain,
join(top,converse(X1)) = converse(top),
inference(step,[status(thm)],[t804,t583]) ).
cnf(t44675,plain,
join(top,converse(X1)) = top,
inference(step,[status(thm)],[t44674,t771]) ).
cnf(t818,plain,
join(top,converse(X1)) = top,
inference(orient,[status(thm)],[t44675]) ).
cnf(t44676,plain,
converse(join(top,X1)) = top,
inference(step,[status(thm)],[t791,t818]) ).
cnf(t819,plain,
converse(join(top,X1)) = top,
inference(orient,[status(thm)],[t44676]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t285,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t30,t284]) ).
cnf(t628,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t285]) ).
cnf(t2,axiom,
join(sk1,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t103,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t104,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t61,t103]) ).
cnf(t172,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t104]) ).
cnf(t174,plain,
join(one,X1) = join(sk1,join(X1,one)),
inference(cp,[status(thm)],[t172,t59]) ).
cnf(t469,plain,
join(sk1,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t174]) ).
cnf(t536,plain,
join(top,one) = join(one,complement(sk1)),
inference(cp,[status(thm)],[t535,t469]) ).
cnf(t581,plain,
join(one,complement(sk1)) = join(top,one),
inference(orient,[status(thm)],[t536]) ).
cnf(t542,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t535,t59]) ).
cnf(t606,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t542]) ).
cnf(t609,plain,
join(top,one) = join(sk1,join(top,one)),
inference(cp,[status(thm)],[t606,t581]) ).
cnf(t44645,plain,
join(top,one) = join(one,top),
inference(step,[status(thm)],[t609,t469]) ).
cnf(t44646,plain,
join(top,one) = top,
inference(step,[status(thm)],[t44645,t583]) ).
cnf(t625,plain,
join(top,one) = top,
inference(orient,[status(thm)],[t44646]) ).
cnf(t44647,plain,
join(one,complement(sk1)) = top,
inference(step,[status(thm)],[t581,t625]) ).
cnf(t626,plain,
join(one,complement(sk1)) = top,
inference(orient,[status(thm)],[t44647]) ).
cnf(t631,plain,
join(X1,composition(complement(sk1),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t628,t626]) ).
cnf(t982,plain,
join(X1,composition(complement(sk1),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t631]) ).
cnf(t984,plain,
top = converse(composition(top,top)),
inference(cp,[status(thm)],[t819,t982]) ).
cnf(t782,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t40,t771]) ).
cnf(t842,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t782]) ).
cnf(t44681,plain,
top = composition(converse(top),top),
inference(step,[status(thm)],[t984,t842]) ).
cnf(t44682,plain,
top = composition(top,top),
inference(step,[status(thm)],[t44681,t771]) ).
cnf(t991,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t44682]) ).
cnf(t993,plain,
composition(top,composition(top,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t28,t991]) ).
cnf(t1017,plain,
composition(top,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t993]) ).
cnf(t1020,plain,
complement(composition(top,X1)) = join(complement(composition(top,X1)),composition(converse(top),complement(composition(top,X1)))),
inference(cp,[status(thm)],[t69,t1017]) ).
cnf(t286,plain,
composition(join(X1,one),X2) = join(composition(X1,X2),X2),
inference(cp,[status(thm)],[t30,t284]) ).
cnf(t44649,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(step,[status(thm)],[t286,t59]) ).
cnf(t650,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t44649]) ).
cnf(t44941,plain,
complement(composition(top,X1)) = composition(join(converse(top),one),complement(composition(top,X1))),
inference(step,[status(thm)],[t1020,t650]) ).
cnf(t44942,plain,
complement(composition(top,X1)) = composition(join(one,converse(top)),complement(composition(top,X1))),
inference(step,[status(thm)],[t44941,t59]) ).
cnf(t44943,plain,
complement(composition(top,X1)) = composition(converse(top),complement(composition(top,X1))),
inference(step,[status(thm)],[t44942,t586]) ).
cnf(t44944,plain,
complement(composition(top,X1)) = composition(top,complement(composition(top,X1))),
inference(step,[status(thm)],[t44943,t771]) ).
cnf(t5924,plain,
composition(top,complement(composition(top,X1))) = complement(composition(top,X1)),
inference(orient,[status(thm)],[t44944]) ).
cnf(t45154,plain,
complement(X1) = join(complement(X1),complement(composition(top,X1))),
inference(step,[status(thm)],[t12237,t5924]) ).
cnf(t12285,plain,
join(complement(X1),complement(composition(top,X1))) = complement(X1),
inference(orient,[status(thm)],[t45154]) ).
cnf(t12327,plain,
meet(X1,composition(top,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t105,t12285]) ).
cnf(t12338,plain,
meet(X1,composition(top,X1)) = complement(complement(X1)),
inference(orient,[status(thm)],[t12327]) ).
cnf(t12361,plain,
join(complement(X1),complement(composition(top,X1))) = join(complement(X1),complement(join(complement(X1),join(composition(top,X1),complement(complement(X1)))))),
inference(cp,[status(thm)],[t290,t12338]) ).
cnf(t45155,plain,
complement(X1) = join(complement(X1),complement(join(complement(X1),join(composition(top,X1),complement(complement(X1)))))),
inference(step,[status(thm)],[t12361,t12285]) ).
cnf(t45156,plain,
complement(X1) = join(complement(X1),complement(join(top,composition(top,X1)))),
inference(step,[status(thm)],[t45155,t606]) ).
cnf(t41,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t40,t27]) ).
cnf(t240,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t41]) ).
cnf(t823,plain,
top = join(top,composition(X1,converse(X2))),
inference(cp,[status(thm)],[t818,t240]) ).
cnf(t2182,plain,
join(top,composition(X1,converse(X2))) = top,
inference(orient,[status(thm)],[t823]) ).
cnf(t2194,plain,
top = join(top,composition(X1,X2)),
inference(cp,[status(thm)],[t2182,t27]) ).
cnf(t2198,plain,
join(top,composition(X1,X2)) = top,
inference(orient,[status(thm)],[t2194]) ).
cnf(t45157,plain,
complement(X1) = join(complement(X1),complement(top)),
inference(step,[status(thm)],[t45156,t2198]) ).
cnf(t106,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t105,t66]) ).
cnf(t44602,plain,
zero = complement(top),
inference(step,[status(thm)],[t106,t112]) ).
cnf(t149,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t44602]) ).
cnf(t45158,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t45157,t149]) ).
cnf(t45159,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t45158,t59]) ).
cnf(t12365,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t45159]) ).
cnf(t45651,plain,
X1 = complement(join(complement(X1),complement(X1))),
inference(step,[status(thm)],[t24429,t12365]) ).
cnf(t45652,plain,
X1 = meet(X1,X1),
inference(step,[status(thm)],[t45651,t105]) ).
cnf(t24693,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t45652]) ).
cnf(t24712,plain,
meet(join(complement(X1),complement(X1)),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t1371,t24693]) ).
cnf(t45779,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(step,[status(thm)],[t24712,t472]) ).
cnf(t25971,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t45779]) ).
cnf(t102,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t61,t99]) ).
cnf(t1066,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t102]) ).
cnf(t652,plain,
join(X1,composition(sk1,X1)) = composition(one,X1),
inference(cp,[status(thm)],[t650,t103]) ).
cnf(t44652,plain,
join(X1,composition(sk1,X1)) = X1,
inference(step,[status(thm)],[t652,t284]) ).
cnf(t729,plain,
join(X1,composition(sk1,X1)) = X1,
inference(orient,[status(thm)],[t44652]) ).
cnf(t1077,plain,
join(converse(join(X1,X2)),composition(sk1,converse(X2))) = join(converse(X1),converse(X2)),
inference(cp,[status(thm)],[t1066,t729]) ).
cnf(t45424,plain,
join(composition(sk1,converse(X2)),converse(join(X1,X2))) = join(converse(X1),converse(X2)),
inference(step,[status(thm)],[t1077,t59]) ).
cnf(t45425,plain,
join(composition(sk1,converse(X2)),converse(join(X1,X2))) = converse(join(X1,X2)),
inference(step,[status(thm)],[t45424,t99]) ).
cnf(t19314,plain,
join(composition(sk1,converse(X1)),converse(join(X2,X1))) = converse(join(X2,X1)),
inference(orient,[status(thm)],[t45425]) ).
cnf(t19334,plain,
converse(join(X1,converse(X2))) = join(composition(sk1,X2),converse(join(X1,converse(X2)))),
inference(cp,[status(thm)],[t19314,t27]) ).
cnf(t101,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t99,t27]) ).
cnf(t349,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t101]) ).
cnf(t45467,plain,
join(converse(X1),X2) = join(composition(sk1,X2),converse(join(X1,converse(X2)))),
inference(step,[status(thm)],[t19334,t349]) ).
cnf(t45468,plain,
join(converse(X1),X2) = join(composition(sk1,X2),join(converse(X1),X2)),
inference(step,[status(thm)],[t45467,t349]) ).
cnf(t45469,plain,
join(converse(X1),X2) = join(X2,join(composition(sk1,X2),converse(X1))),
inference(step,[status(thm)],[t45468,t382]) ).
cnf(t19977,plain,
join(X1,join(composition(sk1,X1),converse(X2))) = join(converse(X2),X1),
inference(orient,[status(thm)],[t45469]) ).
cnf(t20018,plain,
join(converse(converse(X1)),X2) = join(X2,join(composition(sk1,X2),X1)),
inference(cp,[status(thm)],[t19977,t27]) ).
cnf(t45476,plain,
join(X1,X2) = join(X2,join(composition(sk1,X2),X1)),
inference(step,[status(thm)],[t20018,t27]) ).
cnf(t20175,plain,
join(X1,join(composition(sk1,X1),X2)) = join(X2,X1),
inference(orient,[status(thm)],[t45476]) ).
cnf(t20224,plain,
join(X1,X2) = join(X2,join(X1,composition(sk1,X2))),
inference(cp,[status(thm)],[t20175,t59]) ).
cnf(t20368,plain,
join(X1,join(X2,composition(sk1,X1))) = join(X2,X1),
inference(orient,[status(thm)],[t20224]) ).
cnf(t255,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t99,t250]) ).
cnf(t3669,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t255]) ).
cnf(t43,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t30,t40]) ).
cnf(t12893,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t43]) ).
cnf(t13039,plain,
join(converse(converse(composition(X1,X2))),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(cp,[status(thm)],[t3669,t12893]) ).
cnf(t45262,plain,
join(composition(X1,X2),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t13039,t27]) ).
cnf(t45263,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t45262,t27]) ).
cnf(t331,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t40,t322]) ).
cnf(t3815,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t331]) ).
cnf(t45264,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(converse(converse(X1)),join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t45263,t3815]) ).
cnf(t45265,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t45264,t27]) ).
cnf(t45266,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t45265,t27]) ).
cnf(t14471,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t45266]) ).
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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t16]) ).
cnf(t38,plain,
composition(meet(X1,composition(one,converse(X2))),meet(X2,composition(converse(X1),one))) = join(meet(composition(X1,X2),one),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(cp,[status(thm)],[t33,t23]) ).
cnf(t45059,plain,
composition(meet(X1,converse(X2)),meet(X2,composition(converse(X1),one))) = join(meet(composition(X1,X2),one),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t38,t284]) ).
cnf(t45060,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(composition(X1,X2),one),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t45059,t23]) ).
cnf(t45061,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(one,composition(X1,X2)),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t45060,t141]) ).
cnf(t45062,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(one,composition(X1,X2)),composition(meet(X1,converse(X2)),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t45061,t284]) ).
cnf(t8865,plain,
join(meet(one,composition(X1,X2)),composition(meet(X1,converse(X2)),meet(X2,converse(X1)))) = composition(meet(X1,converse(X2)),meet(X2,converse(X1))),
inference(orient,[status(thm)],[t45062]) ).
cnf(t26969,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t26941,t141]) ).
cnf(t28824,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t26969]) ).
cnf(t19459,plain,
join(converse(composition(sk1,converse(X1))),join(X2,X1)) = converse(converse(join(X2,X1))),
inference(cp,[status(thm)],[t349,t19314]) ).
cnf(t45445,plain,
join(X1,join(converse(composition(sk1,converse(X1))),X2)) = converse(converse(join(X2,X1))),
inference(step,[status(thm)],[t19459,t382]) ).
cnf(t45446,plain,
join(X1,join(composition(X1,converse(sk1)),X2)) = converse(converse(join(X2,X1))),
inference(step,[status(thm)],[t45445,t240]) ).
cnf(t45447,plain,
join(X1,join(composition(X1,converse(sk1)),X2)) = join(X2,X1),
inference(step,[status(thm)],[t45446,t27]) ).
cnf(t19528,plain,
join(X1,join(composition(X1,converse(sk1)),X2)) = join(X2,X1),
inference(orient,[status(thm)],[t45447]) ).
cnf(t44667,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t592,t771]) ).
cnf(t774,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t44667]) ).
cnf(t19569,plain,
join(converse(complement(converse(composition(X1,converse(sk1))))),X1) = join(X1,top),
inference(cp,[status(thm)],[t19528,t774]) ).
cnf(t45453,plain,
join(X1,converse(complement(converse(composition(X1,converse(sk1)))))) = join(X1,top),
inference(step,[status(thm)],[t19569,t59]) ).
cnf(t45454,plain,
join(X1,converse(complement(composition(sk1,converse(X1))))) = join(X1,top),
inference(step,[status(thm)],[t45453,t240]) ).
cnf(t45455,plain,
join(X1,converse(complement(composition(sk1,converse(X1))))) = top,
inference(step,[status(thm)],[t45454,t583]) ).
cnf(t19775,plain,
join(X1,converse(complement(composition(sk1,converse(X1))))) = top,
inference(orient,[status(thm)],[t45455]) ).
cnf(t19834,plain,
join(X1,converse(converse(complement(composition(sk1,converse(converse(X1))))))) = converse(top),
inference(cp,[status(thm)],[t322,t19775]) ).
cnf(t45456,plain,
join(X1,complement(composition(sk1,converse(converse(X1))))) = converse(top),
inference(step,[status(thm)],[t19834,t27]) ).
cnf(t45457,plain,
join(X1,complement(composition(sk1,X1))) = converse(top),
inference(step,[status(thm)],[t45456,t27]) ).
cnf(t45458,plain,
join(X1,complement(composition(sk1,X1))) = top,
inference(step,[status(thm)],[t45457,t771]) ).
cnf(t19849,plain,
join(X1,complement(composition(sk1,X1))) = top,
inference(orient,[status(thm)],[t45458]) ).
cnf(t19870,plain,
meet(X1,composition(sk1,complement(X1))) = complement(top),
inference(cp,[status(thm)],[t105,t19849]) ).
cnf(t45465,plain,
meet(X1,composition(sk1,complement(X1))) = zero,
inference(step,[status(thm)],[t19870,t149]) ).
cnf(t19926,plain,
meet(X1,composition(sk1,complement(X1))) = zero,
inference(orient,[status(thm)],[t45465]) ).
cnf(t28859,plain,
composition(sk1,complement(complement(X1))) = join(meet(composition(sk1,complement(complement(X1))),X1),zero),
inference(cp,[status(thm)],[t28824,t19926]) ).
cnf(t152,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t105,t149]) ).
cnf(t438,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t152]) ).
cnf(t45174,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t438,t12365]) ).
cnf(t12415,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t45174]) ).
cnf(t12464,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t12415]) ).
cnf(t24488,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t24414,t472]) ).
cnf(t45665,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t24488,t59]) ).
cnf(t45666,plain,
X1 = join(meet(top,X1),meet(X1,complement(X1))),
inference(step,[status(thm)],[t45665,t12464]) ).
cnf(t45667,plain,
X1 = join(meet(top,X1),zero),
inference(step,[status(thm)],[t45666,t112]) ).
cnf(t45668,plain,
X1 = join(zero,meet(top,X1)),
inference(step,[status(thm)],[t45667,t59]) ).
cnf(t12405,plain,
complement(join(complement(X1),complement(X2))) = join(zero,meet(X1,X2)),
inference(cp,[status(thm)],[t12365,t105]) ).
cnf(t45198,plain,
meet(X1,X2) = join(zero,meet(X1,X2)),
inference(step,[status(thm)],[t12405,t105]) ).
cnf(t12671,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t45198]) ).
cnf(t45669,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t45668,t12671]) ).
cnf(t24747,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t45669]) ).
cnf(t45672,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t12464,t24747]) ).
cnf(t24750,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t45672]) ).
cnf(t46059,plain,
composition(sk1,X1) = join(meet(composition(sk1,complement(complement(X1))),X1),zero),
inference(step,[status(thm)],[t28859,t24750]) ).
cnf(t24703,plain,
meet(X1,X1) = join(zero,X1),
inference(cp,[status(thm)],[t12671,t24693]) ).
cnf(t45717,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t24703,t24693]) ).
cnf(t24919,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t45717]) ).
cnf(t24968,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t24919,t59]) ).
cnf(t25039,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t24968]) ).
cnf(t46060,plain,
composition(sk1,X1) = meet(composition(sk1,complement(complement(X1))),X1),
inference(step,[status(thm)],[t46059,t25039]) ).
cnf(t46061,plain,
composition(sk1,X1) = meet(X1,composition(sk1,complement(complement(X1)))),
inference(step,[status(thm)],[t46060,t141]) ).
cnf(t46062,plain,
composition(sk1,X1) = meet(X1,composition(sk1,X1)),
inference(step,[status(thm)],[t46061,t24750]) ).
cnf(t30431,plain,
meet(X1,composition(sk1,X1)) = composition(sk1,X1),
inference(orient,[status(thm)],[t46062]) ).
cnf(t30460,plain,
composition(meet(sk1,converse(one)),meet(one,converse(sk1))) = join(composition(sk1,one),composition(meet(sk1,converse(one)),meet(one,converse(sk1)))),
inference(cp,[status(thm)],[t8865,t30431]) ).
cnf(t46063,plain,
composition(meet(sk1,one),meet(one,converse(sk1))) = join(composition(sk1,one),composition(meet(sk1,converse(one)),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t30460,t273]) ).
cnf(t25991,plain,
meet(complement(one),sk1) = complement(top),
inference(cp,[status(thm)],[t25971,t626]) ).
cnf(t45781,plain,
meet(sk1,complement(one)) = complement(top),
inference(step,[status(thm)],[t25991,t141]) ).
cnf(t45782,plain,
meet(sk1,complement(one)) = zero,
inference(step,[status(thm)],[t45781,t149]) ).
cnf(t26053,plain,
meet(sk1,complement(one)) = zero,
inference(orient,[status(thm)],[t45782]) ).
cnf(t26950,plain,
sk1 = join(zero,meet(sk1,complement(complement(one)))),
inference(cp,[status(thm)],[t26941,t26053]) ).
cnf(t45841,plain,
sk1 = meet(sk1,complement(complement(one))),
inference(step,[status(thm)],[t26950,t12671]) ).
cnf(t45842,plain,
sk1 = meet(sk1,one),
inference(step,[status(thm)],[t45841,t24750]) ).
cnf(t27003,plain,
meet(sk1,one) = sk1,
inference(orient,[status(thm)],[t45842]) ).
cnf(t46064,plain,
composition(sk1,meet(one,converse(sk1))) = join(composition(sk1,one),composition(meet(sk1,converse(one)),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t46063,t27003]) ).
cnf(t353,plain,
join(converse(X1),one) = converse(join(X1,one)),
inference(cp,[status(thm)],[t349,t273]) ).
cnf(t44614,plain,
join(one,converse(X1)) = converse(join(X1,one)),
inference(step,[status(thm)],[t353,t59]) ).
cnf(t366,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t44614]) ).
cnf(t367,plain,
join(one,converse(sk1)) = converse(one),
inference(cp,[status(thm)],[t366,t103]) ).
cnf(t44615,plain,
join(one,converse(sk1)) = one,
inference(step,[status(thm)],[t367,t273]) ).
cnf(t380,plain,
join(one,converse(sk1)) = one,
inference(orient,[status(thm)],[t44615]) ).
cnf(t381,plain,
join(one,join(converse(sk1),X1)) = join(one,X1),
inference(cp,[status(thm)],[t61,t380]) ).
cnf(t1093,plain,
join(one,join(converse(sk1),X1)) = join(one,X1),
inference(orient,[status(thm)],[t381]) ).
cnf(t1102,plain,
join(one,complement(converse(sk1))) = join(one,top),
inference(cp,[status(thm)],[t1093,t66]) ).
cnf(t44698,plain,
join(one,complement(converse(sk1))) = top,
inference(step,[status(thm)],[t1102,t583]) ).
cnf(t1109,plain,
join(one,complement(converse(sk1))) = top,
inference(orient,[status(thm)],[t44698]) ).
cnf(t25992,plain,
meet(complement(one),converse(sk1)) = complement(top),
inference(cp,[status(thm)],[t25971,t1109]) ).
cnf(t45878,plain,
meet(converse(sk1),complement(one)) = complement(top),
inference(step,[status(thm)],[t25992,t141]) ).
cnf(t45879,plain,
meet(converse(sk1),complement(one)) = zero,
inference(step,[status(thm)],[t45878,t149]) ).
cnf(t27180,plain,
meet(converse(sk1),complement(one)) = zero,
inference(orient,[status(thm)],[t45879]) ).
cnf(t27181,plain,
converse(sk1) = join(zero,meet(converse(sk1),complement(complement(one)))),
inference(cp,[status(thm)],[t26941,t27180]) ).
cnf(t45880,plain,
converse(sk1) = meet(converse(sk1),complement(complement(one))),
inference(step,[status(thm)],[t27181,t12671]) ).
cnf(t45881,plain,
converse(sk1) = meet(converse(sk1),one),
inference(step,[status(thm)],[t45880,t24750]) ).
cnf(t45882,plain,
converse(sk1) = meet(one,converse(sk1)),
inference(step,[status(thm)],[t45881,t141]) ).
cnf(t27183,plain,
meet(one,converse(sk1)) = converse(sk1),
inference(orient,[status(thm)],[t45882]) ).
cnf(t46065,plain,
composition(sk1,converse(sk1)) = join(composition(sk1,one),composition(meet(sk1,converse(one)),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t46064,t27183]) ).
cnf(t46066,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(meet(sk1,converse(one)),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t46065,t23]) ).
cnf(t46067,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(meet(sk1,one),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t46066,t273]) ).
cnf(t46068,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(sk1,meet(one,converse(sk1)))),
inference(step,[status(thm)],[t46067,t27003]) ).
cnf(t46069,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(sk1,converse(sk1))),
inference(step,[status(thm)],[t46068,t27183]) ).
cnf(t734,plain,
join(X1,converse(composition(sk1,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t322,t729]) ).
cnf(t44696,plain,
join(X1,composition(X1,converse(sk1))) = converse(converse(X1)),
inference(step,[status(thm)],[t734,t240]) ).
cnf(t44697,plain,
join(X1,composition(X1,converse(sk1))) = X1,
inference(step,[status(thm)],[t44696,t27]) ).
cnf(t1033,plain,
join(X1,composition(X1,converse(sk1))) = X1,
inference(orient,[status(thm)],[t44697]) ).
cnf(t46070,plain,
composition(sk1,converse(sk1)) = sk1,
inference(step,[status(thm)],[t46069,t1033]) ).
cnf(t30475,plain,
composition(sk1,converse(sk1)) = sk1,
inference(orient,[status(thm)],[t46070]) ).
cnf(t30502,plain,
composition(sk1,converse(sk1)) = converse(sk1),
inference(cp,[status(thm)],[t240,t30475]) ).
cnf(t46072,plain,
sk1 = converse(sk1),
inference(step,[status(thm)],[t30502,t30475]) ).
cnf(t30539,plain,
converse(sk1) = sk1,
inference(orient,[status(thm)],[t46072]) ).
cnf(t46077,plain,
composition(sk1,sk1) = sk1,
inference(step,[status(thm)],[t30475,t30539]) ).
cnf(t30630,plain,
composition(sk1,sk1) = sk1,
inference(rw,[status(thm)],[t46077]) ).
cnf(t30664,plain,
composition(sk1,sk1) = sk1,
inference(orient,[status(thm)],[t30630]) ).
cnf(t30669,plain,
composition(sk1,composition(sk1,X1)) = composition(sk1,X1),
inference(cp,[status(thm)],[t28,t30664]) ).
cnf(t30704,plain,
composition(sk1,composition(sk1,X1)) = composition(sk1,X1),
inference(orient,[status(thm)],[t30669]) ).
cnf(t30713,plain,
composition(sk1,sk3) = composition(sk1,sFlat1),
inference(cp,[status(thm)],[t30704,t49]) ).
cnf(t46124,plain,
sFlat1 = composition(sk1,sFlat1),
inference(step,[status(thm)],[t30713,t49]) ).
cnf(t30753,plain,
composition(sk1,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t46124]) ).
cnf(t30754,plain,
composition(sk1,join(sFlat1,X1)) = join(sFlat1,composition(sk1,X1)),
inference(cp,[status(thm)],[t14471,t30753]) ).
cnf(t31883,plain,
composition(sk1,join(sFlat1,X1)) = join(sFlat1,composition(sk1,X1)),
inference(orient,[status(thm)],[t30754]) ).
cnf(t1384,plain,
meet(join(complement(X1),complement(X2)),top) = complement(join(meet(X1,X2),zero)),
inference(cp,[status(thm)],[t1371,t149]) ).
cnf(t44812,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(meet(X1,X2),zero)),
inference(step,[status(thm)],[t1384,t141]) ).
cnf(t44813,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t44812,t59]) ).
cnf(t2843,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t44813]) ).
cnf(t45199,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t2843,t12671]) ).
cnf(t12672,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t45199]) ).
cnf(t45686,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t12672,t24747]) ).
cnf(t24796,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t45686]) ).
cnf(t27794,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t24796]) ).
cnf(t27808,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t27794,t24750]) ).
cnf(t28103,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t27808]) ).
cnf(t28117,plain,
join(sFlat1,complement(X1)) = complement(meet(sFlat2,X1)),
inference(cp,[status(thm)],[t28103,t119]) ).
cnf(t28203,plain,
complement(meet(sFlat2,X1)) = join(sFlat1,complement(X1)),
inference(orient,[status(thm)],[t28117]) ).
cnf(t28205,plain,
join(sFlat1,complement(X1)) = complement(meet(X1,sFlat2)),
inference(cp,[status(thm)],[t28203,t141]) ).
cnf(t28286,plain,
complement(meet(X1,sFlat2)) = join(sFlat1,complement(X1)),
inference(orient,[status(thm)],[t28205]) ).
cnf(t28287,plain,
join(sFlat1,complement(sFlat0)) = complement(sFlat3),
inference(cp,[status(thm)],[t28286,t136]) ).
cnf(t28326,plain,
join(sFlat1,complement(sFlat0)) = complement(sFlat3),
inference(orient,[status(thm)],[t28287]) ).
cnf(t31887,plain,
join(sFlat1,composition(sk1,complement(sFlat0))) = composition(sk1,complement(sFlat3)),
inference(cp,[status(thm)],[t31883,t28326]) ).
cnf(t333,plain,
composition(converse(X1),join(converse(X2),X3)) = converse(composition(join(X2,converse(X3)),X1)),
inference(cp,[status(thm)],[t250,t322]) ).
cnf(t3875,plain,
converse(composition(join(X1,converse(X2)),X3)) = composition(converse(X3),join(converse(X1),X2)),
inference(orient,[status(thm)],[t333]) ).
cnf(t12969,plain,
composition(join(converse(sk3),X1),converse(sk1)) = join(converse(sFlat1),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t12893,t49]) ).
cnf(t13768,plain,
composition(join(converse(sk3),X1),converse(sk1)) = join(converse(sFlat1),composition(X1,converse(sk1))),
inference(orient,[status(thm)],[t12969]) ).
cnf(t13832,plain,
composition(converse(converse(sk1)),join(converse(converse(sk3)),X1)) = converse(join(converse(sFlat1),composition(converse(X1),converse(sk1)))),
inference(cp,[status(thm)],[t3875,t13768]) ).
cnf(t45234,plain,
composition(sk1,join(converse(converse(sk3)),X1)) = converse(join(converse(sFlat1),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t13832,t27]) ).
cnf(t45235,plain,
composition(sk1,join(sk3,X1)) = converse(join(converse(sFlat1),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t45234,t27]) ).
cnf(t45236,plain,
composition(sk1,join(sk3,X1)) = join(sFlat1,converse(composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t45235,t322]) ).
cnf(t45237,plain,
composition(sk1,join(sk3,X1)) = join(sFlat1,composition(converse(converse(sk1)),X1)),
inference(step,[status(thm)],[t45236,t250]) ).
cnf(t45238,plain,
composition(sk1,join(sk3,X1)) = join(sFlat1,composition(sk1,X1)),
inference(step,[status(thm)],[t45237,t27]) ).
cnf(t13860,plain,
composition(sk1,join(sk3,X1)) = join(sFlat1,composition(sk1,X1)),
inference(orient,[status(thm)],[t45238]) ).
cnf(t1375,plain,
meet(join(complement(sFlat0),complement(sFlat4)),X1) = complement(join(sFlat5,complement(X1))),
inference(cp,[status(thm)],[t1371,t140]) ).
cnf(t2267,plain,
meet(join(complement(sFlat0),complement(sFlat4)),X1) = complement(join(sFlat5,complement(X1))),
inference(orient,[status(thm)],[t1375]) ).
cnf(t24701,plain,
join(complement(sFlat0),complement(sFlat4)) = complement(join(sFlat5,complement(join(complement(sFlat0),complement(sFlat4))))),
inference(cp,[status(thm)],[t24693,t2267]) ).
cnf(t45788,plain,
join(complement(sFlat0),complement(sFlat4)) = complement(join(sFlat5,meet(sFlat0,sFlat4))),
inference(step,[status(thm)],[t24701,t105]) ).
cnf(t45789,plain,
join(complement(sFlat0),complement(sFlat4)) = complement(join(sFlat5,sFlat5)),
inference(step,[status(thm)],[t45788,t140]) ).
cnf(t482,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t472,t105]) ).
cnf(t44784,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t482,t105]) ).
cnf(t44785,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t44784,t105]) ).
cnf(t2318,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t44785]) ).
cnf(t2320,plain,
meet(sFlat0,sFlat4) = join(sFlat5,meet(sFlat0,sFlat4)),
inference(cp,[status(thm)],[t2318,t140]) ).
cnf(t44788,plain,
sFlat5 = join(sFlat5,meet(sFlat0,sFlat4)),
inference(step,[status(thm)],[t2320,t140]) ).
cnf(t44789,plain,
sFlat5 = join(sFlat5,sFlat5),
inference(step,[status(thm)],[t44788,t140]) ).
cnf(t2324,plain,
join(sFlat5,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t44789]) ).
cnf(t45790,plain,
join(complement(sFlat0),complement(sFlat4)) = complement(sFlat5),
inference(step,[status(thm)],[t45789,t2324]) ).
cnf(t129,plain,
meet(sk3,X1) = complement(join(sFlat4,complement(X1))),
inference(cp,[status(thm)],[t105,t126]) ).
cnf(t209,plain,
complement(join(sFlat4,complement(X1))) = meet(sk3,X1),
inference(orient,[status(thm)],[t129]) ).
cnf(t19894,plain,
meet(sk3,composition(sk1,sFlat4)) = complement(top),
inference(cp,[status(thm)],[t209,t19849]) ).
cnf(t45461,plain,
meet(sk3,composition(sk1,sFlat4)) = zero,
inference(step,[status(thm)],[t19894,t149]) ).
cnf(t19909,plain,
meet(sk3,composition(sk1,sFlat4)) = zero,
inference(orient,[status(thm)],[t45461]) ).
cnf(t24446,plain,
sk3 = join(zero,complement(join(complement(sk3),composition(sk1,sFlat4)))),
inference(cp,[status(thm)],[t24414,t19909]) ).
cnf(t45689,plain,
sk3 = complement(join(complement(sk3),composition(sk1,sFlat4))),
inference(step,[status(thm)],[t24446,t12365]) ).
cnf(t45690,plain,
sk3 = complement(join(sFlat4,composition(sk1,sFlat4))),
inference(step,[status(thm)],[t45689,t126]) ).
cnf(t45691,plain,
sk3 = complement(sFlat4),
inference(step,[status(thm)],[t45690,t729]) ).
cnf(t24799,plain,
complement(sFlat4) = sk3,
inference(orient,[status(thm)],[t45691]) ).
cnf(t45791,plain,
join(complement(sFlat0),sk3) = complement(sFlat5),
inference(step,[status(thm)],[t45790,t24799]) ).
cnf(t45792,plain,
join(sk3,complement(sFlat0)) = complement(sFlat5),
inference(step,[status(thm)],[t45791,t59]) ).
cnf(t26094,plain,
join(sk3,complement(sFlat0)) = complement(sFlat5),
inference(orient,[status(thm)],[t45792]) ).
cnf(t26095,plain,
join(sFlat1,composition(sk1,complement(sFlat0))) = composition(sk1,complement(sFlat5)),
inference(cp,[status(thm)],[t13860,t26094]) ).
cnf(t36482,plain,
join(sFlat1,composition(sk1,complement(sFlat0))) = composition(sk1,complement(sFlat5)),
inference(orient,[status(thm)],[t26095]) ).
cnf(t46960,plain,
composition(sk1,complement(sFlat5)) = composition(sk1,complement(sFlat3)),
inference(step,[status(thm)],[t31887,t36482]) ).
cnf(t42175,plain,
composition(sk1,complement(sFlat5)) = composition(sk1,complement(sFlat3)),
inference(orient,[status(thm)],[t46960]) ).
cnf(t42181,plain,
composition(sk1,join(complement(sFlat5),X1)) = join(composition(sk1,complement(sFlat3)),composition(sk1,X1)),
inference(cp,[status(thm)],[t14471,t42175]) ).
cnf(t47108,plain,
composition(sk1,join(complement(sFlat5),X1)) = composition(sk1,join(complement(sFlat3),X1)),
inference(step,[status(thm)],[t42181,t14471]) ).
cnf(t44393,plain,
composition(sk1,join(complement(sFlat5),X1)) = composition(sk1,join(complement(sFlat3),X1)),
inference(orient,[status(thm)],[t47108]) ).
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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t77,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(t86,plain,
meet(composition(converse(X1),meet(X2,composition(converse(converse(X1)),X3))),X3) = join(meet(composition(converse(X1),X2),X3),meet(composition(converse(X1),meet(X2,composition(X1,X3))),X3)),
inference(cp,[status(thm)],[t77,t27]) ).
cnf(t46822,plain,
meet(X3,composition(converse(X1),meet(X2,composition(converse(converse(X1)),X3)))) = join(meet(composition(converse(X1),X2),X3),meet(composition(converse(X1),meet(X2,composition(X1,X3))),X3)),
inference(step,[status(thm)],[t86,t141]) ).
cnf(t46823,plain,
meet(X3,composition(converse(X1),meet(X2,composition(X1,X3)))) = join(meet(composition(converse(X1),X2),X3),meet(composition(converse(X1),meet(X2,composition(X1,X3))),X3)),
inference(step,[status(thm)],[t46822,t27]) ).
cnf(t46824,plain,
meet(X3,composition(converse(X1),meet(X2,composition(X1,X3)))) = join(meet(composition(converse(X1),X2),X3),meet(X3,composition(converse(X1),meet(X2,composition(X1,X3))))),
inference(step,[status(thm)],[t46823,t141]) ).
cnf(t40396,plain,
join(meet(composition(converse(X1),X2),X3),meet(X3,composition(converse(X1),meet(X2,composition(X1,X3))))) = meet(X3,composition(converse(X1),meet(X2,composition(X1,X3)))),
inference(orient,[status(thm)],[t46824]) ).
cnf(t110,plain,
meet(X1,join(complement(X2),complement(X3))) = complement(join(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t105,t105]) ).
cnf(t1412,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,join(complement(X2),complement(X3))),
inference(orient,[status(thm)],[t110]) ).
cnf(t24711,plain,
meet(X1,join(complement(X2),complement(X2))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t1412,t24693]) ).
cnf(t45774,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t24711,t472]) ).
cnf(t25822,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t45774]) ).
cnf(t27831,plain,
join(top,complement(X1)) = join(X2,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t606,t27794]) ).
cnf(t45927,plain,
top = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t27831,t561]) ).
cnf(t27860,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t45927]) ).
cnf(t27874,plain,
meet(X1,complement(complement(meet(X2,complement(X1))))) = complement(top),
inference(cp,[status(thm)],[t25822,t27860]) ).
cnf(t45946,plain,
meet(X1,meet(X2,complement(X1))) = complement(top),
inference(step,[status(thm)],[t27874,t24750]) ).
cnf(t45947,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t45946,t149]) ).
cnf(t28013,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t45947]) ).
cnf(t28825,plain,
X1 = join(zero,meet(complement(meet(X2,complement(X1))),X1)),
inference(cp,[status(thm)],[t28824,t28013]) ).
cnf(t45983,plain,
X1 = meet(complement(meet(X2,complement(X1))),X1),
inference(step,[status(thm)],[t28825,t12671]) ).
cnf(t45984,plain,
X1 = meet(X1,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t45983,t141]) ).
cnf(t27823,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t27794,t24750]) ).
cnf(t28334,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t27823]) ).
cnf(t45985,plain,
X1 = meet(X1,join(complement(X2),X1)),
inference(step,[status(thm)],[t45984,t28334]) ).
cnf(t29343,plain,
meet(X1,join(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t45985]) ).
cnf(t29423,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t29343,t24750]) ).
cnf(t29440,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t29423]) ).
cnf(t20179,plain,
join(composition(sk1,X1),X2) = join(X2,composition(sk1,join(X2,X1))),
inference(cp,[status(thm)],[t20175,t14471]) ).
cnf(t20700,plain,
join(X1,composition(sk1,join(X1,X2))) = join(composition(sk1,X2),X1),
inference(orient,[status(thm)],[t20179]) ).
cnf(t24706,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t2318,t24693]) ).
cnf(t45701,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t24706,t24693]) ).
cnf(t45702,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t45701,t24693]) ).
cnf(t24845,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t45702]) ).
cnf(t65,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t61,t59]) ).
cnf(t44616,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t65,t61]) ).
cnf(t388,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t44616]) ).
cnf(t24847,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t24845,t388]) ).
cnf(t45859,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t24847,t61]) ).
cnf(t45860,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t45859,t24845]) ).
cnf(t27089,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t45860]) ).
cnf(t24458,plain,
sFlat0 = join(sFlat5,complement(join(complement(sFlat0),sFlat4))),
inference(cp,[status(thm)],[t24414,t140]) ).
cnf(t45806,plain,
sFlat0 = join(sFlat5,meet(sFlat0,complement(sFlat4))),
inference(step,[status(thm)],[t24458,t25822]) ).
cnf(t45807,plain,
sFlat0 = join(sFlat5,meet(sFlat0,sk3)),
inference(step,[status(thm)],[t45806,t24799]) ).
cnf(t26160,plain,
join(sFlat5,meet(sFlat0,sk3)) = sFlat0,
inference(orient,[status(thm)],[t45807]) ).
cnf(t27093,plain,
join(sFlat5,meet(sFlat0,sk3)) = join(sFlat5,sFlat0),
inference(cp,[status(thm)],[t27089,t26160]) ).
cnf(t45864,plain,
sFlat0 = join(sFlat5,sFlat0),
inference(step,[status(thm)],[t27093,t26160]) ).
cnf(t45865,plain,
sFlat0 = join(sFlat0,sFlat5),
inference(step,[status(thm)],[t45864,t59]) ).
cnf(t27107,plain,
join(sFlat0,sFlat5) = sFlat0,
inference(orient,[status(thm)],[t45865]) ).
cnf(t27109,plain,
join(composition(sk1,sFlat5),sFlat0) = join(sFlat0,composition(sk1,sFlat0)),
inference(cp,[status(thm)],[t20700,t27107]) ).
cnf(t45872,plain,
join(sFlat0,composition(sk1,sFlat5)) = join(sFlat0,composition(sk1,sFlat0)),
inference(step,[status(thm)],[t27109,t59]) ).
cnf(t45873,plain,
join(sFlat0,composition(sk1,sFlat5)) = sFlat0,
inference(step,[status(thm)],[t45872,t729]) ).
cnf(t27163,plain,
join(sFlat0,composition(sk1,sFlat5)) = sFlat0,
inference(orient,[status(thm)],[t45873]) ).
cnf(t29506,plain,
composition(sk1,sFlat5) = meet(composition(sk1,sFlat5),sFlat0),
inference(cp,[status(thm)],[t29440,t27163]) ).
cnf(t46290,plain,
composition(sk1,sFlat5) = meet(sFlat0,composition(sk1,sFlat5)),
inference(step,[status(thm)],[t29506,t141]) ).
cnf(t33859,plain,
meet(sFlat0,composition(sk1,sFlat5)) = composition(sk1,sFlat5),
inference(orient,[status(thm)],[t46290]) ).
cnf(t40522,plain,
meet(sFlat5,composition(converse(sk1),meet(sFlat0,composition(sk1,sFlat5)))) = join(meet(composition(converse(sk1),sFlat0),sFlat5),meet(sFlat5,composition(converse(sk1),composition(sk1,sFlat5)))),
inference(cp,[status(thm)],[t40396,t33859]) ).
cnf(t46836,plain,
meet(sFlat5,composition(sk1,meet(sFlat0,composition(sk1,sFlat5)))) = join(meet(composition(converse(sk1),sFlat0),sFlat5),meet(sFlat5,composition(converse(sk1),composition(sk1,sFlat5)))),
inference(step,[status(thm)],[t40522,t30539]) ).
cnf(t46837,plain,
meet(sFlat5,composition(sk1,composition(sk1,sFlat5))) = join(meet(composition(converse(sk1),sFlat0),sFlat5),meet(sFlat5,composition(converse(sk1),composition(sk1,sFlat5)))),
inference(step,[status(thm)],[t46836,t33859]) ).
cnf(t46838,plain,
meet(sFlat5,composition(sk1,sFlat5)) = join(meet(composition(converse(sk1),sFlat0),sFlat5),meet(sFlat5,composition(converse(sk1),composition(sk1,sFlat5)))),
inference(step,[status(thm)],[t46837,t30704]) ).
cnf(t46839,plain,
composition(sk1,sFlat5) = join(meet(composition(converse(sk1),sFlat0),sFlat5),meet(sFlat5,composition(converse(sk1),composition(sk1,sFlat5)))),
inference(step,[status(thm)],[t46838,t30431]) ).
cnf(t46840,plain,
composition(sk1,sFlat5) = join(meet(sFlat5,composition(converse(sk1),sFlat0)),meet(sFlat5,composition(converse(sk1),composition(sk1,sFlat5)))),
inference(step,[status(thm)],[t46839,t141]) ).
cnf(t46841,plain,
composition(sk1,sFlat5) = join(meet(sFlat5,composition(sk1,sFlat0)),meet(sFlat5,composition(converse(sk1),composition(sk1,sFlat5)))),
inference(step,[status(thm)],[t46840,t30539]) ).
cnf(t30714,plain,
composition(sk1,sk2) = composition(sk1,sFlat0),
inference(cp,[status(thm)],[t30704,t54]) ).
cnf(t46128,plain,
sFlat0 = composition(sk1,sFlat0),
inference(step,[status(thm)],[t30714,t54]) ).
cnf(t30792,plain,
composition(sk1,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t46128]) ).
cnf(t46842,plain,
composition(sk1,sFlat5) = join(meet(sFlat5,sFlat0),meet(sFlat5,composition(converse(sk1),composition(sk1,sFlat5)))),
inference(step,[status(thm)],[t46841,t30792]) ).
cnf(t46843,plain,
composition(sk1,sFlat5) = join(meet(sFlat0,sFlat5),meet(sFlat5,composition(converse(sk1),composition(sk1,sFlat5)))),
inference(step,[status(thm)],[t46842,t141]) ).
cnf(t26105,plain,
join(top,sk3) = join(sFlat0,complement(sFlat5)),
inference(cp,[status(thm)],[t606,t26094]) ).
cnf(t607,plain,
join(top,sk3) = join(top,complement(sFlat4)),
inference(cp,[status(thm)],[t606,t437]) ).
cnf(t44644,plain,
join(top,sk3) = top,
inference(step,[status(thm)],[t607,t561]) ).
cnf(t624,plain,
join(top,sk3) = top,
inference(orient,[status(thm)],[t44644]) ).
cnf(t45797,plain,
top = join(sFlat0,complement(sFlat5)),
inference(step,[status(thm)],[t26105,t624]) ).
cnf(t26115,plain,
join(sFlat0,complement(sFlat5)) = top,
inference(orient,[status(thm)],[t45797]) ).
cnf(t26116,plain,
meet(complement(sFlat0),sFlat5) = complement(top),
inference(cp,[status(thm)],[t25971,t26115]) ).
cnf(t45798,plain,
meet(sFlat5,complement(sFlat0)) = complement(top),
inference(step,[status(thm)],[t26116,t141]) ).
cnf(t45799,plain,
meet(sFlat5,complement(sFlat0)) = zero,
inference(step,[status(thm)],[t45798,t149]) ).
cnf(t26118,plain,
meet(sFlat5,complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t45799]) ).
cnf(t26949,plain,
sFlat5 = join(zero,meet(sFlat5,complement(complement(sFlat0)))),
inference(cp,[status(thm)],[t26941,t26118]) ).
cnf(t45838,plain,
sFlat5 = meet(sFlat5,complement(complement(sFlat0))),
inference(step,[status(thm)],[t26949,t12671]) ).
cnf(t45839,plain,
sFlat5 = meet(sFlat5,sFlat0),
inference(step,[status(thm)],[t45838,t24750]) ).
cnf(t45840,plain,
sFlat5 = meet(sFlat0,sFlat5),
inference(step,[status(thm)],[t45839,t141]) ).
cnf(t26998,plain,
meet(sFlat0,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t45840]) ).
cnf(t46844,plain,
composition(sk1,sFlat5) = join(sFlat5,meet(sFlat5,composition(converse(sk1),composition(sk1,sFlat5)))),
inference(step,[status(thm)],[t46843,t26998]) ).
cnf(t27091,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t27089,t26941]) ).
cnf(t45868,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t27091,t26941]) ).
cnf(t45869,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t45868,t59]) ).
cnf(t27116,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t45869]) ).
cnf(t46845,plain,
composition(sk1,sFlat5) = sFlat5,
inference(step,[status(thm)],[t46844,t27116]) ).
cnf(t40669,plain,
composition(sk1,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t46845]) ).
cnf(t40672,plain,
composition(sk1,join(X1,sFlat5)) = join(composition(sk1,X1),sFlat5),
inference(cp,[status(thm)],[t14471,t40669]) ).
cnf(t47019,plain,
composition(sk1,join(X1,sFlat5)) = join(sFlat5,composition(sk1,X1)),
inference(step,[status(thm)],[t40672,t59]) ).
cnf(t43218,plain,
composition(sk1,join(X1,sFlat5)) = join(sFlat5,composition(sk1,X1)),
inference(orient,[status(thm)],[t47019]) ).
cnf(t44394,plain,
composition(sk1,join(complement(sFlat3),sFlat5)) = join(sFlat5,composition(sk1,complement(sFlat5))),
inference(cp,[status(thm)],[t44393,t43218]) ).
cnf(t47109,plain,
join(sFlat5,composition(sk1,complement(sFlat3))) = join(sFlat5,composition(sk1,complement(sFlat5))),
inference(step,[status(thm)],[t44394,t43218]) ).
cnf(t20747,plain,
join(composition(sk1,complement(X1)),X1) = join(X1,composition(sk1,top)),
inference(cp,[status(thm)],[t20700,t66]) ).
cnf(t45510,plain,
join(X1,composition(sk1,complement(X1))) = join(X1,composition(sk1,top)),
inference(step,[status(thm)],[t20747,t59]) ).
cnf(t20993,plain,
join(X1,composition(sk1,complement(X1))) = join(X1,composition(sk1,top)),
inference(orient,[status(thm)],[t45510]) ).
cnf(t47110,plain,
join(sFlat5,composition(sk1,complement(sFlat3))) = join(sFlat5,composition(sk1,top)),
inference(step,[status(thm)],[t47109,t20993]) ).
cnf(t40671,plain,
composition(sk1,join(sFlat5,X1)) = join(sFlat5,composition(sk1,X1)),
inference(cp,[status(thm)],[t14471,t40669]) ).
cnf(t43113,plain,
composition(sk1,join(sFlat5,X1)) = join(sFlat5,composition(sk1,X1)),
inference(orient,[status(thm)],[t40671]) ).
cnf(t43152,plain,
join(sFlat5,composition(sk1,top)) = composition(sk1,top),
inference(cp,[status(thm)],[t43113,t583]) ).
cnf(t44133,plain,
join(sFlat5,composition(sk1,top)) = composition(sk1,top),
inference(orient,[status(thm)],[t43152]) ).
cnf(t47111,plain,
join(sFlat5,composition(sk1,complement(sFlat3))) = composition(sk1,top),
inference(step,[status(thm)],[t47110,t44133]) ).
cnf(t44532,plain,
join(sFlat5,composition(sk1,complement(sFlat3))) = composition(sk1,top),
inference(orient,[status(thm)],[t47111]) ).
cnf(t44538,plain,
join(sFlat5,complement(sFlat3)) = join(complement(sFlat3),composition(sk1,top)),
inference(cp,[status(thm)],[t20368,t44532]) ).
cnf(t26117,plain,
join(composition(sk1,complement(sFlat5)),sFlat0) = join(sFlat0,composition(sk1,top)),
inference(cp,[status(thm)],[t20700,t26115]) ).
cnf(t46563,plain,
join(sFlat0,composition(sk1,complement(sFlat5))) = join(sFlat0,composition(sk1,top)),
inference(step,[status(thm)],[t26117,t59]) ).
cnf(t12970,plain,
composition(join(converse(sk2),X1),converse(sk1)) = join(converse(sFlat0),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t12893,t54]) ).
cnf(t14097,plain,
composition(join(converse(sk2),X1),converse(sk1)) = join(converse(sFlat0),composition(X1,converse(sk1))),
inference(orient,[status(thm)],[t12970]) ).
cnf(t14161,plain,
composition(converse(converse(sk1)),join(converse(converse(sk2)),X1)) = converse(join(converse(sFlat0),composition(converse(X1),converse(sk1)))),
inference(cp,[status(thm)],[t3875,t14097]) ).
cnf(t45248,plain,
composition(sk1,join(converse(converse(sk2)),X1)) = converse(join(converse(sFlat0),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t14161,t27]) ).
cnf(t45249,plain,
composition(sk1,join(sk2,X1)) = converse(join(converse(sFlat0),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t45248,t27]) ).
cnf(t45250,plain,
composition(sk1,join(sk2,X1)) = join(sFlat0,converse(composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t45249,t322]) ).
cnf(t45251,plain,
composition(sk1,join(sk2,X1)) = join(sFlat0,composition(converse(converse(sk1)),X1)),
inference(step,[status(thm)],[t45250,t250]) ).
cnf(t45252,plain,
composition(sk1,join(sk2,X1)) = join(sFlat0,composition(sk1,X1)),
inference(step,[status(thm)],[t45251,t27]) ).
cnf(t14189,plain,
composition(sk1,join(sk2,X1)) = join(sFlat0,composition(sk1,X1)),
inference(orient,[status(thm)],[t45252]) ).
cnf(t14215,plain,
join(sFlat0,composition(sk1,top)) = composition(sk1,top),
inference(cp,[status(thm)],[t14189,t583]) ).
cnf(t14256,plain,
join(sFlat0,composition(sk1,top)) = composition(sk1,top),
inference(orient,[status(thm)],[t14215]) ).
cnf(t46564,plain,
join(sFlat0,composition(sk1,complement(sFlat5))) = composition(sk1,top),
inference(step,[status(thm)],[t46563,t14256]) ).
cnf(t38856,plain,
join(sFlat0,composition(sk1,complement(sFlat5))) = composition(sk1,top),
inference(orient,[status(thm)],[t46564]) ).
cnf(t46963,plain,
join(sFlat0,composition(sk1,complement(sFlat3))) = composition(sk1,top),
inference(step,[status(thm)],[t38856,t42175]) ).
cnf(t42241,plain,
join(sFlat0,composition(sk1,complement(sFlat3))) = composition(sk1,top),
inference(rw,[status(thm)],[t46963]) ).
cnf(t42243,plain,
join(sFlat0,composition(sk1,complement(sFlat3))) = composition(sk1,top),
inference(orient,[status(thm)],[t42241]) ).
cnf(t42247,plain,
join(sFlat0,complement(sFlat3)) = join(complement(sFlat3),composition(sk1,top)),
inference(cp,[status(thm)],[t20368,t42243]) ).
cnf(t27832,plain,
join(top,complement(X1)) = join(X2,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t535,t27794]) ).
cnf(t45932,plain,
top = join(X2,complement(meet(X2,X1))),
inference(step,[status(thm)],[t27832,t561]) ).
cnf(t27921,plain,
join(X1,complement(meet(X1,X2))) = top,
inference(orient,[status(thm)],[t45932]) ).
cnf(t27925,plain,
top = join(sFlat0,complement(sFlat3)),
inference(cp,[status(thm)],[t27921,t136]) ).
cnf(t27966,plain,
join(sFlat0,complement(sFlat3)) = top,
inference(orient,[status(thm)],[t27925]) ).
cnf(t47093,plain,
top = join(complement(sFlat3),composition(sk1,top)),
inference(step,[status(thm)],[t42247,t27966]) ).
cnf(t44130,plain,
join(complement(sFlat3),composition(sk1,top)) = top,
inference(orient,[status(thm)],[t47093]) ).
cnf(t47112,plain,
join(sFlat5,complement(sFlat3)) = top,
inference(step,[status(thm)],[t44538,t44130]) ).
cnf(t44543,plain,
join(sFlat5,complement(sFlat3)) = top,
inference(orient,[status(thm)],[t47112]) ).
cnf(t44544,plain,
meet(complement(sFlat5),sFlat3) = complement(top),
inference(cp,[status(thm)],[t25971,t44543]) ).
cnf(t47113,plain,
meet(sFlat3,complement(sFlat5)) = complement(top),
inference(step,[status(thm)],[t44544,t141]) ).
cnf(t47114,plain,
meet(sFlat3,complement(sFlat5)) = zero,
inference(step,[status(thm)],[t47113,t149]) ).
cnf(t44545,plain,
meet(sFlat3,complement(sFlat5)) = zero,
inference(orient,[status(thm)],[t47114]) ).
cnf(t44547,plain,
sFlat3 = join(zero,meet(sFlat3,complement(complement(sFlat5)))),
inference(cp,[status(thm)],[t26941,t44545]) ).
cnf(t47115,plain,
sFlat3 = meet(sFlat3,complement(complement(sFlat5))),
inference(step,[status(thm)],[t44547,t12671]) ).
cnf(t47116,plain,
sFlat3 = meet(sFlat3,sFlat5),
inference(step,[status(thm)],[t47115,t24750]) ).
cnf(t25972,plain,
meet(complement(X1),composition(sk1,X1)) = complement(top),
inference(cp,[status(thm)],[t25971,t19849]) ).
cnf(t46154,plain,
meet(complement(X1),composition(sk1,X1)) = zero,
inference(step,[status(thm)],[t25972,t149]) ).
cnf(t31735,plain,
meet(complement(X1),composition(sk1,X1)) = zero,
inference(orient,[status(thm)],[t46154]) ).
cnf(t42178,plain,
zero = meet(complement(complement(sFlat5)),composition(sk1,complement(sFlat3))),
inference(cp,[status(thm)],[t31735,t42175]) ).
cnf(t46969,plain,
zero = meet(sFlat5,composition(sk1,complement(sFlat3))),
inference(step,[status(thm)],[t42178,t24750]) ).
cnf(t42530,plain,
meet(sFlat5,composition(sk1,complement(sFlat3))) = zero,
inference(orient,[status(thm)],[t46969]) ).
cnf(t42533,plain,
meet(complement(sFlat3),composition(converse(sk1),meet(sFlat5,composition(sk1,complement(sFlat3))))) = join(meet(composition(converse(sk1),sFlat5),complement(sFlat3)),meet(complement(sFlat3),composition(converse(sk1),zero))),
inference(cp,[status(thm)],[t40396,t42530]) ).
cnf(t46970,plain,
meet(complement(sFlat3),composition(sk1,meet(sFlat5,composition(sk1,complement(sFlat3))))) = join(meet(composition(converse(sk1),sFlat5),complement(sFlat3)),meet(complement(sFlat3),composition(converse(sk1),zero))),
inference(step,[status(thm)],[t42533,t30539]) ).
cnf(t46971,plain,
meet(complement(sFlat3),composition(sk1,zero)) = join(meet(composition(converse(sk1),sFlat5),complement(sFlat3)),meet(complement(sFlat3),composition(converse(sk1),zero))),
inference(step,[status(thm)],[t46970,t42530]) ).
cnf(t34,plain,
composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t33,t23]) ).
cnf(t44806,plain,
composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t34,t273]) ).
cnf(t44807,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)],[t44806,t23]) ).
cnf(t44808,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)],[t44807,t273]) ).
cnf(t44809,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)],[t44808,t23]) ).
cnf(t649,plain,
join(X1,converse(composition(X2,converse(X1)))) = converse(composition(join(one,X2),converse(X1))),
inference(cp,[status(thm)],[t322,t628]) ).
cnf(t44790,plain,
join(X1,composition(X1,converse(X2))) = converse(composition(join(one,X2),converse(X1))),
inference(step,[status(thm)],[t649,t240]) ).
cnf(t44791,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,converse(join(one,X2))),
inference(step,[status(thm)],[t44790,t240]) ).
cnf(t325,plain,
join(one,converse(X1)) = converse(join(one,X1)),
inference(cp,[status(thm)],[t322,t273]) ).
cnf(t338,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t325]) ).
cnf(t44792,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(step,[status(thm)],[t44791,t338]) ).
cnf(t2325,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(orient,[status(thm)],[t44792]) ).
cnf(t2346,plain,
composition(X1,join(one,converse(converse(X2)))) = join(X1,composition(X1,X2)),
inference(cp,[status(thm)],[t2325,t27]) ).
cnf(t44799,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(step,[status(thm)],[t2346,t27]) ).
cnf(t2431,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(orient,[status(thm)],[t44799]) ).
cnf(t44810,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = composition(meet(X1,X2),join(one,meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t44809,t2431]) ).
cnf(t2677,plain,
composition(meet(X1,X2),join(one,meet(one,composition(converse(X1),X2)))) = composition(meet(X1,X2),meet(one,composition(converse(X1),X2))),
inference(orient,[status(thm)],[t44810]) ).
cnf(t26,plain,
join(complement(X1),complement(X2)) = join(complement(join(complement(join(complement(X1),complement(X2))),complement(complement(join(complement(X1),X2))))),complement(X1)),
inference(cp,[status(thm)],[t24,t24]) ).
cnf(t44650,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(join(complement(X1),complement(X2))),complement(complement(join(complement(X1),X2)))))),
inference(step,[status(thm)],[t26,t59]) ).
cnf(t44651,plain,
join(complement(X1),complement(X2)) = join(complement(X1),meet(join(complement(X1),complement(X2)),complement(join(complement(X1),X2)))),
inference(step,[status(thm)],[t44650,t105]) ).
cnf(t664,plain,
join(complement(X1),meet(join(complement(X1),complement(X2)),complement(join(complement(X1),X2)))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t44651]) ).
cnf(t678,plain,
join(complement(X1),complement(complement(X1))) = join(complement(X1),meet(top,complement(join(complement(X1),complement(X1))))),
inference(cp,[status(thm)],[t664,t66]) ).
cnf(t44732,plain,
top = join(complement(X1),meet(top,complement(join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t678,t66]) ).
cnf(t44733,plain,
top = join(complement(X1),meet(top,meet(X1,X1))),
inference(step,[status(thm)],[t44732,t105]) ).
cnf(t1715,plain,
join(complement(X1),meet(top,meet(X1,X1))) = top,
inference(orient,[status(thm)],[t44733]) ).
cnf(t1742,plain,
meet(X1,join(complement(top),complement(meet(X1,X1)))) = complement(top),
inference(cp,[status(thm)],[t1412,t1715]) ).
cnf(t44863,plain,
meet(X1,join(zero,complement(meet(X1,X1)))) = complement(top),
inference(step,[status(thm)],[t1742,t149]) ).
cnf(t44864,plain,
meet(X1,join(zero,complement(meet(X1,X1)))) = zero,
inference(step,[status(thm)],[t44863,t149]) ).
cnf(t4314,plain,
meet(X1,join(zero,complement(meet(X1,X1)))) = zero,
inference(orient,[status(thm)],[t44864]) ).
cnf(t71,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t69,t23]) ).
cnf(t1276,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t71]) ).
cnf(t1300,plain,
complement(one) = join(complement(one),composition(converse(top),zero)),
inference(cp,[status(thm)],[t1276,t149]) ).
cnf(t44709,plain,
complement(one) = join(complement(one),composition(top,zero)),
inference(step,[status(thm)],[t1300,t771]) ).
cnf(t994,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t69,t991]) ).
cnf(t44683,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t994,t149]) ).
cnf(t44684,plain,
zero = composition(join(converse(top),one),complement(top)),
inference(step,[status(thm)],[t44683,t650]) ).
cnf(t44685,plain,
zero = composition(join(one,converse(top)),complement(top)),
inference(step,[status(thm)],[t44684,t59]) ).
cnf(t44686,plain,
zero = composition(converse(top),complement(top)),
inference(step,[status(thm)],[t44685,t586]) ).
cnf(t44687,plain,
zero = composition(top,complement(top)),
inference(step,[status(thm)],[t44686,t771]) ).
cnf(t44688,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t44687,t149]) ).
cnf(t996,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t44688]) ).
cnf(t44710,plain,
complement(one) = join(complement(one),zero),
inference(step,[status(thm)],[t44709,t996]) ).
cnf(t44711,plain,
complement(one) = join(zero,complement(one)),
inference(step,[status(thm)],[t44710,t59]) ).
cnf(t1310,plain,
join(zero,complement(one)) = complement(one),
inference(orient,[status(thm)],[t44711]) ).
cnf(t1311,plain,
meet(top,one) = complement(complement(one)),
inference(cp,[status(thm)],[t438,t1310]) ).
cnf(t499,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t105,t472]) ).
cnf(t515,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t499]) ).
cnf(t44712,plain,
meet(top,one) = meet(one,one),
inference(step,[status(thm)],[t1311,t515]) ).
cnf(t1312,plain,
meet(one,one) = meet(top,one),
inference(orient,[status(thm)],[t44712]) ).
cnf(t4315,plain,
zero = meet(one,join(zero,complement(meet(top,one)))),
inference(cp,[status(thm)],[t4314,t1312]) ).
cnf(t9310,plain,
meet(one,join(zero,complement(meet(top,one)))) = zero,
inference(orient,[status(thm)],[t4315]) ).
cnf(t9311,plain,
composition(meet(one,join(zero,complement(meet(top,one)))),meet(one,composition(converse(one),join(zero,complement(meet(top,one)))))) = composition(zero,join(one,meet(one,composition(converse(one),join(zero,complement(meet(top,one))))))),
inference(cp,[status(thm)],[t2677,t9310]) ).
cnf(t45092,plain,
composition(zero,meet(one,composition(converse(one),join(zero,complement(meet(top,one)))))) = composition(zero,join(one,meet(one,composition(converse(one),join(zero,complement(meet(top,one))))))),
inference(step,[status(thm)],[t9311,t9310]) ).
cnf(t45093,plain,
composition(zero,meet(one,composition(one,join(zero,complement(meet(top,one)))))) = composition(zero,join(one,meet(one,composition(converse(one),join(zero,complement(meet(top,one))))))),
inference(step,[status(thm)],[t45092,t273]) ).
cnf(t45094,plain,
composition(zero,meet(one,join(zero,complement(meet(top,one))))) = composition(zero,join(one,meet(one,composition(converse(one),join(zero,complement(meet(top,one))))))),
inference(step,[status(thm)],[t45093,t284]) ).
cnf(t45095,plain,
composition(zero,zero) = composition(zero,join(one,meet(one,composition(converse(one),join(zero,complement(meet(top,one))))))),
inference(step,[status(thm)],[t45094,t9310]) ).
cnf(t45096,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(converse(one),join(zero,complement(meet(top,one))))))),
inference(step,[status(thm)],[t45095,t2431]) ).
cnf(t45097,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(one,join(zero,complement(meet(top,one))))))),
inference(step,[status(thm)],[t45096,t273]) ).
cnf(t45098,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,join(zero,complement(meet(top,one)))))),
inference(step,[status(thm)],[t45097,t284]) ).
cnf(t45099,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t45098,t9310]) ).
cnf(t999,plain,
composition(join(X1,top),zero) = join(composition(X1,zero),zero),
inference(cp,[status(thm)],[t30,t996]) ).
cnf(t44693,plain,
composition(top,zero) = join(composition(X1,zero),zero),
inference(step,[status(thm)],[t999,t583]) ).
cnf(t44694,plain,
zero = join(composition(X1,zero),zero),
inference(step,[status(thm)],[t44693,t996]) ).
cnf(t44695,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t44694,t59]) ).
cnf(t1022,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t44695]) ).
cnf(t45100,plain,
composition(zero,zero) = zero,
inference(step,[status(thm)],[t45099,t1022]) ).
cnf(t9313,plain,
composition(zero,zero) = zero,
inference(orient,[status(thm)],[t45100]) ).
cnf(t9314,plain,
composition(join(zero,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t30,t9313]) ).
cnf(t45101,plain,
composition(join(zero,X1),zero) = zero,
inference(step,[status(thm)],[t9314,t1022]) ).
cnf(t9332,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t45101]) ).
cnf(t9334,plain,
zero = composition(join(X1,zero),zero),
inference(cp,[status(thm)],[t9332,t59]) ).
cnf(t9401,plain,
composition(join(X1,zero),zero) = zero,
inference(orient,[status(thm)],[t9334]) ).
cnf(t45741,plain,
composition(X1,zero) = zero,
inference(step,[status(thm)],[t9401,t25039]) ).
cnf(t25065,plain,
composition(X1,zero) = zero,
inference(rw,[status(thm)],[t45741]) ).
cnf(t25066,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t25065]) ).
cnf(t46972,plain,
meet(complement(sFlat3),zero) = join(meet(composition(converse(sk1),sFlat5),complement(sFlat3)),meet(complement(sFlat3),composition(converse(sk1),zero))),
inference(step,[status(thm)],[t46971,t25066]) ).
cnf(t12378,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t12365,t66]) ).
cnf(t12418,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t12378]) ).
cnf(t12423,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t105,t12418]) ).
cnf(t45187,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t12423,t583]) ).
cnf(t45188,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t45187,t149]) ).
cnf(t12456,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t45188]) ).
cnf(t46973,plain,
zero = join(meet(composition(converse(sk1),sFlat5),complement(sFlat3)),meet(complement(sFlat3),composition(converse(sk1),zero))),
inference(step,[status(thm)],[t46972,t12456]) ).
cnf(t46974,plain,
zero = join(meet(complement(sFlat3),composition(converse(sk1),zero)),meet(composition(converse(sk1),sFlat5),complement(sFlat3))),
inference(step,[status(thm)],[t46973,t59]) ).
cnf(t46,plain,
composition(meet(converse(X1),composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(converse(X1)),X2))) = join(meet(converse(composition(X3,X1)),X2),composition(meet(converse(X1),composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(converse(X1)),X2)))),
inference(cp,[status(thm)],[t33,t40]) ).
cnf(t45321,plain,
composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(converse(converse(X1)),X2))) = join(meet(converse(composition(X3,X1)),X2),composition(meet(converse(X1),composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(converse(X1)),X2)))),
inference(step,[status(thm)],[t46,t27]) ).
cnf(t45322,plain,
composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(X1,X2))) = join(meet(converse(composition(X3,X1)),X2),composition(meet(converse(X1),composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(converse(X1)),X2)))),
inference(step,[status(thm)],[t45321,t27]) ).
cnf(t45323,plain,
composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(X1,X2))) = join(meet(converse(composition(X3,X1)),X2),composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(converse(converse(X1)),X2)))),
inference(step,[status(thm)],[t45322,t27]) ).
cnf(t45324,plain,
composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(X1,X2))) = join(meet(converse(composition(X3,X1)),X2),composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(X1,X2)))),
inference(step,[status(thm)],[t45323,t27]) ).
cnf(t16119,plain,
join(meet(converse(composition(X1,X2)),X3),composition(meet(converse(X2),composition(X3,X1)),meet(converse(X1),composition(X2,X3)))) = composition(meet(converse(X2),composition(X3,X1)),meet(converse(X1),composition(X2,X3))),
inference(orient,[status(thm)],[t45324]) ).
cnf(t2452,plain,
join(X1,composition(X1,X2)) = composition(X1,join(X2,one)),
inference(cp,[status(thm)],[t2431,t59]) ).
cnf(t4457,plain,
join(X1,composition(X1,X2)) = composition(X1,join(X2,one)),
inference(orient,[status(thm)],[t2452]) ).
cnf(t4493,plain,
composition(X1,composition(join(X2,one),X3)) = composition(join(X1,composition(X1,X2)),X3),
inference(cp,[status(thm)],[t28,t4457]) ).
cnf(t8610,plain,
composition(join(X1,composition(X1,X2)),X3) = composition(X1,composition(join(X2,one),X3)),
inference(orient,[status(thm)],[t4493]) ).
cnf(t997,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t842,t996]) ).
cnf(t1003,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t997]) ).
cnf(t8696,plain,
composition(converse(zero),composition(join(top,one),X1)) = composition(join(converse(zero),converse(zero)),X1),
inference(cp,[status(thm)],[t8610,t1003]) ).
cnf(t45052,plain,
composition(converse(zero),composition(top,X1)) = composition(join(converse(zero),converse(zero)),X1),
inference(step,[status(thm)],[t8696,t625]) ).
cnf(t45053,plain,
composition(converse(zero),composition(top,X1)) = composition(converse(join(zero,zero)),X1),
inference(step,[status(thm)],[t45052,t99]) ).
cnf(t480,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t472,t149]) ).
cnf(t44625,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t480,t149]) ).
cnf(t44626,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t44625,t149]) ).
cnf(t500,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t44626]) ).
cnf(t45054,plain,
composition(converse(zero),composition(top,X1)) = composition(converse(zero),X1),
inference(step,[status(thm)],[t45053,t500]) ).
cnf(t8777,plain,
composition(converse(zero),composition(top,X1)) = composition(converse(zero),X1),
inference(orient,[status(thm)],[t45054]) ).
cnf(t8626,plain,
composition(top,composition(join(X1,one),X2)) = composition(top,X2),
inference(cp,[status(thm)],[t8610,t2198]) ).
cnf(t9012,plain,
composition(top,composition(join(X1,one),X2)) = composition(top,X2),
inference(orient,[status(thm)],[t8626]) ).
cnf(t9017,plain,
composition(top,X1) = composition(top,join(X1,composition(one,X1))),
inference(cp,[status(thm)],[t9012,t628]) ).
cnf(t45063,plain,
composition(top,X1) = composition(top,join(X1,X1)),
inference(step,[status(thm)],[t9017,t284]) ).
cnf(t9041,plain,
composition(top,join(X1,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t45063]) ).
cnf(t9048,plain,
composition(converse(zero),join(X1,X1)) = composition(converse(zero),composition(top,X1)),
inference(cp,[status(thm)],[t8777,t9041]) ).
cnf(t45069,plain,
composition(converse(zero),join(X1,X1)) = composition(converse(zero),X1),
inference(step,[status(thm)],[t9048,t8777]) ).
cnf(t9139,plain,
composition(converse(zero),join(X1,X1)) = composition(converse(zero),X1),
inference(orient,[status(thm)],[t45069]) ).
cnf(t16264,plain,
composition(meet(converse(join(X1,X1)),composition(X2,converse(zero))),meet(converse(converse(zero)),composition(join(X1,X1),X2))) = join(meet(converse(composition(converse(zero),X1)),X2),composition(meet(converse(join(X1,X1)),composition(X2,converse(zero))),meet(converse(converse(zero)),composition(join(X1,X1),X2)))),
inference(cp,[status(thm)],[t16119,t9139]) ).
cnf(t45325,plain,
composition(meet(converse(join(X1,X1)),composition(X2,converse(zero))),meet(zero,composition(join(X1,X1),X2))) = join(meet(converse(composition(converse(zero),X1)),X2),composition(meet(converse(join(X1,X1)),composition(X2,converse(zero))),meet(converse(converse(zero)),composition(join(X1,X1),X2)))),
inference(step,[status(thm)],[t16264,t27]) ).
cnf(t12422,plain,
meet(zero,X1) = complement(join(top,complement(X1))),
inference(cp,[status(thm)],[t105,t12418]) ).
cnf(t45183,plain,
meet(zero,X1) = complement(top),
inference(step,[status(thm)],[t12422,t561]) ).
cnf(t45184,plain,
meet(zero,X1) = zero,
inference(step,[status(thm)],[t45183,t149]) ).
cnf(t12441,plain,
meet(zero,X1) = zero,
inference(orient,[status(thm)],[t45184]) ).
cnf(t45326,plain,
composition(meet(converse(join(X1,X1)),composition(X2,converse(zero))),zero) = join(meet(converse(composition(converse(zero),X1)),X2),composition(meet(converse(join(X1,X1)),composition(X2,converse(zero))),meet(converse(converse(zero)),composition(join(X1,X1),X2)))),
inference(step,[status(thm)],[t45325,t12441]) ).
cnf(t12676,plain,
zero = composition(meet(X1,X2),zero),
inference(cp,[status(thm)],[t9332,t12671]) ).
cnf(t13051,plain,
composition(meet(X1,X2),zero) = zero,
inference(orient,[status(thm)],[t12676]) ).
cnf(t45327,plain,
zero = join(meet(converse(composition(converse(zero),X1)),X2),composition(meet(converse(join(X1,X1)),composition(X2,converse(zero))),meet(converse(converse(zero)),composition(join(X1,X1),X2)))),
inference(step,[status(thm)],[t45326,t13051]) ).
cnf(t45328,plain,
zero = join(meet(composition(converse(X1),zero),X2),composition(meet(converse(join(X1,X1)),composition(X2,converse(zero))),meet(converse(converse(zero)),composition(join(X1,X1),X2)))),
inference(step,[status(thm)],[t45327,t250]) ).
cnf(t45329,plain,
zero = join(meet(composition(converse(X1),zero),X2),composition(meet(converse(join(X1,X1)),composition(X2,converse(zero))),meet(zero,composition(join(X1,X1),X2)))),
inference(step,[status(thm)],[t45328,t27]) ).
cnf(t45330,plain,
zero = join(meet(composition(converse(X1),zero),X2),composition(meet(converse(join(X1,X1)),composition(X2,converse(zero))),zero)),
inference(step,[status(thm)],[t45329,t12441]) ).
cnf(t45331,plain,
zero = join(meet(composition(converse(X1),zero),X2),zero),
inference(step,[status(thm)],[t45330,t13051]) ).
cnf(t45332,plain,
zero = join(zero,meet(composition(converse(X1),zero),X2)),
inference(step,[status(thm)],[t45331,t59]) ).
cnf(t45333,plain,
zero = meet(composition(converse(X1),zero),X2),
inference(step,[status(thm)],[t45332,t12671]) ).
cnf(t16646,plain,
meet(composition(converse(X1),zero),X2) = zero,
inference(orient,[status(thm)],[t45333]) ).
cnf(t16668,plain,
zero = meet(composition(X1,zero),X2),
inference(cp,[status(thm)],[t16646,t27]) ).
cnf(t16702,plain,
meet(composition(X1,zero),X2) = zero,
inference(orient,[status(thm)],[t16668]) ).
cnf(t16706,plain,
zero = meet(X1,composition(X2,zero)),
inference(cp,[status(thm)],[t16702,t141]) ).
cnf(t16745,plain,
meet(X1,composition(X2,zero)) = zero,
inference(orient,[status(thm)],[t16706]) ).
cnf(t46975,plain,
zero = join(zero,meet(composition(converse(sk1),sFlat5),complement(sFlat3))),
inference(step,[status(thm)],[t46974,t16745]) ).
cnf(t46976,plain,
zero = meet(composition(converse(sk1),sFlat5),complement(sFlat3)),
inference(step,[status(thm)],[t46975,t12671]) ).
cnf(t46977,plain,
zero = meet(complement(sFlat3),composition(converse(sk1),sFlat5)),
inference(step,[status(thm)],[t46976,t141]) ).
cnf(t46978,plain,
zero = meet(complement(sFlat3),composition(sk1,sFlat5)),
inference(step,[status(thm)],[t46977,t30539]) ).
cnf(t46979,plain,
zero = meet(complement(sFlat3),sFlat5),
inference(step,[status(thm)],[t46978,t40669]) ).
cnf(t46980,plain,
zero = meet(sFlat5,complement(sFlat3)),
inference(step,[status(thm)],[t46979,t141]) ).
cnf(t42536,plain,
meet(sFlat5,complement(sFlat3)) = zero,
inference(orient,[status(thm)],[t46980]) ).
cnf(t42539,plain,
sFlat5 = join(zero,meet(sFlat5,complement(complement(sFlat3)))),
inference(cp,[status(thm)],[t26941,t42536]) ).
cnf(t46981,plain,
sFlat5 = meet(sFlat5,complement(complement(sFlat3))),
inference(step,[status(thm)],[t42539,t12671]) ).
cnf(t46982,plain,
sFlat5 = meet(sFlat5,sFlat3),
inference(step,[status(thm)],[t46981,t24750]) ).
cnf(t46983,plain,
sFlat5 = meet(sFlat3,sFlat5),
inference(step,[status(thm)],[t46982,t141]) ).
cnf(t42542,plain,
meet(sFlat3,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t46983]) ).
cnf(t47117,plain,
sFlat3 = sFlat5,
inference(step,[status(thm)],[t47116,t42542]) ).
cnf(t44549,plain,
sFlat5 = sFlat3,
inference(orient,[status(thm)],[t47117]) ).
cnf(t47118,plain,
meet(sFlat0,sFlat4) = sFlat3,
inference(step,[status(thm)],[t140,t44549]) ).
cnf(t44550,plain,
meet(sFlat0,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t47118]) ).
cnf(goal_0,negated_conjecture,
meet(composition(sk1,sk2),complement(composition(sk1,sk3))) != meet(composition(sk1,sk2),complement(sk3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(sFlat0,complement(composition(sk1,sk3))) != meet(composition(sk1,sk2),complement(sk3)),
inference(rw,[status(thm)],[goal_0,t54]) ).
cnf(g0_1,plain,
meet(sFlat0,complement(sFlat1)) != meet(composition(sk1,sk2),complement(sk3)),
inference(rw,[status(thm)],[g0_0,t49]) ).
cnf(g0_2,plain,
meet(sFlat0,sFlat2) != meet(composition(sk1,sk2),complement(sk3)),
inference(rw,[status(thm)],[g0_1,t119]) ).
cnf(g0_3,plain,
sFlat3 != meet(composition(sk1,sk2),complement(sk3)),
inference(rw,[status(thm)],[g0_2,t136]) ).
cnf(g0_4,plain,
sFlat3 != meet(complement(sk3),composition(sk1,sk2)),
inference(rw,[status(thm)],[g0_3,t141]) ).
cnf(g0_5,plain,
sFlat3 != meet(sFlat4,composition(sk1,sk2)),
inference(rw,[status(thm)],[g0_4,t126]) ).
cnf(g0_6,plain,
sFlat3 != meet(sFlat4,sFlat0),
inference(rw,[status(thm)],[g0_5,t54]) ).
cnf(g0_7,plain,
sFlat3 != meet(sFlat0,sFlat4),
inference(rw,[status(thm)],[g0_6,t141]) ).
cnf(g0_8,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_7,t44550]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL030-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.33 % Computer : n001.cluster.edu
% 0.10/0.33 % Model : x86_64 x86_64
% 0.10/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.33 % Memory : 8046.5625MB
% 0.10/0.33 % OS : Linux 6.8.0-71-generic
% 0.10/0.34 % CPULimit : 300
% 0.10/0.34 % WCLimit : 300
% 0.10/0.34 % DateTime : Thu Sep 24 07:32:07 UTC 2026
% 0.10/0.34 % CPUTime :
% 0.10/0.34 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 124.87/16.41 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 124.87/16.41 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------