%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL047-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 : n013.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:12 PM UTC 2026
% Result : Unsatisfiable 9.03s 4.18s
% Output : CNFRefutation 9.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 20
% Syntax : Number of clauses : 221 ( 221 unt; 0 nHn; 135 RR)
% Number of literals : 221 ( 220 equ; 16 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 : 18 ( 18 usr; 13 con; 0-2 aty)
% Number of variables : 105 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t14,axiom,
sF0 = join(sk1,sk2),
introduced(definition) ).
cnf(t2,axiom,
join(sk1,sk2) = sk2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
join(sk1,sk2) = sk2,
inference(orient,[status(thm)],[t2]) ).
cnf(t5293,plain,
sF0 = sk2,
inference(step,[status(thm)],[t14,t25]) ).
cnf(t27,plain,
sk2 = sF0,
inference(orient,[status(thm)],[t5293]) ).
cnf(t16,axiom,
sF2 = complement(sk2),
introduced(definition) ).
cnf(t21,plain,
complement(sk2) = sF2,
inference(orient,[status(thm)],[t16]) ).
cnf(t5294,plain,
complement(sF0) = sF2,
inference(step,[status(thm)],[t21,t27]) ).
cnf(t28,plain,
complement(sF0) = sF2,
inference(rw,[status(thm)],[t5294]) ).
cnf(t30,plain,
complement(sF0) = sF2,
inference(orient,[status(thm)],[t28]) ).
cnf(t15,axiom,
sF1 = join(sk1,sk3),
introduced(definition) ).
cnf(t3,axiom,
join(sk1,sk3) = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
join(sk1,sk3) = sk3,
inference(orient,[status(thm)],[t3]) ).
cnf(t5295,plain,
sF1 = sk3,
inference(step,[status(thm)],[t15,t26]) ).
cnf(t31,plain,
sk3 = sF1,
inference(orient,[status(thm)],[t5295]) ).
cnf(t17,axiom,
sF3 = complement(sk3),
introduced(definition) ).
cnf(t22,plain,
complement(sk3) = sF3,
inference(orient,[status(thm)],[t17]) ).
cnf(t5296,plain,
complement(sF1) = sF3,
inference(step,[status(thm)],[t22,t31]) ).
cnf(t32,plain,
complement(sF1) = sF3,
inference(rw,[status(thm)],[t5296]) ).
cnf(t34,plain,
complement(sF1) = sF3,
inference(orient,[status(thm)],[t32]) ).
cnf(t18,axiom,
sF4 = join(complement(sk2),complement(sk3)),
introduced(definition) ).
cnf(t5299,plain,
sF4 = join(complement(sF0),complement(sk3)),
inference(step,[status(thm)],[t18,t27]) ).
cnf(t5300,plain,
sF4 = join(sF2,complement(sk3)),
inference(step,[status(thm)],[t5299,t30]) ).
cnf(t5301,plain,
sF4 = join(sF2,complement(sF1)),
inference(step,[status(thm)],[t5300,t31]) ).
cnf(t5302,plain,
sF4 = join(sF2,sF3),
inference(step,[status(thm)],[t5301,t34]) ).
cnf(t59,plain,
join(sF2,sF3) = sF4,
inference(orient,[status(thm)],[t5302]) ).
cnf(t19,axiom,
sF5 = complement(join(complement(sk2),complement(sk3))),
introduced(definition) ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t66,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t5321,plain,
sF5 = complement(join(complement(sk3),complement(sk2))),
inference(step,[status(thm)],[t19,t66]) ).
cnf(t5322,plain,
sF5 = complement(join(complement(sF1),complement(sk2))),
inference(step,[status(thm)],[t5321,t31]) ).
cnf(t5323,plain,
sF5 = complement(join(sF3,complement(sk2))),
inference(step,[status(thm)],[t5322,t34]) ).
cnf(t5324,plain,
sF5 = complement(join(sF3,complement(sF0))),
inference(step,[status(thm)],[t5323,t27]) ).
cnf(t5325,plain,
sF5 = complement(join(sF3,sF2)),
inference(step,[status(thm)],[t5324,t30]) ).
cnf(t5326,plain,
sF5 = complement(join(sF2,sF3)),
inference(step,[status(thm)],[t5325,t66]) ).
cnf(t5327,plain,
sF5 = complement(sF4),
inference(step,[status(thm)],[t5326,t59]) ).
cnf(t262,plain,
complement(sF4) = sF5,
inference(orient,[status(thm)],[t5327]) ).
cnf(t20,axiom,
sF6 = join(sk1,complement(join(complement(sk2),complement(sk3)))),
introduced(definition) ).
cnf(t5333,plain,
sF6 = join(sk1,complement(join(complement(sk3),complement(sk2)))),
inference(step,[status(thm)],[t20,t66]) ).
cnf(t5334,plain,
sF6 = join(sk1,complement(join(complement(sF1),complement(sk2)))),
inference(step,[status(thm)],[t5333,t31]) ).
cnf(t5335,plain,
sF6 = join(sk1,complement(join(sF3,complement(sk2)))),
inference(step,[status(thm)],[t5334,t34]) ).
cnf(t5336,plain,
sF6 = join(sk1,complement(join(sF3,complement(sF0)))),
inference(step,[status(thm)],[t5335,t27]) ).
cnf(t5337,plain,
sF6 = join(sk1,complement(join(sF3,sF2))),
inference(step,[status(thm)],[t5336,t30]) ).
cnf(t5338,plain,
sF6 = join(sk1,complement(join(sF2,sF3))),
inference(step,[status(thm)],[t5337,t66]) ).
cnf(t5339,plain,
sF6 = join(sk1,complement(sF4)),
inference(step,[status(thm)],[t5338,t59]) ).
cnf(t5340,plain,
sF6 = join(sk1,sF5),
inference(step,[status(thm)],[t5339,t262]) ).
cnf(t5341,plain,
sF6 = join(sF5,sk1),
inference(step,[status(thm)],[t5340,t66]) ).
cnf(t299,plain,
join(sF5,sk1) = sF6,
inference(orient,[status(thm)],[t5341]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t5312,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t13,t66]) ).
cnf(t206,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t5312]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t5311,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t66]) ).
cnf(t164,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t5311]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t42,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(t44,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t42,t24]) ).
cnf(t82,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t44]) ).
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(t83,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t82,t23]) ).
cnf(t5305,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t83,t24]) ).
cnf(t86,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t5305]) ).
cnf(t87,plain,
one = converse(one),
inference(cp,[status(thm)],[t86,t23]) ).
cnf(t90,plain,
converse(one) = one,
inference(orient,[status(thm)],[t87]) ).
cnf(t175,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t164,t90]) ).
cnf(t5307,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t86,t90]) ).
cnf(t91,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t5307]) ).
cnf(t98,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t91]) ).
cnf(t5329,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t175,t98]) ).
cnf(t5330,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t5329,t98]) ).
cnf(t287,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t5330]) ).
cnf(t293,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t206,t287]) ).
cnf(t4,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t5423,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t293,t35]) ).
cnf(t5424,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t5423,t66]) ).
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(t5306,plain,
complement(top) = zero,
inference(step,[status(thm)],[t6,t35]) ).
cnf(t88,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t5306]) ).
cnf(t5425,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t5424,t88]) ).
cnf(t685,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t5425]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t51,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t290,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t287,t88]) ).
cnf(t5344,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t290,t88]) ).
cnf(t5345,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t5344,t88]) ).
cnf(t307,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t5345]) ).
cnf(t308,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t51,t307]) ).
cnf(t910,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t308]) ).
cnf(t912,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t910,t685]) ).
cnf(t5429,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t912,t685]) ).
cnf(t916,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t5429]) ).
cnf(t5431,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t685,t916]) ).
cnf(t918,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t5431]) ).
cnf(t952,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t918]) ).
cnf(t265,plain,
sF4 = join(complement(join(sF5,X1)),complement(join(complement(sF4),complement(X1)))),
inference(cp,[status(thm)],[t206,t262]) ).
cnf(t5685,plain,
sF4 = join(complement(join(sF5,X1)),complement(join(sF5,complement(X1)))),
inference(step,[status(thm)],[t265,t262]) ).
cnf(t5161,plain,
join(complement(join(sF5,X1)),complement(join(sF5,complement(X1)))) = sF4,
inference(orient,[status(thm)],[t5685]) ).
cnf(t5166,plain,
sF4 = join(complement(sF6),complement(join(sF5,complement(sk1)))),
inference(cp,[status(thm)],[t5161,t299]) ).
cnf(t60,plain,
join(sF2,join(sF3,X1)) = join(sF4,X1),
inference(cp,[status(thm)],[t51,t59]) ).
cnf(t158,plain,
join(sF2,join(sF3,X1)) = join(sF4,X1),
inference(orient,[status(thm)],[t60]) ).
cnf(t210,plain,
X1 = join(complement(join(complement(X1),sF1)),complement(join(complement(X1),sF3))),
inference(cp,[status(thm)],[t206,t34]) ).
cnf(t5606,plain,
X1 = join(complement(join(sF1,complement(X1))),complement(join(complement(X1),sF3))),
inference(step,[status(thm)],[t210,t66]) ).
cnf(t5607,plain,
X1 = join(complement(join(sF1,complement(X1))),complement(join(sF3,complement(X1)))),
inference(step,[status(thm)],[t5606,t66]) ).
cnf(t4166,plain,
join(complement(join(sF1,complement(X1))),complement(join(sF3,complement(X1)))) = X1,
inference(orient,[status(thm)],[t5607]) ).
cnf(t33,plain,
join(sk1,sF1) = sk3,
inference(rw,[status(thm)],[t26]) ).
cnf(t5298,plain,
join(sk1,sF1) = sF1,
inference(step,[status(thm)],[t33,t31]) ).
cnf(t39,plain,
join(sk1,sF1) = sF1,
inference(orient,[status(thm)],[t5298]) ).
cnf(t5304,plain,
join(sF1,sk1) = sF1,
inference(step,[status(thm)],[t39,t66]) ).
cnf(t68,plain,
join(sF1,sk1) = sF1,
inference(rw,[status(thm)],[t5304]) ).
cnf(t79,plain,
join(sF1,sk1) = sF1,
inference(orient,[status(thm)],[t68]) ).
cnf(t81,plain,
join(sF1,join(sk1,X1)) = join(sF1,X1),
inference(cp,[status(thm)],[t51,t79]) ).
cnf(t191,plain,
join(sF1,join(sk1,X1)) = join(sF1,X1),
inference(orient,[status(thm)],[t81]) ).
cnf(t192,plain,
join(sF1,complement(sk1)) = join(sF1,top),
inference(cp,[status(thm)],[t191,t35]) ).
cnf(t195,plain,
join(sF1,complement(sk1)) = join(sF1,top),
inference(orient,[status(thm)],[t192]) ).
cnf(t37,plain,
top = join(sF1,sF3),
inference(cp,[status(thm)],[t35,t34]) ).
cnf(t41,plain,
join(sF1,sF3) = top,
inference(orient,[status(thm)],[t37]) ).
cnf(t57,plain,
join(sF1,join(sF3,X1)) = join(top,X1),
inference(cp,[status(thm)],[t51,t41]) ).
cnf(t150,plain,
join(sF1,join(sF3,X1)) = join(top,X1),
inference(orient,[status(thm)],[t57]) ).
cnf(t151,plain,
join(top,complement(sF3)) = join(sF1,top),
inference(cp,[status(thm)],[t150,t35]) ).
cnf(t155,plain,
join(top,complement(sF3)) = join(sF1,top),
inference(orient,[status(thm)],[t151]) ).
cnf(t52,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t51,t35]) ).
cnf(t368,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t52]) ).
cnf(t394,plain,
top = join(complement(X1),join(complement(X1),complement(complement(X1)))),
inference(cp,[status(thm)],[t368,t287]) ).
cnf(t5371,plain,
top = join(complement(X1),top),
inference(step,[status(thm)],[t394,t35]) ).
cnf(t5372,plain,
top = join(top,complement(X1)),
inference(step,[status(thm)],[t5371,t66]) ).
cnf(t417,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t5372]) ).
cnf(t5374,plain,
top = join(sF1,top),
inference(step,[status(thm)],[t155,t417]) ).
cnf(t419,plain,
top = join(sF1,top),
inference(rw,[status(thm)],[t5374]) ).
cnf(t434,plain,
join(sF1,top) = top,
inference(orient,[status(thm)],[t419]) ).
cnf(t5377,plain,
join(sF1,complement(sk1)) = top,
inference(step,[status(thm)],[t195,t434]) ).
cnf(t435,plain,
join(sF1,complement(sk1)) = top,
inference(orient,[status(thm)],[t5377]) ).
cnf(t4170,plain,
sk1 = join(complement(top),complement(join(sF3,complement(sk1)))),
inference(cp,[status(thm)],[t4166,t435]) ).
cnf(t5608,plain,
sk1 = join(zero,complement(join(sF3,complement(sk1)))),
inference(step,[status(thm)],[t4170,t88]) ).
cnf(t5609,plain,
sk1 = complement(join(sF3,complement(sk1))),
inference(step,[status(thm)],[t5608,t916]) ).
cnf(t4188,plain,
complement(join(sF3,complement(sk1))) = sk1,
inference(orient,[status(thm)],[t5609]) ).
cnf(t4194,plain,
join(sF3,complement(sk1)) = complement(sk1),
inference(cp,[status(thm)],[t952,t4188]) ).
cnf(t4213,plain,
join(sF3,complement(sk1)) = complement(sk1),
inference(orient,[status(thm)],[t4194]) ).
cnf(t4217,plain,
join(sF4,complement(sk1)) = join(sF2,complement(sk1)),
inference(cp,[status(thm)],[t158,t4213]) ).
cnf(t208,plain,
X1 = join(complement(join(complement(X1),sF0)),complement(join(complement(X1),sF2))),
inference(cp,[status(thm)],[t206,t30]) ).
cnf(t5597,plain,
X1 = join(complement(join(sF0,complement(X1))),complement(join(complement(X1),sF2))),
inference(step,[status(thm)],[t208,t66]) ).
cnf(t5598,plain,
X1 = join(complement(join(sF0,complement(X1))),complement(join(sF2,complement(X1)))),
inference(step,[status(thm)],[t5597,t66]) ).
cnf(t3958,plain,
join(complement(join(sF0,complement(X1))),complement(join(sF2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t5598]) ).
cnf(t29,plain,
join(sk1,sF0) = sk2,
inference(rw,[status(thm)],[t25]) ).
cnf(t5297,plain,
join(sk1,sF0) = sF0,
inference(step,[status(thm)],[t29,t27]) ).
cnf(t38,plain,
join(sk1,sF0) = sF0,
inference(orient,[status(thm)],[t5297]) ).
cnf(t5303,plain,
join(sF0,sk1) = sF0,
inference(step,[status(thm)],[t38,t66]) ).
cnf(t67,plain,
join(sF0,sk1) = sF0,
inference(rw,[status(thm)],[t5303]) ).
cnf(t76,plain,
join(sF0,sk1) = sF0,
inference(orient,[status(thm)],[t67]) ).
cnf(t78,plain,
join(sF0,join(sk1,X1)) = join(sF0,X1),
inference(cp,[status(thm)],[t51,t76]) ).
cnf(t184,plain,
join(sF0,join(sk1,X1)) = join(sF0,X1),
inference(orient,[status(thm)],[t78]) ).
cnf(t185,plain,
join(sF0,complement(sk1)) = join(sF0,top),
inference(cp,[status(thm)],[t184,t35]) ).
cnf(t188,plain,
join(sF0,complement(sk1)) = join(sF0,top),
inference(orient,[status(thm)],[t185]) ).
cnf(t36,plain,
top = join(sF0,sF2),
inference(cp,[status(thm)],[t35,t30]) ).
cnf(t40,plain,
join(sF0,sF2) = top,
inference(orient,[status(thm)],[t36]) ).
cnf(t56,plain,
join(sF0,join(sF2,X1)) = join(top,X1),
inference(cp,[status(thm)],[t51,t40]) ).
cnf(t139,plain,
join(sF0,join(sF2,X1)) = join(top,X1),
inference(orient,[status(thm)],[t56]) ).
cnf(t140,plain,
join(top,complement(sF2)) = join(sF0,top),
inference(cp,[status(thm)],[t139,t35]) ).
cnf(t147,plain,
join(top,complement(sF2)) = join(sF0,top),
inference(orient,[status(thm)],[t140]) ).
cnf(t5373,plain,
top = join(sF0,top),
inference(step,[status(thm)],[t147,t417]) ).
cnf(t418,plain,
top = join(sF0,top),
inference(rw,[status(thm)],[t5373]) ).
cnf(t429,plain,
join(sF0,top) = top,
inference(orient,[status(thm)],[t418]) ).
cnf(t5375,plain,
join(sF0,complement(sk1)) = top,
inference(step,[status(thm)],[t188,t429]) ).
cnf(t430,plain,
join(sF0,complement(sk1)) = top,
inference(orient,[status(thm)],[t5375]) ).
cnf(t3962,plain,
sk1 = join(complement(top),complement(join(sF2,complement(sk1)))),
inference(cp,[status(thm)],[t3958,t430]) ).
cnf(t5599,plain,
sk1 = join(zero,complement(join(sF2,complement(sk1)))),
inference(step,[status(thm)],[t3962,t88]) ).
cnf(t5600,plain,
sk1 = complement(join(sF2,complement(sk1))),
inference(step,[status(thm)],[t5599,t916]) ).
cnf(t3980,plain,
complement(join(sF2,complement(sk1))) = sk1,
inference(orient,[status(thm)],[t5600]) ).
cnf(t3986,plain,
join(sF2,complement(sk1)) = complement(sk1),
inference(cp,[status(thm)],[t952,t3980]) ).
cnf(t4003,plain,
join(sF2,complement(sk1)) = complement(sk1),
inference(orient,[status(thm)],[t3986]) ).
cnf(t5610,plain,
join(sF4,complement(sk1)) = complement(sk1),
inference(step,[status(thm)],[t4217,t4003]) ).
cnf(t4225,plain,
join(sF4,complement(sk1)) = complement(sk1),
inference(orient,[status(thm)],[t5610]) ).
cnf(t4227,plain,
join(sF4,join(complement(sk1),X1)) = join(complement(sk1),X1),
inference(cp,[status(thm)],[t51,t4225]) ).
cnf(t5134,plain,
join(sF4,join(complement(sk1),X1)) = join(complement(sk1),X1),
inference(orient,[status(thm)],[t4227]) ).
cnf(t263,plain,
top = join(sF4,sF5),
inference(cp,[status(thm)],[t35,t262]) ).
cnf(t267,plain,
join(sF4,sF5) = top,
inference(orient,[status(thm)],[t263]) ).
cnf(t269,plain,
join(sF4,join(sF5,X1)) = join(top,X1),
inference(cp,[status(thm)],[t51,t267]) ).
cnf(t427,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t368,t417]) ).
cnf(t459,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t427]) ).
cnf(t468,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t459,t66]) ).
cnf(t489,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t468]) ).
cnf(t5419,plain,
join(sF4,join(sF5,X1)) = top,
inference(step,[status(thm)],[t269,t489]) ).
cnf(t641,plain,
join(sF4,join(sF5,X1)) = top,
inference(orient,[status(thm)],[t5419]) ).
cnf(t643,plain,
top = join(sF4,join(X1,sF5)),
inference(cp,[status(thm)],[t641,t66]) ).
cnf(t1287,plain,
join(sF4,join(X1,sF5)) = top,
inference(orient,[status(thm)],[t643]) ).
cnf(t5140,plain,
join(complement(sk1),sF5) = top,
inference(cp,[status(thm)],[t5134,t1287]) ).
cnf(t5684,plain,
join(sF5,complement(sk1)) = top,
inference(step,[status(thm)],[t5140,t66]) ).
cnf(t5153,plain,
join(sF5,complement(sk1)) = top,
inference(orient,[status(thm)],[t5684]) ).
cnf(t5686,plain,
sF4 = join(complement(sF6),complement(top)),
inference(step,[status(thm)],[t5166,t5153]) ).
cnf(t5687,plain,
sF4 = join(complement(sF6),zero),
inference(step,[status(thm)],[t5686,t88]) ).
cnf(t924,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t916,t66]) ).
cnf(t989,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t924]) ).
cnf(t5688,plain,
sF4 = complement(sF6),
inference(step,[status(thm)],[t5687,t989]) ).
cnf(t5218,plain,
complement(sF6) = sF4,
inference(orient,[status(thm)],[t5688]) ).
cnf(t5229,plain,
sF6 = complement(sF4),
inference(cp,[status(thm)],[t952,t5218]) ).
cnf(t5689,plain,
sF6 = sF5,
inference(step,[status(thm)],[t5229,t262]) ).
cnf(t5253,plain,
sF6 = sF5,
inference(orient,[status(thm)],[t5689]) ).
cnf(t5690,plain,
join(sF5,sk1) = sF5,
inference(step,[status(thm)],[t299,t5253]) ).
cnf(t5254,plain,
join(sF5,sk1) = sF5,
inference(orient,[status(thm)],[t5690]) ).
cnf(u1,negated_conjecture,
join(sk1,meet(sk2,sk3)) != meet(sk2,sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
join(sk1,complement(join(complement(sk2),complement(sk3)))) != complement(join(complement(sk2),complement(sk3))),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(g0_0,plain,
join(sk1,complement(join(complement(sF0),complement(sk3)))) != complement(join(complement(sk2),complement(sk3))),
inference(rw,[status(thm)],[goal_0,t27]) ).
cnf(g0_1,plain,
join(sk1,complement(join(sF2,complement(sk3)))) != complement(join(complement(sk2),complement(sk3))),
inference(rw,[status(thm)],[g0_0,t30]) ).
cnf(g0_2,plain,
join(sk1,complement(join(sF2,complement(sF1)))) != complement(join(complement(sk2),complement(sk3))),
inference(rw,[status(thm)],[g0_1,t31]) ).
cnf(g0_3,plain,
join(sk1,complement(join(sF2,sF3))) != complement(join(complement(sk2),complement(sk3))),
inference(rw,[status(thm)],[g0_2,t34]) ).
cnf(g0_4,plain,
join(sk1,complement(sF4)) != complement(join(complement(sk2),complement(sk3))),
inference(rw,[status(thm)],[g0_3,t59]) ).
cnf(g0_5,plain,
join(sk1,sF5) != complement(join(complement(sk2),complement(sk3))),
inference(rw,[status(thm)],[g0_4,t262]) ).
cnf(g0_6,plain,
join(sF5,sk1) != complement(join(complement(sk2),complement(sk3))),
inference(rw,[status(thm)],[g0_5,t66]) ).
cnf(g0_7,plain,
sF5 != complement(join(complement(sk2),complement(sk3))),
inference(rw,[status(thm)],[g0_6,t5254]) ).
cnf(g0_8,plain,
sF5 != complement(join(complement(sF0),complement(sk3))),
inference(rw,[status(thm)],[g0_7,t27]) ).
cnf(g0_9,plain,
sF5 != complement(join(sF2,complement(sk3))),
inference(rw,[status(thm)],[g0_8,t30]) ).
cnf(g0_10,plain,
sF5 != complement(join(sF2,complement(sF1))),
inference(rw,[status(thm)],[g0_9,t31]) ).
cnf(g0_11,plain,
sF5 != complement(join(sF2,sF3)),
inference(rw,[status(thm)],[g0_10,t34]) ).
cnf(g0_12,plain,
sF5 != complement(sF4),
inference(rw,[status(thm)],[g0_11,t59]) ).
cnf(g0_13,plain,
sF5 != sF5,
inference(rw,[status(thm)],[g0_12,t262]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL047-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/2.84 % Computer : n013.cluster.edu
% 0.10/2.84 % Model : x86_64 x86_64
% 0.10/2.84 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/2.84 % Memory : 8046.5625MB
% 0.10/2.84 % OS : Linux 6.8.0-71-generic
% 0.10/2.84 % CPULimit : 300
% 0.10/2.84 % WCLimit : 300
% 0.10/2.84 % DateTime : Thu Sep 24 07:36:57 UTC 2026
% 0.10/2.84 % CPUTime :
% 0.10/2.84 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.03/4.18 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.03/4.18 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------