%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT026-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.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:02 PM UTC 2026
% Result : Unsatisfiable 6.98s 1.78s
% Output : CNFRefutation 6.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 11
% Syntax : Number of clauses : 143 ( 143 unt; 0 nHn; 97 RR)
% Number of literals : 143 ( 142 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 90 ( 58 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t3,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t7,axiom,
sFlat0 = meet(a,b),
introduced(definition) ).
cnf(t2212,plain,
sFlat0 = meet(b,a),
inference(step,[status(thm)],[t7,t32]) ).
cnf(t45,plain,
meet(b,a) = sFlat0,
inference(orient,[status(thm)],[t2212]) ).
cnf(t8,axiom,
sFlat1 = meet(meet(a,b),c),
introduced(definition) ).
cnf(t2206,plain,
sFlat1 = meet(c,meet(a,b)),
inference(step,[status(thm)],[t8,t32]) ).
cnf(t2207,plain,
sFlat1 = meet(c,meet(b,a)),
inference(step,[status(thm)],[t2206,t32]) ).
cnf(t36,plain,
meet(c,meet(b,a)) = sFlat1,
inference(orient,[status(thm)],[t2207]) ).
cnf(t2213,plain,
meet(c,sFlat0) = sFlat1,
inference(step,[status(thm)],[t36,t45]) ).
cnf(t48,plain,
meet(c,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t2213]) ).
cnf(t2214,plain,
meet(sFlat0,c) = sFlat1,
inference(step,[status(thm)],[t48,t32]) ).
cnf(t53,plain,
meet(sFlat0,c) = sFlat1,
inference(orient,[status(thm)],[t2214]) ).
cnf(t9,axiom,
sFlat2 = meet(b,c),
introduced(definition) ).
cnf(t2208,plain,
sFlat2 = meet(c,b),
inference(step,[status(thm)],[t9,t32]) ).
cnf(t39,plain,
meet(c,b) = sFlat2,
inference(orient,[status(thm)],[t2208]) ).
cnf(t10,axiom,
sFlat3 = meet(a,meet(b,c)),
introduced(definition) ).
cnf(t2209,plain,
sFlat3 = meet(a,meet(c,b)),
inference(step,[status(thm)],[t10,t32]) ).
cnf(t2210,plain,
sFlat3 = meet(a,sFlat2),
inference(step,[status(thm)],[t2209,t39]) ).
cnf(t2211,plain,
sFlat3 = meet(sFlat2,a),
inference(step,[status(thm)],[t2210,t32]) ).
cnf(t42,plain,
meet(sFlat2,a) = sFlat3,
inference(orient,[status(thm)],[t2211]) ).
cnf(t6,axiom,
meet(meet(join(X1,X2),join(X3,X2)),X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
meet(meet(join(X1,X2),join(X3,X2)),X2) = X2,
inference(orient,[status(thm)],[t6]) ).
cnf(t35,plain,
meet(meet(join(X1,X2),join(X3,X2)),X2) = X2,
inference(rw,[status(thm)],[t13]) ).
cnf(t2215,plain,
meet(X2,meet(join(X1,X2),join(X3,X2))) = X2,
inference(step,[status(thm)],[t35,t32]) ).
cnf(t62,plain,
meet(X1,meet(join(X2,X1),join(X3,X1))) = X1,
inference(orient,[status(thm)],[t2215]) ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t49,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t63,plain,
X1 = meet(X1,meet(join(X1,X2),join(X3,X1))),
inference(cp,[status(thm)],[t62,t49]) ).
cnf(t268,plain,
meet(X1,meet(join(X1,X2),join(X3,X1))) = X1,
inference(orient,[status(thm)],[t63]) ).
cnf(t5,axiom,
join(join(meet(X1,X2),meet(X3,X2)),X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
join(join(meet(X1,X2),meet(X3,X2)),X2) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t52,plain,
join(join(meet(X1,X2),meet(X3,X2)),X2) = X2,
inference(rw,[status(thm)],[t20]) ).
cnf(t2216,plain,
join(X2,join(meet(X1,X2),meet(X3,X2))) = X2,
inference(step,[status(thm)],[t52,t49]) ).
cnf(t66,plain,
join(X1,join(meet(X2,X1),meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t2216]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t67,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t66,t15]) ).
cnf(t101,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t67]) ).
cnf(t4,axiom,
meet(X1,join(X2,join(X1,X3))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t12,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t50,plain,
X1 = meet(X1,join(join(X1,X2),X3)),
inference(cp,[status(thm)],[t12,t49]) ).
cnf(t57,plain,
meet(X1,join(join(X1,X2),X3)) = X1,
inference(orient,[status(thm)],[t50]) ).
cnf(t58,plain,
X1 = meet(X1,join(join(X2,X1),X3)),
inference(cp,[status(thm)],[t57,t49]) ).
cnf(t61,plain,
meet(X1,join(join(X2,X1),X3)) = X1,
inference(orient,[status(thm)],[t58]) ).
cnf(t113,plain,
X1 = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t101,t32]) ).
cnf(t155,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t113]) ).
cnf(t156,plain,
sFlat0 = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t155,t53]) ).
cnf(t165,plain,
join(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t156]) ).
cnf(t169,plain,
sFlat1 = meet(sFlat1,join(sFlat0,X1)),
inference(cp,[status(thm)],[t61,t165]) ).
cnf(t235,plain,
meet(sFlat1,join(sFlat0,X1)) = sFlat1,
inference(orient,[status(thm)],[t169]) ).
cnf(t110,plain,
a = join(a,sFlat0),
inference(cp,[status(thm)],[t101,t45]) ).
cnf(t2218,plain,
a = join(sFlat0,a),
inference(step,[status(thm)],[t110,t49]) ).
cnf(t124,plain,
join(sFlat0,a) = a,
inference(orient,[status(thm)],[t2218]) ).
cnf(t237,plain,
sFlat1 = meet(sFlat1,a),
inference(cp,[status(thm)],[t235,t124]) ).
cnf(t251,plain,
meet(sFlat1,a) = sFlat1,
inference(orient,[status(thm)],[t237]) ).
cnf(t252,plain,
a = join(a,sFlat1),
inference(cp,[status(thm)],[t101,t251]) ).
cnf(t2226,plain,
a = join(sFlat1,a),
inference(step,[status(thm)],[t252,t49]) ).
cnf(t259,plain,
join(sFlat1,a) = a,
inference(orient,[status(thm)],[t2226]) ).
cnf(t275,plain,
sFlat1 = meet(sFlat1,meet(a,join(X1,sFlat1))),
inference(cp,[status(thm)],[t268,t259]) ).
cnf(t987,plain,
meet(sFlat1,meet(a,join(X1,sFlat1))) = sFlat1,
inference(orient,[status(thm)],[t275]) ).
cnf(t990,plain,
sFlat1 = meet(sFlat1,meet(a,join(sFlat1,X1))),
inference(cp,[status(thm)],[t987,t49]) ).
cnf(t2103,plain,
meet(sFlat1,meet(a,join(sFlat1,X1))) = sFlat1,
inference(orient,[status(thm)],[t990]) ).
cnf(t109,plain,
c = join(c,sFlat1),
inference(cp,[status(thm)],[t101,t53]) ).
cnf(t2217,plain,
c = join(sFlat1,c),
inference(step,[status(thm)],[t109,t49]) ).
cnf(t119,plain,
join(sFlat1,c) = c,
inference(orient,[status(thm)],[t2217]) ).
cnf(t276,plain,
sFlat1 = meet(sFlat1,meet(c,join(X1,sFlat1))),
inference(cp,[status(thm)],[t268,t119]) ).
cnf(t995,plain,
meet(sFlat1,meet(c,join(X1,sFlat1))) = sFlat1,
inference(orient,[status(thm)],[t276]) ).
cnf(t998,plain,
sFlat1 = meet(sFlat1,meet(c,join(sFlat1,X1))),
inference(cp,[status(thm)],[t995,t49]) ).
cnf(t2136,plain,
meet(sFlat1,meet(c,join(sFlat1,X1))) = sFlat1,
inference(orient,[status(thm)],[t998]) ).
cnf(t157,plain,
b = join(b,sFlat0),
inference(cp,[status(thm)],[t155,t45]) ).
cnf(t2221,plain,
b = join(sFlat0,b),
inference(step,[status(thm)],[t157,t49]) ).
cnf(t171,plain,
join(sFlat0,b) = b,
inference(orient,[status(thm)],[t2221]) ).
cnf(t236,plain,
sFlat1 = meet(sFlat1,b),
inference(cp,[status(thm)],[t235,t171]) ).
cnf(t247,plain,
meet(sFlat1,b) = sFlat1,
inference(orient,[status(thm)],[t236]) ).
cnf(t248,plain,
b = join(b,sFlat1),
inference(cp,[status(thm)],[t101,t247]) ).
cnf(t2225,plain,
b = join(sFlat1,b),
inference(step,[status(thm)],[t248,t49]) ).
cnf(t255,plain,
join(sFlat1,b) = b,
inference(orient,[status(thm)],[t2225]) ).
cnf(t2144,plain,
sFlat1 = meet(sFlat1,meet(c,b)),
inference(cp,[status(thm)],[t2136,t255]) ).
cnf(t2303,plain,
sFlat1 = meet(sFlat1,sFlat2),
inference(step,[status(thm)],[t2144,t39]) ).
cnf(t2153,plain,
meet(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t2303]) ).
cnf(t2155,plain,
sFlat2 = join(sFlat2,sFlat1),
inference(cp,[status(thm)],[t101,t2153]) ).
cnf(t2307,plain,
sFlat2 = join(sFlat1,sFlat2),
inference(step,[status(thm)],[t2155,t49]) ).
cnf(t2160,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t2307]) ).
cnf(t2167,plain,
sFlat1 = meet(sFlat1,meet(a,sFlat2)),
inference(cp,[status(thm)],[t2103,t2160]) ).
cnf(t2314,plain,
sFlat1 = meet(sFlat1,meet(sFlat2,a)),
inference(step,[status(thm)],[t2167,t32]) ).
cnf(t2315,plain,
sFlat1 = meet(sFlat1,sFlat3),
inference(step,[status(thm)],[t2314,t42]) ).
cnf(t158,plain,
sFlat2 = join(sFlat2,sFlat3),
inference(cp,[status(thm)],[t155,t42]) ).
cnf(t176,plain,
join(sFlat2,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t158]) ).
cnf(t180,plain,
sFlat3 = meet(sFlat3,join(sFlat2,X1)),
inference(cp,[status(thm)],[t61,t176]) ).
cnf(t305,plain,
meet(sFlat3,join(sFlat2,X1)) = sFlat3,
inference(orient,[status(thm)],[t180]) ).
cnf(t159,plain,
c = join(c,sFlat2),
inference(cp,[status(thm)],[t155,t39]) ).
cnf(t2222,plain,
c = join(sFlat2,c),
inference(step,[status(thm)],[t159,t49]) ).
cnf(t182,plain,
join(sFlat2,c) = c,
inference(orient,[status(thm)],[t2222]) ).
cnf(t306,plain,
sFlat3 = meet(sFlat3,c),
inference(cp,[status(thm)],[t305,t182]) ).
cnf(t317,plain,
meet(sFlat3,c) = sFlat3,
inference(orient,[status(thm)],[t306]) ).
cnf(t318,plain,
c = join(c,sFlat3),
inference(cp,[status(thm)],[t101,t317]) ).
cnf(t2227,plain,
c = join(sFlat3,c),
inference(step,[status(thm)],[t318,t49]) ).
cnf(t325,plain,
join(sFlat3,c) = c,
inference(orient,[status(thm)],[t2227]) ).
cnf(t327,plain,
sFlat3 = meet(sFlat3,meet(c,join(X1,sFlat3))),
inference(cp,[status(thm)],[t268,t325]) ).
cnf(t1086,plain,
meet(sFlat3,meet(c,join(X1,sFlat3))) = sFlat3,
inference(orient,[status(thm)],[t327]) ).
cnf(t111,plain,
a = join(a,sFlat3),
inference(cp,[status(thm)],[t101,t42]) ).
cnf(t2219,plain,
a = join(sFlat3,a),
inference(step,[status(thm)],[t111,t49]) ).
cnf(t129,plain,
join(sFlat3,a) = a,
inference(orient,[status(thm)],[t2219]) ).
cnf(t272,plain,
sFlat3 = meet(sFlat3,meet(a,join(X1,sFlat3))),
inference(cp,[status(thm)],[t268,t129]) ).
cnf(t965,plain,
meet(sFlat3,meet(a,join(X1,sFlat3))) = sFlat3,
inference(orient,[status(thm)],[t272]) ).
cnf(t968,plain,
sFlat3 = meet(sFlat3,meet(a,join(sFlat3,X1))),
inference(cp,[status(thm)],[t965,t49]) ).
cnf(t1712,plain,
meet(sFlat3,meet(a,join(sFlat3,X1))) = sFlat3,
inference(orient,[status(thm)],[t968]) ).
cnf(t112,plain,
b = join(b,sFlat2),
inference(cp,[status(thm)],[t101,t39]) ).
cnf(t2220,plain,
b = join(sFlat2,b),
inference(step,[status(thm)],[t112,t49]) ).
cnf(t134,plain,
join(sFlat2,b) = b,
inference(orient,[status(thm)],[t2220]) ).
cnf(t307,plain,
sFlat3 = meet(sFlat3,b),
inference(cp,[status(thm)],[t305,t134]) ).
cnf(t321,plain,
meet(sFlat3,b) = sFlat3,
inference(orient,[status(thm)],[t307]) ).
cnf(t322,plain,
b = join(b,sFlat3),
inference(cp,[status(thm)],[t101,t321]) ).
cnf(t2228,plain,
b = join(sFlat3,b),
inference(step,[status(thm)],[t322,t49]) ).
cnf(t331,plain,
join(sFlat3,b) = b,
inference(orient,[status(thm)],[t2228]) ).
cnf(t1719,plain,
sFlat3 = meet(sFlat3,meet(a,b)),
inference(cp,[status(thm)],[t1712,t331]) ).
cnf(t2270,plain,
sFlat3 = meet(sFlat3,meet(b,a)),
inference(step,[status(thm)],[t1719,t32]) ).
cnf(t2271,plain,
sFlat3 = meet(sFlat3,sFlat0),
inference(step,[status(thm)],[t2270,t45]) ).
cnf(t2272,plain,
sFlat3 = meet(sFlat0,sFlat3),
inference(step,[status(thm)],[t2271,t32]) ).
cnf(t1729,plain,
meet(sFlat0,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t2272]) ).
cnf(t1730,plain,
sFlat0 = join(sFlat0,sFlat3),
inference(cp,[status(thm)],[t155,t1729]) ).
cnf(t1732,plain,
join(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t1730]) ).
cnf(t1738,plain,
sFlat3 = meet(sFlat3,meet(c,sFlat0)),
inference(cp,[status(thm)],[t1086,t1732]) ).
cnf(t2280,plain,
sFlat3 = meet(sFlat3,meet(sFlat0,c)),
inference(step,[status(thm)],[t1738,t32]) ).
cnf(t2281,plain,
sFlat3 = meet(sFlat3,sFlat1),
inference(step,[status(thm)],[t2280,t53]) ).
cnf(t2282,plain,
sFlat3 = meet(sFlat1,sFlat3),
inference(step,[status(thm)],[t2281,t32]) ).
cnf(t1759,plain,
meet(sFlat1,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t2282]) ).
cnf(t2316,plain,
sFlat1 = sFlat3,
inference(step,[status(thm)],[t2315,t1759]) ).
cnf(t2190,plain,
sFlat3 = sFlat1,
inference(orient,[status(thm)],[t2316]) ).
cnf(t2317,plain,
meet(sFlat2,a) = sFlat1,
inference(step,[status(thm)],[t42,t2190]) ).
cnf(t2191,plain,
meet(sFlat2,a) = sFlat1,
inference(orient,[status(thm)],[t2317]) ).
cnf(goal_0,negated_conjecture,
meet(meet(a,b),c) != meet(a,meet(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(c,meet(a,b)) != meet(a,meet(b,c)),
inference(rw,[status(thm)],[goal_0,t32]) ).
cnf(g0_1,plain,
meet(c,meet(b,a)) != meet(a,meet(b,c)),
inference(rw,[status(thm)],[g0_0,t32]) ).
cnf(g0_2,plain,
meet(c,sFlat0) != meet(a,meet(b,c)),
inference(rw,[status(thm)],[g0_1,t45]) ).
cnf(g0_3,plain,
meet(sFlat0,c) != meet(a,meet(b,c)),
inference(rw,[status(thm)],[g0_2,t32]) ).
cnf(g0_4,plain,
sFlat1 != meet(a,meet(b,c)),
inference(rw,[status(thm)],[g0_3,t53]) ).
cnf(g0_5,plain,
sFlat1 != meet(a,meet(c,b)),
inference(rw,[status(thm)],[g0_4,t32]) ).
cnf(g0_6,plain,
sFlat1 != meet(a,sFlat2),
inference(rw,[status(thm)],[g0_5,t39]) ).
cnf(g0_7,plain,
sFlat1 != meet(sFlat2,a),
inference(rw,[status(thm)],[g0_6,t32]) ).
cnf(g0_8,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_7,t2191]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT026-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 20:03:14 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.98/1.78 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.98/1.78 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------