%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL050-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 : n010.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:13 PM UTC 2026
% Result : Unsatisfiable 7.18s 1.51s
% Output : CNFRefutation 7.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 17
% Syntax : Number of clauses : 198 ( 198 unt; 0 nHn; 93 RR)
% Number of literals : 198 ( 197 equ; 6 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 : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 138 ( 19 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t12,axiom,
sFlat0 = composition(sk1,top),
introduced(definition) ).
cnf(t57,plain,
composition(sk1,top) = sFlat0,
inference(orient,[status(thm)],[t12]) ).
cnf(t13,axiom,
sFlat1 = complement(composition(sk1,top)),
introduced(definition) ).
cnf(t2182,plain,
sFlat1 = complement(sFlat0),
inference(step,[status(thm)],[t13,t57]) ).
cnf(t66,plain,
complement(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t2182]) ).
cnf(t14,axiom,
sFlat2 = composition(complement(composition(sk1,top)),top),
introduced(definition) ).
cnf(t45,plain,
composition(complement(composition(sk1,top)),top) = sFlat2,
inference(orient,[status(thm)],[t14]) ).
cnf(t2180,plain,
composition(complement(sFlat0),top) = sFlat2,
inference(step,[status(thm)],[t45,t57]) ).
cnf(t62,plain,
composition(complement(sFlat0),top) = sFlat2,
inference(rw,[status(thm)],[t2180]) ).
cnf(t2184,plain,
composition(sFlat1,top) = sFlat2,
inference(step,[status(thm)],[t62,t66]) ).
cnf(t73,plain,
composition(sFlat1,top) = sFlat2,
inference(orient,[status(thm)],[t2184]) ).
cnf(t10,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t3,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t2179,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t10,t20]) ).
cnf(t31,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t2179]) ).
cnf(t7,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t5,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t50,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t5]) ).
cnf(t8,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t27,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t22,t25]) ).
cnf(t533,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t27]) ).
cnf(t543,plain,
join(top,complement(complement(X1))) = join(X1,top),
inference(cp,[status(thm)],[t533,t25]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t52,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t50,t19]) ).
cnf(t135,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t52]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t136,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t135,t18]) ).
cnf(t2185,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t136,t19]) ).
cnf(t150,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t2185]) ).
cnf(t151,plain,
one = converse(one),
inference(cp,[status(thm)],[t150,t18]) ).
cnf(t157,plain,
converse(one) = one,
inference(orient,[status(thm)],[t151]) ).
cnf(t2186,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t150,t157]) ).
cnf(t167,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t2186]) ).
cnf(t168,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t167]) ).
cnf(t171,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t31,t168]) ).
cnf(t2188,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t171,t157]) ).
cnf(t2189,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t2188,t168]) ).
cnf(t195,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t2189]) ).
cnf(t542,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t533,t195]) ).
cnf(t2219,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t542,t25]) ).
cnf(t557,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t2219]) ).
cnf(t2223,plain,
top = join(X1,top),
inference(step,[status(thm)],[t543,t557]) ).
cnf(t574,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t2223]) ).
cnf(t575,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t574,t20]) ).
cnf(t586,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t575]) ).
cnf(t6,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t35,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t6]) ).
cnf(t37,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t35,t19]) ).
cnf(t104,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t37]) ).
cnf(t105,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t104,t25]) ).
cnf(t258,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t105]) ).
cnf(t593,plain,
top = converse(top),
inference(cp,[status(thm)],[t586,t258]) ).
cnf(t599,plain,
converse(top) = top,
inference(orient,[status(thm)],[t593]) ).
cnf(t604,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t50,t599]) ).
cnf(t609,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t604]) ).
cnf(t614,plain,
composition(top,converse(sFlat1)) = converse(sFlat2),
inference(cp,[status(thm)],[t609,t73]) ).
cnf(t627,plain,
composition(top,converse(sFlat1)) = converse(sFlat2),
inference(orient,[status(thm)],[t614]) ).
cnf(t630,plain,
composition(top,composition(converse(sFlat1),X1)) = composition(converse(sFlat2),X1),
inference(cp,[status(thm)],[t40,t627]) ).
cnf(t724,plain,
composition(top,composition(converse(sFlat1),X1)) = composition(converse(sFlat2),X1),
inference(orient,[status(thm)],[t630]) ).
cnf(t725,plain,
composition(converse(sFlat2),converse(X1)) = composition(top,converse(composition(X1,sFlat1))),
inference(cp,[status(thm)],[t724,t50]) ).
cnf(t2248,plain,
converse(composition(X1,sFlat2)) = composition(top,converse(composition(X1,sFlat1))),
inference(step,[status(thm)],[t725,t50]) ).
cnf(t738,plain,
composition(top,converse(composition(X1,sFlat1))) = converse(composition(X1,sFlat2)),
inference(orient,[status(thm)],[t2248]) ).
cnf(t58,plain,
composition(sk1,composition(top,X1)) = composition(sFlat0,X1),
inference(cp,[status(thm)],[t40,t57]) ).
cnf(t80,plain,
composition(sk1,composition(top,X1)) = composition(sFlat0,X1),
inference(orient,[status(thm)],[t58]) ).
cnf(t67,plain,
top = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t25,t66]) ).
cnf(t71,plain,
join(sFlat0,sFlat1) = top,
inference(orient,[status(thm)],[t67]) ).
cnf(t72,plain,
join(sFlat0,join(sFlat1,X1)) = join(top,X1),
inference(cp,[status(thm)],[t22,t71]) ).
cnf(t86,plain,
join(sFlat0,join(sFlat1,X1)) = join(top,X1),
inference(orient,[status(thm)],[t72]) ).
cnf(t2232,plain,
join(sFlat0,join(sFlat1,X1)) = top,
inference(step,[status(thm)],[t86,t586]) ).
cnf(t587,plain,
join(sFlat0,join(sFlat1,X1)) = top,
inference(orient,[status(thm)],[t2232]) ).
cnf(t9,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t9]) ).
cnf(t631,plain,
composition(join(top,X1),converse(sFlat1)) = join(converse(sFlat2),composition(X1,converse(sFlat1))),
inference(cp,[status(thm)],[t28,t627]) ).
cnf(t2250,plain,
composition(top,converse(sFlat1)) = join(converse(sFlat2),composition(X1,converse(sFlat1))),
inference(step,[status(thm)],[t631,t586]) ).
cnf(t2251,plain,
converse(sFlat2) = join(converse(sFlat2),composition(X1,converse(sFlat1))),
inference(step,[status(thm)],[t2250,t627]) ).
cnf(t754,plain,
join(converse(sFlat2),composition(X1,converse(sFlat1))) = converse(sFlat2),
inference(orient,[status(thm)],[t2251]) ).
cnf(t756,plain,
converse(sFlat2) = join(converse(sFlat2),converse(sFlat1)),
inference(cp,[status(thm)],[t754,t168]) ).
cnf(t2253,plain,
converse(sFlat2) = converse(join(sFlat2,sFlat1)),
inference(step,[status(thm)],[t756,t35]) ).
cnf(t2254,plain,
converse(sFlat2) = converse(join(sFlat1,sFlat2)),
inference(step,[status(thm)],[t2253,t20]) ).
cnf(t817,plain,
converse(join(sFlat1,sFlat2)) = converse(sFlat2),
inference(orient,[status(thm)],[t2254]) ).
cnf(t818,plain,
join(sFlat1,sFlat2) = converse(converse(sFlat2)),
inference(cp,[status(thm)],[t19,t817]) ).
cnf(t2255,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t818,t19]) ).
cnf(t828,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t2255]) ).
cnf(t830,plain,
top = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t587,t828]) ).
cnf(t835,plain,
join(sFlat0,sFlat2) = top,
inference(orient,[status(thm)],[t830]) ).
cnf(t836,plain,
join(sFlat0,join(sFlat2,X1)) = join(top,X1),
inference(cp,[status(thm)],[t22,t835]) ).
cnf(t2256,plain,
join(sFlat0,join(sFlat2,X1)) = top,
inference(step,[status(thm)],[t836,t586]) ).
cnf(t840,plain,
join(sFlat0,join(sFlat2,X1)) = top,
inference(orient,[status(thm)],[t2256]) ).
cnf(t75,plain,
composition(join(sFlat1,X1),top) = join(sFlat2,composition(X1,top)),
inference(cp,[status(thm)],[t28,t73]) ).
cnf(t412,plain,
composition(join(sFlat1,X1),top) = join(sFlat2,composition(X1,top)),
inference(orient,[status(thm)],[t75]) ).
cnf(t421,plain,
join(sFlat2,composition(complement(sFlat1),top)) = composition(top,top),
inference(cp,[status(thm)],[t412,t25]) ).
cnf(t680,plain,
join(sFlat2,composition(complement(sFlat1),top)) = composition(top,top),
inference(orient,[status(thm)],[t421]) ).
cnf(t841,plain,
top = join(sFlat0,composition(top,top)),
inference(cp,[status(thm)],[t840,t680]) ).
cnf(t59,plain,
composition(join(sk1,X1),top) = join(sFlat0,composition(X1,top)),
inference(cp,[status(thm)],[t28,t57]) ).
cnf(t397,plain,
composition(join(sk1,X1),top) = join(sFlat0,composition(X1,top)),
inference(orient,[status(thm)],[t59]) ).
cnf(t576,plain,
join(sFlat0,composition(top,top)) = composition(top,top),
inference(cp,[status(thm)],[t397,t574]) ).
cnf(t672,plain,
join(sFlat0,composition(top,top)) = composition(top,top),
inference(orient,[status(thm)],[t576]) ).
cnf(t2257,plain,
top = composition(top,top),
inference(step,[status(thm)],[t841,t672]) ).
cnf(t851,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t2257]) ).
cnf(t859,plain,
composition(sFlat0,top) = composition(sk1,top),
inference(cp,[status(thm)],[t80,t851]) ).
cnf(t2265,plain,
composition(sFlat0,top) = sFlat0,
inference(step,[status(thm)],[t859,t57]) ).
cnf(t868,plain,
composition(sFlat0,top) = sFlat0,
inference(orient,[status(thm)],[t2265]) ).
cnf(t873,plain,
complement(top) = join(complement(top),composition(converse(sFlat0),complement(sFlat0))),
inference(cp,[status(thm)],[t31,t868]) ).
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(t4,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t2181,plain,
complement(top) = zero,
inference(step,[status(thm)],[t4,t25]) ).
cnf(t63,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t2181]) ).
cnf(t2278,plain,
zero = join(complement(top),composition(converse(sFlat0),complement(sFlat0))),
inference(step,[status(thm)],[t873,t63]) ).
cnf(t2279,plain,
zero = join(zero,composition(converse(sFlat0),complement(sFlat0))),
inference(step,[status(thm)],[t2278,t63]) ).
cnf(t2280,plain,
zero = join(zero,composition(converse(sFlat0),sFlat1)),
inference(step,[status(thm)],[t2279,t66]) ).
cnf(t1005,plain,
join(zero,composition(converse(sFlat0),sFlat1)) = zero,
inference(orient,[status(thm)],[t2280]) ).
cnf(t196,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t195,t63]) ).
cnf(t2190,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t196,t63]) ).
cnf(t2191,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t2190,t63]) ).
cnf(t201,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t2191]) ).
cnf(t202,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t22,t201]) ).
cnf(t217,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t202]) ).
cnf(t11,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t11]) ).
cnf(t21,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t15]) ).
cnf(t2332,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t21,t20]) ).
cnf(t1936,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t2332]) ).
cnf(t1938,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t1936,t195]) ).
cnf(t2333,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t1938,t25]) ).
cnf(t2334,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t2333,t63]) ).
cnf(t2335,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t2334,t20]) ).
cnf(t1973,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t2335]) ).
cnf(t1975,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t217,t1973]) ).
cnf(t2336,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t1975,t1973]) ).
cnf(t1983,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t2336]) ).
cnf(t2347,plain,
composition(converse(sFlat0),sFlat1) = zero,
inference(step,[status(thm)],[t1005,t1983]) ).
cnf(t2016,plain,
composition(converse(sFlat0),sFlat1) = zero,
inference(rw,[status(thm)],[t2347]) ).
cnf(t2112,plain,
composition(converse(sFlat0),sFlat1) = zero,
inference(orient,[status(thm)],[t2016]) ).
cnf(t2116,plain,
converse(composition(converse(sFlat0),sFlat2)) = composition(top,converse(zero)),
inference(cp,[status(thm)],[t738,t2112]) ).
cnf(t2364,plain,
composition(converse(sFlat2),sFlat0) = composition(top,converse(zero)),
inference(step,[status(thm)],[t2116,t135]) ).
cnf(t2340,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t1973,t1983]) ).
cnf(t2010,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t2340]) ).
cnf(t2039,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t2010]) ).
cnf(t2242,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t258,t599]) ).
cnf(t602,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t2242]) ).
cnf(t1990,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t1983,t602]) ).
cnf(t2087,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t1990]) ).
cnf(t2088,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t19,t2087]) ).
cnf(t2360,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t2088,t599]) ).
cnf(t2101,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t2360]) ).
cnf(t2102,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t2039,t2101]) ).
cnf(t2361,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t2102,t63]) ).
cnf(t2106,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t2361]) ).
cnf(t2365,plain,
composition(converse(sFlat2),sFlat0) = composition(top,zero),
inference(step,[status(thm)],[t2364,t2106]) ).
cnf(t861,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t31,t851]) ).
cnf(t2268,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t861,t63]) ).
cnf(t2269,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t2268,t63]) ).
cnf(t2270,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t2269,t599]) ).
cnf(t2271,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t2270,t63]) ).
cnf(t896,plain,
join(zero,composition(top,zero)) = zero,
inference(orient,[status(thm)],[t2271]) ).
cnf(t897,plain,
join(zero,join(composition(top,zero),X1)) = join(zero,X1),
inference(cp,[status(thm)],[t22,t896]) ).
cnf(t1415,plain,
join(zero,join(composition(top,zero),X1)) = join(zero,X1),
inference(orient,[status(thm)],[t897]) ).
cnf(t1417,plain,
join(zero,composition(X1,zero)) = join(zero,composition(join(top,X1),zero)),
inference(cp,[status(thm)],[t1415,t28]) ).
cnf(t2311,plain,
join(zero,composition(X1,zero)) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t1417,t586]) ).
cnf(t2312,plain,
join(zero,composition(X1,zero)) = zero,
inference(step,[status(thm)],[t2311,t896]) ).
cnf(t1431,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t2312]) ).
cnf(t2337,plain,
composition(X1,zero) = zero,
inference(step,[status(thm)],[t1431,t1983]) ).
cnf(t2008,plain,
composition(X1,zero) = zero,
inference(rw,[status(thm)],[t2337]) ).
cnf(t2031,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t2008]) ).
cnf(t2366,plain,
composition(converse(sFlat2),sFlat0) = zero,
inference(step,[status(thm)],[t2365,t2031]) ).
cnf(t2134,plain,
composition(converse(sFlat2),sFlat0) = zero,
inference(orient,[status(thm)],[t2366]) ).
cnf(t2140,plain,
complement(sFlat0) = join(complement(sFlat0),composition(converse(converse(sFlat2)),complement(zero))),
inference(cp,[status(thm)],[t31,t2134]) ).
cnf(t2367,plain,
sFlat1 = join(complement(sFlat0),composition(converse(converse(sFlat2)),complement(zero))),
inference(step,[status(thm)],[t2140,t66]) ).
cnf(t2368,plain,
sFlat1 = join(sFlat1,composition(converse(converse(sFlat2)),complement(zero))),
inference(step,[status(thm)],[t2367,t66]) ).
cnf(t2369,plain,
sFlat1 = join(sFlat1,composition(sFlat2,complement(zero))),
inference(step,[status(thm)],[t2368,t19]) ).
cnf(t1989,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t1983,t25]) ).
cnf(t2018,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t1989]) ).
cnf(t2370,plain,
sFlat1 = join(sFlat1,composition(sFlat2,top)),
inference(step,[status(thm)],[t2369,t2018]) ).
cnf(t74,plain,
composition(sFlat1,composition(top,X1)) = composition(sFlat2,X1),
inference(cp,[status(thm)],[t40,t73]) ).
cnf(t92,plain,
composition(sFlat1,composition(top,X1)) = composition(sFlat2,X1),
inference(orient,[status(thm)],[t74]) ).
cnf(t858,plain,
composition(sFlat2,top) = composition(sFlat1,top),
inference(cp,[status(thm)],[t92,t851]) ).
cnf(t2264,plain,
composition(sFlat2,top) = sFlat2,
inference(step,[status(thm)],[t858,t73]) ).
cnf(t862,plain,
composition(sFlat2,top) = sFlat2,
inference(orient,[status(thm)],[t2264]) ).
cnf(t2371,plain,
sFlat1 = join(sFlat1,sFlat2),
inference(step,[status(thm)],[t2370,t862]) ).
cnf(t2372,plain,
sFlat1 = sFlat2,
inference(step,[status(thm)],[t2371,t828]) ).
cnf(t2141,plain,
sFlat2 = sFlat1,
inference(orient,[status(thm)],[t2372]) ).
cnf(t2373,plain,
composition(sFlat1,top) = sFlat1,
inference(step,[status(thm)],[t73,t2141]) ).
cnf(t2142,plain,
composition(sFlat1,top) = sFlat1,
inference(orient,[status(thm)],[t2373]) ).
cnf(goal_0,negated_conjecture,
composition(complement(composition(sk1,top)),top) != complement(composition(sk1,top)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
composition(complement(sFlat0),top) != complement(composition(sk1,top)),
inference(rw,[status(thm)],[goal_0,t57]) ).
cnf(g0_1,plain,
composition(sFlat1,top) != complement(composition(sk1,top)),
inference(rw,[status(thm)],[g0_0,t66]) ).
cnf(g0_2,plain,
sFlat1 != complement(composition(sk1,top)),
inference(rw,[status(thm)],[g0_1,t2142]) ).
cnf(g0_3,plain,
sFlat1 != complement(sFlat0),
inference(rw,[status(thm)],[g0_2,t57]) ).
cnf(g0_4,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_3,t66]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL050-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 07:38:47 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.18/1.51 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.18/1.51 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------