%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT165-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n004.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:47 PM UTC 2026
% Result : Unsatisfiable 82.27s 11.15s
% Output : CNFRefutation 82.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 176
% Number of leaves : 10
% Syntax : Number of clauses : 505 ( 505 unt; 0 nHn; 8 RR)
% Number of literals : 505 ( 504 equ; 7 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 1868 ( 423 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t132767,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)],[t132767]) ).
cnf(t8,axiom,
meet(X1,join(X2,meet(X3,join(X4,meet(X1,X2))))) = meet(X1,join(X2,meet(X3,join(X2,X4)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
meet(X1,join(X2,meet(X3,join(X4,meet(X1,X2))))) = meet(X1,join(X2,meet(X3,join(X2,X4)))),
inference(orient,[status(thm)],[t8]) ).
cnf(t5,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t10,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t39,plain,
meet(X1,join(join(X1,X2),meet(X3,join(join(X1,X2),X4)))) = meet(X1,join(join(X1,X2),meet(X3,join(X4,X1)))),
inference(cp,[status(thm)],[t33,t10]) ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t47,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t132952,plain,
meet(X1,join(join(X1,X2),meet(X3,join(X4,join(X1,X2))))) = meet(X1,join(join(X1,X2),meet(X3,join(X4,X1)))),
inference(step,[status(thm)],[t39,t47]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t132768,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t6,t47]) ).
cnf(t50,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t132768]) ).
cnf(t132953,plain,
meet(X1,join(join(X1,X2),meet(X3,join(X2,join(X4,X1))))) = meet(X1,join(join(X1,X2),meet(X3,join(X4,X1)))),
inference(step,[status(thm)],[t132952,t50]) ).
cnf(t132954,plain,
meet(X1,join(join(X1,X2),meet(X3,join(X1,join(X2,X4))))) = meet(X1,join(join(X1,X2),meet(X3,join(X4,X1)))),
inference(step,[status(thm)],[t132953,t50]) ).
cnf(t132955,plain,
meet(X1,join(join(X1,X2),meet(X3,join(X1,join(X2,X4))))) = meet(X1,join(join(X1,X2),meet(X3,join(X1,X4)))),
inference(step,[status(thm)],[t132954,t47]) ).
cnf(t1529,plain,
meet(X1,join(join(X1,X2),meet(X3,join(X1,join(X2,X4))))) = meet(X1,join(join(X1,X2),meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t132955]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t12,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t1568,plain,
meet(X1,join(join(X1,X2),meet(X3,join(X1,meet(X2,X4))))) = meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t1529,t12]) ).
cnf(t37,plain,
meet(X1,join(X2,meet(X3,join(X2,X1)))) = meet(X1,join(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t33,t12]) ).
cnf(t132789,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X3,X1))),
inference(step,[status(thm)],[t37,t47]) ).
cnf(t132790,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t132789,t13]) ).
cnf(t149,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t132790]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t53,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t50,t11]) ).
cnf(t132771,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t53,t50]) ).
cnf(t132772,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t132771,t47]) ).
cnf(t77,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t132772]) ).
cnf(t155,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)],[t149,t77]) ).
cnf(t132849,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)],[t155,t47]) ).
cnf(t132850,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)],[t132849,t50]) ).
cnf(t132851,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)],[t132850,t50]) ).
cnf(t54,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t50,t12]) ).
cnf(t132776,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t54,t50]) ).
cnf(t132777,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t132776,t47]) ).
cnf(t132778,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t132777,t47]) ).
cnf(t96,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t132778]) ).
cnf(t132852,plain,
meet(X1,join(X1,X2)) = meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t132851,t96]) ).
cnf(t132853,plain,
X1 = meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t132852,t10]) ).
cnf(t493,plain,
meet(X1,join(join(X1,X2),meet(X3,join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t132853]) ).
cnf(t132958,plain,
meet(X1,join(join(X1,X2),meet(X3,join(X1,meet(X2,X4))))) = X1,
inference(step,[status(thm)],[t1568,t493]) ).
cnf(t1678,plain,
meet(X1,join(join(X1,X2),meet(X3,join(X1,meet(X2,X4))))) = X1,
inference(orient,[status(thm)],[t132958]) ).
cnf(t150,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(cp,[status(thm)],[t149,t12]) ).
cnf(t167,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t150]) ).
cnf(t181,plain,
meet(X1,meet(join(X2,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t167]) ).
cnf(t132791,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t181,t13]) ).
cnf(t132792,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t132791,t15]) ).
cnf(t132793,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t132792,t15]) ).
cnf(t183,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t132793]) ).
cnf(t200,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,join(meet(X2,join(X3,meet(X1,X3))),meet(X1,meet(X3,X2)))),
inference(cp,[status(thm)],[t167,t183]) ).
cnf(t2877,plain,
meet(X1,join(meet(X1,meet(X2,X3)),meet(X3,join(X2,meet(X1,X2))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t200]) ).
cnf(t2935,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,join(meet(X1,X2),meet(join(X2,X3),join(X2,meet(X1,X2))))),
inference(cp,[status(thm)],[t2877,t10]) ).
cnf(t133007,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(X2,X3),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t2935,t10]) ).
cnf(t3047,plain,
meet(X1,join(meet(X1,X2),meet(join(X2,X3),join(X2,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t133007]) ).
cnf(t3164,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(meet(X1,X2),join(X2,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t1678,t3047]) ).
cnf(t133014,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,X2),join(meet(X1,X2),join(X2,X3)))),
inference(step,[status(thm)],[t3164,t47]) ).
cnf(t133015,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t133014,t77]) ).
cnf(t133016,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),X2))),
inference(step,[status(thm)],[t133015,t50]) ).
cnf(t133017,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t133016,t50]) ).
cnf(t3336,plain,
meet(meet(X1,X2),join(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t133017]) ).
cnf(t3439,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,join(X3,meet(X2,X1)))),
inference(cp,[status(thm)],[t3336,t13]) ).
cnf(t133018,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t3439,t96]) ).
cnf(t3488,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t133018]) ).
cnf(t19,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t15,t10]) ).
cnf(t132773,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t19,t15]) ).
cnf(t132774,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t132773,t13]) ).
cnf(t132775,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t132774,t13]) ).
cnf(t85,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t132775]) ).
cnf(t3523,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(cp,[status(thm)],[t3488,t85]) ).
cnf(t133019,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(step,[status(thm)],[t3523,t85]) ).
cnf(t133020,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t133019,t47]) ).
cnf(t3600,plain,
meet(meet(X1,X2),join(X3,meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t133020]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox2/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(t132769,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t18,t15]) ).
cnf(t132770,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t132769,t13]) ).
cnf(t68,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t132770]) ).
cnf(t3633,plain,
meet(X1,meet(X1,X2)) = meet(meet(X1,X2),join(X3,meet(meet(X1,X2),join(X1,X4)))),
inference(cp,[status(thm)],[t3600,t68]) ).
cnf(t133021,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(meet(X1,X2),join(X1,X4)))),
inference(step,[status(thm)],[t3633,t68]) ).
cnf(t169,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t167,t85]) ).
cnf(t132800,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(step,[status(thm)],[t169,t85]) ).
cnf(t132801,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t132800,t47]) ).
cnf(t222,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t132801]) ).
cnf(t224,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,join(meet(X1,X2),meet(join(X2,meet(X1,X2)),join(X1,X3)))),
inference(cp,[status(thm)],[t222,t167]) ).
cnf(t132872,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(X2,meet(X1,X2)),join(X1,X3)))),
inference(step,[status(thm)],[t224,t167]) ).
cnf(t132873,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(X1,X3),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t132872,t13]) ).
cnf(t715,plain,
meet(X1,join(meet(X1,X2),meet(join(X1,X3),join(X2,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t132873]) ).
cnf(t1702,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(meet(X1,X2),join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t1678,t715]) ).
cnf(t132969,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,X2),join(meet(X1,X2),join(X1,X3)))),
inference(step,[status(thm)],[t1702,t47]) ).
cnf(t132970,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t132969,t77]) ).
cnf(t132971,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),X1))),
inference(step,[status(thm)],[t132970,t50]) ).
cnf(t132972,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t132971,t50]) ).
cnf(t132973,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t132972,t96]) ).
cnf(t2019,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t132973]) ).
cnf(t133022,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t133021,t2019]) ).
cnf(t3733,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t133022]) ).
cnf(t3558,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X2,X4)))) = meet(X1,join(X2,meet(X3,X4))),
inference(cp,[status(thm)],[t33,t3488]) ).
cnf(t5302,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X2,X4)))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t3558]) ).
cnf(t5313,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(join(X2,X4),meet(X3,X4)))),
inference(cp,[status(thm)],[t5302,t13]) ).
cnf(t133054,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X4,meet(join(X2,X4),X3)))),
inference(step,[status(thm)],[t5313,t15]) ).
cnf(t133055,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X3,meet(X4,join(X2,X4))))),
inference(step,[status(thm)],[t133054,t15]) ).
cnf(t5508,plain,
meet(X1,join(X2,meet(X3,meet(X4,join(X2,X4))))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t133055]) ).
cnf(t3645,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(meet(X1,X2),join(X4,meet(join(X1,X3),join(meet(X1,X2),Y4)))),
inference(cp,[status(thm)],[t3600,t2019]) ).
cnf(t133286,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(join(X1,X3),join(meet(X1,X2),Y4)))),
inference(step,[status(thm)],[t3645,t2019]) ).
cnf(t133287,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(join(X1,X3),join(Y4,meet(X1,X2))))),
inference(step,[status(thm)],[t133286,t47]) ).
cnf(t19137,plain,
meet(meet(X1,X2),join(X3,meet(join(X1,X4),join(Y4,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t133287]) ).
cnf(t19241,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,join(X4,meet(X1,X2))))),
inference(cp,[status(thm)],[t19137,t11]) ).
cnf(t19439,plain,
meet(meet(X1,X2),join(X3,meet(X1,join(X4,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t19241]) ).
cnf(t38,plain,
meet(X1,join(X2,meet(X3,join(X2,meet(X1,X2))))) = meet(X1,join(X2,meet(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t33,t11]) ).
cnf(t132794,plain,
meet(X1,join(X2,meet(X3,join(X2,X2)))) = meet(X1,join(X2,meet(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t38,t33]) ).
cnf(t132795,plain,
meet(X1,join(X2,meet(X3,X2))) = meet(X1,join(X2,meet(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t132794,t11]) ).
cnf(t132796,plain,
meet(X1,join(X2,meet(X2,X3))) = meet(X1,join(X2,meet(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t132795,t13]) ).
cnf(t132797,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t132796,t12]) ).
cnf(t132798,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X2,meet(X3,X1)))),
inference(step,[status(thm)],[t132797,t15]) ).
cnf(t132799,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t132798,t15]) ).
cnf(t206,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t132799]) ).
cnf(t19498,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))),
inference(cp,[status(thm)],[t19439,t206]) ).
cnf(t19853,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t19498]) ).
cnf(t252,plain,
meet(X1,meet(join(meet(X1,X2),meet(X2,join(X1,X3))),X4)) = meet(X4,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t222]) ).
cnf(t132859,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t252,t13]) ).
cnf(t132860,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X2,meet(X4,X1)),
inference(step,[status(thm)],[t132859,t15]) ).
cnf(t132861,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t132860,t15]) ).
cnf(t585,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,X4))))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t132861]) ).
cnf(t19867,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)],[t19853,t585]) ).
cnf(t133295,plain,
meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t19867,t585]) ).
cnf(t20381,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133295]) ).
cnf(t20536,plain,
meet(X1,meet(meet(X2,X3),join(X2,X4))) = meet(meet(X1,meet(X2,X3)),join(Y4,meet(X1,join(X2,X4)))),
inference(cp,[status(thm)],[t20381,t2019]) ).
cnf(t133331,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,meet(X1,join(X2,X4)))),
inference(step,[status(thm)],[t20536,t2019]) ).
cnf(t23642,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,join(X2,Y4)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133331]) ).
cnf(t23732,plain,
meet(meet(X1,X2),meet(X3,X4)) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(cp,[status(thm)],[t23642,t19137]) ).
cnf(t133406,plain,
meet(X4,meet(meet(X1,X2),X3)) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t23732,t15]) ).
cnf(t133407,plain,
meet(X3,meet(X4,meet(X1,X2))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t133406,t15]) ).
cnf(t133408,plain,
meet(X3,meet(X2,meet(X4,X1))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t133407,t15]) ).
cnf(t133409,plain,
meet(X3,meet(X1,meet(X2,X4))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t133408,t15]) ).
cnf(t133410,plain,
meet(X1,meet(meet(X2,X4),X3)) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t133409,t15]) ).
cnf(t133411,plain,
meet(X1,meet(X3,meet(X2,X4))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t133410,t13]) ).
cnf(t133412,plain,
meet(X1,meet(X2,meet(X4,X3))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t133411,t15]) ).
cnf(t133413,plain,
meet(X1,meet(X2,meet(X3,X4))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t133412,t13]) ).
cnf(t133414,plain,
meet(X1,meet(X2,meet(X3,X4))) = meet(join(Y4,meet(X1,X2)),meet(meet(X1,X2),meet(X3,X4))),
inference(step,[status(thm)],[t133413,t13]) ).
cnf(t133415,plain,
meet(X1,meet(X2,meet(X3,X4))) = meet(meet(X3,X4),meet(join(Y4,meet(X1,X2)),meet(X1,X2))),
inference(step,[status(thm)],[t133414,t15]) ).
cnf(t133416,plain,
meet(X1,meet(X2,meet(X3,X4))) = meet(meet(X1,X2),meet(meet(X3,X4),join(Y4,meet(X1,X2)))),
inference(step,[status(thm)],[t133415,t15]) ).
cnf(t31267,plain,
meet(meet(X1,X2),meet(meet(X3,X4),join(Y4,meet(X1,X2)))) = meet(X1,meet(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t133416]) ).
cnf(t511,plain,
join(X1,X2) = meet(join(X1,X2),join(join(join(X1,X2),meet(X3,join(X1,X2))),X1)),
inference(cp,[status(thm)],[t493,t493]) ).
cnf(t132884,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(join(X1,X2),meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t511,t47]) ).
cnf(t939,plain,
meet(join(X1,X2),join(X1,join(join(X1,X2),meet(X3,join(X1,X2))))) = join(X1,X2),
inference(orient,[status(thm)],[t132884]) ).
cnf(t31551,plain,
meet(X1,meet(X2,meet(join(X3,X4),join(X3,join(join(X3,X4),meet(Y4,join(X3,X4))))))) = meet(meet(X1,X2),meet(join(X3,X4),join(Y5,meet(X1,X2)))),
inference(cp,[status(thm)],[t31267,t939]) ).
cnf(t133445,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(Y5,meet(X1,X2)))),
inference(step,[status(thm)],[t31551,t939]) ).
cnf(t34905,plain,
meet(meet(X1,X2),meet(join(X3,X4),join(Y4,meet(X1,X2)))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t133445]) ).
cnf(t35080,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(meet(X1,X2),join(X1,X3))))),
inference(cp,[status(thm)],[t34905,t2019]) ).
cnf(t133448,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(X1,X2)))),
inference(step,[status(thm)],[t35080,t2019]) ).
cnf(t133449,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(X4,Y4))) = meet(X1,meet(X2,join(X4,Y4))),
inference(step,[status(thm)],[t133448,t34905]) ).
cnf(t35904,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(X4,Y4))) = meet(X1,meet(X2,join(X4,Y4))),
inference(orient,[status(thm)],[t133449]) ).
cnf(t36176,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),meet(join(Y4,join(Y5,X1)),join(X3,X4))),
inference(cp,[status(thm)],[t35904,t50]) ).
cnf(t133505,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(Y4,join(Y5,X1)))),
inference(step,[status(thm)],[t36176,t13]) ).
cnf(t133506,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(X1,join(Y4,Y5)))),
inference(step,[status(thm)],[t133505,t50]) ).
cnf(t45594,plain,
meet(meet(X1,X2),meet(join(X3,X4),join(X1,join(Y4,Y5)))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t133506]) ).
cnf(t45987,plain,
meet(X1,join(X2,meet(meet(X2,X3),join(X4,Y4)))) = meet(X1,join(X2,meet(X2,meet(X3,join(X4,Y4))))),
inference(cp,[status(thm)],[t5508,t45594]) ).
cnf(t133507,plain,
meet(X1,join(X2,meet(meet(X2,X3),join(X4,Y4)))) = meet(X1,X2),
inference(step,[status(thm)],[t45987,t12]) ).
cnf(t46061,plain,
meet(X1,join(X2,meet(meet(X2,X3),join(X4,Y4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t133507]) ).
cnf(t46063,plain,
meet(join(X1,meet(meet(X1,X2),join(X3,X4))),X1) = join(X1,meet(meet(X1,X2),join(X3,X4))),
inference(cp,[status(thm)],[t46061,t9]) ).
cnf(t133512,plain,
meet(X1,join(X1,meet(meet(X1,X2),join(X3,X4)))) = join(X1,meet(meet(X1,X2),join(X3,X4))),
inference(step,[status(thm)],[t46063,t13]) ).
cnf(t133513,plain,
meet(X1,X1) = join(X1,meet(meet(X1,X2),join(X3,X4))),
inference(step,[status(thm)],[t133512,t46061]) ).
cnf(t133514,plain,
X1 = join(X1,meet(meet(X1,X2),join(X3,X4))),
inference(step,[status(thm)],[t133513,t9]) ).
cnf(t46757,plain,
join(X1,meet(meet(X1,X2),join(X3,X4))) = X1,
inference(orient,[status(thm)],[t133514]) ).
cnf(t46779,plain,
X1 = join(X1,meet(meet(X2,meet(X3,X1)),join(X4,Y4))),
inference(cp,[status(thm)],[t46757,t15]) ).
cnf(t133515,plain,
X1 = join(X1,meet(join(X4,Y4),meet(X2,meet(X3,X1)))),
inference(step,[status(thm)],[t46779,t13]) ).
cnf(t133516,plain,
X1 = join(X1,meet(meet(X3,X1),meet(join(X4,Y4),X2))),
inference(step,[status(thm)],[t133515,t15]) ).
cnf(t133517,plain,
X1 = join(X1,meet(X2,meet(meet(X3,X1),join(X4,Y4)))),
inference(step,[status(thm)],[t133516,t15]) ).
cnf(t133518,plain,
X1 = join(X1,meet(X2,meet(meet(X1,X3),join(X4,Y4)))),
inference(step,[status(thm)],[t133517,t13]) ).
cnf(t47000,plain,
join(X1,meet(X2,meet(meet(X1,X3),join(X4,Y4)))) = X1,
inference(orient,[status(thm)],[t133518]) ).
cnf(t47186,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(join(X1,X2),join(X4,Y4)))),
inference(cp,[status(thm)],[t47000,t939]) ).
cnf(t48905,plain,
join(join(X1,X2),meet(X3,meet(join(X1,X2),join(X4,Y4)))) = join(X1,X2),
inference(orient,[status(thm)],[t47186]) ).
cnf(t35038,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(Y4,meet(X1,meet(X1,X2))))),
inference(cp,[status(thm)],[t34905,t68]) ).
cnf(t133446,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(Y4,meet(X1,X2)))),
inference(step,[status(thm)],[t35038,t68]) ).
cnf(t133447,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(X1,meet(X2,join(X3,X4))),
inference(step,[status(thm)],[t133446,t34905]) ).
cnf(t35522,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t133447]) ).
cnf(t3763,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4)),
inference(cp,[status(thm)],[t3488,t3733]) ).
cnf(t133024,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4)),
inference(step,[status(thm)],[t3763,t3733]) ).
cnf(t133025,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t133024,t47]) ).
cnf(t133026,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),X4))),
inference(step,[status(thm)],[t133025,t50]) ).
cnf(t133027,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t133026,t47]) ).
cnf(t3887,plain,
meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t133027]) ).
cnf(t3920,plain,
meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))) = meet(meet(X1,X2),join(join(X3,join(X4,meet(X1,X2))),Y4)),
inference(cp,[status(thm)],[t3488,t3887]) ).
cnf(t133063,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(X3,join(X4,meet(X1,X2))),Y4)),
inference(step,[status(thm)],[t3920,t3887]) ).
cnf(t133064,plain,
meet(X1,X2) = meet(meet(X1,X2),join(Y4,join(X3,join(X4,meet(X1,X2))))),
inference(step,[status(thm)],[t133063,t47]) ).
cnf(t133065,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(join(X4,meet(X1,X2)),Y4))),
inference(step,[status(thm)],[t133064,t50]) ).
cnf(t133066,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(Y4,join(X4,meet(X1,X2))))),
inference(step,[status(thm)],[t133065,t47]) ).
cnf(t133067,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(X4,join(meet(X1,X2),Y4)))),
inference(step,[status(thm)],[t133066,t50]) ).
cnf(t133068,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(X4,join(Y4,meet(X1,X2))))),
inference(step,[status(thm)],[t133067,t47]) ).
cnf(t6045,plain,
meet(meet(X1,X2),join(X3,join(X4,join(Y4,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t133068]) ).
cnf(t35539,plain,
meet(X1,meet(X2,join(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t35522,t6045]) ).
cnf(t133462,plain,
meet(X1,meet(X2,join(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X1,X2),
inference(step,[status(thm)],[t35539,t68]) ).
cnf(t38114,plain,
meet(X1,meet(X2,join(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X1,X2),
inference(orient,[status(thm)],[t133462]) ).
cnf(t48916,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(cp,[status(thm)],[t48905,t38114]) ).
cnf(t49432,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t48916]) ).
cnf(t3687,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,meet(X2,X3))),
inference(cp,[status(thm)],[t3600,t3600]) ).
cnf(t3961,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X2,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t3687]) ).
cnf(t4035,plain,
X1 = meet(X1,join(join(X1,X2),meet(X3,meet(X2,X4)))),
inference(cp,[status(thm)],[t1678,t3961]) ).
cnf(t133028,plain,
X1 = meet(X1,join(join(X1,X2),meet(X2,meet(X4,X3)))),
inference(step,[status(thm)],[t4035,t15]) ).
cnf(t133029,plain,
X1 = meet(X1,join(join(X1,X2),meet(X2,meet(X3,X4)))),
inference(step,[status(thm)],[t133028,t13]) ).
cnf(t4065,plain,
meet(X1,join(join(X1,X2),meet(X2,meet(X3,X4)))) = X1,
inference(orient,[status(thm)],[t133029]) ).
cnf(t49511,plain,
join(join(X1,X2),meet(X2,meet(X3,X4))) = join(join(join(X1,X2),meet(X2,meet(X3,X4))),X1),
inference(cp,[status(thm)],[t49432,t4065]) ).
cnf(t133557,plain,
join(join(X1,X2),meet(X2,meet(X3,X4))) = join(X1,join(join(X1,X2),meet(X2,meet(X3,X4)))),
inference(step,[status(thm)],[t49511,t47]) ).
cnf(t53415,plain,
join(X1,join(join(X1,X2),meet(X2,meet(X3,X4)))) = join(join(X1,X2),meet(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t133557]) ).
cnf(t53440,plain,
join(join(X1,X2),meet(X2,meet(X3,X4))) = join(X1,join(join(X2,X1),meet(X2,meet(X3,X4)))),
inference(cp,[status(thm)],[t53415,t47]) ).
cnf(t4098,plain,
X1 = meet(X1,join(join(X1,X2),meet(X2,join(X3,X4)))),
inference(cp,[status(thm)],[t4065,t939]) ).
cnf(t4158,plain,
meet(X1,join(join(X1,X2),meet(X2,join(X3,X4)))) = X1,
inference(orient,[status(thm)],[t4098]) ).
cnf(t19523,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X4,X1)),
inference(cp,[status(thm)],[t19439,t4158]) ).
cnf(t133288,plain,
meet(X1,join(X2,X3)) = meet(join(X4,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t19523,t13]) ).
cnf(t133289,plain,
meet(X1,join(X2,X3)) = meet(join(X2,X3),meet(join(X4,X1),X1)),
inference(step,[status(thm)],[t133288,t15]) ).
cnf(t133290,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X4,X1))),
inference(step,[status(thm)],[t133289,t15]) ).
cnf(t133291,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,X4))),
inference(step,[status(thm)],[t133290,t47]) ).
cnf(t133292,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X4),join(X2,X3))),
inference(step,[status(thm)],[t133291,t13]) ).
cnf(t19705,plain,
meet(X1,meet(join(X1,X2),join(X3,X4))) = meet(X1,join(X3,X4)),
inference(orient,[status(thm)],[t133292]) ).
cnf(t48915,plain,
join(X1,X2) = join(join(X1,X2),meet(X1,join(X3,X4))),
inference(cp,[status(thm)],[t48905,t19705]) ).
cnf(t49177,plain,
join(join(X1,X2),meet(X1,join(X3,X4))) = join(X1,X2),
inference(orient,[status(thm)],[t48915]) ).
cnf(t19737,plain,
meet(X1,join(X2,meet(X3,join(join(X1,X4),X2)))) = meet(X1,meet(join(X1,X4),join(X2,meet(join(X1,X4),X3)))),
inference(cp,[status(thm)],[t19705,t149]) ).
cnf(t133312,plain,
meet(X1,join(X2,meet(X3,join(X2,join(X1,X4))))) = meet(X1,meet(join(X1,X4),join(X2,meet(join(X1,X4),X3)))),
inference(step,[status(thm)],[t19737,t47]) ).
cnf(t133313,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X4,X2))))) = meet(X1,meet(join(X1,X4),join(X2,meet(join(X1,X4),X3)))),
inference(step,[status(thm)],[t133312,t50]) ).
cnf(t133314,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X4))))) = meet(X1,meet(join(X1,X4),join(X2,meet(join(X1,X4),X3)))),
inference(step,[status(thm)],[t133313,t47]) ).
cnf(t133315,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X4))))) = meet(X1,join(X2,meet(join(X1,X4),X3))),
inference(step,[status(thm)],[t133314,t19705]) ).
cnf(t133316,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)],[t133315,t13]) ).
cnf(t22277,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)],[t133316]) ).
cnf(t3992,plain,
meet(X1,meet(join(X2,X3),join(X2,join(join(X2,X3),meet(X4,join(X2,X3)))))) = meet(meet(X1,join(X2,X3)),join(Y4,meet(join(X2,X3),join(X2,join(join(X2,X3),meet(X4,join(X2,X3))))))),
inference(cp,[status(thm)],[t3961,t939]) ).
cnf(t133030,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,meet(join(X2,X3),join(X2,join(join(X2,X3),meet(X4,join(X2,X3))))))),
inference(step,[status(thm)],[t3992,t939]) ).
cnf(t133031,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,join(X2,X3))),
inference(step,[status(thm)],[t133030,t939]) ).
cnf(t133032,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X3,join(Y4,X2))),
inference(step,[status(thm)],[t133031,t50]) ).
cnf(t133033,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,join(X3,Y4))),
inference(step,[status(thm)],[t133032,t50]) ).
cnf(t4268,plain,
meet(meet(X1,join(X2,X3)),join(X2,join(X3,X4))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t133033]) ).
cnf(t22290,plain,
meet(X1,join(X2,meet(meet(X3,join(X1,X2)),join(X1,X4)))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t22277,t4268]) ).
cnf(t133370,plain,
meet(X1,join(X2,meet(join(X1,X4),meet(X3,join(X1,X2))))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t22290,t13]) ).
cnf(t133371,plain,
meet(X1,join(X2,meet(join(X1,X2),meet(join(X1,X4),X3)))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t133370,t15]) ).
cnf(t133372,plain,
meet(X1,join(X2,meet(X3,meet(join(X1,X2),join(X1,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t133371,t15]) ).
cnf(t133373,plain,
meet(X1,join(X2,meet(X3,meet(join(X1,X2),join(X1,X4))))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t133372,t149]) ).
cnf(t29009,plain,
meet(X1,join(X2,meet(X3,meet(join(X1,X2),join(X1,X4))))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t133373]) ).
cnf(t35407,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(X3,meet(X4,join(X1,X2))))),
inference(cp,[status(thm)],[t29009,t34905]) ).
cnf(t38777,plain,
meet(X1,join(X2,meet(X3,meet(X4,join(X1,X2))))) = meet(X1,join(X2,meet(X1,meet(X3,X4)))),
inference(orient,[status(thm)],[t35407]) ).
cnf(t19866,plain,
meet(X1,meet(X2,X3)) = meet(join(X4,meet(X1,X2)),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t19853,t13]) ).
cnf(t133293,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X3),meet(join(X4,meet(X1,X2)),X1)),
inference(step,[status(thm)],[t19866,t15]) ).
cnf(t133294,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t133293,t15]) ).
cnf(t20139,plain,
meet(X1,meet(meet(X2,X3),join(X4,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133294]) ).
cnf(t38812,plain,
meet(X1,join(meet(X2,X3),meet(X1,meet(X2,meet(X3,X4))))) = meet(X1,join(meet(X2,X3),meet(X2,meet(X3,X4)))),
inference(cp,[status(thm)],[t38777,t20139]) ).
cnf(t31739,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,meet(X3,X4)))),
inference(cp,[status(thm)],[t12,t31267]) ).
cnf(t31917,plain,
join(meet(X1,X2),meet(X1,meet(X2,meet(X3,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t31739]) ).
cnf(t20660,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X3))) = meet(meet(X1,meet(X2,X3)),join(join(X4,meet(X1,X3)),Y4)),
inference(cp,[status(thm)],[t3488,t20381]) ).
cnf(t133333,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(join(X4,meet(X1,X3)),Y4)),
inference(step,[status(thm)],[t20660,t20381]) ).
cnf(t133334,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,join(X4,meet(X1,X3)))),
inference(step,[status(thm)],[t133333,t47]) ).
cnf(t133335,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,join(meet(X1,X3),Y4))),
inference(step,[status(thm)],[t133334,t50]) ).
cnf(t133336,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,join(Y4,meet(X1,X3)))),
inference(step,[status(thm)],[t133335,t47]) ).
cnf(t24304,plain,
meet(meet(X1,meet(X2,X3)),join(X4,join(Y4,meet(X1,X3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133336]) ).
cnf(t24305,plain,
meet(X1,meet(X2,X3)) = meet(join(X4,join(Y4,meet(X1,X3))),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t24304,t13]) ).
cnf(t133344,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X3),meet(join(X4,join(Y4,meet(X1,X3))),X1)),
inference(step,[status(thm)],[t24305,t15]) ).
cnf(t133345,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X4,join(Y4,meet(X1,X3))))),
inference(step,[status(thm)],[t133344,t15]) ).
cnf(t26415,plain,
meet(X1,meet(meet(X2,X3),join(X4,join(Y4,meet(X1,X3))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133345]) ).
cnf(t26424,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(join(X4,join(Y4,meet(X1,X3))),meet(X2,X3))),
inference(cp,[status(thm)],[t26415,t13]) ).
cnf(t133349,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X3,meet(join(X4,join(Y4,meet(X1,X3))),X2))),
inference(step,[status(thm)],[t26424,t15]) ).
cnf(t133350,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X3)))))),
inference(step,[status(thm)],[t133349,t15]) ).
cnf(t27165,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X3)))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133350]) ).
cnf(t32025,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t31917,t27165]) ).
cnf(t32234,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t32025]) ).
cnf(t133473,plain,
meet(X1,join(meet(X2,X3),meet(X1,meet(X2,meet(X3,X4))))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t38812,t32234]) ).
cnf(t40679,plain,
meet(X1,join(meet(X2,X3),meet(X1,meet(X2,meet(X3,X4))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133473]) ).
cnf(t49200,plain,
join(X1,X2) = join(join(X1,X2),meet(X1,meet(X3,X4))),
inference(cp,[status(thm)],[t49177,t40679]) ).
cnf(t49721,plain,
join(join(X1,X2),meet(X1,meet(X3,X4))) = join(X1,X2),
inference(orient,[status(thm)],[t49200]) ).
cnf(t133558,plain,
join(join(X1,X2),meet(X2,meet(X3,X4))) = join(X1,join(X2,X1)),
inference(step,[status(thm)],[t53440,t49721]) ).
cnf(t133559,plain,
join(join(X1,X2),meet(X2,meet(X3,X4))) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t133558,t47]) ).
cnf(t133560,plain,
join(join(X1,X2),meet(X2,meet(X3,X4))) = join(X1,X2),
inference(step,[status(thm)],[t133559,t77]) ).
cnf(t53640,plain,
join(join(X1,X2),meet(X2,meet(X3,X4))) = join(X1,X2),
inference(orient,[status(thm)],[t133560]) ).
cnf(t53654,plain,
join(X1,join(X2,meet(X1,X3))) = join(join(X1,X2),meet(join(X2,meet(X1,X3)),meet(X4,Y4))),
inference(cp,[status(thm)],[t53640,t96]) ).
cnf(t133572,plain,
join(X1,X2) = join(join(X1,X2),meet(join(X2,meet(X1,X3)),meet(X4,Y4))),
inference(step,[status(thm)],[t53654,t96]) ).
cnf(t133573,plain,
join(X1,X2) = join(join(X1,X2),meet(Y4,meet(join(X2,meet(X1,X3)),X4))),
inference(step,[status(thm)],[t133572,t15]) ).
cnf(t133574,plain,
join(X1,X2) = join(join(X1,X2),meet(X4,meet(Y4,join(X2,meet(X1,X3))))),
inference(step,[status(thm)],[t133573,t15]) ).
cnf(t55450,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X2,meet(X1,Y4))))) = join(X1,X2),
inference(orient,[status(thm)],[t133574]) ).
cnf(t55508,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X2,meet(X1,X4)))),
inference(cp,[status(thm)],[t55450,t68]) ).
cnf(t55817,plain,
join(join(X1,X2),meet(X3,join(X2,meet(X1,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t55508]) ).
cnf(t56014,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(meet(X1,join(X2,meet(X3,X4))),join(X3,X2)),
inference(cp,[status(thm)],[t3733,t55817]) ).
cnf(t133578,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(join(X3,X2),meet(X1,join(X2,meet(X3,X4)))),
inference(step,[status(thm)],[t56014,t13]) ).
cnf(t133579,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,meet(join(X2,meet(X3,X4)),join(X3,X2))),
inference(step,[status(thm)],[t133578,t15]) ).
cnf(t133580,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,meet(join(X3,X2),join(X2,meet(X3,X4)))),
inference(step,[status(thm)],[t133579,t13]) ).
cnf(t133581,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,meet(join(X2,X3),join(X2,meet(X3,X4)))),
inference(step,[status(thm)],[t133580,t47]) ).
cnf(t56913,plain,
meet(X1,meet(join(X2,X3),join(X2,meet(X3,X4)))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t133581]) ).
cnf(t165,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,t149]) ).
cnf(t132856,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)],[t165,t13]) ).
cnf(t132857,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)],[t132856,t15]) ).
cnf(t132858,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)],[t132857,t13]) ).
cnf(t551,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)],[t132858]) ).
cnf(t56914,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,meet(join(X2,X3),join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t56913,t551]) ).
cnf(t133583,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X2,X3),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t56914,t149]) ).
cnf(t57462,plain,
meet(X1,meet(join(X2,X3),join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t133583]) ).
cnf(t57491,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,meet(join(X2,X3),join(X2,meet(X1,join(X2,X3))))),
inference(cp,[status(thm)],[t57462,t77]) ).
cnf(t5513,plain,
meet(meet(X1,meet(X2,join(X3,X2))),join(X3,meet(X1,X2))) = meet(X1,meet(X2,join(X3,X2))),
inference(cp,[status(thm)],[t5508,t3733]) ).
cnf(t133179,plain,
meet(join(X3,meet(X1,X2)),meet(X1,meet(X2,join(X3,X2)))) = meet(X1,meet(X2,join(X3,X2))),
inference(step,[status(thm)],[t5513,t13]) ).
cnf(t133180,plain,
meet(meet(X2,join(X3,X2)),meet(join(X3,meet(X1,X2)),X1)) = meet(X1,meet(X2,join(X3,X2))),
inference(step,[status(thm)],[t133179,t15]) ).
cnf(t133181,plain,
meet(X1,meet(meet(X2,join(X3,X2)),join(X3,meet(X1,X2)))) = meet(X1,meet(X2,join(X3,X2))),
inference(step,[status(thm)],[t133180,t15]) ).
cnf(t133182,plain,
meet(X1,meet(meet(X2,join(X2,X3)),join(X3,meet(X1,X2)))) = meet(X1,meet(X2,join(X3,X2))),
inference(step,[status(thm)],[t133181,t47]) ).
cnf(t133183,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,meet(X2,join(X3,X2))),
inference(step,[status(thm)],[t133182,t10]) ).
cnf(t133184,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t133183,t47]) ).
cnf(t133185,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(step,[status(thm)],[t133184,t10]) ).
cnf(t12506,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t133185]) ).
cnf(t133584,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t57491,t12506]) ).
cnf(t57849,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t133584]) ).
cnf(t22311,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)],[t22277,t12]) ).
cnf(t133319,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,X4))))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t22311,t149]) ).
cnf(t22649,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,X4))))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t133319]) ).
cnf(t22685,plain,
meet(X1,join(join(X2,X3),meet(X1,meet(X2,X4)))) = meet(X1,join(join(X2,X3),meet(X2,X4))),
inference(cp,[status(thm)],[t22649,t19137]) ).
cnf(t133320,plain,
meet(X1,join(join(X2,X3),meet(X1,meet(X2,X4)))) = meet(X1,join(meet(X2,X4),join(X2,X3))),
inference(step,[status(thm)],[t22685,t47]) ).
cnf(t133321,plain,
meet(X1,join(join(X2,X3),meet(X1,meet(X2,X4)))) = meet(X1,join(X3,join(meet(X2,X4),X2))),
inference(step,[status(thm)],[t133320,t50]) ).
cnf(t133322,plain,
meet(X1,join(join(X2,X3),meet(X1,meet(X2,X4)))) = meet(X1,join(X2,join(X3,meet(X2,X4)))),
inference(step,[status(thm)],[t133321,t50]) ).
cnf(t133323,plain,
meet(X1,join(join(X2,X3),meet(X1,meet(X2,X4)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t133322,t96]) ).
cnf(t22820,plain,
meet(X1,join(join(X2,X3),meet(X1,meet(X2,X4)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t133323]) ).
cnf(t22830,plain,
meet(X1,join(X2,join(X3,X4))) = meet(X1,join(join(X3,join(X4,X2)),meet(X1,meet(X2,Y4)))),
inference(cp,[status(thm)],[t22820,t50]) ).
cnf(t133374,plain,
meet(X1,join(X2,join(X3,X4))) = meet(X1,join(meet(X1,meet(X2,Y4)),join(X3,join(X4,X2)))),
inference(step,[status(thm)],[t22830,t47]) ).
cnf(t133375,plain,
meet(X1,join(X2,join(X3,X4))) = meet(X1,join(join(X4,X2),join(meet(X1,meet(X2,Y4)),X3))),
inference(step,[status(thm)],[t133374,t50]) ).
cnf(t133376,plain,
meet(X1,join(X2,join(X3,X4))) = meet(X1,join(X3,join(join(X4,X2),meet(X1,meet(X2,Y4))))),
inference(step,[status(thm)],[t133375,t50]) ).
cnf(t133377,plain,
meet(X1,join(X2,join(X3,X4))) = meet(X1,join(X3,join(join(X2,X4),meet(X1,meet(X2,Y4))))),
inference(step,[status(thm)],[t133376,t47]) ).
cnf(t29190,plain,
meet(X1,join(X2,join(join(X3,X4),meet(X1,meet(X3,Y4))))) = meet(X1,join(X3,join(X2,X4))),
inference(orient,[status(thm)],[t133377]) ).
cnf(t57862,plain,
meet(X1,join(X2,join(join(X3,X4),meet(X1,meet(X3,Y4))))) = meet(X1,join(X2,meet(X1,join(X3,join(X2,X4))))),
inference(cp,[status(thm)],[t57849,t29190]) ).
cnf(t133602,plain,
meet(X1,join(X3,join(X2,X4))) = meet(X1,join(X2,meet(X1,join(X3,join(X2,X4))))),
inference(step,[status(thm)],[t57862,t29190]) ).
cnf(t60723,plain,
meet(X1,join(X2,meet(X1,join(X3,join(X2,X4))))) = meet(X1,join(X3,join(X2,X4))),
inference(orient,[status(thm)],[t133602]) ).
cnf(t34,plain,
meet(X1,join(X2,meet(X3,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(cp,[status(thm)],[t33,t10]) ).
cnf(t106,plain,
meet(X1,join(X2,meet(X3,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t34]) ).
cnf(t108,plain,
meet(join(X1,meet(X2,join(X1,X2))),join(X1,X2)) = join(X1,meet(X2,join(X1,X2))),
inference(cp,[status(thm)],[t106,t9]) ).
cnf(t132805,plain,
meet(join(X1,X2),join(X1,meet(X2,join(X1,X2)))) = join(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t108,t13]) ).
cnf(t132806,plain,
meet(join(X1,X2),join(X1,X2)) = join(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t132805,t106]) ).
cnf(t132807,plain,
join(X1,X2) = join(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t132806,t9]) ).
cnf(t277,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t132807]) ).
cnf(t278,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,meet(join(X2,meet(X1,X3)),join(X1,X2))),
inference(cp,[status(thm)],[t277,t96]) ).
cnf(t132811,plain,
join(X1,X2) = join(X1,meet(join(X2,meet(X1,X3)),join(X1,X2))),
inference(step,[status(thm)],[t278,t96]) ).
cnf(t132812,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t132811,t13]) ).
cnf(t311,plain,
join(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = join(X1,X2),
inference(orient,[status(thm)],[t132812]) ).
cnf(t335,plain,
join(X1,join(meet(join(X1,X2),join(X2,meet(X1,X3))),X4)) = join(X4,join(X1,X2)),
inference(cp,[status(thm)],[t50,t311]) ).
cnf(t132862,plain,
join(X1,join(X4,meet(join(X1,X2),join(X2,meet(X1,X3))))) = join(X4,join(X1,X2)),
inference(step,[status(thm)],[t335,t47]) ).
cnf(t132863,plain,
join(X1,join(X4,meet(join(X1,X2),join(X2,meet(X1,X3))))) = join(X2,join(X4,X1)),
inference(step,[status(thm)],[t132862,t50]) ).
cnf(t132864,plain,
join(X1,join(X4,meet(join(X1,X2),join(X2,meet(X1,X3))))) = join(X1,join(X2,X4)),
inference(step,[status(thm)],[t132863,t50]) ).
cnf(t641,plain,
join(X1,join(X2,meet(join(X1,X3),join(X3,meet(X1,X4))))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t132864]) ).
cnf(t60754,plain,
meet(X1,join(X2,join(X3,meet(join(X2,X4),join(X4,meet(X2,Y4)))))) = meet(X1,join(X3,meet(X1,join(X2,join(X4,X3))))),
inference(cp,[status(thm)],[t60723,t641]) ).
cnf(t133612,plain,
meet(X1,join(X2,join(X4,X3))) = meet(X1,join(X3,meet(X1,join(X2,join(X4,X3))))),
inference(step,[status(thm)],[t60754,t641]) ).
cnf(t62466,plain,
meet(X1,join(X2,meet(X1,join(X3,join(X4,X2))))) = meet(X1,join(X3,join(X4,X2))),
inference(orient,[status(thm)],[t133612]) ).
cnf(t35,plain,
meet(X1,join(X2,meet(join(X3,meet(X1,X2)),join(X2,X3)))) = meet(X1,join(X2,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t33,t9]) ).
cnf(t132885,plain,
meet(X1,join(X2,meet(join(X2,X3),join(X3,meet(X1,X2))))) = meet(X1,join(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t35,t13]) ).
cnf(t132886,plain,
meet(X1,join(X2,meet(join(X2,X3),join(X2,X3)))) = meet(X1,join(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t132885,t33]) ).
cnf(t132887,plain,
meet(X1,join(X2,join(X2,X3))) = meet(X1,join(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t132886,t9]) ).
cnf(t132888,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t132887,t77]) ).
cnf(t992,plain,
meet(X1,join(X2,join(X3,meet(X1,X2)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t132888]) ).
cnf(t1021,plain,
meet(X1,join(meet(X2,X3),X4)) = meet(X1,join(meet(X2,X3),join(X4,meet(X2,meet(X3,X1))))),
inference(cp,[status(thm)],[t992,t15]) ).
cnf(t132892,plain,
meet(X1,join(X4,meet(X2,X3))) = meet(X1,join(meet(X2,X3),join(X4,meet(X2,meet(X3,X1))))),
inference(step,[status(thm)],[t1021,t47]) ).
cnf(t132893,plain,
meet(X1,join(X4,meet(X2,X3))) = meet(X1,join(X4,join(meet(X2,meet(X3,X1)),meet(X2,X3)))),
inference(step,[status(thm)],[t132892,t50]) ).
cnf(t132894,plain,
meet(X1,join(X4,meet(X2,X3))) = meet(X1,join(X4,join(meet(X2,X3),meet(X2,meet(X3,X1))))),
inference(step,[status(thm)],[t132893,t47]) ).
cnf(t132895,plain,
meet(X1,join(X4,meet(X2,X3))) = meet(X1,join(X4,join(meet(X2,X3),meet(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t132894,t15]) ).
cnf(t1091,plain,
meet(X1,join(X2,join(meet(X3,X4),meet(X1,meet(X3,X4))))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t132895]) ).
cnf(t1096,plain,
meet(X1,join(X2,meet(X3,X3))) = meet(X1,join(X2,join(X3,meet(X1,meet(X3,X3))))),
inference(cp,[status(thm)],[t1091,t9]) ).
cnf(t132896,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(X3,meet(X1,meet(X3,X3))))),
inference(step,[status(thm)],[t1096,t9]) ).
cnf(t132897,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(X3,meet(X1,X3)))),
inference(step,[status(thm)],[t132896,t9]) ).
cnf(t1142,plain,
meet(X1,join(X2,join(X3,meet(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t132897]) ).
cnf(t62495,plain,
meet(X1,join(X2,join(X3,meet(X1,X3)))) = meet(X1,join(meet(X1,X3),meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t62466,t1142]) ).
cnf(t133614,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X1,X3),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t62495,t1142]) ).
cnf(t63128,plain,
meet(X1,join(meet(X1,X2),meet(X1,join(X3,X2)))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t133614]) ).
cnf(t62544,plain,
meet(X1,join(X2,join(X3,meet(X3,X4)))) = meet(X1,join(meet(X3,X4),meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t62466,t12]) ).
cnf(t133617,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X3,X4),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t62544,t12]) ).
cnf(t64457,plain,
meet(X1,join(meet(X2,X3),meet(X1,join(X4,X2)))) = meet(X1,join(X4,X2)),
inference(orient,[status(thm)],[t133617]) ).
cnf(t1699,plain,
join(X1,X2) = meet(join(X1,X2),join(join(join(X1,X2),X3),X1)),
inference(cp,[status(thm)],[t1678,t493]) ).
cnf(t132959,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(join(X1,X2),X3))),
inference(step,[status(thm)],[t1699,t47]) ).
cnf(t132960,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X3,join(X1,X2)))),
inference(step,[status(thm)],[t132959,t47]) ).
cnf(t132961,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,join(X3,X1)))),
inference(step,[status(thm)],[t132960,t50]) ).
cnf(t132962,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t132961,t50]) ).
cnf(t132963,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t132962,t77]) ).
cnf(t1742,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t132963]) ).
cnf(t3643,plain,
meet(X1,join(X1,X2)) = meet(X1,join(X3,meet(join(X1,X2),join(X1,X4)))),
inference(cp,[status(thm)],[t3600,t10]) ).
cnf(t133023,plain,
X1 = meet(X1,join(X3,meet(join(X1,X2),join(X1,X4)))),
inference(step,[status(thm)],[t3643,t10]) ).
cnf(t3813,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X1,X4)))) = X1,
inference(orient,[status(thm)],[t133023]) ).
cnf(t49474,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)],[t49432,t3813]) ).
cnf(t133553,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)],[t49474,t47]) ).
cnf(t133554,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)],[t133553,t50]) ).
cnf(t133555,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)],[t133554,t47]) ).
cnf(t52720,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)],[t133555]) ).
cnf(t52761,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,meet(join(X2,X3),join(X2,X4)))),
inference(cp,[status(thm)],[t1742,t52720]) ).
cnf(t52839,plain,
meet(join(X1,X2),join(X1,meet(join(X2,X3),join(X2,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t52761]) ).
cnf(t52840,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,meet(join(X2,X3),join(X1,X2)))),
inference(cp,[status(thm)],[t52839,t33]) ).
cnf(t133556,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,meet(join(X1,X2),join(X2,X3)))),
inference(step,[status(thm)],[t52840,t13]) ).
cnf(t53122,plain,
meet(join(X1,X2),join(X1,meet(join(X1,X2),join(X2,X3)))) = join(X1,X2),
inference(orient,[status(thm)],[t133556]) ).
cnf(t64469,plain,
meet(join(meet(X1,X2),X3),join(X3,X1)) = join(meet(X1,X2),X3),
inference(cp,[status(thm)],[t64457,t53122]) ).
cnf(t133618,plain,
meet(join(X3,X1),join(meet(X1,X2),X3)) = join(meet(X1,X2),X3),
inference(step,[status(thm)],[t64469,t13]) ).
cnf(t133619,plain,
meet(join(X1,X3),join(meet(X1,X2),X3)) = join(meet(X1,X2),X3),
inference(step,[status(thm)],[t133618,t47]) ).
cnf(t133620,plain,
meet(join(X1,X3),join(X3,meet(X1,X2))) = join(meet(X1,X2),X3),
inference(step,[status(thm)],[t133619,t47]) ).
cnf(t133621,plain,
meet(join(X1,X3),join(X3,meet(X1,X2))) = join(X3,meet(X1,X2)),
inference(step,[status(thm)],[t133620,t47]) ).
cnf(t64806,plain,
meet(join(X1,X2),join(X2,meet(X1,X3))) = join(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t133621]) ).
cnf(t64848,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t64806,t12]) ).
cnf(t66609,plain,
meet(X1,join(meet(X1,X2),meet(X1,X3))) = join(meet(X1,X2),meet(X1,X3)),
inference(orient,[status(thm)],[t64848]) ).
cnf(t133629,plain,
join(meet(X1,X2),meet(X1,join(X3,X2))) = meet(X1,join(X3,X2)),
inference(step,[status(thm)],[t63128,t66609]) ).
cnf(t66955,plain,
join(meet(X1,X2),meet(X1,join(X3,X2))) = meet(X1,join(X3,X2)),
inference(rw,[status(thm)],[t133629]) ).
cnf(t133631,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X3,X2)),
inference(step,[status(thm)],[t66955,t47]) ).
cnf(t133632,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t133631,t47]) ).
cnf(t66957,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t133632]) ).
cnf(t22828,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X1,meet(X2,X4)),join(X2,X3))),
inference(cp,[status(thm)],[t22820,t47]) ).
cnf(t133324,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X3,join(meet(X1,meet(X2,X4)),X2))),
inference(step,[status(thm)],[t22828,t50]) ).
cnf(t133325,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(X3,meet(X1,meet(X2,X4))))),
inference(step,[status(thm)],[t133324,t50]) ).
cnf(t23048,plain,
meet(X1,join(X2,join(X3,meet(X1,meet(X2,X4))))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t133325]) ).
cnf(t60738,plain,
meet(X1,join(X2,join(X3,meet(X1,meet(X2,X4))))) = meet(X1,join(X3,meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t60723,t23048]) ).
cnf(t133603,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X3,meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t60738,t23048]) ).
cnf(t60990,plain,
meet(X1,join(X2,meet(X1,join(X3,X2)))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t133603]) ).
cnf(t67130,plain,
meet(X1,join(X2,meet(X1,join(X3,X2)))) = join(meet(X1,X2),meet(X1,join(X3,X2))),
inference(cp,[status(thm)],[t66957,t60990]) ).
cnf(t133633,plain,
meet(X1,join(X3,X2)) = join(meet(X1,X2),meet(X1,join(X3,X2))),
inference(step,[status(thm)],[t67130,t60990]) ).
cnf(t67407,plain,
join(meet(X1,X2),meet(X1,join(X3,X2))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t133633]) ).
cnf(t67625,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(meet(join(X1,X2),join(X2,X3)),join(X1,X2)),
inference(cp,[status(thm)],[t67407,t1742]) ).
cnf(t133636,plain,
join(X1,X2) = join(meet(join(X1,X2),join(X2,X3)),join(X1,X2)),
inference(step,[status(thm)],[t67625,t1742]) ).
cnf(t133637,plain,
join(X1,X2) = join(X2,join(meet(join(X1,X2),join(X2,X3)),X1)),
inference(step,[status(thm)],[t133636,t50]) ).
cnf(t133638,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X2),join(X2,X3)))),
inference(step,[status(thm)],[t133637,t50]) ).
cnf(t68256,plain,
join(X1,join(X2,meet(join(X1,X2),join(X2,X3)))) = join(X1,X2),
inference(orient,[status(thm)],[t133638]) ).
cnf(t68301,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X2,X1),join(X2,X3)))),
inference(cp,[status(thm)],[t68256,t47]) ).
cnf(t133639,plain,
join(X1,X2) = join(X1,meet(join(X2,X1),join(X2,X3))),
inference(step,[status(thm)],[t68301,t52720]) ).
cnf(t133640,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t133639,t47]) ).
cnf(t68404,plain,
join(X1,meet(join(X1,X2),join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t133640]) ).
cnf(t12637,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)],[t167,t12506]) ).
cnf(t133197,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X3,meet(X1,X2))),meet(X1,X2))),
inference(step,[status(thm)],[t12637,t12506]) ).
cnf(t133198,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t133197,t47]) ).
cnf(t14316,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X3,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t133198]) ).
cnf(t14576,plain,
meet(X1,meet(X2,join(meet(X2,X3),meet(X1,X3)))) = meet(X1,meet(X2,X3)),
inference(cp,[status(thm)],[t551,t14316]) ).
cnf(t133199,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X2,X3)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t14576,t47]) ).
cnf(t14599,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X2,X3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133199]) ).
cnf(t14692,plain,
meet(meet(X1,X2),meet(X3,join(X4,meet(X2,join(X1,Y4))))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,meet(X2,join(X1,Y4))))))),
inference(cp,[status(thm)],[t14599,t3600]) ).
cnf(t133212,plain,
meet(X3,meet(join(X4,meet(X2,join(X1,Y4))),meet(X1,X2))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,meet(X2,join(X1,Y4))))))),
inference(step,[status(thm)],[t14692,t15]) ).
cnf(t133213,plain,
meet(X3,meet(X2,meet(join(X4,meet(X2,join(X1,Y4))),X1))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,meet(X2,join(X1,Y4))))))),
inference(step,[status(thm)],[t133212,t15]) ).
cnf(t133214,plain,
meet(X3,meet(X1,meet(X2,join(X4,meet(X2,join(X1,Y4)))))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,meet(X2,join(X1,Y4))))))),
inference(step,[status(thm)],[t133213,t15]) ).
cnf(t133215,plain,
meet(X1,meet(meet(X2,join(X4,meet(X2,join(X1,Y4)))),X3)) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,meet(X2,join(X1,Y4))))))),
inference(step,[status(thm)],[t133214,t15]) ).
cnf(t133216,plain,
meet(X1,meet(X3,meet(X2,join(X4,meet(X2,join(X1,Y4)))))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,meet(X2,join(X1,Y4))))))),
inference(step,[status(thm)],[t133215,t13]) ).
cnf(t133217,plain,
meet(X1,meet(X2,meet(join(X4,meet(X2,join(X1,Y4))),X3))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,meet(X2,join(X1,Y4))))))),
inference(step,[status(thm)],[t133216,t15]) ).
cnf(t133218,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X2,join(X1,Y4)))))) = meet(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X3,join(X4,meet(X2,join(X1,Y4))))))),
inference(step,[status(thm)],[t133217,t13]) ).
cnf(t133219,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X2,join(X1,Y4)))))) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t133218,t85]) ).
cnf(t133220,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X2,join(X1,Y4)))))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t133219,t13]) ).
cnf(t133221,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X2,join(X1,Y4)))))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t133220,t15]) ).
cnf(t133222,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X2,join(X1,Y4)))))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t133221,t15]) ).
cnf(t15266,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X2,join(X1,Y4)))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133222]) ).
cnf(t15271,plain,
meet(X1,meet(X2,X2)) = meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))),
inference(cp,[status(thm)],[t15266,t68]) ).
cnf(t133223,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))),
inference(step,[status(thm)],[t15271,t9]) ).
cnf(t15414,plain,
meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t133223]) ).
cnf(t66875,plain,
meet(X1,X2) = meet(X1,join(meet(X2,X3),meet(X2,join(X1,X4)))),
inference(cp,[status(thm)],[t15414,t66609]) ).
cnf(t67894,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t66875]) ).
cnf(t68414,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X1,meet(X2,X3)),X2)),
inference(cp,[status(thm)],[t68404,t67894]) ).
cnf(t133641,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t68414,t13]) ).
cnf(t68645,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133641]) ).
cnf(t4333,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)],[t149,t4268]) ).
cnf(t133077,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)],[t4333,t85]) ).
cnf(t133078,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)],[t133077,t47]) ).
cnf(t133079,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)],[t133078,t50]) ).
cnf(t133080,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)],[t133079,t50]) ).
cnf(t6554,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)],[t133080]) ).
cnf(t68660,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)],[t68645,t6554]) ).
cnf(t133666,plain,
join(join(X1,X2),X3) = join(join(X1,X2),meet(X3,join(X1,join(X2,meet(X3,X3))))),
inference(step,[status(thm)],[t68660,t10]) ).
cnf(t133667,plain,
join(X3,join(X1,X2)) = join(join(X1,X2),meet(X3,join(X1,join(X2,meet(X3,X3))))),
inference(step,[status(thm)],[t133666,t47]) ).
cnf(t133668,plain,
join(X2,join(X3,X1)) = join(join(X1,X2),meet(X3,join(X1,join(X2,meet(X3,X3))))),
inference(step,[status(thm)],[t133667,t50]) ).
cnf(t133669,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(X3,join(X1,join(X2,meet(X3,X3))))),
inference(step,[status(thm)],[t133668,t50]) ).
cnf(t133670,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(X3,join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t133669,t9]) ).
cnf(t73233,plain,
join(join(X1,X2),meet(X3,join(X1,join(X2,X3)))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t133670]) ).
cnf(t2042,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X2,X3)))) = meet(X1,join(X2,meet(X3,X4))),
inference(cp,[status(thm)],[t33,t2019]) ).
cnf(t2066,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X2,X3)))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t2042]) ).
cnf(t2070,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(join(X2,X3),meet(X3,X4)))),
inference(cp,[status(thm)],[t2066,t13]) ).
cnf(t132974,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X4,meet(join(X2,X3),X3)))),
inference(step,[status(thm)],[t2070,t15]) ).
cnf(t132975,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X3,meet(X4,join(X2,X3))))),
inference(step,[status(thm)],[t132974,t15]) ).
cnf(t2126,plain,
meet(X1,join(X2,meet(X3,meet(X4,join(X2,X3))))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t132975]) ).
cnf(t64813,plain,
join(X1,meet(X2,meet(X3,join(X1,X2)))) = meet(join(X2,X1),join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t64806,t2126]) ).
cnf(t133624,plain,
join(X1,meet(X2,meet(X3,join(X1,X2)))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t64813,t64806]) ).
cnf(t65188,plain,
join(X1,meet(X2,meet(X3,join(X1,X2)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133624]) ).
cnf(t65401,plain,
join(X1,join(meet(X2,meet(X3,join(X1,X2))),X4)) = join(X4,join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t50,t65188]) ).
cnf(t133681,plain,
join(X1,join(X4,meet(X2,meet(X3,join(X1,X2))))) = join(X4,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t65401,t47]) ).
cnf(t133682,plain,
join(X1,join(X4,meet(X2,meet(X3,join(X1,X2))))) = join(X1,join(meet(X2,X3),X4)),
inference(step,[status(thm)],[t133681,t50]) ).
cnf(t133683,plain,
join(X1,join(X4,meet(X2,meet(X3,join(X1,X2))))) = join(X1,join(X4,meet(X2,X3))),
inference(step,[status(thm)],[t133682,t47]) ).
cnf(t75769,plain,
join(X1,join(X2,meet(X3,meet(X4,join(X1,X3))))) = join(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t133683]) ).
cnf(t75930,plain,
join(X1,join(X2,meet(X3,meet(X4,join(X1,X3))))) = join(join(X1,X2),meet(meet(X3,meet(X4,join(X1,X3))),join(X1,join(X2,meet(X3,X4))))),
inference(cp,[status(thm)],[t73233,t75769]) ).
cnf(t133729,plain,
join(X1,join(X2,meet(X3,X4))) = join(join(X1,X2),meet(meet(X3,meet(X4,join(X1,X3))),join(X1,join(X2,meet(X3,X4))))),
inference(step,[status(thm)],[t75930,t75769]) ).
cnf(t20024,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))) = meet(meet(X1,meet(X2,X3)),join(join(X4,meet(X1,X2)),Y4)),
inference(cp,[status(thm)],[t3488,t19853]) ).
cnf(t133327,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(join(X4,meet(X1,X2)),Y4)),
inference(step,[status(thm)],[t20024,t19853]) ).
cnf(t133328,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t133327,t47]) ).
cnf(t133329,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,join(meet(X1,X2),Y4))),
inference(step,[status(thm)],[t133328,t50]) ).
cnf(t133330,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,join(Y4,meet(X1,X2)))),
inference(step,[status(thm)],[t133329,t47]) ).
cnf(t23352,plain,
meet(meet(X1,meet(X2,X3)),join(X4,join(Y4,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t133330]) ).
cnf(t133730,plain,
join(X1,join(X2,meet(X3,X4))) = join(join(X1,X2),meet(X3,meet(X4,join(X1,X3)))),
inference(step,[status(thm)],[t133729,t23352]) ).
cnf(t84988,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X3)))) = join(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t133730]) ).
cnf(t85035,plain,
join(X1,join(meet(X1,X2),meet(X3,X4))) = join(X1,meet(X3,meet(X4,join(X1,X3)))),
inference(cp,[status(thm)],[t84988,t12]) ).
cnf(t133731,plain,
join(X1,join(meet(X1,X2),meet(X3,X4))) = join(X1,meet(X3,X4)),
inference(step,[status(thm)],[t85035,t65188]) ).
cnf(t85526,plain,
join(X1,join(meet(X1,X2),meet(X3,X4))) = join(X1,meet(X3,X4)),
inference(orient,[status(thm)],[t133731]) ).
cnf(t68653,plain,
join(X1,meet(X2,join(X3,meet(X2,X1)))) = join(X1,meet(X2,join(X1,meet(X2,join(X1,X3))))),
inference(cp,[status(thm)],[t68645,t33]) ).
cnf(t133642,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,join(X1,meet(X2,join(X1,X3))))),
inference(step,[status(thm)],[t68653,t13]) ).
cnf(t133643,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t133642,t68645]) ).
cnf(t68817,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t133643]) ).
cnf(t85533,plain,
join(X1,meet(X2,join(X3,meet(meet(X1,X4),X2)))) = join(X1,join(meet(X1,X4),meet(X2,join(meet(X1,X4),X3)))),
inference(cp,[status(thm)],[t85526,t68817]) ).
cnf(t133938,plain,
join(X1,meet(X2,join(X3,meet(X2,meet(X1,X4))))) = join(X1,join(meet(X1,X4),meet(X2,join(meet(X1,X4),X3)))),
inference(step,[status(thm)],[t85533,t13]) ).
cnf(t133939,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X4,X2))))) = join(X1,join(meet(X1,X4),meet(X2,join(meet(X1,X4),X3)))),
inference(step,[status(thm)],[t133938,t15]) ).
cnf(t133940,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X2,X4))))) = join(X1,join(meet(X1,X4),meet(X2,join(meet(X1,X4),X3)))),
inference(step,[status(thm)],[t133939,t13]) ).
cnf(t133941,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X2,X4))))) = join(X1,meet(X2,join(meet(X1,X4),X3))),
inference(step,[status(thm)],[t133940,t85526]) ).
cnf(t133942,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X2,X4))))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(step,[status(thm)],[t133941,t47]) ).
cnf(t132338,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X2,X4))))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t133942]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(b,meet(c,join(d,meet(a,meet(b,c)))))) != meet(a,join(b,meet(c,join(b,d)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(b,meet(c,join(d,meet(a,meet(b,c)))))) != meet(join(b,meet(c,join(d,meet(a,meet(b,c))))),a),
inference(rw,[status(thm)],[goal_0,t13]) ).
cnf(g0_1,plain,
meet(a,join(b,meet(c,join(d,meet(a,meet(b,c)))))) != meet(join(b,meet(c,join(d,meet(b,meet(c,a))))),a),
inference(rw,[status(thm)],[g0_0,t15]) ).
cnf(g0_2,plain,
meet(a,join(b,meet(c,join(d,meet(a,meet(b,c)))))) != meet(join(b,meet(c,join(d,meet(b,a)))),a),
inference(rw,[status(thm)],[g0_1,t132338]) ).
cnf(g0_3,plain,
meet(a,join(b,meet(c,join(d,meet(a,meet(b,c)))))) != meet(join(b,meet(c,join(d,meet(a,b)))),a),
inference(rw,[status(thm)],[g0_2,t13]) ).
cnf(g0_4,plain,
meet(a,join(b,meet(c,join(d,meet(a,meet(b,c)))))) != meet(a,join(b,meet(c,join(d,meet(a,b))))),
inference(rw,[status(thm)],[g0_3,t13]) ).
cnf(g0_5,plain,
meet(a,join(b,meet(c,join(d,meet(a,meet(b,c)))))) != meet(a,join(b,meet(c,join(b,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 : LAT165-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.58 % Computer : n004.cluster.edu
% 0.10/0.58 % Model : x86_64 x86_64
% 0.10/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.58 % Memory : 8046.5625MB
% 0.10/0.58 % OS : Linux 6.8.0-71-generic
% 0.10/0.58 % CPULimit : 300
% 0.10/0.58 % WCLimit : 300
% 0.10/0.58 % DateTime : Wed Sep 23 20:25:51 UTC 2026
% 0.10/0.59 % CPUTime :
% 0.10/0.59 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 82.27/11.15 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 82.27/11.15 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------