%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT164-1 : TPTP v9.3.1. Released v3.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:55:47 PM UTC 2026
% Result : Unsatisfiable 18.91s 2.84s
% Output : CNFRefutation 18.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 17
% Syntax : Number of clauses : 242 ( 242 unt; 0 nHn; 158 RR)
% Number of literals : 242 ( 241 equ; 22 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 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 : 158 ( 33 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t61,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t12,axiom,
sFlat3 = join(a,b),
introduced(definition) ).
cnf(t3907,plain,
sFlat3 = join(b,a),
inference(step,[status(thm)],[t12,t61]) ).
cnf(t77,plain,
join(b,a) = sFlat3,
inference(orient,[status(thm)],[t3907]) ).
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/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(t57,plain,
meet(c,join(a,b)) = sFlat4,
inference(orient,[status(thm)],[t13]) ).
cnf(t62,plain,
meet(c,join(a,b)) = sFlat4,
inference(rw,[status(thm)],[t57]) ).
cnf(t3921,plain,
meet(c,join(b,a)) = sFlat4,
inference(step,[status(thm)],[t62,t61]) ).
cnf(t3922,plain,
meet(c,sFlat3) = sFlat4,
inference(step,[status(thm)],[t3921,t77]) ).
cnf(t3923,plain,
meet(sFlat3,c) = sFlat4,
inference(step,[status(thm)],[t3922,t20]) ).
cnf(t129,plain,
meet(sFlat3,c) = sFlat4,
inference(orient,[status(thm)],[t3923]) ).
cnf(t9,axiom,
sFlat0 = meet(a,c),
introduced(definition) ).
cnf(t3900,plain,
sFlat0 = meet(c,a),
inference(step,[status(thm)],[t9,t20]) ).
cnf(t52,plain,
meet(c,a) = sFlat0,
inference(orient,[status(thm)],[t3900]) ).
cnf(t10,axiom,
sFlat1 = join(b,meet(a,c)),
introduced(definition) ).
cnf(t3909,plain,
sFlat1 = join(b,meet(c,a)),
inference(step,[status(thm)],[t10,t20]) ).
cnf(t3910,plain,
sFlat1 = join(b,sFlat0),
inference(step,[status(thm)],[t3909,t52]) ).
cnf(t3911,plain,
sFlat1 = join(sFlat0,b),
inference(step,[status(thm)],[t3910,t61]) ).
cnf(t81,plain,
join(sFlat0,b) = sFlat1,
inference(orient,[status(thm)],[t3911]) ).
cnf(t11,axiom,
sFlat2 = meet(a,join(b,meet(a,c))),
introduced(definition) ).
cnf(t3898,plain,
sFlat2 = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t11,t20]) ).
cnf(t46,plain,
meet(a,join(b,meet(c,a))) = sFlat2,
inference(orient,[status(thm)],[t3898]) ).
cnf(t3901,plain,
meet(a,join(b,sFlat0)) = sFlat2,
inference(step,[status(thm)],[t46,t52]) ).
cnf(t56,plain,
meet(a,join(b,sFlat0)) = sFlat2,
inference(rw,[status(thm)],[t3901]) ).
cnf(t3917,plain,
meet(a,join(sFlat0,b)) = sFlat2,
inference(step,[status(thm)],[t56,t61]) ).
cnf(t3918,plain,
meet(a,sFlat1) = sFlat2,
inference(step,[status(thm)],[t3917,t81]) ).
cnf(t3919,plain,
meet(sFlat1,a) = sFlat2,
inference(step,[status(thm)],[t3918,t20]) ).
cnf(t119,plain,
meet(sFlat1,a) = sFlat2,
inference(orient,[status(thm)],[t3919]) ).
cnf(t14,axiom,
sFlat5 = join(meet(a,join(b,meet(a,c))),meet(c,join(a,b))),
introduced(definition) ).
cnf(t3902,plain,
sFlat5 = join(meet(c,join(a,b)),meet(a,join(b,meet(a,c)))),
inference(step,[status(thm)],[t14,t61]) ).
cnf(t3903,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(b,meet(a,c)))),
inference(step,[status(thm)],[t3902,t61]) ).
cnf(t3904,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(b,meet(c,a)))),
inference(step,[status(thm)],[t3903,t20]) ).
cnf(t3905,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(b,sFlat0))),
inference(step,[status(thm)],[t3904,t52]) ).
cnf(t3906,plain,
sFlat5 = join(meet(c,join(b,a)),meet(a,join(sFlat0,b))),
inference(step,[status(thm)],[t3905,t61]) ).
cnf(t73,plain,
join(meet(c,join(b,a)),meet(a,join(sFlat0,b))) = sFlat5,
inference(orient,[status(thm)],[t3906]) ).
cnf(t3908,plain,
join(meet(c,sFlat3),meet(a,join(sFlat0,b))) = sFlat5,
inference(step,[status(thm)],[t73,t77]) ).
cnf(t80,plain,
join(meet(c,sFlat3),meet(a,join(sFlat0,b))) = sFlat5,
inference(rw,[status(thm)],[t3908]) ).
cnf(t4144,plain,
join(meet(sFlat3,c),meet(a,join(sFlat0,b))) = sFlat5,
inference(step,[status(thm)],[t80,t20]) ).
cnf(t4145,plain,
join(sFlat4,meet(a,join(sFlat0,b))) = sFlat5,
inference(step,[status(thm)],[t4144,t129]) ).
cnf(t4146,plain,
join(sFlat4,meet(a,sFlat1)) = sFlat5,
inference(step,[status(thm)],[t4145,t81]) ).
cnf(t4147,plain,
join(sFlat4,meet(sFlat1,a)) = sFlat5,
inference(step,[status(thm)],[t4146,t20]) ).
cnf(t4148,plain,
join(sFlat4,sFlat2) = sFlat5,
inference(step,[status(thm)],[t4147,t119]) ).
cnf(t4149,plain,
join(sFlat2,sFlat4) = sFlat5,
inference(step,[status(thm)],[t4148,t61]) ).
cnf(t3699,plain,
join(sFlat2,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t4149]) ).
cnf(t15,axiom,
sFlat6 = meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))),
introduced(definition) ).
cnf(t3897,plain,
sFlat6 = meet(a,join(meet(a,join(b,meet(c,a))),meet(c,join(a,b)))),
inference(step,[status(thm)],[t15,t20]) ).
cnf(t41,plain,
meet(a,join(meet(a,join(b,meet(c,a))),meet(c,join(a,b)))) = sFlat6,
inference(orient,[status(thm)],[t3897]) ).
cnf(t3899,plain,
meet(a,join(sFlat2,meet(c,join(a,b)))) = sFlat6,
inference(step,[status(thm)],[t41,t46]) ).
cnf(t51,plain,
meet(a,join(sFlat2,meet(c,join(a,b)))) = sFlat6,
inference(rw,[status(thm)],[t3899]) ).
cnf(t4108,plain,
meet(a,join(sFlat2,meet(c,join(b,a)))) = sFlat6,
inference(step,[status(thm)],[t51,t61]) ).
cnf(t4109,plain,
meet(a,join(sFlat2,meet(c,sFlat3))) = sFlat6,
inference(step,[status(thm)],[t4108,t77]) ).
cnf(t4110,plain,
meet(a,join(sFlat2,meet(sFlat3,c))) = sFlat6,
inference(step,[status(thm)],[t4109,t20]) ).
cnf(t4111,plain,
meet(a,join(sFlat2,sFlat4)) = sFlat6,
inference(step,[status(thm)],[t4110,t129]) ).
cnf(t3563,plain,
meet(a,join(sFlat2,sFlat4)) = sFlat6,
inference(orient,[status(thm)],[t4111]) ).
cnf(t4153,plain,
meet(a,sFlat5) = sFlat6,
inference(step,[status(thm)],[t3563,t3699]) ).
cnf(t3714,plain,
meet(a,sFlat5) = sFlat6,
inference(rw,[status(thm)],[t4153]) ).
cnf(t4156,plain,
meet(sFlat5,a) = sFlat6,
inference(step,[status(thm)],[t3714,t20]) ).
cnf(t3735,plain,
meet(sFlat5,a) = sFlat6,
inference(orient,[status(thm)],[t4156]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t43,plain,
a = join(a,sFlat6),
inference(cp,[status(thm)],[t19,t41]) ).
cnf(t3912,plain,
a = join(sFlat6,a),
inference(step,[status(thm)],[t43,t61]) ).
cnf(t84,plain,
join(sFlat6,a) = a,
inference(orient,[status(thm)],[t3912]) ).
cnf(t85,plain,
sFlat6 = meet(sFlat6,a),
inference(cp,[status(thm)],[t17,t84]) ).
cnf(t102,plain,
meet(sFlat6,a) = sFlat6,
inference(orient,[status(thm)],[t85]) ).
cnf(t103,plain,
meet(sFlat6,meet(a,X1)) = meet(sFlat6,X1),
inference(cp,[status(thm)],[t21,t102]) ).
cnf(t428,plain,
meet(sFlat6,meet(a,X1)) = meet(sFlat6,X1),
inference(orient,[status(thm)],[t103]) ).
cnf(t8,axiom,
meet(X1,join(X2,meet(X3,join(X4,meet(X1,X2))))) = meet(X1,join(X2,meet(X3,join(X2,X4)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
meet(X1,join(X2,meet(X3,join(X4,meet(X1,X2))))) = meet(X1,join(X2,meet(X3,join(X2,X4)))),
inference(orient,[status(thm)],[t8]) ).
cnf(t34,plain,
meet(X1,join(X2,meet(X3,join(X2,X1)))) = meet(X1,join(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t29,t19]) ).
cnf(t2710,plain,
meet(X1,join(X2,meet(X3,join(X2,X1)))) = meet(X1,join(X2,meet(X3,X1))),
inference(orient,[status(thm)],[t34]) ).
cnf(t2765,plain,
meet(a,join(b,meet(X1,a))) = meet(a,join(b,meet(X1,sFlat3))),
inference(cp,[status(thm)],[t2710,t77]) ).
cnf(t3125,plain,
meet(a,join(b,meet(X1,a))) = meet(a,join(b,meet(X1,sFlat3))),
inference(orient,[status(thm)],[t2765]) ).
cnf(t3128,plain,
meet(a,join(b,meet(c,sFlat3))) = meet(a,join(b,sFlat0)),
inference(cp,[status(thm)],[t3125,t52]) ).
cnf(t4176,plain,
meet(a,join(b,meet(sFlat3,c))) = meet(a,join(b,sFlat0)),
inference(step,[status(thm)],[t3128,t20]) ).
cnf(t4177,plain,
meet(a,join(b,sFlat4)) = meet(a,join(b,sFlat0)),
inference(step,[status(thm)],[t4176,t129]) ).
cnf(t4178,plain,
meet(a,join(sFlat4,b)) = meet(a,join(b,sFlat0)),
inference(step,[status(thm)],[t4177,t61]) ).
cnf(t24,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t21,t20]) ).
cnf(t205,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t24]) ).
cnf(t212,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t19,t205]) ).
cnf(t537,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t212]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/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(t116,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t25]) ).
cnf(t539,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t537,t116]) ).
cnf(t603,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t539]) ).
cnf(t26,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t21,t17]) ).
cnf(t447,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t26]) ).
cnf(t450,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t447,t20]) ).
cnf(t881,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t450]) ).
cnf(t131,plain,
meet(sFlat3,meet(c,X1)) = meet(sFlat4,X1),
inference(cp,[status(thm)],[t21,t129]) ).
cnf(t283,plain,
meet(sFlat3,meet(c,X1)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t131]) ).
cnf(t53,plain,
meet(c,meet(a,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t21,t52]) ).
cnf(t145,plain,
meet(c,meet(a,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t53]) ).
cnf(t285,plain,
meet(sFlat4,meet(a,X1)) = meet(sFlat3,meet(sFlat0,X1)),
inference(cp,[status(thm)],[t283,t145]) ).
cnf(t27,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t21,t20]) ).
cnf(t3932,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t27,t21]) ).
cnf(t214,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t3932]) ).
cnf(t3965,plain,
meet(sFlat4,meet(a,X1)) = meet(sFlat0,meet(sFlat3,X1)),
inference(step,[status(thm)],[t285,t214]) ).
cnf(t496,plain,
meet(sFlat4,meet(a,X1)) = meet(sFlat0,meet(sFlat3,X1)),
inference(orient,[status(thm)],[t3965]) ).
cnf(t882,plain,
meet(sFlat4,a) = meet(sFlat0,meet(sFlat3,join(sFlat4,X1))),
inference(cp,[status(thm)],[t881,t496]) ).
cnf(t284,plain,
meet(sFlat4,a) = meet(sFlat3,sFlat0),
inference(cp,[status(thm)],[t283,t52]) ).
cnf(t3935,plain,
meet(sFlat4,a) = meet(sFlat0,sFlat3),
inference(step,[status(thm)],[t284,t20]) ).
cnf(t291,plain,
meet(sFlat4,a) = meet(sFlat0,sFlat3),
inference(orient,[status(thm)],[t3935]) ).
cnf(t148,plain,
meet(sFlat0,join(a,X1)) = meet(c,a),
inference(cp,[status(thm)],[t145,t17]) ).
cnf(t3929,plain,
meet(sFlat0,join(a,X1)) = sFlat0,
inference(step,[status(thm)],[t148,t52]) ).
cnf(t181,plain,
meet(sFlat0,join(a,X1)) = sFlat0,
inference(orient,[status(thm)],[t3929]) ).
cnf(t182,plain,
sFlat0 = meet(sFlat0,join(X1,a)),
inference(cp,[status(thm)],[t181,t61]) ).
cnf(t345,plain,
meet(sFlat0,join(X1,a)) = sFlat0,
inference(orient,[status(thm)],[t182]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t63,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t79,plain,
join(b,join(a,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t63,t77]) ).
cnf(t157,plain,
join(b,join(a,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t79]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t158,plain,
join(sFlat3,a) = join(b,a),
inference(cp,[status(thm)],[t157,t18]) ).
cnf(t3927,plain,
join(sFlat3,a) = sFlat3,
inference(step,[status(thm)],[t158,t77]) ).
cnf(t164,plain,
join(sFlat3,a) = sFlat3,
inference(orient,[status(thm)],[t3927]) ).
cnf(t346,plain,
sFlat0 = meet(sFlat0,sFlat3),
inference(cp,[status(thm)],[t345,t164]) ).
cnf(t351,plain,
meet(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t346]) ).
cnf(t3952,plain,
meet(sFlat4,a) = sFlat0,
inference(step,[status(thm)],[t291,t351]) ).
cnf(t352,plain,
meet(sFlat4,a) = sFlat0,
inference(orient,[status(thm)],[t3952]) ).
cnf(t4026,plain,
sFlat0 = meet(sFlat0,meet(sFlat3,join(sFlat4,X1))),
inference(step,[status(thm)],[t882,t352]) ).
cnf(t1661,plain,
meet(sFlat0,meet(sFlat3,join(sFlat4,X1))) = sFlat0,
inference(orient,[status(thm)],[t4026]) ).
cnf(t66,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t63,t61]) ).
cnf(t244,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t66]) ).
cnf(t249,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t17,t244]) ).
cnf(t665,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t249]) ).
cnf(t67,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t63,t18]) ).
cnf(t139,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t67]) ).
cnf(t667,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t665,t139]) ).
cnf(t742,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t667]) ).
cnf(t132,plain,
sFlat3 = join(sFlat3,sFlat4),
inference(cp,[status(thm)],[t19,t129]) ).
cnf(t137,plain,
join(sFlat3,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t132]) ).
cnf(t138,plain,
join(sFlat3,join(sFlat4,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t63,t137]) ).
cnf(t461,plain,
join(sFlat3,join(sFlat4,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t138]) ).
cnf(t754,plain,
join(sFlat4,X1) = meet(join(sFlat4,X1),join(sFlat3,X1)),
inference(cp,[status(thm)],[t742,t461]) ).
cnf(t4054,plain,
join(sFlat4,X1) = meet(join(sFlat3,X1),join(sFlat4,X1)),
inference(step,[status(thm)],[t754,t20]) ).
cnf(t2214,plain,
meet(join(sFlat3,X1),join(sFlat4,X1)) = join(sFlat4,X1),
inference(orient,[status(thm)],[t4054]) ).
cnf(t78,plain,
b = meet(b,sFlat3),
inference(cp,[status(thm)],[t17,t77]) ).
cnf(t3916,plain,
b = meet(sFlat3,b),
inference(step,[status(thm)],[t78,t20]) ).
cnf(t96,plain,
meet(sFlat3,b) = b,
inference(orient,[status(thm)],[t3916]) ).
cnf(t98,plain,
sFlat3 = join(sFlat3,b),
inference(cp,[status(thm)],[t19,t96]) ).
cnf(t114,plain,
join(sFlat3,b) = sFlat3,
inference(orient,[status(thm)],[t98]) ).
cnf(t2231,plain,
join(sFlat4,b) = meet(sFlat3,join(sFlat4,b)),
inference(cp,[status(thm)],[t2214,t114]) ).
cnf(t2273,plain,
meet(sFlat3,join(sFlat4,b)) = join(sFlat4,b),
inference(orient,[status(thm)],[t2231]) ).
cnf(t2274,plain,
sFlat0 = meet(sFlat0,join(sFlat4,b)),
inference(cp,[status(thm)],[t1661,t2273]) ).
cnf(t2292,plain,
meet(sFlat0,join(sFlat4,b)) = sFlat0,
inference(orient,[status(thm)],[t2274]) ).
cnf(t2297,plain,
join(sFlat4,b) = join(join(sFlat4,b),sFlat0),
inference(cp,[status(thm)],[t603,t2292]) ).
cnf(t4164,plain,
join(sFlat4,b) = join(sFlat4,join(b,sFlat0)),
inference(step,[status(thm)],[t2297,t63]) ).
cnf(t4165,plain,
join(sFlat4,b) = join(sFlat0,join(sFlat4,b)),
inference(step,[status(thm)],[t4164,t244]) ).
cnf(t83,plain,
join(sFlat0,join(b,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t63,t81]) ).
cnf(t166,plain,
join(sFlat0,join(b,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t83]) ).
cnf(t172,plain,
join(sFlat1,X1) = join(sFlat0,join(X1,b)),
inference(cp,[status(thm)],[t166,t61]) ).
cnf(t338,plain,
join(sFlat0,join(X1,b)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t172]) ).
cnf(t4166,plain,
join(sFlat4,b) = join(sFlat1,sFlat4),
inference(step,[status(thm)],[t4165,t338]) ).
cnf(t3843,plain,
join(sFlat4,b) = join(sFlat1,sFlat4),
inference(orient,[status(thm)],[t4166]) ).
cnf(t4179,plain,
meet(a,join(sFlat1,sFlat4)) = meet(a,join(b,sFlat0)),
inference(step,[status(thm)],[t4178,t3843]) ).
cnf(t4180,plain,
meet(a,join(sFlat1,sFlat4)) = meet(a,join(sFlat0,b)),
inference(step,[status(thm)],[t4179,t61]) ).
cnf(t4181,plain,
meet(a,join(sFlat1,sFlat4)) = meet(a,sFlat1),
inference(step,[status(thm)],[t4180,t81]) ).
cnf(t4182,plain,
meet(a,join(sFlat1,sFlat4)) = meet(sFlat1,a),
inference(step,[status(thm)],[t4181,t20]) ).
cnf(t4183,plain,
meet(a,join(sFlat1,sFlat4)) = sFlat2,
inference(step,[status(thm)],[t4182,t119]) ).
cnf(t3871,plain,
meet(a,join(sFlat1,sFlat4)) = sFlat2,
inference(orient,[status(thm)],[t4183]) ).
cnf(t3874,plain,
meet(sFlat6,join(sFlat1,sFlat4)) = meet(sFlat6,sFlat2),
inference(cp,[status(thm)],[t428,t3871]) ).
cnf(t122,plain,
sFlat1 = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t19,t119]) ).
cnf(t127,plain,
join(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t122]) ).
cnf(t128,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t63,t127]) ).
cnf(t459,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t128]) ).
cnf(t3566,plain,
join(sFlat2,sFlat4) = join(join(sFlat2,sFlat4),sFlat6),
inference(cp,[status(thm)],[t603,t3563]) ).
cnf(t4142,plain,
join(sFlat2,sFlat4) = join(sFlat2,join(sFlat4,sFlat6)),
inference(step,[status(thm)],[t3566,t63]) ).
cnf(t3675,plain,
join(sFlat2,join(sFlat4,sFlat6)) = join(sFlat2,sFlat4),
inference(orient,[status(thm)],[t4142]) ).
cnf(t3678,plain,
join(sFlat1,join(sFlat4,sFlat6)) = join(sFlat1,join(sFlat2,sFlat4)),
inference(cp,[status(thm)],[t459,t3675]) ).
cnf(t4143,plain,
join(sFlat1,join(sFlat4,sFlat6)) = join(sFlat1,sFlat4),
inference(step,[status(thm)],[t3678,t459]) ).
cnf(t3683,plain,
join(sFlat1,join(sFlat4,sFlat6)) = join(sFlat1,sFlat4),
inference(orient,[status(thm)],[t4143]) ).
cnf(t3687,plain,
sFlat6 = meet(sFlat6,join(sFlat1,sFlat4)),
inference(cp,[status(thm)],[t665,t3683]) ).
cnf(t3691,plain,
meet(sFlat6,join(sFlat1,sFlat4)) = sFlat6,
inference(orient,[status(thm)],[t3687]) ).
cnf(t4184,plain,
sFlat6 = meet(sFlat6,sFlat2),
inference(step,[status(thm)],[t3874,t3691]) ).
cnf(t4185,plain,
sFlat6 = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t4184,t20]) ).
cnf(t676,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,X1)),
inference(cp,[status(thm)],[t665,t19]) ).
cnf(t3997,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,X1))),
inference(step,[status(thm)],[t676,t21]) ).
cnf(t1113,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t3997]) ).
cnf(t121,plain,
meet(sFlat1,meet(a,X1)) = meet(sFlat2,X1),
inference(cp,[status(thm)],[t21,t119]) ).
cnf(t277,plain,
meet(sFlat1,meet(a,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t121]) ).
cnf(t70,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(cp,[status(thm)],[t17,t63]) ).
cnf(t2537,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t70]) ).
cnf(t48,plain,
a = join(a,sFlat2),
inference(cp,[status(thm)],[t19,t46]) ).
cnf(t3913,plain,
a = join(sFlat2,a),
inference(step,[status(thm)],[t48,t61]) ).
cnf(t87,plain,
join(sFlat2,a) = a,
inference(orient,[status(thm)],[t3913]) ).
cnf(t2578,plain,
join(X1,sFlat2) = meet(join(X1,sFlat2),join(X1,a)),
inference(cp,[status(thm)],[t2537,t87]) ).
cnf(t2614,plain,
meet(join(X1,sFlat2),join(X1,a)) = join(X1,sFlat2),
inference(orient,[status(thm)],[t2578]) ).
cnf(t2616,plain,
join(sFlat6,sFlat2) = meet(join(sFlat6,sFlat2),a),
inference(cp,[status(thm)],[t2614,t84]) ).
cnf(t4061,plain,
join(sFlat2,sFlat6) = meet(join(sFlat6,sFlat2),a),
inference(step,[status(thm)],[t2616,t61]) ).
cnf(t4062,plain,
join(sFlat2,sFlat6) = meet(a,join(sFlat6,sFlat2)),
inference(step,[status(thm)],[t4061,t20]) ).
cnf(t4063,plain,
join(sFlat2,sFlat6) = meet(a,join(sFlat2,sFlat6)),
inference(step,[status(thm)],[t4062,t61]) ).
cnf(t2624,plain,
meet(a,join(sFlat2,sFlat6)) = join(sFlat2,sFlat6),
inference(orient,[status(thm)],[t4063]) ).
cnf(t2628,plain,
meet(sFlat2,join(sFlat2,sFlat6)) = meet(sFlat1,join(sFlat2,sFlat6)),
inference(cp,[status(thm)],[t277,t2624]) ).
cnf(t4067,plain,
sFlat2 = meet(sFlat1,join(sFlat2,sFlat6)),
inference(step,[status(thm)],[t2628,t17]) ).
cnf(t2643,plain,
meet(sFlat1,join(sFlat2,sFlat6)) = sFlat2,
inference(orient,[status(thm)],[t4067]) ).
cnf(t2646,plain,
meet(sFlat6,sFlat1) = meet(sFlat6,sFlat2),
inference(cp,[status(thm)],[t1113,t2643]) ).
cnf(t4068,plain,
meet(sFlat1,sFlat6) = meet(sFlat6,sFlat2),
inference(step,[status(thm)],[t2646,t20]) ).
cnf(t4069,plain,
meet(sFlat1,sFlat6) = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t4068,t20]) ).
cnf(t2651,plain,
meet(sFlat2,sFlat6) = meet(sFlat1,sFlat6),
inference(orient,[status(thm)],[t4069]) ).
cnf(t3571,plain,
meet(sFlat2,join(sFlat2,sFlat4)) = meet(sFlat1,sFlat6),
inference(cp,[status(thm)],[t277,t3563]) ).
cnf(t4120,plain,
sFlat2 = meet(sFlat1,sFlat6),
inference(step,[status(thm)],[t3571,t17]) ).
cnf(t3599,plain,
meet(sFlat1,sFlat6) = sFlat2,
inference(orient,[status(thm)],[t4120]) ).
cnf(t4121,plain,
meet(sFlat2,sFlat6) = sFlat2,
inference(step,[status(thm)],[t2651,t3599]) ).
cnf(t3600,plain,
meet(sFlat2,sFlat6) = sFlat2,
inference(orient,[status(thm)],[t4121]) ).
cnf(t4186,plain,
sFlat6 = sFlat2,
inference(step,[status(thm)],[t4185,t3600]) ).
cnf(t3882,plain,
sFlat6 = sFlat2,
inference(orient,[status(thm)],[t4186]) ).
cnf(t4187,plain,
meet(sFlat5,a) = sFlat2,
inference(step,[status(thm)],[t3735,t3882]) ).
cnf(t3883,plain,
meet(sFlat5,a) = sFlat2,
inference(orient,[status(thm)],[t4187]) ).
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/sandbox/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,t61]) ).
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,t61]) ).
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,t77]) ).
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,t129]) ).
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,t52]) ).
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,t61]) ).
cnf(g0_8,plain,
meet(a,join(sFlat4,meet(a,sFlat1))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_7,t81]) ).
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,t61]) ).
cnf(g0_12,plain,
meet(a,sFlat5) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_11,t3699]) ).
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,t3883]) ).
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,t52]) ).
cnf(g0_17,plain,
sFlat2 != meet(a,join(sFlat0,b)),
inference(rw,[status(thm)],[g0_16,t61]) ).
cnf(g0_18,plain,
sFlat2 != meet(a,sFlat1),
inference(rw,[status(thm)],[g0_17,t81]) ).
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.02 % Problem : LAT164-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n026.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 20:28:09 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 18.91/2.84 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.91/2.84 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------