%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT214-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:56:10 PM UTC 2026
% Result : Unsatisfiable 40.62s 6.06s
% Output : Proof 40.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 162
% Number of leaves : 14
% Syntax : Number of formulae : 474 ( 470 unt; 0 def)
% Number of atoms : 482 ( 481 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-4 aty)
% Number of variables : 1092 ( 223 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f10,axiom,
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f10_nnf,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( complement(X0) = X1
| join(X0,X1) != one
| meet(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t11,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t18,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(f4,axiom,
meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f4_nnf,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t7,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t23,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t25,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X2,X1),one,complement(X2),X1),X1),
inference(cp,[status(thm)],[t18,t23]) ).
cnf(f5,axiom,
join(X,Y) = join(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f5_nnf,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t72,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t36493,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(step,[status(thm)],[t25,t72]) ).
cnf(t343,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t36493]) ).
cnf(f9,axiom,
meet(X,complement(X)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f9_nnf,plain,
! [X] : meet(X,complement(X)) = zero,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] : meet(X,complement(X)) = zero,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
meet(X0,complement(X0)) = zero,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t3,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t65,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t352,plain,
X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t343,t65]) ).
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(t36494,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t352,t17]) ).
cnf(f8,axiom,
join(X,complement(X)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f8_nnf,plain,
! [X] : join(X,complement(X)) = one,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] : join(X,complement(X)) = one,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
join(X0,complement(X0)) = one,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t2,plain,
join(X1,complement(X1)) = one,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t96,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t36495,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t36494,t96]) ).
cnf(t36496,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t36495,t17]) ).
cnf(t370,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t36496]) ).
cnf(f7,axiom,
join(join(X,Y),Z) = join(X,join(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f7_nnf,plain,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t9,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t36397,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t9,t72]) ).
cnf(t76,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t36397]) ).
cnf(t98,plain,
join(X1,join(complement(X1),X2)) = join(X2,one),
inference(cp,[status(thm)],[t76,t96]) ).
cnf(t36410,plain,
join(X1,join(X2,complement(X1))) = join(X2,one),
inference(step,[status(thm)],[t98,t72]) ).
cnf(f1,axiom,
join(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f1_nnf,plain,
! [X] : join(X,X) = X,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] : join(X,X) = X,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t0,plain,
join(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t15,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t79,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t76,t15]) ).
cnf(t36401,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t79,t76]) ).
cnf(t36402,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t36401,t72]) ).
cnf(t125,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t36402]) ).
cnf(t128,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t125,t96]) ).
cnf(t36403,plain,
one = join(X1,one),
inference(step,[status(thm)],[t128,t96]) ).
cnf(t135,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t36403]) ).
cnf(t36411,plain,
join(X1,join(X2,complement(X1))) = one,
inference(step,[status(thm)],[t36410,t135]) ).
cnf(t159,plain,
join(X1,join(X2,complement(X1))) = one,
inference(orient,[status(thm)],[t36411]) ).
cnf(t363,plain,
X1 = ifeq(meet(X1,join(X2,complement(X1))),zero,ifeq(one,one,complement(join(X2,complement(X1))),X1),X1),
inference(cp,[status(thm)],[t343,t159]) ).
cnf(t36521,plain,
X1 = ifeq(meet(X1,join(X2,complement(X1))),zero,complement(join(X2,complement(X1))),X1),
inference(step,[status(thm)],[t363,t17]) ).
cnf(t467,plain,
ifeq(meet(X1,join(X2,complement(X1))),zero,complement(join(X2,complement(X1))),X1) = X1,
inference(orient,[status(thm)],[t36521]) ).
cnf(t469,plain,
complement(X1) = ifeq(meet(complement(X1),join(X2,X1)),zero,complement(join(X2,complement(complement(X1)))),complement(X1)),
inference(cp,[status(thm)],[t467,t370]) ).
cnf(t36525,plain,
complement(X1) = ifeq(meet(complement(X1),join(X1,X2)),zero,complement(join(X2,complement(complement(X1)))),complement(X1)),
inference(step,[status(thm)],[t469,t72]) ).
cnf(t36526,plain,
complement(X1) = ifeq(meet(complement(X1),join(X1,X2)),zero,complement(join(X2,X1)),complement(X1)),
inference(step,[status(thm)],[t36525,t370]) ).
cnf(t36527,plain,
complement(X1) = ifeq(meet(complement(X1),join(X1,X2)),zero,complement(join(X1,X2)),complement(X1)),
inference(step,[status(thm)],[t36526,t72]) ).
cnf(t494,plain,
ifeq(meet(complement(X1),join(X1,X2)),zero,complement(join(X1,X2)),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t36527]) ).
cnf(f11,axiom,
meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(meet(X,join(Y,meet(X,Z))),meet(Z,U))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H79) ).
fof(f11_nnf,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(meet(X,join(Y,meet(X,Z))),meet(Z,U))),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(meet(X,join(Y,meet(X,Z))),meet(Z,U))),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(meet(X0,join(X1,meet(X0,X2))),meet(X2,X3))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t12,plain,
meet(X1,join(meet(X1,join(X2,meet(X1,X3))),meet(X3,X4))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t46,plain,
meet(X1,join(meet(X1,join(X2,meet(X1,X3))),meet(X3,X4))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t12]) ).
cnf(t75,plain,
meet(X1,join(meet(X1,join(X2,meet(X1,X3))),meet(X3,X4))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(rw,[status(thm)],[t46]) ).
cnf(t36568,plain,
meet(X1,join(meet(X3,X4),meet(X1,join(X2,meet(X1,X3))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(step,[status(thm)],[t75,t72]) ).
cnf(t658,plain,
meet(X1,join(meet(X2,X3),meet(X1,join(X4,meet(X1,X2))))) = meet(X1,join(X4,meet(X2,join(X1,X3)))),
inference(orient,[status(thm)],[t36568]) ).
cnf(f2,axiom,
meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f2_nnf,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t8,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t14,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t97,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t14,t96]) ).
cnf(t105,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t97]) ).
cnf(t674,plain,
meet(X1,join(X2,meet(X3,join(X1,one)))) = meet(X1,join(X3,meet(X1,join(X2,meet(X1,X3))))),
inference(cp,[status(thm)],[t658,t105]) ).
cnf(t36569,plain,
meet(X1,join(X2,meet(X3,one))) = meet(X1,join(X3,meet(X1,join(X2,meet(X1,X3))))),
inference(step,[status(thm)],[t674,t135]) ).
cnf(t36570,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X3,meet(X1,join(X2,meet(X1,X3))))),
inference(step,[status(thm)],[t36569,t105]) ).
cnf(t715,plain,
meet(X1,join(X2,meet(X1,join(X3,meet(X1,X2))))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t36570]) ).
cnf(t735,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(complement(X1),meet(X1,join(X2,zero)))),
inference(cp,[status(thm)],[t715,t65]) ).
cnf(f3,axiom,
join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f3_nnf,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t6,plain,
join(X1,meet(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t16,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t66,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t16,t65]) ).
cnf(t100,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t66]) ).
cnf(t36594,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(complement(X1),meet(X1,X2))),
inference(step,[status(thm)],[t735,t100]) ).
cnf(t958,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(X2,complement(X1))),
inference(orient,[status(thm)],[t36594]) ).
cnf(f6,axiom,
meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f6_nnf,plain,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t10,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t36396,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)],[t36396]) ).
cnf(f0,axiom,
meet(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f0_nnf,plain,
! [X] : meet(X,X) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : meet(X,X) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
meet(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
meet(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t13,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t29,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t26,t13]) ).
cnf(t36398,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t29,t26]) ).
cnf(t36399,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t36398,t23]) ).
cnf(t110,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t36399]) ).
cnf(t113,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t110,t65]) ).
cnf(t36400,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t113,t65]) ).
cnf(t120,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t36400]) ).
cnf(t731,plain,
meet(X1,join(X2,zero)) = meet(X1,join(zero,meet(X1,join(X2,zero)))),
inference(cp,[status(thm)],[t715,t120]) ).
cnf(t36571,plain,
meet(X1,X2) = meet(X1,join(zero,meet(X1,join(X2,zero)))),
inference(step,[status(thm)],[t731,t100]) ).
cnf(t36572,plain,
meet(X1,X2) = meet(X1,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t36571,t100]) ).
cnf(t756,plain,
meet(X1,join(zero,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t36572]) ).
cnf(t772,plain,
meet(X1,join(zero,X2)) = meet(X1,join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t715,t756]) ).
cnf(t36573,plain,
meet(X1,join(X2,zero)) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t772,t72]) ).
cnf(t36574,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t36573,t100]) ).
cnf(t780,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t36574]) ).
cnf(t801,plain,
meet(X1,join(X2,meet(X2,join(X1,X3)))) = meet(X1,join(meet(X2,X3),meet(X1,X2))),
inference(cp,[status(thm)],[t658,t780]) ).
cnf(t36575,plain,
meet(X1,X2) = meet(X1,join(meet(X2,X3),meet(X1,X2))),
inference(step,[status(thm)],[t801,t16]) ).
cnf(t36576,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t36575,t72]) ).
cnf(t806,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t36576]) ).
cnf(t822,plain,
meet(X1,complement(X1)) = meet(X1,join(zero,meet(complement(X1),X2))),
inference(cp,[status(thm)],[t806,t65]) ).
cnf(t36577,plain,
zero = meet(X1,join(zero,meet(complement(X1),X2))),
inference(step,[status(thm)],[t822,t65]) ).
cnf(t36578,plain,
zero = meet(X1,join(zero,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t36577,t23]) ).
cnf(t850,plain,
meet(X1,join(zero,meet(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t36578]) ).
cnf(t853,plain,
zero = meet(complement(X1),join(zero,meet(X2,X1))),
inference(cp,[status(thm)],[t850,t370]) ).
cnf(t36582,plain,
zero = meet(complement(X1),join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t853,t23]) ).
cnf(t903,plain,
meet(complement(X1),join(zero,meet(X1,X2))) = zero,
inference(orient,[status(thm)],[t36582]) ).
cnf(t775,plain,
meet(X1,join(zero,meet(X2,join(X1,X3)))) = meet(X1,join(meet(X2,X3),meet(X1,X2))),
inference(cp,[status(thm)],[t658,t756]) ).
cnf(t36674,plain,
meet(X1,join(zero,meet(X2,join(X1,X3)))) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t775,t72]) ).
cnf(t36675,plain,
meet(X1,join(zero,meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(step,[status(thm)],[t36674,t806]) ).
cnf(t1726,plain,
meet(X1,join(zero,meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t36675]) ).
cnf(t1748,plain,
meet(meet(X1,X2),X1) = meet(meet(X1,X2),join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t1726,t806]) ).
cnf(t36676,plain,
meet(X1,meet(X1,X2)) = meet(meet(X1,X2),join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t1748,t23]) ).
cnf(t36677,plain,
meet(X1,X2) = meet(meet(X1,X2),join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t36676,t110]) ).
cnf(t1792,plain,
meet(meet(X1,X2),join(zero,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t36677]) ).
cnf(t1807,plain,
zero = meet(complement(meet(X1,X2)),join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t903,t1792]) ).
cnf(t1830,plain,
meet(complement(meet(X1,X2)),join(zero,meet(X1,X2))) = zero,
inference(orient,[status(thm)],[t1807]) ).
cnf(t163,plain,
join(X1,complement(X2)) = ifeq(meet(X2,join(X1,complement(X2))),zero,ifeq(one,one,complement(X2),join(X1,complement(X2))),join(X1,complement(X2))),
inference(cp,[status(thm)],[t18,t159]) ).
cnf(t36537,plain,
join(X1,complement(X2)) = ifeq(meet(X2,join(X1,complement(X2))),zero,complement(X2),join(X1,complement(X2))),
inference(step,[status(thm)],[t163,t17]) ).
cnf(t562,plain,
ifeq(meet(X1,join(X2,complement(X1))),zero,complement(X1),join(X2,complement(X1))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t36537]) ).
cnf(t564,plain,
join(X1,complement(complement(X2))) = ifeq(meet(complement(X2),join(X1,X2)),zero,complement(complement(X2)),join(X1,complement(complement(X2)))),
inference(cp,[status(thm)],[t562,t370]) ).
cnf(t36538,plain,
join(X1,X2) = ifeq(meet(complement(X2),join(X1,X2)),zero,complement(complement(X2)),join(X1,complement(complement(X2)))),
inference(step,[status(thm)],[t564,t370]) ).
cnf(t36539,plain,
join(X1,X2) = ifeq(meet(complement(X2),join(X1,X2)),zero,X2,join(X1,complement(complement(X2)))),
inference(step,[status(thm)],[t36538,t370]) ).
cnf(t36540,plain,
join(X1,X2) = ifeq(meet(complement(X2),join(X1,X2)),zero,X2,join(X1,X2)),
inference(step,[status(thm)],[t36539,t370]) ).
cnf(t571,plain,
ifeq(meet(complement(X1),join(X2,X1)),zero,X1,join(X2,X1)) = join(X2,X1),
inference(orient,[status(thm)],[t36540]) ).
cnf(t1844,plain,
join(zero,meet(X1,X2)) = ifeq(zero,zero,meet(X1,X2),join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t571,t1830]) ).
cnf(t36678,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t1844,t17]) ).
cnf(t1857,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t36678]) ).
cnf(t36679,plain,
meet(complement(meet(X1,X2)),meet(X1,X2)) = zero,
inference(step,[status(thm)],[t1830,t1857]) ).
cnf(t1884,plain,
meet(complement(meet(X1,X2)),meet(X1,X2)) = zero,
inference(rw,[status(thm)],[t36679]) ).
cnf(t36684,plain,
meet(X2,meet(complement(meet(X1,X2)),X1)) = zero,
inference(step,[status(thm)],[t1884,t26]) ).
cnf(t36685,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = zero,
inference(step,[status(thm)],[t36684,t26]) ).
cnf(t1888,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = zero,
inference(orient,[status(thm)],[t36685]) ).
cnf(t1911,plain,
meet(X1,join(meet(X2,complement(meet(X1,X2))),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t958,t1888]) ).
cnf(t36695,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t1911,t72]) ).
cnf(t36696,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t36695,t100]) ).
cnf(t36697,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = zero,
inference(step,[status(thm)],[t36696,t65]) ).
cnf(t2012,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t36697]) ).
cnf(t2013,plain,
zero = meet(complement(X1),join(X1,meet(X2,complement(meet(complement(X1),X2))))),
inference(cp,[status(thm)],[t2012,t370]) ).
cnf(t36719,plain,
zero = meet(complement(X1),join(X1,meet(X2,complement(meet(X2,complement(X1)))))),
inference(step,[status(thm)],[t2013,t23]) ).
cnf(t2231,plain,
meet(complement(X1),join(X1,meet(X2,complement(meet(X2,complement(X1)))))) = zero,
inference(orient,[status(thm)],[t36719]) ).
cnf(t2243,plain,
complement(X1) = ifeq(zero,zero,complement(join(X1,meet(X2,complement(meet(X2,complement(X1)))))),complement(X1)),
inference(cp,[status(thm)],[t494,t2231]) ).
cnf(t36720,plain,
complement(X1) = complement(join(X1,meet(X2,complement(meet(X2,complement(X1)))))),
inference(step,[status(thm)],[t2243,t17]) ).
cnf(t2258,plain,
complement(join(X1,meet(X2,complement(meet(X2,complement(X1)))))) = complement(X1),
inference(orient,[status(thm)],[t36720]) ).
cnf(t2264,plain,
join(X1,meet(X2,complement(meet(X2,complement(X1))))) = complement(complement(X1)),
inference(cp,[status(thm)],[t370,t2258]) ).
cnf(t36721,plain,
join(X1,meet(X2,complement(meet(X2,complement(X1))))) = X1,
inference(step,[status(thm)],[t2264,t370]) ).
cnf(t2337,plain,
join(X1,meet(X2,complement(meet(X2,complement(X1))))) = X1,
inference(orient,[status(thm)],[t36721]) ).
cnf(t2339,plain,
complement(X1) = join(complement(X1),meet(X2,complement(meet(X2,X1)))),
inference(cp,[status(thm)],[t2337,t370]) ).
cnf(t36723,plain,
complement(X1) = join(complement(X1),meet(X2,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t2339,t23]) ).
cnf(t2357,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = complement(X1),
inference(orient,[status(thm)],[t36723]) ).
cnf(t70,plain,
meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
inference(cp,[status(thm)],[t26,t65]) ).
cnf(t36408,plain,
meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
inference(step,[status(thm)],[t70,t23]) ).
cnf(t36409,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t36408,t120]) ).
cnf(t152,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t36409]) ).
cnf(t975,plain,
meet(X1,join(meet(X2,complement(X1)),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t958,t152]) ).
cnf(t36600,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t975,t72]) ).
cnf(t36601,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t36600,t100]) ).
cnf(t36602,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = zero,
inference(step,[status(thm)],[t36601,t65]) ).
cnf(t1042,plain,
meet(X1,join(complement(X1),meet(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t36602]) ).
cnf(t2372,plain,
complement(X1) = join(complement(X1),meet(join(complement(X1),meet(X2,complement(X1))),complement(zero))),
inference(cp,[status(thm)],[t2357,t1042]) ).
cnf(t137,plain,
one = ifeq(meet(X1,one),zero,ifeq(one,one,complement(X1),one),one),
inference(cp,[status(thm)],[t18,t135]) ).
cnf(t36406,plain,
one = ifeq(X1,zero,ifeq(one,one,complement(X1),one),one),
inference(step,[status(thm)],[t137,t105]) ).
cnf(t36407,plain,
one = ifeq(X1,zero,complement(X1),one),
inference(step,[status(thm)],[t36406,t17]) ).
cnf(t144,plain,
ifeq(X1,zero,complement(X1),one) = one,
inference(orient,[status(thm)],[t36407]) ).
cnf(t145,plain,
one = complement(zero),
inference(cp,[status(thm)],[t144,t17]) ).
cnf(t147,plain,
complement(zero) = one,
inference(orient,[status(thm)],[t145]) ).
cnf(t36728,plain,
complement(X1) = join(complement(X1),meet(join(complement(X1),meet(X2,complement(X1))),one)),
inference(step,[status(thm)],[t2372,t147]) ).
cnf(t36729,plain,
complement(X1) = join(complement(X1),join(complement(X1),meet(X2,complement(X1)))),
inference(step,[status(thm)],[t36728,t105]) ).
cnf(t36730,plain,
complement(X1) = join(complement(X1),meet(X2,complement(X1))),
inference(step,[status(thm)],[t36729,t125]) ).
cnf(t2419,plain,
join(complement(X1),meet(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t36730]) ).
cnf(t848,plain,
meet(X1,meet(join(meet(X1,X2),meet(X2,X3)),X4)) = meet(X4,meet(X1,X2)),
inference(cp,[status(thm)],[t26,t806]) ).
cnf(t36759,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,X3)))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t848,t23]) ).
cnf(t36760,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,X3)))) = meet(X2,meet(X4,X1)),
inference(step,[status(thm)],[t36759,t26]) ).
cnf(t36761,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,X3)))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t36760,t26]) ).
cnf(t2691,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X3,X4)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t36761]) ).
cnf(t2694,plain,
meet(X1,meet(X2,X2)) = meet(X1,meet(X2,join(X3,meet(X1,join(X2,X2))))),
inference(cp,[status(thm)],[t2691,t658]) ).
cnf(t36762,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,join(X2,X2))))),
inference(step,[status(thm)],[t2694,t13]) ).
cnf(t36763,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t36762,t15]) ).
cnf(t2794,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t36763]) ).
cnf(t2808,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,meet(complement(meet(X2,X1)),complement(X2))),
inference(cp,[status(thm)],[t2794,t2357]) ).
cnf(t36764,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,meet(complement(meet(X2,X1)),complement(X2))),
inference(step,[status(thm)],[t2808,t23]) ).
cnf(t36765,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,meet(complement(X2),complement(meet(X2,X1)))),
inference(step,[status(thm)],[t36764,t23]) ).
cnf(t36766,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,meet(complement(X2),complement(meet(X1,X2)))),
inference(step,[status(thm)],[t36765,t23]) ).
cnf(t2875,plain,
meet(X1,meet(complement(X2),complement(meet(X1,X2)))) = meet(X1,complement(meet(X1,X2))),
inference(orient,[status(thm)],[t36766]) ).
cnf(t2900,plain,
meet(X1,complement(meet(X1,meet(X2,complement(X1))))) = meet(X1,meet(complement(meet(X2,complement(X1))),complement(zero))),
inference(cp,[status(thm)],[t2875,t152]) ).
cnf(t36767,plain,
meet(X1,complement(zero)) = meet(X1,meet(complement(meet(X2,complement(X1))),complement(zero))),
inference(step,[status(thm)],[t2900,t152]) ).
cnf(t36768,plain,
meet(X1,one) = meet(X1,meet(complement(meet(X2,complement(X1))),complement(zero))),
inference(step,[status(thm)],[t36767,t147]) ).
cnf(t36769,plain,
X1 = meet(X1,meet(complement(meet(X2,complement(X1))),complement(zero))),
inference(step,[status(thm)],[t36768,t105]) ).
cnf(t36770,plain,
X1 = meet(X1,meet(complement(meet(X2,complement(X1))),one)),
inference(step,[status(thm)],[t36769,t147]) ).
cnf(t36771,plain,
X1 = meet(X1,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t36770,t105]) ).
cnf(t2937,plain,
meet(X1,complement(meet(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t36771]) ).
cnf(t2943,plain,
complement(meet(X1,complement(X2))) = join(complement(meet(X1,complement(X2))),X2),
inference(cp,[status(thm)],[t2419,t2937]) ).
cnf(t36774,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(meet(X1,complement(X2)))),
inference(step,[status(thm)],[t2943,t72]) ).
cnf(t3055,plain,
join(X1,complement(meet(X2,complement(X1)))) = complement(meet(X2,complement(X1))),
inference(orient,[status(thm)],[t36774]) ).
cnf(t3059,plain,
complement(meet(X1,complement(complement(X2)))) = join(complement(X2),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t3055,t370]) ).
cnf(t36775,plain,
complement(meet(X1,X2)) = join(complement(X2),complement(meet(X1,X2))),
inference(step,[status(thm)],[t3059,t370]) ).
cnf(t3077,plain,
join(complement(X1),complement(meet(X2,X1))) = complement(meet(X2,X1)),
inference(orient,[status(thm)],[t36775]) ).
cnf(t157,plain,
meet(X1,meet(meet(X2,complement(X1)),X3)) = meet(X3,zero),
inference(cp,[status(thm)],[t26,t152]) ).
cnf(t36418,plain,
meet(X1,meet(X3,meet(X2,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t157,t23]) ).
cnf(t36419,plain,
meet(X1,meet(X2,meet(complement(X1),X3))) = meet(X3,zero),
inference(step,[status(thm)],[t36418,t26]) ).
cnf(t36420,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t36419,t23]) ).
cnf(t36421,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(step,[status(thm)],[t36420,t120]) ).
cnf(t190,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t36421]) ).
cnf(t2891,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)],[t2875,t190]) ).
cnf(t36780,plain,
meet(X1,complement(zero)) = meet(X1,meet(complement(meet(X2,meet(X3,complement(X1)))),complement(zero))),
inference(step,[status(thm)],[t2891,t190]) ).
cnf(t36781,plain,
meet(X1,one) = meet(X1,meet(complement(meet(X2,meet(X3,complement(X1)))),complement(zero))),
inference(step,[status(thm)],[t36780,t147]) ).
cnf(t36782,plain,
X1 = meet(X1,meet(complement(meet(X2,meet(X3,complement(X1)))),complement(zero))),
inference(step,[status(thm)],[t36781,t105]) ).
cnf(t36783,plain,
X1 = meet(X1,meet(complement(meet(X2,meet(X3,complement(X1)))),one)),
inference(step,[status(thm)],[t36782,t147]) ).
cnf(t36784,plain,
X1 = meet(X1,complement(meet(X2,meet(X3,complement(X1))))),
inference(step,[status(thm)],[t36783,t105]) ).
cnf(t3181,plain,
meet(X1,complement(meet(X2,meet(X3,complement(X1))))) = X1,
inference(orient,[status(thm)],[t36784]) ).
cnf(t3185,plain,
meet(X1,complement(X2)) = meet(meet(X1,complement(X2)),complement(meet(X3,X2))),
inference(cp,[status(thm)],[t3181,t2937]) ).
cnf(t36813,plain,
meet(X1,complement(X2)) = meet(meet(X1,complement(X2)),complement(meet(X2,X3))),
inference(step,[status(thm)],[t3185,t23]) ).
cnf(t3822,plain,
meet(meet(X1,complement(X2)),complement(meet(X2,X3))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t36813]) ).
cnf(t3830,plain,
meet(X1,complement(complement(X2))) = meet(meet(X1,X2),complement(meet(complement(X2),X3))),
inference(cp,[status(thm)],[t3822,t370]) ).
cnf(t36814,plain,
meet(X1,X2) = meet(meet(X1,X2),complement(meet(complement(X2),X3))),
inference(step,[status(thm)],[t3830,t370]) ).
cnf(t36815,plain,
meet(X1,X2) = meet(meet(X1,X2),complement(meet(X3,complement(X2)))),
inference(step,[status(thm)],[t36814,t23]) ).
cnf(t3894,plain,
meet(meet(X1,X2),complement(meet(X3,complement(X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t36815]) ).
cnf(t3938,plain,
complement(meet(meet(X1,X2),complement(meet(X3,complement(X2))))) = join(complement(complement(meet(X3,complement(X2)))),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t3077,t3894]) ).
cnf(t36833,plain,
complement(meet(X1,X2)) = join(complement(complement(meet(X3,complement(X2)))),complement(meet(X1,X2))),
inference(step,[status(thm)],[t3938,t3894]) ).
cnf(t36834,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(complement(meet(X3,complement(X2))))),
inference(step,[status(thm)],[t36833,t72]) ).
cnf(t36835,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),meet(X3,complement(X2))),
inference(step,[status(thm)],[t36834,t370]) ).
cnf(t36836,plain,
complement(meet(X1,X2)) = join(meet(X3,complement(X2)),complement(meet(X1,X2))),
inference(step,[status(thm)],[t36835,t72]) ).
cnf(t4361,plain,
join(meet(X1,complement(X2)),complement(meet(X3,X2))) = complement(meet(X3,X2)),
inference(orient,[status(thm)],[t36836]) ).
cnf(t2907,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,meet(complement(X2),complement(meet(X2,X1)))),
inference(cp,[status(thm)],[t2875,t23]) ).
cnf(t2939,plain,
complement(X1) = meet(complement(X1),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t2937,t370]) ).
cnf(t36772,plain,
complement(X1) = meet(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t2939,t23]) ).
cnf(t2988,plain,
meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t36772]) ).
cnf(t36858,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t2907,t2988]) ).
cnf(t4862,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t36858]) ).
cnf(t30,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t26,t14]) ).
cnf(t36412,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t30,t26]) ).
cnf(t36413,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t36412,t23]) ).
cnf(t36414,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t36413,t23]) ).
cnf(t166,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t36414]) ).
cnf(t4887,plain,
meet(X1,complement(meet(X2,join(X1,X3)))) = meet(X1,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t4862,t166]) ).
cnf(t36869,plain,
meet(X1,complement(meet(X2,join(X1,X3)))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t4887,t4862]) ).
cnf(t5078,plain,
meet(X1,complement(meet(X2,join(X1,X3)))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t36869]) ).
cnf(t3913,plain,
meet(X1,join(X1,X2)) = meet(X1,complement(meet(X3,complement(join(X1,X2))))),
inference(cp,[status(thm)],[t3894,t14]) ).
cnf(t36816,plain,
X1 = meet(X1,complement(meet(X3,complement(join(X1,X2))))),
inference(step,[status(thm)],[t3913,t14]) ).
cnf(t3996,plain,
meet(X1,complement(meet(X2,complement(join(X1,X3))))) = X1,
inference(orient,[status(thm)],[t36816]) ).
cnf(t4011,plain,
complement(meet(X1,complement(meet(X2,complement(join(X1,X3)))))) = join(complement(complement(meet(X2,complement(join(X1,X3))))),complement(X1)),
inference(cp,[status(thm)],[t3077,t3996]) ).
cnf(t36823,plain,
complement(X1) = join(complement(complement(meet(X2,complement(join(X1,X3))))),complement(X1)),
inference(step,[status(thm)],[t4011,t3996]) ).
cnf(t36824,plain,
complement(X1) = join(complement(X1),complement(complement(meet(X2,complement(join(X1,X3)))))),
inference(step,[status(thm)],[t36823,t72]) ).
cnf(t36825,plain,
complement(X1) = join(complement(X1),meet(X2,complement(join(X1,X3)))),
inference(step,[status(thm)],[t36824,t370]) ).
cnf(t4186,plain,
join(complement(X1),meet(X2,complement(join(X1,X3)))) = complement(X1),
inference(orient,[status(thm)],[t36825]) ).
cnf(t5097,plain,
meet(complement(X1),complement(X2)) = meet(complement(X1),complement(meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t5078,t4186]) ).
cnf(t5176,plain,
meet(complement(X1),complement(meet(X2,complement(X1)))) = meet(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t5097]) ).
cnf(t4024,plain,
zero = meet(meet(X1,complement(join(X2,X3))),X2),
inference(cp,[status(thm)],[t152,t3996]) ).
cnf(t36817,plain,
zero = meet(X2,meet(X1,complement(join(X2,X3)))),
inference(step,[status(thm)],[t4024,t23]) ).
cnf(t36818,plain,
zero = meet(X1,meet(complement(join(X2,X3)),X2)),
inference(step,[status(thm)],[t36817,t26]) ).
cnf(t36819,plain,
zero = meet(X1,meet(X2,complement(join(X2,X3)))),
inference(step,[status(thm)],[t36818,t23]) ).
cnf(t4071,plain,
meet(X1,meet(X2,complement(join(X2,X3)))) = zero,
inference(orient,[status(thm)],[t36819]) ).
cnf(t4072,plain,
zero = meet(X1,complement(join(X1,X2))),
inference(cp,[status(thm)],[t4071,t110]) ).
cnf(t4109,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(orient,[status(thm)],[t4072]) ).
cnf(t5180,plain,
meet(complement(join(X1,X2)),complement(X1)) = meet(complement(join(X1,X2)),complement(zero)),
inference(cp,[status(thm)],[t5176,t4109]) ).
cnf(t36873,plain,
meet(complement(join(X1,X2)),complement(X1)) = meet(complement(join(X1,X2)),one),
inference(step,[status(thm)],[t5180,t147]) ).
cnf(t36874,plain,
meet(complement(join(X1,X2)),complement(X1)) = complement(join(X1,X2)),
inference(step,[status(thm)],[t36873,t105]) ).
cnf(t36875,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(step,[status(thm)],[t36874,t23]) ).
cnf(t5369,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t36875]) ).
cnf(t5385,plain,
complement(meet(complement(X1),complement(join(X1,X2)))) = join(meet(X3,complement(complement(join(X1,X2)))),complement(complement(join(X1,X2)))),
inference(cp,[status(thm)],[t4361,t5369]) ).
cnf(t36919,plain,
complement(complement(join(X1,X2))) = join(meet(X3,complement(complement(join(X1,X2)))),complement(complement(join(X1,X2)))),
inference(step,[status(thm)],[t5385,t5369]) ).
cnf(t36920,plain,
join(X1,X2) = join(meet(X3,complement(complement(join(X1,X2)))),complement(complement(join(X1,X2)))),
inference(step,[status(thm)],[t36919,t370]) ).
cnf(t36921,plain,
join(X1,X2) = join(meet(X3,join(X1,X2)),complement(complement(join(X1,X2)))),
inference(step,[status(thm)],[t36920,t370]) ).
cnf(t36922,plain,
join(X1,X2) = join(meet(X3,join(X1,X2)),join(X1,X2)),
inference(step,[status(thm)],[t36921,t370]) ).
cnf(t36923,plain,
join(X1,X2) = join(X2,join(meet(X3,join(X1,X2)),X1)),
inference(step,[status(thm)],[t36922,t76]) ).
cnf(t36924,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t36923,t76]) ).
cnf(t6440,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t36924]) ).
cnf(t4914,plain,
X1 = ifeq(meet(X1,complement(X2)),zero,ifeq(join(X1,complement(meet(X1,X2))),one,complement(complement(meet(X1,X2))),X1),X1),
inference(cp,[status(thm)],[t343,t4862]) ).
cnf(t2996,plain,
meet(complement(X1),join(complement(meet(X1,X2)),complement(complement(X1)))) = meet(complement(X1),join(complement(complement(X1)),complement(X1))),
inference(cp,[status(thm)],[t958,t2988]) ).
cnf(t36790,plain,
meet(complement(X1),join(complement(complement(X1)),complement(meet(X1,X2)))) = meet(complement(X1),join(complement(complement(X1)),complement(X1))),
inference(step,[status(thm)],[t2996,t72]) ).
cnf(t36791,plain,
meet(complement(X1),join(X1,complement(meet(X1,X2)))) = meet(complement(X1),join(complement(complement(X1)),complement(X1))),
inference(step,[status(thm)],[t36790,t370]) ).
cnf(t36792,plain,
meet(complement(X1),join(X1,complement(meet(X1,X2)))) = meet(complement(X1),join(complement(X1),complement(complement(X1)))),
inference(step,[status(thm)],[t36791,t72]) ).
cnf(t36793,plain,
meet(complement(X1),join(X1,complement(meet(X1,X2)))) = meet(complement(X1),one),
inference(step,[status(thm)],[t36792,t96]) ).
cnf(t36794,plain,
meet(complement(X1),join(X1,complement(meet(X1,X2)))) = complement(X1),
inference(step,[status(thm)],[t36793,t105]) ).
cnf(t3321,plain,
meet(complement(X1),join(X1,complement(meet(X1,X2)))) = complement(X1),
inference(orient,[status(thm)],[t36794]) ).
cnf(t3328,plain,
complement(meet(complement(X1),join(X1,complement(meet(X1,X2))))) = join(complement(join(X1,complement(meet(X1,X2)))),complement(complement(X1))),
inference(cp,[status(thm)],[t3077,t3321]) ).
cnf(t36795,plain,
complement(complement(X1)) = join(complement(join(X1,complement(meet(X1,X2)))),complement(complement(X1))),
inference(step,[status(thm)],[t3328,t3321]) ).
cnf(t36796,plain,
X1 = join(complement(join(X1,complement(meet(X1,X2)))),complement(complement(X1))),
inference(step,[status(thm)],[t36795,t370]) ).
cnf(t36797,plain,
X1 = join(complement(complement(X1)),complement(join(X1,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t36796,t72]) ).
cnf(t36798,plain,
X1 = join(X1,complement(join(X1,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t36797,t370]) ).
cnf(t3352,plain,
join(X1,complement(join(X1,complement(meet(X1,X2))))) = X1,
inference(orient,[status(thm)],[t36798]) ).
cnf(t3366,plain,
one = join(join(X1,complement(meet(X1,X2))),X1),
inference(cp,[status(thm)],[t159,t3352]) ).
cnf(t36799,plain,
one = join(X1,join(X1,complement(meet(X1,X2)))),
inference(step,[status(thm)],[t3366,t72]) ).
cnf(t36800,plain,
one = join(X1,complement(meet(X1,X2))),
inference(step,[status(thm)],[t36799,t125]) ).
cnf(t3384,plain,
join(X1,complement(meet(X1,X2))) = one,
inference(orient,[status(thm)],[t36800]) ).
cnf(t36938,plain,
X1 = ifeq(meet(X1,complement(X2)),zero,ifeq(one,one,complement(complement(meet(X1,X2))),X1),X1),
inference(step,[status(thm)],[t4914,t3384]) ).
cnf(t36939,plain,
X1 = ifeq(meet(X1,complement(X2)),zero,complement(complement(meet(X1,X2))),X1),
inference(step,[status(thm)],[t36938,t17]) ).
cnf(t36940,plain,
X1 = ifeq(meet(X1,complement(X2)),zero,meet(X1,X2),X1),
inference(step,[status(thm)],[t36939,t370]) ).
cnf(t7177,plain,
ifeq(meet(X1,complement(X2)),zero,meet(X1,X2),X1) = X1,
inference(orient,[status(thm)],[t36940]) ).
cnf(t7191,plain,
X1 = ifeq(meet(X1,X2),zero,meet(X1,complement(X2)),X1),
inference(cp,[status(thm)],[t7177,t370]) ).
cnf(t8154,plain,
ifeq(meet(X1,X2),zero,meet(X1,complement(X2)),X1) = X1,
inference(orient,[status(thm)],[t7191]) ).
cnf(t5388,plain,
meet(X1,complement(complement(X2))) = meet(meet(X1,complement(complement(X2))),complement(complement(join(X2,X3)))),
inference(cp,[status(thm)],[t3822,t5369]) ).
cnf(t36880,plain,
meet(X1,X2) = meet(meet(X1,complement(complement(X2))),complement(complement(join(X2,X3)))),
inference(step,[status(thm)],[t5388,t370]) ).
cnf(t36881,plain,
meet(X1,X2) = meet(meet(X1,X2),complement(complement(join(X2,X3)))),
inference(step,[status(thm)],[t36880,t370]) ).
cnf(t36882,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t36881,t370]) ).
cnf(t5469,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t36882]) ).
cnf(t5540,plain,
meet(meet(X1,X2),complement(join(X2,X3))) = meet(meet(X1,X2),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t4862,t5469]) ).
cnf(t36883,plain,
meet(meet(X1,X2),complement(join(X2,X3))) = zero,
inference(step,[status(thm)],[t5540,t65]) ).
cnf(t5581,plain,
meet(meet(X1,X2),complement(join(X2,X3))) = zero,
inference(orient,[status(thm)],[t36883]) ).
cnf(t5623,plain,
zero = meet(meet(X1,X2),complement(join(X1,X3))),
inference(cp,[status(thm)],[t5581,t23]) ).
cnf(t5684,plain,
meet(meet(X1,X2),complement(join(X1,X3))) = zero,
inference(orient,[status(thm)],[t5623]) ).
cnf(t5688,plain,
zero = meet(complement(join(X1,X2)),complement(join(complement(X1),X3))),
inference(cp,[status(thm)],[t5684,t5369]) ).
cnf(t36950,plain,
zero = meet(complement(join(X1,X2)),complement(join(X3,complement(X1)))),
inference(step,[status(thm)],[t5688,t72]) ).
cnf(t7487,plain,
meet(complement(join(X1,X2)),complement(join(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t36950]) ).
cnf(t969,plain,
meet(X1,join(meet(X2,meet(X3,complement(X1))),complement(X1))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t958,t190]) ).
cnf(t36623,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = meet(X1,join(complement(X1),zero)),
inference(step,[status(thm)],[t969,t72]) ).
cnf(t36624,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t36623,t100]) ).
cnf(t36625,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = zero,
inference(step,[status(thm)],[t36624,t65]) ).
cnf(t1221,plain,
meet(X1,join(complement(X1),meet(X2,meet(X3,complement(X1))))) = zero,
inference(orient,[status(thm)],[t36625]) ).
cnf(t2373,plain,
complement(X1) = join(complement(X1),meet(join(complement(X1),meet(X2,meet(X3,complement(X1)))),complement(zero))),
inference(cp,[status(thm)],[t2357,t1221]) ).
cnf(t36731,plain,
complement(X1) = join(complement(X1),meet(join(complement(X1),meet(X2,meet(X3,complement(X1)))),one)),
inference(step,[status(thm)],[t2373,t147]) ).
cnf(t36732,plain,
complement(X1) = join(complement(X1),join(complement(X1),meet(X2,meet(X3,complement(X1))))),
inference(step,[status(thm)],[t36731,t105]) ).
cnf(t36733,plain,
complement(X1) = join(complement(X1),meet(X2,meet(X3,complement(X1)))),
inference(step,[status(thm)],[t36732,t125]) ).
cnf(t2437,plain,
join(complement(X1),meet(X2,meet(X3,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t36733]) ).
cnf(t3011,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),meet(X3,complement(X1))),
inference(cp,[status(thm)],[t2437,t2988]) ).
cnf(t36812,plain,
complement(meet(X1,X2)) = join(meet(X3,complement(X1)),complement(meet(X1,X2))),
inference(step,[status(thm)],[t3011,t72]) ).
cnf(t3778,plain,
join(meet(X1,complement(X2)),complement(meet(X2,X3))) = complement(meet(X2,X3)),
inference(orient,[status(thm)],[t36812]) ).
cnf(t7505,plain,
zero = meet(complement(join(meet(X1,X2),X3)),complement(complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t7487,t3778]) ).
cnf(t36967,plain,
zero = meet(complement(join(meet(X1,X2),X3)),meet(X1,X2)),
inference(step,[status(thm)],[t7505,t370]) ).
cnf(t36968,plain,
zero = meet(X2,meet(complement(join(meet(X1,X2),X3)),X1)),
inference(step,[status(thm)],[t36967,t26]) ).
cnf(t36969,plain,
zero = meet(X1,meet(X2,complement(join(meet(X1,X2),X3)))),
inference(step,[status(thm)],[t36968,t26]) ).
cnf(t36970,plain,
zero = meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t36969,t72]) ).
cnf(t8288,plain,
meet(X1,meet(X2,complement(join(X3,meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t36970]) ).
cnf(t8290,plain,
zero = meet(X1,complement(join(X2,meet(X1,complement(X2))))),
inference(cp,[status(thm)],[t8288,t5369]) ).
cnf(t8394,plain,
meet(X1,complement(join(X2,meet(X1,complement(X2))))) = zero,
inference(orient,[status(thm)],[t8290]) ).
cnf(t8402,plain,
X1 = ifeq(zero,zero,meet(X1,complement(complement(join(X2,meet(X1,complement(X2)))))),X1),
inference(cp,[status(thm)],[t8154,t8394]) ).
cnf(t36971,plain,
X1 = meet(X1,complement(complement(join(X2,meet(X1,complement(X2)))))),
inference(step,[status(thm)],[t8402,t17]) ).
cnf(t36972,plain,
X1 = meet(X1,join(X2,meet(X1,complement(X2)))),
inference(step,[status(thm)],[t36971,t370]) ).
cnf(t8444,plain,
meet(X1,join(X2,meet(X1,complement(X2)))) = X1,
inference(orient,[status(thm)],[t36972]) ).
cnf(t8490,plain,
join(X1,meet(X2,complement(X1))) = join(X1,join(meet(X2,complement(X1)),X2)),
inference(cp,[status(thm)],[t6440,t8444]) ).
cnf(t36997,plain,
join(X1,meet(X2,complement(X1))) = join(X1,join(X2,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t8490,t72]) ).
cnf(t36998,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(step,[status(thm)],[t36997,t16]) ).
cnf(t10017,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t36998]) ).
cnf(t10042,plain,
join(complement(X1),X2) = join(complement(X1),meet(X2,X1)),
inference(cp,[status(thm)],[t10017,t370]) ).
cnf(t37003,plain,
join(X2,complement(X1)) = join(complement(X1),meet(X2,X1)),
inference(step,[status(thm)],[t10042,t72]) ).
cnf(t37004,plain,
join(X2,complement(X1)) = join(complement(X1),meet(X1,X2)),
inference(step,[status(thm)],[t37003,t23]) ).
cnf(t10086,plain,
join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t37004]) ).
cnf(t10147,plain,
join(meet(X1,join(X2,X3)),complement(X2)) = join(complement(X2),meet(X2,X1)),
inference(cp,[status(thm)],[t10086,t166]) ).
cnf(t37086,plain,
join(complement(X2),meet(X1,join(X2,X3))) = join(complement(X2),meet(X2,X1)),
inference(step,[status(thm)],[t10147,t72]) ).
cnf(t37087,plain,
join(complement(X2),meet(X1,join(X2,X3))) = join(X1,complement(X2)),
inference(step,[status(thm)],[t37086,t10086]) ).
cnf(t12554,plain,
join(complement(X1),meet(X2,join(X1,X3))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t37087]) ).
cnf(t5371,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(join(complement(X1),X2))),
inference(cp,[status(thm)],[t5369,t370]) ).
cnf(t36890,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t5371,t72]) ).
cnf(t36891,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(join(X2,complement(X1)))),
inference(step,[status(thm)],[t36890,t72]) ).
cnf(t5828,plain,
meet(X1,complement(join(X2,complement(X1)))) = complement(join(X2,complement(X1))),
inference(orient,[status(thm)],[t36891]) ).
cnf(t5833,plain,
complement(join(X1,complement(complement(X2)))) = meet(complement(X2),complement(join(X1,X2))),
inference(cp,[status(thm)],[t5828,t370]) ).
cnf(t36896,plain,
complement(join(X1,X2)) = meet(complement(X2),complement(join(X1,X2))),
inference(step,[status(thm)],[t5833,t370]) ).
cnf(t5961,plain,
meet(complement(X1),complement(join(X2,X1))) = complement(join(X2,X1)),
inference(orient,[status(thm)],[t36896]) ).
cnf(t6006,plain,
meet(complement(join(X1,X2)),complement(complement(X2))) = meet(complement(join(X1,X2)),complement(complement(join(X1,X2)))),
inference(cp,[status(thm)],[t5176,t5961]) ).
cnf(t36897,plain,
meet(complement(complement(X2)),complement(join(X1,X2))) = meet(complement(join(X1,X2)),complement(complement(join(X1,X2)))),
inference(step,[status(thm)],[t6006,t23]) ).
cnf(t36898,plain,
meet(X2,complement(join(X1,X2))) = meet(complement(join(X1,X2)),complement(complement(join(X1,X2)))),
inference(step,[status(thm)],[t36897,t370]) ).
cnf(t36899,plain,
meet(X2,complement(join(X1,X2))) = zero,
inference(step,[status(thm)],[t36898,t65]) ).
cnf(t6037,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t36899]) ).
cnf(t80,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t76,t16]) ).
cnf(t36415,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t80,t76]) ).
cnf(t36416,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t36415,t72]) ).
cnf(t36417,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t36416,t72]) ).
cnf(t178,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t36417]) ).
cnf(t6042,plain,
zero = meet(join(X1,meet(X2,X3)),complement(join(X2,X1))),
inference(cp,[status(thm)],[t6037,t178]) ).
cnf(t36962,plain,
zero = meet(complement(join(X2,X1)),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t6042,t23]) ).
cnf(t36963,plain,
zero = meet(complement(join(X1,X2)),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t36962,t72]) ).
cnf(t7818,plain,
meet(complement(join(X1,X2)),join(X1,meet(X2,X3))) = zero,
inference(orient,[status(thm)],[t36963]) ).
cnf(t7855,plain,
zero = meet(complement(join(X1,X2)),join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t7818,t72]) ).
cnf(t8746,plain,
meet(complement(join(X1,X2)),join(X2,meet(X1,X3))) = zero,
inference(orient,[status(thm)],[t7855]) ).
cnf(t10183,plain,
join(complement(meet(X1,complement(X2))),complement(complement(X2))) = join(complement(complement(X2)),meet(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t10086,t5176]) ).
cnf(t37023,plain,
join(complement(complement(X2)),complement(meet(X1,complement(X2)))) = join(complement(complement(X2)),meet(complement(X2),complement(X1))),
inference(step,[status(thm)],[t10183,t72]) ).
cnf(t37024,plain,
complement(meet(X1,complement(X2))) = join(complement(complement(X2)),meet(complement(X2),complement(X1))),
inference(step,[status(thm)],[t37023,t3077]) ).
cnf(t37025,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),complement(complement(X2))),
inference(step,[status(thm)],[t37024,t10086]) ).
cnf(t37026,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(step,[status(thm)],[t37025,t370]) ).
cnf(t37027,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
inference(step,[status(thm)],[t37026,t72]) ).
cnf(t10759,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t37027]) ).
cnf(t10786,plain,
join(complement(X1),complement(X2)) = complement(meet(X2,X1)),
inference(cp,[status(thm)],[t10759,t370]) ).
cnf(t37042,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t10786,t23]) ).
cnf(t10920,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t37042]) ).
cnf(t10934,plain,
zero = meet(complement(complement(meet(X1,X2))),join(complement(X2),meet(complement(X1),X3))),
inference(cp,[status(thm)],[t8746,t10920]) ).
cnf(t37367,plain,
zero = meet(meet(X1,X2),join(complement(X2),meet(complement(X1),X3))),
inference(step,[status(thm)],[t10934,t370]) ).
cnf(t37368,plain,
zero = meet(meet(X1,X2),join(complement(X2),meet(X3,complement(X1)))),
inference(step,[status(thm)],[t37367,t23]) ).
cnf(t34598,plain,
meet(meet(X1,X2),join(complement(X2),meet(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t37368]) ).
cnf(t34755,plain,
join(meet(X1,X2),complement(complement(X2))) = join(complement(complement(X2)),zero),
inference(cp,[status(thm)],[t12554,t34598]) ).
cnf(t37369,plain,
join(meet(X1,X2),X2) = join(complement(complement(X2)),zero),
inference(step,[status(thm)],[t34755,t370]) ).
cnf(t37370,plain,
join(X2,meet(X1,X2)) = join(complement(complement(X2)),zero),
inference(step,[status(thm)],[t37369,t72]) ).
cnf(t37371,plain,
join(X2,meet(X1,X2)) = complement(complement(X2)),
inference(step,[status(thm)],[t37370,t100]) ).
cnf(t37372,plain,
join(X2,meet(X1,X2)) = X2,
inference(step,[status(thm)],[t37371,t370]) ).
cnf(t34805,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t37372]) ).
cnf(t34837,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X2,X1)),
inference(cp,[status(thm)],[t34805,t166]) ).
cnf(t37386,plain,
meet(X1,join(X2,X3)) = join(meet(X2,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t34837,t72]) ).
cnf(t37387,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t37386,t23]) ).
cnf(t35780,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t37387]) ).
cnf(t35811,plain,
meet(X1,join(meet(X1,X2),X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t35780,t110]) ).
cnf(t37388,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t35811,t72]) ).
cnf(t4966,plain,
meet(X1,meet(complement(meet(X1,X2)),X3)) = meet(X3,meet(X1,complement(X2))),
inference(cp,[status(thm)],[t26,t4862]) ).
cnf(t36989,plain,
meet(X1,meet(X3,complement(meet(X1,X2)))) = meet(X3,meet(X1,complement(X2))),
inference(step,[status(thm)],[t4966,t23]) ).
cnf(t36990,plain,
meet(X1,meet(X3,complement(meet(X1,X2)))) = meet(X1,meet(complement(X2),X3)),
inference(step,[status(thm)],[t36989,t26]) ).
cnf(t36991,plain,
meet(X1,meet(X3,complement(meet(X1,X2)))) = meet(X1,meet(X3,complement(X2))),
inference(step,[status(thm)],[t36990,t23]) ).
cnf(t9809,plain,
meet(X1,meet(X2,complement(meet(X1,X3)))) = meet(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t36991]) ).
cnf(t10794,plain,
meet(X1,complement(X2)) = complement(join(X2,complement(X1))),
inference(cp,[status(thm)],[t370,t10759]) ).
cnf(t11013,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t10794]) ).
cnf(t11019,plain,
meet(complement(X1),complement(X2)) = complement(join(X2,X1)),
inference(cp,[status(thm)],[t11013,t370]) ).
cnf(t37053,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(step,[status(thm)],[t11019,t72]) ).
cnf(t11128,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t37053]) ).
cnf(t11187,plain,
meet(X1,meet(complement(X2),complement(X3))) = meet(X1,complement(join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t9809,t11128]) ).
cnf(t37250,plain,
meet(X1,complement(join(X2,X3))) = meet(X1,complement(join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t11187,t11128]) ).
cnf(t24070,plain,
meet(X1,complement(join(X2,meet(X1,X3)))) = meet(X1,complement(join(X2,X3))),
inference(orient,[status(thm)],[t37250]) ).
cnf(t24207,plain,
meet(X1,complement(complement(join(X2,meet(X1,X3))))) = meet(X1,complement(meet(X1,complement(join(X2,X3))))),
inference(cp,[status(thm)],[t4862,t24070]) ).
cnf(t37251,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,complement(meet(X1,complement(join(X2,X3))))),
inference(step,[status(thm)],[t24207,t370]) ).
cnf(t37252,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,complement(complement(join(X2,X3)))),
inference(step,[status(thm)],[t37251,t4862]) ).
cnf(t37253,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t37252,t370]) ).
cnf(t24273,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t37253]) ).
cnf(t37389,plain,
meet(X1,join(X3,X2)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t37388,t24273]) ).
cnf(t37390,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t37389,t72]) ).
cnf(t11157,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t10017,t11128]) ).
cnf(t37063,plain,
join(X1,complement(X2)) = join(X1,complement(join(X1,X2))),
inference(step,[status(thm)],[t11157,t72]) ).
cnf(t11410,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t37063]) ).
cnf(t11018,plain,
meet(meet(X1,complement(X2)),complement(X3)) = complement(join(X3,join(X2,complement(X1)))),
inference(cp,[status(thm)],[t11013,t10759]) ).
cnf(t37131,plain,
meet(complement(X3),meet(X1,complement(X2))) = complement(join(X3,join(X2,complement(X1)))),
inference(step,[status(thm)],[t11018,t23]) ).
cnf(t37132,plain,
meet(complement(X2),meet(complement(X3),X1)) = complement(join(X3,join(X2,complement(X1)))),
inference(step,[status(thm)],[t37131,t26]) ).
cnf(t37133,plain,
meet(X1,meet(complement(X2),complement(X3))) = complement(join(X3,join(X2,complement(X1)))),
inference(step,[status(thm)],[t37132,t26]) ).
cnf(t37134,plain,
meet(X1,complement(join(X2,X3))) = complement(join(X3,join(X2,complement(X1)))),
inference(step,[status(thm)],[t37133,t11128]) ).
cnf(t37135,plain,
meet(X1,complement(join(X2,X3))) = complement(join(X2,join(complement(X1),X3))),
inference(step,[status(thm)],[t37134,t76]) ).
cnf(t37136,plain,
meet(X1,complement(join(X2,X3))) = complement(join(X2,join(X3,complement(X1)))),
inference(step,[status(thm)],[t37135,t72]) ).
cnf(t14684,plain,
complement(join(X1,join(X2,complement(X3)))) = meet(X3,complement(join(X1,X2))),
inference(orient,[status(thm)],[t37136]) ).
cnf(t14735,plain,
join(X1,complement(join(X2,complement(X3)))) = join(X1,meet(X3,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t11410,t14684]) ).
cnf(t37289,plain,
join(X1,meet(X3,complement(X2))) = join(X1,meet(X3,complement(join(X1,X2)))),
inference(step,[status(thm)],[t14735,t11013]) ).
cnf(t27226,plain,
join(X1,meet(X2,complement(join(X1,X3)))) = join(X1,meet(X2,complement(X3))),
inference(orient,[status(thm)],[t37289]) ).
cnf(t27258,plain,
join(X1,meet(X2,complement(complement(join(X1,X3))))) = join(X1,meet(X2,complement(join(X1,complement(X3))))),
inference(cp,[status(thm)],[t27226,t11410]) ).
cnf(t37290,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,complement(join(X1,complement(X3))))),
inference(step,[status(thm)],[t27258,t370]) ).
cnf(t37291,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,complement(complement(X3)))),
inference(step,[status(thm)],[t37290,t27226]) ).
cnf(t37292,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t37291,t370]) ).
cnf(t27385,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t37292]) ).
cnf(t37391,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,X3)),
inference(step,[status(thm)],[t37390,t27385]) ).
cnf(t36032,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t37391]) ).
cnf(f12,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f12_nnf,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(goal_0,negated_conjecture,
join(meet(a,b),meet(a,c)) != meet(a,join(b,c)),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(g0_0,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[goal_0,t36032]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT214-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 20:34:37 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 40.62/6.06 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.62/6.06 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------