%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL035-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:35:57 PM UTC 2026
% Result : Unsatisfiable 42.95s 5.88s
% Output : CNFRefutation 42.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 19
% Syntax : Number of clauses : 236 ( 236 unt; 0 nHn; 84 RR)
% Number of literals : 236 ( 235 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 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 : 230 ( 17 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t14,axiom,
sFlat0 = converse(sk1),
introduced(definition) ).
cnf(t78,plain,
converse(sk1) = sFlat0,
inference(orient,[status(thm)],[t14]) ).
cnf(t6,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t71,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(t24,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t73,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t71,t24]) ).
cnf(t28766,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t73,t71]) ).
cnf(t194,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t28766]) ).
cnf(t15,axiom,
sFlat1 = meet(sk2,converse(sk1)),
introduced(definition) ).
cnf(t28758,plain,
sFlat1 = meet(sk2,sFlat0),
inference(step,[status(thm)],[t15,t78]) ).
cnf(t90,plain,
meet(sk2,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t28758]) ).
cnf(t196,plain,
meet(sk2,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t90]) ).
cnf(t28768,plain,
meet(sFlat0,sk2) = sFlat1,
inference(step,[status(thm)],[t196,t194]) ).
cnf(t199,plain,
meet(sFlat0,sk2) = sFlat1,
inference(orient,[status(thm)],[t28768]) ).
cnf(t16,axiom,
sFlat2 = meet(sk1,sk3),
introduced(definition) ).
cnf(t88,plain,
meet(sk1,sk3) = sFlat2,
inference(orient,[status(thm)],[t16]) ).
cnf(t197,plain,
meet(sk1,sk3) = sFlat2,
inference(rw,[status(thm)],[t88]) ).
cnf(t28769,plain,
meet(sk3,sk1) = sFlat2,
inference(step,[status(thm)],[t197,t194]) ).
cnf(t200,plain,
meet(sk3,sk1) = sFlat2,
inference(orient,[status(thm)],[t28769]) ).
cnf(t17,axiom,
sFlat3 = composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
introduced(definition) ).
cnf(t61,plain,
composition(meet(sk2,converse(sk1)),meet(sk1,sk3)) = sFlat3,
inference(orient,[status(thm)],[t17]) ).
cnf(t28756,plain,
composition(meet(sk2,sFlat0),meet(sk1,sk3)) = sFlat3,
inference(step,[status(thm)],[t61,t78]) ).
cnf(t85,plain,
composition(meet(sk2,sFlat0),meet(sk1,sk3)) = sFlat3,
inference(rw,[status(thm)],[t28756]) ).
cnf(t28813,plain,
composition(meet(sFlat0,sk2),meet(sk1,sk3)) = sFlat3,
inference(step,[status(thm)],[t85,t194]) ).
cnf(t28814,plain,
composition(sFlat1,meet(sk1,sk3)) = sFlat3,
inference(step,[status(thm)],[t28813,t199]) ).
cnf(t28815,plain,
composition(sFlat1,meet(sk3,sk1)) = sFlat3,
inference(step,[status(thm)],[t28814,t194]) ).
cnf(t28816,plain,
composition(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t28815,t200]) ).
cnf(t827,plain,
composition(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t28816]) ).
cnf(t18,axiom,
sFlat4 = composition(sk2,meet(sk1,sk3)),
introduced(definition) ).
cnf(t66,plain,
composition(sk2,meet(sk1,sk3)) = sFlat4,
inference(orient,[status(thm)],[t18]) ).
cnf(t28757,plain,
composition(sk2,sFlat2) = sFlat4,
inference(step,[status(thm)],[t66,t88]) ).
cnf(t89,plain,
composition(sk2,sFlat2) = sFlat4,
inference(rw,[status(thm)],[t28757]) ).
cnf(t97,plain,
composition(sk2,sFlat2) = sFlat4,
inference(orient,[status(thm)],[t89]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t49,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(t51,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t49,t23]) ).
cnf(t337,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t51]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28755,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t24]) ).
cnf(t35,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t28755]) ).
cnf(t38,plain,
join(complement(X1),join(composition(converse(X2),complement(composition(X2,X1))),X3)) = join(complement(X1),X3),
inference(cp,[status(thm)],[t26,t35]) ).
cnf(t3304,plain,
join(complement(X1),join(composition(converse(X2),complement(composition(X2,X1))),X3)) = join(complement(X1),X3),
inference(orient,[status(thm)],[t38]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t56,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t3387,plain,
join(complement(top),X1) = join(complement(top),join(composition(converse(sk1),complement(sk1)),X1)),
inference(cp,[status(thm)],[t3304,t56]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t72,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t71,t29]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t86,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t28759,plain,
zero = complement(top),
inference(step,[status(thm)],[t72,t86]) ).
cnf(t102,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t28759]) ).
cnf(t29051,plain,
join(zero,X1) = join(complement(top),join(composition(converse(sk1),complement(sk1)),X1)),
inference(step,[status(thm)],[t3387,t102]) ).
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(t338,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t337,t22]) ).
cnf(t28770,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t338,t23]) ).
cnf(t356,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t28770]) ).
cnf(t357,plain,
one = converse(one),
inference(cp,[status(thm)],[t356,t22]) ).
cnf(t363,plain,
converse(one) = one,
inference(orient,[status(thm)],[t357]) ).
cnf(t28771,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t356,t363]) ).
cnf(t373,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t28771]) ).
cnf(t374,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t373]) ).
cnf(t377,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t35,t374]) ).
cnf(t28773,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t377,t363]) ).
cnf(t28774,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t28773,t374]) ).
cnf(t407,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t28774]) ).
cnf(t411,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t407,t102]) ).
cnf(t28775,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t411,t102]) ).
cnf(t28776,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t28775,t102]) ).
cnf(t420,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t28776]) ).
cnf(t421,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t26,t420]) ).
cnf(t440,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t421]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t25,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t19]) ).
cnf(t28882,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t25,t24]) ).
cnf(t28883,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t28882,t71]) ).
cnf(t28884,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t28883,t24]) ).
cnf(t1881,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t28884]) ).
cnf(t1882,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t1881,t86]) ).
cnf(t28885,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t1882,t71]) ).
cnf(t1927,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t28885]) ).
cnf(t1929,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t440,t1927]) ).
cnf(t28887,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t1929,t1927]) ).
cnf(t1937,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t28887]) ).
cnf(t29052,plain,
X1 = join(complement(top),join(composition(converse(sk1),complement(sk1)),X1)),
inference(step,[status(thm)],[t29051,t1937]) ).
cnf(t29053,plain,
X1 = join(zero,join(composition(converse(sk1),complement(sk1)),X1)),
inference(step,[status(thm)],[t29052,t102]) ).
cnf(t29054,plain,
X1 = join(composition(converse(sk1),complement(sk1)),X1),
inference(step,[status(thm)],[t29053,t1937]) ).
cnf(t29055,plain,
X1 = join(composition(sFlat0,complement(sk1)),X1),
inference(step,[status(thm)],[t29054,t78]) ).
cnf(t3717,plain,
join(composition(sFlat0,complement(sk1)),X1) = X1,
inference(orient,[status(thm)],[t29055]) ).
cnf(t1947,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t1937,t24]) ).
cnf(t1977,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t1947]) ).
cnf(t3721,plain,
zero = composition(sFlat0,complement(sk1)),
inference(cp,[status(thm)],[t3717,t1977]) ).
cnf(t3750,plain,
composition(sFlat0,complement(sk1)) = zero,
inference(orient,[status(thm)],[t3721]) ).
cnf(t3756,plain,
composition(join(sFlat0,X1),complement(sk1)) = join(zero,composition(X1,complement(sk1))),
inference(cp,[status(thm)],[t32,t3750]) ).
cnf(t29231,plain,
composition(join(sFlat0,X1),complement(sk1)) = composition(X1,complement(sk1)),
inference(step,[status(thm)],[t3756,t1937]) ).
cnf(t6662,plain,
composition(join(sFlat0,X1),complement(sk1)) = composition(X1,complement(sk1)),
inference(orient,[status(thm)],[t29231]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t39,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t83,plain,
converse(join(X1,sk1)) = join(converse(X1),sFlat0),
inference(cp,[status(thm)],[t39,t78]) ).
cnf(t28763,plain,
converse(join(X1,sk1)) = join(sFlat0,converse(X1)),
inference(step,[status(thm)],[t83,t24]) ).
cnf(t146,plain,
converse(join(X1,sk1)) = join(sFlat0,converse(X1)),
inference(orient,[status(thm)],[t28763]) ).
cnf(t408,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t407,t71]) ).
cnf(t28835,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t408,t71]) ).
cnf(t28836,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t28835,t71]) ).
cnf(t1141,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t28836]) ).
cnf(t28888,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t1927,t1937]) ).
cnf(t1961,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t28888]) ).
cnf(t1989,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1961]) ).
cnf(t1990,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t1141,t1989]) ).
cnf(t28907,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t1990,t1989]) ).
cnf(t28908,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t28907,t1989]) ).
cnf(t2004,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t28908]) ).
cnf(t28,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t26,t24]) ).
cnf(t28811,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t28,t26]) ).
cnf(t763,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t28811]) ).
cnf(t2006,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t2004,t763]) ).
cnf(t28922,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t2006,t26]) ).
cnf(t28923,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t28922,t2004]) ).
cnf(t2123,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t28923]) ).
cnf(t2127,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t2123,t1881]) ).
cnf(t28924,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t2127,t1881]) ).
cnf(t28925,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t28924,t24]) ).
cnf(t2137,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t28925]) ).
cnf(t2141,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t2137,t194]) ).
cnf(t2176,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t2141]) ).
cnf(t2178,plain,
sk1 = join(sk1,sFlat2),
inference(cp,[status(thm)],[t2176,t200]) ).
cnf(t28928,plain,
sk1 = join(sFlat2,sk1),
inference(step,[status(thm)],[t2178,t24]) ).
cnf(t2195,plain,
join(sFlat2,sk1) = sk1,
inference(orient,[status(thm)],[t28928]) ).
cnf(t2197,plain,
join(sFlat0,converse(sFlat2)) = converse(sk1),
inference(cp,[status(thm)],[t146,t2195]) ).
cnf(t28932,plain,
join(sFlat0,converse(sFlat2)) = sFlat0,
inference(step,[status(thm)],[t2197,t78]) ).
cnf(t2214,plain,
join(sFlat0,converse(sFlat2)) = sFlat0,
inference(orient,[status(thm)],[t28932]) ).
cnf(t6698,plain,
composition(converse(sFlat2),complement(sk1)) = composition(sFlat0,complement(sk1)),
inference(cp,[status(thm)],[t6662,t2214]) ).
cnf(t29233,plain,
composition(converse(sFlat2),complement(sk1)) = zero,
inference(step,[status(thm)],[t6698,t3750]) ).
cnf(t6768,plain,
composition(converse(sFlat2),complement(sk1)) = zero,
inference(orient,[status(thm)],[t29233]) ).
cnf(t6778,plain,
composition(converse(complement(sk1)),sFlat2) = converse(zero),
inference(cp,[status(thm)],[t337,t6768]) ).
cnf(t417,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t71,t407]) ).
cnf(t430,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t417]) ).
cnf(t28896,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t430,t1989]) ).
cnf(t1993,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t28896]) ).
cnf(t2017,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1993]) ).
cnf(t41,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t39,t23]) ).
cnf(t237,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t41]) ).
cnf(t240,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t237,t29]) ).
cnf(t467,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t240]) ).
cnf(t31,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t26,t29]) ).
cnf(t529,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t31]) ).
cnf(t435,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t29,t430]) ).
cnf(t460,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t435]) ).
cnf(t534,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t529,t460]) ).
cnf(t536,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t529,t407]) ).
cnf(t28783,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t536,t29]) ).
cnf(t555,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t28783]) ).
cnf(t556,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t555,t71]) ).
cnf(t567,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t556]) ).
cnf(t28787,plain,
top = join(X1,top),
inference(step,[status(thm)],[t534,t567]) ).
cnf(t586,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t28787]) ).
cnf(t587,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t586,t24]) ).
cnf(t598,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t587]) ).
cnf(t601,plain,
top = converse(top),
inference(cp,[status(thm)],[t598,t467]) ).
cnf(t608,plain,
converse(top) = top,
inference(orient,[status(thm)],[t601]) ).
cnf(t28798,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t467,t608]) ).
cnf(t615,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t28798]) ).
cnf(t1945,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t1937,t615]) ).
cnf(t2033,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t1945]) ).
cnf(t2034,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t23,t2033]) ).
cnf(t28910,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t2034,t608]) ).
cnf(t2048,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t28910]) ).
cnf(t2049,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t2017,t2048]) ).
cnf(t28911,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t2049,t102]) ).
cnf(t2054,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t28911]) ).
cnf(t29234,plain,
composition(converse(complement(sk1)),sFlat2) = zero,
inference(step,[status(thm)],[t6778,t2054]) ).
cnf(t6781,plain,
composition(converse(complement(sk1)),sFlat2) = zero,
inference(orient,[status(thm)],[t29234]) ).
cnf(t6783,plain,
composition(join(converse(complement(sk1)),X1),sFlat2) = join(zero,composition(X1,sFlat2)),
inference(cp,[status(thm)],[t32,t6781]) ).
cnf(t29470,plain,
composition(join(converse(complement(sk1)),X1),sFlat2) = composition(X1,sFlat2),
inference(step,[status(thm)],[t6783,t1937]) ).
cnf(t13153,plain,
composition(join(converse(complement(sk1)),X1),sFlat2) = composition(X1,sFlat2),
inference(orient,[status(thm)],[t29470]) ).
cnf(t2187,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t26,t2176]) ).
cnf(t9779,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t2187]) ).
cnf(t2018,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t2017,t71]) ).
cnf(t2687,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t2018]) ).
cnf(t2690,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t2687,t2017]) ).
cnf(t2874,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t2690]) ).
cnf(t2880,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t2017,t2874]) ).
cnf(t3123,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t2880]) ).
cnf(t29022,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t1881,t3123]) ).
cnf(t3167,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t29022]) ).
cnf(t26317,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t3167]) ).
cnf(t26482,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t9779,t26317]) ).
cnf(t26930,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t26482]) ).
cnf(t26976,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t26930,t194]) ).
cnf(t27583,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t26976]) ).
cnf(t3136,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t3123,t615]) ).
cnf(t29731,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(step,[status(thm)],[t3136,t102]) ).
cnf(t26305,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(orient,[status(thm)],[t29731]) ).
cnf(t27599,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t27583,t26305]) ).
cnf(t29773,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t27599,t2017]) ).
cnf(t29774,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t29773,t1977]) ).
cnf(t28018,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t29774]) ).
cnf(t28135,plain,
composition(complement(converse(complement(converse(converse(complement(sk1)))))),sFlat2) = composition(converse(complement(sk1)),sFlat2),
inference(cp,[status(thm)],[t13153,t28018]) ).
cnf(t29775,plain,
composition(complement(converse(complement(complement(sk1)))),sFlat2) = composition(converse(complement(sk1)),sFlat2),
inference(step,[status(thm)],[t28135,t23]) ).
cnf(t29776,plain,
composition(complement(converse(sk1)),sFlat2) = composition(converse(complement(sk1)),sFlat2),
inference(step,[status(thm)],[t29775,t2017]) ).
cnf(t29777,plain,
composition(complement(sFlat0),sFlat2) = composition(converse(complement(sk1)),sFlat2),
inference(step,[status(thm)],[t29776,t78]) ).
cnf(t29778,plain,
composition(complement(sFlat0),sFlat2) = zero,
inference(step,[status(thm)],[t29777,t6781]) ).
cnf(t28143,plain,
composition(complement(sFlat0),sFlat2) = zero,
inference(orient,[status(thm)],[t29778]) ).
cnf(t28145,plain,
composition(join(complement(sFlat0),X1),sFlat2) = join(zero,composition(X1,sFlat2)),
inference(cp,[status(thm)],[t32,t28143]) ).
cnf(t29802,plain,
composition(join(complement(sFlat0),X1),sFlat2) = composition(X1,sFlat2),
inference(step,[status(thm)],[t28145,t1937]) ).
cnf(t28659,plain,
composition(join(complement(sFlat0),X1),sFlat2) = composition(X1,sFlat2),
inference(orient,[status(thm)],[t29802]) ).
cnf(t28669,plain,
composition(meet(complement(complement(sFlat0)),X1),sFlat2) = composition(join(complement(sFlat0),X1),sFlat2),
inference(cp,[status(thm)],[t28659,t27583]) ).
cnf(t29803,plain,
composition(meet(sFlat0,X1),sFlat2) = composition(join(complement(sFlat0),X1),sFlat2),
inference(step,[status(thm)],[t28669,t2017]) ).
cnf(t29804,plain,
composition(meet(sFlat0,X1),sFlat2) = composition(X1,sFlat2),
inference(step,[status(thm)],[t29803,t28659]) ).
cnf(t28709,plain,
composition(meet(sFlat0,X1),sFlat2) = composition(X1,sFlat2),
inference(orient,[status(thm)],[t29804]) ).
cnf(t28713,plain,
composition(sk2,sFlat2) = composition(sFlat1,sFlat2),
inference(cp,[status(thm)],[t28709,t199]) ).
cnf(t29805,plain,
sFlat4 = composition(sFlat1,sFlat2),
inference(step,[status(thm)],[t28713,t97]) ).
cnf(t29806,plain,
sFlat4 = sFlat3,
inference(step,[status(thm)],[t29805,t827]) ).
cnf(t28740,plain,
sFlat4 = sFlat3,
inference(orient,[status(thm)],[t29806]) ).
cnf(t29807,plain,
composition(sk2,sFlat2) = sFlat3,
inference(step,[status(thm)],[t97,t28740]) ).
cnf(t28741,plain,
composition(sk2,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t29807]) ).
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,t78]) ).
cnf(g0_1,plain,
composition(meet(sFlat0,sk2),meet(sk1,sk3)) != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_0,t194]) ).
cnf(g0_2,plain,
composition(sFlat1,meet(sk1,sk3)) != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_1,t199]) ).
cnf(g0_3,plain,
composition(sFlat1,meet(sk3,sk1)) != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_2,t194]) ).
cnf(g0_4,plain,
composition(sFlat1,sFlat2) != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_3,t200]) ).
cnf(g0_5,plain,
sFlat3 != composition(sk2,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_4,t827]) ).
cnf(g0_6,plain,
sFlat3 != composition(sk2,meet(sk3,sk1)),
inference(rw,[status(thm)],[g0_5,t194]) ).
cnf(g0_7,plain,
sFlat3 != composition(sk2,sFlat2),
inference(rw,[status(thm)],[g0_6,t200]) ).
cnf(g0_8,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_7,t28741]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL035-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 07:30:02 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 42.95/5.88 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.95/5.88 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------