%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL050-3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.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:14 PM UTC 2026
% Result : Unsatisfiable 14.16s 2.18s
% Output : CNFRefutation 14.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 94
% Number of leaves : 18
% Syntax : Number of clauses : 249 ( 249 unt; 0 nHn; 113 RR)
% Number of literals : 249 ( 248 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 : 185 ( 22 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t16,axiom,
sFlat0 = composition(sk1,top),
introduced(definition) ).
cnf(t50,plain,
composition(sk1,top) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t17,axiom,
sFlat1 = complement(composition(sk1,top)),
introduced(definition) ).
cnf(t16243,plain,
sFlat1 = complement(sFlat0),
inference(step,[status(thm)],[t17,t50]) ).
cnf(t111,plain,
complement(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t16243]) ).
cnf(t18,axiom,
sFlat2 = composition(complement(composition(sk1,top)),top),
introduced(definition) ).
cnf(t45,plain,
composition(complement(composition(sk1,top)),top) = sFlat2,
inference(orient,[status(thm)],[t18]) ).
cnf(t16241,plain,
composition(complement(sFlat0),top) = sFlat2,
inference(step,[status(thm)],[t45,t50]) ).
cnf(t55,plain,
composition(complement(sFlat0),top) = sFlat2,
inference(rw,[status(thm)],[t16241]) ).
cnf(t16244,plain,
composition(sFlat1,top) = sFlat2,
inference(step,[status(thm)],[t55,t111]) ).
cnf(t120,plain,
composition(sFlat1,top) = sFlat2,
inference(orient,[status(thm)],[t16244]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t56,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t16242,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t56]) ).
cnf(t67,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t16242]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t59,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t64,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t66,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t59,t64]) ).
cnf(t605,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t66]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t99,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t31,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t29,t23]) ).
cnf(t235,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t31]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t236,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t235,t19]) ).
cnf(t16251,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t236,t23]) ).
cnf(t248,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t16251]) ).
cnf(t249,plain,
one = converse(one),
inference(cp,[status(thm)],[t248,t19]) ).
cnf(t258,plain,
converse(one) = one,
inference(orient,[status(thm)],[t249]) ).
cnf(t16252,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t248,t258]) ).
cnf(t268,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t16252]) ).
cnf(t269,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t268]) ).
cnf(t272,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t67,t269]) ).
cnf(t16254,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t272,t258]) ).
cnf(t16255,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t16254,t269]) ).
cnf(t298,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t16255]) ).
cnf(t316,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t99,t298]) ).
cnf(t354,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t316]) ).
cnf(t362,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t64,t354]) ).
cnf(t415,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t362]) ).
cnf(t613,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t605,t415]) ).
cnf(t615,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t605,t298]) ).
cnf(t16289,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t615,t64]) ).
cnf(t632,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t16289]) ).
cnf(t635,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t632,t99]) ).
cnf(t654,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t635]) ).
cnf(t16293,plain,
top = join(X1,top),
inference(step,[status(thm)],[t613,t654]) ).
cnf(t660,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t16293]) ).
cnf(t661,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t660,t56]) ).
cnf(t670,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t661]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t74,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t76,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t74,t23]) ).
cnf(t422,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t76]) ).
cnf(t424,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t422,t64]) ).
cnf(t458,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t424]) ).
cnf(t677,plain,
top = converse(top),
inference(cp,[status(thm)],[t670,t458]) ).
cnf(t704,plain,
converse(top) = top,
inference(orient,[status(thm)],[t677]) ).
cnf(t709,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t29,t704]) ).
cnf(t716,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t709]) ).
cnf(t721,plain,
composition(top,converse(sFlat1)) = converse(sFlat2),
inference(cp,[status(thm)],[t716,t120]) ).
cnf(t736,plain,
composition(top,converse(sFlat1)) = converse(sFlat2),
inference(orient,[status(thm)],[t721]) ).
cnf(t741,plain,
composition(top,composition(converse(sFlat1),X1)) = composition(converse(sFlat2),X1),
inference(cp,[status(thm)],[t24,t736]) ).
cnf(t884,plain,
composition(top,composition(converse(sFlat1),X1)) = composition(converse(sFlat2),X1),
inference(orient,[status(thm)],[t741]) ).
cnf(t885,plain,
composition(converse(sFlat2),converse(X1)) = composition(top,converse(composition(X1,sFlat1))),
inference(cp,[status(thm)],[t884,t29]) ).
cnf(t16318,plain,
converse(composition(X1,sFlat2)) = composition(top,converse(composition(X1,sFlat1))),
inference(step,[status(thm)],[t885,t29]) ).
cnf(t908,plain,
composition(top,converse(composition(X1,sFlat1))) = converse(composition(X1,sFlat2)),
inference(orient,[status(thm)],[t16318]) ).
cnf(t53,plain,
composition(sk1,composition(top,X1)) = composition(sFlat0,X1),
inference(cp,[status(thm)],[t24,t50]) ).
cnf(t149,plain,
composition(sk1,composition(top,X1)) = composition(sFlat0,X1),
inference(orient,[status(thm)],[t53]) ).
cnf(t113,plain,
top = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t64,t111]) ).
cnf(t118,plain,
join(sFlat0,sFlat1) = top,
inference(orient,[status(thm)],[t113]) ).
cnf(t119,plain,
join(sFlat0,join(sFlat1,X1)) = join(top,X1),
inference(cp,[status(thm)],[t59,t118]) ).
cnf(t178,plain,
join(sFlat0,join(sFlat1,X1)) = join(top,X1),
inference(orient,[status(thm)],[t119]) ).
cnf(t16302,plain,
join(sFlat0,join(sFlat1,X1)) = top,
inference(step,[status(thm)],[t178,t670]) ).
cnf(t671,plain,
join(sFlat0,join(sFlat1,X1)) = top,
inference(orient,[status(thm)],[t16302]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t739,plain,
composition(join(top,X1),converse(sFlat1)) = join(converse(sFlat2),composition(X1,converse(sFlat1))),
inference(cp,[status(thm)],[t26,t736]) ).
cnf(t16320,plain,
composition(top,converse(sFlat1)) = join(converse(sFlat2),composition(X1,converse(sFlat1))),
inference(step,[status(thm)],[t739,t670]) ).
cnf(t16321,plain,
converse(sFlat2) = join(converse(sFlat2),composition(X1,converse(sFlat1))),
inference(step,[status(thm)],[t16320,t736]) ).
cnf(t936,plain,
join(converse(sFlat2),composition(X1,converse(sFlat1))) = converse(sFlat2),
inference(orient,[status(thm)],[t16321]) ).
cnf(t938,plain,
converse(sFlat2) = join(converse(sFlat2),converse(sFlat1)),
inference(cp,[status(thm)],[t936,t269]) ).
cnf(t16322,plain,
converse(sFlat2) = converse(join(sFlat2,sFlat1)),
inference(step,[status(thm)],[t938,t74]) ).
cnf(t16323,plain,
converse(sFlat2) = converse(join(sFlat1,sFlat2)),
inference(step,[status(thm)],[t16322,t56]) ).
cnf(t943,plain,
converse(join(sFlat1,sFlat2)) = converse(sFlat2),
inference(orient,[status(thm)],[t16323]) ).
cnf(t944,plain,
join(sFlat1,sFlat2) = converse(converse(sFlat2)),
inference(cp,[status(thm)],[t23,t943]) ).
cnf(t16324,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t944,t23]) ).
cnf(t956,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t16324]) ).
cnf(t959,plain,
top = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t671,t956]) ).
cnf(t961,plain,
join(sFlat0,sFlat2) = top,
inference(orient,[status(thm)],[t959]) ).
cnf(t963,plain,
join(sFlat0,join(sFlat2,X1)) = join(top,X1),
inference(cp,[status(thm)],[t59,t961]) ).
cnf(t16325,plain,
join(sFlat0,join(sFlat2,X1)) = top,
inference(step,[status(thm)],[t963,t670]) ).
cnf(t964,plain,
join(sFlat0,join(sFlat2,X1)) = top,
inference(orient,[status(thm)],[t16325]) ).
cnf(t121,plain,
composition(join(sFlat1,X1),top) = join(sFlat2,composition(X1,top)),
inference(cp,[status(thm)],[t26,t120]) ).
cnf(t515,plain,
composition(join(sFlat1,X1),top) = join(sFlat2,composition(X1,top)),
inference(orient,[status(thm)],[t121]) ).
cnf(t524,plain,
join(sFlat2,composition(complement(sFlat1),top)) = composition(top,top),
inference(cp,[status(thm)],[t515,t64]) ).
cnf(t823,plain,
join(sFlat2,composition(complement(sFlat1),top)) = composition(top,top),
inference(orient,[status(thm)],[t524]) ).
cnf(t965,plain,
top = join(sFlat0,composition(top,top)),
inference(cp,[status(thm)],[t964,t823]) ).
cnf(t51,plain,
composition(join(sk1,X1),top) = join(sFlat0,composition(X1,top)),
inference(cp,[status(thm)],[t26,t50]) ).
cnf(t496,plain,
composition(join(sk1,X1),top) = join(sFlat0,composition(X1,top)),
inference(orient,[status(thm)],[t51]) ).
cnf(t662,plain,
join(sFlat0,composition(top,top)) = composition(top,top),
inference(cp,[status(thm)],[t496,t660]) ).
cnf(t819,plain,
join(sFlat0,composition(top,top)) = composition(top,top),
inference(orient,[status(thm)],[t662]) ).
cnf(t16326,plain,
top = composition(top,top),
inference(step,[status(thm)],[t965,t819]) ).
cnf(t969,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t16326]) ).
cnf(t977,plain,
composition(sFlat0,top) = composition(sk1,top),
inference(cp,[status(thm)],[t149,t969]) ).
cnf(t16334,plain,
composition(sFlat0,top) = sFlat0,
inference(step,[status(thm)],[t977,t50]) ).
cnf(t994,plain,
composition(sFlat0,top) = sFlat0,
inference(orient,[status(thm)],[t16334]) ).
cnf(t1003,plain,
complement(top) = join(complement(top),composition(converse(sFlat0),complement(sFlat0))),
inference(cp,[status(thm)],[t67,t994]) ).
cnf(t100,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t99,t64]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t106,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t16245,plain,
zero = complement(top),
inference(step,[status(thm)],[t100,t106]) ).
cnf(t128,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t16245]) ).
cnf(t16346,plain,
zero = join(complement(top),composition(converse(sFlat0),complement(sFlat0))),
inference(step,[status(thm)],[t1003,t128]) ).
cnf(t16347,plain,
zero = join(zero,composition(converse(sFlat0),complement(sFlat0))),
inference(step,[status(thm)],[t16346,t128]) ).
cnf(t16348,plain,
zero = join(zero,composition(converse(sFlat0),sFlat1)),
inference(step,[status(thm)],[t16347,t111]) ).
cnf(t1209,plain,
join(zero,composition(converse(sFlat0),sFlat1)) = zero,
inference(orient,[status(thm)],[t16348]) ).
cnf(t302,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t298,t128]) ).
cnf(t16256,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t302,t128]) ).
cnf(t16257,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t16256,t128]) ).
cnf(t317,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t16257]) ).
cnf(t318,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t59,t317]) ).
cnf(t368,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t318]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t58,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t20]) ).
cnf(t16978,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t58,t56]) ).
cnf(t16979,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t16978,t99]) ).
cnf(t16980,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t16979,t56]) ).
cnf(t15192,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t16980]) ).
cnf(t15193,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t15192,t106]) ).
cnf(t17013,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t15193,t99]) ).
cnf(t15564,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t17013]) ).
cnf(t15572,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t368,t15564]) ).
cnf(t17023,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t15572,t15564]) ).
cnf(t15660,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t17023]) ).
cnf(t17073,plain,
composition(converse(sFlat0),sFlat1) = zero,
inference(step,[status(thm)],[t1209,t15660]) ).
cnf(t15747,plain,
composition(converse(sFlat0),sFlat1) = zero,
inference(rw,[status(thm)],[t17073]) ).
cnf(t16088,plain,
composition(converse(sFlat0),sFlat1) = zero,
inference(orient,[status(thm)],[t15747]) ).
cnf(t16096,plain,
converse(composition(converse(sFlat0),sFlat2)) = composition(top,converse(zero)),
inference(cp,[status(thm)],[t908,t16088]) ).
cnf(t17177,plain,
composition(converse(sFlat2),sFlat0) = composition(top,converse(zero)),
inference(step,[status(thm)],[t16096,t235]) ).
cnf(t17030,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t15564,t15660]) ).
cnf(t15707,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t17030]) ).
cnf(t15837,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t15707]) ).
cnf(t17107,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t354,t15837]) ).
cnf(t15872,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t17107]) ).
cnf(t15919,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t15872]) ).
cnf(t16312,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t458,t704]) ).
cnf(t707,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t16312]) ).
cnf(t15675,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t15660,t707]) ).
cnf(t16001,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t15675]) ).
cnf(t16002,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t23,t16001]) ).
cnf(t17136,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t16002,t704]) ).
cnf(t16039,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t17136]) ).
cnf(t16040,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t15919,t16039]) ).
cnf(t17137,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t16040,t128]) ).
cnf(t16049,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t17137]) ).
cnf(t17178,plain,
composition(converse(sFlat2),sFlat0) = composition(top,zero),
inference(step,[status(thm)],[t17177,t16049]) ).
cnf(t15,axiom,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t15]) ).
cnf(t131,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t99,t128]) ).
cnf(t188,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t131]) ).
cnf(t65,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t64,t59]) ).
cnf(t1772,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t65]) ).
cnf(t1823,plain,
top = join(X1,join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t1772,t56]) ).
cnf(t2244,plain,
join(X1,join(X2,complement(join(X2,X1)))) = top,
inference(orient,[status(thm)],[t1823]) ).
cnf(t2267,plain,
top = join(complement(X1),join(X1,complement(top))),
inference(cp,[status(thm)],[t2244,t64]) ).
cnf(t16457,plain,
top = join(complement(X1),join(X1,zero)),
inference(step,[status(thm)],[t2267,t128]) ).
cnf(t2387,plain,
join(complement(X1),join(X1,zero)) = top,
inference(orient,[status(thm)],[t16457]) ).
cnf(t2399,plain,
top = join(complement(X1),join(zero,X1)),
inference(cp,[status(thm)],[t2387,t56]) ).
cnf(t2405,plain,
join(complement(X1),join(zero,X1)) = top,
inference(orient,[status(thm)],[t2399]) ).
cnf(t2418,plain,
top = join(complement(composition(converse(sFlat0),sFlat1)),zero),
inference(cp,[status(thm)],[t2405,t1209]) ).
cnf(t16472,plain,
top = join(zero,complement(composition(converse(sFlat0),sFlat1))),
inference(step,[status(thm)],[t2418,t56]) ).
cnf(t2448,plain,
join(zero,complement(composition(converse(sFlat0),sFlat1))) = top,
inference(orient,[status(thm)],[t16472]) ).
cnf(t2451,plain,
meet(top,composition(converse(sFlat0),sFlat1)) = complement(top),
inference(cp,[status(thm)],[t188,t2448]) ).
cnf(t16473,plain,
meet(top,composition(converse(sFlat0),sFlat1)) = zero,
inference(step,[status(thm)],[t2451,t128]) ).
cnf(t2453,plain,
meet(top,composition(converse(sFlat0),sFlat1)) = zero,
inference(orient,[status(thm)],[t16473]) ).
cnf(t2456,plain,
composition(meet(sFlat0,composition(sFlat1,converse(top))),meet(top,composition(converse(sFlat0),sFlat1))) = join(meet(composition(sFlat0,top),sFlat1),composition(meet(sFlat0,composition(sFlat1,converse(top))),zero)),
inference(cp,[status(thm)],[t35,t2453]) ).
cnf(t16474,plain,
composition(meet(sFlat0,composition(sFlat1,top)),meet(top,composition(converse(sFlat0),sFlat1))) = join(meet(composition(sFlat0,top),sFlat1),composition(meet(sFlat0,composition(sFlat1,converse(top))),zero)),
inference(step,[status(thm)],[t2456,t704]) ).
cnf(t16475,plain,
composition(meet(sFlat0,sFlat2),meet(top,composition(converse(sFlat0),sFlat1))) = join(meet(composition(sFlat0,top),sFlat1),composition(meet(sFlat0,composition(sFlat1,converse(top))),zero)),
inference(step,[status(thm)],[t16474,t120]) ).
cnf(t16476,plain,
composition(meet(sFlat0,sFlat2),zero) = join(meet(composition(sFlat0,top),sFlat1),composition(meet(sFlat0,composition(sFlat1,converse(top))),zero)),
inference(step,[status(thm)],[t16475,t2453]) ).
cnf(t101,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t99,t56]) ).
cnf(t16247,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t101,t99]) ).
cnf(t137,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t16247]) ).
cnf(t16477,plain,
composition(meet(sFlat0,sFlat2),zero) = join(meet(sFlat1,composition(sFlat0,top)),composition(meet(sFlat0,composition(sFlat1,converse(top))),zero)),
inference(step,[status(thm)],[t16476,t137]) ).
cnf(t16478,plain,
composition(meet(sFlat0,sFlat2),zero) = join(meet(sFlat1,sFlat0),composition(meet(sFlat0,composition(sFlat1,converse(top))),zero)),
inference(step,[status(thm)],[t16477,t994]) ).
cnf(t16479,plain,
composition(meet(sFlat0,sFlat2),zero) = join(meet(sFlat0,sFlat1),composition(meet(sFlat0,composition(sFlat1,converse(top))),zero)),
inference(step,[status(thm)],[t16478,t137]) ).
cnf(t112,plain,
zero = meet(sFlat0,sFlat1),
inference(cp,[status(thm)],[t106,t111]) ).
cnf(t117,plain,
meet(sFlat0,sFlat1) = zero,
inference(orient,[status(thm)],[t112]) ).
cnf(t16480,plain,
composition(meet(sFlat0,sFlat2),zero) = join(zero,composition(meet(sFlat0,composition(sFlat1,converse(top))),zero)),
inference(step,[status(thm)],[t16479,t117]) ).
cnf(t981,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t67,t969]) ).
cnf(t16336,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t981,t128]) ).
cnf(t16337,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t16336,t128]) ).
cnf(t16338,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t16337,t704]) ).
cnf(t16339,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t16338,t128]) ).
cnf(t1035,plain,
join(zero,composition(top,zero)) = zero,
inference(orient,[status(thm)],[t16339]) ).
cnf(t1036,plain,
join(zero,join(composition(top,zero),X1)) = join(zero,X1),
inference(cp,[status(thm)],[t59,t1035]) ).
cnf(t1527,plain,
join(zero,join(composition(top,zero),X1)) = join(zero,X1),
inference(orient,[status(thm)],[t1036]) ).
cnf(t1528,plain,
join(zero,composition(X1,zero)) = join(zero,composition(join(top,X1),zero)),
inference(cp,[status(thm)],[t1527,t26]) ).
cnf(t16386,plain,
join(zero,composition(X1,zero)) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t1528,t670]) ).
cnf(t16387,plain,
join(zero,composition(X1,zero)) = zero,
inference(step,[status(thm)],[t16386,t1035]) ).
cnf(t1535,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t16387]) ).
cnf(t16481,plain,
composition(meet(sFlat0,sFlat2),zero) = zero,
inference(step,[status(thm)],[t16480,t1535]) ).
cnf(t2457,plain,
composition(meet(sFlat0,sFlat2),zero) = zero,
inference(orient,[status(thm)],[t16481]) ).
cnf(t2459,plain,
composition(join(meet(sFlat0,sFlat2),X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t26,t2457]) ).
cnf(t16482,plain,
composition(join(meet(sFlat0,sFlat2),X1),zero) = zero,
inference(step,[status(thm)],[t2459,t1535]) ).
cnf(t2478,plain,
composition(join(meet(sFlat0,sFlat2),X1),zero) = zero,
inference(orient,[status(thm)],[t16482]) ).
cnf(t1784,plain,
top = join(X1,join(converse(complement(converse(X1))),complement(top))),
inference(cp,[status(thm)],[t1772,t707]) ).
cnf(t16449,plain,
top = join(X1,join(complement(top),converse(complement(converse(X1))))),
inference(step,[status(thm)],[t1784,t56]) ).
cnf(t16450,plain,
top = join(X1,join(zero,converse(complement(converse(X1))))),
inference(step,[status(thm)],[t16449,t128]) ).
cnf(t2216,plain,
join(X1,join(zero,converse(complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t16450]) ).
cnf(t2480,plain,
zero = composition(top,zero),
inference(cp,[status(thm)],[t2478,t2216]) ).
cnf(t2502,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t2480]) ).
cnf(t17179,plain,
composition(converse(sFlat2),sFlat0) = zero,
inference(step,[status(thm)],[t17178,t2502]) ).
cnf(t16113,plain,
composition(converse(sFlat2),sFlat0) = zero,
inference(orient,[status(thm)],[t17179]) ).
cnf(t16130,plain,
complement(sFlat0) = join(complement(sFlat0),composition(converse(converse(sFlat2)),complement(zero))),
inference(cp,[status(thm)],[t67,t16113]) ).
cnf(t17180,plain,
sFlat1 = join(complement(sFlat0),composition(converse(converse(sFlat2)),complement(zero))),
inference(step,[status(thm)],[t16130,t111]) ).
cnf(t17181,plain,
sFlat1 = join(sFlat1,composition(converse(converse(sFlat2)),complement(zero))),
inference(step,[status(thm)],[t17180,t111]) ).
cnf(t17182,plain,
sFlat1 = join(sFlat1,composition(sFlat2,complement(zero))),
inference(step,[status(thm)],[t17181,t23]) ).
cnf(t15674,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t15660,t64]) ).
cnf(t15760,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t15674]) ).
cnf(t17183,plain,
sFlat1 = join(sFlat1,composition(sFlat2,top)),
inference(step,[status(thm)],[t17182,t15760]) ).
cnf(t123,plain,
composition(sFlat1,composition(top,X1)) = composition(sFlat2,X1),
inference(cp,[status(thm)],[t24,t120]) ).
cnf(t183,plain,
composition(sFlat1,composition(top,X1)) = composition(sFlat2,X1),
inference(orient,[status(thm)],[t123]) ).
cnf(t976,plain,
composition(sFlat2,top) = composition(sFlat1,top),
inference(cp,[status(thm)],[t183,t969]) ).
cnf(t16333,plain,
composition(sFlat2,top) = sFlat2,
inference(step,[status(thm)],[t976,t120]) ).
cnf(t983,plain,
composition(sFlat2,top) = sFlat2,
inference(orient,[status(thm)],[t16333]) ).
cnf(t17184,plain,
sFlat1 = join(sFlat1,sFlat2),
inference(step,[status(thm)],[t17183,t983]) ).
cnf(t17185,plain,
sFlat1 = sFlat2,
inference(step,[status(thm)],[t17184,t956]) ).
cnf(t16143,plain,
sFlat2 = sFlat1,
inference(orient,[status(thm)],[t17185]) ).
cnf(t17186,plain,
composition(sFlat1,top) = sFlat1,
inference(step,[status(thm)],[t120,t16143]) ).
cnf(t16144,plain,
composition(sFlat1,top) = sFlat1,
inference(orient,[status(thm)],[t17186]) ).
cnf(goal_0,negated_conjecture,
composition(complement(composition(sk1,top)),top) != complement(composition(sk1,top)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
composition(complement(sFlat0),top) != complement(composition(sk1,top)),
inference(rw,[status(thm)],[goal_0,t50]) ).
cnf(g0_1,plain,
composition(sFlat1,top) != complement(composition(sk1,top)),
inference(rw,[status(thm)],[g0_0,t111]) ).
cnf(g0_2,plain,
sFlat1 != complement(composition(sk1,top)),
inference(rw,[status(thm)],[g0_1,t16144]) ).
cnf(g0_3,plain,
sFlat1 != complement(sFlat0),
inference(rw,[status(thm)],[g0_2,t50]) ).
cnf(g0_4,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_3,t111]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL050-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n020.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 07:40:18 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 14.16/2.18 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.16/2.18 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------