%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP660-13 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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 9.63s 1.72s
% Output : CNFRefutation 9.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 8
% Syntax : Number of clauses : 129 ( 129 unt; 0 nHn; 76 RR)
% Number of literals : 129 ( 128 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 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 : 83 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t3,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t4,axiom,
mult(mult(mult(X1,X2),X3),X1) = mult(X1,mult(X2,mult(X3,X1))),
file('/export/starexec/sandbox/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(t17,plain,
mult(mult(X1,X2),X3) = rd(mult(X1,mult(X2,mult(X3,X1))),X1),
inference(cp,[status(thm)],[t11,t13]) ).
cnf(t1368,plain,
rd(mult(X1,mult(X2,mult(X3,X1))),X1) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t17]) ).
cnf(t2,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t1,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t7,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t0,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,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(t169,plain,
mult(X1,mult(ld(X1,X2),mult(X3,X1))) = mult(mult(X2,X3),X1),
inference(orient,[status(thm)],[t15]) ).
cnf(t201,plain,
mult(ld(X1,X2),mult(X3,X1)) = ld(X1,mult(mult(X2,X3),X1)),
inference(cp,[status(thm)],[t9,t169]) ).
cnf(t831,plain,
ld(X1,mult(mult(X2,X3),X1)) = mult(ld(X1,X2),mult(X3,X1)),
inference(orient,[status(thm)],[t201]) ).
cnf(t6,axiom,
sFlat1 = mult(x0,ld(x1,x1)),
introduced(definition) ).
cnf(t21,plain,
mult(x0,ld(x1,x1)) = sFlat1,
inference(orient,[status(thm)],[t6]) ).
cnf(t5,axiom,
sFlat0 = ld(x1,x1),
introduced(definition) ).
cnf(t25,plain,
ld(x1,x1) = sFlat0,
inference(orient,[status(thm)],[t5]) ).
cnf(t2066,plain,
mult(x0,sFlat0) = sFlat1,
inference(step,[status(thm)],[t21,t25]) ).
cnf(t27,plain,
mult(x0,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t2066]) ).
cnf(t31,plain,
mult(x0,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t27]) ).
cnf(t870,plain,
mult(ld(X1,x0),mult(sFlat0,X1)) = ld(X1,mult(sFlat1,X1)),
inference(cp,[status(thm)],[t831,t31]) ).
cnf(t897,plain,
mult(ld(X1,x0),mult(sFlat0,X1)) = ld(X1,mult(sFlat1,X1)),
inference(orient,[status(thm)],[t870]) ).
cnf(t26,plain,
x1 = mult(x1,sFlat0),
inference(cp,[status(thm)],[t7,t25]) ).
cnf(t28,plain,
mult(x1,sFlat0) = x1,
inference(orient,[status(thm)],[t26]) ).
cnf(t195,plain,
mult(mult(X1,x1),sFlat0) = mult(sFlat0,mult(ld(sFlat0,X1),x1)),
inference(cp,[status(thm)],[t169,t28]) ).
cnf(t222,plain,
mult(sFlat0,mult(ld(sFlat0,X1),x1)) = mult(mult(X1,x1),sFlat0),
inference(orient,[status(thm)],[t195]) ).
cnf(t228,plain,
mult(ld(sFlat0,X1),x1) = ld(sFlat0,mult(mult(X1,x1),sFlat0)),
inference(cp,[status(thm)],[t9,t222]) ).
cnf(t294,plain,
ld(sFlat0,mult(mult(X1,x1),sFlat0)) = mult(ld(sFlat0,X1),x1),
inference(orient,[status(thm)],[t228]) ).
cnf(t298,plain,
mult(ld(sFlat0,rd(X1,x1)),x1) = ld(sFlat0,mult(X1,sFlat0)),
inference(cp,[status(thm)],[t294,t8]) ).
cnf(t314,plain,
mult(ld(sFlat0,rd(X1,x1)),x1) = ld(sFlat0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t298]) ).
cnf(t317,plain,
ld(sFlat0,rd(X1,x1)) = rd(ld(sFlat0,mult(X1,sFlat0)),x1),
inference(cp,[status(thm)],[t11,t314]) ).
cnf(t376,plain,
rd(ld(sFlat0,mult(X1,sFlat0)),x1) = ld(sFlat0,rd(X1,x1)),
inference(orient,[status(thm)],[t317]) ).
cnf(t380,plain,
ld(sFlat0,rd(x1,x1)) = rd(ld(sFlat0,x1),x1),
inference(cp,[status(thm)],[t376,t28]) ).
cnf(t30,plain,
mult(x1,mult(sFlat0,mult(X1,x1))) = mult(mult(x1,X1),x1),
inference(cp,[status(thm)],[t13,t28]) ).
cnf(t40,plain,
mult(x1,mult(sFlat0,mult(X1,x1))) = mult(mult(x1,X1),x1),
inference(orient,[status(thm)],[t30]) ).
cnf(t44,plain,
mult(sFlat0,mult(X1,x1)) = ld(x1,mult(mult(x1,X1),x1)),
inference(cp,[status(thm)],[t9,t40]) ).
cnf(t58,plain,
ld(x1,mult(mult(x1,X1),x1)) = mult(sFlat0,mult(X1,x1)),
inference(orient,[status(thm)],[t44]) ).
cnf(t59,plain,
mult(sFlat0,mult(sFlat0,x1)) = ld(x1,mult(x1,x1)),
inference(cp,[status(thm)],[t58,t28]) ).
cnf(t2067,plain,
mult(sFlat0,mult(sFlat0,x1)) = x1,
inference(step,[status(thm)],[t59,t9]) ).
cnf(t63,plain,
mult(sFlat0,mult(sFlat0,x1)) = x1,
inference(orient,[status(thm)],[t2067]) ).
cnf(t65,plain,
mult(sFlat0,x1) = ld(sFlat0,x1),
inference(cp,[status(thm)],[t9,t63]) ).
cnf(t67,plain,
ld(sFlat0,x1) = mult(sFlat0,x1),
inference(orient,[status(thm)],[t65]) ).
cnf(t2069,plain,
ld(sFlat0,rd(x1,x1)) = rd(mult(sFlat0,x1),x1),
inference(step,[status(thm)],[t380,t67]) ).
cnf(t2070,plain,
ld(sFlat0,rd(x1,x1)) = sFlat0,
inference(step,[status(thm)],[t2069,t11]) ).
cnf(t388,plain,
ld(sFlat0,rd(x1,x1)) = sFlat0,
inference(orient,[status(thm)],[t2070]) ).
cnf(t389,plain,
rd(x1,x1) = mult(sFlat0,sFlat0),
inference(cp,[status(thm)],[t7,t388]) ).
cnf(t395,plain,
mult(sFlat0,sFlat0) = rd(x1,x1),
inference(orient,[status(thm)],[t389]) ).
cnf(t901,plain,
ld(sFlat0,mult(sFlat1,sFlat0)) = mult(ld(sFlat0,x0),rd(x1,x1)),
inference(cp,[status(thm)],[t897,t395]) ).
cnf(t969,plain,
mult(ld(sFlat0,x0),rd(x1,x1)) = ld(sFlat0,mult(sFlat1,sFlat0)),
inference(orient,[status(thm)],[t901]) ).
cnf(t382,plain,
ld(sFlat0,rd(rd(X1,sFlat0),x1)) = rd(ld(sFlat0,X1),x1),
inference(cp,[status(thm)],[t376,t8]) ).
cnf(t440,plain,
ld(sFlat0,rd(rd(X1,sFlat0),x1)) = rd(ld(sFlat0,X1),x1),
inference(orient,[status(thm)],[t382]) ).
cnf(t441,plain,
rd(rd(X1,sFlat0),x1) = mult(sFlat0,rd(ld(sFlat0,X1),x1)),
inference(cp,[status(thm)],[t7,t440]) ).
cnf(t482,plain,
mult(sFlat0,rd(ld(sFlat0,X1),x1)) = rd(rd(X1,sFlat0),x1),
inference(orient,[status(thm)],[t441]) ).
cnf(t495,plain,
rd(rd(mult(sFlat0,X1),sFlat0),x1) = mult(sFlat0,rd(X1,x1)),
inference(cp,[status(thm)],[t482,t9]) ).
cnf(t521,plain,
rd(rd(mult(sFlat0,X1),sFlat0),x1) = mult(sFlat0,rd(X1,x1)),
inference(orient,[status(thm)],[t495]) ).
cnf(t535,plain,
rd(mult(sFlat0,X1),sFlat0) = mult(mult(sFlat0,rd(X1,x1)),x1),
inference(cp,[status(thm)],[t8,t521]) ).
cnf(t546,plain,
mult(mult(sFlat0,rd(X1,x1)),x1) = rd(mult(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t535]) ).
cnf(t199,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(X3,mult(ld(X3,X1),X2)),
inference(cp,[status(thm)],[t169,t8]) ).
cnf(t575,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(X3,mult(ld(X3,X1),X2)),
inference(orient,[status(thm)],[t199]) ).
cnf(t2071,plain,
mult(x1,mult(ld(x1,sFlat0),X1)) = rd(mult(sFlat0,X1),sFlat0),
inference(step,[status(thm)],[t546,t575]) ).
cnf(t623,plain,
mult(x1,mult(ld(x1,sFlat0),X1)) = rd(mult(sFlat0,X1),sFlat0),
inference(rw,[status(thm)],[t2071]) ).
cnf(t654,plain,
mult(x1,mult(ld(x1,sFlat0),X1)) = rd(mult(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t623]) ).
cnf(t655,plain,
rd(mult(sFlat0,ld(ld(x1,sFlat0),X1)),sFlat0) = mult(x1,X1),
inference(cp,[status(thm)],[t654,t7]) ).
cnf(t1356,plain,
rd(mult(sFlat0,ld(ld(x1,sFlat0),X1)),sFlat0) = mult(x1,X1),
inference(orient,[status(thm)],[t655]) ).
cnf(t1360,plain,
mult(sFlat0,ld(ld(x1,sFlat0),X1)) = mult(mult(x1,X1),sFlat0),
inference(cp,[status(thm)],[t8,t1356]) ).
cnf(t1464,plain,
mult(sFlat0,ld(ld(x1,sFlat0),X1)) = mult(mult(x1,X1),sFlat0),
inference(orient,[status(thm)],[t1360]) ).
cnf(t1470,plain,
ld(ld(x1,sFlat0),X1) = ld(sFlat0,mult(mult(x1,X1),sFlat0)),
inference(cp,[status(thm)],[t9,t1464]) ).
cnf(t2091,plain,
ld(ld(x1,sFlat0),X1) = mult(ld(sFlat0,x1),mult(X1,sFlat0)),
inference(step,[status(thm)],[t1470,t831]) ).
cnf(t2092,plain,
ld(ld(x1,sFlat0),X1) = mult(mult(sFlat0,x1),mult(X1,sFlat0)),
inference(step,[status(thm)],[t2091,t67]) ).
cnf(t1481,plain,
mult(mult(sFlat0,x1),mult(X1,sFlat0)) = ld(ld(x1,sFlat0),X1),
inference(orient,[status(thm)],[t2092]) ).
cnf(t378,plain,
ld(sFlat0,rd(sFlat0,x1)) = rd(sFlat0,x1),
inference(cp,[status(thm)],[t376,t9]) ).
cnf(t404,plain,
ld(sFlat0,rd(sFlat0,x1)) = rd(sFlat0,x1),
inference(orient,[status(thm)],[t378]) ).
cnf(t405,plain,
rd(sFlat0,x1) = mult(sFlat0,rd(sFlat0,x1)),
inference(cp,[status(thm)],[t7,t404]) ).
cnf(t411,plain,
mult(sFlat0,rd(sFlat0,x1)) = rd(sFlat0,x1),
inference(orient,[status(thm)],[t405]) ).
cnf(t580,plain,
mult(x1,mult(ld(x1,sFlat0),sFlat0)) = mult(rd(sFlat0,x1),x1),
inference(cp,[status(thm)],[t575,t411]) ).
cnf(t2072,plain,
mult(x1,mult(ld(x1,sFlat0),sFlat0)) = sFlat0,
inference(step,[status(thm)],[t580,t8]) ).
cnf(t624,plain,
mult(x1,mult(ld(x1,sFlat0),sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t2072]) ).
cnf(t626,plain,
mult(ld(x1,sFlat0),sFlat0) = ld(x1,sFlat0),
inference(cp,[status(thm)],[t9,t624]) ).
cnf(t632,plain,
mult(ld(x1,sFlat0),sFlat0) = ld(x1,sFlat0),
inference(orient,[status(thm)],[t626]) ).
cnf(t1486,plain,
ld(ld(x1,sFlat0),ld(x1,sFlat0)) = mult(mult(sFlat0,x1),ld(x1,sFlat0)),
inference(cp,[status(thm)],[t1481,t632]) ).
cnf(t634,plain,
sFlat0 = ld(ld(x1,sFlat0),ld(x1,sFlat0)),
inference(cp,[status(thm)],[t9,t632]) ).
cnf(t645,plain,
ld(ld(x1,sFlat0),ld(x1,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t634]) ).
cnf(t2093,plain,
sFlat0 = mult(mult(sFlat0,x1),ld(x1,sFlat0)),
inference(step,[status(thm)],[t1486,t645]) ).
cnf(t1498,plain,
mult(mult(sFlat0,x1),ld(x1,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t2093]) ).
cnf(t1499,plain,
mult(sFlat0,x1) = rd(sFlat0,ld(x1,sFlat0)),
inference(cp,[status(thm)],[t11,t1498]) ).
cnf(t12,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t11,t7]) ).
cnf(t39,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t2094,plain,
mult(sFlat0,x1) = x1,
inference(step,[status(thm)],[t1499,t39]) ).
cnf(t1507,plain,
mult(sFlat0,x1) = x1,
inference(orient,[status(thm)],[t2094]) ).
cnf(t1519,plain,
sFlat0 = rd(x1,x1),
inference(cp,[status(thm)],[t11,t1507]) ).
cnf(t1549,plain,
rd(x1,x1) = sFlat0,
inference(orient,[status(thm)],[t1519]) ).
cnf(t2129,plain,
mult(ld(sFlat0,x0),sFlat0) = ld(sFlat0,mult(sFlat1,sFlat0)),
inference(step,[status(thm)],[t969,t1549]) ).
cnf(t1561,plain,
mult(ld(sFlat0,x0),sFlat0) = ld(sFlat0,mult(sFlat1,sFlat0)),
inference(rw,[status(thm)],[t2129]) ).
cnf(t1738,plain,
ld(sFlat0,mult(sFlat1,sFlat0)) = mult(ld(sFlat0,x0),sFlat0),
inference(orient,[status(thm)],[t1561]) ).
cnf(t1739,plain,
mult(sFlat1,sFlat0) = mult(sFlat0,mult(ld(sFlat0,x0),sFlat0)),
inference(cp,[status(thm)],[t7,t1738]) ).
cnf(t1881,plain,
mult(sFlat0,mult(ld(sFlat0,x0),sFlat0)) = mult(sFlat1,sFlat0),
inference(orient,[status(thm)],[t1739]) ).
cnf(t1894,plain,
mult(mult(sFlat0,sFlat0),ld(sFlat0,x0)) = rd(mult(sFlat0,mult(sFlat1,sFlat0)),sFlat0),
inference(cp,[status(thm)],[t1368,t1881]) ).
cnf(t2125,plain,
mult(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t395,t1549]) ).
cnf(t1550,plain,
mult(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t2125]) ).
cnf(t2203,plain,
mult(sFlat0,ld(sFlat0,x0)) = rd(mult(sFlat0,mult(sFlat1,sFlat0)),sFlat0),
inference(step,[status(thm)],[t1894,t1550]) ).
cnf(t2204,plain,
x0 = rd(mult(sFlat0,mult(sFlat1,sFlat0)),sFlat0),
inference(step,[status(thm)],[t2203,t7]) ).
cnf(t1897,plain,
rd(mult(sFlat0,mult(sFlat1,sFlat0)),sFlat0) = x0,
inference(orient,[status(thm)],[t2204]) ).
cnf(t1899,plain,
mult(sFlat0,mult(sFlat1,sFlat0)) = mult(x0,sFlat0),
inference(cp,[status(thm)],[t8,t1897]) ).
cnf(t2205,plain,
mult(sFlat0,mult(sFlat1,sFlat0)) = sFlat1,
inference(step,[status(thm)],[t1899,t31]) ).
cnf(t1908,plain,
mult(sFlat0,mult(sFlat1,sFlat0)) = sFlat1,
inference(orient,[status(thm)],[t2205]) ).
cnf(t1922,plain,
mult(mult(sFlat0,sFlat0),sFlat1) = rd(mult(sFlat0,sFlat1),sFlat0),
inference(cp,[status(thm)],[t1368,t1908]) ).
cnf(t2212,plain,
mult(sFlat0,sFlat1) = rd(mult(sFlat0,sFlat1),sFlat0),
inference(step,[status(thm)],[t1922,t1550]) ).
cnf(t1945,plain,
rd(mult(sFlat0,sFlat1),sFlat0) = mult(sFlat0,sFlat1),
inference(orient,[status(thm)],[t2212]) ).
cnf(t1947,plain,
mult(sFlat0,sFlat1) = mult(mult(sFlat0,sFlat1),sFlat0),
inference(cp,[status(thm)],[t8,t1945]) ).
cnf(t1956,plain,
mult(mult(sFlat0,sFlat1),sFlat0) = mult(sFlat0,sFlat1),
inference(orient,[status(thm)],[t1947]) ).
cnf(t1958,plain,
mult(sFlat0,mult(sFlat1,mult(sFlat0,sFlat0))) = mult(mult(sFlat0,sFlat1),sFlat0),
inference(cp,[status(thm)],[t13,t1956]) ).
cnf(t2213,plain,
mult(sFlat0,mult(sFlat1,sFlat0)) = mult(mult(sFlat0,sFlat1),sFlat0),
inference(step,[status(thm)],[t1958,t1550]) ).
cnf(t2214,plain,
sFlat1 = mult(mult(sFlat0,sFlat1),sFlat0),
inference(step,[status(thm)],[t2213,t1908]) ).
cnf(t2215,plain,
sFlat1 = mult(sFlat0,sFlat1),
inference(step,[status(thm)],[t2214,t1956]) ).
cnf(t1967,plain,
mult(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t2215]) ).
cnf(t2222,plain,
rd(sFlat1,sFlat0) = mult(sFlat0,sFlat1),
inference(step,[status(thm)],[t1945,t1967]) ).
cnf(t32,plain,
x0 = rd(sFlat1,sFlat0),
inference(cp,[status(thm)],[t11,t31]) ).
cnf(t36,plain,
rd(sFlat1,sFlat0) = x0,
inference(orient,[status(thm)],[t32]) ).
cnf(t2223,plain,
x0 = mult(sFlat0,sFlat1),
inference(step,[status(thm)],[t2222,t36]) ).
cnf(t2224,plain,
x0 = sFlat1,
inference(step,[status(thm)],[t2223,t1967]) ).
cnf(t1988,plain,
x0 = sFlat1,
inference(rw,[status(thm)],[t2224]) ).
cnf(t1989,plain,
x0 = sFlat1,
inference(orient,[status(thm)],[t1988]) ).
cnf(goal_0,negated_conjecture,
mult(x0,ld(x1,x1)) != x0,
file('/export/starexec/sandbox/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,t1989]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP660-13 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n005.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.02/0.36 % CPULimit : 300
% 0.02/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Wed Sep 23 15:32:02 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.63/1.72 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.63/1.72 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------