%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL011-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : 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:42 PM UTC 2026
% Result : Unsatisfiable 61.10s 9.54s
% Output : CNFRefutation 61.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 25
% Syntax : Number of clauses : 255 ( 255 unt; 0 nHn; 147 RR)
% Number of literals : 255 ( 254 equ; 8 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 : 22 ( 22 usr; 17 con; 0-2 aty)
% Number of variables : 152 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t19,axiom,
sF6 = composition(sk2,sk1),
introduced(definition) ).
cnf(t31,plain,
composition(sk2,sk1) = sF6,
inference(orient,[status(thm)],[t19]) ).
cnf(t20,axiom,
sF7 = complement(composition(sk2,sk1)),
introduced(definition) ).
cnf(t26429,plain,
sF7 = complement(sF6),
inference(step,[status(thm)],[t20,t31]) ).
cnf(t46,plain,
complement(sF6) = sF7,
inference(orient,[status(thm)],[t26429]) ).
cnf(t21,axiom,
sF8 = complement(sk3),
introduced(definition) ).
cnf(t26,plain,
complement(sk3) = sF8,
inference(orient,[status(thm)],[t21]) ).
cnf(t22,axiom,
sF9 = join(complement(composition(sk2,sk1)),complement(sk3)),
introduced(definition) ).
cnf(t3,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t37,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t26489,plain,
sF9 = join(complement(sk3),complement(composition(sk2,sk1))),
inference(step,[status(thm)],[t22,t37]) ).
cnf(t26490,plain,
sF9 = join(sF8,complement(composition(sk2,sk1))),
inference(step,[status(thm)],[t26489,t26]) ).
cnf(t26491,plain,
sF9 = join(sF8,complement(sF6)),
inference(step,[status(thm)],[t26490,t31]) ).
cnf(t26492,plain,
sF9 = join(sF8,sF7),
inference(step,[status(thm)],[t26491,t46]) ).
cnf(t26493,plain,
sF9 = join(sF7,sF8),
inference(step,[status(thm)],[t26492,t37]) ).
cnf(t435,plain,
join(sF7,sF8) = sF9,
inference(orient,[status(thm)],[t26493]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t139,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t437,plain,
join(sF7,join(sF8,X1)) = join(sF9,X1),
inference(cp,[status(thm)],[t139,t435]) ).
cnf(t1433,plain,
join(sF7,join(sF8,X1)) = join(sF9,X1),
inference(orient,[status(thm)],[t437]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26447,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t37]) ).
cnf(t232,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t26447]) ).
cnf(t15,axiom,
sF2 = composition(converse(sk2),sk3),
introduced(definition) ).
cnf(t14,axiom,
sF1 = converse(sk2),
introduced(definition) ).
cnf(t25,plain,
converse(sk2) = sF1,
inference(orient,[status(thm)],[t14]) ).
cnf(t26428,plain,
sF2 = composition(sF1,sk3),
inference(step,[status(thm)],[t15,t25]) ).
cnf(t45,plain,
composition(sF1,sk3) = sF2,
inference(orient,[status(thm)],[t26428]) ).
cnf(t241,plain,
complement(sk3) = join(complement(sk3),composition(converse(sF1),complement(sF2))),
inference(cp,[status(thm)],[t232,t45]) ).
cnf(t26475,plain,
sF8 = join(complement(sk3),composition(converse(sF1),complement(sF2))),
inference(step,[status(thm)],[t241,t26]) ).
cnf(t26476,plain,
sF8 = join(sF8,composition(converse(sF1),complement(sF2))),
inference(step,[status(thm)],[t26475,t26]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t29,plain,
sk2 = converse(sF1),
inference(cp,[status(thm)],[t28,t25]) ).
cnf(t30,plain,
converse(sF1) = sk2,
inference(orient,[status(thm)],[t29]) ).
cnf(t26477,plain,
sF8 = join(sF8,composition(sk2,complement(sF2))),
inference(step,[status(thm)],[t26476,t30]) ).
cnf(t16,axiom,
sF3 = complement(composition(converse(sk2),sk3)),
introduced(definition) ).
cnf(t26439,plain,
sF3 = complement(composition(sF1,sk3)),
inference(step,[status(thm)],[t16,t25]) ).
cnf(t26440,plain,
sF3 = complement(sF2),
inference(step,[status(thm)],[t26439,t45]) ).
cnf(t154,plain,
complement(sF2) = sF3,
inference(orient,[status(thm)],[t26440]) ).
cnf(t26478,plain,
sF8 = join(sF8,composition(sk2,sF3)),
inference(step,[status(thm)],[t26477,t154]) ).
cnf(t414,plain,
join(sF8,composition(sk2,sF3)) = sF8,
inference(orient,[status(thm)],[t26478]) ).
cnf(t1438,plain,
join(sF9,composition(sk2,sF3)) = join(sF7,sF8),
inference(cp,[status(thm)],[t1433,t414]) ).
cnf(t26763,plain,
join(sF9,composition(sk2,sF3)) = sF9,
inference(step,[status(thm)],[t1438,t435]) ).
cnf(t2245,plain,
join(sF9,composition(sk2,sF3)) = sF9,
inference(orient,[status(thm)],[t26763]) ).
cnf(t2247,plain,
join(sF9,join(composition(sk2,sF3),X1)) = join(sF9,X1),
inference(cp,[status(thm)],[t139,t2245]) ).
cnf(t23579,plain,
join(sF9,join(composition(sk2,sF3),X1)) = join(sF9,X1),
inference(orient,[status(thm)],[t2247]) ).
cnf(t5,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t50,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t5]) ).
cnf(t54,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t50,t28]) ).
cnf(t176,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t54]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t177,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t176,t27]) ).
cnf(t26442,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t177,t28]) ).
cnf(t184,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t26442]) ).
cnf(t187,plain,
one = converse(one),
inference(cp,[status(thm)],[t184,t27]) ).
cnf(t205,plain,
converse(one) = one,
inference(orient,[status(thm)],[t187]) ).
cnf(t260,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t232,t205]) ).
cnf(t26445,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t184,t205]) ).
cnf(t206,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t26445]) ).
cnf(t210,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t206]) ).
cnf(t26479,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t260,t210]) ).
cnf(t26480,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t26479,t210]) ).
cnf(t417,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t26480]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26450,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t12,t37]) ).
cnf(t314,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t26450]) ).
cnf(t424,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t314,t417]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t26559,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t424,t32]) ).
cnf(t26560,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t26559,t37]) ).
cnf(u0,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t26430,plain,
complement(top) = zero,
inference(step,[status(thm)],[t4,t32]) ).
cnf(t57,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t26430]) ).
cnf(t18,axiom,
sF5 = complement(join(complement(sk1),complement(composition(converse(sk2),sk3)))),
introduced(definition) ).
cnf(t13,axiom,
sF0 = complement(sk1),
introduced(definition) ).
cnf(t24,plain,
complement(sk1) = sF0,
inference(orient,[status(thm)],[t13]) ).
cnf(t26462,plain,
sF5 = complement(join(sF0,complement(composition(converse(sk2),sk3)))),
inference(step,[status(thm)],[t18,t24]) ).
cnf(t26463,plain,
sF5 = complement(join(sF0,complement(composition(sF1,sk3)))),
inference(step,[status(thm)],[t26462,t25]) ).
cnf(t26464,plain,
sF5 = complement(join(sF0,complement(sF2))),
inference(step,[status(thm)],[t26463,t45]) ).
cnf(t26465,plain,
sF5 = complement(join(sF0,sF3)),
inference(step,[status(thm)],[t26464,t154]) ).
cnf(t17,axiom,
sF4 = join(complement(sk1),complement(composition(converse(sk2),sk3))),
introduced(definition) ).
cnf(t26451,plain,
sF4 = join(sF0,complement(composition(converse(sk2),sk3))),
inference(step,[status(thm)],[t17,t24]) ).
cnf(t26452,plain,
sF4 = join(sF0,complement(composition(sF1,sk3))),
inference(step,[status(thm)],[t26451,t25]) ).
cnf(t26453,plain,
sF4 = join(sF0,complement(sF2)),
inference(step,[status(thm)],[t26452,t45]) ).
cnf(t26454,plain,
sF4 = join(sF0,sF3),
inference(step,[status(thm)],[t26453,t154]) ).
cnf(t359,plain,
join(sF0,sF3) = sF4,
inference(orient,[status(thm)],[t26454]) ).
cnf(t26466,plain,
sF5 = complement(sF4),
inference(step,[status(thm)],[t26465,t359]) ).
cnf(u1,axiom,
meet(sk1,composition(converse(sk2),sk3)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t7,plain,
complement(join(complement(sk1),complement(composition(converse(sk2),sk3)))) = zero,
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t26436,plain,
complement(join(sF0,complement(composition(converse(sk2),sk3)))) = zero,
inference(step,[status(thm)],[t7,t24]) ).
cnf(t26437,plain,
complement(join(sF0,complement(composition(sF1,sk3)))) = zero,
inference(step,[status(thm)],[t26436,t25]) ).
cnf(t26438,plain,
complement(join(sF0,complement(sF2))) = zero,
inference(step,[status(thm)],[t26437,t45]) ).
cnf(t151,plain,
complement(join(sF0,complement(sF2))) = zero,
inference(orient,[status(thm)],[t26438]) ).
cnf(t26441,plain,
complement(join(sF0,sF3)) = zero,
inference(step,[status(thm)],[t151,t154]) ).
cnf(t155,plain,
complement(join(sF0,sF3)) = zero,
inference(rw,[status(thm)],[t26441]) ).
cnf(t160,plain,
complement(join(sF0,sF3)) = zero,
inference(orient,[status(thm)],[t155]) ).
cnf(t26455,plain,
complement(sF4) = zero,
inference(step,[status(thm)],[t160,t359]) ).
cnf(t360,plain,
complement(sF4) = zero,
inference(rw,[status(thm)],[t26455]) ).
cnf(t363,plain,
complement(sF4) = zero,
inference(orient,[status(thm)],[t360]) ).
cnf(t26467,plain,
sF5 = zero,
inference(step,[status(thm)],[t26466,t363]) ).
cnf(t401,plain,
zero = sF5,
inference(orient,[status(thm)],[t26467]) ).
cnf(t26468,plain,
complement(top) = sF5,
inference(step,[status(thm)],[t57,t401]) ).
cnf(t402,plain,
complement(top) = sF5,
inference(orient,[status(thm)],[t26468]) ).
cnf(t26561,plain,
X1 = join(sF5,complement(complement(X1))),
inference(step,[status(thm)],[t26560,t402]) ).
cnf(t663,plain,
join(sF5,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t26561]) ).
cnf(t421,plain,
complement(top) = join(sF5,complement(top)),
inference(cp,[status(thm)],[t417,t402]) ).
cnf(t26487,plain,
sF5 = join(sF5,complement(top)),
inference(step,[status(thm)],[t421,t402]) ).
cnf(t26488,plain,
sF5 = join(sF5,sF5),
inference(step,[status(thm)],[t26487,t402]) ).
cnf(t433,plain,
join(sF5,sF5) = sF5,
inference(orient,[status(thm)],[t26488]) ).
cnf(t434,plain,
join(sF5,join(sF5,X1)) = join(sF5,X1),
inference(cp,[status(thm)],[t139,t433]) ).
cnf(t1043,plain,
join(sF5,join(sF5,X1)) = join(sF5,X1),
inference(orient,[status(thm)],[t434]) ).
cnf(t1046,plain,
join(sF5,complement(complement(X1))) = join(sF5,X1),
inference(cp,[status(thm)],[t1043,t663]) ).
cnf(t26643,plain,
X1 = join(sF5,X1),
inference(step,[status(thm)],[t1046,t663]) ).
cnf(t1048,plain,
join(sF5,X1) = X1,
inference(orient,[status(thm)],[t26643]) ).
cnf(t26646,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t663,t1048]) ).
cnf(t1051,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t26646]) ).
cnf(t1136,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1051]) ).
cnf(t1140,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t417,t1136]) ).
cnf(t26664,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1140,t1136]) ).
cnf(t26665,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t26664,t1136]) ).
cnf(t1219,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t26665]) ).
cnf(t1233,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t139,t1219]) ).
cnf(t1985,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1233]) ).
cnf(t1991,plain,
join(X1,X2) = join(join(X1,X2),X1),
inference(cp,[status(thm)],[t1985,t37]) ).
cnf(t26789,plain,
join(X1,X2) = join(X1,join(X2,X1)),
inference(step,[status(thm)],[t1991,t139]) ).
cnf(t2554,plain,
join(X1,join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t26789]) ).
cnf(t2589,plain,
join(X1,join(join(X2,X1),X3)) = join(join(X1,X2),X3),
inference(cp,[status(thm)],[t139,t2554]) ).
cnf(t27398,plain,
join(X1,join(X2,join(X1,X3))) = join(join(X1,X2),X3),
inference(step,[status(thm)],[t2589,t139]) ).
cnf(t27399,plain,
join(X1,join(X2,join(X1,X3))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t27398,t139]) ).
cnf(t25441,plain,
join(X1,join(X2,join(X1,X3))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t27399]) ).
cnf(t324,plain,
sF6 = join(complement(join(sF7,X1)),complement(join(complement(sF6),complement(X1)))),
inference(cp,[status(thm)],[t314,t46]) ).
cnf(t27126,plain,
sF6 = join(complement(join(sF7,X1)),complement(join(sF7,complement(X1)))),
inference(step,[status(thm)],[t324,t46]) ).
cnf(t14291,plain,
join(complement(join(sF7,X1)),complement(join(sF7,complement(X1)))) = sF6,
inference(orient,[status(thm)],[t27126]) ).
cnf(t14293,plain,
sF6 = join(complement(join(sF7,sk3)),complement(join(sF7,sF8))),
inference(cp,[status(thm)],[t14291,t26]) ).
cnf(t27154,plain,
sF6 = join(complement(join(sF7,sF8)),complement(join(sF7,sk3))),
inference(step,[status(thm)],[t14293,t37]) ).
cnf(t27155,plain,
sF6 = join(complement(sF9),complement(join(sF7,sk3))),
inference(step,[status(thm)],[t27154,t435]) ).
cnf(t23,axiom,
sF10 = complement(join(complement(composition(sk2,sk1)),complement(sk3))),
introduced(definition) ).
cnf(t26506,plain,
sF10 = complement(join(complement(sk3),complement(composition(sk2,sk1)))),
inference(step,[status(thm)],[t23,t37]) ).
cnf(t26507,plain,
sF10 = complement(join(sF8,complement(composition(sk2,sk1)))),
inference(step,[status(thm)],[t26506,t26]) ).
cnf(t26508,plain,
sF10 = complement(join(sF8,complement(sF6))),
inference(step,[status(thm)],[t26507,t31]) ).
cnf(t26509,plain,
sF10 = complement(join(sF8,sF7)),
inference(step,[status(thm)],[t26508,t46]) ).
cnf(t26510,plain,
sF10 = complement(join(sF7,sF8)),
inference(step,[status(thm)],[t26509,t37]) ).
cnf(t26511,plain,
sF10 = complement(sF9),
inference(step,[status(thm)],[t26510,t435]) ).
cnf(t462,plain,
complement(sF9) = sF10,
inference(orient,[status(thm)],[t26511]) ).
cnf(t27156,plain,
sF6 = join(sF10,complement(join(sF7,sk3))),
inference(step,[status(thm)],[t27155,t462]) ).
cnf(t15129,plain,
join(sF10,complement(join(sF7,sk3))) = sF6,
inference(orient,[status(thm)],[t27156]) ).
cnf(t15135,plain,
join(sF10,complement(join(sF7,sk3))) = join(sF10,sF6),
inference(cp,[status(thm)],[t1985,t15129]) ).
cnf(t27157,plain,
sF6 = join(sF10,sF6),
inference(step,[status(thm)],[t15135,t15129]) ).
cnf(t27158,plain,
sF6 = join(sF6,sF10),
inference(step,[status(thm)],[t27157,t37]) ).
cnf(t15146,plain,
join(sF6,sF10) = sF6,
inference(orient,[status(thm)],[t27158]) ).
cnf(t25561,plain,
join(sF6,join(X1,sF10)) = join(sF6,join(X1,sF6)),
inference(cp,[status(thm)],[t25441,t15146]) ).
cnf(t143,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t139,t37]) ).
cnf(t26793,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t143,t139]) ).
cnf(t2723,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t26793]) ).
cnf(t15152,plain,
join(sF6,join(X1,sF10)) = join(X1,sF6),
inference(cp,[status(thm)],[t2723,t15146]) ).
cnf(t15212,plain,
join(sF6,join(X1,sF10)) = join(X1,sF6),
inference(orient,[status(thm)],[t15152]) ).
cnf(t27402,plain,
join(X1,sF6) = join(sF6,join(X1,sF6)),
inference(step,[status(thm)],[t25561,t15212]) ).
cnf(t27403,plain,
join(X1,sF6) = join(sF6,X1),
inference(step,[status(thm)],[t27402,t2554]) ).
cnf(t26160,plain,
join(X1,sF6) = join(sF6,X1),
inference(orient,[status(thm)],[t27403]) ).
cnf(t26175,plain,
join(sF9,sF6) = join(sF9,join(sF6,composition(sk2,sF3))),
inference(cp,[status(thm)],[t23579,t26160]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t188,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t52,plain,
converse(composition(sk2,X1)) = composition(converse(X1),sF1),
inference(cp,[status(thm)],[t50,t25]) ).
cnf(t65,plain,
converse(composition(sk2,X1)) = composition(converse(X1),sF1),
inference(orient,[status(thm)],[t52]) ).
cnf(t67,plain,
composition(converse(sk1),sF1) = converse(sF6),
inference(cp,[status(thm)],[t65,t31]) ).
cnf(t80,plain,
composition(converse(sk1),sF1) = converse(sF6),
inference(orient,[status(thm)],[t67]) ).
cnf(t196,plain,
composition(join(converse(sk1),X1),sF1) = join(converse(sF6),composition(X1,sF1)),
inference(cp,[status(thm)],[t188,t80]) ).
cnf(t3082,plain,
composition(join(converse(sk1),X1),sF1) = join(converse(sF6),composition(X1,sF1)),
inference(orient,[status(thm)],[t196]) ).
cnf(t6,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t83,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t6]) ).
cnf(t3085,plain,
join(converse(sF6),composition(converse(X1),sF1)) = composition(converse(join(sk1,X1)),sF1),
inference(cp,[status(thm)],[t3082,t83]) ).
cnf(t94,plain,
converse(join(X1,composition(sk2,X2))) = join(converse(X1),composition(converse(X2),sF1)),
inference(cp,[status(thm)],[t83,t65]) ).
cnf(t1071,plain,
join(converse(X1),composition(converse(X2),sF1)) = converse(join(X1,composition(sk2,X2))),
inference(orient,[status(thm)],[t94]) ).
cnf(t26956,plain,
converse(join(sF6,composition(sk2,X1))) = composition(converse(join(sk1,X1)),sF1),
inference(step,[status(thm)],[t3085,t1071]) ).
cnf(t8074,plain,
converse(join(sF6,composition(sk2,X1))) = composition(converse(join(sk1,X1)),sF1),
inference(orient,[status(thm)],[t26956]) ).
cnf(t8077,plain,
join(sF6,composition(sk2,X1)) = converse(composition(converse(join(sk1,X1)),sF1)),
inference(cp,[status(thm)],[t28,t8074]) ).
cnf(t55,plain,
converse(composition(X1,sF1)) = composition(sk2,converse(X1)),
inference(cp,[status(thm)],[t50,t30]) ).
cnf(t71,plain,
converse(composition(X1,sF1)) = composition(sk2,converse(X1)),
inference(orient,[status(thm)],[t55]) ).
cnf(t26957,plain,
join(sF6,composition(sk2,X1)) = composition(sk2,converse(converse(join(sk1,X1)))),
inference(step,[status(thm)],[t8077,t71]) ).
cnf(t26958,plain,
join(sF6,composition(sk2,X1)) = composition(sk2,join(sk1,X1)),
inference(step,[status(thm)],[t26957,t28]) ).
cnf(t8142,plain,
composition(sk2,join(sk1,X1)) = join(sF6,composition(sk2,X1)),
inference(orient,[status(thm)],[t26958]) ).
cnf(t8145,plain,
join(sF6,composition(sk2,X1)) = composition(sk2,join(X1,sk1)),
inference(cp,[status(thm)],[t8142,t37]) ).
cnf(t8204,plain,
composition(sk2,join(X1,sk1)) = join(sF6,composition(sk2,X1)),
inference(orient,[status(thm)],[t8145]) ).
cnf(t316,plain,
X1 = join(complement(join(complement(X1),sk1)),complement(join(complement(X1),sF0))),
inference(cp,[status(thm)],[t314,t24]) ).
cnf(t27102,plain,
X1 = join(complement(join(complement(X1),sF0)),complement(join(complement(X1),sk1))),
inference(step,[status(thm)],[t316,t37]) ).
cnf(t27103,plain,
X1 = join(complement(join(sF0,complement(X1))),complement(join(complement(X1),sk1))),
inference(step,[status(thm)],[t27102,t37]) ).
cnf(t27104,plain,
X1 = join(complement(join(sF0,complement(X1))),complement(join(sk1,complement(X1)))),
inference(step,[status(thm)],[t27103,t37]) ).
cnf(t13800,plain,
join(complement(join(sF0,complement(X1))),complement(join(sk1,complement(X1)))) = X1,
inference(orient,[status(thm)],[t27104]) ).
cnf(t13806,plain,
sF2 = join(complement(join(sF0,sF3)),complement(join(sk1,complement(sF2)))),
inference(cp,[status(thm)],[t13800,t154]) ).
cnf(t27105,plain,
sF2 = join(complement(sF4),complement(join(sk1,complement(sF2)))),
inference(step,[status(thm)],[t13806,t359]) ).
cnf(t26472,plain,
complement(sF4) = sF5,
inference(step,[status(thm)],[t363,t401]) ).
cnf(t406,plain,
complement(sF4) = sF5,
inference(orient,[status(thm)],[t26472]) ).
cnf(t27106,plain,
sF2 = join(sF5,complement(join(sk1,complement(sF2)))),
inference(step,[status(thm)],[t27105,t406]) ).
cnf(t27107,plain,
sF2 = complement(join(sk1,complement(sF2))),
inference(step,[status(thm)],[t27106,t1048]) ).
cnf(t27108,plain,
sF2 = complement(join(sk1,sF3)),
inference(step,[status(thm)],[t27107,t154]) ).
cnf(t27109,plain,
sF2 = complement(join(sF3,sk1)),
inference(step,[status(thm)],[t27108,t37]) ).
cnf(t13829,plain,
complement(join(sF3,sk1)) = sF2,
inference(orient,[status(thm)],[t27109]) ).
cnf(t13835,plain,
join(sF3,sk1) = complement(sF2),
inference(cp,[status(thm)],[t1136,t13829]) ).
cnf(t27110,plain,
join(sF3,sk1) = sF3,
inference(step,[status(thm)],[t13835,t154]) ).
cnf(t13862,plain,
join(sF3,sk1) = sF3,
inference(orient,[status(thm)],[t27110]) ).
cnf(t13874,plain,
join(sF6,composition(sk2,sF3)) = composition(sk2,sF3),
inference(cp,[status(thm)],[t8204,t13862]) ).
cnf(t14054,plain,
join(sF6,composition(sk2,sF3)) = composition(sk2,sF3),
inference(orient,[status(thm)],[t13874]) ).
cnf(t27409,plain,
join(sF9,sF6) = join(sF9,composition(sk2,sF3)),
inference(step,[status(thm)],[t26175,t14054]) ).
cnf(t27410,plain,
join(sF9,sF6) = sF9,
inference(step,[status(thm)],[t27409,t2245]) ).
cnf(t27411,plain,
join(sF6,sF9) = sF9,
inference(step,[status(thm)],[t27410,t37]) ).
cnf(t34,plain,
top = join(sk3,sF8),
inference(cp,[status(thm)],[t32,t26]) ).
cnf(t36,plain,
join(sk3,sF8) = top,
inference(orient,[status(thm)],[t34]) ).
cnf(t26427,plain,
join(sF8,sk3) = top,
inference(step,[status(thm)],[t36,t37]) ).
cnf(t39,plain,
join(sF8,sk3) = top,
inference(rw,[status(thm)],[t26427]) ).
cnf(t43,plain,
join(sF8,sk3) = top,
inference(orient,[status(thm)],[t39]) ).
cnf(t145,plain,
join(sF8,join(sk3,X1)) = join(top,X1),
inference(cp,[status(thm)],[t139,t43]) ).
cnf(t336,plain,
join(sF8,join(sk3,X1)) = join(top,X1),
inference(orient,[status(thm)],[t145]) ).
cnf(t338,plain,
join(top,X1) = join(join(sk3,X1),sF8),
inference(cp,[status(thm)],[t336,t37]) ).
cnf(t26521,plain,
join(top,X1) = join(sk3,join(X1,sF8)),
inference(step,[status(thm)],[t338,t139]) ).
cnf(t497,plain,
join(sk3,join(X1,sF8)) = join(top,X1),
inference(orient,[status(thm)],[t26521]) ).
cnf(t419,plain,
complement(sk3) = join(sF8,complement(sk3)),
inference(cp,[status(thm)],[t417,t26]) ).
cnf(t26483,plain,
sF8 = join(sF8,complement(sk3)),
inference(step,[status(thm)],[t419,t26]) ).
cnf(t26484,plain,
sF8 = join(sF8,sF8),
inference(step,[status(thm)],[t26483,t26]) ).
cnf(t428,plain,
join(sF8,sF8) = sF8,
inference(orient,[status(thm)],[t26484]) ).
cnf(t500,plain,
join(top,sF8) = join(sk3,sF8),
inference(cp,[status(thm)],[t497,t428]) ).
cnf(t26522,plain,
join(sF8,top) = join(sk3,sF8),
inference(step,[status(thm)],[t500,t37]) ).
cnf(t47,plain,
top = join(sF6,sF7),
inference(cp,[status(thm)],[t32,t46]) ).
cnf(t48,plain,
join(sF6,sF7) = top,
inference(orient,[status(thm)],[t47]) ).
cnf(t146,plain,
join(sF6,join(sF7,X1)) = join(top,X1),
inference(cp,[status(thm)],[t139,t48]) ).
cnf(t340,plain,
join(sF6,join(sF7,X1)) = join(top,X1),
inference(orient,[status(thm)],[t146]) ).
cnf(t438,plain,
join(top,sF8) = join(sF6,sF9),
inference(cp,[status(thm)],[t340,t435]) ).
cnf(t26498,plain,
join(sF8,top) = join(sF6,sF9),
inference(step,[status(thm)],[t438,t37]) ).
cnf(t446,plain,
join(sF8,top) = join(sF6,sF9),
inference(orient,[status(thm)],[t26498]) ).
cnf(t26523,plain,
join(sF6,sF9) = join(sk3,sF8),
inference(step,[status(thm)],[t26522,t446]) ).
cnf(t26524,plain,
join(sF6,sF9) = join(sF8,sk3),
inference(step,[status(thm)],[t26523,t37]) ).
cnf(t26525,plain,
join(sF6,sF9) = top,
inference(step,[status(thm)],[t26524,t43]) ).
cnf(t503,plain,
join(sF6,sF9) = top,
inference(orient,[status(thm)],[t26525]) ).
cnf(t669,plain,
sF4 = join(sF5,complement(sF5)),
inference(cp,[status(thm)],[t663,t406]) ).
cnf(t26562,plain,
sF4 = top,
inference(step,[status(thm)],[t669,t32]) ).
cnf(t673,plain,
top = sF4,
inference(orient,[status(thm)],[t26562]) ).
cnf(t26597,plain,
join(sF6,sF9) = sF4,
inference(step,[status(thm)],[t503,t673]) ).
cnf(t718,plain,
join(sF6,sF9) = sF4,
inference(orient,[status(thm)],[t26597]) ).
cnf(t27412,plain,
sF4 = sF9,
inference(step,[status(thm)],[t27411,t718]) ).
cnf(t26332,plain,
sF9 = sF4,
inference(orient,[status(thm)],[t27412]) ).
cnf(t27413,plain,
join(sF7,sF8) = sF4,
inference(step,[status(thm)],[t435,t26332]) ).
cnf(t26333,plain,
join(sF7,sF8) = sF4,
inference(orient,[status(thm)],[t27413]) ).
cnf(u2,negated_conjecture,
meet(composition(sk2,sk1),sk3) != zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
complement(join(complement(composition(sk2,sk1)),complement(sk3))) != zero,
inference(definition_unfolding,[status(thm)],[u2,d0]) ).
cnf(g0_0,plain,
complement(join(complement(sF6),complement(sk3))) != zero,
inference(rw,[status(thm)],[goal_0,t31]) ).
cnf(g0_1,plain,
complement(join(sF7,complement(sk3))) != zero,
inference(rw,[status(thm)],[g0_0,t46]) ).
cnf(g0_2,plain,
complement(join(sF7,sF8)) != zero,
inference(rw,[status(thm)],[g0_1,t26]) ).
cnf(g0_3,plain,
complement(sF4) != zero,
inference(rw,[status(thm)],[g0_2,t26333]) ).
cnf(g0_4,plain,
sF5 != zero,
inference(rw,[status(thm)],[g0_3,t406]) ).
cnf(g0_5,plain,
sF5 != sF5,
inference(rw,[status(thm)],[g0_4,t401]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL011-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n016.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:16:11 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 61.10/9.54 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.10/9.54 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------