%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL021-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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:48 PM UTC 2026
% Result : Unsatisfiable 33.22s 4.68s
% Output : CNFRefutation 33.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 83
% Number of leaves : 18
% Syntax : Number of clauses : 280 ( 280 unt; 0 nHn; 106 RR)
% Number of literals : 280 ( 279 equ; 10 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 : 14 ( 14 usr; 9 con; 0-2 aty)
% Number of variables : 274 ( 54 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t6,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t68,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t70,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t68,t23]) ).
cnf(t25667,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t70,t68]) ).
cnf(t96,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t25667]) ).
cnf(t16,axiom,
sFlat2 = meet(sk1,sk2),
introduced(definition) ).
cnf(t77,plain,
meet(sk1,sk2) = sFlat2,
inference(orient,[status(thm)],[t16]) ).
cnf(t98,plain,
meet(sk1,sk2) = sFlat2,
inference(rw,[status(thm)],[t77]) ).
cnf(t25669,plain,
meet(sk2,sk1) = sFlat2,
inference(step,[status(thm)],[t98,t96]) ).
cnf(t100,plain,
meet(sk2,sk1) = sFlat2,
inference(orient,[status(thm)],[t25669]) ).
cnf(t14,axiom,
sFlat0 = meet(sk1,one),
introduced(definition) ).
cnf(t78,plain,
meet(sk1,one) = sFlat0,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sFlat1 = composition(meet(sk1,one),sk2),
introduced(definition) ).
cnf(t62,plain,
composition(meet(sk1,one),sk2) = sFlat1,
inference(orient,[status(thm)],[t15]) ).
cnf(t25662,plain,
composition(sFlat0,sk2) = sFlat1,
inference(step,[status(thm)],[t62,t78]) ).
cnf(t79,plain,
composition(sFlat0,sk2) = sFlat1,
inference(rw,[status(thm)],[t25662]) ).
cnf(t80,plain,
composition(sFlat0,sk2) = sFlat1,
inference(orient,[status(thm)],[t79]) ).
cnf(t17,axiom,
sFlat3 = join(composition(meet(sk1,one),sk2),meet(sk1,sk2)),
introduced(definition) ).
cnf(t25660,plain,
sFlat3 = join(meet(sk1,sk2),composition(meet(sk1,one),sk2)),
inference(step,[status(thm)],[t17,t23]) ).
cnf(t38,plain,
join(meet(sk1,sk2),composition(meet(sk1,one),sk2)) = sFlat3,
inference(orient,[status(thm)],[t25660]) ).
cnf(t25661,plain,
join(meet(sk1,sk2),sFlat1) = sFlat3,
inference(step,[status(thm)],[t38,t62]) ).
cnf(t67,plain,
join(meet(sk1,sk2),sFlat1) = sFlat3,
inference(rw,[status(thm)],[t25661]) ).
cnf(t25665,plain,
join(sFlat1,meet(sk1,sk2)) = sFlat3,
inference(step,[status(thm)],[t67,t23]) ).
cnf(t25666,plain,
join(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t25665,t77]) ).
cnf(t94,plain,
join(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t25666]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t24,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t18]) ).
cnf(t25678,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t24,t23]) ).
cnf(t25679,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t25678,t68]) ).
cnf(t25680,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t25679,t23]) ).
cnf(t264,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t25680]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25659,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t23]) ).
cnf(t34,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t25659]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t50,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(t22,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t52,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t50,t22]) ).
cnf(t174,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t52]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t175,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t174,t21]) ).
cnf(t25670,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t175,t22]) ).
cnf(t189,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t25670]) ).
cnf(t190,plain,
one = converse(one),
inference(cp,[status(thm)],[t189,t21]) ).
cnf(t196,plain,
converse(one) = one,
inference(orient,[status(thm)],[t190]) ).
cnf(t25671,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t189,t196]) ).
cnf(t206,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t25671]) ).
cnf(t207,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t206]) ).
cnf(t210,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t34,t207]) ).
cnf(t25673,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t210,t196]) ).
cnf(t25674,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t25673,t207]) ).
cnf(t234,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t25674]) ).
cnf(t244,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t68,t234]) ).
cnf(t251,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t244]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t75,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t265,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t264,t75]) ).
cnf(t25681,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t265,t68]) ).
cnf(t282,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t25681]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,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(t28,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t69,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t68,t28]) ).
cnf(t25663,plain,
zero = complement(top),
inference(step,[status(thm)],[t69,t75]) ).
cnf(t85,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t25663]) ).
cnf(t238,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t234,t85]) ).
cnf(t25675,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t238,t85]) ).
cnf(t25676,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t25675,t85]) ).
cnf(t245,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t25676]) ).
cnf(t246,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t25,t245]) ).
cnf(t261,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t246]) ).
cnf(t284,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t261,t282]) ).
cnf(t25682,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t284,t282]) ).
cnf(t286,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t25682]) ).
cnf(t25683,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t282,t286]) ).
cnf(t292,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t25683]) ).
cnf(t309,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t292]) ).
cnf(t25688,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t251,t309]) ).
cnf(t311,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t25688]) ).
cnf(t314,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t311]) ).
cnf(t315,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t314,t68]) ).
cnf(t1264,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t315]) ).
cnf(t1267,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t1264,t314]) ).
cnf(t1437,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t1267]) ).
cnf(t1443,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t314,t1437]) ).
cnf(t1901,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t1443]) ).
cnf(t25796,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t264,t1901]) ).
cnf(t1929,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t25796]) ).
cnf(t24802,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t1929]) ).
cnf(t1266,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t1264,t314]) ).
cnf(t1421,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t1266]) ).
cnf(t1428,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t314,t1421]) ).
cnf(t1453,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t1428]) ).
cnf(t26,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t25,t23]) ).
cnf(t582,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t26]) ).
cnf(t596,plain,
join(complement(X1),join(X2,X1)) = join(X2,top),
inference(cp,[status(thm)],[t582,t28]) ).
cnf(t25725,plain,
join(X1,join(complement(X1),X2)) = join(X2,top),
inference(step,[status(thm)],[t596,t582]) ).
cnf(t316,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t234,t314]) ).
cnf(t25691,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t316,t314]) ).
cnf(t25692,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t25691,t314]) ).
cnf(t324,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t25692]) ).
cnf(t328,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t25,t324]) ).
cnf(t418,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t328]) ).
cnf(t421,plain,
join(X1,complement(X1)) = join(X1,top),
inference(cp,[status(thm)],[t418,t28]) ).
cnf(t25703,plain,
top = join(X1,top),
inference(step,[status(thm)],[t421,t28]) ).
cnf(t432,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t25703]) ).
cnf(t25726,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t25725,t432]) ).
cnf(t800,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t25726]) ).
cnf(t808,plain,
top = join(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t800,t23]) ).
cnf(t1068,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t808]) ).
cnf(t1283,plain,
top = join(X1,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t1068,t1264]) ).
cnf(t1364,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t1283]) ).
cnf(t1455,plain,
meet(complement(X1),meet(X2,X1)) = complement(top),
inference(cp,[status(thm)],[t1453,t1364]) ).
cnf(t25766,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(step,[status(thm)],[t1455,t85]) ).
cnf(t1509,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t25766]) ).
cnf(t817,plain,
X1 = join(meet(X1,join(complement(complement(X1)),X2)),complement(top)),
inference(cp,[status(thm)],[t264,t800]) ).
cnf(t25727,plain,
X1 = join(complement(top),meet(X1,join(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t817,t23]) ).
cnf(t25728,plain,
X1 = join(zero,meet(X1,join(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t25727,t85]) ).
cnf(t25729,plain,
X1 = meet(X1,join(complement(complement(X1)),X2)),
inference(step,[status(thm)],[t25728,t286]) ).
cnf(t25730,plain,
X1 = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t25729,t314]) ).
cnf(t845,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t25730]) ).
cnf(t873,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t845,t23]) ).
cnf(t949,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t873]) ).
cnf(t1519,plain,
zero = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t1509,t949]) ).
cnf(t25781,plain,
zero = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t1519,t96]) ).
cnf(t1764,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t25781]) ).
cnf(t428,plain,
join(X1,X2) = join(X1,join(X2,X1)),
inference(cp,[status(thm)],[t418,t23]) ).
cnf(t549,plain,
join(X1,join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t428]) ).
cnf(t1767,plain,
zero = meet(join(X1,X2),complement(join(X2,X1))),
inference(cp,[status(thm)],[t1764,t549]) ).
cnf(t23801,plain,
meet(join(X1,X2),complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t1767]) ).
cnf(t95,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t25,t94]) ).
cnf(t130,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t95]) ).
cnf(t422,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t418,t264]) ).
cnf(t25713,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t422,t264]) ).
cnf(t25714,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t25713,t23]) ).
cnf(t466,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t25714]) ).
cnf(t468,plain,
sk2 = join(sk2,sFlat2),
inference(cp,[status(thm)],[t466,t100]) ).
cnf(t25715,plain,
sk2 = join(sFlat2,sk2),
inference(step,[status(thm)],[t468,t23]) ).
cnf(t476,plain,
join(sFlat2,sk2) = sk2,
inference(orient,[status(thm)],[t25715]) ).
cnf(t477,plain,
join(sFlat3,sk2) = join(sFlat1,sk2),
inference(cp,[status(thm)],[t130,t476]) ).
cnf(t481,plain,
join(sFlat3,sk2) = join(sFlat1,sk2),
inference(orient,[status(thm)],[t477]) ).
cnf(t483,plain,
join(sFlat3,join(sk2,X1)) = join(join(sFlat1,sk2),X1),
inference(cp,[status(thm)],[t25,t481]) ).
cnf(t25839,plain,
join(sFlat3,join(sk2,X1)) = join(sFlat1,join(sk2,X1)),
inference(step,[status(thm)],[t483,t25]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t82,plain,
composition(join(sFlat0,X1),sk2) = join(sFlat1,composition(X1,sk2)),
inference(cp,[status(thm)],[t31,t80]) ).
cnf(t2208,plain,
composition(join(sFlat0,X1),sk2) = join(sFlat1,composition(X1,sk2)),
inference(orient,[status(thm)],[t82]) ).
cnf(t470,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t466,t96]) ).
cnf(t484,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t470]) ).
cnf(t487,plain,
one = join(one,sFlat0),
inference(cp,[status(thm)],[t484,t78]) ).
cnf(t25718,plain,
one = join(sFlat0,one),
inference(step,[status(thm)],[t487,t23]) ).
cnf(t496,plain,
join(sFlat0,one) = one,
inference(orient,[status(thm)],[t25718]) ).
cnf(t2215,plain,
join(sFlat1,composition(one,sk2)) = composition(one,sk2),
inference(cp,[status(thm)],[t2208,t496]) ).
cnf(t25817,plain,
join(sFlat1,sk2) = composition(one,sk2),
inference(step,[status(thm)],[t2215,t207]) ).
cnf(t25818,plain,
join(sFlat1,sk2) = sk2,
inference(step,[status(thm)],[t25817,t207]) ).
cnf(t2236,plain,
join(sFlat1,sk2) = sk2,
inference(orient,[status(thm)],[t25818]) ).
cnf(t2242,plain,
join(sFlat1,join(sk2,X1)) = join(sk2,X1),
inference(cp,[status(thm)],[t25,t2236]) ).
cnf(t2317,plain,
join(sFlat1,join(sk2,X1)) = join(sk2,X1),
inference(orient,[status(thm)],[t2242]) ).
cnf(t25840,plain,
join(sFlat3,join(sk2,X1)) = join(sk2,X1),
inference(step,[status(thm)],[t25839,t2317]) ).
cnf(t2565,plain,
join(sFlat3,join(sk2,X1)) = join(sk2,X1),
inference(orient,[status(thm)],[t25840]) ).
cnf(t2572,plain,
sFlat3 = meet(sFlat3,join(sk2,X1)),
inference(cp,[status(thm)],[t845,t2565]) ).
cnf(t2578,plain,
meet(sFlat3,join(sk2,X1)) = sFlat3,
inference(orient,[status(thm)],[t2572]) ).
cnf(t27,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t25,t23]) ).
cnf(t25740,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t27,t25]) ).
cnf(t1088,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t25740]) ).
cnf(t1104,plain,
join(X1,join(X2,meet(X3,X1))) = join(X2,X1),
inference(cp,[status(thm)],[t1088,t484]) ).
cnf(t9333,plain,
join(X1,join(X2,meet(X3,X1))) = join(X2,X1),
inference(orient,[status(thm)],[t1104]) ).
cnf(t24896,plain,
sk2 = join(sFlat2,meet(sk2,complement(sk1))),
inference(cp,[status(thm)],[t24802,t100]) ).
cnf(t25007,plain,
join(sFlat2,meet(sk2,complement(sk1))) = sk2,
inference(orient,[status(thm)],[t24896]) ).
cnf(t25026,plain,
join(sFlat2,complement(sk1)) = join(complement(sk1),sk2),
inference(cp,[status(thm)],[t9333,t25007]) ).
cnf(t26193,plain,
join(sFlat2,complement(sk1)) = join(sk2,complement(sk1)),
inference(step,[status(thm)],[t25026,t23]) ).
cnf(t25037,plain,
join(sk2,complement(sk1)) = join(sFlat2,complement(sk1)),
inference(orient,[status(thm)],[t26193]) ).
cnf(t25052,plain,
sFlat3 = meet(sFlat3,join(sFlat2,complement(sk1))),
inference(cp,[status(thm)],[t2578,t25037]) ).
cnf(t25301,plain,
meet(sFlat3,join(sFlat2,complement(sk1))) = sFlat3,
inference(orient,[status(thm)],[t25052]) ).
cnf(t25330,plain,
top = join(join(sFlat2,complement(sk1)),complement(sFlat3)),
inference(cp,[status(thm)],[t1364,t25301]) ).
cnf(t26221,plain,
top = join(sFlat2,join(complement(sk1),complement(sFlat3))),
inference(step,[status(thm)],[t25330,t25]) ).
cnf(t26222,plain,
top = join(sFlat2,complement(meet(sk1,sFlat3))),
inference(step,[status(thm)],[t26221,t1264]) ).
cnf(t26223,plain,
top = join(sFlat2,complement(meet(sFlat3,sk1))),
inference(step,[status(thm)],[t26222,t96]) ).
cnf(t486,plain,
sk1 = join(sk1,sFlat2),
inference(cp,[status(thm)],[t484,t100]) ).
cnf(t25717,plain,
sk1 = join(sFlat2,sk1),
inference(step,[status(thm)],[t486,t23]) ).
cnf(t493,plain,
join(sFlat2,sk1) = sk1,
inference(orient,[status(thm)],[t25717]) ).
cnf(t494,plain,
join(sFlat3,sk1) = join(sFlat1,sk1),
inference(cp,[status(thm)],[t130,t493]) ).
cnf(t499,plain,
join(sFlat3,sk1) = join(sFlat1,sk1),
inference(orient,[status(thm)],[t494]) ).
cnf(t501,plain,
join(sFlat3,join(sk1,X1)) = join(join(sFlat1,sk1),X1),
inference(cp,[status(thm)],[t25,t499]) ).
cnf(t25842,plain,
join(sFlat3,join(sk1,X1)) = join(sFlat1,join(sk1,X1)),
inference(step,[status(thm)],[t501,t25]) ).
cnf(t2629,plain,
join(sFlat3,join(sk1,X1)) = join(sFlat1,join(sk1,X1)),
inference(orient,[status(thm)],[t25842]) ).
cnf(t2638,plain,
sFlat3 = meet(sFlat3,join(sFlat1,join(sk1,X1))),
inference(cp,[status(thm)],[t845,t2629]) ).
cnf(t3722,plain,
meet(sFlat3,join(sFlat1,join(sk1,X1))) = sFlat3,
inference(orient,[status(thm)],[t2638]) ).
cnf(t3724,plain,
sFlat3 = meet(sFlat3,join(sFlat1,join(X1,sk1))),
inference(cp,[status(thm)],[t3722,t23]) ).
cnf(t3971,plain,
meet(sFlat3,join(sFlat1,join(X1,sk1))) = sFlat3,
inference(orient,[status(thm)],[t3724]) ).
cnf(t875,plain,
X1 = meet(X1,join(X2,join(X1,X3))),
inference(cp,[status(thm)],[t845,t582]) ).
cnf(t3032,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t875]) ).
cnf(t469,plain,
sk1 = join(sk1,sFlat0),
inference(cp,[status(thm)],[t466,t78]) ).
cnf(t25716,plain,
sk1 = join(sFlat0,sk1),
inference(step,[status(thm)],[t469,t23]) ).
cnf(t479,plain,
join(sFlat0,sk1) = sk1,
inference(orient,[status(thm)],[t25716]) ).
cnf(t2214,plain,
join(sFlat1,composition(sk1,sk2)) = composition(sk1,sk2),
inference(cp,[status(thm)],[t2208,t479]) ).
cnf(t2287,plain,
join(sFlat1,composition(sk1,sk2)) = composition(sk1,sk2),
inference(orient,[status(thm)],[t2214]) ).
cnf(t3062,plain,
sFlat1 = meet(sFlat1,join(X1,composition(sk1,sk2))),
inference(cp,[status(thm)],[t3032,t2287]) ).
cnf(t3881,plain,
meet(sFlat1,join(X1,composition(sk1,sk2))) = sFlat1,
inference(orient,[status(thm)],[t3062]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t42,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t40,t22]) ).
cnf(t143,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t42]) ).
cnf(t438,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t143,t432]) ).
cnf(t453,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t438]) ).
cnf(t435,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t432,t23]) ).
cnf(t440,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t435]) ).
cnf(t454,plain,
converse(top) = top,
inference(cp,[status(thm)],[t453,t440]) ).
cnf(t458,plain,
converse(top) = top,
inference(orient,[status(thm)],[t454]) ).
cnf(t461,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t50,t458]) ).
cnf(t515,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t461]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t57,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t516,plain,
composition(top,converse(sk1)) = converse(sk1),
inference(cp,[status(thm)],[t515,t57]) ).
cnf(t527,plain,
composition(top,converse(sk1)) = converse(sk1),
inference(orient,[status(thm)],[t516]) ).
cnf(t529,plain,
composition(join(top,X1),converse(sk1)) = join(converse(sk1),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t31,t527]) ).
cnf(t25952,plain,
composition(top,converse(sk1)) = join(converse(sk1),composition(X1,converse(sk1))),
inference(step,[status(thm)],[t529,t440]) ).
cnf(t25953,plain,
converse(sk1) = join(converse(sk1),composition(X1,converse(sk1))),
inference(step,[status(thm)],[t25952,t527]) ).
cnf(t4267,plain,
join(converse(sk1),composition(X1,converse(sk1))) = converse(sk1),
inference(orient,[status(thm)],[t25953]) ).
cnf(t4275,plain,
join(sk1,converse(composition(X1,converse(sk1)))) = converse(converse(sk1)),
inference(cp,[status(thm)],[t143,t4267]) ).
cnf(t51,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t50,t22]) ).
cnf(t162,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t51]) ).
cnf(t25954,plain,
join(sk1,composition(sk1,converse(X1))) = converse(converse(sk1)),
inference(step,[status(thm)],[t4275,t162]) ).
cnf(t25955,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(step,[status(thm)],[t25954,t22]) ).
cnf(t4279,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(orient,[status(thm)],[t25955]) ).
cnf(t4283,plain,
sk1 = join(sk1,composition(sk1,X1)),
inference(cp,[status(thm)],[t4279,t22]) ).
cnf(t4294,plain,
join(sk1,composition(sk1,X1)) = sk1,
inference(orient,[status(thm)],[t4283]) ).
cnf(t4297,plain,
sFlat1 = meet(sFlat1,sk1),
inference(cp,[status(thm)],[t3881,t4294]) ).
cnf(t4303,plain,
meet(sFlat1,sk1) = sFlat1,
inference(orient,[status(thm)],[t4297]) ).
cnf(t4309,plain,
sk1 = join(sk1,sFlat1),
inference(cp,[status(thm)],[t484,t4303]) ).
cnf(t25956,plain,
sk1 = join(sFlat1,sk1),
inference(step,[status(thm)],[t4309,t23]) ).
cnf(t4312,plain,
join(sFlat1,sk1) = sk1,
inference(orient,[status(thm)],[t25956]) ).
cnf(t4320,plain,
sFlat3 = meet(sFlat3,join(sFlat1,sk1)),
inference(cp,[status(thm)],[t3971,t4312]) ).
cnf(t25962,plain,
sFlat3 = meet(sFlat3,sk1),
inference(step,[status(thm)],[t4320,t4312]) ).
cnf(t4329,plain,
meet(sFlat3,sk1) = sFlat3,
inference(orient,[status(thm)],[t25962]) ).
cnf(t26224,plain,
top = join(sFlat2,complement(sFlat3)),
inference(step,[status(thm)],[t26223,t4329]) ).
cnf(t25571,plain,
join(sFlat2,complement(sFlat3)) = top,
inference(orient,[status(thm)],[t26224]) ).
cnf(t25578,plain,
zero = meet(top,complement(join(complement(sFlat3),sFlat2))),
inference(cp,[status(thm)],[t23801,t25571]) ).
cnf(t88,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t68,t85]) ).
cnf(t111,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t88]) ).
cnf(t25685,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t111,t286]) ).
cnf(t294,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t25685]) ).
cnf(t25696,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t294,t314]) ).
cnf(t334,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t25696]) ).
cnf(t26225,plain,
zero = complement(join(complement(sFlat3),sFlat2)),
inference(step,[status(thm)],[t25578,t334]) ).
cnf(t26226,plain,
zero = meet(sFlat3,complement(sFlat2)),
inference(step,[status(thm)],[t26225,t1901]) ).
cnf(t25584,plain,
meet(sFlat3,complement(sFlat2)) = zero,
inference(orient,[status(thm)],[t26226]) ).
cnf(t25585,plain,
sFlat3 = join(zero,meet(sFlat3,complement(complement(sFlat2)))),
inference(cp,[status(thm)],[t24802,t25584]) ).
cnf(t26227,plain,
sFlat3 = meet(sFlat3,complement(complement(sFlat2))),
inference(step,[status(thm)],[t25585,t286]) ).
cnf(t26228,plain,
sFlat3 = meet(sFlat3,sFlat2),
inference(step,[status(thm)],[t26227,t314]) ).
cnf(t26229,plain,
sFlat3 = meet(sFlat2,sFlat3),
inference(step,[status(thm)],[t26228,t96]) ).
cnf(t132,plain,
join(sFlat3,X1) = join(sFlat1,join(X1,sFlat2)),
inference(cp,[status(thm)],[t130,t23]) ).
cnf(t139,plain,
join(sFlat1,join(X1,sFlat2)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t132]) ).
cnf(t326,plain,
join(sFlat3,sFlat2) = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t139,t324]) ).
cnf(t25693,plain,
join(sFlat2,sFlat3) = join(sFlat1,sFlat2),
inference(step,[status(thm)],[t326,t23]) ).
cnf(t25694,plain,
join(sFlat2,sFlat3) = sFlat3,
inference(step,[status(thm)],[t25693,t94]) ).
cnf(t329,plain,
join(sFlat2,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t25694]) ).
cnf(t859,plain,
sFlat2 = meet(sFlat2,sFlat3),
inference(cp,[status(thm)],[t845,t329]) ).
cnf(t888,plain,
meet(sFlat2,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t859]) ).
cnf(t26230,plain,
sFlat3 = sFlat2,
inference(step,[status(thm)],[t26229,t888]) ).
cnf(t25592,plain,
sFlat3 = sFlat2,
inference(orient,[status(thm)],[t26230]) ).
cnf(t26231,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t94,t25592]) ).
cnf(t25593,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t26231]) ).
cnf(goal_0,negated_conjecture,
join(composition(meet(sk1,one),sk2),meet(sk1,sk2)) != meet(sk1,sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(meet(sk1,sk2),composition(meet(sk1,one),sk2)) != meet(sk1,sk2),
inference(rw,[status(thm)],[goal_0,t23]) ).
cnf(g0_1,plain,
join(meet(sk2,sk1),composition(meet(sk1,one),sk2)) != meet(sk1,sk2),
inference(rw,[status(thm)],[g0_0,t96]) ).
cnf(g0_2,plain,
join(sFlat2,composition(meet(sk1,one),sk2)) != meet(sk1,sk2),
inference(rw,[status(thm)],[g0_1,t100]) ).
cnf(g0_3,plain,
join(sFlat2,composition(sFlat0,sk2)) != meet(sk1,sk2),
inference(rw,[status(thm)],[g0_2,t78]) ).
cnf(g0_4,plain,
join(sFlat2,sFlat1) != meet(sk1,sk2),
inference(rw,[status(thm)],[g0_3,t80]) ).
cnf(g0_5,plain,
join(sFlat1,sFlat2) != meet(sk1,sk2),
inference(rw,[status(thm)],[g0_4,t23]) ).
cnf(g0_6,plain,
sFlat2 != meet(sk1,sk2),
inference(rw,[status(thm)],[g0_5,t25593]) ).
cnf(g0_7,plain,
sFlat2 != meet(sk2,sk1),
inference(rw,[status(thm)],[g0_6,t96]) ).
cnf(g0_8,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_7,t100]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL021-1 : 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.36 % Computer : n014.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 07:16:48 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 33.22/4.68 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 33.22/4.68 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------