%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP655-14 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:27:52 PM UTC 2026
% Result : Unsatisfiable 37.51s 5.30s
% Output : CNFRefutation 37.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 8
% Syntax : Number of clauses : 309 ( 309 unt; 0 nHn; 107 RR)
% Number of literals : 309 ( 308 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 338 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t0]) ).
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(t10,plain,
X1 = ld(rd(X2,X1),X2),
inference(cp,[status(thm)],[t9,t8]) ).
cnf(t38,plain,
ld(rd(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t3,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t3]) ).
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(t12,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t11,t7]) ).
cnf(t39,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t4,axiom,
mult(mult(mult(X1,X2),X3),X2) = mult(X1,mult(X2,mult(X3,X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(mult(mult(X1,X2),X3),X2) = mult(X1,mult(X2,mult(X3,X2))),
inference(orient,[status(thm)],[t4]) ).
cnf(t16,plain,
mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(cp,[status(thm)],[t13,t8]) ).
cnf(t233,plain,
mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(orient,[status(thm)],[t16]) ).
cnf(t14,plain,
mult(X1,mult(X2,mult(ld(mult(X1,X2),X3),X2))) = mult(X3,X2),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t191,plain,
mult(X1,mult(X2,mult(ld(mult(X1,X2),X3),X2))) = mult(X3,X2),
inference(orient,[status(thm)],[t14]) ).
cnf(t213,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(cp,[status(thm)],[t9,t191]) ).
cnf(t2605,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(orient,[status(thm)],[t213]) ).
cnf(t2662,plain,
ld(rd(X1,X2),mult(X3,X2)) = mult(X2,mult(ld(X1,X3),X2)),
inference(cp,[status(thm)],[t2605,t8]) ).
cnf(t2694,plain,
ld(rd(X1,X2),mult(X3,X2)) = mult(X2,mult(ld(X1,X3),X2)),
inference(orient,[status(thm)],[t2662]) ).
cnf(t2695,plain,
mult(X1,mult(ld(X2,rd(X2,X1)),X1)) = X1,
inference(cp,[status(thm)],[t2694,t9]) ).
cnf(t3026,plain,
mult(X1,mult(ld(X2,rd(X2,X1)),X1)) = X1,
inference(orient,[status(thm)],[t2695]) ).
cnf(t3087,plain,
mult(ld(X1,rd(X1,X2)),X2) = ld(X2,X2),
inference(cp,[status(thm)],[t9,t3026]) ).
cnf(t3117,plain,
mult(ld(X1,rd(X1,X2)),X2) = ld(X2,X2),
inference(orient,[status(thm)],[t3087]) ).
cnf(t3189,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = mult(rd(X1,X3),mult(X3,ld(X3,X3))),
inference(cp,[status(thm)],[t233,t3117]) ).
cnf(t27077,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = mult(rd(X1,X3),X3),
inference(step,[status(thm)],[t3189,t7]) ).
cnf(t27078,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = X1,
inference(step,[status(thm)],[t27077,t8]) ).
cnf(t5069,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = X1,
inference(orient,[status(thm)],[t27078]) ).
cnf(t5080,plain,
rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
inference(cp,[status(thm)],[t5069,t8]) ).
cnf(t5164,plain,
rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t5080]) ).
cnf(t5166,plain,
mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
inference(cp,[status(thm)],[t5164,t39]) ).
cnf(t5238,plain,
mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
inference(orient,[status(thm)],[t5166]) ).
cnf(t5299,plain,
ld(X1,X2) = ld(X3,rd(X3,ld(X2,X1))),
inference(cp,[status(thm)],[t9,t5238]) ).
cnf(t5508,plain,
ld(X1,rd(X1,ld(X2,X3))) = ld(X3,X2),
inference(orient,[status(thm)],[t5299]) ).
cnf(t268,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(rd(X1,X3),mult(X3,X2)),
inference(cp,[status(thm)],[t233,t8]) ).
cnf(t593,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(rd(X1,X3),mult(X3,X2)),
inference(orient,[status(thm)],[t268]) ).
cnf(t5,axiom,
sFlat0 = ld(x1,x1),
introduced(definition) ).
cnf(t25,plain,
ld(x1,x1) = sFlat0,
inference(orient,[status(thm)],[t5]) ).
cnf(t26,plain,
x1 = mult(x1,sFlat0),
inference(cp,[status(thm)],[t7,t25]) ).
cnf(t28,plain,
mult(x1,sFlat0) = x1,
inference(orient,[status(thm)],[t26]) ).
cnf(t30,plain,
mult(x1,mult(sFlat0,mult(X1,sFlat0))) = mult(mult(x1,X1),sFlat0),
inference(cp,[status(thm)],[t13,t28]) ).
cnf(t40,plain,
mult(x1,mult(sFlat0,mult(X1,sFlat0))) = mult(mult(x1,X1),sFlat0),
inference(orient,[status(thm)],[t30]) ).
cnf(t45,plain,
mult(sFlat0,mult(X1,sFlat0)) = ld(x1,mult(mult(x1,X1),sFlat0)),
inference(cp,[status(thm)],[t9,t40]) ).
cnf(t77,plain,
ld(x1,mult(mult(x1,X1),sFlat0)) = mult(sFlat0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t45]) ).
cnf(t78,plain,
mult(sFlat0,mult(sFlat0,sFlat0)) = ld(x1,mult(x1,sFlat0)),
inference(cp,[status(thm)],[t77,t28]) ).
cnf(t26866,plain,
mult(sFlat0,mult(sFlat0,sFlat0)) = sFlat0,
inference(step,[status(thm)],[t78,t9]) ).
cnf(t82,plain,
mult(sFlat0,mult(sFlat0,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t26866]) ).
cnf(t245,plain,
mult(mult(X1,sFlat0),sFlat0) = mult(rd(X1,sFlat0),sFlat0),
inference(cp,[status(thm)],[t233,t82]) ).
cnf(t26867,plain,
mult(mult(X1,sFlat0),sFlat0) = X1,
inference(step,[status(thm)],[t245,t8]) ).
cnf(t274,plain,
mult(mult(X1,sFlat0),sFlat0) = X1,
inference(orient,[status(thm)],[t26867]) ).
cnf(t280,plain,
rd(X1,sFlat0) = mult(X1,sFlat0),
inference(cp,[status(thm)],[t274,t8]) ).
cnf(t288,plain,
mult(X1,sFlat0) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t280]) ).
cnf(t594,plain,
mult(rd(X1,sFlat0),mult(sFlat0,X2)) = rd(mult(X1,rd(X2,sFlat0)),sFlat0),
inference(cp,[status(thm)],[t593,t288]) ).
cnf(t1164,plain,
mult(rd(X1,sFlat0),mult(sFlat0,X2)) = rd(mult(X1,rd(X2,sFlat0)),sFlat0),
inference(orient,[status(thm)],[t594]) ).
cnf(t26883,plain,
ld(x1,rd(mult(x1,X1),sFlat0)) = mult(sFlat0,mult(X1,sFlat0)),
inference(step,[status(thm)],[t77,t288]) ).
cnf(t43,plain,
mult(mult(x1,rd(X1,sFlat0)),sFlat0) = mult(x1,mult(sFlat0,X1)),
inference(cp,[status(thm)],[t40,t8]) ).
cnf(t70,plain,
mult(mult(x1,rd(X1,sFlat0)),sFlat0) = mult(x1,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t43]) ).
cnf(t72,plain,
mult(x1,rd(X1,sFlat0)) = rd(mult(x1,mult(sFlat0,X1)),sFlat0),
inference(cp,[status(thm)],[t11,t70]) ).
cnf(t99,plain,
rd(mult(x1,mult(sFlat0,X1)),sFlat0) = mult(x1,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t72]) ).
cnf(t102,plain,
mult(x1,rd(ld(sFlat0,X1),sFlat0)) = rd(mult(x1,X1),sFlat0),
inference(cp,[status(thm)],[t99,t7]) ).
cnf(t124,plain,
mult(x1,rd(ld(sFlat0,X1),sFlat0)) = rd(mult(x1,X1),sFlat0),
inference(orient,[status(thm)],[t102]) ).
cnf(t127,plain,
rd(ld(sFlat0,X1),sFlat0) = ld(x1,rd(mult(x1,X1),sFlat0)),
inference(cp,[status(thm)],[t9,t124]) ).
cnf(t151,plain,
ld(x1,rd(mult(x1,X1),sFlat0)) = rd(ld(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t127]) ).
cnf(t26884,plain,
rd(ld(sFlat0,X1),sFlat0) = mult(sFlat0,mult(X1,sFlat0)),
inference(step,[status(thm)],[t26883,t151]) ).
cnf(t26885,plain,
rd(ld(sFlat0,X1),sFlat0) = mult(sFlat0,rd(X1,sFlat0)),
inference(step,[status(thm)],[t26884,t288]) ).
cnf(t315,plain,
rd(ld(sFlat0,X1),sFlat0) = mult(sFlat0,rd(X1,sFlat0)),
inference(rw,[status(thm)],[t26885]) ).
cnf(t363,plain,
mult(sFlat0,rd(X1,sFlat0)) = rd(ld(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t315]) ).
cnf(t596,plain,
mult(rd(sFlat0,sFlat0),mult(sFlat0,X1)) = mult(rd(ld(sFlat0,X1),sFlat0),sFlat0),
inference(cp,[status(thm)],[t593,t363]) ).
cnf(t26899,plain,
mult(rd(sFlat0,sFlat0),mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(step,[status(thm)],[t596,t8]) ).
cnf(t636,plain,
mult(rd(sFlat0,sFlat0),mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(orient,[status(thm)],[t26899]) ).
cnf(t641,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(rd(sFlat0,sFlat0),X1),
inference(cp,[status(thm)],[t636,t7]) ).
cnf(t660,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(rd(sFlat0,sFlat0),X1),
inference(orient,[status(thm)],[t641]) ).
cnf(t3179,plain,
X1 = ld(ld(X2,rd(X2,X1)),ld(X1,X1)),
inference(cp,[status(thm)],[t9,t3117]) ).
cnf(t3284,plain,
ld(ld(X1,rd(X1,X2)),ld(X2,X2)) = X2,
inference(orient,[status(thm)],[t3179]) ).
cnf(t3340,plain,
x1 = ld(ld(X1,rd(X1,x1)),sFlat0),
inference(cp,[status(thm)],[t3284,t25]) ).
cnf(t3345,plain,
ld(ld(X1,rd(X1,x1)),sFlat0) = x1,
inference(orient,[status(thm)],[t3340]) ).
cnf(t3350,plain,
ld(X1,rd(X1,x1)) = rd(sFlat0,x1),
inference(cp,[status(thm)],[t39,t3345]) ).
cnf(t3354,plain,
ld(X1,rd(X1,x1)) = rd(sFlat0,x1),
inference(orient,[status(thm)],[t3350]) ).
cnf(t3363,plain,
mult(rd(sFlat0,sFlat0),rd(sFlat0,x1)) = ld(sFlat0,rd(sFlat0,x1)),
inference(cp,[status(thm)],[t660,t3354]) ).
cnf(t3358,plain,
rd(X1,x1) = mult(X1,rd(sFlat0,x1)),
inference(cp,[status(thm)],[t7,t3354]) ).
cnf(t3386,plain,
mult(X1,rd(sFlat0,x1)) = rd(X1,x1),
inference(orient,[status(thm)],[t3358]) ).
cnf(t26940,plain,
rd(rd(sFlat0,sFlat0),x1) = ld(sFlat0,rd(sFlat0,x1)),
inference(step,[status(thm)],[t3363,t3386]) ).
cnf(t26941,plain,
rd(rd(sFlat0,sFlat0),x1) = rd(sFlat0,x1),
inference(step,[status(thm)],[t26940,t3354]) ).
cnf(t3431,plain,
rd(rd(sFlat0,sFlat0),x1) = rd(sFlat0,x1),
inference(orient,[status(thm)],[t26941]) ).
cnf(t3435,plain,
rd(sFlat0,sFlat0) = mult(rd(sFlat0,x1),x1),
inference(cp,[status(thm)],[t8,t3431]) ).
cnf(t26942,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t3435,t8]) ).
cnf(t3440,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t26942]) ).
cnf(t3460,plain,
rd(mult(sFlat0,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,mult(sFlat0,X1)),
inference(cp,[status(thm)],[t1164,t3440]) ).
cnf(t26974,plain,
rd(rd(ld(sFlat0,X1),sFlat0),sFlat0) = mult(sFlat0,mult(sFlat0,X1)),
inference(step,[status(thm)],[t3460,t363]) ).
cnf(t292,plain,
rd(rd(X1,sFlat0),sFlat0) = X1,
inference(cp,[status(thm)],[t288,t8]) ).
cnf(t318,plain,
rd(rd(X1,sFlat0),sFlat0) = X1,
inference(orient,[status(thm)],[t292]) ).
cnf(t26975,plain,
ld(sFlat0,X1) = mult(sFlat0,mult(sFlat0,X1)),
inference(step,[status(thm)],[t26974,t318]) ).
cnf(t3507,plain,
mult(sFlat0,mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(orient,[status(thm)],[t26975]) ).
cnf(t5293,plain,
ld(sFlat0,ld(X1,X2)) = mult(sFlat0,rd(sFlat0,ld(X2,X1))),
inference(cp,[status(thm)],[t3507,t5238]) ).
cnf(t5758,plain,
mult(sFlat0,rd(sFlat0,ld(X1,X2))) = ld(sFlat0,ld(X2,X1)),
inference(orient,[status(thm)],[t5293]) ).
cnf(t5760,plain,
ld(sFlat0,ld(mult(X1,X2),X1)) = mult(sFlat0,rd(sFlat0,X2)),
inference(cp,[status(thm)],[t5758,t9]) ).
cnf(t6154,plain,
ld(sFlat0,ld(mult(X1,X2),X1)) = mult(sFlat0,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t5760]) ).
cnf(t6219,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(X3,rd(X3,mult(sFlat0,rd(sFlat0,X2)))),
inference(cp,[status(thm)],[t5508,t6154]) ).
cnf(t26947,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(sFlat0,X1),
inference(step,[status(thm)],[t660,t3440]) ).
cnf(t3445,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t26947]) ).
cnf(t5542,plain,
ld(ld(sFlat0,X1),sFlat0) = ld(X2,rd(X2,mult(sFlat0,X1))),
inference(cp,[status(thm)],[t5508,t3445]) ).
cnf(t6053,plain,
ld(X1,rd(X1,mult(sFlat0,X2))) = ld(ld(sFlat0,X2),sFlat0),
inference(orient,[status(thm)],[t5542]) ).
cnf(t27182,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0),
inference(step,[status(thm)],[t6219,t6053]) ).
cnf(t9980,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0),
inference(orient,[status(thm)],[t27182]) ).
cnf(t10058,plain,
ld(mult(X1,X2),X1) = rd(sFlat0,ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0)),
inference(cp,[status(thm)],[t39,t9980]) ).
cnf(t644,plain,
rd(sFlat0,sFlat0) = rd(ld(sFlat0,X1),mult(sFlat0,X1)),
inference(cp,[status(thm)],[t11,t636]) ).
cnf(t741,plain,
rd(ld(sFlat0,X1),mult(sFlat0,X1)) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t644]) ).
cnf(t26949,plain,
rd(ld(sFlat0,X1),mult(sFlat0,X1)) = sFlat0,
inference(step,[status(thm)],[t741,t3440]) ).
cnf(t3447,plain,
rd(ld(sFlat0,X1),mult(sFlat0,X1)) = sFlat0,
inference(orient,[status(thm)],[t26949]) ).
cnf(t5198,plain,
mult(X1,mult(sFlat0,X2)) = rd(X1,ld(ld(sFlat0,X2),sFlat0)),
inference(cp,[status(thm)],[t5164,t3447]) ).
cnf(t5634,plain,
rd(X1,ld(ld(sFlat0,X2),sFlat0)) = mult(X1,mult(sFlat0,X2)),
inference(orient,[status(thm)],[t5198]) ).
cnf(t27183,plain,
ld(mult(X1,X2),X1) = mult(sFlat0,mult(sFlat0,rd(sFlat0,X2))),
inference(step,[status(thm)],[t10058,t5634]) ).
cnf(t27184,plain,
ld(mult(X1,X2),X1) = ld(sFlat0,rd(sFlat0,X2)),
inference(step,[status(thm)],[t27183,t3507]) ).
cnf(t10063,plain,
ld(mult(X1,X2),X1) = ld(sFlat0,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t27184]) ).
cnf(t6,axiom,
sFlat1 = mult(ld(x1,x1),x0),
introduced(definition) ).
cnf(t21,plain,
mult(ld(x1,x1),x0) = sFlat1,
inference(orient,[status(thm)],[t6]) ).
cnf(t26865,plain,
mult(sFlat0,x0) = sFlat1,
inference(step,[status(thm)],[t21,t25]) ).
cnf(t27,plain,
mult(sFlat0,x0) = sFlat1,
inference(rw,[status(thm)],[t26865]) ).
cnf(t31,plain,
mult(sFlat0,x0) = sFlat1,
inference(orient,[status(thm)],[t27]) ).
cnf(t34,plain,
mult(sFlat0,mult(x0,mult(X1,x0))) = mult(mult(sFlat1,X1),x0),
inference(cp,[status(thm)],[t13,t31]) ).
cnf(t55,plain,
mult(sFlat0,mult(x0,mult(X1,x0))) = mult(mult(sFlat1,X1),x0),
inference(orient,[status(thm)],[t34]) ).
cnf(t58,plain,
mult(mult(sFlat1,rd(X1,x0)),x0) = mult(sFlat0,mult(x0,X1)),
inference(cp,[status(thm)],[t55,t8]) ).
cnf(t89,plain,
mult(mult(sFlat1,rd(X1,x0)),x0) = mult(sFlat0,mult(x0,X1)),
inference(orient,[status(thm)],[t58]) ).
cnf(t91,plain,
mult(sFlat1,rd(X1,x0)) = rd(mult(sFlat0,mult(x0,X1)),x0),
inference(cp,[status(thm)],[t11,t89]) ).
cnf(t116,plain,
rd(mult(sFlat0,mult(x0,X1)),x0) = mult(sFlat1,rd(X1,x0)),
inference(orient,[status(thm)],[t91]) ).
cnf(t117,plain,
mult(sFlat1,rd(ld(x0,X1),x0)) = rd(mult(sFlat0,X1),x0),
inference(cp,[status(thm)],[t116,t7]) ).
cnf(t133,plain,
mult(sFlat1,rd(ld(x0,X1),x0)) = rd(mult(sFlat0,X1),x0),
inference(orient,[status(thm)],[t117]) ).
cnf(t10109,plain,
ld(sFlat0,rd(sFlat0,rd(ld(x0,X1),x0))) = ld(rd(mult(sFlat0,X1),x0),sFlat1),
inference(cp,[status(thm)],[t10063,t133]) ).
cnf(t2792,plain,
mult(x0,mult(ld(X1,sFlat0),x0)) = ld(rd(X1,x0),sFlat1),
inference(cp,[status(thm)],[t2694,t31]) ).
cnf(t2809,plain,
mult(x0,mult(ld(X1,sFlat0),x0)) = ld(rd(X1,x0),sFlat1),
inference(orient,[status(thm)],[t2792]) ).
cnf(t2810,plain,
ld(rd(rd(sFlat0,X1),x0),sFlat1) = mult(x0,mult(X1,x0)),
inference(cp,[status(thm)],[t2809,t38]) ).
cnf(t2829,plain,
ld(rd(rd(sFlat0,X1),x0),sFlat1) = mult(x0,mult(X1,x0)),
inference(orient,[status(thm)],[t2810]) ).
cnf(t2832,plain,
rd(rd(sFlat0,X1),x0) = rd(sFlat1,mult(x0,mult(X1,x0))),
inference(cp,[status(thm)],[t39,t2829]) ).
cnf(t2870,plain,
rd(sFlat1,mult(x0,mult(X1,x0))) = rd(rd(sFlat0,X1),x0),
inference(orient,[status(thm)],[t2832]) ).
cnf(t2881,plain,
rd(rd(sFlat0,rd(X1,x0)),x0) = rd(sFlat1,mult(x0,X1)),
inference(cp,[status(thm)],[t2870,t8]) ).
cnf(t2913,plain,
rd(rd(sFlat0,rd(X1,x0)),x0) = rd(sFlat1,mult(x0,X1)),
inference(orient,[status(thm)],[t2881]) ).
cnf(t2929,plain,
rd(sFlat0,rd(X1,x0)) = mult(rd(sFlat1,mult(x0,X1)),x0),
inference(cp,[status(thm)],[t8,t2913]) ).
cnf(t2950,plain,
mult(rd(sFlat1,mult(x0,X1)),x0) = rd(sFlat0,rd(X1,x0)),
inference(orient,[status(thm)],[t2929]) ).
cnf(t2956,plain,
rd(sFlat0,rd(ld(x0,X1),x0)) = mult(rd(sFlat1,X1),x0),
inference(cp,[status(thm)],[t2950,t7]) ).
cnf(t3001,plain,
rd(sFlat0,rd(ld(x0,X1),x0)) = mult(rd(sFlat1,X1),x0),
inference(orient,[status(thm)],[t2956]) ).
cnf(t27214,plain,
ld(sFlat0,mult(rd(sFlat1,X1),x0)) = ld(rd(mult(sFlat0,X1),x0),sFlat1),
inference(step,[status(thm)],[t10109,t3001]) ).
cnf(t10986,plain,
ld(rd(mult(sFlat0,X1),x0),sFlat1) = ld(sFlat0,mult(rd(sFlat1,X1),x0)),
inference(orient,[status(thm)],[t27214]) ).
cnf(t2803,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(cp,[status(thm)],[t2694,t8]) ).
cnf(t13287,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(orient,[status(thm)],[t2803]) ).
cnf(t13467,plain,
mult(ld(X1,rd(X2,X3)),X3) = ld(X3,ld(rd(X1,X3),X2)),
inference(cp,[status(thm)],[t9,t13287]) ).
cnf(t13543,plain,
ld(X1,ld(rd(X2,X1),X3)) = mult(ld(X2,rd(X3,X1)),X1),
inference(orient,[status(thm)],[t13467]) ).
cnf(t15,plain,
mult(X1,mult(ld(X1,X2),mult(X3,ld(X1,X2)))) = mult(mult(X2,X3),ld(X1,X2)),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t677,plain,
mult(X1,mult(ld(X1,X2),mult(X3,ld(X1,X2)))) = mult(mult(X2,X3),ld(X1,X2)),
inference(orient,[status(thm)],[t15]) ).
cnf(t698,plain,
mult(mult(X1,X2),ld(X2,X1)) = mult(X2,mult(ld(X2,X1),X1)),
inference(cp,[status(thm)],[t677,t7]) ).
cnf(t1240,plain,
mult(mult(X1,X2),ld(X2,X1)) = mult(X2,mult(ld(X2,X1),X1)),
inference(orient,[status(thm)],[t698]) ).
cnf(t27084,plain,
rd(mult(X1,X2),ld(X1,X2)) = mult(X2,mult(ld(X2,X1),X1)),
inference(step,[status(thm)],[t1240,t5238]) ).
cnf(t5326,plain,
rd(mult(X1,X2),ld(X1,X2)) = mult(X2,mult(ld(X2,X1),X1)),
inference(rw,[status(thm)],[t27084]) ).
cnf(t9544,plain,
mult(X1,mult(ld(X1,X2),X2)) = rd(mult(X2,X1),ld(X2,X1)),
inference(orient,[status(thm)],[t5326]) ).
cnf(t9657,plain,
mult(ld(X1,X2),X2) = ld(X1,rd(mult(X2,X1),ld(X2,X1))),
inference(cp,[status(thm)],[t9,t9544]) ).
cnf(t15903,plain,
ld(X1,rd(mult(X2,X1),ld(X2,X1))) = mult(ld(X1,X2),X2),
inference(orient,[status(thm)],[t9657]) ).
cnf(t135,plain,
rd(ld(x0,X1),x0) = ld(sFlat1,rd(mult(sFlat0,X1),x0)),
inference(cp,[status(thm)],[t9,t133]) ).
cnf(t161,plain,
ld(sFlat1,rd(mult(sFlat0,X1),x0)) = rd(ld(x0,X1),x0),
inference(orient,[status(thm)],[t135]) ).
cnf(t163,plain,
rd(ld(x0,mult(sFlat0,sFlat0)),x0) = ld(sFlat1,rd(sFlat0,x0)),
inference(cp,[status(thm)],[t161,t82]) ).
cnf(t176,plain,
rd(ld(x0,mult(sFlat0,sFlat0)),x0) = ld(sFlat1,rd(sFlat0,x0)),
inference(orient,[status(thm)],[t163]) ).
cnf(t26877,plain,
rd(ld(x0,rd(sFlat0,sFlat0)),x0) = ld(sFlat1,rd(sFlat0,x0)),
inference(step,[status(thm)],[t176,t288]) ).
cnf(t311,plain,
rd(ld(x0,rd(sFlat0,sFlat0)),x0) = ld(sFlat1,rd(sFlat0,x0)),
inference(rw,[status(thm)],[t26877]) ).
cnf(t463,plain,
rd(ld(x0,rd(sFlat0,sFlat0)),x0) = ld(sFlat1,rd(sFlat0,x0)),
inference(orient,[status(thm)],[t311]) ).
cnf(t26967,plain,
rd(ld(x0,sFlat0),x0) = ld(sFlat1,rd(sFlat0,x0)),
inference(step,[status(thm)],[t463,t3440]) ).
cnf(t3478,plain,
rd(ld(x0,sFlat0),x0) = ld(sFlat1,rd(sFlat0,x0)),
inference(rw,[status(thm)],[t26967]) ).
cnf(t3721,plain,
ld(sFlat1,rd(sFlat0,x0)) = rd(ld(x0,sFlat0),x0),
inference(orient,[status(thm)],[t3478]) ).
cnf(t16083,plain,
mult(ld(rd(sFlat0,x0),sFlat1),sFlat1) = ld(rd(sFlat0,x0),rd(mult(sFlat1,rd(sFlat0,x0)),rd(ld(x0,sFlat0),x0))),
inference(cp,[status(thm)],[t15903,t3721]) ).
cnf(t3461,plain,
mult(x0,mult(sFlat0,x0)) = ld(rd(sFlat0,x0),sFlat1),
inference(cp,[status(thm)],[t2829,t3440]) ).
cnf(t26977,plain,
mult(x0,sFlat1) = ld(rd(sFlat0,x0),sFlat1),
inference(step,[status(thm)],[t3461,t31]) ).
cnf(t3530,plain,
ld(rd(sFlat0,x0),sFlat1) = mult(x0,sFlat1),
inference(orient,[status(thm)],[t26977]) ).
cnf(t27683,plain,
mult(mult(x0,sFlat1),sFlat1) = ld(rd(sFlat0,x0),rd(mult(sFlat1,rd(sFlat0,x0)),rd(ld(x0,sFlat0),x0))),
inference(step,[status(thm)],[t16083,t3530]) ).
cnf(t258,plain,
mult(mult(X1,sFlat0),x0) = mult(rd(X1,x0),mult(x0,sFlat1)),
inference(cp,[status(thm)],[t233,t31]) ).
cnf(t26894,plain,
mult(rd(X1,sFlat0),x0) = mult(rd(X1,x0),mult(x0,sFlat1)),
inference(step,[status(thm)],[t258,t288]) ).
cnf(t439,plain,
mult(rd(X1,x0),mult(x0,sFlat1)) = mult(rd(X1,sFlat0),x0),
inference(orient,[status(thm)],[t26894]) ).
cnf(t444,plain,
rd(X1,x0) = rd(mult(rd(X1,sFlat0),x0),mult(x0,sFlat1)),
inference(cp,[status(thm)],[t11,t439]) ).
cnf(t1787,plain,
rd(mult(rd(X1,sFlat0),x0),mult(x0,sFlat1)) = rd(X1,x0),
inference(orient,[status(thm)],[t444]) ).
cnf(t1799,plain,
rd(rd(X1,sFlat0),x0) = rd(mult(X1,x0),mult(x0,sFlat1)),
inference(cp,[status(thm)],[t1787,t318]) ).
cnf(t1826,plain,
rd(mult(X1,x0),mult(x0,sFlat1)) = rd(rd(X1,sFlat0),x0),
inference(orient,[status(thm)],[t1799]) ).
cnf(t1829,plain,
rd(rd(sFlat0,sFlat0),x0) = rd(sFlat1,mult(x0,sFlat1)),
inference(cp,[status(thm)],[t1826,t31]) ).
cnf(t1837,plain,
rd(rd(sFlat0,sFlat0),x0) = rd(sFlat1,mult(x0,sFlat1)),
inference(orient,[status(thm)],[t1829]) ).
cnf(t26959,plain,
rd(sFlat0,x0) = rd(sFlat1,mult(x0,sFlat1)),
inference(step,[status(thm)],[t1837,t3440]) ).
cnf(t3471,plain,
rd(sFlat0,x0) = rd(sFlat1,mult(x0,sFlat1)),
inference(rw,[status(thm)],[t26959]) ).
cnf(t3535,plain,
rd(sFlat1,mult(x0,sFlat1)) = rd(sFlat0,x0),
inference(orient,[status(thm)],[t3471]) ).
cnf(t5219,plain,
mult(X1,mult(x0,sFlat1)) = rd(X1,ld(sFlat1,rd(sFlat0,x0))),
inference(cp,[status(thm)],[t5164,t3535]) ).
cnf(t27098,plain,
mult(X1,mult(x0,sFlat1)) = rd(X1,rd(ld(x0,sFlat0),x0)),
inference(step,[status(thm)],[t5219,t3721]) ).
cnf(t5670,plain,
rd(X1,rd(ld(x0,sFlat0),x0)) = mult(X1,mult(x0,sFlat1)),
inference(orient,[status(thm)],[t27098]) ).
cnf(t27684,plain,
mult(mult(x0,sFlat1),sFlat1) = ld(rd(sFlat0,x0),mult(mult(sFlat1,rd(sFlat0,x0)),mult(x0,sFlat1))),
inference(step,[status(thm)],[t27683,t5670]) ).
cnf(t300,plain,
mult(sFlat1,rd(sFlat0,x0)) = rd(mult(sFlat0,rd(x0,sFlat0)),x0),
inference(cp,[status(thm)],[t116,t288]) ).
cnf(t26895,plain,
mult(sFlat1,rd(sFlat0,x0)) = rd(rd(ld(sFlat0,x0),sFlat0),x0),
inference(step,[status(thm)],[t300,t363]) ).
cnf(t451,plain,
rd(rd(ld(sFlat0,x0),sFlat0),x0) = mult(sFlat1,rd(sFlat0,x0)),
inference(orient,[status(thm)],[t26895]) ).
cnf(t638,plain,
ld(sFlat0,x0) = mult(rd(sFlat0,sFlat0),sFlat1),
inference(cp,[status(thm)],[t636,t31]) ).
cnf(t650,plain,
mult(rd(sFlat0,sFlat0),sFlat1) = ld(sFlat0,x0),
inference(orient,[status(thm)],[t638]) ).
cnf(t26962,plain,
mult(sFlat0,sFlat1) = ld(sFlat0,x0),
inference(step,[status(thm)],[t650,t3440]) ).
cnf(t3474,plain,
mult(sFlat0,sFlat1) = ld(sFlat0,x0),
inference(rw,[status(thm)],[t26962]) ).
cnf(t3479,plain,
ld(sFlat0,x0) = mult(sFlat0,sFlat1),
inference(orient,[status(thm)],[t3474]) ).
cnf(t26973,plain,
rd(rd(mult(sFlat0,sFlat1),sFlat0),x0) = mult(sFlat1,rd(sFlat0,x0)),
inference(step,[status(thm)],[t451,t3479]) ).
cnf(t3491,plain,
rd(rd(mult(sFlat0,sFlat1),sFlat0),x0) = mult(sFlat1,rd(sFlat0,x0)),
inference(rw,[status(thm)],[t26973]) ).
cnf(t4099,plain,
rd(rd(mult(sFlat0,sFlat1),sFlat0),x0) = mult(sFlat1,rd(sFlat0,x0)),
inference(orient,[status(thm)],[t3491]) ).
cnf(t4102,plain,
mult(rd(rd(mult(sFlat0,sFlat1),sFlat0),sFlat0),x0) = mult(mult(sFlat1,rd(sFlat0,x0)),mult(x0,sFlat1)),
inference(cp,[status(thm)],[t439,t4099]) ).
cnf(t27310,plain,
mult(mult(sFlat0,sFlat1),x0) = mult(mult(sFlat1,rd(sFlat0,x0)),mult(x0,sFlat1)),
inference(step,[status(thm)],[t4102,t318]) ).
cnf(t1244,plain,
mult(sFlat0,mult(ld(sFlat0,X1),X1)) = mult(rd(X1,sFlat0),ld(sFlat0,X1)),
inference(cp,[status(thm)],[t1240,t288]) ).
cnf(t1549,plain,
mult(rd(X1,sFlat0),ld(sFlat0,X1)) = mult(sFlat0,mult(ld(sFlat0,X1),X1)),
inference(orient,[status(thm)],[t1244]) ).
cnf(t3483,plain,
mult(sFlat0,mult(ld(sFlat0,x0),x0)) = mult(rd(x0,sFlat0),mult(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t1549,t3479]) ).
cnf(t27052,plain,
mult(sFlat0,mult(mult(sFlat0,sFlat1),x0)) = mult(rd(x0,sFlat0),mult(sFlat0,sFlat1)),
inference(step,[status(thm)],[t3483,t3479]) ).
cnf(t27053,plain,
mult(sFlat0,mult(mult(sFlat0,sFlat1),x0)) = rd(mult(x0,rd(sFlat1,sFlat0)),sFlat0),
inference(step,[status(thm)],[t27052,t1164]) ).
cnf(t295,plain,
mult(X1,mult(X2,mult(sFlat0,X2))) = mult(rd(mult(X1,X2),sFlat0),X2),
inference(cp,[status(thm)],[t13,t288]) ).
cnf(t1053,plain,
mult(rd(mult(X1,X2),sFlat0),X2) = mult(X1,mult(X2,mult(sFlat0,X2))),
inference(orient,[status(thm)],[t295]) ).
cnf(t1084,plain,
mult(sFlat0,mult(rd(X1,sFlat0),mult(sFlat0,rd(X1,sFlat0)))) = mult(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),rd(X1,sFlat0)),
inference(cp,[status(thm)],[t1053,t363]) ).
cnf(t26923,plain,
mult(sFlat0,rd(mult(X1,rd(rd(X1,sFlat0),sFlat0)),sFlat0)) = mult(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),rd(X1,sFlat0)),
inference(step,[status(thm)],[t1084,t1164]) ).
cnf(t26924,plain,
rd(ld(sFlat0,mult(X1,rd(rd(X1,sFlat0),sFlat0))),sFlat0) = mult(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),rd(X1,sFlat0)),
inference(step,[status(thm)],[t26923,t363]) ).
cnf(t26925,plain,
rd(ld(sFlat0,mult(X1,X1)),sFlat0) = mult(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),rd(X1,sFlat0)),
inference(step,[status(thm)],[t26924,t318]) ).
cnf(t26926,plain,
rd(ld(sFlat0,mult(X1,X1)),sFlat0) = mult(ld(sFlat0,X1),rd(X1,sFlat0)),
inference(step,[status(thm)],[t26925,t318]) ).
cnf(t1377,plain,
mult(ld(sFlat0,X1),rd(X1,sFlat0)) = rd(ld(sFlat0,mult(X1,X1)),sFlat0),
inference(orient,[status(thm)],[t26926]) ).
cnf(t33,plain,
x0 = ld(sFlat0,sFlat1),
inference(cp,[status(thm)],[t9,t31]) ).
cnf(t37,plain,
ld(sFlat0,sFlat1) = x0,
inference(orient,[status(thm)],[t33]) ).
cnf(t1387,plain,
rd(ld(sFlat0,mult(sFlat1,sFlat1)),sFlat0) = mult(x0,rd(sFlat1,sFlat0)),
inference(cp,[status(thm)],[t1377,t37]) ).
cnf(t1475,plain,
rd(ld(sFlat0,mult(sFlat1,sFlat1)),sFlat0) = mult(x0,rd(sFlat1,sFlat0)),
inference(orient,[status(thm)],[t1387]) ).
cnf(t1483,plain,
ld(sFlat0,mult(sFlat1,sFlat1)) = rd(mult(x0,rd(sFlat1,sFlat0)),sFlat0),
inference(cp,[status(thm)],[t318,t1475]) ).
cnf(t1518,plain,
rd(mult(x0,rd(sFlat1,sFlat0)),sFlat0) = ld(sFlat0,mult(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t1483]) ).
cnf(t27054,plain,
mult(sFlat0,mult(mult(sFlat0,sFlat1),x0)) = ld(sFlat0,mult(sFlat1,sFlat1)),
inference(step,[status(thm)],[t27053,t1518]) ).
cnf(t4026,plain,
mult(sFlat0,mult(mult(sFlat0,sFlat1),x0)) = ld(sFlat0,mult(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t27054]) ).
cnf(t4034,plain,
mult(mult(sFlat0,sFlat1),x0) = ld(sFlat0,ld(sFlat0,mult(sFlat1,sFlat1))),
inference(cp,[status(thm)],[t9,t4026]) ).
cnf(t27055,plain,
mult(mult(sFlat0,sFlat1),x0) = mult(sFlat0,mult(sFlat1,sFlat1)),
inference(step,[status(thm)],[t4034,t3445]) ).
cnf(t4046,plain,
mult(mult(sFlat0,sFlat1),x0) = mult(sFlat0,mult(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t27055]) ).
cnf(t27311,plain,
mult(sFlat0,mult(sFlat1,sFlat1)) = mult(mult(sFlat1,rd(sFlat0,x0)),mult(x0,sFlat1)),
inference(step,[status(thm)],[t27310,t4046]) ).
cnf(t14138,plain,
mult(mult(sFlat1,rd(sFlat0,x0)),mult(x0,sFlat1)) = mult(sFlat0,mult(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t27311]) ).
cnf(t27685,plain,
mult(mult(x0,sFlat1),sFlat1) = ld(rd(sFlat0,x0),mult(sFlat0,mult(sFlat1,sFlat1))),
inference(step,[status(thm)],[t27684,t14138]) ).
cnf(t26250,plain,
ld(rd(sFlat0,x0),mult(sFlat0,mult(sFlat1,sFlat1))) = mult(mult(x0,sFlat1),sFlat1),
inference(orient,[status(thm)],[t27685]) ).
cnf(t26256,plain,
mult(ld(sFlat0,rd(mult(sFlat0,mult(sFlat1,sFlat1)),x0)),x0) = ld(x0,mult(mult(x0,sFlat1),sFlat1)),
inference(cp,[status(thm)],[t13543,t26250]) ).
cnf(t4052,plain,
mult(sFlat0,sFlat1) = rd(mult(sFlat0,mult(sFlat1,sFlat1)),x0),
inference(cp,[status(thm)],[t11,t4046]) ).
cnf(t4069,plain,
rd(mult(sFlat0,mult(sFlat1,sFlat1)),x0) = mult(sFlat0,sFlat1),
inference(orient,[status(thm)],[t4052]) ).
cnf(t27686,plain,
mult(ld(sFlat0,mult(sFlat0,sFlat1)),x0) = ld(x0,mult(mult(x0,sFlat1),sFlat1)),
inference(step,[status(thm)],[t26256,t4069]) ).
cnf(t27687,plain,
mult(sFlat1,x0) = ld(x0,mult(mult(x0,sFlat1),sFlat1)),
inference(step,[status(thm)],[t27686,t9]) ).
cnf(t291,plain,
rd(mult(mult(X1,sFlat0),X2),sFlat0) = mult(X1,mult(sFlat0,mult(X2,sFlat0))),
inference(cp,[status(thm)],[t288,t13]) ).
cnf(t26912,plain,
rd(mult(rd(X1,sFlat0),X2),sFlat0) = mult(X1,mult(sFlat0,mult(X2,sFlat0))),
inference(step,[status(thm)],[t291,t288]) ).
cnf(t26913,plain,
rd(mult(rd(X1,sFlat0),X2),sFlat0) = mult(X1,mult(sFlat0,rd(X2,sFlat0))),
inference(step,[status(thm)],[t26912,t288]) ).
cnf(t26914,plain,
rd(mult(rd(X1,sFlat0),X2),sFlat0) = mult(X1,rd(ld(sFlat0,X2),sFlat0)),
inference(step,[status(thm)],[t26913,t363]) ).
cnf(t960,plain,
mult(X1,rd(ld(sFlat0,X2),sFlat0)) = rd(mult(rd(X1,sFlat0),X2),sFlat0),
inference(orient,[status(thm)],[t26914]) ).
cnf(t971,plain,
rd(mult(rd(X1,sFlat0),sFlat1),sFlat0) = mult(X1,rd(x0,sFlat0)),
inference(cp,[status(thm)],[t960,t37]) ).
cnf(t988,plain,
rd(mult(rd(X1,sFlat0),sFlat1),sFlat0) = mult(X1,rd(x0,sFlat0)),
inference(orient,[status(thm)],[t971]) ).
cnf(t1006,plain,
mult(rd(X1,sFlat0),sFlat1) = rd(mult(X1,rd(x0,sFlat0)),sFlat0),
inference(cp,[status(thm)],[t318,t988]) ).
cnf(t1035,plain,
rd(mult(X1,rd(x0,sFlat0)),sFlat0) = mult(rd(X1,sFlat0),sFlat1),
inference(orient,[status(thm)],[t1006]) ).
cnf(t625,plain,
mult(X1,rd(X2,X3)) = rd(mult(rd(X1,X3),mult(X3,X2)),X3),
inference(cp,[status(thm)],[t11,t593]) ).
cnf(t12493,plain,
rd(mult(rd(X1,X2),mult(X2,X3)),X2) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t625]) ).
cnf(t12673,plain,
mult(X1,rd(X2,ld(X3,rd(X3,X2)))) = rd(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),ld(X3,rd(X3,X2))),
inference(cp,[status(thm)],[t12493,t3117]) ).
cnf(t27405,plain,
mult(X1,mult(X2,X2)) = rd(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),ld(X3,rd(X3,X2))),
inference(step,[status(thm)],[t12673,t5164]) ).
cnf(t27406,plain,
mult(X1,mult(X2,X2)) = mult(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t27405,t5164]) ).
cnf(t27407,plain,
mult(X1,mult(X2,X2)) = mult(rd(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t27406,t5238]) ).
cnf(t27408,plain,
mult(X1,mult(X2,X2)) = mult(rd(mult(X1,X2),ld(X2,X2)),X2),
inference(step,[status(thm)],[t27407,t5164]) ).
cnf(t17649,plain,
mult(rd(mult(X1,X2),ld(X2,X2)),X2) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t27408]) ).
cnf(t17769,plain,
mult(rd(X1,X2),mult(X2,X2)) = mult(rd(X1,ld(X2,X2)),X2),
inference(cp,[status(thm)],[t17649,t8]) ).
cnf(t17830,plain,
mult(rd(X1,ld(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t17769]) ).
cnf(t17861,plain,
rd(X1,ld(X2,X2)) = rd(mult(rd(X1,X2),mult(X2,X2)),X2),
inference(cp,[status(thm)],[t11,t17830]) ).
cnf(t27409,plain,
rd(X1,ld(X2,X2)) = mult(X1,rd(X2,X2)),
inference(step,[status(thm)],[t17861,t12493]) ).
cnf(t17910,plain,
mult(X1,rd(X2,X2)) = rd(X1,ld(X2,X2)),
inference(orient,[status(thm)],[t27409]) ).
cnf(t17942,plain,
rd(X1,X1) = ld(X2,rd(X2,ld(X1,X1))),
inference(cp,[status(thm)],[t9,t17910]) ).
cnf(t27410,plain,
rd(X1,X1) = ld(X1,X1),
inference(step,[status(thm)],[t17942,t5508]) ).
cnf(t17993,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t27410]) ).
cnf(t18013,plain,
rd(mult(X1,X1),ld(X1,X1)) = mult(X1,mult(rd(X1,X1),X1)),
inference(cp,[status(thm)],[t9544,t17993]) ).
cnf(t27444,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,mult(rd(X1,X1),X1)),
inference(step,[status(thm)],[t18013,t17993]) ).
cnf(t27445,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
inference(step,[status(thm)],[t27444,t8]) ).
cnf(t18102,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t27445]) ).
cnf(t18135,plain,
mult(X1,X1) = mult(mult(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t8,t18102]) ).
cnf(t17,plain,
mult(mult(X1,X2),X3) = rd(mult(X1,mult(X2,mult(X3,X2))),X2),
inference(cp,[status(thm)],[t11,t13]) ).
cnf(t1413,plain,
rd(mult(X1,mult(X2,mult(X3,X2))),X2) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t17]) ).
cnf(t1461,plain,
mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
inference(cp,[status(thm)],[t1413,t8]) ).
cnf(t1615,plain,
mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
inference(orient,[status(thm)],[t1461]) ).
cnf(t27451,plain,
mult(X1,X1) = rd(mult(X1,mult(X1,X1)),X1),
inference(step,[status(thm)],[t18135,t1615]) ).
cnf(t18404,plain,
rd(mult(X1,mult(X1,X1)),X1) = mult(X1,X1),
inference(orient,[status(thm)],[t27451]) ).
cnf(t18434,plain,
mult(X1,mult(X1,X1)) = mult(mult(X1,X1),X1),
inference(cp,[status(thm)],[t8,t18404]) ).
cnf(t18501,plain,
mult(mult(X1,X1),X1) = mult(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t18434]) ).
cnf(t18562,plain,
mult(rd(mult(rd(x0,sFlat0),rd(x0,sFlat0)),sFlat0),sFlat1) = rd(mult(rd(x0,sFlat0),mult(rd(x0,sFlat0),rd(x0,sFlat0))),sFlat0),
inference(cp,[status(thm)],[t1035,t18501]) ).
cnf(t27463,plain,
mult(mult(rd(rd(x0,sFlat0),sFlat0),sFlat1),sFlat1) = rd(mult(rd(x0,sFlat0),mult(rd(x0,sFlat0),rd(x0,sFlat0))),sFlat0),
inference(step,[status(thm)],[t18562,t1035]) ).
cnf(t27464,plain,
mult(mult(x0,sFlat1),sFlat1) = rd(mult(rd(x0,sFlat0),mult(rd(x0,sFlat0),rd(x0,sFlat0))),sFlat0),
inference(step,[status(thm)],[t27463,t318]) ).
cnf(t994,plain,
mult(rd(X1,sFlat0),rd(x0,sFlat0)) = rd(mult(X1,sFlat1),sFlat0),
inference(cp,[status(thm)],[t988,t318]) ).
cnf(t1017,plain,
mult(rd(X1,sFlat0),rd(x0,sFlat0)) = rd(mult(X1,sFlat1),sFlat0),
inference(orient,[status(thm)],[t994]) ).
cnf(t27465,plain,
mult(mult(x0,sFlat1),sFlat1) = rd(mult(rd(x0,sFlat0),rd(mult(x0,sFlat1),sFlat0)),sFlat0),
inference(step,[status(thm)],[t27464,t1017]) ).
cnf(t1619,plain,
rd(mult(X1,mult(sFlat0,X2)),sFlat0) = mult(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(cp,[status(thm)],[t1615,t288]) ).
cnf(t1742,plain,
mult(rd(X1,sFlat0),rd(X2,sFlat0)) = rd(mult(X1,mult(sFlat0,X2)),sFlat0),
inference(orient,[status(thm)],[t1619]) ).
cnf(t27466,plain,
mult(mult(x0,sFlat1),sFlat1) = rd(rd(mult(x0,mult(sFlat0,mult(x0,sFlat1))),sFlat0),sFlat0),
inference(step,[status(thm)],[t27465,t1742]) ).
cnf(t27467,plain,
mult(mult(x0,sFlat1),sFlat1) = mult(x0,mult(sFlat0,mult(x0,sFlat1))),
inference(step,[status(thm)],[t27466,t318]) ).
cnf(t18867,plain,
mult(x0,mult(sFlat0,mult(x0,sFlat1))) = mult(mult(x0,sFlat1),sFlat1),
inference(orient,[status(thm)],[t27467]) ).
cnf(t18873,plain,
mult(sFlat0,mult(x0,sFlat1)) = ld(x0,mult(mult(x0,sFlat1),sFlat1)),
inference(cp,[status(thm)],[t9,t18867]) ).
cnf(t18889,plain,
ld(x0,mult(mult(x0,sFlat1),sFlat1)) = mult(sFlat0,mult(x0,sFlat1)),
inference(orient,[status(thm)],[t18873]) ).
cnf(t27688,plain,
mult(sFlat1,x0) = mult(sFlat0,mult(x0,sFlat1)),
inference(step,[status(thm)],[t27687,t18889]) ).
cnf(t26263,plain,
mult(sFlat0,mult(x0,sFlat1)) = mult(sFlat1,x0),
inference(orient,[status(thm)],[t27688]) ).
cnf(t26296,plain,
ld(sFlat0,mult(rd(sFlat1,mult(x0,sFlat1)),x0)) = ld(rd(mult(sFlat1,x0),x0),sFlat1),
inference(cp,[status(thm)],[t10986,t26263]) ).
cnf(t1841,plain,
rd(sFlat0,sFlat0) = mult(rd(sFlat1,mult(x0,sFlat1)),x0),
inference(cp,[status(thm)],[t8,t1837]) ).
cnf(t1847,plain,
mult(rd(sFlat1,mult(x0,sFlat1)),x0) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t1841]) ).
cnf(t27764,plain,
ld(sFlat0,rd(sFlat0,sFlat0)) = ld(rd(mult(sFlat1,x0),x0),sFlat1),
inference(step,[status(thm)],[t26296,t1847]) ).
cnf(t27765,plain,
ld(sFlat0,sFlat0) = ld(rd(mult(sFlat1,x0),x0),sFlat1),
inference(step,[status(thm)],[t27764,t3440]) ).
cnf(t84,plain,
mult(sFlat0,sFlat0) = ld(sFlat0,sFlat0),
inference(cp,[status(thm)],[t9,t82]) ).
cnf(t86,plain,
ld(sFlat0,sFlat0) = mult(sFlat0,sFlat0),
inference(orient,[status(thm)],[t84]) ).
cnf(t26868,plain,
ld(sFlat0,sFlat0) = rd(sFlat0,sFlat0),
inference(step,[status(thm)],[t86,t288]) ).
cnf(t289,plain,
ld(sFlat0,sFlat0) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t26868]) ).
cnf(t26943,plain,
ld(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t289,t3440]) ).
cnf(t3441,plain,
ld(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t26943]) ).
cnf(t27766,plain,
sFlat0 = ld(rd(mult(sFlat1,x0),x0),sFlat1),
inference(step,[status(thm)],[t27765,t3441]) ).
cnf(t27767,plain,
sFlat0 = ld(sFlat1,sFlat1),
inference(step,[status(thm)],[t27766,t11]) ).
cnf(t27768,plain,
sFlat0 = rd(sFlat1,sFlat1),
inference(step,[status(thm)],[t27767,t17993]) ).
cnf(t26422,plain,
rd(sFlat1,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t27768]) ).
cnf(t26446,plain,
sFlat1 = ld(sFlat0,sFlat1),
inference(cp,[status(thm)],[t38,t26422]) ).
cnf(t27824,plain,
sFlat1 = x0,
inference(step,[status(thm)],[t26446,t37]) ).
cnf(t26587,plain,
x0 = sFlat1,
inference(orient,[status(thm)],[t27824]) ).
cnf(goal_0,negated_conjecture,
mult(ld(x1,x1),x0) != x0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
sFlat1 != x0,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_0,t26587]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP655-14 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.43 % Computer : n008.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Wed Sep 23 15:31:40 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 37.51/5.30 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.51/5.30 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------