%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL044-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:36:11 PM UTC 2026
% Result : Unsatisfiable 44.51s 6.91s
% Output : CNFRefutation 44.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 19
% Syntax : Number of clauses : 272 ( 272 unt; 0 nHn; 91 RR)
% Number of literals : 272 ( 271 equ; 8 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 : 301 ( 48 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t52,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t112,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t49653,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t52]) ).
cnf(t63,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t49653]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t32,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t30,t24]) ).
cnf(t350,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t32]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t351,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t350,t20]) ).
cnf(t49667,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t351,t24]) ).
cnf(t385,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t49667]) ).
cnf(t386,plain,
one = converse(one),
inference(cp,[status(thm)],[t385,t20]) ).
cnf(t397,plain,
converse(one) = one,
inference(orient,[status(thm)],[t386]) ).
cnf(t49668,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t385,t397]) ).
cnf(t407,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t49668]) ).
cnf(t408,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t407]) ).
cnf(t412,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t63,t408]) ).
cnf(t49670,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t412,t397]) ).
cnf(t49671,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t49670,t408]) ).
cnf(t442,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t49671]) ).
cnf(t452,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t112,t442]) ).
cnf(t459,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t452]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t54,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t21]) ).
cnf(t50239,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t54,t52]) ).
cnf(t50240,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t50239,t112]) ).
cnf(t50241,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t50240,t52]) ).
cnf(t12181,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t50241]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t119,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t12182,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t12181,t119]) ).
cnf(t50242,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t12182,t112]) ).
cnf(t12379,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t50242]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t55,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t60,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t113,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t112,t60]) ).
cnf(t49659,plain,
zero = complement(top),
inference(step,[status(thm)],[t113,t119]) ).
cnf(t142,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t49659]) ).
cnf(t446,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t442,t142]) ).
cnf(t49672,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t446,t142]) ).
cnf(t49673,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t49672,t142]) ).
cnf(t453,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t49673]) ).
cnf(t454,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t55,t453]) ).
cnf(t472,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t454]) ).
cnf(t12387,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t472,t12379]) ).
cnf(t50244,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t12387,t12379]) ).
cnf(t12404,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t50244]) ).
cnf(t50245,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t12379,t12404]) ).
cnf(t12490,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t50245]) ).
cnf(t12593,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t12490]) ).
cnf(t50280,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t459,t12593]) ).
cnf(t12621,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t50280]) ).
cnf(t12746,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t12621]) ).
cnf(t443,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t442,t112]) ).
cnf(t49709,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t443,t112]) ).
cnf(t49710,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t49709,t112]) ).
cnf(t821,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t49710]) ).
cnf(t114,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t112,t52]) ).
cnf(t49665,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t114,t112]) ).
cnf(t281,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t49665]) ).
cnf(t822,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t821,t281]) ).
cnf(t842,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t822]) ).
cnf(t12594,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t842,t12593]) ).
cnf(t50298,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t12594,t12593]) ).
cnf(t50299,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t50298,t12593]) ).
cnf(t12652,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t50299]) ).
cnf(t12662,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t55,t12652]) ).
cnf(t13157,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t12662]) ).
cnf(t13201,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t13157,t12181]) ).
cnf(t50320,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t13201,t12181]) ).
cnf(t50321,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t50320,t52]) ).
cnf(t13216,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t50321]) ).
cnf(t13218,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t13216,t281]) ).
cnf(t13274,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t13218]) ).
cnf(t13285,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t55,t13274]) ).
cnf(t20281,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t13285]) ).
cnf(t470,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t112,t459]) ).
cnf(t2062,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t470]) ).
cnf(t50285,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t2062,t12593]) ).
cnf(t12626,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t50285]) ).
cnf(t15120,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t12626]) ).
cnf(t50394,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t12181,t15120]) ).
cnf(t15208,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t50394]) ).
cnf(t27035,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t15208]) ).
cnf(t27134,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t20281,t27035]) ).
cnf(t28785,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t27134]) ).
cnf(t28821,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t28785,t281]) ).
cnf(t30560,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t28821]) ).
cnf(t30580,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t30560,t12746]) ).
cnf(t34531,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t30580]) ).
cnf(t469,plain,
meet(complement(X1),X2) = complement(join(meet(X1,X1),complement(X2))),
inference(cp,[status(thm)],[t112,t459]) ).
cnf(t2012,plain,
complement(join(meet(X1,X1),complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t469]) ).
cnf(t50286,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(step,[status(thm)],[t2012,t12593]) ).
cnf(t12627,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(rw,[status(thm)],[t50286]) ).
cnf(t15404,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t12627]) ).
cnf(t15174,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t15120,t12746]) ).
cnf(t15461,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t15174]) ).
cnf(t28816,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t28785,t15461]) ).
cnf(t33473,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t28816]) ).
cnf(t19,axiom,
sFlat2 = join(composition(sk3,converse(sk2)),sk1),
introduced(definition) ).
cnf(t49655,plain,
sFlat2 = join(sk1,composition(sk3,converse(sk2))),
inference(step,[status(thm)],[t19,t52]) ).
cnf(t18,axiom,
sFlat1 = composition(sk3,converse(sk2)),
introduced(definition) ).
cnf(t46,plain,
composition(sk3,converse(sk2)) = sFlat1,
inference(orient,[status(thm)],[t18]) ).
cnf(t49656,plain,
sFlat2 = join(sk1,sFlat1),
inference(step,[status(thm)],[t49655,t46]) ).
cnf(t49657,plain,
sFlat2 = join(sFlat1,sk1),
inference(step,[status(thm)],[t49656,t52]) ).
cnf(t72,plain,
join(sFlat1,sk1) = sFlat2,
inference(orient,[status(thm)],[t49657]) ).
cnf(t33655,plain,
join(sk1,complement(sFlat1)) = join(sk1,complement(sFlat2)),
inference(cp,[status(thm)],[t33473,t72]) ).
cnf(t33733,plain,
join(sk1,complement(sFlat2)) = join(sk1,complement(sFlat1)),
inference(orient,[status(thm)],[t33655]) ).
cnf(t33749,plain,
meet(complement(sk1),sFlat2) = complement(join(sk1,complement(sFlat1))),
inference(cp,[status(thm)],[t15404,t33733]) ).
cnf(t50789,plain,
meet(sFlat2,complement(sk1)) = complement(join(sk1,complement(sFlat1))),
inference(step,[status(thm)],[t33749,t281]) ).
cnf(t50790,plain,
meet(sFlat2,complement(sk1)) = meet(complement(sk1),sFlat1),
inference(step,[status(thm)],[t50789,t15404]) ).
cnf(t50791,plain,
meet(sFlat2,complement(sk1)) = meet(sFlat1,complement(sk1)),
inference(step,[status(thm)],[t50790,t281]) ).
cnf(t33757,plain,
meet(sFlat2,complement(sk1)) = meet(sFlat1,complement(sk1)),
inference(orient,[status(thm)],[t50791]) ).
cnf(t34579,plain,
join(complement(sFlat2),complement(sk1)) = join(complement(sFlat2),meet(sFlat1,complement(sk1))),
inference(cp,[status(thm)],[t34531,t33757]) ).
cnf(t15177,plain,
join(complement(X1),X2) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t12746,t15120]) ).
cnf(t15480,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t15177]) ).
cnf(t15493,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t15480,t12746]) ).
cnf(t15565,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t15493]) ).
cnf(t50848,plain,
complement(meet(sFlat2,sk1)) = join(complement(sFlat2),meet(sFlat1,complement(sk1))),
inference(step,[status(thm)],[t34579,t15565]) ).
cnf(t15158,plain,
meet(X1,complement(meet(complement(X1),X2))) = complement(complement(X1)),
inference(cp,[status(thm)],[t15120,t13216]) ).
cnf(t15421,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t12746,t15404]) ).
cnf(t15526,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t15421]) ).
cnf(t50502,plain,
meet(X1,join(X1,complement(X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t15158,t15526]) ).
cnf(t50503,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t50502,t12746]) ).
cnf(t16838,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t50503]) ).
cnf(t16845,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t16838,t12746]) ).
cnf(t16864,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t16845]) ).
cnf(t16913,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t16864,t52]) ).
cnf(t17006,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t16913]) ).
cnf(t73,plain,
join(sFlat1,join(sk1,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t55,t72]) ).
cnf(t295,plain,
join(sFlat1,join(sk1,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t73]) ).
cnf(t297,plain,
join(sFlat2,X1) = join(sFlat1,join(X1,sk1)),
inference(cp,[status(thm)],[t295,t52]) ).
cnf(t324,plain,
join(sFlat1,join(X1,sk1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t297]) ).
cnf(t12660,plain,
join(sFlat2,sk1) = join(sFlat1,sk1),
inference(cp,[status(thm)],[t324,t12652]) ).
cnf(t50306,plain,
join(sFlat2,sk1) = sFlat2,
inference(step,[status(thm)],[t12660,t72]) ).
cnf(t12789,plain,
join(sFlat2,sk1) = sFlat2,
inference(orient,[status(thm)],[t50306]) ).
cnf(t17032,plain,
sk1 = meet(sk1,sFlat2),
inference(cp,[status(thm)],[t17006,t12789]) ).
cnf(t50504,plain,
sk1 = meet(sFlat2,sk1),
inference(step,[status(thm)],[t17032,t281]) ).
cnf(t17083,plain,
meet(sFlat2,sk1) = sk1,
inference(orient,[status(thm)],[t50504]) ).
cnf(t50849,plain,
complement(sk1) = join(complement(sFlat2),meet(sFlat1,complement(sk1))),
inference(step,[status(thm)],[t50848,t17083]) ).
cnf(t36498,plain,
join(complement(sFlat2),meet(sFlat1,complement(sk1))) = complement(sk1),
inference(orient,[status(thm)],[t50849]) ).
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(t36,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(t17,axiom,
sFlat0 = converse(sk2),
introduced(definition) ).
cnf(t100,plain,
converse(sk2) = sFlat0,
inference(orient,[status(thm)],[t17]) ).
cnf(t101,plain,
sk2 = converse(sFlat0),
inference(cp,[status(thm)],[t24,t100]) ).
cnf(t124,plain,
converse(sFlat0) = sk2,
inference(orient,[status(thm)],[t101]) ).
cnf(t130,plain,
composition(meet(X1,composition(X2,converse(sFlat0))),meet(sFlat0,composition(converse(X1),X2))) = join(meet(composition(X1,sFlat0),X2),composition(meet(X1,composition(X2,sk2)),meet(sFlat0,composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t36,t124]) ).
cnf(t51016,plain,
composition(meet(X1,composition(X2,sk2)),meet(sFlat0,composition(converse(X1),X2))) = join(meet(composition(X1,sFlat0),X2),composition(meet(X1,composition(X2,sk2)),meet(sFlat0,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t130,t124]) ).
cnf(t49382,plain,
join(meet(composition(X1,sFlat0),X2),composition(meet(X1,composition(X2,sk2)),meet(sFlat0,composition(converse(X1),X2)))) = composition(meet(X1,composition(X2,sk2)),meet(sFlat0,composition(converse(X1),X2))),
inference(orient,[status(thm)],[t51016]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t74,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t78,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t55,t74]) ).
cnf(t3946,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t78]) ).
cnf(t62,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t55,t60]) ).
cnf(t589,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t62]) ).
cnf(t600,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t589,t52]) ).
cnf(t467,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t60,t459]) ).
cnf(t483,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t467]) ).
cnf(t594,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t589,t483]) ).
cnf(t596,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t589,t442]) ).
cnf(t49679,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t596,t60]) ).
cnf(t612,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t49679]) ).
cnf(t613,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t612,t112]) ).
cnf(t622,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t613]) ).
cnf(t49681,plain,
top = join(X1,top),
inference(step,[status(thm)],[t594,t622]) ).
cnf(t627,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t49681]) ).
cnf(t630,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t627,t52]) ).
cnf(t638,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t630]) ).
cnf(t49698,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t600,t638]) ).
cnf(t695,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t49698]) ).
cnf(t3954,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t3946,t695]) ).
cnf(t49946,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t3954,t52]) ).
cnf(t4088,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t49946]) ).
cnf(t4155,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t4088,t74]) ).
cnf(t49947,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t4155,t24]) ).
cnf(t49948,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t49947,t24]) ).
cnf(t4176,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t49948]) ).
cnf(t4221,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t4176,t52]) ).
cnf(t4234,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t4221]) ).
cnf(t7,axiom,
join(composition(complement(sk1),sk2),complement(sk3)) = complement(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t49654,plain,
join(complement(sk3),composition(complement(sk1),sk2)) = complement(sk3),
inference(step,[status(thm)],[t7,t52]) ).
cnf(t70,plain,
join(complement(sk3),composition(complement(sk1),sk2)) = complement(sk3),
inference(orient,[status(thm)],[t49654]) ).
cnf(t4286,plain,
top = join(complement(composition(complement(sk1),sk2)),complement(sk3)),
inference(cp,[status(thm)],[t4234,t70]) ).
cnf(t49974,plain,
top = join(complement(sk3),complement(composition(complement(sk1),sk2))),
inference(step,[status(thm)],[t4286,t52]) ).
cnf(t4745,plain,
join(complement(sk3),complement(composition(complement(sk1),sk2))) = top,
inference(orient,[status(thm)],[t49974]) ).
cnf(t4750,plain,
meet(sk3,composition(complement(sk1),sk2)) = complement(top),
inference(cp,[status(thm)],[t112,t4745]) ).
cnf(t49975,plain,
meet(sk3,composition(complement(sk1),sk2)) = zero,
inference(step,[status(thm)],[t4750,t142]) ).
cnf(t4753,plain,
meet(sk3,composition(complement(sk1),sk2)) = zero,
inference(orient,[status(thm)],[t49975]) ).
cnf(t49428,plain,
composition(meet(sk3,composition(complement(sk1),sk2)),meet(sFlat0,composition(converse(sk3),complement(sk1)))) = join(meet(composition(sk3,sFlat0),complement(sk1)),composition(zero,meet(sFlat0,composition(converse(sk3),complement(sk1))))),
inference(cp,[status(thm)],[t49382,t4753]) ).
cnf(t51017,plain,
composition(zero,meet(sFlat0,composition(converse(sk3),complement(sk1)))) = join(meet(composition(sk3,sFlat0),complement(sk1)),composition(zero,meet(sFlat0,composition(converse(sk3),complement(sk1))))),
inference(step,[status(thm)],[t49428,t4753]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t147,plain,
complement(top) = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(cp,[status(thm)],[t63,t142]) ).
cnf(t49805,plain,
zero = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(step,[status(thm)],[t147,t142]) ).
cnf(t2616,plain,
join(zero,composition(converse(X1),complement(composition(X1,top)))) = zero,
inference(orient,[status(thm)],[t49805]) ).
cnf(t76,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t74,t24]) ).
cnf(t488,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t76]) ).
cnf(t492,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t488,t60]) ).
cnf(t542,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t492]) ).
cnf(t643,plain,
top = converse(top),
inference(cp,[status(thm)],[t638,t542]) ).
cnf(t649,plain,
converse(top) = top,
inference(orient,[status(thm)],[t643]) ).
cnf(t2629,plain,
zero = join(zero,composition(top,complement(composition(top,top)))),
inference(cp,[status(thm)],[t2616,t649]) ).
cnf(t2655,plain,
join(zero,composition(top,complement(composition(top,top)))) = zero,
inference(orient,[status(thm)],[t2629]) ).
cnf(t50272,plain,
composition(top,complement(composition(top,top))) = zero,
inference(step,[status(thm)],[t2655,t12404]) ).
cnf(t12512,plain,
composition(top,complement(composition(top,top))) = zero,
inference(rw,[status(thm)],[t50272]) ).
cnf(t13868,plain,
composition(top,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t12512]) ).
cnf(t13870,plain,
composition(join(top,X1),complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(cp,[status(thm)],[t27,t13868]) ).
cnf(t50363,plain,
composition(top,complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t13870,t638]) ).
cnf(t50364,plain,
zero = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t50363,t13868]) ).
cnf(t50365,plain,
zero = composition(X1,complement(composition(top,top))),
inference(step,[status(thm)],[t50364,t12404]) ).
cnf(t14944,plain,
composition(X1,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t50365]) ).
cnf(t9,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t14946,plain,
zero = composition(X1,composition(X2,complement(composition(top,top)))),
inference(cp,[status(thm)],[t14944,t25]) ).
cnf(t50366,plain,
zero = composition(X1,zero),
inference(step,[status(thm)],[t14946,t14944]) ).
cnf(t14981,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t50366]) ).
cnf(t14991,plain,
composition(converse(zero),X1) = converse(zero),
inference(cp,[status(thm)],[t350,t14981]) ).
cnf(t49696,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t542,t649]) ).
cnf(t656,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t49696]) ).
cnf(t12413,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t12404,t656]) ).
cnf(t12853,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t12413]) ).
cnf(t12854,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t24,t12853]) ).
cnf(t50314,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t12854,t649]) ).
cnf(t12922,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t50314]) ).
cnf(t12923,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t12746,t12922]) ).
cnf(t50315,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t12923,t142]) ).
cnf(t12938,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t50315]) ).
cnf(t50381,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t14991,t12938]) ).
cnf(t50382,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t50381,t12938]) ).
cnf(t15015,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t50382]) ).
cnf(t51018,plain,
zero = join(meet(composition(sk3,sFlat0),complement(sk1)),composition(zero,meet(sFlat0,composition(converse(sk3),complement(sk1))))),
inference(step,[status(thm)],[t51017,t15015]) ).
cnf(t51019,plain,
zero = join(meet(complement(sk1),composition(sk3,sFlat0)),composition(zero,meet(sFlat0,composition(converse(sk3),complement(sk1))))),
inference(step,[status(thm)],[t51018,t281]) ).
cnf(t49658,plain,
composition(sk3,sFlat0) = sFlat1,
inference(step,[status(thm)],[t46,t100]) ).
cnf(t111,plain,
composition(sk3,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t49658]) ).
cnf(t134,plain,
composition(sk3,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t111]) ).
cnf(t51020,plain,
zero = join(meet(complement(sk1),sFlat1),composition(zero,meet(sFlat0,composition(converse(sk3),complement(sk1))))),
inference(step,[status(thm)],[t51019,t134]) ).
cnf(t51021,plain,
zero = join(meet(sFlat1,complement(sk1)),composition(zero,meet(sFlat0,composition(converse(sk3),complement(sk1))))),
inference(step,[status(thm)],[t51020,t281]) ).
cnf(t51022,plain,
zero = join(meet(sFlat1,complement(sk1)),zero),
inference(step,[status(thm)],[t51021,t15015]) ).
cnf(t12416,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t12404,t52]) ).
cnf(t12543,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t12416]) ).
cnf(t51023,plain,
zero = meet(sFlat1,complement(sk1)),
inference(step,[status(thm)],[t51022,t12543]) ).
cnf(t49569,plain,
meet(sFlat1,complement(sk1)) = zero,
inference(orient,[status(thm)],[t51023]) ).
cnf(t51026,plain,
join(complement(sFlat2),zero) = complement(sk1),
inference(step,[status(thm)],[t36498,t49569]) ).
cnf(t51027,plain,
complement(sFlat2) = complement(sk1),
inference(step,[status(thm)],[t51026,t12543]) ).
cnf(t49587,plain,
complement(sFlat2) = complement(sk1),
inference(rw,[status(thm)],[t51027]) ).
cnf(t49588,plain,
complement(sk1) = complement(sFlat2),
inference(orient,[status(thm)],[t49587]) ).
cnf(t49597,plain,
sk1 = complement(complement(sFlat2)),
inference(cp,[status(thm)],[t12746,t49588]) ).
cnf(t51032,plain,
sk1 = sFlat2,
inference(step,[status(thm)],[t49597,t12746]) ).
cnf(t49643,plain,
sk1 = sFlat2,
inference(orient,[status(thm)],[t51032]) ).
cnf(t12794,plain,
join(sFlat2,sFlat2) = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t324,t12789]) ).
cnf(t50307,plain,
sFlat2 = join(sFlat1,sFlat2),
inference(step,[status(thm)],[t12794,t12652]) ).
cnf(t12805,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t50307]) ).
cnf(goal_0,negated_conjecture,
join(composition(sk3,converse(sk2)),sk1) != sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(sk1,composition(sk3,converse(sk2))) != sk1,
inference(rw,[status(thm)],[goal_0,t52]) ).
cnf(g0_1,plain,
join(sFlat2,composition(sk3,converse(sk2))) != sk1,
inference(rw,[status(thm)],[g0_0,t49643]) ).
cnf(g0_2,plain,
join(sFlat2,composition(sk3,sFlat0)) != sk1,
inference(rw,[status(thm)],[g0_1,t100]) ).
cnf(g0_3,plain,
join(sFlat2,sFlat1) != sk1,
inference(rw,[status(thm)],[g0_2,t134]) ).
cnf(g0_4,plain,
join(sFlat1,sFlat2) != sk1,
inference(rw,[status(thm)],[g0_3,t52]) ).
cnf(g0_5,plain,
sFlat2 != sk1,
inference(rw,[status(thm)],[g0_4,t12805]) ).
cnf(g0_6,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_5,t49643]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL044-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n026.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 07:38:53 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 44.51/6.91 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 44.51/6.91 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------