%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP701-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 : n013.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:14 AM UTC 2026
% Result : Unsatisfiable 16.01s 2.43s
% Output : CNFRefutation 16.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 158
% Number of leaves : 11
% Syntax : Number of formulae : 620 ( 620 unt; 0 def)
% Number of atoms : 620 ( 619 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 1211 ( 0 sgn 18 !; 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(c09,axiom,
! [VAR_0] : mult(VAR_0,i(VAR_0)) = unit,
file('theBenchmark.p',c09) ).
cnf(c_10,plain,
mult(A,i(A)) = unit,
inference(clausify,[status(thm)],[c09]) ).
fof(c10,axiom,
! [VAR_0] : mult(i(VAR_0),VAR_0) = unit,
file('theBenchmark.p',c10) ).
cnf(c_11,plain,
mult(i(A),A) = unit,
inference(clausify,[status(thm)],[c10]) ).
fof(goals,axiom,
mult(a,i(mult(b,a))) != i(b),
file('theBenchmark.p',goals) ).
cnf(c_12,plain,
mult(a,i(mult(b,a))) != i(b),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_13,plain,
ld(rd(A,B),A) = B,
inference(paramod,[status(thm)],[c_3,c_2]) ).
cnf(c_14,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_15,plain,
ld(A,A) = unit,
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_4151,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_19,plain,
mult(A,mult(mult(mult(ld(A,B),A),A),C)) = mult(mult(B,A),mult(A,C)),
inference(copy,[status(thm)],[c_4151]) ).
cnf(c_20,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_21,plain,
mult(mult(mult(ld(A,B),A),ld(A,B)),mult(ld(A,B),C)) = mult(ld(A,B),mult(mult(B,ld(A,B)),C)),
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_22,plain,
mult(mult(mult(A,B),A),mult(A,ld(mult(mult(B,A),A),C))) = mult(A,C),
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_27,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_4152,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_31,plain,
mult(mult(mult(A,B),A),A) = mult(A,mult(mult(B,A),A)),
inference(paramod,[status(thm)],[c_5,c_4152]) ).
cnf(c_33,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_34,plain,
ld(mult(A,mult(B,mult(B,C))),mult(mult(A,B),mult(B,mult(C,B)))) = B,
inference(paramod,[status(thm)],[c_9,c_2]) ).
cnf(c_4153,plain,
mult(A,B) = mult(mult(rd(A,mult(B,mult(B,C))),B),mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_3,c_9]) ).
cnf(c_36,plain,
mult(mult(rd(A,mult(B,mult(B,C))),B),mult(B,mult(C,B))) = mult(A,B),
inference(copy,[status(thm)],[c_4153]) ).
cnf(c_37,plain,
rd(mult(mult(A,B),mult(B,mult(C,B))),B) = mult(A,mult(B,mult(B,C))),
inference(paramod,[status(thm)],[c_9,c_4]) ).
cnf(c_4154,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_38,plain,
mult(mult(A,mult(B,B)),B) = mult(mult(A,B),mult(B,B)),
inference(paramod,[status(thm)],[c_6,c_4154]) ).
cnf(c_4155,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_39,plain,
mult(mult(A,mult(A,B)),A) = mult(A,mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_6,c_4155]) ).
cnf(c_40,plain,
ld(A,unit) = i(A),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_4156,plain,
mult(mult(mult(A,B),A),unit) = mult(A,mult(mult(mult(B,A),A),i(A))),
inference(paramod,[status(thm)],[c_10,c_7]) ).
cnf(c_4157,plain,
mult(mult(A,B),A) = mult(A,mult(mult(mult(B,A),A),i(A))),
inference(paramod,[status(thm)],[c_5,c_4156]) ).
cnf(c_43,plain,
mult(A,mult(mult(mult(B,A),A),i(A))) = mult(mult(A,B),A),
inference(copy,[status(thm)],[c_4157]) ).
cnf(c_4158,plain,
ld(i(A),unit) = A,
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_45,plain,
i(i(A)) = A,
inference(paramod,[status(thm)],[c_40,c_4158]) ).
cnf(c_46,plain,
rd(unit,A) = i(A),
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_4159,plain,
mult(mult(mult(i(A),B),i(A)),unit) = mult(i(A),mult(mult(mult(B,i(A)),i(A)),A)),
inference(paramod,[status(thm)],[c_11,c_7]) ).
cnf(c_4160,plain,
mult(mult(i(A),B),i(A)) = mult(i(A),mult(mult(mult(B,i(A)),i(A)),A)),
inference(paramod,[status(thm)],[c_5,c_4159]) ).
cnf(c_47,plain,
mult(i(A),mult(mult(mult(B,i(A)),i(A)),A)) = mult(mult(i(A),B),i(A)),
inference(copy,[status(thm)],[c_4160]) ).
cnf(c_4161,plain,
mult(A,mult(mult(ld(A,B),A),A)) = mult(mult(B,A),mult(A,unit)),
inference(paramod,[status(thm)],[c_5,c_19]) ).
cnf(c_52,plain,
mult(A,mult(mult(ld(A,B),A),A)) = mult(mult(B,A),A),
inference(paramod,[status(thm)],[c_5,c_4161]) ).
cnf(c_4162,plain,
mult(mult(A,mult(B,mult(B,mult(mult(ld(B,C),B),B)))),B) = mult(mult(A,B),mult(mult(C,B),mult(B,B))),
inference(paramod,[status(thm)],[c_19,c_9]) ).
cnf(c_53,plain,
mult(mult(A,mult(B,mult(mult(C,B),B))),B) = mult(mult(A,B),mult(mult(C,B),mult(B,B))),
inference(paramod,[status(thm)],[c_52,c_4162]) ).
cnf(c_59,plain,
rd(mult(A,mult(mult(mult(B,A),A),ld(A,C))),C) = mult(mult(A,B),A),
inference(paramod,[status(thm)],[c_20,c_4]) ).
cnf(c_4163,plain,
mult(mult(A,A),B) = mult(A,mult(mult(mult(unit,A),A),ld(A,B))),
inference(paramod,[status(thm)],[c_5,c_20]) ).
cnf(c_4164,plain,
mult(mult(A,A),B) = mult(A,mult(mult(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_6,c_4163]) ).
cnf(c_61,plain,
mult(A,mult(mult(A,A),ld(A,B))) = mult(mult(A,A),B),
inference(copy,[status(thm)],[c_4164]) ).
cnf(c_4165,plain,
mult(mult(mult(A,mult(A,B)),A),mult(A,C)) = mult(A,mult(mult(A,mult(mult(mult(B,A),A),ld(A,A))),C)),
inference(paramod,[status(thm)],[c_20,c_7]) ).
cnf(c_4166,plain,
mult(mult(A,mult(A,mult(B,A))),mult(A,C)) = mult(A,mult(mult(A,mult(mult(mult(B,A),A),ld(A,A))),C)),
inference(paramod,[status(thm)],[c_39,c_4165]) ).
cnf(c_4167,plain,
mult(mult(A,mult(A,mult(B,A))),mult(A,C)) = mult(A,mult(mult(A,mult(mult(mult(B,A),A),unit)),C)),
inference(paramod,[status(thm)],[c_15,c_4166]) ).
cnf(c_4168,plain,
mult(mult(A,mult(A,mult(B,A))),mult(A,C)) = mult(A,mult(mult(A,mult(mult(B,A),A)),C)),
inference(paramod,[status(thm)],[c_5,c_4167]) ).
cnf(c_62,plain,
mult(A,mult(mult(A,mult(mult(B,A),A)),C)) = mult(mult(A,mult(A,mult(B,A))),mult(A,C)),
inference(copy,[status(thm)],[c_4168]) ).
cnf(c_68,plain,
ld(A,mult(mult(A,A),B)) = mult(mult(A,A),ld(A,B)),
inference(paramod,[status(thm)],[c_61,c_2]) ).
cnf(c_4169,plain,
mult(A,mult(mult(A,A),ld(A,unit))) = mult(A,A),
inference(paramod,[status(thm)],[c_5,c_61]) ).
cnf(c_70,plain,
mult(A,mult(mult(A,A),i(A))) = mult(A,A),
inference(paramod,[status(thm)],[c_40,c_4169]) ).
cnf(c_4170,plain,
mult(A,mult(mult(A,A),unit)) = mult(mult(A,A),A),
inference(paramod,[status(thm)],[c_15,c_61]) ).
cnf(c_4171,plain,
mult(A,mult(A,A)) = mult(mult(A,A),A),
inference(paramod,[status(thm)],[c_5,c_4170]) ).
cnf(c_73,plain,
mult(mult(A,A),A) = mult(A,mult(A,A)),
inference(copy,[status(thm)],[c_4171]) ).
cnf(c_78,plain,
rd(mult(A,mult(A,A)),A) = mult(A,A),
inference(paramod,[status(thm)],[c_73,c_4]) ).
cnf(c_4172,plain,
ld(A,mult(A,A)) = mult(mult(A,A),i(A)),
inference(paramod,[status(thm)],[c_70,c_2]) ).
cnf(c_4173,plain,
A = mult(mult(A,A),i(A)),
inference(paramod,[status(thm)],[c_2,c_4172]) ).
cnf(c_85,plain,
mult(mult(A,A),i(A)) = A,
inference(copy,[status(thm)],[c_4173]) ).
cnf(c_105,plain,
rd(A,i(A)) = mult(A,A),
inference(paramod,[status(thm)],[c_85,c_4]) ).
cnf(c_109,plain,
mult(mult(i(A),i(A)),A) = i(A),
inference(paramod,[status(thm)],[c_45,c_85]) ).
cnf(c_112,plain,
rd(i(A),A) = mult(i(A),i(A)),
inference(paramod,[status(thm)],[c_45,c_105]) ).
cnf(c_4174,plain,
ld(A,unit) = mult(mult(A,A),ld(A,i(mult(A,A)))),
inference(paramod,[status(thm)],[c_10,c_68]) ).
cnf(c_4175,plain,
i(A) = mult(mult(A,A),ld(A,i(mult(A,A)))),
inference(paramod,[status(thm)],[c_40,c_4174]) ).
cnf(c_118,plain,
mult(mult(A,A),ld(A,i(mult(A,A)))) = i(A),
inference(copy,[status(thm)],[c_4175]) ).
cnf(c_4176,plain,
ld(A,A) = mult(mult(A,A),ld(A,i(A))),
inference(paramod,[status(thm)],[c_85,c_68]) ).
cnf(c_4177,plain,
unit = mult(mult(A,A),ld(A,i(A))),
inference(paramod,[status(thm)],[c_15,c_4176]) ).
cnf(c_120,plain,
mult(mult(A,A),ld(A,i(A))) = unit,
inference(copy,[status(thm)],[c_4177]) ).
cnf(c_127,plain,
rd(mult(A,mult(mult(B,A),C)),mult(A,C)) = mult(mult(A,rd(B,A)),A),
inference(paramod,[status(thm)],[c_27,c_4]) ).
cnf(c_4178,plain,
mult(mult(A,mult(mult(B,A),mult(A,C))),A) = mult(mult(mult(mult(A,rd(B,A)),A),A),mult(A,mult(C,A))),
inference(paramod,[status(thm)],[c_27,c_9]) ).
cnf(c_4179,plain,
mult(mult(A,mult(mult(B,A),mult(A,C))),A) = mult(mult(A,mult(mult(rd(B,A),A),A)),mult(A,mult(C,A))),
inference(paramod,[status(thm)],[c_31,c_4178]) ).
cnf(c_129,plain,
mult(mult(A,mult(mult(B,A),mult(A,C))),A) = mult(mult(A,mult(B,A)),mult(A,mult(C,A))),
inference(paramod,[status(thm)],[c_3,c_4179]) ).
cnf(c_4180,plain,
mult(mult(mult(A,rd(B,A)),A),unit) = mult(A,mult(mult(B,A),i(A))),
inference(paramod,[status(thm)],[c_10,c_27]) ).
cnf(c_130,plain,
mult(mult(A,rd(B,A)),A) = mult(A,mult(mult(B,A),i(A))),
inference(paramod,[status(thm)],[c_5,c_4180]) ).
cnf(c_4181,plain,
mult(mult(mult(mult(mult(A,rd(B,A)),A),C),mult(mult(A,rd(B,A)),A)),mult(mult(mult(A,rd(B,A)),A),ld(mult(mult(C,mult(mult(A,rd(B,A)),A)),mult(mult(A,rd(B,A)),A)),mult(A,D)))) = mult(A,mult(mult(B,A),D)),
inference(paramod,[status(thm)],[c_27,c_22]) ).
cnf(c_4182,plain,
mult(mult(mult(mult(A,mult(mult(B,A),i(A))),C),mult(mult(A,rd(B,A)),A)),mult(mult(mult(A,rd(B,A)),A),ld(mult(mult(C,mult(mult(A,rd(B,A)),A)),mult(mult(A,rd(B,A)),A)),mult(A,D)))) = mult(A,mult(mult(B,A),D)),
inference(paramod,[status(thm)],[c_130,c_4181]) ).
cnf(c_4183,plain,
mult(mult(mult(mult(A,mult(mult(B,A),i(A))),C),mult(A,mult(mult(B,A),i(A)))),mult(mult(mult(A,rd(B,A)),A),ld(mult(mult(C,mult(mult(A,rd(B,A)),A)),mult(mult(A,rd(B,A)),A)),mult(A,D)))) = mult(A,mult(mult(B,A),D)),
inference(paramod,[status(thm)],[c_130,c_4182]) ).
cnf(c_4184,plain,
mult(mult(mult(mult(A,mult(mult(B,A),i(A))),C),mult(A,mult(mult(B,A),i(A)))),mult(mult(A,mult(mult(B,A),i(A))),ld(mult(mult(C,mult(mult(A,rd(B,A)),A)),mult(mult(A,rd(B,A)),A)),mult(A,D)))) = mult(A,mult(mult(B,A),D)),
inference(paramod,[status(thm)],[c_130,c_4183]) ).
cnf(c_4185,plain,
mult(mult(mult(mult(A,mult(mult(B,A),i(A))),C),mult(A,mult(mult(B,A),i(A)))),mult(mult(A,mult(mult(B,A),i(A))),ld(mult(mult(C,mult(A,mult(mult(B,A),i(A)))),mult(mult(A,rd(B,A)),A)),mult(A,D)))) = mult(A,mult(mult(B,A),D)),
inference(paramod,[status(thm)],[c_130,c_4184]) ).
cnf(c_4186,plain,
mult(mult(mult(mult(A,mult(mult(B,A),i(A))),C),mult(A,mult(mult(B,A),i(A)))),mult(mult(A,mult(mult(B,A),i(A))),ld(mult(mult(C,mult(A,mult(mult(B,A),i(A)))),mult(A,mult(mult(B,A),i(A)))),mult(A,D)))) = mult(A,mult(mult(B,A),D)),
inference(paramod,[status(thm)],[c_130,c_4185]) ).
cnf(c_133,plain,
mult(mult(A,mult(mult(B,A),i(A))),mult(A,C)) = mult(A,mult(mult(B,A),C)),
inference(paramod,[status(thm)],[c_22,c_4186]) ).
cnf(c_136,plain,
rd(mult(A,mult(mult(B,A),C)),mult(A,C)) = mult(A,mult(mult(B,A),i(A))),
inference(paramod,[status(thm)],[c_130,c_127]) ).
cnf(c_4187,plain,
ld(mult(A,A),unit) = ld(A,i(A)),
inference(paramod,[status(thm)],[c_120,c_2]) ).
cnf(c_4188,plain,
i(mult(A,A)) = ld(A,i(A)),
inference(paramod,[status(thm)],[c_40,c_4187]) ).
cnf(c_146,plain,
ld(A,i(A)) = i(mult(A,A)),
inference(copy,[status(thm)],[c_4188]) ).
cnf(c_147,plain,
mult(A,i(mult(A,A))) = i(A),
inference(paramod,[status(thm)],[c_146,c_1]) ).
cnf(c_150,plain,
mult(mult(mult(A,B),A),i(A)) = mult(A,mult(mult(mult(B,A),A),i(mult(A,A)))),
inference(paramod,[status(thm)],[c_146,c_20]) ).
cnf(c_152,plain,
ld(i(A),A) = i(mult(i(A),i(A))),
inference(paramod,[status(thm)],[c_45,c_146]) ).
cnf(c_4189,plain,
mult(mult(A,B),A) = mult(mult(unit,A),mult(A,mult(ld(A,B),A))),
inference(paramod,[status(thm)],[c_6,c_33]) ).
cnf(c_4190,plain,
mult(mult(A,B),A) = mult(A,mult(A,mult(ld(A,B),A))),
inference(paramod,[status(thm)],[c_6,c_4189]) ).
cnf(c_185,plain,
mult(A,mult(A,mult(ld(A,B),A))) = mult(mult(A,B),A),
inference(copy,[status(thm)],[c_4190]) ).
cnf(c_4191,plain,
mult(mult(i(A),mult(A,B)),A) = mult(unit,mult(A,mult(ld(A,B),A))),
inference(paramod,[status(thm)],[c_11,c_33]) ).
cnf(c_4192,plain,
mult(mult(i(A),mult(A,B)),A) = mult(A,mult(ld(A,B),A)),
inference(paramod,[status(thm)],[c_6,c_4191]) ).
cnf(c_190,plain,
mult(A,mult(ld(A,B),A)) = mult(mult(i(A),mult(A,B)),A),
inference(copy,[status(thm)],[c_4192]) ).
cnf(c_4193,plain,
mult(mult(A,i(B)),B) = mult(mult(A,B),mult(B,mult(ld(B,i(mult(B,B))),B))),
inference(paramod,[status(thm)],[c_147,c_33]) ).
cnf(c_4194,plain,
mult(mult(A,i(B)),B) = mult(mult(A,B),mult(mult(i(B),mult(B,i(mult(B,B)))),B)),
inference(paramod,[status(thm)],[c_190,c_4193]) ).
cnf(c_4195,plain,
mult(mult(A,i(B)),B) = mult(mult(A,B),mult(mult(i(B),i(B)),B)),
inference(paramod,[status(thm)],[c_147,c_4194]) ).
cnf(c_204,plain,
mult(mult(A,i(B)),B) = mult(mult(A,B),i(B)),
inference(paramod,[status(thm)],[c_109,c_4195]) ).
cnf(c_208,plain,
mult(A,mult(mult(i(A),mult(A,B)),A)) = mult(mult(A,B),A),
inference(paramod,[status(thm)],[c_190,c_185]) ).
cnf(c_4196,plain,
mult(i(A),mult(mult(mult(B,i(A)),A),i(A))) = mult(mult(i(A),B),i(A)),
inference(paramod,[status(thm)],[c_204,c_47]) ).
cnf(c_219,plain,
mult(i(A),mult(mult(mult(B,A),i(A)),i(A))) = mult(mult(i(A),B),i(A)),
inference(paramod,[status(thm)],[c_204,c_4196]) ).
cnf(c_222,plain,
rd(i(A),ld(A,i(mult(A,A)))) = mult(A,A),
inference(paramod,[status(thm)],[c_118,c_4]) ).
cnf(c_228,plain,
rd(A,ld(i(A),i(mult(i(A),i(A))))) = mult(i(A),i(A)),
inference(paramod,[status(thm)],[c_45,c_222]) ).
cnf(c_230,plain,
ld(mult(A,i(B)),mult(mult(A,B),i(B))) = B,
inference(paramod,[status(thm)],[c_204,c_2]) ).
cnf(c_4197,plain,
mult(i(A),mult(mult(mult(ld(i(A),B),i(A)),A),i(A))) = mult(mult(B,i(A)),mult(i(A),A)),
inference(paramod,[status(thm)],[c_204,c_19]) ).
cnf(c_4198,plain,
mult(i(A),mult(mult(mult(ld(i(A),B),A),i(A)),i(A))) = mult(mult(B,i(A)),mult(i(A),A)),
inference(paramod,[status(thm)],[c_204,c_4197]) ).
cnf(c_4199,plain,
mult(i(A),mult(mult(mult(ld(i(A),B),A),i(A)),i(A))) = mult(mult(B,i(A)),unit),
inference(paramod,[status(thm)],[c_11,c_4198]) ).
cnf(c_235,plain,
mult(i(A),mult(mult(mult(ld(i(A),B),A),i(A)),i(A))) = mult(B,i(A)),
inference(paramod,[status(thm)],[c_5,c_4199]) ).
cnf(c_4200,plain,
mult(mult(mult(A,A),i(A)),A) = mult(mult(A,mult(A,A)),i(A)),
inference(paramod,[status(thm)],[c_73,c_204]) ).
cnf(c_4201,plain,
mult(A,A) = mult(mult(A,mult(A,A)),i(A)),
inference(paramod,[status(thm)],[c_85,c_4200]) ).
cnf(c_240,plain,
mult(mult(A,mult(A,A)),i(A)) = mult(A,A),
inference(copy,[status(thm)],[c_4201]) ).
cnf(c_4202,plain,
mult(i(A),mult(A,A)) = mult(mult(A,mult(A,A)),i(mult(A,A))),
inference(paramod,[status(thm)],[c_147,c_204]) ).
cnf(c_245,plain,
mult(mult(A,mult(A,A)),i(mult(A,A))) = mult(i(A),mult(A,A)),
inference(copy,[status(thm)],[c_4202]) ).
cnf(c_4203,plain,
mult(mult(i(A),mult(mult(B,i(A)),i(A))),A) = mult(mult(mult(mult(i(A),B),i(A)),A),i(A)),
inference(paramod,[status(thm)],[c_31,c_204]) ).
cnf(c_4204,plain,
mult(mult(i(A),mult(mult(B,i(A)),i(A))),A) = mult(mult(mult(mult(i(A),B),A),i(A)),i(A)),
inference(paramod,[status(thm)],[c_204,c_4203]) ).
cnf(c_246,plain,
mult(mult(mult(mult(i(A),B),A),i(A)),i(A)) = mult(mult(i(A),mult(mult(B,i(A)),i(A))),A),
inference(copy,[status(thm)],[c_4204]) ).
cnf(c_248,plain,
ld(mult(rd(A,B),i(B)),mult(A,i(B))) = B,
inference(paramod,[status(thm)],[c_3,c_230]) ).
cnf(c_4205,plain,
ld(mult(mult(A,A),i(i(A))),mult(A,i(i(A)))) = i(A),
inference(paramod,[status(thm)],[c_85,c_230]) ).
cnf(c_4206,plain,
ld(mult(mult(A,A),A),mult(A,i(i(A)))) = i(A),
inference(paramod,[status(thm)],[c_45,c_4205]) ).
cnf(c_4207,plain,
ld(mult(A,mult(A,A)),mult(A,i(i(A)))) = i(A),
inference(paramod,[status(thm)],[c_73,c_4206]) ).
cnf(c_256,plain,
ld(mult(A,mult(A,A)),mult(A,A)) = i(A),
inference(paramod,[status(thm)],[c_45,c_4207]) ).
cnf(c_4208,plain,
ld(mult(A,i(i(mult(A,A)))),mult(i(A),i(i(mult(A,A))))) = i(mult(A,A)),
inference(paramod,[status(thm)],[c_147,c_230]) ).
cnf(c_4209,plain,
ld(mult(A,mult(A,A)),mult(i(A),i(i(mult(A,A))))) = i(mult(A,A)),
inference(paramod,[status(thm)],[c_45,c_4208]) ).
cnf(c_257,plain,
ld(mult(A,mult(A,A)),mult(i(A),mult(A,A))) = i(mult(A,A)),
inference(paramod,[status(thm)],[c_45,c_4209]) ).
cnf(c_4210,plain,
ld(mult(A,mult(B,B)),mult(mult(A,B),mult(B,mult(unit,B)))) = B,
inference(paramod,[status(thm)],[c_5,c_34]) ).
cnf(c_267,plain,
ld(mult(A,mult(B,B)),mult(mult(A,B),mult(B,B))) = B,
inference(paramod,[status(thm)],[c_6,c_4210]) ).
cnf(c_292,plain,
rd(mult(A,B),mult(B,mult(C,B))) = mult(rd(A,mult(B,mult(B,C))),B),
inference(paramod,[status(thm)],[c_36,c_4]) ).
cnf(c_4211,plain,
mult(mult(rd(A,mult(B,B)),B),mult(B,mult(unit,B))) = mult(A,B),
inference(paramod,[status(thm)],[c_5,c_36]) ).
cnf(c_293,plain,
mult(mult(rd(A,mult(B,B)),B),mult(B,B)) = mult(A,B),
inference(paramod,[status(thm)],[c_6,c_4211]) ).
cnf(c_306,plain,
rd(mult(A,i(B)),B) = mult(rd(A,B),i(B)),
inference(paramod,[status(thm)],[c_248,c_14]) ).
cnf(c_4212,plain,
rd(mult(A,B),i(B)) = mult(rd(A,i(B)),i(i(B))),
inference(paramod,[status(thm)],[c_45,c_306]) ).
cnf(c_318,plain,
rd(mult(A,B),i(B)) = mult(rd(A,i(B)),B),
inference(paramod,[status(thm)],[c_45,c_4212]) ).
cnf(c_4213,plain,
rd(A,i(B)) = mult(rd(rd(A,B),i(B)),B),
inference(paramod,[status(thm)],[c_3,c_318]) ).
cnf(c_325,plain,
mult(rd(rd(A,B),i(B)),B) = rd(A,i(B)),
inference(copy,[status(thm)],[c_4213]) ).
cnf(c_4214,plain,
mult(mult(mult(i(A),mult(A,mult(A,A))),ld(mult(A,mult(A,A)),mult(A,A))),mult(ld(mult(A,mult(A,A)),mult(A,A)),B)) = mult(ld(mult(A,mult(A,A)),mult(A,A)),mult(mult(mult(A,A),ld(mult(A,mult(A,A)),mult(A,A))),B)),
inference(paramod,[status(thm)],[c_256,c_21]) ).
cnf(c_4215,plain,
mult(mult(mult(i(A),mult(A,mult(A,A))),i(A)),mult(ld(mult(A,mult(A,A)),mult(A,A)),B)) = mult(ld(mult(A,mult(A,A)),mult(A,A)),mult(mult(mult(A,A),ld(mult(A,mult(A,A)),mult(A,A))),B)),
inference(paramod,[status(thm)],[c_256,c_4214]) ).
cnf(c_4216,plain,
mult(mult(mult(i(A),mult(A,mult(A,A))),i(A)),mult(i(A),B)) = mult(ld(mult(A,mult(A,A)),mult(A,A)),mult(mult(mult(A,A),ld(mult(A,mult(A,A)),mult(A,A))),B)),
inference(paramod,[status(thm)],[c_256,c_4215]) ).
cnf(c_4217,plain,
mult(mult(mult(i(A),mult(A,mult(A,A))),i(A)),mult(i(A),B)) = mult(i(A),mult(mult(mult(A,A),ld(mult(A,mult(A,A)),mult(A,A))),B)),
inference(paramod,[status(thm)],[c_256,c_4216]) ).
cnf(c_4218,plain,
mult(mult(mult(i(A),mult(A,mult(A,A))),i(A)),mult(i(A),B)) = mult(i(A),mult(mult(mult(A,A),i(A)),B)),
inference(paramod,[status(thm)],[c_256,c_4217]) ).
cnf(c_338,plain,
mult(mult(mult(i(A),mult(A,mult(A,A))),i(A)),mult(i(A),B)) = mult(i(A),mult(A,B)),
inference(paramod,[status(thm)],[c_85,c_4218]) ).
cnf(c_359,plain,
rd(mult(A,mult(B,mult(C,B))),B) = mult(rd(A,B),mult(B,mult(B,C))),
inference(paramod,[status(thm)],[c_3,c_37]) ).
cnf(c_4219,plain,
rd(mult(unit,mult(A,mult(B,A))),A) = mult(i(A),mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_11,c_37]) ).
cnf(c_363,plain,
rd(mult(A,mult(B,A)),A) = mult(i(A),mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_6,c_4219]) ).
cnf(c_371,plain,
mult(i(A),mult(A,mult(A,A))) = mult(A,A),
inference(paramod,[status(thm)],[c_363,c_78]) ).
cnf(c_4220,plain,
mult(mult(mult(A,A),i(A)),mult(i(A),B)) = mult(i(A),mult(A,B)),
inference(paramod,[status(thm)],[c_371,c_338]) ).
cnf(c_4221,plain,
mult(A,mult(i(A),B)) = mult(i(A),mult(A,B)),
inference(paramod,[status(thm)],[c_85,c_4220]) ).
cnf(c_372,plain,
mult(i(A),mult(A,B)) = mult(A,mult(i(A),B)),
inference(copy,[status(thm)],[c_4221]) ).
cnf(c_4222,plain,
rd(mult(A,mult(B,A)),A) = mult(A,mult(i(A),mult(A,B))),
inference(paramod,[status(thm)],[c_372,c_363]) ).
cnf(c_374,plain,
rd(mult(A,mult(B,A)),A) = mult(A,mult(A,mult(i(A),B))),
inference(paramod,[status(thm)],[c_372,c_4222]) ).
cnf(c_4223,plain,
ld(mult(A,mult(A,A)),mult(A,mult(i(A),A))) = i(mult(A,A)),
inference(paramod,[status(thm)],[c_372,c_257]) ).
cnf(c_4224,plain,
ld(mult(A,mult(A,A)),mult(A,unit)) = i(mult(A,A)),
inference(paramod,[status(thm)],[c_11,c_4223]) ).
cnf(c_379,plain,
ld(mult(A,mult(A,A)),A) = i(mult(A,A)),
inference(paramod,[status(thm)],[c_5,c_4224]) ).
cnf(c_4225,plain,
mult(mult(A,mult(A,A)),i(mult(A,A))) = mult(A,mult(i(A),A)),
inference(paramod,[status(thm)],[c_372,c_245]) ).
cnf(c_4226,plain,
mult(mult(A,mult(A,A)),i(mult(A,A))) = mult(A,unit),
inference(paramod,[status(thm)],[c_11,c_4225]) ).
cnf(c_380,plain,
mult(mult(A,mult(A,A)),i(mult(A,A))) = A,
inference(paramod,[status(thm)],[c_5,c_4226]) ).
cnf(c_387,plain,
mult(A,mult(mult(A,mult(i(A),B)),A)) = mult(mult(A,B),A),
inference(paramod,[status(thm)],[c_372,c_208]) ).
cnf(c_395,plain,
mult(A,mult(ld(A,B),A)) = mult(mult(A,mult(i(A),B)),A),
inference(paramod,[status(thm)],[c_372,c_190]) ).
cnf(c_4227,plain,
mult(mult(mult(A,mult(B,B)),i(mult(B,B))),B) = mult(mult(mult(A,i(mult(B,B))),B),mult(B,B)),
inference(paramod,[status(thm)],[c_204,c_38]) ).
cnf(c_403,plain,
mult(mult(mult(A,i(mult(B,B))),B),mult(B,B)) = mult(mult(mult(A,mult(B,B)),i(mult(B,B))),B),
inference(copy,[status(thm)],[c_4227]) ).
cnf(c_422,plain,
rd(A,i(mult(A,A))) = mult(A,mult(A,A)),
inference(paramod,[status(thm)],[c_379,c_14]) ).
cnf(c_429,plain,
rd(rd(A,i(B)),B) = rd(rd(A,B),i(B)),
inference(paramod,[status(thm)],[c_325,c_4]) ).
cnf(c_4228,plain,
mult(rd(mult(A,mult(A,A)),i(i(mult(A,A)))),i(mult(A,A))) = rd(A,i(i(mult(A,A)))),
inference(paramod,[status(thm)],[c_422,c_325]) ).
cnf(c_4229,plain,
mult(rd(mult(A,mult(A,A)),mult(A,A)),i(mult(A,A))) = rd(A,i(i(mult(A,A)))),
inference(paramod,[status(thm)],[c_45,c_4228]) ).
cnf(c_4230,plain,
mult(A,i(mult(A,A))) = rd(A,i(i(mult(A,A)))),
inference(paramod,[status(thm)],[c_4,c_4229]) ).
cnf(c_4231,plain,
i(A) = rd(A,i(i(mult(A,A)))),
inference(paramod,[status(thm)],[c_147,c_4230]) ).
cnf(c_4232,plain,
i(A) = rd(A,mult(A,A)),
inference(paramod,[status(thm)],[c_45,c_4231]) ).
cnf(c_439,plain,
rd(A,mult(A,A)) = i(A),
inference(copy,[status(thm)],[c_4232]) ).
cnf(c_4233,plain,
ld(i(A),A) = mult(A,A),
inference(paramod,[status(thm)],[c_439,c_13]) ).
cnf(c_444,plain,
i(mult(i(A),i(A))) = mult(A,A),
inference(paramod,[status(thm)],[c_152,c_4233]) ).
cnf(c_449,plain,
rd(A,ld(i(A),mult(A,A))) = mult(i(A),i(A)),
inference(paramod,[status(thm)],[c_444,c_228]) ).
cnf(c_451,plain,
ld(i(A),A) = mult(A,A),
inference(paramod,[status(thm)],[c_444,c_152]) ).
cnf(c_4234,plain,
ld(A,i(A)) = mult(i(A),i(A)),
inference(paramod,[status(thm)],[c_45,c_451]) ).
cnf(c_454,plain,
i(mult(A,A)) = mult(i(A),i(A)),
inference(paramod,[status(thm)],[c_146,c_4234]) ).
cnf(c_4235,plain,
mult(mult(mult(A,mult(i(B),i(B))),B),mult(B,B)) = mult(mult(mult(A,mult(B,B)),i(mult(B,B))),B),
inference(paramod,[status(thm)],[c_454,c_403]) ).
cnf(c_465,plain,
mult(mult(mult(A,mult(i(B),i(B))),B),mult(B,B)) = mult(mult(mult(A,mult(B,B)),mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_454,c_4235]) ).
cnf(c_466,plain,
mult(mult(A,mult(A,A)),mult(i(A),i(A))) = A,
inference(paramod,[status(thm)],[c_454,c_380]) ).
cnf(c_491,plain,
mult(mult(mult(A,B),A),i(A)) = mult(A,mult(mult(mult(B,A),A),mult(i(A),i(A)))),
inference(paramod,[status(thm)],[c_454,c_150]) ).
cnf(c_492,plain,
mult(A,mult(i(A),i(A))) = i(A),
inference(paramod,[status(thm)],[c_454,c_147]) ).
cnf(c_493,plain,
ld(A,i(A)) = mult(i(A),i(A)),
inference(paramod,[status(thm)],[c_454,c_146]) ).
cnf(c_4236,plain,
mult(mult(A,mult(i(B),i(B))),mult(B,B)) = mult(mult(A,mult(B,B)),i(mult(B,B))),
inference(paramod,[status(thm)],[c_454,c_204]) ).
cnf(c_499,plain,
mult(mult(A,mult(i(B),i(B))),mult(B,B)) = mult(mult(A,mult(B,B)),mult(i(B),i(B))),
inference(paramod,[status(thm)],[c_454,c_4236]) ).
cnf(c_4237,plain,
mult(A,mult(mult(mult(mult(B,A),mult(A,A)),A),i(A))) = mult(mult(A,mult(B,mult(A,A))),A),
inference(paramod,[status(thm)],[c_38,c_43]) ).
cnf(c_525,plain,
mult(A,mult(mult(mult(mult(B,A),A),mult(A,A)),i(A))) = mult(mult(A,mult(B,mult(A,A))),A),
inference(paramod,[status(thm)],[c_38,c_4237]) ).
cnf(c_558,plain,
mult(mult(i(A),i(A)),ld(i(A),mult(A,A))) = A,
inference(paramod,[status(thm)],[c_449,c_3]) ).
cnf(c_4238,plain,
mult(mult(A,mult(B,mult(C,B))),B) = mult(mult(A,B),mult(mult(rd(C,B),B),mult(B,B))),
inference(paramod,[status(thm)],[c_3,c_53]) ).
cnf(c_627,plain,
mult(mult(A,mult(B,mult(C,B))),B) = mult(mult(A,B),mult(C,mult(B,B))),
inference(paramod,[status(thm)],[c_3,c_4238]) ).
cnf(c_4239,plain,
mult(mult(mult(i(A),mult(A,mult(A,A))),i(A)),mult(i(A),ld(mult(mult(A,A),i(A)),B))) = mult(i(A),B),
inference(paramod,[status(thm)],[c_240,c_22]) ).
cnf(c_4240,plain,
mult(mult(mult(A,mult(i(A),mult(A,A))),i(A)),mult(i(A),ld(mult(mult(A,A),i(A)),B))) = mult(i(A),B),
inference(paramod,[status(thm)],[c_372,c_4239]) ).
cnf(c_4241,plain,
mult(mult(mult(A,mult(A,mult(i(A),A))),i(A)),mult(i(A),ld(mult(mult(A,A),i(A)),B))) = mult(i(A),B),
inference(paramod,[status(thm)],[c_372,c_4240]) ).
cnf(c_4242,plain,
mult(mult(mult(A,mult(A,unit)),i(A)),mult(i(A),ld(mult(mult(A,A),i(A)),B))) = mult(i(A),B),
inference(paramod,[status(thm)],[c_11,c_4241]) ).
cnf(c_4243,plain,
mult(mult(mult(A,A),i(A)),mult(i(A),ld(mult(mult(A,A),i(A)),B))) = mult(i(A),B),
inference(paramod,[status(thm)],[c_5,c_4242]) ).
cnf(c_4244,plain,
mult(A,mult(i(A),ld(mult(mult(A,A),i(A)),B))) = mult(i(A),B),
inference(paramod,[status(thm)],[c_85,c_4243]) ).
cnf(c_651,plain,
mult(A,mult(i(A),ld(A,B))) = mult(i(A),B),
inference(paramod,[status(thm)],[c_85,c_4244]) ).
cnf(c_659,plain,
ld(A,mult(i(A),B)) = mult(i(A),ld(A,B)),
inference(paramod,[status(thm)],[c_651,c_2]) ).
cnf(c_660,plain,
rd(mult(i(A),B),mult(i(A),ld(A,B))) = A,
inference(paramod,[status(thm)],[c_651,c_4]) ).
cnf(c_4245,plain,
mult(rd(A,B),mult(i(rd(A,B)),B)) = mult(i(rd(A,B)),A),
inference(paramod,[status(thm)],[c_13,c_651]) ).
cnf(c_665,plain,
mult(i(rd(A,B)),A) = mult(rd(A,B),mult(i(rd(A,B)),B)),
inference(copy,[status(thm)],[c_4245]) ).
cnf(c_4246,plain,
ld(A,B) = mult(i(A),ld(A,ld(i(A),B))),
inference(paramod,[status(thm)],[c_1,c_659]) ).
cnf(c_698,plain,
mult(i(A),ld(A,ld(i(A),B))) = ld(A,B),
inference(copy,[status(thm)],[c_4246]) ).
cnf(c_4247,plain,
ld(i(A),mult(A,B)) = mult(i(i(A)),ld(i(A),B)),
inference(paramod,[status(thm)],[c_45,c_659]) ).
cnf(c_702,plain,
ld(i(A),mult(A,B)) = mult(A,ld(i(A),B)),
inference(paramod,[status(thm)],[c_45,c_4247]) ).
cnf(c_4248,plain,
mult(mult(i(A),i(A)),mult(A,ld(i(A),A))) = A,
inference(paramod,[status(thm)],[c_702,c_558]) ).
cnf(c_714,plain,
mult(mult(i(A),i(A)),mult(A,mult(A,A))) = A,
inference(paramod,[status(thm)],[c_451,c_4248]) ).
cnf(c_4249,plain,
rd(mult(A,B),mult(i(i(A)),ld(i(A),B))) = i(A),
inference(paramod,[status(thm)],[c_45,c_660]) ).
cnf(c_721,plain,
rd(mult(A,B),mult(A,ld(i(A),B))) = i(A),
inference(paramod,[status(thm)],[c_45,c_4249]) ).
cnf(c_4250,plain,
ld(i(A),B) = mult(A,ld(i(A),ld(A,B))),
inference(paramod,[status(thm)],[c_1,c_702]) ).
cnf(c_727,plain,
mult(A,ld(i(A),ld(A,B))) = ld(i(A),B),
inference(copy,[status(thm)],[c_4250]) ).
cnf(c_4251,plain,
ld(i(rd(A,B)),A) = mult(rd(A,B),ld(i(rd(A,B)),B)),
inference(paramod,[status(thm)],[c_3,c_702]) ).
cnf(c_728,plain,
mult(rd(A,B),ld(i(rd(A,B)),B)) = ld(i(rd(A,B)),A),
inference(copy,[status(thm)],[c_4251]) ).
cnf(c_765,plain,
rd(mult(A,mult(mult(mult(B,A),A),mult(i(A),i(A)))),i(A)) = mult(mult(A,B),A),
inference(paramod,[status(thm)],[c_493,c_59]) ).
cnf(c_772,plain,
rd(A,mult(rd(A,B),ld(i(rd(A,B)),B))) = i(rd(A,B)),
inference(paramod,[status(thm)],[c_3,c_721]) ).
cnf(c_4252,plain,
ld(A,ld(i(A),B)) = ld(i(A),ld(A,B)),
inference(paramod,[status(thm)],[c_727,c_2]) ).
cnf(c_788,plain,
ld(i(A),ld(A,B)) = ld(A,ld(i(A),B)),
inference(copy,[status(thm)],[c_4252]) ).
cnf(c_4253,plain,
mult(mult(A,ld(i(A),B)),A) = mult(A,mult(A,mult(ld(i(A),ld(A,B)),A))),
inference(paramod,[status(thm)],[c_727,c_39]) ).
cnf(c_4254,plain,
mult(mult(A,ld(i(A),B)),A) = mult(A,mult(A,mult(ld(A,ld(i(A),B)),A))),
inference(paramod,[status(thm)],[c_788,c_4253]) ).
cnf(c_4255,plain,
mult(mult(A,ld(i(A),B)),A) = mult(A,mult(mult(A,mult(i(A),ld(i(A),B))),A)),
inference(paramod,[status(thm)],[c_395,c_4254]) ).
cnf(c_795,plain,
mult(mult(A,ld(i(A),B)),A) = mult(A,mult(mult(A,B),A)),
inference(paramod,[status(thm)],[c_1,c_4255]) ).
cnf(c_4256,plain,
mult(A,mult(mult(mult(B,A),mult(A,A)),C)) = mult(mult(A,mult(A,mult(mult(ld(A,B),A),A))),mult(A,C)),
inference(paramod,[status(thm)],[c_19,c_62]) ).
cnf(c_850,plain,
mult(A,mult(mult(mult(B,A),mult(A,A)),C)) = mult(mult(A,mult(mult(B,A),A)),mult(A,C)),
inference(paramod,[status(thm)],[c_52,c_4256]) ).
cnf(c_4257,plain,
mult(mult(A,mult(mult(mult(B,A),A),A)),mult(A,i(A))) = mult(mult(A,mult(B,mult(A,A))),A),
inference(paramod,[status(thm)],[c_850,c_525]) ).
cnf(c_4258,plain,
mult(mult(A,mult(mult(mult(B,A),A),A)),unit) = mult(mult(A,mult(B,mult(A,A))),A),
inference(paramod,[status(thm)],[c_10,c_4257]) ).
cnf(c_854,plain,
mult(A,mult(mult(mult(B,A),A),A)) = mult(mult(A,mult(B,mult(A,A))),A),
inference(paramod,[status(thm)],[c_5,c_4258]) ).
cnf(c_4259,plain,
mult(rd(A,B),mult(mult(mult(ld(i(rd(A,B)),B),rd(A,B)),rd(A,B)),i(rd(A,B)))) = mult(ld(i(rd(A,B)),A),rd(A,B)),
inference(paramod,[status(thm)],[c_728,c_43]) ).
cnf(c_4260,plain,
mult(mult(rd(A,B),ld(i(rd(A,B)),B)),rd(A,B)) = mult(ld(i(rd(A,B)),A),rd(A,B)),
inference(paramod,[status(thm)],[c_43,c_4259]) ).
cnf(c_4261,plain,
mult(rd(A,B),mult(mult(rd(A,B),B),rd(A,B))) = mult(ld(i(rd(A,B)),A),rd(A,B)),
inference(paramod,[status(thm)],[c_795,c_4260]) ).
cnf(c_4262,plain,
mult(rd(A,B),mult(A,rd(A,B))) = mult(ld(i(rd(A,B)),A),rd(A,B)),
inference(paramod,[status(thm)],[c_3,c_4261]) ).
cnf(c_897,plain,
mult(ld(i(rd(A,B)),A),rd(A,B)) = mult(rd(A,B),mult(A,rd(A,B))),
inference(copy,[status(thm)],[c_4262]) ).
cnf(c_961,plain,
mult(mult(mult(A,mult(i(A),B)),i(A)),i(A)) = mult(i(A),mult(mult(mult(A,B),i(A)),i(A))),
inference(paramod,[status(thm)],[c_372,c_31]) ).
cnf(c_4263,plain,
mult(mult(i(A),i(A)),mult(mult(A,A),B)) = mult(mult(A,A),mult(i(mult(A,A)),B)),
inference(paramod,[status(thm)],[c_454,c_372]) ).
cnf(c_972,plain,
mult(mult(i(A),i(A)),mult(mult(A,A),B)) = mult(mult(A,A),mult(mult(i(A),i(A)),B)),
inference(paramod,[status(thm)],[c_454,c_4263]) ).
cnf(c_4264,plain,
mult(i(A),mult(mult(mult(mult(A,B),i(A)),i(A)),i(i(A)))) = mult(mult(A,mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_372,c_43]) ).
cnf(c_4265,plain,
mult(i(A),mult(mult(mult(mult(A,B),i(A)),i(A)),A)) = mult(mult(A,mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_45,c_4264]) ).
cnf(c_4266,plain,
mult(i(A),mult(mult(mult(mult(A,B),i(A)),A),i(A))) = mult(mult(A,mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_204,c_4265]) ).
cnf(c_973,plain,
mult(i(A),mult(mult(mult(mult(A,B),A),i(A)),i(A))) = mult(mult(A,mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_204,c_4266]) ).
cnf(c_4267,plain,
mult(i(A),mult(mult(A,B),A)) = mult(A,mult(i(A),mult(mult(mult(B,A),A),i(A)))),
inference(paramod,[status(thm)],[c_43,c_372]) ).
cnf(c_974,plain,
mult(A,mult(i(A),mult(mult(mult(B,A),A),i(A)))) = mult(i(A),mult(mult(A,B),A)),
inference(copy,[status(thm)],[c_4267]) ).
cnf(c_4268,plain,
mult(i(A),mult(mult(mult(ld(A,ld(i(A),B)),i(A)),i(A)),i(i(A)))) = mult(ld(A,B),i(A)),
inference(paramod,[status(thm)],[c_698,c_43]) ).
cnf(c_4269,plain,
mult(i(A),mult(mult(mult(ld(A,ld(i(A),B)),i(A)),i(A)),A)) = mult(ld(A,B),i(A)),
inference(paramod,[status(thm)],[c_45,c_4268]) ).
cnf(c_4270,plain,
mult(i(A),mult(mult(mult(ld(A,ld(i(A),B)),i(A)),A),i(A))) = mult(ld(A,B),i(A)),
inference(paramod,[status(thm)],[c_204,c_4269]) ).
cnf(c_1052,plain,
mult(i(A),mult(mult(mult(ld(A,ld(i(A),B)),A),i(A)),i(A))) = mult(ld(A,B),i(A)),
inference(paramod,[status(thm)],[c_204,c_4270]) ).
cnf(c_1706,plain,
ld(mult(rd(A,B),mult(B,B)),mult(A,mult(B,B))) = B,
inference(paramod,[status(thm)],[c_3,c_267]) ).
cnf(c_1724,plain,
rd(mult(A,mult(B,B)),B) = mult(rd(A,B),mult(B,B)),
inference(paramod,[status(thm)],[c_1706,c_14]) ).
cnf(c_4271,plain,
rd(mult(A,mult(mult(mult(B,A),A),A)),A) = mult(rd(mult(mult(A,B),A),A),mult(A,A)),
inference(paramod,[status(thm)],[c_7,c_1724]) ).
cnf(c_4272,plain,
rd(mult(mult(A,mult(B,mult(A,A))),A),A) = mult(rd(mult(mult(A,B),A),A),mult(A,A)),
inference(paramod,[status(thm)],[c_854,c_4271]) ).
cnf(c_4273,plain,
mult(A,mult(B,mult(A,A))) = mult(rd(mult(mult(A,B),A),A),mult(A,A)),
inference(paramod,[status(thm)],[c_4,c_4272]) ).
cnf(c_4274,plain,
mult(A,mult(B,mult(A,A))) = mult(mult(A,B),mult(A,A)),
inference(paramod,[status(thm)],[c_4,c_4273]) ).
cnf(c_1741,plain,
mult(mult(A,B),mult(A,A)) = mult(A,mult(B,mult(A,A))),
inference(copy,[status(thm)],[c_4274]) ).
cnf(c_4275,plain,
rd(rd(A,i(mult(B,B))),B) = mult(rd(rd(rd(A,mult(B,B)),i(mult(B,B))),B),mult(B,B)),
inference(paramod,[status(thm)],[c_325,c_1724]) ).
cnf(c_4276,plain,
rd(rd(A,mult(i(B),i(B))),B) = mult(rd(rd(rd(A,mult(B,B)),i(mult(B,B))),B),mult(B,B)),
inference(paramod,[status(thm)],[c_454,c_4275]) ).
cnf(c_4277,plain,
rd(rd(A,mult(i(B),i(B))),B) = mult(rd(rd(rd(A,mult(B,B)),mult(i(B),i(B))),B),mult(B,B)),
inference(paramod,[status(thm)],[c_454,c_4276]) ).
cnf(c_1748,plain,
mult(rd(rd(rd(A,mult(B,B)),mult(i(B),i(B))),B),mult(B,B)) = rd(rd(A,mult(i(B),i(B))),B),
inference(copy,[status(thm)],[c_4277]) ).
cnf(c_1768,plain,
rd(mult(A,B),mult(B,B)) = mult(rd(A,mult(B,B)),B),
inference(paramod,[status(thm)],[c_293,c_4]) ).
cnf(c_4278,plain,
rd(A,mult(B,B)) = mult(rd(rd(A,B),mult(B,B)),B),
inference(paramod,[status(thm)],[c_3,c_1768]) ).
cnf(c_1781,plain,
mult(rd(rd(A,B),mult(B,B)),B) = rd(A,mult(B,B)),
inference(copy,[status(thm)],[c_4278]) ).
cnf(c_1867,plain,
rd(rd(A,mult(B,B)),B) = rd(rd(A,B),mult(B,B)),
inference(paramod,[status(thm)],[c_1781,c_4]) ).
cnf(c_4279,plain,
rd(rd(A,mult(i(B),i(B))),B) = mult(rd(rd(rd(A,i(B)),mult(i(B),i(B))),B),i(B)),
inference(paramod,[status(thm)],[c_1781,c_306]) ).
cnf(c_1879,plain,
mult(rd(rd(rd(A,i(B)),mult(i(B),i(B))),B),i(B)) = rd(rd(A,mult(i(B),i(B))),B),
inference(copy,[status(thm)],[c_4279]) ).
cnf(c_4280,plain,
rd(rd(rd(A,mult(B,B)),i(mult(B,B))),B) = rd(rd(rd(A,i(mult(B,B))),B),mult(B,B)),
inference(paramod,[status(thm)],[c_429,c_1867]) ).
cnf(c_4281,plain,
rd(rd(rd(A,mult(B,B)),mult(i(B),i(B))),B) = rd(rd(rd(A,i(mult(B,B))),B),mult(B,B)),
inference(paramod,[status(thm)],[c_454,c_4280]) ).
cnf(c_4282,plain,
rd(rd(rd(A,mult(B,B)),mult(i(B),i(B))),B) = rd(rd(rd(A,mult(i(B),i(B))),B),mult(B,B)),
inference(paramod,[status(thm)],[c_454,c_4281]) ).
cnf(c_1919,plain,
rd(rd(rd(A,mult(i(B),i(B))),B),mult(B,B)) = rd(rd(rd(A,mult(B,B)),mult(i(B),i(B))),B),
inference(copy,[status(thm)],[c_4282]) ).
cnf(c_4283,plain,
mult(ld(i(A),B),rd(B,ld(A,B))) = mult(rd(B,ld(A,B)),mult(B,rd(B,ld(A,B)))),
inference(paramod,[status(thm)],[c_14,c_897]) ).
cnf(c_4284,plain,
mult(ld(i(A),B),A) = mult(rd(B,ld(A,B)),mult(B,rd(B,ld(A,B)))),
inference(paramod,[status(thm)],[c_14,c_4283]) ).
cnf(c_4285,plain,
mult(ld(i(A),B),A) = mult(A,mult(B,rd(B,ld(A,B)))),
inference(paramod,[status(thm)],[c_14,c_4284]) ).
cnf(c_2093,plain,
mult(ld(i(A),B),A) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_14,c_4285]) ).
cnf(c_4286,plain,
mult(ld(i(A),mult(i(A),B)),rd(mult(i(A),B),mult(i(A),ld(A,B)))) = mult(rd(mult(i(A),B),mult(i(A),ld(A,B))),mult(mult(i(A),B),rd(mult(i(A),B),mult(i(A),ld(A,B))))),
inference(paramod,[status(thm)],[c_660,c_897]) ).
cnf(c_4287,plain,
mult(B,rd(mult(i(A),B),mult(i(A),ld(A,B)))) = mult(rd(mult(i(A),B),mult(i(A),ld(A,B))),mult(mult(i(A),B),rd(mult(i(A),B),mult(i(A),ld(A,B))))),
inference(paramod,[status(thm)],[c_2,c_4286]) ).
cnf(c_4288,plain,
mult(B,A) = mult(rd(mult(i(A),B),mult(i(A),ld(A,B))),mult(mult(i(A),B),rd(mult(i(A),B),mult(i(A),ld(A,B))))),
inference(paramod,[status(thm)],[c_660,c_4287]) ).
cnf(c_4289,plain,
mult(B,A) = mult(A,mult(mult(i(A),B),rd(mult(i(A),B),mult(i(A),ld(A,B))))),
inference(paramod,[status(thm)],[c_660,c_4288]) ).
cnf(c_4290,plain,
mult(B,A) = mult(A,mult(mult(i(A),B),A)),
inference(paramod,[status(thm)],[c_660,c_4289]) ).
cnf(c_2097,plain,
mult(A,mult(mult(i(A),B),A)) = mult(B,A),
inference(copy,[status(thm)],[c_4290]) ).
cnf(c_4291,plain,
mult(ld(i(i(A)),mult(A,B)),rd(mult(A,B),mult(A,ld(i(A),B)))) = mult(rd(mult(A,B),mult(A,ld(i(A),B))),mult(mult(A,B),rd(mult(A,B),mult(A,ld(i(A),B))))),
inference(paramod,[status(thm)],[c_721,c_897]) ).
cnf(c_4292,plain,
mult(ld(A,mult(A,B)),rd(mult(A,B),mult(A,ld(i(A),B)))) = mult(rd(mult(A,B),mult(A,ld(i(A),B))),mult(mult(A,B),rd(mult(A,B),mult(A,ld(i(A),B))))),
inference(paramod,[status(thm)],[c_45,c_4291]) ).
cnf(c_4293,plain,
mult(B,rd(mult(A,B),mult(A,ld(i(A),B)))) = mult(rd(mult(A,B),mult(A,ld(i(A),B))),mult(mult(A,B),rd(mult(A,B),mult(A,ld(i(A),B))))),
inference(paramod,[status(thm)],[c_2,c_4292]) ).
cnf(c_4294,plain,
mult(B,i(A)) = mult(rd(mult(A,B),mult(A,ld(i(A),B))),mult(mult(A,B),rd(mult(A,B),mult(A,ld(i(A),B))))),
inference(paramod,[status(thm)],[c_721,c_4293]) ).
cnf(c_4295,plain,
mult(B,i(A)) = mult(i(A),mult(mult(A,B),rd(mult(A,B),mult(A,ld(i(A),B))))),
inference(paramod,[status(thm)],[c_721,c_4294]) ).
cnf(c_4296,plain,
mult(B,i(A)) = mult(i(A),mult(mult(A,B),i(A))),
inference(paramod,[status(thm)],[c_721,c_4295]) ).
cnf(c_2098,plain,
mult(i(A),mult(mult(A,B),i(A))) = mult(B,i(A)),
inference(copy,[status(thm)],[c_4296]) ).
cnf(c_4297,plain,
mult(ld(i(i(rd(A,B))),A),rd(A,mult(rd(A,B),ld(i(rd(A,B)),B)))) = mult(rd(A,mult(rd(A,B),ld(i(rd(A,B)),B))),mult(A,rd(A,mult(rd(A,B),ld(i(rd(A,B)),B))))),
inference(paramod,[status(thm)],[c_772,c_897]) ).
cnf(c_4298,plain,
mult(ld(rd(A,B),A),rd(A,mult(rd(A,B),ld(i(rd(A,B)),B)))) = mult(rd(A,mult(rd(A,B),ld(i(rd(A,B)),B))),mult(A,rd(A,mult(rd(A,B),ld(i(rd(A,B)),B))))),
inference(paramod,[status(thm)],[c_45,c_4297]) ).
cnf(c_4299,plain,
mult(B,rd(A,mult(rd(A,B),ld(i(rd(A,B)),B)))) = mult(rd(A,mult(rd(A,B),ld(i(rd(A,B)),B))),mult(A,rd(A,mult(rd(A,B),ld(i(rd(A,B)),B))))),
inference(paramod,[status(thm)],[c_13,c_4298]) ).
cnf(c_4300,plain,
mult(B,i(rd(A,B))) = mult(rd(A,mult(rd(A,B),ld(i(rd(A,B)),B))),mult(A,rd(A,mult(rd(A,B),ld(i(rd(A,B)),B))))),
inference(paramod,[status(thm)],[c_772,c_4299]) ).
cnf(c_4301,plain,
mult(B,i(rd(A,B))) = mult(i(rd(A,B)),mult(A,rd(A,mult(rd(A,B),ld(i(rd(A,B)),B))))),
inference(paramod,[status(thm)],[c_772,c_4300]) ).
cnf(c_4302,plain,
mult(B,i(rd(A,B))) = mult(i(rd(A,B)),mult(A,i(rd(A,B)))),
inference(paramod,[status(thm)],[c_772,c_4301]) ).
cnf(c_2103,plain,
mult(i(rd(A,B)),mult(A,i(rd(A,B)))) = mult(B,i(rd(A,B))),
inference(copy,[status(thm)],[c_4302]) ).
cnf(c_2145,plain,
mult(i(A),mult(mult(mult(A,mult(B,A)),i(A)),i(A))) = mult(B,i(A)),
inference(paramod,[status(thm)],[c_2093,c_235]) ).
cnf(c_4303,plain,
rd(mult(A,mult(B,A)),A) = ld(i(A),B),
inference(paramod,[status(thm)],[c_2093,c_4]) ).
cnf(c_4304,plain,
mult(A,mult(A,mult(i(A),B))) = ld(i(A),B),
inference(paramod,[status(thm)],[c_374,c_4303]) ).
cnf(c_2167,plain,
ld(i(A),B) = mult(A,mult(A,mult(i(A),B))),
inference(copy,[status(thm)],[c_4304]) ).
cnf(c_2170,plain,
mult(ld(A,B),i(A)) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_45,c_2093]) ).
cnf(c_4305,plain,
mult(i(A),mult(mult(mult(ld(A,mult(A,mult(A,mult(i(A),B)))),A),i(A)),i(A))) = mult(ld(A,B),i(A)),
inference(paramod,[status(thm)],[c_2167,c_1052]) ).
cnf(c_4306,plain,
mult(i(A),mult(mult(mult(mult(A,mult(i(A),B)),A),i(A)),i(A))) = mult(ld(A,B),i(A)),
inference(paramod,[status(thm)],[c_2,c_4305]) ).
cnf(c_2227,plain,
mult(i(A),mult(mult(mult(mult(A,mult(i(A),B)),A),i(A)),i(A))) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_2170,c_4306]) ).
cnf(c_4307,plain,
mult(i(A),ld(A,mult(A,mult(A,mult(i(A),B))))) = ld(A,B),
inference(paramod,[status(thm)],[c_2167,c_698]) ).
cnf(c_4308,plain,
mult(i(A),mult(A,mult(i(A),B))) = ld(A,B),
inference(paramod,[status(thm)],[c_2,c_4307]) ).
cnf(c_4309,plain,
mult(A,mult(i(A),mult(i(A),B))) = ld(A,B),
inference(paramod,[status(thm)],[c_372,c_4308]) ).
cnf(c_2249,plain,
ld(A,B) = mult(A,mult(i(A),mult(i(A),B))),
inference(copy,[status(thm)],[c_4309]) ).
cnf(c_4310,plain,
mult(A,mult(i(A),mult(i(A),mult(A,B)))) = B,
inference(paramod,[status(thm)],[c_2249,c_2]) ).
cnf(c_4311,plain,
mult(A,mult(i(A),mult(A,mult(i(A),B)))) = B,
inference(paramod,[status(thm)],[c_372,c_4310]) ).
cnf(c_2284,plain,
mult(A,mult(A,mult(i(A),mult(i(A),B)))) = B,
inference(paramod,[status(thm)],[c_372,c_4311]) ).
cnf(c_2285,plain,
rd(mult(A,i(B)),mult(mult(B,A),i(B))) = i(B),
inference(paramod,[status(thm)],[c_2098,c_4]) ).
cnf(c_4312,plain,
mult(i(i(A)),mult(mult(B,i(A)),i(i(A)))) = mult(mult(mult(A,B),i(A)),i(i(A))),
inference(paramod,[status(thm)],[c_2098,c_2098]) ).
cnf(c_4313,plain,
mult(A,mult(mult(B,i(A)),i(i(A)))) = mult(mult(mult(A,B),i(A)),i(i(A))),
inference(paramod,[status(thm)],[c_45,c_4312]) ).
cnf(c_4314,plain,
mult(A,mult(mult(B,i(A)),A)) = mult(mult(mult(A,B),i(A)),i(i(A))),
inference(paramod,[status(thm)],[c_45,c_4313]) ).
cnf(c_4315,plain,
mult(A,mult(mult(B,A),i(A))) = mult(mult(mult(A,B),i(A)),i(i(A))),
inference(paramod,[status(thm)],[c_204,c_4314]) ).
cnf(c_4316,plain,
mult(A,mult(mult(B,A),i(A))) = mult(mult(mult(A,B),i(A)),A),
inference(paramod,[status(thm)],[c_45,c_4315]) ).
cnf(c_4317,plain,
mult(A,mult(mult(B,A),i(A))) = mult(mult(mult(A,B),A),i(A)),
inference(paramod,[status(thm)],[c_204,c_4316]) ).
cnf(c_2319,plain,
mult(mult(mult(A,B),A),i(A)) = mult(A,mult(mult(B,A),i(A))),
inference(copy,[status(thm)],[c_4317]) ).
cnf(c_4318,plain,
mult(i(A),mult(mult(A,mult(mult(mult(i(A),B),A),i(A))),i(A))) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_2319,c_2227]) ).
cnf(c_4319,plain,
mult(mult(mult(mult(i(A),B),A),i(A)),i(A)) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_2098,c_4318]) ).
cnf(c_2323,plain,
mult(mult(i(A),mult(mult(B,i(A)),i(A))),A) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_246,c_4319]) ).
cnf(c_4320,plain,
mult(i(A),mult(mult(A,mult(mult(B,A),i(A))),i(A))) = mult(mult(A,mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_2319,c_973]) ).
cnf(c_2324,plain,
mult(mult(mult(A,B),i(B)),i(B)) = mult(mult(B,mult(i(B),A)),i(B)),
inference(paramod,[status(thm)],[c_2098,c_4320]) ).
cnf(c_4321,plain,
mult(A,mult(mult(B,A),i(A))) = mult(A,mult(mult(mult(B,A),A),mult(i(A),i(A)))),
inference(paramod,[status(thm)],[c_2319,c_491]) ).
cnf(c_2325,plain,
mult(A,mult(mult(mult(B,A),A),mult(i(A),i(A)))) = mult(A,mult(mult(B,A),i(A))),
inference(copy,[status(thm)],[c_4321]) ).
cnf(c_2330,plain,
rd(mult(A,mult(mult(B,A),i(A))),i(A)) = mult(mult(A,B),A),
inference(paramod,[status(thm)],[c_2325,c_765]) ).
cnf(c_4322,plain,
mult(mult(A,mult(B,mult(A,C))),A) = mult(mult(A,mult(rd(B,A),A)),mult(A,mult(C,A))),
inference(paramod,[status(thm)],[c_3,c_129]) ).
cnf(c_2344,plain,
mult(mult(A,mult(B,mult(A,C))),A) = mult(mult(A,B),mult(A,mult(C,A))),
inference(paramod,[status(thm)],[c_3,c_4322]) ).
cnf(c_4323,plain,
mult(mult(i(A),mult(mult(B,i(A)),mult(i(A),mult(A,A)))),i(A)) = mult(mult(i(A),mult(B,i(A))),mult(i(A),A)),
inference(paramod,[status(thm)],[c_85,c_129]) ).
cnf(c_4324,plain,
mult(mult(i(A),mult(mult(B,i(A)),mult(A,mult(i(A),A)))),i(A)) = mult(mult(i(A),mult(B,i(A))),mult(i(A),A)),
inference(paramod,[status(thm)],[c_372,c_4323]) ).
cnf(c_4325,plain,
mult(mult(i(A),mult(mult(B,i(A)),mult(A,unit))),i(A)) = mult(mult(i(A),mult(B,i(A))),mult(i(A),A)),
inference(paramod,[status(thm)],[c_11,c_4324]) ).
cnf(c_4326,plain,
mult(mult(i(A),mult(mult(B,i(A)),A)),i(A)) = mult(mult(i(A),mult(B,i(A))),mult(i(A),A)),
inference(paramod,[status(thm)],[c_5,c_4325]) ).
cnf(c_4327,plain,
mult(mult(i(A),mult(mult(B,A),i(A))),i(A)) = mult(mult(i(A),mult(B,i(A))),mult(i(A),A)),
inference(paramod,[status(thm)],[c_204,c_4326]) ).
cnf(c_4328,plain,
mult(mult(i(A),mult(mult(B,A),i(A))),i(A)) = mult(mult(i(A),mult(B,i(A))),unit),
inference(paramod,[status(thm)],[c_11,c_4327]) ).
cnf(c_2347,plain,
mult(mult(i(A),mult(mult(B,A),i(A))),i(A)) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_5,c_4328]) ).
cnf(c_4329,plain,
rd(mult(A,B),mult(mult(i(B),A),i(i(B)))) = i(i(B)),
inference(paramod,[status(thm)],[c_45,c_2285]) ).
cnf(c_4330,plain,
rd(mult(A,B),mult(mult(i(B),A),B)) = i(i(B)),
inference(paramod,[status(thm)],[c_45,c_4329]) ).
cnf(c_2365,plain,
rd(mult(A,B),mult(mult(i(B),A),B)) = B,
inference(paramod,[status(thm)],[c_45,c_4330]) ).
cnf(c_4331,plain,
mult(i(A),mult(B,A)) = mult(rd(mult(B,A),mult(mult(i(A),B),A)),mult(i(rd(mult(B,A),mult(mult(i(A),B),A))),mult(mult(i(A),B),A))),
inference(paramod,[status(thm)],[c_2365,c_665]) ).
cnf(c_4332,plain,
mult(i(A),mult(B,A)) = mult(A,mult(i(rd(mult(B,A),mult(mult(i(A),B),A))),mult(mult(i(A),B),A))),
inference(paramod,[status(thm)],[c_2365,c_4331]) ).
cnf(c_4333,plain,
mult(i(A),mult(B,A)) = mult(A,mult(i(A),mult(mult(i(A),B),A))),
inference(paramod,[status(thm)],[c_2365,c_4332]) ).
cnf(c_2410,plain,
mult(A,mult(i(A),mult(mult(i(A),B),A))) = mult(i(A),mult(B,A)),
inference(copy,[status(thm)],[c_4333]) ).
cnf(c_4334,plain,
mult(i(A),mult(mult(B,A),i(A))) = mult(mult(mult(i(A),B),A),i(A)),
inference(paramod,[status(thm)],[c_2097,c_2098]) ).
cnf(c_2459,plain,
mult(mult(mult(i(A),B),A),i(A)) = mult(i(A),mult(mult(B,A),i(A))),
inference(copy,[status(thm)],[c_4334]) ).
cnf(c_2470,plain,
rd(mult(A,mult(mult(B,A),i(A))),A) = mult(A,rd(B,A)),
inference(paramod,[status(thm)],[c_130,c_4]) ).
cnf(c_4335,plain,
rd(mult(A,mult(mult(B,A),i(A))),i(A)) = mult(rd(mult(A,rd(B,A)),i(A)),A),
inference(paramod,[status(thm)],[c_130,c_318]) ).
cnf(c_4336,plain,
mult(mult(A,B),A) = mult(rd(mult(A,rd(B,A)),i(A)),A),
inference(paramod,[status(thm)],[c_2330,c_4335]) ).
cnf(c_2475,plain,
mult(rd(mult(A,rd(B,A)),i(A)),A) = mult(mult(A,B),A),
inference(copy,[status(thm)],[c_4336]) ).
cnf(c_2498,plain,
mult(mult(A,mult(mult(B,A),i(A))),i(A)) = mult(A,mult(mult(B,A),mult(i(A),i(A)))),
inference(paramod,[status(thm)],[c_492,c_133]) ).
cnf(c_4337,plain,
mult(mult(mult(i(A),i(A)),mult(A,i(mult(i(A),i(A))))),mult(mult(i(A),i(A)),B)) = mult(mult(i(A),i(A)),mult(mult(mult(A,mult(A,A)),mult(i(A),i(A))),B)),
inference(paramod,[status(thm)],[c_466,c_133]) ).
cnf(c_4338,plain,
mult(mult(mult(i(A),i(A)),mult(A,mult(i(i(A)),i(i(A))))),mult(mult(i(A),i(A)),B)) = mult(mult(i(A),i(A)),mult(mult(mult(A,mult(A,A)),mult(i(A),i(A))),B)),
inference(paramod,[status(thm)],[c_454,c_4337]) ).
cnf(c_4339,plain,
mult(mult(mult(i(A),i(A)),mult(A,mult(A,i(i(A))))),mult(mult(i(A),i(A)),B)) = mult(mult(i(A),i(A)),mult(mult(mult(A,mult(A,A)),mult(i(A),i(A))),B)),
inference(paramod,[status(thm)],[c_45,c_4338]) ).
cnf(c_4340,plain,
mult(mult(mult(i(A),i(A)),mult(A,mult(A,A))),mult(mult(i(A),i(A)),B)) = mult(mult(i(A),i(A)),mult(mult(mult(A,mult(A,A)),mult(i(A),i(A))),B)),
inference(paramod,[status(thm)],[c_45,c_4339]) ).
cnf(c_4341,plain,
mult(A,mult(mult(i(A),i(A)),B)) = mult(mult(i(A),i(A)),mult(mult(mult(A,mult(A,A)),mult(i(A),i(A))),B)),
inference(paramod,[status(thm)],[c_714,c_4340]) ).
cnf(c_4342,plain,
mult(A,mult(mult(i(A),i(A)),B)) = mult(mult(i(A),i(A)),mult(A,B)),
inference(paramod,[status(thm)],[c_466,c_4341]) ).
cnf(c_2503,plain,
mult(mult(i(A),i(A)),mult(A,B)) = mult(A,mult(mult(i(A),i(A)),B)),
inference(copy,[status(thm)],[c_4342]) ).
cnf(c_4343,plain,
rd(mult(A,mult(mult(B,A),A)),A) = mult(rd(mult(A,mult(mult(B,A),i(A))),A),mult(A,A)),
inference(paramod,[status(thm)],[c_133,c_1724]) ).
cnf(c_4344,plain,
mult(A,mult(A,mult(i(A),mult(B,A)))) = mult(rd(mult(A,mult(mult(B,A),i(A))),A),mult(A,A)),
inference(paramod,[status(thm)],[c_374,c_4343]) ).
cnf(c_4345,plain,
mult(A,mult(A,mult(i(A),mult(B,A)))) = mult(mult(A,rd(B,A)),mult(A,A)),
inference(paramod,[status(thm)],[c_2470,c_4344]) ).
cnf(c_4346,plain,
mult(A,mult(A,mult(i(A),mult(B,A)))) = mult(A,mult(rd(B,A),mult(A,A))),
inference(paramod,[status(thm)],[c_1741,c_4345]) ).
cnf(c_2504,plain,
mult(A,mult(rd(B,A),mult(A,A))) = mult(A,mult(A,mult(i(A),mult(B,A)))),
inference(copy,[status(thm)],[c_4346]) ).
cnf(c_4347,plain,
rd(mult(A,mult(B,C)),mult(A,C)) = mult(A,mult(mult(rd(B,A),A),i(A))),
inference(paramod,[status(thm)],[c_3,c_136]) ).
cnf(c_2515,plain,
rd(mult(A,mult(B,C)),mult(A,C)) = mult(A,mult(B,i(A))),
inference(paramod,[status(thm)],[c_3,c_4347]) ).
cnf(c_4348,plain,
rd(mult(mult(A,B),A),A) = rd(mult(A,rd(B,A)),i(A)),
inference(paramod,[status(thm)],[c_2475,c_4]) ).
cnf(c_4349,plain,
mult(A,B) = rd(mult(A,rd(B,A)),i(A)),
inference(paramod,[status(thm)],[c_4,c_4348]) ).
cnf(c_2538,plain,
rd(mult(A,rd(B,A)),i(A)) = mult(A,B),
inference(copy,[status(thm)],[c_4349]) ).
cnf(c_4350,plain,
mult(mult(A,B),i(A)) = mult(A,rd(B,A)),
inference(paramod,[status(thm)],[c_2538,c_3]) ).
cnf(c_2555,plain,
mult(A,rd(B,A)) = mult(mult(A,B),i(A)),
inference(copy,[status(thm)],[c_4350]) ).
cnf(c_2556,plain,
rd(mult(A,B),i(A)) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_4,c_2538]) ).
cnf(c_4351,plain,
rd(mult(A,mult(rd(B,A),mult(A,A))),i(A)) = mult(A,mult(B,mult(A,A))),
inference(paramod,[status(thm)],[c_1724,c_2538]) ).
cnf(c_4352,plain,
rd(mult(A,mult(A,mult(i(A),mult(B,A)))),i(A)) = mult(A,mult(B,mult(A,A))),
inference(paramod,[status(thm)],[c_2504,c_4351]) ).
cnf(c_4353,plain,
mult(A,mult(mult(A,mult(i(A),mult(B,A))),A)) = mult(A,mult(B,mult(A,A))),
inference(paramod,[status(thm)],[c_2556,c_4352]) ).
cnf(c_2561,plain,
mult(mult(A,mult(B,A)),A) = mult(A,mult(B,mult(A,A))),
inference(paramod,[status(thm)],[c_387,c_4353]) ).
cnf(c_4354,plain,
rd(mult(i(A),rd(mult(mult(A,B),i(A)),i(A))),i(i(A))) = mult(B,i(A)),
inference(paramod,[status(thm)],[c_2098,c_2538]) ).
cnf(c_4355,plain,
rd(mult(i(A),mult(A,B)),i(i(A))) = mult(B,i(A)),
inference(paramod,[status(thm)],[c_4,c_4354]) ).
cnf(c_4356,plain,
rd(mult(A,mult(i(A),B)),i(i(A))) = mult(B,i(A)),
inference(paramod,[status(thm)],[c_372,c_4355]) ).
cnf(c_2566,plain,
rd(mult(A,mult(i(A),B)),A) = mult(B,i(A)),
inference(paramod,[status(thm)],[c_45,c_4356]) ).
cnf(c_4357,plain,
mult(mult(i(A),mult(A,B)),i(A)) = mult(i(A),mult(mult(mult(A,rd(B,A)),i(A)),i(i(A)))),
inference(paramod,[status(thm)],[c_2538,c_130]) ).
cnf(c_4358,plain,
mult(mult(A,mult(i(A),B)),i(A)) = mult(i(A),mult(mult(mult(A,rd(B,A)),i(A)),i(i(A)))),
inference(paramod,[status(thm)],[c_372,c_4357]) ).
cnf(c_4359,plain,
mult(mult(A,mult(i(A),B)),i(A)) = mult(i(A),mult(mult(mult(mult(A,B),i(A)),i(A)),i(i(A)))),
inference(paramod,[status(thm)],[c_2555,c_4358]) ).
cnf(c_4360,plain,
mult(mult(A,mult(i(A),B)),i(A)) = mult(i(A),mult(mult(mult(mult(A,B),i(A)),i(A)),A)),
inference(paramod,[status(thm)],[c_45,c_4359]) ).
cnf(c_4361,plain,
mult(mult(A,mult(i(A),B)),i(A)) = mult(i(A),mult(mult(mult(mult(A,B),i(A)),A),i(A))),
inference(paramod,[status(thm)],[c_204,c_4360]) ).
cnf(c_4362,plain,
mult(mult(A,mult(i(A),B)),i(A)) = mult(i(A),mult(mult(mult(mult(A,B),A),i(A)),i(A))),
inference(paramod,[status(thm)],[c_204,c_4361]) ).
cnf(c_4363,plain,
mult(mult(A,mult(i(A),B)),i(A)) = mult(i(A),mult(mult(A,mult(mult(B,A),i(A))),i(A))),
inference(paramod,[status(thm)],[c_2319,c_4362]) ).
cnf(c_4364,plain,
mult(mult(A,mult(i(A),B)),i(A)) = mult(i(A),mult(A,mult(mult(B,A),mult(i(A),i(A))))),
inference(paramod,[status(thm)],[c_2498,c_4363]) ).
cnf(c_2568,plain,
mult(mult(A,mult(i(A),B)),i(A)) = mult(A,mult(i(A),mult(mult(B,A),mult(i(A),i(A))))),
inference(paramod,[status(thm)],[c_372,c_4364]) ).
cnf(c_2608,plain,
mult(i(A),mult(mult(B,A),mult(i(A),i(A)))) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_2561,c_2347]) ).
cnf(c_2622,plain,
mult(mult(A,mult(i(A),B)),i(A)) = mult(A,mult(i(A),mult(B,i(A)))),
inference(paramod,[status(thm)],[c_2608,c_2568]) ).
cnf(c_2648,plain,
mult(mult(mult(A,B),i(B)),i(B)) = mult(B,mult(i(B),mult(A,i(B)))),
inference(paramod,[status(thm)],[c_2622,c_2324]) ).
cnf(c_4365,plain,
mult(mult(A,mult(i(A),mult(B,i(A)))),i(A)) = mult(i(A),mult(mult(mult(A,B),i(A)),i(A))),
inference(paramod,[status(thm)],[c_2622,c_961]) ).
cnf(c_4366,plain,
mult(mult(A,i(A)),mult(B,mult(i(A),i(A)))) = mult(i(A),mult(mult(mult(A,B),i(A)),i(A))),
inference(paramod,[status(thm)],[c_627,c_4365]) ).
cnf(c_4367,plain,
mult(unit,mult(B,mult(i(A),i(A)))) = mult(i(A),mult(mult(mult(A,B),i(A)),i(A))),
inference(paramod,[status(thm)],[c_10,c_4366]) ).
cnf(c_4368,plain,
mult(B,mult(i(A),i(A))) = mult(i(A),mult(mult(mult(A,B),i(A)),i(A))),
inference(paramod,[status(thm)],[c_6,c_4367]) ).
cnf(c_2650,plain,
mult(i(A),mult(mult(mult(A,B),i(A)),i(A))) = mult(B,mult(i(A),i(A))),
inference(copy,[status(thm)],[c_4368]) ).
cnf(c_4369,plain,
mult(i(A),mult(A,mult(i(A),mult(B,i(A))))) = mult(mult(i(A),B),i(A)),
inference(paramod,[status(thm)],[c_2648,c_219]) ).
cnf(c_4370,plain,
mult(A,mult(i(A),mult(i(A),mult(B,i(A))))) = mult(mult(i(A),B),i(A)),
inference(paramod,[status(thm)],[c_372,c_4369]) ).
cnf(c_2671,plain,
mult(mult(i(A),B),i(A)) = mult(A,mult(i(A),mult(i(A),mult(B,i(A))))),
inference(copy,[status(thm)],[c_4370]) ).
cnf(c_2674,plain,
mult(mult(A,B),mult(i(B),i(B))) = mult(A,i(B)),
inference(paramod,[status(thm)],[c_2650,c_2145]) ).
cnf(c_4371,plain,
mult(A,B) = mult(mult(A,mult(B,A)),i(A)),
inference(paramod,[status(thm)],[c_4,c_2555]) ).
cnf(c_2682,plain,
mult(mult(A,mult(B,A)),i(A)) = mult(A,B),
inference(copy,[status(thm)],[c_4371]) ).
cnf(c_4372,plain,
mult(i(A),mult(mult(A,B),i(A))) = mult(A,mult(i(A),rd(B,A))),
inference(paramod,[status(thm)],[c_2555,c_372]) ).
cnf(c_4373,plain,
mult(B,i(A)) = mult(A,mult(i(A),rd(B,A))),
inference(paramod,[status(thm)],[c_2098,c_4372]) ).
cnf(c_2691,plain,
mult(A,mult(i(A),rd(B,A))) = mult(B,i(A)),
inference(copy,[status(thm)],[c_4373]) ).
cnf(c_4374,plain,
mult(i(A),rd(mult(A,B),i(A))) = mult(mult(A,mult(i(A),B)),i(i(A))),
inference(paramod,[status(thm)],[c_372,c_2555]) ).
cnf(c_4375,plain,
mult(i(A),mult(A,mult(B,A))) = mult(mult(A,mult(i(A),B)),i(i(A))),
inference(paramod,[status(thm)],[c_2556,c_4374]) ).
cnf(c_4376,plain,
mult(A,mult(i(A),mult(B,A))) = mult(mult(A,mult(i(A),B)),i(i(A))),
inference(paramod,[status(thm)],[c_372,c_4375]) ).
cnf(c_4377,plain,
mult(A,mult(i(A),mult(B,A))) = mult(mult(A,mult(i(A),B)),A),
inference(paramod,[status(thm)],[c_45,c_4376]) ).
cnf(c_2692,plain,
mult(mult(A,mult(i(A),B)),A) = mult(A,mult(i(A),mult(B,A))),
inference(copy,[status(thm)],[c_4377]) ).
cnf(c_4378,plain,
mult(i(A),mult(mult(mult(A,B),i(A)),i(A))) = mult(rd(B,A),i(A)),
inference(paramod,[status(thm)],[c_2555,c_2098]) ).
cnf(c_4379,plain,
mult(B,mult(i(A),i(A))) = mult(rd(B,A),i(A)),
inference(paramod,[status(thm)],[c_2650,c_4378]) ).
cnf(c_2701,plain,
mult(rd(A,B),i(B)) = mult(A,mult(i(B),i(B))),
inference(copy,[status(thm)],[c_4379]) ).
cnf(c_4380,plain,
mult(A,mult(mult(mult(i(A),B),i(i(A))),A)) = mult(rd(B,i(A)),A),
inference(paramod,[status(thm)],[c_2555,c_2097]) ).
cnf(c_4381,plain,
mult(A,mult(mult(mult(i(A),B),A),A)) = mult(rd(B,i(A)),A),
inference(paramod,[status(thm)],[c_45,c_4380]) ).
cnf(c_2709,plain,
mult(rd(A,i(B)),B) = mult(B,mult(mult(mult(i(B),A),B),B)),
inference(copy,[status(thm)],[c_4381]) ).
cnf(c_4382,plain,
mult(rd(rd(A,i(B)),mult(i(B),i(B))),mult(i(B),i(B))) = rd(rd(A,mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_2701,c_1879]) ).
cnf(c_4383,plain,
rd(A,i(B)) = rd(rd(A,mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_3,c_4382]) ).
cnf(c_2738,plain,
rd(rd(A,mult(i(B),i(B))),B) = rd(A,i(B)),
inference(copy,[status(thm)],[c_4383]) ).
cnf(c_2744,plain,
rd(mult(A,i(B)),B) = mult(A,mult(i(B),i(B))),
inference(paramod,[status(thm)],[c_2701,c_306]) ).
cnf(c_4384,plain,
mult(B,mult(mult(mult(i(B),rd(A,B)),B),B)) = rd(A,i(B)),
inference(paramod,[status(thm)],[c_2709,c_325]) ).
cnf(c_2756,plain,
rd(A,i(B)) = mult(B,mult(mult(mult(i(B),rd(A,B)),B),B)),
inference(copy,[status(thm)],[c_4384]) ).
cnf(c_4385,plain,
rd(rd(A,i(B)),mult(B,B)) = rd(rd(rd(A,mult(B,B)),mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_2738,c_1919]) ).
cnf(c_4386,plain,
rd(mult(B,mult(mult(mult(i(B),rd(A,B)),B),B)),mult(B,B)) = rd(rd(rd(A,mult(B,B)),mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_2756,c_4385]) ).
cnf(c_4387,plain,
mult(B,mult(mult(mult(i(B),rd(A,B)),B),i(B))) = rd(rd(rd(A,mult(B,B)),mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_2515,c_4386]) ).
cnf(c_4388,plain,
mult(B,mult(i(B),mult(mult(rd(A,B),B),i(B)))) = rd(rd(rd(A,mult(B,B)),mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_2459,c_4387]) ).
cnf(c_4389,plain,
mult(B,mult(i(B),mult(A,i(B)))) = rd(rd(rd(A,mult(B,B)),mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_3,c_4388]) ).
cnf(c_4390,plain,
mult(B,mult(i(B),mult(A,i(B)))) = rd(rd(A,mult(B,B)),i(B)),
inference(paramod,[status(thm)],[c_2738,c_4389]) ).
cnf(c_4391,plain,
mult(B,mult(i(B),mult(A,i(B)))) = mult(B,mult(mult(mult(i(B),rd(rd(A,mult(B,B)),B)),B),B)),
inference(paramod,[status(thm)],[c_2756,c_4390]) ).
cnf(c_4392,plain,
mult(B,mult(i(B),mult(A,i(B)))) = mult(B,mult(mult(mult(i(B),rd(rd(A,B),mult(B,B))),B),B)),
inference(paramod,[status(thm)],[c_1867,c_4391]) ).
cnf(c_2764,plain,
mult(A,mult(mult(mult(i(A),rd(rd(B,A),mult(A,A))),A),A)) = mult(A,mult(i(A),mult(B,i(A)))),
inference(copy,[status(thm)],[c_4392]) ).
cnf(c_4393,plain,
mult(rd(rd(A,mult(B,B)),i(B)),mult(B,B)) = rd(rd(A,mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_2738,c_1748]) ).
cnf(c_4394,plain,
mult(mult(B,mult(mult(mult(i(B),rd(rd(A,mult(B,B)),B)),B),B)),mult(B,B)) = rd(rd(A,mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_2756,c_4393]) ).
cnf(c_4395,plain,
mult(mult(B,mult(mult(mult(i(B),rd(rd(A,B),mult(B,B))),B),B)),mult(B,B)) = rd(rd(A,mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_1867,c_4394]) ).
cnf(c_4396,plain,
mult(mult(B,mult(i(B),mult(A,i(B)))),mult(B,B)) = rd(rd(A,mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_2764,c_4395]) ).
cnf(c_4397,plain,
mult(B,mult(mult(i(B),mult(A,i(B))),mult(B,B))) = rd(rd(A,mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_1741,c_4396]) ).
cnf(c_4398,plain,
mult(B,mult(mult(i(B),mult(A,i(B))),mult(B,B))) = rd(A,i(B)),
inference(paramod,[status(thm)],[c_2738,c_4397]) ).
cnf(c_4399,plain,
mult(B,mult(mult(i(B),mult(A,i(B))),mult(B,B))) = mult(B,mult(mult(mult(i(B),rd(A,B)),B),B)),
inference(paramod,[status(thm)],[c_2756,c_4398]) ).
cnf(c_2765,plain,
mult(A,mult(mult(mult(i(A),rd(B,A)),A),A)) = mult(A,mult(mult(i(A),mult(B,i(A))),mult(A,A))),
inference(copy,[status(thm)],[c_4399]) ).
cnf(c_4400,plain,
rd(rd(A,mult(i(B),i(B))),B) = mult(B,mult(mult(mult(i(B),rd(A,B)),B),B)),
inference(paramod,[status(thm)],[c_2756,c_2738]) ).
cnf(c_2766,plain,
rd(rd(A,mult(i(B),i(B))),B) = mult(B,mult(mult(i(B),mult(A,i(B))),mult(B,B))),
inference(paramod,[status(thm)],[c_2765,c_4400]) ).
cnf(c_4401,plain,
mult(mult(B,mult(mult(mult(i(B),rd(A,B)),B),B)),B) = mult(B,mult(mult(mult(i(B),A),B),B)),
inference(paramod,[status(thm)],[c_2756,c_2709]) ).
cnf(c_4402,plain,
mult(mult(B,mult(mult(i(B),mult(A,i(B))),mult(B,B))),B) = mult(B,mult(mult(mult(i(B),A),B),B)),
inference(paramod,[status(thm)],[c_2765,c_4401]) ).
cnf(c_4403,plain,
mult(mult(B,mult(i(B),mult(A,i(B)))),mult(B,mult(B,B))) = mult(B,mult(mult(mult(i(B),A),B),B)),
inference(paramod,[status(thm)],[c_2344,c_4402]) ).
cnf(c_2767,plain,
mult(A,mult(mult(mult(i(A),B),A),A)) = mult(mult(A,mult(i(A),mult(B,i(A)))),mult(A,mult(A,A))),
inference(copy,[status(thm)],[c_4403]) ).
cnf(c_4404,plain,
rd(A,i(B)) = mult(mult(B,mult(i(B),mult(rd(A,B),i(B)))),mult(B,mult(B,B))),
inference(paramod,[status(thm)],[c_2767,c_2756]) ).
cnf(c_2769,plain,
rd(A,i(B)) = mult(mult(B,mult(i(B),mult(A,mult(i(B),i(B))))),mult(B,mult(B,B))),
inference(paramod,[status(thm)],[c_2701,c_4404]) ).
cnf(c_2774,plain,
rd(mult(A,i(B)),mult(i(B),rd(A,B))) = B,
inference(paramod,[status(thm)],[c_2691,c_4]) ).
cnf(c_4405,plain,
mult(A,mult(i(A),rd(mult(mult(i(A),B),i(A)),A))) = mult(i(A),mult(mult(B,i(A)),i(A))),
inference(paramod,[status(thm)],[c_31,c_2691]) ).
cnf(c_4406,plain,
mult(A,mult(i(A),rd(mult(A,mult(i(A),mult(i(A),mult(B,i(A))))),A))) = mult(i(A),mult(mult(B,i(A)),i(A))),
inference(paramod,[status(thm)],[c_2671,c_4405]) ).
cnf(c_4407,plain,
mult(A,mult(i(A),mult(mult(i(A),mult(B,i(A))),i(A)))) = mult(i(A),mult(mult(B,i(A)),i(A))),
inference(paramod,[status(thm)],[c_2566,c_4406]) ).
cnf(c_4408,plain,
mult(A,mult(i(A),mult(i(A),mult(B,mult(i(A),i(A)))))) = mult(i(A),mult(mult(B,i(A)),i(A))),
inference(paramod,[status(thm)],[c_2561,c_4407]) ).
cnf(c_2782,plain,
mult(i(A),mult(mult(B,i(A)),i(A))) = mult(A,mult(i(A),mult(i(A),mult(B,mult(i(A),i(A)))))),
inference(copy,[status(thm)],[c_4408]) ).
cnf(c_4409,plain,
mult(mult(A,A),mult(mult(i(A),i(A)),rd(B,mult(A,A)))) = mult(B,i(mult(A,A))),
inference(paramod,[status(thm)],[c_454,c_2691]) ).
cnf(c_2785,plain,
mult(mult(A,A),mult(mult(i(A),i(A)),rd(B,mult(A,A)))) = mult(B,mult(i(A),i(A))),
inference(paramod,[status(thm)],[c_454,c_4409]) ).
cnf(c_4410,plain,
mult(mult(A,mult(i(A),mult(i(A),mult(B,mult(i(A),i(A)))))),A) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_2782,c_2323]) ).
cnf(c_4411,plain,
mult(A,mult(i(A),mult(mult(i(A),mult(B,mult(i(A),i(A)))),A))) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_2692,c_4410]) ).
cnf(c_2802,plain,
mult(i(A),mult(mult(B,mult(i(A),i(A))),A)) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_2410,c_4411]) ).
cnf(c_2805,plain,
rd(mult(mult(A,B),i(B)),mult(i(B),A)) = B,
inference(paramod,[status(thm)],[c_4,c_2774]) ).
cnf(c_4412,plain,
rd(mult(mult(A,i(B)),B),mult(i(i(B)),A)) = i(B),
inference(paramod,[status(thm)],[c_45,c_2805]) ).
cnf(c_4413,plain,
rd(mult(mult(A,B),i(B)),mult(i(i(B)),A)) = i(B),
inference(paramod,[status(thm)],[c_204,c_4412]) ).
cnf(c_2825,plain,
rd(mult(mult(A,B),i(B)),mult(B,A)) = i(B),
inference(paramod,[status(thm)],[c_45,c_4413]) ).
cnf(c_4414,plain,
rd(mult(mult(A,mult(B,B)),mult(i(B),i(B))),mult(mult(B,B),A)) = i(mult(B,B)),
inference(paramod,[status(thm)],[c_454,c_2825]) ).
cnf(c_2874,plain,
rd(mult(mult(A,mult(B,B)),mult(i(B),i(B))),mult(mult(B,B),A)) = mult(i(B),i(B)),
inference(paramod,[status(thm)],[c_454,c_4414]) ).
cnf(c_4415,plain,
mult(rd(rd(A,mult(i(B),i(B))),B),i(B)) = A,
inference(paramod,[status(thm)],[c_3,c_2701]) ).
cnf(c_2894,plain,
mult(mult(A,mult(mult(i(A),mult(B,i(A))),mult(A,A))),i(A)) = B,
inference(paramod,[status(thm)],[c_2766,c_4415]) ).
cnf(c_4416,plain,
mult(rd(A,i(B)),B) = mult(A,mult(i(i(B)),i(i(B)))),
inference(paramod,[status(thm)],[c_45,c_2701]) ).
cnf(c_4417,plain,
mult(mult(mult(B,mult(i(B),mult(A,mult(i(B),i(B))))),mult(B,mult(B,B))),B) = mult(A,mult(i(i(B)),i(i(B)))),
inference(paramod,[status(thm)],[c_2769,c_4416]) ).
cnf(c_4418,plain,
mult(mult(mult(B,mult(i(B),mult(A,mult(i(B),i(B))))),B),mult(B,mult(B,B))) = mult(A,mult(i(i(B)),i(i(B)))),
inference(paramod,[status(thm)],[c_9,c_4417]) ).
cnf(c_4419,plain,
mult(mult(B,mult(i(B),mult(mult(A,mult(i(B),i(B))),B))),mult(B,mult(B,B))) = mult(A,mult(i(i(B)),i(i(B)))),
inference(paramod,[status(thm)],[c_2692,c_4418]) ).
cnf(c_4420,plain,
mult(mult(B,mult(i(B),mult(A,i(B)))),mult(B,mult(B,B))) = mult(A,mult(i(i(B)),i(i(B)))),
inference(paramod,[status(thm)],[c_2802,c_4419]) ).
cnf(c_4421,plain,
mult(mult(B,mult(i(B),mult(A,i(B)))),mult(B,mult(B,B))) = mult(A,mult(B,i(i(B)))),
inference(paramod,[status(thm)],[c_45,c_4420]) ).
cnf(c_2897,plain,
mult(mult(A,mult(i(A),mult(B,i(A)))),mult(A,mult(A,A))) = mult(B,mult(A,A)),
inference(paramod,[status(thm)],[c_45,c_4421]) ).
cnf(c_4422,plain,
mult(mult(A,mult(i(B),i(B))),B) = mult(mult(rd(A,B),B),i(B)),
inference(paramod,[status(thm)],[c_2701,c_204]) ).
cnf(c_2902,plain,
mult(mult(A,mult(i(B),i(B))),B) = mult(A,i(B)),
inference(paramod,[status(thm)],[c_3,c_4422]) ).
cnf(c_4423,plain,
mult(rd(mult(A,i(mult(i(B),i(B)))),B),i(B)) = mult(mult(A,mult(i(B),i(B))),i(mult(i(B),i(B)))),
inference(paramod,[status(thm)],[c_204,c_2701]) ).
cnf(c_4424,plain,
mult(rd(mult(A,mult(i(i(B)),i(i(B)))),B),i(B)) = mult(mult(A,mult(i(B),i(B))),i(mult(i(B),i(B)))),
inference(paramod,[status(thm)],[c_454,c_4423]) ).
cnf(c_4425,plain,
mult(rd(mult(A,mult(B,i(i(B)))),B),i(B)) = mult(mult(A,mult(i(B),i(B))),i(mult(i(B),i(B)))),
inference(paramod,[status(thm)],[c_45,c_4424]) ).
cnf(c_4426,plain,
mult(rd(mult(A,mult(B,B)),B),i(B)) = mult(mult(A,mult(i(B),i(B))),i(mult(i(B),i(B)))),
inference(paramod,[status(thm)],[c_45,c_4425]) ).
cnf(c_4427,plain,
mult(mult(rd(A,B),mult(B,B)),i(B)) = mult(mult(A,mult(i(B),i(B))),i(mult(i(B),i(B)))),
inference(paramod,[status(thm)],[c_1724,c_4426]) ).
cnf(c_4428,plain,
mult(mult(rd(A,B),mult(B,B)),i(B)) = mult(mult(A,mult(i(B),i(B))),mult(i(i(B)),i(i(B)))),
inference(paramod,[status(thm)],[c_454,c_4427]) ).
cnf(c_4429,plain,
mult(mult(rd(A,B),mult(B,B)),i(B)) = mult(mult(A,mult(i(B),i(B))),mult(B,i(i(B)))),
inference(paramod,[status(thm)],[c_45,c_4428]) ).
cnf(c_4430,plain,
mult(mult(rd(A,B),mult(B,B)),i(B)) = mult(mult(A,mult(i(B),i(B))),mult(B,B)),
inference(paramod,[status(thm)],[c_45,c_4429]) ).
cnf(c_2903,plain,
mult(mult(rd(A,B),mult(B,B)),i(B)) = mult(mult(A,mult(B,B)),mult(i(B),i(B))),
inference(paramod,[status(thm)],[c_499,c_4430]) ).
cnf(c_2928,plain,
mult(A,mult(mult(mult(i(A),B),A),A)) = mult(B,mult(A,A)),
inference(paramod,[status(thm)],[c_2897,c_2767]) ).
cnf(c_4431,plain,
mult(mult(A,i(B)),mult(B,B)) = mult(mult(mult(A,mult(B,B)),mult(i(B),i(B))),B),
inference(paramod,[status(thm)],[c_2902,c_465]) ).
cnf(c_2931,plain,
mult(mult(A,i(B)),mult(B,B)) = mult(mult(A,mult(B,B)),i(B)),
inference(paramod,[status(thm)],[c_2902,c_4431]) ).
cnf(c_4432,plain,
mult(A,mult(i(A),mult(B,mult(i(A),i(A))))) = mult(mult(B,i(A)),i(A)),
inference(paramod,[status(thm)],[c_2744,c_2691]) ).
cnf(c_2941,plain,
mult(mult(A,i(B)),i(B)) = mult(B,mult(i(B),mult(A,mult(i(B),i(B))))),
inference(copy,[status(thm)],[c_4432]) ).
cnf(c_4433,plain,
mult(mult(A,B),A) = mult(mult(mult(A,mult(B,A)),A),i(A)),
inference(paramod,[status(thm)],[c_2682,c_204]) ).
cnf(c_4434,plain,
mult(mult(A,B),A) = mult(mult(A,mult(B,mult(A,A))),i(A)),
inference(paramod,[status(thm)],[c_2561,c_4433]) ).
cnf(c_2984,plain,
mult(mult(A,mult(B,mult(A,A))),i(A)) = mult(mult(A,B),A),
inference(copy,[status(thm)],[c_4434]) ).
cnf(c_4435,plain,
mult(mult(A,mult(mult(mult(i(A),B),A),A)),i(A)) = mult(B,A),
inference(paramod,[status(thm)],[c_2097,c_2682]) ).
cnf(c_3006,plain,
mult(mult(A,mult(B,B)),i(B)) = mult(A,B),
inference(paramod,[status(thm)],[c_2928,c_4435]) ).
cnf(c_3011,plain,
rd(mult(A,B),A) = mult(mult(A,mult(B,A)),mult(i(A),i(A))),
inference(paramod,[status(thm)],[c_2682,c_2744]) ).
cnf(c_4436,plain,
mult(mult(A,mult(i(A),mult(B,i(A)))),A) = B,
inference(paramod,[status(thm)],[c_2984,c_2894]) ).
cnf(c_4437,plain,
mult(A,mult(i(A),mult(mult(B,i(A)),A))) = B,
inference(paramod,[status(thm)],[c_2692,c_4436]) ).
cnf(c_3014,plain,
mult(A,mult(i(A),mult(mult(B,A),i(A)))) = B,
inference(paramod,[status(thm)],[c_204,c_4437]) ).
cnf(c_3016,plain,
mult(mult(A,i(B)),mult(B,B)) = mult(A,B),
inference(paramod,[status(thm)],[c_3006,c_2931]) ).
cnf(c_4438,plain,
mult(rd(A,B),B) = mult(mult(A,mult(B,B)),mult(i(B),i(B))),
inference(paramod,[status(thm)],[c_3006,c_2903]) ).
cnf(c_4439,plain,
A = mult(mult(A,mult(B,B)),mult(i(B),i(B))),
inference(paramod,[status(thm)],[c_3,c_4438]) ).
cnf(c_3018,plain,
mult(mult(A,mult(B,B)),mult(i(B),i(B))) = A,
inference(copy,[status(thm)],[c_4439]) ).
cnf(c_4440,plain,
mult(B,A) = mult(i(A),mult(mult(A,B),A)),
inference(paramod,[status(thm)],[c_3014,c_974]) ).
cnf(c_3034,plain,
mult(i(A),mult(mult(A,B),A)) = mult(B,A),
inference(copy,[status(thm)],[c_4440]) ).
cnf(c_3037,plain,
rd(A,mult(mult(B,B),A)) = mult(i(B),i(B)),
inference(paramod,[status(thm)],[c_3018,c_2874]) ).
cnf(c_3040,plain,
mult(mult(A,mult(i(B),i(B))),mult(B,B)) = A,
inference(paramod,[status(thm)],[c_3018,c_499]) ).
cnf(c_4441,plain,
mult(mult(i(A),i(A)),mult(mult(A,A),B)) = B,
inference(paramod,[status(thm)],[c_3037,c_3]) ).
cnf(c_3105,plain,
mult(mult(A,A),mult(mult(i(A),i(A)),B)) = B,
inference(paramod,[status(thm)],[c_972,c_4441]) ).
cnf(c_3117,plain,
rd(A,mult(B,B)) = mult(A,mult(i(B),i(B))),
inference(paramod,[status(thm)],[c_3105,c_2785]) ).
cnf(c_3118,plain,
mult(mult(i(A),i(A)),mult(mult(A,A),B)) = B,
inference(paramod,[status(thm)],[c_3105,c_972]) ).
cnf(c_4442,plain,
mult(mult(mult(A,i(B)),i(B)),mult(B,B)) = mult(mult(A,B),i(B)),
inference(paramod,[status(thm)],[c_204,c_3016]) ).
cnf(c_4443,plain,
mult(mult(B,mult(i(B),mult(A,mult(i(B),i(B))))),mult(B,B)) = mult(mult(A,B),i(B)),
inference(paramod,[status(thm)],[c_2941,c_4442]) ).
cnf(c_3189,plain,
mult(A,mult(mult(i(A),mult(B,mult(i(A),i(A)))),mult(A,A))) = mult(mult(B,A),i(A)),
inference(paramod,[status(thm)],[c_1741,c_4443]) ).
cnf(c_4444,plain,
mult(mult(i(A),mult(B,A)),i(A)) = mult(i(A),mult(i(A),mult(mult(mult(A,B),A),i(A)))),
inference(paramod,[status(thm)],[c_3034,c_39]) ).
cnf(c_4445,plain,
mult(A,mult(i(A),mult(i(A),mult(mult(B,A),i(A))))) = mult(i(A),mult(i(A),mult(mult(mult(A,B),A),i(A)))),
inference(paramod,[status(thm)],[c_2671,c_4444]) ).
cnf(c_4446,plain,
mult(A,mult(i(A),mult(i(A),mult(mult(B,A),i(A))))) = mult(i(A),mult(i(A),mult(A,mult(mult(B,A),i(A))))),
inference(paramod,[status(thm)],[c_2319,c_4445]) ).
cnf(c_4447,plain,
mult(A,mult(i(A),mult(i(A),mult(mult(B,A),i(A))))) = mult(i(A),mult(A,mult(i(A),mult(mult(B,A),i(A))))),
inference(paramod,[status(thm)],[c_372,c_4446]) ).
cnf(c_3206,plain,
mult(A,mult(i(A),mult(i(A),mult(mult(B,A),i(A))))) = mult(i(A),B),
inference(paramod,[status(thm)],[c_3014,c_4447]) ).
cnf(c_4448,plain,
mult(i(A),mult(mult(B,A),A)) = mult(mult(mult(i(A),B),A),A),
inference(paramod,[status(thm)],[c_2097,c_3034]) ).
cnf(c_3216,plain,
mult(mult(mult(i(A),B),A),A) = mult(i(A),mult(mult(B,A),A)),
inference(copy,[status(thm)],[c_4448]) ).
cnf(c_3233,plain,
mult(A,mult(i(A),mult(mult(B,A),A))) = mult(B,mult(A,A)),
inference(paramod,[status(thm)],[c_3216,c_2928]) ).
cnf(c_4449,plain,
rd(mult(A,i(B)),mult(i(B),mult(mult(mult(B,C),B),i(B)))) = mult(rd(A,mult(i(B),mult(C,B))),i(B)),
inference(paramod,[status(thm)],[c_3034,c_292]) ).
cnf(c_4450,plain,
rd(mult(A,i(B)),mult(i(B),mult(B,mult(mult(C,B),i(B))))) = mult(rd(A,mult(i(B),mult(C,B))),i(B)),
inference(paramod,[status(thm)],[c_2319,c_4449]) ).
cnf(c_4451,plain,
rd(mult(A,i(B)),mult(B,mult(i(B),mult(mult(C,B),i(B))))) = mult(rd(A,mult(i(B),mult(C,B))),i(B)),
inference(paramod,[status(thm)],[c_372,c_4450]) ).
cnf(c_3424,plain,
rd(mult(A,i(B)),C) = mult(rd(A,mult(i(B),mult(C,B))),i(B)),
inference(paramod,[status(thm)],[c_3014,c_4451]) ).
cnf(c_3509,plain,
rd(mult(A,B),mult(A,C)) = mult(A,mult(rd(B,C),i(A))),
inference(paramod,[status(thm)],[c_3,c_2515]) ).
cnf(c_4452,plain,
rd(mult(A,B),mult(A,unit)) = mult(A,mult(B,i(A))),
inference(paramod,[status(thm)],[c_5,c_2515]) ).
cnf(c_4453,plain,
rd(mult(A,B),A) = mult(A,mult(B,i(A))),
inference(paramod,[status(thm)],[c_5,c_4452]) ).
cnf(c_3512,plain,
mult(mult(A,mult(B,A)),mult(i(A),i(A))) = mult(A,mult(B,i(A))),
inference(paramod,[status(thm)],[c_3011,c_4453]) ).
cnf(c_4454,plain,
rd(mult(A,unit),mult(A,B)) = mult(A,mult(i(B),i(A))),
inference(paramod,[status(thm)],[c_11,c_2515]) ).
cnf(c_3514,plain,
rd(A,mult(A,B)) = mult(A,mult(i(B),i(A))),
inference(paramod,[status(thm)],[c_5,c_4454]) ).
cnf(c_3554,plain,
rd(mult(A,B),A) = mult(A,mult(B,i(A))),
inference(paramod,[status(thm)],[c_3512,c_3011]) ).
cnf(c_4455,plain,
rd(i(A),mult(A,mult(i(A),B))) = mult(i(A),mult(i(mult(A,B)),i(i(A)))),
inference(paramod,[status(thm)],[c_372,c_3514]) ).
cnf(c_3594,plain,
rd(i(A),mult(A,mult(i(A),B))) = mult(i(A),mult(i(mult(A,B)),A)),
inference(paramod,[status(thm)],[c_45,c_4455]) ).
cnf(c_3597,plain,
rd(A,mult(B,A)) = mult(A,mult(i(mult(mult(i(A),B),A)),i(A))),
inference(paramod,[status(thm)],[c_2097,c_3514]) ).
cnf(c_4456,plain,
rd(unit,mult(i(A),B)) = mult(i(A),mult(rd(A,B),i(i(A)))),
inference(paramod,[status(thm)],[c_11,c_3509]) ).
cnf(c_4457,plain,
i(mult(i(A),B)) = mult(i(A),mult(rd(A,B),i(i(A)))),
inference(paramod,[status(thm)],[c_46,c_4456]) ).
cnf(c_4458,plain,
i(mult(i(A),B)) = mult(i(A),mult(rd(A,B),A)),
inference(paramod,[status(thm)],[c_45,c_4457]) ).
cnf(c_3619,plain,
mult(i(A),mult(rd(A,B),A)) = i(mult(i(A),B)),
inference(copy,[status(thm)],[c_4458]) ).
cnf(c_4459,plain,
rd(i(A),mult(A,B)) = mult(A,mult(rd(mult(i(A),i(A)),B),i(A))),
inference(paramod,[status(thm)],[c_492,c_3509]) ).
cnf(c_4460,plain,
rd(i(A),mult(A,B)) = mult(A,mult(mult(rd(i(A),mult(i(A),mult(B,A))),i(A)),i(A))),
inference(paramod,[status(thm)],[c_3424,c_4459]) ).
cnf(c_4461,plain,
rd(i(A),mult(A,B)) = mult(A,mult(mult(mult(i(A),mult(i(mult(B,A)),i(i(A)))),i(A)),i(A))),
inference(paramod,[status(thm)],[c_3514,c_4460]) ).
cnf(c_4462,plain,
rd(i(A),mult(A,B)) = mult(A,mult(mult(mult(i(A),mult(i(mult(B,A)),A)),i(A)),i(A))),
inference(paramod,[status(thm)],[c_45,c_4461]) ).
cnf(c_4463,plain,
rd(i(A),mult(A,B)) = mult(A,mult(mult(A,mult(i(A),mult(i(A),mult(mult(i(mult(B,A)),A),i(A))))),i(A))),
inference(paramod,[status(thm)],[c_2671,c_4462]) ).
cnf(c_4464,plain,
rd(i(A),mult(A,B)) = mult(A,mult(mult(i(A),i(mult(B,A))),i(A))),
inference(paramod,[status(thm)],[c_3206,c_4463]) ).
cnf(c_4465,plain,
rd(i(A),mult(A,B)) = mult(A,mult(A,mult(i(A),mult(i(A),mult(i(mult(B,A)),i(A)))))),
inference(paramod,[status(thm)],[c_2671,c_4464]) ).
cnf(c_3627,plain,
rd(i(A),mult(A,B)) = mult(i(mult(B,A)),i(A)),
inference(paramod,[status(thm)],[c_2284,c_4465]) ).
cnf(c_3657,plain,
mult(i(mult(mult(i(A),B),A)),i(A)) = mult(i(A),mult(i(mult(A,B)),A)),
inference(paramod,[status(thm)],[c_3627,c_3594]) ).
cnf(c_3663,plain,
rd(A,mult(B,A)) = mult(A,mult(i(A),mult(i(mult(A,B)),A))),
inference(paramod,[status(thm)],[c_3657,c_3597]) ).
cnf(c_4466,plain,
rd(mult(i(A),mult(A,mult(B,A))),A) = mult(mult(i(A),i(A)),mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_112,c_359]) ).
cnf(c_4467,plain,
rd(mult(A,mult(i(A),mult(B,A))),A) = mult(mult(i(A),i(A)),mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_372,c_4466]) ).
cnf(c_4468,plain,
mult(A,mult(mult(i(A),mult(B,A)),i(A))) = mult(mult(i(A),i(A)),mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_3554,c_4467]) ).
cnf(c_4469,plain,
mult(A,mult(A,mult(i(A),mult(i(A),mult(mult(B,A),i(A)))))) = mult(mult(i(A),i(A)),mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_2671,c_4468]) ).
cnf(c_4470,plain,
mult(A,mult(i(A),B)) = mult(mult(i(A),i(A)),mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_3206,c_4469]) ).
cnf(c_4471,plain,
mult(A,mult(i(A),B)) = mult(A,mult(mult(i(A),i(A)),mult(A,B))),
inference(paramod,[status(thm)],[c_2503,c_4470]) ).
cnf(c_4472,plain,
mult(A,mult(i(A),B)) = mult(A,mult(A,mult(mult(i(A),i(A)),B))),
inference(paramod,[status(thm)],[c_2503,c_4471]) ).
cnf(c_3681,plain,
mult(A,mult(A,mult(mult(i(A),i(A)),B))) = mult(A,mult(i(A),B)),
inference(copy,[status(thm)],[c_4472]) ).
cnf(c_4473,plain,
mult(i(A),mult(mult(mult(mult(rd(A,B),A),i(A)),i(A)),i(i(A)))) = mult(i(mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_3619,c_43]) ).
cnf(c_4474,plain,
mult(i(A),mult(mult(A,mult(i(A),mult(mult(rd(A,B),A),mult(i(A),i(A))))),i(i(A)))) = mult(i(mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_2941,c_4473]) ).
cnf(c_4475,plain,
mult(i(A),mult(mult(A,mult(i(A),mult(rd(A,B),i(A)))),i(i(A)))) = mult(i(mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_2674,c_4474]) ).
cnf(c_4476,plain,
mult(i(A),mult(mult(A,mult(i(A),mult(rd(A,B),i(A)))),A)) = mult(i(mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_45,c_4475]) ).
cnf(c_4477,plain,
mult(i(A),mult(A,mult(i(A),mult(mult(rd(A,B),i(A)),A)))) = mult(i(mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_2692,c_4476]) ).
cnf(c_4478,plain,
mult(i(A),mult(A,mult(i(A),mult(mult(rd(A,B),A),i(A))))) = mult(i(mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_204,c_4477]) ).
cnf(c_3739,plain,
mult(i(A),rd(A,B)) = mult(i(mult(i(A),B)),i(A)),
inference(paramod,[status(thm)],[c_3014,c_4478]) ).
cnf(c_4479,plain,
mult(i(A),mult(mult(A,mult(i(B),i(B))),A)) = i(mult(i(A),mult(B,B))),
inference(paramod,[status(thm)],[c_3117,c_3619]) ).
cnf(c_4480,plain,
mult(mult(i(B),i(B)),A) = i(mult(i(A),mult(B,B))),
inference(paramod,[status(thm)],[c_3034,c_4479]) ).
cnf(c_3748,plain,
i(mult(i(A),mult(B,B))) = mult(mult(i(B),i(B)),A),
inference(copy,[status(thm)],[c_4480]) ).
cnf(c_4481,plain,
mult(i(A),mult(rd(A,mult(mult(A,B),A)),A)) = i(mult(B,A)),
inference(paramod,[status(thm)],[c_3034,c_3619]) ).
cnf(c_4482,plain,
mult(i(A),mult(mult(A,mult(i(A),mult(i(mult(A,mult(A,B))),A))),A)) = i(mult(B,A)),
inference(paramod,[status(thm)],[c_3663,c_4481]) ).
cnf(c_4483,plain,
mult(i(A),mult(A,mult(i(A),mult(mult(i(mult(A,mult(A,B))),A),A)))) = i(mult(B,A)),
inference(paramod,[status(thm)],[c_2692,c_4482]) ).
cnf(c_4484,plain,
mult(i(A),mult(i(mult(A,mult(A,B))),mult(A,A))) = i(mult(B,A)),
inference(paramod,[status(thm)],[c_3233,c_4483]) ).
cnf(c_3751,plain,
i(mult(A,B)) = mult(i(B),mult(i(mult(B,mult(B,A))),mult(B,B))),
inference(copy,[status(thm)],[c_4484]) ).
cnf(c_4485,plain,
mult(i(i(A)),mult(mult(i(mult(B,A)),i(A)),i(A))) = i(mult(i(i(A)),mult(A,B))),
inference(paramod,[status(thm)],[c_3627,c_3619]) ).
cnf(c_4486,plain,
mult(A,mult(mult(i(mult(B,A)),i(A)),i(A))) = i(mult(i(i(A)),mult(A,B))),
inference(paramod,[status(thm)],[c_45,c_4485]) ).
cnf(c_4487,plain,
mult(A,mult(A,mult(i(A),mult(i(mult(B,A)),mult(i(A),i(A)))))) = i(mult(i(i(A)),mult(A,B))),
inference(paramod,[status(thm)],[c_2941,c_4486]) ).
cnf(c_4488,plain,
mult(A,mult(A,mult(i(A),mult(i(mult(B,A)),mult(i(A),i(A)))))) = i(mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_45,c_4487]) ).
cnf(c_3763,plain,
i(mult(A,mult(A,B))) = mult(A,mult(A,mult(i(A),mult(i(mult(B,A)),mult(i(A),i(A)))))),
inference(copy,[status(thm)],[c_4488]) ).
cnf(c_4489,plain,
mult(A,rd(i(A),B)) = mult(i(mult(i(i(A)),B)),i(i(A))),
inference(paramod,[status(thm)],[c_45,c_3739]) ).
cnf(c_4490,plain,
mult(A,rd(i(A),B)) = mult(i(mult(A,B)),i(i(A))),
inference(paramod,[status(thm)],[c_45,c_4489]) ).
cnf(c_3819,plain,
mult(A,rd(i(A),B)) = mult(i(mult(A,B)),A),
inference(paramod,[status(thm)],[c_45,c_4490]) ).
cnf(c_4491,plain,
mult(mult(i(A),i(A)),rd(mult(A,A),B)) = mult(i(mult(i(mult(A,A)),B)),i(mult(A,A))),
inference(paramod,[status(thm)],[c_454,c_3739]) ).
cnf(c_4492,plain,
mult(mult(i(A),i(A)),rd(mult(A,A),B)) = mult(i(mult(mult(i(A),i(A)),B)),i(mult(A,A))),
inference(paramod,[status(thm)],[c_454,c_4491]) ).
cnf(c_3823,plain,
mult(mult(i(A),i(A)),rd(mult(A,A),B)) = mult(i(mult(mult(i(A),i(A)),B)),mult(i(A),i(A))),
inference(paramod,[status(thm)],[c_454,c_4492]) ).
cnf(c_3896,plain,
rd(mult(i(mult(A,B)),A),rd(i(A),B)) = A,
inference(paramod,[status(thm)],[c_3819,c_4]) ).
cnf(c_4493,plain,
rd(mult(i(mult(mult(A,A),B)),mult(A,A)),rd(mult(i(A),i(A)),B)) = mult(A,A),
inference(paramod,[status(thm)],[c_454,c_3896]) ).
cnf(c_4494,plain,
rd(mult(i(mult(mult(A,A),B)),mult(A,A)),mult(rd(i(A),mult(i(A),mult(B,A))),i(A))) = mult(A,A),
inference(paramod,[status(thm)],[c_3424,c_4493]) ).
cnf(c_4495,plain,
rd(mult(i(mult(mult(A,A),B)),mult(A,A)),mult(mult(i(A),mult(i(mult(B,A)),i(i(A)))),i(A))) = mult(A,A),
inference(paramod,[status(thm)],[c_3514,c_4494]) ).
cnf(c_4496,plain,
rd(mult(i(mult(mult(A,A),B)),mult(A,A)),mult(mult(i(A),mult(i(mult(B,A)),A)),i(A))) = mult(A,A),
inference(paramod,[status(thm)],[c_45,c_4495]) ).
cnf(c_4497,plain,
rd(mult(i(mult(mult(A,A),B)),mult(A,A)),mult(A,mult(i(A),mult(i(A),mult(mult(i(mult(B,A)),A),i(A)))))) = mult(A,A),
inference(paramod,[status(thm)],[c_2671,c_4496]) ).
cnf(c_3956,plain,
rd(mult(i(mult(mult(A,A),B)),mult(A,A)),mult(i(A),i(mult(B,A)))) = mult(A,A),
inference(paramod,[status(thm)],[c_3206,c_4497]) ).
cnf(c_3971,plain,
i(mult(mult(i(A),i(A)),B)) = mult(i(B),mult(A,A)),
inference(paramod,[status(thm)],[c_3748,c_45]) ).
cnf(c_4498,plain,
mult(mult(i(A),i(A)),rd(mult(A,A),B)) = mult(mult(i(B),mult(A,A)),mult(i(A),i(A))),
inference(paramod,[status(thm)],[c_3971,c_3823]) ).
cnf(c_3985,plain,
mult(mult(i(A),i(A)),rd(mult(A,A),B)) = i(B),
inference(paramod,[status(thm)],[c_3018,c_4498]) ).
cnf(c_4499,plain,
mult(mult(i(A),i(A)),mult(mult(A,A),mult(i(B),i(mult(A,A))))) = i(mult(mult(A,A),B)),
inference(paramod,[status(thm)],[c_3514,c_3985]) ).
cnf(c_4500,plain,
mult(mult(i(A),i(A)),mult(mult(A,A),mult(i(B),mult(i(A),i(A))))) = i(mult(mult(A,A),B)),
inference(paramod,[status(thm)],[c_454,c_4499]) ).
cnf(c_4501,plain,
mult(i(B),mult(i(A),i(A))) = i(mult(mult(A,A),B)),
inference(paramod,[status(thm)],[c_3118,c_4500]) ).
cnf(c_4012,plain,
i(mult(mult(A,A),B)) = mult(i(B),mult(i(A),i(A))),
inference(copy,[status(thm)],[c_4501]) ).
cnf(c_4502,plain,
rd(mult(mult(i(B),mult(i(A),i(A))),mult(A,A)),mult(i(A),i(mult(B,A)))) = mult(A,A),
inference(paramod,[status(thm)],[c_4012,c_3956]) ).
cnf(c_4021,plain,
rd(i(A),mult(i(B),i(mult(A,B)))) = mult(B,B),
inference(paramod,[status(thm)],[c_3040,c_4502]) ).
cnf(c_4503,plain,
mult(i(mult(A,A)),mult(i(B),i(rd(i(B),mult(i(A),i(mult(B,A))))))) = mult(mult(i(A),i(mult(B,A))),i(rd(i(B),mult(i(A),i(mult(B,A)))))),
inference(paramod,[status(thm)],[c_4021,c_2103]) ).
cnf(c_4504,plain,
mult(mult(i(A),i(A)),mult(i(B),i(rd(i(B),mult(i(A),i(mult(B,A))))))) = mult(mult(i(A),i(mult(B,A))),i(rd(i(B),mult(i(A),i(mult(B,A)))))),
inference(paramod,[status(thm)],[c_454,c_4503]) ).
cnf(c_4505,plain,
mult(mult(i(A),i(A)),mult(i(B),i(mult(A,A)))) = mult(mult(i(A),i(mult(B,A))),i(rd(i(B),mult(i(A),i(mult(B,A)))))),
inference(paramod,[status(thm)],[c_4021,c_4504]) ).
cnf(c_4506,plain,
mult(mult(i(A),i(A)),mult(i(B),mult(i(A),i(A)))) = mult(mult(i(A),i(mult(B,A))),i(rd(i(B),mult(i(A),i(mult(B,A)))))),
inference(paramod,[status(thm)],[c_454,c_4505]) ).
cnf(c_4507,plain,
mult(mult(i(A),i(A)),mult(i(B),mult(i(A),i(A)))) = mult(mult(i(A),i(mult(B,A))),i(mult(A,A))),
inference(paramod,[status(thm)],[c_4021,c_4506]) ).
cnf(c_4508,plain,
mult(mult(i(A),i(A)),mult(i(B),mult(i(A),i(A)))) = mult(mult(i(A),i(mult(B,A))),mult(i(A),i(A))),
inference(paramod,[status(thm)],[c_454,c_4507]) ).
cnf(c_4509,plain,
mult(mult(i(A),i(A)),mult(i(B),mult(i(A),i(A)))) = mult(i(A),mult(i(mult(B,A)),mult(i(A),i(A)))),
inference(paramod,[status(thm)],[c_1741,c_4508]) ).
cnf(c_4049,plain,
mult(i(A),mult(i(mult(B,A)),mult(i(A),i(A)))) = mult(mult(i(A),i(A)),mult(i(B),mult(i(A),i(A)))),
inference(copy,[status(thm)],[c_4509]) ).
cnf(c_4510,plain,
i(mult(A,mult(A,B))) = mult(A,mult(A,mult(mult(i(A),i(A)),mult(i(B),mult(i(A),i(A)))))),
inference(paramod,[status(thm)],[c_4049,c_3763]) ).
cnf(c_4069,plain,
i(mult(A,mult(A,B))) = mult(A,mult(i(A),mult(i(B),mult(i(A),i(A))))),
inference(paramod,[status(thm)],[c_3681,c_4510]) ).
cnf(c_4511,plain,
i(mult(A,B)) = mult(i(B),mult(mult(B,mult(i(B),mult(i(A),mult(i(B),i(B))))),mult(B,B))),
inference(paramod,[status(thm)],[c_4069,c_3751]) ).
cnf(c_4512,plain,
i(mult(A,B)) = mult(i(B),mult(B,mult(mult(i(B),mult(i(A),mult(i(B),i(B)))),mult(B,B)))),
inference(paramod,[status(thm)],[c_1741,c_4511]) ).
cnf(c_4084,plain,
i(mult(A,B)) = mult(i(B),mult(mult(i(A),B),i(B))),
inference(paramod,[status(thm)],[c_3189,c_4512]) ).
cnf(c_4513,plain,
mult(a,mult(i(a),mult(mult(i(b),a),i(a)))) != i(b),
inference(paramod,[status(thm)],[c_4084,c_12]) ).
cnf(c_4514,plain,
i(b) != i(b),
inference(paramod,[status(thm)],[c_3014,c_4513]) ).
cnf(c_4150,plain,
$false,
inference(copy,[status(thm)],[c_4514]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP701-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.10/0.37 % Computer : n013.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 15:38:11 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 750833 was started by sandbox2 on n013,
% 0.10/0.38 % Fri Sep 25 15:38:11 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 16.01/2.43
% 16.01/2.43 % SZS status Unsatisfiable for theBenchmark
% 16.01/2.43
% 16.01/2.43 % Proof 1 at 1.65 (+ 0.36) seconds.
% 16.01/2.43 % Length of proof is 245.
% 16.01/2.43 % Level of proof is 52.
% 16.01/2.43 % Maximum clause weight is 97.000.
% 16.01/2.43 % Given clauses 245.
% 16.01/2.43
% 16.01/2.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------