%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT005-4 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n026.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 7.83s 1.63s
% Output : Proof 7.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 15
% Syntax : Number of formulae : 210 ( 206 unt; 0 def)
% Number of atoms : 214 ( 213 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 16 ( 12 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-4 aty)
% Number of variables : 212 ( 32 sgn 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f4,axiom,
meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox/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(t13,plain,
meet(X1,X2) = meet(X2,X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t28,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t13]) ).
cnf(t20,axiom,
sFlat0 = meet(a2,b2),
introduced(definition) ).
cnf(t6235,plain,
sFlat0 = meet(b2,a2),
inference(step,[status(thm)],[t20,t28]) ).
cnf(t47,plain,
meet(b2,a2) = sFlat0,
inference(orient,[status(thm)],[t6235]) ).
cnf(f12,axiom,
( meet(Z,join(X,Y)) = join(X,meet(Y,Z))
| meet(X,Z) != X ),
file('/export/starexec/sandbox/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(t19,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(t54,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)],[t19]) ).
cnf(f2,axiom,
meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox/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(t14,plain,
meet(X1,join(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t22,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(f17,negated_conjecture,
join(r1,meet(a,r2)) = b2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',define_b2) ).
fof(f17_nnf,plain,
join(r1,meet(a,r2)) = b2,
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
join(r1,meet(a,r2)) = b2,
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(t10,plain,
join(r1,meet(a,r2)) = b2,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t6236,plain,
join(r1,meet(r2,a)) = b2,
inference(step,[status(thm)],[t10,t28]) ).
cnf(t97,plain,
join(r1,meet(r2,a)) = b2,
inference(orient,[status(thm)],[t6236]) ).
cnf(t98,plain,
r1 = meet(r1,b2),
inference(cp,[status(thm)],[t22,t97]) ).
cnf(t133,plain,
meet(r1,b2) = r1,
inference(orient,[status(thm)],[t98]) ).
cnf(t135,plain,
join(r1,meet(X1,b2)) = ifeq(r1,r1,meet(b2,join(r1,X1)),join(r1,meet(X1,b2))),
inference(cp,[status(thm)],[t54,t133]) ).
cnf(t6,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t27,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t6]) ).
cnf(t6320,plain,
join(r1,meet(X1,b2)) = meet(b2,join(r1,X1)),
inference(step,[status(thm)],[t135,t27]) ).
cnf(t924,plain,
join(r1,meet(X1,b2)) = meet(b2,join(r1,X1)),
inference(orient,[status(thm)],[t6320]) ).
cnf(t930,plain,
meet(b2,join(r1,X1)) = join(r1,meet(b2,X1)),
inference(cp,[status(thm)],[t924,t28]) ).
cnf(t994,plain,
join(r1,meet(b2,X1)) = meet(b2,join(r1,X1)),
inference(orient,[status(thm)],[t930]) ).
cnf(f6,axiom,
meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
file('/export/starexec/sandbox/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(t18,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t31,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t18]) ).
cnf(t48,plain,
meet(b2,meet(a2,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t31,t47]) ).
cnf(t194,plain,
meet(b2,meet(a2,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t48]) ).
cnf(t198,plain,
meet(sFlat0,X1) = meet(b2,meet(X1,a2)),
inference(cp,[status(thm)],[t194,t28]) ).
cnf(t425,plain,
meet(b2,meet(X1,a2)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t198]) ).
cnf(t1002,plain,
meet(b2,join(r1,meet(X1,a2))) = join(r1,meet(sFlat0,X1)),
inference(cp,[status(thm)],[t994,t425]) ).
cnf(f18,negated_conjecture,
join(r1,meet(b,r2)) = a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',define_a2) ).
fof(f18_nnf,plain,
join(r1,meet(b,r2)) = a2,
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c18,plain,
join(r1,meet(b,r2)) = a2,
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(t11,plain,
join(r1,meet(b,r2)) = a2,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t6237,plain,
join(r1,meet(r2,b)) = a2,
inference(step,[status(thm)],[t11,t28]) ).
cnf(t102,plain,
join(r1,meet(r2,b)) = a2,
inference(orient,[status(thm)],[t6237]) ).
cnf(t103,plain,
r1 = meet(r1,a2),
inference(cp,[status(thm)],[t22,t102]) ).
cnf(t137,plain,
meet(r1,a2) = r1,
inference(orient,[status(thm)],[t103]) ).
cnf(t139,plain,
join(r1,meet(X1,a2)) = ifeq(r1,r1,meet(a2,join(r1,X1)),join(r1,meet(X1,a2))),
inference(cp,[status(thm)],[t54,t137]) ).
cnf(t6321,plain,
join(r1,meet(X1,a2)) = meet(a2,join(r1,X1)),
inference(step,[status(thm)],[t139,t27]) ).
cnf(t938,plain,
join(r1,meet(X1,a2)) = meet(a2,join(r1,X1)),
inference(orient,[status(thm)],[t6321]) ).
cnf(t6327,plain,
meet(b2,meet(a2,join(r1,X1))) = join(r1,meet(sFlat0,X1)),
inference(step,[status(thm)],[t1002,t938]) ).
cnf(t6328,plain,
meet(sFlat0,join(r1,X1)) = join(r1,meet(sFlat0,X1)),
inference(step,[status(thm)],[t6327,t194]) ).
cnf(t1056,plain,
join(r1,meet(sFlat0,X1)) = meet(sFlat0,join(r1,X1)),
inference(orient,[status(thm)],[t6328]) ).
cnf(t33,plain,
meet(X1,meet(X2,join(meet(X1,X2),X3))) = meet(X1,X2),
inference(cp,[status(thm)],[t31,t22]) ).
cnf(t707,plain,
meet(X1,meet(X2,join(meet(X1,X2),X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t33]) ).
cnf(f14,negated_conjecture,
meet(r2,meet(a,b)) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r2_complement_meet_a_b_2) ).
fof(f14_nnf,plain,
meet(r2,meet(a,b)) = n0,
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
meet(r2,meet(a,b)) = n0,
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(t16,plain,
meet(r2,meet(a,b)) = n0,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t6234,plain,
meet(r2,meet(b,a)) = n0,
inference(step,[status(thm)],[t16,t28]) ).
cnf(t45,plain,
meet(r2,meet(b,a)) = n0,
inference(orient,[status(thm)],[t6234]) ).
cnf(t732,plain,
meet(r2,meet(b,a)) = meet(r2,meet(meet(b,a),join(n0,X1))),
inference(cp,[status(thm)],[t707,t45]) ).
cnf(t6354,plain,
n0 = meet(r2,meet(meet(b,a),join(n0,X1))),
inference(step,[status(thm)],[t732,t45]) ).
cnf(t6355,plain,
n0 = meet(r2,meet(b,meet(a,join(n0,X1)))),
inference(step,[status(thm)],[t6354,t31]) ).
cnf(f5,axiom,
join(X,Y) = join(Y,X),
file('/export/starexec/sandbox/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(t7,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t50,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(f9,axiom,
join(X,n0) = X,
file('/export/starexec/sandbox/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(t26,plain,
join(X1,n0) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t51,plain,
join(n0,X1) = X1,
inference(cp,[status(thm)],[t50,t26]) ).
cnf(t127,plain,
join(n0,X1) = X1,
inference(orient,[status(thm)],[t51]) ).
cnf(t6356,plain,
n0 = meet(r2,meet(b,meet(a,X1))),
inference(step,[status(thm)],[t6355,t127]) ).
cnf(t1333,plain,
meet(r2,meet(b,meet(a,X1))) = n0,
inference(orient,[status(thm)],[t6356]) ).
cnf(t34,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t31,t28]) ).
cnf(t1347,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t34]) ).
cnf(t1430,plain,
n0 = meet(r2,meet(X1,meet(b,a))),
inference(cp,[status(thm)],[t1333,t1347]) ).
cnf(t1903,plain,
meet(r2,meet(X1,meet(b,a))) = n0,
inference(orient,[status(thm)],[t1430]) ).
cnf(t52,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t22,t50]) ).
cnf(t170,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t52]) ).
cnf(f7,axiom,
join(join(X,Y),Z) = join(X,join(Y,Z)),
file('/export/starexec/sandbox/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(t17,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t82,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t17]) ).
cnf(t175,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t170,t82]) ).
cnf(t1134,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t175]) ).
cnf(f3,axiom,
join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox/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(t8,plain,
join(X1,meet(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t25,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t1139,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(cp,[status(thm)],[t1134,t25]) ).
cnf(t6709,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,X1))),
inference(step,[status(thm)],[t1139,t31]) ).
cnf(t6001,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t6709]) ).
cnf(t37,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t31,t22]) ).
cnf(t2076,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t37]) ).
cnf(t58,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)],[t54,t22]) ).
cnf(t6679,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X3),join(X1,X2)),
inference(step,[status(thm)],[t58,t27]) ).
cnf(t5216,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X3),join(X1,X2)),
inference(orient,[status(thm)],[t6679]) ).
cnf(f16,negated_conjecture,
meet(r1,join(a,b)) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r1_complement_join_a_b_2) ).
fof(f16_nnf,plain,
meet(r1,join(a,b)) = n0,
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
meet(r1,join(a,b)) = n0,
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(t15,plain,
meet(r1,join(a,b)) = n0,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t43,plain,
meet(r1,join(a,b)) = n0,
inference(orient,[status(thm)],[t15]) ).
cnf(t53,plain,
meet(r1,join(a,b)) = n0,
inference(rw,[status(thm)],[t43]) ).
cnf(t6244,plain,
meet(r1,join(b,a)) = n0,
inference(step,[status(thm)],[t53,t50]) ).
cnf(t180,plain,
meet(r1,join(b,a)) = n0,
inference(orient,[status(thm)],[t6244]) ).
cnf(t5258,plain,
meet(join(b,a),join(b,r1)) = join(b,n0),
inference(cp,[status(thm)],[t5216,t180]) ).
cnf(t6680,plain,
meet(join(b,r1),join(b,a)) = join(b,n0),
inference(step,[status(thm)],[t5258,t28]) ).
cnf(t6681,plain,
meet(join(r1,b),join(b,a)) = join(b,n0),
inference(step,[status(thm)],[t6680,t50]) ).
cnf(t30,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t25,t28]) ).
cnf(t145,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t30]) ).
cnf(t151,plain,
a2 = join(a2,sFlat0),
inference(cp,[status(thm)],[t145,t47]) ).
cnf(t6243,plain,
a2 = join(sFlat0,a2),
inference(step,[status(thm)],[t151,t50]) ).
cnf(t161,plain,
join(sFlat0,a2) = a2,
inference(orient,[status(thm)],[t6243]) ).
cnf(t163,plain,
join(sFlat0,join(a2,X1)) = join(a2,X1),
inference(cp,[status(thm)],[t82,t161]) ).
cnf(t381,plain,
join(sFlat0,join(a2,X1)) = join(a2,X1),
inference(orient,[status(thm)],[t163]) ).
cnf(t383,plain,
join(a2,X1) = join(sFlat0,join(X1,a2)),
inference(cp,[status(thm)],[t381,t50]) ).
cnf(t612,plain,
join(sFlat0,join(X1,a2)) = join(a2,X1),
inference(orient,[status(thm)],[t383]) ).
cnf(t104,plain,
join(r1,join(meet(r2,b),X1)) = join(a2,X1),
inference(cp,[status(thm)],[t82,t102]) ).
cnf(t2656,plain,
join(r1,join(meet(r2,b),X1)) = join(a2,X1),
inference(orient,[status(thm)],[t104]) ).
cnf(t174,plain,
meet(r2,b) = meet(meet(r2,b),a2),
inference(cp,[status(thm)],[t170,t102]) ).
cnf(t6276,plain,
meet(r2,b) = meet(r2,meet(b,a2)),
inference(step,[status(thm)],[t174,t31]) ).
cnf(t419,plain,
meet(r2,meet(b,a2)) = meet(r2,b),
inference(orient,[status(thm)],[t6276]) ).
cnf(t421,plain,
meet(b,a2) = join(meet(b,a2),meet(r2,b)),
inference(cp,[status(thm)],[t145,t419]) ).
cnf(t6651,plain,
meet(b,a2) = join(meet(r2,b),meet(b,a2)),
inference(step,[status(thm)],[t421,t50]) ).
cnf(t4026,plain,
join(meet(r2,b),meet(b,a2)) = meet(b,a2),
inference(orient,[status(thm)],[t6651]) ).
cnf(t4033,plain,
join(a2,meet(b,a2)) = join(r1,meet(b,a2)),
inference(cp,[status(thm)],[t2656,t4026]) ).
cnf(t6652,plain,
a2 = join(r1,meet(b,a2)),
inference(step,[status(thm)],[t4033,t145]) ).
cnf(t6653,plain,
a2 = meet(a2,join(r1,b)),
inference(step,[status(thm)],[t6652,t938]) ).
cnf(t4037,plain,
meet(a2,join(r1,b)) = a2,
inference(orient,[status(thm)],[t6653]) ).
cnf(t4043,plain,
join(r1,b) = join(join(r1,b),a2),
inference(cp,[status(thm)],[t145,t4037]) ).
cnf(t6654,plain,
join(r1,b) = join(r1,join(b,a2)),
inference(step,[status(thm)],[t4043,t82]) ).
cnf(t150,plain,
a2 = join(a2,r1),
inference(cp,[status(thm)],[t145,t137]) ).
cnf(t6242,plain,
a2 = join(r1,a2),
inference(step,[status(thm)],[t150,t50]) ).
cnf(t158,plain,
join(r1,a2) = a2,
inference(orient,[status(thm)],[t6242]) ).
cnf(t159,plain,
join(r1,join(a2,X1)) = join(a2,X1),
inference(cp,[status(thm)],[t82,t158]) ).
cnf(t376,plain,
join(r1,join(a2,X1)) = join(a2,X1),
inference(orient,[status(thm)],[t159]) ).
cnf(t378,plain,
join(a2,X1) = join(r1,join(X1,a2)),
inference(cp,[status(thm)],[t376,t50]) ).
cnf(t601,plain,
join(r1,join(X1,a2)) = join(a2,X1),
inference(orient,[status(thm)],[t378]) ).
cnf(t6655,plain,
join(r1,b) = join(a2,b),
inference(step,[status(thm)],[t6654,t601]) ).
cnf(t6656,plain,
join(r1,b) = join(b,a2),
inference(step,[status(thm)],[t6655,t50]) ).
cnf(t4053,plain,
join(b,a2) = join(r1,b),
inference(orient,[status(thm)],[t6656]) ).
cnf(t4056,plain,
join(a2,b) = join(sFlat0,join(r1,b)),
inference(cp,[status(thm)],[t612,t4053]) ).
cnf(t6657,plain,
join(b,a2) = join(sFlat0,join(r1,b)),
inference(step,[status(thm)],[t4056,t50]) ).
cnf(t6658,plain,
join(r1,b) = join(sFlat0,join(r1,b)),
inference(step,[status(thm)],[t6657,t4053]) ).
cnf(t134,plain,
meet(r1,meet(b2,X1)) = meet(r1,X1),
inference(cp,[status(thm)],[t31,t133]) ).
cnf(t264,plain,
meet(r1,meet(b2,X1)) = meet(r1,X1),
inference(orient,[status(thm)],[t134]) ).
cnf(t265,plain,
meet(r1,a2) = meet(r1,sFlat0),
inference(cp,[status(thm)],[t264,t47]) ).
cnf(t6256,plain,
r1 = meet(r1,sFlat0),
inference(step,[status(thm)],[t265,t137]) ).
cnf(t6257,plain,
r1 = meet(sFlat0,r1),
inference(step,[status(thm)],[t6256,t28]) ).
cnf(t273,plain,
meet(sFlat0,r1) = r1,
inference(orient,[status(thm)],[t6257]) ).
cnf(t276,plain,
sFlat0 = join(sFlat0,r1),
inference(cp,[status(thm)],[t25,t273]) ).
cnf(t279,plain,
join(sFlat0,r1) = sFlat0,
inference(orient,[status(thm)],[t276]) ).
cnf(t281,plain,
join(sFlat0,join(r1,X1)) = join(sFlat0,X1),
inference(cp,[status(thm)],[t82,t279]) ).
cnf(t539,plain,
join(sFlat0,join(r1,X1)) = join(sFlat0,X1),
inference(orient,[status(thm)],[t281]) ).
cnf(t6659,plain,
join(r1,b) = join(sFlat0,b),
inference(step,[status(thm)],[t6658,t539]) ).
cnf(t4066,plain,
join(r1,b) = join(sFlat0,b),
inference(orient,[status(thm)],[t6659]) ).
cnf(t6682,plain,
meet(join(sFlat0,b),join(b,a)) = join(b,n0),
inference(step,[status(thm)],[t6681,t4066]) ).
cnf(t6683,plain,
meet(join(sFlat0,b),join(b,a)) = b,
inference(step,[status(thm)],[t6682,t26]) ).
cnf(t5407,plain,
meet(join(sFlat0,b),join(b,a)) = b,
inference(orient,[status(thm)],[t6683]) ).
cnf(t5420,plain,
meet(sFlat0,join(b,a)) = meet(sFlat0,b),
inference(cp,[status(thm)],[t2076,t5407]) ).
cnf(t5426,plain,
meet(sFlat0,join(b,a)) = meet(sFlat0,b),
inference(orient,[status(thm)],[t5420]) ).
cnf(t6006,plain,
meet(a,sFlat0) = meet(a,meet(sFlat0,b)),
inference(cp,[status(thm)],[t6001,t5426]) ).
cnf(t6711,plain,
meet(sFlat0,a) = meet(a,meet(sFlat0,b)),
inference(step,[status(thm)],[t6006,t28]) ).
cnf(t38,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t31,t28]) ).
cnf(t6604,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t38,t31]) ).
cnf(t2710,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t6604]) ).
cnf(t6712,plain,
meet(sFlat0,a) = meet(sFlat0,meet(a,b)),
inference(step,[status(thm)],[t6711,t2710]) ).
cnf(t6713,plain,
meet(sFlat0,a) = meet(sFlat0,meet(b,a)),
inference(step,[status(thm)],[t6712,t28]) ).
cnf(t6179,plain,
meet(sFlat0,meet(b,a)) = meet(sFlat0,a),
inference(orient,[status(thm)],[t6713]) ).
cnf(t6195,plain,
n0 = meet(r2,meet(sFlat0,a)),
inference(cp,[status(thm)],[t1903,t6179]) ).
cnf(t6714,plain,
n0 = meet(sFlat0,meet(r2,a)),
inference(step,[status(thm)],[t6195,t2710]) ).
cnf(t6202,plain,
meet(sFlat0,meet(r2,a)) = n0,
inference(orient,[status(thm)],[t6714]) ).
cnf(t6204,plain,
meet(sFlat0,join(r1,meet(r2,a))) = join(r1,n0),
inference(cp,[status(thm)],[t1056,t6202]) ).
cnf(t6715,plain,
meet(sFlat0,b2) = join(r1,n0),
inference(step,[status(thm)],[t6204,t97]) ).
cnf(t49,plain,
b2 = join(b2,sFlat0),
inference(cp,[status(thm)],[t25,t47]) ).
cnf(t6240,plain,
b2 = join(sFlat0,b2),
inference(step,[status(thm)],[t49,t50]) ).
cnf(t123,plain,
join(sFlat0,b2) = b2,
inference(orient,[status(thm)],[t6240]) ).
cnf(t124,plain,
sFlat0 = meet(sFlat0,b2),
inference(cp,[status(thm)],[t22,t123]) ).
cnf(t141,plain,
meet(sFlat0,b2) = sFlat0,
inference(orient,[status(thm)],[t124]) ).
cnf(t6716,plain,
sFlat0 = join(r1,n0),
inference(step,[status(thm)],[t6715,t141]) ).
cnf(t6717,plain,
sFlat0 = r1,
inference(step,[status(thm)],[t6716,t26]) ).
cnf(t6214,plain,
r1 = sFlat0,
inference(orient,[status(thm)],[t6717]) ).
cnf(f19,negated_conjecture,
meet(a2,b2) != r1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_SAMs_lemma) ).
fof(f19_nnf,plain,
meet(a2,b2) != r1,
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
meet(a2,b2) != r1,
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
meet(a2,b2) != r1,
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(goal_0,negated_conjecture,
meet(a2,b2) != r1,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(g0_0,plain,
meet(b2,a2) != r1,
inference(rw,[status(thm)],[goal_0,t28]) ).
cnf(g0_1,plain,
sFlat0 != r1,
inference(rw,[status(thm)],[g0_0,t47]) ).
cnf(g0_2,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_1,t6214]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT005-4 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 20:02:08 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.83/1.63 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.83/1.63 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------