%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP698-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:31:13 AM UTC 2026
% Result : Unsatisfiable 16.44s 2.55s
% Output : CNFRefutation 16.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 99
% Number of leaves : 9
% Syntax : Number of formulae : 606 ( 606 unt; 0 def)
% Number of atoms : 606 ( 605 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 16 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 1064 ( 0 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(c01,axiom,
! [VAR_0,VAR_1] : mult(VAR_0,ld(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',c01) ).
cnf(c_1,plain,
mult(A,ld(A,B)) = B,
inference(clausify,[status(thm)],[c01]) ).
fof(c02,axiom,
! [VAR_0,VAR_1] : ld(VAR_0,mult(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',c02) ).
cnf(c_2,plain,
ld(A,mult(A,B)) = B,
inference(clausify,[status(thm)],[c02]) ).
fof(c03,axiom,
! [VAR_0,VAR_1] : mult(rd(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',c03) ).
cnf(c_3,plain,
mult(rd(A,B),B) = A,
inference(clausify,[status(thm)],[c03]) ).
fof(c04,axiom,
! [VAR_0,VAR_1] : rd(mult(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',c04) ).
cnf(c_4,plain,
rd(mult(A,B),B) = A,
inference(clausify,[status(thm)],[c04]) ).
fof(c05,axiom,
! [VAR_0] : mult(VAR_0,unit) = VAR_0,
file('theBenchmark.p',c05) ).
cnf(c_5,plain,
mult(A,unit) = A,
inference(clausify,[status(thm)],[c05]) ).
fof(c06,axiom,
! [VAR_0] : mult(unit,VAR_0) = VAR_0,
file('theBenchmark.p',c06) ).
cnf(c_6,plain,
mult(unit,A) = A,
inference(clausify,[status(thm)],[c06]) ).
fof(c07,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(mult(mult(VAR_0,VAR_1),VAR_0),mult(VAR_0,VAR_2)) = mult(VAR_0,mult(mult(mult(VAR_1,VAR_0),VAR_0),VAR_2)),
file('theBenchmark.p',c07) ).
cnf(c_7,plain,
mult(mult(mult(A,B),A),mult(A,C)) = mult(A,mult(mult(mult(B,A),A),C)),
inference(clausify,[status(thm)],[c07]) ).
fof(c08,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(mult(VAR_0,VAR_1),mult(VAR_1,mult(VAR_2,VAR_1))) = mult(mult(VAR_0,mult(VAR_1,mult(VAR_1,VAR_2))),VAR_1),
file('theBenchmark.p',c08) ).
cnf(c_8,plain,
mult(mult(A,B),mult(B,mult(C,B))) = mult(mult(A,mult(B,mult(B,C))),B),
inference(clausify,[status(thm)],[c08]) ).
cnf(c_9,plain,
mult(mult(A,mult(B,mult(B,C))),B) = mult(mult(A,B),mult(B,mult(C,B))),
inference(copy,[status(thm)],[c_8]) ).
fof(goals,axiom,
mult(a,mult(b,c)) != mult(rd(mult(a,b),a),mult(a,c)),
file('theBenchmark.p',goals) ).
cnf(c_10,plain,
mult(a,mult(b,c)) != mult(rd(mult(a,b),a),mult(a,c)),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_11,plain,
mult(rd(mult(a,b),a),mult(a,c)) != mult(a,mult(b,c)),
inference(copy,[status(thm)],[c_10]) ).
cnf(c_12,plain,
ld(rd(A,B),A) = B,
inference(paramod,[status(thm)],[c_3,c_2]) ).
cnf(c_13,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_14,plain,
ld(A,A) = unit,
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_3098,plain,
mult(mult(A,B),mult(B,C)) = mult(B,mult(mult(mult(ld(B,A),B),B),C)),
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_18,plain,
mult(A,mult(mult(mult(ld(A,B),A),A),C)) = mult(mult(B,A),mult(A,C)),
inference(copy,[status(thm)],[c_3098]) ).
cnf(c_19,plain,
mult(mult(mult(A,B),A),C) = mult(A,mult(mult(mult(B,A),A),ld(A,C))),
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_26,plain,
mult(mult(mult(A,rd(B,A)),A),mult(A,C)) = mult(A,mult(mult(B,A),C)),
inference(paramod,[status(thm)],[c_3,c_7]) ).
cnf(c_3099,plain,
mult(mult(A,A),mult(A,B)) = mult(A,mult(mult(mult(unit,A),A),B)),
inference(paramod,[status(thm)],[c_5,c_7]) ).
cnf(c_29,plain,
mult(mult(A,A),mult(A,B)) = mult(A,mult(mult(A,A),B)),
inference(paramod,[status(thm)],[c_6,c_3099]) ).
cnf(c_3100,plain,
mult(mult(mult(A,B),A),A) = mult(A,mult(mult(mult(B,A),A),unit)),
inference(paramod,[status(thm)],[c_5,c_7]) ).
cnf(c_30,plain,
mult(mult(mult(A,B),A),A) = mult(A,mult(mult(B,A),A)),
inference(paramod,[status(thm)],[c_5,c_3100]) ).
cnf(c_32,plain,
mult(mult(A,mult(B,C)),B) = mult(mult(A,B),mult(B,mult(ld(B,C),B))),
inference(paramod,[status(thm)],[c_1,c_9]) ).
cnf(c_3101,plain,
mult(mult(A,mult(B,B)),B) = mult(mult(A,B),mult(B,mult(unit,B))),
inference(paramod,[status(thm)],[c_5,c_9]) ).
cnf(c_37,plain,
mult(mult(A,mult(B,B)),B) = mult(mult(A,B),mult(B,B)),
inference(paramod,[status(thm)],[c_6,c_3101]) ).
cnf(c_3102,plain,
mult(mult(A,mult(A,B)),A) = mult(mult(unit,A),mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_6,c_9]) ).
cnf(c_38,plain,
mult(mult(A,mult(A,B)),A) = mult(A,mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_6,c_3102]) ).
cnf(c_3103,plain,
mult(mult(A,A),B) = mult(A,mult(mult(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_1,c_29]) ).
cnf(c_39,plain,
mult(A,mult(mult(A,A),ld(A,B))) = mult(mult(A,A),B),
inference(copy,[status(thm)],[c_3103]) ).
cnf(c_40,plain,
ld(mult(A,A),mult(A,mult(mult(A,A),B))) = mult(A,B),
inference(paramod,[status(thm)],[c_29,c_2]) ).
cnf(c_3104,plain,
mult(mult(A,A),A) = mult(A,mult(mult(A,A),unit)),
inference(paramod,[status(thm)],[c_5,c_29]) ).
cnf(c_43,plain,
mult(mult(A,A),A) = mult(A,mult(A,A)),
inference(paramod,[status(thm)],[c_5,c_3104]) ).
cnf(c_3105,plain,
mult(mult(A,mult(mult(A,A),mult(A,B))),A) = mult(mult(mult(A,A),A),mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_29,c_9]) ).
cnf(c_3106,plain,
mult(mult(A,mult(A,mult(mult(A,A),B))),A) = mult(mult(mult(A,A),A),mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_29,c_3105]) ).
cnf(c_3107,plain,
mult(A,mult(A,mult(mult(mult(A,A),B),A))) = mult(mult(mult(A,A),A),mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_38,c_3106]) ).
cnf(c_44,plain,
mult(A,mult(A,mult(mult(mult(A,A),B),A))) = mult(mult(A,mult(A,A)),mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_43,c_3107]) ).
cnf(c_3108,plain,
mult(mult(A,mult(A,A)),mult(A,B)) = mult(A,mult(mult(mult(A,A),A),B)),
inference(paramod,[status(thm)],[c_43,c_7]) ).
cnf(c_49,plain,
mult(mult(A,mult(A,A)),mult(A,B)) = mult(A,mult(mult(A,mult(A,A)),B)),
inference(paramod,[status(thm)],[c_43,c_3108]) ).
cnf(c_51,plain,
mult(A,mult(A,mult(mult(mult(A,A),B),A))) = mult(A,mult(mult(A,mult(A,A)),mult(B,A))),
inference(paramod,[status(thm)],[c_49,c_44]) ).
cnf(c_3109,plain,
mult(A,B) = mult(mult(C,A),mult(A,ld(mult(mult(ld(A,C),A),A),B))),
inference(paramod,[status(thm)],[c_1,c_18]) ).
cnf(c_53,plain,
mult(mult(A,B),mult(B,ld(mult(mult(ld(B,A),B),B),C))) = mult(B,C),
inference(copy,[status(thm)],[c_3109]) ).
cnf(c_54,plain,
ld(A,mult(mult(B,A),mult(A,C))) = mult(mult(mult(ld(A,B),A),A),C),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_3110,plain,
mult(A,mult(mult(ld(A,B),A),A)) = mult(mult(B,A),mult(A,unit)),
inference(paramod,[status(thm)],[c_5,c_18]) ).
cnf(c_56,plain,
mult(A,mult(mult(ld(A,B),A),A)) = mult(mult(B,A),A),
inference(paramod,[status(thm)],[c_5,c_3110]) ).
cnf(c_63,plain,
rd(mult(mult(mult(A,B),A),C),mult(mult(mult(B,A),A),ld(A,C))) = A,
inference(paramod,[status(thm)],[c_19,c_4]) ).
cnf(c_64,plain,
mult(A,mult(mult(mult(B,A),A),ld(A,unit))) = mult(mult(A,B),A),
inference(paramod,[status(thm)],[c_19,c_5]) ).
cnf(c_3111,plain,
mult(mult(A,mult(A,A)),B) = mult(A,mult(mult(mult(A,A),A),ld(A,B))),
inference(paramod,[status(thm)],[c_43,c_19]) ).
cnf(c_3112,plain,
mult(mult(A,mult(A,A)),B) = mult(A,mult(mult(A,mult(A,A)),ld(A,B))),
inference(paramod,[status(thm)],[c_43,c_3111]) ).
cnf(c_67,plain,
mult(A,mult(mult(A,mult(A,A)),ld(A,B))) = mult(mult(A,mult(A,A)),B),
inference(copy,[status(thm)],[c_3112]) ).
cnf(c_73,plain,
ld(A,mult(mult(A,A),B)) = mult(mult(A,A),ld(A,B)),
inference(paramod,[status(thm)],[c_39,c_2]) ).
cnf(c_3113,plain,
ld(A,mult(A,A)) = mult(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_5,c_73]) ).
cnf(c_3114,plain,
A = mult(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_2,c_3113]) ).
cnf(c_79,plain,
mult(mult(A,A),ld(A,unit)) = A,
inference(copy,[status(thm)],[c_3114]) ).
cnf(c_81,plain,
ld(mult(A,A),A) = ld(A,unit),
inference(paramod,[status(thm)],[c_79,c_2]) ).
cnf(c_84,plain,
mult(mult(rd(unit,A),rd(unit,A)),A) = rd(unit,A),
inference(paramod,[status(thm)],[c_12,c_79]) ).
cnf(c_3115,plain,
ld(mult(A,mult(mult(A,A),A)),mult(A,A)) = ld(mult(A,A),unit),
inference(paramod,[status(thm)],[c_29,c_81]) ).
cnf(c_90,plain,
ld(mult(A,mult(A,mult(A,A))),mult(A,A)) = ld(mult(A,A),unit),
inference(paramod,[status(thm)],[c_43,c_3115]) ).
cnf(c_3116,plain,
ld(mult(A,A),mult(mult(mult(A,A),mult(A,A)),A)) = mult(mult(mult(A,A),mult(A,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_81,c_73]) ).
cnf(c_3117,plain,
ld(mult(A,A),mult(mult(A,mult(mult(A,A),A)),A)) = mult(mult(mult(A,A),mult(A,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_29,c_3116]) ).
cnf(c_3118,plain,
ld(mult(A,A),mult(mult(A,mult(A,mult(A,A))),A)) = mult(mult(mult(A,A),mult(A,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_43,c_3117]) ).
cnf(c_3119,plain,
ld(mult(A,A),mult(A,mult(A,mult(mult(A,A),A)))) = mult(mult(mult(A,A),mult(A,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_38,c_3118]) ).
cnf(c_3120,plain,
ld(mult(A,A),mult(A,mult(A,mult(A,mult(A,A))))) = mult(mult(mult(A,A),mult(A,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_43,c_3119]) ).
cnf(c_3121,plain,
ld(mult(A,A),mult(A,mult(A,mult(A,mult(A,A))))) = mult(mult(A,mult(mult(A,A),A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_29,c_3120]) ).
cnf(c_91,plain,
ld(mult(A,A),mult(A,mult(A,mult(A,mult(A,A))))) = mult(mult(A,mult(A,mult(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_43,c_3121]) ).
cnf(c_3122,plain,
ld(rd(unit,A),rd(unit,A)) = mult(mult(rd(unit,A),rd(unit,A)),ld(rd(unit,A),A)),
inference(paramod,[status(thm)],[c_84,c_73]) ).
cnf(c_3123,plain,
unit = mult(mult(rd(unit,A),rd(unit,A)),ld(rd(unit,A),A)),
inference(paramod,[status(thm)],[c_14,c_3122]) ).
cnf(c_108,plain,
mult(mult(rd(unit,A),rd(unit,A)),ld(rd(unit,A),A)) = unit,
inference(copy,[status(thm)],[c_3123]) ).
cnf(c_110,plain,
ld(mult(rd(unit,A),rd(unit,A)),unit) = ld(rd(unit,A),A),
inference(paramod,[status(thm)],[c_108,c_2]) ).
cnf(c_3124,plain,
ld(mult(A,rd(unit,ld(A,unit))),unit) = ld(rd(unit,ld(A,unit)),ld(A,unit)),
inference(paramod,[status(thm)],[c_13,c_110]) ).
cnf(c_3125,plain,
ld(mult(A,A),unit) = ld(rd(unit,ld(A,unit)),ld(A,unit)),
inference(paramod,[status(thm)],[c_13,c_3124]) ).
cnf(c_117,plain,
ld(mult(A,A),unit) = ld(A,ld(A,unit)),
inference(paramod,[status(thm)],[c_13,c_3125]) ).
cnf(c_121,plain,
ld(mult(A,mult(A,mult(A,A))),mult(A,A)) = ld(A,ld(A,unit)),
inference(paramod,[status(thm)],[c_117,c_90]) ).
cnf(c_157,plain,
ld(mult(A,A),mult(A,B)) = mult(A,ld(mult(A,A),B)),
inference(paramod,[status(thm)],[c_1,c_40]) ).
cnf(c_3126,plain,
mult(A,ld(mult(A,A),mult(A,mult(A,mult(A,A))))) = mult(mult(A,mult(A,mult(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_157,c_91]) ).
cnf(c_3127,plain,
mult(A,mult(A,ld(mult(A,A),mult(A,mult(A,A))))) = mult(mult(A,mult(A,mult(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_157,c_3126]) ).
cnf(c_3128,plain,
mult(A,mult(A,mult(A,ld(mult(A,A),mult(A,A))))) = mult(mult(A,mult(A,mult(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_157,c_3127]) ).
cnf(c_3129,plain,
mult(A,mult(A,mult(A,unit))) = mult(mult(A,mult(A,mult(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_14,c_3128]) ).
cnf(c_3130,plain,
mult(A,mult(A,A)) = mult(mult(A,mult(A,mult(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_5,c_3129]) ).
cnf(c_159,plain,
mult(mult(A,mult(A,mult(A,A))),ld(A,unit)) = mult(A,mult(A,A)),
inference(copy,[status(thm)],[c_3130]) ).
cnf(c_3131,plain,
ld(mult(A,A),B) = mult(A,ld(mult(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_1,c_157]) ).
cnf(c_161,plain,
mult(A,ld(mult(A,A),ld(A,B))) = ld(mult(A,A),B),
inference(copy,[status(thm)],[c_3131]) ).
cnf(c_3132,plain,
ld(mult(rd(A,B),rd(A,B)),A) = mult(rd(A,B),ld(mult(rd(A,B),rd(A,B)),B)),
inference(paramod,[status(thm)],[c_3,c_157]) ).
cnf(c_162,plain,
mult(rd(A,B),ld(mult(rd(A,B),rd(A,B)),B)) = ld(mult(rd(A,B),rd(A,B)),A),
inference(copy,[status(thm)],[c_3132]) ).
cnf(c_164,plain,
rd(mult(A,B),mult(A,ld(mult(A,A),B))) = mult(A,A),
inference(paramod,[status(thm)],[c_157,c_13]) ).
cnf(c_3133,plain,
ld(mult(mult(A,A),mult(A,A)),mult(A,mult(A,A))) = mult(mult(A,A),ld(mult(mult(A,A),mult(A,A)),A)),
inference(paramod,[status(thm)],[c_43,c_157]) ).
cnf(c_3134,plain,
ld(mult(A,mult(mult(A,A),A)),mult(A,mult(A,A))) = mult(mult(A,A),ld(mult(mult(A,A),mult(A,A)),A)),
inference(paramod,[status(thm)],[c_29,c_3133]) ).
cnf(c_3135,plain,
ld(mult(A,mult(A,mult(A,A))),mult(A,mult(A,A))) = mult(mult(A,A),ld(mult(mult(A,A),mult(A,A)),A)),
inference(paramod,[status(thm)],[c_43,c_3134]) ).
cnf(c_3136,plain,
ld(mult(A,mult(A,mult(A,A))),mult(A,mult(A,A))) = mult(mult(A,A),ld(mult(A,mult(mult(A,A),A)),A)),
inference(paramod,[status(thm)],[c_29,c_3135]) ).
cnf(c_167,plain,
ld(mult(A,mult(A,mult(A,A))),mult(A,mult(A,A))) = mult(mult(A,A),ld(mult(A,mult(A,mult(A,A))),A)),
inference(paramod,[status(thm)],[c_43,c_3136]) ).
cnf(c_3137,plain,
ld(A,ld(mult(A,A),B)) = ld(mult(A,A),ld(A,B)),
inference(paramod,[status(thm)],[c_161,c_2]) ).
cnf(c_174,plain,
ld(mult(A,A),ld(A,B)) = ld(A,ld(mult(A,A),B)),
inference(copy,[status(thm)],[c_3137]) ).
cnf(c_3138,plain,
mult(mult(mult(mult(A,A),B),A),A) = mult(A,mult(mult(mult(mult(A,A),ld(A,B)),A),A)),
inference(paramod,[status(thm)],[c_39,c_30]) ).
cnf(c_185,plain,
mult(A,mult(mult(mult(mult(A,A),ld(A,B)),A),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(copy,[status(thm)],[c_3138]) ).
cnf(c_3139,plain,
mult(mult(A,mult(ld(A,B),C)),ld(A,B)) = mult(B,mult(ld(A,B),mult(ld(ld(A,B),C),ld(A,B)))),
inference(paramod,[status(thm)],[c_1,c_32]) ).
cnf(c_189,plain,
mult(A,mult(ld(B,A),mult(ld(ld(B,A),C),ld(B,A)))) = mult(mult(B,mult(ld(B,A),C)),ld(B,A)),
inference(copy,[status(thm)],[c_3139]) ).
cnf(c_3140,plain,
mult(mult(A,B),A) = mult(mult(unit,A),mult(A,mult(ld(A,B),A))),
inference(paramod,[status(thm)],[c_6,c_32]) ).
cnf(c_3141,plain,
mult(mult(A,B),A) = mult(A,mult(A,mult(ld(A,B),A))),
inference(paramod,[status(thm)],[c_6,c_3140]) ).
cnf(c_197,plain,
mult(A,mult(A,mult(ld(A,B),A))) = mult(mult(A,B),A),
inference(copy,[status(thm)],[c_3141]) ).
cnf(c_3142,plain,
ld(A,mult(mult(A,mult(A,B)),A)) = mult(mult(A,A),ld(A,mult(A,mult(ld(A,B),A)))),
inference(paramod,[status(thm)],[c_32,c_73]) ).
cnf(c_3143,plain,
ld(A,mult(A,mult(A,mult(B,A)))) = mult(mult(A,A),ld(A,mult(A,mult(ld(A,B),A)))),
inference(paramod,[status(thm)],[c_38,c_3142]) ).
cnf(c_3144,plain,
mult(A,mult(B,A)) = mult(mult(A,A),ld(A,mult(A,mult(ld(A,B),A)))),
inference(paramod,[status(thm)],[c_2,c_3143]) ).
cnf(c_3145,plain,
mult(A,mult(B,A)) = mult(mult(A,A),mult(ld(A,B),A)),
inference(paramod,[status(thm)],[c_2,c_3144]) ).
cnf(c_207,plain,
mult(mult(A,A),mult(ld(A,B),A)) = mult(A,mult(B,A)),
inference(copy,[status(thm)],[c_3145]) ).
cnf(c_3146,plain,
ld(mult(mult(rd(unit,A),rd(unit,A)),mult(rd(unit,A),rd(unit,A))),mult(rd(unit,A),rd(unit,A))) = mult(rd(unit,A),ld(mult(rd(unit,A),rd(unit,A)),A)),
inference(paramod,[status(thm)],[c_162,c_81]) ).
cnf(c_3147,plain,
ld(mult(rd(unit,A),mult(mult(rd(unit,A),rd(unit,A)),rd(unit,A))),mult(rd(unit,A),rd(unit,A))) = mult(rd(unit,A),ld(mult(rd(unit,A),rd(unit,A)),A)),
inference(paramod,[status(thm)],[c_29,c_3146]) ).
cnf(c_3148,plain,
ld(mult(rd(unit,A),mult(rd(unit,A),mult(rd(unit,A),rd(unit,A)))),mult(rd(unit,A),rd(unit,A))) = mult(rd(unit,A),ld(mult(rd(unit,A),rd(unit,A)),A)),
inference(paramod,[status(thm)],[c_43,c_3147]) ).
cnf(c_3149,plain,
ld(rd(unit,A),ld(rd(unit,A),unit)) = mult(rd(unit,A),ld(mult(rd(unit,A),rd(unit,A)),A)),
inference(paramod,[status(thm)],[c_121,c_3148]) ).
cnf(c_3150,plain,
ld(rd(unit,A),A) = mult(rd(unit,A),ld(mult(rd(unit,A),rd(unit,A)),A)),
inference(paramod,[status(thm)],[c_12,c_3149]) ).
cnf(c_270,plain,
mult(rd(unit,A),ld(mult(rd(unit,A),rd(unit,A)),A)) = ld(rd(unit,A),A),
inference(copy,[status(thm)],[c_3150]) ).
cnf(c_3151,plain,
ld(rd(unit,A),ld(rd(unit,A),A)) = ld(mult(rd(unit,A),rd(unit,A)),A),
inference(paramod,[status(thm)],[c_270,c_2]) ).
cnf(c_283,plain,
ld(mult(rd(unit,A),rd(unit,A)),A) = ld(rd(unit,A),ld(rd(unit,A),A)),
inference(copy,[status(thm)],[c_3151]) ).
cnf(c_3152,plain,
ld(mult(A,A),mult(A,mult(B,A))) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_207,c_2]) ).
cnf(c_333,plain,
mult(A,ld(mult(A,A),mult(B,A))) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_157,c_3152]) ).
cnf(c_3153,plain,
ld(A,mult(ld(A,B),A)) = ld(mult(A,A),mult(B,A)),
inference(paramod,[status(thm)],[c_333,c_2]) ).
cnf(c_348,plain,
ld(mult(A,A),mult(B,A)) = ld(A,mult(ld(A,B),A)),
inference(copy,[status(thm)],[c_3153]) ).
cnf(c_3154,plain,
mult(A,ld(mult(A,A),B)) = mult(ld(A,rd(B,A)),A),
inference(paramod,[status(thm)],[c_3,c_333]) ).
cnf(c_349,plain,
mult(ld(A,rd(B,A)),A) = mult(A,ld(mult(A,A),B)),
inference(copy,[status(thm)],[c_3154]) ).
cnf(c_3155,plain,
mult(A,ld(mult(A,A),A)) = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_6,c_333]) ).
cnf(c_3156,plain,
mult(A,ld(A,unit)) = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_81,c_3155]) ).
cnf(c_3157,plain,
unit = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_1,c_3156]) ).
cnf(c_350,plain,
mult(ld(A,unit),A) = unit,
inference(copy,[status(thm)],[c_3157]) ).
cnf(c_356,plain,
mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),A)) = mult(ld(ld(A,unit),mult(A,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_79,c_333]) ).
cnf(c_3158,plain,
mult(A,ld(mult(A,A),mult(A,mult(mult(B,A),A)))) = mult(ld(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_30,c_333]) ).
cnf(c_3159,plain,
mult(A,mult(A,ld(mult(A,A),mult(mult(B,A),A)))) = mult(ld(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_157,c_3158]) ).
cnf(c_3160,plain,
mult(A,mult(A,ld(A,mult(ld(A,mult(B,A)),A)))) = mult(ld(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_348,c_3159]) ).
cnf(c_3161,plain,
mult(A,mult(ld(A,mult(B,A)),A)) = mult(ld(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_1,c_3160]) ).
cnf(c_364,plain,
mult(ld(A,mult(mult(A,B),A)),A) = mult(A,mult(ld(A,mult(B,A)),A)),
inference(copy,[status(thm)],[c_3161]) ).
cnf(c_3162,plain,
mult(mult(A,mult(mult(B,A),A)),A) = mult(mult(mult(mult(A,rd(B,A)),A),A),mult(A,A)),
inference(paramod,[status(thm)],[c_26,c_37]) ).
cnf(c_3163,plain,
mult(mult(A,mult(mult(B,A),A)),A) = mult(mult(A,mult(mult(rd(B,A),A),A)),mult(A,A)),
inference(paramod,[status(thm)],[c_30,c_3162]) ).
cnf(c_376,plain,
mult(mult(A,mult(mult(B,A),A)),A) = mult(mult(A,mult(B,A)),mult(A,A)),
inference(paramod,[status(thm)],[c_3,c_3163]) ).
cnf(c_3164,plain,
mult(mult(A,mult(A,mult(mult(ld(A,B),A),A))),A) = mult(A,mult(mult(B,A),mult(A,A))),
inference(paramod,[status(thm)],[c_18,c_38]) ).
cnf(c_3165,plain,
mult(mult(A,mult(mult(B,A),A)),A) = mult(A,mult(mult(B,A),mult(A,A))),
inference(paramod,[status(thm)],[c_56,c_3164]) ).
cnf(c_379,plain,
mult(mult(A,mult(B,A)),mult(A,A)) = mult(A,mult(mult(B,A),mult(A,A))),
inference(paramod,[status(thm)],[c_376,c_3165]) ).
cnf(c_383,plain,
mult(mult(A,mult(mult(B,A),A)),A) = mult(A,mult(mult(B,A),mult(A,A))),
inference(paramod,[status(thm)],[c_379,c_376]) ).
cnf(c_389,plain,
ld(ld(A,unit),unit) = A,
inference(paramod,[status(thm)],[c_350,c_2]) ).
cnf(c_390,plain,
rd(unit,A) = ld(A,unit),
inference(paramod,[status(thm)],[c_350,c_4]) ).
cnf(c_3166,plain,
ld(mult(ld(A,unit),ld(A,unit)),unit) = mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),A)),
inference(paramod,[status(thm)],[c_350,c_157]) ).
cnf(c_3167,plain,
ld(ld(A,unit),ld(ld(A,unit),unit)) = mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),A)),
inference(paramod,[status(thm)],[c_117,c_3166]) ).
cnf(c_3168,plain,
ld(ld(A,unit),A) = mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),A)),
inference(paramod,[status(thm)],[c_389,c_3167]) ).
cnf(c_3169,plain,
ld(ld(A,unit),A) = mult(ld(ld(A,unit),mult(A,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_356,c_3168]) ).
cnf(c_396,plain,
mult(ld(ld(A,unit),mult(A,A)),ld(A,unit)) = ld(ld(A,unit),A),
inference(copy,[status(thm)],[c_3169]) ).
cnf(c_3170,plain,
rd(unit,mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),A))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_350,c_164]) ).
cnf(c_3171,plain,
rd(unit,mult(ld(ld(A,unit),mult(A,A)),ld(A,unit))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_356,c_3170]) ).
cnf(c_3172,plain,
rd(unit,ld(ld(A,unit),A)) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_396,c_3171]) ).
cnf(c_401,plain,
ld(ld(ld(A,unit),A),unit) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_390,c_3172]) ).
cnf(c_3173,plain,
mult(unit,A) = mult(mult(ld(mult(A,A),unit),A),mult(A,A)),
inference(paramod,[status(thm)],[c_350,c_37]) ).
cnf(c_3174,plain,
A = mult(mult(ld(mult(A,A),unit),A),mult(A,A)),
inference(paramod,[status(thm)],[c_6,c_3173]) ).
cnf(c_3175,plain,
A = mult(mult(ld(A,ld(A,unit)),A),mult(A,A)),
inference(paramod,[status(thm)],[c_117,c_3174]) ).
cnf(c_404,plain,
mult(mult(ld(A,ld(A,unit)),A),mult(A,A)) = A,
inference(copy,[status(thm)],[c_3175]) ).
cnf(c_3176,plain,
ld(mult(ld(A,unit),rd(unit,A)),A) = ld(rd(unit,A),ld(rd(unit,A),A)),
inference(paramod,[status(thm)],[c_390,c_283]) ).
cnf(c_3177,plain,
ld(mult(ld(A,unit),ld(A,unit)),A) = ld(rd(unit,A),ld(rd(unit,A),A)),
inference(paramod,[status(thm)],[c_390,c_3176]) ).
cnf(c_3178,plain,
ld(mult(ld(A,unit),ld(A,unit)),A) = ld(ld(A,unit),ld(rd(unit,A),A)),
inference(paramod,[status(thm)],[c_390,c_3177]) ).
cnf(c_413,plain,
ld(mult(ld(A,unit),ld(A,unit)),A) = ld(ld(A,unit),ld(ld(A,unit),A)),
inference(paramod,[status(thm)],[c_390,c_3178]) ).
cnf(c_3179,plain,
ld(mult(mult(A,A),mult(A,A)),mult(A,mult(A,A))) = ld(mult(A,A),mult(ld(A,unit),mult(A,A))),
inference(paramod,[status(thm)],[c_81,c_348]) ).
cnf(c_3180,plain,
ld(mult(A,mult(mult(A,A),A)),mult(A,mult(A,A))) = ld(mult(A,A),mult(ld(A,unit),mult(A,A))),
inference(paramod,[status(thm)],[c_29,c_3179]) ).
cnf(c_3181,plain,
ld(mult(A,mult(A,mult(A,A))),mult(A,mult(A,A))) = ld(mult(A,A),mult(ld(A,unit),mult(A,A))),
inference(paramod,[status(thm)],[c_43,c_3180]) ).
cnf(c_438,plain,
mult(mult(A,A),ld(mult(A,mult(A,mult(A,A))),A)) = ld(mult(A,A),mult(ld(A,unit),mult(A,A))),
inference(paramod,[status(thm)],[c_167,c_3181]) ).
cnf(c_3182,plain,
ld(mult(A,A),mult(A,mult(A,mult(B,A)))) = ld(A,mult(ld(A,mult(A,mult(A,B))),A)),
inference(paramod,[status(thm)],[c_38,c_348]) ).
cnf(c_3183,plain,
mult(A,ld(mult(A,A),mult(A,mult(B,A)))) = ld(A,mult(ld(A,mult(A,mult(A,B))),A)),
inference(paramod,[status(thm)],[c_157,c_3182]) ).
cnf(c_3184,plain,
mult(A,mult(A,ld(mult(A,A),mult(B,A)))) = ld(A,mult(ld(A,mult(A,mult(A,B))),A)),
inference(paramod,[status(thm)],[c_157,c_3183]) ).
cnf(c_3185,plain,
mult(A,mult(A,ld(A,mult(ld(A,B),A)))) = ld(A,mult(ld(A,mult(A,mult(A,B))),A)),
inference(paramod,[status(thm)],[c_348,c_3184]) ).
cnf(c_3186,plain,
mult(A,mult(ld(A,B),A)) = ld(A,mult(ld(A,mult(A,mult(A,B))),A)),
inference(paramod,[status(thm)],[c_1,c_3185]) ).
cnf(c_3187,plain,
mult(A,mult(ld(A,B),A)) = ld(A,mult(mult(A,B),A)),
inference(paramod,[status(thm)],[c_2,c_3186]) ).
cnf(c_449,plain,
ld(A,mult(mult(A,B),A)) = mult(A,mult(ld(A,B),A)),
inference(copy,[status(thm)],[c_3187]) ).
cnf(c_3188,plain,
mult(mult(A,mult(ld(A,B),A)),A) = mult(A,mult(ld(A,mult(B,A)),A)),
inference(paramod,[status(thm)],[c_449,c_364]) ).
cnf(c_453,plain,
mult(A,mult(ld(A,mult(B,A)),A)) = mult(mult(A,mult(ld(A,B),A)),A),
inference(copy,[status(thm)],[c_3188]) ).
cnf(c_456,plain,
rd(mult(A,ld(mult(A,A),B)),A) = ld(A,rd(B,A)),
inference(paramod,[status(thm)],[c_349,c_4]) ).
cnf(c_3189,plain,
mult(mult(mult(A,ld(A,rd(B,A))),A),mult(A,C)) = mult(A,mult(mult(mult(A,ld(mult(A,A),B)),A),C)),
inference(paramod,[status(thm)],[c_349,c_7]) ).
cnf(c_3190,plain,
mult(mult(rd(B,A),A),mult(A,C)) = mult(A,mult(mult(mult(A,ld(mult(A,A),B)),A),C)),
inference(paramod,[status(thm)],[c_1,c_3189]) ).
cnf(c_3191,plain,
mult(B,mult(A,C)) = mult(A,mult(mult(mult(A,ld(mult(A,A),B)),A),C)),
inference(paramod,[status(thm)],[c_3,c_3190]) ).
cnf(c_458,plain,
mult(A,mult(mult(mult(A,ld(mult(A,A),B)),A),C)) = mult(B,mult(A,C)),
inference(copy,[status(thm)],[c_3191]) ).
cnf(c_3192,plain,
mult(ld(A,rd(unit,A)),A) = mult(A,ld(A,ld(A,unit))),
inference(paramod,[status(thm)],[c_117,c_349]) ).
cnf(c_3193,plain,
mult(ld(A,ld(A,unit)),A) = mult(A,ld(A,ld(A,unit))),
inference(paramod,[status(thm)],[c_390,c_3192]) ).
cnf(c_464,plain,
mult(ld(A,ld(A,unit)),A) = ld(A,unit),
inference(paramod,[status(thm)],[c_1,c_3193]) ).
cnf(c_483,plain,
mult(ld(A,unit),mult(A,A)) = A,
inference(paramod,[status(thm)],[c_464,c_404]) ).
cnf(c_3194,plain,
mult(mult(A,A),ld(mult(A,mult(A,mult(A,A))),A)) = ld(mult(A,A),A),
inference(paramod,[status(thm)],[c_483,c_438]) ).
cnf(c_491,plain,
mult(mult(A,A),ld(mult(A,mult(A,mult(A,A))),A)) = ld(A,unit),
inference(paramod,[status(thm)],[c_81,c_3194]) ).
cnf(c_509,plain,
ld(ld(A,unit),A) = mult(A,A),
inference(paramod,[status(thm)],[c_483,c_2]) ).
cnf(c_510,plain,
rd(A,mult(A,A)) = ld(A,unit),
inference(paramod,[status(thm)],[c_483,c_4]) ).
cnf(c_3195,plain,
mult(A,mult(rd(unit,A),rd(unit,A))) = rd(unit,A),
inference(paramod,[status(thm)],[c_12,c_483]) ).
cnf(c_3196,plain,
mult(A,mult(ld(A,unit),rd(unit,A))) = rd(unit,A),
inference(paramod,[status(thm)],[c_390,c_3195]) ).
cnf(c_3197,plain,
mult(A,mult(ld(A,unit),ld(A,unit))) = rd(unit,A),
inference(paramod,[status(thm)],[c_390,c_3196]) ).
cnf(c_514,plain,
mult(A,mult(ld(A,unit),ld(A,unit))) = ld(A,unit),
inference(paramod,[status(thm)],[c_390,c_3197]) ).
cnf(c_3198,plain,
ld(mult(ld(A,unit),ld(A,unit)),A) = mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),mult(A,A))),
inference(paramod,[status(thm)],[c_483,c_157]) ).
cnf(c_3199,plain,
ld(ld(A,unit),ld(ld(A,unit),A)) = mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),mult(A,A))),
inference(paramod,[status(thm)],[c_413,c_3198]) ).
cnf(c_3200,plain,
ld(ld(A,unit),mult(A,A)) = mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),mult(A,A))),
inference(paramod,[status(thm)],[c_509,c_3199]) ).
cnf(c_519,plain,
mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),mult(A,A))) = ld(ld(A,unit),mult(A,A)),
inference(copy,[status(thm)],[c_3200]) ).
cnf(c_3201,plain,
mult(mult(A,B),ld(B,unit)) = mult(mult(A,ld(B,unit)),mult(ld(B,unit),mult(ld(ld(B,unit),mult(B,B)),ld(B,unit)))),
inference(paramod,[status(thm)],[c_483,c_32]) ).
cnf(c_3202,plain,
mult(mult(A,B),ld(B,unit)) = mult(mult(A,ld(B,unit)),mult(ld(B,unit),ld(ld(B,unit),B))),
inference(paramod,[status(thm)],[c_396,c_3201]) ).
cnf(c_3203,plain,
mult(mult(A,B),ld(B,unit)) = mult(mult(A,ld(B,unit)),mult(ld(B,unit),mult(B,B))),
inference(paramod,[status(thm)],[c_509,c_3202]) ).
cnf(c_3204,plain,
mult(mult(A,B),ld(B,unit)) = mult(mult(A,ld(B,unit)),B),
inference(paramod,[status(thm)],[c_483,c_3203]) ).
cnf(c_520,plain,
mult(mult(A,ld(B,unit)),B) = mult(mult(A,B),ld(B,unit)),
inference(copy,[status(thm)],[c_3204]) ).
cnf(c_3205,plain,
rd(A,mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),mult(A,A)))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_483,c_164]) ).
cnf(c_523,plain,
rd(A,ld(ld(A,unit),mult(A,A))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_519,c_3205]) ).
cnf(c_3206,plain,
mult(mult(rd(unit,A),ld(mult(rd(unit,A),rd(unit,A)),A)),mult(mult(rd(unit,A),rd(unit,A)),mult(rd(unit,A),rd(unit,A)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_162,c_483]) ).
cnf(c_3207,plain,
mult(mult(ld(A,unit),ld(mult(rd(unit,A),rd(unit,A)),A)),mult(mult(rd(unit,A),rd(unit,A)),mult(rd(unit,A),rd(unit,A)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_390,c_3206]) ).
cnf(c_3208,plain,
mult(mult(ld(A,unit),ld(mult(ld(A,unit),rd(unit,A)),A)),mult(mult(rd(unit,A),rd(unit,A)),mult(rd(unit,A),rd(unit,A)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_390,c_3207]) ).
cnf(c_3209,plain,
mult(mult(ld(A,unit),ld(mult(ld(A,unit),ld(A,unit)),A)),mult(mult(rd(unit,A),rd(unit,A)),mult(rd(unit,A),rd(unit,A)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_390,c_3208]) ).
cnf(c_3210,plain,
mult(mult(ld(A,unit),ld(ld(A,unit),ld(ld(A,unit),A))),mult(mult(rd(unit,A),rd(unit,A)),mult(rd(unit,A),rd(unit,A)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_413,c_3209]) ).
cnf(c_3211,plain,
mult(mult(ld(A,unit),ld(ld(A,unit),mult(A,A))),mult(mult(rd(unit,A),rd(unit,A)),mult(rd(unit,A),rd(unit,A)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_509,c_3210]) ).
cnf(c_3212,plain,
mult(mult(A,A),mult(mult(rd(unit,A),rd(unit,A)),mult(rd(unit,A),rd(unit,A)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_1,c_3211]) ).
cnf(c_3213,plain,
mult(mult(A,A),mult(mult(ld(A,unit),rd(unit,A)),mult(rd(unit,A),rd(unit,A)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_390,c_3212]) ).
cnf(c_3214,plain,
mult(mult(A,A),mult(mult(ld(A,unit),ld(A,unit)),mult(rd(unit,A),rd(unit,A)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_390,c_3213]) ).
cnf(c_3215,plain,
mult(mult(A,A),mult(mult(ld(A,unit),ld(A,unit)),mult(ld(A,unit),rd(unit,A)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_390,c_3214]) ).
cnf(c_3216,plain,
mult(mult(A,A),mult(mult(ld(A,unit),ld(A,unit)),mult(ld(A,unit),ld(A,unit)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_390,c_3215]) ).
cnf(c_3217,plain,
mult(mult(A,A),mult(ld(A,unit),mult(mult(ld(A,unit),ld(A,unit)),ld(A,unit)))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_29,c_3216]) ).
cnf(c_3218,plain,
mult(mult(A,A),mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))))) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_43,c_3217]) ).
cnf(c_3219,plain,
mult(mult(A,A),mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))))) = mult(ld(A,unit),rd(unit,A)),
inference(paramod,[status(thm)],[c_390,c_3218]) ).
cnf(c_524,plain,
mult(mult(A,A),mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_390,c_3219]) ).
cnf(c_3220,plain,
ld(mult(mult(A,A),mult(A,A)),A) = ld(mult(A,A),mult(ld(mult(A,A),ld(A,unit)),mult(A,A))),
inference(paramod,[status(thm)],[c_483,c_348]) ).
cnf(c_3221,plain,
ld(mult(A,mult(mult(A,A),A)),A) = ld(mult(A,A),mult(ld(mult(A,A),ld(A,unit)),mult(A,A))),
inference(paramod,[status(thm)],[c_29,c_3220]) ).
cnf(c_3222,plain,
ld(mult(A,mult(A,mult(A,A))),A) = ld(mult(A,A),mult(ld(mult(A,A),ld(A,unit)),mult(A,A))),
inference(paramod,[status(thm)],[c_43,c_3221]) ).
cnf(c_3223,plain,
ld(mult(A,mult(A,mult(A,A))),A) = ld(mult(A,A),mult(ld(A,ld(mult(A,A),unit)),mult(A,A))),
inference(paramod,[status(thm)],[c_174,c_3222]) ).
cnf(c_527,plain,
ld(mult(A,mult(A,mult(A,A))),A) = ld(mult(A,A),mult(ld(A,ld(A,ld(A,unit))),mult(A,A))),
inference(paramod,[status(thm)],[c_117,c_3223]) ).
cnf(c_535,plain,
ld(mult(ld(A,unit),ld(A,unit)),A) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_509,c_413]) ).
cnf(c_3224,plain,
ld(mult(A,A),unit) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_509,c_401]) ).
cnf(c_540,plain,
ld(A,ld(A,unit)) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_117,c_3224]) ).
cnf(c_541,plain,
mult(ld(ld(A,unit),mult(A,A)),ld(A,unit)) = mult(A,A),
inference(paramod,[status(thm)],[c_509,c_396]) ).
cnf(c_3225,plain,
mult(mult(A,A),ld(mult(A,A),mult(ld(A,ld(A,ld(A,unit))),mult(A,A)))) = ld(A,unit),
inference(paramod,[status(thm)],[c_527,c_491]) ).
cnf(c_3226,plain,
mult(mult(A,A),ld(mult(A,A),mult(ld(A,mult(ld(A,unit),ld(A,unit))),mult(A,A)))) = ld(A,unit),
inference(paramod,[status(thm)],[c_540,c_3225]) ).
cnf(c_547,plain,
mult(ld(A,mult(ld(A,unit),ld(A,unit))),mult(A,A)) = ld(A,unit),
inference(paramod,[status(thm)],[c_1,c_3226]) ).
cnf(c_3227,plain,
ld(mult(A,mult(A,mult(A,A))),A) = ld(mult(A,A),mult(ld(A,mult(ld(A,unit),ld(A,unit))),mult(A,A))),
inference(paramod,[status(thm)],[c_540,c_527]) ).
cnf(c_3228,plain,
ld(mult(A,mult(A,mult(A,A))),A) = ld(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_547,c_3227]) ).
cnf(c_3229,plain,
ld(mult(A,mult(A,mult(A,A))),A) = ld(A,ld(mult(A,A),unit)),
inference(paramod,[status(thm)],[c_174,c_3228]) ).
cnf(c_3230,plain,
ld(mult(A,mult(A,mult(A,A))),A) = ld(A,ld(A,ld(A,unit))),
inference(paramod,[status(thm)],[c_117,c_3229]) ).
cnf(c_550,plain,
ld(mult(A,mult(A,mult(A,A))),A) = ld(A,mult(ld(A,unit),ld(A,unit))),
inference(paramod,[status(thm)],[c_540,c_3230]) ).
cnf(c_565,plain,
ld(mult(A,A),unit) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_540,c_117]) ).
cnf(c_3231,plain,
ld(ld(mult(A,A),unit),mult(A,A)) = mult(A,mult(mult(A,A),A)),
inference(paramod,[status(thm)],[c_29,c_509]) ).
cnf(c_3232,plain,
ld(mult(ld(A,unit),ld(A,unit)),mult(A,A)) = mult(A,mult(mult(A,A),A)),
inference(paramod,[status(thm)],[c_565,c_3231]) ).
cnf(c_577,plain,
ld(mult(ld(A,unit),ld(A,unit)),mult(A,A)) = mult(A,mult(A,mult(A,A))),
inference(paramod,[status(thm)],[c_43,c_3232]) ).
cnf(c_3233,plain,
mult(ld(A,unit),mult(A,mult(A,mult(A,A)))) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_577,c_519]) ).
cnf(c_580,plain,
ld(ld(A,unit),mult(A,A)) = mult(ld(A,unit),mult(A,mult(A,mult(A,A)))),
inference(copy,[status(thm)],[c_3233]) ).
cnf(c_583,plain,
mult(mult(ld(A,unit),mult(A,mult(A,mult(A,A)))),ld(A,unit)) = mult(A,A),
inference(paramod,[status(thm)],[c_580,c_541]) ).
cnf(c_584,plain,
ld(mult(ld(A,unit),ld(A,unit)),A) = mult(ld(A,unit),mult(A,mult(A,mult(A,A)))),
inference(paramod,[status(thm)],[c_580,c_535]) ).
cnf(c_585,plain,
rd(A,mult(ld(A,unit),mult(A,mult(A,mult(A,A))))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_580,c_523]) ).
cnf(c_3234,plain,
ld(mult(A,A),mult(A,ld(mult(A,A),unit))) = mult(A,mult(ld(mult(A,A),unit),ld(mult(A,A),unit))),
inference(paramod,[status(thm)],[c_540,c_157]) ).
cnf(c_3235,plain,
ld(mult(A,A),mult(A,mult(ld(A,unit),ld(A,unit)))) = mult(A,mult(ld(mult(A,A),unit),ld(mult(A,A),unit))),
inference(paramod,[status(thm)],[c_565,c_3234]) ).
cnf(c_3236,plain,
ld(mult(A,A),ld(A,unit)) = mult(A,mult(ld(mult(A,A),unit),ld(mult(A,A),unit))),
inference(paramod,[status(thm)],[c_514,c_3235]) ).
cnf(c_3237,plain,
ld(A,ld(mult(A,A),unit)) = mult(A,mult(ld(mult(A,A),unit),ld(mult(A,A),unit))),
inference(paramod,[status(thm)],[c_174,c_3236]) ).
cnf(c_3238,plain,
ld(A,mult(ld(A,unit),ld(A,unit))) = mult(A,mult(ld(mult(A,A),unit),ld(mult(A,A),unit))),
inference(paramod,[status(thm)],[c_565,c_3237]) ).
cnf(c_3239,plain,
ld(A,mult(ld(A,unit),ld(A,unit))) = mult(A,mult(mult(ld(A,unit),ld(A,unit)),ld(mult(A,A),unit))),
inference(paramod,[status(thm)],[c_565,c_3238]) ).
cnf(c_3240,plain,
ld(A,mult(ld(A,unit),ld(A,unit))) = mult(A,mult(mult(ld(A,unit),ld(A,unit)),mult(ld(A,unit),ld(A,unit)))),
inference(paramod,[status(thm)],[c_565,c_3239]) ).
cnf(c_3241,plain,
ld(A,mult(ld(A,unit),ld(A,unit))) = mult(A,mult(ld(A,unit),mult(mult(ld(A,unit),ld(A,unit)),ld(A,unit)))),
inference(paramod,[status(thm)],[c_29,c_3240]) ).
cnf(c_587,plain,
ld(A,mult(ld(A,unit),ld(A,unit))) = mult(A,mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))))),
inference(paramod,[status(thm)],[c_43,c_3241]) ).
cnf(c_593,plain,
ld(mult(A,mult(A,mult(A,A))),A) = mult(A,mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))))),
inference(paramod,[status(thm)],[c_587,c_550]) ).
cnf(c_3242,plain,
mult(A,mult(A,mult(B,A))) = mult(A,mult(mult(A,mult(A,A)),mult(ld(mult(A,A),B),A))),
inference(paramod,[status(thm)],[c_1,c_51]) ).
cnf(c_600,plain,
mult(A,mult(mult(A,mult(A,A)),mult(ld(mult(A,A),B),A))) = mult(A,mult(A,mult(B,A))),
inference(copy,[status(thm)],[c_3242]) ).
cnf(c_3243,plain,
ld(A,mult(A,mult(mult(A,mult(A,A)),mult(B,A)))) = mult(A,mult(mult(mult(A,A),B),A)),
inference(paramod,[status(thm)],[c_51,c_2]) ).
cnf(c_3244,plain,
mult(mult(A,mult(A,A)),mult(B,A)) = mult(A,mult(mult(mult(A,A),B),A)),
inference(paramod,[status(thm)],[c_2,c_3243]) ).
cnf(c_601,plain,
mult(A,mult(mult(mult(A,A),B),A)) = mult(mult(A,mult(A,A)),mult(B,A)),
inference(copy,[status(thm)],[c_3244]) ).
cnf(c_3245,plain,
mult(A,mult(ld(A,unit),ld(mult(mult(ld(ld(A,unit),mult(A,A)),ld(A,unit)),ld(A,unit)),B))) = mult(ld(A,unit),B),
inference(paramod,[status(thm)],[c_79,c_53]) ).
cnf(c_3246,plain,
mult(A,mult(ld(A,unit),ld(mult(mult(mult(ld(A,unit),mult(A,mult(A,mult(A,A)))),ld(A,unit)),ld(A,unit)),B))) = mult(ld(A,unit),B),
inference(paramod,[status(thm)],[c_580,c_3245]) ).
cnf(c_3247,plain,
mult(A,mult(ld(A,unit),ld(mult(mult(A,A),ld(A,unit)),B))) = mult(ld(A,unit),B),
inference(paramod,[status(thm)],[c_583,c_3246]) ).
cnf(c_607,plain,
mult(A,mult(ld(A,unit),ld(A,B))) = mult(ld(A,unit),B),
inference(paramod,[status(thm)],[c_79,c_3247]) ).
cnf(c_3248,plain,
rd(mult(A,B),A) = ld(A,rd(mult(mult(A,A),B),A)),
inference(paramod,[status(thm)],[c_2,c_456]) ).
cnf(c_656,plain,
ld(A,rd(mult(mult(A,A),B),A)) = rd(mult(A,B),A),
inference(copy,[status(thm)],[c_3248]) ).
cnf(c_3249,plain,
rd(mult(mult(A,A),ld(mult(mult(A,A),mult(A,A)),A)),mult(A,A)) = ld(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_510,c_456]) ).
cnf(c_3250,plain,
rd(mult(mult(A,A),ld(mult(A,mult(mult(A,A),A)),A)),mult(A,A)) = ld(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_29,c_3249]) ).
cnf(c_3251,plain,
rd(mult(mult(A,A),ld(mult(A,mult(A,mult(A,A))),A)),mult(A,A)) = ld(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_43,c_3250]) ).
cnf(c_3252,plain,
rd(mult(mult(A,A),mult(A,mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit)))))),mult(A,A)) = ld(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_593,c_3251]) ).
cnf(c_3253,plain,
rd(mult(A,mult(mult(A,A),mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit)))))),mult(A,A)) = ld(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_29,c_3252]) ).
cnf(c_3254,plain,
rd(mult(A,mult(ld(A,unit),ld(A,unit))),mult(A,A)) = ld(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_524,c_3253]) ).
cnf(c_3255,plain,
rd(mult(ld(A,unit),unit),mult(A,A)) = ld(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_607,c_3254]) ).
cnf(c_3256,plain,
rd(ld(A,unit),mult(A,A)) = ld(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_5,c_3255]) ).
cnf(c_3257,plain,
rd(ld(A,unit),mult(A,A)) = ld(A,ld(mult(A,A),unit)),
inference(paramod,[status(thm)],[c_174,c_3256]) ).
cnf(c_3258,plain,
rd(ld(A,unit),mult(A,A)) = ld(A,mult(ld(A,unit),ld(A,unit))),
inference(paramod,[status(thm)],[c_565,c_3257]) ).
cnf(c_662,plain,
rd(ld(A,unit),mult(A,A)) = mult(A,mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))))),
inference(paramod,[status(thm)],[c_587,c_3258]) ).
cnf(c_677,plain,
ld(A,mult(ld(A,unit),B)) = mult(ld(A,unit),ld(A,B)),
inference(paramod,[status(thm)],[c_607,c_2]) ).
cnf(c_3259,plain,
mult(A,mult(ld(A,unit),B)) = mult(ld(A,unit),mult(A,B)),
inference(paramod,[status(thm)],[c_2,c_607]) ).
cnf(c_678,plain,
mult(ld(A,unit),mult(A,B)) = mult(A,mult(ld(A,unit),B)),
inference(copy,[status(thm)],[c_3259]) ).
cnf(c_3260,plain,
mult(ld(A,unit),ld(A,ld(A,unit))) = mult(A,mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))))),
inference(paramod,[status(thm)],[c_677,c_587]) ).
cnf(c_3261,plain,
mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))) = mult(A,mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))))),
inference(paramod,[status(thm)],[c_540,c_3260]) ).
cnf(c_711,plain,
mult(A,mult(ld(A,unit),mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))))) = mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))),
inference(copy,[status(thm)],[c_3261]) ).
cnf(c_3262,plain,
rd(A,mult(A,mult(ld(A,unit),mult(A,mult(A,A))))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_678,c_585]) ).
cnf(c_3263,plain,
rd(A,mult(A,mult(A,mult(ld(A,unit),mult(A,A))))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_678,c_3262]) ).
cnf(c_715,plain,
rd(A,mult(A,mult(A,A))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_483,c_3263]) ).
cnf(c_3264,plain,
ld(mult(ld(A,unit),ld(A,unit)),A) = mult(A,mult(ld(A,unit),mult(A,mult(A,A)))),
inference(paramod,[status(thm)],[c_678,c_584]) ).
cnf(c_3265,plain,
ld(mult(ld(A,unit),ld(A,unit)),A) = mult(A,mult(A,mult(ld(A,unit),mult(A,A)))),
inference(paramod,[status(thm)],[c_678,c_3264]) ).
cnf(c_716,plain,
ld(mult(ld(A,unit),ld(A,unit)),A) = mult(A,mult(A,A)),
inference(paramod,[status(thm)],[c_483,c_3265]) ).
cnf(c_3266,plain,
mult(mult(A,mult(ld(A,unit),mult(A,mult(A,A)))),ld(A,unit)) = mult(A,A),
inference(paramod,[status(thm)],[c_678,c_583]) ).
cnf(c_3267,plain,
mult(mult(A,mult(A,mult(ld(A,unit),mult(A,A)))),ld(A,unit)) = mult(A,A),
inference(paramod,[status(thm)],[c_678,c_3266]) ).
cnf(c_717,plain,
mult(mult(A,mult(A,A)),ld(A,unit)) = mult(A,A),
inference(paramod,[status(thm)],[c_483,c_3267]) ).
cnf(c_725,plain,
rd(ld(A,unit),mult(A,A)) = mult(ld(A,unit),mult(ld(A,unit),ld(A,unit))),
inference(paramod,[status(thm)],[c_711,c_662]) ).
cnf(c_735,plain,
ld(A,mult(mult(B,A),C)) = mult(mult(mult(ld(A,B),A),A),ld(A,C)),
inference(paramod,[status(thm)],[c_1,c_54]) ).
cnf(c_3268,plain,
mult(mult(A,mult(B,mult(B,mult(ld(B,C),B)))),B) = mult(mult(A,B),mult(mult(C,B),B)),
inference(paramod,[status(thm)],[c_56,c_9]) ).
cnf(c_766,plain,
mult(mult(A,mult(mult(B,C),B)),B) = mult(mult(A,B),mult(mult(C,B),B)),
inference(paramod,[status(thm)],[c_197,c_3268]) ).
cnf(c_3269,plain,
ld(mult(A,A),mult(mult(B,A),A)) = mult(A,ld(mult(A,A),mult(mult(ld(A,B),A),A))),
inference(paramod,[status(thm)],[c_56,c_157]) ).
cnf(c_3270,plain,
ld(A,mult(ld(A,mult(B,A)),A)) = mult(A,ld(mult(A,A),mult(mult(ld(A,B),A),A))),
inference(paramod,[status(thm)],[c_348,c_3269]) ).
cnf(c_3271,plain,
ld(A,mult(ld(A,mult(B,A)),A)) = mult(A,ld(A,mult(ld(A,mult(ld(A,B),A)),A))),
inference(paramod,[status(thm)],[c_348,c_3270]) ).
cnf(c_770,plain,
ld(A,mult(ld(A,mult(B,A)),A)) = mult(ld(A,mult(ld(A,B),A)),A),
inference(paramod,[status(thm)],[c_1,c_3271]) ).
cnf(c_3272,plain,
ld(A,B) = mult(ld(A,unit),ld(A,ld(ld(A,unit),B))),
inference(paramod,[status(thm)],[c_1,c_677]) ).
cnf(c_782,plain,
mult(ld(A,unit),ld(A,ld(ld(A,unit),B))) = ld(A,B),
inference(copy,[status(thm)],[c_3272]) ).
cnf(c_3273,plain,
ld(rd(unit,A),mult(A,B)) = mult(ld(rd(unit,A),unit),ld(rd(unit,A),B)),
inference(paramod,[status(thm)],[c_12,c_677]) ).
cnf(c_3274,plain,
ld(ld(A,unit),mult(A,B)) = mult(ld(rd(unit,A),unit),ld(rd(unit,A),B)),
inference(paramod,[status(thm)],[c_390,c_3273]) ).
cnf(c_3275,plain,
ld(ld(A,unit),mult(A,B)) = mult(ld(ld(A,unit),unit),ld(rd(unit,A),B)),
inference(paramod,[status(thm)],[c_390,c_3274]) ).
cnf(c_3276,plain,
ld(ld(A,unit),mult(A,B)) = mult(A,ld(rd(unit,A),B)),
inference(paramod,[status(thm)],[c_389,c_3275]) ).
cnf(c_784,plain,
ld(ld(A,unit),mult(A,B)) = mult(A,ld(ld(A,unit),B)),
inference(paramod,[status(thm)],[c_390,c_3276]) ).
cnf(c_850,plain,
mult(mult(ld(A,unit),ld(A,unit)),mult(A,mult(A,A))) = A,
inference(paramod,[status(thm)],[c_715,c_3]) ).
cnf(c_3277,plain,
mult(ld(A,unit),mult(mult(mult(ld(ld(A,unit),mult(A,mult(A,A))),ld(A,unit)),ld(A,unit)),B)) = mult(mult(A,A),mult(ld(A,unit),B)),
inference(paramod,[status(thm)],[c_717,c_18]) ).
cnf(c_3278,plain,
mult(ld(A,unit),mult(mult(mult(mult(A,ld(ld(A,unit),mult(A,A))),ld(A,unit)),ld(A,unit)),B)) = mult(mult(A,A),mult(ld(A,unit),B)),
inference(paramod,[status(thm)],[c_784,c_3277]) ).
cnf(c_3279,plain,
mult(ld(A,unit),mult(mult(mult(mult(A,mult(A,ld(ld(A,unit),A))),ld(A,unit)),ld(A,unit)),B)) = mult(mult(A,A),mult(ld(A,unit),B)),
inference(paramod,[status(thm)],[c_784,c_3278]) ).
cnf(c_3280,plain,
mult(ld(A,unit),mult(mult(mult(mult(A,mult(A,mult(A,A))),ld(A,unit)),ld(A,unit)),B)) = mult(mult(A,A),mult(ld(A,unit),B)),
inference(paramod,[status(thm)],[c_509,c_3279]) ).
cnf(c_3281,plain,
mult(ld(A,unit),mult(mult(mult(A,mult(A,A)),ld(A,unit)),B)) = mult(mult(A,A),mult(ld(A,unit),B)),
inference(paramod,[status(thm)],[c_159,c_3280]) ).
cnf(c_873,plain,
mult(ld(A,unit),mult(mult(A,A),B)) = mult(mult(A,A),mult(ld(A,unit),B)),
inference(paramod,[status(thm)],[c_717,c_3281]) ).
cnf(c_3282,plain,
rd(A,mult(rd(unit,A),rd(unit,A))) = mult(ld(rd(unit,A),unit),mult(ld(rd(unit,A),unit),ld(rd(unit,A),unit))),
inference(paramod,[status(thm)],[c_12,c_725]) ).
cnf(c_3283,plain,
rd(A,mult(ld(A,unit),rd(unit,A))) = mult(ld(rd(unit,A),unit),mult(ld(rd(unit,A),unit),ld(rd(unit,A),unit))),
inference(paramod,[status(thm)],[c_390,c_3282]) ).
cnf(c_3284,plain,
rd(A,mult(ld(A,unit),ld(A,unit))) = mult(ld(rd(unit,A),unit),mult(ld(rd(unit,A),unit),ld(rd(unit,A),unit))),
inference(paramod,[status(thm)],[c_390,c_3283]) ).
cnf(c_3285,plain,
rd(A,mult(ld(A,unit),ld(A,unit))) = mult(ld(ld(A,unit),unit),mult(ld(rd(unit,A),unit),ld(rd(unit,A),unit))),
inference(paramod,[status(thm)],[c_390,c_3284]) ).
cnf(c_3286,plain,
rd(A,mult(ld(A,unit),ld(A,unit))) = mult(A,mult(ld(rd(unit,A),unit),ld(rd(unit,A),unit))),
inference(paramod,[status(thm)],[c_389,c_3285]) ).
cnf(c_3287,plain,
rd(A,mult(ld(A,unit),ld(A,unit))) = mult(A,mult(ld(ld(A,unit),unit),ld(rd(unit,A),unit))),
inference(paramod,[status(thm)],[c_390,c_3286]) ).
cnf(c_3288,plain,
rd(A,mult(ld(A,unit),ld(A,unit))) = mult(A,mult(A,ld(rd(unit,A),unit))),
inference(paramod,[status(thm)],[c_389,c_3287]) ).
cnf(c_3289,plain,
rd(A,mult(ld(A,unit),ld(A,unit))) = mult(A,mult(A,ld(ld(A,unit),unit))),
inference(paramod,[status(thm)],[c_390,c_3288]) ).
cnf(c_892,plain,
rd(A,mult(ld(A,unit),ld(A,unit))) = mult(A,mult(A,A)),
inference(paramod,[status(thm)],[c_389,c_3289]) ).
cnf(c_895,plain,
mult(mult(A,mult(A,A)),mult(ld(A,unit),ld(A,unit))) = A,
inference(paramod,[status(thm)],[c_892,c_3]) ).
cnf(c_3290,plain,
rd(mult(mult(mult(A,ld(A,rd(B,A))),A),C),mult(mult(mult(A,ld(mult(A,A),B)),A),ld(A,C))) = A,
inference(paramod,[status(thm)],[c_349,c_63]) ).
cnf(c_3291,plain,
rd(mult(mult(rd(B,A),A),C),mult(mult(mult(A,ld(mult(A,A),B)),A),ld(A,C))) = A,
inference(paramod,[status(thm)],[c_1,c_3290]) ).
cnf(c_916,plain,
rd(mult(A,B),mult(mult(mult(C,ld(mult(C,C),A)),C),ld(C,B))) = C,
inference(paramod,[status(thm)],[c_3,c_3291]) ).
cnf(c_3292,plain,
ld(A,mult(mult(A,B),A)) = mult(mult(mult(B,A),A),ld(A,unit)),
inference(paramod,[status(thm)],[c_64,c_2]) ).
cnf(c_3293,plain,
mult(A,mult(ld(A,B),A)) = mult(mult(mult(B,A),A),ld(A,unit)),
inference(paramod,[status(thm)],[c_449,c_3292]) ).
cnf(c_919,plain,
mult(mult(mult(A,B),B),ld(B,unit)) = mult(B,mult(ld(B,A),B)),
inference(copy,[status(thm)],[c_3293]) ).
cnf(c_3294,plain,
mult(A,mult(mult(mult(A,mult(mult(B,A),A)),A),ld(A,unit))) = mult(mult(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_30,c_64]) ).
cnf(c_3295,plain,
mult(A,mult(mult(A,mult(mult(B,A),mult(A,A))),ld(A,unit))) = mult(mult(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_383,c_3294]) ).
cnf(c_927,plain,
mult(A,mult(mult(A,mult(mult(B,A),mult(A,A))),ld(A,unit))) = mult(mult(A,A),mult(mult(B,A),A)),
inference(paramod,[status(thm)],[c_766,c_3295]) ).
cnf(c_3296,plain,
ld(A,mult(ld(A,B),A)) = mult(ld(A,mult(ld(A,rd(B,A)),A)),A),
inference(paramod,[status(thm)],[c_3,c_770]) ).
cnf(c_3297,plain,
ld(A,mult(ld(A,B),A)) = mult(ld(A,mult(A,ld(mult(A,A),B))),A),
inference(paramod,[status(thm)],[c_349,c_3296]) ).
cnf(c_3298,plain,
ld(A,mult(ld(A,B),A)) = mult(ld(mult(A,A),B),A),
inference(paramod,[status(thm)],[c_2,c_3297]) ).
cnf(c_951,plain,
mult(ld(mult(A,A),B),A) = ld(A,mult(ld(A,B),A)),
inference(copy,[status(thm)],[c_3298]) ).
cnf(c_3299,plain,
mult(A,mult(mult(A,mult(A,A)),ld(A,mult(ld(A,B),A)))) = mult(A,mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_951,c_600]) ).
cnf(c_972,plain,
mult(mult(A,mult(A,A)),mult(ld(A,B),A)) = mult(A,mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_67,c_3299]) ).
cnf(c_3300,plain,
mult(A,B) = ld(B,mult(ld(B,mult(mult(B,B),A)),B)),
inference(paramod,[status(thm)],[c_2,c_951]) ).
cnf(c_3301,plain,
mult(A,B) = ld(B,mult(mult(mult(mult(ld(B,B),B),B),ld(B,A)),B)),
inference(paramod,[status(thm)],[c_735,c_3300]) ).
cnf(c_3302,plain,
mult(A,B) = ld(B,mult(mult(mult(mult(unit,B),B),ld(B,A)),B)),
inference(paramod,[status(thm)],[c_14,c_3301]) ).
cnf(c_3303,plain,
mult(A,B) = ld(B,mult(mult(mult(B,B),ld(B,A)),B)),
inference(paramod,[status(thm)],[c_6,c_3302]) ).
cnf(c_981,plain,
ld(A,mult(mult(mult(A,A),ld(A,B)),A)) = mult(B,A),
inference(copy,[status(thm)],[c_3303]) ).
cnf(c_3304,plain,
mult(ld(mult(A,A),mult(A,B)),A) = ld(A,mult(B,A)),
inference(paramod,[status(thm)],[c_2,c_951]) ).
cnf(c_982,plain,
mult(mult(A,ld(mult(A,A),B)),A) = ld(A,mult(B,A)),
inference(paramod,[status(thm)],[c_157,c_3304]) ).
cnf(c_1019,plain,
rd(mult(A,B),mult(ld(C,mult(A,C)),ld(C,B))) = C,
inference(paramod,[status(thm)],[c_982,c_916]) ).
cnf(c_1023,plain,
mult(A,mult(ld(A,mult(B,A)),C)) = mult(B,mult(A,C)),
inference(paramod,[status(thm)],[c_982,c_458]) ).
cnf(c_3305,plain,
mult(B,mult(A,A)) = mult(mult(A,mult(ld(A,B),A)),A),
inference(paramod,[status(thm)],[c_1023,c_453]) ).
cnf(c_1035,plain,
mult(mult(A,mult(ld(A,B),A)),A) = mult(B,mult(A,A)),
inference(copy,[status(thm)],[c_3305]) ).
cnf(c_3306,plain,
ld(A,mult(B,C)) = mult(ld(A,mult(B,A)),ld(A,C)),
inference(paramod,[status(thm)],[c_1019,c_12]) ).
cnf(c_1047,plain,
mult(ld(A,mult(B,A)),ld(A,C)) = ld(A,mult(B,C)),
inference(copy,[status(thm)],[c_3306]) ).
cnf(c_1185,plain,
mult(ld(A,mult(B,A)),ld(A,unit)) = ld(A,B),
inference(paramod,[status(thm)],[c_5,c_1047]) ).
cnf(c_3307,plain,
mult(ld(A,B),ld(A,unit)) = ld(A,rd(B,A)),
inference(paramod,[status(thm)],[c_3,c_1185]) ).
cnf(c_1372,plain,
ld(A,rd(B,A)) = mult(ld(A,B),ld(A,unit)),
inference(copy,[status(thm)],[c_3307]) ).
cnf(c_3308,plain,
mult(ld(A,mult(A,mult(A,mult(B,A)))),ld(A,unit)) = ld(A,mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_38,c_1185]) ).
cnf(c_3309,plain,
mult(mult(A,mult(B,A)),ld(A,unit)) = ld(A,mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_2,c_3308]) ).
cnf(c_1411,plain,
mult(mult(A,mult(B,A)),ld(A,unit)) = mult(A,B),
inference(paramod,[status(thm)],[c_2,c_3309]) ).
cnf(c_3310,plain,
mult(ld(A,mult(mult(A,A),B)),ld(A,unit)) = rd(mult(A,B),A),
inference(paramod,[status(thm)],[c_1372,c_656]) ).
cnf(c_3311,plain,
mult(mult(mult(mult(ld(A,A),A),A),ld(A,B)),ld(A,unit)) = rd(mult(A,B),A),
inference(paramod,[status(thm)],[c_735,c_3310]) ).
cnf(c_3312,plain,
mult(mult(mult(mult(unit,A),A),ld(A,B)),ld(A,unit)) = rd(mult(A,B),A),
inference(paramod,[status(thm)],[c_14,c_3311]) ).
cnf(c_3313,plain,
mult(mult(mult(A,A),ld(A,B)),ld(A,unit)) = rd(mult(A,B),A),
inference(paramod,[status(thm)],[c_6,c_3312]) ).
cnf(c_1453,plain,
rd(mult(A,B),A) = mult(mult(mult(A,A),ld(A,B)),ld(A,unit)),
inference(copy,[status(thm)],[c_3313]) ).
cnf(c_3314,plain,
mult(mult(ld(A,B),ld(A,unit)),A) = mult(A,ld(mult(A,A),B)),
inference(paramod,[status(thm)],[c_1372,c_349]) ).
cnf(c_3315,plain,
mult(mult(ld(A,B),A),ld(A,unit)) = mult(A,ld(mult(A,A),B)),
inference(paramod,[status(thm)],[c_520,c_3314]) ).
cnf(c_1458,plain,
mult(A,ld(mult(A,A),B)) = mult(mult(ld(A,B),A),ld(A,unit)),
inference(copy,[status(thm)],[c_3315]) ).
cnf(c_1494,plain,
mult(mult(mult(mult(a,a),ld(a,b)),ld(a,unit)),mult(a,c)) != mult(a,mult(b,c)),
inference(paramod,[status(thm)],[c_1453,c_11]) ).
cnf(c_3316,plain,
mult(mult(mult(ld(A,B),A),ld(A,unit)),A) = ld(A,mult(B,A)),
inference(paramod,[status(thm)],[c_1458,c_982]) ).
cnf(c_3317,plain,
mult(mult(mult(ld(A,B),A),A),ld(A,unit)) = ld(A,mult(B,A)),
inference(paramod,[status(thm)],[c_520,c_3316]) ).
cnf(c_1519,plain,
ld(A,mult(B,A)) = mult(mult(mult(ld(A,B),A),A),ld(A,unit)),
inference(copy,[status(thm)],[c_3317]) ).
cnf(c_3318,plain,
mult(mult(mult(mult(ld(A,B),A),A),ld(A,unit)),ld(A,C)) = ld(A,mult(B,C)),
inference(paramod,[status(thm)],[c_1519,c_1047]) ).
cnf(c_1590,plain,
ld(A,mult(B,C)) = mult(mult(mult(mult(ld(A,B),A),A),ld(A,unit)),ld(A,C)),
inference(copy,[status(thm)],[c_3318]) ).
cnf(c_3319,plain,
mult(mult(mult(ld(A,mult(mult(A,A),ld(A,B))),A),A),ld(A,unit)) = mult(B,A),
inference(paramod,[status(thm)],[c_1519,c_981]) ).
cnf(c_3320,plain,
mult(mult(mult(mult(mult(mult(mult(ld(A,mult(A,A)),A),A),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)) = mult(B,A),
inference(paramod,[status(thm)],[c_1590,c_3319]) ).
cnf(c_3321,plain,
mult(mult(mult(mult(mult(mult(mult(A,A),A),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)) = mult(B,A),
inference(paramod,[status(thm)],[c_2,c_3320]) ).
cnf(c_3322,plain,
mult(mult(mult(mult(mult(mult(A,mult(A,A)),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)) = mult(B,A),
inference(paramod,[status(thm)],[c_43,c_3321]) ).
cnf(c_1597,plain,
mult(mult(mult(mult(mult(A,A),ld(A,ld(A,B))),A),A),ld(A,unit)) = mult(B,A),
inference(paramod,[status(thm)],[c_1411,c_3322]) ).
cnf(c_3323,plain,
mult(A,mult(ld(A,B),ld(A,unit))) = rd(B,A),
inference(paramod,[status(thm)],[c_1372,c_1]) ).
cnf(c_1612,plain,
rd(A,B) = mult(B,mult(ld(B,A),ld(B,unit))),
inference(copy,[status(thm)],[c_3323]) ).
cnf(c_3324,plain,
mult(A,mult(ld(A,mult(A,B)),ld(A,unit))) = mult(mult(mult(A,A),ld(A,B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1612,c_1453]) ).
cnf(c_3325,plain,
mult(A,mult(mult(mult(mult(mult(ld(A,A),A),A),ld(A,unit)),ld(A,B)),ld(A,unit))) = mult(mult(mult(A,A),ld(A,B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1590,c_3324]) ).
cnf(c_3326,plain,
mult(A,mult(mult(mult(mult(mult(unit,A),A),ld(A,unit)),ld(A,B)),ld(A,unit))) = mult(mult(mult(A,A),ld(A,B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_14,c_3325]) ).
cnf(c_3327,plain,
mult(A,mult(mult(mult(mult(A,A),ld(A,unit)),ld(A,B)),ld(A,unit))) = mult(mult(mult(A,A),ld(A,B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_6,c_3326]) ).
cnf(c_3328,plain,
mult(A,mult(mult(A,ld(A,B)),ld(A,unit))) = mult(mult(mult(A,A),ld(A,B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_79,c_3327]) ).
cnf(c_3329,plain,
mult(A,mult(B,ld(A,unit))) = mult(mult(mult(A,A),ld(A,B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1,c_3328]) ).
cnf(c_1619,plain,
mult(mult(mult(A,A),ld(A,B)),ld(A,unit)) = mult(A,mult(B,ld(A,unit))),
inference(copy,[status(thm)],[c_3329]) ).
cnf(c_1630,plain,
ld(mult(A,mult(ld(A,B),ld(A,unit))),B) = A,
inference(paramod,[status(thm)],[c_1612,c_12]) ).
cnf(c_1631,plain,
mult(mult(A,mult(ld(A,B),ld(A,unit))),A) = B,
inference(paramod,[status(thm)],[c_1612,c_3]) ).
cnf(c_1632,plain,
mult(mult(a,mult(b,ld(a,unit))),mult(a,c)) != mult(a,mult(b,c)),
inference(paramod,[status(thm)],[c_1619,c_1494]) ).
cnf(c_1639,plain,
mult(mult(ld(A,B),B),ld(ld(A,B),unit)) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_1,c_1411]) ).
cnf(c_3330,plain,
mult(mult(A,mult(mult(A,A),mult(A,A))),ld(mult(A,A),unit)) = mult(mult(A,A),A),
inference(paramod,[status(thm)],[c_29,c_1411]) ).
cnf(c_3331,plain,
mult(mult(A,mult(A,mult(mult(A,A),A))),ld(mult(A,A),unit)) = mult(mult(A,A),A),
inference(paramod,[status(thm)],[c_29,c_3330]) ).
cnf(c_3332,plain,
mult(mult(A,mult(A,mult(A,mult(A,A)))),ld(mult(A,A),unit)) = mult(mult(A,A),A),
inference(paramod,[status(thm)],[c_43,c_3331]) ).
cnf(c_3333,plain,
mult(mult(A,mult(A,mult(A,mult(A,A)))),mult(ld(A,unit),ld(A,unit))) = mult(mult(A,A),A),
inference(paramod,[status(thm)],[c_565,c_3332]) ).
cnf(c_1643,plain,
mult(mult(A,mult(A,mult(A,mult(A,A)))),mult(ld(A,unit),ld(A,unit))) = mult(A,mult(A,A)),
inference(paramod,[status(thm)],[c_43,c_3333]) ).
cnf(c_3334,plain,
mult(mult(A,mult(mult(mult(A,A),ld(A,B)),A)),ld(A,unit)) = mult(mult(A,A),B),
inference(paramod,[status(thm)],[c_39,c_1411]) ).
cnf(c_3335,plain,
mult(mult(mult(A,mult(A,A)),mult(ld(A,B),A)),ld(A,unit)) = mult(mult(A,A),B),
inference(paramod,[status(thm)],[c_601,c_3334]) ).
cnf(c_1648,plain,
mult(mult(A,mult(A,mult(B,A))),ld(A,unit)) = mult(mult(A,A),B),
inference(paramod,[status(thm)],[c_972,c_3335]) ).
cnf(c_1654,plain,
mult(mult(A,mult(mult(B,A),mult(A,A))),ld(A,unit)) = mult(A,mult(B,mult(A,A))),
inference(paramod,[status(thm)],[c_37,c_1411]) ).
cnf(c_3336,plain,
mult(A,mult(A,mult(B,mult(A,A)))) = mult(mult(A,A),mult(mult(B,A),A)),
inference(paramod,[status(thm)],[c_1654,c_927]) ).
cnf(c_1668,plain,
mult(mult(A,A),mult(mult(B,A),A)) = mult(A,mult(A,mult(B,mult(A,A)))),
inference(copy,[status(thm)],[c_3336]) ).
cnf(c_1698,plain,
mult(mult(A,mult(mult(B,A),ld(A,unit))),ld(A,unit)) = mult(A,mult(B,ld(A,unit))),
inference(paramod,[status(thm)],[c_520,c_1411]) ).
cnf(c_3337,plain,
mult(ld(A,unit),mult(mult(B,A),A)) = mult(A,mult(ld(A,unit),mult(mult(ld(A,B),A),A))),
inference(paramod,[status(thm)],[c_56,c_678]) ).
cnf(c_1712,plain,
mult(A,mult(ld(A,unit),mult(mult(ld(A,B),A),A))) = mult(ld(A,unit),mult(mult(B,A),A)),
inference(copy,[status(thm)],[c_3337]) ).
cnf(c_3338,plain,
mult(ld(A,unit),mult(mult(mult(mult(A,B),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit))) = mult(mult(A,mult(ld(A,unit),B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_678,c_64]) ).
cnf(c_3339,plain,
mult(ld(A,unit),mult(mult(mult(mult(A,B),ld(A,unit)),ld(A,unit)),A)) = mult(mult(A,mult(ld(A,unit),B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_389,c_3338]) ).
cnf(c_3340,plain,
mult(ld(A,unit),mult(mult(mult(mult(A,B),ld(A,unit)),A),ld(A,unit))) = mult(mult(A,mult(ld(A,unit),B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3339]) ).
cnf(c_3341,plain,
mult(ld(A,unit),mult(mult(mult(mult(A,B),A),ld(A,unit)),ld(A,unit))) = mult(mult(A,mult(ld(A,unit),B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3340]) ).
cnf(c_1713,plain,
mult(mult(A,mult(ld(A,unit),B)),ld(A,unit)) = mult(ld(A,unit),mult(mult(mult(mult(A,B),A),ld(A,unit)),ld(A,unit))),
inference(copy,[status(thm)],[c_3341]) ).
cnf(c_3342,plain,
mult(ld(A,unit),mult(mult(A,B),A)) = mult(A,mult(ld(A,unit),mult(mult(mult(B,A),A),ld(A,unit)))),
inference(paramod,[status(thm)],[c_64,c_678]) ).
cnf(c_1714,plain,
mult(A,mult(ld(A,unit),mult(mult(mult(B,A),A),ld(A,unit)))) = mult(ld(A,unit),mult(mult(A,B),A)),
inference(copy,[status(thm)],[c_3342]) ).
cnf(c_3343,plain,
mult(mult(A,B),ld(ld(mult(A,mult(ld(A,B),ld(A,unit))),B),unit)) = mult(ld(mult(A,mult(ld(A,B),ld(A,unit))),B),mult(A,mult(ld(A,B),ld(A,unit)))),
inference(paramod,[status(thm)],[c_1630,c_1639]) ).
cnf(c_3344,plain,
mult(mult(A,B),ld(A,unit)) = mult(ld(mult(A,mult(ld(A,B),ld(A,unit))),B),mult(A,mult(ld(A,B),ld(A,unit)))),
inference(paramod,[status(thm)],[c_1630,c_3343]) ).
cnf(c_3345,plain,
mult(mult(A,B),ld(A,unit)) = mult(A,mult(A,mult(ld(A,B),ld(A,unit)))),
inference(paramod,[status(thm)],[c_1630,c_3344]) ).
cnf(c_1735,plain,
mult(A,mult(A,mult(ld(A,B),ld(A,unit)))) = mult(mult(A,B),ld(A,unit)),
inference(copy,[status(thm)],[c_3345]) ).
cnf(c_3346,plain,
mult(A,mult(mult(B,A),ld(A,unit))) = mult(mult(A,mult(A,mult(ld(A,B),ld(A,unit)))),A),
inference(paramod,[status(thm)],[c_1631,c_64]) ).
cnf(c_3347,plain,
mult(A,mult(mult(B,A),ld(A,unit))) = mult(mult(mult(A,B),ld(A,unit)),A),
inference(paramod,[status(thm)],[c_1735,c_3346]) ).
cnf(c_3348,plain,
mult(A,mult(mult(B,A),ld(A,unit))) = mult(mult(mult(A,B),A),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3347]) ).
cnf(c_1745,plain,
mult(mult(mult(A,B),A),ld(A,unit)) = mult(A,mult(mult(B,A),ld(A,unit))),
inference(copy,[status(thm)],[c_3348]) ).
cnf(c_3349,plain,
mult(mult(A,mult(ld(A,unit),B)),ld(A,unit)) = mult(ld(A,unit),mult(mult(A,mult(mult(B,A),ld(A,unit))),ld(A,unit))),
inference(paramod,[status(thm)],[c_1745,c_1713]) ).
cnf(c_3350,plain,
mult(mult(A,mult(ld(A,unit),B)),ld(A,unit)) = mult(ld(A,unit),mult(A,mult(B,ld(A,unit)))),
inference(paramod,[status(thm)],[c_1698,c_3349]) ).
cnf(c_1749,plain,
mult(mult(A,mult(ld(A,unit),B)),ld(A,unit)) = mult(A,mult(ld(A,unit),mult(B,ld(A,unit)))),
inference(paramod,[status(thm)],[c_678,c_3350]) ).
cnf(c_3351,plain,
mult(A,ld(ld(A,unit),ld(ld(ld(A,unit),unit),B))) = ld(ld(A,unit),B),
inference(paramod,[status(thm)],[c_389,c_782]) ).
cnf(c_1776,plain,
mult(A,ld(ld(A,unit),ld(A,B))) = ld(ld(A,unit),B),
inference(paramod,[status(thm)],[c_389,c_3351]) ).
cnf(c_3352,plain,
mult(ld(A,unit),mult(mult(mult(ld(A,ld(ld(A,unit),B)),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit))) = mult(ld(A,B),ld(A,unit)),
inference(paramod,[status(thm)],[c_782,c_64]) ).
cnf(c_3353,plain,
mult(ld(A,unit),mult(mult(mult(ld(A,ld(ld(A,unit),B)),ld(A,unit)),ld(A,unit)),A)) = mult(ld(A,B),ld(A,unit)),
inference(paramod,[status(thm)],[c_389,c_3352]) ).
cnf(c_3354,plain,
mult(ld(A,unit),mult(mult(mult(ld(A,ld(ld(A,unit),B)),ld(A,unit)),A),ld(A,unit))) = mult(ld(A,B),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3353]) ).
cnf(c_1778,plain,
mult(ld(A,unit),mult(mult(mult(ld(A,ld(ld(A,unit),B)),A),ld(A,unit)),ld(A,unit))) = mult(ld(A,B),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3354]) ).
cnf(c_3355,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(ld(mult(ld(B,unit),ld(B,unit)),mult(B,mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_850,c_32]) ).
cnf(c_3356,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(mult(mult(mult(ld(mult(ld(B,unit),ld(B,unit)),B),mult(ld(B,unit),ld(B,unit))),mult(ld(B,unit),ld(B,unit))),ld(mult(ld(B,unit),ld(B,unit)),unit)),ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_1590,c_3355]) ).
cnf(c_3357,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(mult(mult(mult(mult(B,mult(B,B)),mult(ld(B,unit),ld(B,unit))),mult(ld(B,unit),ld(B,unit))),ld(mult(ld(B,unit),ld(B,unit)),unit)),ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_716,c_3356]) ).
cnf(c_3358,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(mult(mult(B,mult(ld(B,unit),ld(B,unit))),ld(mult(ld(B,unit),ld(B,unit)),unit)),ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_895,c_3357]) ).
cnf(c_3359,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(mult(mult(ld(B,unit),unit),ld(mult(ld(B,unit),ld(B,unit)),unit)),ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_607,c_3358]) ).
cnf(c_3360,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(mult(ld(B,unit),ld(mult(ld(B,unit),ld(B,unit)),unit)),ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_5,c_3359]) ).
cnf(c_3361,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(mult(ld(B,unit),mult(ld(ld(B,unit),unit),ld(ld(B,unit),unit))),ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_565,c_3360]) ).
cnf(c_3362,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(mult(ld(B,unit),mult(B,ld(ld(B,unit),unit))),ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_389,c_3361]) ).
cnf(c_3363,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(mult(ld(B,unit),mult(B,B)),ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_389,c_3362]) ).
cnf(c_3364,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(mult(B,mult(ld(B,unit),B)),ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_678,c_3363]) ).
cnf(c_3365,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(mult(B,unit),ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_350,c_3364]) ).
cnf(c_3366,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,ld(mult(ld(B,unit),ld(B,unit)),mult(B,B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_5,c_3365]) ).
cnf(c_3367,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(mult(mult(mult(ld(mult(ld(B,unit),ld(B,unit)),B),mult(ld(B,unit),ld(B,unit))),mult(ld(B,unit),ld(B,unit))),ld(mult(ld(B,unit),ld(B,unit)),unit)),ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_1590,c_3366]) ).
cnf(c_3368,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(mult(mult(mult(mult(B,mult(B,B)),mult(ld(B,unit),ld(B,unit))),mult(ld(B,unit),ld(B,unit))),ld(mult(ld(B,unit),ld(B,unit)),unit)),ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_716,c_3367]) ).
cnf(c_3369,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(mult(mult(B,mult(ld(B,unit),ld(B,unit))),ld(mult(ld(B,unit),ld(B,unit)),unit)),ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_895,c_3368]) ).
cnf(c_3370,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(mult(mult(ld(B,unit),unit),ld(mult(ld(B,unit),ld(B,unit)),unit)),ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_607,c_3369]) ).
cnf(c_3371,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(mult(ld(B,unit),ld(mult(ld(B,unit),ld(B,unit)),unit)),ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_5,c_3370]) ).
cnf(c_3372,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(mult(ld(B,unit),mult(ld(ld(B,unit),unit),ld(ld(B,unit),unit))),ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_565,c_3371]) ).
cnf(c_3373,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(mult(ld(B,unit),mult(B,ld(ld(B,unit),unit))),ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_389,c_3372]) ).
cnf(c_3374,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(mult(ld(B,unit),mult(B,B)),ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_389,c_3373]) ).
cnf(c_3375,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(mult(B,mult(ld(B,unit),B)),ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_678,c_3374]) ).
cnf(c_3376,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(mult(B,unit),ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_350,c_3375]) ).
cnf(c_3377,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(B,ld(mult(ld(B,unit),ld(B,unit)),B))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_5,c_3376]) ).
cnf(c_3378,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(mult(B,mult(B,mult(B,mult(B,B)))),mult(ld(B,unit),ld(B,unit))))),
inference(paramod,[status(thm)],[c_716,c_3377]) ).
cnf(c_3379,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),mult(mult(ld(B,unit),ld(B,unit)),mult(B,mult(B,B)))),
inference(paramod,[status(thm)],[c_1643,c_3378]) ).
cnf(c_3380,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(mult(A,mult(ld(B,unit),ld(B,unit))),B),
inference(paramod,[status(thm)],[c_850,c_3379]) ).
cnf(c_1779,plain,
mult(mult(A,mult(ld(B,unit),ld(B,unit))),B) = mult(mult(A,B),mult(ld(B,unit),ld(B,unit))),
inference(copy,[status(thm)],[c_3380]) ).
cnf(c_3381,plain,
mult(mult(A,ld(ld(A,unit),B)),A) = mult(A,mult(A,mult(ld(ld(A,unit),ld(A,B)),A))),
inference(paramod,[status(thm)],[c_1776,c_38]) ).
cnf(c_1800,plain,
mult(A,mult(A,mult(ld(ld(A,unit),ld(A,B)),A))) = mult(mult(A,ld(ld(A,unit),B)),A),
inference(copy,[status(thm)],[c_3381]) ).
cnf(c_3382,plain,
mult(mult(mult(A,mult(mult(B,A),A)),A),ld(A,unit)) = mult(A,mult(ld(A,mult(mult(A,B),A)),A)),
inference(paramod,[status(thm)],[c_30,c_919]) ).
cnf(c_3383,plain,
mult(mult(A,mult(mult(B,A),mult(A,A))),ld(A,unit)) = mult(A,mult(ld(A,mult(mult(A,B),A)),A)),
inference(paramod,[status(thm)],[c_383,c_3382]) ).
cnf(c_3384,plain,
mult(A,mult(B,mult(A,A))) = mult(A,mult(ld(A,mult(mult(A,B),A)),A)),
inference(paramod,[status(thm)],[c_1654,c_3383]) ).
cnf(c_3385,plain,
mult(A,mult(B,mult(A,A))) = mult(A,mult(mult(mult(mult(mult(ld(A,mult(A,B)),A),A),ld(A,unit)),ld(A,A)),A)),
inference(paramod,[status(thm)],[c_1590,c_3384]) ).
cnf(c_3386,plain,
mult(A,mult(B,mult(A,A))) = mult(A,mult(mult(mult(mult(mult(mult(mult(mult(mult(ld(A,A),A),A),ld(A,unit)),ld(A,B)),A),A),ld(A,unit)),ld(A,A)),A)),
inference(paramod,[status(thm)],[c_1590,c_3385]) ).
cnf(c_3387,plain,
mult(A,mult(B,mult(A,A))) = mult(A,mult(mult(mult(mult(mult(mult(mult(mult(mult(unit,A),A),ld(A,unit)),ld(A,B)),A),A),ld(A,unit)),ld(A,A)),A)),
inference(paramod,[status(thm)],[c_14,c_3386]) ).
cnf(c_3388,plain,
mult(A,mult(B,mult(A,A))) = mult(A,mult(mult(mult(mult(mult(mult(mult(mult(A,A),ld(A,unit)),ld(A,B)),A),A),ld(A,unit)),ld(A,A)),A)),
inference(paramod,[status(thm)],[c_6,c_3387]) ).
cnf(c_3389,plain,
mult(A,mult(B,mult(A,A))) = mult(A,mult(mult(mult(mult(mult(mult(A,ld(A,B)),A),A),ld(A,unit)),ld(A,A)),A)),
inference(paramod,[status(thm)],[c_79,c_3388]) ).
cnf(c_3390,plain,
mult(A,mult(B,mult(A,A))) = mult(A,mult(mult(mult(mult(mult(B,A),A),ld(A,unit)),ld(A,A)),A)),
inference(paramod,[status(thm)],[c_1,c_3389]) ).
cnf(c_3391,plain,
mult(A,mult(B,mult(A,A))) = mult(A,mult(mult(mult(mult(mult(B,A),A),ld(A,unit)),unit),A)),
inference(paramod,[status(thm)],[c_14,c_3390]) ).
cnf(c_3392,plain,
mult(A,mult(B,mult(A,A))) = mult(A,mult(mult(mult(mult(B,A),A),ld(A,unit)),A)),
inference(paramod,[status(thm)],[c_5,c_3391]) ).
cnf(c_3393,plain,
mult(A,mult(B,mult(A,A))) = mult(A,mult(mult(mult(mult(B,A),A),A),ld(A,unit))),
inference(paramod,[status(thm)],[c_520,c_3392]) ).
cnf(c_3394,plain,
mult(A,mult(B,mult(A,A))) = mult(mult(A,mult(B,A)),A),
inference(paramod,[status(thm)],[c_64,c_3393]) ).
cnf(c_1812,plain,
mult(mult(A,mult(B,A)),A) = mult(A,mult(B,mult(A,A))),
inference(copy,[status(thm)],[c_3394]) ).
cnf(c_3395,plain,
mult(mult(mult(A,ld(B,unit)),ld(B,unit)),B) = mult(ld(B,unit),mult(ld(ld(B,unit),A),ld(B,unit))),
inference(paramod,[status(thm)],[c_389,c_919]) ).
cnf(c_3396,plain,
mult(mult(mult(A,ld(B,unit)),B),ld(B,unit)) = mult(ld(B,unit),mult(ld(ld(B,unit),A),ld(B,unit))),
inference(paramod,[status(thm)],[c_520,c_3395]) ).
cnf(c_3397,plain,
mult(mult(mult(A,B),ld(B,unit)),ld(B,unit)) = mult(ld(B,unit),mult(ld(ld(B,unit),A),ld(B,unit))),
inference(paramod,[status(thm)],[c_520,c_3396]) ).
cnf(c_1817,plain,
mult(ld(A,unit),mult(ld(ld(A,unit),B),ld(A,unit))) = mult(mult(mult(B,A),ld(A,unit)),ld(A,unit)),
inference(copy,[status(thm)],[c_3397]) ).
cnf(c_3398,plain,
mult(A,mult(mult(mult(mult(ld(A,B),A),A),A),ld(A,unit))) = mult(mult(mult(mult(B,A),A),ld(A,unit)),A),
inference(paramod,[status(thm)],[c_919,c_64]) ).
cnf(c_3399,plain,
mult(mult(A,mult(ld(A,B),A)),A) = mult(mult(mult(mult(B,A),A),ld(A,unit)),A),
inference(paramod,[status(thm)],[c_64,c_3398]) ).
cnf(c_3400,plain,
mult(A,mult(ld(A,B),mult(A,A))) = mult(mult(mult(mult(B,A),A),ld(A,unit)),A),
inference(paramod,[status(thm)],[c_1812,c_3399]) ).
cnf(c_3401,plain,
mult(A,mult(ld(A,B),mult(A,A))) = mult(mult(mult(mult(B,A),A),A),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3400]) ).
cnf(c_1822,plain,
mult(mult(mult(mult(A,B),B),B),ld(B,unit)) = mult(B,mult(ld(B,A),mult(B,B))),
inference(copy,[status(thm)],[c_3401]) ).
cnf(c_3402,plain,
mult(mult(mult(mult(A,B),B),ld(B,unit)),ld(B,unit)) = mult(B,ld(B,A)),
inference(paramod,[status(thm)],[c_919,c_1411]) ).
cnf(c_1824,plain,
mult(mult(mult(mult(A,B),B),ld(B,unit)),ld(B,unit)) = A,
inference(paramod,[status(thm)],[c_1,c_3402]) ).
cnf(c_1834,plain,
mult(A,mult(ld(A,B),mult(A,A))) = mult(B,mult(A,A)),
inference(paramod,[status(thm)],[c_1812,c_1035]) ).
cnf(c_1841,plain,
mult(mult(mult(mult(A,B),B),B),ld(B,unit)) = mult(A,mult(B,B)),
inference(paramod,[status(thm)],[c_1834,c_1822]) ).
cnf(c_3403,plain,
mult(mult(A,A),mult(ld(A,mult(mult(mult(A,A),ld(A,B)),A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_185,c_207]) ).
cnf(c_3404,plain,
mult(mult(A,A),mult(mult(mult(mult(mult(ld(A,mult(mult(A,A),ld(A,B))),A),A),ld(A,unit)),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_1590,c_3403]) ).
cnf(c_3405,plain,
mult(mult(A,A),mult(mult(mult(mult(mult(mult(mult(mult(mult(ld(A,mult(A,A)),A),A),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_1590,c_3404]) ).
cnf(c_3406,plain,
mult(mult(A,A),mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(ld(A,A),A),A),ld(A,unit)),ld(A,A)),A),A),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_1590,c_3405]) ).
cnf(c_3407,plain,
mult(mult(A,A),mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(unit,A),A),ld(A,unit)),ld(A,A)),A),A),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_14,c_3406]) ).
cnf(c_3408,plain,
mult(mult(A,A),mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(A,A),ld(A,unit)),ld(A,A)),A),A),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_6,c_3407]) ).
cnf(c_3409,plain,
mult(mult(A,A),mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(A,ld(A,A)),A),A),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_79,c_3408]) ).
cnf(c_3410,plain,
mult(mult(A,A),mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(A,unit),A),A),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_14,c_3409]) ).
cnf(c_3411,plain,
mult(mult(A,A),mult(mult(mult(mult(mult(mult(mult(mult(mult(A,A),A),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_5,c_3410]) ).
cnf(c_3412,plain,
mult(mult(A,A),mult(mult(mult(mult(mult(mult(mult(mult(A,mult(A,A)),ld(A,unit)),ld(A,ld(A,B))),A),A),ld(A,unit)),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_43,c_3411]) ).
cnf(c_3413,plain,
mult(mult(A,A),mult(mult(mult(mult(mult(mult(mult(A,A),ld(A,ld(A,B))),A),A),ld(A,unit)),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_1411,c_3412]) ).
cnf(c_3414,plain,
mult(mult(A,A),mult(mult(mult(B,A),ld(A,A)),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_1597,c_3413]) ).
cnf(c_3415,plain,
mult(mult(A,A),mult(mult(mult(B,A),unit),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_14,c_3414]) ).
cnf(c_3416,plain,
mult(mult(A,A),mult(mult(B,A),A)) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_5,c_3415]) ).
cnf(c_3417,plain,
mult(A,mult(A,mult(B,mult(A,A)))) = mult(mult(mult(mult(A,A),B),A),A),
inference(paramod,[status(thm)],[c_1668,c_3416]) ).
cnf(c_1865,plain,
mult(mult(mult(mult(A,A),B),A),A) = mult(A,mult(A,mult(B,mult(A,A)))),
inference(copy,[status(thm)],[c_3417]) ).
cnf(c_3418,plain,
mult(mult(A,mult(A,mult(ld(A,ld(A,B)),mult(A,A)))),ld(A,unit)) = mult(B,A),
inference(paramod,[status(thm)],[c_1865,c_1597]) ).
cnf(c_3419,plain,
mult(mult(A,mult(ld(A,B),mult(A,A))),ld(A,unit)) = mult(B,A),
inference(paramod,[status(thm)],[c_1834,c_3418]) ).
cnf(c_1870,plain,
mult(mult(A,mult(B,B)),ld(B,unit)) = mult(A,B),
inference(paramod,[status(thm)],[c_1834,c_3419]) ).
cnf(c_3420,plain,
mult(mult(A,mult(ld(A,unit),B)),ld(A,unit)) = mult(ld(A,unit),mult(ld(ld(A,unit),B),ld(A,unit))),
inference(paramod,[status(thm)],[c_189,c_6]) ).
cnf(c_3421,plain,
mult(A,mult(ld(A,unit),mult(B,ld(A,unit)))) = mult(ld(A,unit),mult(ld(ld(A,unit),B),ld(A,unit))),
inference(paramod,[status(thm)],[c_1749,c_3420]) ).
cnf(c_3422,plain,
mult(A,mult(ld(A,unit),mult(B,ld(A,unit)))) = mult(mult(mult(B,A),ld(A,unit)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1817,c_3421]) ).
cnf(c_1872,plain,
mult(mult(mult(A,B),ld(B,unit)),ld(B,unit)) = mult(B,mult(ld(B,unit),mult(A,ld(B,unit)))),
inference(copy,[status(thm)],[c_3422]) ).
cnf(c_3423,plain,
mult(unit,mult(ld(A,unit),mult(ld(ld(A,unit),ld(A,ld(ld(A,unit),B))),ld(A,unit)))) = mult(mult(A,ld(A,B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_782,c_189]) ).
cnf(c_3424,plain,
mult(unit,mult(mult(mult(ld(A,ld(ld(A,unit),B)),A),ld(A,unit)),ld(A,unit))) = mult(mult(A,ld(A,B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1817,c_3423]) ).
cnf(c_3425,plain,
mult(unit,mult(A,mult(ld(A,unit),mult(ld(A,ld(ld(A,unit),B)),ld(A,unit))))) = mult(mult(A,ld(A,B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1872,c_3424]) ).
cnf(c_3426,plain,
mult(A,mult(ld(A,unit),mult(ld(A,ld(ld(A,unit),B)),ld(A,unit)))) = mult(mult(A,ld(A,B)),ld(A,unit)),
inference(paramod,[status(thm)],[c_6,c_3425]) ).
cnf(c_1883,plain,
mult(A,mult(ld(A,unit),mult(ld(A,ld(ld(A,unit),B)),ld(A,unit)))) = mult(B,ld(A,unit)),
inference(paramod,[status(thm)],[c_1,c_3426]) ).
cnf(c_1885,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),ld(A,unit)))) = B,
inference(paramod,[status(thm)],[c_1872,c_1824]) ).
cnf(c_3427,plain,
mult(ld(A,unit),mult(A,mult(ld(A,unit),mult(ld(A,ld(ld(A,unit),B)),ld(A,unit))))) = mult(ld(A,B),ld(A,unit)),
inference(paramod,[status(thm)],[c_1872,c_1778]) ).
cnf(c_1887,plain,
mult(ld(A,unit),mult(B,ld(A,unit))) = mult(ld(A,B),ld(A,unit)),
inference(paramod,[status(thm)],[c_1883,c_3427]) ).
cnf(c_3428,plain,
mult(B,A) = mult(ld(A,unit),mult(mult(A,B),A)),
inference(paramod,[status(thm)],[c_1885,c_1714]) ).
cnf(c_1893,plain,
mult(ld(A,unit),mult(mult(A,B),A)) = mult(B,A),
inference(copy,[status(thm)],[c_3428]) ).
cnf(c_3429,plain,
mult(A,mult(B,ld(ld(A,unit),unit))) = mult(ld(ld(A,unit),B),ld(ld(A,unit),unit)),
inference(paramod,[status(thm)],[c_389,c_1887]) ).
cnf(c_3430,plain,
mult(A,mult(B,A)) = mult(ld(ld(A,unit),B),ld(ld(A,unit),unit)),
inference(paramod,[status(thm)],[c_389,c_3429]) ).
cnf(c_3431,plain,
mult(A,mult(B,A)) = mult(ld(ld(A,unit),B),A),
inference(paramod,[status(thm)],[c_389,c_3430]) ).
cnf(c_1918,plain,
mult(ld(ld(A,unit),B),A) = mult(A,mult(B,A)),
inference(copy,[status(thm)],[c_3431]) ).
cnf(c_3432,plain,
mult(ld(A,unit),mult(mult(ld(ld(A,unit),ld(A,B)),ld(A,unit)),ld(A,unit))) = mult(mult(ld(A,unit),mult(B,ld(A,unit))),ld(A,unit)),
inference(paramod,[status(thm)],[c_1887,c_56]) ).
cnf(c_3433,plain,
mult(mult(ld(A,B),ld(A,unit)),ld(A,unit)) = mult(mult(ld(A,unit),mult(B,ld(A,unit))),ld(A,unit)),
inference(paramod,[status(thm)],[c_56,c_3432]) ).
cnf(c_1921,plain,
mult(mult(ld(A,B),ld(A,unit)),ld(A,unit)) = mult(ld(A,unit),mult(B,mult(ld(A,unit),ld(A,unit)))),
inference(paramod,[status(thm)],[c_1812,c_3433]) ).
cnf(c_3434,plain,
mult(A,mult(A,mult(A,mult(ld(A,B),A)))) = mult(mult(A,ld(ld(A,unit),B)),A),
inference(paramod,[status(thm)],[c_1918,c_1800]) ).
cnf(c_3435,plain,
mult(A,mult(mult(A,B),A)) = mult(mult(A,ld(ld(A,unit),B)),A),
inference(paramod,[status(thm)],[c_197,c_3434]) ).
cnf(c_1942,plain,
mult(mult(A,ld(ld(A,unit),B)),A) = mult(A,mult(mult(A,B),A)),
inference(copy,[status(thm)],[c_3435]) ).
cnf(c_3436,plain,
mult(mult(A,mult(ld(B,unit),ld(B,unit))),B) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_389,c_1870]) ).
cnf(c_2021,plain,
mult(mult(A,B),mult(ld(B,unit),ld(B,unit))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_1779,c_3436]) ).
cnf(c_3437,plain,
mult(ld(A,unit),mult(B,A)) = mult(ld(A,mult(B,mult(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_1870,c_1887]) ).
cnf(c_3438,plain,
mult(ld(A,unit),mult(B,A)) = mult(mult(mult(mult(mult(ld(A,B),A),A),ld(A,unit)),ld(A,mult(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_1590,c_3437]) ).
cnf(c_3439,plain,
mult(ld(A,unit),mult(B,A)) = mult(mult(mult(mult(mult(ld(A,B),A),A),ld(A,unit)),mult(mult(mult(mult(ld(A,A),A),A),ld(A,unit)),ld(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_1590,c_3438]) ).
cnf(c_3440,plain,
mult(ld(A,unit),mult(B,A)) = mult(mult(mult(mult(mult(ld(A,B),A),A),ld(A,unit)),mult(mult(mult(mult(unit,A),A),ld(A,unit)),ld(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_14,c_3439]) ).
cnf(c_3441,plain,
mult(ld(A,unit),mult(B,A)) = mult(mult(mult(mult(mult(ld(A,B),A),A),ld(A,unit)),mult(mult(mult(A,A),ld(A,unit)),ld(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_6,c_3440]) ).
cnf(c_3442,plain,
mult(ld(A,unit),mult(B,A)) = mult(mult(mult(mult(mult(ld(A,B),A),A),ld(A,unit)),mult(A,ld(A,A))),ld(A,unit)),
inference(paramod,[status(thm)],[c_79,c_3441]) ).
cnf(c_3443,plain,
mult(ld(A,unit),mult(B,A)) = mult(mult(mult(mult(mult(ld(A,B),A),A),ld(A,unit)),mult(A,unit)),ld(A,unit)),
inference(paramod,[status(thm)],[c_14,c_3442]) ).
cnf(c_3444,plain,
mult(ld(A,unit),mult(B,A)) = mult(mult(mult(mult(mult(ld(A,B),A),A),ld(A,unit)),A),ld(A,unit)),
inference(paramod,[status(thm)],[c_5,c_3443]) ).
cnf(c_3445,plain,
mult(ld(A,unit),mult(B,A)) = mult(mult(mult(mult(mult(ld(A,B),A),A),A),ld(A,unit)),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3444]) ).
cnf(c_3446,plain,
mult(ld(A,unit),mult(B,A)) = mult(mult(ld(A,B),mult(A,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1841,c_3445]) ).
cnf(c_2029,plain,
mult(ld(A,unit),mult(B,A)) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_1870,c_3446]) ).
cnf(c_3447,plain,
mult(ld(A,unit),mult(A,mult(mult(B,A),A))) = mult(ld(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_30,c_2029]) ).
cnf(c_3448,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(ld(A,mult(mult(A,B),A)),A),
inference(paramod,[status(thm)],[c_678,c_3447]) ).
cnf(c_3449,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(mult(mult(mult(mult(ld(A,mult(A,B)),A),A),ld(A,unit)),ld(A,A)),A),
inference(paramod,[status(thm)],[c_1590,c_3448]) ).
cnf(c_3450,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(mult(mult(mult(mult(mult(mult(mult(mult(ld(A,A),A),A),ld(A,unit)),ld(A,B)),A),A),ld(A,unit)),ld(A,A)),A),
inference(paramod,[status(thm)],[c_1590,c_3449]) ).
cnf(c_3451,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(mult(mult(mult(mult(mult(mult(mult(mult(unit,A),A),ld(A,unit)),ld(A,B)),A),A),ld(A,unit)),ld(A,A)),A),
inference(paramod,[status(thm)],[c_14,c_3450]) ).
cnf(c_3452,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(mult(mult(mult(mult(mult(mult(mult(A,A),ld(A,unit)),ld(A,B)),A),A),ld(A,unit)),ld(A,A)),A),
inference(paramod,[status(thm)],[c_6,c_3451]) ).
cnf(c_3453,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(mult(mult(mult(mult(mult(A,ld(A,B)),A),A),ld(A,unit)),ld(A,A)),A),
inference(paramod,[status(thm)],[c_79,c_3452]) ).
cnf(c_3454,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(mult(mult(mult(mult(B,A),A),ld(A,unit)),ld(A,A)),A),
inference(paramod,[status(thm)],[c_1,c_3453]) ).
cnf(c_3455,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(mult(mult(mult(mult(B,A),A),ld(A,unit)),unit),A),
inference(paramod,[status(thm)],[c_14,c_3454]) ).
cnf(c_3456,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(mult(mult(mult(B,A),A),ld(A,unit)),A),
inference(paramod,[status(thm)],[c_5,c_3455]) ).
cnf(c_3457,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(mult(mult(mult(B,A),A),A),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3456]) ).
cnf(c_2060,plain,
mult(A,mult(ld(A,unit),mult(mult(B,A),A))) = mult(B,mult(A,A)),
inference(paramod,[status(thm)],[c_1841,c_3457]) ).
cnf(c_3458,plain,
mult(ld(A,B),mult(A,A)) = mult(ld(A,unit),mult(mult(B,A),A)),
inference(paramod,[status(thm)],[c_2060,c_1712]) ).
cnf(c_2106,plain,
mult(ld(A,unit),mult(mult(B,A),A)) = mult(ld(A,B),mult(A,A)),
inference(copy,[status(thm)],[c_3458]) ).
cnf(c_3459,plain,
mult(unit,mult(ld(A,unit),mult(ld(ld(A,unit),mult(mult(A,B),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1893,c_189]) ).
cnf(c_3460,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(ld(ld(A,unit),mult(A,B)),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1590,c_3459]) ).
cnf(c_3461,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(mult(mult(mult(mult(ld(ld(A,unit),A),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit)),ld(ld(A,unit),B)),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1590,c_3460]) ).
cnf(c_3462,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(mult(mult(mult(mult(mult(A,A),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit)),ld(ld(A,unit),B)),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_509,c_3461]) ).
cnf(c_3463,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(mult(mult(mult(A,ld(A,unit)),ld(ld(A,unit),unit)),ld(ld(A,unit),B)),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_79,c_3462]) ).
cnf(c_3464,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(mult(mult(unit,ld(ld(A,unit),unit)),ld(ld(A,unit),B)),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1,c_3463]) ).
cnf(c_3465,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(mult(mult(unit,A),ld(ld(A,unit),B)),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_389,c_3464]) ).
cnf(c_3466,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(mult(A,ld(ld(A,unit),B)),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_6,c_3465]) ).
cnf(c_3467,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(mult(A,ld(ld(A,unit),B)),ld(A,unit)),ld(A,unit)),A),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_389,c_3466]) ).
cnf(c_3468,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(mult(A,ld(ld(A,unit),B)),ld(A,unit)),A),ld(A,unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3467]) ).
cnf(c_3469,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(mult(A,ld(ld(A,unit),B)),A),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3468]) ).
cnf(c_3470,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(mult(A,mult(mult(A,B),A)),ld(A,unit)),ld(A,unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1942,c_3469]) ).
cnf(c_3471,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(A,mult(A,B)),ld(A,unit)),ld(ld(A,unit),A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1411,c_3470]) ).
cnf(c_3472,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(mult(A,mult(A,B)),ld(A,unit)),mult(A,A)),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_509,c_3471]) ).
cnf(c_3473,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(A,mult(A,B)),ld(A,unit)),A))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1870,c_3472]) ).
cnf(c_3474,plain,
mult(unit,mult(ld(A,unit),mult(mult(mult(A,mult(A,B)),A),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_520,c_3473]) ).
cnf(c_3475,plain,
mult(unit,mult(ld(A,unit),mult(mult(A,mult(A,mult(B,A))),ld(A,unit)))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_38,c_3474]) ).
cnf(c_3476,plain,
mult(unit,mult(ld(A,unit),mult(mult(A,A),B))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1648,c_3475]) ).
cnf(c_3477,plain,
mult(unit,mult(mult(A,A),mult(ld(A,unit),B))) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_873,c_3476]) ).
cnf(c_3478,plain,
mult(mult(A,A),mult(ld(A,unit),B)) = mult(mult(A,mult(B,A)),ld(A,unit)),
inference(paramod,[status(thm)],[c_6,c_3477]) ).
cnf(c_2151,plain,
mult(mult(A,A),mult(ld(A,unit),B)) = mult(A,B),
inference(paramod,[status(thm)],[c_1411,c_3478]) ).
cnf(c_3479,plain,
mult(ld(ld(A,unit),unit),mult(mult(ld(A,B),ld(A,unit)),ld(A,unit))) = mult(mult(B,ld(A,unit)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1887,c_1893]) ).
cnf(c_3480,plain,
mult(A,mult(mult(ld(A,B),ld(A,unit)),ld(A,unit))) = mult(mult(B,ld(A,unit)),ld(A,unit)),
inference(paramod,[status(thm)],[c_389,c_3479]) ).
cnf(c_3481,plain,
mult(A,mult(ld(A,unit),mult(B,mult(ld(A,unit),ld(A,unit))))) = mult(mult(B,ld(A,unit)),ld(A,unit)),
inference(paramod,[status(thm)],[c_1921,c_3480]) ).
cnf(c_2152,plain,
mult(mult(A,ld(B,unit)),ld(B,unit)) = mult(B,mult(ld(B,unit),mult(A,mult(ld(B,unit),ld(B,unit))))),
inference(copy,[status(thm)],[c_3481]) ).
cnf(c_2163,plain,
mult(ld(A,unit),mult(mult(A,A),B)) = mult(A,B),
inference(paramod,[status(thm)],[c_2151,c_873]) ).
cnf(c_3482,plain,
mult(mult(A,mult(A,mult(B,A))),ld(A,unit)) = mult(A,ld(ld(A,unit),B)),
inference(paramod,[status(thm)],[c_1918,c_1411]) ).
cnf(c_3483,plain,
mult(mult(A,A),B) = mult(A,ld(ld(A,unit),B)),
inference(paramod,[status(thm)],[c_1648,c_3482]) ).
cnf(c_2177,plain,
mult(A,ld(ld(A,unit),B)) = mult(mult(A,A),B),
inference(copy,[status(thm)],[c_3483]) ).
cnf(c_3484,plain,
mult(mult(A,A),ld(A,B)) = ld(ld(A,unit),B),
inference(paramod,[status(thm)],[c_2177,c_1776]) ).
cnf(c_2191,plain,
ld(ld(A,unit),B) = mult(mult(A,A),ld(A,B)),
inference(copy,[status(thm)],[c_3484]) ).
cnf(c_3485,plain,
mult(ld(ld(A,unit),unit),mult(mult(A,B),ld(A,unit))) = mult(mult(mult(A,A),B),ld(A,unit)),
inference(paramod,[status(thm)],[c_2163,c_1893]) ).
cnf(c_3486,plain,
mult(mult(mult(A,A),ld(A,unit)),mult(mult(A,B),ld(A,unit))) = mult(mult(mult(A,A),B),ld(A,unit)),
inference(paramod,[status(thm)],[c_2191,c_3485]) ).
cnf(c_3487,plain,
mult(A,mult(mult(A,B),ld(A,unit))) = mult(mult(mult(A,A),B),ld(A,unit)),
inference(paramod,[status(thm)],[c_79,c_3486]) ).
cnf(c_2282,plain,
mult(mult(mult(A,A),B),ld(A,unit)) = mult(A,mult(mult(A,B),ld(A,unit))),
inference(copy,[status(thm)],[c_3487]) ).
cnf(c_3488,plain,
mult(mult(mult(ld(A,B),mult(A,A)),ld(A,unit)),mult(ld(A,unit),C)) = mult(ld(A,unit),mult(mult(mult(mult(mult(B,A),A),ld(A,unit)),ld(A,unit)),C)),
inference(paramod,[status(thm)],[c_2106,c_7]) ).
cnf(c_3489,plain,
mult(mult(ld(A,B),A),mult(ld(A,unit),C)) = mult(ld(A,unit),mult(mult(mult(mult(mult(B,A),A),ld(A,unit)),ld(A,unit)),C)),
inference(paramod,[status(thm)],[c_1870,c_3488]) ).
cnf(c_3490,plain,
mult(mult(ld(A,B),A),mult(ld(A,unit),C)) = mult(ld(A,unit),mult(mult(A,mult(ld(A,unit),mult(mult(mult(B,A),A),mult(ld(A,unit),ld(A,unit))))),C)),
inference(paramod,[status(thm)],[c_2152,c_3489]) ).
cnf(c_3491,plain,
mult(mult(ld(A,B),A),mult(ld(A,unit),C)) = mult(ld(A,unit),mult(mult(A,mult(ld(A,unit),mult(mult(B,A),ld(A,unit)))),C)),
inference(paramod,[status(thm)],[c_2021,c_3490]) ).
cnf(c_2847,plain,
mult(mult(ld(A,B),A),mult(ld(A,unit),C)) = mult(ld(A,unit),mult(B,C)),
inference(paramod,[status(thm)],[c_1885,c_3491]) ).
cnf(c_3492,plain,
mult(mult(ld(mult(A,mult(ld(A,unit),ld(A,unit))),B),mult(A,mult(ld(A,unit),ld(A,unit)))),mult(A,C)) = mult(ld(mult(A,mult(ld(A,unit),ld(A,unit))),unit),mult(B,C)),
inference(paramod,[status(thm)],[c_1630,c_2847]) ).
cnf(c_3493,plain,
mult(mult(ld(mult(ld(A,unit),unit),B),mult(A,mult(ld(A,unit),ld(A,unit)))),mult(A,C)) = mult(ld(mult(A,mult(ld(A,unit),ld(A,unit))),unit),mult(B,C)),
inference(paramod,[status(thm)],[c_607,c_3492]) ).
cnf(c_3494,plain,
mult(mult(ld(ld(A,unit),B),mult(A,mult(ld(A,unit),ld(A,unit)))),mult(A,C)) = mult(ld(mult(A,mult(ld(A,unit),ld(A,unit))),unit),mult(B,C)),
inference(paramod,[status(thm)],[c_5,c_3493]) ).
cnf(c_3495,plain,
mult(mult(mult(mult(A,A),ld(A,B)),mult(A,mult(ld(A,unit),ld(A,unit)))),mult(A,C)) = mult(ld(mult(A,mult(ld(A,unit),ld(A,unit))),unit),mult(B,C)),
inference(paramod,[status(thm)],[c_2191,c_3494]) ).
cnf(c_3496,plain,
mult(mult(mult(mult(A,A),ld(A,B)),mult(ld(A,unit),unit)),mult(A,C)) = mult(ld(mult(A,mult(ld(A,unit),ld(A,unit))),unit),mult(B,C)),
inference(paramod,[status(thm)],[c_607,c_3495]) ).
cnf(c_3497,plain,
mult(mult(mult(mult(A,A),ld(A,B)),ld(A,unit)),mult(A,C)) = mult(ld(mult(A,mult(ld(A,unit),ld(A,unit))),unit),mult(B,C)),
inference(paramod,[status(thm)],[c_5,c_3496]) ).
cnf(c_3498,plain,
mult(mult(A,mult(mult(A,ld(A,B)),ld(A,unit))),mult(A,C)) = mult(ld(mult(A,mult(ld(A,unit),ld(A,unit))),unit),mult(B,C)),
inference(paramod,[status(thm)],[c_2282,c_3497]) ).
cnf(c_3499,plain,
mult(mult(A,mult(B,ld(A,unit))),mult(A,C)) = mult(ld(mult(A,mult(ld(A,unit),ld(A,unit))),unit),mult(B,C)),
inference(paramod,[status(thm)],[c_1,c_3498]) ).
cnf(c_3500,plain,
mult(mult(A,mult(B,ld(A,unit))),mult(A,C)) = mult(ld(mult(ld(A,unit),unit),unit),mult(B,C)),
inference(paramod,[status(thm)],[c_607,c_3499]) ).
cnf(c_3501,plain,
mult(mult(A,mult(B,ld(A,unit))),mult(A,C)) = mult(ld(ld(A,unit),unit),mult(B,C)),
inference(paramod,[status(thm)],[c_5,c_3500]) ).
cnf(c_3502,plain,
mult(mult(A,mult(B,ld(A,unit))),mult(A,C)) = mult(mult(mult(A,A),ld(A,unit)),mult(B,C)),
inference(paramod,[status(thm)],[c_2191,c_3501]) ).
cnf(c_3096,plain,
mult(mult(A,mult(B,ld(A,unit))),mult(A,C)) = mult(A,mult(B,C)),
inference(paramod,[status(thm)],[c_79,c_3502]) ).
cnf(c_3097,plain,
$false,
inference(resolve,[status(thm)],[c_3096,c_1632]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP698-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.02/0.36 % CPULimit : 300
% 0.02/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Fri Sep 25 15:33:02 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/0.37 % Process 2662729 was started by sandbox2 on n017,
% 0.02/0.37 % Fri Sep 25 15:33:02 2026
% 0.02/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.02/0.37
% 0.02/0.37 % From the command line: assign(max_seconds, 300).
% 16.44/2.55
% 16.44/2.55 % SZS status Unsatisfiable for theBenchmark
% 16.44/2.55
% 16.44/2.55 % Proof 1 at 1.69 (+ 0.33) seconds.
% 16.44/2.55 % Length of proof is 192.
% 16.44/2.55 % Level of proof is 30.
% 16.44/2.55 % Maximum clause weight is 95.000.
% 16.44/2.55 % Given clauses 205.
% 16.44/2.55
% 16.44/2.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------