%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL019-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 : n013.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 19.37s 7.97s
% Output : CNFRefutation 19.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 22
% Syntax : Number of clauses : 231 ( 231 unt; 0 nHn; 143 RR)
% Number of literals : 231 ( 230 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 : 121 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t14,axiom,
sF0 = composition(sk1,top),
introduced(definition) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t4290,plain,
sF0 = sk1,
inference(step,[status(thm)],[t14,t24]) ).
cnf(t27,plain,
sk1 = sF0,
inference(orient,[status(thm)],[t4290]) ).
cnf(t16,axiom,
sF2 = complement(sk1),
introduced(definition) ).
cnf(t21,plain,
complement(sk1) = sF2,
inference(orient,[status(thm)],[t16]) ).
cnf(t4291,plain,
complement(sF0) = sF2,
inference(step,[status(thm)],[t21,t27]) ).
cnf(t28,plain,
complement(sF0) = sF2,
inference(rw,[status(thm)],[t4291]) ).
cnf(t30,plain,
complement(sF0) = sF2,
inference(orient,[status(thm)],[t28]) ).
cnf(t15,axiom,
sF1 = composition(sk2,top),
introduced(definition) ).
cnf(t2,axiom,
composition(sk2,top) = sk2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
composition(sk2,top) = sk2,
inference(orient,[status(thm)],[t2]) ).
cnf(t4292,plain,
sF1 = sk2,
inference(step,[status(thm)],[t15,t25]) ).
cnf(t31,plain,
sk2 = sF1,
inference(orient,[status(thm)],[t4292]) ).
cnf(t17,axiom,
sF3 = complement(sk2),
introduced(definition) ).
cnf(t22,plain,
complement(sk2) = sF3,
inference(orient,[status(thm)],[t17]) ).
cnf(t4293,plain,
complement(sF1) = sF3,
inference(step,[status(thm)],[t22,t31]) ).
cnf(t32,plain,
complement(sF1) = sF3,
inference(rw,[status(thm)],[t4293]) ).
cnf(t34,plain,
complement(sF1) = sF3,
inference(orient,[status(thm)],[t32]) ).
cnf(t18,axiom,
sF4 = join(complement(sk1),complement(sk2)),
introduced(definition) ).
cnf(t4296,plain,
sF4 = join(complement(sF0),complement(sk2)),
inference(step,[status(thm)],[t18,t27]) ).
cnf(t4297,plain,
sF4 = join(sF2,complement(sk2)),
inference(step,[status(thm)],[t4296,t30]) ).
cnf(t4298,plain,
sF4 = join(sF2,complement(sF1)),
inference(step,[status(thm)],[t4297,t31]) ).
cnf(t4299,plain,
sF4 = join(sF2,sF3),
inference(step,[status(thm)],[t4298,t34]) ).
cnf(t59,plain,
join(sF2,sF3) = sF4,
inference(orient,[status(thm)],[t4299]) ).
cnf(t19,axiom,
sF5 = complement(join(complement(sk1),complement(sk2))),
introduced(definition) ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t66,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t4318,plain,
sF5 = complement(join(complement(sk2),complement(sk1))),
inference(step,[status(thm)],[t19,t66]) ).
cnf(t4319,plain,
sF5 = complement(join(complement(sF1),complement(sk1))),
inference(step,[status(thm)],[t4318,t31]) ).
cnf(t4320,plain,
sF5 = complement(join(sF3,complement(sk1))),
inference(step,[status(thm)],[t4319,t34]) ).
cnf(t4321,plain,
sF5 = complement(join(sF3,complement(sF0))),
inference(step,[status(thm)],[t4320,t27]) ).
cnf(t4322,plain,
sF5 = complement(join(sF3,sF2)),
inference(step,[status(thm)],[t4321,t30]) ).
cnf(t4323,plain,
sF5 = complement(join(sF2,sF3)),
inference(step,[status(thm)],[t4322,t66]) ).
cnf(t4324,plain,
sF5 = complement(sF4),
inference(step,[status(thm)],[t4323,t59]) ).
cnf(t296,plain,
complement(sF4) = sF5,
inference(orient,[status(thm)],[t4324]) ).
cnf(t20,axiom,
sF6 = composition(complement(join(complement(sk1),complement(sk2))),top),
introduced(definition) ).
cnf(t4351,plain,
sF6 = composition(complement(join(complement(sk2),complement(sk1))),top),
inference(step,[status(thm)],[t20,t66]) ).
cnf(t4352,plain,
sF6 = composition(complement(join(complement(sF1),complement(sk1))),top),
inference(step,[status(thm)],[t4351,t31]) ).
cnf(t4353,plain,
sF6 = composition(complement(join(sF3,complement(sk1))),top),
inference(step,[status(thm)],[t4352,t34]) ).
cnf(t4354,plain,
sF6 = composition(complement(join(sF3,complement(sF0))),top),
inference(step,[status(thm)],[t4353,t27]) ).
cnf(t4355,plain,
sF6 = composition(complement(join(sF3,sF2)),top),
inference(step,[status(thm)],[t4354,t30]) ).
cnf(t4356,plain,
sF6 = composition(complement(join(sF2,sF3)),top),
inference(step,[status(thm)],[t4355,t66]) ).
cnf(t4357,plain,
sF6 = composition(complement(sF4),top),
inference(step,[status(thm)],[t4356,t59]) ).
cnf(t4358,plain,
sF6 = composition(sF5,top),
inference(step,[status(thm)],[t4357,t296]) ).
cnf(t345,plain,
composition(sF5,top) = sF6,
inference(orient,[status(thm)],[t4358]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4306,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t66]) ).
cnf(t169,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t4306]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t42,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t44,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t42,t26]) ).
cnf(t74,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t44]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t129,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t29,plain,
composition(sF0,top) = sk1,
inference(rw,[status(thm)],[t24]) ).
cnf(t4294,plain,
composition(sF0,top) = sF0,
inference(step,[status(thm)],[t29,t27]) ).
cnf(t38,plain,
composition(sF0,top) = sF0,
inference(orient,[status(thm)],[t4294]) ).
cnf(t174,plain,
complement(top) = join(complement(top),composition(converse(sF0),complement(sF0))),
inference(cp,[status(thm)],[t169,t38]) ).
cnf(u0,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t35,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t4302,plain,
complement(top) = zero,
inference(step,[status(thm)],[t6,t35]) ).
cnf(t94,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t4302]) ).
cnf(t4478,plain,
zero = join(complement(top),composition(converse(sF0),complement(sF0))),
inference(step,[status(thm)],[t174,t94]) ).
cnf(t4479,plain,
zero = join(zero,composition(converse(sF0),complement(sF0))),
inference(step,[status(thm)],[t4478,t94]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t53,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t75,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t74,t23]) ).
cnf(t4300,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t75,t26]) ).
cnf(t78,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t4300]) ).
cnf(t79,plain,
one = converse(one),
inference(cp,[status(thm)],[t78,t23]) ).
cnf(t80,plain,
converse(one) = one,
inference(orient,[status(thm)],[t79]) ).
cnf(t181,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t169,t80]) ).
cnf(t4301,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t78,t80]) ).
cnf(t81,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t4301]) ).
cnf(t85,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t81]) ).
cnf(t4325,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t181,t85]) ).
cnf(t4326,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t4325,t85]) ).
cnf(t304,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t4326]) ).
cnf(t307,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t304,t94]) ).
cnf(t4331,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t307,t94]) ).
cnf(t4332,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t4331,t94]) ).
cnf(t321,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t4332]) ).
cnf(t322,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t53,t321]) ).
cnf(t876,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t322]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4311,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t13,t66]) ).
cnf(t236,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t4311]) ).
cnf(t310,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t236,t304]) ).
cnf(t4419,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t310,t35]) ).
cnf(t4420,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t4419,t66]) ).
cnf(t4421,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t4420,t94]) ).
cnf(t748,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t4421]) ).
cnf(t878,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t876,t748]) ).
cnf(t4423,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t878,t748]) ).
cnf(t882,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t4423]) ).
cnf(t4480,plain,
zero = composition(converse(sF0),complement(sF0)),
inference(step,[status(thm)],[t4479,t882]) ).
cnf(t4481,plain,
zero = composition(converse(sF0),sF2),
inference(step,[status(thm)],[t4480,t30]) ).
cnf(t1610,plain,
composition(converse(sF0),sF2) = zero,
inference(orient,[status(thm)],[t4481]) ).
cnf(t1612,plain,
composition(converse(sF2),sF0) = converse(zero),
inference(cp,[status(thm)],[t74,t1610]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t45,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t47,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t45,t26]) ).
cnf(t116,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t47]) ).
cnf(t894,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t116,t882]) ).
cnf(t4446,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t894,t26]) ).
cnf(t1058,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t4446]) ).
cnf(t890,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t882,t66]) ).
cnf(t969,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t890]) ).
cnf(t1062,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t1058,t969]) ).
cnf(t1066,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t1062]) ).
cnf(t4482,plain,
composition(converse(sF2),sF0) = zero,
inference(step,[status(thm)],[t1612,t1066]) ).
cnf(t1619,plain,
composition(converse(sF2),sF0) = zero,
inference(orient,[status(thm)],[t4482]) ).
cnf(t1623,plain,
complement(sF0) = join(complement(sF0),composition(converse(converse(sF2)),complement(zero))),
inference(cp,[status(thm)],[t169,t1619]) ).
cnf(t4483,plain,
sF2 = join(complement(sF0),composition(converse(converse(sF2)),complement(zero))),
inference(step,[status(thm)],[t1623,t30]) ).
cnf(t4484,plain,
sF2 = join(sF2,composition(converse(converse(sF2)),complement(zero))),
inference(step,[status(thm)],[t4483,t30]) ).
cnf(t4485,plain,
sF2 = join(sF2,composition(sF2,complement(zero))),
inference(step,[status(thm)],[t4484,t26]) ).
cnf(t889,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t882,t35]) ).
cnf(t921,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t889]) ).
cnf(t4486,plain,
sF2 = join(sF2,composition(sF2,top)),
inference(step,[status(thm)],[t4485,t921]) ).
cnf(t1625,plain,
join(sF2,composition(sF2,top)) = sF2,
inference(orient,[status(thm)],[t4486]) ).
cnf(t46,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t45,t26]) ).
cnf(t108,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t46]) ).
cnf(t139,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t129,t85]) ).
cnf(t3235,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t139]) ).
cnf(t54,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t53,t35]) ).
cnf(t394,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t54]) ).
cnf(t417,plain,
top = join(complement(X1),join(complement(X1),complement(complement(X1)))),
inference(cp,[status(thm)],[t394,t304]) ).
cnf(t4366,plain,
top = join(complement(X1),top),
inference(step,[status(thm)],[t417,t35]) ).
cnf(t4367,plain,
top = join(top,complement(X1)),
inference(step,[status(thm)],[t4366,t66]) ).
cnf(t440,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t4367]) ).
cnf(t450,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t394,t440]) ).
cnf(t478,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t450]) ).
cnf(t3241,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t3235,t478]) ).
cnf(t3284,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t3241]) ).
cnf(t3297,plain,
join(X1,converse(composition(top,converse(X1)))) = converse(composition(top,converse(X1))),
inference(cp,[status(thm)],[t108,t3284]) ).
cnf(t43,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t42,t26]) ).
cnf(t61,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t43]) ).
cnf(t4607,plain,
join(X1,composition(X1,converse(top))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t3297,t61]) ).
cnf(t490,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t108,t478]) ).
cnf(t538,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t490]) ).
cnf(t95,plain,
top = join(top,zero),
inference(cp,[status(thm)],[t35,t94]) ).
cnf(t4303,plain,
top = join(zero,top),
inference(step,[status(thm)],[t95,t66]) ).
cnf(t96,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t4303]) ).
cnf(t98,plain,
join(zero,join(top,X1)) = join(top,X1),
inference(cp,[status(thm)],[t53,t96]) ).
cnf(t193,plain,
join(zero,join(top,X1)) = join(top,X1),
inference(orient,[status(thm)],[t98]) ).
cnf(t195,plain,
join(top,X1) = join(zero,join(X1,top)),
inference(cp,[status(thm)],[t193,t66]) ).
cnf(t382,plain,
join(zero,join(X1,top)) = join(top,X1),
inference(orient,[status(thm)],[t195]) ).
cnf(t4377,plain,
join(zero,top) = join(top,X1),
inference(step,[status(thm)],[t382,t478]) ).
cnf(t4378,plain,
top = join(top,X1),
inference(step,[status(thm)],[t4377,t478]) ).
cnf(t484,plain,
top = join(top,X1),
inference(rw,[status(thm)],[t4378]) ).
cnf(t510,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t484]) ).
cnf(t540,plain,
converse(top) = top,
inference(cp,[status(thm)],[t538,t510]) ).
cnf(t563,plain,
converse(top) = top,
inference(orient,[status(thm)],[t540]) ).
cnf(t4608,plain,
join(X1,composition(X1,top)) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t4607,t563]) ).
cnf(t4609,plain,
join(X1,composition(X1,top)) = composition(X1,converse(top)),
inference(step,[status(thm)],[t4608,t61]) ).
cnf(t4610,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t4609,t563]) ).
cnf(t3449,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t4610]) ).
cnf(t4611,plain,
composition(sF2,top) = sF2,
inference(step,[status(thm)],[t1625,t3449]) ).
cnf(t3450,plain,
composition(sF2,top) = sF2,
inference(rw,[status(thm)],[t4611]) ).
cnf(t3482,plain,
composition(sF2,top) = sF2,
inference(orient,[status(thm)],[t3450]) ).
cnf(t3485,plain,
composition(join(sF2,X1),top) = join(sF2,composition(X1,top)),
inference(cp,[status(thm)],[t129,t3482]) ).
cnf(t4095,plain,
composition(join(sF2,X1),top) = join(sF2,composition(X1,top)),
inference(orient,[status(thm)],[t3485]) ).
cnf(t4097,plain,
join(sF2,composition(sF3,top)) = composition(sF4,top),
inference(cp,[status(thm)],[t4095,t59]) ).
cnf(t33,plain,
composition(sF1,top) = sk2,
inference(rw,[status(thm)],[t25]) ).
cnf(t4295,plain,
composition(sF1,top) = sF1,
inference(step,[status(thm)],[t33,t31]) ).
cnf(t39,plain,
composition(sF1,top) = sF1,
inference(orient,[status(thm)],[t4295]) ).
cnf(t175,plain,
complement(top) = join(complement(top),composition(converse(sF1),complement(sF1))),
inference(cp,[status(thm)],[t169,t39]) ).
cnf(t4487,plain,
zero = join(complement(top),composition(converse(sF1),complement(sF1))),
inference(step,[status(thm)],[t175,t94]) ).
cnf(t4488,plain,
zero = join(zero,composition(converse(sF1),complement(sF1))),
inference(step,[status(thm)],[t4487,t94]) ).
cnf(t4489,plain,
zero = composition(converse(sF1),complement(sF1)),
inference(step,[status(thm)],[t4488,t882]) ).
cnf(t4490,plain,
zero = composition(converse(sF1),sF3),
inference(step,[status(thm)],[t4489,t34]) ).
cnf(t1633,plain,
composition(converse(sF1),sF3) = zero,
inference(orient,[status(thm)],[t4490]) ).
cnf(t1635,plain,
composition(converse(sF3),sF1) = converse(zero),
inference(cp,[status(thm)],[t74,t1633]) ).
cnf(t4491,plain,
composition(converse(sF3),sF1) = zero,
inference(step,[status(thm)],[t1635,t1066]) ).
cnf(t1642,plain,
composition(converse(sF3),sF1) = zero,
inference(orient,[status(thm)],[t4491]) ).
cnf(t1646,plain,
complement(sF1) = join(complement(sF1),composition(converse(converse(sF3)),complement(zero))),
inference(cp,[status(thm)],[t169,t1642]) ).
cnf(t4492,plain,
sF3 = join(complement(sF1),composition(converse(converse(sF3)),complement(zero))),
inference(step,[status(thm)],[t1646,t34]) ).
cnf(t4493,plain,
sF3 = join(sF3,composition(converse(converse(sF3)),complement(zero))),
inference(step,[status(thm)],[t4492,t34]) ).
cnf(t4494,plain,
sF3 = join(sF3,composition(sF3,complement(zero))),
inference(step,[status(thm)],[t4493,t26]) ).
cnf(t4495,plain,
sF3 = join(sF3,composition(sF3,top)),
inference(step,[status(thm)],[t4494,t921]) ).
cnf(t1648,plain,
join(sF3,composition(sF3,top)) = sF3,
inference(orient,[status(thm)],[t4495]) ).
cnf(t4612,plain,
composition(sF3,top) = sF3,
inference(step,[status(thm)],[t1648,t3449]) ).
cnf(t3451,plain,
composition(sF3,top) = sF3,
inference(rw,[status(thm)],[t4612]) ).
cnf(t3497,plain,
composition(sF3,top) = sF3,
inference(orient,[status(thm)],[t3451]) ).
cnf(t4643,plain,
join(sF2,sF3) = composition(sF4,top),
inference(step,[status(thm)],[t4097,t3497]) ).
cnf(t4644,plain,
sF4 = composition(sF4,top),
inference(step,[status(thm)],[t4643,t59]) ).
cnf(t4128,plain,
composition(sF4,top) = sF4,
inference(orient,[status(thm)],[t4644]) ).
cnf(t4137,plain,
complement(top) = join(complement(top),composition(converse(sF4),complement(sF4))),
inference(cp,[status(thm)],[t169,t4128]) ).
cnf(t4646,plain,
zero = join(complement(top),composition(converse(sF4),complement(sF4))),
inference(step,[status(thm)],[t4137,t94]) ).
cnf(t4647,plain,
zero = join(zero,composition(converse(sF4),complement(sF4))),
inference(step,[status(thm)],[t4646,t94]) ).
cnf(t4648,plain,
zero = composition(converse(sF4),complement(sF4)),
inference(step,[status(thm)],[t4647,t882]) ).
cnf(t4649,plain,
zero = composition(converse(sF4),sF5),
inference(step,[status(thm)],[t4648,t296]) ).
cnf(t4191,plain,
composition(converse(sF4),sF5) = zero,
inference(orient,[status(thm)],[t4649]) ).
cnf(t4193,plain,
composition(converse(sF5),sF4) = converse(zero),
inference(cp,[status(thm)],[t74,t4191]) ).
cnf(t4650,plain,
composition(converse(sF5),sF4) = zero,
inference(step,[status(thm)],[t4193,t1066]) ).
cnf(t4224,plain,
composition(converse(sF5),sF4) = zero,
inference(orient,[status(thm)],[t4650]) ).
cnf(t4226,plain,
complement(sF4) = join(complement(sF4),composition(converse(converse(sF5)),complement(zero))),
inference(cp,[status(thm)],[t169,t4224]) ).
cnf(t4651,plain,
sF5 = join(complement(sF4),composition(converse(converse(sF5)),complement(zero))),
inference(step,[status(thm)],[t4226,t296]) ).
cnf(t4652,plain,
sF5 = join(sF5,composition(converse(converse(sF5)),complement(zero))),
inference(step,[status(thm)],[t4651,t296]) ).
cnf(t4653,plain,
sF5 = join(sF5,composition(sF5,complement(zero))),
inference(step,[status(thm)],[t4652,t26]) ).
cnf(t4654,plain,
sF5 = join(sF5,composition(sF5,top)),
inference(step,[status(thm)],[t4653,t921]) ).
cnf(t4655,plain,
sF5 = composition(sF5,top),
inference(step,[status(thm)],[t4654,t3449]) ).
cnf(t4656,plain,
sF5 = sF6,
inference(step,[status(thm)],[t4655,t345]) ).
cnf(t4234,plain,
sF6 = sF5,
inference(orient,[status(thm)],[t4656]) ).
cnf(t4657,plain,
composition(sF5,top) = sF5,
inference(step,[status(thm)],[t345,t4234]) ).
cnf(t4235,plain,
composition(sF5,top) = sF5,
inference(orient,[status(thm)],[t4657]) ).
cnf(u1,negated_conjecture,
composition(meet(sk1,sk2),top) != meet(sk1,sk2),
file('/export/starexec/sandbox2/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)],[u1,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,t27]) ).
cnf(g0_1,plain,
composition(complement(join(sF2,complement(sk2))),top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_0,t30]) ).
cnf(g0_2,plain,
composition(complement(join(sF2,complement(sF1))),top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_1,t31]) ).
cnf(g0_3,plain,
composition(complement(join(sF2,sF3)),top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_2,t34]) ).
cnf(g0_4,plain,
composition(complement(sF4),top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_3,t59]) ).
cnf(g0_5,plain,
composition(sF5,top) != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_4,t296]) ).
cnf(g0_6,plain,
sF5 != complement(join(complement(sk1),complement(sk2))),
inference(rw,[status(thm)],[g0_5,t4235]) ).
cnf(g0_7,plain,
sF5 != complement(join(complement(sF0),complement(sk2))),
inference(rw,[status(thm)],[g0_6,t27]) ).
cnf(g0_8,plain,
sF5 != complement(join(sF2,complement(sk2))),
inference(rw,[status(thm)],[g0_7,t30]) ).
cnf(g0_9,plain,
sF5 != complement(join(sF2,complement(sF1))),
inference(rw,[status(thm)],[g0_8,t31]) ).
cnf(g0_10,plain,
sF5 != complement(join(sF2,sF3)),
inference(rw,[status(thm)],[g0_9,t34]) ).
cnf(g0_11,plain,
sF5 != complement(sF4),
inference(rw,[status(thm)],[g0_10,t59]) ).
cnf(g0_12,plain,
sF5 != sF5,
inference(rw,[status(thm)],[g0_11,t296]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL019-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.18/5.46 % Computer : n013.cluster.edu
% 0.18/5.46 % Model : x86_64 x86_64
% 0.18/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.46 % Memory : 8046.5625MB
% 0.18/5.46 % OS : Linux 6.8.0-71-generic
% 0.18/5.46 % CPULimit : 300
% 0.18/5.46 % WCLimit : 300
% 0.18/5.46 % DateTime : Thu Sep 24 07:15:41 UTC 2026
% 0.18/5.46 % CPUTime :
% 0.18/5.46 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 19.37/7.97 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.37/7.97 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------