%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL038-1 : 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:35:59 PM UTC 2026
% Result : Unsatisfiable 132.81s 19.74s
% Output : CNFRefutation 132.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 84
% Number of leaves : 29
% Syntax : Number of clauses : 431 ( 431 unt; 0 nHn; 279 RR)
% Number of literals : 431 ( 430 equ; 32 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 22 con; 0-2 aty)
% Number of variables : 192 ( 6 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t12,axiom,
sF0 = composition(sk1,sk2),
introduced(definition) ).
cnf(t35,plain,
composition(sk1,sk2) = sF0,
inference(orient,[status(thm)],[t12]) ).
cnf(t13,axiom,
sF1 = complement(composition(sk1,sk2)),
introduced(definition) ).
cnf(t87204,plain,
sF1 = complement(sF0),
inference(step,[status(thm)],[t13,t35]) ).
cnf(t49,plain,
complement(sF0) = sF1,
inference(orient,[status(thm)],[t87204]) ).
cnf(t14,axiom,
sF2 = complement(sk3),
introduced(definition) ).
cnf(t28,plain,
complement(sk3) = sF2,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sF3 = join(complement(composition(sk1,sk2)),complement(sk3)),
introduced(definition) ).
cnf(t3,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t41,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t87223,plain,
sF3 = join(complement(sk3),complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t15,t41]) ).
cnf(t87224,plain,
sF3 = join(sF2,complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t87223,t28]) ).
cnf(t87225,plain,
sF3 = join(sF2,complement(sF0)),
inference(step,[status(thm)],[t87224,t35]) ).
cnf(t87226,plain,
sF3 = join(sF2,sF1),
inference(step,[status(thm)],[t87225,t49]) ).
cnf(t87227,plain,
sF3 = join(sF1,sF2),
inference(step,[status(thm)],[t87226,t41]) ).
cnf(t338,plain,
join(sF1,sF2) = sF3,
inference(orient,[status(thm)],[t87227]) ).
cnf(t16,axiom,
sF4 = complement(join(complement(composition(sk1,sk2)),complement(sk3))),
introduced(definition) ).
cnf(t87230,plain,
sF4 = complement(join(complement(sk3),complement(composition(sk1,sk2)))),
inference(step,[status(thm)],[t16,t41]) ).
cnf(t87231,plain,
sF4 = complement(join(sF2,complement(composition(sk1,sk2)))),
inference(step,[status(thm)],[t87230,t28]) ).
cnf(t87232,plain,
sF4 = complement(join(sF2,complement(sF0))),
inference(step,[status(thm)],[t87231,t35]) ).
cnf(t87233,plain,
sF4 = complement(join(sF2,sF1)),
inference(step,[status(thm)],[t87232,t49]) ).
cnf(t87234,plain,
sF4 = complement(join(sF1,sF2)),
inference(step,[status(thm)],[t87233,t41]) ).
cnf(t87235,plain,
sF4 = complement(sF3),
inference(step,[status(thm)],[t87234,t338]) ).
cnf(t368,plain,
complement(sF3) = sF4,
inference(orient,[status(thm)],[t87235]) ).
cnf(t17,axiom,
sF5 = complement(sk2),
introduced(definition) ).
cnf(t29,plain,
complement(sk2) = sF5,
inference(orient,[status(thm)],[t17]) ).
cnf(t18,axiom,
sF6 = converse(sk1),
introduced(definition) ).
cnf(t30,plain,
converse(sk1) = sF6,
inference(orient,[status(thm)],[t18]) ).
cnf(t19,axiom,
sF7 = composition(converse(sk1),sk3),
introduced(definition) ).
cnf(t87205,plain,
sF7 = composition(sF6,sk3),
inference(step,[status(thm)],[t19,t30]) ).
cnf(t53,plain,
composition(sF6,sk3) = sF7,
inference(orient,[status(thm)],[t87205]) ).
cnf(t20,axiom,
sF8 = complement(composition(converse(sk1),sk3)),
introduced(definition) ).
cnf(t87212,plain,
sF8 = complement(composition(sF6,sk3)),
inference(step,[status(thm)],[t20,t30]) ).
cnf(t87213,plain,
sF8 = complement(sF7),
inference(step,[status(thm)],[t87212,t53]) ).
cnf(t174,plain,
complement(sF7) = sF8,
inference(orient,[status(thm)],[t87213]) ).
cnf(t21,axiom,
sF9 = join(complement(sk2),complement(composition(converse(sk1),sk3))),
introduced(definition) ).
cnf(t87247,plain,
sF9 = join(sF5,complement(composition(converse(sk1),sk3))),
inference(step,[status(thm)],[t21,t29]) ).
cnf(t87248,plain,
sF9 = join(sF5,complement(composition(sF6,sk3))),
inference(step,[status(thm)],[t87247,t30]) ).
cnf(t87249,plain,
sF9 = join(sF5,complement(sF7)),
inference(step,[status(thm)],[t87248,t53]) ).
cnf(t87250,plain,
sF9 = join(sF5,sF8),
inference(step,[status(thm)],[t87249,t174]) ).
cnf(t412,plain,
join(sF5,sF8) = sF9,
inference(orient,[status(thm)],[t87250]) ).
cnf(t22,axiom,
sF10 = complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))),
introduced(definition) ).
cnf(t87267,plain,
sF10 = complement(join(sF5,complement(composition(converse(sk1),sk3)))),
inference(step,[status(thm)],[t22,t29]) ).
cnf(t87268,plain,
sF10 = complement(join(sF5,complement(composition(sF6,sk3)))),
inference(step,[status(thm)],[t87267,t30]) ).
cnf(t87269,plain,
sF10 = complement(join(sF5,complement(sF7))),
inference(step,[status(thm)],[t87268,t53]) ).
cnf(t87270,plain,
sF10 = complement(join(sF5,sF8)),
inference(step,[status(thm)],[t87269,t174]) ).
cnf(t87271,plain,
sF10 = complement(sF9),
inference(step,[status(thm)],[t87270,t412]) ).
cnf(t437,plain,
complement(sF9) = sF10,
inference(orient,[status(thm)],[t87271]) ).
cnf(t23,axiom,
sF11 = composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3))))),
introduced(definition) ).
cnf(t87278,plain,
sF11 = composition(sk1,complement(join(sF5,complement(composition(converse(sk1),sk3))))),
inference(step,[status(thm)],[t23,t29]) ).
cnf(t87279,plain,
sF11 = composition(sk1,complement(join(sF5,complement(composition(sF6,sk3))))),
inference(step,[status(thm)],[t87278,t30]) ).
cnf(t87280,plain,
sF11 = composition(sk1,complement(join(sF5,complement(sF7)))),
inference(step,[status(thm)],[t87279,t53]) ).
cnf(t87281,plain,
sF11 = composition(sk1,complement(join(sF5,sF8))),
inference(step,[status(thm)],[t87280,t174]) ).
cnf(t87282,plain,
sF11 = composition(sk1,complement(sF9)),
inference(step,[status(thm)],[t87281,t412]) ).
cnf(t87283,plain,
sF11 = composition(sk1,sF10),
inference(step,[status(thm)],[t87282,t437]) ).
cnf(t460,plain,
composition(sk1,sF10) = sF11,
inference(orient,[status(thm)],[t87283]) ).
cnf(t24,axiom,
sF12 = complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),
introduced(definition) ).
cnf(t87296,plain,
sF12 = complement(composition(sk1,complement(join(sF5,complement(composition(converse(sk1),sk3)))))),
inference(step,[status(thm)],[t24,t29]) ).
cnf(t87297,plain,
sF12 = complement(composition(sk1,complement(join(sF5,complement(composition(sF6,sk3)))))),
inference(step,[status(thm)],[t87296,t30]) ).
cnf(t87298,plain,
sF12 = complement(composition(sk1,complement(join(sF5,complement(sF7))))),
inference(step,[status(thm)],[t87297,t53]) ).
cnf(t87299,plain,
sF12 = complement(composition(sk1,complement(join(sF5,sF8)))),
inference(step,[status(thm)],[t87298,t174]) ).
cnf(t87300,plain,
sF12 = complement(composition(sk1,complement(sF9))),
inference(step,[status(thm)],[t87299,t412]) ).
cnf(t87301,plain,
sF12 = complement(composition(sk1,sF10)),
inference(step,[status(thm)],[t87300,t437]) ).
cnf(t87302,plain,
sF12 = complement(sF11),
inference(step,[status(thm)],[t87301,t460]) ).
cnf(t494,plain,
complement(sF11) = sF12,
inference(orient,[status(thm)],[t87302]) ).
cnf(t25,axiom,
sF13 = join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)),
introduced(definition) ).
cnf(t87309,plain,
sF13 = join(complement(sk3),complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3))))))),
inference(step,[status(thm)],[t25,t41]) ).
cnf(t87310,plain,
sF13 = join(sF2,complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3))))))),
inference(step,[status(thm)],[t87309,t28]) ).
cnf(t87311,plain,
sF13 = join(sF2,complement(composition(sk1,complement(join(sF5,complement(composition(converse(sk1),sk3))))))),
inference(step,[status(thm)],[t87310,t29]) ).
cnf(t87312,plain,
sF13 = join(sF2,complement(composition(sk1,complement(join(sF5,complement(composition(sF6,sk3))))))),
inference(step,[status(thm)],[t87311,t30]) ).
cnf(t87313,plain,
sF13 = join(sF2,complement(composition(sk1,complement(join(sF5,complement(sF7)))))),
inference(step,[status(thm)],[t87312,t53]) ).
cnf(t87314,plain,
sF13 = join(sF2,complement(composition(sk1,complement(join(sF5,sF8))))),
inference(step,[status(thm)],[t87313,t174]) ).
cnf(t87315,plain,
sF13 = join(sF2,complement(composition(sk1,complement(sF9)))),
inference(step,[status(thm)],[t87314,t412]) ).
cnf(t87316,plain,
sF13 = join(sF2,complement(composition(sk1,sF10))),
inference(step,[status(thm)],[t87315,t437]) ).
cnf(t87317,plain,
sF13 = join(sF2,complement(sF11)),
inference(step,[status(thm)],[t87316,t460]) ).
cnf(t87318,plain,
sF13 = join(sF2,sF12),
inference(step,[status(thm)],[t87317,t494]) ).
cnf(t527,plain,
join(sF2,sF12) = sF13,
inference(orient,[status(thm)],[t87318]) ).
cnf(t26,axiom,
sF14 = complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
introduced(definition) ).
cnf(t87323,plain,
sF14 = complement(join(complement(sk3),complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))))),
inference(step,[status(thm)],[t26,t41]) ).
cnf(t87324,plain,
sF14 = complement(join(sF2,complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))))),
inference(step,[status(thm)],[t87323,t28]) ).
cnf(t87325,plain,
sF14 = complement(join(sF2,complement(composition(sk1,complement(join(sF5,complement(composition(converse(sk1),sk3)))))))),
inference(step,[status(thm)],[t87324,t29]) ).
cnf(t87326,plain,
sF14 = complement(join(sF2,complement(composition(sk1,complement(join(sF5,complement(composition(sF6,sk3)))))))),
inference(step,[status(thm)],[t87325,t30]) ).
cnf(t87327,plain,
sF14 = complement(join(sF2,complement(composition(sk1,complement(join(sF5,complement(sF7))))))),
inference(step,[status(thm)],[t87326,t53]) ).
cnf(t87328,plain,
sF14 = complement(join(sF2,complement(composition(sk1,complement(join(sF5,sF8)))))),
inference(step,[status(thm)],[t87327,t174]) ).
cnf(t87329,plain,
sF14 = complement(join(sF2,complement(composition(sk1,complement(sF9))))),
inference(step,[status(thm)],[t87328,t412]) ).
cnf(t87330,plain,
sF14 = complement(join(sF2,complement(composition(sk1,sF10)))),
inference(step,[status(thm)],[t87329,t437]) ).
cnf(t87331,plain,
sF14 = complement(join(sF2,complement(sF11))),
inference(step,[status(thm)],[t87330,t460]) ).
cnf(t87332,plain,
sF14 = complement(join(sF2,sF12)),
inference(step,[status(thm)],[t87331,t494]) ).
cnf(t87333,plain,
sF14 = complement(sF13),
inference(step,[status(thm)],[t87332,t527]) ).
cnf(t548,plain,
complement(sF13) = sF14,
inference(orient,[status(thm)],[t87333]) ).
cnf(t11,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t87220,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t11,t41]) ).
cnf(t293,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t87220]) ).
cnf(t10,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t87218,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t10,t41]) ).
cnf(t214,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t87218]) ).
cnf(t5,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t54,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t5]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t32,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t58,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t54,t32]) ).
cnf(t192,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t58]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t31,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t193,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t192,t31]) ).
cnf(t87214,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t193,t32]) ).
cnf(t200,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t87214]) ).
cnf(t203,plain,
one = converse(one),
inference(cp,[status(thm)],[t200,t31]) ).
cnf(t206,plain,
converse(one) = one,
inference(orient,[status(thm)],[t203]) ).
cnf(t241,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t214,t206]) ).
cnf(t87217,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t200,t206]) ).
cnf(t207,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t87217]) ).
cnf(t211,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t207]) ).
cnf(t87245,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t241,t211]) ).
cnf(t87246,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t87245,t211]) ).
cnf(t402,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t87246]) ).
cnf(t410,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t293,t402]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t36,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t87377,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t410,t36]) ).
cnf(t87378,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t87377,t41]) ).
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(t4,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t87206,plain,
complement(top) = zero,
inference(step,[status(thm)],[t4,t36]) ).
cnf(t61,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t87206]) ).
cnf(t87379,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t87378,t61]) ).
cnf(t676,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t87379]) ).
cnf(t8,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)],[t8]) ).
cnf(t406,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t402,t61]) ).
cnf(t87257,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t406,t61]) ).
cnf(t87258,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t87257,t61]) ).
cnf(t422,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t87258]) ).
cnf(t423,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t143,t422]) ).
cnf(t837,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t423]) ).
cnf(t840,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t837,t676]) ).
cnf(t87398,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t840,t676]) ).
cnf(t841,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t87398]) ).
cnf(t87403,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t676,t841]) ).
cnf(t846,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t87403]) ).
cnf(t947,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t846]) ).
cnf(t950,plain,
complement(X1) = join(complement(join(X1,X2)),complement(join(complement(complement(X1)),complement(X2)))),
inference(cp,[status(thm)],[t293,t947]) ).
cnf(t88425,plain,
complement(X1) = join(complement(join(X1,X2)),complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t950,t947]) ).
cnf(t31006,plain,
join(complement(join(X1,X2)),complement(join(X1,complement(X2)))) = complement(X1),
inference(orient,[status(thm)],[t88425]) ).
cnf(t340,plain,
join(sF1,join(sF2,X1)) = join(sF3,X1),
inference(cp,[status(thm)],[t143,t338]) ).
cnf(t518,plain,
join(sF1,join(sF2,X1)) = join(sF3,X1),
inference(orient,[status(thm)],[t340]) ).
cnf(t147,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t143,t41]) ).
cnf(t87575,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t147,t143]) ).
cnf(t2863,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t87575]) ).
cnf(t224,plain,
complement(sk3) = join(complement(sk3),composition(converse(sF6),complement(sF7))),
inference(cp,[status(thm)],[t214,t53]) ).
cnf(t87241,plain,
sF2 = join(complement(sk3),composition(converse(sF6),complement(sF7))),
inference(step,[status(thm)],[t224,t28]) ).
cnf(t87242,plain,
sF2 = join(sF2,composition(converse(sF6),complement(sF7))),
inference(step,[status(thm)],[t87241,t28]) ).
cnf(t33,plain,
sk1 = converse(sF6),
inference(cp,[status(thm)],[t32,t30]) ).
cnf(t34,plain,
converse(sF6) = sk1,
inference(orient,[status(thm)],[t33]) ).
cnf(t87243,plain,
sF2 = join(sF2,composition(sk1,complement(sF7))),
inference(step,[status(thm)],[t87242,t34]) ).
cnf(t87244,plain,
sF2 = join(sF2,composition(sk1,sF8)),
inference(step,[status(thm)],[t87243,t174]) ).
cnf(t399,plain,
join(sF2,composition(sk1,sF8)) = sF2,
inference(orient,[status(thm)],[t87244]) ).
cnf(t2877,plain,
join(sF2,join(X1,composition(sk1,sF8))) = join(X1,sF2),
inference(cp,[status(thm)],[t2863,t399]) ).
cnf(t86726,plain,
join(sF2,join(X1,composition(sk1,sF8))) = join(X1,sF2),
inference(orient,[status(thm)],[t2877]) ).
cnf(t6,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t87,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t6]) ).
cnf(t90,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t87,t32]) ).
cnf(t264,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t90]) ).
cnf(t274,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t54,t264]) ).
cnf(t10574,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t274]) ).
cnf(t9,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t155,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t9]) ).
cnf(t56,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sF6),
inference(cp,[status(thm)],[t54,t30]) ).
cnf(t69,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sF6),
inference(orient,[status(thm)],[t56]) ).
cnf(t71,plain,
composition(converse(sk2),sF6) = converse(sF0),
inference(cp,[status(thm)],[t69,t35]) ).
cnf(t84,plain,
composition(converse(sk2),sF6) = converse(sF0),
inference(orient,[status(thm)],[t71]) ).
cnf(t166,plain,
composition(join(X1,converse(sk2)),sF6) = join(composition(X1,sF6),converse(sF0)),
inference(cp,[status(thm)],[t155,t84]) ).
cnf(t87598,plain,
composition(join(X1,converse(sk2)),sF6) = join(converse(sF0),composition(X1,sF6)),
inference(step,[status(thm)],[t166,t41]) ).
cnf(t3488,plain,
composition(join(X1,converse(sk2)),sF6) = join(converse(sF0),composition(X1,sF6)),
inference(orient,[status(thm)],[t87598]) ).
cnf(t10605,plain,
composition(converse(sF6),join(X1,converse(converse(sk2)))) = converse(join(converse(sF0),composition(converse(X1),sF6))),
inference(cp,[status(thm)],[t10574,t3488]) ).
cnf(t87842,plain,
composition(sk1,join(X1,converse(converse(sk2)))) = converse(join(converse(sF0),composition(converse(X1),sF6))),
inference(step,[status(thm)],[t10605,t34]) ).
cnf(t87843,plain,
composition(sk1,join(X1,sk2)) = converse(join(converse(sF0),composition(converse(X1),sF6))),
inference(step,[status(thm)],[t87842,t32]) ).
cnf(t87844,plain,
composition(sk1,join(X1,sk2)) = join(sF0,converse(composition(converse(X1),sF6))),
inference(step,[status(thm)],[t87843,t264]) ).
cnf(t59,plain,
converse(composition(X1,sF6)) = composition(sk1,converse(X1)),
inference(cp,[status(thm)],[t54,t34]) ).
cnf(t75,plain,
converse(composition(X1,sF6)) = composition(sk1,converse(X1)),
inference(orient,[status(thm)],[t59]) ).
cnf(t87845,plain,
composition(sk1,join(X1,sk2)) = join(sF0,composition(sk1,converse(converse(X1)))),
inference(step,[status(thm)],[t87844,t75]) ).
cnf(t87846,plain,
composition(sk1,join(X1,sk2)) = join(sF0,composition(sk1,X1)),
inference(step,[status(thm)],[t87845,t32]) ).
cnf(t10700,plain,
composition(sk1,join(X1,sk2)) = join(sF0,composition(sk1,X1)),
inference(orient,[status(thm)],[t87846]) ).
cnf(t308,plain,
X1 = join(complement(join(complement(X1),sF7)),complement(join(complement(X1),sF8))),
inference(cp,[status(thm)],[t293,t174]) ).
cnf(t87951,plain,
X1 = join(complement(join(sF7,complement(X1))),complement(join(complement(X1),sF8))),
inference(step,[status(thm)],[t308,t41]) ).
cnf(t87952,plain,
X1 = join(complement(join(sF7,complement(X1))),complement(join(sF8,complement(X1)))),
inference(step,[status(thm)],[t87951,t41]) ).
cnf(t14634,plain,
join(complement(join(sF7,complement(X1))),complement(join(sF8,complement(X1)))) = X1,
inference(orient,[status(thm)],[t87952]) ).
cnf(t440,plain,
sF9 = join(complement(join(sF10,X1)),complement(join(complement(sF9),complement(X1)))),
inference(cp,[status(thm)],[t293,t437]) ).
cnf(t88049,plain,
sF9 = join(complement(join(sF10,X1)),complement(join(sF10,complement(X1)))),
inference(step,[status(thm)],[t440,t437]) ).
cnf(t17645,plain,
join(complement(join(sF10,X1)),complement(join(sF10,complement(X1)))) = sF9,
inference(orient,[status(thm)],[t88049]) ).
cnf(t297,plain,
X1 = join(complement(join(complement(X1),sk2)),complement(join(complement(X1),sF5))),
inference(cp,[status(thm)],[t293,t29]) ).
cnf(t87909,plain,
X1 = join(complement(join(complement(X1),sF5)),complement(join(complement(X1),sk2))),
inference(step,[status(thm)],[t297,t41]) ).
cnf(t87910,plain,
X1 = join(complement(join(sF5,complement(X1))),complement(join(complement(X1),sk2))),
inference(step,[status(thm)],[t87909,t41]) ).
cnf(t87911,plain,
X1 = join(complement(join(sF5,complement(X1))),complement(join(sk2,complement(X1)))),
inference(step,[status(thm)],[t87910,t41]) ).
cnf(t13641,plain,
join(complement(join(sF5,complement(X1))),complement(join(sk2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t87911]) ).
cnf(t13647,plain,
sF7 = join(complement(join(sF5,sF8)),complement(join(sk2,complement(sF7)))),
inference(cp,[status(thm)],[t13641,t174]) ).
cnf(t88171,plain,
sF7 = join(complement(sF9),complement(join(sk2,complement(sF7)))),
inference(step,[status(thm)],[t13647,t412]) ).
cnf(t88172,plain,
sF7 = join(sF10,complement(join(sk2,complement(sF7)))),
inference(step,[status(thm)],[t88171,t437]) ).
cnf(t88173,plain,
sF7 = join(sF10,complement(join(sk2,sF8))),
inference(step,[status(thm)],[t88172,t174]) ).
cnf(t88174,plain,
sF7 = join(sF10,complement(join(sF8,sk2))),
inference(step,[status(thm)],[t88173,t41]) ).
cnf(t20549,plain,
join(sF10,complement(join(sF8,sk2))) = sF7,
inference(orient,[status(thm)],[t88174]) ).
cnf(t20569,plain,
sF9 = join(complement(sF7),complement(join(sF10,complement(complement(join(sF8,sk2)))))),
inference(cp,[status(thm)],[t17645,t20549]) ).
cnf(t88372,plain,
sF9 = join(sF8,complement(join(sF10,complement(complement(join(sF8,sk2)))))),
inference(step,[status(thm)],[t20569,t174]) ).
cnf(t88373,plain,
sF9 = join(sF8,complement(join(sF10,join(sF8,sk2)))),
inference(step,[status(thm)],[t88372,t947]) ).
cnf(t441,plain,
X1 = join(complement(join(complement(X1),sF9)),complement(join(complement(X1),sF10))),
inference(cp,[status(thm)],[t293,t437]) ).
cnf(t88059,plain,
X1 = join(complement(join(sF9,complement(X1))),complement(join(complement(X1),sF10))),
inference(step,[status(thm)],[t441,t41]) ).
cnf(t88060,plain,
X1 = join(complement(join(sF9,complement(X1))),complement(join(sF10,complement(X1)))),
inference(step,[status(thm)],[t88059,t41]) ).
cnf(t17746,plain,
join(complement(join(sF9,complement(X1))),complement(join(sF10,complement(X1)))) = X1,
inference(orient,[status(thm)],[t88060]) ).
cnf(t678,plain,
sk2 = join(zero,complement(sF5)),
inference(cp,[status(thm)],[t676,t29]) ).
cnf(t690,plain,
join(zero,complement(sF5)) = sk2,
inference(orient,[status(thm)],[t678]) ).
cnf(t87405,plain,
complement(sF5) = sk2,
inference(step,[status(thm)],[t690,t841]) ).
cnf(t848,plain,
complement(sF5) = sk2,
inference(rw,[status(thm)],[t87405]) ).
cnf(t874,plain,
complement(sF5) = sk2,
inference(orient,[status(thm)],[t848]) ).
cnf(t17756,plain,
sF5 = join(complement(join(sF9,sk2)),complement(join(sF10,complement(sF5)))),
inference(cp,[status(thm)],[t17746,t874]) ).
cnf(t414,plain,
join(sF5,join(sF8,X1)) = join(sF9,X1),
inference(cp,[status(thm)],[t143,t412]) ).
cnf(t738,plain,
join(sF5,join(sF8,X1)) = join(sF9,X1),
inference(orient,[status(thm)],[t414]) ).
cnf(t38,plain,
top = join(sk2,sF5),
inference(cp,[status(thm)],[t36,t29]) ).
cnf(t40,plain,
join(sk2,sF5) = top,
inference(orient,[status(thm)],[t38]) ).
cnf(t87203,plain,
join(sF5,sk2) = top,
inference(step,[status(thm)],[t40,t41]) ).
cnf(t43,plain,
join(sF5,sk2) = top,
inference(rw,[status(thm)],[t87203]) ).
cnf(t47,plain,
join(sF5,sk2) = top,
inference(orient,[status(thm)],[t43]) ).
cnf(t149,plain,
join(sF5,join(sk2,X1)) = join(top,X1),
inference(cp,[status(thm)],[t143,t47]) ).
cnf(t334,plain,
join(sF5,join(sk2,X1)) = join(top,X1),
inference(orient,[status(thm)],[t149]) ).
cnf(t337,plain,
join(top,X1) = join(sF5,join(X1,sk2)),
inference(cp,[status(thm)],[t334,t41]) ).
cnf(t513,plain,
join(sF5,join(X1,sk2)) = join(top,X1),
inference(orient,[status(thm)],[t337]) ).
cnf(t744,plain,
join(sF9,sk2) = join(top,sF8),
inference(cp,[status(thm)],[t738,t513]) ).
cnf(t87385,plain,
join(sF9,sk2) = join(sF8,top),
inference(step,[status(thm)],[t744,t41]) ).
cnf(t175,plain,
top = join(sF7,sF8),
inference(cp,[status(thm)],[t36,t174]) ).
cnf(t176,plain,
join(sF7,sF8) = top,
inference(orient,[status(thm)],[t175]) ).
cnf(t178,plain,
join(sF7,join(sF8,X1)) = join(top,X1),
inference(cp,[status(thm)],[t143,t176]) ).
cnf(t388,plain,
join(sF7,join(sF8,X1)) = join(top,X1),
inference(orient,[status(thm)],[t178]) ).
cnf(t407,plain,
complement(sF7) = join(sF8,complement(sF7)),
inference(cp,[status(thm)],[t402,t174]) ).
cnf(t87259,plain,
sF8 = join(sF8,complement(sF7)),
inference(step,[status(thm)],[t407,t174]) ).
cnf(t87260,plain,
sF8 = join(sF8,sF8),
inference(step,[status(thm)],[t87259,t174]) ).
cnf(t424,plain,
join(sF8,sF8) = sF8,
inference(orient,[status(thm)],[t87260]) ).
cnf(t426,plain,
join(top,sF8) = join(sF7,sF8),
inference(cp,[status(thm)],[t388,t424]) ).
cnf(t87265,plain,
join(sF8,top) = join(sF7,sF8),
inference(step,[status(thm)],[t426,t41]) ).
cnf(t87266,plain,
join(sF8,top) = top,
inference(step,[status(thm)],[t87265,t176]) ).
cnf(t433,plain,
join(sF8,top) = top,
inference(orient,[status(thm)],[t87266]) ).
cnf(t87386,plain,
join(sF9,sk2) = top,
inference(step,[status(thm)],[t87385,t433]) ).
cnf(t753,plain,
join(sF9,sk2) = top,
inference(orient,[status(thm)],[t87386]) ).
cnf(t88061,plain,
sF5 = join(complement(top),complement(join(sF10,complement(sF5)))),
inference(step,[status(thm)],[t17756,t753]) ).
cnf(t88062,plain,
sF5 = join(zero,complement(join(sF10,complement(sF5)))),
inference(step,[status(thm)],[t88061,t61]) ).
cnf(t88063,plain,
sF5 = complement(join(sF10,complement(sF5))),
inference(step,[status(thm)],[t88062,t841]) ).
cnf(t88064,plain,
sF5 = complement(join(sF10,sk2)),
inference(step,[status(thm)],[t88063,t874]) ).
cnf(t17788,plain,
complement(join(sF10,sk2)) = sF5,
inference(orient,[status(thm)],[t88064]) ).
cnf(t17792,plain,
join(sF10,sk2) = join(complement(join(sF5,X1)),complement(join(complement(join(sF10,sk2)),complement(X1)))),
inference(cp,[status(thm)],[t293,t17788]) ).
cnf(t88065,plain,
join(sF10,sk2) = join(complement(join(sF5,X1)),complement(join(sF5,complement(X1)))),
inference(step,[status(thm)],[t17792,t17788]) ).
cnf(t296,plain,
sk2 = join(complement(join(sF5,X1)),complement(join(complement(sk2),complement(X1)))),
inference(cp,[status(thm)],[t293,t29]) ).
cnf(t87903,plain,
sk2 = join(complement(join(sF5,X1)),complement(join(sF5,complement(X1)))),
inference(step,[status(thm)],[t296,t29]) ).
cnf(t13277,plain,
join(complement(join(sF5,X1)),complement(join(sF5,complement(X1)))) = sk2,
inference(orient,[status(thm)],[t87903]) ).
cnf(t88066,plain,
join(sF10,sk2) = sk2,
inference(step,[status(thm)],[t88065,t13277]) ).
cnf(t17836,plain,
join(sF10,sk2) = sk2,
inference(orient,[status(thm)],[t88066]) ).
cnf(t17844,plain,
join(sF10,join(X1,sk2)) = join(X1,sk2),
inference(cp,[status(thm)],[t2863,t17836]) ).
cnf(t17959,plain,
join(sF10,join(X1,sk2)) = join(X1,sk2),
inference(orient,[status(thm)],[t17844]) ).
cnf(t88374,plain,
sF9 = join(sF8,complement(join(sF8,sk2))),
inference(step,[status(thm)],[t88373,t17959]) ).
cnf(t28638,plain,
join(sF8,complement(join(sF8,sk2))) = sF9,
inference(orient,[status(thm)],[t88374]) ).
cnf(t28653,plain,
join(sF8,sk2) = join(complement(join(sF7,complement(join(sF8,sk2)))),complement(sF9)),
inference(cp,[status(thm)],[t14634,t28638]) ).
cnf(t88376,plain,
join(sF8,sk2) = join(complement(sF9),complement(join(sF7,complement(join(sF8,sk2))))),
inference(step,[status(thm)],[t28653,t41]) ).
cnf(t88377,plain,
join(sF8,sk2) = join(sF10,complement(join(sF7,complement(join(sF8,sk2))))),
inference(step,[status(thm)],[t88376,t437]) ).
cnf(t951,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t402,t947]) ).
cnf(t87432,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t951,t947]) ).
cnf(t87433,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t87432,t947]) ).
cnf(t1076,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t87433]) ).
cnf(t1096,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t143,t1076]) ).
cnf(t3161,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1096]) ).
cnf(t307,plain,
sF7 = join(complement(join(sF8,X1)),complement(join(complement(sF7),complement(X1)))),
inference(cp,[status(thm)],[t293,t174]) ).
cnf(t87950,plain,
sF7 = join(complement(join(sF8,X1)),complement(join(sF8,complement(X1)))),
inference(step,[status(thm)],[t307,t174]) ).
cnf(t14574,plain,
join(complement(join(sF8,X1)),complement(join(sF8,complement(X1)))) = sF7,
inference(orient,[status(thm)],[t87950]) ).
cnf(t14625,plain,
join(complement(join(sF8,X1)),complement(join(sF8,complement(X1)))) = join(complement(join(sF8,X1)),sF7),
inference(cp,[status(thm)],[t3161,t14574]) ).
cnf(t88209,plain,
sF7 = join(complement(join(sF8,X1)),sF7),
inference(step,[status(thm)],[t14625,t14574]) ).
cnf(t88210,plain,
sF7 = join(sF7,complement(join(sF8,X1))),
inference(step,[status(thm)],[t88209,t41]) ).
cnf(t22369,plain,
join(sF7,complement(join(sF8,X1))) = sF7,
inference(orient,[status(thm)],[t88210]) ).
cnf(t88378,plain,
join(sF8,sk2) = join(sF10,complement(sF7)),
inference(step,[status(thm)],[t88377,t22369]) ).
cnf(t88379,plain,
join(sF8,sk2) = join(sF10,sF8),
inference(step,[status(thm)],[t88378,t174]) ).
cnf(t88380,plain,
join(sF8,sk2) = join(sF8,sF10),
inference(step,[status(thm)],[t88379,t41]) ).
cnf(t28758,plain,
join(sF8,sk2) = join(sF8,sF10),
inference(orient,[status(thm)],[t88380]) ).
cnf(t28772,plain,
join(sF0,composition(sk1,sF8)) = composition(sk1,join(sF8,sF10)),
inference(cp,[status(thm)],[t10700,t28758]) ).
cnf(t461,plain,
composition(converse(sF10),sF6) = converse(sF11),
inference(cp,[status(thm)],[t69,t460]) ).
cnf(t466,plain,
composition(converse(sF10),sF6) = converse(sF11),
inference(orient,[status(thm)],[t461]) ).
cnf(t469,plain,
composition(join(X1,converse(sF10)),sF6) = join(composition(X1,sF6),converse(sF11)),
inference(cp,[status(thm)],[t155,t466]) ).
cnf(t87822,plain,
composition(join(X1,converse(sF10)),sF6) = join(converse(sF11),composition(X1,sF6)),
inference(step,[status(thm)],[t469,t41]) ).
cnf(t8526,plain,
composition(join(X1,converse(sF10)),sF6) = join(converse(sF11),composition(X1,sF6)),
inference(orient,[status(thm)],[t87822]) ).
cnf(t10622,plain,
composition(converse(sF6),join(X1,converse(converse(sF10)))) = converse(join(converse(sF11),composition(converse(X1),sF6))),
inference(cp,[status(thm)],[t10574,t8526]) ).
cnf(t87854,plain,
composition(sk1,join(X1,converse(converse(sF10)))) = converse(join(converse(sF11),composition(converse(X1),sF6))),
inference(step,[status(thm)],[t10622,t34]) ).
cnf(t87855,plain,
composition(sk1,join(X1,sF10)) = converse(join(converse(sF11),composition(converse(X1),sF6))),
inference(step,[status(thm)],[t87854,t32]) ).
cnf(t87856,plain,
composition(sk1,join(X1,sF10)) = join(sF11,converse(composition(converse(X1),sF6))),
inference(step,[status(thm)],[t87855,t264]) ).
cnf(t87857,plain,
composition(sk1,join(X1,sF10)) = join(sF11,composition(sk1,converse(converse(X1)))),
inference(step,[status(thm)],[t87856,t75]) ).
cnf(t87858,plain,
composition(sk1,join(X1,sF10)) = join(sF11,composition(sk1,X1)),
inference(step,[status(thm)],[t87857,t32]) ).
cnf(t10756,plain,
composition(sk1,join(X1,sF10)) = join(sF11,composition(sk1,X1)),
inference(orient,[status(thm)],[t87858]) ).
cnf(t88383,plain,
join(sF0,composition(sk1,sF8)) = join(sF11,composition(sk1,sF8)),
inference(step,[status(thm)],[t28772,t10756]) ).
cnf(t28813,plain,
join(sF11,composition(sk1,sF8)) = join(sF0,composition(sk1,sF8)),
inference(orient,[status(thm)],[t88383]) ).
cnf(t86741,plain,
join(sF11,sF2) = join(sF2,join(sF0,composition(sk1,sF8))),
inference(cp,[status(thm)],[t86726,t28813]) ).
cnf(t88834,plain,
join(sF2,sF11) = join(sF2,join(sF0,composition(sk1,sF8))),
inference(step,[status(thm)],[t86741,t41]) ).
cnf(t88835,plain,
join(sF2,sF11) = join(sF0,sF2),
inference(step,[status(thm)],[t88834,t86726]) ).
cnf(t86779,plain,
join(sF2,sF11) = join(sF0,sF2),
inference(orient,[status(thm)],[t88835]) ).
cnf(t86786,plain,
join(sF3,sF11) = join(sF1,join(sF0,sF2)),
inference(cp,[status(thm)],[t518,t86779]) ).
cnf(t521,plain,
join(sF3,X1) = join(sF1,join(X1,sF2)),
inference(cp,[status(thm)],[t518,t41]) ).
cnf(t1777,plain,
join(sF1,join(X1,sF2)) = join(sF3,X1),
inference(orient,[status(thm)],[t521]) ).
cnf(t88838,plain,
join(sF3,sF11) = join(sF3,sF0),
inference(step,[status(thm)],[t86786,t1777]) ).
cnf(t88839,plain,
join(sF3,sF11) = join(sF0,sF3),
inference(step,[status(thm)],[t88838,t41]) ).
cnf(t37,plain,
top = join(sk3,sF2),
inference(cp,[status(thm)],[t36,t28]) ).
cnf(t39,plain,
join(sk3,sF2) = top,
inference(orient,[status(thm)],[t37]) ).
cnf(t87202,plain,
join(sF2,sk3) = top,
inference(step,[status(thm)],[t39,t41]) ).
cnf(t42,plain,
join(sF2,sk3) = top,
inference(rw,[status(thm)],[t87202]) ).
cnf(t45,plain,
join(sF2,sk3) = top,
inference(orient,[status(thm)],[t42]) ).
cnf(t148,plain,
join(sF2,join(sk3,X1)) = join(top,X1),
inference(cp,[status(thm)],[t143,t45]) ).
cnf(t330,plain,
join(sF2,join(sk3,X1)) = join(top,X1),
inference(orient,[status(thm)],[t148]) ).
cnf(t332,plain,
join(top,X1) = join(join(sk3,X1),sF2),
inference(cp,[status(thm)],[t330,t41]) ).
cnf(t87284,plain,
join(top,X1) = join(sk3,join(X1,sF2)),
inference(step,[status(thm)],[t332,t143]) ).
cnf(t471,plain,
join(sk3,join(X1,sF2)) = join(top,X1),
inference(orient,[status(thm)],[t87284]) ).
cnf(t403,plain,
complement(sk3) = join(sF2,complement(sk3)),
inference(cp,[status(thm)],[t402,t28]) ).
cnf(t87251,plain,
sF2 = join(sF2,complement(sk3)),
inference(step,[status(thm)],[t403,t28]) ).
cnf(t87252,plain,
sF2 = join(sF2,sF2),
inference(step,[status(thm)],[t87251,t28]) ).
cnf(t415,plain,
join(sF2,sF2) = sF2,
inference(orient,[status(thm)],[t87252]) ).
cnf(t475,plain,
join(top,sF2) = join(sk3,sF2),
inference(cp,[status(thm)],[t471,t415]) ).
cnf(t87288,plain,
join(sF2,top) = join(sk3,sF2),
inference(step,[status(thm)],[t475,t41]) ).
cnf(t50,plain,
top = join(sF0,sF1),
inference(cp,[status(thm)],[t36,t49]) ).
cnf(t51,plain,
join(sF0,sF1) = top,
inference(orient,[status(thm)],[t50]) ).
cnf(t150,plain,
join(sF0,join(sF1,X1)) = join(top,X1),
inference(cp,[status(thm)],[t143,t51]) ).
cnf(t341,plain,
join(sF0,join(sF1,X1)) = join(top,X1),
inference(orient,[status(thm)],[t150]) ).
cnf(t345,plain,
join(top,sF2) = join(sF0,sF3),
inference(cp,[status(thm)],[t341,t338]) ).
cnf(t87228,plain,
join(sF2,top) = join(sF0,sF3),
inference(step,[status(thm)],[t345,t41]) ).
cnf(t346,plain,
join(sF2,top) = join(sF0,sF3),
inference(orient,[status(thm)],[t87228]) ).
cnf(t87289,plain,
join(sF0,sF3) = join(sk3,sF2),
inference(step,[status(thm)],[t87288,t346]) ).
cnf(t87290,plain,
join(sF0,sF3) = join(sF2,sk3),
inference(step,[status(thm)],[t87289,t41]) ).
cnf(t87291,plain,
join(sF0,sF3) = top,
inference(step,[status(thm)],[t87290,t45]) ).
cnf(t480,plain,
join(sF0,sF3) = top,
inference(orient,[status(thm)],[t87291]) ).
cnf(t88840,plain,
join(sF3,sF11) = top,
inference(step,[status(thm)],[t88839,t480]) ).
cnf(t87089,plain,
join(sF3,sF11) = top,
inference(orient,[status(thm)],[t88840]) ).
cnf(t87107,plain,
complement(sF3) = join(complement(top),complement(join(sF3,complement(sF11)))),
inference(cp,[status(thm)],[t31006,t87089]) ).
cnf(t88841,plain,
sF4 = join(complement(top),complement(join(sF3,complement(sF11)))),
inference(step,[status(thm)],[t87107,t368]) ).
cnf(t88842,plain,
sF4 = join(zero,complement(join(sF3,complement(sF11)))),
inference(step,[status(thm)],[t88841,t61]) ).
cnf(t88843,plain,
sF4 = complement(join(sF3,complement(sF11))),
inference(step,[status(thm)],[t88842,t841]) ).
cnf(t88844,plain,
sF4 = complement(join(sF3,sF12)),
inference(step,[status(thm)],[t88843,t494]) ).
cnf(t530,plain,
join(sF3,sF12) = join(sF1,sF13),
inference(cp,[status(thm)],[t518,t527]) ).
cnf(t535,plain,
join(sF3,sF12) = join(sF1,sF13),
inference(orient,[status(thm)],[t530]) ).
cnf(t551,plain,
sF13 = join(complement(join(sF14,X1)),complement(join(complement(sF13),complement(X1)))),
inference(cp,[status(thm)],[t293,t548]) ).
cnf(t88112,plain,
sF13 = join(complement(join(sF14,X1)),complement(join(sF14,complement(X1)))),
inference(step,[status(thm)],[t551,t548]) ).
cnf(t18579,plain,
join(complement(join(sF14,X1)),complement(join(sF14,complement(X1)))) = sF13,
inference(orient,[status(thm)],[t88112]) ).
cnf(t18634,plain,
join(complement(join(sF14,X1)),complement(join(sF14,complement(X1)))) = join(complement(join(sF14,X1)),sF13),
inference(cp,[status(thm)],[t3161,t18579]) ).
cnf(t88270,plain,
sF13 = join(complement(join(sF14,X1)),sF13),
inference(step,[status(thm)],[t18634,t18579]) ).
cnf(t88271,plain,
sF13 = join(sF13,complement(join(sF14,X1))),
inference(step,[status(thm)],[t88270,t41]) ).
cnf(t24890,plain,
join(sF13,complement(join(sF14,X1))) = sF13,
inference(orient,[status(thm)],[t88271]) ).
cnf(t27,axiom,
sF15 = join(complement(join(complement(composition(sk1,sk2)),complement(sk3))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))),
introduced(definition) ).
cnf(t87338,plain,
sF15 = join(complement(join(complement(sk3),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))),
inference(step,[status(thm)],[t27,t41]) ).
cnf(t87339,plain,
sF15 = join(complement(join(sF2,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))),
inference(step,[status(thm)],[t87338,t28]) ).
cnf(t87340,plain,
sF15 = join(complement(join(sF2,complement(sF0))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))),
inference(step,[status(thm)],[t87339,t35]) ).
cnf(t87341,plain,
sF15 = join(complement(join(sF2,sF1)),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))),
inference(step,[status(thm)],[t87340,t49]) ).
cnf(t87342,plain,
sF15 = join(complement(join(sF1,sF2)),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))),
inference(step,[status(thm)],[t87341,t41]) ).
cnf(t87343,plain,
sF15 = join(complement(sF3),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))),
inference(step,[status(thm)],[t87342,t338]) ).
cnf(t87344,plain,
sF15 = join(sF4,complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))),
inference(step,[status(thm)],[t87343,t368]) ).
cnf(t87345,plain,
sF15 = join(sF4,complement(join(complement(sk3),complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3))))))))),
inference(step,[status(thm)],[t87344,t41]) ).
cnf(t87346,plain,
sF15 = join(sF4,complement(join(sF2,complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3))))))))),
inference(step,[status(thm)],[t87345,t28]) ).
cnf(t87347,plain,
sF15 = join(sF4,complement(join(sF2,complement(composition(sk1,complement(join(sF5,complement(composition(converse(sk1),sk3))))))))),
inference(step,[status(thm)],[t87346,t29]) ).
cnf(t87348,plain,
sF15 = join(sF4,complement(join(sF2,complement(composition(sk1,complement(join(sF5,complement(composition(sF6,sk3))))))))),
inference(step,[status(thm)],[t87347,t30]) ).
cnf(t87349,plain,
sF15 = join(sF4,complement(join(sF2,complement(composition(sk1,complement(join(sF5,complement(sF7)))))))),
inference(step,[status(thm)],[t87348,t53]) ).
cnf(t87350,plain,
sF15 = join(sF4,complement(join(sF2,complement(composition(sk1,complement(join(sF5,sF8))))))),
inference(step,[status(thm)],[t87349,t174]) ).
cnf(t87351,plain,
sF15 = join(sF4,complement(join(sF2,complement(composition(sk1,complement(sF9)))))),
inference(step,[status(thm)],[t87350,t412]) ).
cnf(t87352,plain,
sF15 = join(sF4,complement(join(sF2,complement(composition(sk1,sF10))))),
inference(step,[status(thm)],[t87351,t437]) ).
cnf(t87353,plain,
sF15 = join(sF4,complement(join(sF2,complement(sF11)))),
inference(step,[status(thm)],[t87352,t460]) ).
cnf(t87354,plain,
sF15 = join(sF4,complement(join(sF2,sF12))),
inference(step,[status(thm)],[t87353,t494]) ).
cnf(t87355,plain,
sF15 = join(sF4,complement(sF13)),
inference(step,[status(thm)],[t87354,t527]) ).
cnf(t87356,plain,
sF15 = join(sF4,sF14),
inference(step,[status(thm)],[t87355,t548]) ).
cnf(t588,plain,
join(sF4,sF14) = sF15,
inference(orient,[status(thm)],[t87356]) ).
cnf(t590,plain,
join(sF4,join(sF14,X1)) = join(sF15,X1),
inference(cp,[status(thm)],[t143,t588]) ).
cnf(t2092,plain,
join(sF4,join(sF14,X1)) = join(sF15,X1),
inference(orient,[status(thm)],[t590]) ).
cnf(t2096,plain,
join(sF15,sF14) = join(sF4,sF14),
inference(cp,[status(thm)],[t2092,t1076]) ).
cnf(t87515,plain,
join(sF14,sF15) = join(sF4,sF14),
inference(step,[status(thm)],[t2096,t41]) ).
cnf(t87516,plain,
join(sF14,sF15) = sF15,
inference(step,[status(thm)],[t87515,t588]) ).
cnf(t2103,plain,
join(sF14,sF15) = sF15,
inference(orient,[status(thm)],[t87516]) ).
cnf(t24893,plain,
sF13 = join(sF13,complement(sF15)),
inference(cp,[status(thm)],[t24890,t2103]) ).
cnf(t24920,plain,
join(sF13,complement(sF15)) = sF13,
inference(orient,[status(thm)],[t24893]) ).
cnf(t26336,plain,
join(sF13,complement(sF4)) = sF13,
inference(rw,[status(thm)],[t24920]) ).
cnf(t682,plain,
sF3 = join(zero,complement(sF4)),
inference(cp,[status(thm)],[t676,t368]) ).
cnf(t699,plain,
join(zero,complement(sF4)) = sF3,
inference(orient,[status(thm)],[t682]) ).
cnf(t87408,plain,
complement(sF4) = sF3,
inference(step,[status(thm)],[t699,t841]) ).
cnf(t851,plain,
complement(sF4) = sF3,
inference(rw,[status(thm)],[t87408]) ).
cnf(t894,plain,
complement(sF4) = sF3,
inference(orient,[status(thm)],[t851]) ).
cnf(t88320,plain,
join(sF13,sF3) = sF13,
inference(step,[status(thm)],[t26336,t894]) ).
cnf(t88321,plain,
join(sF3,sF13) = sF13,
inference(step,[status(thm)],[t88320,t41]) ).
cnf(t416,plain,
join(sF2,join(sF2,X1)) = join(sF2,X1),
inference(cp,[status(thm)],[t143,t415]) ).
cnf(t774,plain,
join(sF2,join(sF2,X1)) = join(sF2,X1),
inference(orient,[status(thm)],[t416]) ).
cnf(t777,plain,
join(sF2,sF12) = join(sF2,sF13),
inference(cp,[status(thm)],[t774,t527]) ).
cnf(t87390,plain,
sF13 = join(sF2,sF13),
inference(step,[status(thm)],[t777,t527]) ).
cnf(t780,plain,
join(sF2,sF13) = sF13,
inference(orient,[status(thm)],[t87390]) ).
cnf(t783,plain,
join(sF3,sF13) = join(sF1,sF13),
inference(cp,[status(thm)],[t518,t780]) ).
cnf(t784,plain,
join(sF3,sF13) = join(sF1,sF13),
inference(orient,[status(thm)],[t783]) ).
cnf(t88322,plain,
join(sF1,sF13) = sF13,
inference(step,[status(thm)],[t88321,t784]) ).
cnf(t26503,plain,
join(sF1,sF13) = sF13,
inference(orient,[status(thm)],[t88322]) ).
cnf(t88323,plain,
join(sF3,sF12) = sF13,
inference(step,[status(thm)],[t535,t26503]) ).
cnf(t26504,plain,
join(sF3,sF12) = sF13,
inference(orient,[status(thm)],[t88323]) ).
cnf(t88845,plain,
sF4 = complement(sF13),
inference(step,[status(thm)],[t88844,t26504]) ).
cnf(t88846,plain,
sF4 = sF14,
inference(step,[status(thm)],[t88845,t548]) ).
cnf(t87134,plain,
sF14 = sF4,
inference(orient,[status(thm)],[t88846]) ).
cnf(t88847,plain,
complement(sF13) = sF4,
inference(step,[status(thm)],[t548,t87134]) ).
cnf(t87135,plain,
complement(sF13) = sF4,
inference(orient,[status(thm)],[t88847]) ).
cnf(u1,negated_conjecture,
join(meet(composition(sk1,sk2),sk3),meet(composition(sk1,meet(sk2,composition(converse(sk1),sk3))),sk3)) != meet(composition(sk1,meet(sk2,composition(converse(sk1),sk3))),sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
join(complement(join(complement(composition(sk1,sk2)),complement(sk3))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(g0_0,plain,
join(complement(join(complement(sF0),complement(sk3))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[goal_0,t35]) ).
cnf(g0_1,plain,
join(complement(join(sF1,complement(sk3))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_0,t49]) ).
cnf(g0_2,plain,
join(complement(join(sF1,sF2)),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_1,t28]) ).
cnf(g0_3,plain,
join(complement(sF3),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_2,t338]) ).
cnf(g0_4,plain,
join(sF4,complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_3,t368]) ).
cnf(g0_5,plain,
join(sF4,complement(join(complement(composition(sk1,complement(join(sF5,complement(composition(converse(sk1),sk3)))))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_4,t29]) ).
cnf(g0_6,plain,
join(sF4,complement(join(complement(composition(sk1,complement(join(sF5,complement(composition(sF6,sk3)))))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_5,t30]) ).
cnf(g0_7,plain,
join(sF4,complement(join(complement(composition(sk1,complement(join(sF5,complement(sF7))))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_6,t53]) ).
cnf(g0_8,plain,
join(sF4,complement(join(complement(composition(sk1,complement(join(sF5,sF8)))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_7,t174]) ).
cnf(g0_9,plain,
join(sF4,complement(join(complement(composition(sk1,complement(sF9))),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_8,t412]) ).
cnf(g0_10,plain,
join(sF4,complement(join(complement(composition(sk1,sF10)),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_9,t437]) ).
cnf(g0_11,plain,
join(sF4,complement(join(complement(sF11),complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_10,t460]) ).
cnf(g0_12,plain,
join(sF4,complement(join(sF12,complement(sk3)))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_11,t494]) ).
cnf(g0_13,plain,
join(sF4,complement(join(sF12,sF2))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_12,t28]) ).
cnf(g0_14,plain,
join(sF4,complement(join(sF2,sF12))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_13,t41]) ).
cnf(g0_15,plain,
join(sF4,complement(sF13)) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_14,t527]) ).
cnf(g0_16,plain,
join(sF4,sF4) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_15,t87135]) ).
cnf(g0_17,plain,
sF4 != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_16,t1076]) ).
cnf(g0_18,plain,
sF4 != complement(join(complement(composition(sk1,complement(join(sF5,complement(composition(converse(sk1),sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_17,t29]) ).
cnf(g0_19,plain,
sF4 != complement(join(complement(composition(sk1,complement(join(sF5,complement(composition(sF6,sk3)))))),complement(sk3))),
inference(rw,[status(thm)],[g0_18,t30]) ).
cnf(g0_20,plain,
sF4 != complement(join(complement(composition(sk1,complement(join(sF5,complement(sF7))))),complement(sk3))),
inference(rw,[status(thm)],[g0_19,t53]) ).
cnf(g0_21,plain,
sF4 != complement(join(complement(composition(sk1,complement(join(sF5,sF8)))),complement(sk3))),
inference(rw,[status(thm)],[g0_20,t174]) ).
cnf(g0_22,plain,
sF4 != complement(join(complement(composition(sk1,complement(sF9))),complement(sk3))),
inference(rw,[status(thm)],[g0_21,t412]) ).
cnf(g0_23,plain,
sF4 != complement(join(complement(composition(sk1,sF10)),complement(sk3))),
inference(rw,[status(thm)],[g0_22,t437]) ).
cnf(g0_24,plain,
sF4 != complement(join(complement(sF11),complement(sk3))),
inference(rw,[status(thm)],[g0_23,t460]) ).
cnf(g0_25,plain,
sF4 != complement(join(sF12,complement(sk3))),
inference(rw,[status(thm)],[g0_24,t494]) ).
cnf(g0_26,plain,
sF4 != complement(join(sF12,sF2)),
inference(rw,[status(thm)],[g0_25,t28]) ).
cnf(g0_27,plain,
sF4 != complement(join(sF2,sF12)),
inference(rw,[status(thm)],[g0_26,t41]) ).
cnf(g0_28,plain,
sF4 != complement(sF13),
inference(rw,[status(thm)],[g0_27,t527]) ).
cnf(g0_29,plain,
sF4 != sF4,
inference(rw,[status(thm)],[g0_28,t87135]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_29]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL038-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.46 % Computer : n017.cluster.edu
% 0.18/0.46 % Model : x86_64 x86_64
% 0.18/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.46 % Memory : 8046.5625MB
% 0.18/0.46 % OS : Linux 6.8.0-71-generic
% 0.18/0.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Thu Sep 24 07:27:15 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.46 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 132.81/19.74 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 132.81/19.74 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------