%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP681-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.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:28:01 PM UTC 2026
% Result : Unsatisfiable 19.71s 3.24s
% Output : CNFRefutation 19.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 14
% Syntax : Number of clauses : 181 ( 181 unt; 0 nHn; 63 RR)
% Number of literals : 181 ( 180 equ; 9 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 149 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
mult(mult(X1,mult(X2,X1)),X3) = mult(X1,mult(X2,mult(X1,X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
mult(mult(X1,mult(X2,X1)),X3) = mult(X1,mult(X2,mult(X1,X3))),
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
mult(unit,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
mult(unit,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t31,plain,
mult(X1,mult(unit,mult(X1,X2))) = mult(mult(X1,X1),X2),
inference(cp,[status(thm)],[t27,t15]) ).
cnf(t29597,plain,
mult(X1,mult(X1,X2)) = mult(mult(X1,X1),X2),
inference(step,[status(thm)],[t31,t15]) ).
cnf(t139,plain,
mult(mult(X1,X1),X2) = mult(X1,mult(X1,X2)),
inference(orient,[status(thm)],[t29597]) ).
cnf(t9,axiom,
sFlat0 = mult(op_c,op_c),
introduced(definition) ).
cnf(t63,plain,
mult(op_c,op_c) = sFlat0,
inference(orient,[status(thm)],[t9]) ).
cnf(t143,plain,
mult(op_c,mult(op_c,X1)) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t139,t63]) ).
cnf(t152,plain,
mult(op_c,mult(op_c,X1)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t143]) ).
cnf(t10,axiom,
sFlat1 = mult(mult(op_c,op_c),op_d),
introduced(definition) ).
cnf(t5,axiom,
mult(op_d,X1) = mult(X1,op_d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t45,plain,
mult(X1,op_d) = mult(op_d,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t29589,plain,
sFlat1 = mult(op_d,mult(op_c,op_c)),
inference(step,[status(thm)],[t10,t45]) ).
cnf(t58,plain,
mult(op_d,mult(op_c,op_c)) = sFlat1,
inference(orient,[status(thm)],[t29589]) ).
cnf(t29591,plain,
mult(op_d,sFlat0) = sFlat1,
inference(step,[status(thm)],[t58,t63]) ).
cnf(t67,plain,
mult(op_d,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t29591]) ).
cnf(t29595,plain,
mult(sFlat0,op_d) = sFlat1,
inference(step,[status(thm)],[t67,t45]) ).
cnf(t82,plain,
mult(sFlat0,op_d) = sFlat1,
inference(orient,[status(thm)],[t29595]) ).
cnf(t11,axiom,
sFlat2 = mult(mult(mult(op_c,op_c),op_d),a),
introduced(definition) ).
cnf(t29588,plain,
sFlat2 = mult(mult(op_d,mult(op_c,op_c)),a),
inference(step,[status(thm)],[t11,t45]) ).
cnf(t54,plain,
mult(mult(op_d,mult(op_c,op_c)),a) = sFlat2,
inference(orient,[status(thm)],[t29588]) ).
cnf(t29590,plain,
mult(sFlat1,a) = sFlat2,
inference(step,[status(thm)],[t54,t58]) ).
cnf(t62,plain,
mult(sFlat1,a) = sFlat2,
inference(rw,[status(thm)],[t29590]) ).
cnf(t76,plain,
mult(sFlat1,a) = sFlat2,
inference(orient,[status(thm)],[t62]) ).
cnf(t12,axiom,
sFlat3 = mult(a,mult(mult(op_c,op_c),op_d)),
introduced(definition) ).
cnf(t29592,plain,
sFlat3 = mult(a,mult(op_d,mult(op_c,op_c))),
inference(step,[status(thm)],[t12,t45]) ).
cnf(t29593,plain,
sFlat3 = mult(a,mult(op_d,sFlat0)),
inference(step,[status(thm)],[t29592,t63]) ).
cnf(t29594,plain,
sFlat3 = mult(a,mult(sFlat0,op_d)),
inference(step,[status(thm)],[t29593,t45]) ).
cnf(t68,plain,
mult(a,mult(sFlat0,op_d)) = sFlat3,
inference(orient,[status(thm)],[t29594]) ).
cnf(t29596,plain,
mult(a,sFlat1) = sFlat3,
inference(step,[status(thm)],[t68,t82]) ).
cnf(t86,plain,
mult(a,sFlat1) = sFlat3,
inference(rw,[status(thm)],[t29596]) ).
cnf(t91,plain,
mult(a,sFlat1) = sFlat3,
inference(orient,[status(thm)],[t86]) ).
cnf(t2,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t7,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t4,axiom,
mult(op_c,X1) = mult(X1,op_c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t36,plain,
mult(X1,op_c) = mult(op_c,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t40,plain,
X1 = rd(mult(op_c,X1),op_c),
inference(cp,[status(thm)],[t19,t36]) ).
cnf(t110,plain,
rd(mult(op_c,X1),op_c) = X1,
inference(orient,[status(thm)],[t40]) ).
cnf(t157,plain,
mult(sFlat0,op_d) = mult(op_c,mult(op_d,op_c)),
inference(cp,[status(thm)],[t152,t45]) ).
cnf(t29598,plain,
sFlat1 = mult(op_c,mult(op_d,op_c)),
inference(step,[status(thm)],[t157,t82]) ).
cnf(t165,plain,
mult(op_c,mult(op_d,op_c)) = sFlat1,
inference(orient,[status(thm)],[t29598]) ).
cnf(t167,plain,
mult(op_d,op_c) = rd(sFlat1,op_c),
inference(cp,[status(thm)],[t110,t165]) ).
cnf(t173,plain,
mult(op_d,op_c) = rd(sFlat1,op_c),
inference(orient,[status(thm)],[t167]) ).
cnf(t179,plain,
mult(op_c,mult(op_d,mult(op_c,X1))) = mult(mult(op_c,rd(sFlat1,op_c)),X1),
inference(cp,[status(thm)],[t27,t173]) ).
cnf(t6,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t38,plain,
mult(op_c,rd(X1,op_c)) = X1,
inference(cp,[status(thm)],[t36,t17]) ).
cnf(t99,plain,
mult(op_c,rd(X1,op_c)) = X1,
inference(orient,[status(thm)],[t38]) ).
cnf(t29621,plain,
mult(op_c,mult(op_d,mult(op_c,X1))) = mult(sFlat1,X1),
inference(step,[status(thm)],[t179,t99]) ).
cnf(t708,plain,
mult(op_c,mult(op_d,mult(op_c,X1))) = mult(sFlat1,X1),
inference(orient,[status(thm)],[t29621]) ).
cnf(t715,plain,
mult(sFlat1,rd(X1,op_c)) = mult(op_c,mult(op_d,X1)),
inference(cp,[status(thm)],[t708,t99]) ).
cnf(t738,plain,
mult(op_c,mult(op_d,X1)) = mult(sFlat1,rd(X1,op_c)),
inference(orient,[status(thm)],[t715]) ).
cnf(t47,plain,
mult(op_d,rd(X1,op_d)) = X1,
inference(cp,[status(thm)],[t45,t17]) ).
cnf(t116,plain,
mult(op_d,rd(X1,op_d)) = X1,
inference(orient,[status(thm)],[t47]) ).
cnf(t742,plain,
mult(sFlat1,rd(rd(X1,op_d),op_c)) = mult(op_c,X1),
inference(cp,[status(thm)],[t738,t116]) ).
cnf(t1095,plain,
mult(sFlat1,rd(rd(X1,op_d),op_c)) = mult(op_c,X1),
inference(orient,[status(thm)],[t742]) ).
cnf(t1105,plain,
rd(rd(X1,op_d),op_c) = ld(sFlat1,mult(op_c,X1)),
inference(cp,[status(thm)],[t23,t1095]) ).
cnf(t1110,plain,
ld(sFlat1,mult(op_c,X1)) = rd(rd(X1,op_d),op_c),
inference(orient,[status(thm)],[t1105]) ).
cnf(t1116,plain,
rd(rd(rd(X1,op_c),op_d),op_c) = ld(sFlat1,X1),
inference(cp,[status(thm)],[t1110,t99]) ).
cnf(t1758,plain,
rd(rd(rd(X1,op_c),op_d),op_c) = ld(sFlat1,X1),
inference(orient,[status(thm)],[t1116]) ).
cnf(t3,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t151,plain,
mult(X1,mult(mult(X2,X2),mult(X1,X3))) = mult(mult(X1,mult(X2,mult(X2,X1))),X3),
inference(cp,[status(thm)],[t27,t139]) ).
cnf(t30318,plain,
mult(X1,mult(X2,mult(X2,mult(X1,X3)))) = mult(mult(X1,mult(X2,mult(X2,X1))),X3),
inference(step,[status(thm)],[t151,t139]) ).
cnf(t27951,plain,
mult(mult(X1,mult(X2,mult(X2,X1))),X3) = mult(X1,mult(X2,mult(X2,mult(X1,X3)))),
inference(orient,[status(thm)],[t30318]) ).
cnf(t27997,plain,
mult(op_c,mult(op_d,mult(op_d,mult(op_c,X1)))) = mult(mult(sFlat1,rd(mult(op_d,op_c),op_c)),X1),
inference(cp,[status(thm)],[t27951,t738]) ).
cnf(t30328,plain,
mult(sFlat1,rd(mult(op_d,mult(op_c,X1)),op_c)) = mult(mult(sFlat1,rd(mult(op_d,op_c),op_c)),X1),
inference(step,[status(thm)],[t27997,t738]) ).
cnf(t756,plain,
mult(op_d,X1) = rd(mult(sFlat1,rd(X1,op_c)),op_c),
inference(cp,[status(thm)],[t110,t738]) ).
cnf(t1402,plain,
rd(mult(sFlat1,rd(X1,op_c)),op_c) = mult(op_d,X1),
inference(orient,[status(thm)],[t756]) ).
cnf(t1417,plain,
mult(op_d,mult(op_c,X1)) = rd(mult(sFlat1,X1),op_c),
inference(cp,[status(thm)],[t1402,t110]) ).
cnf(t1450,plain,
mult(op_d,mult(op_c,X1)) = rd(mult(sFlat1,X1),op_c),
inference(orient,[status(thm)],[t1417]) ).
cnf(t30329,plain,
mult(sFlat1,rd(rd(mult(sFlat1,X1),op_c),op_c)) = mult(mult(sFlat1,rd(mult(op_d,op_c),op_c)),X1),
inference(step,[status(thm)],[t30328,t1450]) ).
cnf(t154,plain,
mult(sFlat0,rd(X1,op_c)) = mult(op_c,X1),
inference(cp,[status(thm)],[t152,t99]) ).
cnf(t186,plain,
mult(sFlat0,rd(X1,op_c)) = mult(op_c,X1),
inference(orient,[status(thm)],[t154]) ).
cnf(t189,plain,
rd(X1,op_c) = ld(sFlat0,mult(op_c,X1)),
inference(cp,[status(thm)],[t23,t186]) ).
cnf(t255,plain,
ld(sFlat0,mult(op_c,X1)) = rd(X1,op_c),
inference(orient,[status(thm)],[t189]) ).
cnf(t256,plain,
rd(rd(X1,op_c),op_c) = ld(sFlat0,X1),
inference(cp,[status(thm)],[t255,t99]) ).
cnf(t276,plain,
rd(rd(X1,op_c),op_c) = ld(sFlat0,X1),
inference(orient,[status(thm)],[t256]) ).
cnf(t28,plain,
mult(X1,mult(X2,mult(X1,ld(mult(X1,mult(X2,X1)),X3)))) = X3,
inference(cp,[status(thm)],[t27,t13]) ).
cnf(t203,plain,
mult(X1,mult(X2,mult(X1,ld(mult(X1,mult(X2,X1)),X3)))) = X3,
inference(orient,[status(thm)],[t28]) ).
cnf(t39,plain,
op_c = ld(X1,mult(op_c,X1)),
inference(cp,[status(thm)],[t23,t36]) ).
cnf(t107,plain,
ld(X1,mult(op_c,X1)) = op_c,
inference(orient,[status(thm)],[t39]) ).
cnf(t160,plain,
op_c = ld(mult(op_c,X1),mult(sFlat0,X1)),
inference(cp,[status(thm)],[t107,t152]) ).
cnf(t329,plain,
ld(mult(op_c,X1),mult(sFlat0,X1)) = op_c,
inference(orient,[status(thm)],[t160]) ).
cnf(t338,plain,
mult(sFlat0,mult(X1,op_c)) = mult(op_c,mult(X1,mult(op_c,op_c))),
inference(cp,[status(thm)],[t203,t329]) ).
cnf(t29606,plain,
mult(sFlat0,mult(X1,op_c)) = mult(op_c,mult(X1,sFlat0)),
inference(step,[status(thm)],[t338,t63]) ).
cnf(t339,plain,
mult(op_c,mult(X1,sFlat0)) = mult(sFlat0,mult(X1,op_c)),
inference(orient,[status(thm)],[t29606]) ).
cnf(t349,plain,
mult(X1,sFlat0) = rd(mult(sFlat0,mult(X1,op_c)),op_c),
inference(cp,[status(thm)],[t110,t339]) ).
cnf(t159,plain,
mult(op_c,X1) = rd(mult(sFlat0,X1),op_c),
inference(cp,[status(thm)],[t110,t152]) ).
cnf(t247,plain,
rd(mult(sFlat0,X1),op_c) = mult(op_c,X1),
inference(orient,[status(thm)],[t159]) ).
cnf(t29607,plain,
mult(X1,sFlat0) = mult(op_c,mult(X1,op_c)),
inference(step,[status(thm)],[t349,t247]) ).
cnf(t156,plain,
mult(sFlat0,X1) = mult(op_c,mult(X1,op_c)),
inference(cp,[status(thm)],[t152,t36]) ).
cnf(t192,plain,
mult(op_c,mult(X1,op_c)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t156]) ).
cnf(t29608,plain,
mult(X1,sFlat0) = mult(sFlat0,X1),
inference(step,[status(thm)],[t29607,t192]) ).
cnf(t355,plain,
mult(X1,sFlat0) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t29608]) ).
cnf(t359,plain,
mult(sFlat0,rd(X1,sFlat0)) = X1,
inference(cp,[status(thm)],[t355,t17]) ).
cnf(t374,plain,
mult(sFlat0,rd(X1,sFlat0)) = X1,
inference(orient,[status(thm)],[t359]) ).
cnf(t379,plain,
rd(X1,sFlat0) = ld(sFlat0,X1),
inference(cp,[status(thm)],[t23,t374]) ).
cnf(t383,plain,
ld(sFlat0,X1) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t379]) ).
cnf(t29609,plain,
rd(rd(X1,op_c),op_c) = rd(X1,sFlat0),
inference(step,[status(thm)],[t276,t383]) ).
cnf(t384,plain,
rd(rd(X1,op_c),op_c) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t29609]) ).
cnf(t30330,plain,
mult(sFlat1,rd(mult(sFlat1,X1),sFlat0)) = mult(mult(sFlat1,rd(mult(op_d,op_c),op_c)),X1),
inference(step,[status(thm)],[t30329,t384]) ).
cnf(t30331,plain,
mult(sFlat1,rd(mult(sFlat1,X1),sFlat0)) = mult(mult(sFlat1,op_d),X1),
inference(step,[status(thm)],[t30330,t19]) ).
cnf(t28633,plain,
mult(sFlat1,rd(mult(sFlat1,X1),sFlat0)) = mult(mult(sFlat1,op_d),X1),
inference(orient,[status(thm)],[t30331]) ).
cnf(t28677,plain,
rd(mult(sFlat1,X1),sFlat0) = ld(sFlat1,mult(mult(sFlat1,op_d),X1)),
inference(cp,[status(thm)],[t23,t28633]) ).
cnf(t28930,plain,
ld(sFlat1,mult(mult(sFlat1,op_d),X1)) = rd(mult(sFlat1,X1),sFlat0),
inference(orient,[status(thm)],[t28677]) ).
cnf(t85,plain,
mult(op_d,mult(sFlat0,mult(op_d,X1))) = mult(mult(op_d,sFlat1),X1),
inference(cp,[status(thm)],[t27,t82]) ).
cnf(t29651,plain,
mult(op_d,mult(sFlat0,mult(op_d,X1))) = mult(mult(sFlat1,op_d),X1),
inference(step,[status(thm)],[t85,t45]) ).
cnf(t2125,plain,
mult(op_d,mult(sFlat0,mult(op_d,X1))) = mult(mult(sFlat1,op_d),X1),
inference(orient,[status(thm)],[t29651]) ).
cnf(t2133,plain,
mult(mult(sFlat1,op_d),rd(X1,op_d)) = mult(op_d,mult(sFlat0,X1)),
inference(cp,[status(thm)],[t2125,t116]) ).
cnf(t4460,plain,
mult(mult(sFlat1,op_d),rd(X1,op_d)) = mult(op_d,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t2133]) ).
cnf(t1782,plain,
rd(rd(X1,op_c),op_d) = mult(op_c,ld(sFlat1,X1)),
inference(cp,[status(thm)],[t99,t1758]) ).
cnf(t1787,plain,
mult(op_c,ld(sFlat1,X1)) = rd(rd(X1,op_c),op_d),
inference(orient,[status(thm)],[t1782]) ).
cnf(t77,plain,
a = ld(sFlat1,sFlat2),
inference(cp,[status(thm)],[t23,t76]) ).
cnf(t87,plain,
ld(sFlat1,sFlat2) = a,
inference(orient,[status(thm)],[t77]) ).
cnf(t1788,plain,
rd(rd(sFlat2,op_c),op_d) = mult(op_c,a),
inference(cp,[status(thm)],[t1787,t87]) ).
cnf(t1812,plain,
rd(rd(sFlat2,op_c),op_d) = mult(op_c,a),
inference(orient,[status(thm)],[t1788]) ).
cnf(t4467,plain,
mult(op_d,mult(sFlat0,rd(sFlat2,op_c))) = mult(mult(sFlat1,op_d),mult(op_c,a)),
inference(cp,[status(thm)],[t4460,t1812]) ).
cnf(t29809,plain,
mult(op_d,mult(op_c,sFlat2)) = mult(mult(sFlat1,op_d),mult(op_c,a)),
inference(step,[status(thm)],[t4467,t186]) ).
cnf(t29810,plain,
mult(op_d,mult(sFlat2,op_c)) = mult(mult(sFlat1,op_d),mult(op_c,a)),
inference(step,[status(thm)],[t29809,t36]) ).
cnf(t1415,plain,
mult(op_d,mult(X1,op_c)) = rd(mult(sFlat1,X1),op_c),
inference(cp,[status(thm)],[t1402,t19]) ).
cnf(t1432,plain,
mult(op_d,mult(X1,op_c)) = rd(mult(sFlat1,X1),op_c),
inference(orient,[status(thm)],[t1415]) ).
cnf(t29811,plain,
rd(mult(sFlat1,sFlat2),op_c) = mult(mult(sFlat1,op_d),mult(op_c,a)),
inference(step,[status(thm)],[t29810,t1432]) ).
cnf(t7461,plain,
mult(mult(sFlat1,op_d),mult(op_c,a)) = rd(mult(sFlat1,sFlat2),op_c),
inference(orient,[status(thm)],[t29811]) ).
cnf(t28931,plain,
rd(mult(sFlat1,mult(op_c,a)),sFlat0) = ld(sFlat1,rd(mult(sFlat1,sFlat2),op_c)),
inference(cp,[status(thm)],[t28930,t7461]) ).
cnf(t363,plain,
X1 = rd(mult(sFlat0,X1),sFlat0),
inference(cp,[status(thm)],[t19,t355]) ).
cnf(t402,plain,
rd(mult(sFlat0,X1),sFlat0) = X1,
inference(orient,[status(thm)],[t363]) ).
cnf(t201,plain,
mult(op_c,mult(X1,mult(op_c,X2))) = mult(mult(sFlat0,X1),X2),
inference(cp,[status(thm)],[t27,t192]) ).
cnf(t2294,plain,
mult(op_c,mult(X1,mult(op_c,X2))) = mult(mult(sFlat0,X1),X2),
inference(orient,[status(thm)],[t201]) ).
cnf(t2322,plain,
mult(mult(sFlat0,X1),op_d) = mult(op_c,mult(X1,mult(op_d,op_c))),
inference(cp,[status(thm)],[t2294,t45]) ).
cnf(t29724,plain,
mult(mult(sFlat0,X1),op_d) = mult(op_c,mult(X1,rd(sFlat1,op_c))),
inference(step,[status(thm)],[t2322,t173]) ).
cnf(t29725,plain,
mult(op_d,mult(sFlat0,X1)) = mult(op_c,mult(X1,rd(sFlat1,op_c))),
inference(step,[status(thm)],[t29724,t45]) ).
cnf(t4735,plain,
mult(op_c,mult(X1,rd(sFlat1,op_c))) = mult(op_d,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t29725]) ).
cnf(t4764,plain,
mult(sFlat0,mult(X1,rd(sFlat1,op_c))) = mult(op_c,mult(op_d,mult(sFlat0,X1))),
inference(cp,[status(thm)],[t152,t4735]) ).
cnf(t29887,plain,
mult(sFlat0,mult(X1,rd(sFlat1,op_c))) = mult(sFlat1,rd(mult(sFlat0,X1),op_c)),
inference(step,[status(thm)],[t4764,t738]) ).
cnf(t29888,plain,
mult(sFlat0,mult(X1,rd(sFlat1,op_c))) = mult(sFlat1,mult(op_c,X1)),
inference(step,[status(thm)],[t29887,t247]) ).
cnf(t9786,plain,
mult(sFlat0,mult(X1,rd(sFlat1,op_c))) = mult(sFlat1,mult(op_c,X1)),
inference(orient,[status(thm)],[t29888]) ).
cnf(t9824,plain,
mult(X1,rd(sFlat1,op_c)) = rd(mult(sFlat1,mult(op_c,X1)),sFlat0),
inference(cp,[status(thm)],[t402,t9786]) ).
cnf(t13566,plain,
rd(mult(sFlat1,mult(op_c,X1)),sFlat0) = mult(X1,rd(sFlat1,op_c)),
inference(orient,[status(thm)],[t9824]) ).
cnf(t30341,plain,
mult(a,rd(sFlat1,op_c)) = ld(sFlat1,rd(mult(sFlat1,sFlat2),op_c)),
inference(step,[status(thm)],[t28931,t13566]) ).
cnf(t29265,plain,
ld(sFlat1,rd(mult(sFlat1,sFlat2),op_c)) = mult(a,rd(sFlat1,op_c)),
inference(orient,[status(thm)],[t30341]) ).
cnf(t29266,plain,
rd(mult(sFlat1,sFlat2),op_c) = mult(sFlat1,mult(a,rd(sFlat1,op_c))),
inference(cp,[status(thm)],[t13,t29265]) ).
cnf(t94,plain,
mult(sFlat1,mult(a,mult(sFlat1,X1))) = mult(mult(sFlat1,sFlat3),X1),
inference(cp,[status(thm)],[t27,t91]) ).
cnf(t2224,plain,
mult(sFlat1,mult(a,mult(sFlat1,X1))) = mult(mult(sFlat1,sFlat3),X1),
inference(orient,[status(thm)],[t94]) ).
cnf(t2315,plain,
mult(mult(sFlat0,X1),rd(X2,op_c)) = mult(op_c,mult(X1,X2)),
inference(cp,[status(thm)],[t2294,t99]) ).
cnf(t4616,plain,
mult(mult(sFlat0,X1),rd(X2,op_c)) = mult(op_c,mult(X1,X2)),
inference(orient,[status(thm)],[t2315]) ).
cnf(t4627,plain,
mult(op_c,mult(rd(X1,sFlat0),X2)) = mult(X1,rd(X2,op_c)),
inference(cp,[status(thm)],[t4616,t374]) ).
cnf(t7538,plain,
mult(op_c,mult(rd(X1,sFlat0),X2)) = mult(X1,rd(X2,op_c)),
inference(orient,[status(thm)],[t4627]) ).
cnf(t0,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t14,plain,
mult(X1,unit) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t7548,plain,
mult(X1,rd(unit,op_c)) = mult(op_c,rd(X1,sFlat0)),
inference(cp,[status(thm)],[t7538,t14]) ).
cnf(t378,plain,
mult(op_c,rd(X1,sFlat0)) = rd(X1,op_c),
inference(cp,[status(thm)],[t247,t374]) ).
cnf(t424,plain,
mult(op_c,rd(X1,sFlat0)) = rd(X1,op_c),
inference(orient,[status(thm)],[t378]) ).
cnf(t29813,plain,
mult(X1,rd(unit,op_c)) = rd(X1,op_c),
inference(step,[status(thm)],[t7548,t424]) ).
cnf(t7629,plain,
mult(X1,rd(unit,op_c)) = rd(X1,op_c),
inference(orient,[status(thm)],[t29813]) ).
cnf(t7662,plain,
mult(mult(sFlat1,sFlat3),rd(unit,op_c)) = mult(sFlat1,mult(a,rd(sFlat1,op_c))),
inference(cp,[status(thm)],[t2224,t7629]) ).
cnf(t30020,plain,
rd(mult(sFlat1,sFlat3),op_c) = mult(sFlat1,mult(a,rd(sFlat1,op_c))),
inference(step,[status(thm)],[t7662,t7629]) ).
cnf(t12544,plain,
mult(sFlat1,mult(a,rd(sFlat1,op_c))) = rd(mult(sFlat1,sFlat3),op_c),
inference(orient,[status(thm)],[t30020]) ).
cnf(t30342,plain,
rd(mult(sFlat1,sFlat2),op_c) = rd(mult(sFlat1,sFlat3),op_c),
inference(step,[status(thm)],[t29266,t12544]) ).
cnf(t29279,plain,
rd(mult(sFlat1,sFlat3),op_c) = rd(mult(sFlat1,sFlat2),op_c),
inference(orient,[status(thm)],[t30342]) ).
cnf(t29343,plain,
ld(sFlat1,mult(sFlat1,sFlat3)) = rd(rd(rd(mult(sFlat1,sFlat2),op_c),op_d),op_c),
inference(cp,[status(thm)],[t1758,t29279]) ).
cnf(t30345,plain,
sFlat3 = rd(rd(rd(mult(sFlat1,sFlat2),op_c),op_d),op_c),
inference(step,[status(thm)],[t29343,t23]) ).
cnf(t30346,plain,
sFlat3 = ld(sFlat1,mult(sFlat1,sFlat2)),
inference(step,[status(thm)],[t30345,t1758]) ).
cnf(t30347,plain,
sFlat3 = sFlat2,
inference(step,[status(thm)],[t30346,t23]) ).
cnf(t29347,plain,
sFlat3 = sFlat2,
inference(orient,[status(thm)],[t30347]) ).
cnf(t30348,plain,
mult(a,sFlat1) = sFlat2,
inference(step,[status(thm)],[t91,t29347]) ).
cnf(t29348,plain,
mult(a,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t30348]) ).
cnf(goal_0,negated_conjecture,
mult(mult(mult(op_c,op_c),op_d),a) != mult(a,mult(mult(op_c,op_c),op_d)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(mult(op_c,mult(op_c,op_d)),a) != mult(a,mult(mult(op_c,op_c),op_d)),
inference(rw,[status(thm)],[goal_0,t139]) ).
cnf(g0_1,plain,
mult(mult(sFlat0,op_d),a) != mult(a,mult(mult(op_c,op_c),op_d)),
inference(rw,[status(thm)],[g0_0,t152]) ).
cnf(g0_2,plain,
mult(sFlat1,a) != mult(a,mult(mult(op_c,op_c),op_d)),
inference(rw,[status(thm)],[g0_1,t82]) ).
cnf(g0_3,plain,
sFlat2 != mult(a,mult(mult(op_c,op_c),op_d)),
inference(rw,[status(thm)],[g0_2,t76]) ).
cnf(g0_4,plain,
sFlat2 != mult(a,mult(op_c,mult(op_c,op_d))),
inference(rw,[status(thm)],[g0_3,t139]) ).
cnf(g0_5,plain,
sFlat2 != mult(a,mult(sFlat0,op_d)),
inference(rw,[status(thm)],[g0_4,t152]) ).
cnf(g0_6,plain,
sFlat2 != mult(a,sFlat1),
inference(rw,[status(thm)],[g0_5,t82]) ).
cnf(g0_7,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_6,t29348]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP681-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.60 % Computer : n001.cluster.edu
% 0.12/0.60 % Model : x86_64 x86_64
% 0.12/0.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.60 % Memory : 8046.5625MB
% 0.12/0.60 % OS : Linux 6.8.0-71-generic
% 0.12/0.60 % CPULimit : 300
% 0.12/0.60 % WCLimit : 300
% 0.12/0.60 % DateTime : Wed Sep 23 15:46:20 UTC 2026
% 0.12/0.60 % CPUTime :
% 0.12/0.60 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 19.71/3.24 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.71/3.24 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------