%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT176-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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:49 PM UTC 2026
% Result : Unsatisfiable 136.97s 20.51s
% Output : CNFRefutation 136.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 211
% Number of leaves : 10
% Syntax : Number of clauses : 581 ( 581 unt; 0 nHn; 6 RR)
% Number of literals : 581 ( 580 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 2077 ( 404 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t293345,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t6,t13]) ).
cnf(t15,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t293345]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t19,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t15,t10]) ).
cnf(t293351,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t19,t15]) ).
cnf(t293352,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t293351,t13]) ).
cnf(t293353,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t293352,t13]) ).
cnf(t88,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t293353]) ).
cnf(t8,axiom,
join(X1,meet(join(X1,meet(X2,join(X1,X3))),join(X3,X4))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,plain,
join(X1,meet(join(X1,meet(X2,join(X1,X3))),join(X3,X4))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t8]) ).
cnf(t53,plain,
join(X1,meet(join(X1,meet(X2,join(X1,X3))),join(X3,X4))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(rw,[status(thm)],[t33]) ).
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t51,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t293385,plain,
join(X1,meet(join(X3,X4),join(X1,meet(X2,join(X1,X3))))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(step,[status(thm)],[t53,t51]) ).
cnf(t172,plain,
join(X1,meet(join(X2,X3),join(X1,meet(X4,join(X1,X2))))) = join(X1,meet(X4,join(X2,meet(X1,X3)))),
inference(orient,[status(thm)],[t293385]) ).
cnf(t198,plain,
join(join(X1,X2),X3) = join(join(X1,X2),join(X3,meet(X4,join(X1,meet(X3,X2))))),
inference(cp,[status(thm)],[t88,t172]) ).
cnf(t293412,plain,
join(X3,join(X1,X2)) = join(join(X1,X2),join(X3,meet(X4,join(X1,meet(X3,X2))))),
inference(step,[status(thm)],[t198,t13]) ).
cnf(t293413,plain,
join(X2,join(X3,X1)) = join(join(X1,X2),join(X3,meet(X4,join(X1,meet(X3,X2))))),
inference(step,[status(thm)],[t293412,t15]) ).
cnf(t293414,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),join(X3,meet(X4,join(X1,meet(X3,X2))))),
inference(step,[status(thm)],[t293413,t15]) ).
cnf(t293415,plain,
join(X1,join(X2,X3)) = join(X3,join(meet(X4,join(X1,meet(X3,X2))),join(X1,X2))),
inference(step,[status(thm)],[t293414,t15]) ).
cnf(t293416,plain,
join(X1,join(X2,X3)) = join(X3,join(X2,join(meet(X4,join(X1,meet(X3,X2))),X1))),
inference(step,[status(thm)],[t293415,t15]) ).
cnf(t293417,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,join(X2,meet(X4,join(X1,meet(X3,X2)))))),
inference(step,[status(thm)],[t293416,t15]) ).
cnf(t293418,plain,
join(X1,join(X2,X3)) = join(X1,join(join(X2,meet(X4,join(X1,meet(X3,X2)))),X3)),
inference(step,[status(thm)],[t293417,t15]) ).
cnf(t293419,plain,
join(X1,join(X2,X3)) = join(X1,join(X3,join(X2,meet(X4,join(X1,meet(X3,X2)))))),
inference(step,[status(thm)],[t293418,t13]) ).
cnf(t293420,plain,
join(X1,join(X2,X3)) = join(X1,join(X2,join(meet(X4,join(X1,meet(X3,X2))),X3))),
inference(step,[status(thm)],[t293419,t15]) ).
cnf(t293421,plain,
join(X1,join(X2,X3)) = join(X1,join(X2,join(X3,meet(X4,join(X1,meet(X3,X2)))))),
inference(step,[status(thm)],[t293420,t13]) ).
cnf(t293422,plain,
join(X1,join(X2,X3)) = join(X1,join(X2,join(X3,meet(X4,join(X1,meet(X2,X3)))))),
inference(step,[status(thm)],[t293421,t51]) ).
cnf(t499,plain,
join(X1,join(X2,join(X3,meet(X4,join(X1,meet(X2,X3)))))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t293422]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t18,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t15,t9]) ).
cnf(t293347,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t18,t15]) ).
cnf(t293348,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t293347,t13]) ).
cnf(t72,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t293348]) ).
cnf(t503,plain,
join(X1,join(X2,X2)) = join(X1,join(X2,meet(X3,join(X1,meet(X2,X2))))),
inference(cp,[status(thm)],[t499,t72]) ).
cnf(t293423,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,meet(X2,X2))))),
inference(step,[status(thm)],[t503,t9]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t293424,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t293423,t11]) ).
cnf(t542,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t293424]) ).
cnf(t578,plain,
join(X1,join(join(X2,meet(X3,join(X1,X2))),X4)) = join(X4,join(X1,X2)),
inference(cp,[status(thm)],[t15,t542]) ).
cnf(t293425,plain,
join(X1,join(X4,join(X2,meet(X3,join(X1,X2))))) = join(X4,join(X1,X2)),
inference(step,[status(thm)],[t578,t13]) ).
cnf(t293426,plain,
join(X1,join(X2,join(meet(X3,join(X1,X2)),X4))) = join(X4,join(X1,X2)),
inference(step,[status(thm)],[t293425,t15]) ).
cnf(t293427,plain,
join(X1,join(X2,join(X4,meet(X3,join(X1,X2))))) = join(X4,join(X1,X2)),
inference(step,[status(thm)],[t293426,t13]) ).
cnf(t293428,plain,
join(X1,join(X2,join(X4,meet(X3,join(X1,X2))))) = join(X2,join(X4,X1)),
inference(step,[status(thm)],[t293427,t15]) ).
cnf(t293429,plain,
join(X1,join(X2,join(X4,meet(X3,join(X1,X2))))) = join(X1,join(X2,X4)),
inference(step,[status(thm)],[t293428,t15]) ).
cnf(t580,plain,
join(X1,join(X2,join(X3,meet(X4,join(X1,X2))))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t293429]) ).
cnf(t176,plain,
join(X1,meet(X2,join(X3,meet(X1,X3)))) = join(X1,meet(X3,join(X1,meet(X2,join(X1,X3))))),
inference(cp,[status(thm)],[t172,t9]) ).
cnf(t260,plain,
join(X1,meet(X2,join(X1,meet(X3,join(X1,X2))))) = join(X1,meet(X3,join(X2,meet(X1,X2)))),
inference(orient,[status(thm)],[t176]) ).
cnf(t177,plain,
join(X1,meet(X2,join(X3,meet(X1,join(X3,X4))))) = join(X1,meet(join(X3,X4),join(X1,meet(X2,join(X1,X3))))),
inference(cp,[status(thm)],[t172,t72]) ).
cnf(t293392,plain,
join(X1,meet(X2,join(X3,meet(X1,join(X3,X4))))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(step,[status(thm)],[t177,t172]) ).
cnf(t321,plain,
join(X1,meet(X2,join(X3,meet(X1,join(X3,X4))))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t293392]) ).
cnf(t335,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X3,X4))))) = join(X1,meet(X2,join(X3,meet(X1,X3)))),
inference(cp,[status(thm)],[t321,t10]) ).
cnf(t391,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X3,X4))))) = join(X1,meet(X2,join(X3,meet(X1,X3)))),
inference(orient,[status(thm)],[t335]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t293346,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t7,t51]) ).
cnf(t54,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t293346]) ).
cnf(t395,plain,
join(X1,meet(X2,join(X3,meet(X1,X3)))) = join(X1,meet(X2,join(X3,meet(X3,meet(X4,X1))))),
inference(cp,[status(thm)],[t391,t54]) ).
cnf(t293397,plain,
join(X1,meet(X2,join(X3,meet(X1,X3)))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t395,t10]) ).
cnf(t413,plain,
join(X1,meet(X2,join(X3,meet(X1,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293397]) ).
cnf(t293398,plain,
join(X1,meet(X2,join(X1,meet(X3,join(X1,X2))))) = join(X1,meet(X3,X2)),
inference(step,[status(thm)],[t260,t413]) ).
cnf(t293399,plain,
join(X1,meet(X2,join(X1,meet(X3,join(X1,X2))))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t293398,t51]) ).
cnf(t414,plain,
join(X1,meet(X2,join(X1,meet(X3,join(X1,X2))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293399]) ).
cnf(t587,plain,
join(X1,join(meet(X2,join(X1,X3)),X1)) = join(X1,join(meet(X2,join(X1,X3)),join(X1,meet(X3,X2)))),
inference(cp,[status(thm)],[t580,t414]) ).
cnf(t293543,plain,
join(X1,join(X1,meet(X2,join(X1,X3)))) = join(X1,join(meet(X2,join(X1,X3)),join(X1,meet(X3,X2)))),
inference(step,[status(thm)],[t587,t15]) ).
cnf(t293544,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,join(meet(X2,join(X1,X3)),join(X1,meet(X3,X2)))),
inference(step,[status(thm)],[t293543,t72]) ).
cnf(t293545,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,join(meet(X3,X2),join(meet(X2,join(X1,X3)),X1))),
inference(step,[status(thm)],[t293544,t15]) ).
cnf(t293546,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,join(X1,join(meet(X3,X2),meet(X2,join(X1,X3))))),
inference(step,[status(thm)],[t293545,t15]) ).
cnf(t293547,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,join(meet(X3,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t293546,t72]) ).
cnf(t293548,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,join(meet(X2,X3),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t293547,t51]) ).
cnf(t2257,plain,
join(X1,join(meet(X2,X3),meet(X2,join(X1,X3)))) = join(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t293548]) ).
cnf(t5,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t12,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t2267,plain,
join(X1,meet(X2,join(X1,join(X2,X3)))) = join(X1,join(X2,meet(X2,join(X1,join(X2,X3))))),
inference(cp,[status(thm)],[t2257,t12]) ).
cnf(t293550,plain,
join(X1,meet(X2,join(X1,join(X2,X3)))) = join(X1,X2),
inference(step,[status(thm)],[t2267,t10]) ).
cnf(t2423,plain,
join(X1,meet(X2,join(X1,join(X2,X3)))) = join(X1,X2),
inference(orient,[status(thm)],[t293550]) ).
cnf(t2425,plain,
join(X1,meet(X2,X3)) = join(X1,meet(meet(X2,X3),join(X1,meet(X2,join(X1,X3))))),
inference(cp,[status(thm)],[t2423,t2257]) ).
cnf(t3648,plain,
join(X1,meet(meet(X2,X3),join(X1,meet(X2,join(X1,X3))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t2425]) ).
cnf(t57,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t54,t11]) ).
cnf(t293349,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t57,t54]) ).
cnf(t293350,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t293349,t51]) ).
cnf(t80,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t293350]) ).
cnf(t2262,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,join(meet(X2,X3),meet(X2,join(X1,meet(X2,X3))))),
inference(cp,[status(thm)],[t2257,t80]) ).
cnf(t293553,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t2262,t542]) ).
cnf(t2564,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293553]) ).
cnf(t2599,plain,
join(X1,join(meet(X2,join(X1,meet(X2,X3))),X4)) = join(X4,join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t15,t2564]) ).
cnf(t293564,plain,
join(X1,join(X4,meet(X2,join(X1,meet(X2,X3))))) = join(X4,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t2599,t13]) ).
cnf(t293565,plain,
join(X1,join(X4,meet(X2,join(X1,meet(X2,X3))))) = join(X1,join(meet(X2,X3),X4)),
inference(step,[status(thm)],[t293564,t15]) ).
cnf(t293566,plain,
join(X1,join(X4,meet(X2,join(X1,meet(X2,X3))))) = join(X1,join(X4,meet(X2,X3))),
inference(step,[status(thm)],[t293565,t13]) ).
cnf(t2932,plain,
join(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))) = join(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t293566]) ).
cnf(t573,plain,
join(X1,meet(join(X2,meet(X3,join(X1,X2))),X4)) = join(X1,meet(join(X2,meet(X3,join(X1,X2))),join(X1,meet(X4,join(X1,X2))))),
inference(cp,[status(thm)],[t414,t542]) ).
cnf(t293430,plain,
join(X1,meet(X4,join(X2,meet(X3,join(X1,X2))))) = join(X1,meet(join(X2,meet(X3,join(X1,X2))),join(X1,meet(X4,join(X1,X2))))),
inference(step,[status(thm)],[t573,t51]) ).
cnf(t293431,plain,
join(X1,meet(X4,join(X2,meet(X3,join(X1,X2))))) = join(X1,meet(X4,join(X2,meet(X1,meet(X3,join(X1,X2)))))),
inference(step,[status(thm)],[t293430,t172]) ).
cnf(t58,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t54,t12]) ).
cnf(t293354,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t58,t54]) ).
cnf(t293355,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t293354,t51]) ).
cnf(t293356,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t293355,t51]) ).
cnf(t98,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t293356]) ).
cnf(t293432,plain,
join(X1,meet(X4,join(X2,meet(X3,join(X1,X2))))) = join(X1,meet(X4,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t293431,t98]) ).
cnf(t628,plain,
join(X1,meet(X2,join(X3,meet(X4,join(X1,X3))))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t293432]) ).
cnf(t2935,plain,
join(X1,join(X2,meet(X3,join(X2,X1)))) = join(X1,join(X2,meet(X3,join(X1,meet(X2,X3))))),
inference(cp,[status(thm)],[t2932,t628]) ).
cnf(t293583,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,join(X2,meet(X3,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t2935,t13]) ).
cnf(t293584,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t293583,t542]) ).
cnf(t3582,plain,
join(X1,join(X2,meet(X3,join(X1,meet(X2,X3))))) = join(X1,X2),
inference(orient,[status(thm)],[t293584]) ).
cnf(t3641,plain,
join(X1,meet(join(X2,meet(X3,join(X1,meet(X2,X3)))),X4)) = join(X1,meet(join(X2,meet(X3,join(X1,meet(X2,X3)))),join(X1,meet(X4,join(X1,X2))))),
inference(cp,[status(thm)],[t414,t3582]) ).
cnf(t293756,plain,
join(X1,meet(X4,join(X2,meet(X3,join(X1,meet(X2,X3)))))) = join(X1,meet(join(X2,meet(X3,join(X1,meet(X2,X3)))),join(X1,meet(X4,join(X1,X2))))),
inference(step,[status(thm)],[t3641,t51]) ).
cnf(t293757,plain,
join(X1,meet(X4,join(X2,meet(X3,join(X1,meet(X2,X3)))))) = join(X1,meet(X4,join(X2,meet(X1,meet(X3,join(X1,meet(X2,X3))))))),
inference(step,[status(thm)],[t293756,t172]) ).
cnf(t293758,plain,
join(X1,meet(X4,join(X2,meet(X3,join(X1,meet(X2,X3)))))) = join(X1,meet(X4,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t293757,t98]) ).
cnf(t12274,plain,
join(X1,meet(X2,join(X3,meet(X4,join(X1,meet(X3,X4)))))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t293758]) ).
cnf(t12281,plain,
join(X1,meet(join(meet(X1,X2),X3),join(X1,meet(X1,X2)))) = join(X1,meet(X2,join(meet(X1,X2),meet(X1,X3)))),
inference(cp,[status(thm)],[t12274,t172]) ).
cnf(t293759,plain,
join(X1,meet(join(X1,meet(X1,X2)),join(meet(X1,X2),X3))) = join(X1,meet(X2,join(meet(X1,X2),meet(X1,X3)))),
inference(step,[status(thm)],[t12281,t51]) ).
cnf(t2261,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,join(X2,meet(X2,join(X1,X2)))),
inference(cp,[status(thm)],[t2257,t11]) ).
cnf(t293549,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(step,[status(thm)],[t2261,t542]) ).
cnf(t2345,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t293549]) ).
cnf(t2410,plain,
join(X1,meet(X2,join(X2,meet(X1,X3)))) = join(X1,meet(join(X2,X3),join(X1,X2))),
inference(cp,[status(thm)],[t172,t2345]) ).
cnf(t293551,plain,
join(X1,X2) = join(X1,meet(join(X2,X3),join(X1,X2))),
inference(step,[status(thm)],[t2410,t12]) ).
cnf(t293552,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t293551,t51]) ).
cnf(t2470,plain,
join(X1,meet(join(X1,X2),join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t293552]) ).
cnf(t293760,plain,
join(X1,meet(X1,X2)) = join(X1,meet(X2,join(meet(X1,X2),meet(X1,X3)))),
inference(step,[status(thm)],[t293759,t2470]) ).
cnf(t293761,plain,
X1 = join(X1,meet(X2,join(meet(X1,X2),meet(X1,X3)))),
inference(step,[status(thm)],[t293760,t10]) ).
cnf(t12459,plain,
join(X1,meet(X2,join(meet(X1,X2),meet(X1,X3)))) = X1,
inference(orient,[status(thm)],[t293761]) ).
cnf(t2566,plain,
join(X1,meet(join(X2,X3),join(X1,X2))) = join(X1,meet(join(X2,X3),join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t2564,t172]) ).
cnf(t293581,plain,
join(X1,meet(join(X1,X2),join(X2,X3))) = join(X1,meet(join(X2,X3),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t2566,t51]) ).
cnf(t293582,plain,
join(X1,X2) = join(X1,meet(join(X2,X3),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t293581,t2470]) ).
cnf(t3467,plain,
join(X1,meet(join(X2,X3),join(X2,meet(X1,X3)))) = join(X1,X2),
inference(orient,[status(thm)],[t293582]) ).
cnf(t12474,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(meet(join(X1,X2),X3),X1))),
inference(cp,[status(thm)],[t12459,t3467]) ).
cnf(t293762,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,meet(join(X1,X2),X3)))),
inference(step,[status(thm)],[t12474,t13]) ).
cnf(t293763,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t293762,t51]) ).
cnf(t12615,plain,
join(join(X1,X2),meet(X3,join(X1,meet(X3,join(X1,X2))))) = join(X1,X2),
inference(orient,[status(thm)],[t293763]) ).
cnf(t12722,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2)))))) = join(join(X1,X2),meet(meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2))))),join(join(X1,X2),meet(X3,join(X1,X2))))),
inference(cp,[status(thm)],[t3648,t12615]) ).
cnf(t293773,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2)))))) = join(join(X1,X2),meet(join(join(X1,X2),meet(X3,join(X1,X2))),meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2))))))),
inference(step,[status(thm)],[t12722,t51]) ).
cnf(t293774,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2)))))) = join(join(X1,X2),meet(meet(X4,join(X1,meet(X4,join(X1,X2)))),meet(join(join(X1,X2),meet(X3,join(X1,X2))),X3))),
inference(step,[status(thm)],[t293773,t54]) ).
cnf(t293775,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2)))))) = join(join(X1,X2),meet(X3,meet(meet(X4,join(X1,meet(X4,join(X1,X2)))),join(join(X1,X2),meet(X3,join(X1,X2)))))),
inference(step,[status(thm)],[t293774,t54]) ).
cnf(t173,plain,
join(join(X1,X2),meet(X3,join(X1,meet(join(X1,X2),X2)))) = join(X1,X2),
inference(cp,[status(thm)],[t172,t10]) ).
cnf(t293386,plain,
join(join(X1,X2),meet(X3,join(X1,meet(X2,join(X1,X2))))) = join(X1,X2),
inference(step,[status(thm)],[t173,t51]) ).
cnf(t206,plain,
join(join(X1,X2),meet(X3,join(X1,meet(X2,join(X1,X2))))) = join(X1,X2),
inference(orient,[status(thm)],[t293386]) ).
cnf(t208,plain,
join(X1,join(X1,X2)) = join(join(X1,X2),meet(X3,join(X1,meet(join(X1,X2),join(X1,join(X1,X2)))))),
inference(cp,[status(thm)],[t206,t72]) ).
cnf(t293387,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,meet(join(X1,X2),join(X1,join(X1,X2)))))),
inference(step,[status(thm)],[t208,t72]) ).
cnf(t293388,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,meet(join(X1,X2),join(X1,X2))))),
inference(step,[status(thm)],[t293387,t72]) ).
cnf(t293389,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,join(X1,X2)))),
inference(step,[status(thm)],[t293388,t11]) ).
cnf(t293390,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t293389,t72]) ).
cnf(t241,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t293390]) ).
cnf(t293776,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2)))))) = join(join(X1,X2),meet(X3,meet(meet(X4,join(X1,meet(X4,join(X1,X2)))),join(X1,X2)))),
inference(step,[status(thm)],[t293775,t241]) ).
cnf(t293777,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2)))))) = join(join(X1,X2),meet(X3,meet(join(X1,X2),meet(X4,join(X1,meet(X4,join(X1,X2))))))),
inference(step,[status(thm)],[t293776,t51]) ).
cnf(t293778,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2)))))) = join(join(X1,X2),meet(X3,meet(X4,meet(join(X1,meet(X4,join(X1,X2))),join(X1,X2))))),
inference(step,[status(thm)],[t293777,t54]) ).
cnf(t3723,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X2)))) = join(join(X1,X2),meet(meet(X3,meet(X4,join(X1,X2))),join(join(X1,X2),meet(X3,join(X1,X2))))),
inference(cp,[status(thm)],[t3648,t241]) ).
cnf(t293585,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X2)))) = join(join(X1,X2),meet(meet(X3,meet(X4,join(X1,X2))),join(X1,X2))),
inference(step,[status(thm)],[t3723,t241]) ).
cnf(t293586,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X2)))) = join(X1,X2),
inference(step,[status(thm)],[t293585,t241]) ).
cnf(t3774,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t293586]) ).
cnf(t3806,plain,
join(join(X1,X2),meet(X3,meet(X4,meet(Y4,join(X1,X2))))) = join(join(X1,X2),meet(meet(X3,meet(X4,meet(Y4,join(X1,X2)))),join(join(X1,X2),meet(X3,join(X1,X2))))),
inference(cp,[status(thm)],[t3648,t3774]) ).
cnf(t293587,plain,
join(join(X1,X2),meet(X3,meet(X4,meet(Y4,join(X1,X2))))) = join(join(X1,X2),meet(meet(X3,meet(X4,meet(Y4,join(X1,X2)))),join(X1,X2))),
inference(step,[status(thm)],[t3806,t241]) ).
cnf(t293588,plain,
join(join(X1,X2),meet(X3,meet(X4,meet(Y4,join(X1,X2))))) = join(join(X1,X2),meet(join(X1,X2),meet(X3,meet(X4,meet(Y4,join(X1,X2)))))),
inference(step,[status(thm)],[t293587,t51]) ).
cnf(t293589,plain,
join(join(X1,X2),meet(X3,meet(X4,meet(Y4,join(X1,X2))))) = join(join(X1,X2),meet(X3,meet(meet(X4,meet(Y4,join(X1,X2))),join(X1,X2)))),
inference(step,[status(thm)],[t293588,t54]) ).
cnf(t293590,plain,
join(join(X1,X2),meet(X3,meet(X4,meet(Y4,join(X1,X2))))) = join(X1,X2),
inference(step,[status(thm)],[t293589,t3774]) ).
cnf(t3827,plain,
join(join(X1,X2),meet(X3,meet(X4,meet(Y4,join(X1,X2))))) = join(X1,X2),
inference(orient,[status(thm)],[t293590]) ).
cnf(t293779,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2)))))) = join(X1,X2),
inference(step,[status(thm)],[t293778,t3827]) ).
cnf(t13765,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X4,join(X1,X2)))))) = join(X1,X2),
inference(orient,[status(thm)],[t293779]) ).
cnf(t3528,plain,
join(X1,X2) = join(X1,meet(join(X2,meet(X3,join(X1,X4))),join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t3467,t98]) ).
cnf(t293679,plain,
join(X1,X2) = join(X1,meet(join(X2,meet(X1,X3)),join(X2,meet(X3,join(X1,X4))))),
inference(step,[status(thm)],[t3528,t51]) ).
cnf(t7250,plain,
join(X1,meet(join(X2,meet(X1,X3)),join(X2,meet(X3,join(X1,X4))))) = join(X1,X2),
inference(orient,[status(thm)],[t293679]) ).
cnf(t13808,plain,
join(X1,meet(X2,join(X1,X3))) = join(join(X1,meet(X2,join(X1,X3))),meet(X4,meet(join(X1,meet(X1,X2)),join(X1,X1)))),
inference(cp,[status(thm)],[t13765,t7250]) ).
cnf(t293784,plain,
join(X1,meet(X2,join(X1,X3))) = join(join(X1,meet(X2,join(X1,X3))),meet(X4,meet(X1,join(X1,X1)))),
inference(step,[status(thm)],[t13808,t10]) ).
cnf(t293785,plain,
join(X1,meet(X2,join(X1,X3))) = join(join(X1,meet(X2,join(X1,X3))),meet(X4,X1)),
inference(step,[status(thm)],[t293784,t12]) ).
cnf(t293786,plain,
join(X1,meet(X2,join(X1,X3))) = join(meet(X4,X1),join(X1,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t293785,t13]) ).
cnf(t293787,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,join(meet(X2,join(X1,X3)),meet(X4,X1))),
inference(step,[status(thm)],[t293786,t15]) ).
cnf(t293788,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,join(meet(X4,X1),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t293787,t13]) ).
cnf(t293789,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,join(meet(X1,X4),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t293788,t51]) ).
cnf(t14139,plain,
join(X1,join(meet(X1,X2),meet(X3,join(X1,X4)))) = join(X1,meet(X3,join(X1,X4))),
inference(orient,[status(thm)],[t293789]) ).
cnf(t2950,plain,
join(X1,join(X2,meet(X3,join(X1,meet(X4,join(X1,X3)))))) = join(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))),
inference(cp,[status(thm)],[t2932,t414]) ).
cnf(t293658,plain,
join(X1,join(X2,meet(X3,join(X1,meet(X4,join(X1,X3)))))) = join(X1,join(X2,meet(X3,X4))),
inference(step,[status(thm)],[t2950,t2932]) ).
cnf(t5770,plain,
join(X1,join(X2,meet(X3,join(X1,meet(X4,join(X1,X3)))))) = join(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t293658]) ).
cnf(t14145,plain,
join(X1,meet(X2,join(X1,meet(X3,join(X1,X2))))) = join(X1,join(meet(X1,X4),meet(X2,X3))),
inference(cp,[status(thm)],[t14139,t5770]) ).
cnf(t293790,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X1,X4),meet(X2,X3))),
inference(step,[status(thm)],[t14145,t414]) ).
cnf(t14271,plain,
join(X1,join(meet(X1,X2),meet(X3,X4))) = join(X1,meet(X3,X4)),
inference(orient,[status(thm)],[t293790]) ).
cnf(t14333,plain,
join(X1,meet(join(meet(X1,X2),X3),join(X3,X4))) = join(X1,join(meet(X1,X2),X3)),
inference(cp,[status(thm)],[t14271,t2470]) ).
cnf(t293800,plain,
join(X1,meet(join(X3,X4),join(meet(X1,X2),X3))) = join(X1,join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t14333,t51]) ).
cnf(t293801,plain,
join(X1,meet(join(X3,X4),join(X3,meet(X1,X2)))) = join(X1,join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t293800,t13]) ).
cnf(t293802,plain,
join(X1,meet(join(X3,X4),join(X3,meet(X1,X2)))) = join(X1,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t293801,t13]) ).
cnf(t293803,plain,
join(X1,meet(join(X3,X4),join(X3,meet(X1,X2)))) = join(X1,X3),
inference(step,[status(thm)],[t293802,t88]) ).
cnf(t14957,plain,
join(X1,meet(join(X2,X3),join(X2,meet(X1,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t293803]) ).
cnf(t420,plain,
join(X1,meet(X2,meet(X3,join(X1,X4)))) = join(X1,meet(X2,join(meet(X3,join(X1,X4)),meet(X1,X3)))),
inference(cp,[status(thm)],[t413,t98]) ).
cnf(t293500,plain,
join(X1,meet(X2,meet(X3,join(X1,X4)))) = join(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,X4))))),
inference(step,[status(thm)],[t420,t13]) ).
cnf(t1394,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,X4))))) = join(X1,meet(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t293500]) ).
cnf(t1405,plain,
join(X1,meet(X2,meet(meet(X1,X3),join(X1,X4)))) = join(X1,meet(X2,join(meet(X1,X3),meet(meet(X1,X3),join(X1,X4))))),
inference(cp,[status(thm)],[t1394,t80]) ).
cnf(t293501,plain,
join(X1,meet(X2,meet(meet(X1,X3),join(X1,X4)))) = join(X1,meet(X2,meet(X1,X3))),
inference(step,[status(thm)],[t1405,t10]) ).
cnf(t293502,plain,
join(X1,meet(X2,meet(meet(X1,X3),join(X1,X4)))) = join(X1,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t293501,t54]) ).
cnf(t293503,plain,
join(X1,meet(X2,meet(meet(X1,X3),join(X1,X4)))) = X1,
inference(step,[status(thm)],[t293502,t10]) ).
cnf(t1455,plain,
join(X1,meet(X2,meet(meet(X1,X3),join(X1,X4)))) = X1,
inference(orient,[status(thm)],[t293503]) ).
cnf(t1456,plain,
X1 = join(X1,meet(meet(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t1455,t80]) ).
cnf(t1511,plain,
join(X1,meet(meet(X1,X2),join(X1,X3))) = X1,
inference(orient,[status(thm)],[t1456]) ).
cnf(t1557,plain,
join(X1,meet(meet(X1,X2),join(X3,meet(X1,X4)))) = join(X1,meet(join(X3,X4),X1)),
inference(cp,[status(thm)],[t172,t1511]) ).
cnf(t293510,plain,
join(X1,meet(meet(X1,X2),join(X3,meet(X1,X4)))) = join(X1,meet(X1,join(X3,X4))),
inference(step,[status(thm)],[t1557,t51]) ).
cnf(t293511,plain,
join(X1,meet(meet(X1,X2),join(X3,meet(X1,X4)))) = X1,
inference(step,[status(thm)],[t293510,t10]) ).
cnf(t1673,plain,
join(X1,meet(meet(X1,X2),join(X3,meet(X1,X4)))) = X1,
inference(orient,[status(thm)],[t293511]) ).
cnf(t1689,plain,
X1 = join(X1,meet(meet(X1,X2),join(X3,X4))),
inference(cp,[status(thm)],[t1673,t206]) ).
cnf(t1742,plain,
join(X1,meet(meet(X1,X2),join(X3,X4))) = X1,
inference(orient,[status(thm)],[t1689]) ).
cnf(t1749,plain,
X1 = join(X1,meet(meet(X2,meet(X3,X1)),join(X4,Y4))),
inference(cp,[status(thm)],[t1742,t54]) ).
cnf(t293513,plain,
X1 = join(X1,meet(join(X4,Y4),meet(X2,meet(X3,X1)))),
inference(step,[status(thm)],[t1749,t51]) ).
cnf(t293514,plain,
X1 = join(X1,meet(meet(X3,X1),meet(join(X4,Y4),X2))),
inference(step,[status(thm)],[t293513,t54]) ).
cnf(t293515,plain,
X1 = join(X1,meet(X2,meet(meet(X3,X1),join(X4,Y4)))),
inference(step,[status(thm)],[t293514,t54]) ).
cnf(t293516,plain,
X1 = join(X1,meet(X2,meet(meet(X1,X3),join(X4,Y4)))),
inference(step,[status(thm)],[t293515,t51]) ).
cnf(t1858,plain,
join(X1,meet(X2,meet(meet(X1,X3),join(X4,Y4)))) = X1,
inference(orient,[status(thm)],[t293516]) ).
cnf(t15019,plain,
join(join(X1,X2),X3) = join(join(X1,X2),meet(join(X3,X4),join(X3,X1))),
inference(cp,[status(thm)],[t14957,t14957]) ).
cnf(t293804,plain,
join(X3,join(X1,X2)) = join(join(X1,X2),meet(join(X3,X4),join(X3,X1))),
inference(step,[status(thm)],[t15019,t13]) ).
cnf(t293805,plain,
join(X2,join(X3,X1)) = join(join(X1,X2),meet(join(X3,X4),join(X3,X1))),
inference(step,[status(thm)],[t293804,t15]) ).
cnf(t293806,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X3,X4),join(X3,X1))),
inference(step,[status(thm)],[t293805,t15]) ).
cnf(t293807,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X3,X1),join(X3,X4))),
inference(step,[status(thm)],[t293806,t51]) ).
cnf(t293808,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X1,X3),join(X3,X4))),
inference(step,[status(thm)],[t293807,t13]) ).
cnf(t15148,plain,
join(join(X1,X2),meet(join(X1,X3),join(X3,X4))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t293808]) ).
cnf(t15451,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(cp,[status(thm)],[t12,t15148]) ).
cnf(t15636,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t15451]) ).
cnf(t15778,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(join(X1,X2),join(X4,Y4)))),
inference(cp,[status(thm)],[t1858,t15636]) ).
cnf(t23631,plain,
join(join(X1,X2),meet(X3,meet(join(X1,X2),join(X4,Y4)))) = join(X1,X2),
inference(orient,[status(thm)],[t15778]) ).
cnf(t565,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(join(X1,X2),join(meet(X3,join(X1,X2)),meet(X4,join(X1,X2)))),
inference(cp,[status(thm)],[t542,t241]) ).
cnf(t293468,plain,
join(X1,X2) = join(join(X1,X2),join(meet(X3,join(X1,X2)),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t565,t241]) ).
cnf(t1067,plain,
join(join(X1,X2),join(meet(X3,join(X1,X2)),meet(X4,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t293468]) ).
cnf(t2421,plain,
join(X1,join(meet(X2,join(X1,X2)),X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t15,t2345]) ).
cnf(t293554,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X3,join(X1,X2)),
inference(step,[status(thm)],[t2421,t13]) ).
cnf(t293555,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X2,join(X3,X1)),
inference(step,[status(thm)],[t293554,t15]) ).
cnf(t293556,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t293555,t15]) ).
cnf(t2601,plain,
join(X1,join(X2,meet(X3,join(X1,X3)))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t293556]) ).
cnf(t2614,plain,
join(meet(X1,X2),join(meet(X2,join(X1,X3)),X1)) = join(meet(X1,X2),join(X1,meet(meet(X2,join(X1,X3)),meet(X2,join(X1,X3))))),
inference(cp,[status(thm)],[t2601,t1394]) ).
cnf(t293621,plain,
join(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = join(meet(X1,X2),join(X1,meet(meet(X2,join(X1,X3)),meet(X2,join(X1,X3))))),
inference(step,[status(thm)],[t2614,t15]) ).
cnf(t293622,plain,
join(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = join(X1,join(meet(meet(X2,join(X1,X3)),meet(X2,join(X1,X3))),meet(X1,X2))),
inference(step,[status(thm)],[t293621,t15]) ).
cnf(t293623,plain,
join(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = join(X1,meet(meet(X2,join(X1,X3)),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t293622,t88]) ).
cnf(t293624,plain,
join(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = join(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t293623,t11]) ).
cnf(t4678,plain,
join(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = join(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t293624]) ).
cnf(t4681,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,join(meet(X1,X2),meet(X2,X3))),
inference(cp,[status(thm)],[t4678,t2932]) ).
cnf(t293625,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t4681,t2564]) ).
cnf(t4745,plain,
join(X1,join(meet(X1,X2),meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293625]) ).
cnf(t4758,plain,
join(X1,meet(X2,join(X3,meet(meet(X1,X2),X3)))) = join(X1,join(meet(X1,X2),meet(X2,X3))),
inference(cp,[status(thm)],[t4745,t413]) ).
cnf(t293626,plain,
join(X1,meet(X2,join(X3,meet(X3,meet(X1,X2))))) = join(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t4758,t51]) ).
cnf(t293627,plain,
join(X1,meet(X2,join(X3,meet(X2,meet(X3,X1))))) = join(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t293626,t54]) ).
cnf(t293628,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X2,X3))))) = join(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t293627,t54]) ).
cnf(t293629,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X2,X3))))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t293628,t4745]) ).
cnf(t4817,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X2,X3))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293629]) ).
cnf(t4824,plain,
join(meet(X1,X2),meet(X1,X2)) = join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2)))),
inference(cp,[status(thm)],[t4817,t11]) ).
cnf(t293630,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2)))),
inference(step,[status(thm)],[t4824,t9]) ).
cnf(t4887,plain,
join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t293630]) ).
cnf(t4921,plain,
join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2)))) = join(meet(X1,X2),join(meet(X3,join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2))))),meet(X4,join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2))))))),
inference(cp,[status(thm)],[t1067,t4887]) ).
cnf(t293696,plain,
meet(X1,X2) = join(meet(X1,X2),join(meet(X3,join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2))))),meet(X4,join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2))))))),
inference(step,[status(thm)],[t4921,t4887]) ).
cnf(t293697,plain,
meet(X1,X2) = join(meet(X1,X2),join(meet(X3,meet(X1,X2)),meet(X4,join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2))))))),
inference(step,[status(thm)],[t293696,t4887]) ).
cnf(t293698,plain,
meet(X1,X2) = join(meet(X1,X2),join(meet(X2,meet(X3,X1)),meet(X4,join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2))))))),
inference(step,[status(thm)],[t293697,t54]) ).
cnf(t293699,plain,
meet(X1,X2) = join(meet(X1,X2),join(meet(X1,meet(X2,X3)),meet(X4,join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2))))))),
inference(step,[status(thm)],[t293698,t54]) ).
cnf(t293700,plain,
meet(X1,X2) = join(meet(X1,X2),join(meet(X1,meet(X2,X3)),meet(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t293699,t4887]) ).
cnf(t293701,plain,
meet(X1,X2) = join(meet(X1,X2),join(meet(X1,meet(X2,X3)),meet(X2,meet(X4,X1)))),
inference(step,[status(thm)],[t293700,t54]) ).
cnf(t293702,plain,
meet(X1,X2) = join(meet(X1,X2),join(meet(X1,meet(X2,X3)),meet(X1,meet(X2,X4)))),
inference(step,[status(thm)],[t293701,t54]) ).
cnf(t8883,plain,
join(meet(X1,X2),join(meet(X1,meet(X2,X3)),meet(X1,meet(X2,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t293702]) ).
cnf(t23642,plain,
join(meet(X1,X2),join(meet(X1,meet(X2,X3)),meet(X1,meet(X2,X4)))) = join(meet(X1,X2),meet(Y4,meet(join(meet(X1,X2),join(meet(X1,meet(X2,X3)),meet(X1,meet(X2,X4)))),join(Y5,Y6)))),
inference(cp,[status(thm)],[t23631,t8883]) ).
cnf(t293907,plain,
meet(X1,X2) = join(meet(X1,X2),meet(Y4,meet(join(meet(X1,X2),join(meet(X1,meet(X2,X3)),meet(X1,meet(X2,X4)))),join(Y5,Y6)))),
inference(step,[status(thm)],[t23642,t8883]) ).
cnf(t293908,plain,
meet(X1,X2) = join(meet(X1,X2),meet(Y4,meet(meet(X1,X2),join(Y5,Y6)))),
inference(step,[status(thm)],[t293907,t8883]) ).
cnf(t27257,plain,
join(meet(X1,X2),meet(X3,meet(meet(X1,X2),join(X4,Y4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t293908]) ).
cnf(t27335,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(meet(X2,X3),X4),meet(X2,X3))),
inference(cp,[status(thm)],[t14957,t27257]) ).
cnf(t293909,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X3,meet(join(meet(X2,X3),X4),X2))),
inference(step,[status(thm)],[t27335,t54]) ).
cnf(t293910,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(meet(X2,X3),X4)))),
inference(step,[status(thm)],[t293909,t54]) ).
cnf(t293911,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(X4,meet(X2,X3))))),
inference(step,[status(thm)],[t293910,t13]) ).
cnf(t27437,plain,
join(X1,meet(X2,meet(X3,join(X4,meet(X2,X3))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293911]) ).
cnf(t27476,plain,
join(X1,meet(meet(X2,X3),join(X4,Y4))) = join(X1,meet(meet(X2,X3),meet(join(X4,Y4),X2))),
inference(cp,[status(thm)],[t27437,t1742]) ).
cnf(t293927,plain,
join(X1,meet(meet(X2,X3),join(X4,Y4))) = join(X1,meet(X2,meet(meet(X2,X3),join(X4,Y4)))),
inference(step,[status(thm)],[t27476,t54]) ).
cnf(t28507,plain,
join(X1,meet(X2,meet(meet(X2,X3),join(X4,Y4)))) = join(X1,meet(meet(X2,X3),join(X4,Y4))),
inference(orient,[status(thm)],[t293927]) ).
cnf(t28513,plain,
join(X1,meet(meet(X2,X3),join(X2,X4))) = join(X1,meet(X2,meet(X2,X3))),
inference(cp,[status(thm)],[t28507,t98]) ).
cnf(t293928,plain,
join(X1,meet(meet(X2,X3),join(X2,X4))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t28513,t80]) ).
cnf(t28656,plain,
join(X1,meet(meet(X2,X3),join(X2,X4))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293928]) ).
cnf(t28667,plain,
join(meet(meet(X1,X2),join(X1,X3)),meet(X1,X2)) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t28656,t9]) ).
cnf(t293935,plain,
join(meet(X1,X2),meet(meet(X1,X2),join(X1,X3))) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t28667,t13]) ).
cnf(t293936,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t293935,t28656]) ).
cnf(t293937,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t293936,t9]) ).
cnf(t29962,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t293937]) ).
cnf(t15154,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X1,X3),X3)),
inference(cp,[status(thm)],[t15148,t413]) ).
cnf(t293810,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(X3,join(X1,X3))),
inference(step,[status(thm)],[t15154,t51]) ).
cnf(t15980,plain,
join(join(X1,X2),meet(X3,join(X1,X3))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t293810]) ).
cnf(t16291,plain,
join(join(X1,X2),meet(X3,join(X1,X3))) = join(join(X1,X2),meet(X3,join(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t2564,t15980]) ).
cnf(t293811,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(X3,join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t16291,t15980]) ).
cnf(t16408,plain,
join(join(X1,X2),meet(X3,join(X1,join(X2,X3)))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t293811]) ).
cnf(t29990,plain,
meet(join(X1,X2),X3) = meet(meet(join(X1,X2),X3),join(X1,join(X2,X4))),
inference(cp,[status(thm)],[t29962,t16408]) ).
cnf(t293939,plain,
meet(X3,join(X1,X2)) = meet(meet(join(X1,X2),X3),join(X1,join(X2,X4))),
inference(step,[status(thm)],[t29990,t51]) ).
cnf(t293940,plain,
meet(X3,join(X1,X2)) = meet(meet(X3,join(X1,X2)),join(X1,join(X2,X4))),
inference(step,[status(thm)],[t293939,t51]) ).
cnf(t30134,plain,
meet(meet(X1,join(X2,X3)),join(X2,join(X3,X4))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t293940]) ).
cnf(t30138,plain,
meet(X1,join(X2,X2)) = meet(meet(X1,X2),join(X2,join(X2,X3))),
inference(cp,[status(thm)],[t30134,t9]) ).
cnf(t293941,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,join(X2,X3))),
inference(step,[status(thm)],[t30138,t9]) ).
cnf(t293942,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t293941,t72]) ).
cnf(t30469,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t293942]) ).
cnf(t30471,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(cp,[status(thm)],[t30469,t98]) ).
cnf(t293943,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(step,[status(thm)],[t30471,t98]) ).
cnf(t293944,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t293943,t13]) ).
cnf(t30659,plain,
meet(meet(X1,X2),join(X3,meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t293944]) ).
cnf(t30661,plain,
meet(X1,meet(X1,X2)) = meet(meet(X1,X2),join(X3,meet(meet(X1,X2),join(X1,X4)))),
inference(cp,[status(thm)],[t30659,t80]) ).
cnf(t293945,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(meet(X1,X2),join(X1,X4)))),
inference(step,[status(thm)],[t30661,t80]) ).
cnf(t293946,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t293945,t28656]) ).
cnf(t30864,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t293946]) ).
cnf(t2492,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,meet(join(X1,X2),join(meet(X2,join(X1,X2)),X3))),
inference(cp,[status(thm)],[t2470,t2345]) ).
cnf(t293579,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(meet(X2,join(X1,X2)),X3))),
inference(step,[status(thm)],[t2492,t2345]) ).
cnf(t293580,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(X3,meet(X2,join(X1,X2))))),
inference(step,[status(thm)],[t293579,t13]) ).
cnf(t3317,plain,
join(X1,meet(join(X1,X2),join(X3,meet(X2,join(X1,X2))))) = join(X1,X2),
inference(orient,[status(thm)],[t293580]) ).
cnf(t14968,plain,
join(X1,X2) = join(X1,meet(join(X3,join(X4,X2)),join(X2,meet(X1,Y4)))),
inference(cp,[status(thm)],[t14957,t15]) ).
cnf(t293817,plain,
join(X1,X2) = join(X1,meet(join(X2,meet(X1,Y4)),join(X3,join(X4,X2)))),
inference(step,[status(thm)],[t14968,t51]) ).
cnf(t293818,plain,
join(X1,X2) = join(X1,meet(join(X2,meet(X1,Y4)),join(X2,join(X3,X4)))),
inference(step,[status(thm)],[t293817,t15]) ).
cnf(t17252,plain,
join(X1,meet(join(X2,meet(X1,X3)),join(X2,join(X4,Y4)))) = join(X1,X2),
inference(orient,[status(thm)],[t293818]) ).
cnf(t17395,plain,
join(X1,join(X1,meet(X2,X3))) = join(X1,meet(join(X1,join(X1,meet(X2,X3))),join(X2,X1))),
inference(cp,[status(thm)],[t3317,t17252]) ).
cnf(t293819,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X1,join(X1,meet(X2,X3))),join(X2,X1))),
inference(step,[status(thm)],[t17395,t72]) ).
cnf(t293820,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X2,X1),join(X1,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t293819,t51]) ).
cnf(t293821,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X1,X2),join(X1,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t293820,t13]) ).
cnf(t293822,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X1,X2),join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t293821,t72]) ).
cnf(t17446,plain,
join(X1,meet(join(X1,X2),join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293822]) ).
cnf(t17653,plain,
join(X1,meet(meet(X2,X3),join(X1,X2))) = join(X1,meet(meet(X2,X3),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t414,t17446]) ).
cnf(t293823,plain,
join(X1,meet(meet(X2,X3),join(X1,X2))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t17653,t2345]) ).
cnf(t17685,plain,
join(X1,meet(meet(X2,X3),join(X1,X2))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293823]) ).
cnf(t17697,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(meet(X3,meet(X4,X2)),join(X1,X2))),
inference(cp,[status(thm)],[t17685,t54]) ).
cnf(t293839,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(join(X1,X2),meet(X3,meet(X4,X2)))),
inference(step,[status(thm)],[t17697,t51]) ).
cnf(t293840,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(meet(X4,X2),meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t293839,t54]) ).
cnf(t293841,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(X3,meet(meet(X4,X2),join(X1,X2)))),
inference(step,[status(thm)],[t293840,t54]) ).
cnf(t293842,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(X3,meet(meet(X2,X4),join(X1,X2)))),
inference(step,[status(thm)],[t293841,t51]) ).
cnf(t18888,plain,
join(X1,meet(X2,meet(meet(X3,X4),join(X1,X3)))) = join(X1,meet(X3,meet(X2,X4))),
inference(orient,[status(thm)],[t293842]) ).
cnf(t19070,plain,
join(X1,meet(X2,meet(meet(X3,X4),join(X1,X3)))) = join(X1,meet(X2,join(X1,meet(X3,meet(X2,X4))))),
inference(cp,[status(thm)],[t2564,t18888]) ).
cnf(t293854,plain,
join(X1,meet(X3,meet(X2,X4))) = join(X1,meet(X2,join(X1,meet(X3,meet(X2,X4))))),
inference(step,[status(thm)],[t19070,t18888]) ).
cnf(t20004,plain,
join(X1,meet(X2,join(X1,meet(X3,meet(X2,X4))))) = join(X1,meet(X3,meet(X2,X4))),
inference(orient,[status(thm)],[t293854]) ).
cnf(t4902,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X1,meet(X2,X3)),meet(X2,X3))),
inference(cp,[status(thm)],[t2470,t4887]) ).
cnf(t293636,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X3,meet(join(X1,meet(X2,X3)),X2))),
inference(step,[status(thm)],[t4902,t54]) ).
cnf(t293637,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t293636,t54]) ).
cnf(t5124,plain,
join(X1,meet(X2,meet(X3,join(X1,meet(X2,X3))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293637]) ).
cnf(t20013,plain,
join(X1,meet(X2,meet(X3,join(X1,meet(X2,X3))))) = join(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t20004,t5124]) ).
cnf(t293855,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t20013,t5124]) ).
cnf(t20156,plain,
join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t293855]) ).
cnf(t20246,plain,
join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(X1,meet(join(X1,X2),join(X1,meet(X3,X2)))),
inference(cp,[status(thm)],[t17446,t20156]) ).
cnf(t293856,plain,
join(X1,meet(X3,X2)) = join(X1,meet(join(X1,X2),join(X1,meet(X3,X2)))),
inference(step,[status(thm)],[t20246,t20156]) ).
cnf(t20344,plain,
join(X1,meet(join(X1,X2),join(X1,meet(X3,X2)))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t293856]) ).
cnf(t20585,plain,
join(X1,meet(meet(X2,X3),join(X1,X3))) = join(X1,meet(meet(X2,X3),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t414,t20344]) ).
cnf(t293857,plain,
join(X1,meet(meet(X2,X3),join(X1,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t20585,t2345]) ).
cnf(t20613,plain,
join(X1,meet(meet(X2,X3),join(X1,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293857]) ).
cnf(t14407,plain,
join(X1,join(join(meet(X1,X2),meet(X3,X4)),Y4)) = join(Y4,join(X1,meet(X3,X4))),
inference(cp,[status(thm)],[t15,t14271]) ).
cnf(t293812,plain,
join(X1,join(Y4,join(meet(X1,X2),meet(X3,X4)))) = join(Y4,join(X1,meet(X3,X4))),
inference(step,[status(thm)],[t14407,t13]) ).
cnf(t293813,plain,
join(X1,join(Y4,join(meet(X1,X2),meet(X3,X4)))) = join(X1,join(meet(X3,X4),Y4)),
inference(step,[status(thm)],[t293812,t15]) ).
cnf(t293814,plain,
join(X1,join(Y4,join(meet(X1,X2),meet(X3,X4)))) = join(X1,join(Y4,meet(X3,X4))),
inference(step,[status(thm)],[t293813,t13]) ).
cnf(t16820,plain,
join(X1,join(X2,join(meet(X1,X3),meet(X4,Y4)))) = join(X1,join(X2,meet(X4,Y4))),
inference(orient,[status(thm)],[t293814]) ).
cnf(t16835,plain,
join(X1,join(X2,meet(X3,join(X2,meet(X1,X4))))) = join(X1,join(X2,meet(X1,X4))),
inference(cp,[status(thm)],[t16820,t542]) ).
cnf(t293815,plain,
join(X1,join(X2,meet(X3,join(X2,meet(X1,X4))))) = join(X1,X2),
inference(step,[status(thm)],[t16835,t88]) ).
cnf(t16964,plain,
join(X1,join(X2,meet(X3,join(X2,meet(X1,X4))))) = join(X1,X2),
inference(orient,[status(thm)],[t293815]) ).
cnf(t16971,plain,
join(X1,meet(X1,X2)) = join(X1,meet(X3,join(meet(X1,X2),meet(X1,X4)))),
inference(cp,[status(thm)],[t16964,t14271]) ).
cnf(t293816,plain,
X1 = join(X1,meet(X3,join(meet(X1,X2),meet(X1,X4)))),
inference(step,[status(thm)],[t16971,t10]) ).
cnf(t17085,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X1,X4)))) = X1,
inference(orient,[status(thm)],[t293816]) ).
cnf(t17103,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(meet(join(X1,X2),X4),X1))),
inference(cp,[status(thm)],[t17085,t14957]) ).
cnf(t293881,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,meet(join(X1,X2),X4)))),
inference(step,[status(thm)],[t17103,t13]) ).
cnf(t293882,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,meet(X4,join(X1,X2))))),
inference(step,[status(thm)],[t293881,t51]) ).
cnf(t24414,plain,
join(join(X1,X2),meet(X3,join(X1,meet(X4,join(X1,X2))))) = join(X1,X2),
inference(orient,[status(thm)],[t293882]) ).
cnf(t24470,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,meet(X4,X2)))),
inference(cp,[status(thm)],[t24414,t20613]) ).
cnf(t293883,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,meet(X2,X4)))),
inference(step,[status(thm)],[t24470,t51]) ).
cnf(t24603,plain,
join(join(X1,X2),meet(X3,join(X1,meet(X2,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t293883]) ).
cnf(t24797,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X2,Y4))))) = join(join(X1,X2),meet(meet(X3,meet(X4,join(X1,meet(X2,Y4)))),join(X1,X2))),
inference(cp,[status(thm)],[t20613,t24603]) ).
cnf(t293912,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X2,Y4))))) = join(X1,X2),
inference(step,[status(thm)],[t24797,t241]) ).
cnf(t27625,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,meet(X2,Y4))))) = join(X1,X2),
inference(orient,[status(thm)],[t293912]) ).
cnf(t30791,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(X4,X2))),
inference(cp,[status(thm)],[t27625,t30659]) ).
cnf(t293947,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,meet(X3,X4))),
inference(step,[status(thm)],[t30791,t54]) ).
cnf(t31067,plain,
join(join(X1,X2),meet(X2,meet(X3,X4))) = join(X1,X2),
inference(orient,[status(thm)],[t293947]) ).
cnf(t31226,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,join(X3,X4))),
inference(cp,[status(thm)],[t31067,t15636]) ).
cnf(t31329,plain,
join(join(X1,X2),meet(X2,join(X3,X4))) = join(X1,X2),
inference(orient,[status(thm)],[t31226]) ).
cnf(t31508,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X4,X1)),
inference(cp,[status(thm)],[t30864,t31329]) ).
cnf(t293948,plain,
meet(X1,join(X2,X3)) = meet(join(X4,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t31508,t51]) ).
cnf(t293949,plain,
meet(X1,join(X2,X3)) = meet(join(X2,X3),meet(join(X4,X1),X1)),
inference(step,[status(thm)],[t293948,t54]) ).
cnf(t293950,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X4,X1))),
inference(step,[status(thm)],[t293949,t54]) ).
cnf(t293951,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,X4))),
inference(step,[status(thm)],[t293950,t13]) ).
cnf(t293952,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X4),join(X2,X3))),
inference(step,[status(thm)],[t293951,t51]) ).
cnf(t31636,plain,
meet(X1,meet(join(X1,X2),join(X3,X4))) = meet(X1,join(X3,X4)),
inference(orient,[status(thm)],[t293952]) ).
cnf(t30875,plain,
meet(X1,join(meet(X2,X3),meet(X2,X4))) = meet(meet(X1,join(meet(X2,X3),meet(X2,X4))),X2),
inference(cp,[status(thm)],[t30864,t17085]) ).
cnf(t294106,plain,
meet(X1,join(meet(X2,X3),meet(X2,X4))) = meet(X2,meet(X1,join(meet(X2,X3),meet(X2,X4)))),
inference(step,[status(thm)],[t30875,t51]) ).
cnf(t294107,plain,
meet(X1,join(meet(X2,X3),meet(X2,X4))) = meet(X1,meet(join(meet(X2,X3),meet(X2,X4)),X2)),
inference(step,[status(thm)],[t294106,t54]) ).
cnf(t294108,plain,
meet(X1,join(meet(X2,X3),meet(X2,X4))) = meet(X1,meet(X2,join(meet(X2,X3),meet(X2,X4)))),
inference(step,[status(thm)],[t294107,t51]) ).
cnf(t48519,plain,
meet(X1,meet(X2,join(meet(X2,X3),meet(X2,X4)))) = meet(X1,join(meet(X2,X3),meet(X2,X4))),
inference(orient,[status(thm)],[t294108]) ).
cnf(t31711,plain,
meet(X1,meet(meet(join(X1,X2),join(X3,X4)),Y4)) = meet(Y4,meet(X1,join(X3,X4))),
inference(cp,[status(thm)],[t54,t31636]) ).
cnf(t293989,plain,
meet(X1,meet(Y4,meet(join(X1,X2),join(X3,X4)))) = meet(Y4,meet(X1,join(X3,X4))),
inference(step,[status(thm)],[t31711,t51]) ).
cnf(t293990,plain,
meet(X1,meet(Y4,meet(join(X1,X2),join(X3,X4)))) = meet(X1,meet(join(X3,X4),Y4)),
inference(step,[status(thm)],[t293989,t54]) ).
cnf(t293991,plain,
meet(X1,meet(Y4,meet(join(X1,X2),join(X3,X4)))) = meet(X1,meet(Y4,join(X3,X4))),
inference(step,[status(thm)],[t293990,t51]) ).
cnf(t35423,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(X4,Y4)))) = meet(X1,meet(X2,join(X4,Y4))),
inference(orient,[status(thm)],[t293991]) ).
cnf(t30953,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4)),
inference(cp,[status(thm)],[t30469,t30864]) ).
cnf(t293955,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4)),
inference(step,[status(thm)],[t30953,t30864]) ).
cnf(t293956,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t293955,t13]) ).
cnf(t293957,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),X4))),
inference(step,[status(thm)],[t293956,t15]) ).
cnf(t293958,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t293957,t13]) ).
cnf(t32059,plain,
meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t293958]) ).
cnf(t4905,plain,
join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2)))) = join(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2)))))),
inference(cp,[status(thm)],[t241,t4887]) ).
cnf(t293631,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2)))))),
inference(step,[status(thm)],[t4905,t4887]) ).
cnf(t293632,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X3,meet(X1,X2))),
inference(step,[status(thm)],[t293631,t4887]) ).
cnf(t293633,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X2,meet(X3,X1))),
inference(step,[status(thm)],[t293632,t54]) ).
cnf(t293634,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t293633,t54]) ).
cnf(t4965,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t293634]) ).
cnf(t32161,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))),
inference(cp,[status(thm)],[t32059,t4965]) ).
cnf(t33198,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t32161]) ).
cnf(t33199,plain,
meet(X1,meet(X2,X3)) = meet(join(X4,meet(X1,X2)),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t33198,t51]) ).
cnf(t293965,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X3),meet(join(X4,meet(X1,X2)),X1)),
inference(step,[status(thm)],[t33199,t54]) ).
cnf(t293966,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t293965,t54]) ).
cnf(t33708,plain,
meet(X1,meet(meet(X2,X3),join(X4,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293966]) ).
cnf(t33713,plain,
meet(X1,meet(X2,X2)) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t33708,t11]) ).
cnf(t293967,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t33713,t11]) ).
cnf(t33895,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t293967]) ).
cnf(t35425,plain,
meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))) = meet(X1,meet(X2,join(X1,X4))),
inference(cp,[status(thm)],[t35423,t33895]) ).
cnf(t293992,plain,
meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))) = meet(X1,X2),
inference(step,[status(thm)],[t35425,t98]) ).
cnf(t35546,plain,
meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t293992]) ).
cnf(t48520,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(cp,[status(thm)],[t48519,t35546]) ).
cnf(t48690,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t48520]) ).
cnf(t48702,plain,
meet(X1,X2) = meet(X1,join(meet(X2,X3),meet(X2,X1))),
inference(cp,[status(thm)],[t48690,t413]) ).
cnf(t294109,plain,
meet(X1,X2) = meet(X1,join(meet(X2,X1),meet(X2,X3))),
inference(step,[status(thm)],[t48702,t13]) ).
cnf(t294110,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t294109,t51]) ).
cnf(t48997,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t294110]) ).
cnf(t49022,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X1,join(X2,X3)),X2)),
inference(cp,[status(thm)],[t48997,t14957]) ).
cnf(t294111,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t49022,t13]) ).
cnf(t49277,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t294111]) ).
cnf(t49283,plain,
meet(X1,join(X2,meet(X3,join(X2,X1)))) = meet(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t49277,t414]) ).
cnf(t294124,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t49283,t13]) ).
cnf(t50626,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t294124]) ).
cnf(t50842,plain,
meet(X1,join(X2,meet(X3,join(join(X1,X4),X2)))) = meet(X1,meet(join(X1,X4),join(X2,meet(join(X1,X4),X3)))),
inference(cp,[status(thm)],[t31636,t50626]) ).
cnf(t294274,plain,
meet(X1,join(X2,meet(X3,join(X2,join(X1,X4))))) = meet(X1,meet(join(X1,X4),join(X2,meet(join(X1,X4),X3)))),
inference(step,[status(thm)],[t50842,t13]) ).
cnf(t294275,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X4,X2))))) = meet(X1,meet(join(X1,X4),join(X2,meet(join(X1,X4),X3)))),
inference(step,[status(thm)],[t294274,t15]) ).
cnf(t294276,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X4))))) = meet(X1,meet(join(X1,X4),join(X2,meet(join(X1,X4),X3)))),
inference(step,[status(thm)],[t294275,t13]) ).
cnf(t294277,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X4))))) = meet(X1,join(X2,meet(join(X1,X4),X3))),
inference(step,[status(thm)],[t294276,t31636]) ).
cnf(t294278,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(step,[status(thm)],[t294277,t51]) ).
cnf(t72452,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t294278]) ).
cnf(t72621,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t72452,t10]) ).
cnf(t294279,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,X4))))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t72621,t50626]) ).
cnf(t72809,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,X4))))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t294279]) ).
cnf(t28752,plain,
join(X1,meet(meet(X2,X3),join(X2,X4))) = join(X1,meet(join(X2,X4),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t20156,t28656]) ).
cnf(t293932,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X2,X4),join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t28752,t28656]) ).
cnf(t29272,plain,
join(X1,meet(join(X2,X3),join(X1,meet(X2,X4)))) = join(X1,meet(X2,X4)),
inference(orient,[status(thm)],[t293932]) ).
cnf(t29298,plain,
join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(X1,meet(join(X2,X4),join(X1,meet(X3,X2)))),
inference(cp,[status(thm)],[t29272,t20156]) ).
cnf(t293933,plain,
join(X1,meet(X3,X2)) = join(X1,meet(join(X2,X4),join(X1,meet(X3,X2)))),
inference(step,[status(thm)],[t29298,t20156]) ).
cnf(t29484,plain,
join(X1,meet(join(X2,X3),join(X1,meet(X4,X2)))) = join(X1,meet(X4,X2)),
inference(orient,[status(thm)],[t293933]) ).
cnf(t49147,plain,
join(meet(join(X1,X2),X3),meet(X3,X1)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(cp,[status(thm)],[t29484,t48997]) ).
cnf(t294112,plain,
join(meet(X3,X1),meet(join(X1,X2),X3)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t49147,t13]) ).
cnf(t294113,plain,
join(meet(X1,X3),meet(join(X1,X2),X3)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t294112,t51]) ).
cnf(t294114,plain,
join(meet(X1,X3),meet(X3,join(X1,X2))) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t294113,t51]) ).
cnf(t294115,plain,
join(meet(X1,X3),meet(X3,join(X1,X2))) = meet(join(X1,X2),X3),
inference(step,[status(thm)],[t294114,t9]) ).
cnf(t294116,plain,
join(meet(X1,X3),meet(X3,join(X1,X2))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t294115,t51]) ).
cnf(t49429,plain,
join(meet(X1,X2),meet(X2,join(X1,X3))) = meet(X2,join(X1,X3)),
inference(orient,[status(thm)],[t294116]) ).
cnf(t49469,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(join(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t49429,t12]) ).
cnf(t51154,plain,
join(X1,meet(join(X1,X2),join(X1,X3))) = meet(join(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t49469]) ).
cnf(t627,plain,
join(join(X1,join(X2,meet(X3,join(X4,X1)))),join(Y4,X4)) = join(Y4,join(X4,join(X1,X2))),
inference(cp,[status(thm)],[t15,t580]) ).
cnf(t293446,plain,
join(X4,join(join(X1,join(X2,meet(X3,join(X4,X1)))),Y4)) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t627,t15]) ).
cnf(t293447,plain,
join(X4,join(Y4,join(X1,join(X2,meet(X3,join(X4,X1)))))) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t293446,t13]) ).
cnf(t293448,plain,
join(X4,join(X1,join(join(X2,meet(X3,join(X4,X1))),Y4))) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t293447,t15]) ).
cnf(t293449,plain,
join(X1,join(join(join(X2,meet(X3,join(X4,X1))),Y4),X4)) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t293448,t15]) ).
cnf(t293450,plain,
join(X1,join(X4,join(join(X2,meet(X3,join(X4,X1))),Y4))) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t293449,t13]) ).
cnf(t293451,plain,
join(X1,join(X4,join(Y4,join(X2,meet(X3,join(X4,X1)))))) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t293450,t13]) ).
cnf(t293452,plain,
join(X1,join(X4,join(X2,join(meet(X3,join(X4,X1)),Y4)))) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t293451,t15]) ).
cnf(t293453,plain,
join(X1,join(X2,join(join(meet(X3,join(X4,X1)),Y4),X4))) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t293452,t15]) ).
cnf(t293454,plain,
join(X1,join(X2,join(X4,join(meet(X3,join(X4,X1)),Y4)))) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t293453,t13]) ).
cnf(t293455,plain,
join(X1,join(X2,join(X4,join(Y4,meet(X3,join(X4,X1)))))) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t293454,t13]) ).
cnf(t293456,plain,
join(X1,join(X2,join(X4,join(Y4,meet(X3,join(X1,X4)))))) = join(Y4,join(X4,join(X1,X2))),
inference(step,[status(thm)],[t293455,t13]) ).
cnf(t293457,plain,
join(X1,join(X2,join(X4,join(Y4,meet(X3,join(X1,X4)))))) = join(X4,join(join(X1,X2),Y4)),
inference(step,[status(thm)],[t293456,t15]) ).
cnf(t293458,plain,
join(X1,join(X2,join(X4,join(Y4,meet(X3,join(X1,X4)))))) = join(X4,join(Y4,join(X1,X2))),
inference(step,[status(thm)],[t293457,t13]) ).
cnf(t293459,plain,
join(X1,join(X2,join(X4,join(Y4,meet(X3,join(X1,X4)))))) = join(X4,join(X2,join(Y4,X1))),
inference(step,[status(thm)],[t293458,t15]) ).
cnf(t293460,plain,
join(X1,join(X2,join(X4,join(Y4,meet(X3,join(X1,X4)))))) = join(X4,join(X1,join(X2,Y4))),
inference(step,[status(thm)],[t293459,t15]) ).
cnf(t293461,plain,
join(X1,join(X2,join(X4,join(Y4,meet(X3,join(X1,X4)))))) = join(X1,join(join(X2,Y4),X4)),
inference(step,[status(thm)],[t293460,t15]) ).
cnf(t293462,plain,
join(X1,join(X2,join(X4,join(Y4,meet(X3,join(X1,X4)))))) = join(X1,join(X4,join(X2,Y4))),
inference(step,[status(thm)],[t293461,t13]) ).
cnf(t293463,plain,
join(X1,join(X2,join(X4,join(Y4,meet(X3,join(X1,X4)))))) = join(X1,join(X2,join(Y4,X4))),
inference(step,[status(thm)],[t293462,t15]) ).
cnf(t293464,plain,
join(X1,join(X2,join(X4,join(Y4,meet(X3,join(X1,X4)))))) = join(X1,join(X2,join(X4,Y4))),
inference(step,[status(thm)],[t293463,t13]) ).
cnf(t847,plain,
join(X1,join(X2,join(X3,join(X4,meet(Y4,join(X1,X3)))))) = join(X1,join(X2,join(X3,X4))),
inference(orient,[status(thm)],[t293464]) ).
cnf(t854,plain,
join(X1,join(X2,join(X3,X3))) = join(X1,join(X2,join(X3,meet(X4,join(X1,X3))))),
inference(cp,[status(thm)],[t847,t72]) ).
cnf(t293465,plain,
join(X1,join(X2,X3)) = join(X1,join(X2,join(X3,meet(X4,join(X1,X3))))),
inference(step,[status(thm)],[t854,t9]) ).
cnf(t911,plain,
join(X1,join(X2,join(X3,meet(X4,join(X1,X3))))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t293465]) ).
cnf(t51475,plain,
join(X1,join(meet(join(X1,X2),join(X1,X3)),X4)) = join(X4,meet(join(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t15,t51154]) ).
cnf(t294280,plain,
join(X1,join(X4,meet(join(X1,X2),join(X1,X3)))) = join(X4,meet(join(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t51475,t13]) ).
cnf(t73080,plain,
join(X1,join(X2,meet(join(X1,X3),join(X1,X4)))) = join(X2,meet(join(X1,X3),join(X1,X4))),
inference(orient,[status(thm)],[t294280]) ).
cnf(t73399,plain,
join(X1,join(X1,X2)) = join(X1,join(X2,meet(join(X1,X3),join(X1,X2)))),
inference(cp,[status(thm)],[t911,t73080]) ).
cnf(t294283,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X3),join(X1,X2)))),
inference(step,[status(thm)],[t73399,t72]) ).
cnf(t294284,plain,
join(X1,X2) = join(X2,meet(join(X1,X3),join(X1,X2))),
inference(step,[status(thm)],[t294283,t73080]) ).
cnf(t294285,plain,
join(X1,X2) = join(X2,meet(join(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t294284,t51]) ).
cnf(t73438,plain,
join(X1,meet(join(X2,X1),join(X2,X3))) = join(X2,X1),
inference(orient,[status(thm)],[t294285]) ).
cnf(t73706,plain,
meet(join(X1,meet(join(X2,X1),join(X2,X3))),join(X1,X4)) = join(X1,meet(join(X2,X1),join(X1,X4))),
inference(cp,[status(thm)],[t51154,t73438]) ).
cnf(t294287,plain,
meet(join(X2,X1),join(X1,X4)) = join(X1,meet(join(X2,X1),join(X1,X4))),
inference(step,[status(thm)],[t73706,t73438]) ).
cnf(t74361,plain,
join(X1,meet(join(X2,X1),join(X1,X3))) = meet(join(X2,X1),join(X1,X3)),
inference(orient,[status(thm)],[t294287]) ).
cnf(t74884,plain,
join(meet(join(X1,X2),join(X2,X3)),join(X4,X2)) = join(X4,meet(join(X1,X2),join(X2,X3))),
inference(cp,[status(thm)],[t15,t74361]) ).
cnf(t294395,plain,
join(X2,join(meet(join(X1,X2),join(X2,X3)),X4)) = join(X4,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t74884,t15]) ).
cnf(t294396,plain,
join(X2,join(X4,meet(join(X1,X2),join(X2,X3)))) = join(X4,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t294395,t13]) ).
cnf(t99499,plain,
join(X1,join(X2,meet(join(X3,X1),join(X1,X4)))) = join(X2,meet(join(X3,X1),join(X1,X4))),
inference(orient,[status(thm)],[t294396]) ).
cnf(t14386,plain,
join(X1,join(X2,meet(X2,X3))) = join(X1,join(X2,meet(X4,join(X1,meet(X2,X3))))),
inference(cp,[status(thm)],[t911,t14271]) ).
cnf(t293798,plain,
join(X1,X2) = join(X1,join(X2,meet(X4,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t14386,t10]) ).
cnf(t14689,plain,
join(X1,join(X2,meet(X3,join(X1,meet(X2,X4))))) = join(X1,X2),
inference(orient,[status(thm)],[t293798]) ).
cnf(t99509,plain,
join(X1,meet(join(X2,X3),join(X3,meet(X1,X4)))) = join(X3,X1),
inference(cp,[status(thm)],[t99499,t14689]) ).
cnf(t294397,plain,
join(X1,meet(join(X2,X3),join(X3,meet(X1,X4)))) = join(X1,X3),
inference(step,[status(thm)],[t99509,t13]) ).
cnf(t100039,plain,
join(X1,meet(join(X2,X3),join(X3,meet(X1,X4)))) = join(X1,X3),
inference(orient,[status(thm)],[t294397]) ).
cnf(t100511,plain,
meet(X1,join(join(X2,X3),meet(X1,X4))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))),
inference(cp,[status(thm)],[t72809,t100039]) ).
cnf(t294500,plain,
meet(X1,join(meet(X1,X4),join(X2,X3))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))),
inference(step,[status(thm)],[t100511,t13]) ).
cnf(t294501,plain,
meet(X1,join(X3,join(meet(X1,X4),X2))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))),
inference(step,[status(thm)],[t294500,t15]) ).
cnf(t294502,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))),
inference(step,[status(thm)],[t294501,t15]) ).
cnf(t122848,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,X3)))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t294502]) ).
cnf(t122867,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(meet(X4,join(X1,X3)),join(X2,X3))),
inference(cp,[status(thm)],[t122848,t13]) ).
cnf(t294526,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X3,join(meet(X4,join(X1,X3)),X2))),
inference(step,[status(thm)],[t122867,t15]) ).
cnf(t294527,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X2,join(X3,meet(X4,join(X1,X3))))),
inference(step,[status(thm)],[t294526,t15]) ).
cnf(t131522,plain,
meet(X1,join(X2,join(X3,meet(X4,join(X1,X3))))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t294527]) ).
cnf(t49501,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t49429,t51]) ).
cnf(t50265,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t49501]) ).
cnf(t50297,plain,
meet(X1,join(meet(X1,X2),X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t50265,t80]) ).
cnf(t294178,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t50297,t13]) ).
cnf(t294179,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t294178,t13]) ).
cnf(t59125,plain,
join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))) = meet(X1,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t294179]) ).
cnf(t131545,plain,
meet(X1,join(X2,join(meet(X3,X4),meet(X1,X3)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))),
inference(cp,[status(thm)],[t131522,t59125]) ).
cnf(t295025,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X3,X4)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))),
inference(step,[status(thm)],[t131545,t13]) ).
cnf(t291702,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X3,X4)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))),
inference(orient,[status(thm)],[t295025]) ).
cnf(t74363,plain,
meet(join(X1,X2),join(X2,meet(X3,X1))) = join(X2,meet(X3,X1)),
inference(cp,[status(thm)],[t74361,t29484]) ).
cnf(t294308,plain,
meet(join(X1,X2),join(X2,meet(X1,X3))) = join(X2,meet(X3,X1)),
inference(step,[status(thm)],[t74363,t51]) ).
cnf(t294309,plain,
meet(join(X1,X2),join(X2,meet(X1,X3))) = join(X2,meet(X1,X3)),
inference(step,[status(thm)],[t294308,t51]) ).
cnf(t76023,plain,
meet(join(X1,X2),join(X2,meet(X1,X3))) = join(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t294309]) ).
cnf(t76131,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t76023,t10]) ).
cnf(t76501,plain,
meet(X1,join(meet(X1,X2),meet(X1,X3))) = join(meet(X1,X2),meet(X1,X3)),
inference(orient,[status(thm)],[t76131]) ).
cnf(t30751,plain,
join(X1,meet(X2,join(X3,X4))) = join(join(X1,meet(X2,join(X3,X4))),meet(X3,X2)),
inference(cp,[status(thm)],[t241,t30659]) ).
cnf(t293974,plain,
join(X1,meet(X2,join(X3,X4))) = join(meet(X3,X2),join(X1,meet(X2,join(X3,X4)))),
inference(step,[status(thm)],[t30751,t13]) ).
cnf(t293975,plain,
join(X1,meet(X2,join(X3,X4))) = join(X1,join(meet(X2,join(X3,X4)),meet(X3,X2))),
inference(step,[status(thm)],[t293974,t15]) ).
cnf(t293976,plain,
join(X1,meet(X2,join(X3,X4))) = join(X1,join(meet(X3,X2),meet(X2,join(X3,X4)))),
inference(step,[status(thm)],[t293975,t13]) ).
cnf(t293977,plain,
join(X1,meet(X2,join(X3,X4))) = join(X1,join(meet(X2,X3),meet(X2,join(X3,X4)))),
inference(step,[status(thm)],[t293976,t51]) ).
cnf(t34489,plain,
join(X1,join(meet(X2,X3),meet(X2,join(X3,X4)))) = join(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t293977]) ).
cnf(t34517,plain,
join(X1,meet(X2,join(X3,meet(meet(X2,X3),meet(X2,X3))))) = join(X1,join(meet(X2,X3),meet(X2,X3))),
inference(cp,[status(thm)],[t34489,t4817]) ).
cnf(t293978,plain,
join(X1,meet(X2,join(X3,meet(X2,X3)))) = join(X1,join(meet(X2,X3),meet(X2,X3))),
inference(step,[status(thm)],[t34517,t11]) ).
cnf(t293979,plain,
join(X1,meet(X2,join(X3,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t293978,t9]) ).
cnf(t34677,plain,
join(X1,meet(X2,join(X3,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293979]) ).
cnf(t34682,plain,
join(meet(X1,join(X2,meet(X1,X2))),meet(X1,X2)) = meet(X1,join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t34677,t9]) ).
cnf(t293995,plain,
join(meet(X1,X2),meet(X1,join(X2,meet(X1,X2)))) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t34682,t13]) ).
cnf(t20771,plain,
join(X1,meet(meet(X2,X3),join(meet(X1,X4),X3))) = join(X1,join(meet(X1,X4),meet(X2,X3))),
inference(cp,[status(thm)],[t14271,t20613]) ).
cnf(t293860,plain,
join(X1,meet(meet(X2,X3),join(X3,meet(X1,X4)))) = join(X1,join(meet(X1,X4),meet(X2,X3))),
inference(step,[status(thm)],[t20771,t13]) ).
cnf(t293861,plain,
join(X1,meet(meet(X2,X3),join(X3,meet(X1,X4)))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t293860,t14271]) ).
cnf(t21108,plain,
join(X1,meet(meet(X2,X3),join(X3,meet(X1,X4)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293861]) ).
cnf(t21277,plain,
join(meet(X1,X2),meet(X3,join(X2,meet(meet(X1,X2),meet(X2,X4))))) = join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2)))),
inference(cp,[status(thm)],[t321,t21108]) ).
cnf(t293402,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X3,X4))))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t391,t413]) ).
cnf(t416,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X3,X4))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t293402]) ).
cnf(t293874,plain,
join(meet(X1,X2),meet(X3,X2)) = join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2)))),
inference(step,[status(thm)],[t21277,t416]) ).
cnf(t293875,plain,
join(meet(X1,X2),meet(X2,X3)) = join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2)))),
inference(step,[status(thm)],[t293874,t51]) ).
cnf(t23021,plain,
join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2)))) = join(meet(X1,X2),meet(X2,X3)),
inference(orient,[status(thm)],[t293875]) ).
cnf(t293996,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t293995,t23021]) ).
cnf(t293997,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t293996,t51]) ).
cnf(t293998,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t293997,t9]) ).
cnf(t35916,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t293998]) ).
cnf(t36061,plain,
meet(X1,meet(join(X2,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t54,t35916]) ).
cnf(t293999,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t36061,t51]) ).
cnf(t294000,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t293999,t54]) ).
cnf(t294001,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t294000,t54]) ).
cnf(t36063,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t294001]) ).
cnf(t30907,plain,
meet(meet(X1,X2),join(X3,X4)) = meet(meet(meet(X1,X2),join(X3,X4)),X1),
inference(cp,[status(thm)],[t30864,t1742]) ).
cnf(t293954,plain,
meet(meet(X1,X2),join(X3,X4)) = meet(X1,meet(meet(X1,X2),join(X3,X4))),
inference(step,[status(thm)],[t30907,t51]) ).
cnf(t31952,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(meet(X1,X2),join(X3,X4)),
inference(orient,[status(thm)],[t293954]) ).
cnf(t36066,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(meet(X1,X3),join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t36063,t31952]) ).
cnf(t294002,plain,
meet(X1,meet(X1,meet(X3,X2))) = meet(meet(X1,X3),join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t36066,t54]) ).
cnf(t294003,plain,
meet(X1,meet(X3,X2)) = meet(meet(X1,X3),join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t294002,t80]) ).
cnf(t294004,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X3),join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t294003,t51]) ).
cnf(t36211,plain,
meet(meet(X1,X2),join(X3,meet(X1,X3))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t294004]) ).
cnf(t36221,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X3))))) = meet(meet(X1,X3),join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t36211,t33895]) ).
cnf(t294020,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X3))))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t36221,t36211]) ).
cnf(t37763,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X3))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t294020]) ).
cnf(t76804,plain,
meet(X1,meet(join(meet(X1,X2),meet(X1,X3)),X4)) = meet(X4,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t54,t76501]) ).
cnf(t294406,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X1,X3)))) = meet(X4,join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t76804,t51]) ).
cnf(t102364,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X1,X4)))) = meet(X2,join(meet(X1,X3),meet(X1,X4))),
inference(orient,[status(thm)],[t294406]) ).
cnf(t102695,plain,
meet(X1,meet(X1,X2)) = meet(X1,meet(X2,join(meet(X1,X3),meet(X1,X2)))),
inference(cp,[status(thm)],[t37763,t102364]) ).
cnf(t294408,plain,
meet(X1,X2) = meet(X1,meet(X2,join(meet(X1,X3),meet(X1,X2)))),
inference(step,[status(thm)],[t102695,t80]) ).
cnf(t294409,plain,
meet(X1,X2) = meet(X2,join(meet(X1,X3),meet(X1,X2))),
inference(step,[status(thm)],[t294408,t102364]) ).
cnf(t294410,plain,
meet(X1,X2) = meet(X2,join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t294409,t13]) ).
cnf(t102737,plain,
meet(X1,join(meet(X2,X1),meet(X2,X3))) = meet(X2,X1),
inference(orient,[status(thm)],[t294410]) ).
cnf(t102960,plain,
join(meet(X1,join(meet(X2,X1),meet(X2,X3))),meet(X1,X4)) = meet(X1,join(meet(X2,X1),meet(X1,X4))),
inference(cp,[status(thm)],[t76501,t102737]) ).
cnf(t294411,plain,
join(meet(X2,X1),meet(X1,X4)) = meet(X1,join(meet(X2,X1),meet(X1,X4))),
inference(step,[status(thm)],[t102960,t102737]) ).
cnf(t103271,plain,
meet(X1,join(meet(X2,X1),meet(X1,X3))) = join(meet(X2,X1),meet(X1,X3)),
inference(orient,[status(thm)],[t294411]) ).
cnf(t103275,plain,
join(meet(X1,X2),meet(X2,join(meet(X1,X2),X3))) = meet(X2,join(meet(X1,X2),X3)),
inference(cp,[status(thm)],[t103271,t49277]) ).
cnf(t294439,plain,
join(meet(X1,X2),meet(X2,join(X3,meet(X1,X2)))) = meet(X2,join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t103275,t13]) ).
cnf(t294440,plain,
join(meet(X1,X2),meet(X2,join(X3,meet(X1,X2)))) = meet(X2,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t294439,t13]) ).
cnf(t109757,plain,
join(meet(X1,X2),meet(X2,join(X3,meet(X1,X2)))) = meet(X2,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t294440]) ).
cnf(t291740,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X4,meet(X1,X3))))))) = meet(X1,join(X2,meet(X3,join(X4,meet(X1,X3))))),
inference(cp,[status(thm)],[t291702,t109757]) ).
cnf(t30441,plain,
join(X1,meet(join(X2,X3),meet(X4,join(X1,X2)))) = join(X1,meet(join(X2,X3),join(X1,meet(X4,join(X1,X2))))),
inference(cp,[status(thm)],[t414,t30134]) ).
cnf(t294100,plain,
join(X1,meet(join(X1,X2),meet(join(X2,X3),X4))) = join(X1,meet(join(X2,X3),join(X1,meet(X4,join(X1,X2))))),
inference(step,[status(thm)],[t30441,t54]) ).
cnf(t294101,plain,
join(X1,meet(X4,meet(join(X1,X2),join(X2,X3)))) = join(X1,meet(join(X2,X3),join(X1,meet(X4,join(X1,X2))))),
inference(step,[status(thm)],[t294100,t54]) ).
cnf(t294102,plain,
join(X1,meet(X4,meet(join(X1,X2),join(X2,X3)))) = join(X1,meet(X4,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t294101,t172]) ).
cnf(t47236,plain,
join(X1,meet(X2,meet(join(X1,X3),join(X3,X4)))) = join(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t294102]) ).
cnf(t47247,plain,
join(X1,meet(X2,join(X3,meet(X1,meet(X2,join(X1,X3)))))) = join(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t47236,t33895]) ).
cnf(t294103,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t47247,t98]) ).
cnf(t47701,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t294103]) ).
cnf(t295026,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X1,X4)))))) = meet(X1,join(X2,meet(X3,join(X4,meet(X1,X3))))),
inference(step,[status(thm)],[t291740,t47701]) ).
cnf(t295027,plain,
meet(X1,join(X2,meet(X3,join(X1,X4)))) = meet(X1,join(X2,meet(X3,join(X4,meet(X1,X3))))),
inference(step,[status(thm)],[t295026,t49277]) ).
cnf(t292480,plain,
meet(X1,join(X2,meet(X3,join(X4,meet(X1,X3))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t295027]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(b,meet(c,join(b,join(d,meet(a,c)))))) != meet(a,join(b,meet(c,join(a,d)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(b,meet(c,join(b,join(d,meet(a,c)))))) != meet(a,join(b,meet(c,join(meet(a,c),join(b,d))))),
inference(rw,[status(thm)],[goal_0,t15]) ).
cnf(g0_1,plain,
meet(a,join(b,meet(c,join(b,join(d,meet(a,c)))))) != meet(a,join(b,meet(c,join(join(b,d),meet(a,c))))),
inference(rw,[status(thm)],[g0_0,t13]) ).
cnf(g0_2,plain,
meet(a,join(b,meet(c,join(b,join(d,meet(a,c)))))) != meet(a,join(b,meet(c,join(a,join(b,d))))),
inference(rw,[status(thm)],[g0_1,t292480]) ).
cnf(g0_3,plain,
meet(a,join(b,meet(c,join(b,join(d,meet(a,c)))))) != meet(a,join(b,meet(c,join(a,d)))),
inference(rw,[status(thm)],[g0_2,t72452]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT176-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.15/0.40 % Computer : n011.cluster.edu
% 0.15/0.40 % Model : x86_64 x86_64
% 0.15/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40 % Memory : 8046.5625MB
% 0.15/0.40 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Wed Sep 23 20:27:27 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.15/0.40 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 136.97/20.51 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 136.97/20.51 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------