%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT257-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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:26 PM UTC 2026
% Result : Unsatisfiable 46.97s 6.45s
% Output : Proof 46.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 134
% Number of leaves : 15
% Syntax : Number of formulae : 438 ( 434 unt; 0 def)
% Number of atoms : 446 ( 445 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-4 aty)
% Number of variables : 954 ( 207 sgn 46 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f10,axiom,
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f10_nnf,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( complement(X0) = X1
| join(X0,X1) != one
| meet(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t12,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t19,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(f6,axiom,
meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f6_nnf,plain,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t11,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/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f4_nnf,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t8,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t24,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t43336,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t11,t24]) ).
cnf(t27,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t43336]) ).
cnf(f0,axiom,
meet(X,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f0_nnf,plain,
! [X] : meet(X,X) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : meet(X,X) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
meet(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
meet(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t14,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t30,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t27,t14]) ).
cnf(t43338,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t30,t27]) ).
cnf(t43339,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t43338,t24]) ).
cnf(t127,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t43339]) ).
cnf(f11,axiom,
meet(X,join(meet(Y,join(X,Z)),meet(Z,join(X,Y)))) = join(meet(X,Y),meet(X,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H82) ).
fof(f11_nnf,plain,
! [X,Y,Z] : meet(X,join(meet(Y,join(X,Z)),meet(Z,join(X,Y)))) = join(meet(X,Y),meet(X,Z)),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z] : meet(X,join(meet(Y,join(X,Z)),meet(Z,join(X,Y)))) = join(meet(X,Y),meet(X,Z)),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(meet(X1,join(X0,X2)),meet(X2,join(X0,X1)))) = join(meet(X0,X1),meet(X0,X2)),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t13,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X3,join(X1,X2)))) = join(meet(X1,X2),meet(X1,X3)),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t47,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X3,join(X1,X2)))) = join(meet(X1,X2),meet(X1,X3)),
inference(orient,[status(thm)],[t13]) ).
cnf(t131,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X3,join(X1,X2)))) = meet(X1,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t127,t47]) ).
cnf(t43396,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t131,t47]) ).
cnf(t351,plain,
meet(X1,join(meet(X1,X2),meet(X1,X3))) = join(meet(X1,X2),meet(X1,X3)),
inference(orient,[status(thm)],[t43396]) ).
cnf(f8,axiom,
join(X,complement(X)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_join) ).
fof(f8_nnf,plain,
! [X] : join(X,complement(X)) = one,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] : join(X,complement(X)) = one,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
join(X0,complement(X0)) = one,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t3,plain,
join(X1,complement(X1)) = one,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t103,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t105,plain,
join(meet(X1,X2),meet(X1,complement(X1))) = meet(X1,join(meet(X2,one),meet(complement(X1),join(X1,X2)))),
inference(cp,[status(thm)],[t47,t103]) ).
cnf(f9,axiom,
meet(X,complement(X)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_meet) ).
fof(f9_nnf,plain,
! [X] : meet(X,complement(X)) = zero,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] : meet(X,complement(X)) = zero,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
meet(X0,complement(X0)) = zero,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t4,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t63,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t43764,plain,
join(meet(X1,X2),zero) = meet(X1,join(meet(X2,one),meet(complement(X1),join(X1,X2)))),
inference(step,[status(thm)],[t105,t63]) ).
cnf(f3,axiom,
join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption2) ).
fof(f3_nnf,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t7,plain,
join(X1,meet(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t17,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t64,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t17,t63]) ).
cnf(t109,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t64]) ).
cnf(t43765,plain,
meet(X1,X2) = meet(X1,join(meet(X2,one),meet(complement(X1),join(X1,X2)))),
inference(step,[status(thm)],[t43764,t109]) ).
cnf(f2,axiom,
meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption1) ).
fof(f2_nnf,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t9,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t15,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t104,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t15,t103]) ).
cnf(t122,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t104]) ).
cnf(t43766,plain,
meet(X1,X2) = meet(X1,join(X2,meet(complement(X1),join(X1,X2)))),
inference(step,[status(thm)],[t43765,t122]) ).
cnf(t5523,plain,
meet(X1,join(X2,meet(complement(X1),join(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t43766]) ).
cnf(t26,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X2,X1),one,complement(X2),X1),X1),
inference(cp,[status(thm)],[t19,t24]) ).
cnf(f5,axiom,
join(X,Y) = join(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f5_nnf,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t6,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t73,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t43648,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(step,[status(thm)],[t26,t73]) ).
cnf(t2817,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t43648]) ).
cnf(t2828,plain,
X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t2817,t63]) ).
cnf(t5,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t18,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t43649,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t2828,t18]) ).
cnf(t43650,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t43649,t103]) ).
cnf(t43651,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t43650,t18]) ).
cnf(t2867,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t43651]) ).
cnf(t5526,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X2,meet(X1,join(complement(X1),X2)))),
inference(cp,[status(thm)],[t5523,t2867]) ).
cnf(t43768,plain,
meet(X2,complement(X1)) = meet(complement(X1),join(X2,meet(X1,join(complement(X1),X2)))),
inference(step,[status(thm)],[t5526,t24]) ).
cnf(t43769,plain,
meet(X2,complement(X1)) = meet(complement(X1),join(X2,meet(X1,join(X2,complement(X1))))),
inference(step,[status(thm)],[t43768,t73]) ).
cnf(t5684,plain,
meet(complement(X1),join(X2,meet(X1,join(X2,complement(X1))))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t43769]) ).
cnf(t5685,plain,
meet(X1,complement(complement(X2))) = meet(X2,join(X1,meet(complement(X2),join(X1,complement(complement(X2)))))),
inference(cp,[status(thm)],[t5684,t2867]) ).
cnf(t43774,plain,
meet(X1,X2) = meet(X2,join(X1,meet(complement(X2),join(X1,complement(complement(X2)))))),
inference(step,[status(thm)],[t5685,t2867]) ).
cnf(t43775,plain,
meet(X1,X2) = meet(X2,join(X1,meet(complement(X2),join(X1,X2)))),
inference(step,[status(thm)],[t43774,t2867]) ).
cnf(t5804,plain,
meet(X1,join(X2,meet(complement(X1),join(X2,X1)))) = meet(X2,X1),
inference(orient,[status(thm)],[t43775]) ).
cnf(t5851,plain,
join(meet(X1,join(X2,meet(complement(X1),join(X2,X1)))),meet(X1,X3)) = meet(X1,join(meet(X2,X1),meet(X1,X3))),
inference(cp,[status(thm)],[t351,t5804]) ).
cnf(t43798,plain,
join(meet(X2,X1),meet(X1,X3)) = meet(X1,join(meet(X2,X1),meet(X1,X3))),
inference(step,[status(thm)],[t5851,t5804]) ).
cnf(t6353,plain,
meet(X1,join(meet(X2,X1),meet(X1,X3))) = join(meet(X2,X1),meet(X1,X3)),
inference(orient,[status(thm)],[t43798]) ).
cnf(t6378,plain,
join(meet(X1,X2),meet(X2,X2)) = meet(X2,join(meet(X1,X2),X2)),
inference(cp,[status(thm)],[t6353,t14]) ).
cnf(t43799,plain,
join(meet(X1,X2),X2) = meet(X2,join(meet(X1,X2),X2)),
inference(step,[status(thm)],[t6378,t14]) ).
cnf(t43800,plain,
join(X2,meet(X1,X2)) = meet(X2,join(meet(X1,X2),X2)),
inference(step,[status(thm)],[t43799,t73]) ).
cnf(t43801,plain,
join(X2,meet(X1,X2)) = meet(X2,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t43800,t73]) ).
cnf(t43802,plain,
join(X2,meet(X1,X2)) = X2,
inference(step,[status(thm)],[t43801,t15]) ).
cnf(t6475,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t43802]) ).
cnf(t31,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t27,t15]) ).
cnf(t43352,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t31,t27]) ).
cnf(t43353,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t43352,t24]) ).
cnf(t43354,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t43353,t24]) ).
cnf(t190,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t43354]) ).
cnf(t6484,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X2,X1)),
inference(cp,[status(thm)],[t6475,t190]) ).
cnf(t43807,plain,
meet(X1,join(X2,X3)) = join(meet(X2,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t6484,t73]) ).
cnf(t43808,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t43807,t24]) ).
cnf(t6654,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t43808]) ).
cnf(t6664,plain,
meet(X1,join(meet(X1,X2),X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t6654,t127]) ).
cnf(t43999,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t6664,t73]) ).
cnf(t44000,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t43999,t73]) ).
cnf(t11225,plain,
join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))) = meet(X1,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t44000]) ).
cnf(t11316,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t15,t11225]) ).
cnf(t44005,plain,
meet(X1,X2) = meet(X1,meet(join(X3,meet(X1,X2)),meet(X1,X2))),
inference(step,[status(thm)],[t11316,t27]) ).
cnf(t44006,plain,
meet(X1,X2) = meet(X1,meet(X2,meet(join(X3,meet(X1,X2)),X1))),
inference(step,[status(thm)],[t44005,t27]) ).
cnf(t44007,plain,
meet(X1,X2) = meet(X1,meet(X1,meet(X2,join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t44006,t27]) ).
cnf(t44008,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t44007,t127]) ).
cnf(t11456,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t44008]) ).
cnf(t11494,plain,
meet(X1,meet(X1,X2)) = meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t11456,t127]) ).
cnf(t44065,plain,
meet(X1,X2) = meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t11494,t127]) ).
cnf(t14043,plain,
meet(X1,meet(meet(X1,X2),join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t44065]) ).
cnf(t14046,plain,
meet(X1,join(X2,meet(complement(X1),join(X2,X1)))) = meet(X1,meet(meet(X2,X1),join(X3,meet(X1,join(X2,meet(complement(X1),join(X2,X1))))))),
inference(cp,[status(thm)],[t14043,t5804]) ).
cnf(t44093,plain,
meet(X2,X1) = meet(X1,meet(meet(X2,X1),join(X3,meet(X1,join(X2,meet(complement(X1),join(X2,X1))))))),
inference(step,[status(thm)],[t14046,t5804]) ).
cnf(t44094,plain,
meet(X2,X1) = meet(X1,meet(meet(X2,X1),join(X3,meet(X2,X1)))),
inference(step,[status(thm)],[t44093,t5804]) ).
cnf(t15399,plain,
meet(X1,meet(meet(X2,X1),join(X3,meet(X2,X1)))) = meet(X2,X1),
inference(orient,[status(thm)],[t44094]) ).
cnf(t15415,plain,
meet(X1,meet(X1,X2)) = meet(meet(X1,X2),meet(meet(X1,X2),join(X3,meet(X1,meet(X1,X2))))),
inference(cp,[status(thm)],[t15399,t127]) ).
cnf(t44095,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(X3,meet(X1,meet(X1,X2))))),
inference(step,[status(thm)],[t15415,t127]) ).
cnf(t44096,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,meet(X1,X2)))),
inference(step,[status(thm)],[t44095,t127]) ).
cnf(t44097,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t44096,t127]) ).
cnf(t15667,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t44097]) ).
cnf(t15736,plain,
meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3)) = join(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3))),
inference(cp,[status(thm)],[t6654,t15667]) ).
cnf(t44103,plain,
meet(meet(X1,X2),join(Y3,join(X3,meet(X1,X2)))) = join(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3))),
inference(step,[status(thm)],[t15736,t73]) ).
cnf(f7,axiom,
join(join(X,Y),Z) = join(X,join(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f7_nnf,plain,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t10,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t43337,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t10,t73]) ).
cnf(t79,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t43337]) ).
cnf(t44104,plain,
meet(meet(X1,X2),join(X3,join(meet(X1,X2),Y3))) = join(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3))),
inference(step,[status(thm)],[t44103,t79]) ).
cnf(t44105,plain,
meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = join(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),Y3))),
inference(step,[status(thm)],[t44104,t73]) ).
cnf(t44106,plain,
meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = meet(X1,X2),
inference(step,[status(thm)],[t44105,t17]) ).
cnf(t16217,plain,
meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t44106]) ).
cnf(t6492,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t6475,t27]) ).
cnf(t6560,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t6492]) ).
cnf(t16257,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X2))),
inference(cp,[status(thm)],[t16217,t6560]) ).
cnf(t19689,plain,
meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t16257]) ).
cnf(t49,plain,
join(meet(X1,join(X1,X2)),meet(X1,X2)) = meet(X1,join(join(X1,X2),meet(X2,join(X1,join(X1,X2))))),
inference(cp,[status(thm)],[t47,t14]) ).
cnf(t43543,plain,
join(meet(X1,X2),meet(X1,join(X1,X2))) = meet(X1,join(join(X1,X2),meet(X2,join(X1,join(X1,X2))))),
inference(step,[status(thm)],[t49,t73]) ).
cnf(t43544,plain,
join(meet(X1,X2),X1) = meet(X1,join(join(X1,X2),meet(X2,join(X1,join(X1,X2))))),
inference(step,[status(thm)],[t43543,t15]) ).
cnf(t43545,plain,
join(X1,meet(X1,X2)) = meet(X1,join(join(X1,X2),meet(X2,join(X1,join(X1,X2))))),
inference(step,[status(thm)],[t43544,t73]) ).
cnf(t43546,plain,
X1 = meet(X1,join(join(X1,X2),meet(X2,join(X1,join(X1,X2))))),
inference(step,[status(thm)],[t43545,t17]) ).
cnf(f1,axiom,
join(X,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f1_nnf,plain,
! [X] : join(X,X) = X,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] : join(X,X) = X,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t0,plain,
join(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t16,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t82,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t79,t16]) ).
cnf(t43341,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t82,t79]) ).
cnf(t43342,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t43341,t73]) ).
cnf(t143,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t43342]) ).
cnf(t43547,plain,
X1 = meet(X1,join(join(X1,X2),meet(X2,join(X1,X2)))),
inference(step,[status(thm)],[t43546,t143]) ).
cnf(t1066,plain,
meet(X1,join(join(X1,X2),meet(X2,join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t43547]) ).
cnf(t1075,plain,
X1 = meet(X1,join(one,meet(complement(X1),join(X1,complement(X1))))),
inference(cp,[status(thm)],[t1066,t103]) ).
cnf(t43548,plain,
X1 = meet(X1,join(one,meet(complement(X1),one))),
inference(step,[status(thm)],[t1075,t103]) ).
cnf(t43549,plain,
X1 = meet(X1,join(one,complement(X1))),
inference(step,[status(thm)],[t43548,t122]) ).
cnf(t1107,plain,
meet(X1,join(one,complement(X1))) = X1,
inference(orient,[status(thm)],[t43549]) ).
cnf(t1112,plain,
join(meet(one,X1),meet(one,complement(X1))) = meet(one,join(X1,meet(complement(X1),join(one,X1)))),
inference(cp,[status(thm)],[t47,t1107]) ).
cnf(t43559,plain,
join(meet(X1,one),meet(one,complement(X1))) = meet(one,join(X1,meet(complement(X1),join(one,X1)))),
inference(step,[status(thm)],[t1112,t24]) ).
cnf(t43560,plain,
join(X1,meet(one,complement(X1))) = meet(one,join(X1,meet(complement(X1),join(one,X1)))),
inference(step,[status(thm)],[t43559,t122]) ).
cnf(t43561,plain,
join(X1,meet(one,complement(X1))) = meet(one,join(X1,meet(complement(X1),join(X1,one)))),
inference(step,[status(thm)],[t43560,t73]) ).
cnf(t146,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t143,t103]) ).
cnf(t43343,plain,
one = join(X1,one),
inference(step,[status(thm)],[t146,t103]) ).
cnf(t155,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t43343]) ).
cnf(t43562,plain,
join(X1,meet(one,complement(X1))) = meet(one,join(X1,meet(complement(X1),one))),
inference(step,[status(thm)],[t43561,t155]) ).
cnf(t43563,plain,
join(X1,meet(one,complement(X1))) = meet(one,join(X1,complement(X1))),
inference(step,[status(thm)],[t43562,t122]) ).
cnf(t43564,plain,
join(X1,meet(one,complement(X1))) = meet(one,one),
inference(step,[status(thm)],[t43563,t103]) ).
cnf(t43565,plain,
join(X1,meet(one,complement(X1))) = one,
inference(step,[status(thm)],[t43564,t122]) ).
cnf(t1138,plain,
join(X1,meet(one,complement(X1))) = one,
inference(orient,[status(thm)],[t43565]) ).
cnf(t1139,plain,
meet(one,complement(X1)) = ifeq(meet(X1,meet(one,complement(X1))),zero,ifeq(one,one,complement(X1),meet(one,complement(X1))),meet(one,complement(X1))),
inference(cp,[status(thm)],[t19,t1138]) ).
cnf(t66,plain,
meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
inference(cp,[status(thm)],[t27,t63]) ).
cnf(t43348,plain,
meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
inference(step,[status(thm)],[t66,t24]) ).
cnf(t130,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t127,t63]) ).
cnf(t43340,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t130,t63]) ).
cnf(t138,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t43340]) ).
cnf(t43349,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t43348,t138]) ).
cnf(t174,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t43349]) ).
cnf(t43566,plain,
meet(one,complement(X1)) = ifeq(zero,zero,ifeq(one,one,complement(X1),meet(one,complement(X1))),meet(one,complement(X1))),
inference(step,[status(thm)],[t1139,t174]) ).
cnf(t43567,plain,
meet(one,complement(X1)) = ifeq(one,one,complement(X1),meet(one,complement(X1))),
inference(step,[status(thm)],[t43566,t18]) ).
cnf(t43568,plain,
meet(one,complement(X1)) = complement(X1),
inference(step,[status(thm)],[t43567,t18]) ).
cnf(t1150,plain,
meet(one,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t43568]) ).
cnf(t1154,plain,
join(meet(one,complement(X1)),meet(one,X2)) = meet(one,join(complement(X1),meet(one,X2))),
inference(cp,[status(thm)],[t351,t1150]) ).
cnf(t43590,plain,
join(meet(one,X2),meet(one,complement(X1))) = meet(one,join(complement(X1),meet(one,X2))),
inference(step,[status(thm)],[t1154,t73]) ).
cnf(t43591,plain,
join(meet(X2,one),meet(one,complement(X1))) = meet(one,join(complement(X1),meet(one,X2))),
inference(step,[status(thm)],[t43590,t24]) ).
cnf(t43592,plain,
join(X2,meet(one,complement(X1))) = meet(one,join(complement(X1),meet(one,X2))),
inference(step,[status(thm)],[t43591,t122]) ).
cnf(t43593,plain,
join(X2,complement(X1)) = meet(one,join(complement(X1),meet(one,X2))),
inference(step,[status(thm)],[t43592,t1150]) ).
cnf(t43594,plain,
join(X2,complement(X1)) = meet(one,join(complement(X1),meet(X2,one))),
inference(step,[status(thm)],[t43593,t24]) ).
cnf(t43595,plain,
join(X2,complement(X1)) = meet(one,join(complement(X1),X2)),
inference(step,[status(thm)],[t43594,t122]) ).
cnf(t43596,plain,
join(X2,complement(X1)) = meet(one,join(X2,complement(X1))),
inference(step,[status(thm)],[t43595,t73]) ).
cnf(t1256,plain,
meet(one,join(X1,complement(X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t43596]) ).
cnf(t1262,plain,
join(meet(one,join(X1,complement(X2))),meet(one,X3)) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(cp,[status(thm)],[t351,t1256]) ).
cnf(t43620,plain,
join(meet(one,X3),meet(one,join(X1,complement(X2)))) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t1262,t73]) ).
cnf(t43621,plain,
join(meet(X3,one),meet(one,join(X1,complement(X2)))) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t43620,t24]) ).
cnf(t43622,plain,
join(X3,meet(one,join(X1,complement(X2)))) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t43621,t122]) ).
cnf(t43623,plain,
join(X3,join(X1,complement(X2))) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t43622,t1256]) ).
cnf(t43624,plain,
join(X1,join(complement(X2),X3)) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t43623,t79]) ).
cnf(t43625,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(join(X1,complement(X2)),meet(one,X3))),
inference(step,[status(thm)],[t43624,t73]) ).
cnf(t43626,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(meet(one,X3),join(X1,complement(X2)))),
inference(step,[status(thm)],[t43625,t73]) ).
cnf(t43627,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(complement(X2),join(meet(one,X3),X1))),
inference(step,[status(thm)],[t43626,t79]) ).
cnf(t43628,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(X1,join(complement(X2),meet(one,X3)))),
inference(step,[status(thm)],[t43627,t79]) ).
cnf(t43629,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(X1,join(complement(X2),meet(X3,one)))),
inference(step,[status(thm)],[t43628,t24]) ).
cnf(t43630,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(X1,join(complement(X2),X3))),
inference(step,[status(thm)],[t43629,t122]) ).
cnf(t43631,plain,
join(X1,join(X3,complement(X2))) = meet(one,join(X1,join(X3,complement(X2)))),
inference(step,[status(thm)],[t43630,t73]) ).
cnf(t2328,plain,
meet(one,join(X1,join(X2,complement(X3)))) = join(X1,join(X2,complement(X3))),
inference(orient,[status(thm)],[t43631]) ).
cnf(t140,plain,
zero = ifeq(zero,zero,ifeq(join(X1,zero),one,complement(X1),zero),zero),
inference(cp,[status(thm)],[t19,t138]) ).
cnf(t43344,plain,
zero = ifeq(join(X1,zero),one,complement(X1),zero),
inference(step,[status(thm)],[t140,t18]) ).
cnf(t43345,plain,
zero = ifeq(X1,one,complement(X1),zero),
inference(step,[status(thm)],[t43344,t109]) ).
cnf(t162,plain,
ifeq(X1,one,complement(X1),zero) = zero,
inference(orient,[status(thm)],[t43345]) ).
cnf(t163,plain,
zero = complement(one),
inference(cp,[status(thm)],[t162,t18]) ).
cnf(t164,plain,
complement(one) = zero,
inference(orient,[status(thm)],[t163]) ).
cnf(t2334,plain,
join(X1,join(X2,complement(one))) = meet(one,join(X1,join(X2,zero))),
inference(cp,[status(thm)],[t2328,t164]) ).
cnf(t43632,plain,
join(X1,join(X2,zero)) = meet(one,join(X1,join(X2,zero))),
inference(step,[status(thm)],[t2334,t164]) ).
cnf(t43633,plain,
join(X1,X2) = meet(one,join(X1,join(X2,zero))),
inference(step,[status(thm)],[t43632,t109]) ).
cnf(t43634,plain,
join(X1,X2) = meet(one,join(X1,X2)),
inference(step,[status(thm)],[t43633,t109]) ).
cnf(t2379,plain,
meet(one,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t43634]) ).
cnf(t19719,plain,
meet(X1,meet(one,join(X2,X3))) = meet(meet(X1,join(X2,X3)),join(Y3,meet(X1,one))),
inference(cp,[status(thm)],[t19689,t2379]) ).
cnf(t44190,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y3,meet(X1,one))),
inference(step,[status(thm)],[t19719,t2379]) ).
cnf(t44191,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y3,X1)),
inference(step,[status(thm)],[t44190,t122]) ).
cnf(t44192,plain,
meet(X1,join(X2,X3)) = meet(join(Y3,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t44191,t24]) ).
cnf(t44193,plain,
meet(X1,join(X2,X3)) = meet(join(X2,X3),meet(join(Y3,X1),X1)),
inference(step,[status(thm)],[t44192,t27]) ).
cnf(t44194,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(Y3,X1))),
inference(step,[status(thm)],[t44193,t27]) ).
cnf(t44195,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,Y3))),
inference(step,[status(thm)],[t44194,t73]) ).
cnf(t44196,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,Y3),join(X2,X3))),
inference(step,[status(thm)],[t44195,t24]) ).
cnf(t20853,plain,
meet(X1,meet(join(X1,X2),join(X3,Y3))) = meet(X1,join(X3,Y3)),
inference(orient,[status(thm)],[t44196]) ).
cnf(f12,hypothesis,
meet(b,a) = a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distributivity_hypothesis) ).
fof(f12_nnf,plain,
meet(b,a) = a,
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
meet(b,a) = a,
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(t2,plain,
meet(b,a) = a,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t68,plain,
meet(b,a) = a,
inference(orient,[status(thm)],[t2]) ).
cnf(t6675,plain,
meet(b,join(a,X1)) = join(a,meet(b,join(a,X1))),
inference(cp,[status(thm)],[t6654,t68]) ).
cnf(t43809,plain,
meet(b,join(X1,a)) = join(a,meet(b,join(a,X1))),
inference(step,[status(thm)],[t6675,t73]) ).
cnf(t43810,plain,
meet(b,join(X1,a)) = join(a,meet(b,join(X1,a))),
inference(step,[status(thm)],[t43809,t73]) ).
cnf(t6726,plain,
join(a,meet(b,join(X1,a))) = meet(b,join(X1,a)),
inference(orient,[status(thm)],[t43810]) ).
cnf(t20864,plain,
meet(a,join(X1,X2)) = meet(a,meet(meet(b,join(X3,a)),join(X1,X2))),
inference(cp,[status(thm)],[t20853,t6726]) ).
cnf(t44247,plain,
meet(a,join(X1,X2)) = meet(a,meet(join(X1,X2),meet(b,join(X3,a)))),
inference(step,[status(thm)],[t20864,t24]) ).
cnf(t44248,plain,
meet(a,join(X1,X2)) = meet(a,meet(b,meet(join(X3,a),join(X1,X2)))),
inference(step,[status(thm)],[t44247,t27]) ).
cnf(t44249,plain,
meet(a,join(X1,X2)) = meet(b,meet(meet(join(X3,a),join(X1,X2)),a)),
inference(step,[status(thm)],[t44248,t27]) ).
cnf(t44250,plain,
meet(a,join(X1,X2)) = meet(b,meet(a,meet(join(X3,a),join(X1,X2)))),
inference(step,[status(thm)],[t44249,t24]) ).
cnf(t44251,plain,
meet(a,join(X1,X2)) = meet(b,meet(a,meet(join(X1,X2),join(X3,a)))),
inference(step,[status(thm)],[t44250,t24]) ).
cnf(t24458,plain,
meet(b,meet(a,meet(join(X1,X2),join(X3,a)))) = meet(a,join(X1,X2)),
inference(orient,[status(thm)],[t44251]) ).
cnf(t24513,plain,
meet(b,meet(a,meet(join(X1,X2),join(X3,a)))) = meet(meet(a,join(X1,X2)),join(Y3,meet(b,a))),
inference(cp,[status(thm)],[t19689,t24458]) ).
cnf(t44282,plain,
meet(a,join(X1,X2)) = meet(meet(a,join(X1,X2)),join(Y3,meet(b,a))),
inference(step,[status(thm)],[t24513,t24458]) ).
cnf(t44283,plain,
meet(a,join(X1,X2)) = meet(meet(a,join(X1,X2)),join(Y3,a)),
inference(step,[status(thm)],[t44282,t68]) ).
cnf(t44284,plain,
meet(a,join(X1,X2)) = meet(join(Y3,a),meet(a,join(X1,X2))),
inference(step,[status(thm)],[t44283,t24]) ).
cnf(t44285,plain,
meet(a,join(X1,X2)) = meet(join(X1,X2),meet(join(Y3,a),a)),
inference(step,[status(thm)],[t44284,t27]) ).
cnf(t44286,plain,
meet(a,join(X1,X2)) = meet(a,meet(join(X1,X2),join(Y3,a))),
inference(step,[status(thm)],[t44285,t27]) ).
cnf(t25868,plain,
meet(a,meet(join(X1,X2),join(X3,a))) = meet(a,join(X1,X2)),
inference(orient,[status(thm)],[t44286]) ).
cnf(t25888,plain,
meet(a,join(meet(X1,X2),meet(X1,meet(X2,X3)))) = meet(a,meet(meet(X1,X2),join(Y3,a))),
inference(cp,[status(thm)],[t25868,t6560]) ).
cnf(t44308,plain,
meet(a,meet(X1,X2)) = meet(a,meet(meet(X1,X2),join(Y3,a))),
inference(step,[status(thm)],[t25888,t6560]) ).
cnf(t44309,plain,
meet(X2,meet(a,X1)) = meet(a,meet(meet(X1,X2),join(Y3,a))),
inference(step,[status(thm)],[t44308,t27]) ).
cnf(t44310,plain,
meet(X1,meet(X2,a)) = meet(a,meet(meet(X1,X2),join(Y3,a))),
inference(step,[status(thm)],[t44309,t27]) ).
cnf(t26504,plain,
meet(a,meet(meet(X1,X2),join(X3,a))) = meet(X1,meet(X2,a)),
inference(orient,[status(thm)],[t44310]) ).
cnf(t19690,plain,
meet(X1,meet(X2,X3)) = meet(join(Y3,meet(X1,X2)),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t19689,t24]) ).
cnf(t44239,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X3),meet(join(Y3,meet(X1,X2)),X1)),
inference(step,[status(thm)],[t19690,t27]) ).
cnf(t44240,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t44239,t27]) ).
cnf(t23143,plain,
meet(X1,meet(meet(X2,X3),join(Y3,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t44240]) ).
cnf(t23153,plain,
meet(X1,meet(X2,join(X3,meet(complement(X2),join(X3,X2))))) = meet(X1,meet(meet(X3,X2),join(Y3,meet(X1,X2)))),
inference(cp,[status(thm)],[t23143,t5804]) ).
cnf(t44383,plain,
meet(X1,meet(X3,X2)) = meet(X1,meet(meet(X3,X2),join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t23153,t5804]) ).
cnf(t31200,plain,
meet(X1,meet(meet(X2,X3),join(Y3,meet(X1,X3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t44383]) ).
cnf(t31240,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(Y3,meet(X1,join(X2,X3))))),
inference(cp,[status(thm)],[t31200,t15]) ).
cnf(t44384,plain,
meet(X1,X2) = meet(X1,meet(X2,join(Y3,meet(X1,join(X2,X3))))),
inference(step,[status(thm)],[t31240,t15]) ).
cnf(t31604,plain,
meet(X1,meet(X2,join(X3,meet(X1,join(X2,Y3))))) = meet(X1,X2),
inference(orient,[status(thm)],[t44384]) ).
cnf(t31614,plain,
meet(X1,X2) = meet(X1,join(meet(X2,X3),meet(X2,X1))),
inference(cp,[status(thm)],[t31604,t47]) ).
cnf(t44385,plain,
meet(X1,X2) = meet(X1,join(meet(X2,X1),meet(X2,X3))),
inference(step,[status(thm)],[t31614,t73]) ).
cnf(t44386,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t44385,t24]) ).
cnf(t31796,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t44386]) ).
cnf(t31987,plain,
meet(X1,meet(join(meet(X1,X2),meet(X2,X3)),a)) = meet(a,meet(meet(X1,X2),join(Y3,a))),
inference(cp,[status(thm)],[t26504,t31796]) ).
cnf(t44487,plain,
meet(X1,meet(a,join(meet(X1,X2),meet(X2,X3)))) = meet(a,meet(meet(X1,X2),join(Y3,a))),
inference(step,[status(thm)],[t31987,t24]) ).
cnf(t44488,plain,
meet(X1,meet(a,join(meet(X1,X2),meet(X2,X3)))) = meet(X1,meet(X2,a)),
inference(step,[status(thm)],[t44487,t26504]) ).
cnf(t38151,plain,
meet(X1,meet(a,join(meet(X1,X2),meet(X2,X3)))) = meet(X1,meet(X2,a)),
inference(orient,[status(thm)],[t44488]) ).
cnf(t69,plain,
b = join(b,a),
inference(cp,[status(thm)],[t17,t68]) ).
cnf(t116,plain,
join(b,a) = b,
inference(orient,[status(thm)],[t69]) ).
cnf(t118,plain,
join(meet(b,X1),meet(b,a)) = meet(b,join(meet(X1,b),meet(a,join(b,X1)))),
inference(cp,[status(thm)],[t47,t116]) ).
cnf(t43530,plain,
join(meet(X1,b),meet(b,a)) = meet(b,join(meet(X1,b),meet(a,join(b,X1)))),
inference(step,[status(thm)],[t118,t24]) ).
cnf(t43531,plain,
join(meet(X1,b),a) = meet(b,join(meet(X1,b),meet(a,join(b,X1)))),
inference(step,[status(thm)],[t43530,t68]) ).
cnf(t43532,plain,
join(a,meet(X1,b)) = meet(b,join(meet(X1,b),meet(a,join(b,X1)))),
inference(step,[status(thm)],[t43531,t73]) ).
cnf(t43533,plain,
join(a,meet(X1,b)) = meet(b,join(meet(X1,b),meet(a,join(X1,b)))),
inference(step,[status(thm)],[t43532,t73]) ).
cnf(t936,plain,
meet(b,join(meet(X1,b),meet(a,join(X1,b)))) = join(a,meet(X1,b)),
inference(orient,[status(thm)],[t43533]) ).
cnf(t950,plain,
meet(meet(X1,b),b) = meet(meet(X1,b),join(a,meet(X1,b))),
inference(cp,[status(thm)],[t190,t936]) ).
cnf(t43534,plain,
meet(b,meet(X1,b)) = meet(meet(X1,b),join(a,meet(X1,b))),
inference(step,[status(thm)],[t950,t24]) ).
cnf(t43535,plain,
meet(X1,meet(b,b)) = meet(meet(X1,b),join(a,meet(X1,b))),
inference(step,[status(thm)],[t43534,t27]) ).
cnf(t43536,plain,
meet(X1,b) = meet(meet(X1,b),join(a,meet(X1,b))),
inference(step,[status(thm)],[t43535,t14]) ).
cnf(t959,plain,
meet(meet(X1,b),join(a,meet(X1,b))) = meet(X1,b),
inference(orient,[status(thm)],[t43536]) ).
cnf(t6673,plain,
meet(meet(X1,b),join(join(a,meet(X1,b)),X2)) = join(meet(X1,b),meet(meet(X1,b),join(join(a,meet(X1,b)),X2))),
inference(cp,[status(thm)],[t6654,t959]) ).
cnf(t43873,plain,
meet(meet(X1,b),join(X2,join(a,meet(X1,b)))) = join(meet(X1,b),meet(meet(X1,b),join(join(a,meet(X1,b)),X2))),
inference(step,[status(thm)],[t6673,t73]) ).
cnf(t43874,plain,
meet(meet(X1,b),join(X2,join(a,meet(X1,b)))) = meet(X1,b),
inference(step,[status(thm)],[t43873,t17]) ).
cnf(t8010,plain,
meet(meet(X1,b),join(X2,join(a,meet(X1,b)))) = meet(X1,b),
inference(orient,[status(thm)],[t43874]) ).
cnf(t8011,plain,
meet(b,b) = meet(b,join(X1,join(a,meet(b,b)))),
inference(cp,[status(thm)],[t8010,t14]) ).
cnf(t43875,plain,
b = meet(b,join(X1,join(a,meet(b,b)))),
inference(step,[status(thm)],[t8011,t14]) ).
cnf(t43876,plain,
b = meet(b,join(X1,join(a,b))),
inference(step,[status(thm)],[t43875,t14]) ).
cnf(t43877,plain,
b = meet(b,join(X1,join(b,a))),
inference(step,[status(thm)],[t43876,t73]) ).
cnf(t43878,plain,
b = meet(b,join(X1,b)),
inference(step,[status(thm)],[t43877,t116]) ).
cnf(t8073,plain,
meet(b,join(X1,b)) = b,
inference(orient,[status(thm)],[t43878]) ).
cnf(t38393,plain,
meet(b,meet(join(X1,b),a)) = meet(b,meet(a,join(b,meet(join(X1,b),X2)))),
inference(cp,[status(thm)],[t38151,t8073]) ).
cnf(t44495,plain,
meet(b,meet(a,join(X1,b))) = meet(b,meet(a,join(b,meet(join(X1,b),X2)))),
inference(step,[status(thm)],[t38393,t24]) ).
cnf(t6731,plain,
a = meet(a,meet(b,join(X1,a))),
inference(cp,[status(thm)],[t15,t6726]) ).
cnf(t43811,plain,
a = meet(b,meet(join(X1,a),a)),
inference(step,[status(thm)],[t6731,t27]) ).
cnf(t43812,plain,
a = meet(b,meet(a,join(X1,a))),
inference(step,[status(thm)],[t43811,t24]) ).
cnf(t6759,plain,
meet(b,meet(a,join(X1,a))) = a,
inference(orient,[status(thm)],[t43812]) ).
cnf(t6761,plain,
meet(a,join(X1,a)) = join(meet(a,join(X1,a)),a),
inference(cp,[status(thm)],[t6475,t6759]) ).
cnf(t43814,plain,
meet(a,join(X1,a)) = join(a,meet(a,join(X1,a))),
inference(step,[status(thm)],[t6761,t73]) ).
cnf(t43815,plain,
meet(a,join(X1,a)) = a,
inference(step,[status(thm)],[t43814,t17]) ).
cnf(t6858,plain,
meet(a,join(X1,a)) = a,
inference(orient,[status(thm)],[t43815]) ).
cnf(t6862,plain,
meet(a,join(join(X1,a),X2)) = join(a,meet(a,join(join(X1,a),X2))),
inference(cp,[status(thm)],[t6654,t6858]) ).
cnf(t43816,plain,
meet(a,join(X2,join(X1,a))) = join(a,meet(a,join(join(X1,a),X2))),
inference(step,[status(thm)],[t6862,t73]) ).
cnf(t43817,plain,
meet(a,join(X1,join(a,X2))) = join(a,meet(a,join(join(X1,a),X2))),
inference(step,[status(thm)],[t43816,t79]) ).
cnf(t43818,plain,
meet(a,join(X1,join(X2,a))) = join(a,meet(a,join(join(X1,a),X2))),
inference(step,[status(thm)],[t43817,t73]) ).
cnf(t43819,plain,
meet(a,join(X1,join(X2,a))) = a,
inference(step,[status(thm)],[t43818,t17]) ).
cnf(t6914,plain,
meet(a,join(X1,join(X2,a))) = a,
inference(orient,[status(thm)],[t43819]) ).
cnf(t6917,plain,
a = meet(a,join(X1,b)),
inference(cp,[status(thm)],[t6914,t116]) ).
cnf(t6976,plain,
meet(a,join(X1,b)) = a,
inference(orient,[status(thm)],[t6917]) ).
cnf(t44496,plain,
meet(b,a) = meet(b,meet(a,join(b,meet(join(X1,b),X2)))),
inference(step,[status(thm)],[t44495,t6976]) ).
cnf(t44497,plain,
a = meet(b,meet(a,join(b,meet(join(X1,b),X2)))),
inference(step,[status(thm)],[t44496,t68]) ).
cnf(t202,plain,
meet(X1,meet(meet(X2,join(X1,X3)),Y3)) = meet(Y3,meet(X1,X2)),
inference(cp,[status(thm)],[t27,t190]) ).
cnf(t43386,plain,
meet(X1,meet(Y3,meet(X2,join(X1,X3)))) = meet(Y3,meet(X1,X2)),
inference(step,[status(thm)],[t202,t24]) ).
cnf(t43387,plain,
meet(X1,meet(X2,meet(join(X1,X3),Y3))) = meet(Y3,meet(X1,X2)),
inference(step,[status(thm)],[t43386,t27]) ).
cnf(t43388,plain,
meet(X1,meet(X2,meet(Y3,join(X1,X3)))) = meet(Y3,meet(X1,X2)),
inference(step,[status(thm)],[t43387,t24]) ).
cnf(t43389,plain,
meet(X1,meet(X2,meet(Y3,join(X1,X3)))) = meet(X2,meet(Y3,X1)),
inference(step,[status(thm)],[t43388,t27]) ).
cnf(t43390,plain,
meet(X1,meet(X2,meet(Y3,join(X1,X3)))) = meet(X1,meet(X2,Y3)),
inference(step,[status(thm)],[t43389,t27]) ).
cnf(t295,plain,
meet(X1,meet(X2,meet(X3,join(X1,Y3)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t43390]) ).
cnf(t24459,plain,
meet(a,join(X1,X2)) = meet(b,meet(a,join(X1,X2))),
inference(cp,[status(thm)],[t24458,t295]) ).
cnf(t25329,plain,
meet(b,meet(a,join(X1,X2))) = meet(a,join(X1,X2)),
inference(orient,[status(thm)],[t24459]) ).
cnf(t44498,plain,
a = meet(a,join(b,meet(join(X1,b),X2))),
inference(step,[status(thm)],[t44497,t25329]) ).
cnf(t44499,plain,
a = meet(a,join(b,meet(X2,join(X1,b)))),
inference(step,[status(thm)],[t44498,t24]) ).
cnf(t38981,plain,
meet(a,join(b,meet(X1,join(X2,b)))) = a,
inference(orient,[status(thm)],[t44499]) ).
cnf(t6515,plain,
join(meet(X1,X2),join(X3,X2)) = join(X3,X2),
inference(cp,[status(thm)],[t79,t6475]) ).
cnf(t43804,plain,
join(X2,join(meet(X1,X2),X3)) = join(X3,X2),
inference(step,[status(thm)],[t6515,t79]) ).
cnf(t43805,plain,
join(X2,join(X3,meet(X1,X2))) = join(X3,X2),
inference(step,[status(thm)],[t43804,t73]) ).
cnf(t43806,plain,
join(X2,join(X3,meet(X1,X2))) = join(X2,X3),
inference(step,[status(thm)],[t43805,t73]) ).
cnf(t6517,plain,
join(X1,join(X2,meet(X3,X1))) = join(X1,X2),
inference(orient,[status(thm)],[t43806]) ).
cnf(t16242,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(cp,[status(thm)],[t16217,t6517]) ).
cnf(t16344,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t16242]) ).
cnf(t38988,plain,
a = meet(a,join(b,meet(X1,X2))),
inference(cp,[status(thm)],[t38981,t16344]) ).
cnf(t39094,plain,
meet(a,join(b,meet(X1,X2))) = a,
inference(orient,[status(thm)],[t38988]) ).
cnf(t16359,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),Y3)),
inference(cp,[status(thm)],[t16344,t190]) ).
cnf(t44119,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),Y3)),
inference(step,[status(thm)],[t16359,t190]) ).
cnf(t44120,plain,
meet(X1,X2) = meet(meet(X1,X2),join(Y3,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t44119,t73]) ).
cnf(t17208,plain,
meet(meet(X1,X2),join(X3,meet(X2,join(X1,Y3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t44120]) ).
cnf(t17324,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y3,meet(X2,X3))),
inference(cp,[status(thm)],[t17208,t15667]) ).
cnf(t22615,plain,
meet(meet(X1,meet(X2,X3)),join(Y3,meet(X2,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t17324]) ).
cnf(t11531,plain,
meet(one,join(X1,X2)) = meet(one,meet(join(X1,X2),join(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t11456,t2379]) ).
cnf(t44066,plain,
join(X1,X2) = meet(one,meet(join(X1,X2),join(X3,join(X1,X2)))),
inference(step,[status(thm)],[t11531,t2379]) ).
cnf(t44067,plain,
join(X1,X2) = meet(one,meet(join(X1,X2),join(X2,join(X3,X1)))),
inference(step,[status(thm)],[t44066,t79]) ).
cnf(t44068,plain,
join(X1,X2) = meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t44067,t79]) ).
cnf(t14138,plain,
meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))) = join(X1,X2),
inference(orient,[status(thm)],[t44068]) ).
cnf(t15686,plain,
meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))) = meet(join(X1,X2),join(Y3,meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))))),
inference(cp,[status(thm)],[t15667,t14138]) ).
cnf(t44099,plain,
join(X1,X2) = meet(join(X1,X2),join(Y3,meet(one,meet(join(X1,X2),join(X1,join(X2,X3)))))),
inference(step,[status(thm)],[t15686,t14138]) ).
cnf(t44100,plain,
join(X1,X2) = meet(join(X1,X2),join(Y3,join(X1,X2))),
inference(step,[status(thm)],[t44099,t14138]) ).
cnf(t44101,plain,
join(X1,X2) = meet(join(X1,X2),join(X2,join(Y3,X1))),
inference(step,[status(thm)],[t44100,t79]) ).
cnf(t44102,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,Y3))),
inference(step,[status(thm)],[t44101,t79]) ).
cnf(t15810,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t44102]) ).
cnf(t22660,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)],[t22615,t15810]) ).
cnf(t44377,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)],[t22660,t15810]) ).
cnf(t44378,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,join(X2,X3))),
inference(step,[status(thm)],[t44377,t15810]) ).
cnf(t44379,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X3,join(Y4,X2))),
inference(step,[status(thm)],[t44378,t79]) ).
cnf(t44380,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,join(X3,Y4))),
inference(step,[status(thm)],[t44379,t79]) ).
cnf(t30885,plain,
meet(meet(X1,join(X2,X3)),join(X2,join(X3,Y3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t44380]) ).
cnf(t31062,plain,
join(X1,join(X2,X3)) = join(join(X1,join(X2,X3)),meet(Y3,join(X1,X2))),
inference(cp,[status(thm)],[t6475,t30885]) ).
cnf(t44446,plain,
join(X1,join(X2,X3)) = join(meet(Y3,join(X1,X2)),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t31062,t73]) ).
cnf(t44447,plain,
join(X1,join(X2,X3)) = join(join(X2,X3),join(meet(Y3,join(X1,X2)),X1)),
inference(step,[status(thm)],[t44446,t79]) ).
cnf(t44448,plain,
join(X1,join(X2,X3)) = join(X1,join(join(X2,X3),meet(Y3,join(X1,X2)))),
inference(step,[status(thm)],[t44447,t79]) ).
cnf(t35357,plain,
join(X1,join(join(X2,X3),meet(Y3,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t44448]) ).
cnf(t35365,plain,
join(X1,join(X2,X2)) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t35357,t16]) ).
cnf(t44449,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t35365,t16]) ).
cnf(t35606,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t44449]) ).
cnf(t35610,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t35606,t11225]) ).
cnf(t35828,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t35610]) ).
cnf(t35842,plain,
join(X1,meet(X2,join(X3,meet(complement(X2),join(X3,X2))))) = join(X1,meet(X2,join(X1,meet(X3,X2)))),
inference(cp,[status(thm)],[t35828,t5804]) ).
cnf(t44452,plain,
join(X1,meet(X3,X2)) = join(X1,meet(X2,join(X1,meet(X3,X2)))),
inference(step,[status(thm)],[t35842,t5804]) ).
cnf(t36055,plain,
join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t44452]) ).
cnf(t11532,plain,
meet(one,complement(X1)) = meet(one,meet(complement(X1),join(X2,complement(X1)))),
inference(cp,[status(thm)],[t11456,t1150]) ).
cnf(t44012,plain,
complement(X1) = meet(one,meet(complement(X1),join(X2,complement(X1)))),
inference(step,[status(thm)],[t11532,t1150]) ).
cnf(t11857,plain,
meet(one,meet(complement(X1),join(X2,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t44012]) ).
cnf(t11918,plain,
meet(meet(complement(X1),join(X2,complement(X1))),meet(X3,one)) = meet(X3,complement(X1)),
inference(cp,[status(thm)],[t27,t11857]) ).
cnf(t44013,plain,
meet(meet(complement(X1),join(X2,complement(X1))),X3) = meet(X3,complement(X1)),
inference(step,[status(thm)],[t11918,t122]) ).
cnf(t44014,plain,
meet(X3,meet(complement(X1),join(X2,complement(X1)))) = meet(X3,complement(X1)),
inference(step,[status(thm)],[t44013,t24]) ).
cnf(t11919,plain,
meet(X1,meet(complement(X2),join(X3,complement(X2)))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t44014]) ).
cnf(t11920,plain,
meet(complement(X1),complement(X1)) = meet(complement(X1),join(X2,complement(X1))),
inference(cp,[status(thm)],[t11919,t127]) ).
cnf(t44015,plain,
complement(X1) = meet(complement(X1),join(X2,complement(X1))),
inference(step,[status(thm)],[t11920,t14]) ).
cnf(t11962,plain,
meet(complement(X1),join(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t44015]) ).
cnf(t36205,plain,
join(X1,meet(complement(X2),join(X3,complement(X2)))) = join(X1,meet(join(X3,complement(X2)),join(X1,complement(X2)))),
inference(cp,[status(thm)],[t36055,t11962]) ).
cnf(t44478,plain,
join(X1,complement(X2)) = join(X1,meet(join(X3,complement(X2)),join(X1,complement(X2)))),
inference(step,[status(thm)],[t36205,t11962]) ).
cnf(t44479,plain,
join(X1,complement(X2)) = join(X1,meet(join(X1,complement(X2)),join(X3,complement(X2)))),
inference(step,[status(thm)],[t44478,t24]) ).
cnf(t37529,plain,
join(X1,meet(join(X1,complement(X2)),join(X3,complement(X2)))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t44479]) ).
cnf(t39114,plain,
a = meet(a,join(b,complement(X1))),
inference(cp,[status(thm)],[t39094,t37529]) ).
cnf(t39277,plain,
meet(a,join(b,complement(X1))) = a,
inference(orient,[status(thm)],[t39114]) ).
cnf(t39281,plain,
join(b,complement(X1)) = join(join(b,complement(X1)),a),
inference(cp,[status(thm)],[t6475,t39277]) ).
cnf(t44500,plain,
join(b,complement(X1)) = join(a,join(b,complement(X1))),
inference(step,[status(thm)],[t39281,t73]) ).
cnf(t44501,plain,
join(b,complement(X1)) = join(b,join(complement(X1),a)),
inference(step,[status(thm)],[t44500,t79]) ).
cnf(t44502,plain,
join(b,complement(X1)) = join(b,join(a,complement(X1))),
inference(step,[status(thm)],[t44501,t73]) ).
cnf(t39378,plain,
join(b,join(a,complement(X1))) = join(b,complement(X1)),
inference(orient,[status(thm)],[t44502]) ).
cnf(t39379,plain,
join(b,complement(a)) = join(b,one),
inference(cp,[status(thm)],[t39378,t103]) ).
cnf(t44503,plain,
join(b,complement(a)) = one,
inference(step,[status(thm)],[t39379,t155]) ).
cnf(t39418,plain,
join(b,complement(a)) = one,
inference(orient,[status(thm)],[t44503]) ).
cnf(t39449,plain,
meet(b,complement(a)) = meet(b,join(complement(a),meet(complement(b),one))),
inference(cp,[status(thm)],[t5523,t39418]) ).
cnf(t44508,plain,
meet(b,complement(a)) = meet(b,join(complement(a),complement(b))),
inference(step,[status(thm)],[t39449,t122]) ).
cnf(t44509,plain,
meet(b,complement(a)) = meet(b,join(complement(b),complement(a))),
inference(step,[status(thm)],[t44508,t73]) ).
cnf(t39573,plain,
meet(b,join(complement(b),complement(a))) = meet(b,complement(a)),
inference(orient,[status(thm)],[t44509]) ).
cnf(t39583,plain,
meet(b,meet(join(complement(b),complement(a)),a)) = meet(a,meet(meet(b,complement(a)),join(X1,a))),
inference(cp,[status(thm)],[t26504,t39573]) ).
cnf(t44571,plain,
meet(b,meet(a,join(complement(b),complement(a)))) = meet(a,meet(meet(b,complement(a)),join(X1,a))),
inference(step,[status(thm)],[t39583,t24]) ).
cnf(t44572,plain,
meet(a,join(complement(b),complement(a))) = meet(a,meet(meet(b,complement(a)),join(X1,a))),
inference(step,[status(thm)],[t44571,t25329]) ).
cnf(t44573,plain,
meet(a,join(complement(b),complement(a))) = meet(b,meet(complement(a),a)),
inference(step,[status(thm)],[t44572,t26504]) ).
cnf(t44574,plain,
meet(a,join(complement(b),complement(a))) = meet(b,meet(a,complement(a))),
inference(step,[status(thm)],[t44573,t24]) ).
cnf(t44575,plain,
meet(a,join(complement(b),complement(a))) = meet(b,zero),
inference(step,[status(thm)],[t44574,t63]) ).
cnf(t44576,plain,
meet(a,join(complement(b),complement(a))) = zero,
inference(step,[status(thm)],[t44575,t138]) ).
cnf(t43198,plain,
meet(a,join(complement(b),complement(a))) = zero,
inference(orient,[status(thm)],[t44576]) ).
cnf(t43199,plain,
join(complement(b),complement(a)) = ifeq(zero,zero,ifeq(join(a,join(complement(b),complement(a))),one,complement(a),join(complement(b),complement(a))),join(complement(b),complement(a))),
inference(cp,[status(thm)],[t19,t43198]) ).
cnf(t44577,plain,
join(complement(b),complement(a)) = ifeq(join(a,join(complement(b),complement(a))),one,complement(a),join(complement(b),complement(a))),
inference(step,[status(thm)],[t43199,t18]) ).
cnf(t107,plain,
join(X1,join(complement(X1),X2)) = join(X2,one),
inference(cp,[status(thm)],[t79,t103]) ).
cnf(t43350,plain,
join(X1,join(X2,complement(X1))) = join(X2,one),
inference(step,[status(thm)],[t107,t73]) ).
cnf(t43351,plain,
join(X1,join(X2,complement(X1))) = one,
inference(step,[status(thm)],[t43350,t155]) ).
cnf(t181,plain,
join(X1,join(X2,complement(X1))) = one,
inference(orient,[status(thm)],[t43351]) ).
cnf(t44578,plain,
join(complement(b),complement(a)) = ifeq(one,one,complement(a),join(complement(b),complement(a))),
inference(step,[status(thm)],[t44577,t181]) ).
cnf(t44579,plain,
join(complement(b),complement(a)) = complement(a),
inference(step,[status(thm)],[t44578,t18]) ).
cnf(t43264,plain,
join(complement(b),complement(a)) = complement(a),
inference(orient,[status(thm)],[t44579]) ).
cnf(f13,negated_conjecture,
join(complement(b),complement(a)) != complement(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f13_nnf,plain,
join(complement(b),complement(a)) != complement(a),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
join(complement(b),complement(a)) != complement(a),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
join(complement(b),complement(a)) != complement(a),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
join(complement(b),complement(a)) != complement(a),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(g0_0,plain,
complement(a) != complement(a),
inference(rw,[status(thm)],[goal_0,t43264]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT257-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n009.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.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 20:42:28 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 46.97/6.45 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.97/6.45 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------