%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT158-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 : n006.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:37 PM UTC 2026
% Result : Unsatisfiable 196.84s 33.86s
% Output : CNFRefutation 196.84s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t42,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t8,axiom,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,X4)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,X4)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t8]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t273611,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t6,t42]) ).
cnf(t46,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t273611]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t12,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t50,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t46,t12]) ).
cnf(t273619,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t50,t46]) ).
cnf(t273620,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t273619,t42]) ).
cnf(t273621,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t273620,t42]) ).
cnf(t93,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t273621]) ).
cnf(t101,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X4,meet(X2,Y4)))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,X4)))))),
inference(cp,[status(thm)],[t33,t93]) ).
cnf(t273689,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X4,meet(X2,Y4)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(step,[status(thm)],[t101,t33]) ).
cnf(t646,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X4,meet(X2,Y4)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t273689]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t273610,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t7,t13]) ).
cnf(t15,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t273610]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t49,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t46,t11]) ).
cnf(t273614,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t49,t46]) ).
cnf(t273615,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t273614,t42]) ).
cnf(t74,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t273615]) ).
cnf(t80,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X4))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,X4)))))),
inference(cp,[status(thm)],[t33,t74]) ).
cnf(t273651,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(step,[status(thm)],[t80,t33]) ).
cnf(t185,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t273651]) ).
cnf(t188,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X1,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t185,t93]) ).
cnf(t273652,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t188,t12]) ).
cnf(t273653,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t273652,t13]) ).
cnf(t204,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t273653]) ).
cnf(t207,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(cp,[status(thm)],[t204,t12]) ).
cnf(t227,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t207]) ).
cnf(t5,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t19,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t15,t10]) ).
cnf(t273616,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t19,t15]) ).
cnf(t273617,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t273616,t13]) ).
cnf(t273618,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t273617,t13]) ).
cnf(t83,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t273618]) ).
cnf(t230,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t227,t83]) ).
cnf(t273659,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(step,[status(thm)],[t230,t83]) ).
cnf(t273660,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t273659,t42]) ).
cnf(t273,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t273660]) ).
cnf(t303,plain,
meet(X1,meet(join(meet(X1,X2),meet(X2,join(X1,X3))),X4)) = meet(X4,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t273]) ).
cnf(t273679,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t303,t13]) ).
cnf(t273680,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X2,meet(X4,X1)),
inference(step,[status(thm)],[t273679,t15]) ).
cnf(t273681,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t273680,t15]) ).
cnf(t442,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,X4))))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t273681]) ).
cnf(t488,plain,
meet(X1,meet(meet(X2,join(meet(X1,X3),meet(X3,join(X1,X4)))),Y4)) = meet(Y4,meet(X1,meet(X3,X2))),
inference(cp,[status(thm)],[t15,t442]) ).
cnf(t273766,plain,
meet(X1,meet(Y4,meet(X2,join(meet(X1,X3),meet(X3,join(X1,X4)))))) = meet(Y4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t488,t13]) ).
cnf(t273767,plain,
meet(X1,meet(X2,meet(join(meet(X1,X3),meet(X3,join(X1,X4))),Y4))) = meet(Y4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t273766,t15]) ).
cnf(t273768,plain,
meet(X1,meet(X2,meet(Y4,join(meet(X1,X3),meet(X3,join(X1,X4)))))) = meet(Y4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t273767,t13]) ).
cnf(t273769,plain,
meet(X1,meet(X2,meet(Y4,join(meet(X1,X3),meet(X3,join(X1,X4)))))) = meet(X1,meet(meet(X3,X2),Y4)),
inference(step,[status(thm)],[t273768,t15]) ).
cnf(t273770,plain,
meet(X1,meet(X2,meet(Y4,join(meet(X1,X3),meet(X3,join(X1,X4)))))) = meet(X1,meet(Y4,meet(X3,X2))),
inference(step,[status(thm)],[t273769,t13]) ).
cnf(t273771,plain,
meet(X1,meet(X2,meet(Y4,join(meet(X1,X3),meet(X3,join(X1,X4)))))) = meet(X1,meet(X2,meet(Y4,X3))),
inference(step,[status(thm)],[t273770,t15]) ).
cnf(t273772,plain,
meet(X1,meet(X2,meet(Y4,join(meet(X1,X3),meet(X3,join(X1,X4)))))) = meet(X1,meet(X2,meet(X3,Y4))),
inference(step,[status(thm)],[t273771,t13]) ).
cnf(t1634,plain,
meet(X1,meet(X2,meet(X3,join(meet(X1,X4),meet(X4,join(X1,Y4)))))) = meet(X1,meet(X2,meet(X4,X3))),
inference(orient,[status(thm)],[t273772]) ).
cnf(t213,plain,
meet(X1,join(join(X1,X2),meet(X1,X3))) = meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t204,t74]) ).
cnf(t273669,plain,
meet(X1,join(meet(X1,X3),join(X1,X2))) = meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t213,t42]) ).
cnf(t273670,plain,
meet(X1,join(X2,join(meet(X1,X3),X1))) = meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t273669,t46]) ).
cnf(t273671,plain,
meet(X1,join(X1,join(X2,meet(X1,X3)))) = meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t273670,t46]) ).
cnf(t273672,plain,
meet(X1,join(X1,X2)) = meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t273671,t93]) ).
cnf(t273673,plain,
X1 = meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t273672,t10]) ).
cnf(t359,plain,
meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t273673]) ).
cnf(t1694,plain,
meet(join(X1,X2),meet(X3,meet(X1,X4))) = meet(join(X1,X2),meet(X3,meet(X4,join(meet(join(X1,X2),X1),X1)))),
inference(cp,[status(thm)],[t1634,t359]) ).
cnf(t273881,plain,
meet(meet(X1,X4),meet(join(X1,X2),X3)) = meet(join(X1,X2),meet(X3,meet(X4,join(meet(join(X1,X2),X1),X1)))),
inference(step,[status(thm)],[t1694,t15]) ).
cnf(t273882,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(join(X1,X2),meet(X3,meet(X4,join(meet(join(X1,X2),X1),X1)))),
inference(step,[status(thm)],[t273881,t15]) ).
cnf(t273883,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X3,meet(meet(X4,join(meet(join(X1,X2),X1),X1)),join(X1,X2))),
inference(step,[status(thm)],[t273882,t15]) ).
cnf(t273884,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X3,meet(join(X1,X2),meet(X4,join(meet(join(X1,X2),X1),X1)))),
inference(step,[status(thm)],[t273883,t13]) ).
cnf(t273885,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X3,meet(X4,meet(join(meet(join(X1,X2),X1),X1),join(X1,X2)))),
inference(step,[status(thm)],[t273884,t15]) ).
cnf(t273886,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X3,meet(X4,meet(join(X1,X2),join(meet(join(X1,X2),X1),X1)))),
inference(step,[status(thm)],[t273885,t13]) ).
cnf(t273887,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X3,meet(X4,meet(join(X1,X2),join(X1,meet(join(X1,X2),X1))))),
inference(step,[status(thm)],[t273886,t42]) ).
cnf(t273888,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X3,meet(X4,meet(join(X1,X2),X1))),
inference(step,[status(thm)],[t273887,t227]) ).
cnf(t273889,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X3,meet(X4,meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t273888,t13]) ).
cnf(t273890,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X3,meet(X4,X1)),
inference(step,[status(thm)],[t273889,t10]) ).
cnf(t273891,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X3,meet(X1,X4)),
inference(step,[status(thm)],[t273890,t13]) ).
cnf(t273892,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X1,meet(X4,X3)),
inference(step,[status(thm)],[t273891,t15]) ).
cnf(t273893,plain,
meet(X3,meet(meet(X1,X4),join(X1,X2))) = meet(X1,meet(X3,X4)),
inference(step,[status(thm)],[t273892,t13]) ).
cnf(t4465,plain,
meet(X1,meet(meet(X2,X3),join(X2,X4))) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t273893]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t18,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t15,t9]) ).
cnf(t273612,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t18,t15]) ).
cnf(t273613,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t273612,t13]) ).
cnf(t66,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t273613]) ).
cnf(t4469,plain,
meet(X1,meet(meet(X1,X2),X2)) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t4465,t66]) ).
cnf(t273894,plain,
meet(X1,meet(X2,meet(X1,X2))) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t4469,t13]) ).
cnf(t273895,plain,
meet(X1,meet(X1,meet(X2,X2))) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t273894,t15]) ).
cnf(t273896,plain,
meet(X1,meet(X2,X2)) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t273895,t66]) ).
cnf(t273897,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t273896,t9]) ).
cnf(t4614,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t273897]) ).
cnf(t4655,plain,
meet(X1,join(X2,meet(meet(X2,X3),join(X1,X4)))) = meet(X1,join(X2,meet(meet(X2,X3),join(X1,meet(X2,X3))))),
inference(cp,[status(thm)],[t33,t4614]) ).
cnf(t196,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t185,t12]) ).
cnf(t273668,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,X4))))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t196,t204]) ).
cnf(t341,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,X4))))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t273668]) ).
cnf(t273899,plain,
meet(X1,join(X2,meet(meet(X2,X3),join(X1,X4)))) = meet(X1,join(X2,meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t4655,t341]) ).
cnf(t4680,plain,
meet(X1,join(X2,meet(meet(X2,X3),join(X1,X4)))) = meet(X1,join(X2,meet(X1,meet(X2,X3)))),
inference(orient,[status(thm)],[t273899]) ).
cnf(t4695,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,join(X2,meet(join(X1,X4),meet(X2,X3)))),
inference(cp,[status(thm)],[t4680,t13]) ).
cnf(t273900,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,join(X2,meet(X3,meet(join(X1,X4),X2)))),
inference(step,[status(thm)],[t4695,t15]) ).
cnf(t273901,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,join(X2,meet(X2,meet(X3,join(X1,X4))))),
inference(step,[status(thm)],[t273900,t15]) ).
cnf(t273902,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,X2),
inference(step,[status(thm)],[t273901,t12]) ).
cnf(t4782,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t273902]) ).
cnf(t273903,plain,
meet(X1,join(X2,meet(meet(X2,X3),join(X1,X4)))) = meet(X1,X2),
inference(step,[status(thm)],[t4680,t4782]) ).
cnf(t4783,plain,
meet(X1,join(X2,meet(meet(X2,X3),join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t273903]) ).
cnf(t225,plain,
meet(X1,meet(join(X2,meet(X3,join(X1,X2))),X4)) = meet(X4,meet(X1,join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t15,t204]) ).
cnf(t273676,plain,
meet(X1,meet(X4,join(X2,meet(X3,join(X1,X2))))) = meet(X4,meet(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t225,t13]) ).
cnf(t273677,plain,
meet(X1,meet(X4,join(X2,meet(X3,join(X1,X2))))) = meet(X1,meet(join(X2,meet(X1,X3)),X4)),
inference(step,[status(thm)],[t273676,t15]) ).
cnf(t273678,plain,
meet(X1,meet(X4,join(X2,meet(X3,join(X1,X2))))) = meet(X1,meet(X4,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t273677,t13]) ).
cnf(t414,plain,
meet(X1,meet(X2,join(X3,meet(X4,join(X1,X3))))) = meet(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t273678]) ).
cnf(t214,plain,
meet(X1,join(join(X2,meet(X1,X3)),meet(X1,X4))) = meet(X1,join(join(X2,meet(X1,X3)),meet(X4,join(X1,X2)))),
inference(cp,[status(thm)],[t204,t93]) ).
cnf(t273747,plain,
meet(X1,join(meet(X1,X4),join(X2,meet(X1,X3)))) = meet(X1,join(join(X2,meet(X1,X3)),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t214,t42]) ).
cnf(t273748,plain,
meet(X1,join(meet(X1,X3),join(meet(X1,X4),X2))) = meet(X1,join(join(X2,meet(X1,X3)),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t273747,t46]) ).
cnf(t273749,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X1,X4)))) = meet(X1,join(join(X2,meet(X1,X3)),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t273748,t46]) ).
cnf(t273750,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X1,X4)))) = meet(X1,join(meet(X4,join(X1,X2)),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t273749,t42]) ).
cnf(t273751,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X1,X4)))) = meet(X1,join(meet(X1,X3),join(meet(X4,join(X1,X2)),X2))),
inference(step,[status(thm)],[t273750,t46]) ).
cnf(t273752,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X1,X4)))) = meet(X1,join(X2,join(meet(X1,X3),meet(X4,join(X1,X2))))),
inference(step,[status(thm)],[t273751,t46]) ).
cnf(t1306,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X4,join(X1,X2))))) = meet(X1,join(X2,join(meet(X1,X3),meet(X1,X4)))),
inference(orient,[status(thm)],[t273752]) ).
cnf(t1307,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t1306,t93]) ).
cnf(t273753,plain,
meet(X1,join(X2,join(meet(X1,X2),meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t1307,t42]) ).
cnf(t1370,plain,
meet(X1,join(X2,join(meet(X1,X2),meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t273753]) ).
cnf(t4628,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(meet(X1,X2),X4))) = meet(meet(X1,X2),join(join(X1,X3),join(meet(X1,X2),meet(meet(X1,X2),X4)))),
inference(cp,[status(thm)],[t1370,t4614]) ).
cnf(t273909,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X4,meet(X1,X2)))) = meet(meet(X1,X2),join(join(X1,X3),join(meet(X1,X2),meet(meet(X1,X2),X4)))),
inference(step,[status(thm)],[t4628,t13]) ).
cnf(t273910,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X2,meet(X4,X1)))) = meet(meet(X1,X2),join(join(X1,X3),join(meet(X1,X2),meet(meet(X1,X2),X4)))),
inference(step,[status(thm)],[t273909,t15]) ).
cnf(t273911,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X1,meet(X2,X4)))) = meet(meet(X1,X2),join(join(X1,X3),join(meet(X1,X2),meet(meet(X1,X2),X4)))),
inference(step,[status(thm)],[t273910,t15]) ).
cnf(t273912,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X1,meet(X2,X4)))) = meet(meet(X1,X2),join(meet(X1,X2),join(meet(meet(X1,X2),X4),join(X1,X3)))),
inference(step,[status(thm)],[t273911,t46]) ).
cnf(t273913,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X1,meet(X2,X4)))) = meet(X1,X2),
inference(step,[status(thm)],[t273912,t10]) ).
cnf(t5048,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X1,meet(X2,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t273913]) ).
cnf(t245,plain,
meet(X1,meet(join(X2,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t227]) ).
cnf(t273656,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t245,t13]) ).
cnf(t273657,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t273656,t15]) ).
cnf(t273658,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t273657,t15]) ).
cnf(t247,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t273658]) ).
cnf(t5114,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(X3,join(X4,X1)),meet(X1,meet(X2,Y4)))),
inference(cp,[status(thm)],[t5048,t46]) ).
cnf(t273914,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,meet(X2,Y4)),join(X3,join(X4,X1)))),
inference(step,[status(thm)],[t5114,t42]) ).
cnf(t273915,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(X4,X1),join(meet(X1,meet(X2,Y4)),X3))),
inference(step,[status(thm)],[t273914,t46]) ).
cnf(t273916,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(join(X4,X1),meet(X1,meet(X2,Y4))))),
inference(step,[status(thm)],[t273915,t46]) ).
cnf(t273917,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(join(X1,X4),meet(X1,meet(X2,Y4))))),
inference(step,[status(thm)],[t273916,t42]) ).
cnf(t5207,plain,
meet(meet(X1,X2),join(X3,join(join(X1,X4),meet(X1,meet(X2,Y4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t273917]) ).
cnf(t5347,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,join(join(X3,Y4),meet(X3,meet(X4,Y5))))))) = meet(X1,join(X2,meet(meet(X3,X4),join(X1,meet(X3,X4))))),
inference(cp,[status(thm)],[t33,t5207]) ).
cnf(t273918,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(meet(X3,X4),join(X1,meet(X3,X4))))),
inference(step,[status(thm)],[t5347,t5207]) ).
cnf(t5379,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,meet(X3,X4))))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t273918]) ).
cnf(t5384,plain,
meet(X1,join(X2,meet(X3,X3))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X3))))),
inference(cp,[status(thm)],[t5379,t9]) ).
cnf(t273919,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X3))))),
inference(step,[status(thm)],[t5384,t9]) ).
cnf(t273920,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X1,X3)))),
inference(step,[status(thm)],[t273919,t9]) ).
cnf(t5485,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t273920]) ).
cnf(t5492,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X2,meet(join(X3,meet(X1,X4)),join(X1,X3)))),
inference(cp,[status(thm)],[t5485,t93]) ).
cnf(t273944,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X2,meet(join(X1,X3),join(X3,meet(X1,X4))))),
inference(step,[status(thm)],[t5492,t13]) ).
cnf(t7443,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X3,meet(X1,X4))))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t273944]) ).
cnf(t7492,plain,
meet(join(X1,X2),meet(join(X2,meet(X1,X3)),X1)) = meet(join(X1,X2),meet(X1,join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3))))),
inference(cp,[status(thm)],[t247,t7443]) ).
cnf(t273945,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(join(X1,X2),meet(X1,join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3))))),
inference(step,[status(thm)],[t7492,t15]) ).
cnf(t273946,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,meet(join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3))),join(X1,X2))),
inference(step,[status(thm)],[t273945,t15]) ).
cnf(t273947,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t273946,t83]) ).
cnf(t273948,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t273947,t11]) ).
cnf(t7575,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t273948]) ).
cnf(t7613,plain,
meet(X1,join(X1,X2)) = meet(meet(X1,join(X1,X2)),join(join(X1,X3),meet(X1,join(X2,meet(X1,X4))))),
inference(cp,[status(thm)],[t5048,t7575]) ).
cnf(t273949,plain,
X1 = meet(meet(X1,join(X1,X2)),join(join(X1,X3),meet(X1,join(X2,meet(X1,X4))))),
inference(step,[status(thm)],[t7613,t10]) ).
cnf(t273950,plain,
X1 = meet(X1,join(join(X1,X3),meet(X1,join(X2,meet(X1,X4))))),
inference(step,[status(thm)],[t273949,t10]) ).
cnf(t7677,plain,
meet(X1,join(join(X1,X2),meet(X1,join(X3,meet(X1,X4))))) = X1,
inference(orient,[status(thm)],[t273950]) ).
cnf(t7701,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(meet(X1,X2),X3),meet(X1,X2))),
inference(cp,[status(thm)],[t7677,t4614]) ).
cnf(t273951,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,X2),join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t7701,t42]) ).
cnf(t273952,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t273951,t74]) ).
cnf(t273953,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t273952,t42]) ).
cnf(t7811,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t273953]) ).
cnf(t7889,plain,
meet(meet(X1,X2),meet(X3,meet(join(X4,meet(X1,X2)),Y4))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),join(meet(X1,X2),Y5)))))),
inference(cp,[status(thm)],[t1634,t7811]) ).
cnf(t273972,plain,
meet(X3,meet(meet(join(X4,meet(X1,X2)),Y4),meet(X1,X2))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),join(meet(X1,X2),Y5)))))),
inference(step,[status(thm)],[t7889,t15]) ).
cnf(t273973,plain,
meet(X3,meet(X2,meet(meet(join(X4,meet(X1,X2)),Y4),X1))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),join(meet(X1,X2),Y5)))))),
inference(step,[status(thm)],[t273972,t15]) ).
cnf(t273974,plain,
meet(X3,meet(X1,meet(X2,meet(join(X4,meet(X1,X2)),Y4)))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),join(meet(X1,X2),Y5)))))),
inference(step,[status(thm)],[t273973,t15]) ).
cnf(t273975,plain,
meet(X1,meet(meet(X2,meet(join(X4,meet(X1,X2)),Y4)),X3)) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),join(meet(X1,X2),Y5)))))),
inference(step,[status(thm)],[t273974,t15]) ).
cnf(t273976,plain,
meet(X1,meet(X3,meet(X2,meet(join(X4,meet(X1,X2)),Y4)))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),join(meet(X1,X2),Y5)))))),
inference(step,[status(thm)],[t273975,t13]) ).
cnf(t273977,plain,
meet(X1,meet(X2,meet(meet(join(X4,meet(X1,X2)),Y4),X3))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),join(meet(X1,X2),Y5)))))),
inference(step,[status(thm)],[t273976,t15]) ).
cnf(t273978,plain,
meet(X1,meet(X2,meet(X3,meet(join(X4,meet(X1,X2)),Y4)))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),join(meet(X1,X2),Y5)))))),
inference(step,[status(thm)],[t273977,t13]) ).
cnf(t273979,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),join(meet(X1,X2),Y5)))))),
inference(step,[status(thm)],[t273978,t13]) ).
cnf(t91,plain,
meet(X1,meet(meet(X2,join(X1,X3)),X4)) = meet(X4,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t83]) ).
cnf(t273622,plain,
meet(X1,meet(X4,meet(X2,join(X1,X3)))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t91,t13]) ).
cnf(t273623,plain,
meet(X1,meet(X2,meet(join(X1,X3),X4))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t273622,t15]) ).
cnf(t273624,plain,
meet(X1,meet(X2,meet(X4,join(X1,X3)))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t273623,t13]) ).
cnf(t273625,plain,
meet(X1,meet(X2,meet(X4,join(X1,X3)))) = meet(X2,meet(X4,X1)),
inference(step,[status(thm)],[t273624,t15]) ).
cnf(t273626,plain,
meet(X1,meet(X2,meet(X4,join(X1,X3)))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t273625,t15]) ).
cnf(t104,plain,
meet(X1,meet(X2,meet(X3,join(X1,X4)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t273626]) ).
cnf(t273980,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(meet(X1,X2),meet(X3,Y4)),
inference(step,[status(thm)],[t273979,t104]) ).
cnf(t273981,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(Y4,meet(meet(X1,X2),X3)),
inference(step,[status(thm)],[t273980,t15]) ).
cnf(t273982,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X3,meet(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t273981,t15]) ).
cnf(t273983,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X3,meet(X2,meet(Y4,X1))),
inference(step,[status(thm)],[t273982,t15]) ).
cnf(t273984,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X3,meet(X1,meet(X2,Y4))),
inference(step,[status(thm)],[t273983,t15]) ).
cnf(t273985,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(meet(X2,Y4),X3)),
inference(step,[status(thm)],[t273984,t15]) ).
cnf(t273986,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(X3,meet(X2,Y4))),
inference(step,[status(thm)],[t273985,t13]) ).
cnf(t273987,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(X2,meet(Y4,X3))),
inference(step,[status(thm)],[t273986,t15]) ).
cnf(t273988,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(X2,meet(X3,Y4))),
inference(step,[status(thm)],[t273987,t13]) ).
cnf(t9198,plain,
meet(X1,meet(X2,meet(X3,meet(X4,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t273988]) ).
cnf(t9204,plain,
meet(X1,meet(X2,meet(X2,X3))) = meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X2))))),
inference(cp,[status(thm)],[t9198,t66]) ).
cnf(t273989,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X2))))),
inference(step,[status(thm)],[t9204,t66]) ).
cnf(t9401,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X2))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t273989]) ).
cnf(t9409,plain,
meet(X1,meet(X2,X2)) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t9401,t66]) ).
cnf(t273990,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t9409,t9]) ).
cnf(t9589,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t273990]) ).
cnf(t9689,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,join(meet(X2,join(X3,meet(X1,X2))),meet(X1,X2))),
inference(cp,[status(thm)],[t227,t9589]) ).
cnf(t273994,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X3,meet(X1,X2))),meet(X1,X2))),
inference(step,[status(thm)],[t9689,t9589]) ).
cnf(t273995,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t273994,t42]) ).
cnf(t10275,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X3,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t273995]) ).
cnf(t10489,plain,
meet(X1,meet(X2,join(meet(X2,X3),meet(X1,X3)))) = meet(X1,meet(X2,X3)),
inference(cp,[status(thm)],[t414,t10275]) ).
cnf(t273996,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X2,X3)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t10489,t42]) ).
cnf(t10525,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X2,X3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t273996]) ).
cnf(t7621,plain,
meet(X1,join(X1,X2)) = meet(meet(X1,join(X1,X2)),join(X3,join(join(X1,X4),meet(X1,join(X2,meet(X1,Y4)))))),
inference(cp,[status(thm)],[t5207,t7575]) ).
cnf(t273968,plain,
X1 = meet(meet(X1,join(X1,X2)),join(X3,join(join(X1,X4),meet(X1,join(X2,meet(X1,Y4)))))),
inference(step,[status(thm)],[t7621,t10]) ).
cnf(t273969,plain,
X1 = meet(X1,join(X3,join(join(X1,X4),meet(X1,join(X2,meet(X1,Y4)))))),
inference(step,[status(thm)],[t273968,t10]) ).
cnf(t8748,plain,
meet(X1,join(X2,join(join(X1,X3),meet(X1,join(X4,meet(X1,Y4)))))) = X1,
inference(orient,[status(thm)],[t273969]) ).
cnf(t8774,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(join(meet(X1,X2),X4),meet(X1,X2)))),
inference(cp,[status(thm)],[t8748,t4614]) ).
cnf(t274038,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),join(meet(X1,X2),X4)))),
inference(step,[status(thm)],[t8774,t42]) ).
cnf(t274039,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),X4))),
inference(step,[status(thm)],[t274038,t74]) ).
cnf(t274040,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t274039,t42]) ).
cnf(t12663,plain,
meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t274040]) ).
cnf(t12705,plain,
meet(meet(X1,X2),meet(X3,join(X4,join(Y4,meet(X1,X2))))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,join(Y4,meet(X1,X2))))))),
inference(cp,[status(thm)],[t10525,t12663]) ).
cnf(t274041,plain,
meet(X3,meet(join(X4,join(Y4,meet(X1,X2))),meet(X1,X2))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,join(Y4,meet(X1,X2))))))),
inference(step,[status(thm)],[t12705,t15]) ).
cnf(t274042,plain,
meet(X3,meet(X2,meet(join(X4,join(Y4,meet(X1,X2))),X1))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,join(Y4,meet(X1,X2))))))),
inference(step,[status(thm)],[t274041,t15]) ).
cnf(t274043,plain,
meet(X3,meet(X1,meet(X2,join(X4,join(Y4,meet(X1,X2)))))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,join(Y4,meet(X1,X2))))))),
inference(step,[status(thm)],[t274042,t15]) ).
cnf(t274044,plain,
meet(X1,meet(meet(X2,join(X4,join(Y4,meet(X1,X2)))),X3)) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,join(Y4,meet(X1,X2))))))),
inference(step,[status(thm)],[t274043,t15]) ).
cnf(t274045,plain,
meet(X1,meet(X3,meet(X2,join(X4,join(Y4,meet(X1,X2)))))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,join(Y4,meet(X1,X2))))))),
inference(step,[status(thm)],[t274044,t13]) ).
cnf(t274046,plain,
meet(X1,meet(X2,meet(join(X4,join(Y4,meet(X1,X2))),X3))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,join(Y4,meet(X1,X2))))))),
inference(step,[status(thm)],[t274045,t15]) ).
cnf(t274047,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,join(Y4,meet(X1,X2))))))),
inference(step,[status(thm)],[t274046,t13]) ).
cnf(t274048,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t274047,t83]) ).
cnf(t274049,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t274048,t13]) ).
cnf(t274050,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t274049,t15]) ).
cnf(t274051,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t274050,t15]) ).
cnf(t12779,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274051]) ).
cnf(t12783,plain,
meet(X1,meet(X2,X2)) = meet(X1,meet(X2,join(X3,join(X4,meet(X1,X2))))),
inference(cp,[status(thm)],[t12779,t66]) ).
cnf(t274052,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,join(X4,meet(X1,X2))))),
inference(step,[status(thm)],[t12783,t9]) ).
cnf(t12948,plain,
meet(X1,meet(X2,join(X3,join(X4,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t274052]) ).
cnf(t13026,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(meet(X2,join(X1,X3)),join(X4,join(Y4,meet(X1,X2))))),
inference(cp,[status(thm)],[t12948,t83]) ).
cnf(t274063,plain,
meet(X1,X2) = meet(X1,meet(meet(X2,join(X1,X3)),join(X4,join(Y4,meet(X1,X2))))),
inference(step,[status(thm)],[t13026,t83]) ).
cnf(t14020,plain,
meet(X1,meet(meet(X2,join(X1,X3)),join(X4,join(Y4,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t274063]) ).
cnf(t302,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X3,join(X2,X4)))))) = meet(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X2,X3))))),
inference(cp,[status(thm)],[t33,t273]) ).
cnf(t273781,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X3,join(X2,X4)))))) = meet(X1,join(meet(X2,X3),meet(X1,X2))),
inference(step,[status(thm)],[t302,t204]) ).
cnf(t273782,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X3,join(X2,X4)))))) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t273781,t42]) ).
cnf(t2216,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X3,join(X2,X4)))))) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(orient,[status(thm)],[t273782]) ).
cnf(t2293,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X3,join(meet(X3,X1),meet(X1,X2)))),
inference(cp,[status(thm)],[t83,t2216]) ).
cnf(t273783,plain,
meet(X3,meet(X1,X2)) = meet(meet(X1,X2),meet(X3,join(meet(X3,X1),meet(X1,X2)))),
inference(step,[status(thm)],[t2293,t13]) ).
cnf(t273784,plain,
meet(X2,meet(X3,X1)) = meet(meet(X1,X2),meet(X3,join(meet(X3,X1),meet(X1,X2)))),
inference(step,[status(thm)],[t273783,t15]) ).
cnf(t273785,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),meet(X3,join(meet(X3,X1),meet(X1,X2)))),
inference(step,[status(thm)],[t273784,t15]) ).
cnf(t273786,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(join(meet(X3,X1),meet(X1,X2)),meet(X1,X2))),
inference(step,[status(thm)],[t273785,t15]) ).
cnf(t273787,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X2,meet(join(meet(X3,X1),meet(X1,X2)),X1))),
inference(step,[status(thm)],[t273786,t15]) ).
cnf(t273788,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,meet(X2,join(meet(X3,X1),meet(X1,X2))))),
inference(step,[status(thm)],[t273787,t15]) ).
cnf(t273789,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,join(meet(X3,X1),meet(X1,X2))),X3)),
inference(step,[status(thm)],[t273788,t15]) ).
cnf(t273790,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X3,meet(X2,join(meet(X3,X1),meet(X1,X2))))),
inference(step,[status(thm)],[t273789,t13]) ).
cnf(t273791,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(join(meet(X3,X1),meet(X1,X2)),X3))),
inference(step,[status(thm)],[t273790,t15]) ).
cnf(t273792,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(X3,join(meet(X3,X1),meet(X1,X2))))),
inference(step,[status(thm)],[t273791,t13]) ).
cnf(t273793,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(X3,join(meet(X1,X2),meet(X3,X1))))),
inference(step,[status(thm)],[t273792,t42]) ).
cnf(t273794,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(X3,join(meet(X1,X2),meet(X1,X3))))),
inference(step,[status(thm)],[t273793,t13]) ).
cnf(t2348,plain,
meet(X1,meet(X2,meet(X3,join(meet(X1,X2),meet(X1,X3))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t273794]) ).
cnf(t2425,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(X1,meet(X2,meet(meet(X1,X3),join(meet(X1,X2),meet(X1,X3))))),
inference(cp,[status(thm)],[t2348,t66]) ).
cnf(t273812,plain,
meet(X1,meet(X1,meet(X3,X2))) = meet(X1,meet(X2,meet(meet(X1,X3),join(meet(X1,X2),meet(X1,X3))))),
inference(step,[status(thm)],[t2425,t15]) ).
cnf(t273813,plain,
meet(X1,meet(X3,X2)) = meet(X1,meet(X2,meet(meet(X1,X3),join(meet(X1,X2),meet(X1,X3))))),
inference(step,[status(thm)],[t273812,t66]) ).
cnf(t273814,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(meet(X1,X3),join(meet(X1,X2),meet(X1,X3))))),
inference(step,[status(thm)],[t273813,t13]) ).
cnf(t2612,plain,
meet(X1,meet(X2,meet(meet(X1,X3),join(meet(X1,X2),meet(X1,X3))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t273814]) ).
cnf(t5560,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,join(meet(X2,X3),meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t2216,t5485]) ).
cnf(t5847,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,X3)))) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(orient,[status(thm)],[t5560]) ).
cnf(t376,plain,
join(X1,X2) = meet(join(X1,X2),join(join(join(X1,X2),meet(X3,join(X1,X2))),X1)),
inference(cp,[status(thm)],[t359,t359]) ).
cnf(t273688,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(join(X1,X2),meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t376,t42]) ).
cnf(t608,plain,
meet(join(X1,X2),join(X1,join(join(X1,X2),meet(X3,join(X1,X2))))) = join(X1,X2),
inference(orient,[status(thm)],[t273688]) ).
cnf(t5914,plain,
meet(X1,join(meet(X1,join(X2,X3)),meet(join(X2,X3),join(X2,join(join(X2,X3),meet(X4,join(X2,X3))))))) = meet(X1,join(join(X2,X3),meet(join(X2,X3),join(X1,join(X2,join(join(X2,X3),meet(X4,join(X2,X3)))))))),
inference(cp,[status(thm)],[t5847,t608]) ).
cnf(t273925,plain,
meet(X1,join(meet(X1,join(X2,X3)),join(X2,X3))) = meet(X1,join(join(X2,X3),meet(join(X2,X3),join(X1,join(X2,join(join(X2,X3),meet(X4,join(X2,X3)))))))),
inference(step,[status(thm)],[t5914,t608]) ).
cnf(t273926,plain,
meet(X1,join(X3,join(meet(X1,join(X2,X3)),X2))) = meet(X1,join(join(X2,X3),meet(join(X2,X3),join(X1,join(X2,join(join(X2,X3),meet(X4,join(X2,X3)))))))),
inference(step,[status(thm)],[t273925,t46]) ).
cnf(t273927,plain,
meet(X1,join(X2,join(X3,meet(X1,join(X2,X3))))) = meet(X1,join(join(X2,X3),meet(join(X2,X3),join(X1,join(X2,join(join(X2,X3),meet(X4,join(X2,X3)))))))),
inference(step,[status(thm)],[t273926,t46]) ).
cnf(t273928,plain,
meet(X1,join(X2,join(X3,meet(X1,join(X2,X3))))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t273927,t12]) ).
cnf(t6037,plain,
meet(X1,join(X2,join(X3,meet(X1,join(X2,X3))))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t273928]) ).
cnf(t6095,plain,
meet(X1,meet(X2,join(X3,join(X4,meet(X1,join(X3,X4)))))) = meet(X1,meet(X2,meet(meet(X1,join(X3,X4)),join(meet(X1,X2),meet(X1,join(X3,join(X4,meet(X1,join(X3,X4))))))))),
inference(cp,[status(thm)],[t2612,t6037]) ).
cnf(t273938,plain,
meet(X1,meet(X2,join(X3,join(X4,meet(X1,join(X3,X4)))))) = meet(X1,meet(X2,meet(meet(X1,join(X3,X4)),join(meet(X1,X2),meet(X1,join(X3,X4)))))),
inference(step,[status(thm)],[t6095,t6037]) ).
cnf(t273939,plain,
meet(X1,meet(X2,join(X3,join(X4,meet(X1,join(X3,X4)))))) = meet(X1,meet(X2,join(X3,X4))),
inference(step,[status(thm)],[t273938,t2612]) ).
cnf(t6743,plain,
meet(X1,meet(X2,join(X3,join(X4,meet(X1,join(X3,X4)))))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t273939]) ).
cnf(t14021,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(meet(join(X2,X3),join(X1,X4)),join(X2,X3))),
inference(cp,[status(thm)],[t14020,t6743]) ).
cnf(t274064,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),meet(join(X2,X3),join(X1,X4)))),
inference(step,[status(thm)],[t14021,t13]) ).
cnf(t274065,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,X4))),
inference(step,[status(thm)],[t274064,t66]) ).
cnf(t274066,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X4),join(X2,X3))),
inference(step,[status(thm)],[t274065,t13]) ).
cnf(t14219,plain,
meet(X1,meet(join(X1,X2),join(X3,X4))) = meet(X1,join(X3,X4)),
inference(orient,[status(thm)],[t274066]) ).
cnf(t14239,plain,
meet(X1,join(X2,meet(X3,join(join(X1,X4),X3)))) = meet(X1,meet(join(X1,X4),join(X2,X3))),
inference(cp,[status(thm)],[t14219,t5485]) ).
cnf(t274073,plain,
meet(X1,join(X2,meet(X3,join(X3,join(X1,X4))))) = meet(X1,meet(join(X1,X4),join(X2,X3))),
inference(step,[status(thm)],[t14239,t42]) ).
cnf(t274074,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X4,X3))))) = meet(X1,meet(join(X1,X4),join(X2,X3))),
inference(step,[status(thm)],[t274073,t46]) ).
cnf(t274075,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X3,X4))))) = meet(X1,meet(join(X1,X4),join(X2,X3))),
inference(step,[status(thm)],[t274074,t42]) ).
cnf(t274076,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X3,X4))))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t274075,t14219]) ).
cnf(t14957,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X3,X4))))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t274076]) ).
cnf(t14958,plain,
meet(X1,join(join(X2,X3),X2)) = meet(X1,join(join(X2,X3),meet(X1,X2))),
inference(cp,[status(thm)],[t14957,t204]) ).
cnf(t274077,plain,
meet(X1,join(X2,join(X2,X3))) = meet(X1,join(join(X2,X3),meet(X1,X2))),
inference(step,[status(thm)],[t14958,t42]) ).
cnf(t274078,plain,
meet(X1,join(X2,X3)) = meet(X1,join(join(X2,X3),meet(X1,X2))),
inference(step,[status(thm)],[t274077,t74]) ).
cnf(t274079,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t274078,t42]) ).
cnf(t274080,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X3,join(meet(X1,X2),X2))),
inference(step,[status(thm)],[t274079,t46]) ).
cnf(t274081,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t274080,t46]) ).
cnf(t15081,plain,
meet(X1,join(X2,join(X3,meet(X1,X2)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t274081]) ).
cnf(t15275,plain,
meet(X1,meet(join(X2,join(X3,meet(X1,X2))),X4)) = meet(X4,meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t15,t15081]) ).
cnf(t274095,plain,
meet(X1,meet(X4,join(X2,join(X3,meet(X1,X2))))) = meet(X4,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t15275,t13]) ).
cnf(t274096,plain,
meet(X1,meet(X4,join(X2,join(X3,meet(X1,X2))))) = meet(X1,meet(join(X2,X3),X4)),
inference(step,[status(thm)],[t274095,t15]) ).
cnf(t274097,plain,
meet(X1,meet(X4,join(X2,join(X3,meet(X1,X2))))) = meet(X1,meet(X4,join(X2,X3))),
inference(step,[status(thm)],[t274096,t13]) ).
cnf(t16016,plain,
meet(X1,meet(X2,join(X3,join(X4,meet(X1,X3))))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t274097]) ).
cnf(t16024,plain,
meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t16016,t12663]) ).
cnf(t274098,plain,
meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(X1,X2),
inference(step,[status(thm)],[t16024,t66]) ).
cnf(t16201,plain,
meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t274098]) ).
cnf(t14350,plain,
meet(X1,meet(meet(join(X1,X2),join(X3,X4)),Y4)) = meet(Y4,meet(X1,join(X3,X4))),
inference(cp,[status(thm)],[t15,t14219]) ).
cnf(t274090,plain,
meet(X1,meet(Y4,meet(join(X1,X2),join(X3,X4)))) = meet(Y4,meet(X1,join(X3,X4))),
inference(step,[status(thm)],[t14350,t13]) ).
cnf(t274091,plain,
meet(X1,meet(Y4,meet(join(X1,X2),join(X3,X4)))) = meet(X1,meet(join(X3,X4),Y4)),
inference(step,[status(thm)],[t274090,t15]) ).
cnf(t274092,plain,
meet(X1,meet(Y4,meet(join(X1,X2),join(X3,X4)))) = meet(X1,meet(Y4,join(X3,X4))),
inference(step,[status(thm)],[t274091,t13]) ).
cnf(t15595,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(X4,Y4)))) = meet(X1,meet(X2,join(X4,Y4))),
inference(orient,[status(thm)],[t274092]) ).
cnf(t15606,plain,
meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))) = meet(X1,meet(X2,join(X1,X4))),
inference(cp,[status(thm)],[t15595,t9589]) ).
cnf(t274093,plain,
meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))) = meet(X1,X2),
inference(step,[status(thm)],[t15606,t83]) ).
cnf(t15737,plain,
meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t274093]) ).
cnf(t15741,plain,
meet(X1,join(X1,X2)) = meet(X1,join(X3,meet(join(X1,X2),join(X1,X4)))),
inference(cp,[status(thm)],[t15737,t14219]) ).
cnf(t274094,plain,
X1 = meet(X1,join(X3,meet(join(X1,X2),join(X1,X4)))),
inference(step,[status(thm)],[t15741,t10]) ).
cnf(t15857,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X1,X4)))) = X1,
inference(orient,[status(thm)],[t274094]) ).
cnf(t16216,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X1,X4)))) = meet(X1,meet(X1,join(join(X2,meet(join(X1,X3),join(X1,X4))),Y4))),
inference(cp,[status(thm)],[t16201,t15857]) ).
cnf(t274102,plain,
X1 = meet(X1,meet(X1,join(join(X2,meet(join(X1,X3),join(X1,X4))),Y4))),
inference(step,[status(thm)],[t16216,t15857]) ).
cnf(t274103,plain,
X1 = meet(X1,join(join(X2,meet(join(X1,X3),join(X1,X4))),Y4)),
inference(step,[status(thm)],[t274102,t66]) ).
cnf(t274104,plain,
X1 = meet(X1,join(Y4,join(X2,meet(join(X1,X3),join(X1,X4))))),
inference(step,[status(thm)],[t274103,t42]) ).
cnf(t274105,plain,
X1 = meet(X1,join(X2,join(meet(join(X1,X3),join(X1,X4)),Y4))),
inference(step,[status(thm)],[t274104,t46]) ).
cnf(t274106,plain,
X1 = meet(X1,join(X2,join(Y4,meet(join(X1,X3),join(X1,X4))))),
inference(step,[status(thm)],[t274105,t42]) ).
cnf(t16644,plain,
meet(X1,join(X2,join(X3,meet(join(X1,X4),join(X1,Y4))))) = X1,
inference(orient,[status(thm)],[t274106]) ).
cnf(t16791,plain,
meet(X1,join(join(X2,X3),meet(X2,join(X1,X4)))) = meet(X1,join(join(X2,X3),X2)),
inference(cp,[status(thm)],[t646,t16644]) ).
cnf(t274116,plain,
meet(X1,join(join(X2,X3),meet(X2,join(X1,X4)))) = meet(X1,join(X2,join(X2,X3))),
inference(step,[status(thm)],[t16791,t42]) ).
cnf(t274117,plain,
meet(X1,join(join(X2,X3),meet(X2,join(X1,X4)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t274116,t74]) ).
cnf(t17303,plain,
meet(X1,join(join(X2,X3),meet(X2,join(X1,X4)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t274117]) ).
cnf(t17378,plain,
meet(join(X1,X2),X3) = meet(join(X1,X2),join(X3,meet(meet(X3,X4),join(X1,X2)))),
inference(cp,[status(thm)],[t4783,t17303]) ).
cnf(t274167,plain,
meet(X3,join(X1,X2)) = meet(join(X1,X2),join(X3,meet(meet(X3,X4),join(X1,X2)))),
inference(step,[status(thm)],[t17378,t13]) ).
cnf(t19841,plain,
meet(join(X1,X2),join(X3,meet(meet(X3,X4),join(X1,X2)))) = meet(X3,join(X1,X2)),
inference(orient,[status(thm)],[t274167]) ).
cnf(t19948,plain,
join(join(X1,X2),X3) = join(join(X1,X2),join(X3,meet(X4,join(X1,X2)))),
inference(cp,[status(thm)],[t93,t19841]) ).
cnf(t274178,plain,
join(X3,join(X1,X2)) = join(join(X1,X2),join(X3,meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t19948,t42]) ).
cnf(t274179,plain,
join(X2,join(X3,X1)) = join(join(X1,X2),join(X3,meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t274178,t46]) ).
cnf(t274180,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),join(X3,meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t274179,t46]) ).
cnf(t274181,plain,
join(X1,join(X2,X3)) = join(X3,join(meet(X4,join(X1,X2)),join(X1,X2))),
inference(step,[status(thm)],[t274180,t46]) ).
cnf(t274182,plain,
join(X1,join(X2,X3)) = join(X3,join(X2,join(meet(X4,join(X1,X2)),X1))),
inference(step,[status(thm)],[t274181,t46]) ).
cnf(t274183,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,join(X2,meet(X4,join(X1,X2))))),
inference(step,[status(thm)],[t274182,t46]) ).
cnf(t274184,plain,
join(X1,join(X2,X3)) = join(X1,join(join(X2,meet(X4,join(X1,X2))),X3)),
inference(step,[status(thm)],[t274183,t46]) ).
cnf(t274185,plain,
join(X1,join(X2,X3)) = join(X1,join(X3,join(X2,meet(X4,join(X1,X2))))),
inference(step,[status(thm)],[t274184,t42]) ).
cnf(t274186,plain,
join(X1,join(X2,X3)) = join(X1,join(X2,join(meet(X4,join(X1,X2)),X3))),
inference(step,[status(thm)],[t274185,t46]) ).
cnf(t274187,plain,
join(X1,join(X2,X3)) = join(X1,join(X2,join(X3,meet(X4,join(X1,X2))))),
inference(step,[status(thm)],[t274186,t42]) ).
cnf(t20948,plain,
join(X1,join(X2,join(X3,meet(X4,join(X1,X2))))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t274187]) ).
cnf(t20951,plain,
join(X1,join(X2,X2)) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t20948,t74]) ).
cnf(t274188,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t20951,t11]) ).
cnf(t21069,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t274188]) ).
cnf(t19945,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(cp,[status(thm)],[t12,t19841]) ).
cnf(t20086,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t19945]) ).
cnf(t19943,plain,
meet(join(X1,X2),join(X3,meet(meet(X3,X4),join(X1,X2)))) = meet(meet(X3,join(X1,X2)),join(join(X1,X2),Y4)),
inference(cp,[status(thm)],[t4614,t19841]) ).
cnf(t274169,plain,
meet(X3,join(X1,X2)) = meet(meet(X3,join(X1,X2)),join(join(X1,X2),Y4)),
inference(step,[status(thm)],[t19943,t19841]) ).
cnf(t274170,plain,
meet(X3,join(X1,X2)) = meet(meet(X3,join(X1,X2)),join(Y4,join(X1,X2))),
inference(step,[status(thm)],[t274169,t42]) ).
cnf(t274171,plain,
meet(X3,join(X1,X2)) = meet(meet(X3,join(X1,X2)),join(X2,join(Y4,X1))),
inference(step,[status(thm)],[t274170,t46]) ).
cnf(t274172,plain,
meet(X3,join(X1,X2)) = meet(meet(X3,join(X1,X2)),join(X1,join(X2,Y4))),
inference(step,[status(thm)],[t274171,t46]) ).
cnf(t20267,plain,
meet(meet(X1,join(X2,X3)),join(X2,join(X3,X4))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t274172]) ).
cnf(t20321,plain,
meet(X1,join(X2,X2)) = meet(meet(X1,X2),join(X2,join(X2,X3))),
inference(cp,[status(thm)],[t20267,t11]) ).
cnf(t274173,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,join(X2,X3))),
inference(step,[status(thm)],[t20321,t11]) ).
cnf(t274174,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t274173,t74]) ).
cnf(t20437,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t274174]) ).
cnf(t20534,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(cp,[status(thm)],[t20437,t83]) ).
cnf(t274176,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(step,[status(thm)],[t20534,t83]) ).
cnf(t274177,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t274176,t42]) ).
cnf(t20681,plain,
meet(meet(X1,X2),join(X3,meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t274177]) ).
cnf(t20836,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,meet(X2,X3))),
inference(cp,[status(thm)],[t20681,t5207]) ).
cnf(t21314,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X2,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t20836]) ).
cnf(t21419,plain,
join(X1,meet(X2,X3)) = join(join(X1,meet(X2,X3)),meet(X4,meet(X2,X3))),
inference(cp,[status(thm)],[t20086,t21314]) ).
cnf(t274192,plain,
join(X1,meet(X2,X3)) = join(meet(X4,meet(X2,X3)),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t21419,t42]) ).
cnf(t274193,plain,
join(X1,meet(X2,X3)) = join(meet(X2,X3),join(meet(X4,meet(X2,X3)),X1)),
inference(step,[status(thm)],[t274192,t46]) ).
cnf(t274194,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X4,meet(X2,X3)))),
inference(step,[status(thm)],[t274193,t46]) ).
cnf(t274195,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X3,meet(X4,X2)))),
inference(step,[status(thm)],[t274194,t15]) ).
cnf(t274196,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X2,meet(X3,X4)))),
inference(step,[status(thm)],[t274195,t15]) ).
cnf(t21524,plain,
join(X1,join(meet(X2,X3),meet(X2,meet(X3,X4)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274196]) ).
cnf(t21525,plain,
join(meet(X1,X2),meet(X1,X2)) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t21524,t74]) ).
cnf(t274197,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t21525,t11]) ).
cnf(t21675,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t274197]) ).
cnf(t21778,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X1,meet(X4,join(X2,X3)))),
inference(cp,[status(thm)],[t21675,t19841]) ).
cnf(t29802,plain,
join(meet(X1,join(X2,X3)),meet(X1,meet(X4,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t21778]) ).
cnf(t29848,plain,
meet(X1,join(X2,meet(X1,X3))) = join(meet(X1,join(X2,meet(X1,X3))),meet(X1,X3)),
inference(cp,[status(thm)],[t29802,t9589]) ).
cnf(t274300,plain,
meet(X1,join(X2,meet(X1,X3))) = join(meet(X1,X3),meet(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t29848,t42]) ).
cnf(t30646,plain,
join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))) = meet(X1,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t274300]) ).
cnf(t30762,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t21069,t30646]) ).
cnf(t31167,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t30762]) ).
cnf(t20365,plain,
meet(X1,join(join(X2,X3),meet(X1,meet(X4,join(X1,X2))))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(cp,[status(thm)],[t204,t20267]) ).
cnf(t274262,plain,
meet(X1,join(join(X2,X3),meet(X1,X4))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t20365,t83]) ).
cnf(t274263,plain,
meet(X1,join(meet(X1,X4),join(X2,X3))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t274262,t42]) ).
cnf(t274264,plain,
meet(X1,join(X3,join(meet(X1,X4),X2))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t274263,t46]) ).
cnf(t274265,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t274264,t46]) ).
cnf(t27450,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t274265]) ).
cnf(t31176,plain,
join(join(X1,X2),meet(X3,join(X3,X1))) = join(join(X1,X2),meet(X3,join(X1,join(X2,meet(X3,X3))))),
inference(cp,[status(thm)],[t31167,t27450]) ).
cnf(t274323,plain,
join(join(X1,X2),X3) = join(join(X1,X2),meet(X3,join(X1,join(X2,meet(X3,X3))))),
inference(step,[status(thm)],[t31176,t10]) ).
cnf(t274324,plain,
join(X3,join(X1,X2)) = join(join(X1,X2),meet(X3,join(X1,join(X2,meet(X3,X3))))),
inference(step,[status(thm)],[t274323,t42]) ).
cnf(t274325,plain,
join(X2,join(X3,X1)) = join(join(X1,X2),meet(X3,join(X1,join(X2,meet(X3,X3))))),
inference(step,[status(thm)],[t274324,t46]) ).
cnf(t274326,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(X3,join(X1,join(X2,meet(X3,X3))))),
inference(step,[status(thm)],[t274325,t46]) ).
cnf(t274327,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(X3,join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t274326,t9]) ).
cnf(t32498,plain,
join(join(X1,X2),meet(X3,join(X1,join(X2,X3)))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t274327]) ).
cnf(t31169,plain,
join(X1,meet(X2,join(X2,join(X2,X3)))) = join(X1,meet(X2,join(X1,X2))),
inference(cp,[status(thm)],[t31167,t14957]) ).
cnf(t274307,plain,
join(X1,X2) = join(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t31169,t10]) ).
cnf(t31272,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t274307]) ).
cnf(t31380,plain,
join(X1,join(meet(X2,join(X1,X2)),X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t46,t31272]) ).
cnf(t274308,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X3,join(X1,X2)),
inference(step,[status(thm)],[t31380,t42]) ).
cnf(t274309,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X2,join(X3,X1)),
inference(step,[status(thm)],[t274308,t46]) ).
cnf(t274310,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t274309,t46]) ).
cnf(t31382,plain,
join(X1,join(X2,meet(X3,join(X1,X3)))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t274310]) ).
cnf(t32538,plain,
join(X1,join(X2,meet(X3,join(X1,X3)))) = join(join(X1,X2),meet(meet(X3,join(X1,X3)),join(X1,join(X3,X2)))),
inference(cp,[status(thm)],[t32498,t31382]) ).
cnf(t274328,plain,
join(X1,join(X3,X2)) = join(join(X1,X2),meet(meet(X3,join(X1,X3)),join(X1,join(X3,X2)))),
inference(step,[status(thm)],[t32538,t31382]) ).
cnf(t274329,plain,
join(X1,join(X3,X2)) = join(join(X1,X2),meet(X3,join(X1,X3))),
inference(step,[status(thm)],[t274328,t20267]) ).
cnf(t32733,plain,
join(join(X1,X2),meet(X3,join(X1,X3))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t274329]) ).
cnf(t32743,plain,
join(X1,join(X2,join(X3,meet(X4,join(X1,X3))))) = join(join(X1,X3),meet(X2,join(X1,X2))),
inference(cp,[status(thm)],[t32733,t21069]) ).
cnf(t274330,plain,
join(X1,join(X2,join(X3,meet(X4,join(X1,X3))))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t32743,t32733]) ).
cnf(t33195,plain,
join(X1,join(X2,join(X3,meet(X4,join(X1,X3))))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t274330]) ).
cnf(t224,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X3,X2)))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,meet(X3,X4))))))),
inference(cp,[status(thm)],[t33,t204]) ).
cnf(t273757,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X2,X3)))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,meet(X3,X4))))))),
inference(step,[status(thm)],[t224,t42]) ).
cnf(t273758,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X2,X3)))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))),
inference(step,[status(thm)],[t273757,t33]) ).
cnf(t1509,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X2,X3)))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))),
inference(orient,[status(thm)],[t273758]) ).
cnf(t37,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X2))))),
inference(cp,[status(thm)],[t33,t11]) ).
cnf(t273650,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t37,t13]) ).
cnf(t170,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,X3))))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(orient,[status(thm)],[t273650]) ).
cnf(t182,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X3,meet(X2,X4))))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,meet(X4,join(X3,X2)))))))),
inference(cp,[status(thm)],[t33,t170]) ).
cnf(t274487,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X3,meet(X2,X4))))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X3,X2)))))),
inference(step,[status(thm)],[t182,t33]) ).
cnf(t274488,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X3,meet(X2,X4))))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X2,X3)))))),
inference(step,[status(thm)],[t274487,t42]) ).
cnf(t274489,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X3,meet(X2,X4))))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))),
inference(step,[status(thm)],[t274488,t1509]) ).
cnf(t51133,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X4,join(X3,meet(X2,X4))))))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))),
inference(orient,[status(thm)],[t274489]) ).
cnf(t20096,plain,
join(X1,meet(join(X2,X3),join(X2,X4))) = join(join(X1,meet(join(X2,X3),join(X2,X4))),X2),
inference(cp,[status(thm)],[t20086,t15857]) ).
cnf(t274225,plain,
join(X1,meet(join(X2,X3),join(X2,X4))) = join(X2,join(X1,meet(join(X2,X3),join(X2,X4)))),
inference(step,[status(thm)],[t20096,t42]) ).
cnf(t274226,plain,
join(X1,meet(join(X2,X3),join(X2,X4))) = join(X1,join(meet(join(X2,X3),join(X2,X4)),X2)),
inference(step,[status(thm)],[t274225,t46]) ).
cnf(t274227,plain,
join(X1,meet(join(X2,X3),join(X2,X4))) = join(X1,join(X2,meet(join(X2,X3),join(X2,X4)))),
inference(step,[status(thm)],[t274226,t42]) ).
cnf(t25299,plain,
join(X1,join(X2,meet(join(X2,X3),join(X2,X4)))) = join(X1,meet(join(X2,X3),join(X2,X4))),
inference(orient,[status(thm)],[t274227]) ).
cnf(t32537,plain,
join(X1,join(X2,meet(join(X2,X3),join(X2,X4)))) = join(join(X1,X2),meet(meet(join(X2,X3),join(X2,X4)),join(X1,meet(join(X2,X3),join(X2,X4))))),
inference(cp,[status(thm)],[t32498,t25299]) ).
cnf(t274396,plain,
join(X1,meet(join(X2,X3),join(X2,X4))) = join(join(X1,X2),meet(meet(join(X2,X3),join(X2,X4)),join(X1,meet(join(X2,X3),join(X2,X4))))),
inference(step,[status(thm)],[t32537,t25299]) ).
cnf(t274397,plain,
join(X1,meet(join(X2,X3),join(X2,X4))) = join(join(X1,X2),meet(join(X2,X3),join(X2,X4))),
inference(step,[status(thm)],[t274396,t7811]) ).
cnf(t40579,plain,
join(join(X1,X2),meet(join(X2,X3),join(X2,X4))) = join(X1,meet(join(X2,X3),join(X2,X4))),
inference(orient,[status(thm)],[t274397]) ).
cnf(t51158,plain,
meet(join(X1,X2),join(X3,meet(X2,join(join(X1,X2),meet(X2,join(X2,X4)))))) = meet(join(X1,X2),join(X3,meet(X2,join(X1,meet(join(X2,X4),join(X2,meet(X3,join(X2,X4)))))))),
inference(cp,[status(thm)],[t51133,t40579]) ).
cnf(t19979,plain,
meet(X1,join(X2,X3)) = meet(X1,join(join(X2,X3),meet(X1,meet(X4,join(X2,X3))))),
inference(cp,[status(thm)],[t4782,t19841]) ).
cnf(t29322,plain,
meet(X1,join(join(X2,X3),meet(X1,meet(X4,join(X2,X3))))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t19979]) ).
cnf(t31178,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X2)))) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(cp,[status(thm)],[t31167,t29322]) ).
cnf(t274311,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X2)))) = join(X1,X2),
inference(step,[status(thm)],[t31178,t20086]) ).
cnf(t31482,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t274311]) ).
cnf(t21805,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))),
inference(cp,[status(thm)],[t12663,t21675]) ).
cnf(t21885,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t21805]) ).
cnf(t21887,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,X4))))) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
inference(cp,[status(thm)],[t21885,t442]) ).
cnf(t274198,plain,
meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t21887,t442]) ).
cnf(t22353,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274198]) ).
cnf(t22486,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(X4,meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t22353,t10]) ).
cnf(t274199,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t22486,t10]) ).
cnf(t22720,plain,
meet(meet(X1,X2),join(X3,meet(X1,join(X2,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t274199]) ).
cnf(t5487,plain,
meet(X1,join(X2,join(X3,meet(X2,X4)))) = meet(X1,join(X2,meet(join(X3,meet(X2,X4)),join(X1,X3)))),
inference(cp,[status(thm)],[t5485,t646]) ).
cnf(t273932,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(join(X3,meet(X2,X4)),join(X1,X3)))),
inference(step,[status(thm)],[t5487,t93]) ).
cnf(t273933,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(join(X1,X3),join(X3,meet(X2,X4))))),
inference(step,[status(thm)],[t273932,t13]) ).
cnf(t6296,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X3,meet(X2,X4))))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t273933]) ).
cnf(t6313,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X1,join(meet(X1,X3),meet(X2,X4))))),
inference(cp,[status(thm)],[t6296,t12]) ).
cnf(t6978,plain,
meet(X1,join(X2,meet(X1,join(meet(X1,X3),meet(X2,X4))))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t6313]) ).
cnf(t31171,plain,
join(X1,meet(X2,join(meet(X2,X3),meet(X1,X4)))) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t31167,t6978]) ).
cnf(t274321,plain,
join(X1,meet(X2,join(meet(X1,X4),meet(X2,X3)))) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t31171,t42]) ).
cnf(t274322,plain,
join(X1,meet(X2,join(meet(X1,X4),meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t274321,t31167]) ).
cnf(t32362,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X2,X4)))) = join(X1,meet(X2,X4)),
inference(orient,[status(thm)],[t274322]) ).
cnf(t32418,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X2,meet(X1,X4))),
inference(cp,[status(thm)],[t22720,t32362]) ).
cnf(t32983,plain,
meet(meet(X1,meet(X2,X3)),join(X2,meet(X1,X4))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t32418]) ).
cnf(t32996,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(meet(X1,meet(X3,X2)),join(X2,meet(X1,X4))),
inference(cp,[status(thm)],[t32983,t247]) ).
cnf(t274333,plain,
meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(X2,meet(X1,X4))),
inference(step,[status(thm)],[t32996,t247]) ).
cnf(t33779,plain,
meet(meet(X1,meet(X2,X3)),join(X3,meet(X1,X4))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274333]) ).
cnf(t31270,plain,
join(X1,join(meet(X2,join(X1,meet(X2,X3))),X4)) = join(X4,join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t46,t31167]) ).
cnf(t274348,plain,
join(X1,join(X4,meet(X2,join(X1,meet(X2,X3))))) = join(X4,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t31270,t42]) ).
cnf(t274349,plain,
join(X1,join(X4,meet(X2,join(X1,meet(X2,X3))))) = join(X1,join(meet(X2,X3),X4)),
inference(step,[status(thm)],[t274348,t46]) ).
cnf(t274350,plain,
join(X1,join(X4,meet(X2,join(X1,meet(X2,X3))))) = join(X1,join(X4,meet(X2,X3))),
inference(step,[status(thm)],[t274349,t42]) ).
cnf(t35807,plain,
join(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))) = join(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t274350]) ).
cnf(t40789,plain,
join(X1,join(join(X2,X1),meet(join(X1,X3),X4))) = join(X1,join(X2,meet(join(X1,X3),join(X1,meet(join(X1,X3),X4))))),
inference(cp,[status(thm)],[t35807,t40579]) ).
cnf(t274398,plain,
join(X1,join(join(X1,X2),meet(join(X1,X3),X4))) = join(X1,join(X2,meet(join(X1,X3),join(X1,meet(join(X1,X3),X4))))),
inference(step,[status(thm)],[t40789,t42]) ).
cnf(t274399,plain,
join(X1,join(join(X1,X2),meet(X4,join(X1,X3)))) = join(X1,join(X2,meet(join(X1,X3),join(X1,meet(join(X1,X3),X4))))),
inference(step,[status(thm)],[t274398,t13]) ).
cnf(t274400,plain,
join(X1,join(join(X1,X2),meet(X4,join(X1,X3)))) = join(X1,join(X2,meet(join(X1,X3),X4))),
inference(step,[status(thm)],[t274399,t35807]) ).
cnf(t274401,plain,
join(X1,join(join(X1,X2),meet(X4,join(X1,X3)))) = join(X1,join(X2,meet(X4,join(X1,X3)))),
inference(step,[status(thm)],[t274400,t13]) ).
cnf(t40861,plain,
join(X1,join(join(X1,X2),meet(X3,join(X1,X4)))) = join(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t274401]) ).
cnf(t40895,plain,
join(X1,join(meet(X1,X2),meet(X3,join(X1,X4)))) = join(X1,join(X1,meet(X3,join(X1,X4)))),
inference(cp,[status(thm)],[t40861,t12]) ).
cnf(t274403,plain,
join(X1,join(meet(X1,X2),meet(X3,join(X1,X4)))) = join(X1,meet(X3,join(X1,X4))),
inference(step,[status(thm)],[t40895,t74]) ).
cnf(t41186,plain,
join(X1,join(meet(X1,X2),meet(X3,join(X1,X4)))) = join(X1,meet(X3,join(X1,X4))),
inference(orient,[status(thm)],[t274403]) ).
cnf(t41191,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,join(meet(X1,X4),meet(X2,X3))),
inference(cp,[status(thm)],[t41186,t35807]) ).
cnf(t274404,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X1,X4),meet(X2,X3))),
inference(step,[status(thm)],[t41191,t31167]) ).
cnf(t41334,plain,
join(X1,join(meet(X1,X2),meet(X3,X4))) = join(X1,meet(X3,X4)),
inference(orient,[status(thm)],[t274404]) ).
cnf(t41369,plain,
join(X1,join(X2,join(meet(X1,X3),meet(X4,Y4)))) = join(join(X1,meet(X4,Y4)),meet(X2,join(X1,X2))),
inference(cp,[status(thm)],[t32733,t41334]) ).
cnf(t274408,plain,
join(X1,join(X2,join(meet(X1,X3),meet(X4,Y4)))) = join(X1,join(X2,meet(X4,Y4))),
inference(step,[status(thm)],[t41369,t32733]) ).
cnf(t41948,plain,
join(X1,join(X2,join(meet(X1,X3),meet(X4,Y4)))) = join(X1,join(X2,meet(X4,Y4))),
inference(orient,[status(thm)],[t274408]) ).
cnf(t1438,plain,
meet(X1,meet(join(X2,join(meet(X1,X2),meet(X1,X3))),X4)) = meet(X4,meet(X1,join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t15,t1370]) ).
cnf(t273754,plain,
meet(X1,meet(X4,join(X2,join(meet(X1,X2),meet(X1,X3))))) = meet(X4,meet(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t1438,t13]) ).
cnf(t273755,plain,
meet(X1,meet(X4,join(X2,join(meet(X1,X2),meet(X1,X3))))) = meet(X1,meet(join(X2,meet(X1,X3)),X4)),
inference(step,[status(thm)],[t273754,t15]) ).
cnf(t273756,plain,
meet(X1,meet(X4,join(X2,join(meet(X1,X2),meet(X1,X3))))) = meet(X1,meet(X4,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t273755,t13]) ).
cnf(t1440,plain,
meet(X1,meet(X2,join(X3,join(meet(X1,X3),meet(X1,X4))))) = meet(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t273756]) ).
cnf(t7819,plain,
meet(join(X1,X2),join(X1,join(join(X1,X2),meet(X3,join(X1,X2))))) = meet(join(X1,X2),join(X4,meet(join(X1,X2),join(X1,join(join(X1,X2),meet(X3,join(X1,X2))))))),
inference(cp,[status(thm)],[t7811,t608]) ).
cnf(t273957,plain,
join(X1,X2) = meet(join(X1,X2),join(X4,meet(join(X1,X2),join(X1,join(join(X1,X2),meet(X3,join(X1,X2))))))),
inference(step,[status(thm)],[t7819,t608]) ).
cnf(t273958,plain,
join(X1,X2) = meet(join(X1,X2),join(X4,join(X1,X2))),
inference(step,[status(thm)],[t273957,t608]) ).
cnf(t273959,plain,
join(X1,X2) = meet(join(X1,X2),join(X2,join(X4,X1))),
inference(step,[status(thm)],[t273958,t46]) ).
cnf(t273960,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X4))),
inference(step,[status(thm)],[t273959,t46]) ).
cnf(t7903,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t273960]) ).
cnf(t7953,plain,
meet(X1,meet(join(X2,meet(X1,X2)),join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t1440,t7903]) ).
cnf(t273964,plain,
meet(X1,meet(join(X2,meet(X1,X2)),join(X2,meet(X1,X3)))) = meet(X1,X2),
inference(step,[status(thm)],[t7953,t227]) ).
cnf(t8322,plain,
meet(X1,meet(join(X2,meet(X1,X2)),join(X2,meet(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t273964]) ).
cnf(t31523,plain,
join(X1,meet(X2,X3)) = join(join(X1,meet(X2,X3)),meet(X2,X1)),
inference(cp,[status(thm)],[t31482,t8322]) ).
cnf(t274312,plain,
join(X1,meet(X2,X3)) = join(meet(X2,X1),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t31523,t42]) ).
cnf(t274313,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X2,X1))),
inference(step,[status(thm)],[t274312,t46]) ).
cnf(t274314,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X1),meet(X2,X3))),
inference(step,[status(thm)],[t274313,t42]) ).
cnf(t274315,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t274314,t13]) ).
cnf(t31711,plain,
join(X1,join(meet(X1,X2),meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274315]) ).
cnf(t31894,plain,
join(X1,join(join(meet(X1,X2),meet(X2,X3)),X4)) = join(X4,join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t46,t31711]) ).
cnf(t274358,plain,
join(X1,join(X4,join(meet(X1,X2),meet(X2,X3)))) = join(X4,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t31894,t42]) ).
cnf(t274359,plain,
join(X1,join(X4,join(meet(X1,X2),meet(X2,X3)))) = join(X1,join(meet(X2,X3),X4)),
inference(step,[status(thm)],[t274358,t46]) ).
cnf(t274360,plain,
join(X1,join(X4,join(meet(X1,X2),meet(X2,X3)))) = join(X1,join(X4,meet(X2,X3))),
inference(step,[status(thm)],[t274359,t42]) ).
cnf(t36064,plain,
join(X1,join(X2,join(meet(X1,X3),meet(X3,X4)))) = join(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t274360]) ).
cnf(t36069,plain,
join(X1,join(X2,meet(X3,join(X2,meet(X1,X3))))) = join(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t36064,t21069]) ).
cnf(t274361,plain,
join(X1,join(X2,meet(X3,join(X2,meet(X1,X3))))) = join(X1,X2),
inference(step,[status(thm)],[t36069,t93]) ).
cnf(t36300,plain,
join(X1,join(X2,meet(X3,join(X2,meet(X1,X3))))) = join(X1,X2),
inference(orient,[status(thm)],[t274361]) ).
cnf(t36416,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X3),join(X2,X1)))),
inference(cp,[status(thm)],[t36300,t10]) ).
cnf(t274362,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X3),join(X1,X2)))),
inference(step,[status(thm)],[t36416,t42]) ).
cnf(t274363,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X2),join(X1,X3)))),
inference(step,[status(thm)],[t274362,t13]) ).
cnf(t36522,plain,
join(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = join(X1,X2),
inference(orient,[status(thm)],[t274363]) ).
cnf(t41958,plain,
join(X1,join(X2,meet(join(X2,meet(X1,X3)),join(X2,X4)))) = join(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t41948,t36522]) ).
cnf(t274411,plain,
join(X1,meet(join(X2,meet(X1,X3)),join(X2,X4))) = join(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t41958,t25299]) ).
cnf(t274412,plain,
join(X1,meet(join(X2,X4),join(X2,meet(X1,X3)))) = join(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t274411,t13]) ).
cnf(t274413,plain,
join(X1,meet(join(X2,X4),join(X2,meet(X1,X3)))) = join(X1,X2),
inference(step,[status(thm)],[t274412,t93]) ).
cnf(t42538,plain,
join(X1,meet(join(X2,X3),join(X2,meet(X1,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t274413]) ).
cnf(t42643,plain,
meet(join(X1,X2),meet(X3,X4)) = meet(meet(join(X1,X2),meet(X3,X4)),join(X4,X1)),
inference(cp,[status(thm)],[t33779,t42538]) ).
cnf(t274441,plain,
meet(X4,meet(join(X1,X2),X3)) = meet(meet(join(X1,X2),meet(X3,X4)),join(X4,X1)),
inference(step,[status(thm)],[t42643,t15]) ).
cnf(t274442,plain,
meet(X3,meet(X4,join(X1,X2))) = meet(meet(join(X1,X2),meet(X3,X4)),join(X4,X1)),
inference(step,[status(thm)],[t274441,t15]) ).
cnf(t274443,plain,
meet(X3,meet(X4,join(X1,X2))) = meet(join(X4,X1),meet(join(X1,X2),meet(X3,X4))),
inference(step,[status(thm)],[t274442,t13]) ).
cnf(t274444,plain,
meet(X3,meet(X4,join(X1,X2))) = meet(meet(X3,X4),meet(join(X4,X1),join(X1,X2))),
inference(step,[status(thm)],[t274443,t15]) ).
cnf(t274445,plain,
meet(X3,meet(X4,join(X1,X2))) = meet(meet(X3,X4),meet(join(X1,X2),join(X4,X1))),
inference(step,[status(thm)],[t274444,t13]) ).
cnf(t274446,plain,
meet(X3,meet(X4,join(X1,X2))) = meet(meet(X3,X4),meet(join(X1,X2),join(X1,X4))),
inference(step,[status(thm)],[t274445,t42]) ).
cnf(t45163,plain,
meet(meet(X1,X2),meet(join(X3,X4),join(X3,X2))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t274446]) ).
cnf(t45477,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(X2,join(X1,X4)))),
inference(cp,[status(thm)],[t31482,t45163]) ).
cnf(t274447,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,meet(join(X1,X4),X3))),
inference(step,[status(thm)],[t45477,t15]) ).
cnf(t274448,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,meet(X3,join(X1,X4)))),
inference(step,[status(thm)],[t274447,t13]) ).
cnf(t45604,plain,
join(join(X1,X2),meet(X2,meet(X3,join(X1,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t274448]) ).
cnf(t21839,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X4,meet(X1,X2)))),
inference(cp,[status(thm)],[t12948,t21675]) ).
cnf(t22132,plain,
meet(X1,meet(meet(X2,X3),join(X4,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t21839]) ).
cnf(t45664,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,meet(X3,X4))),
inference(cp,[status(thm)],[t45604,t22132]) ).
cnf(t45872,plain,
join(join(X1,X2),meet(X2,meet(X3,X4))) = join(X1,X2),
inference(orient,[status(thm)],[t45664]) ).
cnf(t7967,plain,
meet(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = meet(X1,join(X2,join(X1,X2))),
inference(cp,[status(thm)],[t185,t7903]) ).
cnf(t273961,plain,
meet(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = meet(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t7967,t46]) ).
cnf(t273962,plain,
meet(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = X1,
inference(step,[status(thm)],[t273961,t10]) ).
cnf(t7995,plain,
meet(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = X1,
inference(orient,[status(thm)],[t273962]) ).
cnf(t8011,plain,
X1 = meet(X1,join(join(X2,meet(X1,X3)),meet(join(X1,X2),join(X1,X4)))),
inference(cp,[status(thm)],[t7995,t93]) ).
cnf(t8892,plain,
meet(X1,join(join(X2,meet(X1,X3)),meet(join(X1,X2),join(X1,X4)))) = X1,
inference(orient,[status(thm)],[t8011]) ).
cnf(t8897,plain,
X1 = meet(X1,join(meet(join(X1,X2),join(X1,X3)),join(X2,meet(X1,X4)))),
inference(cp,[status(thm)],[t8892,t42]) ).
cnf(t273970,plain,
X1 = meet(X1,join(meet(X1,X4),join(meet(join(X1,X2),join(X1,X3)),X2))),
inference(step,[status(thm)],[t8897,t46]) ).
cnf(t273971,plain,
X1 = meet(X1,join(X2,join(meet(X1,X4),meet(join(X1,X2),join(X1,X3))))),
inference(step,[status(thm)],[t273970,t46]) ).
cnf(t9046,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(join(X1,X2),join(X1,X4))))) = X1,
inference(orient,[status(thm)],[t273971]) ).
cnf(t9193,plain,
meet(X1,join(join(X2,X1),meet(X2,join(X1,meet(X2,X3))))) = meet(X1,join(join(X2,X1),X2)),
inference(cp,[status(thm)],[t646,t9046]) ).
cnf(t273997,plain,
meet(X1,join(join(X1,X2),meet(X2,join(X1,meet(X2,X3))))) = meet(X1,join(join(X2,X1),X2)),
inference(step,[status(thm)],[t9193,t42]) ).
cnf(t273998,plain,
meet(X1,join(join(X1,X2),meet(X2,join(X1,meet(X2,X3))))) = meet(X1,join(X2,join(X2,X1))),
inference(step,[status(thm)],[t273997,t42]) ).
cnf(t273999,plain,
meet(X1,join(join(X1,X2),meet(X2,join(X1,meet(X2,X3))))) = meet(X1,join(X2,X1)),
inference(step,[status(thm)],[t273998,t74]) ).
cnf(t274000,plain,
meet(X1,join(join(X1,X2),meet(X2,join(X1,meet(X2,X3))))) = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t273999,t42]) ).
cnf(t274001,plain,
meet(X1,join(join(X1,X2),meet(X2,join(X1,meet(X2,X3))))) = X1,
inference(step,[status(thm)],[t274000,t10]) ).
cnf(t10759,plain,
meet(X1,join(join(X1,X2),meet(X2,join(X1,meet(X2,X3))))) = X1,
inference(orient,[status(thm)],[t274001]) ).
cnf(t10760,plain,
X1 = meet(X1,join(join(X1,X2),meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t10759,t33]) ).
cnf(t10875,plain,
meet(X1,join(join(X1,X2),meet(X2,join(X1,X3)))) = X1,
inference(orient,[status(thm)],[t10760]) ).
cnf(t20132,plain,
join(join(X1,X2),meet(X2,join(X1,X3))) = join(join(join(X1,X2),meet(X2,join(X1,X3))),X1),
inference(cp,[status(thm)],[t20086,t10875]) ).
cnf(t274235,plain,
join(join(X1,X2),meet(X2,join(X1,X3))) = join(X1,join(join(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t20132,t42]) ).
cnf(t25840,plain,
join(X1,join(join(X1,X2),meet(X2,join(X1,X3)))) = join(join(X1,X2),meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t274235]) ).
cnf(t25851,plain,
join(join(X1,X2),meet(X2,join(X1,X3))) = join(X1,join(join(X2,X1),meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t25840,t42]) ).
cnf(t14293,plain,
meet(X1,join(X1,X2)) = meet(meet(X1,join(X1,X2)),join(join(X1,X3),meet(X1,join(X4,Y4)))),
inference(cp,[status(thm)],[t5048,t14219]) ).
cnf(t274067,plain,
X1 = meet(meet(X1,join(X1,X2)),join(join(X1,X3),meet(X1,join(X4,Y4)))),
inference(step,[status(thm)],[t14293,t10]) ).
cnf(t274068,plain,
X1 = meet(X1,join(join(X1,X3),meet(X1,join(X4,Y4)))),
inference(step,[status(thm)],[t274067,t10]) ).
cnf(t14352,plain,
meet(X1,join(join(X1,X2),meet(X1,join(X3,X4)))) = X1,
inference(orient,[status(thm)],[t274068]) ).
cnf(t20129,plain,
join(join(X1,X2),meet(X1,join(X3,X4))) = join(join(join(X1,X2),meet(X1,join(X3,X4))),X1),
inference(cp,[status(thm)],[t20086,t14352]) ).
cnf(t274228,plain,
join(join(X1,X2),meet(X1,join(X3,X4))) = join(X1,join(join(X1,X2),meet(X1,join(X3,X4)))),
inference(step,[status(thm)],[t20129,t42]) ).
cnf(t274229,plain,
join(join(X1,X2),meet(X1,join(X3,X4))) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t274228,t93]) ).
cnf(t274230,plain,
join(join(X1,X2),meet(X1,join(X3,X4))) = join(X1,X2),
inference(step,[status(thm)],[t274229,t74]) ).
cnf(t25547,plain,
join(join(X1,X2),meet(X1,join(X3,X4))) = join(X1,X2),
inference(orient,[status(thm)],[t274230]) ).
cnf(t274236,plain,
join(join(X1,X2),meet(X2,join(X1,X3))) = join(X1,join(X2,X1)),
inference(step,[status(thm)],[t25851,t25547]) ).
cnf(t274237,plain,
join(join(X1,X2),meet(X2,join(X1,X3))) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t274236,t42]) ).
cnf(t274238,plain,
join(join(X1,X2),meet(X2,join(X1,X3))) = join(X1,X2),
inference(step,[status(thm)],[t274237,t74]) ).
cnf(t25991,plain,
join(join(X1,X2),meet(X2,join(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t274238]) ).
cnf(t25995,plain,
join(X1,join(X2,meet(X1,X3))) = join(join(X1,X2),meet(join(X2,meet(X1,X3)),join(X1,X4))),
inference(cp,[status(thm)],[t25991,t93]) ).
cnf(t274240,plain,
join(X1,X2) = join(join(X1,X2),meet(join(X2,meet(X1,X3)),join(X1,X4))),
inference(step,[status(thm)],[t25995,t93]) ).
cnf(t274241,plain,
join(X1,X2) = join(join(X1,X2),meet(join(X1,X4),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t274240,t13]) ).
cnf(t26175,plain,
join(join(X1,X2),meet(join(X1,X3),join(X2,meet(X1,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t274241]) ).
cnf(t26272,plain,
meet(join(X1,X2),X3) = meet(meet(join(X1,X2),X3),join(X1,X3)),
inference(cp,[status(thm)],[t22720,t26175]) ).
cnf(t274242,plain,
meet(X3,join(X1,X2)) = meet(meet(join(X1,X2),X3),join(X1,X3)),
inference(step,[status(thm)],[t26272,t13]) ).
cnf(t274243,plain,
meet(X3,join(X1,X2)) = meet(join(X1,X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t274242,t13]) ).
cnf(t274244,plain,
meet(X3,join(X1,X2)) = meet(X3,meet(join(X1,X3),join(X1,X2))),
inference(step,[status(thm)],[t274243,t15]) ).
cnf(t274245,plain,
meet(X3,join(X1,X2)) = meet(X3,meet(join(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t274244,t13]) ).
cnf(t26364,plain,
meet(X1,meet(join(X2,X3),join(X2,X1))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t274245]) ).
cnf(t45927,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,join(X3,X4))),
inference(cp,[status(thm)],[t45872,t26364]) ).
cnf(t46085,plain,
join(join(X1,X2),meet(X2,join(X3,X4))) = join(X1,X2),
inference(orient,[status(thm)],[t45927]) ).
cnf(t274490,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X1,X2)))) = meet(join(X1,X2),join(X3,meet(X2,join(X1,meet(join(X2,X4),join(X2,meet(X3,join(X2,X4)))))))),
inference(step,[status(thm)],[t51158,t46085]) ).
cnf(t274491,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X1,X2)))) = meet(join(X1,X2),join(X3,X2)),
inference(step,[status(thm)],[t274490,t15857]) ).
cnf(t274492,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X1,X2)))) = meet(join(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t274491,t42]) ).
cnf(t51470,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X1,X2)))) = meet(join(X1,X2),join(X2,X3)),
inference(orient,[status(thm)],[t274492]) ).
cnf(t42572,plain,
join(X1,X2) = join(X1,meet(join(X3,join(X4,X2)),join(X2,meet(X1,Y4)))),
inference(cp,[status(thm)],[t42538,t46]) ).
cnf(t274505,plain,
join(X1,X2) = join(X1,meet(join(X2,meet(X1,Y4)),join(X3,join(X4,X2)))),
inference(step,[status(thm)],[t42572,t13]) ).
cnf(t274506,plain,
join(X1,X2) = join(X1,meet(join(X2,meet(X1,Y4)),join(X2,join(X3,X4)))),
inference(step,[status(thm)],[t274505,t46]) ).
cnf(t53753,plain,
join(X1,meet(join(X2,meet(X1,X3)),join(X2,join(X4,Y4)))) = join(X1,X2),
inference(orient,[status(thm)],[t274506]) ).
cnf(t53876,plain,
meet(join(X1,join(X1,meet(X2,X3))),join(join(X1,meet(X2,X3)),X2)) = meet(join(X1,join(X1,meet(X2,X3))),join(X2,X1)),
inference(cp,[status(thm)],[t51470,t53753]) ).
cnf(t274507,plain,
meet(join(X1,meet(X2,X3)),join(join(X1,meet(X2,X3)),X2)) = meet(join(X1,join(X1,meet(X2,X3))),join(X2,X1)),
inference(step,[status(thm)],[t53876,t74]) ).
cnf(t274508,plain,
join(X1,meet(X2,X3)) = meet(join(X1,join(X1,meet(X2,X3))),join(X2,X1)),
inference(step,[status(thm)],[t274507,t10]) ).
cnf(t274509,plain,
join(X1,meet(X2,X3)) = meet(join(X2,X1),join(X1,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t274508,t13]) ).
cnf(t274510,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t274509,t42]) ).
cnf(t274511,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t274510,t74]) ).
cnf(t54023,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274511]) ).
cnf(t54334,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,meet(meet(X3,X4),join(X2,X3)))))) = meet(X1,join(X2,meet(meet(X3,X4),join(X1,join(X2,meet(X3,X4)))))),
inference(cp,[status(thm)],[t1509,t54023]) ).
cnf(t274520,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,X3)))) = meet(X1,join(X2,meet(meet(X3,X4),join(X1,join(X2,meet(X3,X4)))))),
inference(step,[status(thm)],[t54334,t33]) ).
cnf(t274521,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,X3)))) = meet(X1,join(X2,meet(meet(X3,X4),join(X1,meet(X3,X4))))),
inference(step,[status(thm)],[t274520,t185]) ).
cnf(t274522,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,X3)))) = meet(X1,join(X2,meet(X3,X4))),
inference(step,[status(thm)],[t274521,t5379]) ).
cnf(t54958,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,X3)))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t274522]) ).
cnf(t54986,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(join(X1,X3),meet(X3,X4)))),
inference(cp,[status(thm)],[t54958,t13]) ).
cnf(t274523,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X4,meet(join(X1,X3),X3)))),
inference(step,[status(thm)],[t54986,t15]) ).
cnf(t274524,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X3,meet(X4,join(X1,X3))))),
inference(step,[status(thm)],[t274523,t15]) ).
cnf(t55204,plain,
meet(X1,join(X2,meet(X3,meet(X4,join(X1,X3))))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t274524]) ).
cnf(t55211,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,meet(X3,join(join(X1,X2),X2)))),
inference(cp,[status(thm)],[t55204,t54023]) ).
cnf(t274525,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(join(X1,X2),X2)))),
inference(step,[status(thm)],[t55211,t54023]) ).
cnf(t274526,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(X2,join(X1,X2))))),
inference(step,[status(thm)],[t274525,t42]) ).
cnf(t274527,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(X1,join(X2,X2))))),
inference(step,[status(thm)],[t274526,t46]) ).
cnf(t9588,plain,
meet(meet(X1,meet(X2,join(X3,meet(X4,X1)))),meet(Y4,X4)) = meet(Y4,meet(X4,meet(X1,X2))),
inference(cp,[status(thm)],[t15,t9401]) ).
cnf(t274004,plain,
meet(X4,meet(meet(X1,meet(X2,join(X3,meet(X4,X1)))),Y4)) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t9588,t15]) ).
cnf(t274005,plain,
meet(X4,meet(Y4,meet(X1,meet(X2,join(X3,meet(X4,X1)))))) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t274004,t13]) ).
cnf(t274006,plain,
meet(X4,meet(X1,meet(meet(X2,join(X3,meet(X4,X1))),Y4))) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t274005,t15]) ).
cnf(t274007,plain,
meet(X1,meet(meet(meet(X2,join(X3,meet(X4,X1))),Y4),X4)) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t274006,t15]) ).
cnf(t274008,plain,
meet(X1,meet(X4,meet(meet(X2,join(X3,meet(X4,X1))),Y4))) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t274007,t13]) ).
cnf(t274009,plain,
meet(X1,meet(X4,meet(Y4,meet(X2,join(X3,meet(X4,X1)))))) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t274008,t13]) ).
cnf(t274010,plain,
meet(X1,meet(X4,meet(X2,meet(join(X3,meet(X4,X1)),Y4)))) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t274009,t15]) ).
cnf(t274011,plain,
meet(X1,meet(X2,meet(meet(join(X3,meet(X4,X1)),Y4),X4))) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t274010,t15]) ).
cnf(t274012,plain,
meet(X1,meet(X2,meet(X4,meet(join(X3,meet(X4,X1)),Y4)))) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t274011,t13]) ).
cnf(t274013,plain,
meet(X1,meet(X2,meet(X4,meet(Y4,join(X3,meet(X4,X1)))))) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t274012,t13]) ).
cnf(t274014,plain,
meet(X1,meet(X2,meet(X4,meet(Y4,join(X3,meet(X1,X4)))))) = meet(Y4,meet(X4,meet(X1,X2))),
inference(step,[status(thm)],[t274013,t13]) ).
cnf(t274015,plain,
meet(X1,meet(X2,meet(X4,meet(Y4,join(X3,meet(X1,X4)))))) = meet(X4,meet(meet(X1,X2),Y4)),
inference(step,[status(thm)],[t274014,t15]) ).
cnf(t274016,plain,
meet(X1,meet(X2,meet(X4,meet(Y4,join(X3,meet(X1,X4)))))) = meet(X4,meet(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t274015,t13]) ).
cnf(t274017,plain,
meet(X1,meet(X2,meet(X4,meet(Y4,join(X3,meet(X1,X4)))))) = meet(X4,meet(X2,meet(Y4,X1))),
inference(step,[status(thm)],[t274016,t15]) ).
cnf(t274018,plain,
meet(X1,meet(X2,meet(X4,meet(Y4,join(X3,meet(X1,X4)))))) = meet(X4,meet(X1,meet(X2,Y4))),
inference(step,[status(thm)],[t274017,t15]) ).
cnf(t274019,plain,
meet(X1,meet(X2,meet(X4,meet(Y4,join(X3,meet(X1,X4)))))) = meet(X1,meet(meet(X2,Y4),X4)),
inference(step,[status(thm)],[t274018,t15]) ).
cnf(t274020,plain,
meet(X1,meet(X2,meet(X4,meet(Y4,join(X3,meet(X1,X4)))))) = meet(X1,meet(X4,meet(X2,Y4))),
inference(step,[status(thm)],[t274019,t13]) ).
cnf(t274021,plain,
meet(X1,meet(X2,meet(X4,meet(Y4,join(X3,meet(X1,X4)))))) = meet(X1,meet(X2,meet(Y4,X4))),
inference(step,[status(thm)],[t274020,t15]) ).
cnf(t274022,plain,
meet(X1,meet(X2,meet(X4,meet(Y4,join(X3,meet(X1,X4)))))) = meet(X1,meet(X2,meet(X4,Y4))),
inference(step,[status(thm)],[t274021,t13]) ).
cnf(t11274,plain,
meet(X1,meet(X2,meet(X3,meet(X4,join(Y4,meet(X1,X3)))))) = meet(X1,meet(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t274022]) ).
cnf(t11286,plain,
meet(X1,meet(X2,meet(X3,X3))) = meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X3))))),
inference(cp,[status(thm)],[t11274,t66]) ).
cnf(t274023,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X3))))),
inference(step,[status(thm)],[t11286,t9]) ).
cnf(t11465,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X3))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274023]) ).
cnf(t14307,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(X4,meet(X1,join(X2,X3))))),
inference(cp,[status(thm)],[t11465,t14219]) ).
cnf(t274069,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X4,meet(X1,join(X2,X3))))),
inference(step,[status(thm)],[t14307,t10]) ).
cnf(t14658,plain,
meet(X1,meet(X2,join(X3,meet(X1,join(X2,X4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t274069]) ).
cnf(t42658,plain,
join(join(X1,X2),X3) = join(join(X1,X2),meet(join(X3,X4),join(X3,X1))),
inference(cp,[status(thm)],[t42538,t42538]) ).
cnf(t274421,plain,
join(X3,join(X1,X2)) = join(join(X1,X2),meet(join(X3,X4),join(X3,X1))),
inference(step,[status(thm)],[t42658,t42]) ).
cnf(t274422,plain,
join(X2,join(X3,X1)) = join(join(X1,X2),meet(join(X3,X4),join(X3,X1))),
inference(step,[status(thm)],[t274421,t46]) ).
cnf(t274423,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X3,X4),join(X3,X1))),
inference(step,[status(thm)],[t274422,t46]) ).
cnf(t274424,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X3,X1),join(X3,X4))),
inference(step,[status(thm)],[t274423,t13]) ).
cnf(t274425,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X1,X3),join(X3,X4))),
inference(step,[status(thm)],[t274424,t42]) ).
cnf(t43136,plain,
join(join(X1,X2),meet(join(X1,X3),join(X3,X4))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t274425]) ).
cnf(t43455,plain,
meet(join(X1,X2),X2) = meet(join(X1,X2),meet(X2,join(X1,join(X3,X2)))),
inference(cp,[status(thm)],[t14658,t43136]) ).
cnf(t274427,plain,
meet(X2,join(X1,X2)) = meet(join(X1,X2),meet(X2,join(X1,join(X3,X2)))),
inference(step,[status(thm)],[t43455,t13]) ).
cnf(t274428,plain,
meet(X2,join(X1,X2)) = meet(X2,meet(join(X1,join(X3,X2)),join(X1,X2))),
inference(step,[status(thm)],[t274427,t15]) ).
cnf(t274429,plain,
meet(X2,join(X1,X2)) = meet(X2,join(X1,join(X3,X2))),
inference(step,[status(thm)],[t274428,t26364]) ).
cnf(t274430,plain,
meet(X2,join(X1,X2)) = meet(X2,join(X1,join(X2,X3))),
inference(step,[status(thm)],[t274429,t42]) ).
cnf(t43712,plain,
meet(X1,join(X2,join(X1,X3))) = meet(X1,join(X2,X1)),
inference(orient,[status(thm)],[t274430]) ).
cnf(t43826,plain,
meet(join(X1,join(X2,X3)),meet(X4,X2)) = meet(X4,meet(X2,join(X1,X2))),
inference(cp,[status(thm)],[t15,t43712]) ).
cnf(t274431,plain,
meet(X2,meet(join(X1,join(X2,X3)),X4)) = meet(X4,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t43826,t15]) ).
cnf(t274432,plain,
meet(X2,meet(X4,join(X1,join(X2,X3)))) = meet(X4,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t274431,t13]) ).
cnf(t274433,plain,
meet(X2,meet(X4,join(X1,join(X2,X3)))) = meet(X2,meet(join(X1,X2),X4)),
inference(step,[status(thm)],[t274432,t15]) ).
cnf(t274434,plain,
meet(X2,meet(X4,join(X1,join(X2,X3)))) = meet(X2,meet(X4,join(X1,X2))),
inference(step,[status(thm)],[t274433,t13]) ).
cnf(t43827,plain,
meet(X1,meet(X2,join(X3,join(X1,X4)))) = meet(X1,meet(X2,join(X3,X1))),
inference(orient,[status(thm)],[t274434]) ).
cnf(t274528,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t274527,t43827]) ).
cnf(t55472,plain,
join(X1,meet(X2,meet(X3,join(X1,X2)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274528]) ).
cnf(t55530,plain,
join(X1,meet(meet(X2,X3),join(X1,X2))) = join(X1,meet(meet(X2,X3),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t55472,t54023]) ).
cnf(t274529,plain,
join(X1,meet(meet(X2,X3),join(X1,X2))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t55530,t31272]) ).
cnf(t55698,plain,
join(X1,meet(meet(X2,X3),join(X1,X2))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274529]) ).
cnf(t55708,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(meet(X3,meet(X4,X2)),join(X1,X2))),
inference(cp,[status(thm)],[t55698,t15]) ).
cnf(t274533,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(join(X1,X2),meet(X3,meet(X4,X2)))),
inference(step,[status(thm)],[t55708,t13]) ).
cnf(t274534,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(meet(X4,X2),meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t274533,t15]) ).
cnf(t274535,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(X3,meet(meet(X4,X2),join(X1,X2)))),
inference(step,[status(thm)],[t274534,t15]) ).
cnf(t274536,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(X3,meet(meet(X2,X4),join(X1,X2)))),
inference(step,[status(thm)],[t274535,t13]) ).
cnf(t56137,plain,
join(X1,meet(X2,meet(meet(X3,X4),join(X1,X3)))) = join(X1,meet(X3,meet(X2,X4))),
inference(orient,[status(thm)],[t274536]) ).
cnf(t56427,plain,
join(X1,meet(X2,meet(meet(X3,X4),join(X1,X3)))) = join(X1,meet(X2,join(X1,meet(X3,meet(X2,X4))))),
inference(cp,[status(thm)],[t31167,t56137]) ).
cnf(t274553,plain,
join(X1,meet(X3,meet(X2,X4))) = join(X1,meet(X2,join(X1,meet(X3,meet(X2,X4))))),
inference(step,[status(thm)],[t56427,t56137]) ).
cnf(t59326,plain,
join(X1,meet(X2,join(X1,meet(X3,meet(X2,X4))))) = join(X1,meet(X3,meet(X2,X4))),
inference(orient,[status(thm)],[t274553]) ).
cnf(t59333,plain,
join(X1,meet(X2,meet(X3,join(X3,X2)))) = join(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t59326,t55204]) ).
cnf(t274554,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t59333,t10]) ).
cnf(t59583,plain,
join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t274554]) ).
cnf(t59763,plain,
join(X1,meet(meet(X2,X3),join(X3,X4))) = join(X1,meet(join(X3,X4),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t59583,t20437]) ).
cnf(t274555,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X3,X4),join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t59763,t20437]) ).
cnf(t59930,plain,
join(X1,meet(join(X2,X3),join(X1,meet(X4,X2)))) = join(X1,meet(X4,X2)),
inference(orient,[status(thm)],[t274555]) ).
cnf(t30787,plain,
meet(X1,join(meet(X2,X3),meet(X1,X2))) = meet(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t204,t30646]) ).
cnf(t274301,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t30787,t42]) ).
cnf(t274302,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
inference(step,[status(thm)],[t274301,t83]) ).
cnf(t30863,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t274302]) ).
cnf(t59944,plain,
join(meet(join(X1,X2),X3),meet(X3,X1)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(cp,[status(thm)],[t59930,t30863]) ).
cnf(t274556,plain,
join(meet(X3,X1),meet(join(X1,X2),X3)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t59944,t42]) ).
cnf(t274557,plain,
join(meet(X1,X3),meet(join(X1,X2),X3)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t274556,t13]) ).
cnf(t274558,plain,
join(meet(X1,X3),meet(X3,join(X1,X2))) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t274557,t13]) ).
cnf(t274559,plain,
join(meet(X1,X3),meet(X3,join(X1,X2))) = meet(join(X1,X2),X3),
inference(step,[status(thm)],[t274558,t11]) ).
cnf(t274560,plain,
join(meet(X1,X3),meet(X3,join(X1,X2))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t274559,t13]) ).
cnf(t60300,plain,
join(meet(X1,X2),meet(X2,join(X1,X3))) = meet(X2,join(X1,X3)),
inference(orient,[status(thm)],[t274560]) ).
cnf(t60404,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(join(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t60300,t10]) ).
cnf(t60757,plain,
join(X1,meet(join(X1,X2),join(X1,X3))) = meet(join(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t60404]) ).
cnf(t61013,plain,
join(X1,join(meet(join(X1,X2),join(X1,X3)),X4)) = join(X4,meet(join(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t46,t60757]) ).
cnf(t274702,plain,
join(X1,join(X4,meet(join(X1,X2),join(X1,X3)))) = join(X4,meet(join(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t61013,t42]) ).
cnf(t85014,plain,
join(X1,join(X2,meet(join(X1,X3),join(X1,X4)))) = join(X2,meet(join(X1,X3),join(X1,X4))),
inference(orient,[status(thm)],[t274702]) ).
cnf(t85296,plain,
join(X1,join(X1,X2)) = join(X1,join(X2,meet(join(X1,X3),join(X1,X2)))),
inference(cp,[status(thm)],[t33195,t85014]) ).
cnf(t274704,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X3),join(X1,X2)))),
inference(step,[status(thm)],[t85296,t74]) ).
cnf(t274705,plain,
join(X1,X2) = join(X2,meet(join(X1,X3),join(X1,X2))),
inference(step,[status(thm)],[t274704,t85014]) ).
cnf(t274706,plain,
join(X1,X2) = join(X2,meet(join(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t274705,t13]) ).
cnf(t85344,plain,
join(X1,meet(join(X2,X1),join(X2,X3))) = join(X2,X1),
inference(orient,[status(thm)],[t274706]) ).
cnf(t85837,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,join(X2,X3))))),
inference(cp,[status(thm)],[t646,t85344]) ).
cnf(t274808,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))) = meet(X1,join(join(X2,X3),meet(X1,X4))),
inference(step,[status(thm)],[t85837,t204]) ).
cnf(t274809,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))) = meet(X1,join(meet(X1,X4),join(X2,X3))),
inference(step,[status(thm)],[t274808,t42]) ).
cnf(t274810,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))) = meet(X1,join(X3,join(meet(X1,X4),X2))),
inference(step,[status(thm)],[t274809,t46]) ).
cnf(t274811,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(step,[status(thm)],[t274810,t46]) ).
cnf(t115502,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t274811]) ).
cnf(t115528,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(meet(X4,join(X1,X3)),join(X2,X3))),
inference(cp,[status(thm)],[t115502,t42]) ).
cnf(t274895,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X3,join(meet(X4,join(X1,X3)),X2))),
inference(step,[status(thm)],[t115528,t46]) ).
cnf(t274896,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X2,join(X3,meet(X4,join(X1,X3))))),
inference(step,[status(thm)],[t274895,t46]) ).
cnf(t133542,plain,
meet(X1,join(X2,join(X3,meet(X4,join(X1,X3))))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t274896]) ).
cnf(t85546,plain,
meet(join(X1,meet(join(X2,X1),join(X2,X3))),join(X1,X4)) = join(X1,meet(join(X2,X1),join(X1,X4))),
inference(cp,[status(thm)],[t60757,t85344]) ).
cnf(t274713,plain,
meet(join(X2,X1),join(X1,X4)) = join(X1,meet(join(X2,X1),join(X1,X4))),
inference(step,[status(thm)],[t85546,t85344]) ).
cnf(t87528,plain,
join(X1,meet(join(X2,X1),join(X1,X3))) = meet(join(X2,X1),join(X1,X3)),
inference(orient,[status(thm)],[t274713]) ).
cnf(t87529,plain,
meet(join(X1,X2),join(X2,meet(X3,X1))) = join(X2,meet(X3,X1)),
inference(cp,[status(thm)],[t87528,t59930]) ).
cnf(t274729,plain,
meet(join(X1,X2),join(X2,meet(X1,X3))) = join(X2,meet(X3,X1)),
inference(step,[status(thm)],[t87529,t13]) ).
cnf(t274730,plain,
meet(join(X1,X2),join(X2,meet(X1,X3))) = join(X2,meet(X1,X3)),
inference(step,[status(thm)],[t274729,t13]) ).
cnf(t88667,plain,
meet(join(X1,X2),join(X2,meet(X1,X3))) = join(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t274730]) ).
cnf(t88751,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t88667,t12]) ).
cnf(t89124,plain,
meet(X1,join(meet(X1,X2),meet(X1,X3))) = join(meet(X1,X2),meet(X1,X3)),
inference(orient,[status(thm)],[t88751]) ).
cnf(t31024,plain,
meet(X1,join(meet(join(X1,X2),X3),meet(X3,X4))) = meet(X1,meet(join(X1,X2),X3)),
inference(cp,[status(thm)],[t14219,t30863]) ).
cnf(t274334,plain,
meet(X1,join(meet(X3,X4),meet(join(X1,X2),X3))) = meet(X1,meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t31024,t42]) ).
cnf(t274335,plain,
meet(X1,join(meet(X3,X4),meet(X3,join(X1,X2)))) = meet(X1,meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t274334,t13]) ).
cnf(t274336,plain,
meet(X1,join(meet(X3,X4),meet(X3,join(X1,X2)))) = meet(X1,meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t274335,t13]) ).
cnf(t274337,plain,
meet(X1,join(meet(X3,X4),meet(X3,join(X1,X2)))) = meet(X1,X3),
inference(step,[status(thm)],[t274336,t83]) ).
cnf(t34167,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t274337]) ).
cnf(t34274,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),join(meet(X3,X4),meet(X3,X1))),
inference(cp,[status(thm)],[t34167,t34167]) ).
cnf(t274338,plain,
meet(X3,meet(X1,X2)) = meet(meet(X1,X2),join(meet(X3,X4),meet(X3,X1))),
inference(step,[status(thm)],[t34274,t13]) ).
cnf(t274339,plain,
meet(X2,meet(X3,X1)) = meet(meet(X1,X2),join(meet(X3,X4),meet(X3,X1))),
inference(step,[status(thm)],[t274338,t15]) ).
cnf(t274340,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X3,X4),meet(X3,X1))),
inference(step,[status(thm)],[t274339,t15]) ).
cnf(t274341,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X3,X1),meet(X3,X4))),
inference(step,[status(thm)],[t274340,t42]) ).
cnf(t274342,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X1,X3),meet(X3,X4))),
inference(step,[status(thm)],[t274341,t13]) ).
cnf(t34405,plain,
meet(meet(X1,X2),join(meet(X1,X3),meet(X3,X4))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274342]) ).
cnf(t42642,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),join(meet(X1,join(X3,X4)),X3)),
inference(cp,[status(thm)],[t34405,t42538]) ).
cnf(t274438,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),join(X3,meet(X1,join(X3,X4)))),
inference(step,[status(thm)],[t42642,t42]) ).
cnf(t44154,plain,
meet(meet(X1,X2),join(X3,meet(X1,join(X3,X4)))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t274438]) ).
cnf(t44280,plain,
meet(meet(X1,X2),meet(join(X2,X3),join(X4,Y4))) = meet(meet(X1,X2),join(X4,meet(meet(X1,X2),join(X4,Y4)))),
inference(cp,[status(thm)],[t44154,t20437]) ).
cnf(t32868,plain,
meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))) = meet(join(X1,meet(join(X1,X2),X3)),join(X1,join(meet(join(X1,X2),X3),X2))),
inference(cp,[status(thm)],[t19841,t32733]) ).
cnf(t274364,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))) = meet(join(X1,meet(join(X1,X2),X3)),join(X1,join(meet(join(X1,X2),X3),X2))),
inference(step,[status(thm)],[t32868,t13]) ).
cnf(t274365,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))) = join(X1,meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t274364,t7903]) ).
cnf(t274366,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))) = join(X1,meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t274365,t13]) ).
cnf(t36652,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))) = join(X1,meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t274366]) ).
cnf(t36837,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t9589,t36652]) ).
cnf(t36931,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t36837]) ).
cnf(t274482,plain,
meet(meet(X1,X2),meet(join(X2,X3),join(X4,Y4))) = meet(meet(X1,X2),join(X4,Y4)),
inference(step,[status(thm)],[t44280,t36931]) ).
cnf(t50294,plain,
meet(meet(X1,X2),meet(join(X2,X3),join(X4,Y4))) = meet(meet(X1,X2),join(X4,Y4)),
inference(orient,[status(thm)],[t274482]) ).
cnf(t51616,plain,
meet(meet(X1,X2),join(X3,meet(X4,join(X2,X4)))) = meet(meet(X1,X2),meet(join(X2,X4),join(X4,X3))),
inference(cp,[status(thm)],[t50294,t51470]) ).
cnf(t274495,plain,
meet(meet(X1,X2),join(X3,meet(X4,join(X2,X4)))) = meet(meet(X1,X2),join(X4,X3)),
inference(step,[status(thm)],[t51616,t50294]) ).
cnf(t274496,plain,
meet(meet(X1,X2),join(X3,meet(X4,join(X2,X4)))) = meet(meet(X1,X2),join(X3,X4)),
inference(step,[status(thm)],[t274495,t42]) ).
cnf(t51997,plain,
meet(meet(X1,X2),join(X3,meet(X4,join(X2,X4)))) = meet(meet(X1,X2),join(X3,X4)),
inference(orient,[status(thm)],[t274496]) ).
cnf(t60594,plain,
meet(meet(X1,X2),join(meet(X2,X3),X3)) = meet(meet(X1,X2),meet(X3,join(X2,X3))),
inference(cp,[status(thm)],[t51997,t60300]) ).
cnf(t274563,plain,
meet(meet(X1,X2),join(X3,meet(X2,X3))) = meet(meet(X1,X2),meet(X3,join(X2,X3))),
inference(step,[status(thm)],[t60594,t42]) ).
cnf(t274564,plain,
meet(meet(X1,X2),join(X3,meet(X2,X3))) = meet(X3,meet(join(X2,X3),meet(X1,X2))),
inference(step,[status(thm)],[t274563,t15]) ).
cnf(t274565,plain,
meet(meet(X1,X2),join(X3,meet(X2,X3))) = meet(X3,meet(X2,meet(join(X2,X3),X1))),
inference(step,[status(thm)],[t274564,t15]) ).
cnf(t274566,plain,
meet(meet(X1,X2),join(X3,meet(X2,X3))) = meet(X3,meet(X1,meet(X2,join(X2,X3)))),
inference(step,[status(thm)],[t274565,t15]) ).
cnf(t274567,plain,
meet(meet(X1,X2),join(X3,meet(X2,X3))) = meet(X1,meet(meet(X2,join(X2,X3)),X3)),
inference(step,[status(thm)],[t274566,t15]) ).
cnf(t274568,plain,
meet(meet(X1,X2),join(X3,meet(X2,X3))) = meet(X1,meet(X3,meet(X2,join(X2,X3)))),
inference(step,[status(thm)],[t274567,t13]) ).
cnf(t274569,plain,
meet(meet(X1,X2),join(X3,meet(X2,X3))) = meet(X1,meet(X2,meet(join(X2,X3),X3))),
inference(step,[status(thm)],[t274568,t15]) ).
cnf(t274570,plain,
meet(meet(X1,X2),join(X3,meet(X2,X3))) = meet(X1,meet(X2,meet(X3,join(X2,X3)))),
inference(step,[status(thm)],[t274569,t13]) ).
cnf(t274571,plain,
meet(meet(X1,X2),join(X3,meet(X2,X3))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t274570,t83]) ).
cnf(t61015,plain,
meet(meet(X1,X2),join(X3,meet(X2,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t274571]) ).
cnf(t89255,plain,
meet(X1,meet(join(meet(X1,X2),meet(X1,X3)),X4)) = meet(join(meet(X1,X2),meet(X1,X3)),join(X4,meet(join(meet(X1,X2),meet(X1,X3)),X4))),
inference(cp,[status(thm)],[t61015,t89124]) ).
cnf(t274825,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X1,X3)))) = meet(join(meet(X1,X2),meet(X1,X3)),join(X4,meet(join(meet(X1,X2),meet(X1,X3)),X4))),
inference(step,[status(thm)],[t89255,t13]) ).
cnf(t274826,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X1,X3)))) = meet(join(meet(X1,X2),meet(X1,X3)),X4),
inference(step,[status(thm)],[t274825,t227]) ).
cnf(t274827,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X1,X3)))) = meet(X4,join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t274826,t13]) ).
cnf(t118690,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X1,X4)))) = meet(X2,join(meet(X1,X3),meet(X1,X4))),
inference(orient,[status(thm)],[t274827]) ).
cnf(t119090,plain,
meet(X1,meet(X1,X2)) = meet(X1,meet(X2,join(meet(X1,X3),meet(X1,X2)))),
inference(cp,[status(thm)],[t11465,t118690]) ).
cnf(t274829,plain,
meet(X1,X2) = meet(X1,meet(X2,join(meet(X1,X3),meet(X1,X2)))),
inference(step,[status(thm)],[t119090,t66]) ).
cnf(t274830,plain,
meet(X1,X2) = meet(X2,join(meet(X1,X3),meet(X1,X2))),
inference(step,[status(thm)],[t274829,t118690]) ).
cnf(t274831,plain,
meet(X1,X2) = meet(X2,join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t274830,t42]) ).
cnf(t119127,plain,
meet(X1,join(meet(X2,X1),meet(X2,X3))) = meet(X2,X1),
inference(orient,[status(thm)],[t274831]) ).
cnf(t119454,plain,
join(meet(X1,join(meet(X2,X1),meet(X2,X3))),meet(X1,X4)) = meet(X1,join(meet(X2,X1),meet(X1,X4))),
inference(cp,[status(thm)],[t89124,t119127]) ).
cnf(t274832,plain,
join(meet(X2,X1),meet(X1,X4)) = meet(X1,join(meet(X2,X1),meet(X1,X4))),
inference(step,[status(thm)],[t119454,t119127]) ).
cnf(t119802,plain,
meet(X1,join(meet(X2,X1),meet(X1,X3))) = join(meet(X2,X1),meet(X1,X3)),
inference(orient,[status(thm)],[t274832]) ).
cnf(t85669,plain,
meet(X1,join(X2,meet(join(X3,X2),join(X3,X4)))) = meet(X1,join(X2,meet(X1,join(X3,X2)))),
inference(cp,[status(thm)],[t36931,t85344]) ).
cnf(t274712,plain,
meet(X1,join(X3,X2)) = meet(X1,join(X2,meet(X1,join(X3,X2)))),
inference(step,[status(thm)],[t85669,t85344]) ).
cnf(t87126,plain,
meet(X1,join(X2,meet(X1,join(X3,X2)))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t274712]) ).
cnf(t119807,plain,
join(meet(X1,X2),meet(X2,join(X3,meet(X1,X2)))) = meet(X2,join(X3,meet(X1,X2))),
inference(cp,[status(thm)],[t119802,t87126]) ).
cnf(t124888,plain,
join(meet(X1,X2),meet(X2,join(X3,meet(X1,X2)))) = meet(X2,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t119807]) ).
cnf(t133560,plain,
meet(X1,join(X2,join(meet(X3,X4),meet(X1,X4)))) = meet(X1,join(X2,meet(X4,join(X1,meet(X3,X4))))),
inference(cp,[status(thm)],[t133542,t124888]) ).
cnf(t275374,plain,
meet(X1,join(X2,join(meet(X1,X4),meet(X3,X4)))) = meet(X1,join(X2,meet(X4,join(X1,meet(X3,X4))))),
inference(step,[status(thm)],[t133560,t42]) ).
cnf(t272771,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X4,X3)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X4,X3))))),
inference(orient,[status(thm)],[t275374]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(b,join(meet(a,c),meet(c,join(b,d))))) != meet(a,join(b,meet(c,join(a,d)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(b,join(meet(a,c),meet(join(b,d),c)))) != meet(a,join(b,meet(c,join(a,d)))),
inference(rw,[status(thm)],[goal_0,t13]) ).
cnf(g0_1,plain,
meet(a,join(b,join(meet(a,c),meet(join(d,b),c)))) != meet(a,join(b,meet(c,join(a,d)))),
inference(rw,[status(thm)],[g0_0,t42]) ).
cnf(g0_2,plain,
meet(a,join(b,meet(c,join(a,meet(join(d,b),c))))) != meet(a,join(b,meet(c,join(a,d)))),
inference(rw,[status(thm)],[g0_1,t272771]) ).
cnf(g0_3,plain,
meet(a,join(b,meet(c,join(a,meet(c,join(d,b)))))) != meet(a,join(b,meet(c,join(a,d)))),
inference(rw,[status(thm)],[g0_2,t13]) ).
cnf(g0_4,plain,
meet(a,join(b,meet(c,join(a,meet(c,join(b,d)))))) != meet(a,join(b,meet(c,join(a,d)))),
inference(rw,[status(thm)],[g0_3,t42]) ).
cnf(g0_5,plain,
meet(a,join(b,meet(c,join(a,d)))) != meet(a,join(b,meet(c,join(a,d)))),
inference(rw,[status(thm)],[g0_4,t33]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT158-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/5.38 % Computer : n006.cluster.edu
% 0.12/5.38 % Model : x86_64 x86_64
% 0.12/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.38 % Memory : 8046.5625MB
% 0.12/5.38 % OS : Linux 6.8.0-71-generic
% 0.12/5.38 % CPULimit : 300
% 0.12/5.38 % WCLimit : 300
% 0.12/5.39 % DateTime : Wed Sep 23 20:24:20 UTC 2026
% 0.12/5.39 % CPUTime :
% 0.12/5.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 196.84/33.86 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 196.84/33.86 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------