%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP654-12 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.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:51 PM UTC 2026
% Result : Unsatisfiable 18.79s 2.86s
% Output : CNFRefutation 18.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 108
% Number of leaves : 8
% Syntax : Number of clauses : 353 ( 353 unt; 0 nHn; 75 RR)
% Number of literals : 353 ( 352 equ; 5 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 : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 400 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(t11,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t0]) ).
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(t3,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/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),X1),X3) = mult(X1,mult(X2,mult(X1,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(mult(mult(X1,X2),X1),X3) = mult(X1,mult(X2,mult(X1,X3))),
inference(orient,[status(thm)],[t4]) ).
cnf(t18,plain,
mult(mult(X1,X2),X1) = rd(mult(X1,mult(X2,mult(X1,X3))),X3),
inference(cp,[status(thm)],[t9,t13]) ).
cnf(t2659,plain,
rd(mult(X1,mult(X2,mult(X1,X3))),X3) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t18]) ).
cnf(t2688,plain,
mult(mult(X1,rd(X2,mult(X1,X3))),X1) = rd(mult(X1,X2),X3),
inference(cp,[status(thm)],[t2659,t8]) ).
cnf(t14740,plain,
mult(mult(X1,rd(X2,mult(X1,X3))),X1) = rd(mult(X1,X2),X3),
inference(orient,[status(thm)],[t2688]) ).
cnf(t14757,plain,
rd(mult(X1,X2),ld(X1,X3)) = mult(mult(X1,rd(X2,X3)),X1),
inference(cp,[status(thm)],[t14740,t7]) ).
cnf(t15020,plain,
mult(mult(X1,rd(X2,X3)),X1) = rd(mult(X1,X2),ld(X1,X3)),
inference(orient,[status(thm)],[t14757]) ).
cnf(t15,plain,
mult(X1,mult(ld(X1,X2),mult(X1,X3))) = mult(mult(X2,X1),X3),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t225,plain,
mult(X1,mult(ld(X1,X2),mult(X1,X3))) = mult(mult(X2,X1),X3),
inference(orient,[status(thm)],[t15]) ).
cnf(t5,axiom,
sFlat0 = rd(x1,x1),
introduced(definition) ).
cnf(t25,plain,
rd(x1,x1) = sFlat0,
inference(orient,[status(thm)],[t5]) ).
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(t250,plain,
mult(mult(X1,sFlat0),x1) = mult(sFlat0,mult(ld(sFlat0,X1),x1)),
inference(cp,[status(thm)],[t225,t28]) ).
cnf(t272,plain,
mult(sFlat0,mult(ld(sFlat0,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(orient,[status(thm)],[t250]) ).
cnf(t279,plain,
mult(ld(sFlat0,X1),x1) = ld(sFlat0,mult(mult(X1,sFlat0),x1)),
inference(cp,[status(thm)],[t11,t272]) ).
cnf(t304,plain,
ld(sFlat0,mult(mult(X1,sFlat0),x1)) = mult(ld(sFlat0,X1),x1),
inference(orient,[status(thm)],[t279]) ).
cnf(t307,plain,
mult(ld(sFlat0,rd(X1,sFlat0)),x1) = ld(sFlat0,mult(X1,x1)),
inference(cp,[status(thm)],[t304,t8]) ).
cnf(t332,plain,
mult(ld(sFlat0,rd(X1,sFlat0)),x1) = ld(sFlat0,mult(X1,x1)),
inference(orient,[status(thm)],[t307]) ).
cnf(t334,plain,
ld(sFlat0,rd(X1,sFlat0)) = rd(ld(sFlat0,mult(X1,x1)),x1),
inference(cp,[status(thm)],[t9,t332]) ).
cnf(t344,plain,
rd(ld(sFlat0,mult(X1,x1)),x1) = ld(sFlat0,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t334]) ).
cnf(t14,plain,
mult(X1,mult(X2,mult(X1,ld(mult(mult(X1,X2),X1),X3)))) = X3,
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t177,plain,
mult(X1,mult(X2,mult(X1,ld(mult(mult(X1,X2),X1),X3)))) = X3,
inference(orient,[status(thm)],[t14]) ).
cnf(t345,plain,
ld(sFlat0,rd(sFlat0,sFlat0)) = rd(x1,x1),
inference(cp,[status(thm)],[t344,t11]) ).
cnf(t37958,plain,
ld(sFlat0,rd(sFlat0,sFlat0)) = sFlat0,
inference(step,[status(thm)],[t345,t25]) ).
cnf(t352,plain,
ld(sFlat0,rd(sFlat0,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t37958]) ).
cnf(t353,plain,
rd(sFlat0,sFlat0) = mult(sFlat0,sFlat0),
inference(cp,[status(thm)],[t7,t352]) ).
cnf(t388,plain,
mult(sFlat0,sFlat0) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t353]) ).
cnf(t400,plain,
X1 = mult(sFlat0,mult(sFlat0,mult(sFlat0,ld(mult(rd(sFlat0,sFlat0),sFlat0),X1)))),
inference(cp,[status(thm)],[t177,t388]) ).
cnf(t37960,plain,
X1 = mult(sFlat0,mult(sFlat0,mult(sFlat0,ld(sFlat0,X1)))),
inference(step,[status(thm)],[t400,t8]) ).
cnf(t37961,plain,
X1 = mult(sFlat0,mult(sFlat0,X1)),
inference(step,[status(thm)],[t37960,t7]) ).
cnf(t404,plain,
mult(sFlat0,mult(sFlat0,X1)) = X1,
inference(orient,[status(thm)],[t37961]) ).
cnf(t412,plain,
ld(sFlat0,X1) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t404,t7]) ).
cnf(t426,plain,
ld(sFlat0,X1) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t412]) ).
cnf(t37981,plain,
rd(mult(sFlat0,mult(X1,x1)),x1) = ld(sFlat0,rd(X1,sFlat0)),
inference(step,[status(thm)],[t344,t426]) ).
cnf(t37982,plain,
rd(mult(sFlat0,mult(X1,x1)),x1) = mult(sFlat0,rd(X1,sFlat0)),
inference(step,[status(thm)],[t37981,t426]) ).
cnf(t448,plain,
rd(mult(sFlat0,mult(X1,x1)),x1) = mult(sFlat0,rd(X1,sFlat0)),
inference(rw,[status(thm)],[t37982]) ).
cnf(t803,plain,
rd(mult(sFlat0,mult(X1,x1)),x1) = mult(sFlat0,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t448]) ).
cnf(t37992,plain,
mult(sFlat0,mult(mult(sFlat0,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(step,[status(thm)],[t272,t426]) ).
cnf(t454,plain,
mult(sFlat0,mult(mult(sFlat0,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(rw,[status(thm)],[t37992]) ).
cnf(t1043,plain,
mult(sFlat0,mult(mult(sFlat0,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(orient,[status(thm)],[t454]) ).
cnf(t1075,plain,
mult(sFlat0,rd(mult(sFlat0,X1),sFlat0)) = rd(mult(mult(X1,sFlat0),x1),x1),
inference(cp,[status(thm)],[t803,t1043]) ).
cnf(t38021,plain,
mult(sFlat0,rd(mult(sFlat0,X1),sFlat0)) = mult(X1,sFlat0),
inference(step,[status(thm)],[t1075,t9]) ).
cnf(t1084,plain,
mult(sFlat0,rd(mult(sFlat0,X1),sFlat0)) = mult(X1,sFlat0),
inference(orient,[status(thm)],[t38021]) ).
cnf(t2779,plain,
mult(mult(X1,mult(sFlat0,sFlat0)),sFlat0) = mult(sFlat0,mult(mult(sFlat0,X1),sFlat0)),
inference(cp,[status(thm)],[t1084,t2659]) ).
cnf(t38046,plain,
mult(mult(X1,rd(sFlat0,sFlat0)),sFlat0) = mult(sFlat0,mult(mult(sFlat0,X1),sFlat0)),
inference(step,[status(thm)],[t2779,t388]) ).
cnf(t1111,plain,
rd(mult(sFlat0,X1),sFlat0) = mult(sFlat0,mult(X1,sFlat0)),
inference(cp,[status(thm)],[t404,t1084]) ).
cnf(t1156,plain,
mult(sFlat0,mult(X1,sFlat0)) = rd(mult(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t1111]) ).
cnf(t38047,plain,
mult(mult(X1,rd(sFlat0,sFlat0)),sFlat0) = rd(mult(sFlat0,mult(sFlat0,X1)),sFlat0),
inference(step,[status(thm)],[t38046,t1156]) ).
cnf(t38048,plain,
mult(mult(X1,rd(sFlat0,sFlat0)),sFlat0) = rd(X1,sFlat0),
inference(step,[status(thm)],[t38047,t404]) ).
cnf(t2784,plain,
mult(mult(X1,rd(sFlat0,sFlat0)),sFlat0) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t38048]) ).
cnf(t2791,plain,
mult(X1,rd(sFlat0,sFlat0)) = rd(rd(X1,sFlat0),sFlat0),
inference(cp,[status(thm)],[t9,t2784]) ).
cnf(t2806,plain,
mult(X1,rd(sFlat0,sFlat0)) = rd(rd(X1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t2791]) ).
cnf(t2810,plain,
rd(sFlat0,sFlat0) = ld(X1,rd(rd(X1,sFlat0),sFlat0)),
inference(cp,[status(thm)],[t11,t2806]) ).
cnf(t2822,plain,
ld(X1,rd(rd(X1,sFlat0),sFlat0)) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t2810]) ).
cnf(t2833,plain,
rd(sFlat0,sFlat0) = ld(mult(X1,sFlat0),rd(X1,sFlat0)),
inference(cp,[status(thm)],[t2822,t9]) ).
cnf(t2840,plain,
ld(mult(X1,sFlat0),rd(X1,sFlat0)) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t2833]) ).
cnf(t240,plain,
mult(mult(X1,X2),ld(X2,X3)) = mult(X2,mult(ld(X2,X1),X3)),
inference(cp,[status(thm)],[t225,t7]) ).
cnf(t3054,plain,
mult(mult(X1,X2),ld(X2,X3)) = mult(X2,mult(ld(X2,X1),X3)),
inference(orient,[status(thm)],[t240]) ).
cnf(t3129,plain,
mult(x1,mult(ld(x1,sFlat0),X1)) = mult(x1,ld(x1,X1)),
inference(cp,[status(thm)],[t3054,t28]) ).
cnf(t38061,plain,
mult(x1,mult(ld(x1,sFlat0),X1)) = X1,
inference(step,[status(thm)],[t3129,t7]) ).
cnf(t3174,plain,
mult(x1,mult(ld(x1,sFlat0),X1)) = X1,
inference(orient,[status(thm)],[t38061]) ).
cnf(t3180,plain,
mult(ld(x1,sFlat0),X1) = ld(x1,X1),
inference(cp,[status(thm)],[t11,t3174]) ).
cnf(t3197,plain,
mult(ld(x1,sFlat0),X1) = ld(x1,X1),
inference(orient,[status(thm)],[t3180]) ).
cnf(t3205,plain,
ld(x1,sFlat0) = rd(ld(x1,X1),X1),
inference(cp,[status(thm)],[t9,t3197]) ).
cnf(t3235,plain,
rd(ld(x1,X1),X1) = ld(x1,sFlat0),
inference(orient,[status(thm)],[t3205]) ).
cnf(t3238,plain,
rd(sFlat0,sFlat0) = ld(mult(ld(x1,sFlat0),sFlat0),ld(x1,sFlat0)),
inference(cp,[status(thm)],[t2840,t3235]) ).
cnf(t38062,plain,
rd(sFlat0,sFlat0) = ld(ld(x1,sFlat0),ld(x1,sFlat0)),
inference(step,[status(thm)],[t3238,t3197]) ).
cnf(t3176,plain,
ld(ld(x1,sFlat0),X1) = mult(x1,X1),
inference(cp,[status(thm)],[t3174,t7]) ).
cnf(t3191,plain,
ld(ld(x1,sFlat0),X1) = mult(x1,X1),
inference(orient,[status(thm)],[t3176]) ).
cnf(t38063,plain,
rd(sFlat0,sFlat0) = mult(x1,ld(x1,sFlat0)),
inference(step,[status(thm)],[t38062,t3191]) ).
cnf(t38064,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t38063,t7]) ).
cnf(t3252,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t38064]) ).
cnf(t15105,plain,
rd(mult(X1,sFlat0),ld(X1,sFlat0)) = mult(mult(X1,sFlat0),X1),
inference(cp,[status(thm)],[t15020,t3252]) ).
cnf(t15193,plain,
rd(mult(X1,sFlat0),ld(X1,sFlat0)) = mult(mult(X1,sFlat0),X1),
inference(orient,[status(thm)],[t15105]) ).
cnf(t15216,plain,
mult(mult(rd(X1,sFlat0),sFlat0),rd(X1,sFlat0)) = rd(X1,ld(rd(X1,sFlat0),sFlat0)),
inference(cp,[status(thm)],[t15193,t8]) ).
cnf(t38327,plain,
mult(X1,rd(X1,sFlat0)) = rd(X1,ld(rd(X1,sFlat0),sFlat0)),
inference(step,[status(thm)],[t15216,t8]) ).
cnf(t15365,plain,
rd(X1,ld(rd(X1,sFlat0),sFlat0)) = mult(X1,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t38327]) ).
cnf(t15380,plain,
ld(rd(X1,sFlat0),sFlat0) = ld(mult(X1,rd(X1,sFlat0)),X1),
inference(cp,[status(thm)],[t39,t15365]) ).
cnf(t15416,plain,
ld(mult(X1,rd(X1,sFlat0)),X1) = ld(rd(X1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t15380]) ).
cnf(t10,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t9,t7]) ).
cnf(t38,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t2854,plain,
mult(X1,sFlat0) = rd(rd(X1,sFlat0),rd(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t38,t2840]) ).
cnf(t2896,plain,
rd(rd(X1,sFlat0),rd(sFlat0,sFlat0)) = mult(X1,sFlat0),
inference(orient,[status(thm)],[t2854]) ).
cnf(t38079,plain,
rd(rd(X1,sFlat0),sFlat0) = mult(X1,sFlat0),
inference(step,[status(thm)],[t2896,t3252]) ).
cnf(t3267,plain,
rd(rd(X1,sFlat0),sFlat0) = mult(X1,sFlat0),
inference(rw,[status(thm)],[t38079]) ).
cnf(t3283,plain,
rd(rd(X1,sFlat0),sFlat0) = mult(X1,sFlat0),
inference(orient,[status(thm)],[t3267]) ).
cnf(t15431,plain,
ld(rd(rd(X1,sFlat0),sFlat0),sFlat0) = ld(mult(rd(X1,sFlat0),mult(X1,sFlat0)),rd(X1,sFlat0)),
inference(cp,[status(thm)],[t15416,t3283]) ).
cnf(t3136,plain,
mult(X1,mult(ld(X1,rd(X2,X1)),X3)) = mult(X2,ld(X1,X3)),
inference(cp,[status(thm)],[t3054,t8]) ).
cnf(t16517,plain,
mult(X1,mult(ld(X1,rd(X2,X1)),X3)) = mult(X2,ld(X1,X3)),
inference(orient,[status(thm)],[t3136]) ).
cnf(t16635,plain,
mult(ld(X1,rd(X2,X1)),X3) = ld(X1,mult(X2,ld(X1,X3))),
inference(cp,[status(thm)],[t11,t16517]) ).
cnf(t16676,plain,
ld(X1,mult(X2,ld(X1,X3))) = mult(ld(X1,rd(X2,X1)),X3),
inference(orient,[status(thm)],[t16635]) ).
cnf(t16677,plain,
mult(ld(X1,rd(X1,X1)),X2) = ld(X1,X2),
inference(cp,[status(thm)],[t16676,t11]) ).
cnf(t16843,plain,
mult(ld(X1,rd(X1,X1)),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t16677]) ).
cnf(t2853,plain,
rd(sFlat0,sFlat0) = ld(mult(mult(X1,sFlat0),sFlat0),X1),
inference(cp,[status(thm)],[t2840,t9]) ).
cnf(t2859,plain,
ld(mult(mult(X1,sFlat0),sFlat0),X1) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t2853]) ).
cnf(t2864,plain,
mult(mult(X1,sFlat0),sFlat0) = rd(X1,rd(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t38,t2859]) ).
cnf(t2866,plain,
mult(mult(X1,sFlat0),sFlat0) = rd(X1,rd(sFlat0,sFlat0)),
inference(orient,[status(thm)],[t2864]) ).
cnf(t38077,plain,
mult(mult(X1,sFlat0),sFlat0) = rd(X1,sFlat0),
inference(step,[status(thm)],[t2866,t3252]) ).
cnf(t3265,plain,
mult(mult(X1,sFlat0),sFlat0) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t38077]) ).
cnf(t16859,plain,
rd(ld(X1,rd(X1,X1)),sFlat0) = mult(ld(X1,sFlat0),sFlat0),
inference(cp,[status(thm)],[t3265,t16843]) ).
cnf(t16984,plain,
rd(ld(X1,rd(X1,X1)),sFlat0) = mult(ld(X1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t16859]) ).
cnf(t16988,plain,
ld(X1,rd(X1,X1)) = mult(mult(ld(X1,sFlat0),sFlat0),sFlat0),
inference(cp,[status(thm)],[t8,t16984]) ).
cnf(t38352,plain,
ld(X1,rd(X1,X1)) = rd(ld(X1,sFlat0),sFlat0),
inference(step,[status(thm)],[t16988,t3265]) ).
cnf(t17003,plain,
ld(X1,rd(X1,X1)) = rd(ld(X1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t38352]) ).
cnf(t38353,plain,
mult(rd(ld(X1,sFlat0),sFlat0),X2) = ld(X1,X2),
inference(step,[status(thm)],[t16843,t17003]) ).
cnf(t17028,plain,
mult(rd(ld(X1,sFlat0),sFlat0),X2) = ld(X1,X2),
inference(rw,[status(thm)],[t38353]) ).
cnf(t17074,plain,
mult(rd(ld(X1,sFlat0),sFlat0),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t17028]) ).
cnf(t17084,plain,
ld(rd(sFlat0,X1),X2) = mult(rd(X1,sFlat0),X2),
inference(cp,[status(thm)],[t17074,t39]) ).
cnf(t17143,plain,
ld(rd(sFlat0,X1),X2) = mult(rd(X1,sFlat0),X2),
inference(orient,[status(thm)],[t17084]) ).
cnf(t17158,plain,
rd(sFlat0,X1) = rd(X2,mult(rd(X1,sFlat0),X2)),
inference(cp,[status(thm)],[t38,t17143]) ).
cnf(t17164,plain,
rd(X1,mult(rd(X2,sFlat0),X1)) = rd(sFlat0,X2),
inference(orient,[status(thm)],[t17158]) ).
cnf(t17170,plain,
rd(sFlat0,X1) = rd(ld(rd(X1,sFlat0),X2),X2),
inference(cp,[status(thm)],[t17164,t7]) ).
cnf(t17195,plain,
rd(ld(rd(X1,sFlat0),X2),X2) = rd(sFlat0,X1),
inference(orient,[status(thm)],[t17170]) ).
cnf(t17214,plain,
rd(sFlat0,mult(X1,sFlat0)) = rd(ld(X1,X2),X2),
inference(cp,[status(thm)],[t17195,t9]) ).
cnf(t17240,plain,
rd(ld(X1,X2),X2) = rd(sFlat0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t17214]) ).
cnf(t17248,plain,
rd(sFlat0,mult(rd(sFlat0,X1),sFlat0)) = rd(mult(rd(X1,sFlat0),X2),X2),
inference(cp,[status(thm)],[t17240,t17143]) ).
cnf(t38358,plain,
rd(sFlat0,mult(rd(sFlat0,X1),sFlat0)) = rd(X1,sFlat0),
inference(step,[status(thm)],[t17248,t9]) ).
cnf(t17352,plain,
rd(sFlat0,mult(rd(sFlat0,X1),sFlat0)) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t38358]) ).
cnf(t17355,plain,
mult(rd(mult(rd(sFlat0,X1),sFlat0),sFlat0),X2) = ld(rd(X1,sFlat0),X2),
inference(cp,[status(thm)],[t17143,t17352]) ).
cnf(t38359,plain,
mult(rd(sFlat0,X1),X2) = ld(rd(X1,sFlat0),X2),
inference(step,[status(thm)],[t17355,t9]) ).
cnf(t17364,plain,
ld(rd(X1,sFlat0),X2) = mult(rd(sFlat0,X1),X2),
inference(orient,[status(thm)],[t38359]) ).
cnf(t38710,plain,
mult(rd(sFlat0,rd(X1,sFlat0)),sFlat0) = ld(mult(rd(X1,sFlat0),mult(X1,sFlat0)),rd(X1,sFlat0)),
inference(step,[status(thm)],[t15431,t17364]) ).
cnf(t17325,plain,
rd(sFlat0,mult(rd(X1,X2),sFlat0)) = rd(X2,X1),
inference(cp,[status(thm)],[t17240,t39]) ).
cnf(t17399,plain,
rd(sFlat0,mult(rd(X1,X2),sFlat0)) = rd(X2,X1),
inference(orient,[status(thm)],[t17325]) ).
cnf(t17447,plain,
mult(rd(mult(rd(X1,X2),sFlat0),sFlat0),X3) = ld(rd(X2,X1),X3),
inference(cp,[status(thm)],[t17143,t17399]) ).
cnf(t38364,plain,
mult(rd(X1,X2),X3) = ld(rd(X2,X1),X3),
inference(step,[status(thm)],[t17447,t9]) ).
cnf(t17456,plain,
ld(rd(X1,X2),X3) = mult(rd(X2,X1),X3),
inference(orient,[status(thm)],[t38364]) ).
cnf(t17495,plain,
mult(rd(sFlat0,rd(X1,sFlat0)),X2) = ld(mult(X1,sFlat0),X2),
inference(cp,[status(thm)],[t17456,t3283]) ).
cnf(t18240,plain,
mult(rd(sFlat0,rd(X1,sFlat0)),X2) = ld(mult(X1,sFlat0),X2),
inference(orient,[status(thm)],[t17495]) ).
cnf(t38711,plain,
ld(mult(X1,sFlat0),sFlat0) = ld(mult(rd(X1,sFlat0),mult(X1,sFlat0)),rd(X1,sFlat0)),
inference(step,[status(thm)],[t38710,t18240]) ).
cnf(t2671,plain,
mult(mult(X1,sFlat0),X1) = rd(mult(X1,rd(mult(sFlat0,X1),sFlat0)),sFlat0),
inference(cp,[status(thm)],[t2659,t1156]) ).
cnf(t14432,plain,
rd(mult(X1,rd(mult(sFlat0,X1),sFlat0)),sFlat0) = mult(mult(X1,sFlat0),X1),
inference(orient,[status(thm)],[t2671]) ).
cnf(t14442,plain,
mult(mult(mult(X1,mult(sFlat0,sFlat0)),sFlat0),mult(X1,mult(sFlat0,sFlat0))) = rd(mult(mult(X1,mult(sFlat0,sFlat0)),mult(mult(sFlat0,X1),sFlat0)),sFlat0),
inference(cp,[status(thm)],[t14432,t2659]) ).
cnf(t38065,plain,
mult(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t388,t3252]) ).
cnf(t3253,plain,
mult(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t38065]) ).
cnf(t38314,plain,
mult(mult(mult(X1,sFlat0),sFlat0),mult(X1,mult(sFlat0,sFlat0))) = rd(mult(mult(X1,mult(sFlat0,sFlat0)),mult(mult(sFlat0,X1),sFlat0)),sFlat0),
inference(step,[status(thm)],[t14442,t3253]) ).
cnf(t38315,plain,
mult(rd(X1,sFlat0),mult(X1,mult(sFlat0,sFlat0))) = rd(mult(mult(X1,mult(sFlat0,sFlat0)),mult(mult(sFlat0,X1),sFlat0)),sFlat0),
inference(step,[status(thm)],[t38314,t3265]) ).
cnf(t38316,plain,
mult(rd(X1,sFlat0),mult(X1,sFlat0)) = rd(mult(mult(X1,mult(sFlat0,sFlat0)),mult(mult(sFlat0,X1),sFlat0)),sFlat0),
inference(step,[status(thm)],[t38315,t3253]) ).
cnf(t38317,plain,
mult(rd(X1,sFlat0),mult(X1,sFlat0)) = rd(mult(mult(X1,sFlat0),mult(mult(sFlat0,X1),sFlat0)),sFlat0),
inference(step,[status(thm)],[t38316,t3253]) ).
cnf(t1098,plain,
mult(mult(sFlat0,X1),sFlat0) = mult(sFlat0,rd(X1,sFlat0)),
inference(cp,[status(thm)],[t1084,t404]) ).
cnf(t1125,plain,
mult(mult(sFlat0,X1),sFlat0) = mult(sFlat0,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t1098]) ).
cnf(t38318,plain,
mult(rd(X1,sFlat0),mult(X1,sFlat0)) = rd(mult(mult(X1,sFlat0),mult(sFlat0,rd(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t38317,t1125]) ).
cnf(t420,plain,
mult(mult(X1,sFlat0),mult(sFlat0,X2)) = mult(sFlat0,mult(ld(sFlat0,X1),X2)),
inference(cp,[status(thm)],[t225,t404]) ).
cnf(t38105,plain,
mult(mult(X1,sFlat0),mult(sFlat0,X2)) = mult(sFlat0,mult(mult(sFlat0,X1),X2)),
inference(step,[status(thm)],[t420,t426]) ).
cnf(t3877,plain,
mult(mult(X1,sFlat0),mult(sFlat0,X2)) = mult(sFlat0,mult(mult(sFlat0,X1),X2)),
inference(orient,[status(thm)],[t38105]) ).
cnf(t38319,plain,
mult(rd(X1,sFlat0),mult(X1,sFlat0)) = rd(mult(sFlat0,mult(mult(sFlat0,X1),rd(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t38318,t3877]) ).
cnf(t19,plain,
mult(mult(X1,X2),mult(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,mult(X2,mult(X1,mult(X1,X2)))),X3),
inference(cp,[status(thm)],[t13,t13]) ).
cnf(t3488,plain,
mult(mult(X1,mult(X2,mult(X1,mult(X1,X2)))),X3) = mult(mult(X1,X2),mult(X1,mult(mult(X1,X2),X3))),
inference(orient,[status(thm)],[t19]) ).
cnf(t3490,plain,
mult(mult(sFlat0,X1),mult(sFlat0,mult(mult(sFlat0,X1),sFlat0))) = mult(sFlat0,rd(mult(X1,mult(sFlat0,mult(sFlat0,X1))),sFlat0)),
inference(cp,[status(thm)],[t3488,t1125]) ).
cnf(t414,plain,
mult(ld(sFlat0,X1),mult(sFlat0,X2)) = mult(sFlat0,mult(mult(X1,sFlat0),X2)),
inference(cp,[status(thm)],[t404,t225]) ).
cnf(t38104,plain,
mult(mult(sFlat0,X1),mult(sFlat0,X2)) = mult(sFlat0,mult(mult(X1,sFlat0),X2)),
inference(step,[status(thm)],[t414,t426]) ).
cnf(t3779,plain,
mult(mult(sFlat0,X1),mult(sFlat0,X2)) = mult(sFlat0,mult(mult(X1,sFlat0),X2)),
inference(orient,[status(thm)],[t38104]) ).
cnf(t38243,plain,
mult(sFlat0,mult(mult(X1,sFlat0),mult(mult(sFlat0,X1),sFlat0))) = mult(sFlat0,rd(mult(X1,mult(sFlat0,mult(sFlat0,X1))),sFlat0)),
inference(step,[status(thm)],[t3490,t3779]) ).
cnf(t38244,plain,
mult(sFlat0,mult(mult(X1,sFlat0),mult(sFlat0,rd(X1,sFlat0)))) = mult(sFlat0,rd(mult(X1,mult(sFlat0,mult(sFlat0,X1))),sFlat0)),
inference(step,[status(thm)],[t38243,t1125]) ).
cnf(t38245,plain,
mult(sFlat0,mult(sFlat0,mult(mult(sFlat0,X1),rd(X1,sFlat0)))) = mult(sFlat0,rd(mult(X1,mult(sFlat0,mult(sFlat0,X1))),sFlat0)),
inference(step,[status(thm)],[t38244,t3877]) ).
cnf(t38246,plain,
mult(mult(sFlat0,X1),rd(X1,sFlat0)) = mult(sFlat0,rd(mult(X1,mult(sFlat0,mult(sFlat0,X1))),sFlat0)),
inference(step,[status(thm)],[t38245,t404]) ).
cnf(t38247,plain,
mult(mult(sFlat0,X1),rd(X1,sFlat0)) = mult(sFlat0,rd(mult(X1,X1),sFlat0)),
inference(step,[status(thm)],[t38246,t404]) ).
cnf(t7224,plain,
mult(mult(sFlat0,X1),rd(X1,sFlat0)) = mult(sFlat0,rd(mult(X1,X1),sFlat0)),
inference(orient,[status(thm)],[t38247]) ).
cnf(t38320,plain,
mult(rd(X1,sFlat0),mult(X1,sFlat0)) = rd(mult(sFlat0,mult(sFlat0,rd(mult(X1,X1),sFlat0))),sFlat0),
inference(step,[status(thm)],[t38319,t7224]) ).
cnf(t38321,plain,
mult(rd(X1,sFlat0),mult(X1,sFlat0)) = rd(rd(mult(X1,X1),sFlat0),sFlat0),
inference(step,[status(thm)],[t38320,t404]) ).
cnf(t38322,plain,
mult(rd(X1,sFlat0),mult(X1,sFlat0)) = mult(mult(X1,X1),sFlat0),
inference(step,[status(thm)],[t38321,t3283]) ).
cnf(t14553,plain,
mult(rd(X1,sFlat0),mult(X1,sFlat0)) = mult(mult(X1,X1),sFlat0),
inference(orient,[status(thm)],[t38322]) ).
cnf(t38712,plain,
ld(mult(X1,sFlat0),sFlat0) = ld(mult(mult(X1,X1),sFlat0),rd(X1,sFlat0)),
inference(step,[status(thm)],[t38711,t14553]) ).
cnf(t37225,plain,
ld(mult(mult(X1,X1),sFlat0),rd(X1,sFlat0)) = ld(mult(X1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t38712]) ).
cnf(t17004,plain,
rd(X1,X1) = mult(X1,rd(ld(X1,sFlat0),sFlat0)),
inference(cp,[status(thm)],[t7,t17003]) ).
cnf(t17029,plain,
mult(X1,rd(ld(X1,sFlat0),sFlat0)) = rd(X1,X1),
inference(orient,[status(thm)],[t17004]) ).
cnf(t38357,plain,
mult(X1,rd(sFlat0,mult(X1,sFlat0))) = rd(X1,X1),
inference(step,[status(thm)],[t17029,t17240]) ).
cnf(t17351,plain,
mult(X1,rd(sFlat0,mult(X1,sFlat0))) = rd(X1,X1),
inference(rw,[status(thm)],[t38357]) ).
cnf(t17627,plain,
mult(X1,rd(sFlat0,mult(X1,sFlat0))) = rd(X1,X1),
inference(orient,[status(thm)],[t17351]) ).
cnf(t17526,plain,
rd(X1,X2) = rd(X3,mult(rd(X2,X1),X3)),
inference(cp,[status(thm)],[t38,t17456]) ).
cnf(t17963,plain,
rd(X1,mult(rd(X2,X3),X1)) = rd(X3,X2),
inference(orient,[status(thm)],[t17526]) ).
cnf(t18047,plain,
rd(rd(X1,X2),rd(X1,X2)) = mult(rd(X1,X2),rd(X2,X1)),
inference(cp,[status(thm)],[t17627,t17963]) ).
cnf(t20348,plain,
mult(rd(X1,X2),rd(X2,X1)) = rd(rd(X1,X2),rd(X1,X2)),
inference(orient,[status(thm)],[t18047]) ).
cnf(t37241,plain,
ld(mult(rd(X1,X1),sFlat0),sFlat0) = ld(mult(rd(rd(X1,X1),rd(X1,X1)),sFlat0),rd(rd(X1,X1),sFlat0)),
inference(cp,[status(thm)],[t37225,t20348]) ).
cnf(t17667,plain,
mult(rd(sFlat0,mult(X1,sFlat0)),mult(ld(rd(sFlat0,mult(X1,sFlat0)),X1),X2)) = mult(rd(X1,X1),ld(rd(sFlat0,mult(X1,sFlat0)),X2)),
inference(cp,[status(thm)],[t3054,t17627]) ).
cnf(t17331,plain,
ld(X1,X2) = mult(rd(sFlat0,mult(X1,sFlat0)),X2),
inference(cp,[status(thm)],[t8,t17240]) ).
cnf(t17532,plain,
mult(rd(sFlat0,mult(X1,sFlat0)),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t17331]) ).
cnf(t38493,plain,
ld(X1,mult(ld(rd(sFlat0,mult(X1,sFlat0)),X1),X2)) = mult(rd(X1,X1),ld(rd(sFlat0,mult(X1,sFlat0)),X2)),
inference(step,[status(thm)],[t17667,t17532]) ).
cnf(t38494,plain,
ld(X1,mult(mult(rd(mult(X1,sFlat0),sFlat0),X1),X2)) = mult(rd(X1,X1),ld(rd(sFlat0,mult(X1,sFlat0)),X2)),
inference(step,[status(thm)],[t38493,t17143]) ).
cnf(t259,plain,
mult(ld(X1,X2),mult(X1,X3)) = ld(X1,mult(mult(X2,X1),X3)),
inference(cp,[status(thm)],[t11,t225]) ).
cnf(t3682,plain,
ld(X1,mult(mult(X2,X1),X3)) = mult(ld(X1,X2),mult(X1,X3)),
inference(orient,[status(thm)],[t259]) ).
cnf(t38495,plain,
mult(ld(X1,rd(mult(X1,sFlat0),sFlat0)),mult(X1,X2)) = mult(rd(X1,X1),ld(rd(sFlat0,mult(X1,sFlat0)),X2)),
inference(step,[status(thm)],[t38494,t3682]) ).
cnf(t38496,plain,
mult(ld(X1,X1),mult(X1,X2)) = mult(rd(X1,X1),ld(rd(sFlat0,mult(X1,sFlat0)),X2)),
inference(step,[status(thm)],[t38495,t9]) ).
cnf(t38497,plain,
mult(ld(X1,X1),mult(X1,X2)) = mult(rd(X1,X1),mult(rd(mult(X1,sFlat0),sFlat0),X2)),
inference(step,[status(thm)],[t38496,t17143]) ).
cnf(t38498,plain,
mult(ld(X1,X1),mult(X1,X2)) = mult(rd(X1,X1),mult(X1,X2)),
inference(step,[status(thm)],[t38497,t9]) ).
cnf(t19947,plain,
mult(ld(X1,X1),mult(X1,X2)) = mult(rd(X1,X1),mult(X1,X2)),
inference(orient,[status(thm)],[t38498]) ).
cnf(t20064,plain,
ld(X1,X1) = rd(mult(rd(X1,X1),mult(X1,X2)),mult(X1,X2)),
inference(cp,[status(thm)],[t9,t19947]) ).
cnf(t38499,plain,
ld(X1,X1) = rd(X1,X1),
inference(step,[status(thm)],[t20064,t9]) ).
cnf(t20090,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t38499]) ).
cnf(t20100,plain,
mult(X1,mult(ld(X1,X2),X1)) = mult(mult(X2,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t3054,t20090]) ).
cnf(t21372,plain,
mult(mult(X1,X2),rd(X2,X2)) = mult(X2,mult(ld(X2,X1),X2)),
inference(orient,[status(thm)],[t20100]) ).
cnf(t20096,plain,
X1 = mult(X1,rd(X1,X1)),
inference(cp,[status(thm)],[t7,t20090]) ).
cnf(t20120,plain,
mult(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t20096]) ).
cnf(t21379,plain,
mult(rd(X1,X1),mult(ld(rd(X1,X1),X1),rd(X1,X1))) = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(cp,[status(thm)],[t21372,t20120]) ).
cnf(t38518,plain,
mult(rd(X1,X1),mult(mult(rd(X1,X1),X1),rd(X1,X1))) = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t21379,t17456]) ).
cnf(t38519,plain,
mult(rd(X1,X1),mult(X1,rd(X1,X1))) = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t38518,t8]) ).
cnf(t38520,plain,
mult(rd(X1,X1),X1) = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t38519,t20120]) ).
cnf(t38521,plain,
X1 = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t38520,t8]) ).
cnf(t21611,plain,
mult(X1,rd(rd(X1,X1),rd(X1,X1))) = X1,
inference(orient,[status(thm)],[t38521]) ).
cnf(t21636,plain,
rd(rd(X1,X1),rd(X1,X1)) = ld(X1,X1),
inference(cp,[status(thm)],[t11,t21611]) ).
cnf(t38522,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(step,[status(thm)],[t21636,t20090]) ).
cnf(t21674,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t38522]) ).
cnf(t38713,plain,
ld(mult(rd(X1,X1),sFlat0),sFlat0) = ld(mult(rd(X1,X1),sFlat0),rd(rd(X1,X1),sFlat0)),
inference(step,[status(thm)],[t37241,t21674]) ).
cnf(t38075,plain,
ld(mult(X1,sFlat0),rd(X1,sFlat0)) = sFlat0,
inference(step,[status(thm)],[t2840,t3252]) ).
cnf(t3263,plain,
ld(mult(X1,sFlat0),rd(X1,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t38075]) ).
cnf(t38714,plain,
ld(mult(rd(X1,X1),sFlat0),sFlat0) = sFlat0,
inference(step,[status(thm)],[t38713,t3263]) ).
cnf(t37280,plain,
ld(mult(rd(X1,X1),sFlat0),sFlat0) = sFlat0,
inference(orient,[status(thm)],[t38714]) ).
cnf(t37283,plain,
sFlat0 = mult(mult(rd(X1,X1),sFlat0),sFlat0),
inference(cp,[status(thm)],[t7,t37280]) ).
cnf(t38715,plain,
sFlat0 = rd(rd(X1,X1),sFlat0),
inference(step,[status(thm)],[t37283,t3265]) ).
cnf(t37297,plain,
rd(rd(X1,X1),sFlat0) = sFlat0,
inference(orient,[status(thm)],[t38715]) ).
cnf(t37315,plain,
rd(X1,X1) = mult(sFlat0,sFlat0),
inference(cp,[status(thm)],[t8,t37297]) ).
cnf(t38738,plain,
rd(X1,X1) = sFlat0,
inference(step,[status(thm)],[t37315,t3253]) ).
cnf(t37349,plain,
rd(X1,X1) = sFlat0,
inference(orient,[status(thm)],[t38738]) ).
cnf(t2755,plain,
mult(mult(sFlat0,X1),sFlat0) = rd(mult(sFlat0,mult(X1,X2)),mult(sFlat0,X2)),
inference(cp,[status(thm)],[t2659,t404]) ).
cnf(t38349,plain,
mult(sFlat0,rd(X1,sFlat0)) = rd(mult(sFlat0,mult(X1,X2)),mult(sFlat0,X2)),
inference(step,[status(thm)],[t2755,t1125]) ).
cnf(t16380,plain,
rd(mult(sFlat0,mult(X1,X2)),mult(sFlat0,X2)) = mult(sFlat0,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t38349]) ).
cnf(t6,axiom,
sFlat1 = mult(rd(x1,x1),x0),
introduced(definition) ).
cnf(t21,plain,
mult(rd(x1,x1),x0) = sFlat1,
inference(orient,[status(thm)],[t6]) ).
cnf(t37957,plain,
mult(sFlat0,x0) = sFlat1,
inference(step,[status(thm)],[t21,t25]) ).
cnf(t27,plain,
mult(sFlat0,x0) = sFlat1,
inference(rw,[status(thm)],[t37957]) ).
cnf(t31,plain,
mult(sFlat0,x0) = sFlat1,
inference(orient,[status(thm)],[t27]) ).
cnf(t251,plain,
mult(mult(X1,sFlat0),x0) = mult(sFlat0,mult(ld(sFlat0,X1),sFlat1)),
inference(cp,[status(thm)],[t225,t31]) ).
cnf(t288,plain,
mult(sFlat0,mult(ld(sFlat0,X1),sFlat1)) = mult(mult(X1,sFlat0),x0),
inference(orient,[status(thm)],[t251]) ).
cnf(t295,plain,
mult(ld(sFlat0,X1),sFlat1) = ld(sFlat0,mult(mult(X1,sFlat0),x0)),
inference(cp,[status(thm)],[t11,t288]) ).
cnf(t318,plain,
ld(sFlat0,mult(mult(X1,sFlat0),x0)) = mult(ld(sFlat0,X1),sFlat1),
inference(orient,[status(thm)],[t295]) ).
cnf(t321,plain,
mult(ld(sFlat0,rd(X1,sFlat0)),sFlat1) = ld(sFlat0,mult(X1,x0)),
inference(cp,[status(thm)],[t318,t8]) ).
cnf(t338,plain,
mult(ld(sFlat0,rd(X1,sFlat0)),sFlat1) = ld(sFlat0,mult(X1,x0)),
inference(orient,[status(thm)],[t321]) ).
cnf(t357,plain,
ld(sFlat0,mult(sFlat0,x0)) = mult(sFlat0,sFlat1),
inference(cp,[status(thm)],[t338,t352]) ).
cnf(t37959,plain,
x0 = mult(sFlat0,sFlat1),
inference(step,[status(thm)],[t357,t11]) ).
cnf(t364,plain,
mult(sFlat0,sFlat1) = x0,
inference(orient,[status(thm)],[t37959]) ).
cnf(t369,plain,
mult(sFlat0,mult(sFlat1,mult(sFlat0,X1))) = mult(mult(x0,sFlat0),X1),
inference(cp,[status(thm)],[t13,t364]) ).
cnf(t519,plain,
mult(sFlat0,mult(sFlat1,mult(sFlat0,X1))) = mult(mult(x0,sFlat0),X1),
inference(orient,[status(thm)],[t369]) ).
cnf(t535,plain,
mult(sFlat1,mult(sFlat0,X1)) = mult(sFlat0,mult(mult(x0,sFlat0),X1)),
inference(cp,[status(thm)],[t404,t519]) ).
cnf(t1319,plain,
mult(sFlat0,mult(mult(x0,sFlat0),X1)) = mult(sFlat1,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t535]) ).
cnf(t1320,plain,
mult(sFlat1,mult(sFlat0,ld(mult(x0,sFlat0),X1))) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t1319,t7]) ).
cnf(t9495,plain,
mult(sFlat1,mult(sFlat0,ld(mult(x0,sFlat0),X1))) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t1320]) ).
cnf(t9500,plain,
mult(sFlat0,ld(mult(x0,sFlat0),X1)) = ld(sFlat1,mult(sFlat0,X1)),
inference(cp,[status(thm)],[t11,t9495]) ).
cnf(t9512,plain,
mult(sFlat0,ld(mult(x0,sFlat0),X1)) = ld(sFlat1,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t9500]) ).
cnf(t9525,plain,
ld(mult(x0,sFlat0),X1) = mult(sFlat0,ld(sFlat1,mult(sFlat0,X1))),
inference(cp,[status(thm)],[t404,t9512]) ).
cnf(t9567,plain,
mult(sFlat0,ld(sFlat1,mult(sFlat0,X1))) = ld(mult(x0,sFlat0),X1),
inference(orient,[status(thm)],[t9525]) ).
cnf(t9643,plain,
ld(mult(x0,sFlat0),mult(sFlat0,X1)) = mult(sFlat0,ld(sFlat1,X1)),
inference(cp,[status(thm)],[t9567,t404]) ).
cnf(t9740,plain,
ld(mult(x0,sFlat0),mult(sFlat0,X1)) = mult(sFlat0,ld(sFlat1,X1)),
inference(orient,[status(thm)],[t9643]) ).
cnf(t3686,plain,
mult(ld(X1,sFlat0),mult(X1,sFlat0)) = ld(X1,mult(sFlat0,rd(X1,sFlat0))),
inference(cp,[status(thm)],[t3682,t1125]) ).
cnf(t7323,plain,
ld(X1,mult(sFlat0,rd(X1,sFlat0))) = mult(ld(X1,sFlat0),mult(X1,sFlat0)),
inference(orient,[status(thm)],[t3686]) ).
cnf(t9741,plain,
mult(sFlat0,ld(sFlat1,rd(mult(x0,sFlat0),sFlat0))) = mult(ld(mult(x0,sFlat0),sFlat0),mult(mult(x0,sFlat0),sFlat0)),
inference(cp,[status(thm)],[t9740,t7323]) ).
cnf(t38623,plain,
mult(sFlat0,ld(sFlat1,x0)) = mult(ld(mult(x0,sFlat0),sFlat0),mult(mult(x0,sFlat0),sFlat0)),
inference(step,[status(thm)],[t9741,t9]) ).
cnf(t9644,plain,
ld(mult(x0,sFlat0),sFlat0) = mult(sFlat0,ld(sFlat1,sFlat0)),
inference(cp,[status(thm)],[t9567,t3253]) ).
cnf(t9708,plain,
ld(mult(x0,sFlat0),sFlat0) = mult(sFlat0,ld(sFlat1,sFlat0)),
inference(orient,[status(thm)],[t9644]) ).
cnf(t38624,plain,
mult(sFlat0,ld(sFlat1,x0)) = mult(mult(sFlat0,ld(sFlat1,sFlat0)),mult(mult(x0,sFlat0),sFlat0)),
inference(step,[status(thm)],[t38623,t9708]) ).
cnf(t38625,plain,
mult(sFlat0,ld(sFlat1,x0)) = mult(mult(sFlat0,ld(sFlat1,sFlat0)),rd(x0,sFlat0)),
inference(step,[status(thm)],[t38624,t3265]) ).
cnf(t26380,plain,
mult(mult(sFlat0,ld(sFlat1,sFlat0)),rd(x0,sFlat0)) = mult(sFlat0,ld(sFlat1,x0)),
inference(orient,[status(thm)],[t38625]) ).
cnf(t26393,plain,
mult(sFlat0,rd(mult(sFlat0,ld(sFlat1,sFlat0)),sFlat0)) = rd(mult(sFlat0,mult(sFlat0,ld(sFlat1,x0))),mult(sFlat0,rd(x0,sFlat0))),
inference(cp,[status(thm)],[t16380,t26380]) ).
cnf(t38626,plain,
mult(ld(sFlat1,sFlat0),sFlat0) = rd(mult(sFlat0,mult(sFlat0,ld(sFlat1,x0))),mult(sFlat0,rd(x0,sFlat0))),
inference(step,[status(thm)],[t26393,t1084]) ).
cnf(t38627,plain,
mult(ld(sFlat1,sFlat0),sFlat0) = rd(ld(sFlat1,x0),mult(sFlat0,rd(x0,sFlat0))),
inference(step,[status(thm)],[t38626,t404]) ).
cnf(t34,plain,
mult(sFlat0,mult(x0,mult(sFlat0,X1))) = mult(mult(sFlat1,sFlat0),X1),
inference(cp,[status(thm)],[t13,t31]) ).
cnf(t61,plain,
mult(sFlat0,mult(x0,mult(sFlat0,X1))) = mult(mult(sFlat1,sFlat0),X1),
inference(orient,[status(thm)],[t34]) ).
cnf(t63,plain,
mult(mult(sFlat1,sFlat0),x1) = mult(sFlat0,mult(x0,x1)),
inference(cp,[status(thm)],[t61,t28]) ).
cnf(t71,plain,
mult(mult(sFlat1,sFlat0),x1) = mult(sFlat0,mult(x0,x1)),
inference(orient,[status(thm)],[t63]) ).
cnf(t73,plain,
mult(sFlat1,sFlat0) = rd(mult(sFlat0,mult(x0,x1)),x1),
inference(cp,[status(thm)],[t9,t71]) ).
cnf(t79,plain,
rd(mult(sFlat0,mult(x0,x1)),x1) = mult(sFlat1,sFlat0),
inference(orient,[status(thm)],[t73]) ).
cnf(t38015,plain,
mult(sFlat0,rd(x0,sFlat0)) = mult(sFlat1,sFlat0),
inference(step,[status(thm)],[t79,t803]) ).
cnf(t812,plain,
mult(sFlat0,rd(x0,sFlat0)) = mult(sFlat1,sFlat0),
inference(rw,[status(thm)],[t38015]) ).
cnf(t831,plain,
mult(sFlat0,rd(x0,sFlat0)) = mult(sFlat1,sFlat0),
inference(orient,[status(thm)],[t812]) ).
cnf(t38628,plain,
mult(ld(sFlat1,sFlat0),sFlat0) = rd(ld(sFlat1,x0),mult(sFlat1,sFlat0)),
inference(step,[status(thm)],[t38627,t831]) ).
cnf(t26407,plain,
rd(ld(sFlat1,x0),mult(sFlat1,sFlat0)) = mult(ld(sFlat1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t38628]) ).
cnf(t26411,plain,
ld(sFlat1,x0) = mult(mult(ld(sFlat1,sFlat0),sFlat0),mult(sFlat1,sFlat0)),
inference(cp,[status(thm)],[t8,t26407]) ).
cnf(t26439,plain,
mult(mult(ld(sFlat1,sFlat0),sFlat0),mult(sFlat1,sFlat0)) = ld(sFlat1,x0),
inference(orient,[status(thm)],[t26411]) ).
cnf(t26455,plain,
mult(mult(sFlat1,mult(ld(sFlat1,sFlat0),sFlat0)),sFlat1) = rd(mult(sFlat1,ld(sFlat1,x0)),sFlat0),
inference(cp,[status(thm)],[t2659,t26439]) ).
cnf(t3123,plain,
mult(sFlat1,mult(ld(sFlat1,sFlat0),X1)) = mult(x0,ld(sFlat1,X1)),
inference(cp,[status(thm)],[t3054,t364]) ).
cnf(t3403,plain,
mult(sFlat1,mult(ld(sFlat1,sFlat0),X1)) = mult(x0,ld(sFlat1,X1)),
inference(orient,[status(thm)],[t3123]) ).
cnf(t38631,plain,
mult(mult(x0,ld(sFlat1,sFlat0)),sFlat1) = rd(mult(sFlat1,ld(sFlat1,x0)),sFlat0),
inference(step,[status(thm)],[t26455,t3403]) ).
cnf(t38632,plain,
mult(mult(x0,ld(sFlat1,sFlat0)),sFlat1) = rd(x0,sFlat0),
inference(step,[status(thm)],[t38631,t7]) ).
cnf(t26465,plain,
mult(mult(x0,ld(sFlat1,sFlat0)),sFlat1) = rd(x0,sFlat0),
inference(orient,[status(thm)],[t38632]) ).
cnf(t26471,plain,
mult(x0,ld(sFlat1,sFlat0)) = rd(rd(x0,sFlat0),sFlat1),
inference(cp,[status(thm)],[t9,t26465]) ).
cnf(t26494,plain,
mult(x0,ld(sFlat1,sFlat0)) = rd(rd(x0,sFlat0),sFlat1),
inference(orient,[status(thm)],[t26471]) ).
cnf(t26502,plain,
x0 = rd(rd(rd(x0,sFlat0),sFlat1),ld(sFlat1,sFlat0)),
inference(cp,[status(thm)],[t9,t26494]) ).
cnf(t26554,plain,
rd(rd(rd(x0,sFlat0),sFlat1),ld(sFlat1,sFlat0)) = x0,
inference(orient,[status(thm)],[t26502]) ).
cnf(t3130,plain,
mult(x0,mult(ld(x0,sFlat0),X1)) = mult(sFlat1,ld(x0,X1)),
inference(cp,[status(thm)],[t3054,t31]) ).
cnf(t3419,plain,
mult(x0,mult(ld(x0,sFlat0),X1)) = mult(sFlat1,ld(x0,X1)),
inference(orient,[status(thm)],[t3130]) ).
cnf(t3420,plain,
mult(sFlat1,ld(x0,ld(ld(x0,sFlat0),X1))) = mult(x0,X1),
inference(cp,[status(thm)],[t3419,t7]) ).
cnf(t9929,plain,
mult(sFlat1,ld(x0,ld(ld(x0,sFlat0),X1))) = mult(x0,X1),
inference(orient,[status(thm)],[t3420]) ).
cnf(t9934,plain,
ld(x0,ld(ld(x0,sFlat0),X1)) = ld(sFlat1,mult(x0,X1)),
inference(cp,[status(thm)],[t11,t9929]) ).
cnf(t9946,plain,
ld(x0,ld(ld(x0,sFlat0),X1)) = ld(sFlat1,mult(x0,X1)),
inference(orient,[status(thm)],[t9934]) ).
cnf(t9949,plain,
ld(ld(x0,sFlat0),X1) = mult(x0,ld(sFlat1,mult(x0,X1))),
inference(cp,[status(thm)],[t7,t9946]) ).
cnf(t9954,plain,
mult(x0,ld(sFlat1,mult(x0,X1))) = ld(ld(x0,sFlat0),X1),
inference(orient,[status(thm)],[t9949]) ).
cnf(t9956,plain,
ld(ld(x0,sFlat0),ld(x0,X1)) = mult(x0,ld(sFlat1,X1)),
inference(cp,[status(thm)],[t9954,t7]) ).
cnf(t9974,plain,
ld(ld(x0,sFlat0),ld(x0,X1)) = mult(x0,ld(sFlat1,X1)),
inference(orient,[status(thm)],[t9956]) ).
cnf(t20094,plain,
rd(ld(x0,sFlat0),ld(x0,sFlat0)) = mult(x0,ld(sFlat1,sFlat0)),
inference(cp,[status(thm)],[t20090,t9974]) ).
cnf(t20314,plain,
rd(ld(x0,sFlat0),ld(x0,sFlat0)) = mult(x0,ld(sFlat1,sFlat0)),
inference(orient,[status(thm)],[t20094]) ).
cnf(t20318,plain,
mult(rd(ld(x0,sFlat0),ld(x0,sFlat0)),X1) = ld(mult(x0,ld(sFlat1,sFlat0)),X1),
inference(cp,[status(thm)],[t17456,t20314]) ).
cnf(t38526,plain,
mult(mult(x0,ld(sFlat1,sFlat0)),X1) = ld(mult(x0,ld(sFlat1,sFlat0)),X1),
inference(step,[status(thm)],[t20318,t20314]) ).
cnf(t22097,plain,
ld(mult(x0,ld(sFlat1,sFlat0)),X1) = mult(mult(x0,ld(sFlat1,sFlat0)),X1),
inference(orient,[status(thm)],[t38526]) ).
cnf(t38636,plain,
ld(rd(rd(x0,sFlat0),sFlat1),X1) = mult(mult(x0,ld(sFlat1,sFlat0)),X1),
inference(step,[status(thm)],[t22097,t26494]) ).
cnf(t38637,plain,
mult(rd(sFlat1,rd(x0,sFlat0)),X1) = mult(mult(x0,ld(sFlat1,sFlat0)),X1),
inference(step,[status(thm)],[t38636,t17456]) ).
cnf(t38638,plain,
mult(rd(sFlat1,rd(x0,sFlat0)),X1) = mult(rd(rd(x0,sFlat0),sFlat1),X1),
inference(step,[status(thm)],[t38637,t26494]) ).
cnf(t26529,plain,
mult(rd(sFlat1,rd(x0,sFlat0)),X1) = mult(rd(rd(x0,sFlat0),sFlat1),X1),
inference(rw,[status(thm)],[t38638]) ).
cnf(t26571,plain,
mult(rd(rd(x0,sFlat0),sFlat1),X1) = mult(rd(sFlat1,rd(x0,sFlat0)),X1),
inference(orient,[status(thm)],[t26529]) ).
cnf(t26603,plain,
rd(rd(x0,sFlat0),sFlat1) = rd(mult(rd(sFlat1,rd(x0,sFlat0)),X1),X1),
inference(cp,[status(thm)],[t9,t26571]) ).
cnf(t38640,plain,
rd(rd(x0,sFlat0),sFlat1) = rd(sFlat1,rd(x0,sFlat0)),
inference(step,[status(thm)],[t26603,t9]) ).
cnf(t26680,plain,
rd(rd(x0,sFlat0),sFlat1) = rd(sFlat1,rd(x0,sFlat0)),
inference(orient,[status(thm)],[t38640]) ).
cnf(t38647,plain,
rd(rd(sFlat1,rd(x0,sFlat0)),ld(sFlat1,sFlat0)) = x0,
inference(step,[status(thm)],[t26554,t26680]) ).
cnf(t26700,plain,
rd(rd(sFlat1,rd(x0,sFlat0)),ld(sFlat1,sFlat0)) = x0,
inference(rw,[status(thm)],[t38647]) ).
cnf(t26782,plain,
rd(rd(sFlat1,rd(x0,sFlat0)),ld(sFlat1,sFlat0)) = x0,
inference(orient,[status(thm)],[t26700]) ).
cnf(t15160,plain,
mult(X1,rd(X2,X3)) = rd(rd(mult(X1,X2),ld(X1,X3)),X1),
inference(cp,[status(thm)],[t9,t15020]) ).
cnf(t32969,plain,
rd(rd(mult(X1,X2),ld(X1,X3)),X1) = mult(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t15160]) ).
cnf(t33259,plain,
mult(sFlat0,rd(mult(sFlat0,X1),X2)) = rd(rd(X1,ld(sFlat0,X2)),sFlat0),
inference(cp,[status(thm)],[t32969,t404]) ).
cnf(t38680,plain,
mult(sFlat0,rd(mult(sFlat0,X1),X2)) = rd(rd(X1,mult(sFlat0,X2)),sFlat0),
inference(step,[status(thm)],[t33259,t426]) ).
cnf(t34672,plain,
mult(sFlat0,rd(mult(sFlat0,X1),X2)) = rd(rd(X1,mult(sFlat0,X2)),sFlat0),
inference(orient,[status(thm)],[t38680]) ).
cnf(t20101,plain,
X1 = rd(X1,rd(X1,X1)),
inference(cp,[status(thm)],[t38,t20090]) ).
cnf(t20166,plain,
rd(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t20101]) ).
cnf(t34673,plain,
rd(rd(X1,mult(sFlat0,rd(mult(sFlat0,X1),mult(sFlat0,X1)))),sFlat0) = mult(sFlat0,mult(sFlat0,X1)),
inference(cp,[status(thm)],[t34672,t20166]) ).
cnf(t15158,plain,
rd(mult(sFlat0,mult(sFlat0,rd(X1,X2))),sFlat0) = mult(sFlat0,rd(mult(sFlat0,X1),ld(sFlat0,X2))),
inference(cp,[status(thm)],[t1156,t15020]) ).
cnf(t38673,plain,
rd(rd(X1,X2),sFlat0) = mult(sFlat0,rd(mult(sFlat0,X1),ld(sFlat0,X2))),
inference(step,[status(thm)],[t15158,t404]) ).
cnf(t38674,plain,
rd(rd(X1,X2),sFlat0) = mult(sFlat0,rd(mult(sFlat0,X1),mult(sFlat0,X2))),
inference(step,[status(thm)],[t38673,t426]) ).
cnf(t28198,plain,
mult(sFlat0,rd(mult(sFlat0,X1),mult(sFlat0,X2))) = rd(rd(X1,X2),sFlat0),
inference(orient,[status(thm)],[t38674]) ).
cnf(t38681,plain,
rd(rd(X1,rd(rd(X1,X1),sFlat0)),sFlat0) = mult(sFlat0,mult(sFlat0,X1)),
inference(step,[status(thm)],[t34673,t28198]) ).
cnf(t38682,plain,
rd(rd(X1,rd(rd(X1,X1),sFlat0)),sFlat0) = X1,
inference(step,[status(thm)],[t38681,t404]) ).
cnf(t34911,plain,
rd(rd(X1,rd(rd(X1,X1),sFlat0)),sFlat0) = X1,
inference(orient,[status(thm)],[t38682]) ).
cnf(t34926,plain,
rd(X1,rd(rd(X1,X1),sFlat0)) = mult(X1,sFlat0),
inference(cp,[status(thm)],[t8,t34911]) ).
cnf(t34947,plain,
rd(X1,rd(rd(X1,X1),sFlat0)) = mult(X1,sFlat0),
inference(orient,[status(thm)],[t34926]) ).
cnf(t34956,plain,
X1 = mult(mult(X1,sFlat0),rd(rd(X1,X1),sFlat0)),
inference(cp,[status(thm)],[t8,t34947]) ).
cnf(t35035,plain,
mult(mult(X1,sFlat0),rd(rd(X1,X1),sFlat0)) = X1,
inference(orient,[status(thm)],[t34956]) ).
cnf(t38722,plain,
mult(mult(X1,sFlat0),sFlat0) = X1,
inference(step,[status(thm)],[t35035,t37297]) ).
cnf(t38723,plain,
rd(X1,sFlat0) = X1,
inference(step,[status(thm)],[t38722,t3265]) ).
cnf(t37338,plain,
rd(X1,sFlat0) = X1,
inference(rw,[status(thm)],[t38723]) ).
cnf(t37403,plain,
rd(X1,sFlat0) = X1,
inference(orient,[status(thm)],[t37338]) ).
cnf(t39085,plain,
rd(rd(sFlat1,x0),ld(sFlat1,sFlat0)) = x0,
inference(step,[status(thm)],[t26782,t37403]) ).
cnf(t33,plain,
sFlat0 = rd(sFlat1,x0),
inference(cp,[status(thm)],[t9,t31]) ).
cnf(t37,plain,
rd(sFlat1,x0) = sFlat0,
inference(orient,[status(thm)],[t33]) ).
cnf(t39086,plain,
rd(sFlat0,ld(sFlat1,sFlat0)) = x0,
inference(step,[status(thm)],[t39085,t37]) ).
cnf(t39087,plain,
sFlat1 = x0,
inference(step,[status(thm)],[t39086,t38]) ).
cnf(t37658,plain,
sFlat1 = x0,
inference(rw,[status(thm)],[t39087]) ).
cnf(t37749,plain,
x0 = sFlat1,
inference(orient,[status(thm)],[t37658]) ).
cnf(t39240,plain,
mult(sFlat0,sFlat1) = sFlat1,
inference(step,[status(thm)],[t364,t37749]) ).
cnf(t37758,plain,
mult(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t39240]) ).
cnf(goal_0,negated_conjecture,
mult(rd(x1,x1),x0) != x0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(sFlat0,x0) != x0,
inference(rw,[status(thm)],[goal_0,t37349]) ).
cnf(g0_1,plain,
mult(sFlat0,sFlat1) != x0,
inference(rw,[status(thm)],[g0_0,t37749]) ).
cnf(g0_2,plain,
sFlat1 != x0,
inference(rw,[status(thm)],[g0_1,t37758]) ).
cnf(g0_3,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_2,t37749]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP654-12 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.38 % Computer : n004.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Wed Sep 23 15:29:51 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 18.79/2.86 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.79/2.86 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------