%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT036-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:55:04 PM UTC 2026
% Result : Unsatisfiable 118.89s 15.65s
% Output : Proof 118.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 91
% Number of leaves : 28
% Syntax : Number of formulae : 496 ( 492 unt; 0 def)
% Number of atoms : 500 ( 499 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 34 ( 30 ~; 4 |; 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 : 17 ( 17 usr; 13 con; 0-4 aty)
% Number of variables : 419 ( 52 sgn 56 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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(t15,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t81,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t15]) ).
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(t9,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t77,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t89,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t81,t77]) ).
cnf(t177873,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t89,t81]) ).
cnf(t4344,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t177873]) ).
cnf(t84,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t81,t77]) ).
cnf(t1709,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t84]) ).
cnf(t31,axiom,
sFlat7 = k(aa),
introduced(definition) ).
cnf(t58,plain,
k(aa) = sFlat7,
inference(orient,[status(thm)],[t31]) ).
cnf(f16,axiom,
k(meet(U,V)) = join(k(U),k(V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',k_on_meet) ).
fof(f16_nnf,plain,
! [U,V] : k(meet(U,V)) = join(k(U),k(V)),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [U,V] : k(meet(U,V)) = join(k(U),k(V)),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
k(meet(X0,X1)) = join(k(X0),k(X1)),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t13,plain,
join(k(X1),k(X2)) = k(meet(X1,X2)),
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t50,plain,
join(k(X1),k(X2)) = k(meet(X1,X2)),
inference(orient,[status(thm)],[t13]) ).
cnf(t24,axiom,
sFlat0 = k(bb),
introduced(definition) ).
cnf(t63,plain,
k(bb) = sFlat0,
inference(orient,[status(thm)],[t24]) ).
cnf(t64,plain,
k(meet(bb,X1)) = join(sFlat0,k(X1)),
inference(cp,[status(thm)],[t50,t63]) ).
cnf(t707,plain,
k(meet(bb,X1)) = join(sFlat0,k(X1)),
inference(orient,[status(thm)],[t64]) ).
cnf(t65,plain,
k(meet(X1,bb)) = join(k(X1),sFlat0),
inference(cp,[status(thm)],[t50,t63]) ).
cnf(t177708,plain,
k(meet(X1,bb)) = join(sFlat0,k(X1)),
inference(step,[status(thm)],[t65,t77]) ).
cnf(t722,plain,
k(meet(X1,bb)) = join(sFlat0,k(X1)),
inference(orient,[status(thm)],[t177708]) ).
cnf(t28,axiom,
sFlat4 = meet(bb,cc),
introduced(definition) ).
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(t11,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t190,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t177656,plain,
sFlat4 = meet(cc,bb),
inference(step,[status(thm)],[t28,t190]) ).
cnf(t228,plain,
meet(cc,bb) = sFlat4,
inference(orient,[status(thm)],[t177656]) ).
cnf(t725,plain,
join(sFlat0,k(cc)) = k(sFlat4),
inference(cp,[status(thm)],[t722,t228]) ).
cnf(t29,axiom,
sFlat5 = k(meet(bb,cc)),
introduced(definition) ).
cnf(t53,plain,
k(meet(bb,cc)) = sFlat5,
inference(orient,[status(thm)],[t29]) ).
cnf(t201,plain,
k(meet(bb,cc)) = sFlat5,
inference(rw,[status(thm)],[t53]) ).
cnf(t177661,plain,
k(meet(cc,bb)) = sFlat5,
inference(step,[status(thm)],[t201,t190]) ).
cnf(t177662,plain,
k(sFlat4) = sFlat5,
inference(step,[status(thm)],[t177661,t228]) ).
cnf(t279,plain,
k(sFlat4) = sFlat5,
inference(orient,[status(thm)],[t177662]) ).
cnf(t177711,plain,
join(sFlat0,k(cc)) = sFlat5,
inference(step,[status(thm)],[t725,t279]) ).
cnf(t744,plain,
join(sFlat0,k(cc)) = sFlat5,
inference(orient,[status(thm)],[t177711]) ).
cnf(t30,axiom,
sFlat6 = meet(aa,k(meet(bb,cc))),
introduced(definition) ).
cnf(t177655,plain,
sFlat6 = meet(aa,k(meet(cc,bb))),
inference(step,[status(thm)],[t30,t190]) ).
cnf(t221,plain,
meet(aa,k(meet(cc,bb))) = sFlat6,
inference(orient,[status(thm)],[t177655]) ).
cnf(t177657,plain,
meet(aa,k(sFlat4)) = sFlat6,
inference(step,[status(thm)],[t221,t228]) ).
cnf(t235,plain,
meet(aa,k(sFlat4)) = sFlat6,
inference(rw,[status(thm)],[t177657]) ).
cnf(t177663,plain,
meet(aa,sFlat5) = sFlat6,
inference(step,[status(thm)],[t235,t279]) ).
cnf(t177664,plain,
meet(sFlat5,aa) = sFlat6,
inference(step,[status(thm)],[t177663,t190]) ).
cnf(t284,plain,
meet(sFlat5,aa) = sFlat6,
inference(orient,[status(thm)],[t177664]) ).
cnf(t32,axiom,
sFlat8 = join(meet(aa,k(meet(bb,cc))),k(aa)),
introduced(definition) ).
cnf(t177649,plain,
sFlat8 = join(k(aa),meet(aa,k(meet(bb,cc)))),
inference(step,[status(thm)],[t32,t77]) ).
cnf(t177650,plain,
sFlat8 = join(sFlat7,meet(aa,k(meet(bb,cc)))),
inference(step,[status(thm)],[t177649,t58]) ).
cnf(t177651,plain,
sFlat8 = join(sFlat7,meet(aa,sFlat5)),
inference(step,[status(thm)],[t177650,t53]) ).
cnf(t176,plain,
join(sFlat7,meet(aa,sFlat5)) = sFlat8,
inference(orient,[status(thm)],[t177651]) ).
cnf(t200,plain,
join(sFlat7,meet(aa,sFlat5)) = sFlat8,
inference(rw,[status(thm)],[t176]) ).
cnf(t177673,plain,
join(sFlat7,meet(sFlat5,aa)) = sFlat8,
inference(step,[status(thm)],[t200,t190]) ).
cnf(t177674,plain,
join(sFlat7,sFlat6) = sFlat8,
inference(step,[status(thm)],[t177673,t284]) ).
cnf(t177675,plain,
join(sFlat6,sFlat7) = sFlat8,
inference(step,[status(thm)],[t177674,t77]) ).
cnf(t383,plain,
join(sFlat6,sFlat7) = sFlat8,
inference(orient,[status(thm)],[t177675]) ).
cnf(t387,plain,
join(sFlat6,join(sFlat7,X1)) = join(sFlat8,X1),
inference(cp,[status(thm)],[t81,t383]) ).
cnf(t1250,plain,
join(sFlat6,join(sFlat7,X1)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t387]) ).
cnf(f15,axiom,
k(join(U,V)) = meet(k(U),k(V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',k_on_join) ).
fof(f15_nnf,plain,
! [U,V] : k(join(U,V)) = meet(k(U),k(V)),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [U,V] : k(join(U,V)) = meet(k(U),k(V)),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
k(join(X0,X1)) = meet(k(X0),k(X1)),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t14,plain,
meet(k(X1),k(X2)) = k(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t42,plain,
meet(k(X1),k(X2)) = k(join(X1,X2)),
inference(orient,[status(thm)],[t14]) ).
cnf(t61,plain,
k(join(aa,X1)) = meet(sFlat7,k(X1)),
inference(cp,[status(thm)],[t42,t58]) ).
cnf(t680,plain,
k(join(aa,X1)) = meet(sFlat7,k(X1)),
inference(orient,[status(thm)],[t61]) ).
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(t10,plain,
join(X1,meet(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t35,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t10]) ).
cnf(t87,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t81,t35]) ).
cnf(t2636,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t87]) ).
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(t12,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t38,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t80,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t38,t77]) ).
cnf(t296,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t80]) ).
cnf(t304,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t296,t81]) ).
cnf(t4933,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t304]) ).
cnf(t4950,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(cp,[status(thm)],[t4933,t35]) ).
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(t16,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t202,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t178179,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,X1))),
inference(step,[status(thm)],[t4950,t202]) ).
cnf(t26016,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t178179]) ).
cnf(f14,axiom,
( meet(Z,join(X,Y)) = join(X,meet(Y,Z))
| meet(X,Z) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',modular) ).
fof(f14_nnf,plain,
! [X,Z,Y] :
( meet(Z,join(X,Y)) = join(X,meet(Y,Z))
| meet(X,Z) != X ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X,Z,Y] :
( meet(Z,join(X,Y)) = join(X,meet(Y,Z))
| meet(X,Z) != X ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( meet(X1,join(X0,X2)) = join(X0,meet(X2,X1))
| meet(X0,X1) != X0 ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t21,plain,
ifeq(meet(X1,X2),X1,meet(X2,join(X1,X3)),join(X1,meet(X3,X2))) = join(X1,meet(X3,X2)),
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t102,plain,
ifeq(meet(X1,X2),X1,meet(X2,join(X1,X3)),join(X1,meet(X3,X2))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t21]) ).
cnf(t116,plain,
join(X1,meet(X2,X3)) = ifeq(meet(X1,X3),X1,meet(X3,join(X2,X1)),join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t102,t77]) ).
cnf(t36995,plain,
ifeq(meet(X1,X2),X1,meet(X2,join(X3,X1)),join(X1,meet(X3,X2))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t116]) ).
cnf(t83,plain,
join(X1,join(X2,meet(join(X1,X2),X3))) = join(X1,X2),
inference(cp,[status(thm)],[t81,t35]) ).
cnf(t1175,plain,
join(X1,join(X2,meet(join(X1,X2),X3))) = join(X1,X2),
inference(orient,[status(thm)],[t83]) ).
cnf(f8,hypothesis,
join(X,meet(Y,Z)) = meet(join(X,Y),join(X,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dist_join) ).
fof(f8_nnf,plain,
! [X,Y,Z] : join(X,meet(Y,Z)) = meet(join(X,Y),join(X,Z)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X,Y,Z] : join(X,meet(Y,Z)) = meet(join(X,Y),join(X,Z)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
join(X0,meet(X1,X2)) = meet(join(X0,X1),join(X0,X2)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t19,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X2,X3)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t91,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t19]) ).
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(t5,plain,
meet(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t37,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t103,plain,
join(X1,meet(X2,X1)) = ifeq(X1,X1,meet(X1,join(X1,X2)),join(X1,meet(X2,X1))),
inference(cp,[status(thm)],[t102,t37]) ).
cnf(t8,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t40,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t8]) ).
cnf(t177667,plain,
join(X1,meet(X2,X1)) = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t103,t40]) ).
cnf(t177668,plain,
join(X1,meet(X2,X1)) = X1,
inference(step,[status(thm)],[t177667,t38]) ).
cnf(t331,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t177668]) ).
cnf(t334,plain,
aa = join(aa,sFlat6),
inference(cp,[status(thm)],[t331,t284]) ).
cnf(t177670,plain,
aa = join(sFlat6,aa),
inference(step,[status(thm)],[t334,t77]) ).
cnf(t352,plain,
join(sFlat6,aa) = aa,
inference(orient,[status(thm)],[t177670]) ).
cnf(t354,plain,
join(sFlat6,meet(X1,aa)) = meet(join(sFlat6,X1),aa),
inference(cp,[status(thm)],[t91,t352]) ).
cnf(t177822,plain,
join(sFlat6,meet(X1,aa)) = meet(aa,join(sFlat6,X1)),
inference(step,[status(thm)],[t354,t190]) ).
cnf(t3520,plain,
join(sFlat6,meet(X1,aa)) = meet(aa,join(sFlat6,X1)),
inference(orient,[status(thm)],[t177822]) ).
cnf(t3535,plain,
join(X1,sFlat6) = join(X1,meet(aa,join(sFlat6,join(X1,sFlat6)))),
inference(cp,[status(thm)],[t1175,t3520]) ).
cnf(t333,plain,
join(X1,X2) = join(join(X1,X2),X1),
inference(cp,[status(thm)],[t331,t38]) ).
cnf(t177731,plain,
join(X1,X2) = join(X1,join(X2,X1)),
inference(step,[status(thm)],[t333,t81]) ).
cnf(t1133,plain,
join(X1,join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t177731]) ).
cnf(t178106,plain,
join(X1,sFlat6) = join(X1,meet(aa,join(sFlat6,X1))),
inference(step,[status(thm)],[t3535,t1133]) ).
cnf(t18854,plain,
join(X1,meet(aa,join(sFlat6,X1))) = join(X1,sFlat6),
inference(orient,[status(thm)],[t178106]) ).
cnf(f9,hypothesis,
meet(X,join(Y,Z)) = join(meet(X,Y),meet(X,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dist_meet) ).
fof(f9_nnf,plain,
! [X,Y,Z] : meet(X,join(Y,Z)) = join(meet(X,Y),meet(X,Z)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X,Y,Z] : meet(X,join(Y,Z)) = join(meet(X,Y),meet(X,Z)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,X2)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t18,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t160,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t18]) ).
cnf(t195,plain,
meet(X1,join(X2,X3)) = join(meet(X2,X1),meet(X1,X3)),
inference(cp,[status(thm)],[t160,t190]) ).
cnf(t63023,plain,
join(meet(X1,X2),meet(X2,X3)) = meet(X2,join(X1,X3)),
inference(orient,[status(thm)],[t195]) ).
cnf(t63391,plain,
meet(aa,join(sFlat5,X1)) = join(sFlat6,meet(aa,X1)),
inference(cp,[status(thm)],[t63023,t284]) ).
cnf(t353,plain,
join(sFlat6,meet(aa,X1)) = meet(aa,join(sFlat6,X1)),
inference(cp,[status(thm)],[t91,t352]) ).
cnf(t3501,plain,
join(sFlat6,meet(aa,X1)) = meet(aa,join(sFlat6,X1)),
inference(orient,[status(thm)],[t353]) ).
cnf(t178678,plain,
meet(aa,join(sFlat5,X1)) = meet(aa,join(sFlat6,X1)),
inference(step,[status(thm)],[t63391,t3501]) ).
cnf(t64032,plain,
meet(aa,join(sFlat6,X1)) = meet(aa,join(sFlat5,X1)),
inference(orient,[status(thm)],[t178678]) ).
cnf(t178683,plain,
join(X1,meet(aa,join(sFlat5,X1))) = join(X1,sFlat6),
inference(step,[status(thm)],[t18854,t64032]) ).
cnf(t64111,plain,
join(X1,meet(aa,join(sFlat5,X1))) = join(X1,sFlat6),
inference(rw,[status(thm)],[t178683]) ).
cnf(t64888,plain,
join(X1,meet(aa,join(sFlat5,X1))) = join(X1,sFlat6),
inference(orient,[status(thm)],[t64111]) ).
cnf(t65043,plain,
join(X1,meet(aa,join(sFlat5,X1))) = ifeq(meet(X1,join(sFlat5,X1)),X1,meet(join(sFlat5,X1),join(aa,X1)),join(X1,sFlat6)),
inference(cp,[status(thm)],[t36995,t64888]) ).
cnf(t178726,plain,
join(X1,sFlat6) = ifeq(meet(X1,join(sFlat5,X1)),X1,meet(join(sFlat5,X1),join(aa,X1)),join(X1,sFlat6)),
inference(step,[status(thm)],[t65043,t64888]) ).
cnf(t178727,plain,
join(X1,sFlat6) = ifeq(X1,X1,meet(join(sFlat5,X1),join(aa,X1)),join(X1,sFlat6)),
inference(step,[status(thm)],[t178726,t296]) ).
cnf(t178728,plain,
join(X1,sFlat6) = meet(join(sFlat5,X1),join(aa,X1)),
inference(step,[status(thm)],[t178727,t40]) ).
cnf(t65245,plain,
meet(join(sFlat5,X1),join(aa,X1)) = join(X1,sFlat6),
inference(orient,[status(thm)],[t178728]) ).
cnf(t105,plain,
join(X1,meet(X2,join(X1,X3))) = ifeq(X1,X1,meet(join(X1,X3),join(X1,X2)),join(X1,meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t102,t38]) ).
cnf(t178077,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X3),join(X1,X2)),
inference(step,[status(thm)],[t105,t40]) ).
cnf(t178078,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X3,X2)),
inference(step,[status(thm)],[t178077,t91]) ).
cnf(t13660,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t178078]) ).
cnf(f21,hypothesis,
join(k(k(aa)),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lhs3) ).
fof(f21_nnf,plain,
join(k(k(aa)),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
join(k(k(aa)),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(t22,plain,
join(k(k(aa)),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t177635,plain,
join(k(sFlat7),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t22,t58]) ).
cnf(t177636,plain,
join(k(sFlat7),join(sFlat7,join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t177635,t58]) ).
cnf(t177637,plain,
join(k(sFlat7),join(sFlat7,k(meet(bb,cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t177636,t50]) ).
cnf(t177638,plain,
join(k(sFlat7),join(sFlat7,sFlat5)) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t177637,t53]) ).
cnf(t177639,plain,
join(k(sFlat7),join(sFlat5,sFlat7)) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t177638,t77]) ).
cnf(t177640,plain,
join(k(sFlat7),join(sFlat5,sFlat7)) = join(sFlat7,join(k(bb),k(cc))),
inference(step,[status(thm)],[t177639,t58]) ).
cnf(t177641,plain,
join(k(sFlat7),join(sFlat5,sFlat7)) = join(sFlat7,k(meet(bb,cc))),
inference(step,[status(thm)],[t177640,t50]) ).
cnf(t177642,plain,
join(k(sFlat7),join(sFlat5,sFlat7)) = join(sFlat7,sFlat5),
inference(step,[status(thm)],[t177641,t53]) ).
cnf(t177643,plain,
join(k(sFlat7),join(sFlat5,sFlat7)) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t177642,t77]) ).
cnf(t148,plain,
join(k(sFlat7),join(sFlat5,sFlat7)) = join(sFlat5,sFlat7),
inference(orient,[status(thm)],[t177643]) ).
cnf(t1956,plain,
join(k(sFlat7),join(sFlat5,sFlat7)) = join(sFlat5,sFlat7),
inference(rw,[status(thm)],[t148]) ).
cnf(t177879,plain,
join(sFlat5,join(k(sFlat7),sFlat7)) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t1956,t4344]) ).
cnf(t177880,plain,
join(sFlat5,join(sFlat7,k(sFlat7))) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t177879,t77]) ).
cnf(t4768,plain,
join(sFlat5,join(sFlat7,k(sFlat7))) = join(sFlat5,sFlat7),
inference(orient,[status(thm)],[t177880]) ).
cnf(t4943,plain,
k(sFlat7) = meet(k(sFlat7),join(sFlat5,sFlat7)),
inference(cp,[status(thm)],[t4933,t4768]) ).
cnf(t5168,plain,
meet(k(sFlat7),join(sFlat5,sFlat7)) = k(sFlat7),
inference(orient,[status(thm)],[t4943]) ).
cnf(t13671,plain,
join(sFlat5,meet(sFlat7,k(sFlat7))) = join(sFlat5,k(sFlat7)),
inference(cp,[status(thm)],[t13660,t5168]) ).
cnf(t14020,plain,
join(sFlat5,meet(sFlat7,k(sFlat7))) = join(sFlat5,k(sFlat7)),
inference(orient,[status(thm)],[t13671]) ).
cnf(t65272,plain,
join(meet(sFlat7,k(sFlat7)),sFlat6) = meet(join(sFlat5,k(sFlat7)),join(aa,meet(sFlat7,k(sFlat7)))),
inference(cp,[status(thm)],[t65245,t14020]) ).
cnf(t178737,plain,
join(sFlat6,meet(sFlat7,k(sFlat7))) = meet(join(sFlat5,k(sFlat7)),join(aa,meet(sFlat7,k(sFlat7)))),
inference(step,[status(thm)],[t65272,t77]) ).
cnf(t385,plain,
join(sFlat6,meet(sFlat7,X1)) = meet(sFlat8,join(sFlat6,X1)),
inference(cp,[status(thm)],[t91,t383]) ).
cnf(t3585,plain,
join(sFlat6,meet(sFlat7,X1)) = meet(sFlat8,join(sFlat6,X1)),
inference(orient,[status(thm)],[t385]) ).
cnf(t178738,plain,
meet(sFlat8,join(sFlat6,k(sFlat7))) = meet(join(sFlat5,k(sFlat7)),join(aa,meet(sFlat7,k(sFlat7)))),
inference(step,[status(thm)],[t178737,t3585]) ).
cnf(t121,plain,
join(X1,meet(X2,X2)) = ifeq(meet(X1,X2),X1,meet(X2,join(X1,X2)),join(X1,X2)),
inference(cp,[status(thm)],[t102,t37]) ).
cnf(t178384,plain,
join(X1,X2) = ifeq(meet(X1,X2),X1,meet(X2,join(X1,X2)),join(X1,X2)),
inference(step,[status(thm)],[t121,t37]) ).
cnf(t178385,plain,
join(X1,X2) = ifeq(meet(X1,X2),X1,X2,join(X1,X2)),
inference(step,[status(thm)],[t178384,t296]) ).
cnf(t44997,plain,
ifeq(meet(X1,X2),X1,X2,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t178385]) ).
cnf(t94,plain,
join(k(X1),meet(k(X2),X3)) = meet(k(meet(X1,X2)),join(k(X1),X3)),
inference(cp,[status(thm)],[t91,t50]) ).
cnf(t5920,plain,
meet(k(meet(X1,X2)),join(k(X1),X3)) = join(k(X1),meet(k(X2),X3)),
inference(orient,[status(thm)],[t94]) ).
cnf(t384,plain,
sFlat7 = meet(sFlat7,sFlat8),
inference(cp,[status(thm)],[t296,t383]) ).
cnf(t390,plain,
meet(sFlat7,sFlat8) = sFlat7,
inference(orient,[status(thm)],[t384]) ).
cnf(t5998,plain,
join(k(sFlat7),meet(k(sFlat8),X1)) = meet(k(sFlat7),join(k(sFlat7),X1)),
inference(cp,[status(thm)],[t5920,t390]) ).
cnf(t178034,plain,
join(k(sFlat7),meet(k(sFlat8),X1)) = k(sFlat7),
inference(step,[status(thm)],[t5998,t38]) ).
cnf(t10150,plain,
join(k(sFlat7),meet(k(sFlat8),X1)) = k(sFlat7),
inference(orient,[status(thm)],[t178034]) ).
cnf(t10155,plain,
meet(k(sFlat8),X1) = meet(meet(k(sFlat8),X1),k(sFlat7)),
inference(cp,[status(thm)],[t296,t10150]) ).
cnf(t178502,plain,
meet(k(sFlat8),X1) = meet(k(sFlat8),meet(X1,k(sFlat7))),
inference(step,[status(thm)],[t10155,t202]) ).
cnf(t56652,plain,
meet(k(sFlat8),meet(X1,k(sFlat7))) = meet(k(sFlat8),X1),
inference(orient,[status(thm)],[t178502]) ).
cnf(t56661,plain,
meet(k(sFlat8),X1) = meet(k(sFlat8),meet(k(sFlat7),X1)),
inference(cp,[status(thm)],[t56652,t190]) ).
cnf(t57081,plain,
meet(k(sFlat8),meet(k(sFlat7),X1)) = meet(k(sFlat8),X1),
inference(orient,[status(thm)],[t56661]) ).
cnf(f19,hypothesis,
join(k(k(aa)),join(aa,k(aa))) = join(aa,k(aa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lhs1) ).
fof(f19_nnf,plain,
join(k(k(aa)),join(aa,k(aa))) = join(aa,k(aa)),
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c19,plain,
join(k(k(aa)),join(aa,k(aa))) = join(aa,k(aa)),
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(t17,plain,
join(k(k(aa)),join(aa,k(aa))) = join(aa,k(aa)),
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t177644,plain,
join(k(sFlat7),join(aa,k(aa))) = join(aa,k(aa)),
inference(step,[status(thm)],[t17,t58]) ).
cnf(t177645,plain,
join(k(sFlat7),join(aa,sFlat7)) = join(aa,k(aa)),
inference(step,[status(thm)],[t177644,t58]) ).
cnf(t177646,plain,
join(k(sFlat7),join(sFlat7,aa)) = join(aa,k(aa)),
inference(step,[status(thm)],[t177645,t77]) ).
cnf(t177647,plain,
join(k(sFlat7),join(sFlat7,aa)) = join(aa,sFlat7),
inference(step,[status(thm)],[t177646,t58]) ).
cnf(t177648,plain,
join(k(sFlat7),join(sFlat7,aa)) = join(sFlat7,aa),
inference(step,[status(thm)],[t177647,t77]) ).
cnf(t154,plain,
join(k(sFlat7),join(sFlat7,aa)) = join(sFlat7,aa),
inference(orient,[status(thm)],[t177648]) ).
cnf(t1955,plain,
join(k(sFlat7),join(sFlat7,aa)) = join(sFlat7,aa),
inference(rw,[status(thm)],[t154]) ).
cnf(t177877,plain,
join(sFlat7,join(k(sFlat7),aa)) = join(sFlat7,aa),
inference(step,[status(thm)],[t1955,t4344]) ).
cnf(t177878,plain,
join(sFlat7,join(aa,k(sFlat7))) = join(sFlat7,aa),
inference(step,[status(thm)],[t177877,t77]) ).
cnf(t4757,plain,
join(sFlat7,join(aa,k(sFlat7))) = join(sFlat7,aa),
inference(orient,[status(thm)],[t177878]) ).
cnf(t4938,plain,
k(sFlat7) = meet(k(sFlat7),join(sFlat7,aa)),
inference(cp,[status(thm)],[t4933,t4757]) ).
cnf(t5148,plain,
meet(k(sFlat7),join(sFlat7,aa)) = k(sFlat7),
inference(orient,[status(thm)],[t4938]) ).
cnf(t57091,plain,
meet(k(sFlat8),join(sFlat7,aa)) = meet(k(sFlat8),k(sFlat7)),
inference(cp,[status(thm)],[t57081,t5148]) ).
cnf(t178536,plain,
meet(k(sFlat8),join(sFlat7,aa)) = k(join(sFlat8,sFlat7)),
inference(step,[status(thm)],[t57091,t42]) ).
cnf(t178537,plain,
meet(k(sFlat8),join(sFlat7,aa)) = k(join(sFlat7,sFlat8)),
inference(step,[status(thm)],[t178536,t77]) ).
cnf(t391,plain,
sFlat8 = join(sFlat8,sFlat7),
inference(cp,[status(thm)],[t331,t390]) ).
cnf(t177676,plain,
sFlat8 = join(sFlat7,sFlat8),
inference(step,[status(thm)],[t391,t77]) ).
cnf(t404,plain,
join(sFlat7,sFlat8) = sFlat8,
inference(orient,[status(thm)],[t177676]) ).
cnf(t178538,plain,
meet(k(sFlat8),join(sFlat7,aa)) = k(sFlat8),
inference(step,[status(thm)],[t178537,t404]) ).
cnf(t57395,plain,
meet(k(sFlat8),join(sFlat7,aa)) = k(sFlat8),
inference(orient,[status(thm)],[t178538]) ).
cnf(t57396,plain,
join(k(sFlat8),join(sFlat7,aa)) = ifeq(k(sFlat8),k(sFlat8),join(sFlat7,aa),join(k(sFlat8),join(sFlat7,aa))),
inference(cp,[status(thm)],[t44997,t57395]) ).
cnf(t178539,plain,
join(sFlat7,join(k(sFlat8),aa)) = ifeq(k(sFlat8),k(sFlat8),join(sFlat7,aa),join(k(sFlat8),join(sFlat7,aa))),
inference(step,[status(thm)],[t57396,t4344]) ).
cnf(t178540,plain,
join(sFlat7,join(aa,k(sFlat8))) = ifeq(k(sFlat8),k(sFlat8),join(sFlat7,aa),join(k(sFlat8),join(sFlat7,aa))),
inference(step,[status(thm)],[t178539,t77]) ).
cnf(t178541,plain,
join(sFlat7,join(aa,k(sFlat8))) = join(sFlat7,aa),
inference(step,[status(thm)],[t178540,t40]) ).
cnf(t57430,plain,
join(sFlat7,join(aa,k(sFlat8))) = join(sFlat7,aa),
inference(orient,[status(thm)],[t178541]) ).
cnf(t57438,plain,
join(aa,k(sFlat8)) = meet(join(aa,k(sFlat8)),join(sFlat7,aa)),
inference(cp,[status(thm)],[t296,t57430]) ).
cnf(t100,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X3,X1)),
inference(cp,[status(thm)],[t91,t77]) ).
cnf(t9432,plain,
meet(join(X1,X2),join(X3,X1)) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t100]) ).
cnf(t178548,plain,
join(aa,k(sFlat8)) = join(aa,meet(k(sFlat8),sFlat7)),
inference(step,[status(thm)],[t57438,t9432]) ).
cnf(t178549,plain,
join(aa,k(sFlat8)) = join(aa,meet(sFlat7,k(sFlat8))),
inference(step,[status(thm)],[t178548,t190]) ).
cnf(t62,plain,
k(join(X1,aa)) = meet(k(X1),sFlat7),
inference(cp,[status(thm)],[t42,t58]) ).
cnf(t177705,plain,
k(join(X1,aa)) = meet(sFlat7,k(X1)),
inference(step,[status(thm)],[t62,t190]) ).
cnf(t685,plain,
k(join(X1,aa)) = meet(sFlat7,k(X1)),
inference(orient,[status(thm)],[t177705]) ).
cnf(t355,plain,
join(sFlat6,join(aa,X1)) = join(aa,X1),
inference(cp,[status(thm)],[t81,t352]) ).
cnf(t1168,plain,
join(sFlat6,join(aa,X1)) = join(aa,X1),
inference(orient,[status(thm)],[t355]) ).
cnf(t1170,plain,
join(aa,X1) = join(sFlat6,join(X1,aa)),
inference(cp,[status(thm)],[t1168,t77]) ).
cnf(t2099,plain,
join(sFlat6,join(X1,aa)) = join(aa,X1),
inference(orient,[status(thm)],[t1170]) ).
cnf(t2101,plain,
join(aa,sFlat7) = join(sFlat8,aa),
inference(cp,[status(thm)],[t2099,t1250]) ).
cnf(t177760,plain,
join(sFlat7,aa) = join(sFlat8,aa),
inference(step,[status(thm)],[t2101,t77]) ).
cnf(t2119,plain,
join(sFlat8,aa) = join(sFlat7,aa),
inference(orient,[status(thm)],[t177760]) ).
cnf(t2123,plain,
meet(sFlat7,k(sFlat8)) = k(join(sFlat7,aa)),
inference(cp,[status(thm)],[t685,t2119]) ).
cnf(t177764,plain,
meet(sFlat7,k(sFlat8)) = meet(sFlat7,k(sFlat7)),
inference(step,[status(thm)],[t2123,t685]) ).
cnf(t2150,plain,
meet(sFlat7,k(sFlat8)) = meet(sFlat7,k(sFlat7)),
inference(orient,[status(thm)],[t177764]) ).
cnf(t178550,plain,
join(aa,k(sFlat8)) = join(aa,meet(sFlat7,k(sFlat7))),
inference(step,[status(thm)],[t178549,t2150]) ).
cnf(t57595,plain,
join(aa,meet(sFlat7,k(sFlat7))) = join(aa,k(sFlat8)),
inference(orient,[status(thm)],[t178550]) ).
cnf(t123,plain,
join(X1,meet(X2,join(X2,X3))) = ifeq(meet(X1,join(X2,X3)),X1,meet(join(X2,X3),join(X1,X2)),join(X1,X2)),
inference(cp,[status(thm)],[t102,t38]) ).
cnf(t178442,plain,
join(X1,X2) = ifeq(meet(X1,join(X2,X3)),X1,meet(join(X2,X3),join(X1,X2)),join(X1,X2)),
inference(step,[status(thm)],[t123,t38]) ).
cnf(t178443,plain,
join(X1,X2) = ifeq(meet(X1,join(X2,X3)),X1,join(X2,meet(X3,X1)),join(X1,X2)),
inference(step,[status(thm)],[t178442,t9432]) ).
cnf(t48977,plain,
ifeq(meet(X1,join(X2,X3)),X1,join(X2,meet(X3,X1)),join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t178443]) ).
cnf(t5150,plain,
meet(k(sFlat7),join(join(sFlat7,aa),X1)) = join(k(sFlat7),meet(k(sFlat7),X1)),
inference(cp,[status(thm)],[t160,t5148]) ).
cnf(t178598,plain,
meet(k(sFlat7),join(sFlat7,join(aa,X1))) = join(k(sFlat7),meet(k(sFlat7),X1)),
inference(step,[status(thm)],[t5150,t81]) ).
cnf(t178599,plain,
meet(k(sFlat7),join(sFlat7,join(aa,X1))) = k(sFlat7),
inference(step,[status(thm)],[t178598,t35]) ).
cnf(t60568,plain,
meet(k(sFlat7),join(sFlat7,join(aa,X1))) = k(sFlat7),
inference(orient,[status(thm)],[t178599]) ).
cnf(t60,plain,
k(meet(X1,aa)) = join(k(X1),sFlat7),
inference(cp,[status(thm)],[t50,t58]) ).
cnf(t177697,plain,
k(meet(X1,aa)) = join(sFlat7,k(X1)),
inference(step,[status(thm)],[t60,t77]) ).
cnf(t579,plain,
k(meet(X1,aa)) = join(sFlat7,k(X1)),
inference(orient,[status(thm)],[t177697]) ).
cnf(t356,plain,
sFlat6 = meet(sFlat6,aa),
inference(cp,[status(thm)],[t38,t352]) ).
cnf(t369,plain,
meet(sFlat6,aa) = sFlat6,
inference(orient,[status(thm)],[t356]) ).
cnf(t580,plain,
join(sFlat7,k(sFlat6)) = k(sFlat6),
inference(cp,[status(thm)],[t579,t369]) ).
cnf(t601,plain,
join(sFlat7,k(sFlat6)) = k(sFlat6),
inference(orient,[status(thm)],[t580]) ).
cnf(t4430,plain,
join(sFlat7,join(X1,k(sFlat6))) = join(X1,k(sFlat6)),
inference(cp,[status(thm)],[t4344,t601]) ).
cnf(t9247,plain,
join(sFlat7,join(X1,k(sFlat6))) = join(X1,k(sFlat6)),
inference(orient,[status(thm)],[t4430]) ).
cnf(t60571,plain,
k(sFlat7) = meet(k(sFlat7),join(aa,k(sFlat6))),
inference(cp,[status(thm)],[t60568,t9247]) ).
cnf(t60624,plain,
meet(k(sFlat7),join(aa,k(sFlat6))) = k(sFlat7),
inference(orient,[status(thm)],[t60571]) ).
cnf(t60637,plain,
join(k(sFlat7),aa) = ifeq(k(sFlat7),k(sFlat7),join(aa,meet(k(sFlat6),k(sFlat7))),join(k(sFlat7),aa)),
inference(cp,[status(thm)],[t48977,t60624]) ).
cnf(t178600,plain,
join(aa,k(sFlat7)) = ifeq(k(sFlat7),k(sFlat7),join(aa,meet(k(sFlat6),k(sFlat7))),join(k(sFlat7),aa)),
inference(step,[status(thm)],[t60637,t77]) ).
cnf(t178601,plain,
join(aa,k(sFlat7)) = join(aa,meet(k(sFlat6),k(sFlat7))),
inference(step,[status(thm)],[t178600,t40]) ).
cnf(t178602,plain,
join(aa,k(sFlat7)) = join(aa,k(join(sFlat6,sFlat7))),
inference(step,[status(thm)],[t178601,t42]) ).
cnf(t178603,plain,
join(aa,k(sFlat7)) = join(aa,k(sFlat8)),
inference(step,[status(thm)],[t178602,t383]) ).
cnf(t60661,plain,
join(aa,k(sFlat8)) = join(aa,k(sFlat7)),
inference(orient,[status(thm)],[t178603]) ).
cnf(t178604,plain,
join(aa,meet(sFlat7,k(sFlat7))) = join(aa,k(sFlat7)),
inference(step,[status(thm)],[t57595,t60661]) ).
cnf(t60662,plain,
join(aa,meet(sFlat7,k(sFlat7))) = join(aa,k(sFlat7)),
inference(orient,[status(thm)],[t178604]) ).
cnf(t178739,plain,
meet(sFlat8,join(sFlat6,k(sFlat7))) = meet(join(sFlat5,k(sFlat7)),join(aa,k(sFlat7))),
inference(step,[status(thm)],[t178738,t60662]) ).
cnf(t178740,plain,
meet(sFlat8,join(sFlat6,k(sFlat7))) = join(k(sFlat7),sFlat6),
inference(step,[status(thm)],[t178739,t65245]) ).
cnf(t178741,plain,
meet(sFlat8,join(sFlat6,k(sFlat7))) = join(sFlat6,k(sFlat7)),
inference(step,[status(thm)],[t178740,t77]) ).
cnf(t65517,plain,
meet(sFlat8,join(sFlat6,k(sFlat7))) = join(sFlat6,k(sFlat7)),
inference(orient,[status(thm)],[t178741]) ).
cnf(t65553,plain,
meet(k(sFlat7),sFlat8) = meet(k(sFlat7),join(sFlat6,k(sFlat7))),
inference(cp,[status(thm)],[t26016,t65517]) ).
cnf(t178742,plain,
meet(sFlat8,k(sFlat7)) = meet(k(sFlat7),join(sFlat6,k(sFlat7))),
inference(step,[status(thm)],[t65553,t190]) ).
cnf(t178743,plain,
meet(sFlat8,k(sFlat7)) = k(sFlat7),
inference(step,[status(thm)],[t178742,t296]) ).
cnf(t65569,plain,
meet(sFlat8,k(sFlat7)) = k(sFlat7),
inference(orient,[status(thm)],[t178743]) ).
cnf(t65608,plain,
join(sFlat8,X1) = join(sFlat8,join(k(sFlat7),X1)),
inference(cp,[status(thm)],[t2636,t65569]) ).
cnf(t66641,plain,
join(sFlat8,join(k(sFlat7),X1)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t65608]) ).
cnf(t66658,plain,
join(sFlat8,k(X1)) = join(sFlat8,k(meet(sFlat7,X1))),
inference(cp,[status(thm)],[t66641,t50]) ).
cnf(t68131,plain,
join(sFlat8,k(meet(sFlat7,X1))) = join(sFlat8,k(X1)),
inference(orient,[status(thm)],[t66658]) ).
cnf(t25,axiom,
sFlat1 = join(aa,k(bb)),
introduced(definition) ).
cnf(t177652,plain,
sFlat1 = join(aa,sFlat0),
inference(step,[status(thm)],[t25,t63]) ).
cnf(t177653,plain,
sFlat1 = join(sFlat0,aa),
inference(step,[status(thm)],[t177652,t77]) ).
cnf(t183,plain,
join(sFlat0,aa) = sFlat1,
inference(orient,[status(thm)],[t177653]) ).
cnf(t687,plain,
meet(sFlat7,k(sFlat0)) = k(sFlat1),
inference(cp,[status(thm)],[t685,t183]) ).
cnf(t26,axiom,
sFlat2 = k(join(aa,k(bb))),
introduced(definition) ).
cnf(t46,plain,
k(join(aa,k(bb))) = sFlat2,
inference(orient,[status(thm)],[t26]) ).
cnf(t177610,plain,
k(join(aa,sFlat0)) = sFlat2,
inference(step,[status(thm)],[t46,t63]) ).
cnf(t68,plain,
k(join(aa,sFlat0)) = sFlat2,
inference(rw,[status(thm)],[t177610]) ).
cnf(t177659,plain,
k(join(sFlat0,aa)) = sFlat2,
inference(step,[status(thm)],[t68,t77]) ).
cnf(t177660,plain,
k(sFlat1) = sFlat2,
inference(step,[status(thm)],[t177659,t183]) ).
cnf(t274,plain,
k(sFlat1) = sFlat2,
inference(orient,[status(thm)],[t177660]) ).
cnf(t177706,plain,
meet(sFlat7,k(sFlat0)) = sFlat2,
inference(step,[status(thm)],[t687,t274]) ).
cnf(t693,plain,
meet(sFlat7,k(sFlat0)) = sFlat2,
inference(orient,[status(thm)],[t177706]) ).
cnf(t68197,plain,
join(sFlat8,k(k(sFlat0))) = join(sFlat8,k(sFlat2)),
inference(cp,[status(thm)],[t68131,t693]) ).
cnf(t27,axiom,
sFlat3 = k(k(join(aa,k(bb)))),
introduced(definition) ).
cnf(t41,plain,
k(k(join(aa,k(bb)))) = sFlat3,
inference(orient,[status(thm)],[t27]) ).
cnf(t177609,plain,
k(sFlat2) = sFlat3,
inference(step,[status(thm)],[t41,t46]) ).
cnf(t49,plain,
k(sFlat2) = sFlat3,
inference(rw,[status(thm)],[t177609]) ).
cnf(t236,plain,
k(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t49]) ).
cnf(t178775,plain,
join(sFlat8,k(k(sFlat0))) = join(sFlat8,sFlat3),
inference(step,[status(thm)],[t68197,t236]) ).
cnf(t178776,plain,
join(sFlat8,k(k(sFlat0))) = join(sFlat3,sFlat8),
inference(step,[status(thm)],[t178775,t77]) ).
cnf(t68250,plain,
join(sFlat8,k(k(sFlat0))) = join(sFlat3,sFlat8),
inference(orient,[status(thm)],[t178776]) ).
cnf(t33,axiom,
sFlat9 = join(k(k(join(aa,k(bb)))),join(meet(aa,k(meet(bb,cc))),k(aa))),
introduced(definition) ).
cnf(t177628,plain,
sFlat9 = join(k(k(join(aa,sFlat0))),join(meet(aa,k(meet(bb,cc))),k(aa))),
inference(step,[status(thm)],[t33,t63]) ).
cnf(t177629,plain,
sFlat9 = join(k(k(join(sFlat0,aa))),join(meet(aa,k(meet(bb,cc))),k(aa))),
inference(step,[status(thm)],[t177628,t77]) ).
cnf(t177630,plain,
sFlat9 = join(k(k(join(sFlat0,aa))),join(k(aa),meet(aa,k(meet(bb,cc))))),
inference(step,[status(thm)],[t177629,t77]) ).
cnf(t177631,plain,
sFlat9 = join(k(k(join(sFlat0,aa))),join(sFlat7,meet(aa,k(meet(bb,cc))))),
inference(step,[status(thm)],[t177630,t58]) ).
cnf(t177632,plain,
sFlat9 = join(k(k(join(sFlat0,aa))),join(sFlat7,meet(aa,sFlat5))),
inference(step,[status(thm)],[t177631,t53]) ).
cnf(t177633,plain,
sFlat9 = join(join(sFlat7,meet(aa,sFlat5)),k(k(join(sFlat0,aa)))),
inference(step,[status(thm)],[t177632,t77]) ).
cnf(t177634,plain,
sFlat9 = join(sFlat7,join(meet(aa,sFlat5),k(k(join(sFlat0,aa))))),
inference(step,[status(thm)],[t177633,t81]) ).
cnf(t142,plain,
join(sFlat7,join(meet(aa,sFlat5),k(k(join(sFlat0,aa))))) = sFlat9,
inference(orient,[status(thm)],[t177634]) ).
cnf(t177654,plain,
join(sFlat7,join(meet(aa,sFlat5),k(k(sFlat1)))) = sFlat9,
inference(step,[status(thm)],[t142,t183]) ).
cnf(t189,plain,
join(sFlat7,join(meet(aa,sFlat5),k(k(sFlat1)))) = sFlat9,
inference(rw,[status(thm)],[t177654]) ).
cnf(t179468,plain,
join(sFlat7,join(meet(sFlat5,aa),k(k(sFlat1)))) = sFlat9,
inference(step,[status(thm)],[t189,t190]) ).
cnf(t179469,plain,
join(sFlat7,join(sFlat6,k(k(sFlat1)))) = sFlat9,
inference(step,[status(thm)],[t179468,t284]) ).
cnf(t179470,plain,
join(sFlat6,join(sFlat7,k(k(sFlat1)))) = sFlat9,
inference(step,[status(thm)],[t179469,t4344]) ).
cnf(t179471,plain,
join(sFlat8,k(k(sFlat1))) = sFlat9,
inference(step,[status(thm)],[t179470,t1250]) ).
cnf(t179472,plain,
join(sFlat8,k(sFlat2)) = sFlat9,
inference(step,[status(thm)],[t179471,t274]) ).
cnf(t179473,plain,
join(sFlat8,sFlat3) = sFlat9,
inference(step,[status(thm)],[t179472,t236]) ).
cnf(t179474,plain,
join(sFlat3,sFlat8) = sFlat9,
inference(step,[status(thm)],[t179473,t77]) ).
cnf(t138415,plain,
join(sFlat3,sFlat8) = sFlat9,
inference(orient,[status(thm)],[t179474]) ).
cnf(t179475,plain,
join(sFlat8,k(k(sFlat0))) = sFlat9,
inference(step,[status(thm)],[t68250,t138415]) ).
cnf(t138416,plain,
join(sFlat8,k(k(sFlat0))) = sFlat9,
inference(orient,[status(thm)],[t179475]) ).
cnf(t95,plain,
join(X1,meet(X2,X3)) = meet(join(X2,X1),join(X1,X3)),
inference(cp,[status(thm)],[t91,t77]) ).
cnf(t6845,plain,
meet(join(X1,X2),join(X2,X3)) = join(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t95]) ).
cnf(t7052,plain,
join(sFlat8,meet(X1,aa)) = meet(join(X1,sFlat8),join(sFlat7,aa)),
inference(cp,[status(thm)],[t6845,t2119]) ).
cnf(t127645,plain,
meet(join(X1,sFlat8),join(sFlat7,aa)) = join(sFlat8,meet(X1,aa)),
inference(orient,[status(thm)],[t7052]) ).
cnf(t138435,plain,
join(sFlat8,meet(sFlat3,aa)) = meet(sFlat9,join(sFlat7,aa)),
inference(cp,[status(thm)],[t127645,t138415]) ).
cnf(t340,plain,
join(X1,meet(meet(X2,X1),X3)) = meet(X1,join(X1,X3)),
inference(cp,[status(thm)],[t91,t331]) ).
cnf(t177887,plain,
join(X1,meet(X2,meet(X1,X3))) = meet(X1,join(X1,X3)),
inference(step,[status(thm)],[t340,t202]) ).
cnf(t177888,plain,
join(X1,meet(X2,meet(X1,X3))) = X1,
inference(step,[status(thm)],[t177887,t38]) ).
cnf(t5683,plain,
join(X1,meet(X2,meet(X1,X3))) = X1,
inference(orient,[status(thm)],[t177888]) ).
cnf(t307,plain,
meet(X1,join(join(X2,X1),X3)) = join(X1,meet(X1,X3)),
inference(cp,[status(thm)],[t160,t296]) ).
cnf(t177885,plain,
meet(X1,join(X2,join(X1,X3))) = join(X1,meet(X1,X3)),
inference(step,[status(thm)],[t307,t81]) ).
cnf(t177886,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(step,[status(thm)],[t177885,t35]) ).
cnf(t5253,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t177886]) ).
cnf(t5255,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t5253,t2636]) ).
cnf(t178192,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t5255,t202]) ).
cnf(t26869,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t178192]) ).
cnf(t285,plain,
sFlat5 = join(sFlat5,sFlat6),
inference(cp,[status(thm)],[t35,t284]) ).
cnf(t291,plain,
join(sFlat5,sFlat6) = sFlat5,
inference(orient,[status(thm)],[t285]) ).
cnf(t294,plain,
join(sFlat5,join(sFlat6,X1)) = join(sFlat5,X1),
inference(cp,[status(thm)],[t81,t291]) ).
cnf(t1053,plain,
join(sFlat5,join(sFlat6,X1)) = join(sFlat5,X1),
inference(orient,[status(thm)],[t294]) ).
cnf(t1054,plain,
join(sFlat5,sFlat7) = join(sFlat5,sFlat8),
inference(cp,[status(thm)],[t1053,t383]) ).
cnf(t1060,plain,
join(sFlat5,sFlat8) = join(sFlat5,sFlat7),
inference(orient,[status(thm)],[t1054]) ).
cnf(t1065,plain,
join(sFlat5,join(sFlat8,X1)) = join(join(sFlat5,sFlat7),X1),
inference(cp,[status(thm)],[t81,t1060]) ).
cnf(t177836,plain,
join(sFlat5,join(sFlat8,X1)) = join(sFlat5,join(sFlat7,X1)),
inference(step,[status(thm)],[t1065,t81]) ).
cnf(t3890,plain,
join(sFlat5,join(sFlat8,X1)) = join(sFlat5,join(sFlat7,X1)),
inference(orient,[status(thm)],[t177836]) ).
cnf(t68260,plain,
join(sFlat5,join(sFlat7,k(k(sFlat0)))) = join(sFlat5,join(sFlat3,sFlat8)),
inference(cp,[status(thm)],[t3890,t68250]) ).
cnf(f22,hypothesis,
join(k(k(k(bb))),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lhs4) ).
fof(f22_nnf,plain,
join(k(k(k(bb))),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
join(k(k(k(bb))),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(t23,plain,
join(k(k(k(bb))),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t177611,plain,
join(k(k(sFlat0)),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t23,t63]) ).
cnf(t177612,plain,
join(k(k(sFlat0)),join(sFlat7,join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t177611,t58]) ).
cnf(t177613,plain,
join(k(k(sFlat0)),join(sFlat7,k(meet(bb,cc)))) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t177612,t50]) ).
cnf(t177614,plain,
join(k(k(sFlat0)),join(sFlat7,sFlat5)) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t177613,t53]) ).
cnf(t177615,plain,
join(k(k(sFlat0)),join(sFlat5,sFlat7)) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t177614,t77]) ).
cnf(t177616,plain,
join(join(sFlat5,sFlat7),k(k(sFlat0))) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t177615,t77]) ).
cnf(t177617,plain,
join(sFlat5,join(sFlat7,k(k(sFlat0)))) = join(k(aa),join(k(bb),k(cc))),
inference(step,[status(thm)],[t177616,t81]) ).
cnf(t177618,plain,
join(sFlat5,join(sFlat7,k(k(sFlat0)))) = join(sFlat7,join(k(bb),k(cc))),
inference(step,[status(thm)],[t177617,t58]) ).
cnf(t177619,plain,
join(sFlat5,join(sFlat7,k(k(sFlat0)))) = join(sFlat7,k(meet(bb,cc))),
inference(step,[status(thm)],[t177618,t50]) ).
cnf(t177620,plain,
join(sFlat5,join(sFlat7,k(k(sFlat0)))) = join(sFlat7,sFlat5),
inference(step,[status(thm)],[t177619,t53]) ).
cnf(t177621,plain,
join(sFlat5,join(sFlat7,k(k(sFlat0)))) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t177620,t77]) ).
cnf(t131,plain,
join(sFlat5,join(sFlat7,k(k(sFlat0)))) = join(sFlat5,sFlat7),
inference(orient,[status(thm)],[t177621]) ).
cnf(t178777,plain,
join(sFlat5,sFlat7) = join(sFlat5,join(sFlat3,sFlat8)),
inference(step,[status(thm)],[t68260,t131]) ).
cnf(t1062,plain,
sFlat8 = meet(sFlat8,join(sFlat5,sFlat7)),
inference(cp,[status(thm)],[t296,t1060]) ).
cnf(t1075,plain,
meet(sFlat8,join(sFlat5,sFlat7)) = sFlat8,
inference(orient,[status(thm)],[t1062]) ).
cnf(t1077,plain,
meet(sFlat8,join(join(sFlat5,sFlat7),X1)) = join(sFlat8,meet(sFlat8,X1)),
inference(cp,[status(thm)],[t160,t1075]) ).
cnf(t177921,plain,
meet(sFlat8,join(sFlat5,join(sFlat7,X1))) = join(sFlat8,meet(sFlat8,X1)),
inference(step,[status(thm)],[t1077,t81]) ).
cnf(t177922,plain,
meet(sFlat8,join(sFlat5,join(sFlat7,X1))) = sFlat8,
inference(step,[status(thm)],[t177921,t35]) ).
cnf(t6434,plain,
meet(sFlat8,join(sFlat5,join(sFlat7,X1))) = sFlat8,
inference(orient,[status(thm)],[t177922]) ).
cnf(t6440,plain,
sFlat8 = meet(sFlat8,join(sFlat5,join(X1,sFlat7))),
inference(cp,[status(thm)],[t6434,t77]) ).
cnf(t7822,plain,
meet(sFlat8,join(sFlat5,join(X1,sFlat7))) = sFlat8,
inference(orient,[status(thm)],[t6440]) ).
cnf(t7829,plain,
join(sFlat5,join(X1,sFlat7)) = join(join(sFlat5,join(X1,sFlat7)),sFlat8),
inference(cp,[status(thm)],[t331,t7822]) ).
cnf(t177995,plain,
join(sFlat5,join(X1,sFlat7)) = join(sFlat5,join(join(X1,sFlat7),sFlat8)),
inference(step,[status(thm)],[t7829,t81]) ).
cnf(t177996,plain,
join(sFlat5,join(X1,sFlat7)) = join(sFlat5,join(X1,join(sFlat7,sFlat8))),
inference(step,[status(thm)],[t177995,t81]) ).
cnf(t177997,plain,
join(sFlat5,join(X1,sFlat7)) = join(sFlat5,join(X1,sFlat8)),
inference(step,[status(thm)],[t177996,t404]) ).
cnf(t7838,plain,
join(sFlat5,join(X1,sFlat8)) = join(sFlat5,join(X1,sFlat7)),
inference(orient,[status(thm)],[t177997]) ).
cnf(t178778,plain,
join(sFlat5,sFlat7) = join(sFlat5,join(sFlat3,sFlat7)),
inference(step,[status(thm)],[t178777,t7838]) ).
cnf(t178779,plain,
join(sFlat5,sFlat7) = join(sFlat3,join(sFlat5,sFlat7)),
inference(step,[status(thm)],[t178778,t4344]) ).
cnf(t68301,plain,
join(sFlat3,join(sFlat5,sFlat7)) = join(sFlat5,sFlat7),
inference(orient,[status(thm)],[t178779]) ).
cnf(t68320,plain,
meet(sFlat3,X1) = meet(sFlat3,meet(X1,join(sFlat5,sFlat7))),
inference(cp,[status(thm)],[t26869,t68301]) ).
cnf(t69593,plain,
meet(sFlat3,meet(X1,join(sFlat5,sFlat7))) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t68320]) ).
cnf(t388,plain,
sFlat6 = meet(sFlat6,sFlat8),
inference(cp,[status(thm)],[t38,t383]) ).
cnf(t397,plain,
meet(sFlat6,sFlat8) = sFlat6,
inference(orient,[status(thm)],[t388]) ).
cnf(t398,plain,
sFlat8 = join(sFlat8,sFlat6),
inference(cp,[status(thm)],[t331,t397]) ).
cnf(t177677,plain,
sFlat8 = join(sFlat6,sFlat8),
inference(step,[status(thm)],[t398,t77]) ).
cnf(t409,plain,
join(sFlat6,sFlat8) = sFlat8,
inference(orient,[status(thm)],[t177677]) ).
cnf(t64052,plain,
meet(aa,join(sFlat5,sFlat8)) = meet(aa,sFlat8),
inference(cp,[status(thm)],[t64032,t409]) ).
cnf(t178698,plain,
meet(aa,join(sFlat5,sFlat7)) = meet(aa,sFlat8),
inference(step,[status(thm)],[t64052,t1060]) ).
cnf(t178699,plain,
meet(aa,join(sFlat5,sFlat7)) = meet(sFlat8,aa),
inference(step,[status(thm)],[t178698,t190]) ).
cnf(t64119,plain,
meet(aa,join(sFlat5,sFlat7)) = meet(sFlat8,aa),
inference(orient,[status(thm)],[t178699]) ).
cnf(t69595,plain,
meet(sFlat3,aa) = meet(sFlat3,meet(sFlat8,aa)),
inference(cp,[status(thm)],[t69593,t64119]) ).
cnf(t69632,plain,
meet(sFlat3,meet(sFlat8,aa)) = meet(sFlat3,aa),
inference(orient,[status(thm)],[t69595]) ).
cnf(t69656,plain,
sFlat8 = join(sFlat8,meet(sFlat3,aa)),
inference(cp,[status(thm)],[t5683,t69632]) ).
cnf(t69662,plain,
join(sFlat8,meet(sFlat3,aa)) = sFlat8,
inference(orient,[status(thm)],[t69656]) ).
cnf(t179512,plain,
sFlat8 = meet(sFlat9,join(sFlat7,aa)),
inference(step,[status(thm)],[t138435,t69662]) ).
cnf(t139756,plain,
meet(sFlat9,join(sFlat7,aa)) = sFlat8,
inference(orient,[status(thm)],[t179512]) ).
cnf(t139767,plain,
meet(sFlat9,meet(join(sFlat7,aa),X1)) = meet(sFlat8,X1),
inference(cp,[status(thm)],[t202,t139756]) ).
cnf(t177347,plain,
meet(sFlat9,meet(join(sFlat7,aa),X1)) = meet(sFlat8,X1),
inference(orient,[status(thm)],[t139767]) ).
cnf(f20,hypothesis,
join(k(k(k(bb))),join(aa,k(aa))) = join(aa,k(aa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lhs2) ).
fof(f20_nnf,plain,
join(k(k(k(bb))),join(aa,k(aa))) = join(aa,k(aa)),
inference(nnf_transformation,[status(thm)],[f20]) ).
cnf(c20,plain,
join(k(k(k(bb))),join(aa,k(aa))) = join(aa,k(aa)),
inference(cnf_transformation,[status(esa)],[f20_nnf]) ).
cnf(t20,plain,
join(k(k(k(bb))),join(aa,k(aa))) = join(aa,k(aa)),
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t177622,plain,
join(join(aa,k(aa)),k(k(k(bb)))) = join(aa,k(aa)),
inference(step,[status(thm)],[t20,t77]) ).
cnf(t177623,plain,
join(aa,join(k(aa),k(k(k(bb))))) = join(aa,k(aa)),
inference(step,[status(thm)],[t177622,t81]) ).
cnf(t177624,plain,
join(aa,k(meet(aa,k(k(bb))))) = join(aa,k(aa)),
inference(step,[status(thm)],[t177623,t50]) ).
cnf(t177625,plain,
join(aa,k(meet(aa,k(sFlat0)))) = join(aa,k(aa)),
inference(step,[status(thm)],[t177624,t63]) ).
cnf(t177626,plain,
join(aa,k(meet(aa,k(sFlat0)))) = join(aa,sFlat7),
inference(step,[status(thm)],[t177625,t58]) ).
cnf(t177627,plain,
join(aa,k(meet(aa,k(sFlat0)))) = join(sFlat7,aa),
inference(step,[status(thm)],[t177626,t77]) ).
cnf(t136,plain,
join(aa,k(meet(aa,k(sFlat0)))) = join(sFlat7,aa),
inference(orient,[status(thm)],[t177627]) ).
cnf(t59,plain,
k(meet(aa,X1)) = join(sFlat7,k(X1)),
inference(cp,[status(thm)],[t50,t58]) ).
cnf(t344,plain,
k(meet(aa,X1)) = join(sFlat7,k(X1)),
inference(orient,[status(thm)],[t59]) ).
cnf(t177669,plain,
join(aa,join(sFlat7,k(k(sFlat0)))) = join(sFlat7,aa),
inference(step,[status(thm)],[t136,t344]) ).
cnf(t351,plain,
join(aa,join(sFlat7,k(k(sFlat0)))) = join(sFlat7,aa),
inference(rw,[status(thm)],[t177669]) ).
cnf(t178050,plain,
join(sFlat7,join(aa,k(k(sFlat0)))) = join(sFlat7,aa),
inference(step,[status(thm)],[t351,t4344]) ).
cnf(t11232,plain,
join(sFlat7,join(aa,k(k(sFlat0)))) = join(sFlat7,aa),
inference(orient,[status(thm)],[t178050]) ).
cnf(t11244,plain,
k(k(sFlat0)) = meet(k(k(sFlat0)),join(sFlat7,aa)),
inference(cp,[status(thm)],[t4933,t11232]) ).
cnf(t178195,plain,
k(k(sFlat0)) = meet(join(sFlat7,aa),k(k(sFlat0))),
inference(step,[status(thm)],[t11244,t190]) ).
cnf(t27188,plain,
meet(join(sFlat7,aa),k(k(sFlat0))) = k(k(sFlat0)),
inference(orient,[status(thm)],[t178195]) ).
cnf(t177350,plain,
meet(sFlat8,k(k(sFlat0))) = meet(sFlat9,k(k(sFlat0))),
inference(cp,[status(thm)],[t177347,t27188]) ).
cnf(t237,plain,
k(meet(sFlat2,X1)) = join(sFlat3,k(X1)),
inference(cp,[status(thm)],[t50,t236]) ).
cnf(t793,plain,
k(meet(sFlat2,X1)) = join(sFlat3,k(X1)),
inference(orient,[status(thm)],[t237]) ).
cnf(t695,plain,
k(sFlat0) = join(k(sFlat0),sFlat2),
inference(cp,[status(thm)],[t331,t693]) ).
cnf(t177707,plain,
k(sFlat0) = join(sFlat2,k(sFlat0)),
inference(step,[status(thm)],[t695,t77]) ).
cnf(t701,plain,
join(sFlat2,k(sFlat0)) = k(sFlat0),
inference(orient,[status(thm)],[t177707]) ).
cnf(t705,plain,
sFlat2 = meet(sFlat2,k(sFlat0)),
inference(cp,[status(thm)],[t38,t701]) ).
cnf(t715,plain,
meet(sFlat2,k(sFlat0)) = sFlat2,
inference(orient,[status(thm)],[t705]) ).
cnf(t798,plain,
join(sFlat3,k(k(sFlat0))) = k(sFlat2),
inference(cp,[status(thm)],[t793,t715]) ).
cnf(t177720,plain,
join(sFlat3,k(k(sFlat0))) = sFlat3,
inference(step,[status(thm)],[t798,t236]) ).
cnf(t840,plain,
join(sFlat3,k(k(sFlat0))) = sFlat3,
inference(orient,[status(thm)],[t177720]) ).
cnf(t844,plain,
join(sFlat3,join(k(k(sFlat0)),X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t81,t840]) ).
cnf(t12059,plain,
join(sFlat3,join(k(k(sFlat0)),X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t844]) ).
cnf(t12085,plain,
k(k(sFlat0)) = meet(k(k(sFlat0)),join(sFlat3,X1)),
inference(cp,[status(thm)],[t5253,t12059]) ).
cnf(t28237,plain,
meet(k(k(sFlat0)),join(sFlat3,X1)) = k(k(sFlat0)),
inference(orient,[status(thm)],[t12085]) ).
cnf(t28238,plain,
k(k(sFlat0)) = meet(join(sFlat3,X1),k(k(sFlat0))),
inference(cp,[status(thm)],[t28237,t190]) ).
cnf(t33882,plain,
meet(join(sFlat3,X1),k(k(sFlat0))) = k(k(sFlat0)),
inference(orient,[status(thm)],[t28238]) ).
cnf(t138499,plain,
k(k(sFlat0)) = meet(sFlat9,k(k(sFlat0))),
inference(cp,[status(thm)],[t33882,t138415]) ).
cnf(t145792,plain,
meet(sFlat9,k(k(sFlat0))) = k(k(sFlat0)),
inference(orient,[status(thm)],[t138499]) ).
cnf(t179752,plain,
meet(sFlat8,k(k(sFlat0))) = k(k(sFlat0)),
inference(step,[status(thm)],[t177350,t145792]) ).
cnf(t177456,plain,
meet(sFlat8,k(k(sFlat0))) = k(k(sFlat0)),
inference(orient,[status(thm)],[t179752]) ).
cnf(t177457,plain,
sFlat8 = join(sFlat8,k(k(sFlat0))),
inference(cp,[status(thm)],[t35,t177456]) ).
cnf(t179753,plain,
sFlat8 = sFlat9,
inference(step,[status(thm)],[t177457,t138416]) ).
cnf(t177527,plain,
sFlat9 = sFlat8,
inference(orient,[status(thm)],[t179753]) ).
cnf(t179754,plain,
join(sFlat8,k(k(sFlat0))) = sFlat8,
inference(step,[status(thm)],[t138416,t177527]) ).
cnf(t177528,plain,
join(sFlat8,k(k(sFlat0))) = sFlat8,
inference(orient,[status(thm)],[t179754]) ).
cnf(f23,negated_conjecture,
join(k(k(join(aa,k(bb)))),join(meet(aa,k(meet(bb,cc))),k(aa))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rhs) ).
fof(f23_nnf,plain,
join(k(k(join(aa,k(bb)))),join(meet(aa,k(meet(bb,cc))),k(aa))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
join(k(k(join(aa,k(bb)))),join(meet(aa,k(meet(bb,cc))),k(aa))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
join(k(k(join(aa,k(bb)))),join(meet(aa,k(meet(bb,cc))),k(aa))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(goal_0,negated_conjecture,
join(k(k(join(aa,k(bb)))),join(meet(aa,k(meet(bb,cc))),k(aa))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(g0_0,plain,
join(meet(aa,k(meet(bb,cc))),join(k(k(join(aa,k(bb)))),k(aa))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[goal_0,t4344]) ).
cnf(g0_1,plain,
join(k(aa),join(meet(aa,k(meet(bb,cc))),k(k(join(aa,k(bb)))))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_0,t1709]) ).
cnf(g0_2,plain,
join(sFlat7,join(meet(aa,k(meet(bb,cc))),k(k(join(aa,k(bb)))))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_1,t58]) ).
cnf(g0_3,plain,
join(sFlat7,join(meet(aa,join(sFlat0,k(cc))),k(k(join(aa,k(bb)))))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_2,t707]) ).
cnf(g0_4,plain,
join(sFlat7,join(meet(aa,sFlat5),k(k(join(aa,k(bb)))))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_3,t744]) ).
cnf(g0_5,plain,
join(sFlat7,join(meet(sFlat5,aa),k(k(join(aa,k(bb)))))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_4,t190]) ).
cnf(g0_6,plain,
join(sFlat7,join(sFlat6,k(k(join(aa,k(bb)))))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_5,t284]) ).
cnf(g0_7,plain,
join(sFlat6,join(sFlat7,k(k(join(aa,k(bb)))))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_6,t4344]) ).
cnf(g0_8,plain,
join(sFlat8,k(k(join(aa,k(bb))))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_7,t1250]) ).
cnf(g0_9,plain,
join(sFlat8,k(meet(sFlat7,k(k(bb))))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_8,t680]) ).
cnf(g0_10,plain,
join(sFlat8,k(k(k(bb)))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_9,t68131]) ).
cnf(g0_11,plain,
join(sFlat8,k(k(sFlat0))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_10,t63]) ).
cnf(g0_12,plain,
sFlat8 != join(meet(aa,k(meet(bb,cc))),k(aa)),
inference(rw,[status(thm)],[g0_11,t177528]) ).
cnf(g0_13,plain,
sFlat8 != join(k(aa),meet(aa,k(meet(bb,cc)))),
inference(rw,[status(thm)],[g0_12,t77]) ).
cnf(g0_14,plain,
sFlat8 != join(sFlat7,meet(aa,k(meet(bb,cc)))),
inference(rw,[status(thm)],[g0_13,t58]) ).
cnf(g0_15,plain,
sFlat8 != join(sFlat7,meet(aa,join(sFlat0,k(cc)))),
inference(rw,[status(thm)],[g0_14,t707]) ).
cnf(g0_16,plain,
sFlat8 != join(sFlat7,meet(aa,sFlat5)),
inference(rw,[status(thm)],[g0_15,t744]) ).
cnf(g0_17,plain,
sFlat8 != join(sFlat7,meet(sFlat5,aa)),
inference(rw,[status(thm)],[g0_16,t190]) ).
cnf(g0_18,plain,
sFlat8 != join(sFlat7,sFlat6),
inference(rw,[status(thm)],[g0_17,t284]) ).
cnf(g0_19,plain,
sFlat8 != join(sFlat6,sFlat7),
inference(rw,[status(thm)],[g0_18,t77]) ).
cnf(g0_20,plain,
sFlat8 != sFlat8,
inference(rw,[status(thm)],[g0_19,t383]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT036-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n011.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Wed Sep 23 20:04:27 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 118.89/15.65 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 118.89/15.65 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------