%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP655-13 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.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 9.66s 6.17s
% Output : CNFRefutation 9.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 91
% Number of leaves : 8
% Syntax : Number of clauses : 364 ( 364 unt; 0 nHn; 52 RR)
% Number of literals : 364 ( 363 equ; 6 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 : 518 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(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(t16,plain,
mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(cp,[status(thm)],[t13,t8]) ).
cnf(t1227,plain,
mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(orient,[status(thm)],[t16]) ).
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(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(t14,plain,
mult(X1,mult(X2,mult(ld(mult(X1,X2),X3),X2))) = mult(X3,X2),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t251,plain,
mult(X1,mult(X2,mult(ld(mult(X1,X2),X3),X2))) = mult(X3,X2),
inference(orient,[status(thm)],[t14]) ).
cnf(t274,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(cp,[status(thm)],[t9,t251]) ).
cnf(t7385,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(orient,[status(thm)],[t274]) ).
cnf(t7473,plain,
ld(rd(X1,X2),mult(X3,X2)) = mult(X2,mult(ld(X1,X3),X2)),
inference(cp,[status(thm)],[t7385,t8]) ).
cnf(t7511,plain,
ld(rd(X1,X2),mult(X3,X2)) = mult(X2,mult(ld(X1,X3),X2)),
inference(orient,[status(thm)],[t7473]) ).
cnf(t7512,plain,
mult(X1,mult(ld(X2,rd(X2,X1)),X1)) = X1,
inference(cp,[status(thm)],[t7511,t9]) ).
cnf(t7695,plain,
mult(X1,mult(ld(X2,rd(X2,X1)),X1)) = X1,
inference(orient,[status(thm)],[t7512]) ).
cnf(t7778,plain,
mult(ld(X1,rd(X1,X2)),X2) = ld(X2,X2),
inference(cp,[status(thm)],[t9,t7695]) ).
cnf(t7800,plain,
mult(ld(X1,rd(X1,X2)),X2) = ld(X2,X2),
inference(orient,[status(thm)],[t7778]) ).
cnf(t7894,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = mult(rd(X1,X3),mult(X3,ld(X3,X3))),
inference(cp,[status(thm)],[t1227,t7800]) ).
cnf(t114815,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = mult(rd(X1,X3),X3),
inference(step,[status(thm)],[t7894,t7]) ).
cnf(t114816,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = X1,
inference(step,[status(thm)],[t114815,t8]) ).
cnf(t11404,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = X1,
inference(orient,[status(thm)],[t114816]) ).
cnf(t11415,plain,
rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
inference(cp,[status(thm)],[t11404,t8]) ).
cnf(t11546,plain,
rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t11415]) ).
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(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(t11548,plain,
mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
inference(cp,[status(thm)],[t11546,t39]) ).
cnf(t11664,plain,
mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
inference(orient,[status(thm)],[t11548]) ).
cnf(t7689,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(cp,[status(thm)],[t7511,t8]) ).
cnf(t28995,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(orient,[status(thm)],[t7689]) ).
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(t29048,plain,
ld(rd(rd(rd(X1,X2),X3),X2),X1) = mult(X2,mult(X3,X2)),
inference(cp,[status(thm)],[t28995,t38]) ).
cnf(t41322,plain,
ld(rd(rd(rd(X1,X2),X3),X2),X1) = mult(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t29048]) ).
cnf(t41707,plain,
rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
inference(cp,[status(thm)],[t39,t41322]) ).
cnf(t41736,plain,
rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
inference(orient,[status(thm)],[t41707]) ).
cnf(t42134,plain,
rd(rd(X1,X2),X3) = mult(rd(X1,mult(X2,mult(X3,X2))),X2),
inference(cp,[status(thm)],[t8,t41736]) ).
cnf(t48524,plain,
mult(rd(X1,mult(X2,mult(X3,X2))),X2) = rd(rd(X1,X2),X3),
inference(orient,[status(thm)],[t42134]) ).
cnf(t48693,plain,
rd(rd(X1,X2),rd(X3,X2)) = mult(rd(X1,mult(X2,X3)),X2),
inference(cp,[status(thm)],[t48524,t8]) ).
cnf(t48741,plain,
mult(rd(X1,mult(X2,X3)),X2) = rd(rd(X1,X2),rd(X3,X2)),
inference(orient,[status(thm)],[t48693]) ).
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(t46,plain,
mult(sFlat0,mult(X1,sFlat0)) = ld(x1,mult(mult(x1,X1),sFlat0)),
inference(cp,[status(thm)],[t9,t40]) ).
cnf(t103,plain,
ld(x1,mult(mult(x1,X1),sFlat0)) = mult(sFlat0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t46]) ).
cnf(t104,plain,
mult(sFlat0,mult(sFlat0,sFlat0)) = ld(x1,mult(x1,sFlat0)),
inference(cp,[status(thm)],[t103,t28]) ).
cnf(t114483,plain,
mult(sFlat0,mult(sFlat0,sFlat0)) = sFlat0,
inference(step,[status(thm)],[t104,t9]) ).
cnf(t108,plain,
mult(sFlat0,mult(sFlat0,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t114483]) ).
cnf(t1254,plain,
mult(mult(X1,sFlat0),sFlat0) = mult(rd(X1,sFlat0),sFlat0),
inference(cp,[status(thm)],[t1227,t108]) ).
cnf(t114500,plain,
mult(mult(X1,sFlat0),sFlat0) = X1,
inference(step,[status(thm)],[t1254,t8]) ).
cnf(t1323,plain,
mult(mult(X1,sFlat0),sFlat0) = X1,
inference(orient,[status(thm)],[t114500]) ).
cnf(t1343,plain,
rd(X1,sFlat0) = mult(X1,sFlat0),
inference(cp,[status(thm)],[t1323,t8]) ).
cnf(t1356,plain,
mult(X1,sFlat0) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t1343]) ).
cnf(t48802,plain,
rd(rd(X1,X2),rd(sFlat0,X2)) = mult(rd(X1,rd(X2,sFlat0)),X2),
inference(cp,[status(thm)],[t48741,t1356]) ).
cnf(t48939,plain,
mult(rd(X1,rd(X2,sFlat0)),X2) = rd(rd(X1,X2),rd(sFlat0,X2)),
inference(orient,[status(thm)],[t48802]) ).
cnf(t6,axiom,
sFlat1 = mult(x0,ld(x1,x1)),
introduced(definition) ).
cnf(t21,plain,
mult(x0,ld(x1,x1)) = sFlat1,
inference(orient,[status(thm)],[t6]) ).
cnf(t114482,plain,
mult(x0,sFlat0) = sFlat1,
inference(step,[status(thm)],[t21,t25]) ).
cnf(t27,plain,
mult(x0,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t114482]) ).
cnf(t31,plain,
mult(x0,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t27]) ).
cnf(t32,plain,
x0 = rd(sFlat1,sFlat0),
inference(cp,[status(thm)],[t11,t31]) ).
cnf(t36,plain,
rd(sFlat1,sFlat0) = x0,
inference(orient,[status(thm)],[t32]) ).
cnf(t49144,plain,
rd(rd(X1,sFlat1),rd(sFlat0,sFlat1)) = mult(rd(X1,x0),sFlat1),
inference(cp,[status(thm)],[t48939,t36]) ).
cnf(t49305,plain,
rd(rd(X1,sFlat1),rd(sFlat0,sFlat1)) = mult(rd(X1,x0),sFlat1),
inference(orient,[status(thm)],[t49144]) ).
cnf(t49317,plain,
mult(rd(mult(X1,sFlat1),x0),sFlat1) = rd(X1,rd(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t49305,t11]) ).
cnf(t49514,plain,
mult(rd(mult(X1,sFlat1),x0),sFlat1) = rd(X1,rd(sFlat0,sFlat1)),
inference(orient,[status(thm)],[t49317]) ).
cnf(t49533,plain,
sFlat1 = ld(rd(mult(X1,sFlat1),x0),rd(X1,rd(sFlat0,sFlat1))),
inference(cp,[status(thm)],[t9,t49514]) ).
cnf(t58588,plain,
ld(rd(mult(X1,sFlat1),x0),rd(X1,rd(sFlat0,sFlat1))) = sFlat1,
inference(orient,[status(thm)],[t49533]) ).
cnf(t1373,plain,
rd(rd(X1,sFlat0),sFlat0) = X1,
inference(cp,[status(thm)],[t1356,t8]) ).
cnf(t1424,plain,
rd(rd(X1,sFlat0),sFlat0) = X1,
inference(orient,[status(thm)],[t1373]) ).
cnf(t11745,plain,
ld(X1,X2) = ld(X3,rd(X3,ld(X2,X1))),
inference(cp,[status(thm)],[t9,t11664]) ).
cnf(t11881,plain,
ld(X1,rd(X1,ld(X2,X3))) = ld(X3,X2),
inference(orient,[status(thm)],[t11745]) ).
cnf(t34,plain,
mult(x0,mult(sFlat0,mult(X1,sFlat0))) = mult(mult(sFlat1,X1),sFlat0),
inference(cp,[status(thm)],[t13,t31]) ).
cnf(t64,plain,
mult(x0,mult(sFlat0,mult(X1,sFlat0))) = mult(mult(sFlat1,X1),sFlat0),
inference(orient,[status(thm)],[t34]) ).
cnf(t112,plain,
mult(mult(sFlat1,sFlat0),sFlat0) = mult(x0,sFlat0),
inference(cp,[status(thm)],[t64,t108]) ).
cnf(t114484,plain,
mult(mult(sFlat1,sFlat0),sFlat0) = sFlat1,
inference(step,[status(thm)],[t112,t31]) ).
cnf(t116,plain,
mult(mult(sFlat1,sFlat0),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t114484]) ).
cnf(t117,plain,
mult(sFlat1,sFlat0) = rd(sFlat1,sFlat0),
inference(cp,[status(thm)],[t11,t116]) ).
cnf(t114485,plain,
mult(sFlat1,sFlat0) = x0,
inference(step,[status(thm)],[t117,t36]) ).
cnf(t122,plain,
mult(sFlat1,sFlat0) = x0,
inference(orient,[status(thm)],[t114485]) ).
cnf(t125,plain,
mult(sFlat1,mult(sFlat0,mult(X1,sFlat0))) = mult(mult(x0,X1),sFlat0),
inference(cp,[status(thm)],[t13,t122]) ).
cnf(t179,plain,
mult(sFlat1,mult(sFlat0,mult(X1,sFlat0))) = mult(mult(x0,X1),sFlat0),
inference(orient,[status(thm)],[t125]) ).
cnf(t195,plain,
mult(sFlat0,mult(X1,sFlat0)) = ld(sFlat1,mult(mult(x0,X1),sFlat0)),
inference(cp,[status(thm)],[t9,t179]) ).
cnf(t314,plain,
ld(sFlat1,mult(mult(x0,X1),sFlat0)) = mult(sFlat0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t195]) ).
cnf(t114546,plain,
ld(sFlat1,rd(mult(x0,X1),sFlat0)) = mult(sFlat0,mult(X1,sFlat0)),
inference(step,[status(thm)],[t314,t1356]) ).
cnf(t70,plain,
mult(mult(sFlat1,rd(X1,sFlat0)),sFlat0) = mult(x0,mult(sFlat0,X1)),
inference(cp,[status(thm)],[t64,t8]) ).
cnf(t152,plain,
mult(mult(sFlat1,rd(X1,sFlat0)),sFlat0) = mult(x0,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t70]) ).
cnf(t159,plain,
mult(sFlat1,rd(X1,sFlat0)) = rd(mult(x0,mult(sFlat0,X1)),sFlat0),
inference(cp,[status(thm)],[t11,t152]) ).
cnf(t234,plain,
rd(mult(x0,mult(sFlat0,X1)),sFlat0) = mult(sFlat1,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t159]) ).
cnf(t236,plain,
mult(sFlat1,rd(ld(sFlat0,X1),sFlat0)) = rd(mult(x0,X1),sFlat0),
inference(cp,[status(thm)],[t234,t7]) ).
cnf(t320,plain,
mult(sFlat1,rd(ld(sFlat0,X1),sFlat0)) = rd(mult(x0,X1),sFlat0),
inference(orient,[status(thm)],[t236]) ).
cnf(t325,plain,
rd(ld(sFlat0,X1),sFlat0) = ld(sFlat1,rd(mult(x0,X1),sFlat0)),
inference(cp,[status(thm)],[t9,t320]) ).
cnf(t401,plain,
ld(sFlat1,rd(mult(x0,X1),sFlat0)) = rd(ld(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t325]) ).
cnf(t114547,plain,
rd(ld(sFlat0,X1),sFlat0) = mult(sFlat0,mult(X1,sFlat0)),
inference(step,[status(thm)],[t114546,t401]) ).
cnf(t114548,plain,
rd(ld(sFlat0,X1),sFlat0) = mult(sFlat0,rd(X1,sFlat0)),
inference(step,[status(thm)],[t114547,t1356]) ).
cnf(t1412,plain,
rd(ld(sFlat0,X1),sFlat0) = mult(sFlat0,rd(X1,sFlat0)),
inference(rw,[status(thm)],[t114548]) ).
cnf(t1685,plain,
mult(sFlat0,rd(X1,sFlat0)) = rd(ld(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t1412]) ).
cnf(t1689,plain,
rd(ld(sFlat0,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t1685,t1424]) ).
cnf(t1753,plain,
rd(ld(sFlat0,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t1689]) ).
cnf(t1775,plain,
ld(sFlat0,rd(X1,sFlat0)) = rd(mult(sFlat0,X1),sFlat0),
inference(cp,[status(thm)],[t1424,t1753]) ).
cnf(t1789,plain,
ld(sFlat0,rd(X1,sFlat0)) = rd(mult(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t1775]) ).
cnf(t11926,plain,
ld(rd(X1,sFlat0),sFlat0) = ld(X2,rd(X2,rd(mult(sFlat0,X1),sFlat0))),
inference(cp,[status(thm)],[t11881,t1789]) ).
cnf(t30117,plain,
ld(X1,rd(X1,rd(mult(sFlat0,X2),sFlat0))) = ld(rd(X2,sFlat0),sFlat0),
inference(orient,[status(thm)],[t11926]) ).
cnf(t1316,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(rd(X1,X3),mult(X3,X2)),
inference(cp,[status(thm)],[t1227,t8]) ).
cnf(t3029,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(rd(X1,X3),mult(X3,X2)),
inference(orient,[status(thm)],[t1316]) ).
cnf(t3109,plain,
mult(X1,rd(X2,X3)) = rd(mult(rd(X1,X3),mult(X3,X2)),X3),
inference(cp,[status(thm)],[t11,t3029]) ).
cnf(t28042,plain,
rd(mult(rd(X1,X2),mult(X2,X3)),X2) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t3109]) ).
cnf(t28270,plain,
mult(X1,rd(sFlat0,X2)) = rd(mult(rd(X1,X2),rd(X2,sFlat0)),X2),
inference(cp,[status(thm)],[t28042,t1356]) ).
cnf(t34954,plain,
rd(mult(rd(X1,X2),rd(X2,sFlat0)),X2) = mult(X1,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t28270]) ).
cnf(t17,plain,
mult(mult(X1,X2),X3) = rd(mult(X1,mult(X2,mult(X3,X2))),X2),
inference(cp,[status(thm)],[t11,t13]) ).
cnf(t1470,plain,
rd(mult(X1,mult(X2,mult(X3,X2))),X2) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t17]) ).
cnf(t1813,plain,
sFlat0 = rd(rd(X1,sFlat0),rd(mult(sFlat0,X1),sFlat0)),
inference(cp,[status(thm)],[t39,t1789]) ).
cnf(t2767,plain,
rd(rd(X1,sFlat0),rd(mult(sFlat0,X1),sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t1813]) ).
cnf(t2805,plain,
sFlat0 = rd(rd(mult(sFlat0,mult(X1,sFlat0)),sFlat0),mult(mult(sFlat0,sFlat0),X1)),
inference(cp,[status(thm)],[t2767,t1470]) ).
cnf(t114610,plain,
sFlat0 = rd(rd(mult(sFlat0,rd(X1,sFlat0)),sFlat0),mult(mult(sFlat0,sFlat0),X1)),
inference(step,[status(thm)],[t2805,t1356]) ).
cnf(t114611,plain,
sFlat0 = rd(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),mult(mult(sFlat0,sFlat0),X1)),
inference(step,[status(thm)],[t114610,t1685]) ).
cnf(t114612,plain,
sFlat0 = rd(ld(sFlat0,X1),mult(mult(sFlat0,sFlat0),X1)),
inference(step,[status(thm)],[t114611,t1424]) ).
cnf(t114613,plain,
sFlat0 = rd(ld(sFlat0,X1),mult(rd(sFlat0,sFlat0),X1)),
inference(step,[status(thm)],[t114612,t1356]) ).
cnf(t2817,plain,
rd(ld(sFlat0,X1),mult(rd(sFlat0,sFlat0),X1)) = sFlat0,
inference(orient,[status(thm)],[t114613]) ).
cnf(t2838,plain,
mult(rd(sFlat0,sFlat0),X1) = ld(sFlat0,ld(sFlat0,X1)),
inference(cp,[status(thm)],[t38,t2817]) ).
cnf(t2842,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(rd(sFlat0,sFlat0),X1),
inference(orient,[status(thm)],[t2838]) ).
cnf(t7884,plain,
X1 = ld(ld(X2,rd(X2,X1)),ld(X1,X1)),
inference(cp,[status(thm)],[t9,t7800]) ).
cnf(t8090,plain,
ld(ld(X1,rd(X1,X2)),ld(X2,X2)) = X2,
inference(orient,[status(thm)],[t7884]) ).
cnf(t8168,plain,
x1 = ld(ld(X1,rd(X1,x1)),sFlat0),
inference(cp,[status(thm)],[t8090,t25]) ).
cnf(t8173,plain,
ld(ld(X1,rd(X1,x1)),sFlat0) = x1,
inference(orient,[status(thm)],[t8168]) ).
cnf(t8178,plain,
ld(X1,rd(X1,x1)) = rd(sFlat0,x1),
inference(cp,[status(thm)],[t39,t8173]) ).
cnf(t8181,plain,
ld(X1,rd(X1,x1)) = rd(sFlat0,x1),
inference(orient,[status(thm)],[t8178]) ).
cnf(t8189,plain,
mult(rd(sFlat0,sFlat0),rd(sFlat0,x1)) = ld(sFlat0,rd(sFlat0,x1)),
inference(cp,[status(thm)],[t2842,t8181]) ).
cnf(t8185,plain,
rd(X1,x1) = mult(X1,rd(sFlat0,x1)),
inference(cp,[status(thm)],[t7,t8181]) ).
cnf(t8211,plain,
mult(X1,rd(sFlat0,x1)) = rd(X1,x1),
inference(orient,[status(thm)],[t8185]) ).
cnf(t114655,plain,
rd(rd(sFlat0,sFlat0),x1) = ld(sFlat0,rd(sFlat0,x1)),
inference(step,[status(thm)],[t8189,t8211]) ).
cnf(t114656,plain,
rd(rd(sFlat0,sFlat0),x1) = rd(sFlat0,x1),
inference(step,[status(thm)],[t114655,t8181]) ).
cnf(t8261,plain,
rd(rd(sFlat0,sFlat0),x1) = rd(sFlat0,x1),
inference(orient,[status(thm)],[t114656]) ).
cnf(t8265,plain,
rd(sFlat0,sFlat0) = mult(rd(sFlat0,x1),x1),
inference(cp,[status(thm)],[t8,t8261]) ).
cnf(t114657,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t8265,t8]) ).
cnf(t8270,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t114657]) ).
cnf(t114660,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(sFlat0,X1),
inference(step,[status(thm)],[t2842,t8270]) ).
cnf(t8273,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t114660]) ).
cnf(t11920,plain,
ld(ld(sFlat0,X1),sFlat0) = ld(X2,rd(X2,mult(sFlat0,X1))),
inference(cp,[status(thm)],[t11881,t8273]) ).
cnf(t13441,plain,
ld(X1,rd(X1,mult(sFlat0,X2))) = ld(ld(sFlat0,X2),sFlat0),
inference(orient,[status(thm)],[t11920]) ).
cnf(t13472,plain,
ld(mult(sFlat0,X1),mult(sFlat0,X1)) = mult(ld(ld(sFlat0,X1),sFlat0),mult(sFlat0,X1)),
inference(cp,[status(thm)],[t7800,t13441]) ).
cnf(t28306,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)],[t28042,t7800]) ).
cnf(t115267,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)],[t28306,t11546]) ).
cnf(t115268,plain,
mult(X1,mult(X2,X2)) = mult(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t115267,t11546]) ).
cnf(t115269,plain,
mult(X1,mult(X2,X2)) = mult(rd(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t115268,t11664]) ).
cnf(t115270,plain,
mult(X1,mult(X2,X2)) = mult(rd(mult(X1,X2),ld(X2,X2)),X2),
inference(step,[status(thm)],[t115269,t11546]) ).
cnf(t35292,plain,
mult(rd(mult(X1,X2),ld(X2,X2)),X2) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t115270]) ).
cnf(t35423,plain,
mult(rd(X1,X2),mult(X2,X2)) = mult(rd(X1,ld(X2,X2)),X2),
inference(cp,[status(thm)],[t35292,t8]) ).
cnf(t35462,plain,
mult(rd(X1,ld(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t35423]) ).
cnf(t35496,plain,
rd(X1,ld(X2,X2)) = rd(mult(rd(X1,X2),mult(X2,X2)),X2),
inference(cp,[status(thm)],[t11,t35462]) ).
cnf(t115271,plain,
rd(X1,ld(X2,X2)) = mult(X1,rd(X2,X2)),
inference(step,[status(thm)],[t35496,t28042]) ).
cnf(t35526,plain,
mult(X1,rd(X2,X2)) = rd(X1,ld(X2,X2)),
inference(orient,[status(thm)],[t115271]) ).
cnf(t35554,plain,
rd(X1,X1) = ld(X2,rd(X2,ld(X1,X1))),
inference(cp,[status(thm)],[t9,t35526]) ).
cnf(t115280,plain,
rd(X1,X1) = ld(X1,X1),
inference(step,[status(thm)],[t35554,t11881]) ).
cnf(t35603,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t115280]) ).
cnf(t116325,plain,
rd(mult(sFlat0,X1),mult(sFlat0,X1)) = mult(ld(ld(sFlat0,X1),sFlat0),mult(sFlat0,X1)),
inference(step,[status(thm)],[t13472,t35603]) ).
cnf(t112400,plain,
mult(ld(ld(sFlat0,X1),sFlat0),mult(sFlat0,X1)) = rd(mult(sFlat0,X1),mult(sFlat0,X1)),
inference(orient,[status(thm)],[t116325]) ).
cnf(t112581,plain,
mult(mult(ld(ld(sFlat0,mult(X1,sFlat0)),sFlat0),sFlat0),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(cp,[status(thm)],[t1470,t112400]) ).
cnf(t116326,plain,
mult(rd(ld(ld(sFlat0,mult(X1,sFlat0)),sFlat0),sFlat0),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t112581,t1356]) ).
cnf(t116327,plain,
mult(rd(ld(ld(sFlat0,rd(X1,sFlat0)),sFlat0),sFlat0),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t116326,t1356]) ).
cnf(t116328,plain,
mult(rd(ld(rd(mult(sFlat0,X1),sFlat0),sFlat0),sFlat0),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t116327,t1789]) ).
cnf(t7611,plain,
mult(sFlat0,mult(ld(X1,X2),sFlat0)) = ld(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(cp,[status(thm)],[t7511,t1356]) ).
cnf(t114917,plain,
mult(sFlat0,rd(ld(X1,X2),sFlat0)) = ld(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(step,[status(thm)],[t7611,t1356]) ).
cnf(t114918,plain,
rd(ld(sFlat0,ld(X1,X2)),sFlat0) = ld(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(step,[status(thm)],[t114917,t1685]) ).
cnf(t14451,plain,
ld(rd(X1,sFlat0),rd(X2,sFlat0)) = rd(ld(sFlat0,ld(X1,X2)),sFlat0),
inference(orient,[status(thm)],[t114918]) ).
cnf(t14599,plain,
rd(ld(sFlat0,ld(X1,sFlat0)),sFlat0) = ld(rd(X1,sFlat0),sFlat0),
inference(cp,[status(thm)],[t14451,t8270]) ).
cnf(t14655,plain,
rd(ld(sFlat0,ld(X1,sFlat0)),sFlat0) = ld(rd(X1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t14599]) ).
cnf(t14658,plain,
ld(rd(rd(sFlat0,X1),sFlat0),sFlat0) = rd(ld(sFlat0,X1),sFlat0),
inference(cp,[status(thm)],[t14655,t38]) ).
cnf(t14974,plain,
ld(rd(rd(sFlat0,X1),sFlat0),sFlat0) = rd(ld(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t14658]) ).
cnf(t14977,plain,
rd(ld(sFlat0,ld(X1,rd(X1,X2))),sFlat0) = ld(rd(mult(sFlat0,X2),sFlat0),sFlat0),
inference(cp,[status(thm)],[t14974,t11546]) ).
cnf(t3031,plain,
mult(rd(X1,sFlat0),mult(sFlat0,X2)) = rd(mult(X1,rd(X2,sFlat0)),sFlat0),
inference(cp,[status(thm)],[t3029,t1356]) ).
cnf(t4545,plain,
mult(rd(X1,sFlat0),mult(sFlat0,X2)) = rd(mult(X1,rd(X2,sFlat0)),sFlat0),
inference(orient,[status(thm)],[t3031]) ).
cnf(t8283,plain,
rd(mult(sFlat0,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,mult(sFlat0,X1)),
inference(cp,[status(thm)],[t4545,t8270]) ).
cnf(t114675,plain,
rd(rd(ld(sFlat0,X1),sFlat0),sFlat0) = mult(sFlat0,mult(sFlat0,X1)),
inference(step,[status(thm)],[t8283,t1685]) ).
cnf(t114676,plain,
ld(sFlat0,X1) = mult(sFlat0,mult(sFlat0,X1)),
inference(step,[status(thm)],[t114675,t1424]) ).
cnf(t8314,plain,
mult(sFlat0,mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(orient,[status(thm)],[t114676]) ).
cnf(t11739,plain,
ld(sFlat0,ld(X1,X2)) = mult(sFlat0,rd(sFlat0,ld(X2,X1))),
inference(cp,[status(thm)],[t8314,t11664]) ).
cnf(t12057,plain,
mult(sFlat0,rd(sFlat0,ld(X1,X2))) = ld(sFlat0,ld(X2,X1)),
inference(orient,[status(thm)],[t11739]) ).
cnf(t12108,plain,
ld(sFlat0,ld(X1,rd(X1,X2))) = mult(sFlat0,rd(sFlat0,X2)),
inference(cp,[status(thm)],[t12057,t38]) ).
cnf(t13675,plain,
ld(sFlat0,ld(X1,rd(X1,X2))) = mult(sFlat0,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t12108]) ).
cnf(t115045,plain,
rd(mult(sFlat0,rd(sFlat0,X2)),sFlat0) = ld(rd(mult(sFlat0,X2),sFlat0),sFlat0),
inference(step,[status(thm)],[t14977,t13675]) ).
cnf(t21715,plain,
ld(rd(mult(sFlat0,X1),sFlat0),sFlat0) = rd(mult(sFlat0,rd(sFlat0,X1)),sFlat0),
inference(orient,[status(thm)],[t115045]) ).
cnf(t116329,plain,
mult(rd(rd(mult(sFlat0,rd(sFlat0,X1)),sFlat0),sFlat0),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t116328,t21715]) ).
cnf(t116330,plain,
mult(mult(sFlat0,rd(sFlat0,X1)),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t116329,t1424]) ).
cnf(t116331,plain,
mult(rd(sFlat0,X1),mult(X1,sFlat0)) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t116330,t3029]) ).
cnf(t116332,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t116331,t1356]) ).
cnf(t1372,plain,
rd(mult(mult(X1,sFlat0),X2),sFlat0) = mult(X1,mult(sFlat0,mult(X2,sFlat0))),
inference(cp,[status(thm)],[t1356,t13]) ).
cnf(t114635,plain,
rd(mult(rd(X1,sFlat0),X2),sFlat0) = mult(X1,mult(sFlat0,mult(X2,sFlat0))),
inference(step,[status(thm)],[t1372,t1356]) ).
cnf(t114636,plain,
rd(mult(rd(X1,sFlat0),X2),sFlat0) = mult(X1,mult(sFlat0,rd(X2,sFlat0))),
inference(step,[status(thm)],[t114635,t1356]) ).
cnf(t114637,plain,
rd(mult(rd(X1,sFlat0),X2),sFlat0) = mult(X1,rd(ld(sFlat0,X2),sFlat0)),
inference(step,[status(thm)],[t114636,t1685]) ).
cnf(t3713,plain,
mult(X1,rd(ld(sFlat0,X2),sFlat0)) = rd(mult(rd(X1,sFlat0),X2),sFlat0),
inference(orient,[status(thm)],[t114637]) ).
cnf(t7883,plain,
ld(X1,rd(X1,X2)) = rd(ld(X2,X2),X2),
inference(cp,[status(thm)],[t11,t7800]) ).
cnf(t25871,plain,
ld(X1,rd(X1,X2)) = rd(ld(X2,X2),X2),
inference(orient,[status(thm)],[t7883]) ).
cnf(t26041,plain,
mult(sFlat0,rd(sFlat0,X1)) = ld(sFlat0,rd(ld(X1,X1),X1)),
inference(cp,[status(thm)],[t8273,t25871]) ).
cnf(t26192,plain,
ld(sFlat0,rd(ld(X1,X1),X1)) = mult(sFlat0,rd(sFlat0,X1)),
inference(orient,[status(thm)],[t26041]) ).
cnf(t26217,plain,
rd(mult(rd(X1,sFlat0),rd(ld(X2,X2),X2)),sFlat0) = mult(X1,rd(mult(sFlat0,rd(sFlat0,X2)),sFlat0)),
inference(cp,[status(thm)],[t3713,t26192]) ).
cnf(t26038,plain,
rd(X1,ld(rd(X2,X3),X2)) = mult(X1,rd(ld(X3,X3),X3)),
inference(cp,[status(thm)],[t11664,t25871]) ).
cnf(t115109,plain,
rd(X1,X3) = mult(X1,rd(ld(X3,X3),X3)),
inference(step,[status(thm)],[t26038,t38]) ).
cnf(t26109,plain,
mult(X1,rd(ld(X2,X2),X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t115109]) ).
cnf(t115110,plain,
rd(rd(rd(X1,sFlat0),X2),sFlat0) = mult(X1,rd(mult(sFlat0,rd(sFlat0,X2)),sFlat0)),
inference(step,[status(thm)],[t26217,t26109]) ).
cnf(t11627,plain,
mult(X1,rd(mult(sFlat0,X2),sFlat0)) = rd(X1,ld(rd(X2,sFlat0),sFlat0)),
inference(cp,[status(thm)],[t11546,t2767]) ).
cnf(t20164,plain,
mult(X1,rd(mult(sFlat0,X2),sFlat0)) = rd(X1,ld(rd(X2,sFlat0),sFlat0)),
inference(orient,[status(thm)],[t11627]) ).
cnf(t115111,plain,
rd(rd(rd(X1,sFlat0),X2),sFlat0) = rd(X1,ld(rd(rd(sFlat0,X2),sFlat0),sFlat0)),
inference(step,[status(thm)],[t115110,t20164]) ).
cnf(t115112,plain,
rd(rd(rd(X1,sFlat0),X2),sFlat0) = rd(X1,rd(ld(sFlat0,X2),sFlat0)),
inference(step,[status(thm)],[t115111,t14974]) ).
cnf(t26219,plain,
rd(rd(rd(X1,sFlat0),X2),sFlat0) = rd(X1,rd(ld(sFlat0,X2),sFlat0)),
inference(orient,[status(thm)],[t115112]) ).
cnf(t26360,plain,
rd(rd(X1,sFlat0),rd(ld(sFlat0,X2),sFlat0)) = rd(rd(X1,X2),sFlat0),
inference(cp,[status(thm)],[t26219,t1424]) ).
cnf(t33369,plain,
rd(rd(X1,sFlat0),rd(ld(sFlat0,X2),sFlat0)) = rd(rd(X1,X2),sFlat0),
inference(orient,[status(thm)],[t26360]) ).
cnf(t33615,plain,
rd(rd(X1,mult(sFlat0,X2)),sFlat0) = rd(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(cp,[status(thm)],[t33369,t9]) ).
cnf(t33991,plain,
rd(rd(X1,mult(sFlat0,X2)),sFlat0) = rd(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(orient,[status(thm)],[t33615]) ).
cnf(t116333,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),sFlat0),rd(mult(X1,sFlat0),sFlat0)),
inference(step,[status(thm)],[t116332,t33991]) ).
cnf(t116334,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(rd(mult(sFlat0,rd(X1,sFlat0)),sFlat0),rd(mult(X1,sFlat0),sFlat0)),
inference(step,[status(thm)],[t116333,t1356]) ).
cnf(t116335,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),rd(mult(X1,sFlat0),sFlat0)),
inference(step,[status(thm)],[t116334,t1685]) ).
cnf(t116336,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(ld(sFlat0,X1),rd(mult(X1,sFlat0),sFlat0)),
inference(step,[status(thm)],[t116335,t1424]) ).
cnf(t116337,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(ld(sFlat0,X1),X1),
inference(step,[status(thm)],[t116336,t11]) ).
cnf(t112583,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(ld(sFlat0,X1),X1),
inference(orient,[status(thm)],[t116337]) ).
cnf(t112962,plain,
mult(sFlat0,rd(sFlat0,X1)) = rd(rd(ld(sFlat0,X1),X1),X1),
inference(cp,[status(thm)],[t34954,t112583]) ).
cnf(t112975,plain,
rd(rd(ld(sFlat0,X1),X1),X1) = mult(sFlat0,rd(sFlat0,X1)),
inference(orient,[status(thm)],[t112962]) ).
cnf(t35652,plain,
ld(X1,X1) = ld(X2,rd(X2,rd(X1,X1))),
inference(cp,[status(thm)],[t11881,t35603]) ).
cnf(t115365,plain,
rd(X1,X1) = ld(X2,rd(X2,rd(X1,X1))),
inference(step,[status(thm)],[t35652,t35603]) ).
cnf(t35831,plain,
ld(X1,rd(X1,rd(X2,X2))) = rd(X2,X2),
inference(orient,[status(thm)],[t115365]) ).
cnf(t113083,plain,
mult(sFlat0,rd(sFlat0,rd(sFlat0,rd(X1,X1)))) = rd(rd(rd(X1,X1),rd(sFlat0,rd(X1,X1))),rd(sFlat0,rd(X1,X1))),
inference(cp,[status(thm)],[t112975,t35831]) ).
cnf(t35624,plain,
rd(rd(X1,sFlat0),rd(X1,sFlat0)) = rd(ld(sFlat0,ld(X1,X1)),sFlat0),
inference(cp,[status(thm)],[t35603,t14451]) ).
cnf(t115398,plain,
rd(rd(X1,sFlat0),rd(X1,sFlat0)) = rd(ld(sFlat0,rd(X1,X1)),sFlat0),
inference(step,[status(thm)],[t35624,t35603]) ).
cnf(t37336,plain,
rd(ld(sFlat0,rd(X1,X1)),sFlat0) = rd(rd(X1,sFlat0),rd(X1,sFlat0)),
inference(orient,[status(thm)],[t115398]) ).
cnf(t37359,plain,
ld(sFlat0,rd(X1,X1)) = rd(rd(rd(X1,sFlat0),rd(X1,sFlat0)),sFlat0),
inference(cp,[status(thm)],[t1424,t37336]) ).
cnf(t115399,plain,
ld(sFlat0,rd(X1,X1)) = rd(X1,rd(ld(sFlat0,rd(X1,sFlat0)),sFlat0)),
inference(step,[status(thm)],[t37359,t26219]) ).
cnf(t115400,plain,
ld(sFlat0,rd(X1,X1)) = rd(X1,mult(sFlat0,X1)),
inference(step,[status(thm)],[t115399,t1753]) ).
cnf(t37415,plain,
ld(sFlat0,rd(X1,X1)) = rd(X1,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t115400]) ).
cnf(t1503,plain,
mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
inference(cp,[status(thm)],[t1470,t8]) ).
cnf(t3927,plain,
mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
inference(orient,[status(thm)],[t1503]) ).
cnf(t35625,plain,
X1 = rd(X1,rd(X1,X1)),
inference(cp,[status(thm)],[t39,t35603]) ).
cnf(t35683,plain,
rd(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t35625]) ).
cnf(t35689,plain,
rd(mult(X1,mult(rd(X2,X2),X2)),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
inference(cp,[status(thm)],[t3927,t35683]) ).
cnf(t115405,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t35689,t8]) ).
cnf(t115406,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(rd(X1,X2),mult(X2,X2)),
inference(step,[status(thm)],[t115405,t3029]) ).
cnf(t38005,plain,
mult(rd(X1,X2),mult(X2,X2)) = rd(mult(X1,X2),rd(X2,X2)),
inference(orient,[status(thm)],[t115406]) ).
cnf(t115336,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(step,[status(thm)],[t8090,t35603]) ).
cnf(t35678,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(rw,[status(thm)],[t115336]) ).
cnf(t36906,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(orient,[status(thm)],[t35678]) ).
cnf(t26080,plain,
mult(X1,X2) = rd(X1,rd(ld(X2,X2),X2)),
inference(cp,[status(thm)],[t11546,t25871]) ).
cnf(t26171,plain,
rd(X1,rd(ld(X2,X2),X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t26080]) ).
cnf(t115324,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(step,[status(thm)],[t26171,t35603]) ).
cnf(t35672,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(rw,[status(thm)],[t115324]) ).
cnf(t36062,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t35672]) ).
cnf(t36920,plain,
rd(rd(X1,X1),X1) = ld(ld(X2,mult(X2,X1)),rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
inference(cp,[status(thm)],[t36906,t36062]) ).
cnf(t115394,plain,
rd(rd(X1,X1),X1) = ld(X1,rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
inference(step,[status(thm)],[t36920,t9]) ).
cnf(t115395,plain,
rd(rd(X1,X1),X1) = ld(X1,mult(rd(rd(X1,X1),X1),X1)),
inference(step,[status(thm)],[t115394,t36062]) ).
cnf(t115396,plain,
rd(rd(X1,X1),X1) = ld(X1,rd(X1,X1)),
inference(step,[status(thm)],[t115395,t8]) ).
cnf(t37142,plain,
ld(X1,rd(X1,X1)) = rd(rd(X1,X1),X1),
inference(orient,[status(thm)],[t115396]) ).
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(t707,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(t727,plain,
mult(mult(X1,X2),ld(X2,X1)) = mult(X2,mult(ld(X2,X1),X1)),
inference(cp,[status(thm)],[t707,t7]) ).
cnf(t1043,plain,
mult(mult(X1,X2),ld(X2,X1)) = mult(X2,mult(ld(X2,X1),X1)),
inference(orient,[status(thm)],[t727]) ).
cnf(t114822,plain,
rd(mult(X1,X2),ld(X1,X2)) = mult(X2,mult(ld(X2,X1),X1)),
inference(step,[status(thm)],[t1043,t11664]) ).
cnf(t11776,plain,
rd(mult(X1,X2),ld(X1,X2)) = mult(X2,mult(ld(X2,X1),X1)),
inference(rw,[status(thm)],[t114822]) ).
cnf(t20435,plain,
mult(X1,mult(ld(X1,X2),X2)) = rd(mult(X2,X1),ld(X2,X1)),
inference(orient,[status(thm)],[t11776]) ).
cnf(t35644,plain,
rd(mult(X1,X1),ld(X1,X1)) = mult(X1,mult(rd(X1,X1),X1)),
inference(cp,[status(thm)],[t20435,t35603]) ).
cnf(t115363,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,mult(rd(X1,X1),X1)),
inference(step,[status(thm)],[t35644,t35603]) ).
cnf(t115364,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
inference(step,[status(thm)],[t115363,t8]) ).
cnf(t35791,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t115364]) ).
cnf(t35819,plain,
rd(X1,X1) = ld(mult(X1,X1),mult(X1,X1)),
inference(cp,[status(thm)],[t38,t35791]) ).
cnf(t115369,plain,
rd(X1,X1) = rd(mult(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t35819,t35603]) ).
cnf(t36158,plain,
rd(mult(X1,X1),mult(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t115369]) ).
cnf(t37158,plain,
rd(rd(mult(X1,X1),mult(X1,X1)),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t37142,t36158]) ).
cnf(t115415,plain,
rd(rd(X1,X1),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
inference(step,[status(thm)],[t37158,t36158]) ).
cnf(t7480,plain,
mult(ld(mult(X1,X2),X3),X2) = ld(X2,ld(X1,mult(X3,X2))),
inference(cp,[status(thm)],[t9,t7385]) ).
cnf(t14353,plain,
ld(X1,ld(X2,mult(X3,X1))) = mult(ld(mult(X2,X1),X3),X1),
inference(orient,[status(thm)],[t7480]) ).
cnf(t14427,plain,
mult(ld(mult(X1,X2),rd(X3,X2)),X2) = ld(X2,ld(X1,X3)),
inference(cp,[status(thm)],[t14353,t8]) ).
cnf(t30471,plain,
mult(ld(mult(X1,X2),rd(X3,X2)),X2) = ld(X2,ld(X1,X3)),
inference(orient,[status(thm)],[t14427]) ).
cnf(t30814,plain,
ld(mult(X1,X2),rd(X3,X2)) = rd(ld(X2,ld(X1,X3)),X2),
inference(cp,[status(thm)],[t11,t30471]) ).
cnf(t30846,plain,
ld(mult(X1,X2),rd(X3,X2)) = rd(ld(X2,ld(X1,X3)),X2),
inference(orient,[status(thm)],[t30814]) ).
cnf(t115416,plain,
rd(rd(X1,X1),mult(X1,X1)) = rd(ld(X1,ld(X1,X1)),X1),
inference(step,[status(thm)],[t115415,t30846]) ).
cnf(t115417,plain,
rd(rd(X1,X1),mult(X1,X1)) = rd(ld(X1,rd(X1,X1)),X1),
inference(step,[status(thm)],[t115416,t35603]) ).
cnf(t115418,plain,
rd(rd(X1,X1),mult(X1,X1)) = rd(rd(rd(X1,X1),X1),X1),
inference(step,[status(thm)],[t115417,t37142]) ).
cnf(t38293,plain,
rd(rd(rd(X1,X1),X1),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(orient,[status(thm)],[t115418]) ).
cnf(t38315,plain,
rd(mult(rd(rd(X1,X1),X1),X1),rd(X1,X1)) = mult(rd(rd(X1,X1),mult(X1,X1)),mult(X1,X1)),
inference(cp,[status(thm)],[t38005,t38293]) ).
cnf(t115419,plain,
rd(rd(X1,X1),rd(X1,X1)) = mult(rd(rd(X1,X1),mult(X1,X1)),mult(X1,X1)),
inference(step,[status(thm)],[t38315,t8]) ).
cnf(t115420,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(step,[status(thm)],[t115419,t8]) ).
cnf(t38371,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t115420]) ).
cnf(t38376,plain,
rd(rd(X1,X1),mult(sFlat0,rd(X1,X1))) = ld(sFlat0,rd(X1,X1)),
inference(cp,[status(thm)],[t37415,t38371]) ).
cnf(t115303,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(step,[status(thm)],[t35526,t35603]) ).
cnf(t35622,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t115303]) ).
cnf(t115540,plain,
rd(rd(X1,X1),rd(sFlat0,rd(X1,X1))) = ld(sFlat0,rd(X1,X1)),
inference(step,[status(thm)],[t38376,t35622]) ).
cnf(t115541,plain,
rd(rd(X1,X1),rd(sFlat0,rd(X1,X1))) = rd(X1,mult(sFlat0,X1)),
inference(step,[status(thm)],[t115540,t37415]) ).
cnf(t45528,plain,
rd(rd(X1,X1),rd(sFlat0,rd(X1,X1))) = rd(X1,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t115541]) ).
cnf(t116338,plain,
mult(sFlat0,rd(sFlat0,rd(sFlat0,rd(X1,X1)))) = rd(rd(X1,mult(sFlat0,X1)),rd(sFlat0,rd(X1,X1))),
inference(step,[status(thm)],[t113083,t45528]) ).
cnf(t2865,plain,
mult(rd(sFlat0,sFlat0),mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(cp,[status(thm)],[t2842,t9]) ).
cnf(t2900,plain,
mult(rd(sFlat0,sFlat0),mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(orient,[status(thm)],[t2865]) ).
cnf(t2909,plain,
rd(sFlat0,sFlat0) = rd(ld(sFlat0,X1),mult(sFlat0,X1)),
inference(cp,[status(thm)],[t11,t2900]) ).
cnf(t2935,plain,
rd(ld(sFlat0,X1),mult(sFlat0,X1)) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t2909]) ).
cnf(t114662,plain,
rd(ld(sFlat0,X1),mult(sFlat0,X1)) = sFlat0,
inference(step,[status(thm)],[t2935,t8270]) ).
cnf(t8275,plain,
rd(ld(sFlat0,X1),mult(sFlat0,X1)) = sFlat0,
inference(orient,[status(thm)],[t114662]) ).
cnf(t35552,plain,
sFlat0 = rd(ld(sFlat0,rd(X1,X1)),rd(sFlat0,ld(X1,X1))),
inference(cp,[status(thm)],[t8275,t35526]) ).
cnf(t115766,plain,
sFlat0 = rd(rd(X1,mult(sFlat0,X1)),rd(sFlat0,ld(X1,X1))),
inference(step,[status(thm)],[t35552,t37415]) ).
cnf(t115767,plain,
sFlat0 = rd(rd(X1,mult(sFlat0,X1)),rd(sFlat0,rd(X1,X1))),
inference(step,[status(thm)],[t115766,t35603]) ).
cnf(t58195,plain,
rd(rd(X1,mult(sFlat0,X1)),rd(sFlat0,rd(X1,X1))) = sFlat0,
inference(orient,[status(thm)],[t115767]) ).
cnf(t116339,plain,
mult(sFlat0,rd(sFlat0,rd(sFlat0,rd(X1,X1)))) = sFlat0,
inference(step,[status(thm)],[t116338,t58195]) ).
cnf(t113208,plain,
mult(sFlat0,rd(sFlat0,rd(sFlat0,rd(X1,X1)))) = sFlat0,
inference(orient,[status(thm)],[t116339]) ).
cnf(t113311,plain,
ld(rd(rd(sFlat0,rd(sFlat0,rd(X1,X1))),sFlat0),sFlat0) = ld(X2,rd(X2,rd(sFlat0,sFlat0))),
inference(cp,[status(thm)],[t30117,t113208]) ).
cnf(t116340,plain,
rd(ld(sFlat0,rd(sFlat0,rd(X1,X1))),sFlat0) = ld(X2,rd(X2,rd(sFlat0,sFlat0))),
inference(step,[status(thm)],[t113311,t14974]) ).
cnf(t12058,plain,
ld(sFlat0,ld(mult(X1,X2),X1)) = mult(sFlat0,rd(sFlat0,X2)),
inference(cp,[status(thm)],[t12057,t9]) ).
cnf(t13609,plain,
ld(sFlat0,ld(mult(X1,X2),X1)) = mult(sFlat0,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t12058]) ).
cnf(t13670,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(X3,rd(X3,mult(sFlat0,rd(sFlat0,X2)))),
inference(cp,[status(thm)],[t11881,t13609]) ).
cnf(t115004,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0),
inference(step,[status(thm)],[t13670,t13441]) ).
cnf(t21047,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0),
inference(orient,[status(thm)],[t115004]) ).
cnf(t21134,plain,
ld(mult(X1,X2),X1) = rd(sFlat0,ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0)),
inference(cp,[status(thm)],[t39,t21047]) ).
cnf(t11594,plain,
mult(X1,mult(sFlat0,X2)) = rd(X1,ld(ld(sFlat0,X2),sFlat0)),
inference(cp,[status(thm)],[t11546,t8275]) ).
cnf(t11974,plain,
rd(X1,ld(ld(sFlat0,X2),sFlat0)) = mult(X1,mult(sFlat0,X2)),
inference(orient,[status(thm)],[t11594]) ).
cnf(t115005,plain,
ld(mult(X1,X2),X1) = mult(sFlat0,mult(sFlat0,rd(sFlat0,X2))),
inference(step,[status(thm)],[t21134,t11974]) ).
cnf(t115006,plain,
ld(mult(X1,X2),X1) = ld(sFlat0,rd(sFlat0,X2)),
inference(step,[status(thm)],[t115005,t8314]) ).
cnf(t21138,plain,
ld(mult(X1,X2),X1) = ld(sFlat0,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t115006]) ).
cnf(t35547,plain,
ld(sFlat0,rd(sFlat0,rd(X1,X1))) = ld(rd(X2,ld(X1,X1)),X2),
inference(cp,[status(thm)],[t21138,t35526]) ).
cnf(t115361,plain,
ld(sFlat0,rd(sFlat0,rd(X1,X1))) = ld(X1,X1),
inference(step,[status(thm)],[t35547,t38]) ).
cnf(t115362,plain,
ld(sFlat0,rd(sFlat0,rd(X1,X1))) = rd(X1,X1),
inference(step,[status(thm)],[t115361,t35603]) ).
cnf(t35763,plain,
ld(sFlat0,rd(sFlat0,rd(X1,X1))) = rd(X1,X1),
inference(orient,[status(thm)],[t115362]) ).
cnf(t116341,plain,
rd(rd(X1,X1),sFlat0) = ld(X2,rd(X2,rd(sFlat0,sFlat0))),
inference(step,[status(thm)],[t116340,t35763]) ).
cnf(t110,plain,
mult(sFlat0,sFlat0) = ld(sFlat0,sFlat0),
inference(cp,[status(thm)],[t9,t108]) ).
cnf(t113,plain,
ld(sFlat0,sFlat0) = mult(sFlat0,sFlat0),
inference(orient,[status(thm)],[t110]) ).
cnf(t1116,plain,
mult(sFlat0,mult(ld(sFlat0,sFlat0),sFlat0)) = mult(mult(sFlat0,sFlat0),mult(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t1043,t113]) ).
cnf(t114498,plain,
mult(sFlat0,mult(mult(sFlat0,sFlat0),sFlat0)) = mult(mult(sFlat0,sFlat0),mult(sFlat0,sFlat0)),
inference(step,[status(thm)],[t1116,t113]) ).
cnf(t1182,plain,
mult(mult(sFlat0,sFlat0),mult(sFlat0,sFlat0)) = mult(sFlat0,mult(mult(sFlat0,sFlat0),sFlat0)),
inference(orient,[status(thm)],[t114498]) ).
cnf(t114501,plain,
mult(mult(sFlat0,sFlat0),mult(sFlat0,sFlat0)) = mult(sFlat0,sFlat0),
inference(step,[status(thm)],[t1182,t1323]) ).
cnf(t1324,plain,
mult(mult(sFlat0,sFlat0),mult(sFlat0,sFlat0)) = mult(sFlat0,sFlat0),
inference(orient,[status(thm)],[t114501]) ).
cnf(t114517,plain,
mult(rd(sFlat0,sFlat0),mult(sFlat0,sFlat0)) = mult(sFlat0,sFlat0),
inference(step,[status(thm)],[t1324,t1356]) ).
cnf(t114518,plain,
mult(rd(sFlat0,sFlat0),rd(sFlat0,sFlat0)) = mult(sFlat0,sFlat0),
inference(step,[status(thm)],[t114517,t1356]) ).
cnf(t114519,plain,
mult(rd(sFlat0,sFlat0),rd(sFlat0,sFlat0)) = rd(sFlat0,sFlat0),
inference(step,[status(thm)],[t114518,t1356]) ).
cnf(t1388,plain,
mult(rd(sFlat0,sFlat0),rd(sFlat0,sFlat0)) = rd(sFlat0,sFlat0),
inference(rw,[status(thm)],[t114519]) ).
cnf(t1745,plain,
mult(rd(sFlat0,sFlat0),rd(sFlat0,sFlat0)) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t1388]) ).
cnf(t1750,plain,
mult(mult(X1,rd(sFlat0,sFlat0)),rd(sFlat0,sFlat0)) = mult(rd(X1,rd(sFlat0,sFlat0)),mult(rd(sFlat0,sFlat0),rd(sFlat0,sFlat0))),
inference(cp,[status(thm)],[t1227,t1745]) ).
cnf(t114602,plain,
mult(mult(X1,rd(sFlat0,sFlat0)),rd(sFlat0,sFlat0)) = mult(rd(X1,rd(sFlat0,sFlat0)),rd(sFlat0,sFlat0)),
inference(step,[status(thm)],[t1750,t1745]) ).
cnf(t114603,plain,
mult(mult(X1,rd(sFlat0,sFlat0)),rd(sFlat0,sFlat0)) = X1,
inference(step,[status(thm)],[t114602,t8]) ).
cnf(t2660,plain,
mult(mult(X1,rd(sFlat0,sFlat0)),rd(sFlat0,sFlat0)) = X1,
inference(orient,[status(thm)],[t114603]) ).
cnf(t2663,plain,
rd(X1,rd(sFlat0,sFlat0)) = mult(X1,rd(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t2660,t8]) ).
cnf(t2673,plain,
mult(X1,rd(sFlat0,sFlat0)) = rd(X1,rd(sFlat0,sFlat0)),
inference(orient,[status(thm)],[t2663]) ).
cnf(t2679,plain,
rd(sFlat0,sFlat0) = ld(X1,rd(X1,rd(sFlat0,sFlat0))),
inference(cp,[status(thm)],[t9,t2673]) ).
cnf(t2695,plain,
ld(X1,rd(X1,rd(sFlat0,sFlat0))) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t2679]) ).
cnf(t116342,plain,
rd(rd(X1,X1),sFlat0) = rd(sFlat0,sFlat0),
inference(step,[status(thm)],[t116341,t2695]) ).
cnf(t116343,plain,
rd(rd(X1,X1),sFlat0) = sFlat0,
inference(step,[status(thm)],[t116342,t8270]) ).
cnf(t113316,plain,
rd(rd(X1,X1),sFlat0) = sFlat0,
inference(orient,[status(thm)],[t116343]) ).
cnf(t113375,plain,
rd(X1,X1) = rd(sFlat0,sFlat0),
inference(cp,[status(thm)],[t1424,t113316]) ).
cnf(t116346,plain,
rd(X1,X1) = sFlat0,
inference(step,[status(thm)],[t113375,t8270]) ).
cnf(t113528,plain,
rd(X1,X1) = sFlat0,
inference(orient,[status(thm)],[t116346]) ).
cnf(t113647,plain,
sFlat1 = ld(rd(mult(rd(sFlat0,sFlat1),sFlat1),x0),sFlat0),
inference(cp,[status(thm)],[t58588,t113528]) ).
cnf(t116590,plain,
sFlat1 = ld(rd(sFlat0,x0),sFlat0),
inference(step,[status(thm)],[t113647,t8]) ).
cnf(t116591,plain,
sFlat1 = x0,
inference(step,[status(thm)],[t116590,t38]) ).
cnf(t113800,plain,
x0 = sFlat1,
inference(orient,[status(thm)],[t116591]) ).
cnf(t116373,plain,
ld(X1,X1) = sFlat0,
inference(step,[status(thm)],[t35603,t113528]) ).
cnf(t113547,plain,
ld(X1,X1) = sFlat0,
inference(orient,[status(thm)],[t116373]) ).
cnf(t116592,plain,
rd(sFlat1,sFlat0) = sFlat1,
inference(step,[status(thm)],[t36,t113800]) ).
cnf(t113801,plain,
rd(sFlat1,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t116592]) ).
cnf(goal_0,negated_conjecture,
mult(x0,ld(x1,x1)) != x0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
rd(x0,ld(x1,x1)) != x0,
inference(rw,[status(thm)],[goal_0,t11664]) ).
cnf(g0_1,plain,
rd(sFlat1,ld(x1,x1)) != x0,
inference(rw,[status(thm)],[g0_0,t113800]) ).
cnf(g0_2,plain,
rd(sFlat1,sFlat0) != x0,
inference(rw,[status(thm)],[g0_1,t113547]) ).
cnf(g0_3,plain,
sFlat1 != x0,
inference(rw,[status(thm)],[g0_2,t113801]) ).
cnf(g0_4,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_3,t113800]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP655-13 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n016.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:35:41 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.66/6.17 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.66/6.17 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------