%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL036-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : 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:35:58 PM UTC 2026
% Result : Unsatisfiable 78.41s 11.83s
% Output : CNFRefutation 78.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 20
% Syntax : Number of clauses : 282 ( 282 unt; 0 nHn; 103 RR)
% Number of literals : 282 ( 281 equ; 16 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 : 16 ( 16 usr; 11 con; 0-2 aty)
% Number of variables : 307 ( 15 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t50,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t43,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t51,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t50,t43]) ).
cnf(t14971,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t51]) ).
cnf(t15073,plain,
composition(join(converse(X1),converse(X2)),converse(X3)) = join(converse(composition(X3,X1)),converse(composition(X3,X2))),
inference(cp,[status(thm)],[t14971,t43]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t99,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t20275,plain,
composition(converse(join(X1,X2)),converse(X3)) = join(converse(composition(X3,X1)),converse(composition(X3,X2))),
inference(step,[status(thm)],[t15073,t99]) ).
cnf(t20276,plain,
converse(composition(X3,join(X1,X2))) = join(converse(composition(X3,X1)),converse(composition(X3,X2))),
inference(step,[status(thm)],[t20275,t43]) ).
cnf(t20277,plain,
converse(composition(X3,join(X1,X2))) = converse(join(composition(X3,X1),composition(X3,X2))),
inference(step,[status(thm)],[t20276,t99]) ).
cnf(t16121,plain,
converse(join(composition(X1,X2),composition(X1,X3))) = converse(composition(X1,join(X2,X3))),
inference(orient,[status(thm)],[t20277]) ).
cnf(t16329,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(converse(composition(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t24,t16121]) ).
cnf(t20279,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t16329,t24]) ).
cnf(t16968,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t20279]) ).
cnf(t17,axiom,
sFlat0 = converse(sk1),
introduced(definition) ).
cnf(t102,plain,
converse(sk1) = sFlat0,
inference(orient,[status(thm)],[t17]) ).
cnf(t6,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t64,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t113,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t114,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t64,t113]) ).
cnf(t19220,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t114,t64]) ).
cnf(t165,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t19220]) ).
cnf(t18,axiom,
sFlat1 = meet(sk2,converse(sk1)),
introduced(definition) ).
cnf(t97,plain,
meet(sk2,converse(sk1)) = sFlat1,
inference(orient,[status(thm)],[t18]) ).
cnf(t19210,plain,
meet(sk2,sFlat0) = sFlat1,
inference(step,[status(thm)],[t97,t102]) ).
cnf(t112,plain,
meet(sk2,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t19210]) ).
cnf(t163,plain,
meet(sk2,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t112]) ).
cnf(t169,plain,
meet(sk2,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t163]) ).
cnf(t19221,plain,
meet(sFlat0,sk2) = sFlat1,
inference(step,[status(thm)],[t169,t165]) ).
cnf(t173,plain,
meet(sFlat0,sk2) = sFlat1,
inference(orient,[status(thm)],[t19221]) ).
cnf(t45,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t43,t24]) ).
cnf(t306,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t45]) ).
cnf(t100,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t99,t24]) ).
cnf(t350,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t100]) ).
cnf(t367,plain,
composition(converse(X1),join(converse(X2),X3)) = converse(composition(join(X2,converse(X3)),X1)),
inference(cp,[status(thm)],[t306,t350]) ).
cnf(t6182,plain,
converse(composition(join(X1,converse(X2)),X3)) = composition(converse(X3),join(converse(X1),X2)),
inference(orient,[status(thm)],[t367]) ).
cnf(t19,axiom,
sFlat2 = composition(meet(sk2,converse(sk1)),sk3),
introduced(definition) ).
cnf(t40,plain,
composition(meet(sk2,converse(sk1)),sk3) = sFlat2,
inference(orient,[status(thm)],[t19]) ).
cnf(t19209,plain,
composition(sFlat1,sk3) = sFlat2,
inference(step,[status(thm)],[t40,t97]) ).
cnf(t98,plain,
composition(sFlat1,sk3) = sFlat2,
inference(rw,[status(thm)],[t19209]) ).
cnf(t155,plain,
composition(sFlat1,sk3) = sFlat2,
inference(orient,[status(thm)],[t98]) ).
cnf(t15045,plain,
composition(join(converse(sk3),X1),converse(sFlat1)) = join(converse(sFlat2),composition(X1,converse(sFlat1))),
inference(cp,[status(thm)],[t14971,t155]) ).
cnf(t15692,plain,
composition(join(converse(sk3),X1),converse(sFlat1)) = join(converse(sFlat2),composition(X1,converse(sFlat1))),
inference(orient,[status(thm)],[t15045]) ).
cnf(t15750,plain,
composition(converse(converse(sFlat1)),join(converse(converse(sk3)),X1)) = converse(join(converse(sFlat2),composition(converse(X1),converse(sFlat1)))),
inference(cp,[status(thm)],[t6182,t15692]) ).
cnf(t20235,plain,
composition(sFlat1,join(converse(converse(sk3)),X1)) = converse(join(converse(sFlat2),composition(converse(X1),converse(sFlat1)))),
inference(step,[status(thm)],[t15750,t24]) ).
cnf(t20236,plain,
composition(sFlat1,join(sk3,X1)) = converse(join(converse(sFlat2),composition(converse(X1),converse(sFlat1)))),
inference(step,[status(thm)],[t20235,t24]) ).
cnf(t20237,plain,
composition(sFlat1,join(sk3,X1)) = join(sFlat2,converse(composition(converse(X1),converse(sFlat1)))),
inference(step,[status(thm)],[t20236,t350]) ).
cnf(t20238,plain,
composition(sFlat1,join(sk3,X1)) = join(sFlat2,composition(converse(converse(sFlat1)),X1)),
inference(step,[status(thm)],[t20237,t306]) ).
cnf(t20239,plain,
composition(sFlat1,join(sk3,X1)) = join(sFlat2,composition(sFlat1,X1)),
inference(step,[status(thm)],[t20238,t24]) ).
cnf(t15776,plain,
composition(sFlat1,join(sk3,X1)) = join(sFlat2,composition(sFlat1,X1)),
inference(orient,[status(thm)],[t20239]) ).
cnf(t20,axiom,
sFlat3 = meet(sk1,sk3),
introduced(definition) ).
cnf(t95,plain,
meet(sk1,sk3) = sFlat3,
inference(orient,[status(thm)],[t20]) ).
cnf(t170,plain,
meet(sk1,sk3) = sFlat3,
inference(rw,[status(thm)],[t95]) ).
cnf(t19222,plain,
meet(sk3,sk1) = sFlat3,
inference(step,[status(thm)],[t170,t165]) ).
cnf(t174,plain,
meet(sk3,sk1) = sFlat3,
inference(orient,[status(thm)],[t19222]) ).
cnf(t21,axiom,
sFlat4 = composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
introduced(definition) ).
cnf(t37,plain,
composition(meet(sk2,converse(sk1)),meet(sk1,sk3)) = sFlat4,
inference(orient,[status(thm)],[t21]) ).
cnf(t19208,plain,
composition(meet(sk2,converse(sk1)),sFlat3) = sFlat4,
inference(step,[status(thm)],[t37,t95]) ).
cnf(t96,plain,
composition(meet(sk2,converse(sk1)),sFlat3) = sFlat4,
inference(rw,[status(thm)],[t19208]) ).
cnf(t19245,plain,
composition(meet(sk2,sFlat0),sFlat3) = sFlat4,
inference(step,[status(thm)],[t96,t102]) ).
cnf(t19246,plain,
composition(meet(sFlat0,sk2),sFlat3) = sFlat4,
inference(step,[status(thm)],[t19245,t165]) ).
cnf(t19247,plain,
composition(sFlat1,sFlat3) = sFlat4,
inference(step,[status(thm)],[t19246,t173]) ).
cnf(t522,plain,
composition(sFlat1,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t19247]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19215,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t113]) ).
cnf(t130,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t19215]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t59,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t135,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t130,t59]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t123,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t127,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t64,t123]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t68,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t19216,plain,
zero = complement(top),
inference(step,[status(thm)],[t127,t68]) ).
cnf(t149,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t19216]) ).
cnf(t19257,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t135,t149]) ).
cnf(t19258,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t19257,t149]) ).
cnf(t19259,plain,
zero = join(zero,composition(sFlat0,complement(sk1))),
inference(step,[status(thm)],[t19258,t102]) ).
cnf(t683,plain,
join(zero,composition(sFlat0,complement(sk1))) = zero,
inference(orient,[status(thm)],[t19259]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t26,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)],[t25,t25]) ).
cnf(t19233,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)],[t26,t113]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t115,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t19234,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)],[t19233,t115]) ).
cnf(t19235,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t19234,t64]) ).
cnf(t372,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t19235]) ).
cnf(t152,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t64,t149]) ).
cnf(t468,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t152]) ).
cnf(t19207,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t25,t64]) ).
cnf(t67,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t19207]) ).
cnf(t2175,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t67]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t307,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t306,t23]) ).
cnf(t19230,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t307,t24]) ).
cnf(t323,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t19230]) ).
cnf(t9,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t29,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t28,t23]) ).
cnf(t276,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t29]) ).
cnf(t325,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t323,t276]) ).
cnf(t19232,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t325,t323]) ).
cnf(t344,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t19232]) ).
cnf(t347,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t130,t344]) ).
cnf(t324,plain,
one = converse(one),
inference(cp,[status(thm)],[t323,t23]) ).
cnf(t333,plain,
converse(one) = one,
inference(orient,[status(thm)],[t324]) ).
cnf(t19240,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t347,t333]) ).
cnf(t19241,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t19240,t344]) ).
cnf(t493,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t19241]) ).
cnf(t2192,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t2175,t493]) ).
cnf(t19420,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t2192,t113]) ).
cnf(t19421,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t19420,t68]) ).
cnf(t19422,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t19421,t113]) ).
cnf(t2233,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t19422]) ).
cnf(t2241,plain,
meet(top,complement(X1)) = complement(X1),
inference(cp,[status(thm)],[t468,t2233]) ).
cnf(t2405,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t2241]) ).
cnf(t2413,plain,
join(complement(top),complement(complement(X1))) = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(cp,[status(thm)],[t372,t2405]) ).
cnf(t19423,plain,
join(zero,complement(complement(X1))) = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t2413,t149]) ).
cnf(t19424,plain,
X1 = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t19423,t2233]) ).
cnf(t19425,plain,
X1 = join(zero,complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t19424,t149]) ).
cnf(t19426,plain,
X1 = join(zero,complement(join(zero,join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t19425,t149]) ).
cnf(t19427,plain,
X1 = join(zero,complement(join(zero,complement(X1)))),
inference(step,[status(thm)],[t19426,t493]) ).
cnf(t19428,plain,
X1 = join(zero,meet(top,X1)),
inference(step,[status(thm)],[t19427,t468]) ).
cnf(t2414,plain,
join(zero,meet(top,X1)) = X1,
inference(orient,[status(thm)],[t19428]) ).
cnf(t2415,plain,
complement(X1) = join(zero,complement(X1)),
inference(cp,[status(thm)],[t2414,t2405]) ).
cnf(t2421,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t2415]) ).
cnf(t502,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t64,t493]) ).
cnf(t507,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t502]) ).
cnf(t2426,plain,
complement(complement(X1)) = join(zero,meet(X1,X1)),
inference(cp,[status(thm)],[t2421,t507]) ).
cnf(t2178,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t2175,t68]) ).
cnf(t19419,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t2178,t64]) ).
cnf(t2225,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t19419]) ).
cnf(t19438,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t2426,t2225]) ).
cnf(t2454,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t19438]) ).
cnf(t2458,plain,
complement(complement(X1)) = join(zero,X1),
inference(cp,[status(thm)],[t2421,t2454]) ).
cnf(t19451,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t2458,t2454]) ).
cnf(t2530,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t19451]) ).
cnf(t19453,plain,
composition(sFlat0,complement(sk1)) = zero,
inference(step,[status(thm)],[t683,t2530]) ).
cnf(t2553,plain,
composition(sFlat0,complement(sk1)) = zero,
inference(rw,[status(thm)],[t19453]) ).
cnf(t2738,plain,
composition(sFlat0,complement(sk1)) = zero,
inference(orient,[status(thm)],[t2553]) ).
cnf(t2740,plain,
composition(join(sFlat0,X1),complement(sk1)) = join(zero,composition(X1,complement(sk1))),
inference(cp,[status(thm)],[t50,t2738]) ).
cnf(t19658,plain,
composition(join(sFlat0,X1),complement(sk1)) = composition(X1,complement(sk1)),
inference(step,[status(thm)],[t2740,t2530]) ).
cnf(t7338,plain,
composition(join(sFlat0,X1),complement(sk1)) = composition(X1,complement(sk1)),
inference(orient,[status(thm)],[t19658]) ).
cnf(t2462,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t493,t2454]) ).
cnf(t19441,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t2462,t2454]) ).
cnf(t19442,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t19441,t2454]) ).
cnf(t2481,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t19442]) ).
cnf(t122,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t115,t113]) ).
cnf(t19237,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t122,t115]) ).
cnf(t443,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t19237]) ).
cnf(t2483,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t2481,t443]) ).
cnf(t19489,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t2483,t115]) ).
cnf(t19490,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t19489,t2481]) ).
cnf(t2800,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t19490]) ).
cnf(t2184,plain,
sFlat0 = join(sFlat1,complement(join(complement(sFlat0),sk2))),
inference(cp,[status(thm)],[t2175,t173]) ).
cnf(t2465,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t64,t2454]) ).
cnf(t2632,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t2465]) ).
cnf(t19488,plain,
sFlat0 = join(sFlat1,meet(sFlat0,complement(sk2))),
inference(step,[status(thm)],[t2184,t2632]) ).
cnf(t2795,plain,
join(sFlat1,meet(sFlat0,complement(sk2))) = sFlat0,
inference(orient,[status(thm)],[t19488]) ).
cnf(t2801,plain,
join(sFlat1,meet(sFlat0,complement(sk2))) = join(sFlat1,sFlat0),
inference(cp,[status(thm)],[t2800,t2795]) ).
cnf(t19491,plain,
sFlat0 = join(sFlat1,sFlat0),
inference(step,[status(thm)],[t2801,t2795]) ).
cnf(t19492,plain,
sFlat0 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t19491,t113]) ).
cnf(t2807,plain,
join(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t19492]) ).
cnf(t7341,plain,
composition(sFlat1,complement(sk1)) = composition(sFlat0,complement(sk1)),
inference(cp,[status(thm)],[t7338,t2807]) ).
cnf(t19661,plain,
composition(sFlat1,complement(sk1)) = zero,
inference(step,[status(thm)],[t7341,t2738]) ).
cnf(t7400,plain,
composition(sFlat1,complement(sk1)) = zero,
inference(orient,[status(thm)],[t19661]) ).
cnf(t17175,plain,
composition(sFlat1,join(X1,complement(sk1))) = join(composition(sFlat1,X1),zero),
inference(cp,[status(thm)],[t16968,t7400]) ).
cnf(t2533,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t2530,t113]) ).
cnf(t2564,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t2533]) ).
cnf(t20336,plain,
composition(sFlat1,join(X1,complement(sk1))) = composition(sFlat1,X1),
inference(step,[status(thm)],[t17175,t2564]) ).
cnf(t19154,plain,
composition(sFlat1,join(X1,complement(sk1))) = composition(sFlat1,X1),
inference(orient,[status(thm)],[t20336]) ).
cnf(t2657,plain,
join(complement(X1),X2) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t2454,t2632]) ).
cnf(t2775,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t2657]) ).
cnf(t2185,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t2175,t64]) ).
cnf(t19517,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t2185,t113]) ).
cnf(t3060,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t19517]) ).
cnf(t126,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t115,t123]) ).
cnf(t530,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t126]) ).
cnf(t536,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t530,t113]) ).
cnf(t610,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t536]) ).
cnf(t2456,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t2454,t64]) ).
cnf(t2582,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t2456]) ).
cnf(t2594,plain,
join(top,complement(X1)) = join(X2,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t610,t2582]) ).
cnf(t534,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t530,t493]) ).
cnf(t19249,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t534,t123]) ).
cnf(t551,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t19249]) ).
cnf(t19498,plain,
top = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t2594,t551]) ).
cnf(t2821,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t19498]) ).
cnf(t2832,plain,
meet(X1,complement(complement(meet(X2,complement(X1))))) = complement(top),
inference(cp,[status(thm)],[t2632,t2821]) ).
cnf(t19533,plain,
meet(X1,meet(X2,complement(X1))) = complement(top),
inference(step,[status(thm)],[t2832,t2454]) ).
cnf(t19534,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t19533,t149]) ).
cnf(t3148,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t19534]) ).
cnf(t3155,plain,
X1 = join(zero,meet(X1,complement(meet(X2,complement(X1))))),
inference(cp,[status(thm)],[t3060,t3148]) ).
cnf(t19584,plain,
X1 = meet(X1,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t3155,t2530]) ).
cnf(t19585,plain,
X1 = meet(X1,join(complement(X2),X1)),
inference(step,[status(thm)],[t19584,t2775]) ).
cnf(t6466,plain,
meet(X1,join(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t19585]) ).
cnf(t6468,plain,
complement(X1) = meet(complement(X1),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t6466,t2582]) ).
cnf(t2653,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t2632,t2454]) ).
cnf(t2770,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t2653]) ).
cnf(t19969,plain,
complement(X1) = complement(join(X1,meet(X2,X1))),
inference(step,[status(thm)],[t6468,t2770]) ).
cnf(t12589,plain,
complement(join(X1,meet(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t19969]) ).
cnf(t3074,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t3060,t165]) ).
cnf(t5251,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t3074]) ).
cnf(t125,plain,
top = join(join(complement(X1),complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t123,t64]) ).
cnf(t19560,plain,
top = join(complement(X1),join(complement(X2),meet(X1,X2))),
inference(step,[status(thm)],[t125,t115]) ).
cnf(t5288,plain,
join(complement(X1),join(complement(X2),meet(X1,X2))) = top,
inference(orient,[status(thm)],[t19560]) ).
cnf(t5300,plain,
meet(X1,complement(join(complement(X2),meet(X1,X2)))) = complement(top),
inference(cp,[status(thm)],[t2632,t5288]) ).
cnf(t66,plain,
meet(X1,join(complement(X2),complement(X3))) = complement(join(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t64,t64]) ).
cnf(t1315,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,join(complement(X2),complement(X3))),
inference(orient,[status(thm)],[t66]) ).
cnf(t19458,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,complement(meet(X2,X3))),
inference(step,[status(thm)],[t1315,t2582]) ).
cnf(t2585,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,complement(meet(X2,X3))),
inference(orient,[status(thm)],[t19458]) ).
cnf(t19561,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = complement(top),
inference(step,[status(thm)],[t5300,t2585]) ).
cnf(t19562,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = zero,
inference(step,[status(thm)],[t19561,t149]) ).
cnf(t5303,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t19562]) ).
cnf(t5308,plain,
zero = meet(sk3,meet(sk1,complement(sFlat3))),
inference(cp,[status(thm)],[t5303,t174]) ).
cnf(t5317,plain,
meet(sk3,meet(sk1,complement(sFlat3))) = zero,
inference(orient,[status(thm)],[t5308]) ).
cnf(t5318,plain,
sk3 = join(zero,meet(complement(meet(sk1,complement(sFlat3))),sk3)),
inference(cp,[status(thm)],[t5251,t5317]) ).
cnf(t19563,plain,
sk3 = meet(complement(meet(sk1,complement(sFlat3))),sk3),
inference(step,[status(thm)],[t5318,t2530]) ).
cnf(t19564,plain,
sk3 = meet(sk3,complement(meet(sk1,complement(sFlat3)))),
inference(step,[status(thm)],[t19563,t165]) ).
cnf(t19565,plain,
sk3 = meet(sk3,join(complement(sk1),sFlat3)),
inference(step,[status(thm)],[t19564,t2775]) ).
cnf(t19566,plain,
sk3 = meet(sk3,join(sFlat3,complement(sk1))),
inference(step,[status(thm)],[t19565,t113]) ).
cnf(t5323,plain,
meet(sk3,join(sFlat3,complement(sk1))) = sk3,
inference(orient,[status(thm)],[t19566]) ).
cnf(t12618,plain,
complement(join(sFlat3,complement(sk1))) = complement(join(join(sFlat3,complement(sk1)),sk3)),
inference(cp,[status(thm)],[t12589,t5323]) ).
cnf(t2464,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t64,t2454]) ).
cnf(t2609,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t2464]) ).
cnf(t20045,plain,
meet(complement(sFlat3),sk1) = complement(join(join(sFlat3,complement(sk1)),sk3)),
inference(step,[status(thm)],[t12618,t2609]) ).
cnf(t20046,plain,
meet(sk1,complement(sFlat3)) = complement(join(join(sFlat3,complement(sk1)),sk3)),
inference(step,[status(thm)],[t20045,t165]) ).
cnf(t20047,plain,
meet(sk1,complement(sFlat3)) = complement(join(sFlat3,join(complement(sk1),sk3))),
inference(step,[status(thm)],[t20046,t115]) ).
cnf(t2650,plain,
meet(X1,complement(join(X2,X3))) = complement(join(X2,join(complement(X1),X3))),
inference(cp,[status(thm)],[t2632,t443]) ).
cnf(t12296,plain,
complement(join(X1,join(complement(X2),X3))) = meet(X2,complement(join(X1,X3))),
inference(orient,[status(thm)],[t2650]) ).
cnf(t20048,plain,
meet(sk1,complement(sFlat3)) = meet(sk1,complement(join(sFlat3,sk3))),
inference(step,[status(thm)],[t20047,t12296]) ).
cnf(t2183,plain,
sk3 = join(sFlat3,complement(join(complement(sk3),sk1))),
inference(cp,[status(thm)],[t2175,t174]) ).
cnf(t19487,plain,
sk3 = join(sFlat3,meet(sk3,complement(sk1))),
inference(step,[status(thm)],[t2183,t2632]) ).
cnf(t2792,plain,
join(sFlat3,meet(sk3,complement(sk1))) = sk3,
inference(orient,[status(thm)],[t19487]) ).
cnf(t2802,plain,
join(sFlat3,meet(sk3,complement(sk1))) = join(sFlat3,sk3),
inference(cp,[status(thm)],[t2800,t2792]) ).
cnf(t19493,plain,
sk3 = join(sFlat3,sk3),
inference(step,[status(thm)],[t2802,t2792]) ).
cnf(t2813,plain,
join(sFlat3,sk3) = sk3,
inference(orient,[status(thm)],[t19493]) ).
cnf(t20049,plain,
meet(sk1,complement(sFlat3)) = meet(sk1,complement(sk3)),
inference(step,[status(thm)],[t20048,t2813]) ).
cnf(t13551,plain,
meet(sk1,complement(sk3)) = meet(sk1,complement(sFlat3)),
inference(orient,[status(thm)],[t20049]) ).
cnf(t13557,plain,
join(complement(sk1),sk3) = complement(meet(sk1,complement(sFlat3))),
inference(cp,[status(thm)],[t2775,t13551]) ).
cnf(t20111,plain,
join(sk3,complement(sk1)) = complement(meet(sk1,complement(sFlat3))),
inference(step,[status(thm)],[t13557,t113]) ).
cnf(t20112,plain,
join(sk3,complement(sk1)) = join(complement(sk1),sFlat3),
inference(step,[status(thm)],[t20111,t2775]) ).
cnf(t20113,plain,
join(sk3,complement(sk1)) = join(sFlat3,complement(sk1)),
inference(step,[status(thm)],[t20112,t113]) ).
cnf(t14447,plain,
join(sk3,complement(sk1)) = join(sFlat3,complement(sk1)),
inference(orient,[status(thm)],[t20113]) ).
cnf(t19155,plain,
composition(sFlat1,sk3) = composition(sFlat1,join(sFlat3,complement(sk1))),
inference(cp,[status(thm)],[t19154,t14447]) ).
cnf(t20337,plain,
sFlat2 = composition(sFlat1,join(sFlat3,complement(sk1))),
inference(step,[status(thm)],[t19155,t155]) ).
cnf(t16204,plain,
converse(composition(sFlat1,join(sFlat3,X1))) = converse(join(sFlat4,composition(sFlat1,X1))),
inference(cp,[status(thm)],[t16121,t522]) ).
cnf(t16710,plain,
converse(composition(sFlat1,join(sFlat3,X1))) = converse(join(sFlat4,composition(sFlat1,X1))),
inference(orient,[status(thm)],[t16204]) ).
cnf(t16750,plain,
composition(sFlat1,join(sFlat3,X1)) = converse(converse(join(sFlat4,composition(sFlat1,X1)))),
inference(cp,[status(thm)],[t24,t16710]) ).
cnf(t20278,plain,
composition(sFlat1,join(sFlat3,X1)) = join(sFlat4,composition(sFlat1,X1)),
inference(step,[status(thm)],[t16750,t24]) ).
cnf(t16852,plain,
composition(sFlat1,join(sFlat3,X1)) = join(sFlat4,composition(sFlat1,X1)),
inference(orient,[status(thm)],[t20278]) ).
cnf(t20338,plain,
sFlat2 = join(sFlat4,composition(sFlat1,complement(sk1))),
inference(step,[status(thm)],[t20337,t16852]) ).
cnf(t20339,plain,
sFlat2 = join(sFlat4,zero),
inference(step,[status(thm)],[t20338,t7400]) ).
cnf(t20340,plain,
sFlat2 = sFlat4,
inference(step,[status(thm)],[t20339,t2564]) ).
cnf(t19186,plain,
sFlat4 = sFlat2,
inference(orient,[status(thm)],[t20340]) ).
cnf(t20341,plain,
composition(sFlat1,sFlat3) = sFlat2,
inference(step,[status(thm)],[t522,t19186]) ).
cnf(t19187,plain,
composition(sFlat1,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t20341]) ).
cnf(goal_0,negated_conjecture,
join(composition(meet(sk2,converse(sk1)),sk3),composition(meet(sk2,converse(sk1)),meet(sk1,sk3))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
composition(meet(sk2,converse(sk1)),join(sk3,meet(sk1,sk3))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[goal_0,t16968]) ).
cnf(g0_1,plain,
composition(meet(sk2,sFlat0),join(sk3,meet(sk1,sk3))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_0,t102]) ).
cnf(g0_2,plain,
composition(meet(sFlat0,sk2),join(sk3,meet(sk1,sk3))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_1,t165]) ).
cnf(g0_3,plain,
composition(sFlat1,join(sk3,meet(sk1,sk3))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_2,t173]) ).
cnf(g0_4,plain,
join(sFlat2,composition(sFlat1,meet(sk1,sk3))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_3,t15776]) ).
cnf(g0_5,plain,
join(sFlat2,composition(sFlat1,meet(sk3,sk1))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_4,t165]) ).
cnf(g0_6,plain,
join(sFlat2,composition(sFlat1,sFlat3)) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_5,t174]) ).
cnf(g0_7,plain,
join(sFlat2,sFlat2) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_6,t19187]) ).
cnf(g0_8,plain,
sFlat2 != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_7,t2481]) ).
cnf(g0_9,plain,
sFlat2 != composition(meet(sk2,sFlat0),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_8,t102]) ).
cnf(g0_10,plain,
sFlat2 != composition(meet(sFlat0,sk2),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_9,t165]) ).
cnf(g0_11,plain,
sFlat2 != composition(sFlat1,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_10,t173]) ).
cnf(g0_12,plain,
sFlat2 != composition(sFlat1,meet(sk3,sk1)),
inference(rw,[status(thm)],[g0_11,t165]) ).
cnf(g0_13,plain,
sFlat2 != composition(sFlat1,sFlat3),
inference(rw,[status(thm)],[g0_12,t174]) ).
cnf(g0_14,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_13,t19187]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL036-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.56 % Computer : n011.cluster.edu
% 0.10/0.56 % Model : x86_64 x86_64
% 0.10/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.56 % Memory : 8046.5625MB
% 0.10/0.56 % OS : Linux 6.8.0-71-generic
% 0.10/0.56 % CPULimit : 300
% 0.10/0.56 % WCLimit : 300
% 0.10/0.56 % DateTime : Thu Sep 24 07:30:58 UTC 2026
% 0.10/0.56 % CPUTime :
% 0.10/0.56 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 78.41/11.83 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 78.41/11.83 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------