FindProof---0.1.UNS-Prf.s

%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : LAT204-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300

% Computer : n019.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Fri Sep 25 01:55:57 PM UTC 2026

% Result   : Unsatisfiable 241.68s 35.72s
% Output   : Proof 241.68s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% Comments : 
%------------------------------------------------------------------------------
cnf(f3,axiom,
    join(X,meet(X,Y)) = X,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).

fof(f3_nnf,plain,
    ! [X,Y] : join(X,meet(X,Y)) = X,
    inference(nnf_transformation,[status(thm)],[f3]) ).

fof(f3_sk,plain,
    ! [X,Y] : join(X,meet(X,Y)) = X,
    inference(skolemisation,[status(esa)],[f3_nnf]) ).

cnf(c3,plain,
    join(X0,meet(X0,X1)) = X0,
    inference(cnf_transformation,[status(esa)],[f3_sk]) ).

cnf(t6,plain,
    join(X1,meet(X1,X2)) = X1,
    inference(equality_encoding,[status(esa)],[c3]) ).

cnf(t14,plain,
    join(X1,meet(X1,X2)) = X1,
    inference(orient,[status(thm)],[t6]) ).

cnf(f6,axiom,
    meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).

fof(f6_nnf,plain,
    ! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
    inference(nnf_transformation,[status(thm)],[f6]) ).

fof(f6_sk,plain,
    ! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
    inference(skolemisation,[status(esa)],[f6_nnf]) ).

cnf(c6,plain,
    meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
    inference(cnf_transformation,[status(esa)],[f6_sk]) ).

cnf(t10,plain,
    meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
    inference(equality_encoding,[status(esa)],[c6]) ).

cnf(f4,axiom,
    meet(X,Y) = meet(Y,X),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).

fof(f4_nnf,plain,
    ! [X,Y] : meet(X,Y) = meet(Y,X),
    inference(nnf_transformation,[status(thm)],[f4]) ).

fof(f4_sk,plain,
    ! [X,Y] : meet(X,Y) = meet(Y,X),
    inference(skolemisation,[status(esa)],[f4_nnf]) ).

cnf(c4,plain,
    meet(X0,X1) = meet(X1,X0),
    inference(cnf_transformation,[status(esa)],[f4_sk]) ).

cnf(t7,plain,
    meet(X1,X2) = meet(X2,X1),
    inference(equality_encoding,[status(esa)],[c4]) ).

cnf(t51,plain,
    meet(X1,X2) = meet(X2,X1),
    inference(orient,[status(thm)],[t7]) ).

cnf(t710099,plain,
    meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
    inference(step,[status(thm)],[t10,t51]) ).

cnf(t67,plain,
    meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
    inference(orient,[status(thm)],[t710099]) ).

cnf(f11,axiom,
    meet(X,join(Y,Z)) = meet(X,join(Y,meet(join(X,Y),join(Z,meet(X,Y))))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H58) ).

fof(f11_nnf,plain,
    ! [X,Y,Z] : meet(X,join(Y,Z)) = meet(X,join(Y,meet(join(X,Y),join(Z,meet(X,Y))))),
    inference(nnf_transformation,[status(thm)],[f11]) ).

fof(f11_sk,plain,
    ! [X,Y,Z] : meet(X,join(Y,Z)) = meet(X,join(Y,meet(join(X,Y),join(Z,meet(X,Y))))),
    inference(skolemisation,[status(esa)],[f11_nnf]) ).

cnf(c11,plain,
    meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(join(X0,X1),join(X2,meet(X0,X1))))),
    inference(cnf_transformation,[status(esa)],[f11_sk]) ).

cnf(t12,plain,
    meet(X1,join(X2,meet(join(X1,X2),join(X3,meet(X1,X2))))) = meet(X1,join(X2,X3)),
    inference(equality_encoding,[status(esa)],[c11]) ).

cnf(t54,plain,
    meet(X1,join(X2,meet(join(X1,X2),join(X3,meet(X1,X2))))) = meet(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t12]) ).

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(t15,plain,
    meet(X1,X1) = X1,
    inference(orient,[status(thm)],[t1]) ).

cnf(t70,plain,
    meet(X1,meet(X2,X1)) = meet(X2,X1),
    inference(cp,[status(thm)],[t67,t15]) ).

cnf(t710103,plain,
    meet(X1,meet(X1,X2)) = meet(X2,X1),
    inference(step,[status(thm)],[t70,t67]) ).

cnf(t710104,plain,
    meet(X1,meet(X1,X2)) = meet(X1,X2),
    inference(step,[status(thm)],[t710103,t51]) ).

cnf(t125,plain,
    meet(X1,meet(X1,X2)) = meet(X1,X2),
    inference(orient,[status(thm)],[t710104]) ).

cnf(f9,axiom,
    meet(X,complement(X)) = zero,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).

fof(f9_nnf,plain,
    ! [X] : meet(X,complement(X)) = zero,
    inference(nnf_transformation,[status(thm)],[f9]) ).

fof(f9_sk,plain,
    ! [X] : meet(X,complement(X)) = zero,
    inference(skolemisation,[status(esa)],[f9_nnf]) ).

cnf(c9,plain,
    meet(X0,complement(X0)) = zero,
    inference(cnf_transformation,[status(esa)],[f9_sk]) ).

cnf(t3,plain,
    meet(X1,complement(X1)) = zero,
    inference(equality_encoding,[status(esa)],[c9]) ).

cnf(t91,plain,
    meet(X1,complement(X1)) = zero,
    inference(orient,[status(thm)],[t3]) ).

cnf(t128,plain,
    meet(X1,complement(X1)) = meet(X1,zero),
    inference(cp,[status(thm)],[t125,t91]) ).

cnf(t710105,plain,
    zero = meet(X1,zero),
    inference(step,[status(thm)],[t128,t91]) ).

cnf(t136,plain,
    meet(X1,zero) = zero,
    inference(orient,[status(thm)],[t710105]) ).

cnf(t139,plain,
    meet(X1,join(zero,X2)) = meet(X1,join(zero,meet(join(X1,zero),join(X2,zero)))),
    inference(cp,[status(thm)],[t54,t136]) ).

cnf(f5,axiom,
    join(X,Y) = join(Y,X),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).

fof(f5_nnf,plain,
    ! [X,Y] : join(X,Y) = join(Y,X),
    inference(nnf_transformation,[status(thm)],[f5]) ).

fof(f5_sk,plain,
    ! [X,Y] : join(X,Y) = join(Y,X),
    inference(skolemisation,[status(esa)],[f5_nnf]) ).

cnf(c5,plain,
    join(X0,X1) = join(X1,X0),
    inference(cnf_transformation,[status(esa)],[f5_sk]) ).

cnf(t5,plain,
    join(X1,X2) = join(X2,X1),
    inference(equality_encoding,[status(esa)],[c5]) ).

cnf(t23,plain,
    join(X1,X2) = join(X2,X1),
    inference(orient,[status(thm)],[t5]) ).

cnf(t710128,plain,
    meet(X1,join(X2,zero)) = meet(X1,join(zero,meet(join(X1,zero),join(X2,zero)))),
    inference(step,[status(thm)],[t139,t23]) ).

cnf(t92,plain,
    X1 = join(X1,zero),
    inference(cp,[status(thm)],[t14,t91]) ).

cnf(t102,plain,
    join(X1,zero) = X1,
    inference(orient,[status(thm)],[t92]) ).

cnf(t710129,plain,
    meet(X1,X2) = meet(X1,join(zero,meet(join(X1,zero),join(X2,zero)))),
    inference(step,[status(thm)],[t710128,t102]) ).

cnf(t710130,plain,
    meet(X1,X2) = meet(X1,join(zero,meet(X1,join(X2,zero)))),
    inference(step,[status(thm)],[t710129,t102]) ).

cnf(t710131,plain,
    meet(X1,X2) = meet(X1,join(zero,meet(X1,X2))),
    inference(step,[status(thm)],[t710130,t102]) ).

cnf(t218,plain,
    meet(X1,join(zero,meet(X1,X2))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710131]) ).

cnf(t230,plain,
    meet(X1,meet(join(zero,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
    inference(cp,[status(thm)],[t67,t218]) ).

cnf(t710155,plain,
    meet(X1,meet(X3,join(zero,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
    inference(step,[status(thm)],[t230,t51]) ).

cnf(t710156,plain,
    meet(X1,meet(X3,join(zero,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
    inference(step,[status(thm)],[t710155,t67]) ).

cnf(t710157,plain,
    meet(X1,meet(X3,join(zero,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
    inference(step,[status(thm)],[t710156,t67]) ).

cnf(t296,plain,
    meet(X1,meet(X2,join(zero,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
    inference(orient,[status(thm)],[t710157]) ).

cnf(f2,axiom,
    meet(X,join(X,Y)) = X,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).

fof(f2_nnf,plain,
    ! [X,Y] : meet(X,join(X,Y)) = X,
    inference(nnf_transformation,[status(thm)],[f2]) ).

fof(f2_sk,plain,
    ! [X,Y] : meet(X,join(X,Y)) = X,
    inference(skolemisation,[status(esa)],[f2_nnf]) ).

cnf(c2,plain,
    meet(X0,join(X0,X1)) = X0,
    inference(cnf_transformation,[status(esa)],[f2_sk]) ).

cnf(t8,plain,
    meet(X1,join(X1,X2)) = X1,
    inference(equality_encoding,[status(esa)],[c2]) ).

cnf(t16,plain,
    meet(X1,join(X1,X2)) = X1,
    inference(orient,[status(thm)],[t8]) ).

cnf(t71,plain,
    meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
    inference(cp,[status(thm)],[t67,t16]) ).

cnf(t710117,plain,
    meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
    inference(step,[status(thm)],[t71,t67]) ).

cnf(t710118,plain,
    meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
    inference(step,[status(thm)],[t710117,t51]) ).

cnf(t710119,plain,
    meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
    inference(step,[status(thm)],[t710118,t51]) ).

cnf(t183,plain,
    meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710119]) ).

cnf(t133,plain,
    meet(X1,join(meet(X1,X2),X3)) = meet(X1,join(meet(X1,X2),meet(join(X1,meet(X1,X2)),join(X3,meet(X1,X2))))),
    inference(cp,[status(thm)],[t54,t125]) ).

cnf(t710262,plain,
    meet(X1,join(X3,meet(X1,X2))) = meet(X1,join(meet(X1,X2),meet(join(X1,meet(X1,X2)),join(X3,meet(X1,X2))))),
    inference(step,[status(thm)],[t133,t23]) ).

cnf(t710263,plain,
    meet(X1,join(X3,meet(X1,X2))) = meet(X1,join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2))))),
    inference(step,[status(thm)],[t710262,t14]) ).

cnf(t726,plain,
    meet(X1,join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2))))) = meet(X1,join(X3,meet(X1,X2))),
    inference(orient,[status(thm)],[t710263]) ).

cnf(t746,plain,
    meet(meet(X1,X2),X1) = meet(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
    inference(cp,[status(thm)],[t183,t726]) ).

cnf(t710264,plain,
    meet(X1,meet(X1,X2)) = meet(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
    inference(step,[status(thm)],[t746,t51]) ).

cnf(t710265,plain,
    meet(X1,X2) = meet(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
    inference(step,[status(thm)],[t710264,t125]) ).

cnf(t710266,plain,
    meet(X1,X2) = meet(X1,meet(join(X3,meet(X1,X2)),meet(X1,X2))),
    inference(step,[status(thm)],[t710265,t67]) ).

cnf(t710267,plain,
    meet(X1,X2) = meet(X1,meet(X2,meet(join(X3,meet(X1,X2)),X1))),
    inference(step,[status(thm)],[t710266,t67]) ).

cnf(t710268,plain,
    meet(X1,X2) = meet(X1,meet(X1,meet(X2,join(X3,meet(X1,X2))))),
    inference(step,[status(thm)],[t710267,t67]) ).

cnf(t710269,plain,
    meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
    inference(step,[status(thm)],[t710268,t125]) ).

cnf(t754,plain,
    meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710269]) ).

cnf(t787,plain,
    meet(X1,meet(meet(X2,join(X3,meet(X1,X2))),Y3)) = meet(X1,meet(Y3,join(zero,meet(X1,X2)))),
    inference(cp,[status(thm)],[t296,t754]) ).

cnf(t710271,plain,
    meet(X1,meet(Y3,meet(X2,join(X3,meet(X1,X2))))) = meet(X1,meet(Y3,join(zero,meet(X1,X2)))),
    inference(step,[status(thm)],[t787,t51]) ).

cnf(t710272,plain,
    meet(X1,meet(X2,meet(join(X3,meet(X1,X2)),Y3))) = meet(X1,meet(Y3,join(zero,meet(X1,X2)))),
    inference(step,[status(thm)],[t710271,t67]) ).

cnf(t710273,plain,
    meet(X1,meet(X2,meet(Y3,join(X3,meet(X1,X2))))) = meet(X1,meet(Y3,join(zero,meet(X1,X2)))),
    inference(step,[status(thm)],[t710272,t51]) ).

cnf(t710274,plain,
    meet(X1,meet(X2,meet(Y3,join(X3,meet(X1,X2))))) = meet(X1,meet(X2,Y3)),
    inference(step,[status(thm)],[t710273,t296]) ).

cnf(t830,plain,
    meet(X1,meet(X2,meet(X3,join(Y3,meet(X1,X2))))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t710274]) ).

cnf(t870,plain,
    meet(X1,meet(meet(X2,meet(X3,join(Y3,meet(X1,X2)))),Y4)) = meet(X1,meet(Y4,join(zero,meet(X1,meet(X2,X3))))),
    inference(cp,[status(thm)],[t296,t830]) ).

cnf(t710283,plain,
    meet(X1,meet(Y4,meet(X2,meet(X3,join(Y3,meet(X1,X2)))))) = meet(X1,meet(Y4,join(zero,meet(X1,meet(X2,X3))))),
    inference(step,[status(thm)],[t870,t51]) ).

cnf(t710284,plain,
    meet(X1,meet(X2,meet(meet(X3,join(Y3,meet(X1,X2))),Y4))) = meet(X1,meet(Y4,join(zero,meet(X1,meet(X2,X3))))),
    inference(step,[status(thm)],[t710283,t67]) ).

cnf(t710285,plain,
    meet(X1,meet(X2,meet(Y4,meet(X3,join(Y3,meet(X1,X2)))))) = meet(X1,meet(Y4,join(zero,meet(X1,meet(X2,X3))))),
    inference(step,[status(thm)],[t710284,t51]) ).

cnf(t710286,plain,
    meet(X1,meet(X2,meet(X3,meet(join(Y3,meet(X1,X2)),Y4)))) = meet(X1,meet(Y4,join(zero,meet(X1,meet(X2,X3))))),
    inference(step,[status(thm)],[t710285,t67]) ).

cnf(t710287,plain,
    meet(X1,meet(X2,meet(X3,meet(Y4,join(Y3,meet(X1,X2)))))) = meet(X1,meet(Y4,join(zero,meet(X1,meet(X2,X3))))),
    inference(step,[status(thm)],[t710286,t51]) ).

cnf(t710288,plain,
    meet(X1,meet(X2,meet(X3,meet(Y4,join(Y3,meet(X1,X2)))))) = meet(X1,meet(meet(X2,X3),Y4)),
    inference(step,[status(thm)],[t710287,t296]) ).

cnf(t710289,plain,
    meet(X1,meet(X2,meet(X3,meet(Y4,join(Y3,meet(X1,X2)))))) = meet(X1,meet(Y4,meet(X2,X3))),
    inference(step,[status(thm)],[t710288,t51]) ).

cnf(t710290,plain,
    meet(X1,meet(X2,meet(X3,meet(Y4,join(Y3,meet(X1,X2)))))) = meet(X1,meet(X3,meet(Y4,X2))),
    inference(step,[status(thm)],[t710289,t67]) ).

cnf(t710291,plain,
    meet(X1,meet(X2,meet(X3,meet(Y4,join(Y3,meet(X1,X2)))))) = meet(X1,meet(X2,meet(X3,Y4))),
    inference(step,[status(thm)],[t710290,t67]) ).

cnf(t1122,plain,
    meet(X1,meet(X2,meet(X3,meet(Y3,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X2,meet(X3,Y3))),
    inference(orient,[status(thm)],[t710291]) ).

cnf(t72,plain,
    meet(join(X1,meet(join(X2,X1),join(X3,meet(X2,X1)))),meet(Y3,X2)) = meet(Y3,meet(X2,join(X1,X3))),
    inference(cp,[status(thm)],[t67,t54]) ).

cnf(t710359,plain,
    meet(X2,meet(join(X1,meet(join(X2,X1),join(X3,meet(X2,X1)))),Y3)) = meet(Y3,meet(X2,join(X1,X3))),
    inference(step,[status(thm)],[t72,t67]) ).

cnf(t710360,plain,
    meet(X2,meet(Y3,join(X1,meet(join(X2,X1),join(X3,meet(X2,X1)))))) = meet(Y3,meet(X2,join(X1,X3))),
    inference(step,[status(thm)],[t710359,t51]) ).

cnf(t710361,plain,
    meet(X2,meet(Y3,join(X1,meet(join(X1,X2),join(X3,meet(X2,X1)))))) = meet(Y3,meet(X2,join(X1,X3))),
    inference(step,[status(thm)],[t710360,t23]) ).

cnf(t710362,plain,
    meet(X2,meet(Y3,join(X1,meet(join(X1,X2),join(X3,meet(X1,X2)))))) = meet(Y3,meet(X2,join(X1,X3))),
    inference(step,[status(thm)],[t710361,t51]) ).

cnf(t710363,plain,
    meet(X2,meet(Y3,join(X1,meet(join(X1,X2),join(X3,meet(X1,X2)))))) = meet(X2,meet(join(X1,X3),Y3)),
    inference(step,[status(thm)],[t710362,t67]) ).

cnf(t710364,plain,
    meet(X2,meet(Y3,join(X1,meet(join(X1,X2),join(X3,meet(X1,X2)))))) = meet(X2,meet(Y3,join(X1,X3))),
    inference(step,[status(thm)],[t710363,t51]) ).

cnf(t1618,plain,
    meet(X1,meet(X2,join(X3,meet(join(X3,X1),join(Y3,meet(X3,X1)))))) = meet(X1,meet(X2,join(X3,Y3))),
    inference(orient,[status(thm)],[t710364]) ).

cnf(t1661,plain,
    meet(join(zero,meet(X1,X2)),meet(X3,join(X1,Y3))) = meet(join(zero,meet(X1,X2)),meet(X3,join(X1,meet(join(X1,join(zero,meet(X1,X2))),join(Y3,meet(X1,X2)))))),
    inference(cp,[status(thm)],[t1618,t218]) ).

cnf(t710395,plain,
    meet(join(X1,Y3),meet(join(zero,meet(X1,X2)),X3)) = meet(join(zero,meet(X1,X2)),meet(X3,join(X1,meet(join(X1,join(zero,meet(X1,X2))),join(Y3,meet(X1,X2)))))),
    inference(step,[status(thm)],[t1661,t67]) ).

cnf(t710396,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(join(zero,meet(X1,X2)),meet(X3,join(X1,meet(join(X1,join(zero,meet(X1,X2))),join(Y3,meet(X1,X2)))))),
    inference(step,[status(thm)],[t710395,t67]) ).

cnf(t710397,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X3,meet(join(X1,meet(join(X1,join(zero,meet(X1,X2))),join(Y3,meet(X1,X2)))),join(zero,meet(X1,X2)))),
    inference(step,[status(thm)],[t710396,t67]) ).

cnf(t710398,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X3,meet(join(zero,meet(X1,X2)),join(X1,meet(join(X1,join(zero,meet(X1,X2))),join(Y3,meet(X1,X2)))))),
    inference(step,[status(thm)],[t710397,t51]) ).

cnf(t710399,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X3,meet(join(zero,meet(X1,X2)),join(X1,meet(join(Y3,meet(X1,X2)),join(X1,join(zero,meet(X1,X2))))))),
    inference(step,[status(thm)],[t710398,t51]) ).

cnf(f7,axiom,
    join(join(X,Y),Z) = join(X,join(Y,Z)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).

fof(f7_nnf,plain,
    ! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
    inference(nnf_transformation,[status(thm)],[f7]) ).

fof(f7_sk,plain,
    ! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
    inference(skolemisation,[status(esa)],[f7_nnf]) ).

cnf(c7,plain,
    join(join(X0,X1),X2) = join(X0,join(X1,X2)),
    inference(cnf_transformation,[status(esa)],[f7_sk]) ).

cnf(t9,plain,
    join(join(X1,X2),X3) = join(X1,join(X2,X3)),
    inference(equality_encoding,[status(esa)],[c7]) ).

cnf(t710098,plain,
    join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
    inference(step,[status(thm)],[t9,t23]) ).

cnf(t26,plain,
    join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
    inference(orient,[status(thm)],[t710098]) ).

cnf(t30,plain,
    join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
    inference(cp,[status(thm)],[t26,t14]) ).

cnf(t710114,plain,
    join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
    inference(step,[status(thm)],[t30,t26]) ).

cnf(t710115,plain,
    join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
    inference(step,[status(thm)],[t710114,t23]) ).

cnf(t710116,plain,
    join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
    inference(step,[status(thm)],[t710115,t23]) ).

cnf(t170,plain,
    join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
    inference(orient,[status(thm)],[t710116]) ).

cnf(t710400,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X3,meet(join(zero,meet(X1,X2)),join(X1,meet(join(Y3,meet(X1,X2)),join(X1,zero))))),
    inference(step,[status(thm)],[t710399,t170]) ).

cnf(t710401,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X3,meet(join(zero,meet(X1,X2)),join(X1,meet(join(Y3,meet(X1,X2)),X1)))),
    inference(step,[status(thm)],[t710400,t102]) ).

cnf(t710402,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X3,meet(join(zero,meet(X1,X2)),join(X1,meet(X1,join(Y3,meet(X1,X2)))))),
    inference(step,[status(thm)],[t710401,t51]) ).

cnf(t710403,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X3,meet(join(zero,meet(X1,X2)),X1)),
    inference(step,[status(thm)],[t710402,t14]) ).

cnf(t710404,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X3,meet(X1,join(zero,meet(X1,X2)))),
    inference(step,[status(thm)],[t710403,t51]) ).

cnf(t710405,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
    inference(step,[status(thm)],[t710404,t218]) ).

cnf(t710406,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
    inference(step,[status(thm)],[t710405,t67]) ).

cnf(t710407,plain,
    meet(X3,meet(join(X1,Y3),join(zero,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
    inference(step,[status(thm)],[t710406,t67]) ).

cnf(t2120,plain,
    meet(X1,meet(join(X2,X3),join(zero,meet(X2,Y3)))) = meet(X2,meet(Y3,X1)),
    inference(orient,[status(thm)],[t710407]) ).

cnf(f8,axiom,
    join(X,complement(X)) = one,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).

fof(f8_nnf,plain,
    ! [X] : join(X,complement(X)) = one,
    inference(nnf_transformation,[status(thm)],[f8]) ).

fof(f8_sk,plain,
    ! [X] : join(X,complement(X)) = one,
    inference(skolemisation,[status(esa)],[f8_nnf]) ).

cnf(c8,plain,
    join(X0,complement(X0)) = one,
    inference(cnf_transformation,[status(esa)],[f8_sk]) ).

cnf(t2,plain,
    join(X1,complement(X1)) = one,
    inference(equality_encoding,[status(esa)],[c8]) ).

cnf(t46,plain,
    join(X1,complement(X1)) = one,
    inference(orient,[status(thm)],[t2]) ).

cnf(t49,plain,
    join(X1,join(complement(X1),X2)) = join(X2,one),
    inference(cp,[status(thm)],[t26,t46]) ).

cnf(t710110,plain,
    join(X1,join(X2,complement(X1))) = join(X2,one),
    inference(step,[status(thm)],[t49,t23]) ).

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(t13,plain,
    join(X1,X1) = X1,
    inference(orient,[status(thm)],[t0]) ).

cnf(t29,plain,
    join(X1,join(X2,X1)) = join(X2,X1),
    inference(cp,[status(thm)],[t26,t13]) ).

cnf(t710100,plain,
    join(X1,join(X1,X2)) = join(X2,X1),
    inference(step,[status(thm)],[t29,t26]) ).

cnf(t710101,plain,
    join(X1,join(X1,X2)) = join(X1,X2),
    inference(step,[status(thm)],[t710100,t23]) ).

cnf(t108,plain,
    join(X1,join(X1,X2)) = join(X1,X2),
    inference(orient,[status(thm)],[t710101]) ).

cnf(t111,plain,
    join(X1,complement(X1)) = join(X1,one),
    inference(cp,[status(thm)],[t108,t46]) ).

cnf(t710102,plain,
    one = join(X1,one),
    inference(step,[status(thm)],[t111,t46]) ).

cnf(t119,plain,
    join(X1,one) = one,
    inference(orient,[status(thm)],[t710102]) ).

cnf(t710111,plain,
    join(X1,join(X2,complement(X1))) = one,
    inference(step,[status(thm)],[t710110,t119]) ).

cnf(t154,plain,
    join(X1,join(X2,complement(X1))) = one,
    inference(orient,[status(thm)],[t710111]) ).

cnf(t160,plain,
    join(X1,join(join(X2,complement(X1)),X3)) = join(X3,one),
    inference(cp,[status(thm)],[t26,t154]) ).

cnf(t710120,plain,
    join(X1,join(X3,join(X2,complement(X1)))) = join(X3,one),
    inference(step,[status(thm)],[t160,t23]) ).

cnf(t710121,plain,
    join(X1,join(X2,join(complement(X1),X3))) = join(X3,one),
    inference(step,[status(thm)],[t710120,t26]) ).

cnf(t710122,plain,
    join(X1,join(X2,join(X3,complement(X1)))) = join(X3,one),
    inference(step,[status(thm)],[t710121,t23]) ).

cnf(t710123,plain,
    join(X1,join(X2,join(X3,complement(X1)))) = one,
    inference(step,[status(thm)],[t710122,t119]) ).

cnf(t196,plain,
    join(X1,join(X2,join(X3,complement(X1)))) = one,
    inference(orient,[status(thm)],[t710123]) ).

cnf(t2133,plain,
    meet(X1,meet(X2,X3)) = meet(X3,meet(one,join(zero,meet(X1,X2)))),
    inference(cp,[status(thm)],[t2120,t196]) ).

cnf(t1632,plain,
    meet(one,meet(X1,join(X2,X3))) = meet(one,meet(X1,join(X2,meet(one,join(X3,meet(X2,one)))))),
    inference(cp,[status(thm)],[t1618,t119]) ).

cnf(t710365,plain,
    meet(X1,meet(join(X2,X3),one)) = meet(one,meet(X1,join(X2,meet(one,join(X3,meet(X2,one)))))),
    inference(step,[status(thm)],[t1632,t67]) ).

cnf(t47,plain,
    X1 = meet(X1,one),
    inference(cp,[status(thm)],[t16,t46]) ).

cnf(t96,plain,
    meet(X1,one) = X1,
    inference(orient,[status(thm)],[t47]) ).

cnf(t710366,plain,
    meet(X1,join(X2,X3)) = meet(one,meet(X1,join(X2,meet(one,join(X3,meet(X2,one)))))),
    inference(step,[status(thm)],[t710365,t96]) ).

cnf(t710367,plain,
    meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,meet(one,join(X3,meet(X2,one)))),one)),
    inference(step,[status(thm)],[t710366,t67]) ).

cnf(t710368,plain,
    meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(one,join(X3,meet(X2,one))))),
    inference(step,[status(thm)],[t710367,t96]) ).

cnf(t710369,plain,
    meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(one,join(X3,X2)))),
    inference(step,[status(thm)],[t710368,t96]) ).

cnf(t710370,plain,
    meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(one,join(X2,X3)))),
    inference(step,[status(thm)],[t710369,t23]) ).

cnf(t1708,plain,
    meet(X1,join(X2,meet(one,join(X2,X3)))) = meet(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t710370]) ).

cnf(t1709,plain,
    meet(join(X1,meet(one,join(X1,X2))),join(X1,X2)) = join(X1,meet(one,join(X1,X2))),
    inference(cp,[status(thm)],[t1708,t15]) ).

cnf(t710371,plain,
    meet(join(X1,X2),join(X1,meet(one,join(X1,X2)))) = join(X1,meet(one,join(X1,X2))),
    inference(step,[status(thm)],[t1709,t51]) ).

cnf(t710372,plain,
    meet(join(X1,X2),join(X1,X2)) = join(X1,meet(one,join(X1,X2))),
    inference(step,[status(thm)],[t710371,t1708]) ).

cnf(t710373,plain,
    join(X1,X2) = join(X1,meet(one,join(X1,X2))),
    inference(step,[status(thm)],[t710372,t15]) ).

cnf(t1755,plain,
    join(X1,meet(one,join(X1,X2))) = join(X1,X2),
    inference(orient,[status(thm)],[t710373]) ).

cnf(t1781,plain,
    meet(one,meet(join(X1,X2),X3)) = meet(one,meet(join(X1,X2),meet(X3,join(X1,X2)))),
    inference(cp,[status(thm)],[t830,t1755]) ).

cnf(t710377,plain,
    meet(X3,meet(one,join(X1,X2))) = meet(one,meet(join(X1,X2),meet(X3,join(X1,X2)))),
    inference(step,[status(thm)],[t1781,t67]) ).

cnf(t710378,plain,
    meet(X3,meet(one,join(X1,X2))) = meet(one,meet(X3,meet(join(X1,X2),join(X1,X2)))),
    inference(step,[status(thm)],[t710377,t67]) ).

cnf(t710379,plain,
    meet(X3,meet(one,join(X1,X2))) = meet(X3,meet(meet(join(X1,X2),join(X1,X2)),one)),
    inference(step,[status(thm)],[t710378,t67]) ).

cnf(t710380,plain,
    meet(X3,meet(one,join(X1,X2))) = meet(X3,meet(join(X1,X2),join(X1,X2))),
    inference(step,[status(thm)],[t710379,t96]) ).

cnf(t710381,plain,
    meet(X3,meet(one,join(X1,X2))) = meet(X3,join(X1,X2)),
    inference(step,[status(thm)],[t710380,t15]) ).

cnf(t1834,plain,
    meet(X1,meet(one,join(X2,X3))) = meet(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t710381]) ).

cnf(t710410,plain,
    meet(X1,meet(X2,X3)) = meet(X3,join(zero,meet(X1,X2))),
    inference(step,[status(thm)],[t2133,t1834]) ).

cnf(t2264,plain,
    meet(X1,join(zero,meet(X2,X3))) = meet(X2,meet(X3,X1)),
    inference(orient,[status(thm)],[t710410]) ).

cnf(t2266,plain,
    meet(X1,meet(X2,join(zero,meet(X1,X2)))) = join(zero,meet(X1,X2)),
    inference(cp,[status(thm)],[t2264,t15]) ).

cnf(t710416,plain,
    meet(X1,meet(X2,X2)) = join(zero,meet(X1,X2)),
    inference(step,[status(thm)],[t2266,t296]) ).

cnf(t710417,plain,
    meet(X1,X2) = join(zero,meet(X1,X2)),
    inference(step,[status(thm)],[t710416,t15]) ).

cnf(t2368,plain,
    join(zero,meet(X1,X2)) = meet(X1,X2),
    inference(orient,[status(thm)],[t710417]) ).

cnf(t2396,plain,
    meet(X1,join(X2,zero)) = meet(X1,join(X2,meet(join(X1,X2),meet(X1,X2)))),
    inference(cp,[status(thm)],[t54,t2368]) ).

cnf(t710424,plain,
    meet(X1,X2) = meet(X1,join(X2,meet(join(X1,X2),meet(X1,X2)))),
    inference(step,[status(thm)],[t2396,t102]) ).

cnf(t710425,plain,
    meet(X1,X2) = meet(X1,join(X2,meet(X2,meet(join(X1,X2),X1)))),
    inference(step,[status(thm)],[t710424,t67]) ).

cnf(t710426,plain,
    meet(X1,X2) = meet(X1,join(X2,meet(X1,meet(X2,join(X1,X2))))),
    inference(step,[status(thm)],[t710425,t67]) ).

cnf(t710427,plain,
    meet(X1,X2) = meet(X1,join(X2,meet(X1,X2))),
    inference(step,[status(thm)],[t710426,t183]) ).

cnf(t2566,plain,
    meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710427]) ).

cnf(t2582,plain,
    meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
    inference(cp,[status(thm)],[t2566,t183]) ).

cnf(t710431,plain,
    meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
    inference(step,[status(thm)],[t2582,t183]) ).

cnf(t710432,plain,
    meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
    inference(step,[status(thm)],[t710431,t23]) ).

cnf(t2680,plain,
    meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710432]) ).

cnf(t2746,plain,
    meet(X1,meet(join(X2,X3),meet(Y3,X2))) = meet(X1,meet(join(X2,X3),meet(Y3,meet(X2,X1)))),
    inference(cp,[status(thm)],[t1122,t2680]) ).

cnf(t710447,plain,
    meet(X1,meet(X2,meet(join(X2,X3),Y3))) = meet(X1,meet(join(X2,X3),meet(Y3,meet(X2,X1)))),
    inference(step,[status(thm)],[t2746,t67]) ).

cnf(t710448,plain,
    meet(X1,meet(X2,meet(Y3,join(X2,X3)))) = meet(X1,meet(join(X2,X3),meet(Y3,meet(X2,X1)))),
    inference(step,[status(thm)],[t710447,t51]) ).

cnf(t710449,plain,
    meet(X1,meet(X2,Y3)) = meet(X1,meet(join(X2,X3),meet(Y3,meet(X2,X1)))),
    inference(step,[status(thm)],[t710448,t183]) ).

cnf(t710450,plain,
    meet(X1,meet(X2,Y3)) = meet(X1,meet(meet(X2,X1),meet(join(X2,X3),Y3))),
    inference(step,[status(thm)],[t710449,t67]) ).

cnf(t710451,plain,
    meet(X1,meet(X2,Y3)) = meet(X1,meet(Y3,meet(meet(X2,X1),join(X2,X3)))),
    inference(step,[status(thm)],[t710450,t67]) ).

cnf(t710452,plain,
    meet(X1,meet(X2,Y3)) = meet(X1,meet(Y3,meet(meet(X1,X2),join(X2,X3)))),
    inference(step,[status(thm)],[t710451,t51]) ).

cnf(t3053,plain,
    meet(X1,meet(X2,meet(meet(X1,X3),join(X3,Y3)))) = meet(X1,meet(X3,X2)),
    inference(orient,[status(thm)],[t710452]) ).

cnf(t3066,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)],[t3053,t15]) ).

cnf(t710453,plain,
    meet(X1,meet(X2,X2)) = meet(X1,meet(meet(X1,X2),join(X2,X3))),
    inference(step,[status(thm)],[t3066,t3053]) ).

cnf(t710454,plain,
    meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(X2,X3))),
    inference(step,[status(thm)],[t710453,t15]) ).

cnf(t3156,plain,
    meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710454]) ).

cnf(t3180,plain,
    meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(meet(X1,X2),join(meet(X2,join(X1,X3)),Y3))),
    inference(cp,[status(thm)],[t3156,t183]) ).

cnf(t710460,plain,
    meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(meet(X2,join(X1,X3)),Y3))),
    inference(step,[status(thm)],[t3180,t183]) ).

cnf(t710461,plain,
    meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(Y3,meet(X2,join(X1,X3))))),
    inference(step,[status(thm)],[t710460,t23]) ).

cnf(t3329,plain,
    meet(X1,meet(meet(X1,X2),join(X3,meet(X2,join(X1,Y3))))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710461]) ).

cnf(t771,plain,
    meet(X1,meet(X1,X2)) = meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
    inference(cp,[status(thm)],[t754,t125]) ).

cnf(t710270,plain,
    meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
    inference(step,[status(thm)],[t771,t125]) ).

cnf(t792,plain,
    meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710270]) ).

cnf(t1837,plain,
    meet(meet(one,join(X1,X2)),join(X1,X2)) = meet(one,join(X1,X2)),
    inference(cp,[status(thm)],[t1834,t15]) ).

cnf(t710382,plain,
    meet(join(X1,X2),meet(one,join(X1,X2))) = meet(one,join(X1,X2)),
    inference(step,[status(thm)],[t1837,t51]) ).

cnf(t710383,plain,
    meet(join(X1,X2),join(X1,X2)) = meet(one,join(X1,X2)),
    inference(step,[status(thm)],[t710382,t1834]) ).

cnf(t710384,plain,
    join(X1,X2) = meet(one,join(X1,X2)),
    inference(step,[status(thm)],[t710383,t15]) ).

cnf(t1874,plain,
    meet(one,join(X1,X2)) = join(X1,X2),
    inference(orient,[status(thm)],[t710384]) ).

cnf(t1896,plain,
    meet(one,join(X1,X2)) = meet(one,meet(meet(one,join(X1,X2)),join(X3,join(X1,X2)))),
    inference(cp,[status(thm)],[t792,t1874]) ).

cnf(t710386,plain,
    join(X1,X2) = meet(one,meet(meet(one,join(X1,X2)),join(X3,join(X1,X2)))),
    inference(step,[status(thm)],[t1896,t1874]) ).

cnf(t710387,plain,
    join(X1,X2) = meet(one,meet(join(X1,X2),join(X3,join(X1,X2)))),
    inference(step,[status(thm)],[t710386,t1874]) ).

cnf(t710388,plain,
    join(X1,X2) = meet(one,meet(join(X1,X2),join(X2,join(X3,X1)))),
    inference(step,[status(thm)],[t710387,t26]) ).

cnf(t710389,plain,
    join(X1,X2) = meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))),
    inference(step,[status(thm)],[t710388,t26]) ).

cnf(t1930,plain,
    meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))) = join(X1,X2),
    inference(orient,[status(thm)],[t710389]) ).

cnf(t1995,plain,
    meet(meet(join(X1,X2),join(X1,join(X2,X3))),meet(Y3,one)) = meet(Y3,join(X1,X2)),
    inference(cp,[status(thm)],[t67,t1930]) ).

cnf(t710392,plain,
    meet(meet(join(X1,X2),join(X1,join(X2,X3))),Y3) = meet(Y3,join(X1,X2)),
    inference(step,[status(thm)],[t1995,t96]) ).

cnf(t710393,plain,
    meet(Y3,meet(join(X1,X2),join(X1,join(X2,X3)))) = meet(Y3,join(X1,X2)),
    inference(step,[status(thm)],[t710392,t51]) ).

cnf(t2011,plain,
    meet(X1,meet(join(X2,X3),join(X2,join(X3,Y3)))) = meet(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t710393]) ).

cnf(t2012,plain,
    meet(join(X1,X2),join(X1,X2)) = meet(join(X1,X2),join(X1,join(X2,X3))),
    inference(cp,[status(thm)],[t2011,t125]) ).

cnf(t710394,plain,
    join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
    inference(step,[status(thm)],[t2012,t15]) ).

cnf(t2060,plain,
    meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
    inference(orient,[status(thm)],[t710394]) ).

cnf(t2382,plain,
    join(zero,meet(X1,X2)) = meet(meet(X1,X2),join(zero,join(meet(X1,X2),X3))),
    inference(cp,[status(thm)],[t2060,t2368]) ).

cnf(t710420,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(zero,join(meet(X1,X2),X3))),
    inference(step,[status(thm)],[t2382,t2368]) ).

cnf(t710421,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(X3,join(zero,meet(X1,X2)))),
    inference(step,[status(thm)],[t710420,t26]) ).

cnf(t710422,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
    inference(step,[status(thm)],[t710421,t2368]) ).

cnf(t2521,plain,
    meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710422]) ).

cnf(t3185,plain,
    meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3))),
    inference(cp,[status(thm)],[t3156,t2521]) ).

cnf(t710455,plain,
    meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3))),
    inference(step,[status(thm)],[t3185,t2521]) ).

cnf(t710456,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3)),
    inference(step,[status(thm)],[t710455,t125]) ).

cnf(t710457,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(Y3,join(X3,meet(X1,X2)))),
    inference(step,[status(thm)],[t710456,t23]) ).

cnf(t710458,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),Y3))),
    inference(step,[status(thm)],[t710457,t26]) ).

cnf(t710459,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))),
    inference(step,[status(thm)],[t710458,t23]) ).

cnf(t3224,plain,
    meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710459]) ).

cnf(t3233,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
    inference(cp,[status(thm)],[t3224,t170]) ).

cnf(t3279,plain,
    meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
    inference(orient,[status(thm)],[t3233]) ).

cnf(t3359,plain,
    meet(meet(X1,X2),join(X1,X3)) = meet(meet(X1,X2),meet(meet(X1,X2),join(Y3,meet(join(X1,X3),join(meet(X1,X2),Y4))))),
    inference(cp,[status(thm)],[t3329,t3279]) ).

cnf(t710518,plain,
    meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(Y3,meet(join(X1,X3),join(meet(X1,X2),Y4))))),
    inference(step,[status(thm)],[t3359,t3279]) ).

cnf(t710519,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(Y3,meet(join(X1,X3),join(meet(X1,X2),Y4)))),
    inference(step,[status(thm)],[t710518,t125]) ).

cnf(t710520,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(Y3,meet(join(X1,X3),join(Y4,meet(X1,X2))))),
    inference(step,[status(thm)],[t710519,t23]) ).

cnf(t5403,plain,
    meet(meet(X1,X2),join(X3,meet(join(X1,Y3),join(Y4,meet(X1,X2))))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710520]) ).

cnf(t5428,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,join(Y3,meet(X1,X2))))),
    inference(cp,[status(thm)],[t5403,t13]) ).

cnf(t5522,plain,
    meet(meet(X1,X2),join(X3,meet(X1,join(Y3,meet(X1,X2))))) = meet(X1,X2),
    inference(orient,[status(thm)],[t5428]) ).

cnf(t5544,plain,
    meet(meet(X1,X2),X3) = meet(meet(meet(X1,X2),X3),join(Y3,meet(X1,X2))),
    inference(cp,[status(thm)],[t5522,t3279]) ).

cnf(t710521,plain,
    meet(X3,meet(X1,X2)) = meet(meet(meet(X1,X2),X3),join(Y3,meet(X1,X2))),
    inference(step,[status(thm)],[t5544,t51]) ).

cnf(t710522,plain,
    meet(X2,meet(X3,X1)) = meet(meet(meet(X1,X2),X3),join(Y3,meet(X1,X2))),
    inference(step,[status(thm)],[t710521,t67]) ).

cnf(t710523,plain,
    meet(X1,meet(X2,X3)) = meet(meet(meet(X1,X2),X3),join(Y3,meet(X1,X2))),
    inference(step,[status(thm)],[t710522,t67]) ).

cnf(t710524,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X3,meet(X1,X2)),join(Y3,meet(X1,X2))),
    inference(step,[status(thm)],[t710523,t51]) ).

cnf(t710525,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X2,meet(X3,X1)),join(Y3,meet(X1,X2))),
    inference(step,[status(thm)],[t710524,t67]) ).

cnf(t710526,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X2))),
    inference(step,[status(thm)],[t710525,t67]) ).

cnf(t5615,plain,
    meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X2))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t710526]) ).

cnf(t2750,plain,
    meet(X1,meet(join(meet(X1,X2),meet(X2,join(X1,X3))),Y3)) = meet(Y3,meet(X1,X2)),
    inference(cp,[status(thm)],[t67,t2680]) ).

cnf(t710479,plain,
    meet(X1,meet(Y3,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(Y3,meet(X1,X2)),
    inference(step,[status(thm)],[t2750,t51]) ).

cnf(t710480,plain,
    meet(X1,meet(Y3,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X2,meet(Y3,X1)),
    inference(step,[status(thm)],[t710479,t67]) ).

cnf(t710481,plain,
    meet(X1,meet(Y3,join(meet(X1,X2),meet(X2,join(X1,X3))))) = meet(X1,meet(X2,Y3)),
    inference(step,[status(thm)],[t710480,t67]) ).

cnf(t3827,plain,
    meet(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,Y3))))) = meet(X1,meet(X3,X2)),
    inference(orient,[status(thm)],[t710481]) ).

cnf(t5617,plain,
    meet(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,Y3))))) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
    inference(cp,[status(thm)],[t5615,t3827]) ).

cnf(t710538,plain,
    meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
    inference(step,[status(thm)],[t5617,t3827]) ).

cnf(t6132,plain,
    meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X3))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t710538]) ).

cnf(t6196,plain,
    meet(X1,meet(meet(X2,X3),join(X2,Y3))) = meet(meet(X1,meet(X2,X3)),join(Y4,meet(X1,join(X2,Y3)))),
    inference(cp,[status(thm)],[t6132,t3279]) ).

cnf(t710590,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,meet(X1,join(X2,Y3)))),
    inference(step,[status(thm)],[t6196,t3279]) ).

cnf(t7968,plain,
    meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,join(X2,Y4)))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t710590]) ).

cnf(t8013,plain,
    meet(meet(X1,X2),meet(X3,Y3)) = meet(meet(meet(X1,X2),meet(X3,Y3)),join(Y4,meet(X1,X2))),
    inference(cp,[status(thm)],[t7968,t2521]) ).

cnf(t710698,plain,
    meet(Y3,meet(meet(X1,X2),X3)) = meet(meet(meet(X1,X2),meet(X3,Y3)),join(Y4,meet(X1,X2))),
    inference(step,[status(thm)],[t8013,t67]) ).

cnf(t710699,plain,
    meet(X3,meet(Y3,meet(X1,X2))) = meet(meet(meet(X1,X2),meet(X3,Y3)),join(Y4,meet(X1,X2))),
    inference(step,[status(thm)],[t710698,t67]) ).

cnf(t710700,plain,
    meet(X3,meet(X2,meet(Y3,X1))) = meet(meet(meet(X1,X2),meet(X3,Y3)),join(Y4,meet(X1,X2))),
    inference(step,[status(thm)],[t710699,t67]) ).

cnf(t710701,plain,
    meet(X3,meet(X1,meet(X2,Y3))) = meet(meet(meet(X1,X2),meet(X3,Y3)),join(Y4,meet(X1,X2))),
    inference(step,[status(thm)],[t710700,t67]) ).

cnf(t710702,plain,
    meet(X1,meet(meet(X2,Y3),X3)) = meet(meet(meet(X1,X2),meet(X3,Y3)),join(Y4,meet(X1,X2))),
    inference(step,[status(thm)],[t710701,t67]) ).

cnf(t710703,plain,
    meet(X1,meet(X3,meet(X2,Y3))) = meet(meet(meet(X1,X2),meet(X3,Y3)),join(Y4,meet(X1,X2))),
    inference(step,[status(thm)],[t710702,t51]) ).

cnf(t710704,plain,
    meet(X1,meet(X2,meet(Y3,X3))) = meet(meet(meet(X1,X2),meet(X3,Y3)),join(Y4,meet(X1,X2))),
    inference(step,[status(thm)],[t710703,t67]) ).

cnf(t710705,plain,
    meet(X1,meet(X2,meet(X3,Y3))) = meet(meet(meet(X1,X2),meet(X3,Y3)),join(Y4,meet(X1,X2))),
    inference(step,[status(thm)],[t710704,t51]) ).

cnf(t710706,plain,
    meet(X1,meet(X2,meet(X3,Y3))) = meet(join(Y4,meet(X1,X2)),meet(meet(X1,X2),meet(X3,Y3))),
    inference(step,[status(thm)],[t710705,t51]) ).

cnf(t710707,plain,
    meet(X1,meet(X2,meet(X3,Y3))) = meet(meet(X3,Y3),meet(join(Y4,meet(X1,X2)),meet(X1,X2))),
    inference(step,[status(thm)],[t710706,t67]) ).

cnf(t710708,plain,
    meet(X1,meet(X2,meet(X3,Y3))) = meet(meet(X1,X2),meet(meet(X3,Y3),join(Y4,meet(X1,X2)))),
    inference(step,[status(thm)],[t710707,t67]) ).

cnf(t13227,plain,
    meet(meet(X1,X2),meet(meet(X3,Y3),join(Y4,meet(X1,X2)))) = meet(X1,meet(X2,meet(X3,Y3))),
    inference(orient,[status(thm)],[t710708]) ).

cnf(t13482,plain,
    meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,meet(X3,Y3)))),
    inference(cp,[status(thm)],[t14,t13227]) ).

cnf(t13596,plain,
    join(meet(X1,X2),meet(X1,meet(X2,meet(X3,Y3)))) = meet(X1,X2),
    inference(orient,[status(thm)],[t13482]) ).

cnf(t5700,plain,
    meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X2))) = meet(meet(X1,meet(X2,X3)),meet(meet(X1,meet(X2,X3)),join(join(Y3,meet(X1,X2)),Y4))),
    inference(cp,[status(thm)],[t3156,t5615]) ).

cnf(t710572,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),meet(meet(X1,meet(X2,X3)),join(join(Y3,meet(X1,X2)),Y4))),
    inference(step,[status(thm)],[t5700,t5615]) ).

cnf(t710573,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(join(Y3,meet(X1,X2)),Y4)),
    inference(step,[status(thm)],[t710572,t125]) ).

cnf(t710574,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,join(Y3,meet(X1,X2)))),
    inference(step,[status(thm)],[t710573,t23]) ).

cnf(t710575,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y3,join(meet(X1,X2),Y4))),
    inference(step,[status(thm)],[t710574,t26]) ).

cnf(t710576,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y3,join(Y4,meet(X1,X2)))),
    inference(step,[status(thm)],[t710575,t23]) ).

cnf(t7559,plain,
    meet(meet(X1,meet(X2,X3)),join(Y3,join(Y4,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t710576]) ).

cnf(t7560,plain,
    meet(X1,meet(X2,X3)) = meet(join(Y3,join(Y4,meet(X1,X2))),meet(X1,meet(X2,X3))),
    inference(cp,[status(thm)],[t7559,t51]) ).

cnf(t710597,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X2,X3),meet(join(Y3,join(Y4,meet(X1,X2))),X1)),
    inference(step,[status(thm)],[t7560,t67]) ).

cnf(t710598,plain,
    meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(Y3,join(Y4,meet(X1,X2))))),
    inference(step,[status(thm)],[t710597,t67]) ).

cnf(t8465,plain,
    meet(X1,meet(meet(X2,X3),join(Y3,join(Y4,meet(X1,X2))))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t710598]) ).

cnf(t8469,plain,
    meet(X1,meet(X2,X3)) = meet(X1,meet(join(Y3,join(Y4,meet(X1,X2))),meet(X2,X3))),
    inference(cp,[status(thm)],[t8465,t51]) ).

cnf(t710667,plain,
    meet(X1,meet(X2,X3)) = meet(X1,meet(X3,meet(join(Y3,join(Y4,meet(X1,X2))),X2))),
    inference(step,[status(thm)],[t8469,t67]) ).

cnf(t710668,plain,
    meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(X3,join(Y3,join(Y4,meet(X1,X2)))))),
    inference(step,[status(thm)],[t710667,t67]) ).

cnf(t11527,plain,
    meet(X1,meet(X2,meet(X3,join(Y3,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t710668]) ).

cnf(t13669,plain,
    meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
    inference(cp,[status(thm)],[t13596,t11527]) ).

cnf(t13816,plain,
    join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
    inference(orient,[status(thm)],[t13669]) ).

cnf(t13885,plain,
    meet(one,join(X1,X2)) = join(join(X1,X2),meet(one,meet(join(X1,X2),X3))),
    inference(cp,[status(thm)],[t13816,t1874]) ).

cnf(t710709,plain,
    join(X1,X2) = join(join(X1,X2),meet(one,meet(join(X1,X2),X3))),
    inference(step,[status(thm)],[t13885,t1874]) ).

cnf(t710710,plain,
    join(X1,X2) = join(join(X1,X2),meet(X3,meet(one,join(X1,X2)))),
    inference(step,[status(thm)],[t710709,t67]) ).

cnf(t710711,plain,
    join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,X2))),
    inference(step,[status(thm)],[t710710,t1834]) ).

cnf(t14008,plain,
    join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,X2),
    inference(orient,[status(thm)],[t710711]) ).

cnf(t3356,plain,
    meet(X1,join(X1,X2)) = meet(X1,meet(X1,join(X3,meet(join(X1,X2),join(X1,Y3))))),
    inference(cp,[status(thm)],[t3329,t16]) ).

cnf(t710462,plain,
    X1 = meet(X1,meet(X1,join(X3,meet(join(X1,X2),join(X1,Y3))))),
    inference(step,[status(thm)],[t3356,t16]) ).

cnf(t710463,plain,
    X1 = meet(X1,join(X3,meet(join(X1,X2),join(X1,Y3)))),
    inference(step,[status(thm)],[t710462,t125]) ).

cnf(t3425,plain,
    meet(X1,join(X2,meet(join(X1,X3),join(X1,Y3)))) = X1,
    inference(orient,[status(thm)],[t710463]) ).

cnf(t14028,plain,
    join(X1,meet(join(X2,X3),join(X2,Y3))) = join(join(X1,meet(join(X2,X3),join(X2,Y3))),X2),
    inference(cp,[status(thm)],[t14008,t3425]) ).

cnf(t710743,plain,
    join(X1,meet(join(X2,X3),join(X2,Y3))) = join(X2,join(X1,meet(join(X2,X3),join(X2,Y3)))),
    inference(step,[status(thm)],[t14028,t23]) ).

cnf(t710744,plain,
    join(X1,meet(join(X2,X3),join(X2,Y3))) = join(X1,join(meet(join(X2,X3),join(X2,Y3)),X2)),
    inference(step,[status(thm)],[t710743,t26]) ).

cnf(t710745,plain,
    join(X1,meet(join(X2,X3),join(X2,Y3))) = join(X1,join(X2,meet(join(X2,X3),join(X2,Y3)))),
    inference(step,[status(thm)],[t710744,t23]) ).

cnf(t16506,plain,
    join(X1,join(X2,meet(join(X2,X3),join(X2,Y3)))) = join(X1,meet(join(X2,X3),join(X2,Y3))),
    inference(orient,[status(thm)],[t710745]) ).

cnf(t7971,plain,
    meet(X1,meet(X2,join(meet(X1,X3),meet(X3,join(X1,Y3))))) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,join(X2,Y5)))),
    inference(cp,[status(thm)],[t7968,t3827]) ).

cnf(t710642,plain,
    meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,join(X2,Y5)))),
    inference(step,[status(thm)],[t7971,t3827]) ).

cnf(t9538,plain,
    meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,join(X3,Y4)))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t710642]) ).

cnf(t9659,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),meet(X1,join(X3,Y3))),
    inference(cp,[status(thm)],[t9538,t13]) ).

cnf(t710643,plain,
    meet(X1,meet(X2,X3)) = meet(join(X3,Y3),meet(meet(X1,meet(X2,X3)),X1)),
    inference(step,[status(thm)],[t9659,t67]) ).

cnf(t710644,plain,
    meet(X1,meet(X2,X3)) = meet(X1,meet(join(X3,Y3),meet(X1,meet(X2,X3)))),
    inference(step,[status(thm)],[t710643,t67]) ).

cnf(t710645,plain,
    meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),meet(join(X3,Y3),X1))),
    inference(step,[status(thm)],[t710644,t67]) ).

cnf(t710646,plain,
    meet(X1,meet(X2,X3)) = meet(X1,meet(X1,meet(meet(X2,X3),join(X3,Y3)))),
    inference(step,[status(thm)],[t710645,t67]) ).

cnf(t710647,plain,
    meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X3,Y3))),
    inference(step,[status(thm)],[t710646,t125]) ).

cnf(t9788,plain,
    meet(X1,meet(meet(X2,X3),join(X3,Y3))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t710647]) ).

cnf(t9791,plain,
    meet(meet(X1,X2),meet(X1,X2)) = meet(meet(X1,X2),join(X2,X3)),
    inference(cp,[status(thm)],[t9788,t125]) ).

cnf(t710650,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
    inference(step,[status(thm)],[t9791,t15]) ).

cnf(t9929,plain,
    meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
    inference(orient,[status(thm)],[t710650]) ).

cnf(t9974,plain,
    meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),Y3)),
    inference(cp,[status(thm)],[t9929,t183]) ).

cnf(t710651,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),Y3)),
    inference(step,[status(thm)],[t9974,t183]) ).

cnf(t710652,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(Y3,meet(X2,join(X1,X3)))),
    inference(step,[status(thm)],[t710651,t23]) ).

cnf(t10080,plain,
    meet(meet(X1,X2),join(X3,meet(X2,join(X1,Y3)))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710652]) ).

cnf(t10173,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y3,meet(X2,X3))),
    inference(cp,[status(thm)],[t10080,t2521]) ).

cnf(t10270,plain,
    meet(meet(X1,meet(X2,X3)),join(Y3,meet(X2,X3))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t10173]) ).

cnf(t10316,plain,
    meet(X1,meet(join(X2,X3),join(X2,join(X3,Y3)))) = meet(meet(X1,join(X2,X3)),join(Y4,meet(join(X2,X3),join(X2,join(X3,Y3))))),
    inference(cp,[status(thm)],[t10270,t2060]) ).

cnf(t710653,plain,
    meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,meet(join(X2,X3),join(X2,join(X3,Y3))))),
    inference(step,[status(thm)],[t10316,t2011]) ).

cnf(t710654,plain,
    meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,join(X2,X3))),
    inference(step,[status(thm)],[t710653,t2060]) ).

cnf(t710655,plain,
    meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X3,join(Y4,X2))),
    inference(step,[status(thm)],[t710654,t26]) ).

cnf(t710656,plain,
    meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,join(X3,Y4))),
    inference(step,[status(thm)],[t710655,t26]) ).

cnf(t10412,plain,
    meet(meet(X1,join(X2,X3)),join(X2,join(X3,Y3))) = meet(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t710656]) ).

cnf(t14036,plain,
    join(X1,join(X2,X3)) = join(join(X1,join(X2,X3)),meet(Y3,join(X1,X2))),
    inference(cp,[status(thm)],[t14008,t10412]) ).

cnf(t710712,plain,
    join(X1,join(X2,X3)) = join(meet(Y3,join(X1,X2)),join(X1,join(X2,X3))),
    inference(step,[status(thm)],[t14036,t23]) ).

cnf(t710713,plain,
    join(X1,join(X2,X3)) = join(join(X2,X3),join(meet(Y3,join(X1,X2)),X1)),
    inference(step,[status(thm)],[t710712,t26]) ).

cnf(t710714,plain,
    join(X1,join(X2,X3)) = join(X1,join(join(X2,X3),meet(Y3,join(X1,X2)))),
    inference(step,[status(thm)],[t710713,t26]) ).

cnf(t14173,plain,
    join(X1,join(join(X2,X3),meet(Y3,join(X1,X2)))) = join(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t710714]) ).

cnf(t14190,plain,
    join(X1,join(zero,meet(X2,X3))) = join(X1,join(meet(X2,X3),meet(Y3,join(X1,zero)))),
    inference(cp,[status(thm)],[t14173,t2368]) ).

cnf(t710718,plain,
    join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(Y3,join(X1,zero)))),
    inference(step,[status(thm)],[t14190,t2368]) ).

cnf(t710719,plain,
    join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(Y3,X1))),
    inference(step,[status(thm)],[t710718,t102]) ).

cnf(t710720,plain,
    join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X1,Y3))),
    inference(step,[status(thm)],[t710719,t51]) ).

cnf(t710721,plain,
    join(X1,meet(X2,X3)) = join(X1,join(meet(X1,Y3),meet(X2,X3))),
    inference(step,[status(thm)],[t710720,t23]) ).

cnf(t14620,plain,
    join(X1,join(meet(X1,X2),meet(X3,Y3))) = join(X1,meet(X3,Y3)),
    inference(orient,[status(thm)],[t710721]) ).

cnf(t14664,plain,
    join(X1,join(join(meet(X1,X2),meet(X3,Y3)),Y4)) = join(Y4,join(X1,meet(X3,Y3))),
    inference(cp,[status(thm)],[t26,t14620]) ).

cnf(t710732,plain,
    join(X1,join(Y4,join(meet(X1,X2),meet(X3,Y3)))) = join(Y4,join(X1,meet(X3,Y3))),
    inference(step,[status(thm)],[t14664,t23]) ).

cnf(t710733,plain,
    join(X1,join(Y4,join(meet(X1,X2),meet(X3,Y3)))) = join(X1,join(meet(X3,Y3),Y4)),
    inference(step,[status(thm)],[t710732,t26]) ).

cnf(t710734,plain,
    join(X1,join(Y4,join(meet(X1,X2),meet(X3,Y3)))) = join(X1,join(Y4,meet(X3,Y3))),
    inference(step,[status(thm)],[t710733,t23]) ).

cnf(t15432,plain,
    join(X1,join(X2,join(meet(X1,X3),meet(Y3,Y4)))) = join(X1,join(X2,meet(Y3,Y4))),
    inference(orient,[status(thm)],[t710734]) ).

cnf(t14177,plain,
    join(X1,join(X2,X2)) = join(X1,join(X2,meet(X3,join(X1,X2)))),
    inference(cp,[status(thm)],[t14173,t13]) ).

cnf(t710717,plain,
    join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
    inference(step,[status(thm)],[t14177,t13]) ).

cnf(t14531,plain,
    join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
    inference(orient,[status(thm)],[t710717]) ).

cnf(t15434,plain,
    join(X1,join(X2,meet(X3,join(X2,meet(X1,Y3))))) = join(X1,join(X2,meet(X1,Y3))),
    inference(cp,[status(thm)],[t15432,t14531]) ).

cnf(t710735,plain,
    join(X1,join(X2,meet(X3,join(X2,meet(X1,Y3))))) = join(X1,X2),
    inference(step,[status(thm)],[t15434,t170]) ).

cnf(t15520,plain,
    join(X1,join(X2,meet(X3,join(X2,meet(X1,Y3))))) = join(X1,X2),
    inference(orient,[status(thm)],[t710735]) ).

cnf(t16507,plain,
    join(X1,meet(join(X2,X3),join(X2,meet(X1,Y3)))) = join(X1,X2),
    inference(cp,[status(thm)],[t16506,t15520]) ).

cnf(t16572,plain,
    join(X1,meet(join(X2,X3),join(X2,meet(X1,Y3)))) = join(X1,X2),
    inference(orient,[status(thm)],[t16507]) ).

cnf(f10,axiom,
    ( complement(X) = Y
    | join(X,Y) != one
    | meet(X,Y) != zero ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).

fof(f10_nnf,plain,
    ! [X,Y] :
      ( complement(X) = Y
      | join(X,Y) != one
      | meet(X,Y) != zero ),
    inference(nnf_transformation,[status(thm)],[f10]) ).

fof(f10_sk,plain,
    ! [X,Y] :
      ( complement(X) = Y
      | join(X,Y) != one
      | meet(X,Y) != zero ),
    inference(skolemisation,[status(esa)],[f10_nnf]) ).

cnf(c10,plain,
    ( complement(X0) = X1
    | join(X0,X1) != one
    | meet(X0,X1) != zero ),
    inference(cnf_transformation,[status(esa)],[f10_sk]) ).

cnf(t11,plain,
    ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
    inference(equality_encoding,[status(esa)],[c10]) ).

cnf(t18,plain,
    ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
    inference(orient,[status(thm)],[t11]) ).

cnf(t16539,plain,
    join(X1,X2) = meet(join(X1,X2),join(X1,meet(join(X2,X3),join(X2,Y3)))),
    inference(cp,[status(thm)],[t2060,t16506]) ).

cnf(t18258,plain,
    meet(join(X1,X2),join(X1,meet(join(X2,X3),join(X2,Y3)))) = join(X1,X2),
    inference(orient,[status(thm)],[t16539]) ).

cnf(t18287,plain,
    join(X1,complement(X1)) = meet(one,join(X1,meet(join(complement(X1),X2),join(complement(X1),X3)))),
    inference(cp,[status(thm)],[t18258,t46]) ).

cnf(t710775,plain,
    one = meet(one,join(X1,meet(join(complement(X1),X2),join(complement(X1),X3)))),
    inference(step,[status(thm)],[t18287,t46]) ).

cnf(t710776,plain,
    one = join(X1,meet(join(complement(X1),X2),join(complement(X1),X3))),
    inference(step,[status(thm)],[t710775,t1874]) ).

cnf(t710777,plain,
    one = join(X1,meet(join(X2,complement(X1)),join(complement(X1),X3))),
    inference(step,[status(thm)],[t710776,t23]) ).

cnf(t710778,plain,
    one = join(X1,meet(join(X2,complement(X1)),join(X3,complement(X1)))),
    inference(step,[status(thm)],[t710777,t23]) ).

cnf(t18473,plain,
    join(X1,meet(join(X2,complement(X1)),join(X3,complement(X1)))) = one,
    inference(orient,[status(thm)],[t710778]) ).

cnf(t18475,plain,
    one = join(X1,meet(complement(X1),join(X2,complement(X1)))),
    inference(cp,[status(thm)],[t18473,t13]) ).

cnf(t18677,plain,
    join(X1,meet(complement(X1),join(X2,complement(X1)))) = one,
    inference(orient,[status(thm)],[t18475]) ).

cnf(t18680,plain,
    meet(complement(X1),join(X2,complement(X1))) = ifeq(meet(X1,meet(complement(X1),join(X2,complement(X1)))),zero,ifeq(one,one,complement(X1),meet(complement(X1),join(X2,complement(X1)))),meet(complement(X1),join(X2,complement(X1)))),
    inference(cp,[status(thm)],[t18,t18677]) ).

cnf(t8470,plain,
    meet(X1,meet(X2,X2)) = meet(X1,meet(X2,join(X3,join(Y3,meet(X1,X2))))),
    inference(cp,[status(thm)],[t8465,t15]) ).

cnf(t710599,plain,
    meet(X1,X2) = meet(X1,meet(X2,join(X3,join(Y3,meet(X1,X2))))),
    inference(step,[status(thm)],[t8470,t15]) ).

cnf(t8649,plain,
    meet(X1,meet(X2,join(X3,join(Y3,meet(X1,X2))))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710599]) ).

cnf(t8702,plain,
    meet(X1,complement(X1)) = meet(X1,meet(complement(X1),join(X2,join(X3,zero)))),
    inference(cp,[status(thm)],[t8649,t91]) ).

cnf(t710600,plain,
    zero = meet(X1,meet(complement(X1),join(X2,join(X3,zero)))),
    inference(step,[status(thm)],[t8702,t91]) ).

cnf(t710601,plain,
    zero = meet(X1,meet(complement(X1),join(X2,X3))),
    inference(step,[status(thm)],[t710600,t102]) ).

cnf(t8784,plain,
    meet(X1,meet(complement(X1),join(X2,X3))) = zero,
    inference(orient,[status(thm)],[t710601]) ).

cnf(t710779,plain,
    meet(complement(X1),join(X2,complement(X1))) = ifeq(zero,zero,ifeq(one,one,complement(X1),meet(complement(X1),join(X2,complement(X1)))),meet(complement(X1),join(X2,complement(X1)))),
    inference(step,[status(thm)],[t18680,t8784]) ).

cnf(t4,plain,
    ifeq(X1,X1,X2,X3) = X2,
    introduced(definition) ).

cnf(t17,plain,
    ifeq(X1,X1,X2,X3) = X2,
    inference(orient,[status(thm)],[t4]) ).

cnf(t710780,plain,
    meet(complement(X1),join(X2,complement(X1))) = ifeq(one,one,complement(X1),meet(complement(X1),join(X2,complement(X1)))),
    inference(step,[status(thm)],[t710779,t17]) ).

cnf(t710781,plain,
    meet(complement(X1),join(X2,complement(X1))) = complement(X1),
    inference(step,[status(thm)],[t710780,t17]) ).

cnf(t18777,plain,
    meet(complement(X1),join(X2,complement(X1))) = complement(X1),
    inference(orient,[status(thm)],[t710781]) ).

cnf(t18801,plain,
    join(complement(X1),X2) = join(complement(X1),meet(join(X2,X3),join(X2,complement(X1)))),
    inference(cp,[status(thm)],[t16572,t18777]) ).

cnf(t711263,plain,
    join(X2,complement(X1)) = join(complement(X1),meet(join(X2,X3),join(X2,complement(X1)))),
    inference(step,[status(thm)],[t18801,t23]) ).

cnf(t56196,plain,
    join(complement(X1),meet(join(X2,X3),join(X2,complement(X1)))) = join(X2,complement(X1)),
    inference(orient,[status(thm)],[t711263]) ).

cnf(t25,plain,
    X1 = ifeq(meet(X2,X1),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
    inference(cp,[status(thm)],[t18,t23]) ).

cnf(t710209,plain,
    X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
    inference(step,[status(thm)],[t25,t51]) ).

cnf(t448,plain,
    ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
    inference(orient,[status(thm)],[t710209]) ).

cnf(t460,plain,
    X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
    inference(cp,[status(thm)],[t448,t91]) ).

cnf(t710210,plain,
    X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
    inference(step,[status(thm)],[t460,t17]) ).

cnf(t710211,plain,
    X1 = ifeq(one,one,complement(complement(X1)),X1),
    inference(step,[status(thm)],[t710210,t46]) ).

cnf(t710212,plain,
    X1 = complement(complement(X1)),
    inference(step,[status(thm)],[t710211,t17]) ).

cnf(t479,plain,
    complement(complement(X1)) = X1,
    inference(orient,[status(thm)],[t710212]) ).

cnf(t56197,plain,
    join(X1,complement(complement(X2))) = join(X2,meet(join(X1,X3),join(X1,complement(complement(X2))))),
    inference(cp,[status(thm)],[t56196,t479]) ).

cnf(t711264,plain,
    join(X1,X2) = join(X2,meet(join(X1,X3),join(X1,complement(complement(X2))))),
    inference(step,[status(thm)],[t56197,t479]) ).

cnf(t711265,plain,
    join(X1,X2) = join(X2,meet(join(X1,X3),join(X1,X2))),
    inference(step,[status(thm)],[t711264,t479]) ).

cnf(t711266,plain,
    join(X1,X2) = join(X2,meet(join(X1,X2),join(X1,X3))),
    inference(step,[status(thm)],[t711265,t51]) ).

cnf(t56645,plain,
    join(X1,meet(join(X2,X1),join(X2,X3))) = join(X2,X1),
    inference(orient,[status(thm)],[t711266]) ).

cnf(t5627,plain,
    meet(X1,meet(one,join(X2,X3))) = meet(meet(X1,join(X2,X3)),join(Y3,meet(X1,one))),
    inference(cp,[status(thm)],[t5615,t1874]) ).

cnf(t710527,plain,
    meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y3,meet(X1,one))),
    inference(step,[status(thm)],[t5627,t1834]) ).

cnf(t710528,plain,
    meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y3,X1)),
    inference(step,[status(thm)],[t710527,t96]) ).

cnf(t710529,plain,
    meet(X1,join(X2,X3)) = meet(join(Y3,X1),meet(X1,join(X2,X3))),
    inference(step,[status(thm)],[t710528,t51]) ).

cnf(t710530,plain,
    meet(X1,join(X2,X3)) = meet(join(X2,X3),meet(join(Y3,X1),X1)),
    inference(step,[status(thm)],[t710529,t67]) ).

cnf(t710531,plain,
    meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(Y3,X1))),
    inference(step,[status(thm)],[t710530,t67]) ).

cnf(t710532,plain,
    meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,Y3))),
    inference(step,[status(thm)],[t710531,t23]) ).

cnf(t710533,plain,
    meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,Y3),join(X2,X3))),
    inference(step,[status(thm)],[t710532,t51]) ).

cnf(t5752,plain,
    meet(X1,meet(join(X1,X2),join(X3,Y3))) = meet(X1,join(X3,Y3)),
    inference(orient,[status(thm)],[t710533]) ).

cnf(t16666,plain,
    join(join(X1,X2),X3) = join(join(X1,X2),meet(join(X3,Y3),join(X3,X1))),
    inference(cp,[status(thm)],[t16572,t16572]) ).

cnf(t710752,plain,
    join(X3,join(X1,X2)) = join(join(X1,X2),meet(join(X3,Y3),join(X3,X1))),
    inference(step,[status(thm)],[t16666,t23]) ).

cnf(t710753,plain,
    join(X2,join(X3,X1)) = join(join(X1,X2),meet(join(X3,Y3),join(X3,X1))),
    inference(step,[status(thm)],[t710752,t26]) ).

cnf(t710754,plain,
    join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X3,Y3),join(X3,X1))),
    inference(step,[status(thm)],[t710753,t26]) ).

cnf(t710755,plain,
    join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X3,X1),join(X3,Y3))),
    inference(step,[status(thm)],[t710754,t51]) ).

cnf(t710756,plain,
    join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X1,X3),join(X3,Y3))),
    inference(step,[status(thm)],[t710755,t23]) ).

cnf(t17128,plain,
    join(join(X1,X2),meet(join(X1,X3),join(X3,Y3))) = join(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t710756]) ).

cnf(t17234,plain,
    join(X1,join(X2,zero)) = join(join(X1,X2),meet(join(X1,zero),meet(X3,Y3))),
    inference(cp,[status(thm)],[t17128,t2368]) ).

cnf(t710757,plain,
    join(X1,X2) = join(join(X1,X2),meet(join(X1,zero),meet(X3,Y3))),
    inference(step,[status(thm)],[t17234,t102]) ).

cnf(t710758,plain,
    join(X1,X2) = join(join(X1,X2),meet(Y3,meet(join(X1,zero),X3))),
    inference(step,[status(thm)],[t710757,t67]) ).

cnf(t710759,plain,
    join(X1,X2) = join(join(X1,X2),meet(X3,meet(Y3,join(X1,zero)))),
    inference(step,[status(thm)],[t710758,t67]) ).

cnf(t710760,plain,
    join(X1,X2) = join(join(X1,X2),meet(X3,meet(Y3,X1))),
    inference(step,[status(thm)],[t710759,t102]) ).

cnf(t710761,plain,
    join(X1,X2) = join(join(X1,X2),meet(X3,meet(X1,Y3))),
    inference(step,[status(thm)],[t710760,t51]) ).

cnf(t710762,plain,
    join(X1,X2) = join(join(X1,X2),meet(X1,meet(Y3,X3))),
    inference(step,[status(thm)],[t710761,t67]) ).

cnf(t710763,plain,
    join(X1,X2) = join(join(X1,X2),meet(X1,meet(X3,Y3))),
    inference(step,[status(thm)],[t710762,t51]) ).

cnf(t17420,plain,
    join(join(X1,X2),meet(X1,meet(X3,Y3))) = join(X1,X2),
    inference(orient,[status(thm)],[t710763]) ).

cnf(t17440,plain,
    join(X1,X2) = join(join(X1,X2),meet(X1,join(X3,Y3))),
    inference(cp,[status(thm)],[t17420,t5752]) ).

cnf(t17556,plain,
    join(join(X1,X2),meet(X1,join(X3,Y3))) = join(X1,X2),
    inference(orient,[status(thm)],[t17440]) ).

cnf(t56960,plain,
    join(X1,meet(join(X2,X1),join(X2,X3))) = join(join(X2,X1),meet(X1,join(Y3,Y4))),
    inference(cp,[status(thm)],[t17556,t56645]) ).

cnf(t711270,plain,
    join(X2,X1) = join(join(X2,X1),meet(X1,join(Y3,Y4))),
    inference(step,[status(thm)],[t56960,t56645]) ).

cnf(t57956,plain,
    join(join(X1,X2),meet(X2,join(X3,Y3))) = join(X1,X2),
    inference(orient,[status(thm)],[t711270]) ).

cnf(t57984,plain,
    join(X1,meet(X1,X2)) = join(X1,meet(meet(X1,X2),join(X3,Y3))),
    inference(cp,[status(thm)],[t57956,t14]) ).

cnf(t711271,plain,
    X1 = join(X1,meet(meet(X1,X2),join(X3,Y3))),
    inference(step,[status(thm)],[t57984,t14]) ).

cnf(t58410,plain,
    join(X1,meet(meet(X1,X2),join(X3,Y3))) = X1,
    inference(orient,[status(thm)],[t711271]) ).

cnf(t58487,plain,
    meet(meet(X1,X2),join(X3,Y3)) = meet(meet(meet(X1,X2),join(X3,Y3)),X1),
    inference(cp,[status(thm)],[t2521,t58410]) ).

cnf(t711295,plain,
    meet(meet(X1,X2),join(X3,Y3)) = meet(X1,meet(meet(X1,X2),join(X3,Y3))),
    inference(step,[status(thm)],[t58487,t51]) ).

cnf(t60989,plain,
    meet(X1,meet(meet(X1,X2),join(X3,Y3))) = meet(meet(X1,X2),join(X3,Y3)),
    inference(orient,[status(thm)],[t711295]) ).

cnf(t61013,plain,
    meet(meet(one,join(X1,X2)),join(X3,Y3)) = meet(one,meet(join(X1,X2),join(X3,Y3))),
    inference(cp,[status(thm)],[t60989,t1874]) ).

cnf(t711304,plain,
    meet(join(X3,Y3),meet(one,join(X1,X2))) = meet(one,meet(join(X1,X2),join(X3,Y3))),
    inference(step,[status(thm)],[t61013,t51]) ).

cnf(t711305,plain,
    meet(join(X3,Y3),join(X1,X2)) = meet(one,meet(join(X1,X2),join(X3,Y3))),
    inference(step,[status(thm)],[t711304,t1834]) ).

cnf(t711306,plain,
    meet(join(X1,X2),join(X3,Y3)) = meet(one,meet(join(X1,X2),join(X3,Y3))),
    inference(step,[status(thm)],[t711305,t51]) ).

cnf(t62894,plain,
    meet(one,meet(join(X1,X2),join(X3,Y3))) = meet(join(X1,X2),join(X3,Y3)),
    inference(orient,[status(thm)],[t711306]) ).

cnf(t6145,plain,
    meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(meet(X1,X2),join(Y3,meet(X1,join(X2,X3)))),
    inference(cp,[status(thm)],[t6132,t3156]) ).

cnf(t710539,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(Y3,meet(X1,join(X2,X3)))),
    inference(step,[status(thm)],[t6145,t3156]) ).

cnf(t6318,plain,
    meet(meet(X1,X2),join(X3,meet(X1,join(X2,Y3)))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710539]) ).

cnf(t6455,plain,
    meet(X1,meet(meet(join(X2,X1),X3),join(X2,X3))) = meet(X1,meet(join(X2,X1),X3)),
    inference(cp,[status(thm)],[t1618,t6318]) ).

cnf(t710546,plain,
    meet(X1,meet(join(X2,X3),meet(join(X2,X1),X3))) = meet(X1,meet(join(X2,X1),X3)),
    inference(step,[status(thm)],[t6455,t51]) ).

cnf(t710547,plain,
    meet(X1,meet(X3,meet(join(X2,X3),join(X2,X1)))) = meet(X1,meet(join(X2,X1),X3)),
    inference(step,[status(thm)],[t710546,t67]) ).

cnf(t710548,plain,
    meet(X1,meet(X3,meet(join(X2,X1),join(X2,X3)))) = meet(X1,meet(join(X2,X1),X3)),
    inference(step,[status(thm)],[t710547,t51]) ).

cnf(t710549,plain,
    meet(X1,meet(X3,meet(join(X1,X2),join(X2,X3)))) = meet(X1,meet(join(X2,X1),X3)),
    inference(step,[status(thm)],[t710548,t23]) ).

cnf(t5819,plain,
    meet(X1,meet(meet(join(X1,X2),join(X3,Y3)),Y4)) = meet(Y4,meet(X1,join(X3,Y3))),
    inference(cp,[status(thm)],[t67,t5752]) ).

cnf(t710542,plain,
    meet(X1,meet(Y4,meet(join(X1,X2),join(X3,Y3)))) = meet(Y4,meet(X1,join(X3,Y3))),
    inference(step,[status(thm)],[t5819,t51]) ).

cnf(t710543,plain,
    meet(X1,meet(Y4,meet(join(X1,X2),join(X3,Y3)))) = meet(X1,meet(join(X3,Y3),Y4)),
    inference(step,[status(thm)],[t710542,t67]) ).

cnf(t710544,plain,
    meet(X1,meet(Y4,meet(join(X1,X2),join(X3,Y3)))) = meet(X1,meet(Y4,join(X3,Y3))),
    inference(step,[status(thm)],[t710543,t51]) ).

cnf(t6641,plain,
    meet(X1,meet(X2,meet(join(X1,X3),join(Y3,Y4)))) = meet(X1,meet(X2,join(Y3,Y4))),
    inference(orient,[status(thm)],[t710544]) ).

cnf(t710550,plain,
    meet(X1,meet(X3,join(X2,X3))) = meet(X1,meet(join(X2,X1),X3)),
    inference(step,[status(thm)],[t710549,t6641]) ).

cnf(t710551,plain,
    meet(X1,meet(X3,join(X2,X3))) = meet(X1,meet(X3,join(X2,X1))),
    inference(step,[status(thm)],[t710550,t51]) ).

cnf(t710552,plain,
    meet(X1,meet(X3,join(X2,X3))) = meet(X1,meet(X3,join(X1,X2))),
    inference(step,[status(thm)],[t710551,t23]) ).

cnf(t710553,plain,
    meet(X1,meet(X3,join(X2,X3))) = meet(X1,X3),
    inference(step,[status(thm)],[t710552,t183]) ).

cnf(t6806,plain,
    meet(X1,meet(X2,join(X3,X2))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710553]) ).

cnf(t6819,plain,
    meet(X1,join(X2,meet(X3,Y3))) = meet(X1,meet(join(X2,meet(X3,Y3)),join(X3,X2))),
    inference(cp,[status(thm)],[t6806,t170]) ).

cnf(t710554,plain,
    meet(X1,join(X2,meet(X3,Y3))) = meet(X1,meet(join(X3,X2),join(X2,meet(X3,Y3)))),
    inference(step,[status(thm)],[t6819,t51]) ).

cnf(t710555,plain,
    meet(X1,join(X2,meet(X3,Y3))) = meet(X1,meet(join(X2,X3),join(X2,meet(X3,Y3)))),
    inference(step,[status(thm)],[t710554,t23]) ).

cnf(t6867,plain,
    meet(X1,meet(join(X2,X3),join(X2,meet(X3,Y3)))) = meet(X1,join(X2,meet(X3,Y3))),
    inference(orient,[status(thm)],[t710555]) ).

cnf(t62895,plain,
    meet(join(X1,X2),join(X1,meet(X2,X3))) = meet(one,join(X1,meet(X2,X3))),
    inference(cp,[status(thm)],[t62894,t6867]) ).

cnf(t711307,plain,
    meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
    inference(step,[status(thm)],[t62895,t1874]) ).

cnf(t63079,plain,
    meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t711307]) ).

cnf(t63101,plain,
    join(X1,meet(join(X1,X2),X3)) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
    inference(cp,[status(thm)],[t63079,t108]) ).

cnf(t711806,plain,
    join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
    inference(step,[status(thm)],[t63101,t51]) ).

cnf(t711807,plain,
    join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
    inference(step,[status(thm)],[t711806,t51]) ).

cnf(t149894,plain,
    meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))) = join(X1,meet(X3,join(X1,X2))),
    inference(orient,[status(thm)],[t711807]) ).

cnf(t150330,plain,
    meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X1,join(X2,X3)))),
    inference(cp,[status(thm)],[t754,t149894]) ).

cnf(t150515,plain,
    meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t150330]) ).

cnf(t150766,plain,
    meet(X1,join(X2,meet(join(X1,X3),join(X2,Y3)))) = meet(X1,meet(join(X1,X3),join(X2,Y3))),
    inference(cp,[status(thm)],[t5752,t150515]) ).

cnf(t711826,plain,
    meet(X1,join(X2,meet(join(X1,X3),join(X2,Y3)))) = meet(X1,join(X2,Y3)),
    inference(step,[status(thm)],[t150766,t5752]) ).

cnf(t156157,plain,
    meet(X1,join(X2,meet(join(X1,X3),join(X2,Y3)))) = meet(X1,join(X2,Y3)),
    inference(orient,[status(thm)],[t711826]) ).

cnf(t156267,plain,
    meet(X1,join(X2,meet(join(X3,X2),join(X3,Y3)))) = meet(X1,join(X2,meet(join(X1,Y4),join(X3,X2)))),
    inference(cp,[status(thm)],[t156157,t56645]) ).

cnf(t711830,plain,
    meet(X1,join(X3,X2)) = meet(X1,join(X2,meet(join(X1,Y4),join(X3,X2)))),
    inference(step,[status(thm)],[t156267,t56645]) ).

cnf(t159919,plain,
    meet(X1,join(X2,meet(join(X1,X3),join(Y3,X2)))) = meet(X1,join(Y3,X2)),
    inference(orient,[status(thm)],[t711830]) ).

cnf(t160303,plain,
    meet(X1,join(X2,meet(X2,X3))) = meet(X1,join(meet(X2,X3),meet(join(X1,Y3),X2))),
    inference(cp,[status(thm)],[t159919,t14]) ).

cnf(t711831,plain,
    meet(X1,X2) = meet(X1,join(meet(X2,X3),meet(join(X1,Y3),X2))),
    inference(step,[status(thm)],[t160303,t14]) ).

cnf(t711832,plain,
    meet(X1,X2) = meet(X1,join(meet(X2,X3),meet(X2,join(X1,Y3)))),
    inference(step,[status(thm)],[t711831,t51]) ).

cnf(t160738,plain,
    meet(X1,join(meet(X2,X3),meet(X2,join(X1,Y3)))) = meet(X1,X2),
    inference(orient,[status(thm)],[t711832]) ).

cnf(t161135,plain,
    join(meet(X1,X2),X3) = join(X3,meet(join(meet(X1,X2),X3),X1)),
    inference(cp,[status(thm)],[t56645,t160738]) ).

cnf(t711838,plain,
    join(X3,meet(X1,X2)) = join(X3,meet(join(meet(X1,X2),X3),X1)),
    inference(step,[status(thm)],[t161135,t23]) ).

cnf(t711839,plain,
    join(X3,meet(X1,X2)) = join(X3,meet(X1,join(meet(X1,X2),X3))),
    inference(step,[status(thm)],[t711838,t51]) ).

cnf(t711840,plain,
    join(X3,meet(X1,X2)) = join(X3,meet(X1,join(X3,meet(X1,X2)))),
    inference(step,[status(thm)],[t711839,t23]) ).

cnf(t162060,plain,
    join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t711840]) ).

cnf(t18786,plain,
    join(X1,X2) = join(join(X1,X2),meet(X1,complement(X3))),
    inference(cp,[status(thm)],[t17420,t18777]) ).

cnf(t19612,plain,
    join(join(X1,X2),meet(X1,complement(X3))) = join(X1,X2),
    inference(orient,[status(thm)],[t18786]) ).

cnf(t56956,plain,
    join(X1,meet(join(X2,X1),join(X2,X3))) = join(join(X2,X1),meet(X1,complement(Y3))),
    inference(cp,[status(thm)],[t19612,t56645]) ).

cnf(t711267,plain,
    join(X2,X1) = join(join(X2,X1),meet(X1,complement(Y3))),
    inference(step,[status(thm)],[t56956,t56645]) ).

cnf(t57249,plain,
    join(join(X1,X2),meet(X2,complement(X3))) = join(X1,X2),
    inference(orient,[status(thm)],[t711267]) ).

cnf(t15522,plain,
    join(X1,meet(X1,X2)) = join(X1,meet(X3,join(meet(X1,X2),meet(X1,Y3)))),
    inference(cp,[status(thm)],[t15520,t14620]) ).

cnf(t710736,plain,
    X1 = join(X1,meet(X3,join(meet(X1,X2),meet(X1,Y3)))),
    inference(step,[status(thm)],[t15522,t14]) ).

cnf(t15647,plain,
    join(X1,meet(X2,join(meet(X1,X3),meet(X1,Y3)))) = X1,
    inference(orient,[status(thm)],[t710736]) ).

cnf(t18803,plain,
    complement(X1) = join(complement(X1),meet(X2,join(complement(X1),meet(complement(X1),X3)))),
    inference(cp,[status(thm)],[t15647,t18777]) ).

cnf(t710786,plain,
    complement(X1) = join(complement(X1),meet(X2,complement(X1))),
    inference(step,[status(thm)],[t18803,t14]) ).

cnf(t19242,plain,
    join(complement(X1),meet(X2,complement(X1))) = complement(X1),
    inference(orient,[status(thm)],[t710786]) ).

cnf(t57279,plain,
    join(complement(X1),meet(X2,complement(X1))) = join(complement(X1),meet(meet(X2,complement(X1)),complement(X3))),
    inference(cp,[status(thm)],[t57249,t19242]) ).

cnf(t711276,plain,
    complement(X1) = join(complement(X1),meet(meet(X2,complement(X1)),complement(X3))),
    inference(step,[status(thm)],[t57279,t19242]) ).

cnf(t711277,plain,
    complement(X1) = join(complement(X1),meet(complement(X3),meet(X2,complement(X1)))),
    inference(step,[status(thm)],[t711276,t51]) ).

cnf(t711278,plain,
    complement(X1) = join(complement(X1),meet(complement(X1),meet(complement(X3),X2))),
    inference(step,[status(thm)],[t711277,t67]) ).

cnf(t711279,plain,
    complement(X1) = join(complement(X1),meet(X2,meet(complement(X1),complement(X3)))),
    inference(step,[status(thm)],[t711278,t67]) ).

cnf(t59723,plain,
    join(complement(X1),meet(X2,meet(complement(X1),complement(X3)))) = complement(X1),
    inference(orient,[status(thm)],[t711279]) ).

cnf(t59734,plain,
    join(complement(X1),meet(X2,meet(complement(X1),complement(X3)))) = join(complement(X1),meet(meet(X2,meet(complement(X1),complement(X3))),complement(Y3))),
    inference(cp,[status(thm)],[t57249,t59723]) ).

cnf(t711790,plain,
    complement(X1) = join(complement(X1),meet(meet(X2,meet(complement(X1),complement(X3))),complement(Y3))),
    inference(step,[status(thm)],[t59734,t59723]) ).

cnf(t711791,plain,
    complement(X1) = join(complement(X1),meet(complement(Y3),meet(X2,meet(complement(X1),complement(X3))))),
    inference(step,[status(thm)],[t711790,t51]) ).

cnf(t711792,plain,
    complement(X1) = join(complement(X1),meet(X2,meet(meet(complement(X1),complement(X3)),complement(Y3)))),
    inference(step,[status(thm)],[t711791,t67]) ).

cnf(t711793,plain,
    complement(X1) = join(complement(X1),meet(X2,meet(complement(Y3),meet(complement(X1),complement(X3))))),
    inference(step,[status(thm)],[t711792,t51]) ).

cnf(t711794,plain,
    complement(X1) = join(complement(X1),meet(X2,meet(complement(X3),meet(complement(Y3),complement(X1))))),
    inference(step,[status(thm)],[t711793,t67]) ).

cnf(t711795,plain,
    complement(X1) = join(complement(X1),meet(X2,meet(complement(X1),meet(complement(X3),complement(Y3))))),
    inference(step,[status(thm)],[t711794,t67]) ).

cnf(t147176,plain,
    join(complement(X1),meet(X2,meet(complement(X1),meet(complement(X3),complement(Y3))))) = complement(X1),
    inference(orient,[status(thm)],[t711795]) ).

cnf(t161026,plain,
    meet(complement(X1),X2) = meet(complement(X1),join(meet(X2,X3),meet(X2,complement(X1)))),
    inference(cp,[status(thm)],[t160738,t147176]) ).

cnf(t711841,plain,
    meet(X2,complement(X1)) = meet(complement(X1),join(meet(X2,X3),meet(X2,complement(X1)))),
    inference(step,[status(thm)],[t161026,t51]) ).

cnf(t162518,plain,
    meet(complement(X1),join(meet(X2,X3),meet(X2,complement(X1)))) = meet(X2,complement(X1)),
    inference(orient,[status(thm)],[t711841]) ).

cnf(t162519,plain,
    meet(X1,complement(complement(X2))) = meet(X2,join(meet(X1,X3),meet(X1,complement(complement(X2))))),
    inference(cp,[status(thm)],[t162518,t479]) ).

cnf(t711842,plain,
    meet(X1,X2) = meet(X2,join(meet(X1,X3),meet(X1,complement(complement(X2))))),
    inference(step,[status(thm)],[t162519,t479]) ).

cnf(t711843,plain,
    meet(X1,X2) = meet(X2,join(meet(X1,X3),meet(X1,X2))),
    inference(step,[status(thm)],[t711842,t479]) ).

cnf(t711844,plain,
    meet(X1,X2) = meet(X2,join(meet(X1,X2),meet(X1,X3))),
    inference(step,[status(thm)],[t711843,t23]) ).

cnf(t163258,plain,
    meet(X1,join(meet(X2,X1),meet(X2,X3))) = meet(X2,X1),
    inference(orient,[status(thm)],[t711844]) ).

cnf(t164007,plain,
    join(X1,meet(X2,join(meet(X3,X2),meet(X3,Y3)))) = join(X1,meet(X2,join(X1,meet(X3,X2)))),
    inference(cp,[status(thm)],[t162060,t163258]) ).

cnf(t711846,plain,
    join(X1,meet(X3,X2)) = join(X1,meet(X2,join(X1,meet(X3,X2)))),
    inference(step,[status(thm)],[t164007,t163258]) ).

cnf(t165317,plain,
    join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(X1,meet(X3,X2)),
    inference(orient,[status(thm)],[t711846]) ).

cnf(t165683,plain,
    join(X1,meet(meet(X2,X3),join(X3,Y3))) = join(X1,meet(join(X3,Y3),join(X1,meet(X2,X3)))),
    inference(cp,[status(thm)],[t165317,t9929]) ).

cnf(t711877,plain,
    join(X1,meet(X2,X3)) = join(X1,meet(join(X3,Y3),join(X1,meet(X2,X3)))),
    inference(step,[status(thm)],[t165683,t9929]) ).

cnf(t176628,plain,
    join(X1,meet(join(X2,X3),join(X1,meet(Y3,X2)))) = join(X1,meet(Y3,X2)),
    inference(orient,[status(thm)],[t711877]) ).

cnf(t150604,plain,
    meet(X1,join(X2,meet(join(X3,X2),join(X3,Y3)))) = meet(X1,join(X2,meet(X1,join(X3,X2)))),
    inference(cp,[status(thm)],[t150515,t56645]) ).

cnf(t711808,plain,
    meet(X1,join(X3,X2)) = meet(X1,join(X2,meet(X1,join(X3,X2)))),
    inference(step,[status(thm)],[t150604,t56645]) ).

cnf(t150964,plain,
    meet(X1,join(X2,meet(X1,join(X3,X2)))) = meet(X1,join(X3,X2)),
    inference(orient,[status(thm)],[t711808]) ).

cnf(t151161,plain,
    meet(X1,join(X2,meet(X2,X3))) = meet(X1,join(meet(X2,X3),meet(X1,X2))),
    inference(cp,[status(thm)],[t150964,t14]) ).

cnf(t711809,plain,
    meet(X1,X2) = meet(X1,join(meet(X2,X3),meet(X1,X2))),
    inference(step,[status(thm)],[t151161,t14]) ).

cnf(t711810,plain,
    meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
    inference(step,[status(thm)],[t711809,t23]) ).

cnf(t151571,plain,
    meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
    inference(orient,[status(thm)],[t711810]) ).

cnf(t176649,plain,
    join(meet(join(X1,X2),X3),meet(X3,X1)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
    inference(cp,[status(thm)],[t176628,t151571]) ).

cnf(t711878,plain,
    join(meet(X3,X1),meet(join(X1,X2),X3)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
    inference(step,[status(thm)],[t176649,t23]) ).

cnf(t711879,plain,
    join(meet(X1,X3),meet(join(X1,X2),X3)) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
    inference(step,[status(thm)],[t711878,t51]) ).

cnf(t711880,plain,
    join(meet(X1,X3),meet(X3,join(X1,X2))) = join(meet(join(X1,X2),X3),meet(join(X1,X2),X3)),
    inference(step,[status(thm)],[t711879,t51]) ).

cnf(t711881,plain,
    join(meet(X1,X3),meet(X3,join(X1,X2))) = meet(join(X1,X2),X3),
    inference(step,[status(thm)],[t711880,t13]) ).

cnf(t711882,plain,
    join(meet(X1,X3),meet(X3,join(X1,X2))) = meet(X3,join(X1,X2)),
    inference(step,[status(thm)],[t711881,t51]) ).

cnf(t177375,plain,
    join(meet(X1,X2),meet(X2,join(X1,X3))) = meet(X2,join(X1,X3)),
    inference(orient,[status(thm)],[t711882]) ).

cnf(t177458,plain,
    meet(join(X1,X2),join(X1,X3)) = join(X1,meet(join(X1,X2),join(X1,X3))),
    inference(cp,[status(thm)],[t177375,t16]) ).

cnf(t178364,plain,
    join(X1,meet(join(X1,X2),join(X1,X3))) = meet(join(X1,X2),join(X1,X3)),
    inference(orient,[status(thm)],[t177458]) ).

cnf(t178381,plain,
    meet(join(X1,meet(join(X2,X1),join(X2,X3))),join(X1,Y3)) = join(X1,meet(join(X2,X1),join(X1,Y3))),
    inference(cp,[status(thm)],[t178364,t56645]) ).

cnf(t711883,plain,
    meet(join(X2,X1),join(X1,Y3)) = join(X1,meet(join(X2,X1),join(X1,Y3))),
    inference(step,[status(thm)],[t178381,t56645]) ).

cnf(t178942,plain,
    join(X1,meet(join(X2,X1),join(X1,X3))) = meet(join(X2,X1),join(X1,X3)),
    inference(orient,[status(thm)],[t711883]) ).

cnf(t178943,plain,
    meet(join(X1,X2),join(X2,meet(X3,X1))) = join(X2,meet(X3,X1)),
    inference(cp,[status(thm)],[t178942,t176628]) ).

cnf(t711896,plain,
    meet(join(X1,X2),join(X2,meet(X1,X3))) = join(X2,meet(X3,X1)),
    inference(step,[status(thm)],[t178943,t51]) ).

cnf(t711897,plain,
    meet(join(X1,X2),join(X2,meet(X1,X3))) = join(X2,meet(X1,X3)),
    inference(step,[status(thm)],[t711896,t51]) ).

cnf(t180707,plain,
    meet(join(X1,X2),join(X2,meet(X1,X3))) = join(X2,meet(X1,X3)),
    inference(orient,[status(thm)],[t711897]) ).

cnf(t180748,plain,
    join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(meet(X1,X2),meet(X1,X3))),
    inference(cp,[status(thm)],[t180707,t14]) ).

cnf(t181587,plain,
    meet(X1,join(meet(X1,X2),meet(X1,X3))) = join(meet(X1,X2),meet(X1,X3)),
    inference(orient,[status(thm)],[t180748]) ).

cnf(t181602,plain,
    join(meet(X1,join(meet(X2,X1),meet(X2,X3))),meet(X1,Y3)) = meet(X1,join(meet(X2,X1),meet(X1,Y3))),
    inference(cp,[status(thm)],[t181587,t163258]) ).

cnf(t711898,plain,
    join(meet(X2,X1),meet(X1,Y3)) = meet(X1,join(meet(X2,X1),meet(X1,Y3))),
    inference(step,[status(thm)],[t181602,t163258]) ).

cnf(t182205,plain,
    meet(X1,join(meet(X2,X1),meet(X1,X3))) = join(meet(X2,X1),meet(X1,X3)),
    inference(orient,[status(thm)],[t711898]) ).

cnf(t178963,plain,
    meet(join(X1,X2),join(X2,meet(join(X1,X2),X2))) = join(X2,meet(join(X1,X2),X2)),
    inference(cp,[status(thm)],[t178942,t2566]) ).

cnf(t711884,plain,
    meet(join(X1,X2),X2) = join(X2,meet(join(X1,X2),X2)),
    inference(step,[status(thm)],[t178963,t2566]) ).

cnf(t711885,plain,
    meet(X2,join(X1,X2)) = join(X2,meet(join(X1,X2),X2)),
    inference(step,[status(thm)],[t711884,t51]) ).

cnf(t711886,plain,
    meet(X2,join(X1,X2)) = join(X2,meet(X2,join(X1,X2))),
    inference(step,[status(thm)],[t711885,t51]) ).

cnf(t711887,plain,
    meet(X2,join(X1,X2)) = X2,
    inference(step,[status(thm)],[t711886,t14]) ).

cnf(t179822,plain,
    meet(X1,join(X2,X1)) = X1,
    inference(orient,[status(thm)],[t711887]) ).

cnf(t15608,plain,
    join(X1,join(X2,meet(X3,join(meet(X1,Y3),meet(X2,Y4))))) = join(X1,join(X2,meet(X1,Y3))),
    inference(cp,[status(thm)],[t15432,t15520]) ).

cnf(t710737,plain,
    join(X1,join(X2,meet(X3,join(meet(X1,Y3),meet(X2,Y4))))) = join(X1,X2),
    inference(step,[status(thm)],[t15608,t170]) ).

cnf(t15934,plain,
    join(X1,join(X2,meet(X3,join(meet(X1,Y3),meet(X2,Y4))))) = join(X1,X2),
    inference(orient,[status(thm)],[t710737]) ).

cnf(t15954,plain,
    join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,meet(X2,Y3))))),
    inference(cp,[status(thm)],[t15934,t15]) ).

cnf(t16118,plain,
    join(X1,join(X2,meet(X3,join(X1,meet(X2,Y3))))) = join(X1,X2),
    inference(orient,[status(thm)],[t15954]) ).

cnf(t17177,plain,
    join(X1,join(X2,X3)) = join(join(X1,X2),meet(join(X1,X3),X3)),
    inference(cp,[status(thm)],[t17128,t2566]) ).

cnf(t710764,plain,
    join(X1,join(X2,X3)) = join(join(X1,X2),meet(X3,join(X1,X3))),
    inference(step,[status(thm)],[t17177,t51]) ).

cnf(t17723,plain,
    join(join(X1,X2),meet(X3,join(X1,X3))) = join(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t710764]) ).

cnf(t15932,plain,
    join(X1,join(meet(X2,join(meet(X1,X3),meet(X1,Y3))),Y4)) = join(Y4,X1),
    inference(cp,[status(thm)],[t26,t15647]) ).

cnf(t710741,plain,
    join(X1,join(Y4,meet(X2,join(meet(X1,X3),meet(X1,Y3))))) = join(Y4,X1),
    inference(step,[status(thm)],[t15932,t23]) ).

cnf(t710742,plain,
    join(X1,join(Y4,meet(X2,join(meet(X1,X3),meet(X1,Y3))))) = join(X1,Y4),
    inference(step,[status(thm)],[t710741,t23]) ).

cnf(t16324,plain,
    join(X1,join(X2,meet(X3,join(meet(X1,Y3),meet(X1,Y4))))) = join(X1,X2),
    inference(orient,[status(thm)],[t710742]) ).

cnf(t18477,plain,
    one = join(complement(X1),meet(join(X2,X1),join(X3,complement(complement(X1))))),
    inference(cp,[status(thm)],[t18473,t479]) ).

cnf(t710792,plain,
    one = join(complement(X1),meet(join(X1,X2),join(X3,complement(complement(X1))))),
    inference(step,[status(thm)],[t18477,t23]) ).

cnf(t710793,plain,
    one = join(complement(X1),meet(join(X1,X2),join(X3,X1))),
    inference(step,[status(thm)],[t710792,t479]) ).

cnf(t710794,plain,
    one = join(complement(X1),meet(join(X1,X2),join(X1,X3))),
    inference(step,[status(thm)],[t710793,t23]) ).

cnf(t19903,plain,
    join(complement(X1),meet(join(X1,X2),join(X1,X3))) = one,
    inference(orient,[status(thm)],[t710794]) ).

cnf(t20018,plain,
    join(X1,complement(meet(X1,X2))) = join(X1,one),
    inference(cp,[status(thm)],[t16324,t19903]) ).

cnf(t710795,plain,
    join(X1,complement(meet(X1,X2))) = one,
    inference(step,[status(thm)],[t20018,t119]) ).

cnf(t20070,plain,
    join(X1,complement(meet(X1,X2))) = one,
    inference(orient,[status(thm)],[t710795]) ).

cnf(t20080,plain,
    join(X1,join(X2,complement(meet(X1,X3)))) = join(join(X1,X2),meet(complement(meet(X1,X3)),one)),
    inference(cp,[status(thm)],[t17723,t20070]) ).

cnf(t20079,plain,
    join(X1,join(complement(meet(X1,X2)),X3)) = join(one,meet(X3,join(X1,X3))),
    inference(cp,[status(thm)],[t17723,t20070]) ).

cnf(t710796,plain,
    join(X1,join(X3,complement(meet(X1,X2)))) = join(one,meet(X3,join(X1,X3))),
    inference(step,[status(thm)],[t20079,t23]) ).

cnf(t14178,plain,
    join(X1,join(X2,join(X3,join(Y3,complement(X2))))) = join(X1,join(one,meet(Y4,join(X1,X2)))),
    inference(cp,[status(thm)],[t14173,t196]) ).

cnf(t710715,plain,
    join(X1,one) = join(X1,join(one,meet(Y4,join(X1,X2)))),
    inference(step,[status(thm)],[t14178,t196]) ).

cnf(t710716,plain,
    one = join(X1,join(one,meet(Y4,join(X1,X2)))),
    inference(step,[status(thm)],[t710715,t119]) ).

cnf(t14284,plain,
    join(X1,join(one,meet(X2,join(X1,X3)))) = one,
    inference(orient,[status(thm)],[t710716]) ).

cnf(t10199,plain,
    meet(meet(X1,X2),join(X3,meet(X2,join(X1,Y3)))) = meet(meet(X1,X2),join(join(X3,meet(X2,join(X1,Y3))),Y4)),
    inference(cp,[status(thm)],[t9929,t10080]) ).

cnf(t710660,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(join(X3,meet(X2,join(X1,Y3))),Y4)),
    inference(step,[status(thm)],[t10199,t10080]) ).

cnf(t710661,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(Y4,join(X3,meet(X2,join(X1,Y3))))),
    inference(step,[status(thm)],[t710660,t23]) ).

cnf(t710662,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X2,join(X1,Y3)),Y4))),
    inference(step,[status(thm)],[t710661,t26]) ).

cnf(t710663,plain,
    meet(X1,X2) = meet(meet(X1,X2),join(X3,join(Y4,meet(X2,join(X1,Y3))))),
    inference(step,[status(thm)],[t710662,t23]) ).

cnf(t10981,plain,
    meet(meet(X1,X2),join(X3,join(Y3,meet(X2,join(X1,Y4))))) = meet(X1,X2),
    inference(orient,[status(thm)],[t710663]) ).

cnf(t14306,plain,
    one = join(X1,join(one,meet(X2,X3))),
    inference(cp,[status(thm)],[t14284,t10981]) ).

cnf(t14393,plain,
    join(X1,join(one,meet(X2,X3))) = one,
    inference(orient,[status(thm)],[t14306]) ).

cnf(t14394,plain,
    one = join(one,meet(X1,X2)),
    inference(cp,[status(thm)],[t14393,t108]) ).

cnf(t14461,plain,
    join(one,meet(X1,X2)) = one,
    inference(orient,[status(thm)],[t14394]) ).

cnf(t710797,plain,
    join(X1,join(X3,complement(meet(X1,X2)))) = one,
    inference(step,[status(thm)],[t710796,t14461]) ).

cnf(t20146,plain,
    join(X1,join(X2,complement(meet(X1,X3)))) = one,
    inference(orient,[status(thm)],[t710797]) ).

cnf(t710812,plain,
    one = join(join(X1,X2),meet(complement(meet(X1,X3)),one)),
    inference(step,[status(thm)],[t20080,t20146]) ).

cnf(t710813,plain,
    one = join(join(X1,X2),complement(meet(X1,X3))),
    inference(step,[status(thm)],[t710812,t96]) ).

cnf(t20742,plain,
    join(join(X1,X2),complement(meet(X1,X3))) = one,
    inference(orient,[status(thm)],[t710813]) ).

cnf(t20744,plain,
    one = join(join(X1,join(X2,X3)),complement(meet(join(X1,X2),Y3))),
    inference(cp,[status(thm)],[t20742,t17723]) ).

cnf(t710851,plain,
    one = join(join(X1,join(X2,X3)),complement(meet(Y3,join(X1,X2)))),
    inference(step,[status(thm)],[t20744,t51]) ).

cnf(t22898,plain,
    join(join(X1,join(X2,X3)),complement(meet(Y3,join(X1,X2)))) = one,
    inference(orient,[status(thm)],[t710851]) ).

cnf(t22903,plain,
    one = join(join(X1,X2),complement(meet(X3,join(X1,X2)))),
    inference(cp,[status(thm)],[t22898,t15934]) ).

cnf(t23127,plain,
    join(join(X1,X2),complement(meet(X3,join(X1,X2)))) = one,
    inference(orient,[status(thm)],[t22903]) ).

cnf(t23162,plain,
    one = join(join(X1,meet(X2,join(X3,Y3))),complement(meet(X3,X2))),
    inference(cp,[status(thm)],[t23127,t10080]) ).

cnf(t710896,plain,
    one = join(complement(meet(X3,X2)),join(X1,meet(X2,join(X3,Y3)))),
    inference(step,[status(thm)],[t23162,t23]) ).

cnf(t710897,plain,
    one = join(X1,join(meet(X2,join(X3,Y3)),complement(meet(X3,X2)))),
    inference(step,[status(thm)],[t710896,t26]) ).

cnf(t710898,plain,
    one = join(X1,join(complement(meet(X3,X2)),meet(X2,join(X3,Y3)))),
    inference(step,[status(thm)],[t710897,t23]) ).

cnf(t710899,plain,
    one = join(X1,join(complement(meet(X2,X3)),meet(X2,join(X3,Y3)))),
    inference(step,[status(thm)],[t710898,t51]) ).

cnf(t26510,plain,
    join(X1,join(complement(meet(X2,X3)),meet(X2,join(X3,Y3)))) = one,
    inference(orient,[status(thm)],[t710899]) ).

cnf(t26516,plain,
    one = join(complement(meet(X1,X2)),meet(X1,join(X2,X3))),
    inference(cp,[status(thm)],[t26510,t108]) ).

cnf(t26805,plain,
    join(complement(meet(X1,X2)),meet(X1,join(X2,X3))) = one,
    inference(orient,[status(thm)],[t26516]) ).

cnf(t27045,plain,
    meet(complement(meet(X1,X2)),X3) = meet(meet(complement(meet(X1,X2)),X3),join(Y3,meet(X3,one))),
    inference(cp,[status(thm)],[t10080,t26805]) ).

cnf(t710985,plain,
    meet(X3,complement(meet(X1,X2))) = meet(meet(complement(meet(X1,X2)),X3),join(Y3,meet(X3,one))),
    inference(step,[status(thm)],[t27045,t51]) ).

cnf(t710986,plain,
    meet(X3,complement(meet(X1,X2))) = meet(join(Y3,meet(X3,one)),meet(complement(meet(X1,X2)),X3)),
    inference(step,[status(thm)],[t710985,t51]) ).

cnf(t710987,plain,
    meet(X3,complement(meet(X1,X2))) = meet(X3,meet(join(Y3,meet(X3,one)),complement(meet(X1,X2)))),
    inference(step,[status(thm)],[t710986,t67]) ).

cnf(t710988,plain,
    meet(X3,complement(meet(X1,X2))) = meet(X3,meet(complement(meet(X1,X2)),join(Y3,meet(X3,one)))),
    inference(step,[status(thm)],[t710987,t51]) ).

cnf(t710989,plain,
    meet(X3,complement(meet(X1,X2))) = meet(X3,meet(complement(meet(X1,X2)),join(Y3,X3))),
    inference(step,[status(thm)],[t710988,t96]) ).

cnf(t710990,plain,
    meet(X3,complement(meet(X1,X2))) = meet(X3,meet(complement(meet(X1,X2)),join(X3,Y3))),
    inference(step,[status(thm)],[t710989,t23]) ).

cnf(t710991,plain,
    meet(X3,complement(meet(X1,X2))) = meet(X3,meet(join(X3,Y3),complement(meet(X1,X2)))),
    inference(step,[status(thm)],[t710990,t51]) ).

cnf(t33712,plain,
    meet(X1,meet(join(X1,X2),complement(meet(X3,Y3)))) = meet(X1,complement(meet(X3,Y3))),
    inference(orient,[status(thm)],[t710991]) ).

cnf(t33730,plain,
    meet(X1,complement(meet(join(X2,X3),join(X2,join(X3,Y3))))) = meet(X1,meet(join(X1,Y4),complement(join(X2,X3)))),
    inference(cp,[status(thm)],[t33712,t2060]) ).

cnf(t710993,plain,
    meet(X1,complement(join(X2,X3))) = meet(X1,meet(join(X1,Y4),complement(join(X2,X3)))),
    inference(step,[status(thm)],[t33730,t2060]) ).

cnf(t34093,plain,
    meet(X1,meet(join(X1,X2),complement(join(X3,Y3)))) = meet(X1,complement(join(X3,Y3))),
    inference(orient,[status(thm)],[t710993]) ).

cnf(t34095,plain,
    meet(X1,complement(join(X1,X2))) = meet(X1,zero),
    inference(cp,[status(thm)],[t34093,t91]) ).

cnf(t710994,plain,
    meet(X1,complement(join(X1,X2))) = zero,
    inference(step,[status(thm)],[t34095,t136]) ).

cnf(t34193,plain,
    meet(X1,complement(join(X1,X2))) = zero,
    inference(orient,[status(thm)],[t710994]) ).

cnf(t34195,plain,
    zero = meet(join(X1,X2),complement(join(X1,join(X2,X3)))),
    inference(cp,[status(thm)],[t34193,t17723]) ).

cnf(t34336,plain,
    meet(join(X1,X2),complement(join(X1,join(X2,X3)))) = zero,
    inference(orient,[status(thm)],[t34195]) ).

cnf(t34447,plain,
    zero = meet(meet(X1,X2),complement(join(zero,join(meet(X1,X2),X3)))),
    inference(cp,[status(thm)],[t34336,t2368]) ).

cnf(t711014,plain,
    zero = meet(meet(X1,X2),complement(join(X3,join(zero,meet(X1,X2))))),
    inference(step,[status(thm)],[t34447,t26]) ).

cnf(t711015,plain,
    zero = meet(meet(X1,X2),complement(join(X3,meet(X1,X2)))),
    inference(step,[status(thm)],[t711014,t2368]) ).

cnf(t35155,plain,
    meet(meet(X1,X2),complement(join(X3,meet(X1,X2)))) = zero,
    inference(orient,[status(thm)],[t711015]) ).

cnf(t35170,plain,
    zero = meet(meet(X1,join(meet(X2,X3),meet(X2,Y3))),complement(X2)),
    inference(cp,[status(thm)],[t35155,t15647]) ).

cnf(t711054,plain,
    zero = meet(complement(X2),meet(X1,join(meet(X2,X3),meet(X2,Y3)))),
    inference(step,[status(thm)],[t35170,t51]) ).

cnf(t711055,plain,
    zero = meet(X1,meet(join(meet(X2,X3),meet(X2,Y3)),complement(X2))),
    inference(step,[status(thm)],[t711054,t67]) ).

cnf(t711056,plain,
    zero = meet(X1,meet(complement(X2),join(meet(X2,X3),meet(X2,Y3)))),
    inference(step,[status(thm)],[t711055,t51]) ).

cnf(t38052,plain,
    meet(X1,meet(complement(X2),join(meet(X2,X3),meet(X2,Y3)))) = zero,
    inference(orient,[status(thm)],[t711056]) ).

cnf(t38054,plain,
    zero = meet(complement(X1),join(meet(X1,X2),meet(X1,X3))),
    inference(cp,[status(thm)],[t38052,t125]) ).

cnf(t38330,plain,
    meet(complement(X1),join(meet(X1,X2),meet(X1,X3))) = zero,
    inference(orient,[status(thm)],[t38054]) ).

cnf(t38337,plain,
    zero = meet(complement(join(X1,X2)),join(meet(join(X1,X2),X3),X1)),
    inference(cp,[status(thm)],[t38330,t16572]) ).

cnf(t711184,plain,
    zero = meet(complement(join(X1,X2)),join(X1,meet(join(X1,X2),X3))),
    inference(step,[status(thm)],[t38337,t23]) ).

cnf(t711185,plain,
    zero = meet(complement(join(X1,X2)),join(X1,meet(X3,join(X1,X2)))),
    inference(step,[status(thm)],[t711184,t51]) ).

cnf(t45279,plain,
    meet(complement(join(X1,X2)),join(X1,meet(X3,join(X1,X2)))) = zero,
    inference(orient,[status(thm)],[t711185]) ).

cnf(t45434,plain,
    join(X1,complement(join(X2,X3))) = join(X1,join(complement(join(X2,X3)),meet(Y3,join(X1,zero)))),
    inference(cp,[status(thm)],[t16118,t45279]) ).

cnf(t711254,plain,
    join(X1,complement(join(X2,X3))) = join(X1,join(complement(join(X2,X3)),meet(Y3,X1))),
    inference(step,[status(thm)],[t45434,t102]) ).

cnf(t711255,plain,
    join(X1,complement(join(X2,X3))) = join(X1,join(complement(join(X2,X3)),meet(X1,Y3))),
    inference(step,[status(thm)],[t711254,t51]) ).

cnf(t711256,plain,
    join(X1,complement(join(X2,X3))) = join(X1,join(meet(X1,Y3),complement(join(X2,X3)))),
    inference(step,[status(thm)],[t711255,t23]) ).

cnf(t53163,plain,
    join(X1,join(meet(X1,X2),complement(join(X3,Y3)))) = join(X1,complement(join(X3,Y3))),
    inference(orient,[status(thm)],[t711256]) ).

cnf(t94,plain,
    meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
    inference(cp,[status(thm)],[t67,t91]) ).

cnf(t710112,plain,
    meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
    inference(step,[status(thm)],[t94,t51]) ).

cnf(t710113,plain,
    meet(X1,meet(X2,complement(X1))) = zero,
    inference(step,[status(thm)],[t710112,t136]) ).

cnf(t162,plain,
    meet(X1,meet(X2,complement(X1))) = zero,
    inference(orient,[status(thm)],[t710113]) ).

cnf(t167,plain,
    meet(X1,join(meet(X2,complement(X1)),X3)) = meet(X1,join(meet(X2,complement(X1)),meet(join(X1,meet(X2,complement(X1))),join(X3,zero)))),
    inference(cp,[status(thm)],[t54,t162]) ).

cnf(t711036,plain,
    meet(X1,join(X3,meet(X2,complement(X1)))) = meet(X1,join(meet(X2,complement(X1)),meet(join(X1,meet(X2,complement(X1))),join(X3,zero)))),
    inference(step,[status(thm)],[t167,t23]) ).

cnf(t711037,plain,
    meet(X1,join(X3,meet(X2,complement(X1)))) = meet(X1,join(meet(X2,complement(X1)),meet(join(X3,zero),join(X1,meet(X2,complement(X1)))))),
    inference(step,[status(thm)],[t711036,t51]) ).

cnf(t711038,plain,
    meet(X1,join(X3,meet(X2,complement(X1)))) = meet(X1,join(meet(X2,complement(X1)),meet(X3,join(X1,meet(X2,complement(X1)))))),
    inference(step,[status(thm)],[t711037,t102]) ).

cnf(t37026,plain,
    meet(X1,join(meet(X2,complement(X1)),meet(X3,join(X1,meet(X2,complement(X1)))))) = meet(X1,join(X3,meet(X2,complement(X1)))),
    inference(orient,[status(thm)],[t711038]) ).

cnf(t35181,plain,
    zero = meet(meet(X1,complement(X2)),complement(join(X1,X3))),
    inference(cp,[status(thm)],[t35155,t19612]) ).

cnf(t35380,plain,
    meet(meet(X1,complement(X2)),complement(join(X1,X3))) = zero,
    inference(orient,[status(thm)],[t35181]) ).

cnf(t35384,plain,
    zero = meet(meet(X1,X2),complement(join(X1,X3))),
    inference(cp,[status(thm)],[t35380,t479]) ).

cnf(t35466,plain,
    meet(meet(X1,X2),complement(join(X1,X3))) = zero,
    inference(orient,[status(thm)],[t35384]) ).

cnf(t35471,plain,
    zero = meet(meet(X1,X2),complement(join(X2,X3))),
    inference(cp,[status(thm)],[t35466,t51]) ).

cnf(t35557,plain,
    meet(meet(X1,X2),complement(join(X2,X3))) = zero,
    inference(orient,[status(thm)],[t35471]) ).

cnf(t35636,plain,
    zero = meet(meet(X1,X2),complement(join(join(X3,meet(X1,X2)),Y3))),
    inference(cp,[status(thm)],[t35557,t2521]) ).

cnf(t711079,plain,
    zero = meet(meet(X1,X2),complement(join(Y3,join(X3,meet(X1,X2))))),
    inference(step,[status(thm)],[t35636,t23]) ).

cnf(t711080,plain,
    zero = meet(meet(X1,X2),complement(join(X3,join(meet(X1,X2),Y3)))),
    inference(step,[status(thm)],[t711079,t26]) ).

cnf(t711081,plain,
    zero = meet(meet(X1,X2),complement(join(X3,join(Y3,meet(X1,X2))))),
    inference(step,[status(thm)],[t711080,t23]) ).

cnf(t40701,plain,
    meet(meet(X1,X2),complement(join(X3,join(Y3,meet(X1,X2))))) = zero,
    inference(orient,[status(thm)],[t711081]) ).

cnf(t40720,plain,
    zero = meet(meet(X1,join(X2,meet(X3,Y3))),complement(join(X2,X3))),
    inference(cp,[status(thm)],[t40701,t16118]) ).

cnf(t711210,plain,
    zero = meet(complement(join(X2,X3)),meet(X1,join(X2,meet(X3,Y3)))),
    inference(step,[status(thm)],[t40720,t51]) ).

cnf(t711211,plain,
    zero = meet(X1,meet(join(X2,meet(X3,Y3)),complement(join(X2,X3)))),
    inference(step,[status(thm)],[t711210,t67]) ).

cnf(t711212,plain,
    zero = meet(X1,meet(complement(join(X2,X3)),join(X2,meet(X3,Y3)))),
    inference(step,[status(thm)],[t711211,t51]) ).

cnf(t48185,plain,
    meet(X1,meet(complement(join(X2,X3)),join(X2,meet(X3,Y3)))) = zero,
    inference(orient,[status(thm)],[t711212]) ).

cnf(t48193,plain,
    zero = meet(complement(join(X1,X2)),join(X1,meet(X2,X3))),
    inference(cp,[status(thm)],[t48185,t125]) ).

cnf(t48491,plain,
    meet(complement(join(X1,X2)),join(X1,meet(X2,X3))) = zero,
    inference(orient,[status(thm)],[t48193]) ).

cnf(t48806,plain,
    meet(X1,join(complement(join(X1,X2)),meet(X2,complement(X1)))) = meet(X1,join(meet(X2,complement(X1)),zero)),
    inference(cp,[status(thm)],[t37026,t48491]) ).

cnf(t711225,plain,
    meet(X1,join(meet(X2,complement(X1)),complement(join(X1,X2)))) = meet(X1,join(meet(X2,complement(X1)),zero)),
    inference(step,[status(thm)],[t48806,t23]) ).

cnf(t711226,plain,
    meet(X1,join(meet(X2,complement(X1)),complement(join(X1,X2)))) = meet(X1,meet(X2,complement(X1))),
    inference(step,[status(thm)],[t711225,t102]) ).

cnf(t711227,plain,
    meet(X1,join(meet(X2,complement(X1)),complement(join(X1,X2)))) = zero,
    inference(step,[status(thm)],[t711226,t162]) ).

cnf(t49639,plain,
    meet(X1,join(meet(X2,complement(X1)),complement(join(X1,X2)))) = zero,
    inference(orient,[status(thm)],[t711227]) ).

cnf(t49642,plain,
    zero = meet(complement(X1),join(meet(X2,X1),complement(join(complement(X1),X2)))),
    inference(cp,[status(thm)],[t49639,t479]) ).

cnf(t711247,plain,
    zero = meet(complement(X1),join(meet(X1,X2),complement(join(complement(X1),X2)))),
    inference(step,[status(thm)],[t49642,t51]) ).

cnf(t711248,plain,
    zero = meet(complement(X1),join(meet(X1,X2),complement(join(X2,complement(X1))))),
    inference(step,[status(thm)],[t711247,t23]) ).

cnf(t51911,plain,
    meet(complement(X1),join(meet(X1,X2),complement(join(X2,complement(X1))))) = zero,
    inference(orient,[status(thm)],[t711248]) ).

cnf(t51966,plain,
    zero = meet(complement(X1),join(meet(X1,X2),complement(join(meet(X1,X2),complement(X1))))),
    inference(cp,[status(thm)],[t51911,t125]) ).

cnf(t713191,plain,
    zero = meet(complement(X1),join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2))))),
    inference(step,[status(thm)],[t51966,t23]) ).

cnf(t502547,plain,
    meet(complement(X1),join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2))))) = zero,
    inference(orient,[status(thm)],[t713191]) ).

cnf(t502867,plain,
    complement(X1) = ifeq(zero,zero,ifeq(join(complement(X1),join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2))))),one,complement(join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2))))),complement(X1)),complement(X1)),
    inference(cp,[status(thm)],[t448,t502547]) ).

cnf(t713192,plain,
    complement(X1) = ifeq(join(complement(X1),join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2))))),one,complement(join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2))))),complement(X1)),
    inference(step,[status(thm)],[t502867,t17]) ).

cnf(t18474,plain,
    one = join(X1,join(X2,complement(join(X1,X2)))),
    inference(cp,[status(thm)],[t18473,t17128]) ).

cnf(t18578,plain,
    join(X1,join(X2,complement(join(X1,X2)))) = one,
    inference(orient,[status(thm)],[t18474]) ).

cnf(t713193,plain,
    complement(X1) = ifeq(one,one,complement(join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2))))),complement(X1)),
    inference(step,[status(thm)],[t713192,t18578]) ).

cnf(t713194,plain,
    complement(X1) = complement(join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2))))),
    inference(step,[status(thm)],[t713193,t17]) ).

cnf(t503188,plain,
    complement(join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2))))) = complement(X1),
    inference(orient,[status(thm)],[t713194]) ).

cnf(t503437,plain,
    join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2)))) = complement(complement(X1)),
    inference(cp,[status(thm)],[t479,t503188]) ).

cnf(t713195,plain,
    join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2)))) = X1,
    inference(step,[status(thm)],[t503437,t479]) ).

cnf(t503797,plain,
    join(meet(X1,X2),complement(join(complement(X1),meet(X1,X2)))) = X1,
    inference(orient,[status(thm)],[t713195]) ).

cnf(t503835,plain,
    complement(X1) = join(meet(X2,complement(X1)),complement(join(complement(complement(X1)),meet(complement(X1),join(meet(X2,X3),meet(X2,complement(X1))))))),
    inference(cp,[status(thm)],[t503797,t162518]) ).

cnf(t713237,plain,
    complement(X1) = join(meet(X2,complement(X1)),complement(join(X1,meet(complement(X1),join(meet(X2,X3),meet(X2,complement(X1))))))),
    inference(step,[status(thm)],[t503835,t479]) ).

cnf(t713238,plain,
    complement(X1) = join(meet(X2,complement(X1)),complement(join(X1,meet(X2,complement(X1))))),
    inference(step,[status(thm)],[t713237,t162518]) ).

cnf(t524982,plain,
    join(meet(X1,complement(X2)),complement(join(X2,meet(X1,complement(X2))))) = complement(X2),
    inference(orient,[status(thm)],[t713238]) ).

cnf(t525411,plain,
    join(X1,complement(join(X2,meet(X1,complement(X2))))) = join(X1,complement(X2)),
    inference(cp,[status(thm)],[t53163,t524982]) ).

cnf(t525858,plain,
    join(X1,complement(join(X2,meet(X1,complement(X2))))) = join(X1,complement(X2)),
    inference(orient,[status(thm)],[t525411]) ).

cnf(t525860,plain,
    join(X1,complement(complement(X2))) = join(X1,complement(join(complement(X2),meet(X1,X2)))),
    inference(cp,[status(thm)],[t525858,t479]) ).

cnf(t713239,plain,
    join(X1,X2) = join(X1,complement(join(complement(X2),meet(X1,X2)))),
    inference(step,[status(thm)],[t525860,t479]) ).

cnf(t526272,plain,
    join(X1,complement(join(complement(X2),meet(X1,X2)))) = join(X1,X2),
    inference(orient,[status(thm)],[t713239]) ).

cnf(t526544,plain,
    X1 = ifeq(meet(X1,complement(join(complement(X2),meet(X1,X2)))),zero,ifeq(join(X1,X2),one,complement(complement(join(complement(X2),meet(X1,X2)))),X1),X1),
    inference(cp,[status(thm)],[t448,t526272]) ).

cnf(t35175,plain,
    zero = meet(meet(X1,meet(X2,X3)),complement(meet(X1,X2))),
    inference(cp,[status(thm)],[t35155,t13816]) ).

cnf(t711021,plain,
    zero = meet(complement(meet(X1,X2)),meet(X1,meet(X2,X3))),
    inference(step,[status(thm)],[t35175,t51]) ).

cnf(t711022,plain,
    zero = meet(meet(X2,X3),meet(complement(meet(X1,X2)),X1)),
    inference(step,[status(thm)],[t711021,t67]) ).

cnf(t711023,plain,
    zero = meet(X1,meet(meet(X2,X3),complement(meet(X1,X2)))),
    inference(step,[status(thm)],[t711022,t67]) ).

cnf(t35730,plain,
    meet(X1,meet(meet(X2,X3),complement(meet(X1,X2)))) = zero,
    inference(orient,[status(thm)],[t711023]) ).

cnf(t35774,plain,
    zero = meet(X1,meet(meet(X2,X3),complement(meet(X1,X3)))),
    inference(cp,[status(thm)],[t35730,t51]) ).

cnf(t36375,plain,
    meet(X1,meet(meet(X2,X3),complement(meet(X1,X3)))) = zero,
    inference(orient,[status(thm)],[t35774]) ).

cnf(t36528,plain,
    zero = meet(meet(X1,X2),meet(meet(X3,complement(join(Y3,meet(X1,X2)))),complement(zero))),
    inference(cp,[status(thm)],[t36375,t35155]) ).

cnf(t711120,plain,
    zero = meet(complement(zero),meet(meet(X1,X2),meet(X3,complement(join(Y3,meet(X1,X2)))))),
    inference(step,[status(thm)],[t36528,t67]) ).

cnf(t121,plain,
    one = ifeq(meet(X1,one),zero,ifeq(one,one,complement(X1),one),one),
    inference(cp,[status(thm)],[t18,t119]) ).

cnf(t710106,plain,
    one = ifeq(X1,zero,ifeq(one,one,complement(X1),one),one),
    inference(step,[status(thm)],[t121,t96]) ).

cnf(t710107,plain,
    one = ifeq(X1,zero,complement(X1),one),
    inference(step,[status(thm)],[t710106,t17]) ).

cnf(t142,plain,
    ifeq(X1,zero,complement(X1),one) = one,
    inference(orient,[status(thm)],[t710107]) ).

cnf(t143,plain,
    one = complement(zero),
    inference(cp,[status(thm)],[t142,t17]) ).

cnf(t144,plain,
    complement(zero) = one,
    inference(orient,[status(thm)],[t143]) ).

cnf(t711121,plain,
    zero = meet(one,meet(meet(X1,X2),meet(X3,complement(join(Y3,meet(X1,X2)))))),
    inference(step,[status(thm)],[t711120,t144]) ).

cnf(t711122,plain,
    zero = meet(one,meet(X3,meet(complement(join(Y3,meet(X1,X2))),meet(X1,X2)))),
    inference(step,[status(thm)],[t711121,t67]) ).

cnf(t711123,plain,
    zero = meet(X3,meet(meet(complement(join(Y3,meet(X1,X2))),meet(X1,X2)),one)),
    inference(step,[status(thm)],[t711122,t67]) ).

cnf(t711124,plain,
    zero = meet(X3,meet(complement(join(Y3,meet(X1,X2))),meet(X1,X2))),
    inference(step,[status(thm)],[t711123,t96]) ).

cnf(t711125,plain,
    zero = meet(X3,meet(X2,meet(complement(join(Y3,meet(X1,X2))),X1))),
    inference(step,[status(thm)],[t711124,t67]) ).

cnf(t711126,plain,
    zero = meet(X3,meet(X1,meet(X2,complement(join(Y3,meet(X1,X2)))))),
    inference(step,[status(thm)],[t711125,t67]) ).

cnf(t711127,plain,
    zero = meet(X1,meet(meet(X2,complement(join(Y3,meet(X1,X2)))),X3)),
    inference(step,[status(thm)],[t711126,t67]) ).

cnf(t711128,plain,
    zero = meet(X1,meet(X3,meet(X2,complement(join(Y3,meet(X1,X2)))))),
    inference(step,[status(thm)],[t711127,t51]) ).

cnf(t711129,plain,
    zero = meet(X1,meet(X2,meet(complement(join(Y3,meet(X1,X2))),X3))),
    inference(step,[status(thm)],[t711128,t67]) ).

cnf(t711130,plain,
    zero = meet(X1,meet(X2,meet(X3,complement(join(Y3,meet(X1,X2)))))),
    inference(step,[status(thm)],[t711129,t51]) ).

cnf(t43298,plain,
    meet(X1,meet(X2,meet(X3,complement(join(Y3,meet(X1,X2)))))) = zero,
    inference(orient,[status(thm)],[t711130]) ).

cnf(t43300,plain,
    zero = meet(X1,meet(meet(X2,complement(join(X3,meet(Y3,X1)))),Y3)),
    inference(cp,[status(thm)],[t43298,t67]) ).

cnf(t711236,plain,
    zero = meet(X1,meet(Y3,meet(X2,complement(join(X3,meet(Y3,X1)))))),
    inference(step,[status(thm)],[t43300,t51]) ).

cnf(t711237,plain,
    zero = meet(X1,meet(X2,meet(complement(join(X3,meet(Y3,X1))),Y3))),
    inference(step,[status(thm)],[t711236,t67]) ).

cnf(t711238,plain,
    zero = meet(X1,meet(X2,meet(Y3,complement(join(X3,meet(Y3,X1)))))),
    inference(step,[status(thm)],[t711237,t51]) ).

cnf(t711239,plain,
    zero = meet(X1,meet(X2,meet(Y3,complement(join(X3,meet(X1,Y3)))))),
    inference(step,[status(thm)],[t711238,t51]) ).

cnf(t50417,plain,
    meet(X1,meet(X2,meet(X3,complement(join(Y3,meet(X1,X3)))))) = zero,
    inference(orient,[status(thm)],[t711239]) ).

cnf(t50419,plain,
    zero = meet(X1,meet(X2,complement(join(X3,meet(X1,join(X2,Y3)))))),
    inference(cp,[status(thm)],[t50417,t34093]) ).

cnf(t52512,plain,
    meet(X1,meet(X2,complement(join(X3,meet(X1,join(X2,Y3)))))) = zero,
    inference(orient,[status(thm)],[t50419]) ).

cnf(t52514,plain,
    zero = meet(X1,meet(complement(join(X2,meet(X3,join(X1,Y3)))),X3)),
    inference(cp,[status(thm)],[t52512,t67]) ).

cnf(t711253,plain,
    zero = meet(X1,meet(X3,complement(join(X2,meet(X3,join(X1,Y3)))))),
    inference(step,[status(thm)],[t52514,t51]) ).

cnf(t53035,plain,
    meet(X1,meet(X2,complement(join(X3,meet(X2,join(X1,Y3)))))) = zero,
    inference(orient,[status(thm)],[t711253]) ).

cnf(t504044,plain,
    complement(join(complement(X1),meet(X1,X2))) = meet(complement(join(complement(X1),meet(X1,X2))),X1),
    inference(cp,[status(thm)],[t179822,t503797]) ).

cnf(t713204,plain,
    complement(join(complement(X1),meet(X1,X2))) = meet(X1,complement(join(complement(X1),meet(X1,X2)))),
    inference(step,[status(thm)],[t504044,t51]) ).

cnf(t510332,plain,
    meet(X1,complement(join(complement(X1),meet(X1,X2)))) = complement(join(complement(X1),meet(X1,X2))),
    inference(orient,[status(thm)],[t713204]) ).

cnf(t511078,plain,
    zero = meet(X1,complement(join(complement(X2),meet(X2,join(X1,X3))))),
    inference(cp,[status(thm)],[t53035,t510332]) ).

cnf(t511119,plain,
    meet(X1,complement(join(complement(X2),meet(X2,join(X1,X3))))) = zero,
    inference(orient,[status(thm)],[t511078]) ).

cnf(t511233,plain,
    zero = meet(X1,complement(join(complement(X2),meet(X2,X1)))),
    inference(cp,[status(thm)],[t511119,t13]) ).

cnf(t713205,plain,
    zero = meet(X1,complement(join(complement(X2),meet(X1,X2)))),
    inference(step,[status(thm)],[t511233,t51]) ).

cnf(t511895,plain,
    meet(X1,complement(join(complement(X2),meet(X1,X2)))) = zero,
    inference(orient,[status(thm)],[t713205]) ).

cnf(t713243,plain,
    X1 = ifeq(zero,zero,ifeq(join(X1,X2),one,complement(complement(join(complement(X2),meet(X1,X2)))),X1),X1),
    inference(step,[status(thm)],[t526544,t511895]) ).

cnf(t713244,plain,
    X1 = ifeq(join(X1,X2),one,complement(complement(join(complement(X2),meet(X1,X2)))),X1),
    inference(step,[status(thm)],[t713243,t17]) ).

cnf(t713245,plain,
    X1 = ifeq(join(X1,X2),one,join(complement(X2),meet(X1,X2)),X1),
    inference(step,[status(thm)],[t713244,t479]) ).

cnf(t528402,plain,
    ifeq(join(X1,X2),one,join(complement(X2),meet(X1,X2)),X1) = X1,
    inference(orient,[status(thm)],[t713245]) ).

cnf(t33,plain,
    join(X1,X2) = ifeq(meet(X3,join(X1,X2)),zero,ifeq(join(X2,join(X3,X1)),one,complement(X3),join(X1,X2)),join(X1,X2)),
    inference(cp,[status(thm)],[t18,t26]) ).

cnf(t710419,plain,
    join(X1,X2) = ifeq(meet(X3,join(X1,X2)),zero,ifeq(join(X1,join(X2,X3)),one,complement(X3),join(X1,X2)),join(X1,X2)),
    inference(step,[status(thm)],[t33,t26]) ).

cnf(t2422,plain,
    ifeq(meet(X1,join(X2,X3)),zero,ifeq(join(X2,join(X3,X1)),one,complement(X1),join(X2,X3)),join(X2,X3)) = join(X2,X3),
    inference(orient,[status(thm)],[t710419]) ).

cnf(t481,plain,
    one = ifeq(complement(X1),zero,X1,one),
    inference(cp,[status(thm)],[t142,t479]) ).

cnf(t496,plain,
    ifeq(complement(X1),zero,X1,one) = one,
    inference(orient,[status(thm)],[t481]) ).

cnf(t48531,plain,
    zero = meet(complement(join(X1,X2)),join(X2,meet(X1,X3))),
    inference(cp,[status(thm)],[t48491,t23]) ).

cnf(t48833,plain,
    meet(complement(join(X1,X2)),join(X2,meet(X1,X3))) = zero,
    inference(orient,[status(thm)],[t48531]) ).

cnf(t177106,plain,
    zero = meet(complement(join(join(X1,X2),X3)),join(X3,meet(Y3,X1))),
    inference(cp,[status(thm)],[t48833,t176628]) ).

cnf(t711909,plain,
    zero = meet(join(X3,meet(Y3,X1)),complement(join(join(X1,X2),X3))),
    inference(step,[status(thm)],[t177106,t51]) ).

cnf(t711910,plain,
    zero = meet(join(X3,meet(X1,Y3)),complement(join(join(X1,X2),X3))),
    inference(step,[status(thm)],[t711909,t51]) ).

cnf(t711911,plain,
    zero = meet(join(X3,meet(X1,Y3)),complement(join(X3,join(X1,X2)))),
    inference(step,[status(thm)],[t711910,t23]) ).

cnf(t711912,plain,
    zero = meet(join(X3,meet(X1,Y3)),complement(join(X2,join(X3,X1)))),
    inference(step,[status(thm)],[t711911,t26]) ).

cnf(t711913,plain,
    zero = meet(join(X3,meet(X1,Y3)),complement(join(X1,join(X2,X3)))),
    inference(step,[status(thm)],[t711912,t26]) ).

cnf(t184710,plain,
    meet(join(X1,meet(X2,X3)),complement(join(X2,join(Y3,X1)))) = zero,
    inference(orient,[status(thm)],[t711913]) ).

cnf(t182453,plain,
    join(meet(X1,X2),meet(X2,X2)) = meet(X2,join(meet(X1,X2),X2)),
    inference(cp,[status(thm)],[t182205,t15]) ).

cnf(t711899,plain,
    join(meet(X1,X2),X2) = meet(X2,join(meet(X1,X2),X2)),
    inference(step,[status(thm)],[t182453,t15]) ).

cnf(t711900,plain,
    join(X2,meet(X1,X2)) = meet(X2,join(meet(X1,X2),X2)),
    inference(step,[status(thm)],[t711899,t23]) ).

cnf(t711901,plain,
    join(X2,meet(X1,X2)) = X2,
    inference(step,[status(thm)],[t711900,t179822]) ).

cnf(t183205,plain,
    join(X1,meet(X2,X1)) = X1,
    inference(orient,[status(thm)],[t711901]) ).

cnf(t185084,plain,
    zero = meet(join(meet(X1,X2),meet(X3,Y3)),complement(join(X3,X2))),
    inference(cp,[status(thm)],[t184710,t183205]) ).

cnf(t711917,plain,
    zero = meet(complement(join(X3,X2)),join(meet(X1,X2),meet(X3,Y3))),
    inference(step,[status(thm)],[t185084,t51]) ).

cnf(t711918,plain,
    zero = meet(complement(join(X2,X3)),join(meet(X1,X2),meet(X3,Y3))),
    inference(step,[status(thm)],[t711917,t23]) ).

cnf(t187972,plain,
    meet(complement(join(X1,X2)),join(meet(X3,X1),meet(X2,Y3))) = zero,
    inference(orient,[status(thm)],[t711918]) ).

cnf(t188818,plain,
    zero = meet(complement(join(meet(X1,X2),meet(X3,Y3))),join(meet(X1,X2),zero)),
    inference(cp,[status(thm)],[t45279,t187972]) ).

cnf(t711937,plain,
    zero = meet(complement(join(meet(X1,X2),meet(X3,Y3))),meet(X1,X2)),
    inference(step,[status(thm)],[t188818,t102]) ).

cnf(t711938,plain,
    zero = meet(X2,meet(complement(join(meet(X1,X2),meet(X3,Y3))),X1)),
    inference(step,[status(thm)],[t711937,t67]) ).

cnf(t711939,plain,
    zero = meet(X1,meet(X2,complement(join(meet(X1,X2),meet(X3,Y3))))),
    inference(step,[status(thm)],[t711938,t67]) ).

cnf(t192956,plain,
    meet(X1,meet(X2,complement(join(meet(X1,X2),meet(X3,Y3))))) = zero,
    inference(orient,[status(thm)],[t711939]) ).

cnf(t193261,plain,
    zero = meet(X1,meet(X2,complement(join(meet(X1,X2),join(X3,Y3))))),
    inference(cp,[status(thm)],[t192956,t2060]) ).

cnf(t711948,plain,
    zero = meet(X1,meet(X2,complement(join(Y3,join(meet(X1,X2),X3))))),
    inference(step,[status(thm)],[t193261,t26]) ).

cnf(t711949,plain,
    zero = meet(X1,meet(X2,complement(join(X3,join(Y3,meet(X1,X2)))))),
    inference(step,[status(thm)],[t711948,t26]) ).

cnf(t195356,plain,
    meet(X1,meet(X2,complement(join(X3,join(Y3,meet(X1,X2)))))) = zero,
    inference(orient,[status(thm)],[t711949]) ).

cnf(t504487,plain,
    join(X1,complement(join(complement(X1),meet(X1,X2)))) = join(X1,X1),
    inference(cp,[status(thm)],[t53163,t503797]) ).

cnf(t713197,plain,
    join(X1,complement(join(complement(X1),meet(X1,X2)))) = X1,
    inference(step,[status(thm)],[t504487,t13]) ).

cnf(t504968,plain,
    join(X1,complement(join(complement(X1),meet(X1,X2)))) = X1,
    inference(orient,[status(thm)],[t713197]) ).

cnf(t504978,plain,
    complement(X1) = join(complement(X1),complement(join(X1,meet(complement(X1),X2)))),
    inference(cp,[status(thm)],[t504968,t479]) ).

cnf(t713198,plain,
    complement(X1) = join(complement(X1),complement(join(X1,meet(X2,complement(X1))))),
    inference(step,[status(thm)],[t504978,t51]) ).

cnf(t505787,plain,
    join(complement(X1),complement(join(X1,meet(X2,complement(X1))))) = complement(X1),
    inference(orient,[status(thm)],[t713198]) ).

cnf(t528614,plain,
    X1 = ifeq(one,one,join(complement(complement(meet(X1,X2))),meet(X1,complement(meet(X1,X2)))),X1),
    inference(cp,[status(thm)],[t528402,t20070]) ).

cnf(t713246,plain,
    X1 = join(complement(complement(meet(X1,X2))),meet(X1,complement(meet(X1,X2)))),
    inference(step,[status(thm)],[t528614,t17]) ).

cnf(t713247,plain,
    X1 = join(meet(X1,X2),meet(X1,complement(meet(X1,X2)))),
    inference(step,[status(thm)],[t713246,t479]) ).

cnf(t529400,plain,
    join(meet(X1,X2),meet(X1,complement(meet(X1,X2)))) = X1,
    inference(orient,[status(thm)],[t713247]) ).

cnf(t530066,plain,
    complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(X1)),
    inference(cp,[status(thm)],[t505787,t529400]) ).

cnf(t713248,plain,
    complement(meet(X1,X2)) = join(complement(X1),complement(meet(X1,X2))),
    inference(step,[status(thm)],[t530066,t23]) ).

cnf(t530434,plain,
    join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
    inference(orient,[status(thm)],[t713248]) ).

cnf(t181768,plain,
    meet(X1,X2) = meet(X2,join(meet(X1,X2),join(meet(X1,X3),meet(X1,Y3)))),
    inference(cp,[status(thm)],[t163258,t181587]) ).

cnf(t331015,plain,
    meet(X1,join(meet(X2,X1),join(meet(X2,X3),meet(X2,Y3)))) = meet(X2,X1),
    inference(orient,[status(thm)],[t181768]) ).

cnf(t530441,plain,
    complement(meet(X1,join(meet(X2,X1),join(meet(X2,X3),meet(X2,Y3))))) = join(complement(X1),complement(meet(X2,X1))),
    inference(cp,[status(thm)],[t530434,t331015]) ).

cnf(t713251,plain,
    complement(meet(X2,X1)) = join(complement(X1),complement(meet(X2,X1))),
    inference(step,[status(thm)],[t530441,t331015]) ).

cnf(t532560,plain,
    join(complement(X1),complement(meet(X2,X1))) = complement(meet(X2,X1)),
    inference(orient,[status(thm)],[t713251]) ).

cnf(t532584,plain,
    complement(meet(X1,join(X2,X1))) = join(complement(join(X2,X1)),complement(X1)),
    inference(cp,[status(thm)],[t532560,t179822]) ).

cnf(t713252,plain,
    complement(X1) = join(complement(join(X2,X1)),complement(X1)),
    inference(step,[status(thm)],[t532584,t179822]) ).

cnf(t713253,plain,
    complement(X1) = join(complement(X1),complement(join(X2,X1))),
    inference(step,[status(thm)],[t713252,t23]) ).

cnf(t713254,plain,
    complement(X1) = join(complement(X1),complement(join(X1,X2))),
    inference(step,[status(thm)],[t713253,t23]) ).

cnf(t533435,plain,
    join(complement(X1),complement(join(X1,X2))) = complement(X1),
    inference(orient,[status(thm)],[t713254]) ).

cnf(t533476,plain,
    complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X1)),
    inference(cp,[status(thm)],[t179822,t533435]) ).

cnf(t713257,plain,
    complement(join(X1,X2)) = meet(complement(X1),complement(join(X1,X2))),
    inference(step,[status(thm)],[t533476,t51]) ).

cnf(t534796,plain,
    meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
    inference(orient,[status(thm)],[t713257]) ).

cnf(t535451,plain,
    zero = meet(X1,complement(join(X2,join(X3,meet(X1,complement(X2)))))),
    inference(cp,[status(thm)],[t195356,t534796]) ).

cnf(t599186,plain,
    meet(X1,complement(join(X2,join(X3,meet(X1,complement(X2)))))) = zero,
    inference(orient,[status(thm)],[t535451]) ).

cnf(t599191,plain,
    zero = meet(X1,complement(join(X2,join(meet(X1,complement(X3)),X3)))),
    inference(cp,[status(thm)],[t599186,t26]) ).

cnf(t713425,plain,
    zero = meet(X1,complement(join(X2,join(X3,meet(X1,complement(X3)))))),
    inference(step,[status(thm)],[t599191,t23]) ).

cnf(t618914,plain,
    meet(X1,complement(join(X2,join(X3,meet(X1,complement(X3)))))) = zero,
    inference(orient,[status(thm)],[t713425]) ).

cnf(t618917,plain,
    zero = complement(join(X1,join(X2,meet(complement(X1),complement(X2))))),
    inference(cp,[status(thm)],[t618914,t534796]) ).

cnf(t619332,plain,
    complement(join(X1,join(X2,meet(complement(X1),complement(X2))))) = zero,
    inference(orient,[status(thm)],[t618917]) ).

cnf(t619373,plain,
    one = ifeq(zero,zero,join(X1,join(X2,meet(complement(X1),complement(X2)))),one),
    inference(cp,[status(thm)],[t496,t619332]) ).

cnf(t713426,plain,
    one = join(X1,join(X2,meet(complement(X1),complement(X2)))),
    inference(step,[status(thm)],[t619373,t17]) ).

cnf(t619637,plain,
    join(X1,join(X2,meet(complement(X1),complement(X2)))) = one,
    inference(orient,[status(thm)],[t713426]) ).

cnf(t619648,plain,
    one = join(X1,join(join(complement(X2),meet(complement(X1),X2)),zero)),
    inference(cp,[status(thm)],[t619637,t511895]) ).

cnf(t713429,plain,
    one = join(X1,join(complement(X2),meet(complement(X1),X2))),
    inference(step,[status(thm)],[t619648,t102]) ).

cnf(t713430,plain,
    one = join(X1,join(complement(X2),meet(X2,complement(X1)))),
    inference(step,[status(thm)],[t713429,t51]) ).

cnf(t623334,plain,
    join(X1,join(complement(X2),meet(X2,complement(X1)))) = one,
    inference(orient,[status(thm)],[t713430]) ).

cnf(t623656,plain,
    join(X1,complement(X2)) = ifeq(meet(meet(X2,complement(X1)),join(X1,complement(X2))),zero,ifeq(one,one,complement(meet(X2,complement(X1))),join(X1,complement(X2))),join(X1,complement(X2))),
    inference(cp,[status(thm)],[t2422,t623334]) ).

cnf(t2614,plain,
    meet(X1,meet(join(X2,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
    inference(cp,[status(thm)],[t67,t2566]) ).

cnf(t710428,plain,
    meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
    inference(step,[status(thm)],[t2614,t51]) ).

cnf(t710429,plain,
    meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
    inference(step,[status(thm)],[t710428,t67]) ).

cnf(t710430,plain,
    meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
    inference(step,[status(thm)],[t710429,t67]) ).

cnf(t2616,plain,
    meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
    inference(orient,[status(thm)],[t710430]) ).

cnf(t60996,plain,
    meet(meet(X1,X2),join(X3,meet(X1,X3))) = meet(X1,meet(X3,meet(X1,X2))),
    inference(cp,[status(thm)],[t60989,t2616]) ).

cnf(t711301,plain,
    meet(meet(X1,X2),join(X3,meet(X1,X3))) = meet(X1,meet(X2,meet(X3,X1))),
    inference(step,[status(thm)],[t60996,t67]) ).

cnf(t711302,plain,
    meet(meet(X1,X2),join(X3,meet(X1,X3))) = meet(X1,meet(X1,meet(X2,X3))),
    inference(step,[status(thm)],[t711301,t67]) ).

cnf(t711303,plain,
    meet(meet(X1,X2),join(X3,meet(X1,X3))) = meet(X1,meet(X2,X3)),
    inference(step,[status(thm)],[t711302,t125]) ).

cnf(t62132,plain,
    meet(meet(X1,X2),join(X3,meet(X1,X3))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t711303]) ).

cnf(t150564,plain,
    meet(meet(X1,X2),join(X3,meet(X1,X3))) = meet(meet(X1,X2),join(X3,meet(X1,meet(X2,X3)))),
    inference(cp,[status(thm)],[t150515,t62132]) ).

cnf(t711825,plain,
    meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(X3,meet(X1,meet(X2,X3)))),
    inference(step,[status(thm)],[t150564,t62132]) ).

cnf(t154981,plain,
    meet(meet(X1,X2),join(X3,meet(X1,meet(X2,X3)))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t711825]) ).

cnf(t138,plain,
    zero = ifeq(zero,zero,ifeq(join(X1,zero),one,complement(X1),zero),zero),
    inference(cp,[status(thm)],[t18,t136]) ).

cnf(t710108,plain,
    zero = ifeq(join(X1,zero),one,complement(X1),zero),
    inference(step,[status(thm)],[t138,t17]) ).

cnf(t710109,plain,
    zero = ifeq(X1,one,complement(X1),zero),
    inference(step,[status(thm)],[t710108,t102]) ).

cnf(t146,plain,
    ifeq(X1,one,complement(X1),zero) = zero,
    inference(orient,[status(thm)],[t710109]) ).

cnf(t480,plain,
    zero = ifeq(complement(X1),one,X1,zero),
    inference(cp,[status(thm)],[t146,t479]) ).

cnf(t495,plain,
    ifeq(complement(X1),one,X1,zero) = zero,
    inference(orient,[status(thm)],[t480]) ).

cnf(t26853,plain,
    one = join(complement(meet(X1,X2)),meet(X1,join(meet(X1,X2),X3))),
    inference(cp,[status(thm)],[t26805,t125]) ).

cnf(t710966,plain,
    one = join(complement(meet(X1,X2)),meet(X1,join(X3,meet(X1,X2)))),
    inference(step,[status(thm)],[t26853,t23]) ).

cnf(t30809,plain,
    join(complement(meet(X1,X2)),meet(X1,join(X3,meet(X1,X2)))) = one,
    inference(orient,[status(thm)],[t710966]) ).

cnf(t26896,plain,
    one = join(complement(meet(X1,X2)),meet(X2,join(X1,X3))),
    inference(cp,[status(thm)],[t26805,t51]) ).

cnf(t27122,plain,
    join(complement(meet(X1,X2)),meet(X2,join(X1,X3))) = one,
    inference(orient,[status(thm)],[t26896]) ).

cnf(t177088,plain,
    meet(join(X1,X2),X3) = meet(X3,join(meet(join(X1,X2),X3),meet(Y3,X1))),
    inference(cp,[status(thm)],[t163258,t176628]) ).

cnf(t711964,plain,
    meet(X3,join(X1,X2)) = meet(X3,join(meet(join(X1,X2),X3),meet(Y3,X1))),
    inference(step,[status(thm)],[t177088,t51]) ).

cnf(t711965,plain,
    meet(X3,join(X1,X2)) = meet(X3,join(meet(Y3,X1),meet(join(X1,X2),X3))),
    inference(step,[status(thm)],[t711964,t23]) ).

cnf(t711966,plain,
    meet(X3,join(X1,X2)) = meet(X3,join(meet(X1,Y3),meet(join(X1,X2),X3))),
    inference(step,[status(thm)],[t711965,t51]) ).

cnf(t711967,plain,
    meet(X3,join(X1,X2)) = meet(X3,join(meet(X1,Y3),meet(X3,join(X1,X2)))),
    inference(step,[status(thm)],[t711966,t51]) ).

cnf(t200288,plain,
    meet(X1,join(meet(X2,X3),meet(X1,join(X2,Y3)))) = meet(X1,join(X2,Y3)),
    inference(orient,[status(thm)],[t711967]) ).

cnf(t200470,plain,
    one = join(complement(meet(meet(X1,X2),X3)),meet(X3,join(X1,Y3))),
    inference(cp,[status(thm)],[t27122,t200288]) ).

cnf(t711968,plain,
    one = join(meet(X3,join(X1,Y3)),complement(meet(meet(X1,X2),X3))),
    inference(step,[status(thm)],[t200470,t23]) ).

cnf(t711969,plain,
    one = join(meet(X3,join(X1,Y3)),complement(meet(X3,meet(X1,X2)))),
    inference(step,[status(thm)],[t711968,t51]) ).

cnf(t711970,plain,
    one = join(meet(X3,join(X1,Y3)),complement(meet(X2,meet(X3,X1)))),
    inference(step,[status(thm)],[t711969,t67]) ).

cnf(t711971,plain,
    one = join(meet(X3,join(X1,Y3)),complement(meet(X1,meet(X2,X3)))),
    inference(step,[status(thm)],[t711970,t67]) ).

cnf(t200742,plain,
    join(meet(X1,join(X2,X3)),complement(meet(X2,meet(Y3,X1)))) = one,
    inference(orient,[status(thm)],[t711971]) ).

cnf(t201124,plain,
    one = join(meet(join(X1,X2),join(X3,Y3)),complement(meet(X3,X2))),
    inference(cp,[status(thm)],[t200742,t179822]) ).

cnf(t711972,plain,
    one = join(complement(meet(X3,X2)),meet(join(X1,X2),join(X3,Y3))),
    inference(step,[status(thm)],[t201124,t23]) ).

cnf(t711973,plain,
    one = join(complement(meet(X2,X3)),meet(join(X1,X2),join(X3,Y3))),
    inference(step,[status(thm)],[t711972,t51]) ).

cnf(t201462,plain,
    join(complement(meet(X1,X2)),meet(join(X3,X1),join(X2,Y3))) = one,
    inference(orient,[status(thm)],[t711973]) ).

cnf(t202265,plain,
    one = join(complement(meet(join(X1,X2),join(X3,Y3))),meet(join(X1,X2),one)),
    inference(cp,[status(thm)],[t30809,t201462]) ).

cnf(t711987,plain,
    one = join(complement(meet(join(X1,X2),join(X3,Y3))),join(X1,X2)),
    inference(step,[status(thm)],[t202265,t96]) ).

cnf(t711988,plain,
    one = join(X2,join(complement(meet(join(X1,X2),join(X3,Y3))),X1)),
    inference(step,[status(thm)],[t711987,t26]) ).

cnf(t711989,plain,
    one = join(X1,join(X2,complement(meet(join(X1,X2),join(X3,Y3))))),
    inference(step,[status(thm)],[t711988,t26]) ).

cnf(t205093,plain,
    join(X1,join(X2,complement(meet(join(X1,X2),join(X3,Y3))))) = one,
    inference(orient,[status(thm)],[t711989]) ).

cnf(t205323,plain,
    one = join(X1,join(X2,complement(meet(join(X1,X2),meet(X3,Y3))))),
    inference(cp,[status(thm)],[t205093,t13816]) ).

cnf(t711995,plain,
    one = join(X1,join(X2,complement(meet(Y3,meet(join(X1,X2),X3))))),
    inference(step,[status(thm)],[t205323,t67]) ).

cnf(t711996,plain,
    one = join(X1,join(X2,complement(meet(X3,meet(Y3,join(X1,X2)))))),
    inference(step,[status(thm)],[t711995,t67]) ).

cnf(t206268,plain,
    join(X1,join(X2,complement(meet(X3,meet(Y3,join(X1,X2)))))) = one,
    inference(orient,[status(thm)],[t711996]) ).

cnf(t531109,plain,
    one = join(X1,complement(meet(X2,meet(X3,join(X1,complement(X2)))))),
    inference(cp,[status(thm)],[t206268,t530434]) ).

cnf(t594538,plain,
    join(X1,complement(meet(X2,meet(X3,join(X1,complement(X2)))))) = one,
    inference(orient,[status(thm)],[t531109]) ).

cnf(t594542,plain,
    one = join(X1,complement(meet(X2,meet(join(X1,complement(X3)),X3)))),
    inference(cp,[status(thm)],[t594538,t67]) ).

cnf(t713406,plain,
    one = join(X1,complement(meet(X2,meet(X3,join(X1,complement(X3)))))),
    inference(step,[status(thm)],[t594542,t51]) ).

cnf(t612122,plain,
    join(X1,complement(meet(X2,meet(X3,join(X1,complement(X3)))))) = one,
    inference(orient,[status(thm)],[t713406]) ).

cnf(t612124,plain,
    one = complement(meet(X1,meet(X2,join(complement(X1),complement(X2))))),
    inference(cp,[status(thm)],[t612122,t530434]) ).

cnf(t612555,plain,
    complement(meet(X1,meet(X2,join(complement(X1),complement(X2))))) = one,
    inference(orient,[status(thm)],[t612124]) ).

cnf(t612596,plain,
    zero = ifeq(one,one,meet(X1,meet(X2,join(complement(X1),complement(X2)))),zero),
    inference(cp,[status(thm)],[t495,t612555]) ).

cnf(t713407,plain,
    zero = meet(X1,meet(X2,join(complement(X1),complement(X2)))),
    inference(step,[status(thm)],[t612596,t17]) ).

cnf(t612895,plain,
    meet(X1,meet(X2,join(complement(X1),complement(X2)))) = zero,
    inference(orient,[status(thm)],[t713407]) ).

cnf(t22899,plain,
    one = join(complement(meet(X1,join(X2,X3))),join(X2,join(X3,Y3))),
    inference(cp,[status(thm)],[t22898,t23]) ).

cnf(t710865,plain,
    one = join(join(X3,Y3),join(complement(meet(X1,join(X2,X3))),X2)),
    inference(step,[status(thm)],[t22899,t26]) ).

cnf(t710866,plain,
    one = join(X2,join(join(X3,Y3),complement(meet(X1,join(X2,X3))))),
    inference(step,[status(thm)],[t710865,t26]) ).

cnf(t25084,plain,
    join(X1,join(join(X2,X3),complement(meet(Y3,join(X1,X2))))) = one,
    inference(orient,[status(thm)],[t710866]) ).

cnf(t25088,plain,
    one = join(X1,join(X2,complement(meet(X3,join(X1,X2))))),
    inference(cp,[status(thm)],[t25084,t13]) ).

cnf(t25304,plain,
    join(X1,join(X2,complement(meet(X3,join(X1,X2))))) = one,
    inference(orient,[status(thm)],[t25088]) ).

cnf(t531047,plain,
    one = join(X1,complement(meet(X2,join(X1,complement(X2))))),
    inference(cp,[status(thm)],[t25304,t530434]) ).

cnf(t537610,plain,
    join(X1,complement(meet(X2,join(X1,complement(X2))))) = one,
    inference(orient,[status(thm)],[t531047]) ).

cnf(t537623,plain,
    one = join(X1,complement(meet(complement(X2),join(X1,X2)))),
    inference(cp,[status(thm)],[t537610,t479]) ).

cnf(t542501,plain,
    join(X1,complement(meet(complement(X2),join(X1,X2)))) = one,
    inference(orient,[status(thm)],[t537623]) ).

cnf(t612907,plain,
    zero = meet(X1,meet(meet(complement(X2),join(complement(X1),X2)),one)),
    inference(cp,[status(thm)],[t612895,t542501]) ).

cnf(t713408,plain,
    zero = meet(X1,meet(complement(X2),join(complement(X1),X2))),
    inference(step,[status(thm)],[t612907,t96]) ).

cnf(t713409,plain,
    zero = meet(X1,meet(complement(X2),join(X2,complement(X1)))),
    inference(step,[status(thm)],[t713408,t23]) ).

cnf(t613235,plain,
    meet(X1,meet(complement(X2),join(X2,complement(X1)))) = zero,
    inference(orient,[status(thm)],[t713409]) ).

cnf(t613476,plain,
    meet(X1,meet(complement(X2),join(X2,complement(X1)))) = meet(meet(X1,complement(X2)),join(join(X2,complement(X1)),zero)),
    inference(cp,[status(thm)],[t154981,t613235]) ).

cnf(t713417,plain,
    zero = meet(meet(X1,complement(X2)),join(join(X2,complement(X1)),zero)),
    inference(step,[status(thm)],[t613476,t613235]) ).

cnf(t713418,plain,
    zero = meet(meet(X1,complement(X2)),join(X2,complement(X1))),
    inference(step,[status(thm)],[t713417,t102]) ).

cnf(t615035,plain,
    meet(meet(X1,complement(X2)),join(X2,complement(X1))) = zero,
    inference(orient,[status(thm)],[t713418]) ).

cnf(t713431,plain,
    join(X1,complement(X2)) = ifeq(zero,zero,ifeq(one,one,complement(meet(X2,complement(X1))),join(X1,complement(X2))),join(X1,complement(X2))),
    inference(step,[status(thm)],[t623656,t615035]) ).

cnf(t713432,plain,
    join(X1,complement(X2)) = ifeq(one,one,complement(meet(X2,complement(X1))),join(X1,complement(X2))),
    inference(step,[status(thm)],[t713431,t17]) ).

cnf(t713433,plain,
    join(X1,complement(X2)) = complement(meet(X2,complement(X1))),
    inference(step,[status(thm)],[t713432,t17]) ).

cnf(t623804,plain,
    complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
    inference(orient,[status(thm)],[t713433]) ).

cnf(t623932,plain,
    meet(X1,complement(X2)) = complement(join(X2,complement(X1))),
    inference(cp,[status(thm)],[t479,t623804]) ).

cnf(t625580,plain,
    complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
    inference(orient,[status(thm)],[t623932]) ).

cnf(t625603,plain,
    meet(join(complement(X1),meet(X2,X1)),complement(X2)) = complement(join(X2,X1)),
    inference(cp,[status(thm)],[t625580,t526272]) ).

cnf(t713569,plain,
    meet(complement(X2),join(complement(X1),meet(X2,X1))) = complement(join(X2,X1)),
    inference(step,[status(thm)],[t625603,t51]) ).

cnf(t713570,plain,
    meet(complement(X2),join(complement(X1),meet(X1,X2))) = complement(join(X2,X1)),
    inference(step,[status(thm)],[t713569,t51]) ).

cnf(t713571,plain,
    meet(complement(X2),join(complement(X1),meet(X1,X2))) = complement(join(X1,X2)),
    inference(step,[status(thm)],[t713570,t23]) ).

cnf(t631435,plain,
    meet(complement(X1),join(complement(X2),meet(X2,X1))) = complement(join(X2,X1)),
    inference(orient,[status(thm)],[t713571]) ).

cnf(t625660,plain,
    meet(complement(X1),complement(X2)) = complement(join(X2,X1)),
    inference(cp,[status(thm)],[t625580,t479]) ).

cnf(t713495,plain,
    meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
    inference(step,[status(thm)],[t625660,t23]) ).

cnf(t626212,plain,
    meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
    inference(orient,[status(thm)],[t713495]) ).

cnf(t631760,plain,
    complement(join(complement(X1),complement(X2))) = meet(complement(complement(X2)),join(complement(complement(X1)),complement(join(X1,X2)))),
    inference(cp,[status(thm)],[t631435,t626212]) ).

cnf(t632818,plain,
    meet(X1,join(X2,complement(join(X1,X2)))) = meet(X1,X2),
    inference(orient,[status(thm)],[t631760]) ).

cnf(t632991,plain,
    X1 = ifeq(join(X1,join(X2,complement(join(X1,X2)))),one,join(complement(join(X2,complement(join(X1,X2)))),meet(X1,X2)),X1),
    inference(cp,[status(thm)],[t528402,t632818]) ).

cnf(t713572,plain,
    X1 = ifeq(one,one,join(complement(join(X2,complement(join(X1,X2)))),meet(X1,X2)),X1),
    inference(step,[status(thm)],[t632991,t18578]) ).

cnf(t713573,plain,
    X1 = join(complement(join(X2,complement(join(X1,X2)))),meet(X1,X2)),
    inference(step,[status(thm)],[t713572,t17]) ).

cnf(t713574,plain,
    X1 = join(meet(X1,X2),complement(join(X2,complement(join(X1,X2))))),
    inference(step,[status(thm)],[t713573,t23]) ).

cnf(t713575,plain,
    X1 = join(meet(X1,X2),meet(join(X1,X2),complement(X2))),
    inference(step,[status(thm)],[t713574,t625580]) ).

cnf(t713576,plain,
    X1 = join(meet(X1,X2),meet(complement(X2),join(X1,X2))),
    inference(step,[status(thm)],[t713575,t51]) ).

cnf(t633569,plain,
    join(meet(X1,X2),meet(complement(X2),join(X1,X2))) = X1,
    inference(orient,[status(thm)],[t713576]) ).

cnf(t634659,plain,
    join(complement(X1),meet(X2,X1)) = join(complement(X1),X2),
    inference(cp,[status(thm)],[t170,t633569]) ).

cnf(t713577,plain,
    join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
    inference(step,[status(thm)],[t634659,t51]) ).

cnf(t713578,plain,
    join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
    inference(step,[status(thm)],[t713577,t23]) ).

cnf(t635510,plain,
    join(complement(X1),meet(X1,X2)) = join(X2,complement(X1)),
    inference(orient,[status(thm)],[t713578]) ).

cnf(t635846,plain,
    join(complement(X1),complement(complement(X2))) = join(complement(complement(X2)),complement(join(X2,X1))),
    inference(cp,[status(thm)],[t635510,t626212]) ).

cnf(t623927,plain,
    join(complement(X1),complement(X2)) = complement(meet(X2,X1)),
    inference(cp,[status(thm)],[t623804,t479]) ).

cnf(t713455,plain,
    join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
    inference(step,[status(thm)],[t623927,t51]) ).

cnf(t624597,plain,
    join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
    inference(orient,[status(thm)],[t713455]) ).

cnf(t713615,plain,
    complement(meet(X1,complement(X2))) = join(complement(complement(X2)),complement(join(X2,X1))),
    inference(step,[status(thm)],[t635846,t624597]) ).

cnf(t713616,plain,
    join(X2,complement(X1)) = join(complement(complement(X2)),complement(join(X2,X1))),
    inference(step,[status(thm)],[t713615,t623804]) ).

cnf(t713617,plain,
    join(X2,complement(X1)) = complement(meet(complement(X2),join(X2,X1))),
    inference(step,[status(thm)],[t713616,t624597]) ).

cnf(t530478,plain,
    complement(X1) = meet(complement(X1),complement(meet(X1,X2))),
    inference(cp,[status(thm)],[t16,t530434]) ).

cnf(t531155,plain,
    meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
    inference(orient,[status(thm)],[t530478]) ).

cnf(t531156,plain,
    complement(complement(X1)) = meet(X1,complement(meet(complement(X1),X2))),
    inference(cp,[status(thm)],[t531155,t479]) ).

cnf(t713249,plain,
    X1 = meet(X1,complement(meet(complement(X1),X2))),
    inference(step,[status(thm)],[t531156,t479]) ).

cnf(t713250,plain,
    X1 = meet(X1,complement(meet(X2,complement(X1)))),
    inference(step,[status(thm)],[t713249,t51]) ).

cnf(t531815,plain,
    meet(X1,complement(meet(X2,complement(X1)))) = X1,
    inference(orient,[status(thm)],[t713250]) ).

cnf(t532281,plain,
    complement(meet(X1,complement(X2))) = join(meet(X2,complement(meet(X1,complement(X2)))),complement(join(meet(X1,complement(X2)),X2))),
    inference(cp,[status(thm)],[t524982,t531815]) ).

cnf(t713321,plain,
    complement(meet(X1,complement(X2))) = join(X2,complement(join(meet(X1,complement(X2)),X2))),
    inference(step,[status(thm)],[t532281,t531815]) ).

cnf(t713322,plain,
    complement(meet(X1,complement(X2))) = join(X2,complement(join(X2,meet(X1,complement(X2))))),
    inference(step,[status(thm)],[t713321,t23]) ).

cnf(t571810,plain,
    join(X1,complement(join(X1,meet(X2,complement(X1))))) = complement(meet(X2,complement(X1))),
    inference(orient,[status(thm)],[t713322]) ).

cnf(t571813,plain,
    complement(meet(X1,complement(meet(X1,X2)))) = join(meet(X1,X2),complement(X1)),
    inference(cp,[status(thm)],[t571810,t529400]) ).

cnf(t713323,plain,
    complement(meet(X1,complement(meet(X1,X2)))) = join(complement(X1),meet(X1,X2)),
    inference(step,[status(thm)],[t571813,t23]) ).

cnf(t572711,plain,
    complement(meet(X1,complement(meet(X1,X2)))) = join(complement(X1),meet(X1,X2)),
    inference(orient,[status(thm)],[t713323]) ).

cnf(t526396,plain,
    join(X1,join(X1,X2)) = join(X1,complement(join(complement(join(X1,X2)),X1))),
    inference(cp,[status(thm)],[t526272,t16]) ).

cnf(t713240,plain,
    join(X1,X2) = join(X1,complement(join(complement(join(X1,X2)),X1))),
    inference(step,[status(thm)],[t526396,t108]) ).

cnf(t713241,plain,
    join(X1,X2) = join(X1,complement(join(X1,complement(join(X1,X2))))),
    inference(step,[status(thm)],[t713240,t23]) ).

cnf(t526954,plain,
    join(X1,complement(join(X1,complement(join(X1,X2))))) = join(X1,X2),
    inference(orient,[status(thm)],[t713241]) ).

cnf(t178500,plain,
    join(X1,X2) = join(X2,meet(join(X1,X2),meet(join(X1,X3),join(X1,Y3)))),
    inference(cp,[status(thm)],[t56645,t178364]) ).

cnf(t329234,plain,
    join(X1,meet(join(X2,X1),meet(join(X2,X3),join(X2,Y3)))) = join(X2,X1),
    inference(orient,[status(thm)],[t178500]) ).

cnf(t526958,plain,
    join(X1,meet(join(X2,X1),meet(join(X2,X3),join(X2,Y3)))) = join(X1,complement(join(X1,complement(join(X2,X1))))),
    inference(cp,[status(thm)],[t526954,t329234]) ).

cnf(t713242,plain,
    join(X2,X1) = join(X1,complement(join(X1,complement(join(X2,X1))))),
    inference(step,[status(thm)],[t526958,t329234]) ).

cnf(t527476,plain,
    join(X1,complement(join(X1,complement(join(X2,X1))))) = join(X2,X1),
    inference(orient,[status(thm)],[t713242]) ).

cnf(t534811,plain,
    complement(join(X1,complement(join(X1,complement(join(X2,X1)))))) = meet(complement(X1),complement(join(X2,X1))),
    inference(cp,[status(thm)],[t534796,t527476]) ).

cnf(t713258,plain,
    complement(join(X2,X1)) = meet(complement(X1),complement(join(X2,X1))),
    inference(step,[status(thm)],[t534811,t527476]) ).

cnf(t535493,plain,
    meet(complement(X1),complement(join(X2,X1))) = complement(join(X2,X1)),
    inference(orient,[status(thm)],[t713258]) ).

cnf(t572763,plain,
    join(complement(complement(X1)),meet(complement(X1),complement(join(X2,X1)))) = complement(meet(complement(X1),complement(complement(join(X2,X1))))),
    inference(cp,[status(thm)],[t572711,t535493]) ).

cnf(t713324,plain,
    join(X1,meet(complement(X1),complement(join(X2,X1)))) = complement(meet(complement(X1),complement(complement(join(X2,X1))))),
    inference(step,[status(thm)],[t572763,t479]) ).

cnf(t713325,plain,
    join(X1,complement(join(X2,X1))) = complement(meet(complement(X1),complement(complement(join(X2,X1))))),
    inference(step,[status(thm)],[t713324,t535493]) ).

cnf(t713326,plain,
    join(X1,complement(join(X1,X2))) = complement(meet(complement(X1),complement(complement(join(X2,X1))))),
    inference(step,[status(thm)],[t713325,t23]) ).

cnf(t713327,plain,
    join(X1,complement(join(X1,X2))) = complement(meet(complement(X1),join(X2,X1))),
    inference(step,[status(thm)],[t713326,t479]) ).

cnf(t713328,plain,
    join(X1,complement(join(X1,X2))) = complement(meet(complement(X1),join(X1,X2))),
    inference(step,[status(thm)],[t713327,t23]) ).

cnf(t573500,plain,
    complement(meet(complement(X1),join(X1,X2))) = join(X1,complement(join(X1,X2))),
    inference(orient,[status(thm)],[t713328]) ).

cnf(t713618,plain,
    join(X2,complement(X1)) = join(X2,complement(join(X2,X1))),
    inference(step,[status(thm)],[t713617,t573500]) ).

cnf(t639522,plain,
    join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
    inference(orient,[status(thm)],[t713618]) ).

cnf(t625659,plain,
    meet(meet(X1,complement(X2)),complement(X3)) = complement(join(X3,join(X2,complement(X1)))),
    inference(cp,[status(thm)],[t625580,t623804]) ).

cnf(t713553,plain,
    meet(complement(X3),meet(X1,complement(X2))) = complement(join(X3,join(X2,complement(X1)))),
    inference(step,[status(thm)],[t625659,t51]) ).

cnf(t713554,plain,
    meet(complement(X2),meet(complement(X3),X1)) = complement(join(X3,join(X2,complement(X1)))),
    inference(step,[status(thm)],[t713553,t67]) ).

cnf(t713555,plain,
    meet(X1,meet(complement(X2),complement(X3))) = complement(join(X3,join(X2,complement(X1)))),
    inference(step,[status(thm)],[t713554,t67]) ).

cnf(t713556,plain,
    meet(X1,complement(join(X2,X3))) = complement(join(X3,join(X2,complement(X1)))),
    inference(step,[status(thm)],[t713555,t626212]) ).

cnf(t713557,plain,
    meet(X1,complement(join(X2,X3))) = complement(join(X2,join(complement(X1),X3))),
    inference(step,[status(thm)],[t713556,t26]) ).

cnf(t713558,plain,
    meet(X1,complement(join(X2,X3))) = complement(join(X2,join(X3,complement(X1)))),
    inference(step,[status(thm)],[t713557,t23]) ).

cnf(t629720,plain,
    complement(join(X1,join(X2,complement(X3)))) = meet(X3,complement(join(X1,X2))),
    inference(orient,[status(thm)],[t713558]) ).

cnf(t639527,plain,
    join(X1,complement(join(X2,complement(X3)))) = join(X1,meet(X3,complement(join(X1,X2)))),
    inference(cp,[status(thm)],[t639522,t629720]) ).

cnf(t713781,plain,
    join(X1,meet(X3,complement(X2))) = join(X1,meet(X3,complement(join(X1,X2)))),
    inference(step,[status(thm)],[t639527,t625580]) ).

cnf(t704191,plain,
    join(X1,meet(X2,complement(join(X1,X3)))) = join(X1,meet(X2,complement(X3))),
    inference(orient,[status(thm)],[t713781]) ).

cnf(t704237,plain,
    join(X1,meet(X2,complement(complement(join(X1,X3))))) = join(X1,meet(X2,complement(join(X1,complement(X3))))),
    inference(cp,[status(thm)],[t704191,t639522]) ).

cnf(t713782,plain,
    join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,complement(join(X1,complement(X3))))),
    inference(step,[status(thm)],[t704237,t479]) ).

cnf(t713783,plain,
    join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,complement(complement(X3)))),
    inference(step,[status(thm)],[t713782,t704191]) ).

cnf(t713784,plain,
    join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
    inference(step,[status(thm)],[t713783,t479]) ).

cnf(t704972,plain,
    join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t713784]) ).

cnf(t705457,plain,
    meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,meet(X1,X3))),
    inference(cp,[status(thm)],[t179822,t704972]) ).

cnf(t163963,plain,
    meet(meet(X1,join(meet(X2,X1),meet(X2,X3))),join(Y3,Y4)) = meet(X1,meet(meet(X2,X1),join(Y3,Y4))),
    inference(cp,[status(thm)],[t60989,t163258]) ).

cnf(t711847,plain,
    meet(meet(X2,X1),join(Y3,Y4)) = meet(X1,meet(meet(X2,X1),join(Y3,Y4))),
    inference(step,[status(thm)],[t163963,t163258]) ).

cnf(t166000,plain,
    meet(X1,meet(meet(X2,X1),join(X3,Y3))) = meet(meet(X2,X1),join(X3,Y3)),
    inference(orient,[status(thm)],[t711847]) ).

cnf(t151940,plain,
    meet(X1,meet(join(meet(X1,X2),meet(X2,X3)),Y3)) = meet(meet(X1,X2),join(Y3,meet(X1,Y3))),
    inference(cp,[status(thm)],[t62132,t151571]) ).

cnf(t711827,plain,
    meet(X1,meet(Y3,join(meet(X1,X2),meet(X2,X3)))) = meet(meet(X1,X2),join(Y3,meet(X1,Y3))),
    inference(step,[status(thm)],[t151940,t51]) ).

cnf(t711828,plain,
    meet(X1,meet(Y3,join(meet(X1,X2),meet(X2,X3)))) = meet(X1,meet(X2,Y3)),
    inference(step,[status(thm)],[t711827,t62132]) ).

cnf(t158862,plain,
    meet(X1,meet(X2,join(meet(X1,X3),meet(X3,Y3)))) = meet(X1,meet(X3,X2)),
    inference(orient,[status(thm)],[t711828]) ).

cnf(t166026,plain,
    meet(meet(X1,X2),join(meet(X2,X3),meet(X3,Y3))) = meet(X2,meet(X3,meet(X1,X2))),
    inference(cp,[status(thm)],[t166000,t158862]) ).

cnf(t712220,plain,
    meet(meet(X1,X2),join(meet(X2,X3),meet(X3,Y3))) = meet(X2,meet(X2,meet(X3,X1))),
    inference(step,[status(thm)],[t166026,t67]) ).

cnf(t712221,plain,
    meet(meet(X1,X2),join(meet(X2,X3),meet(X3,Y3))) = meet(X2,meet(X1,meet(X2,X3))),
    inference(step,[status(thm)],[t712220,t67]) ).

cnf(t712222,plain,
    meet(meet(X1,X2),join(meet(X2,X3),meet(X3,Y3))) = meet(X1,meet(meet(X2,X3),X2)),
    inference(step,[status(thm)],[t712221,t67]) ).

cnf(t712223,plain,
    meet(meet(X1,X2),join(meet(X2,X3),meet(X3,Y3))) = meet(X1,meet(X2,meet(X2,X3))),
    inference(step,[status(thm)],[t712222,t51]) ).

cnf(t712224,plain,
    meet(meet(X1,X2),join(meet(X2,X3),meet(X3,Y3))) = meet(X1,meet(X2,X3)),
    inference(step,[status(thm)],[t712223,t125]) ).

cnf(t250361,plain,
    meet(meet(X1,X2),join(meet(X2,X3),meet(X3,Y3))) = meet(X1,meet(X2,X3)),
    inference(orient,[status(thm)],[t712224]) ).

cnf(t163957,plain,
    join(X1,meet(X2,join(meet(X3,X2),meet(X3,Y3)))) = meet(join(X1,X2),join(X1,meet(X3,X2))),
    inference(cp,[status(thm)],[t63079,t163258]) ).

cnf(t711845,plain,
    join(X1,meet(X3,X2)) = meet(join(X1,X2),join(X1,meet(X3,X2))),
    inference(step,[status(thm)],[t163957,t163258]) ).

cnf(t164395,plain,
    meet(join(X1,X2),join(X1,meet(X3,X2))) = join(X1,meet(X3,X2)),
    inference(orient,[status(thm)],[t711845]) ).

cnf(t251130,plain,
    meet(X1,meet(join(X2,X3),join(X2,meet(Y3,X3)))) = meet(meet(X1,join(X2,X3)),join(join(X2,meet(Y3,X3)),meet(join(X2,meet(Y3,X3)),Y4))),
    inference(cp,[status(thm)],[t250361,t164395]) ).

cnf(t712271,plain,
    meet(X1,join(X2,meet(Y3,X3))) = meet(meet(X1,join(X2,X3)),join(join(X2,meet(Y3,X3)),meet(join(X2,meet(Y3,X3)),Y4))),
    inference(step,[status(thm)],[t251130,t164395]) ).

cnf(t712272,plain,
    meet(X1,join(X2,meet(Y3,X3))) = meet(meet(X1,join(X2,X3)),join(X2,meet(Y3,X3))),
    inference(step,[status(thm)],[t712271,t14]) ).

cnf(t276655,plain,
    meet(meet(X1,join(X2,X3)),join(X2,meet(Y3,X3))) = meet(X1,join(X2,meet(Y3,X3))),
    inference(orient,[status(thm)],[t712272]) ).

cnf(t713807,plain,
    meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X1,X3))),
    inference(step,[status(thm)],[t705457,t276655]) ).

cnf(t705902,plain,
    meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t713807]) ).

cnf(t713810,plain,
    meet(X1,join(meet(X2,X1),X3)) = join(meet(X2,X1),meet(X1,X3)),
    inference(step,[status(thm)],[t182205,t705902]) ).

cnf(t706853,plain,
    meet(X1,join(meet(X2,X1),X3)) = join(meet(X2,X1),meet(X1,X3)),
    inference(rw,[status(thm)],[t713810]) ).

cnf(t713869,plain,
    meet(X1,join(X3,meet(X2,X1))) = join(meet(X2,X1),meet(X1,X3)),
    inference(step,[status(thm)],[t706853,t23]) ).

cnf(t713870,plain,
    meet(X1,join(X3,meet(X1,X2))) = join(meet(X2,X1),meet(X1,X3)),
    inference(step,[status(thm)],[t713869,t51]) ).

cnf(t713871,plain,
    meet(X1,join(X3,X2)) = join(meet(X2,X1),meet(X1,X3)),
    inference(step,[status(thm)],[t713870,t705902]) ).

cnf(t713872,plain,
    meet(X1,join(X2,X3)) = join(meet(X2,X1),meet(X1,X3)),
    inference(step,[status(thm)],[t713871,t23]) ).

cnf(t713873,plain,
    meet(X1,join(X2,X3)) = join(meet(X1,X3),meet(X2,X1)),
    inference(step,[status(thm)],[t713872,t23]) ).

cnf(t713874,plain,
    meet(X1,join(X2,X3)) = join(meet(X1,X3),meet(X1,X2)),
    inference(step,[status(thm)],[t713873,t51]) ).

cnf(t713875,plain,
    meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,X3)),
    inference(step,[status(thm)],[t713874,t23]) ).

cnf(t708481,plain,
    join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
    inference(orient,[status(thm)],[t713875]) ).

cnf(f12,negated_conjecture,
    meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).

fof(f12_nnf,plain,
    meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
    inference(nnf_transformation,[status(thm)],[f12]) ).

fof(f12_sk,plain,
    meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
    inference(skolemisation,[status(esa)],[f12_nnf]) ).

cnf(c12,plain,
    meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
    inference(cnf_transformation,[status(esa)],[f12_sk]) ).

cnf(goal_0,negated_conjecture,
    join(meet(a,b),meet(a,c)) != meet(a,join(b,c)),
    inference(equality_encoding,[status(esa)],[c12]) ).

cnf(g0_0,plain,
    meet(a,join(b,c)) != meet(a,join(b,c)),
    inference(rw,[status(thm)],[goal_0,t708481]) ).

cnf(contradiction_0,plain,
    $false,
    inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LAT204-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36  % Computer : n019.cluster.edu
% 0.10/0.36  % Model    : x86_64 x86_64
% 0.10/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36  % Memory   : 8046.5625MB
% 0.10/0.36  % OS       : Linux 6.8.0-71-generic
% 0.10/0.36  % CPULimit : 300
% 0.10/0.36  % WCLimit  : 300
% 0.10/0.36  % DateTime : Wed Sep 23 20:32:49 UTC 2026
% 0.10/0.37  % CPUTime  : 
% 0.10/0.37  Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 241.68/35.72  % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 241.68/35.72  % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------