%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT022-1 : TPTP v9.3.1. Released v2.2.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:55:01 PM UTC 2026
% Result : Unsatisfiable 21.33s 3.42s
% Output : CNFRefutation 21.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 188
% Number of leaves : 10
% Syntax : Number of clauses : 461 ( 461 unt; 0 nHn; 4 RR)
% Number of literals : 461 ( 460 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 1367 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t3,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t62,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t5,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t70377,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t5,t62]) ).
cnf(t68,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t70377]) ).
cnf(t6,axiom,
join(meet(X1,join(X2,X3)),meet(X1,X2)) = meet(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t70376,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t6,t11]) ).
cnf(t47,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t70376]) ).
cnf(t7,axiom,
meet(join(X1,meet(X2,X3)),join(X1,X2)) = join(X1,meet(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
meet(join(X1,meet(X2,X3)),join(X1,X2)) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t67,plain,
meet(join(X1,meet(X2,X3)),join(X1,X2)) = join(X1,meet(X2,X3)),
inference(rw,[status(thm)],[t26]) ).
cnf(t70391,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t67,t62]) ).
cnf(t128,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t70391]) ).
cnf(t146,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(meet(join(X1,X2),X1),join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t47,t128]) ).
cnf(t70437,plain,
join(X1,meet(X2,X3)) = join(meet(join(X1,X2),X1),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t146,t128]) ).
cnf(t4,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t70375,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t4,t11]) ).
cnf(t12,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t70375]) ).
cnf(t70438,plain,
join(X1,meet(X2,X3)) = join(meet(X2,X3),join(meet(join(X1,X2),X1),X1)),
inference(step,[status(thm)],[t70437,t12]) ).
cnf(t70439,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(join(X1,X2),X1))),
inference(step,[status(thm)],[t70438,t12]) ).
cnf(t70440,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t70439,t62]) ).
cnf(t383,plain,
join(X1,join(meet(X2,X3),meet(X1,join(X1,X2)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t70440]) ).
cnf(t486,plain,
join(X1,join(meet(X2,X3),meet(X1,join(X1,X2)))) = join(X1,meet(X2,X3)),
inference(rw,[status(thm)],[t383]) ).
cnf(t8,axiom,
meet(join(X1,X2),join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X3,join(X1,X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
join(meet(X1,X2),meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t10,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t34,plain,
meet(join(X1,X1),join(X2,meet(X1,X1))) = join(X1,meet(X2,join(X1,X1))),
inference(cp,[status(thm)],[t33,t10]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t70382,plain,
meet(X1,join(X2,meet(X1,X1))) = join(X1,meet(X2,join(X1,X1))),
inference(step,[status(thm)],[t34,t9]) ).
cnf(t70383,plain,
meet(X1,join(X2,X1)) = join(X1,meet(X2,join(X1,X1))),
inference(step,[status(thm)],[t70382,t10]) ).
cnf(t70384,plain,
meet(X1,join(X1,X2)) = join(X1,meet(X2,join(X1,X1))),
inference(step,[status(thm)],[t70383,t11]) ).
cnf(t70385,plain,
meet(X1,join(X1,X2)) = join(X1,meet(X2,X1)),
inference(step,[status(thm)],[t70384,t9]) ).
cnf(t70386,plain,
meet(X1,join(X1,X2)) = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t70385,t62]) ).
cnf(t106,plain,
join(X1,meet(X1,X2)) = meet(X1,join(X1,X2)),
inference(orient,[status(thm)],[t70386]) ).
cnf(t113,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,meet(X1,join(X1,X2))),
inference(cp,[status(thm)],[t12,t106]) ).
cnf(t70441,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t113,t11]) ).
cnf(t420,plain,
join(X1,join(X2,meet(X1,X3))) = join(X2,meet(X1,join(X1,X3))),
inference(orient,[status(thm)],[t70441]) ).
cnf(t70452,plain,
join(X1,join(X1,join(meet(X2,X3),meet(X1,X2)))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t486,t420]) ).
cnf(t15,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t12,t9]) ).
cnf(t70378,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t15,t12]) ).
cnf(t70379,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t70378,t11]) ).
cnf(t86,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t70379]) ).
cnf(t70453,plain,
join(X1,join(meet(X2,X3),meet(X1,X2))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t70452,t86]) ).
cnf(t70454,plain,
join(X1,join(meet(X1,X2),meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t70453,t11]) ).
cnf(t583,plain,
join(X1,join(meet(X1,X2),meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t70454]) ).
cnf(t71,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t68,t10]) ).
cnf(t70380,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t71,t68]) ).
cnf(t70381,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t70380,t62]) ).
cnf(t96,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t70381]) ).
cnf(t590,plain,
join(X1,meet(meet(X1,X2),X3)) = join(X1,join(meet(X1,X2),meet(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t583,t96]) ).
cnf(t70553,plain,
join(X1,meet(X3,meet(X1,X2))) = join(X1,join(meet(X1,X2),meet(meet(X1,X2),X3))),
inference(step,[status(thm)],[t590,t62]) ).
cnf(t70554,plain,
join(X1,meet(X2,meet(X3,X1))) = join(X1,join(meet(X1,X2),meet(meet(X1,X2),X3))),
inference(step,[status(thm)],[t70553,t68]) ).
cnf(t70555,plain,
join(X1,meet(X1,meet(X2,X3))) = join(X1,join(meet(X1,X2),meet(meet(X1,X2),X3))),
inference(step,[status(thm)],[t70554,t68]) ).
cnf(t70556,plain,
meet(X1,join(X1,meet(X2,X3))) = join(X1,join(meet(X1,X2),meet(meet(X1,X2),X3))),
inference(step,[status(thm)],[t70555,t106]) ).
cnf(t70557,plain,
meet(X1,join(X1,meet(X2,X3))) = join(X1,meet(meet(X1,X2),join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t70556,t106]) ).
cnf(t70558,plain,
meet(X1,join(X1,meet(X2,X3))) = join(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t70557,t11]) ).
cnf(t1588,plain,
join(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))) = meet(X1,join(X1,meet(X2,X3))),
inference(orient,[status(thm)],[t70558]) ).
cnf(t1618,plain,
meet(X1,join(X1,meet(join(X2,X3),meet(X1,X2)))) = join(X1,meet(meet(X1,join(X2,X3)),meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t1588,t47]) ).
cnf(t70583,plain,
meet(X1,join(X1,meet(X2,meet(join(X2,X3),X1)))) = join(X1,meet(meet(X1,join(X2,X3)),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t1618,t68]) ).
cnf(t70584,plain,
meet(X1,join(X1,meet(X1,meet(X2,join(X2,X3))))) = join(X1,meet(meet(X1,join(X2,X3)),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t70583,t68]) ).
cnf(t70585,plain,
meet(X1,meet(X1,join(X1,meet(X2,join(X2,X3))))) = join(X1,meet(meet(X1,join(X2,X3)),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t70584,t106]) ).
cnf(t70586,plain,
meet(X1,join(X1,meet(X2,join(X2,X3)))) = join(X1,meet(meet(X1,join(X2,X3)),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t70585,t96]) ).
cnf(t70587,plain,
meet(X1,join(X1,meet(X2,join(X2,X3)))) = join(X1,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t70586,t10]) ).
cnf(t70588,plain,
meet(X1,join(X1,meet(X2,join(X2,X3)))) = meet(X1,join(X1,join(X2,X3))),
inference(step,[status(thm)],[t70587,t106]) ).
cnf(t2100,plain,
meet(X1,join(X1,meet(X2,join(X2,X3)))) = meet(X1,join(X1,join(X2,X3))),
inference(orient,[status(thm)],[t70588]) ).
cnf(t2161,plain,
meet(X1,meet(join(X1,meet(X2,join(X2,X3))),Y3)) = meet(Y3,meet(X1,join(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t68,t2100]) ).
cnf(t70647,plain,
meet(X1,meet(Y3,join(X1,meet(X2,join(X2,X3))))) = meet(Y3,meet(X1,join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t2161,t62]) ).
cnf(t70648,plain,
meet(X1,meet(Y3,join(X1,meet(X2,join(X2,X3))))) = meet(X1,meet(join(X1,join(X2,X3)),Y3)),
inference(step,[status(thm)],[t70647,t68]) ).
cnf(t70649,plain,
meet(X1,meet(Y3,join(X1,meet(X2,join(X2,X3))))) = meet(X1,meet(Y3,join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t70648,t62]) ).
cnf(t4220,plain,
meet(X1,meet(X2,join(X1,meet(X3,join(X3,Y3))))) = meet(X1,meet(X2,join(X1,join(X3,Y3)))),
inference(orient,[status(thm)],[t70649]) ).
cnf(t139,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(join(meet(X1,X2),X1),meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t128,t47]) ).
cnf(t70429,plain,
meet(X1,join(X2,X3)) = meet(join(meet(X1,X2),X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t139,t47]) ).
cnf(t70430,plain,
meet(X1,join(X2,X3)) = meet(join(X2,X3),meet(join(meet(X1,X2),X1),X1)),
inference(step,[status(thm)],[t70429,t68]) ).
cnf(t70431,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(meet(X1,X2),X1))),
inference(step,[status(thm)],[t70430,t68]) ).
cnf(t70432,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,meet(X1,X2)))),
inference(step,[status(thm)],[t70431,t11]) ).
cnf(t70433,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t70432,t106]) ).
cnf(t70434,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X2),meet(join(X2,X3),X1))),
inference(step,[status(thm)],[t70433,t68]) ).
cnf(t70435,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(X1,meet(join(X1,X2),join(X2,X3)))),
inference(step,[status(thm)],[t70434,t68]) ).
cnf(t70436,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t70435,t96]) ).
cnf(t354,plain,
meet(X1,meet(join(X1,X2),join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t70436]) ).
cnf(t130,plain,
join(X1,meet(join(X1,X2),X3)) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t128,t86]) ).
cnf(t70468,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t130,t62]) ).
cnf(t70469,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t70468,t62]) ).
cnf(t753,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))) = join(X1,meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t70469]) ).
cnf(t50,plain,
meet(join(X1,X2),join(X1,X2)) = join(meet(join(X1,X2),X1),join(X1,X2)),
inference(cp,[status(thm)],[t47,t10]) ).
cnf(t70387,plain,
join(X1,X2) = join(meet(join(X1,X2),X1),join(X1,X2)),
inference(step,[status(thm)],[t50,t10]) ).
cnf(t70388,plain,
join(X1,X2) = join(X2,join(meet(join(X1,X2),X1),X1)),
inference(step,[status(thm)],[t70387,t12]) ).
cnf(t70389,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X2),X1))),
inference(step,[status(thm)],[t70388,t12]) ).
cnf(t70390,plain,
join(X1,X2) = join(X1,join(X2,meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t70389,t62]) ).
cnf(t115,plain,
join(X1,join(X2,meet(X1,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t70390]) ).
cnf(t127,plain,
join(join(X1,meet(X2,join(X2,X1))),join(X3,X2)) = join(X3,join(X2,X1)),
inference(cp,[status(thm)],[t12,t115]) ).
cnf(t70413,plain,
join(X2,join(join(X1,meet(X2,join(X2,X1))),X3)) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t127,t12]) ).
cnf(t70414,plain,
join(X2,join(X3,join(X1,meet(X2,join(X2,X1))))) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t70413,t11]) ).
cnf(t70415,plain,
join(X2,join(X1,join(meet(X2,join(X2,X1)),X3))) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t70414,t12]) ).
cnf(t70416,plain,
join(X1,join(join(meet(X2,join(X2,X1)),X3),X2)) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t70415,t12]) ).
cnf(t70417,plain,
join(X1,join(X2,join(meet(X2,join(X2,X1)),X3))) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t70416,t11]) ).
cnf(t70418,plain,
join(X1,join(X2,join(X3,meet(X2,join(X2,X1))))) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t70417,t11]) ).
cnf(t70419,plain,
join(X1,join(X2,join(X3,meet(X2,join(X1,X2))))) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t70418,t11]) ).
cnf(t70420,plain,
join(X1,join(X2,join(X3,meet(X2,join(X1,X2))))) = join(X1,join(X3,X2)),
inference(step,[status(thm)],[t70419,t12]) ).
cnf(t70421,plain,
join(X1,join(X2,join(X3,meet(X2,join(X1,X2))))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t70420,t11]) ).
cnf(t270,plain,
join(X1,join(X2,join(X3,meet(X2,join(X1,X2))))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t70421]) ).
cnf(t273,plain,
join(X1,join(X2,X2)) = join(X1,join(X2,meet(X2,join(X1,X2)))),
inference(cp,[status(thm)],[t270,t86]) ).
cnf(t70422,plain,
join(X1,X2) = join(X1,join(X2,meet(X2,join(X1,X2)))),
inference(step,[status(thm)],[t273,t9]) ).
cnf(t70423,plain,
join(X1,X2) = join(X1,meet(X2,join(X2,join(X1,X2)))),
inference(step,[status(thm)],[t70422,t106]) ).
cnf(t70424,plain,
join(X1,X2) = join(X1,meet(X2,join(X1,join(X2,X2)))),
inference(step,[status(thm)],[t70423,t12]) ).
cnf(t70425,plain,
join(X1,X2) = join(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t70424,t9]) ).
cnf(t301,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t70425]) ).
cnf(t319,plain,
join(X1,join(meet(X2,join(X1,X2)),X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t12,t301]) ).
cnf(t70426,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X3,join(X1,X2)),
inference(step,[status(thm)],[t319,t11]) ).
cnf(t70427,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X2,join(X3,X1)),
inference(step,[status(thm)],[t70426,t12]) ).
cnf(t70428,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t70427,t12]) ).
cnf(t321,plain,
join(X1,join(X2,meet(X3,join(X1,X3)))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t70428]) ).
cnf(t352,plain,
join(X1,join(join(X2,meet(X3,join(X1,X3))),Y3)) = join(Y3,join(X1,join(X3,X2))),
inference(cp,[status(thm)],[t12,t321]) ).
cnf(t70506,plain,
join(X1,join(Y3,join(X2,meet(X3,join(X1,X3))))) = join(Y3,join(X1,join(X3,X2))),
inference(step,[status(thm)],[t352,t11]) ).
cnf(t70507,plain,
join(X1,join(X2,join(meet(X3,join(X1,X3)),Y3))) = join(Y3,join(X1,join(X3,X2))),
inference(step,[status(thm)],[t70506,t12]) ).
cnf(t70508,plain,
join(X1,join(X2,join(Y3,meet(X3,join(X1,X3))))) = join(Y3,join(X1,join(X3,X2))),
inference(step,[status(thm)],[t70507,t11]) ).
cnf(t70509,plain,
join(X1,join(X2,join(Y3,meet(X3,join(X1,X3))))) = join(X1,join(join(X3,X2),Y3)),
inference(step,[status(thm)],[t70508,t12]) ).
cnf(t70510,plain,
join(X1,join(X2,join(Y3,meet(X3,join(X1,X3))))) = join(X1,join(Y3,join(X3,X2))),
inference(step,[status(thm)],[t70509,t11]) ).
cnf(t70511,plain,
join(X1,join(X2,join(Y3,meet(X3,join(X1,X3))))) = join(X1,join(X2,join(Y3,X3))),
inference(step,[status(thm)],[t70510,t12]) ).
cnf(t70512,plain,
join(X1,join(X2,join(Y3,meet(X3,join(X1,X3))))) = join(X1,join(X2,join(X3,Y3))),
inference(step,[status(thm)],[t70511,t11]) ).
cnf(t1077,plain,
join(X1,join(X2,join(X3,meet(Y3,join(X1,Y3))))) = join(X1,join(X2,join(Y3,X3))),
inference(orient,[status(thm)],[t70512]) ).
cnf(t1673,plain,
join(X1,join(X2,join(meet(X3,Y3),X3))) = join(X1,join(X2,meet(X3,join(X3,meet(Y3,X1))))),
inference(cp,[status(thm)],[t1077,t1588]) ).
cnf(t70613,plain,
join(X1,join(X2,join(X3,meet(X3,Y3)))) = join(X1,join(X2,meet(X3,join(X3,meet(Y3,X1))))),
inference(step,[status(thm)],[t1673,t11]) ).
cnf(t70614,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(X1,join(X2,meet(X3,join(X3,meet(Y3,X1))))),
inference(step,[status(thm)],[t70613,t106]) ).
cnf(t70615,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(X1,join(X2,meet(X3,join(X3,meet(X1,Y3))))),
inference(step,[status(thm)],[t70614,t62]) ).
cnf(t2962,plain,
join(X1,join(X2,meet(X3,join(X3,meet(X1,Y3))))) = join(X1,join(X2,meet(X3,join(X3,Y3)))),
inference(orient,[status(thm)],[t70615]) ).
cnf(t1652,plain,
join(X1,join(meet(X2,X3),X2)) = join(X1,meet(X2,join(X2,meet(X3,X1)))),
inference(cp,[status(thm)],[t321,t1588]) ).
cnf(t70575,plain,
join(X1,join(X2,meet(X2,X3))) = join(X1,meet(X2,join(X2,meet(X3,X1)))),
inference(step,[status(thm)],[t1652,t11]) ).
cnf(t70576,plain,
join(X1,meet(X2,join(X2,X3))) = join(X1,meet(X2,join(X2,meet(X3,X1)))),
inference(step,[status(thm)],[t70575,t106]) ).
cnf(t70577,plain,
join(X1,meet(X2,join(X2,X3))) = join(X1,meet(X2,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t70576,t62]) ).
cnf(t1827,plain,
join(X1,meet(X2,join(X2,meet(X1,X3)))) = join(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t70577]) ).
cnf(t137,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(join(meet(X1,X2),X1),meet(X1,X2)),
inference(cp,[status(thm)],[t128,t9]) ).
cnf(t70392,plain,
meet(X1,X2) = meet(join(meet(X1,X2),X1),meet(X1,X2)),
inference(step,[status(thm)],[t137,t9]) ).
cnf(t70393,plain,
meet(X1,X2) = meet(X2,meet(join(meet(X1,X2),X1),X1)),
inference(step,[status(thm)],[t70392,t68]) ).
cnf(t70394,plain,
meet(X1,X2) = meet(X1,meet(X2,join(meet(X1,X2),X1))),
inference(step,[status(thm)],[t70393,t68]) ).
cnf(t70395,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,meet(X1,X2)))),
inference(step,[status(thm)],[t70394,t11]) ).
cnf(t70396,plain,
meet(X1,X2) = meet(X1,meet(X2,meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t70395,t106]) ).
cnf(t70397,plain,
meet(X1,X2) = meet(X1,meet(X1,meet(join(X1,X2),X2))),
inference(step,[status(thm)],[t70396,t68]) ).
cnf(t70398,plain,
meet(X1,X2) = meet(X1,meet(join(X1,X2),X2)),
inference(step,[status(thm)],[t70397,t96]) ).
cnf(t70399,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t70398,t62]) ).
cnf(t152,plain,
meet(X1,meet(X2,join(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t70399]) ).
cnf(t163,plain,
meet(X1,meet(meet(X2,join(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t68,t152]) ).
cnf(t70401,plain,
meet(X1,meet(X3,meet(X2,join(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t163,t62]) ).
cnf(t70402,plain,
meet(X1,meet(X2,meet(join(X1,X2),X3))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t70401,t68]) ).
cnf(t70403,plain,
meet(X1,meet(X2,meet(X3,join(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t70402,t62]) ).
cnf(t70404,plain,
meet(X1,meet(X2,meet(X3,join(X1,X2)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t70403,t68]) ).
cnf(t70405,plain,
meet(X1,meet(X2,meet(X3,join(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t70404,t68]) ).
cnf(t178,plain,
meet(X1,meet(X2,meet(X3,join(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t70405]) ).
cnf(t183,plain,
meet(X1,meet(meet(X2,X3),join(X1,X2))) = meet(X1,meet(meet(X2,X3),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t178,t128]) ).
cnf(t70406,plain,
meet(X1,meet(meet(X2,X3),join(X1,X2))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t183,t152]) ).
cnf(t199,plain,
meet(X1,meet(meet(X2,X3),join(X1,X2))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t70406]) ).
cnf(t216,plain,
meet(X1,join(X1,meet(meet(X2,X3),join(X1,X2)))) = join(X1,meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t106,t199]) ).
cnf(t70505,plain,
meet(X1,join(X1,meet(meet(X2,X3),join(X1,X2)))) = meet(X1,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t216,t106]) ).
cnf(t1028,plain,
meet(X1,join(X1,meet(meet(X2,X3),join(X1,X2)))) = meet(X1,join(X1,meet(X2,X3))),
inference(orient,[status(thm)],[t70505]) ).
cnf(t1831,plain,
join(meet(X1,X2),meet(X3,join(X3,join(X3,X1)))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t1827,t1028]) ).
cnf(t70616,plain,
join(X3,join(meet(X1,X2),meet(X3,join(X3,X1)))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t1831,t420]) ).
cnf(t70617,plain,
join(X3,join(X3,join(meet(X1,X2),meet(X3,X1)))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t70616,t420]) ).
cnf(t70618,plain,
join(X3,join(meet(X1,X2),meet(X3,X1))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t70617,t86]) ).
cnf(t70619,plain,
join(X3,join(meet(X1,X2),meet(X1,X3))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t70618,t62]) ).
cnf(t70620,plain,
join(X3,join(meet(X1,X2),meet(X1,X3))) = join(X3,join(meet(X1,X2),meet(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t70619,t420]) ).
cnf(t485,plain,
join(X1,join(X2,meet(X1,join(X1,X2)))) = join(X1,X2),
inference(rw,[status(thm)],[t115]) ).
cnf(t70442,plain,
join(X1,join(X1,join(X2,meet(X1,X2)))) = join(X1,X2),
inference(step,[status(thm)],[t485,t420]) ).
cnf(t70443,plain,
join(X1,join(X2,meet(X1,X2))) = join(X1,X2),
inference(step,[status(thm)],[t70442,t86]) ).
cnf(t489,plain,
join(X1,join(X2,meet(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t70443]) ).
cnf(t70621,plain,
join(X3,join(meet(X1,X2),meet(X1,X3))) = join(X3,meet(X1,X2)),
inference(step,[status(thm)],[t70620,t489]) ).
cnf(t3049,plain,
join(X1,join(meet(X2,X3),meet(X2,X1))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t70621]) ).
cnf(t3053,plain,
join(join(X1,X2),meet(X3,X1)) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(cp,[status(thm)],[t3049,t47]) ).
cnf(t70622,plain,
join(meet(X3,X1),join(X1,X2)) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t3053,t11]) ).
cnf(t70623,plain,
join(X2,join(meet(X3,X1),X1)) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t70622,t12]) ).
cnf(t70624,plain,
join(X1,join(X2,meet(X3,X1))) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t70623,t12]) ).
cnf(t70625,plain,
join(X1,join(X2,meet(X1,X3))) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t70624,t62]) ).
cnf(t3138,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t70625]) ).
cnf(t3188,plain,
join(X1,join(X2,meet(X1,X3))) = join(join(X1,X2),meet(join(X1,X2),X3)),
inference(cp,[status(thm)],[t3138,t62]) ).
cnf(t70626,plain,
join(X1,join(X2,meet(X1,X3))) = meet(join(X1,X2),join(join(X1,X2),X3)),
inference(step,[status(thm)],[t3188,t106]) ).
cnf(t70627,plain,
join(X1,join(X2,meet(X1,X3))) = meet(join(X1,X2),join(X3,join(X1,X2))),
inference(step,[status(thm)],[t70626,t11]) ).
cnf(t70628,plain,
join(X1,join(X2,meet(X1,X3))) = meet(join(X1,X2),join(X2,join(X3,X1))),
inference(step,[status(thm)],[t70627,t12]) ).
cnf(t70629,plain,
join(X1,join(X2,meet(X1,X3))) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t70628,t12]) ).
cnf(t3298,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t70629]) ).
cnf(t3360,plain,
join(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(join(X1,X2),join(X1,meet(X2,join(X2,X3)))),
inference(cp,[status(thm)],[t3298,t106]) ).
cnf(t70630,plain,
join(X1,join(X2,meet(X1,meet(X2,X3)))) = join(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t3360,t128]) ).
cnf(t3435,plain,
join(X1,join(X2,meet(X1,meet(X2,X3)))) = join(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t70630]) ).
cnf(t3436,plain,
join(X1,meet(X2,join(X2,X3))) = join(X2,meet(X1,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t3435,t420]) ).
cnf(t70632,plain,
join(X1,meet(X2,join(X2,X3))) = join(X2,meet(X1,join(X1,X3))),
inference(step,[status(thm)],[t3436,t1827]) ).
cnf(t70633,plain,
join(X1,meet(X2,join(X2,X3))) = join(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t70632,t420]) ).
cnf(t3594,plain,
join(X1,meet(X2,join(X2,X3))) = join(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t70633]) ).
cnf(t107,plain,
meet(meet(X1,X2),join(meet(X1,X2),join(X1,X2))) = meet(join(X1,X2),join(meet(X1,X2),meet(X1,X2))),
inference(cp,[status(thm)],[t106,t33]) ).
cnf(t70460,plain,
meet(meet(X1,X2),join(X2,join(meet(X1,X2),X1))) = meet(join(X1,X2),join(meet(X1,X2),meet(X1,X2))),
inference(step,[status(thm)],[t107,t12]) ).
cnf(t70461,plain,
meet(meet(X1,X2),join(X1,join(X2,meet(X1,X2)))) = meet(join(X1,X2),join(meet(X1,X2),meet(X1,X2))),
inference(step,[status(thm)],[t70460,t12]) ).
cnf(t70462,plain,
meet(meet(X1,X2),join(X1,X2)) = meet(join(X1,X2),join(meet(X1,X2),meet(X1,X2))),
inference(step,[status(thm)],[t70461,t489]) ).
cnf(t70463,plain,
meet(meet(X1,X2),join(X1,X2)) = meet(join(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t70462,t9]) ).
cnf(t70464,plain,
meet(meet(X1,X2),join(X1,X2)) = meet(X2,meet(join(X1,X2),X1)),
inference(step,[status(thm)],[t70463,t68]) ).
cnf(t70465,plain,
meet(meet(X1,X2),join(X1,X2)) = meet(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t70464,t68]) ).
cnf(t70466,plain,
meet(meet(X1,X2),join(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t70465,t152]) ).
cnf(t672,plain,
meet(meet(X1,X2),join(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t70466]) ).
cnf(t3748,plain,
join(meet(X1,X2),meet(X3,join(X3,join(X1,X2)))) = join(meet(X1,X2),join(X3,meet(X1,X2))),
inference(cp,[status(thm)],[t3594,t672]) ).
cnf(t194,plain,
meet(X1,join(X1,meet(X2,meet(X3,join(X1,X2))))) = join(X1,meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t106,t178]) ).
cnf(t70470,plain,
meet(X1,join(X1,meet(X2,meet(X3,join(X1,X2))))) = meet(X1,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t194,t106]) ).
cnf(t798,plain,
meet(X1,join(X1,meet(X2,meet(X3,join(X1,X2))))) = meet(X1,join(X1,meet(X2,X3))),
inference(orient,[status(thm)],[t70470]) ).
cnf(t1830,plain,
join(X1,meet(X2,join(X2,meet(X3,join(X2,X1))))) = join(X1,meet(X2,join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t1827,t798]) ).
cnf(t70590,plain,
join(X1,meet(X2,join(X2,meet(X3,join(X1,X2))))) = join(X1,meet(X2,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t1830,t11]) ).
cnf(t70591,plain,
join(X1,meet(X2,join(X2,meet(X3,join(X1,X2))))) = join(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t70590,t1827]) ).
cnf(t2230,plain,
join(X1,meet(X2,join(X2,meet(X3,join(X1,X2))))) = join(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t70591]) ).
cnf(t2287,plain,
meet(X1,join(X1,join(X2,meet(X3,join(X1,X2))))) = meet(X1,join(X1,meet(X2,join(X2,X3)))),
inference(cp,[status(thm)],[t2100,t2230]) ).
cnf(t70601,plain,
meet(X1,join(X1,join(X2,meet(X3,join(X1,X2))))) = meet(X1,join(X1,join(X2,X3))),
inference(step,[status(thm)],[t2287,t2100]) ).
cnf(t2557,plain,
meet(X1,join(X1,join(X2,meet(X3,join(X1,X2))))) = meet(X1,join(X1,join(X2,X3))),
inference(orient,[status(thm)],[t70601]) ).
cnf(t102,plain,
meet(X1,join(meet(X1,X2),X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t47,t96]) ).
cnf(t70458,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t102,t11]) ).
cnf(t70459,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t70458,t11]) ).
cnf(t641,plain,
join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))) = meet(X1,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t70459]) ).
cnf(t2565,plain,
meet(X1,join(X1,join(meet(X2,X3),X2))) = meet(X1,join(X1,meet(X2,join(X1,meet(X2,X3))))),
inference(cp,[status(thm)],[t2557,t641]) ).
cnf(t70655,plain,
meet(X1,join(X1,join(X2,meet(X2,X3)))) = meet(X1,join(X1,meet(X2,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t2565,t11]) ).
cnf(t70656,plain,
meet(X1,join(X1,meet(X2,join(X2,X3)))) = meet(X1,join(X1,meet(X2,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t70655,t106]) ).
cnf(t70657,plain,
meet(X1,join(X1,join(X2,X3))) = meet(X1,join(X1,meet(X2,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t70656,t2100]) ).
cnf(t4545,plain,
meet(X1,join(X1,meet(X2,join(X1,meet(X2,X3))))) = meet(X1,join(X1,join(X2,X3))),
inference(orient,[status(thm)],[t70657]) ).
cnf(t4582,plain,
meet(X1,join(X1,join(meet(X2,X3),join(X2,X3)))) = meet(X1,join(X1,meet(meet(X2,X3),join(X1,meet(X2,X3))))),
inference(cp,[status(thm)],[t4545,t672]) ).
cnf(t70658,plain,
meet(X1,join(X1,join(X3,join(meet(X2,X3),X2)))) = meet(X1,join(X1,meet(meet(X2,X3),join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t4582,t12]) ).
cnf(t70659,plain,
meet(X1,join(X1,join(X2,join(X3,meet(X2,X3))))) = meet(X1,join(X1,meet(meet(X2,X3),join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t70658,t12]) ).
cnf(t70660,plain,
meet(X1,join(X1,join(X2,meet(X3,join(X3,X3))))) = meet(X1,join(X1,meet(meet(X2,X3),join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t70659,t3594]) ).
cnf(t2133,plain,
meet(X1,join(X1,join(X2,meet(X3,join(X3,Y3))))) = meet(X1,join(X1,meet(X2,join(X2,join(X3,Y3))))),
inference(cp,[status(thm)],[t2100,t2100]) ).
cnf(t70646,plain,
meet(X1,join(X1,join(X2,meet(X3,join(X3,Y3))))) = meet(X1,join(X1,join(X2,join(X3,Y3)))),
inference(step,[status(thm)],[t2133,t2100]) ).
cnf(t4128,plain,
meet(X1,join(X1,join(X2,meet(X3,join(X3,Y3))))) = meet(X1,join(X1,join(X2,join(X3,Y3)))),
inference(orient,[status(thm)],[t70646]) ).
cnf(t70661,plain,
meet(X1,join(X1,join(X2,join(X3,X3)))) = meet(X1,join(X1,meet(meet(X2,X3),join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t70660,t4128]) ).
cnf(t70662,plain,
meet(X1,join(X1,join(X2,X3))) = meet(X1,join(X1,meet(meet(X2,X3),join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t70661,t9]) ).
cnf(t160,plain,
meet(X1,join(X1,meet(X2,join(X1,X2)))) = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t106,t152]) ).
cnf(t70400,plain,
meet(X1,join(X1,meet(X2,join(X1,X2)))) = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t160,t106]) ).
cnf(t165,plain,
meet(X1,join(X1,meet(X2,join(X1,X2)))) = meet(X1,join(X1,X2)),
inference(orient,[status(thm)],[t70400]) ).
cnf(t70663,plain,
meet(X1,join(X1,join(X2,X3))) = meet(X1,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t70662,t165]) ).
cnf(t4634,plain,
meet(X1,join(X1,join(X2,X3))) = meet(X1,join(X1,meet(X2,X3))),
inference(orient,[status(thm)],[t70663]) ).
cnf(t70700,plain,
join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))) = join(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t3748,t4634]) ).
cnf(t70701,plain,
join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))) = join(X3,join(meet(X1,X2),meet(X1,X2))),
inference(step,[status(thm)],[t70700,t12]) ).
cnf(t70702,plain,
join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))) = join(X3,meet(X1,X2)),
inference(step,[status(thm)],[t70701,t9]) ).
cnf(t5210,plain,
join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))) = join(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t70702]) ).
cnf(t5296,plain,
join(X1,join(meet(X1,X2),meet(X3,join(X3,X2)))) = join(X1,join(X3,meet(X1,X2))),
inference(cp,[status(thm)],[t2962,t5210]) ).
cnf(t70707,plain,
join(X1,join(meet(X1,X2),meet(X3,join(X2,X3)))) = join(X1,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t5296,t11]) ).
cnf(t70708,plain,
join(X1,join(meet(X1,X2),meet(X3,join(X2,X3)))) = join(X1,meet(X3,join(X3,X2))),
inference(step,[status(thm)],[t70707,t3594]) ).
cnf(t70709,plain,
join(X1,join(meet(X1,X2),meet(X3,join(X2,X3)))) = join(X1,meet(X3,join(X2,X3))),
inference(step,[status(thm)],[t70708,t11]) ).
cnf(t5545,plain,
join(X1,join(meet(X1,X2),meet(X3,join(X2,X3)))) = join(X1,meet(X3,join(X2,X3))),
inference(orient,[status(thm)],[t70709]) ).
cnf(t3136,plain,
join(join(meet(X1,X2),meet(X1,X3)),join(Y3,X3)) = join(Y3,join(X3,meet(X1,X2))),
inference(cp,[status(thm)],[t12,t3049]) ).
cnf(t70642,plain,
join(X3,join(join(meet(X1,X2),meet(X1,X3)),Y3)) = join(Y3,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t3136,t12]) ).
cnf(t70643,plain,
join(X3,join(Y3,join(meet(X1,X2),meet(X1,X3)))) = join(Y3,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t70642,t11]) ).
cnf(t70644,plain,
join(X3,join(Y3,join(meet(X1,X2),meet(X1,X3)))) = join(X3,join(meet(X1,X2),Y3)),
inference(step,[status(thm)],[t70643,t12]) ).
cnf(t70645,plain,
join(X3,join(Y3,join(meet(X1,X2),meet(X1,X3)))) = join(X3,join(Y3,meet(X1,X2))),
inference(step,[status(thm)],[t70644,t11]) ).
cnf(t4030,plain,
join(X1,join(X2,join(meet(X3,Y3),meet(X3,X1)))) = join(X1,join(X2,meet(X3,Y3))),
inference(orient,[status(thm)],[t70645]) ).
cnf(t4042,plain,
join(join(X1,X2),join(X3,meet(Y3,X1))) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(cp,[status(thm)],[t4030,t47]) ).
cnf(t70715,plain,
join(meet(Y3,X1),join(join(X1,X2),X3)) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t4042,t12]) ).
cnf(t70716,plain,
join(X3,join(meet(Y3,X1),join(X1,X2))) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t70715,t12]) ).
cnf(t70717,plain,
join(X3,join(X2,join(meet(Y3,X1),X1))) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t70716,t12]) ).
cnf(t70718,plain,
join(X3,join(X1,join(X2,meet(Y3,X1)))) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t70717,t12]) ).
cnf(t70719,plain,
join(X1,join(join(X2,meet(Y3,X1)),X3)) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t70718,t12]) ).
cnf(t70720,plain,
join(X1,join(X3,join(X2,meet(Y3,X1)))) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t70719,t11]) ).
cnf(t70721,plain,
join(X1,join(X2,join(meet(Y3,X1),X3))) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t70720,t12]) ).
cnf(t70722,plain,
join(X1,join(X2,join(X3,meet(Y3,X1)))) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t70721,t11]) ).
cnf(t70723,plain,
join(X1,join(X2,join(X3,meet(X1,Y3)))) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t70722,t62]) ).
cnf(t3294,plain,
join(join(X1,X2),join(meet(X3,join(X1,X2)),Y3)) = join(Y3,join(X1,join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t12,t3138]) ).
cnf(t70690,plain,
join(Y3,join(join(X1,X2),meet(X3,join(X1,X2)))) = join(Y3,join(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t3294,t12]) ).
cnf(t70634,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t3138,t3594]) ).
cnf(t3595,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t70634]) ).
cnf(t70691,plain,
join(Y3,join(X1,meet(X2,join(X2,X3)))) = join(Y3,join(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t70690,t3595]) ).
cnf(t70692,plain,
join(X1,join(meet(X2,join(X2,X3)),Y3)) = join(Y3,join(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t70691,t12]) ).
cnf(t70693,plain,
join(X1,join(Y3,meet(X2,join(X2,X3)))) = join(Y3,join(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t70692,t11]) ).
cnf(t3806,plain,
join(X1,join(X2,meet(X1,X3))) = join(X2,meet(X1,join(X1,X3))),
inference(rw,[status(thm)],[t420]) ).
cnf(t70641,plain,
join(X1,meet(X2,join(X2,X3))) = join(X2,meet(X1,join(X1,X3))),
inference(step,[status(thm)],[t3806,t3594]) ).
cnf(t3911,plain,
join(X1,meet(X2,join(X2,X3))) = join(X2,meet(X1,join(X1,X3))),
inference(orient,[status(thm)],[t70641]) ).
cnf(t70694,plain,
join(X1,join(X2,meet(Y3,join(Y3,X3)))) = join(Y3,join(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t70693,t3911]) ).
cnf(t70695,plain,
join(X1,join(X2,meet(Y3,join(X3,Y3)))) = join(Y3,join(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t70694,t11]) ).
cnf(t70696,plain,
join(X1,join(X2,meet(Y3,join(X3,Y3)))) = join(X1,join(join(X2,meet(X1,X3)),Y3)),
inference(step,[status(thm)],[t70695,t12]) ).
cnf(t70697,plain,
join(X1,join(X2,meet(Y3,join(X3,Y3)))) = join(X1,join(Y3,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t70696,t11]) ).
cnf(t70698,plain,
join(X1,join(X2,meet(Y3,join(X3,Y3)))) = join(X1,join(X2,join(meet(X1,X3),Y3))),
inference(step,[status(thm)],[t70697,t12]) ).
cnf(t70699,plain,
join(X1,join(X2,meet(Y3,join(X3,Y3)))) = join(X1,join(X2,join(Y3,meet(X1,X3)))),
inference(step,[status(thm)],[t70698,t11]) ).
cnf(t4978,plain,
join(X1,join(X2,meet(X3,join(Y3,X3)))) = join(X1,join(X2,join(X3,meet(X1,Y3)))),
inference(orient,[status(thm)],[t70699]) ).
cnf(t70724,plain,
join(X1,join(X2,meet(X3,join(Y3,X3)))) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t70723,t4978]) ).
cnf(t70725,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(join(X1,X2),join(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t70724,t11]) ).
cnf(t70726,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(X3,join(meet(Y3,join(X1,X2)),join(X1,X2))),
inference(step,[status(thm)],[t70725,t12]) ).
cnf(t70727,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(X3,join(X2,join(meet(Y3,join(X1,X2)),X1))),
inference(step,[status(thm)],[t70726,t12]) ).
cnf(t70728,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(X3,join(X1,join(X2,meet(Y3,join(X1,X2))))),
inference(step,[status(thm)],[t70727,t12]) ).
cnf(t70729,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(X1,join(join(X2,meet(Y3,join(X1,X2))),X3)),
inference(step,[status(thm)],[t70728,t12]) ).
cnf(t70730,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(X1,join(X3,join(X2,meet(Y3,join(X1,X2))))),
inference(step,[status(thm)],[t70729,t11]) ).
cnf(t70731,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(X1,join(X2,join(meet(Y3,join(X1,X2)),X3))),
inference(step,[status(thm)],[t70730,t12]) ).
cnf(t70732,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(X1,join(X2,join(X3,meet(Y3,join(X1,X2))))),
inference(step,[status(thm)],[t70731,t11]) ).
cnf(t5970,plain,
join(X1,join(X2,meet(X3,join(X3,Y3)))) = join(X1,join(X2,join(X3,meet(Y3,join(X1,X2))))),
inference(orient,[status(thm)],[t70732]) ).
cnf(t6110,plain,
join(X1,join(X2,meet(X2,join(X2,X3)))) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t5970,t86]) ).
cnf(t70739,plain,
join(X1,meet(X2,join(X2,join(X2,X3)))) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t6110,t106]) ).
cnf(t70740,plain,
join(X1,meet(X2,join(X2,meet(X2,X3)))) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t70739,t4634]) ).
cnf(t70741,plain,
join(X1,meet(X2,meet(X2,join(X2,X3)))) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t70740,t106]) ).
cnf(t70742,plain,
join(X1,meet(X2,join(X2,X3))) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t70741,t96]) ).
cnf(t6326,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t70742]) ).
cnf(t6336,plain,
join(X1,meet(meet(X2,X3),join(meet(X2,X3),X2))) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t6326,t641]) ).
cnf(t70744,plain,
join(meet(X2,X3),meet(X1,join(X1,X2))) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t6336,t3911]) ).
cnf(t6129,plain,
join(X1,join(meet(X2,X3),meet(meet(X2,X3),join(meet(X2,X3),X2)))) = join(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X2,X3))))),
inference(cp,[status(thm)],[t5970,t641]) ).
cnf(t70733,plain,
join(X1,meet(meet(X2,X3),join(meet(X2,X3),join(meet(X2,X3),X2)))) = join(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t6129,t106]) ).
cnf(t70734,plain,
join(X1,meet(meet(X2,X3),join(meet(X2,X3),meet(meet(X2,X3),X2)))) = join(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t70733,t4634]) ).
cnf(t70735,plain,
join(X1,meet(meet(X2,X3),meet(meet(X2,X3),join(meet(X2,X3),X2)))) = join(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t70734,t106]) ).
cnf(t70736,plain,
join(X1,meet(meet(X2,X3),meet(X2,X3))) = join(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t70735,t199]) ).
cnf(t70737,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t70736,t10]) ).
cnf(t70738,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t70737,t641]) ).
cnf(t6248,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t70738]) ).
cnf(t70745,plain,
join(meet(X2,X3),meet(X1,join(X1,X2))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t70744,t6248]) ).
cnf(t6558,plain,
join(meet(X1,X2),meet(X3,join(X3,X1))) = join(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t70745]) ).
cnf(t6595,plain,
join(X1,meet(join(X1,X2),X3)) = join(meet(join(X1,X2),X3),meet(X1,join(X1,X2))),
inference(cp,[status(thm)],[t6558,t86]) ).
cnf(t70768,plain,
join(X1,meet(X3,join(X1,X2))) = join(meet(join(X1,X2),X3),meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t6595,t62]) ).
cnf(t70769,plain,
join(X1,meet(X3,join(X1,X2))) = join(meet(X1,join(X1,X2)),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t70768,t11]) ).
cnf(t70770,plain,
join(X1,meet(X3,join(X1,X2))) = join(meet(X1,join(X1,X2)),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t70769,t62]) ).
cnf(t7599,plain,
join(meet(X1,join(X1,X2)),meet(X3,join(X1,X2))) = join(X1,meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t70770]) ).
cnf(t7622,plain,
join(X1,meet(X2,join(X1,join(X1,X3)))) = join(meet(X1,join(X1,X3)),meet(X2,join(X1,join(X1,X3)))),
inference(cp,[status(thm)],[t7599,t86]) ).
cnf(t70785,plain,
join(X1,meet(X2,join(X1,X3))) = join(meet(X1,join(X1,X3)),meet(X2,join(X1,join(X1,X3)))),
inference(step,[status(thm)],[t7622,t86]) ).
cnf(t70786,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,join(X1,X3)),join(X2,meet(X1,join(X1,X3)))),
inference(step,[status(thm)],[t70785,t33]) ).
cnf(t70787,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X3),join(X2,meet(X1,join(X1,X3)))),
inference(step,[status(thm)],[t70786,t86]) ).
cnf(t70788,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X3),join(X1,meet(X2,join(X2,X3)))),
inference(step,[status(thm)],[t70787,t3911]) ).
cnf(t8835,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X3,X2)))) = join(X1,meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t70788]) ).
cnf(t8905,plain,
join(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X1,X2)))) = meet(join(meet(X1,X2),meet(X1,X2)),join(X3,meet(X1,X2))),
inference(cp,[status(thm)],[t8835,t5210]) ).
cnf(t70789,plain,
join(meet(X1,X2),meet(X3,meet(X1,X2))) = meet(join(meet(X1,X2),meet(X1,X2)),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t8905,t9]) ).
cnf(t70790,plain,
join(meet(X1,X2),meet(X3,meet(X1,X2))) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t70789,t9]) ).
cnf(t70791,plain,
join(meet(X1,X2),meet(X2,meet(X3,X1))) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t70790,t68]) ).
cnf(t70792,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t70791,t68]) ).
cnf(t9044,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t70792]) ).
cnf(t9089,plain,
meet(meet(X1,X2),join(X2,meet(X1,X2))) = join(meet(X1,X2),meet(X1,X2)),
inference(cp,[status(thm)],[t9044,t10]) ).
cnf(t70794,plain,
meet(meet(X1,X2),join(X2,meet(X1,X2))) = meet(X1,X2),
inference(step,[status(thm)],[t9089,t9]) ).
cnf(t9204,plain,
meet(meet(X1,X2),join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t70794]) ).
cnf(t9277,plain,
join(X1,meet(meet(X2,X3),join(X3,meet(X2,X3)))) = join(X1,join(meet(X1,X3),meet(X2,X3))),
inference(cp,[status(thm)],[t5545,t9204]) ).
cnf(t70795,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X1,X3),meet(X2,X3))),
inference(step,[status(thm)],[t9277,t9204]) ).
cnf(t9309,plain,
join(X1,join(meet(X1,X2),meet(X3,X2))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t70795]) ).
cnf(t9314,plain,
join(X1,meet(X2,X3)) = join(meet(X2,X3),join(X1,meet(X1,X3))),
inference(cp,[status(thm)],[t9309,t12]) ).
cnf(t70796,plain,
join(X1,meet(X2,X3)) = join(meet(X2,X3),meet(X1,join(X1,X3))),
inference(step,[status(thm)],[t9314,t106]) ).
cnf(t9446,plain,
join(meet(X1,X2),meet(X3,join(X3,X2))) = join(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t70796]) ).
cnf(t9601,plain,
join(meet(X1,X2),meet(meet(X1,X2),join(meet(X1,X2),X2))) = meet(join(meet(X1,X2),X2),join(meet(X1,X2),meet(X1,X2))),
inference(cp,[status(thm)],[t753,t9446]) ).
cnf(t70798,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(join(meet(X1,X2),X2),join(meet(X1,X2),meet(X1,X2))),
inference(step,[status(thm)],[t9601,t9446]) ).
cnf(t70799,plain,
meet(X1,X2) = meet(join(meet(X1,X2),X2),join(meet(X1,X2),meet(X1,X2))),
inference(step,[status(thm)],[t70798,t9]) ).
cnf(t70800,plain,
meet(X1,X2) = meet(join(X2,meet(X1,X2)),join(meet(X1,X2),meet(X1,X2))),
inference(step,[status(thm)],[t70799,t11]) ).
cnf(t70801,plain,
meet(X1,X2) = meet(join(X2,meet(X1,X2)),meet(X1,X2)),
inference(step,[status(thm)],[t70800,t9]) ).
cnf(t70802,plain,
meet(X1,X2) = meet(X2,meet(join(X2,meet(X1,X2)),X1)),
inference(step,[status(thm)],[t70801,t68]) ).
cnf(t70803,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X2,meet(X1,X2)))),
inference(step,[status(thm)],[t70802,t68]) ).
cnf(t9644,plain,
meet(X1,meet(X2,join(X2,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t70803]) ).
cnf(t9648,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X2,meet(X3,join(X3,X1))))),
inference(cp,[status(thm)],[t9644,t3595]) ).
cnf(t70804,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X3,X1)))),
inference(step,[status(thm)],[t9648,t128]) ).
cnf(t70805,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X1,X3)))),
inference(step,[status(thm)],[t70804,t11]) ).
cnf(t9715,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t70805]) ).
cnf(t9816,plain,
meet(X1,join(X2,meet(X3,join(join(X1,X2),X3)))) = meet(X1,meet(join(X1,X2),join(X2,X3))),
inference(cp,[status(thm)],[t354,t9715]) ).
cnf(t70815,plain,
meet(X1,join(X2,meet(X3,join(X3,join(X1,X2))))) = meet(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t9816,t11]) ).
cnf(t70816,plain,
meet(X1,join(X2,meet(X3,join(X2,join(X3,X1))))) = meet(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t70815,t12]) ).
cnf(t70817,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X3))))) = meet(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t70816,t12]) ).
cnf(t70818,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X3))))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t70817,t354]) ).
cnf(t10292,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X3))))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t70818]) ).
cnf(t10315,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X3,join(X1,X2))))),
inference(cp,[status(thm)],[t10292,t12]) ).
cnf(t70821,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t10315,t4634]) ).
cnf(t10640,plain,
meet(X1,join(X2,meet(X3,join(X3,meet(X1,X2))))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t70821]) ).
cnf(t10775,plain,
meet(X1,meet(X2,join(X1,join(X3,meet(X2,X1))))) = meet(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t4220,t10640]) ).
cnf(t70846,plain,
meet(X1,meet(X2,join(X1,join(X3,meet(X1,X2))))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t10775,t62]) ).
cnf(t70847,plain,
meet(X1,meet(X2,join(X1,meet(X3,join(X3,X2))))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t70846,t3594]) ).
cnf(t70848,plain,
meet(X1,meet(X2,join(X1,join(X3,X2)))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t70847,t4220]) ).
cnf(t70849,plain,
meet(X1,meet(X2,join(X1,join(X2,X3)))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t70848,t11]) ).
cnf(t9719,plain,
meet(X1,join(X2,meet(X2,X3))) = meet(X1,meet(X2,join(X2,meet(X3,X1)))),
inference(cp,[status(thm)],[t9715,t1588]) ).
cnf(t70806,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(X2,meet(X3,X1)))),
inference(step,[status(thm)],[t9719,t106]) ).
cnf(t70807,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t70806,t62]) ).
cnf(t9861,plain,
meet(X1,meet(X2,join(X2,meet(X1,X3)))) = meet(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t70807]) ).
cnf(t9885,plain,
meet(X1,meet(X2,join(X2,join(X1,X3)))) = meet(X1,meet(X2,join(X1,meet(X2,join(X2,X3))))),
inference(cp,[status(thm)],[t9861,t3911]) ).
cnf(t70808,plain,
meet(X1,meet(X2,join(X2,meet(X1,X3)))) = meet(X1,meet(X2,join(X1,meet(X2,join(X2,X3))))),
inference(step,[status(thm)],[t9885,t4634]) ).
cnf(t70809,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(X1,meet(X2,join(X2,X3))))),
inference(step,[status(thm)],[t70808,t9861]) ).
cnf(t70810,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t70809,t4220]) ).
cnf(t9956,plain,
meet(X1,meet(X2,join(X1,join(X2,X3)))) = meet(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t70810]) ).
cnf(t70850,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t70849,t9956]) ).
cnf(t11673,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t70850]) ).
cnf(t11713,plain,
meet(X1,meet(X2,join(X1,meet(X2,X3)))) = meet(X1,meet(X2,meet(X2,join(X2,X3)))),
inference(cp,[status(thm)],[t11673,t106]) ).
cnf(t70857,plain,
meet(X1,meet(X2,join(X1,meet(X2,X3)))) = meet(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t11713,t96]) ).
cnf(t70858,plain,
meet(X1,meet(X2,join(X1,meet(X2,X3)))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t70857,t11673]) ).
cnf(t11972,plain,
meet(X1,meet(X2,join(X1,meet(X2,X3)))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t70858]) ).
cnf(t12011,plain,
meet(X1,meet(X2,join(X1,join(X2,join(X3,Y3))))) = meet(X1,meet(X2,join(X1,meet(X2,join(X2,meet(X3,Y3)))))),
inference(cp,[status(thm)],[t11972,t4634]) ).
cnf(t70851,plain,
meet(X1,meet(X2,join(X1,join(X2,X3)))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t9956,t11673]) ).
cnf(t11674,plain,
meet(X1,meet(X2,join(X1,join(X2,X3)))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t70851]) ).
cnf(t70859,plain,
meet(X1,meet(X2,join(X1,join(X3,Y3)))) = meet(X1,meet(X2,join(X1,meet(X2,join(X2,meet(X3,Y3)))))),
inference(step,[status(thm)],[t12011,t11674]) ).
cnf(t70860,plain,
meet(X1,meet(X2,join(X1,join(X3,Y3)))) = meet(X1,meet(X2,join(X1,join(X2,meet(X3,Y3))))),
inference(step,[status(thm)],[t70859,t4220]) ).
cnf(t70861,plain,
meet(X1,meet(X2,join(X1,join(X3,Y3)))) = meet(X1,meet(X2,join(X1,meet(X3,Y3)))),
inference(step,[status(thm)],[t70860,t11674]) ).
cnf(t12089,plain,
meet(X1,meet(X2,join(X1,join(X3,Y3)))) = meet(X1,meet(X2,join(X1,meet(X3,Y3)))),
inference(orient,[status(thm)],[t70861]) ).
cnf(t12092,plain,
meet(X1,meet(join(X2,X3),join(X1,meet(X2,X3)))) = meet(X1,join(X2,X3)),
inference(cp,[status(thm)],[t12089,t152]) ).
cnf(t12550,plain,
meet(X1,meet(join(X2,X3),join(X1,meet(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t12092]) ).
cnf(t6369,plain,
join(X1,meet(join(X1,X2),join(join(X1,X2),X3))) = join(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t6326,t86]) ).
cnf(t70749,plain,
join(join(X1,X2),meet(X1,join(X1,X3))) = join(X1,join(join(X1,X2),meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t6369,t3911]) ).
cnf(t70750,plain,
join(join(X1,X2),meet(X1,join(X1,X3))) = join(X1,join(X1,meet(X2,join(X2,X3)))),
inference(step,[status(thm)],[t70749,t3595]) ).
cnf(t70751,plain,
join(join(X1,X2),meet(X1,join(X1,X3))) = join(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t70750,t86]) ).
cnf(t6801,plain,
join(join(X1,X2),meet(X1,join(X1,X3))) = join(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t70751]) ).
cnf(t12643,plain,
meet(join(X1,X2),join(X1,join(X1,X3))) = meet(join(X1,X2),meet(join(X1,join(X1,X3)),join(X1,meet(X2,join(X2,X3))))),
inference(cp,[status(thm)],[t12550,t6801]) ).
cnf(t70873,plain,
meet(join(X1,X2),join(X1,X3)) = meet(join(X1,X2),meet(join(X1,join(X1,X3)),join(X1,meet(X2,join(X2,X3))))),
inference(step,[status(thm)],[t12643,t86]) ).
cnf(t70874,plain,
meet(join(X1,X2),join(X1,X3)) = meet(join(X1,X2),meet(join(X1,X3),join(X1,meet(X2,join(X2,X3))))),
inference(step,[status(thm)],[t70873,t86]) ).
cnf(t70875,plain,
meet(join(X1,X2),join(X1,X3)) = meet(join(X1,X2),join(X1,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t70874,t8835]) ).
cnf(t70876,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t70875,t128]) ).
cnf(t12733,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t70876]) ).
cnf(t12766,plain,
meet(join(meet(X1,X2),X3),join(meet(X1,X2),meet(Y3,join(Y3,X2)))) = join(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(cp,[status(thm)],[t12733,t9446]) ).
cnf(t71352,plain,
meet(join(X3,meet(X1,X2)),join(meet(X1,X2),meet(Y3,join(Y3,X2)))) = join(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t12766,t11]) ).
cnf(t71353,plain,
meet(join(X3,meet(X1,X2)),join(Y3,meet(X1,X2))) = join(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t71352,t9446]) ).
cnf(t52508,plain,
join(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))) = meet(join(X3,meet(X1,X2)),join(Y3,meet(X1,X2))),
inference(orient,[status(thm)],[t71353]) ).
cnf(t52621,plain,
meet(join(X1,meet(X2,X3)),join(X2,meet(X2,X3))) = join(meet(X2,X3),meet(X1,meet(X2,join(X2,X3)))),
inference(cp,[status(thm)],[t52508,t106]) ).
cnf(t71498,plain,
meet(join(X1,meet(X2,X3)),meet(X2,join(X2,X3))) = join(meet(X2,X3),meet(X1,meet(X2,join(X2,X3)))),
inference(step,[status(thm)],[t52621,t106]) ).
cnf(t71499,plain,
meet(join(X2,X3),meet(join(X1,meet(X2,X3)),X2)) = join(meet(X2,X3),meet(X1,meet(X2,join(X2,X3)))),
inference(step,[status(thm)],[t71498,t68]) ).
cnf(t71500,plain,
meet(X2,meet(join(X2,X3),join(X1,meet(X2,X3)))) = join(meet(X2,X3),meet(X1,meet(X2,join(X2,X3)))),
inference(step,[status(thm)],[t71499,t68]) ).
cnf(t71355,plain,
meet(join(X1,meet(X1,X2)),join(X3,meet(X1,X2))) = meet(X1,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t641,t52508]) ).
cnf(t71356,plain,
meet(meet(X1,join(X1,X2)),join(X3,meet(X1,X2))) = meet(X1,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t71355,t106]) ).
cnf(t52982,plain,
meet(meet(X1,join(X1,X2)),join(X3,meet(X1,X2))) = meet(X1,join(X3,meet(X1,X2))),
inference(rw,[status(thm)],[t71356]) ).
cnf(t53443,plain,
meet(meet(X1,join(X1,X2)),join(X3,meet(X1,X2))) = meet(X1,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t52982]) ).
cnf(t53450,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(join(X2,meet(X1,X3)),meet(X1,join(X1,X3))),
inference(cp,[status(thm)],[t53443,t62]) ).
cnf(t71373,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(join(X1,X3),meet(join(X2,meet(X1,X3)),X1)),
inference(step,[status(thm)],[t53450,t68]) ).
cnf(t71374,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X1,X3),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t71373,t68]) ).
cnf(t54801,plain,
meet(X1,meet(join(X1,X2),join(X3,meet(X1,X2)))) = meet(X1,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t71374]) ).
cnf(t71501,plain,
meet(X2,join(X1,meet(X2,X3))) = join(meet(X2,X3),meet(X1,meet(X2,join(X2,X3)))),
inference(step,[status(thm)],[t71500,t54801]) ).
cnf(t71502,plain,
meet(X2,join(X1,meet(X2,X3))) = join(meet(X2,X3),meet(X1,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t71501,t11673]) ).
cnf(t12634,plain,
meet(meet(X1,X2),join(X3,join(X3,X1))) = meet(meet(X1,X2),meet(join(X3,join(X3,X1)),join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t12550,t6558]) ).
cnf(t70888,plain,
meet(meet(X1,X2),join(X3,X1)) = meet(meet(X1,X2),meet(join(X3,join(X3,X1)),join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t12634,t86]) ).
cnf(t70889,plain,
meet(meet(X1,X2),join(X3,X1)) = meet(meet(X1,X2),meet(join(X3,X1),join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t70888,t86]) ).
cnf(t70890,plain,
meet(meet(X1,X2),join(X3,X1)) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t70889,t128]) ).
cnf(t70891,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t70890,t11]) ).
cnf(t12901,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(meet(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t70891]) ).
cnf(t70892,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t9044,t12901]) ).
cnf(t12902,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(meet(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t70892]) ).
cnf(t52,plain,
meet(X1,join(meet(X2,X3),meet(Y3,join(X2,X3)))) = join(meet(X1,meet(X2,X3)),meet(X1,meet(join(X2,X3),join(Y3,meet(X2,X3))))),
inference(cp,[status(thm)],[t47,t33]) ).
cnf(t70771,plain,
meet(X1,meet(join(X2,X3),join(Y3,meet(X2,X3)))) = join(meet(X1,meet(X2,X3)),meet(X1,meet(join(X2,X3),join(Y3,meet(X2,X3))))),
inference(step,[status(thm)],[t52,t33]) ).
cnf(t7796,plain,
join(meet(X1,meet(X2,X3)),meet(X1,meet(join(X2,X3),join(Y3,meet(X2,X3))))) = meet(X1,meet(join(X2,X3),join(Y3,meet(X2,X3)))),
inference(orient,[status(thm)],[t70771]) ).
cnf(t7814,plain,
meet(X1,meet(join(X2,X2),join(X3,meet(X2,X2)))) = join(meet(X1,X2),meet(X1,meet(join(X2,X2),join(X3,meet(X2,X2))))),
inference(cp,[status(thm)],[t7796,t10]) ).
cnf(t70822,plain,
meet(X1,meet(X2,join(X3,meet(X2,X2)))) = join(meet(X1,X2),meet(X1,meet(join(X2,X2),join(X3,meet(X2,X2))))),
inference(step,[status(thm)],[t7814,t9]) ).
cnf(t70823,plain,
meet(X1,meet(X2,join(X3,X2))) = join(meet(X1,X2),meet(X1,meet(join(X2,X2),join(X3,meet(X2,X2))))),
inference(step,[status(thm)],[t70822,t10]) ).
cnf(t70824,plain,
meet(X1,meet(X2,join(X2,X3))) = join(meet(X1,X2),meet(X1,meet(join(X2,X2),join(X3,meet(X2,X2))))),
inference(step,[status(thm)],[t70823,t11]) ).
cnf(t70825,plain,
meet(X1,meet(X2,join(X2,X3))) = join(meet(X1,X2),meet(X1,meet(X2,join(X3,meet(X2,X2))))),
inference(step,[status(thm)],[t70824,t9]) ).
cnf(t70826,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(join(X3,meet(X2,X2)),meet(X1,X2))),
inference(step,[status(thm)],[t70825,t9044]) ).
cnf(t70827,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(meet(X1,X2),join(X3,meet(X2,X2)))),
inference(step,[status(thm)],[t70826,t11]) ).
cnf(t70828,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(X3,join(meet(X2,X2),meet(X1,X2)))),
inference(step,[status(thm)],[t70827,t12]) ).
cnf(t70829,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),meet(X2,X2)))),
inference(step,[status(thm)],[t70828,t11]) ).
cnf(t70830,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),X2))),
inference(step,[status(thm)],[t70829,t10]) ).
cnf(t70831,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(X3,join(X2,meet(X1,X2)))),
inference(step,[status(thm)],[t70830,t11]) ).
cnf(t70832,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(X2,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t70831,t12]) ).
cnf(t70833,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t70832,t11]) ).
cnf(t10795,plain,
meet(meet(X1,X2),join(X2,join(X3,meet(X1,X2)))) = meet(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t70833]) ).
cnf(t10834,plain,
meet(X1,meet(X2,join(X2,meet(X1,X3)))) = meet(meet(X1,X2),join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t10795,t3049]) ).
cnf(t70834,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t10834,t9861]) ).
cnf(t10975,plain,
meet(meet(X1,X2),join(X2,meet(X1,X3))) = meet(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t70834]) ).
cnf(t70855,plain,
meet(meet(X1,X2),join(X2,meet(X1,X3))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t10975,t11673]) ).
cnf(t11678,plain,
meet(meet(X1,X2),join(X2,meet(X1,X3))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t70855]) ).
cnf(t12793,plain,
meet(X1,meet(X2,join(X1,join(X2,X3)))) = meet(meet(X1,X2),meet(join(X2,X1),join(X2,X3))),
inference(cp,[status(thm)],[t11678,t12733]) ).
cnf(t70950,plain,
meet(X1,meet(X2,join(X1,meet(X2,X3)))) = meet(meet(X1,X2),meet(join(X2,X1),join(X2,X3))),
inference(step,[status(thm)],[t12793,t12089]) ).
cnf(t70951,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),meet(join(X2,X1),join(X2,X3))),
inference(step,[status(thm)],[t70950,t11972]) ).
cnf(t70952,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t70951,t11]) ).
cnf(t16293,plain,
meet(meet(X1,X2),meet(join(X1,X2),join(X2,X3))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t70952]) ).
cnf(t16496,plain,
meet(meet(meet(X1,X2),join(X1,X2)),join(meet(X1,X2),join(X2,X3))) = join(meet(meet(X1,X2),join(X1,X2)),meet(X1,meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t12902,t16293]) ).
cnf(t70982,plain,
meet(meet(X1,X2),join(meet(X1,X2),join(X2,X3))) = join(meet(meet(X1,X2),join(X1,X2)),meet(X1,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t16496,t672]) ).
cnf(t70983,plain,
meet(meet(X1,X2),join(meet(X1,X2),meet(X2,X3))) = join(meet(meet(X1,X2),join(X1,X2)),meet(X1,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t70982,t4634]) ).
cnf(t70984,plain,
meet(meet(X1,X2),join(meet(X1,X2),meet(X2,X3))) = join(meet(X1,X2),meet(X1,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t70983,t672]) ).
cnf(t70985,plain,
meet(meet(X1,X2),join(meet(X1,X2),meet(X2,X3))) = meet(meet(X1,X2),join(X1,join(X1,X3))),
inference(step,[status(thm)],[t70984,t12902]) ).
cnf(t70986,plain,
meet(meet(X1,X2),join(meet(X1,X2),meet(X2,X3))) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t70985,t86]) ).
cnf(t19049,plain,
meet(meet(X1,X2),join(meet(X1,X2),meet(X2,X3))) = meet(meet(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t70986]) ).
cnf(t19292,plain,
join(meet(X1,X2),meet(X2,X3)) = join(meet(X2,X3),meet(meet(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t5210,t19049]) ).
cnf(t21388,plain,
join(meet(X1,X2),meet(meet(X3,X1),join(X3,X2))) = join(meet(X3,X1),meet(X1,X2)),
inference(orient,[status(thm)],[t19292]) ).
cnf(t21467,plain,
join(meet(X1,X2),meet(X2,X3)) = join(meet(X2,X3),meet(join(X1,X3),meet(X1,X2))),
inference(cp,[status(thm)],[t21388,t62]) ).
cnf(t71032,plain,
join(meet(X1,X2),meet(X2,X3)) = join(meet(X2,X3),meet(X2,meet(join(X1,X3),X1))),
inference(step,[status(thm)],[t21467,t68]) ).
cnf(t71033,plain,
join(meet(X1,X2),meet(X2,X3)) = join(meet(X2,X3),meet(X1,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t71032,t68]) ).
cnf(t23495,plain,
join(meet(X1,X2),meet(X3,meet(X1,join(X3,X2)))) = join(meet(X3,X1),meet(X1,X2)),
inference(orient,[status(thm)],[t71033]) ).
cnf(t71503,plain,
meet(X2,join(X1,meet(X2,X3))) = join(meet(X1,X2),meet(X2,X3)),
inference(step,[status(thm)],[t71502,t23495]) ).
cnf(t69898,plain,
join(meet(X1,X2),meet(X2,X3)) = meet(X2,join(X1,meet(X2,X3))),
inference(orient,[status(thm)],[t71503]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(b,meet(a,c))) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(meet(b,a),meet(a,c)) != join(meet(a,b),meet(a,c)),
inference(rw,[status(thm)],[goal_0,t62]) ).
cnf(g0_1,plain,
meet(a,join(b,meet(a,c))) != join(meet(a,b),meet(a,c)),
inference(rw,[status(thm)],[g0_0,t69898]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT022-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 20:03:09 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 21.33/3.42 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.33/3.42 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------