%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL045-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:36:11 PM UTC 2026
% Result : Unsatisfiable 162.18s 21.27s
% Output : CNFRefutation 162.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 107
% Number of leaves : 18
% Syntax : Number of clauses : 401 ( 401 unt; 0 nHn; 140 RR)
% Number of literals : 401 ( 400 equ; 11 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 : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 398 ( 51 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t44,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t13,axiom,
sFlat0 = converse(sk1),
introduced(definition) ).
cnf(t74,plain,
converse(sk1) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sFlat1 = composition(sk1,converse(sk1)),
introduced(definition) ).
cnf(t62,plain,
composition(sk1,converse(sk1)) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t163433,plain,
composition(sk1,sFlat0) = sFlat1,
inference(step,[status(thm)],[t62,t74]) ).
cnf(t81,plain,
composition(sk1,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t163433]) ).
cnf(t91,plain,
composition(sk1,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t81]) ).
cnf(t92,plain,
composition(sk1,composition(sFlat0,X1)) = composition(sFlat1,X1),
inference(cp,[status(thm)],[t44,t91]) ).
cnf(t255,plain,
composition(sk1,composition(sFlat0,X1)) = composition(sFlat1,X1),
inference(orient,[status(thm)],[t92]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t55,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t75,plain,
sk1 = converse(sFlat0),
inference(cp,[status(thm)],[t21,t74]) ).
cnf(t85,plain,
converse(sFlat0) = sk1,
inference(orient,[status(thm)],[t75]) ).
cnf(t87,plain,
converse(composition(sFlat0,X1)) = composition(converse(X1),sk1),
inference(cp,[status(thm)],[t55,t85]) ).
cnf(t167,plain,
converse(composition(sFlat0,X1)) = composition(converse(X1),sk1),
inference(orient,[status(thm)],[t87]) ).
cnf(t77,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sFlat0),
inference(cp,[status(thm)],[t55,t74]) ).
cnf(t118,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sFlat0),
inference(orient,[status(thm)],[t77]) ).
cnf(t15,axiom,
sFlat2 = composition(composition(sk1,converse(sk1)),sk1),
introduced(definition) ).
cnf(t163432,plain,
sFlat2 = composition(sk1,composition(converse(sk1),sk1)),
inference(step,[status(thm)],[t15,t44]) ).
cnf(t50,plain,
composition(sk1,composition(converse(sk1),sk1)) = sFlat2,
inference(orient,[status(thm)],[t163432]) ).
cnf(t163434,plain,
composition(sk1,composition(sFlat0,sk1)) = sFlat2,
inference(step,[status(thm)],[t50,t74]) ).
cnf(t82,plain,
composition(sk1,composition(sFlat0,sk1)) = sFlat2,
inference(rw,[status(thm)],[t163434]) ).
cnf(t105,plain,
composition(sk1,composition(sFlat0,sk1)) = sFlat2,
inference(orient,[status(thm)],[t82]) ).
cnf(t120,plain,
composition(converse(composition(sFlat0,sk1)),sFlat0) = converse(sFlat2),
inference(cp,[status(thm)],[t118,t105]) ).
cnf(t76,plain,
converse(composition(X1,sk1)) = composition(sFlat0,converse(X1)),
inference(cp,[status(thm)],[t55,t74]) ).
cnf(t110,plain,
converse(composition(X1,sk1)) = composition(sFlat0,converse(X1)),
inference(orient,[status(thm)],[t76]) ).
cnf(t163439,plain,
composition(composition(sFlat0,converse(sFlat0)),sFlat0) = converse(sFlat2),
inference(step,[status(thm)],[t120,t110]) ).
cnf(t163440,plain,
composition(sFlat0,composition(converse(sFlat0),sFlat0)) = converse(sFlat2),
inference(step,[status(thm)],[t163439,t44]) ).
cnf(t163441,plain,
composition(sFlat0,composition(sk1,sFlat0)) = converse(sFlat2),
inference(step,[status(thm)],[t163440,t85]) ).
cnf(t163442,plain,
composition(sFlat0,sFlat1) = converse(sFlat2),
inference(step,[status(thm)],[t163441,t91]) ).
cnf(t134,plain,
composition(sFlat0,sFlat1) = converse(sFlat2),
inference(orient,[status(thm)],[t163442]) ).
cnf(t168,plain,
composition(converse(sFlat1),sk1) = converse(converse(sFlat2)),
inference(cp,[status(thm)],[t167,t134]) ).
cnf(t119,plain,
composition(converse(sFlat0),sFlat0) = converse(sFlat1),
inference(cp,[status(thm)],[t118,t91]) ).
cnf(t163437,plain,
composition(sk1,sFlat0) = converse(sFlat1),
inference(step,[status(thm)],[t119,t85]) ).
cnf(t163438,plain,
sFlat1 = converse(sFlat1),
inference(step,[status(thm)],[t163437,t91]) ).
cnf(t128,plain,
converse(sFlat1) = sFlat1,
inference(orient,[status(thm)],[t163438]) ).
cnf(t163445,plain,
composition(sFlat1,sk1) = converse(converse(sFlat2)),
inference(step,[status(thm)],[t168,t128]) ).
cnf(t163446,plain,
composition(sFlat1,sk1) = sFlat2,
inference(step,[status(thm)],[t163445,t21]) ).
cnf(t175,plain,
composition(sFlat1,sk1) = sFlat2,
inference(orient,[status(thm)],[t163446]) ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t16,axiom,
sFlat3 = join(sk1,composition(composition(sk1,converse(sk1)),sk1)),
introduced(definition) ).
cnf(t42,plain,
join(sk1,composition(composition(sk1,converse(sk1)),sk1)) = sFlat3,
inference(orient,[status(thm)],[t16]) ).
cnf(t163431,plain,
join(sk1,composition(sk1,composition(converse(sk1),sk1))) = sFlat3,
inference(step,[status(thm)],[t42,t44]) ).
cnf(t49,plain,
join(sk1,composition(sk1,composition(converse(sk1),sk1))) = sFlat3,
inference(rw,[status(thm)],[t163431]) ).
cnf(t163742,plain,
join(sk1,composition(sk1,composition(sFlat0,sk1))) = sFlat3,
inference(step,[status(thm)],[t49,t74]) ).
cnf(t163743,plain,
join(sk1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t163742,t105]) ).
cnf(t163744,plain,
join(sFlat2,sk1) = sFlat3,
inference(step,[status(thm)],[t163743,t22]) ).
cnf(t5305,plain,
join(sFlat2,sk1) = sFlat3,
inference(orient,[status(thm)],[t163744]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t177,plain,
composition(join(sFlat1,X1),sk1) = join(sFlat2,composition(X1,sk1)),
inference(cp,[status(thm)],[t30,t175]) ).
cnf(t1354,plain,
composition(join(sFlat1,X1),sk1) = join(sFlat2,composition(X1,sk1)),
inference(orient,[status(thm)],[t177]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t163430,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t22]) ).
cnf(t33,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t163430]) ).
cnf(t57,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t55,t21]) ).
cnf(t385,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t57]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t386,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t385,t20]) ).
cnf(t163460,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t386,t21]) ).
cnf(t406,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t163460]) ).
cnf(t407,plain,
one = converse(one),
inference(cp,[status(thm)],[t406,t20]) ).
cnf(t413,plain,
converse(one) = one,
inference(orient,[status(thm)],[t407]) ).
cnf(t163461,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t406,t413]) ).
cnf(t423,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t163461]) ).
cnf(t424,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t423]) ).
cnf(t427,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t33,t424]) ).
cnf(t163463,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t427,t413]) ).
cnf(t163464,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t163463,t424]) ).
cnf(t457,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t163464]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t23,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t17]) ).
cnf(t163456,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t23,t22]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t67,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t163457,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t163456,t67]) ).
cnf(t163458,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t163457,t22]) ).
cnf(t281,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t163458]) ).
cnf(t468,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t281,t457]) ).
cnf(t163468,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t468,t22]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t83,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t163469,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t163468,t83]) ).
cnf(t163470,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t163469,t22]) ).
cnf(t474,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t163470]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t68,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t67,t27]) ).
cnf(t163435,plain,
zero = complement(top),
inference(step,[status(thm)],[t68,t83]) ).
cnf(t96,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t163435]) ).
cnf(t461,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t457,t96]) ).
cnf(t163465,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t461,t96]) ).
cnf(t163466,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t163465,t96]) ).
cnf(t469,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t163466]) ).
cnf(t470,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t24,t469]) ).
cnf(t499,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t470]) ).
cnf(t501,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t499,t474]) ).
cnf(t163471,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t501,t474]) ).
cnf(t504,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t163471]) ).
cnf(t163474,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t474,t504]) ).
cnf(t514,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t163474]) ).
cnf(t536,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t514]) ).
cnf(t539,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t457,t536]) ).
cnf(t163482,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t539,t536]) ).
cnf(t163483,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t163482,t536]) ).
cnf(t551,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t163483]) ).
cnf(t553,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t24,t551]) ).
cnf(t643,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t553]) ).
cnf(t647,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t643,t281]) ).
cnf(t163508,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t647,t281]) ).
cnf(t163509,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t163508,t22]) ).
cnf(t774,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t163509]) ).
cnf(t1366,plain,
join(sFlat2,composition(meet(sFlat1,X1),sk1)) = composition(sFlat1,sk1),
inference(cp,[status(thm)],[t1354,t774]) ).
cnf(t163592,plain,
join(sFlat2,composition(meet(sFlat1,X1),sk1)) = sFlat2,
inference(step,[status(thm)],[t1366,t175]) ).
cnf(t1925,plain,
join(sFlat2,composition(meet(sFlat1,X1),sk1)) = sFlat2,
inference(orient,[status(thm)],[t163592]) ).
cnf(t34,plain,
complement(X1) = join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))),
inference(cp,[status(thm)],[t33,t21]) ).
cnf(t3679,plain,
join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))) = complement(X1),
inference(orient,[status(thm)],[t34]) ).
cnf(t3685,plain,
complement(top) = join(zero,composition(X1,complement(composition(converse(X1),top)))),
inference(cp,[status(thm)],[t3679,t96]) ).
cnf(t163653,plain,
zero = join(zero,composition(X1,complement(composition(converse(X1),top)))),
inference(step,[status(thm)],[t3685,t96]) ).
cnf(t163654,plain,
zero = composition(X1,complement(composition(converse(X1),top))),
inference(step,[status(thm)],[t163653,t504]) ).
cnf(t3732,plain,
composition(X1,complement(composition(converse(X1),top))) = zero,
inference(orient,[status(thm)],[t163654]) ).
cnf(t3778,plain,
composition(converse(complement(composition(converse(converse(X1)),top))),X1) = converse(zero),
inference(cp,[status(thm)],[t385,t3732]) ).
cnf(t163712,plain,
composition(converse(complement(composition(X1,top))),X1) = converse(zero),
inference(step,[status(thm)],[t3778,t21]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t37,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t40,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t37,t21]) ).
cnf(t336,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t40]) ).
cnf(t511,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t336,t504]) ).
cnf(t163488,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t511,t21]) ).
cnf(t564,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t163488]) ).
cnf(t506,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t504,t22]) ).
cnf(t526,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t506]) ).
cnf(t566,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t564,t526]) ).
cnf(t568,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t566]) ).
cnf(t163713,plain,
composition(converse(complement(composition(X1,top))),X1) = zero,
inference(step,[status(thm)],[t163712,t568]) ).
cnf(t3978,plain,
composition(converse(complement(composition(X1,top))),X1) = zero,
inference(orient,[status(thm)],[t163713]) ).
cnf(t135,plain,
composition(sFlat0,composition(sFlat1,X1)) = composition(converse(sFlat2),X1),
inference(cp,[status(thm)],[t44,t134]) ).
cnf(t941,plain,
composition(sFlat0,composition(sFlat1,X1)) = composition(converse(sFlat2),X1),
inference(orient,[status(thm)],[t135]) ).
cnf(t3768,plain,
composition(sFlat1,complement(composition(converse(sFlat0),top))) = composition(sk1,zero),
inference(cp,[status(thm)],[t255,t3732]) ).
cnf(t163682,plain,
composition(sFlat1,complement(composition(sk1,top))) = composition(sk1,zero),
inference(step,[status(thm)],[t3768,t85]) ).
cnf(t39,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t37,t21]) ).
cnf(t315,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t39]) ).
cnf(t645,plain,
join(X1,complement(X1)) = join(X1,top),
inference(cp,[status(thm)],[t643,t27]) ).
cnf(t163491,plain,
top = join(X1,top),
inference(step,[status(thm)],[t645,t27]) ).
cnf(t655,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t163491]) ).
cnf(t662,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t315,t655]) ).
cnf(t753,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t662]) ).
cnf(t656,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t655,t22]) ).
cnf(t664,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t656]) ).
cnf(t754,plain,
converse(top) = top,
inference(cp,[status(thm)],[t753,t664]) ).
cnf(t760,plain,
converse(top) = top,
inference(orient,[status(thm)],[t754]) ).
cnf(t3736,plain,
zero = composition(top,complement(composition(top,top))),
inference(cp,[status(thm)],[t3732,t760]) ).
cnf(t3779,plain,
composition(top,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t3736]) ).
cnf(t3782,plain,
composition(join(top,X1),complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(cp,[status(thm)],[t30,t3779]) ).
cnf(t163655,plain,
composition(top,complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t3782,t664]) ).
cnf(t163656,plain,
zero = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t163655,t3779]) ).
cnf(t163657,plain,
zero = composition(X1,complement(composition(top,top))),
inference(step,[status(thm)],[t163656,t504]) ).
cnf(t3815,plain,
composition(X1,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t163657]) ).
cnf(t3817,plain,
zero = composition(X1,composition(X2,complement(composition(top,top)))),
inference(cp,[status(thm)],[t3815,t44]) ).
cnf(t163658,plain,
zero = composition(X1,zero),
inference(step,[status(thm)],[t3817,t3815]) ).
cnf(t3831,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t163658]) ).
cnf(t163683,plain,
composition(sFlat1,complement(composition(sk1,top))) = zero,
inference(step,[status(thm)],[t163682,t3831]) ).
cnf(t3883,plain,
composition(sFlat1,complement(composition(sk1,top))) = zero,
inference(orient,[status(thm)],[t163683]) ).
cnf(t3884,plain,
composition(converse(sFlat2),complement(composition(sk1,top))) = composition(sFlat0,zero),
inference(cp,[status(thm)],[t941,t3883]) ).
cnf(t163714,plain,
composition(converse(sFlat2),complement(composition(sk1,top))) = zero,
inference(step,[status(thm)],[t3884,t3831]) ).
cnf(t3990,plain,
composition(converse(sFlat2),complement(composition(sk1,top))) = zero,
inference(orient,[status(thm)],[t163714]) ).
cnf(t3997,plain,
complement(complement(composition(sk1,top))) = join(complement(complement(composition(sk1,top))),composition(converse(converse(sFlat2)),complement(zero))),
inference(cp,[status(thm)],[t33,t3990]) ).
cnf(t163715,plain,
composition(sk1,top) = join(complement(complement(composition(sk1,top))),composition(converse(converse(sFlat2)),complement(zero))),
inference(step,[status(thm)],[t3997,t536]) ).
cnf(t163716,plain,
composition(sk1,top) = join(composition(sk1,top),composition(converse(converse(sFlat2)),complement(zero))),
inference(step,[status(thm)],[t163715,t536]) ).
cnf(t163717,plain,
composition(sk1,top) = join(composition(sk1,top),composition(sFlat2,complement(zero))),
inference(step,[status(thm)],[t163716,t21]) ).
cnf(t505,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t504,t27]) ).
cnf(t516,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t505]) ).
cnf(t163718,plain,
composition(sk1,top) = join(composition(sk1,top),composition(sFlat2,top)),
inference(step,[status(thm)],[t163717,t516]) ).
cnf(t163719,plain,
composition(sk1,top) = composition(join(sk1,sFlat2),top),
inference(step,[status(thm)],[t163718,t30]) ).
cnf(t163720,plain,
composition(sk1,top) = composition(join(sFlat2,sk1),top),
inference(step,[status(thm)],[t163719,t22]) ).
cnf(t3999,plain,
composition(join(sFlat2,sk1),top) = composition(sk1,top),
inference(orient,[status(thm)],[t163720]) ).
cnf(t163745,plain,
composition(sFlat3,top) = composition(sk1,top),
inference(step,[status(thm)],[t3999,t5305]) ).
cnf(t5334,plain,
composition(sFlat3,top) = composition(sk1,top),
inference(rw,[status(thm)],[t163745]) ).
cnf(t5407,plain,
composition(sk1,top) = composition(sFlat3,top),
inference(orient,[status(thm)],[t5334]) ).
cnf(t5425,plain,
zero = composition(converse(complement(composition(sFlat3,top))),sk1),
inference(cp,[status(thm)],[t3978,t5407]) ).
cnf(t7099,plain,
composition(converse(complement(composition(sFlat3,top))),sk1) = zero,
inference(orient,[status(thm)],[t5425]) ).
cnf(t69,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t67,t22]) ).
cnf(t163451,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t69,t67]) ).
cnf(t247,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t163451]) ).
cnf(t776,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t774,t247]) ).
cnf(t786,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t776]) ).
cnf(t792,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t24,t786]) ).
cnf(t2801,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t792]) ).
cnf(t537,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t536,t67]) ).
cnf(t959,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t537]) ).
cnf(t962,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t959,t536]) ).
cnf(t1015,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t962]) ).
cnf(t1021,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t536,t1015]) ).
cnf(t1115,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t1021]) ).
cnf(t163530,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t281,t1115]) ).
cnf(t1140,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t163530]) ).
cnf(t14956,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t1140]) ).
cnf(t15064,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t2801,t14956]) ).
cnf(t15261,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t15064]) ).
cnf(t15299,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t15261,t247]) ).
cnf(t15760,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t15299]) ).
cnf(t15782,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t15760,t536]) ).
cnf(t18763,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t15782]) ).
cnf(t961,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t959,t536]) ).
cnf(t999,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t961]) ).
cnf(t1006,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t536,t999]) ).
cnf(t1031,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t1006]) ).
cnf(t1040,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t1031,t536]) ).
cnf(t1141,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t1040]) ).
cnf(t15298,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t15261,t1141]) ).
cnf(t16047,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t15298]) ).
cnf(t16252,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t1115,t16047]) ).
cnf(t164099,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t16252,t536]) ).
cnf(t164100,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t164099,t67]) ).
cnf(t17295,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t164100]) ).
cnf(t17328,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t17295,t22]) ).
cnf(t17514,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t17328]) ).
cnf(t319,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t315,t27]) ).
cnf(t163531,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t319,t760]) ).
cnf(t1155,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t163531]) ).
cnf(t17539,plain,
meet(X1,converse(complement(converse(complement(X1))))) = meet(X1,top),
inference(cp,[status(thm)],[t17514,t1155]) ).
cnf(t99,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t67,t96]) ).
cnf(t271,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t99]) ).
cnf(t478,plain,
meet(top,complement(X1)) = complement(X1),
inference(cp,[status(thm)],[t271,t474]) ).
cnf(t479,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t478]) ).
cnf(t538,plain,
complement(complement(X1)) = meet(top,X1),
inference(cp,[status(thm)],[t479,t536]) ).
cnf(t163481,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t538,t536]) ).
cnf(t549,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t163481]) ).
cnf(t550,plain,
X1 = meet(X1,top),
inference(cp,[status(thm)],[t549,t247]) ).
cnf(t554,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t550]) ).
cnf(t164109,plain,
meet(X1,converse(complement(converse(complement(X1))))) = X1,
inference(step,[status(thm)],[t17539,t554]) ).
cnf(t17638,plain,
meet(X1,converse(complement(converse(complement(X1))))) = X1,
inference(orient,[status(thm)],[t164109]) ).
cnf(t17699,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = complement(complement(X1)),
inference(cp,[status(thm)],[t999,t17638]) ).
cnf(t164110,plain,
join(X1,complement(converse(complement(converse(X1))))) = complement(complement(X1)),
inference(step,[status(thm)],[t17699,t536]) ).
cnf(t164111,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t164110,t536]) ).
cnf(t17705,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t164111]) ).
cnf(t17788,plain,
join(X1,converse(complement(converse(complement(converse(converse(X1))))))) = converse(converse(X1)),
inference(cp,[status(thm)],[t315,t17705]) ).
cnf(t164112,plain,
join(X1,converse(complement(converse(complement(X1))))) = converse(converse(X1)),
inference(step,[status(thm)],[t17788,t21]) ).
cnf(t164113,plain,
join(X1,converse(complement(converse(complement(X1))))) = X1,
inference(step,[status(thm)],[t164112,t21]) ).
cnf(t17797,plain,
join(X1,converse(complement(converse(complement(X1))))) = X1,
inference(orient,[status(thm)],[t164113]) ).
cnf(t17827,plain,
meet(X1,converse(complement(converse(complement(complement(X1)))))) = meet(X1,complement(X1)),
inference(cp,[status(thm)],[t17514,t17797]) ).
cnf(t164114,plain,
meet(X1,converse(complement(converse(X1)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t17827,t536]) ).
cnf(t164115,plain,
meet(X1,converse(complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t164114,t83]) ).
cnf(t17854,plain,
meet(X1,converse(complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t164115]) ).
cnf(t17895,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(cp,[status(thm)],[t17854,t21]) ).
cnf(t17902,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t17895]) ).
cnf(t18829,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t18763,t17902]) ).
cnf(t164209,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t18829,t22]) ).
cnf(t164210,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t164209,t526]) ).
cnf(t21210,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t164210]) ).
cnf(t21221,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t21210,t536]) ).
cnf(t17743,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t17705,t21]) ).
cnf(t19886,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t17743]) ).
cnf(t164211,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t21221,t19886]) ).
cnf(t21287,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t164211]) ).
cnf(t21298,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t21287,t536]) ).
cnf(t21351,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t21298]) ).
cnf(t770,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t55,t760]) ).
cnf(t808,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t770]) ).
cnf(t21375,plain,
converse(complement(composition(top,X1))) = complement(composition(converse(X1),top)),
inference(cp,[status(thm)],[t21351,t808]) ).
cnf(t22302,plain,
complement(composition(converse(X1),top)) = converse(complement(composition(top,X1))),
inference(orient,[status(thm)],[t21375]) ).
cnf(t22360,plain,
converse(complement(composition(top,sFlat0))) = complement(composition(sk1,top)),
inference(cp,[status(thm)],[t22302,t85]) ).
cnf(t164282,plain,
converse(complement(composition(top,sFlat0))) = complement(composition(sFlat3,top)),
inference(step,[status(thm)],[t22360,t5407]) ).
cnf(t22478,plain,
converse(complement(composition(top,sFlat0))) = complement(composition(sFlat3,top)),
inference(orient,[status(thm)],[t164282]) ).
cnf(t22479,plain,
complement(composition(top,sFlat0)) = converse(complement(composition(sFlat3,top))),
inference(cp,[status(thm)],[t21,t22478]) ).
cnf(t22628,plain,
converse(complement(composition(sFlat3,top))) = complement(composition(top,sFlat0)),
inference(orient,[status(thm)],[t22479]) ).
cnf(t164286,plain,
composition(complement(composition(top,sFlat0)),sk1) = zero,
inference(step,[status(thm)],[t7099,t22628]) ).
cnf(t22664,plain,
composition(complement(composition(top,sFlat0)),sk1) = zero,
inference(rw,[status(thm)],[t164286]) ).
cnf(t22711,plain,
composition(complement(composition(top,sFlat0)),sk1) = zero,
inference(orient,[status(thm)],[t22664]) ).
cnf(t22713,plain,
composition(join(complement(composition(top,sFlat0)),X1),sk1) = join(zero,composition(X1,sk1)),
inference(cp,[status(thm)],[t30,t22711]) ).
cnf(t166674,plain,
composition(join(complement(composition(top,sFlat0)),X1),sk1) = composition(X1,sk1),
inference(step,[status(thm)],[t22713,t504]) ).
cnf(t130738,plain,
composition(join(complement(composition(top,sFlat0)),X1),sk1) = composition(X1,sk1),
inference(orient,[status(thm)],[t166674]) ).
cnf(t26,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t24,t22]) ).
cnf(t163538,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t26,t24]) ).
cnf(t1241,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t163538]) ).
cnf(t1251,plain,
join(X1,join(X2,meet(X3,X1))) = join(X2,X1),
inference(cp,[status(thm)],[t1241,t786]) ).
cnf(t3213,plain,
join(X1,join(X2,meet(X3,X1))) = join(X2,X1),
inference(orient,[status(thm)],[t1251]) ).
cnf(t15062,plain,
join(meet(X1,X2),complement(X2)) = join(complement(X2),X1),
inference(cp,[status(thm)],[t3213,t14956]) ).
cnf(t164053,plain,
join(complement(X2),meet(X1,X2)) = join(complement(X2),X1),
inference(step,[status(thm)],[t15062,t22]) ).
cnf(t15838,plain,
join(complement(X1),meet(X2,X1)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t164053]) ).
cnf(t130753,plain,
composition(meet(X1,composition(top,sFlat0)),sk1) = composition(join(complement(composition(top,sFlat0)),X1),sk1),
inference(cp,[status(thm)],[t130738,t15838]) ).
cnf(t166675,plain,
composition(meet(X1,composition(top,sFlat0)),sk1) = composition(X1,sk1),
inference(step,[status(thm)],[t130753,t130738]) ).
cnf(t130829,plain,
composition(meet(X1,composition(top,sFlat0)),sk1) = composition(X1,sk1),
inference(orient,[status(thm)],[t166675]) ).
cnf(t1250,plain,
join(X1,join(X2,meet(X1,X3))) = join(X2,X1),
inference(cp,[status(thm)],[t1241,t774]) ).
cnf(t3091,plain,
join(X1,join(X2,meet(X1,X3))) = join(X2,X1),
inference(orient,[status(thm)],[t1250]) ).
cnf(t17533,plain,
meet(X1,join(X2,meet(complement(X1),X3))) = meet(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t17514,t3091]) ).
cnf(t166325,plain,
meet(X1,join(X2,meet(complement(X1),X3))) = meet(X1,X2),
inference(step,[status(thm)],[t17533,t17295]) ).
cnf(t118899,plain,
meet(X1,join(X2,meet(complement(X1),X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t166325]) ).
cnf(t15350,plain,
meet(X1,complement(meet(X2,complement(complement(X1))))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t1115,t15261]) ).
cnf(t164119,plain,
meet(X1,join(complement(X2),complement(X1))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t15350,t1015]) ).
cnf(t164120,plain,
meet(X1,complement(meet(X2,X1))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t164119,t959]) ).
cnf(t164121,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t164120,t1115]) ).
cnf(t18086,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t164121]) ).
cnf(t25,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t24,t22]) ).
cnf(t678,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t25]) ).
cnf(t686,plain,
join(complement(X1),join(X2,X1)) = join(X2,top),
inference(cp,[status(thm)],[t678,t27]) ).
cnf(t163510,plain,
join(X1,join(complement(X1),X2)) = join(X2,top),
inference(step,[status(thm)],[t686,t678]) ).
cnf(t163511,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t163510,t655]) ).
cnf(t833,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t163511]) ).
cnf(t835,plain,
top = join(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t833,t22]) ).
cnf(t925,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t835]) ).
cnf(t967,plain,
top = join(X1,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t925,t959]) ).
cnf(t972,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t967]) ).
cnf(t1033,plain,
meet(complement(X1),meet(X2,X1)) = complement(top),
inference(cp,[status(thm)],[t1031,t972]) ).
cnf(t163526,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(step,[status(thm)],[t1033,t96]) ).
cnf(t1053,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t163526]) ).
cnf(t846,plain,
X1 = join(meet(X1,join(complement(complement(X1)),X2)),complement(top)),
inference(cp,[status(thm)],[t281,t833]) ).
cnf(t163512,plain,
X1 = join(complement(top),meet(X1,join(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t846,t22]) ).
cnf(t163513,plain,
X1 = join(zero,meet(X1,join(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t163512,t96]) ).
cnf(t163514,plain,
X1 = meet(X1,join(complement(complement(X1)),X2)),
inference(step,[status(thm)],[t163513,t504]) ).
cnf(t163515,plain,
X1 = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t163514,t536]) ).
cnf(t848,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t163515]) ).
cnf(t853,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t848,t22]) ).
cnf(t857,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t853]) ).
cnf(t1063,plain,
zero = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t1053,t857]) ).
cnf(t163529,plain,
zero = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t1063,t247]) ).
cnf(t1090,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t163529]) ).
cnf(t35,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t33,t20]) ).
cnf(t4696,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t35]) ).
cnf(t4737,plain,
zero = meet(composition(converse(X1),complement(X1)),complement(complement(one))),
inference(cp,[status(thm)],[t1090,t4696]) ).
cnf(t163737,plain,
zero = meet(complement(complement(one)),composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t4737,t247]) ).
cnf(t163738,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t163737,t536]) ).
cnf(t4742,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t163738]) ).
cnf(t4764,plain,
zero = meet(one,composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t4742,t21]) ).
cnf(t4782,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t4764]) ).
cnf(t78,plain,
converse(join(sk1,X1)) = join(sFlat0,converse(X1)),
inference(cp,[status(thm)],[t37,t74]) ).
cnf(t144,plain,
converse(join(sk1,X1)) = join(sFlat0,converse(X1)),
inference(orient,[status(thm)],[t78]) ).
cnf(t145,plain,
join(sFlat0,converse(complement(sk1))) = converse(top),
inference(cp,[status(thm)],[t144,t27]) ).
cnf(t241,plain,
join(sFlat0,converse(complement(sk1))) = converse(top),
inference(orient,[status(thm)],[t145]) ).
cnf(t163500,plain,
join(sFlat0,converse(complement(sk1))) = top,
inference(step,[status(thm)],[t241,t760]) ).
cnf(t761,plain,
join(sFlat0,converse(complement(sk1))) = top,
inference(orient,[status(thm)],[t163500]) ).
cnf(t16194,plain,
join(converse(complement(sk1)),complement(sFlat0)) = join(converse(complement(sk1)),complement(top)),
inference(cp,[status(thm)],[t16047,t761]) ).
cnf(t164092,plain,
join(complement(sFlat0),converse(complement(sk1))) = join(converse(complement(sk1)),complement(top)),
inference(step,[status(thm)],[t16194,t22]) ).
cnf(t88,plain,
converse(join(sFlat0,X1)) = join(sk1,converse(X1)),
inference(cp,[status(thm)],[t37,t85]) ).
cnf(t185,plain,
converse(join(sFlat0,X1)) = join(sk1,converse(X1)),
inference(orient,[status(thm)],[t88]) ).
cnf(t187,plain,
join(sk1,converse(complement(sFlat0))) = converse(top),
inference(cp,[status(thm)],[t185,t27]) ).
cnf(t243,plain,
join(sk1,converse(complement(sFlat0))) = converse(top),
inference(orient,[status(thm)],[t187]) ).
cnf(t163502,plain,
join(sk1,converse(complement(sFlat0))) = top,
inference(step,[status(thm)],[t243,t760]) ).
cnf(t763,plain,
join(sk1,converse(complement(sFlat0))) = top,
inference(orient,[status(thm)],[t163502]) ).
cnf(t16176,plain,
join(converse(complement(sFlat0)),complement(sk1)) = join(converse(complement(sFlat0)),complement(top)),
inference(cp,[status(thm)],[t16047,t763]) ).
cnf(t164081,plain,
join(complement(sk1),converse(complement(sFlat0))) = join(converse(complement(sFlat0)),complement(top)),
inference(step,[status(thm)],[t16176,t22]) ).
cnf(t164082,plain,
join(complement(sk1),converse(complement(sFlat0))) = join(complement(top),converse(complement(sFlat0))),
inference(step,[status(thm)],[t164081,t22]) ).
cnf(t164083,plain,
join(complement(sk1),converse(complement(sFlat0))) = join(zero,converse(complement(sFlat0))),
inference(step,[status(thm)],[t164082,t96]) ).
cnf(t164084,plain,
join(complement(sk1),converse(complement(sFlat0))) = converse(complement(sFlat0)),
inference(step,[status(thm)],[t164083,t504]) ).
cnf(t16733,plain,
join(complement(sk1),converse(complement(sFlat0))) = converse(complement(sFlat0)),
inference(orient,[status(thm)],[t164084]) ).
cnf(t16750,plain,
join(converse(complement(sk1)),complement(sFlat0)) = converse(converse(complement(sFlat0))),
inference(cp,[status(thm)],[t336,t16733]) ).
cnf(t164090,plain,
join(complement(sFlat0),converse(complement(sk1))) = converse(converse(complement(sFlat0))),
inference(step,[status(thm)],[t16750,t22]) ).
cnf(t164091,plain,
join(complement(sFlat0),converse(complement(sk1))) = complement(sFlat0),
inference(step,[status(thm)],[t164090,t21]) ).
cnf(t16834,plain,
join(complement(sFlat0),converse(complement(sk1))) = complement(sFlat0),
inference(orient,[status(thm)],[t164091]) ).
cnf(t164093,plain,
complement(sFlat0) = join(converse(complement(sk1)),complement(top)),
inference(step,[status(thm)],[t164092,t16834]) ).
cnf(t164094,plain,
complement(sFlat0) = join(complement(top),converse(complement(sk1))),
inference(step,[status(thm)],[t164093,t22]) ).
cnf(t164095,plain,
complement(sFlat0) = join(zero,converse(complement(sk1))),
inference(step,[status(thm)],[t164094,t96]) ).
cnf(t164096,plain,
complement(sFlat0) = converse(complement(sk1)),
inference(step,[status(thm)],[t164095,t504]) ).
cnf(t16854,plain,
converse(complement(sk1)) = complement(sFlat0),
inference(orient,[status(thm)],[t164096]) ).
cnf(t16877,plain,
zero = meet(one,composition(complement(sk1),complement(complement(sFlat0)))),
inference(cp,[status(thm)],[t4782,t16854]) ).
cnf(t164098,plain,
zero = meet(one,composition(complement(sk1),sFlat0)),
inference(step,[status(thm)],[t16877,t536]) ).
cnf(t16926,plain,
meet(one,composition(complement(sk1),sFlat0)) = zero,
inference(orient,[status(thm)],[t164098]) ).
cnf(t18174,plain,
meet(composition(complement(sk1),sFlat0),complement(one)) = meet(composition(complement(sk1),sFlat0),complement(zero)),
inference(cp,[status(thm)],[t18086,t16926]) ).
cnf(t165444,plain,
meet(complement(one),composition(complement(sk1),sFlat0)) = meet(composition(complement(sk1),sFlat0),complement(zero)),
inference(step,[status(thm)],[t18174,t247]) ).
cnf(t165445,plain,
meet(complement(one),composition(complement(sk1),sFlat0)) = meet(complement(zero),composition(complement(sk1),sFlat0)),
inference(step,[status(thm)],[t165444,t247]) ).
cnf(t165446,plain,
meet(complement(one),composition(complement(sk1),sFlat0)) = meet(top,composition(complement(sk1),sFlat0)),
inference(step,[status(thm)],[t165445,t516]) ).
cnf(t165447,plain,
meet(complement(one),composition(complement(sk1),sFlat0)) = composition(complement(sk1),sFlat0),
inference(step,[status(thm)],[t165446,t549]) ).
cnf(t77360,plain,
meet(complement(one),composition(complement(sk1),sFlat0)) = composition(complement(sk1),sFlat0),
inference(orient,[status(thm)],[t165447]) ).
cnf(t118933,plain,
meet(one,X1) = meet(one,join(X1,composition(complement(sk1),sFlat0))),
inference(cp,[status(thm)],[t118899,t77360]) ).
cnf(t162867,plain,
meet(one,join(X1,composition(complement(sk1),sFlat0))) = meet(one,X1),
inference(orient,[status(thm)],[t118933]) ).
cnf(t93,plain,
composition(join(sk1,X1),sFlat0) = join(sFlat1,composition(X1,sFlat0)),
inference(cp,[status(thm)],[t30,t91]) ).
cnf(t1184,plain,
composition(join(sk1,X1),sFlat0) = join(sFlat1,composition(X1,sFlat0)),
inference(orient,[status(thm)],[t93]) ).
cnf(t1195,plain,
join(sFlat1,composition(complement(sk1),sFlat0)) = composition(top,sFlat0),
inference(cp,[status(thm)],[t1184,t27]) ).
cnf(t1436,plain,
join(sFlat1,composition(complement(sk1),sFlat0)) = composition(top,sFlat0),
inference(orient,[status(thm)],[t1195]) ).
cnf(t162870,plain,
meet(one,sFlat1) = meet(one,composition(top,sFlat0)),
inference(cp,[status(thm)],[t162867,t1436]) ).
cnf(t167039,plain,
meet(sFlat1,one) = meet(one,composition(top,sFlat0)),
inference(step,[status(thm)],[t162870,t247]) ).
cnf(t162905,plain,
meet(one,composition(top,sFlat0)) = meet(sFlat1,one),
inference(orient,[status(thm)],[t167039]) ).
cnf(t162916,plain,
composition(one,sk1) = composition(meet(sFlat1,one),sk1),
inference(cp,[status(thm)],[t130829,t162905]) ).
cnf(t167040,plain,
sk1 = composition(meet(sFlat1,one),sk1),
inference(step,[status(thm)],[t162916,t424]) ).
cnf(t162942,plain,
composition(meet(sFlat1,one),sk1) = sk1,
inference(orient,[status(thm)],[t167040]) ).
cnf(t162967,plain,
sFlat2 = join(sFlat2,sk1),
inference(cp,[status(thm)],[t1925,t162942]) ).
cnf(t167041,plain,
sFlat2 = sFlat3,
inference(step,[status(thm)],[t162967,t5305]) ).
cnf(t162976,plain,
sFlat3 = sFlat2,
inference(orient,[status(thm)],[t167041]) ).
cnf(t167042,plain,
join(sFlat2,sk1) = sFlat2,
inference(step,[status(thm)],[t5305,t162976]) ).
cnf(t162977,plain,
join(sFlat2,sk1) = sFlat2,
inference(orient,[status(thm)],[t167042]) ).
cnf(goal_0,negated_conjecture,
join(sk1,composition(composition(sk1,converse(sk1)),sk1)) != composition(composition(sk1,converse(sk1)),sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(sk1,composition(sk1,composition(converse(sk1),sk1))) != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[goal_0,t44]) ).
cnf(g0_1,plain,
join(sk1,composition(sk1,composition(sFlat0,sk1))) != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[g0_0,t74]) ).
cnf(g0_2,plain,
join(sk1,composition(sFlat1,sk1)) != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[g0_1,t255]) ).
cnf(g0_3,plain,
join(sk1,sFlat2) != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[g0_2,t175]) ).
cnf(g0_4,plain,
join(sFlat2,sk1) != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[g0_3,t22]) ).
cnf(g0_5,plain,
sFlat2 != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[g0_4,t162977]) ).
cnf(g0_6,plain,
sFlat2 != composition(sk1,composition(converse(sk1),sk1)),
inference(rw,[status(thm)],[g0_5,t44]) ).
cnf(g0_7,plain,
sFlat2 != composition(sk1,composition(sFlat0,sk1)),
inference(rw,[status(thm)],[g0_6,t74]) ).
cnf(g0_8,plain,
sFlat2 != composition(sFlat1,sk1),
inference(rw,[status(thm)],[g0_7,t255]) ).
cnf(g0_9,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_8,t175]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL045-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.21/0.45 % Computer : n011.cluster.edu
% 0.21/0.45 % Model : x86_64 x86_64
% 0.21/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.45 % Memory : 8046.5625MB
% 0.21/0.45 % OS : Linux 6.8.0-71-generic
% 0.21/0.45 % CPULimit : 300
% 0.21/0.45 % WCLimit : 300
% 0.21/0.45 % DateTime : Thu Sep 24 07:36:42 UTC 2026
% 0.21/0.45 % CPUTime :
% 0.21/0.45 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 162.18/21.27 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 162.18/21.27 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------