%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL025-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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:34:51 PM UTC 2026
% Result : Unsatisfiable 61.41s 8.48s
% Output : CNFRefutation 61.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 16
% Syntax : Number of clauses : 242 ( 242 unt; 0 nHn; 82 RR)
% Number of literals : 242 ( 241 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 243 ( 8 sgn)
% Comments :
%------------------------------------------------------------------------------
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(t14,axiom,
sF1 = converse(sk1),
introduced(definition) ).
cnf(t15,plain,
converse(sk1) = sF1,
inference(orient,[status(thm)],[t14]) ).
cnf(t59,plain,
converse(join(X1,sk1)) = join(converse(X1),sF1),
inference(cp,[status(thm)],[t57,t15]) ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t34,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t30901,plain,
converse(join(X1,sk1)) = join(sF1,converse(X1)),
inference(step,[status(thm)],[t59,t34]) ).
cnf(t85,plain,
converse(join(X1,sk1)) = join(sF1,converse(X1)),
inference(orient,[status(thm)],[t30901]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30913,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t12,t34]) ).
cnf(t252,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t30913]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30910,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t34]) ).
cnf(t194,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t30910]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,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(t17,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t31,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t27,t17]) ).
cnf(t141,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(t16,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t13,axiom,
sF0 = join(sk1,one),
introduced(definition) ).
cnf(t2,axiom,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t30893,plain,
sF0 = one,
inference(step,[status(thm)],[t13,t20]) ).
cnf(t21,plain,
one = sF0,
inference(orient,[status(thm)],[t30893]) ).
cnf(t30894,plain,
composition(X1,sF0) = X1,
inference(step,[status(thm)],[t16,t21]) ).
cnf(t22,plain,
composition(X1,sF0) = X1,
inference(rw,[status(thm)],[t30894]) ).
cnf(t24,plain,
composition(X1,sF0) = X1,
inference(orient,[status(thm)],[t22]) ).
cnf(t142,plain,
composition(converse(sF0),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t141,t24]) ).
cnf(t30903,plain,
composition(converse(sF0),X1) = X1,
inference(step,[status(thm)],[t142,t17]) ).
cnf(t149,plain,
composition(converse(sF0),X1) = X1,
inference(orient,[status(thm)],[t30903]) ).
cnf(t152,plain,
sF0 = converse(sF0),
inference(cp,[status(thm)],[t149,t24]) ).
cnf(t153,plain,
converse(sF0) = sF0,
inference(orient,[status(thm)],[t152]) ).
cnf(t213,plain,
complement(X1) = join(complement(X1),composition(sF0,complement(composition(sF0,X1)))),
inference(cp,[status(thm)],[t194,t153]) ).
cnf(t30906,plain,
composition(sF0,X1) = X1,
inference(step,[status(thm)],[t149,t153]) ).
cnf(t155,plain,
composition(sF0,X1) = X1,
inference(rw,[status(thm)],[t30906]) ).
cnf(t170,plain,
composition(sF0,X1) = X1,
inference(orient,[status(thm)],[t155]) ).
cnf(t30916,plain,
complement(X1) = join(complement(X1),complement(composition(sF0,X1))),
inference(step,[status(thm)],[t213,t170]) ).
cnf(t30917,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t30916,t170]) ).
cnf(t298,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t30917]) ).
cnf(t301,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t252,t298]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t30926,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t301,t26]) ).
cnf(t30927,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t30926,t34]) ).
cnf(u0,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t5,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t30899,plain,
complement(top) = zero,
inference(step,[status(thm)],[t5,t26]) ).
cnf(t73,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t30899]) ).
cnf(t30928,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t30927,t73]) ).
cnf(t372,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t30928]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t117,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t299,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t298,t73]) ).
cnf(t30918,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t299,t73]) ).
cnf(t30919,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t30918,t73]) ).
cnf(t303,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t30919]) ).
cnf(t304,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t117,t303]) ).
cnf(t375,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t304]) ).
cnf(t378,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t375,t372]) ).
cnf(t30929,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t378,t372]) ).
cnf(t379,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t30929]) ).
cnf(t30934,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t372,t379]) ).
cnf(t384,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t30934]) ).
cnf(t399,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t384]) ).
cnf(t402,plain,
complement(X1) = join(complement(join(X1,X2)),complement(join(complement(complement(X1)),complement(X2)))),
inference(cp,[status(thm)],[t252,t399]) ).
cnf(t31356,plain,
complement(X1) = join(complement(join(X1,X2)),complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t402,t399]) ).
cnf(t19507,plain,
join(complement(join(X1,X2)),complement(join(X1,complement(X2)))) = complement(X1),
inference(orient,[status(thm)],[t31356]) ).
cnf(t119,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t117,t26]) ).
cnf(t403,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t298,t399]) ).
cnf(t30938,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t403,t399]) ).
cnf(t30939,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t30938,t399]) ).
cnf(t410,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t30939]) ).
cnf(t414,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t117,t410]) ).
cnf(t565,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t414]) ).
cnf(t566,plain,
join(X1,complement(X1)) = join(X1,top),
inference(cp,[status(thm)],[t565,t26]) ).
cnf(t30961,plain,
top = join(X1,top),
inference(step,[status(thm)],[t566,t26]) ).
cnf(t602,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t30961]) ).
cnf(t608,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t602,t34]) ).
cnf(t611,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t608]) ).
cnf(t30993,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t119,t611]) ).
cnf(t856,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t30993]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t159,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t171,plain,
composition(join(sF0,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t159,t170]) ).
cnf(t6833,plain,
composition(join(sF0,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t171]) ).
cnf(t6849,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t6833,t602]) ).
cnf(t7110,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t6849]) ).
cnf(t7120,plain,
top = join(X1,composition(top,complement(X1))),
inference(cp,[status(thm)],[t856,t7110]) ).
cnf(t8130,plain,
join(X1,composition(top,complement(X1))) = top,
inference(orient,[status(thm)],[t7120]) ).
cnf(t8133,plain,
top = join(complement(X1),composition(top,X1)),
inference(cp,[status(thm)],[t8130,t399]) ).
cnf(t8734,plain,
join(complement(X1),composition(top,X1)) = top,
inference(orient,[status(thm)],[t8133]) ).
cnf(t29,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sF1),
inference(cp,[status(thm)],[t27,t15]) ).
cnf(t43,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sF1),
inference(orient,[status(thm)],[t29]) ).
cnf(t67,plain,
converse(join(composition(sk1,X1),X2)) = join(composition(converse(X1),sF1),converse(X2)),
inference(cp,[status(thm)],[t57,t43]) ).
cnf(t811,plain,
join(composition(converse(X1),sF1),converse(X2)) = converse(join(composition(sk1,X1),X2)),
inference(orient,[status(thm)],[t67]) ).
cnf(t60,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t57,t17]) ).
cnf(t217,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t60]) ).
cnf(t610,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t217,t602]) ).
cnf(t620,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t610]) ).
cnf(t624,plain,
converse(top) = top,
inference(cp,[status(thm)],[t620,t611]) ).
cnf(t627,plain,
converse(top) = top,
inference(orient,[status(thm)],[t624]) ).
cnf(t849,plain,
converse(join(composition(sk1,top),X1)) = join(composition(top,sF1),converse(X1)),
inference(cp,[status(thm)],[t811,t627]) ).
cnf(t1706,plain,
converse(join(composition(sk1,top),X1)) = join(composition(top,sF1),converse(X1)),
inference(orient,[status(thm)],[t849]) ).
cnf(t23,plain,
join(sk1,sF0) = one,
inference(rw,[status(thm)],[t20]) ).
cnf(t30895,plain,
join(sk1,sF0) = sF0,
inference(step,[status(thm)],[t23,t21]) ).
cnf(t25,plain,
join(sk1,sF0) = sF0,
inference(orient,[status(thm)],[t30895]) ).
cnf(t30896,plain,
join(sF0,sk1) = sF0,
inference(step,[status(thm)],[t25,t34]) ).
cnf(t35,plain,
join(sF0,sk1) = sF0,
inference(rw,[status(thm)],[t30896]) ).
cnf(t37,plain,
join(sF0,sk1) = sF0,
inference(orient,[status(thm)],[t35]) ).
cnf(t86,plain,
join(sF1,converse(sF0)) = converse(sF0),
inference(cp,[status(thm)],[t85,t37]) ).
cnf(t107,plain,
join(sF1,converse(sF0)) = converse(sF0),
inference(orient,[status(thm)],[t86]) ).
cnf(t154,plain,
join(sF1,sF0) = converse(sF0),
inference(rw,[status(thm)],[t107]) ).
cnf(t30907,plain,
join(sF0,sF1) = converse(sF0),
inference(step,[status(thm)],[t154,t34]) ).
cnf(t30908,plain,
join(sF0,sF1) = sF0,
inference(step,[status(thm)],[t30907,t153]) ).
cnf(t166,plain,
join(sF0,sF1) = sF0,
inference(orient,[status(thm)],[t30908]) ).
cnf(t6837,plain,
join(X1,composition(sF1,X1)) = composition(sF0,X1),
inference(cp,[status(thm)],[t6833,t166]) ).
cnf(t31087,plain,
join(X1,composition(sF1,X1)) = X1,
inference(step,[status(thm)],[t6837,t170]) ).
cnf(t6983,plain,
join(X1,composition(sF1,X1)) = X1,
inference(orient,[status(thm)],[t31087]) ).
cnf(t6990,plain,
join(X1,join(composition(sF1,X1),X2)) = join(X1,X2),
inference(cp,[status(thm)],[t117,t6983]) ).
cnf(t15983,plain,
join(X1,join(composition(sF1,X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t6990]) ).
cnf(t148,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t57,t141]) ).
cnf(t4899,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t148]) ).
cnf(t160,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t159,t27]) ).
cnf(t5551,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t160]) ).
cnf(t5634,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)],[t4899,t5551]) ).
cnf(t31233,plain,
join(composition(X1,X2),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t5634,t17]) ).
cnf(t31234,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t31233,t17]) ).
cnf(t30,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t27,t17]) ).
cnf(t128,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t30]) ).
cnf(t31235,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,converse(join(converse(X2),converse(X3)))),
inference(step,[status(thm)],[t31234,t128]) ).
cnf(t31236,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t31235,t217]) ).
cnf(t31237,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t31236,t17]) ).
cnf(t11994,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t31237]) ).
cnf(t16015,plain,
join(X1,composition(sF1,X2)) = join(X1,composition(sF1,join(X1,X2))),
inference(cp,[status(thm)],[t15983,t11994]) ).
cnf(t30007,plain,
join(X1,composition(sF1,join(X1,X2))) = join(X1,composition(sF1,X2)),
inference(orient,[status(thm)],[t16015]) ).
cnf(t30009,plain,
join(X1,composition(sF1,complement(X1))) = join(X1,composition(sF1,top)),
inference(cp,[status(thm)],[t30007,t26]) ).
cnf(t30257,plain,
join(X1,composition(sF1,complement(X1))) = join(X1,composition(sF1,top)),
inference(orient,[status(thm)],[t30009]) ).
cnf(t30281,plain,
join(composition(top,sF1),converse(composition(sF1,complement(composition(sk1,top))))) = converse(join(composition(sk1,top),composition(sF1,top))),
inference(cp,[status(thm)],[t1706,t30257]) ).
cnf(t18,plain,
sk1 = converse(sF1),
inference(cp,[status(thm)],[t17,t15]) ).
cnf(t19,plain,
converse(sF1) = sk1,
inference(orient,[status(thm)],[t18]) ).
cnf(t33,plain,
converse(composition(sF1,X1)) = composition(converse(X1),sk1),
inference(cp,[status(thm)],[t27,t19]) ).
cnf(t51,plain,
converse(composition(sF1,X1)) = composition(converse(X1),sk1),
inference(orient,[status(thm)],[t33]) ).
cnf(t31593,plain,
join(composition(top,sF1),composition(converse(complement(composition(sk1,top))),sk1)) = converse(join(composition(sk1,top),composition(sF1,top))),
inference(step,[status(thm)],[t30281,t51]) ).
cnf(t205,plain,
complement(top) = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(cp,[status(thm)],[t194,t73]) ).
cnf(t31172,plain,
zero = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(step,[status(thm)],[t205,t73]) ).
cnf(t31173,plain,
zero = composition(converse(X1),complement(composition(X1,top))),
inference(step,[status(thm)],[t31172,t379]) ).
cnf(t8411,plain,
composition(converse(X1),complement(composition(X1,top))) = zero,
inference(orient,[status(thm)],[t31173]) ).
cnf(t8471,plain,
composition(converse(complement(composition(X1,top))),X1) = converse(zero),
inference(cp,[status(thm)],[t141,t8411]) ).
cnf(t61,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t57,t17]) ).
cnf(t231,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t61]) ).
cnf(t391,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t231,t379]) ).
cnf(t30947,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t391,t17]) ).
cnf(t450,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t30947]) ).
cnf(t387,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t379,t34]) ).
cnf(t404,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t387]) ).
cnf(t452,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t450,t404]) ).
cnf(t455,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t452]) ).
cnf(t31421,plain,
composition(converse(complement(composition(X1,top))),X1) = zero,
inference(step,[status(thm)],[t8471,t455]) ).
cnf(t21647,plain,
composition(converse(complement(composition(X1,top))),X1) = zero,
inference(orient,[status(thm)],[t31421]) ).
cnf(t31594,plain,
join(composition(top,sF1),zero) = converse(join(composition(sk1,top),composition(sF1,top))),
inference(step,[status(thm)],[t31593,t21647]) ).
cnf(t31595,plain,
composition(top,sF1) = converse(join(composition(sk1,top),composition(sF1,top))),
inference(step,[status(thm)],[t31594,t404]) ).
cnf(t31596,plain,
composition(top,sF1) = join(composition(top,sF1),converse(composition(sF1,top))),
inference(step,[status(thm)],[t31595,t1706]) ).
cnf(t31597,plain,
composition(top,sF1) = join(composition(top,sF1),composition(converse(top),sk1)),
inference(step,[status(thm)],[t31596,t51]) ).
cnf(t31598,plain,
composition(top,sF1) = join(composition(top,sF1),composition(top,sk1)),
inference(step,[status(thm)],[t31597,t627]) ).
cnf(t31599,plain,
composition(top,sF1) = composition(top,join(sF1,sk1)),
inference(step,[status(thm)],[t31598,t11994]) ).
cnf(t71,plain,
converse(join(composition(sF1,X1),X2)) = join(composition(converse(X1),sk1),converse(X2)),
inference(cp,[status(thm)],[t57,t51]) ).
cnf(t1376,plain,
join(composition(converse(X1),sk1),converse(X2)) = converse(join(composition(sF1,X1),X2)),
inference(orient,[status(thm)],[t71]) ).
cnf(t1412,plain,
converse(join(composition(sF1,top),X1)) = join(composition(top,sk1),converse(X1)),
inference(cp,[status(thm)],[t1376,t627]) ).
cnf(t2717,plain,
converse(join(composition(sF1,top),X1)) = join(composition(top,sk1),converse(X1)),
inference(orient,[status(thm)],[t1412]) ).
cnf(t6836,plain,
join(X1,composition(sk1,X1)) = composition(sF0,X1),
inference(cp,[status(thm)],[t6833,t37]) ).
cnf(t31084,plain,
join(X1,composition(sk1,X1)) = X1,
inference(step,[status(thm)],[t6836,t170]) ).
cnf(t6912,plain,
join(X1,composition(sk1,X1)) = X1,
inference(orient,[status(thm)],[t31084]) ).
cnf(t6919,plain,
join(X1,join(composition(sk1,X1),X2)) = join(X1,X2),
inference(cp,[status(thm)],[t117,t6912]) ).
cnf(t15221,plain,
join(X1,join(composition(sk1,X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t6919]) ).
cnf(t15253,plain,
join(X1,composition(sk1,X2)) = join(X1,composition(sk1,join(X1,X2))),
inference(cp,[status(thm)],[t15221,t11994]) ).
cnf(t26732,plain,
join(X1,composition(sk1,join(X1,X2))) = join(X1,composition(sk1,X2)),
inference(orient,[status(thm)],[t15253]) ).
cnf(t26734,plain,
join(X1,composition(sk1,complement(X1))) = join(X1,composition(sk1,top)),
inference(cp,[status(thm)],[t26732,t26]) ).
cnf(t26962,plain,
join(X1,composition(sk1,complement(X1))) = join(X1,composition(sk1,top)),
inference(orient,[status(thm)],[t26734]) ).
cnf(t26992,plain,
join(composition(top,sk1),converse(composition(sk1,complement(composition(sF1,top))))) = converse(join(composition(sF1,top),composition(sk1,top))),
inference(cp,[status(thm)],[t2717,t26962]) ).
cnf(t31545,plain,
join(composition(top,sk1),composition(converse(complement(composition(sF1,top))),sF1)) = converse(join(composition(sF1,top),composition(sk1,top))),
inference(step,[status(thm)],[t26992,t43]) ).
cnf(t31546,plain,
join(composition(top,sk1),zero) = converse(join(composition(sF1,top),composition(sk1,top))),
inference(step,[status(thm)],[t31545,t21647]) ).
cnf(t31547,plain,
composition(top,sk1) = converse(join(composition(sF1,top),composition(sk1,top))),
inference(step,[status(thm)],[t31546,t404]) ).
cnf(t68,plain,
converse(join(X1,composition(sk1,X2))) = join(converse(X1),composition(converse(X2),sF1)),
inference(cp,[status(thm)],[t57,t43]) ).
cnf(t1012,plain,
join(converse(X1),composition(converse(X2),sF1)) = converse(join(X1,composition(sk1,X2))),
inference(orient,[status(thm)],[t68]) ).
cnf(t1041,plain,
converse(join(X1,composition(sk1,top))) = join(converse(X1),composition(top,sF1)),
inference(cp,[status(thm)],[t1012,t627]) ).
cnf(t2196,plain,
converse(join(X1,composition(sk1,top))) = join(converse(X1),composition(top,sF1)),
inference(orient,[status(thm)],[t1041]) ).
cnf(t31548,plain,
composition(top,sk1) = join(converse(composition(sF1,top)),composition(top,sF1)),
inference(step,[status(thm)],[t31547,t2196]) ).
cnf(t31549,plain,
composition(top,sk1) = join(composition(top,sF1),converse(composition(sF1,top))),
inference(step,[status(thm)],[t31548,t34]) ).
cnf(t31550,plain,
composition(top,sk1) = join(composition(top,sF1),composition(converse(top),sk1)),
inference(step,[status(thm)],[t31549,t51]) ).
cnf(t31551,plain,
composition(top,sk1) = join(composition(top,sF1),composition(top,sk1)),
inference(step,[status(thm)],[t31550,t627]) ).
cnf(t31552,plain,
composition(top,sk1) = composition(top,join(sF1,sk1)),
inference(step,[status(thm)],[t31551,t11994]) ).
cnf(t27184,plain,
composition(top,join(sF1,sk1)) = composition(top,sk1),
inference(orient,[status(thm)],[t31552]) ).
cnf(t31600,plain,
composition(top,sF1) = composition(top,sk1),
inference(step,[status(thm)],[t31599,t27184]) ).
cnf(t30353,plain,
composition(top,sk1) = composition(top,sF1),
inference(orient,[status(thm)],[t31600]) ).
cnf(t30391,plain,
top = join(complement(sk1),composition(top,sF1)),
inference(cp,[status(thm)],[t8734,t30353]) ).
cnf(t121,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t117,t34]) ).
cnf(t31041,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t121,t117]) ).
cnf(t3971,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t31041]) ).
cnf(t6920,plain,
join(X1,converse(composition(sk1,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t217,t6912]) ).
cnf(t31113,plain,
join(X1,composition(converse(converse(X1)),sF1)) = converse(converse(X1)),
inference(step,[status(thm)],[t6920,t43]) ).
cnf(t31114,plain,
join(X1,composition(X1,sF1)) = converse(converse(X1)),
inference(step,[status(thm)],[t31113,t17]) ).
cnf(t31115,plain,
join(X1,composition(X1,sF1)) = X1,
inference(step,[status(thm)],[t31114,t17]) ).
cnf(t7279,plain,
join(X1,composition(X1,sF1)) = X1,
inference(orient,[status(thm)],[t31115]) ).
cnf(t7292,plain,
join(X1,join(X2,composition(X1,sF1))) = join(X2,X1),
inference(cp,[status(thm)],[t3971,t7279]) ).
cnf(t17940,plain,
join(X1,join(X2,composition(X1,sF1))) = join(X2,X1),
inference(orient,[status(thm)],[t7292]) ).
cnf(t122,plain,
join(sF0,join(sk1,X1)) = join(sF0,X1),
inference(cp,[status(thm)],[t117,t37]) ).
cnf(t267,plain,
join(sF0,join(sk1,X1)) = join(sF0,X1),
inference(orient,[status(thm)],[t122]) ).
cnf(t268,plain,
join(sF0,complement(sk1)) = join(sF0,top),
inference(cp,[status(thm)],[t267,t26]) ).
cnf(t272,plain,
join(sF0,complement(sk1)) = join(sF0,top),
inference(orient,[status(thm)],[t268]) ).
cnf(t30962,plain,
join(sF0,complement(sk1)) = top,
inference(step,[status(thm)],[t272,t602]) ).
cnf(t603,plain,
join(sF0,complement(sk1)) = top,
inference(orient,[status(thm)],[t30962]) ).
cnf(t6839,plain,
join(X1,composition(complement(sk1),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t6833,t603]) ).
cnf(t7530,plain,
join(X1,composition(complement(sk1),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t6839]) ).
cnf(t17966,plain,
join(sF1,complement(sk1)) = join(complement(sk1),composition(top,sF1)),
inference(cp,[status(thm)],[t17940,t7530]) ).
cnf(t18236,plain,
join(complement(sk1),composition(top,sF1)) = join(sF1,complement(sk1)),
inference(orient,[status(thm)],[t17966]) ).
cnf(t31638,plain,
top = join(sF1,complement(sk1)),
inference(step,[status(thm)],[t30391,t18236]) ).
cnf(t30531,plain,
join(sF1,complement(sk1)) = top,
inference(orient,[status(thm)],[t31638]) ).
cnf(t30551,plain,
complement(sF1) = join(complement(top),complement(join(sF1,complement(complement(sk1))))),
inference(cp,[status(thm)],[t19507,t30531]) ).
cnf(t31643,plain,
complement(sF1) = join(zero,complement(join(sF1,complement(complement(sk1))))),
inference(step,[status(thm)],[t30551,t73]) ).
cnf(t31644,plain,
complement(sF1) = complement(join(sF1,complement(complement(sk1)))),
inference(step,[status(thm)],[t31643,t379]) ).
cnf(t31645,plain,
complement(sF1) = complement(join(sF1,sk1)),
inference(step,[status(thm)],[t31644,t399]) ).
cnf(t30557,plain,
complement(join(sF1,sk1)) = complement(sF1),
inference(orient,[status(thm)],[t31645]) ).
cnf(t30560,plain,
join(sF1,sk1) = complement(complement(sF1)),
inference(cp,[status(thm)],[t399,t30557]) ).
cnf(t31646,plain,
join(sF1,sk1) = sF1,
inference(step,[status(thm)],[t30560,t399]) ).
cnf(t30593,plain,
join(sF1,sk1) = sF1,
inference(orient,[status(thm)],[t31646]) ).
cnf(t30600,plain,
join(sF1,converse(sF1)) = converse(sF1),
inference(cp,[status(thm)],[t85,t30593]) ).
cnf(t31650,plain,
join(sF1,sk1) = converse(sF1),
inference(step,[status(thm)],[t30600,t19]) ).
cnf(t31651,plain,
sF1 = converse(sF1),
inference(step,[status(thm)],[t31650,t30593]) ).
cnf(t31652,plain,
sF1 = sk1,
inference(step,[status(thm)],[t31651,t19]) ).
cnf(t30630,plain,
sk1 = sF1,
inference(orient,[status(thm)],[t31652]) ).
cnf(t31653,plain,
converse(sF1) = sF1,
inference(step,[status(thm)],[t19,t30630]) ).
cnf(t30632,plain,
converse(sF1) = sF1,
inference(orient,[status(thm)],[t31653]) ).
cnf(goal_0,negated_conjecture,
converse(sk1) != sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
converse(sF1) != sk1,
inference(rw,[status(thm)],[goal_0,t30630]) ).
cnf(g0_1,plain,
sF1 != sk1,
inference(rw,[status(thm)],[g0_0,t30632]) ).
cnf(g0_2,plain,
sF1 != sF1,
inference(rw,[status(thm)],[g0_1,t30630]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL025-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 07:15:30 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 61.41/8.48 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.41/8.48 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------