%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL022-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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:34:49 PM UTC 2026
% Result : Unsatisfiable 55.08s 7.68s
% Output : CNFRefutation 55.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 92
% Number of leaves : 23
% Syntax : Number of clauses : 374 ( 374 unt; 0 nHn; 212 RR)
% Number of literals : 374 ( 373 equ; 19 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 : 211 ( 29 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t80,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t14,axiom,
sFlat1 = complement(sk2),
introduced(definition) ).
cnf(t66,plain,
complement(sk2) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t13,axiom,
sFlat0 = complement(sk1),
introduced(definition) ).
cnf(t57,plain,
complement(sk1) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t15,axiom,
sFlat2 = join(complement(sk1),complement(sk2)),
introduced(definition) ).
cnf(t11815,plain,
sFlat2 = join(complement(sk2),complement(sk1)),
inference(step,[status(thm)],[t15,t80]) ).
cnf(t11816,plain,
sFlat2 = join(sFlat1,complement(sk1)),
inference(step,[status(thm)],[t11815,t66]) ).
cnf(t11817,plain,
sFlat2 = join(sFlat1,sFlat0),
inference(step,[status(thm)],[t11816,t57]) ).
cnf(t11818,plain,
sFlat2 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t11817,t80]) ).
cnf(t95,plain,
join(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t11818]) ).
cnf(t16,axiom,
sFlat3 = complement(join(complement(sk1),complement(sk2))),
introduced(definition) ).
cnf(t39,plain,
complement(join(complement(sk1),complement(sk2))) = sFlat3,
inference(orient,[status(thm)],[t16]) ).
cnf(t11806,plain,
complement(join(sFlat0,complement(sk2))) = sFlat3,
inference(step,[status(thm)],[t39,t57]) ).
cnf(t64,plain,
complement(join(sFlat0,complement(sk2))) = sFlat3,
inference(rw,[status(thm)],[t11806]) ).
cnf(t11829,plain,
complement(join(sFlat0,sFlat1)) = sFlat3,
inference(step,[status(thm)],[t64,t66]) ).
cnf(t11830,plain,
complement(sFlat2) = sFlat3,
inference(step,[status(thm)],[t11829,t95]) ).
cnf(t136,plain,
complement(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t11830]) ).
cnf(t17,axiom,
sFlat4 = complement(one),
introduced(definition) ).
cnf(t73,plain,
complement(one) = sFlat4,
inference(orient,[status(thm)],[t17]) ).
cnf(t18,axiom,
sFlat5 = join(complement(sk1),complement(one)),
introduced(definition) ).
cnf(t11820,plain,
sFlat5 = join(sFlat0,complement(one)),
inference(step,[status(thm)],[t18,t57]) ).
cnf(t11821,plain,
sFlat5 = join(sFlat0,sFlat4),
inference(step,[status(thm)],[t11820,t73]) ).
cnf(t98,plain,
join(sFlat0,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t11821]) ).
cnf(t19,axiom,
sFlat6 = complement(join(complement(sk1),complement(one))),
introduced(definition) ).
cnf(t48,plain,
complement(join(complement(sk1),complement(one))) = sFlat6,
inference(orient,[status(thm)],[t19]) ).
cnf(t11807,plain,
complement(join(sFlat0,complement(one))) = sFlat6,
inference(step,[status(thm)],[t48,t57]) ).
cnf(t65,plain,
complement(join(sFlat0,complement(one))) = sFlat6,
inference(rw,[status(thm)],[t11807]) ).
cnf(t11831,plain,
complement(join(sFlat0,sFlat4)) = sFlat6,
inference(step,[status(thm)],[t65,t73]) ).
cnf(t11832,plain,
complement(sFlat5) = sFlat6,
inference(step,[status(thm)],[t11831,t98]) ).
cnf(t140,plain,
complement(sFlat5) = sFlat6,
inference(orient,[status(thm)],[t11832]) ).
cnf(t20,axiom,
sFlat7 = composition(complement(join(complement(sk1),complement(one))),sk2),
introduced(definition) ).
cnf(t11822,plain,
sFlat7 = composition(complement(join(sFlat0,complement(one))),sk2),
inference(step,[status(thm)],[t20,t57]) ).
cnf(t11823,plain,
sFlat7 = composition(complement(join(sFlat0,sFlat4)),sk2),
inference(step,[status(thm)],[t11822,t73]) ).
cnf(t11824,plain,
sFlat7 = composition(complement(sFlat5),sk2),
inference(step,[status(thm)],[t11823,t98]) ).
cnf(t112,plain,
composition(complement(sFlat5),sk2) = sFlat7,
inference(orient,[status(thm)],[t11824]) ).
cnf(t11833,plain,
composition(sFlat6,sk2) = sFlat7,
inference(step,[status(thm)],[t112,t140]) ).
cnf(t142,plain,
composition(sFlat6,sk2) = sFlat7,
inference(rw,[status(thm)],[t11833]) ).
cnf(t145,plain,
composition(sFlat6,sk2) = sFlat7,
inference(orient,[status(thm)],[t142]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t120,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(t26,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t122,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t120,t26]) ).
cnf(t308,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t122]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t100,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(t27,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t82,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(rw,[status(thm)],[t27]) ).
cnf(t11862,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t82,t80]) ).
cnf(t516,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t11862]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t116,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t543,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t516,t116]) ).
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(t30,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(t83,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t11808,plain,
complement(top) = zero,
inference(step,[status(thm)],[t30,t83]) ).
cnf(t87,plain,
complement(top) = zero,
inference(rw,[status(thm)],[t11808]) ).
cnf(t126,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t87]) ).
cnf(t12067,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t543,t126]) ).
cnf(t12068,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t12067,t126]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t88,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(t25,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t309,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t308,t25]) ).
cnf(t11840,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t309,t26]) ).
cnf(t322,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t11840]) ).
cnf(t323,plain,
one = converse(one),
inference(cp,[status(thm)],[t322,t25]) ).
cnf(t327,plain,
converse(one) = one,
inference(orient,[status(thm)],[t323]) ).
cnf(t525,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t516,t327]) ).
cnf(t11841,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t322,t327]) ).
cnf(t336,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t11841]) ).
cnf(t337,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t336]) ).
cnf(t11863,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t525,t337]) ).
cnf(t11864,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t11863,t337]) ).
cnf(t548,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t11864]) ).
cnf(t551,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t548,t126]) ).
cnf(t11869,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t551,t126]) ).
cnf(t11870,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t11869,t126]) ).
cnf(t574,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t11870]) ).
cnf(t575,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t88,t574]) ).
cnf(t717,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t575]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t81,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t22]) ).
cnf(t11835,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t81,t80]) ).
cnf(t205,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t11835]) ).
cnf(t562,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t205,t548]) ).
cnf(t11907,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t562,t83]) ).
cnf(t11908,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t11907,t126]) ).
cnf(t11909,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t11908,t80]) ).
cnf(t651,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t11909]) ).
cnf(t723,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t717,t651]) ).
cnf(t11938,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t723,t651]) ).
cnf(t742,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t11938]) ).
cnf(t12069,plain,
zero = composition(converse(sk1),complement(sk1)),
inference(step,[status(thm)],[t12068,t742]) ).
cnf(t12070,plain,
zero = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t12069,t57]) ).
cnf(t1654,plain,
composition(converse(sk1),sFlat0) = zero,
inference(orient,[status(thm)],[t12070]) ).
cnf(t1656,plain,
composition(join(converse(sk1),X1),sFlat0) = join(zero,composition(X1,sFlat0)),
inference(cp,[status(thm)],[t100,t1654]) ).
cnf(t12090,plain,
composition(join(converse(sk1),X1),sFlat0) = composition(X1,sFlat0),
inference(step,[status(thm)],[t1656,t742]) ).
cnf(t1825,plain,
composition(join(converse(sk1),X1),sFlat0) = composition(X1,sFlat0),
inference(orient,[status(thm)],[t12090]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t103,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t1826,plain,
composition(converse(X1),sFlat0) = composition(converse(join(sk1,X1)),sFlat0),
inference(cp,[status(thm)],[t1825,t103]) ).
cnf(t5861,plain,
composition(converse(join(sk1,X1)),sFlat0) = composition(converse(X1),sFlat0),
inference(orient,[status(thm)],[t1826]) ).
cnf(t119,plain,
composition(join(X1,sk1),top) = join(composition(X1,top),sk1),
inference(cp,[status(thm)],[t100,t116]) ).
cnf(t11848,plain,
composition(join(X1,sk1),top) = join(sk1,composition(X1,top)),
inference(step,[status(thm)],[t119,t80]) ).
cnf(t416,plain,
composition(join(X1,sk1),top) = join(sk1,composition(X1,top)),
inference(orient,[status(thm)],[t11848]) ).
cnf(t11945,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t651,t742]) ).
cnf(t766,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t11945]) ).
cnf(t896,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t766]) ).
cnf(t897,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t548,t896]) ).
cnf(t11999,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t897,t896]) ).
cnf(t12000,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t11999,t896]) ).
cnf(t974,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t12000]) ).
cnf(t986,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t88,t974]) ).
cnf(t1207,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t986]) ).
cnf(t1214,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = join(complement(join(complement(X1),X2)),X1),
inference(cp,[status(thm)],[t1207,t205]) ).
cnf(t12207,plain,
X1 = join(complement(join(complement(X1),X2)),X1),
inference(step,[status(thm)],[t1214,t205]) ).
cnf(t12208,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t12207,t80]) ).
cnf(t2816,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12208]) ).
cnf(t2832,plain,
sk1 = join(sk1,complement(join(sFlat0,X1))),
inference(cp,[status(thm)],[t2816,t57]) ).
cnf(t3162,plain,
join(sk1,complement(join(sFlat0,X1))) = sk1,
inference(orient,[status(thm)],[t2832]) ).
cnf(t652,plain,
sFlat5 = join(zero,complement(sFlat6)),
inference(cp,[status(thm)],[t651,t140]) ).
cnf(t658,plain,
join(zero,complement(sFlat6)) = sFlat5,
inference(orient,[status(thm)],[t652]) ).
cnf(t11943,plain,
complement(sFlat6) = sFlat5,
inference(step,[status(thm)],[t658,t742]) ).
cnf(t764,plain,
complement(sFlat6) = sFlat5,
inference(rw,[status(thm)],[t11943]) ).
cnf(t804,plain,
complement(sFlat6) = sFlat5,
inference(orient,[status(thm)],[t764]) ).
cnf(t805,plain,
complement(sFlat6) = join(sFlat5,complement(sFlat6)),
inference(cp,[status(thm)],[t548,t804]) ).
cnf(t11970,plain,
sFlat5 = join(sFlat5,complement(sFlat6)),
inference(step,[status(thm)],[t805,t804]) ).
cnf(t11971,plain,
sFlat5 = join(sFlat5,sFlat5),
inference(step,[status(thm)],[t11970,t804]) ).
cnf(t99,plain,
join(sFlat0,join(sFlat4,X1)) = join(sFlat5,X1),
inference(cp,[status(thm)],[t88,t98]) ).
cnf(t157,plain,
join(sFlat0,join(sFlat4,X1)) = join(sFlat5,X1),
inference(orient,[status(thm)],[t99]) ).
cnf(t160,plain,
join(sFlat5,X1) = join(sFlat0,join(X1,sFlat4)),
inference(cp,[status(thm)],[t157,t80]) ).
cnf(t233,plain,
join(sFlat0,join(X1,sFlat4)) = join(sFlat5,X1),
inference(orient,[status(thm)],[t160]) ).
cnf(t552,plain,
complement(one) = join(sFlat4,complement(one)),
inference(cp,[status(thm)],[t548,t73]) ).
cnf(t11871,plain,
sFlat4 = join(sFlat4,complement(one)),
inference(step,[status(thm)],[t552,t73]) ).
cnf(t11872,plain,
sFlat4 = join(sFlat4,sFlat4),
inference(step,[status(thm)],[t11871,t73]) ).
cnf(t576,plain,
join(sFlat4,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t11872]) ).
cnf(t579,plain,
join(sFlat5,sFlat4) = join(sFlat0,sFlat4),
inference(cp,[status(thm)],[t233,t576]) ).
cnf(t11887,plain,
join(sFlat4,sFlat5) = join(sFlat0,sFlat4),
inference(step,[status(thm)],[t579,t80]) ).
cnf(t11888,plain,
join(sFlat4,sFlat5) = sFlat5,
inference(step,[status(thm)],[t11887,t98]) ).
cnf(t603,plain,
join(sFlat4,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t11888]) ).
cnf(t605,plain,
join(sFlat5,sFlat5) = join(sFlat0,sFlat5),
inference(cp,[status(thm)],[t157,t603]) ).
cnf(t647,plain,
join(sFlat5,sFlat5) = join(sFlat0,sFlat5),
inference(orient,[status(thm)],[t605]) ).
cnf(t11972,plain,
sFlat5 = join(sFlat0,sFlat5),
inference(step,[status(thm)],[t11971,t647]) ).
cnf(t941,plain,
join(sFlat0,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t11972]) ).
cnf(t3167,plain,
sk1 = join(sk1,complement(sFlat5)),
inference(cp,[status(thm)],[t3162,t941]) ).
cnf(t12218,plain,
sk1 = join(sk1,sFlat6),
inference(step,[status(thm)],[t3167,t140]) ).
cnf(t12219,plain,
sk1 = join(sFlat6,sk1),
inference(step,[status(thm)],[t12218,t80]) ).
cnf(t3184,plain,
join(sFlat6,sk1) = sk1,
inference(orient,[status(thm)],[t12219]) ).
cnf(t3187,plain,
join(sk1,composition(sFlat6,top)) = composition(sk1,top),
inference(cp,[status(thm)],[t416,t3184]) ).
cnf(t12222,plain,
join(sk1,composition(sFlat6,top)) = sk1,
inference(step,[status(thm)],[t3187,t116]) ).
cnf(t3201,plain,
join(sk1,composition(sFlat6,top)) = sk1,
inference(orient,[status(thm)],[t12222]) ).
cnf(t5875,plain,
composition(converse(composition(sFlat6,top)),sFlat0) = composition(converse(sk1),sFlat0),
inference(cp,[status(thm)],[t5861,t3201]) ).
cnf(t89,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t88,t83]) ).
cnf(t819,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t89]) ).
cnf(t988,plain,
top = join(X1,join(X1,complement(X1))),
inference(cp,[status(thm)],[t819,t974]) ).
cnf(t12001,plain,
top = join(X1,top),
inference(step,[status(thm)],[t988,t83]) ).
cnf(t989,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t12001]) ).
cnf(t990,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t989,t80]) ).
cnf(t996,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t990]) ).
cnf(t105,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t103,t26]) ).
cnf(t280,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t105]) ).
cnf(t281,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t280,t83]) ).
cnf(t381,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t281]) ).
cnf(t1031,plain,
top = converse(top),
inference(cp,[status(thm)],[t996,t381]) ).
cnf(t1041,plain,
converse(top) = top,
inference(orient,[status(thm)],[t1031]) ).
cnf(t1046,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t120,t1041]) ).
cnf(t1087,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t1046]) ).
cnf(t12332,plain,
composition(composition(top,converse(sFlat6)),sFlat0) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t5875,t1087]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t108,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t12333,plain,
composition(top,composition(converse(sFlat6),sFlat0)) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t12332,t108]) ).
cnf(t12334,plain,
composition(top,composition(converse(sFlat6),sFlat0)) = zero,
inference(step,[status(thm)],[t12333,t1654]) ).
cnf(t5900,plain,
composition(top,composition(converse(sFlat6),sFlat0)) = zero,
inference(orient,[status(thm)],[t12334]) ).
cnf(t5904,plain,
composition(join(top,X1),composition(converse(sFlat6),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat6),sFlat0))),
inference(cp,[status(thm)],[t100,t5900]) ).
cnf(t12351,plain,
composition(top,composition(converse(sFlat6),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat6),sFlat0))),
inference(step,[status(thm)],[t5904,t996]) ).
cnf(t12352,plain,
zero = join(zero,composition(X1,composition(converse(sFlat6),sFlat0))),
inference(step,[status(thm)],[t12351,t5900]) ).
cnf(t12353,plain,
zero = composition(X1,composition(converse(sFlat6),sFlat0)),
inference(step,[status(thm)],[t12352,t742]) ).
cnf(t5961,plain,
composition(X1,composition(converse(sFlat6),sFlat0)) = zero,
inference(orient,[status(thm)],[t12353]) ).
cnf(t5962,plain,
zero = composition(converse(sFlat6),sFlat0),
inference(cp,[status(thm)],[t5961,t337]) ).
cnf(t5970,plain,
composition(converse(sFlat6),sFlat0) = zero,
inference(orient,[status(thm)],[t5962]) ).
cnf(t5975,plain,
composition(converse(sFlat0),sFlat6) = converse(zero),
inference(cp,[status(thm)],[t308,t5970]) ).
cnf(t106,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t103,t26]) ).
cnf(t288,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t106]) ).
cnf(t759,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t288,t742]) ).
cnf(t12062,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t759,t26]) ).
cnf(t1058,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t12062]) ).
cnf(t745,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t742,t80]) ).
cnf(t813,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t745]) ).
cnf(t1059,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t1058,t813]) ).
cnf(t1068,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t1059]) ).
cnf(t12354,plain,
composition(converse(sFlat0),sFlat6) = zero,
inference(step,[status(thm)],[t5975,t1068]) ).
cnf(t5976,plain,
composition(converse(sFlat0),sFlat6) = zero,
inference(orient,[status(thm)],[t12354]) ).
cnf(t5978,plain,
composition(join(converse(sFlat0),X1),sFlat6) = join(zero,composition(X1,sFlat6)),
inference(cp,[status(thm)],[t100,t5976]) ).
cnf(t12407,plain,
composition(join(converse(sFlat0),X1),sFlat6) = composition(X1,sFlat6),
inference(step,[status(thm)],[t5978,t742]) ).
cnf(t6498,plain,
composition(join(converse(sFlat0),X1),sFlat6) = composition(X1,sFlat6),
inference(orient,[status(thm)],[t12407]) ).
cnf(t6499,plain,
composition(converse(X1),sFlat6) = composition(converse(join(sFlat0,X1)),sFlat6),
inference(cp,[status(thm)],[t6498,t103]) ).
cnf(t8581,plain,
composition(converse(join(sFlat0,X1)),sFlat6) = composition(converse(X1),sFlat6),
inference(orient,[status(thm)],[t6499]) ).
cnf(t8617,plain,
composition(converse(sFlat6),join(sFlat0,X1)) = converse(composition(converse(X1),sFlat6)),
inference(cp,[status(thm)],[t308,t8581]) ).
cnf(t12702,plain,
composition(converse(sFlat6),join(sFlat0,X1)) = composition(converse(sFlat6),X1),
inference(step,[status(thm)],[t8617,t308]) ).
cnf(t9805,plain,
composition(converse(sFlat6),join(sFlat0,X1)) = composition(converse(sFlat6),X1),
inference(orient,[status(thm)],[t12702]) ).
cnf(t222,plain,
X1 = join(complement(join(complement(X1),sFlat5)),complement(join(complement(X1),sFlat6))),
inference(cp,[status(thm)],[t205,t140]) ).
cnf(t12762,plain,
X1 = join(complement(join(sFlat5,complement(X1))),complement(join(complement(X1),sFlat6))),
inference(step,[status(thm)],[t222,t80]) ).
cnf(t12763,plain,
X1 = join(complement(join(sFlat5,complement(X1))),complement(join(sFlat6,complement(X1)))),
inference(step,[status(thm)],[t12762,t80]) ).
cnf(t10950,plain,
join(complement(join(sFlat5,complement(X1))),complement(join(sFlat6,complement(X1)))) = X1,
inference(orient,[status(thm)],[t12763]) ).
cnf(t213,plain,
sk1 = join(complement(join(sFlat0,X1)),complement(join(complement(sk1),complement(X1)))),
inference(cp,[status(thm)],[t205,t57]) ).
cnf(t12650,plain,
sk1 = join(complement(join(sFlat0,X1)),complement(join(sFlat0,complement(X1)))),
inference(step,[status(thm)],[t213,t57]) ).
cnf(t9297,plain,
join(complement(join(sFlat0,X1)),complement(join(sFlat0,complement(X1)))) = sk1,
inference(orient,[status(thm)],[t12650]) ).
cnf(t9322,plain,
sk1 = join(complement(sFlat5),complement(join(sFlat0,complement(sFlat4)))),
inference(cp,[status(thm)],[t9297,t98]) ).
cnf(t12662,plain,
sk1 = join(sFlat6,complement(join(sFlat0,complement(sFlat4)))),
inference(step,[status(thm)],[t9322,t140]) ).
cnf(t654,plain,
one = join(zero,complement(sFlat4)),
inference(cp,[status(thm)],[t651,t73]) ).
cnf(t662,plain,
join(zero,complement(sFlat4)) = one,
inference(orient,[status(thm)],[t654]) ).
cnf(t11941,plain,
complement(sFlat4) = one,
inference(step,[status(thm)],[t662,t742]) ).
cnf(t762,plain,
complement(sFlat4) = one,
inference(rw,[status(thm)],[t11941]) ).
cnf(t788,plain,
complement(sFlat4) = one,
inference(orient,[status(thm)],[t762]) ).
cnf(t12663,plain,
sk1 = join(sFlat6,complement(join(sFlat0,one))),
inference(step,[status(thm)],[t12662,t788]) ).
cnf(t9413,plain,
join(sFlat6,complement(join(sFlat0,one))) = sk1,
inference(orient,[status(thm)],[t12663]) ).
cnf(t10970,plain,
join(sFlat0,one) = join(complement(join(sFlat5,complement(join(sFlat0,one)))),complement(sk1)),
inference(cp,[status(thm)],[t10950,t9413]) ).
cnf(t12764,plain,
join(sFlat0,one) = join(complement(sk1),complement(join(sFlat5,complement(join(sFlat0,one))))),
inference(step,[status(thm)],[t10970,t80]) ).
cnf(t12765,plain,
join(sFlat0,one) = join(sFlat0,complement(join(sFlat5,complement(join(sFlat0,one))))),
inference(step,[status(thm)],[t12764,t57]) ).
cnf(t2828,plain,
sFlat5 = join(sFlat5,complement(join(sFlat6,X1))),
inference(cp,[status(thm)],[t2816,t140]) ).
cnf(t2918,plain,
join(sFlat5,complement(join(sFlat6,X1))) = sFlat5,
inference(orient,[status(thm)],[t2828]) ).
cnf(t92,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t88,t80]) ).
cnf(t12132,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t92,t88]) ).
cnf(t1963,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t12132]) ).
cnf(t2830,plain,
one = join(one,complement(join(sFlat4,X1))),
inference(cp,[status(thm)],[t2816,t73]) ).
cnf(t2952,plain,
join(one,complement(join(sFlat4,X1))) = one,
inference(orient,[status(thm)],[t2830]) ).
cnf(t2957,plain,
one = join(one,complement(sFlat5)),
inference(cp,[status(thm)],[t2952,t603]) ).
cnf(t12209,plain,
one = join(one,sFlat6),
inference(step,[status(thm)],[t2957,t140]) ).
cnf(t12210,plain,
one = join(sFlat6,one),
inference(step,[status(thm)],[t12209,t80]) ).
cnf(t2967,plain,
join(sFlat6,one) = one,
inference(orient,[status(thm)],[t12210]) ).
cnf(t2973,plain,
join(sFlat6,join(X1,one)) = join(X1,one),
inference(cp,[status(thm)],[t1963,t2967]) ).
cnf(t3021,plain,
join(sFlat6,join(X1,one)) = join(X1,one),
inference(orient,[status(thm)],[t2973]) ).
cnf(t3028,plain,
sFlat5 = join(sFlat5,complement(join(X1,one))),
inference(cp,[status(thm)],[t2918,t3021]) ).
cnf(t3460,plain,
join(sFlat5,complement(join(X1,one))) = sFlat5,
inference(orient,[status(thm)],[t3028]) ).
cnf(t12766,plain,
join(sFlat0,one) = join(sFlat0,complement(sFlat5)),
inference(step,[status(thm)],[t12765,t3460]) ).
cnf(t12767,plain,
join(sFlat0,one) = join(sFlat0,sFlat6),
inference(step,[status(thm)],[t12766,t140]) ).
cnf(t11001,plain,
join(sFlat0,one) = join(sFlat0,sFlat6),
inference(orient,[status(thm)],[t12767]) ).
cnf(t11016,plain,
composition(converse(one),sFlat6) = composition(converse(join(sFlat0,sFlat6)),sFlat6),
inference(cp,[status(thm)],[t8581,t11001]) ).
cnf(t12791,plain,
composition(one,sFlat6) = composition(converse(join(sFlat0,sFlat6)),sFlat6),
inference(step,[status(thm)],[t11016,t327]) ).
cnf(t12792,plain,
sFlat6 = composition(converse(join(sFlat0,sFlat6)),sFlat6),
inference(step,[status(thm)],[t12791,t337]) ).
cnf(t12793,plain,
sFlat6 = composition(converse(sFlat6),sFlat6),
inference(step,[status(thm)],[t12792,t8581]) ).
cnf(t11063,plain,
composition(converse(sFlat6),sFlat6) = sFlat6,
inference(orient,[status(thm)],[t12793]) ).
cnf(t11068,plain,
composition(converse(sFlat6),sFlat6) = converse(sFlat6),
inference(cp,[status(thm)],[t308,t11063]) ).
cnf(t12794,plain,
sFlat6 = converse(sFlat6),
inference(step,[status(thm)],[t11068,t11063]) ).
cnf(t11070,plain,
converse(sFlat6) = sFlat6,
inference(orient,[status(thm)],[t12794]) ).
cnf(t12800,plain,
composition(sFlat6,join(sFlat0,X1)) = composition(converse(sFlat6),X1),
inference(step,[status(thm)],[t9805,t11070]) ).
cnf(t12801,plain,
composition(sFlat6,join(sFlat0,X1)) = composition(sFlat6,X1),
inference(step,[status(thm)],[t12800,t11070]) ).
cnf(t11093,plain,
composition(sFlat6,join(sFlat0,X1)) = composition(sFlat6,X1),
inference(rw,[status(thm)],[t12801]) ).
cnf(t11600,plain,
composition(sFlat6,join(sFlat0,X1)) = composition(sFlat6,X1),
inference(orient,[status(thm)],[t11093]) ).
cnf(t223,plain,
X1 = join(complement(join(complement(X1),sFlat2)),complement(join(complement(X1),sFlat3))),
inference(cp,[status(thm)],[t205,t136]) ).
cnf(t12956,plain,
X1 = join(complement(join(sFlat2,complement(X1))),complement(join(complement(X1),sFlat3))),
inference(step,[status(thm)],[t223,t80]) ).
cnf(t12957,plain,
X1 = join(complement(join(sFlat2,complement(X1))),complement(join(sFlat3,complement(X1)))),
inference(step,[status(thm)],[t12956,t80]) ).
cnf(t11678,plain,
join(complement(join(sFlat2,complement(X1))),complement(join(sFlat3,complement(X1)))) = X1,
inference(orient,[status(thm)],[t12957]) ).
cnf(t9321,plain,
sk1 = join(complement(sFlat2),complement(join(sFlat0,complement(sFlat1)))),
inference(cp,[status(thm)],[t9297,t95]) ).
cnf(t12660,plain,
sk1 = join(sFlat3,complement(join(sFlat0,complement(sFlat1)))),
inference(step,[status(thm)],[t9321,t136]) ).
cnf(t655,plain,
sk2 = join(zero,complement(sFlat1)),
inference(cp,[status(thm)],[t651,t66]) ).
cnf(t664,plain,
join(zero,complement(sFlat1)) = sk2,
inference(orient,[status(thm)],[t655]) ).
cnf(t11940,plain,
complement(sFlat1) = sk2,
inference(step,[status(thm)],[t664,t742]) ).
cnf(t761,plain,
complement(sFlat1) = sk2,
inference(rw,[status(thm)],[t11940]) ).
cnf(t781,plain,
complement(sFlat1) = sk2,
inference(orient,[status(thm)],[t761]) ).
cnf(t12661,plain,
sk1 = join(sFlat3,complement(join(sFlat0,sk2))),
inference(step,[status(thm)],[t12660,t781]) ).
cnf(t9402,plain,
join(sFlat3,complement(join(sFlat0,sk2))) = sk1,
inference(orient,[status(thm)],[t12661]) ).
cnf(t11699,plain,
join(sFlat0,sk2) = join(complement(join(sFlat2,complement(join(sFlat0,sk2)))),complement(sk1)),
inference(cp,[status(thm)],[t11678,t9402]) ).
cnf(t12958,plain,
join(sFlat0,sk2) = join(complement(sk1),complement(join(sFlat2,complement(join(sFlat0,sk2))))),
inference(step,[status(thm)],[t11699,t80]) ).
cnf(t12959,plain,
join(sFlat0,sk2) = join(sFlat0,complement(join(sFlat2,complement(join(sFlat0,sk2))))),
inference(step,[status(thm)],[t12958,t57]) ).
cnf(t2829,plain,
sFlat2 = join(sFlat2,complement(join(sFlat3,X1))),
inference(cp,[status(thm)],[t2816,t136]) ).
cnf(t2929,plain,
join(sFlat2,complement(join(sFlat3,X1))) = sFlat2,
inference(orient,[status(thm)],[t2829]) ).
cnf(t2831,plain,
sk2 = join(sk2,complement(join(sFlat1,X1))),
inference(cp,[status(thm)],[t2816,t66]) ).
cnf(t3063,plain,
join(sk2,complement(join(sFlat1,X1))) = sk2,
inference(orient,[status(thm)],[t2831]) ).
cnf(t96,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t88,t95]) ).
cnf(t149,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t96]) ).
cnf(t152,plain,
join(sFlat2,X1) = join(sFlat0,join(X1,sFlat1)),
inference(cp,[status(thm)],[t149,t80]) ).
cnf(t197,plain,
join(sFlat0,join(X1,sFlat1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t152]) ).
cnf(t553,plain,
complement(sk2) = join(sFlat1,complement(sk2)),
inference(cp,[status(thm)],[t548,t66]) ).
cnf(t11873,plain,
sFlat1 = join(sFlat1,complement(sk2)),
inference(step,[status(thm)],[t553,t66]) ).
cnf(t11874,plain,
sFlat1 = join(sFlat1,sFlat1),
inference(step,[status(thm)],[t11873,t66]) ).
cnf(t582,plain,
join(sFlat1,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t11874]) ).
cnf(t583,plain,
join(sFlat2,sFlat1) = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t197,t582]) ).
cnf(t11889,plain,
join(sFlat1,sFlat2) = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t583,t80]) ).
cnf(t11890,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t11889,t95]) ).
cnf(t607,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t11890]) ).
cnf(t3066,plain,
sk2 = join(sk2,complement(sFlat2)),
inference(cp,[status(thm)],[t3063,t607]) ).
cnf(t12214,plain,
sk2 = join(sk2,sFlat3),
inference(step,[status(thm)],[t3066,t136]) ).
cnf(t12215,plain,
sk2 = join(sFlat3,sk2),
inference(step,[status(thm)],[t12214,t80]) ).
cnf(t3128,plain,
join(sFlat3,sk2) = sk2,
inference(orient,[status(thm)],[t12215]) ).
cnf(t3134,plain,
join(sFlat3,join(X1,sk2)) = join(X1,sk2),
inference(cp,[status(thm)],[t1963,t3128]) ).
cnf(t3152,plain,
join(sFlat3,join(X1,sk2)) = join(X1,sk2),
inference(orient,[status(thm)],[t3134]) ).
cnf(t3158,plain,
sFlat2 = join(sFlat2,complement(join(X1,sk2))),
inference(cp,[status(thm)],[t2929,t3152]) ).
cnf(t3514,plain,
join(sFlat2,complement(join(X1,sk2))) = sFlat2,
inference(orient,[status(thm)],[t3158]) ).
cnf(t12960,plain,
join(sFlat0,sk2) = join(sFlat0,complement(sFlat2)),
inference(step,[status(thm)],[t12959,t3514]) ).
cnf(t12961,plain,
join(sFlat0,sk2) = join(sFlat0,sFlat3),
inference(step,[status(thm)],[t12960,t136]) ).
cnf(t11733,plain,
join(sFlat0,sk2) = join(sFlat0,sFlat3),
inference(orient,[status(thm)],[t12961]) ).
cnf(t11734,plain,
composition(sFlat6,sk2) = composition(sFlat6,join(sFlat0,sFlat3)),
inference(cp,[status(thm)],[t11600,t11733]) ).
cnf(t12962,plain,
sFlat7 = composition(sFlat6,join(sFlat0,sFlat3)),
inference(step,[status(thm)],[t11734,t145]) ).
cnf(t12963,plain,
sFlat7 = composition(sFlat6,sFlat3),
inference(step,[status(thm)],[t12962,t11600]) ).
cnf(t653,plain,
sFlat2 = join(zero,complement(sFlat3)),
inference(cp,[status(thm)],[t651,t136]) ).
cnf(t660,plain,
join(zero,complement(sFlat3)) = sFlat2,
inference(orient,[status(thm)],[t653]) ).
cnf(t11942,plain,
complement(sFlat3) = sFlat2,
inference(step,[status(thm)],[t660,t742]) ).
cnf(t763,plain,
complement(sFlat3) = sFlat2,
inference(rw,[status(thm)],[t11942]) ).
cnf(t795,plain,
complement(sFlat3) = sFlat2,
inference(orient,[status(thm)],[t763]) ).
cnf(t796,plain,
complement(sFlat3) = join(sFlat2,complement(sFlat3)),
inference(cp,[status(thm)],[t548,t795]) ).
cnf(t11965,plain,
sFlat2 = join(sFlat2,complement(sFlat3)),
inference(step,[status(thm)],[t796,t795]) ).
cnf(t11966,plain,
sFlat2 = join(sFlat2,sFlat2),
inference(step,[status(thm)],[t11965,t795]) ).
cnf(t608,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t149,t607]) ).
cnf(t649,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(orient,[status(thm)],[t608]) ).
cnf(t11967,plain,
sFlat2 = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t11966,t649]) ).
cnf(t936,plain,
join(sFlat0,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t11967]) ).
cnf(t3168,plain,
sk1 = join(sk1,complement(sFlat2)),
inference(cp,[status(thm)],[t3162,t936]) ).
cnf(t12220,plain,
sk1 = join(sk1,sFlat3),
inference(step,[status(thm)],[t3168,t136]) ).
cnf(t12221,plain,
sk1 = join(sFlat3,sk1),
inference(step,[status(thm)],[t12220,t80]) ).
cnf(t3193,plain,
join(sFlat3,sk1) = sk1,
inference(orient,[status(thm)],[t12221]) ).
cnf(t3195,plain,
join(sk1,composition(sFlat3,top)) = composition(sk1,top),
inference(cp,[status(thm)],[t416,t3193]) ).
cnf(t12223,plain,
join(sk1,composition(sFlat3,top)) = sk1,
inference(step,[status(thm)],[t3195,t116]) ).
cnf(t3207,plain,
join(sk1,composition(sFlat3,top)) = sk1,
inference(orient,[status(thm)],[t12223]) ).
cnf(t5873,plain,
composition(converse(composition(sFlat3,top)),sFlat0) = composition(converse(sk1),sFlat0),
inference(cp,[status(thm)],[t5861,t3207]) ).
cnf(t12329,plain,
composition(composition(top,converse(sFlat3)),sFlat0) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t5873,t1087]) ).
cnf(t12330,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = composition(converse(sk1),sFlat0),
inference(step,[status(thm)],[t12329,t108]) ).
cnf(t12331,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = zero,
inference(step,[status(thm)],[t12330,t1654]) ).
cnf(t5893,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = zero,
inference(orient,[status(thm)],[t12331]) ).
cnf(t5897,plain,
composition(join(top,X1),composition(converse(sFlat3),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat3),sFlat0))),
inference(cp,[status(thm)],[t100,t5893]) ).
cnf(t12339,plain,
composition(top,composition(converse(sFlat3),sFlat0)) = join(zero,composition(X1,composition(converse(sFlat3),sFlat0))),
inference(step,[status(thm)],[t5897,t996]) ).
cnf(t12340,plain,
zero = join(zero,composition(X1,composition(converse(sFlat3),sFlat0))),
inference(step,[status(thm)],[t12339,t5893]) ).
cnf(t12341,plain,
zero = composition(X1,composition(converse(sFlat3),sFlat0)),
inference(step,[status(thm)],[t12340,t742]) ).
cnf(t5918,plain,
composition(X1,composition(converse(sFlat3),sFlat0)) = zero,
inference(orient,[status(thm)],[t12341]) ).
cnf(t5919,plain,
zero = composition(converse(sFlat3),sFlat0),
inference(cp,[status(thm)],[t5918,t337]) ).
cnf(t5927,plain,
composition(converse(sFlat3),sFlat0) = zero,
inference(orient,[status(thm)],[t5919]) ).
cnf(t5932,plain,
composition(converse(sFlat0),sFlat3) = converse(zero),
inference(cp,[status(thm)],[t308,t5927]) ).
cnf(t12342,plain,
composition(converse(sFlat0),sFlat3) = zero,
inference(step,[status(thm)],[t5932,t1068]) ).
cnf(t5933,plain,
composition(converse(sFlat0),sFlat3) = zero,
inference(orient,[status(thm)],[t12342]) ).
cnf(t5935,plain,
composition(join(converse(sFlat0),X1),sFlat3) = join(zero,composition(X1,sFlat3)),
inference(cp,[status(thm)],[t100,t5933]) ).
cnf(t12381,plain,
composition(join(converse(sFlat0),X1),sFlat3) = composition(X1,sFlat3),
inference(step,[status(thm)],[t5935,t742]) ).
cnf(t6119,plain,
composition(join(converse(sFlat0),X1),sFlat3) = composition(X1,sFlat3),
inference(orient,[status(thm)],[t12381]) ).
cnf(t6120,plain,
composition(converse(X1),sFlat3) = composition(converse(join(sFlat0,X1)),sFlat3),
inference(cp,[status(thm)],[t6119,t103]) ).
cnf(t8176,plain,
composition(converse(join(sFlat0,X1)),sFlat3) = composition(converse(X1),sFlat3),
inference(orient,[status(thm)],[t6120]) ).
cnf(t11017,plain,
composition(converse(one),sFlat3) = composition(converse(join(sFlat0,sFlat6)),sFlat3),
inference(cp,[status(thm)],[t8176,t11001]) ).
cnf(t12910,plain,
composition(one,sFlat3) = composition(converse(join(sFlat0,sFlat6)),sFlat3),
inference(step,[status(thm)],[t11017,t327]) ).
cnf(t12911,plain,
sFlat3 = composition(converse(join(sFlat0,sFlat6)),sFlat3),
inference(step,[status(thm)],[t12910,t337]) ).
cnf(t12912,plain,
sFlat3 = composition(converse(sFlat6),sFlat3),
inference(step,[status(thm)],[t12911,t8176]) ).
cnf(t12913,plain,
sFlat3 = composition(sFlat6,sFlat3),
inference(step,[status(thm)],[t12912,t11070]) ).
cnf(t11232,plain,
composition(sFlat6,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t12913]) ).
cnf(t12964,plain,
sFlat7 = sFlat3,
inference(step,[status(thm)],[t12963,t11232]) ).
cnf(t11761,plain,
sFlat7 = sFlat3,
inference(orient,[status(thm)],[t12964]) ).
cnf(t12965,plain,
composition(sFlat6,sk2) = sFlat3,
inference(step,[status(thm)],[t145,t11761]) ).
cnf(t11762,plain,
composition(sFlat6,sk2) = sFlat3,
inference(orient,[status(thm)],[t12965]) ).
cnf(u1,negated_conjecture,
join(meet(sk1,sk2),composition(meet(sk1,one),sk2)) != composition(meet(sk1,one),sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(g0_0,plain,
join(complement(join(complement(sk2),complement(sk1))),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[goal_0,t80]) ).
cnf(g0_1,plain,
join(complement(join(sFlat1,complement(sk1))),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_0,t66]) ).
cnf(g0_2,plain,
join(complement(join(sFlat1,sFlat0)),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_1,t57]) ).
cnf(g0_3,plain,
join(complement(join(sFlat0,sFlat1)),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_2,t80]) ).
cnf(g0_4,plain,
join(complement(sFlat2),composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_3,t95]) ).
cnf(g0_5,plain,
join(sFlat3,composition(complement(join(complement(sk1),complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_4,t136]) ).
cnf(g0_6,plain,
join(sFlat3,composition(complement(join(sFlat0,complement(one))),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_5,t57]) ).
cnf(g0_7,plain,
join(sFlat3,composition(complement(join(sFlat0,sFlat4)),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_6,t73]) ).
cnf(g0_8,plain,
join(sFlat3,composition(complement(sFlat5),sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_7,t98]) ).
cnf(g0_9,plain,
join(sFlat3,composition(sFlat6,sk2)) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_8,t140]) ).
cnf(g0_10,plain,
join(sFlat3,sFlat3) != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_9,t11762]) ).
cnf(g0_11,plain,
sFlat3 != composition(complement(join(complement(sk1),complement(one))),sk2),
inference(rw,[status(thm)],[g0_10,t974]) ).
cnf(g0_12,plain,
sFlat3 != composition(complement(join(sFlat0,complement(one))),sk2),
inference(rw,[status(thm)],[g0_11,t57]) ).
cnf(g0_13,plain,
sFlat3 != composition(complement(join(sFlat0,sFlat4)),sk2),
inference(rw,[status(thm)],[g0_12,t73]) ).
cnf(g0_14,plain,
sFlat3 != composition(complement(sFlat5),sk2),
inference(rw,[status(thm)],[g0_13,t98]) ).
cnf(g0_15,plain,
sFlat3 != composition(sFlat6,sk2),
inference(rw,[status(thm)],[g0_14,t140]) ).
cnf(g0_16,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_15,t11762]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL022-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.52 % Computer : n017.cluster.edu
% 0.08/0.52 % Model : x86_64 x86_64
% 0.08/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.52 % Memory : 8046.5625MB
% 0.08/0.52 % OS : Linux 6.8.0-71-generic
% 0.08/0.52 % CPULimit : 300
% 0.08/0.52 % WCLimit : 300
% 0.08/0.52 % DateTime : Thu Sep 24 07:13:16 UTC 2026
% 0.08/0.52 % CPUTime :
% 0.08/0.52 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 55.08/7.68 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 55.08/7.68 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------