%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT399-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n008.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 68.59s 10.92s
% Output : CNFRefutation 68.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 10
% Syntax : Number of clauses : 339 ( 339 unt; 0 nHn; 5 RR)
% Number of literals : 339 ( 338 equ; 4 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 : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 1017 ( 136 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
meet(X1,join(X2,X3)) = upme(X1,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
meet(X1,join(X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t4]) ).
cnf(t0,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t36,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t0]) ).
cnf(t39,plain,
upme(X1,X2,X3) = meet(X1,join(X3,X2)),
inference(cp,[status(thm)],[t21,t36]) ).
cnf(t199452,plain,
upme(X1,X2,X3) = upme(X1,X3,X2),
inference(step,[status(thm)],[t39,t21]) ).
cnf(t356,plain,
upme(X1,X2,X3) = upme(X1,X3,X2),
inference(orient,[status(thm)],[t199452]) ).
cnf(t2,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t5,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t41,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t5]) ).
cnf(t46,plain,
upme(X1,join(X2,X3),Y3) = meet(X1,join(X2,join(X3,Y3))),
inference(cp,[status(thm)],[t21,t41]) ).
cnf(t199463,plain,
upme(X1,join(X2,X3),Y3) = upme(X1,X2,join(X3,Y3)),
inference(step,[status(thm)],[t46,t21]) ).
cnf(t917,plain,
upme(X1,join(X2,X3),Y3) = upme(X1,X2,join(X3,Y3)),
inference(orient,[status(thm)],[t199463]) ).
cnf(t3,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t199425,plain,
upme(X1,X1,X2) = X1,
inference(step,[status(thm)],[t9,t21]) ).
cnf(t27,plain,
upme(X1,X1,X2) = X1,
inference(rw,[status(thm)],[t199425]) ).
cnf(t58,plain,
upme(X1,X1,X2) = X1,
inference(orient,[status(thm)],[t27]) ).
cnf(t357,plain,
upme(X1,X2,X1) = X1,
inference(cp,[status(thm)],[t356,t58]) ).
cnf(t367,plain,
upme(X1,X2,X1) = X1,
inference(orient,[status(thm)],[t357]) ).
cnf(t918,plain,
upme(X1,X2,join(X3,X1)) = X1,
inference(cp,[status(thm)],[t917,t367]) ).
cnf(t955,plain,
upme(X1,X2,join(X3,X1)) = X1,
inference(orient,[status(thm)],[t918]) ).
cnf(t7,axiom,
join(meet(X1,X2),meet(X1,X3)) = lome(X1,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t47,plain,
join(meet(X1,X2),meet(X1,X3)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t7]) ).
cnf(t978,plain,
meet(X1,X2) = upme(meet(X1,X2),X3,lome(X1,Y3,X2)),
inference(cp,[status(thm)],[t955,t47]) ).
cnf(t7377,plain,
upme(meet(X1,X2),X3,lome(X1,Y3,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t978]) ).
cnf(t1,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t10,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t26,plain,
X1 = join(X1,upme(X1,X2,X3)),
inference(cp,[status(thm)],[t10,t21]) ).
cnf(t67,plain,
join(X1,upme(X1,X2,X3)) = X1,
inference(orient,[status(thm)],[t26]) ).
cnf(t69,plain,
X1 = join(X1,X1),
inference(cp,[status(thm)],[t67,t58]) ).
cnf(t74,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t69]) ).
cnf(t78,plain,
upme(X1,X2,X2) = meet(X1,X2),
inference(cp,[status(thm)],[t21,t74]) ).
cnf(t81,plain,
upme(X1,X2,X2) = meet(X1,X2),
inference(orient,[status(thm)],[t78]) ).
cnf(t7380,plain,
meet(X1,X2) = meet(meet(X1,X2),lome(X1,X3,X2)),
inference(cp,[status(thm)],[t7377,t81]) ).
cnf(t6,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t199557,plain,
meet(X1,X2) = meet(X1,meet(X2,lome(X1,X3,X2))),
inference(step,[status(thm)],[t7380,t15]) ).
cnf(t7436,plain,
meet(X1,meet(X2,lome(X1,X3,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t199557]) ).
cnf(t19,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t15,t13]) ).
cnf(t199480,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t19,t15]) ).
cnf(t1419,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t199480]) ).
cnf(t7440,plain,
meet(X1,X2) = meet(X2,meet(X1,lome(X1,X3,X2))),
inference(cp,[status(thm)],[t7436,t1419]) ).
cnf(t77,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t41,t74]) ).
cnf(t93,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t77]) ).
cnf(t98,plain,
upme(X1,X2,join(X2,X3)) = meet(X1,join(X2,X3)),
inference(cp,[status(thm)],[t21,t93]) ).
cnf(t199439,plain,
upme(X1,X2,join(X2,X3)) = upme(X1,X2,X3),
inference(step,[status(thm)],[t98,t21]) ).
cnf(t234,plain,
upme(X1,X2,join(X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t199439]) ).
cnf(t44,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t41,t10]) ).
cnf(t470,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t44]) ).
cnf(t472,plain,
join(X1,meet(X1,X2)) = join(X1,lome(X1,X3,X2)),
inference(cp,[status(thm)],[t470,t47]) ).
cnf(t199455,plain,
X1 = join(X1,lome(X1,X3,X2)),
inference(step,[status(thm)],[t472,t10]) ).
cnf(t491,plain,
join(X1,lome(X1,X2,X3)) = X1,
inference(orient,[status(thm)],[t199455]) ).
cnf(t495,plain,
upme(X1,X2,lome(X2,X3,Y3)) = upme(X1,X2,X2),
inference(cp,[status(thm)],[t234,t491]) ).
cnf(t199457,plain,
upme(X1,X2,lome(X2,X3,Y3)) = meet(X1,X2),
inference(step,[status(thm)],[t495,t81]) ).
cnf(t610,plain,
upme(X1,X2,lome(X2,X3,Y3)) = meet(X1,X2),
inference(orient,[status(thm)],[t199457]) ).
cnf(t611,plain,
meet(lome(X1,X2,X3),X1) = lome(X1,X2,X3),
inference(cp,[status(thm)],[t610,t367]) ).
cnf(t199458,plain,
meet(X1,lome(X1,X2,X3)) = lome(X1,X2,X3),
inference(step,[status(thm)],[t611,t13]) ).
cnf(t615,plain,
meet(X1,lome(X1,X2,X3)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t199458]) ).
cnf(t199558,plain,
meet(X1,X2) = meet(X2,lome(X1,X3,X2)),
inference(step,[status(thm)],[t7440,t615]) ).
cnf(t7573,plain,
meet(X1,lome(X2,X3,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t199558]) ).
cnf(t14,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t10,t13]) ).
cnf(t59,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t64,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t41,t59]) ).
cnf(t502,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t64]) ).
cnf(t61,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t59,t41]) ).
cnf(t199483,plain,
join(X1,X2) = join(X1,join(X2,upme(X3,X1,X2))),
inference(step,[status(thm)],[t61,t21]) ).
cnf(t1579,plain,
join(X1,join(X2,upme(X3,X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t199483]) ).
cnf(t1601,plain,
join(X1,join(X2,upme(X3,meet(Y3,X1),X2))) = join(X1,join(meet(Y3,X1),X2)),
inference(cp,[status(thm)],[t502,t1579]) ).
cnf(t199886,plain,
join(X1,join(X2,upme(X3,meet(Y3,X1),X2))) = join(X1,X2),
inference(step,[status(thm)],[t1601,t502]) ).
cnf(t71876,plain,
join(X1,join(X2,upme(X3,meet(Y3,X1),X2))) = join(X1,X2),
inference(orient,[status(thm)],[t199886]) ).
cnf(t45,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t41,t36]) ).
cnf(t199524,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t45,t41]) ).
cnf(t4537,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t199524]) ).
cnf(t71893,plain,
join(X1,X2) = join(X2,join(X1,upme(X3,meet(Y3,X1),X2))),
inference(cp,[status(thm)],[t71876,t4537]) ).
cnf(t93381,plain,
join(X1,join(X2,upme(X3,meet(Y3,X2),X1))) = join(X2,X1),
inference(orient,[status(thm)],[t71893]) ).
cnf(t8,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t199426,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)],[t8,t21]) ).
cnf(t199427,plain,
upme(join(meet(a,meet(X1,X2)),X3),meet(meet(a,X1),X3),X2) = join(upme(meet(a,X1),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t199426,t15]) ).
cnf(t199428,plain,
upme(join(meet(a,meet(X1,X2)),X3),meet(a,meet(X1,X3)),X2) = join(upme(meet(a,X1),X2,X3),meet(X2,X3)),
inference(step,[status(thm)],[t199427,t15]) ).
cnf(t28,plain,
upme(join(meet(a,meet(X1,X2)),X3),meet(a,meet(X1,X3)),X2) = join(upme(meet(a,X1),X2,X3),meet(X2,X3)),
inference(orient,[status(thm)],[t199428]) ).
cnf(t199429,plain,
upme(join(meet(a,meet(X1,X2)),X3),meet(a,meet(X1,X3)),X2) = join(meet(X2,X3),upme(meet(a,X1),X2,X3)),
inference(step,[status(thm)],[t28,t36]) ).
cnf(t37,plain,
upme(join(meet(a,meet(X1,X2)),X3),meet(a,meet(X1,X3)),X2) = join(meet(X2,X3),upme(meet(a,X1),X2,X3)),
inference(orient,[status(thm)],[t199429]) ).
cnf(t57,plain,
join(meet(X1,meet(a,X2)),upme(meet(a,X3),X1,meet(a,X2))) = upme(lome(a,meet(X3,X1),X2),meet(a,meet(X3,meet(a,X2))),X1),
inference(cp,[status(thm)],[t37,t47]) ).
cnf(t23,plain,
upme(X1,X2,X3) = meet(join(X2,X3),X1),
inference(cp,[status(thm)],[t21,t13]) ).
cnf(t130,plain,
meet(join(X1,X2),X3) = upme(X3,X1,X2),
inference(orient,[status(thm)],[t23]) ).
cnf(t144,plain,
meet(join(X1,X2),meet(X3,Y3)) = meet(upme(X3,X1,X2),Y3),
inference(cp,[status(thm)],[t15,t130]) ).
cnf(t199465,plain,
upme(meet(X3,Y3),X1,X2) = meet(upme(X3,X1,X2),Y3),
inference(step,[status(thm)],[t144,t130]) ).
cnf(t1031,plain,
meet(upme(X1,X2,X3),Y3) = upme(meet(X1,Y3),X2,X3),
inference(orient,[status(thm)],[t199465]) ).
cnf(t40,plain,
join(meet(X1,X2),upme(meet(a,X3),X1,X2)) = upme(join(X2,meet(a,meet(X3,X1))),meet(a,meet(X3,X2)),X1),
inference(cp,[status(thm)],[t37,t36]) ).
cnf(t37393,plain,
upme(join(X1,meet(a,meet(X2,X3))),meet(a,meet(X2,X1)),X3) = join(meet(X3,X1),upme(meet(a,X2),X3,X1)),
inference(orient,[status(thm)],[t40]) ).
cnf(t37439,plain,
join(meet(X1,a),upme(meet(a,X2),X1,a)) = upme(a,meet(a,meet(X2,a)),X1),
inference(cp,[status(thm)],[t37393,t10]) ).
cnf(t22,plain,
upme(meet(X1,X2),X3,Y3) = meet(X1,meet(X2,join(X3,Y3))),
inference(cp,[status(thm)],[t21,t15]) ).
cnf(t199462,plain,
upme(meet(X1,X2),X3,Y3) = meet(X1,upme(X2,X3,Y3)),
inference(step,[status(thm)],[t22,t21]) ).
cnf(t804,plain,
meet(X1,upme(X2,X3,Y3)) = upme(meet(X1,X2),X3,Y3),
inference(orient,[status(thm)],[t199462]) ).
cnf(t808,plain,
upme(meet(X1,X2),X3,X2) = meet(X1,X2),
inference(cp,[status(thm)],[t804,t367]) ).
cnf(t849,plain,
upme(meet(X1,X2),X3,X2) = meet(X1,X2),
inference(orient,[status(thm)],[t808]) ).
cnf(t860,plain,
meet(X1,X2) = upme(meet(X2,X1),X3,X2),
inference(cp,[status(thm)],[t849,t13]) ).
cnf(t874,plain,
upme(meet(X1,X2),X3,X1) = meet(X2,X1),
inference(orient,[status(thm)],[t860]) ).
cnf(t199713,plain,
join(meet(X1,a),meet(X2,a)) = upme(a,meet(a,meet(X2,a)),X1),
inference(step,[status(thm)],[t37439,t874]) ).
cnf(t51,plain,
lome(X1,X2,X3) = join(meet(X2,X1),meet(X1,X3)),
inference(cp,[status(thm)],[t47,t13]) ).
cnf(t1099,plain,
join(meet(X1,X2),meet(X2,X3)) = lome(X2,X1,X3),
inference(orient,[status(thm)],[t51]) ).
cnf(t1121,plain,
lome(X1,X2,X3) = join(meet(X2,X1),meet(X3,X1)),
inference(cp,[status(thm)],[t1099,t13]) ).
cnf(t1289,plain,
join(meet(X1,X2),meet(X3,X2)) = lome(X2,X1,X3),
inference(orient,[status(thm)],[t1121]) ).
cnf(t199714,plain,
lome(a,X1,X2) = upme(a,meet(a,meet(X2,a)),X1),
inference(step,[status(thm)],[t199713,t1289]) ).
cnf(t82,plain,
meet(X1,X1) = X1,
inference(cp,[status(thm)],[t81,t58]) ).
cnf(t84,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t82]) ).
cnf(t87,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t15,t84]) ).
cnf(t100,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t87]) ).
cnf(t104,plain,
meet(X1,X2) = meet(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t100,t13]) ).
cnf(t118,plain,
meet(X1,meet(X2,X1)) = meet(X1,X2),
inference(orient,[status(thm)],[t104]) ).
cnf(t199715,plain,
lome(a,X1,X2) = upme(a,meet(a,X2),X1),
inference(step,[status(thm)],[t199714,t118]) ).
cnf(t37739,plain,
upme(a,meet(a,X1),X2) = lome(a,X2,X1),
inference(orient,[status(thm)],[t199715]) ).
cnf(t37776,plain,
lome(a,X1,X2) = upme(a,X1,meet(a,X2)),
inference(cp,[status(thm)],[t37739,t356]) ).
cnf(t37976,plain,
upme(a,X1,meet(a,X2)) = lome(a,X1,X2),
inference(orient,[status(thm)],[t37776]) ).
cnf(t38024,plain,
upme(meet(a,X1),X2,meet(a,X3)) = meet(lome(a,X2,X3),X1),
inference(cp,[status(thm)],[t1031,t37976]) ).
cnf(t41962,plain,
upme(meet(a,X1),X2,meet(a,X3)) = meet(lome(a,X2,X3),X1),
inference(orient,[status(thm)],[t38024]) ).
cnf(t199799,plain,
join(meet(X1,meet(a,X2)),meet(lome(a,X1,X2),X3)) = upme(lome(a,meet(X3,X1),X2),meet(a,meet(X3,meet(a,X2))),X1),
inference(step,[status(thm)],[t57,t41962]) ).
cnf(t122,plain,
meet(X1,meet(meet(X2,X1),X3)) = meet(meet(X1,X2),X3),
inference(cp,[status(thm)],[t15,t118]) ).
cnf(t199481,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t122,t15]) ).
cnf(t199482,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t199481,t15]) ).
cnf(t1531,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t199482]) ).
cnf(t199800,plain,
join(meet(X1,meet(a,X2)),meet(lome(a,X1,X2),X3)) = upme(lome(a,meet(X3,X1),X2),meet(a,meet(X3,X2)),X1),
inference(step,[status(thm)],[t199799,t1531]) ).
cnf(t53629,plain,
upme(lome(a,meet(X1,X2),X3),meet(a,meet(X1,X3)),X2) = join(meet(X2,meet(a,X3)),meet(lome(a,X2,X3),X1)),
inference(orient,[status(thm)],[t199800]) ).
cnf(t93503,plain,
join(meet(X1,X2),X3) = join(X3,join(meet(X1,X2),join(meet(X3,meet(a,X2)),meet(lome(a,X3,X2),X1)))),
inference(cp,[status(thm)],[t93381,t53629]) ).
cnf(t97,plain,
join(X1,X2) = join(X1,join(X2,X1)),
inference(cp,[status(thm)],[t93,t36]) ).
cnf(t111,plain,
join(X1,join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t97]) ).
cnf(t473,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,join(meet(X1,X3),X2)),
inference(cp,[status(thm)],[t470,t111]) ).
cnf(t199456,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(step,[status(thm)],[t473,t470]) ).
cnf(t590,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t199456]) ).
cnf(t606,plain,
join(X1,join(join(X2,meet(X1,X3)),Y3)) = join(join(X1,X2),Y3),
inference(cp,[status(thm)],[t41,t590]) ).
cnf(t199708,plain,
join(X1,join(X2,join(meet(X1,X3),Y3))) = join(join(X1,X2),Y3),
inference(step,[status(thm)],[t606,t41]) ).
cnf(t199709,plain,
join(X1,join(X2,join(meet(X1,X3),Y3))) = join(X1,join(X2,Y3)),
inference(step,[status(thm)],[t199708,t41]) ).
cnf(t37164,plain,
join(X1,join(X2,join(meet(X1,X3),Y3))) = join(X1,join(X2,Y3)),
inference(orient,[status(thm)],[t199709]) ).
cnf(t199957,plain,
join(meet(X1,X2),X3) = join(X3,join(meet(X1,X2),meet(lome(a,X3,X2),X1))),
inference(step,[status(thm)],[t93503,t37164]) ).
cnf(t54,plain,
lome(X1,X2,X3) = join(meet(X1,X2),meet(X3,X1)),
inference(cp,[status(thm)],[t47,t13]) ).
cnf(t1141,plain,
join(meet(X1,X2),meet(X3,X1)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t54]) ).
cnf(t199958,plain,
join(meet(X1,X2),X3) = join(X3,lome(X1,X2,lome(a,X3,X2))),
inference(step,[status(thm)],[t199957,t1141]) ).
cnf(t93970,plain,
join(X1,lome(X2,X3,lome(a,X1,X3))) = join(meet(X2,X3),X1),
inference(orient,[status(thm)],[t199958]) ).
cnf(t48,plain,
lome(X1,X2,X3) = join(meet(X1,X3),meet(X1,X2)),
inference(cp,[status(thm)],[t47,t36]) ).
cnf(t199454,plain,
lome(X1,X2,X3) = lome(X1,X3,X2),
inference(step,[status(thm)],[t48,t47]) ).
cnf(t465,plain,
lome(X1,X2,X3) = lome(X1,X3,X2),
inference(orient,[status(thm)],[t199454]) ).
cnf(t94236,plain,
join(meet(X1,X2),X3) = join(X3,lome(X1,X2,lome(a,X2,X3))),
inference(cp,[status(thm)],[t93970,t465]) ).
cnf(t94471,plain,
join(X1,lome(X2,X3,lome(a,X3,X1))) = join(meet(X2,X3),X1),
inference(orient,[status(thm)],[t94236]) ).
cnf(t17,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t13]) ).
cnf(t369,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t17]) ).
cnf(t434,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t59,t369]) ).
cnf(t199453,plain,
meet(X1,X2) = lome(X1,X2,meet(X2,X3)),
inference(step,[status(thm)],[t434,t47]) ).
cnf(t443,plain,
lome(X1,X2,meet(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t199453]) ).
cnf(t449,plain,
meet(X1,join(X2,X3)) = lome(X1,join(X2,X3),upme(Y3,X2,X3)),
inference(cp,[status(thm)],[t443,t130]) ).
cnf(t199618,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),upme(Y3,X2,X3)),
inference(step,[status(thm)],[t449,t21]) ).
cnf(t16541,plain,
lome(X1,join(X2,X3),upme(Y3,X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t199618]) ).
cnf(t16607,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),X2),
inference(cp,[status(thm)],[t16541,t58]) ).
cnf(t199620,plain,
upme(X1,X2,X3) = lome(X1,X2,join(X2,X3)),
inference(step,[status(thm)],[t16607,t465]) ).
cnf(t16793,plain,
lome(X1,X2,join(X2,X3)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t199620]) ).
cnf(t43,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t41,t36]) ).
cnf(t4314,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t43]) ).
cnf(t16865,plain,
upme(X1,X2,join(X3,Y3)) = lome(X1,X2,join(X3,join(Y3,X2))),
inference(cp,[status(thm)],[t16793,t4314]) ).
cnf(t16605,plain,
upme(X1,X2,join(X3,Y3)) = lome(X1,join(X2,join(X3,Y3)),Y3),
inference(cp,[status(thm)],[t16541,t955]) ).
cnf(t199623,plain,
upme(X1,X2,join(X3,Y3)) = lome(X1,Y3,join(X2,join(X3,Y3))),
inference(step,[status(thm)],[t16605,t465]) ).
cnf(t20020,plain,
lome(X1,X2,join(X3,join(Y3,X2))) = upme(X1,X3,join(Y3,X2)),
inference(orient,[status(thm)],[t199623]) ).
cnf(t199634,plain,
upme(X1,X2,join(X3,Y3)) = upme(X1,X3,join(Y3,X2)),
inference(step,[status(thm)],[t16865,t20020]) ).
cnf(t22157,plain,
upme(X1,X2,join(X3,Y3)) = upme(X1,X3,join(Y3,X2)),
inference(orient,[status(thm)],[t199634]) ).
cnf(t37777,plain,
lome(a,join(X1,X2),X3) = upme(a,X2,join(meet(a,X3),X1)),
inference(cp,[status(thm)],[t37739,t22157]) ).
cnf(t39916,plain,
upme(a,X1,join(meet(a,X2),X3)) = lome(a,join(X3,X1),X2),
inference(orient,[status(thm)],[t37777]) ).
cnf(t39943,plain,
lome(a,join(meet(X1,X2),X3),X1) = upme(a,X3,lome(X1,a,X2)),
inference(cp,[status(thm)],[t39916,t1099]) ).
cnf(t199823,plain,
lome(a,X1,join(meet(X1,X2),X3)) = upme(a,X3,lome(X1,a,X2)),
inference(step,[status(thm)],[t39943,t465]) ).
cnf(t57198,plain,
lome(a,X1,join(meet(X1,X2),X3)) = upme(a,X3,lome(X1,a,X2)),
inference(orient,[status(thm)],[t199823]) ).
cnf(t1586,plain,
join(X1,X2) = join(X1,join(X2,upme(X3,X2,X1))),
inference(cp,[status(thm)],[t1579,t356]) ).
cnf(t2430,plain,
join(X1,join(X2,upme(X3,X2,X1))) = join(X1,X2),
inference(orient,[status(thm)],[t1586]) ).
cnf(t107,plain,
join(meet(X1,X2),upme(meet(a,a),X1,X2)) = upme(join(meet(a,X1),X2),meet(a,meet(a,X2)),X1),
inference(cp,[status(thm)],[t37,t100]) ).
cnf(t200024,plain,
join(meet(X1,X2),upme(a,X1,X2)) = upme(join(meet(a,X1),X2),meet(a,meet(a,X2)),X1),
inference(step,[status(thm)],[t107,t84]) ).
cnf(t200025,plain,
join(meet(X1,X2),upme(a,X1,X2)) = upme(join(meet(a,X1),X2),meet(a,X2),X1),
inference(step,[status(thm)],[t200024,t100]) ).
cnf(t113928,plain,
upme(join(meet(a,X1),X2),meet(a,X2),X1) = join(meet(X1,X2),upme(a,X1,X2)),
inference(orient,[status(thm)],[t200025]) ).
cnf(t114296,plain,
join(X1,meet(a,X2)) = join(X1,join(meet(a,X2),join(meet(X1,X2),upme(a,X1,X2)))),
inference(cp,[status(thm)],[t2430,t113928]) ).
cnf(t200026,plain,
join(X1,meet(a,X2)) = join(X1,join(meet(a,X2),upme(a,X1,X2))),
inference(step,[status(thm)],[t114296,t37164]) ).
cnf(t52,plain,
lome(X1,X2,join(X3,Y3)) = join(meet(X1,X2),upme(X1,X3,Y3)),
inference(cp,[status(thm)],[t47,t21]) ).
cnf(t13139,plain,
join(meet(X1,X2),upme(X1,X3,Y3)) = lome(X1,X2,join(X3,Y3)),
inference(orient,[status(thm)],[t52]) ).
cnf(t200027,plain,
join(X1,meet(a,X2)) = join(X1,lome(a,X2,join(X1,X2))),
inference(step,[status(thm)],[t200026,t13139]) ).
cnf(t16599,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),X3),
inference(cp,[status(thm)],[t16541,t367]) ).
cnf(t199619,plain,
upme(X1,X2,X3) = lome(X1,X3,join(X2,X3)),
inference(step,[status(thm)],[t16599,t465]) ).
cnf(t16677,plain,
lome(X1,X2,join(X3,X2)) = upme(X1,X3,X2),
inference(orient,[status(thm)],[t199619]) ).
cnf(t200028,plain,
join(X1,meet(a,X2)) = join(X1,upme(a,X1,X2)),
inference(step,[status(thm)],[t200027,t16677]) ).
cnf(t114310,plain,
join(X1,upme(a,X1,X2)) = join(X1,meet(a,X2)),
inference(orient,[status(thm)],[t200028]) ).
cnf(t114508,plain,
upme(a,upme(a,meet(X1,X2),X3),lome(X1,a,X2)) = lome(a,X1,join(meet(X1,X2),meet(a,X3))),
inference(cp,[status(thm)],[t57198,t114310]) ).
cnf(t37794,plain,
lome(a,X1,join(X2,X3)) = upme(a,upme(a,X2,X3),X1),
inference(cp,[status(thm)],[t37739,t21]) ).
cnf(t38186,plain,
upme(a,upme(a,X1,X2),X3) = lome(a,X3,join(X1,X2)),
inference(orient,[status(thm)],[t37794]) ).
cnf(t200032,plain,
lome(a,lome(X1,a,X2),join(meet(X1,X2),X3)) = lome(a,X1,join(meet(X1,X2),meet(a,X3))),
inference(step,[status(thm)],[t114508,t38186]) ).
cnf(t485,plain,
upme(X1,X2,join(meet(X2,X3),Y3)) = upme(X1,X2,join(X2,Y3)),
inference(cp,[status(thm)],[t234,t470]) ).
cnf(t199517,plain,
upme(X1,X2,join(meet(X2,X3),Y3)) = upme(X1,X2,Y3),
inference(step,[status(thm)],[t485,t234]) ).
cnf(t3872,plain,
upme(X1,X2,join(meet(X2,X3),Y3)) = upme(X1,X2,Y3),
inference(orient,[status(thm)],[t199517]) ).
cnf(t3874,plain,
upme(join(meet(X1,X2),X3),X1,X3) = join(meet(X1,X2),X3),
inference(cp,[status(thm)],[t3872,t367]) ).
cnf(t5932,plain,
upme(join(meet(X1,X2),X3),X1,X3) = join(meet(X1,X2),X3),
inference(orient,[status(thm)],[t3874]) ).
cnf(t65,plain,
upme(X1,X2,meet(X3,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t21,t59]) ).
cnf(t165,plain,
upme(X1,X2,meet(X3,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t65]) ).
cnf(t5945,plain,
join(meet(X1,X2),meet(X3,X1)) = meet(join(meet(X1,X2),meet(X3,X1)),X1),
inference(cp,[status(thm)],[t5932,t165]) ).
cnf(t199541,plain,
lome(X1,X2,X3) = meet(join(meet(X1,X2),meet(X3,X1)),X1),
inference(step,[status(thm)],[t5945,t1141]) ).
cnf(t199542,plain,
lome(X1,X2,X3) = upme(X1,meet(X1,X2),meet(X3,X1)),
inference(step,[status(thm)],[t199541,t130]) ).
cnf(t6042,plain,
upme(X1,meet(X1,X2),meet(X3,X1)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t199542]) ).
cnf(t7611,plain,
meet(X1,X2) = meet(X2,lome(X1,X2,X3)),
inference(cp,[status(thm)],[t7573,t465]) ).
cnf(t7719,plain,
meet(X1,lome(X2,X1,X3)) = meet(X2,X1),
inference(orient,[status(thm)],[t7611]) ).
cnf(t7764,plain,
lome(X1,lome(X2,X1,X3),Y3) = upme(X1,meet(X2,X1),meet(Y3,X1)),
inference(cp,[status(thm)],[t6042,t7719]) ).
cnf(t6052,plain,
lome(X1,X2,X3) = upme(X1,meet(X2,X1),meet(X3,X1)),
inference(cp,[status(thm)],[t6042,t13]) ).
cnf(t6105,plain,
upme(X1,meet(X2,X1),meet(X3,X1)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t6052]) ).
cnf(t199562,plain,
lome(X1,lome(X2,X1,X3),Y3) = lome(X1,X2,Y3),
inference(step,[status(thm)],[t7764,t6105]) ).
cnf(t7981,plain,
lome(X1,lome(X2,X1,X3),Y3) = lome(X1,X2,Y3),
inference(orient,[status(thm)],[t199562]) ).
cnf(t200033,plain,
lome(a,X1,join(meet(X1,X2),X3)) = lome(a,X1,join(meet(X1,X2),meet(a,X3))),
inference(step,[status(thm)],[t200032,t7981]) ).
cnf(t200034,plain,
upme(a,X3,lome(X1,a,X2)) = lome(a,X1,join(meet(X1,X2),meet(a,X3))),
inference(step,[status(thm)],[t200033,t57198]) ).
cnf(t200035,plain,
upme(a,X3,lome(X1,a,X2)) = upme(a,meet(a,X3),lome(X1,a,X2)),
inference(step,[status(thm)],[t200034,t57198]) ).
cnf(t200036,plain,
upme(a,X3,lome(X1,a,X2)) = lome(a,lome(X1,a,X2),X3),
inference(step,[status(thm)],[t200035,t37739]) ).
cnf(t200037,plain,
upme(a,X3,lome(X1,a,X2)) = lome(a,X1,X3),
inference(step,[status(thm)],[t200036,t7981]) ).
cnf(t114919,plain,
upme(a,X1,lome(X2,a,X3)) = lome(a,X2,X1),
inference(orient,[status(thm)],[t200037]) ).
cnf(t89,plain,
lome(X1,X2,X1) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t47,t84]) ).
cnf(t199432,plain,
lome(X1,X2,X1) = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t89,t36]) ).
cnf(t199433,plain,
lome(X1,X2,X1) = X1,
inference(step,[status(thm)],[t199432,t10]) ).
cnf(t152,plain,
lome(X1,X2,X1) = X1,
inference(orient,[status(thm)],[t199433]) ).
cnf(t114939,plain,
lome(a,X1,X2) = upme(a,X2,X1),
inference(cp,[status(thm)],[t114919,t152]) ).
cnf(t115065,plain,
lome(a,X1,X2) = upme(a,X2,X1),
inference(orient,[status(thm)],[t114939]) ).
cnf(t200129,plain,
join(X1,lome(X2,X3,upme(a,X1,X3))) = join(meet(X2,X3),X1),
inference(step,[status(thm)],[t94471,t115065]) ).
cnf(t115247,plain,
join(X1,lome(X2,X3,upme(a,X1,X3))) = join(meet(X2,X3),X1),
inference(rw,[status(thm)],[t200129]) ).
cnf(t124901,plain,
join(X1,lome(X2,X3,upme(a,X1,X3))) = join(meet(X2,X3),X1),
inference(orient,[status(thm)],[t115247]) ).
cnf(t125,plain,
lome(X1,X2,meet(X3,X1)) = join(meet(X1,X2),meet(X1,X3)),
inference(cp,[status(thm)],[t47,t118]) ).
cnf(t199446,plain,
lome(X1,X2,meet(X3,X1)) = lome(X1,X2,X3),
inference(step,[status(thm)],[t125,t47]) ).
cnf(t297,plain,
lome(X1,X2,meet(X3,X1)) = lome(X1,X2,X3),
inference(orient,[status(thm)],[t199446]) ).
cnf(t299,plain,
lome(meet(X1,X2),X3,X1) = lome(meet(X1,X2),X3,meet(X1,X2)),
inference(cp,[status(thm)],[t297,t100]) ).
cnf(t199447,plain,
lome(meet(X1,X2),X3,X1) = meet(X1,X2),
inference(step,[status(thm)],[t299,t152]) ).
cnf(t304,plain,
lome(meet(X1,X2),X3,X1) = meet(X1,X2),
inference(orient,[status(thm)],[t199447]) ).
cnf(t310,plain,
meet(X1,X2) = lome(meet(X2,X1),X3,X1),
inference(cp,[status(thm)],[t304,t13]) ).
cnf(t311,plain,
lome(meet(X1,X2),X3,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t310]) ).
cnf(t124996,plain,
join(meet(meet(X1,upme(a,X2,X3)),X3),X2) = join(X2,meet(upme(a,X2,X3),X1)),
inference(cp,[status(thm)],[t124901,t311]) ).
cnf(t200283,plain,
join(meet(X1,meet(upme(a,X2,X3),X3)),X2) = join(X2,meet(upme(a,X2,X3),X1)),
inference(step,[status(thm)],[t124996,t15]) ).
cnf(t200284,plain,
join(meet(X1,upme(meet(a,X3),X2,X3)),X2) = join(X2,meet(upme(a,X2,X3),X1)),
inference(step,[status(thm)],[t200283,t1031]) ).
cnf(t200285,plain,
join(meet(X1,meet(a,X3)),X2) = join(X2,meet(upme(a,X2,X3),X1)),
inference(step,[status(thm)],[t200284,t849]) ).
cnf(t200286,plain,
join(meet(X1,meet(a,X3)),X2) = join(X2,upme(meet(a,X1),X2,X3)),
inference(step,[status(thm)],[t200285,t1031]) ).
cnf(t125394,plain,
join(X1,upme(meet(a,X2),X1,X3)) = join(meet(X2,meet(a,X3)),X1),
inference(orient,[status(thm)],[t200286]) ).
cnf(t809,plain,
upme(meet(X1,X2),X2,X3) = meet(X1,X2),
inference(cp,[status(thm)],[t804,t58]) ).
cnf(t864,plain,
upme(meet(X1,X2),X2,X3) = meet(X1,X2),
inference(orient,[status(thm)],[t809]) ).
cnf(t16635,plain,
upme(X1,X2,X3) = lome(X1,join(X2,X3),meet(Y3,X2)),
inference(cp,[status(thm)],[t16541,t864]) ).
cnf(t17424,plain,
lome(X1,join(X2,X3),meet(Y3,X2)) = upme(X1,X2,X3),
inference(orient,[status(thm)],[t16635]) ).
cnf(t17440,plain,
upme(X1,X2,X3) = lome(X1,meet(Y3,X2),join(X2,X3)),
inference(cp,[status(thm)],[t17424,t465]) ).
cnf(t17803,plain,
lome(X1,meet(X2,X3),join(X3,Y3)) = upme(X1,X3,Y3),
inference(orient,[status(thm)],[t17440]) ).
cnf(t17837,plain,
upme(X1,X2,X3) = lome(X1,meet(X2,Y3),join(X2,X3)),
inference(cp,[status(thm)],[t17803,t13]) ).
cnf(t18172,plain,
lome(X1,meet(X2,X3),join(X2,Y3)) = upme(X1,X2,Y3),
inference(orient,[status(thm)],[t17837]) ).
cnf(t18196,plain,
upme(X1,X2,X3) = lome(X1,lome(X2,Y3,Y4),join(X2,X3)),
inference(cp,[status(thm)],[t18172,t615]) ).
cnf(t28889,plain,
lome(X1,lome(X2,X3,Y3),join(X2,Y4)) = upme(X1,X2,Y4),
inference(orient,[status(thm)],[t18196]) ).
cnf(t63,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t59,t15]) ).
cnf(t202,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t63]) ).
cnf(t205,plain,
X1 = join(X1,upme(meet(X2,X1),X3,Y3)),
inference(cp,[status(thm)],[t202,t130]) ).
cnf(t670,plain,
join(X1,upme(meet(X2,X1),X3,Y3)) = X1,
inference(orient,[status(thm)],[t205]) ).
cnf(t674,plain,
X1 = join(X1,upme(upme(X1,X2,X3),Y3,Y4)),
inference(cp,[status(thm)],[t670,t130]) ).
cnf(t2677,plain,
join(X1,upme(upme(X1,X2,X3),Y3,Y4)) = X1,
inference(orient,[status(thm)],[t674]) ).
cnf(t85,plain,
join(X1,X2) = upme(join(X1,X2),X1,X2),
inference(cp,[status(thm)],[t84,t21]) ).
cnf(t171,plain,
upme(join(X1,X2),X1,X2) = join(X1,X2),
inference(orient,[status(thm)],[t85]) ).
cnf(t177,plain,
join(X1,X2) = upme(join(X2,X1),X1,X2),
inference(cp,[status(thm)],[t171,t36]) ).
cnf(t183,plain,
upme(join(X1,X2),X2,X1) = join(X2,X1),
inference(orient,[status(thm)],[t177]) ).
cnf(t2685,plain,
join(X1,X2) = join(join(X1,X2),upme(join(X2,X1),X3,Y3)),
inference(cp,[status(thm)],[t2677,t183]) ).
cnf(t199895,plain,
join(X1,X2) = join(X1,join(X2,upme(join(X2,X1),X3,Y3))),
inference(step,[status(thm)],[t2685,t41]) ).
cnf(t74987,plain,
join(X1,join(X2,upme(join(X2,X1),X3,Y3))) = join(X1,X2),
inference(orient,[status(thm)],[t199895]) ).
cnf(t114306,plain,
join(X1,meet(a,X2)) = join(X1,join(meet(a,X2),join(meet(X2,X1),upme(a,X2,X1)))),
inference(cp,[status(thm)],[t74987,t113928]) ).
cnf(t507,plain,
join(X1,join(X2,meet(X3,X1))) = join(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t502,t111]) ).
cnf(t199459,plain,
join(X1,join(X2,meet(X3,X1))) = join(X1,X2),
inference(step,[status(thm)],[t507,t502]) ).
cnf(t640,plain,
join(X1,join(X2,meet(X3,X1))) = join(X1,X2),
inference(orient,[status(thm)],[t199459]) ).
cnf(t655,plain,
join(X1,join(join(X2,meet(X3,X1)),Y3)) = join(join(X1,X2),Y3),
inference(cp,[status(thm)],[t41,t640]) ).
cnf(t199854,plain,
join(X1,join(X2,join(meet(X3,X1),Y3))) = join(join(X1,X2),Y3),
inference(step,[status(thm)],[t655,t41]) ).
cnf(t199855,plain,
join(X1,join(X2,join(meet(X3,X1),Y3))) = join(X1,join(X2,Y3)),
inference(step,[status(thm)],[t199854,t41]) ).
cnf(t59542,plain,
join(X1,join(X2,join(meet(X3,X1),Y3))) = join(X1,join(X2,Y3)),
inference(orient,[status(thm)],[t199855]) ).
cnf(t200029,plain,
join(X1,meet(a,X2)) = join(X1,join(meet(a,X2),upme(a,X2,X1))),
inference(step,[status(thm)],[t114306,t59542]) ).
cnf(t200030,plain,
join(X1,meet(a,X2)) = join(X1,lome(a,X2,join(X2,X1))),
inference(step,[status(thm)],[t200029,t13139]) ).
cnf(t200031,plain,
join(X1,meet(a,X2)) = join(X1,upme(a,X2,X1)),
inference(step,[status(thm)],[t200030,t16793]) ).
cnf(t114605,plain,
join(X1,upme(a,X2,X1)) = join(X1,meet(a,X2)),
inference(orient,[status(thm)],[t200031]) ).
cnf(t114711,plain,
upme(X1,X2,upme(a,X3,X2)) = lome(X1,lome(X2,Y3,Y4),join(X2,meet(a,X3))),
inference(cp,[status(thm)],[t28889,t114605]) ).
cnf(t200224,plain,
upme(X1,X2,upme(a,X3,X2)) = upme(X1,X2,meet(a,X3)),
inference(step,[status(thm)],[t114711,t28889]) ).
cnf(t116750,plain,
upme(X1,X2,upme(a,X3,X2)) = upme(X1,X2,meet(a,X3)),
inference(orient,[status(thm)],[t200224]) ).
cnf(t125461,plain,
join(meet(X1,meet(a,upme(a,X2,X3))),X3) = join(X3,upme(meet(a,X1),X3,meet(a,X2))),
inference(cp,[status(thm)],[t125394,t116750]) ).
cnf(t200295,plain,
join(X3,meet(X1,meet(a,upme(a,X2,X3)))) = join(X3,upme(meet(a,X1),X3,meet(a,X2))),
inference(step,[status(thm)],[t125461,t36]) ).
cnf(t200296,plain,
join(X3,meet(X1,upme(meet(a,a),X2,X3))) = join(X3,upme(meet(a,X1),X3,meet(a,X2))),
inference(step,[status(thm)],[t200295,t804]) ).
cnf(t200297,plain,
join(X3,upme(meet(X1,meet(a,a)),X2,X3)) = join(X3,upme(meet(a,X1),X3,meet(a,X2))),
inference(step,[status(thm)],[t200296,t804]) ).
cnf(t200298,plain,
join(X3,upme(meet(X1,a),X2,X3)) = join(X3,upme(meet(a,X1),X3,meet(a,X2))),
inference(step,[status(thm)],[t200297,t84]) ).
cnf(t200299,plain,
join(X3,upme(meet(X1,a),X2,X3)) = join(meet(X1,meet(a,meet(a,X2))),X3),
inference(step,[status(thm)],[t200298,t125394]) ).
cnf(t200300,plain,
join(X3,upme(meet(X1,a),X2,X3)) = join(meet(X1,meet(a,X2)),X3),
inference(step,[status(thm)],[t200299,t100]) ).
cnf(t126620,plain,
join(X1,upme(meet(X2,a),X3,X1)) = join(meet(X2,meet(a,X3)),X1),
inference(orient,[status(thm)],[t200300]) ).
cnf(t147,plain,
lome(join(X1,X2),X3,Y3) = join(upme(X3,X1,X2),meet(join(X1,X2),Y3)),
inference(cp,[status(thm)],[t47,t130]) ).
cnf(t200391,plain,
lome(join(X1,X2),X3,Y3) = join(upme(X3,X1,X2),upme(Y3,X1,X2)),
inference(step,[status(thm)],[t147,t130]) ).
cnf(t149807,plain,
join(upme(X1,X2,X3),upme(Y3,X2,X3)) = lome(join(X2,X3),X1,Y3),
inference(orient,[status(thm)],[t200391]) ).
cnf(t149833,plain,
lome(join(X1,X2),X2,X3) = join(X2,upme(X3,X1,X2)),
inference(cp,[status(thm)],[t149807,t367]) ).
cnf(t150607,plain,
join(X1,upme(X2,X3,X1)) = lome(join(X3,X1),X1,X2),
inference(orient,[status(thm)],[t149833]) ).
cnf(t200396,plain,
lome(join(X3,X1),X1,meet(X2,a)) = join(meet(X2,meet(a,X3)),X1),
inference(step,[status(thm)],[t126620,t150607]) ).
cnf(t151261,plain,
lome(join(X3,X1),X1,meet(X2,a)) = join(meet(X2,meet(a,X3)),X1),
inference(rw,[status(thm)],[t200396]) ).
cnf(t197554,plain,
lome(join(X1,X2),X2,meet(X3,a)) = join(meet(X3,meet(a,X1)),X2),
inference(orient,[status(thm)],[t151261]) ).
cnf(t197863,plain,
meet(join(X1,X2),meet(X3,a)) = meet(meet(X3,a),join(meet(X3,meet(a,X1)),X2)),
inference(cp,[status(thm)],[t7573,t197554]) ).
cnf(t200641,plain,
upme(meet(X3,a),X1,X2) = meet(meet(X3,a),join(meet(X3,meet(a,X1)),X2)),
inference(step,[status(thm)],[t197863,t130]) ).
cnf(t200642,plain,
upme(meet(X3,a),X1,X2) = meet(X3,meet(a,join(meet(X3,meet(a,X1)),X2))),
inference(step,[status(thm)],[t200641,t15]) ).
cnf(t200643,plain,
upme(meet(X3,a),X1,X2) = meet(X3,upme(a,meet(X3,meet(a,X1)),X2)),
inference(step,[status(thm)],[t200642,t21]) ).
cnf(t37797,plain,
lome(a,X1,meet(X2,X3)) = upme(a,meet(X2,meet(a,X3)),X1),
inference(cp,[status(thm)],[t37739,t1419]) ).
cnf(t40300,plain,
upme(a,meet(X1,meet(a,X2)),X3) = lome(a,X3,meet(X1,X2)),
inference(orient,[status(thm)],[t37797]) ).
cnf(t200064,plain,
upme(a,meet(X1,meet(a,X2)),X3) = upme(a,meet(X1,X2),X3),
inference(step,[status(thm)],[t40300,t115065]) ).
cnf(t115084,plain,
upme(a,meet(X1,meet(a,X2)),X3) = upme(a,meet(X1,X2),X3),
inference(orient,[status(thm)],[t200064]) ).
cnf(t200644,plain,
upme(meet(X3,a),X1,X2) = meet(X3,upme(a,meet(X3,X1),X2)),
inference(step,[status(thm)],[t200643,t115084]) ).
cnf(t200645,plain,
upme(meet(X3,a),X1,X2) = upme(meet(X3,a),meet(X3,X1),X2),
inference(step,[status(thm)],[t200644,t804]) ).
cnf(t198699,plain,
upme(meet(X1,a),meet(X1,X2),X3) = upme(meet(X1,a),X2,X3),
inference(orient,[status(thm)],[t200645]) ).
cnf(t38025,plain,
upme(meet(X1,a),X2,meet(a,X3)) = meet(X1,lome(a,X2,X3)),
inference(cp,[status(thm)],[t804,t37976]) ).
cnf(t42132,plain,
upme(meet(X1,a),X2,meet(a,X3)) = meet(X1,lome(a,X2,X3)),
inference(orient,[status(thm)],[t38025]) ).
cnf(t200082,plain,
upme(meet(X1,a),X2,meet(a,X3)) = meet(X1,upme(a,X3,X2)),
inference(step,[status(thm)],[t42132,t115065]) ).
cnf(t200083,plain,
upme(meet(X1,a),X2,meet(a,X3)) = upme(meet(X1,a),X3,X2),
inference(step,[status(thm)],[t200082,t804]) ).
cnf(t115096,plain,
upme(meet(X1,a),X2,meet(a,X3)) = upme(meet(X1,a),X3,X2),
inference(orient,[status(thm)],[t200083]) ).
cnf(t198703,plain,
upme(meet(X1,a),X2,meet(a,X3)) = upme(meet(X1,a),X3,meet(X1,X2)),
inference(cp,[status(thm)],[t198699,t115096]) ).
cnf(t200648,plain,
upme(meet(X1,a),X3,X2) = upme(meet(X1,a),X3,meet(X1,X2)),
inference(step,[status(thm)],[t198703,t115096]) ).
cnf(t198890,plain,
upme(meet(X1,a),X2,meet(X1,X3)) = upme(meet(X1,a),X2,X3),
inference(orient,[status(thm)],[t200648]) ).
cnf(t56,plain,
upme(X1,meet(X2,X3),meet(X2,Y3)) = meet(X1,lome(X2,X3,Y3)),
inference(cp,[status(thm)],[t21,t47]) ).
cnf(t13288,plain,
upme(X1,meet(X2,X3),meet(X2,Y3)) = meet(X1,lome(X2,X3,Y3)),
inference(orient,[status(thm)],[t56]) ).
cnf(t198913,plain,
upme(meet(X1,a),meet(X1,X2),X3) = meet(meet(X1,a),lome(X1,X2,X3)),
inference(cp,[status(thm)],[t198890,t13288]) ).
cnf(t200649,plain,
upme(meet(X1,a),X2,X3) = meet(meet(X1,a),lome(X1,X2,X3)),
inference(step,[status(thm)],[t198913,t198699]) ).
cnf(t200650,plain,
upme(meet(X1,a),X2,X3) = meet(X1,meet(a,lome(X1,X2,X3))),
inference(step,[status(thm)],[t200649,t15]) ).
cnf(t639,plain,
meet(lome(X1,X2,X3),meet(Y3,X1)) = meet(Y3,lome(X1,X2,X3)),
inference(cp,[status(thm)],[t369,t615]) ).
cnf(t378,plain,
meet(meet(X1,X2),meet(X3,X2)) = meet(X3,meet(X2,X1)),
inference(cp,[status(thm)],[t369,t118]) ).
cnf(t199525,plain,
meet(X1,meet(X2,meet(X3,X2))) = meet(X3,meet(X2,X1)),
inference(step,[status(thm)],[t378,t15]) ).
cnf(t199526,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X2,X1)),
inference(step,[status(thm)],[t199525,t118]) ).
cnf(t4657,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X2,X1)),
inference(orient,[status(thm)],[t199526]) ).
cnf(t199589,plain,
meet(X1,meet(Y3,lome(X1,X2,X3))) = meet(Y3,lome(X1,X2,X3)),
inference(step,[status(thm)],[t639,t4657]) ).
cnf(t13878,plain,
meet(X1,meet(X2,lome(X1,X3,Y3))) = meet(X2,lome(X1,X3,Y3)),
inference(orient,[status(thm)],[t199589]) ).
cnf(t200651,plain,
upme(meet(X1,a),X2,X3) = meet(a,lome(X1,X2,X3)),
inference(step,[status(thm)],[t200650,t13878]) ).
cnf(t1442,plain,
lome(meet(X1,X2),X3,Y3) = join(meet(X1,meet(X3,X2)),meet(meet(X1,X2),Y3)),
inference(cp,[status(thm)],[t1099,t1419]) ).
cnf(t199602,plain,
lome(meet(X1,X2),X3,Y3) = join(meet(X1,meet(X3,X2)),meet(X1,meet(X2,Y3))),
inference(step,[status(thm)],[t1442,t15]) ).
cnf(t199603,plain,
lome(meet(X1,X2),X3,Y3) = lome(X1,meet(X3,X2),meet(X2,Y3)),
inference(step,[status(thm)],[t199602,t47]) ).
cnf(t15307,plain,
lome(X1,meet(X2,X3),meet(X3,Y3)) = lome(meet(X1,X3),X2,Y3),
inference(orient,[status(thm)],[t199603]) ).
cnf(t115183,plain,
upme(a,meet(X1,X2),meet(X3,X1)) = lome(meet(a,X1),X3,X2),
inference(cp,[status(thm)],[t115065,t15307]) ).
cnf(t1172,plain,
upme(X1,meet(X2,X3),meet(Y3,X2)) = meet(lome(X2,X3,Y3),X1),
inference(cp,[status(thm)],[t130,t1141]) ).
cnf(t14591,plain,
upme(X1,meet(X2,X3),meet(Y3,X2)) = meet(lome(X2,X3,Y3),X1),
inference(orient,[status(thm)],[t1172]) ).
cnf(t200192,plain,
meet(lome(X1,X2,X3),a) = lome(meet(a,X1),X3,X2),
inference(step,[status(thm)],[t115183,t14591]) ).
cnf(t200193,plain,
meet(a,lome(X1,X2,X3)) = lome(meet(a,X1),X3,X2),
inference(step,[status(thm)],[t200192,t13]) ).
cnf(t115267,plain,
meet(a,lome(X1,X2,X3)) = lome(meet(a,X1),X3,X2),
inference(orient,[status(thm)],[t200193]) ).
cnf(t200652,plain,
upme(meet(X1,a),X2,X3) = lome(meet(a,X1),X3,X2),
inference(step,[status(thm)],[t200651,t115267]) ).
cnf(t199025,plain,
lome(meet(a,X1),X2,X3) = upme(meet(X1,a),X3,X2),
inference(orient,[status(thm)],[t200652]) ).
cnf(goal_0,negated_conjecture,
upme(meet(a,z1),z2,z3) != lome(meet(a,z1),z2,z3),
file('/export/starexec/sandbox2/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,t356]) ).
cnf(g0_1,plain,
upme(meet(z1,a),z3,z2) != lome(meet(a,z1),z2,z3),
inference(rw,[status(thm)],[g0_0,t13]) ).
cnf(g0_2,plain,
upme(meet(z1,a),z3,z2) != upme(meet(z1,a),z3,z2),
inference(rw,[status(thm)],[g0_1,t199025]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT399-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Wed Sep 23 21:34:39 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 68.59/10.92 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.59/10.92 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------