%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL027-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/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:06 PM UTC 2026
% Result : Unsatisfiable 15.29s 2.53s
% Output : CNFRefutation 15.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 23
% Syntax : Number of clauses : 254 ( 254 unt; 0 nHn; 143 RR)
% Number of literals : 254 ( 253 equ; 14 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 : 145 ( 9 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t67,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t11263,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t12,t67]) ).
cnf(t210,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t11263]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11260,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t67]) ).
cnf(t162,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t11260]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t48,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t50,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t48,t27]) ).
cnf(t98,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t50]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t11243,plain,
sF0 = one,
inference(step,[status(thm)],[t13,t28]) ).
cnf(t29,plain,
one = sF0,
inference(orient,[status(thm)],[t11243]) ).
cnf(t11245,plain,
composition(X1,sF0) = X1,
inference(step,[status(thm)],[t26,t29]) ).
cnf(t31,plain,
composition(X1,sF0) = X1,
inference(rw,[status(thm)],[t11245]) ).
cnf(t36,plain,
composition(X1,sF0) = X1,
inference(orient,[status(thm)],[t31]) ).
cnf(t99,plain,
composition(converse(sF0),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t98,t36]) ).
cnf(t11255,plain,
composition(converse(sF0),X1) = X1,
inference(step,[status(thm)],[t99,t27]) ).
cnf(t102,plain,
composition(converse(sF0),X1) = X1,
inference(orient,[status(thm)],[t11255]) ).
cnf(t103,plain,
sF0 = converse(sF0),
inference(cp,[status(thm)],[t102,t36]) ).
cnf(t104,plain,
converse(sF0) = sF0,
inference(orient,[status(thm)],[t103]) ).
cnf(t176,plain,
complement(X1) = join(complement(X1),composition(sF0,complement(composition(sF0,X1)))),
inference(cp,[status(thm)],[t162,t104]) ).
cnf(t11256,plain,
composition(sF0,X1) = X1,
inference(step,[status(thm)],[t102,t104]) ).
cnf(t105,plain,
composition(sF0,X1) = X1,
inference(rw,[status(thm)],[t11256]) ).
cnf(t109,plain,
composition(sF0,X1) = X1,
inference(orient,[status(thm)],[t105]) ).
cnf(t11290,plain,
complement(X1) = join(complement(X1),complement(composition(sF0,X1))),
inference(step,[status(thm)],[t176,t109]) ).
cnf(t11291,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t11290,t109]) ).
cnf(t299,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t11291]) ).
cnf(t308,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t210,t299]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t37,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t11415,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t308,t37]) ).
cnf(t11416,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t11415,t67]) ).
cnf(u0,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t11253,plain,
complement(top) = zero,
inference(step,[status(thm)],[t5,t37]) ).
cnf(t88,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t11253]) ).
cnf(t11417,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t11416,t88]) ).
cnf(t950,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t11417]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t58,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t305,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t299,t88]) ).
cnf(t11302,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t305,t88]) ).
cnf(t11303,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t11302,t88]) ).
cnf(t324,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t11303]) ).
cnf(t325,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t58,t324]) ).
cnf(t1217,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t325]) ).
cnf(t1221,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t1217,t950]) ).
cnf(t11431,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t1221,t950]) ).
cnf(t1223,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t11431]) ).
cnf(t11433,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t950,t1223]) ).
cnf(t1225,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t11433]) ).
cnf(t1314,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1225]) ).
cnf(t20,axiom,
sF7 = complement(sk1),
introduced(definition) ).
cnf(t25,plain,
complement(sk1) = sF7,
inference(orient,[status(thm)],[t20]) ).
cnf(t1315,plain,
sk1 = complement(sF7),
inference(cp,[status(thm)],[t1314,t25]) ).
cnf(t21,axiom,
sF8 = complement(complement(sk1)),
introduced(definition) ).
cnf(t11246,plain,
sF8 = complement(sF7),
inference(step,[status(thm)],[t21,t25]) ).
cnf(t35,plain,
complement(sF7) = sF8,
inference(orient,[status(thm)],[t11246]) ).
cnf(t11442,plain,
sk1 = sF8,
inference(step,[status(thm)],[t1315,t35]) ).
cnf(t1321,plain,
sk1 = sF8,
inference(orient,[status(thm)],[t11442]) ).
cnf(t14,axiom,
sF1 = composition(sk1,top),
introduced(definition) ).
cnf(t34,plain,
composition(sk1,top) = sF1,
inference(orient,[status(thm)],[t14]) ).
cnf(t11443,plain,
composition(sF8,top) = sF1,
inference(step,[status(thm)],[t34,t1321]) ).
cnf(t1323,plain,
composition(sF8,top) = sF1,
inference(rw,[status(thm)],[t11443]) ).
cnf(t1464,plain,
composition(sF8,top) = sF1,
inference(orient,[status(thm)],[t1323]) ).
cnf(t17,axiom,
sF4 = complement(one),
introduced(definition) ).
cnf(t24,plain,
complement(one) = sF4,
inference(orient,[status(thm)],[t17]) ).
cnf(t11244,plain,
complement(sF0) = sF4,
inference(step,[status(thm)],[t24,t29]) ).
cnf(t30,plain,
complement(sF0) = sF4,
inference(rw,[status(thm)],[t11244]) ).
cnf(t33,plain,
complement(sF0) = sF4,
inference(orient,[status(thm)],[t30]) ).
cnf(t18,axiom,
sF5 = join(complement(complement(composition(sk1,top))),complement(one)),
introduced(definition) ).
cnf(t11268,plain,
sF5 = join(complement(one),complement(complement(composition(sk1,top)))),
inference(step,[status(thm)],[t18,t67]) ).
cnf(t11269,plain,
sF5 = join(complement(sF0),complement(complement(composition(sk1,top)))),
inference(step,[status(thm)],[t11268,t29]) ).
cnf(t11270,plain,
sF5 = join(sF4,complement(complement(composition(sk1,top)))),
inference(step,[status(thm)],[t11269,t33]) ).
cnf(t11271,plain,
sF5 = join(sF4,complement(complement(sF1))),
inference(step,[status(thm)],[t11270,t34]) ).
cnf(t15,axiom,
sF2 = complement(composition(sk1,top)),
introduced(definition) ).
cnf(t11248,plain,
sF2 = complement(sF1),
inference(step,[status(thm)],[t15,t34]) ).
cnf(t45,plain,
complement(sF1) = sF2,
inference(orient,[status(thm)],[t11248]) ).
cnf(t11272,plain,
sF5 = join(sF4,complement(sF2)),
inference(step,[status(thm)],[t11271,t45]) ).
cnf(t16,axiom,
sF3 = complement(complement(composition(sk1,top))),
introduced(definition) ).
cnf(t11251,plain,
sF3 = complement(complement(sF1)),
inference(step,[status(thm)],[t16,t34]) ).
cnf(t11252,plain,
sF3 = complement(sF2),
inference(step,[status(thm)],[t11251,t45]) ).
cnf(t83,plain,
complement(sF2) = sF3,
inference(orient,[status(thm)],[t11252]) ).
cnf(t11273,plain,
sF5 = join(sF4,sF3),
inference(step,[status(thm)],[t11272,t83]) ).
cnf(t11274,plain,
sF5 = join(sF3,sF4),
inference(step,[status(thm)],[t11273,t67]) ).
cnf(t260,plain,
join(sF3,sF4) = sF5,
inference(orient,[status(thm)],[t11274]) ).
cnf(t1316,plain,
sF1 = complement(sF2),
inference(cp,[status(thm)],[t1314,t45]) ).
cnf(t11452,plain,
sF1 = sF3,
inference(step,[status(thm)],[t1316,t83]) ).
cnf(t1339,plain,
sF3 = sF1,
inference(orient,[status(thm)],[t11452]) ).
cnf(t11457,plain,
join(sF1,sF4) = sF5,
inference(step,[status(thm)],[t260,t1339]) ).
cnf(t1344,plain,
join(sF1,sF4) = sF5,
inference(rw,[status(thm)],[t11457]) ).
cnf(t1468,plain,
join(sF1,sF4) = sF5,
inference(orient,[status(thm)],[t1344]) ).
cnf(t22,axiom,
sF9 = join(complement(complement(sk1)),complement(one)),
introduced(definition) ).
cnf(t11304,plain,
sF9 = join(complement(one),complement(complement(sk1))),
inference(step,[status(thm)],[t22,t67]) ).
cnf(t11305,plain,
sF9 = join(complement(sF0),complement(complement(sk1))),
inference(step,[status(thm)],[t11304,t29]) ).
cnf(t11306,plain,
sF9 = join(sF4,complement(complement(sk1))),
inference(step,[status(thm)],[t11305,t33]) ).
cnf(t11307,plain,
sF9 = join(sF4,complement(sF7)),
inference(step,[status(thm)],[t11306,t25]) ).
cnf(t11308,plain,
sF9 = join(sF4,sF8),
inference(step,[status(thm)],[t11307,t35]) ).
cnf(t326,plain,
join(sF4,sF8) = sF9,
inference(orient,[status(thm)],[t11308]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t51,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t74,plain,
join(converse(X1),converse(X2)) = converse(join(X2,X1)),
inference(cp,[status(thm)],[t67,t51]) ).
cnf(t11367,plain,
converse(join(X1,X2)) = converse(join(X2,X1)),
inference(step,[status(thm)],[t74,t51]) ).
cnf(t540,plain,
converse(join(X1,X2)) = converse(join(X2,X1)),
inference(orient,[status(thm)],[t11367]) ).
cnf(t328,plain,
join(sF4,join(sF8,X1)) = join(sF9,X1),
inference(cp,[status(thm)],[t58,t326]) ).
cnf(t1646,plain,
join(sF4,join(sF8,X1)) = join(sF9,X1),
inference(orient,[status(thm)],[t328]) ).
cnf(t1657,plain,
converse(join(join(sF8,X1),sF4)) = converse(join(sF9,X1)),
inference(cp,[status(thm)],[t540,t1646]) ).
cnf(t165,plain,
complement(sF0) = join(sF4,composition(converse(X1),complement(composition(X1,sF0)))),
inference(cp,[status(thm)],[t162,t33]) ).
cnf(t11614,plain,
sF4 = join(sF4,composition(converse(X1),complement(composition(X1,sF0)))),
inference(step,[status(thm)],[t165,t33]) ).
cnf(t11615,plain,
sF4 = join(sF4,composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t11614,t36]) ).
cnf(t3161,plain,
join(sF4,composition(converse(X1),complement(X1))) = sF4,
inference(orient,[status(thm)],[t11615]) ).
cnf(t952,plain,
sF0 = join(zero,complement(sF4)),
inference(cp,[status(thm)],[t950,t33]) ).
cnf(t977,plain,
join(zero,complement(sF4)) = sF0,
inference(orient,[status(thm)],[t952]) ).
cnf(t11434,plain,
complement(sF4) = sF0,
inference(step,[status(thm)],[t977,t1223]) ).
cnf(t1226,plain,
complement(sF4) = sF0,
inference(rw,[status(thm)],[t11434]) ).
cnf(t1241,plain,
complement(sF4) = sF0,
inference(orient,[status(thm)],[t1226]) ).
cnf(t3181,plain,
sF4 = join(sF4,composition(converse(sF4),sF0)),
inference(cp,[status(thm)],[t3161,t1241]) ).
cnf(t11616,plain,
sF4 = join(sF4,converse(sF4)),
inference(step,[status(thm)],[t3181,t36]) ).
cnf(t3203,plain,
join(sF4,converse(sF4)) = sF4,
inference(orient,[status(thm)],[t11616]) ).
cnf(t3207,plain,
converse(join(converse(sF4),sF4)) = converse(sF4),
inference(cp,[status(thm)],[t540,t3203]) ).
cnf(t52,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t51,t27]) ).
cnf(t145,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t52]) ).
cnf(t11617,plain,
join(sF4,converse(sF4)) = converse(sF4),
inference(step,[status(thm)],[t3207,t145]) ).
cnf(t11618,plain,
sF4 = converse(sF4),
inference(step,[status(thm)],[t11617,t3203]) ).
cnf(t3215,plain,
converse(sF4) = sF4,
inference(orient,[status(thm)],[t11618]) ).
cnf(t3222,plain,
converse(join(X1,sF4)) = join(converse(X1),sF4),
inference(cp,[status(thm)],[t51,t3215]) ).
cnf(t11625,plain,
converse(join(X1,sF4)) = join(sF4,converse(X1)),
inference(step,[status(thm)],[t3222,t67]) ).
cnf(t3392,plain,
converse(join(X1,sF4)) = join(sF4,converse(X1)),
inference(orient,[status(thm)],[t11625]) ).
cnf(t11970,plain,
join(sF4,converse(join(sF8,X1))) = converse(join(sF9,X1)),
inference(step,[status(thm)],[t1657,t3392]) ).
cnf(t10927,plain,
join(sF4,converse(join(sF8,X1))) = converse(join(sF9,X1)),
inference(orient,[status(thm)],[t11970]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t119,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t127,plain,
composition(join(sF0,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t119,t109]) ).
cnf(t1746,plain,
composition(join(sF0,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t127]) ).
cnf(t107,plain,
converse(join(sF0,X1)) = join(sF0,converse(X1)),
inference(cp,[status(thm)],[t51,t104]) ).
cnf(t110,plain,
converse(join(sF0,X1)) = join(sF0,converse(X1)),
inference(orient,[status(thm)],[t107]) ).
cnf(t39,plain,
top = join(sF0,sF4),
inference(cp,[status(thm)],[t37,t33]) ).
cnf(t43,plain,
join(sF0,sF4) = top,
inference(orient,[status(thm)],[t39]) ).
cnf(t63,plain,
join(sF0,join(sF4,X1)) = join(top,X1),
inference(cp,[status(thm)],[t58,t43]) ).
cnf(t183,plain,
join(sF0,join(sF4,X1)) = join(top,X1),
inference(orient,[status(thm)],[t63]) ).
cnf(t329,plain,
join(top,sF8) = join(sF0,sF9),
inference(cp,[status(thm)],[t183,t326]) ).
cnf(t11322,plain,
join(sF8,top) = join(sF0,sF9),
inference(step,[status(thm)],[t329,t67]) ).
cnf(t40,plain,
top = join(sF7,sF8),
inference(cp,[status(thm)],[t37,t35]) ).
cnf(t44,plain,
join(sF7,sF8) = top,
inference(orient,[status(thm)],[t40]) ).
cnf(t64,plain,
join(sF7,join(sF8,X1)) = join(top,X1),
inference(cp,[status(thm)],[t58,t44]) ).
cnf(t191,plain,
join(sF7,join(sF8,X1)) = join(top,X1),
inference(orient,[status(thm)],[t64]) ).
cnf(t302,plain,
complement(sF7) = join(sF8,complement(sF7)),
inference(cp,[status(thm)],[t299,t35]) ).
cnf(t11296,plain,
sF8 = join(sF8,complement(sF7)),
inference(step,[status(thm)],[t302,t35]) ).
cnf(t11297,plain,
sF8 = join(sF8,sF8),
inference(step,[status(thm)],[t11296,t35]) ).
cnf(t315,plain,
join(sF8,sF8) = sF8,
inference(orient,[status(thm)],[t11297]) ).
cnf(t317,plain,
join(top,sF8) = join(sF7,sF8),
inference(cp,[status(thm)],[t191,t315]) ).
cnf(t11316,plain,
join(sF8,top) = join(sF7,sF8),
inference(step,[status(thm)],[t317,t67]) ).
cnf(t11317,plain,
join(sF8,top) = top,
inference(step,[status(thm)],[t11316,t44]) ).
cnf(t338,plain,
join(sF8,top) = top,
inference(orient,[status(thm)],[t11317]) ).
cnf(t11323,plain,
top = join(sF0,sF9),
inference(step,[status(thm)],[t11322,t338]) ).
cnf(t348,plain,
join(sF0,sF9) = top,
inference(orient,[status(thm)],[t11323]) ).
cnf(t351,plain,
join(sF0,converse(sF9)) = converse(top),
inference(cp,[status(thm)],[t110,t348]) ).
cnf(t375,plain,
join(sF0,converse(sF9)) = converse(top),
inference(orient,[status(thm)],[t351]) ).
cnf(t59,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t58,t37]) ).
cnf(t416,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t59]) ).
cnf(t435,plain,
top = join(complement(X1),join(complement(X1),complement(complement(X1)))),
inference(cp,[status(thm)],[t416,t299]) ).
cnf(t11348,plain,
top = join(complement(X1),top),
inference(step,[status(thm)],[t435,t37]) ).
cnf(t11349,plain,
top = join(top,complement(X1)),
inference(step,[status(thm)],[t11348,t67]) ).
cnf(t471,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t11349]) ).
cnf(t485,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t416,t471]) ).
cnf(t507,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t485]) ).
cnf(t522,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t145,t507]) ).
cnf(t602,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t522]) ).
cnf(t520,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t507,t67]) ).
cnf(t573,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t520]) ).
cnf(t604,plain,
converse(top) = top,
inference(cp,[status(thm)],[t602,t573]) ).
cnf(t662,plain,
converse(top) = top,
inference(orient,[status(thm)],[t604]) ).
cnf(t11392,plain,
join(sF0,converse(sF9)) = top,
inference(step,[status(thm)],[t375,t662]) ).
cnf(t665,plain,
join(sF0,converse(sF9)) = top,
inference(orient,[status(thm)],[t11392]) ).
cnf(t1752,plain,
join(X1,composition(converse(sF9),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t1746,t665]) ).
cnf(t10968,plain,
join(X1,composition(converse(sF9),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t1752]) ).
cnf(t10982,plain,
join(X1,converse(composition(converse(sF9),converse(X1)))) = converse(composition(top,converse(X1))),
inference(cp,[status(thm)],[t145,t10968]) ).
cnf(t49,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t48,t27]) ).
cnf(t93,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t49]) ).
cnf(t11971,plain,
join(X1,composition(X1,converse(converse(sF9)))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t10982,t93]) ).
cnf(t11972,plain,
join(X1,composition(X1,sF9)) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t11971,t27]) ).
cnf(t11973,plain,
join(X1,composition(X1,sF9)) = composition(X1,converse(top)),
inference(step,[status(thm)],[t11972,t93]) ).
cnf(t11974,plain,
join(X1,composition(X1,sF9)) = composition(X1,top),
inference(step,[status(thm)],[t11973,t662]) ).
cnf(t11034,plain,
join(X1,composition(X1,sF9)) = composition(X1,top),
inference(orient,[status(thm)],[t11974]) ).
cnf(t11095,plain,
converse(join(sF9,composition(sF8,sF9))) = join(sF4,converse(composition(sF8,top))),
inference(cp,[status(thm)],[t10927,t11034]) ).
cnf(t32,plain,
join(sk1,sF0) = one,
inference(rw,[status(thm)],[t28]) ).
cnf(t11247,plain,
join(sk1,sF0) = sF0,
inference(step,[status(thm)],[t32,t29]) ).
cnf(t41,plain,
join(sk1,sF0) = sF0,
inference(orient,[status(thm)],[t11247]) ).
cnf(t11249,plain,
join(sF0,sk1) = sF0,
inference(step,[status(thm)],[t41,t67]) ).
cnf(t68,plain,
join(sF0,sk1) = sF0,
inference(rw,[status(thm)],[t11249]) ).
cnf(t77,plain,
join(sF0,sk1) = sF0,
inference(orient,[status(thm)],[t68]) ).
cnf(t79,plain,
join(sF0,join(sk1,X1)) = join(sF0,X1),
inference(cp,[status(thm)],[t58,t77]) ).
cnf(t205,plain,
join(sF0,join(sk1,X1)) = join(sF0,X1),
inference(orient,[status(thm)],[t79]) ).
cnf(t208,plain,
join(sF0,X1) = join(sF0,join(X1,sk1)),
inference(cp,[status(thm)],[t205,t67]) ).
cnf(t805,plain,
join(sF0,join(X1,sk1)) = join(sF0,X1),
inference(orient,[status(thm)],[t208]) ).
cnf(t316,plain,
join(sF8,join(sF8,X1)) = join(sF8,X1),
inference(cp,[status(thm)],[t58,t315]) ).
cnf(t1101,plain,
join(sF8,join(sF8,X1)) = join(sF8,X1),
inference(orient,[status(thm)],[t316]) ).
cnf(t951,plain,
sk1 = join(zero,complement(sF7)),
inference(cp,[status(thm)],[t950,t25]) ).
cnf(t11418,plain,
sk1 = join(zero,sF8),
inference(step,[status(thm)],[t951,t35]) ).
cnf(t11419,plain,
sk1 = join(sF8,zero),
inference(step,[status(thm)],[t11418,t67]) ).
cnf(t964,plain,
join(sF8,zero) = sk1,
inference(orient,[status(thm)],[t11419]) ).
cnf(t1105,plain,
join(sF8,zero) = join(sF8,sk1),
inference(cp,[status(thm)],[t1101,t964]) ).
cnf(t11423,plain,
sk1 = join(sF8,sk1),
inference(step,[status(thm)],[t1105,t964]) ).
cnf(t1108,plain,
join(sF8,sk1) = sk1,
inference(orient,[status(thm)],[t11423]) ).
cnf(t1115,plain,
join(sF0,sF8) = join(sF0,sk1),
inference(cp,[status(thm)],[t805,t1108]) ).
cnf(t11424,plain,
join(sF0,sF8) = sF0,
inference(step,[status(thm)],[t1115,t77]) ).
cnf(t1147,plain,
join(sF0,sF8) = sF0,
inference(orient,[status(thm)],[t11424]) ).
cnf(t1763,plain,
join(X1,composition(sF8,X1)) = composition(sF0,X1),
inference(cp,[status(thm)],[t1746,t1147]) ).
cnf(t11613,plain,
join(X1,composition(sF8,X1)) = X1,
inference(step,[status(thm)],[t1763,t109]) ).
cnf(t3138,plain,
join(X1,composition(sF8,X1)) = X1,
inference(orient,[status(thm)],[t11613]) ).
cnf(t11976,plain,
converse(sF9) = join(sF4,converse(composition(sF8,top))),
inference(step,[status(thm)],[t11095,t3138]) ).
cnf(t672,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t48,t662]) ).
cnf(t735,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t672]) ).
cnf(t11977,plain,
converse(sF9) = join(sF4,composition(top,converse(sF8))),
inference(step,[status(thm)],[t11976,t735]) ).
cnf(t736,plain,
composition(top,converse(sk1)) = converse(sF1),
inference(cp,[status(thm)],[t735,t34]) ).
cnf(t761,plain,
composition(top,converse(sk1)) = converse(sF1),
inference(orient,[status(thm)],[t736]) ).
cnf(t11448,plain,
composition(top,converse(sF8)) = converse(sF1),
inference(step,[status(thm)],[t761,t1321]) ).
cnf(t1332,plain,
composition(top,converse(sF8)) = converse(sF1),
inference(rw,[status(thm)],[t11448]) ).
cnf(t1552,plain,
composition(top,converse(sF8)) = converse(sF1),
inference(orient,[status(thm)],[t1332]) ).
cnf(t11978,plain,
converse(sF9) = join(sF4,converse(sF1)),
inference(step,[status(thm)],[t11977,t1552]) ).
cnf(t3394,plain,
join(sF4,converse(sF1)) = converse(sF5),
inference(cp,[status(thm)],[t3392,t1468]) ).
cnf(t3449,plain,
join(sF4,converse(sF1)) = converse(sF5),
inference(orient,[status(thm)],[t3394]) ).
cnf(t11979,plain,
converse(sF9) = converse(sF5),
inference(step,[status(thm)],[t11978,t3449]) ).
cnf(t11096,plain,
converse(sF9) = converse(sF5),
inference(orient,[status(thm)],[t11979]) ).
cnf(t11111,plain,
sF9 = converse(converse(sF5)),
inference(cp,[status(thm)],[t27,t11096]) ).
cnf(t11989,plain,
sF9 = sF5,
inference(step,[status(thm)],[t11111,t27]) ).
cnf(t11158,plain,
sF9 = sF5,
inference(orient,[status(thm)],[t11989]) ).
cnf(t11990,plain,
join(sF4,sF8) = sF5,
inference(step,[status(thm)],[t326,t11158]) ).
cnf(t11159,plain,
join(sF4,sF8) = sF5,
inference(orient,[status(thm)],[t11990]) ).
cnf(u1,negated_conjecture,
meet(complement(composition(sk1,top)),one) != meet(complement(sk1),one),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
complement(join(complement(complement(composition(sk1,top))),complement(one))) != complement(join(complement(complement(sk1)),complement(one))),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(g0_0,plain,
complement(join(composition(sk1,top),complement(one))) != complement(join(complement(complement(sk1)),complement(one))),
inference(rw,[status(thm)],[goal_0,t1314]) ).
cnf(g0_1,plain,
complement(join(composition(sF8,top),complement(one))) != complement(join(complement(complement(sk1)),complement(one))),
inference(rw,[status(thm)],[g0_0,t1321]) ).
cnf(g0_2,plain,
complement(join(sF1,complement(one))) != complement(join(complement(complement(sk1)),complement(one))),
inference(rw,[status(thm)],[g0_1,t1464]) ).
cnf(g0_3,plain,
complement(join(sF1,complement(sF0))) != complement(join(complement(complement(sk1)),complement(one))),
inference(rw,[status(thm)],[g0_2,t29]) ).
cnf(g0_4,plain,
complement(join(sF1,sF4)) != complement(join(complement(complement(sk1)),complement(one))),
inference(rw,[status(thm)],[g0_3,t33]) ).
cnf(g0_5,plain,
complement(sF5) != complement(join(complement(complement(sk1)),complement(one))),
inference(rw,[status(thm)],[g0_4,t1468]) ).
cnf(g0_6,plain,
complement(sF5) != complement(join(sk1,complement(one))),
inference(rw,[status(thm)],[g0_5,t1314]) ).
cnf(g0_7,plain,
complement(sF5) != complement(join(sF8,complement(one))),
inference(rw,[status(thm)],[g0_6,t1321]) ).
cnf(g0_8,plain,
complement(sF5) != complement(join(sF8,complement(sF0))),
inference(rw,[status(thm)],[g0_7,t29]) ).
cnf(g0_9,plain,
complement(sF5) != complement(join(sF8,sF4)),
inference(rw,[status(thm)],[g0_8,t33]) ).
cnf(g0_10,plain,
complement(sF5) != complement(join(sF4,sF8)),
inference(rw,[status(thm)],[g0_9,t67]) ).
cnf(g0_11,plain,
complement(sF5) != complement(sF5),
inference(rw,[status(thm)],[g0_10,t11159]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL027-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n007.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 07:19:52 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 15.29/2.53 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.29/2.53 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------