%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL024-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 : n004.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:51 PM UTC 2026
% Result : Unsatisfiable 18.54s 2.91s
% Output : CNFRefutation 18.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 115
% Number of leaves : 14
% Syntax : Number of clauses : 257 ( 257 unt; 0 nHn; 58 RR)
% Number of literals : 257 ( 256 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 318 ( 63 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t29,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t23,t26]) ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t42,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t4064,plain,
composition(join(X2,converse(X1)),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(step,[status(thm)],[t29,t42]) ).
cnf(t4065,plain,
composition(join(X2,converse(X1)),converse(X3)) = join(composition(X2,converse(X3)),converse(composition(X3,X1))),
inference(step,[status(thm)],[t4064,t42]) ).
cnf(t1512,plain,
join(composition(X1,converse(X2)),converse(composition(X2,X3))) = composition(join(X1,converse(X3)),converse(X2)),
inference(orient,[status(thm)],[t4065]) ).
cnf(t1518,plain,
composition(join(converse(X1),converse(X2)),converse(X3)) = join(converse(composition(X3,X1)),converse(composition(X3,X2))),
inference(cp,[status(thm)],[t1512,t26]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t69,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t4066,plain,
composition(converse(join(X1,X2)),converse(X3)) = join(converse(composition(X3,X1)),converse(composition(X3,X2))),
inference(step,[status(thm)],[t1518,t69]) ).
cnf(t4067,plain,
converse(composition(X3,join(X1,X2))) = join(converse(composition(X3,X1)),converse(composition(X3,X2))),
inference(step,[status(thm)],[t4066,t26]) ).
cnf(t4068,plain,
converse(composition(X3,join(X1,X2))) = converse(join(composition(X3,X1),composition(X3,X2))),
inference(step,[status(thm)],[t4067,t69]) ).
cnf(t1559,plain,
converse(join(composition(X1,X2),composition(X1,X3))) = converse(composition(X1,join(X2,X3))),
inference(orient,[status(thm)],[t4068]) ).
cnf(t1611,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(converse(composition(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t20,t1559]) ).
cnf(t4069,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t1611,t20]) ).
cnf(t1639,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t4069]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t95,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t97,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t95,t42]) ).
cnf(t3963,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t97,t95]) ).
cnf(t117,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t3963]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t3959,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t9,t42]) ).
cnf(t45,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t3959]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t3960,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t42]) ).
cnf(t62,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t3960]) ).
cnf(t28,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t26,t20]) ).
cnf(t149,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t28]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t16,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t150,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t149,t16]) ).
cnf(t3966,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t150,t20]) ).
cnf(t160,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t3966]) ).
cnf(t161,plain,
one = converse(one),
inference(cp,[status(thm)],[t160,t16]) ).
cnf(t167,plain,
converse(one) = one,
inference(orient,[status(thm)],[t161]) ).
cnf(t3967,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t160,t167]) ).
cnf(t175,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t3967]) ).
cnf(t176,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t175]) ).
cnf(t179,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t62,t176]) ).
cnf(t3969,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t179,t167]) ).
cnf(t3970,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t3969,t176]) ).
cnf(t190,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t3970]) ).
cnf(t191,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t190,t95]) ).
cnf(t3983,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t191,t95]) ).
cnf(t3984,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t3983,t95]) ).
cnf(t307,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t3984]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t44,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t17]) ).
cnf(t4115,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t44,t42]) ).
cnf(t4116,plain,
join(complement(join(X2,complement(X1))),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t4115,t42]) ).
cnf(t4117,plain,
join(complement(join(X2,complement(X1))),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t4116,t95]) ).
cnf(t4118,plain,
join(meet(X1,X2),complement(join(X2,complement(X1)))) = X1,
inference(step,[status(thm)],[t4117,t42]) ).
cnf(t3007,plain,
join(meet(X1,X2),complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t4118]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t102,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t3008,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t3007,t102]) ).
cnf(t4131,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t3008,t95]) ).
cnf(t3108,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t4131]) ).
cnf(t71,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t69,t20]) ).
cnf(t3974,plain,
converse(join(X2,converse(X1))) = join(X1,converse(X2)),
inference(step,[status(thm)],[t71,t42]) ).
cnf(t240,plain,
converse(join(X1,converse(X2))) = join(X2,converse(X1)),
inference(orient,[status(thm)],[t3974]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t59,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t60,plain,
join(X1,join(complement(X1),X2)) = join(X2,top),
inference(cp,[status(thm)],[t45,t59]) ).
cnf(t3975,plain,
join(X1,join(X2,complement(X1))) = join(X2,top),
inference(step,[status(thm)],[t60,t42]) ).
cnf(t255,plain,
join(X1,join(X2,complement(X1))) = join(X2,top),
inference(orient,[status(thm)],[t3975]) ).
cnf(t257,plain,
join(complement(X1),top) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t255,t190]) ).
cnf(t3976,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(step,[status(thm)],[t257,t42]) ).
cnf(t3977,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t3976,t59]) ).
cnf(t265,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t3977]) ).
cnf(t270,plain,
join(top,top) = join(X1,top),
inference(cp,[status(thm)],[t255,t265]) ).
cnf(t279,plain,
join(top,top) = join(X1,top),
inference(orient,[status(thm)],[t270]) ).
cnf(t280,plain,
join(X1,top) = join(top,top),
inference(cp,[status(thm)],[t279,t42]) ).
cnf(t3978,plain,
join(X1,top) = join(zero,top),
inference(step,[status(thm)],[t280,t279]) ).
cnf(t96,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t95,t59]) ).
cnf(t3961,plain,
zero = complement(top),
inference(step,[status(thm)],[t96,t102]) ).
cnf(t107,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t3961]) ).
cnf(t109,plain,
top = join(top,zero),
inference(cp,[status(thm)],[t59,t107]) ).
cnf(t3962,plain,
top = join(zero,top),
inference(step,[status(thm)],[t109,t42]) ).
cnf(t114,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t3962]) ).
cnf(t3979,plain,
join(X1,top) = top,
inference(step,[status(thm)],[t3978,t114]) ).
cnf(t288,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t3979]) ).
cnf(t3980,plain,
join(X1,join(X2,complement(X1))) = top,
inference(step,[status(thm)],[t255,t288]) ).
cnf(t289,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t3980]) ).
cnf(t1640,plain,
composition(X1,join(X2,X2)) = composition(join(X1,X1),X2),
inference(cp,[status(thm)],[t1639,t23]) ).
cnf(t1693,plain,
composition(X1,join(X2,X2)) = composition(join(X1,X1),X2),
inference(orient,[status(thm)],[t1640]) ).
cnf(t1734,plain,
composition(top,join(X1,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t1693,t288]) ).
cnf(t1782,plain,
composition(top,join(X1,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t1734]) ).
cnf(t1792,plain,
composition(join(X1,top),join(X2,X2)) = join(composition(X1,join(X2,X2)),composition(top,X2)),
inference(cp,[status(thm)],[t23,t1782]) ).
cnf(t4103,plain,
composition(top,join(X2,X2)) = join(composition(X1,join(X2,X2)),composition(top,X2)),
inference(step,[status(thm)],[t1792,t288]) ).
cnf(t4104,plain,
composition(top,X2) = join(composition(X1,join(X2,X2)),composition(top,X2)),
inference(step,[status(thm)],[t4103,t1782]) ).
cnf(t4105,plain,
composition(top,X2) = join(composition(top,X2),composition(X1,join(X2,X2))),
inference(step,[status(thm)],[t4104,t42]) ).
cnf(t2735,plain,
join(composition(top,X1),composition(X2,join(X1,X1))) = composition(top,X1),
inference(orient,[status(thm)],[t4105]) ).
cnf(t168,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t69,t167]) ).
cnf(t3968,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t168,t42]) ).
cnf(t180,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t3968]) ).
cnf(t186,plain,
converse(composition(join(X1,one),X2)) = composition(converse(X2),join(one,converse(X1))),
inference(cp,[status(thm)],[t26,t180]) ).
cnf(t612,plain,
composition(converse(X1),join(one,converse(X2))) = converse(composition(join(X2,one),X1)),
inference(orient,[status(thm)],[t186]) ).
cnf(t623,plain,
converse(composition(join(one,one),X1)) = composition(converse(X1),join(one,one)),
inference(cp,[status(thm)],[t612,t167]) ).
cnf(t634,plain,
converse(composition(join(one,one),X1)) = composition(converse(X1),join(one,one)),
inference(orient,[status(thm)],[t623]) ).
cnf(t1049,plain,
converse(composition(join(one,one),X1)) = composition(converse(X1),join(one,one)),
inference(rw,[status(thm)],[t634]) ).
cnf(t177,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t23,t176]) ).
cnf(t4028,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(step,[status(thm)],[t177,t42]) ).
cnf(t1026,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t4028]) ).
cnf(t4031,plain,
converse(join(X1,composition(one,X1))) = composition(converse(X1),join(one,one)),
inference(step,[status(thm)],[t1049,t1026]) ).
cnf(t4032,plain,
converse(join(X1,X1)) = composition(converse(X1),join(one,one)),
inference(step,[status(thm)],[t4031,t176]) ).
cnf(t1058,plain,
converse(join(X1,X1)) = composition(converse(X1),join(one,one)),
inference(orient,[status(thm)],[t4032]) ).
cnf(t1064,plain,
composition(converse(meet(X1,X2)),join(one,one)) = converse(meet(X1,X2)),
inference(cp,[status(thm)],[t1058,t307]) ).
cnf(t1217,plain,
composition(converse(meet(X1,X2)),join(one,one)) = converse(meet(X1,X2)),
inference(orient,[status(thm)],[t1064]) ).
cnf(t2753,plain,
composition(top,one) = join(composition(top,one),converse(meet(X1,X2))),
inference(cp,[status(thm)],[t2735,t1217]) ).
cnf(t4106,plain,
top = join(composition(top,one),converse(meet(X1,X2))),
inference(step,[status(thm)],[t2753,t16]) ).
cnf(t4107,plain,
top = join(top,converse(meet(X1,X2))),
inference(step,[status(thm)],[t4106,t16]) ).
cnf(t2774,plain,
join(top,converse(meet(X1,X2))) = top,
inference(orient,[status(thm)],[t4107]) ).
cnf(t110,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t95,t107]) ).
cnf(t3965,plain,
meet(X1,top) = complement(join(zero,complement(X1))),
inference(step,[status(thm)],[t110,t117]) ).
cnf(t125,plain,
complement(join(zero,complement(X1))) = meet(X1,top),
inference(orient,[status(thm)],[t3965]) ).
cnf(t127,plain,
meet(top,top) = complement(join(zero,zero)),
inference(cp,[status(thm)],[t125,t107]) ).
cnf(t134,plain,
complement(join(zero,zero)) = meet(top,top),
inference(orient,[status(thm)],[t127]) ).
cnf(t194,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t190,t107]) ).
cnf(t3971,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t194,t107]) ).
cnf(t3972,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t3971,t107]) ).
cnf(t202,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t3972]) ).
cnf(t3973,plain,
complement(zero) = meet(top,top),
inference(step,[status(thm)],[t134,t202]) ).
cnf(t205,plain,
complement(zero) = meet(top,top),
inference(rw,[status(thm)],[t3973]) ).
cnf(t206,plain,
meet(top,top) = complement(zero),
inference(orient,[status(thm)],[t205]) ).
cnf(t2780,plain,
top = join(top,converse(complement(zero))),
inference(cp,[status(thm)],[t2774,t206]) ).
cnf(t2799,plain,
join(top,converse(complement(zero))) = top,
inference(orient,[status(thm)],[t2780]) ).
cnf(t2800,plain,
join(complement(zero),converse(top)) = converse(top),
inference(cp,[status(thm)],[t240,t2799]) ).
cnf(t4108,plain,
join(converse(top),complement(zero)) = converse(top),
inference(step,[status(thm)],[t2800,t42]) ).
cnf(t2805,plain,
join(converse(top),complement(zero)) = converse(top),
inference(orient,[status(thm)],[t4108]) ).
cnf(t2806,plain,
top = join(zero,converse(top)),
inference(cp,[status(thm)],[t289,t2805]) ).
cnf(t2775,plain,
top = join(top,converse(zero)),
inference(cp,[status(thm)],[t2774,t102]) ).
cnf(t2789,plain,
join(top,converse(zero)) = top,
inference(orient,[status(thm)],[t2775]) ).
cnf(t2790,plain,
join(zero,converse(top)) = converse(top),
inference(cp,[status(thm)],[t240,t2789]) ).
cnf(t2795,plain,
join(zero,converse(top)) = converse(top),
inference(orient,[status(thm)],[t2790]) ).
cnf(t4109,plain,
top = converse(top),
inference(step,[status(thm)],[t2806,t2795]) ).
cnf(t2812,plain,
converse(top) = top,
inference(orient,[status(thm)],[t4109]) ).
cnf(t2824,plain,
join(top,converse(X1)) = converse(join(X1,top)),
inference(cp,[status(thm)],[t240,t2812]) ).
cnf(t4113,plain,
join(top,converse(X1)) = converse(top),
inference(step,[status(thm)],[t2824,t288]) ).
cnf(t4114,plain,
join(top,converse(X1)) = top,
inference(step,[status(thm)],[t4113,t2812]) ).
cnf(t2842,plain,
join(top,converse(X1)) = top,
inference(orient,[status(thm)],[t4114]) ).
cnf(t27,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t26,t20]) ).
cnf(t141,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t27]) ).
cnf(t2853,plain,
top = join(top,composition(X1,converse(X2))),
inference(cp,[status(thm)],[t2842,t141]) ).
cnf(t2972,plain,
join(top,composition(X1,converse(X2))) = top,
inference(orient,[status(thm)],[t2853]) ).
cnf(t2978,plain,
top = join(top,composition(X1,top)),
inference(cp,[status(thm)],[t2972,t2812]) ).
cnf(t2998,plain,
join(top,composition(X1,top)) = top,
inference(orient,[status(thm)],[t2978]) ).
cnf(t1645,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(cp,[status(thm)],[t1639,t16]) ).
cnf(t4098,plain,
composition(X1,join(X2,one)) = join(X1,composition(X1,X2)),
inference(step,[status(thm)],[t1645,t42]) ).
cnf(t2390,plain,
composition(X1,join(X2,one)) = join(X1,composition(X1,X2)),
inference(orient,[status(thm)],[t4098]) ).
cnf(t2851,plain,
top = join(top,one),
inference(cp,[status(thm)],[t2842,t167]) ).
cnf(t2862,plain,
join(top,one) = top,
inference(orient,[status(thm)],[t2851]) ).
cnf(t2865,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(cp,[status(thm)],[t2390,t2862]) ).
cnf(t2930,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t2865]) ).
cnf(t2999,plain,
top = composition(top,top),
inference(cp,[status(thm)],[t2998,t2930]) ).
cnf(t3039,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t2999]) ).
cnf(t3046,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t62,t3039]) ).
cnf(t4119,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t3046,t107]) ).
cnf(t4120,plain,
zero = composition(join(converse(top),one),complement(top)),
inference(step,[status(thm)],[t4119,t1026]) ).
cnf(t4121,plain,
zero = composition(join(one,converse(top)),complement(top)),
inference(step,[status(thm)],[t4120,t42]) ).
cnf(t4122,plain,
zero = composition(join(one,top),complement(top)),
inference(step,[status(thm)],[t4121,t2812]) ).
cnf(t4123,plain,
zero = composition(top,complement(top)),
inference(step,[status(thm)],[t4122,t288]) ).
cnf(t4124,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t4123,t107]) ).
cnf(t3049,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t4124]) ).
cnf(t3055,plain,
composition(join(X1,top),zero) = join(composition(X1,zero),zero),
inference(cp,[status(thm)],[t23,t3049]) ).
cnf(t4138,plain,
composition(top,zero) = join(composition(X1,zero),zero),
inference(step,[status(thm)],[t3055,t288]) ).
cnf(t4139,plain,
zero = join(composition(X1,zero),zero),
inference(step,[status(thm)],[t4138,t3049]) ).
cnf(t4140,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t4139,t42]) ).
cnf(t3137,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t4140]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t3139,plain,
zero = join(zero,composition(X1,composition(X2,zero))),
inference(cp,[status(thm)],[t3137,t21]) ).
cnf(t3561,plain,
join(zero,composition(X1,composition(X2,zero))) = zero,
inference(orient,[status(thm)],[t3139]) ).
cnf(t3052,plain,
composition(top,join(zero,X1)) = join(zero,composition(top,X1)),
inference(cp,[status(thm)],[t1639,t3049]) ).
cnf(t4170,plain,
composition(top,join(X1,zero)) = join(zero,composition(top,X1)),
inference(step,[status(thm)],[t3052,t42]) ).
cnf(t1789,plain,
composition(top,join(join(X1,X1),X2)) = join(composition(top,X1),composition(top,X2)),
inference(cp,[status(thm)],[t1639,t1782]) ).
cnf(t4085,plain,
composition(top,join(X2,join(X1,X1))) = join(composition(top,X1),composition(top,X2)),
inference(step,[status(thm)],[t1789,t42]) ).
cnf(t4086,plain,
composition(top,join(X1,join(X2,X1))) = join(composition(top,X1),composition(top,X2)),
inference(step,[status(thm)],[t4085,t45]) ).
cnf(t4087,plain,
composition(top,join(X1,join(X1,X2))) = join(composition(top,X1),composition(top,X2)),
inference(step,[status(thm)],[t4086,t45]) ).
cnf(t4088,plain,
composition(top,join(X1,join(X1,X2))) = composition(top,join(X1,X2)),
inference(step,[status(thm)],[t4087,t1639]) ).
cnf(t2123,plain,
composition(top,join(X1,join(X1,X2))) = composition(top,join(X1,X2)),
inference(orient,[status(thm)],[t4088]) ).
cnf(t3110,plain,
composition(top,join(zero,meet(X1,X1))) = composition(top,join(zero,X1)),
inference(cp,[status(thm)],[t2123,t3108]) ).
cnf(t4151,plain,
composition(top,X1) = composition(top,join(zero,X1)),
inference(step,[status(thm)],[t3110,t3108]) ).
cnf(t4152,plain,
composition(top,X1) = composition(top,join(X1,zero)),
inference(step,[status(thm)],[t4151,t42]) ).
cnf(t3252,plain,
composition(top,join(X1,zero)) = composition(top,X1),
inference(orient,[status(thm)],[t4152]) ).
cnf(t4171,plain,
composition(top,X1) = join(zero,composition(top,X1)),
inference(step,[status(thm)],[t4170,t3252]) ).
cnf(t3425,plain,
join(zero,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t4171]) ).
cnf(t3563,plain,
zero = composition(top,composition(X1,zero)),
inference(cp,[status(thm)],[t3561,t3425]) ).
cnf(t3593,plain,
composition(top,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t3563]) ).
cnf(t3609,plain,
complement(composition(X1,zero)) = join(complement(composition(X1,zero)),composition(converse(top),complement(zero))),
inference(cp,[status(thm)],[t62,t3593]) ).
cnf(t4196,plain,
complement(composition(X1,zero)) = join(complement(composition(X1,zero)),composition(top,complement(zero))),
inference(step,[status(thm)],[t3609,t2812]) ).
cnf(t3062,plain,
complement(zero) = join(complement(zero),composition(converse(top),complement(zero))),
inference(cp,[status(thm)],[t62,t3049]) ).
cnf(t4127,plain,
complement(zero) = composition(join(converse(top),one),complement(zero)),
inference(step,[status(thm)],[t3062,t1026]) ).
cnf(t4128,plain,
complement(zero) = composition(join(one,converse(top)),complement(zero)),
inference(step,[status(thm)],[t4127,t42]) ).
cnf(t4129,plain,
complement(zero) = composition(join(one,top),complement(zero)),
inference(step,[status(thm)],[t4128,t2812]) ).
cnf(t4130,plain,
complement(zero) = composition(top,complement(zero)),
inference(step,[status(thm)],[t4129,t288]) ).
cnf(t3084,plain,
composition(top,complement(zero)) = complement(zero),
inference(orient,[status(thm)],[t4130]) ).
cnf(t4197,plain,
complement(composition(X1,zero)) = join(complement(composition(X1,zero)),complement(zero)),
inference(step,[status(thm)],[t4196,t3084]) ).
cnf(t3427,plain,
composition(top,complement(zero)) = join(zero,complement(zero)),
inference(cp,[status(thm)],[t3425,t3084]) ).
cnf(t4172,plain,
complement(zero) = join(zero,complement(zero)),
inference(step,[status(thm)],[t3427,t3084]) ).
cnf(t4173,plain,
complement(zero) = top,
inference(step,[status(thm)],[t4172,t59]) ).
cnf(t3433,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t4173]) ).
cnf(t4198,plain,
complement(composition(X1,zero)) = join(complement(composition(X1,zero)),top),
inference(step,[status(thm)],[t4197,t3433]) ).
cnf(t4199,plain,
complement(composition(X1,zero)) = top,
inference(step,[status(thm)],[t4198,t288]) ).
cnf(t3614,plain,
complement(composition(X1,zero)) = top,
inference(orient,[status(thm)],[t4199]) ).
cnf(t3620,plain,
meet(composition(X1,zero),X2) = complement(join(top,complement(X2))),
inference(cp,[status(thm)],[t95,t3614]) ).
cnf(t4201,plain,
meet(X2,composition(X1,zero)) = complement(join(top,complement(X2))),
inference(step,[status(thm)],[t3620,t117]) ).
cnf(t4202,plain,
meet(X2,composition(X1,zero)) = complement(top),
inference(step,[status(thm)],[t4201,t265]) ).
cnf(t4203,plain,
meet(X2,composition(X1,zero)) = zero,
inference(step,[status(thm)],[t4202,t107]) ).
cnf(t3645,plain,
meet(X1,composition(X2,zero)) = zero,
inference(orient,[status(thm)],[t4203]) ).
cnf(t3650,plain,
composition(X1,zero) = join(zero,zero),
inference(cp,[status(thm)],[t3108,t3645]) ).
cnf(t4204,plain,
composition(X1,zero) = zero,
inference(step,[status(thm)],[t3650,t202]) ).
cnf(t3659,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t4204]) ).
cnf(t3666,plain,
composition(converse(zero),X1) = converse(zero),
inference(cp,[status(thm)],[t149,t3659]) ).
cnf(t3673,plain,
composition(converse(zero),X1) = converse(zero),
inference(orient,[status(thm)],[t3666]) ).
cnf(t3674,plain,
converse(zero) = zero,
inference(cp,[status(thm)],[t3673,t3659]) ).
cnf(t3701,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t3674]) ).
cnf(t4205,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t3673,t3701]) ).
cnf(t4206,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t4205,t3701]) ).
cnf(t3731,plain,
composition(zero,X1) = zero,
inference(rw,[status(thm)],[t4206]) ).
cnf(t3734,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t3731]) ).
cnf(t3744,plain,
complement(X1) = join(complement(X1),composition(converse(zero),complement(zero))),
inference(cp,[status(thm)],[t62,t3734]) ).
cnf(t4210,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t3744,t3701]) ).
cnf(t4211,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t4210,t3734]) ).
cnf(t4212,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t4211,t42]) ).
cnf(t3750,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t4212]) ).
cnf(t199,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t95,t190]) ).
cnf(t207,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t199]) ).
cnf(t3753,plain,
complement(complement(X1)) = join(zero,meet(X1,X1)),
inference(cp,[status(thm)],[t3750,t207]) ).
cnf(t4215,plain,
meet(X1,X1) = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t3753,t207]) ).
cnf(t4216,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t4215,t3108]) ).
cnf(t3816,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t4216]) ).
cnf(t3820,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t307,t3816]) ).
cnf(t4227,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t3820,t3816]) ).
cnf(t4228,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t4227,t3816]) ).
cnf(t3884,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t4228]) ).
cnf(t3892,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(cp,[status(thm)],[t45,t3884]) ).
cnf(t4242,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t3892,t42]) ).
cnf(t3941,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t4242]) ).
cnf(t3945,plain,
join(meet(X1,X2),complement(join(X2,complement(X1)))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t3941,t3007]) ).
cnf(t4243,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t3945,t3007]) ).
cnf(t4244,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t4243,t42]) ).
cnf(t3953,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t4244]) ).
cnf(goal_0,negated_conjecture,
join(composition(meet(sk1,converse(sk2)),meet(sk2,sk3)),composition(meet(sk1,converse(sk2)),sk3)) != composition(meet(sk1,converse(sk2)),sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
composition(meet(sk1,converse(sk2)),join(meet(sk2,sk3),sk3)) != composition(meet(sk1,converse(sk2)),sk3),
inference(rw,[status(thm)],[goal_0,t1639]) ).
cnf(g0_1,plain,
composition(meet(sk1,converse(sk2)),join(sk3,meet(sk2,sk3))) != composition(meet(sk1,converse(sk2)),sk3),
inference(rw,[status(thm)],[g0_0,t42]) ).
cnf(g0_2,plain,
composition(meet(sk1,converse(sk2)),join(sk3,meet(sk3,sk2))) != composition(meet(sk1,converse(sk2)),sk3),
inference(rw,[status(thm)],[g0_1,t117]) ).
cnf(g0_3,plain,
composition(meet(sk1,converse(sk2)),sk3) != composition(meet(sk1,converse(sk2)),sk3),
inference(rw,[status(thm)],[g0_2,t3953]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL024-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 07:19:24 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 18.54/2.91 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.54/2.91 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------