%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL021-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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:49 PM UTC 2026
% Result : Unsatisfiable 38.28s 5.25s
% Output : CNFRefutation 38.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 23
% Syntax : Number of clauses : 262 ( 262 unt; 0 nHn; 153 RR)
% Number of literals : 262 ( 261 equ; 22 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 : 19 ( 19 usr; 14 con; 0-2 aty)
% Number of variables : 158 ( 24 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t133,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t21,axiom,
sFlat5 = complement(sk2),
introduced(definition) ).
cnf(t107,plain,
complement(sk2) = sFlat5,
inference(orient,[status(thm)],[t21]) ).
cnf(t16,axiom,
sFlat0 = complement(sk1),
introduced(definition) ).
cnf(t92,plain,
complement(sk1) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t22,axiom,
sFlat6 = join(complement(sk1),complement(sk2)),
introduced(definition) ).
cnf(t22976,plain,
sFlat6 = join(complement(sk2),complement(sk1)),
inference(step,[status(thm)],[t22,t133]) ).
cnf(t22977,plain,
sFlat6 = join(sFlat5,complement(sk1)),
inference(step,[status(thm)],[t22976,t107]) ).
cnf(t22978,plain,
sFlat6 = join(sFlat5,sFlat0),
inference(step,[status(thm)],[t22977,t92]) ).
cnf(t22979,plain,
sFlat6 = join(sFlat0,sFlat5),
inference(step,[status(thm)],[t22978,t133]) ).
cnf(t167,plain,
join(sFlat0,sFlat5) = sFlat6,
inference(orient,[status(thm)],[t22979]) ).
cnf(t23,axiom,
sFlat7 = complement(join(complement(sk1),complement(sk2))),
introduced(definition) ).
cnf(t62,plain,
complement(join(complement(sk1),complement(sk2))) = sFlat7,
inference(orient,[status(thm)],[t23]) ).
cnf(t22973,plain,
complement(join(sFlat0,complement(sk2))) = sFlat7,
inference(step,[status(thm)],[t62,t92]) ).
cnf(t105,plain,
complement(join(sFlat0,complement(sk2))) = sFlat7,
inference(rw,[status(thm)],[t22973]) ).
cnf(t23000,plain,
complement(join(sFlat0,sFlat5)) = sFlat7,
inference(step,[status(thm)],[t105,t107]) ).
cnf(t23001,plain,
complement(sFlat6) = sFlat7,
inference(step,[status(thm)],[t23000,t167]) ).
cnf(t222,plain,
complement(sFlat6) = sFlat7,
inference(orient,[status(thm)],[t23001]) ).
cnf(t17,axiom,
sFlat1 = complement(one),
introduced(definition) ).
cnf(t120,plain,
complement(one) = sFlat1,
inference(orient,[status(thm)],[t17]) ).
cnf(t18,axiom,
sFlat2 = join(complement(sk1),complement(one)),
introduced(definition) ).
cnf(t22980,plain,
sFlat2 = join(sFlat0,complement(one)),
inference(step,[status(thm)],[t18,t92]) ).
cnf(t22981,plain,
sFlat2 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t22980,t120]) ).
cnf(t169,plain,
join(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t22981]) ).
cnf(t19,axiom,
sFlat3 = complement(join(complement(sk1),complement(one))),
introduced(definition) ).
cnf(t77,plain,
complement(join(complement(sk1),complement(one))) = sFlat3,
inference(orient,[status(thm)],[t19]) ).
cnf(t22974,plain,
complement(join(sFlat0,complement(one))) = sFlat3,
inference(step,[status(thm)],[t77,t92]) ).
cnf(t106,plain,
complement(join(sFlat0,complement(one))) = sFlat3,
inference(rw,[status(thm)],[t22974]) ).
cnf(t23003,plain,
complement(join(sFlat0,sFlat1)) = sFlat3,
inference(step,[status(thm)],[t106,t120]) ).
cnf(t23004,plain,
complement(sFlat2) = sFlat3,
inference(step,[status(thm)],[t23003,t169]) ).
cnf(t232,plain,
complement(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t23004]) ).
cnf(t20,axiom,
sFlat4 = composition(complement(join(complement(sk1),complement(one))),sk2),
introduced(definition) ).
cnf(t22991,plain,
sFlat4 = composition(complement(join(sFlat0,complement(one))),sk2),
inference(step,[status(thm)],[t20,t92]) ).
cnf(t22992,plain,
sFlat4 = composition(complement(join(sFlat0,sFlat1)),sk2),
inference(step,[status(thm)],[t22991,t120]) ).
cnf(t22993,plain,
sFlat4 = composition(complement(sFlat2),sk2),
inference(step,[status(thm)],[t22992,t169]) ).
cnf(t187,plain,
composition(complement(sFlat2),sk2) = sFlat4,
inference(orient,[status(thm)],[t22993]) ).
cnf(t23005,plain,
composition(sFlat3,sk2) = sFlat4,
inference(step,[status(thm)],[t187,t232]) ).
cnf(t237,plain,
composition(sFlat3,sk2) = sFlat4,
inference(rw,[status(thm)],[t23005]) ).
cnf(t240,plain,
composition(sFlat3,sk2) = sFlat4,
inference(orient,[status(thm)],[t237]) ).
cnf(t24,axiom,
sFlat8 = join(composition(complement(join(complement(sk1),complement(one))),sk2),complement(join(complement(sk1),complement(sk2)))),
introduced(definition) ).
cnf(t22982,plain,
sFlat8 = join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(one))),sk2)),
inference(step,[status(thm)],[t24,t133]) ).
cnf(t22983,plain,
sFlat8 = join(complement(join(complement(sk2),complement(sk1))),composition(complement(join(complement(sk1),complement(one))),sk2)),
inference(step,[status(thm)],[t22982,t133]) ).
cnf(t22984,plain,
sFlat8 = join(complement(join(sFlat5,complement(sk1))),composition(complement(join(complement(sk1),complement(one))),sk2)),
inference(step,[status(thm)],[t22983,t107]) ).
cnf(t22985,plain,
sFlat8 = join(complement(join(sFlat5,sFlat0)),composition(complement(join(complement(sk1),complement(one))),sk2)),
inference(step,[status(thm)],[t22984,t92]) ).
cnf(t22986,plain,
sFlat8 = join(complement(join(sFlat0,sFlat5)),composition(complement(join(complement(sk1),complement(one))),sk2)),
inference(step,[status(thm)],[t22985,t133]) ).
cnf(t22987,plain,
sFlat8 = join(complement(sFlat6),composition(complement(join(complement(sk1),complement(one))),sk2)),
inference(step,[status(thm)],[t22986,t167]) ).
cnf(t22988,plain,
sFlat8 = join(complement(sFlat6),composition(complement(join(sFlat0,complement(one))),sk2)),
inference(step,[status(thm)],[t22987,t92]) ).
cnf(t22989,plain,
sFlat8 = join(complement(sFlat6),composition(complement(join(sFlat0,sFlat1)),sk2)),
inference(step,[status(thm)],[t22988,t120]) ).
cnf(t22990,plain,
sFlat8 = join(complement(sFlat6),composition(complement(sFlat2),sk2)),
inference(step,[status(thm)],[t22989,t169]) ).
cnf(t174,plain,
join(complement(sFlat6),composition(complement(sFlat2),sk2)) = sFlat8,
inference(orient,[status(thm)],[t22990]) ).
cnf(t22994,plain,
join(complement(sFlat6),sFlat4) = sFlat8,
inference(step,[status(thm)],[t174,t187]) ).
cnf(t192,plain,
join(complement(sFlat6),sFlat4) = sFlat8,
inference(rw,[status(thm)],[t22994]) ).
cnf(t22999,plain,
join(sFlat4,complement(sFlat6)) = sFlat8,
inference(step,[status(thm)],[t192,t133]) ).
cnf(t220,plain,
join(sFlat4,complement(sFlat6)) = sFlat8,
inference(orient,[status(thm)],[t22999]) ).
cnf(t23002,plain,
join(sFlat4,sFlat7) = sFlat8,
inference(step,[status(thm)],[t220,t222]) ).
cnf(t227,plain,
join(sFlat4,sFlat7) = sFlat8,
inference(rw,[status(thm)],[t23002]) ).
cnf(t230,plain,
join(sFlat4,sFlat7) = sFlat8,
inference(orient,[status(thm)],[t227]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t143,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/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t135,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(rw,[status(thm)],[t30]) ).
cnf(t23033,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t135,t133]) ).
cnf(t613,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t23033]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t193,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t2,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t195,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t193,t29]) ).
cnf(t428,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t195]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t429,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t428,t28]) ).
cnf(t23013,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t429,t29]) ).
cnf(t444,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t23013]) ).
cnf(t445,plain,
one = converse(one),
inference(cp,[status(thm)],[t444,t28]) ).
cnf(t452,plain,
converse(one) = one,
inference(orient,[status(thm)],[t445]) ).
cnf(t622,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t613,t452]) ).
cnf(t23014,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t444,t452]) ).
cnf(t463,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t23014]) ).
cnf(t464,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t463]) ).
cnf(t23034,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t622,t464]) ).
cnf(t23035,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t23034,t464]) ).
cnf(t643,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t23035]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t134,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t25]) ).
cnf(t23006,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t134,t133]) ).
cnf(t287,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t23006]) ).
cnf(t657,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t287,t643]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t138,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t23070,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t657,t138]) ).
cnf(u0,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t5,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t33,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t22975,plain,
complement(top) = zero,
inference(step,[status(thm)],[t33,t138]) ).
cnf(t142,plain,
complement(top) = zero,
inference(rw,[status(thm)],[t22975]) ).
cnf(t207,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t142]) ).
cnf(t23071,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t23070,t207]) ).
cnf(t23072,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t23071,t133]) ).
cnf(t744,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t23072]) ).
cnf(t646,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t643,t207]) ).
cnf(t23040,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t646,t207]) ).
cnf(t23041,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t23040,t207]) ).
cnf(t674,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t23041]) ).
cnf(t675,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t143,t674]) ).
cnf(t824,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t675]) ).
cnf(t830,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t824,t744]) ).
cnf(t23109,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t830,t744]) ).
cnf(t846,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t23109]) ).
cnf(t23116,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t744,t846]) ).
cnf(t867,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t23116]) ).
cnf(t1032,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t867]) ).
cnf(t1033,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t643,t1032]) ).
cnf(t23174,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1033,t1032]) ).
cnf(t23175,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t23174,t1032]) ).
cnf(t1104,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t23175]) ).
cnf(t1117,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t143,t1104]) ).
cnf(t1621,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1117]) ).
cnf(t1635,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = join(complement(join(complement(X1),X2)),X1),
inference(cp,[status(thm)],[t1621,t287]) ).
cnf(t23401,plain,
X1 = join(complement(join(complement(X1),X2)),X1),
inference(step,[status(thm)],[t1635,t287]) ).
cnf(t23402,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t23401,t133]) ).
cnf(t3932,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t23402]) ).
cnf(t3943,plain,
complement(X1) = join(complement(X1),complement(join(X1,X2))),
inference(cp,[status(thm)],[t3932,t1032]) ).
cnf(t14474,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t3943]) ).
cnf(t168,plain,
join(sFlat0,join(sFlat5,X1)) = join(sFlat6,X1),
inference(cp,[status(thm)],[t143,t167]) ).
cnf(t245,plain,
join(sFlat0,join(sFlat5,X1)) = join(sFlat6,X1),
inference(orient,[status(thm)],[t168]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t171,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t242,plain,
composition(join(sFlat3,X1),sk2) = join(sFlat4,composition(X1,sk2)),
inference(cp,[status(thm)],[t171,t240]) ).
cnf(t561,plain,
composition(join(sFlat3,X1),sk2) = join(sFlat4,composition(X1,sk2)),
inference(orient,[status(thm)],[t242]) ).
cnf(t3951,plain,
one = join(one,complement(join(sFlat1,X1))),
inference(cp,[status(thm)],[t3932,t120]) ).
cnf(t4090,plain,
join(one,complement(join(sFlat1,X1))) = one,
inference(orient,[status(thm)],[t3951]) ).
cnf(t170,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t143,t169]) ).
cnf(t253,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t170]) ).
cnf(t256,plain,
join(sFlat2,X1) = join(sFlat0,join(X1,sFlat1)),
inference(cp,[status(thm)],[t253,t133]) ).
cnf(t340,plain,
join(sFlat0,join(X1,sFlat1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t256]) ).
cnf(t647,plain,
complement(one) = join(sFlat1,complement(one)),
inference(cp,[status(thm)],[t643,t120]) ).
cnf(t23042,plain,
sFlat1 = join(sFlat1,complement(one)),
inference(step,[status(thm)],[t647,t120]) ).
cnf(t23043,plain,
sFlat1 = join(sFlat1,sFlat1),
inference(step,[status(thm)],[t23042,t120]) ).
cnf(t676,plain,
join(sFlat1,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t23043]) ).
cnf(t677,plain,
join(sFlat2,sFlat1) = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t340,t676]) ).
cnf(t23059,plain,
join(sFlat1,sFlat2) = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t677,t133]) ).
cnf(t23060,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t23059,t169]) ).
cnf(t706,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t23060]) ).
cnf(t4095,plain,
one = join(one,complement(sFlat2)),
inference(cp,[status(thm)],[t4090,t706]) ).
cnf(t23403,plain,
one = join(one,sFlat3),
inference(step,[status(thm)],[t4095,t232]) ).
cnf(t23404,plain,
one = join(sFlat3,one),
inference(step,[status(thm)],[t23403,t133]) ).
cnf(t4107,plain,
join(sFlat3,one) = one,
inference(orient,[status(thm)],[t23404]) ).
cnf(t4108,plain,
join(sFlat4,composition(one,sk2)) = composition(one,sk2),
inference(cp,[status(thm)],[t561,t4107]) ).
cnf(t23405,plain,
join(sFlat4,sk2) = composition(one,sk2),
inference(step,[status(thm)],[t4108,t464]) ).
cnf(t23406,plain,
join(sFlat4,sk2) = sk2,
inference(step,[status(thm)],[t23405,t464]) ).
cnf(t4115,plain,
join(sFlat4,sk2) = sk2,
inference(orient,[status(thm)],[t23406]) ).
cnf(t14498,plain,
complement(sFlat4) = join(complement(sFlat4),complement(sk2)),
inference(cp,[status(thm)],[t14474,t4115]) ).
cnf(t23836,plain,
complement(sFlat4) = join(complement(sFlat4),sFlat5),
inference(step,[status(thm)],[t14498,t107]) ).
cnf(t23837,plain,
complement(sFlat4) = join(sFlat5,complement(sFlat4)),
inference(step,[status(thm)],[t23836,t133]) ).
cnf(t14840,plain,
join(sFlat5,complement(sFlat4)) = complement(sFlat4),
inference(orient,[status(thm)],[t23837]) ).
cnf(t14842,plain,
join(sFlat6,complement(sFlat4)) = join(sFlat0,complement(sFlat4)),
inference(cp,[status(thm)],[t245,t14840]) ).
cnf(t14860,plain,
join(sFlat6,complement(sFlat4)) = join(sFlat0,complement(sFlat4)),
inference(orient,[status(thm)],[t14842]) ).
cnf(t14865,plain,
complement(sFlat6) = join(complement(sFlat6),complement(join(sFlat0,complement(sFlat4)))),
inference(cp,[status(thm)],[t14474,t14860]) ).
cnf(t23855,plain,
sFlat7 = join(complement(sFlat6),complement(join(sFlat0,complement(sFlat4)))),
inference(step,[status(thm)],[t14865,t222]) ).
cnf(t23856,plain,
sFlat7 = join(sFlat7,complement(join(sFlat0,complement(sFlat4)))),
inference(step,[status(thm)],[t23855,t222]) ).
cnf(t15298,plain,
join(sFlat7,complement(join(sFlat0,complement(sFlat4)))) = sFlat7,
inference(orient,[status(thm)],[t23856]) ).
cnf(t147,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t143,t133]) ).
cnf(t23271,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t147,t143]) ).
cnf(t2141,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t23271]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t176,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t178,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t176,t29]) ).
cnf(t394,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t178]) ).
cnf(t144,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t143,t138]) ).
cnf(t888,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t144]) ).
cnf(t1119,plain,
top = join(X1,join(X1,complement(X1))),
inference(cp,[status(thm)],[t888,t1104]) ).
cnf(t23177,plain,
top = join(X1,top),
inference(step,[status(thm)],[t1119,t138]) ).
cnf(t1124,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t23177]) ).
cnf(t1125,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t1124,t133]) ).
cnf(t1133,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t1125]) ).
cnf(t395,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t394,t138]) ).
cnf(t516,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t395]) ).
cnf(t1162,plain,
top = converse(top),
inference(cp,[status(thm)],[t1133,t516]) ).
cnf(t1171,plain,
converse(top) = top,
inference(orient,[status(thm)],[t1162]) ).
cnf(t1176,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t193,t1171]) ).
cnf(t1216,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t1176]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t202,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t1219,plain,
composition(top,converse(sk1)) = converse(sk1),
inference(cp,[status(thm)],[t1216,t202]) ).
cnf(t1233,plain,
composition(top,converse(sk1)) = converse(sk1),
inference(orient,[status(thm)],[t1219]) ).
cnf(t1235,plain,
composition(join(top,X1),converse(sk1)) = join(converse(sk1),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t171,t1233]) ).
cnf(t23829,plain,
composition(top,converse(sk1)) = join(converse(sk1),composition(X1,converse(sk1))),
inference(step,[status(thm)],[t1235,t1133]) ).
cnf(t23830,plain,
converse(sk1) = join(converse(sk1),composition(X1,converse(sk1))),
inference(step,[status(thm)],[t23829,t1233]) ).
cnf(t14428,plain,
join(converse(sk1),composition(X1,converse(sk1))) = converse(sk1),
inference(orient,[status(thm)],[t23830]) ).
cnf(t14433,plain,
join(sk1,converse(composition(X1,converse(sk1)))) = converse(converse(sk1)),
inference(cp,[status(thm)],[t394,t14428]) ).
cnf(t194,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t193,t29]) ).
cnf(t415,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t194]) ).
cnf(t23831,plain,
join(sk1,composition(sk1,converse(X1))) = converse(converse(sk1)),
inference(step,[status(thm)],[t14433,t415]) ).
cnf(t23832,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(step,[status(thm)],[t23831,t29]) ).
cnf(t14438,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(orient,[status(thm)],[t23832]) ).
cnf(t14447,plain,
sk1 = join(sk1,composition(sk1,X1)),
inference(cp,[status(thm)],[t14438,t29]) ).
cnf(t14466,plain,
join(sk1,composition(sk1,X1)) = sk1,
inference(orient,[status(thm)],[t14447]) ).
cnf(t14471,plain,
join(sk1,join(X1,composition(sk1,X2))) = join(X1,sk1),
inference(cp,[status(thm)],[t2141,t14466]) ).
cnf(t22884,plain,
join(sk1,join(X1,composition(sk1,X2))) = join(X1,sk1),
inference(orient,[status(thm)],[t14471]) ).
cnf(t3953,plain,
sk1 = join(sk1,complement(join(sFlat0,X1))),
inference(cp,[status(thm)],[t3932,t92]) ).
cnf(t4312,plain,
join(sk1,complement(join(sFlat0,X1))) = sk1,
inference(orient,[status(thm)],[t3953]) ).
cnf(t745,plain,
sFlat2 = join(zero,complement(sFlat3)),
inference(cp,[status(thm)],[t744,t232]) ).
cnf(t751,plain,
join(zero,complement(sFlat3)) = sFlat2,
inference(orient,[status(thm)],[t745]) ).
cnf(t23114,plain,
complement(sFlat3) = sFlat2,
inference(step,[status(thm)],[t751,t846]) ).
cnf(t865,plain,
complement(sFlat3) = sFlat2,
inference(rw,[status(thm)],[t23114]) ).
cnf(t1014,plain,
complement(sFlat3) = sFlat2,
inference(orient,[status(thm)],[t865]) ).
cnf(t1015,plain,
complement(sFlat3) = join(sFlat2,complement(sFlat3)),
inference(cp,[status(thm)],[t643,t1014]) ).
cnf(t23169,plain,
sFlat2 = join(sFlat2,complement(sFlat3)),
inference(step,[status(thm)],[t1015,t1014]) ).
cnf(t23170,plain,
sFlat2 = join(sFlat2,sFlat2),
inference(step,[status(thm)],[t23169,t1014]) ).
cnf(t707,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t253,t706]) ).
cnf(t740,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(orient,[status(thm)],[t707]) ).
cnf(t23171,plain,
sFlat2 = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t23170,t740]) ).
cnf(t1100,plain,
join(sFlat0,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t23171]) ).
cnf(t4317,plain,
sk1 = join(sk1,complement(sFlat2)),
inference(cp,[status(thm)],[t4312,t1100]) ).
cnf(t23415,plain,
sk1 = join(sk1,sFlat3),
inference(step,[status(thm)],[t4317,t232]) ).
cnf(t23416,plain,
sk1 = join(sFlat3,sk1),
inference(step,[status(thm)],[t23415,t133]) ).
cnf(t4336,plain,
join(sFlat3,sk1) = sk1,
inference(orient,[status(thm)],[t23416]) ).
cnf(t4337,plain,
join(sFlat4,composition(sk1,sk2)) = composition(sk1,sk2),
inference(cp,[status(thm)],[t561,t4336]) ).
cnf(t4375,plain,
join(sFlat4,composition(sk1,sk2)) = composition(sk1,sk2),
inference(orient,[status(thm)],[t4337]) ).
cnf(t22902,plain,
join(sFlat4,sk1) = join(sk1,composition(sk1,sk2)),
inference(cp,[status(thm)],[t22884,t4375]) ).
cnf(t24022,plain,
join(sFlat4,sk1) = sk1,
inference(step,[status(thm)],[t22902,t14466]) ).
cnf(t22922,plain,
join(sFlat4,sk1) = sk1,
inference(orient,[status(thm)],[t24022]) ).
cnf(t22926,plain,
complement(sFlat4) = join(complement(sFlat4),complement(sk1)),
inference(cp,[status(thm)],[t14474,t22922]) ).
cnf(t24027,plain,
complement(sFlat4) = join(complement(sFlat4),sFlat0),
inference(step,[status(thm)],[t22926,t92]) ).
cnf(t24028,plain,
complement(sFlat4) = join(sFlat0,complement(sFlat4)),
inference(step,[status(thm)],[t24027,t133]) ).
cnf(t22933,plain,
join(sFlat0,complement(sFlat4)) = complement(sFlat4),
inference(orient,[status(thm)],[t24028]) ).
cnf(t24033,plain,
join(sFlat7,complement(complement(sFlat4))) = sFlat7,
inference(step,[status(thm)],[t15298,t22933]) ).
cnf(t24034,plain,
join(sFlat7,sFlat4) = sFlat7,
inference(step,[status(thm)],[t24033,t1032]) ).
cnf(t22945,plain,
join(sFlat7,sFlat4) = sFlat7,
inference(rw,[status(thm)],[t24034]) ).
cnf(t24035,plain,
join(sFlat4,sFlat7) = sFlat7,
inference(step,[status(thm)],[t22945,t133]) ).
cnf(t24036,plain,
sFlat8 = sFlat7,
inference(step,[status(thm)],[t24035,t230]) ).
cnf(t22946,plain,
sFlat8 = sFlat7,
inference(orient,[status(thm)],[t24036]) ).
cnf(t24037,plain,
join(sFlat4,sFlat7) = sFlat7,
inference(step,[status(thm)],[t230,t22946]) ).
cnf(t22947,plain,
join(sFlat4,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t24037]) ).
cnf(u4,negated_conjecture,
join(composition(meet(sk1,one),sk2),meet(sk1,sk2)) != meet(sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
join(composition(complement(join(complement(sk1),complement(one))),sk2),complement(join(complement(sk1),complement(sk2)))) != complement(join(complement(sk1),complement(sk2))),
inference(definition_unfolding,[status(thm)],[u4,d0]) ).
cnf(g0_0,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(one))),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[goal_0,t133]) ).
cnf(g0_1,plain,
join(complement(join(complement(sk2),complement(sk1))),composition(complement(join(complement(sk1),complement(one))),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_0,t133]) ).
cnf(g0_2,plain,
join(complement(join(sFlat5,complement(sk1))),composition(complement(join(complement(sk1),complement(one))),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_1,t107]) ).
cnf(g0_3,plain,
join(complement(join(sFlat5,sFlat0)),composition(complement(join(complement(sk1),complement(one))),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_2,t92]) ).
cnf(g0_4,plain,
join(complement(join(sFlat0,sFlat5)),composition(complement(join(complement(sk1),complement(one))),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_3,t133]) ).
cnf(g0_5,plain,
join(complement(sFlat6),composition(complement(join(complement(sk1),complement(one))),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_4,t167]) ).
cnf(g0_6,plain,
join(sFlat7,composition(complement(join(complement(sk1),complement(one))),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_5,t222]) ).
cnf(g0_7,plain,
join(sFlat7,composition(complement(join(sFlat0,complement(one))),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_6,t92]) ).
cnf(g0_8,plain,
join(sFlat7,composition(complement(join(sFlat0,sFlat1)),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_7,t120]) ).
cnf(g0_9,plain,
join(sFlat7,composition(complement(sFlat2),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_8,t169]) ).
cnf(g0_10,plain,
join(sFlat7,composition(sFlat3,sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_9,t232]) ).
cnf(g0_11,plain,
join(sFlat7,sFlat4) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_10,t240]) ).
cnf(g0_12,plain,
join(sFlat4,sFlat7) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_11,t133]) ).
cnf(g0_13,plain,
sFlat7 != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_12,t22947]) ).
cnf(g0_14,plain,
sFlat7 != complement(join(complement(sk2),complement(sk1))),
inference(rw,[status(thm)],[g0_13,t133]) ).
cnf(g0_15,plain,
sFlat7 != complement(join(sFlat5,complement(sk1))),
inference(rw,[status(thm)],[g0_14,t107]) ).
cnf(g0_16,plain,
sFlat7 != complement(join(sFlat5,sFlat0)),
inference(rw,[status(thm)],[g0_15,t92]) ).
cnf(g0_17,plain,
sFlat7 != complement(join(sFlat0,sFlat5)),
inference(rw,[status(thm)],[g0_16,t133]) ).
cnf(g0_18,plain,
sFlat7 != complement(sFlat6),
inference(rw,[status(thm)],[g0_17,t167]) ).
cnf(g0_19,plain,
sFlat7 != sFlat7,
inference(rw,[status(thm)],[g0_18,t222]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_19]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL021-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n017.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:13:02 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 38.28/5.25 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 38.28/5.25 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------