%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT211-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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:56:09 PM UTC 2026
% Result : Unsatisfiable 31.04s 4.33s
% Output : Proof 31.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 84
% Number of leaves : 13
% Syntax : Number of formulae : 360 ( 356 unt; 0 def)
% Number of atoms : 368 ( 367 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 24 ( 16 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-4 aty)
% Number of variables : 798 ( 106 sgn 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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(t64,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(f4,axiom,
meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f4_nnf,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t7,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t23,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(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(t25,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X2,X1),one,complement(X2),X1),X1),
inference(cp,[status(thm)],[t18,t23]) ).
cnf(t10432,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X2,X1),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t25]) ).
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(t57,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t10480,plain,
X1 = ifeq(zero,zero,ifeq(join(complement(X1),X1),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t10432,t57]) ).
cnf(t4,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t17,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t117459,plain,
X1 = ifeq(join(complement(X1),X1),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t10480,t17]) ).
cnf(t117460,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t117459,t64]) ).
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(t82,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t117461,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t117460,t82]) ).
cnf(t117462,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t117461,t17]) ).
cnf(t18996,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t117462]) ).
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(t26,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(f11,axiom,
meet(X,join(Y,Z)) = join(meet(X,join(Z,meet(X,Y))),meet(X,join(Y,meet(X,Z)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H69) ).
fof(f11_nnf,plain,
! [X,Y,Z] : meet(X,join(Y,Z)) = join(meet(X,join(Z,meet(X,Y))),meet(X,join(Y,meet(X,Z)))),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z] : meet(X,join(Y,Z)) = join(meet(X,join(Z,meet(X,Y))),meet(X,join(Y,meet(X,Z)))),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(X1,X2)) = join(meet(X0,join(X2,meet(X0,X1))),meet(X0,join(X1,meet(X0,X2)))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t12,plain,
join(meet(X1,join(X2,meet(X1,X3))),meet(X1,join(X3,meet(X1,X2)))) = meet(X1,join(X3,X2)),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t35,plain,
join(meet(X1,join(X2,meet(X1,X3))),meet(X1,join(X3,meet(X1,X2)))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t12]) ).
cnf(f2,axiom,
meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f2_nnf,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t8,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t14,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t37,plain,
meet(X1,join(X2,X1)) = join(X1,meet(X1,join(X2,meet(X1,X1)))),
inference(cp,[status(thm)],[t35,t14]) ).
cnf(f3,axiom,
join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f3_nnf,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t6,plain,
join(X1,meet(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t16,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t117281,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t37,t16]) ).
cnf(t136,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t117281]) ).
cnf(t138,plain,
meet(X1,X2) = meet(meet(X1,X2),X1),
inference(cp,[status(thm)],[t136,t16]) ).
cnf(t117289,plain,
meet(X1,X2) = meet(X1,meet(X2,X1)),
inference(step,[status(thm)],[t138,t26]) ).
cnf(t168,plain,
meet(X1,meet(X2,X1)) = meet(X1,X2),
inference(orient,[status(thm)],[t117289]) ).
cnf(t173,plain,
meet(X1,meet(meet(X2,X1),X3)) = meet(meet(X1,X2),X3),
inference(cp,[status(thm)],[t26,t168]) ).
cnf(t117341,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t173,t26]) ).
cnf(t117342,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t117341,t26]) ).
cnf(t1378,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t117342]) ).
cnf(t28,plain,
meet(X1,meet(X2,join(meet(X1,X2),X3))) = meet(X1,X2),
inference(cp,[status(thm)],[t26,t14]) ).
cnf(t2286,plain,
meet(X1,meet(X2,join(meet(X1,X2),X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t28]) ).
cnf(t32,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t26,t23]) ).
cnf(t117348,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t32,t26]) ).
cnf(t1753,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t117348]) ).
cnf(t2288,plain,
meet(X1,X2) = meet(X2,meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t2286,t1753]) ).
cnf(t4197,plain,
meet(X1,meet(X2,join(meet(X2,X1),X3))) = meet(X2,X1),
inference(orient,[status(thm)],[t2288]) ).
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(t70,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t75,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t70,t16]) ).
cnf(t356,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t75]) ).
cnf(t368,plain,
join(meet(X1,X2),X3) = meet(join(meet(X1,X2),X3),join(X1,X3)),
inference(cp,[status(thm)],[t136,t356]) ).
cnf(t117464,plain,
join(meet(X1,X2),X3) = meet(join(X1,X3),join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t368,t23]) ).
cnf(t19294,plain,
meet(join(X1,X2),join(meet(X1,X3),X2)) = join(meet(X1,X3),X2),
inference(orient,[status(thm)],[t117464]) ).
cnf(t19312,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t19294,t16]) ).
cnf(t42486,plain,
meet(X1,join(meet(X1,X2),meet(X1,X3))) = join(meet(X1,X2),meet(X1,X3)),
inference(orient,[status(thm)],[t19312]) ).
cnf(t42692,plain,
meet(X1,X2) = meet(X2,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t4197,t42486]) ).
cnf(t42744,plain,
meet(X1,join(meet(X2,X1),meet(X2,X3))) = meet(X2,X1),
inference(orient,[status(thm)],[t42692]) ).
cnf(t42893,plain,
meet(X1,X2) = meet(X2,join(meet(X2,X1),meet(X1,X3))),
inference(cp,[status(thm)],[t42744,t23]) ).
cnf(t44000,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X2,X1),
inference(orient,[status(thm)],[t42893]) ).
cnf(t24,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t16,t23]) ).
cnf(t130,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t24]) ).
cnf(t133,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t130,t26]) ).
cnf(t285,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t133]) ).
cnf(t132,plain,
join(X1,X2) = join(join(X1,X2),X1),
inference(cp,[status(thm)],[t130,t14]) ).
cnf(t117288,plain,
join(X1,X2) = join(X1,join(X2,X1)),
inference(step,[status(thm)],[t132,t70]) ).
cnf(t160,plain,
join(X1,join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t117288]) ).
cnf(t165,plain,
join(X1,X2) = meet(join(X1,X2),join(X2,X1)),
inference(cp,[status(thm)],[t136,t160]) ).
cnf(t428,plain,
meet(join(X1,X2),join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t165]) ).
cnf(t454,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X2,X1))),
inference(cp,[status(thm)],[t285,t428]) ).
cnf(t117354,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X2,X1)))),
inference(step,[status(thm)],[t454,t70]) ).
cnf(t3175,plain,
join(X1,join(X2,meet(X3,join(X2,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t117354]) ).
cnf(t31,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t26,t14]) ).
cnf(t336,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t31]) ).
cnf(t349,plain,
meet(join(X1,X2),X3) = join(meet(join(X1,X2),X3),meet(X1,X3)),
inference(cp,[status(thm)],[t130,t336]) ).
cnf(t117463,plain,
meet(join(X1,X2),X3) = join(meet(X1,X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t349,t64]) ).
cnf(t19020,plain,
join(meet(X1,X2),meet(join(X1,X3),X2)) = meet(join(X1,X3),X2),
inference(orient,[status(thm)],[t117463]) ).
cnf(t19038,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(join(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t19020,t14]) ).
cnf(t35241,plain,
join(X1,meet(join(X1,X2),join(X1,X3))) = meet(join(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t19038]) ).
cnf(t35427,plain,
join(X1,X2) = join(X1,meet(join(X2,X3),join(X2,X1))),
inference(cp,[status(thm)],[t3175,t35241]) ).
cnf(t35865,plain,
join(X1,meet(join(X2,X3),join(X2,X1))) = join(X1,X2),
inference(orient,[status(thm)],[t35427]) ).
cnf(t72,plain,
join(X1,join(X2,meet(join(X1,X2),X3))) = join(X1,X2),
inference(cp,[status(thm)],[t70,t16]) ).
cnf(t2406,plain,
join(X1,join(X2,meet(join(X1,X2),X3))) = join(X1,X2),
inference(orient,[status(thm)],[t72]) ).
cnf(t77,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t70,t64]) ).
cnf(t117349,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t77,t70]) ).
cnf(t2011,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t117349]) ).
cnf(t2408,plain,
join(X1,X2) = join(X2,join(X1,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t2406,t2011]) ).
cnf(t4350,plain,
join(X1,join(X2,meet(join(X2,X1),X3))) = join(X2,X1),
inference(orient,[status(thm)],[t2408]) ).
cnf(t35422,plain,
join(X1,X2) = join(X2,meet(join(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t4350,t35241]) ).
cnf(t35471,plain,
join(X1,meet(join(X2,X1),join(X2,X3))) = join(X2,X1),
inference(orient,[status(thm)],[t35422]) ).
cnf(t35877,plain,
join(X1,X2) = join(X1,meet(join(X3,X2),join(X2,X1))),
inference(cp,[status(thm)],[t35865,t35471]) ).
cnf(t37044,plain,
join(X1,meet(join(X2,X3),join(X3,X1))) = join(X1,X3),
inference(orient,[status(thm)],[t35877]) ).
cnf(t37230,plain,
join(X1,X2) = join(X1,meet(join(X3,X2),join(X1,X2))),
inference(cp,[status(thm)],[t37044,t64]) ).
cnf(t38138,plain,
join(X1,meet(join(X2,X3),join(X1,X3))) = join(X1,X3),
inference(orient,[status(thm)],[t37230]) ).
cnf(t44029,plain,
meet(join(X1,X2),X3) = meet(X3,join(meet(X3,join(X1,X2)),X2)),
inference(cp,[status(thm)],[t44000,t38138]) ).
cnf(t117518,plain,
meet(join(X1,X2),X3) = meet(X3,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t44029,t64]) ).
cnf(t47376,plain,
meet(X1,join(X2,meet(X1,join(X3,X2)))) = meet(join(X3,X2),X1),
inference(orient,[status(thm)],[t117518]) ).
cnf(t290,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,X1)),
inference(cp,[status(thm)],[t285,t14]) ).
cnf(t117313,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,X1))),
inference(step,[status(thm)],[t290,t70]) ).
cnf(t487,plain,
join(X1,join(X2,meet(X3,X1))) = join(X1,X2),
inference(orient,[status(thm)],[t117313]) ).
cnf(t44,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X3,meet(X2,X1))),meet(X1,join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t35,t23]) ).
cnf(t51384,plain,
join(meet(X1,join(X2,meet(X3,X1))),meet(X1,join(X3,meet(X1,X2)))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t44]) ).
cnf(t51929,plain,
join(join(X1,meet(X2,X3)),meet(X2,join(X3,meet(X1,X2)))) = join(join(X1,meet(X2,X3)),meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t487,t51384]) ).
cnf(t117519,plain,
join(X1,join(meet(X2,X3),meet(X2,join(X3,meet(X1,X2))))) = join(join(X1,meet(X2,X3)),meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t51929,t70]) ).
cnf(t1430,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X3,X2))),
inference(cp,[status(thm)],[t285,t1378]) ).
cnf(t3923,plain,
join(meet(X1,X2),meet(X1,meet(X3,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t1430]) ).
cnf(t3975,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X1,X2)),
inference(cp,[status(thm)],[t3923,t14]) ).
cnf(t117493,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t3975,t64]) ).
cnf(t30920,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t117493]) ).
cnf(t117520,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(join(X1,meet(X2,X3)),meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t117519,t30920]) ).
cnf(t117521,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,join(meet(X2,X3),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t117520,t70]) ).
cnf(t3976,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X1,X3)),
inference(cp,[status(thm)],[t3923,t136]) ).
cnf(t117494,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X3),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t3976,t64]) ).
cnf(t31242,plain,
join(meet(X1,X2),meet(X1,join(X3,X2))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t117494]) ).
cnf(t117522,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t117521,t31242]) ).
cnf(t53617,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t117522]) ).
cnf(t53739,plain,
join(X1,meet(complement(X1),join(X1,X2))) = join(X1,meet(complement(X1),join(X2,zero))),
inference(cp,[status(thm)],[t53617,t57]) ).
cnf(t60,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t16,t57]) ).
cnf(t86,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t60]) ).
cnf(t117523,plain,
join(X1,meet(complement(X1),join(X1,X2))) = join(X1,meet(complement(X1),X2)),
inference(step,[status(thm)],[t53739,t86]) ).
cnf(t53998,plain,
join(X1,meet(complement(X1),join(X1,X2))) = join(X1,meet(complement(X1),X2)),
inference(orient,[status(thm)],[t117523]) ).
cnf(t85,plain,
join(X1,join(complement(X1),X2)) = join(one,X2),
inference(cp,[status(thm)],[t70,t82]) ).
cnf(t84,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t14,t82]) ).
cnf(t90,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t84]) ).
cnf(t91,plain,
X1 = meet(one,X1),
inference(cp,[status(thm)],[t90,t23]) ).
cnf(t105,plain,
meet(one,X1) = X1,
inference(orient,[status(thm)],[t91]) ).
cnf(t107,plain,
join(one,X1) = one,
inference(cp,[status(thm)],[t105,t14]) ).
cnf(t119,plain,
join(one,X1) = one,
inference(orient,[status(thm)],[t107]) ).
cnf(t117301,plain,
join(X1,join(complement(X1),X2)) = one,
inference(step,[status(thm)],[t85,t119]) ).
cnf(t238,plain,
join(X1,join(complement(X1),X2)) = one,
inference(orient,[status(thm)],[t117301]) ).
cnf(t241,plain,
join(join(complement(X1),X2),X1) = join(join(complement(X1),X2),one),
inference(cp,[status(thm)],[t160,t238]) ).
cnf(t117302,plain,
join(complement(X1),join(X2,X1)) = join(join(complement(X1),X2),one),
inference(step,[status(thm)],[t241,t70]) ).
cnf(t117303,plain,
join(complement(X1),join(X2,X1)) = join(complement(X1),join(X2,one)),
inference(step,[status(thm)],[t117302,t70]) ).
cnf(t120,plain,
one = join(X1,one),
inference(cp,[status(thm)],[t119,t64]) ).
cnf(t128,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t120]) ).
cnf(t117304,plain,
join(complement(X1),join(X2,X1)) = join(complement(X1),one),
inference(step,[status(thm)],[t117303,t128]) ).
cnf(t117305,plain,
join(complement(X1),join(X2,X1)) = one,
inference(step,[status(thm)],[t117304,t128]) ).
cnf(t249,plain,
join(complement(X1),join(X2,X1)) = one,
inference(orient,[status(thm)],[t117305]) ).
cnf(t254,plain,
one = join(complement(meet(X1,X2)),X1),
inference(cp,[status(thm)],[t249,t16]) ).
cnf(t117306,plain,
one = join(X1,complement(meet(X1,X2))),
inference(step,[status(thm)],[t254,t64]) ).
cnf(t262,plain,
join(X1,complement(meet(X1,X2))) = one,
inference(orient,[status(thm)],[t117306]) ).
cnf(t54087,plain,
join(X1,meet(complement(X1),complement(meet(X1,X2)))) = join(X1,meet(complement(X1),one)),
inference(cp,[status(thm)],[t53998,t262]) ).
cnf(t117524,plain,
join(X1,meet(complement(X1),complement(meet(X1,X2)))) = join(X1,complement(X1)),
inference(step,[status(thm)],[t54087,t90]) ).
cnf(t117525,plain,
join(X1,meet(complement(X1),complement(meet(X1,X2)))) = one,
inference(step,[status(thm)],[t117524,t82]) ).
cnf(t54308,plain,
join(X1,meet(complement(X1),complement(meet(X1,X2)))) = one,
inference(orient,[status(thm)],[t117525]) ).
cnf(t54369,plain,
meet(complement(X1),complement(meet(X1,X2))) = ifeq(meet(X1,meet(complement(X1),complement(meet(X1,X2)))),zero,ifeq(one,one,complement(X1),meet(complement(X1),complement(meet(X1,X2)))),meet(complement(X1),complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t18,t54308]) ).
cnf(t59,plain,
meet(X1,meet(complement(X1),X2)) = meet(zero,X2),
inference(cp,[status(thm)],[t26,t57]) ).
cnf(t87,plain,
X1 = join(zero,X1),
inference(cp,[status(thm)],[t86,t64]) ).
cnf(t96,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t87]) ).
cnf(t98,plain,
meet(zero,X1) = zero,
inference(cp,[status(thm)],[t96,t16]) ).
cnf(t116,plain,
meet(zero,X1) = zero,
inference(orient,[status(thm)],[t98]) ).
cnf(t117294,plain,
meet(X1,meet(complement(X1),X2)) = zero,
inference(step,[status(thm)],[t59,t116]) ).
cnf(t179,plain,
meet(X1,meet(complement(X1),X2)) = zero,
inference(orient,[status(thm)],[t117294]) ).
cnf(t117526,plain,
meet(complement(X1),complement(meet(X1,X2))) = ifeq(zero,zero,ifeq(one,one,complement(X1),meet(complement(X1),complement(meet(X1,X2)))),meet(complement(X1),complement(meet(X1,X2)))),
inference(step,[status(thm)],[t54369,t179]) ).
cnf(t117527,plain,
meet(complement(X1),complement(meet(X1,X2))) = ifeq(one,one,complement(X1),meet(complement(X1),complement(meet(X1,X2)))),
inference(step,[status(thm)],[t117526,t17]) ).
cnf(t117528,plain,
meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
inference(step,[status(thm)],[t117527,t17]) ).
cnf(t54504,plain,
meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t117528]) ).
cnf(t35600,plain,
join(X1,X2) = join(X2,meet(join(X2,X1),join(X1,X3))),
inference(cp,[status(thm)],[t35471,t64]) ).
cnf(t36178,plain,
join(X1,meet(join(X1,X2),join(X2,X3))) = join(X2,X1),
inference(orient,[status(thm)],[t35600]) ).
cnf(t36335,plain,
join(X1,X2) = join(X2,meet(join(X2,X1),join(X3,X1))),
inference(cp,[status(thm)],[t36178,t35471]) ).
cnf(t37659,plain,
join(X1,meet(join(X1,X2),join(X3,X2))) = join(X2,X1),
inference(orient,[status(thm)],[t36335]) ).
cnf(t37900,plain,
join(meet(X1,X2),X3) = join(X3,meet(join(X3,meet(X1,X2)),X2)),
inference(cp,[status(thm)],[t37659,t130]) ).
cnf(t117514,plain,
join(meet(X1,X2),X3) = join(X3,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t37900,t23]) ).
cnf(t39392,plain,
join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(meet(X3,X2),X1),
inference(orient,[status(thm)],[t117514]) ).
cnf(t42763,plain,
meet(X1,X2) = meet(X2,join(meet(X3,X1),meet(X1,X2))),
inference(cp,[status(thm)],[t42744,t39392]) ).
cnf(t43526,plain,
meet(X1,join(meet(X2,X3),meet(X3,X1))) = meet(X3,X1),
inference(orient,[status(thm)],[t42763]) ).
cnf(t44176,plain,
meet(X1,X2) = meet(X2,join(meet(X2,X1),meet(X3,X1))),
inference(cp,[status(thm)],[t44000,t43526]) ).
cnf(t45768,plain,
meet(X1,join(meet(X1,X2),meet(X3,X2))) = meet(X2,X1),
inference(orient,[status(thm)],[t44176]) ).
cnf(t54511,plain,
complement(X1) = meet(complement(X1),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t54504,t45768]) ).
cnf(t55072,plain,
meet(complement(X1),complement(meet(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t54511]) ).
cnf(t55140,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(X2)),
inference(cp,[status(thm)],[t130,t55072]) ).
cnf(t117534,plain,
complement(meet(X1,X2)) = join(complement(X2),complement(meet(X1,X2))),
inference(step,[status(thm)],[t55140,t64]) ).
cnf(t56644,plain,
join(complement(X1),complement(meet(X2,X1))) = complement(meet(X2,X1)),
inference(orient,[status(thm)],[t117534]) ).
cnf(t83,plain,
one = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t82,t70]) ).
cnf(t597,plain,
join(X1,join(X2,complement(join(X1,X2)))) = one,
inference(orient,[status(thm)],[t83]) ).
cnf(t54081,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = join(X1,meet(complement(X1),one)),
inference(cp,[status(thm)],[t53998,t597]) ).
cnf(t117618,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = join(X1,complement(X1)),
inference(step,[status(thm)],[t54081,t90]) ).
cnf(t117619,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = one,
inference(step,[status(thm)],[t117618,t82]) ).
cnf(t98252,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = one,
inference(orient,[status(thm)],[t117619]) ).
cnf(t98425,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = ifeq(meet(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))),zero,ifeq(one,one,complement(X1),meet(complement(X1),join(X2,complement(join(X1,X2))))),meet(complement(X1),join(X2,complement(join(X1,X2))))),
inference(cp,[status(thm)],[t18,t98252]) ).
cnf(t117620,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = ifeq(zero,zero,ifeq(one,one,complement(X1),meet(complement(X1),join(X2,complement(join(X1,X2))))),meet(complement(X1),join(X2,complement(join(X1,X2))))),
inference(step,[status(thm)],[t98425,t179]) ).
cnf(t117621,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = ifeq(one,one,complement(X1),meet(complement(X1),join(X2,complement(join(X1,X2))))),
inference(step,[status(thm)],[t117620,t17]) ).
cnf(t117622,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = complement(X1),
inference(step,[status(thm)],[t117621,t17]) ).
cnf(t98580,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = complement(X1),
inference(orient,[status(thm)],[t117622]) ).
cnf(t98713,plain,
complement(meet(complement(X1),join(X2,complement(join(X1,X2))))) = join(complement(join(X2,complement(join(X1,X2)))),complement(complement(X1))),
inference(cp,[status(thm)],[t56644,t98580]) ).
cnf(t117624,plain,
complement(complement(X1)) = join(complement(join(X2,complement(join(X1,X2)))),complement(complement(X1))),
inference(step,[status(thm)],[t98713,t98580]) ).
cnf(t117625,plain,
X1 = join(complement(join(X2,complement(join(X1,X2)))),complement(complement(X1))),
inference(step,[status(thm)],[t117624,t18996]) ).
cnf(t117626,plain,
X1 = join(complement(complement(X1)),complement(join(X2,complement(join(X1,X2))))),
inference(step,[status(thm)],[t117625,t64]) ).
cnf(t117627,plain,
X1 = join(X1,complement(join(X2,complement(join(X1,X2))))),
inference(step,[status(thm)],[t117626,t18996]) ).
cnf(t99273,plain,
join(X1,complement(join(X2,complement(join(X1,X2))))) = X1,
inference(orient,[status(thm)],[t117627]) ).
cnf(t255,plain,
one = join(complement(meet(X1,X2)),X2),
inference(cp,[status(thm)],[t249,t130]) ).
cnf(t117307,plain,
one = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t255,t64]) ).
cnf(t269,plain,
join(X1,complement(meet(X2,X1))) = one,
inference(orient,[status(thm)],[t117307]) ).
cnf(t272,plain,
one = join(X1,complement(meet(X2,meet(X3,X1)))),
inference(cp,[status(thm)],[t269,t26]) ).
cnf(t880,plain,
join(X1,complement(meet(X2,meet(X3,X1)))) = one,
inference(orient,[status(thm)],[t272]) ).
cnf(t892,plain,
one = join(join(X1,X2),complement(meet(X3,join(X2,X1)))),
inference(cp,[status(thm)],[t880,t428]) ).
cnf(t117418,plain,
one = join(X1,join(X2,complement(meet(X3,join(X2,X1))))),
inference(step,[status(thm)],[t892,t70]) ).
cnf(t9976,plain,
join(X1,join(X2,complement(meet(X3,join(X2,X1))))) = one,
inference(orient,[status(thm)],[t117418]) ).
cnf(t54540,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t130,t54504]) ).
cnf(t117530,plain,
complement(meet(X1,X2)) = join(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t54540,t64]) ).
cnf(t55292,plain,
join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t117530]) ).
cnf(t55459,plain,
one = join(X1,complement(meet(X2,join(complement(X2),X1)))),
inference(cp,[status(thm)],[t9976,t55292]) ).
cnf(t59847,plain,
join(X1,complement(meet(X2,join(complement(X2),X1)))) = one,
inference(orient,[status(thm)],[t55459]) ).
cnf(t99282,plain,
X1 = join(X1,complement(join(complement(meet(X2,join(complement(X2),X1))),complement(one)))),
inference(cp,[status(thm)],[t99273,t59847]) ).
cnf(t117628,plain,
X1 = join(X1,complement(join(complement(one),complement(meet(X2,join(complement(X2),X1)))))),
inference(step,[status(thm)],[t99282,t64]) ).
cnf(t106,plain,
complement(one) = zero,
inference(cp,[status(thm)],[t105,t57]) ).
cnf(t114,plain,
complement(one) = zero,
inference(orient,[status(thm)],[t106]) ).
cnf(t117629,plain,
X1 = join(X1,complement(join(zero,complement(meet(X2,join(complement(X2),X1)))))),
inference(step,[status(thm)],[t117628,t114]) ).
cnf(t117630,plain,
X1 = join(X1,complement(complement(meet(X2,join(complement(X2),X1))))),
inference(step,[status(thm)],[t117629,t96]) ).
cnf(t117631,plain,
X1 = join(X1,meet(X2,join(complement(X2),X1))),
inference(step,[status(thm)],[t117630,t18996]) ).
cnf(t99648,plain,
join(X1,meet(X2,join(complement(X2),X1))) = X1,
inference(orient,[status(thm)],[t117631]) ).
cnf(t99937,plain,
meet(join(complement(X1),X2),X1) = meet(X1,X2),
inference(cp,[status(thm)],[t47376,t99648]) ).
cnf(t117632,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(step,[status(thm)],[t99937,t23]) ).
cnf(t100025,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t117632]) ).
cnf(t100242,plain,
meet(X1,meet(X2,join(complement(X1),X3))) = meet(X1,meet(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t1378,t100025]) ).
cnf(t117673,plain,
meet(X1,meet(X2,join(complement(X1),X3))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t100242,t1378]) ).
cnf(t108092,plain,
meet(X1,meet(X2,join(complement(X1),X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t117673]) ).
cnf(t108121,plain,
meet(X1,meet(complement(X2),complement(join(X2,complement(X1))))) = meet(X1,complement(X2)),
inference(cp,[status(thm)],[t108092,t98580]) ).
cnf(t55114,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t55072,t14]) ).
cnf(t117531,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t55114,t23]) ).
cnf(t55470,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t117531]) ).
cnf(t117674,plain,
meet(X1,complement(join(X2,complement(X1)))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t108121,t55470]) ).
cnf(t55509,plain,
complement(X1) = join(complement(X1),complement(join(X1,X2))),
inference(cp,[status(thm)],[t16,t55470]) ).
cnf(t55661,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t55509]) ).
cnf(t55662,plain,
complement(complement(X1)) = join(X1,complement(join(complement(X1),X2))),
inference(cp,[status(thm)],[t55661,t18996]) ).
cnf(t117532,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t55662,t18996]) ).
cnf(t55839,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t117532]) ).
cnf(t55846,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(cp,[status(thm)],[t55839,t37659]) ).
cnf(t56025,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t55846]) ).
cnf(t56030,plain,
complement(join(X1,complement(X2))) = meet(complement(join(X1,complement(X2))),X2),
inference(cp,[status(thm)],[t136,t56025]) ).
cnf(t117537,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t56030,t23]) ).
cnf(t57401,plain,
meet(X1,complement(join(X2,complement(X1)))) = complement(join(X2,complement(X1))),
inference(orient,[status(thm)],[t117537]) ).
cnf(t117675,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t117674,t57401]) ).
cnf(t108497,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t117675]) ).
cnf(t108531,plain,
join(X1,complement(X2)) = complement(meet(X2,complement(X1))),
inference(cp,[status(thm)],[t18996,t108497]) ).
cnf(t109290,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t108531]) ).
cnf(t109303,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t109290,t23]) ).
cnf(t109475,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t109303]) ).
cnf(t54080,plain,
join(X1,meet(complement(X1),join(X2,X1))) = join(X1,meet(complement(X1),join(X1,X2))),
inference(cp,[status(thm)],[t53998,t160]) ).
cnf(t117575,plain,
join(X1,meet(complement(X1),join(X2,X1))) = join(X1,meet(complement(X1),X2)),
inference(step,[status(thm)],[t54080,t53998]) ).
cnf(t76895,plain,
join(X1,meet(complement(X1),join(X2,X1))) = join(X1,meet(complement(X1),X2)),
inference(orient,[status(thm)],[t117575]) ).
cnf(t100049,plain,
meet(X1,meet(complement(complement(X1)),join(X2,complement(X1)))) = meet(X1,join(complement(X1),meet(complement(complement(X1)),X2))),
inference(cp,[status(thm)],[t100025,t76895]) ).
cnf(t117633,plain,
meet(X1,meet(X1,join(X2,complement(X1)))) = meet(X1,join(complement(X1),meet(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t100049,t18996]) ).
cnf(f0,axiom,
meet(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f0_nnf,plain,
! [X] : meet(X,X) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : meet(X,X) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
meet(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
meet(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t13,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t30,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t26,t13]) ).
cnf(t147,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t30]) ).
cnf(t117634,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(complement(X1),meet(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t117633,t147]) ).
cnf(t117635,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,meet(complement(complement(X1)),X2)),
inference(step,[status(thm)],[t117634,t100025]) ).
cnf(t117636,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,meet(X1,X2)),
inference(step,[status(thm)],[t117635,t18996]) ).
cnf(t117637,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t117636,t147]) ).
cnf(t100372,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t117637]) ).
cnf(t100397,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t100372,t18996]) ).
cnf(t100994,plain,
meet(complement(X1),join(X2,X1)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t100397]) ).
cnf(t109482,plain,
join(X1,complement(join(X2,X1))) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t109475,t100994]) ).
cnf(t117742,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(step,[status(thm)],[t109482,t109475]) ).
cnf(t109993,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t117742]) ).
cnf(t253,plain,
one = join(complement(join(X1,X2)),join(X2,X1)),
inference(cp,[status(thm)],[t249,t160]) ).
cnf(t117327,plain,
one = join(join(X2,X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t253,t64]) ).
cnf(t117328,plain,
one = join(X2,join(X1,complement(join(X1,X2)))),
inference(step,[status(thm)],[t117327,t70]) ).
cnf(t789,plain,
join(X1,join(X2,complement(join(X2,X1)))) = one,
inference(orient,[status(thm)],[t117328]) ).
cnf(t98654,plain,
complement(X1) = meet(complement(X1),join(join(X2,complement(join(X2,X1))),complement(one))),
inference(cp,[status(thm)],[t98580,t789]) ).
cnf(t117666,plain,
complement(X1) = meet(complement(X1),join(X2,join(complement(join(X2,X1)),complement(one)))),
inference(step,[status(thm)],[t98654,t70]) ).
cnf(t117667,plain,
complement(X1) = meet(complement(X1),join(X2,join(complement(one),complement(join(X2,X1))))),
inference(step,[status(thm)],[t117666,t64]) ).
cnf(t117668,plain,
complement(X1) = meet(complement(X1),join(X2,join(zero,complement(join(X2,X1))))),
inference(step,[status(thm)],[t117667,t114]) ).
cnf(t117669,plain,
complement(X1) = meet(complement(X1),join(X2,complement(join(X2,X1)))),
inference(step,[status(thm)],[t117668,t96]) ).
cnf(t106481,plain,
meet(complement(X1),join(X2,complement(join(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t117669]) ).
cnf(t108122,plain,
meet(X1,meet(complement(X2),complement(join(complement(X1),X2)))) = meet(X1,complement(X2)),
inference(cp,[status(thm)],[t108092,t106481]) ).
cnf(t55115,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X2)),
inference(cp,[status(thm)],[t55072,t136]) ).
cnf(t117533,plain,
complement(join(X1,X2)) = meet(complement(X2),complement(join(X1,X2))),
inference(step,[status(thm)],[t55115,t23]) ).
cnf(t56411,plain,
meet(complement(X1),complement(join(X2,X1))) = complement(join(X2,X1)),
inference(orient,[status(thm)],[t117533]) ).
cnf(t117687,plain,
meet(X1,complement(join(complement(X1),X2))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t108122,t56411]) ).
cnf(t55471,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(join(complement(X1),X2))),
inference(cp,[status(thm)],[t55470,t18996]) ).
cnf(t57209,plain,
meet(X1,complement(join(complement(X1),X2))) = complement(join(complement(X1),X2)),
inference(orient,[status(thm)],[t55471]) ).
cnf(t117688,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t117687,t57209]) ).
cnf(t108745,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t117688]) ).
cnf(t109997,plain,
join(X1,complement(complement(X2))) = join(X1,meet(X2,complement(X1))),
inference(cp,[status(thm)],[t109993,t108745]) ).
cnf(t117743,plain,
join(X1,X2) = join(X1,meet(X2,complement(X1))),
inference(step,[status(thm)],[t109997,t18996]) ).
cnf(t110299,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t117743]) ).
cnf(t110311,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t110299,t23]) ).
cnf(t110514,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t110311]) ).
cnf(t110527,plain,
join(X1,meet(X2,join(complement(complement(X1)),X3))) = join(X1,meet(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t110514,t108092]) ).
cnf(t117779,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(complement(X1),meet(X2,X3))),
inference(step,[status(thm)],[t110527,t18996]) ).
cnf(t117780,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t117779,t110514]) ).
cnf(t113328,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t117780]) ).
cnf(t166,plain,
join(X1,join(join(X2,X1),X3)) = join(join(X1,X2),X3),
inference(cp,[status(thm)],[t70,t160]) ).
cnf(t117339,plain,
join(X1,join(X2,join(X1,X3))) = join(join(X1,X2),X3),
inference(step,[status(thm)],[t166,t70]) ).
cnf(t117340,plain,
join(X1,join(X2,join(X1,X3))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t117339,t70]) ).
cnf(t1263,plain,
join(X1,join(X2,join(X1,X3))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t117340]) ).
cnf(t100098,plain,
meet(X1,join(X2,join(complement(X1),X3))) = meet(X1,join(complement(X1),join(X2,X3))),
inference(cp,[status(thm)],[t100025,t1263]) ).
cnf(t117670,plain,
meet(X1,join(X2,join(complement(X1),X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t100098,t100025]) ).
cnf(t106853,plain,
meet(X1,join(X2,join(complement(X1),X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t117670]) ).
cnf(t110418,plain,
meet(X1,join(X2,meet(X3,complement(complement(X1))))) = meet(X1,join(X2,join(complement(X1),X3))),
inference(cp,[status(thm)],[t106853,t110299]) ).
cnf(t117765,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,join(complement(X1),X3))),
inference(step,[status(thm)],[t110418,t18996]) ).
cnf(t117766,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t117765,t106853]) ).
cnf(t112927,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t117766]) ).
cnf(t112987,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t112927,t64]) ).
cnf(t114557,plain,
meet(X1,join(meet(X2,X1),X3)) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t112987]) ).
cnf(t114857,plain,
join(meet(X1,X2),meet(X2,X3)) = join(meet(X1,X2),meet(X2,join(X3,X1))),
inference(cp,[status(thm)],[t113328,t114557]) ).
cnf(t139,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t136,t70]) ).
cnf(t299,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t139]) ).
cnf(t304,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(cp,[status(thm)],[t299,t16]) ).
cnf(t117314,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,X1))),
inference(step,[status(thm)],[t304,t26]) ).
cnf(t512,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t117314]) ).
cnf(t530,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X3,X1)),
inference(cp,[status(thm)],[t130,t512]) ).
cnf(t117470,plain,
meet(X1,join(X2,X3)) = join(meet(X3,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t530,t64]) ).
cnf(t22452,plain,
join(meet(X1,X2),meet(X2,join(X3,X1))) = meet(X2,join(X3,X1)),
inference(orient,[status(thm)],[t117470]) ).
cnf(t117833,plain,
join(meet(X1,X2),meet(X2,X3)) = meet(X2,join(X3,X1)),
inference(step,[status(thm)],[t114857,t22452]) ).
cnf(t116731,plain,
join(meet(X1,X2),meet(X2,X3)) = meet(X2,join(X3,X1)),
inference(orient,[status(thm)],[t117833]) ).
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,
join(meet(a,c),meet(a,b)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[goal_0,t64]) ).
cnf(g0_1,plain,
join(meet(c,a),meet(a,b)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_0,t23]) ).
cnf(g0_2,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_1,t116731]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT211-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 20:36:34 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 31.04/4.33 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 31.04/4.33 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------