%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT156-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 : n019.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 171.93s 22.24s
% Output : CNFRefutation 25.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 17
% Syntax : Number of clauses : 322 ( 322 unt; 0 nHn; 184 RR)
% Number of literals : 322 ( 321 equ; 22 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 : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 193 ( 26 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t65,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t12,axiom,
sFlat3 = join(a,b),
introduced(definition) ).
cnf(t401282,plain,
sFlat3 = join(b,a),
inference(step,[status(thm)],[t12,t65]) ).
cnf(t84,plain,
join(b,a) = sFlat3,
inference(orient,[status(thm)],[t401282]) ).
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t13,axiom,
sFlat4 = meet(c,join(a,b)),
introduced(definition) ).
cnf(t60,plain,
meet(c,join(a,b)) = sFlat4,
inference(orient,[status(thm)],[t13]) ).
cnf(t69,plain,
meet(c,join(a,b)) = sFlat4,
inference(rw,[status(thm)],[t60]) ).
cnf(t401298,plain,
meet(c,join(b,a)) = sFlat4,
inference(step,[status(thm)],[t69,t65]) ).
cnf(t401299,plain,
meet(c,sFlat3) = sFlat4,
inference(step,[status(thm)],[t401298,t84]) ).
cnf(t401300,plain,
meet(sFlat3,c) = sFlat4,
inference(step,[status(thm)],[t401299,t20]) ).
cnf(t177,plain,
meet(sFlat3,c) = sFlat4,
inference(orient,[status(thm)],[t401300]) ).
cnf(t9,axiom,
sFlat0 = meet(a,c),
introduced(definition) ).
cnf(t401275,plain,
sFlat0 = meet(c,a),
inference(step,[status(thm)],[t9,t20]) ).
cnf(t55,plain,
meet(c,a) = sFlat0,
inference(orient,[status(thm)],[t401275]) ).
cnf(t10,axiom,
sFlat1 = join(b,meet(a,c)),
introduced(definition) ).
cnf(t401284,plain,
sFlat1 = join(b,meet(c,a)),
inference(step,[status(thm)],[t10,t20]) ).
cnf(t401285,plain,
sFlat1 = join(b,sFlat0),
inference(step,[status(thm)],[t401284,t55]) ).
cnf(t401286,plain,
sFlat1 = join(sFlat0,b),
inference(step,[status(thm)],[t401285,t65]) ).
cnf(t89,plain,
join(sFlat0,b) = sFlat1,
inference(orient,[status(thm)],[t401286]) ).
cnf(t11,axiom,
sFlat2 = meet(a,join(b,meet(a,c))),
introduced(definition) ).
cnf(t401273,plain,
sFlat2 = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t11,t20]) ).
cnf(t49,plain,
meet(a,join(b,meet(c,a))) = sFlat2,
inference(orient,[status(thm)],[t401273]) ).
cnf(t401276,plain,
meet(a,join(b,sFlat0)) = sFlat2,
inference(step,[status(thm)],[t49,t55]) ).
cnf(t59,plain,
meet(a,join(b,sFlat0)) = sFlat2,
inference(rw,[status(thm)],[t401276]) ).
cnf(t401291,plain,
meet(a,join(sFlat0,b)) = sFlat2,
inference(step,[status(thm)],[t59,t65]) ).
cnf(t401292,plain,
meet(a,sFlat1) = sFlat2,
inference(step,[status(thm)],[t401291,t89]) ).
cnf(t401293,plain,
meet(sFlat1,a) = sFlat2,
inference(step,[status(thm)],[t401292,t20]) ).
cnf(t131,plain,
meet(sFlat1,a) = sFlat2,
inference(orient,[status(thm)],[t401293]) ).
cnf(t14,axiom,
sFlat5 = join(meet(a,join(b,meet(a,c))),meet(c,join(a,b))),
introduced(definition) ).
cnf(t401277,plain,
sFlat5 = join(meet(c,join(a,b)),meet(a,join(b,meet(a,c)))),
inference(step,[status(thm)],[t14,t65]) ).
cnf(t401278,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(b,meet(a,c)))),
inference(step,[status(thm)],[t401277,t65]) ).
cnf(t401279,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(b,meet(c,a)))),
inference(step,[status(thm)],[t401278,t20]) ).
cnf(t401280,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(b,sFlat0))),
inference(step,[status(thm)],[t401279,t55]) ).
cnf(t401281,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(sFlat0,b))),
inference(step,[status(thm)],[t401280,t65]) ).
cnf(t80,plain,
join(meet(c,join(b,a)),meet(a,join(sFlat0,b))) = sFlat5,
inference(orient,[status(thm)],[t401281]) ).
cnf(t401283,plain,
join(meet(c,sFlat3),meet(a,join(sFlat0,b))) = sFlat5,
inference(step,[status(thm)],[t80,t84]) ).
cnf(t88,plain,
join(meet(c,sFlat3),meet(a,join(sFlat0,b))) = sFlat5,
inference(rw,[status(thm)],[t401283]) ).
cnf(t402126,plain,
join(meet(sFlat3,c),meet(a,join(sFlat0,b))) = sFlat5,
inference(step,[status(thm)],[t88,t20]) ).
cnf(t402127,plain,
join(sFlat4,meet(a,join(sFlat0,b))) = sFlat5,
inference(step,[status(thm)],[t402126,t177]) ).
cnf(t402128,plain,
join(sFlat4,meet(a,sFlat1)) = sFlat5,
inference(step,[status(thm)],[t402127,t89]) ).
cnf(t402129,plain,
join(sFlat4,meet(sFlat1,a)) = sFlat5,
inference(step,[status(thm)],[t402128,t20]) ).
cnf(t402130,plain,
join(sFlat4,sFlat2) = sFlat5,
inference(step,[status(thm)],[t402129,t131]) ).
cnf(t402131,plain,
join(sFlat2,sFlat4) = sFlat5,
inference(step,[status(thm)],[t402130,t65]) ).
cnf(t107930,plain,
join(sFlat2,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t402131]) ).
cnf(t15,axiom,
sFlat6 = meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))),
introduced(definition) ).
cnf(t401272,plain,
sFlat6 = meet(a,join(meet(a,join(b,meet(c,a))),meet(c,join(a,b)))),
inference(step,[status(thm)],[t15,t20]) ).
cnf(t44,plain,
meet(a,join(meet(a,join(b,meet(c,a))),meet(c,join(a,b)))) = sFlat6,
inference(orient,[status(thm)],[t401272]) ).
cnf(t401274,plain,
meet(a,join(sFlat2,meet(c,join(a,b)))) = sFlat6,
inference(step,[status(thm)],[t44,t49]) ).
cnf(t54,plain,
meet(a,join(sFlat2,meet(c,join(a,b)))) = sFlat6,
inference(rw,[status(thm)],[t401274]) ).
cnf(t401708,plain,
meet(a,join(sFlat2,meet(c,join(b,a)))) = sFlat6,
inference(step,[status(thm)],[t54,t65]) ).
cnf(t401709,plain,
meet(a,join(sFlat2,meet(c,sFlat3))) = sFlat6,
inference(step,[status(thm)],[t401708,t84]) ).
cnf(t401710,plain,
meet(a,join(sFlat2,meet(sFlat3,c))) = sFlat6,
inference(step,[status(thm)],[t401709,t20]) ).
cnf(t401711,plain,
meet(a,join(sFlat2,sFlat4)) = sFlat6,
inference(step,[status(thm)],[t401710,t177]) ).
cnf(t54002,plain,
meet(a,join(sFlat2,sFlat4)) = sFlat6,
inference(orient,[status(thm)],[t401711]) ).
cnf(t402139,plain,
meet(a,sFlat5) = sFlat6,
inference(step,[status(thm)],[t54002,t107930]) ).
cnf(t108043,plain,
meet(a,sFlat5) = sFlat6,
inference(rw,[status(thm)],[t402139]) ).
cnf(t402173,plain,
meet(sFlat5,a) = sFlat6,
inference(step,[status(thm)],[t108043,t20]) ).
cnf(t108412,plain,
meet(sFlat5,a) = sFlat6,
inference(orient,[status(thm)],[t402173]) ).
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(t30,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(t87,plain,
meet(X1,join(b,meet(X2,join(X1,a)))) = meet(X1,join(b,join(meet(X1,X2),meet(X2,sFlat3)))),
inference(cp,[status(thm)],[t30,t84]) ).
cnf(t101906,plain,
meet(X1,join(b,join(meet(X1,X2),meet(X2,sFlat3)))) = meet(X1,join(b,meet(X2,join(X1,a)))),
inference(orient,[status(thm)],[t87]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t29,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t19,t22]) ).
cnf(t3990,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t29]) ).
cnf(t5,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t66,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t17,t65]) ).
cnf(t147,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t66]) ).
cnf(t153,plain,
a = meet(a,sFlat3),
inference(cp,[status(thm)],[t147,t84]) ).
cnf(t401297,plain,
a = meet(sFlat3,a),
inference(step,[status(thm)],[t153,t20]) ).
cnf(t165,plain,
meet(sFlat3,a) = a,
inference(orient,[status(thm)],[t401297]) ).
cnf(t166,plain,
meet(sFlat3,meet(a,X1)) = meet(a,X1),
inference(cp,[status(thm)],[t22,t165]) ).
cnf(t587,plain,
meet(sFlat3,meet(a,X1)) = meet(a,X1),
inference(orient,[status(thm)],[t166]) ).
cnf(t54016,plain,
meet(a,join(sFlat2,sFlat4)) = meet(sFlat3,sFlat6),
inference(cp,[status(thm)],[t587,t54002]) ).
cnf(t401721,plain,
sFlat6 = meet(sFlat3,sFlat6),
inference(step,[status(thm)],[t54016,t54002]) ).
cnf(t54195,plain,
meet(sFlat3,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t401721]) ).
cnf(t54216,plain,
meet(X1,sFlat3) = join(meet(X1,sFlat3),meet(X1,sFlat6)),
inference(cp,[status(thm)],[t3990,t54195]) ).
cnf(t62690,plain,
join(meet(X1,sFlat3),meet(X1,sFlat6)) = meet(X1,sFlat3),
inference(orient,[status(thm)],[t54216]) ).
cnf(t62696,plain,
meet(X1,sFlat3) = join(meet(X1,sFlat3),meet(sFlat6,X1)),
inference(cp,[status(thm)],[t62690,t20]) ).
cnf(t70625,plain,
join(meet(X1,sFlat3),meet(sFlat6,X1)) = meet(X1,sFlat3),
inference(orient,[status(thm)],[t62696]) ).
cnf(t70626,plain,
meet(X1,sFlat3) = join(meet(sFlat6,X1),meet(X1,sFlat3)),
inference(cp,[status(thm)],[t70625,t65]) ).
cnf(t72588,plain,
join(meet(sFlat6,X1),meet(X1,sFlat3)) = meet(X1,sFlat3),
inference(orient,[status(thm)],[t70626]) ).
cnf(t101914,plain,
meet(sFlat6,join(b,meet(X1,join(sFlat6,a)))) = meet(sFlat6,join(b,meet(X1,sFlat3))),
inference(cp,[status(thm)],[t101906,t72588]) ).
cnf(t54026,plain,
a = join(a,sFlat6),
inference(cp,[status(thm)],[t19,t54002]) ).
cnf(t401729,plain,
a = join(sFlat6,a),
inference(step,[status(thm)],[t54026,t65]) ).
cnf(t54482,plain,
join(sFlat6,a) = a,
inference(orient,[status(thm)],[t401729]) ).
cnf(t403243,plain,
meet(sFlat6,join(b,meet(X1,a))) = meet(sFlat6,join(b,meet(X1,sFlat3))),
inference(step,[status(thm)],[t101914,t54482]) ).
cnf(t401036,plain,
meet(sFlat6,join(b,meet(X1,a))) = meet(sFlat6,join(b,meet(X1,sFlat3))),
inference(orient,[status(thm)],[t403243]) ).
cnf(t179,plain,
meet(sFlat3,meet(c,X1)) = meet(sFlat4,X1),
inference(cp,[status(thm)],[t22,t177]) ).
cnf(t603,plain,
meet(sFlat3,meet(c,X1)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t179]) ).
cnf(t605,plain,
meet(sFlat4,a) = meet(sFlat3,sFlat0),
inference(cp,[status(thm)],[t603,t55]) ).
cnf(t401319,plain,
meet(sFlat4,a) = meet(sFlat0,sFlat3),
inference(step,[status(thm)],[t605,t20]) ).
cnf(t56,plain,
meet(c,meet(a,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t22,t55]) ).
cnf(t203,plain,
meet(c,meet(a,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t56]) ).
cnf(t207,plain,
meet(sFlat0,join(X1,a)) = meet(c,a),
inference(cp,[status(thm)],[t203,t147]) ).
cnf(t401304,plain,
meet(sFlat0,join(X1,a)) = sFlat0,
inference(step,[status(thm)],[t207,t55]) ).
cnf(t219,plain,
meet(sFlat0,join(X1,a)) = sFlat0,
inference(orient,[status(thm)],[t401304]) ).
cnf(t167,plain,
sFlat3 = join(sFlat3,a),
inference(cp,[status(thm)],[t19,t165]) ).
cnf(t173,plain,
join(sFlat3,a) = sFlat3,
inference(orient,[status(thm)],[t167]) ).
cnf(t220,plain,
sFlat0 = meet(sFlat0,sFlat3),
inference(cp,[status(thm)],[t219,t173]) ).
cnf(t227,plain,
meet(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t220]) ).
cnf(t401320,plain,
meet(sFlat4,a) = sFlat0,
inference(step,[status(thm)],[t401319,t227]) ).
cnf(t618,plain,
meet(sFlat4,a) = sFlat0,
inference(orient,[status(thm)],[t401320]) ).
cnf(t401039,plain,
meet(sFlat6,join(b,meet(sFlat4,sFlat3))) = meet(sFlat6,join(b,sFlat0)),
inference(cp,[status(thm)],[t401036,t618]) ).
cnf(t403244,plain,
meet(sFlat6,join(b,meet(sFlat3,sFlat4))) = meet(sFlat6,join(b,sFlat0)),
inference(step,[status(thm)],[t401039,t20]) ).
cnf(t180,plain,
sFlat3 = join(sFlat3,sFlat4),
inference(cp,[status(thm)],[t19,t177]) ).
cnf(t186,plain,
join(sFlat3,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t180]) ).
cnf(t187,plain,
sFlat4 = meet(sFlat4,sFlat3),
inference(cp,[status(thm)],[t147,t186]) ).
cnf(t401302,plain,
sFlat4 = meet(sFlat3,sFlat4),
inference(step,[status(thm)],[t187,t20]) ).
cnf(t194,plain,
meet(sFlat3,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t401302]) ).
cnf(t403245,plain,
meet(sFlat6,join(b,sFlat4)) = meet(sFlat6,join(b,sFlat0)),
inference(step,[status(thm)],[t403244,t194]) ).
cnf(t403246,plain,
meet(sFlat6,join(sFlat4,b)) = meet(sFlat6,join(b,sFlat0)),
inference(step,[status(thm)],[t403245,t65]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t70,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t624,plain,
sFlat4 = join(sFlat4,sFlat0),
inference(cp,[status(thm)],[t19,t618]) ).
cnf(t401323,plain,
sFlat4 = join(sFlat0,sFlat4),
inference(step,[status(thm)],[t624,t65]) ).
cnf(t631,plain,
join(sFlat0,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t401323]) ).
cnf(t633,plain,
join(sFlat0,join(sFlat4,X1)) = join(sFlat4,X1),
inference(cp,[status(thm)],[t70,t631]) ).
cnf(t1693,plain,
join(sFlat0,join(sFlat4,X1)) = join(sFlat4,X1),
inference(orient,[status(thm)],[t633]) ).
cnf(t91,plain,
join(sFlat0,join(b,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t70,t89]) ).
cnf(t339,plain,
join(sFlat0,join(b,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t91]) ).
cnf(t345,plain,
join(sFlat1,X1) = join(sFlat0,join(X1,b)),
inference(cp,[status(thm)],[t339,t65]) ).
cnf(t916,plain,
join(sFlat0,join(X1,b)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t345]) ).
cnf(t1696,plain,
join(sFlat4,b) = join(sFlat1,sFlat4),
inference(cp,[status(thm)],[t1693,t916]) ).
cnf(t1702,plain,
join(sFlat4,b) = join(sFlat1,sFlat4),
inference(orient,[status(thm)],[t1696]) ).
cnf(t403247,plain,
meet(sFlat6,join(sFlat1,sFlat4)) = meet(sFlat6,join(b,sFlat0)),
inference(step,[status(thm)],[t403246,t1702]) ).
cnf(t154,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t147,t70]) ).
cnf(t3201,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t154]) ).
cnf(t21,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t19,t20]) ).
cnf(t110,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t21]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t26,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t22,t16]) ).
cnf(t197,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t621,plain,
meet(sFlat4,a) = meet(sFlat4,sFlat0),
inference(cp,[status(thm)],[t197,t618]) ).
cnf(t401321,plain,
sFlat0 = meet(sFlat4,sFlat0),
inference(step,[status(thm)],[t621,t618]) ).
cnf(t401322,plain,
sFlat0 = meet(sFlat0,sFlat4),
inference(step,[status(thm)],[t401321,t20]) ).
cnf(t626,plain,
meet(sFlat0,sFlat4) = sFlat0,
inference(orient,[status(thm)],[t401322]) ).
cnf(t629,plain,
meet(sFlat0,meet(sFlat4,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t22,t626]) ).
cnf(t1655,plain,
meet(sFlat0,meet(sFlat4,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t629]) ).
cnf(t1659,plain,
meet(sFlat0,join(sFlat4,X1)) = meet(sFlat0,sFlat4),
inference(cp,[status(thm)],[t1655,t17]) ).
cnf(t401350,plain,
meet(sFlat0,join(sFlat4,X1)) = sFlat0,
inference(step,[status(thm)],[t1659,t626]) ).
cnf(t1669,plain,
meet(sFlat0,join(sFlat4,X1)) = sFlat0,
inference(orient,[status(thm)],[t401350]) ).
cnf(t1674,plain,
join(sFlat4,X1) = join(join(sFlat4,X1),sFlat0),
inference(cp,[status(thm)],[t110,t1669]) ).
cnf(t401376,plain,
join(sFlat4,X1) = join(sFlat4,join(X1,sFlat0)),
inference(step,[status(thm)],[t1674,t70]) ).
cnf(t2323,plain,
join(sFlat4,join(X1,sFlat0)) = join(sFlat4,X1),
inference(orient,[status(thm)],[t401376]) ).
cnf(t2329,plain,
join(sFlat4,join(join(X1,sFlat0),X2)) = join(join(sFlat4,X1),X2),
inference(cp,[status(thm)],[t70,t2323]) ).
cnf(t401668,plain,
join(sFlat4,join(X1,join(sFlat0,X2))) = join(join(sFlat4,X1),X2),
inference(step,[status(thm)],[t2329,t70]) ).
cnf(t401669,plain,
join(sFlat4,join(X1,join(sFlat0,X2))) = join(sFlat4,join(X1,X2)),
inference(step,[status(thm)],[t401668,t70]) ).
cnf(t46591,plain,
join(sFlat4,join(X1,join(sFlat0,X2))) = join(sFlat4,join(X1,X2)),
inference(orient,[status(thm)],[t401669]) ).
cnf(t348,plain,
join(b,X1) = meet(join(b,X1),join(sFlat1,X1)),
inference(cp,[status(thm)],[t147,t339]) ).
cnf(t401441,plain,
join(b,X1) = meet(join(sFlat1,X1),join(b,X1)),
inference(step,[status(thm)],[t348,t20]) ).
cnf(t6065,plain,
meet(join(sFlat1,X1),join(b,X1)) = join(b,X1),
inference(orient,[status(thm)],[t401441]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t74,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t70,t18]) ).
cnf(t253,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t74]) ).
cnf(t6083,plain,
join(b,join(sFlat1,X1)) = meet(join(sFlat1,X1),join(b,join(sFlat1,X1))),
inference(cp,[status(thm)],[t6065,t253]) ).
cnf(t401442,plain,
join(b,join(sFlat1,X1)) = join(sFlat1,X1),
inference(step,[status(thm)],[t6083,t147]) ).
cnf(t6110,plain,
join(b,join(sFlat1,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t401442]) ).
cnf(t6137,plain,
join(sFlat1,X1) = join(b,join(X1,sFlat1)),
inference(cp,[status(thm)],[t6110,t65]) ).
cnf(t112,plain,
join(X1,X2) = join(join(X1,X2),X1),
inference(cp,[status(thm)],[t110,t17]) ).
cnf(t401315,plain,
join(X1,X2) = join(X1,join(X2,X1)),
inference(step,[status(thm)],[t112,t70]) ).
cnf(t455,plain,
join(X1,join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t401315]) ).
cnf(t465,plain,
join(join(b,X1),sFlat0) = join(join(b,X1),join(sFlat1,X1)),
inference(cp,[status(thm)],[t455,t339]) ).
cnf(t401392,plain,
join(b,join(X1,sFlat0)) = join(join(b,X1),join(sFlat1,X1)),
inference(step,[status(thm)],[t465,t70]) ).
cnf(t401393,plain,
join(b,join(X1,sFlat0)) = join(b,join(X1,join(sFlat1,X1))),
inference(step,[status(thm)],[t401392,t70]) ).
cnf(t401394,plain,
join(b,join(X1,sFlat0)) = join(b,join(X1,sFlat1)),
inference(step,[status(thm)],[t401393,t455]) ).
cnf(t2672,plain,
join(b,join(X1,sFlat1)) = join(b,join(X1,sFlat0)),
inference(orient,[status(thm)],[t401394]) ).
cnf(t401443,plain,
join(sFlat1,X1) = join(b,join(X1,sFlat0)),
inference(step,[status(thm)],[t6137,t2672]) ).
cnf(t6143,plain,
join(b,join(X1,sFlat0)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t401443]) ).
cnf(t6160,plain,
join(b,join(join(X1,sFlat0),X2)) = join(join(sFlat1,X1),X2),
inference(cp,[status(thm)],[t70,t6143]) ).
cnf(t401704,plain,
join(b,join(X1,join(sFlat0,X2))) = join(join(sFlat1,X1),X2),
inference(step,[status(thm)],[t6160,t70]) ).
cnf(t401705,plain,
join(b,join(X1,join(sFlat0,X2))) = join(sFlat1,join(X1,X2)),
inference(step,[status(thm)],[t401704,t70]) ).
cnf(t53332,plain,
join(b,join(X1,join(sFlat0,X2))) = join(sFlat1,join(X1,X2)),
inference(orient,[status(thm)],[t401705]) ).
cnf(t210,plain,
meet(a,X1) = join(meet(a,X1),meet(sFlat0,X1)),
inference(cp,[status(thm)],[t110,t203]) ).
cnf(t401427,plain,
meet(a,X1) = join(meet(sFlat0,X1),meet(a,X1)),
inference(step,[status(thm)],[t210,t65]) ).
cnf(t5122,plain,
join(meet(sFlat0,X1),meet(a,X1)) = meet(a,X1),
inference(orient,[status(thm)],[t401427]) ).
cnf(t54013,plain,
meet(a,join(sFlat2,sFlat4)) = join(meet(sFlat0,join(sFlat2,sFlat4)),sFlat6),
inference(cp,[status(thm)],[t5122,t54002]) ).
cnf(t401716,plain,
sFlat6 = join(meet(sFlat0,join(sFlat2,sFlat4)),sFlat6),
inference(step,[status(thm)],[t54013,t54002]) ).
cnf(t401717,plain,
sFlat6 = join(sFlat6,meet(sFlat0,join(sFlat2,sFlat4))),
inference(step,[status(thm)],[t401716,t65]) ).
cnf(t90,plain,
sFlat0 = meet(sFlat0,sFlat1),
inference(cp,[status(thm)],[t17,t89]) ).
cnf(t101,plain,
meet(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t90]) ).
cnf(t102,plain,
meet(sFlat0,meet(sFlat1,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t22,t101]) ).
cnf(t427,plain,
meet(sFlat0,meet(sFlat1,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t102]) ).
cnf(t428,plain,
meet(sFlat0,a) = meet(sFlat0,sFlat2),
inference(cp,[status(thm)],[t427,t131]) ).
cnf(t116,plain,
a = join(a,sFlat0),
inference(cp,[status(thm)],[t110,t55]) ).
cnf(t401290,plain,
a = join(sFlat0,a),
inference(step,[status(thm)],[t116,t65]) ).
cnf(t123,plain,
join(sFlat0,a) = a,
inference(orient,[status(thm)],[t401290]) ).
cnf(t124,plain,
sFlat0 = meet(sFlat0,a),
inference(cp,[status(thm)],[t17,t123]) ).
cnf(t127,plain,
meet(sFlat0,a) = sFlat0,
inference(orient,[status(thm)],[t124]) ).
cnf(t401313,plain,
sFlat0 = meet(sFlat0,sFlat2),
inference(step,[status(thm)],[t428,t127]) ).
cnf(t434,plain,
meet(sFlat0,sFlat2) = sFlat0,
inference(orient,[status(thm)],[t401313]) ).
cnf(t437,plain,
meet(sFlat0,meet(sFlat2,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t22,t434]) ).
cnf(t1068,plain,
meet(sFlat0,meet(sFlat2,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t437]) ).
cnf(t1071,plain,
meet(sFlat0,join(sFlat2,X1)) = meet(sFlat0,sFlat2),
inference(cp,[status(thm)],[t1068,t17]) ).
cnf(t401342,plain,
meet(sFlat0,join(sFlat2,X1)) = sFlat0,
inference(step,[status(thm)],[t1071,t434]) ).
cnf(t1077,plain,
meet(sFlat0,join(sFlat2,X1)) = sFlat0,
inference(orient,[status(thm)],[t401342]) ).
cnf(t401718,plain,
sFlat6 = join(sFlat6,sFlat0),
inference(step,[status(thm)],[t401717,t1077]) ).
cnf(t401719,plain,
sFlat6 = join(sFlat0,sFlat6),
inference(step,[status(thm)],[t401718,t65]) ).
cnf(t54117,plain,
join(sFlat0,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t401719]) ).
cnf(t54130,plain,
join(sFlat1,join(X1,sFlat6)) = join(b,join(X1,sFlat6)),
inference(cp,[status(thm)],[t53332,t54117]) ).
cnf(t58264,plain,
join(b,join(X1,sFlat6)) = join(sFlat1,join(X1,sFlat6)),
inference(orient,[status(thm)],[t54130]) ).
cnf(t58282,plain,
join(sFlat4,join(b,sFlat6)) = join(sFlat4,join(sFlat1,join(sFlat0,sFlat6))),
inference(cp,[status(thm)],[t46591,t58264]) ).
cnf(t1708,plain,
join(sFlat4,join(b,X1)) = join(join(sFlat1,sFlat4),X1),
inference(cp,[status(thm)],[t70,t1702]) ).
cnf(t401406,plain,
join(sFlat4,join(b,X1)) = join(sFlat1,join(sFlat4,X1)),
inference(step,[status(thm)],[t1708,t70]) ).
cnf(t2784,plain,
join(sFlat4,join(b,X1)) = join(sFlat1,join(sFlat4,X1)),
inference(orient,[status(thm)],[t401406]) ).
cnf(t401763,plain,
join(sFlat1,join(sFlat4,sFlat6)) = join(sFlat4,join(sFlat1,join(sFlat0,sFlat6))),
inference(step,[status(thm)],[t58282,t2784]) ).
cnf(t1699,plain,
join(sFlat4,X1) = join(sFlat0,join(X1,sFlat4)),
inference(cp,[status(thm)],[t1693,t65]) ).
cnf(t2331,plain,
join(sFlat0,join(X1,sFlat4)) = join(sFlat4,X1),
inference(orient,[status(thm)],[t1699]) ).
cnf(t2346,plain,
join(sFlat0,join(join(X1,sFlat4),X2)) = join(join(sFlat4,X1),X2),
inference(cp,[status(thm)],[t70,t2331]) ).
cnf(t401670,plain,
join(sFlat0,join(X1,join(sFlat4,X2))) = join(join(sFlat4,X1),X2),
inference(step,[status(thm)],[t2346,t70]) ).
cnf(t401671,plain,
join(sFlat0,join(X1,join(sFlat4,X2))) = join(sFlat4,join(X1,X2)),
inference(step,[status(thm)],[t401670,t70]) ).
cnf(t46820,plain,
join(sFlat0,join(X1,join(sFlat4,X2))) = join(sFlat4,join(X1,X2)),
inference(orient,[status(thm)],[t401671]) ).
cnf(t589,plain,
meet(a,X1) = meet(sFlat3,meet(X1,a)),
inference(cp,[status(thm)],[t587,t20]) ).
cnf(t1520,plain,
meet(sFlat3,meet(X1,a)) = meet(a,X1),
inference(orient,[status(thm)],[t589]) ).
cnf(t4022,plain,
meet(sFlat3,X1) = join(meet(sFlat3,X1),meet(a,X1)),
inference(cp,[status(thm)],[t3990,t1520]) ).
cnf(t17779,plain,
join(meet(sFlat3,X1),meet(a,X1)) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t4022]) ).
cnf(t54009,plain,
meet(sFlat3,join(sFlat2,sFlat4)) = join(meet(sFlat3,join(sFlat2,sFlat4)),sFlat6),
inference(cp,[status(thm)],[t17779,t54002]) ).
cnf(t86,plain,
join(b,join(a,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t70,t84]) ).
cnf(t260,plain,
join(b,join(a,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t86]) ).
cnf(t263,plain,
join(sFlat3,meet(X1,a)) = join(b,a),
inference(cp,[status(thm)],[t260,t110]) ).
cnf(t401307,plain,
join(sFlat3,meet(X1,a)) = sFlat3,
inference(step,[status(thm)],[t263,t84]) ).
cnf(t297,plain,
join(sFlat3,meet(X1,a)) = sFlat3,
inference(orient,[status(thm)],[t401307]) ).
cnf(t132,plain,
a = join(a,sFlat2),
inference(cp,[status(thm)],[t110,t131]) ).
cnf(t401294,plain,
a = join(sFlat2,a),
inference(step,[status(thm)],[t132,t65]) ).
cnf(t136,plain,
join(sFlat2,a) = a,
inference(orient,[status(thm)],[t401294]) ).
cnf(t137,plain,
sFlat2 = meet(sFlat2,a),
inference(cp,[status(thm)],[t17,t136]) ).
cnf(t143,plain,
meet(sFlat2,a) = sFlat2,
inference(orient,[status(thm)],[t137]) ).
cnf(t298,plain,
sFlat3 = join(sFlat3,sFlat2),
inference(cp,[status(thm)],[t297,t143]) ).
cnf(t401308,plain,
sFlat3 = join(sFlat2,sFlat3),
inference(step,[status(thm)],[t298,t65]) ).
cnf(t306,plain,
join(sFlat2,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t401308]) ).
cnf(t308,plain,
join(sFlat2,join(sFlat3,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t70,t306]) ).
cnf(t869,plain,
join(sFlat2,join(sFlat3,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t308]) ).
cnf(t873,plain,
join(join(sFlat3,X1),sFlat2) = join(join(sFlat3,X1),join(sFlat3,X1)),
inference(cp,[status(thm)],[t455,t869]) ).
cnf(t401359,plain,
join(sFlat3,join(X1,sFlat2)) = join(join(sFlat3,X1),join(sFlat3,X1)),
inference(step,[status(thm)],[t873,t70]) ).
cnf(t401360,plain,
join(sFlat3,join(X1,sFlat2)) = join(sFlat3,join(X1,join(sFlat3,X1))),
inference(step,[status(thm)],[t401359,t70]) ).
cnf(t401361,plain,
join(sFlat3,join(X1,sFlat2)) = join(sFlat3,join(X1,sFlat3)),
inference(step,[status(thm)],[t401360,t455]) ).
cnf(t401362,plain,
join(sFlat3,join(X1,sFlat2)) = join(sFlat3,X1),
inference(step,[status(thm)],[t401361,t455]) ).
cnf(t1938,plain,
join(sFlat3,join(X1,sFlat2)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t401362]) ).
cnf(t1946,plain,
join(X1,sFlat2) = meet(join(X1,sFlat2),join(sFlat3,X1)),
inference(cp,[status(thm)],[t147,t1938]) ).
cnf(t9909,plain,
meet(join(X1,sFlat2),join(sFlat3,X1)) = join(X1,sFlat2),
inference(orient,[status(thm)],[t1946]) ).
cnf(t9959,plain,
join(sFlat4,sFlat2) = meet(join(sFlat4,sFlat2),sFlat3),
inference(cp,[status(thm)],[t9909,t186]) ).
cnf(t401468,plain,
join(sFlat2,sFlat4) = meet(join(sFlat4,sFlat2),sFlat3),
inference(step,[status(thm)],[t9959,t65]) ).
cnf(t401469,plain,
join(sFlat2,sFlat4) = meet(sFlat3,join(sFlat4,sFlat2)),
inference(step,[status(thm)],[t401468,t20]) ).
cnf(t401470,plain,
join(sFlat2,sFlat4) = meet(sFlat3,join(sFlat2,sFlat4)),
inference(step,[status(thm)],[t401469,t65]) ).
cnf(t9987,plain,
meet(sFlat3,join(sFlat2,sFlat4)) = join(sFlat2,sFlat4),
inference(orient,[status(thm)],[t401470]) ).
cnf(t401739,plain,
join(sFlat2,sFlat4) = join(meet(sFlat3,join(sFlat2,sFlat4)),sFlat6),
inference(step,[status(thm)],[t54009,t9987]) ).
cnf(t401740,plain,
join(sFlat2,sFlat4) = join(join(sFlat2,sFlat4),sFlat6),
inference(step,[status(thm)],[t401739,t9987]) ).
cnf(t401741,plain,
join(sFlat2,sFlat4) = join(sFlat2,join(sFlat4,sFlat6)),
inference(step,[status(thm)],[t401740,t70]) ).
cnf(t55542,plain,
join(sFlat2,join(sFlat4,sFlat6)) = join(sFlat2,sFlat4),
inference(orient,[status(thm)],[t401741]) ).
cnf(t55557,plain,
join(sFlat4,join(sFlat2,sFlat6)) = join(sFlat0,join(sFlat2,sFlat4)),
inference(cp,[status(thm)],[t46820,t55542]) ).
cnf(t133,plain,
meet(sFlat1,meet(a,X1)) = meet(sFlat2,X1),
inference(cp,[status(thm)],[t22,t131]) ).
cnf(t497,plain,
meet(sFlat1,meet(a,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t133]) ).
cnf(t506,plain,
meet(a,X1) = join(meet(a,X1),meet(sFlat2,X1)),
inference(cp,[status(thm)],[t110,t497]) ).
cnf(t401457,plain,
meet(a,X1) = join(meet(sFlat2,X1),meet(a,X1)),
inference(step,[status(thm)],[t506,t65]) ).
cnf(t7043,plain,
join(meet(sFlat2,X1),meet(a,X1)) = meet(a,X1),
inference(orient,[status(thm)],[t401457]) ).
cnf(t54012,plain,
meet(a,join(sFlat2,sFlat4)) = join(meet(sFlat2,join(sFlat2,sFlat4)),sFlat6),
inference(cp,[status(thm)],[t7043,t54002]) ).
cnf(t401712,plain,
sFlat6 = join(meet(sFlat2,join(sFlat2,sFlat4)),sFlat6),
inference(step,[status(thm)],[t54012,t54002]) ).
cnf(t401713,plain,
sFlat6 = join(sFlat6,meet(sFlat2,join(sFlat2,sFlat4))),
inference(step,[status(thm)],[t401712,t65]) ).
cnf(t401714,plain,
sFlat6 = join(sFlat6,sFlat2),
inference(step,[status(thm)],[t401713,t17]) ).
cnf(t401715,plain,
sFlat6 = join(sFlat2,sFlat6),
inference(step,[status(thm)],[t401714,t65]) ).
cnf(t54078,plain,
join(sFlat2,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t401715]) ).
cnf(t401742,plain,
join(sFlat4,sFlat6) = join(sFlat0,join(sFlat2,sFlat4)),
inference(step,[status(thm)],[t55557,t54078]) ).
cnf(t436,plain,
sFlat2 = join(sFlat2,sFlat0),
inference(cp,[status(thm)],[t110,t434]) ).
cnf(t401314,plain,
sFlat2 = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t436,t65]) ).
cnf(t440,plain,
join(sFlat0,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t401314]) ).
cnf(t441,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t70,t440]) ).
cnf(t1095,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t441]) ).
cnf(t401743,plain,
join(sFlat4,sFlat6) = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t401742,t1095]) ).
cnf(t55582,plain,
join(sFlat4,sFlat6) = join(sFlat2,sFlat4),
inference(orient,[status(thm)],[t401743]) ).
cnf(t401764,plain,
join(sFlat1,join(sFlat2,sFlat4)) = join(sFlat4,join(sFlat1,join(sFlat0,sFlat6))),
inference(step,[status(thm)],[t401763,t55582]) ).
cnf(t134,plain,
sFlat1 = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t19,t131]) ).
cnf(t140,plain,
join(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t134]) ).
cnf(t141,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t70,t140]) ).
cnf(t540,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t141]) ).
cnf(t401765,plain,
join(sFlat1,sFlat4) = join(sFlat4,join(sFlat1,join(sFlat0,sFlat6))),
inference(step,[status(thm)],[t401764,t540]) ).
cnf(t401766,plain,
join(sFlat1,sFlat4) = join(sFlat4,join(sFlat1,sFlat6)),
inference(step,[status(thm)],[t401765,t46591]) ).
cnf(t58306,plain,
join(sFlat4,join(sFlat1,sFlat6)) = join(sFlat1,sFlat4),
inference(orient,[status(thm)],[t401766]) ).
cnf(t58327,plain,
sFlat6 = meet(sFlat6,join(sFlat1,sFlat4)),
inference(cp,[status(thm)],[t3201,t58306]) ).
cnf(t58344,plain,
meet(sFlat6,join(sFlat1,sFlat4)) = sFlat6,
inference(orient,[status(thm)],[t58327]) ).
cnf(t403248,plain,
sFlat6 = meet(sFlat6,join(b,sFlat0)),
inference(step,[status(thm)],[t403247,t58344]) ).
cnf(t403249,plain,
sFlat6 = meet(sFlat6,join(sFlat0,b)),
inference(step,[status(thm)],[t403248,t65]) ).
cnf(t403250,plain,
sFlat6 = meet(sFlat6,sFlat1),
inference(step,[status(thm)],[t403249,t89]) ).
cnf(t403251,plain,
sFlat6 = meet(sFlat1,sFlat6),
inference(step,[status(thm)],[t403250,t20]) ).
cnf(t54019,plain,
meet(sFlat2,join(sFlat2,sFlat4)) = meet(sFlat1,sFlat6),
inference(cp,[status(thm)],[t497,t54002]) ).
cnf(t401723,plain,
sFlat2 = meet(sFlat1,sFlat6),
inference(step,[status(thm)],[t54019,t17]) ).
cnf(t54265,plain,
meet(sFlat1,sFlat6) = sFlat2,
inference(orient,[status(thm)],[t401723]) ).
cnf(t403252,plain,
sFlat6 = sFlat2,
inference(step,[status(thm)],[t403251,t54265]) ).
cnf(t401133,plain,
sFlat6 = sFlat2,
inference(orient,[status(thm)],[t403252]) ).
cnf(t403253,plain,
meet(sFlat5,a) = sFlat2,
inference(step,[status(thm)],[t108412,t401133]) ).
cnf(t401134,plain,
meet(sFlat5,a) = sFlat2,
inference(orient,[status(thm)],[t403253]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))) != meet(a,join(b,meet(a,c))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(meet(c,join(a,b)),meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[goal_0,t65]) ).
cnf(g0_1,plain,
meet(a,join(meet(c,join(b,a)),meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_0,t65]) ).
cnf(g0_2,plain,
meet(a,join(meet(c,sFlat3),meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_1,t84]) ).
cnf(g0_3,plain,
meet(a,join(meet(sFlat3,c),meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_2,t20]) ).
cnf(g0_4,plain,
meet(a,join(sFlat4,meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_3,t177]) ).
cnf(g0_5,plain,
meet(a,join(sFlat4,meet(a,join(b,meet(c,a))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_4,t20]) ).
cnf(g0_6,plain,
meet(a,join(sFlat4,meet(a,join(b,sFlat0)))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_5,t55]) ).
cnf(g0_7,plain,
meet(a,join(sFlat4,meet(a,join(sFlat0,b)))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_6,t65]) ).
cnf(g0_8,plain,
meet(a,join(sFlat4,meet(a,sFlat1))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_7,t89]) ).
cnf(g0_9,plain,
meet(a,join(sFlat4,meet(sFlat1,a))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_8,t20]) ).
cnf(g0_10,plain,
meet(a,join(sFlat4,sFlat2)) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_9,t131]) ).
cnf(g0_11,plain,
meet(a,join(sFlat2,sFlat4)) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_10,t65]) ).
cnf(g0_12,plain,
meet(a,sFlat5) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_11,t107930]) ).
cnf(g0_13,plain,
meet(sFlat5,a) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_12,t20]) ).
cnf(g0_14,plain,
sFlat2 != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_13,t401134]) ).
cnf(g0_15,plain,
sFlat2 != meet(a,join(b,meet(c,a))),
inference(rw,[status(thm)],[g0_14,t20]) ).
cnf(g0_16,plain,
sFlat2 != meet(a,join(b,sFlat0)),
inference(rw,[status(thm)],[g0_15,t55]) ).
cnf(g0_17,plain,
sFlat2 != meet(a,join(sFlat0,b)),
inference(rw,[status(thm)],[g0_16,t65]) ).
cnf(g0_18,plain,
sFlat2 != meet(a,sFlat1),
inference(rw,[status(thm)],[g0_17,t89]) ).
cnf(g0_19,plain,
sFlat2 != meet(sFlat1,a),
inference(rw,[status(thm)],[g0_18,t20]) ).
cnf(g0_20,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_19,t131]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT156-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 20:24:23 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 171.93/22.24 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 171.93/22.24 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------