%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT235-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n012.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:22 PM UTC 2026
% Result : Unsatisfiable 11.80s 1.98s
% Output : Proof 11.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 111
% Number of leaves : 15
% Syntax : Number of formulae : 306 ( 302 unt; 0 def)
% Number of atoms : 314 ( 313 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 : 618 ( 126 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f3,axiom,
join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f3_nnf,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(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(f10,axiom,
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f10_nnf,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( complement(X0) = X1
| join(X0,X1) != one
| meet(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t12,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t19,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(f11,axiom,
meet(X,join(Y,meet(Z,U))) = meet(X,join(Y,meet(Z,join(Y,meet(U,join(Y,Z)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H34) ).
fof(f11_nnf,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,U))) = meet(X,join(Y,meet(Z,join(Y,meet(U,join(Y,Z)))))),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,U))) = meet(X,join(Y,meet(Z,join(Y,meet(U,join(Y,Z)))))),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(X1,meet(X2,X3))) = meet(X0,join(X1,meet(X2,join(X1,meet(X3,join(X1,X2)))))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t13,plain,
meet(X1,join(X2,meet(X3,join(X2,meet(X4,join(X2,X3)))))) = meet(X1,join(X2,meet(X3,X4))),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t47,plain,
meet(X1,join(X2,meet(X3,join(X2,meet(X4,join(X2,X3)))))) = meet(X1,join(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t13]) ).
cnf(f7,axiom,
join(join(X,Y),Z) = join(X,join(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f7_nnf,plain,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t10,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(f5,axiom,
join(X,Y) = join(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f5_nnf,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t6,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t68,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t6450,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t10,t68]) ).
cnf(t72,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t6450]) ).
cnf(f1,axiom,
join(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f1_nnf,plain,
! [X] : join(X,X) = X,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] : join(X,X) = X,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t0,plain,
join(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t16,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t75,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t72,t16]) ).
cnf(t6454,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t75,t72]) ).
cnf(t6455,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t6454,t68]) ).
cnf(t130,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t6455]) ).
cnf(f8,axiom,
join(X,complement(X)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f8_nnf,plain,
! [X] : join(X,complement(X)) = one,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] : join(X,complement(X)) = one,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
join(X0,complement(X0)) = one,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t3,plain,
join(X1,complement(X1)) = one,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t94,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t133,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t130,t94]) ).
cnf(t6456,plain,
one = join(X1,one),
inference(step,[status(thm)],[t133,t94]) ).
cnf(t141,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t6456]) ).
cnf(t144,plain,
meet(X1,join(X2,meet(one,X3))) = meet(X1,join(X2,meet(one,join(X2,meet(X3,one))))),
inference(cp,[status(thm)],[t47,t141]) ).
cnf(f4,axiom,
meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f4_nnf,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t8,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t24,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t6503,plain,
meet(X1,join(X2,meet(X3,one))) = meet(X1,join(X2,meet(one,join(X2,meet(X3,one))))),
inference(step,[status(thm)],[t144,t24]) ).
cnf(f2,axiom,
meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f2_nnf,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t9,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t15,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t95,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t15,t94]) ).
cnf(t110,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t95]) ).
cnf(t6504,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(one,join(X2,meet(X3,one))))),
inference(step,[status(thm)],[t6503,t110]) ).
cnf(t6505,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(one,join(X2,X3)))),
inference(step,[status(thm)],[t6504,t110]) ).
cnf(t286,plain,
meet(X1,join(X2,meet(one,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6505]) ).
cnf(f0,axiom,
meet(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f0_nnf,plain,
! [X] : meet(X,X) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : meet(X,X) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
meet(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
meet(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t14,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t288,plain,
meet(join(X1,meet(one,join(X1,X2))),join(X1,X2)) = join(X1,meet(one,join(X1,X2))),
inference(cp,[status(thm)],[t286,t14]) ).
cnf(t6572,plain,
meet(join(X1,X2),join(X1,meet(one,join(X1,X2)))) = join(X1,meet(one,join(X1,X2))),
inference(step,[status(thm)],[t288,t24]) ).
cnf(t6573,plain,
meet(join(X1,X2),join(X1,X2)) = join(X1,meet(one,join(X1,X2))),
inference(step,[status(thm)],[t6572,t286]) ).
cnf(t6574,plain,
join(X1,X2) = join(X1,meet(one,join(X1,X2))),
inference(step,[status(thm)],[t6573,t14]) ).
cnf(t484,plain,
join(X1,meet(one,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t6574]) ).
cnf(t486,plain,
join(X1,meet(X2,join(X1,meet(X3,join(X1,X2))))) = join(X1,meet(one,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t484,t47]) ).
cnf(t6652,plain,
join(X1,meet(X2,join(X1,meet(X3,join(X1,X2))))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t486,t484]) ).
cnf(t1022,plain,
join(X1,meet(X2,join(X1,meet(X3,join(X1,X2))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t6652]) ).
cnf(t1044,plain,
join(X1,meet(complement(X1),X2)) = join(X1,meet(complement(X1),join(X1,meet(X2,one)))),
inference(cp,[status(thm)],[t1022,t94]) ).
cnf(t6669,plain,
join(X1,meet(X2,complement(X1))) = join(X1,meet(complement(X1),join(X1,meet(X2,one)))),
inference(step,[status(thm)],[t1044,t24]) ).
cnf(t6670,plain,
join(X1,meet(X2,complement(X1))) = join(X1,meet(complement(X1),join(X1,X2))),
inference(step,[status(thm)],[t6669,t110]) ).
cnf(t1106,plain,
join(X1,meet(complement(X1),join(X1,X2))) = join(X1,meet(X2,complement(X1))),
inference(orient,[status(thm)],[t6670]) ).
cnf(t76,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t72,t17]) ).
cnf(t6468,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t76,t72]) ).
cnf(t6469,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t6468,t68]) ).
cnf(t6470,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t6469,t68]) ).
cnf(t187,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t6470]) ).
cnf(t1125,plain,
join(X1,meet(join(X2,meet(X1,X3)),complement(X1))) = join(X1,meet(complement(X1),join(X1,X2))),
inference(cp,[status(thm)],[t1106,t187]) ).
cnf(t6761,plain,
join(X1,meet(complement(X1),join(X2,meet(X1,X3)))) = join(X1,meet(complement(X1),join(X1,X2))),
inference(step,[status(thm)],[t1125,t24]) ).
cnf(t6762,plain,
join(X1,meet(complement(X1),join(X2,meet(X1,X3)))) = join(X1,meet(X2,complement(X1))),
inference(step,[status(thm)],[t6761,t1106]) ).
cnf(t1461,plain,
join(X1,meet(complement(X1),join(X2,meet(X1,X3)))) = join(X1,meet(X2,complement(X1))),
inference(orient,[status(thm)],[t6762]) ).
cnf(t97,plain,
join(X1,join(complement(X1),X2)) = join(X2,one),
inference(cp,[status(thm)],[t72,t94]) ).
cnf(t6463,plain,
join(X1,join(X2,complement(X1))) = join(X2,one),
inference(step,[status(thm)],[t97,t68]) ).
cnf(t6464,plain,
join(X1,join(X2,complement(X1))) = one,
inference(step,[status(thm)],[t6463,t141]) ).
cnf(t166,plain,
join(X1,join(X2,complement(X1))) = one,
inference(orient,[status(thm)],[t6464]) ).
cnf(t1039,plain,
join(X1,meet(join(X2,complement(X1)),X3)) = join(X1,meet(join(X2,complement(X1)),join(X1,meet(X3,one)))),
inference(cp,[status(thm)],[t1022,t166]) ).
cnf(t6891,plain,
join(X1,meet(X3,join(X2,complement(X1)))) = join(X1,meet(join(X2,complement(X1)),join(X1,meet(X3,one)))),
inference(step,[status(thm)],[t1039,t24]) ).
cnf(t6892,plain,
join(X1,meet(X3,join(X2,complement(X1)))) = join(X1,meet(join(X2,complement(X1)),join(X1,X3))),
inference(step,[status(thm)],[t6891,t110]) ).
cnf(t6893,plain,
join(X1,meet(X3,join(X2,complement(X1)))) = join(X1,meet(join(X1,X3),join(X2,complement(X1)))),
inference(step,[status(thm)],[t6892,t24]) ).
cnf(t3080,plain,
join(X1,meet(join(X1,X2),join(X3,complement(X1)))) = join(X1,meet(X2,join(X3,complement(X1)))),
inference(orient,[status(thm)],[t6893]) ).
cnf(t3116,plain,
join(X1,meet(join(X2,complement(X1)),join(X3,complement(X1)))) = join(X1,meet(one,join(X3,complement(X1)))),
inference(cp,[status(thm)],[t3080,t166]) ).
cnf(t300,plain,
meet(X1,join(X2,meet(X3,one))) = meet(X1,join(X2,meet(X3,join(X2,X3)))),
inference(cp,[status(thm)],[t47,t286]) ).
cnf(t6510,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X2,X3)))),
inference(step,[status(thm)],[t300,t110]) ).
cnf(t320,plain,
meet(X1,join(X2,meet(X3,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6510]) ).
cnf(t487,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,meet(one,join(X1,X2))),
inference(cp,[status(thm)],[t484,t320]) ).
cnf(t6575,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(step,[status(thm)],[t487,t484]) ).
cnf(t505,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t6575]) ).
cnf(t510,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,meet(join(X2,meet(X1,X3)),join(X1,X2))),
inference(cp,[status(thm)],[t505,t187]) ).
cnf(t6598,plain,
join(X1,X2) = join(X1,meet(join(X2,meet(X1,X3)),join(X1,X2))),
inference(step,[status(thm)],[t510,t187]) ).
cnf(t6599,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t6598,t24]) ).
cnf(t666,plain,
join(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = join(X1,X2),
inference(orient,[status(thm)],[t6599]) ).
cnf(t674,plain,
join(X1,join(X2,complement(X1))) = join(X1,meet(one,join(join(X2,complement(X1)),meet(X1,X3)))),
inference(cp,[status(thm)],[t666,t166]) ).
cnf(t6632,plain,
one = join(X1,meet(one,join(join(X2,complement(X1)),meet(X1,X3)))),
inference(step,[status(thm)],[t674,t166]) ).
cnf(t6633,plain,
one = join(X1,meet(one,join(meet(X1,X3),join(X2,complement(X1))))),
inference(step,[status(thm)],[t6632,t68]) ).
cnf(t6634,plain,
one = join(X1,meet(one,join(complement(X1),join(meet(X1,X3),X2)))),
inference(step,[status(thm)],[t6633,t72]) ).
cnf(t6635,plain,
one = join(X1,meet(one,join(X2,join(complement(X1),meet(X1,X3))))),
inference(step,[status(thm)],[t6634,t72]) ).
cnf(t901,plain,
join(X1,meet(one,join(X2,join(complement(X1),meet(X1,X3))))) = one,
inference(orient,[status(thm)],[t6635]) ).
cnf(f6,axiom,
meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f6_nnf,plain,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t11,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t6449,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)],[t6449]) ).
cnf(f9,axiom,
meet(X,complement(X)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f9_nnf,plain,
! [X] : meet(X,complement(X)) = zero,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] : meet(X,complement(X)) = zero,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
meet(X0,complement(X0)) = zero,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t4,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t58,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t61,plain,
meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
inference(cp,[status(thm)],[t27,t58]) ).
cnf(t6461,plain,
meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
inference(step,[status(thm)],[t61,t24]) ).
cnf(t30,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t27,t14]) ).
cnf(t6451,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t30,t27]) ).
cnf(t6452,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t6451,t24]) ).
cnf(t115,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t6452]) ).
cnf(t118,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t115,t58]) ).
cnf(t6453,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t118,t58]) ).
cnf(t125,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t6453]) ).
cnf(t6462,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t6461,t125]) ).
cnf(t159,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t6462]) ).
cnf(t164,plain,
meet(X1,meet(meet(X2,complement(X1)),X3)) = meet(X3,zero),
inference(cp,[status(thm)],[t27,t159]) ).
cnf(t6471,plain,
meet(X1,meet(X3,meet(X2,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t164,t24]) ).
cnf(t6472,plain,
meet(X1,meet(X2,meet(complement(X1),X3))) = meet(X3,zero),
inference(step,[status(thm)],[t6471,t27]) ).
cnf(t6473,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = meet(X3,zero),
inference(step,[status(thm)],[t6472,t24]) ).
cnf(t6474,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(step,[status(thm)],[t6473,t125]) ).
cnf(t201,plain,
meet(X1,meet(X2,meet(X3,complement(X1)))) = zero,
inference(orient,[status(thm)],[t6474]) ).
cnf(t908,plain,
one = join(X1,meet(one,join(X2,join(complement(X1),zero)))),
inference(cp,[status(thm)],[t901,t201]) ).
cnf(t59,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t17,t58]) ).
cnf(t99,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t59]) ).
cnf(t6636,plain,
one = join(X1,meet(one,join(X2,complement(X1)))),
inference(step,[status(thm)],[t908,t99]) ).
cnf(t932,plain,
join(X1,meet(one,join(X2,complement(X1)))) = one,
inference(orient,[status(thm)],[t6636]) ).
cnf(t6909,plain,
join(X1,meet(join(X2,complement(X1)),join(X3,complement(X1)))) = one,
inference(step,[status(thm)],[t3116,t932]) ).
cnf(t3487,plain,
join(X1,meet(join(X2,complement(X1)),join(X3,complement(X1)))) = one,
inference(orient,[status(thm)],[t6909]) ).
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(t6821,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(step,[status(thm)],[t26,t68]) ).
cnf(t2433,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t6821]) ).
cnf(t2444,plain,
X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t2433,t58]) ).
cnf(t5,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t18,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t6822,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t2444,t18]) ).
cnf(t6823,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t6822,t94]) ).
cnf(t6824,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t6823,t18]) ).
cnf(t2537,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t6824]) ).
cnf(t3489,plain,
one = join(complement(X1),meet(join(X2,X1),join(X3,complement(complement(X1))))),
inference(cp,[status(thm)],[t3487,t2537]) ).
cnf(t6910,plain,
one = join(complement(X1),meet(join(X1,X2),join(X3,complement(complement(X1))))),
inference(step,[status(thm)],[t3489,t68]) ).
cnf(t6911,plain,
one = join(complement(X1),meet(join(X1,X2),join(X3,X1))),
inference(step,[status(thm)],[t6910,t2537]) ).
cnf(t6912,plain,
one = join(complement(X1),meet(join(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t6911,t68]) ).
cnf(t3515,plain,
join(complement(X1),meet(join(X1,X2),join(X1,X3))) = one,
inference(orient,[status(thm)],[t6912]) ).
cnf(t3624,plain,
join(join(X1,X2),meet(complement(X1),complement(join(X1,X2)))) = join(join(X1,X2),meet(complement(join(X1,X2)),one)),
inference(cp,[status(thm)],[t1461,t3515]) ).
cnf(t6919,plain,
join(join(X1,X2),meet(complement(X1),complement(join(X1,X2)))) = join(join(X1,X2),complement(join(X1,X2))),
inference(step,[status(thm)],[t3624,t110]) ).
cnf(t6920,plain,
join(join(X1,X2),meet(complement(X1),complement(join(X1,X2)))) = one,
inference(step,[status(thm)],[t6919,t94]) ).
cnf(t3715,plain,
join(join(X1,X2),meet(complement(X1),complement(join(X1,X2)))) = one,
inference(orient,[status(thm)],[t6920]) ).
cnf(t3737,plain,
meet(complement(X1),complement(join(X1,X2))) = ifeq(meet(join(X1,X2),meet(complement(X1),complement(join(X1,X2)))),zero,ifeq(one,one,complement(join(X1,X2)),meet(complement(X1),complement(join(X1,X2)))),meet(complement(X1),complement(join(X1,X2)))),
inference(cp,[status(thm)],[t19,t3715]) ).
cnf(t6921,plain,
meet(complement(X1),complement(join(X1,X2))) = ifeq(zero,zero,ifeq(one,one,complement(join(X1,X2)),meet(complement(X1),complement(join(X1,X2)))),meet(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t3737,t159]) ).
cnf(t6922,plain,
meet(complement(X1),complement(join(X1,X2))) = ifeq(one,one,complement(join(X1,X2)),meet(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t6921,t18]) ).
cnf(t6923,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(step,[status(thm)],[t6922,t18]) ).
cnf(t3761,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t6923]) ).
cnf(t3769,plain,
complement(X1) = join(complement(X1),complement(join(X1,X2))),
inference(cp,[status(thm)],[t17,t3761]) ).
cnf(t3786,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t3769]) ).
cnf(t3787,plain,
complement(complement(X1)) = join(X1,complement(join(complement(X1),X2))),
inference(cp,[status(thm)],[t3786,t2537]) ).
cnf(t6924,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t3787,t2537]) ).
cnf(t6925,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(step,[status(thm)],[t6924,t68]) ).
cnf(t3832,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t6925]) ).
cnf(t34,plain,
meet(X1,X2) = ifeq(meet(X2,meet(X3,X1)),zero,ifeq(join(X3,meet(X1,X2)),one,complement(X3),meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t19,t27]) ).
cnf(t6943,plain,
meet(X1,X2) = ifeq(meet(X1,meet(X2,X3)),zero,ifeq(join(X3,meet(X1,X2)),one,complement(X3),meet(X1,X2)),meet(X1,X2)),
inference(step,[status(thm)],[t34,t27]) ).
cnf(t4110,plain,
ifeq(meet(X1,meet(X2,X3)),zero,ifeq(join(X3,meet(X1,X2)),one,complement(X3),meet(X1,X2)),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t6943]) ).
cnf(t503,plain,
join(X1,join(meet(one,join(X1,X2)),X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t72,t484]) ).
cnf(t6592,plain,
join(X1,join(X3,meet(one,join(X1,X2)))) = join(X3,join(X1,X2)),
inference(step,[status(thm)],[t503,t68]) ).
cnf(t6593,plain,
join(X1,join(X3,meet(one,join(X1,X2)))) = join(X2,join(X3,X1)),
inference(step,[status(thm)],[t6592,t72]) ).
cnf(t6594,plain,
join(X1,join(X3,meet(one,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t6593,t72]) ).
cnf(t588,plain,
join(X1,join(X2,meet(one,join(X1,X3)))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t6594]) ).
cnf(t172,plain,
join(X1,join(join(X2,complement(X1)),X3)) = join(X3,one),
inference(cp,[status(thm)],[t72,t166]) ).
cnf(t6475,plain,
join(X1,join(X3,join(X2,complement(X1)))) = join(X3,one),
inference(step,[status(thm)],[t172,t68]) ).
cnf(t6476,plain,
join(X1,join(X2,join(complement(X1),X3))) = join(X3,one),
inference(step,[status(thm)],[t6475,t72]) ).
cnf(t6477,plain,
join(X1,join(X2,join(X3,complement(X1)))) = join(X3,one),
inference(step,[status(thm)],[t6476,t68]) ).
cnf(t6478,plain,
join(X1,join(X2,join(X3,complement(X1)))) = one,
inference(step,[status(thm)],[t6477,t141]) ).
cnf(t211,plain,
join(X1,join(X2,join(X3,complement(X1)))) = one,
inference(orient,[status(thm)],[t6478]) ).
cnf(t1120,plain,
join(X1,meet(join(X2,join(X3,complement(X1))),complement(X1))) = join(X1,meet(complement(X1),one)),
inference(cp,[status(thm)],[t1106,t211]) ).
cnf(t6727,plain,
join(X1,meet(complement(X1),join(X2,join(X3,complement(X1))))) = join(X1,meet(complement(X1),one)),
inference(step,[status(thm)],[t1120,t24]) ).
cnf(t6728,plain,
join(X1,meet(complement(X1),join(X2,join(X3,complement(X1))))) = join(X1,complement(X1)),
inference(step,[status(thm)],[t6727,t110]) ).
cnf(t6729,plain,
join(X1,meet(complement(X1),join(X2,join(X3,complement(X1))))) = one,
inference(step,[status(thm)],[t6728,t94]) ).
cnf(t1311,plain,
join(X1,meet(complement(X1),join(X2,join(X3,complement(X1))))) = one,
inference(orient,[status(thm)],[t6729]) ).
cnf(t1124,plain,
join(X1,meet(join(X2,complement(X1)),complement(X1))) = join(X1,meet(complement(X1),one)),
inference(cp,[status(thm)],[t1106,t166]) ).
cnf(t6681,plain,
join(X1,meet(complement(X1),join(X2,complement(X1)))) = join(X1,meet(complement(X1),one)),
inference(step,[status(thm)],[t1124,t24]) ).
cnf(t6682,plain,
join(X1,meet(complement(X1),join(X2,complement(X1)))) = join(X1,complement(X1)),
inference(step,[status(thm)],[t6681,t110]) ).
cnf(t6683,plain,
join(X1,meet(complement(X1),join(X2,complement(X1)))) = one,
inference(step,[status(thm)],[t6682,t94]) ).
cnf(t1212,plain,
join(X1,meet(complement(X1),join(X2,complement(X1)))) = one,
inference(orient,[status(thm)],[t6683]) ).
cnf(t1469,plain,
join(complement(X1),meet(X1,complement(complement(X1)))) = join(complement(X1),meet(complement(complement(X1)),one)),
inference(cp,[status(thm)],[t1461,t1212]) ).
cnf(t6763,plain,
join(complement(X1),meet(X1,complement(complement(X1)))) = join(complement(X1),complement(complement(X1))),
inference(step,[status(thm)],[t1469,t110]) ).
cnf(t6764,plain,
join(complement(X1),meet(X1,complement(complement(X1)))) = one,
inference(step,[status(thm)],[t6763,t94]) ).
cnf(t1517,plain,
join(complement(X1),meet(X1,complement(complement(X1)))) = one,
inference(orient,[status(thm)],[t6764]) ).
cnf(t1518,plain,
meet(X1,complement(complement(X1))) = ifeq(meet(complement(X1),meet(X1,complement(complement(X1)))),zero,ifeq(one,one,complement(complement(X1)),meet(X1,complement(complement(X1)))),meet(X1,complement(complement(X1)))),
inference(cp,[status(thm)],[t19,t1517]) ).
cnf(t6765,plain,
meet(X1,complement(complement(X1))) = ifeq(zero,zero,ifeq(one,one,complement(complement(X1)),meet(X1,complement(complement(X1)))),meet(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t1518,t159]) ).
cnf(t6766,plain,
meet(X1,complement(complement(X1))) = ifeq(one,one,complement(complement(X1)),meet(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t6765,t18]) ).
cnf(t6767,plain,
meet(X1,complement(complement(X1))) = complement(complement(X1)),
inference(step,[status(thm)],[t6766,t18]) ).
cnf(t1526,plain,
meet(X1,complement(complement(X1))) = complement(complement(X1)),
inference(orient,[status(thm)],[t6767]) ).
cnf(t1527,plain,
X1 = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t17,t1526]) ).
cnf(t1541,plain,
join(X1,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t1527]) ).
cnf(t1557,plain,
one = join(complement(X1),meet(complement(complement(X1)),join(X2,X1))),
inference(cp,[status(thm)],[t1311,t1541]) ).
cnf(t6769,plain,
one = join(complement(X1),meet(join(X2,X1),complement(complement(X1)))),
inference(step,[status(thm)],[t1557,t24]) ).
cnf(t6770,plain,
one = join(complement(X1),meet(join(X1,X2),complement(complement(X1)))),
inference(step,[status(thm)],[t6769,t68]) ).
cnf(t1637,plain,
join(complement(X1),meet(join(X1,X2),complement(complement(X1)))) = one,
inference(orient,[status(thm)],[t6770]) ).
cnf(t1646,plain,
meet(join(X1,X2),complement(complement(X1))) = ifeq(meet(complement(X1),meet(join(X1,X2),complement(complement(X1)))),zero,ifeq(one,one,complement(complement(X1)),meet(join(X1,X2),complement(complement(X1)))),meet(join(X1,X2),complement(complement(X1)))),
inference(cp,[status(thm)],[t19,t1637]) ).
cnf(t6771,plain,
meet(join(X1,X2),complement(complement(X1))) = ifeq(zero,zero,ifeq(one,one,complement(complement(X1)),meet(join(X1,X2),complement(complement(X1)))),meet(join(X1,X2),complement(complement(X1)))),
inference(step,[status(thm)],[t1646,t159]) ).
cnf(t6772,plain,
meet(join(X1,X2),complement(complement(X1))) = ifeq(one,one,complement(complement(X1)),meet(join(X1,X2),complement(complement(X1)))),
inference(step,[status(thm)],[t6771,t18]) ).
cnf(t6773,plain,
meet(join(X1,X2),complement(complement(X1))) = complement(complement(X1)),
inference(step,[status(thm)],[t6772,t18]) ).
cnf(t1658,plain,
meet(join(X1,X2),complement(complement(X1))) = complement(complement(X1)),
inference(orient,[status(thm)],[t6773]) ).
cnf(t1666,plain,
join(X1,X2) = join(join(X1,X2),complement(complement(X1))),
inference(cp,[status(thm)],[t17,t1658]) ).
cnf(t1698,plain,
join(join(X1,X2),complement(complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t1666]) ).
cnf(t1714,plain,
one = join(complement(X1),meet(one,join(X1,X2))),
inference(cp,[status(thm)],[t932,t1698]) ).
cnf(t1757,plain,
join(complement(X1),meet(one,join(X1,X2))) = one,
inference(orient,[status(thm)],[t1714]) ).
cnf(t1764,plain,
one = join(complement(join(X1,X2)),meet(one,join(X1,X2))),
inference(cp,[status(thm)],[t1757,t1698]) ).
cnf(t1888,plain,
join(complement(join(X1,X2)),meet(one,join(X1,X2))) = one,
inference(orient,[status(thm)],[t1764]) ).
cnf(t1905,plain,
join(X1,join(X2,complement(join(X1,X2)))) = join(X1,one),
inference(cp,[status(thm)],[t588,t1888]) ).
cnf(t6777,plain,
join(X1,join(X2,complement(join(X1,X2)))) = one,
inference(step,[status(thm)],[t1905,t141]) ).
cnf(t1912,plain,
join(X1,join(X2,complement(join(X1,X2)))) = one,
inference(orient,[status(thm)],[t6777]) ).
cnf(t1936,plain,
join(X1,meet(join(X2,complement(join(X1,X2))),complement(X1))) = join(X1,meet(complement(X1),one)),
inference(cp,[status(thm)],[t1106,t1912]) ).
cnf(t6795,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = join(X1,meet(complement(X1),one)),
inference(step,[status(thm)],[t1936,t24]) ).
cnf(t6796,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = join(X1,complement(X1)),
inference(step,[status(thm)],[t6795,t110]) ).
cnf(t6797,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = one,
inference(step,[status(thm)],[t6796,t94]) ).
cnf(t2189,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = one,
inference(orient,[status(thm)],[t6797]) ).
cnf(t2565,plain,
one = join(complement(X1),meet(X1,join(X2,complement(join(complement(X1),X2))))),
inference(cp,[status(thm)],[t2189,t2537]) ).
cnf(t6883,plain,
one = join(complement(X1),meet(X1,join(X2,complement(join(X2,complement(X1)))))),
inference(step,[status(thm)],[t2565,t68]) ).
cnf(t2835,plain,
join(complement(X1),meet(X1,join(X2,complement(join(X2,complement(X1)))))) = one,
inference(orient,[status(thm)],[t6883]) ).
cnf(t4174,plain,
meet(X1,join(X2,complement(join(X2,complement(X1))))) = ifeq(meet(X1,meet(join(X2,complement(join(X2,complement(X1)))),complement(X1))),zero,ifeq(one,one,complement(complement(X1)),meet(X1,join(X2,complement(join(X2,complement(X1)))))),meet(X1,join(X2,complement(join(X2,complement(X1)))))),
inference(cp,[status(thm)],[t4110,t2835]) ).
cnf(t6982,plain,
meet(X1,join(X2,complement(join(X2,complement(X1))))) = ifeq(zero,zero,ifeq(one,one,complement(complement(X1)),meet(X1,join(X2,complement(join(X2,complement(X1)))))),meet(X1,join(X2,complement(join(X2,complement(X1)))))),
inference(step,[status(thm)],[t4174,t159]) ).
cnf(t6983,plain,
meet(X1,join(X2,complement(join(X2,complement(X1))))) = ifeq(one,one,complement(complement(X1)),meet(X1,join(X2,complement(join(X2,complement(X1)))))),
inference(step,[status(thm)],[t6982,t18]) ).
cnf(t6984,plain,
meet(X1,join(X2,complement(join(X2,complement(X1))))) = complement(complement(X1)),
inference(step,[status(thm)],[t6983,t18]) ).
cnf(t6985,plain,
meet(X1,join(X2,complement(join(X2,complement(X1))))) = X1,
inference(step,[status(thm)],[t6984,t2537]) ).
cnf(t4489,plain,
meet(X1,join(X2,complement(join(X2,complement(X1))))) = X1,
inference(orient,[status(thm)],[t6985]) ).
cnf(t4491,plain,
complement(X1) = meet(complement(X1),join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t4489,t2537]) ).
cnf(t7006,plain,
complement(X1) = meet(complement(X1),join(X2,complement(join(X1,X2)))),
inference(step,[status(thm)],[t4491,t68]) ).
cnf(t4666,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = complement(X1),
inference(orient,[status(thm)],[t7006]) ).
cnf(t4678,plain,
complement(X1) = meet(complement(X1),join(meet(complement(X1),join(X2,join(X3,complement(X1)))),complement(one))),
inference(cp,[status(thm)],[t4666,t1311]) ).
cnf(t127,plain,
zero = ifeq(zero,zero,ifeq(join(X1,zero),one,complement(X1),zero),zero),
inference(cp,[status(thm)],[t19,t125]) ).
cnf(t6457,plain,
zero = ifeq(join(X1,zero),one,complement(X1),zero),
inference(step,[status(thm)],[t127,t18]) ).
cnf(t6458,plain,
zero = ifeq(X1,one,complement(X1),zero),
inference(step,[status(thm)],[t6457,t99]) ).
cnf(t147,plain,
ifeq(X1,one,complement(X1),zero) = zero,
inference(orient,[status(thm)],[t6458]) ).
cnf(t148,plain,
zero = complement(one),
inference(cp,[status(thm)],[t147,t18]) ).
cnf(t149,plain,
complement(one) = zero,
inference(orient,[status(thm)],[t148]) ).
cnf(t7011,plain,
complement(X1) = meet(complement(X1),join(meet(complement(X1),join(X2,join(X3,complement(X1)))),zero)),
inference(step,[status(thm)],[t4678,t149]) ).
cnf(t7012,plain,
complement(X1) = meet(complement(X1),meet(complement(X1),join(X2,join(X3,complement(X1))))),
inference(step,[status(thm)],[t7011,t99]) ).
cnf(t7013,plain,
complement(X1) = meet(complement(X1),join(X2,join(X3,complement(X1)))),
inference(step,[status(thm)],[t7012,t115]) ).
cnf(t4735,plain,
meet(complement(X1),join(X2,join(X3,complement(X1)))) = complement(X1),
inference(orient,[status(thm)],[t7013]) ).
cnf(t4741,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),join(X3,complement(X1))),
inference(cp,[status(thm)],[t4735,t3786]) ).
cnf(t7025,plain,
complement(join(X1,X2)) = meet(join(X3,complement(X1)),complement(join(X1,X2))),
inference(step,[status(thm)],[t4741,t24]) ).
cnf(t4867,plain,
meet(join(X1,complement(X2)),complement(join(X2,X3))) = complement(join(X2,X3)),
inference(orient,[status(thm)],[t7025]) ).
cnf(t4899,plain,
join(X1,complement(X2)) = join(join(X1,complement(X2)),complement(join(X2,X3))),
inference(cp,[status(thm)],[t17,t4867]) ).
cnf(t4947,plain,
join(join(X1,complement(X2)),complement(join(X2,X3))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t4899]) ).
cnf(t4953,plain,
join(X1,complement(complement(X2))) = join(join(X1,X2),complement(join(complement(X2),X3))),
inference(cp,[status(thm)],[t4947,t2537]) ).
cnf(t7040,plain,
join(X1,X2) = join(join(X1,X2),complement(join(complement(X2),X3))),
inference(step,[status(thm)],[t4953,t2537]) ).
cnf(t7041,plain,
join(X1,X2) = join(join(X1,X2),complement(join(X3,complement(X2)))),
inference(step,[status(thm)],[t7040,t68]) ).
cnf(t5124,plain,
join(join(X1,X2),complement(join(X3,complement(X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t7041]) ).
cnf(f12,hypothesis,
meet(b,a) = a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity_hypothesis) ).
fof(f12_nnf,plain,
meet(b,a) = a,
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
meet(b,a) = a,
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(t2,plain,
meet(b,a) = a,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t63,plain,
meet(b,a) = a,
inference(orient,[status(thm)],[t2]) ).
cnf(t64,plain,
b = join(b,a),
inference(cp,[status(thm)],[t17,t63]) ).
cnf(t105,plain,
join(b,a) = b,
inference(orient,[status(thm)],[t64]) ).
cnf(t5160,plain,
join(b,a) = join(b,complement(join(X1,complement(a)))),
inference(cp,[status(thm)],[t5124,t105]) ).
cnf(t7042,plain,
b = join(b,complement(join(X1,complement(a)))),
inference(step,[status(thm)],[t5160,t105]) ).
cnf(t5216,plain,
join(b,complement(join(X1,complement(a)))) = b,
inference(orient,[status(thm)],[t7042]) ).
cnf(t5235,plain,
join(X1,complement(a)) = join(join(X1,complement(a)),complement(b)),
inference(cp,[status(thm)],[t3832,t5216]) ).
cnf(t7051,plain,
join(X1,complement(a)) = join(complement(b),join(X1,complement(a))),
inference(step,[status(thm)],[t5235,t68]) ).
cnf(t7052,plain,
join(X1,complement(a)) = join(X1,join(complement(a),complement(b))),
inference(step,[status(thm)],[t7051,t72]) ).
cnf(t7053,plain,
join(X1,complement(a)) = join(X1,join(complement(b),complement(a))),
inference(step,[status(thm)],[t7052,t68]) ).
cnf(t5320,plain,
join(X1,join(complement(b),complement(a))) = join(X1,complement(a)),
inference(orient,[status(thm)],[t7053]) ).
cnf(t5321,plain,
join(join(complement(b),complement(a)),complement(a)) = join(complement(b),complement(a)),
inference(cp,[status(thm)],[t5320,t16]) ).
cnf(t7100,plain,
join(complement(a),join(complement(b),complement(a))) = join(complement(b),complement(a)),
inference(step,[status(thm)],[t5321,t68]) ).
cnf(t7101,plain,
join(complement(a),complement(a)) = join(complement(b),complement(a)),
inference(step,[status(thm)],[t7100,t5320]) ).
cnf(t7102,plain,
complement(a) = join(complement(b),complement(a)),
inference(step,[status(thm)],[t7101,t16]) ).
cnf(t6415,plain,
join(complement(b),complement(a)) = complement(a),
inference(orient,[status(thm)],[t7102]) ).
cnf(f13,negated_conjecture,
join(complement(b),complement(a)) != complement(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f13_nnf,plain,
join(complement(b),complement(a)) != complement(a),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
join(complement(b),complement(a)) != complement(a),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
join(complement(b),complement(a)) != complement(a),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
join(complement(b),complement(a)) != complement(a),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(g0_0,plain,
complement(a) != complement(a),
inference(rw,[status(thm)],[goal_0,t6415]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT235-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Wed Sep 23 20:38:51 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 11.80/1.98 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.80/1.98 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------