%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL019-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n003.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:47 PM UTC 2026
% Result : Unsatisfiable 14.13s 2.23s
% Output : CNFRefutation 14.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 22
% Syntax : Number of clauses : 233 ( 233 unt; 0 nHn; 142 RR)
% Number of literals : 233 ( 232 equ; 15 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 : 17 ( 17 usr; 12 con; 0-2 aty)
% Number of variables : 124 ( 9 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t17,axiom,
sF0 = composition(sk1,top),
introduced(definition) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t4614,plain,
sF0 = sk1,
inference(step,[status(thm)],[t17,t27]) ).
cnf(t30,plain,
sk1 = sF0,
inference(orient,[status(thm)],[t4614]) ).
cnf(t19,axiom,
sF2 = complement(sk1),
introduced(definition) ).
cnf(t24,plain,
complement(sk1) = sF2,
inference(orient,[status(thm)],[t19]) ).
cnf(t4615,plain,
complement(sF0) = sF2,
inference(step,[status(thm)],[t24,t30]) ).
cnf(t31,plain,
complement(sF0) = sF2,
inference(rw,[status(thm)],[t4615]) ).
cnf(t33,plain,
complement(sF0) = sF2,
inference(orient,[status(thm)],[t31]) ).
cnf(t18,axiom,
sF1 = composition(sk2,top),
introduced(definition) ).
cnf(t2,axiom,
composition(sk2,top) = sk2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
composition(sk2,top) = sk2,
inference(orient,[status(thm)],[t2]) ).
cnf(t4616,plain,
sF1 = sk2,
inference(step,[status(thm)],[t18,t28]) ).
cnf(t34,plain,
sk2 = sF1,
inference(orient,[status(thm)],[t4616]) ).
cnf(t20,axiom,
sF3 = complement(sk2),
introduced(definition) ).
cnf(t25,plain,
complement(sk2) = sF3,
inference(orient,[status(thm)],[t20]) ).
cnf(t4617,plain,
complement(sF1) = sF3,
inference(step,[status(thm)],[t25,t34]) ).
cnf(t35,plain,
complement(sF1) = sF3,
inference(rw,[status(thm)],[t4617]) ).
cnf(t37,plain,
complement(sF1) = sF3,
inference(orient,[status(thm)],[t35]) ).
cnf(t21,axiom,
sF4 = join(complement(sk1),complement(sk2)),
introduced(definition) ).
cnf(t4620,plain,
sF4 = join(complement(sF0),complement(sk2)),
inference(step,[status(thm)],[t21,t30]) ).
cnf(t4621,plain,
sF4 = join(sF2,complement(sk2)),
inference(step,[status(thm)],[t4620,t33]) ).
cnf(t4622,plain,
sF4 = join(sF2,complement(sF1)),
inference(step,[status(thm)],[t4621,t34]) ).
cnf(t4623,plain,
sF4 = join(sF2,sF3),
inference(step,[status(thm)],[t4622,t37]) ).
cnf(t62,plain,
join(sF2,sF3) = sF4,
inference(orient,[status(thm)],[t4623]) ).
cnf(t22,axiom,
sF5 = complement(join(complement(sk1),complement(sk2))),
introduced(definition) ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t69,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t4676,plain,
sF5 = complement(join(complement(sk2),complement(sk1))),
inference(step,[status(thm)],[t22,t69]) ).
cnf(t4677,plain,
sF5 = complement(join(complement(sF1),complement(sk1))),
inference(step,[status(thm)],[t4676,t34]) ).
cnf(t4678,plain,
sF5 = complement(join(sF3,complement(sk1))),
inference(step,[status(thm)],[t4677,t37]) ).
cnf(t4679,plain,
sF5 = complement(join(sF3,complement(sF0))),
inference(step,[status(thm)],[t4678,t30]) ).
cnf(t4680,plain,
sF5 = complement(join(sF3,sF2)),
inference(step,[status(thm)],[t4679,t33]) ).
cnf(t4681,plain,
sF5 = complement(join(sF2,sF3)),
inference(step,[status(thm)],[t4680,t69]) ).
cnf(t4682,plain,
sF5 = complement(sF4),
inference(step,[status(thm)],[t4681,t62]) ).
cnf(t492,plain,
complement(sF4) = sF5,
inference(orient,[status(thm)],[t4682]) ).
cnf(t23,axiom,
sF6 = composition(complement(join(complement(sk1),complement(sk2))),top),
introduced(definition) ).
cnf(t4690,plain,
sF6 = composition(complement(join(complement(sk2),complement(sk1))),top),
inference(step,[status(thm)],[t23,t69]) ).
cnf(t4691,plain,
sF6 = composition(complement(join(complement(sF1),complement(sk1))),top),
inference(step,[status(thm)],[t4690,t34]) ).
cnf(t4692,plain,
sF6 = composition(complement(join(sF3,complement(sk1))),top),
inference(step,[status(thm)],[t4691,t37]) ).
cnf(t4693,plain,
sF6 = composition(complement(join(sF3,complement(sF0))),top),
inference(step,[status(thm)],[t4692,t30]) ).
cnf(t4694,plain,
sF6 = composition(complement(join(sF3,sF2)),top),
inference(step,[status(thm)],[t4693,t33]) ).
cnf(t4695,plain,
sF6 = composition(complement(join(sF2,sF3)),top),
inference(step,[status(thm)],[t4694,t69]) ).
cnf(t4696,plain,
sF6 = composition(complement(sF4),top),
inference(step,[status(thm)],[t4695,t62]) ).
cnf(t4697,plain,
sF6 = composition(sF5,top),
inference(step,[status(thm)],[t4696,t492]) ).
cnf(t523,plain,
composition(sF5,top) = sF6,
inference(orient,[status(thm)],[t4697]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t4630,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t69]) ).
cnf(t172,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t4630]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t45,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t3,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t47,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t45,t29]) ).
cnf(t77,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t47]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t132,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t32,plain,
composition(sF0,top) = sk1,
inference(rw,[status(thm)],[t27]) ).
cnf(t4618,plain,
composition(sF0,top) = sF0,
inference(step,[status(thm)],[t32,t30]) ).
cnf(t41,plain,
composition(sF0,top) = sF0,
inference(orient,[status(thm)],[t4618]) ).
cnf(t177,plain,
complement(top) = join(complement(top),composition(converse(sF0),complement(sF0))),
inference(cp,[status(thm)],[t172,t41]) ).
cnf(u0,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t6,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t4,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t38,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t4626,plain,
complement(top) = zero,
inference(step,[status(thm)],[t6,t38]) ).
cnf(t97,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t4626]) ).
cnf(t4828,plain,
zero = join(complement(top),composition(converse(sF0),complement(sF0))),
inference(step,[status(thm)],[t177,t97]) ).
cnf(t4829,plain,
zero = join(zero,composition(converse(sF0),complement(sF0))),
inference(step,[status(thm)],[t4828,t97]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t56,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t78,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t77,t26]) ).
cnf(t4624,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t78,t29]) ).
cnf(t81,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t4624]) ).
cnf(t82,plain,
one = converse(one),
inference(cp,[status(thm)],[t81,t26]) ).
cnf(t83,plain,
converse(one) = one,
inference(orient,[status(thm)],[t82]) ).
cnf(t184,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t172,t83]) ).
cnf(t4625,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t81,t83]) ).
cnf(t84,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t4625]) ).
cnf(t88,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t84]) ).
cnf(t4644,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t184,t88]) ).
cnf(t4645,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t4644,t88]) ).
cnf(t335,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t4645]) ).
cnf(t338,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t335,t97]) ).
cnf(t4650,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t338,t97]) ).
cnf(t4651,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t4650,t97]) ).
cnf(t353,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t4651]) ).
cnf(t354,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t56,t353]) ).
cnf(t1045,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t354]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t4635,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t13,t69]) ).
cnf(t239,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t4635]) ).
cnf(t340,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t239,t335]) ).
cnf(t4758,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t340,t38]) ).
cnf(t4759,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t4758,t69]) ).
cnf(t4760,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t4759,t97]) ).
cnf(t983,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t4760]) ).
cnf(t1047,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t1045,t983]) ).
cnf(t4761,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t1047,t983]) ).
cnf(t1048,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t4761]) ).
cnf(t4830,plain,
zero = composition(converse(sF0),complement(sF0)),
inference(step,[status(thm)],[t4829,t1048]) ).
cnf(t4831,plain,
zero = composition(converse(sF0),sF2),
inference(step,[status(thm)],[t4830,t33]) ).
cnf(t2198,plain,
composition(converse(sF0),sF2) = zero,
inference(orient,[status(thm)],[t4831]) ).
cnf(t2200,plain,
composition(converse(sF2),sF0) = converse(zero),
inference(cp,[status(thm)],[t77,t2198]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t48,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t50,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t48,t29]) ).
cnf(t119,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t50]) ).
cnf(t1060,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t119,t1048]) ).
cnf(t4785,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t1060,t29]) ).
cnf(t1368,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t4785]) ).
cnf(t1057,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t1048,t69]) ).
cnf(t1183,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t1057]) ).
cnf(t1371,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t1368,t1183]) ).
cnf(t1376,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t1371]) ).
cnf(t4832,plain,
composition(converse(sF2),sF0) = zero,
inference(step,[status(thm)],[t2200,t1376]) ).
cnf(t2209,plain,
composition(converse(sF2),sF0) = zero,
inference(orient,[status(thm)],[t4832]) ).
cnf(t2213,plain,
complement(sF0) = join(complement(sF0),composition(converse(converse(sF2)),complement(zero))),
inference(cp,[status(thm)],[t172,t2209]) ).
cnf(t4833,plain,
sF2 = join(complement(sF0),composition(converse(converse(sF2)),complement(zero))),
inference(step,[status(thm)],[t2213,t33]) ).
cnf(t4834,plain,
sF2 = join(sF2,composition(converse(converse(sF2)),complement(zero))),
inference(step,[status(thm)],[t4833,t33]) ).
cnf(t4835,plain,
sF2 = join(sF2,composition(sF2,complement(zero))),
inference(step,[status(thm)],[t4834,t29]) ).
cnf(t1056,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t1048,t38]) ).
cnf(t1162,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t1056]) ).
cnf(t4836,plain,
sF2 = join(sF2,composition(sF2,top)),
inference(step,[status(thm)],[t4835,t1162]) ).
cnf(t2217,plain,
join(sF2,composition(sF2,top)) = sF2,
inference(orient,[status(thm)],[t4836]) ).
cnf(t49,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t48,t29]) ).
cnf(t111,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t49]) ).
cnf(t142,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t132,t88]) ).
cnf(t3397,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t142]) ).
cnf(t57,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t56,t38]) ).
cnf(t610,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t57]) ).
cnf(t632,plain,
top = join(complement(X1),join(complement(X1),complement(complement(X1)))),
inference(cp,[status(thm)],[t610,t335]) ).
cnf(t4726,plain,
top = join(complement(X1),top),
inference(step,[status(thm)],[t632,t38]) ).
cnf(t4727,plain,
top = join(top,complement(X1)),
inference(step,[status(thm)],[t4726,t69]) ).
cnf(t684,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t4727]) ).
cnf(t695,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t610,t684]) ).
cnf(t716,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t695]) ).
cnf(t3405,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t3397,t716]) ).
cnf(t3455,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t3405]) ).
cnf(t3465,plain,
join(X1,converse(composition(top,converse(X1)))) = converse(composition(top,converse(X1))),
inference(cp,[status(thm)],[t111,t3455]) ).
cnf(t46,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t45,t29]) ).
cnf(t64,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t46]) ).
cnf(t4914,plain,
join(X1,composition(X1,converse(top))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t3465,t64]) ).
cnf(t731,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t111,t716]) ).
cnf(t776,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t731]) ).
cnf(t39,plain,
top = join(sF0,sF2),
inference(cp,[status(thm)],[t38,t33]) ).
cnf(t43,plain,
join(sF0,sF2) = top,
inference(orient,[status(thm)],[t39]) ).
cnf(t59,plain,
join(sF0,join(sF2,X1)) = join(top,X1),
inference(cp,[status(thm)],[t56,t43]) ).
cnf(t127,plain,
join(sF0,join(sF2,X1)) = join(top,X1),
inference(orient,[status(thm)],[t59]) ).
cnf(t131,plain,
join(top,X1) = join(sF0,join(X1,sF2)),
inference(cp,[status(thm)],[t127,t69]) ).
cnf(t208,plain,
join(sF0,join(X1,sF2)) = join(top,X1),
inference(orient,[status(thm)],[t131]) ).
cnf(t210,plain,
join(top,X1) = join(join(X1,sF2),sF0),
inference(cp,[status(thm)],[t208,t69]) ).
cnf(t4685,plain,
join(top,X1) = join(X1,join(sF2,sF0)),
inference(step,[status(thm)],[t210,t56]) ).
cnf(t4686,plain,
join(top,X1) = join(X1,join(sF0,sF2)),
inference(step,[status(thm)],[t4685,t69]) ).
cnf(t4687,plain,
join(top,X1) = join(X1,top),
inference(step,[status(thm)],[t4686,t43]) ).
cnf(t510,plain,
join(top,X1) = join(X1,top),
inference(orient,[status(thm)],[t4687]) ).
cnf(t4737,plain,
join(top,X1) = top,
inference(step,[status(thm)],[t510,t716]) ).
cnf(t723,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t4737]) ).
cnf(t779,plain,
converse(top) = top,
inference(cp,[status(thm)],[t776,t723]) ).
cnf(t784,plain,
converse(top) = top,
inference(orient,[status(thm)],[t779]) ).
cnf(t4915,plain,
join(X1,composition(X1,top)) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t4914,t784]) ).
cnf(t4916,plain,
join(X1,composition(X1,top)) = composition(X1,converse(top)),
inference(step,[status(thm)],[t4915,t64]) ).
cnf(t4917,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t4916,t784]) ).
cnf(t3681,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t4917]) ).
cnf(t4918,plain,
composition(sF2,top) = sF2,
inference(step,[status(thm)],[t2217,t3681]) ).
cnf(t3682,plain,
composition(sF2,top) = sF2,
inference(rw,[status(thm)],[t4918]) ).
cnf(t3713,plain,
composition(sF2,top) = sF2,
inference(orient,[status(thm)],[t3682]) ).
cnf(t3716,plain,
composition(join(sF2,X1),top) = join(sF2,composition(X1,top)),
inference(cp,[status(thm)],[t132,t3713]) ).
cnf(t4409,plain,
composition(join(sF2,X1),top) = join(sF2,composition(X1,top)),
inference(orient,[status(thm)],[t3716]) ).
cnf(t4411,plain,
join(sF2,composition(sF3,top)) = composition(sF4,top),
inference(cp,[status(thm)],[t4409,t62]) ).
cnf(t36,plain,
composition(sF1,top) = sk2,
inference(rw,[status(thm)],[t28]) ).
cnf(t4619,plain,
composition(sF1,top) = sF1,
inference(step,[status(thm)],[t36,t34]) ).
cnf(t42,plain,
composition(sF1,top) = sF1,
inference(orient,[status(thm)],[t4619]) ).
cnf(t178,plain,
complement(top) = join(complement(top),composition(converse(sF1),complement(sF1))),
inference(cp,[status(thm)],[t172,t42]) ).
cnf(t4837,plain,
zero = join(complement(top),composition(converse(sF1),complement(sF1))),
inference(step,[status(thm)],[t178,t97]) ).
cnf(t4838,plain,
zero = join(zero,composition(converse(sF1),complement(sF1))),
inference(step,[status(thm)],[t4837,t97]) ).
cnf(t4839,plain,
zero = composition(converse(sF1),complement(sF1)),
inference(step,[status(thm)],[t4838,t1048]) ).
cnf(t4840,plain,
zero = composition(converse(sF1),sF3),
inference(step,[status(thm)],[t4839,t37]) ).
cnf(t2274,plain,
composition(converse(sF1),sF3) = zero,
inference(orient,[status(thm)],[t4840]) ).
cnf(t2276,plain,
composition(converse(sF3),sF1) = converse(zero),
inference(cp,[status(thm)],[t77,t2274]) ).
cnf(t4841,plain,
composition(converse(sF3),sF1) = zero,
inference(step,[status(thm)],[t2276,t1376]) ).
cnf(t2285,plain,
composition(converse(sF3),sF1) = zero,
inference(orient,[status(thm)],[t4841]) ).
cnf(t2289,plain,
complement(sF1) = join(complement(sF1),composition(converse(converse(sF3)),complement(zero))),
inference(cp,[status(thm)],[t172,t2285]) ).
cnf(t4842,plain,
sF3 = join(complement(sF1),composition(converse(converse(sF3)),complement(zero))),
inference(step,[status(thm)],[t2289,t37]) ).
cnf(t4843,plain,
sF3 = join(sF3,composition(converse(converse(sF3)),complement(zero))),
inference(step,[status(thm)],[t4842,t37]) ).
cnf(t4844,plain,
sF3 = join(sF3,composition(sF3,complement(zero))),
inference(step,[status(thm)],[t4843,t29]) ).
cnf(t4845,plain,
sF3 = join(sF3,composition(sF3,top)),
inference(step,[status(thm)],[t4844,t1162]) ).
cnf(t2293,plain,
join(sF3,composition(sF3,top)) = sF3,
inference(orient,[status(thm)],[t4845]) ).
cnf(t4919,plain,
composition(sF3,top) = sF3,
inference(step,[status(thm)],[t2293,t3681]) ).
cnf(t3683,plain,
composition(sF3,top) = sF3,
inference(rw,[status(thm)],[t4919]) ).
cnf(t3731,plain,
composition(sF3,top) = sF3,
inference(orient,[status(thm)],[t3683]) ).
cnf(t4947,plain,
join(sF2,sF3) = composition(sF4,top),
inference(step,[status(thm)],[t4411,t3731]) ).
cnf(t4948,plain,
sF4 = composition(sF4,top),
inference(step,[status(thm)],[t4947,t62]) ).
cnf(t4449,plain,
composition(sF4,top) = sF4,
inference(orient,[status(thm)],[t4948]) ).
cnf(t4458,plain,
complement(top) = join(complement(top),composition(converse(sF4),complement(sF4))),
inference(cp,[status(thm)],[t172,t4449]) ).
cnf(t4951,plain,
zero = join(complement(top),composition(converse(sF4),complement(sF4))),
inference(step,[status(thm)],[t4458,t97]) ).
cnf(t4952,plain,
zero = join(zero,composition(converse(sF4),complement(sF4))),
inference(step,[status(thm)],[t4951,t97]) ).
cnf(t4953,plain,
zero = composition(converse(sF4),complement(sF4)),
inference(step,[status(thm)],[t4952,t1048]) ).
cnf(t4954,plain,
zero = composition(converse(sF4),sF5),
inference(step,[status(thm)],[t4953,t492]) ).
cnf(t4513,plain,
composition(converse(sF4),sF5) = zero,
inference(orient,[status(thm)],[t4954]) ).
cnf(t4515,plain,
composition(converse(sF5),sF4) = converse(zero),
inference(cp,[status(thm)],[t77,t4513]) ).
cnf(t4955,plain,
composition(converse(sF5),sF4) = zero,
inference(step,[status(thm)],[t4515,t1376]) ).
cnf(t4550,plain,
composition(converse(sF5),sF4) = zero,
inference(orient,[status(thm)],[t4955]) ).
cnf(t4552,plain,
complement(sF4) = join(complement(sF4),composition(converse(converse(sF5)),complement(zero))),
inference(cp,[status(thm)],[t172,t4550]) ).
cnf(t4956,plain,
sF5 = join(complement(sF4),composition(converse(converse(sF5)),complement(zero))),
inference(step,[status(thm)],[t4552,t492]) ).
cnf(t4957,plain,
sF5 = join(sF5,composition(converse(converse(sF5)),complement(zero))),
inference(step,[status(thm)],[t4956,t492]) ).
cnf(t4958,plain,
sF5 = join(sF5,composition(sF5,complement(zero))),
inference(step,[status(thm)],[t4957,t29]) ).
cnf(t4959,plain,
sF5 = join(sF5,composition(sF5,top)),
inference(step,[status(thm)],[t4958,t1162]) ).
cnf(t4960,plain,
sF5 = composition(sF5,top),
inference(step,[status(thm)],[t4959,t3681]) ).
cnf(t4961,plain,
sF5 = sF6,
inference(step,[status(thm)],[t4960,t523]) ).
cnf(t4562,plain,
sF6 = sF5,
inference(orient,[status(thm)],[t4961]) ).
cnf(t4962,plain,
composition(sF5,top) = sF5,
inference(step,[status(thm)],[t523,t4562]) ).
cnf(t4563,plain,
composition(sF5,top) = sF5,
inference(orient,[status(thm)],[t4962]) ).
cnf(u4,negated_conjecture,
composition(meet(sk1,sk2),top) != meet(sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
composition(complement(join(complement(sk1),complement(sk2))),top) != complement(join(complement(sk1),complement(sk2))),
inference(definition_unfolding,[status(thm)],[u4,d0]) ).
cnf(g0_0,plain,
composition(complement(join(complement(sF0),complement(sk2))),top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[goal_0,t30]) ).
cnf(g0_1,plain,
composition(complement(join(sF2,complement(sk2))),top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_0,t33]) ).
cnf(g0_2,plain,
composition(complement(join(sF2,complement(sF1))),top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_1,t34]) ).
cnf(g0_3,plain,
composition(complement(join(sF2,sF3)),top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_2,t37]) ).
cnf(g0_4,plain,
composition(complement(sF4),top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_3,t62]) ).
cnf(g0_5,plain,
composition(sF5,top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_4,t492]) ).
cnf(g0_6,plain,
sF5 != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_5,t4563]) ).
cnf(g0_7,plain,
sF5 != complement(join(complement(sF0),complement(sk2))),
inference(rw,[status(thm)],[g0_6,t30]) ).
cnf(g0_8,plain,
sF5 != complement(join(sF2,complement(sk2))),
inference(rw,[status(thm)],[g0_7,t33]) ).
cnf(g0_9,plain,
sF5 != complement(join(sF2,complement(sF1))),
inference(rw,[status(thm)],[g0_8,t34]) ).
cnf(g0_10,plain,
sF5 != complement(join(sF2,sF3)),
inference(rw,[status(thm)],[g0_9,t37]) ).
cnf(g0_11,plain,
sF5 != complement(sF4),
inference(rw,[status(thm)],[g0_10,t62]) ).
cnf(g0_12,plain,
sF5 != sF5,
inference(rw,[status(thm)],[g0_11,t492]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL019-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n003.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:18:05 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 14.13/2.23 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.13/2.23 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------