%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL045-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 : n016.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 156.54s 30.28s
% Output : CNFRefutation 156.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 19
% Syntax : Number of clauses : 274 ( 274 unt; 0 nHn; 89 RR)
% Number of literals : 274 ( 273 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 : 305 ( 19 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t16,axiom,
sFlat0 = converse(sk1),
introduced(definition) ).
cnf(t60,plain,
converse(sk1) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t17,axiom,
sFlat1 = composition(sk1,converse(sk1)),
introduced(definition) ).
cnf(t51,plain,
composition(sk1,converse(sk1)) = sFlat1,
inference(orient,[status(thm)],[t17]) ).
cnf(t56325,plain,
composition(sk1,sFlat0) = sFlat1,
inference(step,[status(thm)],[t51,t60]) ).
cnf(t68,plain,
composition(sk1,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t56325]) ).
cnf(t132,plain,
composition(sk1,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t68]) ).
cnf(t135,plain,
composition(sk1,composition(sFlat0,X1)) = composition(sFlat1,X1),
inference(cp,[status(thm)],[t25,t132]) ).
cnf(t502,plain,
composition(sk1,composition(sFlat0,X1)) = composition(sFlat1,X1),
inference(orient,[status(thm)],[t135]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,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/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t61,plain,
sk1 = converse(sFlat0),
inference(cp,[status(thm)],[t21,t60]) ).
cnf(t122,plain,
converse(sFlat0) = sk1,
inference(orient,[status(thm)],[t61]) ).
cnf(t126,plain,
converse(composition(sFlat0,X1)) = composition(converse(X1),sk1),
inference(cp,[status(thm)],[t29,t122]) ).
cnf(t256,plain,
converse(composition(sFlat0,X1)) = composition(converse(X1),sk1),
inference(orient,[status(thm)],[t126]) ).
cnf(t65,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sFlat0),
inference(cp,[status(thm)],[t29,t60]) ).
cnf(t186,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sFlat0),
inference(orient,[status(thm)],[t65]) ).
cnf(t18,axiom,
sFlat2 = composition(composition(sk1,converse(sk1)),sk1),
introduced(definition) ).
cnf(t56324,plain,
sFlat2 = composition(sk1,composition(converse(sk1),sk1)),
inference(step,[status(thm)],[t18,t25]) ).
cnf(t27,plain,
composition(sk1,composition(converse(sk1),sk1)) = sFlat2,
inference(orient,[status(thm)],[t56324]) ).
cnf(t56326,plain,
composition(sk1,composition(sFlat0,sk1)) = sFlat2,
inference(step,[status(thm)],[t27,t60]) ).
cnf(t69,plain,
composition(sk1,composition(sFlat0,sk1)) = sFlat2,
inference(rw,[status(thm)],[t56326]) ).
cnf(t212,plain,
composition(sk1,composition(sFlat0,sk1)) = sFlat2,
inference(orient,[status(thm)],[t69]) ).
cnf(t213,plain,
composition(converse(composition(sFlat0,sk1)),sFlat0) = converse(sFlat2),
inference(cp,[status(thm)],[t186,t212]) ).
cnf(t64,plain,
converse(composition(X1,sk1)) = composition(sFlat0,converse(X1)),
inference(cp,[status(thm)],[t29,t60]) ).
cnf(t176,plain,
converse(composition(X1,sk1)) = composition(sFlat0,converse(X1)),
inference(orient,[status(thm)],[t64]) ).
cnf(t56340,plain,
composition(composition(sFlat0,converse(sFlat0)),sFlat0) = converse(sFlat2),
inference(step,[status(thm)],[t213,t176]) ).
cnf(t56341,plain,
composition(sFlat0,composition(converse(sFlat0),sFlat0)) = converse(sFlat2),
inference(step,[status(thm)],[t56340,t25]) ).
cnf(t56342,plain,
composition(sFlat0,composition(sk1,sFlat0)) = converse(sFlat2),
inference(step,[status(thm)],[t56341,t122]) ).
cnf(t56343,plain,
composition(sFlat0,sFlat1) = converse(sFlat2),
inference(step,[status(thm)],[t56342,t132]) ).
cnf(t223,plain,
composition(sFlat0,sFlat1) = converse(sFlat2),
inference(orient,[status(thm)],[t56343]) ).
cnf(t257,plain,
composition(converse(sFlat1),sk1) = converse(converse(sFlat2)),
inference(cp,[status(thm)],[t256,t223]) ).
cnf(t187,plain,
composition(converse(sFlat0),sFlat0) = converse(sFlat1),
inference(cp,[status(thm)],[t186,t132]) ).
cnf(t56335,plain,
composition(sk1,sFlat0) = converse(sFlat1),
inference(step,[status(thm)],[t187,t122]) ).
cnf(t56336,plain,
sFlat1 = converse(sFlat1),
inference(step,[status(thm)],[t56335,t132]) ).
cnf(t197,plain,
converse(sFlat1) = sFlat1,
inference(orient,[status(thm)],[t56336]) ).
cnf(t56345,plain,
composition(sFlat1,sk1) = converse(converse(sFlat2)),
inference(step,[status(thm)],[t257,t197]) ).
cnf(t56346,plain,
composition(sFlat1,sk1) = sFlat2,
inference(step,[status(thm)],[t56345,t21]) ).
cnf(t266,plain,
composition(sFlat1,sk1) = sFlat2,
inference(orient,[status(thm)],[t56346]) ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t70,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t19,axiom,
sFlat3 = join(sk1,composition(composition(sk1,converse(sk1)),sk1)),
introduced(definition) ).
cnf(t56328,plain,
sFlat3 = join(sk1,composition(sk1,composition(converse(sk1),sk1))),
inference(step,[status(thm)],[t19,t25]) ).
cnf(t56329,plain,
sFlat3 = join(sk1,composition(sk1,composition(sFlat0,sk1))),
inference(step,[status(thm)],[t56328,t60]) ).
cnf(t108,plain,
join(sk1,composition(sk1,composition(sFlat0,sk1))) = sFlat3,
inference(orient,[status(thm)],[t56329]) ).
cnf(t56338,plain,
join(sk1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t108,t212]) ).
cnf(t219,plain,
join(sk1,sFlat2) = sFlat3,
inference(rw,[status(thm)],[t56338]) ).
cnf(t56339,plain,
join(sFlat2,sk1) = sFlat3,
inference(step,[status(thm)],[t219,t70]) ).
cnf(t220,plain,
join(sFlat2,sk1) = sFlat3,
inference(orient,[status(thm)],[t56339]) ).
cnf(t15,axiom,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t40,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t15]) ).
cnf(t56,plain,
composition(meet(X1,composition(sk1,converse(sk1))),meet(sk1,composition(converse(X1),sk1))) = join(meet(composition(X1,sk1),sk1),composition(meet(X1,sFlat1),meet(sk1,composition(converse(X1),sk1)))),
inference(cp,[status(thm)],[t40,t51]) ).
cnf(t57549,plain,
composition(meet(X1,composition(sk1,sFlat0)),meet(sk1,composition(converse(X1),sk1))) = join(meet(composition(X1,sk1),sk1),composition(meet(X1,sFlat1),meet(sk1,composition(converse(X1),sk1)))),
inference(step,[status(thm)],[t56,t60]) ).
cnf(t57550,plain,
composition(meet(X1,sFlat1),meet(sk1,composition(converse(X1),sk1))) = join(meet(composition(X1,sk1),sk1),composition(meet(X1,sFlat1),meet(sk1,composition(converse(X1),sk1)))),
inference(step,[status(thm)],[t57549,t132]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t110,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t112,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t110,t70]) ).
cnf(t56330,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t112,t110]) ).
cnf(t140,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t56330]) ).
cnf(t57551,plain,
composition(meet(X1,sFlat1),meet(sk1,composition(converse(X1),sk1))) = join(meet(sk1,composition(X1,sk1)),composition(meet(X1,sFlat1),meet(sk1,composition(converse(X1),sk1)))),
inference(step,[status(thm)],[t57550,t140]) ).
cnf(t44928,plain,
join(meet(sk1,composition(X1,sk1)),composition(meet(X1,sFlat1),meet(sk1,composition(converse(X1),sk1)))) = composition(meet(X1,sFlat1),meet(sk1,composition(converse(X1),sk1))),
inference(orient,[status(thm)],[t57551]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t71,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t22]) ).
cnf(t57812,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t71,t70]) ).
cnf(t57813,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t57812,t110]) ).
cnf(t57814,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t57813,t70]) ).
cnf(t55244,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t57814]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t57,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t58,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t57,t21]) ).
cnf(t369,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t58]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t31,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t29,t21]) ).
cnf(t314,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t31]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t315,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t314,t20]) ).
cnf(t56348,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t315,t21]) ).
cnf(t333,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t56348]) ).
cnf(t26,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t25,t20]) ).
cnf(t279,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t335,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t333,t279]) ).
cnf(t56350,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t335,t333]) ).
cnf(t354,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t56350]) ).
cnf(t355,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t33,t354]) ).
cnf(t678,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t355]) ).
cnf(t703,plain,
join(X1,converse(composition(X2,converse(X1)))) = converse(composition(join(one,X2),converse(X1))),
inference(cp,[status(thm)],[t369,t678]) ).
cnf(t30,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t29,t21]) ).
cnf(t285,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t30]) ).
cnf(t56478,plain,
join(X1,composition(X1,converse(X2))) = converse(composition(join(one,X2),converse(X1))),
inference(step,[status(thm)],[t703,t285]) ).
cnf(t56479,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,converse(join(one,X2))),
inference(step,[status(thm)],[t56478,t285]) ).
cnf(t334,plain,
one = converse(one),
inference(cp,[status(thm)],[t333,t20]) ).
cnf(t343,plain,
converse(one) = one,
inference(orient,[status(thm)],[t334]) ).
cnf(t373,plain,
join(one,converse(X1)) = converse(join(one,X1)),
inference(cp,[status(thm)],[t369,t343]) ).
cnf(t394,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t373]) ).
cnf(t56480,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(step,[status(thm)],[t56479,t394]) ).
cnf(t2149,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(orient,[status(thm)],[t56480]) ).
cnf(t2181,plain,
composition(X1,join(one,converse(one))) = join(X1,composition(X1,one)),
inference(cp,[status(thm)],[t2149,t343]) ).
cnf(t56483,plain,
composition(X1,join(one,one)) = join(X1,composition(X1,one)),
inference(step,[status(thm)],[t2181,t343]) ).
cnf(t56484,plain,
composition(X1,join(one,one)) = join(X1,X1),
inference(step,[status(thm)],[t56483,t20]) ).
cnf(t2273,plain,
composition(X1,join(one,one)) = join(X1,X1),
inference(orient,[status(thm)],[t56484]) ).
cnf(t55366,plain,
X1 = join(meet(X1,complement(X1)),complement(composition(complement(X1),join(one,one)))),
inference(cp,[status(thm)],[t55244,t2273]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t117,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t57837,plain,
X1 = join(zero,complement(composition(complement(X1),join(one,one)))),
inference(step,[status(thm)],[t55366,t117]) ).
cnf(t23,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)],[t22,t22]) ).
cnf(t56351,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)],[t23,t70]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t72,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t56352,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)],[t56351,t72]) ).
cnf(t56353,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t56352,t110]) ).
cnf(t405,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t56353]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t78,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t80,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t72,t78]) ).
cnf(t557,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t80]) ).
cnf(t563,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t557,t70]) ).
cnf(t665,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t563]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t56327,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t70]) ).
cnf(t81,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t56327]) ).
cnf(t357,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t81,t354]) ).
cnf(t56357,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t357,t343]) ).
cnf(t56358,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t56357,t354]) ).
cnf(t528,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t56358]) ).
cnf(t537,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t110,t528]) ).
cnf(t542,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t537]) ).
cnf(t671,plain,
join(top,X1) = join(complement(X2),join(X1,meet(X2,X2))),
inference(cp,[status(thm)],[t665,t542]) ).
cnf(t39531,plain,
join(complement(X1),join(X2,meet(X1,X1))) = join(top,X2),
inference(orient,[status(thm)],[t671]) ).
cnf(t39533,plain,
join(complement(X1),complement(X1)) = join(complement(X1),complement(join(top,X1))),
inference(cp,[status(thm)],[t405,t39531]) ).
cnf(t57343,plain,
complement(X1) = join(complement(X1),complement(join(top,X1))),
inference(step,[status(thm)],[t39533,t528]) ).
cnf(t39534,plain,
join(complement(X1),complement(join(top,X1))) = complement(X1),
inference(orient,[status(thm)],[t57343]) ).
cnf(t39590,plain,
complement(X1) = join(complement(X1),complement(join(X1,top))),
inference(cp,[status(thm)],[t39534,t70]) ).
cnf(t562,plain,
join(top,complement(complement(X1))) = join(X1,top),
inference(cp,[status(thm)],[t557,t78]) ).
cnf(t561,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t557,t528]) ).
cnf(t56362,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t561,t78]) ).
cnf(t578,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t56362]) ).
cnf(t56363,plain,
top = join(X1,top),
inference(step,[status(thm)],[t562,t578]) ).
cnf(t582,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t56363]) ).
cnf(t57344,plain,
complement(X1) = join(complement(X1),complement(top)),
inference(step,[status(thm)],[t39590,t582]) ).
cnf(t111,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t110,t78]) ).
cnf(t56331,plain,
zero = complement(top),
inference(step,[status(thm)],[t111,t117]) ).
cnf(t146,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t56331]) ).
cnf(t57345,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t57344,t146]) ).
cnf(t57346,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t57345,t70]) ).
cnf(t39602,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t57346]) ).
cnf(t57838,plain,
X1 = complement(composition(complement(X1),join(one,one))),
inference(step,[status(thm)],[t57837,t39602]) ).
cnf(t325,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t57,t314]) ).
cnf(t6266,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t325]) ).
cnf(t34,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t33,t29]) ).
cnf(t1579,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t34]) ).
cnf(t6269,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)],[t6266,t1579]) ).
cnf(t56560,plain,
join(composition(X1,X2),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t6269,t21]) ).
cnf(t56561,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t56560,t21]) ).
cnf(t56562,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,converse(join(converse(X2),converse(X3)))),
inference(step,[status(thm)],[t56561,t285]) ).
cnf(t56563,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t56562,t369]) ).
cnf(t56564,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t56563,t21]) ).
cnf(t6453,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t56564]) ).
cnf(t6454,plain,
composition(X1,join(X2,X2)) = composition(join(X1,X1),X2),
inference(cp,[status(thm)],[t6453,t33]) ).
cnf(t6542,plain,
composition(X1,join(X2,X2)) = composition(join(X1,X1),X2),
inference(orient,[status(thm)],[t6454]) ).
cnf(t6588,plain,
composition(complement(X1),join(X2,X2)) = composition(complement(X1),X2),
inference(cp,[status(thm)],[t6542,t528]) ).
cnf(t6707,plain,
composition(complement(X1),join(X2,X2)) = composition(complement(X1),X2),
inference(orient,[status(thm)],[t6588]) ).
cnf(t57839,plain,
X1 = complement(composition(complement(X1),one)),
inference(step,[status(thm)],[t57838,t6707]) ).
cnf(t57840,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t57839,t20]) ).
cnf(t149,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t110,t146]) ).
cnf(t508,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t149]) ).
cnf(t57356,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t508,t39602]) ).
cnf(t39633,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t57356]) ).
cnf(t39650,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t39633]) ).
cnf(t57841,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t57840,t39650]) ).
cnf(t55483,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t57841]) ).
cnf(t55516,plain,
composition(meet(top,sFlat1),meet(sk1,composition(converse(top),sk1))) = join(meet(sk1,composition(top,sk1)),composition(sFlat1,meet(sk1,composition(converse(top),sk1)))),
inference(cp,[status(thm)],[t44928,t55483]) ).
cnf(t57923,plain,
composition(sFlat1,meet(sk1,composition(converse(top),sk1))) = join(meet(sk1,composition(top,sk1)),composition(sFlat1,meet(sk1,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t55516,t55483]) ).
cnf(t63,plain,
converse(join(X1,sk1)) = join(converse(X1),sFlat0),
inference(cp,[status(thm)],[t57,t60]) ).
cnf(t56334,plain,
converse(join(X1,sk1)) = join(sFlat0,converse(X1)),
inference(step,[status(thm)],[t63,t70]) ).
cnf(t166,plain,
converse(join(X1,sk1)) = join(sFlat0,converse(X1)),
inference(orient,[status(thm)],[t56334]) ).
cnf(t169,plain,
converse(join(join(X1,sk1),X2)) = join(join(sFlat0,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t57,t166]) ).
cnf(t56376,plain,
converse(join(X1,join(sk1,X2))) = join(join(sFlat0,converse(X1)),converse(X2)),
inference(step,[status(thm)],[t169,t72]) ).
cnf(t56377,plain,
converse(join(X1,join(sk1,X2))) = join(sFlat0,join(converse(X1),converse(X2))),
inference(step,[status(thm)],[t56376,t72]) ).
cnf(t56378,plain,
converse(join(X1,join(sk1,X2))) = join(sFlat0,converse(join(X1,X2))),
inference(step,[status(thm)],[t56377,t57]) ).
cnf(t786,plain,
converse(join(X1,join(sk1,X2))) = join(sFlat0,converse(join(X1,X2))),
inference(orient,[status(thm)],[t56378]) ).
cnf(t370,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t369,t78]) ).
cnf(t617,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t370]) ).
cnf(t791,plain,
join(sFlat0,converse(join(X1,converse(complement(converse(sk1)))))) = converse(join(X1,converse(top))),
inference(cp,[status(thm)],[t786,t617]) ).
cnf(t59,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t57,t21]) ).
cnf(t426,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t59]) ).
cnf(t56379,plain,
join(sFlat0,join(converse(X1),complement(converse(sk1)))) = converse(join(X1,converse(top))),
inference(step,[status(thm)],[t791,t426]) ).
cnf(t56380,plain,
join(sFlat0,join(converse(X1),complement(sFlat0))) = converse(join(X1,converse(top))),
inference(step,[status(thm)],[t56379,t60]) ).
cnf(t56381,plain,
join(top,converse(X1)) = converse(join(X1,converse(top))),
inference(step,[status(thm)],[t56380,t665]) ).
cnf(t56382,plain,
join(top,converse(X1)) = join(converse(X1),top),
inference(step,[status(thm)],[t56381,t426]) ).
cnf(t56383,plain,
join(top,converse(X1)) = top,
inference(step,[status(thm)],[t56382,t582]) ).
cnf(t808,plain,
join(top,converse(X1)) = top,
inference(orient,[status(thm)],[t56383]) ).
cnf(t587,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t369,t582]) ).
cnf(t588,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t587]) ).
cnf(t809,plain,
top = converse(top),
inference(cp,[status(thm)],[t808,t588]) ).
cnf(t825,plain,
converse(top) = top,
inference(orient,[status(thm)],[t809]) ).
cnf(t57924,plain,
composition(sFlat1,meet(sk1,composition(top,sk1))) = join(meet(sk1,composition(top,sk1)),composition(sFlat1,meet(sk1,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t57923,t825]) ).
cnf(t682,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t678,t582]) ).
cnf(t722,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t682]) ).
cnf(t39,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t33,t25]) ).
cnf(t14050,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t39]) ).
cnf(t14051,plain,
composition(join(X1,composition(X1,X2)),X3) = composition(X1,join(X3,composition(X2,X3))),
inference(cp,[status(thm)],[t14050,t6453]) ).
cnf(t14224,plain,
composition(join(X1,composition(X1,X2)),X3) = composition(X1,join(X3,composition(X2,X3))),
inference(orient,[status(thm)],[t14051]) ).
cnf(t14452,plain,
composition(top,join(X1,composition(X2,X1))) = join(join(X1,composition(X2,X1)),composition(join(top,composition(top,X2)),X1)),
inference(cp,[status(thm)],[t722,t14224]) ).
cnf(t56715,plain,
composition(top,join(X1,composition(X2,X1))) = join(X1,join(composition(X2,X1),composition(join(top,composition(top,X2)),X1))),
inference(step,[status(thm)],[t14452,t72]) ).
cnf(t56716,plain,
composition(top,join(X1,composition(X2,X1))) = join(X1,composition(join(X2,join(top,composition(top,X2))),X1)),
inference(step,[status(thm)],[t56715,t33]) ).
cnf(t815,plain,
top = join(top,composition(converse(X1),X2)),
inference(cp,[status(thm)],[t808,t314]) ).
cnf(t916,plain,
join(top,composition(converse(X1),X2)) = top,
inference(orient,[status(thm)],[t815]) ).
cnf(t936,plain,
top = join(top,composition(X1,X2)),
inference(cp,[status(thm)],[t916,t21]) ).
cnf(t938,plain,
join(top,composition(X1,X2)) = top,
inference(orient,[status(thm)],[t936]) ).
cnf(t56717,plain,
composition(top,join(X1,composition(X2,X1))) = join(X1,composition(join(X2,top),X1)),
inference(step,[status(thm)],[t56716,t938]) ).
cnf(t56718,plain,
composition(top,join(X1,composition(X2,X1))) = join(X1,composition(top,X1)),
inference(step,[status(thm)],[t56717,t582]) ).
cnf(t56719,plain,
composition(top,join(X1,composition(X2,X1))) = composition(top,X1),
inference(step,[status(thm)],[t56718,t722]) ).
cnf(t14472,plain,
composition(top,join(X1,composition(X2,X1))) = composition(top,X1),
inference(orient,[status(thm)],[t56719]) ).
cnf(t14510,plain,
composition(top,sk1) = composition(top,join(sk1,sFlat2)),
inference(cp,[status(thm)],[t14472,t266]) ).
cnf(t56720,plain,
composition(top,sk1) = composition(top,join(sFlat2,sk1)),
inference(step,[status(thm)],[t14510,t70]) ).
cnf(t56721,plain,
composition(top,sk1) = composition(top,sFlat3),
inference(step,[status(thm)],[t56720,t220]) ).
cnf(t14590,plain,
composition(top,sk1) = composition(top,sFlat3),
inference(orient,[status(thm)],[t56721]) ).
cnf(t57925,plain,
composition(sFlat1,meet(sk1,composition(top,sFlat3))) = join(meet(sk1,composition(top,sk1)),composition(sFlat1,meet(sk1,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t57924,t14590]) ).
cnf(t14619,plain,
complement(sk1) = join(complement(sk1),composition(converse(top),complement(composition(top,sFlat3)))),
inference(cp,[status(thm)],[t81,t14590]) ).
cnf(t57215,plain,
complement(sk1) = join(complement(sk1),composition(top,complement(composition(top,sFlat3)))),
inference(step,[status(thm)],[t14619,t825]) ).
cnf(t34133,plain,
join(complement(sk1),composition(top,complement(composition(top,sFlat3)))) = complement(sk1),
inference(orient,[status(thm)],[t57215]) ).
cnf(t939,plain,
top = composition(top,top),
inference(cp,[status(thm)],[t938,t722]) ).
cnf(t940,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t939]) ).
cnf(t941,plain,
composition(top,composition(top,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t25,t940]) ).
cnf(t2142,plain,
composition(top,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t941]) ).
cnf(t2146,plain,
complement(composition(top,X1)) = join(complement(composition(top,X1)),composition(converse(top),complement(composition(top,X1)))),
inference(cp,[status(thm)],[t81,t2142]) ).
cnf(t356,plain,
composition(join(X1,one),X2) = join(composition(X1,X2),X2),
inference(cp,[status(thm)],[t33,t354]) ).
cnf(t56373,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(step,[status(thm)],[t356,t70]) ).
cnf(t704,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t56373]) ).
cnf(t57528,plain,
complement(composition(top,X1)) = composition(join(converse(top),one),complement(composition(top,X1))),
inference(step,[status(thm)],[t2146,t704]) ).
cnf(t57529,plain,
complement(composition(top,X1)) = composition(join(one,converse(top)),complement(composition(top,X1))),
inference(step,[status(thm)],[t57528,t70]) ).
cnf(t57530,plain,
complement(composition(top,X1)) = composition(converse(top),complement(composition(top,X1))),
inference(step,[status(thm)],[t57529,t588]) ).
cnf(t57531,plain,
complement(composition(top,X1)) = composition(top,complement(composition(top,X1))),
inference(step,[status(thm)],[t57530,t825]) ).
cnf(t43661,plain,
composition(top,complement(composition(top,X1))) = complement(composition(top,X1)),
inference(orient,[status(thm)],[t57531]) ).
cnf(t57532,plain,
join(complement(sk1),complement(composition(top,sFlat3))) = complement(sk1),
inference(step,[status(thm)],[t34133,t43661]) ).
cnf(t43708,plain,
join(complement(sk1),complement(composition(top,sFlat3))) = complement(sk1),
inference(rw,[status(thm)],[t57532]) ).
cnf(t51486,plain,
join(complement(sk1),complement(composition(top,sFlat3))) = complement(sk1),
inference(orient,[status(thm)],[t43708]) ).
cnf(t51487,plain,
meet(sk1,composition(top,sFlat3)) = complement(complement(sk1)),
inference(cp,[status(thm)],[t110,t51486]) ).
cnf(t57713,plain,
meet(sk1,composition(top,sFlat3)) = meet(top,sk1),
inference(step,[status(thm)],[t51487,t39650]) ).
cnf(t51494,plain,
meet(sk1,composition(top,sFlat3)) = meet(top,sk1),
inference(orient,[status(thm)],[t57713]) ).
cnf(t57850,plain,
meet(sk1,composition(top,sFlat3)) = sk1,
inference(step,[status(thm)],[t51494,t55483]) ).
cnf(t55492,plain,
meet(sk1,composition(top,sFlat3)) = sk1,
inference(orient,[status(thm)],[t57850]) ).
cnf(t57926,plain,
composition(sFlat1,sk1) = join(meet(sk1,composition(top,sk1)),composition(sFlat1,meet(sk1,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t57925,t55492]) ).
cnf(t57927,plain,
sFlat2 = join(meet(sk1,composition(top,sk1)),composition(sFlat1,meet(sk1,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t57926,t266]) ).
cnf(t57928,plain,
sFlat2 = join(meet(sk1,composition(top,sFlat3)),composition(sFlat1,meet(sk1,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t57927,t14590]) ).
cnf(t57929,plain,
sFlat2 = join(sk1,composition(sFlat1,meet(sk1,composition(converse(top),sk1)))),
inference(step,[status(thm)],[t57928,t55492]) ).
cnf(t57930,plain,
sFlat2 = join(sk1,composition(sFlat1,meet(sk1,composition(top,sk1)))),
inference(step,[status(thm)],[t57929,t825]) ).
cnf(t57931,plain,
sFlat2 = join(sk1,composition(sFlat1,meet(sk1,composition(top,sFlat3)))),
inference(step,[status(thm)],[t57930,t14590]) ).
cnf(t57932,plain,
sFlat2 = join(sk1,composition(sFlat1,sk1)),
inference(step,[status(thm)],[t57931,t55492]) ).
cnf(t57933,plain,
sFlat2 = join(sk1,sFlat2),
inference(step,[status(thm)],[t57932,t266]) ).
cnf(t57934,plain,
sFlat2 = join(sFlat2,sk1),
inference(step,[status(thm)],[t57933,t70]) ).
cnf(t57935,plain,
sFlat2 = sFlat3,
inference(step,[status(thm)],[t57934,t220]) ).
cnf(t56084,plain,
sFlat3 = sFlat2,
inference(orient,[status(thm)],[t57935]) ).
cnf(t57936,plain,
join(sFlat2,sk1) = sFlat2,
inference(step,[status(thm)],[t220,t56084]) ).
cnf(t56085,plain,
join(sFlat2,sk1) = sFlat2,
inference(orient,[status(thm)],[t57936]) ).
cnf(goal_0,negated_conjecture,
join(sk1,composition(composition(sk1,converse(sk1)),sk1)) != composition(composition(sk1,converse(sk1)),sk1),
file('/export/starexec/sandbox/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,t25]) ).
cnf(g0_1,plain,
join(sk1,composition(sk1,composition(sFlat0,sk1))) != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[g0_0,t60]) ).
cnf(g0_2,plain,
join(sk1,composition(sFlat1,sk1)) != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[g0_1,t502]) ).
cnf(g0_3,plain,
join(sk1,sFlat2) != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[g0_2,t266]) ).
cnf(g0_4,plain,
join(sFlat2,sk1) != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[g0_3,t70]) ).
cnf(g0_5,plain,
sFlat2 != composition(composition(sk1,converse(sk1)),sk1),
inference(rw,[status(thm)],[g0_4,t56085]) ).
cnf(g0_6,plain,
sFlat2 != composition(sk1,composition(converse(sk1),sk1)),
inference(rw,[status(thm)],[g0_5,t25]) ).
cnf(g0_7,plain,
sFlat2 != composition(sk1,composition(sFlat0,sk1)),
inference(rw,[status(thm)],[g0_6,t60]) ).
cnf(g0_8,plain,
sFlat2 != composition(sFlat1,sk1),
inference(rw,[status(thm)],[g0_7,t502]) ).
cnf(g0_9,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_8,t266]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL045-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/10.39 % Computer : n016.cluster.edu
% 0.11/10.39 % Model : x86_64 x86_64
% 0.11/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.39 % Memory : 8046.5625MB
% 0.11/10.39 % OS : Linux 6.8.0-71-generic
% 0.11/10.39 % CPULimit : 300
% 0.11/10.39 % WCLimit : 300
% 0.11/10.39 % DateTime : Thu Sep 24 07:41:56 UTC 2026
% 0.11/10.39 % CPUTime :
% 0.11/10.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 156.54/30.28 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 156.54/30.28 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------