%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL028-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 : n007.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:17 PM UTC 2026
% Result : Unsatisfiable 32.36s 4.55s
% Output : CNFRefutation 32.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 22
% Syntax : Number of clauses : 294 ( 294 unt; 0 nHn; 152 RR)
% Number of literals : 294 ( 293 equ; 7 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 : 17 ( 17 usr; 12 con; 0-2 aty)
% Number of variables : 190 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t16,axiom,
sF2 = complement(sk1),
introduced(definition) ).
cnf(t21,plain,
complement(sk1) = sF2,
inference(orient,[status(thm)],[t16]) ).
cnf(t17,axiom,
sF3 = complement(sk2),
introduced(definition) ).
cnf(t22,plain,
complement(sk2) = sF3,
inference(orient,[status(thm)],[t17]) ).
cnf(t18,axiom,
sF4 = join(complement(sk1),complement(sk2)),
introduced(definition) ).
cnf(t61459,plain,
sF4 = join(sF2,complement(sk2)),
inference(step,[status(thm)],[t18,t21]) ).
cnf(t61460,plain,
sF4 = join(sF2,sF3),
inference(step,[status(thm)],[t61459,t22]) ).
cnf(t61,plain,
join(sF2,sF3) = sF4,
inference(orient,[status(thm)],[t61460]) ).
cnf(t19,axiom,
sF5 = complement(join(complement(sk1),complement(sk2))),
introduced(definition) ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t68,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t61483,plain,
sF5 = complement(join(complement(sk2),complement(sk1))),
inference(step,[status(thm)],[t19,t68]) ).
cnf(t61484,plain,
sF5 = complement(join(sF3,complement(sk1))),
inference(step,[status(thm)],[t61483,t22]) ).
cnf(t61485,plain,
sF5 = complement(join(sF3,sF2)),
inference(step,[status(thm)],[t61484,t21]) ).
cnf(t61486,plain,
sF5 = complement(join(sF2,sF3)),
inference(step,[status(thm)],[t61485,t68]) ).
cnf(t61487,plain,
sF5 = complement(sF4),
inference(step,[status(thm)],[t61486,t61]) ).
cnf(t254,plain,
complement(sF4) = sF5,
inference(orient,[status(thm)],[t61487]) ).
cnf(t20,axiom,
sF6 = composition(sk1,sk2),
introduced(definition) ).
cnf(t32,plain,
composition(sk1,sk2) = sF6,
inference(orient,[status(thm)],[t20]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t61479,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t13,t68]) ).
cnf(t213,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t61479]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t61472,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t68]) ).
cnf(t168,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t61472]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t43,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t45,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t43,t24]) ).
cnf(t95,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t45]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t14,axiom,
sF0 = join(sk1,one),
introduced(definition) ).
cnf(t2,axiom,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t61451,plain,
sF0 = one,
inference(step,[status(thm)],[t14,t25]) ).
cnf(t27,plain,
one = sF0,
inference(orient,[status(thm)],[t61451]) ).
cnf(t61452,plain,
composition(X1,sF0) = X1,
inference(step,[status(thm)],[t23,t27]) ).
cnf(t28,plain,
composition(X1,sF0) = X1,
inference(rw,[status(thm)],[t61452]) ).
cnf(t33,plain,
composition(X1,sF0) = X1,
inference(orient,[status(thm)],[t28]) ).
cnf(t96,plain,
composition(converse(sF0),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t95,t33]) ).
cnf(t61467,plain,
composition(converse(sF0),X1) = X1,
inference(step,[status(thm)],[t96,t24]) ).
cnf(t99,plain,
composition(converse(sF0),X1) = X1,
inference(orient,[status(thm)],[t61467]) ).
cnf(t100,plain,
sF0 = converse(sF0),
inference(cp,[status(thm)],[t99,t33]) ).
cnf(t101,plain,
converse(sF0) = sF0,
inference(orient,[status(thm)],[t100]) ).
cnf(t180,plain,
complement(X1) = join(complement(X1),composition(sF0,complement(composition(sF0,X1)))),
inference(cp,[status(thm)],[t168,t101]) ).
cnf(t61468,plain,
composition(sF0,X1) = X1,
inference(step,[status(thm)],[t99,t101]) ).
cnf(t102,plain,
composition(sF0,X1) = X1,
inference(rw,[status(thm)],[t61468]) ).
cnf(t106,plain,
composition(sF0,X1) = X1,
inference(orient,[status(thm)],[t102]) ).
cnf(t61495,plain,
complement(X1) = join(complement(X1),complement(composition(sF0,X1))),
inference(step,[status(thm)],[t180,t106]) ).
cnf(t61496,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t61495,t106]) ).
cnf(t309,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t61496]) ).
cnf(t315,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t213,t309]) ).
cnf(t4,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t34,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t61585,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t315,t34]) ).
cnf(t61586,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t61585,t68]) ).
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(t6,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t61465,plain,
complement(top) = zero,
inference(step,[status(thm)],[t6,t34]) ).
cnf(t90,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t61465]) ).
cnf(t61587,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t61586,t90]) ).
cnf(t879,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t61587]) ).
cnf(t883,plain,
sF4 = join(zero,complement(sF5)),
inference(cp,[status(thm)],[t879,t254]) ).
cnf(t903,plain,
join(zero,complement(sF5)) = sF4,
inference(orient,[status(thm)],[t883]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t53,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t312,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t309,t90]) ).
cnf(t61501,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t312,t90]) ).
cnf(t61502,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t61501,t90]) ).
cnf(t323,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t61502]) ).
cnf(t324,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t53,t323]) ).
cnf(t956,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t324]) ).
cnf(t960,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t956,t879]) ).
cnf(t61588,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t960,t879]) ).
cnf(t962,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t61588]) ).
cnf(t61593,plain,
complement(sF5) = sF4,
inference(step,[status(thm)],[t903,t962]) ).
cnf(t967,plain,
complement(sF5) = sF4,
inference(rw,[status(thm)],[t61593]) ).
cnf(t990,plain,
complement(sF5) = sF4,
inference(orient,[status(thm)],[t967]) ).
cnf(t993,plain,
sF5 = join(complement(join(sF4,X1)),complement(join(complement(sF5),complement(X1)))),
inference(cp,[status(thm)],[t213,t990]) ).
cnf(t62788,plain,
sF5 = join(complement(join(sF4,X1)),complement(join(sF4,complement(X1)))),
inference(step,[status(thm)],[t993,t990]) ).
cnf(t61027,plain,
join(complement(join(sF4,X1)),complement(join(sF4,complement(X1)))) = sF5,
inference(orient,[status(thm)],[t62788]) ).
cnf(t62,plain,
join(sF2,join(sF3,X1)) = join(sF4,X1),
inference(cp,[status(thm)],[t53,t61]) ).
cnf(t160,plain,
join(sF2,join(sF3,X1)) = join(sF4,X1),
inference(orient,[status(thm)],[t62]) ).
cnf(t61590,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t879,t962]) ).
cnf(t964,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t61590]) ).
cnf(t1026,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t964]) ).
cnf(t217,plain,
X1 = join(complement(join(complement(X1),sk2)),complement(join(complement(X1),sF3))),
inference(cp,[status(thm)],[t213,t22]) ).
cnf(t61802,plain,
X1 = join(complement(join(complement(X1),sF3)),complement(join(complement(X1),sk2))),
inference(step,[status(thm)],[t217,t68]) ).
cnf(t61803,plain,
X1 = join(complement(join(sF3,complement(X1))),complement(join(complement(X1),sk2))),
inference(step,[status(thm)],[t61802,t68]) ).
cnf(t61804,plain,
X1 = join(complement(join(sF3,complement(X1))),complement(join(sk2,complement(X1)))),
inference(step,[status(thm)],[t61803,t68]) ).
cnf(t4568,plain,
join(complement(join(sF3,complement(X1))),complement(join(sk2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t61804]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t126,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t128,plain,
composition(join(X1,sk1),sk2) = join(composition(X1,sk2),sF6),
inference(cp,[status(thm)],[t126,t32]) ).
cnf(t61488,plain,
composition(join(X1,sk1),sk2) = join(sF6,composition(X1,sk2)),
inference(step,[status(thm)],[t128,t68]) ).
cnf(t262,plain,
composition(join(X1,sk1),sk2) = join(sF6,composition(X1,sk2)),
inference(orient,[status(thm)],[t61488]) ).
cnf(t29,plain,
join(sk1,sF0) = one,
inference(rw,[status(thm)],[t25]) ).
cnf(t61454,plain,
join(sk1,sF0) = sF0,
inference(step,[status(thm)],[t29,t27]) ).
cnf(t37,plain,
join(sk1,sF0) = sF0,
inference(orient,[status(thm)],[t61454]) ).
cnf(t61462,plain,
join(sF0,sk1) = sF0,
inference(step,[status(thm)],[t37,t68]) ).
cnf(t70,plain,
join(sF0,sk1) = sF0,
inference(rw,[status(thm)],[t61462]) ).
cnf(t81,plain,
join(sF0,sk1) = sF0,
inference(orient,[status(thm)],[t70]) ).
cnf(t264,plain,
join(sF6,composition(sF0,sk2)) = composition(sF0,sk2),
inference(cp,[status(thm)],[t262,t81]) ).
cnf(t61489,plain,
join(sF6,sk2) = composition(sF0,sk2),
inference(step,[status(thm)],[t264,t106]) ).
cnf(t61490,plain,
join(sF6,sk2) = sk2,
inference(step,[status(thm)],[t61489,t106]) ).
cnf(t269,plain,
join(sF6,sk2) = sk2,
inference(orient,[status(thm)],[t61490]) ).
cnf(t271,plain,
join(sF6,join(sk2,X1)) = join(sk2,X1),
inference(cp,[status(thm)],[t53,t269]) ).
cnf(t786,plain,
join(sF6,join(sk2,X1)) = join(sk2,X1),
inference(orient,[status(thm)],[t271]) ).
cnf(t788,plain,
join(sk2,X1) = join(sF6,join(X1,sk2)),
inference(cp,[status(thm)],[t786,t68]) ).
cnf(t1408,plain,
join(sF6,join(X1,sk2)) = join(sk2,X1),
inference(orient,[status(thm)],[t788]) ).
cnf(t56,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t53,t34]) ).
cnf(t394,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t56]) ).
cnf(t55,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t53,t34]) ).
cnf(t327,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t55]) ).
cnf(t350,plain,
top = join(complement(X1),join(complement(X1),complement(complement(X1)))),
inference(cp,[status(thm)],[t327,t309]) ).
cnf(t61522,plain,
top = join(complement(X1),top),
inference(step,[status(thm)],[t350,t34]) ).
cnf(t61523,plain,
top = join(top,complement(X1)),
inference(step,[status(thm)],[t61522,t68]) ).
cnf(t415,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t61523]) ).
cnf(t422,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t327,t415]) ).
cnf(t440,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t422]) ).
cnf(t448,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t440,t68]) ).
cnf(t461,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t448]) ).
cnf(t61537,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t394,t461]) ).
cnf(t469,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t61537]) ).
cnf(t1414,plain,
join(sk2,complement(sF6)) = top,
inference(cp,[status(thm)],[t1408,t469]) ).
cnf(t1420,plain,
join(sk2,complement(sF6)) = top,
inference(orient,[status(thm)],[t1414]) ).
cnf(t4577,plain,
sF6 = join(complement(join(sF3,complement(sF6))),complement(top)),
inference(cp,[status(thm)],[t4568,t1420]) ).
cnf(t61815,plain,
sF6 = join(complement(top),complement(join(sF3,complement(sF6)))),
inference(step,[status(thm)],[t4577,t68]) ).
cnf(t61816,plain,
sF6 = join(zero,complement(join(sF3,complement(sF6)))),
inference(step,[status(thm)],[t61815,t90]) ).
cnf(t61817,plain,
sF6 = complement(join(sF3,complement(sF6))),
inference(step,[status(thm)],[t61816,t962]) ).
cnf(t4674,plain,
complement(join(sF3,complement(sF6))) = sF6,
inference(orient,[status(thm)],[t61817]) ).
cnf(t4680,plain,
join(sF3,complement(sF6)) = complement(sF6),
inference(cp,[status(thm)],[t1026,t4674]) ).
cnf(t4697,plain,
join(sF3,complement(sF6)) = complement(sF6),
inference(orient,[status(thm)],[t4680]) ).
cnf(t4701,plain,
join(sF4,complement(sF6)) = join(sF2,complement(sF6)),
inference(cp,[status(thm)],[t160,t4697]) ).
cnf(t215,plain,
X1 = join(complement(join(complement(X1),sk1)),complement(join(complement(X1),sF2))),
inference(cp,[status(thm)],[t213,t21]) ).
cnf(t61796,plain,
X1 = join(complement(join(complement(X1),sF2)),complement(join(complement(X1),sk1))),
inference(step,[status(thm)],[t215,t68]) ).
cnf(t61797,plain,
X1 = join(complement(join(sF2,complement(X1))),complement(join(complement(X1),sk1))),
inference(step,[status(thm)],[t61796,t68]) ).
cnf(t61798,plain,
X1 = join(complement(join(sF2,complement(X1))),complement(join(sk1,complement(X1)))),
inference(step,[status(thm)],[t61797,t68]) ).
cnf(t4443,plain,
join(complement(join(sF2,complement(X1))),complement(join(sk1,complement(X1)))) = X1,
inference(orient,[status(thm)],[t61798]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t46,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t47,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t46,t24]) ).
cnf(t143,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t47]) ).
cnf(t134,plain,
composition(join(sF0,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t126,t106]) ).
cnf(t1837,plain,
composition(join(sF0,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t134]) ).
cnf(t104,plain,
converse(join(sF0,X1)) = join(sF0,converse(X1)),
inference(cp,[status(thm)],[t46,t101]) ).
cnf(t107,plain,
converse(join(sF0,X1)) = join(sF0,converse(X1)),
inference(orient,[status(thm)],[t104]) ).
cnf(t15,axiom,
sF1 = join(sk2,one),
introduced(definition) ).
cnf(t61453,plain,
sF1 = join(sk2,sF0),
inference(step,[status(thm)],[t15,t27]) ).
cnf(t31,plain,
join(sk2,sF0) = sF1,
inference(orient,[status(thm)],[t61453]) ).
cnf(t3,axiom,
join(sk2,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
join(sk2,one) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t30,plain,
join(sk2,sF0) = one,
inference(rw,[status(thm)],[t26]) ).
cnf(t61455,plain,
sF1 = one,
inference(step,[status(thm)],[t30,t31]) ).
cnf(t61456,plain,
sF1 = sF0,
inference(step,[status(thm)],[t61455,t27]) ).
cnf(t38,plain,
sF1 = sF0,
inference(orient,[status(thm)],[t61456]) ).
cnf(t61457,plain,
join(sk2,sF0) = sF0,
inference(step,[status(thm)],[t31,t38]) ).
cnf(t39,plain,
join(sk2,sF0) = sF0,
inference(orient,[status(thm)],[t61457]) ).
cnf(t61461,plain,
join(sF0,sk2) = sF0,
inference(step,[status(thm)],[t39,t68]) ).
cnf(t69,plain,
join(sF0,sk2) = sF0,
inference(rw,[status(thm)],[t61461]) ).
cnf(t78,plain,
join(sF0,sk2) = sF0,
inference(orient,[status(thm)],[t69]) ).
cnf(t110,plain,
join(sF0,converse(sk2)) = converse(sF0),
inference(cp,[status(thm)],[t107,t78]) ).
cnf(t61470,plain,
join(sF0,converse(sk2)) = sF0,
inference(step,[status(thm)],[t110,t101]) ).
cnf(t137,plain,
join(sF0,converse(sk2)) = sF0,
inference(orient,[status(thm)],[t61470]) ).
cnf(t1842,plain,
join(X1,composition(converse(sk2),X1)) = composition(sF0,X1),
inference(cp,[status(thm)],[t1837,t137]) ).
cnf(t61791,plain,
join(X1,composition(converse(sk2),X1)) = X1,
inference(step,[status(thm)],[t1842,t106]) ).
cnf(t4378,plain,
join(X1,composition(converse(sk2),X1)) = X1,
inference(orient,[status(thm)],[t61791]) ).
cnf(t4388,plain,
join(X1,converse(composition(converse(sk2),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t143,t4378]) ).
cnf(t44,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t43,t24]) ).
cnf(t63,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t44]) ).
cnf(t61792,plain,
join(X1,composition(X1,converse(converse(sk2)))) = converse(converse(X1)),
inference(step,[status(thm)],[t4388,t63]) ).
cnf(t61793,plain,
join(X1,composition(X1,sk2)) = converse(converse(X1)),
inference(step,[status(thm)],[t61792,t24]) ).
cnf(t61794,plain,
join(X1,composition(X1,sk2)) = X1,
inference(step,[status(thm)],[t61793,t24]) ).
cnf(t4412,plain,
join(X1,composition(X1,sk2)) = X1,
inference(orient,[status(thm)],[t61794]) ).
cnf(t4413,plain,
sk1 = join(sk1,sF6),
inference(cp,[status(thm)],[t4412,t32]) ).
cnf(t61795,plain,
sk1 = join(sF6,sk1),
inference(step,[status(thm)],[t4413,t68]) ).
cnf(t4436,plain,
join(sF6,sk1) = sk1,
inference(orient,[status(thm)],[t61795]) ).
cnf(t4438,plain,
join(sF6,join(sk1,X1)) = join(sk1,X1),
inference(cp,[status(thm)],[t53,t4436]) ).
cnf(t4471,plain,
join(sF6,join(sk1,X1)) = join(sk1,X1),
inference(orient,[status(thm)],[t4438]) ).
cnf(t399,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t394,t68]) ).
cnf(t61746,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t399,t461]) ).
cnf(t3223,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t61746]) ).
cnf(t4481,plain,
join(sk1,complement(sF6)) = top,
inference(cp,[status(thm)],[t4471,t3223]) ).
cnf(t4486,plain,
join(sk1,complement(sF6)) = top,
inference(orient,[status(thm)],[t4481]) ).
cnf(t4493,plain,
sF6 = join(complement(join(sF2,complement(sF6))),complement(top)),
inference(cp,[status(thm)],[t4443,t4486]) ).
cnf(t61807,plain,
sF6 = join(complement(top),complement(join(sF2,complement(sF6)))),
inference(step,[status(thm)],[t4493,t68]) ).
cnf(t61808,plain,
sF6 = join(zero,complement(join(sF2,complement(sF6)))),
inference(step,[status(thm)],[t61807,t90]) ).
cnf(t61809,plain,
sF6 = complement(join(sF2,complement(sF6))),
inference(step,[status(thm)],[t61808,t962]) ).
cnf(t4603,plain,
complement(join(sF2,complement(sF6))) = sF6,
inference(orient,[status(thm)],[t61809]) ).
cnf(t4609,plain,
join(sF2,complement(sF6)) = complement(sF6),
inference(cp,[status(thm)],[t1026,t4603]) ).
cnf(t4626,plain,
join(sF2,complement(sF6)) = complement(sF6),
inference(orient,[status(thm)],[t4609]) ).
cnf(t61818,plain,
join(sF4,complement(sF6)) = complement(sF6),
inference(step,[status(thm)],[t4701,t4626]) ).
cnf(t4708,plain,
join(sF4,complement(sF6)) = complement(sF6),
inference(orient,[status(thm)],[t61818]) ).
cnf(t61053,plain,
sF5 = join(complement(complement(sF6)),complement(join(sF4,complement(complement(sF6))))),
inference(cp,[status(thm)],[t61027,t4708]) ).
cnf(t62789,plain,
sF5 = join(sF6,complement(join(sF4,complement(complement(sF6))))),
inference(step,[status(thm)],[t61053,t1026]) ).
cnf(t62790,plain,
sF5 = join(sF6,complement(join(sF4,sF6))),
inference(step,[status(thm)],[t62789,t1026]) ).
cnf(t163,plain,
join(sF4,X1) = join(sF2,join(X1,sF3)),
inference(cp,[status(thm)],[t160,t68]) ).
cnf(t296,plain,
join(sF2,join(X1,sF3)) = join(sF4,X1),
inference(orient,[status(thm)],[t163]) ).
cnf(t35,plain,
top = join(sk1,sF2),
inference(cp,[status(thm)],[t34,t21]) ).
cnf(t41,plain,
join(sk1,sF2) = top,
inference(orient,[status(thm)],[t35]) ).
cnf(t61463,plain,
join(sF2,sk1) = top,
inference(step,[status(thm)],[t41,t68]) ).
cnf(t71,plain,
join(sF2,sk1) = top,
inference(rw,[status(thm)],[t61463]) ).
cnf(t84,plain,
join(sF2,sk1) = top,
inference(orient,[status(thm)],[t71]) ).
cnf(t86,plain,
join(sF2,join(sk1,X1)) = join(top,X1),
inference(cp,[status(thm)],[t53,t84]) ).
cnf(t234,plain,
join(sF2,join(sk1,X1)) = join(top,X1),
inference(orient,[status(thm)],[t86]) ).
cnf(t300,plain,
join(sF4,sk1) = join(top,sF3),
inference(cp,[status(thm)],[t296,t234]) ).
cnf(t61493,plain,
join(sF4,sk1) = join(sF3,top),
inference(step,[status(thm)],[t300,t68]) ).
cnf(t302,plain,
join(sF4,sk1) = join(sF3,top),
inference(orient,[status(thm)],[t61493]) ).
cnf(t305,plain,
join(sF6,composition(sF4,sk2)) = composition(join(sF3,top),sk2),
inference(cp,[status(thm)],[t262,t302]) ).
cnf(t61581,plain,
join(sF6,composition(sF4,sk2)) = composition(top,sk2),
inference(step,[status(thm)],[t305,t440]) ).
cnf(t803,plain,
join(sF6,composition(sF4,sk2)) = composition(top,sk2),
inference(orient,[status(thm)],[t61581]) ).
cnf(t805,plain,
join(sF6,join(composition(sF4,sk2),X1)) = join(composition(top,sk2),X1),
inference(cp,[status(thm)],[t53,t803]) ).
cnf(t45362,plain,
join(sF6,join(composition(sF4,sk2),X1)) = join(composition(top,sk2),X1),
inference(orient,[status(thm)],[t805]) ).
cnf(t311,plain,
complement(sk2) = join(sF3,complement(sk2)),
inference(cp,[status(thm)],[t309,t22]) ).
cnf(t61499,plain,
sF3 = join(sF3,complement(sk2)),
inference(step,[status(thm)],[t311,t22]) ).
cnf(t61500,plain,
sF3 = join(sF3,sF3),
inference(step,[status(thm)],[t61499,t22]) ).
cnf(t320,plain,
join(sF3,sF3) = sF3,
inference(orient,[status(thm)],[t61500]) ).
cnf(t321,plain,
join(sF3,join(sF3,X1)) = join(sF3,X1),
inference(cp,[status(thm)],[t53,t320]) ).
cnf(t949,plain,
join(sF3,join(sF3,X1)) = join(sF3,X1),
inference(orient,[status(thm)],[t321]) ).
cnf(t953,plain,
join(sF4,join(sF3,X1)) = join(sF2,join(sF3,X1)),
inference(cp,[status(thm)],[t160,t949]) ).
cnf(t75,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(cp,[status(thm)],[t68,t53]) ).
cnf(t729,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t75]) ).
cnf(t61630,plain,
join(sF3,join(X1,sF4)) = join(sF2,join(sF3,X1)),
inference(step,[status(thm)],[t953,t729]) ).
cnf(t77,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t53,t68]) ).
cnf(t61582,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t77,t53]) ).
cnf(t809,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t61582]) ).
cnf(t322,plain,
join(sF4,sF3) = join(sF2,sF3),
inference(cp,[status(thm)],[t160,t320]) ).
cnf(t61508,plain,
join(sF3,sF4) = join(sF2,sF3),
inference(step,[status(thm)],[t322,t68]) ).
cnf(t61509,plain,
join(sF3,sF4) = sF4,
inference(step,[status(thm)],[t61508,t61]) ).
cnf(t369,plain,
join(sF3,sF4) = sF4,
inference(orient,[status(thm)],[t61509]) ).
cnf(t841,plain,
join(sF3,join(X1,sF4)) = join(X1,sF4),
inference(cp,[status(thm)],[t809,t369]) ).
cnf(t1486,plain,
join(sF3,join(X1,sF4)) = join(X1,sF4),
inference(orient,[status(thm)],[t841]) ).
cnf(t61631,plain,
join(X1,sF4) = join(sF2,join(sF3,X1)),
inference(step,[status(thm)],[t61630,t1486]) ).
cnf(t61632,plain,
join(X1,sF4) = join(sF4,X1),
inference(step,[status(thm)],[t61631,t160]) ).
cnf(t1545,plain,
join(X1,sF4) = join(sF4,X1),
inference(orient,[status(thm)],[t61632]) ).
cnf(t45372,plain,
join(composition(top,sk2),sF4) = join(sF6,join(sF4,composition(sF4,sk2))),
inference(cp,[status(thm)],[t45362,t1545]) ).
cnf(t62671,plain,
join(composition(top,sk2),sF4) = join(sF6,sF4),
inference(step,[status(thm)],[t45372,t4412]) ).
cnf(t62672,plain,
join(sF4,composition(top,sk2)) = join(sF6,sF4),
inference(step,[status(thm)],[t62671,t68]) ).
cnf(t36,plain,
top = join(sk2,sF3),
inference(cp,[status(thm)],[t34,t22]) ).
cnf(t42,plain,
join(sk2,sF3) = top,
inference(orient,[status(thm)],[t36]) ).
cnf(t61464,plain,
join(sF3,sk2) = top,
inference(step,[status(thm)],[t42,t68]) ).
cnf(t72,plain,
join(sF3,sk2) = top,
inference(rw,[status(thm)],[t61464]) ).
cnf(t87,plain,
join(sF3,sk2) = top,
inference(orient,[status(thm)],[t72]) ).
cnf(t164,plain,
join(sF4,sk2) = join(sF2,top),
inference(cp,[status(thm)],[t160,t87]) ).
cnf(t165,plain,
join(sF4,sk2) = join(sF2,top),
inference(orient,[status(thm)],[t164]) ).
cnf(t167,plain,
join(sF4,join(sk2,X1)) = join(join(sF2,top),X1),
inference(cp,[status(thm)],[t53,t165]) ).
cnf(t61494,plain,
join(sF4,join(sk2,X1)) = join(sF2,join(top,X1)),
inference(step,[status(thm)],[t167,t53]) ).
cnf(t306,plain,
join(sF4,join(sk2,X1)) = join(sF2,join(top,X1)),
inference(orient,[status(thm)],[t61494]) ).
cnf(t467,plain,
join(sF4,join(sk2,X1)) = join(sF2,top),
inference(orient,[status(thm)],[t306]) ).
cnf(t83,plain,
join(sF0,join(sk1,X1)) = join(sF0,X1),
inference(cp,[status(thm)],[t53,t81]) ).
cnf(t202,plain,
join(sF0,join(sk1,X1)) = join(sF0,X1),
inference(orient,[status(thm)],[t83]) ).
cnf(t203,plain,
join(sF0,complement(sk1)) = join(sF0,top),
inference(cp,[status(thm)],[t202,t34]) ).
cnf(t61475,plain,
join(sF0,sF2) = join(sF0,top),
inference(step,[status(thm)],[t203,t21]) ).
cnf(t80,plain,
join(sF0,join(sk2,X1)) = join(sF0,X1),
inference(cp,[status(thm)],[t53,t78]) ).
cnf(t190,plain,
join(sF0,join(sk2,X1)) = join(sF0,X1),
inference(orient,[status(thm)],[t80]) ).
cnf(t191,plain,
join(sF0,complement(sk2)) = join(sF0,top),
inference(cp,[status(thm)],[t190,t34]) ).
cnf(t61473,plain,
join(sF0,sF3) = join(sF0,top),
inference(step,[status(thm)],[t191,t22]) ).
cnf(t195,plain,
join(sF0,top) = join(sF0,sF3),
inference(orient,[status(thm)],[t61473]) ).
cnf(t61476,plain,
join(sF0,sF2) = join(sF0,sF3),
inference(step,[status(thm)],[t61475,t195]) ).
cnf(t207,plain,
join(sF0,sF3) = join(sF0,sF2),
inference(orient,[status(thm)],[t61476]) ).
cnf(t61477,plain,
join(sF0,top) = join(sF0,sF2),
inference(step,[status(thm)],[t195,t207]) ).
cnf(t208,plain,
join(sF0,top) = join(sF0,sF2),
inference(orient,[status(thm)],[t61477]) ).
cnf(t61525,plain,
top = join(sF0,sF2),
inference(step,[status(thm)],[t208,t440]) ).
cnf(t442,plain,
top = join(sF0,sF2),
inference(rw,[status(thm)],[t61525]) ).
cnf(t454,plain,
join(sF0,sF2) = top,
inference(orient,[status(thm)],[t442]) ).
cnf(t61531,plain,
join(sF0,sF3) = top,
inference(step,[status(thm)],[t207,t454]) ).
cnf(t455,plain,
join(sF0,sF3) = top,
inference(orient,[status(thm)],[t61531]) ).
cnf(t1846,plain,
join(X1,composition(sF3,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t1837,t455]) ).
cnf(t2097,plain,
join(X1,composition(sF3,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t1846]) ).
cnf(t2111,plain,
join(sF2,top) = join(sF4,composition(top,sk2)),
inference(cp,[status(thm)],[t467,t2097]) ).
cnf(t61705,plain,
top = join(sF4,composition(top,sk2)),
inference(step,[status(thm)],[t2111,t440]) ).
cnf(t2642,plain,
join(sF4,composition(top,sk2)) = top,
inference(orient,[status(thm)],[t61705]) ).
cnf(t62673,plain,
top = join(sF6,sF4),
inference(step,[status(thm)],[t62672,t2642]) ).
cnf(t62674,plain,
top = join(sF4,sF6),
inference(step,[status(thm)],[t62673,t68]) ).
cnf(t45457,plain,
join(sF4,sF6) = top,
inference(orient,[status(thm)],[t62674]) ).
cnf(t62791,plain,
sF5 = join(sF6,complement(top)),
inference(step,[status(thm)],[t62790,t45457]) ).
cnf(t62792,plain,
sF5 = join(sF6,zero),
inference(step,[status(thm)],[t62791,t90]) ).
cnf(t970,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t962,t68]) ).
cnf(t1031,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t970]) ).
cnf(t62793,plain,
sF5 = sF6,
inference(step,[status(thm)],[t62792,t1031]) ).
cnf(t61221,plain,
sF6 = sF5,
inference(orient,[status(thm)],[t62793]) ).
cnf(t62794,plain,
composition(sk1,sk2) = sF5,
inference(step,[status(thm)],[t32,t61221]) ).
cnf(t61222,plain,
composition(sk1,sk2) = sF5,
inference(orient,[status(thm)],[t62794]) ).
cnf(u1,negated_conjecture,
composition(sk1,sk2) != meet(sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
complement(join(complement(sk1),complement(sk2))) != composition(sk1,sk2),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(g0_0,plain,
complement(join(sF2,complement(sk2))) != composition(sk1,sk2),
inference(rw,[status(thm)],[goal_0,t21]) ).
cnf(g0_1,plain,
complement(join(sF2,sF3)) != composition(sk1,sk2),
inference(rw,[status(thm)],[g0_0,t22]) ).
cnf(g0_2,plain,
complement(sF4) != composition(sk1,sk2),
inference(rw,[status(thm)],[g0_1,t61]) ).
cnf(g0_3,plain,
sF5 != composition(sk1,sk2),
inference(rw,[status(thm)],[g0_2,t254]) ).
cnf(g0_4,plain,
sF5 != sF5,
inference(rw,[status(thm)],[g0_3,t61222]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL028-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n007.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 07:21:08 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 32.36/4.55 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 32.36/4.55 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------