%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT240-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 : n017.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:23 PM UTC 2026
% Result : Unsatisfiable 34.05s 14.89s
% Output : Proof 34.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 87
% Number of leaves : 15
% Syntax : Number of formulae : 258 ( 254 unt; 0 def)
% Number of atoms : 266 ( 265 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 : 7 ( 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 : 412 ( 62 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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,join(X,U)))) = meet(X,join(Y,meet(Z,join(X,meet(Z,join(Y,U)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H50) ).
fof(f11_nnf,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,meet(Z,join(X,meet(Z,join(Y,U)))))),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,meet(Z,join(X,meet(Z,join(Y,U)))))),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(X1,meet(X2,join(X0,meet(X2,join(X1,X3)))))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t13,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,X4)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t47,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,X4)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t13]) ).
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(t51,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X2))))),
inference(cp,[status(thm)],[t47,t16]) ).
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(t13187,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t51,t24]) ).
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(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(t57,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t58,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t17,t57]) ).
cnf(t99,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t58]) ).
cnf(t102,plain,
meet(X1,join(X2,meet(X3,join(X1,zero)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X2))))),
inference(cp,[status(thm)],[t47,t99]) ).
cnf(t12525,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X2))))),
inference(step,[status(thm)],[t102,t99]) ).
cnf(t12526,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,X2))))),
inference(step,[status(thm)],[t12525,t24]) ).
cnf(t12527,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t12526,t24]) ).
cnf(t334,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,X3))))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t12527]) ).
cnf(t13188,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t13187,t334]) ).
cnf(t11891,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t13188]) ).
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(t11961,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),meet(X2,one))),
inference(cp,[status(thm)],[t11891,t94]) ).
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(t13191,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t11961,t110]) ).
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(t67,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t13192,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(X2,complement(X1))),
inference(step,[status(thm)],[t13191,t67]) ).
cnf(t12040,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(X2,complement(X1))),
inference(orient,[status(thm)],[t13192]) ).
cnf(t335,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(cp,[status(thm)],[t334,t17]) ).
cnf(t361,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t335]) ).
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(t12442,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)],[t12442]) ).
cnf(t31,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t27,t15]) ).
cnf(t12458,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t31,t27]) ).
cnf(t12459,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t12458,t24]) ).
cnf(t12460,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t12459,t24]) ).
cnf(t174,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t12460]) ).
cnf(t363,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t361,t174]) ).
cnf(t12606,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(step,[status(thm)],[t363,t174]) ).
cnf(t12607,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t12606,t67]) ).
cnf(t801,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,X2),
inference(orient,[status(thm)],[t12607]) ).
cnf(t60,plain,
meet(X1,meet(complement(X1),X2)) = meet(X2,zero),
inference(cp,[status(thm)],[t27,t57]) ).
cnf(t12454,plain,
meet(X1,meet(X2,complement(X1))) = meet(X2,zero),
inference(step,[status(thm)],[t60,t24]) ).
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(t30,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t27,t14]) ).
cnf(t12444,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t30,t27]) ).
cnf(t12445,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t12444,t24]) ).
cnf(t115,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t12445]) ).
cnf(t118,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t115,t57]) ).
cnf(t12446,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t118,t57]) ).
cnf(t125,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t12446]) ).
cnf(t12455,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t12454,t125]) ).
cnf(t159,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t12455]) ).
cnf(t813,plain,
meet(X1,meet(X2,complement(X1))) = meet(X1,join(zero,meet(meet(X2,complement(X1)),join(X1,X3)))),
inference(cp,[status(thm)],[t801,t159]) ).
cnf(t12625,plain,
zero = meet(X1,join(zero,meet(meet(X2,complement(X1)),join(X1,X3)))),
inference(step,[status(thm)],[t813,t159]) ).
cnf(t12626,plain,
zero = meet(X1,join(zero,meet(join(X1,X3),meet(X2,complement(X1))))),
inference(step,[status(thm)],[t12625,t24]) ).
cnf(t12627,plain,
zero = meet(X1,join(zero,meet(complement(X1),meet(join(X1,X3),X2)))),
inference(step,[status(thm)],[t12626,t27]) ).
cnf(t12628,plain,
zero = meet(X1,join(zero,meet(X2,meet(complement(X1),join(X1,X3))))),
inference(step,[status(thm)],[t12627,t27]) ).
cnf(t1011,plain,
meet(X1,join(zero,meet(X2,meet(complement(X1),join(X1,X3))))) = zero,
inference(orient,[status(thm)],[t12628]) ).
cnf(t346,plain,
meet(X1,join(X2,meet(X1,one))) = meet(X1,join(X2,meet(one,join(X1,X2)))),
inference(cp,[status(thm)],[t334,t110]) ).
cnf(t12532,plain,
meet(X1,join(X2,X1)) = meet(X1,join(X2,meet(one,join(X1,X2)))),
inference(step,[status(thm)],[t346,t110]) ).
cnf(t12533,plain,
meet(X1,join(X1,X2)) = meet(X1,join(X2,meet(one,join(X1,X2)))),
inference(step,[status(thm)],[t12532,t67]) ).
cnf(t12534,plain,
X1 = meet(X1,join(X2,meet(one,join(X1,X2)))),
inference(step,[status(thm)],[t12533,t15]) ).
cnf(t403,plain,
meet(X1,join(X2,meet(one,join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t12534]) ).
cnf(t425,plain,
meet(X1,meet(join(X2,meet(one,join(X1,X2))),X3)) = meet(X3,X1),
inference(cp,[status(thm)],[t27,t403]) ).
cnf(t12617,plain,
meet(X1,meet(X3,join(X2,meet(one,join(X1,X2))))) = meet(X3,X1),
inference(step,[status(thm)],[t425,t24]) ).
cnf(t12618,plain,
meet(X1,meet(X3,join(X2,meet(one,join(X1,X2))))) = meet(X1,X3),
inference(step,[status(thm)],[t12617,t24]) ).
cnf(t940,plain,
meet(X1,meet(X2,join(X3,meet(one,join(X1,X3))))) = meet(X1,X2),
inference(orient,[status(thm)],[t12618]) ).
cnf(t1012,plain,
zero = meet(X1,join(zero,meet(X2,complement(X1)))),
inference(cp,[status(thm)],[t1011,t940]) ).
cnf(t1047,plain,
meet(X1,join(zero,meet(X2,complement(X1)))) = zero,
inference(orient,[status(thm)],[t1012]) ).
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(t12751,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1),
inference(step,[status(thm)],[t26,t67]) ).
cnf(t2359,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t12751]) ).
cnf(t2402,plain,
X1 = ifeq(zero,zero,ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t2359,t57]) ).
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(t12752,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t2402,t18]) ).
cnf(t12753,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t12752,t94]) ).
cnf(t12754,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t12753,t18]) ).
cnf(t2440,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t12754]) ).
cnf(t2458,plain,
zero = meet(complement(X1),join(zero,meet(X2,X1))),
inference(cp,[status(thm)],[t1047,t2440]) ).
cnf(t12755,plain,
zero = meet(complement(X1),join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t2458,t24]) ).
cnf(t2496,plain,
meet(complement(X1),join(zero,meet(X1,X2))) = zero,
inference(orient,[status(thm)],[t12755]) ).
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(t62,plain,
meet(b,a) = a,
inference(orient,[status(thm)],[t2]) ).
cnf(t2519,plain,
zero = meet(complement(b),join(zero,a)),
inference(cp,[status(thm)],[t2496,t62]) ).
cnf(t2572,plain,
meet(complement(b),join(zero,a)) = zero,
inference(orient,[status(thm)],[t2519]) ).
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(t12443,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t10,t67]) ).
cnf(t72,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t12443]) ).
cnf(t76,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t72,t17]) ).
cnf(t12461,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t76,t72]) ).
cnf(t12462,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t12461,t67]) ).
cnf(t12463,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t12462,t67]) ).
cnf(t187,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t12463]) ).
cnf(t412,plain,
X1 = meet(X1,join(join(X2,meet(X1,X3)),meet(one,join(X1,X2)))),
inference(cp,[status(thm)],[t403,t187]) ).
cnf(t12672,plain,
X1 = meet(X1,join(meet(one,join(X1,X2)),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t412,t67]) ).
cnf(t12673,plain,
X1 = meet(X1,join(meet(X1,X3),join(meet(one,join(X1,X2)),X2))),
inference(step,[status(thm)],[t12672,t72]) ).
cnf(t12674,plain,
X1 = meet(X1,join(X2,join(meet(X1,X3),meet(one,join(X1,X2))))),
inference(step,[status(thm)],[t12673,t72]) ).
cnf(t1322,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(one,join(X1,X2))))) = X1,
inference(orient,[status(thm)],[t12674]) ).
cnf(t377,plain,
meet(X1,meet(join(X2,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t27,t361]) ).
cnf(t12539,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t377,t24]) ).
cnf(t12540,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t12539,t27]) ).
cnf(t12541,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t12540,t27]) ).
cnf(t465,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t12541]) ).
cnf(t75,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t72,t16]) ).
cnf(t12447,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t75,t72]) ).
cnf(t12448,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t12447,t67]) ).
cnf(t130,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t12448]) ).
cnf(t133,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t130,t94]) ).
cnf(t12449,plain,
one = join(X1,one),
inference(step,[status(thm)],[t133,t94]) ).
cnf(t141,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t12449]) ).
cnf(t144,plain,
meet(X1,join(X2,meet(X3,join(X1,one)))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,one))))),
inference(cp,[status(thm)],[t47,t141]) ).
cnf(t12486,plain,
meet(X1,join(X2,meet(X3,one))) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,one))))),
inference(step,[status(thm)],[t144,t141]) ).
cnf(t12487,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X1,meet(X3,one))))),
inference(step,[status(thm)],[t12486,t110]) ).
cnf(t12488,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X1,X3)))),
inference(step,[status(thm)],[t12487,t110]) ).
cnf(t251,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t12488]) ).
cnf(t63,plain,
b = join(b,a),
inference(cp,[status(thm)],[t17,t62]) ).
cnf(t105,plain,
join(b,a) = b,
inference(orient,[status(thm)],[t63]) ).
cnf(t415,plain,
b = meet(b,join(a,meet(one,b))),
inference(cp,[status(thm)],[t403,t105]) ).
cnf(t427,plain,
meet(b,join(a,meet(one,b))) = b,
inference(orient,[status(thm)],[t415]) ).
cnf(t432,plain,
meet(a,join(one,meet(a,b))) = meet(a,join(one,b)),
inference(cp,[status(thm)],[t334,t427]) ).
cnf(t12535,plain,
meet(a,join(one,meet(b,a))) = meet(a,join(one,b)),
inference(step,[status(thm)],[t432,t24]) ).
cnf(t12536,plain,
meet(a,join(one,a)) = meet(a,join(one,b)),
inference(step,[status(thm)],[t12535,t62]) ).
cnf(t437,plain,
meet(a,join(one,a)) = meet(a,join(one,b)),
inference(orient,[status(thm)],[t12536]) ).
cnf(t440,plain,
meet(one,join(X1,a)) = meet(one,join(X1,meet(a,join(one,b)))),
inference(cp,[status(thm)],[t251,t437]) ).
cnf(t519,plain,
meet(one,join(X1,meet(a,join(one,b)))) = meet(one,join(X1,a)),
inference(orient,[status(thm)],[t440]) ).
cnf(t524,plain,
meet(a,meet(join(one,b),one)) = meet(a,meet(one,join(join(one,b),a))),
inference(cp,[status(thm)],[t465,t519]) ).
cnf(t12547,plain,
meet(a,join(one,b)) = meet(a,meet(one,join(join(one,b),a))),
inference(step,[status(thm)],[t524,t110]) ).
cnf(t12548,plain,
meet(a,join(one,b)) = meet(one,meet(join(join(one,b),a),a)),
inference(step,[status(thm)],[t12547,t27]) ).
cnf(t12549,plain,
meet(a,join(one,b)) = meet(one,meet(a,join(join(one,b),a))),
inference(step,[status(thm)],[t12548,t24]) ).
cnf(t12550,plain,
meet(a,join(one,b)) = meet(one,meet(a,join(a,join(one,b)))),
inference(step,[status(thm)],[t12549,t67]) ).
cnf(t12551,plain,
meet(a,join(one,b)) = meet(one,meet(a,join(b,join(a,one)))),
inference(step,[status(thm)],[t12550,t72]) ).
cnf(t12552,plain,
meet(a,join(one,b)) = meet(one,meet(a,join(one,join(b,a)))),
inference(step,[status(thm)],[t12551,t72]) ).
cnf(t12553,plain,
meet(a,join(one,b)) = meet(one,a),
inference(step,[status(thm)],[t12552,t174]) ).
cnf(t540,plain,
meet(a,join(one,b)) = meet(one,a),
inference(orient,[status(thm)],[t12553]) ).
cnf(t544,plain,
a = join(a,meet(one,a)),
inference(cp,[status(thm)],[t17,t540]) ).
cnf(t557,plain,
join(a,meet(one,a)) = a,
inference(orient,[status(thm)],[t544]) ).
cnf(t561,plain,
a = meet(a,join(meet(one,a),meet(one,a))),
inference(cp,[status(thm)],[t403,t557]) ).
cnf(t12557,plain,
a = meet(a,meet(one,a)),
inference(step,[status(thm)],[t561,t16]) ).
cnf(t12558,plain,
a = meet(one,meet(a,a)),
inference(step,[status(thm)],[t12557,t27]) ).
cnf(t12559,plain,
a = meet(one,a),
inference(step,[status(thm)],[t12558,t14]) ).
cnf(t567,plain,
meet(one,a) = a,
inference(orient,[status(thm)],[t12559]) ).
cnf(t572,plain,
one = join(one,a),
inference(cp,[status(thm)],[t17,t567]) ).
cnf(t582,plain,
join(one,a) = one,
inference(orient,[status(thm)],[t572]) ).
cnf(t585,plain,
meet(X1,join(one,meet(X2,join(X1,a)))) = meet(X1,join(one,meet(X2,join(X1,meet(X2,one))))),
inference(cp,[status(thm)],[t47,t582]) ).
cnf(t12572,plain,
meet(X1,join(one,meet(X2,join(X1,a)))) = meet(X1,join(one,meet(X2,join(X1,X2)))),
inference(step,[status(thm)],[t585,t110]) ).
cnf(t12573,plain,
meet(X1,join(one,meet(X2,join(X1,a)))) = meet(X1,join(one,X2)),
inference(step,[status(thm)],[t12572,t251]) ).
cnf(t12574,plain,
meet(X1,join(one,meet(X2,join(X1,a)))) = meet(X1,join(X2,one)),
inference(step,[status(thm)],[t12573,t67]) ).
cnf(t12575,plain,
meet(X1,join(one,meet(X2,join(X1,a)))) = meet(X1,one),
inference(step,[status(thm)],[t12574,t141]) ).
cnf(t12576,plain,
meet(X1,join(one,meet(X2,join(X1,a)))) = X1,
inference(step,[status(thm)],[t12575,t110]) ).
cnf(t608,plain,
meet(X1,join(one,meet(X2,join(X1,a)))) = X1,
inference(orient,[status(thm)],[t12576]) ).
cnf(t612,plain,
a = meet(a,join(one,meet(X1,a))),
inference(cp,[status(thm)],[t608,t16]) ).
cnf(t624,plain,
meet(a,join(one,meet(X1,a))) = a,
inference(orient,[status(thm)],[t612]) ).
cnf(t627,plain,
meet(a,join(one,meet(X1,a))) = meet(a,join(join(one,meet(X1,a)),a)),
inference(cp,[status(thm)],[t361,t624]) ).
cnf(t12577,plain,
a = meet(a,join(join(one,meet(X1,a)),a)),
inference(step,[status(thm)],[t627,t624]) ).
cnf(t12578,plain,
a = meet(a,join(a,join(one,meet(X1,a)))),
inference(step,[status(thm)],[t12577,t67]) ).
cnf(t12579,plain,
a = meet(a,join(one,join(meet(X1,a),a))),
inference(step,[status(thm)],[t12578,t72]) ).
cnf(t12580,plain,
a = meet(a,join(one,join(a,meet(X1,a)))),
inference(step,[status(thm)],[t12579,t67]) ).
cnf(t667,plain,
meet(a,join(one,join(a,meet(X1,a)))) = a,
inference(orient,[status(thm)],[t12580]) ).
cnf(t1359,plain,
a = meet(a,join(X1,join(a,meet(one,join(a,X1))))),
inference(cp,[status(thm)],[t1322,t667]) ).
cnf(t12682,plain,
a = meet(a,join(X1,join(a,meet(one,join(X1,a))))),
inference(step,[status(thm)],[t1359,t67]) ).
cnf(t1510,plain,
meet(a,join(X1,join(a,meet(one,join(X1,a))))) = a,
inference(orient,[status(thm)],[t12682]) ).
cnf(t2512,plain,
zero = meet(complement(a),join(zero,a)),
inference(cp,[status(thm)],[t2496,t1510]) ).
cnf(t2540,plain,
meet(complement(a),join(zero,a)) = zero,
inference(orient,[status(thm)],[t2512]) ).
cnf(t2541,plain,
join(zero,a) = ifeq(zero,zero,ifeq(join(complement(a),join(zero,a)),one,complement(complement(a)),join(zero,a)),join(zero,a)),
inference(cp,[status(thm)],[t19,t2540]) ).
cnf(t12783,plain,
join(zero,a) = ifeq(join(complement(a),join(zero,a)),one,complement(complement(a)),join(zero,a)),
inference(step,[status(thm)],[t2541,t18]) ).
cnf(t12784,plain,
join(zero,a) = ifeq(join(a,join(complement(a),zero)),one,complement(complement(a)),join(zero,a)),
inference(step,[status(thm)],[t12783,t72]) ).
cnf(t12785,plain,
join(zero,a) = ifeq(join(zero,join(a,complement(a))),one,complement(complement(a)),join(zero,a)),
inference(step,[status(thm)],[t12784,t72]) ).
cnf(t12786,plain,
join(zero,a) = ifeq(join(zero,one),one,complement(complement(a)),join(zero,a)),
inference(step,[status(thm)],[t12785,t94]) ).
cnf(t12787,plain,
join(zero,a) = ifeq(one,one,complement(complement(a)),join(zero,a)),
inference(step,[status(thm)],[t12786,t141]) ).
cnf(t12788,plain,
join(zero,a) = complement(complement(a)),
inference(step,[status(thm)],[t12787,t18]) ).
cnf(t12789,plain,
join(zero,a) = a,
inference(step,[status(thm)],[t12788,t2440]) ).
cnf(t3121,plain,
join(zero,a) = a,
inference(orient,[status(thm)],[t12789]) ).
cnf(t12790,plain,
meet(complement(b),a) = zero,
inference(step,[status(thm)],[t2572,t3121]) ).
cnf(t3140,plain,
meet(complement(b),a) = zero,
inference(rw,[status(thm)],[t12790]) ).
cnf(t12792,plain,
meet(a,complement(b)) = zero,
inference(step,[status(thm)],[t3140,t24]) ).
cnf(t3151,plain,
meet(a,complement(b)) = zero,
inference(orient,[status(thm)],[t12792]) ).
cnf(t12198,plain,
meet(a,join(complement(b),complement(a))) = meet(a,join(complement(a),zero)),
inference(cp,[status(thm)],[t12040,t3151]) ).
cnf(t13196,plain,
meet(a,join(complement(b),complement(a))) = meet(a,complement(a)),
inference(step,[status(thm)],[t12198,t99]) ).
cnf(t13197,plain,
meet(a,join(complement(b),complement(a))) = zero,
inference(step,[status(thm)],[t13196,t57]) ).
cnf(t12341,plain,
meet(a,join(complement(b),complement(a))) = zero,
inference(orient,[status(thm)],[t13197]) ).
cnf(t12342,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,t12341]) ).
cnf(t13198,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)],[t12342,t18]) ).
cnf(t97,plain,
join(X1,join(complement(X1),X2)) = join(X2,one),
inference(cp,[status(thm)],[t72,t94]) ).
cnf(t12456,plain,
join(X1,join(X2,complement(X1))) = join(X2,one),
inference(step,[status(thm)],[t97,t67]) ).
cnf(t12457,plain,
join(X1,join(X2,complement(X1))) = one,
inference(step,[status(thm)],[t12456,t141]) ).
cnf(t166,plain,
join(X1,join(X2,complement(X1))) = one,
inference(orient,[status(thm)],[t12457]) ).
cnf(t13199,plain,
join(complement(b),complement(a)) = ifeq(one,one,complement(a),join(complement(b),complement(a))),
inference(step,[status(thm)],[t13198,t166]) ).
cnf(t13200,plain,
join(complement(b),complement(a)) = complement(a),
inference(step,[status(thm)],[t13199,t18]) ).
cnf(t12390,plain,
join(complement(b),complement(a)) = complement(a),
inference(orient,[status(thm)],[t13200]) ).
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,t12390]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT240-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/10.42 % Computer : n017.cluster.edu
% 0.13/10.42 % Model : x86_64 x86_64
% 0.13/10.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.42 % Memory : 8046.5625MB
% 0.13/10.42 % OS : Linux 6.8.0-71-generic
% 0.13/10.42 % CPULimit : 300
% 0.13/10.42 % WCLimit : 300
% 0.13/10.42 % DateTime : Wed Sep 23 20:35:28 UTC 2026
% 0.13/10.42 % CPUTime :
% 0.13/10.42 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 34.05/14.89 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 34.05/14.89 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------