%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL037-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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:35:59 PM UTC 2026
% Result : Unsatisfiable 95.26s 12.57s
% Output : CNFRefutation 95.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 107
% Number of leaves : 25
% Syntax : Number of clauses : 491 ( 491 unt; 0 nHn; 299 RR)
% Number of literals : 491 ( 490 equ; 20 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 17 con; 0-2 aty)
% Number of variables : 251 ( 16 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t13,axiom,
sFlat0 = complement(sk2),
introduced(definition) ).
cnf(t75,plain,
complement(sk2) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sFlat1 = converse(sk1),
introduced(definition) ).
cnf(t120,plain,
converse(sk1) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sFlat2 = complement(converse(sk1)),
introduced(definition) ).
cnf(t59,plain,
complement(converse(sk1)) = sFlat2,
inference(orient,[status(thm)],[t15]) ).
cnf(t30461,plain,
complement(sFlat1) = sFlat2,
inference(step,[status(thm)],[t59,t120]) ).
cnf(t126,plain,
complement(sFlat1) = sFlat2,
inference(rw,[status(thm)],[t30461]) ).
cnf(t151,plain,
complement(sFlat1) = sFlat2,
inference(orient,[status(thm)],[t126]) ).
cnf(t16,axiom,
sFlat3 = join(complement(sk2),complement(converse(sk1))),
introduced(definition) ).
cnf(t30459,plain,
sFlat3 = join(sFlat0,complement(converse(sk1))),
inference(step,[status(thm)],[t16,t75]) ).
cnf(t30460,plain,
sFlat3 = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t30459,t59]) ).
cnf(t105,plain,
join(sFlat0,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t30460]) ).
cnf(t17,axiom,
sFlat4 = complement(join(complement(sk2),complement(converse(sk1)))),
introduced(definition) ).
cnf(t50,plain,
complement(join(complement(sk2),complement(converse(sk1)))) = sFlat4,
inference(orient,[status(thm)],[t17]) ).
cnf(t30452,plain,
complement(join(complement(sk2),sFlat2)) = sFlat4,
inference(step,[status(thm)],[t50,t59]) ).
cnf(t66,plain,
complement(join(complement(sk2),sFlat2)) = sFlat4,
inference(rw,[status(thm)],[t30452]) ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t89,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t30479,plain,
complement(join(sFlat2,complement(sk2))) = sFlat4,
inference(step,[status(thm)],[t66,t89]) ).
cnf(t30480,plain,
complement(join(sFlat2,sFlat0)) = sFlat4,
inference(step,[status(thm)],[t30479,t75]) ).
cnf(t30481,plain,
complement(join(sFlat0,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t30480,t89]) ).
cnf(t30482,plain,
complement(sFlat3) = sFlat4,
inference(step,[status(thm)],[t30481,t105]) ).
cnf(t169,plain,
complement(sFlat3) = sFlat4,
inference(orient,[status(thm)],[t30482]) ).
cnf(t19,axiom,
sFlat6 = complement(sk3),
introduced(definition) ).
cnf(t82,plain,
complement(sk3) = sFlat6,
inference(orient,[status(thm)],[t19]) ).
cnf(t18,axiom,
sFlat5 = complement(sk1),
introduced(definition) ).
cnf(t67,plain,
complement(sk1) = sFlat5,
inference(orient,[status(thm)],[t18]) ).
cnf(t20,axiom,
sFlat7 = join(complement(sk1),complement(sk3)),
introduced(definition) ).
cnf(t30455,plain,
sFlat7 = join(complement(sk3),complement(sk1)),
inference(step,[status(thm)],[t20,t89]) ).
cnf(t30456,plain,
sFlat7 = join(sFlat6,complement(sk1)),
inference(step,[status(thm)],[t30455,t82]) ).
cnf(t30457,plain,
sFlat7 = join(sFlat6,sFlat5),
inference(step,[status(thm)],[t30456,t67]) ).
cnf(t30458,plain,
sFlat7 = join(sFlat5,sFlat6),
inference(step,[status(thm)],[t30457,t89]) ).
cnf(t103,plain,
join(sFlat5,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t30458]) ).
cnf(t21,axiom,
sFlat8 = complement(join(complement(sk1),complement(sk3))),
introduced(definition) ).
cnf(t41,plain,
complement(join(complement(sk1),complement(sk3))) = sFlat8,
inference(orient,[status(thm)],[t21]) ).
cnf(t30453,plain,
complement(join(sFlat5,complement(sk3))) = sFlat8,
inference(step,[status(thm)],[t41,t67]) ).
cnf(t74,plain,
complement(join(sFlat5,complement(sk3))) = sFlat8,
inference(rw,[status(thm)],[t30453]) ).
cnf(t30484,plain,
complement(join(sFlat5,sFlat6)) = sFlat8,
inference(step,[status(thm)],[t74,t82]) ).
cnf(t30485,plain,
complement(sFlat7) = sFlat8,
inference(step,[status(thm)],[t30484,t103]) ).
cnf(t178,plain,
complement(sFlat7) = sFlat8,
inference(orient,[status(thm)],[t30485]) ).
cnf(t22,axiom,
sFlat9 = composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
introduced(definition) ).
cnf(t30462,plain,
sFlat9 = composition(complement(join(sFlat0,complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(step,[status(thm)],[t22,t75]) ).
cnf(t30463,plain,
sFlat9 = composition(complement(join(sFlat0,complement(sFlat1))),complement(join(complement(sk1),complement(sk3)))),
inference(step,[status(thm)],[t30462,t120]) ).
cnf(t30464,plain,
sFlat9 = composition(complement(join(sFlat0,complement(sFlat1))),complement(join(complement(sk3),complement(sk1)))),
inference(step,[status(thm)],[t30463,t89]) ).
cnf(t30465,plain,
sFlat9 = composition(complement(join(sFlat0,complement(sFlat1))),complement(join(sFlat6,complement(sk1)))),
inference(step,[status(thm)],[t30464,t82]) ).
cnf(t30466,plain,
sFlat9 = composition(complement(join(sFlat0,complement(sFlat1))),complement(join(sFlat6,sFlat5))),
inference(step,[status(thm)],[t30465,t67]) ).
cnf(t30467,plain,
sFlat9 = composition(complement(join(sFlat0,complement(sFlat1))),complement(join(sFlat5,sFlat6))),
inference(step,[status(thm)],[t30466,t89]) ).
cnf(t30468,plain,
sFlat9 = composition(complement(join(sFlat0,complement(sFlat1))),complement(sFlat7)),
inference(step,[status(thm)],[t30467,t103]) ).
cnf(t132,plain,
composition(complement(join(sFlat0,complement(sFlat1))),complement(sFlat7)) = sFlat9,
inference(orient,[status(thm)],[t30468]) ).
cnf(t30471,plain,
composition(complement(join(sFlat0,sFlat2)),complement(sFlat7)) = sFlat9,
inference(step,[status(thm)],[t132,t151]) ).
cnf(t30472,plain,
composition(complement(sFlat3),complement(sFlat7)) = sFlat9,
inference(step,[status(thm)],[t30471,t105]) ).
cnf(t153,plain,
composition(complement(sFlat3),complement(sFlat7)) = sFlat9,
inference(rw,[status(thm)],[t30472]) ).
cnf(t30486,plain,
composition(sFlat4,complement(sFlat7)) = sFlat9,
inference(step,[status(thm)],[t153,t169]) ).
cnf(t30487,plain,
composition(sFlat4,sFlat8) = sFlat9,
inference(step,[status(thm)],[t30486,t178]) ).
cnf(t182,plain,
composition(sFlat4,sFlat8) = sFlat9,
inference(orient,[status(thm)],[t30487]) ).
cnf(t23,axiom,
sFlat10 = composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
introduced(definition) ).
cnf(t30469,plain,
sFlat10 = composition(complement(join(sFlat0,complement(converse(sk1)))),sk3),
inference(step,[status(thm)],[t23,t75]) ).
cnf(t30470,plain,
sFlat10 = composition(complement(join(sFlat0,complement(sFlat1))),sk3),
inference(step,[status(thm)],[t30469,t120]) ).
cnf(t136,plain,
composition(complement(join(sFlat0,complement(sFlat1))),sk3) = sFlat10,
inference(orient,[status(thm)],[t30470]) ).
cnf(t30473,plain,
composition(complement(join(sFlat0,sFlat2)),sk3) = sFlat10,
inference(step,[status(thm)],[t136,t151]) ).
cnf(t30474,plain,
composition(complement(sFlat3),sk3) = sFlat10,
inference(step,[status(thm)],[t30473,t105]) ).
cnf(t154,plain,
composition(complement(sFlat3),sk3) = sFlat10,
inference(rw,[status(thm)],[t30474]) ).
cnf(t165,plain,
composition(complement(sFlat3),sk3) = sFlat10,
inference(orient,[status(thm)],[t154]) ).
cnf(t30483,plain,
composition(sFlat4,sk3) = sFlat10,
inference(step,[status(thm)],[t165,t169]) ).
cnf(t171,plain,
composition(sFlat4,sk3) = sFlat10,
inference(rw,[status(thm)],[t30483]) ).
cnf(t174,plain,
composition(sFlat4,sk3) = sFlat10,
inference(orient,[status(thm)],[t171]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t115,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(t27,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t116,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t115,t27]) ).
cnf(t464,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t116]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t112,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t122,plain,
converse(composition(X1,sk1)) = composition(sFlat1,converse(X1)),
inference(cp,[status(thm)],[t115,t120]) ).
cnf(t186,plain,
converse(composition(X1,sk1)) = composition(sFlat1,converse(X1)),
inference(orient,[status(thm)],[t122]) ).
cnf(t121,plain,
sk1 = converse(sFlat1),
inference(cp,[status(thm)],[t27,t120]) ).
cnf(t146,plain,
converse(sFlat1) = sk1,
inference(orient,[status(thm)],[t121]) ).
cnf(t148,plain,
converse(composition(sFlat1,X1)) = composition(converse(X1),sk1),
inference(cp,[status(thm)],[t115,t146]) ).
cnf(t231,plain,
converse(composition(sFlat1,X1)) = composition(converse(X1),sk1),
inference(orient,[status(thm)],[t148]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t91,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(rw,[status(thm)],[t29]) ).
cnf(t30508,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t91,t89]) ).
cnf(t585,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t30508]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t140,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t619,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t585,t140]) ).
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(t32,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t92,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t30454,plain,
complement(top) = zero,
inference(step,[status(thm)],[t32,t92]) ).
cnf(t97,plain,
complement(top) = zero,
inference(rw,[status(thm)],[t30454]) ).
cnf(t144,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t97]) ).
cnf(t30509,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t619,t144]) ).
cnf(t30510,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t30509,t144]) ).
cnf(t30511,plain,
zero = join(zero,composition(sFlat1,complement(sk1))),
inference(step,[status(thm)],[t30510,t120]) ).
cnf(t30512,plain,
zero = join(zero,composition(sFlat1,sFlat5)),
inference(step,[status(thm)],[t30511,t67]) ).
cnf(t626,plain,
join(zero,composition(sFlat1,sFlat5)) = zero,
inference(orient,[status(thm)],[t30512]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t98,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t117,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t115,t27]) ).
cnf(t485,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t117]) ).
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(t486,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t485,t28]) ).
cnf(t30502,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t486,t27]) ).
cnf(t505,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t30502]) ).
cnf(t506,plain,
one = converse(one),
inference(cp,[status(thm)],[t505,t28]) ).
cnf(t510,plain,
converse(one) = one,
inference(orient,[status(thm)],[t506]) ).
cnf(t595,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t585,t510]) ).
cnf(t30503,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t505,t510]) ).
cnf(t519,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t30503]) ).
cnf(t520,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t519]) ).
cnf(t30519,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t595,t520]) ).
cnf(t30520,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t30519,t520]) ).
cnf(t636,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t30520]) ).
cnf(t640,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t636,t144]) ).
cnf(t30527,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t640,t144]) ).
cnf(t30528,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t30527,t144]) ).
cnf(t668,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t30528]) ).
cnf(t669,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t98,t668]) ).
cnf(t856,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t669]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t90,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t24]) ).
cnf(t30493,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t90,t89]) ).
cnf(t252,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t30493]) ).
cnf(t652,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t252,t636]) ).
cnf(t30580,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t652,t92]) ).
cnf(t30581,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t30580,t144]) ).
cnf(t30582,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t30581,t89]) ).
cnf(t748,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t30582]) ).
cnf(t863,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t856,t748]) ).
cnf(t30645,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t863,t748]) ).
cnf(t974,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t30645]) ).
cnf(t30652,plain,
composition(sFlat1,sFlat5) = zero,
inference(step,[status(thm)],[t626,t974]) ).
cnf(t996,plain,
composition(sFlat1,sFlat5) = zero,
inference(rw,[status(thm)],[t30652]) ).
cnf(t1086,plain,
composition(sFlat1,sFlat5) = zero,
inference(orient,[status(thm)],[t996]) ).
cnf(t1087,plain,
composition(converse(sFlat5),sk1) = converse(zero),
inference(cp,[status(thm)],[t231,t1086]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t107,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t110,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t107,t27]) ).
cnf(t437,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t110]) ).
cnf(t988,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t437,t974]) ).
cnf(t30760,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t988,t27]) ).
cnf(t1233,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t30760]) ).
cnf(t977,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t974,t89]) ).
cnf(t1080,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t977]) ).
cnf(t1234,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t1233,t1080]) ).
cnf(t1240,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t1234]) ).
cnf(t30763,plain,
composition(converse(sFlat5),sk1) = zero,
inference(step,[status(thm)],[t1087,t1240]) ).
cnf(t1252,plain,
composition(converse(sFlat5),sk1) = zero,
inference(orient,[status(thm)],[t30763]) ).
cnf(t1254,plain,
composition(join(converse(sFlat5),X1),sk1) = join(zero,composition(X1,sk1)),
inference(cp,[status(thm)],[t112,t1252]) ).
cnf(t30863,plain,
composition(join(converse(sFlat5),X1),sk1) = composition(X1,sk1),
inference(step,[status(thm)],[t1254,t974]) ).
cnf(t2294,plain,
composition(join(converse(sFlat5),X1),sk1) = composition(X1,sk1),
inference(orient,[status(thm)],[t30863]) ).
cnf(t2295,plain,
composition(converse(X1),sk1) = composition(converse(join(sFlat5,X1)),sk1),
inference(cp,[status(thm)],[t2294,t107]) ).
cnf(t5595,plain,
composition(converse(join(sFlat5,X1)),sk1) = composition(converse(X1),sk1),
inference(orient,[status(thm)],[t2295]) ).
cnf(t5614,plain,
composition(sFlat1,converse(converse(join(sFlat5,X1)))) = converse(composition(converse(X1),sk1)),
inference(cp,[status(thm)],[t186,t5595]) ).
cnf(t31086,plain,
composition(sFlat1,join(sFlat5,X1)) = converse(composition(converse(X1),sk1)),
inference(step,[status(thm)],[t5614,t27]) ).
cnf(t31087,plain,
composition(sFlat1,join(sFlat5,X1)) = composition(converse(sk1),X1),
inference(step,[status(thm)],[t31086,t485]) ).
cnf(t31088,plain,
composition(sFlat1,join(sFlat5,X1)) = composition(sFlat1,X1),
inference(step,[status(thm)],[t31087,t120]) ).
cnf(t5636,plain,
composition(sFlat1,join(sFlat5,X1)) = composition(sFlat1,X1),
inference(orient,[status(thm)],[t31088]) ).
cnf(t30654,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t748,t974]) ).
cnf(t998,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t30654]) ).
cnf(t1092,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t998]) ).
cnf(t1093,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t636,t1092]) ).
cnf(t30698,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1093,t1092]) ).
cnf(t30699,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t30698,t1092]) ).
cnf(t1127,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t30699]) ).
cnf(t1145,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t98,t1127]) ).
cnf(t1755,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1145]) ).
cnf(t1762,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = join(complement(join(complement(X1),X2)),X1),
inference(cp,[status(thm)],[t1755,t252]) ).
cnf(t30950,plain,
X1 = join(complement(join(complement(X1),X2)),X1),
inference(step,[status(thm)],[t1762,t252]) ).
cnf(t30951,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t30950,t89]) ).
cnf(t3298,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t30951]) ).
cnf(t754,plain,
sk1 = join(zero,complement(sFlat5)),
inference(cp,[status(thm)],[t748,t67]) ).
cnf(t766,plain,
join(zero,complement(sFlat5)) = sk1,
inference(orient,[status(thm)],[t754]) ).
cnf(t30646,plain,
complement(sFlat5) = sk1,
inference(step,[status(thm)],[t766,t974]) ).
cnf(t990,plain,
complement(sFlat5) = sk1,
inference(rw,[status(thm)],[t30646]) ).
cnf(t1006,plain,
complement(sFlat5) = sk1,
inference(orient,[status(thm)],[t990]) ).
cnf(t3312,plain,
sFlat5 = join(sFlat5,complement(join(sk1,X1))),
inference(cp,[status(thm)],[t3298,t1006]) ).
cnf(t3406,plain,
join(sFlat5,complement(join(sk1,X1))) = sFlat5,
inference(orient,[status(thm)],[t3312]) ).
cnf(t5639,plain,
composition(sFlat1,complement(join(sk1,X1))) = composition(sFlat1,sFlat5),
inference(cp,[status(thm)],[t5636,t3406]) ).
cnf(t31089,plain,
composition(sFlat1,complement(join(sk1,X1))) = zero,
inference(step,[status(thm)],[t5639,t1086]) ).
cnf(t5665,plain,
composition(sFlat1,complement(join(sk1,X1))) = zero,
inference(orient,[status(thm)],[t31089]) ).
cnf(t149,plain,
converse(join(sFlat1,X1)) = join(sk1,converse(X1)),
inference(cp,[status(thm)],[t107,t146]) ).
cnf(t241,plain,
converse(join(sFlat1,X1)) = join(sk1,converse(X1)),
inference(orient,[status(thm)],[t149]) ).
cnf(t100,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t98,t89]) ).
cnf(t1324,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t100]) ).
cnf(t1338,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t1324,t1127]) ).
cnf(t1815,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(orient,[status(thm)],[t1338]) ).
cnf(t3301,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(cp,[status(thm)],[t3298,t1815]) ).
cnf(t5076,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t3301]) ).
cnf(t5112,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t5076,t1092]) ).
cnf(t6146,plain,
join(complement(X1),complement(join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t5112]) ).
cnf(t254,plain,
X1 = join(complement(join(X2,complement(X1))),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t252,t89]) ).
cnf(t19809,plain,
join(complement(join(X1,complement(X2))),complement(join(complement(X2),complement(X1)))) = X2,
inference(orient,[status(thm)],[t254]) ).
cnf(t257,plain,
sFlat1 = join(complement(join(sFlat2,X1)),complement(join(complement(sFlat1),complement(X1)))),
inference(cp,[status(thm)],[t252,t151]) ).
cnf(t31965,plain,
sFlat1 = join(complement(join(sFlat2,X1)),complement(join(sFlat2,complement(X1)))),
inference(step,[status(thm)],[t257,t151]) ).
cnf(t22905,plain,
join(complement(join(sFlat2,X1)),complement(join(sFlat2,complement(X1)))) = sFlat1,
inference(orient,[status(thm)],[t31965]) ).
cnf(t22973,plain,
join(sFlat2,X1) = join(complement(join(join(sFlat2,complement(X1)),complement(join(sFlat2,X1)))),complement(sFlat1)),
inference(cp,[status(thm)],[t19809,t22905]) ).
cnf(t31980,plain,
join(sFlat2,X1) = join(complement(sFlat1),complement(join(join(sFlat2,complement(X1)),complement(join(sFlat2,X1))))),
inference(step,[status(thm)],[t22973,t89]) ).
cnf(t31981,plain,
join(sFlat2,X1) = join(sFlat2,complement(join(join(sFlat2,complement(X1)),complement(join(sFlat2,X1))))),
inference(step,[status(thm)],[t31980,t151]) ).
cnf(t31982,plain,
join(sFlat2,X1) = join(sFlat2,complement(join(sFlat2,join(complement(X1),complement(join(sFlat2,X1)))))),
inference(step,[status(thm)],[t31981,t98]) ).
cnf(t31983,plain,
join(sFlat2,X1) = join(sFlat2,complement(join(sFlat2,complement(X1)))),
inference(step,[status(thm)],[t31982,t6146]) ).
cnf(t23131,plain,
join(sFlat2,complement(join(sFlat2,complement(X1)))) = join(sFlat2,X1),
inference(orient,[status(thm)],[t31983]) ).
cnf(t23134,plain,
join(sFlat2,complement(X1)) = join(sFlat2,complement(join(sFlat2,X1))),
inference(cp,[status(thm)],[t23131,t1092]) ).
cnf(t23385,plain,
join(sFlat2,complement(join(sFlat2,X1))) = join(sFlat2,complement(X1)),
inference(orient,[status(thm)],[t23134]) ).
cnf(t109,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t107,t27]) ).
cnf(t419,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t109]) ).
cnf(t422,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t419,t92]) ).
cnf(t550,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t422]) ).
cnf(t125,plain,
converse(join(X1,sk1)) = join(converse(X1),sFlat1),
inference(cp,[status(thm)],[t107,t120]) ).
cnf(t30491,plain,
converse(join(X1,sk1)) = join(sFlat1,converse(X1)),
inference(step,[status(thm)],[t125,t89]) ).
cnf(t218,plain,
converse(join(X1,sk1)) = join(sFlat1,converse(X1)),
inference(orient,[status(thm)],[t30491]) ).
cnf(t95,plain,
top = join(sk1,sFlat5),
inference(cp,[status(thm)],[t92,t67]) ).
cnf(t30477,plain,
top = join(sFlat5,sk1),
inference(step,[status(thm)],[t95,t89]) ).
cnf(t159,plain,
join(sFlat5,sk1) = top,
inference(orient,[status(thm)],[t30477]) ).
cnf(t160,plain,
join(sFlat5,join(sk1,X1)) = join(top,X1),
inference(cp,[status(thm)],[t98,t159]) ).
cnf(t316,plain,
join(sFlat5,join(sk1,X1)) = join(top,X1),
inference(orient,[status(thm)],[t160]) ).
cnf(t319,plain,
join(top,X1) = join(sFlat5,join(X1,sk1)),
inference(cp,[status(thm)],[t316,t89]) ).
cnf(t392,plain,
join(sFlat5,join(X1,sk1)) = join(top,X1),
inference(orient,[status(thm)],[t319]) ).
cnf(t1007,plain,
complement(sFlat5) = join(sk1,complement(sFlat5)),
inference(cp,[status(thm)],[t636,t1006]) ).
cnf(t30680,plain,
sk1 = join(sk1,complement(sFlat5)),
inference(step,[status(thm)],[t1007,t1006]) ).
cnf(t30681,plain,
sk1 = join(sk1,sk1),
inference(step,[status(thm)],[t30680,t1006]) ).
cnf(t1100,plain,
join(sk1,sk1) = sk1,
inference(orient,[status(thm)],[t30681]) ).
cnf(t1101,plain,
join(top,sk1) = join(sFlat5,sk1),
inference(cp,[status(thm)],[t392,t1100]) ).
cnf(t30700,plain,
join(top,sk1) = top,
inference(step,[status(thm)],[t1101,t159]) ).
cnf(t1148,plain,
join(top,sk1) = top,
inference(orient,[status(thm)],[t30700]) ).
cnf(t1165,plain,
join(sFlat1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t218,t1148]) ).
cnf(t152,plain,
top = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t92,t151]) ).
cnf(t163,plain,
join(sFlat1,sFlat2) = top,
inference(orient,[status(thm)],[t152]) ).
cnf(t164,plain,
join(sFlat1,join(sFlat2,X1)) = join(top,X1),
inference(cp,[status(thm)],[t98,t163]) ).
cnf(t325,plain,
join(sFlat1,join(sFlat2,X1)) = join(top,X1),
inference(orient,[status(thm)],[t164]) ).
cnf(t639,plain,
complement(sFlat1) = join(sFlat2,complement(sFlat1)),
inference(cp,[status(thm)],[t636,t151]) ).
cnf(t30525,plain,
sFlat2 = join(sFlat2,complement(sFlat1)),
inference(step,[status(thm)],[t639,t151]) ).
cnf(t30526,plain,
sFlat2 = join(sFlat2,sFlat2),
inference(step,[status(thm)],[t30525,t151]) ).
cnf(t662,plain,
join(sFlat2,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t30526]) ).
cnf(t667,plain,
join(sFlat2,join(sFlat2,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t98,t662]) ).
cnf(t808,plain,
join(sFlat2,join(sFlat2,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t667]) ).
cnf(t809,plain,
join(sFlat2,converse(complement(converse(sFlat2)))) = join(sFlat2,converse(top)),
inference(cp,[status(thm)],[t808,t550]) ).
cnf(t30602,plain,
converse(top) = join(sFlat2,converse(top)),
inference(step,[status(thm)],[t809,t550]) ).
cnf(t813,plain,
join(sFlat2,converse(top)) = converse(top),
inference(orient,[status(thm)],[t30602]) ).
cnf(t816,plain,
join(top,converse(top)) = join(sFlat1,converse(top)),
inference(cp,[status(thm)],[t325,t813]) ).
cnf(t106,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t98,t105]) ).
cnf(t297,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t106]) ).
cnf(t327,plain,
join(top,X1) = join(sFlat1,join(X1,sFlat2)),
inference(cp,[status(thm)],[t325,t89]) ).
cnf(t402,plain,
join(sFlat1,join(X1,sFlat2)) = join(top,X1),
inference(orient,[status(thm)],[t327]) ).
cnf(t663,plain,
join(top,sFlat2) = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t402,t662]) ).
cnf(t30539,plain,
join(sFlat2,top) = join(sFlat1,sFlat2),
inference(step,[status(thm)],[t663,t89]) ).
cnf(t30540,plain,
join(sFlat2,top) = top,
inference(step,[status(thm)],[t30539,t163]) ).
cnf(t686,plain,
join(sFlat2,top) = top,
inference(orient,[status(thm)],[t30540]) ).
cnf(t691,plain,
join(sFlat3,top) = join(sFlat0,top),
inference(cp,[status(thm)],[t297,t686]) ).
cnf(t690,plain,
join(top,top) = join(sFlat1,top),
inference(cp,[status(thm)],[t325,t686]) ).
cnf(t179,plain,
top = join(sFlat7,sFlat8),
inference(cp,[status(thm)],[t92,t178]) ).
cnf(t180,plain,
join(sFlat7,sFlat8) = top,
inference(orient,[status(thm)],[t179]) ).
cnf(t181,plain,
join(sFlat7,join(sFlat8,X1)) = join(top,X1),
inference(cp,[status(thm)],[t98,t180]) ).
cnf(t341,plain,
join(sFlat7,join(sFlat8,X1)) = join(top,X1),
inference(orient,[status(thm)],[t181]) ).
cnf(t343,plain,
join(top,X1) = join(sFlat7,join(X1,sFlat8)),
inference(cp,[status(thm)],[t341,t89]) ).
cnf(t412,plain,
join(sFlat7,join(X1,sFlat8)) = join(top,X1),
inference(orient,[status(thm)],[t343]) ).
cnf(t637,plain,
complement(sFlat7) = join(sFlat8,complement(sFlat7)),
inference(cp,[status(thm)],[t636,t178]) ).
cnf(t30521,plain,
sFlat8 = join(sFlat8,complement(sFlat7)),
inference(step,[status(thm)],[t637,t178]) ).
cnf(t30522,plain,
sFlat8 = join(sFlat8,sFlat8),
inference(step,[status(thm)],[t30521,t178]) ).
cnf(t654,plain,
join(sFlat8,sFlat8) = sFlat8,
inference(orient,[status(thm)],[t30522]) ).
cnf(t655,plain,
join(top,sFlat8) = join(sFlat7,sFlat8),
inference(cp,[status(thm)],[t412,t654]) ).
cnf(t30535,plain,
join(sFlat8,top) = join(sFlat7,sFlat8),
inference(step,[status(thm)],[t655,t89]) ).
cnf(t30536,plain,
join(sFlat8,top) = top,
inference(step,[status(thm)],[t30535,t180]) ).
cnf(t678,plain,
join(sFlat8,top) = top,
inference(orient,[status(thm)],[t30536]) ).
cnf(t680,plain,
join(top,top) = join(sFlat7,top),
inference(cp,[status(thm)],[t341,t678]) ).
cnf(t700,plain,
join(top,top) = join(sFlat7,top),
inference(orient,[status(thm)],[t680]) ).
cnf(t170,plain,
top = join(sFlat3,sFlat4),
inference(cp,[status(thm)],[t92,t169]) ).
cnf(t172,plain,
join(sFlat3,sFlat4) = top,
inference(orient,[status(thm)],[t170]) ).
cnf(t173,plain,
join(sFlat3,join(sFlat4,X1)) = join(top,X1),
inference(cp,[status(thm)],[t98,t172]) ).
cnf(t332,plain,
join(sFlat3,join(sFlat4,X1)) = join(top,X1),
inference(orient,[status(thm)],[t173]) ).
cnf(t334,plain,
join(top,X1) = join(sFlat3,join(X1,sFlat4)),
inference(cp,[status(thm)],[t332,t89]) ).
cnf(t408,plain,
join(sFlat3,join(X1,sFlat4)) = join(top,X1),
inference(orient,[status(thm)],[t334]) ).
cnf(t638,plain,
complement(sFlat3) = join(sFlat4,complement(sFlat3)),
inference(cp,[status(thm)],[t636,t169]) ).
cnf(t30523,plain,
sFlat4 = join(sFlat4,complement(sFlat3)),
inference(step,[status(thm)],[t638,t169]) ).
cnf(t30524,plain,
sFlat4 = join(sFlat4,sFlat4),
inference(step,[status(thm)],[t30523,t169]) ).
cnf(t658,plain,
join(sFlat4,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t30524]) ).
cnf(t659,plain,
join(top,sFlat4) = join(sFlat3,sFlat4),
inference(cp,[status(thm)],[t408,t658]) ).
cnf(t30537,plain,
join(sFlat4,top) = join(sFlat3,sFlat4),
inference(step,[status(thm)],[t659,t89]) ).
cnf(t30538,plain,
join(sFlat4,top) = top,
inference(step,[status(thm)],[t30537,t172]) ).
cnf(t682,plain,
join(sFlat4,top) = top,
inference(orient,[status(thm)],[t30538]) ).
cnf(t684,plain,
join(top,top) = join(sFlat3,top),
inference(cp,[status(thm)],[t332,t682]) ).
cnf(t30547,plain,
join(sFlat7,top) = join(sFlat3,top),
inference(step,[status(thm)],[t684,t700]) ).
cnf(t704,plain,
join(sFlat7,top) = join(sFlat3,top),
inference(orient,[status(thm)],[t30547]) ).
cnf(t30552,plain,
join(top,top) = join(sFlat3,top),
inference(step,[status(thm)],[t700,t704]) ).
cnf(t709,plain,
join(top,top) = join(sFlat3,top),
inference(orient,[status(thm)],[t30552]) ).
cnf(t30554,plain,
join(sFlat3,top) = join(sFlat1,top),
inference(step,[status(thm)],[t690,t709]) ).
cnf(t713,plain,
join(sFlat3,top) = join(sFlat1,top),
inference(orient,[status(thm)],[t30554]) ).
cnf(t30565,plain,
join(sFlat1,top) = join(sFlat0,top),
inference(step,[status(thm)],[t691,t713]) ).
cnf(t726,plain,
join(sFlat1,top) = join(sFlat0,top),
inference(orient,[status(thm)],[t30565]) ).
cnf(t742,plain,
join(sk1,converse(top)) = converse(join(sFlat0,top)),
inference(cp,[status(thm)],[t241,t726]) ).
cnf(t299,plain,
join(sFlat3,X1) = join(sFlat0,join(X1,sFlat2)),
inference(cp,[status(thm)],[t297,t89]) ).
cnf(t364,plain,
join(sFlat0,join(X1,sFlat2)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t299]) ).
cnf(t366,plain,
join(sFlat3,sFlat1) = join(sFlat0,top),
inference(cp,[status(thm)],[t364,t163]) ).
cnf(t30497,plain,
join(sFlat1,sFlat3) = join(sFlat0,top),
inference(step,[status(thm)],[t366,t89]) ).
cnf(t372,plain,
join(sFlat1,sFlat3) = join(sFlat0,top),
inference(orient,[status(thm)],[t30497]) ).
cnf(t373,plain,
join(sk1,converse(sFlat3)) = converse(join(sFlat0,top)),
inference(cp,[status(thm)],[t241,t372]) ).
cnf(t375,plain,
converse(join(sFlat0,top)) = join(sk1,converse(sFlat3)),
inference(orient,[status(thm)],[t373]) ).
cnf(t30583,plain,
join(sk1,converse(top)) = join(sk1,converse(sFlat3)),
inference(step,[status(thm)],[t742,t375]) ).
cnf(t768,plain,
join(sk1,converse(top)) = join(sk1,converse(sFlat3)),
inference(orient,[status(thm)],[t30583]) ).
cnf(t769,plain,
join(top,converse(top)) = join(sFlat5,join(sk1,converse(sFlat3))),
inference(cp,[status(thm)],[t316,t768]) ).
cnf(t30584,plain,
join(top,converse(top)) = join(top,converse(sFlat3)),
inference(step,[status(thm)],[t769,t316]) ).
cnf(t771,plain,
join(top,converse(top)) = join(top,converse(sFlat3)),
inference(orient,[status(thm)],[t30584]) ).
cnf(t773,plain,
join(converse(top),top) = converse(join(top,converse(sFlat3))),
inference(cp,[status(thm)],[t437,t771]) ).
cnf(t30585,plain,
join(top,converse(top)) = converse(join(top,converse(sFlat3))),
inference(step,[status(thm)],[t773,t89]) ).
cnf(t30586,plain,
join(top,converse(sFlat3)) = converse(join(top,converse(sFlat3))),
inference(step,[status(thm)],[t30585,t771]) ).
cnf(t30587,plain,
join(top,converse(sFlat3)) = join(converse(top),sFlat3),
inference(step,[status(thm)],[t30586,t437]) ).
cnf(t30588,plain,
join(top,converse(sFlat3)) = join(sFlat3,converse(top)),
inference(step,[status(thm)],[t30587,t89]) ).
cnf(t774,plain,
join(top,converse(sFlat3)) = join(sFlat3,converse(top)),
inference(orient,[status(thm)],[t30588]) ).
cnf(t30589,plain,
join(top,converse(top)) = join(sFlat3,converse(top)),
inference(step,[status(thm)],[t771,t774]) ).
cnf(t775,plain,
join(top,converse(top)) = join(sFlat3,converse(top)),
inference(orient,[status(thm)],[t30589]) ).
cnf(t30610,plain,
join(sFlat3,converse(top)) = join(sFlat1,converse(top)),
inference(step,[status(thm)],[t816,t775]) ).
cnf(t825,plain,
join(sFlat3,converse(top)) = join(sFlat1,converse(top)),
inference(orient,[status(thm)],[t30610]) ).
cnf(t835,plain,
join(converse(sFlat3),top) = converse(join(sFlat1,converse(top))),
inference(cp,[status(thm)],[t437,t825]) ).
cnf(t30619,plain,
join(top,converse(sFlat3)) = converse(join(sFlat1,converse(top))),
inference(step,[status(thm)],[t835,t89]) ).
cnf(t30613,plain,
join(top,converse(sFlat3)) = join(sFlat1,converse(top)),
inference(step,[status(thm)],[t774,t825]) ).
cnf(t828,plain,
join(top,converse(sFlat3)) = join(sFlat1,converse(top)),
inference(orient,[status(thm)],[t30613]) ).
cnf(t30620,plain,
join(sFlat1,converse(top)) = converse(join(sFlat1,converse(top))),
inference(step,[status(thm)],[t30619,t828]) ).
cnf(t30621,plain,
join(sFlat1,converse(top)) = join(sk1,converse(converse(top))),
inference(step,[status(thm)],[t30620,t241]) ).
cnf(t30622,plain,
join(sFlat1,converse(top)) = join(sk1,top),
inference(step,[status(thm)],[t30621,t27]) ).
cnf(t30623,plain,
join(sFlat1,converse(top)) = join(top,sk1),
inference(step,[status(thm)],[t30622,t89]) ).
cnf(t836,plain,
join(sFlat1,converse(top)) = join(top,sk1),
inference(orient,[status(thm)],[t30623]) ).
cnf(t30711,plain,
join(sFlat1,converse(top)) = top,
inference(step,[status(thm)],[t836,t1148]) ).
cnf(t1159,plain,
join(sFlat1,converse(top)) = top,
inference(orient,[status(thm)],[t30711]) ).
cnf(t30717,plain,
top = converse(top),
inference(step,[status(thm)],[t1165,t1159]) ).
cnf(t1167,plain,
converse(top) = top,
inference(orient,[status(thm)],[t30717]) ).
cnf(t30726,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t550,t1167]) ).
cnf(t1176,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t30726]) ).
cnf(t23411,plain,
join(sFlat2,complement(converse(complement(converse(sFlat2))))) = join(sFlat2,complement(top)),
inference(cp,[status(thm)],[t23385,t1176]) ).
cnf(t31997,plain,
join(sFlat2,complement(converse(complement(converse(sFlat2))))) = join(sFlat2,zero),
inference(step,[status(thm)],[t23411,t144]) ).
cnf(t31998,plain,
join(sFlat2,complement(converse(complement(converse(sFlat2))))) = sFlat2,
inference(step,[status(thm)],[t31997,t1080]) ).
cnf(t23429,plain,
join(sFlat2,complement(converse(complement(converse(sFlat2))))) = sFlat2,
inference(orient,[status(thm)],[t31998]) ).
cnf(t23436,plain,
complement(complement(converse(complement(converse(sFlat2))))) = join(complement(complement(converse(complement(converse(sFlat2))))),complement(sFlat2)),
inference(cp,[status(thm)],[t6146,t23429]) ).
cnf(t32000,plain,
converse(complement(converse(sFlat2))) = join(complement(complement(converse(complement(converse(sFlat2))))),complement(sFlat2)),
inference(step,[status(thm)],[t23436,t1092]) ).
cnf(t32001,plain,
converse(complement(converse(sFlat2))) = join(complement(sFlat2),complement(complement(converse(complement(converse(sFlat2)))))),
inference(step,[status(thm)],[t32000,t89]) ).
cnf(t751,plain,
sFlat1 = join(zero,complement(sFlat2)),
inference(cp,[status(thm)],[t748,t151]) ).
cnf(t760,plain,
join(zero,complement(sFlat2)) = sFlat1,
inference(orient,[status(thm)],[t751]) ).
cnf(t30649,plain,
complement(sFlat2) = sFlat1,
inference(step,[status(thm)],[t760,t974]) ).
cnf(t993,plain,
complement(sFlat2) = sFlat1,
inference(rw,[status(thm)],[t30649]) ).
cnf(t1027,plain,
complement(sFlat2) = sFlat1,
inference(orient,[status(thm)],[t993]) ).
cnf(t32002,plain,
converse(complement(converse(sFlat2))) = join(sFlat1,complement(complement(converse(complement(converse(sFlat2)))))),
inference(step,[status(thm)],[t32001,t1027]) ).
cnf(t32003,plain,
converse(complement(converse(sFlat2))) = join(sFlat1,converse(complement(converse(sFlat2)))),
inference(step,[status(thm)],[t32002,t1092]) ).
cnf(t23525,plain,
join(sFlat1,converse(complement(converse(sFlat2)))) = converse(complement(converse(sFlat2))),
inference(orient,[status(thm)],[t32003]) ).
cnf(t23531,plain,
join(sk1,converse(converse(complement(converse(sFlat2))))) = converse(converse(complement(converse(sFlat2)))),
inference(cp,[status(thm)],[t241,t23525]) ).
cnf(t32007,plain,
join(sk1,complement(converse(sFlat2))) = converse(converse(complement(converse(sFlat2)))),
inference(step,[status(thm)],[t23531,t27]) ).
cnf(t32008,plain,
join(sk1,complement(converse(sFlat2))) = complement(converse(sFlat2)),
inference(step,[status(thm)],[t32007,t27]) ).
cnf(t23570,plain,
join(sk1,complement(converse(sFlat2))) = complement(converse(sFlat2)),
inference(orient,[status(thm)],[t32008]) ).
cnf(t23587,plain,
zero = composition(sFlat1,complement(complement(converse(sFlat2)))),
inference(cp,[status(thm)],[t5665,t23570]) ).
cnf(t32016,plain,
zero = composition(sFlat1,converse(sFlat2)),
inference(step,[status(thm)],[t23587,t1092]) ).
cnf(t23630,plain,
composition(sFlat1,converse(sFlat2)) = zero,
inference(orient,[status(thm)],[t32016]) ).
cnf(t23632,plain,
composition(join(sFlat1,X1),converse(sFlat2)) = join(zero,composition(X1,converse(sFlat2))),
inference(cp,[status(thm)],[t112,t23630]) ).
cnf(t32158,plain,
composition(join(sFlat1,X1),converse(sFlat2)) = composition(X1,converse(sFlat2)),
inference(step,[status(thm)],[t23632,t974]) ).
cnf(t26003,plain,
composition(join(sFlat1,X1),converse(sFlat2)) = composition(X1,converse(sFlat2)),
inference(orient,[status(thm)],[t32158]) ).
cnf(t3315,plain,
sFlat1 = join(sFlat1,complement(join(sFlat2,X1))),
inference(cp,[status(thm)],[t3298,t151]) ).
cnf(t3450,plain,
join(sFlat1,complement(join(sFlat2,X1))) = sFlat1,
inference(orient,[status(thm)],[t3315]) ).
cnf(t664,plain,
join(sFlat3,sFlat2) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t364,t662]) ).
cnf(t30543,plain,
join(sFlat2,sFlat3) = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t664,t89]) ).
cnf(t30544,plain,
join(sFlat2,sFlat3) = sFlat3,
inference(step,[status(thm)],[t30543,t105]) ).
cnf(t693,plain,
join(sFlat2,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t30544]) ).
cnf(t3453,plain,
sFlat1 = join(sFlat1,complement(sFlat3)),
inference(cp,[status(thm)],[t3450,t693]) ).
cnf(t30952,plain,
sFlat1 = join(sFlat1,sFlat4),
inference(step,[status(thm)],[t3453,t169]) ).
cnf(t3468,plain,
join(sFlat1,sFlat4) = sFlat1,
inference(orient,[status(thm)],[t30952]) ).
cnf(t26104,plain,
composition(sFlat4,converse(sFlat2)) = composition(sFlat1,converse(sFlat2)),
inference(cp,[status(thm)],[t26003,t3468]) ).
cnf(t32159,plain,
composition(sFlat4,converse(sFlat2)) = zero,
inference(step,[status(thm)],[t26104,t23630]) ).
cnf(t26157,plain,
composition(sFlat4,converse(sFlat2)) = zero,
inference(orient,[status(thm)],[t32159]) ).
cnf(t26161,plain,
composition(sFlat2,converse(sFlat4)) = converse(zero),
inference(cp,[status(thm)],[t464,t26157]) ).
cnf(t32160,plain,
composition(sFlat2,converse(sFlat4)) = zero,
inference(step,[status(thm)],[t26161,t1240]) ).
cnf(t26163,plain,
composition(sFlat2,converse(sFlat4)) = zero,
inference(orient,[status(thm)],[t32160]) ).
cnf(t26165,plain,
composition(join(sFlat2,X1),converse(sFlat4)) = join(zero,composition(X1,converse(sFlat4))),
inference(cp,[status(thm)],[t112,t26163]) ).
cnf(t32292,plain,
composition(join(sFlat2,X1),converse(sFlat4)) = composition(X1,converse(sFlat4)),
inference(step,[status(thm)],[t26165,t974]) ).
cnf(t28391,plain,
composition(join(sFlat2,X1),converse(sFlat4)) = composition(X1,converse(sFlat4)),
inference(orient,[status(thm)],[t32292]) ).
cnf(t28461,plain,
composition(sFlat4,converse(join(sFlat2,X1))) = converse(composition(X1,converse(sFlat4))),
inference(cp,[status(thm)],[t464,t28391]) ).
cnf(t32346,plain,
composition(sFlat4,converse(join(sFlat2,X1))) = composition(sFlat4,converse(X1)),
inference(step,[status(thm)],[t28461,t464]) ).
cnf(t28867,plain,
composition(sFlat4,converse(join(sFlat2,X1))) = composition(sFlat4,converse(X1)),
inference(orient,[status(thm)],[t32346]) ).
cnf(t28877,plain,
composition(sFlat4,converse(converse(X1))) = composition(sFlat4,join(converse(sFlat2),X1)),
inference(cp,[status(thm)],[t28867,t437]) ).
cnf(t32349,plain,
composition(sFlat4,X1) = composition(sFlat4,join(converse(sFlat2),X1)),
inference(step,[status(thm)],[t28877,t27]) ).
cnf(t28937,plain,
composition(sFlat4,join(converse(sFlat2),X1)) = composition(sFlat4,X1),
inference(orient,[status(thm)],[t32349]) ).
cnf(t28955,plain,
composition(sFlat4,X1) = composition(sFlat4,join(X1,converse(sFlat2))),
inference(cp,[status(thm)],[t28937,t89]) ).
cnf(t28968,plain,
composition(sFlat4,join(X1,converse(sFlat2))) = composition(sFlat4,X1),
inference(orient,[status(thm)],[t28955]) ).
cnf(t259,plain,
sk3 = join(complement(join(sFlat6,X1)),complement(join(complement(sk3),complement(X1)))),
inference(cp,[status(thm)],[t252,t82]) ).
cnf(t32026,plain,
sk3 = join(complement(join(sFlat6,X1)),complement(join(sFlat6,complement(X1)))),
inference(step,[status(thm)],[t259,t82]) ).
cnf(t23772,plain,
join(complement(join(sFlat6,X1)),complement(join(sFlat6,complement(X1)))) = sk3,
inference(orient,[status(thm)],[t32026]) ).
cnf(t23811,plain,
join(sFlat6,X1) = join(complement(join(join(sFlat6,complement(X1)),complement(join(sFlat6,X1)))),complement(sk3)),
inference(cp,[status(thm)],[t19809,t23772]) ).
cnf(t32370,plain,
join(sFlat6,X1) = join(complement(sk3),complement(join(join(sFlat6,complement(X1)),complement(join(sFlat6,X1))))),
inference(step,[status(thm)],[t23811,t89]) ).
cnf(t32371,plain,
join(sFlat6,X1) = join(sFlat6,complement(join(join(sFlat6,complement(X1)),complement(join(sFlat6,X1))))),
inference(step,[status(thm)],[t32370,t82]) ).
cnf(t32372,plain,
join(sFlat6,X1) = join(sFlat6,complement(join(sFlat6,join(complement(X1),complement(join(sFlat6,X1)))))),
inference(step,[status(thm)],[t32371,t98]) ).
cnf(t32373,plain,
join(sFlat6,X1) = join(sFlat6,complement(join(sFlat6,complement(X1)))),
inference(step,[status(thm)],[t32372,t6146]) ).
cnf(t29709,plain,
join(sFlat6,complement(join(sFlat6,complement(X1)))) = join(sFlat6,X1),
inference(orient,[status(thm)],[t32373]) ).
cnf(t29711,plain,
join(sFlat6,complement(X1)) = join(sFlat6,complement(join(sFlat6,X1))),
inference(cp,[status(thm)],[t29709,t1092]) ).
cnf(t30312,plain,
join(sFlat6,complement(join(sFlat6,X1))) = join(sFlat6,complement(X1)),
inference(orient,[status(thm)],[t29711]) ).
cnf(t29715,plain,
join(sFlat6,sFlat5) = join(sFlat6,complement(join(sFlat6,sk1))),
inference(cp,[status(thm)],[t29709,t1006]) ).
cnf(t32379,plain,
join(sFlat5,sFlat6) = join(sFlat6,complement(join(sFlat6,sk1))),
inference(step,[status(thm)],[t29715,t89]) ).
cnf(t32380,plain,
sFlat7 = join(sFlat6,complement(join(sFlat6,sk1))),
inference(step,[status(thm)],[t32379,t103]) ).
cnf(t29779,plain,
join(sFlat6,complement(join(sFlat6,sk1))) = sFlat7,
inference(orient,[status(thm)],[t32380]) ).
cnf(t29788,plain,
join(sFlat6,join(sFlat6,sk1)) = join(sFlat6,complement(sFlat7)),
inference(cp,[status(thm)],[t29709,t29779]) ).
cnf(t641,plain,
complement(sk3) = join(sFlat6,complement(sk3)),
inference(cp,[status(thm)],[t636,t82]) ).
cnf(t30529,plain,
sFlat6 = join(sFlat6,complement(sk3)),
inference(step,[status(thm)],[t641,t82]) ).
cnf(t30530,plain,
sFlat6 = join(sFlat6,sFlat6),
inference(step,[status(thm)],[t30529,t82]) ).
cnf(t670,plain,
join(sFlat6,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t30530]) ).
cnf(t673,plain,
join(sFlat6,join(sFlat6,X1)) = join(sFlat6,X1),
inference(cp,[status(thm)],[t98,t670]) ).
cnf(t1307,plain,
join(sFlat6,join(sFlat6,X1)) = join(sFlat6,X1),
inference(orient,[status(thm)],[t673]) ).
cnf(t32381,plain,
join(sFlat6,sk1) = join(sFlat6,complement(sFlat7)),
inference(step,[status(thm)],[t29788,t1307]) ).
cnf(t32382,plain,
join(sFlat6,sk1) = join(sFlat6,sFlat8),
inference(step,[status(thm)],[t32381,t178]) ).
cnf(t29798,plain,
join(sFlat6,sk1) = join(sFlat6,sFlat8),
inference(orient,[status(thm)],[t32382]) ).
cnf(t29804,plain,
join(sFlat6,join(sk1,X1)) = join(join(sFlat6,sFlat8),X1),
inference(cp,[status(thm)],[t98,t29798]) ).
cnf(t32385,plain,
join(sFlat6,join(sk1,X1)) = join(sFlat6,join(sFlat8,X1)),
inference(step,[status(thm)],[t29804,t98]) ).
cnf(t29923,plain,
join(sFlat6,join(sk1,X1)) = join(sFlat6,join(sFlat8,X1)),
inference(orient,[status(thm)],[t32385]) ).
cnf(t243,plain,
join(sk1,converse(sFlat2)) = converse(top),
inference(cp,[status(thm)],[t241,t163]) ).
cnf(t250,plain,
join(sk1,converse(sFlat2)) = converse(top),
inference(orient,[status(thm)],[t243]) ).
cnf(t30720,plain,
join(sk1,converse(sFlat2)) = top,
inference(step,[status(thm)],[t250,t1167]) ).
cnf(t1170,plain,
join(sk1,converse(sFlat2)) = top,
inference(orient,[status(thm)],[t30720]) ).
cnf(t30035,plain,
join(sFlat6,join(sFlat8,converse(sFlat2))) = join(sFlat6,top),
inference(cp,[status(thm)],[t29923,t1170]) ).
cnf(t99,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t98,t92]) ).
cnf(t870,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t99]) ).
cnf(t104,plain,
join(sFlat5,join(sFlat6,X1)) = join(sFlat7,X1),
inference(cp,[status(thm)],[t98,t103]) ).
cnf(t289,plain,
join(sFlat5,join(sFlat6,X1)) = join(sFlat7,X1),
inference(orient,[status(thm)],[t104]) ).
cnf(t292,plain,
join(sFlat7,X1) = join(sFlat5,join(X1,sFlat6)),
inference(cp,[status(thm)],[t289,t89]) ).
cnf(t350,plain,
join(sFlat5,join(X1,sFlat6)) = join(sFlat7,X1),
inference(orient,[status(thm)],[t292]) ).
cnf(t671,plain,
join(sFlat7,sFlat6) = join(sFlat5,sFlat6),
inference(cp,[status(thm)],[t350,t670]) ).
cnf(t30545,plain,
join(sFlat6,sFlat7) = join(sFlat5,sFlat6),
inference(step,[status(thm)],[t671,t89]) ).
cnf(t30546,plain,
join(sFlat6,sFlat7) = sFlat7,
inference(step,[status(thm)],[t30545,t103]) ).
cnf(t697,plain,
join(sFlat6,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t30546]) ).
cnf(t930,plain,
top = join(sFlat6,join(sFlat7,complement(sFlat7))),
inference(cp,[status(thm)],[t870,t697]) ).
cnf(t30659,plain,
top = join(sFlat6,top),
inference(step,[status(thm)],[t930,t92]) ).
cnf(t1055,plain,
join(sFlat6,top) = top,
inference(orient,[status(thm)],[t30659]) ).
cnf(t32386,plain,
join(sFlat6,join(sFlat8,converse(sFlat2))) = top,
inference(step,[status(thm)],[t30035,t1055]) ).
cnf(t30067,plain,
join(sFlat6,join(sFlat8,converse(sFlat2))) = top,
inference(orient,[status(thm)],[t32386]) ).
cnf(t30317,plain,
join(sFlat6,complement(join(sFlat8,converse(sFlat2)))) = join(sFlat6,complement(top)),
inference(cp,[status(thm)],[t30312,t30067]) ).
cnf(t32415,plain,
join(sFlat6,complement(join(sFlat8,converse(sFlat2)))) = join(sFlat6,zero),
inference(step,[status(thm)],[t30317,t144]) ).
cnf(t32416,plain,
join(sFlat6,complement(join(sFlat8,converse(sFlat2)))) = sFlat6,
inference(step,[status(thm)],[t32415,t1080]) ).
cnf(t30385,plain,
join(sFlat6,complement(join(sFlat8,converse(sFlat2)))) = sFlat6,
inference(orient,[status(thm)],[t32416]) ).
cnf(t30390,plain,
complement(complement(join(sFlat8,converse(sFlat2)))) = join(complement(complement(join(sFlat8,converse(sFlat2)))),complement(sFlat6)),
inference(cp,[status(thm)],[t6146,t30385]) ).
cnf(t32417,plain,
join(sFlat8,converse(sFlat2)) = join(complement(complement(join(sFlat8,converse(sFlat2)))),complement(sFlat6)),
inference(step,[status(thm)],[t30390,t1092]) ).
cnf(t32418,plain,
join(sFlat8,converse(sFlat2)) = join(complement(sFlat6),complement(complement(join(sFlat8,converse(sFlat2))))),
inference(step,[status(thm)],[t32417,t89]) ).
cnf(t752,plain,
sk3 = join(zero,complement(sFlat6)),
inference(cp,[status(thm)],[t748,t82]) ).
cnf(t762,plain,
join(zero,complement(sFlat6)) = sk3,
inference(orient,[status(thm)],[t752]) ).
cnf(t30648,plain,
complement(sFlat6) = sk3,
inference(step,[status(thm)],[t762,t974]) ).
cnf(t992,plain,
complement(sFlat6) = sk3,
inference(rw,[status(thm)],[t30648]) ).
cnf(t1020,plain,
complement(sFlat6) = sk3,
inference(orient,[status(thm)],[t992]) ).
cnf(t32419,plain,
join(sFlat8,converse(sFlat2)) = join(sk3,complement(complement(join(sFlat8,converse(sFlat2))))),
inference(step,[status(thm)],[t32418,t1020]) ).
cnf(t32420,plain,
join(sFlat8,converse(sFlat2)) = join(sk3,join(sFlat8,converse(sFlat2))),
inference(step,[status(thm)],[t32419,t1092]) ).
cnf(t102,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t98,t89]) ).
cnf(t30887,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t102,t98]) ).
cnf(t2364,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t30887]) ).
cnf(t32421,plain,
join(sFlat8,converse(sFlat2)) = join(sFlat8,join(sk3,converse(sFlat2))),
inference(step,[status(thm)],[t32420,t2364]) ).
cnf(t3316,plain,
sk3 = join(sk3,complement(join(sFlat6,X1))),
inference(cp,[status(thm)],[t3298,t82]) ).
cnf(t3573,plain,
join(sk3,complement(join(sFlat6,X1))) = sk3,
inference(orient,[status(thm)],[t3316]) ).
cnf(t3576,plain,
sk3 = join(sk3,complement(sFlat7)),
inference(cp,[status(thm)],[t3573,t697]) ).
cnf(t30958,plain,
sk3 = join(sk3,sFlat8),
inference(step,[status(thm)],[t3576,t178]) ).
cnf(t30959,plain,
sk3 = join(sFlat8,sk3),
inference(step,[status(thm)],[t30958,t89]) ).
cnf(t3587,plain,
join(sFlat8,sk3) = sk3,
inference(orient,[status(thm)],[t30959]) ).
cnf(t3588,plain,
join(sFlat8,join(sk3,X1)) = join(sk3,X1),
inference(cp,[status(thm)],[t98,t3587]) ).
cnf(t3593,plain,
join(sFlat8,join(sk3,X1)) = join(sk3,X1),
inference(orient,[status(thm)],[t3588]) ).
cnf(t32422,plain,
join(sFlat8,converse(sFlat2)) = join(sk3,converse(sFlat2)),
inference(step,[status(thm)],[t32421,t3593]) ).
cnf(t30399,plain,
join(sk3,converse(sFlat2)) = join(sFlat8,converse(sFlat2)),
inference(orient,[status(thm)],[t32422]) ).
cnf(t30402,plain,
composition(sFlat4,sk3) = composition(sFlat4,join(sFlat8,converse(sFlat2))),
inference(cp,[status(thm)],[t28968,t30399]) ).
cnf(t32423,plain,
sFlat10 = composition(sFlat4,join(sFlat8,converse(sFlat2))),
inference(step,[status(thm)],[t30402,t174]) ).
cnf(t32424,plain,
sFlat10 = composition(sFlat4,sFlat8),
inference(step,[status(thm)],[t32423,t28968]) ).
cnf(t32425,plain,
sFlat10 = sFlat9,
inference(step,[status(thm)],[t32424,t182]) ).
cnf(t30413,plain,
sFlat10 = sFlat9,
inference(orient,[status(thm)],[t32425]) ).
cnf(t32426,plain,
composition(sFlat4,sk3) = sFlat9,
inference(step,[status(thm)],[t174,t30413]) ).
cnf(t30414,plain,
composition(sFlat4,sk3) = sFlat9,
inference(orient,[status(thm)],[t32426]) ).
cnf(u1,negated_conjecture,
composition(meet(sk2,converse(sk1)),meet(sk1,sk3)) != composition(meet(sk2,converse(sk1)),sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(g0_0,plain,
composition(complement(join(sFlat0,complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[goal_0,t75]) ).
cnf(g0_1,plain,
composition(complement(join(sFlat0,complement(sFlat1))),complement(join(complement(sk1),complement(sk3)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_0,t120]) ).
cnf(g0_2,plain,
composition(complement(join(sFlat0,sFlat2)),complement(join(complement(sk1),complement(sk3)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_1,t151]) ).
cnf(g0_3,plain,
composition(complement(sFlat3),complement(join(complement(sk1),complement(sk3)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_2,t105]) ).
cnf(g0_4,plain,
composition(sFlat4,complement(join(complement(sk1),complement(sk3)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_3,t169]) ).
cnf(g0_5,plain,
composition(sFlat4,complement(join(complement(sk3),complement(sk1)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_4,t89]) ).
cnf(g0_6,plain,
composition(sFlat4,complement(join(sFlat6,complement(sk1)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_5,t82]) ).
cnf(g0_7,plain,
composition(sFlat4,complement(join(sFlat6,sFlat5))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_6,t67]) ).
cnf(g0_8,plain,
composition(sFlat4,complement(join(sFlat5,sFlat6))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_7,t89]) ).
cnf(g0_9,plain,
composition(sFlat4,complement(sFlat7)) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_8,t103]) ).
cnf(g0_10,plain,
composition(sFlat4,sFlat8) != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_9,t178]) ).
cnf(g0_11,plain,
sFlat9 != composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_10,t182]) ).
cnf(g0_12,plain,
sFlat9 != composition(complement(join(sFlat0,complement(converse(sk1)))),sk3),
inference(rw,[status(thm)],[g0_11,t75]) ).
cnf(g0_13,plain,
sFlat9 != composition(complement(join(sFlat0,complement(sFlat1))),sk3),
inference(rw,[status(thm)],[g0_12,t120]) ).
cnf(g0_14,plain,
sFlat9 != composition(complement(join(sFlat0,sFlat2)),sk3),
inference(rw,[status(thm)],[g0_13,t151]) ).
cnf(g0_15,plain,
sFlat9 != composition(complement(sFlat3),sk3),
inference(rw,[status(thm)],[g0_14,t105]) ).
cnf(g0_16,plain,
sFlat9 != composition(sFlat4,sk3),
inference(rw,[status(thm)],[g0_15,t169]) ).
cnf(g0_17,plain,
sFlat9 != sFlat9,
inference(rw,[status(thm)],[g0_16,t30414]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL037-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.42 % Computer : n011.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Thu Sep 24 07:31:12 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.43 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 95.26/12.57 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 95.26/12.57 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------