%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT212-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 : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:56:09 PM UTC 2026
% Result : Unsatisfiable 53.60s 12.38s
% Output : Proof 53.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 87
% Number of leaves : 14
% Syntax : Number of formulae : 355 ( 351 unt; 0 def)
% Number of atoms : 363 ( 362 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 24 ( 16 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-4 aty)
% Number of variables : 778 ( 101 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f5,axiom,
join(X,Y) = join(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f5_nnf,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] : join(X,Y) = join(Y,X),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t53,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(f4,axiom,
meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f4_nnf,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] : meet(X,Y) = meet(Y,X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t7,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t23,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(f10,axiom,
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f10_nnf,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y] :
( complement(X) = Y
| join(X,Y) != one
| meet(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( complement(X0) = X1
| join(X0,X1) != one
| meet(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t11,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t18,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X1,X2),one,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t25,plain,
X1 = ifeq(meet(X1,X2),zero,ifeq(join(X2,X1),one,complement(X2),X1),X1),
inference(cp,[status(thm)],[t18,t23]) ).
cnf(t10294,plain,
ifeq(meet(X1,X2),zero,ifeq(join(X2,X1),one,complement(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t25]) ).
cnf(f9,axiom,
meet(X,complement(X)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f9_nnf,plain,
! [X] : meet(X,complement(X)) = zero,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] : meet(X,complement(X)) = zero,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
meet(X0,complement(X0)) = zero,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t3,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t48,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t10346,plain,
X1 = ifeq(zero,zero,ifeq(join(complement(X1),X1),one,complement(complement(X1)),X1),X1),
inference(cp,[status(thm)],[t10294,t48]) ).
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(t114585,plain,
X1 = ifeq(join(complement(X1),X1),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t10346,t17]) ).
cnf(t114586,plain,
X1 = ifeq(join(X1,complement(X1)),one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t114585,t53]) ).
cnf(f8,axiom,
join(X,complement(X)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f8_nnf,plain,
! [X] : join(X,complement(X)) = one,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] : join(X,complement(X)) = one,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
join(X0,complement(X0)) = one,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t2,plain,
join(X1,complement(X1)) = one,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t70,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t114587,plain,
X1 = ifeq(one,one,complement(complement(X1)),X1),
inference(step,[status(thm)],[t114586,t70]) ).
cnf(t114588,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t114587,t17]) ).
cnf(t18812,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t114588]) ).
cnf(f6,axiom,
meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f6_nnf,plain,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t10,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t26,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(f2,axiom,
meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f2_nnf,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : meet(X,join(X,Y)) = X,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t8,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t14,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t54,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t14,t53]) ).
cnf(t126,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t54]) ).
cnf(f3,axiom,
join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f3_nnf,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] : join(X,meet(X,Y)) = X,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t6,plain,
join(X1,meet(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t16,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t128,plain,
meet(X1,X2) = meet(meet(X1,X2),X1),
inference(cp,[status(thm)],[t126,t16]) ).
cnf(t114421,plain,
meet(X1,X2) = meet(X1,meet(X2,X1)),
inference(step,[status(thm)],[t128,t26]) ).
cnf(t153,plain,
meet(X1,meet(X2,X1)) = meet(X1,X2),
inference(orient,[status(thm)],[t114421]) ).
cnf(t159,plain,
meet(X1,meet(meet(X2,X1),X3)) = meet(meet(X1,X2),X3),
inference(cp,[status(thm)],[t26,t153]) ).
cnf(t114471,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t159,t26]) ).
cnf(t114472,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t114471,t26]) ).
cnf(t1317,plain,
meet(X1,meet(X2,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t114472]) ).
cnf(t28,plain,
meet(X1,meet(X2,join(meet(X1,X2),X3))) = meet(X1,X2),
inference(cp,[status(thm)],[t26,t14]) ).
cnf(t2213,plain,
meet(X1,meet(X2,join(meet(X1,X2),X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t28]) ).
cnf(t32,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t26,t23]) ).
cnf(t114474,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t32,t26]) ).
cnf(t1682,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t114474]) ).
cnf(t2215,plain,
meet(X1,X2) = meet(X2,meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t2213,t1682]) ).
cnf(t4103,plain,
meet(X1,meet(X2,join(meet(X2,X1),X3))) = meet(X2,X1),
inference(orient,[status(thm)],[t2215]) ).
cnf(f7,axiom,
join(join(X,Y),Z) = join(X,join(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f7_nnf,plain,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t9,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t58,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t63,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t58,t16]) ).
cnf(t326,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t63]) ).
cnf(t338,plain,
join(meet(X1,X2),X3) = meet(join(meet(X1,X2),X3),join(X1,X3)),
inference(cp,[status(thm)],[t126,t326]) ).
cnf(t114590,plain,
join(meet(X1,X2),X3) = meet(join(X1,X3),join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t338,t23]) ).
cnf(t19111,plain,
meet(join(X1,X2),join(meet(X1,X3),X2)) = join(meet(X1,X3),X2),
inference(orient,[status(thm)],[t114590]) ).
cnf(t19129,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t19111,t16]) ).
cnf(t41977,plain,
meet(X1,join(meet(X1,X2),meet(X1,X3))) = join(meet(X1,X2),meet(X1,X3)),
inference(orient,[status(thm)],[t19129]) ).
cnf(t42180,plain,
meet(X1,X2) = meet(X2,join(meet(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t4103,t41977]) ).
cnf(t42231,plain,
meet(X1,join(meet(X2,X1),meet(X2,X3))) = meet(X2,X1),
inference(orient,[status(thm)],[t42180]) ).
cnf(t42380,plain,
meet(X1,X2) = meet(X2,join(meet(X2,X1),meet(X1,X3))),
inference(cp,[status(thm)],[t42231,t23]) ).
cnf(t43484,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X2,X1),
inference(orient,[status(thm)],[t42380]) ).
cnf(t24,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t16,t23]) ).
cnf(t117,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t24]) ).
cnf(t121,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t117,t26]) ).
cnf(t261,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t121]) ).
cnf(t119,plain,
join(X1,X2) = join(join(X1,X2),X1),
inference(cp,[status(thm)],[t117,t14]) ).
cnf(t114420,plain,
join(X1,X2) = join(X1,join(X2,X1)),
inference(step,[status(thm)],[t119,t58]) ).
cnf(t145,plain,
join(X1,join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t114420]) ).
cnf(t149,plain,
join(X1,X2) = meet(join(X1,X2),join(X2,X1)),
inference(cp,[status(thm)],[t126,t145]) ).
cnf(t398,plain,
meet(join(X1,X2),join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t149]) ).
cnf(t422,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X2,X1))),
inference(cp,[status(thm)],[t261,t398]) ).
cnf(t114480,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X2,X1)))),
inference(step,[status(thm)],[t422,t58]) ).
cnf(t3093,plain,
join(X1,join(X2,meet(X3,join(X2,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t114480]) ).
cnf(t31,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t26,t14]) ).
cnf(t308,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t31]) ).
cnf(t321,plain,
meet(join(X1,X2),X3) = join(meet(join(X1,X2),X3),meet(X1,X3)),
inference(cp,[status(thm)],[t117,t308]) ).
cnf(t114589,plain,
meet(join(X1,X2),X3) = join(meet(X1,X3),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t321,t53]) ).
cnf(t18836,plain,
join(meet(X1,X2),meet(join(X1,X3),X2)) = meet(join(X1,X3),X2),
inference(orient,[status(thm)],[t114589]) ).
cnf(t18858,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(join(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t18836,t14]) ).
cnf(t34786,plain,
join(X1,meet(join(X1,X2),join(X1,X3))) = meet(join(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t18858]) ).
cnf(t34968,plain,
join(X1,X2) = join(X1,meet(join(X2,X3),join(X2,X1))),
inference(cp,[status(thm)],[t3093,t34786]) ).
cnf(t35407,plain,
join(X1,meet(join(X2,X3),join(X2,X1))) = join(X1,X2),
inference(orient,[status(thm)],[t34968]) ).
cnf(t60,plain,
join(X1,join(X2,meet(join(X1,X2),X3))) = join(X1,X2),
inference(cp,[status(thm)],[t58,t16]) ).
cnf(t2331,plain,
join(X1,join(X2,meet(join(X1,X2),X3))) = join(X1,X2),
inference(orient,[status(thm)],[t60]) ).
cnf(t64,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t58,t53]) ).
cnf(t114475,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t64,t58]) ).
cnf(t1939,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t114475]) ).
cnf(t2333,plain,
join(X1,X2) = join(X2,join(X1,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t2331,t1939]) ).
cnf(t4254,plain,
join(X1,join(X2,meet(join(X2,X1),X3))) = join(X2,X1),
inference(orient,[status(thm)],[t2333]) ).
cnf(t34963,plain,
join(X1,X2) = join(X2,meet(join(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t4254,t34786]) ).
cnf(t35014,plain,
join(X1,meet(join(X2,X1),join(X2,X3))) = join(X2,X1),
inference(orient,[status(thm)],[t34963]) ).
cnf(t35420,plain,
join(X1,X2) = join(X1,meet(join(X3,X2),join(X2,X1))),
inference(cp,[status(thm)],[t35407,t35014]) ).
cnf(t36579,plain,
join(X1,meet(join(X2,X3),join(X3,X1))) = join(X1,X3),
inference(orient,[status(thm)],[t35420]) ).
cnf(t36762,plain,
join(X1,X2) = join(X1,meet(join(X3,X2),join(X1,X2))),
inference(cp,[status(thm)],[t36579,t53]) ).
cnf(t37665,plain,
join(X1,meet(join(X2,X3),join(X1,X3))) = join(X1,X3),
inference(orient,[status(thm)],[t36762]) ).
cnf(t43513,plain,
meet(join(X1,X2),X3) = meet(X3,join(meet(X3,join(X1,X2)),X2)),
inference(cp,[status(thm)],[t43484,t37665]) ).
cnf(t114641,plain,
meet(join(X1,X2),X3) = meet(X3,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t43513,t53]) ).
cnf(t46844,plain,
meet(X1,join(X2,meet(X1,join(X3,X2)))) = meet(join(X3,X2),X1),
inference(orient,[status(thm)],[t114641]) ).
cnf(t35141,plain,
join(X1,X2) = join(X2,meet(join(X2,X1),join(X1,X3))),
inference(cp,[status(thm)],[t35014,t53]) ).
cnf(t35717,plain,
join(X1,meet(join(X1,X2),join(X2,X3))) = join(X2,X1),
inference(orient,[status(thm)],[t35141]) ).
cnf(t35872,plain,
join(X1,X2) = join(X2,meet(join(X2,X1),join(X3,X1))),
inference(cp,[status(thm)],[t35717,t35014]) ).
cnf(t37189,plain,
join(X1,meet(join(X1,X2),join(X3,X2))) = join(X2,X1),
inference(orient,[status(thm)],[t35872]) ).
cnf(t37427,plain,
join(meet(X1,X2),X3) = join(X3,meet(join(X3,meet(X1,X2)),X1)),
inference(cp,[status(thm)],[t37189,t16]) ).
cnf(t114636,plain,
join(meet(X1,X2),X3) = join(X3,meet(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t37427,t23]) ).
cnf(t38650,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(meet(X2,X3),X1),
inference(orient,[status(thm)],[t114636]) ).
cnf(f11,axiom,
meet(X,join(Y,meet(Z,join(Y,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Y,join(X,Z)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H70) ).
fof(f11_nnf,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(Y,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Y,join(X,Z)))))),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,join(Y,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Y,join(X,Z)))))),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
meet(X0,join(X1,meet(X2,join(X1,X3)))) = meet(X0,join(X1,meet(X2,join(X3,meet(X1,join(X0,X2)))))),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t12,plain,
meet(X1,join(X2,meet(X3,join(X4,meet(X2,join(X1,X3)))))) = meet(X1,join(X2,meet(X3,join(X2,X4)))),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t35,plain,
meet(X1,join(X2,meet(X3,join(X4,meet(X2,join(X1,X3)))))) = meet(X1,join(X2,meet(X3,join(X2,X4)))),
inference(orient,[status(thm)],[t12]) ).
cnf(t38656,plain,
join(meet(X1,join(X2,meet(X3,join(X1,X1)))),X3) = join(X3,meet(X1,join(X3,meet(X1,join(X3,X2))))),
inference(cp,[status(thm)],[t38650,t35]) ).
cnf(t114643,plain,
join(X3,meet(X1,join(X2,meet(X3,join(X1,X1))))) = join(X3,meet(X1,join(X3,meet(X1,join(X3,X2))))),
inference(step,[status(thm)],[t38656,t53]) ).
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(t15,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t114644,plain,
join(X3,meet(X1,join(X2,meet(X3,X1)))) = join(X3,meet(X1,join(X3,meet(X1,join(X3,X2))))),
inference(step,[status(thm)],[t114643,t15]) ).
cnf(t114645,plain,
join(X3,meet(X1,join(X2,meet(X3,X1)))) = join(meet(X1,join(X3,X2)),X3),
inference(step,[status(thm)],[t114644,t38650]) ).
cnf(t114646,plain,
join(X3,meet(X1,join(X2,meet(X3,X1)))) = join(X3,meet(X1,join(X3,X2))),
inference(step,[status(thm)],[t114645,t53]) ).
cnf(t52844,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t114646]) ).
cnf(t52969,plain,
join(X1,meet(complement(X1),join(X1,X2))) = join(X1,meet(complement(X1),join(X2,zero))),
inference(cp,[status(thm)],[t52844,t48]) ).
cnf(t51,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t16,t48]) ).
cnf(t75,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t51]) ).
cnf(t114647,plain,
join(X1,meet(complement(X1),join(X1,X2))) = join(X1,meet(complement(X1),X2)),
inference(step,[status(thm)],[t52969,t75]) ).
cnf(t53227,plain,
join(X1,meet(complement(X1),join(X1,X2))) = join(X1,meet(complement(X1),X2)),
inference(orient,[status(thm)],[t114647]) ).
cnf(t73,plain,
join(X1,join(complement(X1),X2)) = join(one,X2),
inference(cp,[status(thm)],[t58,t70]) ).
cnf(t72,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t14,t70]) ).
cnf(t80,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t72]) ).
cnf(t81,plain,
X1 = meet(one,X1),
inference(cp,[status(thm)],[t80,t23]) ).
cnf(t94,plain,
meet(one,X1) = X1,
inference(orient,[status(thm)],[t81]) ).
cnf(t96,plain,
join(one,X1) = one,
inference(cp,[status(thm)],[t94,t14]) ).
cnf(t107,plain,
join(one,X1) = one,
inference(orient,[status(thm)],[t96]) ).
cnf(t114433,plain,
join(X1,join(complement(X1),X2)) = one,
inference(step,[status(thm)],[t73,t107]) ).
cnf(t209,plain,
join(X1,join(complement(X1),X2)) = one,
inference(orient,[status(thm)],[t114433]) ).
cnf(t212,plain,
join(join(complement(X1),X2),X1) = join(join(complement(X1),X2),one),
inference(cp,[status(thm)],[t145,t209]) ).
cnf(t114434,plain,
join(complement(X1),join(X2,X1)) = join(join(complement(X1),X2),one),
inference(step,[status(thm)],[t212,t58]) ).
cnf(t114435,plain,
join(complement(X1),join(X2,X1)) = join(complement(X1),join(X2,one)),
inference(step,[status(thm)],[t114434,t58]) ).
cnf(t108,plain,
one = join(X1,one),
inference(cp,[status(thm)],[t107,t53]) ).
cnf(t114,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t108]) ).
cnf(t114436,plain,
join(complement(X1),join(X2,X1)) = join(complement(X1),one),
inference(step,[status(thm)],[t114435,t114]) ).
cnf(t114437,plain,
join(complement(X1),join(X2,X1)) = one,
inference(step,[status(thm)],[t114436,t114]) ).
cnf(t222,plain,
join(complement(X1),join(X2,X1)) = one,
inference(orient,[status(thm)],[t114437]) ).
cnf(t227,plain,
one = join(complement(meet(X1,X2)),X1),
inference(cp,[status(thm)],[t222,t16]) ).
cnf(t114438,plain,
one = join(X1,complement(meet(X1,X2))),
inference(step,[status(thm)],[t227,t53]) ).
cnf(t235,plain,
join(X1,complement(meet(X1,X2))) = one,
inference(orient,[status(thm)],[t114438]) ).
cnf(t53318,plain,
join(X1,meet(complement(X1),complement(meet(X1,X2)))) = join(X1,meet(complement(X1),one)),
inference(cp,[status(thm)],[t53227,t235]) ).
cnf(t114648,plain,
join(X1,meet(complement(X1),complement(meet(X1,X2)))) = join(X1,complement(X1)),
inference(step,[status(thm)],[t53318,t80]) ).
cnf(t114649,plain,
join(X1,meet(complement(X1),complement(meet(X1,X2)))) = one,
inference(step,[status(thm)],[t114648,t70]) ).
cnf(t53536,plain,
join(X1,meet(complement(X1),complement(meet(X1,X2)))) = one,
inference(orient,[status(thm)],[t114649]) ).
cnf(t53597,plain,
meet(complement(X1),complement(meet(X1,X2))) = ifeq(meet(X1,meet(complement(X1),complement(meet(X1,X2)))),zero,ifeq(one,one,complement(X1),meet(complement(X1),complement(meet(X1,X2)))),meet(complement(X1),complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t18,t53536]) ).
cnf(t50,plain,
meet(X1,meet(complement(X1),X2)) = meet(zero,X2),
inference(cp,[status(thm)],[t26,t48]) ).
cnf(t76,plain,
X1 = join(zero,X1),
inference(cp,[status(thm)],[t75,t53]) ).
cnf(t84,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t76]) ).
cnf(t86,plain,
meet(zero,X1) = zero,
inference(cp,[status(thm)],[t84,t16]) ).
cnf(t104,plain,
meet(zero,X1) = zero,
inference(orient,[status(thm)],[t86]) ).
cnf(t114426,plain,
meet(X1,meet(complement(X1),X2)) = zero,
inference(step,[status(thm)],[t50,t104]) ).
cnf(t163,plain,
meet(X1,meet(complement(X1),X2)) = zero,
inference(orient,[status(thm)],[t114426]) ).
cnf(t114650,plain,
meet(complement(X1),complement(meet(X1,X2))) = ifeq(zero,zero,ifeq(one,one,complement(X1),meet(complement(X1),complement(meet(X1,X2)))),meet(complement(X1),complement(meet(X1,X2)))),
inference(step,[status(thm)],[t53597,t163]) ).
cnf(t114651,plain,
meet(complement(X1),complement(meet(X1,X2))) = ifeq(one,one,complement(X1),meet(complement(X1),complement(meet(X1,X2)))),
inference(step,[status(thm)],[t114650,t17]) ).
cnf(t114652,plain,
meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
inference(step,[status(thm)],[t114651,t17]) ).
cnf(t53731,plain,
meet(complement(X1),complement(meet(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t114652]) ).
cnf(t37428,plain,
join(meet(X1,X2),X3) = join(X3,meet(join(X3,meet(X1,X2)),X2)),
inference(cp,[status(thm)],[t37189,t117]) ).
cnf(t114637,plain,
join(meet(X1,X2),X3) = join(X3,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t37428,t23]) ).
cnf(t38918,plain,
join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(meet(X3,X2),X1),
inference(orient,[status(thm)],[t114637]) ).
cnf(t42248,plain,
meet(X1,X2) = meet(X2,join(meet(X3,X1),meet(X1,X2))),
inference(cp,[status(thm)],[t42231,t38918]) ).
cnf(t43009,plain,
meet(X1,join(meet(X2,X3),meet(X3,X1))) = meet(X3,X1),
inference(orient,[status(thm)],[t42248]) ).
cnf(t43662,plain,
meet(X1,X2) = meet(X2,join(meet(X2,X1),meet(X3,X1))),
inference(cp,[status(thm)],[t43484,t43009]) ).
cnf(t45247,plain,
meet(X1,join(meet(X1,X2),meet(X3,X2))) = meet(X2,X1),
inference(orient,[status(thm)],[t43662]) ).
cnf(t53738,plain,
complement(X1) = meet(complement(X1),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t53731,t45247]) ).
cnf(t54287,plain,
meet(complement(X1),complement(meet(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t53738]) ).
cnf(t54358,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(X2)),
inference(cp,[status(thm)],[t117,t54287]) ).
cnf(t114658,plain,
complement(meet(X1,X2)) = join(complement(X2),complement(meet(X1,X2))),
inference(step,[status(thm)],[t54358,t53]) ).
cnf(t55842,plain,
join(complement(X1),complement(meet(X2,X1))) = complement(meet(X2,X1)),
inference(orient,[status(thm)],[t114658]) ).
cnf(t71,plain,
one = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t70,t58]) ).
cnf(t561,plain,
join(X1,join(X2,complement(join(X1,X2)))) = one,
inference(orient,[status(thm)],[t71]) ).
cnf(t53312,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = join(X1,meet(complement(X1),one)),
inference(cp,[status(thm)],[t53227,t561]) ).
cnf(t114736,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = join(X1,complement(X1)),
inference(step,[status(thm)],[t53312,t80]) ).
cnf(t114737,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = one,
inference(step,[status(thm)],[t114736,t70]) ).
cnf(t95444,plain,
join(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))) = one,
inference(orient,[status(thm)],[t114737]) ).
cnf(t95613,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = ifeq(meet(X1,meet(complement(X1),join(X2,complement(join(X1,X2))))),zero,ifeq(one,one,complement(X1),meet(complement(X1),join(X2,complement(join(X1,X2))))),meet(complement(X1),join(X2,complement(join(X1,X2))))),
inference(cp,[status(thm)],[t18,t95444]) ).
cnf(t114738,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = ifeq(zero,zero,ifeq(one,one,complement(X1),meet(complement(X1),join(X2,complement(join(X1,X2))))),meet(complement(X1),join(X2,complement(join(X1,X2))))),
inference(step,[status(thm)],[t95613,t163]) ).
cnf(t114739,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = ifeq(one,one,complement(X1),meet(complement(X1),join(X2,complement(join(X1,X2))))),
inference(step,[status(thm)],[t114738,t17]) ).
cnf(t114740,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = complement(X1),
inference(step,[status(thm)],[t114739,t17]) ).
cnf(t95760,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = complement(X1),
inference(orient,[status(thm)],[t114740]) ).
cnf(t95889,plain,
complement(meet(complement(X1),join(X2,complement(join(X1,X2))))) = join(complement(join(X2,complement(join(X1,X2)))),complement(complement(X1))),
inference(cp,[status(thm)],[t55842,t95760]) ).
cnf(t114742,plain,
complement(complement(X1)) = join(complement(join(X2,complement(join(X1,X2)))),complement(complement(X1))),
inference(step,[status(thm)],[t95889,t95760]) ).
cnf(t114743,plain,
X1 = join(complement(join(X2,complement(join(X1,X2)))),complement(complement(X1))),
inference(step,[status(thm)],[t114742,t18812]) ).
cnf(t114744,plain,
X1 = join(complement(complement(X1)),complement(join(X2,complement(join(X1,X2))))),
inference(step,[status(thm)],[t114743,t53]) ).
cnf(t114745,plain,
X1 = join(X1,complement(join(X2,complement(join(X1,X2))))),
inference(step,[status(thm)],[t114744,t18812]) ).
cnf(t96428,plain,
join(X1,complement(join(X2,complement(join(X1,X2))))) = X1,
inference(orient,[status(thm)],[t114745]) ).
cnf(t228,plain,
one = join(complement(meet(X1,X2)),X2),
inference(cp,[status(thm)],[t222,t117]) ).
cnf(t114439,plain,
one = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t228,t53]) ).
cnf(t243,plain,
join(X1,complement(meet(X2,X1))) = one,
inference(orient,[status(thm)],[t114439]) ).
cnf(t247,plain,
one = join(X1,complement(meet(X2,meet(X3,X1)))),
inference(cp,[status(thm)],[t243,t26]) ).
cnf(t829,plain,
join(X1,complement(meet(X2,meet(X3,X1)))) = one,
inference(orient,[status(thm)],[t247]) ).
cnf(t842,plain,
one = join(join(X1,X2),complement(meet(X3,join(X2,X1)))),
inference(cp,[status(thm)],[t829,t398]) ).
cnf(t114544,plain,
one = join(X1,join(X2,complement(meet(X3,join(X2,X1))))),
inference(step,[status(thm)],[t842,t58]) ).
cnf(t9833,plain,
join(X1,join(X2,complement(meet(X3,join(X2,X1))))) = one,
inference(orient,[status(thm)],[t114544]) ).
cnf(t53767,plain,
complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t117,t53731]) ).
cnf(t114654,plain,
complement(meet(X1,X2)) = join(complement(X1),complement(meet(X1,X2))),
inference(step,[status(thm)],[t53767,t53]) ).
cnf(t54506,plain,
join(complement(X1),complement(meet(X1,X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t114654]) ).
cnf(t54673,plain,
one = join(X1,complement(meet(X2,join(complement(X2),X1)))),
inference(cp,[status(thm)],[t9833,t54506]) ).
cnf(t58996,plain,
join(X1,complement(meet(X2,join(complement(X2),X1)))) = one,
inference(orient,[status(thm)],[t54673]) ).
cnf(t96437,plain,
X1 = join(X1,complement(join(complement(meet(X2,join(complement(X2),X1))),complement(one)))),
inference(cp,[status(thm)],[t96428,t58996]) ).
cnf(t114746,plain,
X1 = join(X1,complement(join(complement(one),complement(meet(X2,join(complement(X2),X1)))))),
inference(step,[status(thm)],[t96437,t53]) ).
cnf(t95,plain,
complement(one) = zero,
inference(cp,[status(thm)],[t94,t48]) ).
cnf(t102,plain,
complement(one) = zero,
inference(orient,[status(thm)],[t95]) ).
cnf(t114747,plain,
X1 = join(X1,complement(join(zero,complement(meet(X2,join(complement(X2),X1)))))),
inference(step,[status(thm)],[t114746,t102]) ).
cnf(t114748,plain,
X1 = join(X1,complement(complement(meet(X2,join(complement(X2),X1))))),
inference(step,[status(thm)],[t114747,t84]) ).
cnf(t114749,plain,
X1 = join(X1,meet(X2,join(complement(X2),X1))),
inference(step,[status(thm)],[t114748,t18812]) ).
cnf(t96802,plain,
join(X1,meet(X2,join(complement(X2),X1))) = X1,
inference(orient,[status(thm)],[t114749]) ).
cnf(t97091,plain,
meet(join(complement(X1),X2),X1) = meet(X1,X2),
inference(cp,[status(thm)],[t46844,t96802]) ).
cnf(t114750,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(step,[status(thm)],[t97091,t23]) ).
cnf(t97178,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t114750]) ).
cnf(t97399,plain,
meet(X1,meet(X2,join(complement(X1),X3))) = meet(X1,meet(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t1317,t97178]) ).
cnf(t114791,plain,
meet(X1,meet(X2,join(complement(X1),X3))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t97399,t1317]) ).
cnf(t105085,plain,
meet(X1,meet(X2,join(complement(X1),X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t114791]) ).
cnf(t105119,plain,
meet(X1,meet(complement(X2),complement(join(X2,complement(X1))))) = meet(X1,complement(X2)),
inference(cp,[status(thm)],[t105085,t95760]) ).
cnf(t54332,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X1)),
inference(cp,[status(thm)],[t54287,t14]) ).
cnf(t114655,plain,
complement(join(X1,X2)) = meet(complement(X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t54332,t23]) ).
cnf(t54684,plain,
meet(complement(X1),complement(join(X1,X2))) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t114655]) ).
cnf(t114792,plain,
meet(X1,complement(join(X2,complement(X1)))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t105119,t54684]) ).
cnf(t54720,plain,
complement(X1) = join(complement(X1),complement(join(X1,X2))),
inference(cp,[status(thm)],[t16,t54684]) ).
cnf(t54867,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t54720]) ).
cnf(t54868,plain,
complement(complement(X1)) = join(X1,complement(join(complement(X1),X2))),
inference(cp,[status(thm)],[t54867,t18812]) ).
cnf(t114656,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t54868,t18812]) ).
cnf(t55043,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t114656]) ).
cnf(t55050,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(cp,[status(thm)],[t55043,t37189]) ).
cnf(t55231,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t55050]) ).
cnf(t55236,plain,
complement(join(X1,complement(X2))) = meet(complement(join(X1,complement(X2))),X2),
inference(cp,[status(thm)],[t126,t55231]) ).
cnf(t114661,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t55236,t23]) ).
cnf(t56597,plain,
meet(X1,complement(join(X2,complement(X1)))) = complement(join(X2,complement(X1))),
inference(orient,[status(thm)],[t114661]) ).
cnf(t114793,plain,
complement(join(X2,complement(X1))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t114792,t56597]) ).
cnf(t105486,plain,
complement(join(X1,complement(X2))) = meet(X2,complement(X1)),
inference(orient,[status(thm)],[t114793]) ).
cnf(t105520,plain,
join(X1,complement(X2)) = complement(meet(X2,complement(X1))),
inference(cp,[status(thm)],[t18812,t105486]) ).
cnf(t106269,plain,
complement(meet(X1,complement(X2))) = join(X2,complement(X1)),
inference(orient,[status(thm)],[t105520]) ).
cnf(t106282,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t106269,t23]) ).
cnf(t106454,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t106282]) ).
cnf(t53311,plain,
join(X1,meet(complement(X1),join(X2,X1))) = join(X1,meet(complement(X1),join(X1,X2))),
inference(cp,[status(thm)],[t53227,t145]) ).
cnf(t114697,plain,
join(X1,meet(complement(X1),join(X2,X1))) = join(X1,meet(complement(X1),X2)),
inference(step,[status(thm)],[t53311,t53227]) ).
cnf(t74684,plain,
join(X1,meet(complement(X1),join(X2,X1))) = join(X1,meet(complement(X1),X2)),
inference(orient,[status(thm)],[t114697]) ).
cnf(t97206,plain,
meet(X1,meet(complement(complement(X1)),join(X2,complement(X1)))) = meet(X1,join(complement(X1),meet(complement(complement(X1)),X2))),
inference(cp,[status(thm)],[t97178,t74684]) ).
cnf(t114751,plain,
meet(X1,meet(X1,join(X2,complement(X1)))) = meet(X1,join(complement(X1),meet(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t97206,t18812]) ).
cnf(f0,axiom,
meet(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f0_nnf,plain,
! [X] : meet(X,X) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : meet(X,X) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
meet(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
meet(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t13,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t30,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t26,t13]) ).
cnf(t134,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t30]) ).
cnf(t114752,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,join(complement(X1),meet(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t114751,t134]) ).
cnf(t114753,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,meet(complement(complement(X1)),X2)),
inference(step,[status(thm)],[t114752,t97178]) ).
cnf(t114754,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,meet(X1,X2)),
inference(step,[status(thm)],[t114753,t18812]) ).
cnf(t114755,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t114754,t134]) ).
cnf(t97523,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t114755]) ).
cnf(t97548,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t97523,t18812]) ).
cnf(t98131,plain,
meet(complement(X1),join(X2,X1)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t97548]) ).
cnf(t106461,plain,
join(X1,complement(join(X2,X1))) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t106454,t98131]) ).
cnf(t114860,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(step,[status(thm)],[t106461,t106454]) ).
cnf(t106978,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t114860]) ).
cnf(t226,plain,
one = join(complement(join(X1,X2)),join(X2,X1)),
inference(cp,[status(thm)],[t222,t145]) ).
cnf(t114457,plain,
one = join(join(X2,X1),complement(join(X1,X2))),
inference(step,[status(thm)],[t226,t53]) ).
cnf(t114458,plain,
one = join(X2,join(X1,complement(join(X1,X2)))),
inference(step,[status(thm)],[t114457,t58]) ).
cnf(t734,plain,
join(X1,join(X2,complement(join(X2,X1)))) = one,
inference(orient,[status(thm)],[t114458]) ).
cnf(t95834,plain,
complement(X1) = meet(complement(X1),join(join(X2,complement(join(X2,X1))),complement(one))),
inference(cp,[status(thm)],[t95760,t734]) ).
cnf(t114784,plain,
complement(X1) = meet(complement(X1),join(X2,join(complement(join(X2,X1)),complement(one)))),
inference(step,[status(thm)],[t95834,t58]) ).
cnf(t114785,plain,
complement(X1) = meet(complement(X1),join(X2,join(complement(one),complement(join(X2,X1))))),
inference(step,[status(thm)],[t114784,t53]) ).
cnf(t114786,plain,
complement(X1) = meet(complement(X1),join(X2,join(zero,complement(join(X2,X1))))),
inference(step,[status(thm)],[t114785,t102]) ).
cnf(t114787,plain,
complement(X1) = meet(complement(X1),join(X2,complement(join(X2,X1)))),
inference(step,[status(thm)],[t114786,t84]) ).
cnf(t103507,plain,
meet(complement(X1),join(X2,complement(join(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t114787]) ).
cnf(t105120,plain,
meet(X1,meet(complement(X2),complement(join(complement(X1),X2)))) = meet(X1,complement(X2)),
inference(cp,[status(thm)],[t105085,t103507]) ).
cnf(t54339,plain,
complement(join(X1,X2)) = meet(complement(join(X1,X2)),complement(X2)),
inference(cp,[status(thm)],[t54287,t126]) ).
cnf(t114657,plain,
complement(join(X1,X2)) = meet(complement(X2),complement(join(X1,X2))),
inference(step,[status(thm)],[t54339,t23]) ).
cnf(t55617,plain,
meet(complement(X1),complement(join(X2,X1))) = complement(join(X2,X1)),
inference(orient,[status(thm)],[t114657]) ).
cnf(t114805,plain,
meet(X1,complement(join(complement(X1),X2))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t105120,t55617]) ).
cnf(t54685,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(join(complement(X1),X2))),
inference(cp,[status(thm)],[t54684,t18812]) ).
cnf(t56410,plain,
meet(X1,complement(join(complement(X1),X2))) = complement(join(complement(X1),X2)),
inference(orient,[status(thm)],[t54685]) ).
cnf(t114806,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t114805,t56410]) ).
cnf(t105734,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t114806]) ).
cnf(t106982,plain,
join(X1,complement(complement(X2))) = join(X1,meet(X2,complement(X1))),
inference(cp,[status(thm)],[t106978,t105734]) ).
cnf(t114861,plain,
join(X1,X2) = join(X1,meet(X2,complement(X1))),
inference(step,[status(thm)],[t106982,t18812]) ).
cnf(t107281,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t114861]) ).
cnf(t107293,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t107281,t23]) ).
cnf(t107491,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t107293]) ).
cnf(t107504,plain,
join(X1,meet(X2,join(complement(complement(X1)),X3))) = join(X1,meet(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t107491,t105085]) ).
cnf(t114889,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(complement(X1),meet(X2,X3))),
inference(step,[status(thm)],[t107504,t18812]) ).
cnf(t114890,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t114889,t107491]) ).
cnf(t110337,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t114890]) ).
cnf(t150,plain,
join(X1,join(join(X2,X1),X3)) = join(join(X1,X2),X3),
inference(cp,[status(thm)],[t58,t145]) ).
cnf(t114469,plain,
join(X1,join(X2,join(X1,X3))) = join(join(X1,X2),X3),
inference(step,[status(thm)],[t150,t58]) ).
cnf(t114470,plain,
join(X1,join(X2,join(X1,X3))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t114469,t58]) ).
cnf(t1203,plain,
join(X1,join(X2,join(X1,X3))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t114470]) ).
cnf(t97255,plain,
meet(X1,join(X2,join(complement(X1),X3))) = meet(X1,join(complement(X1),join(X2,X3))),
inference(cp,[status(thm)],[t97178,t1203]) ).
cnf(t114788,plain,
meet(X1,join(X2,join(complement(X1),X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t97255,t97178]) ).
cnf(t103864,plain,
meet(X1,join(X2,join(complement(X1),X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t114788]) ).
cnf(t107398,plain,
meet(X1,join(X2,meet(X3,complement(complement(X1))))) = meet(X1,join(X2,join(complement(X1),X3))),
inference(cp,[status(thm)],[t103864,t107281]) ).
cnf(t114877,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,join(complement(X1),X3))),
inference(step,[status(thm)],[t107398,t18812]) ).
cnf(t114878,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t114877,t103864]) ).
cnf(t109941,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t114878]) ).
cnf(t109998,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t109941,t53]) ).
cnf(t111598,plain,
meet(X1,join(meet(X2,X1),X3)) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t109998]) ).
cnf(t111907,plain,
join(meet(X1,X2),meet(X2,X3)) = join(meet(X1,X2),meet(X2,join(X3,X1))),
inference(cp,[status(thm)],[t110337,t111598]) ).
cnf(t129,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t126,t58]) ).
cnf(t275,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t129]) ).
cnf(t280,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(cp,[status(thm)],[t275,t16]) ).
cnf(t114444,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,X1))),
inference(step,[status(thm)],[t280,t26]) ).
cnf(t481,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t114444]) ).
cnf(t499,plain,
meet(X1,join(X2,X3)) = join(meet(X1,join(X2,X3)),meet(X3,X1)),
inference(cp,[status(thm)],[t117,t481]) ).
cnf(t114596,plain,
meet(X1,join(X2,X3)) = join(meet(X3,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t499,t53]) ).
cnf(t22259,plain,
join(meet(X1,X2),meet(X2,join(X3,X1))) = meet(X2,join(X3,X1)),
inference(orient,[status(thm)],[t114596]) ).
cnf(t114951,plain,
join(meet(X1,X2),meet(X2,X3)) = meet(X2,join(X3,X1)),
inference(step,[status(thm)],[t111907,t22259]) ).
cnf(t113841,plain,
join(meet(X1,X2),meet(X2,X3)) = meet(X2,join(X3,X1)),
inference(orient,[status(thm)],[t114951]) ).
cnf(f12,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f12_nnf,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(goal_0,negated_conjecture,
join(meet(a,b),meet(a,c)) != meet(a,join(b,c)),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(g0_0,plain,
join(meet(a,c),meet(a,b)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[goal_0,t53]) ).
cnf(g0_1,plain,
join(meet(c,a),meet(a,b)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_0,t23]) ).
cnf(g0_2,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[g0_1,t113841]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT212-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.37 % Computer : n016.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Wed Sep 23 20:39:05 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 53.60/12.38 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 53.60/12.38 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------