%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP750-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n007.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 13.81s 2.23s
% Output : CNFRefutation 13.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 12
% Syntax : Number of clauses : 159 ( 159 unt; 0 nHn; 62 RR)
% Number of literals : 159 ( 158 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 : 141 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
sFlat0 = mult(a,b),
introduced(definition) ).
cnf(t91,plain,
mult(a,b) = sFlat0,
inference(orient,[status(thm)],[t6]) ).
cnf(t7,axiom,
sFlat1 = mult(a,c),
introduced(definition) ).
cnf(t98,plain,
mult(a,c) = sFlat1,
inference(orient,[status(thm)],[t7]) ).
cnf(t8,axiom,
sFlat2 = mult(mult(a,b),mult(a,c)),
introduced(definition) ).
cnf(t75,plain,
mult(mult(a,b),mult(a,c)) = sFlat2,
inference(orient,[status(thm)],[t8]) ).
cnf(t19967,plain,
mult(sFlat0,mult(a,c)) = sFlat2,
inference(step,[status(thm)],[t75,t91]) ).
cnf(t97,plain,
mult(sFlat0,mult(a,c)) = sFlat2,
inference(rw,[status(thm)],[t19967]) ).
cnf(t19969,plain,
mult(sFlat0,sFlat1) = sFlat2,
inference(step,[status(thm)],[t97,t98]) ).
cnf(t130,plain,
mult(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t19969]) ).
cnf(t9,axiom,
sFlat3 = mult(a,a),
introduced(definition) ).
cnf(t81,plain,
mult(a,a) = sFlat3,
inference(orient,[status(thm)],[t9]) ).
cnf(t10,axiom,
sFlat4 = mult(b,c),
introduced(definition) ).
cnf(t104,plain,
mult(b,c) = sFlat4,
inference(orient,[status(thm)],[t10]) ).
cnf(t11,axiom,
sFlat5 = mult(mult(a,a),mult(b,c)),
introduced(definition) ).
cnf(t68,plain,
mult(mult(a,a),mult(b,c)) = sFlat5,
inference(orient,[status(thm)],[t11]) ).
cnf(t19966,plain,
mult(sFlat3,mult(b,c)) = sFlat5,
inference(step,[status(thm)],[t68,t81]) ).
cnf(t90,plain,
mult(sFlat3,mult(b,c)) = sFlat5,
inference(rw,[status(thm)],[t19966]) ).
cnf(t19968,plain,
mult(sFlat3,sFlat4) = sFlat5,
inference(step,[status(thm)],[t90,t104]) ).
cnf(t120,plain,
mult(sFlat3,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t19968]) ).
cnf(t2,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t0,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t3,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t14,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t4,axiom,
mult(mult(X1,X2),mult(X3,X3)) = mult(mult(X1,X3),mult(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
mult(mult(X1,X2),mult(X3,X3)) = mult(mult(X1,X3),mult(X2,X3)),
inference(orient,[status(thm)],[t4]) ).
cnf(t22,plain,
mult(X1,X2) = rd(mult(mult(X1,X3),mult(X2,X3)),mult(X3,X3)),
inference(cp,[status(thm)],[t14,t18]) ).
cnf(t2096,plain,
rd(mult(mult(X1,X2),mult(X3,X2)),mult(X2,X2)) = mult(X1,X3),
inference(orient,[status(thm)],[t22]) ).
cnf(t2165,plain,
mult(rd(X1,X2),X3) = rd(mult(X1,mult(X3,X2)),mult(X2,X2)),
inference(cp,[status(thm)],[t2096,t13]) ).
cnf(t5609,plain,
rd(mult(X1,mult(X2,X3)),mult(X3,X3)) = mult(rd(X1,X3),X2),
inference(orient,[status(thm)],[t2165]) ).
cnf(t5706,plain,
mult(rd(X1,X2),rd(X3,X2)) = rd(mult(X1,X3),mult(X2,X2)),
inference(cp,[status(thm)],[t5609,t13]) ).
cnf(t5740,plain,
mult(rd(X1,X2),rd(X3,X2)) = rd(mult(X1,X3),mult(X2,X2)),
inference(orient,[status(thm)],[t5706]) ).
cnf(t5808,plain,
rd(mult(mult(X1,X2),X3),mult(X2,X2)) = mult(X1,rd(X3,X2)),
inference(cp,[status(thm)],[t5740,t14]) ).
cnf(t7707,plain,
rd(mult(mult(X1,X2),X3),mult(X2,X2)) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t5808]) ).
cnf(t5,axiom,
mult(mult(X1,mult(X1,X1)),mult(X2,X3)) = mult(mult(X1,X2),mult(mult(X1,X1),X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t36,plain,
mult(mult(X1,X2),mult(mult(X1,X1),X3)) = mult(mult(X1,mult(X1,X1)),mult(X2,X3)),
inference(orient,[status(thm)],[t5]) ).
cnf(t101,plain,
mult(mult(a,X1),mult(c,X1)) = mult(sFlat1,mult(X1,X1)),
inference(cp,[status(thm)],[t18,t98]) ).
cnf(t346,plain,
mult(mult(a,X1),mult(c,X1)) = mult(sFlat1,mult(X1,X1)),
inference(orient,[status(thm)],[t101]) ).
cnf(t355,plain,
mult(mult(a,mult(a,a)),mult(X1,mult(c,a))) = mult(mult(a,X1),mult(sFlat1,mult(a,a))),
inference(cp,[status(thm)],[t36,t346]) ).
cnf(t20072,plain,
mult(mult(a,sFlat3),mult(X1,mult(c,a))) = mult(mult(a,X1),mult(sFlat1,mult(a,a))),
inference(step,[status(thm)],[t355,t81]) ).
cnf(t20073,plain,
mult(mult(a,sFlat3),mult(X1,mult(c,a))) = mult(mult(a,X1),mult(sFlat1,sFlat3)),
inference(step,[status(thm)],[t20072,t81]) ).
cnf(t16038,plain,
mult(mult(a,sFlat3),mult(X1,mult(c,a))) = mult(mult(a,X1),mult(sFlat1,sFlat3)),
inference(orient,[status(thm)],[t20073]) ).
cnf(t16055,plain,
mult(a,rd(mult(X1,mult(c,a)),sFlat3)) = rd(mult(mult(a,X1),mult(sFlat1,sFlat3)),mult(sFlat3,sFlat3)),
inference(cp,[status(thm)],[t7707,t16038]) ).
cnf(t85,plain,
mult(mult(X1,a),mult(X2,a)) = mult(mult(X1,X2),sFlat3),
inference(cp,[status(thm)],[t18,t81]) ).
cnf(t242,plain,
mult(mult(X1,a),mult(X2,a)) = mult(mult(X1,X2),sFlat3),
inference(orient,[status(thm)],[t85]) ).
cnf(t243,plain,
mult(mult(rd(X1,a),X2),sFlat3) = mult(X1,mult(X2,a)),
inference(cp,[status(thm)],[t242,t13]) ).
cnf(t462,plain,
mult(mult(rd(X1,a),X2),sFlat3) = mult(X1,mult(X2,a)),
inference(orient,[status(thm)],[t243]) ).
cnf(t467,plain,
mult(rd(X1,a),X2) = rd(mult(X1,mult(X2,a)),sFlat3),
inference(cp,[status(thm)],[t14,t462]) ).
cnf(t554,plain,
rd(mult(X1,mult(X2,a)),sFlat3) = mult(rd(X1,a),X2),
inference(orient,[status(thm)],[t467]) ).
cnf(t20074,plain,
mult(a,mult(rd(X1,a),c)) = rd(mult(mult(a,X1),mult(sFlat1,sFlat3)),mult(sFlat3,sFlat3)),
inference(step,[status(thm)],[t16055,t554]) ).
cnf(t20075,plain,
mult(a,mult(rd(X1,a),c)) = mult(rd(mult(a,X1),sFlat3),sFlat1),
inference(step,[status(thm)],[t20074,t5609]) ).
cnf(t16100,plain,
mult(rd(mult(a,X1),sFlat3),sFlat1) = mult(a,mult(rd(X1,a),c)),
inference(orient,[status(thm)],[t20075]) ).
cnf(t16101,plain,
mult(a,mult(rd(mult(X1,a),a),c)) = mult(mult(rd(a,a),X1),sFlat1),
inference(cp,[status(thm)],[t16100,t554]) ).
cnf(t20076,plain,
mult(a,mult(X1,c)) = mult(mult(rd(a,a),X1),sFlat1),
inference(step,[status(thm)],[t16101,t14]) ).
cnf(t16164,plain,
mult(mult(rd(a,a),X1),sFlat1) = mult(a,mult(X1,c)),
inference(orient,[status(thm)],[t20076]) ).
cnf(t94,plain,
mult(mult(a,X1),mult(b,X1)) = mult(sFlat0,mult(X1,X1)),
inference(cp,[status(thm)],[t18,t91]) ).
cnf(t256,plain,
mult(mult(a,X1),mult(b,X1)) = mult(sFlat0,mult(X1,X1)),
inference(orient,[status(thm)],[t94]) ).
cnf(t266,plain,
mult(mult(a,mult(a,a)),mult(X1,mult(b,a))) = mult(mult(a,X1),mult(sFlat0,mult(a,a))),
inference(cp,[status(thm)],[t36,t256]) ).
cnf(t20036,plain,
mult(mult(a,sFlat3),mult(X1,mult(b,a))) = mult(mult(a,X1),mult(sFlat0,mult(a,a))),
inference(step,[status(thm)],[t266,t81]) ).
cnf(t20037,plain,
mult(mult(a,sFlat3),mult(X1,mult(b,a))) = mult(mult(a,X1),mult(sFlat0,sFlat3)),
inference(step,[status(thm)],[t20036,t81]) ).
cnf(t11431,plain,
mult(mult(a,sFlat3),mult(X1,mult(b,a))) = mult(mult(a,X1),mult(sFlat0,sFlat3)),
inference(orient,[status(thm)],[t20037]) ).
cnf(t11447,plain,
mult(a,rd(mult(X1,mult(b,a)),sFlat3)) = rd(mult(mult(a,X1),mult(sFlat0,sFlat3)),mult(sFlat3,sFlat3)),
inference(cp,[status(thm)],[t7707,t11431]) ).
cnf(t20038,plain,
mult(a,mult(rd(X1,a),b)) = rd(mult(mult(a,X1),mult(sFlat0,sFlat3)),mult(sFlat3,sFlat3)),
inference(step,[status(thm)],[t11447,t554]) ).
cnf(t20039,plain,
mult(a,mult(rd(X1,a),b)) = mult(rd(mult(a,X1),sFlat3),sFlat0),
inference(step,[status(thm)],[t20038,t5609]) ).
cnf(t11481,plain,
mult(rd(mult(a,X1),sFlat3),sFlat0) = mult(a,mult(rd(X1,a),b)),
inference(orient,[status(thm)],[t20039]) ).
cnf(t11482,plain,
mult(a,mult(rd(mult(X1,a),a),b)) = mult(mult(rd(a,a),X1),sFlat0),
inference(cp,[status(thm)],[t11481,t554]) ).
cnf(t20040,plain,
mult(a,mult(X1,b)) = mult(mult(rd(a,a),X1),sFlat0),
inference(step,[status(thm)],[t11482,t14]) ).
cnf(t11529,plain,
mult(mult(rd(a,a),X1),sFlat0) = mult(a,mult(X1,b)),
inference(orient,[status(thm)],[t20040]) ).
cnf(t11537,plain,
mult(rd(a,a),X1) = rd(mult(a,mult(X1,b)),sFlat0),
inference(cp,[status(thm)],[t14,t11529]) ).
cnf(t11704,plain,
rd(mult(a,mult(X1,b)),sFlat0) = mult(rd(a,a),X1),
inference(orient,[status(thm)],[t11537]) ).
cnf(t11715,plain,
mult(rd(a,a),rd(X1,b)) = rd(mult(a,X1),sFlat0),
inference(cp,[status(thm)],[t11704,t13]) ).
cnf(t11869,plain,
mult(rd(a,a),rd(X1,b)) = rd(mult(a,X1),sFlat0),
inference(orient,[status(thm)],[t11715]) ).
cnf(t16165,plain,
mult(a,mult(rd(X1,b),c)) = mult(rd(mult(a,X1),sFlat0),sFlat1),
inference(cp,[status(thm)],[t16164,t11869]) ).
cnf(t17168,plain,
mult(rd(mult(a,X1),sFlat0),sFlat1) = mult(a,mult(rd(X1,b),c)),
inference(orient,[status(thm)],[t16165]) ).
cnf(t136,plain,
mult(mult(X1,sFlat0),mult(mult(X1,X1),sFlat1)) = mult(mult(X1,mult(X1,X1)),sFlat2),
inference(cp,[status(thm)],[t36,t130]) ).
cnf(t10314,plain,
mult(mult(X1,sFlat0),mult(mult(X1,X1),sFlat1)) = mult(mult(X1,mult(X1,X1)),sFlat2),
inference(orient,[status(thm)],[t136]) ).
cnf(t10327,plain,
mult(mult(a,mult(a,a)),sFlat2) = mult(mult(a,sFlat0),mult(sFlat3,sFlat1)),
inference(cp,[status(thm)],[t10314,t81]) ).
cnf(t20032,plain,
mult(mult(a,sFlat3),sFlat2) = mult(mult(a,sFlat0),mult(sFlat3,sFlat1)),
inference(step,[status(thm)],[t10327,t81]) ).
cnf(t10370,plain,
mult(mult(a,sFlat0),mult(sFlat3,sFlat1)) = mult(mult(a,sFlat3),sFlat2),
inference(orient,[status(thm)],[t20032]) ).
cnf(t10376,plain,
mult(rd(mult(a,sFlat0),sFlat1),sFlat3) = rd(mult(mult(a,sFlat3),sFlat2),mult(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t5609,t10370]) ).
cnf(t135,plain,
mult(mult(X1,sFlat0),mult(sFlat1,sFlat1)) = mult(mult(X1,sFlat1),sFlat2),
inference(cp,[status(thm)],[t18,t130]) ).
cnf(t452,plain,
mult(mult(X1,sFlat0),mult(sFlat1,sFlat1)) = mult(mult(X1,sFlat1),sFlat2),
inference(orient,[status(thm)],[t135]) ).
cnf(t455,plain,
mult(X1,sFlat0) = rd(mult(mult(X1,sFlat1),sFlat2),mult(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t14,t452]) ).
cnf(t2483,plain,
rd(mult(mult(X1,sFlat1),sFlat2),mult(sFlat1,sFlat1)) = mult(X1,sFlat0),
inference(orient,[status(thm)],[t455]) ).
cnf(t2485,plain,
mult(rd(X1,sFlat1),sFlat0) = rd(mult(X1,sFlat2),mult(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t2483,t13]) ).
cnf(t2487,plain,
rd(mult(X1,sFlat2),mult(sFlat1,sFlat1)) = mult(rd(X1,sFlat1),sFlat0),
inference(orient,[status(thm)],[t2485]) ).
cnf(t20033,plain,
mult(rd(mult(a,sFlat0),sFlat1),sFlat3) = mult(rd(mult(a,sFlat3),sFlat1),sFlat0),
inference(step,[status(thm)],[t10376,t2487]) ).
cnf(t10401,plain,
mult(rd(mult(a,sFlat3),sFlat1),sFlat0) = mult(rd(mult(a,sFlat0),sFlat1),sFlat3),
inference(orient,[status(thm)],[t20033]) ).
cnf(t16174,plain,
mult(rd(a,a),X1) = rd(mult(a,mult(X1,c)),sFlat1),
inference(cp,[status(thm)],[t14,t16164]) ).
cnf(t16553,plain,
rd(mult(a,mult(X1,c)),sFlat1) = mult(rd(a,a),X1),
inference(orient,[status(thm)],[t16174]) ).
cnf(t16574,plain,
mult(rd(a,a),rd(X1,c)) = rd(mult(a,X1),sFlat1),
inference(cp,[status(thm)],[t16553,t13]) ).
cnf(t16911,plain,
mult(rd(a,a),rd(X1,c)) = rd(mult(a,X1),sFlat1),
inference(orient,[status(thm)],[t16574]) ).
cnf(t16935,plain,
mult(a,mult(rd(X1,c),b)) = mult(rd(mult(a,X1),sFlat1),sFlat0),
inference(cp,[status(thm)],[t11529,t16911]) ).
cnf(t17546,plain,
mult(rd(mult(a,X1),sFlat1),sFlat0) = mult(a,mult(rd(X1,c),b)),
inference(orient,[status(thm)],[t16935]) ).
cnf(t20108,plain,
mult(a,mult(rd(sFlat3,c),b)) = mult(rd(mult(a,sFlat0),sFlat1),sFlat3),
inference(step,[status(thm)],[t10401,t17546]) ).
cnf(t20,plain,
mult(mult(rd(X1,X2),X3),mult(X2,X3)) = mult(X1,mult(X3,X3)),
inference(cp,[status(thm)],[t18,t13]) ).
cnf(t705,plain,
mult(mult(rd(X1,X2),X3),mult(X2,X3)) = mult(X1,mult(X3,X3)),
inference(orient,[status(thm)],[t20]) ).
cnf(t760,plain,
mult(X1,mult(c,c)) = mult(mult(rd(X1,b),c),sFlat4),
inference(cp,[status(thm)],[t705,t104]) ).
cnf(t782,plain,
mult(mult(rd(X1,b),c),sFlat4) = mult(X1,mult(c,c)),
inference(orient,[status(thm)],[t760]) ).
cnf(t785,plain,
mult(rd(X1,b),c) = rd(mult(X1,mult(c,c)),sFlat4),
inference(cp,[status(thm)],[t14,t782]) ).
cnf(t810,plain,
rd(mult(X1,mult(c,c)),sFlat4) = mult(rd(X1,b),c),
inference(orient,[status(thm)],[t785]) ).
cnf(t814,plain,
mult(rd(rd(X1,mult(c,c)),b),c) = rd(X1,sFlat4),
inference(cp,[status(thm)],[t810,t13]) ).
cnf(t2521,plain,
mult(rd(rd(X1,mult(c,c)),b),c) = rd(X1,sFlat4),
inference(orient,[status(thm)],[t814]) ).
cnf(t2524,plain,
rd(rd(X1,mult(c,c)),b) = rd(rd(X1,sFlat4),c),
inference(cp,[status(thm)],[t14,t2521]) ).
cnf(t2539,plain,
rd(rd(X1,mult(c,c)),b) = rd(rd(X1,sFlat4),c),
inference(orient,[status(thm)],[t2524]) ).
cnf(t2544,plain,
rd(X1,mult(c,c)) = mult(rd(rd(X1,sFlat4),c),b),
inference(cp,[status(thm)],[t13,t2539]) ).
cnf(t2546,plain,
mult(rd(rd(X1,sFlat4),c),b) = rd(X1,mult(c,c)),
inference(orient,[status(thm)],[t2544]) ).
cnf(t122,plain,
sFlat3 = rd(sFlat5,sFlat4),
inference(cp,[status(thm)],[t14,t120]) ).
cnf(t129,plain,
rd(sFlat5,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t122]) ).
cnf(t2547,plain,
rd(sFlat5,mult(c,c)) = mult(rd(sFlat3,c),b),
inference(cp,[status(thm)],[t2546,t129]) ).
cnf(t2562,plain,
mult(rd(sFlat3,c),b) = rd(sFlat5,mult(c,c)),
inference(orient,[status(thm)],[t2547]) ).
cnf(t20109,plain,
mult(a,rd(sFlat5,mult(c,c))) = mult(rd(mult(a,sFlat0),sFlat1),sFlat3),
inference(step,[status(thm)],[t20108,t2562]) ).
cnf(t17611,plain,
mult(a,rd(sFlat5,mult(c,c))) = mult(rd(mult(a,sFlat0),sFlat1),sFlat3),
inference(rw,[status(thm)],[t20109]) ).
cnf(t28,plain,
mult(mult(rd(X1,X2),X3),mult(X2,X2)) = mult(X1,mult(X3,X2)),
inference(cp,[status(thm)],[t18,t13]) ).
cnf(t3594,plain,
mult(mult(rd(X1,X2),X3),mult(X2,X2)) = mult(X1,mult(X3,X2)),
inference(orient,[status(thm)],[t28]) ).
cnf(t16942,plain,
mult(a,mult(rd(X1,c),a)) = mult(rd(mult(a,X1),sFlat1),mult(a,a)),
inference(cp,[status(thm)],[t3594,t16911]) ).
cnf(t20122,plain,
mult(a,mult(rd(X1,c),a)) = mult(rd(mult(a,X1),sFlat1),sFlat3),
inference(step,[status(thm)],[t16942,t81]) ).
cnf(t19696,plain,
mult(rd(mult(a,X1),sFlat1),sFlat3) = mult(a,mult(rd(X1,c),a)),
inference(orient,[status(thm)],[t20122]) ).
cnf(t20125,plain,
mult(a,rd(sFlat5,mult(c,c))) = mult(a,mult(rd(sFlat0,c),a)),
inference(step,[status(thm)],[t17611,t19696]) ).
cnf(t763,plain,
mult(X1,mult(c,c)) = mult(mult(rd(X1,a),c),sFlat1),
inference(cp,[status(thm)],[t705,t98]) ).
cnf(t791,plain,
mult(mult(rd(X1,a),c),sFlat1) = mult(X1,mult(c,c)),
inference(orient,[status(thm)],[t763]) ).
cnf(t794,plain,
mult(rd(X1,a),c) = rd(mult(X1,mult(c,c)),sFlat1),
inference(cp,[status(thm)],[t14,t791]) ).
cnf(t830,plain,
rd(mult(X1,mult(c,c)),sFlat1) = mult(rd(X1,a),c),
inference(orient,[status(thm)],[t794]) ).
cnf(t834,plain,
mult(rd(rd(X1,mult(c,c)),a),c) = rd(X1,sFlat1),
inference(cp,[status(thm)],[t830,t13]) ).
cnf(t2627,plain,
mult(rd(rd(X1,mult(c,c)),a),c) = rd(X1,sFlat1),
inference(orient,[status(thm)],[t834]) ).
cnf(t2632,plain,
rd(rd(X1,mult(c,c)),a) = rd(rd(X1,sFlat1),c),
inference(cp,[status(thm)],[t14,t2627]) ).
cnf(t2648,plain,
rd(rd(X1,mult(c,c)),a) = rd(rd(X1,sFlat1),c),
inference(orient,[status(thm)],[t2632]) ).
cnf(t2660,plain,
rd(X1,mult(c,c)) = mult(rd(rd(X1,sFlat1),c),a),
inference(cp,[status(thm)],[t13,t2648]) ).
cnf(t2667,plain,
mult(rd(rd(X1,sFlat1),c),a) = rd(X1,mult(c,c)),
inference(orient,[status(thm)],[t2660]) ).
cnf(t132,plain,
sFlat0 = rd(sFlat2,sFlat1),
inference(cp,[status(thm)],[t14,t130]) ).
cnf(t139,plain,
rd(sFlat2,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t132]) ).
cnf(t2668,plain,
rd(sFlat2,mult(c,c)) = mult(rd(sFlat0,c),a),
inference(cp,[status(thm)],[t2667,t139]) ).
cnf(t2689,plain,
mult(rd(sFlat0,c),a) = rd(sFlat2,mult(c,c)),
inference(orient,[status(thm)],[t2668]) ).
cnf(t20126,plain,
mult(a,rd(sFlat5,mult(c,c))) = mult(a,rd(sFlat2,mult(c,c))),
inference(step,[status(thm)],[t20125,t2689]) ).
cnf(t19772,plain,
mult(a,rd(sFlat5,mult(c,c))) = mult(a,rd(sFlat2,mult(c,c))),
inference(orient,[status(thm)],[t20126]) ).
cnf(t19784,plain,
mult(a,mult(rd(rd(sFlat5,mult(c,c)),b),c)) = mult(rd(mult(a,rd(sFlat2,mult(c,c))),sFlat0),sFlat1),
inference(cp,[status(thm)],[t17168,t19772]) ).
cnf(t20127,plain,
mult(a,rd(sFlat5,sFlat4)) = mult(rd(mult(a,rd(sFlat2,mult(c,c))),sFlat0),sFlat1),
inference(step,[status(thm)],[t19784,t2521]) ).
cnf(t20128,plain,
mult(a,sFlat3) = mult(rd(mult(a,rd(sFlat2,mult(c,c))),sFlat0),sFlat1),
inference(step,[status(thm)],[t20127,t129]) ).
cnf(t20129,plain,
mult(a,sFlat3) = mult(a,mult(rd(rd(sFlat2,mult(c,c)),b),c)),
inference(step,[status(thm)],[t20128,t17168]) ).
cnf(t20130,plain,
mult(a,sFlat3) = mult(a,rd(sFlat2,sFlat4)),
inference(step,[status(thm)],[t20129,t2521]) ).
cnf(t19833,plain,
mult(a,rd(sFlat2,sFlat4)) = mult(a,sFlat3),
inference(orient,[status(thm)],[t20130]) ).
cnf(t19841,plain,
rd(sFlat2,sFlat4) = ld(a,mult(a,sFlat3)),
inference(cp,[status(thm)],[t16,t19833]) ).
cnf(t20131,plain,
rd(sFlat2,sFlat4) = sFlat3,
inference(step,[status(thm)],[t19841,t16]) ).
cnf(t19891,plain,
rd(sFlat2,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t20131]) ).
cnf(t19895,plain,
sFlat2 = mult(sFlat3,sFlat4),
inference(cp,[status(thm)],[t13,t19891]) ).
cnf(t20132,plain,
sFlat2 = sFlat5,
inference(step,[status(thm)],[t19895,t120]) ).
cnf(t19906,plain,
sFlat5 = sFlat2,
inference(orient,[status(thm)],[t20132]) ).
cnf(t20133,plain,
mult(sFlat3,sFlat4) = sFlat2,
inference(step,[status(thm)],[t120,t19906]) ).
cnf(t19907,plain,
mult(sFlat3,sFlat4) = sFlat2,
inference(orient,[status(thm)],[t20133]) ).
cnf(goal_0,negated_conjecture,
mult(mult(a,b),mult(a,c)) != mult(mult(a,a),mult(b,c)),
file('/export/starexec/sandbox/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,t91]) ).
cnf(g0_1,plain,
mult(sFlat0,sFlat1) != mult(mult(a,a),mult(b,c)),
inference(rw,[status(thm)],[g0_0,t98]) ).
cnf(g0_2,plain,
sFlat2 != mult(mult(a,a),mult(b,c)),
inference(rw,[status(thm)],[g0_1,t130]) ).
cnf(g0_3,plain,
sFlat2 != mult(sFlat3,mult(b,c)),
inference(rw,[status(thm)],[g0_2,t81]) ).
cnf(g0_4,plain,
sFlat2 != mult(sFlat3,sFlat4),
inference(rw,[status(thm)],[g0_3,t104]) ).
cnf(g0_5,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_4,t19907]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP750-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n007.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 15:54:06 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 13.81/2.23 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.81/2.23 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------