%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL035-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n026.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:57 PM UTC 2026
% Result : Unsatisfiable 65.49s 8.93s
% Output : CNFRefutation 65.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 21
% Syntax : Number of clauses : 290 ( 290 unt; 0 nHn; 89 RR)
% Number of literals : 290 ( 289 equ; 10 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 : 16 ( 16 usr; 11 con; 0-2 aty)
% Number of variables : 302 ( 72 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t17,axiom,
sFlat0 = converse(sk1),
introduced(definition) ).
cnf(t101,plain,
converse(sk1) = sFlat0,
inference(orient,[status(thm)],[t17]) ).
cnf(t6,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t63,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t112,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t115,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t63,t112]) ).
cnf(t47398,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t115,t63]) ).
cnf(t296,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t47398]) ).
cnf(t18,axiom,
sFlat1 = meet(sk2,converse(sk1)),
introduced(definition) ).
cnf(t97,plain,
meet(sk2,converse(sk1)) = sFlat1,
inference(orient,[status(thm)],[t18]) ).
cnf(t47389,plain,
meet(sk2,sFlat0) = sFlat1,
inference(step,[status(thm)],[t97,t101]) ).
cnf(t111,plain,
meet(sk2,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t47389]) ).
cnf(t162,plain,
meet(sk2,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t111]) ).
cnf(t301,plain,
meet(sk2,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t162]) ).
cnf(t47400,plain,
meet(sFlat0,sk2) = sFlat1,
inference(step,[status(thm)],[t301,t296]) ).
cnf(t306,plain,
meet(sFlat0,sk2) = sFlat1,
inference(orient,[status(thm)],[t47400]) ).
cnf(t19,axiom,
sFlat2 = meet(sk1,sk3),
introduced(definition) ).
cnf(t94,plain,
meet(sk1,sk3) = sFlat2,
inference(orient,[status(thm)],[t19]) ).
cnf(t302,plain,
meet(sk1,sk3) = sFlat2,
inference(rw,[status(thm)],[t94]) ).
cnf(t47401,plain,
meet(sk3,sk1) = sFlat2,
inference(step,[status(thm)],[t302,t296]) ).
cnf(t307,plain,
meet(sk3,sk1) = sFlat2,
inference(orient,[status(thm)],[t47401]) ).
cnf(t20,axiom,
sFlat3 = composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
introduced(definition) ).
cnf(t36,plain,
composition(meet(sk2,converse(sk1)),meet(sk1,sk3)) = sFlat3,
inference(orient,[status(thm)],[t20]) ).
cnf(t47388,plain,
composition(meet(sk2,converse(sk1)),sFlat2) = sFlat3,
inference(step,[status(thm)],[t36,t94]) ).
cnf(t96,plain,
composition(meet(sk2,converse(sk1)),sFlat2) = sFlat3,
inference(rw,[status(thm)],[t47388]) ).
cnf(t47402,plain,
composition(meet(sk2,sFlat0),sFlat2) = sFlat3,
inference(step,[status(thm)],[t96,t101]) ).
cnf(t47403,plain,
composition(meet(sFlat0,sk2),sFlat2) = sFlat3,
inference(step,[status(thm)],[t47402,t296]) ).
cnf(t47404,plain,
composition(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t47403,t306]) ).
cnf(t375,plain,
composition(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t47404]) ).
cnf(t21,axiom,
sFlat4 = composition(sk2,meet(sk1,sk3)),
introduced(definition) ).
cnf(t58,plain,
composition(sk2,meet(sk1,sk3)) = sFlat4,
inference(orient,[status(thm)],[t21]) ).
cnf(t47387,plain,
composition(sk2,sFlat2) = sFlat4,
inference(step,[status(thm)],[t58,t94]) ).
cnf(t95,plain,
composition(sk2,sFlat2) = sFlat4,
inference(rw,[status(thm)],[t47387]) ).
cnf(t154,plain,
composition(sk2,sFlat2) = sFlat4,
inference(orient,[status(thm)],[t95]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t46,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t16,axiom,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t16]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t116,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t124,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t127,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t116,t124]) ).
cnf(t653,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t127]) ).
cnf(t662,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t653,t112]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t47390,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t112]) ).
cnf(t129,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t47390]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t39,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t2,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t41,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t39,t23]) ).
cnf(t405,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t41]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t406,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t405,t22]) ).
cnf(t47405,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t406,t23]) ).
cnf(t423,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t47405]) ).
cnf(t424,plain,
one = converse(one),
inference(cp,[status(thm)],[t423,t22]) ).
cnf(t435,plain,
converse(one) = one,
inference(orient,[status(thm)],[t424]) ).
cnf(t47406,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t423,t435]) ).
cnf(t445,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t47406]) ).
cnf(t447,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t445]) ).
cnf(t450,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t129,t447]) ).
cnf(t47412,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t450,t435]) ).
cnf(t47413,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t47412,t447]) ).
cnf(t480,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t47413]) ).
cnf(t490,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t63,t480]) ).
cnf(t497,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t490]) ).
cnf(t504,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t124,t497]) ).
cnf(t517,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t504]) ).
cnf(t657,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t653,t517]) ).
cnf(t659,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t653,t480]) ).
cnf(t47423,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t659,t124]) ).
cnf(t675,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t47423]) ).
cnf(t676,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t675,t63]) ).
cnf(t683,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t676]) ).
cnf(t47427,plain,
top = join(X1,top),
inference(step,[status(thm)],[t657,t683]) ).
cnf(t697,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t47427]) ).
cnf(t698,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t697,t112]) ).
cnf(t708,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t698]) ).
cnf(t47451,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t662,t708]) ).
cnf(t930,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t47451]) ).
cnf(t13,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)],[t13]) ).
cnf(t47386,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t24,t63]) ).
cnf(t66,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t47386]) ).
cnf(t4512,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t66]) ).
cnf(t4599,plain,
top = join(join(complement(X1),X2),X1),
inference(cp,[status(thm)],[t930,t4512]) ).
cnf(t47729,plain,
top = join(complement(X1),join(X2,X1)),
inference(step,[status(thm)],[t4599,t116]) ).
cnf(t5942,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t47729]) ).
cnf(t481,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t480,t63]) ).
cnf(t47459,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t481,t63]) ).
cnf(t47460,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t47459,t63]) ).
cnf(t1016,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t47460]) ).
cnf(t1019,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t1016,t296]) ).
cnf(t1097,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t1019]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t67,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t4513,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t4512,t67]) ).
cnf(t47609,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t4513,t63]) ).
cnf(t4603,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t47609]) ).
cnf(t128,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t63,t124]) ).
cnf(t47391,plain,
zero = complement(top),
inference(step,[status(thm)],[t128,t67]) ).
cnf(t148,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t47391]) ).
cnf(t484,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t480,t148]) ).
cnf(t47414,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t484,t148]) ).
cnf(t47415,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t47414,t148]) ).
cnf(t491,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t47415]) ).
cnf(t492,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t116,t491]) ).
cnf(t510,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t492]) ).
cnf(t4607,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t510,t4603]) ).
cnf(t47611,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t4607,t4603]) ).
cnf(t4620,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t47611]) ).
cnf(t47612,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t4603,t4620]) ).
cnf(t4673,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t47612]) ).
cnf(t4736,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t4673]) ).
cnf(t4737,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t1097,t4736]) ).
cnf(t47664,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t4737,t4736]) ).
cnf(t47665,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t47664,t4736]) ).
cnf(t4780,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t47665]) ).
cnf(t4782,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t116,t4780]) ).
cnf(t5024,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t4782]) ).
cnf(t5037,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t5024,t4512]) ).
cnf(t47683,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t5037,t4512]) ).
cnf(t47684,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t47683,t112]) ).
cnf(t5045,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t47684]) ).
cnf(t5049,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t5045,t296]) ).
cnf(t5096,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t5049]) ).
cnf(t5948,plain,
top = join(complement(meet(X1,X2)),X2),
inference(cp,[status(thm)],[t5942,t5096]) ).
cnf(t47830,plain,
top = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t5948,t112]) ).
cnf(t7494,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t47830]) ).
cnf(t7520,plain,
meet(X1,meet(X2,complement(X1))) = complement(top),
inference(cp,[status(thm)],[t63,t7494]) ).
cnf(t47889,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t7520,t148]) ).
cnf(t8122,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t47889]) ).
cnf(t47651,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t497,t4736]) ).
cnf(t4757,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t47651]) ).
cnf(t4799,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t4757]) ).
cnf(t8123,plain,
zero = meet(complement(X1),meet(X2,X1)),
inference(cp,[status(thm)],[t8122,t4799]) ).
cnf(t8220,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t8123]) ).
cnf(t6082,plain,
X1 = join(meet(X1,join(X2,X1)),complement(top)),
inference(cp,[status(thm)],[t4512,t5942]) ).
cnf(t47732,plain,
X1 = join(complement(top),meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t6082,t112]) ).
cnf(t47733,plain,
X1 = join(zero,meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t47732,t148]) ).
cnf(t47734,plain,
X1 = meet(X1,join(X2,X1)),
inference(step,[status(thm)],[t47733,t4620]) ).
cnf(t6102,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t47734]) ).
cnf(t8226,plain,
zero = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t8220,t6102]) ).
cnf(t47893,plain,
zero = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t8226,t296]) ).
cnf(t8513,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t47893]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t98,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t103,plain,
converse(join(sk1,X1)) = join(sFlat0,converse(X1)),
inference(cp,[status(thm)],[t98,t101]) ).
cnf(t166,plain,
converse(join(sk1,X1)) = join(sFlat0,converse(X1)),
inference(orient,[status(thm)],[t103]) ).
cnf(t102,plain,
sk1 = converse(sFlat0),
inference(cp,[status(thm)],[t23,t101]) ).
cnf(t138,plain,
converse(sFlat0) = sk1,
inference(orient,[status(thm)],[t102]) ).
cnf(t139,plain,
converse(join(sFlat0,X1)) = join(sk1,converse(X1)),
inference(cp,[status(thm)],[t98,t138]) ).
cnf(t235,plain,
converse(join(sFlat0,X1)) = join(sk1,converse(X1)),
inference(orient,[status(thm)],[t139]) ).
cnf(t106,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sFlat0),
inference(cp,[status(thm)],[t39,t101]) ).
cnf(t202,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sFlat0),
inference(orient,[status(thm)],[t106]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t53,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t203,plain,
composition(converse(top),sFlat0) = converse(sk1),
inference(cp,[status(thm)],[t202,t53]) ).
cnf(t47394,plain,
composition(converse(top),sFlat0) = sFlat0,
inference(step,[status(thm)],[t203,t101]) ).
cnf(t215,plain,
composition(converse(top),sFlat0) = sFlat0,
inference(orient,[status(thm)],[t47394]) ).
cnf(t99,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t98,t23]) ).
cnf(t526,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t99]) ).
cnf(t530,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t526,t124]) ).
cnf(t580,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t530]) ).
cnf(t711,plain,
top = converse(top),
inference(cp,[status(thm)],[t708,t580]) ).
cnf(t719,plain,
converse(top) = top,
inference(orient,[status(thm)],[t711]) ).
cnf(t47440,plain,
composition(top,sFlat0) = sFlat0,
inference(step,[status(thm)],[t215,t719]) ).
cnf(t735,plain,
composition(top,sFlat0) = sFlat0,
inference(rw,[status(thm)],[t47440]) ).
cnf(t736,plain,
composition(top,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t735]) ).
cnf(t737,plain,
composition(join(top,X1),sFlat0) = join(sFlat0,composition(X1,sFlat0)),
inference(cp,[status(thm)],[t46,t736]) ).
cnf(t47441,plain,
composition(top,sFlat0) = join(sFlat0,composition(X1,sFlat0)),
inference(step,[status(thm)],[t737,t708]) ).
cnf(t47442,plain,
sFlat0 = join(sFlat0,composition(X1,sFlat0)),
inference(step,[status(thm)],[t47441,t736]) ).
cnf(t742,plain,
join(sFlat0,composition(X1,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t47442]) ).
cnf(t746,plain,
join(sk1,converse(composition(X1,sFlat0))) = converse(sFlat0),
inference(cp,[status(thm)],[t235,t742]) ).
cnf(t141,plain,
converse(composition(X1,sFlat0)) = composition(sk1,converse(X1)),
inference(cp,[status(thm)],[t39,t138]) ).
cnf(t260,plain,
converse(composition(X1,sFlat0)) = composition(sk1,converse(X1)),
inference(orient,[status(thm)],[t141]) ).
cnf(t47449,plain,
join(sk1,composition(sk1,converse(X1))) = converse(sFlat0),
inference(step,[status(thm)],[t746,t260]) ).
cnf(t47450,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(step,[status(thm)],[t47449,t138]) ).
cnf(t897,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(orient,[status(thm)],[t47450]) ).
cnf(t914,plain,
sk1 = join(sk1,composition(sk1,X1)),
inference(cp,[status(thm)],[t897,t23]) ).
cnf(t920,plain,
join(sk1,composition(sk1,X1)) = sk1,
inference(orient,[status(thm)],[t914]) ).
cnf(t921,plain,
join(sk1,join(composition(sk1,X1),X2)) = join(sk1,X2),
inference(cp,[status(thm)],[t116,t920]) ).
cnf(t1081,plain,
join(sk1,join(composition(sk1,X1),X2)) = join(sk1,X2),
inference(orient,[status(thm)],[t921]) ).
cnf(t1086,plain,
join(sk1,X1) = join(sk1,join(X1,composition(sk1,X2))),
inference(cp,[status(thm)],[t1081,t112]) ).
cnf(t1118,plain,
join(sk1,join(X1,composition(sk1,X2))) = join(sk1,X1),
inference(orient,[status(thm)],[t1086]) ).
cnf(t1120,plain,
join(sk1,composition(X1,X2)) = join(sk1,composition(join(X1,sk1),X2)),
inference(cp,[status(thm)],[t1118,t46]) ).
cnf(t3843,plain,
join(sk1,composition(join(X1,sk1),X2)) = join(sk1,composition(X1,X2)),
inference(orient,[status(thm)],[t1120]) ).
cnf(t5098,plain,
sk1 = join(sk1,sFlat2),
inference(cp,[status(thm)],[t5096,t307]) ).
cnf(t47687,plain,
sk1 = join(sFlat2,sk1),
inference(step,[status(thm)],[t5098,t112]) ).
cnf(t5129,plain,
join(sFlat2,sk1) = sk1,
inference(orient,[status(thm)],[t47687]) ).
cnf(t5135,plain,
join(sk1,composition(sFlat2,X1)) = join(sk1,composition(sk1,X1)),
inference(cp,[status(thm)],[t3843,t5129]) ).
cnf(t47694,plain,
join(sk1,composition(sFlat2,X1)) = sk1,
inference(step,[status(thm)],[t5135,t920]) ).
cnf(t5167,plain,
join(sk1,composition(sFlat2,X1)) = sk1,
inference(orient,[status(thm)],[t47694]) ).
cnf(t5170,plain,
join(sFlat0,converse(composition(sFlat2,X1))) = converse(sk1),
inference(cp,[status(thm)],[t166,t5167]) ).
cnf(t47817,plain,
join(sFlat0,converse(composition(sFlat2,X1))) = sFlat0,
inference(step,[status(thm)],[t5170,t101]) ).
cnf(t7268,plain,
join(sFlat0,converse(composition(sFlat2,X1))) = sFlat0,
inference(orient,[status(thm)],[t47817]) ).
cnf(t40,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t39,t23]) ).
cnf(t386,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t40]) ).
cnf(t7272,plain,
sFlat0 = join(sFlat0,composition(X1,converse(sFlat2))),
inference(cp,[status(thm)],[t7268,t386]) ).
cnf(t7973,plain,
join(sFlat0,composition(X1,converse(sFlat2))) = sFlat0,
inference(orient,[status(thm)],[t7272]) ).
cnf(t8591,plain,
zero = meet(composition(X1,converse(sFlat2)),complement(sFlat0)),
inference(cp,[status(thm)],[t8513,t7973]) ).
cnf(t48186,plain,
zero = meet(complement(sFlat0),composition(X1,converse(sFlat2))),
inference(step,[status(thm)],[t8591,t296]) ).
cnf(t12845,plain,
meet(complement(sFlat0),composition(X1,converse(sFlat2))) = zero,
inference(orient,[status(thm)],[t48186]) ).
cnf(t12850,plain,
composition(meet(complement(sFlat0),composition(X1,converse(sFlat2))),meet(sFlat2,composition(converse(complement(sFlat0)),X1))) = join(meet(composition(complement(sFlat0),sFlat2),X1),composition(zero,meet(sFlat2,composition(converse(complement(sFlat0)),X1)))),
inference(cp,[status(thm)],[t29,t12845]) ).
cnf(t48187,plain,
composition(zero,meet(sFlat2,composition(converse(complement(sFlat0)),X1))) = join(meet(composition(complement(sFlat0),sFlat2),X1),composition(zero,meet(sFlat2,composition(converse(complement(sFlat0)),X1)))),
inference(step,[status(thm)],[t12850,t12845]) ).
cnf(t9,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t739,plain,
composition(top,composition(sFlat0,X1)) = composition(sFlat0,X1),
inference(cp,[status(thm)],[t27,t736]) ).
cnf(t790,plain,
composition(top,composition(sFlat0,X1)) = composition(sFlat0,X1),
inference(orient,[status(thm)],[t739]) ).
cnf(t134,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t129,t53]) ).
cnf(t47455,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t134,t148]) ).
cnf(t47456,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t47455,t148]) ).
cnf(t47457,plain,
zero = join(zero,composition(sFlat0,complement(sk1))),
inference(step,[status(thm)],[t47456,t101]) ).
cnf(t1012,plain,
join(zero,composition(sFlat0,complement(sk1))) = zero,
inference(orient,[status(thm)],[t47457]) ).
cnf(t47639,plain,
composition(sFlat0,complement(sk1)) = zero,
inference(step,[status(thm)],[t1012,t4620]) ).
cnf(t4696,plain,
composition(sFlat0,complement(sk1)) = zero,
inference(rw,[status(thm)],[t47639]) ).
cnf(t4897,plain,
composition(sFlat0,complement(sk1)) = zero,
inference(orient,[status(thm)],[t4696]) ).
cnf(t4899,plain,
composition(sFlat0,complement(sk1)) = composition(top,zero),
inference(cp,[status(thm)],[t790,t4897]) ).
cnf(t47670,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t4899,t4897]) ).
cnf(t4909,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t47670]) ).
cnf(t4911,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t46,t4909]) ).
cnf(t47673,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t4911,t708]) ).
cnf(t47674,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t47673,t4909]) ).
cnf(t47675,plain,
zero = composition(X1,zero),
inference(step,[status(thm)],[t47674,t4620]) ).
cnf(t4925,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t47675]) ).
cnf(t4929,plain,
composition(converse(zero),X1) = converse(zero),
inference(cp,[status(thm)],[t405,t4925]) ).
cnf(t47438,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t580,t719]) ).
cnf(t726,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t47438]) ).
cnf(t4629,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t4620,t726]) ).
cnf(t4837,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t4629]) ).
cnf(t4838,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t23,t4837]) ).
cnf(t47668,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t4838,t719]) ).
cnf(t4868,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t47668]) ).
cnf(t4869,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t4799,t4868]) ).
cnf(t47669,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t4869,t148]) ).
cnf(t4876,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t47669]) ).
cnf(t47680,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t4929,t4876]) ).
cnf(t47681,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t47680,t4876]) ).
cnf(t5009,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t47681]) ).
cnf(t48188,plain,
zero = join(meet(composition(complement(sFlat0),sFlat2),X1),composition(zero,meet(sFlat2,composition(converse(complement(sFlat0)),X1)))),
inference(step,[status(thm)],[t48187,t5009]) ).
cnf(t48189,plain,
zero = join(meet(composition(complement(sFlat0),sFlat2),X1),zero),
inference(step,[status(thm)],[t48188,t5009]) ).
cnf(t4632,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t4620,t112]) ).
cnf(t4714,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t4632]) ).
cnf(t48190,plain,
zero = meet(composition(complement(sFlat0),sFlat2),X1),
inference(step,[status(thm)],[t48189,t4714]) ).
cnf(t12855,plain,
meet(composition(complement(sFlat0),sFlat2),X1) = zero,
inference(orient,[status(thm)],[t48190]) ).
cnf(t12856,plain,
zero = composition(complement(sFlat0),sFlat2),
inference(cp,[status(thm)],[t12855,t4736]) ).
cnf(t12977,plain,
composition(complement(sFlat0),sFlat2) = zero,
inference(orient,[status(thm)],[t12856]) ).
cnf(t12978,plain,
composition(join(complement(sFlat0),X1),sFlat2) = join(zero,composition(X1,sFlat2)),
inference(cp,[status(thm)],[t46,t12977]) ).
cnf(t48193,plain,
composition(join(complement(sFlat0),X1),sFlat2) = composition(X1,sFlat2),
inference(step,[status(thm)],[t12978,t4620]) ).
cnf(t13018,plain,
composition(join(complement(sFlat0),X1),sFlat2) = composition(X1,sFlat2),
inference(orient,[status(thm)],[t48193]) ).
cnf(t5110,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t116,t5096]) ).
cnf(t24909,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t5110]) ).
cnf(t507,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t63,t497]) ).
cnf(t2756,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t507]) ).
cnf(t47654,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t2756,t4736]) ).
cnf(t4760,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t47654]) ).
cnf(t8855,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t4760]) ).
cnf(t47942,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t4512,t8855]) ).
cnf(t8912,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t47942]) ).
cnf(t44690,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t8912]) ).
cnf(t44905,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t24909,t44690]) ).
cnf(t47106,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t44905]) ).
cnf(t47225,plain,
composition(meet(X1,complement(complement(sFlat0))),sFlat2) = composition(join(complement(sFlat0),X1),sFlat2),
inference(cp,[status(thm)],[t13018,t47106]) ).
cnf(t49093,plain,
composition(meet(X1,sFlat0),sFlat2) = composition(join(complement(sFlat0),X1),sFlat2),
inference(step,[status(thm)],[t47225,t4799]) ).
cnf(t49094,plain,
composition(meet(X1,sFlat0),sFlat2) = composition(X1,sFlat2),
inference(step,[status(thm)],[t49093,t13018]) ).
cnf(t47255,plain,
composition(meet(X1,sFlat0),sFlat2) = composition(X1,sFlat2),
inference(orient,[status(thm)],[t49094]) ).
cnf(t47256,plain,
composition(X1,sFlat2) = composition(meet(sFlat0,X1),sFlat2),
inference(cp,[status(thm)],[t47255,t296]) ).
cnf(t47330,plain,
composition(meet(sFlat0,X1),sFlat2) = composition(X1,sFlat2),
inference(orient,[status(thm)],[t47256]) ).
cnf(t47332,plain,
composition(sk2,sFlat2) = composition(sFlat1,sFlat2),
inference(cp,[status(thm)],[t47330,t306]) ).
cnf(t49097,plain,
sFlat4 = composition(sFlat1,sFlat2),
inference(step,[status(thm)],[t47332,t154]) ).
cnf(t49098,plain,
sFlat4 = sFlat3,
inference(step,[status(thm)],[t49097,t375]) ).
cnf(t47369,plain,
sFlat4 = sFlat3,
inference(orient,[status(thm)],[t49098]) ).
cnf(t49099,plain,
composition(sk2,sFlat2) = sFlat3,
inference(step,[status(thm)],[t154,t47369]) ).
cnf(t47370,plain,
composition(sk2,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t49099]) ).
cnf(goal_0,negated_conjecture,
composition(meet(sk2,converse(sk1)),meet(sk1,sk3)) != composition(sk2,meet(sk1,sk3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
composition(meet(sk2,sFlat0),meet(sk1,sk3)) != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[goal_0,t101]) ).
cnf(g0_1,plain,
composition(meet(sFlat0,sk2),meet(sk1,sk3)) != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_0,t296]) ).
cnf(g0_2,plain,
composition(sFlat1,meet(sk1,sk3)) != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_1,t306]) ).
cnf(g0_3,plain,
composition(sFlat1,meet(sk3,sk1)) != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_2,t296]) ).
cnf(g0_4,plain,
composition(sFlat1,sFlat2) != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_3,t307]) ).
cnf(g0_5,plain,
sFlat3 != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_4,t375]) ).
cnf(g0_6,plain,
sFlat3 != composition(sk2,meet(sk3,sk1)),
inference(rw,[status(thm)],[g0_5,t296]) ).
cnf(g0_7,plain,
sFlat3 != composition(sk2,sFlat2),
inference(rw,[status(thm)],[g0_6,t307]) ).
cnf(g0_8,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_7,t47370]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL035-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 07:33:08 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 65.49/8.93 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 65.49/8.93 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------