%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT005-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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 01:54:58 PM UTC 2026
% Result : Unsatisfiable 19.52s 3.00s
% Output : CNFRefutation 19.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 21
% Syntax : Number of clauses : 199 ( 199 unt; 0 nHn; 110 RR)
% Number of literals : 199 ( 198 equ; 11 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 : 16 ( 16 usr; 11 con; 0-4 aty)
% Number of variables : 141 ( 27 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t20,axiom,
ifeq3(meet(X1,X2),X1,meet(X2,join(X1,X3)),join(X1,meet(X3,X2))) = join(X1,meet(X3,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t63,plain,
ifeq3(meet(X1,X2),X1,meet(X2,join(X1,X3)),join(X1,meet(X3,X2))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t20]) ).
cnf(t13,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t13]) ).
cnf(t71,plain,
join(X1,meet(X2,X3)) = ifeq3(meet(X3,X1),X1,meet(X3,join(X1,X2)),join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t63,t35]) ).
cnf(t10737,plain,
ifeq3(meet(X1,X2),X2,meet(X1,join(X2,X3)),join(X2,meet(X3,X1))) = join(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t71]) ).
cnf(t14,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t11,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t60,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t62,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t27,t60]) ).
cnf(t266,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t62]) ).
cnf(t22,axiom,
sFlat1 = join(r1,meet(r2,b)),
introduced(definition) ).
cnf(t21,axiom,
sFlat0 = meet(r2,b),
introduced(definition) ).
cnf(t53,plain,
meet(r2,b) = sFlat0,
inference(orient,[status(thm)],[t21]) ).
cnf(t17956,plain,
sFlat1 = join(r1,sFlat0),
inference(step,[status(thm)],[t22,t53]) ).
cnf(t17957,plain,
sFlat1 = join(sFlat0,r1),
inference(step,[status(thm)],[t17956,t60]) ).
cnf(t106,plain,
join(sFlat0,r1) = sFlat1,
inference(orient,[status(thm)],[t17957]) ).
cnf(t270,plain,
r1 = meet(r1,sFlat1),
inference(cp,[status(thm)],[t266,t106]) ).
cnf(t17969,plain,
r1 = meet(sFlat1,r1),
inference(step,[status(thm)],[t270,t35]) ).
cnf(t285,plain,
meet(sFlat1,r1) = r1,
inference(orient,[status(thm)],[t17969]) ).
cnf(t10835,plain,
join(r1,meet(X1,sFlat1)) = ifeq3(r1,r1,meet(sFlat1,join(r1,X1)),join(r1,meet(X1,sFlat1))),
inference(cp,[status(thm)],[t10737,t285]) ).
cnf(t10,axiom,
ifeq3(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t34,plain,
ifeq3(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t18430,plain,
join(r1,meet(X1,sFlat1)) = meet(sFlat1,join(r1,X1)),
inference(step,[status(thm)],[t10835,t34]) ).
cnf(t11616,plain,
join(r1,meet(X1,sFlat1)) = meet(sFlat1,join(r1,X1)),
inference(orient,[status(thm)],[t18430]) ).
cnf(t11621,plain,
meet(sFlat1,join(r1,X1)) = join(r1,meet(sFlat1,X1)),
inference(cp,[status(thm)],[t11616,t35]) ).
cnf(t11834,plain,
join(r1,meet(sFlat1,X1)) = meet(sFlat1,join(r1,X1)),
inference(orient,[status(thm)],[t11621]) ).
cnf(t107,plain,
sFlat0 = meet(sFlat0,sFlat1),
inference(cp,[status(thm)],[t27,t106]) ).
cnf(t192,plain,
meet(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t107]) ).
cnf(t195,plain,
join(sFlat0,meet(X1,sFlat1)) = ifeq3(sFlat0,sFlat0,meet(sFlat1,join(sFlat0,X1)),join(sFlat0,meet(X1,sFlat1))),
inference(cp,[status(thm)],[t63,t192]) ).
cnf(t18071,plain,
join(sFlat0,meet(X1,sFlat1)) = meet(sFlat1,join(sFlat0,X1)),
inference(step,[status(thm)],[t195,t34]) ).
cnf(t2057,plain,
join(sFlat0,meet(X1,sFlat1)) = meet(sFlat1,join(sFlat0,X1)),
inference(orient,[status(thm)],[t18071]) ).
cnf(t2067,plain,
meet(X1,sFlat1) = meet(meet(X1,sFlat1),meet(sFlat1,join(sFlat0,X1))),
inference(cp,[status(thm)],[t266,t2057]) ).
cnf(t18,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t38,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t18]) ).
cnf(t18482,plain,
meet(X1,sFlat1) = meet(X1,meet(sFlat1,meet(sFlat1,join(sFlat0,X1)))),
inference(step,[status(thm)],[t2067,t38]) ).
cnf(t3,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t42,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t38,t26]) ).
cnf(t345,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t42]) ).
cnf(t18483,plain,
meet(X1,sFlat1) = meet(X1,meet(sFlat1,join(sFlat0,X1))),
inference(step,[status(thm)],[t18482,t345]) ).
cnf(t16866,plain,
meet(X1,meet(sFlat1,join(sFlat0,X1))) = meet(X1,sFlat1),
inference(orient,[status(thm)],[t18483]) ).
cnf(t67,plain,
join(X1,meet(X2,join(X1,X3))) = ifeq3(X1,X1,meet(join(X1,X3),join(X1,X2)),join(X1,meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t63,t27]) ).
cnf(t18221,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X3),join(X1,X2)),
inference(step,[status(thm)],[t67,t34]) ).
cnf(t5223,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X3),join(X1,X2)),
inference(orient,[status(thm)],[t18221]) ).
cnf(t45,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t38,t35]) ).
cnf(t18116,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t45,t38]) ).
cnf(t2865,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t18116]) ).
cnf(t16,axiom,
ifeq(complement(X1,X2),true,meet(X1,X2),n0) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t146,plain,
ifeq(complement(X1,X2),true,meet(X1,X2),n0) = n0,
inference(orient,[status(thm)],[t16]) ).
cnf(t6,axiom,
complement(r1,join(a,b)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17961,plain,
complement(r1,join(b,a)) = true,
inference(step,[status(thm)],[t6,t60]) ).
cnf(t115,plain,
complement(r1,join(b,a)) = true,
inference(orient,[status(thm)],[t17961]) ).
cnf(t148,plain,
n0 = ifeq(true,true,meet(r1,join(b,a)),n0),
inference(cp,[status(thm)],[t146,t115]) ).
cnf(t8,axiom,
ifeq(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t32,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t8]) ).
cnf(t17973,plain,
n0 = meet(r1,join(b,a)),
inference(step,[status(thm)],[t148,t32]) ).
cnf(t338,plain,
meet(r1,join(b,a)) = n0,
inference(orient,[status(thm)],[t17973]) ).
cnf(t2896,plain,
meet(r1,meet(X1,join(b,a))) = meet(X1,n0),
inference(cp,[status(thm)],[t2865,t338]) ).
cnf(t4,axiom,
meet(X1,n0) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t47,plain,
meet(X1,n0) = n0,
inference(orient,[status(thm)],[t4]) ).
cnf(t18169,plain,
meet(r1,meet(X1,join(b,a))) = n0,
inference(step,[status(thm)],[t2896,t47]) ).
cnf(t4096,plain,
meet(r1,meet(X1,join(b,a))) = n0,
inference(orient,[status(thm)],[t18169]) ).
cnf(t12,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t37,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t30,t35]) ).
cnf(t216,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t37]) ).
cnf(t54,plain,
meet(r2,meet(b,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t38,t53]) ).
cnf(t355,plain,
meet(r2,meet(b,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t54]) ).
cnf(t358,plain,
meet(sFlat0,join(b,X1)) = meet(r2,b),
inference(cp,[status(thm)],[t355,t27]) ).
cnf(t17984,plain,
meet(sFlat0,join(b,X1)) = sFlat0,
inference(step,[status(thm)],[t358,t53]) ).
cnf(t376,plain,
meet(sFlat0,join(b,X1)) = sFlat0,
inference(orient,[status(thm)],[t17984]) ).
cnf(t378,plain,
join(b,X1) = join(join(b,X1),sFlat0),
inference(cp,[status(thm)],[t216,t376]) ).
cnf(t17,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t91,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t17]) ).
cnf(t18029,plain,
join(b,X1) = join(b,join(X1,sFlat0)),
inference(step,[status(thm)],[t378,t91]) ).
cnf(t1083,plain,
join(b,join(X1,sFlat0)) = join(b,X1),
inference(orient,[status(thm)],[t18029]) ).
cnf(t1088,plain,
join(X1,sFlat0) = meet(join(X1,sFlat0),join(b,X1)),
inference(cp,[status(thm)],[t266,t1083]) ).
cnf(t15092,plain,
meet(join(X1,sFlat0),join(b,X1)) = join(X1,sFlat0),
inference(orient,[status(thm)],[t1088]) ).
cnf(t15125,plain,
n0 = meet(r1,join(a,sFlat0)),
inference(cp,[status(thm)],[t4096,t15092]) ).
cnf(t18470,plain,
n0 = meet(r1,join(sFlat0,a)),
inference(step,[status(thm)],[t15125,t60]) ).
cnf(t15142,plain,
meet(r1,join(sFlat0,a)) = n0,
inference(orient,[status(thm)],[t18470]) ).
cnf(t15165,plain,
meet(r1,meet(X1,join(sFlat0,a))) = meet(X1,n0),
inference(cp,[status(thm)],[t2865,t15142]) ).
cnf(t18475,plain,
meet(r1,meet(X1,join(sFlat0,a))) = n0,
inference(step,[status(thm)],[t15165,t47]) ).
cnf(t15223,plain,
meet(r1,meet(X1,join(sFlat0,a))) = n0,
inference(orient,[status(thm)],[t18475]) ).
cnf(t55,plain,
r2 = join(r2,sFlat0),
inference(cp,[status(thm)],[t30,t53]) ).
cnf(t17962,plain,
r2 = join(sFlat0,r2),
inference(step,[status(thm)],[t55,t60]) ).
cnf(t170,plain,
join(sFlat0,r2) = r2,
inference(orient,[status(thm)],[t17962]) ).
cnf(t171,plain,
sFlat0 = meet(sFlat0,r2),
inference(cp,[status(thm)],[t27,t170]) ).
cnf(t204,plain,
meet(sFlat0,r2) = sFlat0,
inference(orient,[status(thm)],[t171]) ).
cnf(t207,plain,
join(sFlat0,meet(X1,r2)) = ifeq3(sFlat0,sFlat0,meet(r2,join(sFlat0,X1)),join(sFlat0,meet(X1,r2))),
inference(cp,[status(thm)],[t63,t204]) ).
cnf(t18073,plain,
join(sFlat0,meet(X1,r2)) = meet(r2,join(sFlat0,X1)),
inference(step,[status(thm)],[t207,t34]) ).
cnf(t2087,plain,
join(sFlat0,meet(X1,r2)) = meet(r2,join(sFlat0,X1)),
inference(orient,[status(thm)],[t18073]) ).
cnf(t2093,plain,
meet(r2,join(sFlat0,X1)) = join(sFlat0,meet(r2,X1)),
inference(cp,[status(thm)],[t2087,t35]) ).
cnf(t2585,plain,
join(sFlat0,meet(r2,X1)) = meet(r2,join(sFlat0,X1)),
inference(orient,[status(thm)],[t2093]) ).
cnf(t23,axiom,
sFlat2 = meet(r2,a),
introduced(definition) ).
cnf(t57,plain,
meet(r2,a) = sFlat2,
inference(orient,[status(thm)],[t23]) ).
cnf(t2592,plain,
meet(r2,join(sFlat0,a)) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t2585,t57]) ).
cnf(t2607,plain,
meet(r2,join(sFlat0,a)) = join(sFlat0,sFlat2),
inference(orient,[status(thm)],[t2592]) ).
cnf(t15229,plain,
n0 = meet(r1,join(sFlat0,sFlat2)),
inference(cp,[status(thm)],[t15223,t2607]) ).
cnf(t15256,plain,
meet(r1,join(sFlat0,sFlat2)) = n0,
inference(orient,[status(thm)],[t15229]) ).
cnf(t15266,plain,
meet(join(sFlat0,sFlat2),join(sFlat0,r1)) = join(sFlat0,n0),
inference(cp,[status(thm)],[t5223,t15256]) ).
cnf(t18476,plain,
meet(join(sFlat0,sFlat2),sFlat1) = join(sFlat0,n0),
inference(step,[status(thm)],[t15266,t106]) ).
cnf(t18477,plain,
meet(sFlat1,join(sFlat0,sFlat2)) = join(sFlat0,n0),
inference(step,[status(thm)],[t18476,t35]) ).
cnf(t1,axiom,
join(X1,n0) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t31,plain,
join(X1,n0) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t18478,plain,
meet(sFlat1,join(sFlat0,sFlat2)) = sFlat0,
inference(step,[status(thm)],[t18477,t31]) ).
cnf(t15280,plain,
meet(sFlat1,join(sFlat0,sFlat2)) = sFlat0,
inference(orient,[status(thm)],[t18478]) ).
cnf(t16870,plain,
meet(sFlat2,sFlat1) = meet(sFlat2,sFlat0),
inference(cp,[status(thm)],[t16866,t15280]) ).
cnf(t18484,plain,
meet(sFlat1,sFlat2) = meet(sFlat2,sFlat0),
inference(step,[status(thm)],[t16870,t35]) ).
cnf(t18485,plain,
meet(sFlat1,sFlat2) = meet(sFlat0,sFlat2),
inference(step,[status(thm)],[t18484,t35]) ).
cnf(t7,axiom,
complement(r2,meet(a,b)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17960,plain,
complement(r2,meet(b,a)) = true,
inference(step,[status(thm)],[t7,t35]) ).
cnf(t114,plain,
complement(r2,meet(b,a)) = true,
inference(orient,[status(thm)],[t17960]) ).
cnf(t147,plain,
n0 = ifeq(true,true,meet(r2,meet(b,a)),n0),
inference(cp,[status(thm)],[t146,t114]) ).
cnf(t17972,plain,
n0 = meet(r2,meet(b,a)),
inference(step,[status(thm)],[t147,t32]) ).
cnf(t313,plain,
meet(r2,meet(b,a)) = n0,
inference(orient,[status(thm)],[t17972]) ).
cnf(t17983,plain,
meet(sFlat0,a) = n0,
inference(step,[status(thm)],[t313,t355]) ).
cnf(t369,plain,
meet(sFlat0,a) = n0,
inference(rw,[status(thm)],[t17983]) ).
cnf(t370,plain,
meet(sFlat0,a) = n0,
inference(orient,[status(thm)],[t369]) ).
cnf(t372,plain,
meet(sFlat0,meet(a,X1)) = meet(n0,X1),
inference(cp,[status(thm)],[t38,t370]) ).
cnf(t48,plain,
n0 = meet(n0,X1),
inference(cp,[status(thm)],[t47,t35]) ).
cnf(t164,plain,
meet(n0,X1) = n0,
inference(orient,[status(thm)],[t48]) ).
cnf(t17986,plain,
meet(sFlat0,meet(a,X1)) = n0,
inference(step,[status(thm)],[t372,t164]) ).
cnf(t413,plain,
meet(sFlat0,meet(a,X1)) = n0,
inference(orient,[status(thm)],[t17986]) ).
cnf(t414,plain,
n0 = meet(sFlat0,meet(X1,a)),
inference(cp,[status(thm)],[t413,t35]) ).
cnf(t429,plain,
meet(sFlat0,meet(X1,a)) = n0,
inference(orient,[status(thm)],[t414]) ).
cnf(t224,plain,
a = join(a,sFlat2),
inference(cp,[status(thm)],[t216,t57]) ).
cnf(t17967,plain,
a = join(sFlat2,a),
inference(step,[status(thm)],[t224,t60]) ).
cnf(t246,plain,
join(sFlat2,a) = a,
inference(orient,[status(thm)],[t17967]) ).
cnf(t247,plain,
sFlat2 = meet(sFlat2,a),
inference(cp,[status(thm)],[t27,t246]) ).
cnf(t259,plain,
meet(sFlat2,a) = sFlat2,
inference(orient,[status(thm)],[t247]) ).
cnf(t430,plain,
n0 = meet(sFlat0,sFlat2),
inference(cp,[status(thm)],[t429,t259]) ).
cnf(t438,plain,
meet(sFlat0,sFlat2) = n0,
inference(orient,[status(thm)],[t430]) ).
cnf(t18486,plain,
meet(sFlat1,sFlat2) = n0,
inference(step,[status(thm)],[t18485,t438]) ).
cnf(t16937,plain,
meet(sFlat1,sFlat2) = n0,
inference(orient,[status(thm)],[t18486]) ).
cnf(t16943,plain,
meet(sFlat1,join(r1,sFlat2)) = join(r1,n0),
inference(cp,[status(thm)],[t11834,t16937]) ).
cnf(t18494,plain,
meet(sFlat1,join(sFlat2,r1)) = join(r1,n0),
inference(step,[status(thm)],[t16943,t60]) ).
cnf(t24,axiom,
sFlat3 = join(r1,meet(r2,a)),
introduced(definition) ).
cnf(t17958,plain,
sFlat3 = join(r1,sFlat2),
inference(step,[status(thm)],[t24,t57]) ).
cnf(t17959,plain,
sFlat3 = join(sFlat2,r1),
inference(step,[status(thm)],[t17958,t60]) ).
cnf(t110,plain,
join(sFlat2,r1) = sFlat3,
inference(orient,[status(thm)],[t17959]) ).
cnf(t18495,plain,
meet(sFlat1,sFlat3) = join(r1,n0),
inference(step,[status(thm)],[t18494,t110]) ).
cnf(t25,axiom,
sFlat4 = meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))),
introduced(definition) ).
cnf(t50,plain,
meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))) = sFlat4,
inference(orient,[status(thm)],[t25]) ).
cnf(t17955,plain,
meet(join(r1,sFlat0),join(r1,meet(r2,a))) = sFlat4,
inference(step,[status(thm)],[t50,t53]) ).
cnf(t56,plain,
meet(join(r1,sFlat0),join(r1,meet(r2,a))) = sFlat4,
inference(rw,[status(thm)],[t17955]) ).
cnf(t18186,plain,
meet(join(sFlat0,r1),join(r1,meet(r2,a))) = sFlat4,
inference(step,[status(thm)],[t56,t60]) ).
cnf(t18187,plain,
meet(sFlat1,join(r1,meet(r2,a))) = sFlat4,
inference(step,[status(thm)],[t18186,t106]) ).
cnf(t18188,plain,
meet(sFlat1,join(r1,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t18187,t57]) ).
cnf(t18189,plain,
meet(sFlat1,join(sFlat2,r1)) = sFlat4,
inference(step,[status(thm)],[t18188,t60]) ).
cnf(t18190,plain,
meet(sFlat1,sFlat3) = sFlat4,
inference(step,[status(thm)],[t18189,t110]) ).
cnf(t4465,plain,
meet(sFlat1,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t18190]) ).
cnf(t18496,plain,
sFlat4 = join(r1,n0),
inference(step,[status(thm)],[t18495,t4465]) ).
cnf(t18497,plain,
sFlat4 = r1,
inference(step,[status(thm)],[t18496,t31]) ).
cnf(t17890,plain,
r1 = sFlat4,
inference(orient,[status(thm)],[t18497]) ).
cnf(t2062,plain,
meet(sFlat1,join(sFlat0,X1)) = join(sFlat0,meet(sFlat1,X1)),
inference(cp,[status(thm)],[t2057,t35]) ).
cnf(t2543,plain,
join(sFlat0,meet(sFlat1,X1)) = meet(sFlat1,join(sFlat0,X1)),
inference(orient,[status(thm)],[t2062]) ).
cnf(t4466,plain,
meet(sFlat1,join(sFlat0,sFlat3)) = join(sFlat0,sFlat4),
inference(cp,[status(thm)],[t2543,t4465]) ).
cnf(t108,plain,
join(sFlat0,join(r1,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t91,t106]) ).
cnf(t525,plain,
join(sFlat0,join(r1,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t108]) ).
cnf(t530,plain,
join(sFlat1,X1) = join(sFlat0,join(X1,r1)),
inference(cp,[status(thm)],[t525,t60]) ).
cnf(t1162,plain,
join(sFlat0,join(X1,r1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t530]) ).
cnf(t269,plain,
r1 = meet(r1,sFlat3),
inference(cp,[status(thm)],[t266,t110]) ).
cnf(t17968,plain,
r1 = meet(sFlat3,r1),
inference(step,[status(thm)],[t269,t35]) ).
cnf(t278,plain,
meet(sFlat3,r1) = r1,
inference(orient,[status(thm)],[t17968]) ).
cnf(t281,plain,
sFlat3 = join(sFlat3,r1),
inference(cp,[status(thm)],[t30,t278]) ).
cnf(t292,plain,
join(sFlat3,r1) = sFlat3,
inference(orient,[status(thm)],[t281]) ).
cnf(t1166,plain,
join(sFlat1,sFlat3) = join(sFlat0,sFlat3),
inference(cp,[status(thm)],[t1162,t292]) ).
cnf(t1195,plain,
join(sFlat1,sFlat3) = join(sFlat0,sFlat3),
inference(orient,[status(thm)],[t1166]) ).
cnf(t1196,plain,
sFlat1 = meet(sFlat1,join(sFlat0,sFlat3)),
inference(cp,[status(thm)],[t27,t1195]) ).
cnf(t1229,plain,
meet(sFlat1,join(sFlat0,sFlat3)) = sFlat1,
inference(orient,[status(thm)],[t1196]) ).
cnf(t18193,plain,
sFlat1 = join(sFlat0,sFlat4),
inference(step,[status(thm)],[t4466,t1229]) ).
cnf(t4489,plain,
join(sFlat0,sFlat4) = sFlat1,
inference(orient,[status(thm)],[t18193]) ).
cnf(t111,plain,
sFlat2 = meet(sFlat2,sFlat3),
inference(cp,[status(thm)],[t27,t110]) ).
cnf(t198,plain,
meet(sFlat2,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t111]) ).
cnf(t201,plain,
join(sFlat2,meet(X1,sFlat3)) = ifeq3(sFlat2,sFlat2,meet(sFlat3,join(sFlat2,X1)),join(sFlat2,meet(X1,sFlat3))),
inference(cp,[status(thm)],[t63,t198]) ).
cnf(t18072,plain,
join(sFlat2,meet(X1,sFlat3)) = meet(sFlat3,join(sFlat2,X1)),
inference(step,[status(thm)],[t201,t34]) ).
cnf(t2072,plain,
join(sFlat2,meet(X1,sFlat3)) = meet(sFlat3,join(sFlat2,X1)),
inference(orient,[status(thm)],[t18072]) ).
cnf(t4467,plain,
meet(sFlat3,join(sFlat2,sFlat1)) = join(sFlat2,sFlat4),
inference(cp,[status(thm)],[t2072,t4465]) ).
cnf(t18205,plain,
meet(sFlat3,join(sFlat1,sFlat2)) = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t4467,t60]) ).
cnf(t1167,plain,
join(sFlat1,sFlat2) = join(sFlat0,sFlat3),
inference(cp,[status(thm)],[t1162,t110]) ).
cnf(t1203,plain,
join(sFlat1,sFlat2) = join(sFlat0,sFlat3),
inference(orient,[status(thm)],[t1167]) ).
cnf(t18206,plain,
meet(sFlat3,join(sFlat0,sFlat3)) = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t18205,t1203]) ).
cnf(t18207,plain,
sFlat3 = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t18206,t266]) ).
cnf(t4786,plain,
join(sFlat2,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t18207]) ).
cnf(goal_0,negated_conjecture,
meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))) != r1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(join(sFlat4,meet(r2,b)),join(r1,meet(r2,a))) != r1,
inference(rw,[status(thm)],[goal_0,t17890]) ).
cnf(g0_1,plain,
meet(join(sFlat4,sFlat0),join(r1,meet(r2,a))) != r1,
inference(rw,[status(thm)],[g0_0,t53]) ).
cnf(g0_2,plain,
meet(join(sFlat0,sFlat4),join(r1,meet(r2,a))) != r1,
inference(rw,[status(thm)],[g0_1,t60]) ).
cnf(g0_3,plain,
meet(sFlat1,join(r1,meet(r2,a))) != r1,
inference(rw,[status(thm)],[g0_2,t4489]) ).
cnf(g0_4,plain,
meet(sFlat1,join(sFlat4,meet(r2,a))) != r1,
inference(rw,[status(thm)],[g0_3,t17890]) ).
cnf(g0_5,plain,
meet(sFlat1,join(sFlat4,sFlat2)) != r1,
inference(rw,[status(thm)],[g0_4,t57]) ).
cnf(g0_6,plain,
meet(sFlat1,join(sFlat2,sFlat4)) != r1,
inference(rw,[status(thm)],[g0_5,t60]) ).
cnf(g0_7,plain,
meet(sFlat1,sFlat3) != r1,
inference(rw,[status(thm)],[g0_6,t4786]) ).
cnf(g0_8,plain,
sFlat4 != r1,
inference(rw,[status(thm)],[g0_7,t4465]) ).
cnf(g0_9,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_8,t17890]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT005-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Wed Sep 23 19:53:59 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 19.52/3.00 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.52/3.00 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------