%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL016-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n008.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:44 PM UTC 2026
% Result : Unsatisfiable 27.87s 4.73s
% Output : CNFRefutation 27.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 29
% Syntax : Number of clauses : 475 ( 475 unt; 0 nHn; 273 RR)
% Number of literals : 475 ( 474 equ; 20 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 9 ( 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 : 263 ( 27 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t12,axiom,
sF0 = complement(sk2),
introduced(definition) ).
cnf(t28,plain,
complement(sk2) = sF0,
inference(orient,[status(thm)],[t12]) ).
cnf(t11,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t3,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t41,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t42204,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t11,t41]) ).
cnf(t197,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t42204]) ).
cnf(t10,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t42203,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t10,t41]) ).
cnf(t141,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t42203]) ).
cnf(t5,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t63,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t65,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t63,t31]) ).
cnf(t108,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t65]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t109,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t108,t30]) ).
cnf(t42200,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t109,t31]) ).
cnf(t112,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t42200]) ).
cnf(t113,plain,
one = converse(one),
inference(cp,[status(thm)],[t112,t30]) ).
cnf(t116,plain,
converse(one) = one,
inference(orient,[status(thm)],[t113]) ).
cnf(t158,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t141,t116]) ).
cnf(t42201,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t112,t116]) ).
cnf(t117,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t42201]) ).
cnf(t121,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t117]) ).
cnf(t42212,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t158,t121]) ).
cnf(t42213,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t42212,t121]) ).
cnf(t284,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t42213]) ).
cnf(t293,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t197,t284]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t35,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t42392,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t293,t35]) ).
cnf(t42393,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t42392,t41]) ).
cnf(u0,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t42196,plain,
complement(top) = zero,
inference(step,[status(thm)],[t4,t35]) ).
cnf(t57,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t42196]) ).
cnf(t42394,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t42393,t57]) ).
cnf(t1137,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t42394]) ).
cnf(t8,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t75,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t290,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t284,t57]) ).
cnf(t42228,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t290,t57]) ).
cnf(t42229,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t42228,t57]) ).
cnf(t314,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t42229]) ).
cnf(t315,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t75,t314]) ).
cnf(t1413,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t315]) ).
cnf(t1417,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t1413,t1137]) ).
cnf(t42404,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t1417,t1137]) ).
cnf(t1421,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t42404]) ).
cnf(t42406,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t1137,t1421]) ).
cnf(t1423,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t42406]) ).
cnf(t1530,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1423]) ).
cnf(t13,axiom,
sF1 = complement(sk3),
introduced(definition) ).
cnf(t29,plain,
complement(sk3) = sF1,
inference(orient,[status(thm)],[t13]) ).
cnf(t1531,plain,
sk3 = complement(sF1),
inference(cp,[status(thm)],[t1530,t29]) ).
cnf(t14,axiom,
sF2 = complement(complement(sk3)),
introduced(definition) ).
cnf(t42191,plain,
sF2 = complement(sF1),
inference(step,[status(thm)],[t14,t29]) ).
cnf(t32,plain,
complement(sF1) = sF2,
inference(orient,[status(thm)],[t42191]) ).
cnf(t42416,plain,
sk3 = sF2,
inference(step,[status(thm)],[t1531,t32]) ).
cnf(t1538,plain,
sk3 = sF2,
inference(orient,[status(thm)],[t42416]) ).
cnf(t15,axiom,
sF3 = join(complement(sk2),complement(complement(sk3))),
introduced(definition) ).
cnf(t42207,plain,
sF3 = join(sF0,complement(complement(sk3))),
inference(step,[status(thm)],[t15,t28]) ).
cnf(t42208,plain,
sF3 = join(sF0,complement(sF1)),
inference(step,[status(thm)],[t42207,t29]) ).
cnf(t42209,plain,
sF3 = join(sF0,sF2),
inference(step,[status(thm)],[t42208,t32]) ).
cnf(t244,plain,
join(sF0,sF2) = sF3,
inference(orient,[status(thm)],[t42209]) ).
cnf(t16,axiom,
sF4 = complement(join(complement(sk2),complement(complement(sk3)))),
introduced(definition) ).
cnf(t42214,plain,
sF4 = complement(join(sF0,complement(complement(sk3)))),
inference(step,[status(thm)],[t16,t28]) ).
cnf(t42215,plain,
sF4 = complement(join(sF0,complement(sF1))),
inference(step,[status(thm)],[t42214,t29]) ).
cnf(t42216,plain,
sF4 = complement(join(sF0,sF2)),
inference(step,[status(thm)],[t42215,t32]) ).
cnf(t42217,plain,
sF4 = complement(sF3),
inference(step,[status(thm)],[t42216,t244]) ).
cnf(t295,plain,
complement(sF3) = sF4,
inference(orient,[status(thm)],[t42217]) ).
cnf(t17,axiom,
sF5 = composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))),
introduced(definition) ).
cnf(t42236,plain,
sF5 = composition(sk1,complement(join(sF0,complement(complement(sk3))))),
inference(step,[status(thm)],[t17,t28]) ).
cnf(t42237,plain,
sF5 = composition(sk1,complement(join(sF0,complement(sF1)))),
inference(step,[status(thm)],[t42236,t29]) ).
cnf(t42238,plain,
sF5 = composition(sk1,complement(join(sF0,sF2))),
inference(step,[status(thm)],[t42237,t32]) ).
cnf(t42239,plain,
sF5 = composition(sk1,complement(sF3)),
inference(step,[status(thm)],[t42238,t244]) ).
cnf(t42240,plain,
sF5 = composition(sk1,sF4),
inference(step,[status(thm)],[t42239,t295]) ).
cnf(t328,plain,
composition(sk1,sF4) = sF5,
inference(orient,[status(thm)],[t42240]) ).
cnf(t18,axiom,
sF6 = complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),
introduced(definition) ).
cnf(t42261,plain,
sF6 = complement(composition(sk1,complement(join(sF0,complement(complement(sk3)))))),
inference(step,[status(thm)],[t18,t28]) ).
cnf(t42262,plain,
sF6 = complement(composition(sk1,complement(join(sF0,complement(sF1))))),
inference(step,[status(thm)],[t42261,t29]) ).
cnf(t42263,plain,
sF6 = complement(composition(sk1,complement(join(sF0,sF2)))),
inference(step,[status(thm)],[t42262,t32]) ).
cnf(t42264,plain,
sF6 = complement(composition(sk1,complement(sF3))),
inference(step,[status(thm)],[t42263,t244]) ).
cnf(t42265,plain,
sF6 = complement(composition(sk1,sF4)),
inference(step,[status(thm)],[t42264,t295]) ).
cnf(t42266,plain,
sF6 = complement(sF5),
inference(step,[status(thm)],[t42265,t328]) ).
cnf(t362,plain,
complement(sF5) = sF6,
inference(orient,[status(thm)],[t42266]) ).
cnf(t19,axiom,
sF7 = composition(sk1,sk3),
introduced(definition) ).
cnf(t33,plain,
composition(sk1,sk3) = sF7,
inference(orient,[status(thm)],[t19]) ).
cnf(t42417,plain,
composition(sk1,sF2) = sF7,
inference(step,[status(thm)],[t33,t1538]) ).
cnf(t1540,plain,
composition(sk1,sF2) = sF7,
inference(rw,[status(thm)],[t42417]) ).
cnf(t1735,plain,
composition(sk1,sF2) = sF7,
inference(orient,[status(thm)],[t1540]) ).
cnf(t22,axiom,
sF10 = join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))),
introduced(definition) ).
cnf(t42271,plain,
sF10 = join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
inference(step,[status(thm)],[t22,t41]) ).
cnf(t42272,plain,
sF10 = join(complement(complement(sF7)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
inference(step,[status(thm)],[t42271,t33]) ).
cnf(t20,axiom,
sF8 = complement(composition(sk1,sk3)),
introduced(definition) ).
cnf(t42194,plain,
sF8 = complement(sF7),
inference(step,[status(thm)],[t20,t33]) ).
cnf(t51,plain,
complement(sF7) = sF8,
inference(orient,[status(thm)],[t42194]) ).
cnf(t42273,plain,
sF10 = join(complement(sF8),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
inference(step,[status(thm)],[t42272,t51]) ).
cnf(t21,axiom,
sF9 = complement(complement(composition(sk1,sk3))),
introduced(definition) ).
cnf(t42198,plain,
sF9 = complement(complement(sF7)),
inference(step,[status(thm)],[t21,t33]) ).
cnf(t42199,plain,
sF9 = complement(sF8),
inference(step,[status(thm)],[t42198,t51]) ).
cnf(t87,plain,
complement(sF8) = sF9,
inference(orient,[status(thm)],[t42199]) ).
cnf(t42274,plain,
sF10 = join(sF9,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
inference(step,[status(thm)],[t42273,t87]) ).
cnf(t42275,plain,
sF10 = join(sF9,complement(composition(sk1,complement(join(sF0,complement(complement(sk3))))))),
inference(step,[status(thm)],[t42274,t28]) ).
cnf(t42276,plain,
sF10 = join(sF9,complement(composition(sk1,complement(join(sF0,complement(sF1)))))),
inference(step,[status(thm)],[t42275,t29]) ).
cnf(t42277,plain,
sF10 = join(sF9,complement(composition(sk1,complement(join(sF0,sF2))))),
inference(step,[status(thm)],[t42276,t32]) ).
cnf(t42278,plain,
sF10 = join(sF9,complement(composition(sk1,complement(sF3)))),
inference(step,[status(thm)],[t42277,t244]) ).
cnf(t42279,plain,
sF10 = join(sF9,complement(composition(sk1,sF4))),
inference(step,[status(thm)],[t42278,t295]) ).
cnf(t42280,plain,
sF10 = join(sF9,complement(sF5)),
inference(step,[status(thm)],[t42279,t328]) ).
cnf(t42281,plain,
sF10 = join(sF9,sF6),
inference(step,[status(thm)],[t42280,t362]) ).
cnf(t42282,plain,
sF10 = join(sF6,sF9),
inference(step,[status(thm)],[t42281,t41]) ).
cnf(t388,plain,
join(sF6,sF9) = sF10,
inference(orient,[status(thm)],[t42282]) ).
cnf(t1532,plain,
sF7 = complement(sF8),
inference(cp,[status(thm)],[t1530,t51]) ).
cnf(t42421,plain,
sF7 = sF9,
inference(step,[status(thm)],[t1532,t87]) ).
cnf(t1581,plain,
sF9 = sF7,
inference(orient,[status(thm)],[t42421]) ).
cnf(t42426,plain,
join(sF6,sF7) = sF10,
inference(step,[status(thm)],[t388,t1581]) ).
cnf(t1587,plain,
join(sF6,sF7) = sF10,
inference(rw,[status(thm)],[t42426]) ).
cnf(t1762,plain,
join(sF6,sF7) = sF10,
inference(orient,[status(thm)],[t1587]) ).
cnf(t24,axiom,
sF12 = composition(sk1,sk2),
introduced(definition) ).
cnf(t34,plain,
composition(sk1,sk2) = sF12,
inference(orient,[status(thm)],[t24]) ).
cnf(t25,axiom,
sF13 = complement(composition(sk1,sk2)),
introduced(definition) ).
cnf(t42195,plain,
sF13 = complement(sF12),
inference(step,[status(thm)],[t25,t34]) ).
cnf(t55,plain,
complement(sF12) = sF13,
inference(orient,[status(thm)],[t42195]) ).
cnf(t26,axiom,
sF14 = join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))),
introduced(definition) ).
cnf(t42308,plain,
sF14 = join(complement(sF12),complement(complement(composition(sk1,sk3)))),
inference(step,[status(thm)],[t26,t34]) ).
cnf(t42309,plain,
sF14 = join(sF13,complement(complement(composition(sk1,sk3)))),
inference(step,[status(thm)],[t42308,t55]) ).
cnf(t42310,plain,
sF14 = join(sF13,complement(complement(sF7))),
inference(step,[status(thm)],[t42309,t33]) ).
cnf(t42311,plain,
sF14 = join(sF13,complement(sF8)),
inference(step,[status(thm)],[t42310,t51]) ).
cnf(t42312,plain,
sF14 = join(sF13,sF9),
inference(step,[status(thm)],[t42311,t87]) ).
cnf(t42313,plain,
sF14 = join(sF9,sF13),
inference(step,[status(thm)],[t42312,t41]) ).
cnf(t434,plain,
join(sF9,sF13) = sF14,
inference(orient,[status(thm)],[t42313]) ).
cnf(t42427,plain,
join(sF7,sF13) = sF14,
inference(step,[status(thm)],[t434,t1581]) ).
cnf(t1588,plain,
join(sF7,sF13) = sF14,
inference(rw,[status(thm)],[t42427]) ).
cnf(t1770,plain,
join(sF7,sF13) = sF14,
inference(orient,[status(thm)],[t1588]) ).
cnf(t23,axiom,
sF11 = complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),
introduced(definition) ).
cnf(t42292,plain,
sF11 = complement(join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t23,t41]) ).
cnf(t42293,plain,
sF11 = complement(join(complement(complement(sF7)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t42292,t33]) ).
cnf(t42294,plain,
sF11 = complement(join(complement(sF8),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t42293,t51]) ).
cnf(t42295,plain,
sF11 = complement(join(sF9,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t42294,t87]) ).
cnf(t42296,plain,
sF11 = complement(join(sF9,complement(composition(sk1,complement(join(sF0,complement(complement(sk3)))))))),
inference(step,[status(thm)],[t42295,t28]) ).
cnf(t42297,plain,
sF11 = complement(join(sF9,complement(composition(sk1,complement(join(sF0,complement(sF1))))))),
inference(step,[status(thm)],[t42296,t29]) ).
cnf(t42298,plain,
sF11 = complement(join(sF9,complement(composition(sk1,complement(join(sF0,sF2)))))),
inference(step,[status(thm)],[t42297,t32]) ).
cnf(t42299,plain,
sF11 = complement(join(sF9,complement(composition(sk1,complement(sF3))))),
inference(step,[status(thm)],[t42298,t244]) ).
cnf(t42300,plain,
sF11 = complement(join(sF9,complement(composition(sk1,sF4)))),
inference(step,[status(thm)],[t42299,t295]) ).
cnf(t42301,plain,
sF11 = complement(join(sF9,complement(sF5))),
inference(step,[status(thm)],[t42300,t328]) ).
cnf(t42302,plain,
sF11 = complement(join(sF9,sF6)),
inference(step,[status(thm)],[t42301,t362]) ).
cnf(t42303,plain,
sF11 = complement(join(sF6,sF9)),
inference(step,[status(thm)],[t42302,t41]) ).
cnf(t42304,plain,
sF11 = complement(sF10),
inference(step,[status(thm)],[t42303,t388]) ).
cnf(t407,plain,
complement(sF10) = sF11,
inference(orient,[status(thm)],[t42304]) ).
cnf(t410,plain,
sF10 = join(complement(join(sF11,X1)),complement(join(complement(sF10),complement(X1)))),
inference(cp,[status(thm)],[t197,t407]) ).
cnf(t42714,plain,
sF10 = join(complement(join(sF11,X1)),complement(join(sF11,complement(X1)))),
inference(step,[status(thm)],[t410,t407]) ).
cnf(t7287,plain,
join(complement(join(sF11,X1)),complement(join(sF11,complement(X1)))) = sF10,
inference(orient,[status(thm)],[t42714]) ).
cnf(t411,plain,
X1 = join(complement(join(complement(X1),sF10)),complement(join(complement(X1),sF11))),
inference(cp,[status(thm)],[t197,t407]) ).
cnf(t42719,plain,
X1 = join(complement(join(sF10,complement(X1))),complement(join(complement(X1),sF11))),
inference(step,[status(thm)],[t411,t41]) ).
cnf(t42720,plain,
X1 = join(complement(join(sF10,complement(X1))),complement(join(sF11,complement(X1)))),
inference(step,[status(thm)],[t42719,t41]) ).
cnf(t7388,plain,
join(complement(join(sF10,complement(X1))),complement(join(sF11,complement(X1)))) = X1,
inference(orient,[status(thm)],[t42720]) ).
cnf(t1536,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t284,t1530]) ).
cnf(t42441,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1536,t1530]) ).
cnf(t42442,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t42441,t1530]) ).
cnf(t1649,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t42442]) ).
cnf(t79,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t75,t41]) ).
cnf(t42342,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t79,t75]) ).
cnf(t761,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t42342]) ).
cnf(t1668,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t1649,t761]) ).
cnf(t42517,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t1668,t75]) ).
cnf(t42518,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t42517,t1649]) ).
cnf(t2657,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t42518]) ).
cnf(t7334,plain,
join(complement(join(sF11,X1)),complement(join(sF11,complement(X1)))) = join(complement(join(sF11,X1)),sF10),
inference(cp,[status(thm)],[t2657,t7287]) ).
cnf(t42825,plain,
sF10 = join(complement(join(sF11,X1)),sF10),
inference(step,[status(thm)],[t7334,t7287]) ).
cnf(t42826,plain,
sF10 = join(sF10,complement(join(sF11,X1))),
inference(step,[status(thm)],[t42825,t41]) ).
cnf(t12092,plain,
join(sF10,complement(join(sF11,X1))) = sF10,
inference(orient,[status(thm)],[t42826]) ).
cnf(t211,plain,
sF12 = join(complement(join(sF13,X1)),complement(join(complement(sF12),complement(X1)))),
inference(cp,[status(thm)],[t197,t55]) ).
cnf(t42637,plain,
sF12 = join(complement(join(sF13,X1)),complement(join(sF13,complement(X1)))),
inference(step,[status(thm)],[t211,t55]) ).
cnf(t5505,plain,
join(complement(join(sF13,X1)),complement(join(sF13,complement(X1)))) = sF12,
inference(orient,[status(thm)],[t42637]) ).
cnf(t5552,plain,
join(complement(join(sF13,X1)),complement(join(sF13,complement(X1)))) = join(complement(join(sF13,X1)),sF12),
inference(cp,[status(thm)],[t2657,t5505]) ).
cnf(t42761,plain,
sF12 = join(complement(join(sF13,X1)),sF12),
inference(step,[status(thm)],[t5552,t5505]) ).
cnf(t42762,plain,
sF12 = join(sF12,complement(join(sF13,X1))),
inference(step,[status(thm)],[t42761,t41]) ).
cnf(t7893,plain,
join(sF12,complement(join(sF13,X1))) = sF12,
inference(orient,[status(thm)],[t42762]) ).
cnf(t289,plain,
complement(sF12) = join(sF13,complement(sF12)),
inference(cp,[status(thm)],[t284,t55]) ).
cnf(t42226,plain,
sF13 = join(sF13,complement(sF12)),
inference(step,[status(thm)],[t289,t55]) ).
cnf(t42227,plain,
sF13 = join(sF13,sF13),
inference(step,[status(thm)],[t42226,t55]) ).
cnf(t311,plain,
join(sF13,sF13) = sF13,
inference(orient,[status(thm)],[t42227]) ).
cnf(t312,plain,
join(sF13,join(sF13,X1)) = join(sF13,X1),
inference(cp,[status(thm)],[t75,t311]) ).
cnf(t1405,plain,
join(sF13,join(sF13,X1)) = join(sF13,X1),
inference(orient,[status(thm)],[t312]) ).
cnf(t1406,plain,
join(sF13,X1) = join(join(sF13,X1),sF13),
inference(cp,[status(thm)],[t1405,t41]) ).
cnf(t42511,plain,
join(sF13,X1) = join(sF13,join(X1,sF13)),
inference(step,[status(thm)],[t1406,t75]) ).
cnf(t2488,plain,
join(sF13,join(X1,sF13)) = join(sF13,X1),
inference(orient,[status(thm)],[t42511]) ).
cnf(t2491,plain,
join(sF13,sF7) = join(sF13,sF14),
inference(cp,[status(thm)],[t2488,t1770]) ).
cnf(t42512,plain,
join(sF7,sF13) = join(sF13,sF14),
inference(step,[status(thm)],[t2491,t41]) ).
cnf(t42513,plain,
sF14 = join(sF13,sF14),
inference(step,[status(thm)],[t42512,t1770]) ).
cnf(t2496,plain,
join(sF13,sF14) = sF14,
inference(orient,[status(thm)],[t42513]) ).
cnf(t2501,plain,
join(sF13,join(X1,sF14)) = join(X1,sF14),
inference(cp,[status(thm)],[t761,t2496]) ).
cnf(t3395,plain,
join(sF13,join(X1,sF14)) = join(X1,sF14),
inference(orient,[status(thm)],[t2501]) ).
cnf(t7899,plain,
sF12 = join(sF12,complement(join(X1,sF14))),
inference(cp,[status(thm)],[t7893,t3395]) ).
cnf(t14166,plain,
join(sF12,complement(join(X1,sF14))) = sF12,
inference(orient,[status(thm)],[t7899]) ).
cnf(t1776,plain,
join(sF7,join(X1,sF13)) = join(X1,sF14),
inference(cp,[status(thm)],[t761,t1770]) ).
cnf(t3070,plain,
join(sF7,join(X1,sF13)) = join(X1,sF14),
inference(orient,[status(thm)],[t1776]) ).
cnf(t77,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t75,t35]) ).
cnf(t622,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t77]) ).
cnf(t639,plain,
X1 = join(complement(join(top,X2)),complement(join(complement(X1),complement(join(complement(complement(X1)),X2))))),
inference(cp,[status(thm)],[t197,t622]) ).
cnf(t76,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t75,t35]) ).
cnf(t552,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t76]) ).
cnf(t567,plain,
top = join(complement(X1),join(complement(X1),complement(complement(X1)))),
inference(cp,[status(thm)],[t552,t284]) ).
cnf(t42337,plain,
top = join(complement(X1),top),
inference(step,[status(thm)],[t567,t35]) ).
cnf(t42338,plain,
top = join(top,complement(X1)),
inference(step,[status(thm)],[t42337,t41]) ).
cnf(t643,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t42338]) ).
cnf(t661,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t552,t643]) ).
cnf(t823,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t661]) ).
cnf(t839,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t823,t41]) ).
cnf(t914,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t839]) ).
cnf(t42867,plain,
X1 = join(complement(top),complement(join(complement(X1),complement(join(complement(complement(X1)),X2))))),
inference(step,[status(thm)],[t639,t914]) ).
cnf(t42868,plain,
X1 = join(zero,complement(join(complement(X1),complement(join(complement(complement(X1)),X2))))),
inference(step,[status(thm)],[t42867,t57]) ).
cnf(t42869,plain,
X1 = complement(join(complement(X1),complement(join(complement(complement(X1)),X2)))),
inference(step,[status(thm)],[t42868,t1421]) ).
cnf(t42870,plain,
X1 = complement(join(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t42869,t1530]) ).
cnf(t15156,plain,
complement(join(complement(X1),complement(join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t42870]) ).
cnf(t6,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t66,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t6]) ).
cnf(t67,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t66,t31]) ).
cnf(t162,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t67]) ).
cnf(t169,plain,
composition(converse(X1),join(converse(X2),X3)) = converse(composition(join(X2,converse(X3)),X1)),
inference(cp,[status(thm)],[t108,t162]) ).
cnf(t4124,plain,
converse(composition(join(X1,converse(X2)),X3)) = composition(converse(X3),join(converse(X1),X2)),
inference(orient,[status(thm)],[t169]) ).
cnf(t9,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t89,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t9]) ).
cnf(t95,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t89,t63]) ).
cnf(t966,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t95]) ).
cnf(t968,plain,
composition(join(converse(sk2),X1),converse(sk1)) = join(converse(sF12),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t966,t34]) ).
cnf(t23344,plain,
composition(join(converse(sk2),X1),converse(sk1)) = join(converse(sF12),composition(X1,converse(sk1))),
inference(orient,[status(thm)],[t968]) ).
cnf(t23400,plain,
composition(converse(converse(sk1)),join(converse(converse(sk2)),X1)) = converse(join(converse(sF12),composition(converse(X1),converse(sk1)))),
inference(cp,[status(thm)],[t4124,t23344]) ).
cnf(t42983,plain,
composition(sk1,join(converse(converse(sk2)),X1)) = converse(join(converse(sF12),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t23400,t31]) ).
cnf(t42984,plain,
composition(sk1,join(sk2,X1)) = converse(join(converse(sF12),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t42983,t31]) ).
cnf(t42985,plain,
composition(sk1,join(sk2,X1)) = join(sF12,converse(composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t42984,t162]) ).
cnf(t64,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t63,t31]) ).
cnf(t103,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t64]) ).
cnf(t42986,plain,
composition(sk1,join(sk2,X1)) = join(sF12,composition(sk1,converse(converse(X1)))),
inference(step,[status(thm)],[t42985,t103]) ).
cnf(t42987,plain,
composition(sk1,join(sk2,X1)) = join(sF12,composition(sk1,X1)),
inference(step,[status(thm)],[t42986,t31]) ).
cnf(t23437,plain,
composition(sk1,join(sk2,X1)) = join(sF12,composition(sk1,X1)),
inference(orient,[status(thm)],[t42987]) ).
cnf(t23440,plain,
join(sF12,composition(sk1,X1)) = composition(sk1,join(X1,sk2)),
inference(cp,[status(thm)],[t23437,t41]) ).
cnf(t23553,plain,
composition(sk1,join(X1,sk2)) = join(sF12,composition(sk1,X1)),
inference(orient,[status(thm)],[t23440]) ).
cnf(t299,plain,
X1 = join(complement(join(complement(X1),sF3)),complement(join(complement(X1),sF4))),
inference(cp,[status(thm)],[t197,t295]) ).
cnf(t42674,plain,
X1 = join(complement(join(sF3,complement(X1))),complement(join(complement(X1),sF4))),
inference(step,[status(thm)],[t299,t41]) ).
cnf(t42675,plain,
X1 = join(complement(join(sF3,complement(X1))),complement(join(sF4,complement(X1)))),
inference(step,[status(thm)],[t42674,t41]) ).
cnf(t6795,plain,
join(complement(join(sF3,complement(X1))),complement(join(sF4,complement(X1)))) = X1,
inference(orient,[status(thm)],[t42675]) ).
cnf(t1138,plain,
sk2 = join(zero,complement(sF0)),
inference(cp,[status(thm)],[t1137,t28]) ).
cnf(t1206,plain,
join(zero,complement(sF0)) = sk2,
inference(orient,[status(thm)],[t1138]) ).
cnf(t42407,plain,
complement(sF0) = sk2,
inference(step,[status(thm)],[t1206,t1421]) ).
cnf(t1424,plain,
complement(sF0) = sk2,
inference(rw,[status(thm)],[t42407]) ).
cnf(t1444,plain,
complement(sF0) = sk2,
inference(orient,[status(thm)],[t1424]) ).
cnf(t6805,plain,
sF0 = join(complement(join(sF3,sk2)),complement(join(sF4,complement(sF0)))),
inference(cp,[status(thm)],[t6795,t1444]) ).
cnf(t246,plain,
join(sF0,join(sF2,X1)) = join(sF3,X1),
inference(cp,[status(thm)],[t75,t244]) ).
cnf(t1021,plain,
join(sF0,join(sF2,X1)) = join(sF3,X1),
inference(orient,[status(thm)],[t246]) ).
cnf(t36,plain,
top = join(sk2,sF0),
inference(cp,[status(thm)],[t35,t28]) ).
cnf(t39,plain,
join(sk2,sF0) = top,
inference(orient,[status(thm)],[t36]) ).
cnf(t42192,plain,
join(sF0,sk2) = top,
inference(step,[status(thm)],[t39,t41]) ).
cnf(t42,plain,
join(sF0,sk2) = top,
inference(rw,[status(thm)],[t42192]) ).
cnf(t47,plain,
join(sF0,sk2) = top,
inference(orient,[status(thm)],[t42]) ).
cnf(t81,plain,
join(sF0,join(sk2,X1)) = join(top,X1),
inference(cp,[status(thm)],[t75,t47]) ).
cnf(t193,plain,
join(sF0,join(sk2,X1)) = join(top,X1),
inference(orient,[status(thm)],[t81]) ).
cnf(t196,plain,
join(top,X1) = join(sF0,join(X1,sk2)),
inference(cp,[status(thm)],[t193,t41]) ).
cnf(t418,plain,
join(sF0,join(X1,sk2)) = join(top,X1),
inference(orient,[status(thm)],[t196]) ).
cnf(t42374,plain,
join(sF0,join(X1,sk2)) = top,
inference(step,[status(thm)],[t418,t914]) ).
cnf(t931,plain,
join(sF0,join(X1,sk2)) = top,
inference(orient,[status(thm)],[t42374]) ).
cnf(t1026,plain,
join(sF3,sk2) = top,
inference(cp,[status(thm)],[t1021,t931]) ).
cnf(t1044,plain,
join(sF3,sk2) = top,
inference(orient,[status(thm)],[t1026]) ).
cnf(t42676,plain,
sF0 = join(complement(top),complement(join(sF4,complement(sF0)))),
inference(step,[status(thm)],[t6805,t1044]) ).
cnf(t42677,plain,
sF0 = join(zero,complement(join(sF4,complement(sF0)))),
inference(step,[status(thm)],[t42676,t57]) ).
cnf(t42678,plain,
sF0 = complement(join(sF4,complement(sF0))),
inference(step,[status(thm)],[t42677,t1421]) ).
cnf(t42679,plain,
sF0 = complement(join(sF4,sk2)),
inference(step,[status(thm)],[t42678,t1444]) ).
cnf(t6832,plain,
complement(join(sF4,sk2)) = sF0,
inference(orient,[status(thm)],[t42679]) ).
cnf(t6836,plain,
join(sF4,sk2) = join(complement(join(sF0,X1)),complement(join(complement(join(sF4,sk2)),complement(X1)))),
inference(cp,[status(thm)],[t197,t6832]) ).
cnf(t42680,plain,
join(sF4,sk2) = join(complement(join(sF0,X1)),complement(join(sF0,complement(X1)))),
inference(step,[status(thm)],[t6836,t6832]) ).
cnf(t198,plain,
sk2 = join(complement(join(sF0,X1)),complement(join(complement(sk2),complement(X1)))),
inference(cp,[status(thm)],[t197,t28]) ).
cnf(t42609,plain,
sk2 = join(complement(join(sF0,X1)),complement(join(sF0,complement(X1)))),
inference(step,[status(thm)],[t198,t28]) ).
cnf(t4824,plain,
join(complement(join(sF0,X1)),complement(join(sF0,complement(X1)))) = sk2,
inference(orient,[status(thm)],[t42609]) ).
cnf(t42681,plain,
join(sF4,sk2) = sk2,
inference(step,[status(thm)],[t42680,t4824]) ).
cnf(t6868,plain,
join(sF4,sk2) = sk2,
inference(orient,[status(thm)],[t42681]) ).
cnf(t23555,plain,
join(sF12,composition(sk1,sF4)) = composition(sk1,sk2),
inference(cp,[status(thm)],[t23553,t6868]) ).
cnf(t42989,plain,
join(sF12,sF5) = composition(sk1,sk2),
inference(step,[status(thm)],[t23555,t328]) ).
cnf(t42990,plain,
join(sF5,sF12) = composition(sk1,sk2),
inference(step,[status(thm)],[t42989,t41]) ).
cnf(t42991,plain,
join(sF5,sF12) = sF12,
inference(step,[status(thm)],[t42990,t34]) ).
cnf(t23579,plain,
join(sF5,sF12) = sF12,
inference(orient,[status(thm)],[t42991]) ).
cnf(t23600,plain,
sF5 = complement(join(complement(sF5),complement(sF12))),
inference(cp,[status(thm)],[t15156,t23579]) ).
cnf(t42997,plain,
sF5 = complement(join(sF6,complement(sF12))),
inference(step,[status(thm)],[t23600,t362]) ).
cnf(t42998,plain,
sF5 = complement(join(sF6,sF13)),
inference(step,[status(thm)],[t42997,t55]) ).
cnf(t24096,plain,
complement(join(sF6,sF13)) = sF5,
inference(orient,[status(thm)],[t42998]) ).
cnf(t24102,plain,
join(sF6,sF13) = complement(sF5),
inference(cp,[status(thm)],[t1530,t24096]) ).
cnf(t42999,plain,
join(sF6,sF13) = sF6,
inference(step,[status(thm)],[t24102,t362]) ).
cnf(t24153,plain,
join(sF6,sF13) = sF6,
inference(orient,[status(thm)],[t42999]) ).
cnf(t24163,plain,
join(sF6,sF14) = join(sF7,sF6),
inference(cp,[status(thm)],[t3070,t24153]) ).
cnf(t43001,plain,
join(sF6,sF14) = join(sF6,sF7),
inference(step,[status(thm)],[t24163,t41]) ).
cnf(t43002,plain,
join(sF6,sF14) = sF10,
inference(step,[status(thm)],[t43001,t1762]) ).
cnf(t24223,plain,
join(sF6,sF14) = sF10,
inference(orient,[status(thm)],[t43002]) ).
cnf(t24257,plain,
sF12 = join(sF12,complement(sF10)),
inference(cp,[status(thm)],[t14166,t24223]) ).
cnf(t43016,plain,
sF12 = join(sF12,sF11),
inference(step,[status(thm)],[t24257,t407]) ).
cnf(t43017,plain,
sF12 = join(sF11,sF12),
inference(step,[status(thm)],[t43016,t41]) ).
cnf(t24347,plain,
join(sF11,sF12) = sF12,
inference(orient,[status(thm)],[t43017]) ).
cnf(t24352,plain,
join(sF11,join(X1,sF12)) = join(X1,sF12),
inference(cp,[status(thm)],[t761,t24347]) ).
cnf(t28765,plain,
join(sF11,join(X1,sF12)) = join(X1,sF12),
inference(orient,[status(thm)],[t24352]) ).
cnf(t28785,plain,
sF10 = join(sF10,complement(join(X1,sF12))),
inference(cp,[status(thm)],[t12092,t28765]) ).
cnf(t37035,plain,
join(sF10,complement(join(X1,sF12))) = sF10,
inference(orient,[status(thm)],[t28785]) ).
cnf(t985,plain,
composition(join(converse(sF4),X1),converse(sk1)) = join(converse(sF5),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t966,t328]) ).
cnf(t34549,plain,
composition(join(converse(sF4),X1),converse(sk1)) = join(converse(sF5),composition(X1,converse(sk1))),
inference(orient,[status(thm)],[t985]) ).
cnf(t34609,plain,
composition(converse(converse(sk1)),join(converse(converse(sF4)),X1)) = converse(join(converse(sF5),composition(converse(X1),converse(sk1)))),
inference(cp,[status(thm)],[t4124,t34549]) ).
cnf(t43134,plain,
composition(sk1,join(converse(converse(sF4)),X1)) = converse(join(converse(sF5),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t34609,t31]) ).
cnf(t43135,plain,
composition(sk1,join(sF4,X1)) = converse(join(converse(sF5),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t43134,t31]) ).
cnf(t43136,plain,
composition(sk1,join(sF4,X1)) = join(sF5,converse(composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t43135,t162]) ).
cnf(t43137,plain,
composition(sk1,join(sF4,X1)) = join(sF5,composition(sk1,converse(converse(X1)))),
inference(step,[status(thm)],[t43136,t103]) ).
cnf(t43138,plain,
composition(sk1,join(sF4,X1)) = join(sF5,composition(sk1,X1)),
inference(step,[status(thm)],[t43137,t31]) ).
cnf(t34657,plain,
composition(sk1,join(sF4,X1)) = join(sF5,composition(sk1,X1)),
inference(orient,[status(thm)],[t43138]) ).
cnf(t287,plain,
complement(sF1) = join(sF2,complement(sF1)),
inference(cp,[status(thm)],[t284,t32]) ).
cnf(t42222,plain,
sF2 = join(sF2,complement(sF1)),
inference(step,[status(thm)],[t287,t32]) ).
cnf(t42223,plain,
sF2 = join(sF2,sF2),
inference(step,[status(thm)],[t42222,t32]) ).
cnf(t305,plain,
join(sF2,sF2) = sF2,
inference(orient,[status(thm)],[t42223]) ).
cnf(t306,plain,
join(sF2,join(sF2,X1)) = join(sF2,X1),
inference(cp,[status(thm)],[t75,t305]) ).
cnf(t1354,plain,
join(sF2,join(sF2,X1)) = join(sF2,X1),
inference(orient,[status(thm)],[t306]) ).
cnf(t1355,plain,
join(sF2,X1) = join(join(sF2,X1),sF2),
inference(cp,[status(thm)],[t1354,t41]) ).
cnf(t42505,plain,
join(sF2,X1) = join(sF2,join(X1,sF2)),
inference(step,[status(thm)],[t1355,t75]) ).
cnf(t2429,plain,
join(sF2,join(X1,sF2)) = join(sF2,X1),
inference(orient,[status(thm)],[t42505]) ).
cnf(t78,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t75,t41]) ).
cnf(t663,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t78]) ).
cnf(t1670,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t663,t1649]) ).
cnf(t2733,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(orient,[status(thm)],[t1670]) ).
cnf(t42530,plain,
join(X1,sF2) = join(sF2,X1),
inference(step,[status(thm)],[t2429,t2733]) ).
cnf(t2736,plain,
join(X1,sF2) = join(sF2,X1),
inference(rw,[status(thm)],[t42530]) ).
cnf(t6014,plain,
join(X1,sF2) = join(sF2,X1),
inference(orient,[status(thm)],[t2736]) ).
cnf(t34672,plain,
join(sF5,composition(sk1,sF2)) = composition(sk1,join(sF2,sF4)),
inference(cp,[status(thm)],[t34657,t6014]) ).
cnf(t43139,plain,
join(sF5,sF7) = composition(sk1,join(sF2,sF4)),
inference(step,[status(thm)],[t34672,t1735]) ).
cnf(t23453,plain,
join(sF12,composition(sk1,sF2)) = composition(sk1,join(sF2,sk2)),
inference(cp,[status(thm)],[t23437,t6014]) ).
cnf(t43022,plain,
join(sF12,sF7) = composition(sk1,join(sF2,sk2)),
inference(step,[status(thm)],[t23453,t1735]) ).
cnf(t203,plain,
X1 = join(complement(join(complement(X1),sF1)),complement(join(complement(X1),sF2))),
inference(cp,[status(thm)],[t197,t32]) ).
cnf(t42614,plain,
X1 = join(complement(join(sF1,complement(X1))),complement(join(complement(X1),sF2))),
inference(step,[status(thm)],[t203,t41]) ).
cnf(t42615,plain,
X1 = join(complement(join(sF1,complement(X1))),complement(join(sF2,complement(X1)))),
inference(step,[status(thm)],[t42614,t41]) ).
cnf(t4964,plain,
join(complement(join(sF1,complement(X1))),complement(join(sF2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t42615]) ).
cnf(t298,plain,
sF3 = join(complement(join(sF4,X1)),complement(join(complement(sF3),complement(X1)))),
inference(cp,[status(thm)],[t197,t295]) ).
cnf(t42673,plain,
sF3 = join(complement(join(sF4,X1)),complement(join(sF4,complement(X1)))),
inference(step,[status(thm)],[t298,t295]) ).
cnf(t6740,plain,
join(complement(join(sF4,X1)),complement(join(sF4,complement(X1)))) = sF3,
inference(orient,[status(thm)],[t42673]) ).
cnf(t199,plain,
X1 = join(complement(join(complement(X1),sk2)),complement(join(complement(X1),sF0))),
inference(cp,[status(thm)],[t197,t28]) ).
cnf(t42610,plain,
X1 = join(complement(join(complement(X1),sF0)),complement(join(complement(X1),sk2))),
inference(step,[status(thm)],[t199,t41]) ).
cnf(t42611,plain,
X1 = join(complement(join(sF0,complement(X1))),complement(join(complement(X1),sk2))),
inference(step,[status(thm)],[t42610,t41]) ).
cnf(t42612,plain,
X1 = join(complement(join(sF0,complement(X1))),complement(join(sk2,complement(X1)))),
inference(step,[status(thm)],[t42611,t41]) ).
cnf(t4875,plain,
join(complement(join(sF0,complement(X1))),complement(join(sk2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t42612]) ).
cnf(t4877,plain,
sF1 = join(complement(join(sF0,sF2)),complement(join(sk2,complement(sF1)))),
inference(cp,[status(thm)],[t4875,t32]) ).
cnf(t42710,plain,
sF1 = join(complement(sF3),complement(join(sk2,complement(sF1)))),
inference(step,[status(thm)],[t4877,t244]) ).
cnf(t42711,plain,
sF1 = join(sF4,complement(join(sk2,complement(sF1)))),
inference(step,[status(thm)],[t42710,t295]) ).
cnf(t42712,plain,
sF1 = join(sF4,complement(join(sk2,sF2))),
inference(step,[status(thm)],[t42711,t32]) ).
cnf(t42713,plain,
sF1 = join(sF4,complement(join(sF2,sk2))),
inference(step,[status(thm)],[t42712,t41]) ).
cnf(t7269,plain,
join(sF4,complement(join(sF2,sk2))) = sF1,
inference(orient,[status(thm)],[t42713]) ).
cnf(t7284,plain,
sF3 = join(complement(sF1),complement(join(sF4,complement(complement(join(sF2,sk2)))))),
inference(cp,[status(thm)],[t6740,t7269]) ).
cnf(t42810,plain,
sF3 = join(sF2,complement(join(sF4,complement(complement(join(sF2,sk2)))))),
inference(step,[status(thm)],[t7284,t32]) ).
cnf(t42811,plain,
sF3 = join(sF2,complement(join(sF4,join(sF2,sk2)))),
inference(step,[status(thm)],[t42810,t1530]) ).
cnf(t6874,plain,
join(sF4,join(X1,sk2)) = join(X1,sk2),
inference(cp,[status(thm)],[t761,t6868]) ).
cnf(t6912,plain,
join(sF4,join(X1,sk2)) = join(X1,sk2),
inference(orient,[status(thm)],[t6874]) ).
cnf(t42812,plain,
sF3 = join(sF2,complement(join(sF2,sk2))),
inference(step,[status(thm)],[t42811,t6912]) ).
cnf(t11850,plain,
join(sF2,complement(join(sF2,sk2))) = sF3,
inference(orient,[status(thm)],[t42812]) ).
cnf(t11861,plain,
join(sF2,sk2) = join(complement(join(sF1,complement(join(sF2,sk2)))),complement(sF3)),
inference(cp,[status(thm)],[t4964,t11850]) ).
cnf(t42813,plain,
join(sF2,sk2) = join(complement(sF3),complement(join(sF1,complement(join(sF2,sk2))))),
inference(step,[status(thm)],[t11861,t41]) ).
cnf(t42814,plain,
join(sF2,sk2) = join(sF4,complement(join(sF1,complement(join(sF2,sk2))))),
inference(step,[status(thm)],[t42813,t295]) ).
cnf(t202,plain,
sF1 = join(complement(join(sF2,X1)),complement(join(complement(sF1),complement(X1)))),
inference(cp,[status(thm)],[t197,t32]) ).
cnf(t42613,plain,
sF1 = join(complement(join(sF2,X1)),complement(join(sF2,complement(X1)))),
inference(step,[status(thm)],[t202,t32]) ).
cnf(t4907,plain,
join(complement(join(sF2,X1)),complement(join(sF2,complement(X1)))) = sF1,
inference(orient,[status(thm)],[t42613]) ).
cnf(t4954,plain,
join(complement(join(sF2,X1)),complement(join(sF2,complement(X1)))) = join(complement(join(sF2,X1)),sF1),
inference(cp,[status(thm)],[t2657,t4907]) ).
cnf(t42727,plain,
sF1 = join(complement(join(sF2,X1)),sF1),
inference(step,[status(thm)],[t4954,t4907]) ).
cnf(t42728,plain,
sF1 = join(sF1,complement(join(sF2,X1))),
inference(step,[status(thm)],[t42727,t41]) ).
cnf(t7483,plain,
join(sF1,complement(join(sF2,X1))) = sF1,
inference(orient,[status(thm)],[t42728]) ).
cnf(t42815,plain,
join(sF2,sk2) = join(sF4,complement(sF1)),
inference(step,[status(thm)],[t42814,t7483]) ).
cnf(t42816,plain,
join(sF2,sk2) = join(sF4,sF2),
inference(step,[status(thm)],[t42815,t32]) ).
cnf(t42817,plain,
join(sF2,sk2) = join(sF2,sF4),
inference(step,[status(thm)],[t42816,t41]) ).
cnf(t11875,plain,
join(sF2,sk2) = join(sF2,sF4),
inference(orient,[status(thm)],[t42817]) ).
cnf(t43023,plain,
join(sF12,sF7) = composition(sk1,join(sF2,sF4)),
inference(step,[status(thm)],[t43022,t11875]) ).
cnf(t43024,plain,
join(sF7,sF12) = composition(sk1,join(sF2,sF4)),
inference(step,[status(thm)],[t43023,t41]) ).
cnf(t24616,plain,
composition(sk1,join(sF2,sF4)) = join(sF7,sF12),
inference(orient,[status(thm)],[t43024]) ).
cnf(t43140,plain,
join(sF5,sF7) = join(sF7,sF12),
inference(step,[status(thm)],[t43139,t24616]) ).
cnf(t34728,plain,
join(sF7,sF12) = join(sF5,sF7),
inference(orient,[status(thm)],[t43140]) ).
cnf(t37037,plain,
sF10 = join(sF10,complement(join(sF5,sF7))),
inference(cp,[status(thm)],[t37035,t34728]) ).
cnf(t41743,plain,
join(sF10,complement(join(sF5,sF7))) = sF10,
inference(orient,[status(thm)],[t37037]) ).
cnf(t41754,plain,
join(sF5,sF7) = join(complement(sF10),complement(join(sF11,complement(join(sF5,sF7))))),
inference(cp,[status(thm)],[t7388,t41743]) ).
cnf(t43219,plain,
join(sF5,sF7) = join(sF11,complement(join(sF11,complement(join(sF5,sF7))))),
inference(step,[status(thm)],[t41754,t407]) ).
cnf(t366,plain,
X1 = join(complement(join(complement(X1),sF5)),complement(join(complement(X1),sF6))),
inference(cp,[status(thm)],[t197,t362]) ).
cnf(t42695,plain,
X1 = join(complement(join(sF5,complement(X1))),complement(join(complement(X1),sF6))),
inference(step,[status(thm)],[t366,t41]) ).
cnf(t42696,plain,
X1 = join(complement(join(sF5,complement(X1))),complement(join(sF6,complement(X1)))),
inference(step,[status(thm)],[t42695,t41]) ).
cnf(t7057,plain,
join(complement(join(sF5,complement(X1))),complement(join(sF6,complement(X1)))) = X1,
inference(orient,[status(thm)],[t42696]) ).
cnf(t42422,plain,
complement(sF8) = sF7,
inference(step,[status(thm)],[t87,t1581]) ).
cnf(t1582,plain,
complement(sF8) = sF7,
inference(orient,[status(thm)],[t42422]) ).
cnf(t7063,plain,
sF8 = join(complement(join(sF5,sF7)),complement(join(sF6,complement(sF8)))),
inference(cp,[status(thm)],[t7057,t1582]) ).
cnf(t42801,plain,
sF8 = join(complement(join(sF5,sF7)),complement(join(sF6,sF7))),
inference(step,[status(thm)],[t7063,t1582]) ).
cnf(t42802,plain,
sF8 = join(complement(join(sF5,sF7)),complement(sF10)),
inference(step,[status(thm)],[t42801,t1762]) ).
cnf(t42803,plain,
sF8 = join(complement(sF10),complement(join(sF5,sF7))),
inference(step,[status(thm)],[t42802,t41]) ).
cnf(t42804,plain,
sF8 = join(sF11,complement(join(sF5,sF7))),
inference(step,[status(thm)],[t42803,t407]) ).
cnf(t11446,plain,
join(sF11,complement(join(sF5,sF7))) = sF8,
inference(orient,[status(thm)],[t42804]) ).
cnf(t43220,plain,
join(sF5,sF7) = join(sF11,complement(sF8)),
inference(step,[status(thm)],[t43219,t11446]) ).
cnf(t43221,plain,
join(sF5,sF7) = join(sF11,sF7),
inference(step,[status(thm)],[t43220,t1582]) ).
cnf(t43222,plain,
join(sF5,sF7) = join(sF7,sF11),
inference(step,[status(thm)],[t43221,t41]) ).
cnf(t41797,plain,
join(sF7,sF11) = join(sF5,sF7),
inference(orient,[status(thm)],[t43222]) ).
cnf(t41802,plain,
join(sF7,join(sF11,X1)) = join(join(sF5,sF7),X1),
inference(cp,[status(thm)],[t75,t41797]) ).
cnf(t43224,plain,
join(sF7,join(sF11,X1)) = join(sF5,join(sF7,X1)),
inference(step,[status(thm)],[t41802,t75]) ).
cnf(t41955,plain,
join(sF7,join(sF11,X1)) = join(sF5,join(sF7,X1)),
inference(orient,[status(thm)],[t43224]) ).
cnf(t41965,plain,
join(sF5,join(sF7,sF13)) = join(sF11,sF14),
inference(cp,[status(thm)],[t41955,t3070]) ).
cnf(t43225,plain,
join(sF5,sF14) = join(sF11,sF14),
inference(step,[status(thm)],[t41965,t1770]) ).
cnf(t34734,plain,
join(sF7,join(sF12,X1)) = join(join(sF5,sF7),X1),
inference(cp,[status(thm)],[t75,t34728]) ).
cnf(t43147,plain,
join(sF7,join(sF12,X1)) = join(sF5,join(sF7,X1)),
inference(step,[status(thm)],[t34734,t75]) ).
cnf(t36006,plain,
join(sF7,join(sF12,X1)) = join(sF5,join(sF7,X1)),
inference(orient,[status(thm)],[t43147]) ).
cnf(t36007,plain,
join(sF5,join(sF7,complement(sF12))) = join(sF7,top),
inference(cp,[status(thm)],[t36006,t35]) ).
cnf(t43148,plain,
join(sF5,join(sF7,sF13)) = join(sF7,top),
inference(step,[status(thm)],[t36007,t55]) ).
cnf(t43149,plain,
join(sF5,sF14) = join(sF7,top),
inference(step,[status(thm)],[t43148,t1770]) ).
cnf(t43150,plain,
join(sF5,sF14) = top,
inference(step,[status(thm)],[t43149,t823]) ).
cnf(t36131,plain,
join(sF5,sF14) = top,
inference(orient,[status(thm)],[t43150]) ).
cnf(t43226,plain,
top = join(sF11,sF14),
inference(step,[status(thm)],[t43225,t36131]) ).
cnf(t42063,plain,
join(sF11,sF14) = top,
inference(orient,[status(thm)],[t43226]) ).
cnf(t42071,plain,
sF10 = join(complement(top),complement(join(sF11,complement(sF14)))),
inference(cp,[status(thm)],[t7287,t42063]) ).
cnf(t43227,plain,
sF10 = join(zero,complement(join(sF11,complement(sF14)))),
inference(step,[status(thm)],[t42071,t57]) ).
cnf(t43228,plain,
sF10 = complement(join(sF11,complement(sF14))),
inference(step,[status(thm)],[t43227,t1421]) ).
cnf(t27,axiom,
sF15 = complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
introduced(definition) ).
cnf(t42319,plain,
sF15 = complement(join(complement(sF12),complement(complement(composition(sk1,sk3))))),
inference(step,[status(thm)],[t27,t34]) ).
cnf(t42320,plain,
sF15 = complement(join(sF13,complement(complement(composition(sk1,sk3))))),
inference(step,[status(thm)],[t42319,t55]) ).
cnf(t42321,plain,
sF15 = complement(join(sF13,complement(complement(sF7)))),
inference(step,[status(thm)],[t42320,t33]) ).
cnf(t42322,plain,
sF15 = complement(join(sF13,complement(sF8))),
inference(step,[status(thm)],[t42321,t51]) ).
cnf(t42323,plain,
sF15 = complement(join(sF13,sF9)),
inference(step,[status(thm)],[t42322,t87]) ).
cnf(t42324,plain,
sF15 = complement(join(sF9,sF13)),
inference(step,[status(thm)],[t42323,t41]) ).
cnf(t42325,plain,
sF15 = complement(sF14),
inference(step,[status(thm)],[t42324,t434]) ).
cnf(t456,plain,
complement(sF14) = sF15,
inference(orient,[status(thm)],[t42325]) ).
cnf(t43229,plain,
sF10 = complement(join(sF11,sF15)),
inference(step,[status(thm)],[t43228,t456]) ).
cnf(t1772,plain,
join(sF7,join(sF13,X1)) = join(sF14,X1),
inference(cp,[status(thm)],[t75,t1770]) ).
cnf(t3001,plain,
join(sF7,join(sF13,X1)) = join(sF14,X1),
inference(orient,[status(thm)],[t1772]) ).
cnf(t24356,plain,
sF10 = join(complement(sF12),complement(join(sF11,complement(sF12)))),
inference(cp,[status(thm)],[t7287,t24347]) ).
cnf(t43106,plain,
sF10 = join(sF13,complement(join(sF11,complement(sF12)))),
inference(step,[status(thm)],[t24356,t55]) ).
cnf(t43107,plain,
sF10 = join(sF13,complement(join(sF11,sF13))),
inference(step,[status(thm)],[t43106,t55]) ).
cnf(t33245,plain,
join(sF13,complement(join(sF11,sF13))) = sF10,
inference(orient,[status(thm)],[t43107]) ).
cnf(t33258,plain,
join(sF14,complement(join(sF11,sF13))) = join(sF7,sF10),
inference(cp,[status(thm)],[t3001,t33245]) ).
cnf(t2748,plain,
join(sF6,sF7) = join(sF7,sF10),
inference(cp,[status(thm)],[t2733,t1762]) ).
cnf(t42536,plain,
sF10 = join(sF7,sF10),
inference(step,[status(thm)],[t2748,t1762]) ).
cnf(t2775,plain,
join(sF7,sF10) = sF10,
inference(orient,[status(thm)],[t42536]) ).
cnf(t43194,plain,
join(sF14,complement(join(sF11,sF13))) = sF10,
inference(step,[status(thm)],[t33258,t2775]) ).
cnf(t39696,plain,
join(sF14,complement(join(sF11,sF13))) = sF10,
inference(orient,[status(thm)],[t43194]) ).
cnf(t39730,plain,
sF14 = complement(join(complement(sF14),complement(sF10))),
inference(cp,[status(thm)],[t15156,t39696]) ).
cnf(t43195,plain,
sF14 = complement(join(complement(sF10),complement(sF14))),
inference(step,[status(thm)],[t39730,t41]) ).
cnf(t43196,plain,
sF14 = complement(join(sF11,complement(sF14))),
inference(step,[status(thm)],[t43195,t407]) ).
cnf(t43197,plain,
sF14 = complement(join(sF11,sF15)),
inference(step,[status(thm)],[t43196,t456]) ).
cnf(t39762,plain,
complement(join(sF11,sF15)) = sF14,
inference(orient,[status(thm)],[t43197]) ).
cnf(t39768,plain,
join(sF11,sF15) = complement(sF14),
inference(cp,[status(thm)],[t1530,t39762]) ).
cnf(t43198,plain,
join(sF11,sF15) = sF15,
inference(step,[status(thm)],[t39768,t456]) ).
cnf(t39819,plain,
join(sF11,sF15) = sF15,
inference(orient,[status(thm)],[t43198]) ).
cnf(t43230,plain,
sF10 = complement(sF15),
inference(step,[status(thm)],[t43229,t39819]) ).
cnf(t1148,plain,
sF14 = join(zero,complement(sF15)),
inference(cp,[status(thm)],[t1137,t456]) ).
cnf(t1295,plain,
join(zero,complement(sF15)) = sF14,
inference(orient,[status(thm)],[t1148]) ).
cnf(t42414,plain,
complement(sF15) = sF14,
inference(step,[status(thm)],[t1295,t1421]) ).
cnf(t1431,plain,
complement(sF15) = sF14,
inference(rw,[status(thm)],[t42414]) ).
cnf(t1521,plain,
complement(sF15) = sF14,
inference(orient,[status(thm)],[t1431]) ).
cnf(t43231,plain,
sF10 = sF14,
inference(step,[status(thm)],[t43230,t1521]) ).
cnf(t42104,plain,
sF14 = sF10,
inference(orient,[status(thm)],[t43231]) ).
cnf(t43235,plain,
join(sF7,sF13) = sF10,
inference(step,[status(thm)],[t1770,t42104]) ).
cnf(t42111,plain,
join(sF7,sF13) = sF10,
inference(orient,[status(thm)],[t43235]) ).
cnf(u1,negated_conjecture,
meet(composition(sk1,sk2),complement(composition(sk1,sk3))) != meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(g0_0,plain,
complement(join(complement(composition(sk1,complement(join(sF0,complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[goal_0,t28]) ).
cnf(g0_1,plain,
complement(join(complement(composition(sk1,complement(join(sF0,sk3)))),complement(complement(composition(sk1,sk3))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_0,t1530]) ).
cnf(g0_2,plain,
complement(join(complement(composition(sk1,complement(join(sF0,sF2)))),complement(complement(composition(sk1,sk3))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_1,t1538]) ).
cnf(g0_3,plain,
complement(join(complement(composition(sk1,complement(sF3))),complement(complement(composition(sk1,sk3))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_2,t244]) ).
cnf(g0_4,plain,
complement(join(complement(composition(sk1,sF4)),complement(complement(composition(sk1,sk3))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_3,t295]) ).
cnf(g0_5,plain,
complement(join(complement(sF5),complement(complement(composition(sk1,sk3))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_4,t328]) ).
cnf(g0_6,plain,
complement(join(sF6,complement(complement(composition(sk1,sk3))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_5,t362]) ).
cnf(g0_7,plain,
complement(join(sF6,composition(sk1,sk3))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_6,t1530]) ).
cnf(g0_8,plain,
complement(join(sF6,composition(sk1,sF2))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_7,t1538]) ).
cnf(g0_9,plain,
complement(join(sF6,sF7)) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_8,t1735]) ).
cnf(g0_10,plain,
complement(sF10) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_9,t1762]) ).
cnf(g0_11,plain,
complement(sF10) != complement(join(complement(sF12),complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_10,t34]) ).
cnf(g0_12,plain,
complement(sF10) != complement(join(sF13,complement(complement(composition(sk1,sk3))))),
inference(rw,[status(thm)],[g0_11,t55]) ).
cnf(g0_13,plain,
complement(sF10) != complement(join(sF13,composition(sk1,sk3))),
inference(rw,[status(thm)],[g0_12,t1530]) ).
cnf(g0_14,plain,
complement(sF10) != complement(join(sF13,composition(sk1,sF2))),
inference(rw,[status(thm)],[g0_13,t1538]) ).
cnf(g0_15,plain,
complement(sF10) != complement(join(sF13,sF7)),
inference(rw,[status(thm)],[g0_14,t1735]) ).
cnf(g0_16,plain,
complement(sF10) != complement(join(sF7,sF13)),
inference(rw,[status(thm)],[g0_15,t41]) ).
cnf(g0_17,plain,
complement(sF10) != complement(sF10),
inference(rw,[status(thm)],[g0_16,t42111]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL016-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n008.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 07:12:54 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 27.87/4.73 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.87/4.73 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------