%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT252-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 : n007.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:25 PM UTC 2026
% Result : Unsatisfiable 91.56s 12.59s
% Output : Proof 91.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 223
% Number of leaves : 15
% Syntax : Number of formulae : 789 ( 785 unt; 0 def)
% Number of atoms : 797 ( 796 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 : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-4 aty)
% Number of variables : 1927 ( 555 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(t12,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t19,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(f11,axiom,
meet(X,join(Y,meet(Z,join(Y,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Y,join(X,Z)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H70) ).
fof(f11_nnf,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(Y,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Y,join(X,Z)))))),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(Y,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Y,join(X,Z)))))),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(X1,meet(X2,join(X1,X3)))) = meet(X0,join(X1,meet(X2,join(X3,meet(X1,join(X0,X2)))))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t13,plain,
meet(X1,join(X2,meet(X3,join(X4,meet(X2,join(X1,X3)))))) = meet(X1,join(X2,meet(X3,join(X2,X4)))),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t47,plain,
meet(X1,join(X2,meet(X3,join(X4,meet(X2,join(X1,X3)))))) = meet(X1,join(X2,meet(X3,join(X2,X4)))),
inference(orient,[status(thm)],[t13]) ).
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(t16,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t52,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,meet(X1,join(X3,meet(X2,X1))))),
inference(cp,[status(thm)],[t47,t16]) ).
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(t8,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t24,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t201728,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,meet(X1,join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t52,t24]) ).
cnf(t1299,plain,
meet(X1,join(X2,meet(X1,join(X3,meet(X1,X2))))) = meet(X1,join(X2,meet(X1,join(X2,X3)))),
inference(orient,[status(thm)],[t201728]) ).
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(t4,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t58,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t1330,plain,
meet(X1,join(complement(X1),meet(X1,join(complement(X1),X2)))) = meet(X1,join(complement(X1),meet(X1,join(X2,zero)))),
inference(cp,[status(thm)],[t1299,t58]) ).
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(t6,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t68,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t201737,plain,
meet(X1,join(complement(X1),meet(X1,join(X2,complement(X1))))) = meet(X1,join(complement(X1),meet(X1,join(X2,zero)))),
inference(step,[status(thm)],[t1330,t68]) ).
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(t7,plain,
join(X1,meet(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t17,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t59,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t17,t58]) ).
cnf(t100,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t59]) ).
cnf(t201738,plain,
meet(X1,join(complement(X1),meet(X1,join(X2,complement(X1))))) = meet(X1,join(complement(X1),meet(X1,X2))),
inference(step,[status(thm)],[t201737,t100]) ).
cnf(t1371,plain,
meet(X1,join(complement(X1),meet(X1,join(X2,complement(X1))))) = meet(X1,join(complement(X1),meet(X1,X2))),
inference(orient,[status(thm)],[t201738]) ).
cnf(t26,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X2,X1),one,complement(X2),X1),X1),
inference(cp,[status(thm)],[t19,t24]) ).
cnf(t201657,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(step,[status(thm)],[t26,t68]) ).
cnf(t740,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t201657]) ).
cnf(t749,plain,
X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t740,t58]) ).
cnf(t5,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t18,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t201658,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t749,t18]) ).
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(t3,plain,
join(X1,complement(X1)) = one,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t95,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t201659,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t201658,t95]) ).
cnf(t201660,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t201659,t18]) ).
cnf(t784,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t201660]) ).
cnf(t1372,plain,
meet(complement(X1),join(complement(complement(X1)),meet(complement(X1),X2))) = meet(complement(X1),join(X1,meet(complement(X1),join(X2,complement(complement(X1)))))),
inference(cp,[status(thm)],[t1371,t784]) ).
cnf(t201859,plain,
meet(complement(X1),join(X1,meet(complement(X1),X2))) = meet(complement(X1),join(X1,meet(complement(X1),join(X2,complement(complement(X1)))))),
inference(step,[status(thm)],[t1372,t784]) ).
cnf(t201860,plain,
meet(complement(X1),join(X1,meet(X2,complement(X1)))) = meet(complement(X1),join(X1,meet(complement(X1),join(X2,complement(complement(X1)))))),
inference(step,[status(thm)],[t201859,t24]) ).
cnf(t201861,plain,
meet(complement(X1),join(X1,meet(X2,complement(X1)))) = meet(complement(X1),join(X1,meet(complement(X1),join(X2,X1)))),
inference(step,[status(thm)],[t201860,t784]) ).
cnf(t201862,plain,
meet(complement(X1),join(X1,meet(X2,complement(X1)))) = meet(complement(X1),join(X1,meet(complement(X1),join(X1,X2)))),
inference(step,[status(thm)],[t201861,t68]) ).
cnf(t2746,plain,
meet(complement(X1),join(X1,meet(complement(X1),join(X1,X2)))) = meet(complement(X1),join(X1,meet(X2,complement(X1)))),
inference(orient,[status(thm)],[t201862]) ).
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(t11,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t201516,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t11,t24]) ).
cnf(t27,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t201516]) ).
cnf(t103,plain,
meet(X1,join(X2,meet(zero,join(X2,X3)))) = meet(X1,join(X2,meet(zero,join(X3,meet(X2,X1))))),
inference(cp,[status(thm)],[t47,t100]) ).
cnf(t201739,plain,
meet(X1,join(X2,meet(zero,join(X2,X3)))) = meet(X1,join(X2,meet(zero,join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t103,t24]) ).
cnf(t1384,plain,
meet(X1,join(X2,meet(zero,join(X3,meet(X1,X2))))) = meet(X1,join(X2,meet(zero,join(X2,X3)))),
inference(orient,[status(thm)],[t201739]) ).
cnf(t1389,plain,
meet(X1,join(X2,meet(zero,join(X2,X1)))) = meet(X1,join(X2,meet(zero,X1))),
inference(cp,[status(thm)],[t1384,t17]) ).
cnf(t201741,plain,
meet(X1,join(X2,meet(zero,join(X1,X2)))) = meet(X1,join(X2,meet(zero,X1))),
inference(step,[status(thm)],[t1389,t68]) ).
cnf(t201742,plain,
meet(X1,join(X2,meet(zero,join(X1,X2)))) = meet(X1,join(X2,meet(X1,zero))),
inference(step,[status(thm)],[t201741,t24]) ).
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(t14,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t30,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t27,t14]) ).
cnf(t201518,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t30,t27]) ).
cnf(t201519,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t201518,t24]) ).
cnf(t116,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t201519]) ).
cnf(t119,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t116,t58]) ).
cnf(t201520,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t119,t58]) ).
cnf(t126,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t201520]) ).
cnf(t201743,plain,
meet(X1,join(X2,meet(zero,join(X1,X2)))) = meet(X1,join(X2,zero)),
inference(step,[status(thm)],[t201742,t126]) ).
cnf(t201744,plain,
meet(X1,join(X2,meet(zero,join(X1,X2)))) = meet(X1,X2),
inference(step,[status(thm)],[t201743,t100]) ).
cnf(t1457,plain,
meet(X1,join(X2,meet(zero,join(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t201744]) ).
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(t9,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t15,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t48,plain,
meet(X1,join(X2,meet(X3,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(cp,[status(thm)],[t47,t15]) ).
cnf(t252,plain,
meet(X1,join(X2,meet(X3,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t48]) ).
cnf(t253,plain,
meet(join(X1,meet(X2,join(X1,X2))),join(X1,X2)) = join(X1,meet(X2,join(X1,X2))),
inference(cp,[status(thm)],[t252,t14]) ).
cnf(t201596,plain,
meet(join(X1,X2),join(X1,meet(X2,join(X1,X2)))) = join(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t253,t24]) ).
cnf(t201597,plain,
meet(join(X1,X2),join(X1,X2)) = join(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t201596,t252]) ).
cnf(t201598,plain,
join(X1,X2) = join(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t201597,t14]) ).
cnf(t337,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t201598]) ).
cnf(t1469,plain,
meet(X1,meet(X2,join(X1,X2))) = meet(X1,join(meet(X2,join(X1,X2)),meet(zero,join(X1,X2)))),
inference(cp,[status(thm)],[t1457,t337]) ).
cnf(t31,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t27,t15]) ).
cnf(t201532,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t31,t27]) ).
cnf(t201533,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t201532,t24]) ).
cnf(t201534,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t201533,t24]) ).
cnf(t175,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t201534]) ).
cnf(t201751,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X2)),meet(zero,join(X1,X2)))),
inference(step,[status(thm)],[t1469,t175]) ).
cnf(t1629,plain,
meet(X1,join(meet(X2,join(X1,X2)),meet(zero,join(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t201751]) ).
cnf(t1638,plain,
meet(X1,meet(X1,X2)) = meet(X1,join(meet(meet(X1,X2),X1),meet(zero,join(X1,meet(X1,X2))))),
inference(cp,[status(thm)],[t1629,t17]) ).
cnf(t201752,plain,
meet(X1,X2) = meet(X1,join(meet(meet(X1,X2),X1),meet(zero,join(X1,meet(X1,X2))))),
inference(step,[status(thm)],[t1638,t116]) ).
cnf(t201753,plain,
meet(X1,X2) = meet(X1,join(meet(meet(X1,X2),X1),meet(zero,X1))),
inference(step,[status(thm)],[t201752,t17]) ).
cnf(t201754,plain,
meet(X1,X2) = meet(X1,join(meet(zero,X1),meet(meet(X1,X2),X1))),
inference(step,[status(thm)],[t201753,t68]) ).
cnf(t201755,plain,
meet(X1,X2) = meet(X1,join(meet(X1,zero),meet(meet(X1,X2),X1))),
inference(step,[status(thm)],[t201754,t24]) ).
cnf(t201756,plain,
meet(X1,X2) = meet(X1,join(zero,meet(meet(X1,X2),X1))),
inference(step,[status(thm)],[t201755,t126]) ).
cnf(t201757,plain,
meet(X1,X2) = meet(X1,join(zero,meet(X1,meet(X1,X2)))),
inference(step,[status(thm)],[t201756,t24]) ).
cnf(t201758,plain,
meet(X1,X2) = meet(X1,join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t201757,t116]) ).
cnf(t1678,plain,
meet(X1,join(zero,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t201758]) ).
cnf(t1709,plain,
meet(X1,meet(join(zero,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t27,t1678]) ).
cnf(t201776,plain,
meet(X1,meet(X3,join(zero,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t1709,t24]) ).
cnf(t201777,plain,
meet(X1,meet(X3,join(zero,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t201776,t27]) ).
cnf(t201778,plain,
meet(X1,meet(X3,join(zero,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t201777,t27]) ).
cnf(t1906,plain,
meet(X1,meet(X2,join(zero,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t201778]) ).
cnf(t55,plain,
meet(X1,join(X2,meet(meet(X3,join(X4,meet(X1,join(X2,X3)))),join(X2,Y4)))) = meet(X1,join(X2,meet(meet(X3,join(X4,meet(X1,join(X2,X3)))),join(Y4,meet(X2,join(X1,meet(X3,join(X1,X4)))))))),
inference(cp,[status(thm)],[t47,t47]) ).
cnf(t202275,plain,
meet(X1,join(X2,meet(join(X2,Y4),meet(X3,join(X4,meet(X1,join(X2,X3))))))) = meet(X1,join(X2,meet(meet(X3,join(X4,meet(X1,join(X2,X3)))),join(Y4,meet(X2,join(X1,meet(X3,join(X1,X4)))))))),
inference(step,[status(thm)],[t55,t24]) ).
cnf(t202276,plain,
meet(X1,join(X2,meet(X3,meet(join(X4,meet(X1,join(X2,X3))),join(X2,Y4))))) = meet(X1,join(X2,meet(meet(X3,join(X4,meet(X1,join(X2,X3)))),join(Y4,meet(X2,join(X1,meet(X3,join(X1,X4)))))))),
inference(step,[status(thm)],[t202275,t27]) ).
cnf(t202277,plain,
meet(X1,join(X2,meet(X3,meet(join(X2,Y4),join(X4,meet(X1,join(X2,X3))))))) = meet(X1,join(X2,meet(meet(X3,join(X4,meet(X1,join(X2,X3)))),join(Y4,meet(X2,join(X1,meet(X3,join(X1,X4)))))))),
inference(step,[status(thm)],[t202276,t24]) ).
cnf(t10286,plain,
meet(X1,join(X2,meet(meet(X3,join(X4,meet(X1,join(X2,X3)))),join(Y4,meet(X2,join(X1,meet(X3,join(X1,X4)))))))) = meet(X1,join(X2,meet(X3,meet(join(X2,Y4),join(X4,meet(X1,join(X2,X3))))))),
inference(orient,[status(thm)],[t202277]) ).
cnf(t53,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X2,X4)))) = meet(X1,join(X2,meet(meet(X1,X3),join(X4,meet(X2,X1))))),
inference(cp,[status(thm)],[t47,t17]) ).
cnf(t201985,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X2,X4)))) = meet(X1,join(X2,meet(meet(X1,X3),join(X4,meet(X1,X2))))),
inference(step,[status(thm)],[t53,t24]) ).
cnf(t4576,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X4,meet(X1,X2))))) = meet(X1,join(X2,meet(meet(X1,X3),join(X2,X4)))),
inference(orient,[status(thm)],[t201985]) ).
cnf(t4589,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X2,X1)))) = meet(X1,join(X2,meet(meet(X1,X3),X1))),
inference(cp,[status(thm)],[t4576,t17]) ).
cnf(t201988,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X1,X2)))) = meet(X1,join(X2,meet(meet(X1,X3),X1))),
inference(step,[status(thm)],[t4589,t68]) ).
cnf(t201989,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X1,X2)))) = meet(X1,join(X2,meet(X1,meet(X1,X3)))),
inference(step,[status(thm)],[t201988,t24]) ).
cnf(t201990,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t201989,t116]) ).
cnf(t4715,plain,
meet(X1,join(X2,meet(meet(X1,X3),join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t201990]) ).
cnf(t4726,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(meet(X3,meet(X4,X1)),join(X1,X2)))),
inference(cp,[status(thm)],[t4715,t27]) ).
cnf(t202183,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(join(X1,X2),meet(X3,meet(X4,X1))))),
inference(step,[status(thm)],[t4726,t24]) ).
cnf(t202184,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(meet(X4,X1),meet(join(X1,X2),X3)))),
inference(step,[status(thm)],[t202183,t27]) ).
cnf(t202185,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(X3,meet(meet(X4,X1),join(X1,X2))))),
inference(step,[status(thm)],[t202184,t27]) ).
cnf(t202186,plain,
meet(X1,join(X2,meet(X1,meet(X3,X4)))) = meet(X1,join(X2,meet(X3,meet(meet(X1,X4),join(X1,X2))))),
inference(step,[status(thm)],[t202185,t24]) ).
cnf(t7867,plain,
meet(X1,join(X2,meet(X3,meet(meet(X1,X4),join(X1,X2))))) = meet(X1,join(X2,meet(X1,meet(X3,X4)))),
inference(orient,[status(thm)],[t202186]) ).
cnf(t7868,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,X2),
inference(cp,[status(thm)],[t7867,t17]) ).
cnf(t8046,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t7868]) ).
cnf(t8050,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t8046,t175]) ).
cnf(t8168,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t8050]) ).
cnf(t8182,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t8168,t175]) ).
cnf(t202204,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(step,[status(thm)],[t8182,t175]) ).
cnf(t202205,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t202204,t68]) ).
cnf(t8764,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t202205]) ).
cnf(t10291,plain,
meet(X1,join(X2,meet(X2,meet(join(X2,X3),join(meet(X2,X1),meet(X1,join(X2,X2))))))) = meet(X1,join(X2,meet(meet(X2,X1),join(X3,meet(X2,join(X1,meet(X2,join(X1,meet(X2,X1))))))))),
inference(cp,[status(thm)],[t10286,t8764]) ).
cnf(t202304,plain,
meet(X1,X2) = meet(X1,join(X2,meet(meet(X2,X1),join(X3,meet(X2,join(X1,meet(X2,join(X1,meet(X2,X1))))))))),
inference(step,[status(thm)],[t10291,t17]) ).
cnf(t202305,plain,
meet(X1,X2) = meet(X1,join(X2,meet(meet(X1,X2),join(X3,meet(X2,join(X1,meet(X2,join(X1,meet(X2,X1))))))))),
inference(step,[status(thm)],[t202304,t24]) ).
cnf(t202306,plain,
meet(X1,X2) = meet(X1,join(X2,meet(meet(X1,X2),join(X3,meet(X2,join(X1,meet(X2,join(X1,X1)))))))),
inference(step,[status(thm)],[t202305,t1299]) ).
cnf(t202307,plain,
meet(X1,X2) = meet(X1,join(X2,meet(meet(X1,X2),join(X3,meet(X2,join(X1,meet(X2,X1))))))),
inference(step,[status(thm)],[t202306,t16]) ).
cnf(t202308,plain,
meet(X1,X2) = meet(X1,join(X2,meet(meet(X1,X2),join(X3,meet(X2,join(X1,meet(X1,X2))))))),
inference(step,[status(thm)],[t202307,t24]) ).
cnf(t202309,plain,
meet(X1,X2) = meet(X1,join(X2,meet(meet(X1,X2),join(X3,meet(X2,X1))))),
inference(step,[status(thm)],[t202308,t17]) ).
cnf(t202310,plain,
meet(X1,X2) = meet(X1,join(X2,meet(meet(X1,X2),join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t202309,t24]) ).
cnf(t202311,plain,
meet(X1,X2) = meet(X1,join(X2,meet(meet(X1,X2),join(X2,X3)))),
inference(step,[status(thm)],[t202310,t4576]) ).
cnf(t11619,plain,
meet(X1,join(X2,meet(meet(X1,X2),join(X2,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t202311]) ).
cnf(t11725,plain,
meet(X1,meet(join(X2,meet(meet(X1,X2),join(X2,X3))),X4)) = meet(X1,meet(X4,join(zero,meet(X1,X2)))),
inference(cp,[status(thm)],[t1906,t11619]) ).
cnf(t202460,plain,
meet(X1,meet(X4,join(X2,meet(meet(X1,X2),join(X2,X3))))) = meet(X1,meet(X4,join(zero,meet(X1,X2)))),
inference(step,[status(thm)],[t11725,t24]) ).
cnf(t202461,plain,
meet(X1,meet(X4,join(X2,meet(meet(X1,X2),join(X2,X3))))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t202460,t1906]) ).
cnf(t15181,plain,
meet(X1,meet(X2,join(X3,meet(meet(X1,X3),join(X3,X4))))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t202461]) ).
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(t10,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t201517,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t10,t68]) ).
cnf(t73,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t201517]) ).
cnf(t76,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t73,t16]) ).
cnf(t201521,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t76,t73]) ).
cnf(t201522,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t201521,t68]) ).
cnf(t131,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t201522]) ).
cnf(t4737,plain,
meet(X1,join(join(X1,X2),meet(X1,X3))) = meet(X1,join(join(X1,X2),meet(meet(X1,X3),join(X1,X2)))),
inference(cp,[status(thm)],[t4715,t131]) ).
cnf(t203056,plain,
meet(X1,join(meet(X1,X3),join(X1,X2))) = meet(X1,join(join(X1,X2),meet(meet(X1,X3),join(X1,X2)))),
inference(step,[status(thm)],[t4737,t68]) ).
cnf(t203057,plain,
meet(X1,join(X2,join(meet(X1,X3),X1))) = meet(X1,join(join(X1,X2),meet(meet(X1,X3),join(X1,X2)))),
inference(step,[status(thm)],[t203056,t73]) ).
cnf(t203058,plain,
meet(X1,join(X1,join(X2,meet(X1,X3)))) = meet(X1,join(join(X1,X2),meet(meet(X1,X3),join(X1,X2)))),
inference(step,[status(thm)],[t203057,t73]) ).
cnf(t77,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t73,t17]) ).
cnf(t201535,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t77,t73]) ).
cnf(t201536,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t201535,t68]) ).
cnf(t201537,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t201536,t68]) ).
cnf(t188,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t201537]) ).
cnf(t203059,plain,
meet(X1,join(X1,X2)) = meet(X1,join(join(X1,X2),meet(meet(X1,X3),join(X1,X2)))),
inference(step,[status(thm)],[t203058,t188]) ).
cnf(t203060,plain,
X1 = meet(X1,join(join(X1,X2),meet(meet(X1,X3),join(X1,X2)))),
inference(step,[status(thm)],[t203059,t15]) ).
cnf(t33809,plain,
meet(X1,join(join(X1,X2),meet(meet(X1,X3),join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t203060]) ).
cnf(t33847,plain,
X1 = meet(X1,join(join(X1,X2),meet(meet(X3,meet(X4,X1)),join(X1,X2)))),
inference(cp,[status(thm)],[t33809,t27]) ).
cnf(t203067,plain,
X1 = meet(X1,join(join(X1,X2),meet(join(X1,X2),meet(X3,meet(X4,X1))))),
inference(step,[status(thm)],[t33847,t24]) ).
cnf(t203068,plain,
X1 = meet(X1,join(join(X1,X2),meet(meet(X4,X1),meet(join(X1,X2),X3)))),
inference(step,[status(thm)],[t203067,t27]) ).
cnf(t203069,plain,
X1 = meet(X1,join(join(X1,X2),meet(X3,meet(meet(X4,X1),join(X1,X2))))),
inference(step,[status(thm)],[t203068,t27]) ).
cnf(t203070,plain,
X1 = meet(X1,join(join(X1,X2),meet(X3,meet(meet(X1,X4),join(X1,X2))))),
inference(step,[status(thm)],[t203069,t24]) ).
cnf(t34173,plain,
meet(X1,join(join(X1,X2),meet(X3,meet(meet(X1,X4),join(X1,X2))))) = X1,
inference(orient,[status(thm)],[t203070]) ).
cnf(t34214,plain,
X1 = meet(X1,join(join(X1,X2),meet(X3,meet(meet(X1,X4),join(X1,join(X1,X2)))))),
inference(cp,[status(thm)],[t34173,t131]) ).
cnf(t203079,plain,
X1 = meet(X1,join(join(X1,X2),meet(X1,meet(X3,X4)))),
inference(step,[status(thm)],[t34214,t7867]) ).
cnf(t34658,plain,
meet(X1,join(join(X1,X2),meet(X1,meet(X3,X4)))) = X1,
inference(orient,[status(thm)],[t203079]) ).
cnf(t34670,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(meet(X1,X2),X3),meet(X1,X2))),
inference(cp,[status(thm)],[t34658,t14]) ).
cnf(t203138,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,X2),join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t34670,t68]) ).
cnf(t203139,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t203138,t131]) ).
cnf(t203140,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t203139,t68]) ).
cnf(t38397,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t203140]) ).
cnf(t38480,plain,
meet(X1,meet(X2,meet(meet(X1,X2),join(X2,X3)))) = meet(X1,meet(meet(X1,X2),join(X2,X3))),
inference(cp,[status(thm)],[t15181,t38397]) ).
cnf(t203141,plain,
meet(X1,meet(X2,meet(X1,X2))) = meet(X1,meet(meet(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t38480,t175]) ).
cnf(t203142,plain,
meet(X1,meet(X1,meet(X2,X2))) = meet(X1,meet(meet(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t203141,t27]) ).
cnf(t203143,plain,
meet(X1,meet(X2,X2)) = meet(X1,meet(meet(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t203142,t116]) ).
cnf(t203144,plain,
meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t203143,t14]) ).
cnf(t38548,plain,
meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t203144]) ).
cnf(t38632,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4))),
inference(cp,[status(thm)],[t38548,t38397]) ).
cnf(t203228,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4))),
inference(step,[status(thm)],[t38632,t38397]) ).
cnf(t203229,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4)),
inference(step,[status(thm)],[t203228,t116]) ).
cnf(t203230,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t203229,t68]) ).
cnf(t203231,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),X4))),
inference(step,[status(thm)],[t203230,t73]) ).
cnf(t203232,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t203231,t68]) ).
cnf(t40213,plain,
meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t203232]) ).
cnf(t8188,plain,
meet(X1,join(X2,meet(X1,meet(X2,X3)))) = meet(X1,join(join(X2,meet(X1,meet(X2,X3))),meet(X1,X2))),
inference(cp,[status(thm)],[t8168,t8046]) ).
cnf(t202285,plain,
meet(X1,X2) = meet(X1,join(join(X2,meet(X1,meet(X2,X3))),meet(X1,X2))),
inference(step,[status(thm)],[t8188,t8046]) ).
cnf(t202286,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),join(X2,meet(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t202285,t68]) ).
cnf(t202287,plain,
meet(X1,X2) = meet(X1,join(X2,join(meet(X1,meet(X2,X3)),meet(X1,X2)))),
inference(step,[status(thm)],[t202286,t73]) ).
cnf(t202288,plain,
meet(X1,X2) = meet(X1,join(X2,join(meet(X1,X2),meet(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t202287,t68]) ).
cnf(t10894,plain,
meet(X1,join(X2,join(meet(X1,X2),meet(X1,meet(X2,X3))))) = meet(X1,X2),
inference(orient,[status(thm)],[t202288]) ).
cnf(t199,plain,
meet(X1,join(X2,meet(join(X3,meet(X1,X4)),join(X2,Y4)))) = meet(X1,join(X2,meet(join(X3,meet(X1,X4)),join(Y4,meet(X2,join(X1,X3)))))),
inference(cp,[status(thm)],[t47,t188]) ).
cnf(t203253,plain,
meet(X1,join(X2,meet(join(X2,Y4),join(X3,meet(X1,X4))))) = meet(X1,join(X2,meet(join(X3,meet(X1,X4)),join(Y4,meet(X2,join(X1,X3)))))),
inference(step,[status(thm)],[t199,t24]) ).
cnf(t40903,plain,
meet(X1,join(X2,meet(join(X3,meet(X1,X4)),join(Y4,meet(X2,join(X1,X3)))))) = meet(X1,join(X2,meet(join(X2,Y4),join(X3,meet(X1,X4))))),
inference(orient,[status(thm)],[t203253]) ).
cnf(t34,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)],[t19,t27]) ).
cnf(t201866,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)],[t34,t27]) ).
cnf(t2827,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)],[t201866]) ).
cnf(t2858,plain,
meet(X1,X2) = ifeq(meet(X1,zero),zero,ifeq(join(complement(X2),meet(X1,X2)),one,complement(complement(X2)),meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t2827,t58]) ).
cnf(t201879,plain,
meet(X1,X2) = ifeq(zero,zero,ifeq(join(complement(X2),meet(X1,X2)),one,complement(complement(X2)),meet(X1,X2)),meet(X1,X2)),
inference(step,[status(thm)],[t2858,t126]) ).
cnf(t201880,plain,
meet(X1,X2) = ifeq(join(complement(X2),meet(X1,X2)),one,complement(complement(X2)),meet(X1,X2)),
inference(step,[status(thm)],[t201879,t18]) ).
cnf(t201881,plain,
meet(X1,X2) = ifeq(join(complement(X2),meet(X1,X2)),one,X2,meet(X1,X2)),
inference(step,[status(thm)],[t201880,t784]) ).
cnf(t3087,plain,
ifeq(join(complement(X1),meet(X2,X1)),one,X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t201881]) ).
cnf(t339,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,meet(join(X2,meet(X1,X3)),join(X1,X2))),
inference(cp,[status(thm)],[t337,t188]) ).
cnf(t201602,plain,
join(X1,X2) = join(X1,meet(join(X2,meet(X1,X3)),join(X1,X2))),
inference(step,[status(thm)],[t339,t188]) ).
cnf(t201603,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t201602,t24]) ).
cnf(t381,plain,
join(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = join(X1,X2),
inference(orient,[status(thm)],[t201603]) ).
cnf(t98,plain,
join(X1,join(complement(X1),X2)) = join(X2,one),
inference(cp,[status(thm)],[t73,t95]) ).
cnf(t201530,plain,
join(X1,join(X2,complement(X1))) = join(X2,one),
inference(step,[status(thm)],[t98,t68]) ).
cnf(t134,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t131,t95]) ).
cnf(t201523,plain,
one = join(X1,one),
inference(step,[status(thm)],[t134,t95]) ).
cnf(t142,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t201523]) ).
cnf(t201531,plain,
join(X1,join(X2,complement(X1))) = one,
inference(step,[status(thm)],[t201530,t142]) ).
cnf(t167,plain,
join(X1,join(X2,complement(X1))) = one,
inference(orient,[status(thm)],[t201531]) ).
cnf(t386,plain,
join(X1,join(X2,complement(X1))) = join(X1,meet(one,join(join(X2,complement(X1)),meet(X1,X3)))),
inference(cp,[status(thm)],[t381,t167]) ).
cnf(t201618,plain,
one = join(X1,meet(one,join(join(X2,complement(X1)),meet(X1,X3)))),
inference(step,[status(thm)],[t386,t167]) ).
cnf(t201619,plain,
one = join(X1,meet(one,join(meet(X1,X3),join(X2,complement(X1))))),
inference(step,[status(thm)],[t201618,t68]) ).
cnf(t201620,plain,
one = join(X1,meet(one,join(complement(X1),join(meet(X1,X3),X2)))),
inference(step,[status(thm)],[t201619,t73]) ).
cnf(t201621,plain,
one = join(X1,meet(one,join(X2,join(complement(X1),meet(X1,X3))))),
inference(step,[status(thm)],[t201620,t73]) ).
cnf(t523,plain,
join(X1,meet(one,join(X2,join(complement(X1),meet(X1,X3))))) = one,
inference(orient,[status(thm)],[t201621]) ).
cnf(t61,plain,
meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
inference(cp,[status(thm)],[t27,t58]) ).
cnf(t201528,plain,
meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
inference(step,[status(thm)],[t61,t24]) ).
cnf(t201529,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t201528,t126]) ).
cnf(t160,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t201529]) ).
cnf(t165,plain,
meet(X1,meet(meet(X2,complement(X1)),X3)) = meet(X3,zero),
inference(cp,[status(thm)],[t27,t160]) ).
cnf(t201538,plain,
meet(X1,meet(X3,meet(X2,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t165,t24]) ).
cnf(t201539,plain,
meet(X1,meet(X2,meet(complement(X1),X3))) = meet(X3,zero),
inference(step,[status(thm)],[t201538,t27]) ).
cnf(t201540,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t201539,t24]) ).
cnf(t201541,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(step,[status(thm)],[t201540,t126]) ).
cnf(t202,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t201541]) ).
cnf(t530,plain,
one = join(X1,meet(one,join(X2,join(complement(X1),zero)))),
inference(cp,[status(thm)],[t523,t202]) ).
cnf(t201622,plain,
one = join(X1,meet(one,join(X2,complement(X1)))),
inference(step,[status(thm)],[t530,t100]) ).
cnf(t552,plain,
join(X1,meet(one,join(X2,complement(X1)))) = one,
inference(orient,[status(thm)],[t201622]) ).
cnf(t798,plain,
one = join(complement(X1),meet(one,join(X2,X1))),
inference(cp,[status(thm)],[t552,t784]) ).
cnf(t201662,plain,
one = join(complement(X1),meet(one,join(X1,X2))),
inference(step,[status(thm)],[t798,t68]) ).
cnf(t812,plain,
join(complement(X1),meet(one,join(X1,X2))) = one,
inference(orient,[status(thm)],[t201662]) ).
cnf(t34222,plain,
complement(X1) = meet(complement(X1),join(one,meet(X2,meet(meet(complement(X1),X3),join(complement(X1),meet(one,join(X1,X4))))))),
inference(cp,[status(thm)],[t34173,t812]) ).
cnf(t203093,plain,
complement(X1) = meet(complement(X1),join(one,meet(X2,meet(meet(X3,complement(X1)),join(complement(X1),meet(one,join(X1,X4))))))),
inference(step,[status(thm)],[t34222,t24]) ).
cnf(t203094,plain,
complement(X1) = meet(complement(X1),join(one,meet(X2,meet(meet(X3,complement(X1)),one)))),
inference(step,[status(thm)],[t203093,t812]) ).
cnf(t96,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t15,t95]) ).
cnf(t111,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t96]) ).
cnf(t203095,plain,
complement(X1) = meet(complement(X1),join(one,meet(X2,meet(X3,complement(X1))))),
inference(step,[status(thm)],[t203094,t111]) ).
cnf(t36328,plain,
meet(complement(X1),join(one,meet(X2,meet(X3,complement(X1))))) = complement(X1),
inference(orient,[status(thm)],[t203095]) ).
cnf(t38643,plain,
meet(complement(X1),join(one,meet(X2,meet(X3,complement(X1))))) = meet(complement(X1),meet(complement(X1),join(join(one,meet(X2,meet(X3,complement(X1)))),X4))),
inference(cp,[status(thm)],[t38548,t36328]) ).
cnf(t203391,plain,
complement(X1) = meet(complement(X1),meet(complement(X1),join(join(one,meet(X2,meet(X3,complement(X1)))),X4))),
inference(step,[status(thm)],[t38643,t36328]) ).
cnf(t203392,plain,
complement(X1) = meet(complement(X1),join(join(one,meet(X2,meet(X3,complement(X1)))),X4)),
inference(step,[status(thm)],[t203391,t116]) ).
cnf(t203393,plain,
complement(X1) = meet(complement(X1),join(X4,join(one,meet(X2,meet(X3,complement(X1)))))),
inference(step,[status(thm)],[t203392,t68]) ).
cnf(t45319,plain,
meet(complement(X1),join(X2,join(one,meet(X3,meet(X4,complement(X1)))))) = complement(X1),
inference(orient,[status(thm)],[t203393]) ).
cnf(t144,plain,
one = ifeq(meet(X1,one),zero,ifeq(one,one,complement(X1),one),one),
inference(cp,[status(thm)],[t19,t142]) ).
cnf(t201526,plain,
one = ifeq(X1,zero,ifeq(one,one,complement(X1),one),one),
inference(step,[status(thm)],[t144,t111]) ).
cnf(t201527,plain,
one = ifeq(X1,zero,complement(X1),one),
inference(step,[status(thm)],[t201526,t18]) ).
cnf(t152,plain,
ifeq(X1,zero,complement(X1),one) = one,
inference(orient,[status(thm)],[t201527]) ).
cnf(t153,plain,
one = complement(zero),
inference(cp,[status(thm)],[t152,t18]) ).
cnf(t155,plain,
complement(zero) = one,
inference(orient,[status(thm)],[t153]) ).
cnf(t45321,plain,
complement(zero) = meet(one,join(X1,join(one,meet(X2,meet(X3,complement(zero)))))),
inference(cp,[status(thm)],[t45319,t155]) ).
cnf(t203394,plain,
one = meet(one,join(X1,join(one,meet(X2,meet(X3,complement(zero)))))),
inference(step,[status(thm)],[t45321,t155]) ).
cnf(t203395,plain,
one = meet(one,join(X1,join(one,meet(X2,meet(X3,one))))),
inference(step,[status(thm)],[t203394,t155]) ).
cnf(t203396,plain,
one = meet(one,join(X1,join(one,meet(X2,X3)))),
inference(step,[status(thm)],[t203395,t111]) ).
cnf(t45401,plain,
meet(one,join(X1,join(one,meet(X2,X3)))) = one,
inference(orient,[status(thm)],[t203396]) ).
cnf(t45427,plain,
meet(one,join(X1,join(one,meet(X2,X3)))) = ifeq(join(complement(join(X1,join(one,meet(X2,X3)))),one),one,join(X1,join(one,meet(X2,X3))),meet(one,join(X1,join(one,meet(X2,X3))))),
inference(cp,[status(thm)],[t3087,t45401]) ).
cnf(t203397,plain,
one = ifeq(join(complement(join(X1,join(one,meet(X2,X3)))),one),one,join(X1,join(one,meet(X2,X3))),meet(one,join(X1,join(one,meet(X2,X3))))),
inference(step,[status(thm)],[t45427,t45401]) ).
cnf(t203398,plain,
one = ifeq(one,one,join(X1,join(one,meet(X2,X3))),meet(one,join(X1,join(one,meet(X2,X3))))),
inference(step,[status(thm)],[t203397,t142]) ).
cnf(t203399,plain,
one = join(X1,join(one,meet(X2,X3))),
inference(step,[status(thm)],[t203398,t18]) ).
cnf(t45489,plain,
join(X1,join(one,meet(X2,X3))) = one,
inference(orient,[status(thm)],[t203399]) ).
cnf(t45490,plain,
one = join(one,meet(X1,X2)),
inference(cp,[status(thm)],[t45489,t131]) ).
cnf(t45551,plain,
join(one,meet(X1,X2)) = one,
inference(orient,[status(thm)],[t45490]) ).
cnf(t45592,plain,
meet(X1,join(X2,meet(join(X2,X3),join(one,meet(X1,X4))))) = meet(X1,join(X2,meet(one,join(X3,meet(X2,join(X1,one)))))),
inference(cp,[status(thm)],[t40903,t45551]) ).
cnf(t203408,plain,
meet(X1,join(X2,meet(join(X2,X3),one))) = meet(X1,join(X2,meet(one,join(X3,meet(X2,join(X1,one)))))),
inference(step,[status(thm)],[t45592,t45551]) ).
cnf(t203409,plain,
meet(X1,join(X2,join(X2,X3))) = meet(X1,join(X2,meet(one,join(X3,meet(X2,join(X1,one)))))),
inference(step,[status(thm)],[t203408,t111]) ).
cnf(t203410,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(one,join(X3,meet(X2,join(X1,one)))))),
inference(step,[status(thm)],[t203409,t131]) ).
cnf(t203411,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(one,join(X2,X3)))),
inference(step,[status(thm)],[t203410,t47]) ).
cnf(t390,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,meet(join(X1,X2),join(meet(X2,join(X1,X2)),meet(X1,X3)))),
inference(cp,[status(thm)],[t381,t337]) ).
cnf(t201970,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(meet(X2,join(X1,X2)),meet(X1,X3)))),
inference(step,[status(thm)],[t390,t337]) ).
cnf(t201971,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(meet(X1,X3),meet(X2,join(X1,X2))))),
inference(step,[status(thm)],[t201970,t68]) ).
cnf(t4173,plain,
join(X1,meet(join(X1,X2),join(meet(X1,X3),meet(X2,join(X1,X2))))) = join(X1,X2),
inference(orient,[status(thm)],[t201971]) ).
cnf(t4225,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(zero,meet(X2,join(X1,X2))))),
inference(cp,[status(thm)],[t4173,t202]) ).
cnf(t4324,plain,
join(X1,meet(join(X1,X2),join(zero,meet(X2,join(X1,X2))))) = join(X1,X2),
inference(orient,[status(thm)],[t4225]) ).
cnf(t561,plain,
join(X1,join(meet(one,join(X2,complement(X1))),X3)) = join(X3,one),
inference(cp,[status(thm)],[t73,t552]) ).
cnf(t201624,plain,
join(X1,join(X3,meet(one,join(X2,complement(X1))))) = join(X3,one),
inference(step,[status(thm)],[t561,t68]) ).
cnf(t201625,plain,
join(X1,join(X3,meet(one,join(X2,complement(X1))))) = one,
inference(step,[status(thm)],[t201624,t142]) ).
cnf(t574,plain,
join(X1,join(X2,meet(one,join(X3,complement(X1))))) = one,
inference(orient,[status(thm)],[t201625]) ).
cnf(t4330,plain,
join(X1,join(X2,meet(one,join(X3,complement(X1))))) = join(X1,meet(one,join(zero,meet(join(X2,meet(one,join(X3,complement(X1)))),join(X1,join(X2,meet(one,join(X3,complement(X1))))))))),
inference(cp,[status(thm)],[t4324,t574]) ).
cnf(t201972,plain,
one = join(X1,meet(one,join(zero,meet(join(X2,meet(one,join(X3,complement(X1)))),join(X1,join(X2,meet(one,join(X3,complement(X1))))))))),
inference(step,[status(thm)],[t4330,t574]) ).
cnf(t201973,plain,
one = join(X1,meet(one,join(zero,meet(join(X2,meet(one,join(X3,complement(X1)))),one)))),
inference(step,[status(thm)],[t201972,t574]) ).
cnf(t201974,plain,
one = join(X1,meet(one,join(zero,join(X2,meet(one,join(X3,complement(X1))))))),
inference(step,[status(thm)],[t201973,t111]) ).
cnf(t201975,plain,
one = join(X1,meet(one,join(X2,join(meet(one,join(X3,complement(X1))),zero)))),
inference(step,[status(thm)],[t201974,t73]) ).
cnf(t201976,plain,
one = join(X1,meet(one,join(X2,meet(one,join(X3,complement(X1)))))),
inference(step,[status(thm)],[t201975,t100]) ).
cnf(t4421,plain,
join(X1,meet(one,join(X2,meet(one,join(X3,complement(X1)))))) = one,
inference(orient,[status(thm)],[t201976]) ).
cnf(t4424,plain,
one = join(complement(X1),meet(one,join(X2,meet(one,join(X3,X1))))),
inference(cp,[status(thm)],[t4421,t784]) ).
cnf(t201977,plain,
one = join(complement(X1),meet(one,join(X2,meet(one,join(X1,X3))))),
inference(step,[status(thm)],[t4424,t68]) ).
cnf(t4450,plain,
join(complement(X1),meet(one,join(X2,meet(one,join(X1,X3))))) = one,
inference(orient,[status(thm)],[t201977]) ).
cnf(t389,plain,
join(X1,complement(X1)) = join(X1,meet(one,join(complement(X1),meet(X1,X2)))),
inference(cp,[status(thm)],[t381,t95]) ).
cnf(t201608,plain,
one = join(X1,meet(one,join(complement(X1),meet(X1,X2)))),
inference(step,[status(thm)],[t389,t95]) ).
cnf(t447,plain,
join(X1,meet(one,join(complement(X1),meet(X1,X2)))) = one,
inference(orient,[status(thm)],[t201608]) ).
cnf(t450,plain,
one = join(X1,meet(one,join(complement(X1),zero))),
inference(cp,[status(thm)],[t447,t202]) ).
cnf(t201609,plain,
one = join(X1,meet(one,complement(X1))),
inference(step,[status(thm)],[t450,t100]) ).
cnf(t472,plain,
join(X1,meet(one,complement(X1))) = one,
inference(orient,[status(thm)],[t201609]) ).
cnf(t473,plain,
meet(one,complement(X1)) = ifeq(meet(X1,meet(one,complement(X1))),zero,ifeq(one,one,complement(X1),meet(one,complement(X1))),meet(one,complement(X1))),
inference(cp,[status(thm)],[t19,t472]) ).
cnf(t201611,plain,
meet(one,complement(X1)) = ifeq(zero,zero,ifeq(one,one,complement(X1),meet(one,complement(X1))),meet(one,complement(X1))),
inference(step,[status(thm)],[t473,t160]) ).
cnf(t201612,plain,
meet(one,complement(X1)) = ifeq(one,one,complement(X1),meet(one,complement(X1))),
inference(step,[status(thm)],[t201611,t18]) ).
cnf(t201613,plain,
meet(one,complement(X1)) = complement(X1),
inference(step,[status(thm)],[t201612,t18]) ).
cnf(t495,plain,
meet(one,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t201613]) ).
cnf(t1691,plain,
meet(one,complement(X1)) = meet(one,join(zero,complement(X1))),
inference(cp,[status(thm)],[t1678,t495]) ).
cnf(t201767,plain,
complement(X1) = meet(one,join(zero,complement(X1))),
inference(step,[status(thm)],[t1691,t495]) ).
cnf(t1793,plain,
meet(one,join(zero,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t201767]) ).
cnf(t1798,plain,
meet(zero,one) = meet(zero,complement(X1)),
inference(cp,[status(thm)],[t175,t1793]) ).
cnf(t201768,plain,
zero = meet(zero,complement(X1)),
inference(step,[status(thm)],[t1798,t111]) ).
cnf(t1812,plain,
meet(zero,complement(X1)) = zero,
inference(orient,[status(thm)],[t201768]) ).
cnf(t1817,plain,
meet(zero,join(complement(X1),meet(zero,join(complement(X1),X2)))) = meet(zero,join(complement(X1),meet(zero,join(X2,zero)))),
inference(cp,[status(thm)],[t1384,t1812]) ).
cnf(t201834,plain,
meet(zero,join(complement(X1),meet(zero,join(X2,complement(X1))))) = meet(zero,join(complement(X1),meet(zero,join(X2,zero)))),
inference(step,[status(thm)],[t1817,t68]) ).
cnf(t201835,plain,
meet(zero,join(complement(X1),meet(zero,join(X2,complement(X1))))) = meet(zero,join(complement(X1),meet(zero,X2))),
inference(step,[status(thm)],[t201834,t100]) ).
cnf(t201836,plain,
meet(zero,join(complement(X1),meet(zero,join(X2,complement(X1))))) = meet(zero,join(complement(X1),meet(X2,zero))),
inference(step,[status(thm)],[t201835,t24]) ).
cnf(t201837,plain,
meet(zero,join(complement(X1),meet(zero,join(X2,complement(X1))))) = meet(zero,join(complement(X1),zero)),
inference(step,[status(thm)],[t201836,t126]) ).
cnf(t201838,plain,
meet(zero,join(complement(X1),meet(zero,join(X2,complement(X1))))) = meet(zero,complement(X1)),
inference(step,[status(thm)],[t201837,t100]) ).
cnf(t201839,plain,
meet(zero,join(complement(X1),meet(zero,join(X2,complement(X1))))) = zero,
inference(step,[status(thm)],[t201838,t1812]) ).
cnf(t2584,plain,
meet(zero,join(complement(X1),meet(zero,join(X2,complement(X1))))) = zero,
inference(orient,[status(thm)],[t201839]) ).
cnf(t2586,plain,
zero = meet(zero,join(X1,meet(zero,join(X2,complement(complement(X1)))))),
inference(cp,[status(thm)],[t2584,t784]) ).
cnf(t201840,plain,
zero = meet(zero,join(X1,meet(zero,join(X2,X1)))),
inference(step,[status(thm)],[t2586,t784]) ).
cnf(t201841,plain,
zero = meet(zero,join(X1,meet(zero,join(X1,X2)))),
inference(step,[status(thm)],[t201840,t68]) ).
cnf(t2604,plain,
meet(zero,join(X1,meet(zero,join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t201841]) ).
cnf(t2646,plain,
meet(zero,join(join(X1,X2),meet(zero,join(join(X1,X2),X1)))) = meet(zero,join(join(X1,X2),zero)),
inference(cp,[status(thm)],[t1384,t2604]) ).
cnf(t201842,plain,
zero = meet(zero,join(join(X1,X2),zero)),
inference(step,[status(thm)],[t2646,t2604]) ).
cnf(t201843,plain,
zero = meet(zero,join(X1,X2)),
inference(step,[status(thm)],[t201842,t100]) ).
cnf(t2652,plain,
meet(zero,join(X1,X2)) = zero,
inference(orient,[status(thm)],[t201843]) ).
cnf(t10298,plain,
meet(X1,join(X2,meet(zero,meet(join(X2,X3),join(X4,meet(X1,join(X2,zero))))))) = meet(X1,join(X2,meet(zero,join(X3,meet(X2,join(X1,meet(zero,join(X1,X4)))))))),
inference(cp,[status(thm)],[t10286,t2652]) ).
cnf(t202704,plain,
meet(X1,join(X2,meet(zero,meet(join(X2,X3),join(X4,meet(X1,X2)))))) = meet(X1,join(X2,meet(zero,join(X3,meet(X2,join(X1,meet(zero,join(X1,X4)))))))),
inference(step,[status(thm)],[t10298,t100]) ).
cnf(t202705,plain,
meet(X1,join(X2,meet(zero,meet(join(X2,X3),join(X4,meet(X1,X2)))))) = meet(X1,join(X2,zero)),
inference(step,[status(thm)],[t202704,t2652]) ).
cnf(t202706,plain,
meet(X1,join(X2,meet(zero,meet(join(X2,X3),join(X4,meet(X1,X2)))))) = meet(X1,X2),
inference(step,[status(thm)],[t202705,t100]) ).
cnf(t21898,plain,
meet(X1,join(X2,meet(zero,meet(join(X2,X3),join(X4,meet(X1,X2)))))) = meet(X1,X2),
inference(orient,[status(thm)],[t202706]) ).
cnf(t8789,plain,
meet(X1,meet(X2,complement(X1))) = meet(X1,join(zero,meet(meet(X2,complement(X1)),join(X1,X3)))),
inference(cp,[status(thm)],[t8764,t160]) ).
cnf(t202222,plain,
zero = meet(X1,join(zero,meet(meet(X2,complement(X1)),join(X1,X3)))),
inference(step,[status(thm)],[t8789,t160]) ).
cnf(t202223,plain,
zero = meet(X1,join(zero,meet(join(X1,X3),meet(X2,complement(X1))))),
inference(step,[status(thm)],[t202222,t24]) ).
cnf(t202224,plain,
zero = meet(X1,join(zero,meet(complement(X1),meet(join(X1,X3),X2)))),
inference(step,[status(thm)],[t202223,t27]) ).
cnf(t202225,plain,
zero = meet(X1,join(zero,meet(X2,meet(complement(X1),join(X1,X3))))),
inference(step,[status(thm)],[t202224,t27]) ).
cnf(t9362,plain,
meet(X1,join(zero,meet(X2,meet(complement(X1),join(X1,X3))))) = zero,
inference(orient,[status(thm)],[t202225]) ).
cnf(t2765,plain,
meet(complement(X1),join(X1,meet(meet(one,join(X2,complement(X1))),complement(X1)))) = meet(complement(X1),join(X1,meet(complement(X1),one))),
inference(cp,[status(thm)],[t2746,t552]) ).
cnf(t201917,plain,
meet(complement(X1),join(X1,meet(complement(X1),meet(one,join(X2,complement(X1)))))) = meet(complement(X1),join(X1,meet(complement(X1),one))),
inference(step,[status(thm)],[t2765,t24]) ).
cnf(t201918,plain,
meet(complement(X1),join(X1,meet(one,meet(join(X2,complement(X1)),complement(X1))))) = meet(complement(X1),join(X1,meet(complement(X1),one))),
inference(step,[status(thm)],[t201917,t27]) ).
cnf(t201919,plain,
meet(complement(X1),join(X1,meet(one,meet(complement(X1),join(X2,complement(X1)))))) = meet(complement(X1),join(X1,meet(complement(X1),one))),
inference(step,[status(thm)],[t201918,t24]) ).
cnf(t201920,plain,
meet(complement(X1),join(X1,meet(one,meet(complement(X1),join(X2,complement(X1)))))) = meet(complement(X1),join(X1,complement(X1))),
inference(step,[status(thm)],[t201919,t111]) ).
cnf(t201921,plain,
meet(complement(X1),join(X1,meet(one,meet(complement(X1),join(X2,complement(X1)))))) = meet(complement(X1),one),
inference(step,[status(thm)],[t201920,t95]) ).
cnf(t201922,plain,
meet(complement(X1),join(X1,meet(one,meet(complement(X1),join(X2,complement(X1)))))) = complement(X1),
inference(step,[status(thm)],[t201921,t111]) ).
cnf(t3350,plain,
meet(complement(X1),join(X1,meet(one,meet(complement(X1),join(X2,complement(X1)))))) = complement(X1),
inference(orient,[status(thm)],[t201922]) ).
cnf(t9367,plain,
zero = meet(X1,join(zero,meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t9362,t3350]) ).
cnf(t9482,plain,
meet(X1,join(zero,meet(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t9367]) ).
cnf(t9488,plain,
meet(X1,join(zero,meet(X2,complement(X1)))) = meet(X1,join(zero,meet(join(zero,meet(X2,complement(X1))),join(X1,X3)))),
inference(cp,[status(thm)],[t8764,t9482]) ).
cnf(t202385,plain,
zero = meet(X1,join(zero,meet(join(zero,meet(X2,complement(X1))),join(X1,X3)))),
inference(step,[status(thm)],[t9488,t9482]) ).
cnf(t202386,plain,
zero = meet(X1,join(zero,meet(join(X1,X3),join(zero,meet(X2,complement(X1)))))),
inference(step,[status(thm)],[t202385,t24]) ).
cnf(t13233,plain,
meet(X1,join(zero,meet(join(X1,X2),join(zero,meet(X3,complement(X1)))))) = zero,
inference(orient,[status(thm)],[t202386]) ).
cnf(t13278,plain,
zero = meet(complement(X1),join(zero,meet(one,join(zero,meet(X2,complement(complement(X1))))))),
inference(cp,[status(thm)],[t13233,t812]) ).
cnf(t202387,plain,
zero = meet(complement(X1),join(zero,meet(one,join(zero,meet(X2,X1))))),
inference(step,[status(thm)],[t13278,t784]) ).
cnf(t202388,plain,
zero = meet(complement(X1),join(zero,meet(one,join(zero,meet(X1,X2))))),
inference(step,[status(thm)],[t202387,t24]) ).
cnf(t13407,plain,
meet(complement(X1),join(zero,meet(one,join(zero,meet(X1,X2))))) = zero,
inference(orient,[status(thm)],[t202388]) ).
cnf(t9422,plain,
zero = meet(complement(X1),join(zero,meet(X2,meet(complement(complement(X1)),one)))),
inference(cp,[status(thm)],[t9362,t812]) ).
cnf(t202226,plain,
zero = meet(complement(X1),join(zero,meet(X2,complement(complement(X1))))),
inference(step,[status(thm)],[t9422,t111]) ).
cnf(t202227,plain,
zero = meet(complement(X1),join(zero,meet(X2,X1))),
inference(step,[status(thm)],[t202226,t784]) ).
cnf(t202228,plain,
zero = meet(complement(X1),join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t202227,t24]) ).
cnf(t9520,plain,
meet(complement(X1),join(zero,meet(X1,X2))) = zero,
inference(orient,[status(thm)],[t202228]) ).
cnf(f12,hypothesis,
meet(b,a) = a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity_hypothesis) ).
fof(f12_nnf,plain,
meet(b,a) = a,
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
meet(b,a) = a,
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(t2,plain,
meet(b,a) = a,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t63,plain,
meet(b,a) = a,
inference(orient,[status(thm)],[t2]) ).
cnf(t1694,plain,
meet(b,a) = meet(b,join(zero,a)),
inference(cp,[status(thm)],[t1678,t63]) ).
cnf(t201761,plain,
a = meet(b,join(zero,a)),
inference(step,[status(thm)],[t1694,t63]) ).
cnf(t1737,plain,
meet(b,join(zero,a)) = a,
inference(orient,[status(thm)],[t201761]) ).
cnf(t8802,plain,
meet(b,join(zero,a)) = meet(b,join(a,meet(join(zero,a),join(b,X1)))),
inference(cp,[status(thm)],[t8764,t1737]) ).
cnf(t202209,plain,
a = meet(b,join(a,meet(join(zero,a),join(b,X1)))),
inference(step,[status(thm)],[t8802,t1737]) ).
cnf(t202210,plain,
a = meet(b,join(a,meet(join(zero,a),join(X1,b)))),
inference(step,[status(thm)],[t202209,t68]) ).
cnf(t202211,plain,
a = meet(b,join(a,meet(join(X1,b),join(zero,a)))),
inference(step,[status(thm)],[t202210,t24]) ).
cnf(t9063,plain,
meet(b,join(a,meet(join(X1,b),join(zero,a)))) = a,
inference(orient,[status(thm)],[t202211]) ).
cnf(t9534,plain,
zero = meet(complement(b),join(zero,a)),
inference(cp,[status(thm)],[t9520,t9063]) ).
cnf(t9594,plain,
meet(complement(b),join(zero,a)) = zero,
inference(orient,[status(thm)],[t9534]) ).
cnf(t171,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)],[t19,t167]) ).
cnf(t201941,plain,
join(X1,complement(X2)) = ifeq(meet(X2,join(X1,complement(X2))),zero,complement(X2),join(X1,complement(X2))),
inference(step,[status(thm)],[t171,t18]) ).
cnf(t3633,plain,
ifeq(meet(X1,join(X2,complement(X1))),zero,complement(X1),join(X2,complement(X1))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t201941]) ).
cnf(t3635,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)],[t3633,t784]) ).
cnf(t201942,plain,
join(X1,X2) = ifeq(meet(complement(X2),join(X1,X2)),zero,complement(complement(X2)),join(X1,complement(complement(X2)))),
inference(step,[status(thm)],[t3635,t784]) ).
cnf(t201943,plain,
join(X1,X2) = ifeq(meet(complement(X2),join(X1,X2)),zero,X2,join(X1,complement(complement(X2)))),
inference(step,[status(thm)],[t201942,t784]) ).
cnf(t201944,plain,
join(X1,X2) = ifeq(meet(complement(X2),join(X1,X2)),zero,X2,join(X1,X2)),
inference(step,[status(thm)],[t201943,t784]) ).
cnf(t3642,plain,
ifeq(meet(complement(X1),join(X2,X1)),zero,X1,join(X2,X1)) = join(X2,X1),
inference(orient,[status(thm)],[t201944]) ).
cnf(t11679,plain,
meet(b,join(zero,a)) = meet(b,join(join(zero,a),meet(a,join(join(zero,a),X1)))),
inference(cp,[status(thm)],[t11619,t1737]) ).
cnf(t202312,plain,
a = meet(b,join(join(zero,a),meet(a,join(join(zero,a),X1)))),
inference(step,[status(thm)],[t11679,t1737]) ).
cnf(t202313,plain,
a = meet(b,join(join(zero,a),meet(a,join(X1,join(zero,a))))),
inference(step,[status(thm)],[t202312,t68]) ).
cnf(t11815,plain,
meet(b,join(join(zero,a),meet(a,join(X1,join(zero,a))))) = a,
inference(orient,[status(thm)],[t202313]) ).
cnf(t11833,plain,
meet(join(zero,a),b) = meet(join(zero,a),a),
inference(cp,[status(thm)],[t175,t11815]) ).
cnf(t202314,plain,
meet(b,join(zero,a)) = meet(join(zero,a),a),
inference(step,[status(thm)],[t11833,t24]) ).
cnf(t202315,plain,
a = meet(join(zero,a),a),
inference(step,[status(thm)],[t202314,t1737]) ).
cnf(t202316,plain,
a = meet(a,join(zero,a)),
inference(step,[status(thm)],[t202315,t24]) ).
cnf(t11899,plain,
meet(a,join(zero,a)) = a,
inference(orient,[status(thm)],[t202316]) ).
cnf(t11901,plain,
zero = meet(complement(a),join(zero,a)),
inference(cp,[status(thm)],[t9520,t11899]) ).
cnf(t12042,plain,
meet(complement(a),join(zero,a)) = zero,
inference(orient,[status(thm)],[t11901]) ).
cnf(t12044,plain,
join(zero,a) = ifeq(zero,zero,a,join(zero,a)),
inference(cp,[status(thm)],[t3642,t12042]) ).
cnf(t202317,plain,
join(zero,a) = a,
inference(step,[status(thm)],[t12044,t18]) ).
cnf(t12091,plain,
join(zero,a) = a,
inference(orient,[status(thm)],[t202317]) ).
cnf(t202319,plain,
meet(complement(b),a) = zero,
inference(step,[status(thm)],[t9594,t12091]) ).
cnf(t12117,plain,
meet(complement(b),a) = zero,
inference(rw,[status(thm)],[t202319]) ).
cnf(t202326,plain,
meet(a,complement(b)) = zero,
inference(step,[status(thm)],[t12117,t24]) ).
cnf(t12123,plain,
meet(a,complement(b)) = zero,
inference(orient,[status(thm)],[t202326]) ).
cnf(t12144,plain,
meet(a,join(complement(b),meet(a,join(complement(b),X1)))) = meet(a,join(complement(b),meet(a,join(X1,zero)))),
inference(cp,[status(thm)],[t1299,t12123]) ).
cnf(t202405,plain,
meet(a,join(complement(b),meet(a,join(X1,complement(b))))) = meet(a,join(complement(b),meet(a,join(X1,zero)))),
inference(step,[status(thm)],[t12144,t68]) ).
cnf(t202406,plain,
meet(a,join(complement(b),meet(a,join(X1,complement(b))))) = meet(a,join(complement(b),meet(a,X1))),
inference(step,[status(thm)],[t202405,t100]) ).
cnf(t202407,plain,
meet(a,join(complement(b),meet(a,join(X1,complement(b))))) = meet(a,join(complement(b),meet(X1,a))),
inference(step,[status(thm)],[t202406,t24]) ).
cnf(t14021,plain,
meet(a,join(complement(b),meet(a,join(X1,complement(b))))) = meet(a,join(complement(b),meet(X1,a))),
inference(orient,[status(thm)],[t202407]) ).
cnf(t496,plain,
one = join(one,complement(X1)),
inference(cp,[status(thm)],[t17,t495]) ).
cnf(t503,plain,
join(one,complement(X1)) = one,
inference(orient,[status(thm)],[t496]) ).
cnf(t14022,plain,
meet(a,join(complement(b),meet(one,a))) = meet(a,join(complement(b),meet(a,one))),
inference(cp,[status(thm)],[t14021,t503]) ).
cnf(t202408,plain,
meet(a,join(complement(b),meet(one,a))) = meet(a,join(complement(b),a)),
inference(step,[status(thm)],[t14022,t111]) ).
cnf(t202409,plain,
meet(a,join(complement(b),meet(one,a))) = meet(a,join(a,complement(b))),
inference(step,[status(thm)],[t202408,t68]) ).
cnf(t202410,plain,
meet(a,join(complement(b),meet(one,a))) = a,
inference(step,[status(thm)],[t202409,t15]) ).
cnf(t14061,plain,
meet(a,join(complement(b),meet(one,a))) = a,
inference(orient,[status(thm)],[t202410]) ).
cnf(t14084,plain,
zero = meet(complement(a),join(zero,meet(one,join(zero,a)))),
inference(cp,[status(thm)],[t13407,t14061]) ).
cnf(t202411,plain,
zero = meet(complement(a),join(zero,meet(one,a))),
inference(step,[status(thm)],[t14084,t12091]) ).
cnf(t14125,plain,
meet(complement(a),join(zero,meet(one,a))) = zero,
inference(orient,[status(thm)],[t202411]) ).
cnf(t14135,plain,
one = join(complement(a),meet(one,join(complement(complement(a)),zero))),
inference(cp,[status(thm)],[t447,t14125]) ).
cnf(t202412,plain,
one = join(complement(a),meet(one,complement(complement(a)))),
inference(step,[status(thm)],[t14135,t100]) ).
cnf(t202413,plain,
one = join(complement(a),meet(one,a)),
inference(step,[status(thm)],[t202412,t784]) ).
cnf(t14176,plain,
join(complement(a),meet(one,a)) = one,
inference(orient,[status(thm)],[t202413]) ).
cnf(t14178,plain,
meet(one,a) = ifeq(one,one,a,meet(one,a)),
inference(cp,[status(thm)],[t3087,t14176]) ).
cnf(t202414,plain,
meet(one,a) = a,
inference(step,[status(thm)],[t14178,t18]) ).
cnf(t14213,plain,
meet(one,a) = a,
inference(orient,[status(thm)],[t202414]) ).
cnf(t22099,plain,
meet(one,a) = meet(one,join(a,meet(zero,meet(join(a,X1),join(X2,a))))),
inference(cp,[status(thm)],[t21898,t14213]) ).
cnf(t202710,plain,
a = meet(one,join(a,meet(zero,meet(join(a,X1),join(X2,a))))),
inference(step,[status(thm)],[t22099,t14213]) ).
cnf(t202711,plain,
a = meet(one,join(a,meet(zero,meet(join(X2,a),join(a,X1))))),
inference(step,[status(thm)],[t202710,t24]) ).
cnf(t202712,plain,
a = meet(one,join(a,meet(zero,meet(join(X2,a),join(X1,a))))),
inference(step,[status(thm)],[t202711,t68]) ).
cnf(t202713,plain,
a = meet(one,join(a,meet(zero,meet(join(X1,a),join(X2,a))))),
inference(step,[status(thm)],[t202712,t24]) ).
cnf(t22372,plain,
meet(one,join(a,meet(zero,meet(join(X1,a),join(X2,a))))) = a,
inference(orient,[status(thm)],[t202713]) ).
cnf(t22420,plain,
one = join(complement(a),meet(one,join(X1,a))),
inference(cp,[status(thm)],[t4450,t22372]) ).
cnf(t22463,plain,
join(complement(a),meet(one,join(X1,a))) = one,
inference(orient,[status(thm)],[t22420]) ).
cnf(t22476,plain,
join(complement(a),meet(one,join(X1,a))) = join(complement(a),meet(one,join(meet(one,join(X1,a)),meet(complement(a),X2)))),
inference(cp,[status(thm)],[t381,t22463]) ).
cnf(t202811,plain,
one = join(complement(a),meet(one,join(meet(one,join(X1,a)),meet(complement(a),X2)))),
inference(step,[status(thm)],[t22476,t22463]) ).
cnf(t202812,plain,
one = join(complement(a),meet(one,join(meet(complement(a),X2),meet(one,join(X1,a))))),
inference(step,[status(thm)],[t202811,t68]) ).
cnf(t202813,plain,
one = join(complement(a),meet(one,join(meet(X2,complement(a)),meet(one,join(X1,a))))),
inference(step,[status(thm)],[t202812,t24]) ).
cnf(t25122,plain,
join(complement(a),meet(one,join(meet(X1,complement(a)),meet(one,join(X2,a))))) = one,
inference(orient,[status(thm)],[t202813]) ).
cnf(t40931,plain,
meet(one,join(X1,meet(join(X1,X2),join(complement(a),meet(one,join(meet(X3,complement(a)),meet(one,join(X4,a)))))))) = meet(one,join(X1,meet(one,join(X2,meet(X1,join(one,complement(a))))))),
inference(cp,[status(thm)],[t40903,t25122]) ).
cnf(t203262,plain,
meet(one,join(X1,meet(join(X1,X2),one))) = meet(one,join(X1,meet(one,join(X2,meet(X1,join(one,complement(a))))))),
inference(step,[status(thm)],[t40931,t25122]) ).
cnf(t203263,plain,
meet(one,join(X1,join(X1,X2))) = meet(one,join(X1,meet(one,join(X2,meet(X1,join(one,complement(a))))))),
inference(step,[status(thm)],[t203262,t111]) ).
cnf(t203264,plain,
meet(one,join(X1,X2)) = meet(one,join(X1,meet(one,join(X2,meet(X1,join(one,complement(a))))))),
inference(step,[status(thm)],[t203263,t131]) ).
cnf(t203265,plain,
meet(one,join(X1,X2)) = meet(one,join(X1,meet(one,join(X2,meet(X1,one))))),
inference(step,[status(thm)],[t203264,t503]) ).
cnf(t203266,plain,
meet(one,join(X1,X2)) = meet(one,join(X1,meet(one,join(X2,X1)))),
inference(step,[status(thm)],[t203265,t111]) ).
cnf(t203267,plain,
meet(one,join(X1,X2)) = meet(one,join(X1,meet(one,join(X1,X2)))),
inference(step,[status(thm)],[t203266,t68]) ).
cnf(t41813,plain,
meet(one,join(X1,meet(one,join(X1,X2)))) = meet(one,join(X1,X2)),
inference(orient,[status(thm)],[t203267]) ).
cnf(t41932,plain,
meet(join(X1,meet(one,join(X1,X2))),meet(X3,one)) = meet(X3,meet(one,join(X1,X2))),
inference(cp,[status(thm)],[t27,t41813]) ).
cnf(t203292,plain,
meet(join(X1,meet(one,join(X1,X2))),X3) = meet(X3,meet(one,join(X1,X2))),
inference(step,[status(thm)],[t41932,t111]) ).
cnf(t203293,plain,
meet(X3,join(X1,meet(one,join(X1,X2)))) = meet(X3,meet(one,join(X1,X2))),
inference(step,[status(thm)],[t203292,t24]) ).
cnf(t42933,plain,
meet(X1,join(X2,meet(one,join(X2,X3)))) = meet(X1,meet(one,join(X2,X3))),
inference(orient,[status(thm)],[t203293]) ).
cnf(t203412,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(one,join(X2,X3))),
inference(step,[status(thm)],[t203411,t42933]) ).
cnf(t45621,plain,
meet(X1,meet(one,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t203412]) ).
cnf(t45626,plain,
meet(meet(one,join(X1,X2)),join(X1,X2)) = meet(one,join(X1,X2)),
inference(cp,[status(thm)],[t45621,t14]) ).
cnf(t203417,plain,
meet(join(X1,X2),meet(one,join(X1,X2))) = meet(one,join(X1,X2)),
inference(step,[status(thm)],[t45626,t24]) ).
cnf(t203418,plain,
meet(join(X1,X2),join(X1,X2)) = meet(one,join(X1,X2)),
inference(step,[status(thm)],[t203417,t45621]) ).
cnf(t203419,plain,
join(X1,X2) = meet(one,join(X1,X2)),
inference(step,[status(thm)],[t203418,t14]) ).
cnf(t45738,plain,
meet(one,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t203419]) ).
cnf(t45810,plain,
meet(one,join(X1,X2)) = meet(one,join(join(X1,X2),join(join(X1,X2),meet(one,meet(join(X1,X2),X3))))),
inference(cp,[status(thm)],[t10894,t45738]) ).
cnf(t203461,plain,
join(X1,X2) = meet(one,join(join(X1,X2),join(join(X1,X2),meet(one,meet(join(X1,X2),X3))))),
inference(step,[status(thm)],[t45810,t45738]) ).
cnf(t203462,plain,
join(X1,X2) = join(join(X1,X2),join(join(X1,X2),meet(one,meet(join(X1,X2),X3)))),
inference(step,[status(thm)],[t203461,t45738]) ).
cnf(t203463,plain,
join(X1,X2) = join(join(X1,X2),meet(one,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t203462,t131]) ).
cnf(t203464,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(one,join(X1,X2)))),
inference(step,[status(thm)],[t203463,t27]) ).
cnf(t203465,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t203464,t45621]) ).
cnf(t46458,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t203465]) ).
cnf(t8772,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)],[t8764,t8168]) ).
cnf(t202541,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(X2,meet(X1,X2)),join(X1,X3)))),
inference(step,[status(thm)],[t8772,t8168]) ).
cnf(t202542,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(X1,X3),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t202541,t24]) ).
cnf(t18112,plain,
meet(X1,join(meet(X1,X2),meet(join(X1,X3),join(X2,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t202542]) ).
cnf(t585,plain,
join(X1,join(join(X2,meet(one,join(X3,complement(X1)))),X4)) = join(X4,one),
inference(cp,[status(thm)],[t73,t574]) ).
cnf(t201628,plain,
join(X1,join(X4,join(X2,meet(one,join(X3,complement(X1)))))) = join(X4,one),
inference(step,[status(thm)],[t585,t68]) ).
cnf(t201629,plain,
join(X1,join(X2,join(meet(one,join(X3,complement(X1))),X4))) = join(X4,one),
inference(step,[status(thm)],[t201628,t73]) ).
cnf(t201630,plain,
join(X1,join(X2,join(X4,meet(one,join(X3,complement(X1)))))) = join(X4,one),
inference(step,[status(thm)],[t201629,t68]) ).
cnf(t201631,plain,
join(X1,join(X2,join(X4,meet(one,join(X3,complement(X1)))))) = one,
inference(step,[status(thm)],[t201630,t142]) ).
cnf(t612,plain,
join(X1,join(X2,join(X3,meet(one,join(X4,complement(X1)))))) = one,
inference(orient,[status(thm)],[t201631]) ).
cnf(t4338,plain,
join(X1,join(X2,join(X3,meet(one,join(X4,complement(X1)))))) = join(X1,meet(one,join(zero,meet(join(X2,join(X3,meet(one,join(X4,complement(X1))))),join(X1,join(X2,join(X3,meet(one,join(X4,complement(X1)))))))))),
inference(cp,[status(thm)],[t4324,t612]) ).
cnf(t202083,plain,
one = join(X1,meet(one,join(zero,meet(join(X2,join(X3,meet(one,join(X4,complement(X1))))),join(X1,join(X2,join(X3,meet(one,join(X4,complement(X1)))))))))),
inference(step,[status(thm)],[t4338,t612]) ).
cnf(t202084,plain,
one = join(X1,meet(one,join(zero,meet(join(X2,join(X3,meet(one,join(X4,complement(X1))))),one)))),
inference(step,[status(thm)],[t202083,t612]) ).
cnf(t202085,plain,
one = join(X1,meet(one,join(zero,join(X2,join(X3,meet(one,join(X4,complement(X1)))))))),
inference(step,[status(thm)],[t202084,t111]) ).
cnf(t202086,plain,
one = join(X1,meet(one,join(X2,join(join(X3,meet(one,join(X4,complement(X1)))),zero)))),
inference(step,[status(thm)],[t202085,t73]) ).
cnf(t202087,plain,
one = join(X1,meet(one,join(X2,join(X3,meet(one,join(X4,complement(X1))))))),
inference(step,[status(thm)],[t202086,t100]) ).
cnf(t5956,plain,
join(X1,meet(one,join(X2,join(X3,meet(one,join(X4,complement(X1))))))) = one,
inference(orient,[status(thm)],[t202087]) ).
cnf(t5996,plain,
join(X1,join(meet(one,join(X2,join(X3,meet(one,join(X4,complement(X1)))))),Y4)) = join(Y4,one),
inference(cp,[status(thm)],[t73,t5956]) ).
cnf(t202118,plain,
join(X1,join(Y4,meet(one,join(X2,join(X3,meet(one,join(X4,complement(X1)))))))) = join(Y4,one),
inference(step,[status(thm)],[t5996,t68]) ).
cnf(t202119,plain,
join(X1,join(Y4,meet(one,join(X2,join(X3,meet(one,join(X4,complement(X1)))))))) = one,
inference(step,[status(thm)],[t202118,t142]) ).
cnf(t6401,plain,
join(X1,join(X2,meet(one,join(X3,join(X4,meet(one,join(Y4,complement(X1)))))))) = one,
inference(orient,[status(thm)],[t202119]) ).
cnf(t18255,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(one,join(X2,meet(X1,X2))))),
inference(cp,[status(thm)],[t18112,t6401]) ).
cnf(t18520,plain,
meet(X1,join(meet(X1,X2),meet(one,join(X2,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t18255]) ).
cnf(t13235,plain,
zero = meet(X1,join(zero,meet(one,join(zero,meet(X2,complement(X1)))))),
inference(cp,[status(thm)],[t13233,t6401]) ).
cnf(t13355,plain,
meet(X1,join(zero,meet(one,join(zero,meet(X2,complement(X1)))))) = zero,
inference(orient,[status(thm)],[t13235]) ).
cnf(t13369,plain,
meet(X1,meet(join(zero,meet(one,join(zero,meet(X2,complement(X1))))),X3)) = meet(X1,meet(X3,join(zero,zero))),
inference(cp,[status(thm)],[t1906,t13355]) ).
cnf(t202438,plain,
meet(X1,meet(X3,join(zero,meet(one,join(zero,meet(X2,complement(X1))))))) = meet(X1,meet(X3,join(zero,zero))),
inference(step,[status(thm)],[t13369,t24]) ).
cnf(t202439,plain,
meet(X1,meet(X3,join(zero,meet(one,join(zero,meet(X2,complement(X1))))))) = meet(X1,meet(X3,zero)),
inference(step,[status(thm)],[t202438,t100]) ).
cnf(t202440,plain,
meet(X1,meet(X3,join(zero,meet(one,join(zero,meet(X2,complement(X1))))))) = meet(X1,zero),
inference(step,[status(thm)],[t202439,t126]) ).
cnf(t202441,plain,
meet(X1,meet(X3,join(zero,meet(one,join(zero,meet(X2,complement(X1))))))) = zero,
inference(step,[status(thm)],[t202440,t126]) ).
cnf(t14600,plain,
meet(X1,meet(X2,join(zero,meet(one,join(zero,meet(X3,complement(X1))))))) = zero,
inference(orient,[status(thm)],[t202441]) ).
cnf(t18537,plain,
meet(X1,meet(X2,join(zero,meet(one,join(zero,meet(X3,complement(X1))))))) = meet(X1,join(zero,meet(one,join(meet(X2,join(zero,meet(one,join(zero,meet(X3,complement(X1)))))),meet(X1,meet(X2,join(zero,meet(one,join(zero,meet(X3,complement(X1))))))))))),
inference(cp,[status(thm)],[t18520,t14600]) ).
cnf(t202546,plain,
zero = meet(X1,join(zero,meet(one,join(meet(X2,join(zero,meet(one,join(zero,meet(X3,complement(X1)))))),meet(X1,meet(X2,join(zero,meet(one,join(zero,meet(X3,complement(X1))))))))))),
inference(step,[status(thm)],[t18537,t14600]) ).
cnf(t202547,plain,
zero = meet(X1,join(zero,meet(one,join(meet(X2,join(zero,meet(one,join(zero,meet(X3,complement(X1)))))),zero)))),
inference(step,[status(thm)],[t202546,t14600]) ).
cnf(t202548,plain,
zero = meet(X1,join(zero,meet(one,meet(X2,join(zero,meet(one,join(zero,meet(X3,complement(X1))))))))),
inference(step,[status(thm)],[t202547,t100]) ).
cnf(t202549,plain,
zero = meet(X1,join(zero,meet(one,meet(join(zero,meet(X3,complement(X1))),X2)))),
inference(step,[status(thm)],[t202548,t1906]) ).
cnf(t202550,plain,
zero = meet(X1,join(zero,meet(X2,meet(one,join(zero,meet(X3,complement(X1))))))),
inference(step,[status(thm)],[t202549,t27]) ).
cnf(t18879,plain,
meet(X1,join(zero,meet(X2,meet(one,join(zero,meet(X3,complement(X1))))))) = zero,
inference(orient,[status(thm)],[t202550]) ).
cnf(t18881,plain,
zero = meet(X1,join(zero,meet(join(zero,meet(X2,complement(X1))),meet(X3,one)))),
inference(cp,[status(thm)],[t18879,t27]) ).
cnf(t202551,plain,
zero = meet(X1,join(zero,meet(join(zero,meet(X2,complement(X1))),X3))),
inference(step,[status(thm)],[t18881,t111]) ).
cnf(t202552,plain,
zero = meet(X1,join(zero,meet(X3,join(zero,meet(X2,complement(X1)))))),
inference(step,[status(thm)],[t202551,t24]) ).
cnf(t18949,plain,
meet(X1,join(zero,meet(X2,join(zero,meet(X3,complement(X1)))))) = zero,
inference(orient,[status(thm)],[t202552]) ).
cnf(t18952,plain,
zero = meet(complement(X1),join(zero,meet(X2,join(zero,meet(X3,X1))))),
inference(cp,[status(thm)],[t18949,t784]) ).
cnf(t202553,plain,
zero = meet(complement(X1),join(zero,meet(X2,join(zero,meet(X1,X3))))),
inference(step,[status(thm)],[t18952,t24]) ).
cnf(t19014,plain,
meet(complement(X1),join(zero,meet(X2,join(zero,meet(X1,X3))))) = zero,
inference(orient,[status(thm)],[t202553]) ).
cnf(t19019,plain,
zero = meet(complement(meet(X1,X2)),join(zero,meet(X1,join(zero,meet(X1,X2))))),
inference(cp,[status(thm)],[t19014,t4715]) ).
cnf(t202555,plain,
zero = meet(complement(meet(X1,X2)),join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t19019,t1678]) ).
cnf(t19167,plain,
meet(complement(meet(X1,X2)),join(zero,meet(X1,X2))) = zero,
inference(orient,[status(thm)],[t202555]) ).
cnf(t19198,plain,
join(zero,meet(X1,X2)) = ifeq(zero,zero,meet(X1,X2),join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t3642,t19167]) ).
cnf(t202556,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t19198,t18]) ).
cnf(t19264,plain,
join(zero,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t202556]) ).
cnf(t46462,plain,
join(zero,meet(X1,X2)) = join(meet(X1,X2),meet(X3,join(zero,meet(X1,X2)))),
inference(cp,[status(thm)],[t46458,t19264]) ).
cnf(t203471,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X3,join(zero,meet(X1,X2)))),
inference(step,[status(thm)],[t46462,t19264]) ).
cnf(t203472,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X3,meet(X1,X2))),
inference(step,[status(thm)],[t203471,t19264]) ).
cnf(t203473,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X2,meet(X3,X1))),
inference(step,[status(thm)],[t203472,t27]) ).
cnf(t203474,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t203473,t27]) ).
cnf(t46884,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t203474]) ).
cnf(t47052,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))),
inference(cp,[status(thm)],[t40213,t46884]) ).
cnf(t51262,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t47052]) ).
cnf(t51263,plain,
meet(X1,meet(X2,X3)) = meet(join(X4,meet(X1,X2)),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t51262,t24]) ).
cnf(t203705,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X3),meet(join(X4,meet(X1,X2)),X1)),
inference(step,[status(thm)],[t51263,t27]) ).
cnf(t203706,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t203705,t27]) ).
cnf(t58444,plain,
meet(X1,meet(meet(X2,X3),join(X4,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t203706]) ).
cnf(t58455,plain,
meet(X1,meet(X2,X2)) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t58444,t14]) ).
cnf(t203707,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t58455,t14]) ).
cnf(t58886,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t203707]) ).
cnf(t40231,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t40213,t188]) ).
cnf(t40360,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t40231]) ).
cnf(t40480,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X2,X3)))) = meet(X1,join(X2,meet(X3,X4))),
inference(cp,[status(thm)],[t47,t40360]) ).
cnf(t116145,plain,
meet(X1,join(X2,meet(meet(X3,X4),join(X2,X3)))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t40480]) ).
cnf(t116156,plain,
meet(one,join(X1,meet(X2,X3))) = join(X1,meet(meet(X2,X3),join(X1,X2))),
inference(cp,[status(thm)],[t116145,t45738]) ).
cnf(t204707,plain,
join(X1,meet(X2,X3)) = join(X1,meet(meet(X2,X3),join(X1,X2))),
inference(step,[status(thm)],[t116156,t45738]) ).
cnf(t116469,plain,
join(X1,meet(meet(X2,X3),join(X1,X2))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t204707]) ).
cnf(t116563,plain,
join(join(X1,X2),meet(meet(X3,join(X1,X2)),X4)) = join(join(X1,X2),meet(meet(meet(X3,join(X1,X2)),X4),join(X1,X2))),
inference(cp,[status(thm)],[t116469,t46458]) ).
cnf(t204799,plain,
join(join(X1,X2),meet(X4,meet(X3,join(X1,X2)))) = join(join(X1,X2),meet(meet(meet(X3,join(X1,X2)),X4),join(X1,X2))),
inference(step,[status(thm)],[t116563,t24]) ).
cnf(t204800,plain,
join(join(X1,X2),meet(X3,meet(join(X1,X2),X4))) = join(join(X1,X2),meet(meet(meet(X3,join(X1,X2)),X4),join(X1,X2))),
inference(step,[status(thm)],[t204799,t27]) ).
cnf(t204801,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X2)))) = join(join(X1,X2),meet(meet(meet(X3,join(X1,X2)),X4),join(X1,X2))),
inference(step,[status(thm)],[t204800,t24]) ).
cnf(t204802,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X2)))) = join(X1,X2),
inference(step,[status(thm)],[t204801,t46458]) ).
cnf(t121208,plain,
join(join(X1,X2),meet(X3,meet(X4,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t204802]) ).
cnf(t8909,plain,
meet(X1,meet(join(meet(X1,X2),meet(X2,join(X1,X3))),X4)) = meet(X1,meet(X4,join(zero,meet(X1,X2)))),
inference(cp,[status(thm)],[t1906,t8764]) ).
cnf(t202455,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X1,meet(X4,join(zero,meet(X1,X2)))),
inference(step,[status(thm)],[t8909,t24]) ).
cnf(t202456,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t202455,t1906]) ).
cnf(t14815,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,X4))))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t202456]) ).
cnf(t51264,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,X4))))) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
inference(cp,[status(thm)],[t51262,t14815]) ).
cnf(t203785,plain,
meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t51264,t14815]) ).
cnf(t64283,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t203785]) ).
cnf(t34688,plain,
X1 = meet(X1,join(join(X1,X2),meet(X1,complement(X3)))),
inference(cp,[status(thm)],[t34658,t3350]) ).
cnf(t34909,plain,
meet(X1,join(join(X1,X2),meet(X1,complement(X3)))) = X1,
inference(orient,[status(thm)],[t34688]) ).
cnf(t46488,plain,
join(join(X1,X2),meet(X1,complement(X3))) = join(join(join(X1,X2),meet(X1,complement(X3))),X1),
inference(cp,[status(thm)],[t46458,t34909]) ).
cnf(t204079,plain,
join(join(X1,X2),meet(X1,complement(X3))) = join(X1,join(join(X1,X2),meet(X1,complement(X3)))),
inference(step,[status(thm)],[t46488,t68]) ).
cnf(t204080,plain,
join(join(X1,X2),meet(X1,complement(X3))) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t204079,t188]) ).
cnf(t204081,plain,
join(join(X1,X2),meet(X1,complement(X3))) = join(X1,X2),
inference(step,[status(thm)],[t204080,t131]) ).
cnf(t91151,plain,
join(join(X1,X2),meet(X1,complement(X3))) = join(X1,X2),
inference(orient,[status(thm)],[t204081]) ).
cnf(t46581,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X4,join(X2,X3))),
inference(cp,[status(thm)],[t40213,t46458]) ).
cnf(t203582,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X3,join(X4,X2))),
inference(step,[status(thm)],[t46581,t73]) ).
cnf(t203583,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,join(X3,X4))),
inference(step,[status(thm)],[t203582,t73]) ).
cnf(t51045,plain,
meet(meet(X1,join(X2,X3)),join(X2,join(X3,X4))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t203583]) ).
cnf(t51196,plain,
join(X1,join(X2,X3)) = join(join(X1,join(X2,X3)),meet(X4,join(X1,X2))),
inference(cp,[status(thm)],[t46458,t51045]) ).
cnf(t203636,plain,
join(X1,join(X2,X3)) = join(meet(X4,join(X1,X2)),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t51196,t68]) ).
cnf(t203637,plain,
join(X1,join(X2,X3)) = join(join(X2,X3),join(meet(X4,join(X1,X2)),X1)),
inference(step,[status(thm)],[t203636,t73]) ).
cnf(t203638,plain,
join(X1,join(X2,X3)) = join(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t203637,t73]) ).
cnf(t54336,plain,
join(X1,join(join(X2,X3),meet(X4,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t203638]) ).
cnf(t54353,plain,
join(X1,join(zero,meet(X2,X3))) = join(X1,join(meet(X2,X3),meet(X4,join(X1,zero)))),
inference(cp,[status(thm)],[t54336,t19264]) ).
cnf(t203644,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X4,join(X1,zero)))),
inference(step,[status(thm)],[t54353,t19264]) ).
cnf(t203645,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X4,X1))),
inference(step,[status(thm)],[t203644,t100]) ).
cnf(t203646,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X1,X4))),
inference(step,[status(thm)],[t203645,t24]) ).
cnf(t203647,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X1,X4),meet(X2,X3))),
inference(step,[status(thm)],[t203646,t68]) ).
cnf(t55193,plain,
join(X1,join(meet(X1,X2),meet(X3,X4))) = join(X1,meet(X3,X4)),
inference(orient,[status(thm)],[t203647]) ).
cnf(t54341,plain,
join(X1,join(X2,X2)) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t54336,t16]) ).
cnf(t203639,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t54341,t16]) ).
cnf(t54568,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t203639]) ).
cnf(t771,plain,
X1 = ifeq(meet(X1,join(X2,complement(X1))),zero,ifeq(one,one,complement(join(X2,complement(X1))),X1),X1),
inference(cp,[status(thm)],[t740,t167]) ).
cnf(t201720,plain,
X1 = ifeq(meet(X1,join(X2,complement(X1))),zero,complement(join(X2,complement(X1))),X1),
inference(step,[status(thm)],[t771,t18]) ).
cnf(t1242,plain,
ifeq(meet(X1,join(X2,complement(X1))),zero,complement(join(X2,complement(X1))),X1) = X1,
inference(orient,[status(thm)],[t201720]) ).
cnf(t1811,plain,
meet(join(zero,complement(X1)),meet(X2,one)) = meet(X2,complement(X1)),
inference(cp,[status(thm)],[t27,t1793]) ).
cnf(t201771,plain,
meet(join(zero,complement(X1)),X2) = meet(X2,complement(X1)),
inference(step,[status(thm)],[t1811,t111]) ).
cnf(t201772,plain,
meet(X2,join(zero,complement(X1))) = meet(X2,complement(X1)),
inference(step,[status(thm)],[t201771,t24]) ).
cnf(t1821,plain,
meet(X1,join(zero,complement(X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t201772]) ).
cnf(t1828,plain,
X1 = ifeq(meet(X1,complement(X1)),zero,complement(join(zero,complement(X1))),X1),
inference(cp,[status(thm)],[t1242,t1821]) ).
cnf(t201773,plain,
X1 = ifeq(zero,zero,complement(join(zero,complement(X1))),X1),
inference(step,[status(thm)],[t1828,t58]) ).
cnf(t201774,plain,
X1 = complement(join(zero,complement(X1))),
inference(step,[status(thm)],[t201773,t18]) ).
cnf(t1839,plain,
complement(join(zero,complement(X1))) = X1,
inference(orient,[status(thm)],[t201774]) ).
cnf(t1844,plain,
join(zero,complement(X1)) = complement(X1),
inference(cp,[status(thm)],[t784,t1839]) ).
cnf(t1894,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1844]) ).
cnf(t46464,plain,
join(zero,complement(X1)) = join(complement(X1),meet(X2,join(zero,complement(X1)))),
inference(cp,[status(thm)],[t46458,t1894]) ).
cnf(t203469,plain,
complement(X1) = join(complement(X1),meet(X2,join(zero,complement(X1)))),
inference(step,[status(thm)],[t46464,t1894]) ).
cnf(t203470,plain,
complement(X1) = join(complement(X1),meet(X2,complement(X1))),
inference(step,[status(thm)],[t203469,t1821]) ).
cnf(t46735,plain,
join(complement(X1),meet(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t203470]) ).
cnf(t46747,plain,
meet(X1,complement(X2)) = meet(meet(X1,complement(X2)),join(X3,complement(X2))),
inference(cp,[status(thm)],[t40213,t46735]) ).
cnf(t47692,plain,
meet(meet(X1,complement(X2)),join(X3,complement(X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t46747]) ).
cnf(t47695,plain,
meet(X1,complement(complement(X2))) = meet(meet(X1,X2),join(X3,complement(complement(X2)))),
inference(cp,[status(thm)],[t47692,t784]) ).
cnf(t203491,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,complement(complement(X2)))),
inference(step,[status(thm)],[t47695,t784]) ).
cnf(t203492,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X2)),
inference(step,[status(thm)],[t203491,t784]) ).
cnf(t203493,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t203492,t68]) ).
cnf(t47776,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t203493]) ).
cnf(t47823,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(cp,[status(thm)],[t47776,t175]) ).
cnf(t203508,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(step,[status(thm)],[t47823,t175]) ).
cnf(t203509,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t203508,t68]) ).
cnf(t48203,plain,
meet(meet(X1,X2),join(X3,meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t203509]) ).
cnf(t8061,plain,
meet(X1,b) = meet(X1,join(b,meet(X1,a))),
inference(cp,[status(thm)],[t8046,t1737]) ).
cnf(t8248,plain,
meet(X1,join(b,meet(X1,a))) = meet(X1,b),
inference(orient,[status(thm)],[t8061]) ).
cnf(t21911,plain,
meet(join(a,X1),a) = meet(join(a,X1),join(a,meet(zero,meet(join(a,X1),b)))),
inference(cp,[status(thm)],[t21898,t8248]) ).
cnf(t202779,plain,
meet(a,join(a,X1)) = meet(join(a,X1),join(a,meet(zero,meet(join(a,X1),b)))),
inference(step,[status(thm)],[t21911,t24]) ).
cnf(t202780,plain,
a = meet(join(a,X1),join(a,meet(zero,meet(join(a,X1),b)))),
inference(step,[status(thm)],[t202779,t15]) ).
cnf(t202781,plain,
a = meet(join(X1,a),join(a,meet(zero,meet(join(a,X1),b)))),
inference(step,[status(thm)],[t202780,t68]) ).
cnf(t202782,plain,
a = meet(join(X1,a),join(a,meet(zero,meet(b,join(a,X1))))),
inference(step,[status(thm)],[t202781,t24]) ).
cnf(t202783,plain,
a = meet(join(X1,a),join(a,meet(zero,meet(b,join(X1,a))))),
inference(step,[status(thm)],[t202782,t68]) ).
cnf(t64,plain,
b = join(b,a),
inference(cp,[status(thm)],[t17,t63]) ).
cnf(t106,plain,
join(b,a) = b,
inference(orient,[status(thm)],[t64]) ).
cnf(t22376,plain,
a = meet(one,join(a,meet(zero,meet(b,join(X1,a))))),
inference(cp,[status(thm)],[t22372,t106]) ).
cnf(t22901,plain,
meet(one,join(a,meet(zero,meet(b,join(X1,a))))) = a,
inference(orient,[status(thm)],[t22376]) ).
cnf(t22981,plain,
meet(join(a,meet(zero,meet(b,join(X1,a)))),meet(X2,one)) = meet(X2,a),
inference(cp,[status(thm)],[t27,t22901]) ).
cnf(t202729,plain,
meet(join(a,meet(zero,meet(b,join(X1,a)))),X2) = meet(X2,a),
inference(step,[status(thm)],[t22981,t111]) ).
cnf(t202730,plain,
meet(X2,join(a,meet(zero,meet(b,join(X1,a))))) = meet(X2,a),
inference(step,[status(thm)],[t202729,t24]) ).
cnf(t23498,plain,
meet(X1,join(a,meet(zero,meet(b,join(X2,a))))) = meet(X1,a),
inference(orient,[status(thm)],[t202730]) ).
cnf(t23557,plain,
meet(zero,meet(b,join(X1,a))) = meet(zero,join(meet(b,join(X1,a)),meet(zero,meet(join(meet(b,join(X1,a)),X2),a)))),
inference(cp,[status(thm)],[t21898,t23498]) ).
cnf(t202731,plain,
meet(zero,meet(b,join(X1,a))) = zero,
inference(step,[status(thm)],[t23557,t2652]) ).
cnf(t23581,plain,
meet(zero,meet(b,join(X1,a))) = zero,
inference(orient,[status(thm)],[t202731]) ).
cnf(t202784,plain,
a = meet(join(X1,a),join(a,zero)),
inference(step,[status(thm)],[t202783,t23581]) ).
cnf(t202785,plain,
a = meet(join(X1,a),a),
inference(step,[status(thm)],[t202784,t100]) ).
cnf(t202786,plain,
a = meet(a,join(X1,a)),
inference(step,[status(thm)],[t202785,t24]) ).
cnf(t24695,plain,
meet(a,join(X1,a)) = a,
inference(orient,[status(thm)],[t202786]) ).
cnf(t48268,plain,
meet(a,join(X1,a)) = meet(a,join(X2,meet(join(X1,a),join(a,X3)))),
inference(cp,[status(thm)],[t48203,t24695]) ).
cnf(t203511,plain,
a = meet(a,join(X2,meet(join(X1,a),join(a,X3)))),
inference(step,[status(thm)],[t48268,t24695]) ).
cnf(t203512,plain,
a = meet(a,join(X2,meet(join(X1,a),join(X3,a)))),
inference(step,[status(thm)],[t203511,t68]) ).
cnf(t48642,plain,
meet(a,join(X1,meet(join(X2,a),join(X3,a)))) = a,
inference(orient,[status(thm)],[t203512]) ).
cnf(t48646,plain,
a = meet(a,join(X1,meet(b,join(X2,a)))),
inference(cp,[status(thm)],[t48642,t106]) ).
cnf(t48786,plain,
meet(a,join(X1,meet(b,join(X2,a)))) = a,
inference(orient,[status(thm)],[t48646]) ).
cnf(t48795,plain,
join(X1,meet(b,join(X2,a))) = join(join(X1,meet(b,join(X2,a))),a),
inference(cp,[status(thm)],[t46458,t48786]) ).
cnf(t203521,plain,
join(X1,meet(b,join(X2,a))) = join(a,join(X1,meet(b,join(X2,a)))),
inference(step,[status(thm)],[t48795,t68]) ).
cnf(t203522,plain,
join(X1,meet(b,join(X2,a))) = join(X1,join(meet(b,join(X2,a)),a)),
inference(step,[status(thm)],[t203521,t73]) ).
cnf(t203523,plain,
join(X1,meet(b,join(X2,a))) = join(X1,join(a,meet(b,join(X2,a)))),
inference(step,[status(thm)],[t203522,t68]) ).
cnf(t49368,plain,
join(X1,join(a,meet(b,join(X2,a)))) = join(X1,meet(b,join(X2,a))),
inference(orient,[status(thm)],[t203523]) ).
cnf(t54570,plain,
join(X1,a) = join(X1,meet(b,join(X1,a))),
inference(cp,[status(thm)],[t54568,t49368]) ).
cnf(t54821,plain,
join(X1,meet(b,join(X1,a))) = join(X1,a),
inference(orient,[status(thm)],[t54570]) ).
cnf(t55198,plain,
join(X1,meet(b,join(meet(X1,X2),a))) = join(X1,join(meet(X1,X2),a)),
inference(cp,[status(thm)],[t55193,t54821]) ).
cnf(t203687,plain,
join(X1,meet(b,join(a,meet(X1,X2)))) = join(X1,join(meet(X1,X2),a)),
inference(step,[status(thm)],[t55198,t68]) ).
cnf(t203688,plain,
join(X1,meet(b,join(a,meet(X1,X2)))) = join(X1,join(a,meet(X1,X2))),
inference(step,[status(thm)],[t203687,t68]) ).
cnf(t203689,plain,
join(X1,meet(b,join(a,meet(X1,X2)))) = join(X1,a),
inference(step,[status(thm)],[t203688,t188]) ).
cnf(t57644,plain,
join(X1,meet(b,join(a,meet(X1,X2)))) = join(X1,a),
inference(orient,[status(thm)],[t203689]) ).
cnf(t34918,plain,
complement(X1) = meet(complement(X1),join(join(complement(X1),X2),complement(X1))),
inference(cp,[status(thm)],[t34909,t14]) ).
cnf(t203080,plain,
complement(X1) = meet(complement(X1),join(complement(X1),join(complement(X1),X2))),
inference(step,[status(thm)],[t34918,t68]) ).
cnf(t203081,plain,
complement(X1) = meet(complement(X1),join(complement(X1),X2)),
inference(step,[status(thm)],[t203080,t131]) ).
cnf(t203082,plain,
complement(X1) = meet(complement(X1),join(X2,complement(X1))),
inference(step,[status(thm)],[t203081,t68]) ).
cnf(t35103,plain,
meet(complement(X1),join(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t203082]) ).
cnf(t57688,plain,
join(complement(X1),a) = join(complement(X1),meet(b,join(a,complement(X1)))),
inference(cp,[status(thm)],[t57644,t35103]) ).
cnf(t203690,plain,
join(a,complement(X1)) = join(complement(X1),meet(b,join(a,complement(X1)))),
inference(step,[status(thm)],[t57688,t68]) ).
cnf(t57769,plain,
join(complement(X1),meet(b,join(a,complement(X1)))) = join(a,complement(X1)),
inference(orient,[status(thm)],[t203690]) ).
cnf(t91154,plain,
join(complement(X1),meet(b,join(a,complement(X1)))) = join(join(a,complement(X1)),meet(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t91151,t57769]) ).
cnf(t204085,plain,
join(a,complement(X1)) = join(join(a,complement(X1)),meet(complement(X1),complement(X2))),
inference(step,[status(thm)],[t91154,t57769]) ).
cnf(t91484,plain,
join(join(a,complement(X1)),meet(complement(X1),complement(X2))) = join(a,complement(X1)),
inference(orient,[status(thm)],[t204085]) ).
cnf(t91498,plain,
meet(complement(X1),complement(X2)) = meet(meet(complement(X1),complement(X2)),join(a,complement(X1))),
inference(cp,[status(thm)],[t38397,t91484]) ).
cnf(t204089,plain,
meet(complement(X1),complement(X2)) = meet(join(a,complement(X1)),meet(complement(X1),complement(X2))),
inference(step,[status(thm)],[t91498,t24]) ).
cnf(t204090,plain,
meet(complement(X1),complement(X2)) = meet(complement(X2),meet(join(a,complement(X1)),complement(X1))),
inference(step,[status(thm)],[t204089,t27]) ).
cnf(t204091,plain,
meet(complement(X1),complement(X2)) = meet(complement(X1),meet(complement(X2),join(a,complement(X1)))),
inference(step,[status(thm)],[t204090,t27]) ).
cnf(t92176,plain,
meet(complement(X1),meet(complement(X2),join(a,complement(X1)))) = meet(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t204091]) ).
cnf(t92186,plain,
meet(complement(X1),meet(complement(X2),join(a,complement(X1)))) = meet(meet(complement(X1),complement(X2)),join(X3,meet(complement(X1),join(a,complement(X1))))),
inference(cp,[status(thm)],[t64283,t92176]) ).
cnf(t204092,plain,
meet(complement(X1),complement(X2)) = meet(meet(complement(X1),complement(X2)),join(X3,meet(complement(X1),join(a,complement(X1))))),
inference(step,[status(thm)],[t92186,t92176]) ).
cnf(t204093,plain,
meet(complement(X1),complement(X2)) = meet(meet(complement(X1),complement(X2)),join(X3,complement(X1))),
inference(step,[status(thm)],[t204092,t35103]) ).
cnf(t204094,plain,
meet(complement(X1),complement(X2)) = meet(join(X3,complement(X1)),meet(complement(X1),complement(X2))),
inference(step,[status(thm)],[t204093,t24]) ).
cnf(t204095,plain,
meet(complement(X1),complement(X2)) = meet(complement(X2),meet(join(X3,complement(X1)),complement(X1))),
inference(step,[status(thm)],[t204094,t27]) ).
cnf(t204096,plain,
meet(complement(X1),complement(X2)) = meet(complement(X1),meet(complement(X2),join(X3,complement(X1)))),
inference(step,[status(thm)],[t204095,t27]) ).
cnf(t92291,plain,
meet(complement(X1),meet(complement(X2),join(X3,complement(X1)))) = meet(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t204096]) ).
cnf(t121272,plain,
join(X1,complement(X2)) = join(join(X1,complement(X2)),meet(complement(X2),complement(X3))),
inference(cp,[status(thm)],[t121208,t92291]) ).
cnf(t121977,plain,
join(join(X1,complement(X2)),meet(complement(X2),complement(X3))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t121272]) ).
cnf(t121980,plain,
join(X1,complement(complement(X2))) = join(join(X1,X2),meet(complement(complement(X2)),complement(X3))),
inference(cp,[status(thm)],[t121977,t784]) ).
cnf(t204803,plain,
join(X1,X2) = join(join(X1,X2),meet(complement(complement(X2)),complement(X3))),
inference(step,[status(thm)],[t121980,t784]) ).
cnf(t204804,plain,
join(X1,X2) = join(join(X1,X2),meet(complement(X3),complement(complement(X2)))),
inference(step,[status(thm)],[t204803,t24]) ).
cnf(t204805,plain,
join(X1,X2) = join(join(X1,X2),meet(complement(X3),X2)),
inference(step,[status(thm)],[t204804,t784]) ).
cnf(t204806,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,complement(X3))),
inference(step,[status(thm)],[t204805,t24]) ).
cnf(t122087,plain,
join(join(X1,X2),meet(X2,complement(X3))) = join(X1,X2),
inference(orient,[status(thm)],[t204806]) ).
cnf(t122113,plain,
join(X1,join(X2,meet(X1,X3))) = join(join(X1,X2),meet(join(X2,meet(X1,X3)),complement(X4))),
inference(cp,[status(thm)],[t122087,t188]) ).
cnf(t204982,plain,
join(X1,X2) = join(join(X1,X2),meet(join(X2,meet(X1,X3)),complement(X4))),
inference(step,[status(thm)],[t122113,t188]) ).
cnf(t204983,plain,
join(X1,X2) = join(join(X1,X2),meet(complement(X4),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t204982,t24]) ).
cnf(t139927,plain,
join(join(X1,X2),meet(complement(X3),join(X2,meet(X1,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t204983]) ).
cnf(t140156,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X2,meet(X1,X4)))),
inference(cp,[status(thm)],[t139927,t784]) ).
cnf(t142271,plain,
join(join(X1,X2),meet(X3,join(X2,meet(X1,X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t140156]) ).
cnf(t142974,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(meet(X1,join(X2,meet(X3,X4))),join(X3,X2)),
inference(cp,[status(thm)],[t38397,t142271]) ).
cnf(t205489,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(join(X3,X2),meet(X1,join(X2,meet(X3,X4)))),
inference(step,[status(thm)],[t142974,t24]) ).
cnf(t205490,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,meet(join(X2,meet(X3,X4)),join(X3,X2))),
inference(step,[status(thm)],[t205489,t27]) ).
cnf(t205491,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,meet(join(X3,X2),join(X2,meet(X3,X4)))),
inference(step,[status(thm)],[t205490,t24]) ).
cnf(t205492,plain,
meet(X1,join(X2,meet(X3,X4))) = meet(X1,meet(join(X2,X3),join(X2,meet(X3,X4)))),
inference(step,[status(thm)],[t205491,t68]) ).
cnf(t183359,plain,
meet(X1,meet(join(X2,X3),join(X2,meet(X3,X4)))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t205492]) ).
cnf(t122234,plain,
join(join(X1,X2),meet(meet(X2,complement(X3)),X4)) = join(join(X1,X2),meet(meet(meet(X2,complement(X3)),X4),join(X1,X2))),
inference(cp,[status(thm)],[t116469,t122087]) ).
cnf(t204811,plain,
join(join(X1,X2),meet(X4,meet(X2,complement(X3)))) = join(join(X1,X2),meet(meet(meet(X2,complement(X3)),X4),join(X1,X2))),
inference(step,[status(thm)],[t122234,t24]) ).
cnf(t204812,plain,
join(join(X1,X2),meet(X2,meet(complement(X3),X4))) = join(join(X1,X2),meet(meet(meet(X2,complement(X3)),X4),join(X1,X2))),
inference(step,[status(thm)],[t204811,t27]) ).
cnf(t204813,plain,
join(join(X1,X2),meet(X2,meet(X4,complement(X3)))) = join(join(X1,X2),meet(meet(meet(X2,complement(X3)),X4),join(X1,X2))),
inference(step,[status(thm)],[t204812,t24]) ).
cnf(t204814,plain,
join(join(X1,X2),meet(X2,meet(X4,complement(X3)))) = join(X1,X2),
inference(step,[status(thm)],[t204813,t46458]) ).
cnf(t122470,plain,
join(join(X1,X2),meet(X2,meet(X3,complement(X4)))) = join(X1,X2),
inference(orient,[status(thm)],[t204814]) ).
cnf(t122618,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,meet(X3,X4))),
inference(cp,[status(thm)],[t122470,t784]) ).
cnf(t122726,plain,
join(join(X1,X2),meet(X2,meet(X3,X4))) = join(X1,X2),
inference(orient,[status(thm)],[t122618]) ).
cnf(t51275,plain,
meet(X1,meet(one,join(X2,X3))) = meet(meet(X1,join(X2,X3)),join(X4,meet(X1,one))),
inference(cp,[status(thm)],[t51262,t45738]) ).
cnf(t203584,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X4,meet(X1,one))),
inference(step,[status(thm)],[t51275,t45621]) ).
cnf(t203585,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X4,X1)),
inference(step,[status(thm)],[t203584,t111]) ).
cnf(t203586,plain,
meet(X1,join(X2,X3)) = meet(join(X4,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t203585,t24]) ).
cnf(t203587,plain,
meet(X1,join(X2,X3)) = meet(join(X2,X3),meet(join(X4,X1),X1)),
inference(step,[status(thm)],[t203586,t27]) ).
cnf(t203588,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X4,X1))),
inference(step,[status(thm)],[t203587,t27]) ).
cnf(t203589,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,X4))),
inference(step,[status(thm)],[t203588,t68]) ).
cnf(t203590,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X4),join(X2,X3))),
inference(step,[status(thm)],[t203589,t24]) ).
cnf(t51576,plain,
meet(X1,meet(join(X1,X2),join(X3,X4))) = meet(X1,join(X3,X4)),
inference(orient,[status(thm)],[t203590]) ).
cnf(t122878,plain,
join(X1,X2) = join(join(X1,X2),meet(X2,join(X3,X4))),
inference(cp,[status(thm)],[t122726,t51576]) ).
cnf(t123081,plain,
join(join(X1,X2),meet(X2,join(X3,X4))) = join(X1,X2),
inference(orient,[status(thm)],[t122878]) ).
cnf(t123114,plain,
join(X1,meet(X1,X2)) = join(X1,meet(meet(X1,X2),join(X3,X4))),
inference(cp,[status(thm)],[t123081,t17]) ).
cnf(t204815,plain,
X1 = join(X1,meet(meet(X1,X2),join(X3,X4))),
inference(step,[status(thm)],[t123114,t17]) ).
cnf(t123621,plain,
join(X1,meet(meet(X1,X2),join(X3,X4))) = X1,
inference(orient,[status(thm)],[t204815]) ).
cnf(t123760,plain,
meet(meet(X1,X2),join(X3,X4)) = meet(meet(meet(X1,X2),join(X3,X4)),X1),
inference(cp,[status(thm)],[t38397,t123621]) ).
cnf(t204870,plain,
meet(meet(X1,X2),join(X3,X4)) = meet(X1,meet(meet(X1,X2),join(X3,X4))),
inference(step,[status(thm)],[t123760,t24]) ).
cnf(t128604,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(meet(X1,X2),join(X3,X4)),
inference(orient,[status(thm)],[t204870]) ).
cnf(t128662,plain,
meet(meet(one,join(X1,X2)),join(X3,X4)) = meet(one,meet(join(X1,X2),join(X3,X4))),
inference(cp,[status(thm)],[t128604,t45738]) ).
cnf(t204881,plain,
meet(join(X3,X4),meet(one,join(X1,X2))) = meet(one,meet(join(X1,X2),join(X3,X4))),
inference(step,[status(thm)],[t128662,t24]) ).
cnf(t204882,plain,
meet(join(X3,X4),join(X1,X2)) = meet(one,meet(join(X1,X2),join(X3,X4))),
inference(step,[status(thm)],[t204881,t45621]) ).
cnf(t204883,plain,
meet(join(X1,X2),join(X3,X4)) = meet(one,meet(join(X1,X2),join(X3,X4))),
inference(step,[status(thm)],[t204882,t24]) ).
cnf(t131312,plain,
meet(one,meet(join(X1,X2),join(X3,X4))) = meet(join(X1,X2),join(X3,X4)),
inference(orient,[status(thm)],[t204883]) ).
cnf(t183367,plain,
meet(one,join(X1,meet(X2,X3))) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t183359,t131312]) ).
cnf(t205493,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t183367,t45738]) ).
cnf(t184077,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t205493]) ).
cnf(t184135,plain,
join(X1,meet(join(X1,X2),X3)) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t184077,t131]) ).
cnf(t205601,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t184135,t24]) ).
cnf(t205602,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t205601,t24]) ).
cnf(t198275,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))) = join(X1,meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t205602]) ).
cnf(t198730,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t58886,t198275]) ).
cnf(t199807,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t198730]) ).
cnf(t205608,plain,
meet(complement(X1),join(X1,X2)) = meet(complement(X1),join(X1,meet(X2,complement(X1)))),
inference(step,[status(thm)],[t2746,t199807]) ).
cnf(t200058,plain,
meet(complement(X1),join(X1,X2)) = meet(complement(X1),join(X1,meet(X2,complement(X1)))),
inference(rw,[status(thm)],[t205608]) ).
cnf(t200441,plain,
meet(complement(X1),join(X1,meet(X2,complement(X1)))) = meet(complement(X1),join(X1,X2)),
inference(orient,[status(thm)],[t200058]) ).
cnf(t200449,plain,
meet(complement(complement(X1)),join(complement(X1),X2)) = meet(X1,join(complement(X1),meet(X2,complement(complement(X1))))),
inference(cp,[status(thm)],[t200441,t784]) ).
cnf(t205623,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,join(complement(X1),meet(X2,complement(complement(X1))))),
inference(step,[status(thm)],[t200449,t784]) ).
cnf(t205624,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(complement(X1),meet(X2,complement(complement(X1))))),
inference(step,[status(thm)],[t205623,t68]) ).
cnf(t205625,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(complement(X1),meet(X2,X1))),
inference(step,[status(thm)],[t205624,t784]) ).
cnf(t205626,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(complement(X1),meet(X1,X2))),
inference(step,[status(thm)],[t205625,t24]) ).
cnf(t200612,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(X2,complement(X1))),
inference(orient,[status(thm)],[t205626]) ).
cnf(t200956,plain,
meet(a,join(complement(b),complement(a))) = meet(a,join(complement(a),zero)),
inference(cp,[status(thm)],[t200612,t12123]) ).
cnf(t205631,plain,
meet(a,join(complement(b),complement(a))) = meet(a,complement(a)),
inference(step,[status(thm)],[t200956,t100]) ).
cnf(t205632,plain,
meet(a,join(complement(b),complement(a))) = zero,
inference(step,[status(thm)],[t205631,t58]) ).
cnf(t201192,plain,
meet(a,join(complement(b),complement(a))) = zero,
inference(orient,[status(thm)],[t205632]) ).
cnf(t201193,plain,
join(complement(b),complement(a)) = ifeq(zero,zero,ifeq(join(a,join(complement(b),complement(a))),one,complement(a),join(complement(b),complement(a))),join(complement(b),complement(a))),
inference(cp,[status(thm)],[t19,t201192]) ).
cnf(t205633,plain,
join(complement(b),complement(a)) = ifeq(join(a,join(complement(b),complement(a))),one,complement(a),join(complement(b),complement(a))),
inference(step,[status(thm)],[t201193,t18]) ).
cnf(t205634,plain,
join(complement(b),complement(a)) = ifeq(one,one,complement(a),join(complement(b),complement(a))),
inference(step,[status(thm)],[t205633,t167]) ).
cnf(t205635,plain,
join(complement(b),complement(a)) = complement(a),
inference(step,[status(thm)],[t205634,t18]) ).
cnf(t201331,plain,
join(complement(b),complement(a)) = complement(a),
inference(orient,[status(thm)],[t205635]) ).
cnf(f13,negated_conjecture,
join(complement(b),complement(a)) != complement(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f13_nnf,plain,
join(complement(b),complement(a)) != complement(a),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
join(complement(b),complement(a)) != complement(a),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
join(complement(b),complement(a)) != complement(a),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
join(complement(b),complement(a)) != complement(a),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(g0_0,plain,
complement(a) != complement(a),
inference(rw,[status(thm)],[goal_0,t201331]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT252-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n007.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 20:39:38 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 91.56/12.59 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 91.56/12.59 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------