%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT209-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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:56:07 PM UTC 2026
% Result : Unsatisfiable 59.67s 13.00s
% Output : Proof 59.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 253
% Number of leaves : 14
% Syntax : Number of formulae : 765 ( 761 unt; 0 def)
% Number of atoms : 773 ( 772 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 : 11 ( 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 : 2003 ( 486 sgn 46 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f10,axiom,
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f10_nnf,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( complement(X0) = X1
| join(X0,X1) != one
| meet(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t11,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t18,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(f4,axiom,
meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f4_nnf,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t7,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t23,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t25,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X2,X1),one,complement(X2),X1),X1),
inference(cp,[status(thm)],[t18,t23]) ).
cnf(f5,axiom,
join(X,Y) = join(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f5_nnf,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t63,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t115725,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(step,[status(thm)],[t25,t63]) ).
cnf(t798,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t115725]) ).
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(t57,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t819,plain,
X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t798,t57]) ).
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(t115726,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t819,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(t87,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t115727,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t115726,t87]) ).
cnf(t115728,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t115727,t17]) ).
cnf(t839,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t115728]) ).
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(t115569,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t9,t63]) ).
cnf(t67,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t115569]) ).
cnf(t89,plain,
join(X1,join(complement(X1),X2)) = join(X2,one),
inference(cp,[status(thm)],[t67,t87]) ).
cnf(t115582,plain,
join(X1,join(X2,complement(X1))) = join(X2,one),
inference(step,[status(thm)],[t89,t63]) ).
cnf(f1,axiom,
join(X,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f1_nnf,plain,
! [X] : join(X,X) = X,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] : join(X,X) = X,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t0,plain,
join(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t15,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t70,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t67,t15]) ).
cnf(t115573,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t70,t67]) ).
cnf(t115574,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t115573,t63]) ).
cnf(t119,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t115574]) ).
cnf(t122,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t119,t87]) ).
cnf(t115575,plain,
one = join(X1,one),
inference(step,[status(thm)],[t122,t87]) ).
cnf(t129,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t115575]) ).
cnf(t115583,plain,
join(X1,join(X2,complement(X1))) = one,
inference(step,[status(thm)],[t115582,t129]) ).
cnf(t154,plain,
join(X1,join(X2,complement(X1))) = one,
inference(orient,[status(thm)],[t115583]) ).
cnf(t832,plain,
X1 = ifeq(meet(X1,join(X2,complement(X1))),zero,ifeq(one,one,complement(join(X2,complement(X1))),X1),X1),
inference(cp,[status(thm)],[t798,t154]) ).
cnf(t115787,plain,
X1 = ifeq(meet(X1,join(X2,complement(X1))),zero,complement(join(X2,complement(X1))),X1),
inference(step,[status(thm)],[t832,t17]) ).
cnf(t1230,plain,
ifeq(meet(X1,join(X2,complement(X1))),zero,complement(join(X2,complement(X1))),X1) = X1,
inference(orient,[status(thm)],[t115787]) ).
cnf(t1232,plain,
complement(X1) = ifeq(meet(complement(X1),join(X2,X1)),zero,complement(join(X2,complement(complement(X1)))),complement(X1)),
inference(cp,[status(thm)],[t1230,t839]) ).
cnf(t115808,plain,
complement(X1) = ifeq(meet(complement(X1),join(X1,X2)),zero,complement(join(X2,complement(complement(X1)))),complement(X1)),
inference(step,[status(thm)],[t1232,t63]) ).
cnf(t115809,plain,
complement(X1) = ifeq(meet(complement(X1),join(X1,X2)),zero,complement(join(X2,X1)),complement(X1)),
inference(step,[status(thm)],[t115808,t839]) ).
cnf(t115810,plain,
complement(X1) = ifeq(meet(complement(X1),join(X1,X2)),zero,complement(join(X1,X2)),complement(X1)),
inference(step,[status(thm)],[t115809,t63]) ).
cnf(t1333,plain,
ifeq(meet(complement(X1),join(X1,X2)),zero,complement(join(X1,X2)),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t115810]) ).
cnf(f11,axiom,
meet(X,join(Y,Z)) = meet(X,join(Y,meet(X,join(Z,meet(X,join(Y,meet(X,Z))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H64) ).
fof(f11_nnf,plain,
! [X,Y,Z] : meet(X,join(Y,Z)) = meet(X,join(Y,meet(X,join(Z,meet(X,join(Y,meet(X,Z))))))),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z] : meet(X,join(Y,Z)) = meet(X,join(Y,meet(X,join(Z,meet(X,join(Y,meet(X,Z))))))),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(X0,join(X2,meet(X0,join(X1,meet(X0,X2))))))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t12,plain,
meet(X1,join(X2,meet(X1,join(X3,meet(X1,join(X2,meet(X1,X3))))))) = meet(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t46,plain,
meet(X1,join(X2,meet(X1,join(X3,meet(X1,join(X2,meet(X1,X3))))))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t12]) ).
cnf(t60,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(X2,meet(X1,join(complement(X1),meet(X1,join(X2,zero)))))),
inference(cp,[status(thm)],[t46,t57]) ).
cnf(f3,axiom,
join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption2) ).
fof(f3_nnf,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t6,plain,
join(X1,meet(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t16,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t58,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t16,t57]) ).
cnf(t91,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t58]) ).
cnf(t116016,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(X2,meet(X1,join(complement(X1),meet(X1,X2))))),
inference(step,[status(thm)],[t60,t91]) ).
cnf(t3993,plain,
meet(X1,join(X2,meet(X1,join(complement(X1),meet(X1,X2))))) = meet(X1,join(X2,complement(X1))),
inference(orient,[status(thm)],[t116016]) ).
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(t115568,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)],[t115568]) ).
cnf(f0,axiom,
meet(X,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f0_nnf,plain,
! [X] : meet(X,X) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : meet(X,X) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
meet(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
meet(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t13,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t29,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t26,t13]) ).
cnf(t115570,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t29,t26]) ).
cnf(t115571,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t115570,t23]) ).
cnf(t102,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t115571]) ).
cnf(t105,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t102,t57]) ).
cnf(t115572,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t105,t57]) ).
cnf(t113,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t115572]) ).
cnf(t116,plain,
meet(X1,join(X2,zero)) = meet(X1,join(X2,meet(X1,join(zero,meet(X1,join(X2,zero)))))),
inference(cp,[status(thm)],[t46,t113]) ).
cnf(t115621,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,join(zero,meet(X1,join(X2,zero)))))),
inference(step,[status(thm)],[t116,t91]) ).
cnf(t115622,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,join(zero,meet(X1,X2))))),
inference(step,[status(thm)],[t115621,t91]) ).
cnf(t268,plain,
meet(X1,join(X2,meet(X1,join(zero,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t115622]) ).
cnf(t283,plain,
meet(X1,join(zero,X2)) = meet(X1,join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t46,t268]) ).
cnf(t115623,plain,
meet(X1,join(X2,zero)) = meet(X1,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t283,t63]) ).
cnf(t115624,plain,
meet(X1,X2) = meet(X1,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t115623,t91]) ).
cnf(t288,plain,
meet(X1,join(zero,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t115624]) ).
cnf(t304,plain,
meet(X1,meet(join(zero,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t26,t288]) ).
cnf(t115629,plain,
meet(X1,meet(X3,join(zero,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t304,t23]) ).
cnf(t115630,plain,
meet(X1,meet(X3,join(zero,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t115629,t26]) ).
cnf(t115631,plain,
meet(X1,meet(X3,join(zero,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t115630,t26]) ).
cnf(t323,plain,
meet(X1,meet(X2,join(zero,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t115631]) ).
cnf(t301,plain,
meet(X1,join(X2,zero)) = meet(X1,join(X2,meet(X1,join(X2,meet(X1,zero))))),
inference(cp,[status(thm)],[t46,t288]) ).
cnf(t115626,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,join(X2,meet(X1,zero))))),
inference(step,[status(thm)],[t301,t91]) ).
cnf(t115627,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,join(X2,zero)))),
inference(step,[status(thm)],[t115626,t113]) ).
cnf(t115628,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t115627,t91]) ).
cnf(t307,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t115628]) ).
cnf(f2,axiom,
meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption1) ).
fof(f2_nnf,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t8,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t14,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t30,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t26,t14]) ).
cnf(t115584,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t30,t26]) ).
cnf(t115585,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t115584,t23]) ).
cnf(t115586,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t115585,t23]) ).
cnf(t161,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t115586]) ).
cnf(t310,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t307,t161]) ).
cnf(t115635,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(step,[status(thm)],[t310,t161]) ).
cnf(t115636,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t115635,t63]) ).
cnf(t388,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t115636]) ).
cnf(t61,plain,
meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
inference(cp,[status(thm)],[t26,t57]) ).
cnf(t115580,plain,
meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
inference(step,[status(thm)],[t61,t23]) ).
cnf(t115581,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t115580,t113]) ).
cnf(t146,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t115581]) ).
cnf(t394,plain,
meet(X1,meet(X2,complement(X1))) = meet(X1,join(zero,meet(meet(X2,complement(X1)),join(X1,X3)))),
inference(cp,[status(thm)],[t388,t146]) ).
cnf(t115661,plain,
zero = meet(X1,join(zero,meet(meet(X2,complement(X1)),join(X1,X3)))),
inference(step,[status(thm)],[t394,t146]) ).
cnf(t115662,plain,
zero = meet(X1,join(zero,meet(join(X1,X3),meet(X2,complement(X1))))),
inference(step,[status(thm)],[t115661,t23]) ).
cnf(t115663,plain,
zero = meet(X1,join(zero,meet(complement(X1),meet(join(X1,X3),X2)))),
inference(step,[status(thm)],[t115662,t26]) ).
cnf(t115664,plain,
zero = meet(X1,join(zero,meet(X2,meet(complement(X1),join(X1,X3))))),
inference(step,[status(thm)],[t115663,t26]) ).
cnf(t513,plain,
meet(X1,join(zero,meet(X2,meet(complement(X1),join(X1,X3))))) = zero,
inference(orient,[status(thm)],[t115664]) ).
cnf(t159,plain,
join(X1,join(join(X2,complement(X1)),X3)) = join(X3,one),
inference(cp,[status(thm)],[t67,t154]) ).
cnf(t115594,plain,
join(X1,join(X3,join(X2,complement(X1)))) = join(X3,one),
inference(step,[status(thm)],[t159,t63]) ).
cnf(t115595,plain,
join(X1,join(X2,join(complement(X1),X3))) = join(X3,one),
inference(step,[status(thm)],[t115594,t67]) ).
cnf(t115596,plain,
join(X1,join(X2,join(X3,complement(X1)))) = join(X3,one),
inference(step,[status(thm)],[t115595,t63]) ).
cnf(t115597,plain,
join(X1,join(X2,join(X3,complement(X1)))) = one,
inference(step,[status(thm)],[t115596,t129]) ).
cnf(t197,plain,
join(X1,join(X2,join(X3,complement(X1)))) = one,
inference(orient,[status(thm)],[t115597]) ).
cnf(t520,plain,
zero = meet(X1,join(zero,meet(X2,meet(complement(X1),one)))),
inference(cp,[status(thm)],[t513,t197]) ).
cnf(t88,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t14,t87]) ).
cnf(t96,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t88]) ).
cnf(t115665,plain,
zero = meet(X1,join(zero,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t520,t96]) ).
cnf(t541,plain,
meet(X1,join(zero,meet(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t115665]) ).
cnf(t548,plain,
meet(X1,meet(join(zero,meet(X2,complement(X1))),X3)) = meet(X1,meet(X3,join(zero,zero))),
inference(cp,[status(thm)],[t323,t541]) ).
cnf(t115674,plain,
meet(X1,meet(X3,join(zero,meet(X2,complement(X1))))) = meet(X1,meet(X3,join(zero,zero))),
inference(step,[status(thm)],[t548,t23]) ).
cnf(t115675,plain,
meet(X1,meet(X3,join(zero,meet(X2,complement(X1))))) = meet(X1,meet(X3,zero)),
inference(step,[status(thm)],[t115674,t91]) ).
cnf(t115676,plain,
meet(X1,meet(X3,join(zero,meet(X2,complement(X1))))) = meet(X1,zero),
inference(step,[status(thm)],[t115675,t113]) ).
cnf(t115677,plain,
meet(X1,meet(X3,join(zero,meet(X2,complement(X1))))) = zero,
inference(step,[status(thm)],[t115676,t113]) ).
cnf(t567,plain,
meet(X1,meet(X2,join(zero,meet(X3,complement(X1))))) = zero,
inference(orient,[status(thm)],[t115677]) ).
cnf(t577,plain,
meet(X1,meet(meet(X2,join(zero,meet(X3,complement(X1)))),Y3)) = meet(X1,meet(Y3,join(zero,zero))),
inference(cp,[status(thm)],[t323,t567]) ).
cnf(t115682,plain,
meet(X1,meet(Y3,meet(X2,join(zero,meet(X3,complement(X1)))))) = meet(X1,meet(Y3,join(zero,zero))),
inference(step,[status(thm)],[t577,t23]) ).
cnf(t115683,plain,
meet(X1,meet(X2,meet(join(zero,meet(X3,complement(X1))),Y3))) = meet(X1,meet(Y3,join(zero,zero))),
inference(step,[status(thm)],[t115682,t26]) ).
cnf(t115684,plain,
meet(X1,meet(X2,meet(Y3,join(zero,meet(X3,complement(X1)))))) = meet(X1,meet(Y3,join(zero,zero))),
inference(step,[status(thm)],[t115683,t23]) ).
cnf(t115685,plain,
meet(X1,meet(X2,meet(Y3,join(zero,meet(X3,complement(X1)))))) = meet(X1,meet(Y3,zero)),
inference(step,[status(thm)],[t115684,t91]) ).
cnf(t115686,plain,
meet(X1,meet(X2,meet(Y3,join(zero,meet(X3,complement(X1)))))) = meet(X1,zero),
inference(step,[status(thm)],[t115685,t113]) ).
cnf(t115687,plain,
meet(X1,meet(X2,meet(Y3,join(zero,meet(X3,complement(X1)))))) = zero,
inference(step,[status(thm)],[t115686,t113]) ).
cnf(t608,plain,
meet(X1,meet(X2,meet(X3,join(zero,meet(Y3,complement(X1)))))) = zero,
inference(orient,[status(thm)],[t115687]) ).
cnf(t4037,plain,
meet(X1,join(meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))),complement(X1))) = meet(X1,join(meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))),meet(X1,join(complement(X1),zero)))),
inference(cp,[status(thm)],[t3993,t608]) ).
cnf(t116166,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))) = meet(X1,join(meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))),meet(X1,join(complement(X1),zero)))),
inference(step,[status(thm)],[t4037,t63]) ).
cnf(t116167,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))) = meet(X1,join(meet(X1,join(complement(X1),zero)),meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))),
inference(step,[status(thm)],[t116166,t63]) ).
cnf(t116168,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))) = meet(X1,join(meet(X1,complement(X1)),meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))),
inference(step,[status(thm)],[t116167,t91]) ).
cnf(t116169,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))) = meet(X1,join(zero,meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))),
inference(step,[status(thm)],[t116168,t57]) ).
cnf(t399,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,join(meet(X1,X2),meet(join(X2,meet(X1,X2)),join(X1,X3)))),
inference(cp,[status(thm)],[t388,t307]) ).
cnf(t115848,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(X2,meet(X1,X2)),join(X1,X3)))),
inference(step,[status(thm)],[t399,t307]) ).
cnf(t115849,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(X1,X3),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t115848,t23]) ).
cnf(t2037,plain,
meet(X1,join(meet(X1,X2),meet(join(X1,X3),join(X2,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t115849]) ).
cnf(t2084,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(one,join(X2,meet(X1,X2))))),
inference(cp,[status(thm)],[t2037,t197]) ).
cnf(t2166,plain,
meet(X1,join(meet(X1,X2),meet(one,join(X2,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t2084]) ).
cnf(t2190,plain,
meet(X1,meet(X2,meet(X3,join(zero,meet(Y3,complement(X1)))))) = meet(X1,join(zero,meet(one,join(meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))),meet(X1,meet(X2,meet(X3,join(zero,meet(Y3,complement(X1)))))))))),
inference(cp,[status(thm)],[t2166,t608]) ).
cnf(t115965,plain,
zero = meet(X1,join(zero,meet(one,join(meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))),meet(X1,meet(X2,meet(X3,join(zero,meet(Y3,complement(X1)))))))))),
inference(step,[status(thm)],[t2190,t608]) ).
cnf(t115966,plain,
zero = meet(X1,join(zero,meet(one,join(meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))),zero)))),
inference(step,[status(thm)],[t115965,t608]) ).
cnf(t115967,plain,
zero = meet(X1,join(zero,meet(one,meet(X2,meet(X3,join(zero,meet(Y3,complement(X1)))))))),
inference(step,[status(thm)],[t115966,t91]) ).
cnf(t115968,plain,
zero = meet(X1,join(zero,meet(X2,meet(meet(X3,join(zero,meet(Y3,complement(X1)))),one)))),
inference(step,[status(thm)],[t115967,t26]) ).
cnf(t115969,plain,
zero = meet(X1,join(zero,meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))),
inference(step,[status(thm)],[t115968,t96]) ).
cnf(t3383,plain,
meet(X1,join(zero,meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))) = zero,
inference(orient,[status(thm)],[t115969]) ).
cnf(t116170,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))) = zero,
inference(step,[status(thm)],[t116169,t3383]) ).
cnf(t5941,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,join(zero,meet(Y3,complement(X1))))))) = zero,
inference(orient,[status(thm)],[t116170]) ).
cnf(t5942,plain,
zero = meet(complement(X1),join(X1,meet(X2,meet(X3,join(zero,meet(Y3,complement(complement(X1)))))))),
inference(cp,[status(thm)],[t5941,t839]) ).
cnf(t116171,plain,
zero = meet(complement(X1),join(X1,meet(X2,meet(X3,join(zero,meet(Y3,X1)))))),
inference(step,[status(thm)],[t5942,t839]) ).
cnf(t116172,plain,
zero = meet(complement(X1),join(X1,meet(X2,meet(X3,join(zero,meet(X1,Y3)))))),
inference(step,[status(thm)],[t116171,t23]) ).
cnf(t5985,plain,
meet(complement(X1),join(X1,meet(X2,meet(X3,join(zero,meet(X1,Y3)))))) = zero,
inference(orient,[status(thm)],[t116172]) ).
cnf(t423,plain,
meet(X1,meet(join(meet(X1,X2),meet(X2,join(X1,X3))),Y3)) = meet(X1,meet(Y3,join(zero,meet(X1,X2)))),
inference(cp,[status(thm)],[t323,t388]) ).
cnf(t115816,plain,
meet(X1,meet(Y3,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X1,meet(Y3,join(zero,meet(X1,X2)))),
inference(step,[status(thm)],[t423,t23]) ).
cnf(t115817,plain,
meet(X1,meet(Y3,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X1,meet(X2,Y3)),
inference(step,[status(thm)],[t115816,t323]) ).
cnf(t1359,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,Y3))))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t115817]) ).
cnf(t4057,plain,
meet(X1,join(one,complement(X1))) = meet(X1,join(one,meet(X1,join(complement(X1),X1)))),
inference(cp,[status(thm)],[t3993,t96]) ).
cnf(t116041,plain,
meet(X1,join(one,complement(X1))) = meet(X1,join(one,meet(X1,join(X1,complement(X1))))),
inference(step,[status(thm)],[t4057,t63]) ).
cnf(t116042,plain,
meet(X1,join(one,complement(X1))) = meet(X1,join(one,meet(X1,one))),
inference(step,[status(thm)],[t116041,t87]) ).
cnf(t116043,plain,
meet(X1,join(one,complement(X1))) = meet(X1,join(one,X1)),
inference(step,[status(thm)],[t116042,t96]) ).
cnf(t116044,plain,
meet(X1,join(one,complement(X1))) = meet(X1,join(X1,one)),
inference(step,[status(thm)],[t116043,t63]) ).
cnf(t116045,plain,
meet(X1,join(one,complement(X1))) = meet(X1,one),
inference(step,[status(thm)],[t116044,t129]) ).
cnf(t116046,plain,
meet(X1,join(one,complement(X1))) = X1,
inference(step,[status(thm)],[t116045,t96]) ).
cnf(t4219,plain,
meet(X1,join(one,complement(X1))) = X1,
inference(orient,[status(thm)],[t116046]) ).
cnf(t4243,plain,
meet(X1,meet(join(one,complement(X1)),X2)) = meet(X1,meet(X2,join(X1,meet(join(one,complement(X1)),join(X1,X3))))),
inference(cp,[status(thm)],[t1359,t4219]) ).
cnf(t116047,plain,
meet(X1,meet(X2,join(one,complement(X1)))) = meet(X1,meet(X2,join(X1,meet(join(one,complement(X1)),join(X1,X3))))),
inference(step,[status(thm)],[t4243,t23]) ).
cnf(t116048,plain,
meet(X1,meet(X2,join(one,complement(X1)))) = meet(X1,X2),
inference(step,[status(thm)],[t116047,t161]) ).
cnf(t4253,plain,
meet(X1,meet(X2,join(one,complement(X1)))) = meet(X1,X2),
inference(orient,[status(thm)],[t116048]) ).
cnf(t4261,plain,
meet(X1,meet(X2,join(one,complement(X1)))) = meet(X1,join(meet(X2,join(one,complement(X1))),meet(X1,X2))),
inference(cp,[status(thm)],[t307,t4253]) ).
cnf(t116061,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(one,complement(X1))),meet(X1,X2))),
inference(step,[status(thm)],[t4261,t4253]) ).
cnf(t116062,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(one,complement(X1))))),
inference(step,[status(thm)],[t116061,t63]) ).
cnf(t4725,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(one,complement(X1))))) = meet(X1,X2),
inference(orient,[status(thm)],[t116062]) ).
cnf(t4784,plain,
meet(X1,meet(X2,complement(X1))) = meet(X1,join(zero,meet(meet(X2,complement(X1)),join(one,complement(X1))))),
inference(cp,[status(thm)],[t4725,t146]) ).
cnf(t116109,plain,
zero = meet(X1,join(zero,meet(meet(X2,complement(X1)),join(one,complement(X1))))),
inference(step,[status(thm)],[t4784,t146]) ).
cnf(t5501,plain,
meet(X1,join(zero,meet(meet(X2,complement(X1)),join(one,complement(X1))))) = zero,
inference(orient,[status(thm)],[t116109]) ).
cnf(t6019,plain,
zero = meet(complement(meet(X1,complement(X2))),join(meet(X1,complement(X2)),meet(X3,zero))),
inference(cp,[status(thm)],[t5985,t5501]) ).
cnf(t116173,plain,
zero = meet(complement(meet(X1,complement(X2))),join(meet(X1,complement(X2)),zero)),
inference(step,[status(thm)],[t6019,t113]) ).
cnf(t116174,plain,
zero = meet(complement(meet(X1,complement(X2))),meet(X1,complement(X2))),
inference(step,[status(thm)],[t116173,t91]) ).
cnf(t116175,plain,
zero = meet(complement(X2),meet(complement(meet(X1,complement(X2))),X1)),
inference(step,[status(thm)],[t116174,t26]) ).
cnf(t116176,plain,
zero = meet(X1,meet(complement(X2),complement(meet(X1,complement(X2))))),
inference(step,[status(thm)],[t116175,t26]) ).
cnf(t6136,plain,
meet(X1,meet(complement(X2),complement(meet(X1,complement(X2))))) = zero,
inference(orient,[status(thm)],[t116176]) ).
cnf(t6139,plain,
zero = meet(X1,meet(X2,complement(meet(X1,complement(complement(X2)))))),
inference(cp,[status(thm)],[t6136,t839]) ).
cnf(t116177,plain,
zero = meet(X1,meet(X2,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t6139,t839]) ).
cnf(t6167,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t116177]) ).
cnf(t6208,plain,
meet(X1,join(meet(X2,complement(meet(X1,X2))),complement(X1))) = meet(X1,join(meet(X2,complement(meet(X1,X2))),meet(X1,join(complement(X1),zero)))),
inference(cp,[status(thm)],[t3993,t6167]) ).
cnf(t116188,plain,
meet(X1,join(meet(X2,complement(meet(X1,X2))),complement(X1))) = meet(X1,join(meet(X2,complement(meet(X1,X2))),meet(X1,complement(X1)))),
inference(step,[status(thm)],[t6208,t91]) ).
cnf(t116189,plain,
meet(X1,join(meet(X2,complement(meet(X1,X2))),complement(X1))) = meet(X1,join(meet(X2,complement(meet(X1,X2))),zero)),
inference(step,[status(thm)],[t116188,t57]) ).
cnf(t116190,plain,
meet(X1,join(meet(X2,complement(meet(X1,X2))),complement(X1))) = meet(X1,meet(X2,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t116189,t91]) ).
cnf(t116191,plain,
meet(X1,join(meet(X2,complement(meet(X1,X2))),complement(X1))) = zero,
inference(step,[status(thm)],[t116190,t6167]) ).
cnf(t116192,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = zero,
inference(step,[status(thm)],[t116191,t63]) ).
cnf(t6449,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t116192]) ).
cnf(t6450,plain,
zero = meet(complement(X1),join(X1,meet(X2,complement(meet(complement(X1),X2))))),
inference(cp,[status(thm)],[t6449,t839]) ).
cnf(t116215,plain,
zero = meet(complement(X1),join(X1,meet(X2,complement(meet(X2,complement(X1)))))),
inference(step,[status(thm)],[t6450,t23]) ).
cnf(t7078,plain,
meet(complement(X1),join(X1,meet(X2,complement(meet(X2,complement(X1)))))) = zero,
inference(orient,[status(thm)],[t116215]) ).
cnf(t7088,plain,
complement(X1) = ifeq(zero,zero,complement(join(X1,meet(X2,complement(meet(X2,complement(X1)))))),complement(X1)),
inference(cp,[status(thm)],[t1333,t7078]) ).
cnf(t116216,plain,
complement(X1) = complement(join(X1,meet(X2,complement(meet(X2,complement(X1)))))),
inference(step,[status(thm)],[t7088,t17]) ).
cnf(t7121,plain,
complement(join(X1,meet(X2,complement(meet(X2,complement(X1)))))) = complement(X1),
inference(orient,[status(thm)],[t116216]) ).
cnf(t7127,plain,
join(X1,meet(X2,complement(meet(X2,complement(X1))))) = complement(complement(X1)),
inference(cp,[status(thm)],[t839,t7121]) ).
cnf(t116217,plain,
join(X1,meet(X2,complement(meet(X2,complement(X1))))) = X1,
inference(step,[status(thm)],[t7127,t839]) ).
cnf(t7280,plain,
join(X1,meet(X2,complement(meet(X2,complement(X1))))) = X1,
inference(orient,[status(thm)],[t116217]) ).
cnf(t115,plain,
zero = ifeq(zero,zero,ifeq(join(X1,zero),one,complement(X1),zero),zero),
inference(cp,[status(thm)],[t18,t113]) ).
cnf(t115576,plain,
zero = ifeq(join(X1,zero),one,complement(X1),zero),
inference(step,[status(thm)],[t115,t17]) ).
cnf(t115577,plain,
zero = ifeq(X1,one,complement(X1),zero),
inference(step,[status(thm)],[t115576,t91]) ).
cnf(t134,plain,
ifeq(X1,one,complement(X1),zero) = zero,
inference(orient,[status(thm)],[t115577]) ).
cnf(t843,plain,
zero = ifeq(complement(X1),one,X1,zero),
inference(cp,[status(thm)],[t134,t839]) ).
cnf(t865,plain,
ifeq(complement(X1),one,X1,zero) = zero,
inference(orient,[status(thm)],[t843]) ).
cnf(t7282,plain,
complement(X1) = join(complement(X1),meet(X2,complement(meet(X2,X1)))),
inference(cp,[status(thm)],[t7280,t839]) ).
cnf(t116219,plain,
complement(X1) = join(complement(X1),meet(X2,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t7282,t23]) ).
cnf(t7325,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = complement(X1),
inference(orient,[status(thm)],[t116219]) ).
cnf(t4048,plain,
meet(X1,join(meet(X2,complement(X1)),complement(X1))) = meet(X1,join(meet(X2,complement(X1)),meet(X1,join(complement(X1),zero)))),
inference(cp,[status(thm)],[t3993,t146]) ).
cnf(t116017,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = meet(X1,join(meet(X2,complement(X1)),meet(X1,join(complement(X1),zero)))),
inference(step,[status(thm)],[t4048,t63]) ).
cnf(t116018,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = meet(X1,join(meet(X2,complement(X1)),meet(X1,complement(X1)))),
inference(step,[status(thm)],[t116017,t91]) ).
cnf(t116019,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = meet(X1,join(meet(X2,complement(X1)),zero)),
inference(step,[status(thm)],[t116018,t57]) ).
cnf(t116020,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = meet(X1,meet(X2,complement(X1))),
inference(step,[status(thm)],[t116019,t91]) ).
cnf(t116021,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = zero,
inference(step,[status(thm)],[t116020,t146]) ).
cnf(t4096,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t116021]) ).
cnf(t7349,plain,
complement(X1) = join(complement(X1),meet(join(complement(X1),meet(X2,complement(X1))),complement(zero))),
inference(cp,[status(thm)],[t7325,t4096]) ).
cnf(t131,plain,
one = ifeq(meet(X1,one),zero,ifeq(one,one,complement(X1),one),one),
inference(cp,[status(thm)],[t18,t129]) ).
cnf(t115578,plain,
one = ifeq(X1,zero,ifeq(one,one,complement(X1),one),one),
inference(step,[status(thm)],[t131,t96]) ).
cnf(t115579,plain,
one = ifeq(X1,zero,complement(X1),one),
inference(step,[status(thm)],[t115578,t17]) ).
cnf(t138,plain,
ifeq(X1,zero,complement(X1),one) = one,
inference(orient,[status(thm)],[t115579]) ).
cnf(t139,plain,
one = complement(zero),
inference(cp,[status(thm)],[t138,t17]) ).
cnf(t141,plain,
complement(zero) = one,
inference(orient,[status(thm)],[t139]) ).
cnf(t116226,plain,
complement(X1) = join(complement(X1),meet(join(complement(X1),meet(X2,complement(X1))),one)),
inference(step,[status(thm)],[t7349,t141]) ).
cnf(t116227,plain,
complement(X1) = join(complement(X1),join(complement(X1),meet(X2,complement(X1)))),
inference(step,[status(thm)],[t116226,t96]) ).
cnf(t116228,plain,
complement(X1) = join(complement(X1),meet(X2,complement(X1))),
inference(step,[status(thm)],[t116227,t119]) ).
cnf(t7457,plain,
join(complement(X1),meet(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t116228]) ).
cnf(t55,plain,
meet(X1,meet(join(X2,meet(X1,join(X3,meet(X1,join(X2,meet(X1,X3)))))),Y3)) = meet(Y3,meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t26,t46]) ).
cnf(t116916,plain,
meet(X1,meet(Y3,join(X2,meet(X1,join(X3,meet(X1,join(X2,meet(X1,X3)))))))) = meet(Y3,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t55,t23]) ).
cnf(t116917,plain,
meet(X1,meet(Y3,join(X2,meet(X1,join(X3,meet(X1,join(X2,meet(X1,X3)))))))) = meet(X1,meet(join(X2,X3),Y3)),
inference(step,[status(thm)],[t116916,t26]) ).
cnf(t116918,plain,
meet(X1,meet(Y3,join(X2,meet(X1,join(X3,meet(X1,join(X2,meet(X1,X3)))))))) = meet(X1,meet(Y3,join(X2,X3))),
inference(step,[status(thm)],[t116917,t23]) ).
cnf(t25373,plain,
meet(X1,meet(X2,join(X3,meet(X1,join(Y3,meet(X1,join(X3,meet(X1,Y3)))))))) = meet(X1,meet(X2,join(X3,Y3))),
inference(orient,[status(thm)],[t116918]) ).
cnf(t6206,plain,
meet(X1,meet(meet(X2,complement(meet(X1,X2))),X3)) = meet(X1,meet(X3,join(zero,zero))),
inference(cp,[status(thm)],[t323,t6167]) ).
cnf(t116178,plain,
meet(X1,meet(X3,meet(X2,complement(meet(X1,X2))))) = meet(X1,meet(X3,join(zero,zero))),
inference(step,[status(thm)],[t6206,t23]) ).
cnf(t116179,plain,
meet(X1,meet(X2,meet(complement(meet(X1,X2)),X3))) = meet(X1,meet(X3,join(zero,zero))),
inference(step,[status(thm)],[t116178,t26]) ).
cnf(t116180,plain,
meet(X1,meet(X2,meet(X3,complement(meet(X1,X2))))) = meet(X1,meet(X3,join(zero,zero))),
inference(step,[status(thm)],[t116179,t23]) ).
cnf(t116181,plain,
meet(X1,meet(X2,meet(X3,complement(meet(X1,X2))))) = meet(X1,meet(X3,zero)),
inference(step,[status(thm)],[t116180,t91]) ).
cnf(t116182,plain,
meet(X1,meet(X2,meet(X3,complement(meet(X1,X2))))) = meet(X1,zero),
inference(step,[status(thm)],[t116181,t113]) ).
cnf(t116183,plain,
meet(X1,meet(X2,meet(X3,complement(meet(X1,X2))))) = zero,
inference(step,[status(thm)],[t116182,t113]) ).
cnf(t6222,plain,
meet(X1,meet(X2,meet(X3,complement(meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t116183]) ).
cnf(t6223,plain,
zero = meet(X1,meet(meet(X2,complement(meet(X3,X1))),X3)),
inference(cp,[status(thm)],[t6222,t26]) ).
cnf(t116184,plain,
zero = meet(X1,meet(X3,meet(X2,complement(meet(X3,X1))))),
inference(step,[status(thm)],[t6223,t23]) ).
cnf(t116185,plain,
zero = meet(X1,meet(X2,meet(complement(meet(X3,X1)),X3))),
inference(step,[status(thm)],[t116184,t26]) ).
cnf(t116186,plain,
zero = meet(X1,meet(X2,meet(X3,complement(meet(X3,X1))))),
inference(step,[status(thm)],[t116185,t23]) ).
cnf(t116187,plain,
zero = meet(X1,meet(X2,meet(X3,complement(meet(X1,X3))))),
inference(step,[status(thm)],[t116186,t23]) ).
cnf(t6351,plain,
meet(X1,meet(X2,meet(X3,complement(meet(X1,X3))))) = zero,
inference(orient,[status(thm)],[t116187]) ).
cnf(t7397,plain,
complement(X1) = join(complement(X1),meet(meet(X2,meet(X3,complement(meet(X1,X3)))),complement(zero))),
inference(cp,[status(thm)],[t7325,t6351]) ).
cnf(t116260,plain,
complement(X1) = join(complement(X1),meet(meet(X2,meet(X3,complement(meet(X1,X3)))),one)),
inference(step,[status(thm)],[t7397,t141]) ).
cnf(t116261,plain,
complement(X1) = join(complement(X1),meet(X2,meet(X3,complement(meet(X1,X3))))),
inference(step,[status(thm)],[t116260,t96]) ).
cnf(t8269,plain,
join(complement(X1),meet(X2,meet(X3,complement(meet(X1,X3))))) = complement(X1),
inference(orient,[status(thm)],[t116261]) ).
cnf(t151,plain,
meet(X1,join(X2,meet(X3,complement(X1)))) = meet(X1,join(X2,meet(X1,join(meet(X3,complement(X1)),meet(X1,join(X2,zero)))))),
inference(cp,[status(thm)],[t46,t146]) ).
cnf(t116893,plain,
meet(X1,join(X2,meet(X3,complement(X1)))) = meet(X1,join(X2,meet(X1,join(meet(X3,complement(X1)),meet(X1,X2))))),
inference(step,[status(thm)],[t151,t91]) ).
cnf(t116894,plain,
meet(X1,join(X2,meet(X3,complement(X1)))) = meet(X1,join(X2,meet(X1,join(meet(X1,X2),meet(X3,complement(X1)))))),
inference(step,[status(thm)],[t116893,t63]) ).
cnf(t24338,plain,
meet(X1,join(X2,meet(X1,join(meet(X1,X2),meet(X3,complement(X1)))))) = meet(X1,join(X2,meet(X3,complement(X1)))),
inference(orient,[status(thm)],[t116894]) ).
cnf(t24410,plain,
meet(X1,join(meet(X2,complement(X1)),meet(X3,complement(X1)))) = meet(X1,join(meet(X2,complement(X1)),meet(X1,join(zero,meet(X3,complement(X1)))))),
inference(cp,[status(thm)],[t24338,t146]) ).
cnf(t116895,plain,
meet(X1,join(meet(X2,complement(X1)),meet(X3,complement(X1)))) = meet(X1,join(meet(X2,complement(X1)),zero)),
inference(step,[status(thm)],[t24410,t541]) ).
cnf(t116896,plain,
meet(X1,join(meet(X2,complement(X1)),meet(X3,complement(X1)))) = meet(X1,meet(X2,complement(X1))),
inference(step,[status(thm)],[t116895,t91]) ).
cnf(t116897,plain,
meet(X1,join(meet(X2,complement(X1)),meet(X3,complement(X1)))) = zero,
inference(step,[status(thm)],[t116896,t146]) ).
cnf(t24546,plain,
meet(X1,join(meet(X2,complement(X1)),meet(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t116897]) ).
cnf(t24570,plain,
complement(X1) = join(complement(X1),meet(X2,meet(join(meet(X3,complement(X1)),meet(Y3,complement(X1))),complement(zero)))),
inference(cp,[status(thm)],[t8269,t24546]) ).
cnf(t117109,plain,
complement(X1) = join(complement(X1),meet(X2,meet(join(meet(X3,complement(X1)),meet(Y3,complement(X1))),one))),
inference(step,[status(thm)],[t24570,t141]) ).
cnf(t117110,plain,
complement(X1) = join(complement(X1),meet(X2,join(meet(X3,complement(X1)),meet(Y3,complement(X1))))),
inference(step,[status(thm)],[t117109,t96]) ).
cnf(t33847,plain,
join(complement(X1),meet(X2,join(meet(X3,complement(X1)),meet(Y3,complement(X1))))) = complement(X1),
inference(orient,[status(thm)],[t117110]) ).
cnf(t33894,plain,
meet(X1,join(meet(X2,complement(X3)),complement(X3))) = meet(X1,join(meet(X2,complement(X3)),meet(X1,complement(X3)))),
inference(cp,[status(thm)],[t46,t33847]) ).
cnf(t117111,plain,
meet(X1,join(complement(X3),meet(X2,complement(X3)))) = meet(X1,join(meet(X2,complement(X3)),meet(X1,complement(X3)))),
inference(step,[status(thm)],[t33894,t63]) ).
cnf(t117112,plain,
meet(X1,complement(X3)) = meet(X1,join(meet(X2,complement(X3)),meet(X1,complement(X3)))),
inference(step,[status(thm)],[t117111,t7457]) ).
cnf(t117113,plain,
meet(X1,complement(X3)) = meet(X1,join(meet(X1,complement(X3)),meet(X2,complement(X3)))),
inference(step,[status(thm)],[t117112,t63]) ).
cnf(t33912,plain,
meet(X1,join(meet(X1,complement(X2)),meet(X3,complement(X2)))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t117113]) ).
cnf(t33915,plain,
meet(X1,complement(complement(X2))) = meet(X1,join(meet(X1,X2),meet(X3,complement(complement(X2))))),
inference(cp,[status(thm)],[t33912,t839]) ).
cnf(t117114,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X3,complement(complement(X2))))),
inference(step,[status(thm)],[t33915,t839]) ).
cnf(t117115,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X3,X2))),
inference(step,[status(thm)],[t117114,t839]) ).
cnf(t117116,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t117115,t23]) ).
cnf(t34062,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t117116]) ).
cnf(t34323,plain,
meet(X1,meet(X2,join(meet(X2,X1),X3))) = meet(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t25373,t34062]) ).
cnf(t117117,plain,
meet(X1,meet(X2,join(X3,meet(X2,X1)))) = meet(X1,meet(X2,X1)),
inference(step,[status(thm)],[t34323,t63]) ).
cnf(t117118,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,meet(X2,X1)),
inference(step,[status(thm)],[t117117,t23]) ).
cnf(t117119,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,meet(X1,X2)),
inference(step,[status(thm)],[t117118,t26]) ).
cnf(t117120,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(step,[status(thm)],[t117119,t102]) ).
cnf(t34350,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t117120]) ).
cnf(t34403,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,meet(complement(meet(X2,X1)),complement(X2))),
inference(cp,[status(thm)],[t34350,t7325]) ).
cnf(t117121,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,meet(complement(meet(X2,X1)),complement(X2))),
inference(step,[status(thm)],[t34403,t23]) ).
cnf(t117122,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,meet(complement(X2),complement(meet(X2,X1)))),
inference(step,[status(thm)],[t117121,t23]) ).
cnf(t117123,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,meet(complement(X2),complement(meet(X1,X2)))),
inference(step,[status(thm)],[t117122,t23]) ).
cnf(t34655,plain,
meet(X1,meet(complement(X2),complement(meet(X1,X2)))) = meet(X1,complement(meet(X1,X2))),
inference(orient,[status(thm)],[t117123]) ).
cnf(t34741,plain,
meet(X1,complement(meet(X1,meet(X2,complement(X1))))) = meet(X1,meet(complement(meet(X2,complement(X1))),complement(zero))),
inference(cp,[status(thm)],[t34655,t146]) ).
cnf(t117124,plain,
meet(X1,complement(zero)) = meet(X1,meet(complement(meet(X2,complement(X1))),complement(zero))),
inference(step,[status(thm)],[t34741,t146]) ).
cnf(t117125,plain,
meet(X1,one) = meet(X1,meet(complement(meet(X2,complement(X1))),complement(zero))),
inference(step,[status(thm)],[t117124,t141]) ).
cnf(t117126,plain,
X1 = meet(X1,meet(complement(meet(X2,complement(X1))),complement(zero))),
inference(step,[status(thm)],[t117125,t96]) ).
cnf(t117127,plain,
X1 = meet(X1,meet(complement(zero),complement(meet(X2,complement(X1))))),
inference(step,[status(thm)],[t117126,t23]) ).
cnf(t117128,plain,
X1 = meet(X1,meet(one,complement(meet(X2,complement(X1))))),
inference(step,[status(thm)],[t117127,t141]) ).
cnf(t7472,plain,
meet(X1,complement(X2)) = meet(X1,join(meet(X1,complement(X2)),meet(one,complement(X2)))),
inference(cp,[status(thm)],[t2166,t7457]) ).
cnf(t8769,plain,
meet(X1,join(meet(X1,complement(X2)),meet(one,complement(X2)))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t7472]) ).
cnf(t8823,plain,
meet(X1,meet(join(meet(X1,complement(X2)),meet(one,complement(X2))),X3)) = meet(X3,meet(X1,complement(X2))),
inference(cp,[status(thm)],[t26,t8769]) ).
cnf(t116480,plain,
meet(X1,meet(X3,join(meet(X1,complement(X2)),meet(one,complement(X2))))) = meet(X3,meet(X1,complement(X2))),
inference(step,[status(thm)],[t8823,t23]) ).
cnf(t116481,plain,
meet(X1,meet(X3,join(meet(X1,complement(X2)),meet(one,complement(X2))))) = meet(X1,meet(complement(X2),X3)),
inference(step,[status(thm)],[t116480,t26]) ).
cnf(t116482,plain,
meet(X1,meet(X3,join(meet(X1,complement(X2)),meet(one,complement(X2))))) = meet(X1,meet(X3,complement(X2))),
inference(step,[status(thm)],[t116481,t23]) ).
cnf(t14817,plain,
meet(X1,meet(X2,join(meet(X1,complement(X3)),meet(one,complement(X3))))) = meet(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t116482]) ).
cnf(t14822,plain,
meet(one,meet(X1,complement(X2))) = meet(one,meet(X1,meet(one,complement(X2)))),
inference(cp,[status(thm)],[t14817,t15]) ).
cnf(t116483,plain,
meet(X1,meet(complement(X2),one)) = meet(one,meet(X1,meet(one,complement(X2)))),
inference(step,[status(thm)],[t14822,t26]) ).
cnf(t116484,plain,
meet(X1,complement(X2)) = meet(one,meet(X1,meet(one,complement(X2)))),
inference(step,[status(thm)],[t116483,t96]) ).
cnf(t116485,plain,
meet(X1,complement(X2)) = meet(X1,meet(meet(one,complement(X2)),one)),
inference(step,[status(thm)],[t116484,t26]) ).
cnf(t116486,plain,
meet(X1,complement(X2)) = meet(X1,meet(one,complement(X2))),
inference(step,[status(thm)],[t116485,t96]) ).
cnf(t14895,plain,
meet(X1,meet(one,complement(X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t116486]) ).
cnf(t14896,plain,
meet(meet(one,complement(X1)),complement(X1)) = meet(one,complement(X1)),
inference(cp,[status(thm)],[t14895,t13]) ).
cnf(t116487,plain,
meet(complement(X1),meet(one,complement(X1))) = meet(one,complement(X1)),
inference(step,[status(thm)],[t14896,t23]) ).
cnf(t116488,plain,
meet(complement(X1),complement(X1)) = meet(one,complement(X1)),
inference(step,[status(thm)],[t116487,t14895]) ).
cnf(t116489,plain,
complement(X1) = meet(one,complement(X1)),
inference(step,[status(thm)],[t116488,t13]) ).
cnf(t14956,plain,
meet(one,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t116489]) ).
cnf(t117129,plain,
X1 = meet(X1,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t117128,t14956]) ).
cnf(t34893,plain,
meet(X1,complement(meet(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t117129]) ).
cnf(t34904,plain,
complement(meet(X1,complement(X2))) = join(complement(meet(X1,complement(X2))),X2),
inference(cp,[status(thm)],[t7457,t34893]) ).
cnf(t117138,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(meet(X1,complement(X2)))),
inference(step,[status(thm)],[t34904,t63]) ).
cnf(t35391,plain,
join(X1,complement(meet(X2,complement(X1)))) = complement(meet(X2,complement(X1))),
inference(orient,[status(thm)],[t117138]) ).
cnf(t35396,plain,
complement(meet(X1,complement(complement(X2)))) = join(complement(X2),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t35391,t839]) ).
cnf(t117139,plain,
complement(meet(X1,X2)) = join(complement(X2),complement(meet(X1,X2))),
inference(step,[status(thm)],[t35396,t839]) ).
cnf(t35442,plain,
join(complement(X1),complement(meet(X2,X1))) = complement(meet(X2,X1)),
inference(orient,[status(thm)],[t117139]) ).
cnf(t34895,plain,
complement(X1) = meet(complement(X1),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t34893,t839]) ).
cnf(t117130,plain,
complement(X1) = meet(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t34895,t23]) ).
cnf(t35062,plain,
meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t117130]) ).
cnf(t35162,plain,
meet(complement(X1),join(X2,complement(meet(X1,X3)))) = meet(complement(X1),join(X2,meet(complement(X1),join(complement(meet(X1,X3)),meet(complement(X1),join(X2,complement(X1))))))),
inference(cp,[status(thm)],[t46,t35062]) ).
cnf(t24413,plain,
meet(X1,join(join(X1,X2),meet(X3,complement(X1)))) = meet(X1,join(join(X1,X2),meet(X1,join(X1,meet(X3,complement(X1)))))),
inference(cp,[status(thm)],[t24338,t14]) ).
cnf(t116912,plain,
meet(X1,join(join(X1,X2),meet(X3,complement(X1)))) = meet(X1,join(join(X1,X2),X1)),
inference(step,[status(thm)],[t24413,t14]) ).
cnf(t116913,plain,
meet(X1,join(join(X1,X2),meet(X3,complement(X1)))) = meet(X1,join(X1,join(X1,X2))),
inference(step,[status(thm)],[t116912,t63]) ).
cnf(t116914,plain,
meet(X1,join(join(X1,X2),meet(X3,complement(X1)))) = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t116913,t119]) ).
cnf(t116915,plain,
meet(X1,join(join(X1,X2),meet(X3,complement(X1)))) = X1,
inference(step,[status(thm)],[t116914,t14]) ).
cnf(t25290,plain,
meet(X1,join(join(X1,X2),meet(X3,complement(X1)))) = X1,
inference(orient,[status(thm)],[t116915]) ).
cnf(t25298,plain,
complement(X1) = meet(complement(X1),join(join(complement(X1),X2),meet(X3,X1))),
inference(cp,[status(thm)],[t25290,t839]) ).
cnf(t116940,plain,
complement(X1) = meet(complement(X1),join(meet(X3,X1),join(complement(X1),X2))),
inference(step,[status(thm)],[t25298,t63]) ).
cnf(t116941,plain,
complement(X1) = meet(complement(X1),join(X2,join(meet(X3,X1),complement(X1)))),
inference(step,[status(thm)],[t116940,t67]) ).
cnf(t116942,plain,
complement(X1) = meet(complement(X1),join(X2,join(complement(X1),meet(X3,X1)))),
inference(step,[status(thm)],[t116941,t63]) ).
cnf(t116943,plain,
complement(X1) = meet(complement(X1),join(X2,join(complement(X1),meet(X1,X3)))),
inference(step,[status(thm)],[t116942,t23]) ).
cnf(t26599,plain,
meet(complement(X1),join(X2,join(complement(X1),meet(X1,X3)))) = complement(X1),
inference(orient,[status(thm)],[t116943]) ).
cnf(t6432,plain,
zero = meet(X1,meet(X2,meet(meet(X3,meet(Y3,complement(meet(X1,Y3)))),complement(zero)))),
inference(cp,[status(thm)],[t6351,t6351]) ).
cnf(t116213,plain,
zero = meet(X1,meet(X2,meet(meet(X3,meet(Y3,complement(meet(X1,Y3)))),one))),
inference(step,[status(thm)],[t6432,t141]) ).
cnf(t116214,plain,
zero = meet(X1,meet(X2,meet(X3,meet(Y3,complement(meet(X1,Y3)))))),
inference(step,[status(thm)],[t116213,t96]) ).
cnf(t6950,plain,
meet(X1,meet(X2,meet(X3,meet(Y3,complement(meet(X1,Y3)))))) = zero,
inference(orient,[status(thm)],[t116214]) ).
cnf(t7329,plain,
complement(X1) = join(complement(X1),meet(meet(X2,meet(X3,meet(Y3,complement(meet(X1,Y3))))),complement(zero))),
inference(cp,[status(thm)],[t7325,t6950]) ).
cnf(t116281,plain,
complement(X1) = join(complement(X1),meet(meet(X2,meet(X3,meet(Y3,complement(meet(X1,Y3))))),one)),
inference(step,[status(thm)],[t7329,t141]) ).
cnf(t116282,plain,
complement(X1) = join(complement(X1),meet(X2,meet(X3,meet(Y3,complement(meet(X1,Y3)))))),
inference(step,[status(thm)],[t116281,t96]) ).
cnf(t8934,plain,
join(complement(X1),meet(X2,meet(X3,meet(Y3,complement(meet(X1,Y3)))))) = complement(X1),
inference(orient,[status(thm)],[t116282]) ).
cnf(t8935,plain,
complement(complement(X1)) = join(X1,meet(X2,meet(X3,meet(Y3,complement(meet(complement(X1),Y3)))))),
inference(cp,[status(thm)],[t8934,t839]) ).
cnf(t116283,plain,
X1 = join(X1,meet(X2,meet(X3,meet(Y3,complement(meet(complement(X1),Y3)))))),
inference(step,[status(thm)],[t8935,t839]) ).
cnf(t116284,plain,
X1 = join(X1,meet(X2,meet(X3,meet(Y3,complement(meet(Y3,complement(X1))))))),
inference(step,[status(thm)],[t116283,t23]) ).
cnf(t9050,plain,
join(X1,meet(X2,meet(X3,meet(Y3,complement(meet(Y3,complement(X1))))))) = X1,
inference(orient,[status(thm)],[t116284]) ).
cnf(t9051,plain,
X1 = join(X1,meet(X2,meet(meet(X3,complement(meet(X3,complement(X1)))),Y3))),
inference(cp,[status(thm)],[t9050,t26]) ).
cnf(t116285,plain,
X1 = join(X1,meet(X2,meet(Y3,meet(X3,complement(meet(X3,complement(X1))))))),
inference(step,[status(thm)],[t9051,t23]) ).
cnf(t116286,plain,
X1 = join(X1,meet(X2,meet(X3,meet(complement(meet(X3,complement(X1))),Y3)))),
inference(step,[status(thm)],[t116285,t26]) ).
cnf(t116287,plain,
X1 = join(X1,meet(X2,meet(X3,meet(Y3,complement(meet(X3,complement(X1))))))),
inference(step,[status(thm)],[t116286,t23]) ).
cnf(t9106,plain,
join(X1,meet(X2,meet(X3,meet(Y3,complement(meet(X3,complement(X1))))))) = X1,
inference(orient,[status(thm)],[t116287]) ).
cnf(t9107,plain,
X1 = join(X1,meet(X2,meet(meet(X3,complement(meet(X2,complement(X1)))),Y3))),
inference(cp,[status(thm)],[t9106,t26]) ).
cnf(t116288,plain,
X1 = join(X1,meet(X2,meet(Y3,meet(X3,complement(meet(X2,complement(X1))))))),
inference(step,[status(thm)],[t9107,t23]) ).
cnf(t116289,plain,
X1 = join(X1,meet(X2,meet(X3,meet(complement(meet(X2,complement(X1))),Y3)))),
inference(step,[status(thm)],[t116288,t26]) ).
cnf(t116290,plain,
X1 = join(X1,meet(X2,meet(X3,meet(Y3,complement(meet(X2,complement(X1))))))),
inference(step,[status(thm)],[t116289,t23]) ).
cnf(t9161,plain,
join(X1,meet(X2,meet(X3,meet(Y3,complement(meet(X2,complement(X1))))))) = X1,
inference(orient,[status(thm)],[t116290]) ).
cnf(t9211,plain,
join(X1,join(meet(X2,meet(X3,meet(Y3,complement(meet(X2,complement(X1)))))),Y4)) = join(Y4,X1),
inference(cp,[status(thm)],[t67,t9161]) ).
cnf(t116622,plain,
join(X1,join(Y4,meet(X2,meet(X3,meet(Y3,complement(meet(X2,complement(X1)))))))) = join(Y4,X1),
inference(step,[status(thm)],[t9211,t63]) ).
cnf(t116623,plain,
join(X1,join(Y4,meet(X2,meet(X3,meet(Y3,complement(meet(X2,complement(X1)))))))) = join(X1,Y4),
inference(step,[status(thm)],[t116622,t63]) ).
cnf(t16339,plain,
join(X1,join(X2,meet(X3,meet(Y3,meet(Y4,complement(meet(X3,complement(X1)))))))) = join(X1,X2),
inference(orient,[status(thm)],[t116623]) ).
cnf(t26601,plain,
complement(X1) = meet(complement(X1),join(X2,complement(X1))),
inference(cp,[status(thm)],[t26599,t16339]) ).
cnf(t26774,plain,
meet(complement(X1),join(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t26601]) ).
cnf(t117189,plain,
meet(complement(X1),join(X2,complement(meet(X1,X3)))) = meet(complement(X1),join(X2,meet(complement(X1),join(complement(meet(X1,X3)),complement(X1))))),
inference(step,[status(thm)],[t35162,t26774]) ).
cnf(t117190,plain,
meet(complement(X1),join(X2,complement(meet(X1,X3)))) = meet(complement(X1),join(X2,meet(complement(X1),join(complement(X1),complement(meet(X1,X3)))))),
inference(step,[status(thm)],[t117189,t63]) ).
cnf(t35071,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t7457,t35062]) ).
cnf(t117137,plain,
complement(meet(X1,X2)) = join(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t35071,t63]) ).
cnf(t35336,plain,
join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t117137]) ).
cnf(t117191,plain,
meet(complement(X1),join(X2,complement(meet(X1,X3)))) = meet(complement(X1),join(X2,meet(complement(X1),complement(meet(X1,X3))))),
inference(step,[status(thm)],[t117190,t35336]) ).
cnf(t117192,plain,
meet(complement(X1),join(X2,complement(meet(X1,X3)))) = meet(complement(X1),join(X2,complement(X1))),
inference(step,[status(thm)],[t117191,t35062]) ).
cnf(t117193,plain,
meet(complement(X1),join(X2,complement(meet(X1,X3)))) = complement(X1),
inference(step,[status(thm)],[t117192,t26774]) ).
cnf(t37472,plain,
meet(complement(X1),join(X2,complement(meet(X1,X3)))) = complement(X1),
inference(orient,[status(thm)],[t117193]) ).
cnf(t37473,plain,
complement(complement(X1)) = meet(X1,join(X2,complement(meet(complement(X1),X3)))),
inference(cp,[status(thm)],[t37472,t839]) ).
cnf(t117194,plain,
X1 = meet(X1,join(X2,complement(meet(complement(X1),X3)))),
inference(step,[status(thm)],[t37473,t839]) ).
cnf(t117195,plain,
X1 = meet(X1,join(X2,complement(meet(X3,complement(X1))))),
inference(step,[status(thm)],[t117194,t23]) ).
cnf(t37551,plain,
meet(X1,join(X2,complement(meet(X3,complement(X1))))) = X1,
inference(orient,[status(thm)],[t117195]) ).
cnf(t37562,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,complement(complement(X1)))),
inference(cp,[status(thm)],[t37551,t35062]) ).
cnf(t117196,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(step,[status(thm)],[t37562,t839]) ).
cnf(t117197,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t117196,t63]) ).
cnf(t37661,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t117197]) ).
cnf(t37739,plain,
complement(meet(meet(X1,X2),join(X1,X3))) = join(complement(join(X1,X3)),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t35442,t37661]) ).
cnf(t117249,plain,
complement(meet(X1,X2)) = join(complement(join(X1,X3)),complement(meet(X1,X2))),
inference(step,[status(thm)],[t37739,t37661]) ).
cnf(t117250,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(join(X1,X3))),
inference(step,[status(thm)],[t117249,t63]) ).
cnf(t42334,plain,
join(complement(meet(X1,X2)),complement(join(X1,X3))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t117250]) ).
cnf(t42441,plain,
one = join(join(X1,X2),complement(meet(X1,X3))),
inference(cp,[status(thm)],[t154,t42334]) ).
cnf(t42490,plain,
join(join(X1,X2),complement(meet(X1,X3))) = one,
inference(orient,[status(thm)],[t42441]) ).
cnf(t42499,plain,
one = join(join(X1,X2),complement(meet(X2,X3))),
inference(cp,[status(thm)],[t42490,t63]) ).
cnf(t42573,plain,
join(join(X1,X2),complement(meet(X2,X3))) = one,
inference(orient,[status(thm)],[t42499]) ).
cnf(t35493,plain,
complement(meet(complement(X1),join(X2,complement(X1)))) = join(complement(join(X2,complement(X1))),complement(complement(X1))),
inference(cp,[status(thm)],[t35442,t26774]) ).
cnf(t117140,plain,
complement(complement(X1)) = join(complement(join(X2,complement(X1))),complement(complement(X1))),
inference(step,[status(thm)],[t35493,t26774]) ).
cnf(t117141,plain,
X1 = join(complement(join(X2,complement(X1))),complement(complement(X1))),
inference(step,[status(thm)],[t117140,t839]) ).
cnf(t117142,plain,
X1 = join(complement(complement(X1)),complement(join(X2,complement(X1)))),
inference(step,[status(thm)],[t117141,t63]) ).
cnf(t117143,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(step,[status(thm)],[t117142,t839]) ).
cnf(t35558,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t117143]) ).
cnf(t42577,plain,
one = join(X1,complement(meet(complement(join(X2,complement(X1))),X3))),
inference(cp,[status(thm)],[t42573,t35558]) ).
cnf(t117268,plain,
one = join(X1,complement(meet(X3,complement(join(X2,complement(X1)))))),
inference(step,[status(thm)],[t42577,t23]) ).
cnf(t43348,plain,
join(X1,complement(meet(X2,complement(join(X3,complement(X1)))))) = one,
inference(orient,[status(thm)],[t117268]) ).
cnf(t24548,plain,
zero = meet(complement(X1),join(meet(X2,X1),meet(X3,complement(complement(X1))))),
inference(cp,[status(thm)],[t24546,t839]) ).
cnf(t116898,plain,
zero = meet(complement(X1),join(meet(X1,X2),meet(X3,complement(complement(X1))))),
inference(step,[status(thm)],[t24548,t23]) ).
cnf(t116899,plain,
zero = meet(complement(X1),join(meet(X1,X2),meet(X3,X1))),
inference(step,[status(thm)],[t116898,t839]) ).
cnf(t116900,plain,
zero = meet(complement(X1),join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t116899,t23]) ).
cnf(t24642,plain,
meet(complement(X1),join(meet(X1,X2),meet(X1,X3))) = zero,
inference(orient,[status(thm)],[t116900]) ).
cnf(t25378,plain,
meet(X1,meet(complement(X1),join(meet(X1,X2),X3))) = meet(X1,zero),
inference(cp,[status(thm)],[t25373,t24642]) ).
cnf(t116919,plain,
meet(X1,meet(complement(X1),join(X3,meet(X1,X2)))) = meet(X1,zero),
inference(step,[status(thm)],[t25378,t63]) ).
cnf(t116920,plain,
meet(X1,meet(complement(X1),join(X3,meet(X1,X2)))) = zero,
inference(step,[status(thm)],[t116919,t113]) ).
cnf(t25682,plain,
meet(X1,meet(complement(X1),join(X2,meet(X1,X3)))) = zero,
inference(orient,[status(thm)],[t116920]) ).
cnf(t172,plain,
meet(X1,meet(meet(X2,join(X1,X3)),Y3)) = meet(Y3,meet(X1,X2)),
inference(cp,[status(thm)],[t26,t161]) ).
cnf(t115611,plain,
meet(X1,meet(Y3,meet(X2,join(X1,X3)))) = meet(Y3,meet(X1,X2)),
inference(step,[status(thm)],[t172,t23]) ).
cnf(t115612,plain,
meet(X1,meet(X2,meet(join(X1,X3),Y3))) = meet(Y3,meet(X1,X2)),
inference(step,[status(thm)],[t115611,t26]) ).
cnf(t115613,plain,
meet(X1,meet(X2,meet(Y3,join(X1,X3)))) = meet(Y3,meet(X1,X2)),
inference(step,[status(thm)],[t115612,t23]) ).
cnf(t115614,plain,
meet(X1,meet(X2,meet(Y3,join(X1,X3)))) = meet(X2,meet(Y3,X1)),
inference(step,[status(thm)],[t115613,t26]) ).
cnf(t115615,plain,
meet(X1,meet(X2,meet(Y3,join(X1,X3)))) = meet(X1,meet(X2,Y3)),
inference(step,[status(thm)],[t115614,t26]) ).
cnf(t235,plain,
meet(X1,meet(X2,meet(X3,join(X1,Y3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t115615]) ).
cnf(t6186,plain,
zero = meet(X1,meet(meet(X2,meet(X3,join(X1,Y3))),complement(meet(X1,meet(X2,X3))))),
inference(cp,[status(thm)],[t6167,t235]) ).
cnf(t116630,plain,
zero = meet(X1,meet(complement(meet(X1,meet(X2,X3))),meet(X2,meet(X3,join(X1,Y3))))),
inference(step,[status(thm)],[t6186,t23]) ).
cnf(t116631,plain,
zero = meet(X1,meet(meet(X3,join(X1,Y3)),meet(complement(meet(X1,meet(X2,X3))),X2))),
inference(step,[status(thm)],[t116630,t26]) ).
cnf(t116632,plain,
zero = meet(X1,meet(X2,meet(meet(X3,join(X1,Y3)),complement(meet(X1,meet(X2,X3)))))),
inference(step,[status(thm)],[t116631,t26]) ).
cnf(t16534,plain,
meet(X1,meet(X2,meet(meet(X3,join(X1,Y3)),complement(meet(X1,meet(X2,X3)))))) = zero,
inference(orient,[status(thm)],[t116632]) ).
cnf(t16540,plain,
zero = meet(X1,meet(X2,meet(meet(X3,X1),complement(meet(X1,meet(X2,X3)))))),
inference(cp,[status(thm)],[t16534,t307]) ).
cnf(t116633,plain,
zero = meet(X1,meet(X2,meet(meet(X1,X3),complement(meet(X1,meet(X2,X3)))))),
inference(step,[status(thm)],[t16540,t23]) ).
cnf(t16693,plain,
meet(X1,meet(X2,meet(meet(X1,X3),complement(meet(X1,meet(X2,X3)))))) = zero,
inference(orient,[status(thm)],[t116633]) ).
cnf(t16769,plain,
complement(X1) = join(complement(X1),meet(meet(X2,meet(meet(X1,X3),complement(meet(X1,meet(X2,X3))))),complement(zero))),
inference(cp,[status(thm)],[t7325,t16693]) ).
cnf(t116634,plain,
complement(X1) = join(complement(X1),meet(meet(X2,meet(meet(X1,X3),complement(meet(X1,meet(X2,X3))))),one)),
inference(step,[status(thm)],[t16769,t141]) ).
cnf(t116635,plain,
complement(X1) = join(complement(X1),meet(X2,meet(meet(X1,X3),complement(meet(X1,meet(X2,X3)))))),
inference(step,[status(thm)],[t116634,t96]) ).
cnf(t16822,plain,
join(complement(X1),meet(X2,meet(meet(X1,X3),complement(meet(X1,meet(X2,X3)))))) = complement(X1),
inference(orient,[status(thm)],[t116635]) ).
cnf(t25711,plain,
zero = meet(X1,meet(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t25682,t16822]) ).
cnf(t25893,plain,
meet(X1,meet(complement(X1),complement(X2))) = zero,
inference(orient,[status(thm)],[t25711]) ).
cnf(t34665,plain,
meet(X1,complement(meet(X1,meet(complement(X1),complement(X2))))) = meet(X1,meet(complement(meet(complement(X1),complement(X2))),complement(zero))),
inference(cp,[status(thm)],[t34655,t25893]) ).
cnf(t117131,plain,
meet(X1,complement(zero)) = meet(X1,meet(complement(meet(complement(X1),complement(X2))),complement(zero))),
inference(step,[status(thm)],[t34665,t25893]) ).
cnf(t117132,plain,
meet(X1,one) = meet(X1,meet(complement(meet(complement(X1),complement(X2))),complement(zero))),
inference(step,[status(thm)],[t117131,t141]) ).
cnf(t117133,plain,
X1 = meet(X1,meet(complement(meet(complement(X1),complement(X2))),complement(zero))),
inference(step,[status(thm)],[t117132,t96]) ).
cnf(t117134,plain,
X1 = meet(X1,meet(complement(zero),complement(meet(complement(X1),complement(X2))))),
inference(step,[status(thm)],[t117133,t23]) ).
cnf(t117135,plain,
X1 = meet(X1,meet(one,complement(meet(complement(X1),complement(X2))))),
inference(step,[status(thm)],[t117134,t141]) ).
cnf(t117136,plain,
X1 = meet(X1,complement(meet(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t117135,t14956]) ).
cnf(t35175,plain,
meet(X1,complement(meet(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t117136]) ).
cnf(t35185,plain,
complement(meet(complement(X1),complement(X2))) = join(complement(meet(complement(X1),complement(X2))),X1),
inference(cp,[status(thm)],[t7457,t35175]) ).
cnf(t117235,plain,
complement(meet(complement(X1),complement(X2))) = join(X1,complement(meet(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t35185,t63]) ).
cnf(t40517,plain,
join(X1,complement(meet(complement(X1),complement(X2)))) = complement(meet(complement(X1),complement(X2))),
inference(orient,[status(thm)],[t117235]) ).
cnf(t43349,plain,
one = complement(meet(complement(X1),complement(join(X2,complement(X1))))),
inference(cp,[status(thm)],[t43348,t40517]) ).
cnf(t43394,plain,
complement(meet(complement(X1),complement(join(X2,complement(X1))))) = one,
inference(orient,[status(thm)],[t43349]) ).
cnf(t43405,plain,
zero = ifeq(one,one,meet(complement(X1),complement(join(X2,complement(X1)))),zero),
inference(cp,[status(thm)],[t865,t43394]) ).
cnf(t117269,plain,
zero = meet(complement(X1),complement(join(X2,complement(X1)))),
inference(step,[status(thm)],[t43405,t17]) ).
cnf(t43571,plain,
meet(complement(X1),complement(join(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t117269]) ).
cnf(t26822,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = meet(complement(X1),join(X2,meet(complement(X1),join(join(X3,complement(X1)),meet(complement(X1),join(X2,complement(X1))))))),
inference(cp,[status(thm)],[t46,t26774]) ).
cnf(t116944,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = meet(complement(X1),join(X2,meet(complement(X1),join(join(X3,complement(X1)),complement(X1))))),
inference(step,[status(thm)],[t26822,t26774]) ).
cnf(t116945,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = meet(complement(X1),join(X2,meet(complement(X1),join(complement(X1),join(X3,complement(X1)))))),
inference(step,[status(thm)],[t116944,t63]) ).
cnf(t116946,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = meet(complement(X1),join(X2,meet(complement(X1),join(X3,join(complement(X1),complement(X1)))))),
inference(step,[status(thm)],[t116945,t67]) ).
cnf(t116947,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = meet(complement(X1),join(X2,meet(complement(X1),join(X3,complement(X1))))),
inference(step,[status(thm)],[t116946,t15]) ).
cnf(t116948,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = meet(complement(X1),join(X2,complement(X1))),
inference(step,[status(thm)],[t116947,t26774]) ).
cnf(t116949,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = complement(X1),
inference(step,[status(thm)],[t116948,t26774]) ).
cnf(t26834,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t116949]) ).
cnf(t35498,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)],[t35442,t26834]) ).
cnf(t117167,plain,
complement(complement(X1)) = join(complement(join(X2,join(X3,complement(X1)))),complement(complement(X1))),
inference(step,[status(thm)],[t35498,t26834]) ).
cnf(t117168,plain,
X1 = join(complement(join(X2,join(X3,complement(X1)))),complement(complement(X1))),
inference(step,[status(thm)],[t117167,t839]) ).
cnf(t117169,plain,
X1 = join(complement(complement(X1)),complement(join(X2,join(X3,complement(X1))))),
inference(step,[status(thm)],[t117168,t63]) ).
cnf(t117170,plain,
X1 = join(X1,complement(join(X2,join(X3,complement(X1))))),
inference(step,[status(thm)],[t117169,t839]) ).
cnf(t36995,plain,
join(X1,complement(join(X2,join(X3,complement(X1))))) = X1,
inference(orient,[status(thm)],[t117170]) ).
cnf(t36999,plain,
join(X1,complement(X2)) = join(join(X1,complement(X2)),complement(join(X3,X2))),
inference(cp,[status(thm)],[t36995,t35558]) ).
cnf(t117246,plain,
join(X1,complement(X2)) = join(join(X1,complement(X2)),complement(join(X2,X3))),
inference(step,[status(thm)],[t36999,t63]) ).
cnf(t41687,plain,
join(join(X1,complement(X2)),complement(join(X2,X3))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t117246]) ).
cnf(t43577,plain,
zero = meet(complement(join(X1,X2)),complement(join(X3,complement(X1)))),
inference(cp,[status(thm)],[t43571,t41687]) ).
cnf(t45870,plain,
meet(complement(join(X1,X2)),complement(join(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t43577]) ).
cnf(t152,plain,
meet(X1,meet(meet(X2,complement(X1)),X3)) = meet(X3,zero),
inference(cp,[status(thm)],[t26,t146]) ).
cnf(t115590,plain,
meet(X1,meet(X3,meet(X2,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t152,t23]) ).
cnf(t115591,plain,
meet(X1,meet(X2,meet(complement(X1),X3))) = meet(X3,zero),
inference(step,[status(thm)],[t115590,t26]) ).
cnf(t115592,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t115591,t23]) ).
cnf(t115593,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(step,[status(thm)],[t115592,t113]) ).
cnf(t186,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t115593]) ).
cnf(t4042,plain,
meet(X1,join(meet(X2,meet(X3,complement(X1))),complement(X1))) = meet(X1,join(meet(X2,meet(X3,complement(X1))),meet(X1,join(complement(X1),zero)))),
inference(cp,[status(thm)],[t3993,t186]) ).
cnf(t116032,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = meet(X1,join(meet(X2,meet(X3,complement(X1))),meet(X1,join(complement(X1),zero)))),
inference(step,[status(thm)],[t4042,t63]) ).
cnf(t116033,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = meet(X1,join(meet(X1,join(complement(X1),zero)),meet(X2,meet(X3,complement(X1))))),
inference(step,[status(thm)],[t116032,t63]) ).
cnf(t116034,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = meet(X1,join(meet(X1,complement(X1)),meet(X2,meet(X3,complement(X1))))),
inference(step,[status(thm)],[t116033,t91]) ).
cnf(t116035,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = meet(X1,join(zero,meet(X2,meet(X3,complement(X1))))),
inference(step,[status(thm)],[t116034,t57]) ).
cnf(t392,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = meet(X1,join(zero,meet(meet(X2,meet(X3,complement(X1))),join(X1,Y3)))),
inference(cp,[status(thm)],[t388,t186]) ).
cnf(t115730,plain,
zero = meet(X1,join(zero,meet(meet(X2,meet(X3,complement(X1))),join(X1,Y3)))),
inference(step,[status(thm)],[t392,t186]) ).
cnf(t115731,plain,
zero = meet(X1,join(zero,meet(join(X1,Y3),meet(X2,meet(X3,complement(X1)))))),
inference(step,[status(thm)],[t115730,t23]) ).
cnf(t115732,plain,
zero = meet(X1,join(zero,meet(X2,meet(meet(X3,complement(X1)),join(X1,Y3))))),
inference(step,[status(thm)],[t115731,t26]) ).
cnf(t115733,plain,
zero = meet(X1,join(zero,meet(X2,meet(join(X1,Y3),meet(X3,complement(X1)))))),
inference(step,[status(thm)],[t115732,t23]) ).
cnf(t115734,plain,
zero = meet(X1,join(zero,meet(X2,meet(complement(X1),meet(join(X1,Y3),X3))))),
inference(step,[status(thm)],[t115733,t26]) ).
cnf(t115735,plain,
zero = meet(X1,join(zero,meet(X2,meet(X3,meet(complement(X1),join(X1,Y3)))))),
inference(step,[status(thm)],[t115734,t26]) ).
cnf(t888,plain,
meet(X1,join(zero,meet(X2,meet(X3,meet(complement(X1),join(X1,Y3)))))) = zero,
inference(orient,[status(thm)],[t115735]) ).
cnf(t899,plain,
zero = meet(X1,join(zero,meet(X2,meet(X3,meet(complement(X1),one))))),
inference(cp,[status(thm)],[t888,t197]) ).
cnf(t115736,plain,
zero = meet(X1,join(zero,meet(X2,meet(X3,complement(X1))))),
inference(step,[status(thm)],[t899,t96]) ).
cnf(t926,plain,
meet(X1,join(zero,meet(X2,meet(X3,complement(X1))))) = zero,
inference(orient,[status(thm)],[t115736]) ).
cnf(t116036,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = zero,
inference(step,[status(thm)],[t116035,t926]) ).
cnf(t4160,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = zero,
inference(orient,[status(thm)],[t116036]) ).
cnf(t7350,plain,
complement(X1) = join(complement(X1),meet(join(complement(X1),meet(X2,meet(X3,complement(X1)))),complement(zero))),
inference(cp,[status(thm)],[t7325,t4160]) ).
cnf(t116233,plain,
complement(X1) = join(complement(X1),meet(join(complement(X1),meet(X2,meet(X3,complement(X1)))),one)),
inference(step,[status(thm)],[t7350,t141]) ).
cnf(t116234,plain,
complement(X1) = join(complement(X1),join(complement(X1),meet(X2,meet(X3,complement(X1))))),
inference(step,[status(thm)],[t116233,t96]) ).
cnf(t116235,plain,
complement(X1) = join(complement(X1),meet(X2,meet(X3,complement(X1)))),
inference(step,[status(thm)],[t116234,t119]) ).
cnf(t7493,plain,
join(complement(X1),meet(X2,meet(X3,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t116235]) ).
cnf(t35099,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),meet(X3,complement(X1))),
inference(cp,[status(thm)],[t7493,t35062]) ).
cnf(t117236,plain,
complement(meet(X1,X2)) = join(meet(X3,complement(X1)),complement(meet(X1,X2))),
inference(step,[status(thm)],[t35099,t63]) ).
cnf(t40579,plain,
join(meet(X1,complement(X2)),complement(meet(X2,X3))) = complement(meet(X2,X3)),
inference(orient,[status(thm)],[t117236]) ).
cnf(t45891,plain,
zero = meet(complement(join(meet(X1,X2),X3)),complement(complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t45870,t40579]) ).
cnf(t117329,plain,
zero = meet(complement(join(meet(X1,X2),X3)),meet(X1,X2)),
inference(step,[status(thm)],[t45891,t839]) ).
cnf(t117330,plain,
zero = meet(X2,meet(complement(join(meet(X1,X2),X3)),X1)),
inference(step,[status(thm)],[t117329,t26]) ).
cnf(t117331,plain,
zero = meet(X1,meet(X2,complement(join(meet(X1,X2),X3)))),
inference(step,[status(thm)],[t117330,t26]) ).
cnf(t117332,plain,
zero = meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t117331,t63]) ).
cnf(t49258,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t117332]) ).
cnf(t35476,plain,
complement(meet(X1,join(X1,X2))) = join(complement(join(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t35442,t14]) ).
cnf(t117144,plain,
complement(X1) = join(complement(join(X1,X2)),complement(X1)),
inference(step,[status(thm)],[t35476,t14]) ).
cnf(t117145,plain,
complement(X1) = join(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t117144,t63]) ).
cnf(t35631,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t117145]) ).
cnf(t35640,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t26774,t35631]) ).
cnf(t117146,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t35640,t23]) ).
cnf(t35693,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t117146]) ).
cnf(t49261,plain,
zero = meet(X1,complement(join(X2,meet(X1,complement(X2))))),
inference(cp,[status(thm)],[t49258,t35693]) ).
cnf(t49547,plain,
meet(X1,complement(join(X2,meet(X1,complement(X2))))) = zero,
inference(orient,[status(thm)],[t49261]) ).
cnf(t49595,plain,
join(X1,meet(X2,complement(X1))) = join(join(X1,meet(X2,complement(X1))),meet(X2,complement(zero))),
inference(cp,[status(thm)],[t7280,t49547]) ).
cnf(t117393,plain,
join(X1,meet(X2,complement(X1))) = join(meet(X2,complement(zero)),join(X1,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t49595,t63]) ).
cnf(t117394,plain,
join(X1,meet(X2,complement(X1))) = join(meet(X2,complement(X1)),join(meet(X2,complement(zero)),X1)),
inference(step,[status(thm)],[t117393,t67]) ).
cnf(t117395,plain,
join(X1,meet(X2,complement(X1))) = join(X1,join(meet(X2,complement(X1)),meet(X2,complement(zero)))),
inference(step,[status(thm)],[t117394,t67]) ).
cnf(t117396,plain,
join(X1,meet(X2,complement(X1))) = join(X1,join(meet(X2,complement(X1)),meet(X2,one))),
inference(step,[status(thm)],[t117395,t141]) ).
cnf(t117397,plain,
join(X1,meet(X2,complement(X1))) = join(X1,join(meet(X2,complement(X1)),X2)),
inference(step,[status(thm)],[t117396,t96]) ).
cnf(t117398,plain,
join(X1,meet(X2,complement(X1))) = join(X1,join(X2,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t117397,t63]) ).
cnf(t117399,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(step,[status(thm)],[t117398,t16]) ).
cnf(t56688,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t117399]) ).
cnf(t56711,plain,
join(complement(X1),X2) = join(complement(X1),meet(X2,X1)),
inference(cp,[status(thm)],[t56688,t839]) ).
cnf(t117406,plain,
join(X2,complement(X1)) = join(complement(X1),meet(X2,X1)),
inference(step,[status(thm)],[t56711,t63]) ).
cnf(t117407,plain,
join(X2,complement(X1)) = join(complement(X1),meet(X1,X2)),
inference(step,[status(thm)],[t117406,t23]) ).
cnf(t56803,plain,
join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t117407]) ).
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(t116049,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(t4279,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)],[t116049]) ).
cnf(t57062,plain,
meet(X1,X2) = ifeq(meet(X1,meet(X2,complement(X1))),zero,ifeq(join(X2,complement(X1)),one,complement(complement(X1)),meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t4279,t56803]) ).
cnf(t117532,plain,
meet(X1,X2) = ifeq(zero,zero,ifeq(join(X2,complement(X1)),one,complement(complement(X1)),meet(X1,X2)),meet(X1,X2)),
inference(step,[status(thm)],[t57062,t146]) ).
cnf(t117533,plain,
meet(X1,X2) = ifeq(join(X2,complement(X1)),one,complement(complement(X1)),meet(X1,X2)),
inference(step,[status(thm)],[t117532,t17]) ).
cnf(t117534,plain,
meet(X1,X2) = ifeq(join(X2,complement(X1)),one,X1,meet(X1,X2)),
inference(step,[status(thm)],[t117533,t839]) ).
cnf(t68618,plain,
ifeq(join(X1,complement(X2)),one,X2,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t117534]) ).
cnf(t42493,plain,
one = join(complement(meet(X1,complement(X2))),complement(meet(X2,X3))),
inference(cp,[status(thm)],[t42490,t35391]) ).
cnf(t117251,plain,
one = join(complement(meet(X2,X3)),complement(meet(X1,complement(X2)))),
inference(step,[status(thm)],[t42493,t63]) ).
cnf(t42728,plain,
join(complement(meet(X1,X2)),complement(meet(X3,complement(X1)))) = one,
inference(orient,[status(thm)],[t117251]) ).
cnf(t35654,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),join(X3,complement(X1))),
inference(cp,[status(thm)],[t26834,t35631]) ).
cnf(t117237,plain,
complement(join(X1,X2)) = meet(join(X3,complement(X1)),complement(join(X1,X2))),
inference(step,[status(thm)],[t35654,t23]) ).
cnf(t40699,plain,
meet(join(X1,complement(X2)),complement(join(X2,X3))) = complement(join(X2,X3)),
inference(orient,[status(thm)],[t117237]) ).
cnf(t42783,plain,
one = join(complement(meet(join(X1,X2),X3)),complement(complement(join(X1,X2)))),
inference(cp,[status(thm)],[t42728,t40699]) ).
cnf(t117272,plain,
one = join(complement(meet(join(X1,X2),X3)),join(X1,X2)),
inference(step,[status(thm)],[t42783,t839]) ).
cnf(t117273,plain,
one = join(X2,join(complement(meet(join(X1,X2),X3)),X1)),
inference(step,[status(thm)],[t117272,t67]) ).
cnf(t117274,plain,
one = join(X1,join(X2,complement(meet(join(X1,X2),X3)))),
inference(step,[status(thm)],[t117273,t67]) ).
cnf(t117275,plain,
one = join(X1,join(X2,complement(meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t117274,t23]) ).
cnf(t43807,plain,
join(X1,join(X2,complement(meet(X3,join(X1,X2))))) = one,
inference(orient,[status(thm)],[t117275]) ).
cnf(t43810,plain,
one = join(X1,complement(meet(X2,join(X1,complement(X2))))),
inference(cp,[status(thm)],[t43807,t35336]) ).
cnf(t43935,plain,
join(X1,complement(meet(X2,join(X1,complement(X2))))) = one,
inference(orient,[status(thm)],[t43810]) ).
cnf(t68622,plain,
meet(meet(X1,join(X2,complement(X1))),X2) = ifeq(one,one,meet(X1,join(X2,complement(X1))),meet(meet(X1,join(X2,complement(X1))),X2)),
inference(cp,[status(thm)],[t68618,t43935]) ).
cnf(t117535,plain,
meet(X2,meet(X1,join(X2,complement(X1)))) = ifeq(one,one,meet(X1,join(X2,complement(X1))),meet(meet(X1,join(X2,complement(X1))),X2)),
inference(step,[status(thm)],[t68622,t23]) ).
cnf(t117536,plain,
meet(X2,X1) = ifeq(one,one,meet(X1,join(X2,complement(X1))),meet(meet(X1,join(X2,complement(X1))),X2)),
inference(step,[status(thm)],[t117535,t161]) ).
cnf(t117537,plain,
meet(X1,X2) = ifeq(one,one,meet(X1,join(X2,complement(X1))),meet(meet(X1,join(X2,complement(X1))),X2)),
inference(step,[status(thm)],[t117536,t23]) ).
cnf(t117538,plain,
meet(X1,X2) = meet(X1,join(X2,complement(X1))),
inference(step,[status(thm)],[t117537,t17]) ).
cnf(t68812,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t117538]) ).
cnf(t68846,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t68812,t839]) ).
cnf(t117541,plain,
meet(X2,complement(X1)) = meet(complement(X1),join(X2,X1)),
inference(step,[status(thm)],[t68846,t23]) ).
cnf(t117542,plain,
meet(X2,complement(X1)) = meet(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t117541,t63]) ).
cnf(t69007,plain,
meet(complement(X1),join(X1,X2)) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t117542]) ).
cnf(t69015,plain,
meet(complement(meet(X1,complement(complement(X2)))),complement(X2)) = complement(X2),
inference(cp,[status(thm)],[t69007,t37551]) ).
cnf(t117549,plain,
meet(complement(meet(X1,X2)),complement(X2)) = complement(X2),
inference(step,[status(thm)],[t69015,t839]) ).
cnf(t117550,plain,
meet(complement(X2),complement(meet(X1,X2))) = complement(X2),
inference(step,[status(thm)],[t117549,t23]) ).
cnf(t69746,plain,
meet(complement(X1),complement(meet(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t117550]) ).
cnf(t117551,plain,
meet(X1,complement(X2)) = meet(X1,complement(meet(X1,X2))),
inference(step,[status(thm)],[t34655,t69746]) ).
cnf(t69958,plain,
meet(X1,complement(X2)) = meet(X1,complement(meet(X1,X2))),
inference(rw,[status(thm)],[t117551]) ).
cnf(t69959,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t69958]) ).
cnf(t69963,plain,
meet(X1,complement(join(X2,complement(X1)))) = meet(X1,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t69959,t68812]) ).
cnf(t35568,plain,
complement(join(X1,complement(X2))) = meet(complement(join(X1,complement(X2))),X2),
inference(cp,[status(thm)],[t26774,t35558]) ).
cnf(t117147,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t35568,t23]) ).
cnf(t36057,plain,
meet(X1,complement(join(X2,complement(X1)))) = complement(join(X2,complement(X1))),
inference(orient,[status(thm)],[t117147]) ).
cnf(t117569,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(meet(X1,X2))),
inference(step,[status(thm)],[t69963,t36057]) ).
cnf(t117570,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t117569,t69959]) ).
cnf(t70277,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t117570]) ).
cnf(t56960,plain,
join(meet(X1,join(X2,X3)),complement(X2)) = join(complement(X2),meet(X2,X1)),
inference(cp,[status(thm)],[t56803,t161]) ).
cnf(t117426,plain,
join(complement(X2),meet(X1,join(X2,X3))) = join(complement(X2),meet(X2,X1)),
inference(step,[status(thm)],[t56960,t63]) ).
cnf(t117427,plain,
join(complement(X2),meet(X1,join(X2,X3))) = join(X1,complement(X2)),
inference(step,[status(thm)],[t117426,t56803]) ).
cnf(t57984,plain,
join(complement(X1),meet(X2,join(X1,X3))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t117427]) ).
cnf(t57987,plain,
join(X1,complement(complement(X2))) = join(X2,meet(X1,join(complement(X2),X3))),
inference(cp,[status(thm)],[t57984,t839]) ).
cnf(t117429,plain,
join(X1,X2) = join(X2,meet(X1,join(complement(X2),X3))),
inference(step,[status(thm)],[t57987,t839]) ).
cnf(t117430,plain,
join(X1,X2) = join(X2,meet(X1,join(X3,complement(X2)))),
inference(step,[status(thm)],[t117429,t63]) ).
cnf(t58197,plain,
join(X1,meet(X2,join(X3,complement(X1)))) = join(X2,X1),
inference(orient,[status(thm)],[t117430]) ).
cnf(t58244,plain,
join(X1,join(X2,X3)) = join(join(X2,X3),meet(X1,complement(X2))),
inference(cp,[status(thm)],[t58197,t35631]) ).
cnf(t59493,plain,
join(join(X1,X2),meet(X3,complement(X1))) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t58244]) ).
cnf(t59552,plain,
join(X1,join(complement(X2),complement(meet(X2,X3)))) = join(complement(meet(X2,X3)),meet(X1,complement(complement(X2)))),
inference(cp,[status(thm)],[t59493,t35336]) ).
cnf(t117486,plain,
join(X1,complement(meet(X2,X3))) = join(complement(meet(X2,X3)),meet(X1,complement(complement(X2)))),
inference(step,[status(thm)],[t59552,t35336]) ).
cnf(t117487,plain,
join(X1,complement(meet(X2,X3))) = join(complement(meet(X2,X3)),meet(X1,X2)),
inference(step,[status(thm)],[t117486,t839]) ).
cnf(t117488,plain,
join(X1,complement(meet(X2,X3))) = join(meet(X1,X2),complement(meet(X2,X3))),
inference(step,[status(thm)],[t117487,t63]) ).
cnf(t62285,plain,
join(meet(X1,X2),complement(meet(X2,X3))) = join(X1,complement(meet(X2,X3))),
inference(orient,[status(thm)],[t117488]) ).
cnf(t70296,plain,
meet(meet(X1,X2),complement(meet(X3,X1))) = complement(join(X3,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t70277,t62285]) ).
cnf(t117765,plain,
meet(meet(X1,X2),complement(meet(X1,X3))) = complement(join(X3,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t70296,t23]) ).
cnf(t117766,plain,
meet(meet(X1,X2),complement(meet(X1,X3))) = meet(meet(X1,X2),complement(X3)),
inference(step,[status(thm)],[t117765,t70277]) ).
cnf(t117767,plain,
meet(meet(X1,X2),complement(meet(X1,X3))) = meet(complement(X3),meet(X1,X2)),
inference(step,[status(thm)],[t117766,t23]) ).
cnf(t117768,plain,
meet(meet(X1,X2),complement(meet(X1,X3))) = meet(X2,meet(complement(X3),X1)),
inference(step,[status(thm)],[t117767,t26]) ).
cnf(t117769,plain,
meet(meet(X1,X2),complement(meet(X1,X3))) = meet(X1,meet(X2,complement(X3))),
inference(step,[status(thm)],[t117768,t26]) ).
cnf(t86523,plain,
meet(meet(X1,X2),complement(meet(X1,X3))) = meet(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t117769]) ).
cnf(t69186,plain,
meet(X1,complement(X2)) = meet(complement(X2),join(X1,X2)),
inference(cp,[status(thm)],[t69007,t63]) ).
cnf(t69393,plain,
meet(complement(X1),join(X2,X1)) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t69186]) ).
cnf(t86648,plain,
meet(complement(X1),meet(join(X2,X1),complement(X3))) = meet(meet(X2,complement(X1)),complement(meet(complement(X1),X3))),
inference(cp,[status(thm)],[t86523,t69393]) ).
cnf(t118006,plain,
meet(complement(X1),meet(complement(X3),join(X2,X1))) = meet(meet(X2,complement(X1)),complement(meet(complement(X1),X3))),
inference(step,[status(thm)],[t86648,t23]) ).
cnf(t118007,plain,
meet(complement(X1),meet(complement(X3),join(X1,X2))) = meet(meet(X2,complement(X1)),complement(meet(complement(X1),X3))),
inference(step,[status(thm)],[t118006,t63]) ).
cnf(t59553,plain,
join(X1,join(complement(X2),complement(meet(X3,X2)))) = join(complement(meet(X3,X2)),meet(X1,complement(complement(X2)))),
inference(cp,[status(thm)],[t59493,t35442]) ).
cnf(t62559,plain,
join(meet(X1,X2),complement(meet(X3,X2))) = join(X1,complement(meet(X3,X2))),
inference(orient,[status(thm)],[t59553]) ).
cnf(t70295,plain,
meet(meet(X1,X2),complement(meet(X3,X2))) = complement(join(X3,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t70277,t62559]) ).
cnf(t117760,plain,
meet(meet(X1,X2),complement(meet(X2,X3))) = complement(join(X3,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t70295,t23]) ).
cnf(t117761,plain,
meet(meet(X1,X2),complement(meet(X2,X3))) = meet(meet(X1,X2),complement(X3)),
inference(step,[status(thm)],[t117760,t70277]) ).
cnf(t117762,plain,
meet(meet(X1,X2),complement(meet(X2,X3))) = meet(complement(X3),meet(X1,X2)),
inference(step,[status(thm)],[t117761,t23]) ).
cnf(t117763,plain,
meet(meet(X1,X2),complement(meet(X2,X3))) = meet(X2,meet(complement(X3),X1)),
inference(step,[status(thm)],[t117762,t26]) ).
cnf(t117764,plain,
meet(meet(X1,X2),complement(meet(X2,X3))) = meet(X1,meet(X2,complement(X3))),
inference(step,[status(thm)],[t117763,t26]) ).
cnf(t86021,plain,
meet(meet(X1,X2),complement(meet(X2,X3))) = meet(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t117764]) ).
cnf(t118008,plain,
meet(complement(X1),meet(complement(X3),join(X1,X2))) = meet(X2,meet(complement(X1),complement(X3))),
inference(step,[status(thm)],[t118007,t86021]) ).
cnf(t70310,plain,
meet(complement(X1),complement(X2)) = complement(join(X2,X1)),
inference(cp,[status(thm)],[t70277,t839]) ).
cnf(t117583,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(step,[status(thm)],[t70310,t63]) ).
cnf(t70766,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t117583]) ).
cnf(t118009,plain,
meet(complement(X1),meet(complement(X3),join(X1,X2))) = meet(X2,complement(join(X1,X3))),
inference(step,[status(thm)],[t118008,t70766]) ).
cnf(t109746,plain,
meet(complement(X1),meet(complement(X2),join(X1,X3))) = meet(X3,complement(join(X1,X2))),
inference(orient,[status(thm)],[t118009]) ).
cnf(t109960,plain,
meet(X1,complement(join(X2,X3))) = meet(complement(X2),meet(complement(X3),join(X1,X2))),
inference(cp,[status(thm)],[t109746,t63]) ).
cnf(t111250,plain,
meet(complement(X1),meet(complement(X2),join(X3,X1))) = meet(X3,complement(join(X1,X2))),
inference(orient,[status(thm)],[t109960]) ).
cnf(t111466,plain,
join(meet(complement(X1),join(X2,X3)),complement(complement(X3))) = join(complement(complement(X3)),meet(X2,complement(join(X3,X1)))),
inference(cp,[status(thm)],[t56803,t111250]) ).
cnf(t118016,plain,
join(complement(complement(X3)),meet(complement(X1),join(X2,X3))) = join(complement(complement(X3)),meet(X2,complement(join(X3,X1)))),
inference(step,[status(thm)],[t111466,t63]) ).
cnf(t118017,plain,
join(X3,meet(complement(X1),join(X2,X3))) = join(complement(complement(X3)),meet(X2,complement(join(X3,X1)))),
inference(step,[status(thm)],[t118016,t839]) ).
cnf(t118018,plain,
join(X3,meet(complement(X1),join(X2,X3))) = join(X3,meet(X2,complement(join(X3,X1)))),
inference(step,[status(thm)],[t118017,t839]) ).
cnf(t57011,plain,
join(meet(X1,X2),complement(X3)) = join(complement(X3),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t56803,t26]) ).
cnf(t117471,plain,
join(complement(X3),meet(X1,X2)) = join(complement(X3),meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t57011,t63]) ).
cnf(t61386,plain,
join(complement(X1),meet(X2,meet(X3,X1))) = join(complement(X1),meet(X2,X3)),
inference(orient,[status(thm)],[t117471]) ).
cnf(t70802,plain,
join(complement(complement(X1)),meet(X2,complement(X3))) = join(complement(complement(X1)),meet(X2,complement(join(X3,X1)))),
inference(cp,[status(thm)],[t61386,t70766]) ).
cnf(t117770,plain,
join(X1,meet(X2,complement(X3))) = join(complement(complement(X1)),meet(X2,complement(join(X3,X1)))),
inference(step,[status(thm)],[t70802,t839]) ).
cnf(t117771,plain,
join(X1,meet(X2,complement(X3))) = join(X1,meet(X2,complement(join(X3,X1)))),
inference(step,[status(thm)],[t117770,t839]) ).
cnf(t117772,plain,
join(X1,meet(X2,complement(X3))) = join(X1,meet(X2,complement(join(X1,X3)))),
inference(step,[status(thm)],[t117771,t63]) ).
cnf(t87035,plain,
join(X1,meet(X2,complement(join(X1,X3)))) = join(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t117772]) ).
cnf(t118019,plain,
join(X3,meet(complement(X1),join(X2,X3))) = join(X3,meet(X2,complement(X1))),
inference(step,[status(thm)],[t118018,t87035]) ).
cnf(t111675,plain,
join(X1,meet(complement(X2),join(X3,X1))) = join(X1,meet(X3,complement(X2))),
inference(orient,[status(thm)],[t118019]) ).
cnf(t70318,plain,
join(X1,complement(X2)) = complement(meet(X2,complement(X1))),
inference(cp,[status(thm)],[t839,t70277]) ).
cnf(t71081,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t70318]) ).
cnf(t71099,plain,
join(join(X1,complement(X2)),complement(X3)) = complement(meet(X3,meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t71081,t70277]) ).
cnf(t117678,plain,
join(complement(X3),join(X1,complement(X2))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t71099,t63]) ).
cnf(t117679,plain,
join(complement(X2),join(complement(X3),X1)) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t117678,t67]) ).
cnf(t117680,plain,
join(X1,join(complement(X2),complement(X3))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t117679,t67]) ).
cnf(t71100,plain,
join(complement(X1),complement(X2)) = complement(meet(X2,X1)),
inference(cp,[status(thm)],[t71081,t839]) ).
cnf(t117617,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t71100,t23]) ).
cnf(t71315,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t117617]) ).
cnf(t117681,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X3,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t117680,t71315]) ).
cnf(t117682,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X2,meet(complement(X1),X3))),
inference(step,[status(thm)],[t117681,t26]) ).
cnf(t117683,plain,
join(X1,complement(meet(X2,X3))) = complement(meet(X2,meet(X3,complement(X1)))),
inference(step,[status(thm)],[t117682,t23]) ).
cnf(t75746,plain,
complement(meet(X1,meet(X2,complement(X3)))) = join(X3,complement(meet(X1,X2))),
inference(orient,[status(thm)],[t117683]) ).
cnf(t75811,plain,
meet(X1,complement(meet(X2,complement(X3)))) = meet(X1,join(X3,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t69959,t75746]) ).
cnf(t117796,plain,
meet(X1,join(X3,complement(X2))) = meet(X1,join(X3,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t75811,t71081]) ).
cnf(t90179,plain,
meet(X1,join(X2,complement(meet(X1,X3)))) = meet(X1,join(X2,complement(X3))),
inference(orient,[status(thm)],[t117796]) ).
cnf(t90207,plain,
meet(X1,join(X2,complement(complement(meet(X1,X3))))) = meet(X1,join(X2,complement(meet(X1,complement(X3))))),
inference(cp,[status(thm)],[t90179,t69959]) ).
cnf(t117797,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,complement(meet(X1,complement(X3))))),
inference(step,[status(thm)],[t90207,t839]) ).
cnf(t117798,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,complement(complement(X3)))),
inference(step,[status(thm)],[t117797,t90179]) ).
cnf(t117799,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t117798,t839]) ).
cnf(t90444,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t117799]) ).
cnf(t111698,plain,
join(meet(complement(X1),X2),meet(X3,complement(X1))) = join(meet(complement(X1),X2),meet(complement(X1),join(X3,X2))),
inference(cp,[status(thm)],[t111675,t90444]) ).
cnf(t118045,plain,
join(meet(X3,complement(X1)),meet(complement(X1),X2)) = join(meet(complement(X1),X2),meet(complement(X1),join(X3,X2))),
inference(step,[status(thm)],[t111698,t63]) ).
cnf(t118046,plain,
join(meet(X3,complement(X1)),meet(X2,complement(X1))) = join(meet(complement(X1),X2),meet(complement(X1),join(X3,X2))),
inference(step,[status(thm)],[t118045,t23]) ).
cnf(t118047,plain,
join(meet(X2,complement(X1)),meet(X3,complement(X1))) = join(meet(complement(X1),X2),meet(complement(X1),join(X3,X2))),
inference(step,[status(thm)],[t118046,t63]) ).
cnf(t6323,plain,
zero = meet(X1,meet(meet(X2,X3),meet(Y3,complement(meet(X2,meet(X3,X1)))))),
inference(cp,[status(thm)],[t6222,t26]) ).
cnf(t116328,plain,
zero = meet(X1,meet(Y3,meet(complement(meet(X2,meet(X3,X1))),meet(X2,X3)))),
inference(step,[status(thm)],[t6323,t26]) ).
cnf(t116329,plain,
zero = meet(X1,meet(Y3,meet(X3,meet(complement(meet(X2,meet(X3,X1))),X2)))),
inference(step,[status(thm)],[t116328,t26]) ).
cnf(t116330,plain,
zero = meet(X1,meet(Y3,meet(X2,meet(X3,complement(meet(X2,meet(X3,X1))))))),
inference(step,[status(thm)],[t116329,t26]) ).
cnf(t116331,plain,
zero = meet(X1,meet(X2,meet(meet(X3,complement(meet(X2,meet(X3,X1)))),Y3))),
inference(step,[status(thm)],[t116330,t26]) ).
cnf(t116332,plain,
zero = meet(X1,meet(X2,meet(Y3,meet(X3,complement(meet(X2,meet(X3,X1))))))),
inference(step,[status(thm)],[t116331,t23]) ).
cnf(t116333,plain,
zero = meet(X1,meet(X2,meet(X3,meet(complement(meet(X2,meet(X3,X1))),Y3)))),
inference(step,[status(thm)],[t116332,t26]) ).
cnf(t116334,plain,
zero = meet(X1,meet(X2,meet(X3,meet(Y3,complement(meet(X2,meet(X3,X1))))))),
inference(step,[status(thm)],[t116333,t23]) ).
cnf(t116335,plain,
zero = meet(X1,meet(X2,meet(X3,meet(Y3,complement(meet(X1,meet(X2,X3))))))),
inference(step,[status(thm)],[t116334,t26]) ).
cnf(t10026,plain,
meet(X1,meet(X2,meet(X3,meet(Y3,complement(meet(X1,meet(X2,X3))))))) = zero,
inference(orient,[status(thm)],[t116335]) ).
cnf(t10029,plain,
zero = meet(X1,meet(X2,meet(X3,complement(meet(X1,meet(X2,X3)))))),
inference(cp,[status(thm)],[t10026,t102]) ).
cnf(t10214,plain,
meet(X1,meet(X2,meet(X3,complement(meet(X1,meet(X2,X3)))))) = zero,
inference(orient,[status(thm)],[t10029]) ).
cnf(t10256,plain,
complement(X1) = join(complement(X1),meet(meet(X2,meet(X3,complement(meet(X1,meet(X2,X3))))),complement(zero))),
inference(cp,[status(thm)],[t7325,t10214]) ).
cnf(t116336,plain,
complement(X1) = join(complement(X1),meet(meet(X2,meet(X3,complement(meet(X1,meet(X2,X3))))),one)),
inference(step,[status(thm)],[t10256,t141]) ).
cnf(t116337,plain,
complement(X1) = join(complement(X1),meet(X2,meet(X3,complement(meet(X1,meet(X2,X3)))))),
inference(step,[status(thm)],[t116336,t96]) ).
cnf(t10297,plain,
join(complement(X1),meet(X2,meet(X3,complement(meet(X1,meet(X2,X3)))))) = complement(X1),
inference(orient,[status(thm)],[t116337]) ).
cnf(t10298,plain,
complement(complement(X1)) = join(X1,meet(X2,meet(X3,complement(meet(complement(X1),meet(X2,X3)))))),
inference(cp,[status(thm)],[t10297,t839]) ).
cnf(t116338,plain,
X1 = join(X1,meet(X2,meet(X3,complement(meet(complement(X1),meet(X2,X3)))))),
inference(step,[status(thm)],[t10298,t839]) ).
cnf(t116339,plain,
X1 = join(X1,meet(X2,meet(X3,complement(meet(X3,meet(complement(X1),X2)))))),
inference(step,[status(thm)],[t116338,t26]) ).
cnf(t116340,plain,
X1 = join(X1,meet(X2,meet(X3,complement(meet(X2,meet(X3,complement(X1))))))),
inference(step,[status(thm)],[t116339,t26]) ).
cnf(t10380,plain,
join(X1,meet(X2,meet(X3,complement(meet(X2,meet(X3,complement(X1))))))) = X1,
inference(orient,[status(thm)],[t116340]) ).
cnf(t10243,plain,
zero = meet(X1,meet(X2,meet(meet(X3,join(X2,Y3)),complement(meet(X1,meet(X2,X3)))))),
inference(cp,[status(thm)],[t10214,t161]) ).
cnf(t18465,plain,
meet(X1,meet(X2,meet(meet(X3,join(X2,Y3)),complement(meet(X1,meet(X2,X3)))))) = zero,
inference(orient,[status(thm)],[t10243]) ).
cnf(t18467,plain,
zero = meet(X1,meet(meet(meet(X2,join(X1,X3)),complement(meet(Y3,meet(X1,X2)))),Y3)),
inference(cp,[status(thm)],[t18465,t26]) ).
cnf(t116784,plain,
zero = meet(X1,meet(Y3,meet(meet(X2,join(X1,X3)),complement(meet(Y3,meet(X1,X2)))))),
inference(step,[status(thm)],[t18467,t23]) ).
cnf(t116785,plain,
zero = meet(X1,meet(Y3,meet(meet(X2,join(X1,X3)),complement(meet(X2,meet(Y3,X1)))))),
inference(step,[status(thm)],[t116784,t26]) ).
cnf(t116786,plain,
zero = meet(X1,meet(Y3,meet(meet(X2,join(X1,X3)),complement(meet(X1,meet(X2,Y3)))))),
inference(step,[status(thm)],[t116785,t26]) ).
cnf(t20121,plain,
meet(X1,meet(X2,meet(meet(X3,join(X1,Y3)),complement(meet(X1,meet(X3,X2)))))) = zero,
inference(orient,[status(thm)],[t116786]) ).
cnf(t34728,plain,
meet(X1,complement(meet(X1,meet(X2,meet(X3,complement(X1)))))) = meet(X1,meet(complement(meet(X2,meet(X3,complement(X1)))),complement(zero))),
inference(cp,[status(thm)],[t34655,t186]) ).
cnf(t117155,plain,
meet(X1,complement(zero)) = meet(X1,meet(complement(meet(X2,meet(X3,complement(X1)))),complement(zero))),
inference(step,[status(thm)],[t34728,t186]) ).
cnf(t117156,plain,
meet(X1,one) = meet(X1,meet(complement(meet(X2,meet(X3,complement(X1)))),complement(zero))),
inference(step,[status(thm)],[t117155,t141]) ).
cnf(t117157,plain,
X1 = meet(X1,meet(complement(meet(X2,meet(X3,complement(X1)))),complement(zero))),
inference(step,[status(thm)],[t117156,t96]) ).
cnf(t117158,plain,
X1 = meet(X1,meet(complement(zero),complement(meet(X2,meet(X3,complement(X1)))))),
inference(step,[status(thm)],[t117157,t23]) ).
cnf(t117159,plain,
X1 = meet(X1,meet(one,complement(meet(X2,meet(X3,complement(X1)))))),
inference(step,[status(thm)],[t117158,t141]) ).
cnf(t117160,plain,
X1 = meet(X1,complement(meet(X2,meet(X3,complement(X1))))),
inference(step,[status(thm)],[t117159,t14956]) ).
cnf(t36556,plain,
meet(X1,complement(meet(X2,meet(X3,complement(X1))))) = X1,
inference(orient,[status(thm)],[t117160]) ).
cnf(t36683,plain,
zero = meet(X1,meet(complement(meet(X2,join(X1,X3))),meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t20121,t36556]) ).
cnf(t117221,plain,
zero = meet(X1,meet(complement(meet(X2,join(X1,X3))),X2)),
inference(step,[status(thm)],[t36683,t235]) ).
cnf(t117222,plain,
zero = meet(X1,meet(X2,complement(meet(X2,join(X1,X3))))),
inference(step,[status(thm)],[t117221,t23]) ).
cnf(t39689,plain,
meet(X1,meet(X2,complement(meet(X2,join(X1,X3))))) = zero,
inference(orient,[status(thm)],[t117222]) ).
cnf(t39865,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X2,meet(X1,complement(zero)))),
inference(cp,[status(thm)],[t10380,t39689]) ).
cnf(t117501,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X1,meet(complement(zero),X2))),
inference(step,[status(thm)],[t39865,t26]) ).
cnf(t117502,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X1,meet(X2,complement(zero)))),
inference(step,[status(thm)],[t117501,t23]) ).
cnf(t117503,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X1,meet(X2,one))),
inference(step,[status(thm)],[t117502,t141]) ).
cnf(t117504,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X1,X2)),
inference(step,[status(thm)],[t117503,t96]) ).
cnf(t117505,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t117504,t63]) ).
cnf(t64215,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t117505]) ).
cnf(t64305,plain,
meet(X1,join(X2,meet(X3,join(Y3,complement(X2))))) = join(meet(X1,X2),meet(X1,join(X3,X2))),
inference(cp,[status(thm)],[t64215,t58197]) ).
cnf(t117521,plain,
meet(X1,join(X3,X2)) = join(meet(X1,X2),meet(X1,join(X3,X2))),
inference(step,[status(thm)],[t64305,t58197]) ).
cnf(t67227,plain,
join(meet(X1,X2),meet(X1,join(X3,X2))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t117521]) ).
cnf(t118048,plain,
join(meet(X2,complement(X1)),meet(X3,complement(X1))) = meet(complement(X1),join(X3,X2)),
inference(step,[status(thm)],[t118047,t67227]) ).
cnf(t118049,plain,
join(meet(X2,complement(X1)),meet(X3,complement(X1))) = meet(complement(X1),join(X2,X3)),
inference(step,[status(thm)],[t118048,t63]) ).
cnf(t114779,plain,
join(meet(X1,complement(X2)),meet(X3,complement(X2))) = meet(complement(X2),join(X1,X3)),
inference(orient,[status(thm)],[t118049]) ).
cnf(t114827,plain,
meet(complement(complement(X1)),join(X2,X3)) = join(meet(X2,X1),meet(X3,complement(complement(X1)))),
inference(cp,[status(thm)],[t114779,t839]) ).
cnf(t118050,plain,
meet(join(X2,X3),complement(complement(X1))) = join(meet(X2,X1),meet(X3,complement(complement(X1)))),
inference(step,[status(thm)],[t114827,t23]) ).
cnf(t118051,plain,
meet(join(X2,X3),X1) = join(meet(X2,X1),meet(X3,complement(complement(X1)))),
inference(step,[status(thm)],[t118050,t839]) ).
cnf(t118052,plain,
meet(X1,join(X2,X3)) = join(meet(X2,X1),meet(X3,complement(complement(X1)))),
inference(step,[status(thm)],[t118051,t23]) ).
cnf(t118053,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X3,complement(complement(X1)))),
inference(step,[status(thm)],[t118052,t23]) ).
cnf(t118054,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X3,X1)),
inference(step,[status(thm)],[t118053,t839]) ).
cnf(t118055,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,X3)),
inference(step,[status(thm)],[t118054,t23]) ).
cnf(t115046,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t118055]) ).
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,t115046]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT209-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/5.39 % Computer : n011.cluster.edu
% 0.12/5.39 % Model : x86_64 x86_64
% 0.12/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.39 % Memory : 8046.5625MB
% 0.12/5.39 % OS : Linux 6.8.0-71-generic
% 0.12/5.39 % CPULimit : 300
% 0.12/5.39 % WCLimit : 300
% 0.12/5.39 % DateTime : Wed Sep 23 20:34:17 UTC 2026
% 0.16/5.40 % CPUTime :
% 0.16/5.40 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 59.67/13.00 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 59.67/13.00 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------