%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT005-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.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:54:58 PM UTC 2026
% Result : Unsatisfiable 14.24s 2.27s
% Output : Proof 14.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 20
% Syntax : Number of formulae : 251 ( 243 unt; 0 def)
% Number of atoms : 259 ( 248 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 31 ( 23 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-4 aty)
% Number of variables : 223 ( 31 sgn 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f12,axiom,
( meet(Z,join(X,Y)) = join(X,meet(Y,Z))
| meet(X,Z) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',modular) ).
fof(f12_nnf,plain,
! [X,Z,Y] :
( meet(Z,join(X,Y)) = join(X,meet(Y,Z))
| meet(X,Z) != X ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X,Z,Y] :
( meet(Z,join(X,Y)) = join(X,meet(Y,Z))
| meet(X,Z) != X ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( meet(X1,join(X0,X2)) = join(X0,meet(X2,X1))
| meet(X0,X1) != X0 ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t18,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)],[c12]) ).
cnf(t59,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)],[t18]) ).
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(t31,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t67,plain,
join(X1,meet(X2,X3)) = ifeq(meet(X3,X1),X1,meet(X3,join(X1,X2)),join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t59,t31]) ).
cnf(t10786,plain,
ifeq(meet(X1,X2),X2,meet(X1,join(X2,X3)),join(X2,meet(X3,X1))) = join(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t67]) ).
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(t25,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t12]) ).
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(t56,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t58,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t25,t56]) ).
cnf(t262,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t58]) ).
cnf(t20,axiom,
sFlat1 = join(r1,meet(r2,b)),
introduced(definition) ).
cnf(t19,axiom,
sFlat0 = meet(r2,b),
introduced(definition) ).
cnf(t49,plain,
meet(r2,b) = sFlat0,
inference(orient,[status(thm)],[t19]) ).
cnf(t17050,plain,
sFlat1 = join(r1,sFlat0),
inference(step,[status(thm)],[t20,t49]) ).
cnf(t17051,plain,
sFlat1 = join(sFlat0,r1),
inference(step,[status(thm)],[t17050,t56]) ).
cnf(t102,plain,
join(sFlat0,r1) = sFlat1,
inference(orient,[status(thm)],[t17051]) ).
cnf(t266,plain,
r1 = meet(r1,sFlat1),
inference(cp,[status(thm)],[t262,t102]) ).
cnf(t17063,plain,
r1 = meet(sFlat1,r1),
inference(step,[status(thm)],[t266,t31]) ).
cnf(t281,plain,
meet(sFlat1,r1) = r1,
inference(orient,[status(thm)],[t17063]) ).
cnf(t10884,plain,
join(r1,meet(X1,sFlat1)) = ifeq(r1,r1,meet(sFlat1,join(r1,X1)),join(r1,meet(X1,sFlat1))),
inference(cp,[status(thm)],[t10786,t281]) ).
cnf(t8,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t30,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t8]) ).
cnf(t17525,plain,
join(r1,meet(X1,sFlat1)) = meet(sFlat1,join(r1,X1)),
inference(step,[status(thm)],[t10884,t30]) ).
cnf(t11669,plain,
join(r1,meet(X1,sFlat1)) = meet(sFlat1,join(r1,X1)),
inference(orient,[status(thm)],[t17525]) ).
cnf(t11674,plain,
meet(sFlat1,join(r1,X1)) = join(r1,meet(sFlat1,X1)),
inference(cp,[status(thm)],[t11669,t31]) ).
cnf(t11887,plain,
join(r1,meet(sFlat1,X1)) = meet(sFlat1,join(r1,X1)),
inference(orient,[status(thm)],[t11674]) ).
cnf(t103,plain,
sFlat0 = meet(sFlat0,sFlat1),
inference(cp,[status(thm)],[t25,t102]) ).
cnf(t188,plain,
meet(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t103]) ).
cnf(t191,plain,
join(sFlat0,meet(X1,sFlat1)) = ifeq(sFlat0,sFlat0,meet(sFlat1,join(sFlat0,X1)),join(sFlat0,meet(X1,sFlat1))),
inference(cp,[status(thm)],[t59,t188]) ).
cnf(t17165,plain,
join(sFlat0,meet(X1,sFlat1)) = meet(sFlat1,join(sFlat0,X1)),
inference(step,[status(thm)],[t191,t30]) ).
cnf(t2054,plain,
join(sFlat0,meet(X1,sFlat1)) = meet(sFlat1,join(sFlat0,X1)),
inference(orient,[status(thm)],[t17165]) ).
cnf(t2064,plain,
meet(X1,sFlat1) = meet(meet(X1,sFlat1),meet(sFlat1,join(sFlat0,X1))),
inference(cp,[status(thm)],[t262,t2054]) ).
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(t34,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t17577,plain,
meet(X1,sFlat1) = meet(X1,meet(sFlat1,meet(sFlat1,join(sFlat0,X1)))),
inference(step,[status(thm)],[t2064,t34]) ).
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(t3,plain,
meet(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t24,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t38,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t34,t24]) ).
cnf(t341,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t38]) ).
cnf(t17578,plain,
meet(X1,sFlat1) = meet(X1,meet(sFlat1,join(sFlat0,X1))),
inference(step,[status(thm)],[t17577,t341]) ).
cnf(t16856,plain,
meet(X1,meet(sFlat1,join(sFlat0,X1))) = meet(X1,sFlat1),
inference(orient,[status(thm)],[t17578]) ).
cnf(t63,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)],[t59,t25]) ).
cnf(t17316,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X3),join(X1,X2)),
inference(step,[status(thm)],[t63,t30]) ).
cnf(t5252,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X3),join(X1,X2)),
inference(orient,[status(thm)],[t17316]) ).
cnf(t41,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t34,t31]) ).
cnf(t17210,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t41,t34]) ).
cnf(t2864,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t17210]) ).
cnf(f13,axiom,
( meet(X,Y) = n0
| ~ complement(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f13_nnf,plain,
! [X,Y] :
( meet(X,Y) = n0
| ~ complement(X,Y) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X,Y] :
( meet(X,Y) = n0
| ~ complement(X,Y) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( meet(X0,X1) = n0
| ~ complement(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t14,plain,
ifeq(complement(X1,X2),true,meet(X1,X2),n0) = n0,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t131,plain,
ifeq(complement(X1,X2),true,meet(X1,X2),n0) = n0,
inference(orient,[status(thm)],[t14]) ).
cnf(f16,hypothesis,
complement(r1,join(a,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_of_a_join_b) ).
fof(f16_nnf,plain,
complement(r1,join(a,b)),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
complement(r1,join(a,b)),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(t6,plain,
complement(r1,join(a,b)) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t17055,plain,
complement(r1,join(b,a)) = true,
inference(step,[status(thm)],[t6,t56]) ).
cnf(t129,plain,
complement(r1,join(b,a)) = true,
inference(orient,[status(thm)],[t17055]) ).
cnf(t133,plain,
n0 = ifeq(true,true,meet(r1,join(b,a)),n0),
inference(cp,[status(thm)],[t131,t129]) ).
cnf(t17065,plain,
n0 = meet(r1,join(b,a)),
inference(step,[status(thm)],[t133,t30]) ).
cnf(t305,plain,
meet(r1,join(b,a)) = n0,
inference(orient,[status(thm)],[t17065]) ).
cnf(t2895,plain,
meet(r1,meet(X1,join(b,a))) = meet(X1,n0),
inference(cp,[status(thm)],[t2864,t305]) ).
cnf(f8,axiom,
meet(X,n0) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_meet_0) ).
fof(f8_nnf,plain,
! [X] : meet(X,n0) = n0,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] : meet(X,n0) = n0,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
meet(X0,n0) = n0,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t4,plain,
meet(X1,n0) = n0,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t43,plain,
meet(X1,n0) = n0,
inference(orient,[status(thm)],[t4]) ).
cnf(t17264,plain,
meet(r1,meet(X1,join(b,a))) = n0,
inference(step,[status(thm)],[t2895,t43]) ).
cnf(t4090,plain,
meet(r1,meet(X1,join(b,a))) = n0,
inference(orient,[status(thm)],[t17264]) ).
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(t28,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t10]) ).
cnf(t33,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t28,t31]) ).
cnf(t212,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t33]) ).
cnf(t50,plain,
meet(r2,meet(b,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t34,t49]) ).
cnf(t351,plain,
meet(r2,meet(b,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t50]) ).
cnf(t354,plain,
meet(sFlat0,join(b,X1)) = meet(r2,b),
inference(cp,[status(thm)],[t351,t25]) ).
cnf(t17078,plain,
meet(sFlat0,join(b,X1)) = sFlat0,
inference(step,[status(thm)],[t354,t49]) ).
cnf(t372,plain,
meet(sFlat0,join(b,X1)) = sFlat0,
inference(orient,[status(thm)],[t17078]) ).
cnf(t374,plain,
join(b,X1) = join(join(b,X1),sFlat0),
inference(cp,[status(thm)],[t212,t372]) ).
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(t87,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t15]) ).
cnf(t17123,plain,
join(b,X1) = join(b,join(X1,sFlat0)),
inference(step,[status(thm)],[t374,t87]) ).
cnf(t1079,plain,
join(b,join(X1,sFlat0)) = join(b,X1),
inference(orient,[status(thm)],[t17123]) ).
cnf(t1084,plain,
join(X1,sFlat0) = meet(join(X1,sFlat0),join(b,X1)),
inference(cp,[status(thm)],[t262,t1079]) ).
cnf(t15082,plain,
meet(join(X1,sFlat0),join(b,X1)) = join(X1,sFlat0),
inference(orient,[status(thm)],[t1084]) ).
cnf(t15115,plain,
n0 = meet(r1,join(a,sFlat0)),
inference(cp,[status(thm)],[t4090,t15082]) ).
cnf(t17565,plain,
n0 = meet(r1,join(sFlat0,a)),
inference(step,[status(thm)],[t15115,t56]) ).
cnf(t15132,plain,
meet(r1,join(sFlat0,a)) = n0,
inference(orient,[status(thm)],[t17565]) ).
cnf(t15155,plain,
meet(r1,meet(X1,join(sFlat0,a))) = meet(X1,n0),
inference(cp,[status(thm)],[t2864,t15132]) ).
cnf(t17570,plain,
meet(r1,meet(X1,join(sFlat0,a))) = n0,
inference(step,[status(thm)],[t15155,t43]) ).
cnf(t15213,plain,
meet(r1,meet(X1,join(sFlat0,a))) = n0,
inference(orient,[status(thm)],[t17570]) ).
cnf(t51,plain,
r2 = join(r2,sFlat0),
inference(cp,[status(thm)],[t28,t49]) ).
cnf(t17056,plain,
r2 = join(sFlat0,r2),
inference(step,[status(thm)],[t51,t56]) ).
cnf(t166,plain,
join(sFlat0,r2) = r2,
inference(orient,[status(thm)],[t17056]) ).
cnf(t167,plain,
sFlat0 = meet(sFlat0,r2),
inference(cp,[status(thm)],[t25,t166]) ).
cnf(t200,plain,
meet(sFlat0,r2) = sFlat0,
inference(orient,[status(thm)],[t167]) ).
cnf(t203,plain,
join(sFlat0,meet(X1,r2)) = ifeq(sFlat0,sFlat0,meet(r2,join(sFlat0,X1)),join(sFlat0,meet(X1,r2))),
inference(cp,[status(thm)],[t59,t200]) ).
cnf(t17167,plain,
join(sFlat0,meet(X1,r2)) = meet(r2,join(sFlat0,X1)),
inference(step,[status(thm)],[t203,t30]) ).
cnf(t2084,plain,
join(sFlat0,meet(X1,r2)) = meet(r2,join(sFlat0,X1)),
inference(orient,[status(thm)],[t17167]) ).
cnf(t2090,plain,
meet(r2,join(sFlat0,X1)) = join(sFlat0,meet(r2,X1)),
inference(cp,[status(thm)],[t2084,t31]) ).
cnf(t2582,plain,
join(sFlat0,meet(r2,X1)) = meet(r2,join(sFlat0,X1)),
inference(orient,[status(thm)],[t2090]) ).
cnf(t21,axiom,
sFlat2 = meet(r2,a),
introduced(definition) ).
cnf(t53,plain,
meet(r2,a) = sFlat2,
inference(orient,[status(thm)],[t21]) ).
cnf(t2589,plain,
meet(r2,join(sFlat0,a)) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t2582,t53]) ).
cnf(t2604,plain,
meet(r2,join(sFlat0,a)) = join(sFlat0,sFlat2),
inference(orient,[status(thm)],[t2589]) ).
cnf(t15219,plain,
n0 = meet(r1,join(sFlat0,sFlat2)),
inference(cp,[status(thm)],[t15213,t2604]) ).
cnf(t15246,plain,
meet(r1,join(sFlat0,sFlat2)) = n0,
inference(orient,[status(thm)],[t15219]) ).
cnf(t15256,plain,
meet(join(sFlat0,sFlat2),join(sFlat0,r1)) = join(sFlat0,n0),
inference(cp,[status(thm)],[t5252,t15246]) ).
cnf(t17571,plain,
meet(join(sFlat0,sFlat2),sFlat1) = join(sFlat0,n0),
inference(step,[status(thm)],[t15256,t102]) ).
cnf(t17572,plain,
meet(sFlat1,join(sFlat0,sFlat2)) = join(sFlat0,n0),
inference(step,[status(thm)],[t17571,t31]) ).
cnf(f9,axiom,
join(X,n0) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_join_0) ).
fof(f9_nnf,plain,
! [X] : join(X,n0) = X,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] : join(X,n0) = X,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
join(X0,n0) = X0,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t1,plain,
join(X1,n0) = X1,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t29,plain,
join(X1,n0) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t17573,plain,
meet(sFlat1,join(sFlat0,sFlat2)) = sFlat0,
inference(step,[status(thm)],[t17572,t29]) ).
cnf(t15270,plain,
meet(sFlat1,join(sFlat0,sFlat2)) = sFlat0,
inference(orient,[status(thm)],[t17573]) ).
cnf(t16860,plain,
meet(sFlat2,sFlat1) = meet(sFlat2,sFlat0),
inference(cp,[status(thm)],[t16856,t15270]) ).
cnf(t17579,plain,
meet(sFlat1,sFlat2) = meet(sFlat2,sFlat0),
inference(step,[status(thm)],[t16860,t31]) ).
cnf(t17580,plain,
meet(sFlat1,sFlat2) = meet(sFlat0,sFlat2),
inference(step,[status(thm)],[t17579,t31]) ).
cnf(f17,hypothesis,
complement(r2,meet(a,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_of_a_meet_b) ).
fof(f17_nnf,plain,
complement(r2,meet(a,b)),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
complement(r2,meet(a,b)),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(t7,plain,
complement(r2,meet(a,b)) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t17054,plain,
complement(r2,meet(b,a)) = true,
inference(step,[status(thm)],[t7,t31]) ).
cnf(t127,plain,
complement(r2,meet(b,a)) = true,
inference(orient,[status(thm)],[t17054]) ).
cnf(t132,plain,
n0 = ifeq(true,true,meet(r2,meet(b,a)),n0),
inference(cp,[status(thm)],[t131,t127]) ).
cnf(t17064,plain,
n0 = meet(r2,meet(b,a)),
inference(step,[status(thm)],[t132,t30]) ).
cnf(t300,plain,
meet(r2,meet(b,a)) = n0,
inference(orient,[status(thm)],[t17064]) ).
cnf(t17077,plain,
meet(sFlat0,a) = n0,
inference(step,[status(thm)],[t300,t351]) ).
cnf(t365,plain,
meet(sFlat0,a) = n0,
inference(rw,[status(thm)],[t17077]) ).
cnf(t366,plain,
meet(sFlat0,a) = n0,
inference(orient,[status(thm)],[t365]) ).
cnf(t368,plain,
meet(sFlat0,meet(a,X1)) = meet(n0,X1),
inference(cp,[status(thm)],[t34,t366]) ).
cnf(t44,plain,
n0 = meet(n0,X1),
inference(cp,[status(thm)],[t43,t31]) ).
cnf(t160,plain,
meet(n0,X1) = n0,
inference(orient,[status(thm)],[t44]) ).
cnf(t17080,plain,
meet(sFlat0,meet(a,X1)) = n0,
inference(step,[status(thm)],[t368,t160]) ).
cnf(t409,plain,
meet(sFlat0,meet(a,X1)) = n0,
inference(orient,[status(thm)],[t17080]) ).
cnf(t410,plain,
n0 = meet(sFlat0,meet(X1,a)),
inference(cp,[status(thm)],[t409,t31]) ).
cnf(t425,plain,
meet(sFlat0,meet(X1,a)) = n0,
inference(orient,[status(thm)],[t410]) ).
cnf(t220,plain,
a = join(a,sFlat2),
inference(cp,[status(thm)],[t212,t53]) ).
cnf(t17061,plain,
a = join(sFlat2,a),
inference(step,[status(thm)],[t220,t56]) ).
cnf(t242,plain,
join(sFlat2,a) = a,
inference(orient,[status(thm)],[t17061]) ).
cnf(t243,plain,
sFlat2 = meet(sFlat2,a),
inference(cp,[status(thm)],[t25,t242]) ).
cnf(t255,plain,
meet(sFlat2,a) = sFlat2,
inference(orient,[status(thm)],[t243]) ).
cnf(t426,plain,
n0 = meet(sFlat0,sFlat2),
inference(cp,[status(thm)],[t425,t255]) ).
cnf(t434,plain,
meet(sFlat0,sFlat2) = n0,
inference(orient,[status(thm)],[t426]) ).
cnf(t17581,plain,
meet(sFlat1,sFlat2) = n0,
inference(step,[status(thm)],[t17580,t434]) ).
cnf(t16927,plain,
meet(sFlat1,sFlat2) = n0,
inference(orient,[status(thm)],[t17581]) ).
cnf(t16933,plain,
meet(sFlat1,join(r1,sFlat2)) = join(r1,n0),
inference(cp,[status(thm)],[t11887,t16927]) ).
cnf(t17589,plain,
meet(sFlat1,join(sFlat2,r1)) = join(r1,n0),
inference(step,[status(thm)],[t16933,t56]) ).
cnf(t22,axiom,
sFlat3 = join(r1,meet(r2,a)),
introduced(definition) ).
cnf(t17052,plain,
sFlat3 = join(r1,sFlat2),
inference(step,[status(thm)],[t22,t53]) ).
cnf(t17053,plain,
sFlat3 = join(sFlat2,r1),
inference(step,[status(thm)],[t17052,t56]) ).
cnf(t106,plain,
join(sFlat2,r1) = sFlat3,
inference(orient,[status(thm)],[t17053]) ).
cnf(t17590,plain,
meet(sFlat1,sFlat3) = join(r1,n0),
inference(step,[status(thm)],[t17589,t106]) ).
cnf(t23,axiom,
sFlat4 = meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))),
introduced(definition) ).
cnf(t46,plain,
meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))) = sFlat4,
inference(orient,[status(thm)],[t23]) ).
cnf(t17049,plain,
meet(join(r1,sFlat0),join(r1,meet(r2,a))) = sFlat4,
inference(step,[status(thm)],[t46,t49]) ).
cnf(t52,plain,
meet(join(r1,sFlat0),join(r1,meet(r2,a))) = sFlat4,
inference(rw,[status(thm)],[t17049]) ).
cnf(t17281,plain,
meet(join(sFlat0,r1),join(r1,meet(r2,a))) = sFlat4,
inference(step,[status(thm)],[t52,t56]) ).
cnf(t17282,plain,
meet(sFlat1,join(r1,meet(r2,a))) = sFlat4,
inference(step,[status(thm)],[t17281,t102]) ).
cnf(t17283,plain,
meet(sFlat1,join(r1,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t17282,t53]) ).
cnf(t17284,plain,
meet(sFlat1,join(sFlat2,r1)) = sFlat4,
inference(step,[status(thm)],[t17283,t56]) ).
cnf(t17285,plain,
meet(sFlat1,sFlat3) = sFlat4,
inference(step,[status(thm)],[t17284,t106]) ).
cnf(t4493,plain,
meet(sFlat1,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t17285]) ).
cnf(t17591,plain,
sFlat4 = join(r1,n0),
inference(step,[status(thm)],[t17590,t4493]) ).
cnf(t17592,plain,
sFlat4 = r1,
inference(step,[status(thm)],[t17591,t29]) ).
cnf(t16984,plain,
r1 = sFlat4,
inference(orient,[status(thm)],[t17592]) ).
cnf(t2059,plain,
meet(sFlat1,join(sFlat0,X1)) = join(sFlat0,meet(sFlat1,X1)),
inference(cp,[status(thm)],[t2054,t31]) ).
cnf(t2540,plain,
join(sFlat0,meet(sFlat1,X1)) = meet(sFlat1,join(sFlat0,X1)),
inference(orient,[status(thm)],[t2059]) ).
cnf(t4494,plain,
meet(sFlat1,join(sFlat0,sFlat3)) = join(sFlat0,sFlat4),
inference(cp,[status(thm)],[t2540,t4493]) ).
cnf(t104,plain,
join(sFlat0,join(r1,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t87,t102]) ).
cnf(t521,plain,
join(sFlat0,join(r1,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t104]) ).
cnf(t526,plain,
join(sFlat1,X1) = join(sFlat0,join(X1,r1)),
inference(cp,[status(thm)],[t521,t56]) ).
cnf(t1158,plain,
join(sFlat0,join(X1,r1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t526]) ).
cnf(t265,plain,
r1 = meet(r1,sFlat3),
inference(cp,[status(thm)],[t262,t106]) ).
cnf(t17062,plain,
r1 = meet(sFlat3,r1),
inference(step,[status(thm)],[t265,t31]) ).
cnf(t274,plain,
meet(sFlat3,r1) = r1,
inference(orient,[status(thm)],[t17062]) ).
cnf(t277,plain,
sFlat3 = join(sFlat3,r1),
inference(cp,[status(thm)],[t28,t274]) ).
cnf(t288,plain,
join(sFlat3,r1) = sFlat3,
inference(orient,[status(thm)],[t277]) ).
cnf(t1162,plain,
join(sFlat1,sFlat3) = join(sFlat0,sFlat3),
inference(cp,[status(thm)],[t1158,t288]) ).
cnf(t1191,plain,
join(sFlat1,sFlat3) = join(sFlat0,sFlat3),
inference(orient,[status(thm)],[t1162]) ).
cnf(t1192,plain,
sFlat1 = meet(sFlat1,join(sFlat0,sFlat3)),
inference(cp,[status(thm)],[t25,t1191]) ).
cnf(t1225,plain,
meet(sFlat1,join(sFlat0,sFlat3)) = sFlat1,
inference(orient,[status(thm)],[t1192]) ).
cnf(t17288,plain,
sFlat1 = join(sFlat0,sFlat4),
inference(step,[status(thm)],[t4494,t1225]) ).
cnf(t4517,plain,
join(sFlat0,sFlat4) = sFlat1,
inference(orient,[status(thm)],[t17288]) ).
cnf(t107,plain,
sFlat2 = meet(sFlat2,sFlat3),
inference(cp,[status(thm)],[t25,t106]) ).
cnf(t194,plain,
meet(sFlat2,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t107]) ).
cnf(t197,plain,
join(sFlat2,meet(X1,sFlat3)) = ifeq(sFlat2,sFlat2,meet(sFlat3,join(sFlat2,X1)),join(sFlat2,meet(X1,sFlat3))),
inference(cp,[status(thm)],[t59,t194]) ).
cnf(t17166,plain,
join(sFlat2,meet(X1,sFlat3)) = meet(sFlat3,join(sFlat2,X1)),
inference(step,[status(thm)],[t197,t30]) ).
cnf(t2069,plain,
join(sFlat2,meet(X1,sFlat3)) = meet(sFlat3,join(sFlat2,X1)),
inference(orient,[status(thm)],[t17166]) ).
cnf(t4495,plain,
meet(sFlat3,join(sFlat2,sFlat1)) = join(sFlat2,sFlat4),
inference(cp,[status(thm)],[t2069,t4493]) ).
cnf(t17300,plain,
meet(sFlat3,join(sFlat1,sFlat2)) = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t4495,t56]) ).
cnf(t1163,plain,
join(sFlat1,sFlat2) = join(sFlat0,sFlat3),
inference(cp,[status(thm)],[t1158,t106]) ).
cnf(t1199,plain,
join(sFlat1,sFlat2) = join(sFlat0,sFlat3),
inference(orient,[status(thm)],[t1163]) ).
cnf(t17301,plain,
meet(sFlat3,join(sFlat0,sFlat3)) = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t17300,t1199]) ).
cnf(t17302,plain,
sFlat3 = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t17301,t262]) ).
cnf(t4814,plain,
join(sFlat2,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t17302]) ).
cnf(f18,negated_conjecture,
r1 != meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_lemma) ).
fof(f18_nnf,plain,
r1 != meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
r1 != meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
r1 != meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(goal_0,negated_conjecture,
meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))) != r1,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(g0_0,plain,
meet(join(sFlat4,meet(r2,b)),join(r1,meet(r2,a))) != r1,
inference(rw,[status(thm)],[goal_0,t16984]) ).
cnf(g0_1,plain,
meet(join(sFlat4,sFlat0),join(r1,meet(r2,a))) != r1,
inference(rw,[status(thm)],[g0_0,t49]) ).
cnf(g0_2,plain,
meet(join(sFlat0,sFlat4),join(r1,meet(r2,a))) != r1,
inference(rw,[status(thm)],[g0_1,t56]) ).
cnf(g0_3,plain,
meet(sFlat1,join(r1,meet(r2,a))) != r1,
inference(rw,[status(thm)],[g0_2,t4517]) ).
cnf(g0_4,plain,
meet(sFlat1,join(sFlat4,meet(r2,a))) != r1,
inference(rw,[status(thm)],[g0_3,t16984]) ).
cnf(g0_5,plain,
meet(sFlat1,join(sFlat4,sFlat2)) != r1,
inference(rw,[status(thm)],[g0_4,t53]) ).
cnf(g0_6,plain,
meet(sFlat1,join(sFlat2,sFlat4)) != r1,
inference(rw,[status(thm)],[g0_5,t56]) ).
cnf(g0_7,plain,
meet(sFlat1,sFlat3) != r1,
inference(rw,[status(thm)],[g0_6,t4814]) ).
cnf(g0_8,plain,
sFlat4 != r1,
inference(rw,[status(thm)],[g0_7,t4493]) ).
cnf(g0_9,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_8,t16984]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT005-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n002.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 20:01:48 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 14.24/2.27 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.24/2.27 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------