%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP688-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 : n004.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:12 AM UTC 2026
% Result : Unsatisfiable 43.95s 6.76s
% Output : CNFRefutation 43.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 114
% Number of leaves : 11
% Syntax : Number of formulae : 583 ( 583 unt; 0 def)
% Number of atoms : 583 ( 582 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 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 : 543 ( 0 sgn 15 !; 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(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(VAR_0,mult(VAR_1,mult(VAR_0,VAR_2))) = mult(mult(VAR_0,mult(VAR_1,VAR_0)),VAR_2),
file('theBenchmark.p',c07) ).
cnf(c_7,plain,
mult(A,mult(B,mult(A,C))) = mult(mult(A,mult(B,A)),C),
inference(clausify,[status(thm)],[c07]) ).
cnf(c_8,plain,
mult(mult(A,mult(B,A)),C) = mult(A,mult(B,mult(A,C))),
inference(copy,[status(thm)],[c_7]) ).
fof(c08,axiom,
! [VAR_0,VAR_1] : mult(i(VAR_0),mult(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',c08) ).
cnf(c_9,plain,
mult(i(A),mult(A,B)) = B,
inference(clausify,[status(thm)],[c08]) ).
fof(c09,axiom,
! [VAR_0,VAR_1] : i(mult(VAR_0,VAR_1)) = mult(i(VAR_0),i(VAR_1)),
file('theBenchmark.p',c09) ).
cnf(c_10,plain,
i(mult(A,B)) = mult(i(A),i(B)),
inference(clausify,[status(thm)],[c09]) ).
fof(c10,axiom,
mult(op_c,mult(op_c,mult(op_c,op_c))) = unit,
file('theBenchmark.p',c10) ).
cnf(c_11,plain,
mult(op_c,mult(op_c,mult(op_c,op_c))) = unit,
inference(clausify,[status(thm)],[c10]) ).
fof(c11,axiom,
mult(op_d,mult(op_d,op_d)) = unit,
file('theBenchmark.p',c11) ).
cnf(c_12,plain,
mult(op_d,mult(op_d,op_d)) = unit,
inference(clausify,[status(thm)],[c11]) ).
fof(goals,axiom,
mult(op_c,op_d) != mult(op_d,op_c),
file('theBenchmark.p',goals) ).
cnf(c_13,plain,
mult(op_c,op_d) != mult(op_d,op_c),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_14,plain,
mult(op_d,op_c) != mult(op_c,op_d),
inference(copy,[status(thm)],[c_13]) ).
cnf(c_16,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_20,plain,
rd(A,A) = unit,
inference(paramod,[status(thm)],[c_6,c_4]) ).
cnf(c_10921,plain,
mult(mult(A,B),C) = mult(A,mult(rd(B,A),mult(A,C))),
inference(paramod,[status(thm)],[c_3,c_8]) ).
cnf(c_24,plain,
mult(A,mult(rd(B,A),mult(A,C))) = mult(mult(A,B),C),
inference(copy,[status(thm)],[c_10921]) ).
cnf(c_25,plain,
rd(mult(A,mult(B,mult(A,C))),C) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_8,c_4]) ).
cnf(c_10922,plain,
mult(mult(A,A),B) = mult(A,mult(unit,mult(A,B))),
inference(paramod,[status(thm)],[c_6,c_8]) ).
cnf(c_26,plain,
mult(mult(A,A),B) = mult(A,mult(A,B)),
inference(paramod,[status(thm)],[c_6,c_10922]) ).
cnf(c_10923,plain,
mult(mult(A,mult(B,mult(C,mult(B,A)))),D) = mult(A,mult(mult(B,mult(C,B)),mult(A,D))),
inference(paramod,[status(thm)],[c_8,c_8]) ).
cnf(c_27,plain,
mult(mult(A,mult(B,mult(C,mult(B,A)))),D) = mult(A,mult(B,mult(C,mult(B,mult(A,D))))),
inference(paramod,[status(thm)],[c_8,c_10923]) ).
cnf(c_10924,plain,
mult(i(A),B) = ld(A,B),
inference(paramod,[status(thm)],[c_1,c_9]) ).
cnf(c_29,plain,
ld(A,B) = mult(i(A),B),
inference(copy,[status(thm)],[c_10924]) ).
cnf(c_32,plain,
rd(A,mult(B,A)) = i(B),
inference(paramod,[status(thm)],[c_9,c_4]) ).
cnf(c_33,plain,
mult(i(A),A) = unit,
inference(paramod,[status(thm)],[c_5,c_9]) ).
cnf(c_10925,plain,
rd(A,mult(i(B),A)) = B,
inference(paramod,[status(thm)],[c_29,c_16]) ).
cnf(c_38,plain,
i(i(A)) = A,
inference(paramod,[status(thm)],[c_32,c_10925]) ).
cnf(c_39,plain,
mult(A,mult(i(A),B)) = B,
inference(paramod,[status(thm)],[c_29,c_1]) ).
cnf(c_10926,plain,
i(A) = mult(i(rd(A,B)),i(B)),
inference(paramod,[status(thm)],[c_3,c_10]) ).
cnf(c_40,plain,
mult(i(rd(A,B)),i(B)) = i(A),
inference(copy,[status(thm)],[c_10926]) ).
cnf(c_10927,plain,
mult(i(op_c),unit) = mult(op_c,mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_11,c_9]) ).
cnf(c_10928,plain,
i(op_c) = mult(op_c,mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_5,c_10927]) ).
cnf(c_45,plain,
mult(op_c,mult(op_c,op_c)) = i(op_c),
inference(copy,[status(thm)],[c_10928]) ).
cnf(c_10929,plain,
i(unit) = mult(i(op_c),i(mult(op_c,mult(op_c,op_c)))),
inference(paramod,[status(thm)],[c_11,c_10]) ).
cnf(c_10930,plain,
i(unit) = mult(i(op_c),i(i(op_c))),
inference(paramod,[status(thm)],[c_45,c_10929]) ).
cnf(c_10931,plain,
i(unit) = mult(i(op_c),op_c),
inference(paramod,[status(thm)],[c_38,c_10930]) ).
cnf(c_46,plain,
i(unit) = unit,
inference(paramod,[status(thm)],[c_33,c_10931]) ).
cnf(c_10932,plain,
mult(i(op_d),unit) = mult(op_d,op_d),
inference(paramod,[status(thm)],[c_12,c_9]) ).
cnf(c_10933,plain,
i(op_d) = mult(op_d,op_d),
inference(paramod,[status(thm)],[c_5,c_10932]) ).
cnf(c_52,plain,
mult(op_d,op_d) = i(op_d),
inference(copy,[status(thm)],[c_10933]) ).
cnf(c_56,plain,
mult(i(op_d),i(op_d)) = op_d,
inference(paramod,[status(thm)],[c_52,c_9]) ).
cnf(c_10934,plain,
i(unit) = mult(i(i(A)),i(A)),
inference(paramod,[status(thm)],[c_33,c_10]) ).
cnf(c_10935,plain,
unit = mult(i(i(A)),i(A)),
inference(paramod,[status(thm)],[c_46,c_10934]) ).
cnf(c_10936,plain,
unit = mult(A,i(A)),
inference(paramod,[status(thm)],[c_38,c_10935]) ).
cnf(c_59,plain,
mult(A,i(A)) = unit,
inference(copy,[status(thm)],[c_10936]) ).
cnf(c_61,plain,
mult(rd(A,B),mult(rd(C,rd(A,B)),A)) = mult(mult(rd(A,B),C),B),
inference(paramod,[status(thm)],[c_3,c_24]) ).
cnf(c_10937,plain,
mult(i(A),mult(mult(A,B),C)) = mult(rd(B,A),mult(A,C)),
inference(paramod,[status(thm)],[c_24,c_9]) ).
cnf(c_65,plain,
mult(rd(A,B),mult(B,C)) = mult(i(B),mult(mult(B,A),C)),
inference(copy,[status(thm)],[c_10937]) ).
cnf(c_10938,plain,
mult(i(A),mult(rd(B,i(A)),C)) = mult(mult(i(A),B),mult(A,C)),
inference(paramod,[status(thm)],[c_9,c_24]) ).
cnf(c_66,plain,
mult(mult(i(A),B),mult(A,C)) = mult(i(A),mult(rd(B,i(A)),C)),
inference(copy,[status(thm)],[c_10938]) ).
cnf(c_67,plain,
mult(op_d,mult(rd(A,op_d),i(op_d))) = mult(mult(op_d,A),op_d),
inference(paramod,[status(thm)],[c_52,c_24]) ).
cnf(c_10939,plain,
mult(op_d,mult(rd(op_d,op_d),mult(op_d,A))) = mult(i(op_d),A),
inference(paramod,[status(thm)],[c_52,c_24]) ).
cnf(c_10940,plain,
mult(op_d,mult(unit,mult(op_d,A))) = mult(i(op_d),A),
inference(paramod,[status(thm)],[c_20,c_10939]) ).
cnf(c_68,plain,
mult(op_d,mult(op_d,A)) = mult(i(op_d),A),
inference(paramod,[status(thm)],[c_6,c_10940]) ).
cnf(c_10941,plain,
mult(i(A),mult(rd(B,i(A)),unit)) = mult(mult(i(A),B),A),
inference(paramod,[status(thm)],[c_33,c_24]) ).
cnf(c_10942,plain,
mult(i(A),rd(B,i(A))) = mult(mult(i(A),B),A),
inference(paramod,[status(thm)],[c_5,c_10941]) ).
cnf(c_69,plain,
mult(mult(i(A),B),A) = mult(i(A),rd(B,i(A))),
inference(copy,[status(thm)],[c_10942]) ).
cnf(c_10943,plain,
rd(A,B) = i(rd(B,A)),
inference(paramod,[status(thm)],[c_3,c_32]) ).
cnf(c_79,plain,
i(rd(A,B)) = rd(B,A),
inference(copy,[status(thm)],[c_10943]) ).
cnf(c_10944,plain,
rd(A,mult(B,mult(C,mult(B,A)))) = i(mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_8,c_32]) ).
cnf(c_10945,plain,
rd(A,mult(B,mult(C,mult(B,A)))) = mult(i(B),i(mult(C,B))),
inference(paramod,[status(thm)],[c_10,c_10944]) ).
cnf(c_80,plain,
rd(A,mult(B,mult(C,mult(B,A)))) = mult(i(B),mult(i(C),i(B))),
inference(paramod,[status(thm)],[c_10,c_10945]) ).
cnf(c_81,plain,
mult(rd(A,B),i(A)) = i(B),
inference(paramod,[status(thm)],[c_79,c_40]) ).
cnf(c_82,plain,
rd(mult(rd(A,B),mult(C,A)),B) = mult(rd(A,B),mult(C,rd(A,B))),
inference(paramod,[status(thm)],[c_3,c_25]) ).
cnf(c_10946,plain,
rd(mult(A,B),C) = mult(A,mult(rd(B,mult(A,C)),A)),
inference(paramod,[status(thm)],[c_3,c_25]) ).
cnf(c_83,plain,
mult(A,mult(rd(B,mult(A,C)),A)) = rd(mult(A,B),C),
inference(copy,[status(thm)],[c_10946]) ).
cnf(c_10947,plain,
rd(mult(A,mult(A,B)),B) = mult(A,mult(unit,A)),
inference(paramod,[status(thm)],[c_6,c_25]) ).
cnf(c_84,plain,
rd(mult(A,mult(A,B)),B) = mult(A,A),
inference(paramod,[status(thm)],[c_6,c_10947]) ).
cnf(c_88,plain,
rd(mult(op_d,mult(A,i(op_d))),op_d) = mult(op_d,mult(A,op_d)),
inference(paramod,[status(thm)],[c_52,c_25]) ).
cnf(c_10948,plain,
rd(mult(i(A),mult(B,unit)),A) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_33,c_25]) ).
cnf(c_89,plain,
rd(mult(i(A),B),A) = mult(i(A),mult(B,i(A))),
inference(paramod,[status(thm)],[c_5,c_10948]) ).
cnf(c_10949,plain,
rd(mult(A,unit),B) = mult(A,mult(i(mult(A,B)),A)),
inference(paramod,[status(thm)],[c_33,c_25]) ).
cnf(c_10950,plain,
rd(A,B) = mult(A,mult(i(mult(A,B)),A)),
inference(paramod,[status(thm)],[c_5,c_10949]) ).
cnf(c_10951,plain,
rd(A,B) = mult(A,mult(mult(i(A),i(B)),A)),
inference(paramod,[status(thm)],[c_10,c_10950]) ).
cnf(c_10952,plain,
rd(A,B) = mult(A,mult(i(A),rd(i(B),i(A)))),
inference(paramod,[status(thm)],[c_69,c_10951]) ).
cnf(c_10953,plain,
rd(A,B) = rd(i(B),i(A)),
inference(paramod,[status(thm)],[c_39,c_10952]) ).
cnf(c_90,plain,
rd(i(A),i(B)) = rd(B,A),
inference(copy,[status(thm)],[c_10953]) ).
cnf(c_10954,plain,
rd(mult(A,mult(B,unit)),i(A)) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_59,c_25]) ).
cnf(c_91,plain,
rd(mult(A,B),i(A)) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_5,c_10954]) ).
cnf(c_94,plain,
mult(rd(A,B),rd(B,A)) = unit,
inference(paramod,[status(thm)],[c_79,c_33]) ).
cnf(c_97,plain,
mult(rd(i(A),B),A) = i(B),
inference(paramod,[status(thm)],[c_38,c_81]) ).
cnf(c_100,plain,
rd(mult(i(A),i(B)),i(C)) = rd(C,mult(A,B)),
inference(paramod,[status(thm)],[c_10,c_90]) ).
cnf(c_101,plain,
rd(i(A),mult(i(B),i(C))) = rd(mult(B,C),A),
inference(paramod,[status(thm)],[c_10,c_90]) ).
cnf(c_102,plain,
rd(A,i(B)) = rd(B,i(A)),
inference(paramod,[status(thm)],[c_38,c_90]) ).
cnf(c_104,plain,
rd(rd(A,B),i(C)) = rd(C,rd(B,A)),
inference(paramod,[status(thm)],[c_79,c_90]) ).
cnf(c_10955,plain,
rd(A,i(mult(A,B))) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_102,c_91]) ).
cnf(c_108,plain,
rd(A,mult(i(A),i(B))) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_10,c_10955]) ).
cnf(c_10956,plain,
rd(mult(rd(A,B),mult(C,unit)),rd(B,A)) = mult(rd(A,B),mult(C,rd(A,B))),
inference(paramod,[status(thm)],[c_94,c_25]) ).
cnf(c_109,plain,
rd(mult(rd(A,B),C),rd(B,A)) = mult(rd(A,B),mult(C,rd(A,B))),
inference(paramod,[status(thm)],[c_5,c_10956]) ).
cnf(c_10957,plain,
mult(mult(A,mult(B,mult(B,A))),C) = mult(A,mult(mult(B,B),mult(A,C))),
inference(paramod,[status(thm)],[c_26,c_8]) ).
cnf(c_116,plain,
mult(mult(A,mult(B,mult(B,A))),C) = mult(A,mult(B,mult(B,mult(A,C)))),
inference(paramod,[status(thm)],[c_26,c_10957]) ).
cnf(c_10958,plain,
mult(op_d,A) = mult(i(op_d),mult(i(op_d),A)),
inference(paramod,[status(thm)],[c_56,c_26]) ).
cnf(c_118,plain,
mult(i(op_d),mult(i(op_d),A)) = mult(op_d,A),
inference(copy,[status(thm)],[c_10958]) ).
cnf(c_10959,plain,
rd(A,mult(B,mult(B,A))) = i(mult(B,B)),
inference(paramod,[status(thm)],[c_26,c_32]) ).
cnf(c_119,plain,
rd(A,mult(B,mult(B,A))) = mult(i(B),i(B)),
inference(paramod,[status(thm)],[c_10,c_10959]) ).
cnf(c_10960,plain,
rd(mult(A,mult(B,mult(B,mult(A,C)))),C) = mult(A,mult(mult(B,B),A)),
inference(paramod,[status(thm)],[c_26,c_25]) ).
cnf(c_120,plain,
rd(mult(A,mult(B,mult(B,mult(A,C)))),C) = mult(A,mult(B,mult(B,A))),
inference(paramod,[status(thm)],[c_26,c_10960]) ).
cnf(c_121,plain,
rd(i(op_c),mult(op_c,op_c)) = op_c,
inference(paramod,[status(thm)],[c_45,c_4]) ).
cnf(c_10961,plain,
mult(i(op_c),A) = mult(op_c,mult(op_c,mult(op_c,A))),
inference(paramod,[status(thm)],[c_45,c_8]) ).
cnf(c_123,plain,
mult(op_c,mult(op_c,mult(op_c,A))) = mult(i(op_c),A),
inference(copy,[status(thm)],[c_10961]) ).
cnf(c_124,plain,
mult(i(op_c),i(op_c)) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_45,c_9]) ).
cnf(c_10962,plain,
mult(mult(op_c,op_c),A) = mult(i(op_c),mult(i(op_c),A)),
inference(paramod,[status(thm)],[c_124,c_26]) ).
cnf(c_10963,plain,
mult(op_c,mult(op_c,A)) = mult(i(op_c),mult(i(op_c),A)),
inference(paramod,[status(thm)],[c_26,c_10962]) ).
cnf(c_127,plain,
mult(i(op_c),mult(i(op_c),A)) = mult(op_c,mult(op_c,A)),
inference(copy,[status(thm)],[c_10963]) ).
cnf(c_10964,plain,
mult(mult(A,mult(B,mult(C,mult(C,mult(B,A))))),D) = mult(A,mult(B,mult(mult(C,C),mult(B,mult(A,D))))),
inference(paramod,[status(thm)],[c_26,c_27]) ).
cnf(c_147,plain,
mult(mult(A,mult(B,mult(C,mult(C,mult(B,A))))),D) = mult(A,mult(B,mult(C,mult(C,mult(B,mult(A,D)))))),
inference(paramod,[status(thm)],[c_26,c_10964]) ).
cnf(c_10965,plain,
mult(mult(mult(op_d,A),mult(op_d,mult(B,mult(i(op_d),A)))),C) = mult(mult(op_d,A),mult(op_d,mult(B,mult(op_d,mult(mult(op_d,A),C))))),
inference(paramod,[status(thm)],[c_68,c_27]) ).
cnf(c_148,plain,
mult(mult(op_d,A),mult(op_d,mult(B,mult(op_d,mult(mult(op_d,A),C))))) = mult(mult(mult(op_d,A),mult(op_d,mult(B,mult(i(op_d),A)))),C),
inference(copy,[status(thm)],[c_10965]) ).
cnf(c_10966,plain,
mult(mult(A,mult(B,i(C))),D) = mult(A,mult(B,mult(rd(i(mult(B,A)),C),mult(B,mult(A,D))))),
inference(paramod,[status(thm)],[c_97,c_27]) ).
cnf(c_10967,plain,
mult(mult(A,mult(B,i(C))),D) = mult(A,mult(B,mult(rd(mult(i(B),i(A)),C),mult(B,mult(A,D))))),
inference(paramod,[status(thm)],[c_10,c_10966]) ).
cnf(c_150,plain,
mult(A,mult(B,mult(rd(mult(i(B),i(A)),C),mult(B,mult(A,D))))) = mult(mult(A,mult(B,i(C))),D),
inference(copy,[status(thm)],[c_10967]) ).
cnf(c_153,plain,
rd(rd(A,B),mult(i(C),i(D))) = rd(mult(C,D),rd(B,A)),
inference(paramod,[status(thm)],[c_10,c_104]) ).
cnf(c_212,plain,
rd(mult(i(A),B),mult(A,B)) = mult(i(A),i(A)),
inference(paramod,[status(thm)],[c_9,c_84]) ).
cnf(c_10968,plain,
rd(mult(i(A),unit),A) = mult(i(A),i(A)),
inference(paramod,[status(thm)],[c_33,c_84]) ).
cnf(c_213,plain,
rd(i(A),A) = mult(i(A),i(A)),
inference(paramod,[status(thm)],[c_5,c_10968]) ).
cnf(c_10969,plain,
rd(mult(A,unit),i(A)) = mult(A,A),
inference(paramod,[status(thm)],[c_59,c_84]) ).
cnf(c_214,plain,
rd(A,i(A)) = mult(A,A),
inference(paramod,[status(thm)],[c_5,c_10969]) ).
cnf(c_218,plain,
rd(mult(A,B),mult(i(A),B)) = mult(A,A),
inference(paramod,[status(thm)],[c_39,c_84]) ).
cnf(c_10970,plain,
rd(i(A),mult(i(rd(B,A)),i(B))) = mult(rd(B,A),rd(B,A)),
inference(paramod,[status(thm)],[c_81,c_218]) ).
cnf(c_230,plain,
rd(i(A),mult(rd(A,B),i(B))) = mult(rd(B,A),rd(B,A)),
inference(paramod,[status(thm)],[c_79,c_10970]) ).
cnf(c_10971,plain,
mult(op_c,mult(rd(A,rd(i(op_c),mult(op_c,op_c))),i(op_c))) = mult(mult(rd(i(op_c),mult(op_c,op_c)),A),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_121,c_61]) ).
cnf(c_10972,plain,
mult(op_c,mult(rd(A,op_c),i(op_c))) = mult(mult(rd(i(op_c),mult(op_c,op_c)),A),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_121,c_10971]) ).
cnf(c_10973,plain,
mult(op_c,mult(rd(A,op_c),i(op_c))) = mult(mult(op_c,A),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_121,c_10972]) ).
cnf(c_259,plain,
mult(mult(op_c,A),mult(op_c,op_c)) = mult(op_c,mult(rd(A,op_c),i(op_c))),
inference(copy,[status(thm)],[c_10973]) ).
cnf(c_319,plain,
rd(mult(op_c,op_c),i(A)) = rd(A,mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_124,c_100]) ).
cnf(c_10974,plain,
rd(mult(op_c,op_c),A) = rd(i(A),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_38,c_319]) ).
cnf(c_346,plain,
rd(i(A),mult(op_c,op_c)) = rd(mult(op_c,op_c),A),
inference(copy,[status(thm)],[c_10974]) ).
cnf(c_10975,plain,
rd(mult(op_c,op_c),rd(A,B)) = rd(rd(B,A),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_79,c_319]) ).
cnf(c_347,plain,
rd(rd(A,B),mult(op_c,op_c)) = rd(mult(op_c,op_c),rd(B,A)),
inference(copy,[status(thm)],[c_10975]) ).
cnf(c_374,plain,
mult(rd(mult(op_c,op_c),A),mult(op_c,op_c)) = i(A),
inference(paramod,[status(thm)],[c_346,c_3]) ).
cnf(c_10976,plain,
mult(mult(i(A),mult(mult(A,B),rd(B,A))),C) = mult(rd(B,A),mult(A,mult(rd(B,A),C))),
inference(paramod,[status(thm)],[c_65,c_8]) ).
cnf(c_585,plain,
mult(mult(i(A),mult(mult(A,B),rd(B,A))),C) = mult(i(A),mult(mult(A,B),mult(rd(B,A),C))),
inference(paramod,[status(thm)],[c_65,c_10976]) ).
cnf(c_10977,plain,
mult(rd(A,B),mult(i(A),C)) = mult(i(i(A)),mult(mult(i(A),i(B)),C)),
inference(paramod,[status(thm)],[c_90,c_65]) ).
cnf(c_596,plain,
mult(rd(A,B),mult(i(A),C)) = mult(A,mult(mult(i(A),i(B)),C)),
inference(paramod,[status(thm)],[c_38,c_10977]) ).
cnf(c_10978,plain,
mult(mult(A,B),mult(i(A),C)) = mult(i(i(A)),mult(rd(B,i(i(A))),C)),
inference(paramod,[status(thm)],[c_38,c_66]) ).
cnf(c_10979,plain,
mult(mult(A,B),mult(i(A),C)) = mult(A,mult(rd(B,i(i(A))),C)),
inference(paramod,[status(thm)],[c_38,c_10978]) ).
cnf(c_827,plain,
mult(mult(A,B),mult(i(A),C)) = mult(A,mult(rd(B,A),C)),
inference(paramod,[status(thm)],[c_38,c_10979]) ).
cnf(c_10980,plain,
rd(mult(i(rd(mult(op_c,op_c),A)),mult(op_c,op_c)),i(A)) = mult(i(rd(mult(op_c,op_c),A)),i(rd(mult(op_c,op_c),A))),
inference(paramod,[status(thm)],[c_374,c_212]) ).
cnf(c_10981,plain,
rd(mult(rd(A,mult(op_c,op_c)),mult(op_c,op_c)),i(A)) = mult(i(rd(mult(op_c,op_c),A)),i(rd(mult(op_c,op_c),A))),
inference(paramod,[status(thm)],[c_79,c_10980]) ).
cnf(c_10982,plain,
rd(A,i(A)) = mult(i(rd(mult(op_c,op_c),A)),i(rd(mult(op_c,op_c),A))),
inference(paramod,[status(thm)],[c_3,c_10981]) ).
cnf(c_10983,plain,
mult(A,A) = mult(i(rd(mult(op_c,op_c),A)),i(rd(mult(op_c,op_c),A))),
inference(paramod,[status(thm)],[c_214,c_10982]) ).
cnf(c_10984,plain,
mult(A,A) = mult(rd(A,mult(op_c,op_c)),i(rd(mult(op_c,op_c),A))),
inference(paramod,[status(thm)],[c_79,c_10983]) ).
cnf(c_10985,plain,
mult(A,A) = mult(rd(A,mult(op_c,op_c)),rd(A,mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_79,c_10984]) ).
cnf(c_891,plain,
mult(rd(A,mult(op_c,op_c)),rd(A,mult(op_c,op_c))) = mult(A,A),
inference(copy,[status(thm)],[c_10985]) ).
cnf(c_947,plain,
rd(mult(mult(op_d,A),op_d),mult(rd(A,op_d),i(op_d))) = op_d,
inference(paramod,[status(thm)],[c_67,c_4]) ).
cnf(c_951,plain,
rd(mult(rd(A,op_d),i(op_d)),mult(mult(op_d,A),op_d)) = i(op_d),
inference(paramod,[status(thm)],[c_67,c_32]) ).
cnf(c_968,plain,
rd(A,mult(i(A),B)) = mult(A,mult(i(B),A)),
inference(paramod,[status(thm)],[c_38,c_108]) ).
cnf(c_10986,plain,
rd(i(A),mult(i(i(A)),i(rd(A,B)))) = mult(i(A),i(B)),
inference(paramod,[status(thm)],[c_81,c_108]) ).
cnf(c_10987,plain,
rd(i(A),mult(A,i(rd(A,B)))) = mult(i(A),i(B)),
inference(paramod,[status(thm)],[c_38,c_10986]) ).
cnf(c_970,plain,
rd(i(A),mult(A,rd(B,A))) = mult(i(A),i(B)),
inference(paramod,[status(thm)],[c_79,c_10987]) ).
cnf(c_10988,plain,
rd(rd(A,B),mult(i(rd(A,B)),i(B))) = mult(i(B),mult(mult(B,A),rd(A,B))),
inference(paramod,[status(thm)],[c_65,c_108]) ).
cnf(c_10989,plain,
rd(rd(A,B),mult(rd(B,A),i(B))) = mult(i(B),mult(mult(B,A),rd(A,B))),
inference(paramod,[status(thm)],[c_79,c_10988]) ).
cnf(c_10990,plain,
rd(rd(A,B),i(A)) = mult(i(B),mult(mult(B,A),rd(A,B))),
inference(paramod,[status(thm)],[c_81,c_10989]) ).
cnf(c_10991,plain,
rd(A,i(rd(A,B))) = mult(i(B),mult(mult(B,A),rd(A,B))),
inference(paramod,[status(thm)],[c_102,c_10990]) ).
cnf(c_10992,plain,
rd(A,rd(B,A)) = mult(i(B),mult(mult(B,A),rd(A,B))),
inference(paramod,[status(thm)],[c_79,c_10991]) ).
cnf(c_985,plain,
mult(i(A),mult(mult(A,B),rd(B,A))) = rd(B,rd(A,B)),
inference(copy,[status(thm)],[c_10992]) ).
cnf(c_10993,plain,
mult(rd(B,rd(A,B)),C) = mult(i(A),mult(mult(A,B),mult(rd(B,A),C))),
inference(paramod,[status(thm)],[c_985,c_585]) ).
cnf(c_994,plain,
mult(i(A),mult(mult(A,B),mult(rd(B,A),C))) = mult(rd(B,rd(A,B)),C),
inference(copy,[status(thm)],[c_10993]) ).
cnf(c_10994,plain,
rd(i(A),mult(A,B)) = mult(i(A),i(mult(B,A))),
inference(paramod,[status(thm)],[c_4,c_970]) ).
cnf(c_995,plain,
rd(i(A),mult(A,B)) = mult(i(A),mult(i(B),i(A))),
inference(paramod,[status(thm)],[c_10,c_10994]) ).
cnf(c_10995,plain,
mult(mult(A,B),i(A)) = mult(i(i(A)),rd(B,i(i(A)))),
inference(paramod,[status(thm)],[c_38,c_69]) ).
cnf(c_10996,plain,
mult(mult(A,B),i(A)) = mult(A,rd(B,i(i(A)))),
inference(paramod,[status(thm)],[c_38,c_10995]) ).
cnf(c_1101,plain,
mult(mult(A,B),i(A)) = mult(A,rd(B,A)),
inference(paramod,[status(thm)],[c_38,c_10996]) ).
cnf(c_10997,plain,
mult(A,i(rd(A,B))) = mult(rd(A,B),rd(B,rd(A,B))),
inference(paramod,[status(thm)],[c_3,c_1101]) ).
cnf(c_10998,plain,
mult(A,rd(B,A)) = mult(rd(A,B),rd(B,rd(A,B))),
inference(paramod,[status(thm)],[c_79,c_10997]) ).
cnf(c_1141,plain,
mult(rd(A,B),rd(B,rd(A,B))) = mult(A,rd(B,A)),
inference(copy,[status(thm)],[c_10998]) ).
cnf(c_10999,plain,
mult(mult(A,mult(op_c,op_c)),i(A)) = mult(A,rd(i(A),mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_346,c_1101]) ).
cnf(c_11000,plain,
mult(A,rd(mult(op_c,op_c),A)) = mult(A,rd(i(A),mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_1101,c_10999]) ).
cnf(c_1161,plain,
mult(A,rd(i(A),mult(op_c,op_c))) = mult(A,rd(mult(op_c,op_c),A)),
inference(copy,[status(thm)],[c_11000]) ).
cnf(c_11001,plain,
mult(rd(A,mult(op_c,op_c)),mult(rd(rd(A,mult(op_c,op_c)),rd(A,mult(op_c,op_c))),A)) = mult(mult(A,A),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_891,c_61]) ).
cnf(c_11002,plain,
mult(rd(A,mult(op_c,op_c)),mult(unit,A)) = mult(mult(A,A),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_20,c_11001]) ).
cnf(c_11003,plain,
mult(rd(A,mult(op_c,op_c)),A) = mult(mult(A,A),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_6,c_11002]) ).
cnf(c_1399,plain,
mult(rd(A,mult(op_c,op_c)),A) = mult(A,mult(A,mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_26,c_11003]) ).
cnf(c_11004,plain,
mult(mult(A,A),i(rd(A,mult(op_c,op_c)))) = mult(rd(A,mult(op_c,op_c)),rd(rd(A,mult(op_c,op_c)),rd(A,mult(op_c,op_c)))),
inference(paramod,[status(thm)],[c_891,c_1101]) ).
cnf(c_11005,plain,
mult(mult(A,A),rd(mult(op_c,op_c),A)) = mult(rd(A,mult(op_c,op_c)),rd(rd(A,mult(op_c,op_c)),rd(A,mult(op_c,op_c)))),
inference(paramod,[status(thm)],[c_79,c_11004]) ).
cnf(c_11006,plain,
mult(A,mult(A,rd(mult(op_c,op_c),A))) = mult(rd(A,mult(op_c,op_c)),rd(rd(A,mult(op_c,op_c)),rd(A,mult(op_c,op_c)))),
inference(paramod,[status(thm)],[c_26,c_11005]) ).
cnf(c_11007,plain,
mult(A,mult(A,rd(mult(op_c,op_c),A))) = mult(rd(A,mult(op_c,op_c)),unit),
inference(paramod,[status(thm)],[c_20,c_11006]) ).
cnf(c_1411,plain,
mult(A,mult(A,rd(mult(op_c,op_c),A))) = rd(A,mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_5,c_11007]) ).
cnf(c_11008,plain,
rd(A,mult(B,C)) = mult(i(B),mult(i(rd(C,mult(B,A))),i(B))),
inference(paramod,[status(thm)],[c_3,c_80]) ).
cnf(c_11009,plain,
rd(A,mult(B,C)) = mult(i(B),mult(rd(mult(B,A),C),i(B))),
inference(paramod,[status(thm)],[c_79,c_11008]) ).
cnf(c_1557,plain,
mult(i(A),mult(rd(mult(A,B),C),i(A))) = rd(B,mult(A,C)),
inference(copy,[status(thm)],[c_11009]) ).
cnf(c_11010,plain,
rd(A,mult(i(B),mult(mult(B,C),mult(rd(C,B),A)))) = mult(i(rd(C,B)),mult(i(B),i(rd(C,B)))),
inference(paramod,[status(thm)],[c_65,c_80]) ).
cnf(c_11011,plain,
rd(A,mult(rd(C,rd(B,C)),A)) = mult(i(rd(C,B)),mult(i(B),i(rd(C,B)))),
inference(paramod,[status(thm)],[c_994,c_11010]) ).
cnf(c_11012,plain,
i(rd(C,rd(B,C))) = mult(i(rd(C,B)),mult(i(B),i(rd(C,B)))),
inference(paramod,[status(thm)],[c_32,c_11011]) ).
cnf(c_11013,plain,
rd(rd(B,C),C) = mult(i(rd(C,B)),mult(i(B),i(rd(C,B)))),
inference(paramod,[status(thm)],[c_79,c_11012]) ).
cnf(c_11014,plain,
rd(rd(B,C),C) = mult(rd(B,C),mult(i(B),i(rd(C,B)))),
inference(paramod,[status(thm)],[c_79,c_11013]) ).
cnf(c_11015,plain,
rd(rd(B,C),C) = mult(rd(B,C),mult(i(B),rd(B,C))),
inference(paramod,[status(thm)],[c_79,c_11014]) ).
cnf(c_11016,plain,
rd(rd(B,C),C) = mult(B,mult(mult(i(B),i(C)),rd(B,C))),
inference(paramod,[status(thm)],[c_596,c_11015]) ).
cnf(c_1579,plain,
mult(A,mult(mult(i(A),i(B)),rd(A,B))) = rd(rd(A,B),B),
inference(copy,[status(thm)],[c_11016]) ).
cnf(c_11017,plain,
rd(mult(rd(op_d,A),i(op_d)),A) = mult(rd(op_d,A),mult(op_d,rd(op_d,A))),
inference(paramod,[status(thm)],[c_52,c_82]) ).
cnf(c_11018,plain,
rd(i(A),A) = mult(rd(op_d,A),mult(op_d,rd(op_d,A))),
inference(paramod,[status(thm)],[c_81,c_11017]) ).
cnf(c_11019,plain,
mult(i(A),i(A)) = mult(rd(op_d,A),mult(op_d,rd(op_d,A))),
inference(paramod,[status(thm)],[c_213,c_11018]) ).
cnf(c_1723,plain,
mult(rd(op_d,A),mult(op_d,rd(op_d,A))) = mult(i(A),i(A)),
inference(copy,[status(thm)],[c_11019]) ).
cnf(c_11020,plain,
rd(rd(mult(rd(A,op_d),i(op_d)),mult(mult(op_d,A),op_d)),mult(op_c,op_c)) = rd(mult(op_c,op_c),op_d),
inference(paramod,[status(thm)],[c_947,c_347]) ).
cnf(c_11021,plain,
rd(i(op_d),mult(op_c,op_c)) = rd(mult(op_c,op_c),op_d),
inference(paramod,[status(thm)],[c_951,c_11020]) ).
cnf(c_1892,plain,
rd(mult(op_c,op_c),op_d) = rd(i(op_d),mult(op_c,op_c)),
inference(copy,[status(thm)],[c_11021]) ).
cnf(c_11022,plain,
mult(mult(A,A),rd(i(A),mult(op_c,op_c))) = mult(A,mult(A,rd(mult(op_c,op_c),A))),
inference(paramod,[status(thm)],[c_1161,c_26]) ).
cnf(c_11023,plain,
mult(A,mult(A,rd(i(A),mult(op_c,op_c)))) = mult(A,mult(A,rd(mult(op_c,op_c),A))),
inference(paramod,[status(thm)],[c_26,c_11022]) ).
cnf(c_1917,plain,
mult(A,mult(A,rd(i(A),mult(op_c,op_c)))) = rd(A,mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_1411,c_11023]) ).
cnf(c_11024,plain,
mult(op_d,mult(op_d,rd(mult(op_c,op_c),op_d))) = mult(i(op_d),rd(i(op_d),mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_1161,c_68]) ).
cnf(c_11025,plain,
mult(op_d,mult(op_d,rd(i(op_d),mult(op_c,op_c)))) = mult(i(op_d),rd(i(op_d),mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_1892,c_11024]) ).
cnf(c_11026,plain,
rd(op_d,mult(op_c,op_c)) = mult(i(op_d),rd(i(op_d),mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_1917,c_11025]) ).
cnf(c_1918,plain,
mult(i(op_d),rd(i(op_d),mult(op_c,op_c))) = rd(op_d,mult(op_c,op_c)),
inference(copy,[status(thm)],[c_11026]) ).
cnf(c_11027,plain,
mult(i(op_d),mult(i(op_d),rd(i(op_d),mult(op_c,op_c)))) = mult(op_d,rd(mult(op_c,op_c),op_d)),
inference(paramod,[status(thm)],[c_1161,c_118]) ).
cnf(c_11028,plain,
mult(i(op_d),rd(op_d,mult(op_c,op_c))) = mult(op_d,rd(mult(op_c,op_c),op_d)),
inference(paramod,[status(thm)],[c_1918,c_11027]) ).
cnf(c_1927,plain,
mult(i(op_d),rd(op_d,mult(op_c,op_c))) = mult(op_d,rd(i(op_d),mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_1892,c_11028]) ).
cnf(c_11029,plain,
mult(i(op_d),mult(i(op_d),rd(i(i(op_d)),mult(op_c,op_c)))) = mult(op_d,rd(mult(op_c,op_c),i(op_d))),
inference(paramod,[status(thm)],[c_1161,c_118]) ).
cnf(c_11030,plain,
mult(i(op_d),mult(i(op_d),rd(op_d,mult(op_c,op_c)))) = mult(op_d,rd(mult(op_c,op_c),i(op_d))),
inference(paramod,[status(thm)],[c_38,c_11029]) ).
cnf(c_11031,plain,
mult(i(op_d),mult(op_d,rd(i(op_d),mult(op_c,op_c)))) = mult(op_d,rd(mult(op_c,op_c),i(op_d))),
inference(paramod,[status(thm)],[c_1927,c_11030]) ).
cnf(c_11032,plain,
rd(i(op_d),mult(op_c,op_c)) = mult(op_d,rd(mult(op_c,op_c),i(op_d))),
inference(paramod,[status(thm)],[c_9,c_11031]) ).
cnf(c_11033,plain,
rd(i(op_d),mult(op_c,op_c)) = mult(op_d,rd(op_d,i(mult(op_c,op_c)))),
inference(paramod,[status(thm)],[c_102,c_11032]) ).
cnf(c_11034,plain,
rd(i(op_d),mult(op_c,op_c)) = mult(op_d,rd(op_d,mult(i(op_c),i(op_c)))),
inference(paramod,[status(thm)],[c_10,c_11033]) ).
cnf(c_11035,plain,
rd(i(op_d),mult(op_c,op_c)) = mult(op_d,rd(op_d,mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_124,c_11034]) ).
cnf(c_1928,plain,
mult(op_d,rd(op_d,mult(op_c,op_c))) = rd(i(op_d),mult(op_c,op_c)),
inference(copy,[status(thm)],[c_11035]) ).
cnf(c_11036,plain,
mult(i(A),rd(mult(A,B),C)) = mult(rd(B,mult(A,C)),A),
inference(paramod,[status(thm)],[c_83,c_9]) ).
cnf(c_1980,plain,
mult(rd(A,mult(B,C)),B) = mult(i(B),rd(mult(B,A),C)),
inference(copy,[status(thm)],[c_11036]) ).
cnf(c_11037,plain,
mult(A,mult(rd(B,C),A)) = rd(mult(A,B),mult(i(A),C)),
inference(paramod,[status(thm)],[c_39,c_83]) ).
cnf(c_1989,plain,
rd(mult(A,B),mult(i(A),C)) = mult(A,mult(rd(B,C),A)),
inference(copy,[status(thm)],[c_11037]) ).
cnf(c_11038,plain,
mult(A,mult(rd(B,mult(A,i(mult(A,B)))),A)) = mult(mult(A,B),mult(A,B)),
inference(paramod,[status(thm)],[c_214,c_83]) ).
cnf(c_11039,plain,
mult(A,mult(rd(B,mult(A,mult(i(A),i(B)))),A)) = mult(mult(A,B),mult(A,B)),
inference(paramod,[status(thm)],[c_10,c_11038]) ).
cnf(c_11040,plain,
mult(A,mult(rd(B,i(B)),A)) = mult(mult(A,B),mult(A,B)),
inference(paramod,[status(thm)],[c_39,c_11039]) ).
cnf(c_11041,plain,
mult(A,mult(mult(B,B),A)) = mult(mult(A,B),mult(A,B)),
inference(paramod,[status(thm)],[c_214,c_11040]) ).
cnf(c_11042,plain,
mult(A,mult(B,mult(B,A))) = mult(mult(A,B),mult(A,B)),
inference(paramod,[status(thm)],[c_26,c_11041]) ).
cnf(c_1992,plain,
mult(mult(A,B),mult(A,B)) = mult(A,mult(B,mult(B,A))),
inference(copy,[status(thm)],[c_11042]) ).
cnf(c_11043,plain,
mult(rd(mult(A,B),C),i(A)) = mult(A,rd(mult(rd(B,mult(A,C)),A),A)),
inference(paramod,[status(thm)],[c_83,c_1101]) ).
cnf(c_11044,plain,
mult(rd(mult(A,B),C),i(A)) = mult(A,rd(mult(i(A),rd(mult(A,B),C)),A)),
inference(paramod,[status(thm)],[c_1980,c_11043]) ).
cnf(c_11045,plain,
mult(rd(mult(A,B),C),i(A)) = mult(A,mult(i(A),mult(rd(mult(A,B),C),i(A)))),
inference(paramod,[status(thm)],[c_89,c_11044]) ).
cnf(c_2016,plain,
mult(rd(mult(A,B),C),i(A)) = mult(A,rd(B,mult(A,C))),
inference(paramod,[status(thm)],[c_1557,c_11045]) ).
cnf(c_11046,plain,
rd(op_d,rd(op_d,mult(op_c,op_c))) = mult(op_d,mult(i(rd(i(op_d),mult(op_c,op_c))),op_d)),
inference(paramod,[status(thm)],[c_1918,c_968]) ).
cnf(c_11047,plain,
rd(op_d,rd(op_d,mult(op_c,op_c))) = mult(op_d,mult(rd(mult(op_c,op_c),i(op_d)),op_d)),
inference(paramod,[status(thm)],[c_79,c_11046]) ).
cnf(c_11048,plain,
rd(op_d,rd(op_d,mult(op_c,op_c))) = mult(op_d,mult(rd(op_d,i(mult(op_c,op_c))),op_d)),
inference(paramod,[status(thm)],[c_102,c_11047]) ).
cnf(c_11049,plain,
rd(op_d,rd(op_d,mult(op_c,op_c))) = mult(op_d,mult(rd(op_d,mult(i(op_c),i(op_c))),op_d)),
inference(paramod,[status(thm)],[c_10,c_11048]) ).
cnf(c_11050,plain,
rd(op_d,rd(op_d,mult(op_c,op_c))) = mult(op_d,mult(rd(op_d,mult(op_c,op_c)),op_d)),
inference(paramod,[status(thm)],[c_124,c_11049]) ).
cnf(c_11051,plain,
rd(op_d,rd(op_d,mult(op_c,op_c))) = mult(op_d,mult(op_d,mult(op_d,mult(op_c,op_c)))),
inference(paramod,[status(thm)],[c_1399,c_11050]) ).
cnf(c_11052,plain,
rd(op_d,rd(op_d,mult(op_c,op_c))) = mult(op_d,mult(i(op_d),mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_68,c_11051]) ).
cnf(c_2103,plain,
rd(op_d,rd(op_d,mult(op_c,op_c))) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_39,c_11052]) ).
cnf(c_11053,plain,
rd(rd(op_d,mult(op_c,op_c)),op_d) = mult(i(op_d),mult(rd(i(op_d),mult(op_c,op_c)),i(op_d))),
inference(paramod,[status(thm)],[c_1918,c_89]) ).
cnf(c_11054,plain,
rd(rd(op_d,mult(op_c,op_c)),op_d) = mult(i(op_d),mult(i(op_d),mult(i(op_d),mult(op_c,op_c)))),
inference(paramod,[status(thm)],[c_1399,c_11053]) ).
cnf(c_11055,plain,
rd(rd(op_d,mult(op_c,op_c)),op_d) = mult(i(op_d),mult(op_d,mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_118,c_11054]) ).
cnf(c_2106,plain,
rd(rd(op_d,mult(op_c,op_c)),op_d) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_9,c_11055]) ).
cnf(c_11056,plain,
mult(mult(op_c,op_c),i(op_d)) = i(rd(op_d,mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_2103,c_81]) ).
cnf(c_11057,plain,
mult(op_c,mult(op_c,i(op_d))) = i(rd(op_d,mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_26,c_11056]) ).
cnf(c_11058,plain,
mult(op_c,mult(op_c,i(op_d))) = rd(mult(op_c,op_c),op_d),
inference(paramod,[status(thm)],[c_79,c_11057]) ).
cnf(c_11059,plain,
mult(op_c,mult(op_c,i(op_d))) = rd(i(op_d),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_1892,c_11058]) ).
cnf(c_2113,plain,
rd(i(op_d),mult(op_c,op_c)) = mult(op_c,mult(op_c,i(op_d))),
inference(copy,[status(thm)],[c_11059]) ).
cnf(c_2135,plain,
mult(op_d,rd(op_d,mult(op_c,op_c))) = mult(op_c,mult(op_c,i(op_d))),
inference(paramod,[status(thm)],[c_2113,c_1928]) ).
cnf(c_2136,plain,
mult(i(op_d),rd(op_d,mult(op_c,op_c))) = mult(op_d,mult(op_c,mult(op_c,i(op_d)))),
inference(paramod,[status(thm)],[c_2113,c_1927]) ).
cnf(c_2138,plain,
rd(mult(op_c,op_c),op_d) = mult(op_c,mult(op_c,i(op_d))),
inference(paramod,[status(thm)],[c_2113,c_1892]) ).
cnf(c_11060,plain,
mult(mult(op_c,op_c),op_d) = rd(op_d,mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_2106,c_3]) ).
cnf(c_11061,plain,
mult(op_c,mult(op_c,op_d)) = rd(op_d,mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_26,c_11060]) ).
cnf(c_2139,plain,
rd(op_d,mult(op_c,op_c)) = mult(op_c,mult(op_c,op_d)),
inference(copy,[status(thm)],[c_11061]) ).
cnf(c_2141,plain,
mult(i(op_d),mult(op_c,mult(op_c,op_d))) = mult(op_d,mult(op_c,mult(op_c,i(op_d)))),
inference(paramod,[status(thm)],[c_2139,c_2136]) ).
cnf(c_2142,plain,
mult(op_d,mult(op_c,mult(op_c,op_d))) = mult(op_c,mult(op_c,i(op_d))),
inference(paramod,[status(thm)],[c_2139,c_2135]) ).
cnf(c_11062,plain,
mult(mult(op_c,mult(op_c,op_d)),i(op_d)) = i(mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_2139,c_81]) ).
cnf(c_11063,plain,
mult(mult(op_c,mult(op_c,op_d)),i(op_d)) = mult(i(op_c),i(op_c)),
inference(paramod,[status(thm)],[c_10,c_11062]) ).
cnf(c_2159,plain,
mult(mult(op_c,mult(op_c,op_d)),i(op_d)) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_124,c_11063]) ).
cnf(c_2179,plain,
mult(mult(op_c,mult(op_c,i(op_d))),mult(op_d,A)) = mult(i(op_d),mult(mult(op_d,mult(op_c,op_c)),A)),
inference(paramod,[status(thm)],[c_2138,c_65]) ).
cnf(c_11064,plain,
mult(mult(op_c,mult(op_c,i(op_d))),i(op_c)) = mult(op_c,rd(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_2138,c_2016]) ).
cnf(c_2558,plain,
mult(op_c,rd(mult(op_c,i(op_d)),op_c)) = mult(op_c,rd(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_1101,c_11064]) ).
cnf(c_11065,plain,
rd(mult(op_d,i(A)),op_d) = mult(op_d,mult(rd(op_d,A),op_d)),
inference(paramod,[status(thm)],[c_81,c_88]) ).
cnf(c_2573,plain,
mult(op_d,mult(rd(op_d,A),op_d)) = rd(mult(op_d,i(A)),op_d),
inference(copy,[status(thm)],[c_11065]) ).
cnf(c_11066,plain,
rd(mult(op_d,mult(A,mult(A,i(op_d)))),op_d) = mult(op_d,mult(mult(A,A),op_d)),
inference(paramod,[status(thm)],[c_26,c_88]) ).
cnf(c_2574,plain,
rd(mult(op_d,mult(A,mult(A,i(op_d)))),op_d) = mult(op_d,mult(A,mult(A,op_d))),
inference(paramod,[status(thm)],[c_26,c_11066]) ).
cnf(c_11067,plain,
rd(mult(i(op_d),mult(op_c,mult(op_c,op_d))),op_d) = mult(i(op_d),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_2159,c_89]) ).
cnf(c_11068,plain,
rd(mult(op_d,mult(op_c,mult(op_c,i(op_d)))),op_d) = mult(i(op_d),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_2141,c_11067]) ).
cnf(c_11069,plain,
mult(op_d,mult(op_c,mult(op_c,op_d))) = mult(i(op_d),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_2574,c_11068]) ).
cnf(c_11070,plain,
mult(op_c,mult(op_c,i(op_d))) = mult(i(op_d),mult(op_c,op_c)),
inference(paramod,[status(thm)],[c_2142,c_11069]) ).
cnf(c_2586,plain,
mult(i(op_d),mult(op_c,op_c)) = mult(op_c,mult(op_c,i(op_d))),
inference(copy,[status(thm)],[c_11070]) ).
cnf(c_11071,plain,
rd(mult(op_d,mult(op_c,op_c)),op_d) = mult(op_d,mult(mult(op_c,mult(op_c,op_d)),op_d)),
inference(paramod,[status(thm)],[c_2159,c_88]) ).
cnf(c_2592,plain,
mult(op_d,mult(mult(op_c,mult(op_c,op_d)),op_d)) = rd(mult(op_d,mult(op_c,op_c)),op_d),
inference(copy,[status(thm)],[c_11071]) ).
cnf(c_11072,plain,
mult(mult(rd(op_d,A),mult(op_d,rd(op_d,A))),op_d) = mult(rd(op_d,A),rd(mult(op_d,i(A)),op_d)),
inference(paramod,[status(thm)],[c_2573,c_8]) ).
cnf(c_11073,plain,
mult(mult(i(A),i(A)),op_d) = mult(rd(op_d,A),rd(mult(op_d,i(A)),op_d)),
inference(paramod,[status(thm)],[c_1723,c_11072]) ).
cnf(c_11074,plain,
mult(i(A),mult(i(A),op_d)) = mult(rd(op_d,A),rd(mult(op_d,i(A)),op_d)),
inference(paramod,[status(thm)],[c_26,c_11073]) ).
cnf(c_2702,plain,
mult(rd(op_d,A),rd(mult(op_d,i(A)),op_d)) = mult(i(A),mult(i(A),op_d)),
inference(copy,[status(thm)],[c_11074]) ).
cnf(c_11075,plain,
mult(op_d,mult(rd(op_d,A),op_d)) = rd(i(op_d),i(mult(op_d,i(A)))),
inference(paramod,[status(thm)],[c_90,c_2573]) ).
cnf(c_11076,plain,
rd(mult(op_d,i(A)),op_d) = rd(i(op_d),i(mult(op_d,i(A)))),
inference(paramod,[status(thm)],[c_2573,c_11075]) ).
cnf(c_11077,plain,
rd(mult(op_d,i(A)),op_d) = rd(i(op_d),mult(i(op_d),i(i(A)))),
inference(paramod,[status(thm)],[c_10,c_11076]) ).
cnf(c_2705,plain,
rd(mult(op_d,i(A)),op_d) = rd(i(op_d),mult(i(op_d),A)),
inference(paramod,[status(thm)],[c_38,c_11077]) ).
cnf(c_11078,plain,
rd(op_d,mult(rd(op_d,A),rd(mult(op_d,i(A)),op_d))) = mult(i(rd(op_d,A)),mult(i(op_d),i(rd(op_d,A)))),
inference(paramod,[status(thm)],[c_2573,c_80]) ).
cnf(c_11079,plain,
rd(op_d,mult(rd(op_d,A),rd(i(op_d),mult(i(op_d),A)))) = mult(i(rd(op_d,A)),mult(i(op_d),i(rd(op_d,A)))),
inference(paramod,[status(thm)],[c_2705,c_11078]) ).
cnf(c_11080,plain,
rd(op_d,mult(rd(op_d,A),rd(i(op_d),mult(i(op_d),A)))) = mult(rd(A,op_d),mult(i(op_d),i(rd(op_d,A)))),
inference(paramod,[status(thm)],[c_79,c_11079]) ).
cnf(c_2715,plain,
rd(op_d,mult(rd(op_d,A),rd(i(op_d),mult(i(op_d),A)))) = mult(rd(A,op_d),mult(i(op_d),rd(A,op_d))),
inference(paramod,[status(thm)],[c_79,c_11080]) ).
cnf(c_2726,plain,
mult(rd(op_d,A),rd(i(op_d),mult(i(op_d),A))) = mult(i(A),mult(i(A),op_d)),
inference(paramod,[status(thm)],[c_2705,c_2702]) ).
cnf(c_11081,plain,
rd(op_d,mult(i(A),mult(i(A),op_d))) = mult(rd(A,op_d),mult(i(op_d),rd(A,op_d))),
inference(paramod,[status(thm)],[c_2726,c_2715]) ).
cnf(c_11082,plain,
mult(i(i(A)),i(i(A))) = mult(rd(A,op_d),mult(i(op_d),rd(A,op_d))),
inference(paramod,[status(thm)],[c_119,c_11081]) ).
cnf(c_11083,plain,
mult(A,i(i(A))) = mult(rd(A,op_d),mult(i(op_d),rd(A,op_d))),
inference(paramod,[status(thm)],[c_38,c_11082]) ).
cnf(c_11084,plain,
mult(A,A) = mult(rd(A,op_d),mult(i(op_d),rd(A,op_d))),
inference(paramod,[status(thm)],[c_38,c_11083]) ).
cnf(c_2733,plain,
mult(rd(A,op_d),mult(i(op_d),rd(A,op_d))) = mult(A,A),
inference(copy,[status(thm)],[c_11084]) ).
cnf(c_2736,plain,
rd(mult(op_d,A),op_d) = rd(i(op_d),mult(i(op_d),i(A))),
inference(paramod,[status(thm)],[c_38,c_2705]) ).
cnf(c_11085,plain,
mult(op_d,mult(mult(op_c,mult(op_c,op_d)),op_d)) = rd(i(op_d),mult(i(op_d),i(mult(op_c,op_c)))),
inference(paramod,[status(thm)],[c_2736,c_2592]) ).
cnf(c_11086,plain,
mult(op_d,mult(mult(op_c,mult(op_c,op_d)),op_d)) = rd(i(op_d),mult(i(op_d),mult(i(op_c),i(op_c)))),
inference(paramod,[status(thm)],[c_10,c_11085]) ).
cnf(c_11087,plain,
mult(op_d,mult(mult(op_c,mult(op_c,op_d)),op_d)) = rd(i(op_d),mult(i(op_d),mult(op_c,op_c))),
inference(paramod,[status(thm)],[c_124,c_11086]) ).
cnf(c_11088,plain,
mult(op_d,mult(mult(op_c,mult(op_c,op_d)),op_d)) = rd(i(op_d),mult(op_c,mult(op_c,i(op_d)))),
inference(paramod,[status(thm)],[c_2586,c_11087]) ).
cnf(c_11089,plain,
mult(op_d,mult(mult(op_c,mult(op_c,op_d)),op_d)) = mult(i(op_c),i(op_c)),
inference(paramod,[status(thm)],[c_119,c_11088]) ).
cnf(c_2744,plain,
mult(op_d,mult(mult(op_c,mult(op_c,op_d)),op_d)) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_124,c_11089]) ).
cnf(c_11090,plain,
rd(i(A),rd(A,B)) = mult(rd(B,A),mult(i(B),rd(B,A))),
inference(paramod,[status(thm)],[c_81,c_109]) ).
cnf(c_11091,plain,
rd(i(A),rd(A,B)) = mult(B,mult(mult(i(B),i(A)),rd(B,A))),
inference(paramod,[status(thm)],[c_596,c_11090]) ).
cnf(c_11092,plain,
rd(i(A),rd(A,B)) = rd(rd(B,A),A),
inference(paramod,[status(thm)],[c_1579,c_11091]) ).
cnf(c_2768,plain,
rd(rd(A,B),B) = rd(i(B),rd(B,A)),
inference(copy,[status(thm)],[c_11092]) ).
cnf(c_2878,plain,
rd(mult(A,A),mult(i(op_d),rd(A,op_d))) = rd(A,op_d),
inference(paramod,[status(thm)],[c_2733,c_4]) ).
cnf(c_11093,plain,
mult(rd(A,op_d),mult(rd(mult(i(op_d),rd(A,op_d)),rd(A,op_d)),A)) = mult(mult(A,A),op_d),
inference(paramod,[status(thm)],[c_2733,c_61]) ).
cnf(c_11094,plain,
mult(rd(A,op_d),mult(i(op_d),A)) = mult(mult(A,A),op_d),
inference(paramod,[status(thm)],[c_4,c_11093]) ).
cnf(c_2897,plain,
mult(rd(A,op_d),mult(i(op_d),A)) = mult(A,mult(A,op_d)),
inference(paramod,[status(thm)],[c_26,c_11094]) ).
cnf(c_11095,plain,
mult(mult(A,A),i(rd(A,op_d))) = mult(rd(A,op_d),rd(mult(i(op_d),rd(A,op_d)),rd(A,op_d))),
inference(paramod,[status(thm)],[c_2733,c_1101]) ).
cnf(c_11096,plain,
mult(mult(A,A),rd(op_d,A)) = mult(rd(A,op_d),rd(mult(i(op_d),rd(A,op_d)),rd(A,op_d))),
inference(paramod,[status(thm)],[c_79,c_11095]) ).
cnf(c_11097,plain,
mult(A,mult(A,rd(op_d,A))) = mult(rd(A,op_d),rd(mult(i(op_d),rd(A,op_d)),rd(A,op_d))),
inference(paramod,[status(thm)],[c_26,c_11096]) ).
cnf(c_2910,plain,
mult(A,mult(A,rd(op_d,A))) = mult(rd(A,op_d),i(op_d)),
inference(paramod,[status(thm)],[c_4,c_11097]) ).
cnf(c_11098,plain,
rd(i(mult(i(op_d),rd(A,op_d))),i(mult(A,A))) = rd(A,op_d),
inference(paramod,[status(thm)],[c_2878,c_90]) ).
cnf(c_11099,plain,
rd(mult(i(i(op_d)),i(rd(A,op_d))),i(mult(A,A))) = rd(A,op_d),
inference(paramod,[status(thm)],[c_10,c_11098]) ).
cnf(c_11100,plain,
rd(mult(op_d,i(rd(A,op_d))),i(mult(A,A))) = rd(A,op_d),
inference(paramod,[status(thm)],[c_38,c_11099]) ).
cnf(c_11101,plain,
rd(mult(op_d,rd(op_d,A)),i(mult(A,A))) = rd(A,op_d),
inference(paramod,[status(thm)],[c_79,c_11100]) ).
cnf(c_2927,plain,
rd(mult(op_d,rd(op_d,A)),mult(i(A),i(A))) = rd(A,op_d),
inference(paramod,[status(thm)],[c_10,c_11101]) ).
cnf(c_11102,plain,
rd(mult(op_d,rd(op_d,mult(A,B))),mult(mult(i(A),i(B)),i(mult(A,B)))) = rd(mult(A,B),op_d),
inference(paramod,[status(thm)],[c_10,c_2927]) ).
cnf(c_11103,plain,
rd(mult(op_d,rd(op_d,mult(A,B))),mult(mult(i(A),i(B)),mult(i(A),i(B)))) = rd(mult(A,B),op_d),
inference(paramod,[status(thm)],[c_10,c_11102]) ).
cnf(c_3143,plain,
rd(mult(op_d,rd(op_d,mult(A,B))),mult(i(A),mult(i(B),mult(i(B),i(A))))) = rd(mult(A,B),op_d),
inference(paramod,[status(thm)],[c_1992,c_11103]) ).
cnf(c_11104,plain,
rd(mult(op_d,rd(op_d,mult(A,B))),mult(i(mult(A,B)),i(mult(A,B)))) = rd(i(op_d),mult(i(A),i(B))),
inference(paramod,[status(thm)],[c_101,c_2927]) ).
cnf(c_11105,plain,
rd(mult(op_d,rd(op_d,mult(A,B))),mult(mult(i(A),i(B)),i(mult(A,B)))) = rd(i(op_d),mult(i(A),i(B))),
inference(paramod,[status(thm)],[c_10,c_11104]) ).
cnf(c_11106,plain,
rd(mult(op_d,rd(op_d,mult(A,B))),mult(mult(i(A),i(B)),mult(i(A),i(B)))) = rd(i(op_d),mult(i(A),i(B))),
inference(paramod,[status(thm)],[c_10,c_11105]) ).
cnf(c_11107,plain,
rd(mult(op_d,rd(op_d,mult(A,B))),mult(i(A),mult(i(B),mult(i(B),i(A))))) = rd(i(op_d),mult(i(A),i(B))),
inference(paramod,[status(thm)],[c_1992,c_11106]) ).
cnf(c_3150,plain,
rd(mult(A,B),op_d) = rd(i(op_d),mult(i(A),i(B))),
inference(paramod,[status(thm)],[c_3143,c_11107]) ).
cnf(c_3288,plain,
rd(mult(rd(A,op_d),i(op_d)),mult(A,rd(op_d,A))) = A,
inference(paramod,[status(thm)],[c_2910,c_4]) ).
cnf(c_11108,plain,
rd(mult(A,i(op_d)),mult(mult(A,op_d),rd(op_d,mult(A,op_d)))) = mult(A,op_d),
inference(paramod,[status(thm)],[c_4,c_3288]) ).
cnf(c_11109,plain,
rd(mult(A,i(op_d)),mult(mult(A,op_d),i(A))) = mult(A,op_d),
inference(paramod,[status(thm)],[c_32,c_11108]) ).
cnf(c_3355,plain,
rd(mult(A,i(op_d)),mult(A,rd(op_d,A))) = mult(A,op_d),
inference(paramod,[status(thm)],[c_1101,c_11109]) ).
cnf(c_11110,plain,
mult(A,i(mult(rd(A,op_d),i(op_d)))) = i(mult(A,rd(op_d,A))),
inference(paramod,[status(thm)],[c_3288,c_81]) ).
cnf(c_11111,plain,
mult(A,mult(i(rd(A,op_d)),i(i(op_d)))) = i(mult(A,rd(op_d,A))),
inference(paramod,[status(thm)],[c_10,c_11110]) ).
cnf(c_11112,plain,
mult(A,mult(rd(op_d,A),i(i(op_d)))) = i(mult(A,rd(op_d,A))),
inference(paramod,[status(thm)],[c_79,c_11111]) ).
cnf(c_11113,plain,
mult(A,mult(rd(op_d,A),op_d)) = i(mult(A,rd(op_d,A))),
inference(paramod,[status(thm)],[c_38,c_11112]) ).
cnf(c_11114,plain,
mult(A,mult(rd(op_d,A),op_d)) = mult(i(A),i(rd(op_d,A))),
inference(paramod,[status(thm)],[c_10,c_11113]) ).
cnf(c_3358,plain,
mult(A,mult(rd(op_d,A),op_d)) = mult(i(A),rd(A,op_d)),
inference(paramod,[status(thm)],[c_79,c_11114]) ).
cnf(c_11115,plain,
rd(mult(op_c,op_c),mult(mult(op_c,mult(op_c,op_d)),rd(op_d,mult(op_c,mult(op_c,op_d))))) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_2159,c_3355]) ).
cnf(c_11116,plain,
rd(mult(op_c,op_c),mult(mult(op_c,mult(op_c,op_d)),mult(i(op_c),i(op_c)))) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_119,c_11115]) ).
cnf(c_11117,plain,
rd(mult(op_c,op_c),mult(mult(op_c,mult(op_c,op_d)),mult(op_c,op_c))) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_124,c_11116]) ).
cnf(c_11118,plain,
rd(mult(op_c,op_c),mult(op_c,mult(rd(mult(op_c,op_d),op_c),i(op_c)))) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_259,c_11117]) ).
cnf(c_11119,plain,
rd(mult(op_c,op_c),mult(op_c,mult(op_c,rd(op_d,mult(op_c,op_c))))) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_2016,c_11118]) ).
cnf(c_11120,plain,
rd(mult(op_c,op_c),mult(op_c,mult(op_c,mult(op_c,mult(op_c,op_d))))) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_2139,c_11119]) ).
cnf(c_11121,plain,
rd(mult(op_c,op_c),mult(op_c,mult(i(op_c),op_d))) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_123,c_11120]) ).
cnf(c_11122,plain,
rd(mult(op_c,op_c),op_d) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_39,c_11121]) ).
cnf(c_11123,plain,
rd(i(op_d),mult(i(op_c),i(op_c))) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_3150,c_11122]) ).
cnf(c_11124,plain,
rd(i(op_d),mult(op_c,op_c)) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_124,c_11123]) ).
cnf(c_11125,plain,
mult(op_c,mult(op_c,i(op_d))) = mult(mult(op_c,mult(op_c,op_d)),op_d),
inference(paramod,[status(thm)],[c_2113,c_11124]) ).
cnf(c_3436,plain,
mult(mult(op_c,mult(op_c,op_d)),op_d) = mult(op_c,mult(op_c,i(op_d))),
inference(copy,[status(thm)],[c_11125]) ).
cnf(c_3438,plain,
mult(op_d,mult(op_c,mult(op_c,i(op_d)))) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_3436,c_2744]) ).
cnf(c_3439,plain,
mult(i(op_d),mult(op_c,mult(op_c,op_d))) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_3438,c_2141]) ).
cnf(c_11126,plain,
mult(op_c,mult(op_c,mult(i(op_c),rd(op_c,op_d)))) = mult(i(op_c),mult(rd(op_d,op_c),op_d)),
inference(paramod,[status(thm)],[c_3358,c_123]) ).
cnf(c_11127,plain,
mult(op_c,rd(op_c,op_d)) = mult(i(op_c),mult(rd(op_d,op_c),op_d)),
inference(paramod,[status(thm)],[c_39,c_11126]) ).
cnf(c_3594,plain,
mult(i(op_c),mult(rd(op_d,op_c),op_d)) = mult(op_c,rd(op_c,op_d)),
inference(copy,[status(thm)],[c_11127]) ).
cnf(c_11128,plain,
mult(i(i(op_d)),mult(op_c,op_c)) = mult(op_c,mult(op_c,op_d)),
inference(paramod,[status(thm)],[c_3439,c_9]) ).
cnf(c_3646,plain,
mult(op_d,mult(op_c,op_c)) = mult(op_c,mult(op_c,op_d)),
inference(paramod,[status(thm)],[c_38,c_11128]) ).
cnf(c_11129,plain,
rd(mult(op_c,op_d),mult(op_c,mult(op_c,op_c))) = mult(i(op_c),mult(i(i(op_d)),i(op_c))),
inference(paramod,[status(thm)],[c_3439,c_80]) ).
cnf(c_11130,plain,
rd(mult(op_c,op_d),i(op_c)) = mult(i(op_c),mult(i(i(op_d)),i(op_c))),
inference(paramod,[status(thm)],[c_45,c_11129]) ).
cnf(c_11131,plain,
rd(op_c,i(mult(op_c,op_d))) = mult(i(op_c),mult(i(i(op_d)),i(op_c))),
inference(paramod,[status(thm)],[c_102,c_11130]) ).
cnf(c_11132,plain,
rd(op_c,mult(i(op_c),i(op_d))) = mult(i(op_c),mult(i(i(op_d)),i(op_c))),
inference(paramod,[status(thm)],[c_10,c_11131]) ).
cnf(c_11133,plain,
mult(op_c,mult(i(i(op_d)),op_c)) = mult(i(op_c),mult(i(i(op_d)),i(op_c))),
inference(paramod,[status(thm)],[c_968,c_11132]) ).
cnf(c_11134,plain,
mult(op_c,mult(op_d,op_c)) = mult(i(op_c),mult(i(i(op_d)),i(op_c))),
inference(paramod,[status(thm)],[c_38,c_11133]) ).
cnf(c_11135,plain,
mult(op_c,mult(op_d,op_c)) = mult(i(op_c),mult(op_d,i(op_c))),
inference(paramod,[status(thm)],[c_38,c_11134]) ).
cnf(c_3655,plain,
mult(i(op_c),mult(op_d,i(op_c))) = mult(op_c,mult(op_d,op_c)),
inference(copy,[status(thm)],[c_11135]) ).
cnf(c_3665,plain,
mult(mult(op_c,mult(op_c,i(op_d))),mult(op_d,A)) = mult(i(op_d),mult(mult(op_c,mult(op_c,op_d)),A)),
inference(paramod,[status(thm)],[c_3646,c_2179]) ).
cnf(c_3683,plain,
rd(mult(op_c,rd(op_c,op_d)),mult(rd(op_d,op_c),op_d)) = i(op_c),
inference(paramod,[status(thm)],[c_3594,c_4]) ).
cnf(c_11136,plain,
rd(mult(rd(op_d,op_c),op_d),mult(op_c,rd(op_c,op_d))) = i(i(op_c)),
inference(paramod,[status(thm)],[c_3594,c_32]) ).
cnf(c_3686,plain,
rd(mult(rd(op_d,op_c),op_d),mult(op_c,rd(op_c,op_d))) = op_c,
inference(paramod,[status(thm)],[c_38,c_11136]) ).
cnf(c_11137,plain,
rd(i(op_c),mult(i(op_c),A)) = mult(i(op_c),mult(i(mult(op_c,mult(op_c,A))),i(op_c))),
inference(paramod,[status(thm)],[c_123,c_995]) ).
cnf(c_11138,plain,
rd(i(op_c),mult(i(op_c),A)) = mult(i(op_c),mult(mult(i(op_c),i(mult(op_c,A))),i(op_c))),
inference(paramod,[status(thm)],[c_10,c_11137]) ).
cnf(c_11139,plain,
rd(i(op_c),mult(i(op_c),A)) = mult(i(op_c),mult(mult(i(op_c),mult(i(op_c),i(A))),i(op_c))),
inference(paramod,[status(thm)],[c_10,c_11138]) ).
cnf(c_11140,plain,
rd(i(op_c),mult(i(op_c),A)) = mult(i(op_c),mult(mult(op_c,mult(op_c,i(A))),i(op_c))),
inference(paramod,[status(thm)],[c_127,c_11139]) ).
cnf(c_11141,plain,
rd(i(op_c),mult(i(op_c),A)) = mult(i(op_c),mult(op_c,rd(mult(op_c,i(A)),op_c))),
inference(paramod,[status(thm)],[c_1101,c_11140]) ).
cnf(c_11142,plain,
rd(i(op_c),mult(i(op_c),A)) = rd(mult(op_c,i(A)),op_c),
inference(paramod,[status(thm)],[c_9,c_11141]) ).
cnf(c_4934,plain,
rd(mult(op_c,i(A)),op_c) = rd(i(op_c),mult(i(op_c),A)),
inference(copy,[status(thm)],[c_11142]) ).
cnf(c_4949,plain,
mult(op_c,rd(i(op_c),mult(i(op_c),op_d))) = mult(op_c,rd(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_4934,c_2558]) ).
cnf(c_4951,plain,
rd(mult(op_c,A),op_c) = rd(i(op_c),mult(i(op_c),i(A))),
inference(paramod,[status(thm)],[c_38,c_4934]) ).
cnf(c_11143,plain,
mult(rd(mult(op_c,op_c),i(op_d)),mult(i(op_d),A)) = mult(i(i(op_d)),mult(mult(op_c,mult(op_c,i(op_d))),A)),
inference(paramod,[status(thm)],[c_2586,c_65]) ).
cnf(c_11144,plain,
mult(rd(op_d,i(mult(op_c,op_c))),mult(i(op_d),A)) = mult(i(i(op_d)),mult(mult(op_c,mult(op_c,i(op_d))),A)),
inference(paramod,[status(thm)],[c_102,c_11143]) ).
cnf(c_11145,plain,
mult(rd(op_d,mult(i(op_c),i(op_c))),mult(i(op_d),A)) = mult(i(i(op_d)),mult(mult(op_c,mult(op_c,i(op_d))),A)),
inference(paramod,[status(thm)],[c_10,c_11144]) ).
cnf(c_11146,plain,
mult(rd(op_d,mult(op_c,op_c)),mult(i(op_d),A)) = mult(i(i(op_d)),mult(mult(op_c,mult(op_c,i(op_d))),A)),
inference(paramod,[status(thm)],[c_124,c_11145]) ).
cnf(c_11147,plain,
mult(mult(op_c,mult(op_c,op_d)),mult(i(op_d),A)) = mult(i(i(op_d)),mult(mult(op_c,mult(op_c,i(op_d))),A)),
inference(paramod,[status(thm)],[c_2139,c_11146]) ).
cnf(c_5796,plain,
mult(mult(op_c,mult(op_c,op_d)),mult(i(op_d),A)) = mult(op_d,mult(mult(op_c,mult(op_c,i(op_d))),A)),
inference(paramod,[status(thm)],[c_38,c_11147]) ).
cnf(c_11148,plain,
mult(mult(op_c,mult(op_d,op_c)),A) = mult(i(op_c),mult(op_d,mult(i(op_c),A))),
inference(paramod,[status(thm)],[c_3655,c_8]) ).
cnf(c_11149,plain,
mult(op_c,mult(op_d,mult(op_c,A))) = mult(i(op_c),mult(op_d,mult(i(op_c),A))),
inference(paramod,[status(thm)],[c_8,c_11148]) ).
cnf(c_5987,plain,
mult(i(op_c),mult(op_d,mult(i(op_c),A))) = mult(op_c,mult(op_d,mult(op_c,A))),
inference(copy,[status(thm)],[c_11149]) ).
cnf(c_11150,plain,
mult(i(i(op_c)),mult(op_c,mult(op_d,op_c))) = mult(op_d,i(op_c)),
inference(paramod,[status(thm)],[c_3655,c_9]) ).
cnf(c_5988,plain,
mult(op_c,mult(op_c,mult(op_d,op_c))) = mult(op_d,i(op_c)),
inference(paramod,[status(thm)],[c_38,c_11150]) ).
cnf(c_11151,plain,
mult(rd(mult(op_d,i(op_c)),i(op_c)),mult(i(op_c),A)) = mult(i(i(op_c)),mult(mult(op_c,mult(op_d,op_c)),A)),
inference(paramod,[status(thm)],[c_3655,c_65]) ).
cnf(c_11152,plain,
mult(rd(op_c,i(mult(op_d,i(op_c)))),mult(i(op_c),A)) = mult(i(i(op_c)),mult(mult(op_c,mult(op_d,op_c)),A)),
inference(paramod,[status(thm)],[c_102,c_11151]) ).
cnf(c_11153,plain,
mult(rd(op_c,mult(i(op_d),i(i(op_c)))),mult(i(op_c),A)) = mult(i(i(op_c)),mult(mult(op_c,mult(op_d,op_c)),A)),
inference(paramod,[status(thm)],[c_10,c_11152]) ).
cnf(c_11154,plain,
mult(rd(op_c,mult(i(op_d),op_c)),mult(i(op_c),A)) = mult(i(i(op_c)),mult(mult(op_c,mult(op_d,op_c)),A)),
inference(paramod,[status(thm)],[c_38,c_11153]) ).
cnf(c_11155,plain,
mult(i(i(op_d)),mult(i(op_c),A)) = mult(i(i(op_c)),mult(mult(op_c,mult(op_d,op_c)),A)),
inference(paramod,[status(thm)],[c_32,c_11154]) ).
cnf(c_11156,plain,
mult(op_d,mult(i(op_c),A)) = mult(i(i(op_c)),mult(mult(op_c,mult(op_d,op_c)),A)),
inference(paramod,[status(thm)],[c_38,c_11155]) ).
cnf(c_11157,plain,
mult(op_d,mult(i(op_c),A)) = mult(op_c,mult(mult(op_c,mult(op_d,op_c)),A)),
inference(paramod,[status(thm)],[c_38,c_11156]) ).
cnf(c_11158,plain,
mult(op_d,mult(i(op_c),A)) = mult(op_c,mult(op_c,mult(op_d,mult(op_c,A)))),
inference(paramod,[status(thm)],[c_8,c_11157]) ).
cnf(c_6000,plain,
mult(op_c,mult(op_c,mult(op_d,mult(op_c,A)))) = mult(op_d,mult(i(op_c),A)),
inference(copy,[status(thm)],[c_11158]) ).
cnf(c_11159,plain,
rd(mult(op_d,i(op_c)),mult(i(op_c),mult(op_c,mult(op_d,op_c)))) = mult(i(i(op_c)),i(i(op_c))),
inference(paramod,[status(thm)],[c_3655,c_119]) ).
cnf(c_11160,plain,
rd(mult(op_d,i(op_c)),mult(op_d,op_c)) = mult(i(i(op_c)),i(i(op_c))),
inference(paramod,[status(thm)],[c_9,c_11159]) ).
cnf(c_11161,plain,
rd(mult(op_d,i(op_c)),mult(op_d,op_c)) = mult(op_c,i(i(op_c))),
inference(paramod,[status(thm)],[c_38,c_11160]) ).
cnf(c_6003,plain,
rd(mult(op_d,i(op_c)),mult(op_d,op_c)) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_38,c_11161]) ).
cnf(c_11162,plain,
mult(mult(op_d,mult(i(op_c),mult(i(op_c),op_d))),i(op_c)) = mult(op_d,mult(i(op_c),mult(op_c,mult(op_d,op_c)))),
inference(paramod,[status(thm)],[c_3655,c_116]) ).
cnf(c_11163,plain,
mult(mult(op_d,mult(op_c,mult(op_c,op_d))),i(op_c)) = mult(op_d,mult(i(op_c),mult(op_c,mult(op_d,op_c)))),
inference(paramod,[status(thm)],[c_127,c_11162]) ).
cnf(c_11164,plain,
mult(mult(op_c,mult(op_c,i(op_d))),i(op_c)) = mult(op_d,mult(i(op_c),mult(op_c,mult(op_d,op_c)))),
inference(paramod,[status(thm)],[c_2142,c_11163]) ).
cnf(c_11165,plain,
mult(op_c,rd(mult(op_c,i(op_d)),op_c)) = mult(op_d,mult(i(op_c),mult(op_c,mult(op_d,op_c)))),
inference(paramod,[status(thm)],[c_1101,c_11164]) ).
cnf(c_11166,plain,
mult(op_c,rd(i(op_c),mult(i(op_c),i(i(op_d))))) = mult(op_d,mult(i(op_c),mult(op_c,mult(op_d,op_c)))),
inference(paramod,[status(thm)],[c_4951,c_11165]) ).
cnf(c_11167,plain,
mult(op_c,rd(i(op_c),mult(i(op_c),op_d))) = mult(op_d,mult(i(op_c),mult(op_c,mult(op_d,op_c)))),
inference(paramod,[status(thm)],[c_38,c_11166]) ).
cnf(c_11168,plain,
mult(op_c,rd(op_c,mult(op_c,op_d))) = mult(op_d,mult(i(op_c),mult(op_c,mult(op_d,op_c)))),
inference(paramod,[status(thm)],[c_4949,c_11167]) ).
cnf(c_11169,plain,
mult(op_c,rd(op_c,mult(op_c,op_d))) = mult(op_d,mult(op_d,op_c)),
inference(paramod,[status(thm)],[c_9,c_11168]) ).
cnf(c_6016,plain,
mult(op_c,rd(op_c,mult(op_c,op_d))) = mult(i(op_d),op_c),
inference(paramod,[status(thm)],[c_68,c_11169]) ).
cnf(c_11170,plain,
rd(mult(op_d,mult(i(op_c),mult(op_c,mult(op_d,op_c)))),i(op_c)) = mult(op_d,mult(i(op_c),mult(i(op_c),op_d))),
inference(paramod,[status(thm)],[c_3655,c_120]) ).
cnf(c_11171,plain,
rd(mult(op_d,mult(op_d,op_c)),i(op_c)) = mult(op_d,mult(i(op_c),mult(i(op_c),op_d))),
inference(paramod,[status(thm)],[c_9,c_11170]) ).
cnf(c_11172,plain,
rd(mult(i(op_d),op_c),i(op_c)) = mult(op_d,mult(i(op_c),mult(i(op_c),op_d))),
inference(paramod,[status(thm)],[c_68,c_11171]) ).
cnf(c_11173,plain,
rd(op_c,i(mult(i(op_d),op_c))) = mult(op_d,mult(i(op_c),mult(i(op_c),op_d))),
inference(paramod,[status(thm)],[c_102,c_11172]) ).
cnf(c_11174,plain,
rd(op_c,mult(i(i(op_d)),i(op_c))) = mult(op_d,mult(i(op_c),mult(i(op_c),op_d))),
inference(paramod,[status(thm)],[c_10,c_11173]) ).
cnf(c_11175,plain,
rd(op_c,mult(op_d,i(op_c))) = mult(op_d,mult(i(op_c),mult(i(op_c),op_d))),
inference(paramod,[status(thm)],[c_38,c_11174]) ).
cnf(c_11176,plain,
rd(op_c,mult(op_d,i(op_c))) = mult(op_d,mult(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_127,c_11175]) ).
cnf(c_6018,plain,
rd(op_c,mult(op_d,i(op_c))) = mult(op_c,mult(op_c,i(op_d))),
inference(paramod,[status(thm)],[c_2142,c_11176]) ).
cnf(c_11177,plain,
mult(mult(i(op_c),mult(op_d,mult(i(op_c),mult(op_c,mult(op_d,op_c))))),A) = mult(i(op_c),mult(op_d,mult(i(op_c),mult(i(op_c),mult(op_d,mult(i(op_c),A)))))),
inference(paramod,[status(thm)],[c_3655,c_147]) ).
cnf(c_11178,plain,
mult(mult(i(op_c),mult(op_d,mult(op_d,op_c))),A) = mult(i(op_c),mult(op_d,mult(i(op_c),mult(i(op_c),mult(op_d,mult(i(op_c),A)))))),
inference(paramod,[status(thm)],[c_9,c_11177]) ).
cnf(c_11179,plain,
mult(mult(i(op_c),mult(i(op_d),op_c)),A) = mult(i(op_c),mult(op_d,mult(i(op_c),mult(i(op_c),mult(op_d,mult(i(op_c),A)))))),
inference(paramod,[status(thm)],[c_68,c_11178]) ).
cnf(c_11180,plain,
mult(mult(i(op_c),mult(i(op_d),op_c)),A) = mult(i(op_c),mult(op_d,mult(i(op_c),mult(op_c,mult(op_d,mult(op_c,A)))))),
inference(paramod,[status(thm)],[c_5987,c_11179]) ).
cnf(c_11181,plain,
mult(mult(i(op_c),mult(i(op_d),op_c)),A) = mult(i(op_c),mult(op_d,mult(op_d,mult(op_c,A)))),
inference(paramod,[status(thm)],[c_9,c_11180]) ).
cnf(c_6022,plain,
mult(mult(i(op_c),mult(i(op_d),op_c)),A) = mult(i(op_c),mult(i(op_d),mult(op_c,A))),
inference(paramod,[status(thm)],[c_68,c_11181]) ).
cnf(c_11182,plain,
rd(i(mult(op_d,op_c)),i(mult(op_d,i(op_c)))) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_6003,c_90]) ).
cnf(c_11183,plain,
rd(mult(i(op_d),i(op_c)),i(mult(op_d,i(op_c)))) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_10,c_11182]) ).
cnf(c_11184,plain,
rd(mult(i(op_d),i(op_c)),mult(i(op_d),i(i(op_c)))) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_10,c_11183]) ).
cnf(c_6043,plain,
rd(mult(i(op_d),i(op_c)),mult(i(op_d),op_c)) = mult(op_c,op_c),
inference(paramod,[status(thm)],[c_38,c_11184]) ).
cnf(c_11185,plain,
mult(i(op_c),mult(i(op_d),op_c)) = rd(op_c,mult(op_c,op_d)),
inference(paramod,[status(thm)],[c_6016,c_9]) ).
cnf(c_6053,plain,
rd(op_c,mult(op_c,op_d)) = mult(i(op_c),mult(i(op_d),op_c)),
inference(copy,[status(thm)],[c_11185]) ).
cnf(c_11186,plain,
rd(i(op_c),mult(i(op_d),op_c)) = mult(i(op_c),mult(i(rd(op_c,mult(op_c,op_d))),i(op_c))),
inference(paramod,[status(thm)],[c_6016,c_995]) ).
cnf(c_11187,plain,
rd(i(op_c),mult(i(op_d),op_c)) = mult(i(op_c),mult(i(mult(i(op_c),mult(i(op_d),op_c))),i(op_c))),
inference(paramod,[status(thm)],[c_6053,c_11186]) ).
cnf(c_11188,plain,
rd(i(op_c),mult(i(op_d),op_c)) = mult(i(op_c),mult(mult(i(i(op_c)),i(mult(i(op_d),op_c))),i(op_c))),
inference(paramod,[status(thm)],[c_10,c_11187]) ).
cnf(c_11189,plain,
rd(i(op_c),mult(i(op_d),op_c)) = mult(i(op_c),mult(mult(op_c,i(mult(i(op_d),op_c))),i(op_c))),
inference(paramod,[status(thm)],[c_38,c_11188]) ).
cnf(c_11190,plain,
rd(i(op_c),mult(i(op_d),op_c)) = mult(i(op_c),mult(mult(op_c,mult(i(i(op_d)),i(op_c))),i(op_c))),
inference(paramod,[status(thm)],[c_10,c_11189]) ).
cnf(c_11191,plain,
rd(i(op_c),mult(i(op_d),op_c)) = mult(i(op_c),mult(mult(op_c,mult(op_d,i(op_c))),i(op_c))),
inference(paramod,[status(thm)],[c_38,c_11190]) ).
cnf(c_11192,plain,
rd(i(op_c),mult(i(op_d),op_c)) = mult(i(op_c),mult(op_c,rd(mult(op_d,i(op_c)),op_c))),
inference(paramod,[status(thm)],[c_1101,c_11191]) ).
cnf(c_11193,plain,
rd(i(op_c),mult(i(op_d),op_c)) = rd(mult(op_d,i(op_c)),op_c),
inference(paramod,[status(thm)],[c_9,c_11192]) ).
cnf(c_6063,plain,
rd(mult(op_d,i(op_c)),op_c) = rd(i(op_c),mult(i(op_d),op_c)),
inference(copy,[status(thm)],[c_11193]) ).
cnf(c_11194,plain,
mult(mult(op_d,A),mult(op_d,mult(i(i(op_d)),mult(op_d,mult(mult(op_d,A),B))))) = mult(mult(mult(op_d,A),mult(op_d,A)),B),
inference(paramod,[status(thm)],[c_9,c_148]) ).
cnf(c_11195,plain,
mult(mult(op_d,A),mult(op_d,mult(op_d,mult(op_d,mult(mult(op_d,A),B))))) = mult(mult(mult(op_d,A),mult(op_d,A)),B),
inference(paramod,[status(thm)],[c_38,c_11194]) ).
cnf(c_11196,plain,
mult(mult(op_d,A),mult(op_d,mult(i(op_d),mult(mult(op_d,A),B)))) = mult(mult(mult(op_d,A),mult(op_d,A)),B),
inference(paramod,[status(thm)],[c_68,c_11195]) ).
cnf(c_11197,plain,
mult(mult(op_d,A),mult(mult(op_d,A),B)) = mult(mult(mult(op_d,A),mult(op_d,A)),B),
inference(paramod,[status(thm)],[c_39,c_11196]) ).
cnf(c_11198,plain,
mult(mult(op_d,A),mult(mult(op_d,A),B)) = mult(mult(op_d,mult(A,mult(A,op_d))),B),
inference(paramod,[status(thm)],[c_1992,c_11197]) ).
cnf(c_6070,plain,
mult(mult(op_d,A),mult(mult(op_d,A),B)) = mult(op_d,mult(A,mult(A,mult(op_d,B)))),
inference(paramod,[status(thm)],[c_116,c_11198]) ).
cnf(c_11199,plain,
i(rd(op_c,mult(op_d,i(op_c)))) = rd(i(op_c),mult(i(op_d),op_c)),
inference(paramod,[status(thm)],[c_6063,c_79]) ).
cnf(c_11200,plain,
i(mult(op_c,mult(op_c,i(op_d)))) = rd(i(op_c),mult(i(op_d),op_c)),
inference(paramod,[status(thm)],[c_6018,c_11199]) ).
cnf(c_11201,plain,
mult(i(op_c),i(mult(op_c,i(op_d)))) = rd(i(op_c),mult(i(op_d),op_c)),
inference(paramod,[status(thm)],[c_10,c_11200]) ).
cnf(c_11202,plain,
mult(i(op_c),mult(i(op_c),i(i(op_d)))) = rd(i(op_c),mult(i(op_d),op_c)),
inference(paramod,[status(thm)],[c_10,c_11201]) ).
cnf(c_11203,plain,
mult(i(op_c),mult(i(op_c),op_d)) = rd(i(op_c),mult(i(op_d),op_c)),
inference(paramod,[status(thm)],[c_38,c_11202]) ).
cnf(c_11204,plain,
mult(op_c,mult(op_c,op_d)) = rd(i(op_c),mult(i(op_d),op_c)),
inference(paramod,[status(thm)],[c_127,c_11203]) ).
cnf(c_6116,plain,
rd(i(op_c),mult(i(op_d),op_c)) = mult(op_c,mult(op_c,op_d)),
inference(copy,[status(thm)],[c_11204]) ).
cnf(c_11205,plain,
mult(rd(i(op_c),mult(i(op_d),op_c)),i(op_d)) = mult(op_d,rd(i(op_c),mult(op_d,op_c))),
inference(paramod,[status(thm)],[c_6063,c_2016]) ).
cnf(c_11206,plain,
mult(mult(op_c,mult(op_c,op_d)),i(op_d)) = mult(op_d,rd(i(op_c),mult(op_d,op_c))),
inference(paramod,[status(thm)],[c_6116,c_11205]) ).
cnf(c_11207,plain,
mult(op_c,op_c) = mult(op_d,rd(i(op_c),mult(op_d,op_c))),
inference(paramod,[status(thm)],[c_2159,c_11206]) ).
cnf(c_6120,plain,
mult(op_d,rd(i(op_c),mult(op_d,op_c))) = mult(op_c,op_c),
inference(copy,[status(thm)],[c_11207]) ).
cnf(c_11208,plain,
rd(rd(op_c,mult(op_d,i(op_c))),mult(op_d,i(op_c))) = rd(i(mult(op_d,i(op_c))),rd(i(op_c),mult(i(op_d),op_c))),
inference(paramod,[status(thm)],[c_6063,c_2768]) ).
cnf(c_11209,plain,
rd(mult(op_c,mult(op_c,i(op_d))),mult(op_d,i(op_c))) = rd(i(mult(op_d,i(op_c))),rd(i(op_c),mult(i(op_d),op_c))),
inference(paramod,[status(thm)],[c_6018,c_11208]) ).
cnf(c_11210,plain,
rd(mult(op_c,mult(op_c,i(op_d))),mult(op_d,i(op_c))) = rd(mult(i(op_d),i(i(op_c))),rd(i(op_c),mult(i(op_d),op_c))),
inference(paramod,[status(thm)],[c_10,c_11209]) ).
cnf(c_11211,plain,
rd(mult(op_c,mult(op_c,i(op_d))),mult(op_d,i(op_c))) = rd(mult(i(op_d),op_c),rd(i(op_c),mult(i(op_d),op_c))),
inference(paramod,[status(thm)],[c_38,c_11210]) ).
cnf(c_6121,plain,
rd(mult(op_c,mult(op_c,i(op_d))),mult(op_d,i(op_c))) = rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_6116,c_11211]) ).
cnf(c_11212,plain,
mult(i(op_d),mult(op_c,op_c)) = rd(i(op_c),mult(op_d,op_c)),
inference(paramod,[status(thm)],[c_6120,c_9]) ).
cnf(c_11213,plain,
mult(op_c,mult(op_c,i(op_d))) = rd(i(op_c),mult(op_d,op_c)),
inference(paramod,[status(thm)],[c_2586,c_11212]) ).
cnf(c_6128,plain,
rd(i(op_c),mult(op_d,op_c)) = mult(op_c,mult(op_c,i(op_d))),
inference(copy,[status(thm)],[c_11213]) ).
cnf(c_11214,plain,
mult(op_c,mult(op_d,mult(mult(op_c,op_c),mult(op_d,mult(op_c,A))))) = mult(mult(op_c,mult(op_d,i(mult(i(op_d),op_c)))),A),
inference(paramod,[status(thm)],[c_6043,c_150]) ).
cnf(c_11215,plain,
mult(op_c,mult(op_d,mult(op_c,mult(op_c,mult(op_d,mult(op_c,A)))))) = mult(mult(op_c,mult(op_d,i(mult(i(op_d),op_c)))),A),
inference(paramod,[status(thm)],[c_26,c_11214]) ).
cnf(c_11216,plain,
mult(op_c,mult(op_d,mult(op_d,mult(i(op_c),A)))) = mult(mult(op_c,mult(op_d,i(mult(i(op_d),op_c)))),A),
inference(paramod,[status(thm)],[c_6000,c_11215]) ).
cnf(c_11217,plain,
mult(op_c,mult(i(op_d),mult(i(op_c),A))) = mult(mult(op_c,mult(op_d,i(mult(i(op_d),op_c)))),A),
inference(paramod,[status(thm)],[c_68,c_11216]) ).
cnf(c_11218,plain,
mult(op_c,mult(i(op_d),mult(i(op_c),A))) = mult(mult(op_c,mult(op_d,mult(i(i(op_d)),i(op_c)))),A),
inference(paramod,[status(thm)],[c_10,c_11217]) ).
cnf(c_11219,plain,
mult(op_c,mult(i(op_d),mult(i(op_c),A))) = mult(mult(op_c,mult(op_d,mult(op_d,i(op_c)))),A),
inference(paramod,[status(thm)],[c_38,c_11218]) ).
cnf(c_11220,plain,
mult(op_c,mult(i(op_d),mult(i(op_c),A))) = mult(mult(op_c,mult(i(op_d),i(op_c))),A),
inference(paramod,[status(thm)],[c_68,c_11219]) ).
cnf(c_6276,plain,
mult(mult(op_c,mult(i(op_d),i(op_c))),A) = mult(op_c,mult(i(op_d),mult(i(op_c),A))),
inference(copy,[status(thm)],[c_11220]) ).
cnf(c_11221,plain,
i(mult(i(op_c),mult(i(op_d),op_c))) = rd(mult(op_c,op_d),op_c),
inference(paramod,[status(thm)],[c_6053,c_79]) ).
cnf(c_11222,plain,
mult(i(i(op_c)),i(mult(i(op_d),op_c))) = rd(mult(op_c,op_d),op_c),
inference(paramod,[status(thm)],[c_10,c_11221]) ).
cnf(c_11223,plain,
mult(op_c,i(mult(i(op_d),op_c))) = rd(mult(op_c,op_d),op_c),
inference(paramod,[status(thm)],[c_38,c_11222]) ).
cnf(c_11224,plain,
mult(op_c,mult(i(i(op_d)),i(op_c))) = rd(mult(op_c,op_d),op_c),
inference(paramod,[status(thm)],[c_10,c_11223]) ).
cnf(c_11225,plain,
mult(op_c,mult(op_d,i(op_c))) = rd(mult(op_c,op_d),op_c),
inference(paramod,[status(thm)],[c_38,c_11224]) ).
cnf(c_11226,plain,
mult(op_c,mult(op_d,i(op_c))) = rd(i(op_c),mult(i(op_c),i(op_d))),
inference(paramod,[status(thm)],[c_4951,c_11225]) ).
cnf(c_6285,plain,
rd(i(op_c),mult(i(op_c),i(op_d))) = mult(op_c,mult(op_d,i(op_c))),
inference(copy,[status(thm)],[c_11226]) ).
cnf(c_11227,plain,
rd(i(op_c),mult(mult(i(op_c),mult(i(op_d),op_c)),i(mult(op_c,op_d)))) = mult(rd(mult(op_c,op_d),op_c),rd(mult(op_c,op_d),op_c)),
inference(paramod,[status(thm)],[c_6053,c_230]) ).
cnf(c_11228,plain,
rd(i(op_c),mult(mult(i(op_c),mult(i(op_d),op_c)),mult(i(op_c),i(op_d)))) = mult(rd(mult(op_c,op_d),op_c),rd(mult(op_c,op_d),op_c)),
inference(paramod,[status(thm)],[c_10,c_11227]) ).
cnf(c_11229,plain,
rd(i(op_c),mult(i(op_c),mult(i(op_d),mult(op_c,mult(i(op_c),i(op_d)))))) = mult(rd(mult(op_c,op_d),op_c),rd(mult(op_c,op_d),op_c)),
inference(paramod,[status(thm)],[c_6022,c_11228]) ).
cnf(c_11230,plain,
rd(i(op_c),mult(i(op_c),mult(i(op_d),i(op_d)))) = mult(rd(mult(op_c,op_d),op_c),rd(mult(op_c,op_d),op_c)),
inference(paramod,[status(thm)],[c_39,c_11229]) ).
cnf(c_11231,plain,
rd(i(op_c),mult(i(op_c),op_d)) = mult(rd(mult(op_c,op_d),op_c),rd(mult(op_c,op_d),op_c)),
inference(paramod,[status(thm)],[c_56,c_11230]) ).
cnf(c_11232,plain,
rd(i(op_c),mult(i(op_c),op_d)) = mult(rd(i(op_c),mult(i(op_c),i(op_d))),rd(mult(op_c,op_d),op_c)),
inference(paramod,[status(thm)],[c_4951,c_11231]) ).
cnf(c_11233,plain,
rd(i(op_c),mult(i(op_c),op_d)) = mult(mult(op_c,mult(op_d,i(op_c))),rd(mult(op_c,op_d),op_c)),
inference(paramod,[status(thm)],[c_6285,c_11232]) ).
cnf(c_11234,plain,
rd(i(op_c),mult(i(op_c),op_d)) = mult(mult(op_c,mult(op_d,i(op_c))),rd(i(op_c),mult(i(op_c),i(op_d)))),
inference(paramod,[status(thm)],[c_4951,c_11233]) ).
cnf(c_11235,plain,
rd(i(op_c),mult(i(op_c),op_d)) = mult(mult(op_c,mult(op_d,i(op_c))),mult(op_c,mult(op_d,i(op_c)))),
inference(paramod,[status(thm)],[c_6285,c_11234]) ).
cnf(c_11236,plain,
rd(i(op_c),mult(i(op_c),op_d)) = mult(op_c,mult(mult(op_d,i(op_c)),mult(mult(op_d,i(op_c)),op_c))),
inference(paramod,[status(thm)],[c_1992,c_11235]) ).
cnf(c_11237,plain,
rd(i(op_c),mult(i(op_c),op_d)) = mult(op_c,mult(op_d,mult(i(op_c),mult(i(op_c),mult(op_d,op_c))))),
inference(paramod,[status(thm)],[c_6070,c_11236]) ).
cnf(c_11238,plain,
rd(i(op_c),mult(i(op_c),op_d)) = mult(op_c,mult(op_d,mult(op_c,mult(op_c,mult(op_d,op_c))))),
inference(paramod,[status(thm)],[c_127,c_11237]) ).
cnf(c_11239,plain,
rd(i(op_c),mult(i(op_c),op_d)) = mult(op_c,mult(op_d,mult(op_d,i(op_c)))),
inference(paramod,[status(thm)],[c_5988,c_11238]) ).
cnf(c_6300,plain,
rd(i(op_c),mult(i(op_c),op_d)) = mult(op_c,mult(i(op_d),i(op_c))),
inference(paramod,[status(thm)],[c_68,c_11239]) ).
cnf(c_11240,plain,
mult(mult(op_c,mult(op_c,op_d)),rd(mult(i(op_d),op_c),rd(i(op_c),mult(i(op_d),op_c)))) = mult(i(op_c),rd(mult(i(op_d),op_c),i(op_c))),
inference(paramod,[status(thm)],[c_6116,c_1141]) ).
cnf(c_11241,plain,
mult(mult(op_c,mult(op_c,op_d)),rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d)))) = mult(i(op_c),rd(mult(i(op_d),op_c),i(op_c))),
inference(paramod,[status(thm)],[c_6116,c_11240]) ).
cnf(c_11242,plain,
mult(mult(op_c,mult(op_c,op_d)),rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d)))) = mult(i(op_c),rd(op_c,i(mult(i(op_d),op_c)))),
inference(paramod,[status(thm)],[c_102,c_11241]) ).
cnf(c_11243,plain,
mult(mult(op_c,mult(op_c,op_d)),rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d)))) = mult(i(op_c),rd(op_c,mult(i(i(op_d)),i(op_c)))),
inference(paramod,[status(thm)],[c_10,c_11242]) ).
cnf(c_11244,plain,
mult(mult(op_c,mult(op_c,op_d)),rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d)))) = mult(i(op_c),rd(op_c,mult(op_d,i(op_c)))),
inference(paramod,[status(thm)],[c_38,c_11243]) ).
cnf(c_11245,plain,
mult(mult(op_c,mult(op_c,op_d)),rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d)))) = mult(i(op_c),mult(op_c,mult(op_c,i(op_d)))),
inference(paramod,[status(thm)],[c_6018,c_11244]) ).
cnf(c_6326,plain,
mult(mult(op_c,mult(op_c,op_d)),rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d)))) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_9,c_11245]) ).
cnf(c_11246,plain,
i(mult(op_c,mult(op_c,i(op_d)))) = rd(mult(op_d,op_c),i(op_c)),
inference(paramod,[status(thm)],[c_6128,c_79]) ).
cnf(c_11247,plain,
mult(i(op_c),i(mult(op_c,i(op_d)))) = rd(mult(op_d,op_c),i(op_c)),
inference(paramod,[status(thm)],[c_10,c_11246]) ).
cnf(c_11248,plain,
mult(i(op_c),mult(i(op_c),i(i(op_d)))) = rd(mult(op_d,op_c),i(op_c)),
inference(paramod,[status(thm)],[c_10,c_11247]) ).
cnf(c_11249,plain,
mult(i(op_c),mult(i(op_c),op_d)) = rd(mult(op_d,op_c),i(op_c)),
inference(paramod,[status(thm)],[c_38,c_11248]) ).
cnf(c_11250,plain,
mult(op_c,mult(op_c,op_d)) = rd(mult(op_d,op_c),i(op_c)),
inference(paramod,[status(thm)],[c_127,c_11249]) ).
cnf(c_11251,plain,
mult(op_c,mult(op_c,op_d)) = rd(op_c,i(mult(op_d,op_c))),
inference(paramod,[status(thm)],[c_102,c_11250]) ).
cnf(c_11252,plain,
mult(op_c,mult(op_c,op_d)) = rd(op_c,mult(i(op_d),i(op_c))),
inference(paramod,[status(thm)],[c_10,c_11251]) ).
cnf(c_6328,plain,
rd(op_c,mult(i(op_d),i(op_c))) = mult(op_c,mult(op_c,op_d)),
inference(copy,[status(thm)],[c_11252]) ).
cnf(c_11253,plain,
mult(mult(op_c,mult(op_c,i(op_d))),rd(mult(op_d,op_c),rd(i(op_c),mult(op_d,op_c)))) = mult(i(op_c),rd(mult(op_d,op_c),i(op_c))),
inference(paramod,[status(thm)],[c_6128,c_1141]) ).
cnf(c_11254,plain,
mult(mult(op_c,mult(op_c,i(op_d))),rd(mult(op_d,op_c),mult(op_c,mult(op_c,i(op_d))))) = mult(i(op_c),rd(mult(op_d,op_c),i(op_c))),
inference(paramod,[status(thm)],[c_6128,c_11253]) ).
cnf(c_11255,plain,
mult(mult(op_c,mult(op_c,i(op_d))),rd(mult(op_d,op_c),mult(op_c,mult(op_c,i(op_d))))) = mult(i(op_c),rd(op_c,i(mult(op_d,op_c)))),
inference(paramod,[status(thm)],[c_102,c_11254]) ).
cnf(c_11256,plain,
mult(mult(op_c,mult(op_c,i(op_d))),rd(mult(op_d,op_c),mult(op_c,mult(op_c,i(op_d))))) = mult(i(op_c),rd(op_c,mult(i(op_d),i(op_c)))),
inference(paramod,[status(thm)],[c_10,c_11255]) ).
cnf(c_11257,plain,
mult(mult(op_c,mult(op_c,i(op_d))),rd(mult(op_d,op_c),mult(op_c,mult(op_c,i(op_d))))) = mult(i(op_c),mult(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_6328,c_11256]) ).
cnf(c_6334,plain,
mult(mult(op_c,mult(op_c,i(op_d))),rd(mult(op_d,op_c),mult(op_c,mult(op_c,i(op_d))))) = mult(op_c,op_d),
inference(paramod,[status(thm)],[c_9,c_11257]) ).
cnf(c_11258,plain,
mult(mult(op_c,mult(op_c,op_c)),mult(op_d,op_c)) = mult(op_c,mult(op_d,i(op_c))),
inference(paramod,[status(thm)],[c_5988,c_8]) ).
cnf(c_6405,plain,
mult(i(op_c),mult(op_d,op_c)) = mult(op_c,mult(op_d,i(op_c))),
inference(paramod,[status(thm)],[c_45,c_11258]) ).
cnf(c_11259,plain,
rd(rd(mult(op_c,rd(op_c,op_d)),mult(rd(op_d,op_c),op_d)),mult(i(A),i(B))) = rd(mult(A,B),op_c),
inference(paramod,[status(thm)],[c_3686,c_153]) ).
cnf(c_11260,plain,
rd(i(op_c),mult(i(A),i(B))) = rd(mult(A,B),op_c),
inference(paramod,[status(thm)],[c_3683,c_11259]) ).
cnf(c_6721,plain,
rd(mult(A,B),op_c) = rd(i(op_c),mult(i(A),i(B))),
inference(copy,[status(thm)],[c_11260]) ).
cnf(c_11261,plain,
i(mult(op_c,mult(i(op_d),i(op_c)))) = rd(mult(i(op_c),op_d),i(op_c)),
inference(paramod,[status(thm)],[c_6300,c_79]) ).
cnf(c_11262,plain,
mult(i(op_c),i(mult(i(op_d),i(op_c)))) = rd(mult(i(op_c),op_d),i(op_c)),
inference(paramod,[status(thm)],[c_10,c_11261]) ).
cnf(c_11263,plain,
mult(i(op_c),mult(i(i(op_d)),i(i(op_c)))) = rd(mult(i(op_c),op_d),i(op_c)),
inference(paramod,[status(thm)],[c_10,c_11262]) ).
cnf(c_11264,plain,
mult(i(op_c),mult(op_d,i(i(op_c)))) = rd(mult(i(op_c),op_d),i(op_c)),
inference(paramod,[status(thm)],[c_38,c_11263]) ).
cnf(c_11265,plain,
mult(i(op_c),mult(op_d,op_c)) = rd(mult(i(op_c),op_d),i(op_c)),
inference(paramod,[status(thm)],[c_38,c_11264]) ).
cnf(c_11266,plain,
mult(op_c,mult(op_d,i(op_c))) = rd(mult(i(op_c),op_d),i(op_c)),
inference(paramod,[status(thm)],[c_6405,c_11265]) ).
cnf(c_11267,plain,
mult(op_c,mult(op_d,i(op_c))) = rd(op_c,i(mult(i(op_c),op_d))),
inference(paramod,[status(thm)],[c_102,c_11266]) ).
cnf(c_11268,plain,
mult(op_c,mult(op_d,i(op_c))) = rd(op_c,mult(i(i(op_c)),i(op_d))),
inference(paramod,[status(thm)],[c_10,c_11267]) ).
cnf(c_11269,plain,
mult(op_c,mult(op_d,i(op_c))) = rd(op_c,mult(op_c,i(op_d))),
inference(paramod,[status(thm)],[c_38,c_11268]) ).
cnf(c_7087,plain,
rd(op_c,mult(op_c,i(op_d))) = mult(op_c,mult(op_d,i(op_c))),
inference(copy,[status(thm)],[c_11269]) ).
cnf(c_11270,plain,
rd(mult(op_c,mult(op_c,i(op_d))),mult(i(i(op_d)),A)) = mult(i(op_d),mult(rd(mult(op_c,op_c),A),i(op_d))),
inference(paramod,[status(thm)],[c_2586,c_1989]) ).
cnf(c_9198,plain,
rd(mult(op_c,mult(op_c,i(op_d))),mult(op_d,A)) = mult(i(op_d),mult(rd(mult(op_c,op_c),A),i(op_d))),
inference(paramod,[status(thm)],[c_38,c_11270]) ).
cnf(c_9199,plain,
rd(mult(op_d,A),mult(op_c,mult(op_c,i(op_d)))) = mult(op_d,mult(rd(A,mult(op_c,op_c)),op_d)),
inference(paramod,[status(thm)],[c_2586,c_1989]) ).
cnf(c_11271,plain,
mult(i(op_d),mult(rd(mult(op_c,op_c),i(op_c)),i(op_d))) = rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_9198,c_6121]) ).
cnf(c_11272,plain,
mult(i(op_d),mult(rd(op_c,i(mult(op_c,op_c))),i(op_d))) = rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_102,c_11271]) ).
cnf(c_11273,plain,
mult(i(op_d),mult(rd(op_c,mult(i(op_c),i(op_c))),i(op_d))) = rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_10,c_11272]) ).
cnf(c_11274,plain,
mult(i(op_d),mult(rd(op_c,mult(op_c,op_c)),i(op_d))) = rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_124,c_11273]) ).
cnf(c_11275,plain,
mult(i(op_d),mult(i(op_c),i(op_d))) = rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d))),
inference(paramod,[status(thm)],[c_32,c_11274]) ).
cnf(c_9269,plain,
rd(mult(i(op_d),op_c),mult(op_c,mult(op_c,op_d))) = mult(i(op_d),mult(i(op_c),i(op_d))),
inference(copy,[status(thm)],[c_11275]) ).
cnf(c_11276,plain,
mult(mult(op_c,mult(op_c,i(op_d))),mult(op_d,mult(rd(op_c,mult(op_c,op_c)),op_d))) = mult(op_c,op_d),
inference(paramod,[status(thm)],[c_9199,c_6334]) ).
cnf(c_11277,plain,
mult(mult(op_c,mult(op_c,i(op_d))),mult(op_d,mult(i(op_c),op_d))) = mult(op_c,op_d),
inference(paramod,[status(thm)],[c_32,c_11276]) ).
cnf(c_11278,plain,
mult(i(op_d),mult(mult(op_c,mult(op_c,op_d)),mult(i(op_c),op_d))) = mult(op_c,op_d),
inference(paramod,[status(thm)],[c_3665,c_11277]) ).
cnf(c_11279,plain,
mult(i(op_d),mult(op_c,mult(rd(mult(op_c,op_d),op_c),op_d))) = mult(op_c,op_d),
inference(paramod,[status(thm)],[c_827,c_11278]) ).
cnf(c_11280,plain,
mult(i(op_d),mult(op_c,mult(rd(i(op_c),mult(i(op_c),i(op_d))),op_d))) = mult(op_c,op_d),
inference(paramod,[status(thm)],[c_6721,c_11279]) ).
cnf(c_9270,plain,
mult(i(op_d),mult(op_c,mult(mult(op_c,mult(op_d,i(op_c))),op_d))) = mult(op_c,op_d),
inference(paramod,[status(thm)],[c_6285,c_11280]) ).
cnf(c_11281,plain,
mult(mult(op_c,mult(op_c,op_d)),mult(i(op_d),mult(i(op_c),i(op_d)))) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_9269,c_6326]) ).
cnf(c_11282,plain,
mult(op_d,mult(mult(op_c,mult(op_c,i(op_d))),mult(i(op_c),i(op_d)))) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_5796,c_11281]) ).
cnf(c_11283,plain,
mult(op_d,mult(op_c,mult(rd(mult(op_c,i(op_d)),op_c),i(op_d)))) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_827,c_11282]) ).
cnf(c_11284,plain,
mult(op_d,mult(op_c,mult(rd(i(op_c),mult(i(op_c),i(i(op_d)))),i(op_d)))) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_6721,c_11283]) ).
cnf(c_11285,plain,
mult(op_d,mult(op_c,mult(rd(i(op_c),mult(i(op_c),op_d)),i(op_d)))) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_38,c_11284]) ).
cnf(c_11286,plain,
mult(op_d,mult(op_c,mult(mult(op_c,mult(i(op_d),i(op_c))),i(op_d)))) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_6300,c_11285]) ).
cnf(c_9275,plain,
mult(op_d,mult(op_c,mult(op_c,mult(i(op_d),mult(i(op_c),i(op_d)))))) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_6276,c_11286]) ).
cnf(c_11287,plain,
rd(mult(i(op_d),A),mult(A,mult(A,op_d))) = i(rd(A,op_d)),
inference(paramod,[status(thm)],[c_2897,c_32]) ).
cnf(c_10187,plain,
rd(mult(i(op_d),A),mult(A,mult(A,op_d))) = rd(op_d,A),
inference(paramod,[status(thm)],[c_79,c_11287]) ).
cnf(c_11288,plain,
rd(op_d,op_c) = mult(i(op_d),mult(i(op_c),i(op_d))),
inference(paramod,[status(thm)],[c_10187,c_9269]) ).
cnf(c_10243,plain,
mult(i(op_d),mult(i(op_c),i(op_d))) = rd(op_d,op_c),
inference(copy,[status(thm)],[c_11288]) ).
cnf(c_11289,plain,
mult(op_d,mult(op_c,mult(op_c,rd(op_d,op_c)))) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_10243,c_9275]) ).
cnf(c_11290,plain,
mult(op_d,mult(rd(op_c,op_d),i(op_d))) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_2910,c_11289]) ).
cnf(c_10244,plain,
mult(mult(op_d,op_c),op_d) = mult(op_c,i(op_d)),
inference(paramod,[status(thm)],[c_67,c_11290]) ).
cnf(c_11291,plain,
mult(rd(op_c,op_d),mult(op_d,op_d)) = mult(i(op_d),mult(op_c,i(op_d))),
inference(paramod,[status(thm)],[c_10244,c_65]) ).
cnf(c_10255,plain,
mult(rd(op_c,op_d),i(op_d)) = mult(i(op_d),mult(op_c,i(op_d))),
inference(paramod,[status(thm)],[c_52,c_11291]) ).
cnf(c_11292,plain,
i(rd(op_d,op_c)) = mult(i(i(op_d)),i(mult(i(op_c),i(op_d)))),
inference(paramod,[status(thm)],[c_10243,c_10]) ).
cnf(c_11293,plain,
rd(op_c,op_d) = mult(i(i(op_d)),i(mult(i(op_c),i(op_d)))),
inference(paramod,[status(thm)],[c_79,c_11292]) ).
cnf(c_11294,plain,
rd(op_c,op_d) = mult(op_d,i(mult(i(op_c),i(op_d)))),
inference(paramod,[status(thm)],[c_38,c_11293]) ).
cnf(c_11295,plain,
rd(op_c,op_d) = mult(op_d,mult(i(i(op_c)),i(i(op_d)))),
inference(paramod,[status(thm)],[c_10,c_11294]) ).
cnf(c_11296,plain,
rd(op_c,op_d) = mult(op_d,mult(op_c,i(i(op_d)))),
inference(paramod,[status(thm)],[c_38,c_11295]) ).
cnf(c_11297,plain,
rd(op_c,op_d) = mult(op_d,mult(op_c,op_d)),
inference(paramod,[status(thm)],[c_38,c_11296]) ).
cnf(c_10623,plain,
mult(op_d,mult(op_c,op_d)) = rd(op_c,op_d),
inference(copy,[status(thm)],[c_11297]) ).
cnf(c_11298,plain,
mult(rd(op_c,op_d),i(op_d)) = mult(op_d,rd(mult(op_c,op_d),op_d)),
inference(paramod,[status(thm)],[c_10623,c_1101]) ).
cnf(c_11299,plain,
mult(i(op_d),mult(op_c,i(op_d))) = mult(op_d,rd(mult(op_c,op_d),op_d)),
inference(paramod,[status(thm)],[c_10255,c_11298]) ).
cnf(c_10867,plain,
mult(i(op_d),mult(op_c,i(op_d))) = mult(op_d,op_c),
inference(paramod,[status(thm)],[c_4,c_11299]) ).
cnf(c_11300,plain,
rd(mult(rd(op_c,op_d),op_d),mult(rd(mult(op_c,op_d),op_d),i(op_d))) = op_d,
inference(paramod,[status(thm)],[c_10623,c_947]) ).
cnf(c_11301,plain,
rd(op_c,mult(rd(mult(op_c,op_d),op_d),i(op_d))) = op_d,
inference(paramod,[status(thm)],[c_3,c_11300]) ).
cnf(c_11302,plain,
rd(op_c,mult(op_c,i(op_d))) = op_d,
inference(paramod,[status(thm)],[c_4,c_11301]) ).
cnf(c_10869,plain,
mult(op_c,mult(op_d,i(op_c))) = op_d,
inference(paramod,[status(thm)],[c_7087,c_11302]) ).
cnf(c_11303,plain,
mult(i(op_d),mult(op_c,mult(op_d,op_d))) = mult(op_c,op_d),
inference(paramod,[status(thm)],[c_10869,c_9270]) ).
cnf(c_11304,plain,
mult(i(op_d),mult(op_c,i(op_d))) = mult(op_c,op_d),
inference(paramod,[status(thm)],[c_52,c_11303]) ).
cnf(c_11305,plain,
mult(op_d,op_c) = mult(op_c,op_d),
inference(paramod,[status(thm)],[c_10867,c_11304]) ).
cnf(c_10920,plain,
$false,
inference(resolve,[status(thm)],[c_14,c_11305]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP688-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n004.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Fri Sep 25 15:37:06 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.44 % Process 3561613 was started by sandbox2 on n004,
% 0.16/0.44 % Fri Sep 25 15:37:06 2026
% 0.16/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.44
% 0.16/0.44 % From the command line: assign(max_seconds, 300).
% 43.95/6.76
% 43.95/6.76 % Assigning unary symbol i kb_weight 0 and highest precedence (8).
% 43.95/6.76
% 43.95/6.76 % SZS status Unsatisfiable for theBenchmark
% 43.95/6.76
% 43.95/6.76 % Proof 1 at 4.59 (+ 1.19) seconds.
% 43.95/6.76 % Length of proof is 187.
% 43.95/6.76 % Level of proof is 32.
% 43.95/6.76 % Maximum clause weight is 87.000.
% 43.95/6.76 % Given clauses 290.
% 43.95/6.76
% 43.95/6.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------