%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT197-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:55:51 PM UTC 2026
% Result : Unsatisfiable 32.12s 15.16s
% Output : Proof 32.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 239
% Number of leaves : 14
% Syntax : Number of formulae : 657 ( 653 unt; 0 def)
% Number of atoms : 665 ( 664 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-4 aty)
% Number of variables : 1571 ( 365 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f10,axiom,
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f10_nnf,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( complement(X0) = X1
| join(X0,X1) != one
| meet(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t11,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t18,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(f4,axiom,
meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f4_nnf,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t7,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t23,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t25,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X2,X1),one,complement(X2),X1),X1),
inference(cp,[status(thm)],[t18,t23]) ).
cnf(f5,axiom,
join(X,Y) = join(Y,X),
file('/export/starexec/sandbox2/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(t63,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t71866,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(step,[status(thm)],[t25,t63]) ).
cnf(t2596,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t71866]) ).
cnf(f9,axiom,
meet(X,complement(X)) = zero,
file('/export/starexec/sandbox2/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(t58,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t2664,plain,
X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t2596,t58]) ).
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(t71867,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t2664,t17]) ).
cnf(f8,axiom,
join(X,complement(X)) = one,
file('/export/starexec/sandbox2/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(t90,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t71868,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t71867,t90]) ).
cnf(t71869,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t71868,t17]) ).
cnf(t2710,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t71869]) ).
cnf(f11,axiom,
meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Z,join(X,Y)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H40) ).
fof(f11_nnf,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Z,join(X,Y)))))),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Z,join(X,Y)))))),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(X1,meet(X2,join(X3,meet(X2,join(X0,X1)))))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t12,plain,
meet(X1,join(X2,meet(X3,join(X4,meet(X3,join(X1,X2)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t46,plain,
meet(X1,join(X2,meet(X3,join(X4,meet(X3,join(X1,X2)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t12]) ).
cnf(f6,axiom,
meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
file('/export/starexec/sandbox2/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(t71585,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)],[t71585]) ).
cnf(f1,axiom,
join(X,X) = X,
file('/export/starexec/sandbox2/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(t49,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X1,X2)))))) = meet(X1,join(X2,meet(X3,meet(X3,join(X1,X2))))),
inference(cp,[status(thm)],[t46,t15]) ).
cnf(t71664,plain,
meet(X1,join(X2,meet(X3,join(X1,X1)))) = meet(X1,join(X2,meet(X3,meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t49,t46]) ).
cnf(t71665,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,meet(X3,meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t71664,t15]) ).
cnf(t71666,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t71665,t23]) ).
cnf(f0,axiom,
meet(X,X) = X,
file('/export/starexec/sandbox2/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(t71587,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t29,t26]) ).
cnf(t71588,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t71587,t23]) ).
cnf(t106,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t71588]) ).
cnf(t71667,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t71666,t106]) ).
cnf(t320,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t71667]) ).
cnf(t336,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),meet(X2,one))),
inference(cp,[status(thm)],[t320,t90]) ).
cnf(f2,axiom,
meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox2/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(t91,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t14,t90]) ).
cnf(t101,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t91]) ).
cnf(t71675,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t336,t101]) ).
cnf(t71676,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(X2,complement(X1))),
inference(step,[status(thm)],[t71675,t63]) ).
cnf(t397,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(X2,complement(X1))),
inference(orient,[status(thm)],[t71676]) ).
cnf(t30,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t26,t14]) ).
cnf(t71601,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t30,t26]) ).
cnf(t71602,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t71601,t23]) ).
cnf(t71603,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t71602,t23]) ).
cnf(t165,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t71603]) ).
cnf(t412,plain,
meet(X1,join(meet(X2,join(X1,X3)),complement(X1))) = meet(X1,join(complement(X1),meet(X1,X2))),
inference(cp,[status(thm)],[t397,t165]) ).
cnf(t71746,plain,
meet(X1,join(complement(X1),meet(X2,join(X1,X3)))) = meet(X1,join(complement(X1),meet(X1,X2))),
inference(step,[status(thm)],[t412,t63]) ).
cnf(t71747,plain,
meet(X1,join(complement(X1),meet(X2,join(X1,X3)))) = meet(X1,join(X2,complement(X1))),
inference(step,[status(thm)],[t71746,t397]) ).
cnf(t842,plain,
meet(X1,join(complement(X1),meet(X2,join(X1,X3)))) = meet(X1,join(X2,complement(X1))),
inference(orient,[status(thm)],[t71747]) ).
cnf(f7,axiom,
join(join(X,Y),Z) = join(X,join(Y,Z)),
file('/export/starexec/sandbox2/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(t71586,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t9,t63]) ).
cnf(t68,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t71586]) ).
cnf(t71,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t68,t15]) ).
cnf(t71590,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t71,t68]) ).
cnf(t71591,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t71590,t63]) ).
cnf(t121,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t71591]) ).
cnf(t124,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t121,t90]) ).
cnf(t71592,plain,
one = join(X1,one),
inference(step,[status(thm)],[t124,t90]) ).
cnf(t132,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t71592]) ).
cnf(t331,plain,
meet(X1,join(one,meet(X1,X2))) = meet(X1,join(one,meet(X2,one))),
inference(cp,[status(thm)],[t320,t132]) ).
cnf(t71669,plain,
meet(X1,join(one,meet(X1,X2))) = meet(X1,join(one,X2)),
inference(step,[status(thm)],[t331,t101]) ).
cnf(t71670,plain,
meet(X1,join(one,meet(X1,X2))) = meet(X1,join(X2,one)),
inference(step,[status(thm)],[t71669,t63]) ).
cnf(t71671,plain,
meet(X1,join(one,meet(X1,X2))) = meet(X1,one),
inference(step,[status(thm)],[t71670,t132]) ).
cnf(t71672,plain,
meet(X1,join(one,meet(X1,X2))) = X1,
inference(step,[status(thm)],[t71671,t101]) ).
cnf(t365,plain,
meet(X1,join(one,meet(X1,X2))) = X1,
inference(orient,[status(thm)],[t71672]) ).
cnf(t61,plain,
meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
inference(cp,[status(thm)],[t26,t58]) ).
cnf(t71597,plain,
meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
inference(step,[status(thm)],[t61,t23]) ).
cnf(t109,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t106,t58]) ).
cnf(t71589,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t109,t58]) ).
cnf(t116,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t71589]) ).
cnf(t71598,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t71597,t116]) ).
cnf(t150,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t71598]) ).
cnf(t155,plain,
meet(X1,meet(meet(X2,complement(X1)),X3)) = meet(X3,zero),
inference(cp,[status(thm)],[t26,t150]) ).
cnf(t71607,plain,
meet(X1,meet(X3,meet(X2,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t155,t23]) ).
cnf(t71608,plain,
meet(X1,meet(X2,meet(complement(X1),X3))) = meet(X3,zero),
inference(step,[status(thm)],[t71607,t26]) ).
cnf(t71609,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t71608,t23]) ).
cnf(t71610,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(step,[status(thm)],[t71609,t116]) ).
cnf(t190,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t71610]) ).
cnf(t406,plain,
meet(X1,join(meet(X2,meet(X3,complement(X1))),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t397,t190]) ).
cnf(t71696,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t406,t63]) ).
cnf(f3,axiom,
join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox2/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(t59,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t16,t58]) ).
cnf(t95,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t59]) ).
cnf(t71697,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t71696,t95]) ).
cnf(t71698,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = zero,
inference(step,[status(thm)],[t71697,t58]) ).
cnf(t538,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = zero,
inference(orient,[status(thm)],[t71698]) ).
cnf(t411,plain,
meet(X1,join(meet(X2,complement(X1)),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t397,t150]) ).
cnf(t71688,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t411,t63]) ).
cnf(t71689,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t71688,t95]) ).
cnf(t71690,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = zero,
inference(step,[status(thm)],[t71689,t58]) ).
cnf(t483,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t71690]) ).
cnf(t850,plain,
meet(complement(X1),join(X1,complement(complement(X1)))) = meet(complement(X1),join(complement(complement(X1)),zero)),
inference(cp,[status(thm)],[t842,t483]) ).
cnf(t71748,plain,
meet(complement(X1),join(X1,complement(complement(X1)))) = meet(complement(X1),complement(complement(X1))),
inference(step,[status(thm)],[t850,t95]) ).
cnf(t71749,plain,
meet(complement(X1),join(X1,complement(complement(X1)))) = zero,
inference(step,[status(thm)],[t71748,t58]) ).
cnf(t883,plain,
meet(complement(X1),join(X1,complement(complement(X1)))) = zero,
inference(orient,[status(thm)],[t71749]) ).
cnf(t884,plain,
join(X1,complement(complement(X1))) = ifeq(zero,zero,ifeq(join(complement(X1),join(X1,complement(complement(X1)))),one,complement(complement(X1)),join(X1,complement(complement(X1)))),join(X1,complement(complement(X1)))),
inference(cp,[status(thm)],[t18,t883]) ).
cnf(t71750,plain,
join(X1,complement(complement(X1))) = ifeq(join(complement(X1),join(X1,complement(complement(X1)))),one,complement(complement(X1)),join(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t884,t17]) ).
cnf(t93,plain,
join(X1,join(complement(X1),X2)) = join(X2,one),
inference(cp,[status(thm)],[t68,t90]) ).
cnf(t71599,plain,
join(X1,join(X2,complement(X1))) = join(X2,one),
inference(step,[status(thm)],[t93,t63]) ).
cnf(t71600,plain,
join(X1,join(X2,complement(X1))) = one,
inference(step,[status(thm)],[t71599,t132]) ).
cnf(t157,plain,
join(X1,join(X2,complement(X1))) = one,
inference(orient,[status(thm)],[t71600]) ).
cnf(t71751,plain,
join(X1,complement(complement(X1))) = ifeq(one,one,complement(complement(X1)),join(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t71750,t157]) ).
cnf(t71752,plain,
join(X1,complement(complement(X1))) = complement(complement(X1)),
inference(step,[status(thm)],[t71751,t17]) ).
cnf(t891,plain,
join(X1,complement(complement(X1))) = complement(complement(X1)),
inference(orient,[status(thm)],[t71752]) ).
cnf(t892,plain,
X1 = meet(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t14,t891]) ).
cnf(t907,plain,
meet(X1,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t892]) ).
cnf(t929,plain,
zero = meet(complement(X1),join(complement(complement(X1)),meet(X2,X1))),
inference(cp,[status(thm)],[t538,t907]) ).
cnf(t71754,plain,
zero = meet(complement(X1),join(meet(X2,X1),complement(complement(X1)))),
inference(step,[status(thm)],[t929,t63]) ).
cnf(t71755,plain,
zero = meet(complement(X1),join(meet(X1,X2),complement(complement(X1)))),
inference(step,[status(thm)],[t71754,t23]) ).
cnf(t1004,plain,
meet(complement(X1),join(meet(X1,X2),complement(complement(X1)))) = zero,
inference(orient,[status(thm)],[t71755]) ).
cnf(t1011,plain,
join(meet(X1,X2),complement(complement(X1))) = ifeq(zero,zero,ifeq(join(complement(X1),join(meet(X1,X2),complement(complement(X1)))),one,complement(complement(X1)),join(meet(X1,X2),complement(complement(X1)))),join(meet(X1,X2),complement(complement(X1)))),
inference(cp,[status(thm)],[t18,t1004]) ).
cnf(t71756,plain,
join(meet(X1,X2),complement(complement(X1))) = ifeq(join(complement(X1),join(meet(X1,X2),complement(complement(X1)))),one,complement(complement(X1)),join(meet(X1,X2),complement(complement(X1)))),
inference(step,[status(thm)],[t1011,t17]) ).
cnf(t71757,plain,
join(meet(X1,X2),complement(complement(X1))) = ifeq(one,one,complement(complement(X1)),join(meet(X1,X2),complement(complement(X1)))),
inference(step,[status(thm)],[t71756,t157]) ).
cnf(t71758,plain,
join(meet(X1,X2),complement(complement(X1))) = complement(complement(X1)),
inference(step,[status(thm)],[t71757,t17]) ).
cnf(t1022,plain,
join(meet(X1,X2),complement(complement(X1))) = complement(complement(X1)),
inference(orient,[status(thm)],[t71758]) ).
cnf(t1028,plain,
meet(X1,X2) = meet(meet(X1,X2),complement(complement(X1))),
inference(cp,[status(thm)],[t14,t1022]) ).
cnf(t1044,plain,
meet(meet(X1,X2),complement(complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t1028]) ).
cnf(t1053,plain,
meet(X1,X2) = meet(meet(X1,X2),join(one,meet(X1,X2))),
inference(cp,[status(thm)],[t365,t1044]) ).
cnf(t1130,plain,
meet(meet(X1,X2),join(one,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t1053]) ).
cnf(t1151,plain,
meet(one,join(meet(X1,X2),complement(one))) = meet(one,join(complement(one),meet(X1,X2))),
inference(cp,[status(thm)],[t842,t1130]) ).
cnf(t118,plain,
zero = ifeq(zero,zero,ifeq(join(X1,zero),one,complement(X1),zero),zero),
inference(cp,[status(thm)],[t18,t116]) ).
cnf(t71593,plain,
zero = ifeq(join(X1,zero),one,complement(X1),zero),
inference(step,[status(thm)],[t118,t17]) ).
cnf(t71594,plain,
zero = ifeq(X1,one,complement(X1),zero),
inference(step,[status(thm)],[t71593,t95]) ).
cnf(t138,plain,
ifeq(X1,one,complement(X1),zero) = zero,
inference(orient,[status(thm)],[t71594]) ).
cnf(t139,plain,
zero = complement(one),
inference(cp,[status(thm)],[t138,t17]) ).
cnf(t140,plain,
complement(one) = zero,
inference(orient,[status(thm)],[t139]) ).
cnf(t71761,plain,
meet(one,join(meet(X1,X2),zero)) = meet(one,join(complement(one),meet(X1,X2))),
inference(step,[status(thm)],[t1151,t140]) ).
cnf(t71762,plain,
meet(one,meet(X1,X2)) = meet(one,join(complement(one),meet(X1,X2))),
inference(step,[status(thm)],[t71761,t95]) ).
cnf(t71763,plain,
meet(one,meet(X1,X2)) = meet(one,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t71762,t140]) ).
cnf(t71764,plain,
meet(X2,meet(one,X1)) = meet(one,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t71763,t26]) ).
cnf(t71765,plain,
meet(X1,meet(X2,one)) = meet(one,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t71764,t26]) ).
cnf(t71766,plain,
meet(X1,X2) = meet(one,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t71765,t101]) ).
cnf(t1161,plain,
meet(one,join(zero,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t71766]) ).
cnf(t1193,plain,
meet(join(zero,meet(X1,X2)),meet(X3,one)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t26,t1161]) ).
cnf(t71767,plain,
meet(join(zero,meet(X1,X2)),X3) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t1193,t101]) ).
cnf(t71768,plain,
meet(X3,join(zero,meet(X1,X2))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t71767,t23]) ).
cnf(t71769,plain,
meet(X3,join(zero,meet(X1,X2))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t71768,t26]) ).
cnf(t71770,plain,
meet(X3,join(zero,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t71769,t26]) ).
cnf(t1210,plain,
meet(X1,join(zero,meet(X2,X3))) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t71770]) ).
cnf(t1215,plain,
meet(X1,meet(X2,join(zero,meet(X1,X2)))) = join(zero,meet(X1,X2)),
inference(cp,[status(thm)],[t1210,t13]) ).
cnf(t71777,plain,
meet(X1,meet(X1,meet(X2,X2))) = join(zero,meet(X1,X2)),
inference(step,[status(thm)],[t1215,t1210]) ).
cnf(t71778,plain,
meet(X1,meet(X2,X2)) = join(zero,meet(X1,X2)),
inference(step,[status(thm)],[t71777,t106]) ).
cnf(t71779,plain,
meet(X1,X2) = join(zero,meet(X1,X2)),
inference(step,[status(thm)],[t71778,t13]) ).
cnf(t1286,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t71779]) ).
cnf(t1306,plain,
meet(X1,join(zero,meet(X2,join(X1,X3)))) = meet(X1,meet(X2,join(X3,meet(X2,join(X1,zero))))),
inference(cp,[status(thm)],[t46,t1286]) ).
cnf(t71781,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(X2,join(X3,meet(X2,join(X1,zero))))),
inference(step,[status(thm)],[t1306,t1286]) ).
cnf(t71782,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X2,join(X1,zero))))),
inference(step,[status(thm)],[t71781,t165]) ).
cnf(t71783,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X2,X1)))),
inference(step,[status(thm)],[t71782,t95]) ).
cnf(t71784,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t71783,t23]) ).
cnf(t1312,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t71784]) ).
cnf(t1340,plain,
meet(X1,meet(X1,X2)) = meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t1312,t106]) ).
cnf(t71929,plain,
meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t1340,t106]) ).
cnf(t3004,plain,
meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t71929]) ).
cnf(t198,plain,
meet(X1,meet(meet(X2,meet(X3,complement(X1))),X4)) = meet(X4,zero),
inference(cp,[status(thm)],[t26,t190]) ).
cnf(t71616,plain,
meet(X1,meet(X4,meet(X2,meet(X3,complement(X1))))) = meet(X4,zero),
inference(step,[status(thm)],[t198,t23]) ).
cnf(t71617,plain,
meet(X1,meet(X2,meet(meet(X3,complement(X1)),X4))) = meet(X4,zero),
inference(step,[status(thm)],[t71616,t26]) ).
cnf(t71618,plain,
meet(X1,meet(X2,meet(X4,meet(X3,complement(X1))))) = meet(X4,zero),
inference(step,[status(thm)],[t71617,t23]) ).
cnf(t71619,plain,
meet(X1,meet(X2,meet(X3,meet(complement(X1),X4)))) = meet(X4,zero),
inference(step,[status(thm)],[t71618,t26]) ).
cnf(t71620,plain,
meet(X1,meet(X2,meet(X3,meet(X4,complement(X1))))) = meet(X4,zero),
inference(step,[status(thm)],[t71619,t23]) ).
cnf(t71621,plain,
meet(X1,meet(X2,meet(X3,meet(X4,complement(X1))))) = zero,
inference(step,[status(thm)],[t71620,t116]) ).
cnf(t212,plain,
meet(X1,meet(X2,meet(X3,meet(X4,complement(X1))))) = zero,
inference(orient,[status(thm)],[t71621]) ).
cnf(t905,plain,
join(X1,join(complement(complement(X1)),X2)) = join(X2,complement(complement(X1))),
inference(cp,[status(thm)],[t68,t891]) ).
cnf(t71753,plain,
join(X1,join(X2,complement(complement(X1)))) = join(X2,complement(complement(X1))),
inference(step,[status(thm)],[t905,t63]) ).
cnf(t950,plain,
join(X1,join(X2,complement(complement(X1)))) = join(X2,complement(complement(X1))),
inference(orient,[status(thm)],[t71753]) ).
cnf(t954,plain,
X1 = meet(X1,join(X2,complement(complement(X1)))),
inference(cp,[status(thm)],[t14,t950]) ).
cnf(t970,plain,
meet(X1,join(X2,complement(complement(X1)))) = X1,
inference(orient,[status(thm)],[t954]) ).
cnf(t986,plain,
meet(X1,join(complement(complement(X2)),meet(X1,X2))) = meet(X1,join(complement(complement(X2)),X2)),
inference(cp,[status(thm)],[t320,t970]) ).
cnf(t71792,plain,
meet(X1,join(meet(X1,X2),complement(complement(X2)))) = meet(X1,join(complement(complement(X2)),X2)),
inference(step,[status(thm)],[t986,t63]) ).
cnf(t71793,plain,
meet(X1,join(meet(X1,X2),complement(complement(X2)))) = meet(X1,join(X2,complement(complement(X2)))),
inference(step,[status(thm)],[t71792,t63]) ).
cnf(t71794,plain,
meet(X1,join(meet(X1,X2),complement(complement(X2)))) = meet(X1,complement(complement(X2))),
inference(step,[status(thm)],[t71793,t891]) ).
cnf(t1443,plain,
meet(X1,join(meet(X1,X2),complement(complement(X2)))) = meet(X1,complement(complement(X2))),
inference(orient,[status(thm)],[t71794]) ).
cnf(t1464,plain,
meet(X1,complement(complement(join(X1,X2)))) = meet(X1,join(X1,complement(complement(join(X1,X2))))),
inference(cp,[status(thm)],[t1443,t14]) ).
cnf(t71797,plain,
meet(X1,complement(complement(join(X1,X2)))) = X1,
inference(step,[status(thm)],[t1464,t14]) ).
cnf(t1520,plain,
meet(X1,complement(complement(join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t71797]) ).
cnf(t1543,plain,
zero = meet(complement(join(X1,X2)),meet(X3,meet(X4,X1))),
inference(cp,[status(thm)],[t212,t1520]) ).
cnf(t71819,plain,
zero = meet(meet(X4,X1),meet(complement(join(X1,X2)),X3)),
inference(step,[status(thm)],[t1543,t26]) ).
cnf(t71820,plain,
zero = meet(X3,meet(meet(X4,X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t71819,t26]) ).
cnf(t71821,plain,
zero = meet(X3,meet(meet(X1,X4),complement(join(X1,X2)))),
inference(step,[status(thm)],[t71820,t23]) ).
cnf(t1922,plain,
meet(X1,meet(meet(X2,X3),complement(join(X2,X4)))) = zero,
inference(orient,[status(thm)],[t71821]) ).
cnf(t1923,plain,
zero = meet(meet(X1,X2),complement(join(X1,X3))),
inference(cp,[status(thm)],[t1922,t106]) ).
cnf(t1950,plain,
meet(meet(X1,X2),complement(join(X1,X3))) = zero,
inference(orient,[status(thm)],[t1923]) ).
cnf(t1968,plain,
meet(meet(X1,X2),join(complement(join(X1,X3)),complement(meet(X1,X2)))) = meet(meet(X1,X2),join(complement(meet(X1,X2)),zero)),
inference(cp,[status(thm)],[t397,t1950]) ).
cnf(t72191,plain,
meet(meet(X1,X2),join(complement(meet(X1,X2)),complement(join(X1,X3)))) = meet(meet(X1,X2),join(complement(meet(X1,X2)),zero)),
inference(step,[status(thm)],[t1968,t63]) ).
cnf(t72192,plain,
meet(meet(X1,X2),join(complement(meet(X1,X2)),complement(join(X1,X3)))) = meet(meet(X1,X2),complement(meet(X1,X2))),
inference(step,[status(thm)],[t72191,t95]) ).
cnf(t72193,plain,
meet(meet(X1,X2),join(complement(meet(X1,X2)),complement(join(X1,X3)))) = zero,
inference(step,[status(thm)],[t72192,t58]) ).
cnf(t8769,plain,
meet(meet(X1,X2),join(complement(meet(X1,X2)),complement(join(X1,X3)))) = zero,
inference(orient,[status(thm)],[t72193]) ).
cnf(t8777,plain,
zero = meet(meet(X1,X2),join(complement(meet(X1,X2)),complement(X1))),
inference(cp,[status(thm)],[t8769,t15]) ).
cnf(t72194,plain,
zero = meet(meet(X1,X2),join(complement(X1),complement(meet(X1,X2)))),
inference(step,[status(thm)],[t8777,t63]) ).
cnf(t8829,plain,
meet(meet(X1,X2),join(complement(X1),complement(meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t72194]) ).
cnf(t8839,plain,
join(complement(X1),complement(meet(X1,X2))) = ifeq(zero,zero,ifeq(join(meet(X1,X2),join(complement(X1),complement(meet(X1,X2)))),one,complement(meet(X1,X2)),join(complement(X1),complement(meet(X1,X2)))),join(complement(X1),complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t18,t8829]) ).
cnf(t72195,plain,
join(complement(X1),complement(meet(X1,X2))) = ifeq(join(meet(X1,X2),join(complement(X1),complement(meet(X1,X2)))),one,complement(meet(X1,X2)),join(complement(X1),complement(meet(X1,X2)))),
inference(step,[status(thm)],[t8839,t17]) ).
cnf(t72196,plain,
join(complement(X1),complement(meet(X1,X2))) = ifeq(one,one,complement(meet(X1,X2)),join(complement(X1),complement(meet(X1,X2)))),
inference(step,[status(thm)],[t72195,t157]) ).
cnf(t72197,plain,
join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t72196,t17]) ).
cnf(t8887,plain,
join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t72197]) ).
cnf(t8893,plain,
complement(X1) = meet(complement(X1),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t14,t8887]) ).
cnf(t8948,plain,
meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t8893]) ).
cnf(t8986,plain,
meet(complement(X1),complement(meet(X1,X2))) = meet(complement(X1),meet(complement(X1),join(X3,meet(complement(X1),complement(meet(X1,X2)))))),
inference(cp,[status(thm)],[t3004,t8948]) ).
cnf(t72200,plain,
complement(X1) = meet(complement(X1),meet(complement(X1),join(X3,meet(complement(X1),complement(meet(X1,X2)))))),
inference(step,[status(thm)],[t8986,t8948]) ).
cnf(t72201,plain,
complement(X1) = meet(complement(X1),join(X3,meet(complement(X1),complement(meet(X1,X2))))),
inference(step,[status(thm)],[t72200,t106]) ).
cnf(t72202,plain,
complement(X1) = meet(complement(X1),join(X3,complement(X1))),
inference(step,[status(thm)],[t72201,t8948]) ).
cnf(t9091,plain,
meet(complement(X1),join(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t72202]) ).
cnf(t8888,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(meet(complement(X1),X2))),
inference(cp,[status(thm)],[t8887,t2710]) ).
cnf(t72203,plain,
complement(meet(X2,complement(X1))) = join(X1,complement(meet(complement(X1),X2))),
inference(step,[status(thm)],[t8888,t23]) ).
cnf(t72204,plain,
complement(meet(X2,complement(X1))) = join(X1,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t72203,t23]) ).
cnf(t9149,plain,
join(X1,complement(meet(X2,complement(X1)))) = complement(meet(X2,complement(X1))),
inference(orient,[status(thm)],[t72204]) ).
cnf(t9153,plain,
complement(meet(X1,complement(complement(X2)))) = join(complement(X2),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t9149,t2710]) ).
cnf(t72208,plain,
complement(meet(X1,X2)) = join(complement(X2),complement(meet(X1,X2))),
inference(step,[status(thm)],[t9153,t2710]) ).
cnf(t9299,plain,
join(complement(X1),complement(meet(X2,X1))) = complement(meet(X2,X1)),
inference(orient,[status(thm)],[t72208]) ).
cnf(t9320,plain,
complement(meet(complement(X1),join(X2,complement(X1)))) = join(complement(join(X2,complement(X1))),complement(complement(X1))),
inference(cp,[status(thm)],[t9299,t9091]) ).
cnf(t72209,plain,
complement(complement(X1)) = join(complement(join(X2,complement(X1))),complement(complement(X1))),
inference(step,[status(thm)],[t9320,t9091]) ).
cnf(t72210,plain,
X1 = join(complement(join(X2,complement(X1))),complement(complement(X1))),
inference(step,[status(thm)],[t72209,t2710]) ).
cnf(t72211,plain,
X1 = join(complement(complement(X1)),complement(join(X2,complement(X1)))),
inference(step,[status(thm)],[t72210,t63]) ).
cnf(t72212,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(step,[status(thm)],[t72211,t2710]) ).
cnf(t9381,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t72212]) ).
cnf(t9386,plain,
complement(join(X1,complement(X2))) = meet(complement(join(X1,complement(X2))),X2),
inference(cp,[status(thm)],[t9091,t9381]) ).
cnf(t72223,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t9386,t23]) ).
cnf(t9610,plain,
meet(X1,complement(join(X2,complement(X1)))) = complement(join(X2,complement(X1))),
inference(orient,[status(thm)],[t72223]) ).
cnf(t9616,plain,
complement(join(X1,complement(complement(X2)))) = meet(complement(X2),complement(join(X1,X2))),
inference(cp,[status(thm)],[t9610,t2710]) ).
cnf(t72228,plain,
complement(join(X1,X2)) = meet(complement(X2),complement(join(X1,X2))),
inference(step,[status(thm)],[t9616,t2710]) ).
cnf(t9760,plain,
meet(complement(X1),complement(join(X2,X1))) = complement(join(X2,X1)),
inference(orient,[status(thm)],[t72228]) ).
cnf(t134,plain,
one = ifeq(meet(X1,one),zero,ifeq(one,one,complement(X1),one),one),
inference(cp,[status(thm)],[t18,t132]) ).
cnf(t71595,plain,
one = ifeq(X1,zero,ifeq(one,one,complement(X1),one),one),
inference(step,[status(thm)],[t134,t101]) ).
cnf(t71596,plain,
one = ifeq(X1,zero,complement(X1),one),
inference(step,[status(thm)],[t71595,t17]) ).
cnf(t142,plain,
ifeq(X1,zero,complement(X1),one) = one,
inference(orient,[status(thm)],[t71596]) ).
cnf(t2713,plain,
one = ifeq(complement(X1),zero,X1,one),
inference(cp,[status(thm)],[t142,t2710]) ).
cnf(t2784,plain,
ifeq(complement(X1),zero,X1,one) = one,
inference(orient,[status(thm)],[t2713]) ).
cnf(t1952,plain,
zero = meet(meet(X1,X2),complement(join(X2,X3))),
inference(cp,[status(thm)],[t1950,t23]) ).
cnf(t1973,plain,
meet(meet(X1,X2),complement(join(X2,X3))) = zero,
inference(orient,[status(thm)],[t1952]) ).
cnf(t2010,plain,
zero = meet(meet(X1,meet(X2,X3)),complement(join(meet(X1,X2),X4))),
inference(cp,[status(thm)],[t1973,t26]) ).
cnf(t71960,plain,
zero = meet(meet(X1,meet(X2,X3)),complement(join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t2010,t63]) ).
cnf(t3615,plain,
meet(meet(X1,meet(X2,X3)),complement(join(X4,meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t71960]) ).
cnf(t3616,plain,
zero = meet(complement(join(X1,meet(X2,X3))),meet(X2,meet(X3,X4))),
inference(cp,[status(thm)],[t3615,t23]) ).
cnf(t72083,plain,
zero = meet(meet(X3,X4),meet(complement(join(X1,meet(X2,X3))),X2)),
inference(step,[status(thm)],[t3616,t26]) ).
cnf(t72084,plain,
zero = meet(X2,meet(meet(X3,X4),complement(join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t72083,t26]) ).
cnf(t6153,plain,
meet(X1,meet(meet(X2,X3),complement(join(X4,meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t72084]) ).
cnf(t6157,plain,
zero = meet(X1,meet(meet(X2,X3),complement(join(X4,meet(X1,X3))))),
inference(cp,[status(thm)],[t6153,t23]) ).
cnf(t7383,plain,
meet(X1,meet(meet(X2,X3),complement(join(X4,meet(X1,X3))))) = zero,
inference(orient,[status(thm)],[t6157]) ).
cnf(t7399,plain,
zero = meet(X1,meet(X2,complement(join(X3,meet(X1,join(X2,X4)))))),
inference(cp,[status(thm)],[t7383,t14]) ).
cnf(t7541,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,join(X2,X4)))))) = zero,
inference(orient,[status(thm)],[t7399]) ).
cnf(t9316,plain,
complement(meet(X1,join(X1,X2))) = join(complement(join(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t9299,t14]) ).
cnf(t72214,plain,
complement(X1) = join(complement(join(X1,X2)),complement(X1)),
inference(step,[status(thm)],[t9316,t14]) ).
cnf(t72215,plain,
complement(X1) = join(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t72214,t63]) ).
cnf(t9435,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t72215]) ).
cnf(t9443,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t9091,t9435]) ).
cnf(t72216,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t9443,t23]) ).
cnf(t9490,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t72216]) ).
cnf(t9554,plain,
zero = meet(X1,complement(join(X2,meet(X1,join(complement(X2),X3))))),
inference(cp,[status(thm)],[t7541,t9490]) ).
cnf(t72268,plain,
zero = meet(X1,complement(join(X2,meet(X1,join(X3,complement(X2)))))),
inference(step,[status(thm)],[t9554,t63]) ).
cnf(t11753,plain,
meet(X1,complement(join(X2,meet(X1,join(X3,complement(X2)))))) = zero,
inference(orient,[status(thm)],[t72268]) ).
cnf(t11755,plain,
zero = meet(X1,complement(join(join(X2,complement(X3)),meet(X1,X3)))),
inference(cp,[status(thm)],[t11753,t9381]) ).
cnf(t72279,plain,
zero = meet(X1,complement(join(meet(X1,X3),join(X2,complement(X3))))),
inference(step,[status(thm)],[t11755,t63]) ).
cnf(t72280,plain,
zero = meet(X1,complement(join(complement(X3),join(meet(X1,X3),X2)))),
inference(step,[status(thm)],[t72279,t68]) ).
cnf(t72281,plain,
zero = meet(X1,complement(join(X2,join(complement(X3),meet(X1,X3))))),
inference(step,[status(thm)],[t72280,t68]) ).
cnf(t12206,plain,
meet(X1,complement(join(X2,join(complement(X3),meet(X1,X3))))) = zero,
inference(orient,[status(thm)],[t72281]) ).
cnf(t12208,plain,
zero = complement(join(X1,join(complement(X2),meet(complement(X1),X2)))),
inference(cp,[status(thm)],[t12206,t9490]) ).
cnf(t72282,plain,
zero = complement(join(X1,join(complement(X2),meet(X2,complement(X1))))),
inference(step,[status(thm)],[t12208,t23]) ).
cnf(t12370,plain,
complement(join(X1,join(complement(X2),meet(X2,complement(X1))))) = zero,
inference(orient,[status(thm)],[t72282]) ).
cnf(t12413,plain,
one = ifeq(zero,zero,join(X1,join(complement(X2),meet(X2,complement(X1)))),one),
inference(cp,[status(thm)],[t2784,t12370]) ).
cnf(t72290,plain,
one = join(X1,join(complement(X2),meet(X2,complement(X1)))),
inference(step,[status(thm)],[t12413,t17]) ).
cnf(t12649,plain,
join(X1,join(complement(X2),meet(X2,complement(X1)))) = one,
inference(orient,[status(thm)],[t72290]) ).
cnf(t1998,plain,
zero = meet(meet(X1,X2),complement(join(meet(X2,join(X1,X3)),X4))),
inference(cp,[status(thm)],[t1973,t165]) ).
cnf(t71933,plain,
zero = meet(meet(X1,X2),complement(join(X4,meet(X2,join(X1,X3))))),
inference(step,[status(thm)],[t1998,t63]) ).
cnf(t3053,plain,
meet(meet(X1,X2),complement(join(X3,meet(X2,join(X1,X4))))) = zero,
inference(orient,[status(thm)],[t71933]) ).
cnf(t3080,plain,
zero = meet(meet(X1,X2),complement(meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t3053,t15]) ).
cnf(t3158,plain,
meet(meet(X1,X2),complement(meet(X2,join(X1,X3)))) = zero,
inference(orient,[status(thm)],[t3080]) ).
cnf(t12680,plain,
one = join(meet(X1,join(X2,X3)),join(complement(meet(X2,X1)),zero)),
inference(cp,[status(thm)],[t12649,t3158]) ).
cnf(t72326,plain,
one = join(meet(X1,join(X2,X3)),complement(meet(X2,X1))),
inference(step,[status(thm)],[t12680,t95]) ).
cnf(t72327,plain,
one = join(complement(meet(X2,X1)),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t72326,t63]) ).
cnf(t72328,plain,
one = join(complement(meet(X1,X2)),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t72327,t23]) ).
cnf(t13548,plain,
join(complement(meet(X1,X2)),meet(X1,join(X2,X3))) = one,
inference(orient,[status(thm)],[t72328]) ).
cnf(t13576,plain,
one = join(complement(complement(X1)),meet(complement(X1),join(join(X2,complement(X1)),X3))),
inference(cp,[status(thm)],[t13548,t9091]) ).
cnf(t72427,plain,
one = join(X1,meet(complement(X1),join(join(X2,complement(X1)),X3))),
inference(step,[status(thm)],[t13576,t2710]) ).
cnf(t72428,plain,
one = join(X1,meet(complement(X1),join(X3,join(X2,complement(X1))))),
inference(step,[status(thm)],[t72427,t63]) ).
cnf(t72429,plain,
one = join(X1,meet(complement(X1),join(X2,join(complement(X1),X3)))),
inference(step,[status(thm)],[t72428,t68]) ).
cnf(t72430,plain,
one = join(X1,meet(complement(X1),join(X2,join(X3,complement(X1))))),
inference(step,[status(thm)],[t72429,t63]) ).
cnf(t16973,plain,
join(X1,meet(complement(X1),join(X2,join(X3,complement(X1))))) = one,
inference(orient,[status(thm)],[t72430]) ).
cnf(t16982,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = ifeq(meet(X1,meet(complement(X1),join(X2,join(X3,complement(X1))))),zero,ifeq(one,one,complement(X1),meet(complement(X1),join(X2,join(X3,complement(X1))))),meet(complement(X1),join(X2,join(X3,complement(X1))))),
inference(cp,[status(thm)],[t18,t16973]) ).
cnf(t12407,plain,
zero = complement(join(join(X1,X2),join(complement(meet(X1,X3)),zero))),
inference(cp,[status(thm)],[t12370,t1950]) ).
cnf(t72283,plain,
zero = complement(join(join(X1,X2),complement(meet(X1,X3)))),
inference(step,[status(thm)],[t12407,t95]) ).
cnf(t12452,plain,
complement(join(join(X1,X2),complement(meet(X1,X3)))) = zero,
inference(orient,[status(thm)],[t72283]) ).
cnf(t12477,plain,
one = ifeq(zero,zero,join(join(X1,X2),complement(meet(X1,X3))),one),
inference(cp,[status(thm)],[t2784,t12452]) ).
cnf(t72284,plain,
one = join(join(X1,X2),complement(meet(X1,X3))),
inference(step,[status(thm)],[t12477,t17]) ).
cnf(t12517,plain,
join(join(X1,X2),complement(meet(X1,X3))) = one,
inference(orient,[status(thm)],[t72284]) ).
cnf(t12545,plain,
zero = meet(meet(join(X1,X2),X3),complement(meet(X3,one))),
inference(cp,[status(thm)],[t3158,t12517]) ).
cnf(t72285,plain,
zero = meet(complement(meet(X3,one)),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t12545,t23]) ).
cnf(t72286,plain,
zero = meet(X3,meet(complement(meet(X3,one)),join(X1,X2))),
inference(step,[status(thm)],[t72285,t26]) ).
cnf(t72287,plain,
zero = meet(X3,meet(join(X1,X2),complement(meet(X3,one)))),
inference(step,[status(thm)],[t72286,t23]) ).
cnf(t72288,plain,
zero = meet(X3,meet(join(X1,X2),complement(X3))),
inference(step,[status(thm)],[t72287,t101]) ).
cnf(t72289,plain,
zero = meet(X3,meet(complement(X3),join(X1,X2))),
inference(step,[status(thm)],[t72288,t23]) ).
cnf(t12603,plain,
meet(X1,meet(complement(X1),join(X2,X3))) = zero,
inference(orient,[status(thm)],[t72289]) ).
cnf(t72431,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = ifeq(zero,zero,ifeq(one,one,complement(X1),meet(complement(X1),join(X2,join(X3,complement(X1))))),meet(complement(X1),join(X2,join(X3,complement(X1))))),
inference(step,[status(thm)],[t16982,t12603]) ).
cnf(t72432,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = ifeq(one,one,complement(X1),meet(complement(X1),join(X2,join(X3,complement(X1))))),
inference(step,[status(thm)],[t72431,t17]) ).
cnf(t72433,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = complement(X1),
inference(step,[status(thm)],[t72432,t17]) ).
cnf(t17026,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t72433]) ).
cnf(t17046,plain,
complement(meet(complement(X1),join(X2,join(X3,complement(X1))))) = join(complement(join(X2,join(X3,complement(X1)))),complement(complement(X1))),
inference(cp,[status(thm)],[t9299,t17026]) ).
cnf(t72434,plain,
complement(complement(X1)) = join(complement(join(X2,join(X3,complement(X1)))),complement(complement(X1))),
inference(step,[status(thm)],[t17046,t17026]) ).
cnf(t72435,plain,
X1 = join(complement(join(X2,join(X3,complement(X1)))),complement(complement(X1))),
inference(step,[status(thm)],[t72434,t2710]) ).
cnf(t72436,plain,
X1 = join(complement(complement(X1)),complement(join(X2,join(X3,complement(X1))))),
inference(step,[status(thm)],[t72435,t63]) ).
cnf(t72437,plain,
X1 = join(X1,complement(join(X2,join(X3,complement(X1))))),
inference(step,[status(thm)],[t72436,t2710]) ).
cnf(t17111,plain,
join(X1,complement(join(X2,join(X3,complement(X1))))) = X1,
inference(orient,[status(thm)],[t72437]) ).
cnf(t9432,plain,
join(X1,join(complement(join(X2,complement(X1))),X3)) = join(X3,X1),
inference(cp,[status(thm)],[t68,t9381]) ).
cnf(t72235,plain,
join(X1,join(X3,complement(join(X2,complement(X1))))) = join(X3,X1),
inference(step,[status(thm)],[t9432,t63]) ).
cnf(t72236,plain,
join(X1,join(X3,complement(join(X2,complement(X1))))) = join(X1,X3),
inference(step,[status(thm)],[t72235,t63]) ).
cnf(t10132,plain,
join(X1,join(X2,complement(join(X3,complement(X1))))) = join(X1,X2),
inference(orient,[status(thm)],[t72236]) ).
cnf(t17112,plain,
join(X1,complement(X2)) = join(join(X1,complement(X2)),complement(join(X2,X3))),
inference(cp,[status(thm)],[t17111,t10132]) ).
cnf(t17621,plain,
join(join(X1,complement(X2)),complement(join(X2,X3))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t17112]) ).
cnf(t17628,plain,
join(X1,complement(complement(X2))) = join(join(X1,X2),complement(join(complement(X2),X3))),
inference(cp,[status(thm)],[t17621,t2710]) ).
cnf(t72445,plain,
join(X1,X2) = join(join(X1,X2),complement(join(complement(X2),X3))),
inference(step,[status(thm)],[t17628,t2710]) ).
cnf(t72446,plain,
join(X1,X2) = join(join(X1,X2),complement(join(X3,complement(X2)))),
inference(step,[status(thm)],[t72445,t63]) ).
cnf(t17722,plain,
join(join(X1,X2),complement(join(X3,complement(X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t72446]) ).
cnf(t17728,plain,
join(X1,meet(X1,X2)) = join(X1,complement(join(X3,complement(meet(X1,X2))))),
inference(cp,[status(thm)],[t17722,t16]) ).
cnf(t72447,plain,
X1 = join(X1,complement(join(X3,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t17728,t16]) ).
cnf(t17833,plain,
join(X1,complement(join(X2,complement(meet(X1,X3))))) = X1,
inference(orient,[status(thm)],[t72447]) ).
cnf(t17858,plain,
complement(join(X1,complement(join(X2,complement(meet(X1,X3)))))) = meet(complement(complement(join(X2,complement(meet(X1,X3))))),complement(X1)),
inference(cp,[status(thm)],[t9760,t17833]) ).
cnf(t72448,plain,
complement(X1) = meet(complement(complement(join(X2,complement(meet(X1,X3))))),complement(X1)),
inference(step,[status(thm)],[t17858,t17833]) ).
cnf(t72449,plain,
complement(X1) = meet(complement(X1),complement(complement(join(X2,complement(meet(X1,X3)))))),
inference(step,[status(thm)],[t72448,t23]) ).
cnf(t72450,plain,
complement(X1) = meet(complement(X1),join(X2,complement(meet(X1,X3)))),
inference(step,[status(thm)],[t72449,t2710]) ).
cnf(t17932,plain,
meet(complement(X1),join(X2,complement(meet(X1,X3)))) = complement(X1),
inference(orient,[status(thm)],[t72450]) ).
cnf(t17933,plain,
complement(complement(X1)) = meet(X1,join(X2,complement(meet(complement(X1),X3)))),
inference(cp,[status(thm)],[t17932,t2710]) ).
cnf(t72451,plain,
X1 = meet(X1,join(X2,complement(meet(complement(X1),X3)))),
inference(step,[status(thm)],[t17933,t2710]) ).
cnf(t72452,plain,
X1 = meet(X1,join(X2,complement(meet(X3,complement(X1))))),
inference(step,[status(thm)],[t72451,t23]) ).
cnf(t18018,plain,
meet(X1,join(X2,complement(meet(X3,complement(X1))))) = X1,
inference(orient,[status(thm)],[t72452]) ).
cnf(t18027,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,complement(complement(X1)))),
inference(cp,[status(thm)],[t18018,t8948]) ).
cnf(t72453,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(step,[status(thm)],[t18027,t2710]) ).
cnf(t72454,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t72453,t63]) ).
cnf(t18118,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t72454]) ).
cnf(t18194,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(meet(X1,X2),meet(meet(X1,X2),join(X4,meet(meet(X1,X2),join(X1,X3))))),
inference(cp,[status(thm)],[t3004,t18118]) ).
cnf(t72459,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(X4,meet(meet(X1,X2),join(X1,X3))))),
inference(step,[status(thm)],[t18194,t18118]) ).
cnf(t72460,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(meet(X1,X2),join(X1,X3)))),
inference(step,[status(thm)],[t72459,t106]) ).
cnf(t72461,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(X1,X2))),
inference(step,[status(thm)],[t72460,t18118]) ).
cnf(t18514,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t72461]) ).
cnf(t47,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(cp,[status(thm)],[t46,t14]) ).
cnf(t239,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t47]) ).
cnf(t321,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,join(X2,X2)),
inference(cp,[status(thm)],[t320,t239]) ).
cnf(t71668,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(step,[status(thm)],[t321,t15]) ).
cnf(t347,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t71668]) ).
cnf(t349,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t347,t165]) ).
cnf(t71711,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(step,[status(thm)],[t349,t165]) ).
cnf(t71712,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t71711,t63]) ).
cnf(t601,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t71712]) ).
cnf(t3183,plain,
zero = meet(meet(meet(X1,X2),X1),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t3158,t601]) ).
cnf(t71938,plain,
zero = meet(complement(meet(X1,X2)),meet(meet(X1,X2),X1)),
inference(step,[status(thm)],[t3183,t23]) ).
cnf(t71939,plain,
zero = meet(X1,meet(complement(meet(X1,X2)),meet(X1,X2))),
inference(step,[status(thm)],[t71938,t26]) ).
cnf(t71940,plain,
zero = meet(X1,meet(X2,meet(complement(meet(X1,X2)),X1))),
inference(step,[status(thm)],[t71939,t26]) ).
cnf(t71941,plain,
zero = meet(X1,meet(X1,meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t71940,t26]) ).
cnf(t71942,plain,
zero = meet(X1,meet(X2,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t71941,t106]) ).
cnf(t3329,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t71942]) ).
cnf(t3353,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = meet(X1,meet(meet(X2,complement(meet(X1,X2))),join(X3,zero))),
inference(cp,[status(thm)],[t1312,t3329]) ).
cnf(t71943,plain,
zero = meet(X1,meet(meet(X2,complement(meet(X1,X2))),join(X3,zero))),
inference(step,[status(thm)],[t3353,t3329]) ).
cnf(t71944,plain,
zero = meet(X1,meet(join(X3,zero),meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t71943,t23]) ).
cnf(t71945,plain,
zero = meet(X1,meet(X2,meet(complement(meet(X1,X2)),join(X3,zero)))),
inference(step,[status(thm)],[t71944,t26]) ).
cnf(t71946,plain,
zero = meet(X1,meet(X2,meet(join(X3,zero),complement(meet(X1,X2))))),
inference(step,[status(thm)],[t71945,t23]) ).
cnf(t71947,plain,
zero = meet(X1,meet(X2,meet(X3,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t71946,t95]) ).
cnf(t3357,plain,
meet(X1,meet(X2,meet(X3,complement(meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t71947]) ).
cnf(t3358,plain,
zero = meet(X1,meet(meet(X2,complement(meet(X3,X1))),X3)),
inference(cp,[status(thm)],[t3357,t26]) ).
cnf(t71948,plain,
zero = meet(X1,meet(X3,meet(X2,complement(meet(X3,X1))))),
inference(step,[status(thm)],[t3358,t23]) ).
cnf(t71949,plain,
zero = meet(X1,meet(X2,meet(complement(meet(X3,X1)),X3))),
inference(step,[status(thm)],[t71948,t26]) ).
cnf(t71950,plain,
zero = meet(X1,meet(X2,meet(X3,complement(meet(X3,X1))))),
inference(step,[status(thm)],[t71949,t23]) ).
cnf(t71951,plain,
zero = meet(X1,meet(X2,meet(X3,complement(meet(X1,X3))))),
inference(step,[status(thm)],[t71950,t23]) ).
cnf(t3431,plain,
meet(X1,meet(X2,meet(X3,complement(meet(X1,X3))))) = zero,
inference(orient,[status(thm)],[t71951]) ).
cnf(t3083,plain,
zero = meet(meet(X1,X2),complement(join(X3,meet(X2,X1)))),
inference(cp,[status(thm)],[t3053,t347]) ).
cnf(t71934,plain,
zero = meet(meet(X1,X2),complement(join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t3083,t23]) ).
cnf(t3219,plain,
meet(meet(X1,X2),complement(join(X3,meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t71934]) ).
cnf(t3475,plain,
zero = meet(meet(X1,X2),meet(X3,meet(complement(join(X4,meet(X1,X2))),complement(zero)))),
inference(cp,[status(thm)],[t3431,t3219]) ).
cnf(t143,plain,
one = complement(zero),
inference(cp,[status(thm)],[t142,t17]) ).
cnf(t145,plain,
complement(zero) = one,
inference(orient,[status(thm)],[t143]) ).
cnf(t72043,plain,
zero = meet(meet(X1,X2),meet(X3,meet(complement(join(X4,meet(X1,X2))),one))),
inference(step,[status(thm)],[t3475,t145]) ).
cnf(t72044,plain,
zero = meet(meet(X1,X2),meet(X3,complement(join(X4,meet(X1,X2))))),
inference(step,[status(thm)],[t72043,t101]) ).
cnf(t72045,plain,
zero = meet(X3,meet(complement(join(X4,meet(X1,X2))),meet(X1,X2))),
inference(step,[status(thm)],[t72044,t26]) ).
cnf(t72046,plain,
zero = meet(X3,meet(X2,meet(complement(join(X4,meet(X1,X2))),X1))),
inference(step,[status(thm)],[t72045,t26]) ).
cnf(t72047,plain,
zero = meet(X3,meet(X1,meet(X2,complement(join(X4,meet(X1,X2)))))),
inference(step,[status(thm)],[t72046,t26]) ).
cnf(t72048,plain,
zero = meet(X1,meet(meet(X2,complement(join(X4,meet(X1,X2)))),X3)),
inference(step,[status(thm)],[t72047,t26]) ).
cnf(t72049,plain,
zero = meet(X1,meet(X3,meet(X2,complement(join(X4,meet(X1,X2)))))),
inference(step,[status(thm)],[t72048,t23]) ).
cnf(t72050,plain,
zero = meet(X1,meet(X2,meet(complement(join(X4,meet(X1,X2))),X3))),
inference(step,[status(thm)],[t72049,t26]) ).
cnf(t72051,plain,
zero = meet(X1,meet(X2,meet(X3,complement(join(X4,meet(X1,X2)))))),
inference(step,[status(thm)],[t72050,t23]) ).
cnf(t5434,plain,
meet(X1,meet(X2,meet(X3,complement(join(X4,meet(X1,X2)))))) = zero,
inference(orient,[status(thm)],[t72051]) ).
cnf(t5437,plain,
zero = meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))),
inference(cp,[status(thm)],[t5434,t106]) ).
cnf(t5572,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t5437]) ).
cnf(t9547,plain,
zero = meet(X1,complement(join(X2,meet(X1,complement(X2))))),
inference(cp,[status(thm)],[t5572,t9490]) ).
cnf(t9957,plain,
meet(X1,complement(join(X2,meet(X1,complement(X2))))) = zero,
inference(orient,[status(thm)],[t9547]) ).
cnf(t9960,plain,
zero = meet(X1,complement(join(complement(X2),meet(X1,X2)))),
inference(cp,[status(thm)],[t9957,t2710]) ).
cnf(t9994,plain,
meet(X1,complement(join(complement(X2),meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t9960]) ).
cnf(t12657,plain,
one = join(join(complement(X1),meet(X2,X1)),join(complement(X2),zero)),
inference(cp,[status(thm)],[t12649,t9994]) ).
cnf(t72292,plain,
one = join(join(complement(X1),meet(X2,X1)),complement(X2)),
inference(step,[status(thm)],[t12657,t95]) ).
cnf(t72293,plain,
one = join(complement(X2),join(complement(X1),meet(X2,X1))),
inference(step,[status(thm)],[t72292,t63]) ).
cnf(t72294,plain,
one = join(complement(X1),join(meet(X2,X1),complement(X2))),
inference(step,[status(thm)],[t72293,t68]) ).
cnf(t72295,plain,
one = join(complement(X1),join(complement(X2),meet(X2,X1))),
inference(step,[status(thm)],[t72294,t63]) ).
cnf(t72296,plain,
one = join(complement(X1),join(complement(X2),meet(X1,X2))),
inference(step,[status(thm)],[t72295,t23]) ).
cnf(t12746,plain,
join(complement(X1),join(complement(X2),meet(X1,X2))) = one,
inference(orient,[status(thm)],[t72296]) ).
cnf(t3352,plain,
meet(X1,join(meet(X2,complement(meet(X1,X2))),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t397,t3329]) ).
cnf(t71957,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t3352,t63]) ).
cnf(t71958,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t71957,t95]) ).
cnf(t71959,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = zero,
inference(step,[status(thm)],[t71958,t58]) ).
cnf(t3548,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t71959]) ).
cnf(t2714,plain,
zero = ifeq(complement(X1),one,X1,zero),
inference(cp,[status(thm)],[t138,t2710]) ).
cnf(t2785,plain,
ifeq(complement(X1),one,X1,zero) = zero,
inference(orient,[status(thm)],[t2714]) ).
cnf(t12519,plain,
one = join(complement(meet(X1,complement(X2))),complement(meet(X2,X3))),
inference(cp,[status(thm)],[t12517,t9149]) ).
cnf(t72307,plain,
one = join(complement(meet(X2,X3)),complement(meet(X1,complement(X2)))),
inference(step,[status(thm)],[t12519,t63]) ).
cnf(t13040,plain,
join(complement(meet(X1,X2)),complement(meet(X3,complement(X1)))) = one,
inference(orient,[status(thm)],[t72307]) ).
cnf(t13053,plain,
one = join(complement(meet(join(X1,X2),X3)),complement(complement(join(X1,X2)))),
inference(cp,[status(thm)],[t13040,t9760]) ).
cnf(t72346,plain,
one = join(complement(meet(join(X1,X2),X3)),join(X1,X2)),
inference(step,[status(thm)],[t13053,t2710]) ).
cnf(t72347,plain,
one = join(X2,join(complement(meet(join(X1,X2),X3)),X1)),
inference(step,[status(thm)],[t72346,t68]) ).
cnf(t72348,plain,
one = join(X1,join(X2,complement(meet(join(X1,X2),X3)))),
inference(step,[status(thm)],[t72347,t68]) ).
cnf(t72349,plain,
one = join(X1,join(X2,complement(meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t72348,t23]) ).
cnf(t14367,plain,
join(X1,join(X2,complement(meet(X3,join(X1,X2))))) = one,
inference(orient,[status(thm)],[t72349]) ).
cnf(t18135,plain,
meet(X1,X2) = meet(meet(X1,X2),complement(meet(X3,complement(X1)))),
inference(cp,[status(thm)],[t18118,t9149]) ).
cnf(t18401,plain,
meet(meet(X1,X2),complement(meet(X3,complement(X1)))) = meet(X1,X2),
inference(orient,[status(thm)],[t18135]) ).
cnf(t18433,plain,
complement(meet(meet(X1,X2),complement(meet(X3,complement(X1))))) = join(complement(complement(meet(X3,complement(X1)))),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t9299,t18401]) ).
cnf(t72502,plain,
complement(meet(X1,X2)) = join(complement(complement(meet(X3,complement(X1)))),complement(meet(X1,X2))),
inference(step,[status(thm)],[t18433,t18401]) ).
cnf(t72503,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(complement(meet(X3,complement(X1))))),
inference(step,[status(thm)],[t72502,t63]) ).
cnf(t72504,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),meet(X3,complement(X1))),
inference(step,[status(thm)],[t72503,t2710]) ).
cnf(t72505,plain,
complement(meet(X1,X2)) = join(meet(X3,complement(X1)),complement(meet(X1,X2))),
inference(step,[status(thm)],[t72504,t63]) ).
cnf(t21274,plain,
join(meet(X1,complement(X2)),complement(meet(X2,X3))) = complement(meet(X2,X3)),
inference(orient,[status(thm)],[t72505]) ).
cnf(t21388,plain,
one = join(X1,complement(meet(X2,join(X1,meet(X3,complement(X2)))))),
inference(cp,[status(thm)],[t14367,t21274]) ).
cnf(t24830,plain,
join(X1,complement(meet(X2,join(X1,meet(X3,complement(X2)))))) = one,
inference(orient,[status(thm)],[t21388]) ).
cnf(t8949,plain,
complement(complement(X1)) = meet(X1,complement(meet(complement(X1),X2))),
inference(cp,[status(thm)],[t8948,t2710]) ).
cnf(t72198,plain,
X1 = meet(X1,complement(meet(complement(X1),X2))),
inference(step,[status(thm)],[t8949,t2710]) ).
cnf(t72199,plain,
X1 = meet(X1,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t72198,t23]) ).
cnf(t9017,plain,
meet(X1,complement(meet(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t72199]) ).
cnf(t24832,plain,
one = join(X1,complement(meet(meet(X2,complement(X3)),join(X1,X3)))),
inference(cp,[status(thm)],[t24830,t9017]) ).
cnf(t72624,plain,
one = join(X1,complement(meet(join(X1,X3),meet(X2,complement(X3))))),
inference(step,[status(thm)],[t24832,t23]) ).
cnf(t72625,plain,
one = join(X1,complement(meet(complement(X3),meet(join(X1,X3),X2)))),
inference(step,[status(thm)],[t72624,t26]) ).
cnf(t72626,plain,
one = join(X1,complement(meet(X2,meet(complement(X3),join(X1,X3))))),
inference(step,[status(thm)],[t72625,t26]) ).
cnf(t26669,plain,
join(X1,complement(meet(X2,meet(complement(X3),join(X1,X3))))) = one,
inference(orient,[status(thm)],[t72626]) ).
cnf(t26671,plain,
one = complement(meet(X1,meet(complement(X2),join(complement(X1),X2)))),
inference(cp,[status(thm)],[t26669,t8887]) ).
cnf(t72627,plain,
one = complement(meet(X1,meet(complement(X2),join(X2,complement(X1))))),
inference(step,[status(thm)],[t26671,t63]) ).
cnf(t26816,plain,
complement(meet(X1,meet(complement(X2),join(X2,complement(X1))))) = one,
inference(orient,[status(thm)],[t72627]) ).
cnf(t26855,plain,
zero = ifeq(one,one,meet(X1,meet(complement(X2),join(X2,complement(X1)))),zero),
inference(cp,[status(thm)],[t2785,t26816]) ).
cnf(t72628,plain,
zero = meet(X1,meet(complement(X2),join(X2,complement(X1)))),
inference(step,[status(thm)],[t26855,t17]) ).
cnf(t26950,plain,
meet(X1,meet(complement(X2),join(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t72628]) ).
cnf(t14369,plain,
one = join(X1,complement(meet(X2,join(X1,complement(X2))))),
inference(cp,[status(thm)],[t14367,t8887]) ).
cnf(t14445,plain,
join(X1,complement(meet(X2,join(X1,complement(X2))))) = one,
inference(orient,[status(thm)],[t14369]) ).
cnf(t14447,plain,
one = join(X1,complement(meet(complement(X2),join(X1,X2)))),
inference(cp,[status(thm)],[t14445,t2710]) ).
cnf(t14954,plain,
join(X1,complement(meet(complement(X2),join(X1,X2)))) = one,
inference(orient,[status(thm)],[t14447]) ).
cnf(t26960,plain,
zero = meet(meet(complement(X1),join(X2,X1)),meet(complement(X2),one)),
inference(cp,[status(thm)],[t26950,t14954]) ).
cnf(t72630,plain,
zero = meet(meet(complement(X1),join(X2,X1)),complement(X2)),
inference(step,[status(thm)],[t26960,t101]) ).
cnf(t72631,plain,
zero = meet(complement(X2),meet(complement(X1),join(X2,X1))),
inference(step,[status(thm)],[t72630,t23]) ).
cnf(t72632,plain,
zero = meet(complement(X1),meet(join(X2,X1),complement(X2))),
inference(step,[status(thm)],[t72631,t26]) ).
cnf(t72633,plain,
zero = meet(complement(X1),meet(complement(X2),join(X2,X1))),
inference(step,[status(thm)],[t72632,t23]) ).
cnf(t72634,plain,
zero = meet(complement(X1),meet(complement(X2),join(X1,X2))),
inference(step,[status(thm)],[t72633,t63]) ).
cnf(t27104,plain,
meet(complement(X1),meet(complement(X2),join(X1,X2))) = zero,
inference(orient,[status(thm)],[t72634]) ).
cnf(t27218,plain,
zero = meet(complement(X1),join(complement(complement(X1)),meet(meet(complement(X2),join(X1,X2)),complement(zero)))),
inference(cp,[status(thm)],[t3548,t27104]) ).
cnf(t72668,plain,
zero = meet(complement(X1),join(X1,meet(meet(complement(X2),join(X1,X2)),complement(zero)))),
inference(step,[status(thm)],[t27218,t2710]) ).
cnf(t72669,plain,
zero = meet(complement(X1),join(X1,meet(complement(zero),meet(complement(X2),join(X1,X2))))),
inference(step,[status(thm)],[t72668,t23]) ).
cnf(t72670,plain,
zero = meet(complement(X1),join(X1,meet(complement(X2),meet(join(X1,X2),complement(zero))))),
inference(step,[status(thm)],[t72669,t26]) ).
cnf(t72671,plain,
zero = meet(complement(X1),join(X1,meet(complement(X2),meet(complement(zero),join(X1,X2))))),
inference(step,[status(thm)],[t72670,t23]) ).
cnf(t72672,plain,
zero = meet(complement(X1),join(X1,meet(complement(X2),meet(one,join(X1,X2))))),
inference(step,[status(thm)],[t72671,t145]) ).
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(t72008,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(t4365,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)],[t72008]) ).
cnf(t4469,plain,
meet(X1,X2) = ifeq(meet(X1,zero),zero,ifeq(join(complement(X2),meet(X1,X2)),one,complement(complement(X2)),meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t4365,t58]) ).
cnf(t72154,plain,
meet(X1,X2) = ifeq(zero,zero,ifeq(join(complement(X2),meet(X1,X2)),one,complement(complement(X2)),meet(X1,X2)),meet(X1,X2)),
inference(step,[status(thm)],[t4469,t116]) ).
cnf(t72155,plain,
meet(X1,X2) = ifeq(join(complement(X2),meet(X1,X2)),one,complement(complement(X2)),meet(X1,X2)),
inference(step,[status(thm)],[t72154,t17]) ).
cnf(t72156,plain,
meet(X1,X2) = ifeq(join(complement(X2),meet(X1,X2)),one,X2,meet(X1,X2)),
inference(step,[status(thm)],[t72155,t2710]) ).
cnf(t8001,plain,
ifeq(join(complement(X1),meet(X2,X1)),one,X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t72156]) ).
cnf(t3070,plain,
zero = meet(X1,complement(join(X2,meet(one,join(X1,X3))))),
inference(cp,[status(thm)],[t3053,t101]) ).
cnf(t3122,plain,
meet(X1,complement(join(X2,meet(one,join(X1,X3))))) = zero,
inference(orient,[status(thm)],[t3070]) ).
cnf(t9491,plain,
complement(join(X1,meet(one,join(complement(X1),X2)))) = zero,
inference(cp,[status(thm)],[t9490,t3122]) ).
cnf(t72229,plain,
complement(join(X1,meet(one,join(X2,complement(X1))))) = zero,
inference(step,[status(thm)],[t9491,t63]) ).
cnf(t9834,plain,
complement(join(X1,meet(one,join(X2,complement(X1))))) = zero,
inference(orient,[status(thm)],[t72229]) ).
cnf(t9840,plain,
one = ifeq(zero,zero,join(X1,meet(one,join(X2,complement(X1)))),one),
inference(cp,[status(thm)],[t2784,t9834]) ).
cnf(t72230,plain,
one = join(X1,meet(one,join(X2,complement(X1)))),
inference(step,[status(thm)],[t9840,t17]) ).
cnf(t9867,plain,
join(X1,meet(one,join(X2,complement(X1)))) = one,
inference(orient,[status(thm)],[t72230]) ).
cnf(t9871,plain,
one = join(complement(X1),meet(one,join(X2,X1))),
inference(cp,[status(thm)],[t9867,t2710]) ).
cnf(t72231,plain,
one = join(complement(X1),meet(one,join(X1,X2))),
inference(step,[status(thm)],[t9871,t63]) ).
cnf(t9894,plain,
join(complement(X1),meet(one,join(X1,X2))) = one,
inference(orient,[status(thm)],[t72231]) ).
cnf(t17117,plain,
join(X1,X2) = join(join(X1,X2),complement(join(X3,complement(X1)))),
inference(cp,[status(thm)],[t17111,t9435]) ).
cnf(t17215,plain,
join(join(X1,X2),complement(join(X3,complement(X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t17117]) ).
cnf(t17243,plain,
one = join(complement(join(X1,X2)),meet(one,join(X1,X2))),
inference(cp,[status(thm)],[t9894,t17215]) ).
cnf(t17324,plain,
join(complement(join(X1,X2)),meet(one,join(X1,X2))) = one,
inference(orient,[status(thm)],[t17243]) ).
cnf(t17354,plain,
meet(one,join(X1,X2)) = ifeq(one,one,join(X1,X2),meet(one,join(X1,X2))),
inference(cp,[status(thm)],[t8001,t17324]) ).
cnf(t72438,plain,
meet(one,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t17354,t17]) ).
cnf(t17392,plain,
meet(one,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t72438]) ).
cnf(t72673,plain,
zero = meet(complement(X1),join(X1,meet(complement(X2),join(X1,X2)))),
inference(step,[status(thm)],[t72672,t17392]) ).
cnf(t28460,plain,
meet(complement(X1),join(X1,meet(complement(X2),join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t72673]) ).
cnf(t28580,plain,
one = join(complement(complement(X1)),join(complement(join(X1,meet(complement(X2),join(X1,X2)))),zero)),
inference(cp,[status(thm)],[t12746,t28460]) ).
cnf(t72691,plain,
one = join(zero,join(complement(complement(X1)),complement(join(X1,meet(complement(X2),join(X1,X2)))))),
inference(step,[status(thm)],[t28580,t68]) ).
cnf(t72692,plain,
one = join(zero,join(X1,complement(join(X1,meet(complement(X2),join(X1,X2)))))),
inference(step,[status(thm)],[t72691,t2710]) ).
cnf(t72693,plain,
one = join(X1,join(complement(join(X1,meet(complement(X2),join(X1,X2)))),zero)),
inference(step,[status(thm)],[t72692,t68]) ).
cnf(t72694,plain,
one = join(X1,complement(join(X1,meet(complement(X2),join(X1,X2))))),
inference(step,[status(thm)],[t72693,t95]) ).
cnf(t30506,plain,
join(X1,complement(join(X1,meet(complement(X2),join(X1,X2))))) = one,
inference(orient,[status(thm)],[t72694]) ).
cnf(t30629,plain,
X1 = ifeq(meet(X1,complement(join(X1,meet(complement(X2),join(X1,X2))))),zero,ifeq(one,one,complement(complement(join(X1,meet(complement(X2),join(X1,X2))))),X1),X1),
inference(cp,[status(thm)],[t2596,t30506]) ).
cnf(t1534,plain,
zero = meet(complement(join(X1,X2)),X1),
inference(cp,[status(thm)],[t150,t1520]) ).
cnf(t71798,plain,
zero = meet(X1,complement(join(X1,X2))),
inference(step,[status(thm)],[t1534,t23]) ).
cnf(t1550,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(orient,[status(thm)],[t71798]) ).
cnf(t72695,plain,
X1 = ifeq(zero,zero,ifeq(one,one,complement(complement(join(X1,meet(complement(X2),join(X1,X2))))),X1),X1),
inference(step,[status(thm)],[t30629,t1550]) ).
cnf(t72696,plain,
X1 = ifeq(one,one,complement(complement(join(X1,meet(complement(X2),join(X1,X2))))),X1),
inference(step,[status(thm)],[t72695,t17]) ).
cnf(t72697,plain,
X1 = complement(complement(join(X1,meet(complement(X2),join(X1,X2))))),
inference(step,[status(thm)],[t72696,t17]) ).
cnf(t72698,plain,
X1 = join(X1,meet(complement(X2),join(X1,X2))),
inference(step,[status(thm)],[t72697,t2710]) ).
cnf(t30679,plain,
join(X1,meet(complement(X2),join(X1,X2))) = X1,
inference(orient,[status(thm)],[t72698]) ).
cnf(t30797,plain,
meet(complement(X1),join(X2,X1)) = meet(meet(complement(X1),join(X2,X1)),X2),
inference(cp,[status(thm)],[t18514,t30679]) ).
cnf(t72850,plain,
meet(complement(X1),join(X1,X2)) = meet(meet(complement(X1),join(X2,X1)),X2),
inference(step,[status(thm)],[t30797,t63]) ).
cnf(t72851,plain,
meet(complement(X1),join(X1,X2)) = meet(X2,meet(complement(X1),join(X2,X1))),
inference(step,[status(thm)],[t72850,t23]) ).
cnf(t72852,plain,
meet(complement(X1),join(X1,X2)) = meet(X2,complement(X1)),
inference(step,[status(thm)],[t72851,t165]) ).
cnf(t44121,plain,
meet(complement(X1),join(X1,X2)) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t72852]) ).
cnf(t44143,plain,
meet(X1,complement(complement(X2))) = meet(X2,join(complement(X2),X1)),
inference(cp,[status(thm)],[t44121,t2710]) ).
cnf(t72858,plain,
meet(X1,X2) = meet(X2,join(complement(X2),X1)),
inference(step,[status(thm)],[t44143,t2710]) ).
cnf(t72859,plain,
meet(X1,X2) = meet(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t72858,t63]) ).
cnf(t44482,plain,
meet(X1,join(X2,complement(X1))) = meet(X2,X1),
inference(orient,[status(thm)],[t72859]) ).
cnf(t12800,plain,
one = join(complement(X1),join(complement(meet(X2,complement(meet(X1,X2)))),zero)),
inference(cp,[status(thm)],[t12746,t3329]) ).
cnf(t72329,plain,
one = join(complement(X1),complement(meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t12800,t95]) ).
cnf(t13671,plain,
join(complement(X1),complement(meet(X2,complement(meet(X1,X2))))) = one,
inference(orient,[status(thm)],[t72329]) ).
cnf(t13672,plain,
one = join(X1,complement(meet(X2,complement(meet(complement(X1),X2))))),
inference(cp,[status(thm)],[t13671,t2710]) ).
cnf(t72362,plain,
one = join(X1,complement(meet(X2,complement(meet(X2,complement(X1)))))),
inference(step,[status(thm)],[t13672,t23]) ).
cnf(t15366,plain,
join(X1,complement(meet(X2,complement(meet(X2,complement(X1)))))) = one,
inference(orient,[status(thm)],[t72362]) ).
cnf(t44503,plain,
meet(X1,meet(X2,complement(meet(X2,complement(X1))))) = meet(meet(X2,complement(meet(X2,complement(X1)))),one),
inference(cp,[status(thm)],[t44482,t15366]) ).
cnf(t9089,plain,
meet(X1,meet(complement(meet(X2,complement(X1))),X3)) = meet(X3,X1),
inference(cp,[status(thm)],[t26,t9017]) ).
cnf(t72233,plain,
meet(X1,meet(X3,complement(meet(X2,complement(X1))))) = meet(X3,X1),
inference(step,[status(thm)],[t9089,t23]) ).
cnf(t72234,plain,
meet(X1,meet(X3,complement(meet(X2,complement(X1))))) = meet(X1,X3),
inference(step,[status(thm)],[t72233,t23]) ).
cnf(t10058,plain,
meet(X1,meet(X2,complement(meet(X3,complement(X1))))) = meet(X1,X2),
inference(orient,[status(thm)],[t72234]) ).
cnf(t72876,plain,
meet(X1,X2) = meet(meet(X2,complement(meet(X2,complement(X1)))),one),
inference(step,[status(thm)],[t44503,t10058]) ).
cnf(t72877,plain,
meet(X1,X2) = meet(X2,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t72876,t101]) ).
cnf(t45213,plain,
meet(X1,complement(meet(X1,complement(X2)))) = meet(X2,X1),
inference(orient,[status(thm)],[t72877]) ).
cnf(t45278,plain,
meet(complement(X1),X2) = meet(X2,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t45213,t2710]) ).
cnf(t72887,plain,
meet(X2,complement(X1)) = meet(X2,complement(meet(X2,X1))),
inference(step,[status(thm)],[t45278,t23]) ).
cnf(t72888,plain,
meet(X2,complement(X1)) = meet(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t72887,t23]) ).
cnf(t45998,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t72888]) ).
cnf(t46129,plain,
meet(X1,complement(X2)) = meet(X1,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t45998,t23]) ).
cnf(t46274,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t46129]) ).
cnf(t46279,plain,
meet(X1,complement(join(X2,complement(X1)))) = meet(X1,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t46274,t44482]) ).
cnf(t72891,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(meet(X2,X1))),
inference(step,[status(thm)],[t46279,t9610]) ).
cnf(t72892,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t72891,t45998]) ).
cnf(t46522,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t72892]) ).
cnf(t46566,plain,
join(X1,complement(X2)) = complement(meet(X2,complement(X1))),
inference(cp,[status(thm)],[t2710,t46522]) ).
cnf(t47054,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t46566]) ).
cnf(t47055,plain,
join(meet(X1,X2),complement(X1)) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t47054,t46274]) ).
cnf(t72933,plain,
join(complement(X1),meet(X1,X2)) = complement(meet(X1,complement(X2))),
inference(step,[status(thm)],[t47055,t63]) ).
cnf(t72934,plain,
join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
inference(step,[status(thm)],[t72933,t47054]) ).
cnf(t47465,plain,
join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t72934]) ).
cnf(t47474,plain,
join(X1,complement(complement(X2))) = join(X2,meet(complement(X2),X1)),
inference(cp,[status(thm)],[t47465,t2710]) ).
cnf(t72943,plain,
join(X1,X2) = join(X2,meet(complement(X2),X1)),
inference(step,[status(thm)],[t47474,t2710]) ).
cnf(t72944,plain,
join(X1,X2) = join(X2,meet(X1,complement(X2))),
inference(step,[status(thm)],[t72943,t23]) ).
cnf(t47758,plain,
join(X1,meet(X2,complement(X1))) = join(X2,X1),
inference(orient,[status(thm)],[t72944]) ).
cnf(t44294,plain,
meet(X1,complement(X2)) = meet(complement(X2),join(X1,X2)),
inference(cp,[status(thm)],[t44121,t63]) ).
cnf(t44723,plain,
meet(complement(X1),join(X2,X1)) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t44294]) ).
cnf(t46355,plain,
meet(complement(X1),complement(join(X2,X1))) = meet(complement(X1),complement(meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t46274,t44723]) ).
cnf(t72911,plain,
complement(join(X2,X1)) = meet(complement(X1),complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t46355,t9760]) ).
cnf(t72912,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t72911,t63]) ).
cnf(t72913,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(X2)),
inference(step,[status(thm)],[t72912,t45998]) ).
cnf(t46840,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t72913]) ).
cnf(t47794,plain,
join(complement(X1),X2) = join(X2,complement(join(X1,X2))),
inference(cp,[status(thm)],[t47758,t46840]) ).
cnf(t72949,plain,
join(X2,complement(X1)) = join(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t47794,t63]) ).
cnf(t48177,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t72949]) ).
cnf(t48227,plain,
join(meet(X1,join(X2,X3)),complement(complement(meet(X1,X2)))) = join(meet(X1,join(X2,X3)),complement(one)),
inference(cp,[status(thm)],[t48177,t13548]) ).
cnf(t73220,plain,
join(meet(X1,join(X2,X3)),meet(X1,X2)) = join(meet(X1,join(X2,X3)),complement(one)),
inference(step,[status(thm)],[t48227,t2710]) ).
cnf(t73221,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = join(meet(X1,join(X2,X3)),complement(one)),
inference(step,[status(thm)],[t73220,t63]) ).
cnf(t73222,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = join(complement(one),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t73221,t63]) ).
cnf(t73223,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = join(zero,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t73222,t140]) ).
cnf(t73224,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t73223,t1286]) ).
cnf(t70931,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t73224]) ).
cnf(t70964,plain,
meet(X1,join(meet(X1,X2),X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t70931,t106]) ).
cnf(t73225,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t70964,t63]) ).
cnf(t47093,plain,
join(join(X1,complement(X2)),complement(X3)) = complement(meet(X3,meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t47054,t46522]) ).
cnf(t73014,plain,
join(complement(X3),join(X1,complement(X2))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t47093,t63]) ).
cnf(t73015,plain,
join(complement(X2),join(complement(X3),X1)) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t73014,t68]) ).
cnf(t73016,plain,
join(X1,join(complement(X2),complement(X3))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t73015,t68]) ).
cnf(t47094,plain,
join(complement(X1),complement(X2)) = complement(meet(X2,X1)),
inference(cp,[status(thm)],[t47054,t2710]) ).
cnf(t72929,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t47094,t23]) ).
cnf(t47307,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t72929]) ).
cnf(t73017,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t73016,t47307]) ).
cnf(t73018,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X2,meet(complement(X1),X3))),
inference(step,[status(thm)],[t73017,t26]) ).
cnf(t73019,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X2,meet(X3,complement(X1)))),
inference(step,[status(thm)],[t73018,t23]) ).
cnf(t52256,plain,
complement(meet(X1,meet(X2,complement(X3)))) = join(X3,complement(meet(X1,X2))),
inference(orient,[status(thm)],[t73019]) ).
cnf(t52337,plain,
meet(X1,complement(meet(X2,complement(X3)))) = meet(X1,join(X3,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t46274,t52256]) ).
cnf(t73173,plain,
meet(X1,join(X3,complement(X2))) = meet(X1,join(X3,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t52337,t47054]) ).
cnf(t66467,plain,
meet(X1,join(X2,complement(meet(X1,X3)))) = meet(X1,join(X2,complement(X3))),
inference(orient,[status(thm)],[t73173]) ).
cnf(t66493,plain,
meet(X1,join(X2,complement(complement(meet(X1,X3))))) = meet(X1,join(X2,complement(meet(X1,complement(X3))))),
inference(cp,[status(thm)],[t66467,t46274]) ).
cnf(t73176,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,complement(meet(X1,complement(X3))))),
inference(step,[status(thm)],[t66493,t2710]) ).
cnf(t73177,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,complement(complement(X3)))),
inference(step,[status(thm)],[t73176,t66467]) ).
cnf(t73178,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t73177,t2710]) ).
cnf(t66691,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t73178]) ).
cnf(t73226,plain,
meet(X1,join(X3,X2)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t73225,t66691]) ).
cnf(t73227,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t73226,t63]) ).
cnf(t48241,plain,
join(X1,complement(X2)) = join(X1,complement(join(X1,X2))),
inference(cp,[status(thm)],[t48177,t63]) ).
cnf(t48326,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t48241]) ).
cnf(t46857,plain,
complement(join(join(X1,complement(X2)),X3)) = meet(meet(X2,complement(X1)),complement(X3)),
inference(cp,[status(thm)],[t46840,t46522]) ).
cnf(t73006,plain,
complement(join(X3,join(X1,complement(X2)))) = meet(meet(X2,complement(X1)),complement(X3)),
inference(step,[status(thm)],[t46857,t63]) ).
cnf(t73007,plain,
complement(join(X1,join(complement(X2),X3))) = meet(meet(X2,complement(X1)),complement(X3)),
inference(step,[status(thm)],[t73006,t68]) ).
cnf(t73008,plain,
complement(join(X1,join(X3,complement(X2)))) = meet(meet(X2,complement(X1)),complement(X3)),
inference(step,[status(thm)],[t73007,t63]) ).
cnf(t73009,plain,
complement(join(X1,join(X3,complement(X2)))) = meet(complement(X3),meet(X2,complement(X1))),
inference(step,[status(thm)],[t73008,t23]) ).
cnf(t73010,plain,
complement(join(X1,join(X3,complement(X2)))) = meet(complement(X1),meet(complement(X3),X2)),
inference(step,[status(thm)],[t73009,t26]) ).
cnf(t73011,plain,
complement(join(X1,join(X3,complement(X2)))) = meet(X2,meet(complement(X1),complement(X3))),
inference(step,[status(thm)],[t73010,t26]) ).
cnf(t73012,plain,
complement(join(X1,join(X3,complement(X2)))) = meet(X2,complement(join(X1,X3))),
inference(step,[status(thm)],[t73011,t46840]) ).
cnf(t52077,plain,
complement(join(X1,join(X2,complement(X3)))) = meet(X3,complement(join(X1,X2))),
inference(orient,[status(thm)],[t73012]) ).
cnf(t52143,plain,
join(X1,complement(join(X2,complement(X3)))) = join(X1,meet(X3,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t48326,t52077]) ).
cnf(t73166,plain,
join(X1,meet(X3,complement(X2))) = join(X1,meet(X3,complement(join(X1,X2)))),
inference(step,[status(thm)],[t52143,t46522]) ).
cnf(t65721,plain,
join(X1,meet(X2,complement(join(X1,X3)))) = join(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t73166]) ).
cnf(t65752,plain,
join(X1,meet(X2,complement(complement(join(X1,X3))))) = join(X1,meet(X2,complement(join(X1,complement(X3))))),
inference(cp,[status(thm)],[t65721,t48326]) ).
cnf(t73167,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,complement(join(X1,complement(X3))))),
inference(step,[status(thm)],[t65752,t2710]) ).
cnf(t73168,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,complement(complement(X3)))),
inference(step,[status(thm)],[t73167,t65721]) ).
cnf(t73169,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t73168,t2710]) ).
cnf(t65912,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t73169]) ).
cnf(t73228,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,X3)),
inference(step,[status(thm)],[t73227,t65912]) ).
cnf(t71199,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t73228]) ).
cnf(f12,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/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,t71199]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT197-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/10.63 % Computer : n019.cluster.edu
% 0.16/10.63 % Model : x86_64 x86_64
% 0.16/10.63 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/10.63 % Memory : 8046.5625MB
% 0.16/10.63 % OS : Linux 6.8.0-71-generic
% 0.16/10.63 % CPULimit : 300
% 0.16/10.63 % WCLimit : 300
% 0.16/10.63 % DateTime : Wed Sep 23 20:31:49 UTC 2026
% 0.16/10.64 % CPUTime :
% 0.16/10.64 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 32.12/15.16 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.12/15.16 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------