%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL020-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.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:48 PM UTC 2026
% Result : Unsatisfiable 83.48s 12.42s
% Output : CNFRefutation 83.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 139
% Number of leaves : 18
% Syntax : Number of clauses : 576 ( 576 unt; 0 nHn; 126 RR)
% Number of literals : 576 ( 575 equ; 3 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 : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 725 ( 88 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t17,axiom,
sFlat0 = meet(sk1,one),
introduced(definition) ).
cnf(t85,plain,
meet(sk1,one) = sFlat0,
inference(orient,[status(thm)],[t17]) ).
cnf(t6,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t56,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t58,plain,
meet(X1,join(complement(X2),complement(X3))) = complement(join(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t56,t56]) ).
cnf(t760,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,join(complement(X2),complement(X3))),
inference(orient,[status(thm)],[t58]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t88,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t23515,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t88]) ).
cnf(t102,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t23515]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t42,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t2,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t44,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t42,t24]) ).
cnf(t158,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t159,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t158,t20]) ).
cnf(t23521,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t159,t24]) ).
cnf(t171,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t23521]) ).
cnf(t9,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t26,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t25,t20]) ).
cnf(t139,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t173,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t171,t139]) ).
cnf(t23523,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t173,t171]) ).
cnf(t192,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t23523]) ).
cnf(t195,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t102,t192]) ).
cnf(t172,plain,
one = converse(one),
inference(cp,[status(thm)],[t171,t20]) ).
cnf(t181,plain,
converse(one) = one,
inference(orient,[status(thm)],[t172]) ).
cnf(t23527,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t195,t181]) ).
cnf(t23528,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t23527,t192]) ).
cnf(t301,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t23528]) ).
cnf(t302,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t301,t56]) ).
cnf(t23611,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t302,t56]) ).
cnf(t23612,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t23611,t56]) ).
cnf(t1125,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t23612]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t22,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)],[t21,t21]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t90,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t96,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t90,t88]) ).
cnf(t23525,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t96,t90]) ).
cnf(t260,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t23525]) ).
cnf(t23534,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(complement(join(complement(X1),complement(X2))),X2)))),
inference(step,[status(thm)],[t22,t260]) ).
cnf(t23535,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)],[t23534,t88]) ).
cnf(t23536,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t23535,t56]) ).
cnf(t351,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t23536]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t97,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t101,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t56,t97]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t60,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t23516,plain,
zero = complement(top),
inference(step,[status(thm)],[t101,t60]) ).
cnf(t114,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t23516]) ).
cnf(t117,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t56,t114]) ).
cnf(t280,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t117]) ).
cnf(t23513,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t21,t56]) ).
cnf(t59,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t23513]) ).
cnf(t1309,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t59]) ).
cnf(t1326,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t1309,t301]) ).
cnf(t23633,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t1326,t88]) ).
cnf(t23634,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t23633,t60]) ).
cnf(t23635,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t23634,t88]) ).
cnf(t1367,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t23635]) ).
cnf(t1375,plain,
meet(top,complement(X1)) = complement(X1),
inference(cp,[status(thm)],[t280,t1367]) ).
cnf(t1376,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1375]) ).
cnf(t1384,plain,
join(complement(top),complement(complement(X1))) = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(cp,[status(thm)],[t351,t1376]) ).
cnf(t23636,plain,
join(zero,complement(complement(X1))) = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t1384,t114]) ).
cnf(t23637,plain,
X1 = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t23636,t1367]) ).
cnf(t23638,plain,
X1 = join(zero,complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t23637,t114]) ).
cnf(t23639,plain,
X1 = join(zero,complement(join(zero,join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t23638,t114]) ).
cnf(t23640,plain,
X1 = join(zero,complement(join(zero,complement(X1)))),
inference(step,[status(thm)],[t23639,t301]) ).
cnf(t23641,plain,
X1 = join(zero,meet(top,X1)),
inference(step,[status(thm)],[t23640,t280]) ).
cnf(t1385,plain,
join(zero,meet(top,X1)) = X1,
inference(orient,[status(thm)],[t23641]) ).
cnf(t1386,plain,
complement(X1) = join(zero,complement(X1)),
inference(cp,[status(thm)],[t1385,t1376]) ).
cnf(t1624,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1386]) ).
cnf(t287,plain,
meet(top,join(zero,complement(X1))) = complement(join(zero,meet(top,X1))),
inference(cp,[status(thm)],[t280,t280]) ).
cnf(t871,plain,
complement(join(zero,meet(top,X1))) = meet(top,join(zero,complement(X1))),
inference(orient,[status(thm)],[t287]) ).
cnf(t23642,plain,
complement(X1) = meet(top,join(zero,complement(X1))),
inference(step,[status(thm)],[t871,t1385]) ).
cnf(t1392,plain,
complement(X1) = meet(top,join(zero,complement(X1))),
inference(rw,[status(thm)],[t23642]) ).
cnf(t1421,plain,
meet(top,join(zero,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t1392]) ).
cnf(t310,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t56,t301]) ).
cnf(t314,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t310]) ).
cnf(t1426,plain,
complement(complement(X1)) = meet(top,join(zero,meet(X1,X1))),
inference(cp,[status(thm)],[t1421,t314]) ).
cnf(t1312,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t1309,t60]) ).
cnf(t23632,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t1312,t56]) ).
cnf(t1359,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t23632]) ).
cnf(t23650,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t1426,t1359]) ).
cnf(t1429,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t23650]) ).
cnf(t1629,plain,
complement(complement(X1)) = join(zero,meet(top,X1)),
inference(cp,[status(thm)],[t1624,t1429]) ).
cnf(t23687,plain,
meet(top,X1) = join(zero,meet(top,X1)),
inference(step,[status(thm)],[t1629,t1429]) ).
cnf(t23688,plain,
meet(top,X1) = X1,
inference(step,[status(thm)],[t23687,t1385]) ).
cnf(t1634,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t23688]) ).
cnf(t1638,plain,
meet(top,X1) = join(X1,meet(top,X1)),
inference(cp,[status(thm)],[t1125,t1634]) ).
cnf(t23695,plain,
X1 = join(X1,meet(top,X1)),
inference(step,[status(thm)],[t1638,t1634]) ).
cnf(t23696,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t23695,t1634]) ).
cnf(t1651,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t23696]) ).
cnf(t1653,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t1651,t260]) ).
cnf(t23711,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t1653,t90]) ).
cnf(t23712,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t23711,t1651]) ).
cnf(t1745,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t23712]) ).
cnf(t1748,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t1745,t1309]) ).
cnf(t23713,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t1748,t1309]) ).
cnf(t23714,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t23713,t88]) ).
cnf(t1751,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t23714]) ).
cnf(t1759,plain,
meet(X1,join(complement(complement(X1)),complement(X2))) = complement(complement(X1)),
inference(cp,[status(thm)],[t760,t1751]) ).
cnf(t23689,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t1429,t1634]) ).
cnf(t1635,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t23689]) ).
cnf(t23739,plain,
meet(X1,join(X1,complement(X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t1759,t1635]) ).
cnf(t23740,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t23739,t1635]) ).
cnf(t1883,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t23740]) ).
cnf(t1887,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t1883,t1635]) ).
cnf(t1892,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t1887]) ).
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(t63,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(t67,plain,
meet(composition(converse(X1),meet(converse(X2),composition(converse(converse(X1)),X3))),X3) = join(meet(converse(composition(X2,X1)),X3),meet(composition(converse(X1),meet(converse(X2),composition(converse(converse(X1)),X3))),X3)),
inference(cp,[status(thm)],[t63,t42]) ).
cnf(t89,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t56,t88]) ).
cnf(t23517,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t89,t56]) ).
cnf(t128,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t23517]) ).
cnf(t24736,plain,
meet(X3,composition(converse(X1),meet(converse(X2),composition(converse(converse(X1)),X3)))) = join(meet(converse(composition(X2,X1)),X3),meet(composition(converse(X1),meet(converse(X2),composition(converse(converse(X1)),X3))),X3)),
inference(step,[status(thm)],[t67,t128]) ).
cnf(t24737,plain,
meet(X3,composition(converse(X1),meet(converse(X2),composition(X1,X3)))) = join(meet(converse(composition(X2,X1)),X3),meet(composition(converse(X1),meet(converse(X2),composition(converse(converse(X1)),X3))),X3)),
inference(step,[status(thm)],[t24736,t24]) ).
cnf(t24738,plain,
meet(X3,composition(converse(X1),meet(converse(X2),composition(X1,X3)))) = join(meet(converse(composition(X2,X1)),X3),meet(X3,composition(converse(X1),meet(converse(X2),composition(converse(converse(X1)),X3))))),
inference(step,[status(thm)],[t24737,t128]) ).
cnf(t24739,plain,
meet(X3,composition(converse(X1),meet(converse(X2),composition(X1,X3)))) = join(meet(converse(composition(X2,X1)),X3),meet(X3,composition(converse(X1),meet(converse(X2),composition(X1,X3))))),
inference(step,[status(thm)],[t24738,t24]) ).
cnf(t22900,plain,
join(meet(converse(composition(X1,X2)),X3),meet(X3,composition(converse(X2),meet(converse(X1),composition(X2,X3))))) = meet(X3,composition(converse(X2),meet(converse(X1),composition(X2,X3)))),
inference(orient,[status(thm)],[t24739]) ).
cnf(t43,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t42,t24]) ).
cnf(t148,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t43]) ).
cnf(t149,plain,
composition(X1,converse(composition(X2,X3))) = converse(composition(X2,composition(X3,converse(X1)))),
inference(cp,[status(thm)],[t148,t25]) ).
cnf(t933,plain,
converse(composition(X1,composition(X2,converse(X3)))) = composition(X3,converse(composition(X1,X2))),
inference(orient,[status(thm)],[t149]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t110,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t112,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t110,t24]) ).
cnf(t225,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t112]) ).
cnf(t229,plain,
join(converse(X1),one) = converse(join(X1,one)),
inference(cp,[status(thm)],[t225,t181]) ).
cnf(t23524,plain,
join(one,converse(X1)) = converse(join(X1,one)),
inference(step,[status(thm)],[t229,t88]) ).
cnf(t242,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t23524]) ).
cnf(t244,plain,
converse(join(join(X1,one),X2)) = join(join(one,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t110,t242]) ).
cnf(t23543,plain,
converse(join(X1,join(one,X2))) = join(join(one,converse(X1)),converse(X2)),
inference(step,[status(thm)],[t244,t90]) ).
cnf(t23544,plain,
converse(join(X1,join(one,X2))) = join(one,join(converse(X1),converse(X2))),
inference(step,[status(thm)],[t23543,t90]) ).
cnf(t23545,plain,
converse(join(X1,join(one,X2))) = join(one,converse(join(X1,X2))),
inference(step,[status(thm)],[t23544,t110]) ).
cnf(t556,plain,
converse(join(X1,join(one,X2))) = join(one,converse(join(X1,X2))),
inference(orient,[status(thm)],[t23545]) ).
cnf(t111,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t110,t24]) ).
cnf(t198,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t111]) ).
cnf(t201,plain,
join(one,converse(X1)) = converse(join(one,X1)),
inference(cp,[status(thm)],[t198,t181]) ).
cnf(t214,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t201]) ).
cnf(t215,plain,
join(one,converse(complement(one))) = converse(top),
inference(cp,[status(thm)],[t214,t97]) ).
cnf(t373,plain,
join(one,converse(complement(one))) = converse(top),
inference(orient,[status(thm)],[t215]) ).
cnf(t559,plain,
join(one,converse(join(X1,converse(complement(one))))) = converse(join(X1,converse(top))),
inference(cp,[status(thm)],[t556,t373]) ).
cnf(t23546,plain,
join(one,join(converse(X1),complement(one))) = converse(join(X1,converse(top))),
inference(step,[status(thm)],[t559,t225]) ).
cnf(t100,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t90,t97]) ).
cnf(t326,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t100]) ).
cnf(t331,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t326,t88]) ).
cnf(t409,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t331]) ).
cnf(t23547,plain,
join(top,converse(X1)) = converse(join(X1,converse(top))),
inference(step,[status(thm)],[t23546,t409]) ).
cnf(t23548,plain,
join(top,converse(X1)) = join(converse(X1),top),
inference(step,[status(thm)],[t23547,t225]) ).
cnf(t330,plain,
join(top,complement(complement(X1))) = join(X1,top),
inference(cp,[status(thm)],[t326,t97]) ).
cnf(t329,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t326,t301]) ).
cnf(t23532,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t329,t97]) ).
cnf(t343,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t23532]) ).
cnf(t23533,plain,
top = join(X1,top),
inference(step,[status(thm)],[t330,t343]) ).
cnf(t347,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t23533]) ).
cnf(t23549,plain,
join(top,converse(X1)) = top,
inference(step,[status(thm)],[t23548,t347]) ).
cnf(t581,plain,
join(top,converse(X1)) = top,
inference(orient,[status(thm)],[t23549]) ).
cnf(t350,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t198,t347]) ).
cnf(t370,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t350]) ).
cnf(t582,plain,
top = converse(top),
inference(cp,[status(thm)],[t581,t370]) ).
cnf(t591,plain,
converse(top) = top,
inference(orient,[status(thm)],[t582]) ).
cnf(t937,plain,
composition(top,converse(composition(X1,X2))) = converse(composition(X1,composition(X2,top))),
inference(cp,[status(thm)],[t933,t591]) ).
cnf(t2211,plain,
converse(composition(X1,composition(X2,top))) = composition(top,converse(composition(X1,X2))),
inference(orient,[status(thm)],[t937]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t51,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t2216,plain,
composition(top,converse(composition(X1,sk1))) = converse(composition(X1,sk1)),
inference(cp,[status(thm)],[t2211,t51]) ).
cnf(t3266,plain,
composition(top,converse(composition(X1,sk1))) = converse(composition(X1,sk1)),
inference(orient,[status(thm)],[t2216]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t37,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t39,plain,
composition(join(composition(X1,X2),X3),Y3) = join(composition(X1,composition(X2,Y3)),composition(X3,Y3)),
inference(cp,[status(thm)],[t37,t25]) ).
cnf(t7905,plain,
join(composition(X1,composition(X2,X3)),composition(Y3,X3)) = composition(join(composition(X1,X2),Y3),X3),
inference(orient,[status(thm)],[t39]) ).
cnf(t7961,plain,
composition(join(composition(X1,sk1),X2),top) = join(composition(X1,sk1),composition(X2,top)),
inference(cp,[status(thm)],[t7905,t51]) ).
cnf(t8107,plain,
composition(join(composition(X1,sk1),X2),top) = join(composition(X1,sk1),composition(X2,top)),
inference(orient,[status(thm)],[t7961]) ).
cnf(t8130,plain,
join(composition(X1,sk1),composition(X2,top)) = composition(join(X2,composition(X1,sk1)),top),
inference(cp,[status(thm)],[t8107,t88]) ).
cnf(t8345,plain,
composition(join(X1,composition(X2,sk1)),top) = join(composition(X2,sk1),composition(X1,top)),
inference(orient,[status(thm)],[t8130]) ).
cnf(t163,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t110,t158]) ).
cnf(t2577,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t163]) ).
cnf(t45,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t37,t42]) ).
cnf(t9700,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t45]) ).
cnf(t9796,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)],[t2577,t9700]) ).
cnf(t24156,plain,
join(composition(X1,X2),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t9796,t24]) ).
cnf(t24157,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t24156,t24]) ).
cnf(t207,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t42,t198]) ).
cnf(t2741,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t207]) ).
cnf(t24158,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(converse(converse(X1)),join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t24157,t2741]) ).
cnf(t24159,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t24158,t24]) ).
cnf(t24160,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t24159,t24]) ).
cnf(t9803,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t24160]) ).
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(t27,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(t32,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)],[t27,t20]) ).
cnf(t23901,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)],[t32,t192]) ).
cnf(t23902,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)],[t23901,t20]) ).
cnf(t23903,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)],[t23902,t128]) ).
cnf(t23904,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)],[t23903,t192]) ).
cnf(t4982,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)],[t23904]) ).
cnf(t1320,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t1309,t56]) ).
cnf(t23732,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t1320,t88]) ).
cnf(t1816,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t23732]) ).
cnf(t1819,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t1816,t128]) ).
cnf(t2274,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t1819]) ).
cnf(t1640,plain,
meet(X1,join(complement(top),complement(X2))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t760,t1634]) ).
cnf(t23733,plain,
meet(X1,join(zero,complement(X2))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t1640,t114]) ).
cnf(t23734,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t23733,t1624]) ).
cnf(t1831,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t23734]) ).
cnf(t1855,plain,
join(complement(X1),X2) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t1635,t1831]) ).
cnf(t4231,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t1855]) ).
cnf(t4255,plain,
meet(meet(X1,complement(X2)),complement(X3)) = complement(join(join(complement(X1),X2),X3)),
inference(cp,[status(thm)],[t1831,t4231]) ).
cnf(t23925,plain,
meet(meet(X1,complement(X2)),complement(X3)) = complement(join(complement(X1),join(X2,X3))),
inference(step,[status(thm)],[t4255,t90]) ).
cnf(t23926,plain,
meet(meet(X1,complement(X2)),complement(X3)) = meet(X1,complement(join(X2,X3))),
inference(step,[status(thm)],[t23925,t1831]) ).
cnf(t5285,plain,
meet(meet(X1,complement(X2)),complement(X3)) = meet(X1,complement(join(X2,X3))),
inference(orient,[status(thm)],[t23926]) ).
cnf(t5313,plain,
meet(X1,complement(join(complement(X2),X3))) = meet(meet(X1,X2),complement(X3)),
inference(cp,[status(thm)],[t5285,t1635]) ).
cnf(t23927,plain,
meet(X1,meet(X2,complement(X3))) = meet(meet(X1,X2),complement(X3)),
inference(step,[status(thm)],[t5313,t1831]) ).
cnf(t5337,plain,
meet(meet(X1,X2),complement(X3)) = meet(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t23927]) ).
cnf(t5396,plain,
meet(X1,meet(X2,complement(complement(X3)))) = meet(meet(X1,X2),X3),
inference(cp,[status(thm)],[t5337,t1635]) ).
cnf(t23928,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t5396,t1635]) ).
cnf(t5417,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t23928]) ).
cnf(t5486,plain,
meet(sk1,meet(one,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t5417,t85]) ).
cnf(t5572,plain,
meet(sk1,meet(one,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t5486]) ).
cnf(t332,plain,
join(top,join(X1,X2)) = join(X3,join(X1,join(complement(X3),X2))),
inference(cp,[status(thm)],[t326,t260]) ).
cnf(t23651,plain,
meet(X1,X1) = meet(top,X1),
inference(step,[status(thm)],[t314,t1429]) ).
cnf(t1455,plain,
meet(X1,X1) = meet(top,X1),
inference(rw,[status(thm)],[t23651]) ).
cnf(t1457,plain,
meet(X1,X1) = meet(top,X1),
inference(orient,[status(thm)],[t1455]) ).
cnf(t23691,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t1457,t1634]) ).
cnf(t1647,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t23691]) ).
cnf(t1664,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1647]) ).
cnf(t23698,plain,
join(zero,X1) = X1,
inference(step,[status(thm)],[t1359,t1664]) ).
cnf(t1673,plain,
join(zero,X1) = X1,
inference(rw,[status(thm)],[t23698]) ).
cnf(t1684,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t1673]) ).
cnf(t1692,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t225,t1684]) ).
cnf(t23708,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t1692,t24]) ).
cnf(t1711,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t23708]) ).
cnf(t1717,plain,
join(X1,complement(converse(zero))) = join(top,X1),
inference(cp,[status(thm)],[t1711,t409]) ).
cnf(t1464,plain,
meet(X1,X1) = meet(X1,top),
inference(cp,[status(thm)],[t1457,t128]) ).
cnf(t1469,plain,
meet(X1,X1) = meet(X1,top),
inference(orient,[status(thm)],[t1464]) ).
cnf(t23697,plain,
X1 = meet(X1,top),
inference(step,[status(thm)],[t1469,t1664]) ).
cnf(t1672,plain,
X1 = meet(X1,top),
inference(rw,[status(thm)],[t23697]) ).
cnf(t1677,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t1672]) ).
cnf(t1680,plain,
X1 = join(X1,complement(join(complement(X1),top))),
inference(cp,[status(thm)],[t1309,t1677]) ).
cnf(t23706,plain,
X1 = join(X1,complement(top)),
inference(step,[status(thm)],[t1680,t347]) ).
cnf(t23707,plain,
X1 = join(X1,zero),
inference(step,[status(thm)],[t23706,t114]) ).
cnf(t1701,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t23707]) ).
cnf(t1712,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t1711,t1701]) ).
cnf(t1731,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t1712]) ).
cnf(t23816,plain,
join(X1,complement(zero)) = join(top,X1),
inference(step,[status(thm)],[t1717,t1731]) ).
cnf(t320,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t97,t314]) ).
cnf(t491,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t320]) ).
cnf(t1323,plain,
X1 = join(meet(X1,meet(X1,X1)),complement(top)),
inference(cp,[status(thm)],[t1309,t491]) ).
cnf(t23674,plain,
X1 = join(complement(top),meet(X1,meet(X1,X1))),
inference(step,[status(thm)],[t1323,t88]) ).
cnf(t23675,plain,
X1 = join(zero,meet(X1,meet(X1,X1))),
inference(step,[status(thm)],[t23674,t114]) ).
cnf(t1600,plain,
join(zero,meet(X1,meet(X1,X1))) = X1,
inference(orient,[status(thm)],[t23675]) ).
cnf(t1601,plain,
top = meet(top,top),
inference(cp,[status(thm)],[t1600,t1385]) ).
cnf(t282,plain,
meet(top,top) = complement(join(zero,zero)),
inference(cp,[status(thm)],[t280,t114]) ).
cnf(t289,plain,
complement(join(zero,zero)) = meet(top,top),
inference(orient,[status(thm)],[t282]) ).
cnf(t305,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t301,t114]) ).
cnf(t23529,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t305,t114]) ).
cnf(t23530,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t23529,t114]) ).
cnf(t311,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t23530]) ).
cnf(t23531,plain,
complement(zero) = meet(top,top),
inference(step,[status(thm)],[t289,t311]) ).
cnf(t312,plain,
complement(zero) = meet(top,top),
inference(rw,[status(thm)],[t23531]) ).
cnf(t313,plain,
meet(top,top) = complement(zero),
inference(orient,[status(thm)],[t312]) ).
cnf(t23676,plain,
top = complement(zero),
inference(step,[status(thm)],[t1601,t313]) ).
cnf(t1607,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t23676]) ).
cnf(t23817,plain,
join(X1,top) = join(top,X1),
inference(step,[status(thm)],[t23816,t1607]) ).
cnf(t23818,plain,
top = join(top,X1),
inference(step,[status(thm)],[t23817,t347]) ).
cnf(t3518,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t23818]) ).
cnf(t23823,plain,
top = join(X3,join(X1,join(complement(X3),X2))),
inference(step,[status(thm)],[t332,t3518]) ).
cnf(t3523,plain,
join(X1,join(X2,join(complement(X1),X3))) = top,
inference(orient,[status(thm)],[t23823]) ).
cnf(t3551,plain,
meet(X1,complement(join(X2,join(complement(complement(X1)),X3)))) = complement(top),
inference(cp,[status(thm)],[t1831,t3523]) ).
cnf(t23824,plain,
meet(X1,complement(join(X2,join(X1,X3)))) = complement(top),
inference(step,[status(thm)],[t3551,t1635]) ).
cnf(t23825,plain,
meet(X1,complement(join(X2,join(X1,X3)))) = zero,
inference(step,[status(thm)],[t23824,t114]) ).
cnf(t3585,plain,
meet(X1,complement(join(X2,join(X1,X3)))) = zero,
inference(orient,[status(thm)],[t23825]) ).
cnf(t3598,plain,
zero = meet(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t3585,t1751]) ).
cnf(t3683,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t3598]) ).
cnf(t3685,plain,
zero = meet(X1,meet(X2,complement(X1))),
inference(cp,[status(thm)],[t3683,t1831]) ).
cnf(t3851,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t3685]) ).
cnf(t105,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t102,t20]) ).
cnf(t781,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t105]) ).
cnf(t792,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t781,t24]) ).
cnf(t2929,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t792]) ).
cnf(t2956,plain,
meet(one,complement(composition(X1,complement(converse(X1))))) = complement(complement(one)),
inference(cp,[status(thm)],[t1831,t2929]) ).
cnf(t23815,plain,
meet(one,complement(composition(X1,complement(converse(X1))))) = one,
inference(step,[status(thm)],[t2956,t1635]) ).
cnf(t3485,plain,
meet(one,complement(composition(X1,complement(converse(X1))))) = one,
inference(orient,[status(thm)],[t23815]) ).
cnf(t3508,plain,
one = meet(one,complement(composition(converse(X1),complement(X1)))),
inference(cp,[status(thm)],[t3485,t24]) ).
cnf(t5254,plain,
meet(one,complement(composition(converse(X1),complement(X1)))) = one,
inference(orient,[status(thm)],[t3508]) ).
cnf(t5284,plain,
zero = meet(composition(converse(X1),complement(X1)),one),
inference(cp,[status(thm)],[t3851,t5254]) ).
cnf(t23973,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t5284,t128]) ).
cnf(t6077,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t23973]) ).
cnf(t6108,plain,
meet(sFlat0,composition(converse(X1),complement(X1))) = meet(sk1,zero),
inference(cp,[status(thm)],[t5572,t6077]) ).
cnf(t1611,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t56,t1607]) ).
cnf(t23681,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t1611,t347]) ).
cnf(t23682,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t23681,t114]) ).
cnf(t1621,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t23682]) ).
cnf(t24200,plain,
meet(sFlat0,composition(converse(X1),complement(X1))) = zero,
inference(step,[status(thm)],[t6108,t1621]) ).
cnf(t10884,plain,
meet(sFlat0,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t24200]) ).
cnf(t10918,plain,
composition(meet(X1,composition(complement(X1),converse(sFlat0))),meet(sFlat0,composition(converse(X1),complement(X1)))) = join(meet(composition(X1,sFlat0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sFlat0))),zero)),
inference(cp,[status(thm)],[t27,t10884]) ).
cnf(t24201,plain,
composition(meet(X1,composition(complement(X1),converse(sFlat0))),zero) = join(meet(composition(X1,sFlat0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sFlat0))),zero)),
inference(step,[status(thm)],[t10918,t10884]) ).
cnf(t589,plain,
top = join(top,composition(X1,converse(X2))),
inference(cp,[status(thm)],[t581,t148]) ).
cnf(t673,plain,
join(top,composition(X1,converse(X2))) = top,
inference(orient,[status(thm)],[t589]) ).
cnf(t683,plain,
top = join(top,composition(X1,X2)),
inference(cp,[status(thm)],[t673,t24]) ).
cnf(t687,plain,
join(top,composition(X1,X2)) = top,
inference(orient,[status(thm)],[t683]) ).
cnf(t193,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t37,t192]) ).
cnf(t420,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t193]) ).
cnf(t425,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t420,t347]) ).
cnf(t458,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t425]) ).
cnf(t688,plain,
top = composition(top,top),
inference(cp,[status(thm)],[t687,t458]) ).
cnf(t692,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t688]) ).
cnf(t696,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t102,t692]) ).
cnf(t23559,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t696,t114]) ).
cnf(t194,plain,
composition(join(X1,one),X2) = join(composition(X1,X2),X2),
inference(cp,[status(thm)],[t37,t192]) ).
cnf(t23541,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(step,[status(thm)],[t194,t88]) ).
cnf(t444,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t23541]) ).
cnf(t23560,plain,
zero = composition(join(converse(top),one),complement(top)),
inference(step,[status(thm)],[t23559,t444]) ).
cnf(t23561,plain,
zero = composition(join(one,converse(top)),complement(top)),
inference(step,[status(thm)],[t23560,t88]) ).
cnf(t23562,plain,
zero = composition(converse(top),complement(top)),
inference(step,[status(thm)],[t23561,t370]) ).
cnf(t23563,plain,
zero = composition(top,complement(top)),
inference(step,[status(thm)],[t23562,t591]) ).
cnf(t23564,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t23563,t114]) ).
cnf(t698,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t23564]) ).
cnf(t701,plain,
composition(join(X1,top),zero) = join(composition(X1,zero),zero),
inference(cp,[status(thm)],[t37,t698]) ).
cnf(t23569,plain,
composition(top,zero) = join(composition(X1,zero),zero),
inference(step,[status(thm)],[t701,t347]) ).
cnf(t23570,plain,
zero = join(composition(X1,zero),zero),
inference(step,[status(thm)],[t23569,t698]) ).
cnf(t23571,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t23570,t88]) ).
cnf(t736,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t23571]) ).
cnf(t23704,plain,
composition(X1,zero) = zero,
inference(step,[status(thm)],[t736,t1684]) ).
cnf(t1699,plain,
composition(X1,zero) = zero,
inference(rw,[status(thm)],[t23704]) ).
cnf(t1708,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t1699]) ).
cnf(t24202,plain,
zero = join(meet(composition(X1,sFlat0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sFlat0))),zero)),
inference(step,[status(thm)],[t24201,t1708]) ).
cnf(t24203,plain,
zero = join(meet(complement(X1),composition(X1,sFlat0)),composition(meet(X1,composition(complement(X1),converse(sFlat0))),zero)),
inference(step,[status(thm)],[t24202,t128]) ).
cnf(t24204,plain,
zero = join(meet(complement(X1),composition(X1,sFlat0)),zero),
inference(step,[status(thm)],[t24203,t1708]) ).
cnf(t24205,plain,
zero = meet(complement(X1),composition(X1,sFlat0)),
inference(step,[status(thm)],[t24204,t1701]) ).
cnf(t10922,plain,
meet(complement(X1),composition(X1,sFlat0)) = zero,
inference(orient,[status(thm)],[t24205]) ).
cnf(t10940,plain,
composition(X1,sFlat0) = join(meet(composition(X1,sFlat0),X1),zero),
inference(cp,[status(thm)],[t2274,t10922]) ).
cnf(t24206,plain,
composition(X1,sFlat0) = meet(composition(X1,sFlat0),X1),
inference(step,[status(thm)],[t10940,t1701]) ).
cnf(t24207,plain,
composition(X1,sFlat0) = meet(X1,composition(X1,sFlat0)),
inference(step,[status(thm)],[t24206,t128]) ).
cnf(t10944,plain,
meet(X1,composition(X1,sFlat0)) = composition(X1,sFlat0),
inference(orient,[status(thm)],[t24207]) ).
cnf(t10969,plain,
composition(meet(one,converse(sFlat0)),meet(sFlat0,converse(one))) = join(composition(one,sFlat0),composition(meet(one,converse(sFlat0)),meet(sFlat0,converse(one)))),
inference(cp,[status(thm)],[t4982,t10944]) ).
cnf(t1757,plain,
join(one,converse(meet(one,X1))) = converse(one),
inference(cp,[status(thm)],[t214,t1751]) ).
cnf(t23755,plain,
join(one,converse(meet(one,X1))) = one,
inference(step,[status(thm)],[t1757,t181]) ).
cnf(t2204,plain,
join(one,converse(meet(one,X1))) = one,
inference(orient,[status(thm)],[t23755]) ).
cnf(t2205,plain,
one = join(one,converse(meet(X1,one))),
inference(cp,[status(thm)],[t2204,t128]) ).
cnf(t3896,plain,
join(one,converse(meet(X1,one))) = one,
inference(orient,[status(thm)],[t2205]) ).
cnf(t3898,plain,
one = join(one,converse(sFlat0)),
inference(cp,[status(thm)],[t3896,t85]) ).
cnf(t3910,plain,
join(one,converse(sFlat0)) = one,
inference(orient,[status(thm)],[t3898]) ).
cnf(t3912,plain,
zero = meet(converse(sFlat0),complement(one)),
inference(cp,[status(thm)],[t3683,t3910]) ).
cnf(t4379,plain,
meet(converse(sFlat0),complement(one)) = zero,
inference(orient,[status(thm)],[t3912]) ).
cnf(t4382,plain,
converse(sFlat0) = join(zero,meet(complement(complement(one)),converse(sFlat0))),
inference(cp,[status(thm)],[t2274,t4379]) ).
cnf(t23885,plain,
converse(sFlat0) = meet(complement(complement(one)),converse(sFlat0)),
inference(step,[status(thm)],[t4382,t1684]) ).
cnf(t23886,plain,
converse(sFlat0) = meet(converse(sFlat0),complement(complement(one))),
inference(step,[status(thm)],[t23885,t128]) ).
cnf(t23887,plain,
converse(sFlat0) = meet(converse(sFlat0),one),
inference(step,[status(thm)],[t23886,t1635]) ).
cnf(t23888,plain,
converse(sFlat0) = meet(one,converse(sFlat0)),
inference(step,[status(thm)],[t23887,t128]) ).
cnf(t4385,plain,
meet(one,converse(sFlat0)) = converse(sFlat0),
inference(orient,[status(thm)],[t23888]) ).
cnf(t24208,plain,
composition(converse(sFlat0),meet(sFlat0,converse(one))) = join(composition(one,sFlat0),composition(meet(one,converse(sFlat0)),meet(sFlat0,converse(one)))),
inference(step,[status(thm)],[t10969,t4385]) ).
cnf(t24209,plain,
composition(converse(sFlat0),meet(sFlat0,one)) = join(composition(one,sFlat0),composition(meet(one,converse(sFlat0)),meet(sFlat0,converse(one)))),
inference(step,[status(thm)],[t24208,t181]) ).
cnf(t1369,plain,
join(complement(X1),complement(X2)) = join(zero,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t1367,t56]) ).
cnf(t23741,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t1369,t1624]) ).
cnf(t1909,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t23741]) ).
cnf(t3705,plain,
zero = meet(complement(X1),complement(complement(meet(X2,X1)))),
inference(cp,[status(thm)],[t3683,t1909]) ).
cnf(t57,plain,
meet(join(complement(X1),complement(X2)),X3) = complement(join(meet(X1,X2),complement(X3))),
inference(cp,[status(thm)],[t56,t56]) ).
cnf(t738,plain,
complement(join(meet(X1,X2),complement(X3))) = meet(join(complement(X1),complement(X2)),X3),
inference(orient,[status(thm)],[t57]) ).
cnf(t1641,plain,
meet(join(complement(top),complement(X1)),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t738,t1634]) ).
cnf(t23756,plain,
meet(complement(meet(top,X1)),X2) = complement(join(X1,complement(X2))),
inference(step,[status(thm)],[t1641,t1909]) ).
cnf(t1433,plain,
meet(top,join(zero,complement(X1))) = complement(meet(top,X1)),
inference(cp,[status(thm)],[t1429,t280]) ).
cnf(t23662,plain,
complement(X1) = complement(meet(top,X1)),
inference(step,[status(thm)],[t1433,t1421]) ).
cnf(t1542,plain,
complement(meet(top,X1)) = complement(X1),
inference(orient,[status(thm)],[t23662]) ).
cnf(t23757,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(step,[status(thm)],[t23756,t1542]) ).
cnf(t2242,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t23757]) ).
cnf(t2250,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t2242,t1635]) ).
cnf(t2294,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t2250]) ).
cnf(t23835,plain,
zero = complement(join(X1,complement(meet(X2,X1)))),
inference(step,[status(thm)],[t3705,t2294]) ).
cnf(t23836,plain,
zero = meet(complement(X1),meet(X2,X1)),
inference(step,[status(thm)],[t23835,t2242]) ).
cnf(t3863,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t23836]) ).
cnf(t3870,plain,
zero = meet(complement(one),sFlat0),
inference(cp,[status(thm)],[t3863,t85]) ).
cnf(t23837,plain,
zero = meet(sFlat0,complement(one)),
inference(step,[status(thm)],[t3870,t128]) ).
cnf(t3873,plain,
meet(sFlat0,complement(one)) = zero,
inference(orient,[status(thm)],[t23837]) ).
cnf(t3875,plain,
sFlat0 = join(zero,meet(complement(complement(one)),sFlat0)),
inference(cp,[status(thm)],[t2274,t3873]) ).
cnf(t23838,plain,
sFlat0 = meet(complement(complement(one)),sFlat0),
inference(step,[status(thm)],[t3875,t1684]) ).
cnf(t23839,plain,
sFlat0 = meet(sFlat0,complement(complement(one))),
inference(step,[status(thm)],[t23838,t128]) ).
cnf(t23840,plain,
sFlat0 = meet(sFlat0,one),
inference(step,[status(thm)],[t23839,t1635]) ).
cnf(t3878,plain,
meet(sFlat0,one) = sFlat0,
inference(orient,[status(thm)],[t23840]) ).
cnf(t24210,plain,
composition(converse(sFlat0),sFlat0) = join(composition(one,sFlat0),composition(meet(one,converse(sFlat0)),meet(sFlat0,converse(one)))),
inference(step,[status(thm)],[t24209,t3878]) ).
cnf(t24211,plain,
composition(converse(sFlat0),sFlat0) = join(sFlat0,composition(meet(one,converse(sFlat0)),meet(sFlat0,converse(one)))),
inference(step,[status(thm)],[t24210,t192]) ).
cnf(t24212,plain,
composition(converse(sFlat0),sFlat0) = join(sFlat0,composition(converse(sFlat0),meet(sFlat0,converse(one)))),
inference(step,[status(thm)],[t24211,t4385]) ).
cnf(t24213,plain,
composition(converse(sFlat0),sFlat0) = join(sFlat0,composition(converse(sFlat0),meet(sFlat0,one))),
inference(step,[status(thm)],[t24212,t181]) ).
cnf(t24214,plain,
composition(converse(sFlat0),sFlat0) = join(sFlat0,composition(converse(sFlat0),sFlat0)),
inference(step,[status(thm)],[t24213,t3878]) ).
cnf(t3920,plain,
join(X1,composition(converse(sFlat0),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t420,t3910]) ).
cnf(t24155,plain,
join(X1,composition(converse(sFlat0),X1)) = X1,
inference(step,[status(thm)],[t3920,t192]) ).
cnf(t9649,plain,
join(X1,composition(converse(sFlat0),X1)) = X1,
inference(orient,[status(thm)],[t24155]) ).
cnf(t24215,plain,
composition(converse(sFlat0),sFlat0) = sFlat0,
inference(step,[status(thm)],[t24214,t9649]) ).
cnf(t10981,plain,
composition(converse(sFlat0),sFlat0) = sFlat0,
inference(orient,[status(thm)],[t24215]) ).
cnf(t11002,plain,
composition(converse(sFlat0),sFlat0) = converse(sFlat0),
inference(cp,[status(thm)],[t158,t10981]) ).
cnf(t24216,plain,
sFlat0 = converse(sFlat0),
inference(step,[status(thm)],[t11002,t10981]) ).
cnf(t11021,plain,
converse(sFlat0) = sFlat0,
inference(orient,[status(thm)],[t24216]) ).
cnf(t24217,plain,
composition(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t10981,t11021]) ).
cnf(t11100,plain,
composition(sFlat0,sFlat0) = sFlat0,
inference(rw,[status(thm)],[t24217]) ).
cnf(t11614,plain,
composition(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t11100]) ).
cnf(t11615,plain,
composition(sFlat0,join(sFlat0,X1)) = join(sFlat0,composition(sFlat0,X1)),
inference(cp,[status(thm)],[t9803,t11614]) ).
cnf(t12182,plain,
composition(sFlat0,join(sFlat0,X1)) = join(sFlat0,composition(sFlat0,X1)),
inference(orient,[status(thm)],[t11615]) ).
cnf(t1754,plain,
sk1 = join(sk1,sFlat0),
inference(cp,[status(thm)],[t1751,t85]) ).
cnf(t23718,plain,
sk1 = join(sFlat0,sk1),
inference(step,[status(thm)],[t1754,t88]) ).
cnf(t1769,plain,
join(sFlat0,sk1) = sk1,
inference(orient,[status(thm)],[t23718]) ).
cnf(t12188,plain,
join(sFlat0,composition(sFlat0,sk1)) = composition(sFlat0,sk1),
inference(cp,[status(thm)],[t12182,t1769]) ).
cnf(t12447,plain,
join(sFlat0,composition(sFlat0,sk1)) = composition(sFlat0,sk1),
inference(orient,[status(thm)],[t12188]) ).
cnf(t12453,plain,
join(composition(sFlat0,sk1),composition(sFlat0,top)) = composition(composition(sFlat0,sk1),top),
inference(cp,[status(thm)],[t8345,t12447]) ).
cnf(t24276,plain,
composition(sFlat0,join(sk1,top)) = composition(composition(sFlat0,sk1),top),
inference(step,[status(thm)],[t12453,t9803]) ).
cnf(t24277,plain,
composition(sFlat0,top) = composition(composition(sFlat0,sk1),top),
inference(step,[status(thm)],[t24276,t347]) ).
cnf(t24278,plain,
composition(sFlat0,top) = composition(sFlat0,composition(sk1,top)),
inference(step,[status(thm)],[t24277,t25]) ).
cnf(t24279,plain,
composition(sFlat0,top) = composition(sFlat0,sk1),
inference(step,[status(thm)],[t24278,t51]) ).
cnf(t12460,plain,
composition(sFlat0,sk1) = composition(sFlat0,top),
inference(orient,[status(thm)],[t24279]) ).
cnf(t12475,plain,
converse(composition(sFlat0,sk1)) = composition(top,converse(composition(sFlat0,top))),
inference(cp,[status(thm)],[t3266,t12460]) ).
cnf(t11025,plain,
converse(composition(sFlat0,X1)) = composition(converse(X1),sFlat0),
inference(cp,[status(thm)],[t42,t11021]) ).
cnf(t11402,plain,
converse(composition(sFlat0,X1)) = composition(converse(X1),sFlat0),
inference(orient,[status(thm)],[t11025]) ).
cnf(t24280,plain,
composition(converse(sk1),sFlat0) = composition(top,converse(composition(sFlat0,top))),
inference(step,[status(thm)],[t12475,t11402]) ).
cnf(t24281,plain,
composition(converse(sk1),sFlat0) = composition(top,composition(converse(top),sFlat0)),
inference(step,[status(thm)],[t24280,t11402]) ).
cnf(t24282,plain,
composition(converse(sk1),sFlat0) = composition(top,composition(top,sFlat0)),
inference(step,[status(thm)],[t24281,t591]) ).
cnf(t695,plain,
composition(top,composition(top,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t25,t692]) ).
cnf(t720,plain,
composition(top,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t695]) ).
cnf(t24283,plain,
composition(converse(sk1),sFlat0) = composition(top,sFlat0),
inference(step,[status(thm)],[t24282,t720]) ).
cnf(t12486,plain,
composition(converse(sk1),sFlat0) = composition(top,sFlat0),
inference(orient,[status(thm)],[t24283]) ).
cnf(t65,plain,
meet(composition(X1,meet(one,composition(converse(X1),X2))),X2) = join(meet(X1,X2),meet(composition(X1,meet(one,composition(converse(X1),X2))),X2)),
inference(cp,[status(thm)],[t63,t20]) ).
cnf(t24562,plain,
meet(X2,composition(X1,meet(one,composition(converse(X1),X2)))) = join(meet(X1,X2),meet(composition(X1,meet(one,composition(converse(X1),X2))),X2)),
inference(step,[status(thm)],[t65,t128]) ).
cnf(t24563,plain,
meet(X2,composition(X1,meet(one,composition(converse(X1),X2)))) = join(meet(X1,X2),meet(X2,composition(X1,meet(one,composition(converse(X1),X2))))),
inference(step,[status(thm)],[t24562,t128]) ).
cnf(t19003,plain,
join(meet(X1,X2),meet(X2,composition(X1,meet(one,composition(converse(X1),X2))))) = meet(X2,composition(X1,meet(one,composition(converse(X1),X2)))),
inference(orient,[status(thm)],[t24563]) ).
cnf(t19114,plain,
meet(top,composition(X1,meet(one,composition(converse(X1),top)))) = join(meet(X1,top),composition(X1,meet(one,composition(converse(X1),top)))),
inference(cp,[status(thm)],[t19003,t1634]) ).
cnf(t24569,plain,
composition(X1,meet(one,composition(converse(X1),top))) = join(meet(X1,top),composition(X1,meet(one,composition(converse(X1),top)))),
inference(step,[status(thm)],[t19114,t1634]) ).
cnf(t24570,plain,
composition(X1,meet(one,composition(converse(X1),top))) = join(X1,composition(X1,meet(one,composition(converse(X1),top)))),
inference(step,[status(thm)],[t24569,t1677]) ).
cnf(t442,plain,
join(X1,converse(composition(X2,converse(X1)))) = converse(composition(join(one,X2),converse(X1))),
inference(cp,[status(thm)],[t198,t420]) ).
cnf(t23619,plain,
join(X1,composition(X1,converse(X2))) = converse(composition(join(one,X2),converse(X1))),
inference(step,[status(thm)],[t442,t148]) ).
cnf(t23620,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,converse(join(one,X2))),
inference(step,[status(thm)],[t23619,t148]) ).
cnf(t23621,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(step,[status(thm)],[t23620,t214]) ).
cnf(t1135,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(orient,[status(thm)],[t23621]) ).
cnf(t1154,plain,
composition(X1,join(one,converse(converse(X2)))) = join(X1,composition(X1,X2)),
inference(cp,[status(thm)],[t1135,t24]) ).
cnf(t23626,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(step,[status(thm)],[t1154,t24]) ).
cnf(t1214,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(orient,[status(thm)],[t23626]) ).
cnf(t1765,plain,
join(X1,composition(X1,meet(one,X2))) = composition(X1,one),
inference(cp,[status(thm)],[t1214,t1751]) ).
cnf(t23890,plain,
join(X1,composition(X1,meet(one,X2))) = X1,
inference(step,[status(thm)],[t1765,t20]) ).
cnf(t4428,plain,
join(X1,composition(X1,meet(one,X2))) = X1,
inference(orient,[status(thm)],[t23890]) ).
cnf(t24571,plain,
composition(X1,meet(one,composition(converse(X1),top))) = X1,
inference(step,[status(thm)],[t24570,t4428]) ).
cnf(t19236,plain,
composition(X1,meet(one,composition(converse(X1),top))) = X1,
inference(orient,[status(thm)],[t24571]) ).
cnf(t19310,plain,
composition(converse(meet(one,composition(converse(converse(X1)),top))),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t158,t19236]) ).
cnf(t24590,plain,
composition(converse(meet(one,composition(X1,top))),X1) = converse(converse(X1)),
inference(step,[status(thm)],[t19310,t24]) ).
cnf(t24591,plain,
composition(converse(meet(one,composition(X1,top))),X1) = X1,
inference(step,[status(thm)],[t24590,t24]) ).
cnf(t19474,plain,
composition(converse(meet(one,composition(X1,top))),X1) = X1,
inference(orient,[status(thm)],[t24591]) ).
cnf(t19493,plain,
sk1 = composition(converse(meet(one,sk1)),sk1),
inference(cp,[status(thm)],[t19474,t51]) ).
cnf(t24592,plain,
sk1 = composition(converse(meet(sk1,one)),sk1),
inference(step,[status(thm)],[t19493,t128]) ).
cnf(t24593,plain,
sk1 = composition(converse(sFlat0),sk1),
inference(step,[status(thm)],[t24592,t85]) ).
cnf(t24594,plain,
sk1 = composition(sFlat0,sk1),
inference(step,[status(thm)],[t24593,t11021]) ).
cnf(t24595,plain,
sk1 = composition(sFlat0,top),
inference(step,[status(thm)],[t24594,t12460]) ).
cnf(t19574,plain,
composition(sFlat0,top) = sk1,
inference(orient,[status(thm)],[t24595]) ).
cnf(t19587,plain,
composition(converse(top),sFlat0) = converse(sk1),
inference(cp,[status(thm)],[t11402,t19574]) ).
cnf(t24614,plain,
composition(top,sFlat0) = converse(sk1),
inference(step,[status(thm)],[t19587,t591]) ).
cnf(t19628,plain,
composition(top,sFlat0) = converse(sk1),
inference(orient,[status(thm)],[t24614]) ).
cnf(t24615,plain,
composition(converse(sk1),sFlat0) = converse(sk1),
inference(step,[status(thm)],[t12486,t19628]) ).
cnf(t19629,plain,
composition(converse(sk1),sFlat0) = converse(sk1),
inference(orient,[status(thm)],[t24615]) ).
cnf(t23010,plain,
meet(X1,composition(converse(sFlat0),meet(converse(converse(sk1)),composition(sFlat0,X1)))) = join(meet(converse(converse(sk1)),X1),meet(X1,composition(converse(sFlat0),meet(converse(converse(sk1)),composition(sFlat0,X1))))),
inference(cp,[status(thm)],[t22900,t19629]) ).
cnf(t24740,plain,
meet(X1,composition(sFlat0,meet(converse(converse(sk1)),composition(sFlat0,X1)))) = join(meet(converse(converse(sk1)),X1),meet(X1,composition(converse(sFlat0),meet(converse(converse(sk1)),composition(sFlat0,X1))))),
inference(step,[status(thm)],[t23010,t11021]) ).
cnf(t24741,plain,
meet(X1,composition(sFlat0,meet(sk1,composition(sFlat0,X1)))) = join(meet(converse(converse(sk1)),X1),meet(X1,composition(converse(sFlat0),meet(converse(converse(sk1)),composition(sFlat0,X1))))),
inference(step,[status(thm)],[t24740,t24]) ).
cnf(t49,plain,
composition(meet(X1,composition(converse(X2),converse(X3))),meet(X3,composition(converse(X1),converse(X2)))) = join(meet(composition(X1,X3),converse(X2)),composition(meet(X1,converse(composition(X3,X2))),meet(X3,composition(converse(X1),converse(X2))))),
inference(cp,[status(thm)],[t27,t42]) ).
cnf(t24412,plain,
composition(meet(X1,converse(composition(X3,X2))),meet(X3,composition(converse(X1),converse(X2)))) = join(meet(composition(X1,X3),converse(X2)),composition(meet(X1,converse(composition(X3,X2))),meet(X3,composition(converse(X1),converse(X2))))),
inference(step,[status(thm)],[t49,t42]) ).
cnf(t24413,plain,
composition(meet(X1,converse(composition(X3,X2))),meet(X3,converse(composition(X2,X1)))) = join(meet(composition(X1,X3),converse(X2)),composition(meet(X1,converse(composition(X3,X2))),meet(X3,composition(converse(X1),converse(X2))))),
inference(step,[status(thm)],[t24412,t42]) ).
cnf(t24414,plain,
composition(meet(X1,converse(composition(X3,X2))),meet(X3,converse(composition(X2,X1)))) = join(meet(composition(X1,X3),converse(X2)),composition(meet(X1,converse(composition(X3,X2))),meet(X3,converse(composition(X2,X1))))),
inference(step,[status(thm)],[t24413,t42]) ).
cnf(t15651,plain,
join(meet(composition(X1,X2),converse(X3)),composition(meet(X1,converse(composition(X2,X3))),meet(X2,converse(composition(X3,X1))))) = composition(meet(X1,converse(composition(X2,X3))),meet(X2,converse(composition(X3,X1)))),
inference(orient,[status(thm)],[t24414]) ).
cnf(t33,plain,
composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(converse(converse(X1)),X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))),
inference(cp,[status(thm)],[t27,t24]) ).
cnf(t23955,plain,
composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))),
inference(step,[status(thm)],[t33,t24]) ).
cnf(t5849,plain,
join(meet(composition(converse(X1),X2),X3),composition(meet(converse(X1),composition(X3,converse(X2))),meet(X2,composition(X1,X3)))) = composition(meet(converse(X1),composition(X3,converse(X2))),meet(X2,composition(X1,X3))),
inference(orient,[status(thm)],[t23955]) ).
cnf(t53,plain,
composition(join(X1,sk1),top) = join(composition(X1,top),sk1),
inference(cp,[status(thm)],[t37,t51]) ).
cnf(t23526,plain,
composition(join(X1,sk1),top) = join(sk1,composition(X1,top)),
inference(step,[status(thm)],[t53,t88]) ).
cnf(t273,plain,
composition(join(X1,sk1),top) = join(sk1,composition(X1,top)),
inference(orient,[status(thm)],[t23526]) ).
cnf(t1771,plain,
join(sk1,composition(sFlat0,top)) = composition(sk1,top),
inference(cp,[status(thm)],[t273,t1769]) ).
cnf(t23738,plain,
join(sk1,composition(sFlat0,top)) = sk1,
inference(step,[status(thm)],[t1771,t51]) ).
cnf(t1881,plain,
join(sk1,composition(sFlat0,top)) = sk1,
inference(orient,[status(thm)],[t23738]) ).
cnf(t3697,plain,
zero = meet(composition(sFlat0,top),complement(sk1)),
inference(cp,[status(thm)],[t3683,t1881]) ).
cnf(t24040,plain,
zero = meet(complement(sk1),composition(sFlat0,top)),
inference(step,[status(thm)],[t3697,t128]) ).
cnf(t7337,plain,
meet(complement(sk1),composition(sFlat0,top)) = zero,
inference(orient,[status(thm)],[t24040]) ).
cnf(t7341,plain,
composition(meet(converse(sFlat0),composition(top,converse(complement(sk1)))),meet(complement(sk1),composition(sFlat0,top))) = join(meet(composition(converse(sFlat0),complement(sk1)),top),composition(meet(converse(sFlat0),composition(top,converse(complement(sk1)))),zero)),
inference(cp,[status(thm)],[t5849,t7337]) ).
cnf(t24041,plain,
composition(meet(converse(sFlat0),composition(top,converse(complement(sk1)))),zero) = join(meet(composition(converse(sFlat0),complement(sk1)),top),composition(meet(converse(sFlat0),composition(top,converse(complement(sk1)))),zero)),
inference(step,[status(thm)],[t7341,t7337]) ).
cnf(t24042,plain,
zero = join(meet(composition(converse(sFlat0),complement(sk1)),top),composition(meet(converse(sFlat0),composition(top,converse(complement(sk1)))),zero)),
inference(step,[status(thm)],[t24041,t1708]) ).
cnf(t24043,plain,
zero = join(composition(converse(sFlat0),complement(sk1)),composition(meet(converse(sFlat0),composition(top,converse(complement(sk1)))),zero)),
inference(step,[status(thm)],[t24042,t1677]) ).
cnf(t24044,plain,
zero = join(composition(converse(sFlat0),complement(sk1)),zero),
inference(step,[status(thm)],[t24043,t1708]) ).
cnf(t24045,plain,
zero = composition(converse(sFlat0),complement(sk1)),
inference(step,[status(thm)],[t24044,t1701]) ).
cnf(t7342,plain,
composition(converse(sFlat0),complement(sk1)) = zero,
inference(orient,[status(thm)],[t24045]) ).
cnf(t24218,plain,
composition(sFlat0,complement(sk1)) = zero,
inference(step,[status(thm)],[t7342,t11021]) ).
cnf(t11101,plain,
composition(sFlat0,complement(sk1)) = zero,
inference(rw,[status(thm)],[t24218]) ).
cnf(t12036,plain,
composition(sFlat0,complement(sk1)) = zero,
inference(orient,[status(thm)],[t11101]) ).
cnf(t16020,plain,
composition(meet(complement(sk1),converse(composition(X1,sFlat0))),meet(X1,converse(composition(sFlat0,complement(sk1))))) = join(meet(composition(complement(sk1),X1),converse(sFlat0)),composition(meet(complement(sk1),converse(composition(X1,sFlat0))),meet(X1,converse(zero)))),
inference(cp,[status(thm)],[t15651,t12036]) ).
cnf(t11024,plain,
converse(composition(X1,sFlat0)) = composition(sFlat0,converse(X1)),
inference(cp,[status(thm)],[t42,t11021]) ).
cnf(t11318,plain,
converse(composition(X1,sFlat0)) = composition(sFlat0,converse(X1)),
inference(orient,[status(thm)],[t11024]) ).
cnf(t24415,plain,
composition(meet(complement(sk1),composition(sFlat0,converse(X1))),meet(X1,converse(composition(sFlat0,complement(sk1))))) = join(meet(composition(complement(sk1),X1),converse(sFlat0)),composition(meet(complement(sk1),converse(composition(X1,sFlat0))),meet(X1,converse(zero)))),
inference(step,[status(thm)],[t16020,t11318]) ).
cnf(t24416,plain,
composition(meet(complement(sk1),composition(sFlat0,converse(X1))),meet(X1,composition(converse(complement(sk1)),sFlat0))) = join(meet(composition(complement(sk1),X1),converse(sFlat0)),composition(meet(complement(sk1),converse(composition(X1,sFlat0))),meet(X1,converse(zero)))),
inference(step,[status(thm)],[t24415,t11402]) ).
cnf(t7347,plain,
composition(converse(complement(sk1)),sFlat0) = converse(zero),
inference(cp,[status(thm)],[t158,t7342]) ).
cnf(t24091,plain,
composition(converse(complement(sk1)),sFlat0) = zero,
inference(step,[status(thm)],[t7347,t1731]) ).
cnf(t7741,plain,
composition(converse(complement(sk1)),sFlat0) = zero,
inference(orient,[status(thm)],[t24091]) ).
cnf(t24417,plain,
composition(meet(complement(sk1),composition(sFlat0,converse(X1))),meet(X1,zero)) = join(meet(composition(complement(sk1),X1),converse(sFlat0)),composition(meet(complement(sk1),converse(composition(X1,sFlat0))),meet(X1,converse(zero)))),
inference(step,[status(thm)],[t24416,t7741]) ).
cnf(t24418,plain,
composition(meet(complement(sk1),composition(sFlat0,converse(X1))),zero) = join(meet(composition(complement(sk1),X1),converse(sFlat0)),composition(meet(complement(sk1),converse(composition(X1,sFlat0))),meet(X1,converse(zero)))),
inference(step,[status(thm)],[t24417,t1621]) ).
cnf(t24419,plain,
zero = join(meet(composition(complement(sk1),X1),converse(sFlat0)),composition(meet(complement(sk1),converse(composition(X1,sFlat0))),meet(X1,converse(zero)))),
inference(step,[status(thm)],[t24418,t1708]) ).
cnf(t24420,plain,
zero = join(meet(converse(sFlat0),composition(complement(sk1),X1)),composition(meet(complement(sk1),converse(composition(X1,sFlat0))),meet(X1,converse(zero)))),
inference(step,[status(thm)],[t24419,t128]) ).
cnf(t24421,plain,
zero = join(meet(sFlat0,composition(complement(sk1),X1)),composition(meet(complement(sk1),converse(composition(X1,sFlat0))),meet(X1,converse(zero)))),
inference(step,[status(thm)],[t24420,t11021]) ).
cnf(t24422,plain,
zero = join(meet(sFlat0,composition(complement(sk1),X1)),composition(meet(complement(sk1),composition(sFlat0,converse(X1))),meet(X1,converse(zero)))),
inference(step,[status(thm)],[t24421,t11318]) ).
cnf(t24423,plain,
zero = join(meet(sFlat0,composition(complement(sk1),X1)),composition(meet(complement(sk1),composition(sFlat0,converse(X1))),meet(X1,zero))),
inference(step,[status(thm)],[t24422,t1731]) ).
cnf(t24424,plain,
zero = join(meet(sFlat0,composition(complement(sk1),X1)),composition(meet(complement(sk1),composition(sFlat0,converse(X1))),zero)),
inference(step,[status(thm)],[t24423,t1621]) ).
cnf(t24425,plain,
zero = join(meet(sFlat0,composition(complement(sk1),X1)),zero),
inference(step,[status(thm)],[t24424,t1708]) ).
cnf(t24426,plain,
zero = meet(sFlat0,composition(complement(sk1),X1)),
inference(step,[status(thm)],[t24425,t1701]) ).
cnf(t16061,plain,
meet(sFlat0,composition(complement(sk1),X1)) = zero,
inference(orient,[status(thm)],[t24426]) ).
cnf(t16064,plain,
composition(meet(sFlat0,composition(complement(sk1),converse(X1))),meet(X1,composition(converse(sFlat0),complement(sk1)))) = join(meet(composition(sFlat0,X1),complement(sk1)),composition(zero,meet(X1,composition(converse(sFlat0),complement(sk1))))),
inference(cp,[status(thm)],[t27,t16061]) ).
cnf(t24427,plain,
composition(zero,meet(X1,composition(converse(sFlat0),complement(sk1)))) = join(meet(composition(sFlat0,X1),complement(sk1)),composition(zero,meet(X1,composition(converse(sFlat0),complement(sk1))))),
inference(step,[status(thm)],[t16064,t16061]) ).
cnf(t1732,plain,
converse(composition(X1,zero)) = composition(zero,converse(X1)),
inference(cp,[status(thm)],[t42,t1731]) ).
cnf(t23719,plain,
converse(zero) = composition(zero,converse(X1)),
inference(step,[status(thm)],[t1732,t1708]) ).
cnf(t23720,plain,
zero = composition(zero,converse(X1)),
inference(step,[status(thm)],[t23719,t1731]) ).
cnf(t1772,plain,
composition(zero,converse(X1)) = zero,
inference(orient,[status(thm)],[t23720]) ).
cnf(t1779,plain,
zero = composition(zero,X1),
inference(cp,[status(thm)],[t1772,t24]) ).
cnf(t1784,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t1779]) ).
cnf(t24428,plain,
zero = join(meet(composition(sFlat0,X1),complement(sk1)),composition(zero,meet(X1,composition(converse(sFlat0),complement(sk1))))),
inference(step,[status(thm)],[t24427,t1784]) ).
cnf(t24429,plain,
zero = join(meet(complement(sk1),composition(sFlat0,X1)),composition(zero,meet(X1,composition(converse(sFlat0),complement(sk1))))),
inference(step,[status(thm)],[t24428,t128]) ).
cnf(t24430,plain,
zero = join(meet(complement(sk1),composition(sFlat0,X1)),zero),
inference(step,[status(thm)],[t24429,t1784]) ).
cnf(t24431,plain,
zero = meet(complement(sk1),composition(sFlat0,X1)),
inference(step,[status(thm)],[t24430,t1701]) ).
cnf(t16067,plain,
meet(complement(sk1),composition(sFlat0,X1)) = zero,
inference(orient,[status(thm)],[t24431]) ).
cnf(t16080,plain,
composition(sFlat0,X1) = join(meet(composition(sFlat0,X1),sk1),zero),
inference(cp,[status(thm)],[t2274,t16067]) ).
cnf(t24432,plain,
composition(sFlat0,X1) = meet(composition(sFlat0,X1),sk1),
inference(step,[status(thm)],[t16080,t1701]) ).
cnf(t24433,plain,
composition(sFlat0,X1) = meet(sk1,composition(sFlat0,X1)),
inference(step,[status(thm)],[t24432,t128]) ).
cnf(t16083,plain,
meet(sk1,composition(sFlat0,X1)) = composition(sFlat0,X1),
inference(orient,[status(thm)],[t24433]) ).
cnf(t24742,plain,
meet(X1,composition(sFlat0,composition(sFlat0,X1))) = join(meet(converse(converse(sk1)),X1),meet(X1,composition(converse(sFlat0),meet(converse(converse(sk1)),composition(sFlat0,X1))))),
inference(step,[status(thm)],[t24741,t16083]) ).
cnf(t11619,plain,
composition(sFlat0,composition(sFlat0,X1)) = composition(sFlat0,X1),
inference(cp,[status(thm)],[t25,t11614]) ).
cnf(t11699,plain,
composition(sFlat0,composition(sFlat0,X1)) = composition(sFlat0,X1),
inference(orient,[status(thm)],[t11619]) ).
cnf(t24743,plain,
meet(X1,composition(sFlat0,X1)) = join(meet(converse(converse(sk1)),X1),meet(X1,composition(converse(sFlat0),meet(converse(converse(sk1)),composition(sFlat0,X1))))),
inference(step,[status(thm)],[t24742,t11699]) ).
cnf(t113,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t90,t110]) ).
cnf(t518,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t113]) ).
cnf(t526,plain,
join(converse(join(X1,X2)),complement(converse(X2))) = join(converse(X1),top),
inference(cp,[status(thm)],[t518,t97]) ).
cnf(t23580,plain,
join(complement(converse(X2)),converse(join(X1,X2))) = join(converse(X1),top),
inference(step,[status(thm)],[t526,t88]) ).
cnf(t23581,plain,
join(complement(converse(X2)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t23580,t347]) ).
cnf(t890,plain,
join(complement(converse(X1)),converse(join(X2,X1))) = top,
inference(orient,[status(thm)],[t23581]) ).
cnf(t1328,plain,
converse(X1) = join(meet(converse(X1),converse(join(X2,X1))),complement(top)),
inference(cp,[status(thm)],[t1309,t890]) ).
cnf(t24491,plain,
converse(X1) = join(complement(top),meet(converse(X1),converse(join(X2,X1)))),
inference(step,[status(thm)],[t1328,t88]) ).
cnf(t24492,plain,
converse(X1) = join(zero,meet(converse(X1),converse(join(X2,X1)))),
inference(step,[status(thm)],[t24491,t114]) ).
cnf(t24493,plain,
converse(X1) = meet(converse(X1),converse(join(X2,X1))),
inference(step,[status(thm)],[t24492,t1684]) ).
cnf(t16772,plain,
meet(converse(X1),converse(join(X2,X1))) = converse(X1),
inference(orient,[status(thm)],[t24493]) ).
cnf(t16886,plain,
converse(converse(X1)) = meet(converse(converse(X1)),converse(converse(join(X2,X1)))),
inference(cp,[status(thm)],[t16772,t110]) ).
cnf(t24494,plain,
X1 = meet(converse(converse(X1)),converse(converse(join(X2,X1)))),
inference(step,[status(thm)],[t16886,t24]) ).
cnf(t24495,plain,
X1 = meet(X1,converse(converse(join(X2,X1)))),
inference(step,[status(thm)],[t24494,t24]) ).
cnf(t24496,plain,
X1 = meet(X1,join(X2,X1)),
inference(step,[status(thm)],[t24495,t24]) ).
cnf(t16902,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t24496]) ).
cnf(t3911,plain,
join(one,converse(converse(sFlat0))) = converse(one),
inference(cp,[status(thm)],[t214,t3910]) ).
cnf(t23847,plain,
join(one,sFlat0) = converse(one),
inference(step,[status(thm)],[t3911,t24]) ).
cnf(t23848,plain,
join(sFlat0,one) = converse(one),
inference(step,[status(thm)],[t23847,t88]) ).
cnf(t23849,plain,
join(sFlat0,one) = one,
inference(step,[status(thm)],[t23848,t181]) ).
cnf(t4068,plain,
join(sFlat0,one) = one,
inference(orient,[status(thm)],[t23849]) ).
cnf(t4073,plain,
join(X1,composition(sFlat0,X1)) = composition(one,X1),
inference(cp,[status(thm)],[t444,t4068]) ).
cnf(t23897,plain,
join(X1,composition(sFlat0,X1)) = X1,
inference(step,[status(thm)],[t4073,t192]) ).
cnf(t4818,plain,
join(X1,composition(sFlat0,X1)) = X1,
inference(orient,[status(thm)],[t23897]) ).
cnf(t16908,plain,
composition(sFlat0,X1) = meet(composition(sFlat0,X1),X1),
inference(cp,[status(thm)],[t16902,t4818]) ).
cnf(t24497,plain,
composition(sFlat0,X1) = meet(X1,composition(sFlat0,X1)),
inference(step,[status(thm)],[t16908,t128]) ).
cnf(t16973,plain,
meet(X1,composition(sFlat0,X1)) = composition(sFlat0,X1),
inference(orient,[status(thm)],[t24497]) ).
cnf(t24744,plain,
composition(sFlat0,X1) = join(meet(converse(converse(sk1)),X1),meet(X1,composition(converse(sFlat0),meet(converse(converse(sk1)),composition(sFlat0,X1))))),
inference(step,[status(thm)],[t24743,t16973]) ).
cnf(t24745,plain,
composition(sFlat0,X1) = join(meet(sk1,X1),meet(X1,composition(converse(sFlat0),meet(converse(converse(sk1)),composition(sFlat0,X1))))),
inference(step,[status(thm)],[t24744,t24]) ).
cnf(t24746,plain,
composition(sFlat0,X1) = join(meet(sk1,X1),meet(X1,composition(sFlat0,meet(converse(converse(sk1)),composition(sFlat0,X1))))),
inference(step,[status(thm)],[t24745,t11021]) ).
cnf(t24747,plain,
composition(sFlat0,X1) = join(meet(sk1,X1),meet(X1,composition(sFlat0,meet(sk1,composition(sFlat0,X1))))),
inference(step,[status(thm)],[t24746,t24]) ).
cnf(t24748,plain,
composition(sFlat0,X1) = join(meet(sk1,X1),meet(X1,composition(sFlat0,composition(sFlat0,X1)))),
inference(step,[status(thm)],[t24747,t16083]) ).
cnf(t24749,plain,
composition(sFlat0,X1) = join(meet(sk1,X1),meet(X1,composition(sFlat0,X1))),
inference(step,[status(thm)],[t24748,t11699]) ).
cnf(t24750,plain,
composition(sFlat0,X1) = join(meet(sk1,X1),composition(sFlat0,X1)),
inference(step,[status(thm)],[t24749,t16973]) ).
cnf(t23363,plain,
join(meet(sk1,X1),composition(sFlat0,X1)) = composition(sFlat0,X1),
inference(orient,[status(thm)],[t24750]) ).
cnf(t23400,plain,
meet(sk1,X1) = meet(meet(sk1,X1),composition(sFlat0,X1)),
inference(cp,[status(thm)],[t1892,t23363]) ).
cnf(t24751,plain,
meet(sk1,X1) = meet(sk1,meet(X1,composition(sFlat0,X1))),
inference(step,[status(thm)],[t23400,t5417]) ).
cnf(t24752,plain,
meet(sk1,X1) = meet(sk1,composition(sFlat0,X1)),
inference(step,[status(thm)],[t24751,t16973]) ).
cnf(t24753,plain,
meet(sk1,X1) = composition(sFlat0,X1),
inference(step,[status(thm)],[t24752,t16083]) ).
cnf(t23409,plain,
composition(sFlat0,X1) = meet(sk1,X1),
inference(orient,[status(thm)],[t24753]) ).
cnf(goal_0,negated_conjecture,
composition(meet(sk1,one),sk2) != meet(sk1,sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
composition(sFlat0,sk2) != meet(sk1,sk2),
inference(rw,[status(thm)],[goal_0,t85]) ).
cnf(g0_1,plain,
meet(sk1,sk2) != meet(sk1,sk2),
inference(rw,[status(thm)],[g0_0,t23409]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : REL020-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.42 % Computer : n009.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Thu Sep 24 07:17:29 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 83.48/12.42 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 83.48/12.42 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------