%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT217-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 : n012.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:56:10 PM UTC 2026
% Result : Unsatisfiable 225.87s 52.82s
% Output : Proof 225.87s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
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(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(t1169934,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)],[t1169934]) ).
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(t1169936,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t29,t26]) ).
cnf(t1169937,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t1169936,t23]) ).
cnf(t115,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t1169937]) ).
cnf(f11,axiom,
meet(X,join(meet(Y,join(X,Z)),meet(Z,join(X,Y)))) = join(meet(X,Y),meet(X,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H82) ).
fof(f11_nnf,plain,
! [X,Y,Z] : meet(X,join(meet(Y,join(X,Z)),meet(Z,join(X,Y)))) = join(meet(X,Y),meet(X,Z)),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z] : meet(X,join(meet(Y,join(X,Z)),meet(Z,join(X,Y)))) = join(meet(X,Y),meet(X,Z)),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(meet(X1,join(X0,X2)),meet(X2,join(X0,X1)))) = join(meet(X0,X1),meet(X0,X2)),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t12,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X3,join(X1,X2)))) = join(meet(X1,X2),meet(X1,X3)),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t46,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X3,join(X1,X2)))) = join(meet(X1,X2),meet(X1,X3)),
inference(orient,[status(thm)],[t12]) ).
cnf(t119,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X3,join(X1,X2)))) = meet(X1,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t115,t46]) ).
cnf(t1169993,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t119,t46]) ).
cnf(t325,plain,
meet(X1,join(meet(X1,X2),meet(X1,X3))) = join(meet(X1,X2),meet(X1,X3)),
inference(orient,[status(thm)],[t1169993]) ).
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(t97,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t99,plain,
join(meet(X1,X2),meet(X1,complement(X1))) = meet(X1,join(meet(X2,one),meet(complement(X1),join(X1,X2)))),
inference(cp,[status(thm)],[t46,t97]) ).
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(t1170128,plain,
join(meet(X1,X2),zero) = meet(X1,join(meet(X2,one),meet(complement(X1),join(X1,X2)))),
inference(step,[status(thm)],[t99,t62]) ).
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(t63,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t16,t62]) ).
cnf(t103,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t63]) ).
cnf(t1170129,plain,
meet(X1,X2) = meet(X1,join(meet(X2,one),meet(complement(X1),join(X1,X2)))),
inference(step,[status(thm)],[t1170128,t103]) ).
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(t98,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t14,t97]) ).
cnf(t110,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t98]) ).
cnf(t1170130,plain,
meet(X1,X2) = meet(X1,join(X2,meet(complement(X1),join(X1,X2)))),
inference(step,[status(thm)],[t1170129,t110]) ).
cnf(t2274,plain,
meet(X1,join(X2,meet(complement(X1),join(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170130]) ).
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(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(t67,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t1170161,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(step,[status(thm)],[t25,t67]) ).
cnf(t2771,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t1170161]) ).
cnf(t2785,plain,
X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t2771,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(t1170162,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t2785,t17]) ).
cnf(t1170163,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t1170162,t97]) ).
cnf(t1170164,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t1170163,t17]) ).
cnf(t2811,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1170164]) ).
cnf(t2831,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X2,meet(X1,join(complement(X1),X2)))),
inference(cp,[status(thm)],[t2274,t2811]) ).
cnf(t1170165,plain,
meet(X2,complement(X1)) = meet(complement(X1),join(X2,meet(X1,join(complement(X1),X2)))),
inference(step,[status(thm)],[t2831,t23]) ).
cnf(t1170166,plain,
meet(X2,complement(X1)) = meet(complement(X1),join(X2,meet(X1,join(X2,complement(X1))))),
inference(step,[status(thm)],[t1170165,t67]) ).
cnf(t2843,plain,
meet(complement(X1),join(X2,meet(X1,join(X2,complement(X1))))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t1170166]) ).
cnf(t2844,plain,
meet(X1,complement(complement(X2))) = meet(X2,join(X1,meet(complement(X2),join(X1,complement(complement(X2)))))),
inference(cp,[status(thm)],[t2843,t2811]) ).
cnf(t1170167,plain,
meet(X1,X2) = meet(X2,join(X1,meet(complement(X2),join(X1,complement(complement(X2)))))),
inference(step,[status(thm)],[t2844,t2811]) ).
cnf(t1170168,plain,
meet(X1,X2) = meet(X2,join(X1,meet(complement(X2),join(X1,X2)))),
inference(step,[status(thm)],[t1170167,t2811]) ).
cnf(t2904,plain,
meet(X1,join(X2,meet(complement(X1),join(X2,X1)))) = meet(X2,X1),
inference(orient,[status(thm)],[t1170168]) ).
cnf(t2937,plain,
join(meet(X1,join(X2,meet(complement(X1),join(X2,X1)))),meet(X1,X3)) = meet(X1,join(meet(X2,X1),meet(X1,X3))),
inference(cp,[status(thm)],[t325,t2904]) ).
cnf(t1170170,plain,
join(meet(X2,X1),meet(X1,X3)) = meet(X1,join(meet(X2,X1),meet(X1,X3))),
inference(step,[status(thm)],[t2937,t2904]) ).
cnf(t3015,plain,
meet(X1,join(meet(X2,X1),meet(X1,X3))) = join(meet(X2,X1),meet(X1,X3)),
inference(orient,[status(thm)],[t1170170]) ).
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(t1169935,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t9,t67]) ).
cnf(t73,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t1169935]) ).
cnf(t80,plain,
join(X1,X2) = ifeq(meet(X3,join(X1,X2)),zero,ifeq(join(X2,join(X3,X1)),one,complement(X3),join(X1,X2)),join(X1,X2)),
inference(cp,[status(thm)],[t18,t73]) ).
cnf(t1170730,plain,
join(X1,X2) = ifeq(meet(X3,join(X1,X2)),zero,ifeq(join(X1,join(X2,X3)),one,complement(X3),join(X1,X2)),join(X1,X2)),
inference(step,[status(thm)],[t80,t73]) ).
cnf(t49091,plain,
ifeq(meet(X1,join(X2,X3)),zero,ifeq(join(X2,join(X3,X1)),one,complement(X1),join(X2,X3)),join(X2,X3)) = join(X2,X3),
inference(orient,[status(thm)],[t1170730]) ).
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(t76,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t73,t15]) ).
cnf(t1169939,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t76,t73]) ).
cnf(t1169940,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t1169939,t67]) ).
cnf(t131,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1169940]) ).
cnf(t134,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t131,t97]) ).
cnf(t1169941,plain,
one = join(X1,one),
inference(step,[status(thm)],[t134,t97]) ).
cnf(t143,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t1169941]) ).
cnf(t145,plain,
one = ifeq(meet(X1,one),zero,ifeq(one,one,complement(X1),one),one),
inference(cp,[status(thm)],[t18,t143]) ).
cnf(t1169944,plain,
one = ifeq(X1,zero,ifeq(one,one,complement(X1),one),one),
inference(step,[status(thm)],[t145,t110]) ).
cnf(t1169945,plain,
one = ifeq(X1,zero,complement(X1),one),
inference(step,[status(thm)],[t1169944,t17]) ).
cnf(t154,plain,
ifeq(X1,zero,complement(X1),one) = one,
inference(orient,[status(thm)],[t1169945]) ).
cnf(t2816,plain,
one = ifeq(complement(X1),zero,X1,one),
inference(cp,[status(thm)],[t154,t2811]) ).
cnf(t2841,plain,
ifeq(complement(X1),zero,X1,one) = one,
inference(orient,[status(thm)],[t2816]) ).
cnf(t3036,plain,
join(meet(X1,X2),meet(X2,X2)) = meet(X2,join(meet(X1,X2),X2)),
inference(cp,[status(thm)],[t3015,t13]) ).
cnf(t1170171,plain,
join(meet(X1,X2),X2) = meet(X2,join(meet(X1,X2),X2)),
inference(step,[status(thm)],[t3036,t13]) ).
cnf(t1170172,plain,
join(X2,meet(X1,X2)) = meet(X2,join(meet(X1,X2),X2)),
inference(step,[status(thm)],[t1170171,t67]) ).
cnf(t1170173,plain,
join(X2,meet(X1,X2)) = meet(X2,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t1170172,t67]) ).
cnf(t1170174,plain,
join(X2,meet(X1,X2)) = X2,
inference(step,[status(thm)],[t1170173,t14]) ).
cnf(t3095,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t1170174]) ).
cnf(t30,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t26,t14]) ).
cnf(t1169950,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t30,t26]) ).
cnf(t1169951,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t1169950,t23]) ).
cnf(t1169952,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t1169951,t23]) ).
cnf(t178,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t1169952]) ).
cnf(t3100,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X2,X1)),
inference(cp,[status(thm)],[t3095,t178]) ).
cnf(t1170179,plain,
meet(X1,join(X2,X3)) = join(meet(X2,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t3100,t67]) ).
cnf(t1170180,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t1170179,t23]) ).
cnf(t3214,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t1170180]) ).
cnf(t3219,plain,
meet(X1,join(meet(X1,X2),X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t3214,t115]) ).
cnf(t1170184,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t3219,t67]) ).
cnf(t1170185,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t1170184,t67]) ).
cnf(t3380,plain,
join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))) = meet(X1,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t1170185]) ).
cnf(t3422,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t14,t3380]) ).
cnf(t1170186,plain,
meet(X1,X2) = meet(X1,meet(join(X3,meet(X1,X2)),meet(X1,X2))),
inference(step,[status(thm)],[t3422,t26]) ).
cnf(t1170187,plain,
meet(X1,X2) = meet(X1,meet(X2,meet(join(X3,meet(X1,X2)),X1))),
inference(step,[status(thm)],[t1170186,t26]) ).
cnf(t1170188,plain,
meet(X1,X2) = meet(X1,meet(X1,meet(X2,join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t1170187,t26]) ).
cnf(t1170189,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t1170188,t115]) ).
cnf(t3449,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170189]) ).
cnf(t3473,plain,
meet(X1,meet(X1,X2)) = meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t3449,t115]) ).
cnf(t1170204,plain,
meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t3473,t115]) ).
cnf(t3735,plain,
meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170204]) ).
cnf(t3736,plain,
meet(X1,join(X2,meet(complement(X1),join(X2,X1)))) = meet(X1,meet(meet(X2,X1),join(X3,meet(X1,join(X2,meet(complement(X1),join(X2,X1))))))),
inference(cp,[status(thm)],[t3735,t2904]) ).
cnf(t1170208,plain,
meet(X2,X1) = meet(X1,meet(meet(X2,X1),join(X3,meet(X1,join(X2,meet(complement(X1),join(X2,X1))))))),
inference(step,[status(thm)],[t3736,t2904]) ).
cnf(t1170209,plain,
meet(X2,X1) = meet(X1,meet(meet(X2,X1),join(X3,meet(X2,X1)))),
inference(step,[status(thm)],[t1170208,t2904]) ).
cnf(t3866,plain,
meet(X1,meet(meet(X2,X1),join(X3,meet(X2,X1)))) = meet(X2,X1),
inference(orient,[status(thm)],[t1170209]) ).
cnf(t3875,plain,
meet(X1,meet(X1,X2)) = meet(meet(X1,X2),meet(meet(X1,X2),join(X3,meet(X1,meet(X1,X2))))),
inference(cp,[status(thm)],[t3866,t115]) ).
cnf(t1170210,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(X3,meet(X1,meet(X1,X2))))),
inference(step,[status(thm)],[t3875,t115]) ).
cnf(t1170211,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,meet(X1,X2)))),
inference(step,[status(thm)],[t1170210,t115]) ).
cnf(t1170212,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t1170211,t115]) ).
cnf(t3973,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170212]) ).
cnf(t4005,plain,
meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3)) = join(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3))),
inference(cp,[status(thm)],[t3214,t3973]) ).
cnf(t1170218,plain,
meet(meet(X1,X2),join(Y3,join(X3,meet(X1,X2)))) = join(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3))),
inference(step,[status(thm)],[t4005,t67]) ).
cnf(t1170219,plain,
meet(meet(X1,X2),join(X3,join(meet(X1,X2),Y3))) = join(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3))),
inference(step,[status(thm)],[t1170218,t73]) ).
cnf(t1170220,plain,
meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = join(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3))),
inference(step,[status(thm)],[t1170219,t67]) ).
cnf(t1170221,plain,
meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = meet(X1,X2),
inference(step,[status(thm)],[t1170220,t16]) ).
cnf(t4126,plain,
meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170221]) ).
cnf(t3106,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t3095,t26]) ).
cnf(t3160,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t3106]) ).
cnf(t4148,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X2))),
inference(cp,[status(thm)],[t4126,t3160]) ).
cnf(t5107,plain,
meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t4148]) ).
cnf(t5108,plain,
meet(X1,meet(X2,X3)) = meet(join(Y3,meet(X1,X2)),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t5107,t23]) ).
cnf(t1170247,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X3),meet(join(Y3,meet(X1,X2)),X1)),
inference(step,[status(thm)],[t5108,t26]) ).
cnf(t1170248,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t1170247,t26]) ).
cnf(t5548,plain,
meet(X1,meet(meet(X2,X3),join(Y3,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t1170248]) ).
cnf(t5556,plain,
meet(X1,meet(X2,join(X3,meet(complement(X2),join(X3,X2))))) = meet(X1,meet(meet(X3,X2),join(Y3,meet(X1,X2)))),
inference(cp,[status(thm)],[t5548,t2904]) ).
cnf(t1170256,plain,
meet(X1,meet(X3,X2)) = meet(X1,meet(meet(X3,X2),join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t5556,t2904]) ).
cnf(t6116,plain,
meet(X1,meet(meet(X2,X3),join(Y3,meet(X1,X3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t1170256]) ).
cnf(t6139,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(Y3,meet(X1,join(X2,X3))))),
inference(cp,[status(thm)],[t6116,t14]) ).
cnf(t1170257,plain,
meet(X1,X2) = meet(X1,meet(X2,join(Y3,meet(X1,join(X2,X3))))),
inference(step,[status(thm)],[t6139,t14]) ).
cnf(t6257,plain,
meet(X1,meet(X2,join(X3,meet(X1,join(X2,Y3))))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170257]) ).
cnf(t6263,plain,
meet(X1,X2) = meet(X1,join(meet(X2,X3),meet(X2,X1))),
inference(cp,[status(thm)],[t6257,t46]) ).
cnf(t1170258,plain,
meet(X1,X2) = meet(X1,join(meet(X2,X1),meet(X2,X3))),
inference(step,[status(thm)],[t6263,t67]) ).
cnf(t1170259,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t1170258,t23]) ).
cnf(t6344,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170259]) ).
cnf(t3126,plain,
join(meet(X1,X2),join(X3,X2)) = join(X3,X2),
inference(cp,[status(thm)],[t73,t3095]) ).
cnf(t1170176,plain,
join(X2,join(meet(X1,X2),X3)) = join(X3,X2),
inference(step,[status(thm)],[t3126,t73]) ).
cnf(t1170177,plain,
join(X2,join(X3,meet(X1,X2))) = join(X3,X2),
inference(step,[status(thm)],[t1170176,t67]) ).
cnf(t1170178,plain,
join(X2,join(X3,meet(X1,X2))) = join(X2,X3),
inference(step,[status(thm)],[t1170177,t67]) ).
cnf(t3128,plain,
join(X1,join(X2,meet(X3,X1))) = join(X1,X2),
inference(orient,[status(thm)],[t1170178]) ).
cnf(t4139,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(cp,[status(thm)],[t4126,t3128]) ).
cnf(t4196,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t4139]) ).
cnf(t4205,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),Y3)),
inference(cp,[status(thm)],[t4196,t178]) ).
cnf(t1170222,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),Y3)),
inference(step,[status(thm)],[t4205,t178]) ).
cnf(t1170223,plain,
meet(X1,X2) = meet(meet(X1,X2),join(Y3,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t1170222,t67]) ).
cnf(t4341,plain,
meet(meet(X1,X2),join(X3,meet(X2,join(X1,Y3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170223]) ).
cnf(t4384,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y3,meet(X2,X3))),
inference(cp,[status(thm)],[t4341,t3973]) ).
cnf(t5452,plain,
meet(meet(X1,meet(X2,X3)),join(Y3,meet(X2,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t4384]) ).
cnf(t48,plain,
join(meet(X1,join(X1,X2)),meet(X1,X2)) = meet(X1,join(join(X1,X2),meet(X2,join(X1,join(X1,X2))))),
inference(cp,[status(thm)],[t46,t13]) ).
cnf(t1170014,plain,
join(meet(X1,X2),meet(X1,join(X1,X2))) = meet(X1,join(join(X1,X2),meet(X2,join(X1,join(X1,X2))))),
inference(step,[status(thm)],[t48,t67]) ).
cnf(t1170015,plain,
join(meet(X1,X2),X1) = meet(X1,join(join(X1,X2),meet(X2,join(X1,join(X1,X2))))),
inference(step,[status(thm)],[t1170014,t14]) ).
cnf(t1170016,plain,
join(X1,meet(X1,X2)) = meet(X1,join(join(X1,X2),meet(X2,join(X1,join(X1,X2))))),
inference(step,[status(thm)],[t1170015,t67]) ).
cnf(t1170017,plain,
X1 = meet(X1,join(join(X1,X2),meet(X2,join(X1,join(X1,X2))))),
inference(step,[status(thm)],[t1170016,t16]) ).
cnf(t1170018,plain,
X1 = meet(X1,join(join(X1,X2),meet(X2,join(X1,X2)))),
inference(step,[status(thm)],[t1170017,t131]) ).
cnf(t529,plain,
meet(X1,join(join(X1,X2),meet(X2,join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t1170018]) ).
cnf(t538,plain,
X1 = meet(X1,join(one,meet(complement(X1),join(X1,complement(X1))))),
inference(cp,[status(thm)],[t529,t97]) ).
cnf(t1170019,plain,
X1 = meet(X1,join(one,meet(complement(X1),one))),
inference(step,[status(thm)],[t538,t97]) ).
cnf(t1170020,plain,
X1 = meet(X1,join(one,complement(X1))),
inference(step,[status(thm)],[t1170019,t110]) ).
cnf(t567,plain,
meet(X1,join(one,complement(X1))) = X1,
inference(orient,[status(thm)],[t1170020]) ).
cnf(t572,plain,
join(meet(one,X1),meet(one,complement(X1))) = meet(one,join(X1,meet(complement(X1),join(one,X1)))),
inference(cp,[status(thm)],[t46,t567]) ).
cnf(t1170038,plain,
join(meet(X1,one),meet(one,complement(X1))) = meet(one,join(X1,meet(complement(X1),join(one,X1)))),
inference(step,[status(thm)],[t572,t23]) ).
cnf(t1170039,plain,
join(X1,meet(one,complement(X1))) = meet(one,join(X1,meet(complement(X1),join(one,X1)))),
inference(step,[status(thm)],[t1170038,t110]) ).
cnf(t1170040,plain,
join(X1,meet(one,complement(X1))) = meet(one,join(X1,meet(complement(X1),join(X1,one)))),
inference(step,[status(thm)],[t1170039,t67]) ).
cnf(t1170041,plain,
join(X1,meet(one,complement(X1))) = meet(one,join(X1,meet(complement(X1),one))),
inference(step,[status(thm)],[t1170040,t143]) ).
cnf(t1170042,plain,
join(X1,meet(one,complement(X1))) = meet(one,join(X1,complement(X1))),
inference(step,[status(thm)],[t1170041,t110]) ).
cnf(t1170043,plain,
join(X1,meet(one,complement(X1))) = meet(one,one),
inference(step,[status(thm)],[t1170042,t97]) ).
cnf(t1170044,plain,
join(X1,meet(one,complement(X1))) = one,
inference(step,[status(thm)],[t1170043,t110]) ).
cnf(t612,plain,
join(X1,meet(one,complement(X1))) = one,
inference(orient,[status(thm)],[t1170044]) ).
cnf(t613,plain,
meet(one,complement(X1)) = ifeq(meet(X1,meet(one,complement(X1))),zero,ifeq(one,one,complement(X1),meet(one,complement(X1))),meet(one,complement(X1))),
inference(cp,[status(thm)],[t18,t612]) ).
cnf(t65,plain,
meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
inference(cp,[status(thm)],[t26,t62]) ).
cnf(t1169946,plain,
meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
inference(step,[status(thm)],[t65,t23]) ).
cnf(t118,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t115,t62]) ).
cnf(t1169938,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t118,t62]) ).
cnf(t126,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t1169938]) ).
cnf(t1169947,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t1169946,t126]) ).
cnf(t162,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t1169947]) ).
cnf(t1170045,plain,
meet(one,complement(X1)) = ifeq(zero,zero,ifeq(one,one,complement(X1),meet(one,complement(X1))),meet(one,complement(X1))),
inference(step,[status(thm)],[t613,t162]) ).
cnf(t1170046,plain,
meet(one,complement(X1)) = ifeq(one,one,complement(X1),meet(one,complement(X1))),
inference(step,[status(thm)],[t1170045,t17]) ).
cnf(t1170047,plain,
meet(one,complement(X1)) = complement(X1),
inference(step,[status(thm)],[t1170046,t17]) ).
cnf(t624,plain,
meet(one,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1170047]) ).
cnf(t628,plain,
join(meet(one,complement(X1)),meet(one,X2)) = meet(one,join(complement(X1),meet(one,X2))),
inference(cp,[status(thm)],[t325,t624]) ).
cnf(t1170052,plain,
join(meet(one,X2),meet(one,complement(X1))) = meet(one,join(complement(X1),meet(one,X2))),
inference(step,[status(thm)],[t628,t67]) ).
cnf(t1170053,plain,
join(meet(X2,one),meet(one,complement(X1))) = meet(one,join(complement(X1),meet(one,X2))),
inference(step,[status(thm)],[t1170052,t23]) ).
cnf(t1170054,plain,
join(X2,meet(one,complement(X1))) = meet(one,join(complement(X1),meet(one,X2))),
inference(step,[status(thm)],[t1170053,t110]) ).
cnf(t1170055,plain,
join(X2,complement(X1)) = meet(one,join(complement(X1),meet(one,X2))),
inference(step,[status(thm)],[t1170054,t624]) ).
cnf(t1170056,plain,
join(X2,complement(X1)) = meet(one,join(complement(X1),meet(X2,one))),
inference(step,[status(thm)],[t1170055,t23]) ).
cnf(t1170057,plain,
join(X2,complement(X1)) = meet(one,join(complement(X1),X2)),
inference(step,[status(thm)],[t1170056,t110]) ).
cnf(t1170058,plain,
join(X2,complement(X1)) = meet(one,join(X2,complement(X1))),
inference(step,[status(thm)],[t1170057,t67]) ).
cnf(t671,plain,
meet(one,join(X1,complement(X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t1170058]) ).
cnf(t677,plain,
join(meet(one,join(X1,complement(X2))),meet(one,X3)) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(cp,[status(thm)],[t325,t671]) ).
cnf(t1170074,plain,
join(meet(one,X3),meet(one,join(X1,complement(X2)))) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t677,t67]) ).
cnf(t1170075,plain,
join(meet(X3,one),meet(one,join(X1,complement(X2)))) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t1170074,t23]) ).
cnf(t1170076,plain,
join(X3,meet(one,join(X1,complement(X2)))) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t1170075,t110]) ).
cnf(t1170077,plain,
join(X3,join(X1,complement(X2))) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t1170076,t671]) ).
cnf(t1170078,plain,
join(X1,join(complement(X2),X3)) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t1170077,t73]) ).
cnf(t1170079,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t1170078,t67]) ).
cnf(t1170080,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(meet(one,X3),join(X1,complement(X2)))),
inference(step,[status(thm)],[t1170079,t67]) ).
cnf(t1170081,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(complement(X2),join(meet(one,X3),X1))),
inference(step,[status(thm)],[t1170080,t73]) ).
cnf(t1170082,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(X1,join(complement(X2),meet(one,X3)))),
inference(step,[status(thm)],[t1170081,t73]) ).
cnf(t1170083,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(X1,join(complement(X2),meet(X3,one)))),
inference(step,[status(thm)],[t1170082,t23]) ).
cnf(t1170084,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(X1,join(complement(X2),X3))),
inference(step,[status(thm)],[t1170083,t110]) ).
cnf(t1170085,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(X1,join(X3,complement(X2)))),
inference(step,[status(thm)],[t1170084,t67]) ).
cnf(t1164,plain,
meet(one,join(X1,join(X2,complement(X3)))) = join(X1,join(X2,complement(X3))),
inference(orient,[status(thm)],[t1170085]) ).
cnf(t128,plain,
zero = ifeq(zero,zero,ifeq(join(X1,zero),one,complement(X1),zero),zero),
inference(cp,[status(thm)],[t18,t126]) ).
cnf(t1169942,plain,
zero = ifeq(join(X1,zero),one,complement(X1),zero),
inference(step,[status(thm)],[t128,t17]) ).
cnf(t1169943,plain,
zero = ifeq(X1,one,complement(X1),zero),
inference(step,[status(thm)],[t1169942,t103]) ).
cnf(t150,plain,
ifeq(X1,one,complement(X1),zero) = zero,
inference(orient,[status(thm)],[t1169943]) ).
cnf(t151,plain,
zero = complement(one),
inference(cp,[status(thm)],[t150,t17]) ).
cnf(t152,plain,
complement(one) = zero,
inference(orient,[status(thm)],[t151]) ).
cnf(t1170,plain,
join(X1,join(X2,complement(one))) = meet(one,join(X1,join(X2,zero))),
inference(cp,[status(thm)],[t1164,t152]) ).
cnf(t1170086,plain,
join(X1,join(X2,zero)) = meet(one,join(X1,join(X2,zero))),
inference(step,[status(thm)],[t1170,t152]) ).
cnf(t1170087,plain,
join(X1,X2) = meet(one,join(X1,join(X2,zero))),
inference(step,[status(thm)],[t1170086,t103]) ).
cnf(t1170088,plain,
join(X1,X2) = meet(one,join(X1,X2)),
inference(step,[status(thm)],[t1170087,t103]) ).
cnf(t1205,plain,
meet(one,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1170088]) ).
cnf(t3488,plain,
meet(one,join(X1,X2)) = meet(one,meet(join(X1,X2),join(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t3449,t1205]) ).
cnf(t1170205,plain,
join(X1,X2) = meet(one,meet(join(X1,X2),join(X3,join(X1,X2)))),
inference(step,[status(thm)],[t3488,t1205]) ).
cnf(t1170206,plain,
join(X1,X2) = meet(one,meet(join(X1,X2),join(X2,join(X3,X1)))),
inference(step,[status(thm)],[t1170205,t73]) ).
cnf(t1170207,plain,
join(X1,X2) = meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t1170206,t73]) ).
cnf(t3776,plain,
meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))) = join(X1,X2),
inference(orient,[status(thm)],[t1170207]) ).
cnf(t3981,plain,
meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))) = meet(join(X1,X2),join(Y3,meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))))),
inference(cp,[status(thm)],[t3973,t3776]) ).
cnf(t1170214,plain,
join(X1,X2) = meet(join(X1,X2),join(Y3,meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))))),
inference(step,[status(thm)],[t3981,t3776]) ).
cnf(t1170215,plain,
join(X1,X2) = meet(join(X1,X2),join(Y3,join(X1,X2))),
inference(step,[status(thm)],[t1170214,t3776]) ).
cnf(t1170216,plain,
join(X1,X2) = meet(join(X1,X2),join(X2,join(Y3,X1))),
inference(step,[status(thm)],[t1170215,t73]) ).
cnf(t1170217,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,Y3))),
inference(step,[status(thm)],[t1170216,t73]) ).
cnf(t4034,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t1170217]) ).
cnf(t5473,plain,
meet(X1,meet(join(X2,X3),join(X2,join(X3,Y3)))) = meet(meet(X1,join(X2,X3)),join(Y4,meet(join(X2,X3),join(X2,join(X3,Y3))))),
inference(cp,[status(thm)],[t5452,t4034]) ).
cnf(t1170252,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,meet(join(X2,X3),join(X2,join(X3,Y3))))),
inference(step,[status(thm)],[t5473,t4034]) ).
cnf(t1170253,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,join(X2,X3))),
inference(step,[status(thm)],[t1170252,t4034]) ).
cnf(t1170254,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X3,join(Y4,X2))),
inference(step,[status(thm)],[t1170253,t73]) ).
cnf(t1170255,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,join(X3,Y4))),
inference(step,[status(thm)],[t1170254,t73]) ).
cnf(t6003,plain,
meet(meet(X1,join(X2,X3)),join(X2,join(X3,Y3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t1170255]) ).
cnf(t6065,plain,
join(X1,join(X2,X3)) = join(join(X1,join(X2,X3)),meet(Y3,join(X1,X2))),
inference(cp,[status(thm)],[t3095,t6003]) ).
cnf(t1170260,plain,
join(X1,join(X2,X3)) = join(meet(Y3,join(X1,X2)),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t6065,t67]) ).
cnf(t1170261,plain,
join(X1,join(X2,X3)) = join(join(X2,X3),join(meet(Y3,join(X1,X2)),X1)),
inference(step,[status(thm)],[t1170260,t73]) ).
cnf(t1170262,plain,
join(X1,join(X2,X3)) = join(X1,join(join(X2,X3),meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t1170261,t73]) ).
cnf(t6512,plain,
join(X1,join(join(X2,X3),meet(Y3,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t1170262]) ).
cnf(t6516,plain,
join(X1,join(X2,X2)) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t6512,t15]) ).
cnf(t1170263,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t6516,t15]) ).
cnf(t6592,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t1170263]) ).
cnf(t6594,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t6592,t3380]) ).
cnf(t6642,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t6594]) ).
cnf(t6650,plain,
join(X1,meet(X2,join(X3,meet(complement(X2),join(X3,X2))))) = join(X1,meet(X2,join(X1,meet(X3,X2)))),
inference(cp,[status(thm)],[t6642,t2904]) ).
cnf(t1170265,plain,
join(X1,meet(X3,X2)) = join(X1,meet(X2,join(X1,meet(X3,X2)))),
inference(step,[status(thm)],[t6650,t2904]) ).
cnf(t6746,plain,
join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t1170265]) ).
cnf(t77,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t73,t16]) ).
cnf(t1169953,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t77,t73]) ).
cnf(t1169954,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t1169953,t67]) ).
cnf(t1169955,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t1169954,t67]) ).
cnf(t191,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t1169955]) ).
cnf(t4141,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t4126,t191]) ).
cnf(t4274,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t4141]) ).
cnf(t6782,plain,
join(X1,meet(meet(X2,X3),join(X2,Y3))) = join(X1,meet(join(X2,Y3),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t6746,t4274]) ).
cnf(t1170285,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X2,Y3),join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t6782,t4274]) ).
cnf(t7509,plain,
join(X1,meet(join(X2,X3),join(X1,meet(X2,Y3)))) = join(X1,meet(X2,Y3)),
inference(orient,[status(thm)],[t1170285]) ).
cnf(t7570,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X1,join(X2,X3)),meet(X2,Y3))),
inference(cp,[status(thm)],[t6344,t7509]) ).
cnf(t1170296,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X2,Y3),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t7570,t67]) ).
cnf(t8776,plain,
meet(X1,join(meet(X2,X3),meet(X1,join(X2,Y3)))) = meet(X1,join(X2,Y3)),
inference(orient,[status(thm)],[t1170296]) ).
cnf(t8798,plain,
meet(X1,join(X2,meet(complement(X1),join(X2,X1)))) = meet(X1,join(meet(X2,X3),meet(X2,X1))),
inference(cp,[status(thm)],[t8776,t2904]) ).
cnf(t8913,plain,
meet(X1,join(meet(X2,X1),meet(X2,X3))) = meet(X2,X1),
inference(orient,[status(thm)],[t8798]) ).
cnf(t8973,plain,
meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = meet(join(X3,join(Y3,meet(X1,X2))),join(meet(X1,X2),meet(meet(X1,X2),Y4))),
inference(cp,[status(thm)],[t8913,t4126]) ).
cnf(t1170321,plain,
meet(X1,X2) = meet(join(X3,join(Y3,meet(X1,X2))),join(meet(X1,X2),meet(meet(X1,X2),Y4))),
inference(step,[status(thm)],[t8973,t4126]) ).
cnf(t1170322,plain,
meet(X1,X2) = meet(join(X3,join(Y3,meet(X1,X2))),meet(X1,X2)),
inference(step,[status(thm)],[t1170321,t16]) ).
cnf(t1170323,plain,
meet(X1,X2) = meet(X2,meet(join(X3,join(Y3,meet(X1,X2))),X1)),
inference(step,[status(thm)],[t1170322,t26]) ).
cnf(t1170324,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,join(Y3,meet(X1,X2))))),
inference(step,[status(thm)],[t1170323,t26]) ).
cnf(t9417,plain,
meet(X1,meet(X2,join(X3,join(Y3,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170324]) ).
cnf(t9469,plain,
meet(X1,complement(X1)) = meet(X1,meet(complement(X1),join(X2,join(X3,zero)))),
inference(cp,[status(thm)],[t9417,t62]) ).
cnf(t1170325,plain,
zero = meet(X1,meet(complement(X1),join(X2,join(X3,zero)))),
inference(step,[status(thm)],[t9469,t62]) ).
cnf(t1170326,plain,
zero = meet(X1,meet(complement(X1),join(X2,X3))),
inference(step,[status(thm)],[t1170325,t103]) ).
cnf(t9544,plain,
meet(X1,meet(complement(X1),join(X2,X3))) = zero,
inference(orient,[status(thm)],[t1170326]) ).
cnf(t9547,plain,
zero = meet(X1,join(meet(complement(X1),X2),meet(complement(X1),X3))),
inference(cp,[status(thm)],[t9544,t46]) ).
cnf(t1170341,plain,
zero = meet(X1,join(meet(X2,complement(X1)),meet(complement(X1),X3))),
inference(step,[status(thm)],[t9547,t23]) ).
cnf(t1170342,plain,
zero = meet(X1,join(meet(X2,complement(X1)),meet(X3,complement(X1)))),
inference(step,[status(thm)],[t1170341,t23]) ).
cnf(t10459,plain,
meet(X1,join(meet(X2,complement(X1)),meet(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t1170342]) ).
cnf(t10461,plain,
zero = meet(complement(X1),join(meet(X2,X1),meet(X3,complement(complement(X1))))),
inference(cp,[status(thm)],[t10459,t2811]) ).
cnf(t1170343,plain,
zero = meet(complement(X1),join(meet(X1,X2),meet(X3,complement(complement(X1))))),
inference(step,[status(thm)],[t10461,t23]) ).
cnf(t1170344,plain,
zero = meet(complement(X1),join(meet(X1,X2),meet(X3,X1))),
inference(step,[status(thm)],[t1170343,t2811]) ).
cnf(t1170345,plain,
zero = meet(complement(X1),join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t1170344,t23]) ).
cnf(t10521,plain,
meet(complement(X1),join(meet(X1,X2),meet(X1,X3))) = zero,
inference(orient,[status(thm)],[t1170345]) ).
cnf(t3030,plain,
join(meet(X1,join(X1,X2)),meet(join(X1,X2),X3)) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t3015,t14]) ).
cnf(t1170181,plain,
join(X1,meet(join(X1,X2),X3)) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t3030,t14]) ).
cnf(t1170182,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t1170181,t23]) ).
cnf(t1170183,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t1170182,t23]) ).
cnf(t3303,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))) = join(X1,meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t1170183]) ).
cnf(t3487,plain,
meet(one,complement(X1)) = meet(one,meet(complement(X1),join(X2,complement(X1)))),
inference(cp,[status(thm)],[t3449,t624]) ).
cnf(t1170190,plain,
complement(X1) = meet(one,meet(complement(X1),join(X2,complement(X1)))),
inference(step,[status(thm)],[t3487,t624]) ).
cnf(t3506,plain,
meet(one,meet(complement(X1),join(X2,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t1170190]) ).
cnf(t3543,plain,
meet(meet(complement(X1),join(X2,complement(X1))),meet(X3,one)) = meet(X3,complement(X1)),
inference(cp,[status(thm)],[t26,t3506]) ).
cnf(t1170191,plain,
meet(meet(complement(X1),join(X2,complement(X1))),X3) = meet(X3,complement(X1)),
inference(step,[status(thm)],[t3543,t110]) ).
cnf(t1170192,plain,
meet(X3,meet(complement(X1),join(X2,complement(X1)))) = meet(X3,complement(X1)),
inference(step,[status(thm)],[t1170191,t23]) ).
cnf(t3544,plain,
meet(X1,meet(complement(X2),join(X3,complement(X2)))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t1170192]) ).
cnf(t3545,plain,
meet(complement(X1),complement(X1)) = meet(complement(X1),join(X2,complement(X1))),
inference(cp,[status(thm)],[t3544,t115]) ).
cnf(t1170193,plain,
complement(X1) = meet(complement(X1),join(X2,complement(X1))),
inference(step,[status(thm)],[t3545,t13]) ).
cnf(t3566,plain,
meet(complement(X1),join(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t1170193]) ).
cnf(t3571,plain,
meet(complement(X1),join(join(X2,complement(X1)),X3)) = join(complement(X1),meet(complement(X1),join(join(X2,complement(X1)),X3))),
inference(cp,[status(thm)],[t3214,t3566]) ).
cnf(t1170194,plain,
meet(complement(X1),join(X3,join(X2,complement(X1)))) = join(complement(X1),meet(complement(X1),join(join(X2,complement(X1)),X3))),
inference(step,[status(thm)],[t3571,t67]) ).
cnf(t1170195,plain,
meet(complement(X1),join(X2,join(complement(X1),X3))) = join(complement(X1),meet(complement(X1),join(join(X2,complement(X1)),X3))),
inference(step,[status(thm)],[t1170194,t73]) ).
cnf(t1170196,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = join(complement(X1),meet(complement(X1),join(join(X2,complement(X1)),X3))),
inference(step,[status(thm)],[t1170195,t67]) ).
cnf(t1170197,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = complement(X1),
inference(step,[status(thm)],[t1170196,t16]) ).
cnf(t3604,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t1170197]) ).
cnf(t4389,plain,
meet(X1,complement(X2)) = meet(meet(X1,complement(X2)),join(X3,complement(X2))),
inference(cp,[status(thm)],[t4341,t3604]) ).
cnf(t4464,plain,
meet(meet(X1,complement(X2)),join(X3,complement(X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t4389]) ).
cnf(t4490,plain,
join(X1,meet(meet(X2,complement(X3)),join(X1,complement(X3)))) = meet(join(X1,complement(X3)),join(X1,meet(X2,complement(X3)))),
inference(cp,[status(thm)],[t3303,t4464]) ).
cnf(t1170439,plain,
join(X1,meet(X2,complement(X3))) = meet(join(X1,complement(X3)),join(X1,meet(X2,complement(X3)))),
inference(step,[status(thm)],[t4490,t4464]) ).
cnf(t14902,plain,
meet(join(X1,complement(X2)),join(X1,meet(X3,complement(X2)))) = join(X1,meet(X3,complement(X2))),
inference(orient,[status(thm)],[t1170439]) ).
cnf(t14905,plain,
join(X1,meet(X2,complement(complement(X3)))) = meet(join(X1,X3),join(X1,meet(X2,complement(complement(X3))))),
inference(cp,[status(thm)],[t14902,t2811]) ).
cnf(t1170440,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X3),join(X1,meet(X2,complement(complement(X3))))),
inference(step,[status(thm)],[t14905,t2811]) ).
cnf(t1170441,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X3),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t1170440,t2811]) ).
cnf(t15039,plain,
meet(join(X1,X2),join(X1,meet(X3,X2))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t1170441]) ).
cnf(t167,plain,
meet(X1,meet(meet(X2,complement(X1)),X3)) = meet(X3,zero),
inference(cp,[status(thm)],[t26,t162]) ).
cnf(t1169956,plain,
meet(X1,meet(X3,meet(X2,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t167,t23]) ).
cnf(t1169957,plain,
meet(X1,meet(X2,meet(complement(X1),X3))) = meet(X3,zero),
inference(step,[status(thm)],[t1169956,t26]) ).
cnf(t1169958,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t1169957,t23]) ).
cnf(t1169959,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(step,[status(thm)],[t1169958,t126]) ).
cnf(t206,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t1169959]) ).
cnf(t327,plain,
join(meet(X1,meet(X2,meet(X3,complement(X1)))),meet(X1,Y3)) = meet(X1,join(zero,meet(X1,Y3))),
inference(cp,[status(thm)],[t325,t206]) ).
cnf(t1169994,plain,
join(zero,meet(X1,Y3)) = meet(X1,join(zero,meet(X1,Y3))),
inference(step,[status(thm)],[t327,t206]) ).
cnf(t356,plain,
meet(X1,join(zero,meet(X1,X2))) = join(zero,meet(X1,X2)),
inference(orient,[status(thm)],[t1169994]) ).
cnf(t376,plain,
meet(X1,meet(join(zero,meet(X1,X2)),X3)) = meet(X3,join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t26,t356]) ).
cnf(t1169995,plain,
meet(X1,meet(X3,join(zero,meet(X1,X2)))) = meet(X3,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t376,t23]) ).
cnf(t378,plain,
meet(X1,meet(X2,join(zero,meet(X1,X3)))) = meet(X2,join(zero,meet(X1,X3))),
inference(orient,[status(thm)],[t1169995]) ).
cnf(t393,plain,
X1 = join(X1,meet(X2,join(zero,meet(X1,X3)))),
inference(cp,[status(thm)],[t16,t378]) ).
cnf(t404,plain,
join(X1,meet(X2,join(zero,meet(X1,X3)))) = X1,
inference(orient,[status(thm)],[t393]) ).
cnf(t413,plain,
X1 = join(X1,meet(X2,join(zero,join(meet(X1,X3),meet(X1,Y3))))),
inference(cp,[status(thm)],[t404,t46]) ).
cnf(t1270,plain,
join(X1,meet(X2,join(zero,join(meet(X1,X3),meet(X1,Y3))))) = X1,
inference(orient,[status(thm)],[t413]) ).
cnf(t100,plain,
join(meet(X1,complement(X1)),meet(X1,X2)) = meet(X1,join(meet(complement(X1),join(X1,X2)),meet(X2,one))),
inference(cp,[status(thm)],[t46,t97]) ).
cnf(t1170132,plain,
join(zero,meet(X1,X2)) = meet(X1,join(meet(complement(X1),join(X1,X2)),meet(X2,one))),
inference(step,[status(thm)],[t100,t62]) ).
cnf(t1170133,plain,
join(zero,meet(X1,X2)) = meet(X1,join(meet(X2,one),meet(complement(X1),join(X1,X2)))),
inference(step,[status(thm)],[t1170132,t67]) ).
cnf(t1170134,plain,
join(zero,meet(X1,X2)) = meet(X1,join(X2,meet(complement(X1),join(X1,X2)))),
inference(step,[status(thm)],[t1170133,t110]) ).
cnf(t1170135,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t1170134,t2274]) ).
cnf(t2359,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t1170135]) ).
cnf(t2367,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X3,join(X1,X2)))) = join(zero,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t2359,t46]) ).
cnf(t1170144,plain,
join(meet(X1,X2),meet(X1,X3)) = join(zero,join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t2367,t46]) ).
cnf(t2434,plain,
join(zero,join(meet(X1,X2),meet(X1,X3))) = join(meet(X1,X2),meet(X1,X3)),
inference(orient,[status(thm)],[t1170144]) ).
cnf(t1170145,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X1,Y3)))) = X1,
inference(step,[status(thm)],[t1270,t2434]) ).
cnf(t2477,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X1,Y3)))) = X1,
inference(rw,[status(thm)],[t1170145]) ).
cnf(t2571,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X1,Y3)))) = X1,
inference(orient,[status(thm)],[t2477]) ).
cnf(t15058,plain,
join(X1,meet(X2,meet(X3,join(meet(X1,Y3),meet(X1,Y4))))) = meet(X1,join(X1,meet(X2,meet(X3,join(meet(X1,Y3),meet(X1,Y4)))))),
inference(cp,[status(thm)],[t15039,t2571]) ).
cnf(t1170448,plain,
join(X1,meet(X2,meet(X3,join(meet(X1,Y3),meet(X1,Y4))))) = X1,
inference(step,[status(thm)],[t15058,t14]) ).
cnf(t16047,plain,
join(X1,meet(X2,meet(X3,join(meet(X1,Y3),meet(X1,Y4))))) = X1,
inference(orient,[status(thm)],[t1170448]) ).
cnf(t16150,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(Y3,join(join(X1,X2),meet(join(X1,X2),Y4))))),
inference(cp,[status(thm)],[t16047,t4034]) ).
cnf(t1170462,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t16150,t16]) ).
cnf(t17106,plain,
join(join(X1,X2),meet(X3,meet(Y3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t1170462]) ).
cnf(t17160,plain,
join(X1,complement(X2)) = join(join(X1,complement(X2)),meet(X3,meet(Y3,complement(X2)))),
inference(cp,[status(thm)],[t17106,t4464]) ).
cnf(t17270,plain,
join(join(X1,complement(X2)),meet(X3,meet(Y3,complement(X2)))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t17160]) ).
cnf(t17273,plain,
join(X1,complement(complement(X2))) = join(join(X1,X2),meet(X3,meet(Y3,complement(complement(X2))))),
inference(cp,[status(thm)],[t17270,t2811]) ).
cnf(t1170463,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(Y3,complement(complement(X2))))),
inference(step,[status(thm)],[t17273,t2811]) ).
cnf(t1170464,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(Y3,X2))),
inference(step,[status(thm)],[t1170463,t2811]) ).
cnf(t1170465,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(X2,Y3))),
inference(step,[status(thm)],[t1170464,t23]) ).
cnf(t1170466,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,meet(Y3,X3))),
inference(step,[status(thm)],[t1170465,t26]) ).
cnf(t1170467,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,meet(X3,Y3))),
inference(step,[status(thm)],[t1170466,t23]) ).
cnf(t17361,plain,
join(join(X1,X2),meet(X2,meet(X3,Y3))) = join(X1,X2),
inference(orient,[status(thm)],[t1170467]) ).
cnf(t3583,plain,
meet(complement(X1),join(X2,complement(X1))) = meet(complement(X1),meet(join(X2,complement(X1)),join(X3,complement(X1)))),
inference(cp,[status(thm)],[t3449,t3566]) ).
cnf(t1170231,plain,
complement(X1) = meet(complement(X1),meet(join(X2,complement(X1)),join(X3,complement(X1)))),
inference(step,[status(thm)],[t3583,t3566]) ).
cnf(t4778,plain,
meet(complement(X1),meet(join(X2,complement(X1)),join(X3,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t1170231]) ).
cnf(t17428,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,complement(X3))),
inference(cp,[status(thm)],[t17361,t4778]) ).
cnf(t17513,plain,
join(join(X1,X2),meet(X2,complement(X3))) = join(X1,X2),
inference(orient,[status(thm)],[t17428]) ).
cnf(t17525,plain,
join(X1,join(X2,meet(X1,X3))) = join(join(X1,X2),meet(join(X2,meet(X1,X3)),complement(Y3))),
inference(cp,[status(thm)],[t17513,t191]) ).
cnf(t1170494,plain,
join(X1,X2) = join(join(X1,X2),meet(join(X2,meet(X1,X3)),complement(Y3))),
inference(step,[status(thm)],[t17525,t191]) ).
cnf(t1170495,plain,
join(X1,X2) = join(join(X1,X2),meet(complement(Y3),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t1170494,t23]) ).
cnf(t20006,plain,
join(join(X1,X2),meet(complement(X3),join(X2,meet(X1,Y3)))) = join(X1,X2),
inference(orient,[status(thm)],[t1170495]) ).
cnf(t20068,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X2,meet(X1,Y3)))),
inference(cp,[status(thm)],[t20006,t2811]) ).
cnf(t20288,plain,
join(join(X1,X2),meet(X3,join(X2,meet(X1,Y3)))) = join(X1,X2),
inference(orient,[status(thm)],[t20068]) ).
cnf(t5122,plain,
meet(X1,meet(one,join(X2,X3))) = meet(meet(X1,join(X2,X3)),join(Y3,meet(X1,one))),
inference(cp,[status(thm)],[t5107,t1205]) ).
cnf(t1170238,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y3,meet(X1,one))),
inference(step,[status(thm)],[t5122,t1205]) ).
cnf(t1170239,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y3,X1)),
inference(step,[status(thm)],[t1170238,t110]) ).
cnf(t1170240,plain,
meet(X1,join(X2,X3)) = meet(join(Y3,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t1170239,t23]) ).
cnf(t1170241,plain,
meet(X1,join(X2,X3)) = meet(join(X2,X3),meet(join(Y3,X1),X1)),
inference(step,[status(thm)],[t1170240,t26]) ).
cnf(t1170242,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(Y3,X1))),
inference(step,[status(thm)],[t1170241,t26]) ).
cnf(t1170243,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,Y3))),
inference(step,[status(thm)],[t1170242,t67]) ).
cnf(t1170244,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,Y3),join(X2,X3))),
inference(step,[status(thm)],[t1170243,t23]) ).
cnf(t5227,plain,
meet(X1,meet(join(X1,X2),join(X3,Y3))) = meet(X1,join(X3,Y3)),
inference(orient,[status(thm)],[t1170244]) ).
cnf(t17404,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,join(X3,Y3))),
inference(cp,[status(thm)],[t17361,t5227]) ).
cnf(t17634,plain,
join(join(X1,X2),meet(X2,join(X3,Y3))) = join(X1,X2),
inference(orient,[status(thm)],[t17404]) ).
cnf(t17656,plain,
join(X1,meet(X1,X2)) = join(X1,meet(meet(X1,X2),join(X3,Y3))),
inference(cp,[status(thm)],[t17634,t16]) ).
cnf(t1170468,plain,
X1 = join(X1,meet(meet(X1,X2),join(X3,Y3))),
inference(step,[status(thm)],[t17656,t16]) ).
cnf(t17838,plain,
join(X1,meet(meet(X1,X2),join(X3,Y3))) = X1,
inference(orient,[status(thm)],[t1170468]) ).
cnf(t17922,plain,
meet(meet(X1,X2),join(X3,Y3)) = meet(meet(meet(X1,X2),join(X3,Y3)),X1),
inference(cp,[status(thm)],[t3973,t17838]) ).
cnf(t1170475,plain,
meet(meet(X1,X2),join(X3,Y3)) = meet(X1,meet(meet(X1,X2),join(X3,Y3))),
inference(step,[status(thm)],[t17922,t23]) ).
cnf(t18475,plain,
meet(X1,meet(meet(X1,X2),join(X3,Y3))) = meet(meet(X1,X2),join(X3,Y3)),
inference(orient,[status(thm)],[t1170475]) ).
cnf(t9462,plain,
meet(X1,meet(X2,complement(X1))) = meet(X1,meet(meet(X2,complement(X1)),join(X3,join(Y3,zero)))),
inference(cp,[status(thm)],[t9417,t162]) ).
cnf(t1170336,plain,
zero = meet(X1,meet(meet(X2,complement(X1)),join(X3,join(Y3,zero)))),
inference(step,[status(thm)],[t9462,t162]) ).
cnf(t1170337,plain,
zero = meet(X1,meet(meet(X2,complement(X1)),join(X3,Y3))),
inference(step,[status(thm)],[t1170336,t103]) ).
cnf(t1170338,plain,
zero = meet(X1,meet(join(X3,Y3),meet(X2,complement(X1)))),
inference(step,[status(thm)],[t1170337,t23]) ).
cnf(t1170339,plain,
zero = meet(X1,meet(complement(X1),meet(join(X3,Y3),X2))),
inference(step,[status(thm)],[t1170338,t26]) ).
cnf(t1170340,plain,
zero = meet(X1,meet(X2,meet(complement(X1),join(X3,Y3)))),
inference(step,[status(thm)],[t1170339,t26]) ).
cnf(t10402,plain,
meet(X1,meet(X2,meet(complement(X1),join(X3,Y3)))) = zero,
inference(orient,[status(thm)],[t1170340]) ).
cnf(t10407,plain,
zero = meet(X1,meet(X2,join(meet(complement(X1),X3),meet(complement(X1),Y3)))),
inference(cp,[status(thm)],[t10402,t46]) ).
cnf(t1170428,plain,
zero = meet(X1,meet(X2,join(meet(X3,complement(X1)),meet(complement(X1),Y3)))),
inference(step,[status(thm)],[t10407,t23]) ).
cnf(t1170429,plain,
zero = meet(X1,meet(X2,join(meet(X3,complement(X1)),meet(Y3,complement(X1))))),
inference(step,[status(thm)],[t1170428,t23]) ).
cnf(t14153,plain,
meet(X1,meet(X2,join(meet(X3,complement(X1)),meet(Y3,complement(X1))))) = zero,
inference(orient,[status(thm)],[t1170429]) ).
cnf(t18481,plain,
meet(meet(X1,X2),join(meet(X3,complement(X1)),meet(Y3,complement(X1)))) = zero,
inference(cp,[status(thm)],[t18475,t14153]) ).
cnf(t21275,plain,
meet(meet(X1,X2),join(meet(X3,complement(X1)),meet(Y3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t18481]) ).
cnf(t8809,plain,
meet(complement(X1),join(X2,meet(X1,join(X2,complement(X1))))) = meet(complement(X1),join(meet(X2,X3),meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t8776,t2843]) ).
cnf(t1170391,plain,
meet(X2,complement(X1)) = meet(complement(X1),join(meet(X2,X3),meet(X2,complement(X1)))),
inference(step,[status(thm)],[t8809,t2843]) ).
cnf(t12015,plain,
meet(complement(X1),join(meet(X2,X3),meet(X2,complement(X1)))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t1170391]) ).
cnf(t21294,plain,
zero = meet(meet(X1,complement(X2)),join(meet(X3,complement(complement(X2))),meet(Y3,complement(complement(X2))))),
inference(cp,[status(thm)],[t21275,t12015]) ).
cnf(t1170503,plain,
zero = meet(meet(X1,complement(X2)),join(meet(X3,X2),meet(Y3,complement(complement(X2))))),
inference(step,[status(thm)],[t21294,t2811]) ).
cnf(t1170504,plain,
zero = meet(meet(X1,complement(X2)),join(meet(X2,X3),meet(Y3,complement(complement(X2))))),
inference(step,[status(thm)],[t1170503,t23]) ).
cnf(t1170505,plain,
zero = meet(meet(X1,complement(X2)),join(meet(X2,X3),meet(Y3,X2))),
inference(step,[status(thm)],[t1170504,t2811]) ).
cnf(t1170506,plain,
zero = meet(meet(X1,complement(X2)),join(meet(X2,X3),meet(X2,Y3))),
inference(step,[status(thm)],[t1170505,t23]) ).
cnf(t21400,plain,
meet(meet(X1,complement(X2)),join(meet(X2,X3),meet(X2,Y3))) = zero,
inference(orient,[status(thm)],[t1170506]) ).
cnf(t21632,plain,
join(meet(X1,complement(X2)),X3) = join(join(meet(X1,complement(X2)),X3),meet(Y3,join(X3,zero))),
inference(cp,[status(thm)],[t20288,t21400]) ).
cnf(t1170507,plain,
join(X3,meet(X1,complement(X2))) = join(join(meet(X1,complement(X2)),X3),meet(Y3,join(X3,zero))),
inference(step,[status(thm)],[t21632,t67]) ).
cnf(t1170508,plain,
join(X3,meet(X1,complement(X2))) = join(meet(Y3,join(X3,zero)),join(meet(X1,complement(X2)),X3)),
inference(step,[status(thm)],[t1170507,t67]) ).
cnf(t1170509,plain,
join(X3,meet(X1,complement(X2))) = join(X3,join(meet(Y3,join(X3,zero)),meet(X1,complement(X2)))),
inference(step,[status(thm)],[t1170508,t73]) ).
cnf(t1170510,plain,
join(X3,meet(X1,complement(X2))) = join(X3,join(meet(X1,complement(X2)),meet(Y3,join(X3,zero)))),
inference(step,[status(thm)],[t1170509,t67]) ).
cnf(t1170511,plain,
join(X3,meet(X1,complement(X2))) = join(X3,join(meet(X1,complement(X2)),meet(Y3,X3))),
inference(step,[status(thm)],[t1170510,t103]) ).
cnf(t1170512,plain,
join(X3,meet(X1,complement(X2))) = join(X3,join(meet(X1,complement(X2)),meet(X3,Y3))),
inference(step,[status(thm)],[t1170511,t23]) ).
cnf(t1170513,plain,
join(X3,meet(X1,complement(X2))) = join(X3,join(meet(X3,Y3),meet(X1,complement(X2)))),
inference(step,[status(thm)],[t1170512,t67]) ).
cnf(t21688,plain,
join(X1,join(meet(X1,X2),meet(X3,complement(Y3)))) = join(X1,meet(X3,complement(Y3))),
inference(orient,[status(thm)],[t1170513]) ).
cnf(t21714,plain,
join(X1,meet(X2,complement(complement(X3)))) = join(X1,join(meet(X1,Y3),meet(X2,X3))),
inference(cp,[status(thm)],[t21688,t2811]) ).
cnf(t1170514,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X1,Y3),meet(X2,X3))),
inference(step,[status(thm)],[t21714,t2811]) ).
cnf(t21758,plain,
join(X1,join(meet(X1,X2),meet(X3,Y3))) = join(X1,meet(X3,Y3)),
inference(orient,[status(thm)],[t1170514]) ).
cnf(t21767,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X2,Y3)))) = join(X1,join(meet(X1,X3),meet(X2,Y3))),
inference(cp,[status(thm)],[t21758,t6642]) ).
cnf(t1170515,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X2,Y3)))) = join(X1,meet(X2,Y3)),
inference(step,[status(thm)],[t21767,t21758]) ).
cnf(t21864,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(X2,Y3)))) = join(X1,meet(X2,Y3)),
inference(orient,[status(thm)],[t1170515]) ).
cnf(t21928,plain,
join(X1,meet(X2,join(X3,meet(complement(X2),join(X3,X2))))) = join(X1,meet(X2,join(meet(X1,Y3),meet(X3,X2)))),
inference(cp,[status(thm)],[t21864,t2904]) ).
cnf(t1170516,plain,
join(X1,meet(X3,X2)) = join(X1,meet(X2,join(meet(X1,Y3),meet(X3,X2)))),
inference(step,[status(thm)],[t21928,t2904]) ).
cnf(t22036,plain,
join(X1,meet(X2,join(meet(X1,X3),meet(Y3,X2)))) = join(X1,meet(Y3,X2)),
inference(orient,[status(thm)],[t1170516]) ).
cnf(t22188,plain,
join(X1,meet(X2,join(X2,X3))) = join(X1,meet(join(X2,X3),join(meet(X1,Y3),X2))),
inference(cp,[status(thm)],[t22036,t14]) ).
cnf(t1170517,plain,
join(X1,X2) = join(X1,meet(join(X2,X3),join(meet(X1,Y3),X2))),
inference(step,[status(thm)],[t22188,t14]) ).
cnf(t1170518,plain,
join(X1,X2) = join(X1,meet(join(X2,X3),join(X2,meet(X1,Y3)))),
inference(step,[status(thm)],[t1170517,t67]) ).
cnf(t22339,plain,
join(X1,meet(join(X2,X3),join(X2,meet(X1,Y3)))) = join(X1,X2),
inference(orient,[status(thm)],[t1170518]) ).
cnf(t22519,plain,
zero = meet(complement(join(X1,X2)),join(meet(join(X1,X2),X3),X1)),
inference(cp,[status(thm)],[t10521,t22339]) ).
cnf(t1170519,plain,
zero = meet(complement(join(X1,X2)),join(X1,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t22519,t67]) ).
cnf(t1170520,plain,
zero = meet(complement(join(X1,X2)),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t1170519,t23]) ).
cnf(t22609,plain,
meet(complement(join(X1,X2)),join(X1,meet(X3,join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t1170520]) ).
cnf(t22643,plain,
zero = meet(complement(join(X1,X2)),join(X2,meet(X3,join(X2,X1)))),
inference(cp,[status(thm)],[t22609,t67]) ).
cnf(t1170563,plain,
zero = meet(complement(join(X1,X2)),join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t22643,t67]) ).
cnf(t25838,plain,
meet(complement(join(X1,X2)),join(X2,meet(X3,join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t1170563]) ).
cnf(t25959,plain,
zero = meet(complement(join(X1,X2)),join(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t25838,t4196]) ).
cnf(t1170570,plain,
zero = meet(complement(join(X1,X2)),join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t25959,t23]) ).
cnf(t26784,plain,
meet(complement(join(X1,X2)),join(X2,meet(X1,X3))) = zero,
inference(orient,[status(thm)],[t1170570]) ).
cnf(t26860,plain,
zero = meet(complement(join(join(X1,X2),X3)),join(X3,meet(X1,Y3))),
inference(cp,[status(thm)],[t26784,t7509]) ).
cnf(t1170673,plain,
zero = meet(join(X3,meet(X1,Y3)),complement(join(join(X1,X2),X3))),
inference(step,[status(thm)],[t26860,t23]) ).
cnf(t1170674,plain,
zero = meet(join(X3,meet(X1,Y3)),complement(join(X3,join(X1,X2)))),
inference(step,[status(thm)],[t1170673,t67]) ).
cnf(t1170675,plain,
zero = meet(join(X3,meet(X1,Y3)),complement(join(X2,join(X3,X1)))),
inference(step,[status(thm)],[t1170674,t73]) ).
cnf(t1170676,plain,
zero = meet(join(X3,meet(X1,Y3)),complement(join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t1170675,t73]) ).
cnf(t37262,plain,
meet(join(X1,meet(X2,X3)),complement(join(X2,join(Y3,X1)))) = zero,
inference(orient,[status(thm)],[t1170676]) ).
cnf(t37501,plain,
zero = meet(join(meet(X1,X2),meet(X3,Y3)),complement(join(X3,X1))),
inference(cp,[status(thm)],[t37262,t16]) ).
cnf(t1170703,plain,
zero = meet(complement(join(X3,X1)),join(meet(X1,X2),meet(X3,Y3))),
inference(step,[status(thm)],[t37501,t23]) ).
cnf(t1170704,plain,
zero = meet(complement(join(X1,X3)),join(meet(X1,X2),meet(X3,Y3))),
inference(step,[status(thm)],[t1170703,t67]) ).
cnf(t42172,plain,
meet(complement(join(X1,X2)),join(meet(X1,X3),meet(X2,Y3))) = zero,
inference(orient,[status(thm)],[t1170704]) ).
cnf(t42632,plain,
zero = meet(complement(join(meet(X1,X2),meet(X3,Y3))),join(meet(X1,X2),zero)),
inference(cp,[status(thm)],[t22609,t42172]) ).
cnf(t1170717,plain,
zero = meet(complement(join(meet(X1,X2),meet(X3,Y3))),meet(X1,X2)),
inference(step,[status(thm)],[t42632,t103]) ).
cnf(t1170718,plain,
zero = meet(X2,meet(complement(join(meet(X1,X2),meet(X3,Y3))),X1)),
inference(step,[status(thm)],[t1170717,t26]) ).
cnf(t1170719,plain,
zero = meet(X1,meet(X2,complement(join(meet(X1,X2),meet(X3,Y3))))),
inference(step,[status(thm)],[t1170718,t26]) ).
cnf(t46267,plain,
meet(X1,meet(X2,complement(join(meet(X1,X2),meet(X3,Y3))))) = zero,
inference(orient,[status(thm)],[t1170719]) ).
cnf(t46445,plain,
zero = meet(X1,meet(X2,complement(join(meet(X1,X2),join(X3,Y3))))),
inference(cp,[status(thm)],[t46267,t4034]) ).
cnf(t1170727,plain,
zero = meet(X1,meet(X2,complement(join(Y3,join(meet(X1,X2),X3))))),
inference(step,[status(thm)],[t46445,t73]) ).
cnf(t1170728,plain,
zero = meet(X1,meet(X2,complement(join(X3,join(Y3,meet(X1,X2)))))),
inference(step,[status(thm)],[t1170727,t73]) ).
cnf(t48631,plain,
meet(X1,meet(X2,complement(join(X3,join(Y3,meet(X1,X2)))))) = zero,
inference(orient,[status(thm)],[t1170728]) ).
cnf(t6783,plain,
join(X1,meet(meet(X2,X3),join(X3,Y3))) = join(X1,meet(join(X3,Y3),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t6746,t4196]) ).
cnf(t1170286,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X3,Y3),join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t6783,t4196]) ).
cnf(t7614,plain,
join(X1,meet(join(X2,X3),join(X1,meet(Y3,X2)))) = join(X1,meet(Y3,X2)),
inference(orient,[status(thm)],[t1170286]) ).
cnf(t7620,plain,
join(meet(join(X1,X2),X3),meet(X3,X1)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(cp,[status(thm)],[t7614,t6344]) ).
cnf(t1170287,plain,
join(meet(X3,X1),meet(join(X1,X2),X3)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t7620,t67]) ).
cnf(t1170288,plain,
join(meet(X1,X3),meet(join(X1,X2),X3)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t1170287,t23]) ).
cnf(t1170289,plain,
join(meet(X1,X3),meet(X3,join(X1,X2))) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t1170288,t23]) ).
cnf(t1170290,plain,
join(meet(X1,X3),meet(X3,join(X1,X2))) = meet(join(X1,X2),X3),
inference(step,[status(thm)],[t1170289,t15]) ).
cnf(t1170291,plain,
join(meet(X1,X3),meet(X3,join(X1,X2))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t1170290,t23]) ).
cnf(t7736,plain,
join(meet(X1,X2),meet(X2,join(X1,X3))) = meet(X2,join(X1,X3)),
inference(orient,[status(thm)],[t1170291]) ).
cnf(t7755,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(join(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t7736,t14]) ).
cnf(t7908,plain,
join(X1,meet(join(X1,X2),join(X1,X3))) = meet(join(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t7755]) ).
cnf(t22475,plain,
join(complement(X1),X2) = join(complement(X1),meet(join(X2,X3),join(X2,complement(X1)))),
inference(cp,[status(thm)],[t22339,t4778]) ).
cnf(t1171105,plain,
join(X2,complement(X1)) = join(complement(X1),meet(join(X2,X3),join(X2,complement(X1)))),
inference(step,[status(thm)],[t22475,t67]) ).
cnf(t88614,plain,
join(complement(X1),meet(join(X2,X3),join(X2,complement(X1)))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t1171105]) ).
cnf(t88616,plain,
join(X1,complement(complement(X2))) = join(X2,meet(join(X1,X3),join(X1,complement(complement(X2))))),
inference(cp,[status(thm)],[t88614,t2811]) ).
cnf(t1171106,plain,
join(X1,X2) = join(X2,meet(join(X1,X3),join(X1,complement(complement(X2))))),
inference(step,[status(thm)],[t88616,t2811]) ).
cnf(t1171107,plain,
join(X1,X2) = join(X2,meet(join(X1,X3),join(X1,X2))),
inference(step,[status(thm)],[t1171106,t2811]) ).
cnf(t1171108,plain,
join(X1,X2) = join(X2,meet(join(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t1171107,t23]) ).
cnf(t89154,plain,
join(X1,meet(join(X2,X1),join(X2,X3))) = join(X2,X1),
inference(orient,[status(thm)],[t1171108]) ).
cnf(t89622,plain,
meet(join(X1,meet(join(X2,X1),join(X2,X3))),join(X1,Y3)) = join(X1,meet(join(X2,X1),join(X1,Y3))),
inference(cp,[status(thm)],[t7908,t89154]) ).
cnf(t1171110,plain,
meet(join(X2,X1),join(X1,Y3)) = join(X1,meet(join(X2,X1),join(X1,Y3))),
inference(step,[status(thm)],[t89622,t89154]) ).
cnf(t91091,plain,
join(X1,meet(join(X2,X1),join(X1,X3))) = meet(join(X2,X1),join(X1,X3)),
inference(orient,[status(thm)],[t1171110]) ).
cnf(t91102,plain,
meet(join(X1,X2),join(X2,meet(complement(join(X1,X2)),join(join(X1,X2),X2)))) = join(X2,meet(join(X1,X2),X2)),
inference(cp,[status(thm)],[t91091,t2274]) ).
cnf(t1171111,plain,
meet(join(X1,X2),X2) = join(X2,meet(join(X1,X2),X2)),
inference(step,[status(thm)],[t91102,t2274]) ).
cnf(t1171112,plain,
meet(X2,join(X1,X2)) = join(X2,meet(join(X1,X2),X2)),
inference(step,[status(thm)],[t1171111,t23]) ).
cnf(t1171113,plain,
meet(X2,join(X1,X2)) = X2,
inference(step,[status(thm)],[t1171112,t3095]) ).
cnf(t91717,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t1171113]) ).
cnf(t101,plain,
join(X1,join(complement(X1),X2)) = join(X2,one),
inference(cp,[status(thm)],[t73,t97]) ).
cnf(t1169948,plain,
join(X1,join(X2,complement(X1))) = join(X2,one),
inference(step,[status(thm)],[t101,t67]) ).
cnf(t1169949,plain,
join(X1,join(X2,complement(X1))) = one,
inference(step,[status(thm)],[t1169948,t143]) ).
cnf(t169,plain,
join(X1,join(X2,complement(X1))) = one,
inference(orient,[status(thm)],[t1169949]) ).
cnf(t173,plain,
join(X1,complement(X2)) = ifeq(meet(X2,join(X1,complement(X2))),zero,ifeq(one,one,complement(X2),join(X1,complement(X2))),join(X1,complement(X2))),
inference(cp,[status(thm)],[t18,t169]) ).
cnf(t1170960,plain,
join(X1,complement(X2)) = ifeq(meet(X2,join(X1,complement(X2))),zero,complement(X2),join(X1,complement(X2))),
inference(step,[status(thm)],[t173,t17]) ).
cnf(t69883,plain,
ifeq(meet(X1,join(X2,complement(X1))),zero,complement(X1),join(X2,complement(X1))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t1170960]) ).
cnf(t2310,plain,
meet(X1,meet(join(X2,meet(complement(X1),join(X1,X2))),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t26,t2274]) ).
cnf(t1170154,plain,
meet(X1,meet(X3,join(X2,meet(complement(X1),join(X1,X2))))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t2310,t23]) ).
cnf(t1170155,plain,
meet(X1,meet(X3,join(X2,meet(complement(X1),join(X1,X2))))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t1170154,t26]) ).
cnf(t1170156,plain,
meet(X1,meet(X3,join(X2,meet(complement(X1),join(X1,X2))))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t1170155,t26]) ).
cnf(t2628,plain,
meet(X1,meet(X2,join(X3,meet(complement(X1),join(X1,X3))))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t1170156]) ).
cnf(t22780,plain,
join(complement(join(X1,X2)),X3) = join(join(complement(join(X1,X2)),X3),meet(Y3,join(X3,zero))),
inference(cp,[status(thm)],[t20288,t22609]) ).
cnf(t1170736,plain,
join(X3,complement(join(X1,X2))) = join(join(complement(join(X1,X2)),X3),meet(Y3,join(X3,zero))),
inference(step,[status(thm)],[t22780,t67]) ).
cnf(t1170737,plain,
join(X3,complement(join(X1,X2))) = join(meet(Y3,join(X3,zero)),join(complement(join(X1,X2)),X3)),
inference(step,[status(thm)],[t1170736,t67]) ).
cnf(t1170738,plain,
join(X3,complement(join(X1,X2))) = join(X3,join(meet(Y3,join(X3,zero)),complement(join(X1,X2)))),
inference(step,[status(thm)],[t1170737,t73]) ).
cnf(t1170739,plain,
join(X3,complement(join(X1,X2))) = join(X3,join(complement(join(X1,X2)),meet(Y3,join(X3,zero)))),
inference(step,[status(thm)],[t1170738,t67]) ).
cnf(t1170740,plain,
join(X3,complement(join(X1,X2))) = join(X3,join(complement(join(X1,X2)),meet(Y3,X3))),
inference(step,[status(thm)],[t1170739,t103]) ).
cnf(t1170741,plain,
join(X3,complement(join(X1,X2))) = join(X3,join(complement(join(X1,X2)),meet(X3,Y3))),
inference(step,[status(thm)],[t1170740,t23]) ).
cnf(t1170742,plain,
join(X3,complement(join(X1,X2))) = join(X3,join(meet(X3,Y3),complement(join(X1,X2)))),
inference(step,[status(thm)],[t1170741,t67]) ).
cnf(t50657,plain,
join(X1,join(meet(X1,X2),complement(join(X3,Y3)))) = join(X1,complement(join(X3,Y3))),
inference(orient,[status(thm)],[t1170742]) ).
cnf(t50703,plain,
join(X1,complement(join(meet(X2,X3),meet(X2,meet(X3,Y3))))) = join(X1,join(meet(X1,Y4),complement(meet(X2,X3)))),
inference(cp,[status(thm)],[t50657,t3160]) ).
cnf(t1170744,plain,
join(X1,complement(meet(X2,X3))) = join(X1,join(meet(X1,Y4),complement(meet(X2,X3)))),
inference(step,[status(thm)],[t50703,t3160]) ).
cnf(t51197,plain,
join(X1,join(meet(X1,X2),complement(meet(X3,Y3)))) = join(X1,complement(meet(X3,Y3))),
inference(orient,[status(thm)],[t1170744]) ).
cnf(t51199,plain,
join(X1,complement(meet(X1,X2))) = join(X1,one),
inference(cp,[status(thm)],[t51197,t97]) ).
cnf(t1170745,plain,
join(X1,complement(meet(X1,X2))) = one,
inference(step,[status(thm)],[t51199,t143]) ).
cnf(t51309,plain,
join(X1,complement(meet(X1,X2))) = one,
inference(orient,[status(thm)],[t1170745]) ).
cnf(t51401,plain,
meet(X1,meet(complement(meet(X1,X2)),X3)) = meet(X1,meet(X3,join(complement(meet(X1,X2)),meet(complement(X1),one)))),
inference(cp,[status(thm)],[t2628,t51309]) ).
cnf(t1172353,plain,
meet(X1,meet(X3,complement(meet(X1,X2)))) = meet(X1,meet(X3,join(complement(meet(X1,X2)),meet(complement(X1),one)))),
inference(step,[status(thm)],[t51401,t23]) ).
cnf(t1172354,plain,
meet(X1,meet(X3,complement(meet(X1,X2)))) = meet(X1,meet(X3,join(meet(complement(X1),one),complement(meet(X1,X2))))),
inference(step,[status(thm)],[t1172353,t67]) ).
cnf(t1172355,plain,
meet(X1,meet(X3,complement(meet(X1,X2)))) = meet(X1,meet(X3,join(complement(X1),complement(meet(X1,X2))))),
inference(step,[status(thm)],[t1172354,t110]) ).
cnf(t417100,plain,
meet(X1,meet(X2,join(complement(X1),complement(meet(X1,X3))))) = meet(X1,meet(X2,complement(meet(X1,X3)))),
inference(orient,[status(thm)],[t1172355]) ).
cnf(t417105,plain,
meet(X1,meet(meet(X1,X2),complement(meet(X1,X3)))) = meet(meet(X1,X2),join(complement(X1),complement(meet(X1,X3)))),
inference(cp,[status(thm)],[t417100,t18475]) ).
cnf(t9058,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X2,Y3))) = meet(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t5227,t8913]) ).
cnf(t1170358,plain,
meet(X1,join(meet(X2,Y3),meet(X2,join(X1,X3)))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t9058,t67]) ).
cnf(t1170359,plain,
meet(X1,join(meet(X2,Y3),meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(step,[status(thm)],[t1170358,t178]) ).
cnf(t10998,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,Y3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170359]) ).
cnf(t11134,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),join(meet(X3,Y3),meet(X3,X1))),
inference(cp,[status(thm)],[t10998,t10998]) ).
cnf(t1170403,plain,
meet(X3,meet(X1,X2)) = meet(meet(X1,X2),join(meet(X3,Y3),meet(X3,X1))),
inference(step,[status(thm)],[t11134,t23]) ).
cnf(t1170404,plain,
meet(X2,meet(X3,X1)) = meet(meet(X1,X2),join(meet(X3,Y3),meet(X3,X1))),
inference(step,[status(thm)],[t1170403,t26]) ).
cnf(t1170405,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X3,Y3),meet(X3,X1))),
inference(step,[status(thm)],[t1170404,t26]) ).
cnf(t1170406,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X3,X1),meet(X3,Y3))),
inference(step,[status(thm)],[t1170405,t67]) ).
cnf(t1170407,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X1,X3),meet(X3,Y3))),
inference(step,[status(thm)],[t1170406,t23]) ).
cnf(t13008,plain,
meet(meet(X1,X2),join(meet(X1,X3),meet(X3,Y3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t1170407]) ).
cnf(t22518,plain,
meet(X1,meet(X2,join(X3,Y3))) = meet(meet(X1,X2),join(meet(X1,join(X3,Y3)),X3)),
inference(cp,[status(thm)],[t13008,t22339]) ).
cnf(t1171413,plain,
meet(X1,meet(X2,join(X3,Y3))) = meet(meet(X1,X2),join(X3,meet(X1,join(X3,Y3)))),
inference(step,[status(thm)],[t22518,t67]) ).
cnf(t137153,plain,
meet(meet(X1,X2),join(X3,meet(X1,join(X3,Y3)))) = meet(X1,meet(X2,join(X3,Y3))),
inference(orient,[status(thm)],[t1171413]) ).
cnf(t137545,plain,
meet(X1,meet(X2,join(X3,meet(join(Y3,X3),join(Y3,Y4))))) = meet(meet(X1,X2),join(X3,meet(X1,join(Y3,X3)))),
inference(cp,[status(thm)],[t137153,t89154]) ).
cnf(t1171440,plain,
meet(X1,meet(X2,join(Y3,X3))) = meet(meet(X1,X2),join(X3,meet(X1,join(Y3,X3)))),
inference(step,[status(thm)],[t137545,t89154]) ).
cnf(t150241,plain,
meet(meet(X1,X2),join(X3,meet(X1,join(Y3,X3)))) = meet(X1,meet(X2,join(Y3,X3))),
inference(orient,[status(thm)],[t1171440]) ).
cnf(t150586,plain,
meet(X1,meet(X2,join(meet(X3,X1),meet(X3,Y3)))) = meet(meet(X1,X2),join(meet(X3,Y3),meet(X3,X1))),
inference(cp,[status(thm)],[t150241,t8913]) ).
cnf(t151419,plain,
meet(meet(X1,X2),join(meet(X3,X1),meet(X3,Y3))) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t150586]) ).
cnf(t37507,plain,
zero = meet(join(meet(X1,X2),meet(X3,Y3)),complement(join(X3,X2))),
inference(cp,[status(thm)],[t37262,t3095]) ).
cnf(t1170710,plain,
zero = meet(complement(join(X3,X2)),join(meet(X1,X2),meet(X3,Y3))),
inference(step,[status(thm)],[t37507,t23]) ).
cnf(t1170711,plain,
zero = meet(complement(join(X2,X3)),join(meet(X1,X2),meet(X3,Y3))),
inference(step,[status(thm)],[t1170710,t67]) ).
cnf(t43169,plain,
meet(complement(join(X1,X2)),join(meet(X3,X1),meet(X2,Y3))) = zero,
inference(orient,[status(thm)],[t1170711]) ).
cnf(t43347,plain,
zero = meet(complement(join(join(X1,X2),X3)),join(X1,meet(X3,Y3))),
inference(cp,[status(thm)],[t43169,t14]) ).
cnf(t1170722,plain,
zero = meet(join(X1,meet(X3,Y3)),complement(join(join(X1,X2),X3))),
inference(step,[status(thm)],[t43347,t23]) ).
cnf(t1170723,plain,
zero = meet(join(X1,meet(X3,Y3)),complement(join(X3,join(X1,X2)))),
inference(step,[status(thm)],[t1170722,t67]) ).
cnf(t1170724,plain,
zero = meet(join(X1,meet(X3,Y3)),complement(join(X2,join(X3,X1)))),
inference(step,[status(thm)],[t1170723,t73]) ).
cnf(t1170725,plain,
zero = meet(join(X1,meet(X3,Y3)),complement(join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t1170724,t73]) ).
cnf(t47251,plain,
meet(join(X1,meet(X2,X3)),complement(join(X1,join(Y3,X2)))) = zero,
inference(orient,[status(thm)],[t1170725]) ).
cnf(t47339,plain,
zero = meet(join(X1,meet(meet(X2,X3),Y3)),complement(join(X1,X3))),
inference(cp,[status(thm)],[t47251,t3095]) ).
cnf(t1170731,plain,
zero = meet(complement(join(X1,X3)),join(X1,meet(meet(X2,X3),Y3))),
inference(step,[status(thm)],[t47339,t23]) ).
cnf(t1170732,plain,
zero = meet(complement(join(X1,X3)),join(X1,meet(Y3,meet(X2,X3)))),
inference(step,[status(thm)],[t1170731,t23]) ).
cnf(t1170733,plain,
zero = meet(complement(join(X1,X3)),join(X1,meet(X3,meet(Y3,X2)))),
inference(step,[status(thm)],[t1170732,t26]) ).
cnf(t1170734,plain,
zero = meet(complement(join(X1,X3)),join(X1,meet(X2,meet(X3,Y3)))),
inference(step,[status(thm)],[t1170733,t26]) ).
cnf(t49488,plain,
meet(complement(join(X1,X2)),join(X1,meet(X3,meet(X2,Y3)))) = zero,
inference(orient,[status(thm)],[t1170734]) ).
cnf(t151931,plain,
meet(complement(join(X1,X2)),meet(X3,Y3)) = meet(meet(X3,Y3),join(meet(complement(join(X1,X2)),X3),zero)),
inference(cp,[status(thm)],[t151419,t49488]) ).
cnf(t1171442,plain,
meet(complement(join(X1,X2)),meet(X3,Y3)) = meet(meet(X3,Y3),meet(complement(join(X1,X2)),X3)),
inference(step,[status(thm)],[t151931,t103]) ).
cnf(t1171443,plain,
meet(Y3,meet(complement(join(X1,X2)),X3)) = meet(meet(X3,Y3),meet(complement(join(X1,X2)),X3)),
inference(step,[status(thm)],[t1171442,t26]) ).
cnf(t1171444,plain,
meet(X3,meet(Y3,complement(join(X1,X2)))) = meet(meet(X3,Y3),meet(complement(join(X1,X2)),X3)),
inference(step,[status(thm)],[t1171443,t26]) ).
cnf(t1171445,plain,
meet(X3,meet(Y3,complement(join(X1,X2)))) = meet(X3,meet(meet(X3,Y3),complement(join(X1,X2)))),
inference(step,[status(thm)],[t1171444,t26]) ).
cnf(t153727,plain,
meet(X1,meet(meet(X1,X2),complement(join(X3,Y3)))) = meet(X1,meet(X2,complement(join(X3,Y3)))),
inference(orient,[status(thm)],[t1171445]) ).
cnf(t154024,plain,
meet(X1,meet(X2,complement(join(meet(X3,Y3),meet(X3,meet(Y3,Y4)))))) = meet(X1,meet(meet(X1,X2),complement(meet(X3,Y3)))),
inference(cp,[status(thm)],[t153727,t3160]) ).
cnf(t1171450,plain,
meet(X1,meet(X2,complement(meet(X3,Y3)))) = meet(X1,meet(meet(X1,X2),complement(meet(X3,Y3)))),
inference(step,[status(thm)],[t154024,t3160]) ).
cnf(t154970,plain,
meet(X1,meet(meet(X1,X2),complement(meet(X3,Y3)))) = meet(X1,meet(X2,complement(meet(X3,Y3)))),
inference(orient,[status(thm)],[t1171450]) ).
cnf(t1173577,plain,
meet(X1,meet(X2,complement(meet(X1,X3)))) = meet(meet(X1,X2),join(complement(X1),complement(meet(X1,X3)))),
inference(step,[status(thm)],[t417105,t154970]) ).
cnf(t886520,plain,
meet(meet(X1,X2),join(complement(X1),complement(meet(X1,X3)))) = meet(X1,meet(X2,complement(meet(X1,X3)))),
inference(orient,[status(thm)],[t1173577]) ).
cnf(t887879,plain,
join(complement(X1),complement(meet(X1,X2))) = ifeq(meet(X1,meet(X2,complement(meet(X1,X2)))),zero,complement(meet(X1,X2)),join(complement(X1),complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t69883,t886520]) ).
cnf(t9102,plain,
meet(meet(X1,complement(meet(X1,X2))),meet(X1,X2)) = meet(meet(X1,X2),join(meet(X1,complement(meet(X1,X2))),meet(X1,complement(meet(X1,X2))))),
inference(cp,[status(thm)],[t2904,t8913]) ).
cnf(t1170297,plain,
meet(X2,meet(meet(X1,complement(meet(X1,X2))),X1)) = meet(meet(X1,X2),join(meet(X1,complement(meet(X1,X2))),meet(X1,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t9102,t26]) ).
cnf(t1170298,plain,
meet(X1,meet(X2,meet(X1,complement(meet(X1,X2))))) = meet(meet(X1,X2),join(meet(X1,complement(meet(X1,X2))),meet(X1,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t1170297,t26]) ).
cnf(t1170299,plain,
meet(X1,meet(X1,meet(complement(meet(X1,X2)),X2))) = meet(meet(X1,X2),join(meet(X1,complement(meet(X1,X2))),meet(X1,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t1170298,t26]) ).
cnf(t1170300,plain,
meet(X1,meet(complement(meet(X1,X2)),X2)) = meet(meet(X1,X2),join(meet(X1,complement(meet(X1,X2))),meet(X1,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t1170299,t115]) ).
cnf(t1170301,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = meet(meet(X1,X2),join(meet(X1,complement(meet(X1,X2))),meet(X1,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t1170300,t23]) ).
cnf(t1170302,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = meet(meet(X1,X2),meet(X1,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t1170301,t15]) ).
cnf(t1170303,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = zero,
inference(step,[status(thm)],[t1170302,t162]) ).
cnf(t9128,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t1170303]) ).
cnf(t1173578,plain,
join(complement(X1),complement(meet(X1,X2))) = ifeq(zero,zero,complement(meet(X1,X2)),join(complement(X1),complement(meet(X1,X2)))),
inference(step,[status(thm)],[t887879,t9128]) ).
cnf(t1173579,plain,
join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t1173578,t17]) ).
cnf(t888679,plain,
join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t1173579]) ).
cnf(t18556,plain,
meet(X1,X2) = meet(X2,join(meet(X1,X2),meet(meet(X1,X3),join(Y3,Y4)))),
inference(cp,[status(thm)],[t8913,t18475]) ).
cnf(t218241,plain,
meet(X1,join(meet(X2,X1),meet(meet(X2,X3),join(Y3,Y4)))) = meet(X2,X1),
inference(orient,[status(thm)],[t18556]) ).
cnf(t888691,plain,
complement(meet(X1,join(meet(X2,X1),meet(meet(X2,X3),join(Y3,Y4))))) = join(complement(X1),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t888679,t218241]) ).
cnf(t1173583,plain,
complement(meet(X2,X1)) = join(complement(X1),complement(meet(X2,X1))),
inference(step,[status(thm)],[t888691,t218241]) ).
cnf(t891711,plain,
join(complement(X1),complement(meet(X2,X1))) = complement(meet(X2,X1)),
inference(orient,[status(thm)],[t1173583]) ).
cnf(t891759,plain,
complement(meet(X1,join(X2,X1))) = join(complement(join(X2,X1)),complement(X1)),
inference(cp,[status(thm)],[t891711,t91717]) ).
cnf(t1173584,plain,
complement(X1) = join(complement(join(X2,X1)),complement(X1)),
inference(step,[status(thm)],[t891759,t91717]) ).
cnf(t1173585,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(step,[status(thm)],[t1173584,t67]) ).
cnf(t1173586,plain,
complement(X1) = join(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t1173585,t67]) ).
cnf(t892868,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t1173586]) ).
cnf(t892903,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t91717,t892868]) ).
cnf(t1173594,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t892903,t23]) ).
cnf(t899096,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t1173594]) ).
cnf(t900054,plain,
zero = meet(X1,complement(join(X2,join(X3,meet(X1,complement(X2)))))),
inference(cp,[status(thm)],[t48631,t899096]) ).
cnf(t947408,plain,
meet(X1,complement(join(X2,join(X3,meet(X1,complement(X2)))))) = zero,
inference(orient,[status(thm)],[t900054]) ).
cnf(t22541,plain,
join(join(X1,X2),X3) = join(join(X1,X2),meet(join(X3,Y3),join(X3,X1))),
inference(cp,[status(thm)],[t22339,t22339]) ).
cnf(t1171149,plain,
join(X3,join(X1,X2)) = join(join(X1,X2),meet(join(X3,Y3),join(X3,X1))),
inference(step,[status(thm)],[t22541,t67]) ).
cnf(t1171150,plain,
join(X2,join(X3,X1)) = join(join(X1,X2),meet(join(X3,Y3),join(X3,X1))),
inference(step,[status(thm)],[t1171149,t73]) ).
cnf(t1171151,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X3,Y3),join(X3,X1))),
inference(step,[status(thm)],[t1171150,t73]) ).
cnf(t1171152,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X3,X1),join(X3,Y3))),
inference(step,[status(thm)],[t1171151,t23]) ).
cnf(t1171153,plain,
join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X1,X3),join(X3,Y3))),
inference(step,[status(thm)],[t1171152,t67]) ).
cnf(t96950,plain,
join(join(X1,X2),meet(join(X1,X3),join(X3,Y3))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t1171153]) ).
cnf(t97203,plain,
join(X1,join(X2,meet(X3,Y3))) = join(join(X1,X2),meet(join(X1,meet(X3,Y3)),X3)),
inference(cp,[status(thm)],[t96950,t10998]) ).
cnf(t1171418,plain,
join(X1,join(X2,meet(X3,Y3))) = join(join(X1,X2),meet(X3,join(X1,meet(X3,Y3)))),
inference(step,[status(thm)],[t97203,t23]) ).
cnf(t139987,plain,
join(join(X1,X2),meet(X3,join(X1,meet(X3,Y3)))) = join(X1,join(X2,meet(X3,Y3))),
inference(orient,[status(thm)],[t1171418]) ).
cnf(t3454,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t3449,t3303]) ).
cnf(t3650,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t3454]) ).
cnf(t89794,plain,
meet(X1,join(X2,meet(join(X3,X2),join(X3,Y3)))) = meet(X1,join(X2,meet(X1,join(X3,X2)))),
inference(cp,[status(thm)],[t3650,t89154]) ).
cnf(t1171109,plain,
meet(X1,join(X3,X2)) = meet(X1,join(X2,meet(X1,join(X3,X2)))),
inference(step,[status(thm)],[t89794,t89154]) ).
cnf(t90587,plain,
meet(X1,join(X2,meet(X1,join(X3,X2)))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t1171109]) ).
cnf(t90614,plain,
meet(X1,join(X2,meet(complement(X1),join(X2,X1)))) = meet(X1,join(meet(complement(X1),join(X2,X1)),meet(X2,X1))),
inference(cp,[status(thm)],[t90587,t2904]) ).
cnf(t107963,plain,
meet(X1,join(meet(X2,X1),meet(complement(X1),join(X2,X1)))) = meet(X2,X1),
inference(orient,[status(thm)],[t90614]) ).
cnf(t140369,plain,
join(X1,join(X2,meet(X3,join(meet(Y3,X3),meet(complement(X3),join(Y3,X3)))))) = join(join(X1,X2),meet(X3,join(X1,meet(Y3,X3)))),
inference(cp,[status(thm)],[t139987,t107963]) ).
cnf(t1171456,plain,
join(X1,join(X2,meet(Y3,X3))) = join(join(X1,X2),meet(X3,join(X1,meet(Y3,X3)))),
inference(step,[status(thm)],[t140369,t107963]) ).
cnf(t157571,plain,
join(join(X1,X2),meet(X3,join(X1,meet(Y3,X3)))) = join(X1,join(X2,meet(Y3,X3))),
inference(orient,[status(thm)],[t1171456]) ).
cnf(t157881,plain,
join(X1,join(X2,meet(join(X3,X1),join(X3,Y3)))) = join(join(X1,X2),meet(join(X3,Y3),join(X3,X1))),
inference(cp,[status(thm)],[t157571,t89154]) ).
cnf(t158727,plain,
join(join(X1,X2),meet(join(X3,X1),join(X3,Y3))) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t157881]) ).
cnf(t158743,plain,
join(X1,join(X2,meet(join(X3,X2),join(X3,Y3)))) = join(join(X3,X2),meet(join(X1,X2),join(X1,Y4))),
inference(cp,[status(thm)],[t158727,t89154]) ).
cnf(t1171457,plain,
join(X1,join(X3,X2)) = join(join(X3,X2),meet(join(X1,X2),join(X1,Y4))),
inference(step,[status(thm)],[t158743,t89154]) ).
cnf(t159729,plain,
join(join(X1,X2),meet(join(X3,X2),join(X3,Y3))) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t1171457]) ).
cnf(t15161,plain,
join(X1,meet(meet(X2,X3),join(X2,Y3))) = meet(join(X1,join(X2,Y3)),join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t15039,t4274]) ).
cnf(t1170443,plain,
join(X1,meet(X2,X3)) = meet(join(X1,join(X2,Y3)),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t15161,t4274]) ).
cnf(t1170444,plain,
join(X1,meet(X2,X3)) = meet(join(X1,meet(X2,X3)),join(X1,join(X2,Y3))),
inference(step,[status(thm)],[t1170443,t23]) ).
cnf(t15413,plain,
meet(join(X1,meet(X2,X3)),join(X1,join(X2,Y3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t1170444]) ).
cnf(t15446,plain,
join(X1,meet(X2,X3)) = meet(join(X1,meet(X2,X3)),join(X1,X2)),
inference(cp,[status(thm)],[t15413,t191]) ).
cnf(t1170445,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t15446,t23]) ).
cnf(t15599,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t1170445]) ).
cnf(t51323,plain,
one = join(join(X1,X2),complement(join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t51309,t15599]) ).
cnf(t52288,plain,
join(join(X1,X2),complement(join(X1,meet(X2,X3)))) = one,
inference(orient,[status(thm)],[t51323]) ).
cnf(t52346,plain,
one = join(join(X1,X2),complement(join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t52288,t67]) ).
cnf(t52741,plain,
join(join(X1,X2),complement(join(X2,meet(X1,X3)))) = one,
inference(orient,[status(thm)],[t52346]) ).
cnf(t22649,plain,
zero = meet(complement(join(X1,X2)),X1),
inference(cp,[status(thm)],[t22609,t16]) ).
cnf(t1170521,plain,
zero = meet(X1,complement(join(X1,X2))),
inference(step,[status(thm)],[t22649,t23]) ).
cnf(t22839,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(orient,[status(thm)],[t1170521]) ).
cnf(t22843,plain,
zero = meet(meet(X1,X2),complement(meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t22839,t7736]) ).
cnf(t23615,plain,
meet(meet(X1,X2),complement(meet(X2,join(X1,X3)))) = zero,
inference(orient,[status(thm)],[t22843]) ).
cnf(t23690,plain,
zero = meet(meet(meet(X1,X2),X3),complement(meet(X3,join(X1,Y3)))),
inference(cp,[status(thm)],[t23615,t8776]) ).
cnf(t1170609,plain,
zero = meet(meet(X3,meet(X1,X2)),complement(meet(X3,join(X1,Y3)))),
inference(step,[status(thm)],[t23690,t23]) ).
cnf(t1170610,plain,
zero = meet(meet(X2,meet(X3,X1)),complement(meet(X3,join(X1,Y3)))),
inference(step,[status(thm)],[t1170609,t26]) ).
cnf(t1170611,plain,
zero = meet(meet(X1,meet(X2,X3)),complement(meet(X3,join(X1,Y3)))),
inference(step,[status(thm)],[t1170610,t26]) ).
cnf(t30684,plain,
meet(meet(X1,meet(X2,X3)),complement(meet(X3,join(X1,Y3)))) = zero,
inference(orient,[status(thm)],[t1170611]) ).
cnf(t30779,plain,
zero = meet(meet(meet(X1,X2),meet(X3,Y3)),complement(meet(Y3,X1))),
inference(cp,[status(thm)],[t30684,t10998]) ).
cnf(t1170684,plain,
zero = meet(complement(meet(Y3,X1)),meet(meet(X1,X2),meet(X3,Y3))),
inference(step,[status(thm)],[t30779,t23]) ).
cnf(t1170685,plain,
zero = meet(meet(X3,Y3),meet(complement(meet(Y3,X1)),meet(X1,X2))),
inference(step,[status(thm)],[t1170684,t26]) ).
cnf(t1170686,plain,
zero = meet(meet(X1,X2),meet(meet(X3,Y3),complement(meet(Y3,X1)))),
inference(step,[status(thm)],[t1170685,t26]) ).
cnf(t1170687,plain,
zero = meet(meet(X1,X2),meet(meet(X3,Y3),complement(meet(X1,Y3)))),
inference(step,[status(thm)],[t1170686,t23]) ).
cnf(t39170,plain,
meet(meet(X1,X2),meet(meet(X3,Y3),complement(meet(X1,Y3)))) = zero,
inference(orient,[status(thm)],[t1170687]) ).
cnf(t39179,plain,
zero = meet(meet(X1,X2),meet(meet(X3,Y3),complement(meet(X2,Y3)))),
inference(cp,[status(thm)],[t39170,t2904]) ).
cnf(t44332,plain,
meet(meet(X1,X2),meet(meet(X3,Y3),complement(meet(X2,Y3)))) = zero,
inference(orient,[status(thm)],[t39179]) ).
cnf(t52961,plain,
one = join(join(meet(X1,X2),X3),complement(join(X3,zero))),
inference(cp,[status(thm)],[t52741,t44332]) ).
cnf(t1170755,plain,
one = join(complement(join(X3,zero)),join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t52961,t67]) ).
cnf(t1170756,plain,
one = join(X3,join(complement(join(X3,zero)),meet(X1,X2))),
inference(step,[status(thm)],[t1170755,t73]) ).
cnf(t1170757,plain,
one = join(X3,join(meet(X1,X2),complement(join(X3,zero)))),
inference(step,[status(thm)],[t1170756,t67]) ).
cnf(t1170758,plain,
one = join(X3,join(meet(X1,X2),complement(X3))),
inference(step,[status(thm)],[t1170757,t103]) ).
cnf(t1170759,plain,
one = join(X3,join(complement(X3),meet(X1,X2))),
inference(step,[status(thm)],[t1170758,t67]) ).
cnf(t53126,plain,
join(X1,join(complement(X1),meet(X2,X3))) = one,
inference(orient,[status(thm)],[t1170759]) ).
cnf(t53130,plain,
one = join(X1,meet(join(complement(X1),X2),join(complement(X1),X3))),
inference(cp,[status(thm)],[t53126,t7908]) ).
cnf(t1170781,plain,
one = join(X1,meet(join(X2,complement(X1)),join(complement(X1),X3))),
inference(step,[status(thm)],[t53130,t67]) ).
cnf(t1170782,plain,
one = join(X1,meet(join(X2,complement(X1)),join(X3,complement(X1)))),
inference(step,[status(thm)],[t1170781,t67]) ).
cnf(t54546,plain,
join(X1,meet(join(X2,complement(X1)),join(X3,complement(X1)))) = one,
inference(orient,[status(thm)],[t1170782]) ).
cnf(t54548,plain,
one = join(complement(X1),meet(join(X2,X1),join(X3,complement(complement(X1))))),
inference(cp,[status(thm)],[t54546,t2811]) ).
cnf(t1170783,plain,
one = join(complement(X1),meet(join(X1,X2),join(X3,complement(complement(X1))))),
inference(step,[status(thm)],[t54548,t67]) ).
cnf(t1170784,plain,
one = join(complement(X1),meet(join(X1,X2),join(X3,X1))),
inference(step,[status(thm)],[t1170783,t2811]) ).
cnf(t1170785,plain,
one = join(complement(X1),meet(join(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t1170784,t67]) ).
cnf(t54668,plain,
join(complement(X1),meet(join(X1,X2),join(X1,X3))) = one,
inference(orient,[status(thm)],[t1170785]) ).
cnf(t54684,plain,
one = join(complement(meet(X1,X2)),meet(join(meet(X1,X2),X3),X1)),
inference(cp,[status(thm)],[t54668,t10998]) ).
cnf(t1170893,plain,
one = join(complement(meet(X1,X2)),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t54684,t23]) ).
cnf(t1170894,plain,
one = join(complement(meet(X1,X2)),meet(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t1170893,t67]) ).
cnf(t61488,plain,
join(complement(meet(X1,X2)),meet(X1,join(X3,meet(X1,X2)))) = one,
inference(orient,[status(thm)],[t1170894]) ).
cnf(t10678,plain,
complement(X1) = join(complement(X1),meet(X2,join(zero,meet(complement(X1),X3)))),
inference(cp,[status(thm)],[t2571,t10521]) ).
cnf(t1170346,plain,
complement(X1) = join(complement(X1),meet(X2,meet(complement(X1),X3))),
inference(step,[status(thm)],[t10678,t2359]) ).
cnf(t1170347,plain,
complement(X1) = join(complement(X1),meet(X2,meet(X3,complement(X1)))),
inference(step,[status(thm)],[t1170346,t23]) ).
cnf(t10704,plain,
join(complement(X1),meet(X2,meet(X3,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t1170347]) ).
cnf(t15067,plain,
join(complement(X1),meet(X2,meet(X3,meet(Y3,complement(X1))))) = meet(complement(X1),join(complement(X1),meet(X2,meet(X3,meet(Y3,complement(X1)))))),
inference(cp,[status(thm)],[t15039,t10704]) ).
cnf(t1170442,plain,
join(complement(X1),meet(X2,meet(X3,meet(Y3,complement(X1))))) = complement(X1),
inference(step,[status(thm)],[t15067,t14]) ).
cnf(t15325,plain,
join(complement(X1),meet(X2,meet(X3,meet(Y3,complement(X1))))) = complement(X1),
inference(orient,[status(thm)],[t1170442]) ).
cnf(t61601,plain,
one = join(complement(meet(X1,meet(X2,meet(X3,complement(Y3))))),meet(X1,complement(Y3))),
inference(cp,[status(thm)],[t61488,t15325]) ).
cnf(t1172706,plain,
one = join(meet(X1,complement(Y3)),complement(meet(X1,meet(X2,meet(X3,complement(Y3)))))),
inference(step,[status(thm)],[t61601,t67]) ).
cnf(t522432,plain,
join(meet(X1,complement(X2)),complement(meet(X1,meet(X3,meet(Y3,complement(X2)))))) = one,
inference(orient,[status(thm)],[t1172706]) ).
cnf(t522557,plain,
join(meet(X1,complement(X2)),join(X3,Y3)) = join(join(X3,Y3),meet(join(meet(X1,complement(X2)),Y3),one)),
inference(cp,[status(thm)],[t159729,t522432]) ).
cnf(t1172707,plain,
join(meet(X1,complement(X2)),join(X3,Y3)) = join(join(X3,Y3),join(meet(X1,complement(X2)),Y3)),
inference(step,[status(thm)],[t522557,t110]) ).
cnf(t1172708,plain,
join(Y3,join(meet(X1,complement(X2)),X3)) = join(join(X3,Y3),join(meet(X1,complement(X2)),Y3)),
inference(step,[status(thm)],[t1172707,t73]) ).
cnf(t1172709,plain,
join(X3,join(Y3,meet(X1,complement(X2)))) = join(join(X3,Y3),join(meet(X1,complement(X2)),Y3)),
inference(step,[status(thm)],[t1172708,t73]) ).
cnf(t1172710,plain,
join(X3,join(Y3,meet(X1,complement(X2)))) = join(Y3,join(join(X3,Y3),meet(X1,complement(X2)))),
inference(step,[status(thm)],[t1172709,t73]) ).
cnf(t522887,plain,
join(X1,join(join(X2,X1),meet(X3,complement(Y3)))) = join(X2,join(X1,meet(X3,complement(Y3)))),
inference(orient,[status(thm)],[t1172710]) ).
cnf(t947411,plain,
zero = meet(X1,complement(join(X2,join(X3,meet(X1,complement(X3)))))),
inference(cp,[status(thm)],[t947408,t522887]) ).
cnf(t975695,plain,
meet(X1,complement(join(X2,join(X3,meet(X1,complement(X3)))))) = zero,
inference(orient,[status(thm)],[t947411]) ).
cnf(t975698,plain,
zero = complement(join(X1,join(X2,meet(complement(X1),complement(X2))))),
inference(cp,[status(thm)],[t975695,t899096]) ).
cnf(t976308,plain,
complement(join(X1,join(X2,meet(complement(X1),complement(X2))))) = zero,
inference(orient,[status(thm)],[t975698]) ).
cnf(t976342,plain,
one = ifeq(zero,zero,join(X1,join(X2,meet(complement(X1),complement(X2)))),one),
inference(cp,[status(thm)],[t2841,t976308]) ).
cnf(t1173724,plain,
one = join(X1,join(X2,meet(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t976342,t17]) ).
cnf(t976648,plain,
join(X1,join(X2,meet(complement(X1),complement(X2)))) = one,
inference(orient,[status(thm)],[t1173724]) ).
cnf(t9127,plain,
meet(join(meet(X1,X2),meet(X1,X3)),meet(Y3,X2)) = meet(Y3,meet(X1,X2)),
inference(cp,[status(thm)],[t26,t8913]) ).
cnf(t1170399,plain,
meet(X2,meet(join(meet(X1,X2),meet(X1,X3)),Y3)) = meet(Y3,meet(X1,X2)),
inference(step,[status(thm)],[t9127,t26]) ).
cnf(t1170400,plain,
meet(X2,meet(Y3,join(meet(X1,X2),meet(X1,X3)))) = meet(Y3,meet(X1,X2)),
inference(step,[status(thm)],[t1170399,t23]) ).
cnf(t1170401,plain,
meet(X2,meet(Y3,join(meet(X1,X2),meet(X1,X3)))) = meet(X2,meet(Y3,X1)),
inference(step,[status(thm)],[t1170400,t26]) ).
cnf(t1170402,plain,
meet(X2,meet(Y3,join(meet(X1,X2),meet(X1,X3)))) = meet(X1,meet(X2,Y3)),
inference(step,[status(thm)],[t1170401,t26]) ).
cnf(t12688,plain,
meet(X1,meet(X2,join(meet(X3,X1),meet(X3,Y3)))) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t1170402]) ).
cnf(t22781,plain,
meet(X1,meet(X2,complement(join(meet(X1,X2),X3)))) = meet(X2,zero),
inference(cp,[status(thm)],[t12688,t22609]) ).
cnf(t1170528,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))) = meet(X2,zero),
inference(step,[status(thm)],[t22781,t67]) ).
cnf(t1170529,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))) = zero,
inference(step,[status(thm)],[t1170528,t126]) ).
cnf(t23117,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t1170529]) ).
cnf(t899934,plain,
zero = meet(X1,complement(join(X2,meet(X1,complement(X2))))),
inference(cp,[status(thm)],[t23117,t899096]) ).
cnf(t909145,plain,
meet(X1,complement(join(X2,meet(X1,complement(X2))))) = zero,
inference(orient,[status(thm)],[t899934]) ).
cnf(t909149,plain,
zero = meet(X1,complement(join(complement(X2),meet(X1,X2)))),
inference(cp,[status(thm)],[t909145,t2811]) ).
cnf(t911235,plain,
meet(X1,complement(join(complement(X2),meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t909149]) ).
cnf(t976657,plain,
one = join(X1,join(join(complement(X2),meet(complement(X1),X2)),zero)),
inference(cp,[status(thm)],[t976648,t911235]) ).
cnf(t1173725,plain,
one = join(X1,join(complement(X2),meet(complement(X1),X2))),
inference(step,[status(thm)],[t976657,t103]) ).
cnf(t1173726,plain,
one = join(X1,join(complement(X2),meet(X2,complement(X1)))),
inference(step,[status(thm)],[t1173725,t23]) ).
cnf(t977173,plain,
join(X1,join(complement(X2),meet(X2,complement(X1)))) = one,
inference(orient,[status(thm)],[t1173726]) ).
cnf(t977558,plain,
join(X1,complement(X2)) = ifeq(meet(meet(X2,complement(X1)),join(X1,complement(X2))),zero,ifeq(one,one,complement(meet(X2,complement(X1))),join(X1,complement(X2))),join(X1,complement(X2))),
inference(cp,[status(thm)],[t49091,t977173]) ).
cnf(t3683,plain,
meet(X1,meet(join(X2,meet(X1,join(X2,X3))),Y3)) = meet(Y3,meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t26,t3650]) ).
cnf(t1171379,plain,
meet(X1,meet(Y3,join(X2,meet(X1,join(X2,X3))))) = meet(Y3,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t3683,t23]) ).
cnf(t1171380,plain,
meet(X1,meet(Y3,join(X2,meet(X1,join(X2,X3))))) = meet(X1,meet(join(X2,X3),Y3)),
inference(step,[status(thm)],[t1171379,t26]) ).
cnf(t1171381,plain,
meet(X1,meet(Y3,join(X2,meet(X1,join(X2,X3))))) = meet(X1,meet(Y3,join(X2,X3))),
inference(step,[status(thm)],[t1171380,t23]) ).
cnf(t129298,plain,
meet(X1,meet(X2,join(X3,meet(X1,join(X3,Y3))))) = meet(X1,meet(X2,join(X3,Y3))),
inference(orient,[status(thm)],[t1171381]) ).
cnf(t18495,plain,
meet(meet(X1,join(X2,meet(complement(X1),join(X2,X1)))),join(X3,Y3)) = meet(X1,meet(meet(X2,X1),join(X3,Y3))),
inference(cp,[status(thm)],[t18475,t2904]) ).
cnf(t1170478,plain,
meet(meet(X2,X1),join(X3,Y3)) = meet(X1,meet(meet(X2,X1),join(X3,Y3))),
inference(step,[status(thm)],[t18495,t2904]) ).
cnf(t18799,plain,
meet(X1,meet(meet(X2,X1),join(X3,Y3))) = meet(meet(X2,X1),join(X3,Y3)),
inference(orient,[status(thm)],[t1170478]) ).
cnf(t129301,plain,
meet(X1,meet(meet(X2,X1),join(X3,Y3))) = meet(meet(X2,X1),join(X3,meet(X1,join(X3,Y3)))),
inference(cp,[status(thm)],[t129298,t18799]) ).
cnf(t1171427,plain,
meet(meet(X2,X1),join(X3,Y3)) = meet(meet(X2,X1),join(X3,meet(X1,join(X3,Y3)))),
inference(step,[status(thm)],[t129301,t18799]) ).
cnf(t144722,plain,
meet(meet(X1,X2),join(X3,meet(X2,join(X3,Y3)))) = meet(meet(X1,X2),join(X3,Y3)),
inference(orient,[status(thm)],[t1171427]) ).
cnf(t144829,plain,
meet(meet(X1,X2),join(X3,meet(complement(X2),join(X2,X3)))) = meet(meet(X1,X2),join(X3,meet(X2,X3))),
inference(cp,[status(thm)],[t144722,t2274]) ).
cnf(t1171493,plain,
meet(meet(X1,X2),join(X3,meet(complement(X2),join(X2,X3)))) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t144829,t3095]) ).
cnf(t1171494,plain,
meet(meet(X1,X2),join(X3,meet(complement(X2),join(X2,X3)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t1171493,t23]) ).
cnf(t1171495,plain,
meet(meet(X1,X2),join(X3,meet(complement(X2),join(X2,X3)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t1171494,t26]) ).
cnf(t1171496,plain,
meet(meet(X1,X2),join(X3,meet(complement(X2),join(X2,X3)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t1171495,t26]) ).
cnf(t175455,plain,
meet(meet(X1,X2),join(X3,meet(complement(X2),join(X2,X3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t1171496]) ).
cnf(t176450,plain,
meet(meet(X1,X2),join(X3,meet(complement(X2),join(X2,X3)))) = meet(meet(X1,X2),join(X3,meet(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t3650,t175455]) ).
cnf(t1171505,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(X3,meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t176450,t175455]) ).
cnf(t178449,plain,
meet(meet(X1,X2),join(X3,meet(X1,meet(X2,X3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t1171505]) ).
cnf(t2817,plain,
zero = ifeq(complement(X1),one,X1,zero),
inference(cp,[status(thm)],[t150,t2811]) ).
cnf(t2842,plain,
ifeq(complement(X1),one,X1,zero) = zero,
inference(orient,[status(thm)],[t2817]) ).
cnf(t60,plain,
meet(X1,meet(join(meet(X2,join(X1,X3)),meet(X3,join(X1,X2))),Y3)) = meet(Y3,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t26,t46]) ).
cnf(t1170655,plain,
meet(X1,meet(Y3,join(meet(X2,join(X1,X3)),meet(X3,join(X1,X2))))) = meet(Y3,join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t60,t23]) ).
cnf(t34727,plain,
meet(X1,meet(X2,join(meet(X3,join(X1,Y3)),meet(Y3,join(X1,X3))))) = meet(X2,join(meet(X1,X3),meet(X1,Y3))),
inference(orient,[status(thm)],[t1170655]) ).
cnf(t51311,plain,
one = join(X1,complement(meet(X2,join(meet(X1,X3),meet(X1,Y3))))),
inference(cp,[status(thm)],[t51309,t34727]) ).
cnf(t55461,plain,
join(X1,complement(meet(X2,join(meet(X1,X3),meet(X1,Y3))))) = one,
inference(orient,[status(thm)],[t51311]) ).
cnf(t55656,plain,
one = join(join(X1,X2),complement(meet(X3,join(join(X1,X2),meet(join(X1,X2),Y3))))),
inference(cp,[status(thm)],[t55461,t4034]) ).
cnf(t1170798,plain,
one = join(join(X1,X2),complement(meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t55656,t16]) ).
cnf(t55988,plain,
join(join(X1,X2),complement(meet(X3,join(X1,X2)))) = one,
inference(orient,[status(thm)],[t1170798]) ).
cnf(t5109,plain,
meet(X1,meet(X2,join(X3,meet(complement(X1),join(X1,X3))))) = meet(meet(X1,meet(X3,X2)),join(Y3,meet(X1,X2))),
inference(cp,[status(thm)],[t5107,t2628]) ).
cnf(t1170249,plain,
meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(Y3,meet(X1,X2))),
inference(step,[status(thm)],[t5109,t2628]) ).
cnf(t5653,plain,
meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t1170249]) ).
cnf(t5676,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(Y3,meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t5653,t14]) ).
cnf(t1170250,plain,
meet(X1,X2) = meet(meet(X1,X2),join(Y3,meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t5676,t14]) ).
cnf(t5801,plain,
meet(meet(X1,X2),join(X3,meet(X1,join(X2,Y3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t1170250]) ).
cnf(t56036,plain,
one = join(join(X1,meet(X2,join(X3,Y3))),complement(meet(X2,X3))),
inference(cp,[status(thm)],[t55988,t5801]) ).
cnf(t1170924,plain,
one = join(complement(meet(X2,X3)),join(X1,meet(X2,join(X3,Y3)))),
inference(step,[status(thm)],[t56036,t67]) ).
cnf(t1170925,plain,
one = join(X1,join(meet(X2,join(X3,Y3)),complement(meet(X2,X3)))),
inference(step,[status(thm)],[t1170924,t73]) ).
cnf(t1170926,plain,
one = join(X1,join(complement(meet(X2,X3)),meet(X2,join(X3,Y3)))),
inference(step,[status(thm)],[t1170925,t67]) ).
cnf(t63890,plain,
join(X1,join(complement(meet(X2,X3)),meet(X2,join(X3,Y3)))) = one,
inference(orient,[status(thm)],[t1170926]) ).
cnf(t63896,plain,
one = join(complement(meet(X1,X2)),meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t63890,t131]) ).
cnf(t64260,plain,
join(complement(meet(X1,X2)),meet(X1,join(X2,X3))) = one,
inference(orient,[status(thm)],[t63896]) ).
cnf(t64337,plain,
one = join(complement(meet(X1,X2)),meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t64260,t23]) ).
cnf(t64983,plain,
join(complement(meet(X1,X2)),meet(X2,join(X1,X3))) = one,
inference(orient,[status(thm)],[t64337]) ).
cnf(t65068,plain,
one = join(complement(meet(meet(X1,X2),X3)),meet(X3,join(X1,Y3))),
inference(cp,[status(thm)],[t64983,t8776]) ).
cnf(t1171005,plain,
one = join(meet(X3,join(X1,Y3)),complement(meet(meet(X1,X2),X3))),
inference(step,[status(thm)],[t65068,t67]) ).
cnf(t1171006,plain,
one = join(meet(X3,join(X1,Y3)),complement(meet(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t1171005,t23]) ).
cnf(t1171007,plain,
one = join(meet(X3,join(X1,Y3)),complement(meet(X2,meet(X3,X1)))),
inference(step,[status(thm)],[t1171006,t26]) ).
cnf(t1171008,plain,
one = join(meet(X3,join(X1,Y3)),complement(meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t1171007,t26]) ).
cnf(t74532,plain,
join(meet(X1,join(X2,X3)),complement(meet(X2,meet(Y3,X1)))) = one,
inference(orient,[status(thm)],[t1171008]) ).
cnf(t74787,plain,
one = join(meet(join(X1,X2),join(X3,Y3)),complement(meet(X3,X1))),
inference(cp,[status(thm)],[t74532,t14]) ).
cnf(t1171051,plain,
one = join(complement(meet(X3,X1)),meet(join(X1,X2),join(X3,Y3))),
inference(step,[status(thm)],[t74787,t67]) ).
cnf(t1171052,plain,
one = join(complement(meet(X1,X3)),meet(join(X1,X2),join(X3,Y3))),
inference(step,[status(thm)],[t1171051,t23]) ).
cnf(t80952,plain,
join(complement(meet(X1,X2)),meet(join(X1,X3),join(X2,Y3))) = one,
inference(orient,[status(thm)],[t1171052]) ).
cnf(t81411,plain,
one = join(complement(meet(join(X1,X2),join(X3,Y3))),meet(join(X1,X2),one)),
inference(cp,[status(thm)],[t61488,t80952]) ).
cnf(t1171081,plain,
one = join(complement(meet(join(X1,X2),join(X3,Y3))),join(X1,X2)),
inference(step,[status(thm)],[t81411,t110]) ).
cnf(t1171082,plain,
one = join(X2,join(complement(meet(join(X1,X2),join(X3,Y3))),X1)),
inference(step,[status(thm)],[t1171081,t73]) ).
cnf(t1171083,plain,
one = join(X1,join(X2,complement(meet(join(X1,X2),join(X3,Y3))))),
inference(step,[status(thm)],[t1171082,t73]) ).
cnf(t85221,plain,
join(X1,join(X2,complement(meet(join(X1,X2),join(X3,Y3))))) = one,
inference(orient,[status(thm)],[t1171083]) ).
cnf(t85404,plain,
one = join(X1,join(X2,complement(meet(join(X1,X2),meet(X3,Y3))))),
inference(cp,[status(thm)],[t85221,t3160]) ).
cnf(t1171096,plain,
one = join(X1,join(X2,complement(meet(Y3,meet(join(X1,X2),X3))))),
inference(step,[status(thm)],[t85404,t26]) ).
cnf(t1171097,plain,
one = join(X1,join(X2,complement(meet(X3,meet(Y3,join(X1,X2)))))),
inference(step,[status(thm)],[t1171096,t26]) ).
cnf(t87505,plain,
join(X1,join(X2,complement(meet(X3,meet(Y3,join(X1,X2)))))) = one,
inference(orient,[status(thm)],[t1171097]) ).
cnf(t889677,plain,
one = join(X1,complement(meet(X2,meet(X3,join(X1,complement(X2)))))),
inference(cp,[status(thm)],[t87505,t888679]) ).
cnf(t939305,plain,
join(X1,complement(meet(X2,meet(X3,join(X1,complement(X2)))))) = one,
inference(orient,[status(thm)],[t889677]) ).
cnf(t939309,plain,
one = join(X1,complement(meet(X2,meet(join(X1,complement(X3)),X3)))),
inference(cp,[status(thm)],[t939305,t26]) ).
cnf(t1173704,plain,
one = join(X1,complement(meet(X2,meet(X3,join(X1,complement(X3)))))),
inference(step,[status(thm)],[t939309,t23]) ).
cnf(t966343,plain,
join(X1,complement(meet(X2,meet(X3,join(X1,complement(X3)))))) = one,
inference(orient,[status(thm)],[t1173704]) ).
cnf(t966344,plain,
one = complement(meet(X1,meet(X2,join(complement(X1),complement(X2))))),
inference(cp,[status(thm)],[t966343,t888679]) ).
cnf(t966965,plain,
complement(meet(X1,meet(X2,join(complement(X1),complement(X2))))) = one,
inference(orient,[status(thm)],[t966344]) ).
cnf(t967001,plain,
zero = ifeq(one,one,meet(X1,meet(X2,join(complement(X1),complement(X2)))),zero),
inference(cp,[status(thm)],[t2842,t966965]) ).
cnf(t1173705,plain,
zero = meet(X1,meet(X2,join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t967001,t17]) ).
cnf(t967349,plain,
meet(X1,meet(X2,join(complement(X1),complement(X2)))) = zero,
inference(orient,[status(thm)],[t1173705]) ).
cnf(t6772,plain,
join(X1,meet(X2,join(X2,X3))) = join(X1,meet(join(X2,X3),join(X1,X2))),
inference(cp,[status(thm)],[t6746,t14]) ).
cnf(t1170266,plain,
join(X1,X2) = join(X1,meet(join(X2,X3),join(X1,X2))),
inference(step,[status(thm)],[t6772,t14]) ).
cnf(t1170267,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t1170266,t23]) ).
cnf(t6836,plain,
join(X1,meet(join(X1,X2),join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t1170267]) ).
cnf(t6915,plain,
join(X1,join(meet(join(X1,X2),join(X2,X3)),Y3)) = join(Y3,join(X1,X2)),
inference(cp,[status(thm)],[t73,t6836]) ).
cnf(t1170293,plain,
join(X1,join(Y3,meet(join(X1,X2),join(X2,X3)))) = join(Y3,join(X1,X2)),
inference(step,[status(thm)],[t6915,t67]) ).
cnf(t1170294,plain,
join(X1,join(Y3,meet(join(X1,X2),join(X2,X3)))) = join(X2,join(Y3,X1)),
inference(step,[status(thm)],[t1170293,t73]) ).
cnf(t1170295,plain,
join(X1,join(Y3,meet(join(X1,X2),join(X2,X3)))) = join(X1,join(X2,Y3)),
inference(step,[status(thm)],[t1170294,t73]) ).
cnf(t8627,plain,
join(X1,join(X2,meet(join(X1,X3),join(X3,Y3)))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t1170295]) ).
cnf(t61725,plain,
join(X1,join(X2,complement(meet(join(X1,X2),X3)))) = join(X1,one),
inference(cp,[status(thm)],[t8627,t61488]) ).
cnf(t1170895,plain,
join(X1,join(X2,complement(meet(X3,join(X1,X2))))) = join(X1,one),
inference(step,[status(thm)],[t61725,t23]) ).
cnf(t1170896,plain,
join(X1,join(X2,complement(meet(X3,join(X1,X2))))) = one,
inference(step,[status(thm)],[t1170895,t143]) ).
cnf(t61796,plain,
join(X1,join(X2,complement(meet(X3,join(X1,X2))))) = one,
inference(orient,[status(thm)],[t1170896]) ).
cnf(t889531,plain,
one = join(X1,complement(meet(X2,join(X1,complement(X2))))),
inference(cp,[status(thm)],[t61796,t888679]) ).
cnf(t903098,plain,
join(X1,complement(meet(X2,join(X1,complement(X2))))) = one,
inference(orient,[status(thm)],[t889531]) ).
cnf(t903103,plain,
one = join(X1,complement(meet(complement(X2),join(X1,X2)))),
inference(cp,[status(thm)],[t903098,t2811]) ).
cnf(t910653,plain,
join(X1,complement(meet(complement(X2),join(X1,X2)))) = one,
inference(orient,[status(thm)],[t903103]) ).
cnf(t967360,plain,
zero = meet(X1,meet(meet(complement(X2),join(complement(X1),X2)),one)),
inference(cp,[status(thm)],[t967349,t910653]) ).
cnf(t1173706,plain,
zero = meet(X1,meet(complement(X2),join(complement(X1),X2))),
inference(step,[status(thm)],[t967360,t110]) ).
cnf(t1173707,plain,
zero = meet(X1,meet(complement(X2),join(X2,complement(X1)))),
inference(step,[status(thm)],[t1173706,t67]) ).
cnf(t967865,plain,
meet(X1,meet(complement(X2),join(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t1173707]) ).
cnf(t968206,plain,
meet(X1,meet(complement(X2),join(X2,complement(X1)))) = meet(meet(X1,complement(X2)),join(join(X2,complement(X1)),zero)),
inference(cp,[status(thm)],[t178449,t967865]) ).
cnf(t1173715,plain,
zero = meet(meet(X1,complement(X2)),join(join(X2,complement(X1)),zero)),
inference(step,[status(thm)],[t968206,t967865]) ).
cnf(t1173716,plain,
zero = meet(meet(X1,complement(X2)),join(X2,complement(X1))),
inference(step,[status(thm)],[t1173715,t103]) ).
cnf(t970368,plain,
meet(meet(X1,complement(X2)),join(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t1173716]) ).
cnf(t1173727,plain,
join(X1,complement(X2)) = ifeq(zero,zero,ifeq(one,one,complement(meet(X2,complement(X1))),join(X1,complement(X2))),join(X1,complement(X2))),
inference(step,[status(thm)],[t977558,t970368]) ).
cnf(t1173728,plain,
join(X1,complement(X2)) = ifeq(one,one,complement(meet(X2,complement(X1))),join(X1,complement(X2))),
inference(step,[status(thm)],[t1173727,t17]) ).
cnf(t1173729,plain,
join(X1,complement(X2)) = complement(meet(X2,complement(X1))),
inference(step,[status(thm)],[t1173728,t17]) ).
cnf(t977820,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t1173729]) ).
cnf(t977976,plain,
meet(X1,complement(X2)) = complement(join(X2,complement(X1))),
inference(cp,[status(thm)],[t2811,t977820]) ).
cnf(t980118,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t977976]) ).
cnf(t980250,plain,
meet(join(X1,complement(X2)),complement(X3)) = complement(join(X3,meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t980118,t980118]) ).
cnf(t1173886,plain,
meet(complement(X3),join(X1,complement(X2))) = complement(join(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t980250,t23]) ).
cnf(t985575,plain,
complement(join(X1,meet(X2,complement(X3)))) = meet(complement(X1),join(X3,complement(X2))),
inference(orient,[status(thm)],[t1173886]) ).
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(t1170232,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(t4823,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)],[t1170232]) ).
cnf(t4829,plain,
meet(X1,X2) = ifeq(zero,zero,ifeq(join(complement(X1),meet(X1,X2)),one,complement(complement(X1)),meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t4823,t162]) ).
cnf(t1170408,plain,
meet(X1,X2) = ifeq(join(complement(X1),meet(X1,X2)),one,complement(complement(X1)),meet(X1,X2)),
inference(step,[status(thm)],[t4829,t17]) ).
cnf(t1170409,plain,
meet(X1,X2) = ifeq(join(complement(X1),meet(X1,X2)),one,X1,meet(X1,X2)),
inference(step,[status(thm)],[t1170408,t2811]) ).
cnf(t13428,plain,
ifeq(join(complement(X1),meet(X1,X2)),one,X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t1170409]) ).
cnf(t61603,plain,
one = join(complement(meet(join(X1,X2),join(X1,X3))),meet(join(X1,X2),one)),
inference(cp,[status(thm)],[t61488,t54668]) ).
cnf(t1170977,plain,
one = join(complement(meet(join(X1,X2),join(X1,X3))),join(X1,X2)),
inference(step,[status(thm)],[t61603,t110]) ).
cnf(t1170978,plain,
one = join(X2,join(complement(meet(join(X1,X2),join(X1,X3))),X1)),
inference(step,[status(thm)],[t1170977,t73]) ).
cnf(t1170979,plain,
one = join(X1,join(X2,complement(meet(join(X1,X2),join(X1,X3))))),
inference(step,[status(thm)],[t1170978,t73]) ).
cnf(t72454,plain,
join(X1,join(X2,complement(meet(join(X1,X2),join(X1,X3))))) = one,
inference(orient,[status(thm)],[t1170979]) ).
cnf(t72456,plain,
one = join(X1,join(X2,complement(join(X1,meet(X3,join(X1,X2)))))),
inference(cp,[status(thm)],[t72454,t3303]) ).
cnf(t79929,plain,
join(X1,join(X2,complement(join(X1,meet(X3,join(X1,X2)))))) = one,
inference(orient,[status(thm)],[t72456]) ).
cnf(t52356,plain,
one = join(join(X1,join(X2,X3)),complement(join(X1,X2))),
inference(cp,[status(thm)],[t52288,t22339]) ).
cnf(t1170763,plain,
one = join(complement(join(X1,X2)),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t52356,t67]) ).
cnf(t1170764,plain,
one = join(join(X2,X3),join(complement(join(X1,X2)),X1)),
inference(step,[status(thm)],[t1170763,t73]) ).
cnf(t1170765,plain,
one = join(X1,join(join(X2,X3),complement(join(X1,X2)))),
inference(step,[status(thm)],[t1170764,t73]) ).
cnf(t53414,plain,
join(X1,join(join(X2,X3),complement(join(X1,X2)))) = one,
inference(orient,[status(thm)],[t1170765]) ).
cnf(t53418,plain,
one = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t53414,t15]) ).
cnf(t53594,plain,
join(X1,join(X2,complement(join(X1,X2)))) = one,
inference(orient,[status(thm)],[t53418]) ).
cnf(t53670,plain,
meet(X1,join(X2,complement(join(X1,X2)))) = meet(X1,join(join(X2,complement(join(X1,X2))),meet(complement(X1),one))),
inference(cp,[status(thm)],[t2274,t53594]) ).
cnf(t1172458,plain,
meet(X1,join(X2,complement(join(X1,X2)))) = meet(X1,join(meet(complement(X1),one),join(X2,complement(join(X1,X2))))),
inference(step,[status(thm)],[t53670,t67]) ).
cnf(t1172459,plain,
meet(X1,join(X2,complement(join(X1,X2)))) = meet(X1,join(X2,join(complement(join(X1,X2)),meet(complement(X1),one)))),
inference(step,[status(thm)],[t1172458,t73]) ).
cnf(t1172460,plain,
meet(X1,join(X2,complement(join(X1,X2)))) = meet(X1,join(X2,join(meet(complement(X1),one),complement(join(X1,X2))))),
inference(step,[status(thm)],[t1172459,t67]) ).
cnf(t1172461,plain,
meet(X1,join(X2,complement(join(X1,X2)))) = meet(X1,join(X2,join(complement(X1),complement(join(X1,X2))))),
inference(step,[status(thm)],[t1172460,t110]) ).
cnf(t470957,plain,
meet(X1,join(X2,join(complement(X1),complement(join(X1,X2))))) = meet(X1,join(X2,complement(join(X1,X2)))),
inference(orient,[status(thm)],[t1172461]) ).
cnf(t1173587,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(X2,complement(join(X1,X2)))),
inference(step,[status(thm)],[t470957,t892868]) ).
cnf(t893831,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(X2,complement(join(X1,X2)))),
inference(rw,[status(thm)],[t1173587]) ).
cnf(t924167,plain,
meet(X1,join(X2,complement(join(X1,X2)))) = meet(X1,join(X2,complement(X1))),
inference(orient,[status(thm)],[t893831]) ).
cnf(t977973,plain,
join(complement(X1),complement(X2)) = complement(meet(X2,X1)),
inference(cp,[status(thm)],[t977820,t2811]) ).
cnf(t1173761,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t977973,t23]) ).
cnf(t978758,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t1173761]) ).
cnf(t978923,plain,
meet(X1,join(complement(X2),complement(X1))) = meet(X1,complement(meet(X2,join(X1,complement(X2))))),
inference(cp,[status(thm)],[t924167,t978758]) ).
cnf(t1174067,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,complement(meet(X2,join(X1,complement(X2))))),
inference(step,[status(thm)],[t978923,t978758]) ).
cnf(t1174068,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(meet(X2,join(X1,complement(X2))))),
inference(step,[status(thm)],[t1174067,t23]) ).
cnf(t977983,plain,
join(meet(X1,complement(X2)),complement(X3)) = complement(meet(X3,join(X2,complement(X1)))),
inference(cp,[status(thm)],[t977820,t977820]) ).
cnf(t1173845,plain,
join(complement(X3),meet(X1,complement(X2))) = complement(meet(X3,join(X2,complement(X1)))),
inference(step,[status(thm)],[t977983,t67]) ).
cnf(t983147,plain,
complement(meet(X1,join(X2,complement(X3)))) = join(complement(X1),meet(X3,complement(X2))),
inference(orient,[status(thm)],[t1173845]) ).
cnf(t1174069,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,join(complement(X2),meet(X2,complement(X1)))),
inference(step,[status(thm)],[t1174068,t983147]) ).
cnf(t1044864,plain,
meet(X1,join(complement(X2),meet(X2,complement(X1)))) = meet(X1,complement(meet(X1,X2))),
inference(orient,[status(thm)],[t1174069]) ).
cnf(t1045860,plain,
one = join(complement(X1),join(meet(X1,complement(X2)),complement(join(complement(X1),meet(X2,complement(meet(X2,X1))))))),
inference(cp,[status(thm)],[t79929,t1044864]) ).
cnf(t1174073,plain,
one = join(complement(X1),join(meet(X1,complement(X2)),meet(complement(complement(X1)),join(meet(X2,X1),complement(X2))))),
inference(step,[status(thm)],[t1045860,t985575]) ).
cnf(t1174074,plain,
one = join(complement(X1),join(meet(X1,complement(X2)),meet(X1,join(meet(X2,X1),complement(X2))))),
inference(step,[status(thm)],[t1174073,t2811]) ).
cnf(t89624,plain,
meet(X1,join(X2,meet(join(X3,X2),join(X3,Y3)))) = join(meet(X2,X1),meet(X1,join(X3,X2))),
inference(cp,[status(thm)],[t7736,t89154]) ).
cnf(t89901,plain,
join(meet(X1,X2),meet(X1,join(X3,X2))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t89624]) ).
cnf(t1174075,plain,
one = join(complement(X1),meet(X1,join(meet(X2,X1),complement(X2)))),
inference(step,[status(thm)],[t1174074,t89901]) ).
cnf(t1174076,plain,
one = join(complement(X1),meet(X1,join(complement(X2),meet(X2,X1)))),
inference(step,[status(thm)],[t1174075,t67]) ).
cnf(t1174077,plain,
one = join(complement(X1),meet(X1,join(complement(X2),meet(X1,X2)))),
inference(step,[status(thm)],[t1174076,t23]) ).
cnf(t1047019,plain,
join(complement(X1),meet(X1,join(complement(X2),meet(X1,X2)))) = one,
inference(orient,[status(thm)],[t1174077]) ).
cnf(t1047784,plain,
meet(X1,join(complement(X2),meet(X1,X2))) = ifeq(one,one,X1,meet(X1,join(complement(X2),meet(X1,X2)))),
inference(cp,[status(thm)],[t13428,t1047019]) ).
cnf(t1174078,plain,
meet(X1,join(complement(X2),meet(X1,X2))) = X1,
inference(step,[status(thm)],[t1047784,t17]) ).
cnf(t1048352,plain,
meet(X1,join(complement(X2),meet(X1,X2))) = X1,
inference(orient,[status(thm)],[t1174078]) ).
cnf(t1049562,plain,
join(complement(X1),meet(X2,X1)) = join(complement(X1),X2),
inference(cp,[status(thm)],[t6642,t1048352]) ).
cnf(t1174080,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(step,[status(thm)],[t1049562,t23]) ).
cnf(t1174081,plain,
join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
inference(step,[status(thm)],[t1174080,t67]) ).
cnf(t1050091,plain,
join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t1174081]) ).
cnf(t1050912,plain,
meet(complement(complement(X1)),join(X2,complement(X1))) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t985575,t1050091]) ).
cnf(t1174097,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X2),complement(X1))),
inference(step,[status(thm)],[t1050912,t2811]) ).
cnf(t1174098,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,complement(complement(X2))),
inference(step,[status(thm)],[t1174097,t980118]) ).
cnf(t1174099,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t1174098,t2811]) ).
cnf(t1053064,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t1174099]) ).
cnf(t1053177,plain,
meet(X1,complement(X2)) = meet(X1,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t1053064,t978758]) ).
cnf(t1174116,plain,
meet(X1,complement(X2)) = meet(X1,complement(meet(X1,X2))),
inference(step,[status(thm)],[t1053177,t23]) ).
cnf(t1056721,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t1174116]) ).
cnf(t978786,plain,
complement(meet(meet(X1,complement(X2)),X3)) = join(join(X2,complement(X1)),complement(X3)),
inference(cp,[status(thm)],[t978758,t977820]) ).
cnf(t1173861,plain,
complement(meet(X3,meet(X1,complement(X2)))) = join(join(X2,complement(X1)),complement(X3)),
inference(step,[status(thm)],[t978786,t23]) ).
cnf(t1173862,plain,
complement(meet(X1,meet(complement(X2),X3))) = join(join(X2,complement(X1)),complement(X3)),
inference(step,[status(thm)],[t1173861,t26]) ).
cnf(t1173863,plain,
complement(meet(X1,meet(X3,complement(X2)))) = join(join(X2,complement(X1)),complement(X3)),
inference(step,[status(thm)],[t1173862,t23]) ).
cnf(t1173864,plain,
complement(meet(X1,meet(X3,complement(X2)))) = join(complement(X3),join(X2,complement(X1))),
inference(step,[status(thm)],[t1173863,t67]) ).
cnf(t1173865,plain,
complement(meet(X1,meet(X3,complement(X2)))) = join(complement(X1),join(complement(X3),X2)),
inference(step,[status(thm)],[t1173864,t73]) ).
cnf(t1173866,plain,
complement(meet(X1,meet(X3,complement(X2)))) = join(X2,join(complement(X1),complement(X3))),
inference(step,[status(thm)],[t1173865,t73]) ).
cnf(t1173867,plain,
complement(meet(X1,meet(X3,complement(X2)))) = join(X2,complement(meet(X1,X3))),
inference(step,[status(thm)],[t1173866,t978758]) ).
cnf(t983951,plain,
complement(meet(X1,meet(X2,complement(X3)))) = join(X3,complement(meet(X1,X2))),
inference(orient,[status(thm)],[t1173867]) ).
cnf(t1056724,plain,
meet(X1,complement(meet(X2,complement(X3)))) = meet(X1,join(X3,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t1056721,t983951]) ).
cnf(t1174347,plain,
meet(X1,join(X3,complement(X2))) = meet(X1,join(X3,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t1056724,t977820]) ).
cnf(t1163822,plain,
meet(X1,join(X2,complement(meet(X1,X3)))) = meet(X1,join(X2,complement(X3))),
inference(orient,[status(thm)],[t1174347]) ).
cnf(t1163880,plain,
meet(X1,join(X2,complement(complement(meet(X1,X3))))) = meet(X1,join(X2,complement(meet(X1,complement(X3))))),
inference(cp,[status(thm)],[t1163822,t1056721]) ).
cnf(t1174349,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,complement(meet(X1,complement(X3))))),
inference(step,[status(thm)],[t1163880,t2811]) ).
cnf(t1174350,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,complement(complement(X3)))),
inference(step,[status(thm)],[t1174349,t1163822]) ).
cnf(t1174351,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t1174350,t2811]) ).
cnf(t1165061,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t1174351]) ).
cnf(t1174354,plain,
meet(X1,join(meet(X2,X1),X3)) = join(meet(X2,X1),meet(X1,X3)),
inference(step,[status(thm)],[t3015,t1165061]) ).
cnf(t1166396,plain,
meet(X1,join(meet(X2,X1),X3)) = join(meet(X2,X1),meet(X1,X3)),
inference(rw,[status(thm)],[t1174354]) ).
cnf(t1174410,plain,
meet(X1,join(X3,meet(X2,X1))) = join(meet(X2,X1),meet(X1,X3)),
inference(step,[status(thm)],[t1166396,t67]) ).
cnf(t1174411,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X2,X1),meet(X1,X3)),
inference(step,[status(thm)],[t1174410,t23]) ).
cnf(t1174412,plain,
meet(X1,join(X3,X2)) = join(meet(X2,X1),meet(X1,X3)),
inference(step,[status(thm)],[t1174411,t1165061]) ).
cnf(t1174413,plain,
meet(X1,join(X2,X3)) = join(meet(X2,X1),meet(X1,X3)),
inference(step,[status(thm)],[t1174412,t67]) ).
cnf(t1174414,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X3),meet(X2,X1)),
inference(step,[status(thm)],[t1174413,t67]) ).
cnf(t1174415,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X3),meet(X1,X2)),
inference(step,[status(thm)],[t1174414,t23]) ).
cnf(t1174416,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,X3)),
inference(step,[status(thm)],[t1174415,t67]) ).
cnf(t1167545,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t1174416]) ).
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,t1167545]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT217-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.04/20.34 % Computer : n012.cluster.edu
% 0.04/20.34 % Model : x86_64 x86_64
% 0.04/20.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/20.34 % Memory : 8046.5625MB
% 0.04/20.34 % OS : Linux 6.8.0-71-generic
% 0.04/20.34 % CPULimit : 300
% 0.04/20.34 % WCLimit : 300
% 0.04/20.34 % DateTime : Wed Sep 23 20:35:18 UTC 2026
% 0.04/20.34 % CPUTime :
% 0.04/20.34 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 225.87/52.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 225.87/52.82 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------