%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL033-3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:35:55 PM UTC 2026
% Result : Unsatisfiable 26.98s 18.21s
% Output : CNFRefutation 26.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 102
% Number of leaves : 25
% Syntax : Number of clauses : 379 ( 379 unt; 0 nHn; 173 RR)
% Number of literals : 379 ( 378 equ; 14 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 15 con; 0-2 aty)
% Number of variables : 283 ( 55 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t136,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t17,axiom,
sFlat1 = complement(sk2),
introduced(definition) ).
cnf(t123,plain,
complement(sk2) = sFlat1,
inference(orient,[status(thm)],[t17]) ).
cnf(t16,axiom,
sFlat0 = complement(sk1),
introduced(definition) ).
cnf(t109,plain,
complement(sk1) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t18,axiom,
sFlat2 = join(complement(sk1),complement(sk2)),
introduced(definition) ).
cnf(t39292,plain,
sFlat2 = join(complement(sk2),complement(sk1)),
inference(step,[status(thm)],[t18,t136]) ).
cnf(t39293,plain,
sFlat2 = join(sFlat1,complement(sk1)),
inference(step,[status(thm)],[t39292,t123]) ).
cnf(t39294,plain,
sFlat2 = join(sFlat1,sFlat0),
inference(step,[status(thm)],[t39293,t109]) ).
cnf(t39295,plain,
sFlat2 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t39294,t136]) ).
cnf(t173,plain,
join(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t39295]) ).
cnf(t19,axiom,
sFlat3 = complement(join(complement(sk1),complement(sk2))),
introduced(definition) ).
cnf(t77,plain,
complement(join(complement(sk1),complement(sk2))) = sFlat3,
inference(orient,[status(thm)],[t19]) ).
cnf(t39288,plain,
complement(join(sFlat0,complement(sk2))) = sFlat3,
inference(step,[status(thm)],[t77,t109]) ).
cnf(t122,plain,
complement(join(sFlat0,complement(sk2))) = sFlat3,
inference(rw,[status(thm)],[t39288]) ).
cnf(t39309,plain,
complement(join(sFlat0,sFlat1)) = sFlat3,
inference(step,[status(thm)],[t122,t123]) ).
cnf(t39310,plain,
complement(sFlat2) = sFlat3,
inference(step,[status(thm)],[t39309,t173]) ).
cnf(t239,plain,
complement(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t39310]) ).
cnf(t20,axiom,
sFlat4 = composition(complement(join(complement(sk1),complement(sk2))),sk3),
introduced(definition) ).
cnf(t39296,plain,
sFlat4 = composition(complement(join(complement(sk2),complement(sk1))),sk3),
inference(step,[status(thm)],[t20,t136]) ).
cnf(t39297,plain,
sFlat4 = composition(complement(join(sFlat1,complement(sk1))),sk3),
inference(step,[status(thm)],[t39296,t123]) ).
cnf(t39298,plain,
sFlat4 = composition(complement(join(sFlat1,sFlat0)),sk3),
inference(step,[status(thm)],[t39297,t109]) ).
cnf(t39299,plain,
sFlat4 = composition(complement(join(sFlat0,sFlat1)),sk3),
inference(step,[status(thm)],[t39298,t136]) ).
cnf(t39300,plain,
sFlat4 = composition(complement(sFlat2),sk3),
inference(step,[status(thm)],[t39299,t173]) ).
cnf(t189,plain,
composition(complement(sFlat2),sk3) = sFlat4,
inference(orient,[status(thm)],[t39300]) ).
cnf(t39311,plain,
composition(sFlat3,sk3) = sFlat4,
inference(step,[status(thm)],[t189,t239]) ).
cnf(t244,plain,
composition(sFlat3,sk3) = sFlat4,
inference(rw,[status(thm)],[t39311]) ).
cnf(t247,plain,
composition(sFlat3,sk3) = sFlat4,
inference(orient,[status(thm)],[t244]) ).
cnf(t21,axiom,
sFlat5 = composition(sk2,sk3),
introduced(definition) ).
cnf(t208,plain,
composition(sk2,sk3) = sFlat5,
inference(orient,[status(thm)],[t21]) ).
cnf(t22,axiom,
sFlat6 = complement(composition(sk2,sk3)),
introduced(definition) ).
cnf(t92,plain,
complement(composition(sk2,sk3)) = sFlat6,
inference(orient,[status(thm)],[t22]) ).
cnf(t39301,plain,
complement(sFlat5) = sFlat6,
inference(step,[status(thm)],[t92,t208]) ).
cnf(t213,plain,
complement(sFlat5) = sFlat6,
inference(rw,[status(thm)],[t39301]) ).
cnf(t219,plain,
complement(sFlat5) = sFlat6,
inference(orient,[status(thm)],[t213]) ).
cnf(t23,axiom,
sFlat7 = join(complement(sk1),complement(composition(sk2,sk3))),
introduced(definition) ).
cnf(t39290,plain,
sFlat7 = join(sFlat0,complement(composition(sk2,sk3))),
inference(step,[status(thm)],[t23,t109]) ).
cnf(t39291,plain,
sFlat7 = join(sFlat0,sFlat6),
inference(step,[status(thm)],[t39290,t92]) ).
cnf(t171,plain,
join(sFlat0,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t39291]) ).
cnf(t24,axiom,
sFlat8 = complement(join(complement(sk1),complement(composition(sk2,sk3)))),
introduced(definition) ).
cnf(t62,plain,
complement(join(complement(sk1),complement(composition(sk2,sk3)))) = sFlat8,
inference(orient,[status(thm)],[t24]) ).
cnf(t39287,plain,
complement(join(complement(sk1),sFlat6)) = sFlat8,
inference(step,[status(thm)],[t62,t92]) ).
cnf(t108,plain,
complement(join(complement(sk1),sFlat6)) = sFlat8,
inference(rw,[status(thm)],[t39287]) ).
cnf(t39305,plain,
complement(join(sFlat6,complement(sk1))) = sFlat8,
inference(step,[status(thm)],[t108,t136]) ).
cnf(t39306,plain,
complement(join(sFlat6,sFlat0)) = sFlat8,
inference(step,[status(thm)],[t39305,t109]) ).
cnf(t39307,plain,
complement(join(sFlat0,sFlat6)) = sFlat8,
inference(step,[status(thm)],[t39306,t136]) ).
cnf(t39308,plain,
complement(sFlat7) = sFlat8,
inference(step,[status(thm)],[t39307,t171]) ).
cnf(t232,plain,
complement(sFlat7) = sFlat8,
inference(orient,[status(thm)],[t39308]) ).
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(t137,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t25]) ).
cnf(t39312,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t137,t136]) ).
cnf(t297,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t39312]) ).
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(t138,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(rw,[status(thm)],[t30]) ).
cnf(t39343,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t138,t136]) ).
cnf(t620,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t39343]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t194,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(t196,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t194,t29]) ).
cnf(t427,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t196]) ).
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(t428,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t427,t28]) ).
cnf(t39319,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t428,t29]) ).
cnf(t443,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t39319]) ).
cnf(t444,plain,
one = converse(one),
inference(cp,[status(thm)],[t443,t28]) ).
cnf(t451,plain,
converse(one) = one,
inference(orient,[status(thm)],[t444]) ).
cnf(t628,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t620,t451]) ).
cnf(t39320,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t443,t451]) ).
cnf(t462,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t39320]) ).
cnf(t463,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t462]) ).
cnf(t39344,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t628,t463]) ).
cnf(t39345,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t39344,t463]) ).
cnf(t653,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t39345]) ).
cnf(t667,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t297,t653]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t141,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t39407,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t667,t141]) ).
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(t39289,plain,
complement(top) = zero,
inference(step,[status(thm)],[t33,t141]) ).
cnf(t145,plain,
complement(top) = zero,
inference(rw,[status(thm)],[t39289]) ).
cnf(t214,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t145]) ).
cnf(t39408,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t39407,t214]) ).
cnf(t39409,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t39408,t136]) ).
cnf(t785,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t39409]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t146,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t657,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t653,t214]) ).
cnf(t39352,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t657,t214]) ).
cnf(t39353,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t39352,t214]) ).
cnf(t689,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t39353]) ).
cnf(t690,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t146,t689]) ).
cnf(t881,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t690]) ).
cnf(t887,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t881,t785]) ).
cnf(t39454,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t887,t785]) ).
cnf(t997,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t39454]) ).
cnf(t39461,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t785,t997]) ).
cnf(t1019,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t39461]) ).
cnf(t1114,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1019]) ).
cnf(t300,plain,
X1 = join(complement(join(X2,complement(X1))),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t297,t136]) ).
cnf(t29132,plain,
join(complement(join(X1,complement(X2))),complement(join(complement(X2),complement(X1)))) = X2,
inference(orient,[status(thm)],[t300]) ).
cnf(t306,plain,
sk1 = join(complement(join(sFlat0,X1)),complement(join(complement(sk1),complement(X1)))),
inference(cp,[status(thm)],[t297,t109]) ).
cnf(t41025,plain,
sk1 = join(complement(join(sFlat0,X1)),complement(join(sFlat0,complement(X1)))),
inference(step,[status(thm)],[t306,t109]) ).
cnf(t35364,plain,
join(complement(join(sFlat0,X1)),complement(join(sFlat0,complement(X1)))) = sk1,
inference(orient,[status(thm)],[t41025]) ).
cnf(t35427,plain,
join(sFlat0,X1) = join(complement(join(join(sFlat0,complement(X1)),complement(join(sFlat0,X1)))),complement(sk1)),
inference(cp,[status(thm)],[t29132,t35364]) ).
cnf(t41275,plain,
join(sFlat0,X1) = join(complement(sk1),complement(join(join(sFlat0,complement(X1)),complement(join(sFlat0,X1))))),
inference(step,[status(thm)],[t35427,t136]) ).
cnf(t41276,plain,
join(sFlat0,X1) = join(sFlat0,complement(join(join(sFlat0,complement(X1)),complement(join(sFlat0,X1))))),
inference(step,[status(thm)],[t41275,t109]) ).
cnf(t41277,plain,
join(sFlat0,X1) = join(sFlat0,complement(join(sFlat0,join(complement(X1),complement(join(sFlat0,X1)))))),
inference(step,[status(thm)],[t41276,t146]) ).
cnf(t1115,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t653,t1114]) ).
cnf(t39500,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1115,t1114]) ).
cnf(t39501,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t39500,t1114]) ).
cnf(t1143,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t39501]) ).
cnf(t1157,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t146,t1143]) ).
cnf(t1389,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1157]) ).
cnf(t1399,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = join(complement(join(complement(X1),X2)),X1),
inference(cp,[status(thm)],[t1389,t297]) ).
cnf(t39661,plain,
X1 = join(complement(join(complement(X1),X2)),X1),
inference(step,[status(thm)],[t1399,t297]) ).
cnf(t39662,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t39661,t136]) ).
cnf(t2561,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t39662]) ).
cnf(t2564,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(cp,[status(thm)],[t2561,t136]) ).
cnf(t4316,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t2564]) ).
cnf(t4339,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t4316,t1114]) ).
cnf(t9669,plain,
join(complement(X1),complement(join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t4339]) ).
cnf(t41278,plain,
join(sFlat0,X1) = join(sFlat0,complement(join(sFlat0,complement(X1)))),
inference(step,[status(thm)],[t41277,t9669]) ).
cnf(t39076,plain,
join(sFlat0,complement(join(sFlat0,complement(X1)))) = join(sFlat0,X1),
inference(orient,[status(thm)],[t41278]) ).
cnf(t39077,plain,
join(sFlat0,complement(X1)) = join(sFlat0,complement(join(sFlat0,X1))),
inference(cp,[status(thm)],[t39076,t1114]) ).
cnf(t39098,plain,
join(sFlat0,complement(join(sFlat0,X1))) = join(sFlat0,complement(X1)),
inference(orient,[status(thm)],[t39077]) ).
cnf(t150,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t146,t136]) ).
cnf(t39619,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t150,t146]) ).
cnf(t2119,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t39619]) ).
cnf(t2568,plain,
complement(X1) = join(complement(X1),complement(join(X1,X2))),
inference(cp,[status(thm)],[t2561,t1114]) ).
cnf(t9482,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t2568]) ).
cnf(u1,axiom,
join(meet(composition(A,B),C),composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
join(complement(join(complement(composition(X1,X2)),complement(X3))),composition(complement(join(complement(X1),complement(composition(X3,converse(X2))))),complement(join(complement(X2),complement(composition(converse(X1),X3)))))) = composition(complement(join(complement(X1),complement(composition(X3,converse(X2))))),complement(join(complement(X2),complement(composition(converse(X1),X3))))),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t151,plain,
join(complement(join(complement(composition(X1,X2)),complement(X3))),composition(complement(join(complement(X1),complement(composition(X3,converse(X2))))),complement(join(complement(X2),complement(composition(converse(X1),X3)))))) = composition(complement(join(complement(X1),complement(composition(X3,converse(X2))))),complement(join(complement(X2),complement(composition(converse(X1),X3))))),
inference(orient,[status(thm)],[t15]) ).
cnf(t163,plain,
composition(complement(join(complement(X1),complement(composition(X2,converse(converse(X3)))))),complement(join(complement(converse(X3)),complement(composition(converse(X1),X2))))) = join(complement(join(complement(composition(X1,converse(X3))),complement(X2))),composition(complement(join(complement(X1),complement(composition(X2,X3)))),complement(join(complement(converse(X3)),complement(composition(converse(X1),X2)))))),
inference(cp,[status(thm)],[t151,t29]) ).
cnf(t39668,plain,
composition(complement(join(complement(X1),complement(composition(X2,X3)))),complement(join(complement(converse(X3)),complement(composition(converse(X1),X2))))) = join(complement(join(complement(composition(X1,converse(X3))),complement(X2))),composition(complement(join(complement(X1),complement(composition(X2,X3)))),complement(join(complement(converse(X3)),complement(composition(converse(X1),X2)))))),
inference(step,[status(thm)],[t163,t29]) ).
cnf(t2803,plain,
join(complement(join(complement(composition(X1,converse(X2))),complement(X3))),composition(complement(join(complement(X1),complement(composition(X3,X2)))),complement(join(complement(converse(X2)),complement(composition(converse(X1),X3)))))) = composition(complement(join(complement(X1),complement(composition(X3,X2)))),complement(join(complement(converse(X2)),complement(composition(converse(X1),X3))))),
inference(orient,[status(thm)],[t39668]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t203,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t647,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t620,t203]) ).
cnf(t39557,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t647,t214]) ).
cnf(t39558,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t39557,t214]) ).
cnf(t39559,plain,
zero = composition(converse(sk1),complement(sk1)),
inference(step,[status(thm)],[t39558,t997]) ).
cnf(t39560,plain,
zero = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t39559,t109]) ).
cnf(t1812,plain,
composition(converse(sk1),sFlat0) = zero,
inference(orient,[status(thm)],[t39560]) ).
cnf(t1816,plain,
composition(converse(sFlat0),sk1) = converse(zero),
inference(cp,[status(thm)],[t427,t1812]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t178,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t181,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t178,t29]) ).
cnf(t403,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t181]) ).
cnf(t1011,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t403,t997]) ).
cnf(t39549,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t1011,t29]) ).
cnf(t1226,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t39549]) ).
cnf(t1000,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t997,t136]) ).
cnf(t1107,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t1000]) ).
cnf(t1227,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t1226,t1107]) ).
cnf(t1236,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t1227]) ).
cnf(t39561,plain,
composition(converse(sFlat0),sk1) = zero,
inference(step,[status(thm)],[t1816,t1236]) ).
cnf(t1818,plain,
composition(converse(sFlat0),sk1) = zero,
inference(orient,[status(thm)],[t39561]) ).
cnf(t2946,plain,
composition(complement(join(complement(sFlat0),complement(composition(sk1,X1)))),complement(join(complement(converse(X1)),complement(composition(converse(sFlat0),sk1))))) = join(complement(join(complement(composition(sFlat0,converse(X1))),complement(sk1))),composition(complement(join(complement(sFlat0),complement(composition(sk1,X1)))),complement(join(complement(converse(X1)),complement(zero))))),
inference(cp,[status(thm)],[t2803,t1818]) ).
cnf(t790,plain,
sk1 = join(zero,complement(sFlat0)),
inference(cp,[status(thm)],[t785,t109]) ).
cnf(t800,plain,
join(zero,complement(sFlat0)) = sk1,
inference(orient,[status(thm)],[t790]) ).
cnf(t39455,plain,
complement(sFlat0) = sk1,
inference(step,[status(thm)],[t800,t997]) ).
cnf(t1013,plain,
complement(sFlat0) = sk1,
inference(rw,[status(thm)],[t39455]) ).
cnf(t1030,plain,
complement(sFlat0) = sk1,
inference(orient,[status(thm)],[t1013]) ).
cnf(t40184,plain,
composition(complement(join(sk1,complement(composition(sk1,X1)))),complement(join(complement(converse(X1)),complement(composition(converse(sFlat0),sk1))))) = join(complement(join(complement(composition(sFlat0,converse(X1))),complement(sk1))),composition(complement(join(complement(sFlat0),complement(composition(sk1,X1)))),complement(join(complement(converse(X1)),complement(zero))))),
inference(step,[status(thm)],[t2946,t1030]) ).
cnf(t180,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t178,t29]) ).
cnf(t393,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t180]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t175,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t147,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t146,t141]) ).
cnf(t903,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t147]) ).
cnf(t1159,plain,
top = join(X1,join(X1,complement(X1))),
inference(cp,[status(thm)],[t903,t1143]) ).
cnf(t39502,plain,
top = join(X1,top),
inference(step,[status(thm)],[t1159,t141]) ).
cnf(t1163,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t39502]) ).
cnf(t1164,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t1163,t136]) ).
cnf(t1171,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t1164]) ).
cnf(t394,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t393,t141]) ).
cnf(t495,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t394]) ).
cnf(t1200,plain,
top = converse(top),
inference(cp,[status(thm)],[t1171,t495]) ).
cnf(t1211,plain,
converse(top) = top,
inference(orient,[status(thm)],[t1200]) ).
cnf(t1216,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t194,t1211]) ).
cnf(t1253,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t1216]) ).
cnf(t1256,plain,
composition(top,converse(sk1)) = converse(sk1),
inference(cp,[status(thm)],[t1253,t203]) ).
cnf(t1270,plain,
composition(top,converse(sk1)) = converse(sk1),
inference(orient,[status(thm)],[t1256]) ).
cnf(t1272,plain,
composition(join(top,X1),converse(sk1)) = join(converse(sk1),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t175,t1270]) ).
cnf(t40000,plain,
composition(top,converse(sk1)) = join(converse(sk1),composition(X1,converse(sk1))),
inference(step,[status(thm)],[t1272,t1171]) ).
cnf(t40001,plain,
converse(sk1) = join(converse(sk1),composition(X1,converse(sk1))),
inference(step,[status(thm)],[t40000,t1270]) ).
cnf(t9452,plain,
join(converse(sk1),composition(X1,converse(sk1))) = converse(sk1),
inference(orient,[status(thm)],[t40001]) ).
cnf(t9456,plain,
join(sk1,converse(composition(X1,converse(sk1)))) = converse(converse(sk1)),
inference(cp,[status(thm)],[t393,t9452]) ).
cnf(t195,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t194,t29]) ).
cnf(t414,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t195]) ).
cnf(t40002,plain,
join(sk1,composition(sk1,converse(X1))) = converse(converse(sk1)),
inference(step,[status(thm)],[t9456,t414]) ).
cnf(t40003,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(step,[status(thm)],[t40002,t29]) ).
cnf(t9461,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(orient,[status(thm)],[t40003]) ).
cnf(t9465,plain,
sk1 = join(sk1,composition(sk1,X1)),
inference(cp,[status(thm)],[t9461,t29]) ).
cnf(t9475,plain,
join(sk1,composition(sk1,X1)) = sk1,
inference(orient,[status(thm)],[t9465]) ).
cnf(t9476,plain,
join(sk1,join(composition(sk1,X1),X2)) = join(sk1,X2),
inference(cp,[status(thm)],[t146,t9475]) ).
cnf(t13865,plain,
join(sk1,join(composition(sk1,X1),X2)) = join(sk1,X2),
inference(orient,[status(thm)],[t9476]) ).
cnf(t13890,plain,
join(sk1,complement(composition(sk1,X1))) = join(sk1,top),
inference(cp,[status(thm)],[t13865,t141]) ).
cnf(t40093,plain,
join(sk1,complement(composition(sk1,X1))) = top,
inference(step,[status(thm)],[t13890,t1163]) ).
cnf(t13913,plain,
join(sk1,complement(composition(sk1,X1))) = top,
inference(orient,[status(thm)],[t40093]) ).
cnf(t40185,plain,
composition(complement(top),complement(join(complement(converse(X1)),complement(composition(converse(sFlat0),sk1))))) = join(complement(join(complement(composition(sFlat0,converse(X1))),complement(sk1))),composition(complement(join(complement(sFlat0),complement(composition(sk1,X1)))),complement(join(complement(converse(X1)),complement(zero))))),
inference(step,[status(thm)],[t40184,t13913]) ).
cnf(t40186,plain,
composition(zero,complement(join(complement(converse(X1)),complement(composition(converse(sFlat0),sk1))))) = join(complement(join(complement(composition(sFlat0,converse(X1))),complement(sk1))),composition(complement(join(complement(sFlat0),complement(composition(sk1,X1)))),complement(join(complement(converse(X1)),complement(zero))))),
inference(step,[status(thm)],[t40185,t214]) ).
cnf(t1238,plain,
converse(composition(zero,X1)) = composition(converse(X1),zero),
inference(cp,[status(thm)],[t194,t1236]) ).
cnf(t1303,plain,
converse(composition(zero,X1)) = composition(converse(X1),zero),
inference(orient,[status(thm)],[t1238]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t183,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t1819,plain,
composition(converse(sFlat0),composition(sk1,X1)) = composition(zero,X1),
inference(cp,[status(thm)],[t183,t1818]) ).
cnf(t2042,plain,
composition(converse(sFlat0),composition(sk1,X1)) = composition(zero,X1),
inference(orient,[status(thm)],[t1819]) ).
cnf(t2043,plain,
composition(zero,top) = composition(converse(sFlat0),sk1),
inference(cp,[status(thm)],[t2042,t203]) ).
cnf(t39593,plain,
composition(zero,top) = zero,
inference(step,[status(thm)],[t2043,t1818]) ).
cnf(t2051,plain,
composition(zero,top) = zero,
inference(orient,[status(thm)],[t39593]) ).
cnf(t2052,plain,
composition(converse(top),zero) = converse(zero),
inference(cp,[status(thm)],[t1303,t2051]) ).
cnf(t39594,plain,
composition(top,zero) = converse(zero),
inference(step,[status(thm)],[t2052,t1211]) ).
cnf(t39595,plain,
composition(top,zero) = zero,
inference(step,[status(thm)],[t39594,t1236]) ).
cnf(t2055,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t39595]) ).
cnf(t2057,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t175,t2055]) ).
cnf(t39596,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t2057,t1171]) ).
cnf(t39597,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t39596,t2055]) ).
cnf(t39598,plain,
zero = composition(X1,zero),
inference(step,[status(thm)],[t39597,t997]) ).
cnf(t2059,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t39598]) ).
cnf(t2063,plain,
composition(converse(zero),X1) = converse(zero),
inference(cp,[status(thm)],[t427,t2059]) ).
cnf(t39603,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t2063,t1236]) ).
cnf(t39604,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t39603,t1236]) ).
cnf(t2065,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t39604]) ).
cnf(t40187,plain,
zero = join(complement(join(complement(composition(sFlat0,converse(X1))),complement(sk1))),composition(complement(join(complement(sFlat0),complement(composition(sk1,X1)))),complement(join(complement(converse(X1)),complement(zero))))),
inference(step,[status(thm)],[t40186,t2065]) ).
cnf(t40188,plain,
zero = join(complement(join(complement(sk1),complement(composition(sFlat0,converse(X1))))),composition(complement(join(complement(sFlat0),complement(composition(sk1,X1)))),complement(join(complement(converse(X1)),complement(zero))))),
inference(step,[status(thm)],[t40187,t136]) ).
cnf(t40189,plain,
zero = join(complement(join(sFlat0,complement(composition(sFlat0,converse(X1))))),composition(complement(join(complement(sFlat0),complement(composition(sk1,X1)))),complement(join(complement(converse(X1)),complement(zero))))),
inference(step,[status(thm)],[t40188,t109]) ).
cnf(t40190,plain,
zero = join(complement(join(sFlat0,complement(composition(sFlat0,converse(X1))))),composition(complement(join(sk1,complement(composition(sk1,X1)))),complement(join(complement(converse(X1)),complement(zero))))),
inference(step,[status(thm)],[t40189,t1030]) ).
cnf(t40191,plain,
zero = join(complement(join(sFlat0,complement(composition(sFlat0,converse(X1))))),composition(complement(top),complement(join(complement(converse(X1)),complement(zero))))),
inference(step,[status(thm)],[t40190,t13913]) ).
cnf(t40192,plain,
zero = join(complement(join(sFlat0,complement(composition(sFlat0,converse(X1))))),composition(zero,complement(join(complement(converse(X1)),complement(zero))))),
inference(step,[status(thm)],[t40191,t214]) ).
cnf(t40193,plain,
zero = join(complement(join(sFlat0,complement(composition(sFlat0,converse(X1))))),zero),
inference(step,[status(thm)],[t40192,t2065]) ).
cnf(t40194,plain,
zero = complement(join(sFlat0,complement(composition(sFlat0,converse(X1))))),
inference(step,[status(thm)],[t40193,t1107]) ).
cnf(t16889,plain,
complement(join(sFlat0,complement(composition(sFlat0,converse(X1))))) = zero,
inference(orient,[status(thm)],[t40194]) ).
cnf(t16895,plain,
zero = complement(join(sFlat0,complement(composition(sFlat0,X1)))),
inference(cp,[status(thm)],[t16889,t29]) ).
cnf(t16928,plain,
complement(join(sFlat0,complement(composition(sFlat0,X1)))) = zero,
inference(orient,[status(thm)],[t16895]) ).
cnf(t16929,plain,
join(sFlat0,complement(composition(sFlat0,X1))) = complement(zero),
inference(cp,[status(thm)],[t1114,t16928]) ).
cnf(t998,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t997,t141]) ).
cnf(t1020,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t998]) ).
cnf(t40195,plain,
join(sFlat0,complement(composition(sFlat0,X1))) = top,
inference(step,[status(thm)],[t16929,t1020]) ).
cnf(t16958,plain,
join(sFlat0,complement(composition(sFlat0,X1))) = top,
inference(orient,[status(thm)],[t40195]) ).
cnf(t29278,plain,
composition(sFlat0,X1) = join(complement(top),complement(join(complement(composition(sFlat0,X1)),complement(sFlat0)))),
inference(cp,[status(thm)],[t29132,t16958]) ).
cnf(t40758,plain,
composition(sFlat0,X1) = join(zero,complement(join(complement(composition(sFlat0,X1)),complement(sFlat0)))),
inference(step,[status(thm)],[t29278,t214]) ).
cnf(t40759,plain,
composition(sFlat0,X1) = complement(join(complement(composition(sFlat0,X1)),complement(sFlat0))),
inference(step,[status(thm)],[t40758,t997]) ).
cnf(t40760,plain,
composition(sFlat0,X1) = complement(join(complement(sFlat0),complement(composition(sFlat0,X1)))),
inference(step,[status(thm)],[t40759,t136]) ).
cnf(t40761,plain,
composition(sFlat0,X1) = complement(join(sk1,complement(composition(sFlat0,X1)))),
inference(step,[status(thm)],[t40760,t1030]) ).
cnf(t30112,plain,
complement(join(sk1,complement(composition(sFlat0,X1)))) = composition(sFlat0,X1),
inference(orient,[status(thm)],[t40761]) ).
cnf(t30117,plain,
complement(sk1) = join(complement(sk1),composition(sFlat0,X1)),
inference(cp,[status(thm)],[t9482,t30112]) ).
cnf(t40762,plain,
sFlat0 = join(complement(sk1),composition(sFlat0,X1)),
inference(step,[status(thm)],[t30117,t109]) ).
cnf(t40763,plain,
sFlat0 = join(sFlat0,composition(sFlat0,X1)),
inference(step,[status(thm)],[t40762,t109]) ).
cnf(t30156,plain,
join(sFlat0,composition(sFlat0,X1)) = sFlat0,
inference(orient,[status(thm)],[t40763]) ).
cnf(t30166,plain,
join(sFlat0,join(X1,composition(sFlat0,X2))) = join(X1,sFlat0),
inference(cp,[status(thm)],[t2119,t30156]) ).
cnf(t30855,plain,
join(sFlat0,join(X1,composition(sFlat0,X2))) = join(X1,sFlat0),
inference(orient,[status(thm)],[t30166]) ).
cnf(t211,plain,
composition(join(X1,sk2),sk3) = join(composition(X1,sk3),sFlat5),
inference(cp,[status(thm)],[t175,t208]) ).
cnf(t39328,plain,
composition(join(X1,sk2),sk3) = join(sFlat5,composition(X1,sk3)),
inference(step,[status(thm)],[t211,t136]) ).
cnf(t547,plain,
composition(join(X1,sk2),sk3) = join(sFlat5,composition(X1,sk3)),
inference(orient,[status(thm)],[t39328]) ).
cnf(t301,plain,
sFlat2 = join(complement(join(sFlat3,X1)),complement(join(complement(sFlat2),complement(X1)))),
inference(cp,[status(thm)],[t297,t239]) ).
cnf(t40764,plain,
sFlat2 = join(complement(join(sFlat3,X1)),complement(join(sFlat3,complement(X1)))),
inference(step,[status(thm)],[t301,t239]) ).
cnf(t30956,plain,
join(complement(join(sFlat3,X1)),complement(join(sFlat3,complement(X1)))) = sFlat2,
inference(orient,[status(thm)],[t40764]) ).
cnf(t31007,plain,
join(sFlat3,X1) = join(complement(join(join(sFlat3,complement(X1)),complement(join(sFlat3,X1)))),complement(sFlat2)),
inference(cp,[status(thm)],[t29132,t30956]) ).
cnf(t40771,plain,
join(sFlat3,X1) = join(complement(sFlat2),complement(join(join(sFlat3,complement(X1)),complement(join(sFlat3,X1))))),
inference(step,[status(thm)],[t31007,t136]) ).
cnf(t40772,plain,
join(sFlat3,X1) = join(sFlat3,complement(join(join(sFlat3,complement(X1)),complement(join(sFlat3,X1))))),
inference(step,[status(thm)],[t40771,t239]) ).
cnf(t40773,plain,
join(sFlat3,X1) = join(sFlat3,complement(join(sFlat3,join(complement(X1),complement(join(sFlat3,X1)))))),
inference(step,[status(thm)],[t40772,t146]) ).
cnf(t40774,plain,
join(sFlat3,X1) = join(sFlat3,complement(join(sFlat3,complement(X1)))),
inference(step,[status(thm)],[t40773,t9669]) ).
cnf(t31072,plain,
join(sFlat3,complement(join(sFlat3,complement(X1)))) = join(sFlat3,X1),
inference(orient,[status(thm)],[t40774]) ).
cnf(t31079,plain,
join(sFlat3,complement(X1)) = join(sFlat3,complement(join(sFlat3,X1))),
inference(cp,[status(thm)],[t31072,t1114]) ).
cnf(t31192,plain,
join(sFlat3,complement(join(sFlat3,X1))) = join(sFlat3,complement(X1)),
inference(orient,[status(thm)],[t31079]) ).
cnf(t35392,plain,
sk1 = join(complement(sFlat2),complement(join(sFlat0,complement(sFlat1)))),
inference(cp,[status(thm)],[t35364,t173]) ).
cnf(t41062,plain,
sk1 = join(sFlat3,complement(join(sFlat0,complement(sFlat1)))),
inference(step,[status(thm)],[t35392,t239]) ).
cnf(t789,plain,
sk2 = join(zero,complement(sFlat1)),
inference(cp,[status(thm)],[t785,t123]) ).
cnf(t798,plain,
join(zero,complement(sFlat1)) = sk2,
inference(orient,[status(thm)],[t789]) ).
cnf(t39456,plain,
complement(sFlat1) = sk2,
inference(step,[status(thm)],[t798,t997]) ).
cnf(t1014,plain,
complement(sFlat1) = sk2,
inference(rw,[status(thm)],[t39456]) ).
cnf(t1040,plain,
complement(sFlat1) = sk2,
inference(orient,[status(thm)],[t1014]) ).
cnf(t41063,plain,
sk1 = join(sFlat3,complement(join(sFlat0,sk2))),
inference(step,[status(thm)],[t41062,t1040]) ).
cnf(t35802,plain,
join(sFlat3,complement(join(sFlat0,sk2))) = sk1,
inference(orient,[status(thm)],[t41063]) ).
cnf(t35806,plain,
join(sFlat3,complement(complement(join(sFlat0,sk2)))) = join(sFlat3,complement(sk1)),
inference(cp,[status(thm)],[t31192,t35802]) ).
cnf(t41064,plain,
join(sFlat3,join(sFlat0,sk2)) = join(sFlat3,complement(sk1)),
inference(step,[status(thm)],[t35806,t1114]) ).
cnf(t2577,plain,
sk2 = join(sk2,complement(join(sFlat1,X1))),
inference(cp,[status(thm)],[t2561,t123]) ).
cnf(t2736,plain,
join(sk2,complement(join(sFlat1,X1))) = sk2,
inference(orient,[status(thm)],[t2577]) ).
cnf(t174,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t146,t173]) ).
cnf(t257,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t174]) ).
cnf(t260,plain,
join(sFlat2,X1) = join(sFlat0,join(X1,sFlat1)),
inference(cp,[status(thm)],[t257,t136]) ).
cnf(t348,plain,
join(sFlat0,join(X1,sFlat1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t260]) ).
cnf(t658,plain,
complement(sk2) = join(sFlat1,complement(sk2)),
inference(cp,[status(thm)],[t653,t123]) ).
cnf(t39354,plain,
sFlat1 = join(sFlat1,complement(sk2)),
inference(step,[status(thm)],[t658,t123]) ).
cnf(t39355,plain,
sFlat1 = join(sFlat1,sFlat1),
inference(step,[status(thm)],[t39354,t123]) ).
cnf(t691,plain,
join(sFlat1,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t39355]) ).
cnf(t692,plain,
join(sFlat2,sFlat1) = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t348,t691]) ).
cnf(t39376,plain,
join(sFlat1,sFlat2) = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t692,t136]) ).
cnf(t39377,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t39376,t173]) ).
cnf(t727,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t39377]) ).
cnf(t2739,plain,
sk2 = join(sk2,complement(sFlat2)),
inference(cp,[status(thm)],[t2736,t727]) ).
cnf(t39664,plain,
sk2 = join(sk2,sFlat3),
inference(step,[status(thm)],[t2739,t239]) ).
cnf(t39665,plain,
sk2 = join(sFlat3,sk2),
inference(step,[status(thm)],[t39664,t136]) ).
cnf(t2749,plain,
join(sFlat3,sk2) = sk2,
inference(orient,[status(thm)],[t39665]) ).
cnf(t2755,plain,
join(sFlat3,join(X1,sk2)) = join(X1,sk2),
inference(cp,[status(thm)],[t2119,t2749]) ).
cnf(t2779,plain,
join(sFlat3,join(X1,sk2)) = join(X1,sk2),
inference(orient,[status(thm)],[t2755]) ).
cnf(t41065,plain,
join(sFlat0,sk2) = join(sFlat3,complement(sk1)),
inference(step,[status(thm)],[t41064,t2779]) ).
cnf(t41066,plain,
join(sFlat0,sk2) = join(sFlat3,sFlat0),
inference(step,[status(thm)],[t41065,t109]) ).
cnf(t41067,plain,
join(sFlat0,sk2) = join(sFlat0,sFlat3),
inference(step,[status(thm)],[t41066,t136]) ).
cnf(t35818,plain,
join(sFlat0,sk2) = join(sFlat0,sFlat3),
inference(orient,[status(thm)],[t41067]) ).
cnf(t35826,plain,
join(sFlat5,composition(sFlat0,sk3)) = composition(join(sFlat0,sFlat3),sk3),
inference(cp,[status(thm)],[t547,t35818]) ).
cnf(t250,plain,
composition(join(X1,sFlat3),sk3) = join(composition(X1,sk3),sFlat4),
inference(cp,[status(thm)],[t175,t247]) ).
cnf(t39329,plain,
composition(join(X1,sFlat3),sk3) = join(sFlat4,composition(X1,sk3)),
inference(step,[status(thm)],[t250,t136]) ).
cnf(t562,plain,
composition(join(X1,sFlat3),sk3) = join(sFlat4,composition(X1,sk3)),
inference(orient,[status(thm)],[t39329]) ).
cnf(t41086,plain,
join(sFlat5,composition(sFlat0,sk3)) = join(sFlat4,composition(sFlat0,sk3)),
inference(step,[status(thm)],[t35826,t562]) ).
cnf(t36227,plain,
join(sFlat5,composition(sFlat0,sk3)) = join(sFlat4,composition(sFlat0,sk3)),
inference(orient,[status(thm)],[t41086]) ).
cnf(t36231,plain,
join(sFlat5,sFlat0) = join(sFlat0,join(sFlat4,composition(sFlat0,sk3))),
inference(cp,[status(thm)],[t30855,t36227]) ).
cnf(t41089,plain,
join(sFlat0,sFlat5) = join(sFlat0,join(sFlat4,composition(sFlat0,sk3))),
inference(step,[status(thm)],[t36231,t136]) ).
cnf(t41090,plain,
join(sFlat0,sFlat5) = join(sFlat4,sFlat0),
inference(step,[status(thm)],[t41089,t30855]) ).
cnf(t41091,plain,
join(sFlat0,sFlat5) = join(sFlat0,sFlat4),
inference(step,[status(thm)],[t41090,t136]) ).
cnf(t36257,plain,
join(sFlat0,sFlat5) = join(sFlat0,sFlat4),
inference(orient,[status(thm)],[t41091]) ).
cnf(t39106,plain,
join(sFlat0,complement(sFlat5)) = join(sFlat0,complement(join(sFlat0,sFlat4))),
inference(cp,[status(thm)],[t39098,t36257]) ).
cnf(t41281,plain,
join(sFlat0,sFlat6) = join(sFlat0,complement(join(sFlat0,sFlat4))),
inference(step,[status(thm)],[t39106,t219]) ).
cnf(t41282,plain,
sFlat7 = join(sFlat0,complement(join(sFlat0,sFlat4))),
inference(step,[status(thm)],[t41281,t171]) ).
cnf(t41283,plain,
sFlat7 = join(sFlat0,complement(sFlat4)),
inference(step,[status(thm)],[t41282,t39098]) ).
cnf(t9479,plain,
join(sk1,join(X1,composition(sk1,X2))) = join(X1,sk1),
inference(cp,[status(thm)],[t2119,t9475]) ).
cnf(t13922,plain,
join(sk1,join(X1,composition(sk1,X2))) = join(X1,sk1),
inference(orient,[status(thm)],[t9479]) ).
cnf(t249,plain,
composition(join(sFlat3,X1),sk3) = join(sFlat4,composition(X1,sk3)),
inference(cp,[status(thm)],[t175,t247]) ).
cnf(t554,plain,
composition(join(sFlat3,X1),sk3) = join(sFlat4,composition(X1,sk3)),
inference(orient,[status(thm)],[t249]) ).
cnf(t2578,plain,
sk1 = join(sk1,complement(join(sFlat0,X1))),
inference(cp,[status(thm)],[t2561,t109]) ).
cnf(t2992,plain,
join(sk1,complement(join(sFlat0,X1))) = sk1,
inference(orient,[status(thm)],[t2578]) ).
cnf(t786,plain,
sFlat2 = join(zero,complement(sFlat3)),
inference(cp,[status(thm)],[t785,t239]) ).
cnf(t792,plain,
join(zero,complement(sFlat3)) = sFlat2,
inference(orient,[status(thm)],[t786]) ).
cnf(t39459,plain,
complement(sFlat3) = sFlat2,
inference(step,[status(thm)],[t792,t997]) ).
cnf(t1017,plain,
complement(sFlat3) = sFlat2,
inference(rw,[status(thm)],[t39459]) ).
cnf(t1075,plain,
complement(sFlat3) = sFlat2,
inference(orient,[status(thm)],[t1017]) ).
cnf(t1076,plain,
complement(sFlat3) = join(sFlat2,complement(sFlat3)),
inference(cp,[status(thm)],[t653,t1075]) ).
cnf(t39495,plain,
sFlat2 = join(sFlat2,complement(sFlat3)),
inference(step,[status(thm)],[t1076,t1075]) ).
cnf(t39496,plain,
sFlat2 = join(sFlat2,sFlat2),
inference(step,[status(thm)],[t39495,t1075]) ).
cnf(t728,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t257,t727]) ).
cnf(t783,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(orient,[status(thm)],[t728]) ).
cnf(t39497,plain,
sFlat2 = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t39496,t783]) ).
cnf(t1139,plain,
join(sFlat0,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t39497]) ).
cnf(t2997,plain,
sk1 = join(sk1,complement(sFlat2)),
inference(cp,[status(thm)],[t2992,t1139]) ).
cnf(t39669,plain,
sk1 = join(sk1,sFlat3),
inference(step,[status(thm)],[t2997,t239]) ).
cnf(t39670,plain,
sk1 = join(sFlat3,sk1),
inference(step,[status(thm)],[t39669,t136]) ).
cnf(t3014,plain,
join(sFlat3,sk1) = sk1,
inference(orient,[status(thm)],[t39670]) ).
cnf(t3016,plain,
join(sFlat4,composition(sk1,sk3)) = composition(sk1,sk3),
inference(cp,[status(thm)],[t554,t3014]) ).
cnf(t3043,plain,
join(sFlat4,composition(sk1,sk3)) = composition(sk1,sk3),
inference(orient,[status(thm)],[t3016]) ).
cnf(t13936,plain,
join(sFlat4,sk1) = join(sk1,composition(sk1,sk3)),
inference(cp,[status(thm)],[t13922,t3043]) ).
cnf(t40094,plain,
join(sFlat4,sk1) = sk1,
inference(step,[status(thm)],[t13936,t9475]) ).
cnf(t14164,plain,
join(sFlat4,sk1) = sk1,
inference(orient,[status(thm)],[t40094]) ).
cnf(t14167,plain,
complement(sFlat4) = join(complement(sFlat4),complement(sk1)),
inference(cp,[status(thm)],[t9482,t14164]) ).
cnf(t40095,plain,
complement(sFlat4) = join(complement(sFlat4),sFlat0),
inference(step,[status(thm)],[t14167,t109]) ).
cnf(t40096,plain,
complement(sFlat4) = join(sFlat0,complement(sFlat4)),
inference(step,[status(thm)],[t40095,t136]) ).
cnf(t14173,plain,
join(sFlat0,complement(sFlat4)) = complement(sFlat4),
inference(orient,[status(thm)],[t40096]) ).
cnf(t41284,plain,
sFlat7 = complement(sFlat4),
inference(step,[status(thm)],[t41283,t14173]) ).
cnf(t39154,plain,
complement(sFlat4) = sFlat7,
inference(orient,[status(thm)],[t41284]) ).
cnf(t39155,plain,
sFlat4 = complement(sFlat7),
inference(cp,[status(thm)],[t1114,t39154]) ).
cnf(t41301,plain,
sFlat4 = sFlat8,
inference(step,[status(thm)],[t39155,t232]) ).
cnf(t39212,plain,
sFlat8 = sFlat4,
inference(orient,[status(thm)],[t41301]) ).
cnf(t41302,plain,
complement(sFlat7) = sFlat4,
inference(step,[status(thm)],[t232,t39212]) ).
cnf(t39213,plain,
complement(sFlat7) = sFlat4,
inference(orient,[status(thm)],[t41302]) ).
cnf(u4,negated_conjecture,
composition(meet(sk1,sk2),sk3) != meet(sk1,composition(sk2,sk3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
composition(complement(join(complement(sk1),complement(sk2))),sk3) != complement(join(complement(sk1),complement(composition(sk2,sk3)))),
inference(definition_unfolding,[status(thm)],[u4,d0]) ).
cnf(g0_0,plain,
composition(complement(join(complement(sk2),complement(sk1))),sk3) != complement(join(complement(sk1),complement(composition(sk2,sk3)))),
inference(rw,[status(thm)],[goal_0,t136]) ).
cnf(g0_1,plain,
composition(complement(join(sFlat1,complement(sk1))),sk3) != complement(join(complement(sk1),complement(composition(sk2,sk3)))),
inference(rw,[status(thm)],[g0_0,t123]) ).
cnf(g0_2,plain,
composition(complement(join(sFlat1,sFlat0)),sk3) != complement(join(complement(sk1),complement(composition(sk2,sk3)))),
inference(rw,[status(thm)],[g0_1,t109]) ).
cnf(g0_3,plain,
composition(complement(join(sFlat0,sFlat1)),sk3) != complement(join(complement(sk1),complement(composition(sk2,sk3)))),
inference(rw,[status(thm)],[g0_2,t136]) ).
cnf(g0_4,plain,
composition(complement(sFlat2),sk3) != complement(join(complement(sk1),complement(composition(sk2,sk3)))),
inference(rw,[status(thm)],[g0_3,t173]) ).
cnf(g0_5,plain,
composition(sFlat3,sk3) != complement(join(complement(sk1),complement(composition(sk2,sk3)))),
inference(rw,[status(thm)],[g0_4,t239]) ).
cnf(g0_6,plain,
sFlat4 != complement(join(complement(sk1),complement(composition(sk2,sk3)))),
inference(rw,[status(thm)],[g0_5,t247]) ).
cnf(g0_7,plain,
sFlat4 != complement(join(sFlat0,complement(composition(sk2,sk3)))),
inference(rw,[status(thm)],[g0_6,t109]) ).
cnf(g0_8,plain,
sFlat4 != complement(join(sFlat0,complement(sFlat5))),
inference(rw,[status(thm)],[g0_7,t208]) ).
cnf(g0_9,plain,
sFlat4 != complement(join(sFlat0,sFlat6)),
inference(rw,[status(thm)],[g0_8,t219]) ).
cnf(g0_10,plain,
sFlat4 != complement(sFlat7),
inference(rw,[status(thm)],[g0_9,t171]) ).
cnf(g0_11,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_10,t39213]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL033-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.39 % Computer : n017.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Thu Sep 24 07:24:36 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 26.98/18.21 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.98/18.21 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------