%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP754-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 : n020.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:20 PM UTC 2026
% Result : Unsatisfiable 26.11s 3.80s
% Output : CNFRefutation 26.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 13
% Syntax : Number of clauses : 157 ( 157 unt; 0 nHn; 57 RR)
% Number of literals : 157 ( 156 equ; 7 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 : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 156 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
sFlat0 = mult(a,b),
introduced(definition) ).
cnf(t50,plain,
mult(a,b) = sFlat0,
inference(orient,[status(thm)],[t6]) ).
cnf(t7,axiom,
sFlat1 = mult(a,c),
introduced(definition) ).
cnf(t56,plain,
mult(a,c) = sFlat1,
inference(orient,[status(thm)],[t7]) ).
cnf(t8,axiom,
sFlat2 = mult(mult(a,b),mult(a,c)),
introduced(definition) ).
cnf(t39,plain,
mult(mult(a,b),mult(a,c)) = sFlat2,
inference(orient,[status(thm)],[t8]) ).
cnf(t5478,plain,
mult(sFlat0,mult(a,c)) = sFlat2,
inference(step,[status(thm)],[t39,t50]) ).
cnf(t55,plain,
mult(sFlat0,mult(a,c)) = sFlat2,
inference(rw,[status(thm)],[t5478]) ).
cnf(t5480,plain,
mult(sFlat0,sFlat1) = sFlat2,
inference(step,[status(thm)],[t55,t56]) ).
cnf(t84,plain,
mult(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t5480]) ).
cnf(t9,axiom,
sFlat3 = mult(a,a),
introduced(definition) ).
cnf(t44,plain,
mult(a,a) = sFlat3,
inference(orient,[status(thm)],[t9]) ).
cnf(t10,axiom,
sFlat4 = mult(b,c),
introduced(definition) ).
cnf(t61,plain,
mult(b,c) = sFlat4,
inference(orient,[status(thm)],[t10]) ).
cnf(t11,axiom,
sFlat5 = mult(mult(a,a),mult(b,c)),
introduced(definition) ).
cnf(t34,plain,
mult(mult(a,a),mult(b,c)) = sFlat5,
inference(orient,[status(thm)],[t11]) ).
cnf(t5477,plain,
mult(sFlat3,mult(b,c)) = sFlat5,
inference(step,[status(thm)],[t34,t44]) ).
cnf(t49,plain,
mult(sFlat3,mult(b,c)) = sFlat5,
inference(rw,[status(thm)],[t5477]) ).
cnf(t5479,plain,
mult(sFlat3,sFlat4) = sFlat5,
inference(step,[status(thm)],[t49,t61]) ).
cnf(t76,plain,
mult(sFlat3,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t5479]) ).
cnf(t2,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t3,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t14,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t1,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t12,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t15,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t14,t12]) ).
cnf(t74,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t0,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t16,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t4,axiom,
mult(mult(X1,X2),mult(X3,ld(X2,X2))) = mult(mult(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
mult(mult(X1,X2),mult(X3,ld(X2,X2))) = mult(mult(X1,X3),X2),
inference(orient,[status(thm)],[t4]) ).
cnf(t30,plain,
mult(X1,ld(X2,X2)) = ld(mult(X3,X2),mult(mult(X3,X1),X2)),
inference(cp,[status(thm)],[t16,t25]) ).
cnf(t965,plain,
ld(mult(X1,X2),mult(mult(X1,X3),X2)) = mult(X3,ld(X2,X2)),
inference(orient,[status(thm)],[t30]) ).
cnf(t1011,plain,
mult(ld(X1,X2),ld(X3,X3)) = ld(mult(X1,X3),mult(X2,X3)),
inference(cp,[status(thm)],[t965,t12]) ).
cnf(t1128,plain,
ld(mult(X1,X2),mult(X3,X2)) = mult(ld(X1,X3),ld(X2,X2)),
inference(orient,[status(thm)],[t1011]) ).
cnf(t1198,plain,
mult(ld(X1,sFlat0),ld(sFlat1,sFlat1)) = ld(mult(X1,sFlat1),sFlat2),
inference(cp,[status(thm)],[t1128,t84]) ).
cnf(t1218,plain,
mult(ld(X1,sFlat0),ld(sFlat1,sFlat1)) = ld(mult(X1,sFlat1),sFlat2),
inference(orient,[status(thm)],[t1198]) ).
cnf(t17,plain,
X1 = ld(rd(X2,X1),X2),
inference(cp,[status(thm)],[t16,t13]) ).
cnf(t75,plain,
ld(rd(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t17]) ).
cnf(t1219,plain,
ld(mult(rd(sFlat0,X1),sFlat1),sFlat2) = mult(X1,ld(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t1218,t75]) ).
cnf(t1288,plain,
ld(mult(rd(sFlat0,X1),sFlat1),sFlat2) = mult(X1,ld(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t1219]) ).
cnf(t1290,plain,
mult(rd(sFlat0,X1),sFlat1) = rd(sFlat2,mult(X1,ld(sFlat1,sFlat1))),
inference(cp,[status(thm)],[t74,t1288]) ).
cnf(t1305,plain,
rd(sFlat2,mult(X1,ld(sFlat1,sFlat1))) = mult(rd(sFlat0,X1),sFlat1),
inference(orient,[status(thm)],[t1290]) ).
cnf(t29,plain,
mult(mult(X1,rd(X2,ld(X3,X3))),X3) = mult(mult(X1,X3),X2),
inference(cp,[status(thm)],[t25,t13]) ).
cnf(t587,plain,
mult(mult(X1,rd(X2,ld(X3,X3))),X3) = mult(mult(X1,X3),X2),
inference(orient,[status(thm)],[t29]) ).
cnf(t593,plain,
mult(X1,rd(X2,ld(X3,X3))) = rd(mult(mult(X1,X3),X2),X3),
inference(cp,[status(thm)],[t14,t587]) ).
cnf(t733,plain,
mult(X1,rd(X2,ld(X3,X3))) = rd(mult(mult(X1,X3),X2),X3),
inference(orient,[status(thm)],[t593]) ).
cnf(t739,plain,
rd(X1,ld(X2,X2)) = ld(X3,rd(mult(mult(X3,X2),X1),X2)),
inference(cp,[status(thm)],[t16,t733]) ).
cnf(t3054,plain,
ld(X1,rd(mult(mult(X1,X2),X3),X2)) = rd(X3,ld(X2,X2)),
inference(orient,[status(thm)],[t739]) ).
cnf(t5,axiom,
mult(mult(rd(X1,X1),X2),mult(X1,X3)) = mult(X1,mult(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
mult(mult(rd(X1,X1),X2),mult(X1,X3)) = mult(X1,mult(X2,X3)),
inference(orient,[status(thm)],[t5]) ).
cnf(t19,plain,
mult(X1,mult(ld(rd(X1,X1),X2),X3)) = mult(X2,mult(X1,X3)),
inference(cp,[status(thm)],[t18,t12]) ).
cnf(t203,plain,
mult(X1,mult(ld(rd(X1,X1),X2),X3)) = mult(X2,mult(X1,X3)),
inference(orient,[status(thm)],[t19]) ).
cnf(t212,plain,
mult(ld(rd(X1,X1),X2),X3) = ld(X1,mult(X2,mult(X1,X3))),
inference(cp,[status(thm)],[t16,t203]) ).
cnf(t453,plain,
ld(X1,mult(X2,mult(X1,X3))) = mult(ld(rd(X1,X1),X2),X3),
inference(orient,[status(thm)],[t212]) ).
cnf(t488,plain,
mult(ld(rd(a,a),X1),c) = ld(a,mult(X1,sFlat1)),
inference(cp,[status(thm)],[t453,t56]) ).
cnf(t526,plain,
mult(ld(rd(a,a),X1),c) = ld(a,mult(X1,sFlat1)),
inference(orient,[status(thm)],[t488]) ).
cnf(t529,plain,
ld(rd(a,a),X1) = rd(ld(a,mult(X1,sFlat1)),c),
inference(cp,[status(thm)],[t14,t526]) ).
cnf(t571,plain,
rd(ld(a,mult(X1,sFlat1)),c) = ld(rd(a,a),X1),
inference(orient,[status(thm)],[t529]) ).
cnf(t576,plain,
ld(rd(a,a),rd(X1,sFlat1)) = rd(ld(a,X1),c),
inference(cp,[status(thm)],[t571,t13]) ).
cnf(t639,plain,
ld(rd(a,a),rd(X1,sFlat1)) = rd(ld(a,X1),c),
inference(orient,[status(thm)],[t576]) ).
cnf(t3059,plain,
rd(X1,ld(sFlat1,sFlat1)) = rd(ld(a,mult(mult(rd(a,a),sFlat1),X1)),c),
inference(cp,[status(thm)],[t3054,t639]) ).
cnf(t20,plain,
mult(X1,mult(X2,ld(X1,X3))) = mult(mult(rd(X1,X1),X2),X3),
inference(cp,[status(thm)],[t18,t12]) ).
cnf(t379,plain,
mult(mult(rd(X1,X1),X2),X3) = mult(X1,mult(X2,ld(X1,X3))),
inference(orient,[status(thm)],[t20]) ).
cnf(t5496,plain,
rd(X1,ld(sFlat1,sFlat1)) = rd(ld(a,mult(a,mult(sFlat1,ld(a,X1)))),c),
inference(step,[status(thm)],[t3059,t379]) ).
cnf(t5497,plain,
rd(X1,ld(sFlat1,sFlat1)) = rd(mult(sFlat1,ld(a,X1)),c),
inference(step,[status(thm)],[t5496,t16]) ).
cnf(t3322,plain,
rd(mult(sFlat1,ld(a,X1)),c) = rd(X1,ld(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t5497]) ).
cnf(t3337,plain,
rd(mult(a,X1),ld(sFlat1,sFlat1)) = rd(mult(sFlat1,X1),c),
inference(cp,[status(thm)],[t3322,t16]) ).
cnf(t3628,plain,
rd(mult(a,X1),ld(sFlat1,sFlat1)) = rd(mult(sFlat1,X1),c),
inference(orient,[status(thm)],[t3337]) ).
cnf(t3637,plain,
mult(a,X1) = mult(rd(mult(sFlat1,X1),c),ld(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t13,t3628]) ).
cnf(t5107,plain,
mult(rd(mult(sFlat1,X1),c),ld(sFlat1,sFlat1)) = mult(a,X1),
inference(orient,[status(thm)],[t3637]) ).
cnf(t5115,plain,
mult(a,ld(sFlat1,X1)) = mult(rd(X1,c),ld(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t5107,t12]) ).
cnf(t5131,plain,
mult(rd(X1,c),ld(sFlat1,sFlat1)) = mult(a,ld(sFlat1,X1)),
inference(orient,[status(thm)],[t5115]) ).
cnf(t5156,plain,
mult(rd(sFlat0,rd(X1,c)),sFlat1) = rd(sFlat2,mult(a,ld(sFlat1,X1))),
inference(cp,[status(thm)],[t1305,t5131]) ).
cnf(t5357,plain,
mult(rd(sFlat0,rd(X1,c)),sFlat1) = rd(sFlat2,mult(a,ld(sFlat1,X1))),
inference(orient,[status(thm)],[t5156]) ).
cnf(t60,plain,
mult(mult(a,X1),c) = mult(sFlat1,mult(X1,ld(c,c))),
inference(cp,[status(thm)],[t25,t56]) ).
cnf(t122,plain,
mult(sFlat1,mult(X1,ld(c,c))) = mult(mult(a,X1),c),
inference(orient,[status(thm)],[t60]) ).
cnf(t65,plain,
mult(mult(b,X1),c) = mult(sFlat4,mult(X1,ld(c,c))),
inference(cp,[status(thm)],[t25,t61]) ).
cnf(t134,plain,
mult(sFlat4,mult(X1,ld(c,c))) = mult(mult(b,X1),c),
inference(orient,[status(thm)],[t65]) ).
cnf(t136,plain,
mult(X1,ld(c,c)) = ld(sFlat4,mult(mult(b,X1),c)),
inference(cp,[status(thm)],[t16,t134]) ).
cnf(t249,plain,
ld(sFlat4,mult(mult(b,X1),c)) = mult(X1,ld(c,c)),
inference(orient,[status(thm)],[t136]) ).
cnf(t250,plain,
mult(ld(b,X1),ld(c,c)) = ld(sFlat4,mult(X1,c)),
inference(cp,[status(thm)],[t249,t12]) ).
cnf(t330,plain,
mult(ld(b,X1),ld(c,c)) = ld(sFlat4,mult(X1,c)),
inference(orient,[status(thm)],[t250]) ).
cnf(t334,plain,
mult(mult(a,ld(b,X1)),c) = mult(sFlat1,ld(sFlat4,mult(X1,c))),
inference(cp,[status(thm)],[t122,t330]) ).
cnf(t673,plain,
mult(mult(a,ld(b,X1)),c) = mult(sFlat1,ld(sFlat4,mult(X1,c))),
inference(orient,[status(thm)],[t334]) ).
cnf(t676,plain,
mult(a,ld(b,X1)) = rd(mult(sFlat1,ld(sFlat4,mult(X1,c))),c),
inference(cp,[status(thm)],[t14,t673]) ).
cnf(t2978,plain,
rd(mult(sFlat1,ld(sFlat4,mult(X1,c))),c) = mult(a,ld(b,X1)),
inference(orient,[status(thm)],[t676]) ).
cnf(t2994,plain,
mult(a,ld(b,b)) = rd(mult(sFlat1,ld(sFlat4,sFlat4)),c),
inference(cp,[status(thm)],[t2978,t61]) ).
cnf(t3008,plain,
rd(mult(sFlat1,ld(sFlat4,sFlat4)),c) = mult(a,ld(b,b)),
inference(orient,[status(thm)],[t2994]) ).
cnf(t5365,plain,
rd(sFlat2,mult(a,ld(sFlat1,mult(sFlat1,ld(sFlat4,sFlat4))))) = mult(rd(sFlat0,mult(a,ld(b,b))),sFlat1),
inference(cp,[status(thm)],[t5357,t3008]) ).
cnf(t5509,plain,
rd(sFlat2,mult(a,ld(sFlat4,sFlat4))) = mult(rd(sFlat0,mult(a,ld(b,b))),sFlat1),
inference(step,[status(thm)],[t5365,t16]) ).
cnf(t487,plain,
mult(ld(rd(b,b),X1),c) = ld(b,mult(X1,sFlat4)),
inference(cp,[status(thm)],[t453,t61]) ).
cnf(t519,plain,
mult(ld(rd(b,b),X1),c) = ld(b,mult(X1,sFlat4)),
inference(orient,[status(thm)],[t487]) ).
cnf(t522,plain,
ld(rd(b,b),X1) = rd(ld(b,mult(X1,sFlat4)),c),
inference(cp,[status(thm)],[t14,t519]) ).
cnf(t557,plain,
rd(ld(b,mult(X1,sFlat4)),c) = ld(rd(b,b),X1),
inference(orient,[status(thm)],[t522]) ).
cnf(t562,plain,
ld(rd(b,b),rd(X1,sFlat4)) = rd(ld(b,X1),c),
inference(cp,[status(thm)],[t557,t13]) ).
cnf(t635,plain,
ld(rd(b,b),rd(X1,sFlat4)) = rd(ld(b,X1),c),
inference(orient,[status(thm)],[t562]) ).
cnf(t3057,plain,
rd(X1,ld(sFlat4,sFlat4)) = rd(ld(b,mult(mult(rd(b,b),sFlat4),X1)),c),
inference(cp,[status(thm)],[t3054,t635]) ).
cnf(t5492,plain,
rd(X1,ld(sFlat4,sFlat4)) = rd(ld(b,mult(b,mult(sFlat4,ld(b,X1)))),c),
inference(step,[status(thm)],[t3057,t379]) ).
cnf(t5493,plain,
rd(X1,ld(sFlat4,sFlat4)) = rd(mult(sFlat4,ld(b,X1)),c),
inference(step,[status(thm)],[t5492,t16]) ).
cnf(t3242,plain,
rd(mult(sFlat4,ld(b,X1)),c) = rd(X1,ld(sFlat4,sFlat4)),
inference(orient,[status(thm)],[t5493]) ).
cnf(t3245,plain,
rd(mult(b,X1),ld(sFlat4,sFlat4)) = rd(mult(sFlat4,X1),c),
inference(cp,[status(thm)],[t3242,t16]) ).
cnf(t3528,plain,
rd(mult(b,X1),ld(sFlat4,sFlat4)) = rd(mult(sFlat4,X1),c),
inference(orient,[status(thm)],[t3245]) ).
cnf(t3536,plain,
mult(b,X1) = mult(rd(mult(sFlat4,X1),c),ld(sFlat4,sFlat4)),
inference(cp,[status(thm)],[t13,t3528]) ).
cnf(t4374,plain,
mult(rd(mult(sFlat4,X1),c),ld(sFlat4,sFlat4)) = mult(b,X1),
inference(orient,[status(thm)],[t3536]) ).
cnf(t4382,plain,
mult(b,ld(sFlat4,X1)) = mult(rd(X1,c),ld(sFlat4,sFlat4)),
inference(cp,[status(thm)],[t4374,t12]) ).
cnf(t4397,plain,
mult(rd(X1,c),ld(sFlat4,sFlat4)) = mult(b,ld(sFlat4,X1)),
inference(orient,[status(thm)],[t4382]) ).
cnf(t58,plain,
a = rd(sFlat1,c),
inference(cp,[status(thm)],[t14,t56]) ).
cnf(t71,plain,
rd(sFlat1,c) = a,
inference(orient,[status(thm)],[t58]) ).
cnf(t4415,plain,
mult(b,ld(sFlat4,sFlat1)) = mult(a,ld(sFlat4,sFlat4)),
inference(cp,[status(thm)],[t4397,t71]) ).
cnf(t4436,plain,
mult(a,ld(sFlat4,sFlat4)) = mult(b,ld(sFlat4,sFlat1)),
inference(orient,[status(thm)],[t4415]) ).
cnf(t5510,plain,
rd(sFlat2,mult(b,ld(sFlat4,sFlat1))) = mult(rd(sFlat0,mult(a,ld(b,b))),sFlat1),
inference(step,[status(thm)],[t5509,t4436]) ).
cnf(t1206,plain,
mult(ld(X1,a),ld(b,b)) = ld(mult(X1,b),sFlat0),
inference(cp,[status(thm)],[t1128,t50]) ).
cnf(t1277,plain,
mult(ld(X1,a),ld(b,b)) = ld(mult(X1,b),sFlat0),
inference(orient,[status(thm)],[t1206]) ).
cnf(t1278,plain,
ld(mult(rd(a,X1),b),sFlat0) = mult(X1,ld(b,b)),
inference(cp,[status(thm)],[t1277,t75]) ).
cnf(t1301,plain,
ld(mult(rd(a,X1),b),sFlat0) = mult(X1,ld(b,b)),
inference(orient,[status(thm)],[t1278]) ).
cnf(t1304,plain,
mult(rd(a,X1),b) = rd(sFlat0,mult(X1,ld(b,b))),
inference(cp,[status(thm)],[t74,t1301]) ).
cnf(t1353,plain,
rd(sFlat0,mult(X1,ld(b,b))) = mult(rd(a,X1),b),
inference(orient,[status(thm)],[t1304]) ).
cnf(t5511,plain,
rd(sFlat2,mult(b,ld(sFlat4,sFlat1))) = mult(mult(rd(a,a),b),sFlat1),
inference(step,[status(thm)],[t5510,t1353]) ).
cnf(t59,plain,
mult(a,mult(X1,c)) = mult(mult(rd(a,a),X1),sFlat1),
inference(cp,[status(thm)],[t18,t56]) ).
cnf(t116,plain,
mult(mult(rd(a,a),X1),sFlat1) = mult(a,mult(X1,c)),
inference(orient,[status(thm)],[t59]) ).
cnf(t119,plain,
mult(rd(a,a),X1) = rd(mult(a,mult(X1,c)),sFlat1),
inference(cp,[status(thm)],[t14,t116]) ).
cnf(t188,plain,
rd(mult(a,mult(X1,c)),sFlat1) = mult(rd(a,a),X1),
inference(orient,[status(thm)],[t119]) ).
cnf(t189,plain,
mult(rd(a,a),b) = rd(mult(a,sFlat4),sFlat1),
inference(cp,[status(thm)],[t188,t61]) ).
cnf(t192,plain,
mult(rd(a,a),b) = rd(mult(a,sFlat4),sFlat1),
inference(orient,[status(thm)],[t189]) ).
cnf(t5512,plain,
rd(sFlat2,mult(b,ld(sFlat4,sFlat1))) = mult(rd(mult(a,sFlat4),sFlat1),sFlat1),
inference(step,[status(thm)],[t5511,t192]) ).
cnf(t388,plain,
mult(a,mult(b,ld(a,X1))) = mult(rd(mult(a,sFlat4),sFlat1),X1),
inference(cp,[status(thm)],[t379,t192]) ).
cnf(t708,plain,
mult(rd(mult(a,sFlat4),sFlat1),X1) = mult(a,mult(b,ld(a,X1))),
inference(orient,[status(thm)],[t388]) ).
cnf(t5513,plain,
rd(sFlat2,mult(b,ld(sFlat4,sFlat1))) = mult(a,mult(b,ld(a,sFlat1))),
inference(step,[status(thm)],[t5512,t708]) ).
cnf(t57,plain,
c = ld(a,sFlat1),
inference(cp,[status(thm)],[t16,t56]) ).
cnf(t70,plain,
ld(a,sFlat1) = c,
inference(orient,[status(thm)],[t57]) ).
cnf(t5514,plain,
rd(sFlat2,mult(b,ld(sFlat4,sFlat1))) = mult(a,mult(b,c)),
inference(step,[status(thm)],[t5513,t70]) ).
cnf(t5515,plain,
rd(sFlat2,mult(b,ld(sFlat4,sFlat1))) = mult(a,sFlat4),
inference(step,[status(thm)],[t5514,t61]) ).
cnf(t5391,plain,
rd(sFlat2,mult(b,ld(sFlat4,sFlat1))) = mult(a,sFlat4),
inference(orient,[status(thm)],[t5515]) ).
cnf(t5393,plain,
sFlat2 = mult(mult(a,sFlat4),mult(b,ld(sFlat4,sFlat1))),
inference(cp,[status(thm)],[t13,t5391]) ).
cnf(t31,plain,
mult(X1,X2) = rd(mult(mult(X1,X3),X2),mult(X3,ld(X2,X2))),
inference(cp,[status(thm)],[t14,t25]) ).
cnf(t1580,plain,
rd(mult(mult(X1,X2),X3),mult(X2,ld(X3,X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t31]) ).
cnf(t1646,plain,
mult(a,X1) = rd(mult(sFlat3,X1),mult(a,ld(X1,X1))),
inference(cp,[status(thm)],[t1580,t44]) ).
cnf(t2421,plain,
rd(mult(sFlat3,X1),mult(a,ld(X1,X1))) = mult(a,X1),
inference(orient,[status(thm)],[t1646]) ).
cnf(t4446,plain,
mult(a,sFlat4) = rd(mult(sFlat3,sFlat4),mult(b,ld(sFlat4,sFlat1))),
inference(cp,[status(thm)],[t2421,t4436]) ).
cnf(t5502,plain,
mult(a,sFlat4) = rd(sFlat5,mult(b,ld(sFlat4,sFlat1))),
inference(step,[status(thm)],[t4446,t76]) ).
cnf(t4483,plain,
rd(sFlat5,mult(b,ld(sFlat4,sFlat1))) = mult(a,sFlat4),
inference(orient,[status(thm)],[t5502]) ).
cnf(t4484,plain,
sFlat5 = mult(mult(a,sFlat4),mult(b,ld(sFlat4,sFlat1))),
inference(cp,[status(thm)],[t13,t4483]) ).
cnf(t4634,plain,
mult(mult(a,sFlat4),mult(b,ld(sFlat4,sFlat1))) = sFlat5,
inference(orient,[status(thm)],[t4484]) ).
cnf(t5516,plain,
sFlat2 = sFlat5,
inference(step,[status(thm)],[t5393,t4634]) ).
cnf(t5396,plain,
sFlat5 = sFlat2,
inference(orient,[status(thm)],[t5516]) ).
cnf(t5517,plain,
mult(sFlat3,sFlat4) = sFlat2,
inference(step,[status(thm)],[t76,t5396]) ).
cnf(t5397,plain,
mult(sFlat3,sFlat4) = sFlat2,
inference(orient,[status(thm)],[t5517]) ).
cnf(goal_0,negated_conjecture,
mult(mult(a,b),mult(a,c)) != mult(mult(a,a),mult(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(sFlat0,mult(a,c)) != mult(mult(a,a),mult(b,c)),
inference(rw,[status(thm)],[goal_0,t50]) ).
cnf(g0_1,plain,
mult(sFlat0,sFlat1) != mult(mult(a,a),mult(b,c)),
inference(rw,[status(thm)],[g0_0,t56]) ).
cnf(g0_2,plain,
sFlat2 != mult(mult(a,a),mult(b,c)),
inference(rw,[status(thm)],[g0_1,t84]) ).
cnf(g0_3,plain,
sFlat2 != mult(sFlat3,mult(b,c)),
inference(rw,[status(thm)],[g0_2,t44]) ).
cnf(g0_4,plain,
sFlat2 != mult(sFlat3,sFlat4),
inference(rw,[status(thm)],[g0_3,t61]) ).
cnf(g0_5,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_4,t5397]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP754-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.35 % Computer : n020.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 15:57:33 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 26.11/3.80 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.11/3.80 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------