%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT201-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 : n001.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:56 PM UTC 2026
% Result : Unsatisfiable 39.96s 6.19s
% Output : Proof 39.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 221
% Number of leaves : 14
% Syntax : Number of formulae : 757 ( 753 unt; 0 def)
% Number of atoms : 765 ( 764 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-4 aty)
% Number of variables : 1908 ( 470 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f10,axiom,
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f10_nnf,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( complement(X0) = X1
| join(X0,X1) != one
| meet(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t11,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t18,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(f4,axiom,
meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f4_nnf,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t7,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t23,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t25,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X2,X1),one,complement(X2),X1),X1),
inference(cp,[status(thm)],[t18,t23]) ).
cnf(f5,axiom,
join(X,Y) = join(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f5_nnf,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t69,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t109981,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(step,[status(thm)],[t25,t69]) ).
cnf(t1005,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t109981]) ).
cnf(f9,axiom,
meet(X,complement(X)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_meet) ).
fof(f9_nnf,plain,
! [X] : meet(X,complement(X)) = zero,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] : meet(X,complement(X)) = zero,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
meet(X0,complement(X0)) = zero,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t3,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t62,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t1029,plain,
X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t1005,t62]) ).
cnf(t4,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t17,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t109982,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t1029,t17]) ).
cnf(f8,axiom,
join(X,complement(X)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_join) ).
fof(f8_nnf,plain,
! [X] : join(X,complement(X)) = one,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] : join(X,complement(X)) = one,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
join(X0,complement(X0)) = one,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t2,plain,
join(X1,complement(X1)) = one,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t96,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t109983,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t109982,t96]) ).
cnf(t109984,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t109983,t17]) ).
cnf(t1052,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t109984]) ).
cnf(f6,axiom,
meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f6_nnf,plain,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t10,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t109819,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t10,t23]) ).
cnf(t26,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t109819]) ).
cnf(t33,plain,
meet(X1,X2) = ifeq(meet(X2,meet(X3,X1)),zero,ifeq(join(X3,meet(X1,X2)),one,complement(X3),meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t18,t26]) ).
cnf(t110180,plain,
meet(X1,X2) = ifeq(meet(X1,meet(X2,X3)),zero,ifeq(join(X3,meet(X1,X2)),one,complement(X3),meet(X1,X2)),meet(X1,X2)),
inference(step,[status(thm)],[t33,t26]) ).
cnf(t3697,plain,
ifeq(meet(X1,meet(X2,X3)),zero,ifeq(join(X3,meet(X1,X2)),one,complement(X3),meet(X1,X2)),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t110180]) ).
cnf(f11,axiom,
meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,join(meet(X,Z),meet(Z,U)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H51) ).
fof(f11_nnf,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,join(meet(X,Z),meet(Z,U)))),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,join(meet(X,Z),meet(Z,U)))),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(X1,join(meet(X0,X2),meet(X2,X3)))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t12,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X3,X4)))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t46,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X3,X4)))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t12]) ).
cnf(f7,axiom,
join(join(X,Y),Z) = join(X,join(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f7_nnf,plain,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t9,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t109820,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t9,t69]) ).
cnf(t74,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t109820]) ).
cnf(f1,axiom,
join(X,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f1_nnf,plain,
! [X] : join(X,X) = X,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] : join(X,X) = X,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t0,plain,
join(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t15,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t77,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t74,t15]) ).
cnf(t109824,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t77,t74]) ).
cnf(t109825,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t109824,t69]) ).
cnf(t131,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t109825]) ).
cnf(t139,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(cp,[status(thm)],[t46,t131]) ).
cnf(f3,axiom,
join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption2) ).
fof(f3_nnf,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t6,plain,
join(X1,meet(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t16,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t78,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t74,t16]) ).
cnf(t109838,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t78,t74]) ).
cnf(t109839,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t109838,t69]) ).
cnf(t109840,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t109839,t69]) ).
cnf(t189,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t109840]) ).
cnf(t199,plain,
meet(X1,join(X2,meet(X2,join(X1,X3)))) = meet(X1,join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t46,t189]) ).
cnf(t109841,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t199,t16]) ).
cnf(t202,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t109841]) ).
cnf(f2,axiom,
meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption1) ).
fof(f2_nnf,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t8,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t14,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t30,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t26,t14]) ).
cnf(t109835,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t30,t26]) ).
cnf(t109836,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t109835,t23]) ).
cnf(t109837,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t109836,t23]) ).
cnf(t175,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t109837]) ).
cnf(t203,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t202,t175]) ).
cnf(t109878,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(step,[status(thm)],[t203,t175]) ).
cnf(t109879,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t109878,t69]) ).
cnf(t352,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t109879]) ).
cnf(t110043,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t139,t352]) ).
cnf(t1605,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t110043]) ).
cnf(t1647,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,join(meet(X1,X2),meet(join(X2,meet(X1,X2)),X3))),
inference(cp,[status(thm)],[t1605,t202]) ).
cnf(t110058,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(X2,meet(X1,X2)),X3))),
inference(step,[status(thm)],[t1647,t202]) ).
cnf(t110059,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t110058,t23]) ).
cnf(t1914,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t110059]) ).
cnf(t3796,plain,
meet(X1,X2) = ifeq(meet(X1,zero),zero,ifeq(join(complement(X2),meet(X1,X2)),one,complement(complement(X2)),meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t3697,t62]) ).
cnf(f0,axiom,
meet(X,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f0_nnf,plain,
! [X] : meet(X,X) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : meet(X,X) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
meet(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
meet(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t13,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t29,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t26,t13]) ).
cnf(t109821,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t29,t26]) ).
cnf(t109822,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t109821,t23]) ).
cnf(t112,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t109822]) ).
cnf(t115,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t112,t62]) ).
cnf(t109823,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t115,t62]) ).
cnf(t124,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t109823]) ).
cnf(t110186,plain,
meet(X1,X2) = ifeq(zero,zero,ifeq(join(complement(X2),meet(X1,X2)),one,complement(complement(X2)),meet(X1,X2)),meet(X1,X2)),
inference(step,[status(thm)],[t3796,t124]) ).
cnf(t110187,plain,
meet(X1,X2) = ifeq(join(complement(X2),meet(X1,X2)),one,complement(complement(X2)),meet(X1,X2)),
inference(step,[status(thm)],[t110186,t17]) ).
cnf(t110188,plain,
meet(X1,X2) = ifeq(join(complement(X2),meet(X1,X2)),one,X2,meet(X1,X2)),
inference(step,[status(thm)],[t110187,t1052]) ).
cnf(t4105,plain,
ifeq(join(complement(X1),meet(X2,X1)),one,X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t110188]) ).
cnf(t134,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t131,t96]) ).
cnf(t109826,plain,
one = join(X1,one),
inference(step,[status(thm)],[t134,t96]) ).
cnf(t142,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t109826]) ).
cnf(t144,plain,
one = ifeq(meet(X1,one),zero,ifeq(one,one,complement(X1),one),one),
inference(cp,[status(thm)],[t18,t142]) ).
cnf(t97,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t14,t96]) ).
cnf(t105,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t97]) ).
cnf(t109829,plain,
one = ifeq(X1,zero,ifeq(one,one,complement(X1),one),one),
inference(step,[status(thm)],[t144,t105]) ).
cnf(t109830,plain,
one = ifeq(X1,zero,complement(X1),one),
inference(step,[status(thm)],[t109829,t17]) ).
cnf(t151,plain,
ifeq(X1,zero,complement(X1),one) = one,
inference(orient,[status(thm)],[t109830]) ).
cnf(t1055,plain,
one = ifeq(complement(X1),zero,X1,one),
inference(cp,[status(thm)],[t151,t1052]) ).
cnf(t1079,plain,
ifeq(complement(X1),zero,X1,one) = one,
inference(orient,[status(thm)],[t1055]) ).
cnf(t67,plain,
meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
inference(cp,[status(thm)],[t26,t62]) ).
cnf(t109831,plain,
meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
inference(step,[status(thm)],[t67,t23]) ).
cnf(t109832,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t109831,t124]) ).
cnf(t159,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t109832]) ).
cnf(t356,plain,
meet(X1,meet(X2,complement(X1))) = meet(X1,join(zero,meet(meet(X2,complement(X1)),join(X1,X3)))),
inference(cp,[status(thm)],[t352,t159]) ).
cnf(t109904,plain,
zero = meet(X1,join(zero,meet(meet(X2,complement(X1)),join(X1,X3)))),
inference(step,[status(thm)],[t356,t159]) ).
cnf(t109905,plain,
zero = meet(X1,join(zero,meet(join(X1,X3),meet(X2,complement(X1))))),
inference(step,[status(thm)],[t109904,t23]) ).
cnf(t109906,plain,
zero = meet(X1,join(zero,meet(complement(X1),meet(join(X1,X3),X2)))),
inference(step,[status(thm)],[t109905,t26]) ).
cnf(t109907,plain,
zero = meet(X1,join(zero,meet(X2,meet(complement(X1),join(X1,X3))))),
inference(step,[status(thm)],[t109906,t26]) ).
cnf(t477,plain,
meet(X1,join(zero,meet(X2,meet(complement(X1),join(X1,X3))))) = zero,
inference(orient,[status(thm)],[t109907]) ).
cnf(t98,plain,
join(X1,join(complement(X1),X2)) = join(X2,one),
inference(cp,[status(thm)],[t74,t96]) ).
cnf(t109833,plain,
join(X1,join(X2,complement(X1))) = join(X2,one),
inference(step,[status(thm)],[t98,t69]) ).
cnf(t109834,plain,
join(X1,join(X2,complement(X1))) = one,
inference(step,[status(thm)],[t109833,t142]) ).
cnf(t168,plain,
join(X1,join(X2,complement(X1))) = one,
inference(orient,[status(thm)],[t109834]) ).
cnf(t173,plain,
join(X1,join(join(X2,complement(X1)),X3)) = join(X3,one),
inference(cp,[status(thm)],[t74,t168]) ).
cnf(t109846,plain,
join(X1,join(X3,join(X2,complement(X1)))) = join(X3,one),
inference(step,[status(thm)],[t173,t69]) ).
cnf(t109847,plain,
join(X1,join(X2,join(complement(X1),X3))) = join(X3,one),
inference(step,[status(thm)],[t109846,t74]) ).
cnf(t109848,plain,
join(X1,join(X2,join(X3,complement(X1)))) = join(X3,one),
inference(step,[status(thm)],[t109847,t69]) ).
cnf(t109849,plain,
join(X1,join(X2,join(X3,complement(X1)))) = one,
inference(step,[status(thm)],[t109848,t142]) ).
cnf(t228,plain,
join(X1,join(X2,join(X3,complement(X1)))) = one,
inference(orient,[status(thm)],[t109849]) ).
cnf(t485,plain,
zero = meet(X1,join(zero,meet(X2,meet(complement(X1),one)))),
inference(cp,[status(thm)],[t477,t228]) ).
cnf(t109908,plain,
zero = meet(X1,join(zero,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t485,t105]) ).
cnf(t505,plain,
meet(X1,join(zero,meet(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t109908]) ).
cnf(t514,plain,
meet(X1,meet(join(zero,meet(X2,complement(X1))),X3)) = meet(X3,zero),
inference(cp,[status(thm)],[t26,t505]) ).
cnf(t109909,plain,
meet(X1,meet(X3,join(zero,meet(X2,complement(X1))))) = meet(X3,zero),
inference(step,[status(thm)],[t514,t23]) ).
cnf(t109910,plain,
meet(X1,meet(X3,join(zero,meet(X2,complement(X1))))) = zero,
inference(step,[status(thm)],[t109909,t124]) ).
cnf(t516,plain,
meet(X1,meet(X2,join(zero,meet(X3,complement(X1))))) = zero,
inference(orient,[status(thm)],[t109910]) ).
cnf(t1623,plain,
meet(X1,meet(X2,join(zero,meet(X3,complement(X1))))) = meet(X1,join(zero,meet(meet(X2,join(zero,meet(X3,complement(X1)))),X4))),
inference(cp,[status(thm)],[t1605,t516]) ).
cnf(t110077,plain,
zero = meet(X1,join(zero,meet(meet(X2,join(zero,meet(X3,complement(X1)))),X4))),
inference(step,[status(thm)],[t1623,t516]) ).
cnf(t110078,plain,
zero = meet(X1,join(zero,meet(X4,meet(X2,join(zero,meet(X3,complement(X1))))))),
inference(step,[status(thm)],[t110077,t23]) ).
cnf(t110079,plain,
zero = meet(X1,join(zero,meet(X2,meet(join(zero,meet(X3,complement(X1))),X4)))),
inference(step,[status(thm)],[t110078,t26]) ).
cnf(t110080,plain,
zero = meet(X1,join(zero,meet(X2,meet(X4,join(zero,meet(X3,complement(X1))))))),
inference(step,[status(thm)],[t110079,t23]) ).
cnf(t2239,plain,
meet(X1,join(zero,meet(X2,meet(X3,join(zero,meet(X4,complement(X1))))))) = zero,
inference(orient,[status(thm)],[t110080]) ).
cnf(t2245,plain,
zero = meet(complement(X1),join(zero,meet(X2,meet(X3,join(zero,meet(X4,X1)))))),
inference(cp,[status(thm)],[t2239,t1052]) ).
cnf(t110106,plain,
zero = meet(complement(X1),join(zero,meet(X2,meet(X3,join(zero,meet(X1,X4)))))),
inference(step,[status(thm)],[t2245,t23]) ).
cnf(t2554,plain,
meet(complement(X1),join(zero,meet(X2,meet(X3,join(zero,meet(X1,X4)))))) = zero,
inference(orient,[status(thm)],[t110106]) ).
cnf(t48,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X1,X4)))) = meet(X1,join(X2,join(X1,meet(join(X1,X3),X4)))),
inference(cp,[status(thm)],[t46,t14]) ).
cnf(t110205,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X1,X4)))) = meet(X1,join(X1,join(meet(join(X1,X3),X4),X2))),
inference(step,[status(thm)],[t48,t74]) ).
cnf(t110206,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X1,X4)))) = X1,
inference(step,[status(thm)],[t110205,t14]) ).
cnf(t4466,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X1,X4)))) = X1,
inference(orient,[status(thm)],[t110206]) ).
cnf(t4539,plain,
zero = meet(complement(join(X1,X2)),join(zero,meet(X3,X1))),
inference(cp,[status(thm)],[t2554,t4466]) ).
cnf(t110212,plain,
zero = meet(complement(join(X1,X2)),join(zero,meet(X1,X3))),
inference(step,[status(thm)],[t4539,t23]) ).
cnf(t4604,plain,
meet(complement(join(X1,X2)),join(zero,meet(X1,X3))) = zero,
inference(orient,[status(thm)],[t110212]) ).
cnf(t4614,plain,
zero = meet(complement(join(X1,X2)),join(zero,meet(X2,X3))),
inference(cp,[status(thm)],[t4604,t69]) ).
cnf(t4727,plain,
meet(complement(join(X1,X2)),join(zero,meet(X2,X3))) = zero,
inference(orient,[status(thm)],[t4614]) ).
cnf(t53,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X3,X4))))) = meet(X1,join(X2,join(meet(X1,X3),X3))),
inference(cp,[status(thm)],[t46,t14]) ).
cnf(t110040,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X3,X4))))) = meet(X1,join(X2,join(X3,meet(X1,X3)))),
inference(step,[status(thm)],[t53,t69]) ).
cnf(t52,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,join(meet(X1,X3),X3))),
inference(cp,[status(thm)],[t46,t13]) ).
cnf(t109925,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,join(X3,meet(X1,X3)))),
inference(step,[status(thm)],[t52,t69]) ).
cnf(t586,plain,
meet(X1,join(X2,join(X3,meet(X1,X3)))) = meet(X1,join(X2,meet(X3,join(X1,X3)))),
inference(orient,[status(thm)],[t109925]) ).
cnf(t611,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,join(X3,meet(X3,X1)))),
inference(cp,[status(thm)],[t586,t23]) ).
cnf(t109926,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t611,t16]) ).
cnf(t623,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t109926]) ).
cnf(t109927,plain,
meet(X1,join(X2,join(X3,meet(X1,X3)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t586,t623]) ).
cnf(t624,plain,
meet(X1,join(X2,join(X3,meet(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t109927]) ).
cnf(t110041,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X3,X4))))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t110040,t624]) ).
cnf(t1518,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X3,X4))))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t110041]) ).
cnf(t4729,plain,
zero = meet(complement(join(X1,X2)),join(zero,X2)),
inference(cp,[status(thm)],[t4727,t1518]) ).
cnf(t110219,plain,
zero = meet(join(zero,X2),complement(join(X1,X2))),
inference(step,[status(thm)],[t4729,t23]) ).
cnf(t110220,plain,
zero = meet(join(X2,zero),complement(join(X1,X2))),
inference(step,[status(thm)],[t110219,t69]) ).
cnf(t63,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t16,t62]) ).
cnf(t100,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t63]) ).
cnf(t110221,plain,
zero = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t110220,t100]) ).
cnf(t4777,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t110221]) ).
cnf(t4780,plain,
zero = meet(join(X1,meet(X2,X3)),complement(join(X2,X1))),
inference(cp,[status(thm)],[t4777,t189]) ).
cnf(t110225,plain,
zero = meet(complement(join(X2,X1)),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t4780,t23]) ).
cnf(t110226,plain,
zero = meet(complement(join(X1,X2)),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t110225,t69]) ).
cnf(t4847,plain,
meet(complement(join(X1,X2)),join(X1,meet(X2,X3))) = zero,
inference(orient,[status(thm)],[t110226]) ).
cnf(t4857,plain,
zero = meet(complement(join(X1,X2)),join(X1,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t4847,t131]) ).
cnf(t110248,plain,
zero = meet(complement(join(X1,X2)),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t4857,t23]) ).
cnf(t5600,plain,
meet(complement(join(X1,X2)),join(X1,meet(X3,join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t110248]) ).
cnf(t108,plain,
meet(X1,join(X2,meet(one,join(X1,X3)))) = meet(X1,join(X2,join(X1,meet(one,X3)))),
inference(cp,[status(thm)],[t46,t105]) ).
cnf(t109929,plain,
meet(X1,join(X2,meet(one,join(X1,X3)))) = meet(X1,join(X1,join(meet(one,X3),X2))),
inference(step,[status(thm)],[t108,t74]) ).
cnf(t109930,plain,
meet(X1,join(X2,meet(one,join(X1,X3)))) = X1,
inference(step,[status(thm)],[t109929,t14]) ).
cnf(t645,plain,
meet(X1,join(X2,meet(one,join(X1,X3)))) = X1,
inference(orient,[status(thm)],[t109930]) ).
cnf(t5616,plain,
zero = meet(complement(join(X1,meet(one,join(X2,X3)))),join(X1,X2)),
inference(cp,[status(thm)],[t5600,t645]) ).
cnf(t110308,plain,
zero = meet(join(X1,X2),complement(join(X1,meet(one,join(X2,X3))))),
inference(step,[status(thm)],[t5616,t23]) ).
cnf(t7788,plain,
meet(join(X1,X2),complement(join(X1,meet(one,join(X2,X3))))) = zero,
inference(orient,[status(thm)],[t110308]) ).
cnf(t7800,plain,
zero = meet(join(X1,X2),complement(join(X2,meet(one,join(X1,X3))))),
inference(cp,[status(thm)],[t7788,t69]) ).
cnf(t10956,plain,
meet(join(X1,X2),complement(join(X2,meet(one,join(X1,X3))))) = zero,
inference(orient,[status(thm)],[t7800]) ).
cnf(t10963,plain,
zero = meet(one,complement(join(join(X1,complement(X2)),meet(one,join(X2,X3))))),
inference(cp,[status(thm)],[t10956,t168]) ).
cnf(t214,plain,
meet(X1,meet(join(X2,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t26,t202]) ).
cnf(t109875,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t214,t23]) ).
cnf(t109876,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t109875,t26]) ).
cnf(t109877,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t109876,t26]) ).
cnf(t321,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t109877]) ).
cnf(t350,plain,
meet(X1,meet(meet(X2,join(X3,meet(X1,X3))),X4)) = meet(X4,meet(X1,meet(X3,X2))),
inference(cp,[status(thm)],[t26,t321]) ).
cnf(t109961,plain,
meet(X1,meet(X4,meet(X2,join(X3,meet(X1,X3))))) = meet(X4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t350,t23]) ).
cnf(t109962,plain,
meet(X1,meet(X2,meet(join(X3,meet(X1,X3)),X4))) = meet(X4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t109961,t26]) ).
cnf(t109963,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X3))))) = meet(X4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t109962,t23]) ).
cnf(t109964,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X3))))) = meet(X1,meet(meet(X3,X2),X4)),
inference(step,[status(thm)],[t109963,t26]) ).
cnf(t109965,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X3))))) = meet(X1,meet(X4,meet(X3,X2))),
inference(step,[status(thm)],[t109964,t23]) ).
cnf(t109966,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X3))))) = meet(X1,meet(X2,meet(X4,X3))),
inference(step,[status(thm)],[t109965,t26]) ).
cnf(t109967,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X3))))) = meet(X1,meet(X2,meet(X3,X4))),
inference(step,[status(thm)],[t109966,t23]) ).
cnf(t866,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X4))))) = meet(X1,meet(X2,meet(X4,X3))),
inference(orient,[status(thm)],[t109967]) ).
cnf(t66,plain,
meet(X1,join(X2,meet(X3,join(X1,complement(X3))))) = meet(X1,join(X2,join(meet(X1,X3),zero))),
inference(cp,[status(thm)],[t46,t62]) ).
cnf(t109941,plain,
meet(X1,join(X2,meet(X3,join(X1,complement(X3))))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t66,t100]) ).
cnf(t756,plain,
meet(X1,join(X2,meet(X3,join(X1,complement(X3))))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t109941]) ).
cnf(t1071,plain,
meet(X1,join(X2,meet(X1,complement(X3)))) = meet(X1,join(X2,meet(complement(X3),join(X1,X3)))),
inference(cp,[status(thm)],[t756,t1052]) ).
cnf(t1105,plain,
meet(X1,join(X2,meet(complement(X3),join(X1,X3)))) = meet(X1,join(X2,meet(X1,complement(X3)))),
inference(orient,[status(thm)],[t1071]) ).
cnf(t1117,plain,
meet(X1,join(X2,meet(X1,complement(join(X3,complement(X1)))))) = meet(X1,join(X2,meet(complement(join(X3,complement(X1))),one))),
inference(cp,[status(thm)],[t1105,t168]) ).
cnf(t110108,plain,
meet(X1,join(X2,meet(X1,complement(join(X3,complement(X1)))))) = meet(X1,join(X2,complement(join(X3,complement(X1))))),
inference(step,[status(thm)],[t1117,t105]) ).
cnf(t2670,plain,
meet(X1,join(X2,meet(X1,complement(join(X3,complement(X1)))))) = meet(X1,join(X2,complement(join(X3,complement(X1))))),
inference(orient,[status(thm)],[t110108]) ).
cnf(t126,plain,
zero = ifeq(zero,zero,ifeq(join(X1,zero),one,complement(X1),zero),zero),
inference(cp,[status(thm)],[t18,t124]) ).
cnf(t109827,plain,
zero = ifeq(join(X1,zero),one,complement(X1),zero),
inference(step,[status(thm)],[t126,t17]) ).
cnf(t109828,plain,
zero = ifeq(X1,one,complement(X1),zero),
inference(step,[status(thm)],[t109827,t100]) ).
cnf(t147,plain,
ifeq(X1,one,complement(X1),zero) = zero,
inference(orient,[status(thm)],[t109828]) ).
cnf(t148,plain,
zero = complement(one),
inference(cp,[status(thm)],[t147,t17]) ).
cnf(t149,plain,
complement(one) = zero,
inference(orient,[status(thm)],[t148]) ).
cnf(t2675,plain,
meet(one,join(X1,complement(join(X2,complement(one))))) = meet(one,join(X1,meet(one,complement(join(X2,zero))))),
inference(cp,[status(thm)],[t2670,t149]) ).
cnf(t110109,plain,
meet(one,join(X1,complement(join(X2,zero)))) = meet(one,join(X1,meet(one,complement(join(X2,zero))))),
inference(step,[status(thm)],[t2675,t149]) ).
cnf(t110110,plain,
meet(one,join(X1,complement(X2))) = meet(one,join(X1,meet(one,complement(join(X2,zero))))),
inference(step,[status(thm)],[t110109,t100]) ).
cnf(t110111,plain,
meet(one,join(X1,complement(X2))) = meet(one,join(X1,meet(one,complement(X2)))),
inference(step,[status(thm)],[t110110,t100]) ).
cnf(t2699,plain,
meet(one,join(X1,meet(one,complement(X2)))) = meet(one,join(X1,complement(X2))),
inference(orient,[status(thm)],[t110111]) ).
cnf(t2719,plain,
meet(one,meet(X1,meet(complement(X2),one))) = meet(one,meet(X1,meet(one,join(complement(X2),complement(X2))))),
inference(cp,[status(thm)],[t866,t2699]) ).
cnf(t110112,plain,
meet(X1,meet(meet(complement(X2),one),one)) = meet(one,meet(X1,meet(one,join(complement(X2),complement(X2))))),
inference(step,[status(thm)],[t2719,t26]) ).
cnf(t110113,plain,
meet(X1,meet(complement(X2),one)) = meet(one,meet(X1,meet(one,join(complement(X2),complement(X2))))),
inference(step,[status(thm)],[t110112,t105]) ).
cnf(t110114,plain,
meet(X1,complement(X2)) = meet(one,meet(X1,meet(one,join(complement(X2),complement(X2))))),
inference(step,[status(thm)],[t110113,t105]) ).
cnf(t110115,plain,
meet(X1,complement(X2)) = meet(X1,meet(meet(one,join(complement(X2),complement(X2))),one)),
inference(step,[status(thm)],[t110114,t26]) ).
cnf(t110116,plain,
meet(X1,complement(X2)) = meet(X1,meet(one,join(complement(X2),complement(X2)))),
inference(step,[status(thm)],[t110115,t105]) ).
cnf(t110117,plain,
meet(X1,complement(X2)) = meet(X1,meet(one,complement(X2))),
inference(step,[status(thm)],[t110116,t15]) ).
cnf(t2723,plain,
meet(X1,meet(one,complement(X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t110117]) ).
cnf(t2724,plain,
meet(meet(one,complement(X1)),complement(X1)) = meet(one,complement(X1)),
inference(cp,[status(thm)],[t2723,t13]) ).
cnf(t110118,plain,
meet(complement(X1),meet(one,complement(X1))) = meet(one,complement(X1)),
inference(step,[status(thm)],[t2724,t23]) ).
cnf(t110119,plain,
meet(complement(X1),complement(X1)) = meet(one,complement(X1)),
inference(step,[status(thm)],[t110118,t2723]) ).
cnf(t110120,plain,
complement(X1) = meet(one,complement(X1)),
inference(step,[status(thm)],[t110119,t13]) ).
cnf(t2747,plain,
meet(one,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t110120]) ).
cnf(t110405,plain,
zero = complement(join(join(X1,complement(X2)),meet(one,join(X2,X3)))),
inference(step,[status(thm)],[t10963,t2747]) ).
cnf(t11058,plain,
complement(join(join(X1,complement(X2)),meet(one,join(X2,X3)))) = zero,
inference(orient,[status(thm)],[t110405]) ).
cnf(t11076,plain,
one = ifeq(zero,zero,join(join(X1,complement(X2)),meet(one,join(X2,X3))),one),
inference(cp,[status(thm)],[t1079,t11058]) ).
cnf(t110406,plain,
one = join(join(X1,complement(X2)),meet(one,join(X2,X3))),
inference(step,[status(thm)],[t11076,t17]) ).
cnf(t11123,plain,
join(join(X1,complement(X2)),meet(one,join(X2,X3))) = one,
inference(orient,[status(thm)],[t110406]) ).
cnf(t11126,plain,
one = join(join(X1,X2),meet(one,join(complement(X2),X3))),
inference(cp,[status(thm)],[t11123,t1052]) ).
cnf(t110407,plain,
one = join(join(X1,X2),meet(one,join(X3,complement(X2)))),
inference(step,[status(thm)],[t11126,t69]) ).
cnf(t11159,plain,
join(join(X1,X2),meet(one,join(X3,complement(X2)))) = one,
inference(orient,[status(thm)],[t110407]) ).
cnf(t11164,plain,
one = join(X1,meet(one,join(X2,complement(meet(X1,X3))))),
inference(cp,[status(thm)],[t11159,t16]) ).
cnf(t11191,plain,
join(X1,meet(one,join(X2,complement(meet(X1,X3))))) = one,
inference(orient,[status(thm)],[t11164]) ).
cnf(t11192,plain,
one = join(X1,meet(one,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t11191,t15]) ).
cnf(t110408,plain,
one = join(X1,complement(meet(X1,X2))),
inference(step,[status(thm)],[t11192,t2747]) ).
cnf(t11233,plain,
join(X1,complement(meet(X1,X2))) = one,
inference(orient,[status(thm)],[t110408]) ).
cnf(t11244,plain,
zero = meet(one,complement(join(complement(meet(X1,X2)),meet(one,join(X1,X3))))),
inference(cp,[status(thm)],[t10956,t11233]) ).
cnf(t110415,plain,
zero = complement(join(complement(meet(X1,X2)),meet(one,join(X1,X3)))),
inference(step,[status(thm)],[t11244,t2747]) ).
cnf(t11318,plain,
complement(join(complement(meet(X1,X2)),meet(one,join(X1,X3)))) = zero,
inference(orient,[status(thm)],[t110415]) ).
cnf(t11362,plain,
one = ifeq(zero,zero,join(complement(meet(X1,X2)),meet(one,join(X1,X3))),one),
inference(cp,[status(thm)],[t1079,t11318]) ).
cnf(t110416,plain,
one = join(complement(meet(X1,X2)),meet(one,join(X1,X3))),
inference(step,[status(thm)],[t11362,t17]) ).
cnf(t11411,plain,
join(complement(meet(X1,X2)),meet(one,join(X1,X3))) = one,
inference(orient,[status(thm)],[t110416]) ).
cnf(t11414,plain,
one = join(complement(meet(X1,meet(X2,X3))),meet(one,join(X3,X4))),
inference(cp,[status(thm)],[t11411,t26]) ).
cnf(t110576,plain,
one = join(meet(one,join(X3,X4)),complement(meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t11414,t69]) ).
cnf(t17891,plain,
join(meet(one,join(X1,X2)),complement(meet(X3,meet(X4,X1)))) = one,
inference(orient,[status(thm)],[t110576]) ).
cnf(t17901,plain,
one = join(meet(one,join(X1,X2)),complement(meet(X3,meet(X4,X2)))),
inference(cp,[status(thm)],[t17891,t69]) ).
cnf(t110718,plain,
one = join(meet(one,join(X1,X2)),complement(meet(X2,meet(X3,X4)))),
inference(step,[status(thm)],[t17901,t26]) ).
cnf(t23108,plain,
join(meet(one,join(X1,X2)),complement(meet(X2,meet(X3,X4)))) = one,
inference(orient,[status(thm)],[t110718]) ).
cnf(t23154,plain,
one = join(meet(one,join(X1,X2)),complement(meet(X2,complement(X3)))),
inference(cp,[status(thm)],[t23108,t2747]) ).
cnf(t23295,plain,
join(meet(one,join(X1,X2)),complement(meet(X2,complement(X3)))) = one,
inference(orient,[status(thm)],[t23154]) ).
cnf(t152,plain,
one = complement(zero),
inference(cp,[status(thm)],[t151,t17]) ).
cnf(t154,plain,
complement(zero) = one,
inference(orient,[status(thm)],[t152]) ).
cnf(t23325,plain,
one = join(meet(one,join(X1,X2)),complement(meet(X2,one))),
inference(cp,[status(thm)],[t23295,t154]) ).
cnf(t110720,plain,
one = join(meet(one,join(X1,X2)),complement(X2)),
inference(step,[status(thm)],[t23325,t105]) ).
cnf(t110721,plain,
one = join(complement(X2),meet(one,join(X1,X2))),
inference(step,[status(thm)],[t110720,t69]) ).
cnf(t23365,plain,
join(complement(X1),meet(one,join(X2,X1))) = one,
inference(orient,[status(thm)],[t110721]) ).
cnf(t23383,plain,
one = join(complement(join(X1,X2)),meet(one,join(X1,X2))),
inference(cp,[status(thm)],[t23365,t131]) ).
cnf(t23434,plain,
join(complement(join(X1,X2)),meet(one,join(X1,X2))) = one,
inference(orient,[status(thm)],[t23383]) ).
cnf(t23466,plain,
meet(one,join(X1,X2)) = ifeq(one,one,join(X1,X2),meet(one,join(X1,X2))),
inference(cp,[status(thm)],[t4105,t23434]) ).
cnf(t110722,plain,
meet(one,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t23466,t17]) ).
cnf(t23506,plain,
meet(one,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t110722]) ).
cnf(t23598,plain,
meet(one,join(X1,X2)) = meet(one,join(join(X1,X2),meet(X3,join(join(X1,X2),meet(one,join(X1,X2)))))),
inference(cp,[status(thm)],[t1914,t23506]) ).
cnf(t110746,plain,
join(X1,X2) = meet(one,join(join(X1,X2),meet(X3,join(join(X1,X2),meet(one,join(X1,X2)))))),
inference(step,[status(thm)],[t23598,t23506]) ).
cnf(t110747,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(join(X1,X2),meet(one,join(X1,X2))))),
inference(step,[status(thm)],[t110746,t23506]) ).
cnf(t110748,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(join(X1,X2),join(X1,X2)))),
inference(step,[status(thm)],[t110747,t23506]) ).
cnf(t110749,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t110748,t15]) ).
cnf(t23652,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t110749]) ).
cnf(t11413,plain,
one = join(complement(meet(X1,X2)),meet(one,join(X2,X3))),
inference(cp,[status(thm)],[t11411,t23]) ).
cnf(t12589,plain,
join(complement(meet(X1,X2)),meet(one,join(X2,X3))) = one,
inference(orient,[status(thm)],[t11413]) ).
cnf(t12630,plain,
one = join(complement(meet(X1,X2)),meet(one,X2)),
inference(cp,[status(thm)],[t12589,t202]) ).
cnf(t110419,plain,
one = join(meet(one,X2),complement(meet(X1,X2))),
inference(step,[status(thm)],[t12630,t69]) ).
cnf(t110420,plain,
one = join(meet(X2,one),complement(meet(X1,X2))),
inference(step,[status(thm)],[t110419,t23]) ).
cnf(t110421,plain,
one = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t110420,t105]) ).
cnf(t12667,plain,
join(X1,complement(meet(X2,X1))) = one,
inference(orient,[status(thm)],[t110421]) ).
cnf(t12705,plain,
one = join(meet(X1,X2),complement(meet(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t12667,t26]) ).
cnf(t13036,plain,
join(meet(X1,X2),complement(meet(X1,meet(X2,X3)))) = one,
inference(orient,[status(thm)],[t12705]) ).
cnf(t13200,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(join(meet(X1,X2),X4),one))),
inference(cp,[status(thm)],[t4466,t13036]) ).
cnf(t110464,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),X4))),
inference(step,[status(thm)],[t13200,t105]) ).
cnf(t110465,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t110464,t69]) ).
cnf(t14210,plain,
meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t110465]) ).
cnf(t23732,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X4,join(X2,X3))),
inference(cp,[status(thm)],[t14210,t23652]) ).
cnf(t110888,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X3,join(X4,X2))),
inference(step,[status(thm)],[t23732,t74]) ).
cnf(t110889,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,join(X3,X4))),
inference(step,[status(thm)],[t110888,t74]) ).
cnf(t33452,plain,
meet(meet(X1,join(X2,X3)),join(X2,join(X3,X4))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t110889]) ).
cnf(t33600,plain,
join(X1,join(X2,X3)) = join(join(X1,join(X2,X3)),meet(X4,join(X1,X2))),
inference(cp,[status(thm)],[t23652,t33452]) ).
cnf(t110890,plain,
join(X1,join(X2,X3)) = join(meet(X4,join(X1,X2)),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t33600,t69]) ).
cnf(t110891,plain,
join(X1,join(X2,X3)) = join(join(X2,X3),join(meet(X4,join(X1,X2)),X1)),
inference(step,[status(thm)],[t110890,t74]) ).
cnf(t110892,plain,
join(X1,join(X2,X3)) = join(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t110891,t74]) ).
cnf(t34017,plain,
join(X1,join(join(X2,X3),meet(X4,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t110892]) ).
cnf(t34021,plain,
join(X1,join(X2,X2)) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t34017,t15]) ).
cnf(t110893,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t34021,t15]) ).
cnf(t34240,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t110893]) ).
cnf(t34385,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,meet(X1,X3)))))) = meet(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t46,t34240]) ).
cnf(t110905,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t34385,t189]) ).
cnf(t36091,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t110905]) ).
cnf(t36214,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),meet(X2,one))),
inference(cp,[status(thm)],[t36091,t96]) ).
cnf(t110906,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t36214,t105]) ).
cnf(t110907,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(X2,complement(X1))),
inference(step,[status(thm)],[t110906,t69]) ).
cnf(t36371,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(X2,complement(X1))),
inference(orient,[status(thm)],[t110907]) ).
cnf(t1681,plain,
meet(X1,meet(join(meet(X1,X2),meet(X2,X3)),X4)) = meet(X4,meet(X1,X2)),
inference(cp,[status(thm)],[t26,t1605]) ).
cnf(t110055,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,X3)))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t1681,t23]) ).
cnf(t110056,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,X3)))) = meet(X2,meet(X4,X1)),
inference(step,[status(thm)],[t110055,t26]) ).
cnf(t110057,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,X3)))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t110056,t26]) ).
cnf(t1794,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X3,X4)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t110057]) ).
cnf(t5661,plain,
meet(X1,meet(X2,complement(join(meet(X1,X2),X3)))) = meet(X1,zero),
inference(cp,[status(thm)],[t1794,t5600]) ).
cnf(t110249,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))) = meet(X1,zero),
inference(step,[status(thm)],[t5661,t69]) ).
cnf(t110250,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))) = zero,
inference(step,[status(thm)],[t110249,t124]) ).
cnf(t5675,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t110250]) ).
cnf(t5677,plain,
zero = meet(X1,meet(X2,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t5675,t15]) ).
cnf(t5830,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t5677]) ).
cnf(t36440,plain,
meet(X1,join(meet(X2,complement(meet(X1,X2))),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t36371,t5830]) ).
cnf(t111012,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t36440,t69]) ).
cnf(t111013,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t111012,t100]) ).
cnf(t111014,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = zero,
inference(step,[status(thm)],[t111013,t62]) ).
cnf(t46102,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t111014]) ).
cnf(t46233,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = ifeq(zero,zero,ifeq(join(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))),one,complement(X1),join(complement(X1),meet(X2,complement(meet(X1,X2))))),join(complement(X1),meet(X2,complement(meet(X1,X2))))),
inference(cp,[status(thm)],[t18,t46102]) ).
cnf(t111015,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = ifeq(join(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))),one,complement(X1),join(complement(X1),meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t46233,t17]) ).
cnf(t14221,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t14210,t189]) ).
cnf(t14315,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t14221]) ).
cnf(t14358,plain,
one = join(join(X1,X2),complement(meet(X1,X3))),
inference(cp,[status(thm)],[t12667,t14315]) ).
cnf(t14447,plain,
join(join(X1,X2),complement(meet(X1,X3))) = one,
inference(orient,[status(thm)],[t14358]) ).
cnf(t14450,plain,
one = join(join(X1,X2),complement(meet(X2,X3))),
inference(cp,[status(thm)],[t14447,t69]) ).
cnf(t14491,plain,
join(join(X1,X2),complement(meet(X2,X3))) = one,
inference(orient,[status(thm)],[t14450]) ).
cnf(t14495,plain,
one = join(join(X1,X2),complement(meet(join(X2,meet(X1,X3)),X4))),
inference(cp,[status(thm)],[t14491,t189]) ).
cnf(t110662,plain,
one = join(join(X1,X2),complement(meet(X4,join(X2,meet(X1,X3))))),
inference(step,[status(thm)],[t14495,t23]) ).
cnf(t19453,plain,
join(join(X1,X2),complement(meet(X3,join(X2,meet(X1,X4))))) = one,
inference(orient,[status(thm)],[t110662]) ).
cnf(t19479,plain,
one = join(join(X1,X2),complement(join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t19453,t13]) ).
cnf(t19631,plain,
join(join(X1,X2),complement(join(X2,meet(X1,X3)))) = one,
inference(orient,[status(thm)],[t19479]) ).
cnf(t4615,plain,
zero = meet(complement(join(X1,join(X2,X3))),join(zero,meet(X3,X4))),
inference(cp,[status(thm)],[t4604,t74]) ).
cnf(t110237,plain,
zero = meet(join(zero,meet(X3,X4)),complement(join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t4615,t23]) ).
cnf(t5367,plain,
meet(join(zero,meet(X1,X2)),complement(join(X3,join(X4,X1)))) = zero,
inference(orient,[status(thm)],[t110237]) ).
cnf(t5375,plain,
zero = meet(join(zero,meet(X1,X2)),complement(join(X3,join(X4,X2)))),
inference(cp,[status(thm)],[t5367,t23]) ).
cnf(t110283,plain,
zero = meet(join(zero,meet(X1,X2)),complement(join(X2,join(X3,X4)))),
inference(step,[status(thm)],[t5375,t74]) ).
cnf(t6456,plain,
meet(join(zero,meet(X1,X2)),complement(join(X2,join(X3,X4)))) = zero,
inference(orient,[status(thm)],[t110283]) ).
cnf(t2761,plain,
meet(one,complement(X1)) = meet(one,join(complement(X1),meet(X2,join(complement(X1),meet(one,complement(X1)))))),
inference(cp,[status(thm)],[t1914,t2747]) ).
cnf(t110125,plain,
complement(X1) = meet(one,join(complement(X1),meet(X2,join(complement(X1),meet(one,complement(X1)))))),
inference(step,[status(thm)],[t2761,t2747]) ).
cnf(t110126,plain,
complement(X1) = meet(one,join(complement(X1),meet(X2,join(complement(X1),complement(X1))))),
inference(step,[status(thm)],[t110125,t2747]) ).
cnf(t110127,plain,
complement(X1) = meet(one,join(complement(X1),meet(X2,complement(X1)))),
inference(step,[status(thm)],[t110126,t15]) ).
cnf(t2773,plain,
meet(one,join(complement(X1),meet(X2,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t110127]) ).
cnf(t2801,plain,
meet(join(complement(X1),meet(X2,complement(X1))),meet(X3,one)) = meet(X3,complement(X1)),
inference(cp,[status(thm)],[t26,t2773]) ).
cnf(t110128,plain,
meet(join(complement(X1),meet(X2,complement(X1))),X3) = meet(X3,complement(X1)),
inference(step,[status(thm)],[t2801,t105]) ).
cnf(t110129,plain,
meet(X3,join(complement(X1),meet(X2,complement(X1)))) = meet(X3,complement(X1)),
inference(step,[status(thm)],[t110128,t23]) ).
cnf(t2821,plain,
meet(X1,join(complement(X2),meet(X3,complement(X2)))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t110129]) ).
cnf(t2822,plain,
meet(join(complement(X1),meet(X2,complement(X1))),complement(X1)) = join(complement(X1),meet(X2,complement(X1))),
inference(cp,[status(thm)],[t2821,t13]) ).
cnf(t110130,plain,
meet(complement(X1),join(complement(X1),meet(X2,complement(X1)))) = join(complement(X1),meet(X2,complement(X1))),
inference(step,[status(thm)],[t2822,t23]) ).
cnf(t110131,plain,
meet(complement(X1),complement(X1)) = join(complement(X1),meet(X2,complement(X1))),
inference(step,[status(thm)],[t110130,t2821]) ).
cnf(t110132,plain,
complement(X1) = join(complement(X1),meet(X2,complement(X1))),
inference(step,[status(thm)],[t110131,t13]) ).
cnf(t2892,plain,
join(complement(X1),meet(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t110132]) ).
cnf(t6505,plain,
zero = meet(join(zero,meet(X1,X2)),complement(join(X2,complement(X3)))),
inference(cp,[status(thm)],[t6456,t2892]) ).
cnf(t6623,plain,
meet(join(zero,meet(X1,X2)),complement(join(X2,complement(X3)))) = zero,
inference(orient,[status(thm)],[t6505]) ).
cnf(t6664,plain,
zero = meet(join(zero,meet(X1,X2)),complement(join(X2,zero))),
inference(cp,[status(thm)],[t6623,t149]) ).
cnf(t110285,plain,
zero = meet(join(zero,meet(X1,X2)),complement(X2)),
inference(step,[status(thm)],[t6664,t100]) ).
cnf(t110286,plain,
zero = meet(complement(X2),join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t110285,t23]) ).
cnf(t6698,plain,
meet(complement(X1),join(zero,meet(X2,X1))) = zero,
inference(orient,[status(thm)],[t110286]) ).
cnf(t6725,plain,
zero = meet(complement(meet(X1,join(X2,X3))),join(zero,meet(X2,X1))),
inference(cp,[status(thm)],[t6698,t175]) ).
cnf(t110394,plain,
zero = meet(join(zero,meet(X2,X1)),complement(meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t6725,t23]) ).
cnf(t110395,plain,
zero = meet(join(zero,meet(X1,X2)),complement(meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t110394,t23]) ).
cnf(t9996,plain,
meet(join(zero,meet(X1,X2)),complement(meet(X1,join(X2,X3)))) = zero,
inference(orient,[status(thm)],[t110395]) ).
cnf(t11180,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,meet(join(join(X1,X2),X4),one))),
inference(cp,[status(thm)],[t4466,t11159]) ).
cnf(t110443,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,join(join(X1,X2),X4))),
inference(step,[status(thm)],[t11180,t105]) ).
cnf(t110444,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,join(X4,join(X1,X2)))),
inference(step,[status(thm)],[t110443,t69]) ).
cnf(t110445,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,join(X2,join(X4,X1)))),
inference(step,[status(thm)],[t110444,t74]) ).
cnf(t110446,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,join(X1,join(X2,X4)))),
inference(step,[status(thm)],[t110445,t74]) ).
cnf(t110447,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(join(X2,X4),X3))),
inference(step,[status(thm)],[t110446,t74]) ).
cnf(t110448,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X3,join(X2,X4)))),
inference(step,[status(thm)],[t110447,t69]) ).
cnf(t110449,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,join(X4,X3)))),
inference(step,[status(thm)],[t110448,t74]) ).
cnf(t110450,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,join(X3,X4)))),
inference(step,[status(thm)],[t110449,t69]) ).
cnf(t13602,plain,
meet(join(X1,X2),join(X1,join(X2,join(X3,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t110450]) ).
cnf(t200,plain,
join(X1,join(join(X2,meet(X1,X3)),X4)) = join(X4,join(X1,X2)),
inference(cp,[status(thm)],[t74,t189]) ).
cnf(t109870,plain,
join(X1,join(X4,join(X2,meet(X1,X3)))) = join(X4,join(X1,X2)),
inference(step,[status(thm)],[t200,t69]) ).
cnf(t109871,plain,
join(X1,join(X2,join(meet(X1,X3),X4))) = join(X4,join(X1,X2)),
inference(step,[status(thm)],[t109870,t74]) ).
cnf(t109872,plain,
join(X1,join(X2,join(X4,meet(X1,X3)))) = join(X4,join(X1,X2)),
inference(step,[status(thm)],[t109871,t69]) ).
cnf(t109873,plain,
join(X1,join(X2,join(X4,meet(X1,X3)))) = join(X2,join(X4,X1)),
inference(step,[status(thm)],[t109872,t74]) ).
cnf(t109874,plain,
join(X1,join(X2,join(X4,meet(X1,X3)))) = join(X1,join(X2,X4)),
inference(step,[status(thm)],[t109873,t74]) ).
cnf(t305,plain,
join(X1,join(X2,join(X3,meet(X1,X4)))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t109874]) ).
cnf(t13641,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(cp,[status(thm)],[t13602,t305]) ).
cnf(t13736,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t13641]) ).
cnf(t13789,plain,
one = join(join(X1,join(X2,X3)),complement(join(X1,X2))),
inference(cp,[status(thm)],[t12667,t13736]) ).
cnf(t110451,plain,
one = join(complement(join(X1,X2)),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t13789,t69]) ).
cnf(t110452,plain,
one = join(join(X2,X3),join(complement(join(X1,X2)),X1)),
inference(step,[status(thm)],[t110451,t74]) ).
cnf(t110453,plain,
one = join(X1,join(join(X2,X3),complement(join(X1,X2)))),
inference(step,[status(thm)],[t110452,t74]) ).
cnf(t13862,plain,
join(X1,join(join(X2,X3),complement(join(X1,X2)))) = one,
inference(orient,[status(thm)],[t110453]) ).
cnf(t13866,plain,
one = join(X1,join(join(X2,X3),complement(join(X1,X3)))),
inference(cp,[status(thm)],[t13862,t69]) ).
cnf(t13926,plain,
join(X1,join(join(X2,X3),complement(join(X1,X3)))) = one,
inference(orient,[status(thm)],[t13866]) ).
cnf(t13933,plain,
one = join(X1,join(X2,complement(join(X1,meet(X2,X3))))),
inference(cp,[status(thm)],[t13926,t16]) ).
cnf(t13985,plain,
join(X1,join(X2,complement(join(X1,meet(X2,X3))))) = one,
inference(orient,[status(thm)],[t13933]) ).
cnf(t13986,plain,
one = join(X1,join(complement(join(X2,meet(X1,X3))),X2)),
inference(cp,[status(thm)],[t13985,t74]) ).
cnf(t110454,plain,
one = join(X1,join(X2,complement(join(X2,meet(X1,X3))))),
inference(step,[status(thm)],[t13986,t69]) ).
cnf(t14015,plain,
join(X1,join(X2,complement(join(X2,meet(X1,X3))))) = one,
inference(orient,[status(thm)],[t110454]) ).
cnf(t359,plain,
meet(X1,complement(X1)) = meet(X1,join(zero,meet(complement(X1),join(X1,X2)))),
inference(cp,[status(thm)],[t352,t62]) ).
cnf(t109880,plain,
zero = meet(X1,join(zero,meet(complement(X1),join(X1,X2)))),
inference(step,[status(thm)],[t359,t62]) ).
cnf(t392,plain,
meet(X1,join(zero,meet(complement(X1),join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t109880]) ).
cnf(t396,plain,
zero = meet(X1,join(zero,meet(complement(X1),one))),
inference(cp,[status(thm)],[t392,t228]) ).
cnf(t109881,plain,
zero = meet(X1,join(zero,complement(X1))),
inference(step,[status(thm)],[t396,t105]) ).
cnf(t415,plain,
meet(X1,join(zero,complement(X1))) = zero,
inference(orient,[status(thm)],[t109881]) ).
cnf(t416,plain,
join(zero,complement(X1)) = ifeq(zero,zero,ifeq(join(X1,join(zero,complement(X1))),one,complement(X1),join(zero,complement(X1))),join(zero,complement(X1))),
inference(cp,[status(thm)],[t18,t415]) ).
cnf(t109882,plain,
join(zero,complement(X1)) = ifeq(join(X1,join(zero,complement(X1))),one,complement(X1),join(zero,complement(X1))),
inference(step,[status(thm)],[t416,t17]) ).
cnf(t109883,plain,
join(zero,complement(X1)) = ifeq(one,one,complement(X1),join(zero,complement(X1))),
inference(step,[status(thm)],[t109882,t168]) ).
cnf(t109884,plain,
join(zero,complement(X1)) = complement(X1),
inference(step,[status(thm)],[t109883,t17]) ).
cnf(t425,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t109884]) ).
cnf(t14017,plain,
one = join(X1,complement(join(zero,meet(X1,X2)))),
inference(cp,[status(thm)],[t14015,t425]) ).
cnf(t14054,plain,
join(X1,complement(join(zero,meet(X1,X2)))) = one,
inference(orient,[status(thm)],[t14017]) ).
cnf(t14268,plain,
one = join(meet(X1,X2),complement(join(zero,meet(X1,X2)))),
inference(cp,[status(thm)],[t14054,t14210]) ).
cnf(t14640,plain,
join(meet(X1,X2),complement(join(zero,meet(X1,X2)))) = one,
inference(orient,[status(thm)],[t14268]) ).
cnf(t14664,plain,
meet(X1,X2) = ifeq(meet(meet(X1,X2),complement(join(zero,meet(X1,X2)))),zero,ifeq(one,one,complement(complement(join(zero,meet(X1,X2)))),meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t1005,t14640]) ).
cnf(t110466,plain,
meet(X1,X2) = ifeq(zero,zero,ifeq(one,one,complement(complement(join(zero,meet(X1,X2)))),meet(X1,X2)),meet(X1,X2)),
inference(step,[status(thm)],[t14664,t4777]) ).
cnf(t110467,plain,
meet(X1,X2) = ifeq(one,one,complement(complement(join(zero,meet(X1,X2)))),meet(X1,X2)),
inference(step,[status(thm)],[t110466,t17]) ).
cnf(t110468,plain,
meet(X1,X2) = complement(complement(join(zero,meet(X1,X2)))),
inference(step,[status(thm)],[t110467,t17]) ).
cnf(t110469,plain,
meet(X1,X2) = join(zero,meet(X1,X2)),
inference(step,[status(thm)],[t110468,t1052]) ).
cnf(t14680,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t110469]) ).
cnf(t110477,plain,
meet(meet(X1,X2),complement(meet(X1,join(X2,X3)))) = zero,
inference(step,[status(thm)],[t9996,t14680]) ).
cnf(t14748,plain,
meet(meet(X1,X2),complement(meet(X1,join(X2,X3)))) = zero,
inference(rw,[status(thm)],[t110477]) ).
cnf(t15013,plain,
meet(meet(X1,X2),complement(meet(X1,join(X2,X3)))) = zero,
inference(orient,[status(thm)],[t14748]) ).
cnf(t19721,plain,
one = join(join(meet(X1,X2),X3),complement(join(X3,zero))),
inference(cp,[status(thm)],[t19631,t15013]) ).
cnf(t110663,plain,
one = join(complement(join(X3,zero)),join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t19721,t69]) ).
cnf(t110664,plain,
one = join(X3,join(complement(join(X3,zero)),meet(X1,X2))),
inference(step,[status(thm)],[t110663,t74]) ).
cnf(t110665,plain,
one = join(X3,join(meet(X1,X2),complement(join(X3,zero)))),
inference(step,[status(thm)],[t110664,t69]) ).
cnf(t110666,plain,
one = join(X3,join(meet(X1,X2),complement(X3))),
inference(step,[status(thm)],[t110665,t100]) ).
cnf(t110667,plain,
one = join(X3,join(complement(X3),meet(X1,X2))),
inference(step,[status(thm)],[t110666,t69]) ).
cnf(t19790,plain,
join(X1,join(complement(X1),meet(X2,X3))) = one,
inference(orient,[status(thm)],[t110667]) ).
cnf(t111016,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = ifeq(one,one,complement(X1),join(complement(X1),meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t111015,t19790]) ).
cnf(t111017,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = complement(X1),
inference(step,[status(thm)],[t111016,t17]) ).
cnf(t46316,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = complement(X1),
inference(orient,[status(thm)],[t111017]) ).
cnf(t46317,plain,
complement(complement(X1)) = join(X1,meet(X2,complement(meet(complement(X1),X2)))),
inference(cp,[status(thm)],[t46316,t1052]) ).
cnf(t111018,plain,
X1 = join(X1,meet(X2,complement(meet(complement(X1),X2)))),
inference(step,[status(thm)],[t46317,t1052]) ).
cnf(t111019,plain,
X1 = join(X1,meet(X2,complement(meet(X2,complement(X1))))),
inference(step,[status(thm)],[t111018,t23]) ).
cnf(t46557,plain,
join(X1,meet(X2,complement(meet(X2,complement(X1))))) = X1,
inference(orient,[status(thm)],[t111019]) ).
cnf(t2787,plain,
complement(X1) = meet(complement(X1),join(X2,complement(X1))),
inference(cp,[status(thm)],[t645,t2773]) ).
cnf(t2802,plain,
meet(complement(X1),join(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t2787]) ).
cnf(t1066,plain,
zero = meet(complement(X1),join(zero,meet(X2,X1))),
inference(cp,[status(thm)],[t505,t1052]) ).
cnf(t109985,plain,
zero = meet(complement(X1),join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t1066,t23]) ).
cnf(t1081,plain,
meet(complement(X1),join(zero,meet(X1,X2))) = zero,
inference(orient,[status(thm)],[t109985]) ).
cnf(t1648,plain,
meet(complement(X1),join(zero,meet(X1,X2))) = meet(complement(X1),join(zero,meet(join(zero,meet(X1,X2)),X3))),
inference(cp,[status(thm)],[t1605,t1081]) ).
cnf(t110052,plain,
zero = meet(complement(X1),join(zero,meet(join(zero,meet(X1,X2)),X3))),
inference(step,[status(thm)],[t1648,t1081]) ).
cnf(t110053,plain,
zero = meet(complement(X1),join(zero,meet(X3,join(zero,meet(X1,X2))))),
inference(step,[status(thm)],[t110052,t23]) ).
cnf(t1732,plain,
meet(complement(X1),join(zero,meet(X2,join(zero,meet(X1,X3))))) = zero,
inference(orient,[status(thm)],[t110053]) ).
cnf(t4530,plain,
zero = meet(complement(join(X1,X2)),join(zero,X1)),
inference(cp,[status(thm)],[t1732,t4466]) ).
cnf(t110207,plain,
zero = meet(join(zero,X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t4530,t23]) ).
cnf(t110208,plain,
zero = meet(join(X1,zero),complement(join(X1,X2))),
inference(step,[status(thm)],[t110207,t69]) ).
cnf(t110209,plain,
zero = meet(X1,complement(join(X1,X2))),
inference(step,[status(thm)],[t110208,t100]) ).
cnf(t4543,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(orient,[status(thm)],[t110209]) ).
cnf(t36488,plain,
meet(X1,join(complement(join(X1,X2)),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t36371,t4543]) ).
cnf(t110908,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t36488,t69]) ).
cnf(t110909,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t110908,t100]) ).
cnf(t110910,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = zero,
inference(step,[status(thm)],[t110909,t62]) ).
cnf(t36662,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t110910]) ).
cnf(t36680,plain,
join(complement(X1),complement(join(X1,X2))) = ifeq(zero,zero,ifeq(join(X1,join(complement(X1),complement(join(X1,X2)))),one,complement(X1),join(complement(X1),complement(join(X1,X2)))),join(complement(X1),complement(join(X1,X2)))),
inference(cp,[status(thm)],[t18,t36662]) ).
cnf(t110911,plain,
join(complement(X1),complement(join(X1,X2))) = ifeq(join(X1,join(complement(X1),complement(join(X1,X2)))),one,complement(X1),join(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t36680,t17]) ).
cnf(t19799,plain,
one = join(X1,join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t19790,t2747]) ).
cnf(t19833,plain,
join(X1,join(complement(X1),complement(X2))) = one,
inference(orient,[status(thm)],[t19799]) ).
cnf(t110912,plain,
join(complement(X1),complement(join(X1,X2))) = ifeq(one,one,complement(X1),join(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t110911,t19833]) ).
cnf(t110913,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(step,[status(thm)],[t110912,t17]) ).
cnf(t36763,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t110913]) ).
cnf(t36786,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t2802,t36763]) ).
cnf(t110916,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t36786,t23]) ).
cnf(t37029,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t110916]) ).
cnf(t37143,plain,
zero = meet(X1,complement(join(X2,meet(X1,complement(X2))))),
inference(cp,[status(thm)],[t5675,t37029]) ).
cnf(t38193,plain,
meet(X1,complement(join(X2,meet(X1,complement(X2))))) = zero,
inference(orient,[status(thm)],[t37143]) ).
cnf(t38195,plain,
zero = meet(X1,complement(join(complement(X2),meet(X1,X2)))),
inference(cp,[status(thm)],[t38193,t1052]) ).
cnf(t38807,plain,
meet(X1,complement(join(complement(X2),meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t38195]) ).
cnf(t46561,plain,
join(complement(X1),meet(X2,X1)) = join(join(complement(X1),meet(X2,X1)),meet(X2,complement(zero))),
inference(cp,[status(thm)],[t46557,t38807]) ).
cnf(t111082,plain,
join(complement(X1),meet(X2,X1)) = join(join(complement(X1),meet(X2,X1)),meet(X2,one)),
inference(step,[status(thm)],[t46561,t154]) ).
cnf(t111083,plain,
join(complement(X1),meet(X2,X1)) = join(join(complement(X1),meet(X2,X1)),X2),
inference(step,[status(thm)],[t111082,t105]) ).
cnf(t111084,plain,
join(complement(X1),meet(X1,X2)) = join(join(complement(X1),meet(X2,X1)),X2),
inference(step,[status(thm)],[t111083,t23]) ).
cnf(t111085,plain,
join(complement(X1),meet(X1,X2)) = join(X2,join(complement(X1),meet(X2,X1))),
inference(step,[status(thm)],[t111084,t69]) ).
cnf(t111086,plain,
join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
inference(step,[status(thm)],[t111085,t189]) ).
cnf(t52597,plain,
join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t111086]) ).
cnf(t52897,plain,
meet(X1,X2) = ifeq(meet(X1,meet(X2,complement(X1))),zero,ifeq(join(X2,complement(X1)),one,complement(complement(X1)),meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t3697,t52597]) ).
cnf(t111188,plain,
meet(X1,X2) = ifeq(zero,zero,ifeq(join(X2,complement(X1)),one,complement(complement(X1)),meet(X1,X2)),meet(X1,X2)),
inference(step,[status(thm)],[t52897,t159]) ).
cnf(t111189,plain,
meet(X1,X2) = ifeq(join(X2,complement(X1)),one,complement(complement(X1)),meet(X1,X2)),
inference(step,[status(thm)],[t111188,t17]) ).
cnf(t111190,plain,
meet(X1,X2) = ifeq(join(X2,complement(X1)),one,X1,meet(X1,X2)),
inference(step,[status(thm)],[t111189,t1052]) ).
cnf(t62452,plain,
ifeq(join(X1,complement(X2)),one,X2,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t111190]) ).
cnf(t12694,plain,
one = join(meet(X1,join(X2,X3)),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t12667,t175]) ).
cnf(t110425,plain,
one = join(complement(meet(X2,X1)),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t12694,t69]) ).
cnf(t110426,plain,
one = join(complement(meet(X1,X2)),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t110425,t23]) ).
cnf(t12776,plain,
join(complement(meet(X1,X2)),meet(X1,join(X2,X3))) = one,
inference(orient,[status(thm)],[t110426]) ).
cnf(t12872,plain,
one = join(complement(meet(X1,X2)),meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t12776,t112]) ).
cnf(t110584,plain,
one = join(complement(meet(X1,X2)),meet(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t12872,t69]) ).
cnf(t18116,plain,
join(complement(meet(X1,X2)),meet(X1,join(X3,meet(X1,X2)))) = one,
inference(orient,[status(thm)],[t110584]) ).
cnf(t18130,plain,
one = join(complement(meet(X1,X2)),meet(X2,join(X3,meet(X2,X1)))),
inference(cp,[status(thm)],[t18116,t23]) ).
cnf(t110758,plain,
one = join(complement(meet(X1,X2)),meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t18130,t23]) ).
cnf(t24265,plain,
join(complement(meet(X1,X2)),meet(X2,join(X3,meet(X1,X2)))) = one,
inference(orient,[status(thm)],[t110758]) ).
cnf(t12924,plain,
one = join(complement(meet(X1,X2)),meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t12776,t23]) ).
cnf(t13211,plain,
join(complement(meet(X1,X2)),meet(X2,join(X1,X3))) = one,
inference(orient,[status(thm)],[t12924]) ).
cnf(t24321,plain,
one = join(complement(meet(X1,join(X2,X3))),meet(join(X2,X3),one)),
inference(cp,[status(thm)],[t24265,t13211]) ).
cnf(t110759,plain,
one = join(complement(meet(X1,join(X2,X3))),join(X2,X3)),
inference(step,[status(thm)],[t24321,t105]) ).
cnf(t110760,plain,
one = join(X3,join(complement(meet(X1,join(X2,X3))),X2)),
inference(step,[status(thm)],[t110759,t74]) ).
cnf(t110761,plain,
one = join(X2,join(X3,complement(meet(X1,join(X2,X3))))),
inference(step,[status(thm)],[t110760,t74]) ).
cnf(t24428,plain,
join(X1,join(X2,complement(meet(X3,join(X1,X2))))) = one,
inference(orient,[status(thm)],[t110761]) ).
cnf(t36764,plain,
complement(complement(X1)) = join(X1,complement(join(complement(X1),X2))),
inference(cp,[status(thm)],[t36763,t1052]) ).
cnf(t110914,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t36764,t1052]) ).
cnf(t110915,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(step,[status(thm)],[t110914,t69]) ).
cnf(t36882,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t110915]) ).
cnf(t36913,plain,
complement(join(X1,complement(X2))) = meet(complement(join(X1,complement(X2))),X2),
inference(cp,[status(thm)],[t2802,t36882]) ).
cnf(t110917,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t36913,t23]) ).
cnf(t37165,plain,
meet(X1,complement(join(X2,complement(X1)))) = complement(join(X2,complement(X1))),
inference(orient,[status(thm)],[t110917]) ).
cnf(t37169,plain,
complement(join(X1,complement(complement(X2)))) = meet(complement(X2),complement(join(X1,X2))),
inference(cp,[status(thm)],[t37165,t1052]) ).
cnf(t110920,plain,
complement(join(X1,X2)) = meet(complement(X2),complement(join(X1,X2))),
inference(step,[status(thm)],[t37169,t1052]) ).
cnf(t37292,plain,
meet(complement(X1),complement(join(X2,X1))) = complement(join(X2,X1)),
inference(orient,[status(thm)],[t110920]) ).
cnf(t37301,plain,
complement(join(X1,meet(X1,X2))) = meet(complement(meet(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t37292,t16]) ).
cnf(t110925,plain,
complement(X1) = meet(complement(meet(X1,X2)),complement(X1)),
inference(step,[status(thm)],[t37301,t16]) ).
cnf(t110926,plain,
complement(X1) = meet(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t110925,t23]) ).
cnf(t37594,plain,
meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t110926]) ).
cnf(t37618,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t2892,t37594]) ).
cnf(t110927,plain,
complement(meet(X1,X2)) = join(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t37618,t69]) ).
cnf(t37715,plain,
join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t110927]) ).
cnf(t37821,plain,
one = join(X1,complement(meet(X2,join(X1,complement(X2))))),
inference(cp,[status(thm)],[t24428,t37715]) ).
cnf(t38594,plain,
join(X1,complement(meet(X2,join(X1,complement(X2))))) = one,
inference(orient,[status(thm)],[t37821]) ).
cnf(t38596,plain,
one = join(X1,complement(meet(complement(X2),join(X1,X2)))),
inference(cp,[status(thm)],[t38594,t1052]) ).
cnf(t39079,plain,
join(X1,complement(meet(complement(X2),join(X1,X2)))) = one,
inference(orient,[status(thm)],[t38596]) ).
cnf(t62456,plain,
meet(meet(complement(X1),join(X2,X1)),X2) = ifeq(one,one,meet(complement(X1),join(X2,X1)),meet(meet(complement(X1),join(X2,X1)),X2)),
inference(cp,[status(thm)],[t62452,t39079]) ).
cnf(t111191,plain,
meet(X2,meet(complement(X1),join(X2,X1))) = ifeq(one,one,meet(complement(X1),join(X2,X1)),meet(meet(complement(X1),join(X2,X1)),X2)),
inference(step,[status(thm)],[t62456,t23]) ).
cnf(t111192,plain,
meet(X2,complement(X1)) = ifeq(one,one,meet(complement(X1),join(X2,X1)),meet(meet(complement(X1),join(X2,X1)),X2)),
inference(step,[status(thm)],[t111191,t175]) ).
cnf(t111193,plain,
meet(X2,complement(X1)) = meet(complement(X1),join(X2,X1)),
inference(step,[status(thm)],[t111192,t17]) ).
cnf(t111194,plain,
meet(X2,complement(X1)) = meet(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t111193,t69]) ).
cnf(t62675,plain,
meet(complement(X1),join(X1,X2)) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t111194]) ).
cnf(t62700,plain,
meet(X1,complement(complement(X2))) = meet(X2,join(complement(X2),X1)),
inference(cp,[status(thm)],[t62675,t1052]) ).
cnf(t111196,plain,
meet(X1,X2) = meet(X2,join(complement(X2),X1)),
inference(step,[status(thm)],[t62700,t1052]) ).
cnf(t111197,plain,
meet(X1,X2) = meet(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t111196,t69]) ).
cnf(t63062,plain,
meet(X1,join(X2,complement(X1))) = meet(X2,X1),
inference(orient,[status(thm)],[t111197]) ).
cnf(t46442,plain,
complement(join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(complement(meet(X2,complement(meet(X1,X2)))),complement(complement(X1))),
inference(cp,[status(thm)],[t37292,t46316]) ).
cnf(t111020,plain,
complement(complement(X1)) = meet(complement(meet(X2,complement(meet(X1,X2)))),complement(complement(X1))),
inference(step,[status(thm)],[t46442,t46316]) ).
cnf(t111021,plain,
X1 = meet(complement(meet(X2,complement(meet(X1,X2)))),complement(complement(X1))),
inference(step,[status(thm)],[t111020,t1052]) ).
cnf(t111022,plain,
X1 = meet(complement(complement(X1)),complement(meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t111021,t23]) ).
cnf(t111023,plain,
X1 = meet(X1,complement(meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t111022,t1052]) ).
cnf(t46747,plain,
meet(X1,complement(meet(X2,complement(meet(X1,X2))))) = X1,
inference(orient,[status(thm)],[t111023]) ).
cnf(t46886,plain,
one = join(complement(meet(X1,complement(meet(X2,X1)))),complement(X2)),
inference(cp,[status(thm)],[t12667,t46747]) ).
cnf(t111057,plain,
one = join(complement(X2),complement(meet(X1,complement(meet(X2,X1))))),
inference(step,[status(thm)],[t46886,t69]) ).
cnf(t111058,plain,
one = join(complement(X2),complement(meet(X1,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t111057,t23]) ).
cnf(t48461,plain,
join(complement(X1),complement(meet(X2,complement(meet(X2,X1))))) = one,
inference(orient,[status(thm)],[t111058]) ).
cnf(t48462,plain,
one = join(X1,complement(meet(X2,complement(meet(X2,complement(X1)))))),
inference(cp,[status(thm)],[t48461,t1052]) ).
cnf(t50102,plain,
join(X1,complement(meet(X2,complement(meet(X2,complement(X1)))))) = one,
inference(orient,[status(thm)],[t48462]) ).
cnf(t63066,plain,
meet(X1,meet(X2,complement(meet(X2,complement(X1))))) = meet(meet(X2,complement(meet(X2,complement(X1)))),one),
inference(cp,[status(thm)],[t63062,t50102]) ).
cnf(t37305,plain,
complement(join(complement(X1),meet(X2,complement(X1)))) = meet(complement(meet(X2,complement(X1))),complement(complement(X1))),
inference(cp,[status(thm)],[t37292,t2892]) ).
cnf(t110921,plain,
complement(complement(X1)) = meet(complement(meet(X2,complement(X1))),complement(complement(X1))),
inference(step,[status(thm)],[t37305,t2892]) ).
cnf(t110922,plain,
X1 = meet(complement(meet(X2,complement(X1))),complement(complement(X1))),
inference(step,[status(thm)],[t110921,t1052]) ).
cnf(t110923,plain,
X1 = meet(complement(complement(X1)),complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t110922,t23]) ).
cnf(t110924,plain,
X1 = meet(X1,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t110923,t1052]) ).
cnf(t37440,plain,
meet(X1,complement(meet(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t110924]) ).
cnf(t37537,plain,
meet(X1,meet(complement(meet(X2,complement(X1))),X3)) = meet(X1,meet(X3,join(X1,meet(complement(meet(X2,complement(X1))),X4)))),
inference(cp,[status(thm)],[t1794,t37440]) ).
cnf(t110954,plain,
meet(X1,meet(X3,complement(meet(X2,complement(X1))))) = meet(X1,meet(X3,join(X1,meet(complement(meet(X2,complement(X1))),X4)))),
inference(step,[status(thm)],[t37537,t23]) ).
cnf(t110955,plain,
meet(X1,meet(X3,complement(meet(X2,complement(X1))))) = meet(X1,X3),
inference(step,[status(thm)],[t110954,t175]) ).
cnf(t39913,plain,
meet(X1,meet(X2,complement(meet(X3,complement(X1))))) = meet(X1,X2),
inference(orient,[status(thm)],[t110955]) ).
cnf(t111201,plain,
meet(X1,X2) = meet(meet(X2,complement(meet(X2,complement(X1)))),one),
inference(step,[status(thm)],[t63066,t39913]) ).
cnf(t111202,plain,
meet(X1,X2) = meet(X2,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t111201,t105]) ).
cnf(t63880,plain,
meet(X1,complement(meet(X1,complement(X2)))) = meet(X2,X1),
inference(orient,[status(thm)],[t111202]) ).
cnf(t63931,plain,
meet(complement(X1),X2) = meet(X2,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t63880,t1052]) ).
cnf(t111212,plain,
meet(X2,complement(X1)) = meet(X2,complement(meet(X2,X1))),
inference(step,[status(thm)],[t63931,t23]) ).
cnf(t111213,plain,
meet(X2,complement(X1)) = meet(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t111212,t23]) ).
cnf(t64762,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t111213]) ).
cnf(t64890,plain,
meet(X1,complement(X2)) = meet(X1,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t64762,t23]) ).
cnf(t65245,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t64890]) ).
cnf(t65251,plain,
meet(X1,complement(join(X2,complement(X1)))) = meet(X1,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t65245,t63062]) ).
cnf(t111219,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(meet(X2,X1))),
inference(step,[status(thm)],[t65251,t37165]) ).
cnf(t111220,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t111219,t64762]) ).
cnf(t65498,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t111220]) ).
cnf(t65547,plain,
join(X1,complement(X2)) = complement(meet(X2,complement(X1))),
inference(cp,[status(thm)],[t1052,t65498]) ).
cnf(t65976,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t65547]) ).
cnf(t66022,plain,
join(meet(X1,complement(X2)),complement(X3)) = complement(meet(X3,join(X2,complement(X1)))),
inference(cp,[status(thm)],[t65976,t65976]) ).
cnf(t111309,plain,
join(complement(X3),meet(X1,complement(X2))) = complement(meet(X3,join(X2,complement(X1)))),
inference(step,[status(thm)],[t66022,t69]) ).
cnf(t71183,plain,
complement(meet(X1,join(X2,complement(X3)))) = join(complement(X1),meet(X3,complement(X2))),
inference(orient,[status(thm)],[t111309]) ).
cnf(t63899,plain,
meet(join(X1,X2),X2) = meet(X2,complement(zero)),
inference(cp,[status(thm)],[t63880,t4777]) ).
cnf(t111203,plain,
meet(X2,join(X1,X2)) = meet(X2,complement(zero)),
inference(step,[status(thm)],[t63899,t23]) ).
cnf(t111204,plain,
meet(X2,join(X1,X2)) = meet(X2,one),
inference(step,[status(thm)],[t111203,t154]) ).
cnf(t111205,plain,
meet(X2,join(X1,X2)) = X2,
inference(step,[status(thm)],[t111204,t105]) ).
cnf(t64153,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t111205]) ).
cnf(t64171,plain,
join(X1,meet(X2,X3)) = meet(join(X1,meet(X2,X3)),join(X2,X1)),
inference(cp,[status(thm)],[t64153,t189]) ).
cnf(t111453,plain,
join(X1,meet(X2,X3)) = meet(join(X2,X1),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t64171,t23]) ).
cnf(t111454,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t111453,t69]) ).
cnf(t88007,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t111454]) ).
cnf(t88036,plain,
join(X1,meet(join(X1,X2),X3)) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t88007,t131]) ).
cnf(t111455,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t88036,t23]) ).
cnf(t52792,plain,
join(meet(X1,X2),complement(X3)) = join(complement(X3),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t52597,t26]) ).
cnf(t111158,plain,
join(complement(X3),meet(X1,X2)) = join(complement(X3),meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t52792,t69]) ).
cnf(t59234,plain,
join(complement(X1),meet(X2,meet(X3,X1))) = join(complement(X1),meet(X2,X3)),
inference(orient,[status(thm)],[t111158]) ).
cnf(t62857,plain,
meet(X1,complement(X2)) = meet(complement(X2),join(X1,X2)),
inference(cp,[status(thm)],[t62675,t69]) ).
cnf(t63321,plain,
meet(complement(X1),join(X2,X1)) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t62857]) ).
cnf(t65350,plain,
meet(complement(X1),complement(join(X2,X1))) = meet(complement(X1),complement(meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t65245,t63321]) ).
cnf(t111230,plain,
complement(join(X2,X1)) = meet(complement(X1),complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t65350,t37292]) ).
cnf(t111231,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t111230,t69]) ).
cnf(t111232,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(X2)),
inference(step,[status(thm)],[t111231,t64762]) ).
cnf(t65747,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t111232]) ).
cnf(t65782,plain,
join(complement(complement(X1)),meet(X2,complement(X3))) = join(complement(complement(X1)),meet(X2,complement(join(X3,X1)))),
inference(cp,[status(thm)],[t59234,t65747]) ).
cnf(t111412,plain,
join(X1,meet(X2,complement(X3))) = join(complement(complement(X1)),meet(X2,complement(join(X3,X1)))),
inference(step,[status(thm)],[t65782,t1052]) ).
cnf(t111413,plain,
join(X1,meet(X2,complement(X3))) = join(X1,meet(X2,complement(join(X3,X1)))),
inference(step,[status(thm)],[t111412,t1052]) ).
cnf(t111414,plain,
join(X1,meet(X2,complement(X3))) = join(X1,meet(X2,complement(join(X1,X3)))),
inference(step,[status(thm)],[t111413,t69]) ).
cnf(t83217,plain,
join(X1,meet(X2,complement(join(X1,X3)))) = join(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t111414]) ).
cnf(t52791,plain,
join(X1,complement(X2)) = join(complement(X2),meet(X1,X2)),
inference(cp,[status(thm)],[t52597,t23]) ).
cnf(t53252,plain,
join(complement(X1),meet(X2,X1)) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t52791]) ).
cnf(t65766,plain,
join(complement(X1),complement(complement(X2))) = join(complement(complement(X2)),complement(join(X1,X2))),
inference(cp,[status(thm)],[t53252,t65747]) ).
cnf(t111249,plain,
join(complement(X1),X2) = join(complement(complement(X2)),complement(join(X1,X2))),
inference(step,[status(thm)],[t65766,t1052]) ).
cnf(t111250,plain,
join(complement(X1),X2) = join(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t111249,t1052]) ).
cnf(t111251,plain,
join(X2,complement(X1)) = join(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t111250,t69]) ).
cnf(t66375,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t111251]) ).
cnf(t66470,plain,
join(X1,complement(X2)) = join(X1,complement(join(X1,X2))),
inference(cp,[status(thm)],[t66375,t69]) ).
cnf(t66575,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t66470]) ).
cnf(t83242,plain,
join(X1,meet(X2,complement(complement(join(X1,X3))))) = join(X1,meet(X2,complement(join(X1,complement(X3))))),
inference(cp,[status(thm)],[t83217,t66575]) ).
cnf(t111415,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,complement(join(X1,complement(X3))))),
inference(step,[status(thm)],[t83242,t1052]) ).
cnf(t111416,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,complement(complement(X3)))),
inference(step,[status(thm)],[t111415,t83217]) ).
cnf(t111417,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t111416,t1052]) ).
cnf(t83468,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t111417]) ).
cnf(t111456,plain,
join(X1,meet(X3,X2)) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t111455,t83468]) ).
cnf(t111457,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t111456,t23]) ).
cnf(t66005,plain,
join(join(X1,complement(X2)),complement(X3)) = complement(meet(X3,meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t65976,t65498]) ).
cnf(t111302,plain,
join(complement(X3),join(X1,complement(X2))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t66005,t69]) ).
cnf(t111303,plain,
join(complement(X2),join(complement(X3),X1)) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t111302,t74]) ).
cnf(t111304,plain,
join(X1,join(complement(X2),complement(X3))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t111303,t74]) ).
cnf(t66006,plain,
join(complement(X1),complement(X2)) = complement(meet(X2,X1)),
inference(cp,[status(thm)],[t65976,t1052]) ).
cnf(t111245,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t66006,t23]) ).
cnf(t66170,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t111245]) ).
cnf(t111305,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t111304,t66170]) ).
cnf(t111306,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X2,meet(complement(X1),X3))),
inference(step,[status(thm)],[t111305,t26]) ).
cnf(t111307,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X2,meet(X3,complement(X1)))),
inference(step,[status(thm)],[t111306,t23]) ).
cnf(t70985,plain,
complement(meet(X1,meet(X2,complement(X3)))) = join(X3,complement(meet(X1,X2))),
inference(orient,[status(thm)],[t111307]) ).
cnf(t71072,plain,
meet(X1,complement(meet(X2,complement(X3)))) = meet(X1,join(X3,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t65245,t70985]) ).
cnf(t111435,plain,
meet(X1,join(X3,complement(X2))) = meet(X1,join(X3,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t71072,t65976]) ).
cnf(t86170,plain,
meet(X1,join(X2,complement(meet(X1,X3)))) = meet(X1,join(X2,complement(X3))),
inference(orient,[status(thm)],[t111435]) ).
cnf(t86201,plain,
meet(X1,join(X2,complement(complement(meet(X1,X3))))) = meet(X1,join(X2,complement(meet(X1,complement(X3))))),
inference(cp,[status(thm)],[t86170,t65245]) ).
cnf(t111438,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,complement(meet(X1,complement(X3))))),
inference(step,[status(thm)],[t86201,t1052]) ).
cnf(t111439,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,complement(complement(X3)))),
inference(step,[status(thm)],[t111438,t86170]) ).
cnf(t111440,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t111439,t1052]) ).
cnf(t86451,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t111440]) ).
cnf(t111458,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t111457,t86451]) ).
cnf(t88358,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t111458]) ).
cnf(t88605,plain,
join(complement(X1),meet(X2,meet(X3,X1))) = meet(join(complement(X1),X2),join(X3,complement(X1))),
inference(cp,[status(thm)],[t88358,t53252]) ).
cnf(t111633,plain,
join(complement(X1),meet(X2,X3)) = meet(join(complement(X1),X2),join(X3,complement(X1))),
inference(step,[status(thm)],[t88605,t59234]) ).
cnf(t111634,plain,
join(complement(X1),meet(X2,X3)) = meet(join(X3,complement(X1)),join(complement(X1),X2)),
inference(step,[status(thm)],[t111633,t23]) ).
cnf(t111635,plain,
join(complement(X1),meet(X2,X3)) = meet(join(X3,complement(X1)),join(X2,complement(X1))),
inference(step,[status(thm)],[t111634,t69]) ).
cnf(t111636,plain,
join(complement(X1),meet(X2,X3)) = meet(join(X2,complement(X1)),join(X3,complement(X1))),
inference(step,[status(thm)],[t111635,t23]) ).
cnf(t106440,plain,
meet(join(X1,complement(X2)),join(X3,complement(X2))) = join(complement(X2),meet(X1,X3)),
inference(orient,[status(thm)],[t111636]) ).
cnf(t106670,plain,
join(complement(join(X1,complement(X2))),meet(X2,complement(X3))) = complement(join(complement(X2),meet(X1,X3))),
inference(cp,[status(thm)],[t71183,t106440]) ).
cnf(t111650,plain,
join(meet(X2,complement(X3)),complement(join(X1,complement(X2)))) = complement(join(complement(X2),meet(X1,X3))),
inference(step,[status(thm)],[t106670,t69]) ).
cnf(t111651,plain,
join(meet(X2,complement(X3)),meet(X2,complement(X1))) = complement(join(complement(X2),meet(X1,X3))),
inference(step,[status(thm)],[t111650,t65498]) ).
cnf(t111652,plain,
join(meet(X2,complement(X1)),meet(X2,complement(X3))) = complement(join(complement(X2),meet(X1,X3))),
inference(step,[status(thm)],[t111651,t69]) ).
cnf(t7798,plain,
zero = meet(one,complement(join(X1,meet(one,join(complement(X1),X2))))),
inference(cp,[status(thm)],[t7788,t96]) ).
cnf(t110309,plain,
zero = complement(join(X1,meet(one,join(complement(X1),X2)))),
inference(step,[status(thm)],[t7798,t2747]) ).
cnf(t110310,plain,
zero = complement(join(X1,meet(one,join(X2,complement(X1))))),
inference(step,[status(thm)],[t110309,t69]) ).
cnf(t7847,plain,
complement(join(X1,meet(one,join(X2,complement(X1))))) = zero,
inference(orient,[status(thm)],[t110310]) ).
cnf(t7851,plain,
one = ifeq(zero,zero,join(X1,meet(one,join(X2,complement(X1)))),one),
inference(cp,[status(thm)],[t1079,t7847]) ).
cnf(t110311,plain,
one = join(X1,meet(one,join(X2,complement(X1)))),
inference(step,[status(thm)],[t7851,t17]) ).
cnf(t7891,plain,
join(X1,meet(one,join(X2,complement(X1)))) = one,
inference(orient,[status(thm)],[t110311]) ).
cnf(t7893,plain,
one = join(complement(X1),meet(one,join(X2,X1))),
inference(cp,[status(thm)],[t7891,t1052]) ).
cnf(t110312,plain,
one = join(complement(X1),meet(one,join(X1,X2))),
inference(step,[status(thm)],[t7893,t69]) ).
cnf(t7914,plain,
join(complement(X1),meet(one,join(X1,X2))) = one,
inference(orient,[status(thm)],[t110312]) ).
cnf(t7930,plain,
complement(X1) = meet(complement(X1),join(X2,meet(join(complement(X1),X3),one))),
inference(cp,[status(thm)],[t4466,t7914]) ).
cnf(t110313,plain,
complement(X1) = meet(complement(X1),join(X2,join(complement(X1),X3))),
inference(step,[status(thm)],[t7930,t105]) ).
cnf(t110314,plain,
complement(X1) = meet(complement(X1),join(X2,join(X3,complement(X1)))),
inference(step,[status(thm)],[t110313,t69]) ).
cnf(t7947,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t110314]) ).
cnf(t36824,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),join(X3,complement(X1))),
inference(cp,[status(thm)],[t7947,t36763]) ).
cnf(t110974,plain,
complement(join(X1,X2)) = meet(join(X3,complement(X1)),complement(join(X1,X2))),
inference(step,[status(thm)],[t36824,t23]) ).
cnf(t42131,plain,
meet(join(X1,complement(X2)),complement(join(X2,X3))) = complement(join(X2,X3)),
inference(orient,[status(thm)],[t110974]) ).
cnf(t66466,plain,
join(meet(X1,X2),complement(complement(X2))) = join(meet(X1,X2),complement(join(X1,complement(X2)))),
inference(cp,[status(thm)],[t66375,t53252]) ).
cnf(t111313,plain,
join(meet(X1,X2),X2) = join(meet(X1,X2),complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t66466,t1052]) ).
cnf(t111314,plain,
join(X2,meet(X1,X2)) = join(meet(X1,X2),complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t111313,t69]) ).
cnf(t111315,plain,
join(X2,meet(X1,X2)) = join(meet(X1,X2),meet(X2,complement(X1))),
inference(step,[status(thm)],[t111314,t65498]) ).
cnf(t71554,plain,
join(meet(X1,X2),meet(X2,complement(X1))) = join(X2,meet(X1,X2)),
inference(orient,[status(thm)],[t111315]) ).
cnf(t71751,plain,
complement(join(meet(X1,X2),meet(X2,complement(X1)))) = meet(join(X3,complement(meet(X1,X2))),complement(join(X2,meet(X1,X2)))),
inference(cp,[status(thm)],[t42131,t71554]) ).
cnf(t65554,plain,
meet(join(X1,complement(X2)),complement(X3)) = complement(join(X3,meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t65498,t65498]) ).
cnf(t111291,plain,
meet(complement(X3),join(X1,complement(X2))) = complement(join(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t65554,t23]) ).
cnf(t70582,plain,
complement(join(X1,meet(X2,complement(X3)))) = meet(complement(X1),join(X3,complement(X2))),
inference(orient,[status(thm)],[t111291]) ).
cnf(t111316,plain,
meet(complement(meet(X1,X2)),join(X1,complement(X2))) = meet(join(X3,complement(meet(X1,X2))),complement(join(X2,meet(X1,X2)))),
inference(step,[status(thm)],[t71751,t70582]) ).
cnf(t111317,plain,
meet(join(X1,complement(X2)),complement(meet(X1,X2))) = meet(join(X3,complement(meet(X1,X2))),complement(join(X2,meet(X1,X2)))),
inference(step,[status(thm)],[t111316,t23]) ).
cnf(t37309,plain,
meet(complement(X1),complement(join(X2,X1))) = meet(complement(join(X2,X1)),join(complement(X1),X3)),
inference(cp,[status(thm)],[t14315,t37292]) ).
cnf(t42312,plain,
meet(join(X1,complement(X2)),complement(join(X3,X2))) = complement(join(X3,X2)),
inference(orient,[status(thm)],[t37309]) ).
cnf(t111318,plain,
meet(join(X1,complement(X2)),complement(meet(X1,X2))) = complement(join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t111317,t42312]) ).
cnf(t62781,plain,
meet(join(X1,meet(X2,X3)),complement(X2)) = meet(complement(X2),join(X2,X1)),
inference(cp,[status(thm)],[t62675,t189]) ).
cnf(t111272,plain,
meet(complement(X2),join(X1,meet(X2,X3))) = meet(complement(X2),join(X2,X1)),
inference(step,[status(thm)],[t62781,t23]) ).
cnf(t111273,plain,
meet(complement(X2),join(X1,meet(X2,X3))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t111272,t62675]) ).
cnf(t68228,plain,
meet(complement(X1),join(X2,meet(X1,X3))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t111273]) ).
cnf(t121,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))) = meet(X1,join(X2,join(meet(X1,X3),meet(X3,X4)))),
inference(cp,[status(thm)],[t46,t112]) ).
cnf(t110042,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(step,[status(thm)],[t121,t46]) ).
cnf(t1543,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t110042]) ).
cnf(t18206,plain,
meet(X1,join(complement(meet(X2,X3)),meet(X2,join(X1,X3)))) = meet(X1,one),
inference(cp,[status(thm)],[t1543,t18116]) ).
cnf(t110779,plain,
meet(X1,join(complement(meet(X2,X3)),meet(X2,join(X1,X3)))) = X1,
inference(step,[status(thm)],[t18206,t105]) ).
cnf(t24850,plain,
meet(X1,join(complement(meet(X2,X3)),meet(X2,join(X1,X3)))) = X1,
inference(orient,[status(thm)],[t110779]) ).
cnf(t24894,plain,
X1 = meet(X1,join(complement(meet(X2,X3)),meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t24850,t23]) ).
cnf(t28553,plain,
meet(X1,join(complement(meet(X2,X3)),meet(X3,join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t24894]) ).
cnf(t68232,plain,
meet(complement(meet(X1,X2)),complement(X2)) = complement(X2),
inference(cp,[status(thm)],[t68228,t28553]) ).
cnf(t111275,plain,
complement(join(meet(X1,X2),X2)) = complement(X2),
inference(step,[status(thm)],[t68232,t65747]) ).
cnf(t111276,plain,
complement(join(X2,meet(X1,X2))) = complement(X2),
inference(step,[status(thm)],[t111275,t69]) ).
cnf(t68517,plain,
complement(join(X1,meet(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t111276]) ).
cnf(t111319,plain,
meet(join(X1,complement(X2)),complement(meet(X1,X2))) = complement(X2),
inference(step,[status(thm)],[t111318,t68517]) ).
cnf(t71872,plain,
meet(join(X1,complement(X2)),complement(meet(X1,X2))) = complement(X2),
inference(orient,[status(thm)],[t111319]) ).
cnf(t71261,plain,
meet(X1,complement(join(X2,complement(X3)))) = meet(X1,join(complement(X1),meet(X3,complement(X2)))),
inference(cp,[status(thm)],[t65245,t71183]) ).
cnf(t111602,plain,
meet(X1,meet(X3,complement(X2))) = meet(X1,join(complement(X1),meet(X3,complement(X2)))),
inference(step,[status(thm)],[t71261,t65498]) ).
cnf(t102640,plain,
meet(X1,join(complement(X1),meet(X2,complement(X3)))) = meet(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t111602]) ).
cnf(t102679,plain,
meet(X1,meet(X2,complement(complement(X3)))) = meet(X1,join(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t102640,t1052]) ).
cnf(t111603,plain,
meet(X1,meet(X2,X3)) = meet(X1,join(complement(X1),meet(X2,X3))),
inference(step,[status(thm)],[t102679,t1052]) ).
cnf(t102815,plain,
meet(X1,join(complement(X1),meet(X2,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t111603]) ).
cnf(t102908,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(join(X1,complement(join(complement(X1),meet(X2,X3)))),complement(meet(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t71872,t102815]) ).
cnf(t111604,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(complement(meet(X1,meet(X2,X3))),join(X1,complement(join(complement(X1),meet(X2,X3))))),
inference(step,[status(thm)],[t102908,t23]) ).
cnf(t66603,plain,
join(X1,complement(join(complement(X1),meet(X2,X3)))) = join(X1,complement(one)),
inference(cp,[status(thm)],[t66575,t19790]) ).
cnf(t111270,plain,
join(X1,complement(join(complement(X1),meet(X2,X3)))) = join(X1,zero),
inference(step,[status(thm)],[t66603,t149]) ).
cnf(t111271,plain,
join(X1,complement(join(complement(X1),meet(X2,X3)))) = X1,
inference(step,[status(thm)],[t111270,t100]) ).
cnf(t68051,plain,
join(X1,complement(join(complement(X1),meet(X2,X3)))) = X1,
inference(orient,[status(thm)],[t111271]) ).
cnf(t111605,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(complement(meet(X1,meet(X2,X3))),X1),
inference(step,[status(thm)],[t111604,t68051]) ).
cnf(t111606,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,complement(meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t111605,t23]) ).
cnf(t111607,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,complement(meet(X2,X3))),
inference(step,[status(thm)],[t111606,t65245]) ).
cnf(t103020,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,complement(meet(X2,X3))),
inference(orient,[status(thm)],[t111607]) ).
cnf(t111653,plain,
join(meet(X2,complement(X1)),meet(X2,complement(X3))) = meet(X2,complement(meet(X1,X3))),
inference(step,[status(thm)],[t111652,t103020]) ).
cnf(t108571,plain,
join(meet(X1,complement(X2)),meet(X1,complement(X3))) = meet(X1,complement(meet(X2,X3))),
inference(orient,[status(thm)],[t111653]) ).
cnf(t108667,plain,
meet(X1,complement(meet(X2,complement(X3)))) = join(meet(X1,complement(X2)),meet(X1,X3)),
inference(cp,[status(thm)],[t108571,t1052]) ).
cnf(t111654,plain,
meet(X1,join(X3,complement(X2))) = join(meet(X1,complement(X2)),meet(X1,X3)),
inference(step,[status(thm)],[t108667,t65976]) ).
cnf(t111655,plain,
meet(X1,join(X3,complement(X2))) = join(meet(X1,X3),meet(X1,complement(X2))),
inference(step,[status(thm)],[t111654,t69]) ).
cnf(t108882,plain,
join(meet(X1,X2),meet(X1,complement(X3))) = meet(X1,join(X2,complement(X3))),
inference(orient,[status(thm)],[t111655]) ).
cnf(t109076,plain,
meet(X1,join(X2,complement(complement(X3)))) = join(meet(X1,X2),meet(X1,X3)),
inference(cp,[status(thm)],[t108882,t1052]) ).
cnf(t111656,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,X3)),
inference(step,[status(thm)],[t109076,t1052]) ).
cnf(t109283,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t111656]) ).
cnf(f12,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f12_nnf,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(goal_0,negated_conjecture,
join(meet(a,b),meet(a,c)) != meet(a,join(b,c)),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(g0_0,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[goal_0,t109283]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT201-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.35 % Computer : n001.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Wed Sep 23 20:37:35 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 39.96/6.19 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 39.96/6.19 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------