%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP654-10 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 : Sun Sep 27 07:30:41 AM UTC 2026
% Result : Unsatisfiable 142.06s 31.88s
% Output : CNFRefutation 142.06s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f01,axiom,
! [VAR_0,VAR_1] : mult(VAR_0,ld(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',f01) ).
cnf(c_1,plain,
mult(A,ld(A,B)) = B,
inference(clausify,[status(thm)],[f01]) ).
fof(f02,axiom,
! [VAR_0,VAR_1] : ld(VAR_0,mult(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',f02) ).
cnf(c_2,plain,
ld(A,mult(A,B)) = B,
inference(clausify,[status(thm)],[f02]) ).
fof(f03,axiom,
! [VAR_0,VAR_1] : mult(rd(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',f03) ).
cnf(c_3,plain,
mult(rd(A,B),B) = A,
inference(clausify,[status(thm)],[f03]) ).
fof(f04,axiom,
! [VAR_0,VAR_1] : rd(mult(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',f04) ).
cnf(c_4,plain,
rd(mult(A,B),B) = A,
inference(clausify,[status(thm)],[f04]) ).
fof(f05,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(VAR_0,mult(VAR_1,mult(VAR_0,VAR_2))) = mult(mult(mult(VAR_0,VAR_1),VAR_0),VAR_2),
file('theBenchmark.p',f05) ).
cnf(c_5,plain,
mult(A,mult(B,mult(A,C))) = mult(mult(mult(A,B),A),C),
inference(clausify,[status(thm)],[f05]) ).
cnf(c_6,plain,
mult(mult(mult(A,B),A),C) = mult(A,mult(B,mult(A,C))),
inference(copy,[status(thm)],[c_5]) ).
fof(goal,axiom,
! [VAR_0] : tuple(mult(VAR_0,x1(VAR_0)),mult(x1_2(VAR_0),VAR_0)) != tuple(x1(VAR_0),x1_2(VAR_0)),
file('theBenchmark.p',goal) ).
cnf(c_7,plain,
tuple(mult(A,x1(A)),mult(x1_2(A),A)) != tuple(x1(A),x1_2(A)),
inference(clausify,[status(thm)],[goal]) ).
cnf(c_8,plain,
ld(rd(A,B),A) = B,
inference(paramod,[status(thm)],[c_3,c_2]) ).
cnf(c_9,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_10,plain,
mult(A,mult(B,mult(A,ld(mult(mult(A,B),A),C)))) = C,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_11547,plain,
mult(mult(A,B),C) = mult(B,mult(ld(B,A),mult(B,C))),
inference(paramod,[status(thm)],[c_1,c_6]) ).
cnf(c_11,plain,
mult(A,mult(ld(A,B),mult(A,C))) = mult(mult(B,A),C),
inference(copy,[status(thm)],[c_11547]) ).
cnf(c_12,plain,
ld(mult(mult(A,B),A),mult(A,mult(B,mult(A,C)))) = C,
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_13,plain,
mult(mult(A,rd(A,B)),C) = mult(rd(A,B),mult(B,mult(rd(A,B),C))),
inference(paramod,[status(thm)],[c_3,c_6]) ).
cnf(c_14,plain,
rd(mult(A,mult(B,mult(A,C))),C) = mult(mult(A,B),A),
inference(paramod,[status(thm)],[c_6,c_4]) ).
cnf(c_15,plain,
mult(mult(A,mult(B,mult(A,mult(A,B)))),C) = mult(mult(A,B),mult(A,mult(mult(A,B),C))),
inference(paramod,[status(thm)],[c_6,c_6]) ).
cnf(c_11548,plain,
mult(A,mult(ld(A,B),C)) = mult(mult(B,A),ld(A,C)),
inference(paramod,[status(thm)],[c_1,c_11]) ).
cnf(c_16,plain,
mult(mult(A,B),ld(B,C)) = mult(B,mult(ld(B,A),C)),
inference(copy,[status(thm)],[c_11548]) ).
cnf(c_17,plain,
ld(A,mult(mult(B,A),C)) = mult(ld(A,B),mult(A,C)),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_11549,plain,
mult(A,ld(ld(B,A),C)) = mult(ld(B,A),mult(ld(ld(B,A),B),C)),
inference(paramod,[status(thm)],[c_1,c_16]) ).
cnf(c_22,plain,
mult(ld(A,B),mult(ld(ld(A,B),A),C)) = mult(B,ld(ld(A,B),C)),
inference(copy,[status(thm)],[c_11549]) ).
cnf(c_23,plain,
mult(mult(A,B),ld(B,ld(ld(B,A),C))) = mult(B,C),
inference(paramod,[status(thm)],[c_1,c_16]) ).
cnf(c_24,plain,
ld(mult(A,B),mult(B,mult(ld(B,A),C))) = ld(B,C),
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_11550,plain,
mult(A,ld(B,C)) = mult(B,mult(ld(B,rd(A,B)),C)),
inference(paramod,[status(thm)],[c_3,c_16]) ).
cnf(c_25,plain,
mult(A,mult(ld(A,rd(B,A)),C)) = mult(B,ld(A,C)),
inference(copy,[status(thm)],[c_11550]) ).
cnf(c_27,plain,
rd(mult(mult(A,B),ld(B,C)),mult(ld(B,A),C)) = B,
inference(paramod,[status(thm)],[c_16,c_4]) ).
cnf(c_11551,plain,
mult(mult(A,B),mult(ld(mult(A,B),C),mult(B,mult(ld(B,A),D)))) = mult(mult(C,mult(A,B)),ld(B,D)),
inference(paramod,[status(thm)],[c_16,c_11]) ).
cnf(c_35,plain,
mult(mult(A,mult(B,C)),ld(C,D)) = mult(mult(B,C),mult(ld(mult(B,C),A),mult(C,mult(ld(C,B),D)))),
inference(copy,[status(thm)],[c_11551]) ).
cnf(c_41,plain,
mult(mult(mult(A,B),ld(B,C)),ld(mult(ld(B,A),C),D)) = mult(mult(ld(B,A),C),mult(ld(mult(ld(B,A),C),B),D)),
inference(paramod,[status(thm)],[c_16,c_16]) ).
cnf(c_44,plain,
rd(mult(A,ld(B,C)),mult(ld(B,rd(A,B)),C)) = B,
inference(paramod,[status(thm)],[c_3,c_27]) ).
cnf(c_51,plain,
rd(A,mult(ld(B,rd(B,B)),A)) = B,
inference(paramod,[status(thm)],[c_1,c_44]) ).
cnf(c_11552,plain,
ld(A,mult(B,ld(A,C))) = mult(ld(A,rd(B,A)),C),
inference(paramod,[status(thm)],[c_44,c_8]) ).
cnf(c_56,plain,
mult(ld(A,rd(B,A)),C) = ld(A,mult(B,ld(A,C))),
inference(copy,[status(thm)],[c_11552]) ).
cnf(c_62,plain,
mult(ld(A,rd(A,A)),B) = ld(A,B),
inference(paramod,[status(thm)],[c_1,c_56]) ).
cnf(c_64,plain,
mult(ld(A,rd(B,A)),mult(A,C)) = ld(A,mult(B,C)),
inference(paramod,[status(thm)],[c_2,c_56]) ).
cnf(c_66,plain,
rd(ld(A,mult(B,ld(A,C))),C) = ld(A,rd(B,A)),
inference(paramod,[status(thm)],[c_56,c_4]) ).
cnf(c_92,plain,
mult(A,mult(ld(A,rd(A,A)),B)) = B,
inference(paramod,[status(thm)],[c_62,c_1]) ).
cnf(c_94,plain,
mult(ld(A,rd(A,A)),mult(A,B)) = B,
inference(paramod,[status(thm)],[c_62,c_2]) ).
cnf(c_95,plain,
rd(ld(A,B),B) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_62,c_4]) ).
cnf(c_96,plain,
mult(mult(ld(A,B),ld(A,rd(A,A))),C) = mult(ld(A,rd(A,A)),mult(B,mult(ld(A,rd(A,A)),C))),
inference(paramod,[status(thm)],[c_62,c_6]) ).
cnf(c_11553,plain,
ld(A,B) = mult(C,mult(A,ld(mult(mult(A,C),A),B))),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_119,plain,
mult(A,mult(B,ld(mult(mult(B,A),B),C))) = ld(B,C),
inference(copy,[status(thm)],[c_11553]) ).
cnf(c_130,plain,
mult(A,ld(B,mult(A,ld(mult(mult(A,ld(B,rd(B,B))),A),C)))) = C,
inference(paramod,[status(thm)],[c_62,c_10]) ).
cnf(c_131,plain,
ld(mult(mult(A,B),A),mult(A,mult(B,C))) = ld(A,C),
inference(paramod,[status(thm)],[c_1,c_12]) ).
cnf(c_147,plain,
ld(mult(mult(A,ld(B,rd(B,B))),A),mult(A,ld(B,mult(A,C)))) = C,
inference(paramod,[status(thm)],[c_62,c_12]) ).
cnf(c_170,plain,
rd(A,mult(B,A)) = ld(B,rd(B,B)),
inference(paramod,[status(thm)],[c_2,c_95]) ).
cnf(c_11554,plain,
mult(A,rd(B,mult(A,B))) = rd(A,A),
inference(paramod,[status(thm)],[c_170,c_1]) ).
cnf(c_174,plain,
rd(A,A) = mult(A,rd(B,mult(A,B))),
inference(copy,[status(thm)],[c_11554]) ).
cnf(c_176,plain,
ld(ld(A,rd(A,A)),B) = mult(A,B),
inference(paramod,[status(thm)],[c_170,c_8]) ).
cnf(c_177,plain,
rd(rd(A,A),rd(B,mult(A,B))) = A,
inference(paramod,[status(thm)],[c_170,c_9]) ).
cnf(c_11555,plain,
mult(rd(A,mult(B,A)),C) = ld(B,mult(B,ld(B,C))),
inference(paramod,[status(thm)],[c_170,c_56]) ).
cnf(c_189,plain,
mult(rd(A,mult(B,A)),C) = ld(B,C),
inference(paramod,[status(thm)],[c_1,c_11555]) ).
cnf(c_11556,plain,
mult(ld(A,rd(A,A)),rd(A,A)) = rd(B,mult(A,B)),
inference(paramod,[status(thm)],[c_170,c_62]) ).
cnf(c_192,plain,
rd(A,mult(B,A)) = mult(ld(B,rd(B,B)),rd(B,B)),
inference(copy,[status(thm)],[c_11556]) ).
cnf(c_215,plain,
rd(A,mult(B,A)) = rd(C,mult(B,C)),
inference(paramod,[status(thm)],[c_170,c_170]) ).
cnf(c_11557,plain,
rd(A,B) = rd(C,mult(rd(B,A),C)),
inference(paramod,[status(thm)],[c_3,c_215]) ).
cnf(c_219,plain,
rd(A,mult(rd(B,C),A)) = rd(C,B),
inference(copy,[status(thm)],[c_11557]) ).
cnf(c_221,plain,
ld(rd(A,mult(B,A)),C) = mult(B,C),
inference(paramod,[status(thm)],[c_215,c_8]) ).
cnf(c_226,plain,
mult(mult(A,rd(B,mult(A,B))),A) = A,
inference(paramod,[status(thm)],[c_174,c_3]) ).
cnf(c_227,plain,
rd(rd(A,B),rd(A,B)) = mult(rd(A,B),rd(B,A)),
inference(paramod,[status(thm)],[c_3,c_174]) ).
cnf(c_11558,plain,
rd(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,rd(B,mult(ld(A,rd(A,A)),B))),
inference(paramod,[status(thm)],[c_174,c_62]) ).
cnf(c_240,plain,
rd(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,A),
inference(paramod,[status(thm)],[c_51,c_11558]) ).
cnf(c_242,plain,
mult(rd(A,B),C) = ld(rd(B,A),C),
inference(paramod,[status(thm)],[c_3,c_189]) ).
cnf(c_249,plain,
mult(rd(A,mult(rd(B,C),A)),B) = C,
inference(paramod,[status(thm)],[c_189,c_8]) ).
cnf(c_292,plain,
rd(A,mult(B,A)) = mult(rd(C,mult(B,C)),rd(B,B)),
inference(paramod,[status(thm)],[c_189,c_170]) ).
cnf(c_294,plain,
mult(rd(A,B),mult(rd(B,A),C)) = C,
inference(paramod,[status(thm)],[c_242,c_1]) ).
cnf(c_344,plain,
rd(mult(A,B),C) = mult(mult(A,rd(B,mult(A,C))),A),
inference(paramod,[status(thm)],[c_3,c_14]) ).
cnf(c_11559,plain,
rd(mult(ld(A,B),mult(A,mult(ld(A,B),C))),C) = mult(A,mult(ld(A,ld(A,B)),B)),
inference(paramod,[status(thm)],[c_16,c_14]) ).
cnf(c_11560,plain,
mult(mult(ld(A,B),rd(mult(A,mult(ld(A,B),C)),mult(ld(A,B),C))),ld(A,B)) = mult(A,mult(ld(A,ld(A,B)),B)),
inference(paramod,[status(thm)],[c_344,c_11559]) ).
cnf(c_11561,plain,
mult(mult(ld(A,B),A),ld(A,B)) = mult(A,mult(ld(A,ld(A,B)),B)),
inference(paramod,[status(thm)],[c_4,c_11560]) ).
cnf(c_345,plain,
mult(A,mult(ld(A,ld(A,B)),B)) = mult(mult(ld(A,B),A),ld(A,B)),
inference(copy,[status(thm)],[c_11561]) ).
cnf(c_460,plain,
rd(A,mult(rd(B,B),A)) = mult(B,rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_219,c_174]) ).
cnf(c_484,plain,
ld(mult(ld(A,rd(A,A)),rd(A,A)),B) = mult(A,B),
inference(paramod,[status(thm)],[c_192,c_8]) ).
cnf(c_11562,plain,
mult(rd(A,A),mult(ld(rd(A,A),ld(A,rd(A,A))),mult(rd(A,A),B))) = mult(rd(C,mult(A,C)),B),
inference(paramod,[status(thm)],[c_192,c_11]) ).
cnf(c_11563,plain,
mult(rd(A,A),mult(mult(rd(A,A),ld(A,rd(A,A))),mult(rd(A,A),B))) = mult(rd(C,mult(A,C)),B),
inference(paramod,[status(thm)],[c_242,c_11562]) ).
cnf(c_486,plain,
mult(rd(A,mult(B,A)),C) = mult(rd(B,B),mult(mult(rd(B,B),ld(B,rd(B,B))),mult(rd(B,B),C))),
inference(copy,[status(thm)],[c_11563]) ).
cnf(c_501,plain,
rd(A,mult(B,A)) = mult(ld(B,rd(B,B)),rd(C,mult(rd(B,B),C))),
inference(paramod,[status(thm)],[c_219,c_192]) ).
cnf(c_502,plain,
mult(ld(A,A),ld(A,rd(A,A))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_240,c_3]) ).
cnf(c_505,plain,
rd(ld(A,rd(A,A)),mult(ld(A,rd(A,A)),rd(A,A))) = ld(A,A),
inference(paramod,[status(thm)],[c_62,c_240]) ).
cnf(c_11564,plain,
mult(ld(A,A),B) = ld(rd(ld(A,rd(A,A)),ld(A,rd(A,A))),B),
inference(paramod,[status(thm)],[c_240,c_242]) ).
cnf(c_11565,plain,
mult(ld(A,A),B) = ld(ld(A,A),B),
inference(paramod,[status(thm)],[c_240,c_11564]) ).
cnf(c_510,plain,
ld(ld(A,A),B) = mult(ld(A,A),B),
inference(copy,[status(thm)],[c_11565]) ).
cnf(c_11566,plain,
mult(mult(ld(A,rd(A,A)),ld(A,A)),B) = mult(rd(ld(A,rd(A,A)),ld(A,rd(A,A))),mult(ld(A,rd(A,A)),mult(rd(ld(A,rd(A,A)),ld(A,rd(A,A))),B))),
inference(paramod,[status(thm)],[c_240,c_13]) ).
cnf(c_11567,plain,
mult(mult(ld(A,rd(A,A)),ld(A,A)),B) = mult(ld(A,A),mult(ld(A,rd(A,A)),mult(rd(ld(A,rd(A,A)),ld(A,rd(A,A))),B))),
inference(paramod,[status(thm)],[c_240,c_11566]) ).
cnf(c_511,plain,
mult(mult(ld(A,rd(A,A)),ld(A,A)),B) = mult(ld(A,A),mult(ld(A,rd(A,A)),mult(ld(A,A),B))),
inference(paramod,[status(thm)],[c_240,c_11567]) ).
cnf(c_11568,plain,
rd(A,mult(ld(B,B),A)) = rd(ld(B,rd(B,B)),ld(B,rd(B,B))),
inference(paramod,[status(thm)],[c_240,c_219]) ).
cnf(c_513,plain,
rd(A,mult(ld(B,B),A)) = ld(B,B),
inference(paramod,[status(thm)],[c_240,c_11568]) ).
cnf(c_514,plain,
mult(ld(A,A),mult(ld(A,A),B)) = B,
inference(paramod,[status(thm)],[c_510,c_1]) ).
cnf(c_11569,plain,
mult(ld(A,A),mult(mult(ld(A,A),B),mult(ld(A,A),C))) = mult(mult(B,ld(A,A)),C),
inference(paramod,[status(thm)],[c_510,c_11]) ).
cnf(c_515,plain,
mult(mult(A,ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),A),mult(ld(B,B),C))),
inference(copy,[status(thm)],[c_11569]) ).
cnf(c_11570,plain,
mult(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(ld(ld(B,B),A),C)),
inference(paramod,[status(thm)],[c_510,c_16]) ).
cnf(c_516,plain,
mult(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(mult(ld(B,B),A),C)),
inference(paramod,[status(thm)],[c_510,c_11570]) ).
cnf(c_11571,plain,
rd(mult(ld(A,A),B),B) = ld(ld(A,A),rd(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_510,c_95]) ).
cnf(c_11572,plain,
mult(mult(ld(A,A),rd(B,mult(ld(A,A),B))),ld(A,A)) = ld(ld(A,A),rd(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_344,c_11571]) ).
cnf(c_11573,plain,
mult(mult(ld(A,A),ld(A,A)),ld(A,A)) = ld(ld(A,A),rd(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_513,c_11572]) ).
cnf(c_11574,plain,
mult(mult(ld(A,A),ld(A,A)),ld(A,A)) = mult(ld(A,A),rd(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_510,c_11573]) ).
cnf(c_520,plain,
mult(ld(A,A),rd(ld(A,A),ld(A,A))) = mult(mult(ld(A,A),ld(A,A)),ld(A,A)),
inference(copy,[status(thm)],[c_11574]) ).
cnf(c_11575,plain,
rd(A,mult(ld(B,B),A)) = mult(ld(B,B),rd(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_510,c_170]) ).
cnf(c_11576,plain,
ld(B,B) = mult(ld(B,B),rd(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_513,c_11575]) ).
cnf(c_11577,plain,
ld(B,B) = mult(mult(ld(B,B),ld(B,B)),ld(B,B)),
inference(paramod,[status(thm)],[c_520,c_11576]) ).
cnf(c_521,plain,
mult(mult(ld(A,A),ld(A,A)),ld(A,A)) = ld(A,A),
inference(copy,[status(thm)],[c_11577]) ).
cnf(c_11578,plain,
ld(ld(A,A),rd(B,mult(ld(A,A),B))) = rd(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_174,c_510]) ).
cnf(c_11579,plain,
ld(ld(A,A),ld(A,A)) = rd(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_513,c_11578]) ).
cnf(c_11580,plain,
mult(ld(A,A),ld(A,A)) = rd(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_510,c_11579]) ).
cnf(c_522,plain,
rd(ld(A,A),ld(A,A)) = mult(ld(A,A),ld(A,A)),
inference(copy,[status(thm)],[c_11580]) ).
cnf(c_523,plain,
ld(mult(rd(A,mult(B,A)),B),C) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_189,c_510]) ).
cnf(c_11581,plain,
ld(A,B) = mult(ld(A,C),mult(A,ld(mult(C,A),B))),
inference(paramod,[status(thm)],[c_1,c_17]) ).
cnf(c_547,plain,
mult(ld(A,B),mult(A,ld(mult(B,A),C))) = ld(A,C),
inference(copy,[status(thm)],[c_11581]) ).
cnf(c_11582,plain,
mult(ld(ld(A,A),B),mult(ld(A,A),C)) = mult(ld(A,A),mult(mult(B,ld(A,A)),C)),
inference(paramod,[status(thm)],[c_17,c_510]) ).
cnf(c_575,plain,
mult(mult(ld(A,A),B),mult(ld(A,A),C)) = mult(ld(A,A),mult(mult(B,ld(A,A)),C)),
inference(paramod,[status(thm)],[c_510,c_11582]) ).
cnf(c_11583,plain,
ld(rd(A,A),mult(rd(B,mult(A,B)),C)) = mult(ld(rd(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
inference(paramod,[status(thm)],[c_292,c_17]) ).
cnf(c_11584,plain,
mult(rd(A,A),mult(rd(B,mult(A,B)),C)) = mult(ld(rd(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
inference(paramod,[status(thm)],[c_242,c_11583]) ).
cnf(c_724,plain,
mult(rd(A,A),mult(rd(B,mult(A,B)),C)) = mult(mult(rd(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
inference(paramod,[status(thm)],[c_242,c_11584]) ).
cnf(c_908,plain,
mult(ld(A,A),rd(B,mult(A,B))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_170,c_502]) ).
cnf(c_11585,plain,
mult(mult(rd(A,B),rd(B,A)),ld(rd(B,A),rd(rd(B,A),rd(B,A)))) = ld(rd(B,A),rd(rd(B,A),rd(B,A))),
inference(paramod,[status(thm)],[c_242,c_502]) ).
cnf(c_11586,plain,
mult(mult(rd(A,B),rd(B,A)),ld(rd(B,A),mult(rd(B,A),rd(A,B)))) = ld(rd(B,A),rd(rd(B,A),rd(B,A))),
inference(paramod,[status(thm)],[c_227,c_11585]) ).
cnf(c_11587,plain,
mult(mult(rd(A,B),rd(B,A)),rd(A,B)) = ld(rd(B,A),rd(rd(B,A),rd(B,A))),
inference(paramod,[status(thm)],[c_2,c_11586]) ).
cnf(c_11588,plain,
mult(mult(rd(A,B),rd(B,A)),rd(A,B)) = ld(rd(B,A),mult(rd(B,A),rd(A,B))),
inference(paramod,[status(thm)],[c_227,c_11587]) ).
cnf(c_911,plain,
mult(mult(rd(A,B),rd(B,A)),rd(A,B)) = rd(A,B),
inference(paramod,[status(thm)],[c_2,c_11588]) ).
cnf(c_924,plain,
mult(ld(A,rd(A,A)),rd(A,A)) = mult(ld(A,A),rd(B,mult(A,B))),
inference(paramod,[status(thm)],[c_908,c_62]) ).
cnf(c_944,plain,
mult(rd(A,mult(B,A)),rd(B,B)) = mult(ld(B,B),rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_908,c_189]) ).
cnf(c_974,plain,
mult(ld(A,A),rd(B,mult(A,B))) = mult(ld(A,A),rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_908,c_908]) ).
cnf(c_11589,plain,
mult(rd(A,A),ld(ld(A,rd(A,A)),B)) = ld(A,mult(ld(ld(A,rd(A,A)),A),B)),
inference(paramod,[status(thm)],[c_22,c_62]) ).
cnf(c_11590,plain,
mult(rd(A,A),mult(A,B)) = ld(A,mult(ld(ld(A,rd(A,A)),A),B)),
inference(paramod,[status(thm)],[c_176,c_11589]) ).
cnf(c_11591,plain,
mult(rd(A,A),mult(A,B)) = ld(A,mult(mult(A,A),B)),
inference(paramod,[status(thm)],[c_176,c_11590]) ).
cnf(c_1090,plain,
mult(rd(A,A),mult(A,B)) = mult(ld(A,A),mult(A,B)),
inference(paramod,[status(thm)],[c_17,c_11591]) ).
cnf(c_11592,plain,
mult(mult(ld(A,A),B),mult(ld(ld(ld(A,A),B),ld(A,A)),C)) = mult(B,ld(ld(ld(A,A),B),C)),
inference(paramod,[status(thm)],[c_510,c_22]) ).
cnf(c_11593,plain,
mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),ld(A,A)),C)) = mult(B,ld(ld(ld(A,A),B),C)),
inference(paramod,[status(thm)],[c_510,c_11592]) ).
cnf(c_1111,plain,
mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),ld(A,A)),C)) = mult(B,ld(mult(ld(A,A),B),C)),
inference(paramod,[status(thm)],[c_510,c_11593]) ).
cnf(c_11594,plain,
mult(ld(A,A),mult(mult(B,ld(A,A)),ld(ld(A,A),C))) = mult(ld(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_16,c_514]) ).
cnf(c_11595,plain,
mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))) = mult(ld(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_510,c_11594]) ).
cnf(c_11596,plain,
mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))) = mult(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_510,c_11595]) ).
cnf(c_1245,plain,
mult(mult(ld(A,A),B),C) = mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))),
inference(copy,[status(thm)],[c_11596]) ).
cnf(c_1253,plain,
mult(mult(ld(A,A),mult(B,B)),C) = mult(mult(ld(A,A),B),mult(ld(A,A),mult(mult(ld(A,A),B),C))),
inference(paramod,[status(thm)],[c_514,c_15]) ).
cnf(c_11597,plain,
ld(mult(ld(A,A),B),mult(B,C)) = mult(ld(mult(ld(A,A),B),ld(A,A)),mult(mult(ld(A,A),B),C)),
inference(paramod,[status(thm)],[c_514,c_17]) ).
cnf(c_1254,plain,
mult(ld(mult(ld(A,A),B),ld(A,A)),mult(mult(ld(A,A),B),C)) = ld(mult(ld(A,A),B),mult(B,C)),
inference(copy,[status(thm)],[c_11597]) ).
cnf(c_11598,plain,
ld(mult(A,B),mult(B,C)) = ld(B,ld(ld(B,A),C)),
inference(paramod,[status(thm)],[c_23,c_2]) ).
cnf(c_1258,plain,
ld(A,ld(ld(A,B),C)) = ld(mult(B,A),mult(A,C)),
inference(copy,[status(thm)],[c_11598]) ).
cnf(c_11599,plain,
mult(mult(A,ld(B,B)),ld(ld(B,B),ld(mult(ld(B,B),A),C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_510,c_23]) ).
cnf(c_1278,plain,
mult(mult(A,ld(B,B)),mult(ld(B,B),ld(mult(ld(B,B),A),C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_510,c_11599]) ).
cnf(c_11600,plain,
ld(rd(A,mult(B,A)),mult(rd(B,B),mult(ld(rd(B,B),rd(C,mult(B,C))),D))) = ld(rd(B,B),D),
inference(paramod,[status(thm)],[c_292,c_24]) ).
cnf(c_11601,plain,
ld(rd(A,mult(B,A)),mult(rd(B,B),mult(mult(rd(B,B),rd(C,mult(B,C))),D))) = ld(rd(B,B),D),
inference(paramod,[status(thm)],[c_242,c_11600]) ).
cnf(c_11602,plain,
mult(B,mult(rd(B,B),mult(mult(rd(B,B),rd(C,mult(B,C))),D))) = ld(rd(B,B),D),
inference(paramod,[status(thm)],[c_221,c_11601]) ).
cnf(c_1323,plain,
mult(A,mult(rd(A,A),mult(mult(rd(A,A),rd(B,mult(A,B))),C))) = mult(rd(A,A),C),
inference(paramod,[status(thm)],[c_242,c_11602]) ).
cnf(c_1339,plain,
ld(mult(A,A),mult(A,B)) = ld(A,mult(ld(A,A),B)),
inference(paramod,[status(thm)],[c_514,c_24]) ).
cnf(c_1394,plain,
ld(mult(A,A),B) = ld(A,mult(ld(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_1,c_1339]) ).
cnf(c_1405,plain,
mult(rd(A,mult(mult(B,B),A)),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_1339,c_189]) ).
cnf(c_11603,plain,
ld(mult(A,A),mult(A,mult(ld(A,A),rd(B,mult(A,B))))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_974,c_24]) ).
cnf(c_11604,plain,
ld(A,mult(ld(A,A),ld(A,mult(A,mult(ld(A,A),rd(B,mult(A,B))))))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_1394,c_11603]) ).
cnf(c_11605,plain,
ld(A,mult(ld(A,A),mult(ld(A,A),rd(B,mult(A,B))))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_2,c_11604]) ).
cnf(c_1528,plain,
ld(A,rd(B,mult(A,B))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_514,c_11605]) ).
cnf(c_11606,plain,
mult(A,mult(ld(A,rd(B,A)),C)) = mult(B,mult(ld(A,rd(A,A)),C)),
inference(paramod,[status(thm)],[c_62,c_25]) ).
cnf(c_1548,plain,
mult(A,mult(ld(B,rd(B,B)),C)) = mult(B,mult(ld(B,rd(A,B)),C)),
inference(copy,[status(thm)],[c_11606]) ).
cnf(c_1753,plain,
mult(ld(A,rd(A,A)),rd(B,mult(A,B))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_1528,c_62]) ).
cnf(c_11607,plain,
mult(ld(A,rd(A,A)),rd(ld(A,B),B)) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_1,c_1753]) ).
cnf(c_1769,plain,
mult(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,rd(B,mult(A,B))),
inference(paramod,[status(thm)],[c_95,c_11607]) ).
cnf(c_11608,plain,
ld(rd(A,mult(B,A)),mult(ld(B,rd(C,mult(B,C))),D)) = mult(ld(rd(A,mult(B,A)),ld(B,rd(B,B))),mult(rd(A,mult(B,A)),D)),
inference(paramod,[status(thm)],[c_1753,c_17]) ).
cnf(c_11609,plain,
mult(B,mult(ld(B,rd(C,mult(B,C))),D)) = mult(ld(rd(A,mult(B,A)),ld(B,rd(B,B))),mult(rd(A,mult(B,A)),D)),
inference(paramod,[status(thm)],[c_221,c_11608]) ).
cnf(c_11610,plain,
mult(B,mult(ld(B,rd(C,mult(B,C))),D)) = mult(mult(B,ld(B,rd(B,B))),mult(rd(A,mult(B,A)),D)),
inference(paramod,[status(thm)],[c_221,c_11609]) ).
cnf(c_11611,plain,
mult(B,mult(ld(B,rd(C,mult(B,C))),D)) = mult(rd(B,B),mult(rd(A,mult(B,A)),D)),
inference(paramod,[status(thm)],[c_1,c_11610]) ).
cnf(c_1793,plain,
mult(rd(A,A),mult(rd(B,mult(A,B)),C)) = mult(A,mult(ld(A,rd(D,mult(A,D))),C)),
inference(copy,[status(thm)],[c_11611]) ).
cnf(c_11612,plain,
mult(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,rd(ld(A,B),B)),
inference(paramod,[status(thm)],[c_1,c_1769]) ).
cnf(c_11613,plain,
mult(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_95,c_11612]) ).
cnf(c_1864,plain,
ld(A,ld(A,rd(A,A))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
inference(copy,[status(thm)],[c_11613]) ).
cnf(c_11614,plain,
ld(ld(A,rd(A,A)),mult(ld(A,rd(B,mult(A,B))),C)) = mult(ld(ld(A,rd(A,A)),ld(A,rd(A,A))),mult(ld(A,rd(A,A)),C)),
inference(paramod,[status(thm)],[c_1769,c_17]) ).
cnf(c_11615,plain,
mult(A,mult(ld(A,rd(B,mult(A,B))),C)) = mult(ld(ld(A,rd(A,A)),ld(A,rd(A,A))),mult(ld(A,rd(A,A)),C)),
inference(paramod,[status(thm)],[c_176,c_11614]) ).
cnf(c_11616,plain,
mult(A,mult(ld(A,rd(B,mult(A,B))),C)) = mult(mult(A,ld(A,rd(A,A))),mult(ld(A,rd(A,A)),C)),
inference(paramod,[status(thm)],[c_176,c_11615]) ).
cnf(c_11617,plain,
mult(A,mult(ld(A,rd(B,mult(A,B))),C)) = mult(rd(A,A),mult(ld(A,rd(A,A)),C)),
inference(paramod,[status(thm)],[c_1,c_11616]) ).
cnf(c_1881,plain,
mult(rd(A,A),mult(ld(A,rd(A,A)),B)) = mult(A,mult(ld(A,rd(C,mult(A,C))),B)),
inference(copy,[status(thm)],[c_11617]) ).
cnf(c_11618,plain,
ld(mult(rd(A,mult(B,A)),B),mult(B,mult(mult(ld(B,rd(B,B)),ld(B,rd(B,B))),C))) = ld(B,C),
inference(paramod,[status(thm)],[c_1769,c_24]) ).
cnf(c_11619,plain,
ld(mult(rd(A,mult(B,A)),B),mult(B,mult(ld(B,rd(B,B)),mult(rd(B,B),mult(ld(B,rd(B,B)),C))))) = ld(B,C),
inference(paramod,[status(thm)],[c_96,c_11618]) ).
cnf(c_11620,plain,
ld(mult(rd(A,mult(B,A)),B),mult(rd(B,B),mult(ld(B,rd(B,B)),C))) = ld(B,C),
inference(paramod,[status(thm)],[c_92,c_11619]) ).
cnf(c_1891,plain,
mult(ld(A,A),mult(rd(A,A),mult(ld(A,rd(A,A)),B))) = ld(A,B),
inference(paramod,[status(thm)],[c_523,c_11620]) ).
cnf(c_11621,plain,
mult(ld(A,rd(A,A)),mult(B,C)) = mult(ld(A,rd(B,A)),mult(A,C)),
inference(paramod,[status(thm)],[c_64,c_62]) ).
cnf(c_1946,plain,
mult(ld(A,rd(B,A)),mult(A,C)) = mult(ld(A,rd(A,A)),mult(B,C)),
inference(copy,[status(thm)],[c_11621]) ).
cnf(c_11622,plain,
ld(mult(A,A),B) = mult(ld(A,rd(ld(A,A),A)),mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_64,c_1394]) ).
cnf(c_11623,plain,
ld(A,mult(ld(A,A),ld(A,B))) = mult(ld(A,rd(ld(A,A),A)),mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_1394,c_11622]) ).
cnf(c_11624,plain,
ld(A,mult(ld(A,A),ld(A,B))) = mult(ld(A,ld(A,rd(A,A))),mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_95,c_11623]) ).
cnf(c_11625,plain,
ld(A,mult(ld(A,A),ld(A,B))) = mult(mult(ld(A,rd(A,A)),ld(A,rd(A,A))),mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_1864,c_11624]) ).
cnf(c_11626,plain,
ld(A,mult(ld(A,A),ld(A,B))) = mult(mult(ld(A,rd(A,A)),ld(A,rd(A,A))),B),
inference(paramod,[status(thm)],[c_1,c_11625]) ).
cnf(c_11627,plain,
ld(A,mult(ld(A,A),ld(A,B))) = mult(ld(A,rd(A,A)),mult(rd(A,A),mult(ld(A,rd(A,A)),B))),
inference(paramod,[status(thm)],[c_96,c_11626]) ).
cnf(c_2032,plain,
mult(ld(A,rd(A,A)),mult(rd(A,A),mult(ld(A,rd(A,A)),B))) = ld(A,mult(ld(A,A),ld(A,B))),
inference(copy,[status(thm)],[c_11627]) ).
cnf(c_2220,plain,
rd(ld(A,mult(B,C)),mult(A,C)) = ld(A,rd(B,A)),
inference(paramod,[status(thm)],[c_2,c_66]) ).
cnf(c_11628,plain,
rd(ld(mult(A,B),mult(B,ld(mult(A,B),C))),C) = ld(mult(A,B),rd(D,mult(A,D))),
inference(paramod,[status(thm)],[c_215,c_66]) ).
cnf(c_11629,plain,
ld(mult(A,B),rd(B,mult(A,B))) = ld(mult(A,B),rd(D,mult(A,D))),
inference(paramod,[status(thm)],[c_66,c_11628]) ).
cnf(c_2229,plain,
ld(mult(A,B),rd(C,mult(A,C))) = ld(mult(A,B),rd(B,mult(A,B))),
inference(copy,[status(thm)],[c_11629]) ).
cnf(c_11630,plain,
rd(ld(A,ld(A,rd(A,A))),rd(A,A)) = ld(A,rd(ld(A,A),A)),
inference(paramod,[status(thm)],[c_502,c_66]) ).
cnf(c_11631,plain,
rd(mult(ld(A,rd(A,A)),ld(A,rd(A,A))),rd(A,A)) = ld(A,rd(ld(A,A),A)),
inference(paramod,[status(thm)],[c_1864,c_11630]) ).
cnf(c_11632,plain,
mult(mult(ld(A,rd(A,A)),rd(ld(A,rd(A,A)),mult(ld(A,rd(A,A)),rd(A,A)))),ld(A,rd(A,A))) = ld(A,rd(ld(A,A),A)),
inference(paramod,[status(thm)],[c_344,c_11631]) ).
cnf(c_11633,plain,
mult(mult(ld(A,rd(A,A)),ld(A,A)),ld(A,rd(A,A))) = ld(A,rd(ld(A,A),A)),
inference(paramod,[status(thm)],[c_505,c_11632]) ).
cnf(c_11634,plain,
mult(ld(A,A),mult(ld(A,rd(A,A)),mult(ld(A,A),ld(A,rd(A,A))))) = ld(A,rd(ld(A,A),A)),
inference(paramod,[status(thm)],[c_511,c_11633]) ).
cnf(c_11635,plain,
mult(ld(A,A),mult(ld(A,rd(A,A)),ld(A,rd(A,A)))) = ld(A,rd(ld(A,A),A)),
inference(paramod,[status(thm)],[c_502,c_11634]) ).
cnf(c_11636,plain,
mult(ld(A,A),mult(ld(A,rd(A,A)),ld(A,rd(A,A)))) = ld(A,ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_95,c_11635]) ).
cnf(c_2242,plain,
mult(ld(A,A),mult(ld(A,rd(A,A)),ld(A,rd(A,A)))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_1864,c_11636]) ).
cnf(c_2261,plain,
rd(ld(A,B),mult(A,ld(C,B))) = ld(A,rd(C,A)),
inference(paramod,[status(thm)],[c_1,c_2220]) ).
cnf(c_11637,plain,
mult(A,rd(ld(A,B),mult(A,ld(C,B)))) = rd(C,A),
inference(paramod,[status(thm)],[c_2261,c_1]) ).
cnf(c_2341,plain,
rd(A,B) = mult(B,rd(ld(B,C),mult(B,ld(A,C)))),
inference(copy,[status(thm)],[c_11637]) ).
cnf(c_11638,plain,
mult(mult(rd(A,B),B),ld(B,C)) = mult(B,mult(rd(ld(B,D),mult(B,ld(A,D))),C)),
inference(paramod,[status(thm)],[c_2261,c_16]) ).
cnf(c_11639,plain,
mult(A,ld(B,C)) = mult(B,mult(rd(ld(B,D),mult(B,ld(A,D))),C)),
inference(paramod,[status(thm)],[c_3,c_11638]) ).
cnf(c_2351,plain,
mult(A,mult(rd(ld(A,B),mult(A,ld(C,B))),D)) = mult(C,ld(A,D)),
inference(copy,[status(thm)],[c_11639]) ).
cnf(c_11640,plain,
mult(ld(A,rd(A,A)),rd(B,A)) = rd(ld(A,C),mult(A,ld(B,C))),
inference(paramod,[status(thm)],[c_2261,c_62]) ).
cnf(c_2358,plain,
rd(ld(A,B),mult(A,ld(C,B))) = mult(ld(A,rd(A,A)),rd(C,A)),
inference(copy,[status(thm)],[c_11640]) ).
cnf(c_2362,plain,
rd(ld(mult(A,B),C),mult(mult(A,B),ld(B,C))) = ld(mult(A,B),ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_170,c_2261]) ).
cnf(c_2434,plain,
rd(ld(A,B),mult(A,ld(C,B))) = rd(ld(A,D),mult(A,ld(C,D))),
inference(paramod,[status(thm)],[c_2261,c_2261]) ).
cnf(c_2463,plain,
ld(mult(A,B),rd(C,mult(A,C))) = ld(mult(A,B),rd(D,mult(A,D))),
inference(paramod,[status(thm)],[c_215,c_2229]) ).
cnf(c_11641,plain,
rd(ld(mult(rd(A,A),B),C),mult(mult(rd(A,A),B),ld(B,C))) = mult(ld(mult(rd(A,A),B),rd(mult(rd(A,A),B),mult(rd(A,A),B))),mult(A,rd(D,mult(A,D)))),
inference(paramod,[status(thm)],[c_460,c_2358]) ).
cnf(c_11642,plain,
ld(mult(rd(A,A),B),ld(rd(A,A),rd(rd(A,A),rd(A,A)))) = mult(ld(mult(rd(A,A),B),rd(mult(rd(A,A),B),mult(rd(A,A),B))),mult(A,rd(D,mult(A,D)))),
inference(paramod,[status(thm)],[c_2362,c_11641]) ).
cnf(c_11643,plain,
ld(mult(rd(A,A),B),ld(rd(A,A),mult(rd(A,A),rd(A,A)))) = mult(ld(mult(rd(A,A),B),rd(mult(rd(A,A),B),mult(rd(A,A),B))),mult(A,rd(D,mult(A,D)))),
inference(paramod,[status(thm)],[c_227,c_11642]) ).
cnf(c_11644,plain,
ld(mult(rd(A,A),B),rd(A,A)) = mult(ld(mult(rd(A,A),B),rd(mult(rd(A,A),B),mult(rd(A,A),B))),mult(A,rd(D,mult(A,D)))),
inference(paramod,[status(thm)],[c_2,c_11643]) ).
cnf(c_11645,plain,
ld(mult(rd(A,A),B),rd(A,A)) = mult(ld(mult(rd(A,A),B),mult(mult(rd(A,A),rd(B,mult(rd(A,A),mult(rd(A,A),B)))),rd(A,A))),mult(A,rd(D,mult(A,D)))),
inference(paramod,[status(thm)],[c_344,c_11644]) ).
cnf(c_11646,plain,
ld(mult(rd(A,A),B),rd(A,A)) = mult(ld(mult(rd(A,A),B),mult(mult(rd(A,A),rd(B,B)),rd(A,A))),mult(A,rd(D,mult(A,D)))),
inference(paramod,[status(thm)],[c_294,c_11645]) ).
cnf(c_2555,plain,
mult(ld(mult(rd(A,A),B),mult(mult(rd(A,A),rd(B,B)),rd(A,A))),mult(A,rd(C,mult(A,C)))) = ld(mult(rd(A,A),B),rd(A,A)),
inference(copy,[status(thm)],[c_11646]) ).
cnf(c_11647,plain,
rd(ld(A,B),mult(A,C)) = rd(ld(A,D),mult(A,ld(rd(B,C),D))),
inference(paramod,[status(thm)],[c_8,c_2434]) ).
cnf(c_2887,plain,
rd(ld(A,B),mult(A,ld(rd(C,D),B))) = rd(ld(A,C),mult(A,D)),
inference(copy,[status(thm)],[c_11647]) ).
cnf(c_11648,plain,
rd(mult(ld(A,rd(A,A)),B),mult(A,ld(C,B))) = rd(ld(A,D),mult(A,ld(C,D))),
inference(paramod,[status(thm)],[c_62,c_2434]) ).
cnf(c_11649,plain,
mult(mult(ld(A,rd(A,A)),rd(B,mult(ld(A,rd(A,A)),mult(A,ld(C,B))))),ld(A,rd(A,A))) = rd(ld(A,D),mult(A,ld(C,D))),
inference(paramod,[status(thm)],[c_344,c_11648]) ).
cnf(c_11650,plain,
mult(mult(ld(A,rd(A,A)),rd(B,ld(C,B))),ld(A,rd(A,A))) = rd(ld(A,D),mult(A,ld(C,D))),
inference(paramod,[status(thm)],[c_94,c_11649]) ).
cnf(c_11651,plain,
mult(mult(ld(A,rd(A,A)),C),ld(A,rd(A,A))) = rd(ld(A,D),mult(A,ld(C,D))),
inference(paramod,[status(thm)],[c_9,c_11650]) ).
cnf(c_2891,plain,
rd(ld(A,B),mult(A,ld(C,B))) = mult(mult(ld(A,rd(A,A)),C),ld(A,rd(A,A))),
inference(copy,[status(thm)],[c_11651]) ).
cnf(c_11652,plain,
mult(rd(ld(A,B),mult(A,ld(C,B))),D) = ld(rd(mult(A,ld(C,E)),ld(A,E)),D),
inference(paramod,[status(thm)],[c_2434,c_242]) ).
cnf(c_11653,plain,
mult(mult(mult(ld(A,rd(A,A)),C),ld(A,rd(A,A))),D) = ld(rd(mult(A,ld(C,E)),ld(A,E)),D),
inference(paramod,[status(thm)],[c_2891,c_11652]) ).
cnf(c_11654,plain,
mult(ld(A,rd(A,A)),mult(C,mult(ld(A,rd(A,A)),D))) = ld(rd(mult(A,ld(C,E)),ld(A,E)),D),
inference(paramod,[status(thm)],[c_6,c_11653]) ).
cnf(c_11655,plain,
mult(ld(A,rd(A,A)),mult(C,mult(ld(A,rd(A,A)),D))) = ld(mult(mult(A,rd(ld(C,E),mult(A,ld(A,E)))),A),D),
inference(paramod,[status(thm)],[c_344,c_11654]) ).
cnf(c_11656,plain,
mult(ld(A,rd(A,A)),mult(C,mult(ld(A,rd(A,A)),D))) = ld(mult(mult(A,rd(ld(C,E),E)),A),D),
inference(paramod,[status(thm)],[c_1,c_11655]) ).
cnf(c_2896,plain,
mult(ld(A,rd(A,A)),mult(B,mult(ld(A,rd(A,A)),C))) = ld(mult(mult(A,ld(B,rd(B,B))),A),C),
inference(paramod,[status(thm)],[c_95,c_11656]) ).
cnf(c_11657,plain,
mult(mult(ld(A,rd(A,A)),rd(C,D)),ld(A,rd(A,A))) = rd(ld(A,C),mult(A,D)),
inference(paramod,[status(thm)],[c_2891,c_2887]) ).
cnf(c_2918,plain,
rd(ld(A,B),mult(A,C)) = mult(mult(ld(A,rd(A,A)),rd(B,C)),ld(A,rd(A,A))),
inference(copy,[status(thm)],[c_11657]) ).
cnf(c_11658,plain,
mult(A,mult(mult(mult(ld(A,rd(A,A)),rd(B,ld(C,B))),ld(A,rd(A,A))),D)) = mult(C,ld(A,D)),
inference(paramod,[status(thm)],[c_2918,c_2351]) ).
cnf(c_11659,plain,
mult(A,mult(mult(mult(ld(A,rd(A,A)),C),ld(A,rd(A,A))),D)) = mult(C,ld(A,D)),
inference(paramod,[status(thm)],[c_9,c_11658]) ).
cnf(c_11660,plain,
mult(A,mult(ld(A,rd(A,A)),mult(C,mult(ld(A,rd(A,A)),D)))) = mult(C,ld(A,D)),
inference(paramod,[status(thm)],[c_6,c_11659]) ).
cnf(c_2987,plain,
mult(A,mult(ld(B,rd(B,B)),C)) = mult(A,ld(B,C)),
inference(paramod,[status(thm)],[c_92,c_11660]) ).
cnf(c_11661,plain,
rd(A,B) = mult(B,mult(mult(ld(B,rd(B,B)),rd(C,ld(A,C))),ld(B,rd(B,B)))),
inference(paramod,[status(thm)],[c_2918,c_2341]) ).
cnf(c_2991,plain,
rd(A,B) = mult(B,mult(mult(ld(B,rd(B,B)),A),ld(B,rd(B,B)))),
inference(paramod,[status(thm)],[c_9,c_11661]) ).
cnf(c_11662,plain,
ld(A,rd(B,mult(C,B))) = ld(mult(C,ld(C,A)),rd(D,mult(C,D))),
inference(paramod,[status(thm)],[c_1,c_2463]) ).
cnf(c_3019,plain,
ld(A,rd(B,mult(C,B))) = ld(A,rd(D,mult(C,D))),
inference(paramod,[status(thm)],[c_1,c_11662]) ).
cnf(c_11663,plain,
ld(rd(A,mult(B,A)),rd(C,mult(D,C))) = mult(B,rd(E,mult(D,E))),
inference(paramod,[status(thm)],[c_3019,c_221]) ).
cnf(c_3066,plain,
mult(A,rd(B,mult(C,B))) = mult(A,rd(D,mult(C,D))),
inference(paramod,[status(thm)],[c_221,c_11663]) ).
cnf(c_11664,plain,
rd(ld(rd(A,mult(B,A)),rd(C,mult(B,C))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))) = mult(ld(rd(A,mult(B,A)),rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_3019,c_522]) ).
cnf(c_11665,plain,
rd(mult(B,rd(C,mult(B,C))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))) = mult(ld(rd(A,mult(B,A)),rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_221,c_11664]) ).
cnf(c_11666,plain,
rd(mult(B,rd(C,mult(B,C))),mult(B,rd(A,mult(B,A)))) = mult(ld(rd(A,mult(B,A)),rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_221,c_11665]) ).
cnf(c_11667,plain,
mult(mult(B,rd(rd(C,mult(B,C)),mult(B,mult(B,rd(A,mult(B,A)))))),B) = mult(ld(rd(A,mult(B,A)),rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_344,c_11666]) ).
cnf(c_11668,plain,
mult(mult(B,rd(rd(C,mult(B,C)),mult(B,mult(B,rd(A,mult(B,A)))))),B) = mult(mult(B,rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_221,c_11667]) ).
cnf(c_3067,plain,
mult(mult(A,rd(rd(B,mult(A,B)),mult(A,mult(A,rd(C,mult(A,C)))))),A) = mult(mult(A,rd(C,mult(A,C))),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_221,c_11668]) ).
cnf(c_11669,plain,
mult(A,rd(ld(B,C),C)) = mult(A,rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_1,c_3066]) ).
cnf(c_11670,plain,
mult(A,ld(B,rd(B,B))) = mult(A,rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_95,c_11669]) ).
cnf(c_3096,plain,
mult(A,rd(B,mult(C,B))) = mult(A,ld(C,rd(C,C))),
inference(copy,[status(thm)],[c_11670]) ).
cnf(c_3097,plain,
mult(rd(A,rd(B,mult(C,B))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_3066,c_3]) ).
cnf(c_3212,plain,
mult(ld(A,rd(A,A)),ld(B,rd(B,B))) = ld(A,rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_3096,c_62]) ).
cnf(c_3224,plain,
mult(rd(A,B),ld(C,rd(C,C))) = ld(rd(B,A),rd(D,mult(C,D))),
inference(paramod,[status(thm)],[c_3096,c_242]) ).
cnf(c_3236,plain,
mult(A,rd(B,mult(C,B))) = mult(A,ld(C,rd(D,mult(rd(C,C),D)))),
inference(paramod,[status(thm)],[c_219,c_3096]) ).
cnf(c_3238,plain,
ld(rd(ld(A,rd(A,A)),mult(B,rd(C,mult(A,C)))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_3096,c_221]) ).
cnf(c_3284,plain,
mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_3096,c_908]) ).
cnf(c_3334,plain,
mult(ld(A,rd(A,A)),rd(A,A)) = mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))),
inference(paramod,[status(thm)],[c_3096,c_924]) ).
cnf(c_3338,plain,
mult(rd(A,mult(B,A)),rd(B,B)) = mult(ld(B,B),rd(ld(C,rd(C,C)),mult(B,rd(D,mult(C,D))))),
inference(paramod,[status(thm)],[c_3096,c_944]) ).
cnf(c_11671,plain,
rd(ld(rd(A,mult(B,A)),rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),rd(rd(A,mult(B,A)),rd(A,mult(B,A)))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_3212,c_522]) ).
cnf(c_11672,plain,
rd(mult(B,rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),rd(rd(A,mult(B,A)),rd(A,mult(B,A)))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_221,c_11671]) ).
cnf(c_11673,plain,
rd(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),rd(rd(A,mult(B,A)),rd(A,mult(B,A)))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_221,c_11672]) ).
cnf(c_11674,plain,
mult(mult(B,rd(rd(A,mult(B,A)),mult(B,mult(B,rd(A,mult(B,A)))))),B) = mult(mult(ld(rd(A,mult(B,A)),rd(rd(A,mult(B,A)),rd(A,mult(B,A)))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_344,c_11673]) ).
cnf(c_11675,plain,
mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),rd(rd(A,mult(B,A)),rd(A,mult(B,A)))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_3067,c_11674]) ).
cnf(c_11676,plain,
mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),mult(rd(A,mult(B,A)),rd(mult(B,A),A))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_227,c_11675]) ).
cnf(c_11677,plain,
mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),mult(rd(A,mult(B,A)),mult(mult(B,rd(A,mult(B,A))),B))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_344,c_11676]) ).
cnf(c_11678,plain,
mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),mult(rd(A,mult(B,A)),B)),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_226,c_11677]) ).
cnf(c_11679,plain,
mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(B,ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_2,c_11678]) ).
cnf(c_11680,plain,
mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(rd(B,B),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_1,c_11679]) ).
cnf(c_11681,plain,
mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(rd(B,B),mult(B,rd(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_221,c_11680]) ).
cnf(c_3891,plain,
mult(mult(A,rd(B,mult(A,B))),mult(A,rd(B,mult(A,B)))) = mult(ld(A,A),mult(A,rd(B,mult(A,B)))),
inference(paramod,[status(thm)],[c_1090,c_11681]) ).
cnf(c_3933,plain,
mult(mult(A,rd(rd(B,mult(A,B)),mult(A,mult(A,rd(C,mult(A,C)))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_3891,c_3067]) ).
cnf(c_11682,plain,
mult(A,ld(B,rd(B,B))) = ld(rd(mult(ld(A,rd(A,A)),C),C),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_51,c_3224]) ).
cnf(c_11683,plain,
mult(A,ld(B,rd(B,B))) = ld(mult(mult(ld(A,rd(A,A)),rd(C,mult(ld(A,rd(A,A)),C))),ld(A,rd(A,A))),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_344,c_11682]) ).
cnf(c_4023,plain,
mult(A,ld(B,rd(B,B))) = ld(mult(mult(ld(A,rd(A,A)),A),ld(A,rd(A,A))),rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_51,c_11683]) ).
cnf(c_4416,plain,
ld(mult(ld(A,rd(A,A)),rd(B,mult(rd(A,A),B))),C) = mult(A,C),
inference(paramod,[status(thm)],[c_219,c_484]) ).
cnf(c_4643,plain,
mult(mult(mult(rd(A,mult(B,A)),B),ld(B,B)),ld(B,B)) = ld(B,B),
inference(paramod,[status(thm)],[c_189,c_521]) ).
cnf(c_4669,plain,
ld(mult(rd(rd(A,mult(B,A)),mult(C,rd(D,mult(B,D)))),C),E) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_3066,c_523]) ).
cnf(c_11684,plain,
mult(mult(rd(A,mult(B,A)),rd(mult(B,A),A)),ld(B,rd(B,B))) = rd(A,mult(B,A)),
inference(paramod,[status(thm)],[c_170,c_911]) ).
cnf(c_11685,plain,
mult(mult(rd(A,mult(B,A)),mult(mult(B,rd(A,mult(B,A))),B)),ld(B,rd(B,B))) = rd(A,mult(B,A)),
inference(paramod,[status(thm)],[c_344,c_11684]) ).
cnf(c_4692,plain,
mult(mult(rd(A,mult(B,A)),B),ld(B,rd(B,B))) = rd(A,mult(B,A)),
inference(paramod,[status(thm)],[c_226,c_11685]) ).
cnf(c_11686,plain,
mult(rd(A,A),B) = mult(ld(A,A),mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_1,c_1090]) ).
cnf(c_4750,plain,
mult(rd(A,A),B) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_1,c_11686]) ).
cnf(c_11687,plain,
rd(mult(A,B),mult(ld(A,A),mult(A,B))) = ld(rd(A,A),rd(rd(A,A),rd(A,A))),
inference(paramod,[status(thm)],[c_1090,c_170]) ).
cnf(c_11688,plain,
ld(A,A) = ld(rd(A,A),rd(rd(A,A),rd(A,A))),
inference(paramod,[status(thm)],[c_513,c_11687]) ).
cnf(c_11689,plain,
ld(A,A) = ld(rd(A,A),mult(rd(A,A),rd(A,A))),
inference(paramod,[status(thm)],[c_227,c_11688]) ).
cnf(c_11690,plain,
ld(A,A) = ld(rd(A,A),mult(ld(A,A),rd(A,A))),
inference(paramod,[status(thm)],[c_4750,c_11689]) ).
cnf(c_11691,plain,
ld(A,A) = mult(rd(A,A),mult(ld(A,A),rd(A,A))),
inference(paramod,[status(thm)],[c_242,c_11690]) ).
cnf(c_11692,plain,
ld(A,A) = mult(ld(A,A),mult(ld(A,A),rd(A,A))),
inference(paramod,[status(thm)],[c_4750,c_11691]) ).
cnf(c_11693,plain,
ld(A,A) = rd(A,A),
inference(paramod,[status(thm)],[c_514,c_11692]) ).
cnf(c_4759,plain,
rd(A,A) = ld(A,A),
inference(copy,[status(thm)],[c_11693]) ).
cnf(c_11694,plain,
rd(mult(A,B),mult(ld(A,A),mult(A,B))) = mult(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_1090,c_460]) ).
cnf(c_11695,plain,
ld(A,A) = mult(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_513,c_11694]) ).
cnf(c_4769,plain,
mult(A,rd(B,mult(A,B))) = ld(A,A),
inference(copy,[status(thm)],[c_11695]) ).
cnf(c_11696,plain,
mult(rd(mult(A,B),mult(ld(A,A),mult(A,B))),A) = A,
inference(paramod,[status(thm)],[c_1090,c_249]) ).
cnf(c_4772,plain,
mult(ld(A,A),A) = A,
inference(paramod,[status(thm)],[c_513,c_11696]) ).
cnf(c_11697,plain,
ld(mult(ld(A,ld(A,A)),rd(B,mult(rd(A,A),B))),C) = mult(A,C),
inference(paramod,[status(thm)],[c_4759,c_4416]) ).
cnf(c_11698,plain,
ld(mult(ld(A,ld(A,A)),rd(B,mult(ld(A,A),B))),C) = mult(A,C),
inference(paramod,[status(thm)],[c_4759,c_11697]) ).
cnf(c_4793,plain,
ld(mult(ld(A,ld(A,A)),ld(A,A)),B) = mult(A,B),
inference(paramod,[status(thm)],[c_513,c_11698]) ).
cnf(c_11699,plain,
mult(A,rd(B,mult(C,B))) = mult(A,ld(C,rd(D,mult(ld(C,C),D)))),
inference(paramod,[status(thm)],[c_4759,c_3236]) ).
cnf(c_4821,plain,
mult(A,rd(B,mult(C,B))) = mult(A,ld(C,ld(C,C))),
inference(paramod,[status(thm)],[c_513,c_11699]) ).
cnf(c_11700,plain,
mult(ld(mult(ld(A,A),B),mult(mult(rd(A,A),rd(B,B)),rd(A,A))),mult(A,rd(C,mult(A,C)))) = ld(mult(rd(A,A),B),rd(A,A)),
inference(paramod,[status(thm)],[c_4759,c_2555]) ).
cnf(c_11701,plain,
mult(ld(mult(ld(A,A),B),mult(mult(ld(A,A),rd(B,B)),rd(A,A))),mult(A,rd(C,mult(A,C)))) = ld(mult(rd(A,A),B),rd(A,A)),
inference(paramod,[status(thm)],[c_4759,c_11700]) ).
cnf(c_11702,plain,
mult(ld(mult(ld(A,A),B),mult(mult(ld(A,A),ld(B,B)),rd(A,A))),mult(A,rd(C,mult(A,C)))) = ld(mult(rd(A,A),B),rd(A,A)),
inference(paramod,[status(thm)],[c_4759,c_11701]) ).
cnf(c_11703,plain,
mult(ld(mult(ld(A,A),B),mult(mult(ld(A,A),ld(B,B)),ld(A,A))),mult(A,rd(C,mult(A,C)))) = ld(mult(rd(A,A),B),rd(A,A)),
inference(paramod,[status(thm)],[c_4759,c_11702]) ).
cnf(c_11704,plain,
mult(ld(mult(ld(A,A),B),mult(mult(ld(A,A),ld(B,B)),ld(A,A))),ld(A,A)) = ld(mult(rd(A,A),B),rd(A,A)),
inference(paramod,[status(thm)],[c_4769,c_11703]) ).
cnf(c_11705,plain,
mult(ld(mult(ld(A,A),B),mult(mult(ld(A,A),ld(B,B)),ld(A,A))),ld(A,A)) = ld(mult(ld(A,A),B),rd(A,A)),
inference(paramod,[status(thm)],[c_4759,c_11704]) ).
cnf(c_4827,plain,
mult(ld(mult(ld(A,A),B),mult(mult(ld(A,A),ld(B,B)),ld(A,A))),ld(A,A)) = ld(mult(ld(A,A),B),ld(A,A)),
inference(paramod,[status(thm)],[c_4759,c_11705]) ).
cnf(c_11706,plain,
mult(ld(A,ld(A,A)),mult(rd(A,A),mult(ld(A,rd(A,A)),B))) = ld(A,mult(ld(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_4759,c_2032]) ).
cnf(c_11707,plain,
mult(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,rd(A,A)),B))) = ld(A,mult(ld(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_4759,c_11706]) ).
cnf(c_11708,plain,
mult(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,ld(A,A)),B))) = ld(A,mult(ld(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_4759,c_11707]) ).
cnf(c_4828,plain,
ld(A,mult(ld(A,A),ld(A,B))) = mult(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,ld(A,A)),B))),
inference(copy,[status(thm)],[c_11708]) ).
cnf(c_11709,plain,
mult(ld(A,A),mult(ld(A,A),mult(ld(A,rd(A,A)),B))) = ld(A,B),
inference(paramod,[status(thm)],[c_4759,c_1891]) ).
cnf(c_11710,plain,
mult(ld(A,A),mult(ld(A,A),mult(ld(A,ld(A,A)),B))) = ld(A,B),
inference(paramod,[status(thm)],[c_4759,c_11709]) ).
cnf(c_4833,plain,
mult(ld(A,ld(A,A)),B) = ld(A,B),
inference(paramod,[status(thm)],[c_514,c_11710]) ).
cnf(c_11711,plain,
mult(ld(A,A),mult(ld(A,rd(A,A)),B)) = mult(A,mult(ld(A,rd(C,mult(A,C))),B)),
inference(paramod,[status(thm)],[c_4759,c_1881]) ).
cnf(c_11712,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),B)) = mult(A,mult(ld(A,rd(C,mult(A,C))),B)),
inference(paramod,[status(thm)],[c_4759,c_11711]) ).
cnf(c_4835,plain,
mult(A,mult(ld(A,rd(B,mult(A,B))),C)) = mult(ld(A,A),mult(ld(A,ld(A,A)),C)),
inference(copy,[status(thm)],[c_11712]) ).
cnf(c_11713,plain,
mult(ld(A,A),mult(rd(B,mult(A,B)),C)) = mult(A,mult(ld(A,rd(D,mult(A,D))),C)),
inference(paramod,[status(thm)],[c_4759,c_1793]) ).
cnf(c_4841,plain,
mult(ld(A,A),mult(rd(B,mult(A,B)),C)) = mult(ld(A,A),mult(ld(A,ld(A,A)),C)),
inference(paramod,[status(thm)],[c_4835,c_11713]) ).
cnf(c_11714,plain,
mult(A,mult(ld(A,A),mult(mult(rd(A,A),rd(B,mult(A,B))),C))) = mult(rd(A,A),C),
inference(paramod,[status(thm)],[c_4759,c_1323]) ).
cnf(c_11715,plain,
mult(A,mult(ld(A,A),mult(mult(ld(A,A),rd(B,mult(A,B))),C))) = mult(rd(A,A),C),
inference(paramod,[status(thm)],[c_4759,c_11714]) ).
cnf(c_11716,plain,
mult(A,mult(ld(A,A),mult(mult(ld(A,A),ld(A,ld(A,A))),C))) = mult(rd(A,A),C),
inference(paramod,[status(thm)],[c_4821,c_11715]) ).
cnf(c_4850,plain,
mult(A,mult(ld(A,A),mult(mult(ld(A,A),ld(A,ld(A,A))),B))) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_4759,c_11716]) ).
cnf(c_11717,plain,
mult(ld(A,A),mult(rd(B,mult(A,B)),C)) = mult(mult(rd(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
inference(paramod,[status(thm)],[c_4759,c_724]) ).
cnf(c_11718,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),C)) = mult(mult(rd(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
inference(paramod,[status(thm)],[c_4841,c_11717]) ).
cnf(c_11719,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),C)) = mult(mult(ld(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
inference(paramod,[status(thm)],[c_4759,c_11718]) ).
cnf(c_11720,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),C)) = mult(mult(ld(A,A),ld(A,ld(A,A))),mult(rd(A,A),C)),
inference(paramod,[status(thm)],[c_4821,c_11719]) ).
cnf(c_11721,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),C)) = mult(mult(ld(A,A),ld(A,ld(A,A))),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_4759,c_11720]) ).
cnf(c_4859,plain,
mult(mult(ld(A,A),ld(A,ld(A,A))),mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(A,ld(A,A)),B)),
inference(copy,[status(thm)],[c_11721]) ).
cnf(c_11722,plain,
rd(A,mult(B,A)) = mult(ld(B,ld(B,B)),rd(C,mult(rd(B,B),C))),
inference(paramod,[status(thm)],[c_4759,c_501]) ).
cnf(c_11723,plain,
rd(A,mult(B,A)) = mult(ld(B,ld(B,B)),rd(C,mult(ld(B,B),C))),
inference(paramod,[status(thm)],[c_4759,c_11722]) ).
cnf(c_4863,plain,
rd(A,mult(B,A)) = mult(ld(B,ld(B,B)),ld(B,B)),
inference(paramod,[status(thm)],[c_513,c_11723]) ).
cnf(c_11724,plain,
mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(rd(B,B),mult(mult(rd(B,B),ld(B,rd(B,B))),mult(rd(B,B),C))),
inference(paramod,[status(thm)],[c_4863,c_486]) ).
cnf(c_11725,plain,
mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(ld(B,B),mult(mult(rd(B,B),ld(B,rd(B,B))),mult(rd(B,B),C))),
inference(paramod,[status(thm)],[c_4759,c_11724]) ).
cnf(c_11726,plain,
mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(B,rd(B,B))),mult(rd(B,B),C))),
inference(paramod,[status(thm)],[c_4759,c_11725]) ).
cnf(c_11727,plain,
mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(B,ld(B,B))),mult(rd(B,B),C))),
inference(paramod,[status(thm)],[c_4759,c_11726]) ).
cnf(c_11728,plain,
mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(B,ld(B,B))),mult(ld(B,B),C))),
inference(paramod,[status(thm)],[c_4759,c_11727]) ).
cnf(c_11729,plain,
mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(ld(B,B),mult(ld(B,B),mult(ld(B,ld(B,B)),C))),
inference(paramod,[status(thm)],[c_4859,c_11728]) ).
cnf(c_4864,plain,
mult(mult(ld(A,ld(A,A)),ld(A,A)),B) = mult(ld(A,ld(A,A)),B),
inference(paramod,[status(thm)],[c_514,c_11729]) ).
cnf(c_11730,plain,
mult(mult(mult(ld(B,ld(B,B)),ld(B,B)),B),ld(B,rd(B,B))) = rd(A,mult(B,A)),
inference(paramod,[status(thm)],[c_4863,c_4692]) ).
cnf(c_11731,plain,
mult(mult(ld(B,ld(B,B)),B),ld(B,rd(B,B))) = rd(A,mult(B,A)),
inference(paramod,[status(thm)],[c_4864,c_11730]) ).
cnf(c_11732,plain,
mult(mult(ld(B,ld(B,B)),B),ld(B,ld(B,B))) = rd(A,mult(B,A)),
inference(paramod,[status(thm)],[c_4759,c_11731]) ).
cnf(c_4873,plain,
mult(mult(ld(A,ld(A,A)),A),ld(A,ld(A,A))) = mult(ld(A,ld(A,A)),ld(A,A)),
inference(paramod,[status(thm)],[c_4863,c_11732]) ).
cnf(c_11733,plain,
mult(A,ld(B,ld(B,B))) = ld(mult(mult(ld(A,rd(A,A)),A),ld(A,rd(A,A))),rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_4759,c_4023]) ).
cnf(c_11734,plain,
mult(A,ld(B,ld(B,B))) = ld(mult(mult(ld(A,ld(A,A)),A),ld(A,rd(A,A))),rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_4759,c_11733]) ).
cnf(c_11735,plain,
mult(A,ld(B,ld(B,B))) = ld(mult(mult(ld(A,ld(A,A)),A),ld(A,ld(A,A))),rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_4759,c_11734]) ).
cnf(c_11736,plain,
mult(A,ld(B,ld(B,B))) = ld(mult(ld(A,ld(A,A)),ld(A,A)),rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_4873,c_11735]) ).
cnf(c_11737,plain,
mult(A,ld(B,ld(B,B))) = ld(mult(ld(A,ld(A,A)),ld(A,A)),mult(ld(B,ld(B,B)),ld(B,B))),
inference(paramod,[status(thm)],[c_4863,c_11736]) ).
cnf(c_11738,plain,
mult(A,ld(B,ld(B,B))) = mult(A,mult(ld(B,ld(B,B)),ld(B,B))),
inference(paramod,[status(thm)],[c_4793,c_11737]) ).
cnf(c_4947,plain,
mult(A,mult(ld(B,ld(B,B)),ld(B,B))) = mult(A,ld(B,ld(B,B))),
inference(copy,[status(thm)],[c_11738]) ).
cnf(c_11739,plain,
mult(mult(ld(B,ld(B,B)),ld(B,B)),rd(B,B)) = mult(ld(B,B),rd(ld(C,rd(C,C)),mult(B,rd(D,mult(C,D))))),
inference(paramod,[status(thm)],[c_4863,c_3338]) ).
cnf(c_11740,plain,
mult(mult(ld(B,ld(B,B)),ld(B,B)),ld(B,B)) = mult(ld(B,B),rd(ld(C,rd(C,C)),mult(B,rd(D,mult(C,D))))),
inference(paramod,[status(thm)],[c_4759,c_11739]) ).
cnf(c_11741,plain,
mult(ld(B,ld(B,B)),ld(B,B)) = mult(ld(B,B),rd(ld(C,rd(C,C)),mult(B,rd(D,mult(C,D))))),
inference(paramod,[status(thm)],[c_4864,c_11740]) ).
cnf(c_11742,plain,
mult(ld(B,ld(B,B)),ld(B,B)) = mult(ld(B,B),rd(ld(C,ld(C,C)),mult(B,rd(D,mult(C,D))))),
inference(paramod,[status(thm)],[c_4759,c_11741]) ).
cnf(c_11743,plain,
mult(ld(B,ld(B,B)),ld(B,B)) = mult(ld(B,B),rd(ld(C,ld(C,C)),mult(B,mult(ld(C,ld(C,C)),ld(C,C))))),
inference(paramod,[status(thm)],[c_4863,c_11742]) ).
cnf(c_11744,plain,
mult(ld(B,ld(B,B)),ld(B,B)) = mult(ld(B,B),rd(ld(C,ld(C,C)),mult(B,ld(C,ld(C,C))))),
inference(paramod,[status(thm)],[c_4947,c_11743]) ).
cnf(c_11745,plain,
mult(ld(B,ld(B,B)),ld(B,B)) = mult(ld(B,B),mult(ld(B,ld(B,B)),ld(B,B))),
inference(paramod,[status(thm)],[c_4863,c_11744]) ).
cnf(c_5013,plain,
mult(ld(A,ld(A,A)),ld(A,A)) = mult(ld(A,A),ld(A,ld(A,A))),
inference(paramod,[status(thm)],[c_4947,c_11745]) ).
cnf(c_11746,plain,
mult(ld(A,ld(A,A)),rd(A,A)) = mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))),
inference(paramod,[status(thm)],[c_4759,c_3334]) ).
cnf(c_11747,plain,
mult(ld(A,ld(A,A)),ld(A,A)) = mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))),
inference(paramod,[status(thm)],[c_4759,c_11746]) ).
cnf(c_11748,plain,
mult(ld(A,A),ld(A,ld(A,A))) = mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))),
inference(paramod,[status(thm)],[c_5013,c_11747]) ).
cnf(c_11749,plain,
mult(ld(A,A),ld(A,ld(A,A))) = mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,rd(C,mult(B,C))))),
inference(paramod,[status(thm)],[c_4759,c_11748]) ).
cnf(c_11750,plain,
mult(ld(A,A),ld(A,ld(A,A))) = mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,ld(B,B)),ld(B,B))))),
inference(paramod,[status(thm)],[c_4863,c_11749]) ).
cnf(c_11751,plain,
mult(ld(A,A),ld(A,ld(A,A))) = mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,B),ld(B,ld(B,B)))))),
inference(paramod,[status(thm)],[c_5013,c_11750]) ).
cnf(c_5014,plain,
mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,B),ld(B,ld(B,B)))))) = mult(ld(A,A),ld(A,ld(A,A))),
inference(copy,[status(thm)],[c_11751]) ).
cnf(c_11752,plain,
mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,rd(C,mult(B,C))))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_4759,c_3284]) ).
cnf(c_11753,plain,
mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,ld(B,B)),ld(B,B))))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_4863,c_11752]) ).
cnf(c_11754,plain,
mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,B),ld(B,ld(B,B)))))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_5013,c_11753]) ).
cnf(c_11755,plain,
mult(ld(A,A),ld(A,ld(A,A))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_5014,c_11754]) ).
cnf(c_5024,plain,
mult(ld(A,A),ld(A,ld(A,A))) = ld(A,ld(A,A)),
inference(paramod,[status(thm)],[c_4759,c_11755]) ).
cnf(c_11756,plain,
ld(rd(ld(A,ld(A,A)),mult(B,rd(C,mult(A,C)))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_4759,c_3238]) ).
cnf(c_11757,plain,
ld(rd(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),ld(A,A)))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_4863,c_11756]) ).
cnf(c_11758,plain,
ld(rd(ld(A,ld(A,A)),mult(B,mult(ld(A,A),ld(A,ld(A,A))))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_5013,c_11757]) ).
cnf(c_11759,plain,
ld(rd(ld(A,ld(A,A)),mult(B,ld(A,ld(A,A)))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_5024,c_11758]) ).
cnf(c_11760,plain,
ld(mult(ld(B,ld(B,B)),ld(B,B)),D) = mult(B,D),
inference(paramod,[status(thm)],[c_4863,c_11759]) ).
cnf(c_11761,plain,
ld(mult(ld(B,B),ld(B,ld(B,B))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_5013,c_11760]) ).
cnf(c_5030,plain,
ld(ld(A,ld(A,A)),B) = mult(A,B),
inference(paramod,[status(thm)],[c_5024,c_11761]) ).
cnf(c_11762,plain,
rd(A,B) = mult(B,mult(mult(ld(B,ld(B,B)),A),ld(B,rd(B,B)))),
inference(paramod,[status(thm)],[c_4759,c_2991]) ).
cnf(c_5038,plain,
rd(A,B) = mult(B,mult(mult(ld(B,ld(B,B)),A),ld(B,ld(B,B)))),
inference(paramod,[status(thm)],[c_4759,c_11762]) ).
cnf(c_5039,plain,
mult(A,mult(ld(B,ld(B,B)),C)) = mult(A,ld(B,C)),
inference(paramod,[status(thm)],[c_4759,c_2987]) ).
cnf(c_11763,plain,
mult(ld(A,ld(A,A)),mult(B,mult(ld(A,rd(A,A)),C))) = ld(mult(mult(A,ld(B,rd(B,B))),A),C),
inference(paramod,[status(thm)],[c_4759,c_2896]) ).
cnf(c_11764,plain,
mult(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),C))) = ld(mult(mult(A,ld(B,rd(B,B))),A),C),
inference(paramod,[status(thm)],[c_4759,c_11763]) ).
cnf(c_11765,plain,
mult(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),C))) = ld(mult(mult(A,ld(B,ld(B,B))),A),C),
inference(paramod,[status(thm)],[c_4759,c_11764]) ).
cnf(c_5052,plain,
ld(mult(mult(A,ld(B,ld(B,B))),A),C) = mult(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),C))),
inference(copy,[status(thm)],[c_11765]) ).
cnf(c_11766,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(A,rd(A,A)))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_4759,c_2242]) ).
cnf(c_11767,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(A,ld(A,A)))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_4759,c_11766]) ).
cnf(c_11768,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(A,ld(A,A)))) = mult(ld(A,ld(A,A)),ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_4759,c_11767]) ).
cnf(c_5061,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(A,ld(A,A)))) = mult(ld(A,ld(A,A)),ld(A,ld(A,A))),
inference(paramod,[status(thm)],[c_4759,c_11768]) ).
cnf(c_11769,plain,
mult(ld(A,mult(A,mult(mult(ld(A,ld(A,A)),B),ld(A,ld(A,A))))),mult(A,C)) = mult(ld(A,rd(A,A)),mult(B,C)),
inference(paramod,[status(thm)],[c_5038,c_1946]) ).
cnf(c_11770,plain,
mult(mult(mult(ld(A,ld(A,A)),B),ld(A,ld(A,A))),mult(A,C)) = mult(ld(A,rd(A,A)),mult(B,C)),
inference(paramod,[status(thm)],[c_2,c_11769]) ).
cnf(c_11771,plain,
mult(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),mult(A,C)))) = mult(ld(A,rd(A,A)),mult(B,C)),
inference(paramod,[status(thm)],[c_6,c_11770]) ).
cnf(c_5071,plain,
mult(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),mult(A,C)))) = mult(ld(A,ld(A,A)),mult(B,C)),
inference(paramod,[status(thm)],[c_4759,c_11771]) ).
cnf(c_11772,plain,
mult(A,mult(ld(B,ld(B,B)),C)) = mult(B,mult(ld(B,rd(A,B)),C)),
inference(paramod,[status(thm)],[c_4759,c_1548]) ).
cnf(c_11773,plain,
mult(A,mult(ld(B,ld(B,B)),C)) = mult(B,mult(ld(B,mult(B,mult(mult(ld(B,ld(B,B)),A),ld(B,ld(B,B))))),C)),
inference(paramod,[status(thm)],[c_5038,c_11772]) ).
cnf(c_11774,plain,
mult(A,mult(ld(B,ld(B,B)),C)) = mult(B,mult(mult(mult(ld(B,ld(B,B)),A),ld(B,ld(B,B))),C)),
inference(paramod,[status(thm)],[c_2,c_11773]) ).
cnf(c_11775,plain,
mult(A,mult(ld(B,ld(B,B)),C)) = mult(B,mult(ld(B,ld(B,B)),mult(A,mult(ld(B,ld(B,B)),C)))),
inference(paramod,[status(thm)],[c_6,c_11774]) ).
cnf(c_5075,plain,
mult(A,mult(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),C)))) = mult(B,mult(ld(A,ld(A,A)),C)),
inference(copy,[status(thm)],[c_11775]) ).
cnf(c_11776,plain,
mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))) = mult(ld(B,rd(B,B)),rd(B,B)),
inference(paramod,[status(thm)],[c_5038,c_192]) ).
cnf(c_11777,plain,
mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))) = mult(ld(B,ld(B,B)),rd(B,B)),
inference(paramod,[status(thm)],[c_4759,c_11776]) ).
cnf(c_11778,plain,
mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))) = mult(ld(B,ld(B,B)),ld(B,B)),
inference(paramod,[status(thm)],[c_4759,c_11777]) ).
cnf(c_11779,plain,
mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))) = mult(ld(B,B),ld(B,ld(B,B))),
inference(paramod,[status(thm)],[c_5013,c_11778]) ).
cnf(c_5121,plain,
mult(mult(A,B),mult(mult(ld(mult(A,B),ld(mult(A,B),mult(A,B))),B),ld(mult(A,B),ld(mult(A,B),mult(A,B))))) = ld(A,ld(A,A)),
inference(paramod,[status(thm)],[c_5024,c_11779]) ).
cnf(c_11780,plain,
rd(ld(A,A),rd(B,mult(A,B))) = A,
inference(paramod,[status(thm)],[c_4759,c_177]) ).
cnf(c_11781,plain,
rd(ld(A,A),mult(mult(A,B),mult(mult(ld(mult(A,B),ld(mult(A,B),mult(A,B))),B),ld(mult(A,B),ld(mult(A,B),mult(A,B)))))) = A,
inference(paramod,[status(thm)],[c_5038,c_11780]) ).
cnf(c_11782,plain,
rd(ld(A,A),ld(A,ld(A,A))) = A,
inference(paramod,[status(thm)],[c_5121,c_11781]) ).
cnf(c_11783,plain,
mult(ld(A,ld(A,A)),mult(mult(ld(ld(A,ld(A,A)),ld(ld(A,ld(A,A)),ld(A,ld(A,A)))),ld(A,A)),ld(ld(A,ld(A,A)),ld(ld(A,ld(A,A)),ld(A,ld(A,A)))))) = A,
inference(paramod,[status(thm)],[c_5038,c_11782]) ).
cnf(c_11784,plain,
mult(ld(A,ld(A,A)),mult(mult(ld(ld(A,ld(A,A)),mult(A,ld(A,ld(A,A)))),ld(A,A)),ld(ld(A,ld(A,A)),ld(ld(A,ld(A,A)),ld(A,ld(A,A)))))) = A,
inference(paramod,[status(thm)],[c_5030,c_11783]) ).
cnf(c_11785,plain,
mult(ld(A,ld(A,A)),mult(mult(ld(ld(A,ld(A,A)),ld(A,A)),ld(A,A)),ld(ld(A,ld(A,A)),ld(ld(A,ld(A,A)),ld(A,ld(A,A)))))) = A,
inference(paramod,[status(thm)],[c_1,c_11784]) ).
cnf(c_11786,plain,
mult(ld(A,ld(A,A)),mult(mult(mult(A,ld(A,A)),ld(A,A)),ld(ld(A,ld(A,A)),ld(ld(A,ld(A,A)),ld(A,ld(A,A)))))) = A,
inference(paramod,[status(thm)],[c_5030,c_11785]) ).
cnf(c_11787,plain,
mult(ld(A,ld(A,A)),mult(mult(A,ld(A,A)),ld(ld(A,ld(A,A)),ld(ld(A,ld(A,A)),ld(A,ld(A,A)))))) = A,
inference(paramod,[status(thm)],[c_1,c_11786]) ).
cnf(c_11788,plain,
mult(ld(A,ld(A,A)),mult(A,ld(ld(A,ld(A,A)),ld(ld(A,ld(A,A)),ld(A,ld(A,A)))))) = A,
inference(paramod,[status(thm)],[c_1,c_11787]) ).
cnf(c_11789,plain,
mult(ld(A,ld(A,A)),mult(A,ld(ld(A,ld(A,A)),mult(A,ld(A,ld(A,A)))))) = A,
inference(paramod,[status(thm)],[c_5030,c_11788]) ).
cnf(c_11790,plain,
mult(ld(A,ld(A,A)),mult(A,ld(ld(A,ld(A,A)),ld(A,A)))) = A,
inference(paramod,[status(thm)],[c_1,c_11789]) ).
cnf(c_11791,plain,
mult(ld(A,ld(A,A)),mult(A,mult(A,ld(A,A)))) = A,
inference(paramod,[status(thm)],[c_5030,c_11790]) ).
cnf(c_5124,plain,
mult(ld(A,ld(A,A)),mult(A,A)) = A,
inference(paramod,[status(thm)],[c_1,c_11791]) ).
cnf(c_11792,plain,
ld(mult(mult(A,ld(B,ld(B,B))),A),mult(A,ld(B,mult(A,C)))) = C,
inference(paramod,[status(thm)],[c_4759,c_147]) ).
cnf(c_11793,plain,
mult(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),mult(A,ld(B,mult(A,C)))))) = C,
inference(paramod,[status(thm)],[c_5052,c_11792]) ).
cnf(c_11794,plain,
mult(ld(A,ld(A,A)),mult(B,ld(B,mult(A,C)))) = C,
inference(paramod,[status(thm)],[c_5071,c_11793]) ).
cnf(c_5126,plain,
mult(ld(A,ld(A,A)),mult(A,B)) = B,
inference(paramod,[status(thm)],[c_1,c_11794]) ).
cnf(c_11795,plain,
mult(A,ld(B,mult(A,ld(mult(mult(A,ld(B,ld(B,B))),A),C)))) = C,
inference(paramod,[status(thm)],[c_4759,c_130]) ).
cnf(c_11796,plain,
mult(A,ld(B,mult(A,mult(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),C)))))) = C,
inference(paramod,[status(thm)],[c_5052,c_11795]) ).
cnf(c_11797,plain,
mult(A,ld(B,mult(B,mult(ld(A,ld(A,A)),C)))) = C,
inference(paramod,[status(thm)],[c_5075,c_11796]) ).
cnf(c_5128,plain,
mult(A,mult(ld(A,ld(A,A)),B)) = B,
inference(paramod,[status(thm)],[c_2,c_11797]) ).
cnf(c_11798,plain,
mult(mult(ld(A,B),ld(A,ld(A,A))),C) = mult(ld(A,rd(A,A)),mult(B,mult(ld(A,rd(A,A)),C))),
inference(paramod,[status(thm)],[c_4759,c_96]) ).
cnf(c_11799,plain,
mult(mult(ld(A,B),ld(A,ld(A,A))),C) = mult(ld(A,ld(A,A)),mult(B,mult(ld(A,rd(A,A)),C))),
inference(paramod,[status(thm)],[c_4759,c_11798]) ).
cnf(c_5137,plain,
mult(mult(ld(A,B),ld(A,ld(A,A))),C) = mult(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),C))),
inference(paramod,[status(thm)],[c_4759,c_11799]) ).
cnf(c_11800,plain,
mult(mult(A,rd(mult(mult(A,B),mult(mult(ld(mult(A,B),ld(mult(A,B),mult(A,B))),B),ld(mult(A,B),ld(mult(A,B),mult(A,B))))),mult(A,mult(A,rd(C,mult(A,C)))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_5038,c_3933]) ).
cnf(c_11801,plain,
mult(mult(A,rd(ld(A,ld(A,A)),mult(A,mult(A,rd(C,mult(A,C)))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_5121,c_11800]) ).
cnf(c_11802,plain,
mult(mult(A,rd(ld(A,ld(A,A)),mult(A,mult(A,mult(mult(A,C),mult(mult(ld(mult(A,C),ld(mult(A,C),mult(A,C))),C),ld(mult(A,C),ld(mult(A,C),mult(A,C))))))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_5038,c_11801]) ).
cnf(c_11803,plain,
mult(mult(A,rd(ld(A,ld(A,A)),mult(A,mult(A,ld(A,ld(A,A)))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_5121,c_11802]) ).
cnf(c_11804,plain,
mult(mult(A,rd(ld(A,ld(A,A)),mult(A,ld(A,A)))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_1,c_11803]) ).
cnf(c_11805,plain,
mult(mult(A,rd(ld(A,ld(A,A)),A)),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_1,c_11804]) ).
cnf(c_11806,plain,
mult(mult(A,mult(A,mult(mult(ld(A,ld(A,A)),ld(A,ld(A,A))),ld(A,ld(A,A))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_5038,c_11805]) ).
cnf(c_11807,plain,
mult(mult(A,mult(A,mult(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,ld(A,A)),ld(A,ld(A,A))))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_5137,c_11806]) ).
cnf(c_11808,plain,
mult(mult(A,mult(A,mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),ld(A,ld(A,A)))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_5061,c_11807]) ).
cnf(c_11809,plain,
mult(mult(A,mult(ld(A,ld(A,A)),ld(A,ld(A,A)))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_5128,c_11808]) ).
cnf(c_11810,plain,
mult(ld(A,ld(A,A)),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
inference(paramod,[status(thm)],[c_5128,c_11809]) ).
cnf(c_11811,plain,
mult(ld(A,ld(A,A)),A) = mult(ld(A,A),mult(A,mult(mult(A,C),mult(mult(ld(mult(A,C),ld(mult(A,C),mult(A,C))),C),ld(mult(A,C),ld(mult(A,C),mult(A,C))))))),
inference(paramod,[status(thm)],[c_5038,c_11810]) ).
cnf(c_11812,plain,
mult(ld(A,ld(A,A)),A) = mult(ld(A,A),mult(A,ld(A,ld(A,A)))),
inference(paramod,[status(thm)],[c_5121,c_11811]) ).
cnf(c_5140,plain,
mult(ld(A,ld(A,A)),A) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_1,c_11812]) ).
cnf(c_11813,plain,
ld(mult(rd(mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))),mult(C,rd(D,mult(B,D)))),C),E) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_5038,c_4669]) ).
cnf(c_11814,plain,
ld(mult(rd(ld(B,ld(B,B)),mult(C,rd(D,mult(B,D)))),C),E) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_5121,c_11813]) ).
cnf(c_11815,plain,
ld(mult(rd(ld(B,ld(B,B)),mult(C,mult(mult(B,D),mult(mult(ld(mult(B,D),ld(mult(B,D),mult(B,D))),D),ld(mult(B,D),ld(mult(B,D),mult(B,D))))))),C),E) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_5038,c_11814]) ).
cnf(c_11816,plain,
ld(mult(rd(ld(B,ld(B,B)),mult(C,ld(B,ld(B,B)))),C),E) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_5121,c_11815]) ).
cnf(c_11817,plain,
ld(mult(mult(mult(C,ld(B,ld(B,B))),mult(mult(ld(mult(C,ld(B,ld(B,B))),ld(mult(C,ld(B,ld(B,B))),mult(C,ld(B,ld(B,B))))),ld(B,ld(B,B))),ld(mult(C,ld(B,ld(B,B))),ld(mult(C,ld(B,ld(B,B))),mult(C,ld(B,ld(B,B))))))),C),E) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_5038,c_11816]) ).
cnf(c_11818,plain,
ld(mult(ld(C,ld(C,C)),C),E) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_5121,c_11817]) ).
cnf(c_11819,plain,
ld(mult(ld(C,C),ld(C,C)),E) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_5140,c_11818]) ).
cnf(c_11820,plain,
ld(ld(C,C),mult(ld(ld(C,C),ld(C,C)),ld(ld(C,C),E))) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_1394,c_11819]) ).
cnf(c_11821,plain,
ld(ld(C,C),mult(mult(ld(C,C),ld(C,C)),ld(ld(C,C),E))) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_510,c_11820]) ).
cnf(c_11822,plain,
ld(ld(C,C),mult(mult(ld(C,C),ld(C,C)),mult(ld(C,C),E))) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_510,c_11821]) ).
cnf(c_11823,plain,
mult(ld(ld(C,C),ld(C,C)),mult(ld(C,C),mult(ld(C,C),E))) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_17,c_11822]) ).
cnf(c_11824,plain,
mult(mult(ld(C,C),ld(C,C)),mult(ld(C,C),mult(ld(C,C),E))) = mult(ld(C,C),E),
inference(paramod,[status(thm)],[c_510,c_11823]) ).
cnf(c_5145,plain,
mult(mult(ld(A,A),ld(A,A)),B) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_514,c_11824]) ).
cnf(c_11825,plain,
mult(rd(A,mult(mult(C,B),mult(mult(ld(mult(C,B),ld(mult(C,B),mult(C,B))),B),ld(mult(C,B),ld(mult(C,B),mult(C,B)))))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_5038,c_3097]) ).
cnf(c_11826,plain,
mult(rd(A,ld(C,ld(C,C))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_5121,c_11825]) ).
cnf(c_11827,plain,
mult(mult(ld(C,ld(C,C)),mult(mult(ld(ld(C,ld(C,C)),ld(ld(C,ld(C,C)),ld(C,ld(C,C)))),A),ld(ld(C,ld(C,C)),ld(ld(C,ld(C,C)),ld(C,ld(C,C)))))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_5038,c_11826]) ).
cnf(c_11828,plain,
mult(mult(ld(C,ld(C,C)),mult(mult(ld(ld(C,ld(C,C)),mult(C,ld(C,ld(C,C)))),A),ld(ld(C,ld(C,C)),ld(ld(C,ld(C,C)),ld(C,ld(C,C)))))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_5030,c_11827]) ).
cnf(c_11829,plain,
mult(mult(ld(C,ld(C,C)),mult(mult(ld(ld(C,ld(C,C)),ld(C,C)),A),ld(ld(C,ld(C,C)),ld(ld(C,ld(C,C)),ld(C,ld(C,C)))))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_1,c_11828]) ).
cnf(c_11830,plain,
mult(mult(ld(C,ld(C,C)),mult(mult(mult(C,ld(C,C)),A),ld(ld(C,ld(C,C)),ld(ld(C,ld(C,C)),ld(C,ld(C,C)))))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_5030,c_11829]) ).
cnf(c_11831,plain,
mult(mult(ld(C,ld(C,C)),mult(mult(C,A),ld(ld(C,ld(C,C)),ld(ld(C,ld(C,C)),ld(C,ld(C,C)))))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_1,c_11830]) ).
cnf(c_11832,plain,
mult(mult(ld(C,ld(C,C)),mult(mult(C,A),ld(ld(C,ld(C,C)),mult(C,ld(C,ld(C,C)))))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_5030,c_11831]) ).
cnf(c_11833,plain,
mult(mult(ld(C,ld(C,C)),mult(mult(C,A),ld(ld(C,ld(C,C)),ld(C,C)))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_1,c_11832]) ).
cnf(c_11834,plain,
mult(mult(ld(C,ld(C,C)),mult(mult(C,A),mult(C,ld(C,C)))),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_5030,c_11833]) ).
cnf(c_11835,plain,
mult(mult(ld(C,ld(C,C)),mult(mult(C,A),C)),rd(D,mult(C,D))) = A,
inference(paramod,[status(thm)],[c_1,c_11834]) ).
cnf(c_11836,plain,
mult(mult(ld(C,ld(C,C)),mult(mult(C,A),C)),mult(mult(C,D),mult(mult(ld(mult(C,D),ld(mult(C,D),mult(C,D))),D),ld(mult(C,D),ld(mult(C,D),mult(C,D)))))) = A,
inference(paramod,[status(thm)],[c_5038,c_11835]) ).
cnf(c_5148,plain,
mult(mult(ld(A,ld(A,A)),mult(mult(A,B),A)),ld(A,ld(A,A))) = B,
inference(paramod,[status(thm)],[c_5121,c_11836]) ).
cnf(c_5151,plain,
ld(mult(A,A),B) = mult(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,ld(A,A)),B))),
inference(paramod,[status(thm)],[c_4828,c_1394]) ).
cnf(c_11837,plain,
mult(mult(mult(mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))),B),ld(B,B)),ld(B,B)) = ld(B,B),
inference(paramod,[status(thm)],[c_5038,c_4643]) ).
cnf(c_11838,plain,
mult(mult(mult(ld(B,ld(B,B)),B),ld(B,B)),ld(B,B)) = ld(B,B),
inference(paramod,[status(thm)],[c_5121,c_11837]) ).
cnf(c_11839,plain,
mult(mult(mult(ld(B,B),ld(B,B)),ld(B,B)),ld(B,B)) = ld(B,B),
inference(paramod,[status(thm)],[c_5140,c_11838]) ).
cnf(c_11840,plain,
mult(mult(ld(B,B),ld(B,B)),ld(B,B)) = ld(B,B),
inference(paramod,[status(thm)],[c_5145,c_11839]) ).
cnf(c_5152,plain,
mult(ld(A,A),ld(A,A)) = ld(A,A),
inference(paramod,[status(thm)],[c_5145,c_11840]) ).
cnf(c_11841,plain,
mult(mult(mult(mult(B,B),A),mult(mult(ld(mult(mult(B,B),A),ld(mult(mult(B,B),A),mult(mult(B,B),A))),A),ld(mult(mult(B,B),A),ld(mult(mult(B,B),A),mult(mult(B,B),A))))),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5038,c_1405]) ).
cnf(c_11842,plain,
mult(ld(mult(B,B),ld(mult(B,B),mult(B,B))),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5121,c_11841]) ).
cnf(c_11843,plain,
mult(ld(mult(B,B),mult(ld(B,ld(B,B)),mult(ld(B,B),mult(ld(B,ld(B,B)),mult(B,B))))),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5151,c_11842]) ).
cnf(c_11844,plain,
mult(ld(mult(B,B),mult(ld(B,ld(B,B)),mult(ld(B,B),B))),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5124,c_11843]) ).
cnf(c_11845,plain,
mult(ld(mult(B,B),mult(ld(B,ld(B,B)),B)),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_4772,c_11844]) ).
cnf(c_11846,plain,
mult(ld(mult(B,B),mult(ld(B,B),ld(B,B))),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5140,c_11845]) ).
cnf(c_11847,plain,
mult(ld(mult(B,B),ld(B,B)),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5152,c_11846]) ).
cnf(c_11848,plain,
mult(mult(ld(B,ld(B,B)),mult(ld(B,B),mult(ld(B,ld(B,B)),ld(B,B)))),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5151,c_11847]) ).
cnf(c_11849,plain,
mult(mult(ld(B,ld(B,B)),mult(ld(B,B),mult(ld(B,B),ld(B,ld(B,B))))),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5013,c_11848]) ).
cnf(c_11850,plain,
mult(mult(ld(B,ld(B,B)),mult(ld(B,B),ld(B,ld(B,B)))),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5024,c_11849]) ).
cnf(c_11851,plain,
mult(mult(ld(B,ld(B,B)),ld(B,ld(B,B))),mult(B,C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5024,c_11850]) ).
cnf(c_11852,plain,
mult(ld(B,ld(B,B)),mult(ld(B,B),mult(ld(B,ld(B,B)),mult(B,C)))) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5137,c_11851]) ).
cnf(c_11853,plain,
mult(ld(B,ld(B,B)),mult(ld(B,B),C)) = ld(B,mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_5126,c_11852]) ).
cnf(c_5161,plain,
ld(A,mult(ld(A,A),B)) = mult(ld(A,ld(A,A)),mult(ld(A,A),B)),
inference(copy,[status(thm)],[c_11853]) ).
cnf(c_5206,plain,
mult(ld(A,ld(A,A)),mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(A,ld(A,A)),B)),
inference(paramod,[status(thm)],[c_5024,c_4859]) ).
cnf(c_5207,plain,
mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_5024,c_4850]) ).
cnf(c_5215,plain,
ld(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(A,ld(A,A)),B)),
inference(paramod,[status(thm)],[c_5206,c_5161]) ).
cnf(c_5216,plain,
ld(mult(A,A),B) = mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),B))),
inference(paramod,[status(thm)],[c_5206,c_5151]) ).
cnf(c_11854,plain,
mult(mult(A,A),ld(A,ld(A,A))) = mult(A,ld(A,A)),
inference(paramod,[status(thm)],[c_5152,c_16]) ).
cnf(c_5232,plain,
mult(mult(A,A),ld(A,ld(A,A))) = A,
inference(paramod,[status(thm)],[c_1,c_11854]) ).
cnf(c_11855,plain,
mult(mult(mult(A,A),ld(A,ld(A,A))),ld(ld(A,A),B)) = mult(mult(ld(A,A),ld(A,A)),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
inference(paramod,[status(thm)],[c_5152,c_41]) ).
cnf(c_11856,plain,
mult(A,ld(ld(A,A),B)) = mult(mult(ld(A,A),ld(A,A)),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
inference(paramod,[status(thm)],[c_5232,c_11855]) ).
cnf(c_11857,plain,
mult(A,mult(ld(A,A),B)) = mult(mult(ld(A,A),ld(A,A)),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
inference(paramod,[status(thm)],[c_510,c_11856]) ).
cnf(c_11858,plain,
mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
inference(paramod,[status(thm)],[c_5152,c_11857]) ).
cnf(c_11859,plain,
mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(ld(A,A),A),B)),
inference(paramod,[status(thm)],[c_5152,c_11858]) ).
cnf(c_11860,plain,
mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(mult(ld(A,A),A),B)),
inference(paramod,[status(thm)],[c_510,c_11859]) ).
cnf(c_11861,plain,
mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(A,B)),
inference(paramod,[status(thm)],[c_4772,c_11860]) ).
cnf(c_5239,plain,
mult(ld(A,A),mult(A,B)) = mult(A,mult(ld(A,A),B)),
inference(copy,[status(thm)],[c_11861]) ).
cnf(c_5255,plain,
mult(mult(ld(A,ld(A,A)),A),mult(ld(A,A),B)) = B,
inference(paramod,[status(thm)],[c_4833,c_514]) ).
cnf(c_5286,plain,
mult(mult(ld(A,ld(A,A)),ld(A,A)),B) = ld(A,B),
inference(paramod,[status(thm)],[c_4833,c_4833]) ).
cnf(c_11862,plain,
ld(A,ld(B,C)) = mult(B,ld(mult(mult(B,A),B),C)),
inference(paramod,[status(thm)],[c_119,c_2]) ).
cnf(c_5305,plain,
mult(A,ld(mult(mult(A,B),A),C)) = ld(B,ld(A,C)),
inference(copy,[status(thm)],[c_11862]) ).
cnf(c_11863,plain,
mult(A,mult(ld(A,B),ld(mult(A,mult(ld(A,ld(A,B)),B)),C))) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_16,c_119]) ).
cnf(c_11864,plain,
mult(A,mult(ld(A,B),ld(mult(mult(ld(A,B),A),ld(A,B)),C))) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_345,c_11863]) ).
cnf(c_11865,plain,
mult(A,ld(A,ld(ld(A,B),C))) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_5305,c_11864]) ).
cnf(c_11866,plain,
mult(A,ld(mult(B,A),mult(A,C))) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_1258,c_11865]) ).
cnf(c_5310,plain,
ld(ld(A,B),C) = mult(A,ld(mult(B,A),mult(A,C))),
inference(copy,[status(thm)],[c_11866]) ).
cnf(c_11867,plain,
mult(A,mult(ld(A,A),ld(mult(A,ld(A,A)),B))) = ld(ld(A,A),B),
inference(paramod,[status(thm)],[c_4772,c_119]) ).
cnf(c_11868,plain,
mult(A,mult(ld(A,A),ld(A,B))) = ld(ld(A,A),B),
inference(paramod,[status(thm)],[c_1,c_11867]) ).
cnf(c_5323,plain,
mult(A,mult(ld(A,A),ld(A,B))) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_510,c_11868]) ).
cnf(c_11869,plain,
ld(ld(ld(A,A),B),mult(ld(A,A),C)) = mult(ld(A,A),ld(mult(B,ld(A,A)),C)),
inference(paramod,[status(thm)],[c_514,c_5310]) ).
cnf(c_11870,plain,
ld(mult(A,ld(mult(A,A),mult(A,B))),mult(ld(A,A),C)) = mult(ld(A,A),ld(mult(B,ld(A,A)),C)),
inference(paramod,[status(thm)],[c_5310,c_11869]) ).
cnf(c_11871,plain,
ld(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B))))),mult(ld(A,A),C)) = mult(ld(A,A),ld(mult(B,ld(A,A)),C)),
inference(paramod,[status(thm)],[c_5216,c_11870]) ).
cnf(c_11872,plain,
ld(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))),mult(ld(A,A),C)) = mult(ld(A,A),ld(mult(B,ld(A,A)),C)),
inference(paramod,[status(thm)],[c_5126,c_11871]) ).
cnf(c_11873,plain,
ld(mult(ld(A,A),B),mult(ld(A,A),C)) = mult(ld(A,A),ld(mult(B,ld(A,A)),C)),
inference(paramod,[status(thm)],[c_5207,c_11872]) ).
cnf(c_5405,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),C)) = ld(mult(ld(A,A),B),mult(ld(A,A),C)),
inference(copy,[status(thm)],[c_11873]) ).
cnf(c_11874,plain,
mult(mult(A,ld(mult(B,A),mult(A,ld(A,B)))),ld(A,B)) = ld(A,B),
inference(paramod,[status(thm)],[c_5310,c_4772]) ).
cnf(c_5414,plain,
mult(mult(A,ld(mult(B,A),B)),ld(A,B)) = ld(A,B),
inference(paramod,[status(thm)],[c_1,c_11874]) ).
cnf(c_11875,plain,
ld(mult(ld(A,ld(A,A)),B),C) = mult(A,ld(mult(B,A),mult(A,C))),
inference(paramod,[status(thm)],[c_4833,c_5310]) ).
cnf(c_5423,plain,
mult(A,ld(mult(B,A),mult(A,C))) = ld(mult(ld(A,ld(A,A)),B),C),
inference(copy,[status(thm)],[c_11875]) ).
cnf(c_5426,plain,
ld(mult(A,ld(mult(B,A),mult(A,C))),D) = mult(ld(A,B),ld(mult(C,ld(A,B)),mult(ld(A,B),D))),
inference(paramod,[status(thm)],[c_5310,c_5310]) ).
cnf(c_5518,plain,
ld(mult(mult(A,B),A),mult(A,C)) = ld(A,ld(B,C)),
inference(paramod,[status(thm)],[c_1,c_131]) ).
cnf(c_11876,plain,
mult(mult(A,ld(mult(B,A),mult(A,ld(A,B)))),mult(ld(A,B),C)) = mult(ld(A,B),mult(ld(ld(A,B),ld(A,B)),C)),
inference(paramod,[status(thm)],[c_5310,c_5239]) ).
cnf(c_11877,plain,
mult(mult(A,ld(mult(B,A),B)),mult(ld(A,B),C)) = mult(ld(A,B),mult(ld(ld(A,B),ld(A,B)),C)),
inference(paramod,[status(thm)],[c_1,c_11876]) ).
cnf(c_11878,plain,
mult(mult(A,ld(mult(B,A),B)),mult(ld(A,B),C)) = mult(ld(A,B),mult(mult(A,ld(mult(B,A),mult(A,ld(A,B)))),C)),
inference(paramod,[status(thm)],[c_5310,c_11877]) ).
cnf(c_5634,plain,
mult(mult(A,ld(mult(B,A),B)),mult(ld(A,B),C)) = mult(ld(A,B),mult(mult(A,ld(mult(B,A),B)),C)),
inference(paramod,[status(thm)],[c_1,c_11878]) ).
cnf(c_5661,plain,
ld(mult(A,ld(mult(B,A),B)),ld(A,B)) = ld(A,B),
inference(paramod,[status(thm)],[c_5414,c_2]) ).
cnf(c_5713,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)))),
inference(paramod,[status(thm)],[c_515,c_516]) ).
cnf(c_5717,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),mult(ld(A,A),C))) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_516,c_516]) ).
cnf(c_5747,plain,
ld(mult(mult(A,B),A),C) = ld(A,ld(B,ld(A,C))),
inference(paramod,[status(thm)],[c_1,c_5518]) ).
cnf(c_11879,plain,
ld(mult(A,ld(B,B)),mult(ld(B,B),C)) = ld(ld(B,B),ld(mult(ld(B,B),A),C)),
inference(paramod,[status(thm)],[c_514,c_5518]) ).
cnf(c_11880,plain,
ld(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(B,ld(mult(B,B),mult(B,ld(mult(ld(B,B),A),C)))),
inference(paramod,[status(thm)],[c_5310,c_11879]) ).
cnf(c_11881,plain,
ld(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(B,mult(ld(B,B),mult(ld(B,ld(B,B)),mult(ld(B,ld(B,B)),mult(B,ld(mult(ld(B,B),A),C)))))),
inference(paramod,[status(thm)],[c_5216,c_11880]) ).
cnf(c_11882,plain,
ld(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(B,mult(ld(B,B),mult(ld(B,ld(B,B)),ld(mult(ld(B,B),A),C)))),
inference(paramod,[status(thm)],[c_5126,c_11881]) ).
cnf(c_11883,plain,
ld(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),ld(mult(ld(B,B),A),C)),
inference(paramod,[status(thm)],[c_5207,c_11882]) ).
cnf(c_5755,plain,
mult(ld(A,A),ld(mult(ld(A,A),B),C)) = ld(mult(B,ld(A,A)),mult(ld(A,A),C)),
inference(copy,[status(thm)],[c_11883]) ).
cnf(c_11884,plain,
ld(mult(ld(A,B),mult(A,ld(mult(B,A),B))),mult(mult(A,ld(mult(B,A),B)),mult(ld(A,B),C))) = ld(mult(A,ld(mult(B,A),B)),C),
inference(paramod,[status(thm)],[c_5661,c_24]) ).
cnf(c_11885,plain,
ld(ld(A,B),mult(mult(A,ld(mult(B,A),B)),mult(ld(A,B),C))) = ld(mult(A,ld(mult(B,A),B)),C),
inference(paramod,[status(thm)],[c_547,c_11884]) ).
cnf(c_11886,plain,
ld(ld(A,B),mult(ld(A,B),mult(mult(A,ld(mult(B,A),B)),C))) = ld(mult(A,ld(mult(B,A),B)),C),
inference(paramod,[status(thm)],[c_5634,c_11885]) ).
cnf(c_11887,plain,
mult(mult(A,ld(mult(B,A),B)),C) = ld(mult(A,ld(mult(B,A),B)),C),
inference(paramod,[status(thm)],[c_2,c_11886]) ).
cnf(c_5790,plain,
ld(mult(A,ld(mult(B,A),B)),C) = mult(mult(A,ld(mult(B,A),B)),C),
inference(copy,[status(thm)],[c_11887]) ).
cnf(c_11888,plain,
ld(mult(A,B),mult(B,C)) = ld(B,mult(ld(ld(B,A),ld(ld(B,A),ld(B,A))),C)),
inference(paramod,[status(thm)],[c_5128,c_24]) ).
cnf(c_11889,plain,
ld(mult(A,B),mult(B,C)) = ld(B,mult(ld(ld(B,A),mult(B,ld(mult(A,B),mult(B,ld(B,A))))),C)),
inference(paramod,[status(thm)],[c_5310,c_11888]) ).
cnf(c_11890,plain,
ld(mult(A,B),mult(B,C)) = ld(B,mult(ld(ld(B,A),mult(B,ld(mult(A,B),A))),C)),
inference(paramod,[status(thm)],[c_1,c_11889]) ).
cnf(c_5804,plain,
ld(mult(A,B),mult(B,C)) = ld(B,mult(mult(B,ld(mult(A,B),mult(B,mult(B,ld(mult(A,B),A))))),C)),
inference(paramod,[status(thm)],[c_5310,c_11890]) ).
cnf(c_11891,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),ld(ld(A,A),C))) = ld(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_1,c_5405]) ).
cnf(c_11892,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),mult(A,ld(mult(A,A),mult(A,C))))) = ld(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_5310,c_11891]) ).
cnf(c_11893,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,C))))))) = ld(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_5216,c_11892]) ).
cnf(c_11894,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),C))))) = ld(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_5126,c_11893]) ).
cnf(c_5821,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),mult(ld(A,A),C))) = ld(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_5207,c_11894]) ).
cnf(c_11895,plain,
ld(ld(A,A),ld(mult(ld(A,A),B),mult(ld(A,A),C))) = ld(mult(B,ld(A,A)),C),
inference(paramod,[status(thm)],[c_5405,c_2]) ).
cnf(c_11896,plain,
mult(A,ld(mult(A,A),mult(A,ld(mult(ld(A,A),B),mult(ld(A,A),C))))) = ld(mult(B,ld(A,A)),C),
inference(paramod,[status(thm)],[c_5310,c_11895]) ).
cnf(c_11897,plain,
mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,ld(mult(ld(A,A),B),mult(ld(A,A),C))))))) = ld(mult(B,ld(A,A)),C),
inference(paramod,[status(thm)],[c_5216,c_11896]) ).
cnf(c_11898,plain,
mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,A),B),mult(ld(A,A),C))))) = ld(mult(B,ld(A,A)),C),
inference(paramod,[status(thm)],[c_5126,c_11897]) ).
cnf(c_5822,plain,
mult(ld(A,A),ld(mult(ld(A,A),B),mult(ld(A,A),C))) = ld(mult(B,ld(A,A)),C),
inference(paramod,[status(thm)],[c_5207,c_11898]) ).
cnf(c_11899,plain,
mult(ld(A,A),ld(mult(ld(mult(ld(A,A),B),mult(ld(A,A),C)),ld(A,A)),mult(ld(A,A),D))) = ld(ld(mult(B,ld(A,A)),C),D),
inference(paramod,[status(thm)],[c_5822,c_5821]) ).
cnf(c_6092,plain,
mult(ld(A,A),ld(mult(ld(mult(ld(A,A),B),mult(ld(A,A),C)),ld(A,A)),mult(ld(A,A),D))) = mult(mult(B,ld(A,A)),ld(mult(C,mult(B,ld(A,A))),mult(mult(B,ld(A,A)),D))),
inference(paramod,[status(thm)],[c_5310,c_11899]) ).
cnf(c_11900,plain,
mult(ld(A,B),ld(mult(C,ld(A,B)),mult(ld(A,B),D))) = ld(mult(ld(ld(A,B),mult(A,ld(mult(B,A),mult(A,ld(A,B))))),C),D),
inference(paramod,[status(thm)],[c_5310,c_5423]) ).
cnf(c_11901,plain,
mult(ld(A,B),ld(mult(C,ld(A,B)),mult(ld(A,B),D))) = ld(mult(ld(ld(A,B),mult(A,ld(mult(B,A),B))),C),D),
inference(paramod,[status(thm)],[c_1,c_11900]) ).
cnf(c_6134,plain,
mult(ld(A,B),ld(mult(C,ld(A,B)),mult(ld(A,B),D))) = ld(mult(mult(A,ld(mult(B,A),mult(A,mult(A,ld(mult(B,A),B))))),C),D),
inference(paramod,[status(thm)],[c_5310,c_11901]) ).
cnf(c_11902,plain,
mult(mult(ld(A,ld(A,A)),B),mult(ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),B)),ld(mult(ld(A,ld(A,A)),B),C))) = mult(mult(A,ld(mult(B,A),mult(A,mult(ld(A,ld(A,A)),B)))),C),
inference(paramod,[status(thm)],[c_5423,c_5323]) ).
cnf(c_11903,plain,
mult(ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),B)),C) = mult(mult(A,ld(mult(B,A),mult(A,mult(ld(A,ld(A,A)),B)))),C),
inference(paramod,[status(thm)],[c_5323,c_11902]) ).
cnf(c_11904,plain,
mult(ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),B)),C) = mult(mult(A,ld(mult(B,A),B)),C),
inference(paramod,[status(thm)],[c_5128,c_11903]) ).
cnf(c_6135,plain,
mult(mult(A,ld(mult(B,A),B)),C) = mult(ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),B)),C),
inference(copy,[status(thm)],[c_11904]) ).
cnf(c_11905,plain,
ld(mult(ld(A,B),ld(B,A)),C) = mult(mult(ld(A,B),ld(mult(A,ld(A,B)),A)),C),
inference(paramod,[status(thm)],[c_1,c_5790]) ).
cnf(c_6176,plain,
ld(mult(ld(A,B),ld(B,A)),C) = mult(mult(ld(A,B),ld(B,A)),C),
inference(paramod,[status(thm)],[c_1,c_11905]) ).
cnf(c_6435,plain,
mult(ld(A,ld(A,A)),ld(B,C)) = ld(A,mult(ld(B,ld(B,B)),C)),
inference(paramod,[status(thm)],[c_5039,c_4833]) ).
cnf(c_11906,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),C)) = mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(mult(B,ld(A,A)),mult(ld(A,A),mult(ld(A,A),B))),C)),
inference(paramod,[status(thm)],[c_5755,c_575]) ).
cnf(c_6596,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),C)) = mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(mult(B,ld(A,A)),B),C)),
inference(paramod,[status(thm)],[c_514,c_11906]) ).
cnf(c_6608,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_575,c_575]) ).
cnf(c_11907,plain,
ld(mult(A,ld(B,ld(B,B))),C) = ld(ld(B,ld(B,B)),ld(mult(B,A),ld(ld(B,ld(B,B)),C))),
inference(paramod,[status(thm)],[c_5126,c_5747]) ).
cnf(c_11908,plain,
ld(mult(A,ld(B,ld(B,B))),C) = ld(ld(B,ld(B,B)),ld(mult(B,A),mult(B,ld(mult(ld(B,B),B),mult(B,C))))),
inference(paramod,[status(thm)],[c_5310,c_11907]) ).
cnf(c_11909,plain,
ld(mult(A,ld(B,ld(B,B))),C) = ld(ld(B,ld(B,B)),ld(mult(B,A),mult(B,ld(B,mult(B,C))))),
inference(paramod,[status(thm)],[c_4772,c_11908]) ).
cnf(c_11910,plain,
ld(mult(A,ld(B,ld(B,B))),C) = ld(ld(B,ld(B,B)),ld(mult(B,A),mult(B,C))),
inference(paramod,[status(thm)],[c_2,c_11909]) ).
cnf(c_11911,plain,
ld(mult(A,ld(B,ld(B,B))),C) = mult(B,ld(mult(ld(B,B),B),mult(B,ld(mult(B,A),mult(B,C))))),
inference(paramod,[status(thm)],[c_5310,c_11910]) ).
cnf(c_11912,plain,
ld(mult(A,ld(B,ld(B,B))),C) = mult(B,ld(B,mult(B,ld(mult(B,A),mult(B,C))))),
inference(paramod,[status(thm)],[c_4772,c_11911]) ).
cnf(c_11913,plain,
ld(mult(A,ld(B,ld(B,B))),C) = mult(B,ld(mult(B,A),mult(B,C))),
inference(paramod,[status(thm)],[c_2,c_11912]) ).
cnf(c_6906,plain,
mult(A,ld(mult(A,B),mult(A,C))) = ld(mult(B,ld(A,ld(A,A))),C),
inference(copy,[status(thm)],[c_11913]) ).
cnf(c_7095,plain,
ld(mult(A,ld(mult(B,A),C)),D) = mult(ld(A,B),ld(mult(ld(A,C),ld(A,B)),mult(ld(A,B),D))),
inference(paramod,[status(thm)],[c_1,c_5426]) ).
cnf(c_7120,plain,
mult(ld(A,A),ld(mult(ld(mult(ld(B,B),ld(A,A)),C),ld(A,A)),D)) = ld(mult(mult(ld(B,B),ld(A,A)),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_1111,c_5405]) ).
cnf(c_7174,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)))),
inference(paramod,[status(thm)],[c_1245,c_575]) ).
cnf(c_11914,plain,
mult(mult(ld(A,A),B),C) = mult(mult(mult(ld(A,ld(A,A)),ld(A,A)),A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))),
inference(paramod,[status(thm)],[c_5286,c_1245]) ).
cnf(c_7176,plain,
mult(mult(mult(ld(A,ld(A,A)),ld(A,A)),A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))) = mult(mult(ld(A,A),B),C),
inference(copy,[status(thm)],[c_11914]) ).
cnf(c_11915,plain,
ld(A,mult(ld(A,A),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C)))) = mult(ld(A,A),ld(mult(B,ld(ld(A,ld(A,A)),ld(ld(A,ld(A,A)),ld(A,ld(A,A))))),C)),
inference(paramod,[status(thm)],[c_6906,c_5215]) ).
cnf(c_11916,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C)))) = mult(ld(A,A),ld(mult(B,ld(ld(A,ld(A,A)),ld(ld(A,ld(A,A)),ld(A,ld(A,A))))),C)),
inference(paramod,[status(thm)],[c_5215,c_11915]) ).
cnf(c_11917,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C)))) = mult(ld(A,A),ld(mult(B,ld(ld(A,ld(A,A)),mult(A,ld(mult(ld(A,A),A),mult(A,ld(A,ld(A,A))))))),C)),
inference(paramod,[status(thm)],[c_5310,c_11916]) ).
cnf(c_11918,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C)))) = mult(ld(A,A),ld(mult(B,ld(ld(A,ld(A,A)),mult(A,ld(A,mult(A,ld(A,ld(A,A))))))),C)),
inference(paramod,[status(thm)],[c_4772,c_11917]) ).
cnf(c_11919,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C)))) = mult(ld(A,A),ld(mult(B,ld(ld(A,ld(A,A)),mult(A,ld(A,ld(A,A))))),C)),
inference(paramod,[status(thm)],[c_1,c_11918]) ).
cnf(c_11920,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C)))) = mult(ld(A,A),ld(mult(B,ld(ld(A,ld(A,A)),ld(A,A))),C)),
inference(paramod,[status(thm)],[c_1,c_11919]) ).
cnf(c_11921,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C)))) = mult(ld(A,A),ld(mult(B,mult(A,ld(mult(ld(A,A),A),mult(A,ld(A,A))))),C)),
inference(paramod,[status(thm)],[c_5310,c_11920]) ).
cnf(c_11922,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C)))) = mult(ld(A,A),ld(mult(B,mult(A,ld(A,mult(A,ld(A,A))))),C)),
inference(paramod,[status(thm)],[c_4772,c_11921]) ).
cnf(c_11923,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C)))) = mult(ld(A,A),ld(mult(B,mult(A,ld(A,A))),C)),
inference(paramod,[status(thm)],[c_1,c_11922]) ).
cnf(c_7380,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C)))) = mult(ld(A,A),ld(mult(B,A),C)),
inference(paramod,[status(thm)],[c_1,c_11923]) ).
cnf(c_11924,plain,
mult(mult(ld(A,A),mult(ld(B,B),ld(B,B))),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))))),
inference(paramod,[status(thm)],[c_515,c_1253]) ).
cnf(c_11925,plain,
mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))))),
inference(paramod,[status(thm)],[c_5152,c_11924]) ).
cnf(c_11926,plain,
mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(B,B),mult(ld(B,B),mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),mult(mult(ld(A,A),ld(B,B)),C))))),
inference(paramod,[status(thm)],[c_6608,c_11925]) ).
cnf(c_11927,plain,
mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_514,c_11926]) ).
cnf(c_7516,plain,
mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),mult(mult(ld(A,A),ld(B,B)),C))) = mult(mult(ld(A,A),ld(B,B)),C),
inference(copy,[status(thm)],[c_11927]) ).
cnf(c_11928,plain,
mult(mult(ld(A,A),mult(ld(B,B),ld(B,B))),mult(ld(B,B),C)) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C)))),
inference(paramod,[status(thm)],[c_516,c_1253]) ).
cnf(c_11929,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C)))),
inference(paramod,[status(thm)],[c_5152,c_11928]) ).
cnf(c_11930,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),mult(mult(ld(B,B),ld(A,A)),C)))),
inference(paramod,[status(thm)],[c_6608,c_11929]) ).
cnf(c_7517,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),C)),
inference(paramod,[status(thm)],[c_7516,c_11930]) ).
cnf(c_7537,plain,
mult(ld(mult(ld(A,A),ld(B,C)),ld(A,A)),mult(mult(ld(A,A),ld(B,C)),mult(B,ld(mult(C,B),D)))) = ld(mult(ld(A,A),ld(B,C)),ld(B,D)),
inference(paramod,[status(thm)],[c_547,c_1254]) ).
cnf(c_11931,plain,
mult(ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),ld(A,A)),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5414,c_1254]) ).
cnf(c_11932,plain,
mult(mult(ld(ld(A,A),B),ld(mult(ld(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_7095,c_11931]) ).
cnf(c_11933,plain,
mult(mult(mult(A,ld(mult(A,A),mult(A,B))),ld(mult(ld(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5310,c_11932]) ).
cnf(c_11934,plain,
mult(mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B))))),ld(mult(ld(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5216,c_11933]) ).
cnf(c_11935,plain,
mult(mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))),ld(mult(ld(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5126,c_11934]) ).
cnf(c_11936,plain,
mult(mult(mult(ld(A,A),B),ld(mult(ld(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5207,c_11935]) ).
cnf(c_11937,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(A,ld(mult(A,A),mult(A,B))),ld(ld(A,A),B)),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5310,c_11936]) ).
cnf(c_11938,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B))))),ld(ld(A,A),B)),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5216,c_11937]) ).
cnf(c_11939,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))),ld(ld(A,A),B)),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5126,c_11938]) ).
cnf(c_11940,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5207,c_11939]) ).
cnf(c_11941,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(A,ld(mult(A,A),mult(A,B)))),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5310,c_11940]) ).
cnf(c_11942,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B)))))),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5216,c_11941]) ).
cnf(c_11943,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B)))),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5126,c_11942]) ).
cnf(c_11944,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5207,c_11943]) ).
cnf(c_11945,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(ld(A,A),B)),mult(mult(A,ld(mult(A,A),mult(A,B))),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5310,c_11944]) ).
cnf(c_11946,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(ld(A,A),B)),mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B))))),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5216,c_11945]) ).
cnf(c_11947,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(ld(A,A),B)),mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5126,c_11946]) ).
cnf(c_11948,plain,
mult(mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(ld(A,A),B)),mult(mult(ld(A,A),B),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5207,c_11947]) ).
cnf(c_11949,plain,
mult(mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(mult(ld(A,A),B),ld(mult(ld(A,A),B),mult(ld(A,A),B))),mult(ld(mult(ld(A,A),B),ld(mult(ld(A,A),B),mult(ld(A,A),B))),mult(mult(ld(A,A),B),ld(A,A)))))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5216,c_11948]) ).
cnf(c_11950,plain,
mult(mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(mult(ld(A,A),B),ld(mult(ld(A,A),B),mult(ld(A,A),B))),ld(A,A)))),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5126,c_11949]) ).
cnf(c_11951,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),ld(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5207,c_11950]) ).
cnf(c_11952,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(A,ld(mult(A,A),mult(A,B)))) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5310,c_11951]) ).
cnf(c_11953,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B)))))) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5216,c_11952]) ).
cnf(c_11954,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B)))) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5126,c_11953]) ).
cnf(c_11955,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),ld(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5207,c_11954]) ).
cnf(c_11956,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),mult(A,ld(mult(A,A),mult(A,B))))),
inference(paramod,[status(thm)],[c_5310,c_11955]) ).
cnf(c_11957,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B))))))),
inference(paramod,[status(thm)],[c_5216,c_11956]) ).
cnf(c_11958,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))))),
inference(paramod,[status(thm)],[c_5126,c_11957]) ).
cnf(c_11959,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = ld(mult(ld(A,A),ld(mult(B,ld(A,A)),B)),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5207,c_11958]) ).
cnf(c_11960,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(ld(ld(A,A),B),ld(mult(ld(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_7095,c_11959]) ).
cnf(c_11961,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(A,ld(mult(A,A),mult(A,B))),ld(mult(ld(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5310,c_11960]) ).
cnf(c_11962,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B))))),ld(mult(ld(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5216,c_11961]) ).
cnf(c_11963,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))),ld(mult(ld(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5126,c_11962]) ).
cnf(c_11964,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(ld(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5207,c_11963]) ).
cnf(c_11965,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(A,ld(mult(A,A),mult(A,B))),ld(ld(A,A),B)),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5310,c_11964]) ).
cnf(c_11966,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B))))),ld(ld(A,A),B)),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5216,c_11965]) ).
cnf(c_11967,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))),ld(ld(A,A),B)),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5126,c_11966]) ).
cnf(c_11968,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),ld(ld(A,A),B)),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5207,c_11967]) ).
cnf(c_11969,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(A,ld(mult(A,A),mult(A,B)))),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5310,c_11968]) ).
cnf(c_11970,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B)))))),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5216,c_11969]) ).
cnf(c_11971,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B)))),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5126,c_11970]) ).
cnf(c_11972,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5207,c_11971]) ).
cnf(c_11973,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(ld(A,A),B)),mult(mult(A,ld(mult(A,A),mult(A,B))),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5310,c_11972]) ).
cnf(c_11974,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(ld(A,A),B)),mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B))))),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5216,c_11973]) ).
cnf(c_11975,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(ld(A,A),B)),mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5126,c_11974]) ).
cnf(c_11976,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),ld(mult(mult(ld(A,A),B),mult(ld(A,A),B)),mult(mult(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5207,c_11975]) ).
cnf(c_11977,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(mult(ld(A,A),B),ld(mult(ld(A,A),B),mult(ld(A,A),B))),mult(ld(mult(ld(A,A),B),ld(mult(ld(A,A),B),mult(ld(A,A),B))),mult(mult(ld(A,A),B),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))))),
inference(paramod,[status(thm)],[c_5216,c_11976]) ).
cnf(c_11978,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(mult(ld(A,A),B),ld(mult(ld(A,A),B),mult(ld(A,A),B))),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))))),
inference(paramod,[status(thm)],[c_5126,c_11977]) ).
cnf(c_7542,plain,
mult(mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),ld(A,A)),mult(ld(A,A),B)) = mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))),
inference(paramod,[status(thm)],[c_5207,c_11978]) ).
cnf(c_11979,plain,
mult(ld(mult(ld(A,A),B),ld(A,A)),mult(B,ld(mult(ld(A,A),B),C))) = ld(mult(ld(A,A),B),mult(B,mult(ld(mult(ld(A,A),B),ld(A,A)),C))),
inference(paramod,[status(thm)],[c_1111,c_1254]) ).
cnf(c_7570,plain,
ld(mult(ld(A,A),B),mult(B,mult(ld(mult(ld(A,A),B),ld(A,A)),C))) = mult(ld(mult(ld(A,A),B),ld(A,A)),mult(B,ld(mult(ld(A,A),B),C))),
inference(copy,[status(thm)],[c_11979]) ).
cnf(c_11980,plain,
mult(A,ld(A,B)) = mult(mult(ld(C,C),A),mult(ld(mult(ld(C,C),A),mult(ld(C,ld(C,C)),C)),mult(A,mult(ld(A,ld(C,C)),B)))),
inference(paramod,[status(thm)],[c_5255,c_35]) ).
cnf(c_11981,plain,
B = mult(mult(ld(C,C),A),mult(ld(mult(ld(C,C),A),mult(ld(C,ld(C,C)),C)),mult(A,mult(ld(A,ld(C,C)),B)))),
inference(paramod,[status(thm)],[c_1,c_11980]) ).
cnf(c_7794,plain,
mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),mult(ld(A,ld(A,A)),A)),mult(B,mult(ld(B,ld(A,A)),C)))) = C,
inference(copy,[status(thm)],[c_11981]) ).
cnf(c_7804,plain,
mult(mult(mult(mult(ld(A,ld(A,A)),ld(A,A)),ld(A,A)),A),mult(ld(A,A),B)) = B,
inference(paramod,[status(thm)],[c_5286,c_5255]) ).
cnf(c_7832,plain,
mult(ld(A,ld(B,B)),mult(ld(B,B),ld(mult(ld(B,B),mult(ld(A,ld(A,A)),ld(A,A))),C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_5286,c_1278]) ).
cnf(c_7839,plain,
mult(ld(A,mult(ld(B,ld(B,B)),B)),mult(ld(B,B),ld(mult(ld(B,B),ld(A,ld(A,A))),C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_6435,c_1278]) ).
cnf(c_11982,plain,
mult(mult(ld(A,A),mult(ld(B,B),ld(B,B))),mult(ld(B,B),ld(mult(ld(B,B),ld(A,A)),C))) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))),
inference(paramod,[status(thm)],[c_1278,c_1253]) ).
cnf(c_11983,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),ld(mult(ld(B,B),ld(A,A)),C))) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))),
inference(paramod,[status(thm)],[c_5152,c_11982]) ).
cnf(c_11984,plain,
mult(ld(B,B),C) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))),
inference(paramod,[status(thm)],[c_1278,c_11983]) ).
cnf(c_11985,plain,
mult(ld(B,B),C) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_6608,c_11984]) ).
cnf(c_7840,plain,
mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),C))) = mult(ld(B,B),C),
inference(copy,[status(thm)],[c_11985]) ).
cnf(c_11986,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)) = mult(ld(B,B),mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_7840,c_7174]) ).
cnf(c_7843,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)) = C,
inference(paramod,[status(thm)],[c_514,c_11986]) ).
cnf(c_11987,plain,
C = mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(mult(B,ld(A,A)),B),C)),
inference(paramod,[status(thm)],[c_7843,c_6596]) ).
cnf(c_7846,plain,
mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(mult(B,ld(A,A)),B),C)) = C,
inference(copy,[status(thm)],[c_11987]) ).
cnf(c_7847,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_7843,c_5713]) ).
cnf(c_11988,plain,
mult(ld(A,A),mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),B)) = mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),mult(ld(mult(B,ld(A,A)),B),mult(ld(A,A),B))),
inference(paramod,[status(thm)],[c_7847,c_7542]) ).
cnf(c_7848,plain,
mult(ld(A,A),mult(ld(mult(ld(A,A),B),mult(ld(A,A),B)),B)) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_7846,c_11988]) ).
cnf(c_11989,plain,
mult(ld(B,B),mult(ld(A,A),C)) = mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),C)),
inference(paramod,[status(thm)],[c_7847,c_7517]) ).
cnf(c_7850,plain,
mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),C)) = mult(ld(B,B),mult(ld(A,A),C)),
inference(copy,[status(thm)],[c_11989]) ).
cnf(c_11990,plain,
mult(ld(B,B),mult(ld(A,A),mult(ld(A,A),C))) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_7847,c_5717]) ).
cnf(c_11991,plain,
mult(ld(B,B),C) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_514,c_11990]) ).
cnf(c_7851,plain,
mult(ld(A,A),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C))) = mult(ld(A,A),C),
inference(copy,[status(thm)],[c_11991]) ).
cnf(c_11992,plain,
mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))) = mult(mult(ld(A,A),ld(B,B)),C),
inference(paramod,[status(thm)],[c_7850,c_7516]) ).
cnf(c_11993,plain,
mult(ld(B,B),C) = mult(mult(ld(A,A),ld(B,B)),C),
inference(paramod,[status(thm)],[c_7851,c_11992]) ).
cnf(c_7853,plain,
mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(B,B),C),
inference(copy,[status(thm)],[c_11993]) ).
cnf(c_11994,plain,
mult(ld(A,A),mult(ld(A,A),C)) = mult(ld(B,B),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_7853,c_7850]) ).
cnf(c_11995,plain,
C = mult(ld(B,B),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_514,c_11994]) ).
cnf(c_7855,plain,
mult(ld(A,A),mult(ld(B,B),C)) = C,
inference(copy,[status(thm)],[c_11995]) ).
cnf(c_7867,plain,
mult(ld(A,A),ld(mult(ld(mult(ld(B,B),ld(A,A)),C),ld(A,A)),D)) = ld(mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_7853,c_7120]) ).
cnf(c_7872,plain,
mult(ld(mult(ld(A,A),B),mult(ld(B,B),ld(A,A))),ld(A,A)) = ld(mult(ld(A,A),B),ld(A,A)),
inference(paramod,[status(thm)],[c_7853,c_4827]) ).
cnf(c_11996,plain,
B = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_7855,c_7848]) ).
cnf(c_7873,plain,
mult(ld(A,A),B) = B,
inference(copy,[status(thm)],[c_11996]) ).
cnf(c_11997,plain,
mult(ld(B,mult(ld(B,B),ld(A,A))),ld(A,A)) = ld(mult(ld(A,A),B),ld(A,A)),
inference(paramod,[status(thm)],[c_7873,c_7872]) ).
cnf(c_11998,plain,
mult(ld(B,ld(A,A)),ld(A,A)) = ld(mult(ld(A,A),B),ld(A,A)),
inference(paramod,[status(thm)],[c_7873,c_11997]) ).
cnf(c_7881,plain,
mult(ld(A,ld(B,B)),ld(B,B)) = ld(A,ld(B,B)),
inference(paramod,[status(thm)],[c_7873,c_11998]) ).
cnf(c_11999,plain,
mult(ld(A,A),ld(mult(ld(ld(A,A),C),ld(A,A)),D)) = ld(mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_7873,c_7867]) ).
cnf(c_12000,plain,
mult(ld(A,A),ld(mult(mult(A,ld(mult(A,A),mult(A,C))),ld(A,A)),D)) = ld(mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_5310,c_11999]) ).
cnf(c_12001,plain,
mult(ld(A,A),ld(mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,C))))),ld(A,A)),D)) = ld(mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_5216,c_12000]) ).
cnf(c_12002,plain,
mult(ld(A,A),ld(mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),C))),ld(A,A)),D)) = ld(mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_5126,c_12001]) ).
cnf(c_12003,plain,
mult(ld(A,A),ld(mult(mult(A,mult(ld(A,ld(A,A)),C)),ld(A,A)),D)) = ld(mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_7873,c_12002]) ).
cnf(c_12004,plain,
mult(ld(A,A),ld(mult(C,ld(A,A)),D)) = ld(mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_5128,c_12003]) ).
cnf(c_12005,plain,
ld(mult(C,ld(A,A)),D) = ld(mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_7873,c_12004]) ).
cnf(c_12006,plain,
ld(mult(C,ld(A,A)),D) = ld(mult(ld(A,A),mult(ld(ld(A,A),ld(B,B)),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_7873,c_12005]) ).
cnf(c_12007,plain,
ld(mult(C,ld(A,A)),D) = ld(mult(ld(A,A),mult(mult(A,ld(mult(A,A),mult(A,ld(B,B)))),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_5310,c_12006]) ).
cnf(c_12008,plain,
ld(mult(C,ld(A,A)),D) = ld(mult(ld(A,A),mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,ld(B,B)))))),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_5216,c_12007]) ).
cnf(c_12009,plain,
ld(mult(C,ld(A,A)),D) = ld(mult(ld(A,A),mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),ld(B,B)))),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_5126,c_12008]) ).
cnf(c_12010,plain,
ld(mult(C,ld(A,A)),D) = ld(mult(ld(A,A),mult(mult(A,mult(ld(A,ld(A,A)),ld(B,B))),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_7873,c_12009]) ).
cnf(c_12011,plain,
ld(mult(C,ld(A,A)),D) = ld(mult(ld(A,A),mult(ld(B,B),C)),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_5128,c_12010]) ).
cnf(c_12012,plain,
ld(mult(C,ld(A,A)),D) = ld(mult(ld(A,A),C),mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_7873,c_12011]) ).
cnf(c_12013,plain,
ld(mult(C,ld(A,A)),D) = ld(C,mult(ld(A,A),D)),
inference(paramod,[status(thm)],[c_7873,c_12012]) ).
cnf(c_7883,plain,
ld(mult(A,ld(B,B)),C) = ld(A,C),
inference(paramod,[status(thm)],[c_7873,c_12013]) ).
cnf(c_12014,plain,
mult(ld(A,mult(ld(B,ld(B,B)),B)),mult(ld(B,B),ld(ld(A,ld(A,A)),C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_7873,c_7839]) ).
cnf(c_12015,plain,
mult(ld(A,mult(ld(B,ld(B,B)),B)),mult(ld(B,B),mult(A,ld(mult(ld(A,A),A),mult(A,C))))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_5310,c_12014]) ).
cnf(c_12016,plain,
mult(ld(A,mult(ld(B,ld(B,B)),B)),mult(ld(B,B),mult(A,ld(A,mult(A,C))))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_7873,c_12015]) ).
cnf(c_12017,plain,
mult(ld(A,mult(ld(B,ld(B,B)),B)),mult(ld(B,B),mult(A,C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_2,c_12016]) ).
cnf(c_12018,plain,
mult(ld(A,mult(ld(B,ld(B,B)),B)),mult(A,C)) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_7873,c_12017]) ).
cnf(c_7885,plain,
mult(ld(A,mult(ld(B,ld(B,B)),B)),mult(A,C)) = C,
inference(paramod,[status(thm)],[c_7873,c_12018]) ).
cnf(c_12019,plain,
mult(ld(A,ld(B,B)),mult(ld(B,B),ld(mult(ld(B,B),ld(A,ld(A,A))),C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_7881,c_7832]) ).
cnf(c_12020,plain,
mult(ld(A,ld(B,B)),mult(ld(B,B),ld(ld(A,ld(A,A)),C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_7873,c_12019]) ).
cnf(c_12021,plain,
mult(ld(A,ld(B,B)),mult(ld(B,B),mult(A,ld(mult(ld(A,A),A),mult(A,C))))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_5310,c_12020]) ).
cnf(c_12022,plain,
mult(ld(A,ld(B,B)),mult(ld(B,B),mult(A,ld(A,mult(A,C))))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_7873,c_12021]) ).
cnf(c_12023,plain,
mult(ld(A,ld(B,B)),mult(ld(B,B),mult(A,C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_2,c_12022]) ).
cnf(c_12024,plain,
mult(ld(A,ld(B,B)),mult(A,C)) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_7873,c_12023]) ).
cnf(c_7891,plain,
mult(ld(A,ld(B,B)),mult(A,C)) = C,
inference(paramod,[status(thm)],[c_7873,c_12024]) ).
cnf(c_12025,plain,
mult(mult(mult(ld(A,ld(A,A)),ld(A,A)),A),mult(ld(A,A),B)) = B,
inference(paramod,[status(thm)],[c_7881,c_7804]) ).
cnf(c_12026,plain,
mult(mult(ld(A,ld(A,A)),A),mult(ld(A,A),B)) = B,
inference(paramod,[status(thm)],[c_7881,c_12025]) ).
cnf(c_7905,plain,
mult(mult(ld(A,ld(A,A)),A),B) = B,
inference(paramod,[status(thm)],[c_7873,c_12026]) ).
cnf(c_12027,plain,
mult(B,mult(ld(mult(ld(A,A),B),mult(ld(A,ld(A,A)),A)),mult(B,mult(ld(B,ld(A,A)),C)))) = C,
inference(paramod,[status(thm)],[c_7873,c_7794]) ).
cnf(c_12028,plain,
mult(B,mult(ld(B,mult(ld(A,ld(A,A)),A)),mult(B,mult(ld(B,ld(A,A)),C)))) = C,
inference(paramod,[status(thm)],[c_7873,c_12027]) ).
cnf(c_7911,plain,
mult(A,mult(ld(A,ld(B,B)),C)) = C,
inference(paramod,[status(thm)],[c_7885,c_12028]) ).
cnf(c_12029,plain,
ld(B,mult(B,mult(ld(mult(ld(A,A),B),ld(A,A)),C))) = mult(ld(mult(ld(A,A),B),ld(A,A)),mult(B,ld(mult(ld(A,A),B),C))),
inference(paramod,[status(thm)],[c_7873,c_7570]) ).
cnf(c_12030,plain,
ld(B,mult(B,mult(ld(B,ld(A,A)),C))) = mult(ld(mult(ld(A,A),B),ld(A,A)),mult(B,ld(mult(ld(A,A),B),C))),
inference(paramod,[status(thm)],[c_7873,c_12029]) ).
cnf(c_12031,plain,
ld(B,C) = mult(ld(mult(ld(A,A),B),ld(A,A)),mult(B,ld(mult(ld(A,A),B),C))),
inference(paramod,[status(thm)],[c_7911,c_12030]) ).
cnf(c_12032,plain,
ld(B,C) = mult(ld(B,ld(A,A)),mult(B,ld(mult(ld(A,A),B),C))),
inference(paramod,[status(thm)],[c_7873,c_12031]) ).
cnf(c_12033,plain,
ld(B,C) = mult(ld(B,ld(A,A)),mult(B,ld(B,C))),
inference(paramod,[status(thm)],[c_7873,c_12032]) ).
cnf(c_12034,plain,
ld(B,C) = mult(ld(B,ld(A,A)),C),
inference(paramod,[status(thm)],[c_1,c_12033]) ).
cnf(c_7934,plain,
mult(ld(A,ld(B,B)),C) = ld(A,C),
inference(copy,[status(thm)],[c_12034]) ).
cnf(c_12035,plain,
mult(ld(ld(B,C),ld(A,A)),mult(mult(ld(A,A),ld(B,C)),mult(B,ld(mult(C,B),D)))) = ld(mult(ld(A,A),ld(B,C)),ld(B,D)),
inference(paramod,[status(thm)],[c_7873,c_7537]) ).
cnf(c_12036,plain,
mult(mult(B,ld(mult(C,B),mult(B,ld(A,A)))),mult(mult(ld(A,A),ld(B,C)),mult(B,ld(mult(C,B),D)))) = ld(mult(ld(A,A),ld(B,C)),ld(B,D)),
inference(paramod,[status(thm)],[c_5310,c_12035]) ).
cnf(c_12037,plain,
mult(mult(B,ld(mult(C,B),mult(B,ld(A,A)))),mult(ld(B,C),mult(B,ld(mult(C,B),D)))) = ld(mult(ld(A,A),ld(B,C)),ld(B,D)),
inference(paramod,[status(thm)],[c_7873,c_12036]) ).
cnf(c_12038,plain,
mult(mult(B,ld(mult(C,B),mult(B,ld(A,A)))),ld(B,D)) = ld(mult(ld(A,A),ld(B,C)),ld(B,D)),
inference(paramod,[status(thm)],[c_547,c_12037]) ).
cnf(c_12039,plain,
mult(mult(B,ld(mult(C,B),mult(B,ld(A,A)))),ld(B,D)) = ld(ld(B,C),ld(B,D)),
inference(paramod,[status(thm)],[c_7873,c_12038]) ).
cnf(c_12040,plain,
mult(mult(B,ld(mult(C,B),mult(B,ld(A,A)))),ld(B,D)) = mult(B,ld(mult(C,B),mult(B,ld(B,D)))),
inference(paramod,[status(thm)],[c_5310,c_12039]) ).
cnf(c_7939,plain,
mult(mult(A,ld(mult(B,A),mult(A,ld(C,C)))),ld(A,D)) = mult(A,ld(mult(B,A),D)),
inference(paramod,[status(thm)],[c_1,c_12040]) ).
cnf(c_12041,plain,
mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C))) = mult(ld(A,A),ld(mult(B,A),C)),
inference(paramod,[status(thm)],[c_7873,c_7380]) ).
cnf(c_7949,plain,
mult(ld(A,ld(A,A)),ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),C))) = ld(mult(B,A),C),
inference(paramod,[status(thm)],[c_7873,c_12041]) ).
cnf(c_12042,plain,
mult(mult(ld(A,ld(A,A)),A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))) = mult(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_7881,c_7176]) ).
cnf(c_12043,plain,
mult(mult(ld(A,ld(A,A)),A),mult(mult(B,ld(A,A)),C)) = mult(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_7873,c_12042]) ).
cnf(c_12044,plain,
mult(mult(B,ld(A,A)),C) = mult(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_7905,c_12043]) ).
cnf(c_7972,plain,
mult(mult(A,ld(B,B)),C) = mult(A,C),
inference(paramod,[status(thm)],[c_7873,c_12044]) ).
cnf(c_8015,plain,
mult(mult(A,ld(mult(B,A),B)),C) = C,
inference(paramod,[status(thm)],[c_7873,c_6135]) ).
cnf(c_12045,plain,
mult(ld(A,A),ld(mult(ld(B,mult(ld(A,A),C)),ld(A,A)),mult(ld(A,A),D))) = mult(mult(B,ld(A,A)),ld(mult(C,mult(B,ld(A,A))),mult(mult(B,ld(A,A)),D))),
inference(paramod,[status(thm)],[c_7873,c_6092]) ).
cnf(c_12046,plain,
mult(ld(A,A),ld(mult(ld(B,C),ld(A,A)),mult(ld(A,A),D))) = mult(mult(B,ld(A,A)),ld(mult(C,mult(B,ld(A,A))),mult(mult(B,ld(A,A)),D))),
inference(paramod,[status(thm)],[c_7873,c_12045]) ).
cnf(c_12047,plain,
mult(ld(A,A),ld(mult(ld(B,C),ld(A,A)),D)) = mult(mult(B,ld(A,A)),ld(mult(C,mult(B,ld(A,A))),mult(mult(B,ld(A,A)),D))),
inference(paramod,[status(thm)],[c_7873,c_12046]) ).
cnf(c_12048,plain,
mult(ld(A,A),ld(ld(B,C),D)) = mult(mult(B,ld(A,A)),ld(mult(C,mult(B,ld(A,A))),mult(mult(B,ld(A,A)),D))),
inference(paramod,[status(thm)],[c_7883,c_12047]) ).
cnf(c_12049,plain,
mult(ld(A,A),mult(B,ld(mult(C,B),mult(B,D)))) = mult(mult(B,ld(A,A)),ld(mult(C,mult(B,ld(A,A))),mult(mult(B,ld(A,A)),D))),
inference(paramod,[status(thm)],[c_5310,c_12048]) ).
cnf(c_12050,plain,
mult(B,ld(mult(C,B),mult(B,D))) = mult(mult(B,ld(A,A)),ld(mult(C,mult(B,ld(A,A))),mult(mult(B,ld(A,A)),D))),
inference(paramod,[status(thm)],[c_7873,c_12049]) ).
cnf(c_12051,plain,
mult(B,ld(mult(C,B),mult(B,D))) = mult(mult(B,ld(A,A)),ld(mult(C,mult(B,ld(A,A))),mult(B,D))),
inference(paramod,[status(thm)],[c_7972,c_12050]) ).
cnf(c_12052,plain,
mult(B,ld(mult(C,B),mult(B,D))) = mult(B,ld(mult(C,mult(B,ld(A,A))),mult(B,D))),
inference(paramod,[status(thm)],[c_7972,c_12051]) ).
cnf(c_8016,plain,
mult(A,ld(mult(B,mult(A,ld(C,C))),mult(A,D))) = mult(A,ld(mult(B,A),mult(A,D))),
inference(copy,[status(thm)],[c_12052]) ).
cnf(c_8152,plain,
tuple(x1(ld(A,A)),mult(x1_2(ld(A,A)),ld(A,A))) != tuple(x1(ld(A,A)),x1_2(ld(A,A))),
inference(paramod,[status(thm)],[c_7873,c_7]) ).
cnf(c_8306,plain,
mult(ld(A,mult(mult(ld(B,C),ld(C,B)),mult(ld(B,C),ld(C,B)))),D) = ld(A,D),
inference(paramod,[status(thm)],[c_6176,c_7934]) ).
cnf(c_8378,plain,
mult(mult(A,mult(mult(ld(B,C),ld(C,B)),mult(ld(B,C),ld(C,B)))),D) = mult(A,D),
inference(paramod,[status(thm)],[c_6176,c_7972]) ).
cnf(c_8507,plain,
mult(mult(ld(A,B),ld(B,A)),C) = C,
inference(paramod,[status(thm)],[c_1,c_8015]) ).
cnf(c_8565,plain,
mult(mult(A,mult(ld(B,C),ld(C,B))),D) = mult(A,D),
inference(paramod,[status(thm)],[c_8507,c_8378]) ).
cnf(c_8566,plain,
mult(ld(A,mult(ld(B,C),ld(C,B))),D) = ld(A,D),
inference(paramod,[status(thm)],[c_8507,c_8306]) ).
cnf(c_12053,plain,
mult(ld(A,B),C) = ld(ld(B,A),C),
inference(paramod,[status(thm)],[c_2,c_8566]) ).
cnf(c_12054,plain,
mult(ld(A,B),C) = mult(B,ld(mult(A,B),mult(B,C))),
inference(paramod,[status(thm)],[c_5310,c_12053]) ).
cnf(c_8717,plain,
mult(A,ld(mult(B,A),mult(A,C))) = mult(ld(B,A),C),
inference(copy,[status(thm)],[c_12054]) ).
cnf(c_8818,plain,
mult(ld(A,mult(ld(B,C),ld(C,mult(B,ld(D,D))))),E) = ld(A,E),
inference(paramod,[status(thm)],[c_7883,c_8566]) ).
cnf(c_12055,plain,
tuple(x1(ld(A,A)),mult(x1_2(mult(ld(A,mult(ld(B,C),ld(C,B))),A)),ld(A,A))) != tuple(x1(ld(A,A)),x1_2(ld(A,A))),
inference(paramod,[status(thm)],[c_8566,c_8152]) ).
cnf(c_8832,plain,
tuple(x1(ld(A,A)),x1_2(ld(A,A))) != tuple(x1(ld(A,A)),mult(x1_2(mult(ld(A,mult(ld(B,C),ld(C,B))),A)),ld(A,A))),
inference(copy,[status(thm)],[c_12055]) ).
cnf(c_8908,plain,
mult(A,ld(mult(B,mult(A,ld(C,C))),mult(A,D))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8717,c_8016]) ).
cnf(c_12056,plain,
mult(mult(ld(B,A),ld(C,C)),ld(A,D)) = mult(A,ld(mult(B,A),D)),
inference(paramod,[status(thm)],[c_8717,c_7939]) ).
cnf(c_12057,plain,
mult(ld(B,A),ld(A,D)) = mult(A,ld(mult(B,A),D)),
inference(paramod,[status(thm)],[c_7972,c_12056]) ).
cnf(c_8914,plain,
mult(A,ld(mult(B,A),C)) = mult(ld(B,A),ld(A,C)),
inference(copy,[status(thm)],[c_12057]) ).
cnf(c_12058,plain,
mult(ld(C,ld(A,B)),ld(ld(A,B),mult(ld(A,B),D))) = ld(mult(mult(A,ld(mult(B,A),mult(A,mult(A,ld(mult(B,A),B))))),C),D),
inference(paramod,[status(thm)],[c_8914,c_6134]) ).
cnf(c_12059,plain,
mult(ld(C,ld(A,B)),D) = ld(mult(mult(A,ld(mult(B,A),mult(A,mult(A,ld(mult(B,A),B))))),C),D),
inference(paramod,[status(thm)],[c_2,c_12058]) ).
cnf(c_12060,plain,
mult(ld(C,ld(A,B)),D) = ld(mult(mult(A,ld(mult(B,A),mult(A,mult(ld(B,A),ld(A,B))))),C),D),
inference(paramod,[status(thm)],[c_8914,c_12059]) ).
cnf(c_12061,plain,
mult(ld(C,ld(A,B)),D) = ld(mult(mult(ld(B,A),ld(A,mult(A,mult(ld(B,A),ld(A,B))))),C),D),
inference(paramod,[status(thm)],[c_8914,c_12060]) ).
cnf(c_12062,plain,
mult(ld(C,ld(A,B)),D) = ld(mult(mult(ld(B,A),mult(ld(B,A),ld(A,B))),C),D),
inference(paramod,[status(thm)],[c_2,c_12061]) ).
cnf(c_12063,plain,
mult(ld(C,ld(A,B)),D) = ld(mult(ld(B,A),C),D),
inference(paramod,[status(thm)],[c_8565,c_12062]) ).
cnf(c_8965,plain,
ld(mult(ld(A,B),C),D) = mult(ld(C,ld(B,A)),D),
inference(copy,[status(thm)],[c_12063]) ).
cnf(c_12064,plain,
ld(mult(A,B),mult(B,C)) = ld(B,mult(mult(B,ld(mult(A,B),mult(B,mult(ld(A,B),ld(B,A))))),C)),
inference(paramod,[status(thm)],[c_8914,c_5804]) ).
cnf(c_12065,plain,
ld(mult(A,B),mult(B,C)) = ld(B,mult(mult(ld(A,B),ld(B,mult(B,mult(ld(A,B),ld(B,A))))),C)),
inference(paramod,[status(thm)],[c_8914,c_12064]) ).
cnf(c_12066,plain,
ld(mult(A,B),mult(B,C)) = ld(B,mult(mult(ld(A,B),mult(ld(A,B),ld(B,A))),C)),
inference(paramod,[status(thm)],[c_2,c_12065]) ).
cnf(c_8970,plain,
ld(mult(A,B),mult(B,C)) = ld(B,mult(ld(A,B),C)),
inference(paramod,[status(thm)],[c_8565,c_12066]) ).
cnf(c_12067,plain,
ld(ld(A,B),C) = mult(A,ld(A,mult(ld(B,A),C))),
inference(paramod,[status(thm)],[c_8970,c_5310]) ).
cnf(c_8996,plain,
ld(ld(A,B),C) = mult(ld(B,A),C),
inference(paramod,[status(thm)],[c_1,c_12067]) ).
cnf(c_12068,plain,
mult(ld(A,ld(A,A)),mult(ld(B,ld(ld(A,A),A)),mult(ld(A,ld(A,A)),C))) = ld(mult(B,A),C),
inference(paramod,[status(thm)],[c_8965,c_7949]) ).
cnf(c_12069,plain,
mult(ld(A,ld(A,A)),mult(ld(B,mult(ld(A,A),A)),mult(ld(A,ld(A,A)),C))) = ld(mult(B,A),C),
inference(paramod,[status(thm)],[c_8996,c_12068]) ).
cnf(c_12070,plain,
mult(ld(A,ld(A,A)),mult(ld(B,A),mult(ld(A,ld(A,A)),C))) = ld(mult(B,A),C),
inference(paramod,[status(thm)],[c_7873,c_12069]) ).
cnf(c_9025,plain,
ld(mult(A,B),C) = mult(ld(B,ld(B,B)),mult(ld(A,B),mult(ld(B,ld(B,B)),C))),
inference(copy,[status(thm)],[c_12070]) ).
cnf(c_12071,plain,
mult(A,mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_9025,c_8908]) ).
cnf(c_12072,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_9025,c_12071]) ).
cnf(c_12073,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(ld(ld(C,C),mult(ld(C,C),ld(C,C))),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12072]) ).
cnf(c_12074,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(ld(ld(C,C),ld(C,C)),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12073]) ).
cnf(c_12075,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(mult(ld(C,C),ld(C,C)),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12074]) ).
cnf(c_12076,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12075]) ).
cnf(c_12077,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),mult(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12076]) ).
cnf(c_12078,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(C,C)),mult(A,ld(C,C)))))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12077]) ).
cnf(c_12079,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(mult(ld(C,C),ld(C,C)),mult(A,ld(C,C)))))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12078]) ).
cnf(c_12080,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(C,C),mult(A,ld(C,C)))))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12079]) ).
cnf(c_12081,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(A,ld(C,C))))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12080]) ).
cnf(c_12082,plain,
mult(A,mult(ld(mult(A,ld(C,C)),mult(ld(C,C),ld(C,C))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7891,c_12081]) ).
cnf(c_12083,plain,
mult(A,mult(ld(mult(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12082]) ).
cnf(c_12084,plain,
mult(A,mult(mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),ld(C,C)))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_9025,c_12083]) ).
cnf(c_12085,plain,
mult(A,mult(mult(ld(ld(C,C),mult(ld(C,C),ld(C,C))),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),ld(C,C)))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12084]) ).
cnf(c_12086,plain,
mult(A,mult(mult(ld(ld(C,C),ld(C,C)),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),ld(C,C)))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12085]) ).
cnf(c_12087,plain,
mult(A,mult(mult(mult(ld(C,C),ld(C,C)),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),ld(C,C)))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12086]) ).
cnf(c_12088,plain,
mult(A,mult(mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),ld(C,C)))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12087]) ).
cnf(c_12089,plain,
mult(A,mult(mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),mult(ld(C,C),ld(C,C))),ld(C,C)))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12088]) ).
cnf(c_12090,plain,
mult(A,mult(mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(C,C)),ld(C,C)))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12089]) ).
cnf(c_12091,plain,
mult(A,mult(mult(ld(C,C),mult(ld(A,ld(C,C)),mult(mult(ld(C,C),ld(C,C)),ld(C,C)))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12090]) ).
cnf(c_12092,plain,
mult(A,mult(mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(C,C),ld(C,C)))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12091]) ).
cnf(c_12093,plain,
mult(A,mult(mult(ld(C,C),mult(ld(A,ld(C,C)),ld(C,C))),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12092]) ).
cnf(c_12094,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(mult(A,ld(C,C)),mult(A,ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12093]) ).
cnf(c_12095,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_9025,c_12094]) ).
cnf(c_12096,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(ld(ld(C,C),mult(ld(C,C),ld(C,C))),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12095]) ).
cnf(c_12097,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(ld(ld(C,C),ld(C,C)),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12096]) ).
cnf(c_12098,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(mult(ld(C,C),ld(C,C)),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12097]) ).
cnf(c_12099,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12098]) ).
cnf(c_12100,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),mult(ld(C,C),ld(C,C))),mult(A,ld(C,C)))))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12099]) ).
cnf(c_12101,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(C,C)),mult(A,ld(C,C)))))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12100]) ).
cnf(c_12102,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(mult(ld(C,C),ld(C,C)),mult(A,ld(C,C)))))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12101]) ).
cnf(c_12103,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(C,C),mult(A,ld(C,C)))))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12102]) ).
cnf(c_12104,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(ld(C,C),mult(ld(A,ld(C,C)),mult(A,ld(C,C))))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12103]) ).
cnf(c_12105,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),mult(ld(C,C),ld(C,C))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7891,c_12104]) ).
cnf(c_12106,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(mult(A,ld(C,C)),ld(C,C)),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12105]) ).
cnf(c_12107,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_9025,c_12106]) ).
cnf(c_12108,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(ld(ld(C,C),mult(ld(C,C),ld(C,C))),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12107]) ).
cnf(c_12109,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(ld(ld(C,C),ld(C,C)),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12108]) ).
cnf(c_12110,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(mult(ld(C,C),ld(C,C)),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12109]) ).
cnf(c_12111,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(ld(C,C),ld(C,C))),ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12110]) ).
cnf(c_12112,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),mult(ld(C,C),ld(C,C))),ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12111]) ).
cnf(c_12113,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(ld(C,C),ld(C,C)),ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12112]) ).
cnf(c_12114,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(ld(C,C),mult(ld(A,ld(C,C)),mult(mult(ld(C,C),ld(C,C)),ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_8996,c_12113]) ).
cnf(c_12115,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(ld(C,C),mult(ld(A,ld(C,C)),mult(ld(C,C),ld(C,C)))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12114]) ).
cnf(c_12116,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(ld(C,C),mult(ld(A,ld(C,C)),ld(C,C))),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12115]) ).
cnf(c_12117,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7873,c_12116]) ).
cnf(c_12118,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),mult(ld(A,ld(C,C)),mult(A,D))))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7972,c_12117]) ).
cnf(c_12119,plain,
mult(A,mult(mult(ld(A,ld(C,C)),ld(C,C)),mult(ld(B,mult(A,ld(C,C))),D))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7891,c_12118]) ).
cnf(c_12120,plain,
mult(A,mult(ld(A,ld(C,C)),mult(ld(B,mult(A,ld(C,C))),D))) = mult(ld(B,A),D),
inference(paramod,[status(thm)],[c_7972,c_12119]) ).
cnf(c_9072,plain,
mult(ld(A,mult(B,ld(C,C))),D) = mult(ld(A,B),D),
inference(paramod,[status(thm)],[c_7911,c_12120]) ).
cnf(c_9190,plain,
mult(ld(A,mult(B,mult(ld(B,C),B))),D) = mult(ld(A,mult(C,B)),D),
inference(paramod,[status(thm)],[c_16,c_9072]) ).
cnf(c_12121,plain,
mult(ld(A,mult(B,mult(C,B))),D) = mult(ld(A,mult(mult(B,C),B)),D),
inference(paramod,[status(thm)],[c_2,c_9190]) ).
cnf(c_10752,plain,
mult(ld(A,mult(mult(B,C),B)),D) = mult(ld(A,mult(B,mult(C,B))),D),
inference(copy,[status(thm)],[c_12121]) ).
cnf(c_10971,plain,
tuple(x1(ld(A,A)),x1_2(mult(ld(A,mult(ld(B,C),ld(C,mult(B,ld(D,D))))),A))) != tuple(x1(ld(A,A)),mult(x1_2(mult(ld(A,mult(ld(E,F),ld(F,E))),A)),ld(A,A))),
inference(paramod,[status(thm)],[c_8818,c_8832]) ).
cnf(c_12122,plain,
mult(mult(ld(A,B),mult(mult(C,D),C)),E) = mult(ld(ld(B,A),mult(C,mult(D,C))),E),
inference(paramod,[status(thm)],[c_8996,c_10752]) ).
cnf(c_11318,plain,
mult(mult(ld(A,B),mult(mult(C,D),C)),E) = mult(mult(ld(A,B),mult(C,mult(D,C))),E),
inference(paramod,[status(thm)],[c_8996,c_12122]) ).
cnf(c_12123,plain,
mult(mult(ld(A,ld(A,A)),mult(A,mult(B,A))),ld(A,ld(A,A))) = B,
inference(paramod,[status(thm)],[c_11318,c_5148]) ).
cnf(c_11352,plain,
mult(mult(A,B),ld(B,ld(B,B))) = A,
inference(paramod,[status(thm)],[c_7891,c_12123]) ).
cnf(c_12124,plain,
A = mult(A,ld(ld(B,B),ld(ld(B,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_11352,c_7972]) ).
cnf(c_12125,plain,
A = mult(A,ld(ld(B,B),mult(ld(B,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_8996,c_12124]) ).
cnf(c_12126,plain,
A = mult(A,ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_7873,c_12125]) ).
cnf(c_12127,plain,
A = mult(A,mult(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_8996,c_12126]) ).
cnf(c_12128,plain,
A = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_7873,c_12127]) ).
cnf(c_11448,plain,
mult(A,ld(B,B)) = A,
inference(copy,[status(thm)],[c_12128]) ).
cnf(c_12129,plain,
tuple(x1(ld(A,A)),x1_2(mult(ld(A,mult(ld(B,C),ld(C,B))),A))) != tuple(x1(ld(A,A)),mult(x1_2(mult(ld(A,mult(ld(E,F),ld(F,E))),A)),ld(A,A))),
inference(paramod,[status(thm)],[c_11448,c_10971]) ).
cnf(c_12130,plain,
tuple(x1(ld(A,A)),x1_2(mult(ld(A,mult(ld(B,C),ld(C,B))),A))) != tuple(x1(ld(A,A)),x1_2(mult(ld(A,mult(ld(E,F),ld(F,E))),A))),
inference(paramod,[status(thm)],[c_11448,c_12129]) ).
cnf(c_11546,plain,
$false,
inference(copy,[status(thm)],[c_12130]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP654-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.46 % Computer : n003.cluster.edu
% 0.09/0.46 % Model : x86_64 x86_64
% 0.09/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.46 % Memory : 8046.5625MB
% 0.09/0.46 % OS : Linux 6.8.0-71-generic
% 0.09/0.46 % CPULimit : 300
% 0.09/0.46 % WCLimit : 300
% 0.09/0.46 % DateTime : Fri Sep 25 15:30:24 UTC 2026
% 0.09/0.46 % CPUTime :
% 0.09/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.46 % Process 535131 was started by sandbox on n003,
% 0.09/0.46 % Fri Sep 25 15:30:24 2026
% 0.09/0.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.47
% 0.09/0.47 % From the command line: assign(max_seconds, 300).
% 142.06/31.88
% 142.06/31.88 % SZS status Unsatisfiable for theBenchmark
% 142.06/31.88
% 142.06/31.88 % Proof 1 at 5.77 (+ 1.07) seconds.
% 142.06/31.88 % Length of proof is 270.
% 142.06/31.88 % Level of proof is 56.
% 142.06/31.88 % Maximum clause weight is 100.000.
% 142.06/31.88 % Given clauses 380.
% 142.06/31.88
% 142.06/31.88 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------