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

%------------------------------------------------------------------------------
% File     : Prover9---2026-6A
% Problem  : GRP122-1 : TPTP v9.3.1. Released v1.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n006.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:27:25 AM UTC 2026

% Result   : Unsatisfiable 0.73s 0.58s
% Output   : CNFRefutation 0.73s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% Comments : 
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
    ! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,multiply(multiply(VAR_0,multiply(multiply(VAR_0,VAR_0),multiply(VAR_1,VAR_2))),multiply(VAR_2,multiply(VAR_2,VAR_2)))) = VAR_1,
    file('theBenchmark.p',single_axiom) ).

cnf(c_1,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),multiply(B,C))),multiply(C,multiply(C,C)))) = B,
    inference(clausify,[status(thm)],[single_axiom]) ).

fof(single_axiom2,axiom,
    multiply(identity,identity) = identity,
    file('theBenchmark.p',single_axiom2) ).

cnf(c_2,plain,
    multiply(identity,identity) = identity,
    inference(clausify,[status(thm)],[single_axiom2]) ).

fof(prove_order3,axiom,
    multiply(multiply(a,b),c) != multiply(a,multiply(b,c)),
    file('theBenchmark.p',prove_order3) ).

cnf(c_3,plain,
    multiply(multiply(a,b),c) != multiply(a,multiply(b,c)),
    inference(clausify,[status(thm)],[prove_order3]) ).

cnf(c_4,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,B))),multiply(B,multiply(B,B)))) = A,
    inference(paramod,[status(thm)],[c_2,c_1]) ).

cnf(c_348,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),multiply(B,identity))),multiply(identity,identity))) = B,
    inference(paramod,[status(thm)],[c_2,c_1]) ).

cnf(c_6,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),multiply(B,identity))),identity)) = B,
    inference(paramod,[status(thm)],[c_2,c_348]) ).

cnf(c_349,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,identity))),multiply(identity,identity))) = A,
    inference(paramod,[status(thm)],[c_2,c_4]) ).

cnf(c_7,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,identity))),identity)) = A,
    inference(paramod,[status(thm)],[c_2,c_349]) ).

cnf(c_350,plain,
    multiply(A,multiply(multiply(A,B),multiply(identity,multiply(identity,identity)))) = multiply(multiply(A,A),multiply(multiply(multiply(A,A),multiply(A,A)),multiply(B,identity))),
    inference(paramod,[status(thm)],[c_6,c_1]) ).

cnf(c_351,plain,
    multiply(A,multiply(multiply(A,B),multiply(identity,identity))) = multiply(multiply(A,A),multiply(multiply(multiply(A,A),multiply(A,A)),multiply(B,identity))),
    inference(paramod,[status(thm)],[c_2,c_350]) ).

cnf(c_352,plain,
    multiply(A,multiply(multiply(A,B),identity)) = multiply(multiply(A,A),multiply(multiply(multiply(A,A),multiply(A,A)),multiply(B,identity))),
    inference(paramod,[status(thm)],[c_2,c_351]) ).

cnf(c_9,plain,
    multiply(multiply(A,A),multiply(multiply(multiply(A,A),multiply(A,A)),multiply(B,identity))) = multiply(A,multiply(multiply(A,B),identity)),
    inference(copy,[status(thm)],[c_352]) ).

cnf(c_353,plain,
    multiply(identity,multiply(multiply(identity,A),multiply(identity,multiply(identity,identity)))) = multiply(identity,multiply(multiply(identity,identity),multiply(A,identity))),
    inference(paramod,[status(thm)],[c_6,c_4]) ).

cnf(c_354,plain,
    multiply(identity,multiply(multiply(identity,A),multiply(identity,identity))) = multiply(identity,multiply(multiply(identity,identity),multiply(A,identity))),
    inference(paramod,[status(thm)],[c_2,c_353]) ).

cnf(c_355,plain,
    multiply(identity,multiply(multiply(identity,A),identity)) = multiply(identity,multiply(multiply(identity,identity),multiply(A,identity))),
    inference(paramod,[status(thm)],[c_2,c_354]) ).

cnf(c_10,plain,
    multiply(identity,multiply(multiply(identity,A),identity)) = multiply(identity,multiply(identity,multiply(A,identity))),
    inference(paramod,[status(thm)],[c_2,c_355]) ).

cnf(c_356,plain,
    multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,identity)),identity))) = A,
    inference(paramod,[status(thm)],[c_10,c_7]) ).

cnf(c_11,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),identity)))) = A,
    inference(paramod,[status(thm)],[c_10,c_356]) ).

cnf(c_357,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,identity))),identity)) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,A),identity),identity))),
    inference(paramod,[status(thm)],[c_10,c_10]) ).

cnf(c_358,plain,
    multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,identity)),identity))) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,A),identity),identity))),
    inference(paramod,[status(thm)],[c_10,c_357]) ).

cnf(c_359,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),identity)))) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,A),identity),identity))),
    inference(paramod,[status(thm)],[c_10,c_358]) ).

cnf(c_360,plain,
    A = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,A),identity),identity))),
    inference(paramod,[status(thm)],[c_11,c_359]) ).

cnf(c_13,plain,
    multiply(identity,multiply(identity,multiply(multiply(multiply(identity,A),identity),identity))) = A,
    inference(copy,[status(thm)],[c_360]) ).

cnf(c_361,plain,
    multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))) = multiply(multiply(identity,multiply(multiply(identity,identity),multiply(A,B))),multiply(B,multiply(B,B))),
    inference(paramod,[status(thm)],[c_1,c_13]) ).

cnf(c_362,plain,
    multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))) = multiply(multiply(identity,multiply(identity,multiply(A,B))),multiply(B,multiply(B,B))),
    inference(paramod,[status(thm)],[c_2,c_361]) ).

cnf(c_14,plain,
    multiply(multiply(identity,multiply(identity,multiply(A,B))),multiply(B,multiply(B,B))) = multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),
    inference(copy,[status(thm)],[c_362]) ).

cnf(c_363,plain,
    multiply(identity,multiply(A,multiply(identity,multiply(identity,identity)))) = multiply(multiply(identity,A),identity),
    inference(paramod,[status(thm)],[c_13,c_4]) ).

cnf(c_364,plain,
    multiply(identity,multiply(A,multiply(identity,identity))) = multiply(multiply(identity,A),identity),
    inference(paramod,[status(thm)],[c_2,c_363]) ).

cnf(c_365,plain,
    multiply(identity,multiply(A,identity)) = multiply(multiply(identity,A),identity),
    inference(paramod,[status(thm)],[c_2,c_364]) ).

cnf(c_15,plain,
    multiply(multiply(identity,A),identity) = multiply(identity,multiply(A,identity)),
    inference(copy,[status(thm)],[c_365]) ).

cnf(c_366,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),multiply(identity,multiply(B,identity)))),multiply(identity,multiply(identity,identity)))) = multiply(identity,B),
    inference(paramod,[status(thm)],[c_15,c_1]) ).

cnf(c_367,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),multiply(identity,multiply(B,identity)))),multiply(identity,identity))) = multiply(identity,B),
    inference(paramod,[status(thm)],[c_2,c_366]) ).

cnf(c_16,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),multiply(identity,multiply(B,identity)))),identity)) = multiply(identity,B),
    inference(paramod,[status(thm)],[c_2,c_367]) ).

cnf(c_368,plain,
    multiply(multiply(A,A),multiply(multiply(A,multiply(multiply(A,B),identity)),multiply(identity,multiply(identity,identity)))) = B,
    inference(paramod,[status(thm)],[c_9,c_1]) ).

cnf(c_369,plain,
    multiply(multiply(A,A),multiply(multiply(A,multiply(multiply(A,B),identity)),multiply(identity,identity))) = B,
    inference(paramod,[status(thm)],[c_2,c_368]) ).

cnf(c_20,plain,
    multiply(multiply(A,A),multiply(multiply(A,multiply(multiply(A,B),identity)),identity)) = B,
    inference(paramod,[status(thm)],[c_2,c_369]) ).

cnf(c_370,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(A,multiply(A,A))) = multiply(identity,multiply(identity,multiply(identity,identity))),
    inference(paramod,[status(thm)],[c_2,c_14]) ).

cnf(c_371,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(A,multiply(A,A))) = multiply(identity,multiply(identity,identity)),
    inference(paramod,[status(thm)],[c_2,c_370]) ).

cnf(c_372,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(A,multiply(A,A))) = multiply(identity,identity),
    inference(paramod,[status(thm)],[c_2,c_371]) ).

cnf(c_24,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(A,multiply(A,A))) = identity,
    inference(paramod,[status(thm)],[c_2,c_372]) ).

cnf(c_373,plain,
    multiply(A,multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(A,identity),identity),multiply(multiply(A,identity),identity)))) = multiply(identity,multiply(identity,multiply(multiply(identity,identity),identity))),
    inference(paramod,[status(thm)],[c_11,c_14]) ).

cnf(c_374,plain,
    multiply(A,multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(A,identity),identity),multiply(multiply(A,identity),identity)))) = multiply(identity,multiply(identity,multiply(identity,identity))),
    inference(paramod,[status(thm)],[c_2,c_373]) ).

cnf(c_375,plain,
    multiply(A,multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(A,identity),identity),multiply(multiply(A,identity),identity)))) = multiply(identity,multiply(identity,identity)),
    inference(paramod,[status(thm)],[c_2,c_374]) ).

cnf(c_376,plain,
    multiply(A,multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(A,identity),identity),multiply(multiply(A,identity),identity)))) = multiply(identity,identity),
    inference(paramod,[status(thm)],[c_2,c_375]) ).

cnf(c_25,plain,
    multiply(A,multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(A,identity),identity),multiply(multiply(A,identity),identity)))) = identity,
    inference(paramod,[status(thm)],[c_2,c_376]) ).

cnf(c_377,plain,
    multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),B))),multiply(B,multiply(B,B))) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,identity)),identity))),
    inference(paramod,[status(thm)],[c_15,c_14]) ).

cnf(c_378,plain,
    multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),B))),multiply(B,multiply(B,B))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),identity)))),
    inference(paramod,[status(thm)],[c_15,c_377]) ).

cnf(c_26,plain,
    multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),B))),multiply(B,multiply(B,B))) = A,
    inference(paramod,[status(thm)],[c_11,c_378]) ).

cnf(c_379,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),B)),identity)) = multiply(identity,multiply(identity,multiply(multiply(identity,identity),multiply(B,identity)))),
    inference(paramod,[status(thm)],[c_6,c_16]) ).

cnf(c_27,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),B)),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(B,identity)))),
    inference(paramod,[status(thm)],[c_2,c_379]) ).

cnf(c_380,plain,
    multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))),
    inference(paramod,[status(thm)],[c_24,c_14]) ).

cnf(c_381,plain,
    multiply(multiply(identity,identity),multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))),
    inference(paramod,[status(thm)],[c_2,c_380]) ).

cnf(c_382,plain,
    multiply(identity,multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))),
    inference(paramod,[status(thm)],[c_2,c_381]) ).

cnf(c_383,plain,
    multiply(identity,multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(identity,multiply(identity,A)),identity)),identity))),
    inference(paramod,[status(thm)],[c_15,c_382]) ).

cnf(c_384,plain,
    multiply(identity,multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),identity))),identity))),
    inference(paramod,[status(thm)],[c_15,c_383]) ).

cnf(c_385,plain,
    multiply(identity,multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,identity)))),identity))),
    inference(paramod,[status(thm)],[c_15,c_384]) ).

cnf(c_386,plain,
    multiply(identity,multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,identity))),identity)))),
    inference(paramod,[status(thm)],[c_15,c_385]) ).

cnf(c_387,plain,
    multiply(identity,multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))) = multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,identity)),identity))))),
    inference(paramod,[status(thm)],[c_15,c_386]) ).

cnf(c_388,plain,
    multiply(identity,multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))) = multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),identity)))))),
    inference(paramod,[status(thm)],[c_15,c_387]) ).

cnf(c_28,plain,
    multiply(identity,multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))) = multiply(identity,multiply(identity,A)),
    inference(paramod,[status(thm)],[c_11,c_388]) ).

cnf(c_389,plain,
    multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,identity)),identity)) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_24,c_20]) ).

cnf(c_390,plain,
    multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity)) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_2,c_389]) ).

cnf(c_391,plain,
    multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,A)),identity)),identity)) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_15,c_390]) ).

cnf(c_392,plain,
    multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),identity))),identity)) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_15,c_391]) ).

cnf(c_393,plain,
    multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,identity)))),identity)) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_15,c_392]) ).

cnf(c_394,plain,
    multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,identity))),identity))) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_15,c_393]) ).

cnf(c_395,plain,
    multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,identity)),identity)))) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_15,c_394]) ).

cnf(c_396,plain,
    multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))))) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_15,c_395]) ).

cnf(c_30,plain,
    multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),A) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_11,c_396]) ).

cnf(c_397,plain,
    multiply(multiply(A,A),multiply(multiply(A,multiply(multiply(identity,multiply(identity,multiply(identity,multiply(B,identity)))),identity)),identity)) = multiply(multiply(A,multiply(multiply(A,A),B)),identity),
    inference(paramod,[status(thm)],[c_27,c_20]) ).

cnf(c_398,plain,
    multiply(multiply(A,A),multiply(multiply(A,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(B,identity))),identity))),identity)) = multiply(multiply(A,multiply(multiply(A,A),B)),identity),
    inference(paramod,[status(thm)],[c_15,c_397]) ).

cnf(c_399,plain,
    multiply(multiply(A,A),multiply(multiply(A,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(B,identity)),identity)))),identity)) = multiply(multiply(A,multiply(multiply(A,A),B)),identity),
    inference(paramod,[status(thm)],[c_15,c_398]) ).

cnf(c_400,plain,
    multiply(multiply(A,A),multiply(multiply(A,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(B,identity),identity))))),identity)) = multiply(multiply(A,multiply(multiply(A,A),B)),identity),
    inference(paramod,[status(thm)],[c_15,c_399]) ).

cnf(c_401,plain,
    multiply(multiply(A,A),multiply(multiply(A,B),identity)) = multiply(multiply(A,multiply(multiply(A,A),B)),identity),
    inference(paramod,[status(thm)],[c_11,c_400]) ).

cnf(c_31,plain,
    multiply(multiply(A,multiply(multiply(A,A),B)),identity) = multiply(multiply(A,A),multiply(multiply(A,B),identity)),
    inference(copy,[status(thm)],[c_401]) ).

cnf(c_32,plain,
    multiply(A,multiply(multiply(A,A),multiply(multiply(A,B),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(B,identity)))),
    inference(paramod,[status(thm)],[c_31,c_27]) ).

cnf(c_35,plain,
    multiply(multiply(A,A),multiply(multiply(A,A),multiply(multiply(A,identity),identity))) = A,
    inference(paramod,[status(thm)],[c_31,c_20]) ).

cnf(c_402,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,B)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,B)))),multiply(multiply(A,B),multiply(multiply(A,B),multiply(A,B)))),multiply(B,multiply(B,B)))) = A,
    inference(paramod,[status(thm)],[c_30,c_1]) ).

cnf(c_37,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,B)))),multiply(identity,multiply(B,multiply(B,B)))) = A,
    inference(paramod,[status(thm)],[c_24,c_402]) ).

cnf(c_403,plain,
    multiply(multiply(identity,multiply(identity,A)),multiply(identity,multiply(multiply(B,multiply(B,B)),multiply(multiply(B,multiply(B,B)),multiply(B,multiply(B,B)))))) = multiply(identity,multiply(multiply(identity,identity),multiply(A,B))),
    inference(paramod,[status(thm)],[c_1,c_37]) ).

cnf(c_404,plain,
    multiply(multiply(identity,multiply(identity,A)),multiply(identity,multiply(identity,B))) = multiply(identity,multiply(multiply(identity,identity),multiply(A,B))),
    inference(paramod,[status(thm)],[c_28,c_403]) ).

cnf(c_38,plain,
    multiply(multiply(identity,multiply(identity,A)),multiply(identity,multiply(identity,B))) = multiply(identity,multiply(identity,multiply(A,B))),
    inference(paramod,[status(thm)],[c_2,c_404]) ).

cnf(c_39,plain,
    multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),multiply(identity,A)))),A) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_38,c_30]) ).

cnf(c_405,plain,
    multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,A)),identity)),identity)) = multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A)))),
    inference(paramod,[status(thm)],[c_28,c_20]) ).

cnf(c_406,plain,
    multiply(identity,multiply(multiply(identity,multiply(multiply(identity,multiply(identity,A)),identity)),identity)) = multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A)))),
    inference(paramod,[status(thm)],[c_2,c_405]) ).

cnf(c_407,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),identity))),identity)) = multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A)))),
    inference(paramod,[status(thm)],[c_15,c_406]) ).

cnf(c_408,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,identity)))),identity)) = multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A)))),
    inference(paramod,[status(thm)],[c_15,c_407]) ).

cnf(c_409,plain,
    multiply(identity,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,identity))),identity))) = multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A)))),
    inference(paramod,[status(thm)],[c_15,c_408]) ).

cnf(c_410,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,identity)),identity)))) = multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A)))),
    inference(paramod,[status(thm)],[c_15,c_409]) ).

cnf(c_411,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))))) = multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A)))),
    inference(paramod,[status(thm)],[c_15,c_410]) ).

cnf(c_412,plain,
    multiply(identity,A) = multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A)))),
    inference(paramod,[status(thm)],[c_11,c_411]) ).

cnf(c_40,plain,
    multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A)))) = multiply(identity,A),
    inference(copy,[status(thm)],[c_412]) ).

cnf(c_413,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(B,multiply(B,B)))))),multiply(identity,multiply(identity,B))) = A,
    inference(paramod,[status(thm)],[c_28,c_37]) ).

cnf(c_41,plain,
    multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,multiply(B,multiply(B,B)))),B))) = A,
    inference(paramod,[status(thm)],[c_38,c_413]) ).

cnf(c_414,plain,
    multiply(A,multiply(identity,multiply(identity,B))) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(A,identity),identity)),B))),
    inference(paramod,[status(thm)],[c_11,c_38]) ).

cnf(c_42,plain,
    multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(A,identity),identity)),B))) = multiply(A,multiply(identity,multiply(identity,B))),
    inference(copy,[status(thm)],[c_414]) ).

cnf(c_43,plain,
    multiply(multiply(identity,multiply(identity,A)),B) = multiply(identity,multiply(identity,multiply(A,multiply(identity,multiply(multiply(B,identity),identity))))),
    inference(paramod,[status(thm)],[c_11,c_38]) ).

cnf(c_47,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(A,A))))),multiply(identity,A)) = identity,
    inference(paramod,[status(thm)],[c_40,c_24]) ).

cnf(c_48,plain,
    multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),multiply(B,multiply(B,B))))),multiply(identity,B)) = A,
    inference(paramod,[status(thm)],[c_40,c_26]) ).

cnf(c_55,plain,
    multiply(multiply(identity,A),multiply(identity,multiply(B,multiply(B,B)))) = multiply(identity,multiply(A,multiply(B,multiply(B,B)))),
    inference(paramod,[status(thm)],[c_41,c_37]) ).

cnf(c_415,plain,
    multiply(multiply(identity,A),multiply(identity,multiply(identity,B))) = multiply(identity,multiply(A,multiply(multiply(B,multiply(B,B)),multiply(multiply(B,multiply(B,B)),multiply(B,multiply(B,B)))))),
    inference(paramod,[status(thm)],[c_40,c_55]) ).

cnf(c_57,plain,
    multiply(multiply(identity,A),multiply(identity,multiply(identity,B))) = multiply(identity,multiply(A,multiply(identity,B))),
    inference(paramod,[status(thm)],[c_40,c_415]) ).

cnf(c_58,plain,
    multiply(identity,multiply(multiply(identity,A),multiply(identity,B))) = multiply(identity,multiply(identity,multiply(A,B))),
    inference(paramod,[status(thm)],[c_57,c_38]) ).

cnf(c_60,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),A) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_58,c_39]) ).

cnf(c_416,plain,
    multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(A,identity),identity)),multiply(identity,multiply(multiply(B,identity),identity))))) = multiply(A,B),
    inference(paramod,[status(thm)],[c_11,c_42]) ).

cnf(c_62,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),multiply(multiply(B,identity),identity))))) = multiply(A,B),
    inference(paramod,[status(thm)],[c_58,c_416]) ).

cnf(c_417,plain,
    multiply(multiply(A,multiply(identity,multiply(identity,B))),multiply(B,multiply(B,B))) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(A,identity),identity)),identity),identity))),
    inference(paramod,[status(thm)],[c_42,c_14]) ).

cnf(c_418,plain,
    multiply(multiply(A,multiply(identity,multiply(identity,B))),multiply(B,multiply(B,B))) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),identity))),
    inference(paramod,[status(thm)],[c_15,c_417]) ).

cnf(c_419,plain,
    multiply(multiply(A,multiply(identity,multiply(identity,B))),multiply(B,multiply(B,B))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(A,identity),identity),identity),identity)))),
    inference(paramod,[status(thm)],[c_15,c_418]) ).

cnf(c_63,plain,
    multiply(multiply(A,multiply(identity,multiply(identity,B))),multiply(B,multiply(B,B))) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_11,c_419]) ).

cnf(c_420,plain,
    multiply(multiply(identity,multiply(A,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(A,identity),identity)),multiply(identity,multiply(multiply(A,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(A,identity),identity)))) = identity,
    inference(paramod,[status(thm)],[c_42,c_47]) ).

cnf(c_421,plain,
    multiply(multiply(identity,multiply(A,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),multiply(multiply(A,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(A,identity),identity)))) = identity,
    inference(paramod,[status(thm)],[c_58,c_420]) ).

cnf(c_422,plain,
    multiply(multiply(identity,multiply(A,multiply(A,A))),multiply(identity,multiply(identity,multiply(multiply(A,identity),identity)))) = identity,
    inference(paramod,[status(thm)],[c_62,c_421]) ).

cnf(c_64,plain,
    multiply(identity,multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),identity)))) = identity,
    inference(paramod,[status(thm)],[c_57,c_422]) ).

cnf(c_423,plain,
    multiply(multiply(identity,A),B) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),multiply(identity,multiply(multiply(B,identity),identity))))),
    inference(paramod,[status(thm)],[c_11,c_43]) ).

cnf(c_424,plain,
    multiply(multiply(identity,A),B) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(A,identity),identity)),multiply(multiply(B,identity),identity))))),
    inference(paramod,[status(thm)],[c_58,c_423]) ).

cnf(c_65,plain,
    multiply(multiply(identity,A),B) = multiply(identity,multiply(A,multiply(identity,multiply(identity,multiply(multiply(B,identity),identity))))),
    inference(paramod,[status(thm)],[c_42,c_424]) ).

cnf(c_425,plain,
    multiply(multiply(identity,A),multiply(identity,B)) = multiply(multiply(identity,identity),multiply(A,B)),
    inference(paramod,[status(thm)],[c_1,c_48]) ).

cnf(c_66,plain,
    multiply(multiply(identity,A),multiply(identity,B)) = multiply(identity,multiply(A,B)),
    inference(paramod,[status(thm)],[c_2,c_425]) ).

cnf(c_67,plain,
    multiply(multiply(A,multiply(identity,multiply(identity,multiply(B,multiply(B,B))))),multiply(identity,B)) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_42,c_48]) ).

cnf(c_426,plain,
    multiply(A,multiply(identity,B)) = multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(identity,identity),multiply(A,C))),multiply(C,multiply(C,C))),B)),
    inference(paramod,[status(thm)],[c_1,c_66]) ).

cnf(c_427,plain,
    multiply(A,multiply(identity,B)) = multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(A,C))),multiply(C,multiply(C,C))),B)),
    inference(paramod,[status(thm)],[c_2,c_426]) ).

cnf(c_69,plain,
    multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(A,B))),multiply(B,multiply(B,B))),C)) = multiply(A,multiply(identity,C)),
    inference(copy,[status(thm)],[c_427]) ).

cnf(c_428,plain,
    multiply(A,multiply(identity,B)) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),B)),
    inference(paramod,[status(thm)],[c_11,c_66]) ).

cnf(c_71,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),B)) = multiply(A,multiply(identity,B)),
    inference(copy,[status(thm)],[c_428]) ).

cnf(c_74,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),B)))) = multiply(A,multiply(identity,multiply(identity,multiply(identity,B)))),
    inference(paramod,[status(thm)],[c_66,c_42]) ).

cnf(c_75,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,A))),B) = multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(multiply(B,identity),identity))))),
    inference(paramod,[status(thm)],[c_66,c_43]) ).

cnf(c_429,plain,
    multiply(A,multiply(A,A)) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),identity))))),
    inference(paramod,[status(thm)],[c_60,c_43]) ).

cnf(c_430,plain,
    multiply(A,multiply(A,A)) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity))))),
    inference(paramod,[status(thm)],[c_66,c_429]) ).

cnf(c_76,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity))))) = multiply(A,multiply(A,A)),
    inference(copy,[status(thm)],[c_430]) ).

cnf(c_431,plain,
    multiply(multiply(identity,identity),multiply(multiply(identity,multiply(identity,identity)),identity)) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),identity))),
    inference(paramod,[status(thm)],[c_64,c_20]) ).

cnf(c_432,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,identity)),identity)) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),identity))),
    inference(paramod,[status(thm)],[c_2,c_431]) ).

cnf(c_433,plain,
    multiply(identity,multiply(multiply(identity,identity),identity)) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),identity))),
    inference(paramod,[status(thm)],[c_2,c_432]) ).

cnf(c_434,plain,
    multiply(identity,multiply(identity,identity)) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),identity))),
    inference(paramod,[status(thm)],[c_2,c_433]) ).

cnf(c_435,plain,
    multiply(identity,identity) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),identity))),
    inference(paramod,[status(thm)],[c_2,c_434]) ).

cnf(c_436,plain,
    identity = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),identity))),
    inference(paramod,[status(thm)],[c_2,c_435]) ).

cnf(c_81,plain,
    multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),identity))) = identity,
    inference(copy,[status(thm)],[c_436]) ).

cnf(c_437,plain,
    multiply(multiply(identity,multiply(identity,multiply(A,multiply(A,A)))),A) = multiply(identity,identity),
    inference(paramod,[status(thm)],[c_64,c_43]) ).

cnf(c_83,plain,
    multiply(multiply(identity,multiply(identity,multiply(A,multiply(A,A)))),A) = identity,
    inference(paramod,[status(thm)],[c_2,c_437]) ).

cnf(c_84,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),identity)),multiply(B,multiply(B,B)))) = multiply(identity,multiply(identity,multiply(B,multiply(B,B)))),
    inference(paramod,[status(thm)],[c_83,c_1]) ).

cnf(c_438,plain,
    multiply(multiply(A,multiply(A,A)),multiply(multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))),multiply(identity,identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(A,identity),identity)),identity)))),
    inference(paramod,[status(thm)],[c_81,c_32]) ).

cnf(c_439,plain,
    multiply(multiply(A,multiply(A,A)),multiply(multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(A,identity),identity)),identity)))),
    inference(paramod,[status(thm)],[c_2,c_438]) ).

cnf(c_440,plain,
    multiply(multiply(A,multiply(A,A)),multiply(multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),identity))))),
    inference(paramod,[status(thm)],[c_15,c_439]) ).

cnf(c_85,plain,
    multiply(multiply(A,multiply(A,A)),multiply(multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))),identity)) = multiply(identity,multiply(A,identity)),
    inference(paramod,[status(thm)],[c_11,c_440]) ).

cnf(c_441,plain,
    multiply(multiply(identity,A),multiply(identity,multiply(multiply(multiply(A,multiply(A,A)),identity),identity))) = identity,
    inference(paramod,[status(thm)],[c_40,c_81]) ).

cnf(c_86,plain,
    multiply(identity,multiply(A,multiply(multiply(multiply(A,multiply(A,A)),identity),identity))) = identity,
    inference(paramod,[status(thm)],[c_66,c_441]) ).

cnf(c_442,plain,
    multiply(multiply(identity,identity),multiply(multiply(identity,multiply(identity,identity)),identity)) = multiply(A,multiply(multiply(multiply(A,multiply(A,A)),identity),identity)),
    inference(paramod,[status(thm)],[c_86,c_20]) ).

cnf(c_443,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,identity)),identity)) = multiply(A,multiply(multiply(multiply(A,multiply(A,A)),identity),identity)),
    inference(paramod,[status(thm)],[c_2,c_442]) ).

cnf(c_444,plain,
    multiply(identity,multiply(multiply(identity,identity),identity)) = multiply(A,multiply(multiply(multiply(A,multiply(A,A)),identity),identity)),
    inference(paramod,[status(thm)],[c_2,c_443]) ).

cnf(c_445,plain,
    multiply(identity,multiply(identity,identity)) = multiply(A,multiply(multiply(multiply(A,multiply(A,A)),identity),identity)),
    inference(paramod,[status(thm)],[c_2,c_444]) ).

cnf(c_446,plain,
    multiply(identity,identity) = multiply(A,multiply(multiply(multiply(A,multiply(A,A)),identity),identity)),
    inference(paramod,[status(thm)],[c_2,c_445]) ).

cnf(c_447,plain,
    identity = multiply(A,multiply(multiply(multiply(A,multiply(A,A)),identity),identity)),
    inference(paramod,[status(thm)],[c_2,c_446]) ).

cnf(c_90,plain,
    multiply(A,multiply(multiply(multiply(A,multiply(A,A)),identity),identity)) = identity,
    inference(copy,[status(thm)],[c_447]) ).

cnf(c_448,plain,
    multiply(multiply(A,A),multiply(multiply(A,multiply(identity,identity)),identity)) = multiply(multiply(multiply(A,multiply(A,A)),identity),identity),
    inference(paramod,[status(thm)],[c_90,c_20]) ).

cnf(c_449,plain,
    multiply(multiply(A,A),multiply(multiply(A,identity),identity)) = multiply(multiply(multiply(A,multiply(A,A)),identity),identity),
    inference(paramod,[status(thm)],[c_2,c_448]) ).

cnf(c_92,plain,
    multiply(multiply(multiply(A,multiply(A,A)),identity),identity) = multiply(multiply(A,A),multiply(multiply(A,identity),identity)),
    inference(copy,[status(thm)],[c_449]) ).

cnf(c_450,plain,
    multiply(multiply(A,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(identity,identity),multiply(B,C))),multiply(C,multiply(C,C))),multiply(multiply(multiply(identity,multiply(multiply(identity,identity),multiply(B,C))),multiply(C,multiply(C,C))),multiply(multiply(identity,multiply(multiply(identity,identity),multiply(B,C))),multiply(C,multiply(C,C)))))))),B) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_1,c_67]) ).

cnf(c_451,plain,
    multiply(multiply(A,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(B,C))),multiply(C,multiply(C,C))),multiply(multiply(multiply(identity,multiply(multiply(identity,identity),multiply(B,C))),multiply(C,multiply(C,C))),multiply(multiply(identity,multiply(multiply(identity,identity),multiply(B,C))),multiply(C,multiply(C,C)))))))),B) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_2,c_450]) ).

cnf(c_452,plain,
    multiply(multiply(A,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(B,C))),multiply(C,multiply(C,C))),multiply(multiply(multiply(identity,multiply(identity,multiply(B,C))),multiply(C,multiply(C,C))),multiply(multiply(identity,multiply(multiply(identity,identity),multiply(B,C))),multiply(C,multiply(C,C)))))))),B) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_2,c_451]) ).

cnf(c_453,plain,
    multiply(multiply(A,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(B,C))),multiply(C,multiply(C,C))),multiply(multiply(multiply(identity,multiply(identity,multiply(B,C))),multiply(C,multiply(C,C))),multiply(multiply(identity,multiply(identity,multiply(B,C))),multiply(C,multiply(C,C)))))))),B) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_2,c_452]) ).

cnf(c_454,plain,
    multiply(multiply(A,multiply(identity,multiply(B,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(B,C))),multiply(C,multiply(C,C))),multiply(multiply(identity,multiply(identity,multiply(B,C))),multiply(C,multiply(C,C)))))))),B) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_69,c_453]) ).

cnf(c_455,plain,
    multiply(multiply(A,multiply(identity,multiply(B,multiply(B,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(B,C))),multiply(C,multiply(C,C)))))))),B) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_69,c_454]) ).

cnf(c_96,plain,
    multiply(multiply(A,multiply(identity,multiply(B,multiply(B,B)))),B) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_4,c_455]) ).

cnf(c_456,plain,
    multiply(multiply(A,multiply(B,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(B,identity),identity)),multiply(identity,multiply(multiply(B,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(B,identity),identity)))) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_42,c_67]) ).

cnf(c_457,plain,
    multiply(multiply(A,multiply(B,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(B,identity),identity),multiply(multiply(B,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(B,identity),identity)))) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_66,c_456]) ).

cnf(c_458,plain,
    multiply(multiply(A,multiply(B,multiply(B,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(B,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(B,identity),identity)))) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_74,c_457]) ).

cnf(c_97,plain,
    multiply(multiply(A,multiply(B,multiply(B,B))),multiply(identity,multiply(identity,multiply(multiply(B,identity),identity)))) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_11,c_458]) ).

cnf(c_459,plain,
    multiply(multiply(multiply(A,identity),identity),B) = multiply(multiply(multiply(A,multiply(identity,multiply(identity,multiply(multiply(B,multiply(B,B)),multiply(multiply(B,multiply(B,B)),multiply(B,multiply(B,B))))))),identity),identity),
    inference(paramod,[status(thm)],[c_67,c_96]) ).

cnf(c_460,plain,
    multiply(multiply(multiply(A,identity),identity),B) = multiply(multiply(multiply(A,multiply(identity,multiply(identity,multiply(identity,B)))),identity),identity),
    inference(paramod,[status(thm)],[c_40,c_459]) ).

cnf(c_99,plain,
    multiply(multiply(multiply(A,multiply(identity,multiply(identity,multiply(identity,B)))),identity),identity) = multiply(multiply(multiply(A,identity),identity),B),
    inference(copy,[status(thm)],[c_460]) ).

cnf(c_461,plain,
    multiply(multiply(multiply(A,B),identity),identity) = multiply(multiply(multiply(A,identity),identity),multiply(multiply(B,identity),identity)),
    inference(paramod,[status(thm)],[c_11,c_99]) ).

cnf(c_106,plain,
    multiply(multiply(multiply(A,identity),identity),multiply(multiply(B,identity),identity)) = multiply(multiply(multiply(A,B),identity),identity),
    inference(copy,[status(thm)],[c_461]) ).

cnf(c_462,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_75,c_35]) ).

cnf(c_463,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(multiply(identity,multiply(multiply(identity,multiply(identity,A)),identity)),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_462]) ).

cnf(c_464,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),identity))),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_463]) ).

cnf(c_465,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,identity)))),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_464]) ).

cnf(c_466,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,identity))),identity)))))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_465]) ).

cnf(c_467,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,identity)),identity))))))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_466]) ).

cnf(c_468,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),identity)))))))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_467]) ).

cnf(c_469,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),multiply(identity,multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_11,c_468]) ).

cnf(c_470,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,A)),multiply(identity,multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_66,c_469]) ).

cnf(c_471,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),multiply(identity,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_66,c_470]) ).

cnf(c_472,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,A))),identity),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_66,c_471]) ).

cnf(c_473,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,A)),identity)),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_472]) ).

cnf(c_474,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(multiply(identity,A),identity))),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_473]) ).

cnf(c_475,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,identity)))),identity))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_474]) ).

cnf(c_476,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,identity))),identity)))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_475]) ).

cnf(c_477,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,identity)),identity))))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_476]) ).

cnf(c_478,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),identity)))))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_15,c_477]) ).

cnf(c_479,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),A)) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_11,c_478]) ).

cnf(c_108,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),multiply(A,multiply(A,A))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_60,c_479]) ).

cnf(c_480,plain,
    multiply(multiply(identity,multiply(multiply(A,B),identity)),identity) = multiply(identity,multiply(multiply(multiply(A,identity),identity),multiply(multiply(B,identity),identity))),
    inference(paramod,[status(thm)],[c_106,c_15]) ).

cnf(c_481,plain,
    multiply(identity,multiply(multiply(multiply(A,B),identity),identity)) = multiply(identity,multiply(multiply(multiply(A,identity),identity),multiply(multiply(B,identity),identity))),
    inference(paramod,[status(thm)],[c_15,c_480]) ).

cnf(c_109,plain,
    multiply(identity,multiply(multiply(multiply(A,identity),identity),multiply(multiply(B,identity),identity))) = multiply(identity,multiply(multiply(multiply(A,B),identity),identity)),
    inference(copy,[status(thm)],[c_481]) ).

cnf(c_482,plain,
    multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(B,identity),identity),identity)) = multiply(multiply(multiply(A,multiply(B,multiply(identity,multiply(identity,multiply(identity,identity))))),identity),identity),
    inference(paramod,[status(thm)],[c_96,c_106]) ).

cnf(c_483,plain,
    multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(B,identity),identity),identity)) = multiply(multiply(multiply(A,multiply(B,multiply(identity,multiply(identity,identity)))),identity),identity),
    inference(paramod,[status(thm)],[c_2,c_482]) ).

cnf(c_484,plain,
    multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(B,identity),identity),identity)) = multiply(multiply(multiply(A,multiply(B,multiply(identity,identity))),identity),identity),
    inference(paramod,[status(thm)],[c_2,c_483]) ).

cnf(c_485,plain,
    multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(B,identity),identity),identity)) = multiply(multiply(multiply(A,multiply(B,identity)),identity),identity),
    inference(paramod,[status(thm)],[c_2,c_484]) ).

cnf(c_115,plain,
    multiply(multiply(multiply(A,multiply(B,identity)),identity),identity) = multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(B,identity),identity),identity)),
    inference(copy,[status(thm)],[c_485]) ).

cnf(c_486,plain,
    multiply(identity,multiply(multiply(multiply(multiply(identity,multiply(identity,multiply(A,B))),identity),identity),multiply(multiply(multiply(B,multiply(B,B)),identity),identity))) = multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),identity),identity)),
    inference(paramod,[status(thm)],[c_14,c_109]) ).

cnf(c_487,plain,
    multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(identity,multiply(A,B)),identity)),identity),multiply(multiply(multiply(B,multiply(B,B)),identity),identity))) = multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),identity),identity)),
    inference(paramod,[status(thm)],[c_15,c_486]) ).

cnf(c_488,plain,
    multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(A,B),identity))),identity),multiply(multiply(multiply(B,multiply(B,B)),identity),identity))) = multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),identity),identity)),
    inference(paramod,[status(thm)],[c_15,c_487]) ).

cnf(c_489,plain,
    multiply(identity,multiply(multiply(identity,multiply(multiply(identity,multiply(multiply(A,B),identity)),identity)),multiply(multiply(multiply(B,multiply(B,B)),identity),identity))) = multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),identity),identity)),
    inference(paramod,[status(thm)],[c_15,c_488]) ).

cnf(c_490,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(A,B),identity),identity))),multiply(multiply(multiply(B,multiply(B,B)),identity),identity))) = multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),identity),identity)),
    inference(paramod,[status(thm)],[c_15,c_489]) ).

cnf(c_491,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(A,B),identity),identity))),multiply(multiply(B,B),multiply(multiply(B,identity),identity)))) = multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),identity),identity)),
    inference(paramod,[status(thm)],[c_92,c_490]) ).

cnf(c_492,plain,
    multiply(multiply(A,B),multiply(identity,multiply(multiply(B,B),multiply(multiply(B,identity),identity)))) = multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(A,identity),identity))),identity),identity)),
    inference(paramod,[status(thm)],[c_71,c_491]) ).

cnf(c_493,plain,
    multiply(multiply(A,B),multiply(identity,multiply(multiply(B,B),multiply(multiply(B,identity),identity)))) = multiply(identity,multiply(multiply(identity,multiply(multiply(identity,multiply(multiply(A,identity),identity)),identity)),identity)),
    inference(paramod,[status(thm)],[c_15,c_492]) ).

cnf(c_494,plain,
    multiply(multiply(A,B),multiply(identity,multiply(multiply(B,B),multiply(multiply(B,identity),identity)))) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),identity))),identity)),
    inference(paramod,[status(thm)],[c_15,c_493]) ).

cnf(c_495,plain,
    multiply(multiply(A,B),multiply(identity,multiply(multiply(B,B),multiply(multiply(B,identity),identity)))) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),identity))),
    inference(paramod,[status(thm)],[c_15,c_494]) ).

cnf(c_496,plain,
    multiply(multiply(A,B),multiply(identity,multiply(multiply(B,B),multiply(multiply(B,identity),identity)))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(A,identity),identity),identity),identity)))),
    inference(paramod,[status(thm)],[c_15,c_495]) ).

cnf(c_497,plain,
    multiply(multiply(A,B),multiply(identity,multiply(multiply(B,B),multiply(multiply(B,identity),identity)))) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_11,c_496]) ).

cnf(c_116,plain,
    multiply(multiply(A,identity),identity) = multiply(multiply(A,B),multiply(identity,multiply(multiply(B,B),multiply(multiply(B,identity),identity)))),
    inference(copy,[status(thm)],[c_497]) ).

cnf(c_498,plain,
    multiply(multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))),identity),identity) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity)))),
    inference(paramod,[status(thm)],[c_60,c_116]) ).

cnf(c_499,plain,
    multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,A))),identity)),identity) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity)))),
    inference(paramod,[status(thm)],[c_15,c_498]) ).

cnf(c_500,plain,
    multiply(multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,A)),identity))),identity) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity)))),
    inference(paramod,[status(thm)],[c_15,c_499]) ).

cnf(c_501,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,A),identity)))),identity) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity)))),
    inference(paramod,[status(thm)],[c_15,c_500]) ).

cnf(c_502,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(A,A),identity))),identity)) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity)))),
    inference(paramod,[status(thm)],[c_15,c_501]) ).

cnf(c_503,plain,
    multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(A,A),identity)),identity))) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity)))),
    inference(paramod,[status(thm)],[c_15,c_502]) ).

cnf(c_504,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,A),identity),identity)))) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity)))),
    inference(paramod,[status(thm)],[c_15,c_503]) ).

cnf(c_505,plain,
    multiply(A,A) = multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity)))),
    inference(paramod,[status(thm)],[c_11,c_504]) ).

cnf(c_119,plain,
    multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,A),multiply(multiply(A,identity),identity)))) = multiply(A,A),
    inference(copy,[status(thm)],[c_505]) ).

cnf(c_506,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),identity)),multiply(identity,B))) = multiply(identity,multiply(identity,multiply(multiply(B,multiply(B,B)),multiply(multiply(B,multiply(B,B)),multiply(B,multiply(B,B)))))),
    inference(paramod,[status(thm)],[c_40,c_84]) ).

cnf(c_121,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),identity)),multiply(identity,B))) = multiply(identity,multiply(identity,multiply(identity,B))),
    inference(paramod,[status(thm)],[c_40,c_506]) ).

cnf(c_507,plain,
    multiply(multiply(identity,A),multiply(multiply(multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A)))),multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))),identity)) = multiply(identity,multiply(multiply(A,multiply(A,A)),identity)),
    inference(paramod,[status(thm)],[c_40,c_85]) ).

cnf(c_508,plain,
    multiply(multiply(identity,A),multiply(multiply(multiply(identity,A),multiply(multiply(A,multiply(A,A)),multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))))),identity)) = multiply(identity,multiply(multiply(A,multiply(A,A)),identity)),
    inference(paramod,[status(thm)],[c_40,c_507]) ).

cnf(c_509,plain,
    multiply(multiply(identity,A),multiply(multiply(multiply(identity,A),multiply(identity,A)),identity)) = multiply(identity,multiply(multiply(A,multiply(A,A)),identity)),
    inference(paramod,[status(thm)],[c_40,c_508]) ).

cnf(c_510,plain,
    multiply(multiply(identity,A),multiply(multiply(identity,multiply(A,A)),identity)) = multiply(identity,multiply(multiply(A,multiply(A,A)),identity)),
    inference(paramod,[status(thm)],[c_66,c_509]) ).

cnf(c_511,plain,
    multiply(multiply(identity,A),multiply(identity,multiply(multiply(A,A),identity))) = multiply(identity,multiply(multiply(A,multiply(A,A)),identity)),
    inference(paramod,[status(thm)],[c_15,c_510]) ).

cnf(c_512,plain,
    multiply(identity,multiply(A,multiply(multiply(A,A),identity))) = multiply(identity,multiply(multiply(A,multiply(A,A)),identity)),
    inference(paramod,[status(thm)],[c_66,c_511]) ).

cnf(c_123,plain,
    multiply(identity,multiply(multiply(A,multiply(A,A)),identity)) = multiply(identity,multiply(A,multiply(multiply(A,A),identity))),
    inference(copy,[status(thm)],[c_512]) ).

cnf(c_513,plain,
    multiply(multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,multiply(multiply(A,A),identity))),B))),multiply(B,multiply(B,B))) = multiply(multiply(A,multiply(A,A)),identity),
    inference(paramod,[status(thm)],[c_123,c_26]) ).

cnf(c_514,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(multiply(A,multiply(A,A)),identity),
    inference(paramod,[status(thm)],[c_26,c_513]) ).

cnf(c_124,plain,
    multiply(multiply(A,multiply(A,A)),identity) = multiply(A,multiply(multiply(A,A),identity)),
    inference(copy,[status(thm)],[c_514]) ).

cnf(c_125,plain,
    multiply(multiply(A,A),multiply(multiply(A,multiply(A,multiply(multiply(A,A),identity))),identity)) = multiply(A,A),
    inference(paramod,[status(thm)],[c_124,c_20]) ).

cnf(c_126,plain,
    multiply(A,multiply(multiply(A,A),multiply(A,multiply(multiply(A,A),identity)))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,A),identity)))),
    inference(paramod,[status(thm)],[c_124,c_32]) ).

cnf(c_515,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),identity)),B)) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(identity,identity),multiply(B,C))),multiply(C,multiply(C,C)))))),
    inference(paramod,[status(thm)],[c_1,c_121]) ).

cnf(c_516,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),identity)),B)) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(B,C))),multiply(C,multiply(C,C)))))),
    inference(paramod,[status(thm)],[c_2,c_515]) ).

cnf(c_127,plain,
    multiply(A,multiply(multiply(A,multiply(multiply(A,A),identity)),B)) = multiply(identity,multiply(identity,B)),
    inference(paramod,[status(thm)],[c_4,c_516]) ).

cnf(c_517,plain,
    multiply(A,multiply(multiply(A,identity),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(A,A),identity),multiply(multiply(A,A),identity)),multiply(multiply(multiply(multiply(A,A),identity),identity),identity))))),
    inference(paramod,[status(thm)],[c_116,c_121]) ).

cnf(c_518,plain,
    multiply(A,multiply(multiply(A,identity),identity)) = multiply(multiply(multiply(A,A),identity),multiply(multiply(multiply(A,A),identity),multiply(multiply(A,A),identity))),
    inference(paramod,[status(thm)],[c_76,c_517]) ).

cnf(c_129,plain,
    multiply(multiply(multiply(A,A),identity),multiply(multiply(multiply(A,A),identity),multiply(multiply(A,A),identity))) = multiply(A,multiply(multiply(A,identity),identity)),
    inference(copy,[status(thm)],[c_518]) ).

cnf(c_519,plain,
    multiply(multiply(A,multiply(A,A)),multiply(multiply(identity,multiply(A,identity)),multiply(identity,B))) = multiply(identity,multiply(identity,multiply(identity,B))),
    inference(paramod,[status(thm)],[c_85,c_121]) ).

cnf(c_130,plain,
    multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),B))) = multiply(identity,multiply(identity,multiply(identity,B))),
    inference(paramod,[status(thm)],[c_66,c_519]) ).

cnf(c_133,plain,
    multiply(multiply(A,multiply(A,A)),multiply(multiply(identity,multiply(A,identity)),B)) = multiply(identity,multiply(identity,B)),
    inference(paramod,[status(thm)],[c_85,c_127]) ).

cnf(c_520,plain,
    multiply(multiply(A,multiply(A,A)),identity) = multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity),multiply(multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity),multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity))))),
    inference(paramod,[status(thm)],[c_25,c_133]) ).

cnf(c_521,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity),multiply(multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity),multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity))))),
    inference(paramod,[status(thm)],[c_124,c_520]) ).

cnf(c_522,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(A,identity),identity)),identity),multiply(multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity),multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity))))),
    inference(paramod,[status(thm)],[c_15,c_521]) ).

cnf(c_523,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),multiply(multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity),multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity))))),
    inference(paramod,[status(thm)],[c_15,c_522]) ).

cnf(c_524,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),multiply(multiply(multiply(identity,multiply(multiply(A,identity),identity)),identity),multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity))))),
    inference(paramod,[status(thm)],[c_15,c_523]) ).

cnf(c_525,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity))))),
    inference(paramod,[status(thm)],[c_15,c_524]) ).

cnf(c_526,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),multiply(multiply(identity,multiply(multiply(A,identity),identity)),identity))))),
    inference(paramod,[status(thm)],[c_15,c_525]) ).

cnf(c_527,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)))))),
    inference(paramod,[status(thm)],[c_15,c_526]) ).

cnf(c_528,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)),multiply(identity,multiply(multiply(multiply(multiply(A,identity),identity),identity),multiply(multiply(multiply(A,identity),identity),identity)))))),
    inference(paramod,[status(thm)],[c_66,c_527]) ).

cnf(c_529,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(A,identity),identity),identity),multiply(multiply(multiply(multiply(A,identity),identity),identity),multiply(multiply(multiply(A,identity),identity),identity)))))),
    inference(paramod,[status(thm)],[c_66,c_528]) ).

cnf(c_530,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(multiply(A,identity),multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(A,identity),identity),identity),multiply(multiply(multiply(A,identity),identity),identity)))))),
    inference(paramod,[status(thm)],[c_74,c_529]) ).

cnf(c_531,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)))))),
    inference(paramod,[status(thm)],[c_74,c_530]) ).

cnf(c_532,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))),
    inference(paramod,[status(thm)],[c_11,c_531]) ).

cnf(c_135,plain,
    multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))) = multiply(A,multiply(multiply(A,A),identity)),
    inference(copy,[status(thm)],[c_532]) ).

cnf(c_533,plain,
    multiply(multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,identity)),multiply(identity,multiply(A,identity))))),multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity)))) = multiply(multiply(multiply(A,multiply(A,A)),identity),identity),
    inference(paramod,[status(thm)],[c_133,c_97]) ).

cnf(c_534,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),multiply(A,identity))))),multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(A,identity)),identity),identity)))) = multiply(multiply(multiply(A,multiply(A,A)),identity),identity),
    inference(paramod,[status(thm)],[c_66,c_533]) ).

cnf(c_535,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),multiply(A,identity))))),multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(A,identity),identity)),identity)))) = multiply(multiply(multiply(A,multiply(A,A)),identity),identity),
    inference(paramod,[status(thm)],[c_15,c_534]) ).

cnf(c_536,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),multiply(A,identity))))),multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),identity))))) = multiply(multiply(multiply(A,multiply(A,A)),identity),identity),
    inference(paramod,[status(thm)],[c_15,c_535]) ).

cnf(c_537,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),multiply(A,identity))))),multiply(A,identity)) = multiply(multiply(multiply(A,multiply(A,A)),identity),identity),
    inference(paramod,[status(thm)],[c_11,c_536]) ).

cnf(c_538,plain,
    multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))) = multiply(multiply(multiply(A,multiply(A,A)),identity),identity),
    inference(paramod,[status(thm)],[c_60,c_537]) ).

cnf(c_539,plain,
    multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))) = multiply(multiply(A,multiply(multiply(A,A),identity)),identity),
    inference(paramod,[status(thm)],[c_124,c_538]) ).

cnf(c_138,plain,
    multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))) = multiply(multiply(A,A),multiply(multiply(A,identity),identity)),
    inference(paramod,[status(thm)],[c_31,c_539]) ).

cnf(c_141,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,multiply(B,identity)))),multiply(B,multiply(multiply(B,B),identity)))) = A,
    inference(paramod,[status(thm)],[c_135,c_4]) ).

cnf(c_540,plain,
    multiply(multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))),identity) = multiply(multiply(A,A),multiply(multiply(A,identity),identity)),
    inference(paramod,[status(thm)],[c_135,c_31]) ).

cnf(c_146,plain,
    multiply(multiply(A,identity),multiply(multiply(multiply(A,identity),multiply(A,identity)),identity)) = multiply(multiply(A,A),multiply(multiply(A,identity),identity)),
    inference(paramod,[status(thm)],[c_124,c_540]) ).

cnf(c_541,plain,
    multiply(multiply(A,A),multiply(multiply(multiply(A,A),identity),multiply(multiply(multiply(A,A),identity),multiply(multiply(A,A),identity)))) = multiply(A,multiply(multiply(A,multiply(multiply(A,A),identity)),identity)),
    inference(paramod,[status(thm)],[c_138,c_9]) ).

cnf(c_542,plain,
    multiply(multiply(A,A),multiply(A,multiply(multiply(A,identity),identity))) = multiply(A,multiply(multiply(A,multiply(multiply(A,A),identity)),identity)),
    inference(paramod,[status(thm)],[c_129,c_541]) ).

cnf(c_543,plain,
    multiply(multiply(A,A),multiply(A,multiply(multiply(A,identity),identity))) = multiply(A,multiply(multiply(A,A),multiply(multiply(A,identity),identity))),
    inference(paramod,[status(thm)],[c_31,c_542]) ).

cnf(c_544,plain,
    multiply(multiply(A,A),multiply(A,multiply(multiply(A,identity),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))),
    inference(paramod,[status(thm)],[c_32,c_543]) ).

cnf(c_545,plain,
    multiply(multiply(A,A),multiply(A,multiply(multiply(A,identity),identity))) = multiply(identity,multiply(identity,multiply(identity,identity))),
    inference(paramod,[status(thm)],[c_2,c_544]) ).

cnf(c_546,plain,
    multiply(multiply(A,A),multiply(A,multiply(multiply(A,identity),identity))) = multiply(identity,multiply(identity,identity)),
    inference(paramod,[status(thm)],[c_2,c_545]) ).

cnf(c_547,plain,
    multiply(multiply(A,A),multiply(A,multiply(multiply(A,identity),identity))) = multiply(identity,identity),
    inference(paramod,[status(thm)],[c_2,c_546]) ).

cnf(c_155,plain,
    multiply(multiply(A,A),multiply(A,multiply(multiply(A,identity),identity))) = identity,
    inference(paramod,[status(thm)],[c_2,c_547]) ).

cnf(c_548,plain,
    multiply(multiply(multiply(A,A),multiply(A,A)),multiply(multiply(multiply(A,A),multiply(multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))),identity)),identity)) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_138,c_20]) ).

cnf(c_549,plain,
    multiply(multiply(multiply(A,A),multiply(A,A)),multiply(multiply(multiply(A,A),multiply(multiply(A,identity),multiply(multiply(multiply(A,identity),multiply(A,identity)),identity))),identity)) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_124,c_548]) ).

cnf(c_550,plain,
    multiply(multiply(multiply(A,A),multiply(A,A)),multiply(multiply(multiply(A,A),multiply(multiply(A,A),multiply(multiply(A,identity),identity))),identity)) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_146,c_549]) ).

cnf(c_156,plain,
    multiply(multiply(multiply(A,A),multiply(A,A)),multiply(A,identity)) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_35,c_550]) ).

cnf(c_551,plain,
    multiply(multiply(A,A),multiply(multiply(multiply(A,A),multiply(A,A)),multiply(multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)))),
    inference(paramod,[status(thm)],[c_138,c_32]) ).

cnf(c_552,plain,
    multiply(multiply(A,A),multiply(multiply(multiply(A,A),multiply(A,A)),multiply(multiply(A,identity),multiply(multiply(multiply(A,identity),multiply(A,identity)),identity)))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)))),
    inference(paramod,[status(thm)],[c_124,c_551]) ).

cnf(c_553,plain,
    multiply(multiply(A,A),multiply(multiply(multiply(A,A),multiply(A,A)),multiply(multiply(A,A),multiply(multiply(A,identity),identity)))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),identity)))),
    inference(paramod,[status(thm)],[c_146,c_552]) ).

cnf(c_161,plain,
    multiply(multiply(A,A),multiply(multiply(multiply(A,A),multiply(A,A)),multiply(multiply(A,A),multiply(multiply(A,identity),identity)))) = multiply(A,identity),
    inference(paramod,[status(thm)],[c_11,c_553]) ).

cnf(c_554,plain,
    multiply(A,multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity)))) = multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))),
    inference(paramod,[status(thm)],[c_138,c_32]) ).

cnf(c_555,plain,
    multiply(A,multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity)))) = multiply(identity,multiply(identity,multiply(identity,identity))),
    inference(paramod,[status(thm)],[c_2,c_554]) ).

cnf(c_556,plain,
    multiply(A,multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity)))) = multiply(identity,multiply(identity,identity)),
    inference(paramod,[status(thm)],[c_2,c_555]) ).

cnf(c_557,plain,
    multiply(A,multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity)))) = multiply(identity,identity),
    inference(paramod,[status(thm)],[c_2,c_556]) ).

cnf(c_162,plain,
    multiply(A,multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity)))) = identity,
    inference(paramod,[status(thm)],[c_2,c_557]) ).

cnf(c_558,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),multiply(A,identity)),multiply(multiply(multiply(A,identity),identity),identity))))) = multiply(A,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),multiply(multiply(A,identity),identity)))))),
    inference(paramod,[status(thm)],[c_138,c_74]) ).

cnf(c_559,plain,
    multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))) = multiply(A,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(A,identity),identity),multiply(multiply(A,identity),identity)))))),
    inference(paramod,[status(thm)],[c_76,c_558]) ).

cnf(c_560,plain,
    multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))) = multiply(A,multiply(A,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,identity),identity)))))),
    inference(paramod,[status(thm)],[c_74,c_559]) ).

cnf(c_167,plain,
    multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_11,c_560]) ).

cnf(c_561,plain,
    multiply(multiply(multiply(multiply(A,identity),identity),identity),multiply(multiply(multiply(multiply(A,identity),multiply(A,identity)),identity),identity)) = multiply(multiply(multiply(multiply(A,A),multiply(multiply(A,identity),identity)),identity),identity),
    inference(paramod,[status(thm)],[c_138,c_106]) ).

cnf(c_562,plain,
    multiply(multiply(multiply(multiply(A,identity),identity),identity),multiply(multiply(multiply(multiply(A,identity),identity),identity),multiply(multiply(multiply(A,identity),identity),identity))) = multiply(multiply(multiply(multiply(A,A),multiply(multiply(A,identity),identity)),identity),identity),
    inference(paramod,[status(thm)],[c_115,c_561]) ).

cnf(c_563,plain,
    multiply(multiply(multiply(A,identity),identity),multiply(multiply(multiply(A,identity),identity),multiply(multiply(A,identity),identity))) = multiply(multiply(multiply(multiply(A,A),multiply(multiply(A,identity),identity)),identity),identity),
    inference(paramod,[status(thm)],[c_167,c_562]) ).

cnf(c_564,plain,
    multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))) = multiply(multiply(multiply(multiply(A,A),multiply(multiply(A,identity),identity)),identity),identity),
    inference(paramod,[status(thm)],[c_167,c_563]) ).

cnf(c_565,plain,
    multiply(A,multiply(A,A)) = multiply(multiply(multiply(multiply(A,A),multiply(multiply(A,identity),identity)),identity),identity),
    inference(paramod,[status(thm)],[c_167,c_564]) ).

cnf(c_566,plain,
    multiply(A,multiply(A,A)) = multiply(multiply(multiply(multiply(A,A),identity),identity),multiply(multiply(multiply(multiply(A,identity),identity),identity),identity)),
    inference(paramod,[status(thm)],[c_115,c_565]) ).

cnf(c_169,plain,
    multiply(multiply(multiply(multiply(A,A),identity),identity),multiply(multiply(multiply(multiply(A,identity),identity),identity),identity)) = multiply(A,multiply(A,A)),
    inference(copy,[status(thm)],[c_566]) ).

cnf(c_567,plain,
    multiply(multiply(multiply(multiply(A,A),identity),identity),multiply(multiply(multiply(multiply(A,identity),identity),identity),identity)) = multiply(multiply(multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))),identity),identity),
    inference(paramod,[status(thm)],[c_138,c_106]) ).

cnf(c_568,plain,
    multiply(A,multiply(A,A)) = multiply(multiply(multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))),identity),identity),
    inference(paramod,[status(thm)],[c_169,c_567]) ).

cnf(c_569,plain,
    multiply(A,multiply(A,A)) = multiply(multiply(multiply(A,multiply(A,A)),identity),identity),
    inference(paramod,[status(thm)],[c_167,c_568]) ).

cnf(c_570,plain,
    multiply(A,multiply(A,A)) = multiply(multiply(A,multiply(multiply(A,A),identity)),identity),
    inference(paramod,[status(thm)],[c_124,c_569]) ).

cnf(c_571,plain,
    multiply(A,multiply(A,A)) = multiply(multiply(A,A),multiply(multiply(A,identity),identity)),
    inference(paramod,[status(thm)],[c_31,c_570]) ).

cnf(c_170,plain,
    multiply(multiply(A,A),multiply(multiply(A,identity),identity)) = multiply(A,multiply(A,A)),
    inference(copy,[status(thm)],[c_571]) ).

cnf(c_572,plain,
    multiply(multiply(A,identity),identity) = multiply(multiply(A,B),multiply(identity,multiply(multiply(B,identity),multiply(multiply(B,identity),multiply(B,identity))))),
    inference(paramod,[status(thm)],[c_138,c_116]) ).

cnf(c_172,plain,
    multiply(multiply(A,identity),identity) = multiply(multiply(A,B),multiply(identity,multiply(B,multiply(B,B)))),
    inference(paramod,[status(thm)],[c_167,c_572]) ).

cnf(c_573,plain,
    multiply(multiply(multiply(A,A),multiply(multiply(A,identity),identity)),multiply(identity,multiply(multiply(multiply(A,identity),multiply(A,identity)),multiply(multiply(multiply(A,identity),identity),identity)))) = multiply(multiply(A,identity),multiply(A,identity)),
    inference(paramod,[status(thm)],[c_138,c_119]) ).

cnf(c_574,plain,
    multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(multiply(A,identity),multiply(A,identity)),multiply(multiply(multiply(A,identity),identity),identity)))) = multiply(multiply(A,identity),multiply(A,identity)),
    inference(paramod,[status(thm)],[c_170,c_573]) ).

cnf(c_575,plain,
    multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))))) = multiply(multiply(A,identity),multiply(A,identity)),
    inference(paramod,[status(thm)],[c_170,c_574]) ).

cnf(c_174,plain,
    multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(A,multiply(A,A)))) = multiply(multiply(A,identity),multiply(A,identity)),
    inference(paramod,[status(thm)],[c_167,c_575]) ).

cnf(c_576,plain,
    multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),multiply(multiply(A,identity),multiply(A,identity))))) = multiply(A,A),
    inference(paramod,[status(thm)],[c_138,c_119]) ).

cnf(c_577,plain,
    multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(A,multiply(A,A)))) = multiply(A,A),
    inference(paramod,[status(thm)],[c_167,c_576]) ).

cnf(c_175,plain,
    multiply(multiply(A,identity),multiply(A,identity)) = multiply(A,A),
    inference(paramod,[status(thm)],[c_174,c_577]) ).

cnf(c_578,plain,
    multiply(multiply(A,A),multiply(multiply(A,identity),identity)) = multiply(A,multiply(multiply(A,A),identity)),
    inference(paramod,[status(thm)],[c_138,c_135]) ).

cnf(c_579,plain,
    multiply(A,multiply(A,A)) = multiply(A,multiply(multiply(A,A),identity)),
    inference(paramod,[status(thm)],[c_170,c_578]) ).

cnf(c_178,plain,
    multiply(A,multiply(multiply(A,A),identity)) = multiply(A,multiply(A,A)),
    inference(copy,[status(thm)],[c_579]) ).

cnf(c_186,plain,
    multiply(A,multiply(multiply(A,identity),multiply(A,A))) = identity,
    inference(paramod,[status(thm)],[c_175,c_162]) ).

cnf(c_580,plain,
    multiply(multiply(A,identity),multiply(A,A)) = multiply(multiply(A,A),multiply(multiply(A,identity),identity)),
    inference(paramod,[status(thm)],[c_175,c_138]) ).

cnf(c_190,plain,
    multiply(multiply(A,identity),multiply(A,A)) = multiply(A,multiply(A,A)),
    inference(paramod,[status(thm)],[c_170,c_580]) ).

cnf(c_195,plain,
    multiply(multiply(A,A),multiply(multiply(multiply(A,A),multiply(A,A)),multiply(A,multiply(A,A)))) = multiply(A,identity),
    inference(paramod,[status(thm)],[c_170,c_161]) ).

cnf(c_202,plain,
    multiply(multiply(A,A),multiply(A,multiply(A,A))) = A,
    inference(paramod,[status(thm)],[c_170,c_35]) ).

cnf(c_209,plain,
    multiply(identity,multiply(multiply(identity,multiply(identity,multiply(A,multiply(B,identity)))),multiply(B,multiply(B,B)))) = A,
    inference(paramod,[status(thm)],[c_178,c_141]) ).

cnf(c_581,plain,
    multiply(A,multiply(multiply(A,A),multiply(A,multiply(A,A)))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,A),identity)))),
    inference(paramod,[status(thm)],[c_178,c_126]) ).

cnf(c_582,plain,
    multiply(A,A) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,A),identity)))),
    inference(paramod,[status(thm)],[c_202,c_581]) ).

cnf(c_212,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,A),identity)))) = multiply(A,A),
    inference(copy,[status(thm)],[c_582]) ).

cnf(c_213,plain,
    multiply(multiply(A,A),multiply(multiply(A,multiply(A,multiply(A,A))),identity)) = multiply(A,A),
    inference(paramod,[status(thm)],[c_178,c_125]) ).

cnf(c_217,plain,
    multiply(A,multiply(A,multiply(A,A))) = identity,
    inference(paramod,[status(thm)],[c_190,c_186]) ).

cnf(c_583,plain,
    multiply(multiply(A,A),multiply(identity,identity)) = multiply(A,A),
    inference(paramod,[status(thm)],[c_217,c_213]) ).

cnf(c_218,plain,
    multiply(multiply(A,A),identity) = multiply(A,A),
    inference(paramod,[status(thm)],[c_2,c_583]) ).

cnf(c_219,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(A,A)))) = multiply(A,A),
    inference(paramod,[status(thm)],[c_218,c_212]) ).

cnf(c_584,plain,
    multiply(multiply(A,A),multiply(A,multiply(A,A))) = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_219,c_108]) ).

cnf(c_585,plain,
    A = multiply(identity,multiply(identity,multiply(identity,A))),
    inference(paramod,[status(thm)],[c_202,c_584]) ).

cnf(c_220,plain,
    multiply(identity,multiply(identity,multiply(identity,A))) = A,
    inference(copy,[status(thm)],[c_585]) ).

cnf(c_222,plain,
    multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(multiply(A,identity),B))) = B,
    inference(paramod,[status(thm)],[c_220,c_130]) ).

cnf(c_586,plain,
    multiply(A,B) = multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(multiply(B,identity),identity))))),
    inference(paramod,[status(thm)],[c_220,c_75]) ).

cnf(c_587,plain,
    multiply(A,B) = multiply(A,multiply(multiply(B,identity),identity)),
    inference(paramod,[status(thm)],[c_220,c_586]) ).

cnf(c_224,plain,
    multiply(A,multiply(multiply(B,identity),identity)) = multiply(A,B),
    inference(copy,[status(thm)],[c_587]) ).

cnf(c_226,plain,
    multiply(A,multiply(multiply(A,A),multiply(multiply(A,B),identity))) = multiply(B,identity),
    inference(paramod,[status(thm)],[c_220,c_32]) ).

cnf(c_233,plain,
    multiply(multiply(A,A),multiply(A,A)) = identity,
    inference(paramod,[status(thm)],[c_224,c_155]) ).

cnf(c_245,plain,
    multiply(multiply(identity,A),B) = multiply(identity,multiply(A,multiply(identity,multiply(identity,B)))),
    inference(paramod,[status(thm)],[c_224,c_65]) ).

cnf(c_247,plain,
    multiply(multiply(A,A),multiply(identity,multiply(A,multiply(A,A)))) = multiply(A,identity),
    inference(paramod,[status(thm)],[c_233,c_195]) ).

cnf(c_588,plain,
    multiply(identity,multiply(A,identity)) = multiply(multiply(A,identity),identity),
    inference(paramod,[status(thm)],[c_233,c_156]) ).

cnf(c_248,plain,
    multiply(multiply(A,identity),identity) = multiply(identity,multiply(A,identity)),
    inference(copy,[status(thm)],[c_588]) ).

cnf(c_250,plain,
    multiply(multiply(A,A),multiply(identity,multiply(B,identity))) = multiply(A,multiply(multiply(A,B),identity)),
    inference(paramod,[status(thm)],[c_233,c_9]) ).

cnf(c_589,plain,
    multiply(identity,multiply(identity,multiply(multiply(identity,multiply(A,multiply(B,identity))),multiply(identity,multiply(identity,multiply(B,multiply(B,B))))))) = A,
    inference(paramod,[status(thm)],[c_245,c_209]) ).

cnf(c_590,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,multiply(B,identity)),multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(B,multiply(B,B)))))))))) = A,
    inference(paramod,[status(thm)],[c_245,c_589]) ).

cnf(c_591,plain,
    multiply(identity,multiply(identity,multiply(identity,multiply(multiply(A,multiply(B,identity)),multiply(identity,multiply(B,multiply(B,B))))))) = A,
    inference(paramod,[status(thm)],[c_220,c_590]) ).

cnf(c_251,plain,
    multiply(multiply(A,multiply(B,identity)),multiply(identity,multiply(B,multiply(B,B)))) = A,
    inference(paramod,[status(thm)],[c_220,c_591]) ).

cnf(c_592,plain,
    multiply(multiply(identity,multiply(identity,multiply(identity,multiply(A,multiply(identity,multiply(identity,B)))))),multiply(B,multiply(B,B))) = A,
    inference(paramod,[status(thm)],[c_245,c_26]) ).

cnf(c_593,plain,
    multiply(multiply(A,multiply(identity,multiply(identity,B))),multiply(B,multiply(B,B))) = A,
    inference(paramod,[status(thm)],[c_220,c_592]) ).

cnf(c_594,plain,
    multiply(multiply(A,identity),identity) = A,
    inference(paramod,[status(thm)],[c_63,c_593]) ).

cnf(c_260,plain,
    multiply(identity,multiply(A,identity)) = A,
    inference(paramod,[status(thm)],[c_248,c_594]) ).

cnf(c_595,plain,
    multiply(identity,multiply(A,identity)) = multiply(multiply(A,B),multiply(identity,multiply(B,multiply(B,B)))),
    inference(paramod,[status(thm)],[c_248,c_172]) ).

cnf(c_596,plain,
    A = multiply(multiply(A,B),multiply(identity,multiply(B,multiply(B,B)))),
    inference(paramod,[status(thm)],[c_260,c_595]) ).

cnf(c_264,plain,
    multiply(multiply(A,B),multiply(identity,multiply(B,multiply(B,B)))) = A,
    inference(copy,[status(thm)],[c_596]) ).

cnf(c_269,plain,
    multiply(multiply(A,A),B) = multiply(A,multiply(multiply(A,B),identity)),
    inference(paramod,[status(thm)],[c_260,c_250]) ).

cnf(c_597,plain,
    A = multiply(A,identity),
    inference(paramod,[status(thm)],[c_264,c_247]) ).

cnf(c_271,plain,
    multiply(A,identity) = A,
    inference(copy,[status(thm)],[c_597]) ).

cnf(c_272,plain,
    multiply(multiply(A,A),B) = multiply(A,multiply(A,B)),
    inference(paramod,[status(thm)],[c_271,c_269]) ).

cnf(c_273,plain,
    multiply(identity,A) = A,
    inference(paramod,[status(thm)],[c_271,c_260]) ).

cnf(c_598,plain,
    multiply(multiply(A,B),multiply(identity,multiply(B,multiply(B,B)))) = A,
    inference(paramod,[status(thm)],[c_271,c_251]) ).

cnf(c_274,plain,
    multiply(multiply(A,B),multiply(B,multiply(B,B))) = A,
    inference(paramod,[status(thm)],[c_273,c_598]) ).

cnf(c_599,plain,
    multiply(A,multiply(multiply(A,A),multiply(A,B))) = multiply(B,identity),
    inference(paramod,[status(thm)],[c_271,c_226]) ).

cnf(c_600,plain,
    multiply(A,multiply(A,multiply(A,multiply(A,B)))) = multiply(B,identity),
    inference(paramod,[status(thm)],[c_272,c_599]) ).

cnf(c_275,plain,
    multiply(A,multiply(A,multiply(A,multiply(A,B)))) = B,
    inference(paramod,[status(thm)],[c_271,c_600]) ).

cnf(c_601,plain,
    multiply(multiply(A,multiply(A,A)),multiply(identity,multiply(A,B))) = B,
    inference(paramod,[status(thm)],[c_271,c_222]) ).

cnf(c_276,plain,
    multiply(multiply(A,multiply(A,A)),multiply(A,B)) = B,
    inference(paramod,[status(thm)],[c_273,c_601]) ).

cnf(c_277,plain,
    multiply(A,multiply(multiply(A,multiply(A,multiply(A,multiply(B,C)))),multiply(C,multiply(C,C)))) = B,
    inference(paramod,[status(thm)],[c_272,c_1]) ).

cnf(c_602,plain,
    multiply(multiply(multiply(A,multiply(A,A)),multiply(A,multiply(A,A))),multiply(A,B)) = multiply(multiply(A,multiply(A,A)),B),
    inference(paramod,[status(thm)],[c_276,c_272]) ).

cnf(c_603,plain,
    multiply(multiply(A,A),multiply(A,B)) = multiply(multiply(A,multiply(A,A)),B),
    inference(paramod,[status(thm)],[c_276,c_602]) ).

cnf(c_604,plain,
    multiply(A,multiply(A,multiply(A,B))) = multiply(multiply(A,multiply(A,A)),B),
    inference(paramod,[status(thm)],[c_272,c_603]) ).

cnf(c_285,plain,
    multiply(multiply(A,multiply(A,A)),B) = multiply(A,multiply(A,multiply(A,B))),
    inference(copy,[status(thm)],[c_604]) ).

cnf(c_605,plain,
    multiply(A,multiply(multiply(A,multiply(A,multiply(A,B))),multiply(multiply(C,multiply(C,C)),multiply(multiply(C,multiply(C,C)),multiply(C,multiply(C,C)))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_274,c_277]) ).

cnf(c_606,plain,
    multiply(A,multiply(multiply(A,multiply(A,multiply(A,B))),multiply(multiply(C,multiply(C,C)),multiply(C,multiply(C,multiply(C,multiply(C,multiply(C,C)))))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_285,c_605]) ).

cnf(c_607,plain,
    multiply(A,multiply(multiply(A,multiply(A,multiply(A,B))),multiply(multiply(C,multiply(C,C)),multiply(C,multiply(C,identity))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_217,c_606]) ).

cnf(c_608,plain,
    multiply(A,multiply(multiply(A,multiply(A,multiply(A,B))),multiply(multiply(C,multiply(C,C)),multiply(C,C)))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_271,c_607]) ).

cnf(c_609,plain,
    multiply(A,multiply(multiply(A,multiply(A,multiply(A,B))),multiply(C,multiply(C,multiply(C,multiply(C,C)))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_285,c_608]) ).

cnf(c_610,plain,
    multiply(A,multiply(multiply(A,multiply(A,multiply(A,B))),multiply(C,identity))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_217,c_609]) ).

cnf(c_298,plain,
    multiply(A,multiply(multiply(A,multiply(A,multiply(A,B))),C)) = multiply(B,C),
    inference(paramod,[status(thm)],[c_271,c_610]) ).

cnf(c_611,plain,
    multiply(A,multiply(multiply(A,multiply(A,B)),multiply(multiply(C,multiply(C,C)),multiply(multiply(C,multiply(C,C)),multiply(C,multiply(C,C)))))) = multiply(A,multiply(A,multiply(A,multiply(B,C)))),
    inference(paramod,[status(thm)],[c_277,c_277]) ).

cnf(c_612,plain,
    multiply(A,multiply(multiply(A,multiply(A,B)),multiply(multiply(C,multiply(C,C)),multiply(C,multiply(C,multiply(C,multiply(C,multiply(C,C)))))))) = multiply(A,multiply(A,multiply(A,multiply(B,C)))),
    inference(paramod,[status(thm)],[c_285,c_611]) ).

cnf(c_613,plain,
    multiply(A,multiply(multiply(A,multiply(A,B)),multiply(multiply(C,multiply(C,C)),multiply(C,multiply(C,identity))))) = multiply(A,multiply(A,multiply(A,multiply(B,C)))),
    inference(paramod,[status(thm)],[c_217,c_612]) ).

cnf(c_614,plain,
    multiply(A,multiply(multiply(A,multiply(A,B)),multiply(multiply(C,multiply(C,C)),multiply(C,C)))) = multiply(A,multiply(A,multiply(A,multiply(B,C)))),
    inference(paramod,[status(thm)],[c_271,c_613]) ).

cnf(c_615,plain,
    multiply(A,multiply(multiply(A,multiply(A,B)),multiply(C,multiply(C,multiply(C,multiply(C,C)))))) = multiply(A,multiply(A,multiply(A,multiply(B,C)))),
    inference(paramod,[status(thm)],[c_285,c_614]) ).

cnf(c_616,plain,
    multiply(A,multiply(multiply(A,multiply(A,B)),multiply(C,identity))) = multiply(A,multiply(A,multiply(A,multiply(B,C)))),
    inference(paramod,[status(thm)],[c_217,c_615]) ).

cnf(c_302,plain,
    multiply(A,multiply(multiply(A,multiply(A,B)),C)) = multiply(A,multiply(A,multiply(A,multiply(B,C)))),
    inference(paramod,[status(thm)],[c_271,c_616]) ).

cnf(c_305,plain,
    multiply(A,multiply(A,multiply(A,multiply(multiply(A,B),C)))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_302,c_298]) ).

cnf(c_617,plain,
    multiply(A,multiply(B,C)) = multiply(multiply(A,B),C),
    inference(paramod,[status(thm)],[c_305,c_275]) ).

cnf(c_346,plain,
    multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
    inference(copy,[status(thm)],[c_617]) ).

cnf(c_347,plain,
    $false,
    inference(resolve,[status(thm)],[c_346,c_3]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP122-1 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04  % Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35  % Computer : n006.cluster.edu
% 0.08/0.35  % Model    : x86_64 x86_64
% 0.08/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35  % Memory   : 8046.5625MB
% 0.08/0.35  % OS       : Linux 6.8.0-71-generic
% 0.08/0.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Fri Sep 25 14:23:55 UTC 2026
% 0.08/0.36  % CPUTime  : 
% 0.08/0.36  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36  % Process 3098834 was started by sandbox on n006,
% 0.08/0.36  % Fri Sep 25 14:23:55 2026
% 0.08/0.36  % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.36  
% 0.08/0.36  % From the command line: assign(max_seconds, 300).
% 0.73/0.58  
% 0.73/0.58  % SZS status Unsatisfiable for theBenchmark
% 0.73/0.58  
% 0.73/0.58  % Proof 1 at 0.15 (+ 0.05) seconds.
% 0.73/0.58  % Length of proof is 123.
% 0.73/0.58  % Level of proof is 44.
% 0.73/0.58  % Maximum clause weight is 100.000.
% 0.73/0.58  % Given clauses 115.
% 0.73/0.58  
% 0.73/0.58  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------