%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL010-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 : n026.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:41 PM UTC 2026
% Result : Unsatisfiable 37.00s 10.13s
% Output : CNFRefutation 37.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 24
% Syntax : Number of clauses : 234 ( 234 unt; 0 nHn; 123 RR)
% Number of literals : 234 ( 233 equ; 9 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 : 21 ( 21 usr; 16 con; 0-2 aty)
% Number of variables : 148 ( 13 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t18,axiom,
sF5 = complement(sk2),
introduced(definition) ).
cnf(t25,plain,
complement(sk2) = sF5,
inference(orient,[status(thm)],[t18]) ).
cnf(t19,axiom,
sF6 = converse(sk1),
introduced(definition) ).
cnf(t26,plain,
converse(sk1) = sF6,
inference(orient,[status(thm)],[t19]) ).
cnf(t20,axiom,
sF7 = composition(converse(sk1),sk3),
introduced(definition) ).
cnf(t21866,plain,
sF7 = composition(sF6,sk3),
inference(step,[status(thm)],[t20,t26]) ).
cnf(t49,plain,
composition(sF6,sk3) = sF7,
inference(orient,[status(thm)],[t21866]) ).
cnf(t21,axiom,
sF8 = complement(composition(converse(sk1),sk3)),
introduced(definition) ).
cnf(t21878,plain,
sF8 = complement(composition(sF6,sk3)),
inference(step,[status(thm)],[t21,t26]) ).
cnf(t21879,plain,
sF8 = complement(sF7),
inference(step,[status(thm)],[t21878,t49]) ).
cnf(t154,plain,
complement(sF7) = sF8,
inference(orient,[status(thm)],[t21879]) ).
cnf(t22,axiom,
sF9 = join(complement(sk2),complement(composition(converse(sk1),sk3))),
introduced(definition) ).
cnf(t21928,plain,
sF9 = join(sF5,complement(composition(converse(sk1),sk3))),
inference(step,[status(thm)],[t22,t25]) ).
cnf(t21929,plain,
sF9 = join(sF5,complement(composition(sF6,sk3))),
inference(step,[status(thm)],[t21928,t26]) ).
cnf(t21930,plain,
sF9 = join(sF5,complement(sF7)),
inference(step,[status(thm)],[t21929,t49]) ).
cnf(t21931,plain,
sF9 = join(sF5,sF8),
inference(step,[status(thm)],[t21930,t154]) ).
cnf(t434,plain,
join(sF5,sF8) = sF9,
inference(orient,[status(thm)],[t21931]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t142,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t436,plain,
join(sF5,join(sF8,X1)) = join(sF9,X1),
inference(cp,[status(thm)],[t142,t434]) ).
cnf(t995,plain,
join(sF5,join(sF8,X1)) = join(sF9,X1),
inference(orient,[status(thm)],[t436]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t32,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t144,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t142,t32]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t3,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t37,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t21889,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t12,t37]) ).
cnf(t312,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t21889]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21886,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t37]) ).
cnf(t230,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t21886]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t50,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(t28,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t54,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t50,t28]) ).
cnf(t172,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t54]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t173,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t172,t27]) ).
cnf(t21880,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t173,t28]) ).
cnf(t180,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t21880]) ).
cnf(t183,plain,
one = converse(one),
inference(cp,[status(thm)],[t180,t27]) ).
cnf(t184,plain,
converse(one) = one,
inference(orient,[status(thm)],[t183]) ).
cnf(t258,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t230,t184]) ).
cnf(t21883,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t180,t184]) ).
cnf(t185,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t21883]) ).
cnf(t204,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t185]) ).
cnf(t21922,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t258,t204]) ).
cnf(t21923,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t21922,t204]) ).
cnf(t421,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t21923]) ).
cnf(t428,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t312,t421]) ).
cnf(t21996,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t428,t32]) ).
cnf(t21997,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t21996,t37]) ).
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(t4,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t21867,plain,
complement(top) = zero,
inference(step,[status(thm)],[t4,t32]) ).
cnf(t57,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t21867]) ).
cnf(t17,axiom,
sF4 = complement(join(complement(composition(sk1,sk2)),complement(sk3))),
introduced(definition) ).
cnf(t21899,plain,
sF4 = complement(join(complement(sk3),complement(composition(sk1,sk2)))),
inference(step,[status(thm)],[t17,t37]) ).
cnf(t15,axiom,
sF2 = complement(sk3),
introduced(definition) ).
cnf(t24,plain,
complement(sk3) = sF2,
inference(orient,[status(thm)],[t15]) ).
cnf(t21900,plain,
sF4 = complement(join(sF2,complement(composition(sk1,sk2)))),
inference(step,[status(thm)],[t21899,t24]) ).
cnf(t13,axiom,
sF0 = composition(sk1,sk2),
introduced(definition) ).
cnf(t31,plain,
composition(sk1,sk2) = sF0,
inference(orient,[status(thm)],[t13]) ).
cnf(t21901,plain,
sF4 = complement(join(sF2,complement(sF0))),
inference(step,[status(thm)],[t21900,t31]) ).
cnf(t14,axiom,
sF1 = complement(composition(sk1,sk2)),
introduced(definition) ).
cnf(t21865,plain,
sF1 = complement(sF0),
inference(step,[status(thm)],[t14,t31]) ).
cnf(t45,plain,
complement(sF0) = sF1,
inference(orient,[status(thm)],[t21865]) ).
cnf(t21902,plain,
sF4 = complement(join(sF2,sF1)),
inference(step,[status(thm)],[t21901,t45]) ).
cnf(t21903,plain,
sF4 = complement(join(sF1,sF2)),
inference(step,[status(thm)],[t21902,t37]) ).
cnf(t16,axiom,
sF3 = join(complement(composition(sk1,sk2)),complement(sk3)),
introduced(definition) ).
cnf(t21890,plain,
sF3 = join(complement(sk3),complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t16,t37]) ).
cnf(t21891,plain,
sF3 = join(sF2,complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t21890,t24]) ).
cnf(t21892,plain,
sF3 = join(sF2,complement(sF0)),
inference(step,[status(thm)],[t21891,t31]) ).
cnf(t21893,plain,
sF3 = join(sF2,sF1),
inference(step,[status(thm)],[t21892,t45]) ).
cnf(t21894,plain,
sF3 = join(sF1,sF2),
inference(step,[status(thm)],[t21893,t37]) ).
cnf(t358,plain,
join(sF1,sF2) = sF3,
inference(orient,[status(thm)],[t21894]) ).
cnf(t21904,plain,
sF4 = complement(sF3),
inference(step,[status(thm)],[t21903,t358]) ).
cnf(u1,axiom,
meet(composition(sk1,sk2),sk3) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t5,plain,
complement(join(complement(composition(sk1,sk2)),complement(sk3))) = zero,
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t21871,plain,
complement(join(complement(sk3),complement(composition(sk1,sk2)))) = zero,
inference(step,[status(thm)],[t5,t37]) ).
cnf(t21872,plain,
complement(join(sF2,complement(composition(sk1,sk2)))) = zero,
inference(step,[status(thm)],[t21871,t24]) ).
cnf(t21873,plain,
complement(join(sF2,complement(sF0))) = zero,
inference(step,[status(thm)],[t21872,t31]) ).
cnf(t21874,plain,
complement(join(sF2,sF1)) = zero,
inference(step,[status(thm)],[t21873,t45]) ).
cnf(t21875,plain,
complement(join(sF1,sF2)) = zero,
inference(step,[status(thm)],[t21874,t37]) ).
cnf(t83,plain,
complement(join(sF1,sF2)) = zero,
inference(orient,[status(thm)],[t21875]) ).
cnf(t21895,plain,
complement(sF3) = zero,
inference(step,[status(thm)],[t83,t358]) ).
cnf(t359,plain,
complement(sF3) = zero,
inference(rw,[status(thm)],[t21895]) ).
cnf(t363,plain,
complement(sF3) = zero,
inference(orient,[status(thm)],[t359]) ).
cnf(t21905,plain,
sF4 = zero,
inference(step,[status(thm)],[t21904,t363]) ).
cnf(t398,plain,
zero = sF4,
inference(orient,[status(thm)],[t21905]) ).
cnf(t21906,plain,
complement(top) = sF4,
inference(step,[status(thm)],[t57,t398]) ).
cnf(t399,plain,
complement(top) = sF4,
inference(orient,[status(thm)],[t21906]) ).
cnf(t21998,plain,
X1 = join(sF4,complement(complement(X1))),
inference(step,[status(thm)],[t21997,t399]) ).
cnf(t664,plain,
join(sF4,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t21998]) ).
cnf(t21911,plain,
complement(sF3) = sF4,
inference(step,[status(thm)],[t363,t398]) ).
cnf(t404,plain,
complement(sF3) = sF4,
inference(orient,[status(thm)],[t21911]) ).
cnf(t670,plain,
sF3 = join(sF4,complement(sF4)),
inference(cp,[status(thm)],[t664,t404]) ).
cnf(t21999,plain,
sF3 = top,
inference(step,[status(thm)],[t670,t32]) ).
cnf(t674,plain,
top = sF3,
inference(orient,[status(thm)],[t21999]) ).
cnf(t22217,plain,
join(X1,join(complement(X1),X2)) = join(sF3,X2),
inference(step,[status(thm)],[t144,t674]) ).
cnf(t33,plain,
top = join(sk3,sF2),
inference(cp,[status(thm)],[t32,t24]) ).
cnf(t35,plain,
join(sk3,sF2) = top,
inference(orient,[status(thm)],[t33]) ).
cnf(t21863,plain,
join(sF2,sk3) = top,
inference(step,[status(thm)],[t35,t37]) ).
cnf(t38,plain,
join(sF2,sk3) = top,
inference(rw,[status(thm)],[t21863]) ).
cnf(t41,plain,
join(sF2,sk3) = top,
inference(orient,[status(thm)],[t38]) ).
cnf(t147,plain,
join(sF2,join(sk3,X1)) = join(top,X1),
inference(cp,[status(thm)],[t142,t41]) ).
cnf(t308,plain,
join(sF2,join(sk3,X1)) = join(top,X1),
inference(orient,[status(thm)],[t147]) ).
cnf(t311,plain,
join(top,X1) = join(sF2,join(X1,sk3)),
inference(cp,[status(thm)],[t308,t37]) ).
cnf(t496,plain,
join(sF2,join(X1,sk3)) = join(top,X1),
inference(orient,[status(thm)],[t311]) ).
cnf(t497,plain,
join(top,X1) = join(join(X1,sk3),sF2),
inference(cp,[status(thm)],[t496,t37]) ).
cnf(t22138,plain,
join(sF3,X1) = join(join(X1,sk3),sF2),
inference(step,[status(thm)],[t497,t674]) ).
cnf(t22139,plain,
join(sF3,X1) = join(X1,join(sk3,sF2)),
inference(step,[status(thm)],[t22138,t142]) ).
cnf(t22140,plain,
join(sF3,X1) = join(X1,join(sF2,sk3)),
inference(step,[status(thm)],[t22139,t37]) ).
cnf(t22002,plain,
join(sF2,sk3) = sF3,
inference(step,[status(thm)],[t41,t674]) ).
cnf(t677,plain,
join(sF2,sk3) = sF3,
inference(orient,[status(thm)],[t22002]) ).
cnf(t22141,plain,
join(sF3,X1) = join(X1,sF3),
inference(step,[status(thm)],[t22140,t677]) ).
cnf(t1569,plain,
join(sF3,X1) = join(X1,sF3),
inference(orient,[status(thm)],[t22141]) ).
cnf(t425,plain,
complement(top) = join(sF4,complement(top)),
inference(cp,[status(thm)],[t421,t399]) ).
cnf(t21934,plain,
sF4 = join(sF4,complement(top)),
inference(step,[status(thm)],[t425,t399]) ).
cnf(t21935,plain,
sF4 = join(sF4,sF4),
inference(step,[status(thm)],[t21934,t399]) ).
cnf(t440,plain,
join(sF4,sF4) = sF4,
inference(orient,[status(thm)],[t21935]) ).
cnf(t441,plain,
join(sF4,join(sF4,X1)) = join(sF4,X1),
inference(cp,[status(thm)],[t142,t440]) ).
cnf(t1095,plain,
join(sF4,join(sF4,X1)) = join(sF4,X1),
inference(orient,[status(thm)],[t441]) ).
cnf(t1098,plain,
join(sF4,complement(complement(X1))) = join(sF4,X1),
inference(cp,[status(thm)],[t1095,t664]) ).
cnf(t22084,plain,
X1 = join(sF4,X1),
inference(step,[status(thm)],[t1098,t664]) ).
cnf(t1100,plain,
join(sF4,X1) = X1,
inference(orient,[status(thm)],[t22084]) ).
cnf(t22087,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t664,t1100]) ).
cnf(t1103,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t22087]) ).
cnf(t1193,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1103]) ).
cnf(t1197,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t421,t1193]) ).
cnf(t22104,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1197,t1193]) ).
cnf(t22105,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t22104,t1193]) ).
cnf(t1271,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t22105]) ).
cnf(t1285,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t142,t1271]) ).
cnf(t2046,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1285]) ).
cnf(t22000,plain,
join(X1,complement(X1)) = sF3,
inference(step,[status(thm)],[t32,t674]) ).
cnf(t675,plain,
join(X1,complement(X1)) = sF3,
inference(orient,[status(thm)],[t22000]) ).
cnf(t2051,plain,
join(X1,complement(X1)) = join(X1,sF3),
inference(cp,[status(thm)],[t2046,t675]) ).
cnf(t22178,plain,
sF3 = join(X1,sF3),
inference(step,[status(thm)],[t2051,t675]) ).
cnf(t2072,plain,
join(X1,sF3) = sF3,
inference(orient,[status(thm)],[t22178]) ).
cnf(t22182,plain,
join(sF3,X1) = sF3,
inference(step,[status(thm)],[t1569,t2072]) ).
cnf(t2076,plain,
join(sF3,X1) = sF3,
inference(orient,[status(thm)],[t22182]) ).
cnf(t22218,plain,
join(X1,join(complement(X1),X2)) = sF3,
inference(step,[status(thm)],[t22217,t2076]) ).
cnf(t2535,plain,
join(X1,join(complement(X1),X2)) = sF3,
inference(orient,[status(thm)],[t22218]) ).
cnf(t2538,plain,
sF3 = join(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t2535,t37]) ).
cnf(t7829,plain,
join(X1,join(X2,complement(X1))) = sF3,
inference(orient,[status(thm)],[t2538]) ).
cnf(t2056,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = join(complement(join(complement(X1),X2)),X1),
inference(cp,[status(thm)],[t2046,t312]) ).
cnf(t22761,plain,
X1 = join(complement(join(complement(X1),X2)),X1),
inference(step,[status(thm)],[t2056,t312]) ).
cnf(t22762,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t22761,t37]) ).
cnf(t20641,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t22762]) ).
cnf(t669,plain,
sF7 = join(sF4,complement(sF8)),
inference(cp,[status(thm)],[t664,t154]) ).
cnf(t804,plain,
join(sF4,complement(sF8)) = sF7,
inference(orient,[status(thm)],[t669]) ).
cnf(t22091,plain,
complement(sF8) = sF7,
inference(step,[status(thm)],[t804,t1100]) ).
cnf(t1107,plain,
complement(sF8) = sF7,
inference(rw,[status(thm)],[t22091]) ).
cnf(t1141,plain,
complement(sF8) = sF7,
inference(orient,[status(thm)],[t1107]) ).
cnf(t20651,plain,
sF8 = join(sF8,complement(join(sF7,X1))),
inference(cp,[status(thm)],[t20641,t1141]) ).
cnf(t20911,plain,
join(sF8,complement(join(sF7,X1))) = sF8,
inference(orient,[status(thm)],[t20651]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t189,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t29,plain,
sk1 = converse(sF6),
inference(cp,[status(thm)],[t28,t26]) ).
cnf(t30,plain,
converse(sF6) = sk1,
inference(orient,[status(thm)],[t29]) ).
cnf(t56,plain,
converse(composition(sF6,X1)) = composition(converse(X1),sk1),
inference(cp,[status(thm)],[t50,t30]) ).
cnf(t74,plain,
converse(composition(sF6,X1)) = composition(converse(X1),sk1),
inference(orient,[status(thm)],[t56]) ).
cnf(t76,plain,
composition(converse(sk3),sk1) = converse(sF7),
inference(cp,[status(thm)],[t74,t49]) ).
cnf(t82,plain,
composition(converse(sk3),sk1) = converse(sF7),
inference(orient,[status(thm)],[t76]) ).
cnf(t199,plain,
composition(join(converse(sk3),X1),sk1) = join(converse(sF7),composition(X1,sk1)),
inference(cp,[status(thm)],[t189,t82]) ).
cnf(t3213,plain,
composition(join(converse(sk3),X1),sk1) = join(converse(sF7),composition(X1,sk1)),
inference(orient,[status(thm)],[t199]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t86,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t3216,plain,
join(converse(sF7),composition(converse(X1),sk1)) = composition(converse(join(sk3,X1)),sk1),
inference(cp,[status(thm)],[t3213,t86]) ).
cnf(t101,plain,
converse(join(X1,composition(sF6,X2))) = join(converse(X1),composition(converse(X2),sk1)),
inference(cp,[status(thm)],[t86,t74]) ).
cnf(t1294,plain,
join(converse(X1),composition(converse(X2),sk1)) = converse(join(X1,composition(sF6,X2))),
inference(orient,[status(thm)],[t101]) ).
cnf(t22397,plain,
converse(join(sF7,composition(sF6,X1))) = composition(converse(join(sk3,X1)),sk1),
inference(step,[status(thm)],[t3216,t1294]) ).
cnf(t8448,plain,
converse(join(sF7,composition(sF6,X1))) = composition(converse(join(sk3,X1)),sk1),
inference(orient,[status(thm)],[t22397]) ).
cnf(t8451,plain,
join(sF7,composition(sF6,X1)) = converse(composition(converse(join(sk3,X1)),sk1)),
inference(cp,[status(thm)],[t28,t8448]) ).
cnf(t51,plain,
converse(composition(X1,sk1)) = composition(sF6,converse(X1)),
inference(cp,[status(thm)],[t50,t26]) ).
cnf(t61,plain,
converse(composition(X1,sk1)) = composition(sF6,converse(X1)),
inference(orient,[status(thm)],[t51]) ).
cnf(t22398,plain,
join(sF7,composition(sF6,X1)) = composition(sF6,converse(converse(join(sk3,X1)))),
inference(step,[status(thm)],[t8451,t61]) ).
cnf(t22399,plain,
join(sF7,composition(sF6,X1)) = composition(sF6,join(sk3,X1)),
inference(step,[status(thm)],[t22398,t28]) ).
cnf(t8518,plain,
composition(sF6,join(sk3,X1)) = join(sF7,composition(sF6,X1)),
inference(orient,[status(thm)],[t22399]) ).
cnf(t8522,plain,
join(sF7,composition(sF6,X1)) = composition(sF6,join(X1,sk3)),
inference(cp,[status(thm)],[t8518,t37]) ).
cnf(t8557,plain,
composition(sF6,join(X1,sk3)) = join(sF7,composition(sF6,X1)),
inference(orient,[status(thm)],[t8522]) ).
cnf(t322,plain,
sF0 = join(complement(join(sF1,X1)),complement(join(complement(sF0),complement(X1)))),
inference(cp,[status(thm)],[t312,t45]) ).
cnf(t22568,plain,
sF0 = join(complement(join(sF1,X1)),complement(join(sF1,complement(X1)))),
inference(step,[status(thm)],[t322,t45]) ).
cnf(t14375,plain,
join(complement(join(sF1,X1)),complement(join(sF1,complement(X1)))) = sF0,
inference(orient,[status(thm)],[t22568]) ).
cnf(t14376,plain,
sF0 = join(complement(join(sF1,sk3)),complement(join(sF1,sF2))),
inference(cp,[status(thm)],[t14375,t24]) ).
cnf(t22569,plain,
sF0 = join(complement(join(sF1,sF2)),complement(join(sF1,sk3))),
inference(step,[status(thm)],[t14376,t37]) ).
cnf(t22570,plain,
sF0 = join(complement(sF3),complement(join(sF1,sk3))),
inference(step,[status(thm)],[t22569,t358]) ).
cnf(t22571,plain,
sF0 = join(sF4,complement(join(sF1,sk3))),
inference(step,[status(thm)],[t22570,t404]) ).
cnf(t22572,plain,
sF0 = complement(join(sF1,sk3)),
inference(step,[status(thm)],[t22571,t1100]) ).
cnf(t14426,plain,
complement(join(sF1,sk3)) = sF0,
inference(orient,[status(thm)],[t22572]) ).
cnf(t14431,plain,
join(sF1,sk3) = complement(sF0),
inference(cp,[status(thm)],[t1193,t14426]) ).
cnf(t22573,plain,
join(sF1,sk3) = sF1,
inference(step,[status(thm)],[t14431,t45]) ).
cnf(t14464,plain,
join(sF1,sk3) = sF1,
inference(orient,[status(thm)],[t22573]) ).
cnf(t14476,plain,
join(sF7,composition(sF6,sF1)) = composition(sF6,sF1),
inference(cp,[status(thm)],[t8557,t14464]) ).
cnf(t14709,plain,
join(sF7,composition(sF6,sF1)) = composition(sF6,sF1),
inference(orient,[status(thm)],[t14476]) ).
cnf(t20920,plain,
sF8 = join(sF8,complement(composition(sF6,sF1))),
inference(cp,[status(thm)],[t20911,t14709]) ).
cnf(t21744,plain,
join(sF8,complement(composition(sF6,sF1))) = sF8,
inference(orient,[status(thm)],[t20920]) ).
cnf(t21755,plain,
sF3 = join(composition(sF6,sF1),sF8),
inference(cp,[status(thm)],[t7829,t21744]) ).
cnf(t22778,plain,
sF3 = join(sF8,composition(sF6,sF1)),
inference(step,[status(thm)],[t21755,t37]) ).
cnf(t21763,plain,
join(sF8,composition(sF6,sF1)) = sF3,
inference(orient,[status(thm)],[t22778]) ).
cnf(t21768,plain,
join(sF9,composition(sF6,sF1)) = join(sF5,sF3),
inference(cp,[status(thm)],[t995,t21763]) ).
cnf(t237,plain,
complement(sk2) = join(complement(sk2),composition(converse(sk1),complement(sF0))),
inference(cp,[status(thm)],[t230,t31]) ).
cnf(t21914,plain,
sF5 = join(complement(sk2),composition(converse(sk1),complement(sF0))),
inference(step,[status(thm)],[t237,t25]) ).
cnf(t21915,plain,
sF5 = join(sF5,composition(converse(sk1),complement(sF0))),
inference(step,[status(thm)],[t21914,t25]) ).
cnf(t21916,plain,
sF5 = join(sF5,composition(sF6,complement(sF0))),
inference(step,[status(thm)],[t21915,t26]) ).
cnf(t21917,plain,
sF5 = join(sF5,composition(sF6,sF1)),
inference(step,[status(thm)],[t21916,t45]) ).
cnf(t415,plain,
join(sF5,composition(sF6,sF1)) = sF5,
inference(orient,[status(thm)],[t21917]) ).
cnf(t417,plain,
join(sF5,join(composition(sF6,sF1),X1)) = join(sF5,X1),
inference(cp,[status(thm)],[t142,t415]) ).
cnf(t13600,plain,
join(sF5,join(composition(sF6,sF1),X1)) = join(sF5,X1),
inference(orient,[status(thm)],[t417]) ).
cnf(t998,plain,
join(sF9,X1) = join(sF5,join(X1,sF8)),
inference(cp,[status(thm)],[t995,t37]) ).
cnf(t1911,plain,
join(sF5,join(X1,sF8)) = join(sF9,X1),
inference(orient,[status(thm)],[t998]) ).
cnf(t13606,plain,
join(sF5,sF8) = join(sF9,composition(sF6,sF1)),
inference(cp,[status(thm)],[t13600,t1911]) ).
cnf(t22523,plain,
sF9 = join(sF9,composition(sF6,sF1)),
inference(step,[status(thm)],[t13606,t434]) ).
cnf(t13628,plain,
join(sF9,composition(sF6,sF1)) = sF9,
inference(orient,[status(thm)],[t22523]) ).
cnf(t22779,plain,
sF9 = join(sF5,sF3),
inference(step,[status(thm)],[t21768,t13628]) ).
cnf(t22780,plain,
sF9 = sF3,
inference(step,[status(thm)],[t22779,t2072]) ).
cnf(t21777,plain,
sF9 = sF3,
inference(orient,[status(thm)],[t22780]) ).
cnf(t22781,plain,
join(sF5,sF8) = sF3,
inference(step,[status(thm)],[t434,t21777]) ).
cnf(t21778,plain,
join(sF5,sF8) = sF3,
inference(orient,[status(thm)],[t22781]) ).
cnf(u2,negated_conjecture,
meet(sk2,composition(converse(sk1),sk3)) != zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))) != zero,
inference(definition_unfolding,[status(thm)],[u2,d0]) ).
cnf(g0_0,plain,
complement(join(sF5,complement(composition(converse(sk1),sk3)))) != zero,
inference(rw,[status(thm)],[goal_0,t25]) ).
cnf(g0_1,plain,
complement(join(sF5,complement(composition(sF6,sk3)))) != zero,
inference(rw,[status(thm)],[g0_0,t26]) ).
cnf(g0_2,plain,
complement(join(sF5,complement(sF7))) != zero,
inference(rw,[status(thm)],[g0_1,t49]) ).
cnf(g0_3,plain,
complement(join(sF5,sF8)) != zero,
inference(rw,[status(thm)],[g0_2,t154]) ).
cnf(g0_4,plain,
complement(sF3) != zero,
inference(rw,[status(thm)],[g0_3,t21778]) ).
cnf(g0_5,plain,
sF4 != zero,
inference(rw,[status(thm)],[g0_4,t404]) ).
cnf(g0_6,plain,
sF4 != sF4,
inference(rw,[status(thm)],[g0_5,t398]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL010-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/5.36 % Computer : n026.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Thu Sep 24 07:10:17 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.08/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 37.00/10.13 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.00/10.13 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------