%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL022-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.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 62.93s 8.73s
% Output : CNFRefutation 62.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 23
% Syntax : Number of clauses : 386 ( 386 unt; 0 nHn; 216 RR)
% Number of literals : 386 ( 385 equ; 19 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 13 con; 0-2 aty)
% Number of variables : 225 ( 25 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t133,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t17,axiom,
sFlat1 = complement(sk2),
introduced(definition) ).
cnf(t107,plain,
complement(sk2) = sFlat1,
inference(orient,[status(thm)],[t17]) ).
cnf(t16,axiom,
sFlat0 = complement(sk1),
introduced(definition) ).
cnf(t92,plain,
complement(sk1) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t18,axiom,
sFlat2 = join(complement(sk1),complement(sk2)),
introduced(definition) ).
cnf(t35733,plain,
sFlat2 = join(complement(sk2),complement(sk1)),
inference(step,[status(thm)],[t18,t133]) ).
cnf(t35734,plain,
sFlat2 = join(sFlat1,complement(sk1)),
inference(step,[status(thm)],[t35733,t107]) ).
cnf(t35735,plain,
sFlat2 = join(sFlat1,sFlat0),
inference(step,[status(thm)],[t35734,t92]) ).
cnf(t35736,plain,
sFlat2 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t35735,t133]) ).
cnf(t169,plain,
join(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t35736]) ).
cnf(t19,axiom,
sFlat3 = complement(join(complement(sk1),complement(sk2))),
introduced(definition) ).
cnf(t62,plain,
complement(join(complement(sk1),complement(sk2))) = sFlat3,
inference(orient,[status(thm)],[t19]) ).
cnf(t35724,plain,
complement(join(sFlat0,complement(sk2))) = sFlat3,
inference(step,[status(thm)],[t62,t92]) ).
cnf(t105,plain,
complement(join(sFlat0,complement(sk2))) = sFlat3,
inference(rw,[status(thm)],[t35724]) ).
cnf(t35747,plain,
complement(join(sFlat0,sFlat1)) = sFlat3,
inference(step,[status(thm)],[t105,t107]) ).
cnf(t35748,plain,
complement(sFlat2) = sFlat3,
inference(step,[status(thm)],[t35747,t169]) ).
cnf(t220,plain,
complement(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t35748]) ).
cnf(t20,axiom,
sFlat4 = complement(one),
introduced(definition) ).
cnf(t120,plain,
complement(one) = sFlat4,
inference(orient,[status(thm)],[t20]) ).
cnf(t21,axiom,
sFlat5 = join(complement(sk1),complement(one)),
introduced(definition) ).
cnf(t35738,plain,
sFlat5 = join(sFlat0,complement(one)),
inference(step,[status(thm)],[t21,t92]) ).
cnf(t35739,plain,
sFlat5 = join(sFlat0,sFlat4),
inference(step,[status(thm)],[t35738,t120]) ).
cnf(t172,plain,
join(sFlat0,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t35739]) ).
cnf(t22,axiom,
sFlat6 = complement(join(complement(sk1),complement(one))),
introduced(definition) ).
cnf(t77,plain,
complement(join(complement(sk1),complement(one))) = sFlat6,
inference(orient,[status(thm)],[t22]) ).
cnf(t35725,plain,
complement(join(sFlat0,complement(one))) = sFlat6,
inference(step,[status(thm)],[t77,t92]) ).
cnf(t106,plain,
complement(join(sFlat0,complement(one))) = sFlat6,
inference(rw,[status(thm)],[t35725]) ).
cnf(t35749,plain,
complement(join(sFlat0,sFlat4)) = sFlat6,
inference(step,[status(thm)],[t106,t120]) ).
cnf(t35750,plain,
complement(sFlat5) = sFlat6,
inference(step,[status(thm)],[t35749,t172]) ).
cnf(t227,plain,
complement(sFlat5) = sFlat6,
inference(orient,[status(thm)],[t35750]) ).
cnf(t23,axiom,
sFlat7 = composition(complement(join(complement(sk1),complement(one))),sk2),
introduced(definition) ).
cnf(t35740,plain,
sFlat7 = composition(complement(join(sFlat0,complement(one))),sk2),
inference(step,[status(thm)],[t23,t92]) ).
cnf(t35741,plain,
sFlat7 = composition(complement(join(sFlat0,sFlat4)),sk2),
inference(step,[status(thm)],[t35740,t120]) ).
cnf(t35742,plain,
sFlat7 = composition(complement(sFlat5),sk2),
inference(step,[status(thm)],[t35741,t172]) ).
cnf(t188,plain,
composition(complement(sFlat5),sk2) = sFlat7,
inference(orient,[status(thm)],[t35742]) ).
cnf(t35751,plain,
composition(sFlat6,sk2) = sFlat7,
inference(step,[status(thm)],[t188,t227]) ).
cnf(t232,plain,
composition(sFlat6,sk2) = sFlat7,
inference(rw,[status(thm)],[t35751]) ).
cnf(t235,plain,
composition(sFlat6,sk2) = sFlat7,
inference(orient,[status(thm)],[t232]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t174,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/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/sandbox2/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(t410,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t195]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/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(t35779,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t135,t133]) ).
cnf(t620,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t35779]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t202,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t646,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t620,t202]) ).
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(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(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t138,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t35726,plain,
complement(top) = zero,
inference(step,[status(thm)],[t33,t138]) ).
cnf(t142,plain,
complement(top) = zero,
inference(rw,[status(thm)],[t35726]) ).
cnf(t207,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t142]) ).
cnf(t35980,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t646,t207]) ).
cnf(t35981,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t35980,t207]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t143,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t411,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t410,t28]) ).
cnf(t35758,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t411,t29]) ).
cnf(t426,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t35758]) ).
cnf(t427,plain,
one = converse(one),
inference(cp,[status(thm)],[t426,t28]) ).
cnf(t434,plain,
converse(one) = one,
inference(orient,[status(thm)],[t427]) ).
cnf(t629,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t620,t434]) ).
cnf(t35759,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t426,t434]) ).
cnf(t445,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t35759]) ).
cnf(t446,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t445]) ).
cnf(t35780,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t629,t446]) ).
cnf(t35781,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t35780,t446]) ).
cnf(t652,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t35781]) ).
cnf(t655,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t652,t207]) ).
cnf(t35786,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t655,t207]) ).
cnf(t35787,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t35786,t207]) ).
cnf(t681,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t35787]) ).
cnf(t682,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t143,t681]) ).
cnf(t823,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t682]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/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(t35752,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t134,t133]) ).
cnf(t288,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t35752]) ).
cnf(t666,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t288,t652]) ).
cnf(t35824,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t666,t138]) ).
cnf(t35825,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t35824,t207]) ).
cnf(t35826,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t35825,t133]) ).
cnf(t757,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t35826]) ).
cnf(t829,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t823,t757]) ).
cnf(t35855,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t829,t757]) ).
cnf(t847,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t35855]) ).
cnf(t35982,plain,
zero = composition(converse(sk1),complement(sk1)),
inference(step,[status(thm)],[t35981,t847]) ).
cnf(t35983,plain,
zero = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t35982,t92]) ).
cnf(t1780,plain,
composition(converse(sk1),sFlat0) = zero,
inference(orient,[status(thm)],[t35983]) ).
cnf(t1782,plain,
composition(join(converse(sk1),X1),sFlat0) = join(zero,composition(X1,sFlat0)),
inference(cp,[status(thm)],[t174,t1780]) ).
cnf(t36005,plain,
composition(join(converse(sk1),X1),sFlat0) = composition(X1,sFlat0),
inference(step,[status(thm)],[t1782,t847]) ).
cnf(t1977,plain,
composition(join(converse(sk1),X1),sFlat0) = composition(X1,sFlat0),
inference(orient,[status(thm)],[t36005]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t177,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t1978,plain,
composition(converse(X1),sFlat0) = composition(converse(join(sk1,X1)),sFlat0),
inference(cp,[status(thm)],[t1977,t177]) ).
cnf(t6598,plain,
composition(converse(join(sk1,X1)),sFlat0) = composition(converse(X1),sFlat0),
inference(orient,[status(thm)],[t1978]) ).
cnf(t205,plain,
composition(join(X1,sk1),top) = join(composition(X1,top),sk1),
inference(cp,[status(thm)],[t174,t202]) ).
cnf(t35766,plain,
composition(join(X1,sk1),top) = join(sk1,composition(X1,top)),
inference(step,[status(thm)],[t205,t133]) ).
cnf(t534,plain,
composition(join(X1,sk1),top) = join(sk1,composition(X1,top)),
inference(orient,[status(thm)],[t35766]) ).
cnf(t35862,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t757,t847]) ).
cnf(t869,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t35862]) ).
cnf(t1015,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t869]) ).
cnf(t1016,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t652,t1015]) ).
cnf(t35915,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1016,t1015]) ).
cnf(t35916,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t35915,t1015]) ).
cnf(t1094,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t35916]) ).
cnf(t1105,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t143,t1094]) ).
cnf(t1339,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1105]) ).
cnf(t1349,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = join(complement(join(complement(X1),X2)),X1),
inference(cp,[status(thm)],[t1339,t288]) ).
cnf(t36109,plain,
X1 = join(complement(join(complement(X1),X2)),X1),
inference(step,[status(thm)],[t1349,t288]) ).
cnf(t36110,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t36109,t133]) ).
cnf(t3060,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t36110]) ).
cnf(t3078,plain,
sk1 = join(sk1,complement(join(sFlat0,X1))),
inference(cp,[status(thm)],[t3060,t92]) ).
cnf(t3329,plain,
join(sk1,complement(join(sFlat0,X1))) = sk1,
inference(orient,[status(thm)],[t3078]) ).
cnf(t759,plain,
sFlat2 = join(zero,complement(sFlat3)),
inference(cp,[status(thm)],[t757,t220]) ).
cnf(t766,plain,
join(zero,complement(sFlat3)) = sFlat2,
inference(orient,[status(thm)],[t759]) ).
cnf(t35859,plain,
complement(sFlat3) = sFlat2,
inference(step,[status(thm)],[t766,t847]) ).
cnf(t866,plain,
complement(sFlat3) = sFlat2,
inference(rw,[status(thm)],[t35859]) ).
cnf(t910,plain,
complement(sFlat3) = sFlat2,
inference(orient,[status(thm)],[t866]) ).
cnf(t911,plain,
complement(sFlat3) = join(sFlat2,complement(sFlat3)),
inference(cp,[status(thm)],[t652,t910]) ).
cnf(t35882,plain,
sFlat2 = join(sFlat2,complement(sFlat3)),
inference(step,[status(thm)],[t911,t910]) ).
cnf(t35883,plain,
sFlat2 = join(sFlat2,sFlat2),
inference(step,[status(thm)],[t35882,t910]) ).
cnf(t170,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t143,t169]) ).
cnf(t240,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t170]) ).
cnf(t243,plain,
join(sFlat2,X1) = join(sFlat0,join(X1,sFlat1)),
inference(cp,[status(thm)],[t240,t133]) ).
cnf(t319,plain,
join(sFlat0,join(X1,sFlat1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t243]) ).
cnf(t657,plain,
complement(sk2) = join(sFlat1,complement(sk2)),
inference(cp,[status(thm)],[t652,t107]) ).
cnf(t35790,plain,
sFlat1 = join(sFlat1,complement(sk2)),
inference(step,[status(thm)],[t657,t107]) ).
cnf(t35791,plain,
sFlat1 = join(sFlat1,sFlat1),
inference(step,[status(thm)],[t35790,t107]) ).
cnf(t688,plain,
join(sFlat1,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t35791]) ).
cnf(t689,plain,
join(sFlat2,sFlat1) = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t319,t688]) ).
cnf(t35806,plain,
join(sFlat1,sFlat2) = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t689,t133]) ).
cnf(t35807,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t35806,t169]) ).
cnf(t713,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t35807]) ).
cnf(t714,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t240,t713]) ).
cnf(t755,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(orient,[status(thm)],[t714]) ).
cnf(t35884,plain,
sFlat2 = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t35883,t755]) ).
cnf(t1057,plain,
join(sFlat0,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t35884]) ).
cnf(t3335,plain,
sk1 = join(sk1,complement(sFlat2)),
inference(cp,[status(thm)],[t3329,t1057]) ).
cnf(t36120,plain,
sk1 = join(sk1,sFlat3),
inference(step,[status(thm)],[t3335,t220]) ).
cnf(t36121,plain,
sk1 = join(sFlat3,sk1),
inference(step,[status(thm)],[t36120,t133]) ).
cnf(t3360,plain,
join(sFlat3,sk1) = sk1,
inference(orient,[status(thm)],[t36121]) ).
cnf(t3362,plain,
join(sk1,composition(sFlat3,top)) = composition(sk1,top),
inference(cp,[status(thm)],[t534,t3360]) ).
cnf(t36123,plain,
join(sk1,composition(sFlat3,top)) = sk1,
inference(step,[status(thm)],[t3362,t202]) ).
cnf(t3374,plain,
join(sk1,composition(sFlat3,top)) = sk1,
inference(orient,[status(thm)],[t36123]) ).
cnf(t6610,plain,
composition(converse(composition(sFlat3,top)),sFlat0) = composition(converse(sk1),sFlat0),
inference(cp,[status(thm)],[t6598,t3374]) ).
cnf(t144,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t143,t138]) ).
cnf(t940,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t144]) ).
cnf(t1107,plain,
top = join(X1,join(X1,complement(X1))),
inference(cp,[status(thm)],[t940,t1094]) ).
cnf(t35917,plain,
top = join(X1,top),
inference(step,[status(thm)],[t1107,t138]) ).
cnf(t1111,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t35917]) ).
cnf(t1112,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t1111,t133]) ).
cnf(t1118,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t1112]) ).
cnf(t179,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t177,t29]) ).
cnf(t376,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t179]) ).
cnf(t377,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t376,t138]) ).
cnf(t498,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t377]) ).
cnf(t1151,plain,
top = converse(top),
inference(cp,[status(thm)],[t1118,t498]) ).
cnf(t1161,plain,
converse(top) = top,
inference(orient,[status(thm)],[t1151]) ).
cnf(t1166,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t193,t1161]) ).
cnf(t1207,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t1166]) ).
cnf(t36234,plain,
composition(composition(top,converse(sFlat3)),sFlat0) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t6610,t1207]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t182,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t36235,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t36234,t182]) ).
cnf(t36236,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = zero,
inference(step,[status(thm)],[t36235,t1780]) ).
cnf(t6639,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = zero,
inference(orient,[status(thm)],[t36236]) ).
cnf(t6643,plain,
composition(join(top,X1),composition(converse(sFlat3),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat3),sFlat0))),
inference(cp,[status(thm)],[t174,t6639]) ).
cnf(t36244,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat3),sFlat0))),
inference(step,[status(thm)],[t6643,t1118]) ).
cnf(t36245,plain,
zero = join(zero,composition(X1,composition(converse(sFlat3),sFlat0))),
inference(step,[status(thm)],[t36244,t6639]) ).
cnf(t36246,plain,
zero = composition(X1,composition(converse(sFlat3),sFlat0)),
inference(step,[status(thm)],[t36245,t847]) ).
cnf(t6691,plain,
composition(X1,composition(converse(sFlat3),sFlat0)) = zero,
inference(orient,[status(thm)],[t36246]) ).
cnf(t6692,plain,
zero = composition(converse(sFlat3),sFlat0),
inference(cp,[status(thm)],[t6691,t446]) ).
cnf(t6705,plain,
composition(converse(sFlat3),sFlat0) = zero,
inference(orient,[status(thm)],[t6692]) ).
cnf(t6711,plain,
composition(converse(sFlat0),sFlat3) = converse(zero),
inference(cp,[status(thm)],[t410,t6705]) ).
cnf(t180,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t177,t29]) ).
cnf(t386,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t180]) ).
cnf(t862,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t386,t847]) ).
cnf(t35974,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t862,t29]) ).
cnf(t1177,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t35974]) ).
cnf(t850,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t847,t133]) ).
cnf(t934,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t850]) ).
cnf(t1178,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t1177,t934]) ).
cnf(t1186,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t1178]) ).
cnf(t36247,plain,
composition(converse(sFlat0),sFlat3) = zero,
inference(step,[status(thm)],[t6711,t1186]) ).
cnf(t6718,plain,
composition(converse(sFlat0),sFlat3) = zero,
inference(orient,[status(thm)],[t36247]) ).
cnf(t6720,plain,
composition(join(converse(sFlat0),X1),sFlat3) = join(zero,composition(X1,sFlat3)),
inference(cp,[status(thm)],[t174,t6718]) ).
cnf(t36286,plain,
composition(join(converse(sFlat0),X1),sFlat3) = composition(X1,sFlat3),
inference(step,[status(thm)],[t6720,t847]) ).
cnf(t7089,plain,
composition(join(converse(sFlat0),X1),sFlat3) = composition(X1,sFlat3),
inference(orient,[status(thm)],[t36286]) ).
cnf(t7090,plain,
composition(converse(X1),sFlat3) = composition(converse(join(sFlat0,X1)),sFlat3),
inference(cp,[status(thm)],[t7089,t177]) ).
cnf(t11051,plain,
composition(converse(join(sFlat0,X1)),sFlat3) = composition(converse(X1),sFlat3),
inference(orient,[status(thm)],[t7090]) ).
cnf(t291,plain,
X1 = join(complement(join(X2,complement(X1))),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t288,t133]) ).
cnf(t28074,plain,
join(complement(join(X1,complement(X2))),complement(join(complement(X2),complement(X1)))) = X2,
inference(orient,[status(thm)],[t291]) ).
cnf(t292,plain,
sFlat5 = join(complement(join(sFlat6,X1)),complement(join(complement(sFlat5),complement(X1)))),
inference(cp,[status(thm)],[t288,t227]) ).
cnf(t37069,plain,
sFlat5 = join(complement(join(sFlat6,X1)),complement(join(sFlat6,complement(X1)))),
inference(step,[status(thm)],[t292,t227]) ).
cnf(t29816,plain,
join(complement(join(sFlat6,X1)),complement(join(sFlat6,complement(X1)))) = sFlat5,
inference(orient,[status(thm)],[t37069]) ).
cnf(t29864,plain,
join(sFlat6,X1) = join(complement(join(join(sFlat6,complement(X1)),complement(join(sFlat6,X1)))),complement(sFlat5)),
inference(cp,[status(thm)],[t28074,t29816]) ).
cnf(t37076,plain,
join(sFlat6,X1) = join(complement(sFlat5),complement(join(join(sFlat6,complement(X1)),complement(join(sFlat6,X1))))),
inference(step,[status(thm)],[t29864,t133]) ).
cnf(t37077,plain,
join(sFlat6,X1) = join(sFlat6,complement(join(join(sFlat6,complement(X1)),complement(join(sFlat6,X1))))),
inference(step,[status(thm)],[t37076,t227]) ).
cnf(t37078,plain,
join(sFlat6,X1) = join(sFlat6,complement(join(sFlat6,join(complement(X1),complement(join(sFlat6,X1)))))),
inference(step,[status(thm)],[t37077,t143]) ).
cnf(t3064,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(cp,[status(thm)],[t3060,t133]) ).
cnf(t4947,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t3064]) ).
cnf(t4970,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t4947,t1015]) ).
cnf(t15315,plain,
join(complement(X1),complement(join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t4970]) ).
cnf(t37079,plain,
join(sFlat6,X1) = join(sFlat6,complement(join(sFlat6,complement(X1)))),
inference(step,[status(thm)],[t37078,t15315]) ).
cnf(t29913,plain,
join(sFlat6,complement(join(sFlat6,complement(X1)))) = join(sFlat6,X1),
inference(orient,[status(thm)],[t37079]) ).
cnf(t29918,plain,
join(sFlat6,complement(X1)) = join(sFlat6,complement(join(sFlat6,X1))),
inference(cp,[status(thm)],[t29913,t1015]) ).
cnf(t30076,plain,
join(sFlat6,complement(join(sFlat6,X1))) = join(sFlat6,complement(X1)),
inference(orient,[status(thm)],[t29918]) ).
cnf(t297,plain,
sk1 = join(complement(join(sFlat0,X1)),complement(join(complement(sk1),complement(X1)))),
inference(cp,[status(thm)],[t288,t92]) ).
cnf(t37358,plain,
sk1 = join(complement(join(sFlat0,X1)),complement(join(sFlat0,complement(X1)))),
inference(step,[status(thm)],[t297,t92]) ).
cnf(t34598,plain,
join(complement(join(sFlat0,X1)),complement(join(sFlat0,complement(X1)))) = sk1,
inference(orient,[status(thm)],[t37358]) ).
cnf(t34626,plain,
sk1 = join(complement(sFlat5),complement(join(sFlat0,complement(sFlat4)))),
inference(cp,[status(thm)],[t34598,t172]) ).
cnf(t37377,plain,
sk1 = join(sFlat6,complement(join(sFlat0,complement(sFlat4)))),
inference(step,[status(thm)],[t34626,t227]) ).
cnf(t760,plain,
one = join(zero,complement(sFlat4)),
inference(cp,[status(thm)],[t757,t120]) ).
cnf(t768,plain,
join(zero,complement(sFlat4)) = one,
inference(orient,[status(thm)],[t760]) ).
cnf(t35858,plain,
complement(sFlat4) = one,
inference(step,[status(thm)],[t768,t847]) ).
cnf(t865,plain,
complement(sFlat4) = one,
inference(rw,[status(thm)],[t35858]) ).
cnf(t900,plain,
complement(sFlat4) = one,
inference(orient,[status(thm)],[t865]) ).
cnf(t37378,plain,
sk1 = join(sFlat6,complement(join(sFlat0,one))),
inference(step,[status(thm)],[t37377,t900]) ).
cnf(t35022,plain,
join(sFlat6,complement(join(sFlat0,one))) = sk1,
inference(orient,[status(thm)],[t37378]) ).
cnf(t35028,plain,
join(sFlat6,complement(complement(join(sFlat0,one)))) = join(sFlat6,complement(sk1)),
inference(cp,[status(thm)],[t30076,t35022]) ).
cnf(t37379,plain,
join(sFlat6,join(sFlat0,one)) = join(sFlat6,complement(sk1)),
inference(step,[status(thm)],[t35028,t1015]) ).
cnf(t147,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t143,t133]) ).
cnf(t36043,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t147,t143]) ).
cnf(t2119,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t36043]) ).
cnf(t3076,plain,
one = join(one,complement(join(sFlat4,X1))),
inference(cp,[status(thm)],[t3060,t120]) ).
cnf(t3187,plain,
join(one,complement(join(sFlat4,X1))) = one,
inference(orient,[status(thm)],[t3076]) ).
cnf(t173,plain,
join(sFlat0,join(sFlat4,X1)) = join(sFlat5,X1),
inference(cp,[status(thm)],[t143,t172]) ).
cnf(t248,plain,
join(sFlat0,join(sFlat4,X1)) = join(sFlat5,X1),
inference(orient,[status(thm)],[t173]) ).
cnf(t251,plain,
join(sFlat5,X1) = join(sFlat0,join(X1,sFlat4)),
inference(cp,[status(thm)],[t248,t133]) ).
cnf(t329,plain,
join(sFlat0,join(X1,sFlat4)) = join(sFlat5,X1),
inference(orient,[status(thm)],[t251]) ).
cnf(t656,plain,
complement(one) = join(sFlat4,complement(one)),
inference(cp,[status(thm)],[t652,t120]) ).
cnf(t35788,plain,
sFlat4 = join(sFlat4,complement(one)),
inference(step,[status(thm)],[t656,t120]) ).
cnf(t35789,plain,
sFlat4 = join(sFlat4,sFlat4),
inference(step,[status(thm)],[t35788,t120]) ).
cnf(t683,plain,
join(sFlat4,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t35789]) ).
cnf(t685,plain,
join(sFlat5,sFlat4) = join(sFlat0,sFlat4),
inference(cp,[status(thm)],[t329,t683]) ).
cnf(t35804,plain,
join(sFlat4,sFlat5) = join(sFlat0,sFlat4),
inference(step,[status(thm)],[t685,t133]) ).
cnf(t35805,plain,
join(sFlat4,sFlat5) = sFlat5,
inference(step,[status(thm)],[t35804,t172]) ).
cnf(t709,plain,
join(sFlat4,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t35805]) ).
cnf(t3192,plain,
one = join(one,complement(sFlat5)),
inference(cp,[status(thm)],[t3187,t709]) ).
cnf(t36111,plain,
one = join(one,sFlat6),
inference(step,[status(thm)],[t3192,t227]) ).
cnf(t36112,plain,
one = join(sFlat6,one),
inference(step,[status(thm)],[t36111,t133]) ).
cnf(t3202,plain,
join(sFlat6,one) = one,
inference(orient,[status(thm)],[t36112]) ).
cnf(t3208,plain,
join(sFlat6,join(X1,one)) = join(X1,one),
inference(cp,[status(thm)],[t2119,t3202]) ).
cnf(t3246,plain,
join(sFlat6,join(X1,one)) = join(X1,one),
inference(orient,[status(thm)],[t3208]) ).
cnf(t37380,plain,
join(sFlat0,one) = join(sFlat6,complement(sk1)),
inference(step,[status(thm)],[t37379,t3246]) ).
cnf(t37381,plain,
join(sFlat0,one) = join(sFlat6,sFlat0),
inference(step,[status(thm)],[t37380,t92]) ).
cnf(t37382,plain,
join(sFlat0,one) = join(sFlat0,sFlat6),
inference(step,[status(thm)],[t37381,t133]) ).
cnf(t35039,plain,
join(sFlat0,one) = join(sFlat0,sFlat6),
inference(orient,[status(thm)],[t37382]) ).
cnf(t35053,plain,
composition(converse(one),sFlat3) = composition(converse(join(sFlat0,sFlat6)),sFlat3),
inference(cp,[status(thm)],[t11051,t35039]) ).
cnf(t37650,plain,
composition(one,sFlat3) = composition(converse(join(sFlat0,sFlat6)),sFlat3),
inference(step,[status(thm)],[t35053,t434]) ).
cnf(t37651,plain,
sFlat3 = composition(converse(join(sFlat0,sFlat6)),sFlat3),
inference(step,[status(thm)],[t37650,t446]) ).
cnf(t37652,plain,
sFlat3 = composition(converse(sFlat6),sFlat3),
inference(step,[status(thm)],[t37651,t11051]) ).
cnf(t758,plain,
sFlat5 = join(zero,complement(sFlat6)),
inference(cp,[status(thm)],[t757,t227]) ).
cnf(t764,plain,
join(zero,complement(sFlat6)) = sFlat5,
inference(orient,[status(thm)],[t758]) ).
cnf(t35860,plain,
complement(sFlat6) = sFlat5,
inference(step,[status(thm)],[t764,t847]) ).
cnf(t867,plain,
complement(sFlat6) = sFlat5,
inference(rw,[status(thm)],[t35860]) ).
cnf(t922,plain,
complement(sFlat6) = sFlat5,
inference(orient,[status(thm)],[t867]) ).
cnf(t923,plain,
complement(sFlat6) = join(sFlat5,complement(sFlat6)),
inference(cp,[status(thm)],[t652,t922]) ).
cnf(t35887,plain,
sFlat5 = join(sFlat5,complement(sFlat6)),
inference(step,[status(thm)],[t923,t922]) ).
cnf(t35888,plain,
sFlat5 = join(sFlat5,sFlat5),
inference(step,[status(thm)],[t35887,t922]) ).
cnf(t711,plain,
join(sFlat5,sFlat5) = join(sFlat0,sFlat5),
inference(cp,[status(thm)],[t248,t709]) ).
cnf(t753,plain,
join(sFlat5,sFlat5) = join(sFlat0,sFlat5),
inference(orient,[status(thm)],[t711]) ).
cnf(t35889,plain,
sFlat5 = join(sFlat0,sFlat5),
inference(step,[status(thm)],[t35888,t753]) ).
cnf(t1062,plain,
join(sFlat0,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t35889]) ).
cnf(t3334,plain,
sk1 = join(sk1,complement(sFlat5)),
inference(cp,[status(thm)],[t3329,t1062]) ).
cnf(t36118,plain,
sk1 = join(sk1,sFlat6),
inference(step,[status(thm)],[t3334,t227]) ).
cnf(t36119,plain,
sk1 = join(sFlat6,sk1),
inference(step,[status(thm)],[t36118,t133]) ).
cnf(t3351,plain,
join(sFlat6,sk1) = sk1,
inference(orient,[status(thm)],[t36119]) ).
cnf(t3354,plain,
join(sk1,composition(sFlat6,top)) = composition(sk1,top),
inference(cp,[status(thm)],[t534,t3351]) ).
cnf(t36122,plain,
join(sk1,composition(sFlat6,top)) = sk1,
inference(step,[status(thm)],[t3354,t202]) ).
cnf(t3368,plain,
join(sk1,composition(sFlat6,top)) = sk1,
inference(orient,[status(thm)],[t36122]) ).
cnf(t6612,plain,
composition(converse(composition(sFlat6,top)),sFlat0) = composition(converse(sk1),sFlat0),
inference(cp,[status(thm)],[t6598,t3368]) ).
cnf(t36237,plain,
composition(composition(top,converse(sFlat6)),sFlat0) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t6612,t1207]) ).
cnf(t36238,plain,
composition(top,composition(converse(sFlat6),sFlat0)) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t36237,t182]) ).
cnf(t36239,plain,
composition(top,composition(converse(sFlat6),sFlat0)) = zero,
inference(step,[status(thm)],[t36238,t1780]) ).
cnf(t6652,plain,
composition(top,composition(converse(sFlat6),sFlat0)) = zero,
inference(orient,[status(thm)],[t36239]) ).
cnf(t6656,plain,
composition(join(top,X1),composition(converse(sFlat6),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat6),sFlat0))),
inference(cp,[status(thm)],[t174,t6652]) ).
cnf(t36256,plain,
composition(top,composition(converse(sFlat6),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat6),sFlat0))),
inference(step,[status(thm)],[t6656,t1118]) ).
cnf(t36257,plain,
zero = join(zero,composition(X1,composition(converse(sFlat6),sFlat0))),
inference(step,[status(thm)],[t36256,t6652]) ).
cnf(t36258,plain,
zero = composition(X1,composition(converse(sFlat6),sFlat0)),
inference(step,[status(thm)],[t36257,t847]) ).
cnf(t6768,plain,
composition(X1,composition(converse(sFlat6),sFlat0)) = zero,
inference(orient,[status(thm)],[t36258]) ).
cnf(t6769,plain,
zero = composition(converse(sFlat6),sFlat0),
inference(cp,[status(thm)],[t6768,t446]) ).
cnf(t6782,plain,
composition(converse(sFlat6),sFlat0) = zero,
inference(orient,[status(thm)],[t6769]) ).
cnf(t6788,plain,
composition(converse(sFlat0),sFlat6) = converse(zero),
inference(cp,[status(thm)],[t410,t6782]) ).
cnf(t36259,plain,
composition(converse(sFlat0),sFlat6) = zero,
inference(step,[status(thm)],[t6788,t1186]) ).
cnf(t6795,plain,
composition(converse(sFlat0),sFlat6) = zero,
inference(orient,[status(thm)],[t36259]) ).
cnf(t6797,plain,
composition(join(converse(sFlat0),X1),sFlat6) = join(zero,composition(X1,sFlat6)),
inference(cp,[status(thm)],[t174,t6795]) ).
cnf(t36295,plain,
composition(join(converse(sFlat0),X1),sFlat6) = composition(X1,sFlat6),
inference(step,[status(thm)],[t6797,t847]) ).
cnf(t7327,plain,
composition(join(converse(sFlat0),X1),sFlat6) = composition(X1,sFlat6),
inference(orient,[status(thm)],[t36295]) ).
cnf(t7328,plain,
composition(converse(X1),sFlat6) = composition(converse(join(sFlat0,X1)),sFlat6),
inference(cp,[status(thm)],[t7327,t177]) ).
cnf(t11456,plain,
composition(converse(join(sFlat0,X1)),sFlat6) = composition(converse(X1),sFlat6),
inference(orient,[status(thm)],[t7328]) ).
cnf(t35052,plain,
composition(converse(one),sFlat6) = composition(converse(join(sFlat0,sFlat6)),sFlat6),
inference(cp,[status(thm)],[t11456,t35039]) ).
cnf(t37417,plain,
composition(one,sFlat6) = composition(converse(join(sFlat0,sFlat6)),sFlat6),
inference(step,[status(thm)],[t35052,t434]) ).
cnf(t37418,plain,
sFlat6 = composition(converse(join(sFlat0,sFlat6)),sFlat6),
inference(step,[status(thm)],[t37417,t446]) ).
cnf(t37419,plain,
sFlat6 = composition(converse(sFlat6),sFlat6),
inference(step,[status(thm)],[t37418,t11456]) ).
cnf(t35167,plain,
composition(converse(sFlat6),sFlat6) = sFlat6,
inference(orient,[status(thm)],[t37419]) ).
cnf(t35180,plain,
composition(converse(sFlat6),sFlat6) = converse(sFlat6),
inference(cp,[status(thm)],[t410,t35167]) ).
cnf(t37420,plain,
sFlat6 = converse(sFlat6),
inference(step,[status(thm)],[t35180,t35167]) ).
cnf(t35205,plain,
converse(sFlat6) = sFlat6,
inference(orient,[status(thm)],[t37420]) ).
cnf(t37653,plain,
sFlat3 = composition(sFlat6,sFlat3),
inference(step,[status(thm)],[t37652,t35205]) ).
cnf(t11489,plain,
composition(converse(sFlat6),join(sFlat0,X1)) = converse(composition(converse(X1),sFlat6)),
inference(cp,[status(thm)],[t410,t11456]) ).
cnf(t36572,plain,
composition(converse(sFlat6),join(sFlat0,X1)) = composition(converse(sFlat6),X1),
inference(step,[status(thm)],[t11489,t410]) ).
cnf(t13911,plain,
composition(converse(sFlat6),join(sFlat0,X1)) = composition(converse(sFlat6),X1),
inference(orient,[status(thm)],[t36572]) ).
cnf(t293,plain,
sFlat2 = join(complement(join(sFlat3,X1)),complement(join(complement(sFlat2),complement(X1)))),
inference(cp,[status(thm)],[t288,t220]) ).
cnf(t37160,plain,
sFlat2 = join(complement(join(sFlat3,X1)),complement(join(sFlat3,complement(X1)))),
inference(step,[status(thm)],[t293,t220]) ).
cnf(t31436,plain,
join(complement(join(sFlat3,X1)),complement(join(sFlat3,complement(X1)))) = sFlat2,
inference(orient,[status(thm)],[t37160]) ).
cnf(t31488,plain,
join(sFlat3,X1) = join(complement(join(join(sFlat3,complement(X1)),complement(join(sFlat3,X1)))),complement(sFlat2)),
inference(cp,[status(thm)],[t28074,t31436]) ).
cnf(t37186,plain,
join(sFlat3,X1) = join(complement(sFlat2),complement(join(join(sFlat3,complement(X1)),complement(join(sFlat3,X1))))),
inference(step,[status(thm)],[t31488,t133]) ).
cnf(t37187,plain,
join(sFlat3,X1) = join(sFlat3,complement(join(join(sFlat3,complement(X1)),complement(join(sFlat3,X1))))),
inference(step,[status(thm)],[t37186,t220]) ).
cnf(t37188,plain,
join(sFlat3,X1) = join(sFlat3,complement(join(sFlat3,join(complement(X1),complement(join(sFlat3,X1)))))),
inference(step,[status(thm)],[t37187,t143]) ).
cnf(t37189,plain,
join(sFlat3,X1) = join(sFlat3,complement(join(sFlat3,complement(X1)))),
inference(step,[status(thm)],[t37188,t15315]) ).
cnf(t31606,plain,
join(sFlat3,complement(join(sFlat3,complement(X1)))) = join(sFlat3,X1),
inference(orient,[status(thm)],[t37189]) ).
cnf(t31611,plain,
join(sFlat3,complement(X1)) = join(sFlat3,complement(join(sFlat3,X1))),
inference(cp,[status(thm)],[t31606,t1015]) ).
cnf(t31757,plain,
join(sFlat3,complement(join(sFlat3,X1))) = join(sFlat3,complement(X1)),
inference(orient,[status(thm)],[t31611]) ).
cnf(t34625,plain,
sk1 = join(complement(sFlat2),complement(join(sFlat0,complement(sFlat1)))),
inference(cp,[status(thm)],[t34598,t169]) ).
cnf(t37361,plain,
sk1 = join(sFlat3,complement(join(sFlat0,complement(sFlat1)))),
inference(step,[status(thm)],[t34625,t220]) ).
cnf(t761,plain,
sk2 = join(zero,complement(sFlat1)),
inference(cp,[status(thm)],[t757,t107]) ).
cnf(t770,plain,
join(zero,complement(sFlat1)) = sk2,
inference(orient,[status(thm)],[t761]) ).
cnf(t35857,plain,
complement(sFlat1) = sk2,
inference(step,[status(thm)],[t770,t847]) ).
cnf(t864,plain,
complement(sFlat1) = sk2,
inference(rw,[status(thm)],[t35857]) ).
cnf(t890,plain,
complement(sFlat1) = sk2,
inference(orient,[status(thm)],[t864]) ).
cnf(t37362,plain,
sk1 = join(sFlat3,complement(join(sFlat0,sk2))),
inference(step,[status(thm)],[t37361,t890]) ).
cnf(t34679,plain,
join(sFlat3,complement(join(sFlat0,sk2))) = sk1,
inference(orient,[status(thm)],[t37362]) ).
cnf(t34682,plain,
join(sFlat3,complement(complement(join(sFlat0,sk2)))) = join(sFlat3,complement(sk1)),
inference(cp,[status(thm)],[t31757,t34679]) ).
cnf(t37363,plain,
join(sFlat3,join(sFlat0,sk2)) = join(sFlat3,complement(sk1)),
inference(step,[status(thm)],[t34682,t1015]) ).
cnf(t3077,plain,
sk2 = join(sk2,complement(join(sFlat1,X1))),
inference(cp,[status(thm)],[t3060,t107]) ).
cnf(t3286,plain,
join(sk2,complement(join(sFlat1,X1))) = sk2,
inference(orient,[status(thm)],[t3077]) ).
cnf(t3289,plain,
sk2 = join(sk2,complement(sFlat2)),
inference(cp,[status(thm)],[t3286,t713]) ).
cnf(t36116,plain,
sk2 = join(sk2,sFlat3),
inference(step,[status(thm)],[t3289,t220]) ).
cnf(t36117,plain,
sk2 = join(sFlat3,sk2),
inference(step,[status(thm)],[t36116,t133]) ).
cnf(t3298,plain,
join(sFlat3,sk2) = sk2,
inference(orient,[status(thm)],[t36117]) ).
cnf(t3302,plain,
join(sFlat3,join(X1,sk2)) = join(X1,sk2),
inference(cp,[status(thm)],[t2119,t3298]) ).
cnf(t3319,plain,
join(sFlat3,join(X1,sk2)) = join(X1,sk2),
inference(orient,[status(thm)],[t3302]) ).
cnf(t37364,plain,
join(sFlat0,sk2) = join(sFlat3,complement(sk1)),
inference(step,[status(thm)],[t37363,t3319]) ).
cnf(t37365,plain,
join(sFlat0,sk2) = join(sFlat3,sFlat0),
inference(step,[status(thm)],[t37364,t92]) ).
cnf(t37366,plain,
join(sFlat0,sk2) = join(sFlat0,sFlat3),
inference(step,[status(thm)],[t37365,t133]) ).
cnf(t34695,plain,
join(sFlat0,sk2) = join(sFlat0,sFlat3),
inference(orient,[status(thm)],[t37366]) ).
cnf(t34698,plain,
composition(converse(sFlat6),sk2) = composition(converse(sFlat6),join(sFlat0,sFlat3)),
inference(cp,[status(thm)],[t13911,t34695]) ).
cnf(t37370,plain,
composition(converse(sFlat6),sk2) = composition(converse(sFlat6),sFlat3),
inference(step,[status(thm)],[t34698,t13911]) ).
cnf(t34798,plain,
composition(converse(sFlat6),sk2) = composition(converse(sFlat6),sFlat3),
inference(orient,[status(thm)],[t37370]) ).
cnf(t37457,plain,
composition(sFlat6,sk2) = composition(converse(sFlat6),sFlat3),
inference(step,[status(thm)],[t34798,t35205]) ).
cnf(t37458,plain,
sFlat7 = composition(converse(sFlat6),sFlat3),
inference(step,[status(thm)],[t37457,t235]) ).
cnf(t37459,plain,
sFlat7 = composition(sFlat6,sFlat3),
inference(step,[status(thm)],[t37458,t35205]) ).
cnf(t35275,plain,
sFlat7 = composition(sFlat6,sFlat3),
inference(rw,[status(thm)],[t37459]) ).
cnf(t35395,plain,
composition(sFlat6,sFlat3) = sFlat7,
inference(orient,[status(thm)],[t35275]) ).
cnf(t37654,plain,
sFlat3 = sFlat7,
inference(step,[status(thm)],[t37653,t35395]) ).
cnf(t35674,plain,
sFlat7 = sFlat3,
inference(orient,[status(thm)],[t37654]) ).
cnf(t37655,plain,
composition(sFlat6,sk2) = sFlat3,
inference(step,[status(thm)],[t235,t35674]) ).
cnf(t35675,plain,
composition(sFlat6,sk2) = sFlat3,
inference(orient,[status(thm)],[t37655]) ).
cnf(u4,negated_conjecture,
join(meet(sk1,sk2),composition(meet(sk1,one),sk2)) != composition(meet(sk1,one),sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(definition_unfolding,[status(thm)],[u4,d0]) ).
cnf(g0_0,plain,
join(complement(join(complement(sk2),complement(sk1))),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[goal_0,t133]) ).
cnf(g0_1,plain,
join(complement(join(sFlat1,complement(sk1))),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_0,t107]) ).
cnf(g0_2,plain,
join(complement(join(sFlat1,sFlat0)),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_1,t92]) ).
cnf(g0_3,plain,
join(complement(join(sFlat0,sFlat1)),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_2,t133]) ).
cnf(g0_4,plain,
join(complement(sFlat2),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_3,t169]) ).
cnf(g0_5,plain,
join(sFlat3,composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_4,t220]) ).
cnf(g0_6,plain,
join(sFlat3,composition(complement(join(sFlat0,complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_5,t92]) ).
cnf(g0_7,plain,
join(sFlat3,composition(complement(join(sFlat0,sFlat4)),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_6,t120]) ).
cnf(g0_8,plain,
join(sFlat3,composition(complement(sFlat5),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_7,t172]) ).
cnf(g0_9,plain,
join(sFlat3,composition(sFlat6,sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_8,t227]) ).
cnf(g0_10,plain,
join(sFlat3,sFlat3) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_9,t35675]) ).
cnf(g0_11,plain,
sFlat3 != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_10,t1094]) ).
cnf(g0_12,plain,
sFlat3 != composition(complement(join(sFlat0,complement(one))),sk2),
inference(rw,[status(thm)],[g0_11,t92]) ).
cnf(g0_13,plain,
sFlat3 != composition(complement(join(sFlat0,sFlat4)),sk2),
inference(rw,[status(thm)],[g0_12,t120]) ).
cnf(g0_14,plain,
sFlat3 != composition(complement(sFlat5),sk2),
inference(rw,[status(thm)],[g0_13,t172]) ).
cnf(g0_15,plain,
sFlat3 != composition(sFlat6,sk2),
inference(rw,[status(thm)],[g0_14,t227]) ).
cnf(g0_16,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_15,t35675]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL022-2 : 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.41 % Computer : n019.cluster.edu
% 0.10/0.41 % Model : x86_64 x86_64
% 0.10/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.41 % Memory : 8046.5625MB
% 0.10/0.41 % OS : Linux 6.8.0-71-generic
% 0.10/0.41 % CPULimit : 300
% 0.10/0.41 % WCLimit : 300
% 0.10/0.41 % DateTime : Thu Sep 24 07:18:34 UTC 2026
% 0.10/0.42 % CPUTime :
% 0.10/0.42 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 62.93/8.73 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 62.93/8.73 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------