%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT151-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 : n010.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:35 PM UTC 2026
% Result : Unsatisfiable 58.22s 7.93s
% Output : CNFRefutation 58.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 162
% Number of leaves : 10
% Syntax : Number of clauses : 564 ( 564 unt; 0 nHn; 6 RR)
% Number of literals : 564 ( 563 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 9 ( 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 : 2285 ( 558 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(t45,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t172970,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t6,t45]) ).
cnf(t49,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t172970]) ).
cnf(t8,axiom,
meet(X1,join(X2,meet(X3,join(X4,meet(X1,X3))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,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)],[t8]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t172969,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t7,t13]) ).
cnf(t15,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t172969]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t34,plain,
meet(X1,join(meet(X2,join(X3,meet(X1,X2))),meet(X2,join(X1,X3)))) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t33,t11]) ).
cnf(t173126,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X2,join(X3,meet(X1,X2))))) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t34,t45]) ).
cnf(t173127,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X2,join(X1,X3)))) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t173126,t33]) ).
cnf(t173128,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t173127,t11]) ).
cnf(t5,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t19,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t15,t10]) ).
cnf(t172975,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t19,t15]) ).
cnf(t172976,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t172975,t13]) ).
cnf(t172977,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t172976,t13]) ).
cnf(t84,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t172977]) ).
cnf(t173129,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t173128,t84]) ).
cnf(t1652,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t173129]) ).
cnf(t1726,plain,
meet(X1,meet(meet(X2,join(X3,meet(X1,X2))),X4)) = meet(X4,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t1652]) ).
cnf(t173131,plain,
meet(X1,meet(X4,meet(X2,join(X3,meet(X1,X2))))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t1726,t13]) ).
cnf(t173132,plain,
meet(X1,meet(X2,meet(join(X3,meet(X1,X2)),X4))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t173131,t15]) ).
cnf(t173133,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X2))))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t173132,t13]) ).
cnf(t173134,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X2))))) = meet(X2,meet(X4,X1)),
inference(step,[status(thm)],[t173133,t15]) ).
cnf(t173135,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X2))))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t173134,t15]) ).
cnf(t1770,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X2))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173135]) ).
cnf(t1856,plain,
meet(X1,meet(meet(X2,meet(X3,join(X4,meet(X1,X2)))),Y4)) = meet(Y4,meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t15,t1770]) ).
cnf(t173146,plain,
meet(X1,meet(Y4,meet(X2,meet(X3,join(X4,meet(X1,X2)))))) = meet(Y4,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t1856,t13]) ).
cnf(t173147,plain,
meet(X1,meet(X2,meet(meet(X3,join(X4,meet(X1,X2))),Y4))) = meet(Y4,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t173146,t15]) ).
cnf(t173148,plain,
meet(X1,meet(X2,meet(Y4,meet(X3,join(X4,meet(X1,X2)))))) = meet(Y4,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t173147,t13]) ).
cnf(t173149,plain,
meet(X1,meet(X2,meet(X3,meet(join(X4,meet(X1,X2)),Y4)))) = meet(Y4,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t173148,t15]) ).
cnf(t173150,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(Y4,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t173149,t13]) ).
cnf(t173151,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(meet(X2,X3),Y4)),
inference(step,[status(thm)],[t173150,t15]) ).
cnf(t173152,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(Y4,meet(X2,X3))),
inference(step,[status(thm)],[t173151,t13]) ).
cnf(t173153,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(X3,meet(Y4,X2))),
inference(step,[status(thm)],[t173152,t15]) ).
cnf(t173154,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(X2,meet(X3,Y4))),
inference(step,[status(thm)],[t173153,t15]) ).
cnf(t2189,plain,
meet(X1,meet(X2,meet(X3,meet(X4,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t173154]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t18,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t15,t9]) ).
cnf(t172971,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t18,t15]) ).
cnf(t172972,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t172971,t13]) ).
cnf(t67,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t172972]) ).
cnf(t73,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X1,X4)))) = meet(X1,join(X2,meet(meet(X1,X3),join(X4,meet(X1,X3))))),
inference(cp,[status(thm)],[t33,t67]) ).
cnf(t318,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X4,meet(X1,X3))))) = meet(X1,join(X2,meet(meet(X1,X3),join(X1,X4)))),
inference(orient,[status(thm)],[t73]) ).
cnf(t332,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X1,X4)))) = meet(X1,join(X2,meet(meet(X1,X3),join(meet(X1,X3),X4)))),
inference(cp,[status(thm)],[t318,t45]) ).
cnf(t173049,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X1,X4)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t332,t10]) ).
cnf(t350,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X1,X4)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t173049]) ).
cnf(t357,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(meet(X3,meet(X4,X1)),join(X1,Y4)))),
inference(cp,[status(thm)],[t350,t15]) ).
cnf(t173052,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(join(X1,Y4),meet(X3,meet(X4,X1))))),
inference(step,[status(thm)],[t357,t13]) ).
cnf(t173053,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(meet(X4,X1),meet(join(X1,Y4),X3)))),
inference(step,[status(thm)],[t173052,t15]) ).
cnf(t173054,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(X3,meet(meet(X4,X1),join(X1,Y4))))),
inference(step,[status(thm)],[t173053,t15]) ).
cnf(t173055,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(X3,meet(meet(X1,X4),join(X1,Y4))))),
inference(step,[status(thm)],[t173054,t13]) ).
cnf(t369,plain,
meet(X1,join(X2,meet(X3,meet(meet(X1,X4),join(X1,Y4))))) = meet(X1,join(X2,meet(X1,meet(X3,X4)))),
inference(orient,[status(thm)],[t173055]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t12,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t370,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,X2),
inference(cp,[status(thm)],[t369,t12]) ).
cnf(t402,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t370]) ).
cnf(t403,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t402,t84]) ).
cnf(t424,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t403]) ).
cnf(t432,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t424,t84]) ).
cnf(t173059,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(step,[status(thm)],[t432,t84]) ).
cnf(t173060,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t173059,t45]) ).
cnf(t506,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t173060]) ).
cnf(t2218,plain,
meet(X1,meet(join(X2,X3),meet(X4,X2))) = meet(X1,meet(join(X2,X3),meet(X4,meet(X2,X1)))),
inference(cp,[status(thm)],[t2189,t506]) ).
cnf(t173155,plain,
meet(X1,meet(X2,meet(join(X2,X3),X4))) = meet(X1,meet(join(X2,X3),meet(X4,meet(X2,X1)))),
inference(step,[status(thm)],[t2218,t15]) ).
cnf(t173156,plain,
meet(X1,meet(X2,meet(X4,join(X2,X3)))) = meet(X1,meet(join(X2,X3),meet(X4,meet(X2,X1)))),
inference(step,[status(thm)],[t173155,t13]) ).
cnf(t173157,plain,
meet(X1,meet(X2,X4)) = meet(X1,meet(join(X2,X3),meet(X4,meet(X2,X1)))),
inference(step,[status(thm)],[t173156,t84]) ).
cnf(t173158,plain,
meet(X1,meet(X2,X4)) = meet(X1,meet(meet(X2,X1),meet(join(X2,X3),X4))),
inference(step,[status(thm)],[t173157,t15]) ).
cnf(t173159,plain,
meet(X1,meet(X2,X4)) = meet(X1,meet(X4,meet(meet(X2,X1),join(X2,X3)))),
inference(step,[status(thm)],[t173158,t15]) ).
cnf(t173160,plain,
meet(X1,meet(X2,X4)) = meet(X1,meet(X4,meet(meet(X1,X2),join(X2,X3)))),
inference(step,[status(thm)],[t173159,t13]) ).
cnf(t2297,plain,
meet(X1,meet(X2,meet(meet(X1,X3),join(X3,X4)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t173160]) ).
cnf(t2312,plain,
meet(X1,meet(X2,meet(meet(X1,X2),join(X2,X3)))) = meet(X1,meet(meet(X1,X2),join(X2,X3))),
inference(cp,[status(thm)],[t2297,t9]) ).
cnf(t173161,plain,
meet(X1,meet(X2,X2)) = meet(X1,meet(meet(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t2312,t2297]) ).
cnf(t173162,plain,
meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t173161,t9]) ).
cnf(t2408,plain,
meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t173162]) ).
cnf(t2447,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4))),
inference(cp,[status(thm)],[t2408,t84]) ).
cnf(t173171,plain,
meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4))),
inference(step,[status(thm)],[t2447,t84]) ).
cnf(t173172,plain,
meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(X4,meet(X2,join(X1,X3))))),
inference(step,[status(thm)],[t173171,t45]) ).
cnf(t2731,plain,
meet(X1,meet(meet(X1,X2),join(X3,meet(X2,join(X1,X4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t173172]) ).
cnf(t1689,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(meet(X2,join(X1,X3)),join(X4,meet(X1,X2)))),
inference(cp,[status(thm)],[t1652,t84]) ).
cnf(t173137,plain,
meet(X1,X2) = meet(X1,meet(meet(X2,join(X1,X3)),join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t1689,t84]) ).
cnf(t1984,plain,
meet(X1,meet(meet(X2,join(X1,X3)),join(X4,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t173137]) ).
cnf(t1992,plain,
meet(meet(X1,X2),X1) = meet(meet(X1,X2),meet(meet(X1,X2),join(X3,meet(meet(X1,X2),X1)))),
inference(cp,[status(thm)],[t1984,t506]) ).
cnf(t173138,plain,
meet(X1,meet(X1,X2)) = meet(meet(X1,X2),meet(meet(X1,X2),join(X3,meet(meet(X1,X2),X1)))),
inference(step,[status(thm)],[t1992,t13]) ).
cnf(t173139,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(X3,meet(meet(X1,X2),X1)))),
inference(step,[status(thm)],[t173138,t67]) ).
cnf(t173140,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(meet(X1,X2),X1))),
inference(step,[status(thm)],[t173139,t67]) ).
cnf(t173141,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,meet(X1,X2)))),
inference(step,[status(thm)],[t173140,t13]) ).
cnf(t173142,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t173141,t67]) ).
cnf(t2081,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t173142]) ).
cnf(t2461,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4))),
inference(cp,[status(thm)],[t2408,t2081]) ).
cnf(t173163,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4))),
inference(step,[status(thm)],[t2461,t2081]) ).
cnf(t173164,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4)),
inference(step,[status(thm)],[t173163,t67]) ).
cnf(t173165,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t173164,t45]) ).
cnf(t173166,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),X4))),
inference(step,[status(thm)],[t173165,t49]) ).
cnf(t173167,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t173166,t45]) ).
cnf(t2502,plain,
meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t173167]) ).
cnf(t53,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t49,t12]) ).
cnf(t172978,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t53,t49]) ).
cnf(t172979,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t172978,t45]) ).
cnf(t172980,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t172979,t45]) ).
cnf(t95,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t172980]) ).
cnf(t2509,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t2502,t95]) ).
cnf(t2555,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t2509]) ).
cnf(t2782,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(meet(X1,X2),meet(meet(X1,X2),join(X4,meet(join(X1,X3),join(meet(X1,X2),Y4))))),
inference(cp,[status(thm)],[t2731,t2555]) ).
cnf(t173235,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(X4,meet(join(X1,X3),join(meet(X1,X2),Y4))))),
inference(step,[status(thm)],[t2782,t2555]) ).
cnf(t173236,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(join(X1,X3),join(meet(X1,X2),Y4)))),
inference(step,[status(thm)],[t173235,t67]) ).
cnf(t173237,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(join(X1,X3),join(Y4,meet(X1,X2))))),
inference(step,[status(thm)],[t173236,t45]) ).
cnf(t4385,plain,
meet(meet(X1,X2),join(X3,meet(join(X1,X4),join(Y4,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t173237]) ).
cnf(t4412,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,join(X4,meet(X1,X2))))),
inference(cp,[status(thm)],[t4385,t11]) ).
cnf(t4492,plain,
meet(meet(X1,X2),join(X3,meet(X1,join(X4,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t4412]) ).
cnf(t4509,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))),
inference(cp,[status(thm)],[t4492,t402]) ).
cnf(t4576,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t4509]) ).
cnf(t4578,plain,
meet(X1,meet(X2,meet(meet(X1,X3),join(X3,X4)))) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
inference(cp,[status(thm)],[t4576,t2297]) ).
cnf(t173240,plain,
meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t4578,t2297]) ).
cnf(t4840,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173240]) ).
cnf(t4919,plain,
meet(X1,meet(meet(X2,X3),join(X2,X4))) = meet(meet(X1,meet(X2,X3)),join(Y4,meet(X1,join(X2,X4)))),
inference(cp,[status(thm)],[t4840,t2555]) ).
cnf(t173260,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,meet(X1,join(X2,X4)))),
inference(step,[status(thm)],[t4919,t2555]) ).
cnf(t5970,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,join(X2,Y4)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173260]) ).
cnf(t6010,plain,
meet(meet(X1,X2),meet(X3,X4)) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(cp,[status(thm)],[t5970,t2081]) ).
cnf(t173342,plain,
meet(X4,meet(meet(X1,X2),X3)) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t6010,t15]) ).
cnf(t173343,plain,
meet(X3,meet(X4,meet(X1,X2))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t173342,t15]) ).
cnf(t173344,plain,
meet(X3,meet(X2,meet(X4,X1))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t173343,t15]) ).
cnf(t173345,plain,
meet(X3,meet(X1,meet(X2,X4))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t173344,t15]) ).
cnf(t173346,plain,
meet(X1,meet(meet(X2,X4),X3)) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t173345,t15]) ).
cnf(t173347,plain,
meet(X1,meet(X3,meet(X2,X4))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t173346,t13]) ).
cnf(t173348,plain,
meet(X1,meet(X2,meet(X4,X3))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t173347,t15]) ).
cnf(t173349,plain,
meet(X1,meet(X2,meet(X3,X4))) = meet(meet(meet(X1,X2),meet(X3,X4)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t173348,t13]) ).
cnf(t173350,plain,
meet(X1,meet(X2,meet(X3,X4))) = meet(join(Y4,meet(X1,X2)),meet(meet(X1,X2),meet(X3,X4))),
inference(step,[status(thm)],[t173349,t13]) ).
cnf(t173351,plain,
meet(X1,meet(X2,meet(X3,X4))) = meet(meet(X3,X4),meet(join(Y4,meet(X1,X2)),meet(X1,X2))),
inference(step,[status(thm)],[t173350,t15]) ).
cnf(t173352,plain,
meet(X1,meet(X2,meet(X3,X4))) = meet(meet(X1,X2),meet(meet(X3,X4),join(Y4,meet(X1,X2)))),
inference(step,[status(thm)],[t173351,t15]) ).
cnf(t11724,plain,
meet(meet(X1,X2),meet(meet(X3,X4),join(Y4,meet(X1,X2)))) = meet(X1,meet(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t173352]) ).
cnf(t457,plain,
meet(X1,meet(join(X2,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t424]) ).
cnf(t173056,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t457,t13]) ).
cnf(t173057,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t173056,t15]) ).
cnf(t173058,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t173057,t15]) ).
cnf(t459,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t173058]) ).
cnf(t35,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(cp,[status(thm)],[t33,t10]) ).
cnf(t105,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t35]) ).
cnf(t108,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X2,meet(join(X3,meet(X1,X4)),join(X1,X3)))),
inference(cp,[status(thm)],[t105,t95]) ).
cnf(t173012,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X2,meet(join(X1,X3),join(X3,meet(X1,X4))))),
inference(step,[status(thm)],[t108,t13]) ).
cnf(t198,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X3,meet(X1,X4))))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t173012]) ).
cnf(t470,plain,
meet(join(X1,X2),meet(join(X2,meet(X1,X3)),X1)) = meet(join(X1,X2),meet(X1,join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3))))),
inference(cp,[status(thm)],[t459,t198]) ).
cnf(t173078,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(join(X1,X2),meet(X1,join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3))))),
inference(step,[status(thm)],[t470,t15]) ).
cnf(t173079,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,meet(join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3))),join(X1,X2))),
inference(step,[status(thm)],[t173078,t15]) ).
cnf(t173080,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t173079,t84]) ).
cnf(t173081,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t173080,t11]) ).
cnf(t818,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t173081]) ).
cnf(t840,plain,
meet(X1,join(X1,X2)) = meet(X1,join(join(X1,X2),meet(X1,join(X2,meet(X1,X3))))),
inference(cp,[status(thm)],[t402,t818]) ).
cnf(t173082,plain,
X1 = meet(X1,join(join(X1,X2),meet(X1,join(X2,meet(X1,X3))))),
inference(step,[status(thm)],[t840,t10]) ).
cnf(t854,plain,
meet(X1,join(join(X1,X2),meet(X1,join(X2,meet(X1,X3))))) = X1,
inference(orient,[status(thm)],[t173082]) ).
cnf(t4511,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(meet(X1,join(X2,meet(X1,X3))),join(X4,X1)),
inference(cp,[status(thm)],[t4492,t854]) ).
cnf(t173245,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(join(X4,X1),meet(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t4511,t13]) ).
cnf(t173246,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X2,meet(X1,X3)),join(X4,X1))),
inference(step,[status(thm)],[t173245,t15]) ).
cnf(t173247,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X4,X1),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t173246,t13]) ).
cnf(t173248,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X1,X4),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t173247,t45]) ).
cnf(t5473,plain,
meet(X1,meet(join(X1,X2),join(X3,meet(X1,X4)))) = meet(X1,join(X3,meet(X1,X4))),
inference(orient,[status(thm)],[t173248]) ).
cnf(t5530,plain,
meet(X1,join(X1,X2)) = meet(X1,join(join(X1,X2),meet(X1,join(X3,meet(X1,X4))))),
inference(cp,[status(thm)],[t402,t5473]) ).
cnf(t173249,plain,
X1 = meet(X1,join(join(X1,X2),meet(X1,join(X3,meet(X1,X4))))),
inference(step,[status(thm)],[t5530,t10]) ).
cnf(t5562,plain,
meet(X1,join(join(X1,X2),meet(X1,join(X3,meet(X1,X4))))) = X1,
inference(orient,[status(thm)],[t173249]) ).
cnf(t493,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,join(meet(X2,join(X3,meet(X1,X3))),meet(X1,meet(X3,X2)))),
inference(cp,[status(thm)],[t424,t459]) ).
cnf(t23776,plain,
meet(X1,join(meet(X1,meet(X2,X3)),meet(X3,join(X2,meet(X1,X2))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t493]) ).
cnf(t23932,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,join(meet(X1,X2),meet(join(X2,X3),join(X2,meet(X1,X2))))),
inference(cp,[status(thm)],[t23776,t10]) ).
cnf(t173466,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(X2,X3),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t23932,t10]) ).
cnf(t24344,plain,
meet(X1,join(meet(X1,X2),meet(join(X2,X3),join(X2,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t173466]) ).
cnf(t24705,plain,
join(X1,X2) = meet(join(X1,X2),join(join(join(X1,X2),X3),meet(join(X1,X2),X1))),
inference(cp,[status(thm)],[t5562,t24344]) ).
cnf(t173467,plain,
join(X1,X2) = meet(join(X1,X2),join(meet(join(X1,X2),X1),join(join(X1,X2),X3))),
inference(step,[status(thm)],[t24705,t45]) ).
cnf(t173468,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,join(meet(join(X1,X2),X1),join(X1,X2)))),
inference(step,[status(thm)],[t173467,t49]) ).
cnf(t173469,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,join(X2,join(meet(join(X1,X2),X1),X1)))),
inference(step,[status(thm)],[t173468,t49]) ).
cnf(t173470,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,join(X1,join(X2,meet(join(X1,X2),X1))))),
inference(step,[status(thm)],[t173469,t49]) ).
cnf(t173471,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(join(X2,meet(join(X1,X2),X1)),X3))),
inference(step,[status(thm)],[t173470,t49]) ).
cnf(t173472,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X3,join(X2,meet(join(X1,X2),X1))))),
inference(step,[status(thm)],[t173471,t45]) ).
cnf(t173473,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,join(meet(join(X1,X2),X1),X3)))),
inference(step,[status(thm)],[t173472,t49]) ).
cnf(t173474,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,join(X3,meet(join(X1,X2),X1))))),
inference(step,[status(thm)],[t173473,t45]) ).
cnf(t173475,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,join(X3,meet(X1,join(X1,X2)))))),
inference(step,[status(thm)],[t173474,t13]) ).
cnf(t173476,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,join(X3,X1)))),
inference(step,[status(thm)],[t173475,t10]) ).
cnf(t173477,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,join(X1,X3)))),
inference(step,[status(thm)],[t173476,t45]) ).
cnf(t173478,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X1,join(X3,X2)))),
inference(step,[status(thm)],[t173477,t49]) ).
cnf(t52,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t49,t11]) ).
cnf(t172973,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t52,t49]) ).
cnf(t172974,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t172973,t45]) ).
cnf(t76,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t172974]) ).
cnf(t173479,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X3,X2))),
inference(step,[status(thm)],[t173478,t76]) ).
cnf(t173480,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t173479,t45]) ).
cnf(t24772,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t173480]) ).
cnf(t24807,plain,
meet(X1,meet(X2,meet(join(X3,X4),join(X3,join(X4,Y4))))) = meet(meet(X1,X2),meet(join(X3,X4),join(Y5,meet(X1,X2)))),
inference(cp,[status(thm)],[t11724,t24772]) ).
cnf(t173485,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(Y5,meet(X1,X2)))),
inference(step,[status(thm)],[t24807,t24772]) ).
cnf(t25168,plain,
meet(meet(X1,X2),meet(join(X3,X4),join(Y4,meet(X1,X2)))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t173485]) ).
cnf(t25171,plain,
meet(X1,meet(X1,join(X2,X3))) = meet(X1,meet(join(X2,X3),join(X4,meet(X1,X1)))),
inference(cp,[status(thm)],[t25168,t9]) ).
cnf(t173486,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X4,meet(X1,X1)))),
inference(step,[status(thm)],[t25171,t67]) ).
cnf(t173487,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X4,X1))),
inference(step,[status(thm)],[t173486,t9]) ).
cnf(t173488,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,X4))),
inference(step,[status(thm)],[t173487,t45]) ).
cnf(t173489,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X4),join(X2,X3))),
inference(step,[status(thm)],[t173488,t13]) ).
cnf(t25670,plain,
meet(X1,meet(join(X1,X2),join(X3,X4))) = meet(X1,join(X3,X4)),
inference(orient,[status(thm)],[t173489]) ).
cnf(t5973,plain,
meet(X1,meet(X2,meet(meet(X1,X3),join(X3,X4)))) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,join(X2,Y5)))),
inference(cp,[status(thm)],[t5970,t2297]) ).
cnf(t173286,plain,
meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,join(X2,Y5)))),
inference(step,[status(thm)],[t5973,t2297]) ).
cnf(t7498,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,join(X3,Y4)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173286]) ).
cnf(t7637,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),meet(X1,join(X3,X4))),
inference(cp,[status(thm)],[t7498,t11]) ).
cnf(t173287,plain,
meet(X1,meet(X2,X3)) = meet(join(X3,X4),meet(meet(X1,meet(X2,X3)),X1)),
inference(step,[status(thm)],[t7637,t15]) ).
cnf(t173288,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(join(X3,X4),meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t173287,t15]) ).
cnf(t173289,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),meet(join(X3,X4),X1))),
inference(step,[status(thm)],[t173288,t15]) ).
cnf(t173290,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X1,meet(meet(X2,X3),join(X3,X4)))),
inference(step,[status(thm)],[t173289,t15]) ).
cnf(t173291,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X3,X4))),
inference(step,[status(thm)],[t173290,t67]) ).
cnf(t7745,plain,
meet(X1,meet(meet(X2,X3),join(X3,X4))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173291]) ).
cnf(t7749,plain,
meet(meet(X1,X2),meet(X1,X2)) = meet(meet(X1,X2),join(X2,X3)),
inference(cp,[status(thm)],[t7745,t67]) ).
cnf(t173294,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t7749,t9]) ).
cnf(t7893,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t173294]) ).
cnf(t7960,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(meet(X1,join(X2,X3)),join(join(X2,meet(X3,join(X1,X3))),X4)),
inference(cp,[status(thm)],[t7893,t105]) ).
cnf(t173830,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(join(X2,meet(X3,join(X1,X3))),X4)),
inference(step,[status(thm)],[t7960,t105]) ).
cnf(t173831,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X4,join(X2,meet(X3,join(X1,X3))))),
inference(step,[status(thm)],[t173830,t45]) ).
cnf(t173832,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,join(meet(X3,join(X1,X3)),X4))),
inference(step,[status(thm)],[t173831,t49]) ).
cnf(t173833,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,join(X4,meet(X3,join(X1,X3))))),
inference(step,[status(thm)],[t173832,t45]) ).
cnf(t92578,plain,
meet(meet(X1,join(X2,X3)),join(X2,join(X4,meet(X3,join(X1,X3))))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t173833]) ).
cnf(t92639,plain,
meet(join(X1,X2),join(X1,X2)) = meet(join(X1,X2),join(X1,join(X3,meet(X2,join(join(X1,X2),X2))))),
inference(cp,[status(thm)],[t92578,t9]) ).
cnf(t173834,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X3,meet(X2,join(join(X1,X2),X2))))),
inference(step,[status(thm)],[t92639,t9]) ).
cnf(t173835,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X3,meet(X2,join(X2,join(X1,X2)))))),
inference(step,[status(thm)],[t173834,t45]) ).
cnf(t173836,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X3,meet(X2,join(X1,join(X2,X2)))))),
inference(step,[status(thm)],[t173835,t49]) ).
cnf(t173837,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X3,meet(X2,join(X1,X2))))),
inference(step,[status(thm)],[t173836,t11]) ).
cnf(t92958,plain,
meet(join(X1,X2),join(X1,join(X3,meet(X2,join(X1,X2))))) = join(X1,X2),
inference(orient,[status(thm)],[t173837]) ).
cnf(t92978,plain,
join(X1,meet(X2,X3)) = meet(join(X1,meet(X2,X3)),join(X1,join(X4,meet(X2,X3)))),
inference(cp,[status(thm)],[t92958,t2081]) ).
cnf(t93599,plain,
meet(join(X1,meet(X2,X3)),join(X1,join(X4,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t92978]) ).
cnf(t93655,plain,
join(X1,meet(X2,X3)) = meet(join(X1,meet(X2,X3)),join(X1,X2)),
inference(cp,[status(thm)],[t93599,t12]) ).
cnf(t173838,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t93655,t13]) ).
cnf(t94014,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173838]) ).
cnf(t94030,plain,
join(X1,meet(join(X1,X2),X3)) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t94014,t76]) ).
cnf(t173875,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t94030,t13]) ).
cnf(t173876,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t173875,t13]) ).
cnf(t98706,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))) = join(X1,meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t173876]) ).
cnf(t98883,plain,
join(X1,X2) = join(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t12,t98706]) ).
cnf(t173877,plain,
join(X1,X2) = join(X1,join(meet(X3,join(X1,X2)),join(X1,X2))),
inference(step,[status(thm)],[t98883,t49]) ).
cnf(t173878,plain,
join(X1,X2) = join(X1,join(X2,join(meet(X3,join(X1,X2)),X1))),
inference(step,[status(thm)],[t173877,t49]) ).
cnf(t173879,plain,
join(X1,X2) = join(X1,join(X1,join(X2,meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t173878,t49]) ).
cnf(t173880,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t173879,t76]) ).
cnf(t99516,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t173880]) ).
cnf(t2779,plain,
meet(X1,join(X1,X2)) = meet(X1,meet(X1,join(X3,meet(join(X1,X2),join(X1,X4))))),
inference(cp,[status(thm)],[t2731,t10]) ).
cnf(t173173,plain,
X1 = meet(X1,meet(X1,join(X3,meet(join(X1,X2),join(X1,X4))))),
inference(step,[status(thm)],[t2779,t10]) ).
cnf(t173174,plain,
X1 = meet(X1,join(X3,meet(join(X1,X2),join(X1,X4)))),
inference(step,[status(thm)],[t173173,t67]) ).
cnf(t2841,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X1,X4)))) = X1,
inference(orient,[status(thm)],[t173174]) ).
cnf(t99558,plain,
join(X1,meet(join(X2,X3),join(X2,X4))) = join(X1,join(meet(join(X2,X3),join(X2,X4)),X2)),
inference(cp,[status(thm)],[t99516,t2841]) ).
cnf(t174067,plain,
join(X1,meet(join(X2,X3),join(X2,X4))) = join(X1,join(X2,meet(join(X2,X3),join(X2,X4)))),
inference(step,[status(thm)],[t99558,t45]) ).
cnf(t134080,plain,
join(X1,join(X2,meet(join(X2,X3),join(X2,X4)))) = join(X1,meet(join(X2,X3),join(X2,X4))),
inference(orient,[status(thm)],[t174067]) ).
cnf(t92968,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,meet(X2,join(X1,X2)))),
inference(cp,[status(thm)],[t92958,t76]) ).
cnf(t93282,plain,
meet(join(X1,X2),join(X1,meet(X2,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t92968]) ).
cnf(t173839,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(step,[status(thm)],[t93282,t94014]) ).
cnf(t94440,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(rw,[status(thm)],[t173839]) ).
cnf(t94898,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t94440]) ).
cnf(t99681,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,join(meet(X2,join(X1,X2)),meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t99516,t94898]) ).
cnf(t174003,plain,
join(X1,X2) = join(X1,join(meet(X2,join(X1,X2)),meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t99681,t94898]) ).
cnf(t118394,plain,
join(X1,join(meet(X2,join(X1,X2)),meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t174003]) ).
cnf(t93,plain,
meet(X1,meet(meet(X2,join(X1,X3)),X4)) = meet(X4,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t84]) ).
cnf(t172981,plain,
meet(X1,meet(X4,meet(X2,join(X1,X3)))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t93,t13]) ).
cnf(t172982,plain,
meet(X1,meet(X2,meet(join(X1,X3),X4))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t172981,t15]) ).
cnf(t172983,plain,
meet(X1,meet(X2,meet(X4,join(X1,X3)))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t172982,t13]) ).
cnf(t172984,plain,
meet(X1,meet(X2,meet(X4,join(X1,X3)))) = meet(X2,meet(X4,X1)),
inference(step,[status(thm)],[t172983,t15]) ).
cnf(t172985,plain,
meet(X1,meet(X2,meet(X4,join(X1,X3)))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t172984,t15]) ).
cnf(t115,plain,
meet(X1,meet(X2,meet(X3,join(X1,X4)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t172985]) ).
cnf(t25252,plain,
meet(X1,meet(meet(X2,meet(X3,join(X1,X4))),join(Y4,Y5))) = meet(meet(X1,meet(X2,X3)),meet(join(Y4,Y5),join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4))))))),
inference(cp,[status(thm)],[t25168,t115]) ).
cnf(t173709,plain,
meet(X1,meet(join(Y4,Y5),meet(X2,meet(X3,join(X1,X4))))) = meet(meet(X1,meet(X2,X3)),meet(join(Y4,Y5),join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4))))))),
inference(step,[status(thm)],[t25252,t13]) ).
cnf(t173710,plain,
meet(X1,meet(X2,meet(meet(X3,join(X1,X4)),join(Y4,Y5)))) = meet(meet(X1,meet(X2,X3)),meet(join(Y4,Y5),join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4))))))),
inference(step,[status(thm)],[t173709,t15]) ).
cnf(t173711,plain,
meet(X1,meet(X2,meet(join(Y4,Y5),meet(X3,join(X1,X4))))) = meet(meet(X1,meet(X2,X3)),meet(join(Y4,Y5),join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4))))))),
inference(step,[status(thm)],[t173710,t13]) ).
cnf(t173712,plain,
meet(X1,meet(X2,meet(join(X1,X4),meet(join(Y4,Y5),X3)))) = meet(meet(X1,meet(X2,X3)),meet(join(Y4,Y5),join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4))))))),
inference(step,[status(thm)],[t173711,t15]) ).
cnf(t173713,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(meet(X1,meet(X2,X3)),meet(join(Y4,Y5),join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4))))))),
inference(step,[status(thm)],[t173712,t15]) ).
cnf(t173714,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(join(Y4,Y5),meet(join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4))))),meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t173713,t15]) ).
cnf(t173715,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(join(Y4,Y5),meet(meet(X2,X3),meet(join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4))))),X1))),
inference(step,[status(thm)],[t173714,t15]) ).
cnf(t173716,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(join(Y4,Y5),meet(X1,meet(meet(X2,X3),join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4)))))))),
inference(step,[status(thm)],[t173715,t15]) ).
cnf(t173717,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(X1,meet(meet(meet(X2,X3),join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4)))))),join(Y4,Y5))),
inference(step,[status(thm)],[t173716,t15]) ).
cnf(t173718,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(X1,meet(join(Y4,Y5),meet(meet(X2,X3),join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4)))))))),
inference(step,[status(thm)],[t173717,t13]) ).
cnf(t173719,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(X1,meet(meet(X2,X3),meet(join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4))))),join(Y4,Y5)))),
inference(step,[status(thm)],[t173718,t15]) ).
cnf(t173720,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(X1,meet(meet(X2,X3),meet(join(Y4,Y5),join(Y6,meet(X1,meet(X2,meet(X3,join(X1,X4)))))))),
inference(step,[status(thm)],[t173719,t13]) ).
cnf(t173721,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(X1,meet(meet(X2,X3),meet(join(Y4,Y5),join(Y6,meet(X1,meet(X2,X3)))))),
inference(step,[status(thm)],[t173720,t115]) ).
cnf(t173722,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(X1,meet(meet(X2,X3),join(Y4,Y5))),
inference(step,[status(thm)],[t173721,t1770]) ).
cnf(t64387,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),join(Y4,Y5))))) = meet(X1,meet(meet(X2,X3),join(Y4,Y5))),
inference(orient,[status(thm)],[t173722]) ).
cnf(t25297,plain,
meet(meet(X1,X2),meet(join(X2,X3),join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(meet(X1,X2),join(X2,X3))))),
inference(cp,[status(thm)],[t25168,t7893]) ).
cnf(t173506,plain,
meet(meet(X1,X2),meet(join(X2,X3),join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(X1,X2)))),
inference(step,[status(thm)],[t25297,t7893]) ).
cnf(t173507,plain,
meet(meet(X1,X2),meet(join(X2,X3),join(X4,Y4))) = meet(X1,meet(X2,join(X4,Y4))),
inference(step,[status(thm)],[t173506,t25168]) ).
cnf(t27208,plain,
meet(meet(X1,X2),meet(join(X2,X3),join(X4,Y4))) = meet(X1,meet(X2,join(X4,Y4))),
inference(orient,[status(thm)],[t173507]) ).
cnf(t27360,plain,
meet(meet(X1,X2),meet(join(X2,X3),join(X4,Y4))) = meet(meet(X1,X2),meet(join(join(X2,X3),Y5),join(X4,Y4))),
inference(cp,[status(thm)],[t27208,t7893]) ).
cnf(t173608,plain,
meet(X1,meet(X2,join(X4,Y4))) = meet(meet(X1,X2),meet(join(join(X2,X3),Y5),join(X4,Y4))),
inference(step,[status(thm)],[t27360,t27208]) ).
cnf(t173609,plain,
meet(X1,meet(X2,join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(join(X2,X3),Y5))),
inference(step,[status(thm)],[t173608,t13]) ).
cnf(t173610,plain,
meet(X1,meet(X2,join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,join(X2,X3)))),
inference(step,[status(thm)],[t173609,t45]) ).
cnf(t173611,plain,
meet(X1,meet(X2,join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(X3,join(Y5,X2)))),
inference(step,[status(thm)],[t173610,t49]) ).
cnf(t173612,plain,
meet(X1,meet(X2,join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(X2,join(X3,Y5)))),
inference(step,[status(thm)],[t173611,t49]) ).
cnf(t42912,plain,
meet(meet(X1,X2),meet(join(X3,X4),join(X2,join(Y4,Y5)))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t173612]) ).
cnf(t64463,plain,
meet(X1,meet(meet(X2,meet(X3,X4)),join(X4,join(Y4,Y5)))) = meet(X1,meet(X2,meet(X3,meet(X4,join(X1,Y6))))),
inference(cp,[status(thm)],[t64387,t42912]) ).
cnf(t128,plain,
meet(X1,meet(meet(X2,meet(X3,join(X1,X4))),Y4)) = meet(Y4,meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t15,t115]) ).
cnf(t172994,plain,
meet(X1,meet(Y4,meet(X2,meet(X3,join(X1,X4))))) = meet(Y4,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t128,t13]) ).
cnf(t172995,plain,
meet(X1,meet(X2,meet(meet(X3,join(X1,X4)),Y4))) = meet(Y4,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t172994,t15]) ).
cnf(t172996,plain,
meet(X1,meet(X2,meet(Y4,meet(X3,join(X1,X4))))) = meet(Y4,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t172995,t13]) ).
cnf(t172997,plain,
meet(X1,meet(X2,meet(X3,meet(join(X1,X4),Y4)))) = meet(Y4,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t172996,t15]) ).
cnf(t172998,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X1,X4))))) = meet(Y4,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t172997,t13]) ).
cnf(t172999,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X1,X4))))) = meet(X1,meet(meet(X2,X3),Y4)),
inference(step,[status(thm)],[t172998,t15]) ).
cnf(t173000,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X1,X4))))) = meet(X1,meet(Y4,meet(X2,X3))),
inference(step,[status(thm)],[t172999,t13]) ).
cnf(t173001,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X1,X4))))) = meet(X1,meet(X3,meet(Y4,X2))),
inference(step,[status(thm)],[t173000,t15]) ).
cnf(t173002,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X1,X4))))) = meet(X1,meet(X2,meet(X3,Y4))),
inference(step,[status(thm)],[t173001,t15]) ).
cnf(t159,plain,
meet(X1,meet(X2,meet(X3,meet(X4,join(X1,Y4))))) = meet(X1,meet(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t173002]) ).
cnf(t173727,plain,
meet(X1,meet(meet(X2,meet(X3,X4)),join(X4,join(Y4,Y5)))) = meet(X1,meet(X2,meet(X3,X4))),
inference(step,[status(thm)],[t64463,t159]) ).
cnf(t67163,plain,
meet(X1,meet(meet(X2,meet(X3,X4)),join(X4,join(Y4,Y5)))) = meet(X1,meet(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t173727]) ).
cnf(t67166,plain,
meet(meet(X1,meet(X2,X3)),meet(X1,meet(X2,X3))) = meet(meet(X1,meet(X2,X3)),join(X3,join(X4,Y4))),
inference(cp,[status(thm)],[t67163,t67]) ).
cnf(t173728,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X3,join(X4,Y4))),
inference(step,[status(thm)],[t67166,t9]) ).
cnf(t67693,plain,
meet(meet(X1,meet(X2,X3)),join(X3,join(X4,Y4))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173728]) ).
cnf(t68037,plain,
meet(X1,meet(meet(X2,X3),join(X2,X4))) = meet(meet(X1,meet(X2,X3)),join(join(X2,X4),join(Y4,Y5))),
inference(cp,[status(thm)],[t67693,t2555]) ).
cnf(t173735,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(join(X2,X4),join(Y4,Y5))),
inference(step,[status(thm)],[t68037,t2555]) ).
cnf(t173736,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y5,join(join(X2,X4),Y4))),
inference(step,[status(thm)],[t173735,t49]) ).
cnf(t173737,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,join(Y5,join(X2,X4)))),
inference(step,[status(thm)],[t173736,t49]) ).
cnf(t173738,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,join(X4,join(Y5,X2)))),
inference(step,[status(thm)],[t173737,t49]) ).
cnf(t173739,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,join(X2,join(X4,Y5)))),
inference(step,[status(thm)],[t173738,t49]) ).
cnf(t173740,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X2,join(join(X4,Y5),Y4))),
inference(step,[status(thm)],[t173739,t49]) ).
cnf(t173741,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X2,join(Y4,join(X4,Y5)))),
inference(step,[status(thm)],[t173740,t45]) ).
cnf(t173742,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X2,join(X4,join(Y5,Y4)))),
inference(step,[status(thm)],[t173741,t49]) ).
cnf(t173743,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X2,join(X4,join(Y4,Y5)))),
inference(step,[status(thm)],[t173742,t45]) ).
cnf(t70501,plain,
meet(meet(X1,meet(X2,X3)),join(X2,join(X4,join(Y4,Y5)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173743]) ).
cnf(t103,plain,
join(X1,join(join(X2,meet(X1,X3)),X4)) = join(X4,join(X1,X2)),
inference(cp,[status(thm)],[t49,t95]) ).
cnf(t172986,plain,
join(X1,join(X4,join(X2,meet(X1,X3)))) = join(X4,join(X1,X2)),
inference(step,[status(thm)],[t103,t45]) ).
cnf(t172987,plain,
join(X1,join(X2,join(meet(X1,X3),X4))) = join(X4,join(X1,X2)),
inference(step,[status(thm)],[t172986,t49]) ).
cnf(t172988,plain,
join(X1,join(X2,join(X4,meet(X1,X3)))) = join(X4,join(X1,X2)),
inference(step,[status(thm)],[t172987,t45]) ).
cnf(t172989,plain,
join(X1,join(X2,join(X4,meet(X1,X3)))) = join(X2,join(X4,X1)),
inference(step,[status(thm)],[t172988,t49]) ).
cnf(t172990,plain,
join(X1,join(X2,join(X4,meet(X1,X3)))) = join(X1,join(X2,X4)),
inference(step,[status(thm)],[t172989,t49]) ).
cnf(t130,plain,
join(X1,join(X2,join(X3,meet(X1,X4)))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t172990]) ).
cnf(t70541,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X2,join(X4,Y4))),
inference(cp,[status(thm)],[t70501,t130]) ).
cnf(t70753,plain,
meet(meet(X1,meet(X2,X3)),join(X2,join(X4,Y4))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t70541]) ).
cnf(t11982,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,meet(X3,X4)))),
inference(cp,[status(thm)],[t12,t11724]) ).
cnf(t12099,plain,
join(meet(X1,X2),meet(X1,meet(X2,meet(X3,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t11982]) ).
cnf(t4665,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))) = meet(meet(X1,meet(X2,X3)),meet(meet(X1,meet(X2,X3)),join(join(X4,meet(X1,X2)),Y4))),
inference(cp,[status(thm)],[t2408,t4576]) ).
cnf(t173255,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),meet(meet(X1,meet(X2,X3)),join(join(X4,meet(X1,X2)),Y4))),
inference(step,[status(thm)],[t4665,t4576]) ).
cnf(t173256,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(join(X4,meet(X1,X2)),Y4)),
inference(step,[status(thm)],[t173255,t67]) ).
cnf(t173257,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t173256,t45]) ).
cnf(t173258,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,join(meet(X1,X2),Y4))),
inference(step,[status(thm)],[t173257,t49]) ).
cnf(t173259,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,join(Y4,meet(X1,X2)))),
inference(step,[status(thm)],[t173258,t45]) ).
cnf(t5815,plain,
meet(meet(X1,meet(X2,X3)),join(X4,join(Y4,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173259]) ).
cnf(t5816,plain,
meet(X1,meet(X2,X3)) = meet(join(X4,join(Y4,meet(X1,X2))),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t5815,t13]) ).
cnf(t173282,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X3),meet(join(X4,join(Y4,meet(X1,X2))),X1)),
inference(step,[status(thm)],[t5816,t15]) ).
cnf(t173283,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X4,join(Y4,meet(X1,X2))))),
inference(step,[status(thm)],[t173282,t15]) ).
cnf(t6928,plain,
meet(X1,meet(meet(X2,X3),join(X4,join(Y4,meet(X1,X2))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173283]) ).
cnf(t6935,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(join(X4,join(Y4,meet(X1,X2))),meet(X2,X3))),
inference(cp,[status(thm)],[t6928,t13]) ).
cnf(t173310,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X3,meet(join(X4,join(Y4,meet(X1,X2))),X2))),
inference(step,[status(thm)],[t6935,t15]) ).
cnf(t173311,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))),
inference(step,[status(thm)],[t173310,t15]) ).
cnf(t9749,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173311]) ).
cnf(t12171,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t12099,t9749]) ).
cnf(t12294,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t12171]) ).
cnf(t25247,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(Y4,meet(X1,meet(X1,X2))))),
inference(cp,[status(thm)],[t25168,t67]) ).
cnf(t173491,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(Y4,meet(X1,X2)))),
inference(step,[status(thm)],[t25247,t67]) ).
cnf(t173492,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(X1,meet(X2,join(X3,X4))),
inference(step,[status(thm)],[t173491,t25168]) ).
cnf(t26263,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t173492]) ).
cnf(t26480,plain,
meet(X1,meet(meet(X2,X3),join(X4,Y4))) = meet(X1,meet(meet(X2,meet(X3,X1)),join(X4,Y4))),
inference(cp,[status(thm)],[t26263,t15]) ).
cnf(t173526,plain,
meet(X1,meet(meet(X2,X3),join(X4,Y4))) = meet(X1,meet(join(X4,Y4),meet(X2,meet(X3,X1)))),
inference(step,[status(thm)],[t26480,t13]) ).
cnf(t173527,plain,
meet(X1,meet(meet(X2,X3),join(X4,Y4))) = meet(X1,meet(meet(X3,X1),meet(join(X4,Y4),X2))),
inference(step,[status(thm)],[t173526,t15]) ).
cnf(t173528,plain,
meet(X1,meet(meet(X2,X3),join(X4,Y4))) = meet(X1,meet(X2,meet(meet(X3,X1),join(X4,Y4)))),
inference(step,[status(thm)],[t173527,t15]) ).
cnf(t173529,plain,
meet(X1,meet(meet(X2,X3),join(X4,Y4))) = meet(X1,meet(X2,meet(meet(X1,X3),join(X4,Y4)))),
inference(step,[status(thm)],[t173528,t13]) ).
cnf(t29416,plain,
meet(X1,meet(X2,meet(meet(X1,X3),join(X4,Y4)))) = meet(X1,meet(meet(X2,X3),join(X4,Y4))),
inference(orient,[status(thm)],[t173529]) ).
cnf(t29715,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(meet(X2,X3),join(X4,Y4)))),
inference(cp,[status(thm)],[t12294,t29416]) ).
cnf(t29835,plain,
join(meet(X1,X2),meet(X1,meet(meet(X2,X3),join(X4,Y4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t29715]) ).
cnf(t29964,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(meet(X3,meet(X4,X2)),join(Y4,Y5)))),
inference(cp,[status(thm)],[t29835,t15]) ).
cnf(t173671,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(join(Y4,Y5),meet(X3,meet(X4,X2))))),
inference(step,[status(thm)],[t29964,t13]) ).
cnf(t173672,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(meet(X4,X2),meet(join(Y4,Y5),X3)))),
inference(step,[status(thm)],[t173671,t15]) ).
cnf(t173673,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X3,meet(meet(X4,X2),join(Y4,Y5))))),
inference(step,[status(thm)],[t173672,t15]) ).
cnf(t173674,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X3,meet(meet(X2,X4),join(Y4,Y5))))),
inference(step,[status(thm)],[t173673,t13]) ).
cnf(t57856,plain,
join(meet(X1,X2),meet(X1,meet(X3,meet(meet(X2,X4),join(Y4,Y5))))) = meet(X1,X2),
inference(orient,[status(thm)],[t173674]) ).
cnf(t70806,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X2,meet(X4,Y4))),
inference(cp,[status(thm)],[t70753,t57856]) ).
cnf(t71000,plain,
meet(meet(X1,meet(X2,X3)),join(X2,meet(X4,Y4))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t70806]) ).
cnf(t118530,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(meet(X2,X3),join(X1,meet(X2,X3))),meet(X4,meet(X1,Y4)))),
inference(cp,[status(thm)],[t118394,t71000]) ).
cnf(t2579,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,X3)))) = meet(X1,join(X2,meet(X3,X4))),
inference(cp,[status(thm)],[t33,t2555]) ).
cnf(t2603,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,X3)))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t2579]) ).
cnf(t2607,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(join(X1,X3),meet(X3,X4)))),
inference(cp,[status(thm)],[t2603,t13]) ).
cnf(t173169,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X4,meet(join(X1,X3),X3)))),
inference(step,[status(thm)],[t2607,t15]) ).
cnf(t173170,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X3,meet(X4,join(X1,X3))))),
inference(step,[status(thm)],[t173169,t15]) ).
cnf(t2661,plain,
meet(X1,join(X2,meet(X3,meet(X4,join(X1,X3))))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t173170]) ).
cnf(t94021,plain,
join(X1,meet(X2,meet(X3,join(join(X1,X2),X2)))) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t94014,t2661]) ).
cnf(t173846,plain,
join(X1,meet(X2,meet(X3,join(X2,join(X1,X2))))) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t94021,t45]) ).
cnf(t173847,plain,
join(X1,meet(X2,meet(X3,join(X1,join(X2,X2))))) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t173846,t49]) ).
cnf(t173848,plain,
join(X1,meet(X2,meet(X3,join(X1,X2)))) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t173847,t11]) ).
cnf(t173849,plain,
join(X1,meet(X2,meet(X3,join(X1,X2)))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t173848,t94014]) ).
cnf(t95581,plain,
join(X1,meet(X2,meet(X3,join(X1,X2)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173849]) ).
cnf(t25301,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(meet(X1,X2),join(X1,X3))))),
inference(cp,[status(thm)],[t25168,t2555]) ).
cnf(t173508,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(X1,X2)))),
inference(step,[status(thm)],[t25301,t2555]) ).
cnf(t173509,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(X4,Y4))) = meet(X1,meet(X2,join(X4,Y4))),
inference(step,[status(thm)],[t173508,t25168]) ).
cnf(t27591,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(X4,Y4))) = meet(X1,meet(X2,join(X4,Y4))),
inference(orient,[status(thm)],[t173509]) ).
cnf(t27802,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),meet(join(Y4,join(Y5,X1)),join(X3,X4))),
inference(cp,[status(thm)],[t27591,t49]) ).
cnf(t173613,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(Y4,join(Y5,X1)))),
inference(step,[status(thm)],[t27802,t13]) ).
cnf(t173614,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(X1,join(Y4,Y5)))),
inference(step,[status(thm)],[t173613,t49]) ).
cnf(t43353,plain,
meet(meet(X1,X2),meet(join(X3,X4),join(X1,join(Y4,Y5)))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t173614]) ).
cnf(t43590,plain,
meet(X1,meet(X2,join(X3,X4))) = meet(meet(X1,X2),meet(join(X3,X4),join(X1,meet(Y4,Y5)))),
inference(cp,[status(thm)],[t43353,t12294]) ).
cnf(t49699,plain,
meet(meet(X1,X2),meet(join(X3,X4),join(X1,meet(Y4,Y5)))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t43590]) ).
cnf(t95592,plain,
join(X1,meet(meet(X1,X2),join(X3,X4))) = join(X1,meet(X1,meet(X2,join(X3,X4)))),
inference(cp,[status(thm)],[t95581,t49699]) ).
cnf(t173850,plain,
join(X1,meet(meet(X1,X2),join(X3,X4))) = X1,
inference(step,[status(thm)],[t95592,t12]) ).
cnf(t95792,plain,
join(X1,meet(meet(X1,X2),join(X3,X4))) = X1,
inference(orient,[status(thm)],[t173850]) ).
cnf(t95814,plain,
join(X1,X2) = join(join(X1,X2),meet(join(X1,meet(X2,X3)),join(X4,Y4))),
inference(cp,[status(thm)],[t95792,t94014]) ).
cnf(t173969,plain,
join(X1,X2) = join(join(X1,X2),meet(join(X4,Y4),join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t95814,t13]) ).
cnf(t111988,plain,
join(join(X1,X2),meet(join(X3,X4),join(X1,meet(X2,Y4)))) = join(X1,X2),
inference(orient,[status(thm)],[t173969]) ).
cnf(t112086,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,meet(X2,X4)))),
inference(cp,[status(thm)],[t111988,t11]) ).
cnf(t112420,plain,
join(join(X1,X2),meet(X3,join(X1,meet(X2,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t112086]) ).
cnf(t29754,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,meet(meet(X2,X3),join(X4,Y4))))),
inference(cp,[status(thm)],[t402,t29416]) ).
cnf(t30100,plain,
meet(X1,join(X2,meet(X1,meet(meet(X2,X3),join(X4,Y4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t29754]) ).
cnf(t30110,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),join(X3,meet(X1,meet(X2,meet(X3,X4))))),
inference(cp,[status(thm)],[t30100,t11724]) ).
cnf(t173538,plain,
meet(X3,meet(X1,X2)) = meet(meet(X1,X2),join(X3,meet(X1,meet(X2,meet(X3,X4))))),
inference(step,[status(thm)],[t30110,t13]) ).
cnf(t173539,plain,
meet(X2,meet(X3,X1)) = meet(meet(X1,X2),join(X3,meet(X1,meet(X2,meet(X3,X4))))),
inference(step,[status(thm)],[t173538,t15]) ).
cnf(t173540,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(X3,meet(X1,meet(X2,meet(X3,X4))))),
inference(step,[status(thm)],[t173539,t15]) ).
cnf(t31100,plain,
meet(meet(X1,X2),join(X3,meet(X1,meet(X2,meet(X3,X4))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173540]) ).
cnf(t31437,plain,
meet(X1,meet(X2,X3)) = meet(X1,join(meet(X2,X3),meet(X1,meet(X2,meet(X3,X4))))),
inference(cp,[status(thm)],[t402,t31100]) ).
cnf(t32257,plain,
meet(X1,join(meet(X2,X3),meet(X1,meet(X2,meet(X3,X4))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t31437]) ).
cnf(t25248,plain,
meet(X1,meet(meet(X2,join(X1,X3)),join(X4,Y4))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(X1,meet(X2,join(X1,X3)))))),
inference(cp,[status(thm)],[t25168,t84]) ).
cnf(t173501,plain,
meet(X1,meet(join(X4,Y4),meet(X2,join(X1,X3)))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(X1,meet(X2,join(X1,X3)))))),
inference(step,[status(thm)],[t25248,t13]) ).
cnf(t173502,plain,
meet(X1,meet(join(X1,X3),meet(join(X4,Y4),X2))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(X1,meet(X2,join(X1,X3)))))),
inference(step,[status(thm)],[t173501,t15]) ).
cnf(t173503,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(X4,Y4)))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(X1,meet(X2,join(X1,X3)))))),
inference(step,[status(thm)],[t173502,t15]) ).
cnf(t173504,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(X4,Y4)))) = meet(meet(X1,X2),meet(join(X4,Y4),join(Y5,meet(X1,X2)))),
inference(step,[status(thm)],[t173503,t84]) ).
cnf(t173505,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(X4,Y4)))) = meet(X1,meet(X2,join(X4,Y4))),
inference(step,[status(thm)],[t173504,t25168]) ).
cnf(t27029,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(X4,Y4)))) = meet(X1,meet(X2,join(X4,Y4))),
inference(orient,[status(thm)],[t173505]) ).
cnf(t32369,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,meet(X2,join(X4,Y4))))),
inference(cp,[status(thm)],[t32257,t27029]) ).
cnf(t173679,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,meet(X2,join(X4,Y4))))),
inference(step,[status(thm)],[t32369,t84]) ).
cnf(t58982,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X1,meet(X2,join(X4,Y4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t173679]) ).
cnf(t59046,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,meet(X4,X2)))),
inference(cp,[status(thm)],[t58982,t459]) ).
cnf(t173680,plain,
meet(X1,X2) = meet(X1,join(meet(X1,meet(X4,X2)),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t59046,t45]) ).
cnf(t173681,plain,
meet(X1,X2) = meet(X1,join(meet(X1,meet(X2,X4)),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t173680,t13]) ).
cnf(t59440,plain,
meet(X1,join(meet(X1,meet(X2,X3)),meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t173681]) ).
cnf(t112501,plain,
join(meet(X1,meet(X2,X3)),X2) = join(join(meet(X1,meet(X2,X3)),X2),meet(X1,X2)),
inference(cp,[status(thm)],[t112420,t59440]) ).
cnf(t173983,plain,
join(X2,meet(X1,meet(X2,X3))) = join(join(meet(X1,meet(X2,X3)),X2),meet(X1,X2)),
inference(step,[status(thm)],[t112501,t45]) ).
cnf(t173984,plain,
join(X2,meet(X1,meet(X2,X3))) = join(meet(X1,X2),join(meet(X1,meet(X2,X3)),X2)),
inference(step,[status(thm)],[t173983,t45]) ).
cnf(t173985,plain,
join(X2,meet(X1,meet(X2,X3))) = join(X2,join(meet(X1,X2),meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t173984,t49]) ).
cnf(t173986,plain,
join(X2,meet(X1,meet(X2,X3))) = join(X2,meet(X1,X2)),
inference(step,[status(thm)],[t173985,t12294]) ).
cnf(t115774,plain,
join(X1,meet(X2,meet(X1,X3))) = join(X1,meet(X2,X1)),
inference(orient,[status(thm)],[t173986]) ).
cnf(t115946,plain,
join(meet(X1,meet(X2,X3)),join(X4,X2)) = join(X4,join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t49,t115774]) ).
cnf(t173987,plain,
join(X2,join(meet(X1,meet(X2,X3)),X4)) = join(X4,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t115946,t49]) ).
cnf(t173988,plain,
join(X2,join(X4,meet(X1,meet(X2,X3)))) = join(X4,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t173987,t45]) ).
cnf(t173989,plain,
join(X2,join(X4,meet(X1,meet(X2,X3)))) = join(X2,join(meet(X1,X2),X4)),
inference(step,[status(thm)],[t173988,t49]) ).
cnf(t173990,plain,
join(X2,join(X4,meet(X1,meet(X2,X3)))) = join(X2,join(X4,meet(X1,X2))),
inference(step,[status(thm)],[t173989,t45]) ).
cnf(t115947,plain,
join(X1,join(X2,meet(X3,meet(X1,X4)))) = join(X1,join(X2,meet(X3,X1))),
inference(orient,[status(thm)],[t173990]) ).
cnf(t174004,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(meet(X2,X3),join(X1,meet(X2,X3))),meet(X4,X1))),
inference(step,[status(thm)],[t118530,t115947]) ).
cnf(t174005,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X4,X1),meet(meet(X2,X3),join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t174004,t45]) ).
cnf(t95094,plain,
join(X1,join(meet(X2,join(X1,X2)),X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t49,t94898]) ).
cnf(t173841,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X3,join(X1,X2)),
inference(step,[status(thm)],[t95094,t45]) ).
cnf(t173842,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X2,join(X3,X1)),
inference(step,[status(thm)],[t173841,t49]) ).
cnf(t173843,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t173842,t49]) ).
cnf(t95096,plain,
join(X1,join(X2,meet(X3,join(X1,X3)))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t173843]) ).
cnf(t174006,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X4,X1))),
inference(step,[status(thm)],[t174005,t95096]) ).
cnf(t174007,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X1,X4))),
inference(step,[status(thm)],[t174006,t13]) ).
cnf(t174008,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X1,X4),meet(X2,X3))),
inference(step,[status(thm)],[t174007,t45]) ).
cnf(t118761,plain,
join(X1,join(meet(X1,X2),meet(X3,X4))) = join(X1,meet(X3,X4)),
inference(orient,[status(thm)],[t174008]) ).
cnf(t118935,plain,
join(X1,join(join(meet(X1,X2),meet(X3,X4)),Y4)) = join(Y4,join(X1,meet(X3,X4))),
inference(cp,[status(thm)],[t49,t118761]) ).
cnf(t174017,plain,
join(X1,join(Y4,join(meet(X1,X2),meet(X3,X4)))) = join(Y4,join(X1,meet(X3,X4))),
inference(step,[status(thm)],[t118935,t45]) ).
cnf(t174018,plain,
join(X1,join(Y4,join(meet(X1,X2),meet(X3,X4)))) = join(X1,join(meet(X3,X4),Y4)),
inference(step,[status(thm)],[t174017,t49]) ).
cnf(t174019,plain,
join(X1,join(Y4,join(meet(X1,X2),meet(X3,X4)))) = join(X1,join(Y4,meet(X3,X4))),
inference(step,[status(thm)],[t174018,t45]) ).
cnf(t121820,plain,
join(X1,join(X2,join(meet(X1,X3),meet(X4,Y4)))) = join(X1,join(X2,meet(X4,Y4))),
inference(orient,[status(thm)],[t174019]) ).
cnf(t121825,plain,
join(X1,join(X2,meet(X3,join(X2,meet(X1,X4))))) = join(X1,join(X2,meet(X1,X4))),
inference(cp,[status(thm)],[t121820,t99516]) ).
cnf(t174020,plain,
join(X1,join(X2,meet(X3,join(X2,meet(X1,X4))))) = join(X1,X2),
inference(step,[status(thm)],[t121825,t95]) ).
cnf(t122075,plain,
join(X1,join(X2,meet(X3,join(X2,meet(X1,X4))))) = join(X1,X2),
inference(orient,[status(thm)],[t174020]) ).
cnf(t134081,plain,
join(X1,meet(join(X2,X3),join(X2,meet(X1,X4)))) = join(X1,X2),
inference(cp,[status(thm)],[t134080,t122075]) ).
cnf(t134228,plain,
join(X1,meet(join(X2,X3),join(X2,meet(X1,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t134081]) ).
cnf(t134236,plain,
join(X1,X2) = join(X1,meet(join(X2,X3),join(X2,X1))),
inference(cp,[status(thm)],[t134228,t105]) ).
cnf(t174068,plain,
join(X1,X2) = join(X1,meet(join(X2,X1),join(X2,X3))),
inference(step,[status(thm)],[t134236,t13]) ).
cnf(t174069,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t174068,t45]) ).
cnf(t134649,plain,
join(X1,meet(join(X1,X2),join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t174069]) ).
cnf(t2609,plain,
meet(X1,join(X2,meet(X3,meet(X4,Y4)))) = meet(X1,join(X2,meet(meet(X4,meet(Y4,X3)),join(X1,X3)))),
inference(cp,[status(thm)],[t2603,t15]) ).
cnf(t173449,plain,
meet(X1,join(X2,meet(X3,meet(X4,Y4)))) = meet(X1,join(X2,meet(join(X1,X3),meet(X4,meet(Y4,X3))))),
inference(step,[status(thm)],[t2609,t13]) ).
cnf(t173450,plain,
meet(X1,join(X2,meet(X3,meet(X4,Y4)))) = meet(X1,join(X2,meet(meet(Y4,X3),meet(join(X1,X3),X4)))),
inference(step,[status(thm)],[t173449,t15]) ).
cnf(t173451,plain,
meet(X1,join(X2,meet(X3,meet(X4,Y4)))) = meet(X1,join(X2,meet(X4,meet(meet(Y4,X3),join(X1,X3))))),
inference(step,[status(thm)],[t173450,t15]) ).
cnf(t173452,plain,
meet(X1,join(X2,meet(X3,meet(X4,Y4)))) = meet(X1,join(X2,meet(X4,meet(meet(X3,Y4),join(X1,X3))))),
inference(step,[status(thm)],[t173451,t13]) ).
cnf(t22501,plain,
meet(X1,join(X2,meet(X3,meet(meet(X4,Y4),join(X1,X4))))) = meet(X1,join(X2,meet(X4,meet(X3,Y4)))),
inference(orient,[status(thm)],[t173452]) ).
cnf(t22538,plain,
meet(X1,join(X2,meet(X3,meet(X4,Y4)))) = meet(X1,join(X2,meet(X4,meet(join(X1,X3),meet(X3,Y4))))),
inference(cp,[status(thm)],[t22501,t13]) ).
cnf(t173462,plain,
meet(X1,join(X2,meet(X3,meet(X4,Y4)))) = meet(X1,join(X2,meet(X4,meet(Y4,meet(join(X1,X3),X3))))),
inference(step,[status(thm)],[t22538,t15]) ).
cnf(t173463,plain,
meet(X1,join(X2,meet(X3,meet(X4,Y4)))) = meet(X1,join(X2,meet(X4,meet(X3,meet(Y4,join(X1,X3)))))),
inference(step,[status(thm)],[t173462,t15]) ).
cnf(t173464,plain,
meet(X1,join(X2,meet(X3,meet(X4,Y4)))) = meet(X1,join(X2,meet(X3,meet(meet(Y4,join(X1,X3)),X4)))),
inference(step,[status(thm)],[t173463,t15]) ).
cnf(t173465,plain,
meet(X1,join(X2,meet(X3,meet(X4,Y4)))) = meet(X1,join(X2,meet(X3,meet(X4,meet(Y4,join(X1,X3)))))),
inference(step,[status(thm)],[t173464,t13]) ).
cnf(t23592,plain,
meet(X1,join(X2,meet(X3,meet(X4,meet(Y4,join(X1,X3)))))) = meet(X1,join(X2,meet(X3,meet(X4,Y4)))),
inference(orient,[status(thm)],[t173465]) ).
cnf(t31102,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(X3,meet(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t31100,t23592]) ).
cnf(t31579,plain,
meet(meet(X1,X2),join(X3,meet(X1,meet(X2,X3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t31102]) ).
cnf(t31864,plain,
meet(X1,meet(X2,meet(X2,X3))) = meet(meet(X1,X2),join(meet(X2,X3),meet(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t31579,t67]) ).
cnf(t173542,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X2,X3),meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t31864,t67]) ).
cnf(t32573,plain,
meet(meet(X1,X2),join(meet(X2,X3),meet(X1,meet(X2,X3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173542]) ).
cnf(t95638,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)],[t95581,t94014]) ).
cnf(t173851,plain,
join(X1,meet(meet(X2,X3),join(X1,X2))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t95638,t94898]) ).
cnf(t96181,plain,
join(X1,meet(meet(X2,X3),join(X1,X2))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t173851]) ).
cnf(t96190,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(meet(X3,meet(X4,X2)),join(X1,X2))),
inference(cp,[status(thm)],[t96181,t15]) ).
cnf(t173917,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(join(X1,X2),meet(X3,meet(X4,X2)))),
inference(step,[status(thm)],[t96190,t13]) ).
cnf(t173918,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(meet(X4,X2),meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t173917,t15]) ).
cnf(t173919,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(X3,meet(meet(X4,X2),join(X1,X2)))),
inference(step,[status(thm)],[t173918,t15]) ).
cnf(t173920,plain,
join(X1,meet(X2,meet(X3,X4))) = join(X1,meet(X3,meet(meet(X2,X4),join(X1,X2)))),
inference(step,[status(thm)],[t173919,t13]) ).
cnf(t102946,plain,
join(X1,meet(X2,meet(meet(X3,X4),join(X1,X3)))) = join(X1,meet(X3,meet(X2,X4))),
inference(orient,[status(thm)],[t173920]) ).
cnf(t103288,plain,
join(X1,meet(X2,meet(meet(X3,X4),join(X1,X3)))) = meet(join(X1,X2),join(X1,meet(X3,meet(X2,X4)))),
inference(cp,[status(thm)],[t94014,t102946]) ).
cnf(t173930,plain,
join(X1,meet(X3,meet(X2,X4))) = meet(join(X1,X2),join(X1,meet(X3,meet(X2,X4)))),
inference(step,[status(thm)],[t103288,t102946]) ).
cnf(t104823,plain,
meet(join(X1,X2),join(X1,meet(X3,meet(X2,X4)))) = join(X1,meet(X3,meet(X2,X4))),
inference(orient,[status(thm)],[t173930]) ).
cnf(t104874,plain,
join(X1,meet(X2,meet(X3,join(X1,X2)))) = meet(join(X1,X3),join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t104823,t95581]) ).
cnf(t173931,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X3),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t104874,t95581]) ).
cnf(t105431,plain,
meet(join(X1,X2),join(X1,meet(X3,X2))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t173931]) ).
cnf(t105813,plain,
meet(X1,meet(join(X2,X3),join(X2,meet(X4,X3)))) = meet(meet(X1,join(X2,X3)),join(meet(join(X2,X3),join(X2,meet(X4,X3))),meet(X1,join(X2,meet(X4,X3))))),
inference(cp,[status(thm)],[t32573,t105431]) ).
cnf(t173942,plain,
meet(X1,join(X2,meet(X4,X3))) = meet(meet(X1,join(X2,X3)),join(meet(join(X2,X3),join(X2,meet(X4,X3))),meet(X1,join(X2,meet(X4,X3))))),
inference(step,[status(thm)],[t105813,t105431]) ).
cnf(t173943,plain,
meet(X1,join(X2,meet(X4,X3))) = meet(meet(X1,join(X2,X3)),join(join(X2,meet(X4,X3)),meet(X1,join(X2,meet(X4,X3))))),
inference(step,[status(thm)],[t173942,t105431]) ).
cnf(t7947,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(cp,[status(thm)],[t7893,t84]) ).
cnf(t173295,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(step,[status(thm)],[t7947,t84]) ).
cnf(t173296,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t173295,t45]) ).
cnf(t8056,plain,
meet(meet(X1,X2),join(X3,meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t173296]) ).
cnf(t8163,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,meet(X2,X3))),
inference(cp,[status(thm)],[t8056,t2081]) ).
cnf(t8246,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X2,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t8163]) ).
cnf(t24790,plain,
meet(X1,meet(join(X2,X3),join(X2,join(X3,X4)))) = meet(meet(X1,join(X2,X3)),join(Y4,meet(join(X2,X3),join(X2,join(X3,X4))))),
inference(cp,[status(thm)],[t8246,t24772]) ).
cnf(t173481,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,meet(join(X2,X3),join(X2,join(X3,X4))))),
inference(step,[status(thm)],[t24790,t24772]) ).
cnf(t173482,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,join(X2,X3))),
inference(step,[status(thm)],[t173481,t24772]) ).
cnf(t173483,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X3,join(Y4,X2))),
inference(step,[status(thm)],[t173482,t49]) ).
cnf(t173484,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,join(X3,Y4))),
inference(step,[status(thm)],[t173483,t49]) ).
cnf(t24958,plain,
meet(meet(X1,join(X2,X3)),join(X2,join(X3,X4))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t173484]) ).
cnf(t99597,plain,
join(X1,join(X2,X3)) = join(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(cp,[status(thm)],[t99516,t24958]) ).
cnf(t100459,plain,
join(X1,join(join(X2,X3),meet(X4,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t99597]) ).
cnf(t100461,plain,
join(join(X1,X2),join(X1,X2)) = join(join(X1,X2),meet(X3,join(join(X1,X2),X1))),
inference(cp,[status(thm)],[t100459,t76]) ).
cnf(t173883,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(join(X1,X2),X1))),
inference(step,[status(thm)],[t100461,t11]) ).
cnf(t173884,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,join(X1,X2)))),
inference(step,[status(thm)],[t173883,t45]) ).
cnf(t173885,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t173884,t76]) ).
cnf(t100759,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t173885]) ).
cnf(t173944,plain,
meet(X1,join(X2,meet(X4,X3))) = meet(meet(X1,join(X2,X3)),join(X2,meet(X4,X3))),
inference(step,[status(thm)],[t173943,t100759]) ).
cnf(t109109,plain,
meet(meet(X1,join(X2,X3)),join(X2,meet(X4,X3))) = meet(X1,join(X2,meet(X4,X3))),
inference(orient,[status(thm)],[t173944]) ).
cnf(t109157,plain,
meet(X1,join(meet(X1,X2),meet(X3,meet(X2,join(X1,X4))))) = meet(meet(X1,X2),join(meet(X1,X2),meet(X3,meet(X2,join(X1,X4))))),
inference(cp,[status(thm)],[t109109,t506]) ).
cnf(t174031,plain,
meet(X1,join(meet(X1,X2),meet(X2,meet(join(X1,X4),X3)))) = meet(meet(X1,X2),join(meet(X1,X2),meet(X3,meet(X2,join(X1,X4))))),
inference(step,[status(thm)],[t109157,t15]) ).
cnf(t174032,plain,
meet(X1,join(meet(X1,X2),meet(X2,meet(X3,join(X1,X4))))) = meet(meet(X1,X2),join(meet(X1,X2),meet(X3,meet(X2,join(X1,X4))))),
inference(step,[status(thm)],[t174031,t13]) ).
cnf(t174033,plain,
meet(X1,join(meet(X1,X2),meet(X2,meet(X3,join(X1,X4))))) = meet(X1,X2),
inference(step,[status(thm)],[t174032,t10]) ).
cnf(t124612,plain,
meet(X1,join(meet(X1,X2),meet(X2,meet(X3,join(X1,X4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t174033]) ).
cnf(t8007,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,X4)))) = meet(X1,join(X2,meet(X3,X4))),
inference(cp,[status(thm)],[t33,t7893]) ).
cnf(t8383,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,X4)))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t8007]) ).
cnf(t8387,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(join(X1,X4),meet(X3,X4)))),
inference(cp,[status(thm)],[t8383,t13]) ).
cnf(t173298,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X4,meet(join(X1,X4),X3)))),
inference(step,[status(thm)],[t8387,t15]) ).
cnf(t173299,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X3,meet(X4,join(X1,X4))))),
inference(step,[status(thm)],[t173298,t15]) ).
cnf(t8630,plain,
meet(X1,join(X2,meet(X3,meet(X4,join(X1,X4))))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t173299]) ).
cnf(t124613,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(cp,[status(thm)],[t124612,t8630]) ).
cnf(t125268,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t124613]) ).
cnf(t125618,plain,
meet(X1,join(meet(join(X1,X2),X3),meet(X3,X4))) = meet(X1,meet(join(X1,X2),X3)),
inference(cp,[status(thm)],[t25670,t125268]) ).
cnf(t174037,plain,
meet(X1,join(meet(X3,X4),meet(join(X1,X2),X3))) = meet(X1,meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t125618,t45]) ).
cnf(t174038,plain,
meet(X1,join(meet(X3,X4),meet(X3,join(X1,X2)))) = meet(X1,meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t174037,t13]) ).
cnf(t174039,plain,
meet(X1,join(meet(X3,X4),meet(X3,join(X1,X2)))) = meet(X1,meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t174038,t13]) ).
cnf(t174040,plain,
meet(X1,join(meet(X3,X4),meet(X3,join(X1,X2)))) = meet(X1,X3),
inference(step,[status(thm)],[t174039,t84]) ).
cnf(t126689,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t174040]) ).
cnf(t134659,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X1,meet(X2,X3)),X2)),
inference(cp,[status(thm)],[t134649,t126689]) ).
cnf(t174070,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t134659,t13]) ).
cnf(t134992,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t174070]) ).
cnf(t135013,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)],[t134992,t102946]) ).
cnf(t174086,plain,
join(X1,meet(X3,meet(X2,X4))) = join(X1,meet(X2,join(X1,meet(X3,meet(X2,X4))))),
inference(step,[status(thm)],[t135013,t102946]) ).
cnf(t139049,plain,
join(X1,meet(X2,join(X1,meet(X3,meet(X2,X4))))) = join(X1,meet(X3,meet(X2,X4))),
inference(orient,[status(thm)],[t174086]) ).
cnf(t8449,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X4,Y4)))) = meet(X1,join(X2,meet(meet(X3,X4),join(X1,join(X4,Y4))))),
inference(cp,[status(thm)],[t8383,t7893]) ).
cnf(t173365,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(meet(X3,X4),join(X1,join(X4,Y4))))),
inference(step,[status(thm)],[t8449,t7893]) ).
cnf(t12653,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X1,join(X4,Y4))))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t173365]) ).
cnf(t12658,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(join(X1,join(X4,Y4)),meet(X3,X4)))),
inference(cp,[status(thm)],[t12653,t13]) ).
cnf(t173373,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X4,meet(join(X1,join(X4,Y4)),X3)))),
inference(step,[status(thm)],[t12658,t15]) ).
cnf(t173374,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,join(X2,meet(X3,meet(X4,join(X1,join(X4,Y4)))))),
inference(step,[status(thm)],[t173373,t15]) ).
cnf(t13651,plain,
meet(X1,join(X2,meet(X3,meet(X4,join(X1,join(X4,Y4)))))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t173374]) ).
cnf(t139056,plain,
join(X1,meet(X2,meet(X3,join(X3,join(X3,X4))))) = join(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t139049,t13651]) ).
cnf(t174087,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t139056,t10]) ).
cnf(t139476,plain,
join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t174087]) ).
cnf(t139854,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t33,t139476]) ).
cnf(t139966,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t139854]) ).
cnf(t140223,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)],[t25670,t139966]) ).
cnf(t174201,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)],[t140223,t45]) ).
cnf(t174202,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)],[t174201,t49]) ).
cnf(t174203,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)],[t174202,t45]) ).
cnf(t174204,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)],[t174203,t25670]) ).
cnf(t174205,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)],[t174204,t13]) ).
cnf(t172537,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)],[t174205]) ).
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,t49]) ).
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,t45]) ).
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,t33]) ).
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,t172537]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT151-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n010.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 20:23:52 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 58.22/7.93 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 58.22/7.93 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------