%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT154-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.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:36 PM UTC 2026
% Result : Unsatisfiable 31.93s 4.79s
% Output : CNFRefutation 31.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 17
% Syntax : Number of clauses : 243 ( 243 unt; 0 nHn; 158 RR)
% Number of literals : 243 ( 242 equ; 22 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 161 ( 33 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t58,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t12,axiom,
sFlat3 = join(a,b),
introduced(definition) ).
cnf(t4415,plain,
sFlat3 = join(b,a),
inference(step,[status(thm)],[t12,t58]) ).
cnf(t75,plain,
join(b,a) = sFlat3,
inference(orient,[status(thm)],[t4415]) ).
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t13,axiom,
sFlat4 = meet(c,join(a,b)),
introduced(definition) ).
cnf(t54,plain,
meet(c,join(a,b)) = sFlat4,
inference(orient,[status(thm)],[t13]) ).
cnf(t59,plain,
meet(c,join(a,b)) = sFlat4,
inference(rw,[status(thm)],[t54]) ).
cnf(t4429,plain,
meet(c,join(b,a)) = sFlat4,
inference(step,[status(thm)],[t59,t58]) ).
cnf(t4430,plain,
meet(c,sFlat3) = sFlat4,
inference(step,[status(thm)],[t4429,t75]) ).
cnf(t4431,plain,
meet(sFlat3,c) = sFlat4,
inference(step,[status(thm)],[t4430,t20]) ).
cnf(t130,plain,
meet(sFlat3,c) = sFlat4,
inference(orient,[status(thm)],[t4431]) ).
cnf(t9,axiom,
sFlat0 = meet(a,c),
introduced(definition) ).
cnf(t4408,plain,
sFlat0 = meet(c,a),
inference(step,[status(thm)],[t9,t20]) ).
cnf(t49,plain,
meet(c,a) = sFlat0,
inference(orient,[status(thm)],[t4408]) ).
cnf(t10,axiom,
sFlat1 = join(b,meet(a,c)),
introduced(definition) ).
cnf(t4417,plain,
sFlat1 = join(b,meet(c,a)),
inference(step,[status(thm)],[t10,t20]) ).
cnf(t4418,plain,
sFlat1 = join(b,sFlat0),
inference(step,[status(thm)],[t4417,t49]) ).
cnf(t4419,plain,
sFlat1 = join(sFlat0,b),
inference(step,[status(thm)],[t4418,t58]) ).
cnf(t79,plain,
join(sFlat0,b) = sFlat1,
inference(orient,[status(thm)],[t4419]) ).
cnf(t11,axiom,
sFlat2 = meet(a,join(b,meet(a,c))),
introduced(definition) ).
cnf(t4406,plain,
sFlat2 = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t11,t20]) ).
cnf(t44,plain,
meet(a,join(b,meet(c,a))) = sFlat2,
inference(orient,[status(thm)],[t4406]) ).
cnf(t4409,plain,
meet(a,join(b,sFlat0)) = sFlat2,
inference(step,[status(thm)],[t44,t49]) ).
cnf(t53,plain,
meet(a,join(b,sFlat0)) = sFlat2,
inference(rw,[status(thm)],[t4409]) ).
cnf(t4425,plain,
meet(a,join(sFlat0,b)) = sFlat2,
inference(step,[status(thm)],[t53,t58]) ).
cnf(t4426,plain,
meet(a,sFlat1) = sFlat2,
inference(step,[status(thm)],[t4425,t79]) ).
cnf(t4427,plain,
meet(sFlat1,a) = sFlat2,
inference(step,[status(thm)],[t4426,t20]) ).
cnf(t119,plain,
meet(sFlat1,a) = sFlat2,
inference(orient,[status(thm)],[t4427]) ).
cnf(t14,axiom,
sFlat5 = join(meet(a,join(b,meet(a,c))),meet(c,join(a,b))),
introduced(definition) ).
cnf(t4410,plain,
sFlat5 = join(meet(c,join(a,b)),meet(a,join(b,meet(a,c)))),
inference(step,[status(thm)],[t14,t58]) ).
cnf(t4411,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(b,meet(a,c)))),
inference(step,[status(thm)],[t4410,t58]) ).
cnf(t4412,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(b,meet(c,a)))),
inference(step,[status(thm)],[t4411,t20]) ).
cnf(t4413,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(b,sFlat0))),
inference(step,[status(thm)],[t4412,t49]) ).
cnf(t4414,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(sFlat0,b))),
inference(step,[status(thm)],[t4413,t58]) ).
cnf(t71,plain,
join(meet(c,join(b,a)),meet(a,join(sFlat0,b))) = sFlat5,
inference(orient,[status(thm)],[t4414]) ).
cnf(t4416,plain,
join(meet(c,sFlat3),meet(a,join(sFlat0,b))) = sFlat5,
inference(step,[status(thm)],[t71,t75]) ).
cnf(t78,plain,
join(meet(c,sFlat3),meet(a,join(sFlat0,b))) = sFlat5,
inference(rw,[status(thm)],[t4416]) ).
cnf(t4653,plain,
join(meet(sFlat3,c),meet(a,join(sFlat0,b))) = sFlat5,
inference(step,[status(thm)],[t78,t20]) ).
cnf(t4654,plain,
join(sFlat4,meet(a,join(sFlat0,b))) = sFlat5,
inference(step,[status(thm)],[t4653,t130]) ).
cnf(t4655,plain,
join(sFlat4,meet(a,sFlat1)) = sFlat5,
inference(step,[status(thm)],[t4654,t79]) ).
cnf(t4656,plain,
join(sFlat4,meet(sFlat1,a)) = sFlat5,
inference(step,[status(thm)],[t4655,t20]) ).
cnf(t4657,plain,
join(sFlat4,sFlat2) = sFlat5,
inference(step,[status(thm)],[t4656,t119]) ).
cnf(t4658,plain,
join(sFlat2,sFlat4) = sFlat5,
inference(step,[status(thm)],[t4657,t58]) ).
cnf(t3974,plain,
join(sFlat2,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t4658]) ).
cnf(t15,axiom,
sFlat6 = meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))),
introduced(definition) ).
cnf(t4405,plain,
sFlat6 = meet(a,join(meet(a,join(b,meet(c,a))),meet(c,join(a,b)))),
inference(step,[status(thm)],[t15,t20]) ).
cnf(t40,plain,
meet(a,join(meet(a,join(b,meet(c,a))),meet(c,join(a,b)))) = sFlat6,
inference(orient,[status(thm)],[t4405]) ).
cnf(t4407,plain,
meet(a,join(sFlat2,meet(c,join(a,b)))) = sFlat6,
inference(step,[status(thm)],[t40,t44]) ).
cnf(t48,plain,
meet(a,join(sFlat2,meet(c,join(a,b)))) = sFlat6,
inference(rw,[status(thm)],[t4407]) ).
cnf(t4594,plain,
meet(a,join(sFlat2,meet(c,join(b,a)))) = sFlat6,
inference(step,[status(thm)],[t48,t58]) ).
cnf(t4595,plain,
meet(a,join(sFlat2,meet(c,sFlat3))) = sFlat6,
inference(step,[status(thm)],[t4594,t75]) ).
cnf(t4596,plain,
meet(a,join(sFlat2,meet(sFlat3,c))) = sFlat6,
inference(step,[status(thm)],[t4595,t20]) ).
cnf(t4597,plain,
meet(a,join(sFlat2,sFlat4)) = sFlat6,
inference(step,[status(thm)],[t4596,t130]) ).
cnf(t3551,plain,
meet(a,join(sFlat2,sFlat4)) = sFlat6,
inference(orient,[status(thm)],[t4597]) ).
cnf(t4662,plain,
meet(a,sFlat5) = sFlat6,
inference(step,[status(thm)],[t3551,t3974]) ).
cnf(t3989,plain,
meet(a,sFlat5) = sFlat6,
inference(rw,[status(thm)],[t4662]) ).
cnf(t4665,plain,
meet(sFlat5,a) = sFlat6,
inference(step,[status(thm)],[t3989,t20]) ).
cnf(t4011,plain,
meet(sFlat5,a) = sFlat6,
inference(orient,[status(thm)],[t4665]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t5,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t42,plain,
a = join(a,sFlat6),
inference(cp,[status(thm)],[t19,t40]) ).
cnf(t4420,plain,
a = join(sFlat6,a),
inference(step,[status(thm)],[t42,t58]) ).
cnf(t82,plain,
join(sFlat6,a) = a,
inference(orient,[status(thm)],[t4420]) ).
cnf(t83,plain,
sFlat6 = meet(sFlat6,a),
inference(cp,[status(thm)],[t17,t82]) ).
cnf(t101,plain,
meet(sFlat6,a) = sFlat6,
inference(orient,[status(thm)],[t83]) ).
cnf(t102,plain,
meet(sFlat6,meet(a,X1)) = meet(sFlat6,X1),
inference(cp,[status(thm)],[t21,t101]) ).
cnf(t454,plain,
meet(sFlat6,meet(a,X1)) = meet(sFlat6,X1),
inference(orient,[status(thm)],[t102]) ).
cnf(t8,axiom,
meet(X1,join(X2,meet(X3,join(X2,join(X4,meet(X1,X3)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
meet(X1,join(X2,meet(X3,join(X2,join(X4,meet(X1,X3)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t8]) ).
cnf(t33,plain,
meet(X1,join(X2,meet(X3,join(X1,X1)))) = meet(X1,join(X2,meet(X3,join(X2,X1)))),
inference(cp,[status(thm)],[t29,t19]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t4624,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,meet(X3,join(X2,X1)))),
inference(step,[status(thm)],[t33,t18]) ).
cnf(t3616,plain,
meet(X1,join(X2,meet(X3,join(X2,X1)))) = meet(X1,join(X2,meet(X3,X1))),
inference(orient,[status(thm)],[t4624]) ).
cnf(t3677,plain,
meet(a,join(b,meet(X1,a))) = meet(a,join(b,meet(X1,sFlat3))),
inference(cp,[status(thm)],[t3616,t75]) ).
cnf(t3813,plain,
meet(a,join(b,meet(X1,a))) = meet(a,join(b,meet(X1,sFlat3))),
inference(orient,[status(thm)],[t3677]) ).
cnf(t3816,plain,
meet(a,join(b,meet(c,sFlat3))) = meet(a,join(b,sFlat0)),
inference(cp,[status(thm)],[t3813,t49]) ).
cnf(t4700,plain,
meet(a,join(b,meet(sFlat3,c))) = meet(a,join(b,sFlat0)),
inference(step,[status(thm)],[t3816,t20]) ).
cnf(t4701,plain,
meet(a,join(b,sFlat4)) = meet(a,join(b,sFlat0)),
inference(step,[status(thm)],[t4700,t130]) ).
cnf(t4702,plain,
meet(a,join(sFlat4,b)) = meet(a,join(b,sFlat0)),
inference(step,[status(thm)],[t4701,t58]) ).
cnf(t24,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t21,t20]) ).
cnf(t213,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t24]) ).
cnf(t221,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t19,t213]) ).
cnf(t574,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t221]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t16,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t25,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t21,t16]) ).
cnf(t115,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t25]) ).
cnf(t576,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t574,t115]) ).
cnf(t641,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t576]) ).
cnf(t26,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t21,t17]) ).
cnf(t474,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t26]) ).
cnf(t477,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t474,t20]) ).
cnf(t935,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t477]) ).
cnf(t132,plain,
meet(sFlat3,meet(c,X1)) = meet(sFlat4,X1),
inference(cp,[status(thm)],[t21,t130]) ).
cnf(t299,plain,
meet(sFlat3,meet(c,X1)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t132]) ).
cnf(t50,plain,
meet(c,meet(a,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t21,t49]) ).
cnf(t148,plain,
meet(c,meet(a,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t50]) ).
cnf(t301,plain,
meet(sFlat4,meet(a,X1)) = meet(sFlat3,meet(sFlat0,X1)),
inference(cp,[status(thm)],[t299,t148]) ).
cnf(t27,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t21,t20]) ).
cnf(t4440,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t27,t21]) ).
cnf(t223,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t4440]) ).
cnf(t4473,plain,
meet(sFlat4,meet(a,X1)) = meet(sFlat0,meet(sFlat3,X1)),
inference(step,[status(thm)],[t301,t223]) ).
cnf(t531,plain,
meet(sFlat4,meet(a,X1)) = meet(sFlat0,meet(sFlat3,X1)),
inference(orient,[status(thm)],[t4473]) ).
cnf(t936,plain,
meet(sFlat4,a) = meet(sFlat0,meet(sFlat3,join(sFlat4,X1))),
inference(cp,[status(thm)],[t935,t531]) ).
cnf(t300,plain,
meet(sFlat4,a) = meet(sFlat3,sFlat0),
inference(cp,[status(thm)],[t299,t49]) ).
cnf(t4443,plain,
meet(sFlat4,a) = meet(sFlat0,sFlat3),
inference(step,[status(thm)],[t300,t20]) ).
cnf(t307,plain,
meet(sFlat4,a) = meet(sFlat0,sFlat3),
inference(orient,[status(thm)],[t4443]) ).
cnf(t151,plain,
meet(sFlat0,join(a,X1)) = meet(c,a),
inference(cp,[status(thm)],[t148,t17]) ).
cnf(t4437,plain,
meet(sFlat0,join(a,X1)) = sFlat0,
inference(step,[status(thm)],[t151,t49]) ).
cnf(t186,plain,
meet(sFlat0,join(a,X1)) = sFlat0,
inference(orient,[status(thm)],[t4437]) ).
cnf(t187,plain,
sFlat0 = meet(sFlat0,join(X1,a)),
inference(cp,[status(thm)],[t186,t58]) ).
cnf(t365,plain,
meet(sFlat0,join(X1,a)) = sFlat0,
inference(orient,[status(thm)],[t187]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t60,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t77,plain,
join(b,join(a,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t60,t75]) ).
cnf(t160,plain,
join(b,join(a,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t77]) ).
cnf(t161,plain,
join(sFlat3,a) = join(b,a),
inference(cp,[status(thm)],[t160,t18]) ).
cnf(t4435,plain,
join(sFlat3,a) = sFlat3,
inference(step,[status(thm)],[t161,t75]) ).
cnf(t168,plain,
join(sFlat3,a) = sFlat3,
inference(orient,[status(thm)],[t4435]) ).
cnf(t366,plain,
sFlat0 = meet(sFlat0,sFlat3),
inference(cp,[status(thm)],[t365,t168]) ).
cnf(t371,plain,
meet(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t366]) ).
cnf(t4460,plain,
meet(sFlat4,a) = sFlat0,
inference(step,[status(thm)],[t307,t371]) ).
cnf(t372,plain,
meet(sFlat4,a) = sFlat0,
inference(orient,[status(thm)],[t4460]) ).
cnf(t4534,plain,
sFlat0 = meet(sFlat0,meet(sFlat3,join(sFlat4,X1))),
inference(step,[status(thm)],[t936,t372]) ).
cnf(t1817,plain,
meet(sFlat0,meet(sFlat3,join(sFlat4,X1))) = sFlat0,
inference(orient,[status(thm)],[t4534]) ).
cnf(t63,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t60,t58]) ).
cnf(t254,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t63]) ).
cnf(t259,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t17,t254]) ).
cnf(t710,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t259]) ).
cnf(t64,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t60,t18]) ).
cnf(t141,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t64]) ).
cnf(t712,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t710,t141]) ).
cnf(t788,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t712]) ).
cnf(t133,plain,
sFlat3 = join(sFlat3,sFlat4),
inference(cp,[status(thm)],[t19,t130]) ).
cnf(t139,plain,
join(sFlat3,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t133]) ).
cnf(t140,plain,
join(sFlat3,join(sFlat4,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t60,t139]) ).
cnf(t490,plain,
join(sFlat3,join(sFlat4,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t140]) ).
cnf(t800,plain,
join(sFlat4,X1) = meet(join(sFlat4,X1),join(sFlat3,X1)),
inference(cp,[status(thm)],[t788,t490]) ).
cnf(t4562,plain,
join(sFlat4,X1) = meet(join(sFlat3,X1),join(sFlat4,X1)),
inference(step,[status(thm)],[t800,t20]) ).
cnf(t2469,plain,
meet(join(sFlat3,X1),join(sFlat4,X1)) = join(sFlat4,X1),
inference(orient,[status(thm)],[t4562]) ).
cnf(t76,plain,
b = meet(b,sFlat3),
inference(cp,[status(thm)],[t17,t75]) ).
cnf(t4424,plain,
b = meet(sFlat3,b),
inference(step,[status(thm)],[t76,t20]) ).
cnf(t94,plain,
meet(sFlat3,b) = b,
inference(orient,[status(thm)],[t4424]) ).
cnf(t96,plain,
sFlat3 = join(sFlat3,b),
inference(cp,[status(thm)],[t19,t94]) ).
cnf(t113,plain,
join(sFlat3,b) = sFlat3,
inference(orient,[status(thm)],[t96]) ).
cnf(t2486,plain,
join(sFlat4,b) = meet(sFlat3,join(sFlat4,b)),
inference(cp,[status(thm)],[t2469,t113]) ).
cnf(t2531,plain,
meet(sFlat3,join(sFlat4,b)) = join(sFlat4,b),
inference(orient,[status(thm)],[t2486]) ).
cnf(t2532,plain,
sFlat0 = meet(sFlat0,join(sFlat4,b)),
inference(cp,[status(thm)],[t1817,t2531]) ).
cnf(t2552,plain,
meet(sFlat0,join(sFlat4,b)) = sFlat0,
inference(orient,[status(thm)],[t2532]) ).
cnf(t2557,plain,
join(sFlat4,b) = join(join(sFlat4,b),sFlat0),
inference(cp,[status(thm)],[t641,t2552]) ).
cnf(t4684,plain,
join(sFlat4,b) = join(sFlat4,join(b,sFlat0)),
inference(step,[status(thm)],[t2557,t60]) ).
cnf(t4685,plain,
join(sFlat4,b) = join(sFlat0,join(sFlat4,b)),
inference(step,[status(thm)],[t4684,t254]) ).
cnf(t81,plain,
join(sFlat0,join(b,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t60,t79]) ).
cnf(t170,plain,
join(sFlat0,join(b,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t81]) ).
cnf(t176,plain,
join(sFlat1,X1) = join(sFlat0,join(X1,b)),
inference(cp,[status(thm)],[t170,t58]) ).
cnf(t357,plain,
join(sFlat0,join(X1,b)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t176]) ).
cnf(t4686,plain,
join(sFlat4,b) = join(sFlat1,sFlat4),
inference(step,[status(thm)],[t4685,t357]) ).
cnf(t4303,plain,
join(sFlat4,b) = join(sFlat1,sFlat4),
inference(orient,[status(thm)],[t4686]) ).
cnf(t4703,plain,
meet(a,join(sFlat1,sFlat4)) = meet(a,join(b,sFlat0)),
inference(step,[status(thm)],[t4702,t4303]) ).
cnf(t4704,plain,
meet(a,join(sFlat1,sFlat4)) = meet(a,join(sFlat0,b)),
inference(step,[status(thm)],[t4703,t58]) ).
cnf(t4705,plain,
meet(a,join(sFlat1,sFlat4)) = meet(a,sFlat1),
inference(step,[status(thm)],[t4704,t79]) ).
cnf(t4706,plain,
meet(a,join(sFlat1,sFlat4)) = meet(sFlat1,a),
inference(step,[status(thm)],[t4705,t20]) ).
cnf(t4707,plain,
meet(a,join(sFlat1,sFlat4)) = sFlat2,
inference(step,[status(thm)],[t4706,t119]) ).
cnf(t4377,plain,
meet(a,join(sFlat1,sFlat4)) = sFlat2,
inference(orient,[status(thm)],[t4707]) ).
cnf(t4379,plain,
meet(sFlat6,join(sFlat1,sFlat4)) = meet(sFlat6,sFlat2),
inference(cp,[status(thm)],[t454,t4377]) ).
cnf(t122,plain,
sFlat1 = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t19,t119]) ).
cnf(t128,plain,
join(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t122]) ).
cnf(t129,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t60,t128]) ).
cnf(t486,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t129]) ).
cnf(t3554,plain,
join(sFlat2,sFlat4) = join(join(sFlat2,sFlat4),sFlat6),
inference(cp,[status(thm)],[t641,t3551]) ).
cnf(t4629,plain,
join(sFlat2,sFlat4) = join(sFlat2,join(sFlat4,sFlat6)),
inference(step,[status(thm)],[t3554,t60]) ).
cnf(t3776,plain,
join(sFlat2,join(sFlat4,sFlat6)) = join(sFlat2,sFlat4),
inference(orient,[status(thm)],[t4629]) ).
cnf(t3779,plain,
join(sFlat1,join(sFlat4,sFlat6)) = join(sFlat1,join(sFlat2,sFlat4)),
inference(cp,[status(thm)],[t486,t3776]) ).
cnf(t4630,plain,
join(sFlat1,join(sFlat4,sFlat6)) = join(sFlat1,sFlat4),
inference(step,[status(thm)],[t3779,t486]) ).
cnf(t3784,plain,
join(sFlat1,join(sFlat4,sFlat6)) = join(sFlat1,sFlat4),
inference(orient,[status(thm)],[t4630]) ).
cnf(t3788,plain,
sFlat6 = meet(sFlat6,join(sFlat1,sFlat4)),
inference(cp,[status(thm)],[t710,t3784]) ).
cnf(t3792,plain,
meet(sFlat6,join(sFlat1,sFlat4)) = sFlat6,
inference(orient,[status(thm)],[t3788]) ).
cnf(t4708,plain,
sFlat6 = meet(sFlat6,sFlat2),
inference(step,[status(thm)],[t4379,t3792]) ).
cnf(t4709,plain,
sFlat6 = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t4708,t20]) ).
cnf(t721,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(cp,[status(thm)],[t710,t19]) ).
cnf(t4505,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,X1))),
inference(step,[status(thm)],[t721,t21]) ).
cnf(t1175,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t4505]) ).
cnf(t121,plain,
meet(sFlat1,meet(a,X1)) = meet(sFlat2,X1),
inference(cp,[status(thm)],[t21,t119]) ).
cnf(t293,plain,
meet(sFlat1,meet(a,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t121]) ).
cnf(t67,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(cp,[status(thm)],[t17,t60]) ).
cnf(t2791,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t67]) ).
cnf(t46,plain,
a = join(a,sFlat2),
inference(cp,[status(thm)],[t19,t44]) ).
cnf(t4421,plain,
a = join(sFlat2,a),
inference(step,[status(thm)],[t46,t58]) ).
cnf(t85,plain,
join(sFlat2,a) = a,
inference(orient,[status(thm)],[t4421]) ).
cnf(t2832,plain,
join(X1,sFlat2) = meet(join(X1,sFlat2),join(X1,a)),
inference(cp,[status(thm)],[t2791,t85]) ).
cnf(t2874,plain,
meet(join(X1,sFlat2),join(X1,a)) = join(X1,sFlat2),
inference(orient,[status(thm)],[t2832]) ).
cnf(t2876,plain,
join(sFlat6,sFlat2) = meet(join(sFlat6,sFlat2),a),
inference(cp,[status(thm)],[t2874,t82]) ).
cnf(t4569,plain,
join(sFlat2,sFlat6) = meet(join(sFlat6,sFlat2),a),
inference(step,[status(thm)],[t2876,t58]) ).
cnf(t4570,plain,
join(sFlat2,sFlat6) = meet(a,join(sFlat6,sFlat2)),
inference(step,[status(thm)],[t4569,t20]) ).
cnf(t4571,plain,
join(sFlat2,sFlat6) = meet(a,join(sFlat2,sFlat6)),
inference(step,[status(thm)],[t4570,t58]) ).
cnf(t2884,plain,
meet(a,join(sFlat2,sFlat6)) = join(sFlat2,sFlat6),
inference(orient,[status(thm)],[t4571]) ).
cnf(t2888,plain,
meet(sFlat2,join(sFlat2,sFlat6)) = meet(sFlat1,join(sFlat2,sFlat6)),
inference(cp,[status(thm)],[t293,t2884]) ).
cnf(t4575,plain,
sFlat2 = meet(sFlat1,join(sFlat2,sFlat6)),
inference(step,[status(thm)],[t2888,t17]) ).
cnf(t2907,plain,
meet(sFlat1,join(sFlat2,sFlat6)) = sFlat2,
inference(orient,[status(thm)],[t4575]) ).
cnf(t2910,plain,
meet(sFlat6,sFlat1) = meet(sFlat6,sFlat2),
inference(cp,[status(thm)],[t1175,t2907]) ).
cnf(t4576,plain,
meet(sFlat1,sFlat6) = meet(sFlat6,sFlat2),
inference(step,[status(thm)],[t2910,t20]) ).
cnf(t4577,plain,
meet(sFlat1,sFlat6) = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t4576,t20]) ).
cnf(t2915,plain,
meet(sFlat2,sFlat6) = meet(sFlat1,sFlat6),
inference(orient,[status(thm)],[t4577]) ).
cnf(t3559,plain,
meet(sFlat2,join(sFlat2,sFlat4)) = meet(sFlat1,sFlat6),
inference(cp,[status(thm)],[t293,t3551]) ).
cnf(t4606,plain,
sFlat2 = meet(sFlat1,sFlat6),
inference(step,[status(thm)],[t3559,t17]) ).
cnf(t3587,plain,
meet(sFlat1,sFlat6) = sFlat2,
inference(orient,[status(thm)],[t4606]) ).
cnf(t4607,plain,
meet(sFlat2,sFlat6) = sFlat2,
inference(step,[status(thm)],[t2915,t3587]) ).
cnf(t3588,plain,
meet(sFlat2,sFlat6) = sFlat2,
inference(orient,[status(thm)],[t4607]) ).
cnf(t4710,plain,
sFlat6 = sFlat2,
inference(step,[status(thm)],[t4709,t3588]) ).
cnf(t4388,plain,
sFlat6 = sFlat2,
inference(orient,[status(thm)],[t4710]) ).
cnf(t4711,plain,
meet(sFlat5,a) = sFlat2,
inference(step,[status(thm)],[t4011,t4388]) ).
cnf(t4389,plain,
meet(sFlat5,a) = sFlat2,
inference(orient,[status(thm)],[t4711]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))) != meet(a,join(b,meet(a,c))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(meet(c,join(a,b)),meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[goal_0,t58]) ).
cnf(g0_1,plain,
meet(a,join(meet(c,join(b,a)),meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_0,t58]) ).
cnf(g0_2,plain,
meet(a,join(meet(c,sFlat3),meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_1,t75]) ).
cnf(g0_3,plain,
meet(a,join(meet(sFlat3,c),meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_2,t20]) ).
cnf(g0_4,plain,
meet(a,join(sFlat4,meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_3,t130]) ).
cnf(g0_5,plain,
meet(a,join(sFlat4,meet(a,join(b,meet(c,a))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_4,t20]) ).
cnf(g0_6,plain,
meet(a,join(sFlat4,meet(a,join(b,sFlat0)))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_5,t49]) ).
cnf(g0_7,plain,
meet(a,join(sFlat4,meet(a,join(sFlat0,b)))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_6,t58]) ).
cnf(g0_8,plain,
meet(a,join(sFlat4,meet(a,sFlat1))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_7,t79]) ).
cnf(g0_9,plain,
meet(a,join(sFlat4,meet(sFlat1,a))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_8,t20]) ).
cnf(g0_10,plain,
meet(a,join(sFlat4,sFlat2)) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_9,t119]) ).
cnf(g0_11,plain,
meet(a,join(sFlat2,sFlat4)) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_10,t58]) ).
cnf(g0_12,plain,
meet(a,sFlat5) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_11,t3974]) ).
cnf(g0_13,plain,
meet(sFlat5,a) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_12,t20]) ).
cnf(g0_14,plain,
sFlat2 != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_13,t4389]) ).
cnf(g0_15,plain,
sFlat2 != meet(a,join(b,meet(c,a))),
inference(rw,[status(thm)],[g0_14,t20]) ).
cnf(g0_16,plain,
sFlat2 != meet(a,join(b,sFlat0)),
inference(rw,[status(thm)],[g0_15,t49]) ).
cnf(g0_17,plain,
sFlat2 != meet(a,join(sFlat0,b)),
inference(rw,[status(thm)],[g0_16,t58]) ).
cnf(g0_18,plain,
sFlat2 != meet(a,sFlat1),
inference(rw,[status(thm)],[g0_17,t79]) ).
cnf(g0_19,plain,
sFlat2 != meet(sFlat1,a),
inference(rw,[status(thm)],[g0_18,t20]) ).
cnf(g0_20,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_19,t119]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT154-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.63 % Computer : n019.cluster.edu
% 0.16/0.63 % Model : x86_64 x86_64
% 0.16/0.63 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.63 % Memory : 8046.5625MB
% 0.16/0.63 % OS : Linux 6.8.0-71-generic
% 0.16/0.63 % CPULimit : 300
% 0.16/0.63 % WCLimit : 300
% 0.16/0.63 % DateTime : Wed Sep 23 20:24:24 UTC 2026
% 0.16/0.64 % CPUTime :
% 0.16/0.64 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 31.93/4.79 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 31.93/4.79 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------