%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT170-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:48 PM UTC 2026
% Result : Unsatisfiable 39.77s 5.53s
% Output : CNFRefutation 39.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 18
% Syntax : Number of clauses : 374 ( 374 unt; 0 nHn; 225 RR)
% Number of literals : 374 ( 373 equ; 16 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 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 : 252 ( 69 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t9,axiom,
sFlat0 = join(a,b),
introduced(definition) ).
cnf(t17836,plain,
sFlat0 = join(b,a),
inference(step,[status(thm)],[t9,t21]) ).
cnf(t51,plain,
join(b,a) = sFlat0,
inference(orient,[status(thm)],[t17836]) ).
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t61,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t10,axiom,
sFlat1 = meet(a,b),
introduced(definition) ).
cnf(t17849,plain,
sFlat1 = meet(b,a),
inference(step,[status(thm)],[t10,t61]) ).
cnf(t85,plain,
meet(b,a) = sFlat1,
inference(orient,[status(thm)],[t17849]) ).
cnf(t11,axiom,
sFlat2 = join(c,meet(a,b)),
introduced(definition) ).
cnf(t56,plain,
join(c,meet(a,b)) = sFlat2,
inference(orient,[status(thm)],[t11]) ).
cnf(t62,plain,
join(c,meet(a,b)) = sFlat2,
inference(rw,[status(thm)],[t56]) ).
cnf(t17857,plain,
join(c,meet(b,a)) = sFlat2,
inference(step,[status(thm)],[t62,t61]) ).
cnf(t17858,plain,
join(c,sFlat1) = sFlat2,
inference(step,[status(thm)],[t17857,t85]) ).
cnf(t17859,plain,
join(sFlat1,c) = sFlat2,
inference(step,[status(thm)],[t17858,t21]) ).
cnf(t142,plain,
join(sFlat1,c) = sFlat2,
inference(orient,[status(thm)],[t17859]) ).
cnf(t12,axiom,
sFlat3 = meet(join(a,b),join(c,meet(a,b))),
introduced(definition) ).
cnf(t17838,plain,
sFlat3 = meet(join(b,a),join(c,meet(a,b))),
inference(step,[status(thm)],[t12,t21]) ).
cnf(t17839,plain,
sFlat3 = meet(sFlat0,join(c,meet(a,b))),
inference(step,[status(thm)],[t17838,t51]) ).
cnf(t17840,plain,
sFlat3 = meet(sFlat0,join(c,meet(b,a))),
inference(step,[status(thm)],[t17839,t61]) ).
cnf(t73,plain,
meet(sFlat0,join(c,meet(b,a))) = sFlat3,
inference(orient,[status(thm)],[t17840]) ).
cnf(t17850,plain,
meet(sFlat0,join(c,sFlat1)) = sFlat3,
inference(step,[status(thm)],[t73,t85]) ).
cnf(t89,plain,
meet(sFlat0,join(c,sFlat1)) = sFlat3,
inference(rw,[status(thm)],[t17850]) ).
cnf(t17862,plain,
meet(sFlat0,join(sFlat1,c)) = sFlat3,
inference(step,[status(thm)],[t89,t21]) ).
cnf(t17863,plain,
meet(sFlat0,sFlat2) = sFlat3,
inference(step,[status(thm)],[t17862,t142]) ).
cnf(t163,plain,
meet(sFlat0,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t17863]) ).
cnf(t13,axiom,
sFlat4 = join(b,meet(join(a,b),join(c,meet(a,b)))),
introduced(definition) ).
cnf(t17834,plain,
sFlat4 = join(b,meet(join(b,a),join(c,meet(a,b)))),
inference(step,[status(thm)],[t13,t21]) ).
cnf(t42,plain,
join(b,meet(join(b,a),join(c,meet(a,b)))) = sFlat4,
inference(orient,[status(thm)],[t17834]) ).
cnf(t17837,plain,
join(b,meet(sFlat0,join(c,meet(a,b)))) = sFlat4,
inference(step,[status(thm)],[t42,t51]) ).
cnf(t55,plain,
join(b,meet(sFlat0,join(c,meet(a,b)))) = sFlat4,
inference(rw,[status(thm)],[t17837]) ).
cnf(t18158,plain,
join(b,meet(sFlat0,join(c,meet(b,a)))) = sFlat4,
inference(step,[status(thm)],[t55,t61]) ).
cnf(t18159,plain,
join(b,meet(sFlat0,join(c,sFlat1))) = sFlat4,
inference(step,[status(thm)],[t18158,t85]) ).
cnf(t18160,plain,
join(b,meet(sFlat0,join(sFlat1,c))) = sFlat4,
inference(step,[status(thm)],[t18159,t21]) ).
cnf(t18161,plain,
join(b,meet(sFlat0,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t18160,t142]) ).
cnf(t18162,plain,
join(b,sFlat3) = sFlat4,
inference(step,[status(thm)],[t18161,t163]) ).
cnf(t18163,plain,
join(sFlat3,b) = sFlat4,
inference(step,[status(thm)],[t18162,t21]) ).
cnf(t6753,plain,
join(sFlat3,b) = sFlat4,
inference(orient,[status(thm)],[t18163]) ).
cnf(t14,axiom,
sFlat5 = meet(a,join(b,meet(join(a,b),join(c,meet(a,b))))),
introduced(definition) ).
cnf(t17841,plain,
sFlat5 = meet(a,join(b,meet(join(b,a),join(c,meet(a,b))))),
inference(step,[status(thm)],[t14,t21]) ).
cnf(t17842,plain,
sFlat5 = meet(a,join(b,meet(sFlat0,join(c,meet(a,b))))),
inference(step,[status(thm)],[t17841,t51]) ).
cnf(t17843,plain,
sFlat5 = meet(a,join(b,meet(sFlat0,join(c,meet(b,a))))),
inference(step,[status(thm)],[t17842,t61]) ).
cnf(t17844,plain,
sFlat5 = meet(a,join(b,sFlat3)),
inference(step,[status(thm)],[t17843,t73]) ).
cnf(t17845,plain,
sFlat5 = meet(a,join(sFlat3,b)),
inference(step,[status(thm)],[t17844,t21]) ).
cnf(t77,plain,
meet(a,join(sFlat3,b)) = sFlat5,
inference(orient,[status(thm)],[t17845]) ).
cnf(t18172,plain,
meet(a,sFlat4) = sFlat5,
inference(step,[status(thm)],[t77,t6753]) ).
cnf(t6779,plain,
meet(a,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t18172]) ).
cnf(t18196,plain,
meet(sFlat4,a) = sFlat5,
inference(step,[status(thm)],[t6779,t61]) ).
cnf(t6865,plain,
meet(sFlat4,a) = sFlat5,
inference(orient,[status(thm)],[t18196]) ).
cnf(t15,axiom,
sFlat6 = join(b,c),
introduced(definition) ).
cnf(t17835,plain,
sFlat6 = join(c,b),
inference(step,[status(thm)],[t15,t21]) ).
cnf(t47,plain,
join(c,b) = sFlat6,
inference(orient,[status(thm)],[t17835]) ).
cnf(t16,axiom,
sFlat7 = meet(a,join(b,c)),
introduced(definition) ).
cnf(t17846,plain,
sFlat7 = meet(a,join(c,b)),
inference(step,[status(thm)],[t16,t21]) ).
cnf(t17847,plain,
sFlat7 = meet(a,sFlat6),
inference(step,[status(thm)],[t17846,t47]) ).
cnf(t17848,plain,
sFlat7 = meet(sFlat6,a),
inference(step,[status(thm)],[t17847,t61]) ).
cnf(t81,plain,
meet(sFlat6,a) = sFlat7,
inference(orient,[status(thm)],[t17848]) ).
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(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t25,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t22,t21]) ).
cnf(t286,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t25]) ).
cnf(t296,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t20,t286]) ).
cnf(t943,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t296]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t26,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t22,t17]) ).
cnf(t138,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t945,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t943,t138]) ).
cnf(t1031,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t945]) ).
cnf(t8,axiom,
join(X1,meet(X2,meet(join(X1,X3),join(X3,meet(X2,X4))))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
join(X1,meet(X2,meet(join(X1,X3),join(X3,meet(X2,X4))))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t8]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t32,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X1,X4)))) = join(X1,meet(X2,meet(X1,join(meet(X1,X3),meet(X2,X4))))),
inference(cp,[status(thm)],[t30,t18]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t63,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t66,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t63,t61]) ).
cnf(t304,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t66]) ).
cnf(t309,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t18,t304]) ).
cnf(t1161,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t309]) ).
cnf(t1168,plain,
X1 = join(X1,meet(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t1161,t304]) ).
cnf(t1570,plain,
join(X1,meet(X2,meet(X1,X3))) = X1,
inference(orient,[status(thm)],[t1168]) ).
cnf(t18039,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X1,X4)))) = X1,
inference(step,[status(thm)],[t32,t1570]) ).
cnf(t2396,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X1,X4)))) = X1,
inference(orient,[status(thm)],[t18039]) ).
cnf(t44,plain,
b = meet(b,sFlat4),
inference(cp,[status(thm)],[t20,t42]) ).
cnf(t17851,plain,
b = meet(sFlat4,b),
inference(step,[status(thm)],[t44,t61]) ).
cnf(t90,plain,
meet(sFlat4,b) = b,
inference(orient,[status(thm)],[t17851]) ).
cnf(t2432,plain,
sFlat4 = join(sFlat4,meet(X1,join(b,meet(sFlat4,X2)))),
inference(cp,[status(thm)],[t2396,t90]) ).
cnf(t13994,plain,
join(sFlat4,meet(X1,join(b,meet(sFlat4,X2)))) = sFlat4,
inference(orient,[status(thm)],[t2432]) ).
cnf(t13998,plain,
sFlat4 = join(sFlat4,meet(X1,join(b,sFlat5))),
inference(cp,[status(thm)],[t13994,t6865]) ).
cnf(t18323,plain,
sFlat4 = join(sFlat4,meet(X1,join(sFlat5,b))),
inference(step,[status(thm)],[t13998,t21]) ).
cnf(t14023,plain,
join(sFlat4,meet(X1,join(sFlat5,b))) = sFlat4,
inference(orient,[status(thm)],[t18323]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t37,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,meet(join(X1,X3),join(X3,X2)))),
inference(cp,[status(thm)],[t30,t19]) ).
cnf(t956,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(cp,[status(thm)],[t943,t18]) ).
cnf(t18022,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,X1))),
inference(step,[status(thm)],[t956,t63]) ).
cnf(t2252,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t18022]) ).
cnf(t18125,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t37,t2252]) ).
cnf(t5518,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t18125]) ).
cnf(t5584,plain,
join(b,meet(a,join(b,X1))) = join(b,meet(a,join(X1,sFlat1))),
inference(cp,[status(thm)],[t5518,t85]) ).
cnf(t6171,plain,
join(b,meet(a,join(b,X1))) = join(b,meet(a,join(X1,sFlat1))),
inference(orient,[status(thm)],[t5584]) ).
cnf(t6172,plain,
join(b,meet(a,join(X1,sFlat1))) = join(b,meet(a,join(X1,b))),
inference(cp,[status(thm)],[t6171,t21]) ).
cnf(t16409,plain,
join(b,meet(a,join(X1,b))) = join(b,meet(a,join(X1,sFlat1))),
inference(orient,[status(thm)],[t6172]) ).
cnf(t144,plain,
join(sFlat1,join(c,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t22,t142]) ).
cnf(t355,plain,
join(sFlat1,join(c,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t144]) ).
cnf(t356,plain,
join(sFlat2,b) = join(sFlat1,sFlat6),
inference(cp,[status(thm)],[t355,t47]) ).
cnf(t48,plain,
join(c,join(b,X1)) = join(sFlat6,X1),
inference(cp,[status(thm)],[t22,t47]) ).
cnf(t170,plain,
join(c,join(b,X1)) = join(sFlat6,X1),
inference(orient,[status(thm)],[t48]) ).
cnf(t174,plain,
join(sFlat6,meet(b,X1)) = join(c,b),
inference(cp,[status(thm)],[t170,t18]) ).
cnf(t17870,plain,
join(sFlat6,meet(b,X1)) = sFlat6,
inference(step,[status(thm)],[t174,t47]) ).
cnf(t225,plain,
join(sFlat6,meet(b,X1)) = sFlat6,
inference(orient,[status(thm)],[t17870]) ).
cnf(t226,plain,
sFlat6 = join(sFlat6,sFlat1),
inference(cp,[status(thm)],[t225,t85]) ).
cnf(t17871,plain,
sFlat6 = join(sFlat1,sFlat6),
inference(step,[status(thm)],[t226,t21]) ).
cnf(t232,plain,
join(sFlat1,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t17871]) ).
cnf(t17880,plain,
join(sFlat2,b) = sFlat6,
inference(step,[status(thm)],[t356,t232]) ).
cnf(t362,plain,
join(sFlat2,b) = sFlat6,
inference(orient,[status(thm)],[t17880]) ).
cnf(t16411,plain,
join(b,meet(a,join(sFlat2,sFlat1))) = join(b,meet(a,sFlat6)),
inference(cp,[status(thm)],[t16409,t362]) ).
cnf(t18439,plain,
join(b,meet(a,join(sFlat1,sFlat2))) = join(b,meet(a,sFlat6)),
inference(step,[status(thm)],[t16411,t21]) ).
cnf(t143,plain,
join(sFlat1,c) = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t138,t142]) ).
cnf(t17860,plain,
sFlat2 = join(sFlat1,sFlat2),
inference(step,[status(thm)],[t143,t142]) ).
cnf(t147,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t17860]) ).
cnf(t18440,plain,
join(b,meet(a,sFlat2)) = join(b,meet(a,sFlat6)),
inference(step,[status(thm)],[t18439,t147]) ).
cnf(t18441,plain,
join(b,meet(sFlat2,a)) = join(b,meet(a,sFlat6)),
inference(step,[status(thm)],[t18440,t61]) ).
cnf(t29,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(cp,[status(thm)],[t20,t22]) ).
cnf(t1122,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t29]) ).
cnf(t1126,plain,
join(X1,X2) = meet(join(X1,X2),join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t1122,t286]) ).
cnf(t11805,plain,
meet(join(X1,X2),join(X2,join(X3,X1))) = join(X1,X2),
inference(orient,[status(thm)],[t1126]) ).
cnf(t53,plain,
b = meet(b,sFlat0),
inference(cp,[status(thm)],[t20,t51]) ).
cnf(t17853,plain,
b = meet(sFlat0,b),
inference(step,[status(thm)],[t53,t61]) ).
cnf(t98,plain,
meet(sFlat0,b) = b,
inference(orient,[status(thm)],[t17853]) ).
cnf(t100,plain,
meet(sFlat0,meet(b,X1)) = meet(b,X1),
inference(cp,[status(thm)],[t63,t98]) ).
cnf(t330,plain,
meet(sFlat0,meet(b,X1)) = meet(b,X1),
inference(orient,[status(thm)],[t100]) ).
cnf(t331,plain,
meet(b,a) = meet(sFlat0,sFlat1),
inference(cp,[status(thm)],[t330,t85]) ).
cnf(t17879,plain,
sFlat1 = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t331,t85]) ).
cnf(t335,plain,
meet(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t17879]) ).
cnf(t336,plain,
sFlat0 = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t18,t335]) ).
cnf(t338,plain,
join(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t336]) ).
cnf(t12041,plain,
join(sFlat1,X1) = meet(join(sFlat1,X1),join(X1,sFlat0)),
inference(cp,[status(thm)],[t11805,t338]) ).
cnf(t12222,plain,
meet(join(sFlat1,X1),join(X1,sFlat0)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t12041]) ).
cnf(t12245,plain,
join(sFlat1,X1) = meet(join(sFlat1,X1),join(sFlat0,X1)),
inference(cp,[status(thm)],[t12222,t21]) ).
cnf(t18291,plain,
join(sFlat1,X1) = meet(join(sFlat0,X1),join(sFlat1,X1)),
inference(step,[status(thm)],[t12245,t61]) ).
cnf(t12697,plain,
meet(join(sFlat0,X1),join(sFlat1,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t18291]) ).
cnf(t67,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t63,t19]) ).
cnf(t154,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t67]) ).
cnf(t1164,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t1161,t154]) ).
cnf(t1258,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t1164]) ).
cnf(t145,plain,
sFlat1 = meet(sFlat1,sFlat2),
inference(cp,[status(thm)],[t20,t142]) ).
cnf(t151,plain,
meet(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t145]) ).
cnf(t152,plain,
meet(sFlat1,meet(sFlat2,X1)) = meet(sFlat1,X1),
inference(cp,[status(thm)],[t63,t151]) ).
cnf(t685,plain,
meet(sFlat1,meet(sFlat2,X1)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t152]) ).
cnf(t1271,plain,
meet(sFlat2,X1) = join(meet(sFlat2,X1),meet(sFlat1,X1)),
inference(cp,[status(thm)],[t1258,t685]) ).
cnf(t18102,plain,
meet(sFlat2,X1) = join(meet(sFlat1,X1),meet(sFlat2,X1)),
inference(step,[status(thm)],[t1271,t21]) ).
cnf(t4779,plain,
join(meet(sFlat1,X1),meet(sFlat2,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t18102]) ).
cnf(t87,plain,
meet(b,meet(a,X1)) = meet(sFlat1,X1),
inference(cp,[status(thm)],[t63,t85]) ).
cnf(t213,plain,
meet(b,meet(a,X1)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t87]) ).
cnf(t214,plain,
meet(sFlat1,join(sFlat3,b)) = meet(b,sFlat5),
inference(cp,[status(thm)],[t213,t77]) ).
cnf(t17919,plain,
meet(sFlat1,join(sFlat3,b)) = meet(sFlat5,b),
inference(step,[status(thm)],[t214,t61]) ).
cnf(t218,plain,
meet(sFlat1,X1) = meet(b,meet(X1,a)),
inference(cp,[status(thm)],[t213,t61]) ).
cnf(t449,plain,
meet(b,meet(X1,a)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t218]) ).
cnf(t78,plain,
a = join(a,sFlat5),
inference(cp,[status(thm)],[t18,t77]) ).
cnf(t17855,plain,
a = join(sFlat5,a),
inference(step,[status(thm)],[t78,t21]) ).
cnf(t109,plain,
join(sFlat5,a) = a,
inference(orient,[status(thm)],[t17855]) ).
cnf(t111,plain,
sFlat5 = meet(sFlat5,a),
inference(cp,[status(thm)],[t20,t109]) ).
cnf(t132,plain,
meet(sFlat5,a) = sFlat5,
inference(orient,[status(thm)],[t111]) ).
cnf(t451,plain,
meet(sFlat1,sFlat5) = meet(b,sFlat5),
inference(cp,[status(thm)],[t449,t132]) ).
cnf(t17908,plain,
meet(sFlat1,sFlat5) = meet(sFlat5,b),
inference(step,[status(thm)],[t451,t61]) ).
cnf(t495,plain,
meet(sFlat5,b) = meet(sFlat1,sFlat5),
inference(orient,[status(thm)],[t17908]) ).
cnf(t17920,plain,
meet(sFlat1,join(sFlat3,b)) = meet(sFlat1,sFlat5),
inference(step,[status(thm)],[t17919,t495]) ).
cnf(t651,plain,
meet(sFlat1,join(sFlat3,b)) = meet(sFlat1,sFlat5),
inference(orient,[status(thm)],[t17920]) ).
cnf(t86,plain,
b = join(b,sFlat1),
inference(cp,[status(thm)],[t18,t85]) ).
cnf(t17856,plain,
b = join(sFlat1,b),
inference(step,[status(thm)],[t86,t21]) ).
cnf(t116,plain,
join(sFlat1,b) = b,
inference(orient,[status(thm)],[t17856]) ).
cnf(t117,plain,
join(sFlat1,join(b,X1)) = join(b,X1),
inference(cp,[status(thm)],[t22,t116]) ).
cnf(t353,plain,
join(sFlat1,join(b,X1)) = join(b,X1),
inference(orient,[status(thm)],[t117]) ).
cnf(t354,plain,
sFlat1 = meet(sFlat1,join(b,X1)),
inference(cp,[status(thm)],[t20,t353]) ).
cnf(t611,plain,
meet(sFlat1,join(b,X1)) = sFlat1,
inference(orient,[status(thm)],[t354]) ).
cnf(t614,plain,
sFlat1 = meet(sFlat1,join(X1,b)),
inference(cp,[status(thm)],[t611,t21]) ).
cnf(t781,plain,
meet(sFlat1,join(X1,b)) = sFlat1,
inference(orient,[status(thm)],[t614]) ).
cnf(t17931,plain,
sFlat1 = meet(sFlat1,sFlat5),
inference(step,[status(thm)],[t651,t781]) ).
cnf(t784,plain,
sFlat1 = meet(sFlat1,sFlat5),
inference(rw,[status(thm)],[t17931]) ).
cnf(t785,plain,
meet(sFlat1,sFlat5) = sFlat1,
inference(orient,[status(thm)],[t784]) ).
cnf(t4795,plain,
meet(sFlat2,sFlat5) = join(sFlat1,meet(sFlat2,sFlat5)),
inference(cp,[status(thm)],[t4779,t785]) ).
cnf(t4838,plain,
join(sFlat1,meet(sFlat2,sFlat5)) = meet(sFlat2,sFlat5),
inference(orient,[status(thm)],[t4795]) ).
cnf(t12761,plain,
join(sFlat1,meet(sFlat2,sFlat5)) = meet(join(sFlat0,meet(sFlat2,sFlat5)),meet(sFlat2,sFlat5)),
inference(cp,[status(thm)],[t12697,t4838]) ).
cnf(t18305,plain,
meet(sFlat2,sFlat5) = meet(join(sFlat0,meet(sFlat2,sFlat5)),meet(sFlat2,sFlat5)),
inference(step,[status(thm)],[t12761,t4838]) ).
cnf(t52,plain,
join(b,join(a,X1)) = join(sFlat0,X1),
inference(cp,[status(thm)],[t22,t51]) ).
cnf(t188,plain,
join(b,join(a,X1)) = join(sFlat0,X1),
inference(orient,[status(thm)],[t52]) ).
cnf(t191,plain,
join(sFlat0,meet(a,X1)) = join(b,a),
inference(cp,[status(thm)],[t188,t18]) ).
cnf(t17872,plain,
join(sFlat0,meet(a,X1)) = sFlat0,
inference(step,[status(thm)],[t191,t51]) ).
cnf(t254,plain,
join(sFlat0,meet(a,X1)) = sFlat0,
inference(orient,[status(thm)],[t17872]) ).
cnf(t255,plain,
sFlat0 = join(sFlat0,sFlat5),
inference(cp,[status(thm)],[t254,t77]) ).
cnf(t260,plain,
join(sFlat0,sFlat5) = sFlat0,
inference(orient,[status(thm)],[t255]) ).
cnf(t261,plain,
join(sFlat0,join(sFlat5,X1)) = join(sFlat0,X1),
inference(cp,[status(thm)],[t22,t260]) ).
cnf(t835,plain,
join(sFlat0,join(sFlat5,X1)) = join(sFlat0,X1),
inference(orient,[status(thm)],[t261]) ).
cnf(t1288,plain,
join(sFlat0,meet(X1,sFlat5)) = join(sFlat0,sFlat5),
inference(cp,[status(thm)],[t835,t1258]) ).
cnf(t17965,plain,
join(sFlat0,meet(X1,sFlat5)) = sFlat0,
inference(step,[status(thm)],[t1288,t260]) ).
cnf(t1349,plain,
join(sFlat0,meet(X1,sFlat5)) = sFlat0,
inference(orient,[status(thm)],[t17965]) ).
cnf(t18306,plain,
meet(sFlat2,sFlat5) = meet(sFlat0,meet(sFlat2,sFlat5)),
inference(step,[status(thm)],[t18305,t1349]) ).
cnf(t165,plain,
meet(sFlat0,meet(sFlat2,X1)) = meet(sFlat3,X1),
inference(cp,[status(thm)],[t63,t163]) ).
cnf(t372,plain,
meet(sFlat0,meet(sFlat2,X1)) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t165]) ).
cnf(t18307,plain,
meet(sFlat2,sFlat5) = meet(sFlat3,sFlat5),
inference(step,[status(thm)],[t18306,t372]) ).
cnf(t215,plain,
meet(sFlat1,a) = meet(b,a),
inference(cp,[status(thm)],[t213,t19]) ).
cnf(t17869,plain,
meet(sFlat1,a) = sFlat1,
inference(step,[status(thm)],[t215,t85]) ).
cnf(t222,plain,
meet(sFlat1,a) = sFlat1,
inference(orient,[status(thm)],[t17869]) ).
cnf(t4806,plain,
meet(sFlat2,a) = join(sFlat1,meet(sFlat2,a)),
inference(cp,[status(thm)],[t4779,t222]) ).
cnf(t4860,plain,
join(sFlat1,meet(sFlat2,a)) = meet(sFlat2,a),
inference(orient,[status(thm)],[t4806]) ).
cnf(t12759,plain,
join(sFlat1,meet(sFlat2,a)) = meet(join(sFlat0,meet(sFlat2,a)),meet(sFlat2,a)),
inference(cp,[status(thm)],[t12697,t4860]) ).
cnf(t18296,plain,
meet(sFlat2,a) = meet(join(sFlat0,meet(sFlat2,a)),meet(sFlat2,a)),
inference(step,[status(thm)],[t12759,t4860]) ).
cnf(t256,plain,
sFlat0 = join(sFlat0,meet(X1,a)),
inference(cp,[status(thm)],[t254,t61]) ).
cnf(t518,plain,
join(sFlat0,meet(X1,a)) = sFlat0,
inference(orient,[status(thm)],[t256]) ).
cnf(t18297,plain,
meet(sFlat2,a) = meet(sFlat0,meet(sFlat2,a)),
inference(step,[status(thm)],[t18296,t518]) ).
cnf(t18298,plain,
meet(sFlat2,a) = meet(sFlat3,a),
inference(step,[status(thm)],[t18297,t372]) ).
cnf(t68,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t63,t20]) ).
cnf(t890,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t68]) ).
cnf(t893,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t890,t61]) ).
cnf(t1485,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t893]) ).
cnf(t1489,plain,
meet(sFlat3,a) = meet(sFlat3,sFlat5),
inference(cp,[status(thm)],[t1485,t77]) ).
cnf(t1497,plain,
meet(sFlat3,a) = meet(sFlat3,sFlat5),
inference(orient,[status(thm)],[t1489]) ).
cnf(t18299,plain,
meet(sFlat2,a) = meet(sFlat3,sFlat5),
inference(step,[status(thm)],[t18298,t1497]) ).
cnf(t13592,plain,
meet(sFlat3,sFlat5) = meet(sFlat2,a),
inference(orient,[status(thm)],[t18299]) ).
cnf(t18308,plain,
meet(sFlat2,sFlat5) = meet(sFlat2,a),
inference(step,[status(thm)],[t18307,t13592]) ).
cnf(t13633,plain,
meet(sFlat2,a) = meet(sFlat2,sFlat5),
inference(orient,[status(thm)],[t18308]) ).
cnf(t18442,plain,
join(b,meet(sFlat2,sFlat5)) = join(b,meet(a,sFlat6)),
inference(step,[status(thm)],[t18441,t13633]) ).
cnf(t45,plain,
join(b,meet(X1,join(meet(join(b,a),join(c,meet(a,b))),meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(join(b,a),join(c,meet(a,b))),meet(X1,X2))))),
inference(cp,[status(thm)],[t30,t42]) ).
cnf(t18390,plain,
join(b,meet(X1,join(meet(sFlat0,join(c,meet(a,b))),meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(join(b,a),join(c,meet(a,b))),meet(X1,X2))))),
inference(step,[status(thm)],[t45,t51]) ).
cnf(t18391,plain,
join(b,meet(X1,join(meet(sFlat0,join(c,meet(b,a))),meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(join(b,a),join(c,meet(a,b))),meet(X1,X2))))),
inference(step,[status(thm)],[t18390,t61]) ).
cnf(t18392,plain,
join(b,meet(X1,join(meet(sFlat0,join(c,sFlat1)),meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(join(b,a),join(c,meet(a,b))),meet(X1,X2))))),
inference(step,[status(thm)],[t18391,t85]) ).
cnf(t18393,plain,
join(b,meet(X1,join(meet(sFlat0,join(sFlat1,c)),meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(join(b,a),join(c,meet(a,b))),meet(X1,X2))))),
inference(step,[status(thm)],[t18392,t21]) ).
cnf(t18394,plain,
join(b,meet(X1,join(meet(sFlat0,sFlat2),meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(join(b,a),join(c,meet(a,b))),meet(X1,X2))))),
inference(step,[status(thm)],[t18393,t142]) ).
cnf(t18395,plain,
join(b,meet(X1,join(sFlat3,meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(join(b,a),join(c,meet(a,b))),meet(X1,X2))))),
inference(step,[status(thm)],[t18394,t163]) ).
cnf(t18396,plain,
join(b,meet(X1,join(sFlat3,meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(sFlat0,join(c,meet(a,b))),meet(X1,X2))))),
inference(step,[status(thm)],[t18395,t51]) ).
cnf(t18397,plain,
join(b,meet(X1,join(sFlat3,meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(sFlat0,join(c,meet(b,a))),meet(X1,X2))))),
inference(step,[status(thm)],[t18396,t61]) ).
cnf(t18398,plain,
join(b,meet(X1,join(sFlat3,meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(sFlat0,join(c,sFlat1)),meet(X1,X2))))),
inference(step,[status(thm)],[t18397,t85]) ).
cnf(t18399,plain,
join(b,meet(X1,join(sFlat3,meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(sFlat0,join(sFlat1,c)),meet(X1,X2))))),
inference(step,[status(thm)],[t18398,t21]) ).
cnf(t18400,plain,
join(b,meet(X1,join(sFlat3,meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(meet(sFlat0,sFlat2),meet(X1,X2))))),
inference(step,[status(thm)],[t18399,t142]) ).
cnf(t18401,plain,
join(b,meet(X1,join(sFlat3,meet(b,X2)))) = join(b,meet(X1,meet(sFlat4,join(sFlat3,meet(X1,X2))))),
inference(step,[status(thm)],[t18400,t163]) ).
cnf(t16845,plain,
join(b,meet(X1,meet(sFlat4,join(sFlat3,meet(X1,X2))))) = join(b,meet(X1,join(sFlat3,meet(b,X2)))),
inference(orient,[status(thm)],[t18401]) ).
cnf(t83,plain,
meet(sFlat6,meet(a,X1)) = meet(sFlat7,X1),
inference(cp,[status(thm)],[t63,t81]) ).
cnf(t201,plain,
meet(sFlat6,meet(a,X1)) = meet(sFlat7,X1),
inference(orient,[status(thm)],[t83]) ).
cnf(t203,plain,
meet(sFlat7,a) = meet(sFlat6,a),
inference(cp,[status(thm)],[t201,t19]) ).
cnf(t17868,plain,
meet(sFlat7,a) = sFlat7,
inference(step,[status(thm)],[t203,t81]) ).
cnf(t210,plain,
meet(sFlat7,a) = sFlat7,
inference(orient,[status(thm)],[t17868]) ).
cnf(t16916,plain,
join(b,meet(sFlat7,join(sFlat3,meet(b,a)))) = join(b,meet(sFlat7,meet(sFlat4,join(sFlat3,sFlat7)))),
inference(cp,[status(thm)],[t16845,t210]) ).
cnf(t18402,plain,
join(b,meet(sFlat7,join(sFlat3,sFlat1))) = join(b,meet(sFlat7,meet(sFlat4,join(sFlat3,sFlat7)))),
inference(step,[status(thm)],[t16916,t85]) ).
cnf(t18403,plain,
join(b,meet(sFlat7,join(sFlat1,sFlat3))) = join(b,meet(sFlat7,meet(sFlat4,join(sFlat3,sFlat7)))),
inference(step,[status(thm)],[t18402,t21]) ).
cnf(t74,plain,
sFlat0 = join(sFlat0,sFlat3),
inference(cp,[status(thm)],[t18,t73]) ).
cnf(t106,plain,
join(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t74]) ).
cnf(t107,plain,
join(sFlat0,join(sFlat3,X1)) = join(sFlat0,X1),
inference(cp,[status(thm)],[t22,t106]) ).
cnf(t343,plain,
join(sFlat0,join(sFlat3,X1)) = join(sFlat0,X1),
inference(orient,[status(thm)],[t107]) ).
cnf(t1056,plain,
join(sFlat3,X1) = meet(join(sFlat3,X1),join(sFlat0,X1)),
inference(cp,[status(thm)],[t1031,t343]) ).
cnf(t18085,plain,
join(sFlat3,X1) = meet(join(sFlat0,X1),join(sFlat3,X1)),
inference(step,[status(thm)],[t1056,t61]) ).
cnf(t3871,plain,
meet(join(sFlat0,X1),join(sFlat3,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t18085]) ).
cnf(t1279,plain,
meet(sFlat2,X1) = join(meet(sFlat2,X1),meet(sFlat3,X1)),
inference(cp,[status(thm)],[t1258,t372]) ).
cnf(t4979,plain,
join(meet(sFlat2,X1),meet(sFlat3,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t1279]) ).
cnf(t6765,plain,
sFlat3 = meet(sFlat3,sFlat4),
inference(cp,[status(thm)],[t20,t6753]) ).
cnf(t6814,plain,
meet(sFlat3,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t6765]) ).
cnf(t6815,plain,
meet(sFlat2,sFlat4) = join(meet(sFlat2,sFlat4),sFlat3),
inference(cp,[status(thm)],[t4979,t6814]) ).
cnf(t18219,plain,
meet(sFlat2,sFlat4) = join(sFlat3,meet(sFlat2,sFlat4)),
inference(step,[status(thm)],[t6815,t21]) ).
cnf(t7124,plain,
join(sFlat3,meet(sFlat2,sFlat4)) = meet(sFlat2,sFlat4),
inference(orient,[status(thm)],[t18219]) ).
cnf(t7125,plain,
join(sFlat3,meet(sFlat2,sFlat4)) = meet(join(sFlat0,meet(sFlat2,sFlat4)),meet(sFlat2,sFlat4)),
inference(cp,[status(thm)],[t3871,t7124]) ).
cnf(t18220,plain,
meet(sFlat2,sFlat4) = meet(join(sFlat0,meet(sFlat2,sFlat4)),meet(sFlat2,sFlat4)),
inference(step,[status(thm)],[t7125,t7124]) ).
cnf(t193,plain,
join(sFlat0,X1) = join(b,join(X1,a)),
inference(cp,[status(thm)],[t188,t21]) ).
cnf(t413,plain,
join(b,join(X1,a)) = join(sFlat0,X1),
inference(orient,[status(thm)],[t193]) ).
cnf(t1123,plain,
join(b,X1) = meet(join(b,X1),join(sFlat0,X1)),
inference(cp,[status(thm)],[t1122,t413]) ).
cnf(t18045,plain,
join(b,X1) = meet(join(sFlat0,X1),join(b,X1)),
inference(step,[status(thm)],[t1123,t61]) ).
cnf(t2669,plain,
meet(join(sFlat0,X1),join(b,X1)) = join(b,X1),
inference(orient,[status(thm)],[t18045]) ).
cnf(t2689,plain,
join(b,sFlat3) = meet(sFlat0,join(b,sFlat3)),
inference(cp,[status(thm)],[t2669,t106]) ).
cnf(t18046,plain,
join(sFlat3,b) = meet(sFlat0,join(b,sFlat3)),
inference(step,[status(thm)],[t2689,t21]) ).
cnf(t18047,plain,
join(sFlat3,b) = meet(sFlat0,join(sFlat3,b)),
inference(step,[status(thm)],[t18046,t21]) ).
cnf(t2716,plain,
meet(sFlat0,join(sFlat3,b)) = join(sFlat3,b),
inference(orient,[status(thm)],[t18047]) ).
cnf(t2717,plain,
sFlat0 = join(sFlat0,meet(X1,join(sFlat3,b))),
inference(cp,[status(thm)],[t1570,t2716]) ).
cnf(t6537,plain,
join(sFlat0,meet(X1,join(sFlat3,b))) = sFlat0,
inference(orient,[status(thm)],[t2717]) ).
cnf(t18173,plain,
join(sFlat0,meet(X1,sFlat4)) = sFlat0,
inference(step,[status(thm)],[t6537,t6753]) ).
cnf(t6780,plain,
join(sFlat0,meet(X1,sFlat4)) = sFlat0,
inference(rw,[status(thm)],[t18173]) ).
cnf(t6931,plain,
join(sFlat0,meet(X1,sFlat4)) = sFlat0,
inference(orient,[status(thm)],[t6780]) ).
cnf(t18221,plain,
meet(sFlat2,sFlat4) = meet(sFlat0,meet(sFlat2,sFlat4)),
inference(step,[status(thm)],[t18220,t6931]) ).
cnf(t18222,plain,
meet(sFlat2,sFlat4) = meet(sFlat3,sFlat4),
inference(step,[status(thm)],[t18221,t372]) ).
cnf(t18223,plain,
meet(sFlat2,sFlat4) = sFlat3,
inference(step,[status(thm)],[t18222,t6814]) ).
cnf(t7137,plain,
meet(sFlat2,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t18223]) ).
cnf(t7139,plain,
meet(sFlat2,sFlat4) = join(meet(sFlat1,sFlat4),sFlat3),
inference(cp,[status(thm)],[t4779,t7137]) ).
cnf(t18227,plain,
sFlat3 = join(meet(sFlat1,sFlat4),sFlat3),
inference(step,[status(thm)],[t7139,t7137]) ).
cnf(t18228,plain,
sFlat3 = join(sFlat3,meet(sFlat1,sFlat4)),
inference(step,[status(thm)],[t18227,t21]) ).
cnf(t92,plain,
meet(sFlat4,meet(b,X1)) = meet(b,X1),
inference(cp,[status(thm)],[t63,t90]) ).
cnf(t320,plain,
meet(sFlat4,meet(b,X1)) = meet(b,X1),
inference(orient,[status(thm)],[t92]) ).
cnf(t321,plain,
meet(b,a) = meet(sFlat4,sFlat1),
inference(cp,[status(thm)],[t320,t85]) ).
cnf(t17877,plain,
sFlat1 = meet(sFlat4,sFlat1),
inference(step,[status(thm)],[t321,t85]) ).
cnf(t17878,plain,
sFlat1 = meet(sFlat1,sFlat4),
inference(step,[status(thm)],[t17877,t61]) ).
cnf(t325,plain,
meet(sFlat1,sFlat4) = sFlat1,
inference(orient,[status(thm)],[t17878]) ).
cnf(t18229,plain,
sFlat3 = join(sFlat3,sFlat1),
inference(step,[status(thm)],[t18228,t325]) ).
cnf(t18230,plain,
sFlat3 = join(sFlat1,sFlat3),
inference(step,[status(thm)],[t18229,t21]) ).
cnf(t7790,plain,
join(sFlat1,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t18230]) ).
cnf(t18404,plain,
join(b,meet(sFlat7,sFlat3)) = join(b,meet(sFlat7,meet(sFlat4,join(sFlat3,sFlat7)))),
inference(step,[status(thm)],[t18403,t7790]) ).
cnf(t18405,plain,
join(b,meet(sFlat3,sFlat7)) = join(b,meet(sFlat7,meet(sFlat4,join(sFlat3,sFlat7)))),
inference(step,[status(thm)],[t18404,t61]) ).
cnf(t202,plain,
meet(sFlat7,join(sFlat3,b)) = meet(sFlat6,sFlat5),
inference(cp,[status(thm)],[t201,t77]) ).
cnf(t17918,plain,
meet(sFlat7,join(sFlat3,b)) = meet(sFlat5,sFlat6),
inference(step,[status(thm)],[t202,t61]) ).
cnf(t647,plain,
meet(sFlat7,join(sFlat3,b)) = meet(sFlat5,sFlat6),
inference(orient,[status(thm)],[t17918]) ).
cnf(t1488,plain,
meet(sFlat3,sFlat7) = meet(sFlat3,meet(sFlat5,sFlat6)),
inference(cp,[status(thm)],[t1485,t647]) ).
cnf(t1501,plain,
meet(sFlat3,meet(sFlat5,sFlat6)) = meet(sFlat3,sFlat7),
inference(orient,[status(thm)],[t1488]) ).
cnf(t79,plain,
meet(a,meet(join(sFlat3,b),X1)) = meet(sFlat5,X1),
inference(cp,[status(thm)],[t63,t77]) ).
cnf(t1401,plain,
meet(a,meet(join(sFlat3,b),X1)) = meet(sFlat5,X1),
inference(orient,[status(thm)],[t79]) ).
cnf(t1402,plain,
meet(sFlat5,join(sFlat3,join(b,X1))) = meet(a,join(sFlat3,b)),
inference(cp,[status(thm)],[t1401,t1122]) ).
cnf(t17987,plain,
meet(sFlat5,join(sFlat3,join(b,X1))) = sFlat5,
inference(step,[status(thm)],[t1402,t77]) ).
cnf(t1512,plain,
meet(sFlat5,join(sFlat3,join(b,X1))) = sFlat5,
inference(orient,[status(thm)],[t17987]) ).
cnf(t1513,plain,
sFlat5 = meet(sFlat5,join(X1,join(sFlat3,b))),
inference(cp,[status(thm)],[t1512,t286]) ).
cnf(t2338,plain,
meet(sFlat5,join(X1,join(sFlat3,b))) = sFlat5,
inference(orient,[status(thm)],[t1513]) ).
cnf(t176,plain,
join(sFlat6,X1) = join(c,join(X1,b)),
inference(cp,[status(thm)],[t170,t21]) ).
cnf(t401,plain,
join(c,join(X1,b)) = join(sFlat6,X1),
inference(orient,[status(thm)],[t176]) ).
cnf(t2339,plain,
sFlat5 = meet(sFlat5,join(sFlat6,sFlat3)),
inference(cp,[status(thm)],[t2338,t401]) ).
cnf(t18024,plain,
sFlat5 = meet(sFlat5,join(sFlat3,sFlat6)),
inference(step,[status(thm)],[t2339,t21]) ).
cnf(t364,plain,
sFlat2 = meet(sFlat2,sFlat6),
inference(cp,[status(thm)],[t20,t362]) ).
cnf(t370,plain,
meet(sFlat2,sFlat6) = sFlat2,
inference(orient,[status(thm)],[t364]) ).
cnf(t373,plain,
meet(sFlat3,sFlat6) = meet(sFlat0,sFlat2),
inference(cp,[status(thm)],[t372,t370]) ).
cnf(t17884,plain,
meet(sFlat3,sFlat6) = sFlat3,
inference(step,[status(thm)],[t373,t163]) ).
cnf(t389,plain,
meet(sFlat3,sFlat6) = sFlat3,
inference(orient,[status(thm)],[t17884]) ).
cnf(t1263,plain,
sFlat6 = join(sFlat6,sFlat3),
inference(cp,[status(thm)],[t1258,t389]) ).
cnf(t17964,plain,
sFlat6 = join(sFlat3,sFlat6),
inference(step,[status(thm)],[t1263,t21]) ).
cnf(t1298,plain,
join(sFlat3,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t17964]) ).
cnf(t18025,plain,
sFlat5 = meet(sFlat5,sFlat6),
inference(step,[status(thm)],[t18024,t1298]) ).
cnf(t2344,plain,
meet(sFlat5,sFlat6) = sFlat5,
inference(orient,[status(thm)],[t18025]) ).
cnf(t18030,plain,
meet(sFlat3,sFlat5) = meet(sFlat3,sFlat7),
inference(step,[status(thm)],[t1501,t2344]) ).
cnf(t2354,plain,
meet(sFlat3,sFlat5) = meet(sFlat3,sFlat7),
inference(rw,[status(thm)],[t18030]) ).
cnf(t2364,plain,
meet(sFlat3,sFlat7) = meet(sFlat3,sFlat5),
inference(orient,[status(thm)],[t2354]) ).
cnf(t18302,plain,
meet(sFlat3,sFlat7) = meet(sFlat2,a),
inference(step,[status(thm)],[t2364,t13592]) ).
cnf(t13595,plain,
meet(sFlat3,sFlat7) = meet(sFlat2,a),
inference(orient,[status(thm)],[t18302]) ).
cnf(t18311,plain,
meet(sFlat3,sFlat7) = meet(sFlat2,sFlat5),
inference(step,[status(thm)],[t13595,t13633]) ).
cnf(t13636,plain,
meet(sFlat3,sFlat7) = meet(sFlat2,sFlat5),
inference(orient,[status(thm)],[t18311]) ).
cnf(t18406,plain,
join(b,meet(sFlat2,sFlat5)) = join(b,meet(sFlat7,meet(sFlat4,join(sFlat3,sFlat7)))),
inference(step,[status(thm)],[t18405,t13636]) ).
cnf(t18407,plain,
join(b,meet(sFlat2,sFlat5)) = join(b,meet(sFlat7,sFlat4)),
inference(step,[status(thm)],[t18406,t2252]) ).
cnf(t18408,plain,
join(b,meet(sFlat2,sFlat5)) = join(b,meet(sFlat4,sFlat7)),
inference(step,[status(thm)],[t18407,t61]) ).
cnf(t18028,plain,
meet(sFlat7,join(sFlat3,b)) = sFlat5,
inference(step,[status(thm)],[t647,t2344]) ).
cnf(t2347,plain,
meet(sFlat7,join(sFlat3,b)) = sFlat5,
inference(orient,[status(thm)],[t18028]) ).
cnf(t18171,plain,
meet(sFlat7,sFlat4) = sFlat5,
inference(step,[status(thm)],[t2347,t6753]) ).
cnf(t6778,plain,
meet(sFlat7,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t18171]) ).
cnf(t18195,plain,
meet(sFlat4,sFlat7) = sFlat5,
inference(step,[status(thm)],[t6778,t61]) ).
cnf(t6849,plain,
meet(sFlat4,sFlat7) = sFlat5,
inference(orient,[status(thm)],[t18195]) ).
cnf(t18409,plain,
join(b,meet(sFlat2,sFlat5)) = join(b,sFlat5),
inference(step,[status(thm)],[t18408,t6849]) ).
cnf(t18410,plain,
join(b,meet(sFlat2,sFlat5)) = join(sFlat5,b),
inference(step,[status(thm)],[t18409,t21]) ).
cnf(t17018,plain,
join(b,meet(sFlat2,sFlat5)) = join(sFlat5,b),
inference(orient,[status(thm)],[t18410]) ).
cnf(t18443,plain,
join(sFlat5,b) = join(b,meet(a,sFlat6)),
inference(step,[status(thm)],[t18442,t17018]) ).
cnf(t18444,plain,
join(sFlat5,b) = join(b,meet(sFlat6,a)),
inference(step,[status(thm)],[t18443,t61]) ).
cnf(t18445,plain,
join(sFlat5,b) = join(b,sFlat7),
inference(step,[status(thm)],[t18444,t81]) ).
cnf(t18446,plain,
join(sFlat5,b) = join(sFlat7,b),
inference(step,[status(thm)],[t18445,t21]) ).
cnf(t17742,plain,
join(sFlat7,b) = join(sFlat5,b),
inference(orient,[status(thm)],[t18446]) ).
cnf(t17745,plain,
sFlat7 = meet(sFlat7,join(sFlat5,b)),
inference(cp,[status(thm)],[t20,t17742]) ).
cnf(t17760,plain,
meet(sFlat7,join(sFlat5,b)) = sFlat7,
inference(orient,[status(thm)],[t17745]) ).
cnf(t17765,plain,
sFlat4 = join(sFlat4,sFlat7),
inference(cp,[status(thm)],[t14023,t17760]) ).
cnf(t17778,plain,
join(sFlat4,sFlat7) = sFlat4,
inference(orient,[status(thm)],[t17765]) ).
cnf(t17779,plain,
sFlat7 = meet(sFlat7,sFlat4),
inference(cp,[status(thm)],[t1031,t17778]) ).
cnf(t18450,plain,
sFlat7 = meet(sFlat4,sFlat7),
inference(step,[status(thm)],[t17779,t61]) ).
cnf(t18451,plain,
sFlat7 = sFlat5,
inference(step,[status(thm)],[t18450,t6849]) ).
cnf(t17792,plain,
sFlat7 = sFlat5,
inference(orient,[status(thm)],[t18451]) ).
cnf(t18452,plain,
meet(sFlat6,a) = sFlat5,
inference(step,[status(thm)],[t81,t17792]) ).
cnf(t17793,plain,
meet(sFlat6,a) = sFlat5,
inference(orient,[status(thm)],[t18452]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(b,meet(join(a,b),join(c,meet(a,b))))) != meet(a,join(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(b,meet(join(b,a),join(c,meet(a,b))))) != meet(a,join(b,c)),
inference(rw,[status(thm)],[goal_0,t21]) ).
cnf(g0_1,plain,
meet(a,join(b,meet(sFlat0,join(c,meet(a,b))))) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_0,t51]) ).
cnf(g0_2,plain,
meet(a,join(b,meet(sFlat0,join(c,meet(b,a))))) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_1,t61]) ).
cnf(g0_3,plain,
meet(a,join(b,meet(sFlat0,join(c,sFlat1)))) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_2,t85]) ).
cnf(g0_4,plain,
meet(a,join(b,meet(sFlat0,join(sFlat1,c)))) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_3,t21]) ).
cnf(g0_5,plain,
meet(a,join(b,meet(sFlat0,sFlat2))) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_4,t142]) ).
cnf(g0_6,plain,
meet(a,join(b,sFlat3)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_5,t163]) ).
cnf(g0_7,plain,
meet(a,join(sFlat3,b)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_6,t21]) ).
cnf(g0_8,plain,
meet(a,sFlat4) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_7,t6753]) ).
cnf(g0_9,plain,
meet(sFlat4,a) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_8,t61]) ).
cnf(g0_10,plain,
sFlat5 != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_9,t6865]) ).
cnf(g0_11,plain,
sFlat5 != meet(a,join(c,b)),
inference(rw,[status(thm)],[g0_10,t21]) ).
cnf(g0_12,plain,
sFlat5 != meet(a,sFlat6),
inference(rw,[status(thm)],[g0_11,t47]) ).
cnf(g0_13,plain,
sFlat5 != meet(sFlat6,a),
inference(rw,[status(thm)],[g0_12,t61]) ).
cnf(g0_14,plain,
sFlat5 != sFlat5,
inference(rw,[status(thm)],[g0_13,t17793]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT170-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 20:27:35 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 39.77/5.53 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 39.77/5.53 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------