%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL032-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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:54 PM UTC 2026
% Result : Unsatisfiable 34.72s 4.82s
% Output : CNFRefutation 34.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 20
% Syntax : Number of clauses : 236 ( 236 unt; 0 nHn; 80 RR)
% Number of literals : 236 ( 235 equ; 15 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 12 con; 0-2 aty)
% Number of variables : 291 ( 25 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t63,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t97,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t98,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t63,t97]) ).
cnf(t9321,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t98,t63]) ).
cnf(t141,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t9321]) ).
cnf(t16,axiom,
sFlat0 = meet(sk2,sk3),
introduced(definition) ).
cnf(t95,plain,
meet(sk2,sk3) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t145,plain,
meet(sk2,sk3) = sFlat0,
inference(rw,[status(thm)],[t95]) ).
cnf(t9322,plain,
meet(sk3,sk2) = sFlat0,
inference(step,[status(thm)],[t145,t141]) ).
cnf(t148,plain,
meet(sk3,sk2) = sFlat0,
inference(orient,[status(thm)],[t9322]) ).
cnf(t17,axiom,
sFlat1 = composition(sk1,meet(sk2,sk3)),
introduced(definition) ).
cnf(t48,plain,
composition(sk1,meet(sk2,sk3)) = sFlat1,
inference(orient,[status(thm)],[t17]) ).
cnf(t9312,plain,
composition(sk1,sFlat0) = sFlat1,
inference(step,[status(thm)],[t48,t95]) ).
cnf(t96,plain,
composition(sk1,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t9312]) ).
cnf(t132,plain,
composition(sk1,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t96]) ).
cnf(t19,axiom,
sFlat3 = composition(sk1,sk3),
introduced(definition) ).
cnf(t58,plain,
composition(sk1,sk3) = sFlat3,
inference(orient,[status(thm)],[t19]) ).
cnf(t18,axiom,
sFlat2 = composition(sk1,sk2),
introduced(definition) ).
cnf(t53,plain,
composition(sk1,sk2) = sFlat2,
inference(orient,[status(thm)],[t18]) ).
cnf(t20,axiom,
sFlat4 = meet(composition(sk1,sk2),composition(sk1,sk3)),
introduced(definition) ).
cnf(t9310,plain,
sFlat4 = meet(sFlat2,composition(sk1,sk3)),
inference(step,[status(thm)],[t20,t53]) ).
cnf(t9311,plain,
sFlat4 = meet(sFlat2,sFlat3),
inference(step,[status(thm)],[t9310,t58]) ).
cnf(t94,plain,
meet(sFlat2,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t9311]) ).
cnf(t21,axiom,
sFlat5 = join(composition(sk1,meet(sk2,sk3)),meet(composition(sk1,sk2),composition(sk1,sk3))),
introduced(definition) ).
cnf(t9314,plain,
sFlat5 = join(composition(sk1,sFlat0),meet(composition(sk1,sk2),composition(sk1,sk3))),
inference(step,[status(thm)],[t21,t95]) ).
cnf(t9315,plain,
sFlat5 = join(composition(sk1,sFlat0),meet(sFlat2,composition(sk1,sk3))),
inference(step,[status(thm)],[t9314,t53]) ).
cnf(t9316,plain,
sFlat5 = join(composition(sk1,sFlat0),meet(sFlat2,sFlat3)),
inference(step,[status(thm)],[t9315,t58]) ).
cnf(t9317,plain,
sFlat5 = join(composition(sk1,sFlat0),sFlat4),
inference(step,[status(thm)],[t9316,t94]) ).
cnf(t9318,plain,
sFlat5 = join(sFlat4,composition(sk1,sFlat0)),
inference(step,[status(thm)],[t9317,t97]) ).
cnf(t120,plain,
join(sFlat4,composition(sk1,sFlat0)) = sFlat5,
inference(orient,[status(thm)],[t9318]) ).
cnf(t9320,plain,
join(sFlat4,sFlat1) = sFlat5,
inference(step,[status(thm)],[t120,t132]) ).
cnf(t140,plain,
join(sFlat4,sFlat1) = sFlat5,
inference(rw,[status(thm)],[t9320]) ).
cnf(t9325,plain,
join(sFlat1,sFlat4) = sFlat5,
inference(step,[status(thm)],[t140,t97]) ).
cnf(t152,plain,
join(sFlat1,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t9325]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t122,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t124,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t122,t26]) ).
cnf(t245,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t124]) ).
cnf(t123,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t122,t26]) ).
cnf(t218,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t123]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9313,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t97]) ).
cnf(t111,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t9313]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t39,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t41,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t39,t26]) ).
cnf(t178,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t41]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t179,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t178,t22]) ).
cnf(t9326,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t179,t26]) ).
cnf(t191,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t9326]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t28,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t27,t22]) ).
cnf(t154,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t28]) ).
cnf(t193,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t191,t154]) ).
cnf(t9328,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t193,t191]) ).
cnf(t212,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t9328]) ).
cnf(t215,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t111,t212]) ).
cnf(t192,plain,
one = converse(one),
inference(cp,[status(thm)],[t191,t22]) ).
cnf(t201,plain,
converse(one) = one,
inference(orient,[status(thm)],[t192]) ).
cnf(t9333,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t215,t201]) ).
cnf(t9334,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t9333,t212]) ).
cnf(t338,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t9334]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t24,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)],[t23,t23]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t99,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t105,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t99,t97]) ).
cnf(t9330,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t105,t99]) ).
cnf(t280,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t9330]) ).
cnf(t9335,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(complement(join(complement(X1),complement(X2))),X2)))),
inference(step,[status(thm)],[t24,t280]) ).
cnf(t9336,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)],[t9335,t97]) ).
cnf(t9337,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t9336,t63]) ).
cnf(t348,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t9337]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t106,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t110,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t63,t106]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t67,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t9319,plain,
zero = complement(top),
inference(step,[status(thm)],[t110,t67]) ).
cnf(t126,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t9319]) ).
cnf(t129,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t63,t126]) ).
cnf(t317,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t129]) ).
cnf(t9309,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t23,t63]) ).
cnf(t66,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t9309]) ).
cnf(t1416,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t66]) ).
cnf(t1432,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t1416,t338]) ).
cnf(t9449,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t1432,t97]) ).
cnf(t9450,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t9449,t67]) ).
cnf(t9451,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t9450,t97]) ).
cnf(t1475,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t9451]) ).
cnf(t1483,plain,
meet(top,complement(X1)) = complement(X1),
inference(cp,[status(thm)],[t317,t1475]) ).
cnf(t1484,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1483]) ).
cnf(t1493,plain,
join(complement(top),complement(complement(X1))) = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(cp,[status(thm)],[t348,t1484]) ).
cnf(t9462,plain,
join(zero,complement(complement(X1))) = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t1493,t126]) ).
cnf(t9463,plain,
X1 = join(complement(top),complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t9462,t1475]) ).
cnf(t9464,plain,
X1 = join(zero,complement(join(complement(top),join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t9463,t126]) ).
cnf(t9465,plain,
X1 = join(zero,complement(join(zero,join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t9464,t126]) ).
cnf(t9466,plain,
X1 = join(zero,complement(join(zero,complement(X1)))),
inference(step,[status(thm)],[t9465,t338]) ).
cnf(t9467,plain,
X1 = join(zero,meet(top,X1)),
inference(step,[status(thm)],[t9466,t317]) ).
cnf(t1527,plain,
join(zero,meet(top,X1)) = X1,
inference(orient,[status(thm)],[t9467]) ).
cnf(t1529,plain,
complement(X1) = join(zero,complement(X1)),
inference(cp,[status(thm)],[t1527,t1484]) ).
cnf(t1553,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1529]) ).
cnf(t347,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t63,t338]) ).
cnf(t370,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t347]) ).
cnf(t1562,plain,
complement(complement(X1)) = join(zero,meet(X1,X1)),
inference(cp,[status(thm)],[t1553,t370]) ).
cnf(t1419,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t1416,t67]) ).
cnf(t9448,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t1419,t63]) ).
cnf(t1467,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t9448]) ).
cnf(t9487,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t1562,t1467]) ).
cnf(t1577,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t9487]) ).
cnf(t1585,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t338,t1577]) ).
cnf(t9501,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1585,t1577]) ).
cnf(t9502,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t9501,t1577]) ).
cnf(t1641,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t9502]) ).
cnf(t1643,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t1641,t280]) ).
cnf(t9533,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t1643,t99]) ).
cnf(t9534,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t9533,t1641]) ).
cnf(t1880,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t9534]) ).
cnf(t1426,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t1416,t63]) ).
cnf(t9538,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t1426,t97]) ).
cnf(t1888,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t9538]) ).
cnf(t1896,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t1880,t1888]) ).
cnf(t9539,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t1896,t1888]) ).
cnf(t9540,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t9539,t97]) ).
cnf(t1898,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t9540]) ).
cnf(t1910,plain,
join(X1,converse(meet(converse(X1),X2))) = converse(converse(X1)),
inference(cp,[status(thm)],[t218,t1898]) ).
cnf(t9550,plain,
join(X1,converse(meet(converse(X1),X2))) = X1,
inference(step,[status(thm)],[t1910,t26]) ).
cnf(t2079,plain,
join(X1,converse(meet(converse(X1),X2))) = X1,
inference(orient,[status(thm)],[t9550]) ).
cnf(t2081,plain,
X1 = join(X1,converse(meet(X2,converse(X1)))),
inference(cp,[status(thm)],[t2079,t141]) ).
cnf(t2186,plain,
join(X1,converse(meet(X2,converse(X1)))) = X1,
inference(orient,[status(thm)],[t2081]) ).
cnf(t2210,plain,
join(converse(X1),meet(X2,converse(X1))) = converse(X1),
inference(cp,[status(thm)],[t245,t2186]) ).
cnf(t4821,plain,
join(converse(X1),meet(X2,converse(X1))) = converse(X1),
inference(orient,[status(thm)],[t2210]) ).
cnf(t4847,plain,
converse(converse(X1)) = join(X1,meet(X2,converse(converse(X1)))),
inference(cp,[status(thm)],[t4821,t26]) ).
cnf(t9703,plain,
X1 = join(X1,meet(X2,converse(converse(X1)))),
inference(step,[status(thm)],[t4847,t26]) ).
cnf(t9704,plain,
X1 = join(X1,meet(X2,X1)),
inference(step,[status(thm)],[t9703,t26]) ).
cnf(t4884,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t9704]) ).
cnf(t1587,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t63,t1577]) ).
cnf(t1712,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t1587]) ).
cnf(t1717,plain,
meet(complement(join(X1,X2)),X3) = complement(join(X1,join(X2,complement(X3)))),
inference(cp,[status(thm)],[t1712,t99]) ).
cnf(t3705,plain,
complement(join(X1,join(X2,complement(X3)))) = meet(complement(join(X1,X2)),X3),
inference(orient,[status(thm)],[t1717]) ).
cnf(t1588,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t63,t1577]) ).
cnf(t1743,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t1588]) ).
cnf(t3706,plain,
meet(complement(join(complement(X1),X2)),X3) = meet(X1,complement(join(X2,complement(X3)))),
inference(cp,[status(thm)],[t3705,t1743]) ).
cnf(t9646,plain,
meet(meet(X1,complement(X2)),X3) = meet(X1,complement(join(X2,complement(X3)))),
inference(step,[status(thm)],[t3706,t1743]) ).
cnf(t9647,plain,
meet(meet(X1,complement(X2)),X3) = meet(X1,meet(complement(X2),X3)),
inference(step,[status(thm)],[t9646,t1712]) ).
cnf(t4074,plain,
meet(meet(X1,complement(X2)),X3) = meet(X1,meet(complement(X2),X3)),
inference(orient,[status(thm)],[t9647]) ).
cnf(t4108,plain,
meet(X1,meet(complement(complement(X2)),X3)) = meet(meet(X1,X2),X3),
inference(cp,[status(thm)],[t4074,t1577]) ).
cnf(t9648,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t4108,t1577]) ).
cnf(t4142,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t9648]) ).
cnf(t1906,plain,
meet(X1,complement(meet(complement(X1),X2))) = complement(complement(X1)),
inference(cp,[status(thm)],[t1743,t1898]) ).
cnf(t1722,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t1577,t1712]) ).
cnf(t1836,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t1722]) ).
cnf(t9547,plain,
meet(X1,join(X1,complement(X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t1906,t1836]) ).
cnf(t9548,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t9547,t1577]) ).
cnf(t2042,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t9548]) ).
cnf(t2046,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t2042,t1577]) ).
cnf(t2051,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t2046]) ).
cnf(t4161,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t4142,t2051]) ).
cnf(t8814,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t4161]) ).
cnf(t183,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t122,t178]) ).
cnf(t2683,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t183]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t36,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t42,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t36,t39]) ).
cnf(t8882,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t42]) ).
cnf(t8987,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)],[t2683,t8882]) ).
cnf(t9926,plain,
join(composition(X1,X2),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t8987,t26]) ).
cnf(t9927,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t9926,t26]) ).
cnf(t227,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t39,t218]) ).
cnf(t2862,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t227]) ).
cnf(t9928,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(converse(converse(X1)),join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t9927,t2862]) ).
cnf(t9929,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t9928,t26]) ).
cnf(t9930,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t9929,t26]) ).
cnf(t8993,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9930]) ).
cnf(t9049,plain,
composition(sk1,join(sFlat0,X1)) = join(sFlat1,composition(sk1,X1)),
inference(cp,[status(thm)],[t8993,t132]) ).
cnf(t9135,plain,
composition(sk1,join(sFlat0,X1)) = join(sFlat1,composition(sk1,X1)),
inference(orient,[status(thm)],[t9049]) ).
cnf(t2187,plain,
converse(X1) = converse(join(X1,meet(X2,converse(converse(X1))))),
inference(cp,[status(thm)],[t2186,t122]) ).
cnf(t9580,plain,
converse(X1) = converse(join(X1,meet(X2,X1))),
inference(step,[status(thm)],[t2187,t26]) ).
cnf(t2215,plain,
converse(join(X1,meet(X2,X1))) = converse(X1),
inference(orient,[status(thm)],[t9580]) ).
cnf(t2219,plain,
converse(sk2) = converse(join(sk2,sFlat0)),
inference(cp,[status(thm)],[t2215,t148]) ).
cnf(t9581,plain,
converse(sk2) = converse(join(sFlat0,sk2)),
inference(step,[status(thm)],[t2219,t97]) ).
cnf(t2231,plain,
converse(join(sFlat0,sk2)) = converse(sk2),
inference(orient,[status(thm)],[t9581]) ).
cnf(t2232,plain,
join(sFlat0,sk2) = converse(converse(sk2)),
inference(cp,[status(thm)],[t26,t2231]) ).
cnf(t9582,plain,
join(sFlat0,sk2) = sk2,
inference(step,[status(thm)],[t2232,t26]) ).
cnf(t2254,plain,
join(sFlat0,sk2) = sk2,
inference(orient,[status(thm)],[t9582]) ).
cnf(t9137,plain,
join(sFlat1,composition(sk1,sk2)) = composition(sk1,sk2),
inference(cp,[status(thm)],[t9135,t2254]) ).
cnf(t9931,plain,
join(sFlat1,sFlat2) = composition(sk1,sk2),
inference(step,[status(thm)],[t9137,t53]) ).
cnf(t9932,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t9931,t53]) ).
cnf(t9201,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t9932]) ).
cnf(t9207,plain,
meet(sFlat1,X1) = meet(sFlat1,meet(sFlat2,X1)),
inference(cp,[status(thm)],[t8814,t9201]) ).
cnf(t9241,plain,
meet(sFlat1,meet(sFlat2,X1)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t9207]) ).
cnf(t9246,plain,
meet(sFlat1,sFlat3) = meet(sFlat1,sFlat4),
inference(cp,[status(thm)],[t9241,t94]) ).
cnf(t1424,plain,
sk3 = join(sFlat0,complement(join(complement(sk3),sk2))),
inference(cp,[status(thm)],[t1416,t148]) ).
cnf(t9531,plain,
sk3 = join(sFlat0,meet(sk3,complement(sk2))),
inference(step,[status(thm)],[t1424,t1743]) ).
cnf(t1873,plain,
join(sFlat0,meet(sk3,complement(sk2))) = sk3,
inference(orient,[status(thm)],[t9531]) ).
cnf(t1881,plain,
join(sFlat0,meet(sk3,complement(sk2))) = join(sFlat0,sk3),
inference(cp,[status(thm)],[t1880,t1873]) ).
cnf(t9535,plain,
sk3 = join(sFlat0,sk3),
inference(step,[status(thm)],[t1881,t1873]) ).
cnf(t1885,plain,
join(sFlat0,sk3) = sk3,
inference(orient,[status(thm)],[t9535]) ).
cnf(t9139,plain,
join(sFlat1,composition(sk1,sk3)) = composition(sk1,sk3),
inference(cp,[status(thm)],[t9135,t1885]) ).
cnf(t9940,plain,
join(sFlat1,sFlat3) = composition(sk1,sk3),
inference(step,[status(thm)],[t9139,t58]) ).
cnf(t9941,plain,
join(sFlat1,sFlat3) = sFlat3,
inference(step,[status(thm)],[t9940,t58]) ).
cnf(t9219,plain,
join(sFlat1,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t9941]) ).
cnf(t9220,plain,
sFlat1 = meet(sFlat1,sFlat3),
inference(cp,[status(thm)],[t2051,t9219]) ).
cnf(t9234,plain,
meet(sFlat1,sFlat3) = sFlat1,
inference(orient,[status(thm)],[t9220]) ).
cnf(t9942,plain,
sFlat1 = meet(sFlat1,sFlat4),
inference(step,[status(thm)],[t9246,t9234]) ).
cnf(t9269,plain,
meet(sFlat1,sFlat4) = sFlat1,
inference(orient,[status(thm)],[t9942]) ).
cnf(t9270,plain,
sFlat4 = join(sFlat4,sFlat1),
inference(cp,[status(thm)],[t4884,t9269]) ).
cnf(t9943,plain,
sFlat4 = join(sFlat1,sFlat4),
inference(step,[status(thm)],[t9270,t97]) ).
cnf(t9944,plain,
sFlat4 = sFlat5,
inference(step,[status(thm)],[t9943,t152]) ).
cnf(t9273,plain,
sFlat5 = sFlat4,
inference(orient,[status(thm)],[t9944]) ).
cnf(t9945,plain,
join(sFlat1,sFlat4) = sFlat4,
inference(step,[status(thm)],[t152,t9273]) ).
cnf(t9274,plain,
join(sFlat1,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t9945]) ).
cnf(goal_0,negated_conjecture,
join(composition(sk1,meet(sk2,sk3)),meet(composition(sk1,sk2),composition(sk1,sk3))) != meet(composition(sk1,sk2),composition(sk1,sk3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(composition(sk1,meet(sk3,sk2)),meet(composition(sk1,sk2),composition(sk1,sk3))) != meet(composition(sk1,sk2),composition(sk1,sk3)),
inference(rw,[status(thm)],[goal_0,t141]) ).
cnf(g0_1,plain,
join(composition(sk1,sFlat0),meet(composition(sk1,sk2),composition(sk1,sk3))) != meet(composition(sk1,sk2),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_0,t148]) ).
cnf(g0_2,plain,
join(sFlat1,meet(composition(sk1,sk2),composition(sk1,sk3))) != meet(composition(sk1,sk2),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_1,t132]) ).
cnf(g0_3,plain,
join(sFlat1,meet(composition(sk1,sk3),composition(sk1,sk2))) != meet(composition(sk1,sk2),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_2,t141]) ).
cnf(g0_4,plain,
join(sFlat1,meet(sFlat3,composition(sk1,sk2))) != meet(composition(sk1,sk2),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_3,t58]) ).
cnf(g0_5,plain,
join(sFlat1,meet(sFlat3,sFlat2)) != meet(composition(sk1,sk2),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_4,t53]) ).
cnf(g0_6,plain,
join(sFlat1,meet(sFlat2,sFlat3)) != meet(composition(sk1,sk2),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_5,t141]) ).
cnf(g0_7,plain,
join(sFlat1,sFlat4) != meet(composition(sk1,sk2),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_6,t94]) ).
cnf(g0_8,plain,
sFlat4 != meet(composition(sk1,sk2),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_7,t9274]) ).
cnf(g0_9,plain,
sFlat4 != meet(composition(sk1,sk3),composition(sk1,sk2)),
inference(rw,[status(thm)],[g0_8,t141]) ).
cnf(g0_10,plain,
sFlat4 != meet(sFlat3,composition(sk1,sk2)),
inference(rw,[status(thm)],[g0_9,t58]) ).
cnf(g0_11,plain,
sFlat4 != meet(sFlat3,sFlat2),
inference(rw,[status(thm)],[g0_10,t53]) ).
cnf(g0_12,plain,
sFlat4 != meet(sFlat2,sFlat3),
inference(rw,[status(thm)],[g0_11,t141]) ).
cnf(g0_13,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_12,t94]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL032-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.37 % Computer : n011.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Thu Sep 24 07:27:42 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 34.72/4.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 34.72/4.82 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------