%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT143-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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:55:34 PM UTC 2026
% Result : Unsatisfiable 63.36s 8.59s
% Output : CNFRefutation 63.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 16
% Syntax : Number of clauses : 246 ( 246 unt; 0 nHn; 181 RR)
% Number of literals : 246 ( 245 equ; 27 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 : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 109 ( 8 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t49,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t31,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t54,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t49,t31]) ).
cnf(t417,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t54]) ).
cnf(t55,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t49,t31]) ).
cnf(t21210,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t55,t49]) ).
cnf(t534,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t21210]) ).
cnf(t536,plain,
join(X1,join(X2,X3)) = join(join(X1,X3),X2),
inference(cp,[status(thm)],[t534,t31]) ).
cnf(t21596,plain,
join(X1,join(X2,X3)) = join(X1,join(X3,X2)),
inference(step,[status(thm)],[t536,t49]) ).
cnf(t18887,plain,
join(X1,join(X2,X3)) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t21596]) ).
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t60,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t10,axiom,
sF1 = meet(a,c),
introduced(definition) ).
cnf(t21,plain,
meet(a,c) = sF1,
inference(orient,[status(thm)],[t10]) ).
cnf(t21149,plain,
meet(c,a) = sF1,
inference(step,[status(thm)],[t21,t60]) ).
cnf(t62,plain,
meet(c,a) = sF1,
inference(rw,[status(thm)],[t21149]) ).
cnf(t72,plain,
meet(c,a) = sF1,
inference(orient,[status(thm)],[t62]) ).
cnf(t9,axiom,
sF0 = meet(a,b),
introduced(definition) ).
cnf(t20,plain,
meet(a,b) = sF0,
inference(orient,[status(thm)],[t9]) ).
cnf(t21148,plain,
meet(b,a) = sF0,
inference(step,[status(thm)],[t20,t60]) ).
cnf(t61,plain,
meet(b,a) = sF0,
inference(rw,[status(thm)],[t21148]) ).
cnf(t69,plain,
meet(b,a) = sF0,
inference(orient,[status(thm)],[t61]) ).
cnf(t16,axiom,
sF7 = join(meet(a,b),meet(a,c)),
introduced(definition) ).
cnf(t21187,plain,
sF7 = join(meet(a,c),meet(a,b)),
inference(step,[status(thm)],[t16,t31]) ).
cnf(t21188,plain,
sF7 = join(meet(c,a),meet(a,b)),
inference(step,[status(thm)],[t21187,t60]) ).
cnf(t21189,plain,
sF7 = join(sF1,meet(a,b)),
inference(step,[status(thm)],[t21188,t72]) ).
cnf(t21190,plain,
sF7 = join(sF1,meet(b,a)),
inference(step,[status(thm)],[t21189,t60]) ).
cnf(t21191,plain,
sF7 = join(sF1,sF0),
inference(step,[status(thm)],[t21190,t69]) ).
cnf(t21192,plain,
sF7 = join(sF0,sF1),
inference(step,[status(thm)],[t21191,t31]) ).
cnf(t253,plain,
join(sF0,sF1) = sF7,
inference(orient,[status(thm)],[t21192]) ).
cnf(t559,plain,
join(sF0,join(X1,sF1)) = join(X1,sF7),
inference(cp,[status(thm)],[t534,t253]) ).
cnf(t5358,plain,
join(sF0,join(X1,sF1)) = join(X1,sF7),
inference(orient,[status(thm)],[t559]) ).
cnf(t8,axiom,
join(meet(X1,X2),meet(X2,join(meet(X1,X2),meet(X3,join(X1,X2))))) = join(meet(X1,X2),meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t115,plain,
join(meet(X1,X2),meet(X2,join(meet(X1,X2),meet(X3,join(X1,X2))))) = join(meet(X1,X2),meet(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t11,axiom,
sF2 = join(a,b),
introduced(definition) ).
cnf(t22,plain,
join(a,b) = sF2,
inference(orient,[status(thm)],[t11]) ).
cnf(t21145,plain,
join(b,a) = sF2,
inference(step,[status(thm)],[t22,t31]) ).
cnf(t32,plain,
join(b,a) = sF2,
inference(rw,[status(thm)],[t21145]) ).
cnf(t37,plain,
join(b,a) = sF2,
inference(orient,[status(thm)],[t32]) ).
cnf(t123,plain,
join(meet(b,a),meet(a,X1)) = join(meet(b,a),meet(a,join(meet(b,a),meet(X1,sF2)))),
inference(cp,[status(thm)],[t115,t37]) ).
cnf(t21263,plain,
join(sF0,meet(a,X1)) = join(meet(b,a),meet(a,join(meet(b,a),meet(X1,sF2)))),
inference(step,[status(thm)],[t123,t69]) ).
cnf(t21264,plain,
join(sF0,meet(a,X1)) = join(sF0,meet(a,join(meet(b,a),meet(X1,sF2)))),
inference(step,[status(thm)],[t21263,t69]) ).
cnf(t21265,plain,
join(sF0,meet(a,X1)) = join(sF0,meet(a,join(sF0,meet(X1,sF2)))),
inference(step,[status(thm)],[t21264,t69]) ).
cnf(t1674,plain,
join(sF0,meet(a,join(sF0,meet(X1,sF2)))) = join(sF0,meet(a,X1)),
inference(orient,[status(thm)],[t21265]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t89,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t96,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t89,t60]) ).
cnf(t837,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t96]) ).
cnf(t12,axiom,
sF3 = meet(c,join(a,b)),
introduced(definition) ).
cnf(t21154,plain,
sF3 = meet(c,join(b,a)),
inference(step,[status(thm)],[t12,t31]) ).
cnf(t21155,plain,
sF3 = meet(c,sF2),
inference(step,[status(thm)],[t21154,t37]) ).
cnf(t21156,plain,
sF3 = meet(sF2,c),
inference(step,[status(thm)],[t21155,t60]) ).
cnf(t139,plain,
meet(sF2,c) = sF3,
inference(orient,[status(thm)],[t21156]) ).
cnf(t849,plain,
meet(c,meet(X1,sF2)) = meet(X1,sF3),
inference(cp,[status(thm)],[t837,t139]) ).
cnf(t21415,plain,
meet(sF2,meet(c,X1)) = meet(X1,sF3),
inference(step,[status(thm)],[t849,t837]) ).
cnf(t142,plain,
meet(sF2,meet(c,X1)) = meet(sF3,X1),
inference(cp,[status(thm)],[t89,t139]) ).
cnf(t523,plain,
meet(sF2,meet(c,X1)) = meet(sF3,X1),
inference(orient,[status(thm)],[t142]) ).
cnf(t21416,plain,
meet(sF3,X1) = meet(X1,sF3),
inference(step,[status(thm)],[t21415,t523]) ).
cnf(t6647,plain,
meet(sF3,X1) = meet(X1,sF3),
inference(orient,[status(thm)],[t21416]) ).
cnf(t6658,plain,
join(sF0,meet(a,sF3)) = join(sF0,meet(a,join(sF0,meet(sF2,sF3)))),
inference(cp,[status(thm)],[t1674,t6647]) ).
cnf(t21606,plain,
join(sF0,meet(sF3,a)) = join(sF0,meet(a,join(sF0,meet(sF2,sF3)))),
inference(step,[status(thm)],[t6658,t60]) ).
cnf(t527,plain,
meet(sF3,a) = meet(sF2,sF1),
inference(cp,[status(thm)],[t523,t72]) ).
cnf(t21211,plain,
meet(sF3,a) = meet(sF1,sF2),
inference(step,[status(thm)],[t527,t60]) ).
cnf(t595,plain,
meet(sF3,a) = meet(sF1,sF2),
inference(orient,[status(thm)],[t21211]) ).
cnf(t5,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t56,plain,
join(b,join(a,X1)) = join(sF2,X1),
inference(cp,[status(thm)],[t49,t37]) ).
cnf(t205,plain,
join(b,join(a,X1)) = join(sF2,X1),
inference(orient,[status(thm)],[t56]) ).
cnf(t208,plain,
join(sF2,X1) = join(b,join(X1,a)),
inference(cp,[status(thm)],[t205,t31]) ).
cnf(t1160,plain,
join(b,join(X1,a)) = join(sF2,X1),
inference(orient,[status(thm)],[t208]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t25,plain,
a = join(a,sF1),
inference(cp,[status(thm)],[t23,t21]) ).
cnf(t27,plain,
join(a,sF1) = a,
inference(orient,[status(thm)],[t25]) ).
cnf(t21147,plain,
join(sF1,a) = a,
inference(step,[status(thm)],[t27,t31]) ).
cnf(t34,plain,
join(sF1,a) = a,
inference(rw,[status(thm)],[t21147]) ).
cnf(t43,plain,
join(sF1,a) = a,
inference(orient,[status(thm)],[t34]) ).
cnf(t1164,plain,
join(sF2,sF1) = join(b,a),
inference(cp,[status(thm)],[t1160,t43]) ).
cnf(t21230,plain,
join(sF1,sF2) = join(b,a),
inference(step,[status(thm)],[t1164,t31]) ).
cnf(t21231,plain,
join(sF1,sF2) = sF2,
inference(step,[status(thm)],[t21230,t37]) ).
cnf(t1175,plain,
join(sF1,sF2) = sF2,
inference(orient,[status(thm)],[t21231]) ).
cnf(t1177,plain,
sF1 = meet(sF1,sF2),
inference(cp,[status(thm)],[t28,t1175]) ).
cnf(t1200,plain,
meet(sF1,sF2) = sF1,
inference(orient,[status(thm)],[t1177]) ).
cnf(t21234,plain,
meet(sF3,a) = sF1,
inference(step,[status(thm)],[t595,t1200]) ).
cnf(t1201,plain,
meet(sF3,a) = sF1,
inference(orient,[status(thm)],[t21234]) ).
cnf(t21607,plain,
join(sF0,sF1) = join(sF0,meet(a,join(sF0,meet(sF2,sF3)))),
inference(step,[status(thm)],[t21606,t1201]) ).
cnf(t21608,plain,
sF7 = join(sF0,meet(a,join(sF0,meet(sF2,sF3)))),
inference(step,[status(thm)],[t21607,t253]) ).
cnf(t36,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t28,t31]) ).
cnf(t148,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t36]) ).
cnf(t141,plain,
sF2 = join(sF2,sF3),
inference(cp,[status(thm)],[t23,t139]) ).
cnf(t144,plain,
join(sF2,sF3) = sF2,
inference(orient,[status(thm)],[t141]) ).
cnf(t156,plain,
sF3 = meet(sF3,sF2),
inference(cp,[status(thm)],[t148,t144]) ).
cnf(t21163,plain,
sF3 = meet(sF2,sF3),
inference(step,[status(thm)],[t156,t60]) ).
cnf(t165,plain,
meet(sF2,sF3) = sF3,
inference(orient,[status(thm)],[t21163]) ).
cnf(t21609,plain,
sF7 = join(sF0,meet(a,join(sF0,sF3))),
inference(step,[status(thm)],[t21608,t165]) ).
cnf(t14,axiom,
sF5 = join(meet(a,b),join(meet(a,c),meet(c,join(a,b)))),
introduced(definition) ).
cnf(t21165,plain,
sF5 = join(meet(b,a),join(meet(a,c),meet(c,join(a,b)))),
inference(step,[status(thm)],[t14,t60]) ).
cnf(t21166,plain,
sF5 = join(sF0,join(meet(a,c),meet(c,join(a,b)))),
inference(step,[status(thm)],[t21165,t69]) ).
cnf(t21167,plain,
sF5 = join(sF0,join(meet(c,a),meet(c,join(a,b)))),
inference(step,[status(thm)],[t21166,t60]) ).
cnf(t21168,plain,
sF5 = join(sF0,join(sF1,meet(c,join(a,b)))),
inference(step,[status(thm)],[t21167,t72]) ).
cnf(t21169,plain,
sF5 = join(sF0,join(sF1,meet(c,join(b,a)))),
inference(step,[status(thm)],[t21168,t31]) ).
cnf(t21170,plain,
sF5 = join(sF0,join(sF1,meet(c,sF2))),
inference(step,[status(thm)],[t21169,t37]) ).
cnf(t21171,plain,
sF5 = join(sF0,join(sF1,meet(sF2,c))),
inference(step,[status(thm)],[t21170,t60]) ).
cnf(t21172,plain,
sF5 = join(sF0,join(sF1,sF3)),
inference(step,[status(thm)],[t21171,t139]) ).
cnf(t13,axiom,
sF4 = join(meet(a,c),meet(c,join(a,b))),
introduced(definition) ).
cnf(t21157,plain,
sF4 = join(meet(c,a),meet(c,join(a,b))),
inference(step,[status(thm)],[t13,t60]) ).
cnf(t21158,plain,
sF4 = join(sF1,meet(c,join(a,b))),
inference(step,[status(thm)],[t21157,t72]) ).
cnf(t21159,plain,
sF4 = join(sF1,meet(c,join(b,a))),
inference(step,[status(thm)],[t21158,t31]) ).
cnf(t21160,plain,
sF4 = join(sF1,meet(c,sF2)),
inference(step,[status(thm)],[t21159,t37]) ).
cnf(t21161,plain,
sF4 = join(sF1,meet(sF2,c)),
inference(step,[status(thm)],[t21160,t60]) ).
cnf(t21162,plain,
sF4 = join(sF1,sF3),
inference(step,[status(thm)],[t21161,t139]) ).
cnf(t159,plain,
join(sF1,sF3) = sF4,
inference(orient,[status(thm)],[t21162]) ).
cnf(t21173,plain,
sF5 = join(sF0,sF4),
inference(step,[status(thm)],[t21172,t159]) ).
cnf(t186,plain,
join(sF0,sF4) = sF5,
inference(orient,[status(thm)],[t21173]) ).
cnf(t68,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t23,t60]) ).
cnf(t236,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t68]) ).
cnf(t244,plain,
c = join(c,sF3),
inference(cp,[status(thm)],[t236,t139]) ).
cnf(t21193,plain,
c = join(sF3,c),
inference(step,[status(thm)],[t244,t31]) ).
cnf(t260,plain,
join(sF3,c) = c,
inference(orient,[status(thm)],[t21193]) ).
cnf(t262,plain,
sF3 = meet(sF3,c),
inference(cp,[status(thm)],[t28,t260]) ).
cnf(t297,plain,
meet(sF3,c) = sF3,
inference(orient,[status(thm)],[t262]) ).
cnf(t299,plain,
meet(sF3,meet(c,X1)) = meet(sF3,X1),
inference(cp,[status(thm)],[t89,t297]) ).
cnf(t2259,plain,
meet(sF3,meet(c,X1)) = meet(sF3,X1),
inference(orient,[status(thm)],[t299]) ).
cnf(t2261,plain,
meet(sF3,a) = meet(sF3,sF1),
inference(cp,[status(thm)],[t2259,t72]) ).
cnf(t21284,plain,
sF1 = meet(sF3,sF1),
inference(step,[status(thm)],[t2261,t1201]) ).
cnf(t21285,plain,
sF1 = meet(sF1,sF3),
inference(step,[status(thm)],[t21284,t60]) ).
cnf(t2272,plain,
meet(sF1,sF3) = sF1,
inference(orient,[status(thm)],[t21285]) ).
cnf(t2276,plain,
sF3 = join(sF3,sF1),
inference(cp,[status(thm)],[t236,t2272]) ).
cnf(t21286,plain,
sF3 = join(sF1,sF3),
inference(step,[status(thm)],[t2276,t31]) ).
cnf(t21287,plain,
sF3 = sF4,
inference(step,[status(thm)],[t21286,t159]) ).
cnf(t2283,plain,
sF4 = sF3,
inference(orient,[status(thm)],[t21287]) ).
cnf(t21290,plain,
join(sF0,sF3) = sF5,
inference(step,[status(thm)],[t186,t2283]) ).
cnf(t2289,plain,
join(sF0,sF3) = sF5,
inference(rw,[status(thm)],[t21290]) ).
cnf(t2309,plain,
join(sF0,sF3) = sF5,
inference(orient,[status(thm)],[t2289]) ).
cnf(t21610,plain,
sF7 = join(sF0,meet(a,sF5)),
inference(step,[status(thm)],[t21609,t2309]) ).
cnf(t21611,plain,
sF7 = join(sF0,meet(sF5,a)),
inference(step,[status(thm)],[t21610,t60]) ).
cnf(t15,axiom,
sF6 = meet(a,join(meet(a,b),join(meet(a,c),meet(c,join(a,b))))),
introduced(definition) ).
cnf(t21175,plain,
sF6 = meet(a,join(meet(b,a),join(meet(a,c),meet(c,join(a,b))))),
inference(step,[status(thm)],[t15,t60]) ).
cnf(t21176,plain,
sF6 = meet(a,join(sF0,join(meet(a,c),meet(c,join(a,b))))),
inference(step,[status(thm)],[t21175,t69]) ).
cnf(t21177,plain,
sF6 = meet(a,join(sF0,join(meet(c,a),meet(c,join(a,b))))),
inference(step,[status(thm)],[t21176,t60]) ).
cnf(t21178,plain,
sF6 = meet(a,join(sF0,join(sF1,meet(c,join(a,b))))),
inference(step,[status(thm)],[t21177,t72]) ).
cnf(t21179,plain,
sF6 = meet(a,join(sF0,join(sF1,meet(c,join(b,a))))),
inference(step,[status(thm)],[t21178,t31]) ).
cnf(t21180,plain,
sF6 = meet(a,join(sF0,join(sF1,meet(c,sF2)))),
inference(step,[status(thm)],[t21179,t37]) ).
cnf(t21181,plain,
sF6 = meet(a,join(sF0,join(sF1,meet(sF2,c)))),
inference(step,[status(thm)],[t21180,t60]) ).
cnf(t21182,plain,
sF6 = meet(a,join(sF0,join(sF1,sF3))),
inference(step,[status(thm)],[t21181,t139]) ).
cnf(t21183,plain,
sF6 = meet(a,join(sF0,sF4)),
inference(step,[status(thm)],[t21182,t159]) ).
cnf(t21184,plain,
sF6 = meet(a,sF5),
inference(step,[status(thm)],[t21183,t186]) ).
cnf(t21185,plain,
sF6 = meet(sF5,a),
inference(step,[status(thm)],[t21184,t60]) ).
cnf(t218,plain,
meet(sF5,a) = sF6,
inference(orient,[status(thm)],[t21185]) ).
cnf(t21612,plain,
sF7 = join(sF0,sF6),
inference(step,[status(thm)],[t21611,t218]) ).
cnf(t188,plain,
sF0 = meet(sF0,sF5),
inference(cp,[status(thm)],[t28,t186]) ).
cnf(t193,plain,
meet(sF0,sF5) = sF0,
inference(orient,[status(thm)],[t188]) ).
cnf(t195,plain,
meet(sF0,meet(sF5,X1)) = meet(sF0,X1),
inference(cp,[status(thm)],[t89,t193]) ).
cnf(t1036,plain,
meet(sF0,meet(sF5,X1)) = meet(sF0,X1),
inference(orient,[status(thm)],[t195]) ).
cnf(t1040,plain,
meet(sF0,a) = meet(sF0,sF6),
inference(cp,[status(thm)],[t1036,t218]) ).
cnf(t24,plain,
a = join(a,sF0),
inference(cp,[status(thm)],[t23,t20]) ).
cnf(t26,plain,
join(a,sF0) = a,
inference(orient,[status(thm)],[t24]) ).
cnf(t21146,plain,
join(sF0,a) = a,
inference(step,[status(thm)],[t26,t31]) ).
cnf(t33,plain,
join(sF0,a) = a,
inference(rw,[status(thm)],[t21146]) ).
cnf(t40,plain,
join(sF0,a) = a,
inference(orient,[status(thm)],[t33]) ).
cnf(t42,plain,
sF0 = meet(sF0,a),
inference(cp,[status(thm)],[t28,t40]) ).
cnf(t47,plain,
meet(sF0,a) = sF0,
inference(orient,[status(thm)],[t42]) ).
cnf(t21222,plain,
sF0 = meet(sF0,sF6),
inference(step,[status(thm)],[t1040,t47]) ).
cnf(t1049,plain,
meet(sF0,sF6) = sF0,
inference(orient,[status(thm)],[t21222]) ).
cnf(t1053,plain,
sF6 = join(sF6,sF0),
inference(cp,[status(thm)],[t236,t1049]) ).
cnf(t21223,plain,
sF6 = join(sF0,sF6),
inference(step,[status(thm)],[t1053,t31]) ).
cnf(t1057,plain,
join(sF0,sF6) = sF6,
inference(orient,[status(thm)],[t21223]) ).
cnf(t21613,plain,
sF7 = sF6,
inference(step,[status(thm)],[t21612,t1057]) ).
cnf(t21060,plain,
sF7 = sF6,
inference(orient,[status(thm)],[t21613]) ).
cnf(t21622,plain,
join(sF0,join(X1,sF1)) = join(X1,sF6),
inference(step,[status(thm)],[t5358,t21060]) ).
cnf(t21091,plain,
join(sF0,join(X1,sF1)) = join(X1,sF6),
inference(orient,[status(thm)],[t21622]) ).
cnf(t256,plain,
join(sF0,join(sF1,X1)) = join(sF7,X1),
inference(cp,[status(thm)],[t49,t253]) ).
cnf(t1591,plain,
join(sF0,join(sF1,X1)) = join(sF7,X1),
inference(orient,[status(thm)],[t256]) ).
cnf(t162,plain,
join(sF1,join(sF3,X1)) = join(sF4,X1),
inference(cp,[status(thm)],[t49,t159]) ).
cnf(t674,plain,
join(sF1,join(sF3,X1)) = join(sF4,X1),
inference(orient,[status(thm)],[t162]) ).
cnf(t1609,plain,
join(sF7,join(sF3,X1)) = join(sF0,join(sF4,X1)),
inference(cp,[status(thm)],[t1591,t674]) ).
cnf(t189,plain,
join(sF0,join(sF4,X1)) = join(sF5,X1),
inference(cp,[status(thm)],[t49,t186]) ).
cnf(t920,plain,
join(sF0,join(sF4,X1)) = join(sF5,X1),
inference(orient,[status(thm)],[t189]) ).
cnf(t21485,plain,
join(sF7,join(sF3,X1)) = join(sF5,X1),
inference(step,[status(thm)],[t1609,t920]) ).
cnf(t21486,plain,
join(sF3,join(X1,sF7)) = join(sF5,X1),
inference(step,[status(thm)],[t21485,t417]) ).
cnf(t9579,plain,
join(sF3,join(X1,sF7)) = join(sF5,X1),
inference(orient,[status(thm)],[t21486]) ).
cnf(t161,plain,
sF1 = meet(sF1,sF4),
inference(cp,[status(thm)],[t28,t159]) ).
cnf(t168,plain,
meet(sF1,sF4) = sF1,
inference(orient,[status(thm)],[t161]) ).
cnf(t170,plain,
meet(sF1,meet(sF4,X1)) = meet(sF1,X1),
inference(cp,[status(thm)],[t89,t168]) ).
cnf(t712,plain,
meet(sF1,meet(sF4,X1)) = meet(sF1,X1),
inference(orient,[status(thm)],[t170]) ).
cnf(t191,plain,
sF4 = meet(sF4,sF5),
inference(cp,[status(thm)],[t148,t186]) ).
cnf(t197,plain,
meet(sF4,sF5) = sF4,
inference(orient,[status(thm)],[t191]) ).
cnf(t199,plain,
meet(sF4,meet(sF5,X1)) = meet(sF4,X1),
inference(cp,[status(thm)],[t89,t197]) ).
cnf(t1064,plain,
meet(sF4,meet(sF5,X1)) = meet(sF4,X1),
inference(orient,[status(thm)],[t199]) ).
cnf(t1069,plain,
meet(sF4,a) = meet(sF4,sF6),
inference(cp,[status(thm)],[t1064,t218]) ).
cnf(t1107,plain,
meet(sF4,a) = meet(sF4,sF6),
inference(orient,[status(thm)],[t1069]) ).
cnf(t1113,plain,
meet(sF1,a) = meet(sF1,meet(sF4,sF6)),
inference(cp,[status(thm)],[t712,t1107]) ).
cnf(t45,plain,
sF1 = meet(sF1,a),
inference(cp,[status(thm)],[t28,t43]) ).
cnf(t48,plain,
meet(sF1,a) = sF1,
inference(orient,[status(thm)],[t45]) ).
cnf(t21224,plain,
sF1 = meet(sF1,meet(sF4,sF6)),
inference(step,[status(thm)],[t1113,t48]) ).
cnf(t21225,plain,
sF1 = meet(sF1,sF6),
inference(step,[status(thm)],[t21224,t712]) ).
cnf(t1119,plain,
meet(sF1,sF6) = sF1,
inference(orient,[status(thm)],[t21225]) ).
cnf(t1123,plain,
sF6 = join(sF6,sF1),
inference(cp,[status(thm)],[t236,t1119]) ).
cnf(t21228,plain,
sF6 = join(sF1,sF6),
inference(step,[status(thm)],[t1123,t31]) ).
cnf(t1137,plain,
join(sF1,sF6) = sF6,
inference(orient,[status(thm)],[t21228]) ).
cnf(t1614,plain,
join(sF7,sF6) = join(sF0,sF6),
inference(cp,[status(thm)],[t1591,t1137]) ).
cnf(t21270,plain,
join(sF6,sF7) = join(sF0,sF6),
inference(step,[status(thm)],[t1614,t31]) ).
cnf(t21271,plain,
join(sF6,sF7) = sF6,
inference(step,[status(thm)],[t21270,t1057]) ).
cnf(t1709,plain,
join(sF6,sF7) = sF6,
inference(orient,[status(thm)],[t21271]) ).
cnf(t9586,plain,
join(sF5,sF6) = join(sF3,sF6),
inference(cp,[status(thm)],[t9579,t1709]) ).
cnf(t220,plain,
sF5 = join(sF5,sF6),
inference(cp,[status(thm)],[t23,t218]) ).
cnf(t223,plain,
join(sF5,sF6) = sF5,
inference(orient,[status(thm)],[t220]) ).
cnf(t21488,plain,
sF5 = join(sF3,sF6),
inference(step,[status(thm)],[t9586,t223]) ).
cnf(t9663,plain,
join(sF3,sF6) = sF5,
inference(orient,[status(thm)],[t21488]) ).
cnf(t21614,plain,
join(sF0,sF1) = sF6,
inference(step,[status(thm)],[t253,t21060]) ).
cnf(t21061,plain,
join(sF0,sF1) = sF6,
inference(orient,[status(thm)],[t21614]) ).
cnf(t249,plain,
a = join(a,sF6),
inference(cp,[status(thm)],[t236,t218]) ).
cnf(t21196,plain,
a = join(sF6,a),
inference(step,[status(thm)],[t249,t31]) ).
cnf(t273,plain,
join(sF6,a) = a,
inference(orient,[status(thm)],[t21196]) ).
cnf(t275,plain,
sF6 = meet(sF6,a),
inference(cp,[status(thm)],[t28,t273]) ).
cnf(t302,plain,
meet(sF6,a) = sF6,
inference(orient,[status(thm)],[t275]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(meet(a,b),join(meet(a,c),meet(c,join(a,b))))) != meet(a,join(meet(a,b),meet(a,c))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(meet(a,c),join(meet(c,join(a,b)),meet(a,b)))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[goal_0,t417]) ).
cnf(g0_1,plain,
meet(a,join(meet(a,c),join(meet(a,b),meet(c,join(a,b))))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_0,t18887]) ).
cnf(g0_2,plain,
meet(a,join(meet(c,a),join(meet(a,b),meet(c,join(a,b))))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_1,t60]) ).
cnf(g0_3,plain,
meet(a,join(sF1,join(meet(a,b),meet(c,join(a,b))))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_2,t72]) ).
cnf(g0_4,plain,
meet(a,join(sF1,join(meet(b,a),meet(c,join(a,b))))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_3,t60]) ).
cnf(g0_5,plain,
meet(a,join(sF1,join(sF0,meet(c,join(a,b))))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_4,t69]) ).
cnf(g0_6,plain,
meet(a,join(sF0,join(meet(c,join(a,b)),sF1))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_5,t417]) ).
cnf(g0_7,plain,
meet(a,join(meet(c,join(a,b)),sF6)) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_6,t21091]) ).
cnf(g0_8,plain,
meet(a,join(sF6,meet(c,join(a,b)))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_7,t31]) ).
cnf(g0_9,plain,
meet(a,join(sF6,meet(c,join(b,a)))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_8,t31]) ).
cnf(g0_10,plain,
meet(a,join(sF6,meet(c,sF2))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_9,t37]) ).
cnf(g0_11,plain,
meet(a,join(sF6,meet(sF2,c))) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_10,t60]) ).
cnf(g0_12,plain,
meet(a,join(sF6,sF3)) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_11,t139]) ).
cnf(g0_13,plain,
meet(a,join(sF3,sF6)) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_12,t31]) ).
cnf(g0_14,plain,
meet(a,sF5) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_13,t9663]) ).
cnf(g0_15,plain,
meet(sF5,a) != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_14,t60]) ).
cnf(g0_16,plain,
sF6 != meet(a,join(meet(a,b),meet(a,c))),
inference(rw,[status(thm)],[g0_15,t218]) ).
cnf(g0_17,plain,
sF6 != meet(a,join(meet(a,c),meet(a,b))),
inference(rw,[status(thm)],[g0_16,t31]) ).
cnf(g0_18,plain,
sF6 != meet(a,join(meet(c,a),meet(a,b))),
inference(rw,[status(thm)],[g0_17,t60]) ).
cnf(g0_19,plain,
sF6 != meet(a,join(sF1,meet(a,b))),
inference(rw,[status(thm)],[g0_18,t72]) ).
cnf(g0_20,plain,
sF6 != meet(a,join(sF1,meet(b,a))),
inference(rw,[status(thm)],[g0_19,t60]) ).
cnf(g0_21,plain,
sF6 != meet(a,join(sF1,sF0)),
inference(rw,[status(thm)],[g0_20,t69]) ).
cnf(g0_22,plain,
sF6 != meet(a,join(sF0,sF1)),
inference(rw,[status(thm)],[g0_21,t31]) ).
cnf(g0_23,plain,
sF6 != meet(a,sF6),
inference(rw,[status(thm)],[g0_22,t21061]) ).
cnf(g0_24,plain,
sF6 != meet(sF6,a),
inference(rw,[status(thm)],[g0_23,t60]) ).
cnf(g0_25,plain,
sF6 != sF6,
inference(rw,[status(thm)],[g0_24,t302]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT143-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.44 % Computer : n011.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Wed Sep 23 20:22:13 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 63.36/8.59 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.36/8.59 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------