%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT155-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.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:55:36 PM UTC 2026
% Result : Unsatisfiable 39.87s 15.47s
% Output : CNFRefutation 39.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 16
% Syntax : Number of clauses : 255 ( 255 unt; 0 nHn; 185 RR)
% Number of literals : 255 ( 254 equ; 18 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 137 ( 31 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t78,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t11,axiom,
sFlat2 = meet(b,c),
introduced(definition) ).
cnf(t109558,plain,
sFlat2 = meet(c,b),
inference(step,[status(thm)],[t11,t23]) ).
cnf(t52,plain,
meet(c,b) = sFlat2,
inference(orient,[status(thm)],[t109558]) ).
cnf(t9,axiom,
sFlat0 = join(b,c),
introduced(definition) ).
cnf(t109579,plain,
sFlat0 = join(c,b),
inference(step,[status(thm)],[t9,t78]) ).
cnf(t105,plain,
join(c,b) = sFlat0,
inference(orient,[status(thm)],[t109579]) ).
cnf(t10,axiom,
sFlat1 = meet(a,join(b,c)),
introduced(definition) ).
cnf(t67,plain,
meet(a,join(b,c)) = sFlat1,
inference(orient,[status(thm)],[t10]) ).
cnf(t82,plain,
meet(a,join(b,c)) = sFlat1,
inference(rw,[status(thm)],[t67]) ).
cnf(t109595,plain,
meet(a,join(c,b)) = sFlat1,
inference(step,[status(thm)],[t82,t78]) ).
cnf(t109596,plain,
meet(a,sFlat0) = sFlat1,
inference(step,[status(thm)],[t109595,t105]) ).
cnf(t109597,plain,
meet(sFlat0,a) = sFlat1,
inference(step,[status(thm)],[t109596,t23]) ).
cnf(t220,plain,
meet(sFlat0,a) = sFlat1,
inference(orient,[status(thm)],[t109597]) ).
cnf(t12,axiom,
sFlat3 = join(meet(a,join(b,c)),meet(b,c)),
introduced(definition) ).
cnf(t109566,plain,
sFlat3 = join(meet(b,c),meet(a,join(b,c))),
inference(step,[status(thm)],[t12,t78]) ).
cnf(t109567,plain,
sFlat3 = join(meet(c,b),meet(a,join(b,c))),
inference(step,[status(thm)],[t109566,t23]) ).
cnf(t109568,plain,
sFlat3 = join(sFlat2,meet(a,join(b,c))),
inference(step,[status(thm)],[t109567,t52]) ).
cnf(t109569,plain,
sFlat3 = join(sFlat2,meet(a,join(c,b))),
inference(step,[status(thm)],[t109568,t78]) ).
cnf(t93,plain,
join(sFlat2,meet(a,join(c,b))) = sFlat3,
inference(orient,[status(thm)],[t109569]) ).
cnf(t109580,plain,
join(sFlat2,meet(a,sFlat0)) = sFlat3,
inference(step,[status(thm)],[t93,t105]) ).
cnf(t109,plain,
join(sFlat2,meet(a,sFlat0)) = sFlat3,
inference(rw,[status(thm)],[t109580]) ).
cnf(t109600,plain,
join(sFlat2,meet(sFlat0,a)) = sFlat3,
inference(step,[status(thm)],[t109,t23]) ).
cnf(t109601,plain,
join(sFlat2,sFlat1) = sFlat3,
inference(step,[status(thm)],[t109600,t220]) ).
cnf(t109602,plain,
join(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t109601,t78]) ).
cnf(t240,plain,
join(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t109602]) ).
cnf(t13,axiom,
sFlat4 = meet(c,join(meet(a,join(b,c)),meet(b,c))),
introduced(definition) ).
cnf(t109557,plain,
sFlat4 = meet(c,join(meet(a,join(b,c)),meet(c,b))),
inference(step,[status(thm)],[t13,t23]) ).
cnf(t47,plain,
meet(c,join(meet(a,join(b,c)),meet(c,b))) = sFlat4,
inference(orient,[status(thm)],[t109557]) ).
cnf(t109559,plain,
meet(c,join(meet(a,join(b,c)),sFlat2)) = sFlat4,
inference(step,[status(thm)],[t47,t52]) ).
cnf(t56,plain,
meet(c,join(meet(a,join(b,c)),sFlat2)) = sFlat4,
inference(rw,[status(thm)],[t109559]) ).
cnf(t110024,plain,
meet(c,join(sFlat2,meet(a,join(b,c)))) = sFlat4,
inference(step,[status(thm)],[t56,t78]) ).
cnf(t110025,plain,
meet(c,join(sFlat2,meet(a,join(c,b)))) = sFlat4,
inference(step,[status(thm)],[t110024,t78]) ).
cnf(t110026,plain,
meet(c,join(sFlat2,meet(a,sFlat0))) = sFlat4,
inference(step,[status(thm)],[t110025,t105]) ).
cnf(t110027,plain,
meet(c,join(sFlat2,meet(sFlat0,a))) = sFlat4,
inference(step,[status(thm)],[t110026,t23]) ).
cnf(t110028,plain,
meet(c,join(sFlat2,sFlat1)) = sFlat4,
inference(step,[status(thm)],[t110027,t220]) ).
cnf(t110029,plain,
meet(c,join(sFlat1,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t110028,t78]) ).
cnf(t110030,plain,
meet(c,sFlat3) = sFlat4,
inference(step,[status(thm)],[t110029,t240]) ).
cnf(t110031,plain,
meet(sFlat3,c) = sFlat4,
inference(step,[status(thm)],[t110030,t23]) ).
cnf(t37830,plain,
meet(sFlat3,c) = sFlat4,
inference(orient,[status(thm)],[t110031]) ).
cnf(t14,axiom,
sFlat5 = join(b,meet(c,join(meet(a,join(b,c)),meet(b,c)))),
introduced(definition) ).
cnf(t109570,plain,
sFlat5 = join(b,meet(c,join(meet(b,c),meet(a,join(b,c))))),
inference(step,[status(thm)],[t14,t78]) ).
cnf(t109571,plain,
sFlat5 = join(b,meet(c,join(meet(c,b),meet(a,join(b,c))))),
inference(step,[status(thm)],[t109570,t23]) ).
cnf(t109572,plain,
sFlat5 = join(b,meet(c,join(sFlat2,meet(a,join(b,c))))),
inference(step,[status(thm)],[t109571,t52]) ).
cnf(t109573,plain,
sFlat5 = join(b,meet(c,join(sFlat2,meet(a,join(c,b))))),
inference(step,[status(thm)],[t109572,t78]) ).
cnf(t109574,plain,
sFlat5 = join(b,meet(c,sFlat3)),
inference(step,[status(thm)],[t109573,t93]) ).
cnf(t109575,plain,
sFlat5 = join(b,meet(sFlat3,c)),
inference(step,[status(thm)],[t109574,t23]) ).
cnf(t97,plain,
join(b,meet(sFlat3,c)) = sFlat5,
inference(orient,[status(thm)],[t109575]) ).
cnf(t110043,plain,
join(b,sFlat4) = sFlat5,
inference(step,[status(thm)],[t97,t37830]) ).
cnf(t37886,plain,
join(b,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t110043]) ).
cnf(t110066,plain,
join(sFlat4,b) = sFlat5,
inference(step,[status(thm)],[t37886,t78]) ).
cnf(t38275,plain,
join(sFlat4,b) = sFlat5,
inference(orient,[status(thm)],[t110066]) ).
cnf(t16,axiom,
sFlat7 = meet(a,c),
introduced(definition) ).
cnf(t109564,plain,
sFlat7 = meet(c,a),
inference(step,[status(thm)],[t16,t23]) ).
cnf(t73,plain,
meet(c,a) = sFlat7,
inference(orient,[status(thm)],[t109564]) ).
cnf(t17,axiom,
sFlat8 = join(b,meet(a,c)),
introduced(definition) ).
cnf(t109576,plain,
sFlat8 = join(b,meet(c,a)),
inference(step,[status(thm)],[t17,t23]) ).
cnf(t109577,plain,
sFlat8 = join(b,sFlat7),
inference(step,[status(thm)],[t109576,t73]) ).
cnf(t109578,plain,
sFlat8 = join(sFlat7,b),
inference(step,[status(thm)],[t109577,t78]) ).
cnf(t101,plain,
join(sFlat7,b) = sFlat8,
inference(orient,[status(thm)],[t109578]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t24,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t22,t23]) ).
cnf(t141,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t24]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t5,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t30,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t25,t20]) ).
cnf(t1830,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t30]) ).
cnf(t37851,plain,
c = join(c,sFlat4),
inference(cp,[status(thm)],[t141,t37830]) ).
cnf(t110063,plain,
c = join(sFlat4,c),
inference(step,[status(thm)],[t37851,t78]) ).
cnf(t38121,plain,
join(sFlat4,c) = c,
inference(orient,[status(thm)],[t110063]) ).
cnf(t38130,plain,
meet(sFlat4,X1) = meet(sFlat4,meet(c,X1)),
inference(cp,[status(thm)],[t1830,t38121]) ).
cnf(t43007,plain,
meet(sFlat4,meet(c,X1)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t38130]) ).
cnf(t8,axiom,
meet(X1,join(X2,join(meet(X1,X3),meet(X3,join(X2,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X3,join(X2,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t8]) ).
cnf(t76,plain,
meet(c,join(X1,meet(a,join(c,X2)))) = meet(c,join(X1,join(sFlat7,meet(a,join(X1,X2))))),
inference(cp,[status(thm)],[t33,t73]) ).
cnf(t41946,plain,
meet(c,join(X1,join(sFlat7,meet(a,join(X1,X2))))) = meet(c,join(X1,meet(a,join(c,X2)))),
inference(orient,[status(thm)],[t76]) ).
cnf(t79,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t20,t78]) ).
cnf(t188,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t79]) ).
cnf(t195,plain,
b = meet(b,sFlat8),
inference(cp,[status(thm)],[t188,t101]) ).
cnf(t109594,plain,
b = meet(sFlat8,b),
inference(step,[status(thm)],[t195,t23]) ).
cnf(t208,plain,
meet(sFlat8,b) = b,
inference(orient,[status(thm)],[t109594]) ).
cnf(t210,plain,
sFlat8 = join(sFlat8,b),
inference(cp,[status(thm)],[t22,t208]) ).
cnf(t216,plain,
join(sFlat8,b) = sFlat8,
inference(orient,[status(thm)],[t210]) ).
cnf(t42108,plain,
meet(c,join(sFlat8,meet(a,join(c,b)))) = meet(c,join(sFlat8,join(sFlat7,meet(a,sFlat8)))),
inference(cp,[status(thm)],[t41946,t216]) ).
cnf(t110427,plain,
meet(c,join(sFlat8,meet(a,sFlat0))) = meet(c,join(sFlat8,join(sFlat7,meet(a,sFlat8)))),
inference(step,[status(thm)],[t42108,t105]) ).
cnf(t110428,plain,
meet(c,join(sFlat8,meet(sFlat0,a))) = meet(c,join(sFlat8,join(sFlat7,meet(a,sFlat8)))),
inference(step,[status(thm)],[t110427,t23]) ).
cnf(t110429,plain,
meet(c,join(sFlat8,sFlat1)) = meet(c,join(sFlat8,join(sFlat7,meet(a,sFlat8)))),
inference(step,[status(thm)],[t110428,t220]) ).
cnf(t110430,plain,
meet(c,join(sFlat1,sFlat8)) = meet(c,join(sFlat8,join(sFlat7,meet(a,sFlat8)))),
inference(step,[status(thm)],[t110429,t78]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t83,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t88,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t83,t22]) ).
cnf(t16420,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t88]) ).
cnf(t37857,plain,
join(sFlat3,X1) = join(sFlat3,join(sFlat4,X1)),
inference(cp,[status(thm)],[t16420,t37830]) ).
cnf(t39900,plain,
join(sFlat3,join(sFlat4,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t37857]) ).
cnf(t39909,plain,
join(sFlat3,b) = join(sFlat3,sFlat5),
inference(cp,[status(thm)],[t39900,t38275]) ).
cnf(t243,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t83,t240]) ).
cnf(t1335,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t243]) ).
cnf(t148,plain,
b = join(b,sFlat2),
inference(cp,[status(thm)],[t141,t52]) ).
cnf(t109586,plain,
b = join(sFlat2,b),
inference(step,[status(thm)],[t148,t78]) ).
cnf(t156,plain,
join(sFlat2,b) = b,
inference(orient,[status(thm)],[t109586]) ).
cnf(t1342,plain,
join(sFlat3,b) = join(sFlat1,b),
inference(cp,[status(thm)],[t1335,t156]) ).
cnf(t1373,plain,
join(sFlat3,b) = join(sFlat1,b),
inference(orient,[status(thm)],[t1342]) ).
cnf(t74,plain,
meet(c,meet(a,X1)) = meet(sFlat7,X1),
inference(cp,[status(thm)],[t25,t73]) ).
cnf(t366,plain,
meet(c,meet(a,X1)) = meet(sFlat7,X1),
inference(orient,[status(thm)],[t74]) ).
cnf(t372,plain,
meet(sFlat7,X1) = meet(c,meet(X1,a)),
inference(cp,[status(thm)],[t366,t23]) ).
cnf(t1708,plain,
meet(c,meet(X1,a)) = meet(sFlat7,X1),
inference(orient,[status(thm)],[t372]) ).
cnf(t1714,plain,
meet(sFlat7,sFlat0) = meet(c,sFlat1),
inference(cp,[status(thm)],[t1708,t220]) ).
cnf(t109655,plain,
meet(sFlat0,sFlat7) = meet(c,sFlat1),
inference(step,[status(thm)],[t1714,t23]) ).
cnf(t75,plain,
c = join(c,sFlat7),
inference(cp,[status(thm)],[t22,t73]) ).
cnf(t109582,plain,
c = join(sFlat7,c),
inference(step,[status(thm)],[t75,t78]) ).
cnf(t114,plain,
join(sFlat7,c) = c,
inference(orient,[status(thm)],[t109582]) ).
cnf(t116,plain,
join(sFlat7,join(c,X1)) = join(c,X1),
inference(cp,[status(thm)],[t83,t114]) ).
cnf(t549,plain,
join(sFlat7,join(c,X1)) = join(c,X1),
inference(orient,[status(thm)],[t116]) ).
cnf(t551,plain,
join(c,b) = join(sFlat7,sFlat0),
inference(cp,[status(thm)],[t549,t105]) ).
cnf(t109616,plain,
sFlat0 = join(sFlat7,sFlat0),
inference(step,[status(thm)],[t551,t105]) ).
cnf(t109617,plain,
sFlat0 = join(sFlat0,sFlat7),
inference(step,[status(thm)],[t109616,t78]) ).
cnf(t555,plain,
join(sFlat0,sFlat7) = sFlat0,
inference(orient,[status(thm)],[t109617]) ).
cnf(t558,plain,
sFlat7 = meet(sFlat7,sFlat0),
inference(cp,[status(thm)],[t188,t555]) ).
cnf(t109618,plain,
sFlat7 = meet(sFlat0,sFlat7),
inference(step,[status(thm)],[t558,t23]) ).
cnf(t561,plain,
meet(sFlat0,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t109618]) ).
cnf(t109656,plain,
sFlat7 = meet(c,sFlat1),
inference(step,[status(thm)],[t109655,t561]) ).
cnf(t109657,plain,
sFlat7 = meet(sFlat1,c),
inference(step,[status(thm)],[t109656,t23]) ).
cnf(t221,plain,
a = join(a,sFlat1),
inference(cp,[status(thm)],[t141,t220]) ).
cnf(t109598,plain,
a = join(sFlat1,a),
inference(step,[status(thm)],[t221,t78]) ).
cnf(t225,plain,
join(sFlat1,a) = a,
inference(orient,[status(thm)],[t109598]) ).
cnf(t226,plain,
sFlat1 = meet(sFlat1,a),
inference(cp,[status(thm)],[t20,t225]) ).
cnf(t233,plain,
meet(sFlat1,a) = sFlat1,
inference(orient,[status(thm)],[t226]) ).
cnf(t1710,plain,
meet(sFlat7,sFlat1) = meet(c,sFlat1),
inference(cp,[status(thm)],[t1708,t233]) ).
cnf(t109653,plain,
meet(sFlat1,sFlat7) = meet(c,sFlat1),
inference(step,[status(thm)],[t1710,t23]) ).
cnf(t109654,plain,
meet(sFlat1,sFlat7) = meet(sFlat1,c),
inference(step,[status(thm)],[t109653,t23]) ).
cnf(t1741,plain,
meet(sFlat1,c) = meet(sFlat1,sFlat7),
inference(orient,[status(thm)],[t109654]) ).
cnf(t109658,plain,
sFlat7 = meet(sFlat1,sFlat7),
inference(step,[status(thm)],[t109657,t1741]) ).
cnf(t1749,plain,
meet(sFlat1,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t109658]) ).
cnf(t1755,plain,
sFlat1 = join(sFlat1,sFlat7),
inference(cp,[status(thm)],[t22,t1749]) ).
cnf(t1759,plain,
join(sFlat1,sFlat7) = sFlat1,
inference(orient,[status(thm)],[t1755]) ).
cnf(t1761,plain,
join(sFlat1,join(sFlat7,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t83,t1759]) ).
cnf(t3732,plain,
join(sFlat1,join(sFlat7,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t1761]) ).
cnf(t3738,plain,
join(sFlat1,b) = join(sFlat1,sFlat8),
inference(cp,[status(thm)],[t3732,t101]) ).
cnf(t3743,plain,
join(sFlat1,b) = join(sFlat1,sFlat8),
inference(orient,[status(thm)],[t3738]) ).
cnf(t109757,plain,
join(sFlat3,b) = join(sFlat1,sFlat8),
inference(step,[status(thm)],[t1373,t3743]) ).
cnf(t3744,plain,
join(sFlat3,b) = join(sFlat1,sFlat8),
inference(orient,[status(thm)],[t109757]) ).
cnf(t110086,plain,
join(sFlat1,sFlat8) = join(sFlat3,sFlat5),
inference(step,[status(thm)],[t39909,t3744]) ).
cnf(t53,plain,
meet(c,meet(b,X1)) = meet(sFlat2,X1),
inference(cp,[status(thm)],[t25,t52]) ).
cnf(t290,plain,
meet(c,meet(b,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t53]) ).
cnf(t293,plain,
meet(sFlat2,join(b,X1)) = meet(c,b),
inference(cp,[status(thm)],[t290,t20]) ).
cnf(t109605,plain,
meet(sFlat2,join(b,X1)) = sFlat2,
inference(step,[status(thm)],[t293,t52]) ).
cnf(t302,plain,
meet(sFlat2,join(b,X1)) = sFlat2,
inference(orient,[status(thm)],[t109605]) ).
cnf(t303,plain,
sFlat2 = meet(sFlat2,sFlat5),
inference(cp,[status(thm)],[t302,t97]) ).
cnf(t310,plain,
meet(sFlat2,sFlat5) = sFlat2,
inference(orient,[status(thm)],[t303]) ).
cnf(t311,plain,
sFlat5 = join(sFlat5,sFlat2),
inference(cp,[status(thm)],[t141,t310]) ).
cnf(t109606,plain,
sFlat5 = join(sFlat2,sFlat5),
inference(step,[status(thm)],[t311,t78]) ).
cnf(t315,plain,
join(sFlat2,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t109606]) ).
cnf(t1340,plain,
join(sFlat3,sFlat5) = join(sFlat1,sFlat5),
inference(cp,[status(thm)],[t1335,t315]) ).
cnf(t1361,plain,
join(sFlat3,sFlat5) = join(sFlat1,sFlat5),
inference(orient,[status(thm)],[t1340]) ).
cnf(t110087,plain,
join(sFlat1,sFlat8) = join(sFlat1,sFlat5),
inference(step,[status(thm)],[t110086,t1361]) ).
cnf(t40277,plain,
join(sFlat1,sFlat8) = join(sFlat1,sFlat5),
inference(orient,[status(thm)],[t110087]) ).
cnf(t110431,plain,
meet(c,join(sFlat1,sFlat5)) = meet(c,join(sFlat8,join(sFlat7,meet(a,sFlat8)))),
inference(step,[status(thm)],[t110430,t40277]) ).
cnf(t150,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t141,t25]) ).
cnf(t8946,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t150]) ).
cnf(t8960,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,X1)),
inference(cp,[status(thm)],[t8946,t20]) ).
cnf(t110279,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,X1))),
inference(step,[status(thm)],[t8960,t83]) ).
cnf(t80564,plain,
join(X1,join(X2,meet(X3,X1))) = join(X1,X2),
inference(orient,[status(thm)],[t110279]) ).
cnf(t110432,plain,
meet(c,join(sFlat1,sFlat5)) = meet(c,join(sFlat8,sFlat7)),
inference(step,[status(thm)],[t110431,t80564]) ).
cnf(t110433,plain,
meet(c,join(sFlat1,sFlat5)) = meet(c,join(sFlat7,sFlat8)),
inference(step,[status(thm)],[t110432,t78]) ).
cnf(t102,plain,
sFlat7 = meet(sFlat7,sFlat8),
inference(cp,[status(thm)],[t20,t101]) ).
cnf(t122,plain,
meet(sFlat7,sFlat8) = sFlat7,
inference(orient,[status(thm)],[t102]) ).
cnf(t146,plain,
sFlat8 = join(sFlat8,sFlat7),
inference(cp,[status(thm)],[t141,t122]) ).
cnf(t109585,plain,
sFlat8 = join(sFlat7,sFlat8),
inference(step,[status(thm)],[t146,t78]) ).
cnf(t153,plain,
join(sFlat7,sFlat8) = sFlat8,
inference(orient,[status(thm)],[t109585]) ).
cnf(t110434,plain,
meet(c,join(sFlat1,sFlat5)) = meet(c,sFlat8),
inference(step,[status(thm)],[t110433,t153]) ).
cnf(t110435,plain,
meet(c,join(sFlat1,sFlat5)) = meet(sFlat8,c),
inference(step,[status(thm)],[t110434,t23]) ).
cnf(t109390,plain,
meet(c,join(sFlat1,sFlat5)) = meet(sFlat8,c),
inference(orient,[status(thm)],[t110435]) ).
cnf(t109396,plain,
meet(sFlat4,join(sFlat1,sFlat5)) = meet(sFlat4,meet(sFlat8,c)),
inference(cp,[status(thm)],[t43007,t109390]) ).
cnf(t1836,plain,
meet(X1,join(X2,join(X1,X3))) = meet(X1,join(X1,X3)),
inference(cp,[status(thm)],[t1830,t188]) ).
cnf(t109888,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(step,[status(thm)],[t1836,t20]) ).
cnf(t11039,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t109888]) ).
cnf(t103,plain,
join(sFlat7,join(b,X1)) = join(sFlat8,X1),
inference(cp,[status(thm)],[t83,t101]) ).
cnf(t418,plain,
join(sFlat7,join(b,X1)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t103]) ).
cnf(t419,plain,
join(sFlat8,meet(sFlat3,c)) = join(sFlat7,sFlat5),
inference(cp,[status(thm)],[t418,t97]) ).
cnf(t109664,plain,
join(sFlat8,meet(sFlat3,c)) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t419,t78]) ).
cnf(t1782,plain,
join(sFlat8,meet(sFlat3,c)) = join(sFlat5,sFlat7),
inference(orient,[status(thm)],[t109664]) ).
cnf(t241,plain,
sFlat1 = meet(sFlat1,sFlat3),
inference(cp,[status(thm)],[t20,t240]) ).
cnf(t245,plain,
meet(sFlat1,sFlat3) = sFlat1,
inference(orient,[status(thm)],[t241]) ).
cnf(t247,plain,
meet(sFlat1,meet(sFlat3,X1)) = meet(sFlat1,X1),
inference(cp,[status(thm)],[t25,t245]) ).
cnf(t1457,plain,
meet(sFlat1,meet(sFlat3,X1)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t247]) ).
cnf(t196,plain,
meet(sFlat3,c) = meet(meet(sFlat3,c),sFlat5),
inference(cp,[status(thm)],[t188,t97]) ).
cnf(t109627,plain,
meet(sFlat3,c) = meet(sFlat3,meet(c,sFlat5)),
inference(step,[status(thm)],[t196,t25]) ).
cnf(t109628,plain,
meet(sFlat3,c) = meet(sFlat3,meet(sFlat5,c)),
inference(step,[status(thm)],[t109627,t23]) ).
cnf(t966,plain,
meet(sFlat3,meet(sFlat5,c)) = meet(sFlat3,c),
inference(orient,[status(thm)],[t109628]) ).
cnf(t1459,plain,
meet(sFlat1,meet(sFlat5,c)) = meet(sFlat1,meet(sFlat3,c)),
inference(cp,[status(thm)],[t1457,t966]) ).
cnf(t109746,plain,
meet(sFlat1,meet(sFlat5,c)) = meet(sFlat1,c),
inference(step,[status(thm)],[t1459,t1457]) ).
cnf(t109659,plain,
meet(sFlat1,c) = sFlat7,
inference(step,[status(thm)],[t1741,t1749]) ).
cnf(t1750,plain,
meet(sFlat1,c) = sFlat7,
inference(orient,[status(thm)],[t109659]) ).
cnf(t109747,plain,
meet(sFlat1,meet(sFlat5,c)) = sFlat7,
inference(step,[status(thm)],[t109746,t1750]) ).
cnf(t3421,plain,
meet(sFlat1,meet(sFlat5,c)) = sFlat7,
inference(orient,[status(thm)],[t109747]) ).
cnf(t31,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t25,t23]) ).
cnf(t109702,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t31,t25]) ).
cnf(t2496,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t109702]) ).
cnf(t2533,plain,
meet(sFlat1,meet(X1,c)) = meet(X1,sFlat7),
inference(cp,[status(thm)],[t2496,t1750]) ).
cnf(t5019,plain,
meet(sFlat1,meet(X1,c)) = meet(X1,sFlat7),
inference(orient,[status(thm)],[t2533]) ).
cnf(t109772,plain,
meet(sFlat5,sFlat7) = sFlat7,
inference(step,[status(thm)],[t3421,t5019]) ).
cnf(t5042,plain,
meet(sFlat5,sFlat7) = sFlat7,
inference(rw,[status(thm)],[t109772]) ).
cnf(t5043,plain,
meet(sFlat5,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t5042]) ).
cnf(t5050,plain,
sFlat5 = join(sFlat5,sFlat7),
inference(cp,[status(thm)],[t22,t5043]) ).
cnf(t5058,plain,
join(sFlat5,sFlat7) = sFlat5,
inference(orient,[status(thm)],[t5050]) ).
cnf(t109773,plain,
join(sFlat8,meet(sFlat3,c)) = sFlat5,
inference(step,[status(thm)],[t1782,t5058]) ).
cnf(t5059,plain,
join(sFlat8,meet(sFlat3,c)) = sFlat5,
inference(orient,[status(thm)],[t109773]) ).
cnf(t110041,plain,
join(sFlat8,sFlat4) = sFlat5,
inference(step,[status(thm)],[t5059,t37830]) ).
cnf(t37884,plain,
join(sFlat8,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t110041]) ).
cnf(t110064,plain,
join(sFlat4,sFlat8) = sFlat5,
inference(step,[status(thm)],[t37884,t78]) ).
cnf(t38201,plain,
join(sFlat4,sFlat8) = sFlat5,
inference(orient,[status(thm)],[t110064]) ).
cnf(t38228,plain,
sFlat4 = meet(sFlat4,join(X1,sFlat5)),
inference(cp,[status(thm)],[t11039,t38201]) ).
cnf(t38977,plain,
meet(sFlat4,join(X1,sFlat5)) = sFlat4,
inference(orient,[status(thm)],[t38228]) ).
cnf(t110436,plain,
sFlat4 = meet(sFlat4,meet(sFlat8,c)),
inference(step,[status(thm)],[t109396,t38977]) ).
cnf(t190,plain,
meet(X1,X2) = meet(meet(X1,X2),X1),
inference(cp,[status(thm)],[t188,t22]) ).
cnf(t109626,plain,
meet(X1,X2) = meet(X1,meet(X2,X1)),
inference(step,[status(thm)],[t190,t25]) ).
cnf(t926,plain,
meet(X1,meet(X2,X1)) = meet(X1,X2),
inference(orient,[status(thm)],[t109626]) ).
cnf(t1834,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(join(X1,X3),X2)),
inference(cp,[status(thm)],[t1830,t926]) ).
cnf(t110020,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(step,[status(thm)],[t1834,t1830]) ).
cnf(t29759,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t110020]) ).
cnf(t38134,plain,
meet(sFlat4,X1) = meet(sFlat4,meet(X1,c)),
inference(cp,[status(thm)],[t29759,t38121]) ).
cnf(t43063,plain,
meet(sFlat4,meet(X1,c)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t38134]) ).
cnf(t110437,plain,
sFlat4 = meet(sFlat4,sFlat8),
inference(step,[status(thm)],[t110436,t43063]) ).
cnf(t109450,plain,
meet(sFlat4,sFlat8) = sFlat4,
inference(orient,[status(thm)],[t110437]) ).
cnf(t109464,plain,
sFlat8 = join(sFlat8,sFlat4),
inference(cp,[status(thm)],[t141,t109450]) ).
cnf(t110441,plain,
sFlat8 = join(sFlat4,sFlat8),
inference(step,[status(thm)],[t109464,t78]) ).
cnf(t110442,plain,
sFlat8 = sFlat5,
inference(step,[status(thm)],[t110441,t38201]) ).
cnf(t109491,plain,
sFlat8 = sFlat5,
inference(orient,[status(thm)],[t110442]) ).
cnf(t110443,plain,
join(sFlat7,b) = sFlat5,
inference(step,[status(thm)],[t101,t109491]) ).
cnf(t109492,plain,
join(sFlat7,b) = sFlat5,
inference(orient,[status(thm)],[t110443]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(b,meet(c,join(meet(a,join(b,c)),meet(b,c))))) != meet(a,join(b,meet(a,c))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(b,meet(c,join(meet(b,c),meet(a,join(b,c)))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[goal_0,t78]) ).
cnf(g0_1,plain,
meet(a,join(b,meet(c,join(meet(c,b),meet(a,join(b,c)))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_0,t23]) ).
cnf(g0_2,plain,
meet(a,join(b,meet(c,join(sFlat2,meet(a,join(b,c)))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_1,t52]) ).
cnf(g0_3,plain,
meet(a,join(b,meet(c,join(sFlat2,meet(a,join(c,b)))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_2,t78]) ).
cnf(g0_4,plain,
meet(a,join(b,meet(c,join(sFlat2,meet(a,sFlat0))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_3,t105]) ).
cnf(g0_5,plain,
meet(a,join(b,meet(c,join(sFlat2,meet(sFlat0,a))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_4,t23]) ).
cnf(g0_6,plain,
meet(a,join(b,meet(c,join(sFlat2,sFlat1)))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_5,t220]) ).
cnf(g0_7,plain,
meet(a,join(b,meet(c,join(sFlat1,sFlat2)))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_6,t78]) ).
cnf(g0_8,plain,
meet(a,join(b,meet(c,sFlat3))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_7,t240]) ).
cnf(g0_9,plain,
meet(a,join(b,meet(sFlat3,c))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_8,t23]) ).
cnf(g0_10,plain,
meet(a,join(b,sFlat4)) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_9,t37830]) ).
cnf(g0_11,plain,
meet(a,join(sFlat4,b)) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_10,t78]) ).
cnf(g0_12,plain,
meet(a,sFlat5) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_11,t38275]) ).
cnf(g0_13,plain,
meet(a,sFlat5) != meet(a,join(b,meet(c,a))),
inference(rw,[status(thm)],[g0_12,t23]) ).
cnf(g0_14,plain,
meet(a,sFlat5) != meet(a,join(b,sFlat7)),
inference(rw,[status(thm)],[g0_13,t73]) ).
cnf(g0_15,plain,
meet(a,sFlat5) != meet(a,join(sFlat7,b)),
inference(rw,[status(thm)],[g0_14,t78]) ).
cnf(g0_16,plain,
meet(a,sFlat5) != meet(a,sFlat5),
inference(rw,[status(thm)],[g0_15,t109492]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT155-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/10.37 % Computer : n020.cluster.edu
% 0.09/10.37 % Model : x86_64 x86_64
% 0.09/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.37 % Memory : 8046.5625MB
% 0.09/10.37 % OS : Linux 6.8.0-71-generic
% 0.09/10.37 % CPULimit : 300
% 0.09/10.37 % WCLimit : 300
% 0.09/10.37 % DateTime : Wed Sep 23 20:25:14 UTC 2026
% 0.09/10.37 % CPUTime :
% 0.09/10.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 39.87/15.47 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 39.87/15.47 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------