%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL017-3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:34:46 PM UTC 2026
% Result : Unsatisfiable 89.70s 11.98s
% Output : CNFRefutation 89.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 107
% Number of leaves : 24
% Syntax : Number of clauses : 510 ( 510 unt; 0 nHn; 177 RR)
% Number of literals : 510 ( 509 equ; 15 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 : 20 ( 20 usr; 15 con; 0-2 aty)
% Number of variables : 566 ( 65 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t98,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t20,axiom,
sFlat4 = composition(sk1,sk3),
introduced(definition) ).
cnf(t56,plain,
composition(sk1,sk3) = sFlat4,
inference(orient,[status(thm)],[t20]) ).
cnf(t16,axiom,
sFlat0 = complement(sk3),
introduced(definition) ).
cnf(t93,plain,
complement(sk3) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t84,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t99,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t84,t98]) ).
cnf(t36019,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t99,t84]) ).
cnf(t163,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t36019]) ).
cnf(t17,axiom,
sFlat1 = meet(sk2,complement(sk3)),
introduced(definition) ).
cnf(t36016,plain,
sFlat1 = meet(sk2,sFlat0),
inference(step,[status(thm)],[t17,t93]) ).
cnf(t152,plain,
meet(sk2,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t36016]) ).
cnf(t168,plain,
meet(sk2,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t152]) ).
cnf(t36021,plain,
meet(sFlat0,sk2) = sFlat1,
inference(step,[status(thm)],[t168,t163]) ).
cnf(t172,plain,
meet(sFlat0,sk2) = sFlat1,
inference(orient,[status(thm)],[t36021]) ).
cnf(t18,axiom,
sFlat2 = composition(sk1,meet(sk2,complement(sk3))),
introduced(definition) ).
cnf(t51,plain,
composition(sk1,meet(sk2,complement(sk3))) = sFlat2,
inference(orient,[status(thm)],[t18]) ).
cnf(t36008,plain,
composition(sk1,meet(sk2,sFlat0)) = sFlat2,
inference(step,[status(thm)],[t51,t93]) ).
cnf(t97,plain,
composition(sk1,meet(sk2,sFlat0)) = sFlat2,
inference(rw,[status(thm)],[t36008]) ).
cnf(t36025,plain,
composition(sk1,meet(sFlat0,sk2)) = sFlat2,
inference(step,[status(thm)],[t97,t163]) ).
cnf(t36026,plain,
composition(sk1,sFlat1) = sFlat2,
inference(step,[status(thm)],[t36025,t172]) ).
cnf(t181,plain,
composition(sk1,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t36026]) ).
cnf(t19,axiom,
sFlat3 = complement(composition(sk1,meet(sk2,complement(sk3)))),
introduced(definition) ).
cnf(t36005,plain,
sFlat3 = complement(sFlat2),
inference(step,[status(thm)],[t19,t51]) ).
cnf(t74,plain,
complement(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t36005]) ).
cnf(t21,axiom,
sFlat5 = join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)),
introduced(definition) ).
cnf(t36009,plain,
sFlat5 = join(composition(sk1,sk3),complement(composition(sk1,meet(sk2,complement(sk3))))),
inference(step,[status(thm)],[t21,t98]) ).
cnf(t36010,plain,
sFlat5 = join(sFlat4,complement(composition(sk1,meet(sk2,complement(sk3))))),
inference(step,[status(thm)],[t36009,t56]) ).
cnf(t36011,plain,
sFlat5 = join(sFlat4,complement(composition(sk1,meet(sk2,sFlat0)))),
inference(step,[status(thm)],[t36010,t93]) ).
cnf(t114,plain,
join(sFlat4,complement(composition(sk1,meet(sk2,sFlat0)))) = sFlat5,
inference(orient,[status(thm)],[t36011]) ).
cnf(t36017,plain,
join(sFlat4,complement(composition(sk1,sFlat1))) = sFlat5,
inference(step,[status(thm)],[t114,t152]) ).
cnf(t153,plain,
join(sFlat4,complement(composition(sk1,sFlat1))) = sFlat5,
inference(rw,[status(thm)],[t36017]) ).
cnf(t36041,plain,
join(sFlat4,complement(sFlat2)) = sFlat5,
inference(step,[status(thm)],[t153,t181]) ).
cnf(t36042,plain,
join(sFlat4,sFlat3) = sFlat5,
inference(step,[status(thm)],[t36041,t74]) ).
cnf(t36043,plain,
join(sFlat3,sFlat4) = sFlat5,
inference(step,[status(thm)],[t36042,t98]) ).
cnf(t541,plain,
join(sFlat3,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t36043]) ).
cnf(t22,axiom,
sFlat6 = composition(sk1,sk2),
introduced(definition) ).
cnf(t61,plain,
composition(sk1,sk2) = sFlat6,
inference(orient,[status(thm)],[t22]) ).
cnf(t23,axiom,
sFlat7 = complement(composition(sk1,sk2)),
introduced(definition) ).
cnf(t36006,plain,
sFlat7 = complement(sFlat6),
inference(step,[status(thm)],[t23,t61]) ).
cnf(t79,plain,
complement(sFlat6) = sFlat7,
inference(orient,[status(thm)],[t36006]) ).
cnf(t24,axiom,
sFlat8 = join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
introduced(definition) ).
cnf(t36012,plain,
sFlat8 = join(composition(sk1,sk3),complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t24,t98]) ).
cnf(t36013,plain,
sFlat8 = join(sFlat4,complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t36012,t56]) ).
cnf(t36014,plain,
sFlat8 = join(sFlat4,complement(sFlat6)),
inference(step,[status(thm)],[t36013,t61]) ).
cnf(t36015,plain,
sFlat8 = join(sFlat4,sFlat7),
inference(step,[status(thm)],[t36014,t79]) ).
cnf(t116,plain,
join(sFlat4,sFlat7) = sFlat8,
inference(orient,[status(thm)],[t36015]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t140,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t141,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t140,t29]) ).
cnf(t398,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t141]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t32,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t42,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t44,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t42,t29]) ).
cnf(t363,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t44]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t364,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t363,t25]) ).
cnf(t36033,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t364,t29]) ).
cnf(t375,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t36033]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t31,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t30,t25]) ).
cnf(t186,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t31]) ).
cnf(t377,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t375,t186]) ).
cnf(t36035,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t377,t375]) ).
cnf(t393,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t36035]) ).
cnf(t394,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t32,t393]) ).
cnf(t665,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t394]) ).
cnf(t684,plain,
join(X1,converse(composition(X2,converse(X1)))) = converse(composition(join(one,X2),converse(X1))),
inference(cp,[status(thm)],[t398,t665]) ).
cnf(t43,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t42,t29]) ).
cnf(t354,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t43]) ).
cnf(t36255,plain,
join(X1,composition(X1,converse(X2))) = converse(composition(join(one,X2),converse(X1))),
inference(step,[status(thm)],[t684,t354]) ).
cnf(t36256,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,converse(join(one,X2))),
inference(step,[status(thm)],[t36255,t354]) ).
cnf(t376,plain,
one = converse(one),
inference(cp,[status(thm)],[t375,t25]) ).
cnf(t383,plain,
converse(one) = one,
inference(orient,[status(thm)],[t376]) ).
cnf(t401,plain,
join(one,converse(X1)) = converse(join(one,X1)),
inference(cp,[status(thm)],[t398,t383]) ).
cnf(t413,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t401]) ).
cnf(t36257,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(step,[status(thm)],[t36256,t413]) ).
cnf(t3009,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(orient,[status(thm)],[t36257]) ).
cnf(t3028,plain,
composition(X1,join(one,converse(converse(X2)))) = join(X1,composition(X1,X2)),
inference(cp,[status(thm)],[t3009,t29]) ).
cnf(t36260,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(step,[status(thm)],[t3028,t29]) ).
cnf(t3089,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(orient,[status(thm)],[t36260]) ).
cnf(t3097,plain,
join(X1,composition(X1,X2)) = composition(X1,join(X2,one)),
inference(cp,[status(thm)],[t3089,t98]) ).
cnf(t3151,plain,
join(X1,composition(X1,X2)) = composition(X1,join(X2,one)),
inference(orient,[status(thm)],[t3097]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t36007,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t26,t84]) ).
cnf(t92,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t36007]) ).
cnf(t3195,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t92]) ).
cnf(t3215,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t3195,t84]) ).
cnf(t36297,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t3215,t98]) ).
cnf(t3413,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t36297]) ).
cnf(t3421,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t3413,t163]) ).
cnf(t4956,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t3421]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t144,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t4967,plain,
complement(complement(X1)) = join(meet(complement(complement(X1)),X1),zero),
inference(cp,[status(thm)],[t4956,t144]) ).
cnf(t36506,plain,
complement(complement(X1)) = join(zero,meet(complement(complement(X1)),X1)),
inference(step,[status(thm)],[t4967,t98]) ).
cnf(t36507,plain,
complement(complement(X1)) = join(zero,meet(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t36506,t163]) ).
cnf(t89,plain,
meet(join(complement(X1),complement(X2)),X3) = complement(join(meet(X1,X2),complement(X3))),
inference(cp,[status(thm)],[t84,t84]) ).
cnf(t1610,plain,
complement(join(meet(X1,X2),complement(X3))) = meet(join(complement(X1),complement(X2)),X3),
inference(orient,[status(thm)],[t89]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t101,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t106,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t84,t101]) ).
cnf(t36022,plain,
zero = complement(top),
inference(step,[status(thm)],[t106,t144]) ).
cnf(t173,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t36022]) ).
cnf(t1636,plain,
meet(join(complement(X1),complement(X2)),top) = complement(join(meet(X1,X2),zero)),
inference(cp,[status(thm)],[t1610,t173]) ).
cnf(t36318,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(meet(X1,X2),zero)),
inference(step,[status(thm)],[t1636,t163]) ).
cnf(t36319,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t36318,t98]) ).
cnf(t4119,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t36319]) ).
cnf(t4213,plain,
complement(join(zero,meet(X1,top))) = meet(top,join(complement(X1),zero)),
inference(cp,[status(thm)],[t4119,t173]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t107,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t117,plain,
join(sFlat4,join(sFlat7,X1)) = join(sFlat8,X1),
inference(cp,[status(thm)],[t107,t116]) ).
cnf(t349,plain,
join(sFlat4,join(sFlat7,X1)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t117]) ).
cnf(t350,plain,
join(sFlat8,complement(sFlat7)) = join(sFlat4,top),
inference(cp,[status(thm)],[t349,t101]) ).
cnf(t352,plain,
join(sFlat8,complement(sFlat7)) = join(sFlat4,top),
inference(orient,[status(thm)],[t350]) ).
cnf(t353,plain,
join(sFlat8,join(complement(sFlat7),X1)) = join(join(sFlat4,top),X1),
inference(cp,[status(thm)],[t107,t352]) ).
cnf(t36081,plain,
join(sFlat8,join(complement(sFlat7),X1)) = join(sFlat4,join(top,X1)),
inference(step,[status(thm)],[t353,t107]) ).
cnf(t1135,plain,
join(sFlat8,join(complement(sFlat7),X1)) = join(sFlat4,join(top,X1)),
inference(orient,[status(thm)],[t36081]) ).
cnf(t28,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)],[t26,t26]) ).
cnf(t36059,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)],[t28,t98]) ).
cnf(t36060,plain,
join(complement(X1),complement(X2)) = join(complement(X1),meet(join(complement(X1),complement(X2)),complement(join(complement(X1),X2)))),
inference(step,[status(thm)],[t36059,t84]) ).
cnf(t702,plain,
join(complement(X1),meet(join(complement(X1),complement(X2)),complement(join(complement(X1),X2)))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t36060]) ).
cnf(t1139,plain,
join(sFlat4,join(top,meet(join(complement(sFlat7),complement(X1)),complement(join(complement(sFlat7),X1))))) = join(sFlat8,join(complement(sFlat7),complement(X1))),
inference(cp,[status(thm)],[t1135,t702]) ).
cnf(t108,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t107,t101]) ).
cnf(t795,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t108]) ).
cnf(t15,axiom,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,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)],[t15]) ).
cnf(t826,plain,
top = join(meet(composition(X1,X2),X3),join(composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),complement(composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))))),
inference(cp,[status(thm)],[t795,t35]) ).
cnf(t36061,plain,
top = join(meet(composition(X1,X2),X3),top),
inference(step,[status(thm)],[t826,t101]) ).
cnf(t36062,plain,
top = join(top,meet(composition(X1,X2),X3)),
inference(step,[status(thm)],[t36061,t98]) ).
cnf(t855,plain,
join(top,meet(composition(X1,X2),X3)) = top,
inference(orient,[status(thm)],[t36062]) ).
cnf(t857,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t855,t25]) ).
cnf(t872,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t857]) ).
cnf(t36082,plain,
join(sFlat4,top) = join(sFlat8,join(complement(sFlat7),complement(X1))),
inference(step,[status(thm)],[t1139,t872]) ).
cnf(t104,plain,
top = join(sFlat2,sFlat3),
inference(cp,[status(thm)],[t101,t74]) ).
cnf(t156,plain,
join(sFlat2,sFlat3) = top,
inference(orient,[status(thm)],[t104]) ).
cnf(t157,plain,
join(sFlat2,join(sFlat3,X1)) = join(top,X1),
inference(cp,[status(thm)],[t107,t156]) ).
cnf(t492,plain,
join(sFlat2,join(sFlat3,X1)) = join(top,X1),
inference(orient,[status(thm)],[t157]) ).
cnf(t542,plain,
join(top,sFlat4) = join(sFlat2,sFlat5),
inference(cp,[status(thm)],[t492,t541]) ).
cnf(t36044,plain,
join(sFlat4,top) = join(sFlat2,sFlat5),
inference(step,[status(thm)],[t542,t98]) ).
cnf(t543,plain,
join(sFlat4,top) = join(sFlat2,sFlat5),
inference(orient,[status(thm)],[t36044]) ).
cnf(t36083,plain,
join(sFlat2,sFlat5) = join(sFlat8,join(complement(sFlat7),complement(X1))),
inference(step,[status(thm)],[t36082,t543]) ).
cnf(t36084,plain,
join(sFlat2,sFlat5) = join(sFlat4,join(top,complement(X1))),
inference(step,[status(thm)],[t36083,t1135]) ).
cnf(t1146,plain,
join(sFlat4,join(top,complement(X1))) = join(sFlat2,sFlat5),
inference(orient,[status(thm)],[t36084]) ).
cnf(t110,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t107,t101]) ).
cnf(t548,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t110]) ).
cnf(t552,plain,
join(top,complement(complement(X1))) = join(X1,top),
inference(cp,[status(thm)],[t548,t101]) ).
cnf(t580,plain,
join(top,complement(complement(X1))) = join(X1,top),
inference(orient,[status(thm)],[t552]) ).
cnf(t1153,plain,
join(sFlat2,sFlat5) = join(sFlat4,join(X1,top)),
inference(cp,[status(thm)],[t1146,t580]) ).
cnf(t553,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t548,t98]) ).
cnf(t638,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t553]) ).
cnf(t1147,plain,
join(sFlat2,sFlat5) = join(top,top),
inference(cp,[status(thm)],[t1146,t638]) ).
cnf(t176,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t84,t173]) ).
cnf(t498,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t176]) ).
cnf(t509,plain,
meet(top,top) = complement(join(zero,zero)),
inference(cp,[status(thm)],[t498,t173]) ).
cnf(t523,plain,
complement(join(zero,zero)) = meet(top,top),
inference(orient,[status(thm)],[t509]) ).
cnf(t582,plain,
join(join(zero,zero),top) = join(top,complement(meet(top,top))),
inference(cp,[status(thm)],[t580,t523]) ).
cnf(t36064,plain,
join(zero,join(zero,top)) = join(top,complement(meet(top,top))),
inference(step,[status(thm)],[t582,t107]) ).
cnf(t175,plain,
top = join(top,zero),
inference(cp,[status(thm)],[t101,t173]) ).
cnf(t36024,plain,
top = join(zero,top),
inference(step,[status(thm)],[t175,t98]) ).
cnf(t179,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t36024]) ).
cnf(t36065,plain,
join(zero,top) = join(top,complement(meet(top,top))),
inference(step,[status(thm)],[t36064,t179]) ).
cnf(t36066,plain,
top = join(top,complement(meet(top,top))),
inference(step,[status(thm)],[t36065,t179]) ).
cnf(t876,plain,
join(top,complement(meet(top,top))) = top,
inference(orient,[status(thm)],[t36066]) ).
cnf(t877,plain,
join(top,top) = join(meet(top,top),top),
inference(cp,[status(thm)],[t638,t876]) ).
cnf(t36074,plain,
join(top,top) = join(top,meet(top,top)),
inference(step,[status(thm)],[t877,t98]) ).
cnf(t36075,plain,
join(top,top) = top,
inference(step,[status(thm)],[t36074,t872]) ).
cnf(t900,plain,
join(top,top) = top,
inference(orient,[status(thm)],[t36075]) ).
cnf(t36086,plain,
join(sFlat2,sFlat5) = top,
inference(step,[status(thm)],[t1147,t900]) ).
cnf(t1161,plain,
join(sFlat2,sFlat5) = top,
inference(orient,[status(thm)],[t36086]) ).
cnf(t36102,plain,
top = join(sFlat4,join(X1,top)),
inference(step,[status(thm)],[t1153,t1161]) ).
cnf(t1177,plain,
join(sFlat4,join(X1,top)) = top,
inference(orient,[status(thm)],[t36102]) ).
cnf(t113,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t107,t98]) ).
cnf(t36037,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t113,t107]) ).
cnf(t457,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t36037]) ).
cnf(t1178,plain,
top = join(X1,join(sFlat4,top)),
inference(cp,[status(thm)],[t1177,t457]) ).
cnf(t36091,plain,
join(sFlat4,top) = top,
inference(step,[status(thm)],[t543,t1161]) ).
cnf(t1166,plain,
join(sFlat4,top) = top,
inference(orient,[status(thm)],[t36091]) ).
cnf(t36103,plain,
top = join(X1,top),
inference(step,[status(thm)],[t1178,t1166]) ).
cnf(t1185,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t36103]) ).
cnf(t3229,plain,
X1 = join(meet(X1,top),complement(top)),
inference(cp,[status(thm)],[t3195,t1185]) ).
cnf(t36285,plain,
X1 = join(complement(top),meet(X1,top)),
inference(step,[status(thm)],[t3229,t98]) ).
cnf(t36286,plain,
X1 = join(zero,meet(X1,top)),
inference(step,[status(thm)],[t36285,t173]) ).
cnf(t3327,plain,
join(zero,meet(X1,top)) = X1,
inference(orient,[status(thm)],[t36286]) ).
cnf(t36320,plain,
complement(X1) = meet(top,join(complement(X1),zero)),
inference(step,[status(thm)],[t4213,t3327]) ).
cnf(t36321,plain,
complement(X1) = meet(top,join(zero,complement(X1))),
inference(step,[status(thm)],[t36320,t98]) ).
cnf(t4224,plain,
meet(top,join(zero,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t36321]) ).
cnf(t4269,plain,
complement(join(complement(X1),complement(X2))) = meet(top,join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t4224,t84]) ).
cnf(t36396,plain,
meet(X1,X2) = meet(top,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t4269,t84]) ).
cnf(t4632,plain,
meet(top,join(zero,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t36396]) ).
cnf(t3233,plain,
X1 = join(meet(X1,complement(complement(X1))),complement(top)),
inference(cp,[status(thm)],[t3195,t101]) ).
cnf(t36295,plain,
X1 = join(complement(top),meet(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t3233,t98]) ).
cnf(t36296,plain,
X1 = join(zero,meet(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t36295,t173]) ).
cnf(t3349,plain,
join(zero,meet(X1,complement(complement(X1)))) = X1,
inference(orient,[status(thm)],[t36296]) ).
cnf(t4634,plain,
meet(X1,complement(complement(X1))) = meet(top,X1),
inference(cp,[status(thm)],[t4632,t3349]) ).
cnf(t4727,plain,
meet(X1,complement(complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t4634]) ).
cnf(t36508,plain,
complement(complement(X1)) = join(zero,meet(top,X1)),
inference(step,[status(thm)],[t36507,t4727]) ).
cnf(t36402,plain,
join(zero,meet(top,X1)) = X1,
inference(step,[status(thm)],[t3349,t4727]) ).
cnf(t4799,plain,
join(zero,meet(top,X1)) = X1,
inference(rw,[status(thm)],[t36402]) ).
cnf(t4811,plain,
join(zero,meet(top,X1)) = X1,
inference(orient,[status(thm)],[t4799]) ).
cnf(t36509,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t36508,t4811]) ).
cnf(t7187,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t36509]) ).
cnf(t7229,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t7187,t84]) ).
cnf(t9485,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t7229]) ).
cnf(t9509,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t9485,t7187]) ).
cnf(t10601,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t9509]) ).
cnf(t3196,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t3195,t144]) ).
cnf(t36270,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t3196,t84]) ).
cnf(t3303,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t36270]) ).
cnf(t4633,plain,
meet(X1,X1) = meet(top,X1),
inference(cp,[status(thm)],[t4632,t3303]) ).
cnf(t4648,plain,
meet(X1,X1) = meet(top,X1),
inference(orient,[status(thm)],[t4633]) ).
cnf(t10605,plain,
join(X1,complement(complement(X1))) = complement(meet(top,complement(X1))),
inference(cp,[status(thm)],[t10601,t4648]) ).
cnf(t36652,plain,
join(X1,X1) = complement(meet(top,complement(X1))),
inference(step,[status(thm)],[t10605,t7187]) ).
cnf(t7219,plain,
join(zero,complement(X1)) = complement(meet(top,X1)),
inference(cp,[status(thm)],[t7187,t498]) ).
cnf(t8682,plain,
complement(meet(top,X1)) = join(zero,complement(X1)),
inference(orient,[status(thm)],[t7219]) ).
cnf(t36653,plain,
join(X1,X1) = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t36652,t8682]) ).
cnf(t36654,plain,
join(X1,X1) = join(zero,X1),
inference(step,[status(thm)],[t36653,t7187]) ).
cnf(t10727,plain,
join(X1,X1) = join(zero,X1),
inference(orient,[status(thm)],[t36654]) ).
cnf(t10771,plain,
join(X1,composition(X1,one)) = composition(X1,join(zero,one)),
inference(cp,[status(thm)],[t3151,t10727]) ).
cnf(t36655,plain,
join(X1,X1) = composition(X1,join(zero,one)),
inference(step,[status(thm)],[t10771,t25]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t66,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t68,plain,
complement(one) = join(composition(converse(X1),complement(X1)),complement(one)),
inference(cp,[status(thm)],[t66,t25]) ).
cnf(t36156,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t68,t98]) ).
cnf(t1455,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t36156]) ).
cnf(t1467,plain,
complement(one) = join(complement(one),composition(one,complement(one))),
inference(cp,[status(thm)],[t1455,t383]) ).
cnf(t36157,plain,
complement(one) = join(complement(one),complement(one)),
inference(step,[status(thm)],[t1467,t393]) ).
cnf(t1503,plain,
join(complement(one),complement(one)) = complement(one),
inference(orient,[status(thm)],[t36157]) ).
cnf(t1504,plain,
meet(one,one) = complement(complement(one)),
inference(cp,[status(thm)],[t84,t1503]) ).
cnf(t1510,plain,
complement(complement(one)) = meet(one,one),
inference(orient,[status(thm)],[t1504]) ).
cnf(t4250,plain,
complement(complement(one)) = meet(top,join(zero,meet(one,one))),
inference(cp,[status(thm)],[t4224,t1510]) ).
cnf(t36363,plain,
meet(one,one) = meet(top,join(zero,meet(one,one))),
inference(step,[status(thm)],[t4250,t1510]) ).
cnf(t36364,plain,
meet(one,one) = meet(top,one),
inference(step,[status(thm)],[t36363,t3303]) ).
cnf(t4423,plain,
meet(one,one) = meet(top,one),
inference(orient,[status(thm)],[t36364]) ).
cnf(t36365,plain,
complement(complement(one)) = meet(top,one),
inference(step,[status(thm)],[t1510,t4423]) ).
cnf(t4424,plain,
complement(complement(one)) = meet(top,one),
inference(orient,[status(thm)],[t36365]) ).
cnf(t36510,plain,
one = meet(top,one),
inference(step,[status(thm)],[t4424,t7187]) ).
cnf(t7279,plain,
one = meet(top,one),
inference(rw,[status(thm)],[t36510]) ).
cnf(t7417,plain,
meet(top,one) = one,
inference(orient,[status(thm)],[t7279]) ).
cnf(t7418,plain,
one = join(zero,one),
inference(cp,[status(thm)],[t4811,t7417]) ).
cnf(t7431,plain,
join(zero,one) = one,
inference(orient,[status(thm)],[t7418]) ).
cnf(t36656,plain,
join(X1,X1) = composition(X1,one),
inference(step,[status(thm)],[t36655,t7431]) ).
cnf(t36657,plain,
join(X1,X1) = X1,
inference(step,[status(thm)],[t36656,t25]) ).
cnf(t10780,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t36657]) ).
cnf(t10783,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t10780,t457]) ).
cnf(t36759,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t10783,t107]) ).
cnf(t36760,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t36759,t10780]) ).
cnf(t11239,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t36760]) ).
cnf(t11253,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t11239,t3413]) ).
cnf(t36789,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t11253,t3413]) ).
cnf(t36790,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t36789,t98]) ).
cnf(t11308,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t36790]) ).
cnf(t7234,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t84,t7187]) ).
cnf(t9811,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t7234]) ).
cnf(t9817,plain,
meet(complement(join(X1,X2)),X3) = complement(join(X1,join(X2,complement(X3)))),
inference(cp,[status(thm)],[t9811,t107]) ).
cnf(t32894,plain,
complement(join(X1,join(X2,complement(X3)))) = meet(complement(join(X1,X2)),X3),
inference(orient,[status(thm)],[t9817]) ).
cnf(t32934,plain,
meet(complement(join(X1,complement(X2))),X3) = complement(join(X1,complement(meet(X2,X3)))),
inference(cp,[status(thm)],[t32894,t9485]) ).
cnf(t38130,plain,
meet(meet(complement(X1),X2),X3) = complement(join(X1,complement(meet(X2,X3)))),
inference(step,[status(thm)],[t32934,t9811]) ).
cnf(t38131,plain,
meet(meet(complement(X1),X2),X3) = meet(complement(X1),meet(X2,X3)),
inference(step,[status(thm)],[t38130,t9811]) ).
cnf(t33133,plain,
meet(meet(complement(X1),X2),X3) = meet(complement(X1),meet(X2,X3)),
inference(orient,[status(thm)],[t38131]) ).
cnf(t81,plain,
X1 = join(complement(join(complement(X1),sFlat7)),complement(join(complement(X1),sFlat6))),
inference(cp,[status(thm)],[t26,t79]) ).
cnf(t37876,plain,
X1 = complement(meet(join(complement(X1),sFlat7),join(complement(X1),sFlat6))),
inference(step,[status(thm)],[t81,t9485]) ).
cnf(t37877,plain,
X1 = complement(meet(join(complement(X1),sFlat6),join(complement(X1),sFlat7))),
inference(step,[status(thm)],[t37876,t163]) ).
cnf(t37878,plain,
X1 = complement(meet(join(sFlat6,complement(X1)),join(complement(X1),sFlat7))),
inference(step,[status(thm)],[t37877,t98]) ).
cnf(t37879,plain,
X1 = complement(meet(join(sFlat6,complement(X1)),join(sFlat7,complement(X1)))),
inference(step,[status(thm)],[t37878,t98]) ).
cnf(t27783,plain,
complement(meet(join(sFlat6,complement(X1)),join(sFlat7,complement(X1)))) = X1,
inference(orient,[status(thm)],[t37879]) ).
cnf(t33247,plain,
meet(complement(meet(join(sFlat6,complement(X1)),join(sFlat7,complement(X1)))),meet(X2,X3)) = meet(meet(X1,X2),X3),
inference(cp,[status(thm)],[t33133,t27783]) ).
cnf(t38132,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t33247,t27783]) ).
cnf(t33409,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t38132]) ).
cnf(t33425,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t33409,t163]) ).
cnf(t33873,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t33425]) ).
cnf(t33954,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t11308,t33873]) ).
cnf(t34360,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t33954]) ).
cnf(t7235,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t84,t7187]) ).
cnf(t10182,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t7235]) ).
cnf(t9538,plain,
join(top,complement(X1)) = join(X2,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t548,t9485]) ).
cnf(t575,plain,
join(top,join(complement(complement(X1)),X2)) = join(X1,join(top,X2)),
inference(cp,[status(thm)],[t548,t548]) ).
cnf(t2403,plain,
join(top,join(complement(complement(X1)),X2)) = join(X1,join(top,X2)),
inference(orient,[status(thm)],[t575]) ).
cnf(t2405,plain,
join(X1,join(top,meet(join(complement(complement(X1)),complement(X2)),complement(join(complement(complement(X1)),X2))))) = join(top,join(complement(complement(X1)),complement(X2))),
inference(cp,[status(thm)],[t2403,t702]) ).
cnf(t36229,plain,
join(X1,top) = join(top,join(complement(complement(X1)),complement(X2))),
inference(step,[status(thm)],[t2405,t872]) ).
cnf(t36230,plain,
top = join(top,join(complement(complement(X1)),complement(X2))),
inference(step,[status(thm)],[t36229,t1185]) ).
cnf(t36231,plain,
top = join(X1,join(top,complement(X2))),
inference(step,[status(thm)],[t36230,t2403]) ).
cnf(t2419,plain,
join(X1,join(top,complement(X2))) = top,
inference(orient,[status(thm)],[t36231]) ).
cnf(t180,plain,
join(zero,join(top,X1)) = join(top,X1),
inference(cp,[status(thm)],[t107,t179]) ).
cnf(t601,plain,
join(zero,join(top,X1)) = join(top,X1),
inference(orient,[status(thm)],[t180]) ).
cnf(t2420,plain,
top = join(top,complement(X1)),
inference(cp,[status(thm)],[t2419,t601]) ).
cnf(t2427,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t2420]) ).
cnf(t36638,plain,
top = join(X2,complement(meet(X2,X1))),
inference(step,[status(thm)],[t9538,t2427]) ).
cnf(t10463,plain,
join(X1,complement(meet(X1,X2))) = top,
inference(orient,[status(thm)],[t36638]) ).
cnf(t10474,plain,
meet(X1,complement(complement(meet(complement(X1),X2)))) = complement(top),
inference(cp,[status(thm)],[t10182,t10463]) ).
cnf(t36891,plain,
meet(X1,meet(complement(X1),X2)) = complement(top),
inference(step,[status(thm)],[t10474,t7187]) ).
cnf(t36892,plain,
meet(X1,meet(complement(X1),X2)) = zero,
inference(step,[status(thm)],[t36891,t173]) ).
cnf(t12441,plain,
meet(X1,meet(complement(X1),X2)) = zero,
inference(orient,[status(thm)],[t36892]) ).
cnf(t12489,plain,
meet(complement(complement(X1)),X2) = join(meet(meet(complement(complement(X1)),X2),X1),zero),
inference(cp,[status(thm)],[t4956,t12441]) ).
cnf(t36893,plain,
meet(X1,X2) = join(meet(meet(complement(complement(X1)),X2),X1),zero),
inference(step,[status(thm)],[t12489,t7187]) ).
cnf(t36658,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t10727,t10780]) ).
cnf(t10815,plain,
X1 = join(zero,X1),
inference(rw,[status(thm)],[t36658]) ).
cnf(t10863,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t10815]) ).
cnf(t10872,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t10863,t98]) ).
cnf(t10899,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t10872]) ).
cnf(t36894,plain,
meet(X1,X2) = meet(meet(complement(complement(X1)),X2),X1),
inference(step,[status(thm)],[t36893,t10899]) ).
cnf(t36895,plain,
meet(X1,X2) = meet(X1,meet(complement(complement(X1)),X2)),
inference(step,[status(thm)],[t36894,t163]) ).
cnf(t36896,plain,
meet(X1,X2) = meet(X1,meet(X1,X2)),
inference(step,[status(thm)],[t36895,t7187]) ).
cnf(t12494,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t36896]) ).
cnf(t34363,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t34360,t12494]) ).
cnf(t34567,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t34363]) ).
cnf(t7232,plain,
sFlat2 = complement(sFlat3),
inference(cp,[status(thm)],[t7187,t74]) ).
cnf(t7332,plain,
complement(sFlat3) = sFlat2,
inference(orient,[status(thm)],[t7232]) ).
cnf(t7366,plain,
sFlat3 = join(meet(sFlat3,X1),complement(join(sFlat2,X1))),
inference(cp,[status(thm)],[t3195,t7332]) ).
cnf(t32365,plain,
join(meet(sFlat3,X1),complement(join(sFlat2,X1))) = sFlat3,
inference(orient,[status(thm)],[t7366]) ).
cnf(t109,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t107,t98]) ).
cnf(t451,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t109]) ).
cnf(t578,plain,
join(join(complement(X1),X2),join(X3,X1)) = join(X3,join(top,X2)),
inference(cp,[status(thm)],[t451,t548]) ).
cnf(t37578,plain,
join(complement(X1),join(X2,join(X3,X1))) = join(X3,join(top,X2)),
inference(step,[status(thm)],[t578,t107]) ).
cnf(t21034,plain,
join(complement(X1),join(X2,join(X3,X1))) = join(X3,join(top,X2)),
inference(orient,[status(thm)],[t37578]) ).
cnf(t368,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t140,t363]) ).
cnf(t5863,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t368]) ).
cnf(t45,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t32,t42]) ).
cnf(t11149,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t45]) ).
cnf(t11213,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)],[t5863,t11149]) ).
cnf(t37559,plain,
join(composition(X1,X2),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t11213,t29]) ).
cnf(t37560,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t37559,t29]) ).
cnf(t407,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t42,t398]) ).
cnf(t5999,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t407]) ).
cnf(t37561,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(converse(converse(X1)),join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t37560,t5999]) ).
cnf(t37562,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t37561,t29]) ).
cnf(t37563,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t37562,t29]) ).
cnf(t20472,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t37563]) ).
cnf(t20514,plain,
composition(sk1,join(sFlat1,X1)) = join(sFlat2,composition(sk1,X1)),
inference(cp,[status(thm)],[t20472,t181]) ).
cnf(t20605,plain,
composition(sk1,join(sFlat1,X1)) = join(sFlat2,composition(sk1,X1)),
inference(orient,[status(thm)],[t20514]) ).
cnf(t7228,plain,
sk3 = complement(sFlat0),
inference(cp,[status(thm)],[t7187,t93]) ).
cnf(t7283,plain,
complement(sFlat0) = sk3,
inference(orient,[status(thm)],[t7228]) ).
cnf(t9508,plain,
complement(meet(sFlat0,X1)) = join(sk3,complement(X1)),
inference(cp,[status(thm)],[t9485,t7283]) ).
cnf(t9547,plain,
complement(meet(sFlat0,X1)) = join(sk3,complement(X1)),
inference(orient,[status(thm)],[t9508]) ).
cnf(t9551,plain,
complement(meet(meet(sFlat0,X1),X2)) = join(join(sk3,complement(X1)),complement(X2)),
inference(cp,[status(thm)],[t9485,t9547]) ).
cnf(t36993,plain,
complement(meet(meet(sFlat0,X1),X2)) = join(sk3,join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t9551,t107]) ).
cnf(t36994,plain,
complement(meet(meet(sFlat0,X1),X2)) = join(sk3,complement(meet(X1,X2))),
inference(step,[status(thm)],[t36993,t9485]) ).
cnf(t14121,plain,
complement(meet(meet(sFlat0,X1),X2)) = join(sk3,complement(meet(X1,X2))),
inference(orient,[status(thm)],[t36994]) ).
cnf(t14149,plain,
meet(meet(sFlat0,X1),X2) = complement(join(sk3,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t7187,t14121]) ).
cnf(t36998,plain,
meet(meet(sFlat0,X1),X2) = meet(complement(sk3),meet(X1,X2)),
inference(step,[status(thm)],[t14149,t9811]) ).
cnf(t36999,plain,
meet(meet(sFlat0,X1),X2) = meet(sFlat0,meet(X1,X2)),
inference(step,[status(thm)],[t36998,t93]) ).
cnf(t14370,plain,
meet(meet(sFlat0,X1),X2) = meet(sFlat0,meet(X1,X2)),
inference(orient,[status(thm)],[t36999]) ).
cnf(t14381,plain,
meet(sFlat0,meet(X1,complement(meet(sFlat0,X1)))) = zero,
inference(cp,[status(thm)],[t14370,t144]) ).
cnf(t37021,plain,
meet(sFlat0,meet(X1,join(sk3,complement(X1)))) = zero,
inference(step,[status(thm)],[t14381,t9547]) ).
cnf(t14842,plain,
meet(sFlat0,meet(X1,join(sk3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t37021]) ).
cnf(t14382,plain,
meet(sFlat0,meet(X1,X2)) = meet(X2,meet(sFlat0,X1)),
inference(cp,[status(thm)],[t14370,t163]) ).
cnf(t14442,plain,
meet(sFlat0,meet(X1,X2)) = meet(X2,meet(sFlat0,X1)),
inference(orient,[status(thm)],[t14382]) ).
cnf(t14448,plain,
meet(X1,meet(sFlat0,X2)) = meet(sFlat0,meet(X1,X2)),
inference(cp,[status(thm)],[t14442,t163]) ).
cnf(t14577,plain,
meet(X1,meet(sFlat0,X2)) = meet(sFlat0,meet(X1,X2)),
inference(orient,[status(thm)],[t14448]) ).
cnf(t14843,plain,
zero = meet(X1,meet(sFlat0,join(sk3,complement(X1)))),
inference(cp,[status(thm)],[t14842,t14577]) ).
cnf(t35770,plain,
meet(X1,meet(sFlat0,join(sk3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t14843]) ).
cnf(t35843,plain,
X1 = join(zero,meet(complement(meet(sFlat0,join(sk3,complement(X1)))),X1)),
inference(cp,[status(thm)],[t4956,t35770]) ).
cnf(t38178,plain,
X1 = meet(complement(meet(sFlat0,join(sk3,complement(X1)))),X1),
inference(step,[status(thm)],[t35843,t10863]) ).
cnf(t38179,plain,
X1 = meet(X1,complement(meet(sFlat0,join(sk3,complement(X1))))),
inference(step,[status(thm)],[t38178,t163]) ).
cnf(t38180,plain,
X1 = meet(X1,join(sk3,complement(join(sk3,complement(X1))))),
inference(step,[status(thm)],[t38179,t9547]) ).
cnf(t38181,plain,
X1 = meet(X1,join(sk3,meet(complement(sk3),X1))),
inference(step,[status(thm)],[t38180,t9811]) ).
cnf(t38182,plain,
X1 = meet(X1,join(sk3,meet(sFlat0,X1))),
inference(step,[status(thm)],[t38181,t93]) ).
cnf(t35853,plain,
meet(X1,join(sk3,meet(sFlat0,X1))) = X1,
inference(orient,[status(thm)],[t38182]) ).
cnf(t35868,plain,
sk2 = meet(sk2,join(sk3,sFlat1)),
inference(cp,[status(thm)],[t35853,t172]) ).
cnf(t38183,plain,
sk2 = meet(sk2,join(sFlat1,sk3)),
inference(step,[status(thm)],[t35868,t98]) ).
cnf(t35908,plain,
meet(sk2,join(sFlat1,sk3)) = sk2,
inference(orient,[status(thm)],[t38183]) ).
cnf(t35909,plain,
join(sFlat1,sk3) = join(join(sFlat1,sk3),sk2),
inference(cp,[status(thm)],[t34567,t35908]) ).
cnf(t38184,plain,
join(sFlat1,sk3) = join(sFlat1,join(sk3,sk2)),
inference(step,[status(thm)],[t35909,t107]) ).
cnf(t35914,plain,
join(sFlat1,join(sk3,sk2)) = join(sFlat1,sk3),
inference(orient,[status(thm)],[t38184]) ).
cnf(t35915,plain,
join(sFlat2,composition(sk1,join(sk3,sk2))) = composition(sk1,join(sFlat1,sk3)),
inference(cp,[status(thm)],[t20605,t35914]) ).
cnf(t409,plain,
composition(converse(X1),join(converse(X2),X3)) = converse(composition(join(X2,converse(X3)),X1)),
inference(cp,[status(thm)],[t363,t398]) ).
cnf(t6058,plain,
converse(composition(join(X1,converse(X2)),X3)) = composition(converse(X3),join(converse(X1),X2)),
inference(orient,[status(thm)],[t409]) ).
cnf(t11181,plain,
composition(join(converse(sk3),X1),converse(sk1)) = join(converse(sFlat4),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t11149,t56]) ).
cnf(t20280,plain,
composition(join(converse(sk3),X1),converse(sk1)) = join(converse(sFlat4),composition(X1,converse(sk1))),
inference(orient,[status(thm)],[t11181]) ).
cnf(t20318,plain,
composition(converse(converse(sk1)),join(converse(converse(sk3)),X1)) = converse(join(converse(sFlat4),composition(converse(X1),converse(sk1)))),
inference(cp,[status(thm)],[t6058,t20280]) ).
cnf(t37553,plain,
composition(sk1,join(converse(converse(sk3)),X1)) = converse(join(converse(sFlat4),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t20318,t29]) ).
cnf(t37554,plain,
composition(sk1,join(sk3,X1)) = converse(join(converse(sFlat4),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t37553,t29]) ).
cnf(t37555,plain,
composition(sk1,join(sk3,X1)) = join(sFlat4,converse(composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t37554,t398]) ).
cnf(t37556,plain,
composition(sk1,join(sk3,X1)) = join(sFlat4,composition(converse(converse(sk1)),X1)),
inference(step,[status(thm)],[t37555,t363]) ).
cnf(t37557,plain,
composition(sk1,join(sk3,X1)) = join(sFlat4,composition(sk1,X1)),
inference(step,[status(thm)],[t37556,t29]) ).
cnf(t20345,plain,
composition(sk1,join(sk3,X1)) = join(sFlat4,composition(sk1,X1)),
inference(orient,[status(thm)],[t37557]) ).
cnf(t38185,plain,
join(sFlat2,join(sFlat4,composition(sk1,sk2))) = composition(sk1,join(sFlat1,sk3)),
inference(step,[status(thm)],[t35915,t20345]) ).
cnf(t38186,plain,
join(sFlat2,join(sFlat4,sFlat6)) = composition(sk1,join(sFlat1,sk3)),
inference(step,[status(thm)],[t38185,t61]) ).
cnf(t38187,plain,
join(sFlat2,join(sFlat4,sFlat6)) = join(sFlat2,composition(sk1,sk3)),
inference(step,[status(thm)],[t38186,t20605]) ).
cnf(t38188,plain,
join(sFlat2,join(sFlat4,sFlat6)) = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t38187,t56]) ).
cnf(t35921,plain,
join(sFlat2,join(sFlat4,sFlat6)) = join(sFlat2,sFlat4),
inference(orient,[status(thm)],[t38188]) ).
cnf(t35926,plain,
join(sFlat4,join(top,sFlat2)) = join(complement(sFlat6),join(sFlat2,sFlat4)),
inference(cp,[status(thm)],[t21034,t35921]) ).
cnf(t1181,plain,
top = join(sFlat4,join(top,X1)),
inference(cp,[status(thm)],[t1177,t98]) ).
cnf(t1219,plain,
join(sFlat4,join(top,X1)) = top,
inference(orient,[status(thm)],[t1181]) ).
cnf(t38189,plain,
top = join(complement(sFlat6),join(sFlat2,sFlat4)),
inference(step,[status(thm)],[t35926,t1219]) ).
cnf(t38190,plain,
top = join(sFlat2,join(complement(sFlat6),sFlat4)),
inference(step,[status(thm)],[t38189,t457]) ).
cnf(t38191,plain,
top = join(sFlat2,join(sFlat4,complement(sFlat6))),
inference(step,[status(thm)],[t38190,t98]) ).
cnf(t38192,plain,
top = join(sFlat2,join(sFlat4,sFlat7)),
inference(step,[status(thm)],[t38191,t79]) ).
cnf(t38193,plain,
top = join(sFlat2,sFlat8),
inference(step,[status(thm)],[t38192,t116]) ).
cnf(t35932,plain,
join(sFlat2,sFlat8) = top,
inference(orient,[status(thm)],[t38193]) ).
cnf(t35933,plain,
sFlat3 = join(meet(sFlat3,sFlat8),complement(top)),
inference(cp,[status(thm)],[t32365,t35932]) ).
cnf(t38194,plain,
sFlat3 = join(complement(top),meet(sFlat3,sFlat8)),
inference(step,[status(thm)],[t35933,t98]) ).
cnf(t38195,plain,
sFlat3 = join(zero,meet(sFlat3,sFlat8)),
inference(step,[status(thm)],[t38194,t173]) ).
cnf(t38196,plain,
sFlat3 = meet(sFlat3,sFlat8),
inference(step,[status(thm)],[t38195,t10863]) ).
cnf(t35934,plain,
meet(sFlat3,sFlat8) = sFlat3,
inference(orient,[status(thm)],[t38196]) ).
cnf(t35935,plain,
sFlat8 = join(sFlat8,sFlat3),
inference(cp,[status(thm)],[t34567,t35934]) ).
cnf(t38197,plain,
sFlat8 = join(sFlat3,sFlat8),
inference(step,[status(thm)],[t35935,t98]) ).
cnf(t351,plain,
join(sFlat8,X1) = join(sFlat4,join(X1,sFlat7)),
inference(cp,[status(thm)],[t349,t98]) ).
cnf(t538,plain,
join(sFlat4,join(X1,sFlat7)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t351]) ).
cnf(t86,plain,
meet(sFlat6,X1) = complement(join(sFlat7,complement(X1))),
inference(cp,[status(thm)],[t84,t79]) ).
cnf(t232,plain,
complement(join(sFlat7,complement(X1))) = meet(sFlat6,X1),
inference(orient,[status(thm)],[t86]) ).
cnf(t7223,plain,
join(sFlat7,complement(X1)) = complement(meet(sFlat6,X1)),
inference(cp,[status(thm)],[t7187,t232]) ).
cnf(t7933,plain,
complement(meet(sFlat6,X1)) = join(sFlat7,complement(X1)),
inference(orient,[status(thm)],[t7223]) ).
cnf(t7934,plain,
join(sFlat7,complement(X1)) = complement(meet(X1,sFlat6)),
inference(cp,[status(thm)],[t7933,t163]) ).
cnf(t8847,plain,
complement(meet(X1,sFlat6)) = join(sFlat7,complement(X1)),
inference(orient,[status(thm)],[t7934]) ).
cnf(t3470,plain,
X1 = join(meet(X1,sFlat6),meet(X1,sFlat7)),
inference(cp,[status(thm)],[t3413,t79]) ).
cnf(t3476,plain,
join(meet(X1,sFlat6),meet(X1,sFlat7)) = X1,
inference(orient,[status(thm)],[t3470]) ).
cnf(t10475,plain,
meet(complement(X1),meet(X1,X2)) = complement(top),
inference(cp,[status(thm)],[t9811,t10463]) ).
cnf(t36900,plain,
meet(complement(X1),meet(X1,X2)) = zero,
inference(step,[status(thm)],[t10475,t173]) ).
cnf(t12718,plain,
meet(complement(X1),meet(X1,X2)) = zero,
inference(orient,[status(thm)],[t36900]) ).
cnf(t7233,plain,
sFlat6 = complement(sFlat7),
inference(cp,[status(thm)],[t7187,t79]) ).
cnf(t7373,plain,
complement(sFlat7) = sFlat6,
inference(orient,[status(thm)],[t7233]) ).
cnf(t9842,plain,
meet(complement(X1),sFlat7) = complement(join(X1,sFlat6)),
inference(cp,[status(thm)],[t9811,t7373]) ).
cnf(t36626,plain,
meet(sFlat7,complement(X1)) = complement(join(X1,sFlat6)),
inference(step,[status(thm)],[t9842,t163]) ).
cnf(t9888,plain,
complement(join(X1,sFlat6)) = meet(sFlat7,complement(X1)),
inference(orient,[status(thm)],[t36626]) ).
cnf(t11180,plain,
composition(join(converse(sk2),X1),converse(sk1)) = join(converse(sFlat6),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t11149,t61]) ).
cnf(t19552,plain,
composition(join(converse(sk2),X1),converse(sk1)) = join(converse(sFlat6),composition(X1,converse(sk1))),
inference(orient,[status(thm)],[t11180]) ).
cnf(t19590,plain,
composition(converse(converse(sk1)),join(converse(converse(sk2)),X1)) = converse(join(converse(sFlat6),composition(converse(X1),converse(sk1)))),
inference(cp,[status(thm)],[t6058,t19552]) ).
cnf(t37395,plain,
composition(sk1,join(converse(converse(sk2)),X1)) = converse(join(converse(sFlat6),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t19590,t29]) ).
cnf(t37396,plain,
composition(sk1,join(sk2,X1)) = converse(join(converse(sFlat6),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t37395,t29]) ).
cnf(t37397,plain,
composition(sk1,join(sk2,X1)) = join(sFlat6,converse(composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t37396,t398]) ).
cnf(t37398,plain,
composition(sk1,join(sk2,X1)) = join(sFlat6,composition(converse(converse(sk1)),X1)),
inference(step,[status(thm)],[t37397,t363]) ).
cnf(t37399,plain,
composition(sk1,join(sk2,X1)) = join(sFlat6,composition(sk1,X1)),
inference(step,[status(thm)],[t37398,t29]) ).
cnf(t19616,plain,
composition(sk1,join(sk2,X1)) = join(sFlat6,composition(sk1,X1)),
inference(orient,[status(thm)],[t37399]) ).
cnf(t19631,plain,
join(sFlat6,composition(sk1,X1)) = composition(sk1,join(X1,sk2)),
inference(cp,[status(thm)],[t19616,t98]) ).
cnf(t19675,plain,
composition(sk1,join(X1,sk2)) = join(sFlat6,composition(sk1,X1)),
inference(orient,[status(thm)],[t19631]) ).
cnf(t9537,plain,
join(top,complement(X1)) = join(X2,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t638,t9485]) ).
cnf(t36729,plain,
top = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t9537,t2427]) ).
cnf(t11057,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t36729]) ).
cnf(t11066,plain,
meet(X1,complement(complement(meet(X2,complement(X1))))) = complement(top),
inference(cp,[status(thm)],[t10182,t11057]) ).
cnf(t36814,plain,
meet(X1,meet(X2,complement(X1))) = complement(top),
inference(step,[status(thm)],[t11066,t7187]) ).
cnf(t36815,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t36814,t173]) ).
cnf(t11428,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t36815]) ).
cnf(t11460,plain,
X1 = join(zero,meet(complement(meet(X2,complement(X1))),X1)),
inference(cp,[status(thm)],[t4956,t11428]) ).
cnf(t36870,plain,
X1 = meet(complement(meet(X2,complement(X1))),X1),
inference(step,[status(thm)],[t11460,t10863]) ).
cnf(t36871,plain,
X1 = meet(X1,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t36870,t163]) ).
cnf(t9532,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t9485,t7187]) ).
cnf(t10966,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t9532]) ).
cnf(t36872,plain,
X1 = meet(X1,join(complement(X2),X1)),
inference(step,[status(thm)],[t36871,t10966]) ).
cnf(t12146,plain,
meet(X1,join(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t36872]) ).
cnf(t12208,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t12146,t7187]) ).
cnf(t12234,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t12208]) ).
cnf(t9548,plain,
join(sk3,complement(sk2)) = complement(sFlat1),
inference(cp,[status(thm)],[t9547,t172]) ).
cnf(t9688,plain,
join(sk3,complement(sk2)) = complement(sFlat1),
inference(orient,[status(thm)],[t9548]) ).
cnf(t12245,plain,
complement(sk2) = meet(complement(sk2),complement(sFlat1)),
inference(cp,[status(thm)],[t12234,t9688]) ).
cnf(t9845,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t9811,t7187]) ).
cnf(t15292,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t9845]) ).
cnf(t37392,plain,
complement(sk2) = complement(join(sk2,sFlat1)),
inference(step,[status(thm)],[t12245,t15292]) ).
cnf(t37393,plain,
complement(sk2) = complement(join(sFlat1,sk2)),
inference(step,[status(thm)],[t37392,t98]) ).
cnf(t19441,plain,
complement(join(sFlat1,sk2)) = complement(sk2),
inference(orient,[status(thm)],[t37393]) ).
cnf(t19448,plain,
join(sFlat1,sk2) = complement(complement(sk2)),
inference(cp,[status(thm)],[t7187,t19441]) ).
cnf(t37394,plain,
join(sFlat1,sk2) = sk2,
inference(step,[status(thm)],[t19448,t7187]) ).
cnf(t19485,plain,
join(sFlat1,sk2) = sk2,
inference(orient,[status(thm)],[t37394]) ).
cnf(t19676,plain,
join(sFlat6,composition(sk1,sFlat1)) = composition(sk1,sk2),
inference(cp,[status(thm)],[t19675,t19485]) ).
cnf(t37400,plain,
join(sFlat6,sFlat2) = composition(sk1,sk2),
inference(step,[status(thm)],[t19676,t181]) ).
cnf(t37401,plain,
join(sFlat2,sFlat6) = composition(sk1,sk2),
inference(step,[status(thm)],[t37400,t98]) ).
cnf(t37402,plain,
join(sFlat2,sFlat6) = sFlat6,
inference(step,[status(thm)],[t37401,t61]) ).
cnf(t19706,plain,
join(sFlat2,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t37402]) ).
cnf(t19710,plain,
meet(sFlat7,complement(sFlat2)) = complement(sFlat6),
inference(cp,[status(thm)],[t9888,t19706]) ).
cnf(t37411,plain,
meet(sFlat7,sFlat3) = complement(sFlat6),
inference(step,[status(thm)],[t19710,t74]) ).
cnf(t37412,plain,
meet(sFlat3,sFlat7) = complement(sFlat6),
inference(step,[status(thm)],[t37411,t163]) ).
cnf(t37413,plain,
meet(sFlat3,sFlat7) = sFlat7,
inference(step,[status(thm)],[t37412,t79]) ).
cnf(t19715,plain,
meet(sFlat3,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t37413]) ).
cnf(t19718,plain,
zero = meet(complement(sFlat3),sFlat7),
inference(cp,[status(thm)],[t12718,t19715]) ).
cnf(t37418,plain,
zero = meet(sFlat7,complement(sFlat3)),
inference(step,[status(thm)],[t19718,t163]) ).
cnf(t37419,plain,
zero = meet(sFlat7,sFlat2),
inference(step,[status(thm)],[t37418,t7332]) ).
cnf(t37420,plain,
zero = meet(sFlat2,sFlat7),
inference(step,[status(thm)],[t37419,t163]) ).
cnf(t19729,plain,
meet(sFlat2,sFlat7) = zero,
inference(orient,[status(thm)],[t37420]) ).
cnf(t19732,plain,
sFlat2 = join(meet(sFlat2,sFlat6),zero),
inference(cp,[status(thm)],[t3476,t19729]) ).
cnf(t37424,plain,
sFlat2 = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t19732,t10899]) ).
cnf(t19742,plain,
meet(sFlat2,sFlat6) = sFlat2,
inference(orient,[status(thm)],[t37424]) ).
cnf(t19743,plain,
join(sFlat7,complement(sFlat2)) = complement(sFlat2),
inference(cp,[status(thm)],[t8847,t19742]) ).
cnf(t37428,plain,
join(sFlat7,sFlat3) = complement(sFlat2),
inference(step,[status(thm)],[t19743,t74]) ).
cnf(t37429,plain,
join(sFlat3,sFlat7) = complement(sFlat2),
inference(step,[status(thm)],[t37428,t98]) ).
cnf(t37430,plain,
join(sFlat3,sFlat7) = sFlat3,
inference(step,[status(thm)],[t37429,t74]) ).
cnf(t19756,plain,
join(sFlat3,sFlat7) = sFlat3,
inference(orient,[status(thm)],[t37430]) ).
cnf(t19757,plain,
join(sFlat8,sFlat3) = join(sFlat4,sFlat3),
inference(cp,[status(thm)],[t538,t19756]) ).
cnf(t37433,plain,
join(sFlat3,sFlat8) = join(sFlat4,sFlat3),
inference(step,[status(thm)],[t19757,t98]) ).
cnf(t37434,plain,
join(sFlat3,sFlat8) = join(sFlat3,sFlat4),
inference(step,[status(thm)],[t37433,t98]) ).
cnf(t37435,plain,
join(sFlat3,sFlat8) = sFlat5,
inference(step,[status(thm)],[t37434,t541]) ).
cnf(t19762,plain,
join(sFlat3,sFlat8) = sFlat5,
inference(orient,[status(thm)],[t37435]) ).
cnf(t38198,plain,
sFlat8 = sFlat5,
inference(step,[status(thm)],[t38197,t19762]) ).
cnf(t35942,plain,
sFlat8 = sFlat5,
inference(orient,[status(thm)],[t38198]) ).
cnf(t38199,plain,
join(sFlat4,sFlat7) = sFlat5,
inference(step,[status(thm)],[t116,t35942]) ).
cnf(t35943,plain,
join(sFlat4,sFlat7) = sFlat5,
inference(orient,[status(thm)],[t38199]) ).
cnf(goal_0,negated_conjecture,
join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(composition(sk1,sk3),complement(composition(sk1,meet(sk2,complement(sk3))))) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[goal_0,t98]) ).
cnf(g0_1,plain,
join(sFlat4,complement(composition(sk1,meet(sk2,complement(sk3))))) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_0,t56]) ).
cnf(g0_2,plain,
join(sFlat4,complement(composition(sk1,meet(sk2,sFlat0)))) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_1,t93]) ).
cnf(g0_3,plain,
join(sFlat4,complement(composition(sk1,meet(sFlat0,sk2)))) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_2,t163]) ).
cnf(g0_4,plain,
join(sFlat4,complement(composition(sk1,sFlat1))) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_3,t172]) ).
cnf(g0_5,plain,
join(sFlat4,complement(sFlat2)) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_4,t181]) ).
cnf(g0_6,plain,
join(sFlat4,sFlat3) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_5,t74]) ).
cnf(g0_7,plain,
join(sFlat3,sFlat4) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_6,t98]) ).
cnf(g0_8,plain,
sFlat5 != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_7,t541]) ).
cnf(g0_9,plain,
sFlat5 != join(composition(sk1,sk3),complement(composition(sk1,sk2))),
inference(rw,[status(thm)],[g0_8,t98]) ).
cnf(g0_10,plain,
sFlat5 != join(sFlat4,complement(composition(sk1,sk2))),
inference(rw,[status(thm)],[g0_9,t56]) ).
cnf(g0_11,plain,
sFlat5 != join(sFlat4,complement(sFlat6)),
inference(rw,[status(thm)],[g0_10,t61]) ).
cnf(g0_12,plain,
sFlat5 != join(sFlat4,sFlat7),
inference(rw,[status(thm)],[g0_11,t79]) ).
cnf(g0_13,plain,
sFlat5 != sFlat5,
inference(rw,[status(thm)],[g0_12,t35943]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL017-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Thu Sep 24 07:17:48 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 89.70/11.98 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 89.70/11.98 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------