%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL004-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n016.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:36 PM UTC 2026
% Result : Unsatisfiable 14.04s 2.25s
% Output : CNFRefutation 14.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 73
% Number of leaves : 16
% Syntax : Number of clauses : 287 ( 287 unt; 0 nHn; 163 RR)
% Number of literals : 287 ( 286 equ; 5 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 : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 167 ( 5 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t16,axiom,
sFlat0 = complement(sk1),
introduced(definition) ).
cnf(t126,plain,
complement(sk1) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t17,axiom,
sFlat1 = converse(complement(sk1)),
introduced(definition) ).
cnf(t49,plain,
converse(complement(sk1)) = sFlat1,
inference(orient,[status(thm)],[t17]) ).
cnf(t4646,plain,
converse(sFlat0) = sFlat1,
inference(step,[status(thm)],[t49,t126]) ).
cnf(t132,plain,
converse(sFlat0) = sFlat1,
inference(rw,[status(thm)],[t4646]) ).
cnf(t143,plain,
converse(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t132]) ).
cnf(t18,axiom,
sFlat2 = converse(sk1),
introduced(definition) ).
cnf(t57,plain,
converse(sk1) = sFlat2,
inference(orient,[status(thm)],[t18]) ).
cnf(t19,axiom,
sFlat3 = complement(converse(sk1)),
introduced(definition) ).
cnf(t4645,plain,
sFlat3 = complement(sFlat2),
inference(step,[status(thm)],[t19,t57]) ).
cnf(t120,plain,
complement(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t4645]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t69,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t65,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t4644,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t65]) ).
cnf(t78,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t4644]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t29,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t615,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t29]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t616,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t615,t20]) ).
cnf(t4679,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t616,t21]) ).
cnf(t636,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t4679]) ).
cnf(t637,plain,
one = converse(one),
inference(cp,[status(thm)],[t636,t20]) ).
cnf(t646,plain,
converse(one) = one,
inference(orient,[status(thm)],[t637]) ).
cnf(t4680,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t636,t646]) ).
cnf(t656,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t4680]) ).
cnf(t658,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t656]) ).
cnf(t661,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t78,t658]) ).
cnf(t4690,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t661,t646]) ).
cnf(t4691,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t4690,t658]) ).
cnf(t720,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t4691]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t108,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t727,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t720,t108]) ).
cnf(t4890,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t727,t108]) ).
cnf(t4891,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t4890,t108]) ).
cnf(t2212,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t4891]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t68,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t22]) ).
cnf(t4967,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t68,t65]) ).
cnf(t4968,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t4967,t108]) ).
cnf(t4969,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t4968,t65]) ).
cnf(t2991,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t4969]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t115,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t2992,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t2991,t115]) ).
cnf(t5031,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t2992,t108]) ).
cnf(t3124,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t5031]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t75,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t109,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t108,t75]) ).
cnf(t4648,plain,
zero = complement(top),
inference(step,[status(thm)],[t109,t115]) ).
cnf(t170,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t4648]) ).
cnf(t726,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t720,t170]) ).
cnf(t4692,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t726,t170]) ).
cnf(t4693,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t4692,t170]) ).
cnf(t741,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t4693]) ).
cnf(t742,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t69,t741]) ).
cnf(t844,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t742]) ).
cnf(t3126,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t844,t3124]) ).
cnf(t5033,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t3126,t3124]) ).
cnf(t3131,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t5033]) ).
cnf(t5034,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t3124,t3131]) ).
cnf(t3151,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t5034]) ).
cnf(t3237,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t3151]) ).
cnf(t3242,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t2212,t3237]) ).
cnf(t5069,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t3242,t3237]) ).
cnf(t5070,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t5069,t3237]) ).
cnf(t3270,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t5070]) ).
cnf(t3276,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t69,t3270]) ).
cnf(t4502,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t3276]) ).
cnf(t4511,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t4502,t2991]) ).
cnf(t5134,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t4511,t2991]) ).
cnf(t5135,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t5134,t65]) ).
cnf(t4531,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t5135]) ).
cnf(t110,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t108,t65]) ).
cnf(t4669,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t110,t108]) ).
cnf(t445,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4669]) ).
cnf(t4534,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t4531,t445]) ).
cnf(t4563,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t4534]) ).
cnf(t129,plain,
meet(sk1,X1) = complement(join(sFlat0,complement(X1))),
inference(cp,[status(thm)],[t108,t126]) ).
cnf(t487,plain,
complement(join(sFlat0,complement(X1))) = meet(sk1,X1),
inference(orient,[status(thm)],[t129]) ).
cnf(t492,plain,
meet(sk1,sk1) = complement(join(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t487,t126]) ).
cnf(t512,plain,
complement(join(sFlat0,sFlat0)) = meet(sk1,sk1),
inference(orient,[status(thm)],[t492]) ).
cnf(t58,plain,
sk1 = converse(sFlat2),
inference(cp,[status(thm)],[t21,t57]) ).
cnf(t133,plain,
converse(sFlat2) = sk1,
inference(orient,[status(thm)],[t58]) ).
cnf(t137,plain,
converse(composition(sFlat2,X1)) = composition(converse(X1),sk1),
inference(cp,[status(thm)],[t27,t133]) ).
cnf(t282,plain,
converse(composition(sFlat2,X1)) = composition(converse(X1),sk1),
inference(orient,[status(thm)],[t137]) ).
cnf(t283,plain,
composition(converse(one),sk1) = converse(sFlat2),
inference(cp,[status(thm)],[t282,t20]) ).
cnf(t4660,plain,
composition(converse(one),sk1) = sk1,
inference(step,[status(thm)],[t283,t133]) ).
cnf(t293,plain,
composition(converse(one),sk1) = sk1,
inference(orient,[status(thm)],[t4660]) ).
cnf(t297,plain,
complement(sk1) = join(complement(sk1),composition(converse(converse(one)),complement(sk1))),
inference(cp,[status(thm)],[t78,t293]) ).
cnf(t4661,plain,
sFlat0 = join(complement(sk1),composition(converse(converse(one)),complement(sk1))),
inference(step,[status(thm)],[t297,t126]) ).
cnf(t4662,plain,
sFlat0 = join(sFlat0,composition(converse(converse(one)),complement(sk1))),
inference(step,[status(thm)],[t4661,t126]) ).
cnf(t4663,plain,
sFlat0 = join(sFlat0,composition(one,complement(sk1))),
inference(step,[status(thm)],[t4662,t21]) ).
cnf(t4664,plain,
sFlat0 = join(sFlat0,composition(one,sFlat0)),
inference(step,[status(thm)],[t4663,t126]) ).
cnf(t303,plain,
join(sFlat0,composition(one,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t4664]) ).
cnf(t4684,plain,
join(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t303,t658]) ).
cnf(t665,plain,
join(sFlat0,sFlat0) = sFlat0,
inference(rw,[status(thm)],[t4684]) ).
cnf(t675,plain,
join(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t665]) ).
cnf(t4687,plain,
complement(sFlat0) = meet(sk1,sk1),
inference(step,[status(thm)],[t512,t675]) ).
cnf(t677,plain,
complement(sFlat0) = meet(sk1,sk1),
inference(rw,[status(thm)],[t4687]) ).
cnf(t683,plain,
meet(sk1,sk1) = complement(sFlat0),
inference(orient,[status(thm)],[t677]) ).
cnf(t3001,plain,
sk1 = join(complement(sFlat0),complement(join(complement(sk1),sk1))),
inference(cp,[status(thm)],[t2991,t683]) ).
cnf(t4970,plain,
sk1 = join(complement(sFlat0),complement(join(sk1,complement(sk1)))),
inference(step,[status(thm)],[t3001,t65]) ).
cnf(t4971,plain,
sk1 = join(complement(sFlat0),complement(top)),
inference(step,[status(thm)],[t4970,t75]) ).
cnf(t4972,plain,
sk1 = join(complement(sFlat0),zero),
inference(step,[status(thm)],[t4971,t170]) ).
cnf(t4973,plain,
sk1 = join(zero,complement(sFlat0)),
inference(step,[status(thm)],[t4972,t65]) ).
cnf(t3050,plain,
join(zero,complement(sFlat0)) = sk1,
inference(orient,[status(thm)],[t4973]) ).
cnf(t5036,plain,
complement(sFlat0) = sk1,
inference(step,[status(thm)],[t3050,t3131]) ).
cnf(t3153,plain,
complement(sFlat0) = sk1,
inference(rw,[status(thm)],[t5036]) ).
cnf(t3202,plain,
complement(sFlat0) = sk1,
inference(orient,[status(thm)],[t3153]) ).
cnf(t3211,plain,
meet(sFlat0,X1) = complement(join(sk1,complement(X1))),
inference(cp,[status(thm)],[t108,t3202]) ).
cnf(t4349,plain,
complement(join(sk1,complement(X1))) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t3211]) ).
cnf(t740,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t108,t720]) ).
cnf(t747,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t740]) ).
cnf(t5053,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t747,t3237]) ).
cnf(t3250,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t5053]) ).
cnf(t3279,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t3250]) ).
cnf(t4360,plain,
meet(sFlat0,complement(X1)) = complement(join(sk1,X1)),
inference(cp,[status(thm)],[t4349,t3279]) ).
cnf(t4381,plain,
complement(join(sk1,X1)) = meet(sFlat0,complement(X1)),
inference(orient,[status(thm)],[t4360]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t46,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t134,plain,
converse(join(sFlat2,X1)) = join(sk1,converse(X1)),
inference(cp,[status(thm)],[t46,t133]) ).
cnf(t242,plain,
converse(join(sFlat2,X1)) = join(sk1,converse(X1)),
inference(orient,[status(thm)],[t134]) ).
cnf(t122,plain,
top = join(sFlat2,sFlat3),
inference(cp,[status(thm)],[t75,t120]) ).
cnf(t165,plain,
join(sFlat2,sFlat3) = top,
inference(orient,[status(thm)],[t122]) ).
cnf(t244,plain,
join(sk1,converse(sFlat3)) = converse(top),
inference(cp,[status(thm)],[t242,t165]) ).
cnf(t255,plain,
join(sk1,converse(sFlat3)) = converse(top),
inference(orient,[status(thm)],[t244]) ).
cnf(t48,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t46,t21]) ).
cnf(t995,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t48]) ).
cnf(t166,plain,
join(sFlat2,join(sFlat3,X1)) = join(top,X1),
inference(cp,[status(thm)],[t69,t165]) ).
cnf(t520,plain,
join(sFlat2,join(sFlat3,X1)) = join(top,X1),
inference(orient,[status(thm)],[t166]) ).
cnf(t62,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sFlat2),
inference(cp,[status(thm)],[t27,t57]) ).
cnf(t218,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sFlat2),
inference(orient,[status(thm)],[t62]) ).
cnf(t219,plain,
composition(converse(one),sFlat2) = converse(sk1),
inference(cp,[status(thm)],[t218,t20]) ).
cnf(t4654,plain,
composition(converse(one),sFlat2) = sFlat2,
inference(step,[status(thm)],[t219,t57]) ).
cnf(t230,plain,
composition(converse(one),sFlat2) = sFlat2,
inference(orient,[status(thm)],[t4654]) ).
cnf(t234,plain,
complement(sFlat2) = join(complement(sFlat2),composition(converse(converse(one)),complement(sFlat2))),
inference(cp,[status(thm)],[t78,t230]) ).
cnf(t4655,plain,
sFlat3 = join(complement(sFlat2),composition(converse(converse(one)),complement(sFlat2))),
inference(step,[status(thm)],[t234,t120]) ).
cnf(t4656,plain,
sFlat3 = join(sFlat3,composition(converse(converse(one)),complement(sFlat2))),
inference(step,[status(thm)],[t4655,t120]) ).
cnf(t4657,plain,
sFlat3 = join(sFlat3,composition(one,complement(sFlat2))),
inference(step,[status(thm)],[t4656,t21]) ).
cnf(t4658,plain,
sFlat3 = join(sFlat3,composition(one,sFlat3)),
inference(step,[status(thm)],[t4657,t120]) ).
cnf(t240,plain,
join(sFlat3,composition(one,sFlat3)) = sFlat3,
inference(orient,[status(thm)],[t4658]) ).
cnf(t521,plain,
join(top,composition(one,sFlat3)) = join(sFlat2,sFlat3),
inference(cp,[status(thm)],[t520,t240]) ).
cnf(t4674,plain,
join(top,composition(one,sFlat3)) = top,
inference(step,[status(thm)],[t521,t165]) ).
cnf(t527,plain,
join(top,composition(one,sFlat3)) = top,
inference(orient,[status(thm)],[t4674]) ).
cnf(t4683,plain,
join(top,sFlat3) = top,
inference(step,[status(thm)],[t527,t658]) ).
cnf(t664,plain,
join(top,sFlat3) = top,
inference(rw,[status(thm)],[t4683]) ).
cnf(t4686,plain,
join(sFlat3,top) = top,
inference(step,[status(thm)],[t664,t65]) ).
cnf(t671,plain,
join(sFlat3,top) = top,
inference(orient,[status(thm)],[t4686]) ).
cnf(t674,plain,
join(sFlat3,join(top,X1)) = join(top,X1),
inference(cp,[status(thm)],[t69,t671]) ).
cnf(t823,plain,
join(sFlat3,join(top,X1)) = join(top,X1),
inference(orient,[status(thm)],[t674]) ).
cnf(t128,plain,
top = join(sk1,sFlat0),
inference(cp,[status(thm)],[t75,t126]) ).
cnf(t4647,plain,
top = join(sFlat0,sk1),
inference(step,[status(thm)],[t128,t65]) ).
cnf(t168,plain,
join(sFlat0,sk1) = top,
inference(orient,[status(thm)],[t4647]) ).
cnf(t169,plain,
join(sFlat0,join(sk1,X1)) = join(top,X1),
inference(cp,[status(thm)],[t69,t168]) ).
cnf(t529,plain,
join(sFlat0,join(sk1,X1)) = join(top,X1),
inference(orient,[status(thm)],[t169]) ).
cnf(t530,plain,
join(top,converse(sFlat3)) = join(sFlat0,converse(top)),
inference(cp,[status(thm)],[t529,t255]) ).
cnf(t534,plain,
join(top,converse(sFlat3)) = join(sFlat0,converse(top)),
inference(orient,[status(thm)],[t530]) ).
cnf(t144,plain,
sFlat0 = converse(sFlat1),
inference(cp,[status(thm)],[t21,t143]) ).
cnf(t154,plain,
converse(sFlat1) = sFlat0,
inference(orient,[status(thm)],[t144]) ).
cnf(t155,plain,
converse(join(sFlat1,X1)) = join(sFlat0,converse(X1)),
inference(cp,[status(thm)],[t46,t154]) ).
cnf(t368,plain,
converse(join(sFlat1,X1)) = join(sFlat0,converse(X1)),
inference(orient,[status(thm)],[t155]) ).
cnf(t145,plain,
converse(join(sFlat0,X1)) = join(sFlat1,converse(X1)),
inference(cp,[status(thm)],[t46,t143]) ).
cnf(t305,plain,
converse(join(sFlat0,X1)) = join(sFlat1,converse(X1)),
inference(orient,[status(thm)],[t145]) ).
cnf(t308,plain,
join(sFlat1,converse(composition(one,sFlat0))) = converse(sFlat0),
inference(cp,[status(thm)],[t305,t303]) ).
cnf(t147,plain,
converse(composition(X1,sFlat0)) = composition(sFlat1,converse(X1)),
inference(cp,[status(thm)],[t27,t143]) ).
cnf(t334,plain,
converse(composition(X1,sFlat0)) = composition(sFlat1,converse(X1)),
inference(orient,[status(thm)],[t147]) ).
cnf(t4677,plain,
join(sFlat1,composition(sFlat1,converse(one))) = converse(sFlat0),
inference(step,[status(thm)],[t308,t334]) ).
cnf(t4678,plain,
join(sFlat1,composition(sFlat1,converse(one))) = sFlat1,
inference(step,[status(thm)],[t4677,t143]) ).
cnf(t587,plain,
join(sFlat1,composition(sFlat1,converse(one))) = sFlat1,
inference(orient,[status(thm)],[t4678]) ).
cnf(t4681,plain,
join(sFlat1,composition(sFlat1,one)) = sFlat1,
inference(step,[status(thm)],[t587,t646]) ).
cnf(t4682,plain,
join(sFlat1,sFlat1) = sFlat1,
inference(step,[status(thm)],[t4681,t20]) ).
cnf(t657,plain,
join(sFlat1,sFlat1) = sFlat1,
inference(rw,[status(thm)],[t4682]) ).
cnf(t667,plain,
join(sFlat1,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t657]) ).
cnf(t670,plain,
join(sFlat1,join(sFlat1,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t69,t667]) ).
cnf(t762,plain,
join(sFlat1,join(sFlat1,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t670]) ).
cnf(t765,plain,
join(sFlat1,complement(sFlat1)) = join(sFlat1,top),
inference(cp,[status(thm)],[t762,t75]) ).
cnf(t4695,plain,
top = join(sFlat1,top),
inference(step,[status(thm)],[t765,t75]) ).
cnf(t768,plain,
join(sFlat1,top) = top,
inference(orient,[status(thm)],[t4695]) ).
cnf(t770,plain,
join(sFlat0,converse(top)) = converse(top),
inference(cp,[status(thm)],[t368,t768]) ).
cnf(t819,plain,
join(sFlat0,converse(top)) = converse(top),
inference(orient,[status(thm)],[t770]) ).
cnf(t4699,plain,
join(top,converse(sFlat3)) = converse(top),
inference(step,[status(thm)],[t534,t819]) ).
cnf(t820,plain,
join(top,converse(sFlat3)) = converse(top),
inference(orient,[status(thm)],[t4699]) ).
cnf(t825,plain,
join(top,converse(sFlat3)) = join(sFlat3,converse(top)),
inference(cp,[status(thm)],[t823,t820]) ).
cnf(t4701,plain,
converse(top) = join(sFlat3,converse(top)),
inference(step,[status(thm)],[t825,t820]) ).
cnf(t829,plain,
join(sFlat3,converse(top)) = converse(top),
inference(orient,[status(thm)],[t4701]) ).
cnf(t996,plain,
join(converse(sFlat3),top) = converse(converse(top)),
inference(cp,[status(thm)],[t995,t829]) ).
cnf(t4712,plain,
join(top,converse(sFlat3)) = converse(converse(top)),
inference(step,[status(thm)],[t996,t65]) ).
cnf(t4713,plain,
converse(top) = converse(converse(top)),
inference(step,[status(thm)],[t4712,t820]) ).
cnf(t4714,plain,
converse(top) = top,
inference(step,[status(thm)],[t4713,t21]) ).
cnf(t1040,plain,
converse(top) = top,
inference(orient,[status(thm)],[t4714]) ).
cnf(t4717,plain,
join(sk1,converse(sFlat3)) = top,
inference(step,[status(thm)],[t255,t1040]) ).
cnf(t1043,plain,
join(sk1,converse(sFlat3)) = top,
inference(orient,[status(thm)],[t4717]) ).
cnf(t4414,plain,
meet(sFlat0,complement(converse(sFlat3))) = complement(top),
inference(cp,[status(thm)],[t4381,t1043]) ).
cnf(t5131,plain,
meet(sFlat0,complement(converse(sFlat3))) = zero,
inference(step,[status(thm)],[t4414,t170]) ).
cnf(t4446,plain,
meet(sFlat0,complement(converse(sFlat3))) = zero,
inference(orient,[status(thm)],[t5131]) ).
cnf(t4447,plain,
sFlat0 = join(zero,complement(join(complement(sFlat0),complement(converse(sFlat3))))),
inference(cp,[status(thm)],[t2991,t4446]) ).
cnf(t5132,plain,
sFlat0 = complement(join(complement(sFlat0),complement(converse(sFlat3)))),
inference(step,[status(thm)],[t4447,t3131]) ).
cnf(t5133,plain,
sFlat0 = meet(sFlat0,converse(sFlat3)),
inference(step,[status(thm)],[t5132,t108]) ).
cnf(t4448,plain,
meet(sFlat0,converse(sFlat3)) = sFlat0,
inference(orient,[status(thm)],[t5133]) ).
cnf(t4566,plain,
converse(sFlat3) = join(converse(sFlat3),sFlat0),
inference(cp,[status(thm)],[t4563,t4448]) ).
cnf(t5136,plain,
converse(sFlat3) = join(sFlat0,converse(sFlat3)),
inference(step,[status(thm)],[t4566,t65]) ).
cnf(t4685,plain,
join(sFlat3,sFlat3) = sFlat3,
inference(step,[status(thm)],[t240,t658]) ).
cnf(t666,plain,
join(sFlat3,sFlat3) = sFlat3,
inference(rw,[status(thm)],[t4685]) ).
cnf(t678,plain,
join(sFlat3,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t666]) ).
cnf(t681,plain,
join(sFlat3,join(sFlat3,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t69,t678]) ).
cnf(t841,plain,
join(sFlat3,join(sFlat3,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t681]) ).
cnf(t121,plain,
zero = meet(sFlat2,sFlat3),
inference(cp,[status(thm)],[t115,t120]) ).
cnf(t164,plain,
meet(sFlat2,sFlat3) = zero,
inference(orient,[status(thm)],[t121]) ).
cnf(t3003,plain,
sFlat2 = join(zero,complement(join(complement(sFlat2),sFlat3))),
inference(cp,[status(thm)],[t2991,t164]) ).
cnf(t4999,plain,
sFlat2 = join(zero,complement(join(sFlat3,complement(sFlat2)))),
inference(step,[status(thm)],[t3003,t65]) ).
cnf(t123,plain,
meet(sFlat2,X1) = complement(join(sFlat3,complement(X1))),
inference(cp,[status(thm)],[t108,t120]) ).
cnf(t455,plain,
complement(join(sFlat3,complement(X1))) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t123]) ).
cnf(t5000,plain,
sFlat2 = join(zero,meet(sFlat2,sFlat2)),
inference(step,[status(thm)],[t4999,t455]) ).
cnf(t459,plain,
meet(sFlat2,sFlat2) = complement(join(sFlat3,sFlat3)),
inference(cp,[status(thm)],[t455,t120]) ).
cnf(t480,plain,
complement(join(sFlat3,sFlat3)) = meet(sFlat2,sFlat2),
inference(orient,[status(thm)],[t459]) ).
cnf(t4688,plain,
complement(sFlat3) = meet(sFlat2,sFlat2),
inference(step,[status(thm)],[t480,t678]) ).
cnf(t682,plain,
complement(sFlat3) = meet(sFlat2,sFlat2),
inference(rw,[status(thm)],[t4688]) ).
cnf(t684,plain,
meet(sFlat2,sFlat2) = complement(sFlat3),
inference(orient,[status(thm)],[t682]) ).
cnf(t5001,plain,
sFlat2 = join(zero,complement(sFlat3)),
inference(step,[status(thm)],[t5000,t684]) ).
cnf(t3083,plain,
join(zero,complement(sFlat3)) = sFlat2,
inference(orient,[status(thm)],[t5001]) ).
cnf(t5035,plain,
complement(sFlat3) = sFlat2,
inference(step,[status(thm)],[t3083,t3131]) ).
cnf(t3152,plain,
complement(sFlat3) = sFlat2,
inference(rw,[status(thm)],[t5035]) ).
cnf(t3173,plain,
complement(sFlat3) = sFlat2,
inference(orient,[status(thm)],[t3152]) ).
cnf(t3184,plain,
meet(sFlat3,X1) = complement(join(sFlat2,complement(X1))),
inference(cp,[status(thm)],[t108,t3173]) ).
cnf(t4147,plain,
complement(join(sFlat2,complement(X1))) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t3184]) ).
cnf(t4156,plain,
meet(sFlat3,complement(X1)) = complement(join(sFlat2,X1)),
inference(cp,[status(thm)],[t4147,t3279]) ).
cnf(t4224,plain,
complement(join(sFlat2,X1)) = meet(sFlat3,complement(X1)),
inference(orient,[status(thm)],[t4156]) ).
cnf(t47,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t46,t21]) ).
cnf(t960,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t47]) ).
cnf(t966,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t960,t75]) ).
cnf(t4737,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t966,t1040]) ).
cnf(t1167,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t4737]) ).
cnf(t4262,plain,
meet(sFlat3,complement(converse(complement(converse(sFlat2))))) = complement(top),
inference(cp,[status(thm)],[t4224,t1167]) ).
cnf(t5117,plain,
meet(sFlat3,complement(converse(complement(sk1)))) = complement(top),
inference(step,[status(thm)],[t4262,t133]) ).
cnf(t5118,plain,
meet(sFlat3,complement(converse(sFlat0))) = complement(top),
inference(step,[status(thm)],[t5117,t126]) ).
cnf(t5119,plain,
meet(sFlat3,complement(sFlat1)) = complement(top),
inference(step,[status(thm)],[t5118,t143]) ).
cnf(t5120,plain,
meet(sFlat3,complement(sFlat1)) = zero,
inference(step,[status(thm)],[t5119,t170]) ).
cnf(t4284,plain,
meet(sFlat3,complement(sFlat1)) = zero,
inference(orient,[status(thm)],[t5120]) ).
cnf(t4285,plain,
sFlat3 = join(zero,complement(join(complement(sFlat3),complement(sFlat1)))),
inference(cp,[status(thm)],[t2991,t4284]) ).
cnf(t5121,plain,
sFlat3 = complement(join(complement(sFlat3),complement(sFlat1))),
inference(step,[status(thm)],[t4285,t3131]) ).
cnf(t5122,plain,
sFlat3 = meet(sFlat3,sFlat1),
inference(step,[status(thm)],[t5121,t108]) ).
cnf(t5123,plain,
sFlat3 = meet(sFlat1,sFlat3),
inference(step,[status(thm)],[t5122,t445]) ).
cnf(t4286,plain,
meet(sFlat1,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t5123]) ).
cnf(t4287,plain,
sFlat1 = join(sFlat3,complement(join(complement(sFlat1),sFlat3))),
inference(cp,[status(thm)],[t2991,t4286]) ).
cnf(t760,plain,
meet(sFlat2,complement(X1)) = complement(join(sFlat3,meet(X1,X1))),
inference(cp,[status(thm)],[t455,t747]) ).
cnf(t1600,plain,
complement(join(sFlat3,meet(X1,X1))) = meet(sFlat2,complement(X1)),
inference(orient,[status(thm)],[t760]) ).
cnf(t5059,plain,
complement(join(sFlat3,X1)) = meet(sFlat2,complement(X1)),
inference(step,[status(thm)],[t1600,t3237]) ).
cnf(t3256,plain,
complement(join(sFlat3,X1)) = meet(sFlat2,complement(X1)),
inference(rw,[status(thm)],[t5059]) ).
cnf(t3494,plain,
complement(join(sFlat3,X1)) = meet(sFlat2,complement(X1)),
inference(orient,[status(thm)],[t3256]) ).
cnf(t3510,plain,
meet(sFlat2,complement(X1)) = complement(join(X1,sFlat3)),
inference(cp,[status(thm)],[t3494,t65]) ).
cnf(t4107,plain,
complement(join(X1,sFlat3)) = meet(sFlat2,complement(X1)),
inference(orient,[status(thm)],[t3510]) ).
cnf(t5124,plain,
sFlat1 = join(sFlat3,meet(sFlat2,complement(complement(sFlat1)))),
inference(step,[status(thm)],[t4287,t4107]) ).
cnf(t5125,plain,
sFlat1 = join(sFlat3,meet(sFlat2,sFlat1)),
inference(step,[status(thm)],[t5124,t3279]) ).
cnf(t5126,plain,
sFlat1 = join(sFlat3,meet(sFlat1,sFlat2)),
inference(step,[status(thm)],[t5125,t445]) ).
cnf(t4288,plain,
join(sFlat3,meet(sFlat1,sFlat2)) = sFlat1,
inference(orient,[status(thm)],[t5126]) ).
cnf(t4290,plain,
join(sFlat3,meet(sFlat1,sFlat2)) = join(sFlat3,sFlat1),
inference(cp,[status(thm)],[t841,t4288]) ).
cnf(t5127,plain,
sFlat1 = join(sFlat3,sFlat1),
inference(step,[status(thm)],[t4290,t4288]) ).
cnf(t5128,plain,
sFlat1 = join(sFlat1,sFlat3),
inference(step,[status(thm)],[t5127,t65]) ).
cnf(t4299,plain,
join(sFlat1,sFlat3) = sFlat1,
inference(orient,[status(thm)],[t5128]) ).
cnf(t4302,plain,
join(sFlat0,converse(sFlat3)) = converse(sFlat1),
inference(cp,[status(thm)],[t368,t4299]) ).
cnf(t5129,plain,
join(sFlat0,converse(sFlat3)) = sFlat0,
inference(step,[status(thm)],[t4302,t154]) ).
cnf(t4312,plain,
join(sFlat0,converse(sFlat3)) = sFlat0,
inference(orient,[status(thm)],[t5129]) ).
cnf(t5137,plain,
converse(sFlat3) = sFlat0,
inference(step,[status(thm)],[t5136,t4312]) ).
cnf(t4589,plain,
converse(sFlat3) = sFlat0,
inference(orient,[status(thm)],[t5137]) ).
cnf(t4590,plain,
sFlat3 = converse(sFlat0),
inference(cp,[status(thm)],[t21,t4589]) ).
cnf(t5141,plain,
sFlat3 = sFlat1,
inference(step,[status(thm)],[t4590,t143]) ).
cnf(t4612,plain,
sFlat3 = sFlat1,
inference(orient,[status(thm)],[t5141]) ).
cnf(t5142,plain,
complement(sFlat2) = sFlat1,
inference(step,[status(thm)],[t120,t4612]) ).
cnf(t4613,plain,
complement(sFlat2) = sFlat1,
inference(orient,[status(thm)],[t5142]) ).
cnf(goal_0,negated_conjecture,
converse(complement(sk1)) != complement(converse(sk1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
converse(sFlat0) != complement(converse(sk1)),
inference(rw,[status(thm)],[goal_0,t126]) ).
cnf(g0_1,plain,
sFlat1 != complement(converse(sk1)),
inference(rw,[status(thm)],[g0_0,t143]) ).
cnf(g0_2,plain,
sFlat1 != complement(sFlat2),
inference(rw,[status(thm)],[g0_1,t57]) ).
cnf(g0_3,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_2,t4613]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL004-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.37 % Computer : n016.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Thu Sep 24 07:10:27 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 14.04/2.25 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.04/2.25 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------