%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT198-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:55:54 PM UTC 2026
% Result : Unsatisfiable 38.37s 5.33s
% Output : Proof 38.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 206
% Number of leaves : 14
% Syntax : Number of formulae : 670 ( 666 unt; 0 def)
% Number of atoms : 678 ( 677 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 : 9 ( 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 : 1536 ( 367 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f10,axiom,
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f10_nnf,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( complement(X0) = X1
| join(X0,X1) != one
| meet(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t11,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t18,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(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(t23,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t25,plain,
X1 = ifeq(meet(X2,X1),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(cp,[status(thm)],[t18,t23]) ).
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(t51,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t50354,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(step,[status(thm)],[t25,t51]) ).
cnf(t2529,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t50354]) ).
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(t91,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t2597,plain,
X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t2529,t91]) ).
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(t50355,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t2597,t17]) ).
cnf(f8,axiom,
join(X,complement(X)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_join) ).
fof(f8_nnf,plain,
! [X] : join(X,complement(X)) = one,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] : join(X,complement(X)) = one,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
join(X0,complement(X0)) = one,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t2,plain,
join(X1,complement(X1)) = one,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t46,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t50356,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t50355,t46]) ).
cnf(t50357,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t50356,t17]) ).
cnf(t2642,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t50357]) ).
cnf(f11,axiom,
meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,meet(Z,join(Y,join(U,meet(X,Z)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H42) ).
fof(f11_nnf,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,meet(Z,join(Y,join(U,meet(X,Z)))))),
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(Y,join(U,meet(X,Z)))))),
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(X1,join(X3,meet(X0,X2)))))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t12,plain,
meet(X1,join(X2,meet(X3,join(X2,join(X4,meet(X1,X3)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t54,plain,
meet(X1,join(X2,meet(X3,join(X2,join(X4,meet(X1,X3)))))) = 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/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(t50076,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t10,t51]) ).
cnf(t67,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t50076]) ).
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(t14,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t59,plain,
meet(X1,join(X2,meet(X3,join(X1,X1)))) = meet(X1,join(X2,meet(X3,join(X2,X1)))),
inference(cp,[status(thm)],[t54,t14]) ).
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(t13,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t50128,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,meet(X3,join(X2,X1)))),
inference(step,[status(thm)],[t59,t13]) ).
cnf(t50129,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,join(X2,X1)))),
inference(step,[status(thm)],[t50128,t51]) ).
cnf(t50130,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t50129,t23]) ).
cnf(t274,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t50130]) ).
cnf(t287,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),meet(X2,one))),
inference(cp,[status(thm)],[t274,t46]) ).
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(t16,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t47,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t16,t46]) ).
cnf(t96,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t47]) ).
cnf(t50137,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t287,t96]) ).
cnf(t50138,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(X2,complement(X1))),
inference(step,[status(thm)],[t50137,t23]) ).
cnf(t345,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(X2,complement(X1))),
inference(orient,[status(thm)],[t50138]) ).
cnf(t71,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t67,t16]) ).
cnf(t50094,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t71,t67]) ).
cnf(t50095,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t50094,t51]) ).
cnf(t50096,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t50095,t51]) ).
cnf(t179,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t50096]) ).
cnf(t358,plain,
meet(X1,join(meet(X2,join(X1,X3)),complement(X1))) = meet(X1,join(complement(X1),meet(X1,X2))),
inference(cp,[status(thm)],[t345,t179]) ).
cnf(t50234,plain,
meet(X1,join(complement(X1),meet(X2,join(X1,X3)))) = meet(X1,join(complement(X1),meet(X1,X2))),
inference(step,[status(thm)],[t358,t23]) ).
cnf(t50235,plain,
meet(X1,join(complement(X1),meet(X2,join(X1,X3)))) = meet(X1,join(X2,complement(X1))),
inference(step,[status(thm)],[t50234,t345]) ).
cnf(t828,plain,
meet(X1,join(complement(X1),meet(X2,join(X1,X3)))) = meet(X1,join(X2,complement(X1))),
inference(orient,[status(thm)],[t50235]) ).
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(t50075,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t9,t23]) ).
cnf(t26,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t50075]) ).
cnf(t29,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t26,t13]) ).
cnf(t50077,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t29,t26]) ).
cnf(t50078,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t50077,t23]) ).
cnf(t107,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t50078]) ).
cnf(t110,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t107,t46]) ).
cnf(t50079,plain,
one = join(X1,one),
inference(step,[status(thm)],[t110,t46]) ).
cnf(t118,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t50079]) ).
cnf(t282,plain,
meet(X1,join(one,meet(X1,X2))) = meet(X1,join(one,meet(X2,one))),
inference(cp,[status(thm)],[t274,t118]) ).
cnf(t50131,plain,
meet(X1,join(one,meet(X1,X2))) = meet(X1,join(one,X2)),
inference(step,[status(thm)],[t282,t96]) ).
cnf(t50132,plain,
meet(X1,join(one,meet(X1,X2))) = meet(X1,join(X2,one)),
inference(step,[status(thm)],[t50131,t23]) ).
cnf(t50133,plain,
meet(X1,join(one,meet(X1,X2))) = meet(X1,one),
inference(step,[status(thm)],[t50132,t118]) ).
cnf(t50134,plain,
meet(X1,join(one,meet(X1,X2))) = X1,
inference(step,[status(thm)],[t50133,t96]) ).
cnf(t314,plain,
meet(X1,join(one,meet(X1,X2))) = X1,
inference(orient,[status(thm)],[t50134]) ).
cnf(t94,plain,
meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
inference(cp,[status(thm)],[t67,t91]) ).
cnf(t50089,plain,
meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
inference(step,[status(thm)],[t94,t51]) ).
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(t15,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t70,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t67,t15]) ).
cnf(t50080,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t70,t67]) ).
cnf(t50081,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t50080,t51]) ).
cnf(t123,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t50081]) ).
cnf(t126,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t123,t91]) ).
cnf(t50082,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t126,t91]) ).
cnf(t134,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t50082]) ).
cnf(t50090,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t50089,t134]) ).
cnf(t159,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t50090]) ).
cnf(t165,plain,
meet(X1,meet(meet(X2,complement(X1)),X3)) = meet(X3,zero),
inference(cp,[status(thm)],[t67,t159]) ).
cnf(t50101,plain,
meet(X1,meet(X3,meet(X2,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t165,t51]) ).
cnf(t50102,plain,
meet(X1,meet(X2,meet(complement(X1),X3))) = meet(X3,zero),
inference(step,[status(thm)],[t50101,t67]) ).
cnf(t50103,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t50102,t51]) ).
cnf(t50104,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(step,[status(thm)],[t50103,t134]) ).
cnf(t202,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t50104]) ).
cnf(t353,plain,
meet(X1,join(meet(X2,meet(X3,complement(X1))),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t345,t202]) ).
cnf(t50160,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t353,t23]) ).
cnf(t92,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t14,t91]) ).
cnf(t102,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t92]) ).
cnf(t50161,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t50160,t102]) ).
cnf(t50162,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = zero,
inference(step,[status(thm)],[t50161,t91]) ).
cnf(t472,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = zero,
inference(orient,[status(thm)],[t50162]) ).
cnf(t357,plain,
meet(X1,join(meet(X2,complement(X1)),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t345,t159]) ).
cnf(t50152,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t357,t23]) ).
cnf(t50153,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t50152,t102]) ).
cnf(t50154,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = zero,
inference(step,[status(thm)],[t50153,t91]) ).
cnf(t419,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t50154]) ).
cnf(t835,plain,
meet(complement(X1),join(X1,complement(complement(X1)))) = meet(complement(X1),join(complement(complement(X1)),zero)),
inference(cp,[status(thm)],[t828,t419]) ).
cnf(t50236,plain,
meet(complement(X1),join(X1,complement(complement(X1)))) = meet(complement(X1),complement(complement(X1))),
inference(step,[status(thm)],[t835,t102]) ).
cnf(t50237,plain,
meet(complement(X1),join(X1,complement(complement(X1)))) = zero,
inference(step,[status(thm)],[t50236,t91]) ).
cnf(t868,plain,
meet(complement(X1),join(X1,complement(complement(X1)))) = zero,
inference(orient,[status(thm)],[t50237]) ).
cnf(t869,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,t868]) ).
cnf(t50238,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)],[t869,t17]) ).
cnf(t49,plain,
join(X1,join(complement(X1),X2)) = join(X2,one),
inference(cp,[status(thm)],[t26,t46]) ).
cnf(t50087,plain,
join(X1,join(X2,complement(X1))) = join(X2,one),
inference(step,[status(thm)],[t49,t23]) ).
cnf(t50088,plain,
join(X1,join(X2,complement(X1))) = one,
inference(step,[status(thm)],[t50087,t118]) ).
cnf(t152,plain,
join(X1,join(X2,complement(X1))) = one,
inference(orient,[status(thm)],[t50088]) ).
cnf(t50239,plain,
join(X1,complement(complement(X1))) = ifeq(one,one,complement(complement(X1)),join(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t50238,t152]) ).
cnf(t50240,plain,
join(X1,complement(complement(X1))) = complement(complement(X1)),
inference(step,[status(thm)],[t50239,t17]) ).
cnf(t876,plain,
join(X1,complement(complement(X1))) = complement(complement(X1)),
inference(orient,[status(thm)],[t50240]) ).
cnf(t877,plain,
X1 = meet(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t16,t876]) ).
cnf(t891,plain,
meet(X1,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t877]) ).
cnf(t912,plain,
zero = meet(complement(X1),join(complement(complement(X1)),meet(X2,X1))),
inference(cp,[status(thm)],[t472,t891]) ).
cnf(t50242,plain,
zero = meet(complement(X1),join(meet(X2,X1),complement(complement(X1)))),
inference(step,[status(thm)],[t912,t23]) ).
cnf(t50243,plain,
zero = meet(complement(X1),join(meet(X1,X2),complement(complement(X1)))),
inference(step,[status(thm)],[t50242,t51]) ).
cnf(t990,plain,
meet(complement(X1),join(meet(X1,X2),complement(complement(X1)))) = zero,
inference(orient,[status(thm)],[t50243]) ).
cnf(t997,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,t990]) ).
cnf(t50244,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)],[t997,t17]) ).
cnf(t50245,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)],[t50244,t152]) ).
cnf(t50246,plain,
join(meet(X1,X2),complement(complement(X1))) = complement(complement(X1)),
inference(step,[status(thm)],[t50245,t17]) ).
cnf(t1008,plain,
join(meet(X1,X2),complement(complement(X1))) = complement(complement(X1)),
inference(orient,[status(thm)],[t50246]) ).
cnf(t1014,plain,
meet(X1,X2) = meet(meet(X1,X2),complement(complement(X1))),
inference(cp,[status(thm)],[t16,t1008]) ).
cnf(t1029,plain,
meet(meet(X1,X2),complement(complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t1014]) ).
cnf(t1038,plain,
meet(X1,X2) = meet(meet(X1,X2),join(one,meet(X1,X2))),
inference(cp,[status(thm)],[t314,t1029]) ).
cnf(t1115,plain,
meet(meet(X1,X2),join(one,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t1038]) ).
cnf(t1136,plain,
meet(one,join(meet(X1,X2),complement(one))) = meet(one,join(complement(one),meet(X1,X2))),
inference(cp,[status(thm)],[t828,t1115]) ).
cnf(t136,plain,
zero = ifeq(zero,zero,ifeq(join(X1,zero),one,complement(X1),zero),zero),
inference(cp,[status(thm)],[t18,t134]) ).
cnf(t50085,plain,
zero = ifeq(join(X1,zero),one,complement(X1),zero),
inference(step,[status(thm)],[t136,t17]) ).
cnf(t50086,plain,
zero = ifeq(X1,one,complement(X1),zero),
inference(step,[status(thm)],[t50085,t102]) ).
cnf(t144,plain,
ifeq(X1,one,complement(X1),zero) = zero,
inference(orient,[status(thm)],[t50086]) ).
cnf(t145,plain,
zero = complement(one),
inference(cp,[status(thm)],[t144,t17]) ).
cnf(t147,plain,
complement(one) = zero,
inference(orient,[status(thm)],[t145]) ).
cnf(t50249,plain,
meet(one,join(meet(X1,X2),zero)) = meet(one,join(complement(one),meet(X1,X2))),
inference(step,[status(thm)],[t1136,t147]) ).
cnf(t50250,plain,
meet(one,meet(X1,X2)) = meet(one,join(complement(one),meet(X1,X2))),
inference(step,[status(thm)],[t50249,t102]) ).
cnf(t50251,plain,
meet(one,meet(X1,X2)) = meet(one,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t50250,t147]) ).
cnf(t50252,plain,
meet(X2,meet(one,X1)) = meet(one,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t50251,t67]) ).
cnf(t50253,plain,
meet(X1,meet(X2,one)) = meet(one,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t50252,t67]) ).
cnf(t50254,plain,
meet(X1,X2) = meet(one,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t50253,t96]) ).
cnf(t1147,plain,
meet(one,join(zero,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t50254]) ).
cnf(t1177,plain,
meet(join(zero,meet(X1,X2)),meet(X3,one)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t67,t1147]) ).
cnf(t50255,plain,
meet(join(zero,meet(X1,X2)),X3) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t1177,t96]) ).
cnf(t50256,plain,
meet(X3,join(zero,meet(X1,X2))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t50255,t51]) ).
cnf(t50257,plain,
meet(X3,join(zero,meet(X1,X2))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t50256,t67]) ).
cnf(t50258,plain,
meet(X3,join(zero,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t50257,t67]) ).
cnf(t1192,plain,
meet(X1,join(zero,meet(X2,X3))) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t50258]) ).
cnf(t1196,plain,
meet(X1,meet(X2,join(zero,meet(X1,X2)))) = join(zero,meet(X1,X2)),
inference(cp,[status(thm)],[t1192,t15]) ).
cnf(t50265,plain,
meet(X1,meet(X1,meet(X2,X2))) = join(zero,meet(X1,X2)),
inference(step,[status(thm)],[t1196,t1192]) ).
cnf(t50266,plain,
meet(X1,meet(X2,X2)) = join(zero,meet(X1,X2)),
inference(step,[status(thm)],[t50265,t123]) ).
cnf(t50267,plain,
meet(X1,X2) = join(zero,meet(X1,X2)),
inference(step,[status(thm)],[t50266,t15]) ).
cnf(t1264,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t50267]) ).
cnf(t1283,plain,
meet(X1,join(zero,meet(X2,join(X1,X3)))) = meet(X1,meet(X2,join(zero,join(X3,meet(X1,X2))))),
inference(cp,[status(thm)],[t54,t1264]) ).
cnf(t50416,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(X2,join(zero,join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t1283,t1264]) ).
cnf(t50417,plain,
meet(X1,X2) = meet(X1,meet(X2,join(zero,join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t50416,t179]) ).
cnf(t50418,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,join(meet(X1,X2),zero)))),
inference(step,[status(thm)],[t50417,t26]) ).
cnf(t50419,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t50418,t102]) ).
cnf(t2929,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t50419]) ).
cnf(t2970,plain,
meet(X1,meet(X1,X2)) = meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t2929,t123]) ).
cnf(t50420,plain,
meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t2970,t123]) ).
cnf(t3010,plain,
meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t50420]) ).
cnf(t33,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,t26]) ).
cnf(t50496,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)],[t33,t26]) ).
cnf(t4364,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)],[t50496]) ).
cnf(t211,plain,
meet(X1,meet(meet(X2,meet(X3,complement(X1))),X4)) = meet(X4,zero),
inference(cp,[status(thm)],[t67,t202]) ).
cnf(t50112,plain,
meet(X1,meet(X4,meet(X2,meet(X3,complement(X1))))) = meet(X4,zero),
inference(step,[status(thm)],[t211,t51]) ).
cnf(t50113,plain,
meet(X1,meet(X2,meet(meet(X3,complement(X1)),X4))) = meet(X4,zero),
inference(step,[status(thm)],[t50112,t67]) ).
cnf(t50114,plain,
meet(X1,meet(X2,meet(X4,meet(X3,complement(X1))))) = meet(X4,zero),
inference(step,[status(thm)],[t50113,t51]) ).
cnf(t50115,plain,
meet(X1,meet(X2,meet(X3,meet(complement(X1),X4)))) = meet(X4,zero),
inference(step,[status(thm)],[t50114,t67]) ).
cnf(t50116,plain,
meet(X1,meet(X2,meet(X3,meet(X4,complement(X1))))) = meet(X4,zero),
inference(step,[status(thm)],[t50115,t51]) ).
cnf(t50117,plain,
meet(X1,meet(X2,meet(X3,meet(X4,complement(X1))))) = zero,
inference(step,[status(thm)],[t50116,t134]) ).
cnf(t227,plain,
meet(X1,meet(X2,meet(X3,meet(X4,complement(X1))))) = zero,
inference(orient,[status(thm)],[t50117]) ).
cnf(t889,plain,
join(X1,join(complement(complement(X1)),X2)) = join(X2,complement(complement(X1))),
inference(cp,[status(thm)],[t26,t876]) ).
cnf(t50241,plain,
join(X1,join(X2,complement(complement(X1)))) = join(X2,complement(complement(X1))),
inference(step,[status(thm)],[t889,t23]) ).
cnf(t936,plain,
join(X1,join(X2,complement(complement(X1)))) = join(X2,complement(complement(X1))),
inference(orient,[status(thm)],[t50241]) ).
cnf(t940,plain,
X1 = meet(X1,join(X2,complement(complement(X1)))),
inference(cp,[status(thm)],[t16,t936]) ).
cnf(t955,plain,
meet(X1,join(X2,complement(complement(X1)))) = X1,
inference(orient,[status(thm)],[t940]) ).
cnf(t971,plain,
meet(X1,join(complement(complement(X2)),meet(X1,X2))) = meet(X1,join(complement(complement(X2)),X2)),
inference(cp,[status(thm)],[t274,t955]) ).
cnf(t50276,plain,
meet(X1,join(meet(X1,X2),complement(complement(X2)))) = meet(X1,join(complement(complement(X2)),X2)),
inference(step,[status(thm)],[t971,t23]) ).
cnf(t50277,plain,
meet(X1,join(meet(X1,X2),complement(complement(X2)))) = meet(X1,join(X2,complement(complement(X2)))),
inference(step,[status(thm)],[t50276,t23]) ).
cnf(t50278,plain,
meet(X1,join(meet(X1,X2),complement(complement(X2)))) = meet(X1,complement(complement(X2))),
inference(step,[status(thm)],[t50277,t876]) ).
cnf(t1360,plain,
meet(X1,join(meet(X1,X2),complement(complement(X2)))) = meet(X1,complement(complement(X2))),
inference(orient,[status(thm)],[t50278]) ).
cnf(t1380,plain,
meet(X1,complement(complement(join(X1,X2)))) = meet(X1,join(X1,complement(complement(join(X1,X2))))),
inference(cp,[status(thm)],[t1360,t16]) ).
cnf(t50281,plain,
meet(X1,complement(complement(join(X1,X2)))) = X1,
inference(step,[status(thm)],[t1380,t16]) ).
cnf(t1434,plain,
meet(X1,complement(complement(join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t50281]) ).
cnf(t1459,plain,
zero = meet(complement(join(X1,X2)),meet(X3,meet(X4,X1))),
inference(cp,[status(thm)],[t227,t1434]) ).
cnf(t50310,plain,
zero = meet(meet(X4,X1),meet(complement(join(X1,X2)),X3)),
inference(step,[status(thm)],[t1459,t67]) ).
cnf(t50311,plain,
zero = meet(X3,meet(meet(X4,X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t50310,t67]) ).
cnf(t50312,plain,
zero = meet(X3,meet(meet(X1,X4),complement(join(X1,X2)))),
inference(step,[status(thm)],[t50311,t51]) ).
cnf(t1836,plain,
meet(X1,meet(meet(X2,X3),complement(join(X2,X4)))) = zero,
inference(orient,[status(thm)],[t50312]) ).
cnf(t1837,plain,
zero = meet(meet(X1,X2),complement(join(X1,X3))),
inference(cp,[status(thm)],[t1836,t123]) ).
cnf(t1864,plain,
meet(meet(X1,X2),complement(join(X1,X3))) = zero,
inference(orient,[status(thm)],[t1837]) ).
cnf(t1866,plain,
zero = meet(meet(X1,X2),complement(join(X2,X3))),
inference(cp,[status(thm)],[t1864,t51]) ).
cnf(t1887,plain,
meet(meet(X1,X2),complement(join(X2,X3))) = zero,
inference(orient,[status(thm)],[t1866]) ).
cnf(t1911,plain,
zero = meet(meet(X1,X2),complement(join(meet(X2,join(X1,X3)),X4))),
inference(cp,[status(thm)],[t1887,t179]) ).
cnf(t50424,plain,
zero = meet(meet(X1,X2),complement(join(X4,meet(X2,join(X1,X3))))),
inference(step,[status(thm)],[t1911,t23]) ).
cnf(t3060,plain,
meet(meet(X1,X2),complement(join(X3,meet(X2,join(X1,X4))))) = zero,
inference(orient,[status(thm)],[t50424]) ).
cnf(t3077,plain,
zero = meet(X1,complement(join(X2,meet(one,join(X1,X3))))),
inference(cp,[status(thm)],[t3060,t96]) ).
cnf(t3129,plain,
meet(X1,complement(join(X2,meet(one,join(X1,X3))))) = zero,
inference(orient,[status(thm)],[t3077]) ).
cnf(t3130,plain,
zero = meet(X1,complement(meet(one,join(X1,X2)))),
inference(cp,[status(thm)],[t3129,t13]) ).
cnf(t3150,plain,
meet(X1,complement(meet(one,join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t3130]) ).
cnf(t3160,plain,
meet(X1,join(complement(meet(one,join(X1,X2))),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t345,t3150]) ).
cnf(t50443,plain,
meet(X1,join(complement(X1),complement(meet(one,join(X1,X2))))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t3160,t23]) ).
cnf(t50444,plain,
meet(X1,join(complement(X1),complement(meet(one,join(X1,X2))))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t50443,t102]) ).
cnf(t50445,plain,
meet(X1,join(complement(X1),complement(meet(one,join(X1,X2))))) = zero,
inference(step,[status(thm)],[t50444,t91]) ).
cnf(t3506,plain,
meet(X1,join(complement(X1),complement(meet(one,join(X1,X2))))) = zero,
inference(orient,[status(thm)],[t50445]) ).
cnf(t1448,plain,
zero = meet(complement(join(X1,X2)),X1),
inference(cp,[status(thm)],[t159,t1434]) ).
cnf(t50282,plain,
zero = meet(X1,complement(join(X1,X2))),
inference(step,[status(thm)],[t1448,t51]) ).
cnf(t1464,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(orient,[status(thm)],[t50282]) ).
cnf(t1472,plain,
meet(X1,join(complement(join(X1,X2)),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t345,t1464]) ).
cnf(t50293,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t1472,t23]) ).
cnf(t50294,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t50293,t102]) ).
cnf(t50295,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = zero,
inference(step,[status(thm)],[t50294,t91]) ).
cnf(t1723,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t50295]) ).
cnf(t2663,plain,
zero = meet(complement(X1),join(X1,complement(join(complement(X1),X2)))),
inference(cp,[status(thm)],[t1723,t2642]) ).
cnf(t50402,plain,
zero = meet(complement(X1),join(X1,complement(join(X2,complement(X1))))),
inference(step,[status(thm)],[t2663,t23]) ).
cnf(t2721,plain,
meet(complement(X1),join(X1,complement(join(X2,complement(X1))))) = zero,
inference(orient,[status(thm)],[t50402]) ).
cnf(t4387,plain,
join(X1,complement(join(X2,complement(X1)))) = ifeq(zero,zero,ifeq(join(X1,join(complement(join(X2,complement(X1))),complement(X1))),one,complement(complement(X1)),join(X1,complement(join(X2,complement(X1))))),join(X1,complement(join(X2,complement(X1))))),
inference(cp,[status(thm)],[t4364,t2721]) ).
cnf(t50497,plain,
join(X1,complement(join(X2,complement(X1)))) = ifeq(join(X1,join(complement(join(X2,complement(X1))),complement(X1))),one,complement(complement(X1)),join(X1,complement(join(X2,complement(X1))))),
inference(step,[status(thm)],[t4387,t17]) ).
cnf(t50498,plain,
join(X1,complement(join(X2,complement(X1)))) = ifeq(one,one,complement(complement(X1)),join(X1,complement(join(X2,complement(X1))))),
inference(step,[status(thm)],[t50497,t152]) ).
cnf(t50499,plain,
join(X1,complement(join(X2,complement(X1)))) = complement(complement(X1)),
inference(step,[status(thm)],[t50498,t17]) ).
cnf(t50500,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(step,[status(thm)],[t50499,t2642]) ).
cnf(t4473,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t50500]) ).
cnf(t4475,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t4473,t2642]) ).
cnf(t50503,plain,
complement(X1) = join(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t4475,t23]) ).
cnf(t4521,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t50503]) ).
cnf(t4552,plain,
zero = meet(complement(X1),join(complement(complement(X1)),complement(meet(one,complement(X1))))),
inference(cp,[status(thm)],[t3506,t4521]) ).
cnf(t50516,plain,
zero = meet(complement(X1),join(X1,complement(meet(one,complement(X1))))),
inference(step,[status(thm)],[t4552,t2642]) ).
cnf(t4736,plain,
meet(complement(X1),join(X1,complement(meet(one,complement(X1))))) = zero,
inference(orient,[status(thm)],[t50516]) ).
cnf(t4744,plain,
join(X1,complement(meet(one,complement(X1)))) = ifeq(zero,zero,ifeq(join(X1,join(complement(meet(one,complement(X1))),complement(X1))),one,complement(complement(X1)),join(X1,complement(meet(one,complement(X1))))),join(X1,complement(meet(one,complement(X1))))),
inference(cp,[status(thm)],[t4364,t4736]) ).
cnf(t50517,plain,
join(X1,complement(meet(one,complement(X1)))) = ifeq(join(X1,join(complement(meet(one,complement(X1))),complement(X1))),one,complement(complement(X1)),join(X1,complement(meet(one,complement(X1))))),
inference(step,[status(thm)],[t4744,t17]) ).
cnf(t50518,plain,
join(X1,complement(meet(one,complement(X1)))) = ifeq(one,one,complement(complement(X1)),join(X1,complement(meet(one,complement(X1))))),
inference(step,[status(thm)],[t50517,t152]) ).
cnf(t50519,plain,
join(X1,complement(meet(one,complement(X1)))) = complement(complement(X1)),
inference(step,[status(thm)],[t50518,t17]) ).
cnf(t50520,plain,
join(X1,complement(meet(one,complement(X1)))) = X1,
inference(step,[status(thm)],[t50519,t2642]) ).
cnf(t4759,plain,
join(X1,complement(meet(one,complement(X1)))) = X1,
inference(orient,[status(thm)],[t50520]) ).
cnf(t4769,plain,
one = join(meet(one,complement(X1)),X1),
inference(cp,[status(thm)],[t152,t4759]) ).
cnf(t50522,plain,
one = join(X1,meet(one,complement(X1))),
inference(step,[status(thm)],[t4769,t23]) ).
cnf(t4795,plain,
join(X1,meet(one,complement(X1))) = one,
inference(orient,[status(thm)],[t50522]) ).
cnf(t4799,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,t4795]) ).
cnf(t50523,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)],[t4799,t159]) ).
cnf(t50524,plain,
meet(one,complement(X1)) = ifeq(one,one,complement(X1),meet(one,complement(X1))),
inference(step,[status(thm)],[t50523,t17]) ).
cnf(t50525,plain,
meet(one,complement(X1)) = complement(X1),
inference(step,[status(thm)],[t50524,t17]) ).
cnf(t4816,plain,
meet(one,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t50525]) ).
cnf(t4830,plain,
meet(one,complement(X1)) = meet(one,meet(meet(one,complement(X1)),join(X2,complement(X1)))),
inference(cp,[status(thm)],[t3010,t4816]) ).
cnf(t50529,plain,
complement(X1) = meet(one,meet(meet(one,complement(X1)),join(X2,complement(X1)))),
inference(step,[status(thm)],[t4830,t4816]) ).
cnf(t50530,plain,
complement(X1) = meet(one,meet(complement(X1),join(X2,complement(X1)))),
inference(step,[status(thm)],[t50529,t4816]) ).
cnf(t4862,plain,
meet(one,meet(complement(X1),join(X2,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t50530]) ).
cnf(t4895,plain,
meet(meet(complement(X1),join(X2,complement(X1))),meet(X3,one)) = meet(X3,complement(X1)),
inference(cp,[status(thm)],[t67,t4862]) ).
cnf(t50561,plain,
meet(meet(complement(X1),join(X2,complement(X1))),X3) = meet(X3,complement(X1)),
inference(step,[status(thm)],[t4895,t96]) ).
cnf(t50562,plain,
meet(X3,meet(complement(X1),join(X2,complement(X1)))) = meet(X3,complement(X1)),
inference(step,[status(thm)],[t50561,t51]) ).
cnf(t5786,plain,
meet(X1,meet(complement(X2),join(X3,complement(X2)))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t50562]) ).
cnf(t5787,plain,
meet(complement(X1),complement(X1)) = meet(complement(X1),join(X2,complement(X1))),
inference(cp,[status(thm)],[t5786,t123]) ).
cnf(t50563,plain,
complement(X1) = meet(complement(X1),join(X2,complement(X1))),
inference(step,[status(thm)],[t5787,t15]) ).
cnf(t5817,plain,
meet(complement(X1),join(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t50563]) ).
cnf(t5819,plain,
complement(join(X1,complement(X2))) = meet(complement(join(X1,complement(X2))),X2),
inference(cp,[status(thm)],[t5817,t4473]) ).
cnf(t50565,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t5819,t51]) ).
cnf(t5898,plain,
meet(X1,complement(join(X2,complement(X1)))) = complement(join(X2,complement(X1))),
inference(orient,[status(thm)],[t50565]) ).
cnf(t5903,plain,
complement(join(X1,complement(complement(X2)))) = meet(complement(X2),complement(join(X1,X2))),
inference(cp,[status(thm)],[t5898,t2642]) ).
cnf(t50566,plain,
complement(join(X1,X2)) = meet(complement(X2),complement(join(X1,X2))),
inference(step,[status(thm)],[t5903,t2642]) ).
cnf(t5933,plain,
meet(complement(X1),complement(join(X2,X1))) = complement(join(X2,X1)),
inference(orient,[status(thm)],[t50566]) ).
cnf(t1455,plain,
zero = meet(complement(join(X1,X2)),meet(X3,X1)),
inference(cp,[status(thm)],[t202,t1434]) ).
cnf(t50287,plain,
zero = meet(X1,meet(complement(join(X1,X2)),X3)),
inference(step,[status(thm)],[t1455,t67]) ).
cnf(t50288,plain,
zero = meet(X1,meet(X3,complement(join(X1,X2)))),
inference(step,[status(thm)],[t50287,t51]) ).
cnf(t1521,plain,
meet(X1,meet(X2,complement(join(X1,X3)))) = zero,
inference(orient,[status(thm)],[t50288]) ).
cnf(t1533,plain,
meet(X1,join(meet(X2,complement(join(X1,X3))),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t345,t1521]) ).
cnf(t50341,plain,
meet(X1,join(complement(X1),meet(X2,complement(join(X1,X3))))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t1533,t23]) ).
cnf(t50342,plain,
meet(X1,join(complement(X1),meet(X2,complement(join(X1,X3))))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t50341,t102]) ).
cnf(t50343,plain,
meet(X1,join(complement(X1),meet(X2,complement(join(X1,X3))))) = zero,
inference(step,[status(thm)],[t50342,t91]) ).
cnf(t2429,plain,
meet(X1,join(complement(X1),meet(X2,complement(join(X1,X3))))) = zero,
inference(orient,[status(thm)],[t50343]) ).
cnf(t2673,plain,
zero = meet(complement(X1),join(X1,meet(X2,complement(join(complement(X1),X3))))),
inference(cp,[status(thm)],[t2429,t2642]) ).
cnf(t50495,plain,
zero = meet(complement(X1),join(X1,meet(X2,complement(join(X3,complement(X1)))))),
inference(step,[status(thm)],[t2673,t23]) ).
cnf(t4324,plain,
meet(complement(X1),join(X1,meet(X2,complement(join(X3,complement(X1)))))) = zero,
inference(orient,[status(thm)],[t50495]) ).
cnf(t4389,plain,
join(X1,meet(X2,complement(join(X3,complement(X1))))) = ifeq(zero,zero,ifeq(join(X1,join(meet(X2,complement(join(X3,complement(X1)))),complement(X1))),one,complement(complement(X1)),join(X1,meet(X2,complement(join(X3,complement(X1)))))),join(X1,meet(X2,complement(join(X3,complement(X1)))))),
inference(cp,[status(thm)],[t4364,t4324]) ).
cnf(t50506,plain,
join(X1,meet(X2,complement(join(X3,complement(X1))))) = ifeq(join(X1,join(meet(X2,complement(join(X3,complement(X1)))),complement(X1))),one,complement(complement(X1)),join(X1,meet(X2,complement(join(X3,complement(X1)))))),
inference(step,[status(thm)],[t4389,t17]) ).
cnf(t50507,plain,
join(X1,meet(X2,complement(join(X3,complement(X1))))) = ifeq(one,one,complement(complement(X1)),join(X1,meet(X2,complement(join(X3,complement(X1)))))),
inference(step,[status(thm)],[t50506,t152]) ).
cnf(t50508,plain,
join(X1,meet(X2,complement(join(X3,complement(X1))))) = complement(complement(X1)),
inference(step,[status(thm)],[t50507,t17]) ).
cnf(t50509,plain,
join(X1,meet(X2,complement(join(X3,complement(X1))))) = X1,
inference(step,[status(thm)],[t50508,t2642]) ).
cnf(t4586,plain,
join(X1,meet(X2,complement(join(X3,complement(X1))))) = X1,
inference(orient,[status(thm)],[t50509]) ).
cnf(t4593,plain,
complement(X1) = join(complement(X1),meet(X2,complement(join(X3,X1)))),
inference(cp,[status(thm)],[t4586,t2642]) ).
cnf(t50513,plain,
complement(X1) = join(complement(X1),meet(X2,complement(join(X1,X3)))),
inference(step,[status(thm)],[t4593,t23]) ).
cnf(t4631,plain,
join(complement(X1),meet(X2,complement(join(X1,X3)))) = complement(X1),
inference(orient,[status(thm)],[t50513]) ).
cnf(t5942,plain,
complement(join(complement(X1),meet(X2,complement(join(X1,X3))))) = meet(complement(meet(X2,complement(join(X1,X3)))),complement(complement(X1))),
inference(cp,[status(thm)],[t5933,t4631]) ).
cnf(t50577,plain,
complement(complement(X1)) = meet(complement(meet(X2,complement(join(X1,X3)))),complement(complement(X1))),
inference(step,[status(thm)],[t5942,t4631]) ).
cnf(t50578,plain,
X1 = meet(complement(meet(X2,complement(join(X1,X3)))),complement(complement(X1))),
inference(step,[status(thm)],[t50577,t2642]) ).
cnf(t50579,plain,
X1 = meet(complement(complement(X1)),complement(meet(X2,complement(join(X1,X3))))),
inference(step,[status(thm)],[t50578,t51]) ).
cnf(t50580,plain,
X1 = meet(X1,complement(meet(X2,complement(join(X1,X3))))),
inference(step,[status(thm)],[t50579,t2642]) ).
cnf(t6252,plain,
meet(X1,complement(meet(X2,complement(join(X1,X3))))) = X1,
inference(orient,[status(thm)],[t50580]) ).
cnf(t4635,plain,
complement(X1) = join(complement(X1),meet(X2,complement(X1))),
inference(cp,[status(thm)],[t4631,t13]) ).
cnf(t4678,plain,
join(complement(X1),meet(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t4635]) ).
cnf(t5943,plain,
complement(join(complement(X1),meet(X2,complement(X1)))) = meet(complement(meet(X2,complement(X1))),complement(complement(X1))),
inference(cp,[status(thm)],[t5933,t4678]) ).
cnf(t50567,plain,
complement(complement(X1)) = meet(complement(meet(X2,complement(X1))),complement(complement(X1))),
inference(step,[status(thm)],[t5943,t4678]) ).
cnf(t50568,plain,
X1 = meet(complement(meet(X2,complement(X1))),complement(complement(X1))),
inference(step,[status(thm)],[t50567,t2642]) ).
cnf(t50569,plain,
X1 = meet(complement(complement(X1)),complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t50568,t51]) ).
cnf(t50570,plain,
X1 = meet(X1,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t50569,t2642]) ).
cnf(t5983,plain,
meet(X1,complement(meet(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t50570]) ).
cnf(t5993,plain,
complement(meet(X1,complement(X2))) = join(complement(meet(X1,complement(X2))),X2),
inference(cp,[status(thm)],[t4678,t5983]) ).
cnf(t50574,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(meet(X1,complement(X2)))),
inference(step,[status(thm)],[t5993,t23]) ).
cnf(t6116,plain,
join(X1,complement(meet(X2,complement(X1)))) = complement(meet(X2,complement(X1))),
inference(orient,[status(thm)],[t50574]) ).
cnf(t6255,plain,
X1 = meet(X1,complement(meet(X2,complement(complement(meet(X3,complement(X1))))))),
inference(cp,[status(thm)],[t6252,t6116]) ).
cnf(t50584,plain,
X1 = meet(X1,complement(meet(X2,meet(X3,complement(X1))))),
inference(step,[status(thm)],[t6255,t2642]) ).
cnf(t6518,plain,
meet(X1,complement(meet(X2,meet(X3,complement(X1))))) = X1,
inference(orient,[status(thm)],[t50584]) ).
cnf(t5939,plain,
complement(join(X1,meet(X1,X2))) = meet(complement(meet(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t5933,t14]) ).
cnf(t50571,plain,
complement(X1) = meet(complement(meet(X1,X2)),complement(X1)),
inference(step,[status(thm)],[t5939,t14]) ).
cnf(t50572,plain,
complement(X1) = meet(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t50571,t51]) ).
cnf(t6024,plain,
meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t50572]) ).
cnf(t6524,plain,
meet(X1,X2) = meet(meet(X1,X2),complement(meet(X3,complement(X1)))),
inference(cp,[status(thm)],[t6518,t6024]) ).
cnf(t6797,plain,
meet(meet(X1,X2),complement(meet(X3,complement(X1)))) = meet(X1,X2),
inference(orient,[status(thm)],[t6524]) ).
cnf(t6841,plain,
meet(meet(X1,X2),complement(meet(X3,complement(X1)))) = meet(meet(X1,X2),meet(meet(X1,X2),join(X4,meet(meet(X1,X2),complement(meet(X3,complement(X1))))))),
inference(cp,[status(thm)],[t3010,t6797]) ).
cnf(t50591,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(X4,meet(meet(X1,X2),complement(meet(X3,complement(X1))))))),
inference(step,[status(thm)],[t6841,t6797]) ).
cnf(t50592,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(meet(X1,X2),complement(meet(X3,complement(X1)))))),
inference(step,[status(thm)],[t50591,t123]) ).
cnf(t50593,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(X1,X2))),
inference(step,[status(thm)],[t50592,t6797]) ).
cnf(t6861,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t50593]) ).
cnf(t3086,plain,
zero = meet(meet(X1,X2),complement(meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t3060,t13]) ).
cnf(t3167,plain,
meet(meet(X1,X2),complement(meet(X2,join(X1,X3)))) = zero,
inference(orient,[status(thm)],[t3086]) ).
cnf(t275,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(cp,[status(thm)],[t274,t14]) ).
cnf(t297,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t275]) ).
cnf(t299,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t297,t179]) ).
cnf(t50183,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(step,[status(thm)],[t299,t179]) ).
cnf(t50184,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t50183,t23]) ).
cnf(t550,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t50184]) ).
cnf(t3191,plain,
zero = meet(meet(meet(X1,X2),X1),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t3167,t550]) ).
cnf(t50429,plain,
zero = meet(complement(meet(X1,X2)),meet(meet(X1,X2),X1)),
inference(step,[status(thm)],[t3191,t51]) ).
cnf(t50430,plain,
zero = meet(X1,meet(complement(meet(X1,X2)),meet(X1,X2))),
inference(step,[status(thm)],[t50429,t67]) ).
cnf(t50431,plain,
zero = meet(X1,meet(X2,meet(complement(meet(X1,X2)),X1))),
inference(step,[status(thm)],[t50430,t67]) ).
cnf(t50432,plain,
zero = meet(X1,meet(X1,meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t50431,t67]) ).
cnf(t50433,plain,
zero = meet(X1,meet(X2,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t50432,t123]) ).
cnf(t3341,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t50433]) ).
cnf(t3363,plain,
meet(X1,join(meet(X2,complement(meet(X1,X2))),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t345,t3341]) ).
cnf(t50448,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t3363,t23]) ).
cnf(t50449,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t50448,t102]) ).
cnf(t50450,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = zero,
inference(step,[status(thm)],[t50449,t91]) ).
cnf(t3562,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t50450]) ).
cnf(t2645,plain,
zero = ifeq(complement(X1),one,X1,zero),
inference(cp,[status(thm)],[t144,t2642]) ).
cnf(t2717,plain,
ifeq(complement(X1),one,X1,zero) = zero,
inference(orient,[status(thm)],[t2645]) ).
cnf(t120,plain,
one = ifeq(meet(X1,one),zero,ifeq(one,one,complement(X1),one),one),
inference(cp,[status(thm)],[t18,t118]) ).
cnf(t50083,plain,
one = ifeq(X1,zero,ifeq(one,one,complement(X1),one),one),
inference(step,[status(thm)],[t120,t96]) ).
cnf(t50084,plain,
one = ifeq(X1,zero,complement(X1),one),
inference(step,[status(thm)],[t50083,t17]) ).
cnf(t140,plain,
ifeq(X1,zero,complement(X1),one) = one,
inference(orient,[status(thm)],[t50084]) ).
cnf(t2646,plain,
one = ifeq(complement(X1),zero,X1,one),
inference(cp,[status(thm)],[t140,t2642]) ).
cnf(t2718,plain,
ifeq(complement(X1),zero,X1,one) = one,
inference(orient,[status(thm)],[t2646]) ).
cnf(t4865,plain,
complement(join(X1,X2)) = meet(one,meet(complement(join(X1,X2)),complement(X1))),
inference(cp,[status(thm)],[t4862,t4521]) ).
cnf(t50531,plain,
complement(join(X1,X2)) = meet(one,meet(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t4865,t51]) ).
cnf(t4896,plain,
meet(one,meet(complement(X1),complement(join(X1,X2)))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t50531]) ).
cnf(t4899,plain,
complement(join(X1,meet(one,join(complement(X1),X2)))) = meet(one,zero),
inference(cp,[status(thm)],[t4896,t3129]) ).
cnf(t50532,plain,
complement(join(X1,meet(one,join(X2,complement(X1))))) = meet(one,zero),
inference(step,[status(thm)],[t4899,t23]) ).
cnf(t50533,plain,
complement(join(X1,meet(one,join(X2,complement(X1))))) = zero,
inference(step,[status(thm)],[t50532,t134]) ).
cnf(t4938,plain,
complement(join(X1,meet(one,join(X2,complement(X1))))) = zero,
inference(orient,[status(thm)],[t50533]) ).
cnf(t4943,plain,
one = ifeq(zero,zero,join(X1,meet(one,join(X2,complement(X1)))),one),
inference(cp,[status(thm)],[t2718,t4938]) ).
cnf(t50534,plain,
one = join(X1,meet(one,join(X2,complement(X1)))),
inference(step,[status(thm)],[t4943,t17]) ).
cnf(t4966,plain,
join(X1,meet(one,join(X2,complement(X1)))) = one,
inference(orient,[status(thm)],[t50534]) ).
cnf(t4970,plain,
one = join(complement(X1),meet(one,join(X2,X1))),
inference(cp,[status(thm)],[t4966,t2642]) ).
cnf(t50535,plain,
one = join(complement(X1),meet(one,join(X1,X2))),
inference(step,[status(thm)],[t4970,t23]) ).
cnf(t4988,plain,
join(complement(X1),meet(one,join(X1,X2))) = one,
inference(orient,[status(thm)],[t50535]) ).
cnf(t6125,plain,
one = join(complement(X1),meet(one,complement(meet(X2,complement(X1))))),
inference(cp,[status(thm)],[t4988,t6116]) ).
cnf(t50575,plain,
one = join(complement(X1),complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t6125,t4816]) ).
cnf(t6159,plain,
join(complement(X1),complement(meet(X2,complement(X1)))) = one,
inference(orient,[status(thm)],[t50575]) ).
cnf(t6832,plain,
one = join(complement(meet(X1,complement(X2))),complement(meet(X2,X3))),
inference(cp,[status(thm)],[t6159,t6797]) ).
cnf(t50599,plain,
one = join(complement(meet(X2,X3)),complement(meet(X1,complement(X2)))),
inference(step,[status(thm)],[t6832,t23]) ).
cnf(t7183,plain,
join(complement(meet(X1,X2)),complement(meet(X3,complement(X1)))) = one,
inference(orient,[status(thm)],[t50599]) ).
cnf(t7199,plain,
one = join(complement(meet(join(X1,X2),X3)),complement(complement(join(X1,X2)))),
inference(cp,[status(thm)],[t7183,t5933]) ).
cnf(t50626,plain,
one = join(complement(meet(join(X1,X2),X3)),join(X1,X2)),
inference(step,[status(thm)],[t7199,t2642]) ).
cnf(t50627,plain,
one = join(X2,join(complement(meet(join(X1,X2),X3)),X1)),
inference(step,[status(thm)],[t50626,t26]) ).
cnf(t50628,plain,
one = join(X1,join(X2,complement(meet(join(X1,X2),X3)))),
inference(step,[status(thm)],[t50627,t26]) ).
cnf(t50629,plain,
one = join(X1,join(X2,complement(meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t50628,t51]) ).
cnf(t7642,plain,
join(X1,join(X2,complement(meet(X3,join(X1,X2))))) = one,
inference(orient,[status(thm)],[t50629]) ).
cnf(t6137,plain,
complement(X1) = join(complement(X1),meet(X2,complement(complement(meet(X3,complement(X1)))))),
inference(cp,[status(thm)],[t4631,t6116]) ).
cnf(t50585,plain,
complement(X1) = join(complement(X1),meet(X2,meet(X3,complement(X1)))),
inference(step,[status(thm)],[t6137,t2642]) ).
cnf(t6571,plain,
join(complement(X1),meet(X2,meet(X3,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t50585]) ).
cnf(t6578,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),meet(X3,complement(X1))),
inference(cp,[status(thm)],[t6571,t6024]) ).
cnf(t50698,plain,
complement(meet(X1,X2)) = join(meet(X3,complement(X1)),complement(meet(X1,X2))),
inference(step,[status(thm)],[t6578,t23]) ).
cnf(t10092,plain,
join(meet(X1,complement(X2)),complement(meet(X2,X3))) = complement(meet(X2,X3)),
inference(orient,[status(thm)],[t50698]) ).
cnf(t10180,plain,
one = join(X1,complement(meet(X2,join(X1,meet(X3,complement(X2)))))),
inference(cp,[status(thm)],[t7642,t10092]) ).
cnf(t13770,plain,
join(X1,complement(meet(X2,join(X1,meet(X3,complement(X2)))))) = one,
inference(orient,[status(thm)],[t10180]) ).
cnf(t13775,plain,
one = join(X1,complement(meet(meet(X2,complement(X3)),join(X1,X3)))),
inference(cp,[status(thm)],[t13770,t5983]) ).
cnf(t50823,plain,
one = join(X1,complement(meet(join(X1,X3),meet(X2,complement(X3))))),
inference(step,[status(thm)],[t13775,t51]) ).
cnf(t50824,plain,
one = join(X1,complement(meet(complement(X3),meet(join(X1,X3),X2)))),
inference(step,[status(thm)],[t50823,t67]) ).
cnf(t50825,plain,
one = join(X1,complement(meet(X2,meet(complement(X3),join(X1,X3))))),
inference(step,[status(thm)],[t50824,t67]) ).
cnf(t14282,plain,
join(X1,complement(meet(X2,meet(complement(X3),join(X1,X3))))) = one,
inference(orient,[status(thm)],[t50825]) ).
cnf(t6035,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t4678,t6024]) ).
cnf(t50573,plain,
complement(meet(X1,X2)) = join(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t6035,t23]) ).
cnf(t6065,plain,
join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t50573]) ).
cnf(t14284,plain,
one = complement(meet(X1,meet(complement(X2),join(complement(X1),X2)))),
inference(cp,[status(thm)],[t14282,t6065]) ).
cnf(t50826,plain,
one = complement(meet(X1,meet(complement(X2),join(X2,complement(X1))))),
inference(step,[status(thm)],[t14284,t23]) ).
cnf(t14391,plain,
complement(meet(X1,meet(complement(X2),join(X2,complement(X1))))) = one,
inference(orient,[status(thm)],[t50826]) ).
cnf(t14426,plain,
zero = ifeq(one,one,meet(X1,meet(complement(X2),join(X2,complement(X1)))),zero),
inference(cp,[status(thm)],[t2717,t14391]) ).
cnf(t50827,plain,
zero = meet(X1,meet(complement(X2),join(X2,complement(X1)))),
inference(step,[status(thm)],[t14426,t17]) ).
cnf(t14488,plain,
meet(X1,meet(complement(X2),join(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t50827]) ).
cnf(t7644,plain,
one = join(X1,complement(meet(X2,join(X1,complement(X2))))),
inference(cp,[status(thm)],[t7642,t6065]) ).
cnf(t7744,plain,
join(X1,complement(meet(X2,join(X1,complement(X2))))) = one,
inference(orient,[status(thm)],[t7644]) ).
cnf(t7746,plain,
one = join(X1,complement(meet(complement(X2),join(X1,X2)))),
inference(cp,[status(thm)],[t7744,t2642]) ).
cnf(t7787,plain,
join(X1,complement(meet(complement(X2),join(X1,X2)))) = one,
inference(orient,[status(thm)],[t7746]) ).
cnf(t14500,plain,
zero = meet(meet(complement(X1),join(X2,X1)),meet(complement(X2),one)),
inference(cp,[status(thm)],[t14488,t7787]) ).
cnf(t50829,plain,
zero = meet(meet(complement(X1),join(X2,X1)),complement(X2)),
inference(step,[status(thm)],[t14500,t96]) ).
cnf(t50830,plain,
zero = meet(complement(X2),meet(complement(X1),join(X2,X1))),
inference(step,[status(thm)],[t50829,t51]) ).
cnf(t50831,plain,
zero = meet(complement(X1),meet(join(X2,X1),complement(X2))),
inference(step,[status(thm)],[t50830,t67]) ).
cnf(t50832,plain,
zero = meet(complement(X1),meet(complement(X2),join(X2,X1))),
inference(step,[status(thm)],[t50831,t51]) ).
cnf(t50833,plain,
zero = meet(complement(X1),meet(complement(X2),join(X1,X2))),
inference(step,[status(thm)],[t50832,t23]) ).
cnf(t14589,plain,
meet(complement(X1),meet(complement(X2),join(X1,X2))) = zero,
inference(orient,[status(thm)],[t50833]) ).
cnf(t14679,plain,
zero = meet(complement(X1),join(complement(complement(X1)),meet(meet(complement(X2),join(X1,X2)),complement(zero)))),
inference(cp,[status(thm)],[t3562,t14589]) ).
cnf(t50891,plain,
zero = meet(complement(X1),join(X1,meet(meet(complement(X2),join(X1,X2)),complement(zero)))),
inference(step,[status(thm)],[t14679,t2642]) ).
cnf(t50892,plain,
zero = meet(complement(X1),join(X1,meet(complement(zero),meet(complement(X2),join(X1,X2))))),
inference(step,[status(thm)],[t50891,t51]) ).
cnf(t50893,plain,
zero = meet(complement(X1),join(X1,meet(complement(X2),meet(join(X1,X2),complement(zero))))),
inference(step,[status(thm)],[t50892,t67]) ).
cnf(t50894,plain,
zero = meet(complement(X1),join(X1,meet(complement(X2),meet(complement(zero),join(X1,X2))))),
inference(step,[status(thm)],[t50893,t51]) ).
cnf(t141,plain,
one = complement(zero),
inference(cp,[status(thm)],[t140,t17]) ).
cnf(t142,plain,
complement(zero) = one,
inference(orient,[status(thm)],[t141]) ).
cnf(t50895,plain,
zero = meet(complement(X1),join(X1,meet(complement(X2),meet(one,join(X1,X2))))),
inference(step,[status(thm)],[t50894,t142]) ).
cnf(t6120,plain,
complement(meet(X1,complement(complement(X2)))) = join(complement(X2),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t6116,t2642]) ).
cnf(t50576,plain,
complement(meet(X1,X2)) = join(complement(X2),complement(meet(X1,X2))),
inference(step,[status(thm)],[t6120,t2642]) ).
cnf(t6180,plain,
join(complement(X1),complement(meet(X2,X1))) = complement(meet(X2,X1)),
inference(orient,[status(thm)],[t50576]) ).
cnf(t6522,plain,
meet(X1,complement(X2)) = meet(meet(X1,complement(X2)),complement(meet(X3,X2))),
inference(cp,[status(thm)],[t6518,t5983]) ).
cnf(t50659,plain,
meet(X1,complement(X2)) = meet(meet(X1,complement(X2)),complement(meet(X2,X3))),
inference(step,[status(thm)],[t6522,t51]) ).
cnf(t8502,plain,
meet(meet(X1,complement(X2)),complement(meet(X2,X3))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t50659]) ).
cnf(t8521,plain,
meet(X1,complement(complement(X2))) = meet(meet(X1,complement(complement(X2))),complement(complement(join(X3,X2)))),
inference(cp,[status(thm)],[t8502,t5933]) ).
cnf(t50660,plain,
meet(X1,X2) = meet(meet(X1,complement(complement(X2))),complement(complement(join(X3,X2)))),
inference(step,[status(thm)],[t8521,t2642]) ).
cnf(t50661,plain,
meet(X1,X2) = meet(meet(X1,X2),complement(complement(join(X3,X2)))),
inference(step,[status(thm)],[t50660,t2642]) ).
cnf(t50662,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X2)),
inference(step,[status(thm)],[t50661,t2642]) ).
cnf(t50663,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t50662,t23]) ).
cnf(t8579,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t50663]) ).
cnf(t8602,plain,
meet(complement(X1),complement(meet(X1,X2))) = meet(complement(X1),join(complement(meet(X1,X2)),X3)),
inference(cp,[status(thm)],[t8579,t6024]) ).
cnf(t50668,plain,
complement(X1) = meet(complement(X1),join(complement(meet(X1,X2)),X3)),
inference(step,[status(thm)],[t8602,t6024]) ).
cnf(t50669,plain,
complement(X1) = meet(complement(X1),join(X3,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t50668,t23]) ).
cnf(t8809,plain,
meet(complement(X1),join(X2,complement(meet(X1,X3)))) = complement(X1),
inference(orient,[status(thm)],[t50669]) ).
cnf(t8829,plain,
complement(meet(complement(X1),join(X2,complement(meet(X1,X3))))) = join(complement(join(X2,complement(meet(X1,X3)))),complement(complement(X1))),
inference(cp,[status(thm)],[t6180,t8809]) ).
cnf(t50670,plain,
complement(complement(X1)) = join(complement(join(X2,complement(meet(X1,X3)))),complement(complement(X1))),
inference(step,[status(thm)],[t8829,t8809]) ).
cnf(t50671,plain,
X1 = join(complement(join(X2,complement(meet(X1,X3)))),complement(complement(X1))),
inference(step,[status(thm)],[t50670,t2642]) ).
cnf(t50672,plain,
X1 = join(complement(complement(X1)),complement(join(X2,complement(meet(X1,X3))))),
inference(step,[status(thm)],[t50671,t23]) ).
cnf(t50673,plain,
X1 = join(X1,complement(join(X2,complement(meet(X1,X3))))),
inference(step,[status(thm)],[t50672,t2642]) ).
cnf(t8866,plain,
join(X1,complement(join(X2,complement(meet(X1,X3))))) = X1,
inference(orient,[status(thm)],[t50673]) ).
cnf(t8869,plain,
X1 = join(X1,complement(join(X2,complement(complement(join(X3,complement(X1))))))),
inference(cp,[status(thm)],[t8866,t5898]) ).
cnf(t50674,plain,
X1 = join(X1,complement(join(X2,join(X3,complement(X1))))),
inference(step,[status(thm)],[t8869,t2642]) ).
cnf(t8934,plain,
join(X1,complement(join(X2,join(X3,complement(X1))))) = X1,
inference(orient,[status(thm)],[t50674]) ).
cnf(t8941,plain,
join(X1,X2) = join(join(X1,X2),complement(join(X3,complement(X1)))),
inference(cp,[status(thm)],[t8934,t4521]) ).
cnf(t9423,plain,
join(join(X1,X2),complement(join(X3,complement(X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t8941]) ).
cnf(t9480,plain,
zero = meet(join(X1,X2),complement(meet(one,join(X1,X2)))),
inference(cp,[status(thm)],[t3150,t9423]) ).
cnf(t9777,plain,
meet(join(X1,X2),complement(meet(one,join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t9480]) ).
cnf(t9822,plain,
join(X1,X2) = ifeq(zero,zero,ifeq(join(join(X1,X2),complement(meet(one,join(X1,X2)))),one,complement(complement(meet(one,join(X1,X2)))),join(X1,X2)),join(X1,X2)),
inference(cp,[status(thm)],[t2529,t9777]) ).
cnf(t50690,plain,
join(X1,X2) = ifeq(join(join(X1,X2),complement(meet(one,join(X1,X2)))),one,complement(complement(meet(one,join(X1,X2)))),join(X1,X2)),
inference(step,[status(thm)],[t9822,t17]) ).
cnf(t7189,plain,
one = join(complement(meet(X1,X2)),complement(meet(X3,complement(X2)))),
inference(cp,[status(thm)],[t7183,t51]) ).
cnf(t7479,plain,
join(complement(meet(X1,X2)),complement(meet(X3,complement(X2)))) = one,
inference(orient,[status(thm)],[t7189]) ).
cnf(t7507,plain,
one = join(complement(meet(X1,X2)),complement(complement(X2))),
inference(cp,[status(thm)],[t7479,t15]) ).
cnf(t50619,plain,
one = join(complement(complement(X2)),complement(meet(X1,X2))),
inference(step,[status(thm)],[t7507,t23]) ).
cnf(t50620,plain,
one = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t50619,t2642]) ).
cnf(t7531,plain,
join(X1,complement(meet(X2,X1))) = one,
inference(orient,[status(thm)],[t50620]) ).
cnf(t50691,plain,
join(X1,X2) = ifeq(one,one,complement(complement(meet(one,join(X1,X2)))),join(X1,X2)),
inference(step,[status(thm)],[t50690,t7531]) ).
cnf(t50692,plain,
join(X1,X2) = complement(complement(meet(one,join(X1,X2)))),
inference(step,[status(thm)],[t50691,t17]) ).
cnf(t50693,plain,
join(X1,X2) = meet(one,join(X1,X2)),
inference(step,[status(thm)],[t50692,t2642]) ).
cnf(t9841,plain,
meet(one,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t50693]) ).
cnf(t50896,plain,
zero = meet(complement(X1),join(X1,meet(complement(X2),join(X1,X2)))),
inference(step,[status(thm)],[t50895,t9841]) ).
cnf(t16784,plain,
meet(complement(X1),join(X1,meet(complement(X2),join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t50896]) ).
cnf(t16894,plain,
join(X1,meet(complement(X2),join(X1,X2))) = ifeq(zero,zero,ifeq(join(X1,join(meet(complement(X2),join(X1,X2)),complement(X1))),one,complement(complement(X1)),join(X1,meet(complement(X2),join(X1,X2)))),join(X1,meet(complement(X2),join(X1,X2)))),
inference(cp,[status(thm)],[t4364,t16784]) ).
cnf(t50897,plain,
join(X1,meet(complement(X2),join(X1,X2))) = ifeq(join(X1,join(meet(complement(X2),join(X1,X2)),complement(X1))),one,complement(complement(X1)),join(X1,meet(complement(X2),join(X1,X2)))),
inference(step,[status(thm)],[t16894,t17]) ).
cnf(t50898,plain,
join(X1,meet(complement(X2),join(X1,X2))) = ifeq(one,one,complement(complement(X1)),join(X1,meet(complement(X2),join(X1,X2)))),
inference(step,[status(thm)],[t50897,t152]) ).
cnf(t50899,plain,
join(X1,meet(complement(X2),join(X1,X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t50898,t17]) ).
cnf(t50900,plain,
join(X1,meet(complement(X2),join(X1,X2))) = X1,
inference(step,[status(thm)],[t50899,t2642]) ).
cnf(t16915,plain,
join(X1,meet(complement(X2),join(X1,X2))) = X1,
inference(orient,[status(thm)],[t50900]) ).
cnf(t17015,plain,
meet(complement(X1),join(X2,X1)) = meet(meet(complement(X1),join(X2,X1)),X2),
inference(cp,[status(thm)],[t6861,t16915]) ).
cnf(t51025,plain,
meet(complement(X1),join(X1,X2)) = meet(meet(complement(X1),join(X2,X1)),X2),
inference(step,[status(thm)],[t17015,t23]) ).
cnf(t51026,plain,
meet(complement(X1),join(X1,X2)) = meet(X2,meet(complement(X1),join(X2,X1))),
inference(step,[status(thm)],[t51025,t51]) ).
cnf(t51027,plain,
meet(complement(X1),join(X1,X2)) = meet(X2,complement(X1)),
inference(step,[status(thm)],[t51026,t179]) ).
cnf(t26200,plain,
meet(complement(X1),join(X1,X2)) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t51027]) ).
cnf(t26222,plain,
meet(X1,complement(complement(X2))) = meet(X2,join(complement(X2),X1)),
inference(cp,[status(thm)],[t26200,t2642]) ).
cnf(t51031,plain,
meet(X1,X2) = meet(X2,join(complement(X2),X1)),
inference(step,[status(thm)],[t26222,t2642]) ).
cnf(t51032,plain,
meet(X1,X2) = meet(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t51031,t23]) ).
cnf(t26468,plain,
meet(X1,join(X2,complement(X1))) = meet(X2,X1),
inference(orient,[status(thm)],[t51032]) ).
cnf(t1922,plain,
zero = meet(meet(X1,meet(X2,X3)),complement(join(meet(X1,X2),X4))),
inference(cp,[status(thm)],[t1887,t67]) ).
cnf(t50451,plain,
zero = meet(meet(X1,meet(X2,X3)),complement(join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t1922,t23]) ).
cnf(t3628,plain,
meet(meet(X1,meet(X2,X3)),complement(join(X4,meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t50451]) ).
cnf(t4920,plain,
zero = meet(complement(join(X1,X2)),complement(join(X3,meet(one,complement(X1))))),
inference(cp,[status(thm)],[t3628,t4896]) ).
cnf(t50536,plain,
zero = meet(complement(join(X1,X2)),complement(join(X3,complement(X1)))),
inference(step,[status(thm)],[t4920,t4816]) ).
cnf(t5016,plain,
meet(complement(join(X1,X2)),complement(join(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t50536]) ).
cnf(t5018,plain,
zero = meet(complement(join(X1,X2)),complement(join(X3,complement(X2)))),
inference(cp,[status(thm)],[t5016,t23]) ).
cnf(t5073,plain,
meet(complement(join(X1,X2)),complement(join(X3,complement(X2)))) = zero,
inference(orient,[status(thm)],[t5018]) ).
cnf(t6085,plain,
zero = meet(complement(join(X1,meet(X2,X3))),complement(complement(meet(X2,X3)))),
inference(cp,[status(thm)],[t5073,t6065]) ).
cnf(t50594,plain,
zero = meet(complement(join(X1,meet(X2,X3))),meet(X2,X3)),
inference(step,[status(thm)],[t6085,t2642]) ).
cnf(t50595,plain,
zero = meet(X3,meet(complement(join(X1,meet(X2,X3))),X2)),
inference(step,[status(thm)],[t50594,t67]) ).
cnf(t50596,plain,
zero = meet(X2,meet(X3,complement(join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t50595,t67]) ).
cnf(t6960,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t50596]) ).
cnf(t8585,plain,
meet(X1,complement(meet(X2,complement(X1)))) = meet(X1,join(complement(meet(X2,complement(X1))),X3)),
inference(cp,[status(thm)],[t8579,t5983]) ).
cnf(t50664,plain,
X1 = meet(X1,join(complement(meet(X2,complement(X1))),X3)),
inference(step,[status(thm)],[t8585,t5983]) ).
cnf(t50665,plain,
X1 = meet(X1,join(X3,complement(meet(X2,complement(X1))))),
inference(step,[status(thm)],[t50664,t23]) ).
cnf(t8674,plain,
meet(X1,join(X2,complement(meet(X3,complement(X1))))) = X1,
inference(orient,[status(thm)],[t50665]) ).
cnf(t8683,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,complement(complement(X1)))),
inference(cp,[status(thm)],[t8674,t6024]) ).
cnf(t50666,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(step,[status(thm)],[t8683,t2642]) ).
cnf(t50667,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t50666,t23]) ).
cnf(t8741,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t50667]) ).
cnf(t5820,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t5817,t4521]) ).
cnf(t50564,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t5820,t51]) ).
cnf(t5854,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t50564]) ).
cnf(t8747,plain,
meet(complement(X1),complement(join(X1,X2))) = meet(complement(join(X1,X2)),join(complement(X1),X3)),
inference(cp,[status(thm)],[t8741,t5854]) ).
cnf(t50710,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),join(complement(X1),X3)),
inference(step,[status(thm)],[t8747,t5854]) ).
cnf(t50711,plain,
complement(join(X1,X2)) = meet(join(complement(X1),X3),complement(join(X1,X2))),
inference(step,[status(thm)],[t50710,t51]) ).
cnf(t50712,plain,
complement(join(X1,X2)) = meet(join(X3,complement(X1)),complement(join(X1,X2))),
inference(step,[status(thm)],[t50711,t23]) ).
cnf(t10956,plain,
meet(join(X1,complement(X2)),complement(join(X2,X3))) = complement(join(X2,X3)),
inference(orient,[status(thm)],[t50712]) ).
cnf(t11053,plain,
zero = meet(X1,complement(join(X2,meet(X1,join(X3,complement(X2)))))),
inference(cp,[status(thm)],[t6960,t10956]) ).
cnf(t14061,plain,
meet(X1,complement(join(X2,meet(X1,join(X3,complement(X2)))))) = zero,
inference(orient,[status(thm)],[t11053]) ).
cnf(t14067,plain,
zero = meet(X1,complement(join(join(X2,complement(X3)),meet(X1,X3)))),
inference(cp,[status(thm)],[t14061,t4473]) ).
cnf(t50839,plain,
zero = meet(X1,complement(join(meet(X1,X3),join(X2,complement(X3))))),
inference(step,[status(thm)],[t14067,t23]) ).
cnf(t50840,plain,
zero = meet(X1,complement(join(complement(X3),join(meet(X1,X3),X2)))),
inference(step,[status(thm)],[t50839,t26]) ).
cnf(t50841,plain,
zero = meet(X1,complement(join(X2,join(complement(X3),meet(X1,X3))))),
inference(step,[status(thm)],[t50840,t26]) ).
cnf(t15000,plain,
meet(X1,complement(join(X2,join(complement(X3),meet(X1,X3))))) = zero,
inference(orient,[status(thm)],[t50841]) ).
cnf(t15004,plain,
zero = complement(join(X1,join(complement(X2),meet(complement(X1),X2)))),
inference(cp,[status(thm)],[t15000,t5854]) ).
cnf(t50842,plain,
zero = complement(join(X1,join(complement(X2),meet(X2,complement(X1))))),
inference(step,[status(thm)],[t15004,t51]) ).
cnf(t15138,plain,
complement(join(X1,join(complement(X2),meet(X2,complement(X1))))) = zero,
inference(orient,[status(thm)],[t50842]) ).
cnf(t15181,plain,
one = ifeq(zero,zero,join(X1,join(complement(X2),meet(X2,complement(X1)))),one),
inference(cp,[status(thm)],[t2718,t15138]) ).
cnf(t50843,plain,
one = join(X1,join(complement(X2),meet(X2,complement(X1)))),
inference(step,[status(thm)],[t15181,t17]) ).
cnf(t15240,plain,
join(X1,join(complement(X2),meet(X2,complement(X1)))) = one,
inference(orient,[status(thm)],[t50843]) ).
cnf(t6962,plain,
zero = meet(X1,complement(join(X2,meet(X1,complement(X2))))),
inference(cp,[status(thm)],[t6960,t5854]) ).
cnf(t7052,plain,
meet(X1,complement(join(X2,meet(X1,complement(X2))))) = zero,
inference(orient,[status(thm)],[t6962]) ).
cnf(t7054,plain,
zero = meet(X1,complement(join(complement(X2),meet(X1,X2)))),
inference(cp,[status(thm)],[t7052,t2642]) ).
cnf(t7079,plain,
meet(X1,complement(join(complement(X2),meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t7054]) ).
cnf(t15250,plain,
one = join(join(complement(X1),meet(X2,X1)),join(complement(X2),zero)),
inference(cp,[status(thm)],[t15240,t7079]) ).
cnf(t50845,plain,
one = join(join(complement(X1),meet(X2,X1)),complement(X2)),
inference(step,[status(thm)],[t15250,t102]) ).
cnf(t50846,plain,
one = join(complement(X2),join(complement(X1),meet(X2,X1))),
inference(step,[status(thm)],[t50845,t23]) ).
cnf(t50847,plain,
one = join(complement(X1),join(meet(X2,X1),complement(X2))),
inference(step,[status(thm)],[t50846,t26]) ).
cnf(t50848,plain,
one = join(complement(X1),join(complement(X2),meet(X2,X1))),
inference(step,[status(thm)],[t50847,t23]) ).
cnf(t50849,plain,
one = join(complement(X1),join(complement(X2),meet(X1,X2))),
inference(step,[status(thm)],[t50848,t51]) ).
cnf(t15374,plain,
join(complement(X1),join(complement(X2),meet(X1,X2))) = one,
inference(orient,[status(thm)],[t50849]) ).
cnf(t15412,plain,
one = join(complement(X1),join(complement(meet(X2,complement(meet(X1,X2)))),zero)),
inference(cp,[status(thm)],[t15374,t3341]) ).
cnf(t50850,plain,
one = join(complement(X1),complement(meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t15412,t102]) ).
cnf(t15506,plain,
join(complement(X1),complement(meet(X2,complement(meet(X1,X2))))) = one,
inference(orient,[status(thm)],[t50850]) ).
cnf(t15507,plain,
one = join(X1,complement(meet(X2,complement(meet(complement(X1),X2))))),
inference(cp,[status(thm)],[t15506,t2642]) ).
cnf(t50864,plain,
one = join(X1,complement(meet(X2,complement(meet(X2,complement(X1)))))),
inference(step,[status(thm)],[t15507,t51]) ).
cnf(t16124,plain,
join(X1,complement(meet(X2,complement(meet(X2,complement(X1)))))) = one,
inference(orient,[status(thm)],[t50864]) ).
cnf(t26482,plain,
meet(X1,meet(X2,complement(meet(X2,complement(X1))))) = meet(meet(X2,complement(meet(X2,complement(X1)))),one),
inference(cp,[status(thm)],[t26468,t16124]) ).
cnf(t6022,plain,
meet(X1,meet(complement(meet(X2,complement(X1))),X3)) = meet(X3,X1),
inference(cp,[status(thm)],[t67,t5983]) ).
cnf(t50586,plain,
meet(X1,meet(X3,complement(meet(X2,complement(X1))))) = meet(X3,X1),
inference(step,[status(thm)],[t6022,t51]) ).
cnf(t50587,plain,
meet(X1,meet(X3,complement(meet(X2,complement(X1))))) = meet(X1,X3),
inference(step,[status(thm)],[t50586,t51]) ).
cnf(t6623,plain,
meet(X1,meet(X2,complement(meet(X3,complement(X1))))) = meet(X1,X2),
inference(orient,[status(thm)],[t50587]) ).
cnf(t51050,plain,
meet(X1,X2) = meet(meet(X2,complement(meet(X2,complement(X1)))),one),
inference(step,[status(thm)],[t26482,t6623]) ).
cnf(t51051,plain,
meet(X1,X2) = meet(X2,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t51050,t96]) ).
cnf(t27578,plain,
meet(X1,complement(meet(X1,complement(X2)))) = meet(X2,X1),
inference(orient,[status(thm)],[t51051]) ).
cnf(t27629,plain,
meet(complement(X1),X2) = meet(X2,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t27578,t2642]) ).
cnf(t51059,plain,
meet(X2,complement(X1)) = meet(X2,complement(meet(X2,X1))),
inference(step,[status(thm)],[t27629,t51]) ).
cnf(t51060,plain,
meet(X2,complement(X1)) = meet(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t51059,t51]) ).
cnf(t28029,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t51060]) ).
cnf(t28117,plain,
meet(X1,complement(X2)) = meet(X1,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t28029,t51]) ).
cnf(t28218,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t28117]) ).
cnf(t28223,plain,
meet(X1,complement(join(X2,complement(X1)))) = meet(X1,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t28218,t26468]) ).
cnf(t51063,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(meet(X2,X1))),
inference(step,[status(thm)],[t28223,t5898]) ).
cnf(t51064,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t51063,t28029]) ).
cnf(t28392,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t51064]) ).
cnf(t28431,plain,
join(X1,complement(X2)) = complement(meet(X2,complement(X1))),
inference(cp,[status(thm)],[t2642,t28392]) ).
cnf(t28797,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t28431]) ).
cnf(t28798,plain,
join(meet(X1,X2),complement(X1)) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t28797,t28218]) ).
cnf(t51106,plain,
join(complement(X1),meet(X1,X2)) = complement(meet(X1,complement(X2))),
inference(step,[status(thm)],[t28798,t23]) ).
cnf(t51107,plain,
join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
inference(step,[status(thm)],[t51106,t28797]) ).
cnf(t29110,plain,
join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t51107]) ).
cnf(t29119,plain,
join(X1,complement(complement(X2))) = join(X2,meet(complement(X2),X1)),
inference(cp,[status(thm)],[t29110,t2642]) ).
cnf(t51111,plain,
join(X1,X2) = join(X2,meet(complement(X2),X1)),
inference(step,[status(thm)],[t29119,t2642]) ).
cnf(t51112,plain,
join(X1,X2) = join(X2,meet(X1,complement(X2))),
inference(step,[status(thm)],[t51111,t51]) ).
cnf(t29330,plain,
join(X1,meet(X2,complement(X1))) = join(X2,X1),
inference(orient,[status(thm)],[t51112]) ).
cnf(t26346,plain,
meet(X1,complement(X2)) = meet(complement(X2),join(X1,X2)),
inference(cp,[status(thm)],[t26200,t23]) ).
cnf(t27199,plain,
meet(complement(X1),join(X2,X1)) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t26346]) ).
cnf(t28275,plain,
meet(complement(X1),complement(join(X2,X1))) = meet(complement(X1),complement(meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t28218,t27199]) ).
cnf(t51084,plain,
complement(join(X2,X1)) = meet(complement(X1),complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t28275,t5933]) ).
cnf(t51085,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t51084,t23]) ).
cnf(t51086,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(X2)),
inference(step,[status(thm)],[t51085,t28029]) ).
cnf(t28630,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t51086]) ).
cnf(t29358,plain,
join(complement(X1),X2) = join(X2,complement(join(X1,X2))),
inference(cp,[status(thm)],[t29330,t28630]) ).
cnf(t51116,plain,
join(X2,complement(X1)) = join(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t29358,t23]) ).
cnf(t29647,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t51116]) ).
cnf(t7546,plain,
one = join(meet(X1,join(X2,X3)),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t7531,t179]) ).
cnf(t50638,plain,
one = join(complement(meet(X2,X1)),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t7546,t23]) ).
cnf(t50639,plain,
one = join(complement(meet(X1,X2)),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t50638,t51]) ).
cnf(t7852,plain,
join(complement(meet(X1,X2)),meet(X1,join(X2,X3))) = one,
inference(orient,[status(thm)],[t50639]) ).
cnf(t29687,plain,
join(meet(X1,join(X2,X3)),complement(complement(meet(X1,X2)))) = join(meet(X1,join(X2,X3)),complement(one)),
inference(cp,[status(thm)],[t29647,t7852]) ).
cnf(t51382,plain,
join(meet(X1,join(X2,X3)),meet(X1,X2)) = join(meet(X1,join(X2,X3)),complement(one)),
inference(step,[status(thm)],[t29687,t2642]) ).
cnf(t51383,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = join(meet(X1,join(X2,X3)),complement(one)),
inference(step,[status(thm)],[t51382,t23]) ).
cnf(t51384,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = join(complement(one),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t51383,t23]) ).
cnf(t51385,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = join(zero,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t51384,t147]) ).
cnf(t51386,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t51385,t1264]) ).
cnf(t49492,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t51386]) ).
cnf(t49519,plain,
meet(X1,join(meet(X1,X2),X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t49492,t123]) ).
cnf(t51387,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t49519,t23]) ).
cnf(t28825,plain,
join(join(X1,complement(X2)),complement(X3)) = complement(meet(X3,meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t28797,t28392]) ).
cnf(t51177,plain,
join(complement(X3),join(X1,complement(X2))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t28825,t23]) ).
cnf(t51178,plain,
join(complement(X2),join(complement(X3),X1)) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t51177,t26]) ).
cnf(t51179,plain,
join(X1,join(complement(X2),complement(X3))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t51178,t26]) ).
cnf(t28826,plain,
join(complement(X1),complement(X2)) = complement(meet(X2,X1)),
inference(cp,[status(thm)],[t28797,t2642]) ).
cnf(t51102,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t28826,t51]) ).
cnf(t28979,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t51102]) ).
cnf(t51180,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t51179,t28979]) ).
cnf(t51181,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X2,meet(complement(X1),X3))),
inference(step,[status(thm)],[t51180,t67]) ).
cnf(t51182,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X2,meet(X3,complement(X1)))),
inference(step,[status(thm)],[t51181,t51]) ).
cnf(t33006,plain,
complement(meet(X1,meet(X2,complement(X3)))) = join(X3,complement(meet(X1,X2))),
inference(orient,[status(thm)],[t51182]) ).
cnf(t33074,plain,
meet(X1,complement(meet(X2,complement(X3)))) = meet(X1,join(X3,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t28218,t33006]) ).
cnf(t51336,plain,
meet(X1,join(X3,complement(X2))) = meet(X1,join(X3,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t33074,t28797]) ).
cnf(t45306,plain,
meet(X1,join(X2,complement(meet(X1,X3)))) = meet(X1,join(X2,complement(X3))),
inference(orient,[status(thm)],[t51336]) ).
cnf(t45337,plain,
meet(X1,join(X2,complement(complement(meet(X1,X3))))) = meet(X1,join(X2,complement(meet(X1,complement(X3))))),
inference(cp,[status(thm)],[t45306,t28218]) ).
cnf(t51339,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,complement(meet(X1,complement(X3))))),
inference(step,[status(thm)],[t45337,t2642]) ).
cnf(t51340,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,complement(complement(X3)))),
inference(step,[status(thm)],[t51339,t45306]) ).
cnf(t51341,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t51340,t2642]) ).
cnf(t45475,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t51341]) ).
cnf(t51388,plain,
meet(X1,join(X3,X2)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t51387,t45475]) ).
cnf(t51389,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t51388,t23]) ).
cnf(t29694,plain,
join(X1,complement(X2)) = join(X1,complement(join(X1,X2))),
inference(cp,[status(thm)],[t29647,t23]) ).
cnf(t29762,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t29694]) ).
cnf(t28646,plain,
complement(join(join(X1,complement(X2)),X3)) = meet(meet(X2,complement(X1)),complement(X3)),
inference(cp,[status(thm)],[t28630,t28392]) ).
cnf(t51169,plain,
complement(join(X3,join(X1,complement(X2)))) = meet(meet(X2,complement(X1)),complement(X3)),
inference(step,[status(thm)],[t28646,t23]) ).
cnf(t51170,plain,
complement(join(X1,join(complement(X2),X3))) = meet(meet(X2,complement(X1)),complement(X3)),
inference(step,[status(thm)],[t51169,t26]) ).
cnf(t51171,plain,
complement(join(X1,join(X3,complement(X2)))) = meet(meet(X2,complement(X1)),complement(X3)),
inference(step,[status(thm)],[t51170,t23]) ).
cnf(t51172,plain,
complement(join(X1,join(X3,complement(X2)))) = meet(complement(X3),meet(X2,complement(X1))),
inference(step,[status(thm)],[t51171,t51]) ).
cnf(t51173,plain,
complement(join(X1,join(X3,complement(X2)))) = meet(complement(X1),meet(complement(X3),X2)),
inference(step,[status(thm)],[t51172,t67]) ).
cnf(t51174,plain,
complement(join(X1,join(X3,complement(X2)))) = meet(X2,meet(complement(X1),complement(X3))),
inference(step,[status(thm)],[t51173,t67]) ).
cnf(t51175,plain,
complement(join(X1,join(X3,complement(X2)))) = meet(X2,complement(join(X1,X3))),
inference(step,[status(thm)],[t51174,t28630]) ).
cnf(t32863,plain,
complement(join(X1,join(X2,complement(X3)))) = meet(X3,complement(join(X1,X2))),
inference(orient,[status(thm)],[t51175]) ).
cnf(t32923,plain,
join(X1,complement(join(X2,complement(X3)))) = join(X1,meet(X3,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t29762,t32863]) ).
cnf(t51322,plain,
join(X1,meet(X3,complement(X2))) = join(X1,meet(X3,complement(join(X1,X2)))),
inference(step,[status(thm)],[t32923,t28392]) ).
cnf(t44683,plain,
join(X1,meet(X2,complement(join(X1,X3)))) = join(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t51322]) ).
cnf(t44713,plain,
join(X1,meet(X2,complement(complement(join(X1,X3))))) = join(X1,meet(X2,complement(join(X1,complement(X3))))),
inference(cp,[status(thm)],[t44683,t29762]) ).
cnf(t51323,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,complement(join(X1,complement(X3))))),
inference(step,[status(thm)],[t44713,t2642]) ).
cnf(t51324,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,complement(complement(X3)))),
inference(step,[status(thm)],[t51323,t44683]) ).
cnf(t51325,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t51324,t2642]) ).
cnf(t44856,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t51325]) ).
cnf(t51390,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,X3)),
inference(step,[status(thm)],[t51389,t44856]) ).
cnf(t49737,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t51390]) ).
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,t49737]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT198-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 20:32:12 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 38.37/5.33 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 38.37/5.33 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------