%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL020-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:34:47 PM UTC 2026
% Result : Unsatisfiable 42.76s 5.98s
% Output : CNFRefutation 42.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 23
% Syntax : Number of clauses : 367 ( 367 unt; 0 nHn; 209 RR)
% Number of literals : 367 ( 366 equ; 13 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 13 con; 0-2 aty)
% Number of variables : 207 ( 29 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t13,axiom,
sFlat0 = complement(sk1),
introduced(definition) ).
cnf(t56,plain,
complement(sk1) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sFlat1 = complement(one),
introduced(definition) ).
cnf(t65,plain,
complement(one) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sFlat2 = join(complement(sk1),complement(one)),
introduced(definition) ).
cnf(t11561,plain,
sFlat2 = join(sFlat0,complement(one)),
inference(step,[status(thm)],[t15,t56]) ).
cnf(t11562,plain,
sFlat2 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t11561,t65]) ).
cnf(t92,plain,
join(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t11562]) ).
cnf(t16,axiom,
sFlat3 = complement(join(complement(sk1),complement(one))),
introduced(definition) ).
cnf(t38,plain,
complement(join(complement(sk1),complement(one))) = sFlat3,
inference(orient,[status(thm)],[t16]) ).
cnf(t11558,plain,
complement(join(sFlat0,complement(one))) = sFlat3,
inference(step,[status(thm)],[t38,t56]) ).
cnf(t63,plain,
complement(join(sFlat0,complement(one))) = sFlat3,
inference(rw,[status(thm)],[t11558]) ).
cnf(t11574,plain,
complement(join(sFlat0,sFlat1)) = sFlat3,
inference(step,[status(thm)],[t63,t65]) ).
cnf(t11575,plain,
complement(sFlat2) = sFlat3,
inference(step,[status(thm)],[t11574,t92]) ).
cnf(t132,plain,
complement(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t11575]) ).
cnf(t17,axiom,
sFlat4 = composition(complement(join(complement(sk1),complement(one))),sk2),
introduced(definition) ).
cnf(t11567,plain,
sFlat4 = composition(complement(join(sFlat0,complement(one))),sk2),
inference(step,[status(thm)],[t17,t56]) ).
cnf(t11568,plain,
sFlat4 = composition(complement(join(sFlat0,sFlat1)),sk2),
inference(step,[status(thm)],[t11567,t65]) ).
cnf(t11569,plain,
sFlat4 = composition(complement(sFlat2),sk2),
inference(step,[status(thm)],[t11568,t92]) ).
cnf(t108,plain,
composition(complement(sFlat2),sk2) = sFlat4,
inference(orient,[status(thm)],[t11569]) ).
cnf(t11576,plain,
composition(sFlat3,sk2) = sFlat4,
inference(step,[status(thm)],[t108,t132]) ).
cnf(t134,plain,
composition(sFlat3,sk2) = sFlat4,
inference(rw,[status(thm)],[t11576]) ).
cnf(t137,plain,
composition(sFlat3,sk2) = sFlat4,
inference(orient,[status(thm)],[t134]) ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t79,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t18,axiom,
sFlat5 = complement(sk2),
introduced(definition) ).
cnf(t72,plain,
complement(sk2) = sFlat5,
inference(orient,[status(thm)],[t18]) ).
cnf(t19,axiom,
sFlat6 = join(complement(sk1),complement(sk2)),
introduced(definition) ).
cnf(t11563,plain,
sFlat6 = join(complement(sk2),complement(sk1)),
inference(step,[status(thm)],[t19,t79]) ).
cnf(t11564,plain,
sFlat6 = join(sFlat5,complement(sk1)),
inference(step,[status(thm)],[t11563,t72]) ).
cnf(t11565,plain,
sFlat6 = join(sFlat5,sFlat0),
inference(step,[status(thm)],[t11564,t56]) ).
cnf(t11566,plain,
sFlat6 = join(sFlat0,sFlat5),
inference(step,[status(thm)],[t11565,t79]) ).
cnf(t94,plain,
join(sFlat0,sFlat5) = sFlat6,
inference(orient,[status(thm)],[t11566]) ).
cnf(t20,axiom,
sFlat7 = complement(join(complement(sk1),complement(sk2))),
introduced(definition) ).
cnf(t47,plain,
complement(join(complement(sk1),complement(sk2))) = sFlat7,
inference(orient,[status(thm)],[t20]) ).
cnf(t11559,plain,
complement(join(sFlat0,complement(sk2))) = sFlat7,
inference(step,[status(thm)],[t47,t56]) ).
cnf(t64,plain,
complement(join(sFlat0,complement(sk2))) = sFlat7,
inference(rw,[status(thm)],[t11559]) ).
cnf(t11577,plain,
complement(join(sFlat0,sFlat5)) = sFlat7,
inference(step,[status(thm)],[t64,t72]) ).
cnf(t11578,plain,
complement(sFlat6) = sFlat7,
inference(step,[status(thm)],[t11577,t94]) ).
cnf(t141,plain,
complement(sFlat6) = sFlat7,
inference(orient,[status(thm)],[t11578]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t112,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/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t114,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t112,t25]) ).
cnf(t304,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t114]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t96,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t81,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(rw,[status(thm)],[t26]) ).
cnf(t11607,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t81,t79]) ).
cnf(t519,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t11607]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t118,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t545,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t519,t118]) ).
cnf(u0,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t5,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t29,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/sandbox/benchmark/theBenchmark.p') ).
cnf(t82,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t11560,plain,
complement(top) = zero,
inference(step,[status(thm)],[t29,t82]) ).
cnf(t86,plain,
complement(top) = zero,
inference(rw,[status(thm)],[t11560]) ).
cnf(t122,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t86]) ).
cnf(t11812,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t545,t122]) ).
cnf(t11813,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t11812,t122]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t87,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t305,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t304,t24]) ).
cnf(t11585,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t305,t25]) ).
cnf(t318,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t11585]) ).
cnf(t319,plain,
one = converse(one),
inference(cp,[status(thm)],[t318,t24]) ).
cnf(t323,plain,
converse(one) = one,
inference(orient,[status(thm)],[t319]) ).
cnf(t528,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t519,t323]) ).
cnf(t11586,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t318,t323]) ).
cnf(t332,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t11586]) ).
cnf(t333,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t332]) ).
cnf(t11608,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t528,t333]) ).
cnf(t11609,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t11608,t333]) ).
cnf(t551,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t11609]) ).
cnf(t554,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t551,t122]) ).
cnf(t11614,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t554,t122]) ).
cnf(t11615,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t11614,t122]) ).
cnf(t577,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t11615]) ).
cnf(t578,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t87,t577]) ).
cnf(t717,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t578]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t80,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t21]) ).
cnf(t11581,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t80,t79]) ).
cnf(t203,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t11581]) ).
cnf(t565,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t203,t551]) ).
cnf(t11652,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t565,t82]) ).
cnf(t11653,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t11652,t122]) ).
cnf(t11654,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t11653,t79]) ).
cnf(t655,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t11654]) ).
cnf(t723,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t717,t655]) ).
cnf(t11679,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t723,t655]) ).
cnf(t743,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t11679]) ).
cnf(t11814,plain,
zero = composition(converse(sk1),complement(sk1)),
inference(step,[status(thm)],[t11813,t743]) ).
cnf(t11815,plain,
zero = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t11814,t56]) ).
cnf(t1664,plain,
composition(converse(sk1),sFlat0) = zero,
inference(orient,[status(thm)],[t11815]) ).
cnf(t1666,plain,
composition(join(converse(sk1),X1),sFlat0) = join(zero,composition(X1,sFlat0)),
inference(cp,[status(thm)],[t96,t1664]) ).
cnf(t11833,plain,
composition(join(converse(sk1),X1),sFlat0) = composition(X1,sFlat0),
inference(step,[status(thm)],[t1666,t743]) ).
cnf(t1832,plain,
composition(join(converse(sk1),X1),sFlat0) = composition(X1,sFlat0),
inference(orient,[status(thm)],[t11833]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t99,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t1833,plain,
composition(converse(X1),sFlat0) = composition(converse(join(sk1,X1)),sFlat0),
inference(cp,[status(thm)],[t1832,t99]) ).
cnf(t5084,plain,
composition(converse(join(sk1,X1)),sFlat0) = composition(converse(X1),sFlat0),
inference(orient,[status(thm)],[t1833]) ).
cnf(t121,plain,
composition(join(X1,sk1),top) = join(composition(X1,top),sk1),
inference(cp,[status(thm)],[t96,t118]) ).
cnf(t11593,plain,
composition(join(X1,sk1),top) = join(sk1,composition(X1,top)),
inference(step,[status(thm)],[t121,t79]) ).
cnf(t412,plain,
composition(join(X1,sk1),top) = join(sk1,composition(X1,top)),
inference(orient,[status(thm)],[t11593]) ).
cnf(t11686,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t655,t743]) ).
cnf(t768,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t11686]) ).
cnf(t899,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t768]) ).
cnf(t900,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t551,t899]) ).
cnf(t11740,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t900,t899]) ).
cnf(t11741,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t11740,t899]) ).
cnf(t978,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t11741]) ).
cnf(t990,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t87,t978]) ).
cnf(t1213,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t990]) ).
cnf(t1220,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = join(complement(join(complement(X1),X2)),X1),
inference(cp,[status(thm)],[t1213,t203]) ).
cnf(t11941,plain,
X1 = join(complement(join(complement(X1),X2)),X1),
inference(step,[status(thm)],[t1220,t203]) ).
cnf(t11942,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t11941,t79]) ).
cnf(t2682,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t11942]) ).
cnf(t2698,plain,
sk1 = join(sk1,complement(join(sFlat0,X1))),
inference(cp,[status(thm)],[t2682,t56]) ).
cnf(t2948,plain,
join(sk1,complement(join(sFlat0,X1))) = sk1,
inference(orient,[status(thm)],[t2698]) ).
cnf(t657,plain,
sFlat2 = join(zero,complement(sFlat3)),
inference(cp,[status(thm)],[t655,t132]) ).
cnf(t664,plain,
join(zero,complement(sFlat3)) = sFlat2,
inference(orient,[status(thm)],[t657]) ).
cnf(t11683,plain,
complement(sFlat3) = sFlat2,
inference(step,[status(thm)],[t664,t743]) ).
cnf(t765,plain,
complement(sFlat3) = sFlat2,
inference(rw,[status(thm)],[t11683]) ).
cnf(t797,plain,
complement(sFlat3) = sFlat2,
inference(orient,[status(thm)],[t765]) ).
cnf(t798,plain,
complement(sFlat3) = join(sFlat2,complement(sFlat3)),
inference(cp,[status(thm)],[t551,t797]) ).
cnf(t11706,plain,
sFlat2 = join(sFlat2,complement(sFlat3)),
inference(step,[status(thm)],[t798,t797]) ).
cnf(t11707,plain,
sFlat2 = join(sFlat2,sFlat2),
inference(step,[status(thm)],[t11706,t797]) ).
cnf(t93,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t87,t92]) ).
cnf(t145,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t93]) ).
cnf(t148,plain,
join(sFlat2,X1) = join(sFlat0,join(X1,sFlat1)),
inference(cp,[status(thm)],[t145,t79]) ).
cnf(t193,plain,
join(sFlat0,join(X1,sFlat1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t148]) ).
cnf(t556,plain,
complement(one) = join(sFlat1,complement(one)),
inference(cp,[status(thm)],[t551,t65]) ).
cnf(t11618,plain,
sFlat1 = join(sFlat1,complement(one)),
inference(step,[status(thm)],[t556,t65]) ).
cnf(t11619,plain,
sFlat1 = join(sFlat1,sFlat1),
inference(step,[status(thm)],[t11618,t65]) ).
cnf(t585,plain,
join(sFlat1,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t11619]) ).
cnf(t586,plain,
join(sFlat2,sFlat1) = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t193,t585]) ).
cnf(t11634,plain,
join(sFlat1,sFlat2) = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t586,t79]) ).
cnf(t11635,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t11634,t92]) ).
cnf(t610,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t11635]) ).
cnf(t611,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t145,t610]) ).
cnf(t653,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(orient,[status(thm)],[t611]) ).
cnf(t11708,plain,
sFlat2 = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t11707,t653]) ).
cnf(t940,plain,
join(sFlat0,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t11708]) ).
cnf(t2954,plain,
sk1 = join(sk1,complement(sFlat2)),
inference(cp,[status(thm)],[t2948,t940]) ).
cnf(t11952,plain,
sk1 = join(sk1,sFlat3),
inference(step,[status(thm)],[t2954,t132]) ).
cnf(t11953,plain,
sk1 = join(sFlat3,sk1),
inference(step,[status(thm)],[t11952,t79]) ).
cnf(t2978,plain,
join(sFlat3,sk1) = sk1,
inference(orient,[status(thm)],[t11953]) ).
cnf(t2981,plain,
join(sk1,composition(sFlat3,top)) = composition(sk1,top),
inference(cp,[status(thm)],[t412,t2978]) ).
cnf(t11955,plain,
join(sk1,composition(sFlat3,top)) = sk1,
inference(step,[status(thm)],[t2981,t118]) ).
cnf(t2993,plain,
join(sk1,composition(sFlat3,top)) = sk1,
inference(orient,[status(thm)],[t11955]) ).
cnf(t5095,plain,
composition(converse(composition(sFlat3,top)),sFlat0) = composition(converse(sk1),sFlat0),
inference(cp,[status(thm)],[t5084,t2993]) ).
cnf(t88,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t87,t82]) ).
cnf(t821,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t88]) ).
cnf(t992,plain,
top = join(X1,join(X1,complement(X1))),
inference(cp,[status(thm)],[t821,t978]) ).
cnf(t11742,plain,
top = join(X1,top),
inference(step,[status(thm)],[t992,t82]) ).
cnf(t993,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t11742]) ).
cnf(t994,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t993,t79]) ).
cnf(t1000,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t994]) ).
cnf(t101,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t99,t25]) ).
cnf(t276,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t101]) ).
cnf(t277,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t276,t82]) ).
cnf(t377,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t277]) ).
cnf(t1037,plain,
top = converse(top),
inference(cp,[status(thm)],[t1000,t377]) ).
cnf(t1047,plain,
converse(top) = top,
inference(orient,[status(thm)],[t1037]) ).
cnf(t1052,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t112,t1047]) ).
cnf(t1093,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t1052]) ).
cnf(t12033,plain,
composition(composition(top,converse(sFlat3)),sFlat0) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t5095,t1093]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t104,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t12034,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t12033,t104]) ).
cnf(t12035,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = zero,
inference(step,[status(thm)],[t12034,t1664]) ).
cnf(t5115,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = zero,
inference(orient,[status(thm)],[t12035]) ).
cnf(t5119,plain,
composition(join(top,X1),composition(converse(sFlat3),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat3),sFlat0))),
inference(cp,[status(thm)],[t96,t5115]) ).
cnf(t12043,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat3),sFlat0))),
inference(step,[status(thm)],[t5119,t1000]) ).
cnf(t12044,plain,
zero = join(zero,composition(X1,composition(converse(sFlat3),sFlat0))),
inference(step,[status(thm)],[t12043,t5115]) ).
cnf(t12045,plain,
zero = composition(X1,composition(converse(sFlat3),sFlat0)),
inference(step,[status(thm)],[t12044,t743]) ).
cnf(t5140,plain,
composition(X1,composition(converse(sFlat3),sFlat0)) = zero,
inference(orient,[status(thm)],[t12045]) ).
cnf(t5141,plain,
zero = composition(converse(sFlat3),sFlat0),
inference(cp,[status(thm)],[t5140,t333]) ).
cnf(t5149,plain,
composition(converse(sFlat3),sFlat0) = zero,
inference(orient,[status(thm)],[t5141]) ).
cnf(t5154,plain,
composition(converse(sFlat0),sFlat3) = converse(zero),
inference(cp,[status(thm)],[t304,t5149]) ).
cnf(t102,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t99,t25]) ).
cnf(t284,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t102]) ).
cnf(t761,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t284,t743]) ).
cnf(t11807,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t761,t25]) ).
cnf(t1064,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t11807]) ).
cnf(t746,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t743,t79]) ).
cnf(t815,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t746]) ).
cnf(t1065,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t1064,t815]) ).
cnf(t1074,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t1065]) ).
cnf(t12046,plain,
composition(converse(sFlat0),sFlat3) = zero,
inference(step,[status(thm)],[t5154,t1074]) ).
cnf(t5155,plain,
composition(converse(sFlat0),sFlat3) = zero,
inference(orient,[status(thm)],[t12046]) ).
cnf(t5157,plain,
composition(join(converse(sFlat0),X1),sFlat3) = join(zero,composition(X1,sFlat3)),
inference(cp,[status(thm)],[t96,t5155]) ).
cnf(t12083,plain,
composition(join(converse(sFlat0),X1),sFlat3) = composition(X1,sFlat3),
inference(step,[status(thm)],[t5157,t743]) ).
cnf(t5337,plain,
composition(join(converse(sFlat0),X1),sFlat3) = composition(X1,sFlat3),
inference(orient,[status(thm)],[t12083]) ).
cnf(t5338,plain,
composition(converse(X1),sFlat3) = composition(converse(join(sFlat0,X1)),sFlat3),
inference(cp,[status(thm)],[t5337,t99]) ).
cnf(t6880,plain,
composition(converse(join(sFlat0,X1)),sFlat3) = composition(converse(X1),sFlat3),
inference(orient,[status(thm)],[t5338]) ).
cnf(t6913,plain,
composition(converse(sFlat3),join(sFlat0,X1)) = converse(composition(converse(X1),sFlat3)),
inference(cp,[status(thm)],[t304,t6880]) ).
cnf(t12273,plain,
composition(converse(sFlat3),join(sFlat0,X1)) = composition(converse(sFlat3),X1),
inference(step,[status(thm)],[t6913,t304]) ).
cnf(t7685,plain,
composition(converse(sFlat3),join(sFlat0,X1)) = composition(converse(sFlat3),X1),
inference(orient,[status(thm)],[t12273]) ).
cnf(t220,plain,
X1 = join(complement(join(complement(X1),sFlat6)),complement(join(complement(X1),sFlat7))),
inference(cp,[status(thm)],[t203,t141]) ).
cnf(t12409,plain,
X1 = join(complement(join(sFlat6,complement(X1))),complement(join(complement(X1),sFlat7))),
inference(step,[status(thm)],[t220,t79]) ).
cnf(t12410,plain,
X1 = join(complement(join(sFlat6,complement(X1))),complement(join(sFlat7,complement(X1)))),
inference(step,[status(thm)],[t12409,t79]) ).
cnf(t10647,plain,
join(complement(join(sFlat6,complement(X1))),complement(join(sFlat7,complement(X1)))) = X1,
inference(orient,[status(thm)],[t12410]) ).
cnf(t211,plain,
sk1 = join(complement(join(sFlat0,X1)),complement(join(complement(sk1),complement(X1)))),
inference(cp,[status(thm)],[t203,t56]) ).
cnf(t12343,plain,
sk1 = join(complement(join(sFlat0,X1)),complement(join(sFlat0,complement(X1)))),
inference(step,[status(thm)],[t211,t56]) ).
cnf(t8708,plain,
join(complement(join(sFlat0,X1)),complement(join(sFlat0,complement(X1)))) = sk1,
inference(orient,[status(thm)],[t12343]) ).
cnf(t8737,plain,
sk1 = join(complement(sFlat6),complement(join(sFlat0,complement(sFlat5)))),
inference(cp,[status(thm)],[t8708,t94]) ).
cnf(t12352,plain,
sk1 = join(sFlat7,complement(join(sFlat0,complement(sFlat5)))),
inference(step,[status(thm)],[t8737,t141]) ).
cnf(t658,plain,
sk2 = join(zero,complement(sFlat5)),
inference(cp,[status(thm)],[t655,t72]) ).
cnf(t666,plain,
join(zero,complement(sFlat5)) = sk2,
inference(orient,[status(thm)],[t658]) ).
cnf(t11682,plain,
complement(sFlat5) = sk2,
inference(step,[status(thm)],[t666,t743]) ).
cnf(t764,plain,
complement(sFlat5) = sk2,
inference(rw,[status(thm)],[t11682]) ).
cnf(t790,plain,
complement(sFlat5) = sk2,
inference(orient,[status(thm)],[t764]) ).
cnf(t12353,plain,
sk1 = join(sFlat7,complement(join(sFlat0,sk2))),
inference(step,[status(thm)],[t12352,t790]) ).
cnf(t8815,plain,
join(sFlat7,complement(join(sFlat0,sk2))) = sk1,
inference(orient,[status(thm)],[t12353]) ).
cnf(t10666,plain,
join(sFlat0,sk2) = join(complement(join(sFlat6,complement(join(sFlat0,sk2)))),complement(sk1)),
inference(cp,[status(thm)],[t10647,t8815]) ).
cnf(t12411,plain,
join(sFlat0,sk2) = join(complement(sk1),complement(join(sFlat6,complement(join(sFlat0,sk2))))),
inference(step,[status(thm)],[t10666,t79]) ).
cnf(t12412,plain,
join(sFlat0,sk2) = join(sFlat0,complement(join(sFlat6,complement(join(sFlat0,sk2))))),
inference(step,[status(thm)],[t12411,t56]) ).
cnf(t2694,plain,
sFlat6 = join(sFlat6,complement(join(sFlat7,X1))),
inference(cp,[status(thm)],[t2682,t141]) ).
cnf(t2784,plain,
join(sFlat6,complement(join(sFlat7,X1))) = sFlat6,
inference(orient,[status(thm)],[t2694]) ).
cnf(t91,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t87,t79]) ).
cnf(t11877,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t91,t87]) ).
cnf(t1978,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t11877]) ).
cnf(t2696,plain,
sk2 = join(sk2,complement(join(sFlat5,X1))),
inference(cp,[status(thm)],[t2682,t72]) ).
cnf(t2806,plain,
join(sk2,complement(join(sFlat5,X1))) = sk2,
inference(orient,[status(thm)],[t2696]) ).
cnf(t95,plain,
join(sFlat0,join(sFlat5,X1)) = join(sFlat6,X1),
inference(cp,[status(thm)],[t87,t94]) ).
cnf(t153,plain,
join(sFlat0,join(sFlat5,X1)) = join(sFlat6,X1),
inference(orient,[status(thm)],[t95]) ).
cnf(t156,plain,
join(sFlat6,X1) = join(sFlat0,join(X1,sFlat5)),
inference(cp,[status(thm)],[t153,t79]) ).
cnf(t229,plain,
join(sFlat0,join(X1,sFlat5)) = join(sFlat6,X1),
inference(orient,[status(thm)],[t156]) ).
cnf(t555,plain,
complement(sk2) = join(sFlat5,complement(sk2)),
inference(cp,[status(thm)],[t551,t72]) ).
cnf(t11616,plain,
sFlat5 = join(sFlat5,complement(sk2)),
inference(step,[status(thm)],[t555,t72]) ).
cnf(t11617,plain,
sFlat5 = join(sFlat5,sFlat5),
inference(step,[status(thm)],[t11616,t72]) ).
cnf(t579,plain,
join(sFlat5,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t11617]) ).
cnf(t582,plain,
join(sFlat6,sFlat5) = join(sFlat0,sFlat5),
inference(cp,[status(thm)],[t229,t579]) ).
cnf(t11632,plain,
join(sFlat5,sFlat6) = join(sFlat0,sFlat5),
inference(step,[status(thm)],[t582,t79]) ).
cnf(t11633,plain,
join(sFlat5,sFlat6) = sFlat6,
inference(step,[status(thm)],[t11632,t94]) ).
cnf(t606,plain,
join(sFlat5,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t11633]) ).
cnf(t2809,plain,
sk2 = join(sk2,complement(sFlat6)),
inference(cp,[status(thm)],[t2806,t606]) ).
cnf(t11943,plain,
sk2 = join(sk2,sFlat7),
inference(step,[status(thm)],[t2809,t141]) ).
cnf(t11944,plain,
sk2 = join(sFlat7,sk2),
inference(step,[status(thm)],[t11943,t79]) ).
cnf(t2818,plain,
join(sFlat7,sk2) = sk2,
inference(orient,[status(thm)],[t11944]) ).
cnf(t2822,plain,
join(sFlat7,join(X1,sk2)) = join(X1,sk2),
inference(cp,[status(thm)],[t1978,t2818]) ).
cnf(t2839,plain,
join(sFlat7,join(X1,sk2)) = join(X1,sk2),
inference(orient,[status(thm)],[t2822]) ).
cnf(t2845,plain,
sFlat6 = join(sFlat6,complement(join(X1,sk2))),
inference(cp,[status(thm)],[t2784,t2839]) ).
cnf(t3256,plain,
join(sFlat6,complement(join(X1,sk2))) = sFlat6,
inference(orient,[status(thm)],[t2845]) ).
cnf(t12413,plain,
join(sFlat0,sk2) = join(sFlat0,complement(sFlat6)),
inference(step,[status(thm)],[t12412,t3256]) ).
cnf(t12414,plain,
join(sFlat0,sk2) = join(sFlat0,sFlat7),
inference(step,[status(thm)],[t12413,t141]) ).
cnf(t10697,plain,
join(sFlat0,sk2) = join(sFlat0,sFlat7),
inference(orient,[status(thm)],[t12414]) ).
cnf(t10700,plain,
composition(converse(sFlat3),sk2) = composition(converse(sFlat3),join(sFlat0,sFlat7)),
inference(cp,[status(thm)],[t7685,t10697]) ).
cnf(t12419,plain,
composition(converse(sFlat3),sk2) = composition(converse(sFlat3),sFlat7),
inference(step,[status(thm)],[t10700,t7685]) ).
cnf(t10742,plain,
composition(converse(sFlat3),sk2) = composition(converse(sFlat3),sFlat7),
inference(orient,[status(thm)],[t12419]) ).
cnf(t656,plain,
sFlat6 = join(zero,complement(sFlat7)),
inference(cp,[status(thm)],[t655,t141]) ).
cnf(t662,plain,
join(zero,complement(sFlat7)) = sFlat6,
inference(orient,[status(thm)],[t656]) ).
cnf(t11684,plain,
complement(sFlat7) = sFlat6,
inference(step,[status(thm)],[t662,t743]) ).
cnf(t766,plain,
complement(sFlat7) = sFlat6,
inference(rw,[status(thm)],[t11684]) ).
cnf(t806,plain,
complement(sFlat7) = sFlat6,
inference(orient,[status(thm)],[t766]) ).
cnf(t807,plain,
complement(sFlat7) = join(sFlat6,complement(sFlat7)),
inference(cp,[status(thm)],[t551,t806]) ).
cnf(t11711,plain,
sFlat6 = join(sFlat6,complement(sFlat7)),
inference(step,[status(thm)],[t807,t806]) ).
cnf(t11712,plain,
sFlat6 = join(sFlat6,sFlat6),
inference(step,[status(thm)],[t11711,t806]) ).
cnf(t608,plain,
join(sFlat6,sFlat6) = join(sFlat0,sFlat6),
inference(cp,[status(thm)],[t153,t606]) ).
cnf(t651,plain,
join(sFlat6,sFlat6) = join(sFlat0,sFlat6),
inference(orient,[status(thm)],[t608]) ).
cnf(t11713,plain,
sFlat6 = join(sFlat0,sFlat6),
inference(step,[status(thm)],[t11712,t651]) ).
cnf(t945,plain,
join(sFlat0,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t11713]) ).
cnf(t2953,plain,
sk1 = join(sk1,complement(sFlat6)),
inference(cp,[status(thm)],[t2948,t945]) ).
cnf(t11950,plain,
sk1 = join(sk1,sFlat7),
inference(step,[status(thm)],[t2953,t141]) ).
cnf(t11951,plain,
sk1 = join(sFlat7,sk1),
inference(step,[status(thm)],[t11950,t79]) ).
cnf(t2970,plain,
join(sFlat7,sk1) = sk1,
inference(orient,[status(thm)],[t11951]) ).
cnf(t2972,plain,
join(sk1,composition(sFlat7,top)) = composition(sk1,top),
inference(cp,[status(thm)],[t412,t2970]) ).
cnf(t11954,plain,
join(sk1,composition(sFlat7,top)) = sk1,
inference(step,[status(thm)],[t2972,t118]) ).
cnf(t2987,plain,
join(sk1,composition(sFlat7,top)) = sk1,
inference(orient,[status(thm)],[t11954]) ).
cnf(t5097,plain,
composition(converse(composition(sFlat7,top)),sFlat0) = composition(converse(sk1),sFlat0),
inference(cp,[status(thm)],[t5084,t2987]) ).
cnf(t12036,plain,
composition(composition(top,converse(sFlat7)),sFlat0) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t5097,t1093]) ).
cnf(t12037,plain,
composition(top,composition(converse(sFlat7),sFlat0)) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t12036,t104]) ).
cnf(t12038,plain,
composition(top,composition(converse(sFlat7),sFlat0)) = zero,
inference(step,[status(thm)],[t12037,t1664]) ).
cnf(t5122,plain,
composition(top,composition(converse(sFlat7),sFlat0)) = zero,
inference(orient,[status(thm)],[t12038]) ).
cnf(t5126,plain,
composition(join(top,X1),composition(converse(sFlat7),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat7),sFlat0))),
inference(cp,[status(thm)],[t96,t5122]) ).
cnf(t12055,plain,
composition(top,composition(converse(sFlat7),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat7),sFlat0))),
inference(step,[status(thm)],[t5126,t1000]) ).
cnf(t12056,plain,
zero = join(zero,composition(X1,composition(converse(sFlat7),sFlat0))),
inference(step,[status(thm)],[t12055,t5122]) ).
cnf(t12057,plain,
zero = composition(X1,composition(converse(sFlat7),sFlat0)),
inference(step,[status(thm)],[t12056,t743]) ).
cnf(t5182,plain,
composition(X1,composition(converse(sFlat7),sFlat0)) = zero,
inference(orient,[status(thm)],[t12057]) ).
cnf(t5183,plain,
zero = composition(converse(sFlat7),sFlat0),
inference(cp,[status(thm)],[t5182,t333]) ).
cnf(t5191,plain,
composition(converse(sFlat7),sFlat0) = zero,
inference(orient,[status(thm)],[t5183]) ).
cnf(t5196,plain,
composition(converse(sFlat0),sFlat7) = converse(zero),
inference(cp,[status(thm)],[t304,t5191]) ).
cnf(t12058,plain,
composition(converse(sFlat0),sFlat7) = zero,
inference(step,[status(thm)],[t5196,t1074]) ).
cnf(t5197,plain,
composition(converse(sFlat0),sFlat7) = zero,
inference(orient,[status(thm)],[t12058]) ).
cnf(t5199,plain,
composition(join(converse(sFlat0),X1),sFlat7) = join(zero,composition(X1,sFlat7)),
inference(cp,[status(thm)],[t96,t5197]) ).
cnf(t12106,plain,
composition(join(converse(sFlat0),X1),sFlat7) = composition(X1,sFlat7),
inference(step,[status(thm)],[t5199,t743]) ).
cnf(t5663,plain,
composition(join(converse(sFlat0),X1),sFlat7) = composition(X1,sFlat7),
inference(orient,[status(thm)],[t12106]) ).
cnf(t5664,plain,
composition(converse(X1),sFlat7) = composition(converse(join(sFlat0,X1)),sFlat7),
inference(cp,[status(thm)],[t5663,t99]) ).
cnf(t7130,plain,
composition(converse(join(sFlat0,X1)),sFlat7) = composition(converse(X1),sFlat7),
inference(orient,[status(thm)],[t5664]) ).
cnf(t221,plain,
X1 = join(complement(join(complement(X1),sFlat2)),complement(join(complement(X1),sFlat3))),
inference(cp,[status(thm)],[t203,t132]) ).
cnf(t12464,plain,
X1 = join(complement(join(sFlat2,complement(X1))),complement(join(complement(X1),sFlat3))),
inference(step,[status(thm)],[t221,t79]) ).
cnf(t12465,plain,
X1 = join(complement(join(sFlat2,complement(X1))),complement(join(sFlat3,complement(X1)))),
inference(step,[status(thm)],[t12464,t79]) ).
cnf(t11314,plain,
join(complement(join(sFlat2,complement(X1))),complement(join(sFlat3,complement(X1)))) = X1,
inference(orient,[status(thm)],[t12465]) ).
cnf(t8736,plain,
sk1 = join(complement(sFlat2),complement(join(sFlat0,complement(sFlat1)))),
inference(cp,[status(thm)],[t8708,t92]) ).
cnf(t12350,plain,
sk1 = join(sFlat3,complement(join(sFlat0,complement(sFlat1)))),
inference(step,[status(thm)],[t8736,t132]) ).
cnf(t659,plain,
one = join(zero,complement(sFlat1)),
inference(cp,[status(thm)],[t655,t65]) ).
cnf(t668,plain,
join(zero,complement(sFlat1)) = one,
inference(orient,[status(thm)],[t659]) ).
cnf(t11681,plain,
complement(sFlat1) = one,
inference(step,[status(thm)],[t668,t743]) ).
cnf(t763,plain,
complement(sFlat1) = one,
inference(rw,[status(thm)],[t11681]) ).
cnf(t783,plain,
complement(sFlat1) = one,
inference(orient,[status(thm)],[t763]) ).
cnf(t12351,plain,
sk1 = join(sFlat3,complement(join(sFlat0,one))),
inference(step,[status(thm)],[t12350,t783]) ).
cnf(t8801,plain,
join(sFlat3,complement(join(sFlat0,one))) = sk1,
inference(orient,[status(thm)],[t12351]) ).
cnf(t11333,plain,
join(sFlat0,one) = join(complement(join(sFlat2,complement(join(sFlat0,one)))),complement(sk1)),
inference(cp,[status(thm)],[t11314,t8801]) ).
cnf(t12466,plain,
join(sFlat0,one) = join(complement(sk1),complement(join(sFlat2,complement(join(sFlat0,one))))),
inference(step,[status(thm)],[t11333,t79]) ).
cnf(t12467,plain,
join(sFlat0,one) = join(sFlat0,complement(join(sFlat2,complement(join(sFlat0,one))))),
inference(step,[status(thm)],[t12466,t56]) ).
cnf(t2695,plain,
sFlat2 = join(sFlat2,complement(join(sFlat3,X1))),
inference(cp,[status(thm)],[t2682,t132]) ).
cnf(t2795,plain,
join(sFlat2,complement(join(sFlat3,X1))) = sFlat2,
inference(orient,[status(thm)],[t2695]) ).
cnf(t2697,plain,
one = join(one,complement(join(sFlat1,X1))),
inference(cp,[status(thm)],[t2682,t65]) ).
cnf(t2849,plain,
join(one,complement(join(sFlat1,X1))) = one,
inference(orient,[status(thm)],[t2697]) ).
cnf(t2854,plain,
one = join(one,complement(sFlat2)),
inference(cp,[status(thm)],[t2849,t610]) ).
cnf(t11945,plain,
one = join(one,sFlat3),
inference(step,[status(thm)],[t2854,t132]) ).
cnf(t11946,plain,
one = join(sFlat3,one),
inference(step,[status(thm)],[t11945,t79]) ).
cnf(t2864,plain,
join(sFlat3,one) = one,
inference(orient,[status(thm)],[t11946]) ).
cnf(t2870,plain,
join(sFlat3,join(X1,one)) = join(X1,one),
inference(cp,[status(thm)],[t1978,t2864]) ).
cnf(t2908,plain,
join(sFlat3,join(X1,one)) = join(X1,one),
inference(orient,[status(thm)],[t2870]) ).
cnf(t2915,plain,
sFlat2 = join(sFlat2,complement(join(X1,one))),
inference(cp,[status(thm)],[t2795,t2908]) ).
cnf(t3308,plain,
join(sFlat2,complement(join(X1,one))) = sFlat2,
inference(orient,[status(thm)],[t2915]) ).
cnf(t12468,plain,
join(sFlat0,one) = join(sFlat0,complement(sFlat2)),
inference(step,[status(thm)],[t12467,t3308]) ).
cnf(t12469,plain,
join(sFlat0,one) = join(sFlat0,sFlat3),
inference(step,[status(thm)],[t12468,t132]) ).
cnf(t11365,plain,
join(sFlat0,one) = join(sFlat0,sFlat3),
inference(orient,[status(thm)],[t12469]) ).
cnf(t11379,plain,
composition(converse(one),sFlat7) = composition(converse(join(sFlat0,sFlat3)),sFlat7),
inference(cp,[status(thm)],[t7130,t11365]) ).
cnf(t12498,plain,
composition(one,sFlat7) = composition(converse(join(sFlat0,sFlat3)),sFlat7),
inference(step,[status(thm)],[t11379,t323]) ).
cnf(t12499,plain,
sFlat7 = composition(converse(join(sFlat0,sFlat3)),sFlat7),
inference(step,[status(thm)],[t12498,t333]) ).
cnf(t12500,plain,
sFlat7 = composition(converse(sFlat3),sFlat7),
inference(step,[status(thm)],[t12499,t7130]) ).
cnf(t11429,plain,
composition(converse(sFlat3),sFlat7) = sFlat7,
inference(orient,[status(thm)],[t12500]) ).
cnf(t12501,plain,
composition(converse(sFlat3),sk2) = sFlat7,
inference(step,[status(thm)],[t10742,t11429]) ).
cnf(t11430,plain,
composition(converse(sFlat3),sk2) = sFlat7,
inference(orient,[status(thm)],[t12501]) ).
cnf(t11380,plain,
composition(converse(one),sFlat3) = composition(converse(join(sFlat0,sFlat3)),sFlat3),
inference(cp,[status(thm)],[t6880,t11365]) ).
cnf(t12505,plain,
composition(one,sFlat3) = composition(converse(join(sFlat0,sFlat3)),sFlat3),
inference(step,[status(thm)],[t11380,t323]) ).
cnf(t12506,plain,
sFlat3 = composition(converse(join(sFlat0,sFlat3)),sFlat3),
inference(step,[status(thm)],[t12505,t333]) ).
cnf(t12507,plain,
sFlat3 = composition(converse(sFlat3),sFlat3),
inference(step,[status(thm)],[t12506,t6880]) ).
cnf(t11440,plain,
composition(converse(sFlat3),sFlat3) = sFlat3,
inference(orient,[status(thm)],[t12507]) ).
cnf(t11445,plain,
composition(converse(sFlat3),sFlat3) = converse(sFlat3),
inference(cp,[status(thm)],[t304,t11440]) ).
cnf(t12508,plain,
sFlat3 = converse(sFlat3),
inference(step,[status(thm)],[t11445,t11440]) ).
cnf(t11447,plain,
converse(sFlat3) = sFlat3,
inference(orient,[status(thm)],[t12508]) ).
cnf(t12513,plain,
composition(sFlat3,sk2) = sFlat7,
inference(step,[status(thm)],[t11430,t11447]) ).
cnf(t12514,plain,
sFlat4 = sFlat7,
inference(step,[status(thm)],[t12513,t137]) ).
cnf(t11470,plain,
sFlat4 = sFlat7,
inference(rw,[status(thm)],[t12514]) ).
cnf(t11504,plain,
sFlat7 = sFlat4,
inference(orient,[status(thm)],[t11470]) ).
cnf(t12563,plain,
complement(sFlat6) = sFlat4,
inference(step,[status(thm)],[t141,t11504]) ).
cnf(t11505,plain,
complement(sFlat6) = sFlat4,
inference(orient,[status(thm)],[t12563]) ).
cnf(u1,negated_conjecture,
composition(meet(sk1,one),sk2) != meet(sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
composition(complement(join(complement(sk1),complement(one))),sk2) != complement(join(complement(sk1),complement(sk2))),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(g0_0,plain,
composition(complement(join(sFlat0,complement(one))),sk2) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[goal_0,t56]) ).
cnf(g0_1,plain,
composition(complement(join(sFlat0,sFlat1)),sk2) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_0,t65]) ).
cnf(g0_2,plain,
composition(complement(sFlat2),sk2) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_1,t92]) ).
cnf(g0_3,plain,
composition(sFlat3,sk2) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_2,t132]) ).
cnf(g0_4,plain,
sFlat4 != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_3,t137]) ).
cnf(g0_5,plain,
sFlat4 != complement(join(complement(sk2),complement(sk1))),
inference(rw,[status(thm)],[g0_4,t79]) ).
cnf(g0_6,plain,
sFlat4 != complement(join(sFlat5,complement(sk1))),
inference(rw,[status(thm)],[g0_5,t72]) ).
cnf(g0_7,plain,
sFlat4 != complement(join(sFlat5,sFlat0)),
inference(rw,[status(thm)],[g0_6,t56]) ).
cnf(g0_8,plain,
sFlat4 != complement(join(sFlat0,sFlat5)),
inference(rw,[status(thm)],[g0_7,t79]) ).
cnf(g0_9,plain,
sFlat4 != complement(sFlat6),
inference(rw,[status(thm)],[g0_8,t94]) ).
cnf(g0_10,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_9,t11505]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL020-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 07:18:48 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 42.76/5.98 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 42.76/5.98 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------