%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL029-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:35:28 PM UTC 2026
% Result : Unsatisfiable 234.10s 30.15s
% Output : CNFRefutation 234.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 162
% Number of leaves : 23
% Syntax : Number of clauses : 967 ( 967 unt; 0 nHn; 468 RR)
% Number of literals : 967 ( 966 equ; 28 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 11 con; 0-2 aty)
% Number of variables : 768 ( 65 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t102,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t7,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t68,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t7]) ).
cnf(t103,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t68,t102]) ).
cnf(t90082,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t103,t68]) ).
cnf(t159,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t90082]) ).
cnf(t21,axiom,
sFlat3 = meet(sk1,sk2),
introduced(definition) ).
cnf(t100,plain,
meet(sk1,sk2) = sFlat3,
inference(orient,[status(thm)],[t21]) ).
cnf(t163,plain,
meet(sk1,sk2) = sFlat3,
inference(rw,[status(thm)],[t100]) ).
cnf(t90083,plain,
meet(sk2,sk1) = sFlat3,
inference(step,[status(thm)],[t163,t159]) ).
cnf(t166,plain,
meet(sk2,sk1) = sFlat3,
inference(orient,[status(thm)],[t90083]) ).
cnf(t22,axiom,
sFlat4 = composition(meet(sk1,sk2),sk3),
introduced(definition) ).
cnf(t41,plain,
composition(meet(sk1,sk2),sk3) = sFlat4,
inference(orient,[status(thm)],[t22]) ).
cnf(t90046,plain,
composition(sFlat3,sk3) = sFlat4,
inference(step,[status(thm)],[t41,t100]) ).
cnf(t101,plain,
composition(sFlat3,sk3) = sFlat4,
inference(rw,[status(thm)],[t90046]) ).
cnf(t146,plain,
composition(sFlat3,sk3) = sFlat4,
inference(orient,[status(thm)],[t101]) ).
cnf(t14,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t29,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)],[t28,t28]) ).
cnf(t90093,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(join(complement(X1),X2),complement(join(complement(X1),complement(X2)))))),
inference(step,[status(thm)],[t29,t102]) ).
cnf(t11,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t104,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t90094,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)],[t90093,t104]) ).
cnf(t90095,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t90094,t68]) ).
cnf(t293,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t90095]) ).
cnf(t304,plain,
meet(X1,join(complement(X1),join(X2,meet(X1,X2)))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t68,t293]) ).
cnf(t93377,plain,
meet(X1,join(complement(X1),join(X2,meet(X1,X2)))) = meet(X1,X2),
inference(step,[status(thm)],[t304,t68]) ).
cnf(t71632,plain,
meet(X1,join(complement(X1),join(X2,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t93377]) ).
cnf(t71762,plain,
meet(X1,X2) = meet(X1,join(complement(X1),join(X2,meet(X2,X1)))),
inference(cp,[status(thm)],[t71632,t159]) ).
cnf(t13,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t90052,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t13,t102]) ).
cnf(t118,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t90052]) ).
cnf(t8,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t49,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t51,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t49,t31]) ).
cnf(t209,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t51]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t210,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t209,t27]) ).
cnf(t90090,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t210,t31]) ).
cnf(t222,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t90090]) ).
cnf(t10,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t33,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t32,t27]) ).
cnf(t170,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t33]) ).
cnf(t224,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t222,t170]) ).
cnf(t90092,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t224,t222]) ).
cnf(t243,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t90092]) ).
cnf(t246,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t118,t243]) ).
cnf(t223,plain,
one = converse(one),
inference(cp,[status(thm)],[t222,t27]) ).
cnf(t232,plain,
converse(one) = one,
inference(orient,[status(thm)],[t223]) ).
cnf(t90107,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t246,t232]) ).
cnf(t90108,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t90107,t243]) ).
cnf(t420,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t90108]) ).
cnf(t90043,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t28,t68]) ).
cnf(t71,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t90043]) ).
cnf(t2560,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t71]) ).
cnf(t2578,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t2560,t420]) ).
cnf(t90349,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t2578,t102]) ).
cnf(t5,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t72,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t90350,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t90349,t72]) ).
cnf(t90351,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t90350,t102]) ).
cnf(t2630,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t90351]) ).
cnf(t4,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t111,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t115,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t68,t111]) ).
cnf(t90079,plain,
zero = complement(top),
inference(step,[status(thm)],[t115,t72]) ).
cnf(t140,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t90079]) ).
cnf(t143,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t68,t140]) ).
cnf(t376,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t143]) ).
cnf(t2638,plain,
meet(top,complement(X1)) = complement(X1),
inference(cp,[status(thm)],[t376,t2630]) ).
cnf(t2639,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t2638]) ).
cnf(t2647,plain,
join(complement(top),complement(complement(X1))) = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(cp,[status(thm)],[t293,t2639]) ).
cnf(t90354,plain,
join(zero,complement(complement(X1))) = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t2647,t140]) ).
cnf(t90355,plain,
X1 = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t90354,t2630]) ).
cnf(t90356,plain,
X1 = join(zero,complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t90355,t140]) ).
cnf(t90357,plain,
X1 = join(zero,complement(join(zero,join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t90356,t140]) ).
cnf(t90358,plain,
X1 = join(zero,complement(join(zero,complement(X1)))),
inference(step,[status(thm)],[t90357,t420]) ).
cnf(t90359,plain,
X1 = join(zero,meet(top,X1)),
inference(step,[status(thm)],[t90358,t376]) ).
cnf(t2653,plain,
join(zero,meet(top,X1)) = X1,
inference(orient,[status(thm)],[t90359]) ).
cnf(t2654,plain,
complement(X1) = join(zero,complement(X1)),
inference(cp,[status(thm)],[t2653,t2639]) ).
cnf(t2660,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t2654]) ).
cnf(t90361,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t2630,t2660]) ).
cnf(t2668,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t90361]) ).
cnf(t2682,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t2668]) ).
cnf(t2690,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t420,t2682]) ).
cnf(t90372,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t2690,t2682]) ).
cnf(t90373,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t90372,t2682]) ).
cnf(t2729,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t90373]) ).
cnf(t110,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t104,t102]) ).
cnf(t90099,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t110,t104]) ).
cnf(t330,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t90099]) ).
cnf(t2731,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t2729,t330]) ).
cnf(t90466,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t2731,t104]) ).
cnf(t90467,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t90466,t2729]) ).
cnf(t3213,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t90467]) ).
cnf(t2571,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t2560,t68]) ).
cnf(t90455,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t2571,t102]) ).
cnf(t3165,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t90455]) ).
cnf(t3214,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t3213,t3165]) ).
cnf(t90486,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t3214,t3165]) ).
cnf(t90487,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t90486,t102]) ).
cnf(t3259,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t90487]) ).
cnf(t93393,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t71762,t3259]) ).
cnf(t71819,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t93393]) ).
cnf(t71898,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(complement(X1),X3))),
inference(cp,[status(thm)],[t71819,t330]) ).
cnf(t88838,plain,
meet(X1,join(X2,join(complement(X1),X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t71898]) ).
cnf(t2692,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t68,t2682]) ).
cnf(t2958,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t2692]) ).
cnf(t2976,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t2682,t2958]) ).
cnf(t3193,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t2976]) ).
cnf(t71926,plain,
join(X1,complement(join(complement(complement(X1)),X2))) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t3193,t71819]) ).
cnf(t2693,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t68,t2682]) ).
cnf(t3106,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t2693]) ).
cnf(t93395,plain,
join(X1,meet(complement(X1),complement(X2))) = complement(meet(complement(X1),X2)),
inference(step,[status(thm)],[t71926,t3106]) ).
cnf(t2972,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t2958,t2682]) ).
cnf(t3183,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t2972]) ).
cnf(t93396,plain,
join(X1,complement(join(X1,X2))) = complement(meet(complement(X1),X2)),
inference(step,[status(thm)],[t93395,t3183]) ).
cnf(t93397,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(step,[status(thm)],[t93396,t3193]) ).
cnf(t72240,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t93397]) ).
cnf(t2684,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t2682,t68]) ).
cnf(t2935,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t2684]) ).
cnf(t72419,plain,
join(complement(X1),complement(complement(X2))) = join(complement(X1),complement(complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t72240,t2935]) ).
cnf(t93537,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),complement(complement(meet(X1,X2)))),
inference(step,[status(thm)],[t72419,t2935]) ).
cnf(t2943,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t2935,t2682]) ).
cnf(t3288,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t2943]) ).
cnf(t93538,plain,
join(complement(X1),X2) = join(complement(X1),complement(complement(meet(X1,X2)))),
inference(step,[status(thm)],[t93537,t3288]) ).
cnf(t93539,plain,
join(complement(X1),X2) = complement(meet(X1,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t93538,t2935]) ).
cnf(t93540,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(step,[status(thm)],[t93539,t3288]) ).
cnf(t76943,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t93540]) ).
cnf(t88844,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,join(complement(X1),X3))),
inference(cp,[status(thm)],[t88838,t76943]) ).
cnf(t94075,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t88844,t88838]) ).
cnf(t89119,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t94075]) ).
cnf(t114,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t104,t111]) ).
cnf(t451,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t114]) ).
cnf(t459,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t451,t102]) ).
cnf(t519,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t459]) ).
cnf(t2947,plain,
join(top,complement(X1)) = join(X2,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t519,t2935]) ).
cnf(t457,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t451,t420]) ).
cnf(t90112,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t457,t111]) ).
cnf(t474,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t90112]) ).
cnf(t90531,plain,
top = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t2947,t474]) ).
cnf(t4218,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t90531]) ).
cnf(t4226,plain,
meet(X1,complement(complement(meet(X2,complement(X1))))) = complement(top),
inference(cp,[status(thm)],[t3106,t4218]) ).
cnf(t90586,plain,
meet(X1,meet(X2,complement(X1))) = complement(top),
inference(step,[status(thm)],[t4226,t2682]) ).
cnf(t90587,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t90586,t140]) ).
cnf(t5639,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t90587]) ).
cnf(t5640,plain,
zero = meet(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t5639,t3183]) ).
cnf(t12358,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t5640]) ).
cnf(t12,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t44,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t46,plain,
composition(join(composition(X1,X2),X3),Y3) = join(composition(X1,composition(X2,Y3)),composition(X3,Y3)),
inference(cp,[status(thm)],[t44,t32]) ).
cnf(t6761,plain,
join(composition(X1,composition(X2,X3)),composition(Y3,X3)) = composition(join(composition(X1,X2),Y3),X3),
inference(orient,[status(thm)],[t46]) ).
cnf(t6815,plain,
composition(join(composition(X1,sFlat3),X2),sk3) = join(composition(X1,sFlat4),composition(X2,sk3)),
inference(cp,[status(thm)],[t6761,t146]) ).
cnf(t6875,plain,
composition(join(composition(X1,sFlat3),X2),sk3) = join(composition(X1,sFlat4),composition(X2,sk3)),
inference(orient,[status(thm)],[t6815]) ).
cnf(t6915,plain,
join(composition(X1,sFlat4),composition(X2,sk3)) = composition(join(X2,composition(X1,sFlat3)),sk3),
inference(cp,[status(thm)],[t6875,t102]) ).
cnf(t7216,plain,
composition(join(X1,composition(X2,sFlat3)),sk3) = join(composition(X2,sFlat4),composition(X1,sk3)),
inference(orient,[status(thm)],[t6915]) ).
cnf(t9,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t130,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t131,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t130,t31]) ).
cnf(t249,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t131]) ).
cnf(t244,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t44,t243]) ).
cnf(t533,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t244]) ).
cnf(t557,plain,
join(X1,converse(composition(X2,converse(X1)))) = converse(composition(join(one,X2),converse(X1))),
inference(cp,[status(thm)],[t249,t533]) ).
cnf(t50,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t49,t31]) ).
cnf(t199,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t50]) ).
cnf(t90324,plain,
join(X1,composition(X1,converse(X2))) = converse(composition(join(one,X2),converse(X1))),
inference(step,[status(thm)],[t557,t199]) ).
cnf(t90325,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,converse(join(one,X2))),
inference(step,[status(thm)],[t90324,t199]) ).
cnf(t252,plain,
join(one,converse(X1)) = converse(join(one,X1)),
inference(cp,[status(thm)],[t249,t232]) ).
cnf(t265,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t252]) ).
cnf(t90326,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(step,[status(thm)],[t90325,t265]) ).
cnf(t2068,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(orient,[status(thm)],[t90326]) ).
cnf(t2089,plain,
composition(X1,join(one,converse(converse(X2)))) = join(X1,composition(X1,X2)),
inference(cp,[status(thm)],[t2068,t31]) ).
cnf(t90331,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(step,[status(thm)],[t2089,t31]) ).
cnf(t2179,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(orient,[status(thm)],[t90331]) ).
cnf(t7221,plain,
join(composition(X1,sFlat4),composition(X1,sk3)) = composition(composition(X1,join(one,sFlat3)),sk3),
inference(cp,[status(thm)],[t7216,t2179]) ).
cnf(t90737,plain,
join(composition(X1,sFlat4),composition(X1,sk3)) = composition(X1,composition(join(one,sFlat3),sk3)),
inference(step,[status(thm)],[t7221,t32]) ).
cnf(t148,plain,
composition(join(X1,sFlat3),sk3) = join(composition(X1,sk3),sFlat4),
inference(cp,[status(thm)],[t44,t146]) ).
cnf(t90106,plain,
composition(join(X1,sFlat3),sk3) = join(sFlat4,composition(X1,sk3)),
inference(step,[status(thm)],[t148,t102]) ).
cnf(t406,plain,
composition(join(X1,sFlat3),sk3) = join(sFlat4,composition(X1,sk3)),
inference(orient,[status(thm)],[t90106]) ).
cnf(t90738,plain,
join(composition(X1,sFlat4),composition(X1,sk3)) = composition(X1,join(sFlat4,composition(one,sk3))),
inference(step,[status(thm)],[t90737,t406]) ).
cnf(t90739,plain,
join(composition(X1,sFlat4),composition(X1,sk3)) = composition(X1,join(sFlat4,sk3)),
inference(step,[status(thm)],[t90738,t243]) ).
cnf(t147,plain,
composition(join(sFlat3,X1),sk3) = join(sFlat4,composition(X1,sk3)),
inference(cp,[status(thm)],[t44,t146]) ).
cnf(t396,plain,
composition(join(sFlat3,X1),sk3) = join(sFlat4,composition(X1,sk3)),
inference(orient,[status(thm)],[t147]) ).
cnf(t132,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t130,t31]) ).
cnf(t276,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t132]) ).
cnf(t280,plain,
join(converse(X1),one) = converse(join(X1,one)),
inference(cp,[status(thm)],[t276,t232]) ).
cnf(t90096,plain,
join(one,converse(X1)) = converse(join(X1,one)),
inference(step,[status(thm)],[t280,t102]) ).
cnf(t305,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t90096]) ).
cnf(t308,plain,
join(one,converse(join(X1,X2))) = converse(join(X1,join(X2,one))),
inference(cp,[status(thm)],[t305,t104]) ).
cnf(t1038,plain,
converse(join(X1,join(X2,one))) = join(one,converse(join(X1,X2))),
inference(orient,[status(thm)],[t308]) ).
cnf(t3,axiom,
join(sk2,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t136,plain,
join(sk2,one) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t1042,plain,
join(one,converse(join(X1,sk2))) = converse(join(X1,one)),
inference(cp,[status(thm)],[t1038,t136]) ).
cnf(t90252,plain,
join(one,converse(join(X1,sk2))) = join(one,converse(X1)),
inference(step,[status(thm)],[t1042,t305]) ).
cnf(t1424,plain,
join(one,converse(join(X1,sk2))) = join(one,converse(X1)),
inference(orient,[status(thm)],[t90252]) ).
cnf(t2569,plain,
sk2 = join(sFlat3,complement(join(complement(sk2),sk1))),
inference(cp,[status(thm)],[t2560,t166]) ).
cnf(t90447,plain,
sk2 = join(sFlat3,meet(sk2,complement(sk1))),
inference(step,[status(thm)],[t2569,t3106]) ).
cnf(t3155,plain,
join(sFlat3,meet(sk2,complement(sk1))) = sk2,
inference(orient,[status(thm)],[t90447]) ).
cnf(t3215,plain,
join(sFlat3,meet(sk2,complement(sk1))) = join(sFlat3,sk2),
inference(cp,[status(thm)],[t3213,t3155]) ).
cnf(t90468,plain,
sk2 = join(sFlat3,sk2),
inference(step,[status(thm)],[t3215,t3155]) ).
cnf(t3221,plain,
join(sFlat3,sk2) = sk2,
inference(orient,[status(thm)],[t90468]) ).
cnf(t3224,plain,
join(one,converse(sFlat3)) = join(one,converse(sk2)),
inference(cp,[status(thm)],[t1424,t3221]) ).
cnf(t306,plain,
join(one,converse(sk2)) = converse(one),
inference(cp,[status(thm)],[t305,t136]) ).
cnf(t90097,plain,
join(one,converse(sk2)) = one,
inference(step,[status(thm)],[t306,t232]) ).
cnf(t320,plain,
join(one,converse(sk2)) = one,
inference(orient,[status(thm)],[t90097]) ).
cnf(t90476,plain,
join(one,converse(sFlat3)) = one,
inference(step,[status(thm)],[t3224,t320]) ).
cnf(t3241,plain,
join(one,converse(sFlat3)) = one,
inference(orient,[status(thm)],[t90476]) ).
cnf(t3242,plain,
join(one,converse(converse(sFlat3))) = converse(one),
inference(cp,[status(thm)],[t265,t3241]) ).
cnf(t90477,plain,
join(one,sFlat3) = converse(one),
inference(step,[status(thm)],[t3242,t31]) ).
cnf(t90478,plain,
join(sFlat3,one) = converse(one),
inference(step,[status(thm)],[t90477,t102]) ).
cnf(t90479,plain,
join(sFlat3,one) = one,
inference(step,[status(thm)],[t90478,t232]) ).
cnf(t3248,plain,
join(sFlat3,one) = one,
inference(orient,[status(thm)],[t90479]) ).
cnf(t3249,plain,
join(sFlat4,composition(one,sk3)) = composition(one,sk3),
inference(cp,[status(thm)],[t396,t3248]) ).
cnf(t90484,plain,
join(sFlat4,sk3) = composition(one,sk3),
inference(step,[status(thm)],[t3249,t243]) ).
cnf(t90485,plain,
join(sFlat4,sk3) = sk3,
inference(step,[status(thm)],[t90484,t243]) ).
cnf(t3257,plain,
join(sFlat4,sk3) = sk3,
inference(orient,[status(thm)],[t90485]) ).
cnf(t90740,plain,
join(composition(X1,sFlat4),composition(X1,sk3)) = composition(X1,sk3),
inference(step,[status(thm)],[t90739,t3257]) ).
cnf(t7255,plain,
join(composition(X1,sFlat4),composition(X1,sk3)) = composition(X1,sk3),
inference(orient,[status(thm)],[t90740]) ).
cnf(t18,axiom,
sFlat0 = composition(sk1,sk3),
introduced(definition) ).
cnf(t58,plain,
composition(sk1,sk3) = sFlat0,
inference(orient,[status(thm)],[t18]) ).
cnf(t7284,plain,
composition(sk1,sk3) = join(composition(sk1,sFlat4),sFlat0),
inference(cp,[status(thm)],[t7255,t58]) ).
cnf(t90745,plain,
sFlat0 = join(composition(sk1,sFlat4),sFlat0),
inference(step,[status(thm)],[t7284,t58]) ).
cnf(t90746,plain,
sFlat0 = join(sFlat0,composition(sk1,sFlat4)),
inference(step,[status(thm)],[t90745,t102]) ).
cnf(t7295,plain,
join(sFlat0,composition(sk1,sFlat4)) = sFlat0,
inference(orient,[status(thm)],[t90746]) ).
cnf(t17,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(t34,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)],[t17]) ).
cnf(t39,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)],[t34,t27]) ).
cnf(t90498,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)],[t39,t243]) ).
cnf(t90499,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)],[t90498,t27]) ).
cnf(t90500,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)],[t90499,t159]) ).
cnf(t90501,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)],[t90500,t243]) ).
cnf(t3626,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)],[t90501]) ).
cnf(t3173,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t3165,t159]) ).
cnf(t3308,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t3173]) ).
cnf(t106,plain,
join(composition(X1,X2),join(composition(X3,X2),Y3)) = join(composition(join(X1,X3),X2),Y3),
inference(cp,[status(thm)],[t104,t44]) ).
cnf(t12847,plain,
join(composition(X1,X2),join(composition(X3,X2),Y3)) = join(composition(join(X1,X3),X2),Y3),
inference(orient,[status(thm)],[t106]) ).
cnf(t12944,plain,
join(composition(join(X1,X2),X3),complement(composition(X2,X3))) = join(composition(X1,X3),top),
inference(cp,[status(thm)],[t12847,t111]) ).
cnf(t91446,plain,
join(complement(composition(X2,X3)),composition(join(X1,X2),X3)) = join(composition(X1,X3),top),
inference(step,[status(thm)],[t12944,t102]) ).
cnf(t458,plain,
join(top,complement(complement(X1))) = join(X1,top),
inference(cp,[status(thm)],[t451,t111]) ).
cnf(t90113,plain,
top = join(X1,top),
inference(step,[status(thm)],[t458,t474]) ).
cnf(t480,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t90113]) ).
cnf(t91447,plain,
join(complement(composition(X2,X3)),composition(join(X1,X2),X3)) = top,
inference(step,[status(thm)],[t91446,t480]) ).
cnf(t19598,plain,
join(complement(composition(X1,X2)),composition(join(X3,X1),X2)) = top,
inference(orient,[status(thm)],[t91447]) ).
cnf(t256,plain,
converse(join(X1,join(converse(X2),X3))) = join(converse(X1),join(X2,converse(X3))),
inference(cp,[status(thm)],[t130,t249]) ).
cnf(t105,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t104,t102]) ).
cnf(t324,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t105]) ).
cnf(t326,plain,
join(X1,converse(join(X2,X3))) = converse(join(X3,join(converse(X1),X2))),
inference(cp,[status(thm)],[t249,t324]) ).
cnf(t1800,plain,
converse(join(X1,join(converse(X2),X3))) = join(X2,converse(join(X3,X1))),
inference(orient,[status(thm)],[t326]) ).
cnf(t90502,plain,
join(X2,converse(join(X3,X1))) = join(converse(X1),join(X2,converse(X3))),
inference(step,[status(thm)],[t256,t1800]) ).
cnf(t3704,plain,
join(converse(X1),join(X2,converse(X3))) = join(X2,converse(join(X3,X1))),
inference(orient,[status(thm)],[t90502]) ).
cnf(t3721,plain,
join(one,converse(join(sFlat3,X1))) = join(converse(X1),one),
inference(cp,[status(thm)],[t3704,t3241]) ).
cnf(t90973,plain,
join(one,converse(join(sFlat3,X1))) = join(one,converse(X1)),
inference(step,[status(thm)],[t3721,t102]) ).
cnf(t11221,plain,
join(one,converse(join(sFlat3,X1))) = join(one,converse(X1)),
inference(orient,[status(thm)],[t90973]) ).
cnf(t11252,plain,
join(one,converse(meet(sFlat3,X1))) = join(one,converse(sFlat3)),
inference(cp,[status(thm)],[t11221,t3259]) ).
cnf(t90993,plain,
join(one,converse(meet(sFlat3,X1))) = one,
inference(step,[status(thm)],[t11252,t3241]) ).
cnf(t11843,plain,
join(one,converse(meet(sFlat3,X1))) = one,
inference(orient,[status(thm)],[t90993]) ).
cnf(t11846,plain,
join(one,converse(converse(meet(sFlat3,X1)))) = converse(one),
inference(cp,[status(thm)],[t265,t11843]) ).
cnf(t90994,plain,
join(one,meet(sFlat3,X1)) = converse(one),
inference(step,[status(thm)],[t11846,t31]) ).
cnf(t90995,plain,
join(one,meet(sFlat3,X1)) = one,
inference(step,[status(thm)],[t90994,t232]) ).
cnf(t11862,plain,
join(one,meet(sFlat3,X1)) = one,
inference(orient,[status(thm)],[t90995]) ).
cnf(t19905,plain,
top = join(complement(composition(meet(sFlat3,X1),X2)),composition(one,X2)),
inference(cp,[status(thm)],[t19598,t11862]) ).
cnf(t91451,plain,
top = join(composition(one,X2),complement(composition(meet(sFlat3,X1),X2))),
inference(step,[status(thm)],[t19905,t102]) ).
cnf(t91452,plain,
top = join(X2,complement(composition(meet(sFlat3,X1),X2))),
inference(step,[status(thm)],[t91451,t243]) ).
cnf(t20062,plain,
join(X1,complement(composition(meet(sFlat3,X2),X1))) = top,
inference(orient,[status(thm)],[t91452]) ).
cnf(t20066,plain,
top = join(one,complement(meet(sFlat3,X1))),
inference(cp,[status(thm)],[t20062,t27]) ).
cnf(t20194,plain,
join(one,complement(meet(sFlat3,X1))) = top,
inference(orient,[status(thm)],[t20066]) ).
cnf(t20204,plain,
meet(complement(one),meet(sFlat3,X1)) = complement(top),
inference(cp,[status(thm)],[t2958,t20194]) ).
cnf(t91456,plain,
meet(complement(one),meet(sFlat3,X1)) = zero,
inference(step,[status(thm)],[t20204,t140]) ).
cnf(t20289,plain,
meet(complement(one),meet(sFlat3,X1)) = zero,
inference(orient,[status(thm)],[t91456]) ).
cnf(t20298,plain,
meet(sFlat3,X1) = join(meet(meet(sFlat3,X1),one),zero),
inference(cp,[status(thm)],[t3308,t20289]) ).
cnf(t2663,plain,
complement(join(complement(X1),complement(X2))) = join(zero,meet(X1,X2)),
inference(cp,[status(thm)],[t2660,t68]) ).
cnf(t90382,plain,
meet(X1,X2) = join(zero,meet(X1,X2)),
inference(step,[status(thm)],[t2663,t68]) ).
cnf(t2776,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t90382]) ).
cnf(t90362,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t376,t2660]) ).
cnf(t2669,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t90362]) ).
cnf(t90367,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t2669,t2682]) ).
cnf(t2710,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t90367]) ).
cnf(t2778,plain,
meet(top,X1) = join(zero,X1),
inference(cp,[status(thm)],[t2776,t2710]) ).
cnf(t90384,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t2778,t2710]) ).
cnf(t2783,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t90384]) ).
cnf(t2796,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t2783,t102]) ).
cnf(t2824,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t2796]) ).
cnf(t91457,plain,
meet(sFlat3,X1) = meet(meet(sFlat3,X1),one),
inference(step,[status(thm)],[t20298,t2824]) ).
cnf(t91458,plain,
meet(sFlat3,X1) = meet(one,meet(sFlat3,X1)),
inference(step,[status(thm)],[t91457,t159]) ).
cnf(t20299,plain,
meet(one,meet(sFlat3,X1)) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t91458]) ).
cnf(t133,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t104,t130]) ).
cnf(t821,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t133]) ).
cnf(t835,plain,
join(converse(join(X1,X2)),complement(converse(X2))) = join(converse(X1),top),
inference(cp,[status(thm)],[t821,t111]) ).
cnf(t90242,plain,
join(complement(converse(X2)),converse(join(X1,X2))) = join(converse(X1),top),
inference(step,[status(thm)],[t835,t102]) ).
cnf(t90243,plain,
join(complement(converse(X2)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t90242,t480]) ).
cnf(t1311,plain,
join(complement(converse(X1)),converse(join(X2,X1))) = top,
inference(orient,[status(thm)],[t90243]) ).
cnf(t245,plain,
composition(join(X1,one),X2) = join(composition(X1,X2),X2),
inference(cp,[status(thm)],[t44,t243]) ).
cnf(t90125,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(step,[status(thm)],[t245,t102]) ).
cnf(t558,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t90125]) ).
cnf(t560,plain,
join(X1,composition(sk2,X1)) = composition(one,X1),
inference(cp,[status(thm)],[t558,t136]) ).
cnf(t90126,plain,
join(X1,composition(sk2,X1)) = X1,
inference(step,[status(thm)],[t560,t243]) ).
cnf(t574,plain,
join(X1,composition(sk2,X1)) = X1,
inference(orient,[status(thm)],[t90126]) ).
cnf(t1332,plain,
top = join(complement(converse(composition(sk2,X1))),converse(X1)),
inference(cp,[status(thm)],[t1311,t574]) ).
cnf(t90671,plain,
top = join(converse(X1),complement(converse(composition(sk2,X1)))),
inference(step,[status(thm)],[t1332,t102]) ).
cnf(t6389,plain,
join(converse(X1),complement(converse(composition(sk2,X1)))) = top,
inference(orient,[status(thm)],[t90671]) ).
cnf(t6410,plain,
top = join(X1,complement(converse(composition(sk2,converse(X1))))),
inference(cp,[status(thm)],[t6389,t31]) ).
cnf(t90673,plain,
top = join(X1,complement(composition(X1,converse(sk2)))),
inference(step,[status(thm)],[t6410,t199]) ).
cnf(t6442,plain,
join(X1,complement(composition(X1,converse(sk2)))) = top,
inference(orient,[status(thm)],[t90673]) ).
cnf(t580,plain,
join(X1,converse(composition(sk2,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t249,t574]) ).
cnf(t90176,plain,
join(X1,composition(X1,converse(sk2))) = converse(converse(X1)),
inference(step,[status(thm)],[t580,t199]) ).
cnf(t90177,plain,
join(X1,composition(X1,converse(sk2))) = X1,
inference(step,[status(thm)],[t90176,t31]) ).
cnf(t782,plain,
join(X1,composition(X1,converse(sk2))) = X1,
inference(orient,[status(thm)],[t90177]) ).
cnf(t1324,plain,
top = join(complement(converse(composition(X1,converse(sk2)))),converse(X1)),
inference(cp,[status(thm)],[t1311,t782]) ).
cnf(t91078,plain,
top = join(converse(X1),complement(converse(composition(X1,converse(sk2))))),
inference(step,[status(thm)],[t1324,t102]) ).
cnf(t91079,plain,
top = join(converse(X1),complement(composition(sk2,converse(X1)))),
inference(step,[status(thm)],[t91078,t199]) ).
cnf(t14931,plain,
join(converse(X1),complement(composition(sk2,converse(X1)))) = top,
inference(orient,[status(thm)],[t91079]) ).
cnf(t14952,plain,
top = join(X1,complement(composition(sk2,converse(converse(X1))))),
inference(cp,[status(thm)],[t14931,t31]) ).
cnf(t91080,plain,
top = join(X1,complement(composition(sk2,X1))),
inference(step,[status(thm)],[t14952,t31]) ).
cnf(t14992,plain,
join(X1,complement(composition(sk2,X1))) = top,
inference(orient,[status(thm)],[t91080]) ).
cnf(t15028,plain,
meet(complement(X1),composition(sk2,X1)) = complement(top),
inference(cp,[status(thm)],[t2958,t14992]) ).
cnf(t91081,plain,
meet(complement(X1),composition(sk2,X1)) = zero,
inference(step,[status(thm)],[t15028,t140]) ).
cnf(t15042,plain,
meet(complement(X1),composition(sk2,X1)) = zero,
inference(orient,[status(thm)],[t91081]) ).
cnf(t15056,plain,
composition(sk2,X1) = join(meet(composition(sk2,X1),X1),zero),
inference(cp,[status(thm)],[t3308,t15042]) ).
cnf(t91082,plain,
composition(sk2,X1) = meet(composition(sk2,X1),X1),
inference(step,[status(thm)],[t15056,t2824]) ).
cnf(t91083,plain,
composition(sk2,X1) = meet(X1,composition(sk2,X1)),
inference(step,[status(thm)],[t91082,t159]) ).
cnf(t15061,plain,
meet(X1,composition(sk2,X1)) = composition(sk2,X1),
inference(orient,[status(thm)],[t91083]) ).
cnf(t15078,plain,
composition(meet(sk2,converse(one)),meet(one,converse(sk2))) = join(composition(sk2,one),composition(meet(sk2,converse(one)),meet(one,converse(sk2)))),
inference(cp,[status(thm)],[t3626,t15061]) ).
cnf(t91084,plain,
composition(meet(sk2,one),meet(one,converse(sk2))) = join(composition(sk2,one),composition(meet(sk2,converse(one)),meet(one,converse(sk2)))),
inference(step,[status(thm)],[t15078,t232]) ).
cnf(t137,plain,
join(sk2,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t104,t136]) ).
cnf(t189,plain,
join(sk2,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t137]) ).
cnf(t191,plain,
join(one,X1) = join(sk2,join(X1,one)),
inference(cp,[status(thm)],[t189,t102]) ).
cnf(t418,plain,
join(sk2,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t191]) ).
cnf(t452,plain,
join(top,one) = join(one,complement(sk2)),
inference(cp,[status(thm)],[t451,t418]) ).
cnf(t478,plain,
join(one,complement(sk2)) = join(top,one),
inference(orient,[status(thm)],[t452]) ).
cnf(t2,axiom,
join(sk1,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t134,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t135,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t104,t134]) ).
cnf(t184,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t135]) ).
cnf(t186,plain,
join(one,X1) = join(sk1,join(X1,one)),
inference(cp,[status(thm)],[t184,t102]) ).
cnf(t416,plain,
join(sk1,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t186]) ).
cnf(t453,plain,
join(top,one) = join(one,complement(sk1)),
inference(cp,[status(thm)],[t451,t416]) ).
cnf(t490,plain,
join(one,complement(sk1)) = join(top,one),
inference(orient,[status(thm)],[t453]) ).
cnf(t492,plain,
join(one,complement(sk1)) = join(sk2,join(top,one)),
inference(cp,[status(thm)],[t189,t490]) ).
cnf(t90116,plain,
join(top,one) = join(sk2,join(top,one)),
inference(step,[status(thm)],[t492,t490]) ).
cnf(t90117,plain,
join(top,one) = join(one,top),
inference(step,[status(thm)],[t90116,t418]) ).
cnf(t90118,plain,
join(top,one) = top,
inference(step,[status(thm)],[t90117,t480]) ).
cnf(t494,plain,
join(top,one) = top,
inference(orient,[status(thm)],[t90118]) ).
cnf(t90119,plain,
join(one,complement(sk2)) = top,
inference(step,[status(thm)],[t478,t494]) ).
cnf(t495,plain,
join(one,complement(sk2)) = top,
inference(orient,[status(thm)],[t90119]) ).
cnf(t2965,plain,
meet(complement(one),sk2) = complement(top),
inference(cp,[status(thm)],[t2958,t495]) ).
cnf(t90430,plain,
meet(sk2,complement(one)) = complement(top),
inference(step,[status(thm)],[t2965,t159]) ).
cnf(t90431,plain,
meet(sk2,complement(one)) = zero,
inference(step,[status(thm)],[t90430,t140]) ).
cnf(t3094,plain,
meet(sk2,complement(one)) = zero,
inference(orient,[status(thm)],[t90431]) ).
cnf(t3095,plain,
sk2 = join(zero,complement(join(complement(sk2),complement(one)))),
inference(cp,[status(thm)],[t2560,t3094]) ).
cnf(t90432,plain,
sk2 = complement(join(complement(sk2),complement(one))),
inference(step,[status(thm)],[t3095,t2660]) ).
cnf(t90433,plain,
sk2 = meet(sk2,one),
inference(step,[status(thm)],[t90432,t68]) ).
cnf(t3096,plain,
meet(sk2,one) = sk2,
inference(orient,[status(thm)],[t90433]) ).
cnf(t91085,plain,
composition(sk2,meet(one,converse(sk2))) = join(composition(sk2,one),composition(meet(sk2,converse(one)),meet(one,converse(sk2)))),
inference(step,[status(thm)],[t91084,t3096]) ).
cnf(t321,plain,
join(one,join(converse(sk2),X1)) = join(one,X1),
inference(cp,[status(thm)],[t104,t320]) ).
cnf(t960,plain,
join(one,join(converse(sk2),X1)) = join(one,X1),
inference(orient,[status(thm)],[t321]) ).
cnf(t973,plain,
join(one,complement(converse(sk2))) = join(one,top),
inference(cp,[status(thm)],[t960,t111]) ).
cnf(t90201,plain,
join(one,complement(converse(sk2))) = top,
inference(step,[status(thm)],[t973,t480]) ).
cnf(t980,plain,
join(one,complement(converse(sk2))) = top,
inference(orient,[status(thm)],[t90201]) ).
cnf(t2963,plain,
meet(complement(one),converse(sk2)) = complement(top),
inference(cp,[status(thm)],[t2958,t980]) ).
cnf(t90451,plain,
meet(converse(sk2),complement(one)) = complement(top),
inference(step,[status(thm)],[t2963,t159]) ).
cnf(t90452,plain,
meet(converse(sk2),complement(one)) = zero,
inference(step,[status(thm)],[t90451,t140]) ).
cnf(t3163,plain,
meet(converse(sk2),complement(one)) = zero,
inference(orient,[status(thm)],[t90452]) ).
cnf(t3166,plain,
converse(sk2) = join(zero,meet(converse(sk2),complement(complement(one)))),
inference(cp,[status(thm)],[t3165,t3163]) ).
cnf(t90459,plain,
converse(sk2) = meet(converse(sk2),complement(complement(one))),
inference(step,[status(thm)],[t3166,t2776]) ).
cnf(t90460,plain,
converse(sk2) = meet(converse(sk2),one),
inference(step,[status(thm)],[t90459,t2682]) ).
cnf(t90461,plain,
converse(sk2) = meet(one,converse(sk2)),
inference(step,[status(thm)],[t90460,t159]) ).
cnf(t3179,plain,
meet(one,converse(sk2)) = converse(sk2),
inference(orient,[status(thm)],[t90461]) ).
cnf(t91086,plain,
composition(sk2,converse(sk2)) = join(composition(sk2,one),composition(meet(sk2,converse(one)),meet(one,converse(sk2)))),
inference(step,[status(thm)],[t91085,t3179]) ).
cnf(t91087,plain,
composition(sk2,converse(sk2)) = join(sk2,composition(meet(sk2,converse(one)),meet(one,converse(sk2)))),
inference(step,[status(thm)],[t91086,t27]) ).
cnf(t91088,plain,
composition(sk2,converse(sk2)) = join(sk2,composition(meet(sk2,one),meet(one,converse(sk2)))),
inference(step,[status(thm)],[t91087,t232]) ).
cnf(t91089,plain,
composition(sk2,converse(sk2)) = join(sk2,composition(sk2,meet(one,converse(sk2)))),
inference(step,[status(thm)],[t91088,t3096]) ).
cnf(t91090,plain,
composition(sk2,converse(sk2)) = join(sk2,composition(sk2,converse(sk2))),
inference(step,[status(thm)],[t91089,t3179]) ).
cnf(t91091,plain,
composition(sk2,converse(sk2)) = sk2,
inference(step,[status(thm)],[t91090,t782]) ).
cnf(t15091,plain,
composition(sk2,converse(sk2)) = sk2,
inference(orient,[status(thm)],[t91091]) ).
cnf(t15116,plain,
composition(sk2,converse(sk2)) = converse(sk2),
inference(cp,[status(thm)],[t199,t15091]) ).
cnf(t91093,plain,
sk2 = converse(sk2),
inference(step,[status(thm)],[t15116,t15091]) ).
cnf(t15145,plain,
converse(sk2) = sk2,
inference(orient,[status(thm)],[t91093]) ).
cnf(t91118,plain,
join(X1,complement(composition(X1,sk2))) = top,
inference(step,[status(thm)],[t6442,t15145]) ).
cnf(t15234,plain,
join(X1,complement(composition(X1,sk2))) = top,
inference(rw,[status(thm)],[t91118]) ).
cnf(t15653,plain,
join(X1,complement(composition(X1,sk2))) = top,
inference(orient,[status(thm)],[t15234]) ).
cnf(t15689,plain,
meet(X1,complement(complement(composition(complement(X1),sk2)))) = complement(top),
inference(cp,[status(thm)],[t3106,t15653]) ).
cnf(t91138,plain,
meet(X1,composition(complement(X1),sk2)) = complement(top),
inference(step,[status(thm)],[t15689,t2682]) ).
cnf(t91139,plain,
meet(X1,composition(complement(X1),sk2)) = zero,
inference(step,[status(thm)],[t91138,t140]) ).
cnf(t15768,plain,
meet(X1,composition(complement(X1),sk2)) = zero,
inference(orient,[status(thm)],[t91139]) ).
cnf(t15775,plain,
composition(complement(complement(X1)),sk2) = join(meet(composition(complement(complement(X1)),sk2),X1),zero),
inference(cp,[status(thm)],[t3308,t15768]) ).
cnf(t91140,plain,
composition(X1,sk2) = join(meet(composition(complement(complement(X1)),sk2),X1),zero),
inference(step,[status(thm)],[t15775,t2682]) ).
cnf(t91141,plain,
composition(X1,sk2) = meet(composition(complement(complement(X1)),sk2),X1),
inference(step,[status(thm)],[t91140,t2824]) ).
cnf(t91142,plain,
composition(X1,sk2) = meet(X1,composition(complement(complement(X1)),sk2)),
inference(step,[status(thm)],[t91141,t159]) ).
cnf(t91143,plain,
composition(X1,sk2) = meet(X1,composition(X1,sk2)),
inference(step,[status(thm)],[t91142,t2682]) ).
cnf(t15785,plain,
meet(X1,composition(X1,sk2)) = composition(X1,sk2),
inference(orient,[status(thm)],[t91143]) ).
cnf(t20305,plain,
meet(sFlat3,composition(sFlat3,sk2)) = meet(one,composition(sFlat3,sk2)),
inference(cp,[status(thm)],[t20299,t15785]) ).
cnf(t91484,plain,
composition(sFlat3,sk2) = meet(one,composition(sFlat3,sk2)),
inference(step,[status(thm)],[t20305,t15785]) ).
cnf(t20508,plain,
meet(one,composition(sFlat3,sk2)) = composition(sFlat3,sk2),
inference(orient,[status(thm)],[t91484]) ).
cnf(t20515,plain,
composition(meet(sFlat3,converse(sk2)),meet(sk2,converse(sFlat3))) = join(composition(sFlat3,sk2),composition(meet(sFlat3,converse(sk2)),meet(sk2,converse(sFlat3)))),
inference(cp,[status(thm)],[t3626,t20508]) ).
cnf(t91485,plain,
composition(meet(sFlat3,sk2),meet(sk2,converse(sFlat3))) = join(composition(sFlat3,sk2),composition(meet(sFlat3,converse(sk2)),meet(sk2,converse(sFlat3)))),
inference(step,[status(thm)],[t20515,t15145]) ).
cnf(t2563,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t2560,t72]) ).
cnf(t90348,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t2563,t68]) ).
cnf(t2622,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t90348]) ).
cnf(t69,plain,
meet(join(complement(X1),complement(X2)),X3) = complement(join(meet(X1,X2),complement(X3))),
inference(cp,[status(thm)],[t68,t68]) ).
cnf(t1102,plain,
complement(join(meet(X1,X2),complement(X3))) = meet(join(complement(X1),complement(X2)),X3),
inference(orient,[status(thm)],[t69]) ).
cnf(t1105,plain,
meet(join(complement(sk2),complement(sk1)),X1) = complement(join(sFlat3,complement(X1))),
inference(cp,[status(thm)],[t1102,t166]) ).
cnf(t1913,plain,
meet(join(complement(sk2),complement(sk1)),X1) = complement(join(sFlat3,complement(X1))),
inference(orient,[status(thm)],[t1105]) ).
cnf(t2625,plain,
join(complement(sk2),complement(sk1)) = join(zero,complement(join(sFlat3,complement(join(complement(sk2),complement(sk1)))))),
inference(cp,[status(thm)],[t2622,t1913]) ).
cnf(t90400,plain,
join(complement(sk2),complement(sk1)) = complement(join(sFlat3,complement(join(complement(sk2),complement(sk1))))),
inference(step,[status(thm)],[t2625,t2660]) ).
cnf(t90401,plain,
join(complement(sk2),complement(sk1)) = complement(join(sFlat3,meet(sk2,sk1))),
inference(step,[status(thm)],[t90400,t68]) ).
cnf(t90402,plain,
join(complement(sk2),complement(sk1)) = complement(join(sFlat3,sFlat3)),
inference(step,[status(thm)],[t90401,t166]) ).
cnf(t421,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t420,t68]) ).
cnf(t90314,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t421,t68]) ).
cnf(t90315,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t90314,t68]) ).
cnf(t2053,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t90315]) ).
cnf(t2054,plain,
meet(sk2,sk1) = join(sFlat3,meet(sk2,sk1)),
inference(cp,[status(thm)],[t2053,t166]) ).
cnf(t90316,plain,
sFlat3 = join(sFlat3,meet(sk2,sk1)),
inference(step,[status(thm)],[t2054,t166]) ).
cnf(t90317,plain,
sFlat3 = join(sFlat3,sFlat3),
inference(step,[status(thm)],[t90316,t166]) ).
cnf(t2058,plain,
join(sFlat3,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t90317]) ).
cnf(t90403,plain,
join(complement(sk2),complement(sk1)) = complement(sFlat3),
inference(step,[status(thm)],[t90402,t2058]) ).
cnf(t2919,plain,
join(complement(sk2),complement(sk1)) = complement(sFlat3),
inference(orient,[status(thm)],[t90403]) ).
cnf(t2922,plain,
join(top,complement(sk1)) = join(sk2,complement(sFlat3)),
inference(cp,[status(thm)],[t451,t2919]) ).
cnf(t90407,plain,
top = join(sk2,complement(sFlat3)),
inference(step,[status(thm)],[t2922,t474]) ).
cnf(t2932,plain,
join(sk2,complement(sFlat3)) = top,
inference(orient,[status(thm)],[t90407]) ).
cnf(t2968,plain,
meet(complement(sk2),sFlat3) = complement(top),
inference(cp,[status(thm)],[t2958,t2932]) ).
cnf(t90438,plain,
meet(sFlat3,complement(sk2)) = complement(top),
inference(step,[status(thm)],[t2968,t159]) ).
cnf(t90439,plain,
meet(sFlat3,complement(sk2)) = zero,
inference(step,[status(thm)],[t90438,t140]) ).
cnf(t3100,plain,
meet(sFlat3,complement(sk2)) = zero,
inference(orient,[status(thm)],[t90439]) ).
cnf(t3101,plain,
sFlat3 = join(zero,complement(join(complement(sFlat3),complement(sk2)))),
inference(cp,[status(thm)],[t2560,t3100]) ).
cnf(t90440,plain,
sFlat3 = complement(join(complement(sFlat3),complement(sk2))),
inference(step,[status(thm)],[t3101,t2660]) ).
cnf(t90441,plain,
sFlat3 = meet(sFlat3,sk2),
inference(step,[status(thm)],[t90440,t68]) ).
cnf(t3102,plain,
meet(sFlat3,sk2) = sFlat3,
inference(orient,[status(thm)],[t90441]) ).
cnf(t91486,plain,
composition(sFlat3,meet(sk2,converse(sFlat3))) = join(composition(sFlat3,sk2),composition(meet(sFlat3,converse(sk2)),meet(sk2,converse(sFlat3)))),
inference(step,[status(thm)],[t91485,t3102]) ).
cnf(t822,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = join(top,converse(X2)),
inference(cp,[status(thm)],[t821,t519]) ).
cnf(t90692,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = join(top,converse(X2)),
inference(step,[status(thm)],[t822,t102]) ).
cnf(t190,plain,
join(one,complement(one)) = join(sk2,top),
inference(cp,[status(thm)],[t189,t111]) ).
cnf(t90088,plain,
top = join(sk2,top),
inference(step,[status(thm)],[t190,t111]) ).
cnf(t90089,plain,
top = join(top,sk2),
inference(step,[status(thm)],[t90088,t102]) ).
cnf(t192,plain,
join(top,sk2) = top,
inference(orient,[status(thm)],[t90089]) ).
cnf(t193,plain,
join(top,join(sk2,X1)) = join(top,X1),
inference(cp,[status(thm)],[t104,t192]) ).
cnf(t503,plain,
join(top,join(sk2,X1)) = join(top,X1),
inference(orient,[status(thm)],[t193]) ).
cnf(t250,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t249,t111]) ).
cnf(t504,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t250]) ).
cnf(t512,plain,
join(top,converse(complement(converse(sk2)))) = join(top,converse(top)),
inference(cp,[status(thm)],[t503,t504]) ).
cnf(t485,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t249,t480]) ).
cnf(t486,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t485]) ).
cnf(t90180,plain,
join(top,converse(complement(converse(sk2)))) = converse(top),
inference(step,[status(thm)],[t512,t486]) ).
cnf(t847,plain,
join(top,converse(complement(converse(sk2)))) = converse(top),
inference(orient,[status(thm)],[t90180]) ).
cnf(t850,plain,
join(converse(complement(converse(sk2))),join(X1,top)) = join(X1,converse(top)),
inference(cp,[status(thm)],[t324,t847]) ).
cnf(t90181,plain,
join(converse(complement(converse(sk2))),top) = join(X1,converse(top)),
inference(step,[status(thm)],[t850,t480]) ).
cnf(t90182,plain,
top = join(X1,converse(top)),
inference(step,[status(thm)],[t90181,t480]) ).
cnf(t90183,plain,
top = converse(top),
inference(step,[status(thm)],[t90182,t486]) ).
cnf(t851,plain,
converse(top) = top,
inference(orient,[status(thm)],[t90183]) ).
cnf(t864,plain,
converse(join(top,X1)) = join(top,converse(X1)),
inference(cp,[status(thm)],[t130,t851]) ).
cnf(t879,plain,
converse(join(top,X1)) = join(top,converse(X1)),
inference(orient,[status(thm)],[t864]) ).
cnf(t900,plain,
join(top,converse(X1)) = converse(join(X1,top)),
inference(cp,[status(thm)],[t879,t102]) ).
cnf(t90197,plain,
join(top,converse(X1)) = converse(top),
inference(step,[status(thm)],[t900,t480]) ).
cnf(t90198,plain,
join(top,converse(X1)) = top,
inference(step,[status(thm)],[t90197,t851]) ).
cnf(t917,plain,
join(top,converse(X1)) = top,
inference(orient,[status(thm)],[t90198]) ).
cnf(t90693,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t90692,t917]) ).
cnf(t6629,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t90693]) ).
cnf(t6657,plain,
top = join(complement(converse(sFlat3)),converse(sk2)),
inference(cp,[status(thm)],[t6629,t3155]) ).
cnf(t90702,plain,
top = join(converse(sk2),complement(converse(sFlat3))),
inference(step,[status(thm)],[t6657,t102]) ).
cnf(t6731,plain,
join(converse(sk2),complement(converse(sFlat3))) = top,
inference(orient,[status(thm)],[t90702]) ).
cnf(t6732,plain,
meet(complement(converse(sk2)),converse(sFlat3)) = complement(top),
inference(cp,[status(thm)],[t2958,t6731]) ).
cnf(t90901,plain,
meet(converse(sFlat3),complement(converse(sk2))) = complement(top),
inference(step,[status(thm)],[t6732,t159]) ).
cnf(t90902,plain,
meet(converse(sFlat3),complement(converse(sk2))) = zero,
inference(step,[status(thm)],[t90901,t140]) ).
cnf(t10424,plain,
meet(converse(sFlat3),complement(converse(sk2))) = zero,
inference(orient,[status(thm)],[t90902]) ).
cnf(t10425,plain,
converse(sFlat3) = join(zero,meet(complement(complement(converse(sk2))),converse(sFlat3))),
inference(cp,[status(thm)],[t3308,t10424]) ).
cnf(t90903,plain,
converse(sFlat3) = meet(complement(complement(converse(sk2))),converse(sFlat3)),
inference(step,[status(thm)],[t10425,t2776]) ).
cnf(t90904,plain,
converse(sFlat3) = meet(converse(sFlat3),complement(complement(converse(sk2)))),
inference(step,[status(thm)],[t90903,t159]) ).
cnf(t90905,plain,
converse(sFlat3) = meet(converse(sFlat3),converse(sk2)),
inference(step,[status(thm)],[t90904,t2682]) ).
cnf(t10428,plain,
meet(converse(sFlat3),converse(sk2)) = converse(sFlat3),
inference(orient,[status(thm)],[t90905]) ).
cnf(t91095,plain,
meet(converse(sFlat3),sk2) = converse(sFlat3),
inference(step,[status(thm)],[t10428,t15145]) ).
cnf(t15216,plain,
meet(converse(sFlat3),sk2) = converse(sFlat3),
inference(rw,[status(thm)],[t91095]) ).
cnf(t91135,plain,
meet(sk2,converse(sFlat3)) = converse(sFlat3),
inference(step,[status(thm)],[t15216,t159]) ).
cnf(t15618,plain,
meet(sk2,converse(sFlat3)) = converse(sFlat3),
inference(orient,[status(thm)],[t91135]) ).
cnf(t91487,plain,
composition(sFlat3,converse(sFlat3)) = join(composition(sFlat3,sk2),composition(meet(sFlat3,converse(sk2)),meet(sk2,converse(sFlat3)))),
inference(step,[status(thm)],[t91486,t15618]) ).
cnf(t91488,plain,
composition(sFlat3,converse(sFlat3)) = join(composition(sFlat3,sk2),composition(meet(sFlat3,sk2),meet(sk2,converse(sFlat3)))),
inference(step,[status(thm)],[t91487,t15145]) ).
cnf(t91489,plain,
composition(sFlat3,converse(sFlat3)) = join(composition(sFlat3,sk2),composition(sFlat3,meet(sk2,converse(sFlat3)))),
inference(step,[status(thm)],[t91488,t3102]) ).
cnf(t214,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t130,t209]) ).
cnf(t3567,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t214]) ).
cnf(t52,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t44,t49]) ).
cnf(t9330,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t52]) ).
cnf(t9417,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)],[t3567,t9330]) ).
cnf(t90861,plain,
join(composition(X1,X2),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t9417,t31]) ).
cnf(t90862,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t90861,t31]) ).
cnf(t258,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t49,t249]) ).
cnf(t3811,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t258]) ).
cnf(t90863,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(converse(converse(X1)),join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t90862,t3811]) ).
cnf(t90864,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t90863,t31]) ).
cnf(t90865,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t90864,t31]) ).
cnf(t9424,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t90865]) ).
cnf(t91490,plain,
composition(sFlat3,converse(sFlat3)) = composition(sFlat3,join(sk2,meet(sk2,converse(sFlat3)))),
inference(step,[status(thm)],[t91489,t9424]) ).
cnf(t91491,plain,
composition(sFlat3,converse(sFlat3)) = composition(sFlat3,sk2),
inference(step,[status(thm)],[t91490,t3259]) ).
cnf(t20519,plain,
composition(sFlat3,converse(sFlat3)) = composition(sFlat3,sk2),
inference(orient,[status(thm)],[t91491]) ).
cnf(t15,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(t75,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)],[t15]) ).
cnf(t77,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)],[t75,t27]) ).
cnf(t91359,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)],[t77,t159]) ).
cnf(t91360,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)],[t91359,t159]) ).
cnf(t19194,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)],[t91360]) ).
cnf(t19930,plain,
top = join(complement(composition(converse(sFlat3),X1)),composition(one,X1)),
inference(cp,[status(thm)],[t19598,t3241]) ).
cnf(t91448,plain,
top = join(composition(one,X1),complement(composition(converse(sFlat3),X1))),
inference(step,[status(thm)],[t19930,t102]) ).
cnf(t91449,plain,
top = join(X1,complement(composition(converse(sFlat3),X1))),
inference(step,[status(thm)],[t91448,t243]) ).
cnf(t20002,plain,
join(X1,complement(composition(converse(sFlat3),X1))) = top,
inference(orient,[status(thm)],[t91449]) ).
cnf(t20042,plain,
meet(complement(X1),composition(converse(sFlat3),X1)) = complement(top),
inference(cp,[status(thm)],[t2958,t20002]) ).
cnf(t91505,plain,
meet(complement(X1),composition(converse(sFlat3),X1)) = zero,
inference(step,[status(thm)],[t20042,t140]) ).
cnf(t20810,plain,
meet(complement(X1),composition(converse(sFlat3),X1)) = zero,
inference(orient,[status(thm)],[t91505]) ).
cnf(t20823,plain,
composition(converse(sFlat3),X1) = join(meet(composition(converse(sFlat3),X1),X1),zero),
inference(cp,[status(thm)],[t3308,t20810]) ).
cnf(t91506,plain,
composition(converse(sFlat3),X1) = meet(composition(converse(sFlat3),X1),X1),
inference(step,[status(thm)],[t20823,t2824]) ).
cnf(t91507,plain,
composition(converse(sFlat3),X1) = meet(X1,composition(converse(sFlat3),X1)),
inference(step,[status(thm)],[t91506,t159]) ).
cnf(t20840,plain,
meet(X1,composition(converse(sFlat3),X1)) = composition(converse(sFlat3),X1),
inference(orient,[status(thm)],[t91507]) ).
cnf(t20885,plain,
meet(one,composition(sFlat3,meet(one,composition(converse(sFlat3),one)))) = join(meet(sFlat3,one),meet(one,composition(sFlat3,composition(converse(sFlat3),one)))),
inference(cp,[status(thm)],[t19194,t20840]) ).
cnf(t91508,plain,
meet(one,composition(sFlat3,composition(converse(sFlat3),one))) = join(meet(sFlat3,one),meet(one,composition(sFlat3,composition(converse(sFlat3),one)))),
inference(step,[status(thm)],[t20885,t20840]) ).
cnf(t91509,plain,
meet(one,composition(sFlat3,converse(sFlat3))) = join(meet(sFlat3,one),meet(one,composition(sFlat3,composition(converse(sFlat3),one)))),
inference(step,[status(thm)],[t91508,t27]) ).
cnf(t91510,plain,
meet(one,composition(sFlat3,sk2)) = join(meet(sFlat3,one),meet(one,composition(sFlat3,composition(converse(sFlat3),one)))),
inference(step,[status(thm)],[t91509,t20519]) ).
cnf(t91511,plain,
composition(sFlat3,sk2) = join(meet(sFlat3,one),meet(one,composition(sFlat3,composition(converse(sFlat3),one)))),
inference(step,[status(thm)],[t91510,t20508]) ).
cnf(t309,plain,
converse(join(join(X1,one),X2)) = join(join(one,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t130,t305]) ).
cnf(t90209,plain,
converse(join(X1,join(one,X2))) = join(join(one,converse(X1)),converse(X2)),
inference(step,[status(thm)],[t309,t104]) ).
cnf(t90210,plain,
converse(join(X1,join(one,X2))) = join(one,join(converse(X1),converse(X2))),
inference(step,[status(thm)],[t90209,t104]) ).
cnf(t90211,plain,
converse(join(X1,join(one,X2))) = join(one,converse(join(X1,X2))),
inference(step,[status(thm)],[t90210,t130]) ).
cnf(t1062,plain,
converse(join(X1,join(one,X2))) = join(one,converse(join(X1,X2))),
inference(orient,[status(thm)],[t90211]) ).
cnf(t90121,plain,
join(one,complement(sk1)) = top,
inference(step,[status(thm)],[t490,t494]) ).
cnf(t497,plain,
join(one,complement(sk1)) = top,
inference(orient,[status(thm)],[t90121]) ).
cnf(t1074,plain,
join(one,converse(join(X1,complement(sk1)))) = converse(join(X1,top)),
inference(cp,[status(thm)],[t1062,t497]) ).
cnf(t90344,plain,
join(one,converse(join(X1,complement(sk1)))) = converse(top),
inference(step,[status(thm)],[t1074,t480]) ).
cnf(t90345,plain,
join(one,converse(join(X1,complement(sk1)))) = top,
inference(step,[status(thm)],[t90344,t851]) ).
cnf(t2549,plain,
join(one,converse(join(X1,complement(sk1)))) = top,
inference(orient,[status(thm)],[t90345]) ).
cnf(t2924,plain,
top = join(one,converse(complement(sFlat3))),
inference(cp,[status(thm)],[t2549,t2919]) ).
cnf(t3229,plain,
join(one,converse(complement(sFlat3))) = top,
inference(orient,[status(thm)],[t2924]) ).
cnf(t3230,plain,
join(one,converse(converse(complement(sFlat3)))) = converse(top),
inference(cp,[status(thm)],[t265,t3229]) ).
cnf(t90474,plain,
join(one,complement(sFlat3)) = converse(top),
inference(step,[status(thm)],[t3230,t31]) ).
cnf(t90475,plain,
join(one,complement(sFlat3)) = top,
inference(step,[status(thm)],[t90474,t851]) ).
cnf(t3236,plain,
join(one,complement(sFlat3)) = top,
inference(orient,[status(thm)],[t90475]) ).
cnf(t3237,plain,
meet(complement(one),sFlat3) = complement(top),
inference(cp,[status(thm)],[t2958,t3236]) ).
cnf(t90480,plain,
meet(sFlat3,complement(one)) = complement(top),
inference(step,[status(thm)],[t3237,t159]) ).
cnf(t90481,plain,
meet(sFlat3,complement(one)) = zero,
inference(step,[status(thm)],[t90480,t140]) ).
cnf(t3253,plain,
meet(sFlat3,complement(one)) = zero,
inference(orient,[status(thm)],[t90481]) ).
cnf(t3254,plain,
sFlat3 = join(zero,meet(sFlat3,complement(complement(one)))),
inference(cp,[status(thm)],[t3165,t3253]) ).
cnf(t90482,plain,
sFlat3 = meet(sFlat3,complement(complement(one))),
inference(step,[status(thm)],[t3254,t2776]) ).
cnf(t90483,plain,
sFlat3 = meet(sFlat3,one),
inference(step,[status(thm)],[t90482,t2682]) ).
cnf(t3256,plain,
meet(sFlat3,one) = sFlat3,
inference(orient,[status(thm)],[t90483]) ).
cnf(t91512,plain,
composition(sFlat3,sk2) = join(sFlat3,meet(one,composition(sFlat3,composition(converse(sFlat3),one)))),
inference(step,[status(thm)],[t91511,t3256]) ).
cnf(t91513,plain,
composition(sFlat3,sk2) = join(sFlat3,meet(one,composition(sFlat3,converse(sFlat3)))),
inference(step,[status(thm)],[t91512,t27]) ).
cnf(t91514,plain,
composition(sFlat3,sk2) = join(sFlat3,meet(one,composition(sFlat3,sk2))),
inference(step,[status(thm)],[t91513,t20519]) ).
cnf(t91515,plain,
composition(sFlat3,sk2) = join(sFlat3,composition(sFlat3,sk2)),
inference(step,[status(thm)],[t91514,t20508]) ).
cnf(t537,plain,
join(X1,composition(converse(sk2),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t533,t320]) ).
cnf(t90136,plain,
join(X1,composition(converse(sk2),X1)) = X1,
inference(step,[status(thm)],[t537,t243]) ).
cnf(t646,plain,
join(X1,composition(converse(sk2),X1)) = X1,
inference(orient,[status(thm)],[t90136]) ).
cnf(t653,plain,
join(X1,converse(composition(converse(sk2),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t249,t646]) ).
cnf(t90137,plain,
join(X1,composition(converse(converse(X1)),sk2)) = converse(converse(X1)),
inference(step,[status(thm)],[t653,t209]) ).
cnf(t90138,plain,
join(X1,composition(X1,sk2)) = converse(converse(X1)),
inference(step,[status(thm)],[t90137,t31]) ).
cnf(t90139,plain,
join(X1,composition(X1,sk2)) = X1,
inference(step,[status(thm)],[t90138,t31]) ).
cnf(t655,plain,
join(X1,composition(X1,sk2)) = X1,
inference(orient,[status(thm)],[t90139]) ).
cnf(t91516,plain,
composition(sFlat3,sk2) = sFlat3,
inference(step,[status(thm)],[t91515,t655]) ).
cnf(t20889,plain,
composition(sFlat3,sk2) = sFlat3,
inference(orient,[status(thm)],[t91516]) ).
cnf(t91517,plain,
composition(sFlat3,converse(sFlat3)) = sFlat3,
inference(step,[status(thm)],[t20519,t20889]) ).
cnf(t20890,plain,
composition(sFlat3,converse(sFlat3)) = sFlat3,
inference(orient,[status(thm)],[t91517]) ).
cnf(t15149,plain,
converse(composition(X1,sk2)) = composition(sk2,converse(X1)),
inference(cp,[status(thm)],[t49,t15145]) ).
cnf(t15460,plain,
converse(composition(X1,sk2)) = composition(sk2,converse(X1)),
inference(orient,[status(thm)],[t15149]) ).
cnf(t20894,plain,
composition(sk2,converse(sFlat3)) = converse(sFlat3),
inference(cp,[status(thm)],[t15460,t20889]) ).
cnf(t20543,plain,
composition(sFlat3,converse(sFlat3)) = converse(composition(sFlat3,sk2)),
inference(cp,[status(thm)],[t199,t20519]) ).
cnf(t91498,plain,
composition(sFlat3,sk2) = converse(composition(sFlat3,sk2)),
inference(step,[status(thm)],[t20543,t20519]) ).
cnf(t91499,plain,
composition(sFlat3,sk2) = composition(sk2,converse(sFlat3)),
inference(step,[status(thm)],[t91498,t15460]) ).
cnf(t20637,plain,
composition(sk2,converse(sFlat3)) = composition(sFlat3,sk2),
inference(orient,[status(thm)],[t91499]) ).
cnf(t91519,plain,
composition(sk2,converse(sFlat3)) = sFlat3,
inference(step,[status(thm)],[t20637,t20889]) ).
cnf(t20892,plain,
composition(sk2,converse(sFlat3)) = sFlat3,
inference(orient,[status(thm)],[t91519]) ).
cnf(t91524,plain,
sFlat3 = converse(sFlat3),
inference(step,[status(thm)],[t20894,t20892]) ).
cnf(t20931,plain,
converse(sFlat3) = sFlat3,
inference(orient,[status(thm)],[t91524]) ).
cnf(t91528,plain,
composition(sFlat3,sFlat3) = sFlat3,
inference(step,[status(thm)],[t20890,t20931]) ).
cnf(t21006,plain,
composition(sFlat3,sFlat3) = sFlat3,
inference(rw,[status(thm)],[t91528]) ).
cnf(t21061,plain,
composition(sFlat3,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t21006]) ).
cnf(t21066,plain,
composition(sFlat3,composition(sFlat3,X1)) = composition(sFlat3,X1),
inference(cp,[status(thm)],[t32,t21061]) ).
cnf(t21494,plain,
composition(sFlat3,composition(sFlat3,X1)) = composition(sFlat3,X1),
inference(orient,[status(thm)],[t21066]) ).
cnf(t21499,plain,
composition(sFlat3,sk3) = composition(sFlat3,sFlat4),
inference(cp,[status(thm)],[t21494,t146]) ).
cnf(t91555,plain,
sFlat4 = composition(sFlat3,sFlat4),
inference(step,[status(thm)],[t21499,t146]) ).
cnf(t21534,plain,
composition(sFlat3,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t91555]) ).
cnf(t21538,plain,
composition(join(sFlat3,X1),sFlat4) = join(sFlat4,composition(X1,sFlat4)),
inference(cp,[status(thm)],[t44,t21534]) ).
cnf(t22271,plain,
composition(join(sFlat3,X1),sFlat4) = join(sFlat4,composition(X1,sFlat4)),
inference(orient,[status(thm)],[t21538]) ).
cnf(t2217,plain,
join(X1,composition(X1,X2)) = composition(X1,join(X2,one)),
inference(cp,[status(thm)],[t2179,t102]) ).
cnf(t2449,plain,
join(X1,composition(X1,X2)) = composition(X1,join(X2,one)),
inference(orient,[status(thm)],[t2217]) ).
cnf(t3251,plain,
join(X1,composition(X1,sFlat3)) = composition(X1,one),
inference(cp,[status(thm)],[t2449,t3248]) ).
cnf(t91069,plain,
join(X1,composition(X1,sFlat3)) = X1,
inference(step,[status(thm)],[t3251,t27]) ).
cnf(t14724,plain,
join(X1,composition(X1,sFlat3)) = X1,
inference(orient,[status(thm)],[t91069]) ).
cnf(t21064,plain,
composition(join(sFlat3,X1),sFlat3) = join(sFlat3,composition(X1,sFlat3)),
inference(cp,[status(thm)],[t44,t21061]) ).
cnf(t21757,plain,
composition(join(sFlat3,X1),sFlat3) = join(sFlat3,composition(X1,sFlat3)),
inference(orient,[status(thm)],[t21064]) ).
cnf(t19240,plain,
meet(sk1,composition(sk2,meet(one,composition(converse(sk2),sk1)))) = join(sFlat3,meet(sk1,composition(sk2,meet(one,composition(converse(sk2),sk1))))),
inference(cp,[status(thm)],[t19194,t166]) ).
cnf(t91361,plain,
meet(sk1,composition(sk2,meet(one,composition(sk2,sk1)))) = join(sFlat3,meet(sk1,composition(sk2,meet(one,composition(converse(sk2),sk1))))),
inference(step,[status(thm)],[t19240,t15145]) ).
cnf(t307,plain,
join(one,converse(sk1)) = converse(one),
inference(cp,[status(thm)],[t305,t134]) ).
cnf(t90098,plain,
join(one,converse(sk1)) = one,
inference(step,[status(thm)],[t307,t232]) ).
cnf(t322,plain,
join(one,converse(sk1)) = one,
inference(orient,[status(thm)],[t90098]) ).
cnf(t323,plain,
join(one,join(converse(sk1),X1)) = join(one,X1),
inference(cp,[status(thm)],[t104,t322]) ).
cnf(t983,plain,
join(one,join(converse(sk1),X1)) = join(one,X1),
inference(orient,[status(thm)],[t323]) ).
cnf(t986,plain,
join(one,composition(converse(sk1),converse(sk2))) = join(one,converse(sk1)),
inference(cp,[status(thm)],[t983,t782]) ).
cnf(t90231,plain,
join(one,converse(composition(sk2,sk1))) = join(one,converse(sk1)),
inference(step,[status(thm)],[t986,t49]) ).
cnf(t90232,plain,
join(one,converse(composition(sk2,sk1))) = one,
inference(step,[status(thm)],[t90231,t322]) ).
cnf(t1258,plain,
join(one,converse(composition(sk2,sk1))) = one,
inference(orient,[status(thm)],[t90232]) ).
cnf(t1363,plain,
top = join(complement(converse(converse(composition(sk2,sk1)))),converse(one)),
inference(cp,[status(thm)],[t1311,t1258]) ).
cnf(t90510,plain,
top = join(converse(one),complement(converse(converse(composition(sk2,sk1))))),
inference(step,[status(thm)],[t1363,t102]) ).
cnf(t90511,plain,
top = join(one,complement(converse(converse(composition(sk2,sk1))))),
inference(step,[status(thm)],[t90510,t232]) ).
cnf(t90512,plain,
top = join(one,complement(composition(sk2,sk1))),
inference(step,[status(thm)],[t90511,t31]) ).
cnf(t4058,plain,
join(one,complement(composition(sk2,sk1))) = top,
inference(orient,[status(thm)],[t90512]) ).
cnf(t4060,plain,
meet(complement(one),composition(sk2,sk1)) = complement(top),
inference(cp,[status(thm)],[t2958,t4058]) ).
cnf(t90563,plain,
meet(complement(one),composition(sk2,sk1)) = zero,
inference(step,[status(thm)],[t4060,t140]) ).
cnf(t5493,plain,
meet(complement(one),composition(sk2,sk1)) = zero,
inference(orient,[status(thm)],[t90563]) ).
cnf(t5494,plain,
composition(sk2,sk1) = join(meet(composition(sk2,sk1),one),zero),
inference(cp,[status(thm)],[t3308,t5493]) ).
cnf(t90574,plain,
composition(sk2,sk1) = meet(composition(sk2,sk1),one),
inference(step,[status(thm)],[t5494,t2824]) ).
cnf(t90575,plain,
composition(sk2,sk1) = meet(one,composition(sk2,sk1)),
inference(step,[status(thm)],[t90574,t159]) ).
cnf(t5524,plain,
meet(one,composition(sk2,sk1)) = composition(sk2,sk1),
inference(orient,[status(thm)],[t90575]) ).
cnf(t91362,plain,
meet(sk1,composition(sk2,composition(sk2,sk1))) = join(sFlat3,meet(sk1,composition(sk2,meet(one,composition(converse(sk2),sk1))))),
inference(step,[status(thm)],[t91361,t5524]) ).
cnf(t91094,plain,
composition(sk2,sk2) = sk2,
inference(step,[status(thm)],[t15091,t15145]) ).
cnf(t15215,plain,
composition(sk2,sk2) = sk2,
inference(rw,[status(thm)],[t91094]) ).
cnf(t15235,plain,
composition(sk2,sk2) = sk2,
inference(orient,[status(thm)],[t15215]) ).
cnf(t15240,plain,
composition(sk2,composition(sk2,X1)) = composition(sk2,X1),
inference(cp,[status(thm)],[t32,t15235]) ).
cnf(t16008,plain,
composition(sk2,composition(sk2,X1)) = composition(sk2,X1),
inference(orient,[status(thm)],[t15240]) ).
cnf(t91363,plain,
meet(sk1,composition(sk2,sk1)) = join(sFlat3,meet(sk1,composition(sk2,meet(one,composition(converse(sk2),sk1))))),
inference(step,[status(thm)],[t91362,t16008]) ).
cnf(t91364,plain,
composition(sk2,sk1) = join(sFlat3,meet(sk1,composition(sk2,meet(one,composition(converse(sk2),sk1))))),
inference(step,[status(thm)],[t91363,t15061]) ).
cnf(t91365,plain,
composition(sk2,sk1) = join(sFlat3,meet(sk1,composition(sk2,meet(one,composition(sk2,sk1))))),
inference(step,[status(thm)],[t91364,t15145]) ).
cnf(t91366,plain,
composition(sk2,sk1) = join(sFlat3,meet(sk1,composition(sk2,composition(sk2,sk1)))),
inference(step,[status(thm)],[t91365,t5524]) ).
cnf(t91367,plain,
composition(sk2,sk1) = join(sFlat3,meet(sk1,composition(sk2,sk1))),
inference(step,[status(thm)],[t91366,t16008]) ).
cnf(t91368,plain,
composition(sk2,sk1) = join(sFlat3,composition(sk2,sk1)),
inference(step,[status(thm)],[t91367,t15061]) ).
cnf(t19326,plain,
join(sFlat3,composition(sk2,sk1)) = composition(sk2,sk1),
inference(orient,[status(thm)],[t91368]) ).
cnf(t21760,plain,
join(sFlat3,composition(composition(sk2,sk1),sFlat3)) = composition(composition(sk2,sk1),sFlat3),
inference(cp,[status(thm)],[t21757,t19326]) ).
cnf(t91591,plain,
join(sFlat3,composition(sk2,composition(sk1,sFlat3))) = composition(composition(sk2,sk1),sFlat3),
inference(step,[status(thm)],[t21760,t32]) ).
cnf(t1259,plain,
join(one,converse(converse(composition(sk2,sk1)))) = converse(one),
inference(cp,[status(thm)],[t265,t1258]) ).
cnf(t90233,plain,
join(one,composition(sk2,sk1)) = converse(one),
inference(step,[status(thm)],[t1259,t31]) ).
cnf(t90234,plain,
join(one,composition(sk2,sk1)) = one,
inference(step,[status(thm)],[t90233,t232]) ).
cnf(t1263,plain,
join(one,composition(sk2,sk1)) = one,
inference(orient,[status(thm)],[t90234]) ).
cnf(t1265,plain,
join(X1,composition(composition(sk2,sk1),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t533,t1263]) ).
cnf(t91062,plain,
join(X1,composition(sk2,composition(sk1,X1))) = composition(one,X1),
inference(step,[status(thm)],[t1265,t32]) ).
cnf(t91063,plain,
join(X1,composition(sk2,composition(sk1,X1))) = X1,
inference(step,[status(thm)],[t91062,t243]) ).
cnf(t14453,plain,
join(X1,composition(sk2,composition(sk1,X1))) = X1,
inference(orient,[status(thm)],[t91063]) ).
cnf(t91592,plain,
sFlat3 = composition(composition(sk2,sk1),sFlat3),
inference(step,[status(thm)],[t91591,t14453]) ).
cnf(t91593,plain,
sFlat3 = composition(sk2,composition(sk1,sFlat3)),
inference(step,[status(thm)],[t91592,t32]) ).
cnf(t22724,plain,
composition(sk2,composition(sk1,sFlat3)) = sFlat3,
inference(orient,[status(thm)],[t91593]) ).
cnf(t22727,plain,
composition(sk2,composition(sk1,sFlat3)) = meet(composition(sk1,sFlat3),sFlat3),
inference(cp,[status(thm)],[t15061,t22724]) ).
cnf(t91614,plain,
sFlat3 = meet(composition(sk1,sFlat3),sFlat3),
inference(step,[status(thm)],[t22727,t22724]) ).
cnf(t91615,plain,
sFlat3 = meet(sFlat3,composition(sk1,sFlat3)),
inference(step,[status(thm)],[t91614,t159]) ).
cnf(t538,plain,
join(X1,composition(converse(sk1),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t533,t322]) ).
cnf(t90140,plain,
join(X1,composition(converse(sk1),X1)) = X1,
inference(step,[status(thm)],[t538,t243]) ).
cnf(t665,plain,
join(X1,composition(converse(sk1),X1)) = X1,
inference(orient,[status(thm)],[t90140]) ).
cnf(t672,plain,
join(X1,converse(composition(converse(sk1),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t249,t665]) ).
cnf(t90141,plain,
join(X1,composition(converse(converse(X1)),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t672,t209]) ).
cnf(t90142,plain,
join(X1,composition(X1,sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t90141,t31]) ).
cnf(t90143,plain,
join(X1,composition(X1,sk1)) = X1,
inference(step,[status(thm)],[t90142,t31]) ).
cnf(t674,plain,
join(X1,composition(X1,sk1)) = X1,
inference(orient,[status(thm)],[t90143]) ).
cnf(t1329,plain,
top = join(complement(converse(composition(X1,sk1))),converse(X1)),
inference(cp,[status(thm)],[t1311,t674]) ).
cnf(t91217,plain,
top = join(converse(X1),complement(converse(composition(X1,sk1)))),
inference(step,[status(thm)],[t1329,t102]) ).
cnf(t16701,plain,
join(converse(X1),complement(converse(composition(X1,sk1)))) = top,
inference(orient,[status(thm)],[t91217]) ).
cnf(t16730,plain,
top = join(X1,complement(converse(composition(converse(X1),sk1)))),
inference(cp,[status(thm)],[t16701,t31]) ).
cnf(t91218,plain,
top = join(X1,complement(composition(converse(sk1),X1))),
inference(step,[status(thm)],[t16730,t209]) ).
cnf(t16763,plain,
join(X1,complement(composition(converse(sk1),X1))) = top,
inference(orient,[status(thm)],[t91218]) ).
cnf(t16795,plain,
meet(X1,complement(complement(composition(converse(sk1),complement(X1))))) = complement(top),
inference(cp,[status(thm)],[t3106,t16763]) ).
cnf(t91278,plain,
meet(X1,composition(converse(sk1),complement(X1))) = complement(top),
inference(step,[status(thm)],[t16795,t2682]) ).
cnf(t91279,plain,
meet(X1,composition(converse(sk1),complement(X1))) = zero,
inference(step,[status(thm)],[t91278,t140]) ).
cnf(t17583,plain,
meet(X1,composition(converse(sk1),complement(X1))) = zero,
inference(orient,[status(thm)],[t91279]) ).
cnf(t17598,plain,
composition(meet(sk1,composition(complement(X1),converse(X1))),meet(X1,composition(converse(sk1),complement(X1)))) = join(meet(composition(sk1,X1),complement(X1)),composition(meet(sk1,composition(complement(X1),converse(X1))),zero)),
inference(cp,[status(thm)],[t34,t17583]) ).
cnf(t91280,plain,
composition(meet(sk1,composition(complement(X1),converse(X1))),zero) = join(meet(composition(sk1,X1),complement(X1)),composition(meet(sk1,composition(complement(X1),converse(X1))),zero)),
inference(step,[status(thm)],[t17598,t17583]) ).
cnf(t90199,plain,
converse(join(top,X1)) = top,
inference(step,[status(thm)],[t879,t917]) ).
cnf(t918,plain,
converse(join(top,X1)) = top,
inference(orient,[status(thm)],[t90199]) ).
cnf(t536,plain,
join(X1,composition(complement(sk1),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t533,t497]) ).
cnf(t1446,plain,
join(X1,composition(complement(sk1),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t536]) ).
cnf(t1448,plain,
top = converse(composition(top,top)),
inference(cp,[status(thm)],[t918,t1446]) ).
cnf(t866,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t49,t851]) ).
cnf(t945,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t866]) ).
cnf(t90254,plain,
top = composition(converse(top),top),
inference(step,[status(thm)],[t1448,t945]) ).
cnf(t90255,plain,
top = composition(top,top),
inference(step,[status(thm)],[t90254,t851]) ).
cnf(t1462,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t90255]) ).
cnf(t1465,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t118,t1462]) ).
cnf(t90256,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t1465,t140]) ).
cnf(t90257,plain,
zero = composition(join(converse(top),one),complement(top)),
inference(step,[status(thm)],[t90256,t558]) ).
cnf(t90258,plain,
zero = composition(join(one,converse(top)),complement(top)),
inference(step,[status(thm)],[t90257,t102]) ).
cnf(t90259,plain,
zero = composition(converse(top),complement(top)),
inference(step,[status(thm)],[t90258,t486]) ).
cnf(t90260,plain,
zero = composition(top,complement(top)),
inference(step,[status(thm)],[t90259,t851]) ).
cnf(t90261,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t90260,t140]) ).
cnf(t1467,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t90261]) ).
cnf(t1470,plain,
composition(join(X1,top),zero) = join(composition(X1,zero),zero),
inference(cp,[status(thm)],[t44,t1467]) ).
cnf(t90270,plain,
composition(top,zero) = join(composition(X1,zero),zero),
inference(step,[status(thm)],[t1470,t480]) ).
cnf(t90271,plain,
zero = join(composition(X1,zero),zero),
inference(step,[status(thm)],[t90270,t1467]) ).
cnf(t90272,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t90271,t102]) ).
cnf(t1581,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t90272]) ).
cnf(t90385,plain,
composition(X1,zero) = zero,
inference(step,[status(thm)],[t1581,t2783]) ).
cnf(t2814,plain,
composition(X1,zero) = zero,
inference(rw,[status(thm)],[t90385]) ).
cnf(t2835,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t2814]) ).
cnf(t91281,plain,
zero = join(meet(composition(sk1,X1),complement(X1)),composition(meet(sk1,composition(complement(X1),converse(X1))),zero)),
inference(step,[status(thm)],[t91280,t2835]) ).
cnf(t91282,plain,
zero = join(meet(complement(X1),composition(sk1,X1)),composition(meet(sk1,composition(complement(X1),converse(X1))),zero)),
inference(step,[status(thm)],[t91281,t159]) ).
cnf(t91283,plain,
zero = join(meet(complement(X1),composition(sk1,X1)),zero),
inference(step,[status(thm)],[t91282,t2835]) ).
cnf(t91284,plain,
zero = meet(complement(X1),composition(sk1,X1)),
inference(step,[status(thm)],[t91283,t2824]) ).
cnf(t17606,plain,
meet(complement(X1),composition(sk1,X1)) = zero,
inference(orient,[status(thm)],[t91284]) ).
cnf(t17623,plain,
composition(sk1,X1) = join(meet(composition(sk1,X1),X1),zero),
inference(cp,[status(thm)],[t3308,t17606]) ).
cnf(t91285,plain,
composition(sk1,X1) = meet(composition(sk1,X1),X1),
inference(step,[status(thm)],[t17623,t2824]) ).
cnf(t91286,plain,
composition(sk1,X1) = meet(X1,composition(sk1,X1)),
inference(step,[status(thm)],[t91285,t159]) ).
cnf(t17630,plain,
meet(X1,composition(sk1,X1)) = composition(sk1,X1),
inference(orient,[status(thm)],[t91286]) ).
cnf(t91616,plain,
sFlat3 = composition(sk1,sFlat3),
inference(step,[status(thm)],[t91615,t17630]) ).
cnf(t23352,plain,
composition(sk1,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t91616]) ).
cnf(t23355,plain,
sk1 = join(sk1,sFlat3),
inference(cp,[status(thm)],[t14724,t23352]) ).
cnf(t91621,plain,
sk1 = join(sFlat3,sk1),
inference(step,[status(thm)],[t23355,t102]) ).
cnf(t23431,plain,
join(sFlat3,sk1) = sk1,
inference(orient,[status(thm)],[t91621]) ).
cnf(t23434,plain,
join(sFlat4,composition(sk1,sFlat4)) = composition(sk1,sFlat4),
inference(cp,[status(thm)],[t22271,t23431]) ).
cnf(t561,plain,
join(X1,composition(sk1,X1)) = composition(one,X1),
inference(cp,[status(thm)],[t558,t134]) ).
cnf(t90127,plain,
join(X1,composition(sk1,X1)) = X1,
inference(step,[status(thm)],[t561,t243]) ).
cnf(t581,plain,
join(X1,composition(sk1,X1)) = X1,
inference(orient,[status(thm)],[t90127]) ).
cnf(t91624,plain,
sFlat4 = composition(sk1,sFlat4),
inference(step,[status(thm)],[t23434,t581]) ).
cnf(t23441,plain,
composition(sk1,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t91624]) ).
cnf(t91629,plain,
join(sFlat0,sFlat4) = sFlat0,
inference(step,[status(thm)],[t7295,t23441]) ).
cnf(t23482,plain,
join(sFlat0,sFlat4) = sFlat0,
inference(rw,[status(thm)],[t91629]) ).
cnf(t23484,plain,
join(sFlat0,sFlat4) = sFlat0,
inference(orient,[status(thm)],[t23482]) ).
cnf(t23486,plain,
zero = meet(sFlat4,complement(sFlat0)),
inference(cp,[status(thm)],[t12358,t23484]) ).
cnf(t23488,plain,
meet(sFlat4,complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t23486]) ).
cnf(t89469,plain,
meet(sFlat4,join(X1,complement(sFlat0))) = meet(sFlat4,join(X1,zero)),
inference(cp,[status(thm)],[t89119,t23488]) ).
cnf(t94088,plain,
meet(sFlat4,join(X1,complement(sFlat0))) = meet(sFlat4,X1),
inference(step,[status(thm)],[t89469,t2824]) ).
cnf(t89700,plain,
meet(sFlat4,join(X1,complement(sFlat0))) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t94088]) ).
cnf(t71827,plain,
meet(X1,complement(X2)) = meet(X1,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t71819,t2935]) ).
cnf(t75798,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t71827]) ).
cnf(t20,axiom,
sFlat2 = meet(composition(sk1,sk3),composition(sk2,sk3)),
introduced(definition) ).
cnf(t90044,plain,
sFlat2 = meet(sFlat0,composition(sk2,sk3)),
inference(step,[status(thm)],[t20,t58]) ).
cnf(t19,axiom,
sFlat1 = composition(sk2,sk3),
introduced(definition) ).
cnf(t63,plain,
composition(sk2,sk3) = sFlat1,
inference(orient,[status(thm)],[t19]) ).
cnf(t90045,plain,
sFlat2 = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t90044,t63]) ).
cnf(t99,plain,
meet(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t90045]) ).
cnf(t75881,plain,
meet(sFlat0,complement(sFlat1)) = meet(sFlat0,complement(sFlat2)),
inference(cp,[status(thm)],[t75798,t99]) ).
cnf(t75940,plain,
meet(sFlat0,complement(sFlat2)) = meet(sFlat0,complement(sFlat1)),
inference(orient,[status(thm)],[t75881]) ).
cnf(t75945,plain,
join(complement(sFlat0),sFlat2) = complement(meet(sFlat0,complement(sFlat1))),
inference(cp,[status(thm)],[t3288,t75940]) ).
cnf(t93524,plain,
join(sFlat2,complement(sFlat0)) = complement(meet(sFlat0,complement(sFlat1))),
inference(step,[status(thm)],[t75945,t102]) ).
cnf(t93525,plain,
join(sFlat2,complement(sFlat0)) = join(complement(sFlat0),sFlat1),
inference(step,[status(thm)],[t93524,t3288]) ).
cnf(t93526,plain,
join(sFlat2,complement(sFlat0)) = join(sFlat1,complement(sFlat0)),
inference(step,[status(thm)],[t93525,t102]) ).
cnf(t75950,plain,
join(sFlat2,complement(sFlat0)) = join(sFlat1,complement(sFlat0)),
inference(orient,[status(thm)],[t93526]) ).
cnf(t89701,plain,
meet(sFlat4,sFlat2) = meet(sFlat4,join(sFlat1,complement(sFlat0))),
inference(cp,[status(thm)],[t89700,t75950]) ).
cnf(t94089,plain,
meet(sFlat2,sFlat4) = meet(sFlat4,join(sFlat1,complement(sFlat0))),
inference(step,[status(thm)],[t89701,t159]) ).
cnf(t3268,plain,
meet(X1,complement(meet(complement(X1),X2))) = complement(complement(X1)),
inference(cp,[status(thm)],[t3106,t3259]) ).
cnf(t90961,plain,
meet(X1,join(X1,complement(X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t3268,t3193]) ).
cnf(t90962,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t90961,t2682]) ).
cnf(t11043,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t90962]) ).
cnf(t11047,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t11043,t2682]) ).
cnf(t11056,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t11047]) ).
cnf(t78,plain,
meet(composition(sk2,meet(sk3,composition(converse(sk2),X1))),X1) = join(meet(sFlat1,X1),meet(composition(sk2,meet(sk3,composition(converse(sk2),X1))),X1)),
inference(cp,[status(thm)],[t75,t63]) ).
cnf(t91468,plain,
meet(X1,composition(sk2,meet(sk3,composition(converse(sk2),X1)))) = join(meet(sFlat1,X1),meet(composition(sk2,meet(sk3,composition(converse(sk2),X1))),X1)),
inference(step,[status(thm)],[t78,t159]) ).
cnf(t91469,plain,
meet(X1,composition(sk2,meet(sk3,composition(sk2,X1)))) = join(meet(sFlat1,X1),meet(composition(sk2,meet(sk3,composition(converse(sk2),X1))),X1)),
inference(step,[status(thm)],[t91468,t15145]) ).
cnf(t91470,plain,
meet(X1,composition(sk2,meet(sk3,composition(sk2,X1)))) = join(meet(sFlat1,X1),meet(X1,composition(sk2,meet(sk3,composition(converse(sk2),X1))))),
inference(step,[status(thm)],[t91469,t159]) ).
cnf(t91471,plain,
meet(X1,composition(sk2,meet(sk3,composition(sk2,X1)))) = join(meet(sFlat1,X1),meet(X1,composition(sk2,meet(sk3,composition(sk2,X1))))),
inference(step,[status(thm)],[t91470,t15145]) ).
cnf(t20386,plain,
join(meet(sFlat1,X1),meet(X1,composition(sk2,meet(sk3,composition(sk2,X1))))) = meet(X1,composition(sk2,meet(sk3,composition(sk2,X1)))),
inference(orient,[status(thm)],[t91471]) ).
cnf(t6819,plain,
composition(join(composition(X1,sk1),X2),sk3) = join(composition(X1,sFlat0),composition(X2,sk3)),
inference(cp,[status(thm)],[t6761,t58]) ).
cnf(t7045,plain,
composition(join(composition(X1,sk1),X2),sk3) = join(composition(X1,sFlat0),composition(X2,sk3)),
inference(orient,[status(thm)],[t6819]) ).
cnf(t7085,plain,
join(composition(X1,sFlat0),composition(X2,sk3)) = composition(join(X2,composition(X1,sk1)),sk3),
inference(cp,[status(thm)],[t7045,t102]) ).
cnf(t7432,plain,
composition(join(X1,composition(X2,sk1)),sk3) = join(composition(X2,sFlat0),composition(X1,sk3)),
inference(orient,[status(thm)],[t7085]) ).
cnf(t968,plain,
join(one,composition(converse(sk2),sk1)) = join(one,converse(sk2)),
inference(cp,[status(thm)],[t960,t674]) ).
cnf(t90228,plain,
join(one,composition(converse(sk2),sk1)) = one,
inference(step,[status(thm)],[t968,t320]) ).
cnf(t1247,plain,
join(one,composition(converse(sk2),sk1)) = one,
inference(orient,[status(thm)],[t90228]) ).
cnf(t7439,plain,
join(composition(converse(sk2),sFlat0),composition(one,sk3)) = composition(one,sk3),
inference(cp,[status(thm)],[t7432,t1247]) ).
cnf(t90774,plain,
join(composition(one,sk3),composition(converse(sk2),sFlat0)) = composition(one,sk3),
inference(step,[status(thm)],[t7439,t102]) ).
cnf(t90775,plain,
join(sk3,composition(converse(sk2),sFlat0)) = composition(one,sk3),
inference(step,[status(thm)],[t90774,t243]) ).
cnf(t90776,plain,
join(sk3,composition(converse(sk2),sFlat0)) = sk3,
inference(step,[status(thm)],[t90775,t243]) ).
cnf(t7484,plain,
join(sk3,composition(converse(sk2),sFlat0)) = sk3,
inference(orient,[status(thm)],[t90776]) ).
cnf(t7486,plain,
join(converse(sk3),composition(converse(sFlat0),sk2)) = converse(sk3),
inference(cp,[status(thm)],[t3567,t7484]) ).
cnf(t7552,plain,
join(converse(sk3),composition(converse(sFlat0),sk2)) = converse(sk3),
inference(orient,[status(thm)],[t7486]) ).
cnf(t7554,plain,
top = join(complement(converse(composition(converse(sFlat0),sk2))),converse(converse(sk3))),
inference(cp,[status(thm)],[t1311,t7552]) ).
cnf(t90923,plain,
top = join(converse(converse(sk3)),complement(converse(composition(converse(sFlat0),sk2)))),
inference(step,[status(thm)],[t7554,t102]) ).
cnf(t90924,plain,
top = join(sk3,complement(converse(composition(converse(sFlat0),sk2)))),
inference(step,[status(thm)],[t90923,t31]) ).
cnf(t90925,plain,
top = join(sk3,complement(composition(converse(sk2),sFlat0))),
inference(step,[status(thm)],[t90924,t209]) ).
cnf(t10546,plain,
join(sk3,complement(composition(converse(sk2),sFlat0))) = top,
inference(orient,[status(thm)],[t90925]) ).
cnf(t91111,plain,
join(sk3,complement(composition(sk2,sFlat0))) = top,
inference(step,[status(thm)],[t10546,t15145]) ).
cnf(t15228,plain,
join(sk3,complement(composition(sk2,sFlat0))) = top,
inference(rw,[status(thm)],[t91111]) ).
cnf(t15743,plain,
join(sk3,complement(composition(sk2,sFlat0))) = top,
inference(orient,[status(thm)],[t15228]) ).
cnf(t15750,plain,
meet(complement(sk3),composition(sk2,sFlat0)) = complement(top),
inference(cp,[status(thm)],[t2958,t15743]) ).
cnf(t91145,plain,
meet(complement(sk3),composition(sk2,sFlat0)) = zero,
inference(step,[status(thm)],[t15750,t140]) ).
cnf(t15890,plain,
meet(complement(sk3),composition(sk2,sFlat0)) = zero,
inference(orient,[status(thm)],[t91145]) ).
cnf(t15891,plain,
composition(sk2,sFlat0) = join(meet(composition(sk2,sFlat0),sk3),zero),
inference(cp,[status(thm)],[t3308,t15890]) ).
cnf(t91149,plain,
composition(sk2,sFlat0) = meet(composition(sk2,sFlat0),sk3),
inference(step,[status(thm)],[t15891,t2824]) ).
cnf(t91150,plain,
composition(sk2,sFlat0) = meet(sk3,composition(sk2,sFlat0)),
inference(step,[status(thm)],[t91149,t159]) ).
cnf(t15946,plain,
meet(sk3,composition(sk2,sFlat0)) = composition(sk2,sFlat0),
inference(orient,[status(thm)],[t91150]) ).
cnf(t20407,plain,
meet(sFlat0,composition(sk2,meet(sk3,composition(sk2,sFlat0)))) = join(meet(sFlat1,sFlat0),meet(sFlat0,composition(sk2,composition(sk2,sFlat0)))),
inference(cp,[status(thm)],[t20386,t15946]) ).
cnf(t91827,plain,
meet(sFlat0,composition(sk2,composition(sk2,sFlat0))) = join(meet(sFlat1,sFlat0),meet(sFlat0,composition(sk2,composition(sk2,sFlat0)))),
inference(step,[status(thm)],[t20407,t15946]) ).
cnf(t91828,plain,
meet(sFlat0,composition(sk2,sFlat0)) = join(meet(sFlat1,sFlat0),meet(sFlat0,composition(sk2,composition(sk2,sFlat0)))),
inference(step,[status(thm)],[t91827,t16008]) ).
cnf(t91829,plain,
composition(sk2,sFlat0) = join(meet(sFlat1,sFlat0),meet(sFlat0,composition(sk2,composition(sk2,sFlat0)))),
inference(step,[status(thm)],[t91828,t15061]) ).
cnf(t91830,plain,
composition(sk2,sFlat0) = join(meet(sFlat0,sFlat1),meet(sFlat0,composition(sk2,composition(sk2,sFlat0)))),
inference(step,[status(thm)],[t91829,t159]) ).
cnf(t91831,plain,
composition(sk2,sFlat0) = join(sFlat2,meet(sFlat0,composition(sk2,composition(sk2,sFlat0)))),
inference(step,[status(thm)],[t91830,t99]) ).
cnf(t91832,plain,
composition(sk2,sFlat0) = join(sFlat2,meet(sFlat0,composition(sk2,sFlat0))),
inference(step,[status(thm)],[t91831,t16008]) ).
cnf(t91833,plain,
composition(sk2,sFlat0) = join(sFlat2,composition(sk2,sFlat0)),
inference(step,[status(thm)],[t91832,t15061]) ).
cnf(t29451,plain,
join(sFlat2,composition(sk2,sFlat0)) = composition(sk2,sFlat0),
inference(orient,[status(thm)],[t91833]) ).
cnf(t29454,plain,
sFlat2 = meet(sFlat2,composition(sk2,sFlat0)),
inference(cp,[status(thm)],[t11056,t29451]) ).
cnf(t29458,plain,
meet(sFlat2,composition(sk2,sFlat0)) = sFlat2,
inference(orient,[status(thm)],[t29454]) ).
cnf(t17648,plain,
composition(meet(sk1,converse(one)),meet(one,converse(sk1))) = join(composition(sk1,one),composition(meet(sk1,converse(one)),meet(one,converse(sk1)))),
inference(cp,[status(thm)],[t3626,t17630]) ).
cnf(t91287,plain,
composition(meet(sk1,one),meet(one,converse(sk1))) = join(composition(sk1,one),composition(meet(sk1,converse(one)),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t17648,t232]) ).
cnf(t2966,plain,
meet(complement(one),sk1) = complement(top),
inference(cp,[status(thm)],[t2958,t497]) ).
cnf(t90434,plain,
meet(sk1,complement(one)) = complement(top),
inference(step,[status(thm)],[t2966,t159]) ).
cnf(t90435,plain,
meet(sk1,complement(one)) = zero,
inference(step,[status(thm)],[t90434,t140]) ).
cnf(t3097,plain,
meet(sk1,complement(one)) = zero,
inference(orient,[status(thm)],[t90435]) ).
cnf(t3098,plain,
sk1 = join(zero,complement(join(complement(sk1),complement(one)))),
inference(cp,[status(thm)],[t2560,t3097]) ).
cnf(t90436,plain,
sk1 = complement(join(complement(sk1),complement(one))),
inference(step,[status(thm)],[t3098,t2660]) ).
cnf(t90437,plain,
sk1 = meet(sk1,one),
inference(step,[status(thm)],[t90436,t68]) ).
cnf(t3099,plain,
meet(sk1,one) = sk1,
inference(orient,[status(thm)],[t90437]) ).
cnf(t91288,plain,
composition(sk1,meet(one,converse(sk1))) = join(composition(sk1,one),composition(meet(sk1,converse(one)),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t91287,t3099]) ).
cnf(t996,plain,
join(one,complement(converse(sk1))) = join(one,top),
inference(cp,[status(thm)],[t983,t111]) ).
cnf(t90206,plain,
join(one,complement(converse(sk1))) = top,
inference(step,[status(thm)],[t996,t480]) ).
cnf(t1031,plain,
join(one,complement(converse(sk1))) = top,
inference(orient,[status(thm)],[t90206]) ).
cnf(t2964,plain,
meet(complement(one),converse(sk1)) = complement(top),
inference(cp,[status(thm)],[t2958,t1031]) ).
cnf(t90453,plain,
meet(converse(sk1),complement(one)) = complement(top),
inference(step,[status(thm)],[t2964,t159]) ).
cnf(t90454,plain,
meet(converse(sk1),complement(one)) = zero,
inference(step,[status(thm)],[t90453,t140]) ).
cnf(t3164,plain,
meet(converse(sk1),complement(one)) = zero,
inference(orient,[status(thm)],[t90454]) ).
cnf(t3167,plain,
converse(sk1) = join(zero,meet(converse(sk1),complement(complement(one)))),
inference(cp,[status(thm)],[t3165,t3164]) ).
cnf(t90462,plain,
converse(sk1) = meet(converse(sk1),complement(complement(one))),
inference(step,[status(thm)],[t3167,t2776]) ).
cnf(t90463,plain,
converse(sk1) = meet(converse(sk1),one),
inference(step,[status(thm)],[t90462,t2682]) ).
cnf(t90464,plain,
converse(sk1) = meet(one,converse(sk1)),
inference(step,[status(thm)],[t90463,t159]) ).
cnf(t3181,plain,
meet(one,converse(sk1)) = converse(sk1),
inference(orient,[status(thm)],[t90464]) ).
cnf(t91289,plain,
composition(sk1,converse(sk1)) = join(composition(sk1,one),composition(meet(sk1,converse(one)),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t91288,t3181]) ).
cnf(t91290,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(meet(sk1,converse(one)),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t91289,t27]) ).
cnf(t91291,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(meet(sk1,one),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t91290,t232]) ).
cnf(t91292,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(sk1,meet(one,converse(sk1)))),
inference(step,[status(thm)],[t91291,t3099]) ).
cnf(t91293,plain,
composition(sk1,converse(sk1)) = join(sk1,composition(sk1,converse(sk1))),
inference(step,[status(thm)],[t91292,t3181]) ).
cnf(t587,plain,
join(X1,converse(composition(sk1,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t249,t581]) ).
cnf(t90178,plain,
join(X1,composition(X1,converse(sk1))) = converse(converse(X1)),
inference(step,[status(thm)],[t587,t199]) ).
cnf(t90179,plain,
join(X1,composition(X1,converse(sk1))) = X1,
inference(step,[status(thm)],[t90178,t31]) ).
cnf(t792,plain,
join(X1,composition(X1,converse(sk1))) = X1,
inference(orient,[status(thm)],[t90179]) ).
cnf(t91294,plain,
composition(sk1,converse(sk1)) = sk1,
inference(step,[status(thm)],[t91293,t792]) ).
cnf(t17663,plain,
composition(sk1,converse(sk1)) = sk1,
inference(orient,[status(thm)],[t91294]) ).
cnf(t17687,plain,
composition(sk1,converse(sk1)) = converse(sk1),
inference(cp,[status(thm)],[t199,t17663]) ).
cnf(t91296,plain,
sk1 = converse(sk1),
inference(step,[status(thm)],[t17687,t17663]) ).
cnf(t17716,plain,
converse(sk1) = sk1,
inference(orient,[status(thm)],[t91296]) ).
cnf(t17721,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sk1),
inference(cp,[status(thm)],[t49,t17716]) ).
cnf(t18126,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sk1),
inference(orient,[status(thm)],[t17721]) ).
cnf(t91297,plain,
composition(sk1,sk1) = sk1,
inference(step,[status(thm)],[t17663,t17716]) ).
cnf(t17790,plain,
composition(sk1,sk1) = sk1,
inference(rw,[status(thm)],[t91297]) ).
cnf(t17807,plain,
composition(sk1,sk1) = sk1,
inference(orient,[status(thm)],[t17790]) ).
cnf(t17812,plain,
composition(sk1,composition(sk1,X1)) = composition(sk1,X1),
inference(cp,[status(thm)],[t32,t17807]) ).
cnf(t18242,plain,
composition(sk1,composition(sk1,X1)) = composition(sk1,X1),
inference(orient,[status(thm)],[t17812]) ).
cnf(t18247,plain,
composition(sk1,sk3) = composition(sk1,sFlat0),
inference(cp,[status(thm)],[t18242,t58]) ).
cnf(t91336,plain,
sFlat0 = composition(sk1,sFlat0),
inference(step,[status(thm)],[t18247,t58]) ).
cnf(t18281,plain,
composition(sk1,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t91336]) ).
cnf(t18282,plain,
composition(converse(sFlat0),sk1) = converse(sFlat0),
inference(cp,[status(thm)],[t18126,t18281]) ).
cnf(t18313,plain,
composition(converse(sFlat0),sk1) = converse(sFlat0),
inference(orient,[status(thm)],[t18282]) ).
cnf(t18318,plain,
composition(converse(sFlat0),composition(sk1,X1)) = composition(converse(sFlat0),X1),
inference(cp,[status(thm)],[t32,t18313]) ).
cnf(t18946,plain,
composition(converse(sFlat0),composition(sk1,X1)) = composition(converse(sFlat0),X1),
inference(orient,[status(thm)],[t18318]) ).
cnf(t85,plain,
meet(composition(X1,meet(X2,composition(converse(X1),one))),one) = join(meet(composition(X1,X2),one),meet(composition(X1,meet(X2,converse(X1))),one)),
inference(cp,[status(thm)],[t75,t27]) ).
cnf(t91985,plain,
meet(one,composition(X1,meet(X2,composition(converse(X1),one)))) = join(meet(composition(X1,X2),one),meet(composition(X1,meet(X2,converse(X1))),one)),
inference(step,[status(thm)],[t85,t159]) ).
cnf(t91986,plain,
meet(one,composition(X1,meet(X2,converse(X1)))) = join(meet(composition(X1,X2),one),meet(composition(X1,meet(X2,converse(X1))),one)),
inference(step,[status(thm)],[t91985,t27]) ).
cnf(t91987,plain,
meet(one,composition(X1,meet(X2,converse(X1)))) = join(meet(one,composition(X1,X2)),meet(composition(X1,meet(X2,converse(X1))),one)),
inference(step,[status(thm)],[t91986,t159]) ).
cnf(t91988,plain,
meet(one,composition(X1,meet(X2,converse(X1)))) = join(meet(one,composition(X1,X2)),meet(one,composition(X1,meet(X2,converse(X1))))),
inference(step,[status(thm)],[t91987,t159]) ).
cnf(t32207,plain,
join(meet(one,composition(X1,X2)),meet(one,composition(X1,meet(X2,converse(X1))))) = meet(one,composition(X1,meet(X2,converse(X1)))),
inference(orient,[status(thm)],[t91988]) ).
cnf(t1039,plain,
join(one,converse(join(sk2,X1))) = converse(join(one,X1)),
inference(cp,[status(thm)],[t1038,t418]) ).
cnf(t90244,plain,
join(one,converse(join(sk2,X1))) = join(one,converse(X1)),
inference(step,[status(thm)],[t1039,t265]) ).
cnf(t1375,plain,
join(one,converse(join(sk2,X1))) = join(one,converse(X1)),
inference(orient,[status(thm)],[t90244]) ).
cnf(t1378,plain,
join(one,converse(composition(sk1,sk2))) = join(one,converse(sk2)),
inference(cp,[status(thm)],[t1375,t581]) ).
cnf(t90245,plain,
join(one,converse(composition(sk1,sk2))) = one,
inference(step,[status(thm)],[t1378,t320]) ).
cnf(t1389,plain,
join(one,converse(composition(sk1,sk2))) = one,
inference(orient,[status(thm)],[t90245]) ).
cnf(t1391,plain,
top = join(complement(converse(converse(composition(sk1,sk2)))),converse(one)),
inference(cp,[status(thm)],[t1311,t1389]) ).
cnf(t90513,plain,
top = join(converse(one),complement(converse(converse(composition(sk1,sk2))))),
inference(step,[status(thm)],[t1391,t102]) ).
cnf(t90514,plain,
top = join(one,complement(converse(converse(composition(sk1,sk2))))),
inference(step,[status(thm)],[t90513,t232]) ).
cnf(t90515,plain,
top = join(one,complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t90514,t31]) ).
cnf(t4064,plain,
join(one,complement(composition(sk1,sk2))) = top,
inference(orient,[status(thm)],[t90515]) ).
cnf(t4066,plain,
meet(complement(one),composition(sk1,sk2)) = complement(top),
inference(cp,[status(thm)],[t2958,t4064]) ).
cnf(t90564,plain,
meet(complement(one),composition(sk1,sk2)) = zero,
inference(step,[status(thm)],[t4066,t140]) ).
cnf(t5497,plain,
meet(complement(one),composition(sk1,sk2)) = zero,
inference(orient,[status(thm)],[t90564]) ).
cnf(t5498,plain,
composition(sk1,sk2) = join(meet(composition(sk1,sk2),one),zero),
inference(cp,[status(thm)],[t3308,t5497]) ).
cnf(t90576,plain,
composition(sk1,sk2) = meet(composition(sk1,sk2),one),
inference(step,[status(thm)],[t5498,t2824]) ).
cnf(t90577,plain,
composition(sk1,sk2) = meet(one,composition(sk1,sk2)),
inference(step,[status(thm)],[t90576,t159]) ).
cnf(t5530,plain,
meet(one,composition(sk1,sk2)) = composition(sk1,sk2),
inference(orient,[status(thm)],[t90577]) ).
cnf(t32208,plain,
meet(one,composition(sk1,meet(sk2,converse(sk1)))) = join(composition(sk1,sk2),meet(one,composition(sk1,meet(sk2,converse(sk1))))),
inference(cp,[status(thm)],[t32207,t5530]) ).
cnf(t91989,plain,
meet(one,composition(sk1,meet(sk2,sk1))) = join(composition(sk1,sk2),meet(one,composition(sk1,meet(sk2,converse(sk1))))),
inference(step,[status(thm)],[t32208,t17716]) ).
cnf(t91990,plain,
meet(one,composition(sk1,sFlat3)) = join(composition(sk1,sk2),meet(one,composition(sk1,meet(sk2,converse(sk1))))),
inference(step,[status(thm)],[t91989,t166]) ).
cnf(t91991,plain,
meet(one,sFlat3) = join(composition(sk1,sk2),meet(one,composition(sk1,meet(sk2,converse(sk1))))),
inference(step,[status(thm)],[t91990,t23352]) ).
cnf(t91992,plain,
meet(sFlat3,one) = join(composition(sk1,sk2),meet(one,composition(sk1,meet(sk2,converse(sk1))))),
inference(step,[status(thm)],[t91991,t159]) ).
cnf(t91993,plain,
sFlat3 = join(composition(sk1,sk2),meet(one,composition(sk1,meet(sk2,converse(sk1))))),
inference(step,[status(thm)],[t91992,t3256]) ).
cnf(t91994,plain,
sFlat3 = join(composition(sk1,sk2),meet(one,composition(sk1,meet(sk2,sk1)))),
inference(step,[status(thm)],[t91993,t17716]) ).
cnf(t91995,plain,
sFlat3 = join(composition(sk1,sk2),meet(one,composition(sk1,sFlat3))),
inference(step,[status(thm)],[t91994,t166]) ).
cnf(t91996,plain,
sFlat3 = join(composition(sk1,sk2),meet(one,sFlat3)),
inference(step,[status(thm)],[t91995,t23352]) ).
cnf(t91997,plain,
sFlat3 = join(composition(sk1,sk2),meet(sFlat3,one)),
inference(step,[status(thm)],[t91996,t159]) ).
cnf(t91998,plain,
sFlat3 = join(composition(sk1,sk2),sFlat3),
inference(step,[status(thm)],[t91997,t3256]) ).
cnf(t91999,plain,
sFlat3 = join(sFlat3,composition(sk1,sk2)),
inference(step,[status(thm)],[t91998,t102]) ).
cnf(t20897,plain,
composition(join(sFlat3,X1),sk2) = join(sFlat3,composition(X1,sk2)),
inference(cp,[status(thm)],[t44,t20889]) ).
cnf(t22820,plain,
composition(join(sFlat3,X1),sk2) = join(sFlat3,composition(X1,sk2)),
inference(orient,[status(thm)],[t20897]) ).
cnf(t23432,plain,
join(sFlat3,composition(sk1,sk2)) = composition(sk1,sk2),
inference(cp,[status(thm)],[t22820,t23431]) ).
cnf(t24084,plain,
join(sFlat3,composition(sk1,sk2)) = composition(sk1,sk2),
inference(orient,[status(thm)],[t23432]) ).
cnf(t92000,plain,
sFlat3 = composition(sk1,sk2),
inference(step,[status(thm)],[t91999,t24084]) ).
cnf(t32443,plain,
composition(sk1,sk2) = sFlat3,
inference(orient,[status(thm)],[t92000]) ).
cnf(t32444,plain,
composition(converse(sFlat0),sk2) = composition(converse(sFlat0),sFlat3),
inference(cp,[status(thm)],[t18946,t32443]) ).
cnf(t20936,plain,
converse(composition(sFlat3,X1)) = composition(converse(X1),sFlat3),
inference(cp,[status(thm)],[t49,t20931]) ).
cnf(t21376,plain,
converse(composition(sFlat3,X1)) = composition(converse(X1),sFlat3),
inference(orient,[status(thm)],[t20936]) ).
cnf(t23354,plain,
composition(converse(sFlat3),sk1) = converse(sFlat3),
inference(cp,[status(thm)],[t18126,t23352]) ).
cnf(t91618,plain,
composition(sFlat3,sk1) = converse(sFlat3),
inference(step,[status(thm)],[t23354,t20931]) ).
cnf(t91619,plain,
composition(sFlat3,sk1) = sFlat3,
inference(step,[status(thm)],[t91618,t20931]) ).
cnf(t23394,plain,
composition(sFlat3,sk1) = sFlat3,
inference(orient,[status(thm)],[t91619]) ).
cnf(t23400,plain,
composition(sFlat3,composition(sk1,X1)) = composition(sFlat3,X1),
inference(cp,[status(thm)],[t32,t23394]) ).
cnf(t23904,plain,
composition(sFlat3,composition(sk1,X1)) = composition(sFlat3,X1),
inference(orient,[status(thm)],[t23400]) ).
cnf(t23915,plain,
composition(sFlat3,sk3) = composition(sFlat3,sFlat0),
inference(cp,[status(thm)],[t23904,t58]) ).
cnf(t91648,plain,
sFlat4 = composition(sFlat3,sFlat0),
inference(step,[status(thm)],[t23915,t146]) ).
cnf(t23956,plain,
composition(sFlat3,sFlat0) = sFlat4,
inference(orient,[status(thm)],[t91648]) ).
cnf(t23957,plain,
composition(converse(sFlat0),sFlat3) = converse(sFlat4),
inference(cp,[status(thm)],[t21376,t23956]) ).
cnf(t23991,plain,
composition(converse(sFlat0),sFlat3) = converse(sFlat4),
inference(orient,[status(thm)],[t23957]) ).
cnf(t92012,plain,
composition(converse(sFlat0),sk2) = converse(sFlat4),
inference(step,[status(thm)],[t32444,t23991]) ).
cnf(t32538,plain,
composition(converse(sFlat0),sk2) = converse(sFlat4),
inference(orient,[status(thm)],[t92012]) ).
cnf(t32539,plain,
composition(sk2,converse(converse(sFlat0))) = converse(converse(sFlat4)),
inference(cp,[status(thm)],[t15460,t32538]) ).
cnf(t92015,plain,
composition(sk2,sFlat0) = converse(converse(sFlat4)),
inference(step,[status(thm)],[t32539,t31]) ).
cnf(t92016,plain,
composition(sk2,sFlat0) = sFlat4,
inference(step,[status(thm)],[t92015,t31]) ).
cnf(t32598,plain,
composition(sk2,sFlat0) = sFlat4,
inference(orient,[status(thm)],[t92016]) ).
cnf(t92020,plain,
meet(sFlat2,sFlat4) = sFlat2,
inference(step,[status(thm)],[t29458,t32598]) ).
cnf(t32642,plain,
meet(sFlat2,sFlat4) = sFlat2,
inference(rw,[status(thm)],[t92020]) ).
cnf(t32694,plain,
meet(sFlat2,sFlat4) = sFlat2,
inference(orient,[status(thm)],[t32642]) ).
cnf(t94090,plain,
sFlat2 = meet(sFlat4,join(sFlat1,complement(sFlat0))),
inference(step,[status(thm)],[t94089,t32694]) ).
cnf(t94091,plain,
sFlat2 = meet(sFlat4,sFlat1),
inference(step,[status(thm)],[t94090,t89700]) ).
cnf(t94092,plain,
sFlat2 = meet(sFlat1,sFlat4),
inference(step,[status(thm)],[t94091,t159]) ).
cnf(t6655,plain,
top = join(complement(converse(meet(X1,X2))),converse(X1)),
inference(cp,[status(thm)],[t6629,t3308]) ).
cnf(t90727,plain,
top = join(converse(X1),complement(converse(meet(X1,X2)))),
inference(step,[status(thm)],[t6655,t102]) ).
cnf(t7148,plain,
join(converse(X1),complement(converse(meet(X1,X2)))) = top,
inference(orient,[status(thm)],[t90727]) ).
cnf(t3156,plain,
join(sFlat4,composition(meet(sk2,complement(sk1)),sk3)) = composition(sk2,sk3),
inference(cp,[status(thm)],[t396,t3155]) ).
cnf(t90561,plain,
join(sFlat4,composition(meet(sk2,complement(sk1)),sk3)) = sFlat1,
inference(step,[status(thm)],[t3156,t63]) ).
cnf(t5483,plain,
join(sFlat4,composition(meet(sk2,complement(sk1)),sk3)) = sFlat1,
inference(orient,[status(thm)],[t90561]) ).
cnf(t6660,plain,
top = join(complement(converse(sFlat4)),converse(sFlat1)),
inference(cp,[status(thm)],[t6629,t5483]) ).
cnf(t90694,plain,
top = join(converse(sFlat1),complement(converse(sFlat4))),
inference(step,[status(thm)],[t6660,t102]) ).
cnf(t6695,plain,
join(converse(sFlat1),complement(converse(sFlat4))) = top,
inference(orient,[status(thm)],[t90694]) ).
cnf(t6696,plain,
meet(complement(converse(sFlat1)),converse(sFlat4)) = complement(top),
inference(cp,[status(thm)],[t2958,t6695]) ).
cnf(t90704,plain,
meet(converse(sFlat4),complement(converse(sFlat1))) = complement(top),
inference(step,[status(thm)],[t6696,t159]) ).
cnf(t90705,plain,
meet(converse(sFlat4),complement(converse(sFlat1))) = zero,
inference(step,[status(thm)],[t90704,t140]) ).
cnf(t6745,plain,
meet(converse(sFlat4),complement(converse(sFlat1))) = zero,
inference(orient,[status(thm)],[t90705]) ).
cnf(t6746,plain,
converse(sFlat4) = join(zero,meet(complement(complement(converse(sFlat1))),converse(sFlat4))),
inference(cp,[status(thm)],[t3308,t6745]) ).
cnf(t90706,plain,
converse(sFlat4) = meet(complement(complement(converse(sFlat1))),converse(sFlat4)),
inference(step,[status(thm)],[t6746,t2776]) ).
cnf(t90707,plain,
converse(sFlat4) = meet(converse(sFlat4),complement(complement(converse(sFlat1)))),
inference(step,[status(thm)],[t90706,t159]) ).
cnf(t90708,plain,
converse(sFlat4) = meet(converse(sFlat4),converse(sFlat1)),
inference(step,[status(thm)],[t90707,t2682]) ).
cnf(t90709,plain,
converse(sFlat4) = meet(converse(sFlat1),converse(sFlat4)),
inference(step,[status(thm)],[t90708,t159]) ).
cnf(t6749,plain,
meet(converse(sFlat1),converse(sFlat4)) = converse(sFlat4),
inference(orient,[status(thm)],[t90709]) ).
cnf(t7174,plain,
top = join(converse(converse(sFlat1)),complement(converse(converse(sFlat4)))),
inference(cp,[status(thm)],[t7148,t6749]) ).
cnf(t90728,plain,
top = join(sFlat1,complement(converse(converse(sFlat4)))),
inference(step,[status(thm)],[t7174,t31]) ).
cnf(t90729,plain,
top = join(sFlat1,complement(sFlat4)),
inference(step,[status(thm)],[t90728,t31]) ).
cnf(t7188,plain,
join(sFlat1,complement(sFlat4)) = top,
inference(orient,[status(thm)],[t90729]) ).
cnf(t7189,plain,
meet(complement(sFlat1),sFlat4) = complement(top),
inference(cp,[status(thm)],[t2958,t7188]) ).
cnf(t90730,plain,
meet(sFlat4,complement(sFlat1)) = complement(top),
inference(step,[status(thm)],[t7189,t159]) ).
cnf(t90731,plain,
meet(sFlat4,complement(sFlat1)) = zero,
inference(step,[status(thm)],[t90730,t140]) ).
cnf(t7190,plain,
meet(sFlat4,complement(sFlat1)) = zero,
inference(orient,[status(thm)],[t90731]) ).
cnf(t7191,plain,
sFlat4 = join(zero,meet(complement(complement(sFlat1)),sFlat4)),
inference(cp,[status(thm)],[t3308,t7190]) ).
cnf(t90732,plain,
sFlat4 = meet(complement(complement(sFlat1)),sFlat4),
inference(step,[status(thm)],[t7191,t2776]) ).
cnf(t90733,plain,
sFlat4 = meet(sFlat4,complement(complement(sFlat1))),
inference(step,[status(thm)],[t90732,t159]) ).
cnf(t90734,plain,
sFlat4 = meet(sFlat4,sFlat1),
inference(step,[status(thm)],[t90733,t2682]) ).
cnf(t90735,plain,
sFlat4 = meet(sFlat1,sFlat4),
inference(step,[status(thm)],[t90734,t159]) ).
cnf(t7194,plain,
meet(sFlat1,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t90735]) ).
cnf(t94093,plain,
sFlat2 = sFlat4,
inference(step,[status(thm)],[t94092,t7194]) ).
cnf(t89718,plain,
sFlat4 = sFlat2,
inference(orient,[status(thm)],[t94093]) ).
cnf(t94096,plain,
composition(sFlat3,sk3) = sFlat2,
inference(step,[status(thm)],[t146,t89718]) ).
cnf(t89721,plain,
composition(sFlat3,sk3) = sFlat2,
inference(orient,[status(thm)],[t94096]) ).
cnf(goal_0,negated_conjecture,
tuple(join(meet(composition(sk1,sk3),composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)),join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
tuple(join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[goal_0,t102]) ).
cnf(g0_1,plain,
tuple(join(composition(meet(sk2,sk1),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_0,t159]) ).
cnf(g0_2,plain,
tuple(join(composition(sFlat3,sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_1,t166]) ).
cnf(g0_3,plain,
tuple(join(sFlat2,meet(composition(sk1,sk3),composition(sk2,sk3))),join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_2,t89721]) ).
cnf(g0_4,plain,
tuple(join(sFlat2,meet(composition(sk2,sk3),composition(sk1,sk3))),join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_3,t159]) ).
cnf(g0_5,plain,
tuple(join(sFlat2,meet(sFlat1,composition(sk1,sk3))),join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_4,t63]) ).
cnf(g0_6,plain,
tuple(join(sFlat2,meet(sFlat1,sFlat0)),join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_5,t58]) ).
cnf(g0_7,plain,
tuple(join(sFlat2,meet(sFlat0,sFlat1)),join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_6,t159]) ).
cnf(g0_8,plain,
tuple(join(sFlat2,sFlat2),join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_7,t99]) ).
cnf(g0_9,plain,
tuple(sFlat2,join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_8,t2729]) ).
cnf(g0_10,plain,
tuple(sFlat2,join(composition(meet(sk2,sk1),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_9,t159]) ).
cnf(g0_11,plain,
tuple(sFlat2,join(composition(sFlat3,sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_10,t166]) ).
cnf(g0_12,plain,
tuple(sFlat2,join(sFlat2,meet(composition(sk1,sk3),composition(sk2,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_11,t89721]) ).
cnf(g0_13,plain,
tuple(sFlat2,join(sFlat2,meet(composition(sk2,sk3),composition(sk1,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_12,t159]) ).
cnf(g0_14,plain,
tuple(sFlat2,join(sFlat2,meet(sFlat1,composition(sk1,sk3)))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_13,t63]) ).
cnf(g0_15,plain,
tuple(sFlat2,join(sFlat2,meet(sFlat1,sFlat0))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_14,t58]) ).
cnf(g0_16,plain,
tuple(sFlat2,join(sFlat2,meet(sFlat0,sFlat1))) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_15,t159]) ).
cnf(g0_17,plain,
tuple(sFlat2,join(sFlat2,sFlat2)) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_16,t99]) ).
cnf(g0_18,plain,
tuple(sFlat2,sFlat2) != tuple(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_17,t2729]) ).
cnf(g0_19,plain,
tuple(sFlat2,sFlat2) != tuple(composition(meet(sk2,sk1),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_18,t159]) ).
cnf(g0_20,plain,
tuple(sFlat2,sFlat2) != tuple(composition(sFlat3,sk3),meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_19,t166]) ).
cnf(g0_21,plain,
tuple(sFlat2,sFlat2) != tuple(sFlat2,meet(composition(sk1,sk3),composition(sk2,sk3))),
inference(rw,[status(thm)],[g0_20,t89721]) ).
cnf(g0_22,plain,
tuple(sFlat2,sFlat2) != tuple(sFlat2,meet(composition(sk2,sk3),composition(sk1,sk3))),
inference(rw,[status(thm)],[g0_21,t159]) ).
cnf(g0_23,plain,
tuple(sFlat2,sFlat2) != tuple(sFlat2,meet(sFlat1,composition(sk1,sk3))),
inference(rw,[status(thm)],[g0_22,t63]) ).
cnf(g0_24,plain,
tuple(sFlat2,sFlat2) != tuple(sFlat2,meet(sFlat1,sFlat0)),
inference(rw,[status(thm)],[g0_23,t58]) ).
cnf(g0_25,plain,
tuple(sFlat2,sFlat2) != tuple(sFlat2,meet(sFlat0,sFlat1)),
inference(rw,[status(thm)],[g0_24,t159]) ).
cnf(g0_26,plain,
tuple(sFlat2,sFlat2) != tuple(sFlat2,sFlat2),
inference(rw,[status(thm)],[g0_25,t99]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_26]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL029-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.14/0.41 % Computer : n019.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Thu Sep 24 07:23:49 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 234.10/30.15 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 234.10/30.15 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------