%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT023-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.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:01 PM UTC 2026
% Result : Unsatisfiable 29.38s 4.24s
% Output : CNFRefutation 29.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 15
% Syntax : Number of clauses : 302 ( 302 unt; 0 nHn; 185 RR)
% Number of literals : 302 ( 301 equ; 13 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 : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 200 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t3,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t9,axiom,
sFlat0 = meet(a,c),
introduced(definition) ).
cnf(t6508,plain,
sFlat0 = meet(c,a),
inference(step,[status(thm)],[t9,t16]) ).
cnf(t46,plain,
meet(c,a) = sFlat0,
inference(orient,[status(thm)],[t6508]) ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t51,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t10,axiom,
sFlat1 = join(b,meet(a,c)),
introduced(definition) ).
cnf(t6517,plain,
sFlat1 = join(b,meet(c,a)),
inference(step,[status(thm)],[t10,t16]) ).
cnf(t6518,plain,
sFlat1 = join(b,sFlat0),
inference(step,[status(thm)],[t6517,t46]) ).
cnf(t6519,plain,
sFlat1 = join(sFlat0,b),
inference(step,[status(thm)],[t6518,t51]) ).
cnf(t74,plain,
join(sFlat0,b) = sFlat1,
inference(orient,[status(thm)],[t6519]) ).
cnf(t11,axiom,
sFlat2 = meet(a,join(b,meet(a,c))),
introduced(definition) ).
cnf(t6506,plain,
sFlat2 = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t11,t16]) ).
cnf(t37,plain,
meet(a,join(b,meet(c,a))) = sFlat2,
inference(orient,[status(thm)],[t6506]) ).
cnf(t6509,plain,
meet(a,join(b,sFlat0)) = sFlat2,
inference(step,[status(thm)],[t37,t46]) ).
cnf(t50,plain,
meet(a,join(b,sFlat0)) = sFlat2,
inference(rw,[status(thm)],[t6509]) ).
cnf(t6527,plain,
meet(a,join(sFlat0,b)) = sFlat2,
inference(step,[status(thm)],[t50,t51]) ).
cnf(t6528,plain,
meet(a,sFlat1) = sFlat2,
inference(step,[status(thm)],[t6527,t74]) ).
cnf(t6529,plain,
meet(sFlat1,a) = sFlat2,
inference(step,[status(thm)],[t6528,t16]) ).
cnf(t91,plain,
meet(sFlat1,a) = sFlat2,
inference(orient,[status(thm)],[t6529]) ).
cnf(t12,axiom,
sFlat3 = meet(a,b),
introduced(definition) ).
cnf(t6507,plain,
sFlat3 = meet(b,a),
inference(step,[status(thm)],[t12,t16]) ).
cnf(t42,plain,
meet(b,a) = sFlat3,
inference(orient,[status(thm)],[t6507]) ).
cnf(t13,axiom,
sFlat4 = join(meet(a,b),meet(a,c)),
introduced(definition) ).
cnf(t6512,plain,
sFlat4 = join(meet(a,c),meet(a,b)),
inference(step,[status(thm)],[t13,t51]) ).
cnf(t6513,plain,
sFlat4 = join(meet(c,a),meet(a,b)),
inference(step,[status(thm)],[t6512,t16]) ).
cnf(t6514,plain,
sFlat4 = join(sFlat0,meet(a,b)),
inference(step,[status(thm)],[t6513,t46]) ).
cnf(t6515,plain,
sFlat4 = join(sFlat0,meet(b,a)),
inference(step,[status(thm)],[t6514,t16]) ).
cnf(t6516,plain,
sFlat4 = join(sFlat0,sFlat3),
inference(step,[status(thm)],[t6515,t42]) ).
cnf(t70,plain,
join(sFlat0,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t6516]) ).
cnf(t7,axiom,
join(meet(join(X1,X2),X3),X2) = join(meet(join(X3,X2),X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t6510,plain,
join(X2,meet(join(X1,X2),X3)) = join(meet(join(X3,X2),X1),X2),
inference(step,[status(thm)],[t7,t51]) ).
cnf(t6511,plain,
join(X2,meet(join(X1,X2),X3)) = join(X2,meet(join(X3,X2),X1)),
inference(step,[status(thm)],[t6510,t51]) ).
cnf(t61,plain,
join(X1,meet(join(X2,X1),X3)) = join(X1,meet(join(X3,X1),X2)),
inference(orient,[status(thm)],[t6511]) ).
cnf(t65,plain,
join(X1,meet(join(X2,X1),X3)) = join(X1,meet(join(X1,X3),X2)),
inference(cp,[status(thm)],[t61,t51]) ).
cnf(t646,plain,
join(X1,meet(join(X2,X1),X3)) = join(X1,meet(join(X1,X3),X2)),
inference(orient,[status(thm)],[t65]) ).
cnf(t4,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t54,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t4]) ).
cnf(t71,plain,
join(sFlat0,join(sFlat3,X1)) = join(sFlat4,X1),
inference(cp,[status(thm)],[t54,t70]) ).
cnf(t129,plain,
join(sFlat0,join(sFlat3,X1)) = join(sFlat4,X1),
inference(orient,[status(thm)],[t71]) ).
cnf(t132,plain,
join(sFlat4,X1) = join(sFlat0,join(X1,sFlat3)),
inference(cp,[status(thm)],[t129,t51]) ).
cnf(t231,plain,
join(sFlat0,join(X1,sFlat3)) = join(sFlat4,X1),
inference(orient,[status(thm)],[t132]) ).
cnf(t75,plain,
join(sFlat0,join(b,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t54,t74]) ).
cnf(t141,plain,
join(sFlat0,join(b,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t75]) ).
cnf(t232,plain,
join(sFlat4,b) = join(sFlat1,sFlat3),
inference(cp,[status(thm)],[t231,t141]) ).
cnf(t237,plain,
join(sFlat4,b) = join(sFlat1,sFlat3),
inference(orient,[status(thm)],[t232]) ).
cnf(t678,plain,
join(sFlat4,meet(join(X1,sFlat4),b)) = join(sFlat4,meet(join(sFlat1,sFlat3),X1)),
inference(cp,[status(thm)],[t646,t237]) ).
cnf(t7030,plain,
join(sFlat4,meet(b,join(X1,sFlat4))) = join(sFlat4,meet(join(sFlat1,sFlat3),X1)),
inference(step,[status(thm)],[t678,t16]) ).
cnf(t77,plain,
join(b,meet(join(X1,b),sFlat0)) = join(b,meet(sFlat1,X1)),
inference(cp,[status(thm)],[t61,t74]) ).
cnf(t6657,plain,
join(b,meet(sFlat0,join(X1,b))) = join(b,meet(sFlat1,X1)),
inference(step,[status(thm)],[t77,t16]) ).
cnf(t797,plain,
join(b,meet(sFlat0,join(X1,b))) = join(b,meet(sFlat1,X1)),
inference(orient,[status(thm)],[t6657]) ).
cnf(t803,plain,
join(sFlat1,meet(sFlat0,join(X1,b))) = join(sFlat0,join(b,meet(sFlat1,X1))),
inference(cp,[status(thm)],[t141,t797]) ).
cnf(t6688,plain,
join(sFlat1,meet(sFlat0,join(X1,b))) = join(sFlat1,meet(sFlat1,X1)),
inference(step,[status(thm)],[t803,t141]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t15,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t63,plain,
join(X1,meet(join(X2,X1),X1)) = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t61,t15]) ).
cnf(t6612,plain,
join(X1,meet(X1,join(X2,X1))) = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t63,t16]) ).
cnf(t385,plain,
join(X1,meet(X1,join(X2,X1))) = join(X1,meet(X1,X2)),
inference(orient,[status(thm)],[t6612]) ).
cnf(t405,plain,
join(X1,meet(X1,X2)) = join(X1,meet(X1,join(X1,X2))),
inference(cp,[status(thm)],[t385,t51]) ).
cnf(t6,axiom,
join(meet(X1,join(X2,X3)),meet(X1,X2)) = meet(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
join(meet(X1,join(X2,X3)),meet(X1,X2)) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t14,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t25,plain,
meet(X1,join(X1,X2)) = join(meet(X1,join(X1,X2)),X1),
inference(cp,[status(thm)],[t22,t14]) ).
cnf(t6606,plain,
meet(X1,join(X1,X2)) = join(X1,meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t25,t51]) ).
cnf(t317,plain,
join(X1,meet(X1,join(X1,X2))) = meet(X1,join(X1,X2)),
inference(orient,[status(thm)],[t6606]) ).
cnf(t6613,plain,
join(X1,meet(X1,X2)) = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t405,t317]) ).
cnf(t418,plain,
join(X1,meet(X1,X2)) = meet(X1,join(X1,X2)),
inference(orient,[status(thm)],[t6613]) ).
cnf(t6689,plain,
join(sFlat1,meet(sFlat0,join(X1,b))) = meet(sFlat1,join(sFlat1,X1)),
inference(step,[status(thm)],[t6688,t418]) ).
cnf(t1038,plain,
join(sFlat1,meet(sFlat0,join(X1,b))) = meet(sFlat1,join(sFlat1,X1)),
inference(orient,[status(thm)],[t6689]) ).
cnf(t5,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t5]) ).
cnf(t47,plain,
meet(c,meet(a,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t17,t46]) ).
cnf(t121,plain,
meet(c,meet(a,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t47]) ).
cnf(t20,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t17,t14]) ).
cnf(t78,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t20]) ).
cnf(t123,plain,
meet(sFlat0,meet(a,X1)) = meet(c,meet(a,X1)),
inference(cp,[status(thm)],[t121,t78]) ).
cnf(t6553,plain,
meet(sFlat0,meet(a,X1)) = meet(sFlat0,X1),
inference(step,[status(thm)],[t123,t121]) ).
cnf(t187,plain,
meet(sFlat0,meet(a,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t6553]) ).
cnf(t8,axiom,
meet(join(X1,meet(X2,X3)),join(X1,X2)) = join(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t6505,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t8,t16]) ).
cnf(t27,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t6505]) ).
cnf(t30,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(join(meet(X1,X2),X1),meet(X1,X2)),
inference(cp,[status(thm)],[t27,t15]) ).
cnf(t6699,plain,
meet(X1,X2) = meet(join(meet(X1,X2),X1),meet(X1,X2)),
inference(step,[status(thm)],[t30,t15]) ).
cnf(t21,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t17,t16]) ).
cnf(t6538,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t21,t17]) ).
cnf(t155,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t6538]) ).
cnf(t6700,plain,
meet(X1,X2) = meet(X1,meet(join(meet(X1,X2),X1),X2)),
inference(step,[status(thm)],[t6699,t155]) ).
cnf(t6701,plain,
meet(X1,X2) = meet(X1,meet(X2,join(meet(X1,X2),X1))),
inference(step,[status(thm)],[t6700,t16]) ).
cnf(t6702,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,meet(X1,X2)))),
inference(step,[status(thm)],[t6701,t51]) ).
cnf(t6703,plain,
meet(X1,X2) = meet(X1,meet(X2,meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t6702,t418]) ).
cnf(t1137,plain,
meet(X1,meet(X2,meet(X1,join(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t6703]) ).
cnf(t1139,plain,
meet(X1,X2) = meet(X2,meet(X1,meet(X1,join(X1,X2)))),
inference(cp,[status(thm)],[t1137,t155]) ).
cnf(t6704,plain,
meet(X1,X2) = meet(X2,meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t1139,t78]) ).
cnf(t1205,plain,
meet(X1,meet(X2,join(X2,X1))) = meet(X2,X1),
inference(orient,[status(thm)],[t6704]) ).
cnf(t444,plain,
meet(b,join(b,a)) = join(b,sFlat3),
inference(cp,[status(thm)],[t418,t42]) ).
cnf(t6624,plain,
meet(b,join(b,a)) = join(sFlat3,b),
inference(step,[status(thm)],[t444,t51]) ).
cnf(t478,plain,
meet(b,join(b,a)) = join(sFlat3,b),
inference(orient,[status(thm)],[t6624]) ).
cnf(t1216,plain,
meet(b,a) = meet(a,join(sFlat3,b)),
inference(cp,[status(thm)],[t1205,t478]) ).
cnf(t6722,plain,
sFlat3 = meet(a,join(sFlat3,b)),
inference(step,[status(thm)],[t1216,t42]) ).
cnf(t1566,plain,
meet(a,join(sFlat3,b)) = sFlat3,
inference(orient,[status(thm)],[t6722]) ).
cnf(t1569,plain,
meet(sFlat0,join(sFlat3,b)) = meet(sFlat0,sFlat3),
inference(cp,[status(thm)],[t187,t1566]) ).
cnf(t1658,plain,
meet(sFlat0,join(sFlat3,b)) = meet(sFlat0,sFlat3),
inference(orient,[status(thm)],[t1569]) ).
cnf(t1660,plain,
meet(sFlat1,join(sFlat1,sFlat3)) = join(sFlat1,meet(sFlat0,sFlat3)),
inference(cp,[status(thm)],[t1038,t1658]) ).
cnf(t45,plain,
join(X1,meet(b,a)) = meet(join(X1,b),join(X1,sFlat3)),
inference(cp,[status(thm)],[t27,t42]) ).
cnf(t6589,plain,
join(X1,sFlat3) = meet(join(X1,b),join(X1,sFlat3)),
inference(step,[status(thm)],[t45,t42]) ).
cnf(t6590,plain,
join(X1,sFlat3) = meet(join(X1,sFlat3),join(X1,b)),
inference(step,[status(thm)],[t6589,t16]) ).
cnf(t291,plain,
meet(join(X1,sFlat3),join(X1,b)) = join(X1,sFlat3),
inference(orient,[status(thm)],[t6590]) ).
cnf(t142,plain,
join(sFlat1,b) = join(sFlat0,b),
inference(cp,[status(thm)],[t141,t15]) ).
cnf(t6537,plain,
join(sFlat1,b) = sFlat1,
inference(step,[status(thm)],[t142,t74]) ).
cnf(t149,plain,
join(sFlat1,b) = sFlat1,
inference(orient,[status(thm)],[t6537]) ).
cnf(t298,plain,
join(sFlat1,sFlat3) = meet(join(sFlat1,sFlat3),sFlat1),
inference(cp,[status(thm)],[t291,t149]) ).
cnf(t6599,plain,
join(sFlat1,sFlat3) = meet(sFlat1,join(sFlat1,sFlat3)),
inference(step,[status(thm)],[t298,t16]) ).
cnf(t307,plain,
meet(sFlat1,join(sFlat1,sFlat3)) = join(sFlat1,sFlat3),
inference(orient,[status(thm)],[t6599]) ).
cnf(t6731,plain,
join(sFlat1,sFlat3) = join(sFlat1,meet(sFlat0,sFlat3)),
inference(step,[status(thm)],[t1660,t307]) ).
cnf(t798,plain,
join(b,meet(sFlat1,b)) = join(b,meet(sFlat0,b)),
inference(cp,[status(thm)],[t797,t15]) ).
cnf(t43,plain,
meet(b,meet(a,X1)) = meet(sFlat3,X1),
inference(cp,[status(thm)],[t17,t42]) ).
cnf(t113,plain,
meet(b,meet(a,X1)) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t43]) ).
cnf(t116,plain,
meet(sFlat3,X1) = meet(b,meet(X1,a)),
inference(cp,[status(thm)],[t113,t16]) ).
cnf(t172,plain,
meet(b,meet(X1,a)) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t116]) ).
cnf(t122,plain,
meet(sFlat0,a) = meet(c,a),
inference(cp,[status(thm)],[t121,t14]) ).
cnf(t6534,plain,
meet(sFlat0,a) = sFlat0,
inference(step,[status(thm)],[t122,t46]) ).
cnf(t127,plain,
meet(sFlat0,a) = sFlat0,
inference(orient,[status(thm)],[t6534]) ).
cnf(t175,plain,
meet(sFlat3,sFlat0) = meet(b,sFlat0),
inference(cp,[status(thm)],[t172,t127]) ).
cnf(t6544,plain,
meet(sFlat0,sFlat3) = meet(b,sFlat0),
inference(step,[status(thm)],[t175,t16]) ).
cnf(t6545,plain,
meet(sFlat0,sFlat3) = meet(sFlat0,b),
inference(step,[status(thm)],[t6544,t16]) ).
cnf(t181,plain,
meet(sFlat0,b) = meet(sFlat0,sFlat3),
inference(orient,[status(thm)],[t6545]) ).
cnf(t6658,plain,
join(b,meet(sFlat1,b)) = join(b,meet(sFlat0,sFlat3)),
inference(step,[status(thm)],[t798,t181]) ).
cnf(t809,plain,
join(b,meet(sFlat1,b)) = join(b,meet(sFlat0,sFlat3)),
inference(orient,[status(thm)],[t6658]) ).
cnf(t811,plain,
join(sFlat1,meet(sFlat1,b)) = join(sFlat0,join(b,meet(sFlat0,sFlat3))),
inference(cp,[status(thm)],[t141,t809]) ).
cnf(t6659,plain,
meet(sFlat1,join(sFlat1,b)) = join(sFlat0,join(b,meet(sFlat0,sFlat3))),
inference(step,[status(thm)],[t811,t418]) ).
cnf(t6660,plain,
meet(sFlat1,sFlat1) = join(sFlat0,join(b,meet(sFlat0,sFlat3))),
inference(step,[status(thm)],[t6659,t149]) ).
cnf(t6661,plain,
sFlat1 = join(sFlat0,join(b,meet(sFlat0,sFlat3))),
inference(step,[status(thm)],[t6660,t14]) ).
cnf(t6662,plain,
sFlat1 = join(sFlat1,meet(sFlat0,sFlat3)),
inference(step,[status(thm)],[t6661,t141]) ).
cnf(t817,plain,
join(sFlat1,meet(sFlat0,sFlat3)) = sFlat1,
inference(orient,[status(thm)],[t6662]) ).
cnf(t6732,plain,
join(sFlat1,sFlat3) = sFlat1,
inference(step,[status(thm)],[t6731,t817]) ).
cnf(t1663,plain,
join(sFlat1,sFlat3) = sFlat1,
inference(orient,[status(thm)],[t6732]) ).
cnf(t7031,plain,
join(sFlat4,meet(b,join(X1,sFlat4))) = join(sFlat4,meet(sFlat1,X1)),
inference(step,[status(thm)],[t7030,t1663]) ).
cnf(t5938,plain,
join(sFlat4,meet(b,join(X1,sFlat4))) = join(sFlat4,meet(sFlat1,X1)),
inference(orient,[status(thm)],[t7031]) ).
cnf(t39,plain,
meet(a,join(b,meet(c,a))) = join(sFlat2,meet(a,b)),
inference(cp,[status(thm)],[t22,t37]) ).
cnf(t6524,plain,
sFlat2 = join(sFlat2,meet(a,b)),
inference(step,[status(thm)],[t39,t37]) ).
cnf(t6525,plain,
sFlat2 = join(sFlat2,meet(b,a)),
inference(step,[status(thm)],[t6524,t16]) ).
cnf(t6526,plain,
sFlat2 = join(sFlat2,sFlat3),
inference(step,[status(thm)],[t6525,t42]) ).
cnf(t87,plain,
join(sFlat2,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t6526]) ).
cnf(t233,plain,
join(sFlat4,sFlat2) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t231,t87]) ).
cnf(t6568,plain,
join(sFlat2,sFlat4) = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t233,t51]) ).
cnf(t242,plain,
join(sFlat2,sFlat4) = join(sFlat0,sFlat2),
inference(orient,[status(thm)],[t6568]) ).
cnf(t53,plain,
join(meet(X1,join(X2,X3)),meet(X1,X2)) = meet(X1,join(X2,X3)),
inference(rw,[status(thm)],[t22]) ).
cnf(t6957,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t53,t51]) ).
cnf(t4691,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6957]) ).
cnf(t6733,plain,
join(sFlat4,b) = sFlat1,
inference(step,[status(thm)],[t237,t1663]) ).
cnf(t1664,plain,
join(sFlat4,b) = sFlat1,
inference(orient,[status(thm)],[t6733]) ).
cnf(t4895,plain,
meet(X1,join(sFlat4,b)) = join(meet(X1,sFlat4),meet(X1,sFlat1)),
inference(cp,[status(thm)],[t4691,t1664]) ).
cnf(t6962,plain,
meet(X1,sFlat1) = join(meet(X1,sFlat4),meet(X1,sFlat1)),
inference(step,[status(thm)],[t4895,t1664]) ).
cnf(t6963,plain,
meet(X1,sFlat1) = join(meet(X1,sFlat1),meet(X1,sFlat4)),
inference(step,[status(thm)],[t6962,t51]) ).
cnf(t4987,plain,
join(meet(X1,sFlat1),meet(X1,sFlat4)) = meet(X1,sFlat1),
inference(orient,[status(thm)],[t6963]) ).
cnf(t33,plain,
meet(join(X1,X2),meet(join(X1,meet(X2,X3)),Y3)) = meet(join(X1,meet(X2,X3)),Y3),
inference(cp,[status(thm)],[t17,t27]) ).
cnf(t3269,plain,
meet(join(X1,X2),meet(join(X1,meet(X2,X3)),Y3)) = meet(join(X1,meet(X2,X3)),Y3),
inference(orient,[status(thm)],[t33]) ).
cnf(t73,plain,
join(sFlat3,meet(join(X1,sFlat3),sFlat0)) = join(sFlat3,meet(sFlat4,X1)),
inference(cp,[status(thm)],[t61,t70]) ).
cnf(t6637,plain,
join(sFlat3,meet(sFlat0,join(X1,sFlat3))) = join(sFlat3,meet(sFlat4,X1)),
inference(step,[status(thm)],[t73,t16]) ).
cnf(t746,plain,
join(sFlat3,meet(sFlat0,join(X1,sFlat3))) = join(sFlat3,meet(sFlat4,X1)),
inference(orient,[status(thm)],[t6637]) ).
cnf(t748,plain,
join(sFlat3,meet(sFlat4,sFlat2)) = join(sFlat3,meet(sFlat0,sFlat2)),
inference(cp,[status(thm)],[t746,t87]) ).
cnf(t6643,plain,
join(sFlat3,meet(sFlat2,sFlat4)) = join(sFlat3,meet(sFlat0,sFlat2)),
inference(step,[status(thm)],[t748,t16]) ).
cnf(t124,plain,
meet(sFlat0,X1) = meet(c,meet(X1,a)),
inference(cp,[status(thm)],[t121,t16]) ).
cnf(t188,plain,
meet(c,meet(X1,a)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t124]) ).
cnf(t92,plain,
meet(sFlat1,meet(a,X1)) = meet(sFlat2,X1),
inference(cp,[status(thm)],[t17,t91]) ).
cnf(t166,plain,
meet(sFlat1,meet(a,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t92]) ).
cnf(t167,plain,
meet(sFlat2,a) = meet(sFlat1,a),
inference(cp,[status(thm)],[t166,t14]) ).
cnf(t6540,plain,
meet(sFlat2,a) = sFlat2,
inference(step,[status(thm)],[t167,t91]) ).
cnf(t170,plain,
meet(sFlat2,a) = sFlat2,
inference(orient,[status(thm)],[t6540]) ).
cnf(t189,plain,
meet(sFlat0,sFlat2) = meet(c,sFlat2),
inference(cp,[status(thm)],[t188,t170]) ).
cnf(t6555,plain,
meet(sFlat0,sFlat2) = meet(sFlat2,c),
inference(step,[status(thm)],[t189,t16]) ).
cnf(t190,plain,
meet(sFlat0,sFlat1) = meet(c,sFlat2),
inference(cp,[status(thm)],[t188,t91]) ).
cnf(t6554,plain,
meet(sFlat0,sFlat1) = meet(sFlat2,c),
inference(step,[status(thm)],[t190,t16]) ).
cnf(t192,plain,
meet(sFlat2,c) = meet(sFlat0,sFlat1),
inference(orient,[status(thm)],[t6554]) ).
cnf(t6556,plain,
meet(sFlat0,sFlat2) = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t6555,t192]) ).
cnf(t195,plain,
meet(sFlat0,sFlat2) = meet(sFlat0,sFlat1),
inference(orient,[status(thm)],[t6556]) ).
cnf(t6644,plain,
join(sFlat3,meet(sFlat2,sFlat4)) = join(sFlat3,meet(sFlat0,sFlat1)),
inference(step,[status(thm)],[t6643,t195]) ).
cnf(t763,plain,
join(sFlat3,meet(sFlat2,sFlat4)) = join(sFlat3,meet(sFlat0,sFlat1)),
inference(orient,[status(thm)],[t6644]) ).
cnf(t1672,plain,
join(sFlat3,meet(sFlat4,sFlat1)) = join(sFlat3,meet(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t746,t1663]) ).
cnf(t6760,plain,
join(sFlat3,meet(sFlat1,sFlat4)) = join(sFlat3,meet(sFlat0,sFlat1)),
inference(step,[status(thm)],[t1672,t16]) ).
cnf(t294,plain,
join(sFlat0,sFlat3) = meet(sFlat4,join(sFlat0,b)),
inference(cp,[status(thm)],[t291,t70]) ).
cnf(t6591,plain,
sFlat4 = meet(sFlat4,join(sFlat0,b)),
inference(step,[status(thm)],[t294,t70]) ).
cnf(t6592,plain,
sFlat4 = meet(sFlat4,sFlat1),
inference(step,[status(thm)],[t6591,t74]) ).
cnf(t6593,plain,
sFlat4 = meet(sFlat1,sFlat4),
inference(step,[status(thm)],[t6592,t16]) ).
cnf(t301,plain,
meet(sFlat1,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t6593]) ).
cnf(t6761,plain,
join(sFlat3,sFlat4) = join(sFlat3,meet(sFlat0,sFlat1)),
inference(step,[status(thm)],[t6760,t301]) ).
cnf(t130,plain,
join(sFlat4,sFlat3) = join(sFlat0,sFlat3),
inference(cp,[status(thm)],[t129,t15]) ).
cnf(t6535,plain,
join(sFlat3,sFlat4) = join(sFlat0,sFlat3),
inference(step,[status(thm)],[t130,t51]) ).
cnf(t6536,plain,
join(sFlat3,sFlat4) = sFlat4,
inference(step,[status(thm)],[t6535,t70]) ).
cnf(t137,plain,
join(sFlat3,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t6536]) ).
cnf(t6762,plain,
sFlat4 = join(sFlat3,meet(sFlat0,sFlat1)),
inference(step,[status(thm)],[t6761,t137]) ).
cnf(t1847,plain,
join(sFlat3,meet(sFlat0,sFlat1)) = sFlat4,
inference(orient,[status(thm)],[t6762]) ).
cnf(t6763,plain,
join(sFlat3,meet(sFlat2,sFlat4)) = sFlat4,
inference(step,[status(thm)],[t763,t1847]) ).
cnf(t1848,plain,
join(sFlat3,meet(sFlat2,sFlat4)) = sFlat4,
inference(orient,[status(thm)],[t6763]) ).
cnf(t3349,plain,
meet(join(sFlat3,meet(sFlat2,sFlat4)),X1) = meet(join(sFlat3,sFlat2),meet(sFlat4,X1)),
inference(cp,[status(thm)],[t3269,t1848]) ).
cnf(t6862,plain,
meet(sFlat4,X1) = meet(join(sFlat3,sFlat2),meet(sFlat4,X1)),
inference(step,[status(thm)],[t3349,t1848]) ).
cnf(t6863,plain,
meet(sFlat4,X1) = meet(sFlat4,meet(join(sFlat3,sFlat2),X1)),
inference(step,[status(thm)],[t6862,t155]) ).
cnf(t6864,plain,
meet(sFlat4,X1) = meet(sFlat4,meet(join(sFlat2,sFlat3),X1)),
inference(step,[status(thm)],[t6863,t51]) ).
cnf(t6865,plain,
meet(sFlat4,X1) = meet(sFlat4,meet(sFlat2,X1)),
inference(step,[status(thm)],[t6864,t87]) ).
cnf(t6866,plain,
meet(sFlat4,X1) = meet(sFlat2,meet(sFlat4,X1)),
inference(step,[status(thm)],[t6865,t155]) ).
cnf(t3448,plain,
meet(sFlat2,meet(sFlat4,X1)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t6866]) ).
cnf(t1143,plain,
meet(X1,X2) = meet(X1,meet(X1,meet(X2,join(X1,X2)))),
inference(cp,[status(thm)],[t1137,t155]) ).
cnf(t6723,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t1143,t78]) ).
cnf(t1576,plain,
meet(X1,meet(X2,join(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6723]) ).
cnf(t3452,plain,
meet(sFlat4,join(sFlat2,sFlat4)) = meet(sFlat2,sFlat4),
inference(cp,[status(thm)],[t3448,t1576]) ).
cnf(t6867,plain,
meet(sFlat4,join(sFlat0,sFlat2)) = meet(sFlat2,sFlat4),
inference(step,[status(thm)],[t3452,t242]) ).
cnf(t765,plain,
join(sFlat4,meet(sFlat2,sFlat4)) = join(sFlat0,join(sFlat3,meet(sFlat0,sFlat1))),
inference(cp,[status(thm)],[t129,t763]) ).
cnf(t6645,plain,
join(sFlat4,meet(sFlat2,sFlat4)) = join(sFlat4,meet(sFlat0,sFlat1)),
inference(step,[status(thm)],[t765,t129]) ).
cnf(t23,plain,
meet(join(X1,X2),join(X1,X2)) = join(join(X1,X2),meet(join(X1,X2),X1)),
inference(cp,[status(thm)],[t22,t14]) ).
cnf(t6561,plain,
join(X1,X2) = join(join(X1,X2),meet(join(X1,X2),X1)),
inference(step,[status(thm)],[t23,t14]) ).
cnf(t6562,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X2),X1))),
inference(step,[status(thm)],[t6561,t54]) ).
cnf(t6563,plain,
join(X1,X2) = join(X1,join(X2,meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t6562,t16]) ).
cnf(t200,plain,
join(X1,join(X2,meet(X1,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t6563]) ).
cnf(t202,plain,
join(sFlat0,sFlat3) = join(sFlat4,meet(sFlat0,join(sFlat0,sFlat3))),
inference(cp,[status(thm)],[t200,t129]) ).
cnf(t6564,plain,
sFlat4 = join(sFlat4,meet(sFlat0,join(sFlat0,sFlat3))),
inference(step,[status(thm)],[t202,t70]) ).
cnf(t6565,plain,
sFlat4 = join(sFlat4,meet(sFlat0,sFlat4)),
inference(step,[status(thm)],[t6564,t70]) ).
cnf(t225,plain,
join(sFlat4,meet(sFlat0,sFlat4)) = sFlat4,
inference(orient,[status(thm)],[t6565]) ).
cnf(t437,plain,
meet(sFlat0,join(sFlat0,b)) = join(sFlat0,meet(sFlat0,sFlat3)),
inference(cp,[status(thm)],[t418,t181]) ).
cnf(t6616,plain,
meet(sFlat0,sFlat1) = join(sFlat0,meet(sFlat0,sFlat3)),
inference(step,[status(thm)],[t437,t74]) ).
cnf(t6617,plain,
meet(sFlat0,sFlat1) = meet(sFlat0,join(sFlat0,sFlat3)),
inference(step,[status(thm)],[t6616,t418]) ).
cnf(t6618,plain,
meet(sFlat0,sFlat1) = meet(sFlat0,sFlat4),
inference(step,[status(thm)],[t6617,t70]) ).
cnf(t460,plain,
meet(sFlat0,sFlat4) = meet(sFlat0,sFlat1),
inference(orient,[status(thm)],[t6618]) ).
cnf(t6619,plain,
join(sFlat4,meet(sFlat0,sFlat1)) = sFlat4,
inference(step,[status(thm)],[t225,t460]) ).
cnf(t461,plain,
join(sFlat4,meet(sFlat0,sFlat1)) = sFlat4,
inference(rw,[status(thm)],[t6619]) ).
cnf(t464,plain,
join(sFlat4,meet(sFlat0,sFlat1)) = sFlat4,
inference(orient,[status(thm)],[t461]) ).
cnf(t6646,plain,
join(sFlat4,meet(sFlat2,sFlat4)) = sFlat4,
inference(step,[status(thm)],[t6645,t464]) ).
cnf(t771,plain,
join(sFlat4,meet(sFlat2,sFlat4)) = sFlat4,
inference(orient,[status(thm)],[t6646]) ).
cnf(t773,plain,
join(sFlat4,meet(sFlat2,sFlat4)) = meet(join(sFlat4,sFlat2),sFlat4),
inference(cp,[status(thm)],[t27,t771]) ).
cnf(t6647,plain,
sFlat4 = meet(join(sFlat4,sFlat2),sFlat4),
inference(step,[status(thm)],[t773,t771]) ).
cnf(t6648,plain,
sFlat4 = meet(sFlat4,join(sFlat4,sFlat2)),
inference(step,[status(thm)],[t6647,t16]) ).
cnf(t6649,plain,
sFlat4 = meet(sFlat4,join(sFlat2,sFlat4)),
inference(step,[status(thm)],[t6648,t51]) ).
cnf(t6650,plain,
sFlat4 = meet(sFlat4,join(sFlat0,sFlat2)),
inference(step,[status(thm)],[t6649,t242]) ).
cnf(t776,plain,
meet(sFlat4,join(sFlat0,sFlat2)) = sFlat4,
inference(orient,[status(thm)],[t6650]) ).
cnf(t6868,plain,
sFlat4 = meet(sFlat2,sFlat4),
inference(step,[status(thm)],[t6867,t776]) ).
cnf(t3482,plain,
meet(sFlat2,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t6868]) ).
cnf(t4989,plain,
meet(sFlat2,sFlat1) = join(meet(sFlat2,sFlat1),sFlat4),
inference(cp,[status(thm)],[t4987,t3482]) ).
cnf(t6964,plain,
meet(sFlat1,sFlat2) = join(meet(sFlat2,sFlat1),sFlat4),
inference(step,[status(thm)],[t4989,t16]) ).
cnf(t93,plain,
meet(sFlat1,a) = meet(sFlat1,sFlat2),
inference(cp,[status(thm)],[t78,t91]) ).
cnf(t6530,plain,
sFlat2 = meet(sFlat1,sFlat2),
inference(step,[status(thm)],[t93,t91]) ).
cnf(t95,plain,
meet(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t6530]) ).
cnf(t6965,plain,
sFlat2 = join(meet(sFlat2,sFlat1),sFlat4),
inference(step,[status(thm)],[t6964,t95]) ).
cnf(t6966,plain,
sFlat2 = join(sFlat4,meet(sFlat2,sFlat1)),
inference(step,[status(thm)],[t6965,t51]) ).
cnf(t6967,plain,
sFlat2 = join(sFlat4,meet(sFlat1,sFlat2)),
inference(step,[status(thm)],[t6966,t16]) ).
cnf(t6968,plain,
sFlat2 = join(sFlat4,sFlat2),
inference(step,[status(thm)],[t6967,t95]) ).
cnf(t6969,plain,
sFlat2 = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t6968,t51]) ).
cnf(t6970,plain,
sFlat2 = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t6969,t242]) ).
cnf(t5000,plain,
join(sFlat0,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t6970]) ).
cnf(t6971,plain,
join(sFlat2,sFlat4) = sFlat2,
inference(step,[status(thm)],[t242,t5000]) ).
cnf(t5001,plain,
join(sFlat2,sFlat4) = sFlat2,
inference(orient,[status(thm)],[t6971]) ).
cnf(t5942,plain,
join(sFlat4,meet(sFlat1,sFlat2)) = join(sFlat4,meet(b,sFlat2)),
inference(cp,[status(thm)],[t5938,t5001]) ).
cnf(t7040,plain,
join(sFlat4,sFlat2) = join(sFlat4,meet(b,sFlat2)),
inference(step,[status(thm)],[t5942,t95]) ).
cnf(t7041,plain,
join(sFlat2,sFlat4) = join(sFlat4,meet(b,sFlat2)),
inference(step,[status(thm)],[t7040,t51]) ).
cnf(t7042,plain,
sFlat2 = join(sFlat4,meet(b,sFlat2)),
inference(step,[status(thm)],[t7041,t5001]) ).
cnf(t7043,plain,
sFlat2 = join(sFlat4,meet(sFlat2,b)),
inference(step,[status(thm)],[t7042,t16]) ).
cnf(t174,plain,
meet(sFlat3,sFlat1) = meet(b,sFlat2),
inference(cp,[status(thm)],[t172,t91]) ).
cnf(t6542,plain,
meet(sFlat1,sFlat3) = meet(b,sFlat2),
inference(step,[status(thm)],[t174,t16]) ).
cnf(t6543,plain,
meet(sFlat1,sFlat3) = meet(sFlat2,b),
inference(step,[status(thm)],[t6542,t16]) ).
cnf(t178,plain,
meet(sFlat2,b) = meet(sFlat1,sFlat3),
inference(orient,[status(thm)],[t6543]) ).
cnf(t7044,plain,
sFlat2 = join(sFlat4,meet(sFlat1,sFlat3)),
inference(step,[status(thm)],[t7043,t178]) ).
cnf(t140,plain,
join(sFlat4,meet(join(X1,sFlat4),sFlat3)) = join(sFlat4,meet(sFlat4,X1)),
inference(cp,[status(thm)],[t61,t137]) ).
cnf(t6818,plain,
join(sFlat4,meet(sFlat3,join(X1,sFlat4))) = join(sFlat4,meet(sFlat4,X1)),
inference(step,[status(thm)],[t140,t16]) ).
cnf(t6819,plain,
join(sFlat4,meet(sFlat3,join(X1,sFlat4))) = meet(sFlat4,join(sFlat4,X1)),
inference(step,[status(thm)],[t6818,t418]) ).
cnf(t2740,plain,
join(sFlat4,meet(sFlat3,join(X1,sFlat4))) = meet(sFlat4,join(sFlat4,X1)),
inference(orient,[status(thm)],[t6819]) ).
cnf(t57,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t54,t15]) ).
cnf(t98,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t57]) ).
cnf(t134,plain,
join(sFlat0,join(sFlat3,X1)) = join(sFlat0,join(sFlat4,X1)),
inference(cp,[status(thm)],[t98,t129]) ).
cnf(t6569,plain,
join(sFlat4,X1) = join(sFlat0,join(sFlat4,X1)),
inference(step,[status(thm)],[t134,t129]) ).
cnf(t246,plain,
join(sFlat0,join(sFlat4,X1)) = join(sFlat4,X1),
inference(orient,[status(thm)],[t6569]) ).
cnf(t247,plain,
join(sFlat4,b) = join(sFlat0,join(sFlat1,sFlat3)),
inference(cp,[status(thm)],[t246,t237]) ).
cnf(t6570,plain,
join(sFlat1,sFlat3) = join(sFlat0,join(sFlat1,sFlat3)),
inference(step,[status(thm)],[t247,t237]) ).
cnf(t6571,plain,
join(sFlat1,sFlat3) = join(sFlat4,sFlat1),
inference(step,[status(thm)],[t6570,t231]) ).
cnf(t6572,plain,
join(sFlat1,sFlat3) = join(sFlat1,sFlat4),
inference(step,[status(thm)],[t6571,t51]) ).
cnf(t251,plain,
join(sFlat1,sFlat4) = join(sFlat1,sFlat3),
inference(orient,[status(thm)],[t6572]) ).
cnf(t6735,plain,
join(sFlat1,sFlat4) = sFlat1,
inference(step,[status(thm)],[t251,t1663]) ).
cnf(t1666,plain,
join(sFlat1,sFlat4) = sFlat1,
inference(orient,[status(thm)],[t6735]) ).
cnf(t2741,plain,
meet(sFlat4,join(sFlat4,sFlat1)) = join(sFlat4,meet(sFlat3,sFlat1)),
inference(cp,[status(thm)],[t2740,t1666]) ).
cnf(t6820,plain,
meet(sFlat4,join(sFlat1,sFlat4)) = join(sFlat4,meet(sFlat3,sFlat1)),
inference(step,[status(thm)],[t2741,t51]) ).
cnf(t6821,plain,
meet(sFlat4,sFlat1) = join(sFlat4,meet(sFlat3,sFlat1)),
inference(step,[status(thm)],[t6820,t1666]) ).
cnf(t6822,plain,
meet(sFlat1,sFlat4) = join(sFlat4,meet(sFlat3,sFlat1)),
inference(step,[status(thm)],[t6821,t16]) ).
cnf(t6823,plain,
sFlat4 = join(sFlat4,meet(sFlat3,sFlat1)),
inference(step,[status(thm)],[t6822,t301]) ).
cnf(t6824,plain,
sFlat4 = join(sFlat4,meet(sFlat1,sFlat3)),
inference(step,[status(thm)],[t6823,t16]) ).
cnf(t2754,plain,
join(sFlat4,meet(sFlat1,sFlat3)) = sFlat4,
inference(orient,[status(thm)],[t6824]) ).
cnf(t7045,plain,
sFlat2 = sFlat4,
inference(step,[status(thm)],[t7044,t2754]) ).
cnf(t6452,plain,
sFlat4 = sFlat2,
inference(orient,[status(thm)],[t7045]) ).
cnf(t7046,plain,
join(sFlat0,sFlat3) = sFlat2,
inference(step,[status(thm)],[t70,t6452]) ).
cnf(t6453,plain,
join(sFlat0,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t7046]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(b,meet(a,c))) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(b,meet(c,a))) != join(meet(a,b),meet(a,c)),
inference(rw,[status(thm)],[goal_0,t16]) ).
cnf(g0_1,plain,
meet(a,join(b,sFlat0)) != join(meet(a,b),meet(a,c)),
inference(rw,[status(thm)],[g0_0,t46]) ).
cnf(g0_2,plain,
meet(a,join(sFlat0,b)) != join(meet(a,b),meet(a,c)),
inference(rw,[status(thm)],[g0_1,t51]) ).
cnf(g0_3,plain,
meet(a,sFlat1) != join(meet(a,b),meet(a,c)),
inference(rw,[status(thm)],[g0_2,t74]) ).
cnf(g0_4,plain,
meet(sFlat1,a) != join(meet(a,b),meet(a,c)),
inference(rw,[status(thm)],[g0_3,t16]) ).
cnf(g0_5,plain,
sFlat2 != join(meet(a,b),meet(a,c)),
inference(rw,[status(thm)],[g0_4,t91]) ).
cnf(g0_6,plain,
sFlat2 != join(meet(a,c),meet(a,b)),
inference(rw,[status(thm)],[g0_5,t51]) ).
cnf(g0_7,plain,
sFlat2 != join(meet(c,a),meet(a,b)),
inference(rw,[status(thm)],[g0_6,t16]) ).
cnf(g0_8,plain,
sFlat2 != join(sFlat0,meet(a,b)),
inference(rw,[status(thm)],[g0_7,t46]) ).
cnf(g0_9,plain,
sFlat2 != join(sFlat0,meet(b,a)),
inference(rw,[status(thm)],[g0_8,t16]) ).
cnf(g0_10,plain,
sFlat2 != join(sFlat0,sFlat3),
inference(rw,[status(thm)],[g0_9,t42]) ).
cnf(g0_11,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_10,t6453]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT023-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n016.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 20:07:27 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 29.38/4.24 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.38/4.24 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------