%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP660-12 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n008.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:27:56 PM UTC 2026
% Result : Unsatisfiable 6.64s 6.59s
% Output : CNFRefutation 6.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 8
% Syntax : Number of clauses : 109 ( 109 unt; 0 nHn; 50 RR)
% Number of literals : 109 ( 108 equ; 3 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 : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 81 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
mult(mult(mult(X1,X2),X3),X1) = mult(X1,mult(X2,mult(X3,X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(mult(mult(X1,X2),X3),X1) = mult(X1,mult(X2,mult(X3,X1))),
inference(orient,[status(thm)],[t4]) ).
cnf(t6,axiom,
sFlat1 = mult(rd(x1,x1),x0),
introduced(definition) ).
cnf(t21,plain,
mult(rd(x1,x1),x0) = sFlat1,
inference(orient,[status(thm)],[t6]) ).
cnf(t5,axiom,
sFlat0 = rd(x1,x1),
introduced(definition) ).
cnf(t25,plain,
rd(x1,x1) = sFlat0,
inference(orient,[status(thm)],[t5]) ).
cnf(t1916,plain,
mult(sFlat0,x0) = sFlat1,
inference(step,[status(thm)],[t21,t25]) ).
cnf(t27,plain,
mult(sFlat0,x0) = sFlat1,
inference(rw,[status(thm)],[t1916]) ).
cnf(t31,plain,
mult(sFlat0,x0) = sFlat1,
inference(orient,[status(thm)],[t27]) ).
cnf(t34,plain,
mult(sFlat0,mult(x0,mult(X1,sFlat0))) = mult(mult(sFlat1,X1),sFlat0),
inference(cp,[status(thm)],[t13,t31]) ).
cnf(t46,plain,
mult(sFlat0,mult(x0,mult(X1,sFlat0))) = mult(mult(sFlat1,X1),sFlat0),
inference(orient,[status(thm)],[t34]) ).
cnf(t1,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t7,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t3,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t0,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t15,plain,
mult(X1,mult(ld(X1,X2),mult(X3,X1))) = mult(mult(X2,X3),X1),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t602,plain,
mult(X1,mult(ld(X1,X2),mult(X3,X1))) = mult(mult(X2,X3),X1),
inference(orient,[status(thm)],[t15]) ).
cnf(t673,plain,
mult(ld(X1,X2),mult(X3,X1)) = ld(X1,mult(mult(X2,X3),X1)),
inference(cp,[status(thm)],[t11,t602]) ).
cnf(t945,plain,
ld(X1,mult(mult(X2,X3),X1)) = mult(ld(X1,X2),mult(X3,X1)),
inference(orient,[status(thm)],[t673]) ).
cnf(t2,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t8,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t26,plain,
x1 = mult(sFlat0,x1),
inference(cp,[status(thm)],[t8,t25]) ).
cnf(t28,plain,
mult(sFlat0,x1) = x1,
inference(orient,[status(thm)],[t26]) ).
cnf(t989,plain,
mult(ld(X1,sFlat0),mult(x1,X1)) = ld(X1,mult(x1,X1)),
inference(cp,[status(thm)],[t945,t28]) ).
cnf(t1014,plain,
mult(ld(X1,sFlat0),mult(x1,X1)) = ld(X1,mult(x1,X1)),
inference(orient,[status(thm)],[t989]) ).
cnf(t1029,plain,
ld(X1,sFlat0) = rd(ld(X1,mult(x1,X1)),mult(x1,X1)),
inference(cp,[status(thm)],[t9,t1014]) ).
cnf(t1277,plain,
rd(ld(X1,mult(x1,X1)),mult(x1,X1)) = ld(X1,sFlat0),
inference(orient,[status(thm)],[t1029]) ).
cnf(t30,plain,
mult(sFlat0,mult(x1,mult(X1,sFlat0))) = mult(mult(x1,X1),sFlat0),
inference(cp,[status(thm)],[t13,t28]) ).
cnf(t40,plain,
mult(sFlat0,mult(x1,mult(X1,sFlat0))) = mult(mult(x1,X1),sFlat0),
inference(orient,[status(thm)],[t30]) ).
cnf(t42,plain,
mult(mult(x1,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,mult(x1,X1)),
inference(cp,[status(thm)],[t40,t8]) ).
cnf(t52,plain,
mult(mult(x1,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,mult(x1,X1)),
inference(orient,[status(thm)],[t42]) ).
cnf(t54,plain,
mult(x1,rd(X1,sFlat0)) = rd(mult(sFlat0,mult(x1,X1)),sFlat0),
inference(cp,[status(thm)],[t9,t52]) ).
cnf(t72,plain,
rd(mult(sFlat0,mult(x1,X1)),sFlat0) = mult(x1,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t54]) ).
cnf(t73,plain,
mult(x1,rd(ld(x1,X1),sFlat0)) = rd(mult(sFlat0,X1),sFlat0),
inference(cp,[status(thm)],[t72,t7]) ).
cnf(t91,plain,
mult(x1,rd(ld(x1,X1),sFlat0)) = rd(mult(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t73]) ).
cnf(t55,plain,
mult(x1,mult(rd(X1,sFlat0),mult(sFlat0,x1))) = mult(mult(sFlat0,mult(x1,X1)),x1),
inference(cp,[status(thm)],[t13,t52]) ).
cnf(t1917,plain,
mult(x1,mult(rd(X1,sFlat0),x1)) = mult(mult(sFlat0,mult(x1,X1)),x1),
inference(step,[status(thm)],[t55,t28]) ).
cnf(t198,plain,
mult(mult(sFlat0,mult(x1,X1)),x1) = mult(x1,mult(rd(X1,sFlat0),x1)),
inference(orient,[status(thm)],[t1917]) ).
cnf(t43,plain,
mult(x1,mult(X1,sFlat0)) = ld(sFlat0,mult(mult(x1,X1),sFlat0)),
inference(cp,[status(thm)],[t11,t40]) ).
cnf(t59,plain,
ld(sFlat0,mult(mult(x1,X1),sFlat0)) = mult(x1,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t43]) ).
cnf(t60,plain,
mult(x1,mult(ld(x1,X1),sFlat0)) = ld(sFlat0,mult(X1,sFlat0)),
inference(cp,[status(thm)],[t59,t7]) ).
cnf(t77,plain,
mult(x1,mult(ld(x1,X1),sFlat0)) = ld(sFlat0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t60]) ).
cnf(t199,plain,
mult(x1,mult(rd(mult(ld(x1,X1),sFlat0),sFlat0),x1)) = mult(mult(sFlat0,ld(sFlat0,mult(X1,sFlat0))),x1),
inference(cp,[status(thm)],[t198,t77]) ).
cnf(t1918,plain,
mult(x1,mult(ld(x1,X1),x1)) = mult(mult(sFlat0,ld(sFlat0,mult(X1,sFlat0))),x1),
inference(step,[status(thm)],[t199,t9]) ).
cnf(t1919,plain,
mult(x1,mult(ld(x1,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(step,[status(thm)],[t1918,t7]) ).
cnf(t206,plain,
mult(x1,mult(ld(x1,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(orient,[status(thm)],[t1919]) ).
cnf(t211,plain,
mult(ld(x1,X1),x1) = ld(x1,mult(mult(X1,sFlat0),x1)),
inference(cp,[status(thm)],[t11,t206]) ).
cnf(t217,plain,
ld(x1,mult(mult(X1,sFlat0),x1)) = mult(ld(x1,X1),x1),
inference(orient,[status(thm)],[t211]) ).
cnf(t224,plain,
mult(ld(x1,rd(X1,sFlat0)),x1) = ld(x1,mult(X1,x1)),
inference(cp,[status(thm)],[t217,t8]) ).
cnf(t259,plain,
mult(ld(x1,rd(X1,sFlat0)),x1) = ld(x1,mult(X1,x1)),
inference(orient,[status(thm)],[t224]) ).
cnf(t92,plain,
rd(ld(x1,X1),sFlat0) = ld(x1,rd(mult(sFlat0,X1),sFlat0)),
inference(cp,[status(thm)],[t11,t91]) ).
cnf(t137,plain,
ld(x1,rd(mult(sFlat0,X1),sFlat0)) = rd(ld(x1,X1),sFlat0),
inference(orient,[status(thm)],[t92]) ).
cnf(t140,plain,
rd(ld(x1,x1),sFlat0) = ld(x1,rd(x1,sFlat0)),
inference(cp,[status(thm)],[t137,t28]) ).
cnf(t145,plain,
ld(x1,rd(x1,sFlat0)) = rd(ld(x1,x1),sFlat0),
inference(orient,[status(thm)],[t140]) ).
cnf(t262,plain,
ld(x1,mult(x1,x1)) = mult(rd(ld(x1,x1),sFlat0),x1),
inference(cp,[status(thm)],[t259,t145]) ).
cnf(t1920,plain,
x1 = mult(rd(ld(x1,x1),sFlat0),x1),
inference(step,[status(thm)],[t262,t11]) ).
cnf(t272,plain,
mult(rd(ld(x1,x1),sFlat0),x1) = x1,
inference(orient,[status(thm)],[t1920]) ).
cnf(t274,plain,
rd(ld(x1,x1),sFlat0) = rd(x1,x1),
inference(cp,[status(thm)],[t9,t272]) ).
cnf(t1921,plain,
rd(ld(x1,x1),sFlat0) = sFlat0,
inference(step,[status(thm)],[t274,t25]) ).
cnf(t277,plain,
rd(ld(x1,x1),sFlat0) = sFlat0,
inference(orient,[status(thm)],[t1921]) ).
cnf(t281,plain,
ld(x1,x1) = mult(sFlat0,sFlat0),
inference(cp,[status(thm)],[t8,t277]) ).
cnf(t289,plain,
ld(x1,x1) = mult(sFlat0,sFlat0),
inference(orient,[status(thm)],[t281]) ).
cnf(t293,plain,
rd(mult(sFlat0,x1),sFlat0) = mult(x1,rd(mult(sFlat0,sFlat0),sFlat0)),
inference(cp,[status(thm)],[t91,t289]) ).
cnf(t1925,plain,
rd(x1,sFlat0) = mult(x1,rd(mult(sFlat0,sFlat0),sFlat0)),
inference(step,[status(thm)],[t293,t28]) ).
cnf(t1926,plain,
rd(x1,sFlat0) = mult(x1,sFlat0),
inference(step,[status(thm)],[t1925,t9]) ).
cnf(t295,plain,
mult(x1,sFlat0) = rd(x1,sFlat0),
inference(orient,[status(thm)],[t1926]) ).
cnf(t1280,plain,
ld(sFlat0,sFlat0) = rd(ld(sFlat0,rd(x1,sFlat0)),mult(x1,sFlat0)),
inference(cp,[status(thm)],[t1277,t295]) ).
cnf(t978,plain,
mult(ld(X1,x1),mult(sFlat0,X1)) = ld(X1,mult(rd(x1,sFlat0),X1)),
inference(cp,[status(thm)],[t945,t295]) ).
cnf(t1172,plain,
ld(X1,mult(rd(x1,sFlat0),X1)) = mult(ld(X1,x1),mult(sFlat0,X1)),
inference(orient,[status(thm)],[t978]) ).
cnf(t1173,plain,
mult(ld(rd(x1,sFlat0),x1),mult(sFlat0,rd(x1,sFlat0))) = rd(x1,sFlat0),
inference(cp,[status(thm)],[t1172,t11]) ).
cnf(t12,plain,
X1 = ld(rd(X2,X1),X2),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t39,plain,
ld(rd(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t1936,plain,
mult(sFlat0,mult(sFlat0,rd(x1,sFlat0))) = rd(x1,sFlat0),
inference(step,[status(thm)],[t1173,t39]) ).
cnf(t1189,plain,
mult(sFlat0,mult(sFlat0,rd(x1,sFlat0))) = rd(x1,sFlat0),
inference(orient,[status(thm)],[t1936]) ).
cnf(t1190,plain,
mult(sFlat0,rd(x1,sFlat0)) = ld(sFlat0,rd(x1,sFlat0)),
inference(cp,[status(thm)],[t11,t1189]) ).
cnf(t1198,plain,
ld(sFlat0,rd(x1,sFlat0)) = mult(sFlat0,rd(x1,sFlat0)),
inference(orient,[status(thm)],[t1190]) ).
cnf(t1943,plain,
ld(sFlat0,sFlat0) = rd(mult(sFlat0,rd(x1,sFlat0)),mult(x1,sFlat0)),
inference(step,[status(thm)],[t1280,t1198]) ).
cnf(t1944,plain,
ld(sFlat0,sFlat0) = rd(mult(sFlat0,rd(x1,sFlat0)),rd(x1,sFlat0)),
inference(step,[status(thm)],[t1943,t295]) ).
cnf(t1945,plain,
ld(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t1944,t9]) ).
cnf(t1301,plain,
ld(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t1945]) ).
cnf(t1304,plain,
sFlat0 = mult(sFlat0,sFlat0),
inference(cp,[status(thm)],[t7,t1301]) ).
cnf(t1310,plain,
mult(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t1304]) ).
cnf(t1325,plain,
mult(mult(sFlat1,sFlat0),sFlat0) = mult(sFlat0,mult(x0,sFlat0)),
inference(cp,[status(thm)],[t46,t1310]) ).
cnf(t1577,plain,
mult(mult(sFlat1,sFlat0),sFlat0) = mult(sFlat0,mult(x0,sFlat0)),
inference(orient,[status(thm)],[t1325]) ).
cnf(t1307,plain,
mult(mult(sFlat0,X1),sFlat0) = mult(sFlat0,mult(sFlat0,mult(X1,sFlat0))),
inference(cp,[status(thm)],[t602,t1301]) ).
cnf(t1720,plain,
mult(sFlat0,mult(sFlat0,mult(X1,sFlat0))) = mult(mult(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t1307]) ).
cnf(t1320,plain,
mult(mult(X1,sFlat0),sFlat0) = mult(sFlat0,mult(ld(sFlat0,X1),sFlat0)),
inference(cp,[status(thm)],[t602,t1310]) ).
cnf(t1759,plain,
mult(sFlat0,mult(ld(sFlat0,X1),sFlat0)) = mult(mult(X1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t1320]) ).
cnf(t1766,plain,
mult(mult(sFlat0,ld(sFlat0,X1)),sFlat0) = mult(sFlat0,mult(mult(X1,sFlat0),sFlat0)),
inference(cp,[status(thm)],[t1720,t1759]) ).
cnf(t2032,plain,
mult(X1,sFlat0) = mult(sFlat0,mult(mult(X1,sFlat0),sFlat0)),
inference(step,[status(thm)],[t1766,t7]) ).
cnf(t1775,plain,
mult(sFlat0,mult(mult(X1,sFlat0),sFlat0)) = mult(X1,sFlat0),
inference(orient,[status(thm)],[t2032]) ).
cnf(t1788,plain,
mult(rd(X1,sFlat0),sFlat0) = mult(sFlat0,mult(X1,sFlat0)),
inference(cp,[status(thm)],[t1775,t8]) ).
cnf(t2033,plain,
X1 = mult(sFlat0,mult(X1,sFlat0)),
inference(step,[status(thm)],[t1788,t8]) ).
cnf(t1802,plain,
mult(sFlat0,mult(X1,sFlat0)) = X1,
inference(orient,[status(thm)],[t2033]) ).
cnf(t2036,plain,
mult(mult(sFlat1,sFlat0),sFlat0) = x0,
inference(step,[status(thm)],[t1577,t1802]) ).
cnf(t1805,plain,
mult(mult(sFlat1,sFlat0),sFlat0) = x0,
inference(orient,[status(thm)],[t2036]) ).
cnf(t1808,plain,
mult(sFlat1,sFlat0) = mult(sFlat0,x0),
inference(cp,[status(thm)],[t1802,t1805]) ).
cnf(t2040,plain,
mult(sFlat1,sFlat0) = sFlat1,
inference(step,[status(thm)],[t1808,t31]) ).
cnf(t1836,plain,
mult(sFlat1,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t2040]) ).
cnf(t2041,plain,
mult(sFlat1,sFlat0) = x0,
inference(step,[status(thm)],[t1805,t1836]) ).
cnf(t2042,plain,
sFlat1 = x0,
inference(step,[status(thm)],[t2041,t1836]) ).
cnf(t1852,plain,
sFlat1 = x0,
inference(rw,[status(thm)],[t2042]) ).
cnf(t1853,plain,
x0 = sFlat1,
inference(orient,[status(thm)],[t1852]) ).
cnf(goal_0,negated_conjecture,
mult(rd(x1,x1),x0) != x0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
sFlat1 != x0,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_0,t1853]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP660-12 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.38 % Computer : n008.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Wed Sep 23 15:32:59 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.64/6.59 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.64/6.59 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------