Prover9---2026-6A.THM-CRf.s

%------------------------------------------------------------------------------
% File     : Prover9---2026-6A
% Problem  : GRP654+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : prover9 -casc 300 -f /export/starexec/sandbox/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:30:54 AM UTC 2026

% Result   : Theorem 155.81s 26.30s
% Output   : CNFRefutation 155.81s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% Comments : 
%------------------------------------------------------------------------------
fof(f01,axiom,
    ! [B,A] : mult(A,ld(A,B)) = B,
    file('theBenchmark.p',f01) ).

fof(f02,axiom,
    ! [B,A] : ld(A,mult(A,B)) = B,
    file('theBenchmark.p',f02) ).

fof(f03,axiom,
    ! [B,A] : mult(rd(A,B),B) = A,
    file('theBenchmark.p',f03) ).

fof(f04,axiom,
    ! [B,A] : rd(mult(A,B),B) = A,
    file('theBenchmark.p',f04) ).

fof(f05,axiom,
    ! [C,B,A] : mult(A,mult(B,mult(A,C))) = mult(mult(mult(A,B),A),C),
    file('theBenchmark.p',f05) ).

fof(goals,conjecture,
    ! [X0,X1] :
      ( mult(ld(X1,X1),X0) = X0
      & mult(X0,ld(X1,X1)) = X0 ),
    file('theBenchmark.p',goals) ).

fof(goals_neg,negated_conjecture,
    ~ ! [X0,X1] :
        ( mult(ld(X1,X1),X0) = X0
        & mult(X0,ld(X1,X1)) = X0 ),
    inference(assume_negation,[status(cth)],[goals]) ).

cnf(c_7,plain,
    mult(A,ld(A,B)) = B,
    inference(clausify,[status(thm)],[f01]) ).

cnf(c_8,plain,
    ld(A,mult(A,B)) = B,
    inference(clausify,[status(thm)],[f02]) ).

cnf(c_9,plain,
    mult(rd(A,B),B) = A,
    inference(clausify,[status(thm)],[f03]) ).

cnf(c_10,plain,
    rd(mult(A,B),B) = A,
    inference(clausify,[status(thm)],[f04]) ).

cnf(c_11,plain,
    mult(mult(mult(A,B),A),C) = mult(A,mult(B,mult(A,C))),
    inference(clausify,[status(thm)],[f05]) ).

fof(nnf_6,plain,
    ? [X0,X1] :
      ( mult(ld(X1,X1),X0) != X0
      | mult(X0,ld(X1,X1)) != X0 ),
    inference(fof_nnf,[status(thm)],[goals_neg]) ).

fof(sk_goals_neg,plain,
    ( mult(ld(sK1,sK1),sK0) != sK0
    | mult(sK0,ld(sK1,sK1)) != sK0 ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[nnf_6]) ).

cnf(c_12,negated_conjecture,
    ( mult(ld(sK1,sK1),sK0) != sK0
    | mult(sK0,ld(sK1,sK1)) != sK0 ),
    inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).

cnf(c_13,plain,
    ld(rd(A,B),A) = B,
    inference(paramod,[status(thm)],[c_9,c_8]) ).

cnf(c_14,plain,
    rd(A,ld(B,A)) = B,
    inference(paramod,[status(thm)],[c_7,c_10]) ).

cnf(c_15,plain,
    mult(A,mult(B,mult(A,ld(mult(mult(A,B),A),C)))) = C,
    inference(paramod,[status(thm)],[c_11,c_7]) ).

cnf(c_11963,plain,
    mult(mult(A,B),C) = mult(B,mult(ld(B,A),mult(B,C))),
    inference(paramod,[status(thm)],[c_7,c_11]) ).

cnf(c_16,plain,
    mult(A,mult(ld(A,B),mult(A,C))) = mult(mult(B,A),C),
    inference(copy,[status(thm)],[c_11963]) ).

cnf(c_17,plain,
    ld(mult(mult(A,B),A),mult(A,mult(B,mult(A,C)))) = C,
    inference(paramod,[status(thm)],[c_11,c_8]) ).

cnf(c_18,plain,
    mult(mult(A,rd(A,B)),C) = mult(rd(A,B),mult(B,mult(rd(A,B),C))),
    inference(paramod,[status(thm)],[c_9,c_11]) ).

cnf(c_19,plain,
    rd(mult(A,mult(B,mult(A,C))),C) = mult(mult(A,B),A),
    inference(paramod,[status(thm)],[c_11,c_10]) ).

cnf(c_20,plain,
    mult(mult(A,mult(B,mult(A,mult(A,B)))),C) = mult(mult(A,B),mult(A,mult(mult(A,B),C))),
    inference(paramod,[status(thm)],[c_11,c_11]) ).

cnf(c_11964,plain,
    mult(A,mult(ld(A,B),C)) = mult(mult(B,A),ld(A,C)),
    inference(paramod,[status(thm)],[c_7,c_16]) ).

cnf(c_21,plain,
    mult(mult(A,B),ld(B,C)) = mult(B,mult(ld(B,A),C)),
    inference(copy,[status(thm)],[c_11964]) ).

cnf(c_22,plain,
    ld(A,mult(mult(B,A),C)) = mult(ld(A,B),mult(A,C)),
    inference(paramod,[status(thm)],[c_16,c_8]) ).

cnf(c_11965,plain,
    mult(A,ld(ld(B,A),C)) = mult(ld(B,A),mult(ld(ld(B,A),B),C)),
    inference(paramod,[status(thm)],[c_7,c_21]) ).

cnf(c_27,plain,
    mult(ld(A,B),mult(ld(ld(A,B),A),C)) = mult(B,ld(ld(A,B),C)),
    inference(copy,[status(thm)],[c_11965]) ).

cnf(c_28,plain,
    mult(mult(A,B),ld(B,ld(ld(B,A),C))) = mult(B,C),
    inference(paramod,[status(thm)],[c_7,c_21]) ).

cnf(c_29,plain,
    ld(mult(A,B),mult(B,mult(ld(B,A),C))) = ld(B,C),
    inference(paramod,[status(thm)],[c_21,c_8]) ).

cnf(c_32,plain,
    rd(mult(mult(A,B),ld(B,C)),mult(ld(B,A),C)) = B,
    inference(paramod,[status(thm)],[c_21,c_10]) ).

cnf(c_45,plain,
    mult(mult(A,mult(ld(A,B),C)),ld(ld(A,C),D)) = mult(ld(A,C),mult(ld(ld(A,C),mult(B,A)),D)),
    inference(paramod,[status(thm)],[c_21,c_21]) ).

cnf(c_46,plain,
    mult(mult(mult(A,B),ld(B,C)),ld(mult(ld(B,A),C),D)) = mult(mult(ld(B,A),C),mult(ld(mult(ld(B,A),C),B),D)),
    inference(paramod,[status(thm)],[c_21,c_21]) ).

cnf(c_49,plain,
    rd(mult(A,ld(B,C)),mult(ld(B,rd(A,B)),C)) = B,
    inference(paramod,[status(thm)],[c_9,c_32]) ).

cnf(c_56,plain,
    rd(A,mult(ld(B,rd(B,B)),A)) = B,
    inference(paramod,[status(thm)],[c_7,c_49]) ).

cnf(c_11966,plain,
    ld(A,mult(B,ld(A,C))) = mult(ld(A,rd(B,A)),C),
    inference(paramod,[status(thm)],[c_49,c_13]) ).

cnf(c_61,plain,
    mult(ld(A,rd(B,A)),C) = ld(A,mult(B,ld(A,C))),
    inference(copy,[status(thm)],[c_11966]) ).

cnf(c_67,plain,
    mult(ld(A,rd(A,A)),B) = ld(A,B),
    inference(paramod,[status(thm)],[c_7,c_61]) ).

cnf(c_69,plain,
    mult(ld(A,rd(B,A)),mult(A,C)) = ld(A,mult(B,C)),
    inference(paramod,[status(thm)],[c_8,c_61]) ).

cnf(c_71,plain,
    rd(ld(A,mult(B,ld(A,C))),C) = ld(A,rd(B,A)),
    inference(paramod,[status(thm)],[c_61,c_10]) ).

cnf(c_11967,plain,
    ld(A,B) = mult(C,mult(A,ld(mult(mult(A,C),A),B))),
    inference(paramod,[status(thm)],[c_15,c_8]) ).

cnf(c_95,plain,
    mult(A,mult(B,ld(mult(mult(B,A),B),C))) = ld(B,C),
    inference(copy,[status(thm)],[c_11967]) ).

cnf(c_104,plain,
    ld(mult(mult(A,B),A),mult(A,mult(B,C))) = ld(A,C),
    inference(paramod,[status(thm)],[c_7,c_17]) ).

cnf(c_119,plain,
    mult(A,mult(ld(A,rd(A,A)),B)) = B,
    inference(paramod,[status(thm)],[c_67,c_7]) ).

cnf(c_121,plain,
    mult(ld(A,rd(A,A)),mult(A,B)) = B,
    inference(paramod,[status(thm)],[c_67,c_8]) ).

cnf(c_122,plain,
    rd(ld(A,B),B) = ld(A,rd(A,A)),
    inference(paramod,[status(thm)],[c_67,c_10]) ).

cnf(c_123,plain,
    mult(mult(ld(A,B),ld(A,rd(A,A))),C) = mult(ld(A,rd(A,A)),mult(B,mult(ld(A,rd(A,A)),C))),
    inference(paramod,[status(thm)],[c_67,c_11]) ).

cnf(c_145,plain,
    rd(A,mult(B,A)) = ld(B,rd(B,B)),
    inference(paramod,[status(thm)],[c_8,c_122]) ).

cnf(c_147,plain,
    mult(ld(A,ld(B,rd(B,B))),C) = ld(A,mult(ld(B,A),ld(A,C))),
    inference(paramod,[status(thm)],[c_122,c_61]) ).

cnf(c_11968,plain,
    mult(A,rd(B,mult(A,B))) = rd(A,A),
    inference(paramod,[status(thm)],[c_145,c_7]) ).

cnf(c_149,plain,
    rd(A,A) = mult(A,rd(B,mult(A,B))),
    inference(copy,[status(thm)],[c_11968]) ).

cnf(c_151,plain,
    ld(ld(A,rd(A,A)),B) = mult(A,B),
    inference(paramod,[status(thm)],[c_145,c_13]) ).

cnf(c_11969,plain,
    mult(rd(A,mult(B,A)),C) = ld(B,mult(B,ld(B,C))),
    inference(paramod,[status(thm)],[c_145,c_61]) ).

cnf(c_164,plain,
    mult(rd(A,mult(B,A)),C) = ld(B,C),
    inference(paramod,[status(thm)],[c_7,c_11969]) ).

cnf(c_11970,plain,
    mult(ld(A,rd(A,A)),rd(A,A)) = rd(B,mult(A,B)),
    inference(paramod,[status(thm)],[c_145,c_67]) ).

cnf(c_167,plain,
    rd(A,mult(B,A)) = mult(ld(B,rd(B,B)),rd(B,B)),
    inference(copy,[status(thm)],[c_11970]) ).

cnf(c_170,plain,
    rd(A,mult(B,A)) = rd(C,mult(B,C)),
    inference(paramod,[status(thm)],[c_145,c_145]) ).

cnf(c_11971,plain,
    rd(A,B) = rd(C,mult(rd(B,A),C)),
    inference(paramod,[status(thm)],[c_9,c_170]) ).

cnf(c_174,plain,
    rd(A,mult(rd(B,C),A)) = rd(C,B),
    inference(copy,[status(thm)],[c_11971]) ).

cnf(c_176,plain,
    ld(rd(A,mult(B,A)),C) = mult(B,C),
    inference(paramod,[status(thm)],[c_170,c_13]) ).

cnf(c_181,plain,
    mult(mult(A,rd(B,mult(A,B))),A) = A,
    inference(paramod,[status(thm)],[c_149,c_9]) ).

cnf(c_182,plain,
    rd(rd(A,B),rd(A,B)) = mult(rd(A,B),rd(B,A)),
    inference(paramod,[status(thm)],[c_9,c_149]) ).

cnf(c_11972,plain,
    rd(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,rd(B,mult(ld(A,rd(A,A)),B))),
    inference(paramod,[status(thm)],[c_149,c_67]) ).

cnf(c_195,plain,
    rd(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,A),
    inference(paramod,[status(thm)],[c_56,c_11972]) ).

cnf(c_222,plain,
    rd(mult(A,B),C) = mult(mult(A,rd(B,mult(A,C))),A),
    inference(paramod,[status(thm)],[c_9,c_19]) ).

cnf(c_11973,plain,
    rd(mult(ld(A,B),mult(A,mult(ld(A,B),C))),C) = mult(A,mult(ld(A,ld(A,B)),B)),
    inference(paramod,[status(thm)],[c_21,c_19]) ).

cnf(c_11974,plain,
    mult(mult(ld(A,B),rd(mult(A,mult(ld(A,B),C)),mult(ld(A,B),C))),ld(A,B)) = mult(A,mult(ld(A,ld(A,B)),B)),
    inference(paramod,[status(thm)],[c_222,c_11973]) ).

cnf(c_11975,plain,
    mult(mult(ld(A,B),A),ld(A,B)) = mult(A,mult(ld(A,ld(A,B)),B)),
    inference(paramod,[status(thm)],[c_10,c_11974]) ).

cnf(c_223,plain,
    mult(A,mult(ld(A,ld(A,B)),B)) = mult(mult(ld(A,B),A),ld(A,B)),
    inference(copy,[status(thm)],[c_11975]) ).

cnf(c_248,plain,
    mult(rd(A,B),C) = ld(rd(B,A),C),
    inference(paramod,[status(thm)],[c_9,c_164]) ).

cnf(c_254,plain,
    mult(rd(A,mult(rd(B,C),A)),B) = C,
    inference(paramod,[status(thm)],[c_164,c_13]) ).

cnf(c_273,plain,
    rd(A,mult(B,A)) = mult(rd(C,mult(B,C)),rd(B,B)),
    inference(paramod,[status(thm)],[c_164,c_145]) ).

cnf(c_316,plain,
    ld(mult(ld(A,rd(A,A)),rd(A,A)),B) = mult(A,B),
    inference(paramod,[status(thm)],[c_167,c_13]) ).

cnf(c_11976,plain,
    mult(rd(A,A),mult(ld(rd(A,A),ld(A,rd(A,A))),mult(rd(A,A),B))) = mult(rd(C,mult(A,C)),B),
    inference(paramod,[status(thm)],[c_167,c_16]) ).

cnf(c_11977,plain,
    mult(rd(A,A),mult(mult(rd(A,A),ld(A,rd(A,A))),mult(rd(A,A),B))) = mult(rd(C,mult(A,C)),B),
    inference(paramod,[status(thm)],[c_248,c_11976]) ).

cnf(c_318,plain,
    mult(rd(A,mult(B,A)),C) = mult(rd(B,B),mult(mult(rd(B,B),ld(B,rd(B,B))),mult(rd(B,B),C))),
    inference(copy,[status(thm)],[c_11977]) ).

cnf(c_327,plain,
    rd(A,mult(B,A)) = mult(ld(B,rd(B,B)),rd(C,mult(rd(B,B),C))),
    inference(paramod,[status(thm)],[c_174,c_167]) ).

cnf(c_11978,plain,
    ld(A,B) = mult(ld(A,C),mult(A,ld(mult(C,A),B))),
    inference(paramod,[status(thm)],[c_7,c_22]) ).

cnf(c_334,plain,
    mult(ld(A,B),mult(A,ld(mult(B,A),C))) = ld(A,C),
    inference(copy,[status(thm)],[c_11978]) ).

cnf(c_362,plain,
    mult(ld(A,A),ld(A,rd(A,A))) = ld(A,rd(A,A)),
    inference(paramod,[status(thm)],[c_195,c_9]) ).

cnf(c_365,plain,
    rd(ld(A,rd(A,A)),mult(ld(A,rd(A,A)),rd(A,A))) = ld(A,A),
    inference(paramod,[status(thm)],[c_67,c_195]) ).

cnf(c_11979,plain,
    mult(mult(ld(A,rd(A,A)),ld(A,A)),B) = mult(rd(ld(A,rd(A,A)),ld(A,rd(A,A))),mult(ld(A,rd(A,A)),mult(rd(ld(A,rd(A,A)),ld(A,rd(A,A))),B))),
    inference(paramod,[status(thm)],[c_195,c_18]) ).

cnf(c_11980,plain,
    mult(mult(ld(A,rd(A,A)),ld(A,A)),B) = mult(ld(A,A),mult(ld(A,rd(A,A)),mult(rd(ld(A,rd(A,A)),ld(A,rd(A,A))),B))),
    inference(paramod,[status(thm)],[c_195,c_11979]) ).

cnf(c_368,plain,
    mult(mult(ld(A,rd(A,A)),ld(A,A)),B) = mult(ld(A,A),mult(ld(A,rd(A,A)),mult(ld(A,A),B))),
    inference(paramod,[status(thm)],[c_195,c_11980]) ).

cnf(c_11981,plain,
    mult(ld(A,A),B) = ld(rd(ld(A,rd(A,A)),ld(A,rd(A,A))),B),
    inference(paramod,[status(thm)],[c_195,c_248]) ).

cnf(c_11982,plain,
    mult(ld(A,A),B) = ld(ld(A,A),B),
    inference(paramod,[status(thm)],[c_195,c_11981]) ).

cnf(c_371,plain,
    ld(ld(A,A),B) = mult(ld(A,A),B),
    inference(copy,[status(thm)],[c_11982]) ).

cnf(c_11983,plain,
    rd(A,mult(ld(B,B),A)) = rd(ld(B,rd(B,B)),ld(B,rd(B,B))),
    inference(paramod,[status(thm)],[c_195,c_174]) ).

cnf(c_372,plain,
    rd(A,mult(ld(B,B),A)) = ld(B,B),
    inference(paramod,[status(thm)],[c_195,c_11983]) ).

cnf(c_373,plain,
    mult(ld(A,A),mult(ld(A,A),B)) = B,
    inference(paramod,[status(thm)],[c_371,c_7]) ).

cnf(c_11984,plain,
    mult(ld(A,A),mult(mult(ld(A,A),B),mult(ld(A,A),C))) = mult(mult(B,ld(A,A)),C),
    inference(paramod,[status(thm)],[c_371,c_16]) ).

cnf(c_374,plain,
    mult(mult(A,ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),A),mult(ld(B,B),C))),
    inference(copy,[status(thm)],[c_11984]) ).

cnf(c_11985,plain,
    mult(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(ld(ld(B,B),A),C)),
    inference(paramod,[status(thm)],[c_371,c_21]) ).

cnf(c_375,plain,
    mult(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(mult(ld(B,B),A),C)),
    inference(paramod,[status(thm)],[c_371,c_11985]) ).

cnf(c_11986,plain,
    rd(mult(ld(A,A),B),B) = ld(ld(A,A),rd(ld(A,A),ld(A,A))),
    inference(paramod,[status(thm)],[c_371,c_122]) ).

cnf(c_11987,plain,
    mult(mult(ld(A,A),rd(B,mult(ld(A,A),B))),ld(A,A)) = ld(ld(A,A),rd(ld(A,A),ld(A,A))),
    inference(paramod,[status(thm)],[c_222,c_11986]) ).

cnf(c_11988,plain,
    mult(mult(ld(A,A),ld(A,A)),ld(A,A)) = ld(ld(A,A),rd(ld(A,A),ld(A,A))),
    inference(paramod,[status(thm)],[c_372,c_11987]) ).

cnf(c_11989,plain,
    mult(mult(ld(A,A),ld(A,A)),ld(A,A)) = mult(ld(A,A),rd(ld(A,A),ld(A,A))),
    inference(paramod,[status(thm)],[c_371,c_11988]) ).

cnf(c_379,plain,
    mult(ld(A,A),rd(ld(A,A),ld(A,A))) = mult(mult(ld(A,A),ld(A,A)),ld(A,A)),
    inference(copy,[status(thm)],[c_11989]) ).

cnf(c_11990,plain,
    rd(A,mult(ld(B,B),A)) = mult(ld(B,B),rd(ld(B,B),ld(B,B))),
    inference(paramod,[status(thm)],[c_371,c_145]) ).

cnf(c_11991,plain,
    ld(B,B) = mult(ld(B,B),rd(ld(B,B),ld(B,B))),
    inference(paramod,[status(thm)],[c_372,c_11990]) ).

cnf(c_11992,plain,
    ld(B,B) = mult(mult(ld(B,B),ld(B,B)),ld(B,B)),
    inference(paramod,[status(thm)],[c_379,c_11991]) ).

cnf(c_380,plain,
    mult(mult(ld(A,A),ld(A,A)),ld(A,A)) = ld(A,A),
    inference(copy,[status(thm)],[c_11992]) ).

cnf(c_11993,plain,
    ld(ld(A,A),rd(B,mult(ld(A,A),B))) = rd(ld(A,A),ld(A,A)),
    inference(paramod,[status(thm)],[c_149,c_371]) ).

cnf(c_11994,plain,
    ld(ld(A,A),ld(A,A)) = rd(ld(A,A),ld(A,A)),
    inference(paramod,[status(thm)],[c_372,c_11993]) ).

cnf(c_11995,plain,
    mult(ld(A,A),ld(A,A)) = rd(ld(A,A),ld(A,A)),
    inference(paramod,[status(thm)],[c_371,c_11994]) ).

cnf(c_381,plain,
    rd(ld(A,A),ld(A,A)) = mult(ld(A,A),ld(A,A)),
    inference(copy,[status(thm)],[c_11995]) ).

cnf(c_382,plain,
    ld(mult(rd(A,mult(B,A)),B),C) = mult(ld(B,B),C),
    inference(paramod,[status(thm)],[c_164,c_371]) ).

cnf(c_11996,plain,
    mult(ld(A,A),mult(mult(B,ld(A,A)),C)) = mult(ld(ld(A,A),B),mult(ld(A,A),C)),
    inference(paramod,[status(thm)],[c_371,c_22]) ).

cnf(c_11997,plain,
    mult(ld(A,A),mult(mult(B,ld(A,A)),C)) = mult(mult(ld(A,A),B),mult(ld(A,A),C)),
    inference(paramod,[status(thm)],[c_371,c_11996]) ).

cnf(c_385,plain,
    mult(mult(ld(A,A),B),mult(ld(A,A),C)) = mult(ld(A,A),mult(mult(B,ld(A,A)),C)),
    inference(copy,[status(thm)],[c_11997]) ).

cnf(c_11998,plain,
    ld(rd(A,A),mult(rd(B,mult(A,B)),C)) = mult(ld(rd(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
    inference(paramod,[status(thm)],[c_273,c_22]) ).

cnf(c_11999,plain,
    mult(rd(A,A),mult(rd(B,mult(A,B)),C)) = mult(ld(rd(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
    inference(paramod,[status(thm)],[c_248,c_11998]) ).

cnf(c_504,plain,
    mult(rd(A,A),mult(rd(B,mult(A,B)),C)) = mult(mult(rd(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
    inference(paramod,[status(thm)],[c_248,c_11999]) ).

cnf(c_560,plain,
    mult(ld(A,A),rd(B,mult(A,B))) = ld(A,rd(A,A)),
    inference(paramod,[status(thm)],[c_145,c_362]) ).

cnf(c_12000,plain,
    mult(mult(rd(A,B),rd(B,A)),ld(rd(B,A),rd(rd(B,A),rd(B,A)))) = ld(rd(B,A),rd(rd(B,A),rd(B,A))),
    inference(paramod,[status(thm)],[c_248,c_362]) ).

cnf(c_12001,plain,
    mult(mult(rd(A,B),rd(B,A)),ld(rd(B,A),mult(rd(B,A),rd(A,B)))) = ld(rd(B,A),rd(rd(B,A),rd(B,A))),
    inference(paramod,[status(thm)],[c_182,c_12000]) ).

cnf(c_12002,plain,
    mult(mult(rd(A,B),rd(B,A)),rd(A,B)) = ld(rd(B,A),rd(rd(B,A),rd(B,A))),
    inference(paramod,[status(thm)],[c_8,c_12001]) ).

cnf(c_12003,plain,
    mult(mult(rd(A,B),rd(B,A)),rd(A,B)) = ld(rd(B,A),mult(rd(B,A),rd(A,B))),
    inference(paramod,[status(thm)],[c_182,c_12002]) ).

cnf(c_563,plain,
    mult(mult(rd(A,B),rd(B,A)),rd(A,B)) = rd(A,B),
    inference(paramod,[status(thm)],[c_8,c_12003]) ).

cnf(c_12004,plain,
    mult(rd(A,A),ld(ld(A,rd(A,A)),B)) = ld(A,mult(ld(ld(A,rd(A,A)),A),B)),
    inference(paramod,[status(thm)],[c_27,c_67]) ).

cnf(c_12005,plain,
    mult(rd(A,A),mult(A,B)) = ld(A,mult(ld(ld(A,rd(A,A)),A),B)),
    inference(paramod,[status(thm)],[c_151,c_12004]) ).

cnf(c_12006,plain,
    mult(rd(A,A),mult(A,B)) = ld(A,mult(mult(A,A),B)),
    inference(paramod,[status(thm)],[c_151,c_12005]) ).

cnf(c_613,plain,
    mult(rd(A,A),mult(A,B)) = mult(ld(A,A),mult(A,B)),
    inference(paramod,[status(thm)],[c_22,c_12006]) ).

cnf(c_12007,plain,
    mult(mult(ld(A,A),B),mult(ld(ld(ld(A,A),B),ld(A,A)),C)) = mult(B,ld(ld(ld(A,A),B),C)),
    inference(paramod,[status(thm)],[c_371,c_27]) ).

cnf(c_12008,plain,
    mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),ld(A,A)),C)) = mult(B,ld(ld(ld(A,A),B),C)),
    inference(paramod,[status(thm)],[c_371,c_12007]) ).

cnf(c_637,plain,
    mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),ld(A,A)),C)) = mult(B,ld(mult(ld(A,A),B),C)),
    inference(paramod,[status(thm)],[c_371,c_12008]) ).

cnf(c_661,plain,
    mult(ld(A,rd(A,A)),rd(A,A)) = mult(ld(A,A),rd(B,mult(A,B))),
    inference(paramod,[status(thm)],[c_560,c_67]) ).

cnf(c_665,plain,
    mult(rd(A,mult(B,A)),rd(B,B)) = mult(ld(B,B),rd(C,mult(B,C))),
    inference(paramod,[status(thm)],[c_560,c_164]) ).

cnf(c_678,plain,
    mult(ld(A,A),rd(B,mult(A,B))) = mult(ld(A,A),rd(C,mult(A,C))),
    inference(paramod,[status(thm)],[c_560,c_560]) ).

cnf(c_12009,plain,
    ld(mult(A,B),mult(B,C)) = ld(B,ld(ld(B,A),C)),
    inference(paramod,[status(thm)],[c_28,c_8]) ).

cnf(c_728,plain,
    ld(A,ld(ld(A,B),C)) = ld(mult(B,A),mult(A,C)),
    inference(copy,[status(thm)],[c_12009]) ).

cnf(c_12010,plain,
    mult(mult(A,ld(B,B)),ld(ld(B,B),ld(mult(ld(B,B),A),C))) = mult(ld(B,B),C),
    inference(paramod,[status(thm)],[c_371,c_28]) ).

cnf(c_749,plain,
    mult(mult(A,ld(B,B)),mult(ld(B,B),ld(mult(ld(B,B),A),C))) = mult(ld(B,B),C),
    inference(paramod,[status(thm)],[c_371,c_12010]) ).

cnf(c_12011,plain,
    ld(mult(A,ld(B,B)),mult(ld(B,B),mult(mult(ld(B,B),A),C))) = ld(ld(B,B),C),
    inference(paramod,[status(thm)],[c_371,c_29]) ).

cnf(c_788,plain,
    ld(mult(A,ld(B,B)),mult(ld(B,B),mult(mult(ld(B,B),A),C))) = mult(ld(B,B),C),
    inference(paramod,[status(thm)],[c_371,c_12011]) ).

cnf(c_12012,plain,
    ld(rd(A,mult(B,A)),mult(rd(B,B),mult(ld(rd(B,B),rd(C,mult(B,C))),D))) = ld(rd(B,B),D),
    inference(paramod,[status(thm)],[c_273,c_29]) ).

cnf(c_12013,plain,
    ld(rd(A,mult(B,A)),mult(rd(B,B),mult(mult(rd(B,B),rd(C,mult(B,C))),D))) = ld(rd(B,B),D),
    inference(paramod,[status(thm)],[c_248,c_12012]) ).

cnf(c_12014,plain,
    mult(B,mult(rd(B,B),mult(mult(rd(B,B),rd(C,mult(B,C))),D))) = ld(rd(B,B),D),
    inference(paramod,[status(thm)],[c_176,c_12013]) ).

cnf(c_796,plain,
    mult(A,mult(rd(A,A),mult(mult(rd(A,A),rd(B,mult(A,B))),C))) = mult(rd(A,A),C),
    inference(paramod,[status(thm)],[c_248,c_12014]) ).

cnf(c_12015,plain,
    mult(ld(A,A),mult(mult(B,ld(A,A)),ld(ld(A,A),C))) = mult(ld(ld(A,A),B),C),
    inference(paramod,[status(thm)],[c_21,c_373]) ).

cnf(c_12016,plain,
    mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))) = mult(ld(ld(A,A),B),C),
    inference(paramod,[status(thm)],[c_371,c_12015]) ).

cnf(c_12017,plain,
    mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))) = mult(mult(ld(A,A),B),C),
    inference(paramod,[status(thm)],[c_371,c_12016]) ).

cnf(c_980,plain,
    mult(mult(ld(A,A),B),C) = mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))),
    inference(copy,[status(thm)],[c_12017]) ).

cnf(c_988,plain,
    mult(mult(ld(A,A),mult(B,B)),C) = mult(mult(ld(A,A),B),mult(ld(A,A),mult(mult(ld(A,A),B),C))),
    inference(paramod,[status(thm)],[c_373,c_20]) ).

cnf(c_993,plain,
    ld(mult(A,A),mult(A,B)) = ld(A,mult(ld(A,A),B)),
    inference(paramod,[status(thm)],[c_373,c_29]) ).

cnf(c_1000,plain,
    ld(mult(A,A),B) = ld(A,mult(ld(A,A),ld(A,B))),
    inference(paramod,[status(thm)],[c_7,c_993]) ).

cnf(c_12018,plain,
    ld(mult(A,A),mult(A,mult(ld(A,A),rd(B,mult(A,B))))) = ld(A,rd(C,mult(A,C))),
    inference(paramod,[status(thm)],[c_678,c_29]) ).

cnf(c_12019,plain,
    ld(A,mult(ld(A,A),ld(A,mult(A,mult(ld(A,A),rd(B,mult(A,B))))))) = ld(A,rd(C,mult(A,C))),
    inference(paramod,[status(thm)],[c_1000,c_12018]) ).

cnf(c_12020,plain,
    ld(A,mult(ld(A,A),mult(ld(A,A),rd(B,mult(A,B))))) = ld(A,rd(C,mult(A,C))),
    inference(paramod,[status(thm)],[c_8,c_12019]) ).

cnf(c_1202,plain,
    ld(A,rd(B,mult(A,B))) = ld(A,rd(C,mult(A,C))),
    inference(paramod,[status(thm)],[c_373,c_12020]) ).

cnf(c_1215,plain,
    mult(ld(A,rd(A,A)),rd(B,mult(A,B))) = ld(A,rd(C,mult(A,C))),
    inference(paramod,[status(thm)],[c_1202,c_67]) ).

cnf(c_12021,plain,
    mult(ld(A,rd(A,A)),rd(ld(A,B),B)) = ld(A,rd(C,mult(A,C))),
    inference(paramod,[status(thm)],[c_7,c_1215]) ).

cnf(c_1232,plain,
    mult(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,rd(B,mult(A,B))),
    inference(paramod,[status(thm)],[c_122,c_12021]) ).

cnf(c_12022,plain,
    ld(rd(A,mult(B,A)),mult(ld(B,rd(C,mult(B,C))),D)) = mult(ld(rd(A,mult(B,A)),ld(B,rd(B,B))),mult(rd(A,mult(B,A)),D)),
    inference(paramod,[status(thm)],[c_1215,c_22]) ).

cnf(c_12023,plain,
    mult(B,mult(ld(B,rd(C,mult(B,C))),D)) = mult(ld(rd(A,mult(B,A)),ld(B,rd(B,B))),mult(rd(A,mult(B,A)),D)),
    inference(paramod,[status(thm)],[c_176,c_12022]) ).

cnf(c_12024,plain,
    mult(B,mult(ld(B,rd(C,mult(B,C))),D)) = mult(mult(B,ld(B,rd(B,B))),mult(rd(A,mult(B,A)),D)),
    inference(paramod,[status(thm)],[c_176,c_12023]) ).

cnf(c_12025,plain,
    mult(B,mult(ld(B,rd(C,mult(B,C))),D)) = mult(rd(B,B),mult(rd(A,mult(B,A)),D)),
    inference(paramod,[status(thm)],[c_7,c_12024]) ).

cnf(c_1256,plain,
    mult(rd(A,A),mult(rd(B,mult(A,B)),C)) = mult(A,mult(ld(A,rd(D,mult(A,D))),C)),
    inference(copy,[status(thm)],[c_12025]) ).

cnf(c_12026,plain,
    mult(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,rd(ld(A,B),B)),
    inference(paramod,[status(thm)],[c_7,c_1232]) ).

cnf(c_12027,plain,
    mult(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,ld(A,rd(A,A))),
    inference(paramod,[status(thm)],[c_122,c_12026]) ).

cnf(c_1426,plain,
    ld(A,ld(A,rd(A,A))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
    inference(copy,[status(thm)],[c_12027]) ).

cnf(c_12028,plain,
    ld(ld(A,rd(A,A)),mult(ld(A,rd(B,mult(A,B))),C)) = mult(ld(ld(A,rd(A,A)),ld(A,rd(A,A))),mult(ld(A,rd(A,A)),C)),
    inference(paramod,[status(thm)],[c_1232,c_22]) ).

cnf(c_12029,plain,
    mult(A,mult(ld(A,rd(B,mult(A,B))),C)) = mult(ld(ld(A,rd(A,A)),ld(A,rd(A,A))),mult(ld(A,rd(A,A)),C)),
    inference(paramod,[status(thm)],[c_151,c_12028]) ).

cnf(c_12030,plain,
    mult(A,mult(ld(A,rd(B,mult(A,B))),C)) = mult(mult(A,ld(A,rd(A,A))),mult(ld(A,rd(A,A)),C)),
    inference(paramod,[status(thm)],[c_151,c_12029]) ).

cnf(c_12031,plain,
    mult(A,mult(ld(A,rd(B,mult(A,B))),C)) = mult(rd(A,A),mult(ld(A,rd(A,A)),C)),
    inference(paramod,[status(thm)],[c_7,c_12030]) ).

cnf(c_1443,plain,
    mult(rd(A,A),mult(ld(A,rd(A,A)),B)) = mult(A,mult(ld(A,rd(C,mult(A,C))),B)),
    inference(copy,[status(thm)],[c_12031]) ).

cnf(c_12032,plain,
    ld(mult(rd(A,mult(B,A)),B),mult(B,mult(mult(ld(B,rd(B,B)),ld(B,rd(B,B))),C))) = ld(B,C),
    inference(paramod,[status(thm)],[c_1232,c_29]) ).

cnf(c_12033,plain,
    ld(mult(rd(A,mult(B,A)),B),mult(B,mult(ld(B,rd(B,B)),mult(rd(B,B),mult(ld(B,rd(B,B)),C))))) = ld(B,C),
    inference(paramod,[status(thm)],[c_123,c_12032]) ).

cnf(c_12034,plain,
    ld(mult(rd(A,mult(B,A)),B),mult(rd(B,B),mult(ld(B,rd(B,B)),C))) = ld(B,C),
    inference(paramod,[status(thm)],[c_119,c_12033]) ).

cnf(c_1453,plain,
    mult(ld(A,A),mult(rd(A,A),mult(ld(A,rd(A,A)),B))) = ld(A,B),
    inference(paramod,[status(thm)],[c_382,c_12034]) ).

cnf(c_12035,plain,
    ld(mult(A,A),B) = mult(ld(A,rd(ld(A,A),A)),mult(A,ld(A,B))),
    inference(paramod,[status(thm)],[c_69,c_1000]) ).

cnf(c_12036,plain,
    ld(A,mult(ld(A,A),ld(A,B))) = mult(ld(A,rd(ld(A,A),A)),mult(A,ld(A,B))),
    inference(paramod,[status(thm)],[c_1000,c_12035]) ).

cnf(c_12037,plain,
    ld(A,mult(ld(A,A),ld(A,B))) = mult(ld(A,ld(A,rd(A,A))),mult(A,ld(A,B))),
    inference(paramod,[status(thm)],[c_122,c_12036]) ).

cnf(c_12038,plain,
    ld(A,mult(ld(A,A),ld(A,B))) = mult(mult(ld(A,rd(A,A)),ld(A,rd(A,A))),mult(A,ld(A,B))),
    inference(paramod,[status(thm)],[c_1426,c_12037]) ).

cnf(c_12039,plain,
    ld(A,mult(ld(A,A),ld(A,B))) = mult(mult(ld(A,rd(A,A)),ld(A,rd(A,A))),B),
    inference(paramod,[status(thm)],[c_7,c_12038]) ).

cnf(c_12040,plain,
    ld(A,mult(ld(A,A),ld(A,B))) = mult(ld(A,rd(A,A)),mult(rd(A,A),mult(ld(A,rd(A,A)),B))),
    inference(paramod,[status(thm)],[c_123,c_12039]) ).

cnf(c_1604,plain,
    mult(ld(A,rd(A,A)),mult(rd(A,A),mult(ld(A,rd(A,A)),B))) = ld(A,mult(ld(A,A),ld(A,B))),
    inference(copy,[status(thm)],[c_12040]) ).

cnf(c_1634,plain,
    rd(ld(A,mult(B,C)),mult(A,C)) = ld(A,rd(B,A)),
    inference(paramod,[status(thm)],[c_8,c_71]) ).

cnf(c_12041,plain,
    rd(ld(mult(A,B),mult(B,ld(mult(A,B),C))),C) = ld(mult(A,B),rd(D,mult(A,D))),
    inference(paramod,[status(thm)],[c_170,c_71]) ).

cnf(c_12042,plain,
    ld(mult(A,B),rd(B,mult(A,B))) = ld(mult(A,B),rd(D,mult(A,D))),
    inference(paramod,[status(thm)],[c_71,c_12041]) ).

cnf(c_1643,plain,
    ld(mult(A,B),rd(C,mult(A,C))) = ld(mult(A,B),rd(B,mult(A,B))),
    inference(copy,[status(thm)],[c_12042]) ).

cnf(c_12043,plain,
    rd(ld(A,ld(A,rd(A,A))),rd(A,A)) = ld(A,rd(ld(A,A),A)),
    inference(paramod,[status(thm)],[c_362,c_71]) ).

cnf(c_12044,plain,
    rd(mult(ld(A,rd(A,A)),ld(A,rd(A,A))),rd(A,A)) = ld(A,rd(ld(A,A),A)),
    inference(paramod,[status(thm)],[c_1426,c_12043]) ).

cnf(c_12045,plain,
    mult(mult(ld(A,rd(A,A)),rd(ld(A,rd(A,A)),mult(ld(A,rd(A,A)),rd(A,A)))),ld(A,rd(A,A))) = ld(A,rd(ld(A,A),A)),
    inference(paramod,[status(thm)],[c_222,c_12044]) ).

cnf(c_12046,plain,
    mult(mult(ld(A,rd(A,A)),ld(A,A)),ld(A,rd(A,A))) = ld(A,rd(ld(A,A),A)),
    inference(paramod,[status(thm)],[c_365,c_12045]) ).

cnf(c_12047,plain,
    mult(ld(A,A),mult(ld(A,rd(A,A)),mult(ld(A,A),ld(A,rd(A,A))))) = ld(A,rd(ld(A,A),A)),
    inference(paramod,[status(thm)],[c_368,c_12046]) ).

cnf(c_12048,plain,
    mult(ld(A,A),mult(ld(A,rd(A,A)),ld(A,rd(A,A)))) = ld(A,rd(ld(A,A),A)),
    inference(paramod,[status(thm)],[c_362,c_12047]) ).

cnf(c_12049,plain,
    mult(ld(A,A),mult(ld(A,rd(A,A)),ld(A,rd(A,A)))) = ld(A,ld(A,rd(A,A))),
    inference(paramod,[status(thm)],[c_122,c_12048]) ).

cnf(c_1653,plain,
    mult(ld(A,A),mult(ld(A,rd(A,A)),ld(A,rd(A,A)))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
    inference(paramod,[status(thm)],[c_1426,c_12049]) ).

cnf(c_1670,plain,
    rd(ld(A,B),mult(A,ld(C,B))) = ld(A,rd(C,A)),
    inference(paramod,[status(thm)],[c_7,c_1634]) ).

cnf(c_12050,plain,
    mult(A,rd(ld(A,B),mult(A,ld(C,B)))) = rd(C,A),
    inference(paramod,[status(thm)],[c_1670,c_7]) ).

cnf(c_1879,plain,
    rd(A,B) = mult(B,rd(ld(B,C),mult(B,ld(A,C)))),
    inference(copy,[status(thm)],[c_12050]) ).

cnf(c_1899,plain,
    rd(ld(A,B),mult(A,ld(ld(C,A),B))) = ld(A,ld(C,rd(C,C))),
    inference(paramod,[status(thm)],[c_122,c_1670]) ).

cnf(c_1981,plain,
    rd(ld(A,B),mult(A,ld(C,B))) = rd(ld(A,D),mult(A,ld(C,D))),
    inference(paramod,[status(thm)],[c_1670,c_1670]) ).

cnf(c_2010,plain,
    ld(mult(A,B),rd(C,mult(A,C))) = ld(mult(A,B),rd(D,mult(A,D))),
    inference(paramod,[status(thm)],[c_170,c_1643]) ).

cnf(c_12051,plain,
    rd(ld(A,B),mult(A,C)) = rd(ld(A,D),mult(A,ld(rd(B,C),D))),
    inference(paramod,[status(thm)],[c_13,c_1981]) ).

cnf(c_2232,plain,
    rd(ld(A,B),mult(A,ld(rd(C,D),B))) = rd(ld(A,C),mult(A,D)),
    inference(copy,[status(thm)],[c_12051]) ).

cnf(c_12052,plain,
    rd(mult(ld(A,rd(A,A)),B),mult(A,ld(C,B))) = rd(ld(A,D),mult(A,ld(C,D))),
    inference(paramod,[status(thm)],[c_67,c_1981]) ).

cnf(c_12053,plain,
    mult(mult(ld(A,rd(A,A)),rd(B,mult(ld(A,rd(A,A)),mult(A,ld(C,B))))),ld(A,rd(A,A))) = rd(ld(A,D),mult(A,ld(C,D))),
    inference(paramod,[status(thm)],[c_222,c_12052]) ).

cnf(c_12054,plain,
    mult(mult(ld(A,rd(A,A)),rd(B,ld(C,B))),ld(A,rd(A,A))) = rd(ld(A,D),mult(A,ld(C,D))),
    inference(paramod,[status(thm)],[c_121,c_12053]) ).

cnf(c_12055,plain,
    mult(mult(ld(A,rd(A,A)),C),ld(A,rd(A,A))) = rd(ld(A,D),mult(A,ld(C,D))),
    inference(paramod,[status(thm)],[c_14,c_12054]) ).

cnf(c_2236,plain,
    rd(ld(A,B),mult(A,ld(C,B))) = mult(mult(ld(A,rd(A,A)),C),ld(A,rd(A,A))),
    inference(copy,[status(thm)],[c_12055]) ).

cnf(c_12056,plain,
    mult(mult(ld(A,rd(A,A)),rd(C,D)),ld(A,rd(A,A))) = rd(ld(A,C),mult(A,D)),
    inference(paramod,[status(thm)],[c_2236,c_2232]) ).

cnf(c_2263,plain,
    rd(ld(A,B),mult(A,C)) = mult(mult(ld(A,rd(A,A)),rd(B,C)),ld(A,rd(A,A))),
    inference(copy,[status(thm)],[c_12056]) ).

cnf(c_12057,plain,
    mult(mult(ld(A,rd(A,A)),rd(B,ld(ld(C,A),B))),ld(A,rd(A,A))) = ld(A,ld(C,rd(C,C))),
    inference(paramod,[status(thm)],[c_2263,c_1899]) ).

cnf(c_2333,plain,
    mult(mult(ld(A,rd(A,A)),ld(B,A)),ld(A,rd(A,A))) = ld(A,ld(B,rd(B,B))),
    inference(paramod,[status(thm)],[c_14,c_12057]) ).

cnf(c_12058,plain,
    rd(A,B) = mult(B,mult(mult(ld(B,rd(B,B)),rd(C,ld(A,C))),ld(B,rd(B,B)))),
    inference(paramod,[status(thm)],[c_2263,c_1879]) ).

cnf(c_2341,plain,
    rd(A,B) = mult(B,mult(mult(ld(B,rd(B,B)),A),ld(B,rd(B,B)))),
    inference(paramod,[status(thm)],[c_14,c_12058]) ).

cnf(c_12059,plain,
    ld(A,rd(B,mult(C,B))) = ld(mult(C,ld(C,A)),rd(D,mult(C,D))),
    inference(paramod,[status(thm)],[c_7,c_2010]) ).

cnf(c_2445,plain,
    ld(A,rd(B,mult(C,B))) = ld(A,rd(D,mult(C,D))),
    inference(paramod,[status(thm)],[c_7,c_12059]) ).

cnf(c_12060,plain,
    ld(rd(A,mult(B,A)),rd(C,mult(D,C))) = mult(B,rd(E,mult(D,E))),
    inference(paramod,[status(thm)],[c_2445,c_176]) ).

cnf(c_2494,plain,
    mult(A,rd(B,mult(C,B))) = mult(A,rd(D,mult(C,D))),
    inference(paramod,[status(thm)],[c_176,c_12060]) ).

cnf(c_12061,plain,
    rd(ld(rd(A,mult(B,A)),rd(C,mult(B,C))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))) = mult(ld(rd(A,mult(B,A)),rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_2445,c_381]) ).

cnf(c_12062,plain,
    rd(mult(B,rd(C,mult(B,C))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))) = mult(ld(rd(A,mult(B,A)),rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_176,c_12061]) ).

cnf(c_12063,plain,
    rd(mult(B,rd(C,mult(B,C))),mult(B,rd(A,mult(B,A)))) = mult(ld(rd(A,mult(B,A)),rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_176,c_12062]) ).

cnf(c_12064,plain,
    mult(mult(B,rd(rd(C,mult(B,C)),mult(B,mult(B,rd(A,mult(B,A)))))),B) = mult(ld(rd(A,mult(B,A)),rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_222,c_12063]) ).

cnf(c_12065,plain,
    mult(mult(B,rd(rd(C,mult(B,C)),mult(B,mult(B,rd(A,mult(B,A)))))),B) = mult(mult(B,rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_176,c_12064]) ).

cnf(c_2495,plain,
    mult(mult(A,rd(rd(B,mult(A,B)),mult(A,mult(A,rd(C,mult(A,C)))))),A) = mult(mult(A,rd(C,mult(A,C))),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_176,c_12065]) ).

cnf(c_12066,plain,
    mult(A,rd(ld(B,C),C)) = mult(A,rd(D,mult(B,D))),
    inference(paramod,[status(thm)],[c_7,c_2494]) ).

cnf(c_12067,plain,
    mult(A,ld(B,rd(B,B))) = mult(A,rd(D,mult(B,D))),
    inference(paramod,[status(thm)],[c_122,c_12066]) ).

cnf(c_2522,plain,
    mult(A,rd(B,mult(C,B))) = mult(A,ld(C,rd(C,C))),
    inference(copy,[status(thm)],[c_12067]) ).

cnf(c_2594,plain,
    mult(ld(A,rd(A,A)),ld(B,rd(B,B))) = ld(A,rd(C,mult(B,C))),
    inference(paramod,[status(thm)],[c_2522,c_67]) ).

cnf(c_2606,plain,
    mult(rd(A,B),ld(C,rd(C,C))) = ld(rd(B,A),rd(D,mult(C,D))),
    inference(paramod,[status(thm)],[c_2522,c_248]) ).

cnf(c_2610,plain,
    mult(A,rd(B,mult(C,B))) = mult(A,ld(C,rd(D,mult(rd(C,C),D)))),
    inference(paramod,[status(thm)],[c_174,c_2522]) ).

cnf(c_2647,plain,
    mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))) = ld(A,rd(A,A)),
    inference(paramod,[status(thm)],[c_2522,c_560]) ).

cnf(c_2670,plain,
    mult(ld(A,rd(A,A)),rd(A,A)) = mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))),
    inference(paramod,[status(thm)],[c_2522,c_661]) ).

cnf(c_2677,plain,
    mult(rd(A,mult(B,A)),rd(B,B)) = mult(ld(B,B),rd(ld(C,rd(C,C)),mult(B,rd(D,mult(C,D))))),
    inference(paramod,[status(thm)],[c_2522,c_665]) ).

cnf(c_12068,plain,
    rd(ld(rd(A,mult(B,A)),rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),rd(rd(A,mult(B,A)),rd(A,mult(B,A)))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_2594,c_381]) ).

cnf(c_12069,plain,
    rd(mult(B,rd(A,mult(B,A))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),rd(rd(A,mult(B,A)),rd(A,mult(B,A)))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_176,c_12068]) ).

cnf(c_12070,plain,
    rd(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),rd(rd(A,mult(B,A)),rd(A,mult(B,A)))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_176,c_12069]) ).

cnf(c_12071,plain,
    mult(mult(B,rd(rd(A,mult(B,A)),mult(B,mult(B,rd(A,mult(B,A)))))),B) = mult(mult(ld(rd(A,mult(B,A)),rd(rd(A,mult(B,A)),rd(A,mult(B,A)))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_222,c_12070]) ).

cnf(c_12072,plain,
    mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),rd(rd(A,mult(B,A)),rd(A,mult(B,A)))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_2495,c_12071]) ).

cnf(c_12073,plain,
    mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),mult(rd(A,mult(B,A)),rd(mult(B,A),A))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_182,c_12072]) ).

cnf(c_12074,plain,
    mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),mult(rd(A,mult(B,A)),mult(mult(B,rd(A,mult(B,A))),B))),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_222,c_12073]) ).

cnf(c_12075,plain,
    mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(ld(rd(A,mult(B,A)),mult(rd(A,mult(B,A)),B)),ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_181,c_12074]) ).

cnf(c_12076,plain,
    mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(mult(B,ld(B,rd(B,B))),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_8,c_12075]) ).

cnf(c_12077,plain,
    mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(rd(B,B),ld(rd(A,mult(B,A)),rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_7,c_12076]) ).

cnf(c_12078,plain,
    mult(mult(B,rd(A,mult(B,A))),mult(B,rd(A,mult(B,A)))) = mult(rd(B,B),mult(B,rd(A,mult(B,A)))),
    inference(paramod,[status(thm)],[c_176,c_12077]) ).

cnf(c_3039,plain,
    mult(mult(A,rd(B,mult(A,B))),mult(A,rd(B,mult(A,B)))) = mult(ld(A,A),mult(A,rd(B,mult(A,B)))),
    inference(paramod,[status(thm)],[c_613,c_12078]) ).

cnf(c_3079,plain,
    mult(mult(A,rd(rd(B,mult(A,B)),mult(A,mult(A,rd(C,mult(A,C)))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_3039,c_2495]) ).

cnf(c_12079,plain,
    mult(A,ld(B,rd(B,B))) = ld(rd(mult(ld(A,rd(A,A)),C),C),rd(D,mult(B,D))),
    inference(paramod,[status(thm)],[c_56,c_2606]) ).

cnf(c_12080,plain,
    mult(A,ld(B,rd(B,B))) = ld(mult(mult(ld(A,rd(A,A)),rd(C,mult(ld(A,rd(A,A)),C))),ld(A,rd(A,A))),rd(D,mult(B,D))),
    inference(paramod,[status(thm)],[c_222,c_12079]) ).

cnf(c_3178,plain,
    mult(A,ld(B,rd(B,B))) = ld(mult(mult(ld(A,rd(A,A)),A),ld(A,rd(A,A))),rd(C,mult(B,C))),
    inference(paramod,[status(thm)],[c_56,c_12080]) ).

cnf(c_3516,plain,
    ld(mult(ld(A,rd(A,A)),rd(B,mult(rd(A,A),B))),C) = mult(A,C),
    inference(paramod,[status(thm)],[c_174,c_316]) ).

cnf(c_3639,plain,
    mult(mult(mult(rd(A,mult(B,A)),B),ld(B,B)),ld(B,B)) = ld(B,B),
    inference(paramod,[status(thm)],[c_164,c_380]) ).

cnf(c_3663,plain,
    ld(mult(rd(rd(A,mult(B,A)),mult(C,rd(D,mult(B,D)))),C),E) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_2494,c_382]) ).

cnf(c_12081,plain,
    mult(mult(rd(A,mult(B,A)),rd(mult(B,A),A)),ld(B,rd(B,B))) = rd(A,mult(B,A)),
    inference(paramod,[status(thm)],[c_145,c_563]) ).

cnf(c_12082,plain,
    mult(mult(rd(A,mult(B,A)),mult(mult(B,rd(A,mult(B,A))),B)),ld(B,rd(B,B))) = rd(A,mult(B,A)),
    inference(paramod,[status(thm)],[c_222,c_12081]) ).

cnf(c_3819,plain,
    mult(mult(rd(A,mult(B,A)),B),ld(B,rd(B,B))) = rd(A,mult(B,A)),
    inference(paramod,[status(thm)],[c_181,c_12082]) ).

cnf(c_12083,plain,
    mult(rd(A,A),B) = mult(ld(A,A),mult(A,ld(A,B))),
    inference(paramod,[status(thm)],[c_7,c_613]) ).

cnf(c_3858,plain,
    mult(rd(A,A),B) = mult(ld(A,A),B),
    inference(paramod,[status(thm)],[c_7,c_12083]) ).

cnf(c_12084,plain,
    rd(mult(A,B),mult(ld(A,A),mult(A,B))) = ld(rd(A,A),rd(rd(A,A),rd(A,A))),
    inference(paramod,[status(thm)],[c_613,c_145]) ).

cnf(c_12085,plain,
    ld(A,A) = ld(rd(A,A),rd(rd(A,A),rd(A,A))),
    inference(paramod,[status(thm)],[c_372,c_12084]) ).

cnf(c_12086,plain,
    ld(A,A) = ld(rd(A,A),mult(rd(A,A),rd(A,A))),
    inference(paramod,[status(thm)],[c_182,c_12085]) ).

cnf(c_12087,plain,
    ld(A,A) = ld(rd(A,A),mult(ld(A,A),rd(A,A))),
    inference(paramod,[status(thm)],[c_3858,c_12086]) ).

cnf(c_12088,plain,
    ld(A,A) = mult(rd(A,A),mult(ld(A,A),rd(A,A))),
    inference(paramod,[status(thm)],[c_248,c_12087]) ).

cnf(c_12089,plain,
    ld(A,A) = mult(ld(A,A),mult(ld(A,A),rd(A,A))),
    inference(paramod,[status(thm)],[c_3858,c_12088]) ).

cnf(c_12090,plain,
    ld(A,A) = rd(A,A),
    inference(paramod,[status(thm)],[c_373,c_12089]) ).

cnf(c_3866,plain,
    rd(A,A) = ld(A,A),
    inference(copy,[status(thm)],[c_12090]) ).

cnf(c_12091,plain,
    mult(mult(A,rd(A,A)),mult(A,B)) = mult(rd(A,A),mult(A,mult(ld(A,A),mult(A,B)))),
    inference(paramod,[status(thm)],[c_613,c_18]) ).

cnf(c_12092,plain,
    mult(mult(A,ld(A,A)),mult(A,B)) = mult(rd(A,A),mult(A,mult(ld(A,A),mult(A,B)))),
    inference(paramod,[status(thm)],[c_3866,c_12091]) ).

cnf(c_12093,plain,
    mult(A,mult(A,B)) = mult(rd(A,A),mult(A,mult(ld(A,A),mult(A,B)))),
    inference(paramod,[status(thm)],[c_7,c_12092]) ).

cnf(c_12094,plain,
    mult(A,mult(A,B)) = mult(ld(A,A),mult(A,mult(ld(A,A),mult(A,B)))),
    inference(paramod,[status(thm)],[c_3866,c_12093]) ).

cnf(c_12095,plain,
    mult(A,mult(A,B)) = mult(ld(A,A),mult(mult(A,A),B)),
    inference(paramod,[status(thm)],[c_16,c_12094]) ).

cnf(c_3869,plain,
    mult(ld(A,A),mult(mult(A,A),B)) = mult(A,mult(A,B)),
    inference(copy,[status(thm)],[c_12095]) ).

cnf(c_12096,plain,
    mult(rd(mult(A,B),mult(ld(A,A),mult(A,B))),A) = A,
    inference(paramod,[status(thm)],[c_613,c_254]) ).

cnf(c_3879,plain,
    mult(ld(A,A),A) = A,
    inference(paramod,[status(thm)],[c_372,c_12096]) ).

cnf(c_12097,plain,
    ld(mult(ld(A,ld(A,A)),rd(B,mult(rd(A,A),B))),C) = mult(A,C),
    inference(paramod,[status(thm)],[c_3866,c_3516]) ).

cnf(c_12098,plain,
    ld(mult(ld(A,ld(A,A)),rd(B,mult(ld(A,A),B))),C) = mult(A,C),
    inference(paramod,[status(thm)],[c_3866,c_12097]) ).

cnf(c_3896,plain,
    ld(mult(ld(A,ld(A,A)),ld(A,A)),B) = mult(A,B),
    inference(paramod,[status(thm)],[c_372,c_12098]) ).

cnf(c_12099,plain,
    mult(A,rd(B,mult(C,B))) = mult(A,ld(C,rd(D,mult(ld(C,C),D)))),
    inference(paramod,[status(thm)],[c_3866,c_2610]) ).

cnf(c_3908,plain,
    mult(A,rd(B,mult(C,B))) = mult(A,ld(C,ld(C,C))),
    inference(paramod,[status(thm)],[c_372,c_12099]) ).

cnf(c_12100,plain,
    mult(ld(A,ld(A,A)),mult(rd(A,A),mult(ld(A,rd(A,A)),B))) = ld(A,mult(ld(A,A),ld(A,B))),
    inference(paramod,[status(thm)],[c_3866,c_1604]) ).

cnf(c_12101,plain,
    mult(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,rd(A,A)),B))) = ld(A,mult(ld(A,A),ld(A,B))),
    inference(paramod,[status(thm)],[c_3866,c_12100]) ).

cnf(c_12102,plain,
    mult(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,ld(A,A)),B))) = ld(A,mult(ld(A,A),ld(A,B))),
    inference(paramod,[status(thm)],[c_3866,c_12101]) ).

cnf(c_3920,plain,
    ld(A,mult(ld(A,A),ld(A,B))) = mult(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,ld(A,A)),B))),
    inference(copy,[status(thm)],[c_12102]) ).

cnf(c_12103,plain,
    mult(ld(A,A),mult(ld(A,A),mult(ld(A,rd(A,A)),B))) = ld(A,B),
    inference(paramod,[status(thm)],[c_3866,c_1453]) ).

cnf(c_12104,plain,
    mult(ld(A,A),mult(ld(A,A),mult(ld(A,ld(A,A)),B))) = ld(A,B),
    inference(paramod,[status(thm)],[c_3866,c_12103]) ).

cnf(c_3925,plain,
    mult(ld(A,ld(A,A)),B) = ld(A,B),
    inference(paramod,[status(thm)],[c_373,c_12104]) ).

cnf(c_12105,plain,
    mult(ld(A,A),mult(ld(A,rd(A,A)),B)) = mult(A,mult(ld(A,rd(C,mult(A,C))),B)),
    inference(paramod,[status(thm)],[c_3866,c_1443]) ).

cnf(c_12106,plain,
    mult(ld(A,A),mult(ld(A,ld(A,A)),B)) = mult(A,mult(ld(A,rd(C,mult(A,C))),B)),
    inference(paramod,[status(thm)],[c_3866,c_12105]) ).

cnf(c_3927,plain,
    mult(A,mult(ld(A,rd(B,mult(A,B))),C)) = mult(ld(A,A),mult(ld(A,ld(A,A)),C)),
    inference(copy,[status(thm)],[c_12106]) ).

cnf(c_12107,plain,
    mult(ld(A,A),mult(rd(B,mult(A,B)),C)) = mult(A,mult(ld(A,rd(D,mult(A,D))),C)),
    inference(paramod,[status(thm)],[c_3866,c_1256]) ).

cnf(c_3933,plain,
    mult(ld(A,A),mult(rd(B,mult(A,B)),C)) = mult(ld(A,A),mult(ld(A,ld(A,A)),C)),
    inference(paramod,[status(thm)],[c_3927,c_12107]) ).

cnf(c_12108,plain,
    mult(A,mult(ld(A,A),mult(mult(rd(A,A),rd(B,mult(A,B))),C))) = mult(rd(A,A),C),
    inference(paramod,[status(thm)],[c_3866,c_796]) ).

cnf(c_12109,plain,
    mult(A,mult(ld(A,A),mult(mult(ld(A,A),rd(B,mult(A,B))),C))) = mult(rd(A,A),C),
    inference(paramod,[status(thm)],[c_3866,c_12108]) ).

cnf(c_12110,plain,
    mult(A,mult(ld(A,A),mult(mult(ld(A,A),ld(A,ld(A,A))),C))) = mult(rd(A,A),C),
    inference(paramod,[status(thm)],[c_3908,c_12109]) ).

cnf(c_3941,plain,
    mult(A,mult(ld(A,A),mult(mult(ld(A,A),ld(A,ld(A,A))),B))) = mult(ld(A,A),B),
    inference(paramod,[status(thm)],[c_3866,c_12110]) ).

cnf(c_12111,plain,
    mult(ld(A,A),mult(rd(B,mult(A,B)),C)) = mult(mult(rd(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
    inference(paramod,[status(thm)],[c_3866,c_504]) ).

cnf(c_12112,plain,
    mult(ld(A,A),mult(ld(A,ld(A,A)),C)) = mult(mult(rd(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
    inference(paramod,[status(thm)],[c_3933,c_12111]) ).

cnf(c_12113,plain,
    mult(ld(A,A),mult(ld(A,ld(A,A)),C)) = mult(mult(ld(A,A),rd(D,mult(A,D))),mult(rd(A,A),C)),
    inference(paramod,[status(thm)],[c_3866,c_12112]) ).

cnf(c_12114,plain,
    mult(ld(A,A),mult(ld(A,ld(A,A)),C)) = mult(mult(ld(A,A),ld(A,ld(A,A))),mult(rd(A,A),C)),
    inference(paramod,[status(thm)],[c_3908,c_12113]) ).

cnf(c_12115,plain,
    mult(ld(A,A),mult(ld(A,ld(A,A)),C)) = mult(mult(ld(A,A),ld(A,ld(A,A))),mult(ld(A,A),C)),
    inference(paramod,[status(thm)],[c_3866,c_12114]) ).

cnf(c_3949,plain,
    mult(mult(ld(A,A),ld(A,ld(A,A))),mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(A,ld(A,A)),B)),
    inference(copy,[status(thm)],[c_12115]) ).

cnf(c_12116,plain,
    rd(A,mult(B,A)) = mult(ld(B,ld(B,B)),rd(C,mult(rd(B,B),C))),
    inference(paramod,[status(thm)],[c_3866,c_327]) ).

cnf(c_12117,plain,
    rd(A,mult(B,A)) = mult(ld(B,ld(B,B)),rd(C,mult(ld(B,B),C))),
    inference(paramod,[status(thm)],[c_3866,c_12116]) ).

cnf(c_3954,plain,
    rd(A,mult(B,A)) = mult(ld(B,ld(B,B)),ld(B,B)),
    inference(paramod,[status(thm)],[c_372,c_12117]) ).

cnf(c_12118,plain,
    mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(rd(B,B),mult(mult(rd(B,B),ld(B,rd(B,B))),mult(rd(B,B),C))),
    inference(paramod,[status(thm)],[c_3954,c_318]) ).

cnf(c_12119,plain,
    mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(ld(B,B),mult(mult(rd(B,B),ld(B,rd(B,B))),mult(rd(B,B),C))),
    inference(paramod,[status(thm)],[c_3866,c_12118]) ).

cnf(c_12120,plain,
    mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(B,rd(B,B))),mult(rd(B,B),C))),
    inference(paramod,[status(thm)],[c_3866,c_12119]) ).

cnf(c_12121,plain,
    mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(B,ld(B,B))),mult(rd(B,B),C))),
    inference(paramod,[status(thm)],[c_3866,c_12120]) ).

cnf(c_12122,plain,
    mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(B,ld(B,B))),mult(ld(B,B),C))),
    inference(paramod,[status(thm)],[c_3866,c_12121]) ).

cnf(c_12123,plain,
    mult(mult(ld(B,ld(B,B)),ld(B,B)),C) = mult(ld(B,B),mult(ld(B,B),mult(ld(B,ld(B,B)),C))),
    inference(paramod,[status(thm)],[c_3949,c_12122]) ).

cnf(c_3955,plain,
    mult(mult(ld(A,ld(A,A)),ld(A,A)),B) = mult(ld(A,ld(A,A)),B),
    inference(paramod,[status(thm)],[c_373,c_12123]) ).

cnf(c_12124,plain,
    mult(mult(mult(ld(B,ld(B,B)),ld(B,B)),B),ld(B,rd(B,B))) = rd(A,mult(B,A)),
    inference(paramod,[status(thm)],[c_3954,c_3819]) ).

cnf(c_12125,plain,
    mult(mult(ld(B,ld(B,B)),B),ld(B,rd(B,B))) = rd(A,mult(B,A)),
    inference(paramod,[status(thm)],[c_3955,c_12124]) ).

cnf(c_12126,plain,
    mult(mult(ld(B,ld(B,B)),B),ld(B,ld(B,B))) = rd(A,mult(B,A)),
    inference(paramod,[status(thm)],[c_3866,c_12125]) ).

cnf(c_3960,plain,
    mult(mult(ld(A,ld(A,A)),A),ld(A,ld(A,A))) = mult(ld(A,ld(A,A)),ld(A,A)),
    inference(paramod,[status(thm)],[c_3954,c_12126]) ).

cnf(c_12127,plain,
    mult(A,ld(B,ld(B,B))) = ld(mult(mult(ld(A,rd(A,A)),A),ld(A,rd(A,A))),rd(C,mult(B,C))),
    inference(paramod,[status(thm)],[c_3866,c_3178]) ).

cnf(c_12128,plain,
    mult(A,ld(B,ld(B,B))) = ld(mult(mult(ld(A,ld(A,A)),A),ld(A,rd(A,A))),rd(C,mult(B,C))),
    inference(paramod,[status(thm)],[c_3866,c_12127]) ).

cnf(c_12129,plain,
    mult(A,ld(B,ld(B,B))) = ld(mult(mult(ld(A,ld(A,A)),A),ld(A,ld(A,A))),rd(C,mult(B,C))),
    inference(paramod,[status(thm)],[c_3866,c_12128]) ).

cnf(c_12130,plain,
    mult(A,ld(B,ld(B,B))) = ld(mult(ld(A,ld(A,A)),ld(A,A)),rd(C,mult(B,C))),
    inference(paramod,[status(thm)],[c_3960,c_12129]) ).

cnf(c_12131,plain,
    mult(A,ld(B,ld(B,B))) = ld(mult(ld(A,ld(A,A)),ld(A,A)),mult(ld(B,ld(B,B)),ld(B,B))),
    inference(paramod,[status(thm)],[c_3954,c_12130]) ).

cnf(c_12132,plain,
    mult(A,ld(B,ld(B,B))) = mult(A,mult(ld(B,ld(B,B)),ld(B,B))),
    inference(paramod,[status(thm)],[c_3896,c_12131]) ).

cnf(c_4042,plain,
    mult(A,mult(ld(B,ld(B,B)),ld(B,B))) = mult(A,ld(B,ld(B,B))),
    inference(copy,[status(thm)],[c_12132]) ).

cnf(c_12133,plain,
    mult(mult(ld(B,ld(B,B)),ld(B,B)),rd(B,B)) = mult(ld(B,B),rd(ld(C,rd(C,C)),mult(B,rd(D,mult(C,D))))),
    inference(paramod,[status(thm)],[c_3954,c_2677]) ).

cnf(c_12134,plain,
    mult(mult(ld(B,ld(B,B)),ld(B,B)),ld(B,B)) = mult(ld(B,B),rd(ld(C,rd(C,C)),mult(B,rd(D,mult(C,D))))),
    inference(paramod,[status(thm)],[c_3866,c_12133]) ).

cnf(c_12135,plain,
    mult(ld(B,ld(B,B)),ld(B,B)) = mult(ld(B,B),rd(ld(C,rd(C,C)),mult(B,rd(D,mult(C,D))))),
    inference(paramod,[status(thm)],[c_3955,c_12134]) ).

cnf(c_12136,plain,
    mult(ld(B,ld(B,B)),ld(B,B)) = mult(ld(B,B),rd(ld(C,ld(C,C)),mult(B,rd(D,mult(C,D))))),
    inference(paramod,[status(thm)],[c_3866,c_12135]) ).

cnf(c_12137,plain,
    mult(ld(B,ld(B,B)),ld(B,B)) = mult(ld(B,B),rd(ld(C,ld(C,C)),mult(B,mult(ld(C,ld(C,C)),ld(C,C))))),
    inference(paramod,[status(thm)],[c_3954,c_12136]) ).

cnf(c_12138,plain,
    mult(ld(B,ld(B,B)),ld(B,B)) = mult(ld(B,B),rd(ld(C,ld(C,C)),mult(B,ld(C,ld(C,C))))),
    inference(paramod,[status(thm)],[c_4042,c_12137]) ).

cnf(c_12139,plain,
    mult(ld(B,ld(B,B)),ld(B,B)) = mult(ld(B,B),mult(ld(B,ld(B,B)),ld(B,B))),
    inference(paramod,[status(thm)],[c_3954,c_12138]) ).

cnf(c_4104,plain,
    mult(ld(A,ld(A,A)),ld(A,A)) = mult(ld(A,A),ld(A,ld(A,A))),
    inference(paramod,[status(thm)],[c_4042,c_12139]) ).

cnf(c_12140,plain,
    mult(ld(A,ld(A,A)),rd(A,A)) = mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))),
    inference(paramod,[status(thm)],[c_3866,c_2670]) ).

cnf(c_12141,plain,
    mult(ld(A,ld(A,A)),ld(A,A)) = mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))),
    inference(paramod,[status(thm)],[c_3866,c_12140]) ).

cnf(c_12142,plain,
    mult(ld(A,A),ld(A,ld(A,A))) = mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))),
    inference(paramod,[status(thm)],[c_4104,c_12141]) ).

cnf(c_12143,plain,
    mult(ld(A,A),ld(A,ld(A,A))) = mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,rd(C,mult(B,C))))),
    inference(paramod,[status(thm)],[c_3866,c_12142]) ).

cnf(c_12144,plain,
    mult(ld(A,A),ld(A,ld(A,A))) = mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,ld(B,B)),ld(B,B))))),
    inference(paramod,[status(thm)],[c_3954,c_12143]) ).

cnf(c_12145,plain,
    mult(ld(A,A),ld(A,ld(A,A))) = mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,B),ld(B,ld(B,B)))))),
    inference(paramod,[status(thm)],[c_4104,c_12144]) ).

cnf(c_4105,plain,
    mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,B),ld(B,ld(B,B)))))) = mult(ld(A,A),ld(A,ld(A,A))),
    inference(copy,[status(thm)],[c_12145]) ).

cnf(c_12146,plain,
    mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,rd(C,mult(B,C))))) = ld(A,rd(A,A)),
    inference(paramod,[status(thm)],[c_3866,c_2647]) ).

cnf(c_12147,plain,
    mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,ld(B,B)),ld(B,B))))) = ld(A,rd(A,A)),
    inference(paramod,[status(thm)],[c_3954,c_12146]) ).

cnf(c_12148,plain,
    mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,B),ld(B,ld(B,B)))))) = ld(A,rd(A,A)),
    inference(paramod,[status(thm)],[c_4104,c_12147]) ).

cnf(c_12149,plain,
    mult(ld(A,A),ld(A,ld(A,A))) = ld(A,rd(A,A)),
    inference(paramod,[status(thm)],[c_4105,c_12148]) ).

cnf(c_4113,plain,
    mult(ld(A,A),ld(A,ld(A,A))) = ld(A,ld(A,A)),
    inference(paramod,[status(thm)],[c_3866,c_12149]) ).

cnf(c_12150,plain,
    rd(A,B) = mult(B,mult(mult(ld(B,ld(B,B)),A),ld(B,rd(B,B)))),
    inference(paramod,[status(thm)],[c_3866,c_2341]) ).

cnf(c_4129,plain,
    rd(A,B) = mult(B,mult(mult(ld(B,ld(B,B)),A),ld(B,ld(B,B)))),
    inference(paramod,[status(thm)],[c_3866,c_12150]) ).

cnf(c_12151,plain,
    mult(mult(ld(A,ld(A,A)),ld(B,A)),ld(A,rd(A,A))) = ld(A,ld(B,rd(B,B))),
    inference(paramod,[status(thm)],[c_3866,c_2333]) ).

cnf(c_12152,plain,
    mult(mult(ld(A,ld(A,A)),ld(B,A)),ld(A,ld(A,A))) = ld(A,ld(B,rd(B,B))),
    inference(paramod,[status(thm)],[c_3866,c_12151]) ).

cnf(c_4132,plain,
    mult(mult(ld(A,ld(A,A)),ld(B,A)),ld(A,ld(A,A))) = ld(A,ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_3866,c_12152]) ).

cnf(c_12153,plain,
    mult(ld(A,A),mult(ld(A,ld(A,A)),ld(A,rd(A,A)))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
    inference(paramod,[status(thm)],[c_3866,c_1653]) ).

cnf(c_12154,plain,
    mult(ld(A,A),mult(ld(A,ld(A,A)),ld(A,ld(A,A)))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
    inference(paramod,[status(thm)],[c_3866,c_12153]) ).

cnf(c_12155,plain,
    mult(ld(A,A),mult(ld(A,ld(A,A)),ld(A,ld(A,A)))) = mult(ld(A,ld(A,A)),ld(A,rd(A,A))),
    inference(paramod,[status(thm)],[c_3866,c_12154]) ).

cnf(c_4154,plain,
    mult(ld(A,A),mult(ld(A,ld(A,A)),ld(A,ld(A,A)))) = mult(ld(A,ld(A,A)),ld(A,ld(A,A))),
    inference(paramod,[status(thm)],[c_3866,c_12155]) ).

cnf(c_12156,plain,
    mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))) = mult(ld(B,rd(B,B)),rd(B,B)),
    inference(paramod,[status(thm)],[c_4129,c_167]) ).

cnf(c_12157,plain,
    mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))) = mult(ld(B,ld(B,B)),rd(B,B)),
    inference(paramod,[status(thm)],[c_3866,c_12156]) ).

cnf(c_12158,plain,
    mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))) = mult(ld(B,ld(B,B)),ld(B,B)),
    inference(paramod,[status(thm)],[c_3866,c_12157]) ).

cnf(c_12159,plain,
    mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))) = mult(ld(B,B),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_4104,c_12158]) ).

cnf(c_4210,plain,
    mult(mult(A,B),mult(mult(ld(mult(A,B),ld(mult(A,B),mult(A,B))),B),ld(mult(A,B),ld(mult(A,B),mult(A,B))))) = ld(A,ld(A,A)),
    inference(paramod,[status(thm)],[c_4113,c_12159]) ).

cnf(c_4214,plain,
    mult(ld(A,ld(B,ld(B,B))),C) = ld(A,mult(ld(B,A),ld(A,C))),
    inference(paramod,[status(thm)],[c_3866,c_147]) ).

cnf(c_12160,plain,
    mult(mult(ld(A,B),ld(A,ld(A,A))),C) = mult(ld(A,rd(A,A)),mult(B,mult(ld(A,rd(A,A)),C))),
    inference(paramod,[status(thm)],[c_3866,c_123]) ).

cnf(c_12161,plain,
    mult(mult(ld(A,B),ld(A,ld(A,A))),C) = mult(ld(A,ld(A,A)),mult(B,mult(ld(A,rd(A,A)),C))),
    inference(paramod,[status(thm)],[c_3866,c_12160]) ).

cnf(c_4221,plain,
    mult(mult(ld(A,B),ld(A,ld(A,A))),C) = mult(ld(A,ld(A,A)),mult(B,mult(ld(A,ld(A,A)),C))),
    inference(paramod,[status(thm)],[c_3866,c_12161]) ).

cnf(c_4223,plain,
    mult(ld(A,ld(A,A)),mult(A,B)) = B,
    inference(paramod,[status(thm)],[c_3866,c_121]) ).

cnf(c_4224,plain,
    mult(A,mult(ld(A,ld(A,A)),B)) = B,
    inference(paramod,[status(thm)],[c_3866,c_119]) ).

cnf(c_12162,plain,
    mult(mult(A,rd(mult(mult(A,B),mult(mult(ld(mult(A,B),ld(mult(A,B),mult(A,B))),B),ld(mult(A,B),ld(mult(A,B),mult(A,B))))),mult(A,mult(A,rd(C,mult(A,C)))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_4129,c_3079]) ).

cnf(c_12163,plain,
    mult(mult(A,rd(ld(A,ld(A,A)),mult(A,mult(A,rd(C,mult(A,C)))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_4210,c_12162]) ).

cnf(c_12164,plain,
    mult(mult(A,rd(ld(A,ld(A,A)),mult(A,mult(A,mult(mult(A,C),mult(mult(ld(mult(A,C),ld(mult(A,C),mult(A,C))),C),ld(mult(A,C),ld(mult(A,C),mult(A,C))))))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_4129,c_12163]) ).

cnf(c_12165,plain,
    mult(mult(A,rd(ld(A,ld(A,A)),mult(A,mult(A,ld(A,ld(A,A)))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_4210,c_12164]) ).

cnf(c_12166,plain,
    mult(mult(A,rd(ld(A,ld(A,A)),mult(A,ld(A,A)))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_7,c_12165]) ).

cnf(c_12167,plain,
    mult(mult(A,rd(ld(A,ld(A,A)),A)),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_7,c_12166]) ).

cnf(c_12168,plain,
    mult(mult(A,mult(A,mult(mult(ld(A,ld(A,A)),ld(A,ld(A,A))),ld(A,ld(A,A))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_4129,c_12167]) ).

cnf(c_12169,plain,
    mult(mult(A,mult(A,mult(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,ld(A,A)),ld(A,ld(A,A))))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_4221,c_12168]) ).

cnf(c_12170,plain,
    mult(mult(A,mult(A,mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),ld(A,ld(A,A)))))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_4154,c_12169]) ).

cnf(c_12171,plain,
    mult(mult(A,mult(ld(A,ld(A,A)),ld(A,ld(A,A)))),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_4224,c_12170]) ).

cnf(c_12172,plain,
    mult(ld(A,ld(A,A)),A) = mult(ld(A,A),mult(A,rd(C,mult(A,C)))),
    inference(paramod,[status(thm)],[c_4224,c_12171]) ).

cnf(c_12173,plain,
    mult(ld(A,ld(A,A)),A) = mult(ld(A,A),mult(A,mult(mult(A,C),mult(mult(ld(mult(A,C),ld(mult(A,C),mult(A,C))),C),ld(mult(A,C),ld(mult(A,C),mult(A,C))))))),
    inference(paramod,[status(thm)],[c_4129,c_12172]) ).

cnf(c_12174,plain,
    mult(ld(A,ld(A,A)),A) = mult(ld(A,A),mult(A,ld(A,ld(A,A)))),
    inference(paramod,[status(thm)],[c_4210,c_12173]) ).

cnf(c_4225,plain,
    mult(ld(A,ld(A,A)),A) = mult(ld(A,A),ld(A,A)),
    inference(paramod,[status(thm)],[c_7,c_12174]) ).

cnf(c_12175,plain,
    ld(mult(rd(mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))),mult(C,rd(D,mult(B,D)))),C),E) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_4129,c_3663]) ).

cnf(c_12176,plain,
    ld(mult(rd(ld(B,ld(B,B)),mult(C,rd(D,mult(B,D)))),C),E) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_4210,c_12175]) ).

cnf(c_12177,plain,
    ld(mult(rd(ld(B,ld(B,B)),mult(C,mult(mult(B,D),mult(mult(ld(mult(B,D),ld(mult(B,D),mult(B,D))),D),ld(mult(B,D),ld(mult(B,D),mult(B,D))))))),C),E) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_4129,c_12176]) ).

cnf(c_12178,plain,
    ld(mult(rd(ld(B,ld(B,B)),mult(C,ld(B,ld(B,B)))),C),E) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_4210,c_12177]) ).

cnf(c_12179,plain,
    ld(mult(mult(mult(C,ld(B,ld(B,B))),mult(mult(ld(mult(C,ld(B,ld(B,B))),ld(mult(C,ld(B,ld(B,B))),mult(C,ld(B,ld(B,B))))),ld(B,ld(B,B))),ld(mult(C,ld(B,ld(B,B))),ld(mult(C,ld(B,ld(B,B))),mult(C,ld(B,ld(B,B))))))),C),E) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_4129,c_12178]) ).

cnf(c_12180,plain,
    ld(mult(ld(C,ld(C,C)),C),E) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_4210,c_12179]) ).

cnf(c_12181,plain,
    ld(mult(ld(C,C),ld(C,C)),E) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_4225,c_12180]) ).

cnf(c_12182,plain,
    ld(ld(C,C),mult(ld(ld(C,C),ld(C,C)),ld(ld(C,C),E))) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_1000,c_12181]) ).

cnf(c_12183,plain,
    ld(ld(C,C),mult(mult(ld(C,C),ld(C,C)),ld(ld(C,C),E))) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_371,c_12182]) ).

cnf(c_12184,plain,
    ld(ld(C,C),mult(mult(ld(C,C),ld(C,C)),mult(ld(C,C),E))) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_371,c_12183]) ).

cnf(c_12185,plain,
    mult(ld(ld(C,C),ld(C,C)),mult(ld(C,C),mult(ld(C,C),E))) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_22,c_12184]) ).

cnf(c_12186,plain,
    mult(mult(ld(C,C),ld(C,C)),mult(ld(C,C),mult(ld(C,C),E))) = mult(ld(C,C),E),
    inference(paramod,[status(thm)],[c_371,c_12185]) ).

cnf(c_4228,plain,
    mult(mult(ld(A,A),ld(A,A)),B) = mult(ld(A,A),B),
    inference(paramod,[status(thm)],[c_373,c_12186]) ).

cnf(c_12187,plain,
    mult(mult(mult(mult(mult(B,A),mult(mult(ld(mult(B,A),ld(mult(B,A),mult(B,A))),A),ld(mult(B,A),ld(mult(B,A),mult(B,A))))),B),ld(B,B)),ld(B,B)) = ld(B,B),
    inference(paramod,[status(thm)],[c_4129,c_3639]) ).

cnf(c_12188,plain,
    mult(mult(mult(ld(B,ld(B,B)),B),ld(B,B)),ld(B,B)) = ld(B,B),
    inference(paramod,[status(thm)],[c_4210,c_12187]) ).

cnf(c_12189,plain,
    mult(mult(mult(ld(B,B),ld(B,B)),ld(B,B)),ld(B,B)) = ld(B,B),
    inference(paramod,[status(thm)],[c_4225,c_12188]) ).

cnf(c_12190,plain,
    mult(mult(ld(B,B),ld(B,B)),ld(B,B)) = ld(B,B),
    inference(paramod,[status(thm)],[c_4228,c_12189]) ).

cnf(c_4233,plain,
    mult(ld(A,A),ld(A,A)) = ld(A,A),
    inference(paramod,[status(thm)],[c_4228,c_12190]) ).

cnf(c_4235,plain,
    ld(mult(A,A),B) = mult(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,ld(A,A)),B))),
    inference(paramod,[status(thm)],[c_3920,c_1000]) ).

cnf(c_4293,plain,
    mult(ld(A,ld(A,A)),mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(A,ld(A,A)),B)),
    inference(paramod,[status(thm)],[c_4113,c_3949]) ).

cnf(c_4294,plain,
    mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))) = mult(ld(A,A),B),
    inference(paramod,[status(thm)],[c_4113,c_3941]) ).

cnf(c_4304,plain,
    ld(mult(A,A),B) = mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),B))),
    inference(paramod,[status(thm)],[c_4293,c_4235]) ).

cnf(c_12191,plain,
    mult(mult(A,A),ld(ld(A,A),B)) = mult(ld(A,A),mult(ld(ld(A,A),mult(A,A)),B)),
    inference(paramod,[status(thm)],[c_3879,c_45]) ).

cnf(c_12192,plain,
    mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(ld(A,A),mult(A,A)),B)),
    inference(paramod,[status(thm)],[c_371,c_12191]) ).

cnf(c_12193,plain,
    mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(mult(ld(A,A),mult(A,A)),B)),
    inference(paramod,[status(thm)],[c_371,c_12192]) ).

cnf(c_12194,plain,
    mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(mult(ld(A,A),A),mult(ld(A,A),mult(mult(ld(A,A),A),B)))),
    inference(paramod,[status(thm)],[c_988,c_12193]) ).

cnf(c_12195,plain,
    mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(A,mult(ld(A,A),mult(mult(ld(A,A),A),B)))),
    inference(paramod,[status(thm)],[c_3879,c_12194]) ).

cnf(c_12196,plain,
    mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(A,mult(ld(A,A),mult(A,B)))),
    inference(paramod,[status(thm)],[c_3879,c_12195]) ).

cnf(c_12197,plain,
    mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(mult(A,A),B)),
    inference(paramod,[status(thm)],[c_16,c_12196]) ).

cnf(c_4314,plain,
    mult(mult(A,A),mult(ld(A,A),B)) = mult(A,mult(A,B)),
    inference(paramod,[status(thm)],[c_3869,c_12197]) ).

cnf(c_12198,plain,
    mult(mult(A,A),ld(A,ld(A,A))) = mult(A,ld(A,A)),
    inference(paramod,[status(thm)],[c_4233,c_21]) ).

cnf(c_4315,plain,
    mult(mult(A,A),ld(A,ld(A,A))) = A,
    inference(paramod,[status(thm)],[c_7,c_12198]) ).

cnf(c_12199,plain,
    mult(mult(mult(A,A),ld(A,ld(A,A))),ld(ld(A,A),B)) = mult(mult(ld(A,A),ld(A,A)),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
    inference(paramod,[status(thm)],[c_4233,c_46]) ).

cnf(c_12200,plain,
    mult(A,ld(ld(A,A),B)) = mult(mult(ld(A,A),ld(A,A)),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
    inference(paramod,[status(thm)],[c_4315,c_12199]) ).

cnf(c_12201,plain,
    mult(A,mult(ld(A,A),B)) = mult(mult(ld(A,A),ld(A,A)),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
    inference(paramod,[status(thm)],[c_371,c_12200]) ).

cnf(c_12202,plain,
    mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
    inference(paramod,[status(thm)],[c_4233,c_12201]) ).

cnf(c_12203,plain,
    mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(ld(A,A),A),B)),
    inference(paramod,[status(thm)],[c_4233,c_12202]) ).

cnf(c_12204,plain,
    mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(mult(ld(A,A),A),B)),
    inference(paramod,[status(thm)],[c_371,c_12203]) ).

cnf(c_12205,plain,
    mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(A,B)),
    inference(paramod,[status(thm)],[c_3879,c_12204]) ).

cnf(c_4322,plain,
    mult(ld(A,A),mult(A,B)) = mult(A,mult(ld(A,A),B)),
    inference(copy,[status(thm)],[c_12205]) ).

cnf(c_12206,plain,
    ld(A,ld(B,C)) = mult(B,ld(mult(mult(B,A),B),C)),
    inference(paramod,[status(thm)],[c_95,c_8]) ).

cnf(c_4325,plain,
    mult(A,ld(mult(mult(A,B),A),C)) = ld(B,ld(A,C)),
    inference(copy,[status(thm)],[c_12206]) ).

cnf(c_12207,plain,
    mult(A,mult(ld(A,B),ld(mult(A,mult(ld(A,ld(A,B)),B)),C))) = ld(ld(A,B),C),
    inference(paramod,[status(thm)],[c_21,c_95]) ).

cnf(c_12208,plain,
    mult(A,mult(ld(A,B),ld(mult(mult(ld(A,B),A),ld(A,B)),C))) = ld(ld(A,B),C),
    inference(paramod,[status(thm)],[c_223,c_12207]) ).

cnf(c_12209,plain,
    mult(A,ld(A,ld(ld(A,B),C))) = ld(ld(A,B),C),
    inference(paramod,[status(thm)],[c_4325,c_12208]) ).

cnf(c_12210,plain,
    mult(A,ld(mult(B,A),mult(A,C))) = ld(ld(A,B),C),
    inference(paramod,[status(thm)],[c_728,c_12209]) ).

cnf(c_4330,plain,
    ld(ld(A,B),C) = mult(A,ld(mult(B,A),mult(A,C))),
    inference(copy,[status(thm)],[c_12210]) ).

cnf(c_12211,plain,
    mult(A,mult(ld(A,A),ld(mult(A,ld(A,A)),B))) = ld(ld(A,A),B),
    inference(paramod,[status(thm)],[c_3879,c_95]) ).

cnf(c_12212,plain,
    mult(A,mult(ld(A,A),ld(A,B))) = ld(ld(A,A),B),
    inference(paramod,[status(thm)],[c_7,c_12211]) ).

cnf(c_4344,plain,
    mult(A,mult(ld(A,A),ld(A,B))) = mult(ld(A,A),B),
    inference(paramod,[status(thm)],[c_371,c_12212]) ).

cnf(c_4382,plain,
    ld(mult(mult(A,B),A),mult(A,C)) = ld(A,ld(B,C)),
    inference(paramod,[status(thm)],[c_7,c_104]) ).

cnf(c_12213,plain,
    ld(ld(ld(A,A),B),mult(ld(A,A),C)) = mult(ld(A,A),ld(mult(B,ld(A,A)),C)),
    inference(paramod,[status(thm)],[c_373,c_4330]) ).

cnf(c_12214,plain,
    ld(mult(A,ld(mult(A,A),mult(A,B))),mult(ld(A,A),C)) = mult(ld(A,A),ld(mult(B,ld(A,A)),C)),
    inference(paramod,[status(thm)],[c_4330,c_12213]) ).

cnf(c_12215,plain,
    ld(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B))))),mult(ld(A,A),C)) = mult(ld(A,A),ld(mult(B,ld(A,A)),C)),
    inference(paramod,[status(thm)],[c_4304,c_12214]) ).

cnf(c_12216,plain,
    ld(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))),mult(ld(A,A),C)) = mult(ld(A,A),ld(mult(B,ld(A,A)),C)),
    inference(paramod,[status(thm)],[c_4223,c_12215]) ).

cnf(c_12217,plain,
    ld(mult(ld(A,A),B),mult(ld(A,A),C)) = mult(ld(A,A),ld(mult(B,ld(A,A)),C)),
    inference(paramod,[status(thm)],[c_4294,c_12216]) ).

cnf(c_4424,plain,
    mult(ld(A,A),ld(mult(B,ld(A,A)),C)) = ld(mult(ld(A,A),B),mult(ld(A,A),C)),
    inference(copy,[status(thm)],[c_12217]) ).

cnf(c_12218,plain,
    mult(mult(A,ld(mult(B,A),mult(A,ld(A,B)))),ld(A,B)) = ld(A,B),
    inference(paramod,[status(thm)],[c_4330,c_3879]) ).

cnf(c_4431,plain,
    mult(mult(A,ld(mult(B,A),B)),ld(A,B)) = ld(A,B),
    inference(paramod,[status(thm)],[c_7,c_12218]) ).

cnf(c_12219,plain,
    ld(ld(ld(A,A),B),A) = mult(ld(A,A),ld(mult(B,ld(A,A)),A)),
    inference(paramod,[status(thm)],[c_3879,c_4330]) ).

cnf(c_12220,plain,
    ld(mult(A,ld(mult(A,A),mult(A,B))),A) = mult(ld(A,A),ld(mult(B,ld(A,A)),A)),
    inference(paramod,[status(thm)],[c_4330,c_12219]) ).

cnf(c_12221,plain,
    ld(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,B))))),A) = mult(ld(A,A),ld(mult(B,ld(A,A)),A)),
    inference(paramod,[status(thm)],[c_4304,c_12220]) ).

cnf(c_12222,plain,
    ld(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),B))),A) = mult(ld(A,A),ld(mult(B,ld(A,A)),A)),
    inference(paramod,[status(thm)],[c_4223,c_12221]) ).

cnf(c_12223,plain,
    ld(mult(ld(A,A),B),A) = mult(ld(A,A),ld(mult(B,ld(A,A)),A)),
    inference(paramod,[status(thm)],[c_4294,c_12222]) ).

cnf(c_4432,plain,
    mult(ld(A,A),ld(mult(B,ld(A,A)),A)) = ld(mult(ld(A,A),B),A),
    inference(copy,[status(thm)],[c_12223]) ).

cnf(c_12224,plain,
    ld(mult(ld(A,ld(A,A)),B),C) = mult(A,ld(mult(B,A),mult(A,C))),
    inference(paramod,[status(thm)],[c_3925,c_4330]) ).

cnf(c_4440,plain,
    mult(A,ld(mult(B,A),mult(A,C))) = ld(mult(ld(A,ld(A,A)),B),C),
    inference(copy,[status(thm)],[c_12224]) ).

cnf(c_12225,plain,
    ld(ld(A,A),ld(mult(ld(A,A),B),A)) = ld(mult(B,ld(A,A)),A),
    inference(paramod,[status(thm)],[c_4432,c_8]) ).

cnf(c_12226,plain,
    mult(A,ld(mult(A,A),mult(A,ld(mult(ld(A,A),B),A)))) = ld(mult(B,ld(A,A)),A),
    inference(paramod,[status(thm)],[c_4330,c_12225]) ).

cnf(c_12227,plain,
    mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,ld(mult(ld(A,A),B),A)))))) = ld(mult(B,ld(A,A)),A),
    inference(paramod,[status(thm)],[c_4304,c_12226]) ).

cnf(c_12228,plain,
    mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,A),B),A)))) = ld(mult(B,ld(A,A)),A),
    inference(paramod,[status(thm)],[c_4223,c_12227]) ).

cnf(c_4494,plain,
    mult(ld(A,A),ld(mult(ld(A,A),B),A)) = ld(mult(B,ld(A,A)),A),
    inference(paramod,[status(thm)],[c_4294,c_12228]) ).

cnf(c_4516,plain,
    mult(mult(mult(A,A),ld(A,B)),mult(ld(A,A),ld(mult(B,ld(A,A)),A))) = mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),A),A)),
    inference(paramod,[status(thm)],[c_4432,c_46]) ).

cnf(c_12229,plain,
    mult(mult(A,ld(mult(B,A),mult(A,ld(A,B)))),mult(ld(A,B),C)) = mult(ld(A,B),mult(ld(ld(A,B),ld(A,B)),C)),
    inference(paramod,[status(thm)],[c_4330,c_4322]) ).

cnf(c_12230,plain,
    mult(mult(A,ld(mult(B,A),B)),mult(ld(A,B),C)) = mult(ld(A,B),mult(ld(ld(A,B),ld(A,B)),C)),
    inference(paramod,[status(thm)],[c_7,c_12229]) ).

cnf(c_12231,plain,
    mult(mult(A,ld(mult(B,A),B)),mult(ld(A,B),C)) = mult(ld(A,B),mult(mult(A,ld(mult(B,A),mult(A,ld(A,B)))),C)),
    inference(paramod,[status(thm)],[c_4330,c_12230]) ).

cnf(c_4596,plain,
    mult(mult(A,ld(mult(B,A),B)),mult(ld(A,B),C)) = mult(ld(A,B),mult(mult(A,ld(mult(B,A),B)),C)),
    inference(paramod,[status(thm)],[c_7,c_12231]) ).

cnf(c_12232,plain,
    ld(mult(A,ld(B,B)),mult(ld(B,B),C)) = ld(ld(B,B),ld(mult(ld(B,B),A),C)),
    inference(paramod,[status(thm)],[c_373,c_4382]) ).

cnf(c_12233,plain,
    ld(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(B,ld(mult(B,B),mult(B,ld(mult(ld(B,B),A),C)))),
    inference(paramod,[status(thm)],[c_4330,c_12232]) ).

cnf(c_12234,plain,
    ld(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(B,mult(ld(B,B),mult(ld(B,ld(B,B)),mult(ld(B,ld(B,B)),mult(B,ld(mult(ld(B,B),A),C)))))),
    inference(paramod,[status(thm)],[c_4304,c_12233]) ).

cnf(c_12235,plain,
    ld(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(B,mult(ld(B,B),mult(ld(B,ld(B,B)),ld(mult(ld(B,B),A),C)))),
    inference(paramod,[status(thm)],[c_4223,c_12234]) ).

cnf(c_12236,plain,
    ld(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),ld(mult(ld(B,B),A),C)),
    inference(paramod,[status(thm)],[c_4294,c_12235]) ).

cnf(c_4612,plain,
    mult(ld(A,A),ld(mult(ld(A,A),B),C)) = ld(mult(B,ld(A,A)),mult(ld(A,A),C)),
    inference(copy,[status(thm)],[c_12236]) ).

cnf(c_4653,plain,
    ld(mult(A,ld(mult(B,A),B)),ld(A,B)) = ld(A,B),
    inference(paramod,[status(thm)],[c_4431,c_8]) ).

cnf(c_12237,plain,
    ld(mult(ld(A,B),mult(A,ld(mult(B,A),B))),mult(mult(A,ld(mult(B,A),B)),mult(ld(A,B),C))) = ld(mult(A,ld(mult(B,A),B)),C),
    inference(paramod,[status(thm)],[c_4653,c_29]) ).

cnf(c_12238,plain,
    ld(ld(A,B),mult(mult(A,ld(mult(B,A),B)),mult(ld(A,B),C))) = ld(mult(A,ld(mult(B,A),B)),C),
    inference(paramod,[status(thm)],[c_334,c_12237]) ).

cnf(c_12239,plain,
    ld(ld(A,B),mult(ld(A,B),mult(mult(A,ld(mult(B,A),B)),C))) = ld(mult(A,ld(mult(B,A),B)),C),
    inference(paramod,[status(thm)],[c_4596,c_12238]) ).

cnf(c_12240,plain,
    mult(mult(A,ld(mult(B,A),B)),C) = ld(mult(A,ld(mult(B,A),B)),C),
    inference(paramod,[status(thm)],[c_8,c_12239]) ).

cnf(c_4705,plain,
    ld(mult(A,ld(mult(B,A),B)),C) = mult(mult(A,ld(mult(B,A),B)),C),
    inference(copy,[status(thm)],[c_12240]) ).

cnf(c_12241,plain,
    ld(mult(A,B),mult(B,C)) = ld(B,mult(ld(ld(B,A),ld(ld(B,A),ld(B,A))),C)),
    inference(paramod,[status(thm)],[c_4224,c_29]) ).

cnf(c_12242,plain,
    ld(mult(A,B),mult(B,C)) = ld(B,mult(ld(ld(B,A),mult(B,ld(mult(A,B),mult(B,ld(B,A))))),C)),
    inference(paramod,[status(thm)],[c_4330,c_12241]) ).

cnf(c_12243,plain,
    ld(mult(A,B),mult(B,C)) = ld(B,mult(ld(ld(B,A),mult(B,ld(mult(A,B),A))),C)),
    inference(paramod,[status(thm)],[c_7,c_12242]) ).

cnf(c_4764,plain,
    ld(mult(A,B),mult(B,C)) = ld(B,mult(mult(B,ld(mult(A,B),mult(B,mult(B,ld(mult(A,B),A))))),C)),
    inference(paramod,[status(thm)],[c_4330,c_12243]) ).

cnf(c_12244,plain,
    mult(ld(A,A),ld(mult(B,ld(A,A)),ld(ld(A,A),C))) = ld(mult(ld(A,A),B),C),
    inference(paramod,[status(thm)],[c_7,c_4424]) ).

cnf(c_12245,plain,
    mult(ld(A,A),ld(mult(B,ld(A,A)),mult(A,ld(mult(A,A),mult(A,C))))) = ld(mult(ld(A,A),B),C),
    inference(paramod,[status(thm)],[c_4330,c_12244]) ).

cnf(c_12246,plain,
    mult(ld(A,A),ld(mult(B,ld(A,A)),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,C))))))) = ld(mult(ld(A,A),B),C),
    inference(paramod,[status(thm)],[c_4304,c_12245]) ).

cnf(c_12247,plain,
    mult(ld(A,A),ld(mult(B,ld(A,A)),mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),C))))) = ld(mult(ld(A,A),B),C),
    inference(paramod,[status(thm)],[c_4223,c_12246]) ).

cnf(c_4784,plain,
    mult(ld(A,A),ld(mult(B,ld(A,A)),mult(ld(A,A),C))) = ld(mult(ld(A,A),B),C),
    inference(paramod,[status(thm)],[c_4294,c_12247]) ).

cnf(c_12248,plain,
    ld(ld(A,A),ld(mult(ld(A,A),B),mult(ld(A,A),C))) = ld(mult(B,ld(A,A)),C),
    inference(paramod,[status(thm)],[c_4424,c_8]) ).

cnf(c_12249,plain,
    mult(A,ld(mult(A,A),mult(A,ld(mult(ld(A,A),B),mult(ld(A,A),C))))) = ld(mult(B,ld(A,A)),C),
    inference(paramod,[status(thm)],[c_4330,c_12248]) ).

cnf(c_12250,plain,
    mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,ld(mult(ld(A,A),B),mult(ld(A,A),C))))))) = ld(mult(B,ld(A,A)),C),
    inference(paramod,[status(thm)],[c_4304,c_12249]) ).

cnf(c_12251,plain,
    mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),ld(mult(ld(A,A),B),mult(ld(A,A),C))))) = ld(mult(B,ld(A,A)),C),
    inference(paramod,[status(thm)],[c_4223,c_12250]) ).

cnf(c_4785,plain,
    mult(ld(A,A),ld(mult(ld(A,A),B),mult(ld(A,A),C))) = ld(mult(B,ld(A,A)),C),
    inference(paramod,[status(thm)],[c_4294,c_12251]) ).

cnf(c_12252,plain,
    mult(ld(A,A),mult(ld(B,B),ld(mult(ld(B,B),ld(A,A)),B))) = ld(mult(ld(B,B),ld(A,A)),mult(ld(A,A),B)),
    inference(paramod,[status(thm)],[c_4494,c_4612]) ).

cnf(c_4916,plain,
    ld(mult(ld(A,A),ld(B,B)),mult(ld(B,B),A)) = mult(ld(B,B),mult(ld(A,A),ld(mult(ld(A,A),ld(B,B)),A))),
    inference(copy,[status(thm)],[c_12252]) ).

cnf(c_12253,plain,
    mult(mult(ld(A,ld(A,A)),B),mult(ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),B)),ld(mult(ld(A,ld(A,A)),B),C))) = mult(mult(A,ld(mult(B,A),mult(A,mult(ld(A,ld(A,A)),B)))),C),
    inference(paramod,[status(thm)],[c_4440,c_4344]) ).

cnf(c_12254,plain,
    mult(ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),B)),C) = mult(mult(A,ld(mult(B,A),mult(A,mult(ld(A,ld(A,A)),B)))),C),
    inference(paramod,[status(thm)],[c_4344,c_12253]) ).

cnf(c_12255,plain,
    mult(ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),B)),C) = mult(mult(A,ld(mult(B,A),B)),C),
    inference(paramod,[status(thm)],[c_4224,c_12254]) ).

cnf(c_5081,plain,
    mult(mult(A,ld(mult(B,A),B)),C) = mult(ld(mult(ld(A,ld(A,A)),B),mult(ld(A,ld(A,A)),B)),C),
    inference(copy,[status(thm)],[c_12255]) ).

cnf(c_5178,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)))),
    inference(paramod,[status(thm)],[c_374,c_375]) ).

cnf(c_5179,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),mult(ld(A,A),C))) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))),
    inference(paramod,[status(thm)],[c_375,c_375]) ).

cnf(c_12256,plain,
    ld(mult(ld(A,B),ld(B,A)),C) = mult(mult(ld(A,B),ld(mult(A,ld(A,B)),A)),C),
    inference(paramod,[status(thm)],[c_7,c_4705]) ).

cnf(c_5180,plain,
    ld(mult(ld(A,B),ld(B,A)),C) = mult(mult(ld(A,B),ld(B,A)),C),
    inference(paramod,[status(thm)],[c_7,c_12256]) ).

cnf(c_5388,plain,
    ld(A,mult(ld(B,B),mult(mult(A,ld(B,B)),C))) = mult(ld(A,ld(B,B)),mult(A,mult(ld(B,B),C))),
    inference(paramod,[status(thm)],[c_385,c_22]) ).

cnf(c_5430,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),C))),
    inference(paramod,[status(thm)],[c_385,c_385]) ).

cnf(c_5591,plain,
    mult(mult(A,A),ld(mult(B,ld(A,A)),C)) = mult(A,mult(A,ld(mult(ld(A,A),B),mult(ld(A,A),C)))),
    inference(paramod,[status(thm)],[c_4785,c_4314]) ).

cnf(c_12257,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),C))) = mult(ld(B,B),mult(ld(B,B),ld(mult(ld(B,B),ld(A,A)),C))),
    inference(paramod,[status(thm)],[c_4612,c_637]) ).

cnf(c_5632,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),C))) = ld(mult(ld(B,B),ld(A,A)),C),
    inference(paramod,[status(thm)],[c_373,c_12257]) ).

cnf(c_5633,plain,
    mult(ld(A,A),ld(mult(ld(mult(ld(B,B),ld(A,A)),C),ld(A,A)),mult(ld(A,A),D))) = ld(mult(mult(ld(B,B),ld(A,A)),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),D),
    inference(paramod,[status(thm)],[c_637,c_4784]) ).

cnf(c_6268,plain,
    mult(ld(A,ld(mult(B,ld(C,C)),ld(mult(B,ld(C,C)),mult(B,ld(C,C))))),D) = ld(A,mult(mult(ld(C,C),ld(mult(ld(C,C),B),mult(ld(C,C),A))),ld(A,D))),
    inference(paramod,[status(thm)],[c_4785,c_4214]) ).

cnf(c_12258,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C)))) = mult(ld(B,B),mult(ld(B,B),C)),
    inference(paramod,[status(thm)],[c_788,c_637]) ).

cnf(c_6753,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C)))) = C,
    inference(paramod,[status(thm)],[c_373,c_12258]) ).

cnf(c_12259,plain,
    ld(mult(A,ld(B,B)),mult(ld(B,B),mult(A,ld(mult(ld(B,B),A),C)))) = mult(ld(B,B),mult(ld(mult(ld(B,B),A),ld(B,B)),C)),
    inference(paramod,[status(thm)],[c_637,c_788]) ).

cnf(c_6754,plain,
    mult(ld(A,A),mult(ld(mult(ld(A,A),B),ld(A,A)),C)) = ld(mult(B,ld(A,A)),mult(ld(A,A),mult(B,ld(mult(ld(A,A),B),C)))),
    inference(copy,[status(thm)],[c_12259]) ).

cnf(c_12260,plain,
    mult(mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),ld(A,A)))),C) = mult(ld(A,A),mult(B,mult(ld(A,A),C))),
    inference(paramod,[status(thm)],[c_980,c_11]) ).

cnf(c_6847,plain,
    mult(mult(ld(A,A),mult(mult(B,ld(A,A)),ld(A,A))),C) = mult(ld(A,A),mult(B,mult(ld(A,A),C))),
    inference(paramod,[status(thm)],[c_4233,c_12260]) ).

cnf(c_12261,plain,
    mult(A,mult(ld(A,mult(ld(B,B),C)),mult(A,D))) = mult(mult(ld(B,B),mult(mult(C,ld(B,B)),mult(ld(B,B),A))),D),
    inference(paramod,[status(thm)],[c_980,c_16]) ).

cnf(c_6848,plain,
    mult(mult(mult(ld(A,A),B),C),D) = mult(mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))),D),
    inference(paramod,[status(thm)],[c_16,c_12261]) ).

cnf(c_6880,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)))),
    inference(paramod,[status(thm)],[c_980,c_385]) ).

cnf(c_12262,plain,
    mult(mult(ld(A,A),mult(ld(B,B),ld(B,B))),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))))),
    inference(paramod,[status(thm)],[c_374,c_988]) ).

cnf(c_12263,plain,
    mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))))),
    inference(paramod,[status(thm)],[c_4233,c_12262]) ).

cnf(c_12264,plain,
    mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(B,B),mult(ld(B,B),mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),mult(mult(ld(A,A),ld(B,B)),C))))),
    inference(paramod,[status(thm)],[c_5430,c_12263]) ).

cnf(c_12265,plain,
    mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),mult(mult(ld(A,A),ld(B,B)),C))),
    inference(paramod,[status(thm)],[c_373,c_12264]) ).

cnf(c_6903,plain,
    mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),mult(mult(ld(A,A),ld(B,B)),C))) = mult(mult(ld(A,A),ld(B,B)),C),
    inference(copy,[status(thm)],[c_12265]) ).

cnf(c_12266,plain,
    mult(mult(ld(A,A),mult(ld(B,B),ld(B,B))),mult(ld(B,B),C)) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C)))),
    inference(paramod,[status(thm)],[c_375,c_988]) ).

cnf(c_12267,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C)))),
    inference(paramod,[status(thm)],[c_4233,c_12266]) ).

cnf(c_12268,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),mult(mult(ld(B,B),ld(A,A)),C)))),
    inference(paramod,[status(thm)],[c_5430,c_12267]) ).

cnf(c_6904,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),C)),
    inference(paramod,[status(thm)],[c_6903,c_12268]) ).

cnf(c_12269,plain,
    mult(mult(ld(A,A),mult(ld(B,B),ld(B,B))),mult(ld(B,B),ld(mult(ld(B,B),ld(A,A)),C))) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))),
    inference(paramod,[status(thm)],[c_749,c_988]) ).

cnf(c_12270,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),ld(mult(ld(B,B),ld(A,A)),C))) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))),
    inference(paramod,[status(thm)],[c_4233,c_12269]) ).

cnf(c_12271,plain,
    mult(ld(B,B),C) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))),
    inference(paramod,[status(thm)],[c_749,c_12270]) ).

cnf(c_12272,plain,
    mult(ld(B,B),C) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),C))),
    inference(paramod,[status(thm)],[c_5430,c_12271]) ).

cnf(c_6905,plain,
    mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),C))) = mult(ld(B,B),C),
    inference(copy,[status(thm)],[c_12272]) ).

cnf(c_12273,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)) = mult(ld(B,B),mult(ld(B,B),C)),
    inference(paramod,[status(thm)],[c_6905,c_6880]) ).

cnf(c_6906,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)) = C,
    inference(paramod,[status(thm)],[c_373,c_12273]) ).

cnf(c_6910,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(ld(A,A),C)),
    inference(paramod,[status(thm)],[c_6906,c_5178]) ).

cnf(c_12274,plain,
    mult(ld(B,B),mult(ld(A,A),C)) = mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),C)),
    inference(paramod,[status(thm)],[c_6910,c_6904]) ).

cnf(c_6911,plain,
    mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),C)) = mult(ld(B,B),mult(ld(A,A),C)),
    inference(copy,[status(thm)],[c_12274]) ).

cnf(c_12275,plain,
    mult(ld(B,B),mult(ld(A,A),mult(ld(A,A),C))) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))),
    inference(paramod,[status(thm)],[c_6910,c_5179]) ).

cnf(c_12276,plain,
    mult(ld(B,B),C) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))),
    inference(paramod,[status(thm)],[c_373,c_12275]) ).

cnf(c_6912,plain,
    mult(ld(A,A),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C))) = mult(ld(A,A),C),
    inference(copy,[status(thm)],[c_12276]) ).

cnf(c_12277,plain,
    mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))) = mult(mult(ld(A,A),ld(B,B)),C),
    inference(paramod,[status(thm)],[c_6911,c_6903]) ).

cnf(c_12278,plain,
    mult(ld(B,B),C) = mult(mult(ld(A,A),ld(B,B)),C),
    inference(paramod,[status(thm)],[c_6912,c_12277]) ).

cnf(c_6913,plain,
    mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(B,B),C),
    inference(copy,[status(thm)],[c_12278]) ).

cnf(c_12279,plain,
    mult(ld(A,A),mult(ld(A,A),C)) = mult(ld(B,B),mult(ld(A,A),C)),
    inference(paramod,[status(thm)],[c_6913,c_6911]) ).

cnf(c_12280,plain,
    C = mult(ld(B,B),mult(ld(A,A),C)),
    inference(paramod,[status(thm)],[c_373,c_12279]) ).

cnf(c_6915,plain,
    mult(ld(A,A),mult(ld(B,B),C)) = C,
    inference(copy,[status(thm)],[c_12280]) ).

cnf(c_12281,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),mult(ld(A,A),C)))) = C,
    inference(paramod,[status(thm)],[c_6913,c_6753]) ).

cnf(c_12282,plain,
    mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),C)) = C,
    inference(paramod,[status(thm)],[c_6915,c_12281]) ).

cnf(c_6916,plain,
    mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)) = C,
    inference(paramod,[status(thm)],[c_6913,c_12282]) ).

cnf(c_12283,plain,
    mult(ld(A,A),ld(mult(ld(mult(ld(B,B),ld(A,A)),C),ld(A,A)),mult(ld(A,A),D))) = ld(mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)),D),
    inference(paramod,[status(thm)],[c_6913,c_5633]) ).

cnf(c_6918,plain,
    mult(ld(A,A),ld(mult(ld(mult(ld(B,B),ld(A,A)),C),ld(A,A)),mult(ld(A,A),D))) = ld(C,D),
    inference(paramod,[status(thm)],[c_6916,c_12283]) ).

cnf(c_12284,plain,
    mult(ld(B,B),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),C))) = ld(mult(ld(B,B),ld(A,A)),C),
    inference(paramod,[status(thm)],[c_6913,c_5632]) ).

cnf(c_12285,plain,
    mult(ld(B,B),C) = ld(mult(ld(B,B),ld(A,A)),C),
    inference(paramod,[status(thm)],[c_6916,c_12284]) ).

cnf(c_6919,plain,
    ld(mult(ld(A,A),ld(B,B)),C) = mult(ld(A,A),C),
    inference(copy,[status(thm)],[c_12285]) ).

cnf(c_12286,plain,
    mult(ld(A,A),mult(ld(B,B),A)) = mult(ld(B,B),mult(ld(A,A),ld(mult(ld(A,A),ld(B,B)),A))),
    inference(paramod,[status(thm)],[c_6919,c_4916]) ).

cnf(c_12287,plain,
    A = mult(ld(B,B),mult(ld(A,A),ld(mult(ld(A,A),ld(B,B)),A))),
    inference(paramod,[status(thm)],[c_6915,c_12286]) ).

cnf(c_12288,plain,
    A = mult(ld(B,B),mult(ld(A,A),mult(ld(A,A),A))),
    inference(paramod,[status(thm)],[c_6919,c_12287]) ).

cnf(c_12289,plain,
    A = mult(ld(B,B),mult(ld(A,A),A)),
    inference(paramod,[status(thm)],[c_3879,c_12288]) ).

cnf(c_12290,plain,
    A = mult(ld(B,B),A),
    inference(paramod,[status(thm)],[c_3879,c_12289]) ).

cnf(c_6929,plain,
    mult(ld(A,A),B) = B,
    inference(copy,[status(thm)],[c_12290]) ).

cnf(c_12291,plain,
    mult(ld(A,A),ld(mult(ld(ld(A,A),C),ld(A,A)),mult(ld(A,A),D))) = ld(C,D),
    inference(paramod,[status(thm)],[c_6929,c_6918]) ).

cnf(c_12292,plain,
    mult(ld(A,A),ld(mult(mult(A,ld(mult(A,A),mult(A,C))),ld(A,A)),mult(ld(A,A),D))) = ld(C,D),
    inference(paramod,[status(thm)],[c_4330,c_12291]) ).

cnf(c_12293,plain,
    mult(ld(A,A),ld(mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),mult(ld(A,ld(A,A)),mult(A,C))))),ld(A,A)),mult(ld(A,A),D))) = ld(C,D),
    inference(paramod,[status(thm)],[c_4304,c_12292]) ).

cnf(c_12294,plain,
    mult(ld(A,A),ld(mult(mult(A,mult(ld(A,A),mult(ld(A,ld(A,A)),C))),ld(A,A)),mult(ld(A,A),D))) = ld(C,D),
    inference(paramod,[status(thm)],[c_4223,c_12293]) ).

cnf(c_12295,plain,
    mult(ld(A,A),ld(mult(mult(A,mult(ld(A,ld(A,A)),C)),ld(A,A)),mult(ld(A,A),D))) = ld(C,D),
    inference(paramod,[status(thm)],[c_6929,c_12294]) ).

cnf(c_12296,plain,
    mult(ld(A,A),ld(mult(C,ld(A,A)),mult(ld(A,A),D))) = ld(C,D),
    inference(paramod,[status(thm)],[c_4224,c_12295]) ).

cnf(c_12297,plain,
    mult(ld(A,A),ld(mult(C,ld(A,A)),D)) = ld(C,D),
    inference(paramod,[status(thm)],[c_6929,c_12296]) ).

cnf(c_6934,plain,
    ld(mult(A,ld(B,B)),C) = ld(A,C),
    inference(paramod,[status(thm)],[c_6929,c_12297]) ).

cnf(c_12298,plain,
    mult(mult(B,C),D) = mult(mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))),D),
    inference(paramod,[status(thm)],[c_6929,c_6848]) ).

cnf(c_12299,plain,
    mult(mult(B,C),D) = mult(mult(ld(A,A),mult(mult(B,ld(A,A)),C)),D),
    inference(paramod,[status(thm)],[c_6929,c_12298]) ).

cnf(c_12300,plain,
    mult(mult(B,C),D) = mult(mult(mult(B,ld(A,A)),C),D),
    inference(paramod,[status(thm)],[c_6929,c_12299]) ).

cnf(c_6973,plain,
    mult(mult(mult(A,ld(B,B)),C),D) = mult(mult(A,C),D),
    inference(copy,[status(thm)],[c_12300]) ).

cnf(c_12301,plain,
    mult(mult(mult(B,ld(A,A)),ld(A,A)),C) = mult(ld(A,A),mult(B,mult(ld(A,A),C))),
    inference(paramod,[status(thm)],[c_6929,c_6847]) ).

cnf(c_12302,plain,
    mult(mult(B,ld(A,A)),C) = mult(ld(A,A),mult(B,mult(ld(A,A),C))),
    inference(paramod,[status(thm)],[c_6973,c_12301]) ).

cnf(c_12303,plain,
    mult(mult(B,ld(A,A)),C) = mult(ld(A,A),mult(B,C)),
    inference(paramod,[status(thm)],[c_6929,c_12302]) ).

cnf(c_6974,plain,
    mult(mult(A,ld(B,B)),C) = mult(A,C),
    inference(paramod,[status(thm)],[c_6929,c_12303]) ).

cnf(c_12304,plain,
    mult(ld(A,A),mult(ld(B,ld(A,A)),C)) = ld(mult(B,ld(A,A)),mult(ld(A,A),mult(B,ld(mult(ld(A,A),B),C)))),
    inference(paramod,[status(thm)],[c_6929,c_6754]) ).

cnf(c_12305,plain,
    mult(ld(B,ld(A,A)),C) = ld(mult(B,ld(A,A)),mult(ld(A,A),mult(B,ld(mult(ld(A,A),B),C)))),
    inference(paramod,[status(thm)],[c_6929,c_12304]) ).

cnf(c_12306,plain,
    mult(ld(B,ld(A,A)),C) = ld(mult(B,ld(A,A)),mult(ld(A,A),mult(B,ld(B,C)))),
    inference(paramod,[status(thm)],[c_6929,c_12305]) ).

cnf(c_12307,plain,
    mult(ld(B,ld(A,A)),C) = ld(mult(B,ld(A,A)),mult(ld(A,A),C)),
    inference(paramod,[status(thm)],[c_7,c_12306]) ).

cnf(c_12308,plain,
    mult(ld(B,ld(A,A)),C) = ld(mult(B,ld(A,A)),C),
    inference(paramod,[status(thm)],[c_6929,c_12307]) ).

cnf(c_6988,plain,
    mult(ld(A,ld(B,B)),C) = ld(A,C),
    inference(paramod,[status(thm)],[c_6934,c_12308]) ).

cnf(c_12309,plain,
    mult(ld(A,ld(mult(B,ld(C,C)),ld(B,mult(B,ld(C,C))))),D) = ld(A,mult(mult(ld(C,C),ld(mult(ld(C,C),B),mult(ld(C,C),A))),ld(A,D))),
    inference(paramod,[status(thm)],[c_6934,c_6268]) ).

cnf(c_12310,plain,
    mult(ld(A,ld(mult(B,ld(C,C)),ld(C,C))),D) = ld(A,mult(mult(ld(C,C),ld(mult(ld(C,C),B),mult(ld(C,C),A))),ld(A,D))),
    inference(paramod,[status(thm)],[c_8,c_12309]) ).

cnf(c_12311,plain,
    mult(ld(A,ld(B,ld(C,C))),D) = ld(A,mult(mult(ld(C,C),ld(mult(ld(C,C),B),mult(ld(C,C),A))),ld(A,D))),
    inference(paramod,[status(thm)],[c_6934,c_12310]) ).

cnf(c_12312,plain,
    mult(ld(A,ld(B,ld(C,C))),D) = ld(A,mult(mult(ld(C,C),ld(B,mult(ld(C,C),A))),ld(A,D))),
    inference(paramod,[status(thm)],[c_6929,c_12311]) ).

cnf(c_12313,plain,
    mult(ld(A,ld(B,ld(C,C))),D) = ld(A,mult(mult(ld(C,C),ld(B,A)),ld(A,D))),
    inference(paramod,[status(thm)],[c_6929,c_12312]) ).

cnf(c_7026,plain,
    mult(ld(A,ld(B,ld(C,C))),D) = ld(A,mult(ld(B,A),ld(A,D))),
    inference(paramod,[status(thm)],[c_6929,c_12313]) ).

cnf(c_12314,plain,
    mult(mult(A,A),ld(B,C)) = mult(A,mult(A,ld(mult(ld(A,A),B),mult(ld(A,A),C)))),
    inference(paramod,[status(thm)],[c_6934,c_5591]) ).

cnf(c_12315,plain,
    mult(mult(A,A),ld(B,C)) = mult(A,mult(A,ld(B,mult(ld(A,A),C)))),
    inference(paramod,[status(thm)],[c_6929,c_12314]) ).

cnf(c_7062,plain,
    mult(mult(A,A),ld(B,C)) = mult(A,mult(A,ld(B,C))),
    inference(paramod,[status(thm)],[c_6929,c_12315]) ).

cnf(c_12316,plain,
    ld(A,mult(ld(B,B),mult(A,C))) = mult(ld(A,ld(B,B)),mult(A,mult(ld(B,B),C))),
    inference(paramod,[status(thm)],[c_6974,c_5388]) ).

cnf(c_12317,plain,
    ld(A,mult(A,C)) = mult(ld(A,ld(B,B)),mult(A,mult(ld(B,B),C))),
    inference(paramod,[status(thm)],[c_6929,c_12316]) ).

cnf(c_12318,plain,
    C = mult(ld(A,ld(B,B)),mult(A,mult(ld(B,B),C))),
    inference(paramod,[status(thm)],[c_8,c_12317]) ).

cnf(c_12319,plain,
    C = mult(ld(A,ld(B,B)),mult(A,C)),
    inference(paramod,[status(thm)],[c_6929,c_12318]) ).

cnf(c_7076,plain,
    mult(ld(A,ld(B,B)),mult(A,C)) = C,
    inference(copy,[status(thm)],[c_12319]) ).

cnf(c_7092,plain,
    mult(mult(A,ld(mult(B,A),B)),C) = C,
    inference(paramod,[status(thm)],[c_6929,c_5081]) ).

cnf(c_12320,plain,
    mult(mult(A,mult(A,ld(A,B))),mult(ld(A,A),ld(mult(B,ld(A,A)),A))) = mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),A),A)),
    inference(paramod,[status(thm)],[c_7062,c_4516]) ).

cnf(c_12321,plain,
    mult(mult(A,B),mult(ld(A,A),ld(mult(B,ld(A,A)),A))) = mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),A),A)),
    inference(paramod,[status(thm)],[c_7,c_12320]) ).

cnf(c_12322,plain,
    mult(mult(A,B),mult(ld(A,A),ld(B,A))) = mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),A),A)),
    inference(paramod,[status(thm)],[c_6934,c_12321]) ).

cnf(c_12323,plain,
    mult(mult(A,B),ld(B,A)) = mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),A),A)),
    inference(paramod,[status(thm)],[c_6929,c_12322]) ).

cnf(c_12324,plain,
    mult(mult(A,B),ld(B,A)) = mult(B,mult(ld(mult(ld(A,A),B),A),A)),
    inference(paramod,[status(thm)],[c_6929,c_12323]) ).

cnf(c_12325,plain,
    mult(mult(A,B),ld(B,A)) = mult(B,mult(ld(B,A),A)),
    inference(paramod,[status(thm)],[c_6929,c_12324]) ).

cnf(c_7111,plain,
    mult(A,mult(ld(A,B),B)) = mult(mult(B,A),ld(A,B)),
    inference(copy,[status(thm)],[c_12325]) ).

cnf(c_12326,negated_conjecture,
    ( sK0 != sK0
    | mult(sK0,ld(sK1,sK1)) != sK0 ),
    inference(paramod,[status(thm)],[c_6929,c_12]) ).

cnf(c_7118,negated_conjecture,
    mult(sK0,ld(sK1,sK1)) != sK0,
    inference(copy,[status(thm)],[c_12326]) ).

cnf(c_7281,plain,
    mult(mult(A,mult(mult(ld(B,C),ld(C,B)),mult(ld(B,C),ld(C,B)))),D) = mult(A,D),
    inference(paramod,[status(thm)],[c_5180,c_6974]) ).

cnf(c_7368,plain,
    mult(ld(A,mult(mult(ld(B,C),ld(C,B)),mult(ld(B,C),ld(C,B)))),D) = ld(A,D),
    inference(paramod,[status(thm)],[c_5180,c_6988]) ).

cnf(c_12327,plain,
    mult(ld(ld(A,B),ld(C,C)),ld(A,D)) = mult(A,ld(mult(B,A),D)),
    inference(paramod,[status(thm)],[c_334,c_7076]) ).

cnf(c_7578,plain,
    mult(mult(A,ld(mult(B,A),mult(A,ld(C,C)))),ld(A,D)) = mult(A,ld(mult(B,A),D)),
    inference(paramod,[status(thm)],[c_4330,c_12327]) ).

cnf(c_7602,plain,
    mult(mult(ld(A,B),ld(B,A)),C) = C,
    inference(paramod,[status(thm)],[c_7,c_7092]) ).

cnf(c_7664,plain,
    mult(ld(A,mult(ld(B,C),ld(C,B))),D) = ld(A,D),
    inference(paramod,[status(thm)],[c_7602,c_7368]) ).

cnf(c_7669,plain,
    mult(mult(A,mult(ld(B,C),ld(C,B))),D) = mult(A,D),
    inference(paramod,[status(thm)],[c_7602,c_7281]) ).

cnf(c_12328,plain,
    mult(ld(A,B),C) = ld(ld(B,A),C),
    inference(paramod,[status(thm)],[c_8,c_7664]) ).

cnf(c_12329,plain,
    mult(ld(A,B),C) = mult(B,ld(mult(A,B),mult(B,C))),
    inference(paramod,[status(thm)],[c_4330,c_12328]) ).

cnf(c_7880,plain,
    mult(A,ld(mult(B,A),mult(A,C))) = mult(ld(B,A),C),
    inference(copy,[status(thm)],[c_12329]) ).

cnf(c_12330,plain,
    mult(mult(ld(B,A),ld(C,C)),ld(A,D)) = mult(A,ld(mult(B,A),D)),
    inference(paramod,[status(thm)],[c_7880,c_7578]) ).

cnf(c_12331,plain,
    mult(ld(B,A),ld(A,D)) = mult(A,ld(mult(B,A),D)),
    inference(paramod,[status(thm)],[c_6974,c_12330]) ).

cnf(c_8070,plain,
    mult(A,ld(mult(B,A),C)) = mult(ld(B,A),ld(A,C)),
    inference(copy,[status(thm)],[c_12331]) ).

cnf(c_12332,plain,
    ld(mult(A,B),mult(B,C)) = ld(B,mult(mult(B,ld(mult(A,B),mult(B,mult(ld(A,B),ld(B,A))))),C)),
    inference(paramod,[status(thm)],[c_8070,c_4764]) ).

cnf(c_12333,plain,
    ld(mult(A,B),mult(B,C)) = ld(B,mult(mult(ld(A,B),ld(B,mult(B,mult(ld(A,B),ld(B,A))))),C)),
    inference(paramod,[status(thm)],[c_8070,c_12332]) ).

cnf(c_12334,plain,
    ld(mult(A,B),mult(B,C)) = ld(B,mult(mult(ld(A,B),mult(ld(A,B),ld(B,A))),C)),
    inference(paramod,[status(thm)],[c_8,c_12333]) ).

cnf(c_8159,plain,
    ld(mult(A,B),mult(B,C)) = ld(B,mult(ld(A,B),C)),
    inference(paramod,[status(thm)],[c_7669,c_12334]) ).

cnf(c_12335,plain,
    ld(ld(A,B),C) = mult(A,ld(A,mult(ld(B,A),C))),
    inference(paramod,[status(thm)],[c_8159,c_4330]) ).

cnf(c_8181,plain,
    ld(ld(A,B),C) = mult(ld(B,A),C),
    inference(paramod,[status(thm)],[c_7,c_12335]) ).

cnf(c_12336,plain,
    mult(ld(ld(A,A),mult(ld(ld(A,A),ld(A,A)),ld(ld(A,A),ld(B,ld(A,A))))),ld(ld(A,A),ld(ld(A,A),ld(A,A)))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_7026,c_4132]) ).

cnf(c_12337,plain,
    mult(ld(ld(A,A),mult(mult(ld(A,A),ld(A,A)),ld(ld(A,A),ld(B,ld(A,A))))),ld(ld(A,A),ld(ld(A,A),ld(A,A)))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_8181,c_12336]) ).

cnf(c_12338,plain,
    mult(ld(ld(A,A),mult(ld(A,A),ld(ld(A,A),ld(B,ld(A,A))))),ld(ld(A,A),ld(ld(A,A),ld(A,A)))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_6929,c_12337]) ).

cnf(c_12339,plain,
    mult(ld(ld(A,A),mult(ld(A,A),mult(ld(A,A),ld(B,ld(A,A))))),ld(ld(A,A),ld(ld(A,A),ld(A,A)))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_8181,c_12338]) ).

cnf(c_12340,plain,
    mult(ld(ld(A,A),mult(ld(A,A),ld(B,ld(A,A)))),ld(ld(A,A),ld(ld(A,A),ld(A,A)))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_6929,c_12339]) ).

cnf(c_12341,plain,
    mult(ld(ld(A,A),ld(B,ld(A,A))),ld(ld(A,A),ld(ld(A,A),ld(A,A)))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_6929,c_12340]) ).

cnf(c_12342,plain,
    mult(mult(ld(A,A),ld(B,ld(A,A))),ld(ld(A,A),ld(ld(A,A),ld(A,A)))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_8181,c_12341]) ).

cnf(c_12343,plain,
    mult(ld(B,ld(A,A)),ld(ld(A,A),ld(ld(A,A),ld(A,A)))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_6929,c_12342]) ).

cnf(c_12344,plain,
    mult(ld(B,ld(A,A)),ld(ld(A,A),mult(ld(A,A),ld(A,A)))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_8181,c_12343]) ).

cnf(c_12345,plain,
    mult(ld(B,ld(A,A)),ld(ld(A,A),ld(A,A))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_6929,c_12344]) ).

cnf(c_12346,plain,
    mult(ld(B,ld(A,A)),mult(ld(A,A),ld(A,A))) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_8181,c_12345]) ).

cnf(c_12347,plain,
    mult(ld(B,ld(A,A)),ld(A,A)) = ld(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_6929,c_12346]) ).

cnf(c_12348,plain,
    mult(ld(B,ld(A,A)),ld(A,A)) = mult(ld(A,A),ld(B,ld(B,B))),
    inference(paramod,[status(thm)],[c_8181,c_12347]) ).

cnf(c_11785,plain,
    mult(ld(A,ld(B,B)),ld(B,B)) = ld(A,ld(A,A)),
    inference(paramod,[status(thm)],[c_6929,c_12348]) ).

cnf(c_12349,plain,
    mult(A,mult(ld(A,ld(B,B)),ld(B,B))) = ld(A,A),
    inference(paramod,[status(thm)],[c_11785,c_7]) ).

cnf(c_12350,plain,
    mult(mult(ld(B,B),A),ld(A,ld(B,B))) = ld(A,A),
    inference(paramod,[status(thm)],[c_7111,c_12349]) ).

cnf(c_12351,plain,
    mult(A,ld(A,ld(B,B))) = ld(A,A),
    inference(paramod,[status(thm)],[c_6929,c_12350]) ).

cnf(c_11884,plain,
    ld(A,A) = ld(B,B),
    inference(paramod,[status(thm)],[c_7,c_12351]) ).

cnf(c_11961,plain,
    mult(A,ld(B,B)) = A,
    inference(paramod,[status(thm)],[c_11884,c_7]) ).

cnf(c_11962,plain,
    $false,
    inference(resolve,[status(thm)],[c_11961,c_7118]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP654+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04  % Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.36  % Computer : n004.cluster.edu
% 0.10/5.36  % Model    : x86_64 x86_64
% 0.10/5.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36  % Memory   : 8046.5625MB
% 0.10/5.36  % OS       : Linux 6.8.0-71-generic
% 0.10/5.36  % CPULimit : 300
% 0.10/5.36  % WCLimit  : 300
% 0.10/5.36  % DateTime : Fri Sep 25 15:29:45 UTC 2026
% 0.10/5.37  % CPUTime  : 
% 0.10/5.37  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.37  % Process 3541154 was started by sandbox on n004,
% 0.10/5.37  % Fri Sep 25 15:29:45 2026
% 0.10/5.37  % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/5.37  
% 0.10/5.37  % From the command line: assign(max_seconds, 300).
% 155.81/26.30  
% 155.81/26.30  % SZS status Theorem for theBenchmark
% 155.81/26.30  
% 155.81/26.30  % Proof 1 at 4.05 (+ 0.71) seconds.
% 155.81/26.30  % Length of proof is 235.
% 155.81/26.30  % Level of proof is 53.
% 155.81/26.30  % Maximum clause weight is 100.000.
% 155.81/26.30  % Given clauses 328.
% 155.81/26.30  
% 155.81/26.30  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------