%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP660-11 : 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 8.09s 1.90s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 8
% Syntax : Number of clauses : 123 ( 123 unt; 0 nHn; 70 RR)
% Number of literals : 123 ( 122 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 : 75 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(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(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(t15,plain,
mult(X1,mult(ld(X1,X2),mult(X3,X1))) = mult(mult(X2,X3),X1),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t451,plain,
mult(X1,mult(ld(X1,X2),mult(X3,X1))) = mult(mult(X2,X3),X1),
inference(orient,[status(thm)],[t15]) ).
cnf(t6,axiom,
sFlat1 = mult(x0,rd(x1,x1)),
introduced(definition) ).
cnf(t21,plain,
mult(x0,rd(x1,x1)) = 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(t1602,plain,
mult(x0,sFlat0) = sFlat1,
inference(step,[status(thm)],[t21,t25]) ).
cnf(t27,plain,
mult(x0,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t1602]) ).
cnf(t31,plain,
mult(x0,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t27]) ).
cnf(t499,plain,
mult(mult(X1,x0),sFlat0) = mult(sFlat0,mult(ld(sFlat0,X1),sFlat1)),
inference(cp,[status(thm)],[t451,t31]) ).
cnf(t527,plain,
mult(sFlat0,mult(ld(sFlat0,X1),sFlat1)) = mult(mult(X1,x0),sFlat0),
inference(orient,[status(thm)],[t499]) ).
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(t510,plain,
mult(ld(X1,X2),mult(X3,X1)) = ld(X1,mult(mult(X2,X3),X1)),
inference(cp,[status(thm)],[t11,t451]) ).
cnf(t739,plain,
ld(X1,mult(mult(X2,X3),X1)) = mult(ld(X1,X2),mult(X3,X1)),
inference(orient,[status(thm)],[t510]) ).
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(t776,plain,
mult(ld(X1,sFlat0),mult(x1,X1)) = ld(X1,mult(x1,X1)),
inference(cp,[status(thm)],[t739,t28]) ).
cnf(t819,plain,
mult(ld(X1,sFlat0),mult(x1,X1)) = ld(X1,mult(x1,X1)),
inference(orient,[status(thm)],[t776]) ).
cnf(t833,plain,
ld(X1,sFlat0) = rd(ld(X1,mult(x1,X1)),mult(x1,X1)),
inference(cp,[status(thm)],[t9,t819]) ).
cnf(t1134,plain,
rd(ld(X1,mult(x1,X1)),mult(x1,X1)) = ld(X1,sFlat0),
inference(orient,[status(thm)],[t833]) ).
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(t43,plain,
mult(mult(x1,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,mult(x1,X1)),
inference(cp,[status(thm)],[t40,t8]) ).
cnf(t61,plain,
mult(mult(x1,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,mult(x1,X1)),
inference(orient,[status(thm)],[t43]) ).
cnf(t64,plain,
mult(x1,rd(X1,sFlat0)) = rd(mult(sFlat0,mult(x1,X1)),sFlat0),
inference(cp,[status(thm)],[t9,t61]) ).
cnf(t85,plain,
rd(mult(sFlat0,mult(x1,X1)),sFlat0) = mult(x1,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t64]) ).
cnf(t86,plain,
mult(x1,rd(ld(x1,X1),sFlat0)) = rd(mult(sFlat0,X1),sFlat0),
inference(cp,[status(thm)],[t85,t7]) ).
cnf(t112,plain,
mult(x1,rd(ld(x1,X1),sFlat0)) = rd(mult(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t86]) ).
cnf(t65,plain,
mult(x1,mult(rd(X1,sFlat0),mult(sFlat0,x1))) = mult(mult(sFlat0,mult(x1,X1)),x1),
inference(cp,[status(thm)],[t13,t61]) ).
cnf(t1604,plain,
mult(x1,mult(rd(X1,sFlat0),x1)) = mult(mult(sFlat0,mult(x1,X1)),x1),
inference(step,[status(thm)],[t65,t28]) ).
cnf(t197,plain,
mult(mult(sFlat0,mult(x1,X1)),x1) = mult(x1,mult(rd(X1,sFlat0),x1)),
inference(orient,[status(thm)],[t1604]) ).
cnf(t44,plain,
mult(x1,mult(X1,sFlat0)) = ld(sFlat0,mult(mult(x1,X1),sFlat0)),
inference(cp,[status(thm)],[t11,t40]) ).
cnf(t68,plain,
ld(sFlat0,mult(mult(x1,X1),sFlat0)) = mult(x1,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t44]) ).
cnf(t69,plain,
mult(x1,mult(ld(x1,X1),sFlat0)) = ld(sFlat0,mult(X1,sFlat0)),
inference(cp,[status(thm)],[t68,t7]) ).
cnf(t89,plain,
mult(x1,mult(ld(x1,X1),sFlat0)) = ld(sFlat0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t69]) ).
cnf(t198,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)],[t197,t89]) ).
cnf(t1605,plain,
mult(x1,mult(ld(x1,X1),x1)) = mult(mult(sFlat0,ld(sFlat0,mult(X1,sFlat0))),x1),
inference(step,[status(thm)],[t198,t9]) ).
cnf(t1606,plain,
mult(x1,mult(ld(x1,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(step,[status(thm)],[t1605,t7]) ).
cnf(t205,plain,
mult(x1,mult(ld(x1,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(orient,[status(thm)],[t1606]) ).
cnf(t210,plain,
mult(ld(x1,X1),x1) = ld(x1,mult(mult(X1,sFlat0),x1)),
inference(cp,[status(thm)],[t11,t205]) ).
cnf(t217,plain,
ld(x1,mult(mult(X1,sFlat0),x1)) = mult(ld(x1,X1),x1),
inference(orient,[status(thm)],[t210]) ).
cnf(t222,plain,
mult(ld(x1,rd(X1,sFlat0)),x1) = ld(x1,mult(X1,x1)),
inference(cp,[status(thm)],[t217,t8]) ).
cnf(t232,plain,
mult(ld(x1,rd(X1,sFlat0)),x1) = ld(x1,mult(X1,x1)),
inference(orient,[status(thm)],[t222]) ).
cnf(t113,plain,
rd(ld(x1,X1),sFlat0) = ld(x1,rd(mult(sFlat0,X1),sFlat0)),
inference(cp,[status(thm)],[t11,t112]) ).
cnf(t153,plain,
ld(x1,rd(mult(sFlat0,X1),sFlat0)) = rd(ld(x1,X1),sFlat0),
inference(orient,[status(thm)],[t113]) ).
cnf(t154,plain,
rd(ld(x1,x1),sFlat0) = ld(x1,rd(x1,sFlat0)),
inference(cp,[status(thm)],[t153,t28]) ).
cnf(t159,plain,
ld(x1,rd(x1,sFlat0)) = rd(ld(x1,x1),sFlat0),
inference(orient,[status(thm)],[t154]) ).
cnf(t234,plain,
ld(x1,mult(x1,x1)) = mult(rd(ld(x1,x1),sFlat0),x1),
inference(cp,[status(thm)],[t232,t159]) ).
cnf(t1607,plain,
x1 = mult(rd(ld(x1,x1),sFlat0),x1),
inference(step,[status(thm)],[t234,t11]) ).
cnf(t240,plain,
mult(rd(ld(x1,x1),sFlat0),x1) = x1,
inference(orient,[status(thm)],[t1607]) ).
cnf(t242,plain,
rd(ld(x1,x1),sFlat0) = rd(x1,x1),
inference(cp,[status(thm)],[t9,t240]) ).
cnf(t1608,plain,
rd(ld(x1,x1),sFlat0) = sFlat0,
inference(step,[status(thm)],[t242,t25]) ).
cnf(t244,plain,
rd(ld(x1,x1),sFlat0) = sFlat0,
inference(orient,[status(thm)],[t1608]) ).
cnf(t248,plain,
ld(x1,x1) = mult(sFlat0,sFlat0),
inference(cp,[status(thm)],[t8,t244]) ).
cnf(t254,plain,
ld(x1,x1) = mult(sFlat0,sFlat0),
inference(orient,[status(thm)],[t248]) ).
cnf(t258,plain,
rd(mult(sFlat0,x1),sFlat0) = mult(x1,rd(mult(sFlat0,sFlat0),sFlat0)),
inference(cp,[status(thm)],[t112,t254]) ).
cnf(t1612,plain,
rd(x1,sFlat0) = mult(x1,rd(mult(sFlat0,sFlat0),sFlat0)),
inference(step,[status(thm)],[t258,t28]) ).
cnf(t1613,plain,
rd(x1,sFlat0) = mult(x1,sFlat0),
inference(step,[status(thm)],[t1612,t9]) ).
cnf(t260,plain,
mult(x1,sFlat0) = rd(x1,sFlat0),
inference(orient,[status(thm)],[t1613]) ).
cnf(t1137,plain,
ld(sFlat0,sFlat0) = rd(ld(sFlat0,rd(x1,sFlat0)),mult(x1,sFlat0)),
inference(cp,[status(thm)],[t1134,t260]) ).
cnf(t765,plain,
mult(ld(X1,x1),mult(sFlat0,X1)) = ld(X1,mult(rd(x1,sFlat0),X1)),
inference(cp,[status(thm)],[t739,t260]) ).
cnf(t1001,plain,
ld(X1,mult(rd(x1,sFlat0),X1)) = mult(ld(X1,x1),mult(sFlat0,X1)),
inference(orient,[status(thm)],[t765]) ).
cnf(t1002,plain,
mult(ld(rd(x1,sFlat0),x1),mult(sFlat0,rd(x1,sFlat0))) = rd(x1,sFlat0),
inference(cp,[status(thm)],[t1001,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(t1623,plain,
mult(sFlat0,mult(sFlat0,rd(x1,sFlat0))) = rd(x1,sFlat0),
inference(step,[status(thm)],[t1002,t39]) ).
cnf(t1015,plain,
mult(sFlat0,mult(sFlat0,rd(x1,sFlat0))) = rd(x1,sFlat0),
inference(orient,[status(thm)],[t1623]) ).
cnf(t1017,plain,
mult(sFlat0,rd(x1,sFlat0)) = ld(sFlat0,rd(x1,sFlat0)),
inference(cp,[status(thm)],[t11,t1015]) ).
cnf(t1026,plain,
ld(sFlat0,rd(x1,sFlat0)) = mult(sFlat0,rd(x1,sFlat0)),
inference(orient,[status(thm)],[t1017]) ).
cnf(t1630,plain,
ld(sFlat0,sFlat0) = rd(mult(sFlat0,rd(x1,sFlat0)),mult(x1,sFlat0)),
inference(step,[status(thm)],[t1137,t1026]) ).
cnf(t1631,plain,
ld(sFlat0,sFlat0) = rd(mult(sFlat0,rd(x1,sFlat0)),rd(x1,sFlat0)),
inference(step,[status(thm)],[t1630,t260]) ).
cnf(t1632,plain,
ld(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t1631,t9]) ).
cnf(t1154,plain,
ld(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t1632]) ).
cnf(t1162,plain,
mult(mult(sFlat0,x0),sFlat0) = mult(sFlat0,mult(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t527,t1154]) ).
cnf(t1299,plain,
mult(mult(sFlat0,x0),sFlat0) = mult(sFlat0,mult(sFlat0,sFlat1)),
inference(orient,[status(thm)],[t1162]) ).
cnf(t1301,plain,
mult(sFlat0,mult(x0,mult(sFlat0,sFlat0))) = mult(mult(sFlat0,mult(sFlat0,sFlat1)),sFlat0),
inference(cp,[status(thm)],[t13,t1299]) ).
cnf(t1159,plain,
sFlat0 = mult(sFlat0,sFlat0),
inference(cp,[status(thm)],[t7,t1154]) ).
cnf(t1167,plain,
mult(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t1159]) ).
cnf(t1716,plain,
mult(sFlat0,mult(x0,sFlat0)) = mult(mult(sFlat0,mult(sFlat0,sFlat1)),sFlat0),
inference(step,[status(thm)],[t1301,t1167]) ).
cnf(t1717,plain,
mult(sFlat0,sFlat1) = mult(mult(sFlat0,mult(sFlat0,sFlat1)),sFlat0),
inference(step,[status(thm)],[t1716,t31]) ).
cnf(t1346,plain,
mult(mult(sFlat0,mult(sFlat0,sFlat1)),sFlat0) = mult(sFlat0,sFlat1),
inference(orient,[status(thm)],[t1717]) ).
cnf(t1348,plain,
mult(sFlat0,mult(sFlat0,sFlat1)) = rd(mult(sFlat0,sFlat1),sFlat0),
inference(cp,[status(thm)],[t9,t1346]) ).
cnf(t1358,plain,
mult(sFlat0,mult(sFlat0,sFlat1)) = rd(mult(sFlat0,sFlat1),sFlat0),
inference(orient,[status(thm)],[t1348]) ).
cnf(t1163,plain,
mult(mult(sFlat0,X1),sFlat0) = mult(sFlat0,mult(sFlat0,mult(X1,sFlat0))),
inference(cp,[status(thm)],[t451,t1154]) ).
cnf(t1453,plain,
mult(sFlat0,mult(sFlat0,mult(X1,sFlat0))) = mult(mult(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t1163]) ).
cnf(t771,plain,
mult(ld(X1,x0),mult(sFlat0,X1)) = ld(X1,mult(sFlat1,X1)),
inference(cp,[status(thm)],[t739,t31]) ).
cnf(t803,plain,
mult(ld(X1,x0),mult(sFlat0,X1)) = ld(X1,mult(sFlat1,X1)),
inference(orient,[status(thm)],[t771]) ).
cnf(t1174,plain,
ld(sFlat0,mult(sFlat1,sFlat0)) = mult(ld(sFlat0,x0),sFlat0),
inference(cp,[status(thm)],[t803,t1167]) ).
cnf(t1308,plain,
ld(sFlat0,mult(sFlat1,sFlat0)) = mult(ld(sFlat0,x0),sFlat0),
inference(orient,[status(thm)],[t1174]) ).
cnf(t1309,plain,
mult(sFlat1,sFlat0) = mult(sFlat0,mult(ld(sFlat0,x0),sFlat0)),
inference(cp,[status(thm)],[t7,t1308]) ).
cnf(t1373,plain,
mult(sFlat0,mult(ld(sFlat0,x0),sFlat0)) = mult(sFlat1,sFlat0),
inference(orient,[status(thm)],[t1309]) ).
cnf(t1454,plain,
mult(mult(sFlat0,ld(sFlat0,x0)),sFlat0) = mult(sFlat0,mult(sFlat1,sFlat0)),
inference(cp,[status(thm)],[t1453,t1373]) ).
cnf(t1724,plain,
mult(x0,sFlat0) = mult(sFlat0,mult(sFlat1,sFlat0)),
inference(step,[status(thm)],[t1454,t7]) ).
cnf(t1725,plain,
sFlat1 = mult(sFlat0,mult(sFlat1,sFlat0)),
inference(step,[status(thm)],[t1724,t31]) ).
cnf(t1472,plain,
mult(sFlat0,mult(sFlat1,sFlat0)) = sFlat1,
inference(orient,[status(thm)],[t1725]) ).
cnf(t1477,plain,
mult(mult(sFlat0,sFlat1),sFlat0) = mult(sFlat0,sFlat1),
inference(cp,[status(thm)],[t1453,t1472]) ).
cnf(t1499,plain,
mult(mult(sFlat0,sFlat1),sFlat0) = mult(sFlat0,sFlat1),
inference(orient,[status(thm)],[t1477]) ).
cnf(t1502,plain,
mult(sFlat0,mult(sFlat1,mult(sFlat0,sFlat0))) = mult(mult(sFlat0,sFlat1),sFlat0),
inference(cp,[status(thm)],[t13,t1499]) ).
cnf(t1731,plain,
mult(sFlat0,mult(sFlat1,sFlat0)) = mult(mult(sFlat0,sFlat1),sFlat0),
inference(step,[status(thm)],[t1502,t1167]) ).
cnf(t1732,plain,
sFlat1 = mult(mult(sFlat0,sFlat1),sFlat0),
inference(step,[status(thm)],[t1731,t1472]) ).
cnf(t1733,plain,
sFlat1 = mult(sFlat0,sFlat1),
inference(step,[status(thm)],[t1732,t1499]) ).
cnf(t1511,plain,
mult(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t1733]) ).
cnf(t1742,plain,
mult(sFlat0,sFlat1) = rd(mult(sFlat0,sFlat1),sFlat0),
inference(step,[status(thm)],[t1358,t1511]) ).
cnf(t1743,plain,
sFlat1 = rd(mult(sFlat0,sFlat1),sFlat0),
inference(step,[status(thm)],[t1742,t1511]) ).
cnf(t1744,plain,
sFlat1 = rd(sFlat1,sFlat0),
inference(step,[status(thm)],[t1743,t1511]) ).
cnf(t33,plain,
x0 = rd(sFlat1,sFlat0),
inference(cp,[status(thm)],[t9,t31]) ).
cnf(t37,plain,
rd(sFlat1,sFlat0) = x0,
inference(orient,[status(thm)],[t33]) ).
cnf(t1745,plain,
sFlat1 = x0,
inference(step,[status(thm)],[t1744,t37]) ).
cnf(t1529,plain,
sFlat1 = x0,
inference(rw,[status(thm)],[t1745]) ).
cnf(t1533,plain,
x0 = sFlat1,
inference(orient,[status(thm)],[t1529]) ).
cnf(goal_0,negated_conjecture,
mult(x0,rd(x1,x1)) != 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,t1533]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP660-11 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n008.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 15:32:38 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.09/1.90 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.09/1.90 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------