%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT399-2 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:57:07 PM UTC 2026
% Result : Unsatisfiable 166.32s 21.55s
% Output : CNFRefutation 166.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 226
% Number of leaves : 12
% Syntax : Number of clauses : 1444 (1444 unt; 0 nHn; 7 RR)
% Number of literals : 1444 (1443 equ; 6 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-3 aty)
% Number of variables : 4716 (1017 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t5,axiom,
meet(X1,join(X2,X3)) = upme(X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t31,plain,
meet(X1,join(X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t5]) ).
cnf(t0,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t51,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t0]) ).
cnf(t53,plain,
upme(X1,X2,X3) = meet(X1,join(X3,X2)),
inference(cp,[status(thm)],[t31,t51]) ).
cnf(t286796,plain,
upme(X1,X2,X3) = upme(X1,X3,X2),
inference(step,[status(thm)],[t53,t31]) ).
cnf(t87,plain,
upme(X1,X2,X3) = upme(X1,X3,X2),
inference(orient,[status(thm)],[t286796]) ).
cnf(t2,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t15,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t9,axiom,
meet(join(X1,X2),join(X1,X3)) = upjo(X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t286786,plain,
upme(join(X1,X2),X1,X3) = upjo(X1,X2,X3),
inference(step,[status(thm)],[t9,t31]) ).
cnf(t38,plain,
upme(join(X1,X2),X1,X3) = upjo(X1,X2,X3),
inference(orient,[status(thm)],[t286786]) ).
cnf(t4,axiom,
join(X1,meet(X2,X3)) = lojo(X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t55,plain,
join(X1,meet(X2,X3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t4]) ).
cnf(t61,plain,
upjo(X1,meet(X2,X3),Y3) = upme(lojo(X1,X2,X3),X1,Y3),
inference(cp,[status(thm)],[t38,t55]) ).
cnf(t396,plain,
upme(lojo(X1,X2,X3),X1,Y3) = upjo(X1,meet(X2,X3),Y3),
inference(orient,[status(thm)],[t61]) ).
cnf(t8,axiom,
join(meet(X1,X2),meet(X1,X3)) = lome(X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t286795,plain,
lojo(meet(X1,X2),X1,X3) = lome(X1,X2,X3),
inference(step,[status(thm)],[t8,t55]) ).
cnf(t80,plain,
lojo(meet(X1,X2),X1,X3) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t286795]) ).
cnf(t403,plain,
upjo(meet(X1,X2),meet(X1,X3),Y3) = upme(lome(X1,X2,X3),meet(X1,X2),Y3),
inference(cp,[status(thm)],[t396,t80]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t286784,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t7,t15]) ).
cnf(t17,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t286784]) ).
cnf(t57,plain,
lojo(X1,X2,join(X3,Y3)) = join(X1,upme(X2,X3,Y3)),
inference(cp,[status(thm)],[t55,t31]) ).
cnf(t93,plain,
join(X1,upme(X2,X3,Y3)) = lojo(X1,X2,join(X3,Y3)),
inference(orient,[status(thm)],[t57]) ).
cnf(t3,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t286785,plain,
upme(X1,X1,X2) = X1,
inference(step,[status(thm)],[t11,t31]) ).
cnf(t37,plain,
upme(X1,X1,X2) = X1,
inference(rw,[status(thm)],[t286785]) ).
cnf(t85,plain,
upme(X1,X1,X2) = X1,
inference(orient,[status(thm)],[t37]) ).
cnf(t95,plain,
lojo(X1,X2,join(X2,X3)) = join(X1,X2),
inference(cp,[status(thm)],[t93,t85]) ).
cnf(t102,plain,
lojo(X1,X2,join(X2,X3)) = join(X1,X2),
inference(orient,[status(thm)],[t95]) ).
cnf(t1,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)],[t1]) ).
cnf(t286793,plain,
lojo(X1,X1,X2) = X1,
inference(step,[status(thm)],[t12,t55]) ).
cnf(t63,plain,
lojo(X1,X1,X2) = X1,
inference(rw,[status(thm)],[t286793]) ).
cnf(t86,plain,
lojo(X1,X1,X2) = X1,
inference(orient,[status(thm)],[t63]) ).
cnf(t103,plain,
join(X1,X1) = X1,
inference(cp,[status(thm)],[t102,t86]) ).
cnf(t110,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t103]) ).
cnf(t117,plain,
upme(X1,X2,X2) = meet(X1,X2),
inference(cp,[status(thm)],[t31,t110]) ).
cnf(t124,plain,
upme(X1,X2,X2) = meet(X1,X2),
inference(orient,[status(thm)],[t117]) ).
cnf(t125,plain,
meet(X1,X1) = X1,
inference(cp,[status(thm)],[t124,t85]) ).
cnf(t127,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t125]) ).
cnf(t132,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(cp,[status(thm)],[t17,t127]) ).
cnf(t286803,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t132,t15]) ).
cnf(t148,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t286803]) ).
cnf(t151,plain,
meet(X1,join(X2,X3)) = meet(X1,upme(X1,X2,X3)),
inference(cp,[status(thm)],[t148,t31]) ).
cnf(t286814,plain,
upme(X1,X2,X3) = meet(X1,upme(X1,X2,X3)),
inference(step,[status(thm)],[t151,t31]) ).
cnf(t189,plain,
meet(X1,upme(X1,X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t286814]) ).
cnf(t190,plain,
upme(join(X1,X2),X1,X3) = meet(join(X1,X2),upjo(X1,X2,X3)),
inference(cp,[status(thm)],[t189,t38]) ).
cnf(t286948,plain,
upjo(X1,X2,X3) = meet(join(X1,X2),upjo(X1,X2,X3)),
inference(step,[status(thm)],[t190,t38]) ).
cnf(t1481,plain,
meet(join(X1,X2),upjo(X1,X2,X3)) = upjo(X1,X2,X3),
inference(orient,[status(thm)],[t286948]) ).
cnf(t62,plain,
upme(X1,X2,meet(X3,Y3)) = meet(X1,lojo(X2,X3,Y3)),
inference(cp,[status(thm)],[t31,t55]) ).
cnf(t253,plain,
meet(X1,lojo(X2,X3,Y3)) = upme(X1,X2,meet(X3,Y3)),
inference(orient,[status(thm)],[t62]) ).
cnf(t256,plain,
upme(X1,X2,meet(X2,X3)) = meet(X1,X2),
inference(cp,[status(thm)],[t253,t86]) ).
cnf(t265,plain,
upme(X1,X2,meet(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t256]) ).
cnf(t266,plain,
meet(join(X1,X2),X1) = upjo(X1,X2,meet(X1,X3)),
inference(cp,[status(thm)],[t265,t38]) ).
cnf(t286824,plain,
meet(X1,join(X1,X2)) = upjo(X1,X2,meet(X1,X3)),
inference(step,[status(thm)],[t266,t15]) ).
cnf(t286825,plain,
upme(X1,X1,X2) = upjo(X1,X2,meet(X1,X3)),
inference(step,[status(thm)],[t286824,t31]) ).
cnf(t286826,plain,
X1 = upjo(X1,X2,meet(X1,X3)),
inference(step,[status(thm)],[t286825,t85]) ).
cnf(t273,plain,
upjo(X1,X2,meet(X1,X3)) = X1,
inference(orient,[status(thm)],[t286826]) ).
cnf(t275,plain,
X1 = upjo(X1,X2,upme(X1,X3,Y3)),
inference(cp,[status(thm)],[t273,t189]) ).
cnf(t280,plain,
upjo(X1,X2,upme(X1,X3,Y3)) = X1,
inference(orient,[status(thm)],[t275]) ).
cnf(t281,plain,
join(X1,X2) = upjo(join(X1,X2),X3,upjo(X1,X2,Y3)),
inference(cp,[status(thm)],[t280,t38]) ).
cnf(t2432,plain,
upjo(join(X1,X2),X3,upjo(X1,X2,Y3)) = join(X1,X2),
inference(orient,[status(thm)],[t281]) ).
cnf(t2466,plain,
upjo(join(X1,X2),X3,upjo(X1,X2,Y3)) = meet(join(join(X1,X2),X3),join(X1,X2)),
inference(cp,[status(thm)],[t1481,t2432]) ).
cnf(t287017,plain,
join(X1,X2) = meet(join(join(X1,X2),X3),join(X1,X2)),
inference(step,[status(thm)],[t2466,t2432]) ).
cnf(t287018,plain,
join(X1,X2) = upme(join(join(X1,X2),X3),X1,X2),
inference(step,[status(thm)],[t287017,t31]) ).
cnf(t287019,plain,
join(X1,X2) = upme(join(X3,join(X1,X2)),X1,X2),
inference(step,[status(thm)],[t287018,t51]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t286794,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t6,t51]) ).
cnf(t64,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t286794]) ).
cnf(t287020,plain,
join(X1,X2) = upme(join(X2,join(X3,X1)),X1,X2),
inference(step,[status(thm)],[t287019,t64]) ).
cnf(t287021,plain,
join(X1,X2) = upme(join(X1,join(X2,X3)),X1,X2),
inference(step,[status(thm)],[t287020,t64]) ).
cnf(t287022,plain,
join(X1,X2) = upjo(X1,join(X2,X3),X2),
inference(step,[status(thm)],[t287021,t38]) ).
cnf(t2640,plain,
upjo(X1,join(X2,X3),X2) = join(X1,X2),
inference(orient,[status(thm)],[t287022]) ).
cnf(t118,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(cp,[status(thm)],[t64,t110]) ).
cnf(t286802,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t118,t51]) ).
cnf(t136,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t286802]) ).
cnf(t139,plain,
join(X1,meet(X2,X3)) = join(X1,lojo(X1,X2,X3)),
inference(cp,[status(thm)],[t136,t55]) ).
cnf(t286810,plain,
lojo(X1,X2,X3) = join(X1,lojo(X1,X2,X3)),
inference(step,[status(thm)],[t139,t55]) ).
cnf(t161,plain,
join(X1,lojo(X1,X2,X3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t286810]) ).
cnf(t162,plain,
lojo(meet(X1,X2),X1,X3) = join(meet(X1,X2),lome(X1,X2,X3)),
inference(cp,[status(thm)],[t161,t80]) ).
cnf(t286941,plain,
lome(X1,X2,X3) = join(meet(X1,X2),lome(X1,X2,X3)),
inference(step,[status(thm)],[t162,t80]) ).
cnf(t1440,plain,
join(meet(X1,X2),lome(X1,X2,X3)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t286941]) ).
cnf(t2657,plain,
join(X1,meet(X2,X3)) = upjo(X1,lome(X2,X3,Y3),meet(X2,X3)),
inference(cp,[status(thm)],[t2640,t1440]) ).
cnf(t287752,plain,
lojo(X1,X2,X3) = upjo(X1,lome(X2,X3,Y3),meet(X2,X3)),
inference(step,[status(thm)],[t2657,t55]) ).
cnf(t40997,plain,
upjo(X1,lome(X2,X3,Y3),meet(X2,X3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t287752]) ).
cnf(t116,plain,
join(X1,X2) = lojo(X1,X2,X2),
inference(cp,[status(thm)],[t102,t110]) ).
cnf(t122,plain,
lojo(X1,X2,X2) = join(X1,X2),
inference(orient,[status(thm)],[t116]) ).
cnf(t123,plain,
join(meet(X1,X2),X1) = lome(X1,X2,X1),
inference(cp,[status(thm)],[t122,t80]) ).
cnf(t286804,plain,
join(X1,meet(X1,X2)) = lome(X1,X2,X1),
inference(step,[status(thm)],[t123,t51]) ).
cnf(t286805,plain,
lojo(X1,X1,X2) = lome(X1,X2,X1),
inference(step,[status(thm)],[t286804,t55]) ).
cnf(t286806,plain,
X1 = lome(X1,X2,X1),
inference(step,[status(thm)],[t286805,t86]) ).
cnf(t159,plain,
lome(X1,X2,X1) = X1,
inference(orient,[status(thm)],[t286806]) ).
cnf(t41009,plain,
lojo(X1,X2,X3) = upjo(X1,X2,meet(X2,X3)),
inference(cp,[status(thm)],[t40997,t159]) ).
cnf(t41195,plain,
upjo(X1,X2,meet(X2,X3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t41009]) ).
cnf(t144,plain,
upjo(X1,join(X1,X2),X3) = upme(join(X1,X2),X1,X3),
inference(cp,[status(thm)],[t38,t136]) ).
cnf(t286811,plain,
upjo(X1,join(X1,X2),X3) = upjo(X1,X2,X3),
inference(step,[status(thm)],[t144,t38]) ).
cnf(t169,plain,
upjo(X1,join(X1,X2),X3) = upjo(X1,X2,X3),
inference(orient,[status(thm)],[t286811]) ).
cnf(t41210,plain,
lojo(X1,join(X1,X2),X3) = upjo(X1,X2,meet(join(X1,X2),X3)),
inference(cp,[status(thm)],[t41195,t169]) ).
cnf(t58,plain,
lojo(X1,X2,X3) = join(X1,meet(X3,X2)),
inference(cp,[status(thm)],[t55,t15]) ).
cnf(t286797,plain,
lojo(X1,X2,X3) = lojo(X1,X3,X2),
inference(step,[status(thm)],[t58,t55]) ).
cnf(t90,plain,
lojo(X1,X2,X3) = lojo(X1,X3,X2),
inference(orient,[status(thm)],[t286797]) ).
cnf(t287831,plain,
lojo(X1,X3,join(X1,X2)) = upjo(X1,X2,meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t41210,t90]) ).
cnf(t287832,plain,
lojo(X1,X3,join(X1,X2)) = upjo(X1,X2,meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t287831,t15]) ).
cnf(t287833,plain,
lojo(X1,X3,join(X1,X2)) = upjo(X1,X2,upme(X3,X1,X2)),
inference(step,[status(thm)],[t287832,t31]) ).
cnf(t51718,plain,
upjo(X1,X2,upme(X3,X1,X2)) = lojo(X1,X3,join(X1,X2)),
inference(orient,[status(thm)],[t287833]) ).
cnf(t104,plain,
join(meet(X1,X2),X1) = lome(X1,X2,join(X1,X3)),
inference(cp,[status(thm)],[t102,t80]) ).
cnf(t286820,plain,
join(X1,meet(X1,X2)) = lome(X1,X2,join(X1,X3)),
inference(step,[status(thm)],[t104,t51]) ).
cnf(t286821,plain,
lojo(X1,X1,X2) = lome(X1,X2,join(X1,X3)),
inference(step,[status(thm)],[t286820,t55]) ).
cnf(t286822,plain,
X1 = lome(X1,X2,join(X1,X3)),
inference(step,[status(thm)],[t286821,t86]) ).
cnf(t224,plain,
lome(X1,X2,join(X1,X3)) = X1,
inference(orient,[status(thm)],[t286822]) ).
cnf(t225,plain,
X1 = lome(X1,X2,lojo(X1,X3,Y3)),
inference(cp,[status(thm)],[t224,t161]) ).
cnf(t231,plain,
lome(X1,X2,lojo(X1,X3,Y3)) = X1,
inference(orient,[status(thm)],[t225]) ).
cnf(t233,plain,
meet(X1,X2) = lome(meet(X1,X2),X3,lome(X1,X2,Y3)),
inference(cp,[status(thm)],[t231,t80]) ).
cnf(t1853,plain,
lome(meet(X1,X2),X3,lome(X1,X2,Y3)) = meet(X1,X2),
inference(orient,[status(thm)],[t233]) ).
cnf(t1890,plain,
lome(meet(X1,X2),X3,lome(X1,X2,Y3)) = join(meet(meet(X1,X2),X3),meet(X1,X2)),
inference(cp,[status(thm)],[t1440,t1853]) ).
cnf(t286985,plain,
meet(X1,X2) = join(meet(meet(X1,X2),X3),meet(X1,X2)),
inference(step,[status(thm)],[t1890,t1853]) ).
cnf(t286986,plain,
meet(X1,X2) = lojo(meet(meet(X1,X2),X3),X1,X2),
inference(step,[status(thm)],[t286985,t55]) ).
cnf(t286987,plain,
meet(X1,X2) = lojo(meet(X3,meet(X1,X2)),X1,X2),
inference(step,[status(thm)],[t286986,t15]) ).
cnf(t286988,plain,
meet(X1,X2) = lojo(meet(X2,meet(X3,X1)),X1,X2),
inference(step,[status(thm)],[t286987,t17]) ).
cnf(t286989,plain,
meet(X1,X2) = lojo(meet(X1,meet(X2,X3)),X1,X2),
inference(step,[status(thm)],[t286988,t17]) ).
cnf(t286990,plain,
meet(X1,X2) = lome(X1,meet(X2,X3),X2),
inference(step,[status(thm)],[t286989,t80]) ).
cnf(t2020,plain,
lome(X1,meet(X2,X3),X2) = meet(X1,X2),
inference(orient,[status(thm)],[t286990]) ).
cnf(t2039,plain,
meet(X1,join(X2,X3)) = lome(X1,upjo(X2,X3,Y3),join(X2,X3)),
inference(cp,[status(thm)],[t2020,t1481]) ).
cnf(t287575,plain,
upme(X1,X2,X3) = lome(X1,upjo(X2,X3,Y3),join(X2,X3)),
inference(step,[status(thm)],[t2039,t31]) ).
cnf(t28084,plain,
lome(X1,upjo(X2,X3,Y3),join(X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t287575]) ).
cnf(t126,plain,
meet(join(X1,X2),X1) = upjo(X1,X2,X1),
inference(cp,[status(thm)],[t124,t38]) ).
cnf(t286807,plain,
meet(X1,join(X1,X2)) = upjo(X1,X2,X1),
inference(step,[status(thm)],[t126,t15]) ).
cnf(t286808,plain,
upme(X1,X1,X2) = upjo(X1,X2,X1),
inference(step,[status(thm)],[t286807,t31]) ).
cnf(t286809,plain,
X1 = upjo(X1,X2,X1),
inference(step,[status(thm)],[t286808,t85]) ).
cnf(t160,plain,
upjo(X1,X2,X1) = X1,
inference(orient,[status(thm)],[t286809]) ).
cnf(t28094,plain,
upme(X1,X2,X3) = lome(X1,X2,join(X2,X3)),
inference(cp,[status(thm)],[t28084,t160]) ).
cnf(t28224,plain,
lome(X1,X2,join(X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t28094]) ).
cnf(t155,plain,
lome(X1,meet(X1,X2),X3) = lojo(meet(X1,X2),X1,X3),
inference(cp,[status(thm)],[t80,t148]) ).
cnf(t286815,plain,
lome(X1,meet(X1,X2),X3) = lome(X1,X2,X3),
inference(step,[status(thm)],[t155,t80]) ).
cnf(t196,plain,
lome(X1,meet(X1,X2),X3) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t286815]) ).
cnf(t35,plain,
meet(X1,meet(join(X2,X3),Y3)) = meet(Y3,upme(X1,X2,X3)),
inference(cp,[status(thm)],[t17,t31]) ).
cnf(t286827,plain,
meet(X1,meet(Y3,join(X2,X3))) = meet(Y3,upme(X1,X2,X3)),
inference(step,[status(thm)],[t35,t15]) ).
cnf(t286828,plain,
meet(X1,upme(Y3,X2,X3)) = meet(Y3,upme(X1,X2,X3)),
inference(step,[status(thm)],[t286827,t31]) ).
cnf(t285,plain,
meet(X1,upme(X2,X3,Y3)) = meet(X2,upme(X1,X3,Y3)),
inference(orient,[status(thm)],[t286828]) ).
cnf(t292,plain,
meet(X1,upme(X2,X1,X3)) = meet(X2,X1),
inference(cp,[status(thm)],[t285,t85]) ).
cnf(t286833,plain,
meet(X1,upme(X2,X1,X3)) = meet(X1,X2),
inference(step,[status(thm)],[t292,t15]) ).
cnf(t328,plain,
meet(X1,upme(X2,X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t286833]) ).
cnf(t334,plain,
meet(X1,join(X1,X2)) = meet(X1,upjo(X1,X2,X3)),
inference(cp,[status(thm)],[t328,t38]) ).
cnf(t286834,plain,
upme(X1,X1,X2) = meet(X1,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t334,t31]) ).
cnf(t286835,plain,
X1 = meet(X1,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t286834,t85]) ).
cnf(t343,plain,
meet(X1,upjo(X1,X2,X3)) = X1,
inference(orient,[status(thm)],[t286835]) ).
cnf(t346,plain,
lome(X1,upjo(X1,X2,X3),Y3) = lome(X1,X1,Y3),
inference(cp,[status(thm)],[t196,t343]) ).
cnf(t131,plain,
lome(X1,X1,X2) = lojo(X1,X1,X2),
inference(cp,[status(thm)],[t80,t127]) ).
cnf(t286800,plain,
lome(X1,X1,X2) = X1,
inference(step,[status(thm)],[t131,t86]) ).
cnf(t134,plain,
lome(X1,X1,X2) = X1,
inference(orient,[status(thm)],[t286800]) ).
cnf(t286837,plain,
lome(X1,upjo(X1,X2,X3),Y3) = X1,
inference(step,[status(thm)],[t346,t134]) ).
cnf(t352,plain,
lome(X1,upjo(X1,X2,X3),Y3) = X1,
inference(orient,[status(thm)],[t286837]) ).
cnf(t28232,plain,
upme(X1,upjo(X1,X2,X3),Y3) = X1,
inference(cp,[status(thm)],[t28224,t352]) ).
cnf(t287576,plain,
upme(X1,Y3,upjo(X1,X2,X3)) = X1,
inference(step,[status(thm)],[t28232,t87]) ).
cnf(t28306,plain,
upme(X1,X2,upjo(X1,X3,Y3)) = X1,
inference(orient,[status(thm)],[t287576]) ).
cnf(t51753,plain,
lojo(X1,X2,join(X1,upjo(X2,X3,Y3))) = upjo(X1,upjo(X2,X3,Y3),X2),
inference(cp,[status(thm)],[t51718,t28306]) ).
cnf(t193,plain,
lojo(X1,X2,upme(X2,X3,Y3)) = join(X1,upme(X2,X3,Y3)),
inference(cp,[status(thm)],[t55,t189]) ).
cnf(t286861,plain,
lojo(X1,X2,upme(X2,X3,Y3)) = lojo(X1,X2,join(X3,Y3)),
inference(step,[status(thm)],[t193,t93]) ).
cnf(t558,plain,
lojo(X1,X2,upme(X2,X3,Y3)) = lojo(X1,X2,join(X3,Y3)),
inference(orient,[status(thm)],[t286861]) ).
cnf(t28397,plain,
lojo(X1,X2,join(X3,upjo(X2,Y3,Y4))) = lojo(X1,X2,X2),
inference(cp,[status(thm)],[t558,t28306]) ).
cnf(t287598,plain,
lojo(X1,X2,join(X3,upjo(X2,Y3,Y4))) = join(X1,X2),
inference(step,[status(thm)],[t28397,t122]) ).
cnf(t30788,plain,
lojo(X1,X2,join(X3,upjo(X2,Y3,Y4))) = join(X1,X2),
inference(orient,[status(thm)],[t287598]) ).
cnf(t287838,plain,
join(X1,X2) = upjo(X1,upjo(X2,X3,Y3),X2),
inference(step,[status(thm)],[t51753,t30788]) ).
cnf(t51942,plain,
upjo(X1,upjo(X2,X3,Y3),X2) = join(X1,X2),
inference(orient,[status(thm)],[t287838]) ).
cnf(t115,plain,
upjo(X1,X1,X2) = upme(X1,X1,X2),
inference(cp,[status(thm)],[t38,t110]) ).
cnf(t286798,plain,
upjo(X1,X1,X2) = X1,
inference(step,[status(thm)],[t115,t85]) ).
cnf(t120,plain,
upjo(X1,X1,X2) = X1,
inference(orient,[status(thm)],[t286798]) ).
cnf(t51950,plain,
join(upjo(X1,X2,X3),X1) = upjo(X1,X2,X3),
inference(cp,[status(thm)],[t51942,t120]) ).
cnf(t287839,plain,
join(X1,upjo(X1,X2,X3)) = upjo(X1,X2,X3),
inference(step,[status(thm)],[t51950,t51]) ).
cnf(t52042,plain,
join(X1,upjo(X1,X2,X3)) = upjo(X1,X2,X3),
inference(orient,[status(thm)],[t287839]) ).
cnf(t96,plain,
lojo(X1,join(X2,X3),join(X2,Y3)) = join(X1,upjo(X2,X3,Y3)),
inference(cp,[status(thm)],[t93,t38]) ).
cnf(t2514,plain,
lojo(X1,join(X2,X3),join(X2,Y3)) = join(X1,upjo(X2,X3,Y3)),
inference(orient,[status(thm)],[t96]) ).
cnf(t2530,plain,
join(X1,upjo(X2,X3,Y3)) = lojo(X1,join(X3,X2),join(X2,Y3)),
inference(cp,[status(thm)],[t2514,t51]) ).
cnf(t287392,plain,
join(X1,upjo(X2,X3,Y3)) = lojo(X1,join(X2,Y3),join(X3,X2)),
inference(step,[status(thm)],[t2530,t90]) ).
cnf(t287393,plain,
join(X1,upjo(X2,X3,Y3)) = lojo(X1,join(X2,Y3),join(X2,X3)),
inference(step,[status(thm)],[t287392,t51]) ).
cnf(t287394,plain,
join(X1,upjo(X2,X3,Y3)) = join(X1,upjo(X2,Y3,X3)),
inference(step,[status(thm)],[t287393,t2514]) ).
cnf(t18119,plain,
join(X1,upjo(X2,X3,Y3)) = join(X1,upjo(X2,Y3,X3)),
inference(orient,[status(thm)],[t287394]) ).
cnf(t52043,plain,
upjo(X1,X2,X3) = join(X1,upjo(X1,X3,X2)),
inference(cp,[status(thm)],[t52042,t18119]) ).
cnf(t287840,plain,
upjo(X1,X2,X3) = upjo(X1,X3,X2),
inference(step,[status(thm)],[t52043,t52042]) ).
cnf(t52112,plain,
upjo(X1,X2,X3) = upjo(X1,X3,X2),
inference(orient,[status(thm)],[t287840]) ).
cnf(t287969,plain,
upjo(meet(X1,X2),Y3,meet(X1,X3)) = upme(lome(X1,X2,X3),meet(X1,X2),Y3),
inference(step,[status(thm)],[t403,t52112]) ).
cnf(t287970,plain,
upjo(meet(X1,X2),Y3,meet(X1,X3)) = upme(lome(X1,X2,X3),Y3,meet(X1,X2)),
inference(step,[status(thm)],[t287969,t87]) ).
cnf(t59109,plain,
upme(lome(X1,X2,X3),Y3,meet(X1,X2)) = upjo(meet(X1,X2),Y3,meet(X1,X3)),
inference(orient,[status(thm)],[t287970]) ).
cnf(t59111,plain,
upjo(meet(X1,X2),X1,meet(X1,X3)) = meet(lome(X1,X2,X3),X1),
inference(cp,[status(thm)],[t59109,t265]) ).
cnf(t287971,plain,
lojo(meet(X1,X2),X1,X3) = meet(lome(X1,X2,X3),X1),
inference(step,[status(thm)],[t59111,t41195]) ).
cnf(t287972,plain,
lome(X1,X2,X3) = meet(lome(X1,X2,X3),X1),
inference(step,[status(thm)],[t287971,t80]) ).
cnf(t287973,plain,
lome(X1,X2,X3) = meet(X1,lome(X1,X2,X3)),
inference(step,[status(thm)],[t287972,t15]) ).
cnf(t59345,plain,
meet(X1,lome(X1,X2,X3)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t287973]) ).
cnf(t257,plain,
upme(X1,meet(X2,X3),meet(X2,Y3)) = meet(X1,lome(X2,X3,Y3)),
inference(cp,[status(thm)],[t253,t80]) ).
cnf(t5229,plain,
upme(X1,meet(X2,X3),meet(X2,Y3)) = meet(X1,lome(X2,X3,Y3)),
inference(orient,[status(thm)],[t257]) ).
cnf(t5252,plain,
meet(X1,lome(X2,X3,Y3)) = upme(X1,meet(X3,X2),meet(X2,Y3)),
inference(cp,[status(thm)],[t5229,t15]) ).
cnf(t287421,plain,
meet(X1,lome(X2,X3,Y3)) = upme(X1,meet(X2,Y3),meet(X3,X2)),
inference(step,[status(thm)],[t5252,t87]) ).
cnf(t287422,plain,
meet(X1,lome(X2,X3,Y3)) = upme(X1,meet(X2,Y3),meet(X2,X3)),
inference(step,[status(thm)],[t287421,t15]) ).
cnf(t287423,plain,
meet(X1,lome(X2,X3,Y3)) = meet(X1,lome(X2,Y3,X3)),
inference(step,[status(thm)],[t287422,t5229]) ).
cnf(t19398,plain,
meet(X1,lome(X2,X3,Y3)) = meet(X1,lome(X2,Y3,X3)),
inference(orient,[status(thm)],[t287423]) ).
cnf(t59353,plain,
lome(X1,X2,X3) = meet(X1,lome(X1,X3,X2)),
inference(cp,[status(thm)],[t59345,t19398]) ).
cnf(t287978,plain,
lome(X1,X2,X3) = lome(X1,X3,X2),
inference(step,[status(thm)],[t59353,t59345]) ).
cnf(t59453,plain,
lome(X1,X2,X3) = lome(X1,X3,X2),
inference(orient,[status(thm)],[t287978]) ).
cnf(t111,plain,
meet(X1,X2) = lojo(meet(X1,X2),X1,X2),
inference(cp,[status(thm)],[t110,t55]) ).
cnf(t286799,plain,
meet(X1,X2) = lome(X1,X2,X2),
inference(step,[status(thm)],[t111,t80]) ).
cnf(t121,plain,
lome(X1,X2,X2) = meet(X1,X2),
inference(orient,[status(thm)],[t286799]) ).
cnf(t1855,plain,
meet(X1,X2) = meet(meet(X1,X2),lome(X1,X2,X3)),
inference(cp,[status(thm)],[t1853,t121]) ).
cnf(t1970,plain,
meet(meet(X1,X2),lome(X1,X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t1855]) ).
cnf(t28302,plain,
meet(X1,X2) = meet(meet(X1,X2),upme(X1,X2,X3)),
inference(cp,[status(thm)],[t1970,t28224]) ).
cnf(t287577,plain,
meet(X1,X2) = meet(X1,upme(meet(X1,X2),X2,X3)),
inference(step,[status(thm)],[t28302,t285]) ).
cnf(t232,plain,
X1 = meet(X1,lojo(X1,X2,X3)),
inference(cp,[status(thm)],[t231,t121]) ).
cnf(t234,plain,
meet(X1,lojo(X1,X2,X3)) = X1,
inference(orient,[status(thm)],[t232]) ).
cnf(t237,plain,
lome(X1,lojo(X1,X2,X3),Y3) = lome(X1,X1,Y3),
inference(cp,[status(thm)],[t196,t234]) ).
cnf(t286823,plain,
lome(X1,lojo(X1,X2,X3),Y3) = X1,
inference(step,[status(thm)],[t237,t134]) ).
cnf(t242,plain,
lome(X1,lojo(X1,X2,X3),Y3) = X1,
inference(orient,[status(thm)],[t286823]) ).
cnf(t245,plain,
meet(X1,X2) = lome(meet(X1,X2),lome(X1,X2,X3),Y3),
inference(cp,[status(thm)],[t242,t80]) ).
cnf(t2316,plain,
lome(meet(X1,X2),lome(X1,X2,X3),Y3) = meet(X1,X2),
inference(orient,[status(thm)],[t245]) ).
cnf(t2336,plain,
meet(X1,X2) = lome(meet(X1,X2),X1,X3),
inference(cp,[status(thm)],[t2316,t159]) ).
cnf(t2363,plain,
lome(meet(X1,X2),X1,X3) = meet(X1,X2),
inference(orient,[status(thm)],[t2336]) ).
cnf(t2371,plain,
meet(X1,upme(X1,X2,X3)) = lome(upme(X1,X2,X3),X1,Y3),
inference(cp,[status(thm)],[t2363,t189]) ).
cnf(t287007,plain,
upme(X1,X2,X3) = lome(upme(X1,X2,X3),X1,Y3),
inference(step,[status(thm)],[t2371,t189]) ).
cnf(t2406,plain,
lome(upme(X1,X2,X3),X1,Y3) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t287007]) ).
cnf(t2411,plain,
upme(meet(X1,X2),X3,Y3) = meet(upme(meet(X1,X2),X3,Y3),X1),
inference(cp,[status(thm)],[t2406,t2020]) ).
cnf(t287387,plain,
upme(meet(X1,X2),X3,Y3) = meet(X1,upme(meet(X1,X2),X3,Y3)),
inference(step,[status(thm)],[t2411,t15]) ).
cnf(t17392,plain,
meet(X1,upme(meet(X1,X2),X3,Y3)) = upme(meet(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t287387]) ).
cnf(t287578,plain,
meet(X1,X2) = upme(meet(X1,X2),X2,X3),
inference(step,[status(thm)],[t287577,t17392]) ).
cnf(t28408,plain,
upme(meet(X1,X2),X2,X3) = meet(X1,X2),
inference(orient,[status(thm)],[t287578]) ).
cnf(t28462,plain,
lojo(X1,meet(X2,X3),join(X3,Y3)) = lojo(X1,meet(X2,X3),meet(X2,X3)),
inference(cp,[status(thm)],[t558,t28408]) ).
cnf(t287592,plain,
lojo(X1,meet(X2,X3),join(X3,Y3)) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t28462,t122]) ).
cnf(t287593,plain,
lojo(X1,meet(X2,X3),join(X3,Y3)) = lojo(X1,X2,X3),
inference(step,[status(thm)],[t287592,t55]) ).
cnf(t29733,plain,
lojo(X1,meet(X2,X3),join(X3,Y3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t287593]) ).
cnf(t59398,plain,
lojo(X1,X2,lome(X2,X3,Y3)) = lojo(X1,lome(X2,X3,Y3),join(lome(X2,X3,Y3),Y4)),
inference(cp,[status(thm)],[t29733,t59345]) ).
cnf(t288003,plain,
lojo(X1,X2,lome(X2,X3,Y3)) = join(X1,lome(X2,X3,Y3)),
inference(step,[status(thm)],[t59398,t102]) ).
cnf(t60655,plain,
lojo(X1,X2,lome(X2,X3,Y3)) = join(X1,lome(X2,X3,Y3)),
inference(orient,[status(thm)],[t288003]) ).
cnf(t75,plain,
join(X1,join(meet(X2,X3),Y3)) = join(Y3,lojo(X1,X2,X3)),
inference(cp,[status(thm)],[t64,t55]) ).
cnf(t286846,plain,
join(X1,join(Y3,meet(X2,X3))) = join(Y3,lojo(X1,X2,X3)),
inference(step,[status(thm)],[t75,t51]) ).
cnf(t286847,plain,
join(X1,lojo(Y3,X2,X3)) = join(Y3,lojo(X1,X2,X3)),
inference(step,[status(thm)],[t286846,t55]) ).
cnf(t424,plain,
join(X1,lojo(X2,X3,Y3)) = join(X2,lojo(X1,X3,Y3)),
inference(orient,[status(thm)],[t286847]) ).
cnf(t433,plain,
join(X1,lojo(X2,X1,X3)) = join(X2,X1),
inference(cp,[status(thm)],[t424,t86]) ).
cnf(t286848,plain,
join(X1,lojo(X2,X1,X3)) = join(X1,X2),
inference(step,[status(thm)],[t433,t51]) ).
cnf(t447,plain,
join(X1,lojo(X2,X1,X3)) = join(X1,X2),
inference(orient,[status(thm)],[t286848]) ).
cnf(t453,plain,
join(X1,meet(X1,X2)) = join(X1,lome(X1,X2,X3)),
inference(cp,[status(thm)],[t447,t80]) ).
cnf(t286849,plain,
lojo(X1,X1,X2) = join(X1,lome(X1,X2,X3)),
inference(step,[status(thm)],[t453,t55]) ).
cnf(t286850,plain,
X1 = join(X1,lome(X1,X2,X3)),
inference(step,[status(thm)],[t286849,t86]) ).
cnf(t462,plain,
join(X1,lome(X1,X2,X3)) = X1,
inference(orient,[status(thm)],[t286850]) ).
cnf(t463,plain,
upjo(X1,lome(X1,X2,X3),Y3) = upme(X1,X1,Y3),
inference(cp,[status(thm)],[t38,t462]) ).
cnf(t286851,plain,
upjo(X1,lome(X1,X2,X3),Y3) = X1,
inference(step,[status(thm)],[t463,t85]) ).
cnf(t470,plain,
upjo(X1,lome(X1,X2,X3),Y3) = X1,
inference(orient,[status(thm)],[t286851]) ).
cnf(t41204,plain,
lojo(X1,lome(X1,X2,X3),Y3) = X1,
inference(cp,[status(thm)],[t41195,t470]) ).
cnf(t287753,plain,
lojo(X1,Y3,lome(X1,X2,X3)) = X1,
inference(step,[status(thm)],[t41204,t90]) ).
cnf(t41310,plain,
lojo(X1,X2,lome(X1,X3,Y3)) = X1,
inference(orient,[status(thm)],[t287753]) ).
cnf(t41451,plain,
join(X1,lojo(X2,X3,lome(X1,Y3,Y4))) = join(X2,X1),
inference(cp,[status(thm)],[t424,t41310]) ).
cnf(t287784,plain,
join(X1,lojo(X2,X3,lome(X1,Y3,Y4))) = join(X1,X2),
inference(step,[status(thm)],[t41451,t51]) ).
cnf(t46243,plain,
join(X1,lojo(X2,X3,lome(X1,Y3,Y4))) = join(X1,X2),
inference(orient,[status(thm)],[t287784]) ).
cnf(t105,plain,
join(X1,X2) = lojo(X1,X2,lojo(X2,X3,Y3)),
inference(cp,[status(thm)],[t102,t55]) ).
cnf(t250,plain,
lojo(X1,X2,lojo(X2,X3,Y3)) = join(X1,X2),
inference(orient,[status(thm)],[t105]) ).
cnf(t252,plain,
join(X1,meet(X2,X3)) = lojo(X1,meet(X2,X3),lome(X2,X3,Y3)),
inference(cp,[status(thm)],[t250,t80]) ).
cnf(t287064,plain,
lojo(X1,X2,X3) = lojo(X1,meet(X2,X3),lome(X2,X3,Y3)),
inference(step,[status(thm)],[t252,t55]) ).
cnf(t3710,plain,
lojo(X1,meet(X2,X3),lome(X2,X3,Y3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t287064]) ).
cnf(t81,plain,
lome(X1,join(X2,X3),Y3) = lojo(upme(X1,X2,X3),X1,Y3),
inference(cp,[status(thm)],[t80,t31]) ).
cnf(t528,plain,
lojo(upme(X1,X2,X3),X1,Y3) = lome(X1,join(X2,X3),Y3),
inference(orient,[status(thm)],[t81]) ).
cnf(t3712,plain,
lojo(upme(meet(X1,X2),X3,Y3),X1,X2) = lome(meet(X1,X2),join(X3,Y3),lome(X1,X2,Y4)),
inference(cp,[status(thm)],[t3710,t528]) ).
cnf(t287186,plain,
lojo(upme(meet(X1,X2),X3,Y3),X1,X2) = meet(X1,X2),
inference(step,[status(thm)],[t3712,t1853]) ).
cnf(t6265,plain,
lojo(upme(meet(X1,X2),X3,Y3),X1,X2) = meet(X1,X2),
inference(orient,[status(thm)],[t287186]) ).
cnf(t10,axiom,
meet(join(meet(meet(a,X1),X2),X3),join(meet(meet(a,X1),X3),X2)) = join(upme(meet(a,X1),X2,X3),meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t286787,plain,
upme(join(meet(meet(a,X1),X2),X3),meet(meet(a,X1),X3),X2) = join(upme(meet(a,X1),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t10,t31]) ).
cnf(t286788,plain,
upme(join(meet(X2,meet(a,X1)),X3),meet(meet(a,X1),X3),X2) = join(upme(meet(a,X1),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t286787,t15]) ).
cnf(t286789,plain,
upme(join(meet(X1,meet(X2,a)),X3),meet(meet(a,X1),X3),X2) = join(upme(meet(a,X1),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t286788,t17]) ).
cnf(t286790,plain,
upme(join(meet(X1,meet(X2,a)),X3),meet(X3,meet(a,X1)),X2) = join(upme(meet(a,X1),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t286789,t15]) ).
cnf(t286791,plain,
upme(join(meet(X1,meet(X2,a)),X3),meet(X1,meet(X3,a)),X2) = join(upme(meet(a,X1),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t286790,t17]) ).
cnf(t286792,plain,
upme(join(meet(X1,meet(X2,a)),X3),meet(X1,meet(X3,a)),X2) = join(upme(meet(X1,a),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t286791,t15]) ).
cnf(t40,plain,
upme(join(meet(X1,meet(X2,a)),X3),meet(X1,meet(X3,a)),X2) = join(upme(meet(X1,a),X2,X3),meet(X2,X3)),
inference(orient,[status(thm)],[t286792]) ).
cnf(t54,plain,
upme(join(meet(X1,meet(X2,a)),X3),meet(X1,meet(X3,a)),X2) = join(upme(meet(X1,a),X2,X3),meet(X2,X3)),
inference(rw,[status(thm)],[t40]) ).
cnf(t286829,plain,
upme(join(meet(X1,meet(X2,a)),X3),X2,meet(X1,meet(X3,a))) = join(upme(meet(X1,a),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t54,t87]) ).
cnf(t286830,plain,
upme(join(X3,meet(X1,meet(X2,a))),X2,meet(X1,meet(X3,a))) = join(upme(meet(X1,a),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t286829,t51]) ).
cnf(t286831,plain,
upme(lojo(X3,X1,meet(X2,a)),X2,meet(X1,meet(X3,a))) = join(upme(meet(X1,a),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t286830,t55]) ).
cnf(t286832,plain,
upme(lojo(X3,X1,meet(X2,a)),X2,meet(X1,meet(X3,a))) = lojo(upme(meet(X1,a),X2,X3),X2,X3),
inference(step,[status(thm)],[t286831,t55]) ).
cnf(t305,plain,
upme(lojo(X1,X2,meet(X3,a)),X3,meet(X2,meet(X1,a))) = lojo(upme(meet(X2,a),X3,X1),X3,X1),
inference(orient,[status(thm)],[t286832]) ).
cnf(t306,plain,
lojo(upme(meet(X1,a),X1,X2),X1,X2) = meet(lojo(X2,X1,meet(X1,a)),X1),
inference(cp,[status(thm)],[t305,t265]) ).
cnf(t156,plain,
lojo(X1,X2,meet(X2,X3)) = join(X1,meet(X2,X3)),
inference(cp,[status(thm)],[t55,t148]) ).
cnf(t286817,plain,
lojo(X1,X2,meet(X2,X3)) = lojo(X1,X2,X3),
inference(step,[status(thm)],[t156,t55]) ).
cnf(t207,plain,
lojo(X1,X2,meet(X2,X3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t286817]) ).
cnf(t208,plain,
lojo(meet(X1,X2),X1,X3) = lome(X1,X2,meet(X1,X3)),
inference(cp,[status(thm)],[t207,t80]) ).
cnf(t286819,plain,
lome(X1,X2,X3) = lome(X1,X2,meet(X1,X3)),
inference(step,[status(thm)],[t208,t80]) ).
cnf(t219,plain,
lome(X1,X2,meet(X1,X3)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t286819]) ).
cnf(t220,plain,
lome(X1,X2,join(X3,Y3)) = lome(X1,X2,upme(X1,X3,Y3)),
inference(cp,[status(thm)],[t219,t31]) ).
cnf(t576,plain,
lome(X1,X2,upme(X1,X3,Y3)) = lome(X1,X2,join(X3,Y3)),
inference(orient,[status(thm)],[t220]) ).
cnf(t338,plain,
lome(X1,upme(X2,X1,X3),Y3) = lome(X1,meet(X1,X2),Y3),
inference(cp,[status(thm)],[t196,t328]) ).
cnf(t286842,plain,
lome(X1,upme(X2,X1,X3),Y3) = lome(X1,X2,Y3),
inference(step,[status(thm)],[t338,t196]) ).
cnf(t376,plain,
lome(X1,upme(X2,X1,X3),Y3) = lome(X1,X2,Y3),
inference(orient,[status(thm)],[t286842]) ).
cnf(t268,plain,
meet(X1,X2) = upme(X1,X2,upme(X2,X3,Y3)),
inference(cp,[status(thm)],[t265,t189]) ).
cnf(t282,plain,
upme(X1,X2,upme(X2,X3,Y3)) = meet(X1,X2),
inference(orient,[status(thm)],[t268]) ).
cnf(t284,plain,
meet(X1,join(X2,X3)) = upme(X1,join(X2,X3),upjo(X2,X3,Y3)),
inference(cp,[status(thm)],[t282,t38]) ).
cnf(t287201,plain,
upme(X1,X2,X3) = upme(X1,join(X2,X3),upjo(X2,X3,Y3)),
inference(step,[status(thm)],[t284,t31]) ).
cnf(t7152,plain,
upme(X1,join(X2,X3),upjo(X2,X3,Y3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t287201]) ).
cnf(t7153,plain,
upme(lojo(join(X1,X2),X3,Y3),X1,X2) = upjo(join(X1,X2),meet(X3,Y3),upjo(X1,X2,Y4)),
inference(cp,[status(thm)],[t7152,t396]) ).
cnf(t287247,plain,
upme(lojo(join(X1,X2),X3,Y3),X1,X2) = join(X1,X2),
inference(step,[status(thm)],[t7153,t2432]) ).
cnf(t8657,plain,
upme(lojo(join(X1,X2),X3,Y3),X1,X2) = join(X1,X2),
inference(orient,[status(thm)],[t287247]) ).
cnf(t8717,plain,
lome(X1,lojo(join(X1,X2),X3,Y3),Y4) = lome(X1,join(X1,X2),Y4),
inference(cp,[status(thm)],[t376,t8657]) ).
cnf(t243,plain,
X1 = lome(X1,join(X1,X2),X3),
inference(cp,[status(thm)],[t242,t122]) ).
cnf(t246,plain,
lome(X1,join(X1,X2),X3) = X1,
inference(orient,[status(thm)],[t243]) ).
cnf(t287249,plain,
lome(X1,lojo(join(X1,X2),X3,Y3),Y4) = X1,
inference(step,[status(thm)],[t8717,t246]) ).
cnf(t8754,plain,
lome(X1,lojo(join(X1,X2),X3,Y3),Y4) = X1,
inference(orient,[status(thm)],[t287249]) ).
cnf(t337,plain,
lojo(X1,X2,upme(X3,X2,Y3)) = lojo(X1,X2,meet(X2,X3)),
inference(cp,[status(thm)],[t207,t328]) ).
cnf(t286841,plain,
lojo(X1,X2,upme(X3,X2,Y3)) = lojo(X1,X2,X3),
inference(step,[status(thm)],[t337,t207]) ).
cnf(t370,plain,
lojo(X1,X2,upme(X3,X2,Y3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t286841]) ).
cnf(t166,plain,
upme(X1,X2,lojo(X2,X3,Y3)) = meet(X1,lojo(X2,X3,Y3)),
inference(cp,[status(thm)],[t31,t161]) ).
cnf(t286860,plain,
upme(X1,X2,lojo(X2,X3,Y3)) = upme(X1,X2,meet(X3,Y3)),
inference(step,[status(thm)],[t166,t253]) ).
cnf(t546,plain,
upme(X1,X2,lojo(X2,X3,Y3)) = upme(X1,X2,meet(X3,Y3)),
inference(orient,[status(thm)],[t286860]) ).
cnf(t397,plain,
upjo(X1,meet(X2,meet(X1,a)),meet(X2,meet(X1,a))) = lojo(upme(meet(X2,a),X1,X1),X1,X1),
inference(cp,[status(thm)],[t396,t305]) ).
cnf(t128,plain,
join(X1,X2) = upme(join(X1,X2),X1,X2),
inference(cp,[status(thm)],[t127,t31]) ).
cnf(t286801,plain,
join(X1,X2) = upjo(X1,X2,X2),
inference(step,[status(thm)],[t128,t38]) ).
cnf(t135,plain,
upjo(X1,X2,X2) = join(X1,X2),
inference(orient,[status(thm)],[t286801]) ).
cnf(t286862,plain,
join(X1,meet(X2,meet(X1,a))) = lojo(upme(meet(X2,a),X1,X1),X1,X1),
inference(step,[status(thm)],[t397,t135]) ).
cnf(t286863,plain,
lojo(X1,X2,meet(X1,a)) = lojo(upme(meet(X2,a),X1,X1),X1,X1),
inference(step,[status(thm)],[t286862,t55]) ).
cnf(t286864,plain,
lojo(X1,X2,meet(X1,a)) = join(upme(meet(X2,a),X1,X1),X1),
inference(step,[status(thm)],[t286863,t122]) ).
cnf(t286865,plain,
lojo(X1,X2,meet(X1,a)) = join(X1,upme(meet(X2,a),X1,X1)),
inference(step,[status(thm)],[t286864,t51]) ).
cnf(t286866,plain,
lojo(X1,X2,meet(X1,a)) = lojo(X1,meet(X2,a),join(X1,X1)),
inference(step,[status(thm)],[t286865,t93]) ).
cnf(t286867,plain,
lojo(X1,X2,meet(X1,a)) = lojo(X1,meet(X2,a),X1),
inference(step,[status(thm)],[t286866,t110]) ).
cnf(t286868,plain,
lojo(X1,X2,meet(X1,a)) = lojo(X1,X1,meet(X2,a)),
inference(step,[status(thm)],[t286867,t90]) ).
cnf(t286869,plain,
lojo(X1,X2,meet(X1,a)) = X1,
inference(step,[status(thm)],[t286868,t86]) ).
cnf(t581,plain,
lojo(X1,X2,meet(X1,a)) = X1,
inference(orient,[status(thm)],[t286869]) ).
cnf(t585,plain,
a = lojo(a,X1,a),
inference(cp,[status(thm)],[t581,t127]) ).
cnf(t594,plain,
lojo(a,X1,a) = a,
inference(orient,[status(thm)],[t585]) ).
cnf(t597,plain,
upme(X1,a,meet(X2,a)) = upme(X1,a,a),
inference(cp,[status(thm)],[t546,t594]) ).
cnf(t286872,plain,
upme(X1,a,meet(X2,a)) = meet(X1,a),
inference(step,[status(thm)],[t597,t124]) ).
cnf(t605,plain,
upme(X1,a,meet(X2,a)) = meet(X1,a),
inference(orient,[status(thm)],[t286872]) ).
cnf(t609,plain,
lojo(X1,a,X2) = lojo(X1,a,meet(X2,a)),
inference(cp,[status(thm)],[t370,t605]) ).
cnf(t286873,plain,
lojo(X1,X2,a) = lojo(X1,a,meet(X2,a)),
inference(step,[status(thm)],[t609,t90]) ).
cnf(t615,plain,
lojo(X1,a,meet(X2,a)) = lojo(X1,X2,a),
inference(orient,[status(thm)],[t286873]) ).
cnf(t617,plain,
lojo(meet(a,X1),X2,a) = lome(a,X1,meet(X2,a)),
inference(cp,[status(thm)],[t615,t80]) ).
cnf(t286874,plain,
lojo(meet(X1,a),X2,a) = lome(a,X1,meet(X2,a)),
inference(step,[status(thm)],[t617,t15]) ).
cnf(t336,plain,
lome(X1,X2,upme(X3,X1,Y3)) = lome(X1,X2,meet(X1,X3)),
inference(cp,[status(thm)],[t219,t328]) ).
cnf(t286839,plain,
lome(X1,X2,upme(X3,X1,Y3)) = lome(X1,X2,X3),
inference(step,[status(thm)],[t336,t219]) ).
cnf(t355,plain,
lome(X1,X2,upme(X3,X1,Y3)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t286839]) ).
cnf(t610,plain,
lome(a,X1,X2) = lome(a,X1,meet(X2,a)),
inference(cp,[status(thm)],[t355,t605]) ).
cnf(t630,plain,
lome(a,X1,meet(X2,a)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t610]) ).
cnf(t286875,plain,
lojo(meet(X1,a),X2,a) = lome(a,X1,X2),
inference(step,[status(thm)],[t286874,t630]) ).
cnf(t632,plain,
lojo(meet(X1,a),X2,a) = lome(a,X1,X2),
inference(orient,[status(thm)],[t286875]) ).
cnf(t644,plain,
join(X1,meet(X2,a)) = join(X1,lome(a,X2,X1)),
inference(cp,[status(thm)],[t447,t632]) ).
cnf(t286876,plain,
lojo(X1,X2,a) = join(X1,lome(a,X2,X1)),
inference(step,[status(thm)],[t644,t55]) ).
cnf(t652,plain,
join(X1,lome(a,X2,X1)) = lojo(X1,X2,a),
inference(orient,[status(thm)],[t286876]) ).
cnf(t4558,plain,
join(X1,lome(a,X2,X1)) = lojo(X1,X2,a),
inference(rw,[status(thm)],[t652]) ).
cnf(t650,plain,
lojo(meet(X1,a),X2,a) = join(meet(X1,a),lome(a,X1,X2)),
inference(cp,[status(thm)],[t161,t632]) ).
cnf(t286955,plain,
lome(a,X1,X2) = join(meet(X1,a),lome(a,X1,X2)),
inference(step,[status(thm)],[t650,t632]) ).
cnf(t1523,plain,
join(meet(X1,a),lome(a,X1,X2)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t286955]) ).
cnf(t145,plain,
upme(X1,X2,join(X2,X3)) = meet(X1,join(X2,X3)),
inference(cp,[status(thm)],[t31,t136]) ).
cnf(t286813,plain,
upme(X1,X2,join(X2,X3)) = upme(X1,X2,X3),
inference(step,[status(thm)],[t145,t31]) ).
cnf(t182,plain,
upme(X1,X2,join(X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t286813]) ).
cnf(t457,plain,
upme(X1,X2,lojo(X3,X2,Y3)) = upme(X1,X2,join(X2,X3)),
inference(cp,[status(thm)],[t182,t447]) ).
cnf(t286857,plain,
upme(X1,X2,lojo(X3,X2,Y3)) = upme(X1,X2,X3),
inference(step,[status(thm)],[t457,t182]) ).
cnf(t503,plain,
upme(X1,X2,lojo(X3,X2,Y3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t286857]) ).
cnf(t622,plain,
upme(X1,a,X2) = upme(X1,a,lojo(X2,X3,a)),
inference(cp,[status(thm)],[t503,t615]) ).
cnf(t286881,plain,
upme(X1,X2,a) = upme(X1,a,lojo(X2,X3,a)),
inference(step,[status(thm)],[t622,t87]) ).
cnf(t686,plain,
upme(X1,a,lojo(X2,X3,a)) = upme(X1,X2,a),
inference(orient,[status(thm)],[t286881]) ).
cnf(t704,plain,
lome(a,X1,X2) = lome(a,X1,upme(X2,X3,a)),
inference(cp,[status(thm)],[t355,t686]) ).
cnf(t862,plain,
lome(a,X1,upme(X2,X3,a)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t704]) ).
cnf(t865,plain,
lome(a,X1,join(X2,X3)) = lome(a,X1,upjo(X2,X3,a)),
inference(cp,[status(thm)],[t862,t38]) ).
cnf(t1216,plain,
lome(a,X1,upjo(X2,X3,a)) = lome(a,X1,join(X2,X3)),
inference(orient,[status(thm)],[t865]) ).
cnf(t1217,plain,
lome(a,upjo(X1,X2,a),join(X1,X2)) = meet(a,upjo(X1,X2,a)),
inference(cp,[status(thm)],[t1216,t121]) ).
cnf(t702,plain,
lome(a,X1,X2) = lome(a,upme(X1,X3,a),X2),
inference(cp,[status(thm)],[t376,t686]) ).
cnf(t836,plain,
lome(a,upme(X1,X2,a),X3) = lome(a,X1,X3),
inference(orient,[status(thm)],[t702]) ).
cnf(t839,plain,
lome(a,join(X1,X2),X3) = lome(a,upjo(X1,X2,a),X3),
inference(cp,[status(thm)],[t836,t38]) ).
cnf(t1164,plain,
lome(a,upjo(X1,X2,a),X3) = lome(a,join(X1,X2),X3),
inference(orient,[status(thm)],[t839]) ).
cnf(t286921,plain,
lome(a,join(X1,X2),join(X1,X2)) = meet(a,upjo(X1,X2,a)),
inference(step,[status(thm)],[t1217,t1164]) ).
cnf(t286922,plain,
meet(a,join(X1,X2)) = meet(a,upjo(X1,X2,a)),
inference(step,[status(thm)],[t286921,t121]) ).
cnf(t286923,plain,
upme(a,X1,X2) = meet(a,upjo(X1,X2,a)),
inference(step,[status(thm)],[t286922,t31]) ).
cnf(t1223,plain,
meet(a,upjo(X1,X2,a)) = upme(a,X1,X2),
inference(orient,[status(thm)],[t286923]) ).
cnf(t171,plain,
upjo(X1,meet(X2,X3),Y3) = upjo(X1,lojo(X1,X2,X3),Y3),
inference(cp,[status(thm)],[t169,t55]) ).
cnf(t553,plain,
upjo(X1,lojo(X1,X2,X3),Y3) = upjo(X1,meet(X2,X3),Y3),
inference(orient,[status(thm)],[t171]) ).
cnf(t2037,plain,
meet(X1,X2) = lome(X1,upme(X2,X3,Y3),X2),
inference(cp,[status(thm)],[t2020,t189]) ).
cnf(t2102,plain,
lome(X1,upme(X2,X3,Y3),X2) = meet(X1,X2),
inference(orient,[status(thm)],[t2037]) ).
cnf(t2140,plain,
lojo(X1,upme(X1,X2,X3),a) = join(X1,meet(a,X1)),
inference(cp,[status(thm)],[t652,t2102]) ).
cnf(t286991,plain,
lojo(X1,a,upme(X1,X2,X3)) = join(X1,meet(a,X1)),
inference(step,[status(thm)],[t2140,t90]) ).
cnf(t286992,plain,
lojo(X1,a,upme(X1,X2,X3)) = lojo(X1,a,X1),
inference(step,[status(thm)],[t286991,t55]) ).
cnf(t286993,plain,
lojo(X1,a,upme(X1,X2,X3)) = lojo(X1,X1,a),
inference(step,[status(thm)],[t286992,t90]) ).
cnf(t286994,plain,
lojo(X1,a,upme(X1,X2,X3)) = X1,
inference(step,[status(thm)],[t286993,t86]) ).
cnf(t2153,plain,
lojo(X1,a,upme(X1,X2,X3)) = X1,
inference(orient,[status(thm)],[t286994]) ).
cnf(t2168,plain,
join(X1,X2) = lojo(join(X1,X2),a,upjo(X1,X2,X3)),
inference(cp,[status(thm)],[t2153,t38]) ).
cnf(t4013,plain,
lojo(join(X1,X2),a,upjo(X1,X2,X3)) = join(X1,X2),
inference(orient,[status(thm)],[t2168]) ).
cnf(t4037,plain,
join(X1,X2) = lojo(join(X1,X2),a,X1),
inference(cp,[status(thm)],[t4013,t160]) ).
cnf(t287077,plain,
join(X1,X2) = lojo(join(X1,X2),X1,a),
inference(step,[status(thm)],[t4037,t90]) ).
cnf(t4085,plain,
lojo(join(X1,X2),X1,a) = join(X1,X2),
inference(orient,[status(thm)],[t287077]) ).
cnf(t4106,plain,
upjo(join(X1,X2),meet(X1,a),X3) = upjo(join(X1,X2),join(X1,X2),X3),
inference(cp,[status(thm)],[t553,t4085]) ).
cnf(t287089,plain,
upjo(join(X1,X2),meet(X1,a),X3) = join(X1,X2),
inference(step,[status(thm)],[t4106,t120]) ).
cnf(t4353,plain,
upjo(join(X1,X2),meet(X1,a),X3) = join(X1,X2),
inference(orient,[status(thm)],[t287089]) ).
cnf(t4366,plain,
upme(a,join(X1,X2),meet(X1,a)) = meet(a,join(X1,X2)),
inference(cp,[status(thm)],[t1223,t4353]) ).
cnf(t183,plain,
upme(join(X1,X2),X1,X3) = upjo(X1,X2,join(X1,X3)),
inference(cp,[status(thm)],[t182,t38]) ).
cnf(t286818,plain,
upjo(X1,X2,X3) = upjo(X1,X2,join(X1,X3)),
inference(step,[status(thm)],[t183,t38]) ).
cnf(t213,plain,
upjo(X1,X2,join(X1,X3)) = upjo(X1,X2,X3),
inference(orient,[status(thm)],[t286818]) ).
cnf(t456,plain,
upjo(X1,X2,lojo(X3,X1,Y3)) = upjo(X1,X2,join(X1,X3)),
inference(cp,[status(thm)],[t213,t447]) ).
cnf(t286856,plain,
upjo(X1,X2,lojo(X3,X1,Y3)) = upjo(X1,X2,X3),
inference(step,[status(thm)],[t456,t213]) ).
cnf(t497,plain,
upjo(X1,X2,lojo(X3,X1,Y3)) = upjo(X1,X2,X3),
inference(orient,[status(thm)],[t286856]) ).
cnf(t703,plain,
lojo(X1,a,X2) = lojo(X1,a,upme(X2,X3,a)),
inference(cp,[status(thm)],[t370,t686]) ).
cnf(t286893,plain,
lojo(X1,X2,a) = lojo(X1,a,upme(X2,X3,a)),
inference(step,[status(thm)],[t703,t90]) ).
cnf(t841,plain,
lojo(X1,a,upme(X2,X3,a)) = lojo(X1,X2,a),
inference(orient,[status(thm)],[t286893]) ).
cnf(t856,plain,
upjo(a,X1,X2) = upjo(a,X1,lojo(X2,X3,a)),
inference(cp,[status(thm)],[t497,t841]) ).
cnf(t867,plain,
upjo(a,X1,lojo(X2,X3,a)) = upjo(a,X1,X2),
inference(orient,[status(thm)],[t856]) ).
cnf(t870,plain,
upjo(a,X1,meet(X2,X3)) = upjo(a,X1,lome(X2,X3,a)),
inference(cp,[status(thm)],[t867,t80]) ).
cnf(t1229,plain,
upjo(a,X1,lome(X2,X3,a)) = upjo(a,X1,meet(X2,X3)),
inference(orient,[status(thm)],[t870]) ).
cnf(t691,plain,
upme(X1,X2,a) = upme(X1,a,join(X2,a)),
inference(cp,[status(thm)],[t686,t122]) ).
cnf(t729,plain,
upme(X1,a,join(X2,a)) = upme(X1,X2,a),
inference(orient,[status(thm)],[t691]) ).
cnf(t731,plain,
upme(join(a,X1),X2,a) = upjo(a,X1,join(X2,a)),
inference(cp,[status(thm)],[t729,t38]) ).
cnf(t286887,plain,
upme(join(X1,a),X2,a) = upjo(a,X1,join(X2,a)),
inference(step,[status(thm)],[t731,t51]) ).
cnf(t688,plain,
upme(a,X1,a) = a,
inference(cp,[status(thm)],[t686,t85]) ).
cnf(t708,plain,
upme(a,X1,a) = a,
inference(orient,[status(thm)],[t688]) ).
cnf(t711,plain,
lojo(X1,a,join(X2,a)) = lojo(X1,a,a),
inference(cp,[status(thm)],[t558,t708]) ).
cnf(t286884,plain,
lojo(X1,a,join(X2,a)) = join(X1,a),
inference(step,[status(thm)],[t711,t122]) ).
cnf(t721,plain,
lojo(X1,a,join(X2,a)) = join(X1,a),
inference(orient,[status(thm)],[t286884]) ).
cnf(t725,plain,
upjo(a,X1,X2) = upjo(a,X1,join(X2,a)),
inference(cp,[status(thm)],[t497,t721]) ).
cnf(t743,plain,
upjo(a,X1,join(X2,a)) = upjo(a,X1,X2),
inference(orient,[status(thm)],[t725]) ).
cnf(t286888,plain,
upme(join(X1,a),X2,a) = upjo(a,X1,X2),
inference(step,[status(thm)],[t286887,t743]) ).
cnf(t779,plain,
upme(join(X1,a),X2,a) = upjo(a,X1,X2),
inference(orient,[status(thm)],[t286888]) ).
cnf(t793,plain,
meet(X1,join(X2,a)) = meet(X1,upjo(a,X2,X1)),
inference(cp,[status(thm)],[t328,t779]) ).
cnf(t286889,plain,
upme(X1,X2,a) = meet(X1,upjo(a,X2,X1)),
inference(step,[status(thm)],[t793,t31]) ).
cnf(t799,plain,
meet(X1,upjo(a,X2,X1)) = upme(X1,X2,a),
inference(orient,[status(thm)],[t286889]) ).
cnf(t214,plain,
upjo(X1,X2,meet(X3,Y3)) = upjo(X1,X2,lojo(X1,X3,Y3)),
inference(cp,[status(thm)],[t213,t55]) ).
cnf(t572,plain,
upjo(X1,X2,lojo(X1,X3,Y3)) = upjo(X1,X2,meet(X3,Y3)),
inference(orient,[status(thm)],[t214]) ).
cnf(t595,plain,
upjo(a,X1,meet(X2,a)) = upjo(a,X1,a),
inference(cp,[status(thm)],[t572,t594]) ).
cnf(t286870,plain,
upjo(a,X1,meet(X2,a)) = a,
inference(step,[status(thm)],[t595,t160]) ).
cnf(t601,plain,
upjo(a,X1,meet(X2,a)) = a,
inference(orient,[status(thm)],[t286870]) ).
cnf(t800,plain,
upme(meet(X1,a),X2,a) = meet(meet(X1,a),a),
inference(cp,[status(thm)],[t799,t601]) ).
cnf(t286890,plain,
upme(meet(X1,a),X2,a) = meet(a,meet(X1,a)),
inference(step,[status(thm)],[t800,t15]) ).
cnf(t286891,plain,
upme(meet(X1,a),X2,a) = meet(X1,meet(a,a)),
inference(step,[status(thm)],[t286890,t17]) ).
cnf(t286892,plain,
upme(meet(X1,a),X2,a) = meet(X1,a),
inference(step,[status(thm)],[t286891,t127]) ).
cnf(t826,plain,
upme(meet(X1,a),X2,a) = meet(X1,a),
inference(orient,[status(thm)],[t286892]) ).
cnf(t830,plain,
lome(meet(X1,a),X2,join(X3,a)) = lome(meet(X1,a),X2,meet(X1,a)),
inference(cp,[status(thm)],[t576,t826]) ).
cnf(t286896,plain,
lome(meet(X1,a),X2,join(X3,a)) = meet(X1,a),
inference(step,[status(thm)],[t830,t159]) ).
cnf(t899,plain,
lome(meet(X1,a),X2,join(X3,a)) = meet(X1,a),
inference(orient,[status(thm)],[t286896]) ).
cnf(t901,plain,
meet(X1,a) = lome(meet(X1,a),X2,a),
inference(cp,[status(thm)],[t899,t110]) ).
cnf(t905,plain,
lome(meet(X1,a),X2,a) = meet(X1,a),
inference(orient,[status(thm)],[t901]) ).
cnf(t1231,plain,
upjo(a,X1,meet(meet(X2,a),X3)) = upjo(a,X1,meet(X2,a)),
inference(cp,[status(thm)],[t1229,t905]) ).
cnf(t286924,plain,
upjo(a,X1,meet(X3,meet(X2,a))) = upjo(a,X1,meet(X2,a)),
inference(step,[status(thm)],[t1231,t15]) ).
cnf(t286925,plain,
upjo(a,X1,meet(X2,meet(a,X3))) = upjo(a,X1,meet(X2,a)),
inference(step,[status(thm)],[t286924,t17]) ).
cnf(t286926,plain,
upjo(a,X1,meet(X2,meet(X3,a))) = upjo(a,X1,meet(X2,a)),
inference(step,[status(thm)],[t286925,t15]) ).
cnf(t286927,plain,
upjo(a,X1,meet(X2,meet(X3,a))) = a,
inference(step,[status(thm)],[t286926,t601]) ).
cnf(t1236,plain,
upjo(a,X1,meet(X2,meet(X3,a))) = a,
inference(orient,[status(thm)],[t286927]) ).
cnf(t1237,plain,
a = join(a,meet(X1,meet(X2,a))),
inference(cp,[status(thm)],[t1236,t135]) ).
cnf(t286928,plain,
a = lojo(a,X1,meet(X2,a)),
inference(step,[status(thm)],[t1237,t55]) ).
cnf(t1246,plain,
lojo(a,X1,meet(X2,a)) = a,
inference(orient,[status(thm)],[t286928]) ).
cnf(t1251,plain,
lojo(upme(meet(X1,a),X2,a),X2,a) = upme(a,X2,meet(X1,meet(a,a))),
inference(cp,[status(thm)],[t305,t1246]) ).
cnf(t286929,plain,
lojo(meet(X1,a),X2,a) = upme(a,X2,meet(X1,meet(a,a))),
inference(step,[status(thm)],[t1251,t826]) ).
cnf(t286930,plain,
lome(a,X1,X2) = upme(a,X2,meet(X1,meet(a,a))),
inference(step,[status(thm)],[t286929,t632]) ).
cnf(t286931,plain,
lome(a,X1,X2) = upme(a,X2,meet(X1,a)),
inference(step,[status(thm)],[t286930,t127]) ).
cnf(t1253,plain,
upme(a,X1,meet(X2,a)) = lome(a,X2,X1),
inference(orient,[status(thm)],[t286931]) ).
cnf(t287090,plain,
lome(a,X1,join(X1,X2)) = meet(a,join(X1,X2)),
inference(step,[status(thm)],[t4366,t1253]) ).
cnf(t287091,plain,
lome(a,X1,join(X1,X2)) = upme(a,X1,X2),
inference(step,[status(thm)],[t287090,t31]) ).
cnf(t4369,plain,
lome(a,X1,join(X1,X2)) = upme(a,X1,X2),
inference(orient,[status(thm)],[t287091]) ).
cnf(t4384,plain,
upme(a,X1,lome(a,X2,X1)) = lome(a,X1,lojo(X1,X2,a)),
inference(cp,[status(thm)],[t4369,t652]) ).
cnf(t641,plain,
upme(X1,X2,meet(X3,a)) = upme(X1,X2,lome(a,X3,X2)),
inference(cp,[status(thm)],[t503,t632]) ).
cnf(t921,plain,
upme(X1,X2,lome(a,X3,X2)) = upme(X1,X2,meet(X3,a)),
inference(orient,[status(thm)],[t641]) ).
cnf(t287094,plain,
upme(a,X1,meet(X2,a)) = lome(a,X1,lojo(X1,X2,a)),
inference(step,[status(thm)],[t4384,t921]) ).
cnf(t287095,plain,
lome(a,X2,X1) = lome(a,X1,lojo(X1,X2,a)),
inference(step,[status(thm)],[t287094,t1253]) ).
cnf(t1257,plain,
lome(a,X1,join(X2,meet(X3,a))) = lome(a,X1,lome(a,X3,X2)),
inference(cp,[status(thm)],[t576,t1253]) ).
cnf(t286963,plain,
lome(a,X1,lojo(X2,X3,a)) = lome(a,X1,lome(a,X3,X2)),
inference(step,[status(thm)],[t1257,t55]) ).
cnf(t1716,plain,
lome(a,X1,lojo(X2,X3,a)) = lome(a,X1,lome(a,X3,X2)),
inference(orient,[status(thm)],[t286963]) ).
cnf(t287096,plain,
lome(a,X2,X1) = lome(a,X1,lome(a,X2,X1)),
inference(step,[status(thm)],[t287095,t1716]) ).
cnf(t4470,plain,
lome(a,X1,lome(a,X2,X1)) = lome(a,X2,X1),
inference(orient,[status(thm)],[t287096]) ).
cnf(t4481,plain,
lome(a,X1,lome(a,X2,X1)) = join(meet(X1,a),lome(a,X2,X1)),
inference(cp,[status(thm)],[t1523,t4470]) ).
cnf(t287097,plain,
lome(a,X2,X1) = join(meet(X1,a),lome(a,X2,X1)),
inference(step,[status(thm)],[t4481,t4470]) ).
cnf(t653,plain,
lojo(meet(X1,a),X2,a) = join(meet(X1,a),lome(a,X2,X1)),
inference(cp,[status(thm)],[t652,t630]) ).
cnf(t286956,plain,
lome(a,X1,X2) = join(meet(X1,a),lome(a,X2,X1)),
inference(step,[status(thm)],[t653,t632]) ).
cnf(t1552,plain,
join(meet(X1,a),lome(a,X2,X1)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t286956]) ).
cnf(t287098,plain,
lome(a,X2,X1) = lome(a,X1,X2),
inference(step,[status(thm)],[t287097,t1552]) ).
cnf(t4492,plain,
lome(a,X1,X2) = lome(a,X2,X1),
inference(orient,[status(thm)],[t287098]) ).
cnf(t287107,plain,
join(X1,lome(a,X1,X2)) = lojo(X1,X2,a),
inference(step,[status(thm)],[t4558,t4492]) ).
cnf(t4566,plain,
join(X1,lome(a,X1,X2)) = lojo(X1,X2,a),
inference(orient,[status(thm)],[t287107]) ).
cnf(t8776,plain,
X1 = lome(X1,lojo(lojo(X1,X2,a),X3,Y3),Y4),
inference(cp,[status(thm)],[t8754,t4566]) ).
cnf(t10740,plain,
lome(X1,lojo(lojo(X1,X2,a),X3,Y3),Y4) = X1,
inference(orient,[status(thm)],[t8776]) ).
cnf(t10741,plain,
X1 = meet(X1,lojo(lojo(X1,X2,a),X3,Y3)),
inference(cp,[status(thm)],[t10740,t121]) ).
cnf(t287277,plain,
X1 = upme(X1,lojo(X1,X2,a),meet(X3,Y3)),
inference(step,[status(thm)],[t10741,t253]) ).
cnf(t287278,plain,
X1 = upme(X1,meet(X3,Y3),lojo(X1,X2,a)),
inference(step,[status(thm)],[t287277,t87]) ).
cnf(t10794,plain,
upme(X1,meet(X2,X3),lojo(X1,Y3,a)) = X1,
inference(orient,[status(thm)],[t287278]) ).
cnf(t10799,plain,
X1 = upme(X1,X2,lojo(X1,X3,a)),
inference(cp,[status(thm)],[t10794,t127]) ).
cnf(t10845,plain,
upme(X1,X2,lojo(X1,X3,a)) = X1,
inference(orient,[status(thm)],[t10799]) ).
cnf(t10864,plain,
meet(X1,X2) = upme(meet(X1,X2),X3,lome(X1,X2,a)),
inference(cp,[status(thm)],[t10845,t80]) ).
cnf(t11140,plain,
upme(meet(X1,X2),X3,lome(X1,X2,a)) = meet(X1,X2),
inference(orient,[status(thm)],[t10864]) ).
cnf(t11156,plain,
meet(meet(X1,X2),lome(X1,X2,X3)) = upme(meet(X1,X2),Y3,lome(meet(X1,X2),lome(X1,X2,X3),a)),
inference(cp,[status(thm)],[t11140,t1970]) ).
cnf(t287288,plain,
meet(X1,X2) = upme(meet(X1,X2),Y3,lome(meet(X1,X2),lome(X1,X2,X3),a)),
inference(step,[status(thm)],[t11156,t1970]) ).
cnf(t287289,plain,
meet(X1,X2) = upme(meet(X1,X2),Y3,meet(X1,X2)),
inference(step,[status(thm)],[t287288,t2316]) ).
cnf(t11239,plain,
upme(meet(X1,X2),X3,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t287289]) ).
cnf(t11285,plain,
lome(meet(X1,X2),X3,join(Y3,meet(X1,X2))) = lome(meet(X1,X2),X3,meet(X1,X2)),
inference(cp,[status(thm)],[t576,t11239]) ).
cnf(t287295,plain,
lome(meet(X1,X2),X3,lojo(Y3,X1,X2)) = lome(meet(X1,X2),X3,meet(X1,X2)),
inference(step,[status(thm)],[t11285,t55]) ).
cnf(t287296,plain,
lome(meet(X1,X2),X3,lojo(Y3,X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t287295,t159]) ).
cnf(t11748,plain,
lome(meet(X1,X2),X3,lojo(Y3,X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t287296]) ).
cnf(t6328,plain,
join(X1,upme(meet(X1,X2),X3,Y3)) = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t447,t6265]) ).
cnf(t287187,plain,
lojo(X1,meet(X1,X2),join(X3,Y3)) = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t6328,t93]) ).
cnf(t287188,plain,
lojo(X1,meet(X1,X2),join(X3,Y3)) = lojo(X1,X1,X2),
inference(step,[status(thm)],[t287187,t55]) ).
cnf(t287189,plain,
lojo(X1,meet(X1,X2),join(X3,Y3)) = X1,
inference(step,[status(thm)],[t287188,t86]) ).
cnf(t6337,plain,
lojo(X1,meet(X1,X2),join(X3,Y3)) = X1,
inference(orient,[status(thm)],[t287189]) ).
cnf(t6341,plain,
X1 = lojo(X1,upme(X1,X2,X3),join(Y3,Y4)),
inference(cp,[status(thm)],[t6337,t189]) ).
cnf(t287200,plain,
X1 = lojo(X1,join(Y3,Y4),upme(X1,X2,X3)),
inference(step,[status(thm)],[t6341,t90]) ).
cnf(t6692,plain,
lojo(X1,join(X2,X3),upme(X1,Y3,Y4)) = X1,
inference(orient,[status(thm)],[t287200]) ).
cnf(t6697,plain,
X1 = lojo(X1,X2,upme(X1,X3,Y3)),
inference(cp,[status(thm)],[t6692,t110]) ).
cnf(t6749,plain,
lojo(X1,X2,upme(X1,X3,Y3)) = X1,
inference(orient,[status(thm)],[t6697]) ).
cnf(t6780,plain,
join(X1,X2) = lojo(join(X1,X2),X3,upjo(X1,X2,Y3)),
inference(cp,[status(thm)],[t6749,t38]) ).
cnf(t7965,plain,
lojo(join(X1,X2),X3,upjo(X1,X2,Y3)) = join(X1,X2),
inference(orient,[status(thm)],[t6780]) ).
cnf(t7989,plain,
join(X1,X2) = lojo(join(X1,X2),X3,X1),
inference(cp,[status(thm)],[t7965,t160]) ).
cnf(t287226,plain,
join(X1,X2) = lojo(join(X1,X2),X1,X3),
inference(step,[status(thm)],[t7989,t90]) ).
cnf(t8051,plain,
lojo(join(X1,X2),X1,X3) = join(X1,X2),
inference(orient,[status(thm)],[t287226]) ).
cnf(t11807,plain,
meet(X1,X2) = lome(meet(X1,X2),X3,join(X1,Y3)),
inference(cp,[status(thm)],[t11748,t8051]) ).
cnf(t11836,plain,
lome(meet(X1,X2),X3,join(X1,Y3)) = meet(X1,X2),
inference(orient,[status(thm)],[t11807]) ).
cnf(t11837,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t11836,t121]) ).
cnf(t287297,plain,
meet(X1,X2) = upme(meet(X1,X2),X1,X3),
inference(step,[status(thm)],[t11837,t31]) ).
cnf(t11881,plain,
upme(meet(X1,X2),X1,X3) = meet(X1,X2),
inference(orient,[status(thm)],[t287297]) ).
cnf(t287325,plain,
lojo(meet(X1,a),X1,X2) = meet(lojo(X2,X1,meet(X1,a)),X1),
inference(step,[status(thm)],[t306,t11881]) ).
cnf(t287326,plain,
lome(X1,a,X2) = meet(lojo(X2,X1,meet(X1,a)),X1),
inference(step,[status(thm)],[t287325,t80]) ).
cnf(t287327,plain,
lome(X1,a,X2) = meet(X1,lojo(X2,X1,meet(X1,a))),
inference(step,[status(thm)],[t287326,t15]) ).
cnf(t287328,plain,
lome(X1,a,X2) = upme(X1,X2,meet(X1,meet(X1,a))),
inference(step,[status(thm)],[t287327,t253]) ).
cnf(t287329,plain,
lome(X1,a,X2) = upme(X1,X2,meet(X1,a)),
inference(step,[status(thm)],[t287328,t148]) ).
cnf(t13513,plain,
upme(X1,X2,meet(X1,a)) = lome(X1,a,X2),
inference(orient,[status(thm)],[t287329]) ).
cnf(t13559,plain,
meet(X1,upme(X2,X3,meet(X1,a))) = meet(X2,lome(X1,a,X3)),
inference(cp,[status(thm)],[t285,t13513]) ).
cnf(t287456,plain,
meet(X1,upme(X2,X3,meet(X1,a))) = meet(X2,lome(X1,X3,a)),
inference(step,[status(thm)],[t13559,t19398]) ).
cnf(t21810,plain,
meet(X1,upme(X2,X3,meet(X1,a))) = meet(X2,lome(X1,X3,a)),
inference(orient,[status(thm)],[t287456]) ).
cnf(t28465,plain,
meet(meet(X1,X2),lome(X3,X2,a)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t21810,t28408]) ).
cnf(t287594,plain,
meet(meet(X1,X2),lome(X3,X2,a)) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t28465,t17]) ).
cnf(t287595,plain,
meet(meet(X1,X2),lome(X3,X2,a)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t287594,t17]) ).
cnf(t29809,plain,
meet(meet(X1,X2),lome(X3,X2,a)) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t287595]) ).
cnf(t29886,plain,
meet(X1,meet(X2,upme(X2,X3,Y3))) = meet(meet(X1,X2),upme(X2,X3,Y3)),
inference(cp,[status(thm)],[t29809,t2406]) ).
cnf(t287629,plain,
meet(X1,upme(X2,X3,Y3)) = meet(meet(X1,X2),upme(X2,X3,Y3)),
inference(step,[status(thm)],[t29886,t189]) ).
cnf(t287630,plain,
meet(X1,upme(X2,X3,Y3)) = meet(X2,upme(meet(X1,X2),X3,Y3)),
inference(step,[status(thm)],[t287629,t285]) ).
cnf(t33430,plain,
meet(X1,upme(meet(X2,X1),X3,Y3)) = meet(X2,upme(X1,X3,Y3)),
inference(orient,[status(thm)],[t287630]) ).
cnf(t33518,plain,
meet(X1,upme(X2,X3,Y3)) = meet(X2,upme(meet(X2,X1),X3,Y3)),
inference(cp,[status(thm)],[t33430,t15]) ).
cnf(t287632,plain,
meet(X1,upme(X2,X3,Y3)) = upme(meet(X2,X1),X3,Y3),
inference(step,[status(thm)],[t33518,t17392]) ).
cnf(t287633,plain,
meet(X1,upme(X2,X3,Y3)) = upme(meet(X1,X2),X3,Y3),
inference(step,[status(thm)],[t287632,t15]) ).
cnf(t33621,plain,
meet(X1,upme(X2,X3,Y3)) = upme(meet(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t287633]) ).
cnf(t287640,plain,
upme(meet(X1,X2),X3,meet(X1,a)) = meet(X2,lome(X1,X3,a)),
inference(step,[status(thm)],[t21810,t33621]) ).
cnf(t33794,plain,
upme(meet(X1,X2),X3,meet(X1,a)) = meet(X2,lome(X1,X3,a)),
inference(rw,[status(thm)],[t287640]) ).
cnf(t36935,plain,
upme(meet(X1,X2),X3,meet(X1,a)) = meet(X2,lome(X1,X3,a)),
inference(orient,[status(thm)],[t33794]) ).
cnf(t37029,plain,
meet(X1,X2) = lojo(meet(X2,lome(X1,X3,a)),X1,X2),
inference(cp,[status(thm)],[t6265,t36935]) ).
cnf(t37033,plain,
lojo(meet(X1,lome(X2,X3,a)),X2,X1) = meet(X2,X1),
inference(orient,[status(thm)],[t37029]) ).
cnf(t46250,plain,
join(X1,meet(lome(X1,X2,X3),lome(Y3,Y4,a))) = join(X1,meet(Y3,lome(X1,X2,X3))),
inference(cp,[status(thm)],[t46243,t37033]) ).
cnf(t287819,plain,
lojo(X1,lome(X1,X2,X3),lome(Y3,Y4,a)) = join(X1,meet(Y3,lome(X1,X2,X3))),
inference(step,[status(thm)],[t46250,t55]) ).
cnf(t287820,plain,
lojo(X1,lome(X1,X2,X3),lome(Y3,Y4,a)) = lojo(X1,Y3,lome(X1,X2,X3)),
inference(step,[status(thm)],[t287819,t55]) ).
cnf(t287821,plain,
lojo(X1,lome(X1,X2,X3),lome(Y3,Y4,a)) = X1,
inference(step,[status(thm)],[t287820,t41310]) ).
cnf(t49680,plain,
lojo(X1,lome(X1,X2,X3),lome(Y3,Y4,a)) = X1,
inference(orient,[status(thm)],[t287821]) ).
cnf(t13516,plain,
lome(join(X1,X2),a,X1) = upjo(X1,X2,meet(join(X1,X2),a)),
inference(cp,[status(thm)],[t13513,t38]) ).
cnf(t287440,plain,
lome(join(X1,X2),a,X1) = upjo(X1,X2,meet(a,join(X1,X2))),
inference(step,[status(thm)],[t13516,t15]) ).
cnf(t287441,plain,
lome(join(X1,X2),a,X1) = upjo(X1,X2,upme(a,X1,X2)),
inference(step,[status(thm)],[t287440,t31]) ).
cnf(t20912,plain,
upjo(X1,X2,upme(a,X1,X2)) = lome(join(X1,X2),a,X1),
inference(orient,[status(thm)],[t287441]) ).
cnf(t455,plain,
upjo(X1,lojo(X2,X1,X3),Y3) = upme(join(X1,X2),X1,Y3),
inference(cp,[status(thm)],[t38,t447]) ).
cnf(t286854,plain,
upjo(X1,lojo(X2,X1,X3),Y3) = upjo(X1,X2,Y3),
inference(step,[status(thm)],[t455,t38]) ).
cnf(t482,plain,
upjo(X1,lojo(X2,X1,X3),Y3) = upjo(X1,X2,Y3),
inference(orient,[status(thm)],[t286854]) ).
cnf(t643,plain,
upjo(X1,meet(X2,a),X3) = upjo(X1,lome(a,X2,X1),X3),
inference(cp,[status(thm)],[t482,t632]) ).
cnf(t964,plain,
upjo(X1,lome(a,X2,X1),X3) = upjo(X1,meet(X2,a),X3),
inference(orient,[status(thm)],[t643]) ).
cnf(t4553,plain,
upjo(X1,lome(a,X2,X1),X3) = upjo(X1,meet(X2,a),X3),
inference(rw,[status(thm)],[t964]) ).
cnf(t287120,plain,
upjo(X1,lome(a,X1,X2),X3) = upjo(X1,meet(X2,a),X3),
inference(step,[status(thm)],[t4553,t4492]) ).
cnf(t4813,plain,
upjo(X1,lome(a,X1,X2),X3) = upjo(X1,meet(X2,a),X3),
inference(orient,[status(thm)],[t287120]) ).
cnf(t20916,plain,
lome(join(X1,lome(a,X1,X2)),a,X1) = upjo(X1,meet(X2,a),upme(a,X1,lome(a,X1,X2))),
inference(cp,[status(thm)],[t20912,t4813]) ).
cnf(t287443,plain,
lome(lojo(X1,X2,a),a,X1) = upjo(X1,meet(X2,a),upme(a,X1,lome(a,X1,X2))),
inference(step,[status(thm)],[t20916,t4566]) ).
cnf(t4599,plain,
upme(a,X1,lome(a,X1,X2)) = lome(a,X1,lojo(X1,X2,a)),
inference(cp,[status(thm)],[t4369,t4566]) ).
cnf(t287105,plain,
lome(a,X1,lojo(X2,X3,a)) = lome(a,X1,lome(a,X2,X3)),
inference(step,[status(thm)],[t1716,t4492]) ).
cnf(t4499,plain,
lome(a,X1,lojo(X2,X3,a)) = lome(a,X1,lome(a,X2,X3)),
inference(orient,[status(thm)],[t287105]) ).
cnf(t287108,plain,
upme(a,X1,lome(a,X1,X2)) = lome(a,X1,lome(a,X1,X2)),
inference(step,[status(thm)],[t4599,t4499]) ).
cnf(t4093,plain,
join(meet(X1,a),lome(a,X1,X2)) = lojo(lome(a,X1,X2),meet(X1,a),a),
inference(cp,[status(thm)],[t4085,t1523]) ).
cnf(t287082,plain,
lome(a,X1,X2) = lojo(lome(a,X1,X2),meet(X1,a),a),
inference(step,[status(thm)],[t4093,t1523]) ).
cnf(t464,plain,
upjo(X1,X2,lome(X1,X3,Y3)) = upjo(X1,X2,X1),
inference(cp,[status(thm)],[t213,t462]) ).
cnf(t286852,plain,
upjo(X1,X2,lome(X1,X3,Y3)) = X1,
inference(step,[status(thm)],[t464,t160]) ).
cnf(t472,plain,
upjo(X1,X2,lome(X1,X3,Y3)) = X1,
inference(orient,[status(thm)],[t286852]) ).
cnf(t807,plain,
upme(lome(a,X1,X2),X3,a) = meet(lome(a,X1,X2),a),
inference(cp,[status(thm)],[t799,t472]) ).
cnf(t286908,plain,
upme(lome(a,X1,X2),X3,a) = meet(a,lome(a,X1,X2)),
inference(step,[status(thm)],[t807,t15]) ).
cnf(t1121,plain,
upme(lome(a,X1,X2),X3,a) = meet(a,lome(a,X1,X2)),
inference(orient,[status(thm)],[t286908]) ).
cnf(t1123,plain,
meet(a,lome(a,X1,X2)) = lome(a,X1,X2),
inference(cp,[status(thm)],[t1121,t85]) ).
cnf(t1141,plain,
meet(a,lome(a,X1,X2)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t1123]) ).
cnf(t1144,plain,
lome(a,lome(a,X1,X2),X3) = lojo(lome(a,X1,X2),a,X3),
inference(cp,[status(thm)],[t80,t1141]) ).
cnf(t286962,plain,
lome(a,lome(a,X1,X2),X3) = lojo(lome(a,X1,X2),X3,a),
inference(step,[status(thm)],[t1144,t90]) ).
cnf(t1696,plain,
lojo(lome(a,X1,X2),X3,a) = lome(a,lome(a,X1,X2),X3),
inference(orient,[status(thm)],[t286962]) ).
cnf(t287083,plain,
lome(a,X1,X2) = lome(a,lome(a,X1,X2),meet(X1,a)),
inference(step,[status(thm)],[t287082,t1696]) ).
cnf(t287084,plain,
lome(a,X1,X2) = lome(a,lome(a,X1,X2),X1),
inference(step,[status(thm)],[t287083,t630]) ).
cnf(t4161,plain,
lome(a,lome(a,X1,X2),X1) = lome(a,X1,X2),
inference(orient,[status(thm)],[t287084]) ).
cnf(t4169,plain,
lome(a,X1,lome(a,X1,X2)) = join(meet(X1,a),lome(a,X1,X2)),
inference(cp,[status(thm)],[t1552,t4161]) ).
cnf(t287085,plain,
lome(a,X1,lome(a,X1,X2)) = lome(a,X1,X2),
inference(step,[status(thm)],[t4169,t1523]) ).
cnf(t4211,plain,
lome(a,X1,lome(a,X1,X2)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t287085]) ).
cnf(t287109,plain,
upme(a,X1,lome(a,X1,X2)) = lome(a,X1,X2),
inference(step,[status(thm)],[t287108,t4211]) ).
cnf(t4621,plain,
upme(a,X1,lome(a,X1,X2)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t287109]) ).
cnf(t287444,plain,
lome(lojo(X1,X2,a),a,X1) = upjo(X1,meet(X2,a),lome(a,X1,X2)),
inference(step,[status(thm)],[t287443,t4621]) ).
cnf(t642,plain,
upjo(X1,X2,meet(X3,a)) = upjo(X1,X2,lome(a,X3,X1)),
inference(cp,[status(thm)],[t497,t632]) ).
cnf(t944,plain,
upjo(X1,X2,lome(a,X3,X1)) = upjo(X1,X2,meet(X3,a)),
inference(orient,[status(thm)],[t642]) ).
cnf(t4554,plain,
upjo(X1,X2,lome(a,X3,X1)) = upjo(X1,X2,meet(X3,a)),
inference(rw,[status(thm)],[t944]) ).
cnf(t287121,plain,
upjo(X1,X2,lome(a,X1,X3)) = upjo(X1,X2,meet(X3,a)),
inference(step,[status(thm)],[t4554,t4492]) ).
cnf(t4857,plain,
upjo(X1,X2,lome(a,X1,X3)) = upjo(X1,X2,meet(X3,a)),
inference(orient,[status(thm)],[t287121]) ).
cnf(t287445,plain,
lome(lojo(X1,X2,a),a,X1) = upjo(X1,meet(X2,a),meet(X2,a)),
inference(step,[status(thm)],[t287444,t4857]) ).
cnf(t287446,plain,
lome(lojo(X1,X2,a),a,X1) = join(X1,meet(X2,a)),
inference(step,[status(thm)],[t287445,t135]) ).
cnf(t287447,plain,
lome(lojo(X1,X2,a),a,X1) = lojo(X1,X2,a),
inference(step,[status(thm)],[t287446,t55]) ).
cnf(t21014,plain,
lome(lojo(X1,X2,a),a,X1) = lojo(X1,X2,a),
inference(orient,[status(thm)],[t287447]) ).
cnf(t22451,plain,
lome(lojo(X1,X2,a),a,X1) = lojo(X1,X2,a),
inference(rw,[status(thm)],[t21014]) ).
cnf(t6339,plain,
X1 = lojo(X1,upme(X1,X2,a),join(X3,Y3)),
inference(cp,[status(thm)],[t6337,t799]) ).
cnf(t287192,plain,
X1 = lojo(X1,join(X3,Y3),upme(X1,X2,a)),
inference(step,[status(thm)],[t6339,t90]) ).
cnf(t6459,plain,
lojo(X1,join(X2,X3),upme(X1,Y3,a)) = X1,
inference(orient,[status(thm)],[t287192]) ).
cnf(t6464,plain,
X1 = lojo(X1,X2,upme(X1,X3,a)),
inference(cp,[status(thm)],[t6459,t110]) ).
cnf(t6502,plain,
lojo(X1,X2,upme(X1,X3,a)) = X1,
inference(orient,[status(thm)],[t6464]) ).
cnf(t2654,plain,
join(X1,X2) = upjo(X1,lojo(X2,X3,Y3),X2),
inference(cp,[status(thm)],[t2640,t161]) ).
cnf(t2711,plain,
upjo(X1,lojo(X2,X3,Y3),X2) = join(X1,X2),
inference(orient,[status(thm)],[t2654]) ).
cnf(t2741,plain,
upme(X1,lojo(X1,X2,X3),a) = meet(X1,join(a,X1)),
inference(cp,[status(thm)],[t799,t2711]) ).
cnf(t287028,plain,
upme(X1,a,lojo(X1,X2,X3)) = meet(X1,join(a,X1)),
inference(step,[status(thm)],[t2741,t87]) ).
cnf(t287029,plain,
upme(X1,a,lojo(X1,X2,X3)) = upme(X1,a,X1),
inference(step,[status(thm)],[t287028,t31]) ).
cnf(t287030,plain,
upme(X1,a,lojo(X1,X2,X3)) = upme(X1,X1,a),
inference(step,[status(thm)],[t287029,t87]) ).
cnf(t287031,plain,
upme(X1,a,lojo(X1,X2,X3)) = X1,
inference(step,[status(thm)],[t287030,t85]) ).
cnf(t2836,plain,
upme(X1,a,lojo(X1,X2,X3)) = X1,
inference(orient,[status(thm)],[t287031]) ).
cnf(t2854,plain,
meet(X1,X2) = upme(meet(X1,X2),a,lome(X1,X2,X3)),
inference(cp,[status(thm)],[t2836,t80]) ).
cnf(t5750,plain,
upme(meet(X1,X2),a,lome(X1,X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t2854]) ).
cnf(t5776,plain,
meet(X1,X2) = upme(meet(X1,X2),a,X1),
inference(cp,[status(thm)],[t5750,t159]) ).
cnf(t287164,plain,
meet(X1,X2) = upme(meet(X1,X2),X1,a),
inference(step,[status(thm)],[t5776,t87]) ).
cnf(t5831,plain,
upme(meet(X1,X2),X1,a) = meet(X1,X2),
inference(orient,[status(thm)],[t287164]) ).
cnf(t6516,plain,
meet(X1,X2) = lojo(meet(X1,X2),X3,meet(X1,X2)),
inference(cp,[status(thm)],[t6502,t5831]) ).
cnf(t59,plain,
lojo(X1,X2,meet(X3,Y3)) = join(X1,meet(X3,meet(Y3,X2))),
inference(cp,[status(thm)],[t55,t17]) ).
cnf(t286885,plain,
lojo(X1,X2,meet(X3,Y3)) = lojo(X1,X3,meet(Y3,X2)),
inference(step,[status(thm)],[t59,t55]) ).
cnf(t286886,plain,
lojo(X1,X2,meet(X3,Y3)) = lojo(X1,X3,meet(X2,Y3)),
inference(step,[status(thm)],[t286885,t15]) ).
cnf(t747,plain,
lojo(X1,X2,meet(X3,Y3)) = lojo(X1,X3,meet(X2,Y3)),
inference(orient,[status(thm)],[t286886]) ).
cnf(t287195,plain,
meet(X1,X2) = lojo(meet(X1,X2),X1,meet(X3,X2)),
inference(step,[status(thm)],[t6516,t747]) ).
cnf(t287196,plain,
meet(X1,X2) = lome(X1,X2,meet(X3,X2)),
inference(step,[status(thm)],[t287195,t80]) ).
cnf(t287197,plain,
meet(X1,X2) = lome(X1,X2,meet(X2,X3)),
inference(step,[status(thm)],[t287196,t15]) ).
cnf(t6545,plain,
lome(X1,X2,meet(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t287197]) ).
cnf(t21855,plain,
meet(X1,X2) = lome(X1,X2,meet(X3,lome(X2,Y3,a))),
inference(cp,[status(thm)],[t6545,t21810]) ).
cnf(t22124,plain,
lome(X1,X2,meet(X3,lome(X2,Y3,a))) = meet(X1,X2),
inference(orient,[status(thm)],[t21855]) ).
cnf(t22125,plain,
meet(X1,X2) = lome(X1,X2,lome(X2,X3,a)),
inference(cp,[status(thm)],[t22124,t219]) ).
cnf(t22274,plain,
lome(X1,X2,lome(X2,X3,a)) = meet(X1,X2),
inference(orient,[status(thm)],[t22125]) ).
cnf(t22275,plain,
meet(lome(X1,X2,a),X1) = lome(X1,X2,a),
inference(cp,[status(thm)],[t22274,t159]) ).
cnf(t287461,plain,
meet(X1,lome(X1,X2,a)) = lome(X1,X2,a),
inference(step,[status(thm)],[t22275,t15]) ).
cnf(t13514,plain,
lome(X1,a,meet(X1,X2)) = meet(X1,lome(X1,X2,a)),
inference(cp,[status(thm)],[t13513,t5229]) ).
cnf(t287330,plain,
lome(X1,a,X2) = meet(X1,lome(X1,X2,a)),
inference(step,[status(thm)],[t13514,t219]) ).
cnf(t13603,plain,
meet(X1,lome(X1,X2,a)) = lome(X1,a,X2),
inference(orient,[status(thm)],[t287330]) ).
cnf(t287462,plain,
lome(X1,a,X2) = lome(X1,X2,a),
inference(step,[status(thm)],[t287461,t13603]) ).
cnf(t22370,plain,
lome(X1,a,X2) = lome(X1,X2,a),
inference(orient,[status(thm)],[t287462]) ).
cnf(t287485,plain,
lome(lojo(X1,X2,a),X1,a) = lojo(X1,X2,a),
inference(step,[status(thm)],[t22451,t22370]) ).
cnf(t22709,plain,
lome(lojo(X1,X2,a),X1,a) = lojo(X1,X2,a),
inference(orient,[status(thm)],[t287485]) ).
cnf(t49714,plain,
X1 = lojo(X1,lome(X1,X2,X3),lojo(Y3,Y4,a)),
inference(cp,[status(thm)],[t49680,t22709]) ).
cnf(t50867,plain,
lojo(X1,lome(X1,X2,X3),lojo(Y3,Y4,a)) = X1,
inference(orient,[status(thm)],[t49714]) ).
cnf(t8071,plain,
join(X1,lojo(X1,X2,X3)) = lojo(lojo(X1,X2,X3),X1,Y3),
inference(cp,[status(thm)],[t8051,t161]) ).
cnf(t287228,plain,
lojo(X1,X2,X3) = lojo(lojo(X1,X2,X3),X1,Y3),
inference(step,[status(thm)],[t8071,t161]) ).
cnf(t8128,plain,
lojo(lojo(X1,X2,X3),X1,Y3) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t287228]) ).
cnf(t50880,plain,
X1 = lojo(X1,lome(X1,X2,X3),lojo(Y3,Y4,Y5)),
inference(cp,[status(thm)],[t50867,t8128]) ).
cnf(t51440,plain,
lojo(X1,lome(X1,X2,X3),lojo(Y3,Y4,Y5)) = X1,
inference(orient,[status(thm)],[t50880]) ).
cnf(t8058,plain,
join(meet(X1,X2),X3) = lojo(join(meet(X1,X2),X3),X1,X2),
inference(cp,[status(thm)],[t8051,t3710]) ).
cnf(t287241,plain,
join(X3,meet(X1,X2)) = lojo(join(meet(X1,X2),X3),X1,X2),
inference(step,[status(thm)],[t8058,t51]) ).
cnf(t287242,plain,
lojo(X3,X1,X2) = lojo(join(meet(X1,X2),X3),X1,X2),
inference(step,[status(thm)],[t287241,t55]) ).
cnf(t287243,plain,
lojo(X3,X1,X2) = lojo(join(X3,meet(X1,X2)),X1,X2),
inference(step,[status(thm)],[t287242,t51]) ).
cnf(t287244,plain,
lojo(X3,X1,X2) = lojo(lojo(X3,X1,X2),X1,X2),
inference(step,[status(thm)],[t287243,t55]) ).
cnf(t8489,plain,
lojo(lojo(X1,X2,X3),X2,X3) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t287244]) ).
cnf(t8511,plain,
lojo(meet(X1,X2),X1,X3) = lojo(lome(X1,X2,X3),X1,X3),
inference(cp,[status(thm)],[t8489,t80]) ).
cnf(t287245,plain,
lome(X1,X2,X3) = lojo(lome(X1,X2,X3),X1,X3),
inference(step,[status(thm)],[t8511,t80]) ).
cnf(t8528,plain,
lojo(lome(X1,X2,X3),X1,X3) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t287245]) ).
cnf(t51491,plain,
X1 = lojo(X1,lome(X1,X2,X3),lome(Y3,Y4,Y5)),
inference(cp,[status(thm)],[t51440,t8528]) ).
cnf(t51559,plain,
lojo(X1,lome(X1,X2,X3),lome(Y3,Y4,Y5)) = X1,
inference(orient,[status(thm)],[t51491]) ).
cnf(t60656,plain,
join(X1,lome(lome(X1,X2,X3),Y3,Y4)) = X1,
inference(cp,[status(thm)],[t60655,t51559]) ).
cnf(t61029,plain,
join(X1,lome(lome(X1,X2,X3),Y3,Y4)) = X1,
inference(orient,[status(thm)],[t60656]) ).
cnf(t61091,plain,
upme(X1,X2,lome(lome(X2,X3,Y3),Y4,Y5)) = lome(X1,X2,X2),
inference(cp,[status(thm)],[t28224,t61029]) ).
cnf(t288810,plain,
upme(X1,X2,lome(lome(X2,X3,Y3),Y4,Y5)) = meet(X1,X2),
inference(step,[status(thm)],[t61091,t121]) ).
cnf(t141754,plain,
upme(X1,X2,lome(lome(X2,X3,Y3),Y4,Y5)) = meet(X1,X2),
inference(orient,[status(thm)],[t288810]) ).
cnf(t535,plain,
lome(lojo(X1,X2,X3),join(X1,Y3),Y4) = lojo(upjo(X1,meet(X2,X3),Y3),lojo(X1,X2,X3),Y4),
inference(cp,[status(thm)],[t528,t396]) ).
cnf(t288418,plain,
lome(lojo(X1,X2,X3),Y4,join(X1,Y3)) = lojo(upjo(X1,meet(X2,X3),Y3),lojo(X1,X2,X3),Y4),
inference(step,[status(thm)],[t535,t59453]) ).
cnf(t288419,plain,
lome(lojo(X1,X2,X3),Y4,join(X1,Y3)) = lojo(upjo(X1,meet(X2,X3),Y3),Y4,lojo(X1,X2,X3)),
inference(step,[status(thm)],[t288418,t90]) ).
cnf(t288420,plain,
lome(lojo(X1,X2,X3),Y4,join(X1,Y3)) = lojo(upjo(X1,Y3,meet(X2,X3)),Y4,lojo(X1,X2,X3)),
inference(step,[status(thm)],[t288419,t52112]) ).
cnf(t102712,plain,
lojo(upjo(X1,X2,meet(X3,Y3)),Y4,lojo(X1,X3,Y3)) = lome(lojo(X1,X3,Y3),Y4,join(X1,X2)),
inference(orient,[status(thm)],[t288420]) ).
cnf(t102734,plain,
lome(lojo(X1,X2,X3),Y3,join(X1,X1)) = lojo(X1,Y3,lojo(X1,X2,X3)),
inference(cp,[status(thm)],[t102712,t120]) ).
cnf(t288421,plain,
lome(lojo(X1,X2,X3),Y3,X1) = lojo(X1,Y3,lojo(X1,X2,X3)),
inference(step,[status(thm)],[t102734,t110]) ).
cnf(t288422,plain,
lome(lojo(X1,X2,X3),X1,Y3) = lojo(X1,Y3,lojo(X1,X2,X3)),
inference(step,[status(thm)],[t288421,t59453]) ).
cnf(t102985,plain,
lojo(X1,X2,lojo(X1,X3,Y3)) = lome(lojo(X1,X3,Y3),X1,X2),
inference(orient,[status(thm)],[t288422]) ).
cnf(t103009,plain,
lome(lojo(X1,X2,X2),X1,X3) = lojo(X1,X3,join(X1,X2)),
inference(cp,[status(thm)],[t102985,t122]) ).
cnf(t288425,plain,
lome(join(X1,X2),X1,X3) = lojo(X1,X3,join(X1,X2)),
inference(step,[status(thm)],[t103009,t122]) ).
cnf(t103184,plain,
lojo(X1,X2,join(X1,X3)) = lome(join(X1,X3),X1,X2),
inference(orient,[status(thm)],[t288425]) ).
cnf(t288426,plain,
upjo(X1,X2,upme(X3,X1,X2)) = lome(join(X1,X2),X1,X3),
inference(step,[status(thm)],[t51718,t103184]) ).
cnf(t103185,plain,
upjo(X1,X2,upme(X3,X1,X2)) = lome(join(X1,X2),X1,X3),
inference(orient,[status(thm)],[t288426]) ).
cnf(t28238,plain,
upme(X1,meet(X1,X2),X3) = lome(X1,X2,join(meet(X1,X2),X3)),
inference(cp,[status(thm)],[t28224,t196]) ).
cnf(t287620,plain,
upme(X1,X3,meet(X1,X2)) = lome(X1,X2,join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t28238,t87]) ).
cnf(t287621,plain,
upme(X1,X3,meet(X1,X2)) = lome(X1,X2,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t287620,t51]) ).
cnf(t287622,plain,
upme(X1,X3,meet(X1,X2)) = lome(X1,X2,lojo(X3,X1,X2)),
inference(step,[status(thm)],[t287621,t55]) ).
cnf(t32986,plain,
lome(X1,X2,lojo(X3,X1,X2)) = upme(X1,X3,meet(X1,X2)),
inference(orient,[status(thm)],[t287622]) ).
cnf(t103260,plain,
upme(X1,X2,meet(X1,join(X2,X3))) = lome(X1,join(X2,X3),lome(join(X2,X3),X2,X1)),
inference(cp,[status(thm)],[t32986,t103184]) ).
cnf(t288448,plain,
upme(X1,X2,upme(X1,X2,X3)) = lome(X1,join(X2,X3),lome(join(X2,X3),X2,X1)),
inference(step,[status(thm)],[t103260,t31]) ).
cnf(t59417,plain,
meet(X1,X2) = lome(X1,X2,lome(X2,X3,Y3)),
inference(cp,[status(thm)],[t6545,t59345]) ).
cnf(t59693,plain,
lome(X1,X2,lome(X2,X3,Y3)) = meet(X1,X2),
inference(orient,[status(thm)],[t59417]) ).
cnf(t288449,plain,
upme(X1,X2,upme(X1,X2,X3)) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t288448,t59693]) ).
cnf(t288450,plain,
upme(X1,X2,upme(X1,X2,X3)) = upme(X1,X2,X3),
inference(step,[status(thm)],[t288449,t31]) ).
cnf(t104099,plain,
upme(X1,X2,upme(X1,X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288450]) ).
cnf(t104109,plain,
upme(X1,X2,X2) = upme(X1,X2,meet(X1,X2)),
inference(cp,[status(thm)],[t104099,t124]) ).
cnf(t288451,plain,
meet(X1,X2) = upme(X1,X2,meet(X1,X2)),
inference(step,[status(thm)],[t104109,t124]) ).
cnf(t104162,plain,
upme(X1,X2,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t288451]) ).
cnf(t59112,plain,
upjo(meet(X1,X2),meet(X1,X2),meet(X1,X3)) = meet(lome(X1,X2,X3),meet(X1,X2)),
inference(cp,[status(thm)],[t59109,t124]) ).
cnf(t287999,plain,
meet(X1,X2) = meet(lome(X1,X2,X3),meet(X1,X2)),
inference(step,[status(thm)],[t59112,t120]) ).
cnf(t288000,plain,
meet(X1,X2) = meet(X2,meet(lome(X1,X2,X3),X1)),
inference(step,[status(thm)],[t287999,t17]) ).
cnf(t288001,plain,
meet(X1,X2) = meet(X1,meet(X2,lome(X1,X2,X3))),
inference(step,[status(thm)],[t288000,t17]) ).
cnf(t60326,plain,
meet(X1,meet(X2,lome(X1,X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t288001]) ).
cnf(t59397,plain,
meet(X1,meet(lome(X1,X2,X3),Y3)) = meet(lome(X1,X2,X3),lome(Y3,lome(X1,X2,X3),a)),
inference(cp,[status(thm)],[t29809,t59345]) ).
cnf(t288091,plain,
meet(X1,meet(Y3,lome(X1,X2,X3))) = meet(lome(X1,X2,X3),lome(Y3,lome(X1,X2,X3),a)),
inference(step,[status(thm)],[t59397,t15]) ).
cnf(t13539,plain,
meet(X1,X2) = meet(X1,lome(X2,a,X1)),
inference(cp,[status(thm)],[t328,t13513]) ).
cnf(t13560,plain,
meet(X1,lome(X2,a,X1)) = meet(X1,X2),
inference(orient,[status(thm)],[t13539]) ).
cnf(t19486,plain,
meet(X1,lome(X2,a,X1)) = meet(X1,X2),
inference(rw,[status(thm)],[t13560]) ).
cnf(t287424,plain,
meet(X1,lome(X2,X1,a)) = meet(X1,X2),
inference(step,[status(thm)],[t19486,t19398]) ).
cnf(t19495,plain,
meet(X1,lome(X2,X1,a)) = meet(X1,X2),
inference(orient,[status(thm)],[t287424]) ).
cnf(t288092,plain,
meet(X1,meet(Y3,lome(X1,X2,X3))) = meet(lome(X1,X2,X3),Y3),
inference(step,[status(thm)],[t288091,t19495]) ).
cnf(t288093,plain,
meet(X1,meet(Y3,lome(X1,X2,X3))) = meet(Y3,lome(X1,X2,X3)),
inference(step,[status(thm)],[t288092,t15]) ).
cnf(t68487,plain,
meet(X1,meet(X2,lome(X1,X3,Y3))) = meet(X2,lome(X1,X3,Y3)),
inference(orient,[status(thm)],[t288093]) ).
cnf(t288094,plain,
meet(X2,lome(X1,X2,X3)) = meet(X1,X2),
inference(step,[status(thm)],[t60326,t68487]) ).
cnf(t68675,plain,
meet(X2,lome(X1,X2,X3)) = meet(X1,X2),
inference(rw,[status(thm)],[t288094]) ).
cnf(t68676,plain,
meet(X1,lome(X2,X1,X3)) = meet(X2,X1),
inference(orient,[status(thm)],[t68675]) ).
cnf(t104183,plain,
meet(X1,lome(X2,X1,X3)) = upme(X1,lome(X2,X1,X3),meet(X2,X1)),
inference(cp,[status(thm)],[t104162,t68676]) ).
cnf(t108381,plain,
upme(X1,meet(X2,X1),lome(X2,X1,X3)) = meet(X2,X1),
inference(orient,[status(thm)],[t104183]) ).
cnf(t108573,plain,
lome(join(meet(X1,X2),lome(X1,X2,X3)),meet(X1,X2),X2) = upjo(meet(X1,X2),lome(X1,X2,X3),meet(X1,X2)),
inference(cp,[status(thm)],[t103185,t108381]) ).
cnf(t288509,plain,
lome(join(meet(X1,X2),lome(X1,X2,X3)),X2,meet(X1,X2)) = upjo(meet(X1,X2),lome(X1,X2,X3),meet(X1,X2)),
inference(step,[status(thm)],[t108573,t59453]) ).
cnf(t288510,plain,
lome(lome(X1,X2,X3),X2,meet(X1,X2)) = upjo(meet(X1,X2),lome(X1,X2,X3),meet(X1,X2)),
inference(step,[status(thm)],[t288509,t1440]) ).
cnf(t59120,plain,
upjo(meet(X1,X2),X3,meet(X1,X2)) = upme(meet(X1,X2),X3,meet(X1,X2)),
inference(cp,[status(thm)],[t59109,t121]) ).
cnf(t288002,plain,
upjo(meet(X1,X2),X3,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t59120,t11239]) ).
cnf(t60478,plain,
upjo(meet(X1,X2),X3,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t288002]) ).
cnf(t288511,plain,
lome(lome(X1,X2,X3),X2,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t288510,t60478]) ).
cnf(t111453,plain,
lome(lome(X1,X2,X3),X2,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t288511]) ).
cnf(t111523,plain,
meet(X1,join(X2,X3)) = lome(lome(X1,join(X2,X3),Y3),join(X2,X3),upme(X1,X2,X3)),
inference(cp,[status(thm)],[t111453,t31]) ).
cnf(t288606,plain,
upme(X1,X2,X3) = lome(lome(X1,join(X2,X3),Y3),join(X2,X3),upme(X1,X2,X3)),
inference(step,[status(thm)],[t111523,t31]) ).
cnf(t68639,plain,
meet(X1,X2) = lome(X1,X2,meet(X3,lome(X2,Y3,Y4))),
inference(cp,[status(thm)],[t6545,t68487]) ).
cnf(t69136,plain,
lome(X1,X2,meet(X3,lome(X2,Y3,Y4))) = meet(X1,X2),
inference(orient,[status(thm)],[t68639]) ).
cnf(t2433,plain,
join(X1,X2) = join(join(X1,X2),upjo(X1,X2,X3)),
inference(cp,[status(thm)],[t2432,t135]) ).
cnf(t2591,plain,
join(join(X1,X2),upjo(X1,X2,X3)) = join(X1,X2),
inference(orient,[status(thm)],[t2433]) ).
cnf(t41292,plain,
join(X1,X2) = join(join(X1,X2),lojo(X1,X2,X3)),
inference(cp,[status(thm)],[t2591,t41195]) ).
cnf(t287757,plain,
join(X1,X2) = join(X1,lojo(join(X1,X2),X2,X3)),
inference(step,[status(thm)],[t41292,t424]) ).
cnf(t402,plain,
upjo(X1,meet(X1,X2),X3) = upme(X1,X1,X3),
inference(cp,[status(thm)],[t396,t86]) ).
cnf(t286845,plain,
upjo(X1,meet(X1,X2),X3) = X1,
inference(step,[status(thm)],[t402,t85]) ).
cnf(t410,plain,
upjo(X1,meet(X1,X2),X3) = X1,
inference(orient,[status(thm)],[t286845]) ).
cnf(t412,plain,
X1 = upjo(X1,upme(X1,X2,X3),Y3),
inference(cp,[status(thm)],[t410,t189]) ).
cnf(t419,plain,
upjo(X1,upme(X1,X2,X3),Y3) = X1,
inference(orient,[status(thm)],[t412]) ).
cnf(t422,plain,
join(X1,X2) = upjo(join(X1,X2),upjo(X1,X2,X3),Y3),
inference(cp,[status(thm)],[t419,t38]) ).
cnf(t2991,plain,
upjo(join(X1,X2),upjo(X1,X2,X3),Y3) = join(X1,X2),
inference(orient,[status(thm)],[t422]) ).
cnf(t3007,plain,
join(X1,X2) = upjo(join(X1,X2),X1,X3),
inference(cp,[status(thm)],[t2991,t160]) ).
cnf(t3036,plain,
upjo(join(X1,X2),X1,X3) = join(X1,X2),
inference(orient,[status(thm)],[t3007]) ).
cnf(t3043,plain,
join(X1,lojo(X1,X2,X3)) = upjo(lojo(X1,X2,X3),X1,Y3),
inference(cp,[status(thm)],[t3036,t161]) ).
cnf(t287044,plain,
lojo(X1,X2,X3) = upjo(lojo(X1,X2,X3),X1,Y3),
inference(step,[status(thm)],[t3043,t161]) ).
cnf(t3082,plain,
upjo(lojo(X1,X2,X3),X1,Y3) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t287044]) ).
cnf(t3087,plain,
lojo(join(X1,X2),X3,Y3) = join(lojo(join(X1,X2),X3,Y3),X1),
inference(cp,[status(thm)],[t3082,t2640]) ).
cnf(t287411,plain,
lojo(join(X1,X2),X3,Y3) = join(X1,lojo(join(X1,X2),X3,Y3)),
inference(step,[status(thm)],[t3087,t51]) ).
cnf(t18860,plain,
join(X1,lojo(join(X1,X2),X3,Y3)) = lojo(join(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t287411]) ).
cnf(t287758,plain,
join(X1,X2) = lojo(join(X1,X2),X2,X3),
inference(step,[status(thm)],[t287757,t18860]) ).
cnf(t41607,plain,
lojo(join(X1,X2),X2,X3) = join(X1,X2),
inference(orient,[status(thm)],[t287758]) ).
cnf(t60668,plain,
join(join(X1,X2),lome(X2,X3,Y3)) = join(X1,X2),
inference(cp,[status(thm)],[t60655,t41607]) ).
cnf(t60833,plain,
join(join(X1,X2),lome(X2,X3,Y3)) = join(X1,X2),
inference(orient,[status(thm)],[t60668]) ).
cnf(t60941,plain,
join(X1,X2) = lome(join(X1,X2),X3,join(X1,X2)),
inference(cp,[status(thm)],[t224,t60833]) ).
cnf(t60956,plain,
lome(join(X1,X2),X3,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t60941]) ).
cnf(t69188,plain,
meet(X1,join(X2,X3)) = lome(X1,join(X2,X3),meet(Y3,join(X2,X3))),
inference(cp,[status(thm)],[t69136,t60956]) ).
cnf(t288338,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),meet(Y3,join(X2,X3))),
inference(step,[status(thm)],[t69188,t31]) ).
cnf(t288339,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),upme(Y3,X2,X3)),
inference(step,[status(thm)],[t288338,t31]) ).
cnf(t91443,plain,
lome(X1,join(X2,X3),upme(Y3,X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288339]) ).
cnf(t288607,plain,
upme(X1,X2,X3) = upme(lome(X1,join(X2,X3),Y3),X2,X3),
inference(step,[status(thm)],[t288606,t91443]) ).
cnf(t288608,plain,
upme(X1,X2,X3) = upme(lome(X1,Y3,join(X2,X3)),X2,X3),
inference(step,[status(thm)],[t288607,t59453]) ).
cnf(t119228,plain,
upme(lome(X1,X2,join(X3,Y3)),X3,Y3) = upme(X1,X3,Y3),
inference(orient,[status(thm)],[t288608]) ).
cnf(t141758,plain,
meet(lome(X1,X2,join(X3,lome(lome(X3,Y3,Y4),Y5,Y6))),X3) = upme(X1,X3,lome(lome(X3,Y3,Y4),Y5,Y6)),
inference(cp,[status(thm)],[t141754,t119228]) ).
cnf(t288811,plain,
meet(lome(X1,X2,X3),X3) = upme(X1,X3,lome(lome(X3,Y3,Y4),Y5,Y6)),
inference(step,[status(thm)],[t141758,t61029]) ).
cnf(t288812,plain,
meet(lome(X1,X2,X3),X3) = meet(X1,X3),
inference(step,[status(thm)],[t288811,t141754]) ).
cnf(t288813,plain,
meet(X3,lome(X1,X2,X3)) = meet(X1,X3),
inference(step,[status(thm)],[t288812,t15]) ).
cnf(t141910,plain,
meet(X1,lome(X2,X3,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t288813]) ).
cnf(t103209,plain,
lome(join(X1,upjo(X1,X2,X3)),X1,Y3) = lojo(X1,Y3,upjo(X1,X2,X3)),
inference(cp,[status(thm)],[t103184,t52042]) ).
cnf(t288479,plain,
lome(upjo(X1,X2,X3),X1,Y3) = lojo(X1,Y3,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t103209,t52042]) ).
cnf(t106237,plain,
lojo(X1,X2,upjo(X1,X3,Y3)) = lome(upjo(X1,X3,Y3),X1,X2),
inference(orient,[status(thm)],[t288479]) ).
cnf(t33696,plain,
upme(meet(X1,join(X2,X3)),X2,Y3) = meet(X1,upjo(X2,X3,Y3)),
inference(cp,[status(thm)],[t33621,t38]) ).
cnf(t287641,plain,
upme(upme(X1,X2,X3),X2,Y3) = meet(X1,upjo(X2,X3,Y3)),
inference(step,[status(thm)],[t33696,t31]) ).
cnf(t33795,plain,
upme(upme(X1,X2,X3),X2,Y3) = meet(X1,upjo(X2,X3,Y3)),
inference(orient,[status(thm)],[t287641]) ).
cnf(t33836,plain,
meet(X1,upjo(X2,upjo(X1,X3,Y3),Y4)) = upme(X1,X2,Y4),
inference(cp,[status(thm)],[t33795,t28306]) ).
cnf(t288208,plain,
meet(X1,upjo(X2,Y4,upjo(X1,X3,Y3))) = upme(X1,X2,Y4),
inference(step,[status(thm)],[t33836,t52112]) ).
cnf(t76880,plain,
meet(X1,upjo(X2,X3,upjo(X1,Y3,Y4))) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288208]) ).
cnf(t61020,plain,
lome(join(X1,X2),X3,join(X1,X2)) = join(meet(join(X1,X2),X3),join(X1,X2)),
inference(cp,[status(thm)],[t1440,t60956]) ).
cnf(t288026,plain,
join(X1,X2) = join(meet(join(X1,X2),X3),join(X1,X2)),
inference(step,[status(thm)],[t61020,t60956]) ).
cnf(t288027,plain,
join(X1,X2) = join(X2,join(meet(join(X1,X2),X3),X1)),
inference(step,[status(thm)],[t288026,t64]) ).
cnf(t288028,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t288027,t64]) ).
cnf(t288029,plain,
join(X1,X2) = join(X1,lojo(X2,join(X1,X2),X3)),
inference(step,[status(thm)],[t288028,t55]) ).
cnf(t288030,plain,
join(X1,X2) = join(X1,lojo(X2,X3,join(X1,X2))),
inference(step,[status(thm)],[t288029,t90]) ).
cnf(t63025,plain,
join(X1,lojo(X2,X3,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t288030]) ).
cnf(t63034,plain,
join(X1,X2) = join(X1,join(X2,upjo(X1,X3,X2))),
inference(cp,[status(thm)],[t63025,t2514]) ).
cnf(t52110,plain,
join(X1,join(upjo(X1,X2,X3),Y3)) = join(Y3,upjo(X1,X2,X3)),
inference(cp,[status(thm)],[t64,t52042]) ).
cnf(t287918,plain,
join(X1,join(Y3,upjo(X1,X2,X3))) = join(Y3,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t52110,t51]) ).
cnf(t56215,plain,
join(X1,join(X2,upjo(X1,X3,Y3))) = join(X2,upjo(X1,X3,Y3)),
inference(orient,[status(thm)],[t287918]) ).
cnf(t288031,plain,
join(X1,X2) = join(X2,upjo(X1,X3,X2)),
inference(step,[status(thm)],[t63034,t56215]) ).
cnf(t288032,plain,
join(X1,X2) = join(X2,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t288031,t18119]) ).
cnf(t63133,plain,
join(X1,upjo(X2,X1,X3)) = join(X2,X1),
inference(orient,[status(thm)],[t288032]) ).
cnf(t63258,plain,
upme(X1,X2,upjo(X3,X2,Y3)) = meet(X1,join(X3,X2)),
inference(cp,[status(thm)],[t31,t63133]) ).
cnf(t288041,plain,
upme(X1,X2,upjo(X3,X2,Y3)) = upme(X1,X3,X2),
inference(step,[status(thm)],[t63258,t31]) ).
cnf(t288042,plain,
upme(X1,X2,upjo(X3,X2,Y3)) = upme(X1,X2,X3),
inference(step,[status(thm)],[t288041,t87]) ).
cnf(t63574,plain,
upme(X1,X2,upjo(X3,X2,Y3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288042]) ).
cnf(t63588,plain,
upme(join(X1,X2),X1,X3) = upjo(X1,X2,upjo(X3,X1,Y3)),
inference(cp,[status(thm)],[t63574,t38]) ).
cnf(t288045,plain,
upjo(X1,X2,X3) = upjo(X1,X2,upjo(X3,X1,Y3)),
inference(step,[status(thm)],[t63588,t38]) ).
cnf(t63645,plain,
upjo(X1,X2,upjo(X3,X1,Y3)) = upjo(X1,X2,X3),
inference(orient,[status(thm)],[t288045]) ).
cnf(t76890,plain,
upme(X1,X2,X3) = meet(X1,upjo(X2,X3,X1)),
inference(cp,[status(thm)],[t76880,t63645]) ).
cnf(t288209,plain,
upme(X1,X2,X3) = meet(X1,upjo(X2,X1,X3)),
inference(step,[status(thm)],[t76890,t52112]) ).
cnf(t77076,plain,
meet(X1,upjo(X2,X1,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288209]) ).
cnf(t77170,plain,
lojo(X1,X2,upjo(X3,X2,Y3)) = upjo(X1,X2,upme(X2,X3,Y3)),
inference(cp,[status(thm)],[t41195,t77076]) ).
cnf(t41244,plain,
lojo(X1,X2,join(X3,Y3)) = upjo(X1,X2,upme(X2,X3,Y3)),
inference(cp,[status(thm)],[t41195,t31]) ).
cnf(t44128,plain,
upjo(X1,X2,upme(X2,X3,Y3)) = lojo(X1,X2,join(X3,Y3)),
inference(orient,[status(thm)],[t41244]) ).
cnf(t288211,plain,
lojo(X1,X2,upjo(X3,X2,Y3)) = lojo(X1,X2,join(X3,Y3)),
inference(step,[status(thm)],[t77170,t44128]) ).
cnf(t77238,plain,
lojo(X1,X2,upjo(X3,X2,Y3)) = lojo(X1,X2,join(X3,Y3)),
inference(orient,[status(thm)],[t288211]) ).
cnf(t106238,plain,
lome(upjo(X1,X2,X3),X1,X2) = lojo(X1,X2,join(X1,X3)),
inference(cp,[status(thm)],[t106237,t77238]) ).
cnf(t288481,plain,
lome(upjo(X1,X2,X3),X1,X2) = lome(join(X1,X3),X1,X2),
inference(step,[status(thm)],[t106238,t103184]) ).
cnf(t106408,plain,
lome(upjo(X1,X2,X3),X1,X2) = lome(join(X1,X3),X1,X2),
inference(orient,[status(thm)],[t288481]) ).
cnf(t287479,plain,
upjo(X1,X2,upme(a,X1,X2)) = lome(join(X1,X2),X1,a),
inference(step,[status(thm)],[t20912,t22370]) ).
cnf(t22387,plain,
upjo(X1,X2,upme(a,X1,X2)) = lome(join(X1,X2),X1,a),
inference(orient,[status(thm)],[t287479]) ).
cnf(t287834,plain,
lojo(X1,a,join(X1,X2)) = lome(join(X1,X2),X1,a),
inference(step,[status(thm)],[t22387,t51718]) ).
cnf(t51867,plain,
lojo(X1,a,join(X1,X2)) = lome(join(X1,X2),X1,a),
inference(rw,[status(thm)],[t287834]) ).
cnf(t52391,plain,
lojo(X1,a,join(X1,X2)) = lome(join(X1,X2),X1,a),
inference(orient,[status(thm)],[t51867]) ).
cnf(t63220,plain,
lome(join(X1,upjo(X2,X1,X3)),X1,a) = lojo(X1,a,join(X2,X1)),
inference(cp,[status(thm)],[t52391,t63133]) ).
cnf(t288034,plain,
lome(join(X2,X1),X1,a) = lojo(X1,a,join(X2,X1)),
inference(step,[status(thm)],[t63220,t63133]) ).
cnf(t63289,plain,
lojo(X1,a,join(X2,X1)) = lome(join(X2,X1),X1,a),
inference(orient,[status(thm)],[t288034]) ).
cnf(t63380,plain,
join(X1,X2) = join(X1,lome(join(X1,X2),X2,a)),
inference(cp,[status(thm)],[t63025,t63289]) ).
cnf(t63677,plain,
join(X1,lome(join(X1,X2),X2,a)) = join(X1,X2),
inference(orient,[status(thm)],[t63380]) ).
cnf(t63707,plain,
upjo(X1,lome(join(X1,X2),X2,a),X3) = upme(join(X1,X2),X1,X3),
inference(cp,[status(thm)],[t38,t63677]) ).
cnf(t288333,plain,
upjo(X1,X3,lome(join(X1,X2),X2,a)) = upme(join(X1,X2),X1,X3),
inference(step,[status(thm)],[t63707,t52112]) ).
cnf(t288334,plain,
upjo(X1,X3,lome(join(X1,X2),X2,a)) = upjo(X1,X2,X3),
inference(step,[status(thm)],[t288333,t38]) ).
cnf(t91101,plain,
upjo(X1,X2,lome(join(X1,X3),X3,a)) = upjo(X1,X3,X2),
inference(orient,[status(thm)],[t288334]) ).
cnf(t106444,plain,
lome(join(X1,lome(join(X1,X2),X2,a)),X1,X3) = lome(upjo(X1,X2,X3),X1,X3),
inference(cp,[status(thm)],[t106408,t91101]) ).
cnf(t288482,plain,
lome(join(X1,X2),X1,X3) = lome(upjo(X1,X2,X3),X1,X3),
inference(step,[status(thm)],[t106444,t63677]) ).
cnf(t106627,plain,
lome(upjo(X1,X2,X3),X1,X3) = lome(join(X1,X2),X1,X3),
inference(orient,[status(thm)],[t288482]) ).
cnf(t142012,plain,
meet(upjo(X1,X2,X3),X3) = meet(X3,lome(join(X1,X2),X1,X3)),
inference(cp,[status(thm)],[t141910,t106627]) ).
cnf(t288818,plain,
meet(X3,upjo(X1,X2,X3)) = meet(X3,lome(join(X1,X2),X1,X3)),
inference(step,[status(thm)],[t142012,t15]) ).
cnf(t103278,plain,
upme(X1,X2,meet(X3,join(X2,Y3))) = meet(X1,lome(join(X2,Y3),X2,X3)),
inference(cp,[status(thm)],[t253,t103184]) ).
cnf(t288695,plain,
upme(X1,X2,upme(X3,X2,Y3)) = meet(X1,lome(join(X2,Y3),X2,X3)),
inference(step,[status(thm)],[t103278,t31]) ).
cnf(t129437,plain,
meet(X1,lome(join(X2,X3),X2,Y3)) = upme(X1,X2,upme(Y3,X2,X3)),
inference(orient,[status(thm)],[t288695]) ).
cnf(t288819,plain,
meet(X3,upjo(X1,X2,X3)) = upme(X3,X1,upme(X3,X1,X2)),
inference(step,[status(thm)],[t288818,t129437]) ).
cnf(t288820,plain,
meet(X3,upjo(X1,X2,X3)) = upme(X3,X1,X2),
inference(step,[status(thm)],[t288819,t104099]) ).
cnf(t142314,plain,
meet(X1,upjo(X2,X3,X1)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288820]) ).
cnf(t142572,plain,
meet(upjo(X1,X2,X3),meet(Y3,X3)) = meet(Y3,upme(X3,X1,X2)),
inference(cp,[status(thm)],[t17,t142314]) ).
cnf(t288850,plain,
meet(X3,meet(upjo(X1,X2,X3),Y3)) = meet(Y3,upme(X3,X1,X2)),
inference(step,[status(thm)],[t142572,t17]) ).
cnf(t288851,plain,
meet(X3,meet(Y3,upjo(X1,X2,X3))) = meet(Y3,upme(X3,X1,X2)),
inference(step,[status(thm)],[t288850,t15]) ).
cnf(t288852,plain,
meet(X3,meet(Y3,upjo(X1,X2,X3))) = upme(meet(Y3,X3),X1,X2),
inference(step,[status(thm)],[t288851,t33621]) ).
cnf(t288853,plain,
meet(X3,meet(Y3,upjo(X1,X2,X3))) = upme(meet(X3,Y3),X1,X2),
inference(step,[status(thm)],[t288852,t15]) ).
cnf(t145310,plain,
meet(X1,meet(X2,upjo(X3,Y3,X1))) = upme(meet(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t288853]) ).
cnf(t287465,plain,
upme(X1,X2,meet(X1,a)) = lome(X1,X2,a),
inference(step,[status(thm)],[t13513,t22370]) ).
cnf(t22373,plain,
upme(X1,X2,meet(X1,a)) = lome(X1,X2,a),
inference(orient,[status(thm)],[t287465]) ).
cnf(t33641,plain,
upme(meet(X1,X2),X3,meet(X2,a)) = meet(X1,lome(X2,X3,a)),
inference(cp,[status(thm)],[t33621,t22373]) ).
cnf(t36575,plain,
upme(meet(X1,X2),X3,meet(X2,a)) = meet(X1,lome(X2,X3,a)),
inference(orient,[status(thm)],[t33641]) ).
cnf(t36649,plain,
lome(X1,X2,meet(X3,Y3)) = lome(X1,X2,meet(X3,lome(Y3,X1,a))),
inference(cp,[status(thm)],[t355,t36575]) ).
cnf(t177652,plain,
lome(X1,X2,meet(X3,lome(Y3,X1,a))) = lome(X1,X2,meet(X3,Y3)),
inference(orient,[status(thm)],[t36649]) ).
cnf(t177681,plain,
lome(a,X1,meet(X2,X3)) = lome(a,X1,meet(X2,meet(X3,a))),
inference(cp,[status(thm)],[t177652,t121]) ).
cnf(t177723,plain,
lome(a,X1,meet(X2,meet(X3,a))) = lome(a,X1,meet(X2,X3)),
inference(orient,[status(thm)],[t177681]) ).
cnf(t8149,plain,
lojo(meet(X1,X2),X1,X3) = lojo(lome(X1,X2,X3),meet(X1,X2),Y3),
inference(cp,[status(thm)],[t8128,t80]) ).
cnf(t288127,plain,
lome(X1,X2,X3) = lojo(lome(X1,X2,X3),meet(X1,X2),Y3),
inference(step,[status(thm)],[t8149,t80]) ).
cnf(t288128,plain,
lome(X1,X2,X3) = lojo(lome(X1,X2,X3),Y3,meet(X1,X2)),
inference(step,[status(thm)],[t288127,t90]) ).
cnf(t288129,plain,
lome(X1,X2,X3) = lojo(lome(X1,X2,X3),X1,meet(Y3,X2)),
inference(step,[status(thm)],[t288128,t747]) ).
cnf(t59429,plain,
lome(X1,lome(X1,X2,X3),Y3) = lojo(lome(X1,X2,X3),X1,Y3),
inference(cp,[status(thm)],[t80,t59345]) ).
cnf(t288014,plain,
lome(X1,Y3,lome(X1,X2,X3)) = lojo(lome(X1,X2,X3),X1,Y3),
inference(step,[status(thm)],[t59429,t59453]) ).
cnf(t61927,plain,
lojo(lome(X1,X2,X3),X1,Y3) = lome(X1,Y3,lome(X1,X2,X3)),
inference(orient,[status(thm)],[t288014]) ).
cnf(t288130,plain,
lome(X1,X2,X3) = lome(X1,meet(Y3,X2),lome(X1,X2,X3)),
inference(step,[status(thm)],[t288129,t61927]) ).
cnf(t288131,plain,
lome(X1,X2,X3) = lome(X1,meet(X2,Y3),lome(X1,X2,X3)),
inference(step,[status(thm)],[t288130,t15]) ).
cnf(t71484,plain,
lome(X1,meet(X2,X3),lome(X1,X2,Y3)) = lome(X1,X2,Y3),
inference(orient,[status(thm)],[t288131]) ).
cnf(t71586,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X3),lome(X1,X2,Y3)),
inference(cp,[status(thm)],[t68676,t71484]) ).
cnf(t71735,plain,
meet(meet(X1,X2),lome(X3,X1,Y3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t71586]) ).
cnf(t71749,plain,
meet(X1,meet(X2,lome(X2,X3,Y3))) = meet(lome(X2,X3,Y3),lome(X1,X2,Y4)),
inference(cp,[status(thm)],[t71735,t59345]) ).
cnf(t2448,plain,
join(X1,X2) = upjo(join(X1,X2),X3,X1),
inference(cp,[status(thm)],[t2432,t160]) ).
cnf(t2468,plain,
upjo(join(X1,X2),X3,X1) = join(X1,X2),
inference(orient,[status(thm)],[t2448]) ).
cnf(t2475,plain,
join(meet(X1,X2),lome(X1,X2,X3)) = upjo(lome(X1,X2,X3),Y3,meet(X1,X2)),
inference(cp,[status(thm)],[t2468,t1440]) ).
cnf(t287715,plain,
lome(X1,X2,X3) = upjo(lome(X1,X2,X3),Y3,meet(X1,X2)),
inference(step,[status(thm)],[t2475,t1440]) ).
cnf(t38773,plain,
upjo(lome(X1,X2,X3),Y3,meet(X1,X2)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t287715]) ).
cnf(t38774,plain,
lome(X1,X2,X3) = join(lome(X1,X2,X3),meet(X1,X2)),
inference(cp,[status(thm)],[t38773,t135]) ).
cnf(t287716,plain,
lome(X1,X2,X3) = lojo(lome(X1,X2,X3),X1,X2),
inference(step,[status(thm)],[t38774,t55]) ).
cnf(t38877,plain,
lojo(lome(X1,X2,X3),X1,X2) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t287716]) ).
cnf(t28264,plain,
upme(X1,X2,lojo(X2,X3,Y3)) = lome(X1,X2,lojo(X2,X3,Y3)),
inference(cp,[status(thm)],[t28224,t161]) ).
cnf(t287590,plain,
upme(X1,X2,meet(X3,Y3)) = lome(X1,X2,lojo(X2,X3,Y3)),
inference(step,[status(thm)],[t28264,t546]) ).
cnf(t29585,plain,
lome(X1,X2,lojo(X2,X3,Y3)) = upme(X1,X2,meet(X3,Y3)),
inference(orient,[status(thm)],[t287590]) ).
cnf(t38899,plain,
lome(X1,X2,lojo(X2,X3,Y3)) = lojo(upme(X1,X2,meet(X3,Y3)),X1,X2),
inference(cp,[status(thm)],[t38877,t29585]) ).
cnf(t287719,plain,
upme(X1,X2,meet(X3,Y3)) = lojo(upme(X1,X2,meet(X3,Y3)),X1,X2),
inference(step,[status(thm)],[t38899,t29585]) ).
cnf(t287720,plain,
upme(X1,X2,meet(X3,Y3)) = lome(X1,join(X2,meet(X3,Y3)),X2),
inference(step,[status(thm)],[t287719,t528]) ).
cnf(t287721,plain,
upme(X1,X2,meet(X3,Y3)) = lome(X1,lojo(X2,X3,Y3),X2),
inference(step,[status(thm)],[t287720,t55]) ).
cnf(t39145,plain,
lome(X1,lojo(X2,X3,Y3),X2) = upme(X1,X2,meet(X3,Y3)),
inference(orient,[status(thm)],[t287721]) ).
cnf(t41426,plain,
upme(X1,X2,meet(X3,lome(X2,Y3,Y4))) = lome(X1,X2,X2),
inference(cp,[status(thm)],[t39145,t41310]) ).
cnf(t287783,plain,
upme(X1,X2,meet(X3,lome(X2,Y3,Y4))) = meet(X1,X2),
inference(step,[status(thm)],[t41426,t121]) ).
cnf(t46066,plain,
upme(X1,X2,meet(X3,lome(X2,Y3,Y4))) = meet(X1,X2),
inference(orient,[status(thm)],[t287783]) ).
cnf(t46073,plain,
meet(meet(X1,lome(X2,X3,Y3)),X2) = meet(X1,lome(X2,X3,Y3)),
inference(cp,[status(thm)],[t46066,t11239]) ).
cnf(t287915,plain,
meet(X2,meet(X1,lome(X2,X3,Y3))) = meet(X1,lome(X2,X3,Y3)),
inference(step,[status(thm)],[t46073,t15]) ).
cnf(t287916,plain,
meet(X1,meet(lome(X2,X3,Y3),X2)) = meet(X1,lome(X2,X3,Y3)),
inference(step,[status(thm)],[t287915,t17]) ).
cnf(t287917,plain,
meet(X1,meet(X2,lome(X2,X3,Y3))) = meet(X1,lome(X2,X3,Y3)),
inference(step,[status(thm)],[t287916,t15]) ).
cnf(t56118,plain,
meet(X1,meet(X2,lome(X2,X3,Y3))) = meet(X1,lome(X2,X3,Y3)),
inference(orient,[status(thm)],[t287917]) ).
cnf(t289163,plain,
meet(X1,lome(X2,X3,Y3)) = meet(lome(X2,X3,Y3),lome(X1,X2,Y4)),
inference(step,[status(thm)],[t71749,t56118]) ).
cnf(t289164,plain,
meet(X1,lome(X2,X3,Y3)) = meet(lome(X1,X2,Y4),lome(X2,X3,Y3)),
inference(step,[status(thm)],[t289163,t15]) ).
cnf(t188222,plain,
meet(lome(X1,X2,X3),lome(X2,Y3,Y4)) = meet(X1,lome(X2,Y3,Y4)),
inference(orient,[status(thm)],[t289164]) ).
cnf(t52048,plain,
upjo(X1,upjo(X1,X2,X3),Y3) = upme(upjo(X1,X2,X3),X1,Y3),
inference(cp,[status(thm)],[t38,t52042]) ).
cnf(t287864,plain,
upjo(X1,Y3,upjo(X1,X2,X3)) = upme(upjo(X1,X2,X3),X1,Y3),
inference(step,[status(thm)],[t52048,t52112]) ).
cnf(t53420,plain,
upjo(X1,X2,upjo(X1,X3,Y3)) = upme(upjo(X1,X3,Y3),X1,X2),
inference(orient,[status(thm)],[t287864]) ).
cnf(t63140,plain,
join(X1,X2) = join(X2,upme(upjo(X1,X3,Y3),X1,X2)),
inference(cp,[status(thm)],[t63133,t53420]) ).
cnf(t288053,plain,
join(X1,X2) = lojo(X2,upjo(X1,X3,Y3),join(X1,X2)),
inference(step,[status(thm)],[t63140,t93]) ).
cnf(t288054,plain,
join(X1,X2) = lojo(X2,join(X1,X2),upjo(X1,X3,Y3)),
inference(step,[status(thm)],[t288053,t90]) ).
cnf(t63960,plain,
lojo(X1,join(X2,X1),upjo(X2,X3,Y3)) = join(X2,X1),
inference(orient,[status(thm)],[t288054]) ).
cnf(t103030,plain,
lome(lojo(X1,join(X2,X1),upjo(X2,X3,Y3)),X1,Y4) = lojo(X1,Y4,join(X2,X1)),
inference(cp,[status(thm)],[t102985,t63960]) ).
cnf(t288435,plain,
lome(join(X2,X1),X1,Y4) = lojo(X1,Y4,join(X2,X1)),
inference(step,[status(thm)],[t103030,t63960]) ).
cnf(t103460,plain,
lojo(X1,X2,join(X3,X1)) = lome(join(X3,X1),X1,X2),
inference(orient,[status(thm)],[t288435]) ).
cnf(t288442,plain,
join(X1,lome(join(X1,X2),X2,X3)) = join(X1,X2),
inference(step,[status(thm)],[t63025,t103460]) ).
cnf(t103641,plain,
join(X1,lome(join(X1,X2),X2,X3)) = join(X1,X2),
inference(rw,[status(thm)],[t288442]) ).
cnf(t104683,plain,
join(X1,lome(join(X1,X2),X2,X3)) = join(X1,X2),
inference(orient,[status(thm)],[t103641]) ).
cnf(t33074,plain,
upme(X1,meet(X1,X2),meet(X1,X3)) = lome(X1,X3,lome(X1,X2,X3)),
inference(cp,[status(thm)],[t32986,t80]) ).
cnf(t287623,plain,
meet(X1,lome(X1,X2,X3)) = lome(X1,X3,lome(X1,X2,X3)),
inference(step,[status(thm)],[t33074,t5229]) ).
cnf(t33110,plain,
lome(X1,X2,lome(X1,X3,X2)) = meet(X1,lome(X1,X3,X2)),
inference(orient,[status(thm)],[t287623]) ).
cnf(t8074,plain,
join(meet(X1,X2),lome(X1,X2,X3)) = lojo(lome(X1,X2,X3),meet(X1,X2),Y3),
inference(cp,[status(thm)],[t8051,t1440]) ).
cnf(t287934,plain,
lome(X1,X2,X3) = lojo(lome(X1,X2,X3),meet(X1,X2),Y3),
inference(step,[status(thm)],[t8074,t1440]) ).
cnf(t287935,plain,
lome(X1,X2,X3) = lojo(lome(X1,X2,X3),Y3,meet(X1,X2)),
inference(step,[status(thm)],[t287934,t90]) ).
cnf(t287936,plain,
lome(X1,X2,X3) = lojo(lome(X1,X2,X3),X1,meet(Y3,X2)),
inference(step,[status(thm)],[t287935,t747]) ).
cnf(t287937,plain,
lome(X1,X2,X3) = lojo(lome(X1,X2,X3),X1,meet(X2,Y3)),
inference(step,[status(thm)],[t287936,t15]) ).
cnf(t57340,plain,
lojo(lome(X1,X2,X3),X1,meet(X2,Y3)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t287937]) ).
cnf(t57348,plain,
lome(X1,X2,join(X2,X3)) = lojo(upme(X1,X2,X3),X1,meet(X2,Y3)),
inference(cp,[status(thm)],[t57340,t28224]) ).
cnf(t287938,plain,
upme(X1,X2,X3) = lojo(upme(X1,X2,X3),X1,meet(X2,Y3)),
inference(step,[status(thm)],[t57348,t28224]) ).
cnf(t287939,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),meet(X2,Y3)),
inference(step,[status(thm)],[t287938,t528]) ).
cnf(t57445,plain,
lome(X1,join(X2,X3),meet(X2,Y3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t287939]) ).
cnf(t57528,plain,
meet(X1,lome(X1,join(X2,X3),meet(X2,Y3))) = lome(X1,meet(X2,Y3),upme(X1,X2,X3)),
inference(cp,[status(thm)],[t33110,t57445]) ).
cnf(t287943,plain,
meet(X1,upme(X1,X2,X3)) = lome(X1,meet(X2,Y3),upme(X1,X2,X3)),
inference(step,[status(thm)],[t57528,t57445]) ).
cnf(t287944,plain,
upme(meet(X1,X1),X2,X3) = lome(X1,meet(X2,Y3),upme(X1,X2,X3)),
inference(step,[status(thm)],[t287943,t33621]) ).
cnf(t287945,plain,
upme(X1,X2,X3) = lome(X1,meet(X2,Y3),upme(X1,X2,X3)),
inference(step,[status(thm)],[t287944,t127]) ).
cnf(t287946,plain,
upme(X1,X2,X3) = lome(X1,meet(X2,Y3),join(X2,X3)),
inference(step,[status(thm)],[t287945,t576]) ).
cnf(t57710,plain,
lome(X1,meet(X2,X3),join(X2,Y3)) = upme(X1,X2,Y3),
inference(orient,[status(thm)],[t287946]) ).
cnf(t104727,plain,
join(X1,meet(X2,X3)) = join(X1,upme(join(X1,meet(X2,X3)),X2,Y3)),
inference(cp,[status(thm)],[t104683,t57710]) ).
cnf(t288579,plain,
lojo(X1,X2,X3) = join(X1,upme(join(X1,meet(X2,X3)),X2,Y3)),
inference(step,[status(thm)],[t104727,t55]) ).
cnf(t288580,plain,
lojo(X1,X2,X3) = lojo(X1,join(X1,meet(X2,X3)),join(X2,Y3)),
inference(step,[status(thm)],[t288579,t93]) ).
cnf(t288581,plain,
lojo(X1,X2,X3) = lojo(X1,join(X2,Y3),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t288580,t90]) ).
cnf(t288582,plain,
lojo(X1,X2,X3) = lome(join(X1,meet(X2,X3)),X1,join(X2,Y3)),
inference(step,[status(thm)],[t288581,t103184]) ).
cnf(t288583,plain,
lojo(X1,X2,X3) = lome(lojo(X1,X2,X3),X1,join(X2,Y3)),
inference(step,[status(thm)],[t288582,t55]) ).
cnf(t117427,plain,
lome(lojo(X1,X2,X3),X1,join(X2,Y3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t288583]) ).
cnf(t103466,plain,
lome(join(X1,X2),X2,X2) = X2,
inference(cp,[status(thm)],[t103460,t86]) ).
cnf(t288443,plain,
meet(join(X1,X2),X2) = X2,
inference(step,[status(thm)],[t103466,t121]) ).
cnf(t288444,plain,
meet(X2,join(X1,X2)) = X2,
inference(step,[status(thm)],[t288443,t15]) ).
cnf(t288445,plain,
upme(X2,X1,X2) = X2,
inference(step,[status(thm)],[t288444,t31]) ).
cnf(t103642,plain,
upme(X1,X2,X1) = X1,
inference(orient,[status(thm)],[t288445]) ).
cnf(t103678,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),X3),
inference(cp,[status(thm)],[t91443,t103642]) ).
cnf(t288446,plain,
upme(X1,X2,X3) = lome(X1,X3,join(X2,X3)),
inference(step,[status(thm)],[t103678,t59453]) ).
cnf(t103717,plain,
lome(X1,X2,join(X3,X2)) = upme(X1,X3,X2),
inference(orient,[status(thm)],[t288446]) ).
cnf(t103803,plain,
lome(X1,X2,join(X3,X2)) = lome(X1,meet(X2,Y3),upme(X1,X3,X2)),
inference(cp,[status(thm)],[t71484,t103717]) ).
cnf(t288463,plain,
upme(X1,X3,X2) = lome(X1,meet(X2,Y3),upme(X1,X3,X2)),
inference(step,[status(thm)],[t103803,t103717]) ).
cnf(t288464,plain,
upme(X1,X3,X2) = lome(X1,meet(X2,Y3),join(X3,X2)),
inference(step,[status(thm)],[t288463,t576]) ).
cnf(t105381,plain,
lome(X1,meet(X2,X3),join(Y3,X2)) = upme(X1,Y3,X2),
inference(orient,[status(thm)],[t288464]) ).
cnf(t117429,plain,
lojo(meet(X1,X2),X3,Y3) = upme(lojo(meet(X1,X2),X3,Y3),X3,X1),
inference(cp,[status(thm)],[t117427,t105381]) ).
cnf(t289336,plain,
lojo(meet(X1,X2),X3,Y3) = upme(lojo(meet(X1,X2),X3,Y3),X1,X3),
inference(step,[status(thm)],[t117429,t87]) ).
cnf(t209175,plain,
upme(lojo(meet(X1,X2),X3,Y3),X1,X3) = lojo(meet(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t289336]) ).
cnf(t209305,plain,
lojo(meet(X1,lome(X2,X3,X1)),Y3,Y4) = upme(lojo(meet(X2,X1),Y3,Y4),X1,Y3),
inference(cp,[status(thm)],[t209175,t141910]) ).
cnf(t289658,plain,
lojo(meet(X2,X1),Y3,Y4) = upme(lojo(meet(X2,X1),Y3,Y4),X1,Y3),
inference(step,[status(thm)],[t209305,t141910]) ).
cnf(t251946,plain,
upme(lojo(meet(X1,X2),X3,Y3),X2,X3) = lojo(meet(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t289658]) ).
cnf(t251947,plain,
lojo(meet(X1,X2),X2,X3) = meet(lojo(meet(X1,X2),X2,X3),X2),
inference(cp,[status(thm)],[t251946,t124]) ).
cnf(t289659,plain,
lojo(meet(X1,X2),X2,X3) = meet(X2,lojo(meet(X1,X2),X2,X3)),
inference(step,[status(thm)],[t251947,t15]) ).
cnf(t289660,plain,
lojo(meet(X1,X2),X2,X3) = upme(X2,meet(X1,X2),meet(X2,X3)),
inference(step,[status(thm)],[t289659,t253]) ).
cnf(t252210,plain,
upme(X1,meet(X2,X1),meet(X1,X3)) = lojo(meet(X2,X1),X1,X3),
inference(orient,[status(thm)],[t289660]) ).
cnf(t252291,plain,
lojo(meet(X1,X2),X2,X2) = upme(X2,meet(X1,X2),X2),
inference(cp,[status(thm)],[t252210,t127]) ).
cnf(t289661,plain,
join(meet(X1,X2),X2) = upme(X2,meet(X1,X2),X2),
inference(step,[status(thm)],[t252291,t122]) ).
cnf(t289662,plain,
join(X2,meet(X1,X2)) = upme(X2,meet(X1,X2),X2),
inference(step,[status(thm)],[t289661,t51]) ).
cnf(t289663,plain,
lojo(X2,X1,X2) = upme(X2,meet(X1,X2),X2),
inference(step,[status(thm)],[t289662,t55]) ).
cnf(t289664,plain,
lojo(X2,X1,X2) = X2,
inference(step,[status(thm)],[t289663,t103642]) ).
cnf(t252519,plain,
lojo(X1,X2,X1) = X1,
inference(orient,[status(thm)],[t289664]) ).
cnf(t252630,plain,
lojo(upme(meet(X1,a),X2,meet(X2,a)),X2,meet(X2,a)) = upme(meet(X2,a),X2,meet(X1,meet(meet(X2,a),a))),
inference(cp,[status(thm)],[t305,t252519]) ).
cnf(t289675,plain,
lojo(upme(meet(X1,a),X2,meet(X2,a)),X2,a) = upme(meet(X2,a),X2,meet(X1,meet(meet(X2,a),a))),
inference(step,[status(thm)],[t252630,t207]) ).
cnf(t287099,plain,
upme(a,X1,meet(X2,a)) = lome(a,X1,X2),
inference(step,[status(thm)],[t1253,t4492]) ).
cnf(t4493,plain,
upme(a,X1,meet(X2,a)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t287099]) ).
cnf(t33681,plain,
upme(meet(X1,a),X2,meet(X3,a)) = meet(X1,lome(a,X2,X3)),
inference(cp,[status(thm)],[t33621,t4493]) ).
cnf(t36664,plain,
upme(meet(X1,a),X2,meet(X3,a)) = meet(X1,lome(a,X2,X3)),
inference(orient,[status(thm)],[t33681]) ).
cnf(t289676,plain,
lojo(meet(X1,lome(a,X2,X2)),X2,a) = upme(meet(X2,a),X2,meet(X1,meet(meet(X2,a),a))),
inference(step,[status(thm)],[t289675,t36664]) ).
cnf(t289677,plain,
lojo(meet(X1,meet(a,X2)),X2,a) = upme(meet(X2,a),X2,meet(X1,meet(meet(X2,a),a))),
inference(step,[status(thm)],[t289676,t121]) ).
cnf(t289678,plain,
lojo(meet(X1,meet(X2,a)),X2,a) = upme(meet(X2,a),X2,meet(X1,meet(meet(X2,a),a))),
inference(step,[status(thm)],[t289677,t15]) ).
cnf(t46255,plain,
join(X1,meet(X2,X3)) = join(X1,lome(X2,X3,lome(X1,Y3,Y4))),
inference(cp,[status(thm)],[t46243,t80]) ).
cnf(t288258,plain,
lojo(X1,X2,X3) = join(X1,lome(X2,X3,lome(X1,Y3,Y4))),
inference(step,[status(thm)],[t46255,t55]) ).
cnf(t81115,plain,
join(X1,lome(X2,X3,lome(X1,Y3,Y4))) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t288258]) ).
cnf(t11915,plain,
lojo(X1,meet(X2,X3),join(X2,Y3)) = lojo(X1,meet(X2,X3),meet(X2,X3)),
inference(cp,[status(thm)],[t558,t11881]) ).
cnf(t287303,plain,
lojo(X1,meet(X2,X3),join(X2,Y3)) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t11915,t122]) ).
cnf(t287304,plain,
lojo(X1,meet(X2,X3),join(X2,Y3)) = lojo(X1,X2,X3),
inference(step,[status(thm)],[t287303,t55]) ).
cnf(t12058,plain,
lojo(X1,meet(X2,X3),join(X2,Y3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t287304]) ).
cnf(t68817,plain,
lojo(X1,X2,lome(X3,X2,Y3)) = lojo(X1,meet(X3,X2),join(X2,Y4)),
inference(cp,[status(thm)],[t12058,t68676]) ).
cnf(t288097,plain,
lojo(X1,X2,lome(X3,X2,Y3)) = lojo(X1,X3,X2),
inference(step,[status(thm)],[t68817,t29733]) ).
cnf(t288098,plain,
lojo(X1,X2,lome(X3,X2,Y3)) = lojo(X1,X2,X3),
inference(step,[status(thm)],[t288097,t90]) ).
cnf(t68867,plain,
lojo(X1,X2,lome(X3,X2,Y3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t288098]) ).
cnf(t68883,plain,
lojo(meet(X1,X2),X1,X3) = lome(X1,X2,lome(X3,X1,Y3)),
inference(cp,[status(thm)],[t68867,t80]) ).
cnf(t288099,plain,
lome(X1,X2,X3) = lome(X1,X2,lome(X3,X1,Y3)),
inference(step,[status(thm)],[t68883,t80]) ).
cnf(t68922,plain,
lome(X1,X2,lome(X3,X1,Y3)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t288099]) ).
cnf(t81122,plain,
lojo(X1,X2,X3) = join(X1,lome(X2,X3,X1)),
inference(cp,[status(thm)],[t81115,t68922]) ).
cnf(t288259,plain,
lojo(X1,X2,X3) = join(X1,lome(X2,X1,X3)),
inference(step,[status(thm)],[t81122,t59453]) ).
cnf(t81316,plain,
join(X1,lome(X2,X1,X3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t288259]) ).
cnf(t81394,plain,
upjo(X1,lome(X2,X1,X3),Y3) = upme(lojo(X1,X2,X3),X1,Y3),
inference(cp,[status(thm)],[t38,t81316]) ).
cnf(t288261,plain,
upjo(X1,Y3,lome(X2,X1,X3)) = upme(lojo(X1,X2,X3),X1,Y3),
inference(step,[status(thm)],[t81394,t52112]) ).
cnf(t287841,plain,
upme(lojo(X1,X2,X3),X1,Y3) = upjo(X1,Y3,meet(X2,X3)),
inference(step,[status(thm)],[t396,t52112]) ).
cnf(t52113,plain,
upme(lojo(X1,X2,X3),X1,Y3) = upjo(X1,Y3,meet(X2,X3)),
inference(orient,[status(thm)],[t287841]) ).
cnf(t288262,plain,
upjo(X1,Y3,lome(X2,X1,X3)) = upjo(X1,Y3,meet(X2,X3)),
inference(step,[status(thm)],[t288261,t52113]) ).
cnf(t81486,plain,
upjo(X1,X2,lome(X3,X1,Y3)) = upjo(X1,X2,meet(X3,Y3)),
inference(orient,[status(thm)],[t288262]) ).
cnf(t63041,plain,
join(X1,meet(X2,X3)) = join(X1,lome(X2,X3,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t63025,t80]) ).
cnf(t288035,plain,
lojo(X1,X2,X3) = join(X1,lome(X2,X3,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t63041,t55]) ).
cnf(t288036,plain,
lojo(X1,X2,X3) = join(X1,lome(X2,X3,lojo(X1,X2,X3))),
inference(step,[status(thm)],[t288035,t55]) ).
cnf(t288037,plain,
lojo(X1,X2,X3) = join(X1,upme(X2,X1,meet(X2,X3))),
inference(step,[status(thm)],[t288036,t32986]) ).
cnf(t288038,plain,
lojo(X1,X2,X3) = lojo(X1,X2,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t288037,t93]) ).
cnf(t288039,plain,
lojo(X1,X2,X3) = lojo(X1,X2,lojo(X1,X2,X3)),
inference(step,[status(thm)],[t288038,t55]) ).
cnf(t63409,plain,
lojo(X1,X2,lojo(X1,X2,X3)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t288039]) ).
cnf(t288423,plain,
lome(lojo(X1,X2,X3),X1,X2) = lojo(X1,X2,X3),
inference(step,[status(thm)],[t63409,t102985]) ).
cnf(t103182,plain,
lome(lojo(X1,X2,X3),X1,X2) = lojo(X1,X2,X3),
inference(rw,[status(thm)],[t288423]) ).
cnf(t103949,plain,
lome(lojo(X1,X2,X3),X1,X2) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t103182]) ).
cnf(t104030,plain,
upjo(X1,X2,meet(lojo(X1,X3,Y3),X3)) = upjo(X1,X2,lojo(X1,X3,Y3)),
inference(cp,[status(thm)],[t81486,t103949]) ).
cnf(t289270,plain,
upjo(X1,X2,meet(X3,lojo(X1,X3,Y3))) = upjo(X1,X2,lojo(X1,X3,Y3)),
inference(step,[status(thm)],[t104030,t15]) ).
cnf(t289271,plain,
upjo(X1,X2,upme(X3,X1,meet(X3,Y3))) = upjo(X1,X2,lojo(X1,X3,Y3)),
inference(step,[status(thm)],[t289270,t253]) ).
cnf(t289272,plain,
upjo(X1,X2,upme(X3,X1,meet(X3,Y3))) = upjo(X1,X2,meet(X3,Y3)),
inference(step,[status(thm)],[t289271,t572]) ).
cnf(t200687,plain,
upjo(X1,X2,upme(X3,X1,meet(X3,Y3))) = upjo(X1,X2,meet(X3,Y3)),
inference(orient,[status(thm)],[t289272]) ).
cnf(t200730,plain,
upjo(X1,X2,meet(X3,lome(Y3,Y4,X3))) = upjo(X1,X2,upme(X3,X1,meet(Y3,X3))),
inference(cp,[status(thm)],[t200687,t141910]) ).
cnf(t289552,plain,
upjo(X1,X2,meet(Y3,X3)) = upjo(X1,X2,upme(X3,X1,meet(Y3,X3))),
inference(step,[status(thm)],[t200730,t141910]) ).
cnf(t235682,plain,
upjo(X1,X2,upme(X3,X1,meet(Y3,X3))) = upjo(X1,X2,meet(Y3,X3)),
inference(orient,[status(thm)],[t289552]) ).
cnf(t235683,plain,
upjo(X1,meet(X2,X3),meet(X2,X3)) = lome(join(X1,meet(X2,X3)),X1,X3),
inference(cp,[status(thm)],[t235682,t103185]) ).
cnf(t289553,plain,
join(X1,meet(X2,X3)) = lome(join(X1,meet(X2,X3)),X1,X3),
inference(step,[status(thm)],[t235683,t135]) ).
cnf(t289554,plain,
lojo(X1,X2,X3) = lome(join(X1,meet(X2,X3)),X1,X3),
inference(step,[status(thm)],[t289553,t55]) ).
cnf(t289555,plain,
lojo(X1,X2,X3) = lome(lojo(X1,X2,X3),X1,X3),
inference(step,[status(thm)],[t289554,t55]) ).
cnf(t235847,plain,
lome(lojo(X1,X2,X3),X1,X3) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t289555]) ).
cnf(t235852,plain,
lojo(X1,X2,join(X3,X1)) = upme(lojo(X1,X2,join(X3,X1)),X3,X1),
inference(cp,[status(thm)],[t235847,t103717]) ).
cnf(t289556,plain,
lome(join(X3,X1),X1,X2) = upme(lojo(X1,X2,join(X3,X1)),X3,X1),
inference(step,[status(thm)],[t235852,t103460]) ).
cnf(t104699,plain,
join(X1,X2) = join(X1,upme(join(X1,X2),X3,X2)),
inference(cp,[status(thm)],[t104683,t103717]) ).
cnf(t288458,plain,
join(X1,X2) = lojo(X1,join(X1,X2),join(X3,X2)),
inference(step,[status(thm)],[t104699,t93]) ).
cnf(t288459,plain,
join(X1,X2) = lojo(X1,join(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t288458,t51]) ).
cnf(t105004,plain,
lojo(X1,join(X1,X2),join(X2,X3)) = join(X1,X2),
inference(orient,[status(thm)],[t288459]) ).
cnf(t105009,plain,
join(X1,X2) = lojo(X1,join(X2,X3),join(X1,X2)),
inference(cp,[status(thm)],[t105004,t90]) ).
cnf(t288460,plain,
join(X1,X2) = lome(join(X1,X2),X1,join(X2,X3)),
inference(step,[status(thm)],[t105009,t103184]) ).
cnf(t105163,plain,
lome(join(X1,X2),X1,join(X2,X3)) = join(X1,X2),
inference(orient,[status(thm)],[t288460]) ).
cnf(t46244,plain,
join(X1,join(X1,X2)) = lojo(join(X1,X2),X3,lome(X1,Y3,Y4)),
inference(cp,[status(thm)],[t46243,t18860]) ).
cnf(t287802,plain,
join(X1,X2) = lojo(join(X1,X2),X3,lome(X1,Y3,Y4)),
inference(step,[status(thm)],[t46244,t136]) ).
cnf(t47961,plain,
lojo(join(X1,X2),X3,lome(X1,Y3,Y4)) = join(X1,X2),
inference(orient,[status(thm)],[t287802]) ).
cnf(t47964,plain,
join(X1,X2) = join(join(X1,X2),lome(X1,X3,Y3)),
inference(cp,[status(thm)],[t47961,t122]) ).
cnf(t48136,plain,
join(join(X1,X2),lome(X1,X3,Y3)) = join(X1,X2),
inference(orient,[status(thm)],[t47964]) ).
cnf(t48142,plain,
join(X1,lojo(X1,X2,X3)) = join(lojo(X1,X2,X3),lome(X1,Y3,Y4)),
inference(cp,[status(thm)],[t48136,t161]) ).
cnf(t288281,plain,
lojo(X1,X2,X3) = join(lojo(X1,X2,X3),lome(X1,Y3,Y4)),
inference(step,[status(thm)],[t48142,t161]) ).
cnf(t288282,plain,
lojo(X1,X2,X3) = join(lome(X1,Y3,Y4),lojo(X1,X2,X3)),
inference(step,[status(thm)],[t288281,t51]) ).
cnf(t288283,plain,
lojo(X1,X2,X3) = join(X1,lojo(lome(X1,Y3,Y4),X2,X3)),
inference(step,[status(thm)],[t288282,t424]) ).
cnf(t85135,plain,
join(X1,lojo(lome(X1,X2,X3),Y3,Y4)) = lojo(X1,Y3,Y4),
inference(orient,[status(thm)],[t288283]) ).
cnf(t85193,plain,
lojo(X1,X2,X3) = join(X1,lojo(upme(X1,Y3,Y4),X2,X3)),
inference(cp,[status(thm)],[t85135,t28224]) ).
cnf(t97684,plain,
join(X1,lojo(upme(X1,X2,X3),Y3,Y4)) = lojo(X1,Y3,Y4),
inference(orient,[status(thm)],[t85193]) ).
cnf(t105211,plain,
join(X1,X2) = lome(join(X1,X2),X1,lojo(X2,X3,Y3)),
inference(cp,[status(thm)],[t105163,t97684]) ).
cnf(t109736,plain,
lome(join(X1,X2),X1,lojo(X2,X3,Y3)) = join(X1,X2),
inference(orient,[status(thm)],[t105211]) ).
cnf(t142008,plain,
meet(join(X1,X2),lojo(X2,X3,Y3)) = meet(lojo(X2,X3,Y3),join(X1,X2)),
inference(cp,[status(thm)],[t141910,t109736]) ).
cnf(t288870,plain,
upme(join(X1,X2),X2,meet(X3,Y3)) = meet(lojo(X2,X3,Y3),join(X1,X2)),
inference(step,[status(thm)],[t142008,t253]) ).
cnf(t288871,plain,
upme(join(X1,X2),X2,meet(X3,Y3)) = upme(lojo(X2,X3,Y3),X1,X2),
inference(step,[status(thm)],[t288870,t31]) ).
cnf(t146801,plain,
upme(join(X1,X2),X2,meet(X3,Y3)) = upme(lojo(X2,X3,Y3),X1,X2),
inference(orient,[status(thm)],[t288871]) ).
cnf(t119259,plain,
upme(upjo(X1,X2,join(X3,Y3)),X3,Y3) = upme(lome(join(X1,X2),X1,join(X3,Y3)),X3,Y3),
inference(cp,[status(thm)],[t119228,t106627]) ).
cnf(t289337,plain,
upme(upjo(X1,X2,join(X3,Y3)),X3,Y3) = upme(join(X1,X2),X3,Y3),
inference(step,[status(thm)],[t119259,t119228]) ).
cnf(t209410,plain,
upme(upjo(X1,X2,join(X3,Y3)),X3,Y3) = upme(join(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t289337]) ).
cnf(t28303,plain,
meet(X1,X2) = lome(meet(X1,X2),X3,upme(X1,X2,Y3)),
inference(cp,[status(thm)],[t1853,t28224]) ).
cnf(t30467,plain,
lome(meet(X1,X2),X3,upme(X1,X2,Y3)) = meet(X1,X2),
inference(orient,[status(thm)],[t28303]) ).
cnf(t59392,plain,
meet(X1,lome(X1,X2,X3)) = lome(lome(X1,X2,X3),Y3,upme(X1,lome(X1,X2,X3),Y4)),
inference(cp,[status(thm)],[t30467,t59345]) ).
cnf(t287990,plain,
lome(X1,X2,X3) = lome(lome(X1,X2,X3),Y3,upme(X1,lome(X1,X2,X3),Y4)),
inference(step,[status(thm)],[t59392,t59345]) ).
cnf(t287991,plain,
lome(X1,X2,X3) = lome(lome(X1,X2,X3),Y3,X1),
inference(step,[status(thm)],[t287990,t355]) ).
cnf(t287992,plain,
lome(X1,X2,X3) = lome(lome(X1,X2,X3),X1,Y3),
inference(step,[status(thm)],[t287991,t59453]) ).
cnf(t60066,plain,
lome(lome(X1,X2,X3),X1,Y3) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t287992]) ).
cnf(t60108,plain,
meet(X1,meet(X2,lome(X2,X3,Y3))) = meet(meet(X1,X2),lome(X2,X3,Y3)),
inference(cp,[status(thm)],[t29809,t60066]) ).
cnf(t288106,plain,
meet(X1,lome(X2,X3,Y3)) = meet(meet(X1,X2),lome(X2,X3,Y3)),
inference(step,[status(thm)],[t60108,t56118]) ).
cnf(t69294,plain,
meet(meet(X1,X2),lome(X2,X3,Y3)) = meet(X1,lome(X2,X3,Y3)),
inference(orient,[status(thm)],[t288106]) ).
cnf(t69297,plain,
meet(X1,lome(X2,meet(X1,X2),X3)) = meet(X2,meet(X1,X2)),
inference(cp,[status(thm)],[t69294,t68676]) ).
cnf(t288107,plain,
meet(X1,lome(X2,X3,meet(X1,X2))) = meet(X2,meet(X1,X2)),
inference(step,[status(thm)],[t69297,t19398]) ).
cnf(t288108,plain,
meet(X1,lome(X2,X3,meet(X1,X2))) = meet(X1,meet(X2,X2)),
inference(step,[status(thm)],[t288107,t17]) ).
cnf(t288109,plain,
meet(X1,lome(X2,X3,meet(X1,X2))) = meet(X1,X2),
inference(step,[status(thm)],[t288108,t127]) ).
cnf(t69516,plain,
meet(X1,lome(X2,X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t288109]) ).
cnf(t33764,plain,
lojo(X1,X2,upme(X3,Y3,Y4)) = join(X1,upme(meet(X2,X3),Y3,Y4)),
inference(cp,[status(thm)],[t55,t33621]) ).
cnf(t288411,plain,
lojo(X1,X2,upme(X3,Y3,Y4)) = lojo(X1,meet(X2,X3),join(Y3,Y4)),
inference(step,[status(thm)],[t33764,t93]) ).
cnf(t100724,plain,
lojo(X1,meet(X2,X3),join(Y3,Y4)) = lojo(X1,X2,upme(X3,Y3,Y4)),
inference(orient,[status(thm)],[t288411]) ).
cnf(t103469,plain,
lome(join(X1,X2),X2,meet(X3,Y3)) = lojo(X2,X3,upme(Y3,X1,X2)),
inference(cp,[status(thm)],[t103460,t100724]) ).
cnf(t131495,plain,
lome(join(X1,X2),X2,meet(X3,Y3)) = lojo(X2,X3,upme(Y3,X1,X2)),
inference(orient,[status(thm)],[t103469]) ).
cnf(t131694,plain,
meet(X1,join(X2,X3)) = meet(X1,lojo(X3,X1,upme(join(X2,X3),X2,X3))),
inference(cp,[status(thm)],[t69516,t131495]) ).
cnf(t288733,plain,
upme(X1,X2,X3) = meet(X1,lojo(X3,X1,upme(join(X2,X3),X2,X3))),
inference(step,[status(thm)],[t131694,t31]) ).
cnf(t288734,plain,
upme(X1,X2,X3) = upme(X1,X3,meet(X1,upme(join(X2,X3),X2,X3))),
inference(step,[status(thm)],[t288733,t253]) ).
cnf(t288735,plain,
upme(X1,X2,X3) = upme(X1,X3,upme(meet(X1,join(X2,X3)),X2,X3)),
inference(step,[status(thm)],[t288734,t33621]) ).
cnf(t288736,plain,
upme(X1,X2,X3) = upme(X1,X3,upme(upme(X1,X2,X3),X2,X3)),
inference(step,[status(thm)],[t288735,t31]) ).
cnf(t288737,plain,
upme(X1,X2,X3) = upme(X1,X3,meet(X1,upjo(X2,X3,X3))),
inference(step,[status(thm)],[t288736,t33795]) ).
cnf(t288738,plain,
upme(X1,X2,X3) = upme(X1,X3,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t288737,t135]) ).
cnf(t288739,plain,
upme(X1,X2,X3) = upme(X1,X3,upme(X1,X2,X3)),
inference(step,[status(thm)],[t288738,t31]) ).
cnf(t131976,plain,
upme(X1,X2,upme(X1,X3,X2)) = upme(X1,X3,X2),
inference(orient,[status(thm)],[t288739]) ).
cnf(t38900,plain,
lome(X1,X2,lome(X1,X3,X2)) = lojo(meet(X1,lome(X1,X3,X2)),X1,X2),
inference(cp,[status(thm)],[t38877,t33110]) ).
cnf(t287722,plain,
meet(X1,lome(X1,X3,X2)) = lojo(meet(X1,lome(X1,X3,X2)),X1,X2),
inference(step,[status(thm)],[t38900,t33110]) ).
cnf(t287723,plain,
meet(X1,lome(X1,X3,X2)) = lome(X1,lome(X1,X3,X2),X2),
inference(step,[status(thm)],[t287722,t80]) ).
cnf(t39336,plain,
lome(X1,lome(X1,X2,X3),X3) = meet(X1,lome(X1,X2,X3)),
inference(orient,[status(thm)],[t287723]) ).
cnf(t287976,plain,
lome(X1,lome(X1,X2,X3),X3) = lome(X1,X2,X3),
inference(step,[status(thm)],[t39336,t59345]) ).
cnf(t59348,plain,
lome(X1,lome(X1,X2,X3),X3) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t287976]) ).
cnf(t59632,plain,
lome(X1,lome(X1,X2,X3),X3) = lome(X1,X2,X3),
inference(rw,[status(thm)],[t59348]) ).
cnf(t287994,plain,
lome(X1,X3,lome(X1,X2,X3)) = lome(X1,X2,X3),
inference(step,[status(thm)],[t59632,t59453]) ).
cnf(t60186,plain,
lome(X1,X2,lome(X1,X3,X2)) = lome(X1,X3,X2),
inference(orient,[status(thm)],[t287994]) ).
cnf(t60292,plain,
lome(X1,X2,lome(X1,X3,X2)) = join(meet(X1,X2),lome(X1,X3,X2)),
inference(cp,[status(thm)],[t1440,t60186]) ).
cnf(t288012,plain,
lome(X1,X3,X2) = join(meet(X1,X2),lome(X1,X3,X2)),
inference(step,[status(thm)],[t60292,t60186]) ).
cnf(t61682,plain,
join(meet(X1,X2),lome(X1,X3,X2)) = lome(X1,X3,X2),
inference(orient,[status(thm)],[t288012]) ).
cnf(t61819,plain,
join(meet(X1,X2),lome(X1,X3,X2)) = lojo(lome(X1,X3,X2),meet(X1,X2),Y3),
inference(cp,[status(thm)],[t8051,t61682]) ).
cnf(t90086,plain,
lome(X1,meet(X2,X3),lome(X1,Y3,X2)) = lome(X1,Y3,X2),
inference(orient,[status(thm)],[t61819]) ).
cnf(t8777,plain,
X1 = lome(X1,lojo(lojo(X1,X2,X3),Y3,Y4),Y5),
inference(cp,[status(thm)],[t8754,t161]) ).
cnf(t12877,plain,
lome(X1,lojo(lojo(X1,X2,X3),Y3,Y4),Y5) = X1,
inference(orient,[status(thm)],[t8777]) ).
cnf(t12878,plain,
X1 = meet(X1,lojo(lojo(X1,X2,X3),Y3,Y4)),
inference(cp,[status(thm)],[t12877,t121]) ).
cnf(t287318,plain,
X1 = upme(X1,lojo(X1,X2,X3),meet(Y3,Y4)),
inference(step,[status(thm)],[t12878,t253]) ).
cnf(t287319,plain,
X1 = upme(X1,meet(Y3,Y4),lojo(X1,X2,X3)),
inference(step,[status(thm)],[t287318,t87]) ).
cnf(t12936,plain,
upme(X1,meet(X2,X3),lojo(X1,Y3,Y4)) = X1,
inference(orient,[status(thm)],[t287319]) ).
cnf(t12940,plain,
X1 = upme(X1,X2,lojo(X1,X3,Y3)),
inference(cp,[status(thm)],[t12936,t127]) ).
cnf(t13008,plain,
upme(X1,X2,lojo(X1,X3,Y3)) = X1,
inference(orient,[status(thm)],[t12940]) ).
cnf(t51756,plain,
lojo(X1,X2,join(X1,lojo(X2,X3,Y3))) = upjo(X1,lojo(X2,X3,Y3),X2),
inference(cp,[status(thm)],[t51718,t13008]) ).
cnf(t287876,plain,
lojo(X1,X2,join(X1,lojo(X2,X3,Y3))) = upjo(X1,X2,lojo(X2,X3,Y3)),
inference(step,[status(thm)],[t51756,t52112]) ).
cnf(t10862,plain,
join(X1,X2) = upme(join(X1,X2),X3,join(X1,X2)),
inference(cp,[status(thm)],[t10845,t8051]) ).
cnf(t69,plain,
upme(X1,X2,join(X3,Y3)) = meet(X1,join(Y3,join(X2,X3))),
inference(cp,[status(thm)],[t31,t64]) ).
cnf(t286937,plain,
upme(X1,X2,join(X3,Y3)) = upme(X1,Y3,join(X2,X3)),
inference(step,[status(thm)],[t69,t31]) ).
cnf(t1341,plain,
upme(X1,X2,join(X3,Y3)) = upme(X1,Y3,join(X2,X3)),
inference(orient,[status(thm)],[t286937]) ).
cnf(t287282,plain,
join(X1,X2) = upme(join(X1,X2),X1,join(X2,X3)),
inference(step,[status(thm)],[t10862,t1341]) ).
cnf(t287283,plain,
join(X1,X2) = upjo(X1,X2,join(X2,X3)),
inference(step,[status(thm)],[t287282,t38]) ).
cnf(t10900,plain,
upjo(X1,X2,join(X2,X3)) = join(X1,X2),
inference(orient,[status(thm)],[t287283]) ).
cnf(t10921,plain,
join(X1,X2) = upjo(X1,X2,lojo(X2,X3,Y3)),
inference(cp,[status(thm)],[t10900,t161]) ).
cnf(t11013,plain,
upjo(X1,X2,lojo(X2,X3,Y3)) = join(X1,X2),
inference(orient,[status(thm)],[t10921]) ).
cnf(t287877,plain,
lojo(X1,X2,join(X1,lojo(X2,X3,Y3))) = join(X1,X2),
inference(step,[status(thm)],[t287876,t11013]) ).
cnf(t54229,plain,
lojo(X1,X2,join(X1,lojo(X2,X3,Y3))) = join(X1,X2),
inference(orient,[status(thm)],[t287877]) ).
cnf(t54241,plain,
join(X1,X2) = lojo(X1,X2,join(X1,join(X2,X3))),
inference(cp,[status(thm)],[t54229,t122]) ).
cnf(t54523,plain,
lojo(X1,X2,join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t54241]) ).
cnf(t288429,plain,
lome(join(X1,join(X2,X3)),X1,X2) = join(X1,X2),
inference(step,[status(thm)],[t54523,t103184]) ).
cnf(t103324,plain,
lome(join(X1,join(X2,X3)),X1,X2) = join(X1,X2),
inference(rw,[status(thm)],[t288429]) ).
cnf(t104501,plain,
lome(join(X1,join(X2,X3)),X1,X2) = join(X1,X2),
inference(orient,[status(thm)],[t103324]) ).
cnf(t104531,plain,
join(X1,X2) = lome(join(X2,upjo(X1,X3,Y3)),X1,X2),
inference(cp,[status(thm)],[t104501,t56215]) ).
cnf(t108885,plain,
lome(join(X1,upjo(X2,X3,Y3)),X2,X1) = join(X2,X1),
inference(orient,[status(thm)],[t104531]) ).
cnf(t109053,plain,
lome(join(X1,upjo(X2,X3,Y3)),X2,X1) = lome(join(X1,upjo(X2,X3,Y3)),meet(X1,Y4),join(X2,X1)),
inference(cp,[status(thm)],[t90086,t108885]) ).
cnf(t288512,plain,
join(X2,X1) = lome(join(X1,upjo(X2,X3,Y3)),meet(X1,Y4),join(X2,X1)),
inference(step,[status(thm)],[t109053,t108885]) ).
cnf(t288513,plain,
join(X2,X1) = upme(join(X1,upjo(X2,X3,Y3)),X2,X1),
inference(step,[status(thm)],[t288512,t105381]) ).
cnf(t111645,plain,
upme(join(X1,upjo(X2,X3,Y3)),X2,X1) = join(X2,X1),
inference(orient,[status(thm)],[t288513]) ).
cnf(t132045,plain,
upme(join(X1,upjo(X2,X3,Y3)),X2,X1) = upme(join(X1,upjo(X2,X3,Y3)),X1,join(X2,X1)),
inference(cp,[status(thm)],[t131976,t111645]) ).
cnf(t132215,plain,
upjo(X1,join(X2,X1),upjo(X2,X3,Y3)) = join(X2,X1),
inference(orient,[status(thm)],[t132045]) ).
cnf(t132274,plain,
join(X1,X2) = upjo(X2,join(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t132215,t135]) ).
cnf(t132523,plain,
upjo(X1,join(X2,X1),join(X2,X3)) = join(X2,X1),
inference(orient,[status(thm)],[t132274]) ).
cnf(t209467,plain,
upme(join(X1,join(X2,X1)),X2,X3) = upme(join(X2,X1),X2,X3),
inference(cp,[status(thm)],[t209410,t132523]) ).
cnf(t289338,plain,
upme(join(X1,join(X1,X2)),X2,X3) = upme(join(X2,X1),X2,X3),
inference(step,[status(thm)],[t209467,t64]) ).
cnf(t289339,plain,
upme(join(X1,X2),X2,X3) = upme(join(X2,X1),X2,X3),
inference(step,[status(thm)],[t289338,t136]) ).
cnf(t289340,plain,
upme(join(X1,X2),X2,X3) = upjo(X2,X1,X3),
inference(step,[status(thm)],[t289339,t38]) ).
cnf(t209644,plain,
upme(join(X1,X2),X2,X3) = upjo(X2,X1,X3),
inference(orient,[status(thm)],[t289340]) ).
cnf(t289341,plain,
upjo(X2,X1,meet(X3,Y3)) = upme(lojo(X2,X3,Y3),X1,X2),
inference(step,[status(thm)],[t146801,t209644]) ).
cnf(t209875,plain,
upjo(X2,X1,meet(X3,Y3)) = upme(lojo(X2,X3,Y3),X1,X2),
inference(rw,[status(thm)],[t289341]) ).
cnf(t210309,plain,
upme(lojo(X1,X2,X3),Y3,X1) = upjo(X1,Y3,meet(X2,X3)),
inference(orient,[status(thm)],[t209875]) ).
cnf(t289557,plain,
lome(join(X3,X1),X1,X2) = upjo(X1,X3,meet(X2,join(X3,X1))),
inference(step,[status(thm)],[t289556,t210309]) ).
cnf(t289558,plain,
lome(join(X3,X1),X1,X2) = upjo(X1,X3,upme(X2,X3,X1)),
inference(step,[status(thm)],[t289557,t31]) ).
cnf(t236100,plain,
upjo(X1,X2,upme(X3,X2,X1)) = lome(join(X2,X1),X1,X3),
inference(orient,[status(thm)],[t289558]) ).
cnf(t695,plain,
upme(X1,meet(X2,X3),a) = upme(X1,a,lome(X2,X3,a)),
inference(cp,[status(thm)],[t686,t80]) ).
cnf(t286903,plain,
upme(X1,a,meet(X2,X3)) = upme(X1,a,lome(X2,X3,a)),
inference(step,[status(thm)],[t695,t87]) ).
cnf(t1027,plain,
upme(X1,a,lome(X2,X3,a)) = upme(X1,a,meet(X2,X3)),
inference(orient,[status(thm)],[t286903]) ).
cnf(t1030,plain,
upme(X1,a,meet(meet(X2,a),X3)) = upme(X1,a,meet(X2,a)),
inference(cp,[status(thm)],[t1027,t905]) ).
cnf(t286904,plain,
upme(X1,a,meet(X3,meet(X2,a))) = upme(X1,a,meet(X2,a)),
inference(step,[status(thm)],[t1030,t15]) ).
cnf(t286905,plain,
upme(X1,a,meet(X2,meet(a,X3))) = upme(X1,a,meet(X2,a)),
inference(step,[status(thm)],[t286904,t17]) ).
cnf(t286906,plain,
upme(X1,a,meet(X2,meet(X3,a))) = upme(X1,a,meet(X2,a)),
inference(step,[status(thm)],[t286905,t15]) ).
cnf(t286907,plain,
upme(X1,a,meet(X2,meet(X3,a))) = meet(X1,a),
inference(step,[status(thm)],[t286906,t605]) ).
cnf(t1037,plain,
upme(X1,a,meet(X2,meet(X3,a))) = meet(X1,a),
inference(orient,[status(thm)],[t286907]) ).
cnf(t236232,plain,
lome(join(a,meet(X1,meet(X2,a))),meet(X1,meet(X2,a)),X3) = upjo(meet(X1,meet(X2,a)),a,meet(X3,a)),
inference(cp,[status(thm)],[t236100,t1037]) ).
cnf(t289613,plain,
lome(join(a,meet(X1,meet(X2,a))),X3,meet(X1,meet(X2,a))) = upjo(meet(X1,meet(X2,a)),a,meet(X3,a)),
inference(step,[status(thm)],[t236232,t59453]) ).
cnf(t289614,plain,
lome(lojo(a,X1,meet(X2,a)),X3,meet(X1,meet(X2,a))) = upjo(meet(X1,meet(X2,a)),a,meet(X3,a)),
inference(step,[status(thm)],[t289613,t55]) ).
cnf(t289615,plain,
lome(a,X3,meet(X1,meet(X2,a))) = upjo(meet(X1,meet(X2,a)),a,meet(X3,a)),
inference(step,[status(thm)],[t289614,t1246]) ).
cnf(t289616,plain,
lome(a,X3,meet(X1,X2)) = upjo(meet(X1,meet(X2,a)),a,meet(X3,a)),
inference(step,[status(thm)],[t289615,t177723]) ).
cnf(t6358,plain,
X1 = lojo(X1,meet(X1,X2),lome(X3,Y3,Y4)),
inference(cp,[status(thm)],[t6337,t1440]) ).
cnf(t6887,plain,
lojo(X1,meet(X1,X2),lome(X3,Y3,Y4)) = X1,
inference(orient,[status(thm)],[t6358]) ).
cnf(t6892,plain,
X1 = lojo(X1,upme(X1,X2,X3),lome(Y3,Y4,Y5)),
inference(cp,[status(thm)],[t6887,t189]) ).
cnf(t10358,plain,
lojo(X1,upme(X1,X2,X3),lome(Y3,Y4,Y5)) = X1,
inference(orient,[status(thm)],[t6892]) ).
cnf(t13522,plain,
X1 = lojo(X1,lome(X1,a,X2),lome(X3,Y3,Y4)),
inference(cp,[status(thm)],[t10358,t13513]) ).
cnf(t16069,plain,
lojo(X1,lome(X1,a,X2),lome(X3,Y3,Y4)) = X1,
inference(orient,[status(thm)],[t13522]) ).
cnf(t16072,plain,
X1 = lojo(X1,lome(X1,a,X2),meet(X3,Y3)),
inference(cp,[status(thm)],[t16069,t121]) ).
cnf(t287372,plain,
X1 = lojo(X1,X3,meet(lome(X1,a,X2),Y3)),
inference(step,[status(thm)],[t16072,t747]) ).
cnf(t287373,plain,
X1 = lojo(X1,X3,meet(Y3,lome(X1,a,X2))),
inference(step,[status(thm)],[t287372,t15]) ).
cnf(t16206,plain,
lojo(X1,X2,meet(X3,lome(X1,a,Y3))) = X1,
inference(orient,[status(thm)],[t287373]) ).
cnf(t19488,plain,
lojo(X1,X2,meet(X3,lome(X1,a,Y3))) = X1,
inference(rw,[status(thm)],[t16206]) ).
cnf(t287429,plain,
lojo(X1,X2,meet(X3,lome(X1,Y3,a))) = X1,
inference(step,[status(thm)],[t19488,t19398]) ).
cnf(t19771,plain,
lojo(X1,X2,meet(X3,lome(X1,Y3,a))) = X1,
inference(orient,[status(thm)],[t287429]) ).
cnf(t20939,plain,
lome(join(X1,a),a,X1) = upjo(X1,a,a),
inference(cp,[status(thm)],[t20912,t708]) ).
cnf(t287442,plain,
lome(join(X1,a),a,X1) = join(X1,a),
inference(step,[status(thm)],[t20939,t135]) ).
cnf(t20987,plain,
lome(join(X1,a),a,X1) = join(X1,a),
inference(orient,[status(thm)],[t287442]) ).
cnf(t21012,plain,
meet(X1,lome(join(X2,a),X2,a)) = meet(X1,join(X2,a)),
inference(cp,[status(thm)],[t19398,t20987]) ).
cnf(t287449,plain,
meet(X1,lome(join(X2,a),X2,a)) = upme(X1,X2,a),
inference(step,[status(thm)],[t21012,t31]) ).
cnf(t21109,plain,
meet(X1,lome(join(X2,a),X2,a)) = upme(X1,X2,a),
inference(orient,[status(thm)],[t287449]) ).
cnf(t21155,plain,
join(X1,a) = lojo(join(X1,a),X2,upme(X3,X1,a)),
inference(cp,[status(thm)],[t19771,t21109]) ).
cnf(t21322,plain,
lojo(join(X1,a),X2,upme(X3,X1,a)) = join(X1,a),
inference(orient,[status(thm)],[t21155]) ).
cnf(t11888,plain,
meet(join(X1,X2),X3) = upme(meet(join(X1,X2),X3),X1,X2),
inference(cp,[status(thm)],[t11881,t7152]) ).
cnf(t287305,plain,
meet(X3,join(X1,X2)) = upme(meet(join(X1,X2),X3),X1,X2),
inference(step,[status(thm)],[t11888,t15]) ).
cnf(t287306,plain,
upme(X3,X1,X2) = upme(meet(join(X1,X2),X3),X1,X2),
inference(step,[status(thm)],[t287305,t31]) ).
cnf(t287307,plain,
upme(X3,X1,X2) = upme(meet(X3,join(X1,X2)),X1,X2),
inference(step,[status(thm)],[t287306,t15]) ).
cnf(t287308,plain,
upme(X3,X1,X2) = upme(upme(X3,X1,X2),X1,X2),
inference(step,[status(thm)],[t287307,t31]) ).
cnf(t12113,plain,
upme(upme(X1,X2,X3),X2,X3) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t287308]) ).
cnf(t12145,plain,
upme(join(X1,X2),X1,X3) = upme(upjo(X1,X2,X3),X1,X3),
inference(cp,[status(thm)],[t12113,t38]) ).
cnf(t287309,plain,
upjo(X1,X2,X3) = upme(upjo(X1,X2,X3),X1,X3),
inference(step,[status(thm)],[t12145,t38]) ).
cnf(t12156,plain,
upme(upjo(X1,X2,X3),X1,X3) = upjo(X1,X2,X3),
inference(orient,[status(thm)],[t287309]) ).
cnf(t21328,plain,
join(X1,a) = lojo(join(X1,a),X2,upjo(X1,X3,a)),
inference(cp,[status(thm)],[t21322,t12156]) ).
cnf(t21354,plain,
lojo(join(X1,a),X2,upjo(X1,X3,a)) = join(X1,a),
inference(orient,[status(thm)],[t21328]) ).
cnf(t4088,plain,
join(X1,lome(a,X2,X1)) = lojo(lojo(X1,X2,a),X1,a),
inference(cp,[status(thm)],[t4085,t652]) ).
cnf(t287078,plain,
lojo(X1,X2,a) = lojo(lojo(X1,X2,a),X1,a),
inference(step,[status(thm)],[t4088,t652]) ).
cnf(t4111,plain,
lojo(lojo(X1,X2,a),X1,a) = lojo(X1,X2,a),
inference(orient,[status(thm)],[t287078]) ).
cnf(t4118,plain,
lojo(X1,X2,a) = upme(lojo(X1,X2,a),a,lojo(X1,X2,a)),
inference(cp,[status(thm)],[t2836,t4111]) ).
cnf(t287079,plain,
lojo(X1,X2,a) = upme(lojo(X1,X2,a),X1,a),
inference(step,[status(thm)],[t4118,t686]) ).
cnf(t287080,plain,
lojo(X1,X2,a) = upjo(X1,meet(X2,a),a),
inference(step,[status(thm)],[t287079,t396]) ).
cnf(t4130,plain,
upjo(X1,meet(X2,a),a) = lojo(X1,X2,a),
inference(orient,[status(thm)],[t287080]) ).
cnf(t21369,plain,
join(X1,a) = lojo(join(X1,a),X2,lojo(X1,X3,a)),
inference(cp,[status(thm)],[t21354,t4130]) ).
cnf(t21492,plain,
lojo(join(X1,a),X2,lojo(X1,X3,a)) = join(X1,a),
inference(orient,[status(thm)],[t21369]) ).
cnf(t13541,plain,
lojo(X1,X2,join(X3,meet(X2,a))) = join(X1,lome(X2,a,X3)),
inference(cp,[status(thm)],[t93,t13513]) ).
cnf(t287342,plain,
lojo(X1,X2,lojo(X3,X2,a)) = join(X1,lome(X2,a,X3)),
inference(step,[status(thm)],[t13541,t55]) ).
cnf(t14602,plain,
lojo(X1,X2,lojo(X3,X2,a)) = join(X1,lome(X2,a,X3)),
inference(orient,[status(thm)],[t287342]) ).
cnf(t21493,plain,
join(X1,a) = join(join(X1,a),lome(X2,a,X1)),
inference(cp,[status(thm)],[t21492,t14602]) ).
cnf(t21532,plain,
join(join(X1,a),lome(X2,a,X1)) = join(X1,a),
inference(orient,[status(thm)],[t21493]) ).
cnf(t22450,plain,
join(join(X1,a),lome(X2,a,X1)) = join(X1,a),
inference(rw,[status(thm)],[t21532]) ).
cnf(t287495,plain,
join(join(X1,a),lome(X2,X1,a)) = join(X1,a),
inference(step,[status(thm)],[t22450,t22370]) ).
cnf(t22947,plain,
join(join(X1,a),lome(X2,X1,a)) = join(X1,a),
inference(orient,[status(thm)],[t287495]) ).
cnf(t22956,plain,
join(upjo(X1,X2,X3),a) = join(join(upjo(X1,X2,X3),a),X1),
inference(cp,[status(thm)],[t22947,t352]) ).
cnf(t287544,plain,
join(a,upjo(X1,X2,X3)) = join(join(upjo(X1,X2,X3),a),X1),
inference(step,[status(thm)],[t22956,t51]) ).
cnf(t287545,plain,
join(a,upjo(X1,X2,X3)) = join(X1,join(upjo(X1,X2,X3),a)),
inference(step,[status(thm)],[t287544,t51]) ).
cnf(t287546,plain,
join(a,upjo(X1,X2,X3)) = join(X1,join(a,upjo(X1,X2,X3))),
inference(step,[status(thm)],[t287545,t51]) ).
cnf(t25496,plain,
join(X1,join(a,upjo(X1,X2,X3))) = join(a,upjo(X1,X2,X3)),
inference(orient,[status(thm)],[t287546]) ).
cnf(t25598,plain,
join(X1,X2) = upjo(X1,join(a,upjo(X2,X3,Y3)),X2),
inference(cp,[status(thm)],[t2640,t25496]) ).
cnf(t26191,plain,
upjo(X1,join(a,upjo(X2,X3,Y3)),X2) = join(X1,X2),
inference(orient,[status(thm)],[t25598]) ).
cnf(t2476,plain,
join(meet(X1,a),lome(a,X1,X2)) = upjo(lome(a,X1,X2),X3,meet(X1,a)),
inference(cp,[status(thm)],[t2468,t1523]) ).
cnf(t287742,plain,
lome(a,X1,X2) = upjo(lome(a,X1,X2),X3,meet(X1,a)),
inference(step,[status(thm)],[t2476,t1523]) ).
cnf(t40337,plain,
upjo(lome(a,X1,X2),X3,meet(X1,a)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t287742]) ).
cnf(t40393,plain,
join(X1,lome(a,X2,X3)) = upjo(X1,join(a,lome(a,X2,X3)),lome(a,X2,X3)),
inference(cp,[status(thm)],[t26191,t40337]) ).
cnf(t287743,plain,
join(X1,lome(a,X2,X3)) = upjo(X1,a,lome(a,X2,X3)),
inference(step,[status(thm)],[t40393,t462]) ).
cnf(t40398,plain,
upjo(X1,a,lome(a,X2,X3)) = join(X1,lome(a,X2,X3)),
inference(orient,[status(thm)],[t287743]) ).
cnf(t40399,plain,
join(X1,lome(a,X1,X2)) = upjo(X1,a,meet(X2,a)),
inference(cp,[status(thm)],[t40398,t4857]) ).
cnf(t287744,plain,
lojo(X1,X2,a) = upjo(X1,a,meet(X2,a)),
inference(step,[status(thm)],[t40399,t4566]) ).
cnf(t40473,plain,
upjo(X1,a,meet(X2,a)) = lojo(X1,X2,a),
inference(orient,[status(thm)],[t287744]) ).
cnf(t289617,plain,
lome(a,X3,meet(X1,X2)) = lojo(meet(X1,meet(X2,a)),X3,a),
inference(step,[status(thm)],[t289616,t40473]) ).
cnf(t243987,plain,
lojo(meet(X1,meet(X2,a)),X3,a) = lome(a,X3,meet(X1,X2)),
inference(orient,[status(thm)],[t289617]) ).
cnf(t289679,plain,
lome(a,X2,meet(X1,X2)) = upme(meet(X2,a),X2,meet(X1,meet(meet(X2,a),a))),
inference(step,[status(thm)],[t289678,t243987]) ).
cnf(t289680,plain,
lome(a,X2,meet(X1,X2)) = meet(X2,a),
inference(step,[status(thm)],[t289679,t11881]) ).
cnf(t253304,plain,
lome(a,X1,meet(X2,X1)) = meet(X1,a),
inference(orient,[status(thm)],[t289680]) ).
cnf(t253414,plain,
meet(a,lome(X1,X2,X3)) = meet(meet(X1,a),lome(X1,X2,X3)),
inference(cp,[status(thm)],[t188222,t253304]) ).
cnf(t254483,plain,
meet(meet(X1,a),lome(X1,X2,X3)) = meet(a,lome(X1,X2,X3)),
inference(orient,[status(thm)],[t253414]) ).
cnf(t44230,plain,
lojo(X1,join(X2,X3),join(X2,Y3)) = upjo(X1,join(X2,X3),upjo(X2,X3,Y3)),
inference(cp,[status(thm)],[t44128,t38]) ).
cnf(t289093,plain,
join(X1,upjo(X2,X3,Y3)) = upjo(X1,join(X2,X3),upjo(X2,X3,Y3)),
inference(step,[status(thm)],[t44230,t2514]) ).
cnf(t179283,plain,
upjo(X1,join(X2,X3),upjo(X2,X3,Y3)) = join(X1,upjo(X2,X3,Y3)),
inference(orient,[status(thm)],[t289093]) ).
cnf(t179386,plain,
join(X1,upjo(X2,X3,meet(X3,Y3))) = upjo(X1,join(X2,X3),lojo(X2,X3,Y3)),
inference(cp,[status(thm)],[t179283,t41195]) ).
cnf(t289513,plain,
join(X1,lojo(X2,X3,Y3)) = upjo(X1,join(X2,X3),lojo(X2,X3,Y3)),
inference(step,[status(thm)],[t179386,t41195]) ).
cnf(t54237,plain,
join(X1,X2) = lojo(X1,X2,join(X1,X2)),
inference(cp,[status(thm)],[t54229,t46243]) ).
cnf(t54372,plain,
lojo(X1,X2,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t54237]) ).
cnf(t54453,plain,
join(X1,lojo(X2,X3,join(X1,X3))) = join(X2,join(X1,X3)),
inference(cp,[status(thm)],[t424,t54372]) ).
cnf(t287882,plain,
join(X1,lojo(X2,X3,join(X1,X3))) = join(X1,join(X3,X2)),
inference(step,[status(thm)],[t54453,t64]) ).
cnf(t287883,plain,
join(X1,lojo(X2,X3,join(X1,X3))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t287882,t51]) ).
cnf(t54602,plain,
join(X1,lojo(X2,X3,join(X1,X3))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t287883]) ).
cnf(t54604,plain,
join(X1,join(join(X1,X2),X3)) = lojo(join(X1,X2),X3,join(X1,X3)),
inference(cp,[status(thm)],[t54602,t18860]) ).
cnf(t288659,plain,
join(X1,join(X3,join(X1,X2))) = lojo(join(X1,X2),X3,join(X1,X3)),
inference(step,[status(thm)],[t54604,t51]) ).
cnf(t288660,plain,
join(X1,join(X2,join(X3,X1))) = lojo(join(X1,X2),X3,join(X1,X3)),
inference(step,[status(thm)],[t288659,t64]) ).
cnf(t288661,plain,
join(X1,join(X1,join(X2,X3))) = lojo(join(X1,X2),X3,join(X1,X3)),
inference(step,[status(thm)],[t288660,t64]) ).
cnf(t288662,plain,
join(X1,join(X2,X3)) = lojo(join(X1,X2),X3,join(X1,X3)),
inference(step,[status(thm)],[t288661,t136]) ).
cnf(t125473,plain,
lojo(join(X1,X2),X3,join(X1,X3)) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t288662]) ).
cnf(t125480,plain,
join(X1,join(X2,meet(X3,Y3))) = lojo(join(X1,X2),X3,upme(Y3,X1,meet(X3,Y3))),
inference(cp,[status(thm)],[t125473,t100724]) ).
cnf(t288663,plain,
join(X1,lojo(X2,X3,Y3)) = lojo(join(X1,X2),X3,upme(Y3,X1,meet(X3,Y3))),
inference(step,[status(thm)],[t125480,t55]) ).
cnf(t68890,plain,
lojo(X1,X2,X3) = lojo(X1,X2,upme(X3,Y3,meet(X3,X2))),
inference(cp,[status(thm)],[t68867,t32986]) ).
cnf(t288336,plain,
lojo(X1,X2,X3) = lojo(X1,X2,upme(X3,Y3,meet(X2,X3))),
inference(step,[status(thm)],[t68890,t15]) ).
cnf(t91270,plain,
lojo(X1,X2,upme(X3,Y3,meet(X2,X3))) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t288336]) ).
cnf(t288664,plain,
join(X1,lojo(X2,X3,Y3)) = lojo(join(X1,X2),X3,Y3),
inference(step,[status(thm)],[t288663,t91270]) ).
cnf(t125705,plain,
join(X1,lojo(X2,X3,Y3)) = lojo(join(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t288664]) ).
cnf(t289514,plain,
lojo(join(X1,X2),X3,Y3) = upjo(X1,join(X2,X3),lojo(X2,X3,Y3)),
inference(step,[status(thm)],[t289513,t125705]) ).
cnf(t229968,plain,
upjo(X1,join(X2,X3),lojo(X2,X3,Y3)) = lojo(join(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t289514]) ).
cnf(t324,plain,
lojo(X1,X2,meet(X3,a)) = upjo(lojo(X1,X2,meet(X3,a)),Y3,lojo(upme(meet(X2,a),X3,X1),X3,X1)),
inference(cp,[status(thm)],[t280,t305]) ).
cnf(t287549,plain,
lojo(X1,X2,meet(X3,a)) = upjo(lojo(X1,X2,meet(X3,a)),Y3,lojo(upme(meet(X2,a),X3,X1),X1,X3)),
inference(step,[status(thm)],[t324,t90]) ).
cnf(t287550,plain,
lojo(X1,X2,meet(X3,a)) = upjo(lojo(X1,X2,meet(X3,a)),Y3,lojo(upme(meet(X2,a),X1,X3),X1,X3)),
inference(step,[status(thm)],[t287549,t87]) ).
cnf(t26329,plain,
upjo(lojo(X1,X2,meet(X3,a)),Y3,lojo(upme(meet(X2,a),X1,X3),X1,X3)) = lojo(X1,X2,meet(X3,a)),
inference(orient,[status(thm)],[t287550]) ).
cnf(t229987,plain,
lojo(join(lojo(X1,X2,meet(X3,a)),upme(meet(X2,a),X1,X3)),X1,X3) = lojo(X1,X2,meet(X3,a)),
inference(cp,[status(thm)],[t229968,t26329]) ).
cnf(t289515,plain,
lojo(lojo(lojo(X1,X2,meet(X3,a)),meet(X2,a),join(X1,X3)),X1,X3) = lojo(X1,X2,meet(X3,a)),
inference(step,[status(thm)],[t229987,t93]) ).
cnf(t289516,plain,
lojo(lojo(lojo(X1,X2,meet(X3,a)),X2,upme(a,X1,X3)),X1,X3) = lojo(X1,X2,meet(X3,a)),
inference(step,[status(thm)],[t289515,t100724]) ).
cnf(t125809,plain,
lojo(join(X1,meet(X2,X3)),X2,Y3) = join(X1,lome(X2,X3,Y3)),
inference(cp,[status(thm)],[t125705,t80]) ).
cnf(t288676,plain,
lojo(lojo(X1,X2,X3),X2,Y3) = join(X1,lome(X2,X3,Y3)),
inference(step,[status(thm)],[t125809,t55]) ).
cnf(t125970,plain,
lojo(lojo(X1,X2,X3),X2,Y3) = join(X1,lome(X2,X3,Y3)),
inference(orient,[status(thm)],[t288676]) ).
cnf(t289517,plain,
lojo(join(X1,lome(X2,meet(X3,a),upme(a,X1,X3))),X1,X3) = lojo(X1,X2,meet(X3,a)),
inference(step,[status(thm)],[t289516,t125970]) ).
cnf(t289518,plain,
join(X1,lome(X2,meet(X3,a),upme(a,X1,X3))) = lojo(X1,X2,meet(X3,a)),
inference(step,[status(thm)],[t289517,t8051]) ).
cnf(t29681,plain,
upme(X1,meet(X2,a),meet(X3,a)) = lome(X1,meet(X2,a),lome(a,X2,X3)),
inference(cp,[status(thm)],[t29585,t632]) ).
cnf(t646,plain,
upme(X1,meet(X2,a),meet(X3,a)) = meet(X1,lome(a,X2,X3)),
inference(cp,[status(thm)],[t253,t632]) ).
cnf(t16784,plain,
upme(X1,meet(X2,a),meet(X3,a)) = meet(X1,lome(a,X2,X3)),
inference(orient,[status(thm)],[t646]) ).
cnf(t289074,plain,
meet(X1,lome(a,X2,X3)) = lome(X1,meet(X2,a),lome(a,X2,X3)),
inference(step,[status(thm)],[t29681,t16784]) ).
cnf(t175943,plain,
lome(X1,meet(X2,a),lome(a,X2,X3)) = meet(X1,lome(a,X2,X3)),
inference(orient,[status(thm)],[t289074]) ).
cnf(t176003,plain,
meet(X1,lome(a,X2,join(X3,X2))) = lome(X1,meet(X2,a),upme(a,X3,X2)),
inference(cp,[status(thm)],[t175943,t103717]) ).
cnf(t6562,plain,
meet(X1,join(X2,X3)) = lome(X1,join(X2,X3),upjo(X2,X3,Y3)),
inference(cp,[status(thm)],[t6545,t1481]) ).
cnf(t287931,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),upjo(X2,X3,Y3)),
inference(step,[status(thm)],[t6562,t31]) ).
cnf(t57108,plain,
lome(X1,join(X2,X3),upjo(X2,X3,Y3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t287931]) ).
cnf(t57168,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),lojo(X2,X3,Y3)),
inference(cp,[status(thm)],[t57108,t41195]) ).
cnf(t86268,plain,
lome(X1,join(X2,X3),lojo(X2,X3,Y3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t57168]) ).
cnf(t86279,plain,
upme(a,X1,X2) = lome(a,join(X1,X2),lome(a,X1,X2)),
inference(cp,[status(thm)],[t86268,t4499]) ).
cnf(t97992,plain,
lome(a,join(X1,X2),lome(a,X1,X2)) = upme(a,X1,X2),
inference(orient,[status(thm)],[t86279]) ).
cnf(t98020,plain,
upme(a,join(X1,X2),lome(X2,X3,Y3)) = lome(a,join(X1,X2),lome(a,join(X1,X2),lome(X2,X3,Y3))),
inference(cp,[status(thm)],[t97992,t60833]) ).
cnf(t60928,plain,
upme(X1,join(X2,X3),lome(X3,Y3,Y4)) = lome(X1,join(X2,X3),join(X2,X3)),
inference(cp,[status(thm)],[t28224,t60833]) ).
cnf(t288316,plain,
upme(X1,join(X2,X3),lome(X3,Y3,Y4)) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t60928,t121]) ).
cnf(t288317,plain,
upme(X1,join(X2,X3),lome(X3,Y3,Y4)) = upme(X1,X2,X3),
inference(step,[status(thm)],[t288316,t31]) ).
cnf(t89729,plain,
upme(X1,join(X2,X3),lome(X3,Y3,Y4)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288317]) ).
cnf(t288388,plain,
upme(a,X1,X2) = lome(a,join(X1,X2),lome(a,join(X1,X2),lome(X2,X3,Y3))),
inference(step,[status(thm)],[t98020,t89729]) ).
cnf(t288389,plain,
upme(a,X1,X2) = lome(a,join(X1,X2),lome(X2,X3,Y3)),
inference(step,[status(thm)],[t288388,t4211]) ).
cnf(t98905,plain,
lome(a,join(X1,X2),lome(X2,X3,Y3)) = upme(a,X1,X2),
inference(orient,[status(thm)],[t288389]) ).
cnf(t5230,plain,
meet(a,lome(X1,X2,a)) = lome(a,meet(X1,X2),X1),
inference(cp,[status(thm)],[t5229,t4493]) ).
cnf(t287138,plain,
meet(a,lome(X1,X2,a)) = meet(a,X1),
inference(step,[status(thm)],[t5230,t2020]) ).
cnf(t287139,plain,
meet(a,lome(X1,X2,a)) = meet(X1,a),
inference(step,[status(thm)],[t287138,t15]) ).
cnf(t5308,plain,
meet(a,lome(X1,X2,a)) = meet(X1,a),
inference(orient,[status(thm)],[t287139]) ).
cnf(t5339,plain,
lome(a,X1,lome(X2,X3,a)) = lome(a,X1,meet(X2,a)),
inference(cp,[status(thm)],[t219,t5308]) ).
cnf(t287145,plain,
lome(a,X1,lome(X2,X3,a)) = lome(a,X1,X2),
inference(step,[status(thm)],[t5339,t630]) ).
cnf(t5352,plain,
lome(a,X1,lome(X2,X3,a)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t287145]) ).
cnf(t98906,plain,
upme(a,X1,X2) = lome(a,join(X1,X2),X2),
inference(cp,[status(thm)],[t98905,t5352]) ).
cnf(t288390,plain,
upme(a,X1,X2) = lome(a,X2,join(X1,X2)),
inference(step,[status(thm)],[t98906,t4492]) ).
cnf(t99103,plain,
lome(a,X1,join(X2,X1)) = upme(a,X2,X1),
inference(orient,[status(thm)],[t288390]) ).
cnf(t289508,plain,
meet(X1,upme(a,X3,X2)) = lome(X1,meet(X2,a),upme(a,X3,X2)),
inference(step,[status(thm)],[t176003,t99103]) ).
cnf(t289509,plain,
upme(meet(X1,a),X3,X2) = lome(X1,meet(X2,a),upme(a,X3,X2)),
inference(step,[status(thm)],[t289508,t33621]) ).
cnf(t228893,plain,
lome(X1,meet(X2,a),upme(a,X3,X2)) = upme(meet(X1,a),X3,X2),
inference(orient,[status(thm)],[t289509]) ).
cnf(t289519,plain,
join(X1,upme(meet(X2,a),X1,X3)) = lojo(X1,X2,meet(X3,a)),
inference(step,[status(thm)],[t289518,t228893]) ).
cnf(t289520,plain,
lojo(X1,meet(X2,a),join(X1,X3)) = lojo(X1,X2,meet(X3,a)),
inference(step,[status(thm)],[t289519,t93]) ).
cnf(t289521,plain,
lojo(X1,X2,upme(a,X1,X3)) = lojo(X1,X2,meet(X3,a)),
inference(step,[status(thm)],[t289520,t100724]) ).
cnf(t230480,plain,
lojo(X1,X2,upme(a,X1,X3)) = lojo(X1,X2,meet(X3,a)),
inference(orient,[status(thm)],[t289521]) ).
cnf(t230485,plain,
lojo(X1,upme(a,X1,X2),meet(X2,a)) = join(X1,upme(a,X1,X2)),
inference(cp,[status(thm)],[t230480,t122]) ).
cnf(t289924,plain,
lojo(X1,X2,meet(upme(a,X1,X2),a)) = join(X1,upme(a,X1,X2)),
inference(step,[status(thm)],[t230485,t747]) ).
cnf(t289925,plain,
lojo(X1,X2,meet(a,upme(a,X1,X2))) = join(X1,upme(a,X1,X2)),
inference(step,[status(thm)],[t289924,t15]) ).
cnf(t289926,plain,
lojo(X1,X2,upme(meet(a,a),X1,X2)) = join(X1,upme(a,X1,X2)),
inference(step,[status(thm)],[t289925,t33621]) ).
cnf(t71754,plain,
meet(X1,meet(X2,lome(X3,X2,Y3))) = meet(meet(X3,X2),lome(X1,X2,Y4)),
inference(cp,[status(thm)],[t71735,t68676]) ).
cnf(t288135,plain,
meet(X1,meet(X3,X2)) = meet(meet(X3,X2),lome(X1,X2,Y4)),
inference(step,[status(thm)],[t71754,t68676]) ).
cnf(t72086,plain,
meet(meet(X1,X2),lome(X3,X2,Y3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t288135]) ).
cnf(t131648,plain,
meet(join(X1,X2),meet(X3,X2)) = meet(meet(X3,X2),lojo(X2,Y3,upme(Y4,X1,X2))),
inference(cp,[status(thm)],[t72086,t131495]) ).
cnf(t288726,plain,
meet(X2,meet(join(X1,X2),X3)) = meet(meet(X3,X2),lojo(X2,Y3,upme(Y4,X1,X2))),
inference(step,[status(thm)],[t131648,t17]) ).
cnf(t288727,plain,
meet(X2,meet(X3,join(X1,X2))) = meet(meet(X3,X2),lojo(X2,Y3,upme(Y4,X1,X2))),
inference(step,[status(thm)],[t288726,t15]) ).
cnf(t288728,plain,
meet(X2,upme(X3,X1,X2)) = meet(meet(X3,X2),lojo(X2,Y3,upme(Y4,X1,X2))),
inference(step,[status(thm)],[t288727,t31]) ).
cnf(t288729,plain,
upme(meet(X2,X3),X1,X2) = meet(meet(X3,X2),lojo(X2,Y3,upme(Y4,X1,X2))),
inference(step,[status(thm)],[t288728,t33621]) ).
cnf(t288730,plain,
upme(meet(X2,X3),X1,X2) = upme(meet(X3,X2),X2,meet(Y3,upme(Y4,X1,X2))),
inference(step,[status(thm)],[t288729,t253]) ).
cnf(t288731,plain,
upme(meet(X2,X3),X1,X2) = meet(X3,X2),
inference(step,[status(thm)],[t288730,t28408]) ).
cnf(t288732,plain,
upme(meet(X2,X3),X1,X2) = meet(X2,X3),
inference(step,[status(thm)],[t288731,t15]) ).
cnf(t131840,plain,
upme(meet(X1,X2),X3,X1) = meet(X1,X2),
inference(orient,[status(thm)],[t288732]) ).
cnf(t131947,plain,
lome(join(X1,X2),X1,meet(X2,X3)) = upjo(X1,X2,meet(X2,X3)),
inference(cp,[status(thm)],[t103185,t131840]) ).
cnf(t103192,plain,
lome(join(X1,X2),X1,meet(X3,Y3)) = lojo(X1,X3,upme(Y3,X1,X2)),
inference(cp,[status(thm)],[t103184,t100724]) ).
cnf(t129237,plain,
lome(join(X1,X2),X1,meet(X3,Y3)) = lojo(X1,X3,upme(Y3,X1,X2)),
inference(orient,[status(thm)],[t103192]) ).
cnf(t288740,plain,
lojo(X1,X2,upme(X3,X1,X2)) = upjo(X1,X2,meet(X2,X3)),
inference(step,[status(thm)],[t131947,t129237]) ).
cnf(t288741,plain,
lojo(X1,X2,upme(X3,X1,X2)) = lojo(X1,X2,X3),
inference(step,[status(thm)],[t288740,t41195]) ).
cnf(t132115,plain,
lojo(X1,X2,upme(X3,X1,X2)) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t288741]) ).
cnf(t289927,plain,
lojo(X1,X2,meet(a,a)) = join(X1,upme(a,X1,X2)),
inference(step,[status(thm)],[t289926,t132115]) ).
cnf(t289928,plain,
lojo(X1,X2,a) = join(X1,upme(a,X1,X2)),
inference(step,[status(thm)],[t289927,t127]) ).
cnf(t289929,plain,
lojo(X1,X2,a) = lojo(X1,a,join(X1,X2)),
inference(step,[status(thm)],[t289928,t93]) ).
cnf(t289930,plain,
lojo(X1,X2,a) = lome(join(X1,X2),X1,a),
inference(step,[status(thm)],[t289929,t52391]) ).
cnf(t281376,plain,
lome(join(X1,X2),X1,a) = lojo(X1,X2,a),
inference(orient,[status(thm)],[t289930]) ).
cnf(t281471,plain,
meet(a,lome(join(X1,X2),X1,a)) = meet(meet(join(X1,X2),a),lojo(X1,X2,a)),
inference(cp,[status(thm)],[t254483,t281376]) ).
cnf(t289934,plain,
meet(join(X1,X2),a) = meet(meet(join(X1,X2),a),lojo(X1,X2,a)),
inference(step,[status(thm)],[t281471,t5308]) ).
cnf(t289935,plain,
meet(a,join(X1,X2)) = meet(meet(join(X1,X2),a),lojo(X1,X2,a)),
inference(step,[status(thm)],[t289934,t15]) ).
cnf(t289936,plain,
upme(a,X1,X2) = meet(meet(join(X1,X2),a),lojo(X1,X2,a)),
inference(step,[status(thm)],[t289935,t31]) ).
cnf(t289937,plain,
upme(a,X1,X2) = upme(meet(join(X1,X2),a),X1,meet(X2,a)),
inference(step,[status(thm)],[t289936,t253]) ).
cnf(t289938,plain,
upme(a,X1,X2) = meet(join(X1,X2),lome(a,X1,X2)),
inference(step,[status(thm)],[t289937,t36664]) ).
cnf(t7978,plain,
join(join(X1,X2),upjo(X1,X2,X3)) = lojo(join(X1,X2),Y3,upjo(join(X1,X2),upjo(X1,X2,X3),Y4)),
inference(cp,[status(thm)],[t7965,t2591]) ).
cnf(t287231,plain,
join(X1,X2) = lojo(join(X1,X2),Y3,upjo(join(X1,X2),upjo(X1,X2,X3),Y4)),
inference(step,[status(thm)],[t7978,t2591]) ).
cnf(t287232,plain,
join(X1,X2) = lojo(join(X1,X2),Y3,join(X1,X2)),
inference(step,[status(thm)],[t287231,t2991]) ).
cnf(t8185,plain,
lojo(join(X1,X2),X3,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t287232]) ).
cnf(t11806,plain,
meet(X1,join(X2,X3)) = lome(meet(X1,join(X2,X3)),Y3,join(X2,X3)),
inference(cp,[status(thm)],[t11748,t8185]) ).
cnf(t288160,plain,
upme(X1,X2,X3) = lome(meet(X1,join(X2,X3)),Y3,join(X2,X3)),
inference(step,[status(thm)],[t11806,t31]) ).
cnf(t288161,plain,
upme(X1,X2,X3) = lome(upme(X1,X2,X3),Y3,join(X2,X3)),
inference(step,[status(thm)],[t288160,t31]) ).
cnf(t74210,plain,
lome(upme(X1,X2,X3),Y3,join(X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288161]) ).
cnf(t41285,plain,
join(X1,X2) = lojo(join(X1,X2),X3,lojo(X1,X2,Y3)),
inference(cp,[status(thm)],[t7965,t41195]) ).
cnf(t45311,plain,
lojo(join(X1,X2),X3,lojo(X1,X2,Y3)) = join(X1,X2),
inference(orient,[status(thm)],[t41285]) ).
cnf(t1265,plain,
lojo(X1,a,join(X2,meet(X3,a))) = join(X1,lome(a,X3,X2)),
inference(cp,[status(thm)],[t93,t1253]) ).
cnf(t286940,plain,
lojo(X1,a,lojo(X2,X3,a)) = join(X1,lome(a,X3,X2)),
inference(step,[status(thm)],[t1265,t55]) ).
cnf(t1429,plain,
lojo(X1,a,lojo(X2,X3,a)) = join(X1,lome(a,X3,X2)),
inference(orient,[status(thm)],[t286940]) ).
cnf(t287101,plain,
lojo(X1,a,lojo(X2,X3,a)) = join(X1,lome(a,X2,X3)),
inference(step,[status(thm)],[t1429,t4492]) ).
cnf(t4495,plain,
lojo(X1,a,lojo(X2,X3,a)) = join(X1,lome(a,X2,X3)),
inference(orient,[status(thm)],[t287101]) ).
cnf(t45316,plain,
join(X1,X2) = join(join(X1,X2),lome(a,X1,X2)),
inference(cp,[status(thm)],[t45311,t4495]) ).
cnf(t45458,plain,
join(join(X1,X2),lome(a,X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t45316]) ).
cnf(t45587,plain,
upme(X1,join(X2,X3),lome(a,X2,X3)) = lome(X1,join(X2,X3),join(X2,X3)),
inference(cp,[status(thm)],[t28224,t45458]) ).
cnf(t288256,plain,
upme(X1,join(X2,X3),lome(a,X2,X3)) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t45587,t121]) ).
cnf(t288257,plain,
upme(X1,join(X2,X3),lome(a,X2,X3)) = upme(X1,X2,X3),
inference(step,[status(thm)],[t288256,t31]) ).
cnf(t80971,plain,
upme(X1,join(X2,X3),lome(a,X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288257]) ).
cnf(t103659,plain,
lome(a,X1,X2) = upme(lome(a,X1,X2),X1,X2),
inference(cp,[status(thm)],[t103642,t80971]) ).
cnf(t104264,plain,
upme(lome(a,X1,X2),X1,X2) = lome(a,X1,X2),
inference(orient,[status(thm)],[t103659]) ).
cnf(t104326,plain,
upme(lome(a,X1,X2),X1,X2) = lome(lome(a,X1,X2),X3,join(X1,X2)),
inference(cp,[status(thm)],[t74210,t104264]) ).
cnf(t288560,plain,
lome(a,X1,X2) = lome(lome(a,X1,X2),X3,join(X1,X2)),
inference(step,[status(thm)],[t104326,t104264]) ).
cnf(t116576,plain,
lome(lome(a,X1,X2),X3,join(X1,X2)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t288560]) ).
cnf(t142028,plain,
meet(lome(a,X1,X2),join(X1,X2)) = meet(join(X1,X2),lome(a,X1,X2)),
inference(cp,[status(thm)],[t141910,t116576]) ).
cnf(t288824,plain,
upme(lome(a,X1,X2),X1,X2) = meet(join(X1,X2),lome(a,X1,X2)),
inference(step,[status(thm)],[t142028,t31]) ).
cnf(t288825,plain,
lome(a,X1,X2) = meet(join(X1,X2),lome(a,X1,X2)),
inference(step,[status(thm)],[t288824,t104264]) ).
cnf(t142731,plain,
meet(join(X1,X2),lome(a,X1,X2)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t288825]) ).
cnf(t289939,plain,
upme(a,X1,X2) = lome(a,X1,X2),
inference(step,[status(thm)],[t289938,t142731]) ).
cnf(t281618,plain,
lome(a,X1,X2) = upme(a,X1,X2),
inference(orient,[status(thm)],[t289939]) ).
cnf(t290039,plain,
upme(a,X1,meet(X2,meet(X3,a))) = lome(a,X1,meet(X2,X3)),
inference(step,[status(thm)],[t177723,t281618]) ).
cnf(t290040,plain,
upme(a,X1,meet(X2,meet(X3,a))) = upme(a,X1,meet(X2,X3)),
inference(step,[status(thm)],[t290039,t281618]) ).
cnf(t281801,plain,
upme(a,X1,meet(X2,meet(X3,a))) = upme(a,X1,meet(X2,X3)),
inference(rw,[status(thm)],[t290040]) ).
cnf(t284120,plain,
upme(a,X1,meet(X2,meet(X3,a))) = upme(a,X1,meet(X2,X3)),
inference(orient,[status(thm)],[t281801]) ).
cnf(t103759,plain,
upme(X1,X2,meet(X3,Y3)) = lome(X1,meet(X3,Y3),lojo(X2,X3,Y3)),
inference(cp,[status(thm)],[t103717,t55]) ).
cnf(t199531,plain,
lome(X1,meet(X2,X3),lojo(Y3,X2,X3)) = upme(X1,Y3,meet(X2,X3)),
inference(orient,[status(thm)],[t103759]) ).
cnf(t252287,plain,
lojo(meet(X1,X2),X2,X3) = upme(X2,meet(X2,X1),meet(X2,X3)),
inference(cp,[status(thm)],[t252210,t15]) ).
cnf(t289665,plain,
lojo(meet(X1,X2),X2,X3) = meet(X2,lome(X2,X1,X3)),
inference(step,[status(thm)],[t252287,t5229]) ).
cnf(t289666,plain,
lojo(meet(X1,X2),X2,X3) = lome(X2,X1,X3),
inference(step,[status(thm)],[t289665,t59345]) ).
cnf(t252651,plain,
lojo(meet(X1,X2),X2,X3) = lome(X2,X1,X3),
inference(orient,[status(thm)],[t289666]) ).
cnf(t252824,plain,
upme(X1,meet(X2,X3),meet(X3,Y3)) = lome(X1,meet(X3,Y3),lome(X3,X2,Y3)),
inference(cp,[status(thm)],[t199531,t252651]) ).
cnf(t406,plain,
lojo(X1,X2,X3) = upjo(lojo(X1,X2,X3),Y3,upjo(X1,meet(X2,X3),Y4)),
inference(cp,[status(thm)],[t280,t396]) ).
cnf(t288120,plain,
lojo(X1,X2,X3) = upjo(lojo(X1,X2,X3),Y3,upjo(X1,Y4,meet(X2,X3))),
inference(step,[status(thm)],[t406,t52112]) ).
cnf(t70421,plain,
upjo(lojo(X1,X2,X3),Y3,upjo(X1,Y4,meet(X2,X3))) = lojo(X1,X2,X3),
inference(orient,[status(thm)],[t288120]) ).
cnf(t64007,plain,
join(X1,X2) = lojo(X2,join(X1,X2),lojo(X1,X3,Y3)),
inference(cp,[status(thm)],[t63960,t41195]) ).
cnf(t64118,plain,
lojo(X1,join(X2,X1),lojo(X2,X3,Y3)) = join(X2,X1),
inference(orient,[status(thm)],[t64007]) ).
cnf(t70451,plain,
lojo(X1,join(X2,X1),lojo(X2,X3,Y3)) = upjo(join(X2,X1),Y4,upjo(X1,Y5,meet(join(X2,X1),lojo(X2,X3,Y3)))),
inference(cp,[status(thm)],[t70421,t64118]) ).
cnf(t70677,plain,
upjo(join(X1,X2),X3,upjo(X2,X1,Y3)) = join(X1,X2),
inference(orient,[status(thm)],[t70451]) ).
cnf(t70679,plain,
join(X1,X2) = join(join(X1,X2),upjo(X2,X1,X3)),
inference(cp,[status(thm)],[t70677,t135]) ).
cnf(t70819,plain,
join(join(X1,X2),upjo(X2,X1,X3)) = join(X1,X2),
inference(orient,[status(thm)],[t70679]) ).
cnf(t103766,plain,
upme(X1,join(X2,X3),upjo(X3,X2,Y3)) = lome(X1,upjo(X3,X2,Y3),join(X2,X3)),
inference(cp,[status(thm)],[t103717,t70819]) ).
cnf(t70954,plain,
upme(X1,join(X2,X3),upjo(X3,X2,Y3)) = lome(X1,join(X2,X3),join(X2,X3)),
inference(cp,[status(thm)],[t28224,t70819]) ).
cnf(t288344,plain,
upme(X1,join(X2,X3),upjo(X3,X2,Y3)) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t70954,t121]) ).
cnf(t288345,plain,
upme(X1,join(X2,X3),upjo(X3,X2,Y3)) = upme(X1,X2,X3),
inference(step,[status(thm)],[t288344,t31]) ).
cnf(t91955,plain,
upme(X1,join(X2,X3),upjo(X3,X2,Y3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288345]) ).
cnf(t288547,plain,
upme(X1,X2,X3) = lome(X1,upjo(X3,X2,Y3),join(X2,X3)),
inference(step,[status(thm)],[t103766,t91955]) ).
cnf(t288548,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),upjo(X3,X2,Y3)),
inference(step,[status(thm)],[t288547,t59453]) ).
cnf(t115472,plain,
lome(X1,join(X2,X3),upjo(X3,X2,Y3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288548]) ).
cnf(t119327,plain,
upme(lome(X1,X2,join(X3,Y3)),X3,Y3) = upme(lome(X1,X2,join(X3,Y3)),X3,upme(X1,X3,Y3)),
inference(cp,[status(thm)],[t104099,t119228]) ).
cnf(t288615,plain,
upme(X1,X3,Y3) = upme(lome(X1,X2,join(X3,Y3)),X3,upme(X1,X3,Y3)),
inference(step,[status(thm)],[t119327,t119228]) ).
cnf(t538,plain,
upjo(upme(X1,X2,X3),meet(X1,Y3),Y4) = upme(lome(X1,join(X2,X3),Y3),upme(X1,X2,X3),Y4),
inference(cp,[status(thm)],[t396,t528]) ).
cnf(t288584,plain,
upjo(upme(X1,X2,X3),Y4,meet(X1,Y3)) = upme(lome(X1,join(X2,X3),Y3),upme(X1,X2,X3),Y4),
inference(step,[status(thm)],[t538,t52112]) ).
cnf(t288585,plain,
upjo(upme(X1,X2,X3),Y4,meet(X1,Y3)) = upme(lome(X1,join(X2,X3),Y3),Y4,upme(X1,X2,X3)),
inference(step,[status(thm)],[t288584,t87]) ).
cnf(t288586,plain,
upjo(upme(X1,X2,X3),Y4,meet(X1,Y3)) = upme(lome(X1,Y3,join(X2,X3)),Y4,upme(X1,X2,X3)),
inference(step,[status(thm)],[t288585,t59453]) ).
cnf(t117561,plain,
upme(lome(X1,X2,join(X3,Y3)),Y4,upme(X1,X3,Y3)) = upjo(upme(X1,X3,Y3),Y4,meet(X1,X2)),
inference(orient,[status(thm)],[t288586]) ).
cnf(t288616,plain,
upme(X1,X3,Y3) = upjo(upme(X1,X3,Y3),X3,meet(X1,X2)),
inference(step,[status(thm)],[t288615,t117561]) ).
cnf(t119829,plain,
upjo(upme(X1,X2,X3),X2,meet(X1,Y3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t288616]) ).
cnf(t119952,plain,
upme(X1,upme(X2,X1,X3),meet(X2,Y3)) = meet(X1,upme(X2,X1,X3)),
inference(cp,[status(thm)],[t77076,t119829]) ).
cnf(t288618,plain,
upme(X1,meet(X2,Y3),upme(X2,X1,X3)) = meet(X1,upme(X2,X1,X3)),
inference(step,[status(thm)],[t119952,t87]) ).
cnf(t288619,plain,
upme(X1,meet(X2,Y3),upme(X2,X1,X3)) = upme(meet(X1,X2),X1,X3),
inference(step,[status(thm)],[t288618,t33621]) ).
cnf(t288620,plain,
upme(X1,meet(X2,Y3),upme(X2,X1,X3)) = meet(X1,X2),
inference(step,[status(thm)],[t288619,t11881]) ).
cnf(t120166,plain,
upme(X1,meet(X2,X3),upme(X2,X1,Y3)) = meet(X1,X2),
inference(orient,[status(thm)],[t288620]) ).
cnf(t120244,plain,
meet(X1,X2) = upme(X1,meet(X2,X3),lome(X2,X1,a)),
inference(cp,[status(thm)],[t120166,t22373]) ).
cnf(t121307,plain,
upme(X1,meet(X2,X3),lome(X2,X1,a)) = meet(X1,X2),
inference(orient,[status(thm)],[t120244]) ).
cnf(t121392,plain,
upme(X1,meet(X2,X3),lome(X2,X1,a)) = upjo(meet(X1,X2),meet(X2,X3),meet(X1,Y3)),
inference(cp,[status(thm)],[t119829,t121307]) ).
cnf(t288933,plain,
meet(X1,X2) = upjo(meet(X1,X2),meet(X2,X3),meet(X1,Y3)),
inference(step,[status(thm)],[t121392,t121307]) ).
cnf(t288934,plain,
meet(X1,X2) = upjo(meet(X1,X2),meet(X1,Y3),meet(X2,X3)),
inference(step,[status(thm)],[t288933,t52112]) ).
cnf(t153692,plain,
upjo(meet(X1,X2),meet(X1,X3),meet(X2,Y3)) = meet(X1,X2),
inference(orient,[status(thm)],[t288934]) ).
cnf(t153874,plain,
upme(X1,meet(X2,X3),meet(X2,Y3)) = lome(X1,join(meet(X2,X3),meet(X2,Y3)),meet(X2,Y3)),
inference(cp,[status(thm)],[t115472,t153692]) ).
cnf(t289491,plain,
meet(X1,lome(X2,X3,Y3)) = lome(X1,join(meet(X2,X3),meet(X2,Y3)),meet(X2,Y3)),
inference(step,[status(thm)],[t153874,t5229]) ).
cnf(t289492,plain,
meet(X1,lome(X2,X3,Y3)) = lome(X1,lojo(meet(X2,X3),X2,Y3),meet(X2,Y3)),
inference(step,[status(thm)],[t289491,t55]) ).
cnf(t289493,plain,
meet(X1,lome(X2,X3,Y3)) = lome(X1,lome(X2,X3,Y3),meet(X2,Y3)),
inference(step,[status(thm)],[t289492,t80]) ).
cnf(t289494,plain,
meet(X1,lome(X2,X3,Y3)) = lome(X1,meet(X2,Y3),lome(X2,X3,Y3)),
inference(step,[status(thm)],[t289493,t59453]) ).
cnf(t226600,plain,
lome(X1,meet(X2,X3),lome(X2,Y3,X3)) = meet(X1,lome(X2,Y3,X3)),
inference(orient,[status(thm)],[t289494]) ).
cnf(t289682,plain,
upme(X1,meet(X2,X3),meet(X3,Y3)) = meet(X1,lome(X3,X2,Y3)),
inference(step,[status(thm)],[t252824,t226600]) ).
cnf(t254134,plain,
upme(X1,meet(X2,X3),meet(X3,Y3)) = meet(X1,lome(X3,X2,Y3)),
inference(orient,[status(thm)],[t289682]) ).
cnf(t284129,plain,
upme(a,meet(X1,X2),meet(X2,X3)) = meet(a,lome(X2,X1,meet(X3,a))),
inference(cp,[status(thm)],[t284120,t254134]) ).
cnf(t290090,plain,
meet(a,lome(X2,X1,X3)) = meet(a,lome(X2,X1,meet(X3,a))),
inference(step,[status(thm)],[t284129,t254134]) ).
cnf(t284394,plain,
meet(a,lome(X1,X2,meet(X3,a))) = meet(a,lome(X1,X2,X3)),
inference(orient,[status(thm)],[t290090]) ).
cnf(t103978,plain,
lojo(X1,X2,join(X1,X3)) = lome(lome(join(X1,X3),X1,X2),X1,X2),
inference(cp,[status(thm)],[t103949,t103184]) ).
cnf(t289264,plain,
lome(join(X1,X3),X1,X2) = lome(lome(join(X1,X3),X1,X2),X1,X2),
inference(step,[status(thm)],[t103978,t103184]) ).
cnf(t199899,plain,
lome(lome(join(X1,X2),X1,X3),X1,X3) = lome(join(X1,X2),X1,X3),
inference(orient,[status(thm)],[t289264]) ).
cnf(t284407,plain,
meet(a,lome(lome(join(X1,X2),X1,meet(X3,a)),X1,X3)) = meet(a,lome(join(X1,X2),X1,meet(X3,a))),
inference(cp,[status(thm)],[t284394,t199899]) ).
cnf(t290091,plain,
meet(a,lome(lojo(X1,X3,upme(a,X1,X2)),X1,X3)) = meet(a,lome(join(X1,X2),X1,meet(X3,a))),
inference(step,[status(thm)],[t284407,t129237]) ).
cnf(t290092,plain,
meet(a,lome(lojo(X1,X3,meet(X2,a)),X1,X3)) = meet(a,lome(join(X1,X2),X1,meet(X3,a))),
inference(step,[status(thm)],[t290091,t230480]) ).
cnf(t290093,plain,
meet(a,lojo(X1,X3,meet(X2,a))) = meet(a,lome(join(X1,X2),X1,meet(X3,a))),
inference(step,[status(thm)],[t290092,t103949]) ).
cnf(t290094,plain,
upme(a,X1,meet(X3,meet(X2,a))) = meet(a,lome(join(X1,X2),X1,meet(X3,a))),
inference(step,[status(thm)],[t290093,t253]) ).
cnf(t290095,plain,
upme(a,X1,meet(X3,X2)) = meet(a,lome(join(X1,X2),X1,meet(X3,a))),
inference(step,[status(thm)],[t290094,t284120]) ).
cnf(t290096,plain,
upme(a,X1,meet(X3,X2)) = meet(a,lome(join(X1,X2),X1,X3)),
inference(step,[status(thm)],[t290095,t284394]) ).
cnf(t290097,plain,
upme(a,X1,meet(X3,X2)) = upme(a,X1,upme(X3,X1,X2)),
inference(step,[status(thm)],[t290096,t129437]) ).
cnf(t284583,plain,
upme(a,X1,upme(X2,X1,X3)) = upme(a,X1,meet(X2,X3)),
inference(orient,[status(thm)],[t290097]) ).
cnf(t284736,plain,
upme(a,X1,meet(join(X2,X1),X3)) = upme(a,X1,upjo(X1,X2,X3)),
inference(cp,[status(thm)],[t284583,t209644]) ).
cnf(t290098,plain,
upme(a,X1,meet(X3,join(X2,X1))) = upme(a,X1,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t284736,t15]) ).
cnf(t290099,plain,
upme(a,X1,upme(X3,X2,X1)) = upme(a,X1,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t290098,t31]) ).
cnf(t290100,plain,
upme(a,X1,upme(X3,X1,X2)) = upme(a,X1,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t290099,t87]) ).
cnf(t290101,plain,
upme(a,X1,meet(X3,X2)) = upme(a,X1,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t290100,t284583]) ).
cnf(t290102,plain,
upme(a,X1,meet(X2,X3)) = upme(a,X1,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t290101,t15]) ).
cnf(t52097,plain,
upme(X1,X2,upjo(X2,X3,Y3)) = meet(X1,upjo(X2,X3,Y3)),
inference(cp,[status(thm)],[t31,t52042]) ).
cnf(t52973,plain,
upme(X1,X2,upjo(X2,X3,Y3)) = meet(X1,upjo(X2,X3,Y3)),
inference(orient,[status(thm)],[t52097]) ).
cnf(t290103,plain,
upme(a,X1,meet(X2,X3)) = meet(a,upjo(X1,X2,X3)),
inference(step,[status(thm)],[t290102,t52973]) ).
cnf(t284812,plain,
meet(a,upjo(X1,X2,X3)) = upme(a,X1,meet(X2,X3)),
inference(orient,[status(thm)],[t290103]) ).
cnf(t285174,plain,
upme(meet(X1,a),X2,X3) = meet(X1,upme(a,X2,meet(X3,X1))),
inference(cp,[status(thm)],[t145310,t284812]) ).
cnf(t290124,plain,
upme(meet(X1,a),X2,X3) = upme(meet(X1,a),X2,meet(X3,X1)),
inference(step,[status(thm)],[t285174,t33621]) ).
cnf(t290125,plain,
upme(meet(X1,a),X2,X3) = upme(meet(X1,a),X2,meet(X1,X3)),
inference(step,[status(thm)],[t290124,t15]) ).
cnf(t209752,plain,
upjo(meet(X1,X2),X3,Y3) = upme(lojo(X3,X1,X2),meet(X1,X2),Y3),
inference(cp,[status(thm)],[t209644,t55]) ).
cnf(t289723,plain,
upjo(meet(X1,X2),X3,Y3) = upme(lojo(X3,X1,X2),Y3,meet(X1,X2)),
inference(step,[status(thm)],[t209752,t87]) ).
cnf(t261232,plain,
upme(lojo(X1,X2,X3),Y3,meet(X2,X3)) = upjo(meet(X2,X3),X1,Y3),
inference(orient,[status(thm)],[t289723]) ).
cnf(t261254,plain,
upjo(meet(X1,X2),X2,X3) = upme(X2,X3,meet(X1,X2)),
inference(cp,[status(thm)],[t261232,t252519]) ).
cnf(t261644,plain,
upjo(meet(X1,X2),X2,X3) = upme(X2,X3,meet(X1,X2)),
inference(orient,[status(thm)],[t261254]) ).
cnf(t284923,plain,
upme(a,meet(X1,X2),meet(X2,X3)) = meet(a,upme(X2,X3,meet(X1,X2))),
inference(cp,[status(thm)],[t284812,t261644]) ).
cnf(t285880,plain,
upme(meet(X1,a),X2,meet(X1,X3)) = meet(a,lome(X1,X3,X2)),
inference(orient,[status(thm)],[t284923]) ).
cnf(t290126,plain,
upme(meet(X1,a),X2,X3) = meet(a,lome(X1,X3,X2)),
inference(step,[status(thm)],[t290125,t285880]) ).
cnf(t290127,plain,
upme(meet(X1,a),X2,X3) = meet(a,lome(X1,X2,X3)),
inference(step,[status(thm)],[t290126,t19398]) ).
cnf(t286106,plain,
meet(a,lome(X1,X2,X3)) = upme(meet(X1,a),X2,X3),
inference(orient,[status(thm)],[t290127]) ).
cnf(t69319,plain,
meet(X1,lome(meet(X1,X2),X3,Y3)) = meet(meet(X1,X2),lome(meet(X1,X2),X3,Y3)),
inference(cp,[status(thm)],[t69294,t148]) ).
cnf(t288118,plain,
meet(X1,lome(meet(X1,X2),X3,Y3)) = lome(meet(X1,X2),X3,Y3),
inference(step,[status(thm)],[t69319,t59345]) ).
cnf(t70161,plain,
meet(X1,lome(meet(X1,X2),X3,Y3)) = lome(meet(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t288118]) ).
cnf(t286116,plain,
upme(meet(meet(a,X1),a),X2,X3) = lome(meet(a,X1),X2,X3),
inference(cp,[status(thm)],[t286106,t70161]) ).
cnf(t290134,plain,
upme(meet(a,meet(a,X1)),X2,X3) = lome(meet(a,X1),X2,X3),
inference(step,[status(thm)],[t286116,t15]) ).
cnf(t290135,plain,
upme(meet(a,X1),X2,X3) = lome(meet(a,X1),X2,X3),
inference(step,[status(thm)],[t290134,t148]) ).
cnf(t290136,plain,
upme(meet(X1,a),X2,X3) = lome(meet(a,X1),X2,X3),
inference(step,[status(thm)],[t290135,t15]) ).
cnf(t290137,plain,
upme(meet(X1,a),X2,X3) = lome(meet(X1,a),X2,X3),
inference(step,[status(thm)],[t290136,t15]) ).
cnf(t286601,plain,
lome(meet(X1,a),X2,X3) = upme(meet(X1,a),X2,X3),
inference(orient,[status(thm)],[t290137]) ).
cnf(goal_0,negated_conjecture,
upme(meet(a,z1),z2,z3) != lome(meet(a,z1),z2,z3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
upme(meet(a,z1),z3,z2) != lome(meet(a,z1),z2,z3),
inference(rw,[status(thm)],[goal_0,t87]) ).
cnf(g0_1,plain,
upme(meet(z1,a),z3,z2) != lome(meet(a,z1),z2,z3),
inference(rw,[status(thm)],[g0_0,t15]) ).
cnf(g0_2,plain,
upme(meet(z1,a),z3,z2) != lome(meet(a,z1),z3,z2),
inference(rw,[status(thm)],[g0_1,t59453]) ).
cnf(g0_3,plain,
upme(meet(z1,a),z3,z2) != lome(meet(z1,a),z3,z2),
inference(rw,[status(thm)],[g0_2,t15]) ).
cnf(g0_4,plain,
upme(meet(z1,a),z3,z2) != upme(meet(z1,a),z3,z2),
inference(rw,[status(thm)],[g0_3,t286601]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT399-2 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.36 % Computer : n016.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.01/0.36 % CPULimit : 300
% 0.01/0.36 % WCLimit : 300
% 0.01/0.36 % DateTime : Wed Sep 23 21:38:27 UTC 2026
% 0.01/0.37 % CPUTime :
% 0.01/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 166.32/21.55 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 166.32/21.55 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------