%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT066-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:55:07 PM UTC 2026
% Result : Unsatisfiable 26.62s 3.87s
% Output : Proof 26.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 85
% Number of leaves : 14
% Syntax : Number of formulae : 304 ( 300 unt; 0 def)
% Number of atoms : 312 ( 311 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-4 aty)
% Number of variables : 648 ( 79 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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(t6,plain,
join(X1,meet(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t14,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(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(t7,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t40,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t41,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t14,t40]) ).
cnf(t125,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t41]) ).
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(t10,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t57,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t129,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t125,t57]) ).
cnf(t275,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t129]) ).
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(t8,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t16,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(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(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t23,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t24,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t16,t23]) ).
cnf(t117,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t24]) ).
cnf(t127,plain,
join(X1,X2) = join(join(X1,X2),X1),
inference(cp,[status(thm)],[t125,t16]) ).
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(t9,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t26,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t99045,plain,
join(X1,X2) = join(X1,join(X2,X1)),
inference(step,[status(thm)],[t127,t26]) ).
cnf(t155,plain,
join(X1,join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t99045]) ).
cnf(t159,plain,
join(X1,X2) = meet(join(X1,X2),join(X2,X1)),
inference(cp,[status(thm)],[t117,t155]) ).
cnf(t430,plain,
meet(join(X1,X2),join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t159]) ).
cnf(t454,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X2,X1))),
inference(cp,[status(thm)],[t275,t430]) ).
cnf(t99105,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X2,X1)))),
inference(step,[status(thm)],[t454,t26]) ).
cnf(t3182,plain,
join(X1,join(X2,meet(X3,join(X2,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t99105]) ).
cnf(t119,plain,
meet(X1,X2) = meet(meet(X1,X2),X1),
inference(cp,[status(thm)],[t117,t14]) ).
cnf(t99044,plain,
meet(X1,X2) = meet(X1,meet(X2,X1)),
inference(step,[status(thm)],[t119,t57]) ).
cnf(t146,plain,
meet(X1,meet(X2,X1)) = meet(X1,X2),
inference(orient,[status(thm)],[t99044]) ).
cnf(t152,plain,
meet(X1,meet(meet(X2,X1),X3)) = meet(meet(X1,X2),X3),
inference(cp,[status(thm)],[t57,t146]) ).
cnf(t99093,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t152,t57]) ).
cnf(t99094,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t99093,t57]) ).
cnf(t1207,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t99094]) ).
cnf(t1260,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X3,X2))),
inference(cp,[status(thm)],[t275,t1207]) ).
cnf(t3631,plain,
join(meet(X1,X2),meet(X1,meet(X3,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t1260]) ).
cnf(t3687,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X1,X2)),
inference(cp,[status(thm)],[t3631,t16]) ).
cnf(t99239,plain,
meet(X1,join(X2,X3)) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t3687,t23]) ).
cnf(t29209,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t99239]) ).
cnf(f10,axiom,
( complement(A) = B
| meet(A,B) != n0
| join(A,B) != n1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complements_are_unique) ).
fof(f10_nnf,plain,
! [A,B] :
( complement(A) = B
| meet(A,B) != n0
| join(A,B) != n1 ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A,B] :
( complement(A) = B
| meet(A,B) != n0
| join(A,B) != n1 ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( complement(X0) = X1
| meet(X0,X1) != n0
| join(X0,X1) != n1 ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t11,plain,
ifeq(join(X1,X2),n1,ifeq(meet(X1,X2),n0,complement(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t18,plain,
ifeq(join(X1,X2),n1,ifeq(meet(X1,X2),n0,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(f11,axiom,
meet(A,join(B,join(C,meet(D,join(A,meet(B,C)))))) = meet(A,join(B,join(C,meet(A,D)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',g61) ).
fof(f11_nnf,plain,
! [A,B,C,D] : meet(A,join(B,join(C,meet(D,join(A,meet(B,C)))))) = meet(A,join(B,join(C,meet(A,D)))),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A,B,C,D] : meet(A,join(B,join(C,meet(D,join(A,meet(B,C)))))) = meet(A,join(B,join(C,meet(A,D)))),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(X1,join(X2,meet(X3,join(X0,meet(X1,X2)))))) = meet(X0,join(X1,join(X2,meet(X0,X3)))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t12,plain,
meet(X1,join(X2,join(X3,meet(X4,join(X1,meet(X2,X3)))))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t43,plain,
meet(X1,join(X2,join(X3,meet(X4,join(X1,meet(X2,X3)))))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t12]) ).
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(t13,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t30,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t26,t13]) ).
cnf(t134,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t30]) ).
cnf(t139,plain,
meet(X1,join(X2,join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X2,X2))))),
inference(cp,[status(thm)],[t43,t134]) ).
cnf(t99247,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,join(X1,meet(X2,X2))))),
inference(step,[status(thm)],[t139,t134]) ).
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(t15,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t99248,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t99247,t15]) ).
cnf(t33282,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t99248]) ).
cnf(f8,axiom,
join(A,complement(A)) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',top) ).
fof(f8_nnf,plain,
! [A] : join(A,complement(A)) = n1,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A] : join(A,complement(A)) = n1,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
join(X0,complement(X0)) = n1,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t2,plain,
join(X1,complement(X1)) = n1,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t35,plain,
join(X1,complement(X1)) = n1,
inference(orient,[status(thm)],[t2]) ).
cnf(t33358,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),meet(X2,n1))),
inference(cp,[status(thm)],[t33282,t35]) ).
cnf(t38,plain,
X1 = meet(X1,n1),
inference(cp,[status(thm)],[t16,t35]) ).
cnf(t75,plain,
meet(X1,n1) = X1,
inference(orient,[status(thm)],[t38]) ).
cnf(t99249,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t33358,t75]) ).
cnf(t33579,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),X2)),
inference(orient,[status(thm)],[t99249]) ).
cnf(f9,axiom,
meet(A,complement(A)) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bottom) ).
fof(f9_nnf,plain,
! [A] : meet(A,complement(A)) = n0,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A] : meet(A,complement(A)) = n0,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
meet(X0,complement(X0)) = n0,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t3,plain,
meet(X1,complement(X1)) = n0,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t70,plain,
meet(X1,complement(X1)) = n0,
inference(orient,[status(thm)],[t3]) ).
cnf(t73,plain,
meet(X1,meet(complement(X1),X2)) = meet(n0,X2),
inference(cp,[status(thm)],[t57,t70]) ).
cnf(t72,plain,
X1 = join(X1,n0),
inference(cp,[status(thm)],[t14,t70]) ).
cnf(t80,plain,
join(X1,n0) = X1,
inference(orient,[status(thm)],[t72]) ).
cnf(t81,plain,
X1 = join(n0,X1),
inference(cp,[status(thm)],[t80,t23]) ).
cnf(t94,plain,
join(n0,X1) = X1,
inference(orient,[status(thm)],[t81]) ).
cnf(t96,plain,
meet(n0,X1) = n0,
inference(cp,[status(thm)],[t94,t14]) ).
cnf(t107,plain,
meet(n0,X1) = n0,
inference(orient,[status(thm)],[t96]) ).
cnf(t99057,plain,
meet(X1,meet(complement(X1),X2)) = n0,
inference(step,[status(thm)],[t73,t107]) ).
cnf(t210,plain,
meet(X1,meet(complement(X1),X2)) = n0,
inference(orient,[status(thm)],[t99057]) ).
cnf(t213,plain,
meet(meet(complement(X1),X2),X1) = meet(meet(complement(X1),X2),n0),
inference(cp,[status(thm)],[t146,t210]) ).
cnf(t99058,plain,
meet(complement(X1),meet(X2,X1)) = meet(meet(complement(X1),X2),n0),
inference(step,[status(thm)],[t213,t57]) ).
cnf(t99059,plain,
meet(complement(X1),meet(X2,X1)) = meet(complement(X1),meet(X2,n0)),
inference(step,[status(thm)],[t99058,t57]) ).
cnf(t108,plain,
n0 = meet(X1,n0),
inference(cp,[status(thm)],[t107,t40]) ).
cnf(t114,plain,
meet(X1,n0) = n0,
inference(orient,[status(thm)],[t108]) ).
cnf(t99060,plain,
meet(complement(X1),meet(X2,X1)) = meet(complement(X1),n0),
inference(step,[status(thm)],[t99059,t114]) ).
cnf(t99061,plain,
meet(complement(X1),meet(X2,X1)) = n0,
inference(step,[status(thm)],[t99060,t114]) ).
cnf(t223,plain,
meet(complement(X1),meet(X2,X1)) = n0,
inference(orient,[status(thm)],[t99061]) ).
cnf(t228,plain,
n0 = meet(complement(join(X1,X2)),X1),
inference(cp,[status(thm)],[t223,t16]) ).
cnf(t99062,plain,
n0 = meet(X1,complement(join(X1,X2))),
inference(step,[status(thm)],[t228,t40]) ).
cnf(t237,plain,
meet(X1,complement(join(X1,X2))) = n0,
inference(orient,[status(thm)],[t99062]) ).
cnf(t33640,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = meet(X1,join(complement(X1),n0)),
inference(cp,[status(thm)],[t33579,t237]) ).
cnf(t99250,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t33640,t80]) ).
cnf(t99251,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = n0,
inference(step,[status(thm)],[t99250,t70]) ).
cnf(t33820,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = n0,
inference(orient,[status(thm)],[t99251]) ).
cnf(t33867,plain,
join(complement(X1),complement(join(X1,X2))) = ifeq(join(X1,join(complement(X1),complement(join(X1,X2)))),n1,ifeq(n0,n0,complement(X1),join(complement(X1),complement(join(X1,X2)))),join(complement(X1),complement(join(X1,X2)))),
inference(cp,[status(thm)],[t18,t33820]) ).
cnf(t37,plain,
join(X1,join(complement(X1),X2)) = join(n1,X2),
inference(cp,[status(thm)],[t26,t35]) ).
cnf(t76,plain,
X1 = meet(n1,X1),
inference(cp,[status(thm)],[t75,t40]) ).
cnf(t84,plain,
meet(n1,X1) = X1,
inference(orient,[status(thm)],[t76]) ).
cnf(t86,plain,
join(n1,X1) = n1,
inference(cp,[status(thm)],[t84,t16]) ).
cnf(t104,plain,
join(n1,X1) = n1,
inference(orient,[status(thm)],[t86]) ).
cnf(t99050,plain,
join(X1,join(complement(X1),X2)) = n1,
inference(step,[status(thm)],[t37,t104]) ).
cnf(t164,plain,
join(X1,join(complement(X1),X2)) = n1,
inference(orient,[status(thm)],[t99050]) ).
cnf(t99252,plain,
join(complement(X1),complement(join(X1,X2))) = ifeq(n1,n1,ifeq(n0,n0,complement(X1),join(complement(X1),complement(join(X1,X2)))),join(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t33867,t164]) ).
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(t99253,plain,
join(complement(X1),complement(join(X1,X2))) = ifeq(n0,n0,complement(X1),join(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t99252,t17]) ).
cnf(t99254,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(step,[status(thm)],[t99253,t17]) ).
cnf(t33971,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t99254]) ).
cnf(t28,plain,
join(X1,join(X2,meet(join(X1,X2),X3))) = join(X1,X2),
inference(cp,[status(thm)],[t26,t14]) ).
cnf(t2221,plain,
join(X1,join(X2,meet(join(X1,X2),X3))) = join(X1,X2),
inference(orient,[status(thm)],[t28]) ).
cnf(t32,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t26,t23]) ).
cnf(t99098,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t32,t26]) ).
cnf(t1687,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t99098]) ).
cnf(t2223,plain,
join(X1,X2) = join(X2,join(X1,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t2221,t1687]) ).
cnf(t4114,plain,
join(X1,join(X2,meet(join(X2,X1),X3))) = join(X2,X1),
inference(orient,[status(thm)],[t2223]) ).
cnf(t33973,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t33971,t4114]) ).
cnf(t34384,plain,
join(complement(X1),complement(join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t33973]) ).
cnf(t34430,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X2)),
inference(cp,[status(thm)],[t117,t34384]) ).
cnf(t99260,plain,
complement(join(X1,X2)) = meet(complement(X2),complement(join(X1,X2))),
inference(step,[status(thm)],[t34430,t40]) ).
cnf(t35538,plain,
meet(complement(X1),complement(join(X2,X1))) = complement(join(X2,X1)),
inference(orient,[status(thm)],[t99260]) ).
cnf(t71,plain,
n0 = meet(X1,meet(X2,complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t70,t57]) ).
cnf(t563,plain,
meet(X1,meet(X2,complement(meet(X1,X2)))) = n0,
inference(orient,[status(thm)],[t71]) ).
cnf(t33634,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(X1,join(complement(X1),n0)),
inference(cp,[status(thm)],[t33579,t563]) ).
cnf(t99338,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t33634,t80]) ).
cnf(t99339,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = n0,
inference(step,[status(thm)],[t99338,t70]) ).
cnf(t66650,plain,
meet(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))) = n0,
inference(orient,[status(thm)],[t99339]) ).
cnf(t66809,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = ifeq(join(X1,join(complement(X1),meet(X2,complement(meet(X1,X2))))),n1,ifeq(n0,n0,complement(X1),join(complement(X1),meet(X2,complement(meet(X1,X2))))),join(complement(X1),meet(X2,complement(meet(X1,X2))))),
inference(cp,[status(thm)],[t18,t66650]) ).
cnf(t99340,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = ifeq(n1,n1,ifeq(n0,n0,complement(X1),join(complement(X1),meet(X2,complement(meet(X1,X2))))),join(complement(X1),meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t66809,t164]) ).
cnf(t99341,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = ifeq(n0,n0,complement(X1),join(complement(X1),meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t99340,t17]) ).
cnf(t99342,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = complement(X1),
inference(step,[status(thm)],[t99341,t17]) ).
cnf(t66924,plain,
join(complement(X1),meet(X2,complement(meet(X1,X2)))) = complement(X1),
inference(orient,[status(thm)],[t99342]) ).
cnf(t67043,plain,
complement(join(complement(X1),meet(X2,complement(meet(X1,X2))))) = meet(complement(meet(X2,complement(meet(X1,X2)))),complement(complement(X1))),
inference(cp,[status(thm)],[t35538,t66924]) ).
cnf(t99344,plain,
complement(complement(X1)) = meet(complement(meet(X2,complement(meet(X1,X2)))),complement(complement(X1))),
inference(step,[status(thm)],[t67043,t66924]) ).
cnf(t25,plain,
X1 = ifeq(join(X1,X2),n1,ifeq(meet(X2,X1),n0,complement(X2),X1),X1),
inference(cp,[status(thm)],[t18,t23]) ).
cnf(t10304,plain,
ifeq(join(X1,X2),n1,ifeq(meet(X2,X1),n0,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t25]) ).
cnf(t10352,plain,
X1 = ifeq(n1,n1,ifeq(meet(complement(X1),X1),n0,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t10304,t35]) ).
cnf(t99209,plain,
X1 = ifeq(meet(complement(X1),X1),n0,complement(complement(X1)),X1),
inference(step,[status(thm)],[t10352,t17]) ).
cnf(t99210,plain,
X1 = ifeq(meet(X1,complement(X1)),n0,complement(complement(X1)),X1),
inference(step,[status(thm)],[t99209,t40]) ).
cnf(t99211,plain,
X1 = ifeq(n0,n0,complement(complement(X1)),X1),
inference(step,[status(thm)],[t99210,t70]) ).
cnf(t99212,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t99211,t17]) ).
cnf(t18817,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t99212]) ).
cnf(t99345,plain,
X1 = meet(complement(meet(X2,complement(meet(X1,X2)))),complement(complement(X1))),
inference(step,[status(thm)],[t99344,t18817]) ).
cnf(t99346,plain,
X1 = meet(complement(complement(X1)),complement(meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t99345,t40]) ).
cnf(t99347,plain,
X1 = meet(X1,complement(meet(X2,complement(meet(X1,X2))))),
inference(step,[status(thm)],[t99346,t18817]) ).
cnf(t67482,plain,
meet(X1,complement(meet(X2,complement(meet(X1,X2))))) = X1,
inference(orient,[status(thm)],[t99347]) ).
cnf(t230,plain,
n0 = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t223,t117]) ).
cnf(t99063,plain,
n0 = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t230,t40]) ).
cnf(t245,plain,
meet(X1,complement(join(X2,X1))) = n0,
inference(orient,[status(thm)],[t99063]) ).
cnf(t248,plain,
n0 = meet(X1,complement(join(X2,join(X3,X1)))),
inference(cp,[status(thm)],[t245,t26]) ).
cnf(t834,plain,
meet(X1,complement(join(X2,join(X3,X1)))) = n0,
inference(orient,[status(thm)],[t248]) ).
cnf(t151,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X2,X1)),
inference(cp,[status(thm)],[t125,t146]) ).
cnf(t401,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X1,X2),
inference(orient,[status(thm)],[t151]) ).
cnf(t846,plain,
n0 = meet(meet(X1,X2),complement(join(X3,meet(X2,X1)))),
inference(cp,[status(thm)],[t834,t401]) ).
cnf(t99168,plain,
n0 = meet(X1,meet(X2,complement(join(X3,meet(X2,X1))))),
inference(step,[status(thm)],[t846,t57]) ).
cnf(t9843,plain,
meet(X1,meet(X2,complement(join(X3,meet(X2,X1))))) = n0,
inference(orient,[status(thm)],[t99168]) ).
cnf(t33993,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t117,t33971]) ).
cnf(t99256,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t33993,t40]) ).
cnf(t34541,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t99256]) ).
cnf(t34660,plain,
n0 = meet(X1,complement(join(X2,meet(complement(X2),X1)))),
inference(cp,[status(thm)],[t9843,t34541]) ).
cnf(t37898,plain,
meet(X1,complement(join(X2,meet(complement(X2),X1)))) = n0,
inference(orient,[status(thm)],[t34660]) ).
cnf(t67493,plain,
X1 = meet(X1,complement(meet(complement(join(X2,meet(complement(X2),X1))),complement(n0)))),
inference(cp,[status(thm)],[t67482,t37898]) ).
cnf(t99348,plain,
X1 = meet(X1,complement(meet(complement(n0),complement(join(X2,meet(complement(X2),X1)))))),
inference(step,[status(thm)],[t67493,t40]) ).
cnf(t95,plain,
complement(n0) = n1,
inference(cp,[status(thm)],[t94,t35]) ).
cnf(t102,plain,
complement(n0) = n1,
inference(orient,[status(thm)],[t95]) ).
cnf(t99349,plain,
X1 = meet(X1,complement(meet(n1,complement(join(X2,meet(complement(X2),X1)))))),
inference(step,[status(thm)],[t99348,t102]) ).
cnf(t99350,plain,
X1 = meet(X1,complement(complement(join(X2,meet(complement(X2),X1))))),
inference(step,[status(thm)],[t99349,t84]) ).
cnf(t99351,plain,
X1 = meet(X1,join(X2,meet(complement(X2),X1))),
inference(step,[status(thm)],[t99350,t18817]) ).
cnf(t67810,plain,
meet(X1,join(X2,meet(complement(X2),X1))) = X1,
inference(orient,[status(thm)],[t99351]) ).
cnf(t67950,plain,
meet(X1,join(join(X2,meet(complement(X2),X1)),X3)) = join(X1,meet(X1,join(join(X2,meet(complement(X2),X1)),X3))),
inference(cp,[status(thm)],[t29209,t67810]) ).
cnf(t99401,plain,
meet(X1,join(X2,join(meet(complement(X2),X1),X3))) = join(X1,meet(X1,join(join(X2,meet(complement(X2),X1)),X3))),
inference(step,[status(thm)],[t67950,t26]) ).
cnf(t99402,plain,
meet(X1,join(X2,join(meet(complement(X2),X1),X3))) = X1,
inference(step,[status(thm)],[t99401,t14]) ).
cnf(t72953,plain,
meet(X1,join(X2,join(meet(complement(X2),X1),X3))) = X1,
inference(orient,[status(thm)],[t99402]) ).
cnf(t73246,plain,
join(join(meet(complement(X1),X2),X3),X1) = join(join(meet(complement(X1),X2),X3),join(X1,X2)),
inference(cp,[status(thm)],[t3182,t72953]) ).
cnf(t99403,plain,
join(meet(complement(X1),X2),join(X3,X1)) = join(join(meet(complement(X1),X2),X3),join(X1,X2)),
inference(step,[status(thm)],[t73246,t26]) ).
cnf(t29,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t26,t23]) ).
cnf(t1517,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t29]) ).
cnf(t1538,plain,
join(join(X1,X2),join(X3,X2)) = join(X3,join(X2,X1)),
inference(cp,[status(thm)],[t1517,t155]) ).
cnf(t99100,plain,
join(X1,join(X2,join(X3,X2))) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t1538,t26]) ).
cnf(t99101,plain,
join(X1,join(X2,X3)) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t99100,t155]) ).
cnf(t2034,plain,
join(X1,join(X2,X3)) = join(X3,join(X2,X1)),
inference(orient,[status(thm)],[t99101]) ).
cnf(t99404,plain,
join(X1,join(X3,meet(complement(X1),X2))) = join(join(meet(complement(X1),X2),X3),join(X1,X2)),
inference(step,[status(thm)],[t99403,t2034]) ).
cnf(t99405,plain,
join(X1,join(X3,meet(complement(X1),X2))) = join(meet(complement(X1),X2),join(X3,join(X1,X2))),
inference(step,[status(thm)],[t99404,t26]) ).
cnf(t130,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t26,t125]) ).
cnf(t373,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t130]) ).
cnf(t1534,plain,
join(join(meet(X1,X2),X3),join(X4,X2)) = join(X4,join(X2,X3)),
inference(cp,[status(thm)],[t1517,t373]) ).
cnf(t99230,plain,
join(meet(X1,X2),join(X3,join(X4,X2))) = join(X4,join(X2,X3)),
inference(step,[status(thm)],[t1534,t26]) ).
cnf(t24778,plain,
join(meet(X1,X2),join(X3,join(X4,X2))) = join(X4,join(X2,X3)),
inference(orient,[status(thm)],[t99230]) ).
cnf(t99406,plain,
join(X1,join(X3,meet(complement(X1),X2))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t99405,t24778]) ).
cnf(t73284,plain,
join(X1,join(X2,meet(complement(X1),X3))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t99406]) ).
cnf(t73285,plain,
join(X1,join(X2,X1)) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t73284,t134]) ).
cnf(t99408,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(step,[status(thm)],[t73285,t155]) ).
cnf(t73671,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t99408]) ).
cnf(t73722,plain,
join(X1,meet(X2,meet(complement(X1),X3))) = join(X1,meet(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t73671,t1207]) ).
cnf(t99437,plain,
join(X1,meet(X2,meet(complement(X1),X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t73722,t73671]) ).
cnf(t80073,plain,
join(X1,meet(X2,meet(complement(X1),X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t99437]) ).
cnf(t66925,plain,
complement(complement(X1)) = join(X1,meet(X2,complement(meet(complement(X1),X2)))),
inference(cp,[status(thm)],[t66924,t18817]) ).
cnf(t99343,plain,
X1 = join(X1,meet(X2,complement(meet(complement(X1),X2)))),
inference(step,[status(thm)],[t66925,t18817]) ).
cnf(t67201,plain,
join(X1,meet(X2,complement(meet(complement(X1),X2)))) = X1,
inference(orient,[status(thm)],[t99343]) ).
cnf(t73302,plain,
join(X1,join(complement(meet(complement(X2),complement(X1))),X2)) = join(X1,X2),
inference(cp,[status(thm)],[t73284,t67201]) ).
cnf(t99466,plain,
join(X1,join(X2,complement(meet(complement(X2),complement(X1))))) = join(X1,X2),
inference(step,[status(thm)],[t73302,t23]) ).
cnf(t34404,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t34384,t14]) ).
cnf(t99257,plain,
complement(meet(X1,X2)) = join(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t34404,t23]) ).
cnf(t34672,plain,
join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t99257]) ).
cnf(t34673,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(meet(complement(X1),X2))),
inference(cp,[status(thm)],[t34672,t18817]) ).
cnf(t35960,plain,
join(X1,complement(meet(complement(X1),X2))) = complement(meet(complement(X1),X2)),
inference(orient,[status(thm)],[t34673]) ).
cnf(t99467,plain,
join(X1,complement(meet(complement(X2),complement(X1)))) = join(X1,X2),
inference(step,[status(thm)],[t99466,t35960]) ).
cnf(t34696,plain,
complement(X1) = meet(complement(X1),complement(meet(X1,X2))),
inference(cp,[status(thm)],[t16,t34672]) ).
cnf(t34807,plain,
meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t34696]) ).
cnf(t34808,plain,
complement(complement(X1)) = meet(X1,complement(meet(complement(X1),X2))),
inference(cp,[status(thm)],[t34807,t18817]) ).
cnf(t99258,plain,
X1 = meet(X1,complement(meet(complement(X1),X2))),
inference(step,[status(thm)],[t34808,t18817]) ).
cnf(t34937,plain,
meet(X1,complement(meet(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t99258]) ).
cnf(t59,plain,
meet(X1,meet(X2,join(meet(X1,X2),X3))) = meet(X1,X2),
inference(cp,[status(thm)],[t57,t16]) ).
cnf(t2338,plain,
meet(X1,meet(X2,join(meet(X1,X2),X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t59]) ).
cnf(t65,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t57,t40]) ).
cnf(t99099,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t65,t57]) ).
cnf(t1946,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t99099]) ).
cnf(t2340,plain,
meet(X1,X2) = meet(X2,meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t2338,t1946]) ).
cnf(t4265,plain,
meet(X1,meet(X2,join(meet(X2,X1),X3))) = meet(X2,X1),
inference(orient,[status(thm)],[t2340]) ).
cnf(t34939,plain,
X1 = meet(X1,complement(meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t34937,t4265]) ).
cnf(t35076,plain,
meet(X1,complement(meet(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t34939]) ).
cnf(t35081,plain,
complement(meet(X1,complement(X2))) = join(complement(meet(X1,complement(X2))),X2),
inference(cp,[status(thm)],[t125,t35076]) ).
cnf(t99263,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(meet(X1,complement(X2)))),
inference(step,[status(thm)],[t35081,t23]) ).
cnf(t36095,plain,
join(X1,complement(meet(X2,complement(X1)))) = complement(meet(X2,complement(X1))),
inference(orient,[status(thm)],[t99263]) ).
cnf(t99468,plain,
complement(meet(complement(X2),complement(X1))) = join(X1,X2),
inference(step,[status(thm)],[t99467,t36095]) ).
cnf(t91919,plain,
complement(meet(complement(X1),complement(X2))) = join(X2,X1),
inference(orient,[status(thm)],[t99468]) ).
cnf(t91962,plain,
join(X1,complement(X2)) = complement(meet(X2,complement(X1))),
inference(cp,[status(thm)],[t91919,t18817]) ).
cnf(t92221,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t91962]) ).
cnf(t92256,plain,
meet(X1,complement(X2)) = complement(join(X2,complement(X1))),
inference(cp,[status(thm)],[t18817,t92221]) ).
cnf(t92949,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t92256]) ).
cnf(t92966,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t92949,t23]) ).
cnf(t93142,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t92966]) ).
cnf(t73314,plain,
join(X1,join(X2,meet(X2,complement(X1)))) = join(X1,meet(X2,complement(X1))),
inference(cp,[status(thm)],[t73284,t401]) ).
cnf(t99410,plain,
join(X1,X2) = join(X1,meet(X2,complement(X1))),
inference(step,[status(thm)],[t73314,t14]) ).
cnf(t73939,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t99410]) ).
cnf(t73964,plain,
join(complement(X1),X2) = join(complement(X1),meet(X2,X1)),
inference(cp,[status(thm)],[t73939,t18817]) ).
cnf(t74443,plain,
join(complement(X1),meet(X2,X1)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t73964]) ).
cnf(t93155,plain,
meet(X1,complement(meet(X2,X1))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t93142,t74443]) ).
cnf(t99533,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t93155,t93142]) ).
cnf(t93617,plain,
meet(X1,complement(meet(X2,X1))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t99533]) ).
cnf(t92250,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t92221,t40]) ).
cnf(t92482,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t92250]) ).
cnf(t93621,plain,
meet(X1,complement(complement(X2))) = meet(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t93617,t92482]) ).
cnf(t99534,plain,
meet(X1,X2) = meet(X1,join(X2,complement(X1))),
inference(step,[status(thm)],[t93621,t18817]) ).
cnf(t93892,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t99534]) ).
cnf(t93993,plain,
join(X1,meet(X2,join(X3,complement(complement(X1))))) = join(X1,meet(X2,meet(complement(X1),X3))),
inference(cp,[status(thm)],[t80073,t93892]) ).
cnf(t99549,plain,
join(X1,meet(X2,join(X3,X1))) = join(X1,meet(X2,meet(complement(X1),X3))),
inference(step,[status(thm)],[t93993,t18817]) ).
cnf(t99550,plain,
join(X1,meet(X2,join(X3,X1))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t99549,t80073]) ).
cnf(t96045,plain,
join(X1,meet(X2,join(X3,X1))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t99550]) ).
cnf(t93908,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t93892,t23]) ).
cnf(t94053,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t93908]) ).
cnf(t73456,plain,
join(complement(X1),join(X2,X3)) = join(complement(X1),join(X3,meet(X1,X2))),
inference(cp,[status(thm)],[t73284,t18817]) ).
cnf(t81214,plain,
join(complement(X1),join(X2,meet(X1,X3))) = join(complement(X1),join(X3,X2)),
inference(orient,[status(thm)],[t73456]) ).
cnf(t94064,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(complement(X1),join(X3,X2))),
inference(cp,[status(thm)],[t94053,t81214]) ).
cnf(t99556,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X3,X2)),
inference(step,[status(thm)],[t94064,t94053]) ).
cnf(t97103,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t99556]) ).
cnf(t97291,plain,
join(meet(X1,X2),meet(X1,X3)) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t96045,t97103]) ).
cnf(t99560,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t97291,t29209]) ).
cnf(t98540,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t99560]) ).
cnf(f12,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f12_nnf,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(goal_0,negated_conjecture,
join(meet(a,b),meet(a,c)) != meet(a,join(b,c)),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(g0_0,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[goal_0,t98540]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT066-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n019.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % 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:09:35 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 26.62/3.87 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.62/3.87 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------