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

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Prover9---2026-6A
% Problem  : GRP423-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n014.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:29:15 AM UTC 2026

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

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

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

fof(prove_these_axioms_3,axiom,
    multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
    file('theBenchmark.p',prove_these_axioms_3) ).

cnf(c_2,plain,
    multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
    inference(clausify,[status(thm)],[prove_these_axioms_3]) ).

cnf(c_8624,plain,
    inverse(multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C))) = multiply(inverse(multiply(D,inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E))))))),multiply(D,E)),
    inference(paramod,[status(thm)],[c_1,c_1]) ).

cnf(c_3,plain,
    multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C)) = inverse(multiply(inverse(multiply(D,inverse(multiply(B,multiply(inverse(E),inverse(multiply(inverse(E),E))))))),multiply(D,E))),
    inference(copy,[status(thm)],[c_8624]) ).

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

cnf(c_4,plain,
    multiply(inverse(A),inverse(multiply(inverse(B),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(C,B)),multiply(C,A))),
    inference(copy,[status(thm)],[c_8625]) ).

cnf(c_6,plain,
    inverse(inverse(multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C)))) = B,
    inference(paramod,[status(thm)],[c_3,c_1]) ).

cnf(c_8626,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(C),multiply(inverse(D),inverse(multiply(inverse(D),D))))))),multiply(B,D)))),multiply(A,E))) = multiply(inverse(E),inverse(multiply(C,multiply(inverse(inverse(multiply(inverse(E),E))),inverse(multiply(inverse(inverse(multiply(inverse(E),E))),inverse(multiply(inverse(E),E)))))))),
    inference(paramod,[status(thm)],[c_3,c_1]) ).

cnf(c_7,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(D,inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E))))))),multiply(D,E)))),multiply(C,A))),
    inference(copy,[status(thm)],[c_8626]) ).

cnf(c_8,plain,
    multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(B)),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C)) = B,
    inference(paramod,[status(thm)],[c_3,c_1]) ).

cnf(c_11,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))),multiply(inverse(C),inverse(multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_4,c_1]) ).

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

cnf(c_14,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(D,multiply(inverse(multiply(B,inverse(multiply(inverse(D),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),A))),
    inference(paramod,[status(thm)],[c_1,c_4]) ).

cnf(c_15,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))),multiply(inverse(C),inverse(multiply(inverse(C),C)))) = inverse(multiply(inverse(multiply(D,inverse(multiply(B,multiply(inverse(E),inverse(multiply(inverse(E),E))))))),multiply(D,E))),
    inference(paramod,[status(thm)],[c_4,c_3]) ).

cnf(c_17,plain,
    inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),
    inference(paramod,[status(thm)],[c_4,c_4]) ).

cnf(c_8627,plain,
    inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,D))),multiply(inverse(E),inverse(multiply(inverse(E),E))))))),multiply(A,E))) = multiply(inverse(multiply(F,C)),multiply(F,D)),
    inference(paramod,[status(thm)],[c_17,c_1]) ).

cnf(c_20,plain,
    multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
    inference(paramod,[status(thm)],[c_1,c_8627]) ).

cnf(c_24,plain,
    inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(multiply(inverse(D),D))))))),multiply(A,D))) = multiply(inverse(D),C),
    inference(paramod,[status(thm)],[c_17,c_1]) ).

cnf(c_8628,plain,
    inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))) = inverse(multiply(inverse(multiply(E,multiply(B,C))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_1,c_17]) ).

cnf(c_25,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))) = inverse(multiply(E,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),
    inference(copy,[status(thm)],[c_8628]) ).

cnf(c_31,plain,
    inverse(multiply(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C)),multiply(inverse(multiply(D,inverse(multiply(B,multiply(inverse(E),inverse(multiply(inverse(E),E))))))),F))) = inverse(multiply(inverse(multiply(V6,multiply(D,E))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_3,c_17]) ).

cnf(c_36,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(A),A))),C))),multiply(D,A))),
    inference(paramod,[status(thm)],[c_17,c_4]) ).

cnf(c_37,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,C))),multiply(inverse(multiply(B,E)),A))),
    inference(paramod,[status(thm)],[c_17,c_4]) ).

cnf(c_44,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E))) = inverse(multiply(inverse(multiply(F,multiply(D,C))),multiply(F,E))),
    inference(paramod,[status(thm)],[c_17,c_17]) ).

cnf(c_8629,plain,
    multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D)) = multiply(inverse(multiply(E,multiply(B,C))),multiply(E,D)),
    inference(paramod,[status(thm)],[c_1,c_20]) ).

cnf(c_46,plain,
    multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D)) = multiply(E,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D)),
    inference(copy,[status(thm)],[c_8629]) ).

cnf(c_49,plain,
    multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D)),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(V6,D)),multiply(V6,multiply(A,C))),
    inference(paramod,[status(thm)],[c_3,c_20]) ).

cnf(c_55,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E)))) = inverse(multiply(inverse(multiply(F,C)),multiply(F,multiply(A,E)))),
    inference(paramod,[status(thm)],[c_20,c_17]) ).

cnf(c_56,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(F,multiply(D,C))),multiply(F,E)),
    inference(paramod,[status(thm)],[c_17,c_20]) ).

cnf(c_57,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,C)),multiply(F,multiply(A,E))),
    inference(paramod,[status(thm)],[c_20,c_20]) ).

cnf(c_58,plain,
    inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D)))),multiply(inverse(D),inverse(multiply(inverse(D),D))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_1,c_11]) ).

cnf(c_100,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),E)),
    inference(paramod,[status(thm)],[c_17,c_56]) ).

cnf(c_104,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,E))),
    inference(paramod,[status(thm)],[c_20,c_56]) ).

cnf(c_154,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
    inference(paramod,[status(thm)],[c_20,c_57]) ).

cnf(c_166,plain,
    multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D))) = multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D))),
    inference(paramod,[status(thm)],[c_57,c_56]) ).

cnf(c_213,plain,
    inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))) = inverse(inverse(multiply(inverse(multiply(D,B)),multiply(D,C)))),
    inference(paramod,[status(thm)],[c_11,c_6]) ).

cnf(c_223,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,C)))),multiply(inverse(C),inverse(multiply(inverse(C),C)))) = B,
    inference(paramod,[status(thm)],[c_4,c_8]) ).

cnf(c_313,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D)))) = inverse(multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D)))),
    inference(paramod,[status(thm)],[c_166,c_17]) ).

cnf(c_8630,plain,
    multiply(inverse(A),multiply(inverse(B),C)) = multiply(inverse(multiply(D,inverse(multiply(inverse(inverse(multiply(inverse(A),multiply(inverse(B),inverse(multiply(inverse(B),B)))))),multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))))))),multiply(D,C)),
    inference(paramod,[status(thm)],[c_13,c_20]) ).

cnf(c_489,plain,
    multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C)))))),multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))))))),multiply(A,D)) = multiply(inverse(B),multiply(inverse(C),D)),
    inference(copy,[status(thm)],[c_8630]) ).

cnf(c_8631,plain,
    multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(multiply(inverse(A),multiply(inverse(multiply(F,C)),inverse(multiply(inverse(multiply(F,C)),multiply(F,C))))))),multiply(inverse(inverse(multiply(inverse(multiply(F,C)),multiply(F,C)))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(F,C)),multiply(F,C)))),inverse(multiply(inverse(multiply(F,C)),multiply(F,C)))))))))),multiply(E,multiply(F,D))),
    inference(paramod,[status(thm)],[c_13,c_57]) ).

cnf(c_494,plain,
    multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(A),multiply(inverse(multiply(E,C)),multiply(E,D))),
    inference(paramod,[status(thm)],[c_489,c_8631]) ).

cnf(c_8632,plain,
    inverse(multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D)))) = inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(multiply(inverse(A),multiply(inverse(multiply(F,C)),inverse(multiply(inverse(multiply(F,C)),multiply(F,C))))))),multiply(inverse(inverse(multiply(inverse(multiply(F,C)),multiply(F,C)))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(F,C)),multiply(F,C)))),inverse(multiply(inverse(multiply(F,C)),multiply(F,C)))))))))),multiply(E,multiply(F,D)))),
    inference(paramod,[status(thm)],[c_13,c_55]) ).

cnf(c_497,plain,
    inverse(multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D)))) = inverse(multiply(inverse(A),multiply(inverse(multiply(E,C)),multiply(E,D)))),
    inference(paramod,[status(thm)],[c_489,c_8632]) ).

cnf(c_8633,plain,
    multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(A),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F))),multiply(inverse(multiply(V6,C)),multiply(V6,D))),
    inference(paramod,[status(thm)],[c_1,c_494]) ).

cnf(c_499,plain,
    multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(A,multiply(inverse(multiply(E,C)),multiply(E,D))),
    inference(paramod,[status(thm)],[c_1,c_8633]) ).

cnf(c_578,plain,
    multiply(inverse(multiply(A,B)),multiply(A,multiply(inverse(multiply(C,D)),multiply(C,E)))) = multiply(inverse(multiply(F,B)),multiply(F,multiply(inverse(multiply(V6,D)),multiply(V6,E)))),
    inference(paramod,[status(thm)],[c_499,c_20]) ).

cnf(c_8634,plain,
    inverse(multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D)))) = inverse(multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(A),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F))),multiply(inverse(multiply(V6,C)),multiply(V6,D)))),
    inference(paramod,[status(thm)],[c_1,c_497]) ).

cnf(c_614,plain,
    inverse(multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D)))) = inverse(multiply(A,multiply(inverse(multiply(E,C)),multiply(E,D)))),
    inference(paramod,[status(thm)],[c_1,c_8634]) ).

cnf(c_8635,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(A,multiply(inverse(inverse(multiply(inverse(multiply(B,C)),multiply(B,D)))),multiply(inverse(D),inverse(multiply(inverse(D),D)))))),multiply(A,E)))),multiply(inverse(E),inverse(multiply(inverse(E),E)))) = multiply(inverse(multiply(F,inverse(multiply(C,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)),
    inference(paramod,[status(thm)],[c_15,c_223]) ).

cnf(c_729,plain,
    multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(multiply(E,B)),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(copy,[status(thm)],[c_8635]) ).

cnf(c_8636,plain,
    inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,F))),multiply(inverse(multiply(D,E)),multiply(D,F))))))))),multiply(A,multiply(inverse(multiply(D,E)),multiply(D,F))))) = multiply(inverse(multiply(inverse(multiply(V6,E)),multiply(V6,F))),C),
    inference(paramod,[status(thm)],[c_17,c_24]) ).

cnf(c_754,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),D) = multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),D),
    inference(paramod,[status(thm)],[c_24,c_8636]) ).

cnf(c_757,plain,
    inverse(multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(inverse(A),A))))))),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
    inference(paramod,[status(thm)],[c_24,c_11]) ).

cnf(c_777,plain,
    inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(inverse(A),A))))))),E)))) = inverse(inverse(multiply(inverse(multiply(F,multiply(C,A))),multiply(F,E)))),
    inference(paramod,[status(thm)],[c_24,c_213]) ).

cnf(c_1075,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_100,c_313]) ).

cnf(c_1189,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,D))),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),V6)),multiply(inverse(multiply(V7,F)),multiply(V7,D)))),multiply(inverse(multiply(inverse(multiply(E,C)),V6)),A))),
    inference(paramod,[status(thm)],[c_154,c_4]) ).

cnf(c_1375,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,F)))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),C))),multiply(V6,V7)),
    inference(paramod,[status(thm)],[c_8,c_104]) ).

cnf(c_1381,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_104,c_223]) ).

cnf(c_1832,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F))))) = multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D),
    inference(paramod,[status(thm)],[c_25,c_11]) ).

cnf(c_1860,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,C)))) = inverse(multiply(inverse(D),D)),
    inference(paramod,[status(thm)],[c_8,c_25]) ).

cnf(c_1862,plain,
    inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))),multiply(E,F)))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_25,c_213]) ).

cnf(c_1872,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E))) = inverse(multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(D,multiply(V6,V7))),E))),
    inference(paramod,[status(thm)],[c_25,c_44]) ).

cnf(c_8637,plain,
    multiply(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(inverse(multiply(E,multiply(B,C))),multiply(E,F))) = multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,F))),
    inference(paramod,[status(thm)],[c_25,c_154]) ).

cnf(c_1926,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(V8,multiply(V6,V7))),multiply(V8,E))),
    inference(copy,[status(thm)],[c_8637]) ).

cnf(c_8638,plain,
    inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(multiply(inverse(inverse(A)),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(B,C)))) = inverse(multiply(inverse(D),D)),
    inference(paramod,[status(thm)],[c_8,c_1860]) ).

cnf(c_2083,plain,
    inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(B),B)),
    inference(paramod,[status(thm)],[c_8,c_8638]) ).

cnf(c_2092,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C))))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_1860,c_223]) ).

cnf(c_8639,plain,
    multiply(inverse(A),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,multiply(C,D))),multiply(B,multiply(C,D)))),multiply(inverse(A),inverse(multiply(inverse(A),A)))))),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = multiply(inverse(E),E),
    inference(paramod,[status(thm)],[c_1860,c_13]) ).

cnf(c_8640,plain,
    multiply(inverse(A),multiply(inverse(multiply(C,inverse(multiply(inverse(inverse(A)),multiply(inverse(D),inverse(multiply(inverse(D),D))))))),multiply(C,D))) = multiply(inverse(E),E),
    inference(paramod,[status(thm)],[c_1832,c_8639]) ).

cnf(c_2116,plain,
    multiply(inverse(A),A) = multiply(inverse(B),B),
    inference(paramod,[status(thm)],[c_8,c_8640]) ).

cnf(c_2252,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),
    inference(paramod,[status(thm)],[c_2116,c_17]) ).

cnf(c_2253,plain,
    inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,A))),
    inference(paramod,[status(thm)],[c_2116,c_17]) ).

cnf(c_2255,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
    inference(paramod,[status(thm)],[c_2116,c_20]) ).

cnf(c_2256,plain,
    multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,A)),
    inference(paramod,[status(thm)],[c_2116,c_20]) ).

cnf(c_2259,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(B),B))))) = B,
    inference(paramod,[status(thm)],[c_2116,c_11]) ).

cnf(c_2287,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_2116,c_7]) ).

cnf(c_8641,plain,
    inverse(inverse(multiply(inverse(A),A))) = inverse(inverse(multiply(inverse(multiply(B,C)),multiply(B,C)))),
    inference(paramod,[status(thm)],[c_2116,c_213]) ).

cnf(c_2295,plain,
    inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,B)))) = inverse(inverse(multiply(inverse(C),C))),
    inference(copy,[status(thm)],[c_8641]) ).

cnf(c_8642,plain,
    multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(inverse(multiply(C,D)),multiply(C,D))),
    inference(paramod,[status(thm)],[c_2116,c_499]) ).

cnf(c_2339,plain,
    multiply(A,multiply(inverse(multiply(B,C)),multiply(B,C))) = multiply(A,multiply(inverse(D),D)),
    inference(copy,[status(thm)],[c_8642]) ).

cnf(c_8643,plain,
    inverse(multiply(A,multiply(inverse(B),B))) = inverse(multiply(A,multiply(inverse(multiply(C,D)),multiply(C,D)))),
    inference(paramod,[status(thm)],[c_2116,c_614]) ).

cnf(c_2342,plain,
    inverse(multiply(A,multiply(inverse(multiply(B,C)),multiply(B,C)))) = inverse(multiply(A,multiply(inverse(D),D))),
    inference(copy,[status(thm)],[c_8643]) ).

cnf(c_2352,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(D,multiply(inverse(multiply(B,inverse(multiply(inverse(D),multiply(inverse(C),inverse(multiply(inverse(E),E))))))),A))),
    inference(paramod,[status(thm)],[c_2116,c_14]) ).

cnf(c_8644,plain,
    multiply(inverse(multiply(inverse(A),A)),B) = multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,D))),B),
    inference(paramod,[status(thm)],[c_2116,c_754]) ).

cnf(c_2381,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,B))),C) = multiply(inverse(multiply(inverse(D),D)),C),
    inference(copy,[status(thm)],[c_8644]) ).

cnf(c_2422,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))) = inverse(multiply(E,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(F),F))))))),D))),
    inference(paramod,[status(thm)],[c_2116,c_25]) ).

cnf(c_2424,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C)))))),C))),multiply(A,D))) = inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D))),
    inference(paramod,[status(thm)],[c_2116,c_25]) ).

cnf(c_2454,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
    inference(paramod,[status(thm)],[c_2083,c_2116]) ).

cnf(c_2635,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))) = multiply(inverse(D),D),
    inference(paramod,[status(thm)],[c_2083,c_2454]) ).

cnf(c_2790,plain,
    inverse(multiply(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C)),multiply(inverse(D),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F)))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_2454,c_31]) ).

cnf(c_2874,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(inverse(C),D))),multiply(inverse(multiply(E,B)),multiply(E,F)))) = inverse(multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,D))),multiply(inverse(multiply(inverse(V7),V7)),multiply(A,F)))),
    inference(paramod,[status(thm)],[c_2255,c_55]) ).

cnf(c_8645,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(inverse(C),B)),multiply(inverse(D),D)),
    inference(paramod,[status(thm)],[c_2116,c_2255]) ).

cnf(c_2980,plain,
    multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(B),A)),
    inference(copy,[status(thm)],[c_8645]) ).

cnf(c_3051,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(F,multiply(D,A))),V6))) = inverse(multiply(inverse(multiply(V7,multiply(F,E))),multiply(V7,V6))),
    inference(paramod,[status(thm)],[c_2256,c_44]) ).

cnf(c_3280,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))) = multiply(A,multiply(inverse(D),D)),
    inference(paramod,[status(thm)],[c_2116,c_2339]) ).

cnf(c_3281,plain,
    multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(inverse(C),C)),
    inference(paramod,[status(thm)],[c_2116,c_2339]) ).

cnf(c_3309,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),F))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_3281,c_44]) ).

cnf(c_3438,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),C) = multiply(inverse(multiply(inverse(D),D)),C),
    inference(paramod,[status(thm)],[c_2116,c_2381]) ).

cnf(c_3579,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(B,multiply(inverse(C),C))),multiply(B,inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(E),E)))),multiply(D,A))),
    inference(paramod,[status(thm)],[c_3281,c_36]) ).

cnf(c_3598,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(E),E))),multiply(inverse(multiply(B,D)),A))),
    inference(paramod,[status(thm)],[c_2116,c_37]) ).

cnf(c_3599,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),multiply(inverse(multiply(inverse(E),E)),A))),
    inference(paramod,[status(thm)],[c_2116,c_37]) ).

cnf(c_3617,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))),multiply(inverse(multiply(B,C)),A))),
    inference(paramod,[status(thm)],[c_2454,c_37]) ).

cnf(c_3647,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),multiply(inverse(multiply(B,multiply(inverse(F),F))),A))),
    inference(paramod,[status(thm)],[c_3281,c_37]) ).

cnf(c_3711,plain,
    inverse(inverse(multiply(inverse(A),A))) = inverse(inverse(multiply(inverse(B),B))),
    inference(paramod,[status(thm)],[c_2116,c_2295]) ).

cnf(c_3749,plain,
    multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
    inference(paramod,[status(thm)],[c_3711,c_2116]) ).

cnf(c_4347,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),D))),multiply(inverse(multiply(inverse(E),E)),multiply(inverse(B),A)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_2980,c_313]) ).

cnf(c_4404,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D)))),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_104,c_2980]) ).

cnf(c_4414,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D)))),multiply(A,E))),multiply(inverse(F),F)) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(multiply(V7,E)),multiply(V7,multiply(inverse(multiply(V8,C)),multiply(V8,D))))),
    inference(paramod,[status(thm)],[c_578,c_2980]) ).

cnf(c_4583,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_2116,c_2259]) ).

cnf(c_4613,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),B))) = inverse(multiply(inverse(C),C)),
    inference(paramod,[status(thm)],[c_3749,c_2259]) ).

cnf(c_4664,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D)))),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D)))))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
    inference(paramod,[status(thm)],[c_313,c_4583]) ).

cnf(c_4665,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(multiply(C,multiply(D,E))),multiply(C,multiply(D,F)))),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
    inference(paramod,[status(thm)],[c_313,c_4583]) ).

cnf(c_4752,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(multiply(inverse(B),B))),C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),F))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_4613,c_44]) ).

cnf(c_8646,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,inverse(multiply(inverse(D),D))))) = multiply(B,inverse(multiply(inverse(inverse(inverse(multiply(inverse(E),E)))),multiply(inverse(C),inverse(multiply(inverse(C),C)))))),
    inference(paramod,[status(thm)],[c_46,c_4583]) ).

cnf(c_5179,plain,
    multiply(A,inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(C),inverse(multiply(inverse(C),C)))))) = inverse(multiply(inverse(multiply(D,multiply(A,C))),multiply(D,inverse(multiply(inverse(E),E))))),
    inference(copy,[status(thm)],[c_8646]) ).

cnf(c_8647,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(multiply(B,C)),D)),E))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,V7))),multiply(inverse(multiply(B,V6)),D))),multiply(inverse(multiply(inverse(multiply(V8,C)),multiply(V8,V7))),E))),
    inference(paramod,[status(thm)],[c_100,c_2252]) ).

cnf(c_5378,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
    inference(copy,[status(thm)],[c_8647]) ).

cnf(c_5499,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),multiply(inverse(C),C))),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_4613,c_2252]) ).

cnf(c_8648,plain,
    inverse(multiply(inverse(multiply(inverse(A),multiply(inverse(multiply(B,C)),D))),multiply(inverse(E),E))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,V7))),multiply(inverse(multiply(B,V6)),D))),multiply(inverse(multiply(inverse(multiply(V8,C)),multiply(V8,V7))),A))),
    inference(paramod,[status(thm)],[c_100,c_2253]) ).

cnf(c_5550,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
    inference(copy,[status(thm)],[c_8648]) ).

cnf(c_8649,plain,
    inverse(multiply(inverse(multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D)))),multiply(inverse(E),E))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),V7)),multiply(inverse(multiply(V8,V6)),multiply(V8,D)))),multiply(inverse(multiply(inverse(multiply(F,C)),V7)),A))),
    inference(paramod,[status(thm)],[c_154,c_2253]) ).

cnf(c_5553,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E)))),multiply(inverse(multiply(inverse(multiply(A,F)),C)),V6))) = inverse(multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(V7,F)),multiply(V7,E)))),multiply(inverse(V8),V8))),
    inference(copy,[status(thm)],[c_8649]) ).

cnf(c_5608,plain,
    inverse(multiply(inverse(multiply(inverse(A),multiply(inverse(B),B))),multiply(inverse(C),C))) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,A))),
    inference(paramod,[status(thm)],[c_3281,c_2253]) ).

cnf(c_5654,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(E),E))),multiply(inverse(multiply(F,D)),multiply(F,C))))))) = B,
    inference(paramod,[status(thm)],[c_2253,c_4583]) ).

cnf(c_5716,plain,
    inverse(multiply(A,multiply(inverse(B),B))) = inverse(multiply(A,multiply(inverse(C),C))),
    inference(paramod,[status(thm)],[c_2116,c_2342]) ).

cnf(c_5829,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(multiply(C,multiply(inverse(D),D))),multiply(C,multiply(inverse(E),E))))))) = B,
    inference(paramod,[status(thm)],[c_5716,c_4583]) ).

cnf(c_5984,plain,
    multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(inverse(D),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_4583,c_49]) ).

cnf(c_6391,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(inverse(multiply(inverse(E),E)),multiply(inverse(F),F))))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_3280,c_44]) ).

cnf(c_7941,plain,
    multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(inverse(multiply(D,multiply(inverse(E),inverse(multiply(inverse(E),E))))),multiply(D,inverse(multiply(F,multiply(inverse(multiply(A,inverse(multiply(inverse(F),multiply(inverse(B),inverse(multiply(inverse(B),B))))))),E))))),
    inference(paramod,[status(thm)],[c_58,c_2256]) ).

cnf(c_7944,plain,
    inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(B,D))))),multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(E),E)))))) = multiply(inverse(D),C),
    inference(paramod,[status(thm)],[c_2256,c_58]) ).

cnf(c_7981,plain,
    inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D))))))) = multiply(A,C),
    inference(paramod,[status(thm)],[c_4583,c_58]) ).

cnf(c_8650,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(multiply(B,inverse(multiply(inverse(inverse(inverse(multiply(inverse(C),C)))),multiply(inverse(D),inverse(multiply(inverse(D),D))))))),inverse(multiply(inverse(multiply(B,inverse(multiply(inverse(inverse(inverse(multiply(inverse(C),C)))),multiply(inverse(D),inverse(multiply(inverse(D),D))))))),multiply(B,inverse(multiply(inverse(inverse(inverse(multiply(inverse(C),C)))),multiply(inverse(D),inverse(multiply(inverse(D),D))))))))))) = multiply(B,D),
    inference(paramod,[status(thm)],[c_4613,c_58]) ).

cnf(c_7985,plain,
    multiply(A,inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(C),inverse(multiply(inverse(C),C)))))) = multiply(A,C),
    inference(paramod,[status(thm)],[c_4583,c_8650]) ).

cnf(c_7991,plain,
    inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(inverse(D),D))))),multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),E))),multiply(inverse(F),F))),multiply(inverse(D),D)))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_4613,c_58]) ).

cnf(c_8010,plain,
    inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D)))),multiply(inverse(D),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(multiply(inverse(F),F)),multiply(inverse(V6),V6))))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_2635,c_58]) ).

cnf(c_8651,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(multiply(C,inverse(multiply(inverse(inverse(multiply(inverse(D),D))),multiply(inverse(E),inverse(multiply(inverse(E),E))))))),F)))),multiply(inverse(F),inverse(multiply(inverse(F),F))))) = multiply(C,E),
    inference(paramod,[status(thm)],[c_3438,c_58]) ).

cnf(c_8014,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(multiply(C,D)),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,D),
    inference(paramod,[status(thm)],[c_4583,c_8651]) ).

cnf(c_8023,plain,
    inverse(multiply(inverse(multiply(A,B)),multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))))) = multiply(A,B),
    inference(paramod,[status(thm)],[c_7985,c_7981]) ).

cnf(c_8652,plain,
    multiply(A,C) = inverse(multiply(inverse(multiply(D,multiply(A,C))),multiply(D,inverse(multiply(inverse(E),E))))),
    inference(paramod,[status(thm)],[c_7985,c_5179]) ).

cnf(c_8025,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,inverse(multiply(inverse(D),D))))) = multiply(B,C),
    inference(copy,[status(thm)],[c_8652]) ).

cnf(c_8653,plain,
    multiply(inverse(A),multiply(B,C)) = inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),multiply(inverse(multiply(B,multiply(inverse(F),F))),A))),
    inference(paramod,[status(thm)],[c_8023,c_3647]) ).

cnf(c_8085,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),F))) = multiply(inverse(F),multiply(D,C)),
    inference(copy,[status(thm)],[c_8653]) ).

cnf(c_8654,plain,
    multiply(inverse(A),multiply(B,C)) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))),multiply(inverse(multiply(B,C)),A))),
    inference(paramod,[status(thm)],[c_8023,c_3617]) ).

cnf(c_8113,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(multiply(C,D)),E))) = multiply(inverse(E),multiply(C,D)),
    inference(copy,[status(thm)],[c_8654]) ).

cnf(c_8655,plain,
    multiply(inverse(A),multiply(inverse(B),C)) = inverse(multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),multiply(inverse(multiply(inverse(E),E)),A))),
    inference(paramod,[status(thm)],[c_8023,c_3599]) ).

cnf(c_8126,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(inverse(D),D)),E))) = multiply(inverse(E),multiply(inverse(B),C)),
    inference(copy,[status(thm)],[c_8655]) ).

cnf(c_8656,plain,
    multiply(inverse(A),multiply(B,C)) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(E),E))),multiply(inverse(multiply(B,D)),A))),
    inference(paramod,[status(thm)],[c_8023,c_3598]) ).

cnf(c_8127,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))),multiply(inverse(multiply(D,B)),E))) = multiply(inverse(E),multiply(D,A)),
    inference(copy,[status(thm)],[c_8656]) ).

cnf(c_8657,plain,
    multiply(inverse(A),multiply(B,C)) = inverse(multiply(D,multiply(inverse(multiply(B,inverse(multiply(inverse(D),multiply(inverse(C),inverse(multiply(inverse(E),E))))))),A))),
    inference(paramod,[status(thm)],[c_8023,c_2352]) ).

cnf(c_8166,plain,
    inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(D),D))))))),E))) = multiply(inverse(E),multiply(B,C)),
    inference(copy,[status(thm)],[c_8657]) ).

cnf(c_8169,plain,
    multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),V6)),multiply(inverse(multiply(V7,F)),multiply(V7,D)))),multiply(inverse(multiply(inverse(multiply(E,C)),V6)),A))),
    inference(paramod,[status(thm)],[c_8023,c_1189]) ).

cnf(c_8184,plain,
    multiply(inverse(A),multiply(inverse(B),B)) = inverse(multiply(inverse(multiply(C,multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(D),D)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8025,c_3579]) ).

cnf(c_8658,plain,
    multiply(inverse(F),multiply(D,C)) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_8085,c_3309]) ).

cnf(c_8195,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))) = multiply(inverse(D),multiply(B,C)),
    inference(copy,[status(thm)],[c_8658]) ).

cnf(c_8659,plain,
    inverse(multiply(multiply(inverse(E),multiply(D,A)),multiply(inverse(multiply(F,multiply(D,A))),V6))) = inverse(multiply(inverse(multiply(V7,multiply(F,E))),multiply(V7,V6))),
    inference(paramod,[status(thm)],[c_8127,c_3051]) ).

cnf(c_8198,plain,
    inverse(multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(multiply(D,multiply(B,C))),E))) = multiply(inverse(E),multiply(D,A)),
    inference(paramod,[status(thm)],[c_8195,c_8659]) ).

cnf(c_8660,plain,
    inverse(multiply(inverse(multiply(inverse(E),multiply(C,D))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,D),
    inference(paramod,[status(thm)],[c_8113,c_8014]) ).

cnf(c_8201,plain,
    multiply(inverse(inverse(multiply(inverse(A),A))),multiply(B,C)) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8195,c_8660]) ).

cnf(c_8238,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(inverse(C),D))),multiply(inverse(multiply(E,B)),multiply(E,F)))) = multiply(inverse(multiply(A,F)),multiply(inverse(C),D)),
    inference(paramod,[status(thm)],[c_8126,c_2874]) ).

cnf(c_8661,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),multiply(inverse(multiply(inverse(C),C)),multiply(inverse(E),E))))) = B,
    inference(paramod,[status(thm)],[c_8238,c_5654]) ).

cnf(c_8249,plain,
    inverse(multiply(inverse(A),multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C)))) = A,
    inference(paramod,[status(thm)],[c_8201,c_8661]) ).

cnf(c_8662,plain,
    inverse(multiply(inverse(multiply(inverse(D),multiply(B,C))),multiply(inverse(D),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(multiply(inverse(F),F)),multiply(inverse(V6),V6))))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8166,c_8010]) ).

cnf(c_8663,plain,
    inverse(multiply(inverse(multiply(inverse(D),multiply(B,C))),multiply(inverse(D),multiply(inverse(E),E)))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8249,c_8662]) ).

cnf(c_8289,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(B,C)) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8195,c_8663]) ).

cnf(c_8664,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(B,C))),multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),E))),multiply(inverse(F),F))),multiply(inverse(D),D)))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8166,c_7991]) ).

cnf(c_8665,plain,
    inverse(multiply(inverse(multiply(B,C)),multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),E))),multiply(inverse(F),F))),multiply(inverse(D),D)))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8289,c_8664]) ).

cnf(c_8666,plain,
    inverse(multiply(inverse(multiply(B,C)),multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(D),D)))))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8201,c_8665]) ).

cnf(c_8295,plain,
    inverse(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(C),C))))) = multiply(A,B),
    inference(paramod,[status(thm)],[c_8289,c_8666]) ).

cnf(c_8667,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(B,D)),multiply(B,C))),multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(E),E)))))) = multiply(inverse(D),C),
    inference(paramod,[status(thm)],[c_8166,c_7944]) ).

cnf(c_8668,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(B,D)),multiply(B,C))),multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(E),E))))) = multiply(inverse(D),C),
    inference(paramod,[status(thm)],[c_8289,c_8667]) ).

cnf(c_8311,plain,
    multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
    inference(paramod,[status(thm)],[c_8295,c_8668]) ).

cnf(c_8669,plain,
    multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(inverse(multiply(D,multiply(inverse(E),inverse(multiply(inverse(E),E))))),multiply(D,multiply(inverse(E),multiply(A,B)))),
    inference(paramod,[status(thm)],[c_8166,c_7941]) ).

cnf(c_8670,plain,
    multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(E),inverse(multiply(inverse(E),E)))),multiply(inverse(E),multiply(A,B))),
    inference(paramod,[status(thm)],[c_8311,c_8669]) ).

cnf(c_8671,plain,
    multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(inverse(inverse(multiply(inverse(E),E))),multiply(A,B)),
    inference(paramod,[status(thm)],[c_8311,c_8670]) ).

cnf(c_8314,plain,
    multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(A,B),
    inference(paramod,[status(thm)],[c_8201,c_8671]) ).

cnf(c_8672,plain,
    inverse(multiply(inverse(multiply(B,C)),D)) = inverse(multiply(E,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(F),F))))))),D))),
    inference(paramod,[status(thm)],[c_8311,c_2422]) ).

cnf(c_8345,plain,
    inverse(multiply(inverse(multiply(A,B)),C)) = multiply(inverse(C),multiply(A,B)),
    inference(paramod,[status(thm)],[c_8166,c_8672]) ).

cnf(c_8673,plain,
    multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(V8,multiply(V6,V7))),multiply(V8,E))),
    inference(paramod,[status(thm)],[c_8311,c_1926]) ).

cnf(c_8674,plain,
    multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),E)) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(V8,multiply(V6,V7))),multiply(V8,E))),
    inference(paramod,[status(thm)],[c_8311,c_8673]) ).

cnf(c_8675,plain,
    multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(V8,multiply(V6,V7))),multiply(V8,E))),
    inference(paramod,[status(thm)],[c_8311,c_8674]) ).

cnf(c_8676,plain,
    multiply(inverse(C),E) = multiply(multiply(inverse(C),multiply(V6,V7)),multiply(inverse(multiply(V8,multiply(V6,V7))),multiply(V8,E))),
    inference(paramod,[status(thm)],[c_8166,c_8675]) ).

cnf(c_8677,plain,
    multiply(inverse(C),E) = multiply(multiply(inverse(C),multiply(V6,V7)),multiply(inverse(multiply(V6,V7)),E)),
    inference(paramod,[status(thm)],[c_8311,c_8676]) ).

cnf(c_8366,plain,
    multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(multiply(B,C)),D)) = multiply(inverse(A),D),
    inference(copy,[status(thm)],[c_8677]) ).

cnf(c_8678,plain,
    inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),E))) = inverse(multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(D,multiply(V6,V7))),E))),
    inference(paramod,[status(thm)],[c_8311,c_1872]) ).

cnf(c_8679,plain,
    multiply(inverse(multiply(inverse(multiply(D,B)),E)),multiply(inverse(B),C)) = inverse(multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(D,multiply(V6,V7))),E))),
    inference(paramod,[status(thm)],[c_8345,c_8678]) ).

cnf(c_8680,plain,
    multiply(multiply(inverse(E),multiply(D,B)),multiply(inverse(B),C)) = inverse(multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(D,multiply(V6,V7))),E))),
    inference(paramod,[status(thm)],[c_8345,c_8679]) ).

cnf(c_8681,plain,
    multiply(multiply(inverse(E),multiply(D,B)),multiply(inverse(B),C)) = inverse(multiply(multiply(inverse(C),multiply(V6,V7)),multiply(inverse(multiply(D,multiply(V6,V7))),E))),
    inference(paramod,[status(thm)],[c_8166,c_8680]) ).

cnf(c_8382,plain,
    multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(C),D)) = multiply(inverse(A),multiply(B,D)),
    inference(paramod,[status(thm)],[c_8198,c_8681]) ).

cnf(c_8682,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8311,c_5550]) ).

cnf(c_8683,plain,
    inverse(multiply(multiply(inverse(multiply(inverse(multiply(D,B)),E)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8345,c_8682]) ).

cnf(c_8684,plain,
    inverse(multiply(multiply(multiply(inverse(E),multiply(D,B)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8345,c_8683]) ).

cnf(c_8685,plain,
    inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8382,c_8684]) ).

cnf(c_8686,plain,
    inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(V6),C)),V7))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8311,c_8685]) ).

cnf(c_8687,plain,
    inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(V6),C)),V7))) = multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),
    inference(paramod,[status(thm)],[c_8345,c_8686]) ).

cnf(c_8411,plain,
    inverse(multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(multiply(inverse(D),C)),E))) = multiply(inverse(E),multiply(inverse(multiply(B,D)),A)),
    inference(paramod,[status(thm)],[c_8289,c_8687]) ).

cnf(c_8688,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
    inference(paramod,[status(thm)],[c_8311,c_5378]) ).

cnf(c_8689,plain,
    inverse(multiply(multiply(inverse(multiply(inverse(multiply(D,B)),E)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
    inference(paramod,[status(thm)],[c_8345,c_8688]) ).

cnf(c_8690,plain,
    inverse(multiply(multiply(multiply(inverse(E),multiply(D,B)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
    inference(paramod,[status(thm)],[c_8345,c_8689]) ).

cnf(c_8691,plain,
    inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
    inference(paramod,[status(thm)],[c_8382,c_8690]) ).

cnf(c_8692,plain,
    inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(V6),C)),V7))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
    inference(paramod,[status(thm)],[c_8311,c_8691]) ).

cnf(c_8693,plain,
    multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E)) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
    inference(paramod,[status(thm)],[c_8411,c_8692]) ).

cnf(c_8694,plain,
    multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E)) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(multiply(inverse(E),multiply(D,V6)),V7))),
    inference(paramod,[status(thm)],[c_8345,c_8693]) ).

cnf(c_8695,plain,
    multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E)) = inverse(multiply(multiply(inverse(E),multiply(D,V6)),V7)),
    inference(paramod,[status(thm)],[c_8289,c_8694]) ).

cnf(c_8412,plain,
    inverse(multiply(multiply(inverse(A),multiply(B,C)),D)) = multiply(inverse(D),multiply(inverse(multiply(B,C)),A)),
    inference(copy,[status(thm)],[c_8695]) ).

cnf(c_8696,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8311,c_1075]) ).

cnf(c_8697,plain,
    inverse(multiply(multiply(inverse(multiply(inverse(multiply(D,B)),E)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8345,c_8696]) ).

cnf(c_8698,plain,
    inverse(multiply(multiply(multiply(inverse(E),multiply(D,B)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8345,c_8697]) ).

cnf(c_8699,plain,
    inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8382,c_8698]) ).

cnf(c_8700,plain,
    inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(V6),C)),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8311,c_8699]) ).

cnf(c_8701,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(V6),C)),multiply(inverse(multiply(D,V6)),V7))),multiply(inverse(multiply(D,C)),E)) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8412,c_8700]) ).

cnf(c_8702,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(D,V6)),V7)),multiply(inverse(V6),C)),multiply(inverse(multiply(D,C)),E)) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8345,c_8701]) ).

cnf(c_8703,plain,
    multiply(multiply(multiply(inverse(V7),multiply(D,V6)),multiply(inverse(V6),C)),multiply(inverse(multiply(D,C)),E)) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8345,c_8702]) ).

cnf(c_8704,plain,
    multiply(multiply(inverse(V7),multiply(D,C)),multiply(inverse(multiply(D,C)),E)) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8382,c_8703]) ).

cnf(c_8705,plain,
    multiply(inverse(V7),E) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8366,c_8704]) ).

cnf(c_8706,plain,
    multiply(inverse(V7),E) = inverse(multiply(inverse(multiply(V9,E)),multiply(V9,V7))),
    inference(paramod,[status(thm)],[c_8311,c_8705]) ).

cnf(c_8707,plain,
    multiply(inverse(V7),E) = inverse(multiply(inverse(E),V7)),
    inference(paramod,[status(thm)],[c_8311,c_8706]) ).

cnf(c_8421,plain,
    inverse(multiply(inverse(A),B)) = multiply(inverse(B),A),
    inference(copy,[status(thm)],[c_8707]) ).

cnf(c_8708,plain,
    inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(E,F)))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_8311,c_1862]) ).

cnf(c_8709,plain,
    inverse(inverse(multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_8421,c_8708]) ).

cnf(c_8710,plain,
    inverse(multiply(inverse(multiply(E,F)),multiply(inverse(multiply(B,C)),D))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_8412,c_8709]) ).

cnf(c_8711,plain,
    multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_8421,c_8710]) ).

cnf(c_8712,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_8421,c_8711]) ).

cnf(c_8713,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),multiply(inverse(C),C)))))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_8421,c_8712]) ).

cnf(c_8714,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,multiply(inverse(multiply(inverse(C),multiply(inverse(C),C))),E))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_8421,c_8713]) ).

cnf(c_8715,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,multiply(multiply(inverse(multiply(inverse(C),C)),C),E))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_8421,c_8714]) ).

cnf(c_8716,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_8421,c_8715]) ).

cnf(c_8717,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),D)),F))),
    inference(paramod,[status(thm)],[c_8311,c_8716]) ).

cnf(c_8718,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(multiply(inverse(D),multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),F))),
    inference(paramod,[status(thm)],[c_8421,c_8717]) ).

cnf(c_8719,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(multiply(inverse(F),multiply(inverse(multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),D))),
    inference(paramod,[status(thm)],[c_8412,c_8718]) ).

cnf(c_8720,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = multiply(inverse(multiply(inverse(multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),D)),F),
    inference(paramod,[status(thm)],[c_8421,c_8719]) ).

cnf(c_8721,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = multiply(multiply(inverse(D),multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),F),
    inference(paramod,[status(thm)],[c_8421,c_8720]) ).

cnf(c_8446,plain,
    multiply(multiply(inverse(A),multiply(B,multiply(multiply(multiply(inverse(C),C),C),D))),E) = multiply(multiply(inverse(A),multiply(B,C)),multiply(D,E)),
    inference(copy,[status(thm)],[c_8721]) ).

cnf(c_8722,plain,
    multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,F)))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),C))),multiply(V6,V7)),
    inference(paramod,[status(thm)],[c_8311,c_1375]) ).

cnf(c_8723,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,F)))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),C))),multiply(V6,V7)),
    inference(paramod,[status(thm)],[c_8421,c_8722]) ).

cnf(c_8724,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),C))),multiply(V6,V7)),
    inference(paramod,[status(thm)],[c_8311,c_8723]) ).

cnf(c_8725,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),multiply(inverse(F),F)))))),C))),multiply(V6,V7)),
    inference(paramod,[status(thm)],[c_8421,c_8724]) ).

cnf(c_8726,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,multiply(inverse(multiply(inverse(F),multiply(inverse(F),F))),inverse(V7)))),C))),multiply(V6,V7)),
    inference(paramod,[status(thm)],[c_8421,c_8725]) ).

cnf(c_8727,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,multiply(multiply(inverse(multiply(inverse(F),F)),F),inverse(V7)))),C))),multiply(V6,V7)),
    inference(paramod,[status(thm)],[c_8421,c_8726]) ).

cnf(c_8728,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,multiply(multiply(multiply(inverse(F),F),F),inverse(V7)))),C))),multiply(V6,V7)),
    inference(paramod,[status(thm)],[c_8421,c_8727]) ).

cnf(c_8729,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(inverse(multiply(E,multiply(multiply(multiply(inverse(F),F),F),inverse(V7)))),C)),V7),
    inference(paramod,[status(thm)],[c_8311,c_8728]) ).

cnf(c_8730,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(multiply(inverse(C),multiply(E,multiply(multiply(multiply(inverse(F),F),F),inverse(V7)))),V7),
    inference(paramod,[status(thm)],[c_8421,c_8729]) ).

cnf(c_8731,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(multiply(inverse(C),multiply(E,F)),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_8446,c_8730]) ).

cnf(c_8447,plain,
    multiply(multiply(inverse(A),B),multiply(inverse(B),multiply(C,D))) = multiply(inverse(A),multiply(C,D)),
    inference(paramod,[status(thm)],[c_8314,c_8731]) ).

cnf(c_8732,plain,
    inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(A),A)))))),E)))) = inverse(inverse(multiply(inverse(multiply(F,multiply(C,A))),multiply(F,E)))),
    inference(paramod,[status(thm)],[c_8421,c_777]) ).

cnf(c_8733,plain,
    inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(B),multiply(inverse(A),A))))),E)))) = inverse(inverse(multiply(inverse(multiply(F,multiply(C,A))),multiply(F,E)))),
    inference(paramod,[status(thm)],[c_8311,c_8732]) ).

cnf(c_8734,plain,
    inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(A),A)),B))),E)))) = inverse(inverse(multiply(inverse(multiply(F,multiply(C,A))),multiply(F,E)))),
    inference(paramod,[status(thm)],[c_8421,c_8733]) ).

cnf(c_8735,plain,
    inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),B))),E)))) = inverse(inverse(multiply(inverse(multiply(F,multiply(C,A))),multiply(F,E)))),
    inference(paramod,[status(thm)],[c_8421,c_8734]) ).

cnf(c_8736,plain,
    inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),B))),E)))) = inverse(inverse(multiply(inverse(multiply(C,A)),E))),
    inference(paramod,[status(thm)],[c_8311,c_8735]) ).

cnf(c_8737,plain,
    inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),B))),E)))) = inverse(multiply(inverse(E),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8736]) ).

cnf(c_8459,plain,
    inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),B))),D)))) = multiply(inverse(multiply(C,A)),D),
    inference(paramod,[status(thm)],[c_8421,c_8737]) ).

cnf(c_8738,plain,
    inverse(multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(A),A)))))),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8421,c_757]) ).

cnf(c_8739,plain,
    inverse(multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(B),multiply(inverse(A),A))))),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8311,c_8738]) ).

cnf(c_8740,plain,
    inverse(multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(A),A)),B))),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8421,c_8739]) ).

cnf(c_8741,plain,
    inverse(multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),B))),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8421,c_8740]) ).

cnf(c_8742,plain,
    inverse(multiply(multiply(inverse(multiply(C,A)),E),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8459,c_8741]) ).

cnf(c_8743,plain,
    inverse(multiply(multiply(inverse(multiply(C,A)),E),multiply(inverse(E),multiply(inverse(E),E)))) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8421,c_8742]) ).

cnf(c_8744,plain,
    inverse(multiply(inverse(multiply(C,A)),multiply(inverse(E),E))) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8447,c_8743]) ).

cnf(c_8745,plain,
    multiply(inverse(multiply(inverse(E),E)),multiply(C,A)) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8421,c_8744]) ).

cnf(c_8460,plain,
    multiply(multiply(inverse(A),A),multiply(B,C)) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8421,c_8745]) ).

cnf(c_8746,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(multiply(C,multiply(D,E))),multiply(C,multiply(D,F)))),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
    inference(paramod,[status(thm)],[c_8421,c_4665]) ).

cnf(c_8747,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(multiply(C,multiply(D,E))),multiply(C,multiply(D,F)))),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
    inference(paramod,[status(thm)],[c_8421,c_8746]) ).

cnf(c_8748,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,F))),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
    inference(paramod,[status(thm)],[c_8311,c_8747]) ).

cnf(c_8749,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(E),F)),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
    inference(paramod,[status(thm)],[c_8311,c_8748]) ).

cnf(c_8750,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(multiply(inverse(F),E),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
    inference(paramod,[status(thm)],[c_8421,c_8749]) ).

cnf(c_8751,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(multiply(inverse(F),E),multiply(inverse(multiply(V7,E)),multiply(V7,F))))))) = B,
    inference(paramod,[status(thm)],[c_8311,c_8750]) ).

cnf(c_8752,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(multiply(inverse(F),E),multiply(inverse(E),F)))))) = B,
    inference(paramod,[status(thm)],[c_8311,c_8751]) ).

cnf(c_8753,plain,
    inverse(multiply(inverse(B),inverse(multiply(multiply(inverse(F),E),multiply(inverse(E),F))))) = B,
    inference(paramod,[status(thm)],[c_8460,c_8752]) ).

cnf(c_8472,plain,
    multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(B),A)))),C) = C,
    inference(paramod,[status(thm)],[c_8421,c_8753]) ).

cnf(c_8754,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,D))),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D)))))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
    inference(paramod,[status(thm)],[c_8311,c_4664]) ).

cnf(c_8755,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D)))))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
    inference(paramod,[status(thm)],[c_8311,c_8754]) ).

cnf(c_8756,plain,
    inverse(multiply(inverse(inverse(multiply(multiply(inverse(D),C),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D)))))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
    inference(paramod,[status(thm)],[c_8421,c_8755]) ).

cnf(c_8757,plain,
    inverse(multiply(inverse(inverse(multiply(multiply(inverse(D),C),multiply(inverse(multiply(F,C)),multiply(F,D))))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
    inference(paramod,[status(thm)],[c_8311,c_8756]) ).

cnf(c_8758,plain,
    inverse(multiply(inverse(inverse(multiply(multiply(inverse(D),C),multiply(inverse(C),D)))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
    inference(paramod,[status(thm)],[c_8311,c_8757]) ).

cnf(c_8759,plain,
    inverse(multiply(inverse(inverse(multiply(multiply(inverse(D),C),multiply(inverse(C),D)))),multiply(inverse(V6),multiply(inverse(V7),V7)))) = V6,
    inference(paramod,[status(thm)],[c_8421,c_8758]) ).

cnf(c_8760,plain,
    inverse(multiply(inverse(V6),multiply(inverse(V7),V7))) = V6,
    inference(paramod,[status(thm)],[c_8472,c_8759]) ).

cnf(c_8761,plain,
    multiply(inverse(multiply(inverse(V7),V7)),V6) = V6,
    inference(paramod,[status(thm)],[c_8421,c_8760]) ).

cnf(c_8473,plain,
    multiply(multiply(inverse(A),A),B) = B,
    inference(paramod,[status(thm)],[c_8421,c_8761]) ).

cnf(c_8762,plain,
    multiply(inverse(A),multiply(inverse(C),D)) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),V6)),multiply(inverse(multiply(V7,F)),multiply(V7,D)))),multiply(inverse(multiply(inverse(multiply(E,C)),V6)),A))),
    inference(paramod,[status(thm)],[c_8311,c_8169]) ).

cnf(c_8763,plain,
    multiply(inverse(A),multiply(inverse(C),D)) = inverse(multiply(inverse(multiply(multiply(inverse(V6),multiply(E,F)),multiply(inverse(multiply(V7,F)),multiply(V7,D)))),multiply(inverse(multiply(inverse(multiply(E,C)),V6)),A))),
    inference(paramod,[status(thm)],[c_8421,c_8762]) ).

cnf(c_8764,plain,
    multiply(inverse(A),multiply(inverse(C),D)) = inverse(multiply(inverse(multiply(multiply(inverse(V6),multiply(E,F)),multiply(inverse(F),D))),multiply(inverse(multiply(inverse(multiply(E,C)),V6)),A))),
    inference(paramod,[status(thm)],[c_8311,c_8763]) ).

cnf(c_8765,plain,
    multiply(inverse(A),multiply(inverse(C),D)) = inverse(multiply(inverse(multiply(inverse(V6),multiply(E,D))),multiply(inverse(multiply(inverse(multiply(E,C)),V6)),A))),
    inference(paramod,[status(thm)],[c_8382,c_8764]) ).

cnf(c_8766,plain,
    multiply(inverse(A),multiply(inverse(C),D)) = inverse(multiply(multiply(inverse(multiply(E,D)),V6),multiply(inverse(multiply(inverse(multiply(E,C)),V6)),A))),
    inference(paramod,[status(thm)],[c_8421,c_8765]) ).

cnf(c_8767,plain,
    multiply(inverse(A),multiply(inverse(C),D)) = inverse(multiply(multiply(inverse(multiply(E,D)),V6),multiply(multiply(inverse(V6),multiply(E,C)),A))),
    inference(paramod,[status(thm)],[c_8421,c_8766]) ).

cnf(c_8493,plain,
    inverse(multiply(multiply(inverse(multiply(A,B)),C),multiply(multiply(inverse(C),multiply(A,D)),E))) = multiply(inverse(E),multiply(inverse(D),B)),
    inference(copy,[status(thm)],[c_8767]) ).

cnf(c_8768,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(C),multiply(A,B)),multiply(inverse(multiply(D,B)),multiply(D,E)))),multiply(inverse(multiply(inverse(multiply(A,F)),C)),V6))) = inverse(multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(V7,F)),multiply(V7,E)))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8421,c_5553]) ).

cnf(c_8769,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(C),multiply(A,B)),multiply(inverse(B),E))),multiply(inverse(multiply(inverse(multiply(A,F)),C)),V6))) = inverse(multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(V7,F)),multiply(V7,E)))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8311,c_8768]) ).

cnf(c_8770,plain,
    inverse(multiply(inverse(multiply(inverse(C),multiply(A,E))),multiply(inverse(multiply(inverse(multiply(A,F)),C)),V6))) = inverse(multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(V7,F)),multiply(V7,E)))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8382,c_8769]) ).

cnf(c_8771,plain,
    inverse(multiply(multiply(inverse(multiply(A,E)),C),multiply(inverse(multiply(inverse(multiply(A,F)),C)),V6))) = inverse(multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(V7,F)),multiply(V7,E)))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8421,c_8770]) ).

cnf(c_8772,plain,
    inverse(multiply(multiply(inverse(multiply(A,E)),C),multiply(multiply(inverse(C),multiply(A,F)),V6))) = inverse(multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(V7,F)),multiply(V7,E)))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8421,c_8771]) ).

cnf(c_8773,plain,
    multiply(inverse(V6),multiply(inverse(F),E)) = inverse(multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(V7,F)),multiply(V7,E)))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8493,c_8772]) ).

cnf(c_8774,plain,
    multiply(inverse(V6),multiply(inverse(F),E)) = inverse(multiply(inverse(multiply(inverse(V6),multiply(inverse(F),E))),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8311,c_8773]) ).

cnf(c_8775,plain,
    multiply(inverse(V6),multiply(inverse(F),E)) = inverse(multiply(multiply(inverse(multiply(inverse(F),E)),V6),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8421,c_8774]) ).

cnf(c_8776,plain,
    multiply(inverse(V6),multiply(inverse(F),E)) = inverse(multiply(multiply(multiply(inverse(E),F),V6),multiply(inverse(V8),V8))),
    inference(paramod,[status(thm)],[c_8421,c_8775]) ).

cnf(c_8777,plain,
    multiply(inverse(V6),multiply(inverse(F),E)) = inverse(multiply(multiply(inverse(E),F),V6)),
    inference(paramod,[status(thm)],[c_8314,c_8776]) ).

cnf(c_8495,plain,
    inverse(multiply(multiply(inverse(A),B),C)) = multiply(inverse(C),multiply(inverse(B),A)),
    inference(copy,[status(thm)],[c_8777]) ).

cnf(c_8778,plain,
    multiply(inverse(A),multiply(inverse(B),B)) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(A),A)),multiply(inverse(D),D)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8184]) ).

cnf(c_8779,plain,
    multiply(inverse(A),multiply(inverse(B),B)) = inverse(multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),multiply(inverse(D),D)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8778]) ).

cnf(c_8780,plain,
    multiply(inverse(A),multiply(inverse(B),B)) = inverse(multiply(inverse(multiply(C,multiply(inverse(A),A))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8314,c_8779]) ).

cnf(c_8781,plain,
    multiply(inverse(A),multiply(inverse(B),B)) = inverse(multiply(inverse(multiply(inverse(A),A)),A)),
    inference(paramod,[status(thm)],[c_8311,c_8780]) ).

cnf(c_8782,plain,
    multiply(inverse(A),multiply(inverse(B),B)) = inverse(multiply(multiply(inverse(A),A),A)),
    inference(paramod,[status(thm)],[c_8421,c_8781]) ).

cnf(c_8531,plain,
    multiply(inverse(A),multiply(inverse(B),B)) = inverse(A),
    inference(paramod,[status(thm)],[c_8473,c_8782]) ).

cnf(c_8783,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(inverse(D),D)))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8421,c_8025]) ).

cnf(c_8784,plain,
    inverse(multiply(inverse(multiply(B,C)),multiply(inverse(D),D))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8311,c_8783]) ).

cnf(c_8537,plain,
    inverse(inverse(multiply(A,B))) = multiply(A,B),
    inference(paramod,[status(thm)],[c_8531,c_8784]) ).

cnf(c_8785,plain,
    inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(inverse(multiply(inverse(E),E)),multiply(inverse(F),F))))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_8311,c_6391]) ).

cnf(c_8786,plain,
    inverse(multiply(multiply(inverse(C),B),multiply(inverse(multiply(D,B)),multiply(inverse(multiply(inverse(E),E)),multiply(inverse(F),F))))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_8421,c_8785]) ).

cnf(c_8787,plain,
    inverse(multiply(multiply(inverse(C),B),multiply(inverse(multiply(D,B)),multiply(multiply(inverse(E),E),multiply(inverse(F),F))))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_8421,c_8786]) ).

cnf(c_8788,plain,
    inverse(multiply(multiply(inverse(C),B),multiply(inverse(multiply(D,B)),multiply(inverse(E),E)))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_8314,c_8787]) ).

cnf(c_8789,plain,
    inverse(multiply(multiply(inverse(C),B),inverse(multiply(D,B)))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_8531,c_8788]) ).

cnf(c_8790,plain,
    multiply(inverse(inverse(multiply(D,B))),multiply(inverse(B),C)) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_8495,c_8789]) ).

cnf(c_8791,plain,
    multiply(multiply(D,B),multiply(inverse(B),C)) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_8537,c_8790]) ).

cnf(c_8792,plain,
    multiply(multiply(D,B),multiply(inverse(B),C)) = inverse(multiply(inverse(multiply(D,C)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_8311,c_8791]) ).

cnf(c_8793,plain,
    multiply(multiply(D,B),multiply(inverse(B),C)) = inverse(inverse(multiply(D,C))),
    inference(paramod,[status(thm)],[c_8531,c_8792]) ).

cnf(c_8563,plain,
    multiply(multiply(A,B),multiply(inverse(B),C)) = multiply(A,C),
    inference(paramod,[status(thm)],[c_8537,c_8793]) ).

cnf(c_8794,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),inverse(multiply(inverse(multiply(C,multiply(inverse(D),D))),multiply(C,multiply(inverse(E),E))))))) = B,
    inference(paramod,[status(thm)],[c_8421,c_5829]) ).

cnf(c_8795,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(inverse(multiply(C,multiply(inverse(D),D))),multiply(C,multiply(inverse(E),E))))))) = B,
    inference(paramod,[status(thm)],[c_8421,c_8794]) ).

cnf(c_8796,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E)))))) = B,
    inference(paramod,[status(thm)],[c_8311,c_8795]) ).

cnf(c_8797,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(multiply(inverse(D),D),multiply(inverse(E),E)))))) = B,
    inference(paramod,[status(thm)],[c_8421,c_8796]) ).

cnf(c_8798,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(inverse(D),D))))) = B,
    inference(paramod,[status(thm)],[c_8314,c_8797]) ).

cnf(c_8799,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),multiply(inverse(D),D)))) = B,
    inference(paramod,[status(thm)],[c_8421,c_8798]) ).

cnf(c_8800,plain,
    inverse(multiply(multiply(inverse(A),A),inverse(B))) = B,
    inference(paramod,[status(thm)],[c_8531,c_8799]) ).

cnf(c_8565,plain,
    inverse(inverse(A)) = A,
    inference(paramod,[status(thm)],[c_8473,c_8800]) ).

cnf(c_8801,plain,
    inverse(multiply(inverse(inverse(A)),multiply(inverse(C),C))) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,A))),
    inference(paramod,[status(thm)],[c_8531,c_5608]) ).

cnf(c_8802,plain,
    inverse(multiply(A,multiply(inverse(C),C))) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,A))),
    inference(paramod,[status(thm)],[c_8565,c_8801]) ).

cnf(c_8803,plain,
    inverse(multiply(A,multiply(inverse(C),C))) = inverse(multiply(inverse(multiply(inverse(E),E)),A)),
    inference(paramod,[status(thm)],[c_8311,c_8802]) ).

cnf(c_8804,plain,
    inverse(multiply(A,multiply(inverse(C),C))) = inverse(multiply(multiply(inverse(E),E),A)),
    inference(paramod,[status(thm)],[c_8421,c_8803]) ).

cnf(c_8567,plain,
    inverse(multiply(A,multiply(inverse(B),B))) = inverse(A),
    inference(paramod,[status(thm)],[c_8473,c_8804]) ).

cnf(c_8805,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),multiply(inverse(C),C))),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_8421,c_5499]) ).

cnf(c_8806,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_8421,c_8805]) ).

cnf(c_8807,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(multiply(multiply(inverse(B),B),multiply(inverse(C),C))),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_8421,c_8806]) ).

cnf(c_8808,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(B),B)),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_8314,c_8807]) ).

cnf(c_8809,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_8421,c_8808]) ).

cnf(c_8810,plain,
    inverse(multiply(multiply(inverse(A),A),D)) = inverse(multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_8473,c_8809]) ).

cnf(c_8811,plain,
    inverse(D) = inverse(multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_8473,c_8810]) ).

cnf(c_8812,plain,
    inverse(D) = inverse(multiply(inverse(E),multiply(E,D))),
    inference(paramod,[status(thm)],[c_8567,c_8811]) ).

cnf(c_8813,plain,
    inverse(D) = multiply(inverse(multiply(E,D)),E),
    inference(paramod,[status(thm)],[c_8421,c_8812]) ).

cnf(c_8569,plain,
    multiply(inverse(multiply(A,B)),A) = inverse(B),
    inference(copy,[status(thm)],[c_8813]) ).

cnf(c_8814,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(inverse(multiply(inverse(B),B))),C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),F))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_8421,c_4752]) ).

cnf(c_8815,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(B),B)),C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),F))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_8421,c_8814]) ).

cnf(c_8816,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),F))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_8421,c_8815]) ).

cnf(c_8817,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(A),A),C)),multiply(inverse(multiply(D,multiply(inverse(E),E))),F))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_8473,c_8816]) ).

cnf(c_8818,plain,
    inverse(multiply(inverse(C),multiply(inverse(multiply(D,multiply(inverse(E),E))),F))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_8473,c_8817]) ).

cnf(c_8819,plain,
    inverse(multiply(inverse(C),multiply(inverse(D),F))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_8567,c_8818]) ).

cnf(c_8820,plain,
    multiply(inverse(multiply(inverse(D),F)),C) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_8421,c_8819]) ).

cnf(c_8821,plain,
    multiply(multiply(inverse(F),D),C) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_8421,c_8820]) ).

cnf(c_8822,plain,
    multiply(multiply(inverse(F),D),C) = inverse(multiply(inverse(multiply(D,C)),F)),
    inference(paramod,[status(thm)],[c_8311,c_8821]) ).

cnf(c_8584,plain,
    multiply(multiply(inverse(A),B),C) = multiply(inverse(A),multiply(B,C)),
    inference(paramod,[status(thm)],[c_8421,c_8822]) ).

cnf(c_8823,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(C),D))),multiply(A,E))),multiply(inverse(F),F)) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(multiply(V7,E)),multiply(V7,multiply(inverse(multiply(V8,C)),multiply(V8,D))))),
    inference(paramod,[status(thm)],[c_8311,c_4414]) ).

cnf(c_8824,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(C),D)),E)),multiply(inverse(F),F)) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(multiply(V7,E)),multiply(V7,multiply(inverse(multiply(V8,C)),multiply(V8,D))))),
    inference(paramod,[status(thm)],[c_8311,c_8823]) ).

cnf(c_8825,plain,
    multiply(inverse(multiply(multiply(inverse(D),C),E)),multiply(inverse(F),F)) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(multiply(V7,E)),multiply(V7,multiply(inverse(multiply(V8,C)),multiply(V8,D))))),
    inference(paramod,[status(thm)],[c_8421,c_8824]) ).

cnf(c_8826,plain,
    multiply(inverse(multiply(inverse(D),multiply(C,E))),multiply(inverse(F),F)) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(multiply(V7,E)),multiply(V7,multiply(inverse(multiply(V8,C)),multiply(V8,D))))),
    inference(paramod,[status(thm)],[c_8584,c_8825]) ).

cnf(c_8827,plain,
    multiply(multiply(inverse(multiply(C,E)),D),multiply(inverse(F),F)) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(multiply(V7,E)),multiply(V7,multiply(inverse(multiply(V8,C)),multiply(V8,D))))),
    inference(paramod,[status(thm)],[c_8421,c_8826]) ).

cnf(c_8828,plain,
    multiply(inverse(multiply(C,E)),D) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(multiply(V7,E)),multiply(V7,multiply(inverse(multiply(V8,C)),multiply(V8,D))))),
    inference(paramod,[status(thm)],[c_8314,c_8827]) ).

cnf(c_8829,plain,
    multiply(inverse(multiply(C,E)),D) = multiply(multiply(inverse(V6),V6),multiply(inverse(multiply(V7,E)),multiply(V7,multiply(inverse(multiply(V8,C)),multiply(V8,D))))),
    inference(paramod,[status(thm)],[c_8421,c_8828]) ).

cnf(c_8830,plain,
    multiply(inverse(multiply(C,E)),D) = multiply(multiply(inverse(V6),V6),multiply(inverse(multiply(V7,E)),multiply(V7,multiply(inverse(C),D)))),
    inference(paramod,[status(thm)],[c_8311,c_8829]) ).

cnf(c_8831,plain,
    multiply(inverse(multiply(C,E)),D) = multiply(multiply(inverse(V6),V6),multiply(inverse(E),multiply(inverse(C),D))),
    inference(paramod,[status(thm)],[c_8311,c_8830]) ).

cnf(c_8586,plain,
    multiply(inverse(multiply(A,B)),C) = multiply(inverse(B),multiply(inverse(A),C)),
    inference(paramod,[status(thm)],[c_8473,c_8831]) ).

cnf(c_8832,plain,
    multiply(inverse(multiply(inverse(multiply(B,C)),multiply(inverse(A),multiply(A,multiply(B,D))))),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8586,c_4404]) ).

cnf(c_8833,plain,
    multiply(inverse(multiply(inverse(C),multiply(inverse(B),multiply(inverse(A),multiply(A,multiply(B,D)))))),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8586,c_8832]) ).

cnf(c_8834,plain,
    multiply(multiply(inverse(multiply(inverse(B),multiply(inverse(A),multiply(A,multiply(B,D))))),C),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8833]) ).

cnf(c_8835,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(A),multiply(A,multiply(B,D)))),B),C),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8834]) ).

cnf(c_8836,plain,
    multiply(multiply(multiply(multiply(inverse(multiply(A,multiply(B,D))),A),B),C),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8835]) ).

cnf(c_8837,plain,
    multiply(multiply(multiply(inverse(multiply(B,D)),B),C),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8569,c_8836]) ).

cnf(c_8838,plain,
    multiply(multiply(inverse(D),C),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8569,c_8837]) ).

cnf(c_8839,plain,
    multiply(inverse(D),C) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8314,c_8838]) ).

cnf(c_8840,plain,
    multiply(inverse(D),C) = multiply(multiply(inverse(F),F),multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8839]) ).

cnf(c_8841,plain,
    multiply(inverse(D),C) = multiply(multiply(inverse(F),F),multiply(inverse(multiply(inverse(V7),multiply(inverse(V6),multiply(V6,D)))),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8586,c_8840]) ).

cnf(c_8842,plain,
    multiply(inverse(D),C) = multiply(multiply(inverse(F),F),multiply(multiply(inverse(multiply(inverse(V6),multiply(V6,D))),V7),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8841]) ).

cnf(c_8843,plain,
    multiply(inverse(D),C) = multiply(multiply(inverse(F),F),multiply(multiply(multiply(inverse(multiply(V6,D)),V6),V7),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8842]) ).

cnf(c_8844,plain,
    multiply(inverse(D),C) = multiply(multiply(inverse(F),F),multiply(multiply(inverse(D),V7),multiply(inverse(multiply(V8,V7)),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8569,c_8843]) ).

cnf(c_8845,plain,
    multiply(inverse(D),C) = multiply(multiply(inverse(F),F),multiply(multiply(inverse(D),V7),multiply(inverse(V7),multiply(inverse(V8),multiply(V8,C))))),
    inference(paramod,[status(thm)],[c_8586,c_8844]) ).

cnf(c_8846,plain,
    multiply(inverse(D),C) = multiply(multiply(inverse(F),F),multiply(inverse(D),multiply(inverse(V8),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8563,c_8845]) ).

cnf(c_8847,plain,
    multiply(inverse(D),C) = multiply(inverse(D),multiply(inverse(V8),multiply(V8,C))),
    inference(paramod,[status(thm)],[c_8473,c_8846]) ).

cnf(c_8587,plain,
    multiply(inverse(A),multiply(inverse(B),multiply(B,C))) = multiply(inverse(A),C),
    inference(copy,[status(thm)],[c_8847]) ).

cnf(c_8848,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(B),A),multiply(inverse(C),D))),multiply(inverse(multiply(inverse(E),E)),multiply(inverse(B),A)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8421,c_4347]) ).

cnf(c_8849,plain,
    inverse(multiply(inverse(multiply(inverse(B),multiply(A,multiply(inverse(C),D)))),multiply(inverse(multiply(inverse(E),E)),multiply(inverse(B),A)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8584,c_8848]) ).

cnf(c_8850,plain,
    inverse(multiply(multiply(inverse(multiply(A,multiply(inverse(C),D))),B),multiply(inverse(multiply(inverse(E),E)),multiply(inverse(B),A)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8849]) ).

cnf(c_8851,plain,
    inverse(multiply(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(A),B)),multiply(inverse(multiply(inverse(E),E)),multiply(inverse(B),A)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8586,c_8850]) ).

cnf(c_8852,plain,
    inverse(multiply(multiply(multiply(inverse(D),C),multiply(inverse(A),B)),multiply(inverse(multiply(inverse(E),E)),multiply(inverse(B),A)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8851]) ).

cnf(c_8853,plain,
    inverse(multiply(multiply(inverse(D),multiply(C,multiply(inverse(A),B))),multiply(inverse(multiply(inverse(E),E)),multiply(inverse(B),A)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8584,c_8852]) ).

cnf(c_8854,plain,
    inverse(multiply(multiply(inverse(D),multiply(C,multiply(inverse(A),B))),multiply(multiply(inverse(E),E),multiply(inverse(B),A)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8853]) ).

cnf(c_8855,plain,
    inverse(multiply(multiply(inverse(D),multiply(C,multiply(inverse(A),B))),multiply(inverse(B),A))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8473,c_8854]) ).

cnf(c_8856,plain,
    inverse(multiply(inverse(D),multiply(multiply(C,multiply(inverse(A),B)),multiply(inverse(B),A)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8584,c_8855]) ).

cnf(c_8857,plain,
    multiply(inverse(multiply(multiply(C,multiply(inverse(A),B)),multiply(inverse(B),A))),D) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8856]) ).

cnf(c_8858,plain,
    multiply(inverse(multiply(inverse(B),A)),multiply(inverse(multiply(C,multiply(inverse(A),B))),D)) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8586,c_8857]) ).

cnf(c_8859,plain,
    multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(inverse(A),B))),D)) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8858]) ).

cnf(c_8860,plain,
    multiply(multiply(inverse(A),B),multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),D))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8586,c_8859]) ).

cnf(c_8861,plain,
    multiply(multiply(inverse(A),B),multiply(multiply(inverse(B),A),multiply(inverse(C),D))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8421,c_8860]) ).

cnf(c_8862,plain,
    multiply(multiply(inverse(A),B),multiply(inverse(B),multiply(A,multiply(inverse(C),D)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8584,c_8861]) ).

cnf(c_8863,plain,
    multiply(inverse(A),multiply(A,multiply(inverse(C),D))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8563,c_8862]) ).

cnf(c_8864,plain,
    multiply(inverse(A),multiply(A,multiply(inverse(C),D))) = inverse(multiply(inverse(multiply(V6,D)),multiply(inverse(F),multiply(F,multiply(V6,C))))),
    inference(paramod,[status(thm)],[c_8586,c_8863]) ).

cnf(c_8865,plain,
    multiply(inverse(A),multiply(A,multiply(inverse(C),D))) = inverse(multiply(inverse(multiply(V6,D)),multiply(V6,C))),
    inference(paramod,[status(thm)],[c_8587,c_8864]) ).

cnf(c_8866,plain,
    multiply(inverse(A),multiply(A,multiply(inverse(C),D))) = inverse(multiply(inverse(D),multiply(inverse(V6),multiply(V6,C)))),
    inference(paramod,[status(thm)],[c_8586,c_8865]) ).

cnf(c_8867,plain,
    multiply(inverse(A),multiply(A,multiply(inverse(C),D))) = inverse(multiply(inverse(D),C)),
    inference(paramod,[status(thm)],[c_8587,c_8866]) ).

cnf(c_8588,plain,
    multiply(inverse(A),multiply(A,multiply(inverse(B),C))) = multiply(inverse(B),C),
    inference(paramod,[status(thm)],[c_8421,c_8867]) ).

cnf(c_8868,plain,
    inverse(multiply(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(C),C)))))),multiply(A,C)),multiply(inverse(D),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F)))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8421,c_2790]) ).

cnf(c_8869,plain,
    inverse(multiply(multiply(inverse(multiply(A,inverse(multiply(inverse(B),inverse(C))))),multiply(A,C)),multiply(inverse(D),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F)))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8531,c_8868]) ).

cnf(c_8870,plain,
    inverse(multiply(multiply(inverse(multiply(A,multiply(inverse(inverse(C)),B))),multiply(A,C)),multiply(inverse(D),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F)))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8421,c_8869]) ).

cnf(c_8871,plain,
    inverse(multiply(multiply(inverse(multiply(A,multiply(C,B))),multiply(A,C)),multiply(inverse(D),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F)))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_8870]) ).

cnf(c_8872,plain,
    inverse(multiply(multiply(inverse(multiply(C,B)),multiply(inverse(A),multiply(A,C))),multiply(inverse(D),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F)))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8586,c_8871]) ).

cnf(c_8873,plain,
    inverse(multiply(multiply(inverse(multiply(C,B)),C),multiply(inverse(D),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F)))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8587,c_8872]) ).

cnf(c_8874,plain,
    inverse(multiply(inverse(B),multiply(inverse(D),D))) = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F)))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8569,c_8873]) ).

cnf(c_8875,plain,
    inverse(inverse(B)) = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F)))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8531,c_8874]) ).

cnf(c_8876,plain,
    B = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F)))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_8875]) ).

cnf(c_8877,plain,
    B = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,multiply(inverse(F),multiply(inverse(F),F))))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8421,c_8876]) ).

cnf(c_8878,plain,
    B = inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(multiply(B,inverse(F)))),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8531,c_8877]) ).

cnf(c_8879,plain,
    B = inverse(multiply(inverse(multiply(E,multiply(multiply(B,inverse(F)),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_8878]) ).

cnf(c_8880,plain,
    B = inverse(multiply(inverse(multiply(multiply(B,inverse(F)),F)),multiply(inverse(E),multiply(E,multiply(inverse(V6),V6))))),
    inference(paramod,[status(thm)],[c_8586,c_8879]) ).

cnf(c_8881,plain,
    B = inverse(multiply(inverse(multiply(multiply(B,inverse(F)),F)),multiply(inverse(V6),V6))),
    inference(paramod,[status(thm)],[c_8588,c_8880]) ).

cnf(c_8882,plain,
    B = inverse(inverse(multiply(multiply(B,inverse(F)),F))),
    inference(paramod,[status(thm)],[c_8531,c_8881]) ).

cnf(c_8883,plain,
    B = multiply(multiply(B,inverse(F)),F),
    inference(paramod,[status(thm)],[c_8565,c_8882]) ).

cnf(c_8595,plain,
    multiply(multiply(A,inverse(B)),B) = A,
    inference(copy,[status(thm)],[c_8883]) ).

cnf(c_8884,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(C),C))))),C))),multiply(A,D))) = inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D))),
    inference(paramod,[status(thm)],[c_8421,c_2424]) ).

cnf(c_8885,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(inverse(multiply(inverse(B),inverse(C)))),C))),multiply(A,D))) = inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D))),
    inference(paramod,[status(thm)],[c_8531,c_8884]) ).

cnf(c_8886,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(inverse(C)),B)),C))),multiply(A,D))) = inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D))),
    inference(paramod,[status(thm)],[c_8421,c_8885]) ).

cnf(c_8887,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(multiply(C,B)),C))),multiply(A,D))) = inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D))),
    inference(paramod,[status(thm)],[c_8565,c_8886]) ).

cnf(c_8888,plain,
    inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,D))) = inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D))),
    inference(paramod,[status(thm)],[c_8569,c_8887]) ).

cnf(c_8889,plain,
    inverse(multiply(inverse(inverse(B)),multiply(inverse(A),multiply(A,D)))) = inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D))),
    inference(paramod,[status(thm)],[c_8586,c_8888]) ).

cnf(c_8890,plain,
    inverse(multiply(B,multiply(inverse(A),multiply(A,D)))) = inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D))),
    inference(paramod,[status(thm)],[c_8565,c_8889]) ).

cnf(c_8891,plain,
    inverse(multiply(B,multiply(inverse(A),multiply(A,D)))) = inverse(multiply(B,multiply(multiply(inverse(E),E),D))),
    inference(paramod,[status(thm)],[c_8421,c_8890]) ).

cnf(c_8597,plain,
    inverse(multiply(A,multiply(inverse(B),multiply(B,C)))) = inverse(multiply(A,C)),
    inference(paramod,[status(thm)],[c_8473,c_8891]) ).

cnf(c_8892,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_2287]) ).

cnf(c_8893,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8892]) ).

cnf(c_8894,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8893]) ).

cnf(c_8895,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(multiply(inverse(A),A),inverse(multiply(multiply(inverse(A),A),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8894]) ).

cnf(c_8896,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(multiply(inverse(A),A),inverse(multiply(multiply(inverse(A),A),multiply(inverse(A),A))))))) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8895]) ).

cnf(c_8897,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(multiply(inverse(A),A),inverse(multiply(inverse(A),A)))))) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8563,c_8896]) ).

cnf(c_8898,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(multiply(inverse(A),A),multiply(inverse(A),A))))) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8897]) ).

cnf(c_8899,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(inverse(A),A)))) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8563,c_8898]) ).

cnf(c_8900,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8567,c_8899]) ).

cnf(c_8901,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(inverse(multiply(C,multiply(multiply(inverse(D),D),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E)))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8900]) ).

cnf(c_8902,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(inverse(multiply(C,multiply(multiply(inverse(D),D),multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),multiply(inverse(E),E))))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8901]) ).

cnf(c_8903,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(inverse(multiply(C,multiply(multiply(inverse(D),D),multiply(inverse(inverse(multiply(inverse(B),inverse(E)))),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8531,c_8902]) ).

cnf(c_8904,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(inverse(multiply(C,multiply(multiply(inverse(D),D),multiply(inverse(multiply(inverse(inverse(E)),B)),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8421,c_8903]) ).

cnf(c_8905,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(inverse(multiply(C,multiply(multiply(inverse(D),D),multiply(inverse(multiply(E,B)),E)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8565,c_8904]) ).

cnf(c_8906,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(inverse(multiply(C,multiply(multiply(inverse(D),D),inverse(B)))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8569,c_8905]) ).

cnf(c_8907,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(inverse(multiply(C,inverse(B))),multiply(C,A))),
    inference(paramod,[status(thm)],[c_8473,c_8906]) ).

cnf(c_8908,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(inverse(inverse(B)),multiply(inverse(C),multiply(C,A)))),
    inference(paramod,[status(thm)],[c_8586,c_8907]) ).

cnf(c_8909,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(B,multiply(inverse(C),multiply(C,A)))),
    inference(paramod,[status(thm)],[c_8565,c_8908]) ).

cnf(c_8910,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
    inference(paramod,[status(thm)],[c_8597,c_8909]) ).

cnf(c_8598,plain,
    inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
    inference(copy,[status(thm)],[c_8910]) ).

cnf(c_8911,plain,
    multiply(inverse(inverse(multiply(multiply(inverse(inverse(B)),inverse(A)),multiply(A,multiply(inverse(C),C))))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_2092]) ).

cnf(c_8912,plain,
    multiply(inverse(inverse(multiply(multiply(B,inverse(A)),multiply(A,multiply(inverse(C),C))))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8565,c_8911]) ).

cnf(c_8913,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(C),C))),inverse(multiply(B,inverse(A))))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8912]) ).

cnf(c_8914,plain,
    multiply(inverse(multiply(multiply(inverse(multiply(inverse(C),C)),inverse(A)),inverse(multiply(B,inverse(A))))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8913]) ).

cnf(c_8915,plain,
    multiply(inverse(multiply(multiply(multiply(inverse(C),inverse(inverse(C))),inverse(A)),inverse(multiply(B,inverse(A))))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8914]) ).

cnf(c_8916,plain,
    multiply(inverse(multiply(multiply(multiply(inverse(C),C),inverse(A)),inverse(multiply(B,inverse(A))))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8565,c_8915]) ).

cnf(c_8917,plain,
    multiply(inverse(multiply(inverse(A),inverse(multiply(B,inverse(A))))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8473,c_8916]) ).

cnf(c_8918,plain,
    multiply(inverse(multiply(inverse(A),multiply(inverse(inverse(A)),inverse(B)))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8917]) ).

cnf(c_8919,plain,
    multiply(inverse(multiply(inverse(A),multiply(A,inverse(B)))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8565,c_8918]) ).

cnf(c_8920,plain,
    multiply(multiply(inverse(multiply(A,inverse(B))),inverse(inverse(A))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8919]) ).

cnf(c_8921,plain,
    multiply(multiply(multiply(inverse(inverse(B)),inverse(A)),inverse(inverse(A))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8920]) ).

cnf(c_8922,plain,
    multiply(multiply(multiply(B,inverse(A)),inverse(inverse(A))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8565,c_8921]) ).

cnf(c_8923,plain,
    multiply(multiply(multiply(B,inverse(A)),A),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8565,c_8922]) ).

cnf(c_8924,plain,
    multiply(B,multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8595,c_8923]) ).

cnf(c_8925,plain,
    multiply(B,multiply(multiply(inverse(C),inverse(inverse(C))),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8924]) ).

cnf(c_8926,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8565,c_8925]) ).

cnf(c_8927,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(multiply(inverse(multiply(E,F)),inverse(D)),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8926]) ).

cnf(c_8928,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(multiply(multiply(inverse(F),inverse(E)),inverse(D)),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8927]) ).

cnf(c_8929,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(multiply(inverse(F),multiply(inverse(E),inverse(D))),multiply(D,multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8584,c_8928]) ).

cnf(c_8930,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(inverse(F),multiply(multiply(inverse(E),inverse(D)),multiply(D,multiply(E,F))))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8584,c_8929]) ).

cnf(c_8931,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(inverse(F),multiply(inverse(E),multiply(inverse(D),multiply(D,multiply(E,F)))))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8584,c_8930]) ).

cnf(c_8932,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(inverse(F),multiply(inverse(E),multiply(E,F)))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8587,c_8931]) ).

cnf(c_8933,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8587,c_8932]) ).

cnf(c_8934,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(multiply(inverse(F),inverse(inverse(F))),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8933]) ).

cnf(c_8935,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(multiply(inverse(F),F),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8565,c_8934]) ).

cnf(c_8936,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(inverse(F),F)))) = B,
    inference(paramod,[status(thm)],[c_8314,c_8935]) ).

cnf(c_8937,plain,
    multiply(B,multiply(multiply(inverse(C),C),multiply(inverse(F),inverse(inverse(F))))) = B,
    inference(paramod,[status(thm)],[c_8598,c_8936]) ).

cnf(c_8938,plain,
    multiply(B,multiply(multiply(inverse(C),C),multiply(inverse(F),F))) = B,
    inference(paramod,[status(thm)],[c_8565,c_8937]) ).

cnf(c_8601,plain,
    multiply(A,multiply(inverse(B),B)) = A,
    inference(paramod,[status(thm)],[c_8314,c_8938]) ).

cnf(c_8939,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(multiply(inverse(multiply(B,C)),inverse(A)),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_1381]) ).

cnf(c_8940,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(multiply(multiply(inverse(C),inverse(B)),inverse(A)),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8939]) ).

cnf(c_8941,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(multiply(inverse(C),multiply(inverse(B),inverse(A))),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8584,c_8940]) ).

cnf(c_8942,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(inverse(C),multiply(multiply(inverse(B),inverse(A)),inverse(D)))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8584,c_8941]) ).

cnf(c_8943,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(inverse(C),multiply(inverse(B),multiply(inverse(A),inverse(D))))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8584,c_8942]) ).

cnf(c_8944,plain,
    multiply(inverse(inverse(multiply(multiply(inverse(multiply(inverse(B),multiply(inverse(A),inverse(D)))),inverse(inverse(C))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8943]) ).

cnf(c_8945,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(inverse(multiply(inverse(A),inverse(D))),inverse(inverse(B))),inverse(inverse(C))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8944]) ).

cnf(c_8946,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(inverse(inverse(D)),inverse(inverse(A))),inverse(inverse(B))),inverse(inverse(C))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8945]) ).

cnf(c_8947,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,inverse(inverse(A))),inverse(inverse(B))),inverse(inverse(C))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8565,c_8946]) ).

cnf(c_8948,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),inverse(inverse(B))),inverse(inverse(C))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8565,c_8947]) ).

cnf(c_8949,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),inverse(inverse(C))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8565,c_8948]) ).

cnf(c_8950,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),C),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8565,c_8949]) ).

cnf(c_8951,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),C),multiply(inverse(multiply(multiply(inverse(F),inverse(E)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8950]) ).

cnf(c_8952,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),C),multiply(inverse(multiply(inverse(F),multiply(inverse(E),multiply(E,C)))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8584,c_8951]) ).

cnf(c_8953,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),C),multiply(inverse(multiply(inverse(F),C)),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8587,c_8952]) ).

cnf(c_8954,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),C),multiply(multiply(inverse(C),inverse(inverse(F))),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8953]) ).

cnf(c_8955,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),C),multiply(multiply(inverse(C),F),multiply(inverse(multiply(V6,F)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8565,c_8954]) ).

cnf(c_8956,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),C),multiply(multiply(inverse(C),F),multiply(multiply(inverse(F),inverse(V6)),multiply(V6,V7)))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8955]) ).

cnf(c_8957,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),C),multiply(multiply(inverse(C),F),multiply(inverse(F),multiply(inverse(V6),multiply(V6,V7))))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8584,c_8956]) ).

cnf(c_8958,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),C),multiply(multiply(inverse(C),F),multiply(inverse(F),V7))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8587,c_8957]) ).

cnf(c_8959,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(multiply(D,A),B),C),multiply(inverse(C),V7)))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8563,c_8958]) ).

cnf(c_8960,plain,
    multiply(inverse(inverse(multiply(multiply(multiply(D,A),B),V7))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8563,c_8959]) ).

cnf(c_8961,plain,
    multiply(inverse(multiply(inverse(V7),inverse(multiply(multiply(D,A),B)))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8960]) ).

cnf(c_8962,plain,
    multiply(inverse(multiply(inverse(V7),multiply(inverse(B),inverse(multiply(D,A))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8961]) ).

cnf(c_8963,plain,
    multiply(inverse(multiply(inverse(V7),multiply(inverse(B),multiply(inverse(A),inverse(D))))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8962]) ).

cnf(c_8964,plain,
    multiply(multiply(inverse(multiply(inverse(B),multiply(inverse(A),inverse(D)))),inverse(inverse(V7))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8963]) ).

cnf(c_8965,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(A),inverse(D))),inverse(inverse(B))),inverse(inverse(V7))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8964]) ).

cnf(c_8966,plain,
    multiply(multiply(multiply(multiply(inverse(inverse(D)),inverse(inverse(A))),inverse(inverse(B))),inverse(inverse(V7))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8965]) ).

cnf(c_8967,plain,
    multiply(multiply(multiply(multiply(D,inverse(inverse(A))),inverse(inverse(B))),inverse(inverse(V7))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8565,c_8966]) ).

cnf(c_8968,plain,
    multiply(multiply(multiply(multiply(D,A),inverse(inverse(B))),inverse(inverse(V7))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8565,c_8967]) ).

cnf(c_8969,plain,
    multiply(multiply(multiply(multiply(D,A),B),inverse(inverse(V7))),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8565,c_8968]) ).

cnf(c_8970,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(inverse(multiply(A,multiply(B,V7))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8565,c_8969]) ).

cnf(c_8971,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(multiply(B,V7)),inverse(A)),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8970]) ).

cnf(c_8972,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(multiply(inverse(V7),inverse(B)),inverse(A)),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8971]) ).

cnf(c_8973,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),inverse(multiply(inverse(multiply(A,multiply(B,V7))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8584,c_8972]) ).

cnf(c_8974,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),inverse(multiply(multiply(inverse(multiply(B,V7)),inverse(A)),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8973]) ).

cnf(c_8975,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),inverse(multiply(multiply(multiply(inverse(V7),inverse(B)),inverse(A)),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8974]) ).

cnf(c_8976,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),inverse(multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),multiply(A,multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8584,c_8975]) ).

cnf(c_8977,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),inverse(multiply(inverse(V7),multiply(multiply(inverse(B),inverse(A)),multiply(A,multiply(B,V7))))))) = D,
    inference(paramod,[status(thm)],[c_8584,c_8976]) ).

cnf(c_8978,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),inverse(multiply(inverse(V7),multiply(inverse(B),multiply(inverse(A),multiply(A,multiply(B,V7)))))))) = D,
    inference(paramod,[status(thm)],[c_8584,c_8977]) ).

cnf(c_8979,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),inverse(multiply(inverse(V7),multiply(inverse(B),multiply(B,V7)))))) = D,
    inference(paramod,[status(thm)],[c_8587,c_8978]) ).

cnf(c_8980,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),inverse(multiply(inverse(V7),V7)))) = D,
    inference(paramod,[status(thm)],[c_8587,c_8979]) ).

cnf(c_8981,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),multiply(inverse(V7),inverse(inverse(V7))))) = D,
    inference(paramod,[status(thm)],[c_8598,c_8980]) ).

cnf(c_8982,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(multiply(inverse(V7),multiply(inverse(B),inverse(A))),multiply(inverse(V7),V7))) = D,
    inference(paramod,[status(thm)],[c_8565,c_8981]) ).

cnf(c_8983,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(inverse(V7),multiply(inverse(B),inverse(A)))) = D,
    inference(paramod,[status(thm)],[c_8601,c_8982]) ).

cnf(c_8984,plain,
    multiply(multiply(multiply(D,A),B),multiply(inverse(B),inverse(A))) = D,
    inference(paramod,[status(thm)],[c_8563,c_8983]) ).

cnf(c_8610,plain,
    multiply(multiply(A,B),inverse(B)) = A,
    inference(paramod,[status(thm)],[c_8563,c_8984]) ).

cnf(c_8985,plain,
    multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(C),multiply(inverse(C),inverse(inverse(C)))))))),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(multiply(E,B)),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_729]) ).

cnf(c_8986,plain,
    multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(C),multiply(inverse(C),C)))))),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(multiply(E,B)),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_8985]) ).

cnf(c_8987,plain,
    multiply(inverse(multiply(A,inverse(multiply(B,inverse(C))))),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(multiply(E,B)),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8601,c_8986]) ).

cnf(c_8988,plain,
    multiply(inverse(multiply(A,multiply(inverse(inverse(C)),inverse(B)))),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(multiply(E,B)),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_8987]) ).

cnf(c_8989,plain,
    multiply(inverse(multiply(A,multiply(C,inverse(B)))),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(multiply(E,B)),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_8988]) ).

cnf(c_8990,plain,
    multiply(multiply(inverse(multiply(C,inverse(B))),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(multiply(E,B)),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_8989]) ).

cnf(c_8991,plain,
    multiply(multiply(multiply(inverse(inverse(B)),inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(multiply(E,B)),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_8990]) ).

cnf(c_8992,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(multiply(E,B)),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_8991]) ).

cnf(c_8993,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(multiply(inverse(B),inverse(E)),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_8992]) ).

cnf(c_8994,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(E),multiply(E,F))))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8584,c_8993]) ).

cnf(c_8995,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(inverse(multiply(inverse(B),F))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8587,c_8994]) ).

cnf(c_8996,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(multiply(inverse(F),inverse(inverse(B)))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_8995]) ).

cnf(c_8997,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(multiply(inverse(F),B)),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_8996]) ).

cnf(c_8998,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(multiply(inverse(B),inverse(inverse(F))),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_8997]) ).

cnf(c_8999,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(multiply(inverse(B),F),multiply(inverse(F),inverse(multiply(inverse(F),F)))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_8998]) ).

cnf(c_9000,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(multiply(inverse(B),F),multiply(inverse(F),multiply(inverse(F),inverse(inverse(F))))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_8999]) ).

cnf(c_9001,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(multiply(inverse(B),F),multiply(inverse(F),multiply(inverse(F),F))))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_9000]) ).

cnf(c_9002,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,multiply(multiply(inverse(B),F),inverse(F)))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8601,c_9001]) ).

cnf(c_9003,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8610,c_9002]) ).

cnf(c_9004,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(multiply(inverse(inverse(B)),inverse(D)),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_9003]) ).

cnf(c_9005,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(inverse(multiply(multiply(B,inverse(D)),multiply(D,V6)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_9004]) ).

cnf(c_9006,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(multiply(inverse(multiply(D,V6)),inverse(multiply(B,inverse(D))))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_9005]) ).

cnf(c_9007,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(multiply(multiply(inverse(V6),inverse(D)),inverse(multiply(B,inverse(D))))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_9006]) ).

cnf(c_9008,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(multiply(multiply(inverse(V6),inverse(D)),multiply(inverse(inverse(D)),inverse(B)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_9007]) ).

cnf(c_9009,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(multiply(multiply(inverse(V6),inverse(D)),multiply(D,inverse(B)))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_9008]) ).

cnf(c_9010,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(D),multiply(D,inverse(B))))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8584,c_9009]) ).

cnf(c_9011,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(inverse(multiply(inverse(V6),inverse(B))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8587,c_9010]) ).

cnf(c_9012,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(multiply(inverse(inverse(B)),inverse(inverse(V6))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8598,c_9011]) ).

cnf(c_9013,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(multiply(B,inverse(inverse(V6))),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_9012]) ).

cnf(c_9014,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(multiply(B,V6),multiply(inverse(V6),inverse(multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8565,c_9013]) ).

cnf(c_9015,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(multiply(B,V6),multiply(inverse(V6),multiply(inverse(V6),inverse(inverse(V6))))),
    inference(paramod,[status(thm)],[c_8598,c_9014]) ).

cnf(c_9016,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(multiply(B,V6),multiply(inverse(V6),multiply(inverse(V6),V6))),
    inference(paramod,[status(thm)],[c_8565,c_9015]) ).

cnf(c_9017,plain,
    multiply(multiply(multiply(B,inverse(C)),inverse(A)),multiply(A,C)) = multiply(multiply(B,V6),inverse(V6)),
    inference(paramod,[status(thm)],[c_8601,c_9016]) ).

cnf(c_8615,plain,
    multiply(multiply(multiply(A,inverse(B)),inverse(C)),multiply(C,B)) = A,
    inference(paramod,[status(thm)],[c_8610,c_9017]) ).

cnf(c_9018,plain,
    multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(C),inverse(inverse(C)))))))),multiply(inverse(D),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_5984]) ).

cnf(c_9019,plain,
    multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(C),C)))))),multiply(inverse(D),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9018]) ).

cnf(c_9020,plain,
    multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),inverse(C))))),multiply(inverse(D),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8601,c_9019]) ).

cnf(c_9021,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(inverse(C)),inverse(inverse(B))))),multiply(inverse(D),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9020]) ).

cnf(c_9022,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(C,inverse(inverse(B))))),multiply(inverse(D),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9021]) ).

cnf(c_9023,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(C,B))),multiply(inverse(D),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9022]) ).

cnf(c_9024,plain,
    multiply(inverse(multiply(multiply(inverse(multiply(C,B)),inverse(A)),multiply(inverse(D),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9023]) ).

cnf(c_9025,plain,
    multiply(inverse(multiply(multiply(multiply(inverse(B),inverse(C)),inverse(A)),multiply(inverse(D),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9024]) ).

cnf(c_9026,plain,
    multiply(inverse(multiply(multiply(inverse(B),multiply(inverse(C),inverse(A))),multiply(inverse(D),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8584,c_9025]) ).

cnf(c_9027,plain,
    multiply(inverse(multiply(multiply(inverse(B),multiply(inverse(C),inverse(A))),multiply(inverse(D),multiply(inverse(E),inverse(inverse(E)))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9026]) ).

cnf(c_9028,plain,
    multiply(inverse(multiply(multiply(inverse(B),multiply(inverse(C),inverse(A))),multiply(inverse(D),multiply(inverse(E),E)))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9027]) ).

cnf(c_9029,plain,
    multiply(inverse(multiply(multiply(inverse(B),multiply(inverse(C),inverse(A))),inverse(D))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8601,c_9028]) ).

cnf(c_9030,plain,
    multiply(inverse(multiply(inverse(B),multiply(multiply(inverse(C),inverse(A)),inverse(D)))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8584,c_9029]) ).

cnf(c_9031,plain,
    multiply(inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(A),inverse(D))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8584,c_9030]) ).

cnf(c_9032,plain,
    multiply(multiply(inverse(multiply(inverse(C),multiply(inverse(A),inverse(D)))),inverse(inverse(B))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9031]) ).

cnf(c_9033,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(A),inverse(D))),inverse(inverse(C))),inverse(inverse(B))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9032]) ).

cnf(c_9034,plain,
    multiply(multiply(multiply(multiply(inverse(inverse(D)),inverse(inverse(A))),inverse(inverse(C))),inverse(inverse(B))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9033]) ).

cnf(c_9035,plain,
    multiply(multiply(multiply(multiply(D,inverse(inverse(A))),inverse(inverse(C))),inverse(inverse(B))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9034]) ).

cnf(c_9036,plain,
    multiply(multiply(multiply(multiply(D,A),inverse(inverse(C))),inverse(inverse(B))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9035]) ).

cnf(c_9037,plain,
    multiply(multiply(multiply(multiply(D,A),C),inverse(inverse(B))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9036]) ).

cnf(c_9038,plain,
    multiply(multiply(multiply(multiply(D,A),C),B),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),inverse(multiply(inverse(V6),V6))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9037]) ).

cnf(c_9039,plain,
    multiply(multiply(multiply(multiply(D,A),C),B),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),multiply(inverse(V6),inverse(inverse(V6)))))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9038]) ).

cnf(c_9040,plain,
    multiply(multiply(multiply(multiply(D,A),C),B),inverse(multiply(inverse(multiply(F,inverse(multiply(B,multiply(inverse(V6),multiply(inverse(V6),V6)))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9039]) ).

cnf(c_9041,plain,
    multiply(multiply(multiply(multiply(D,A),C),B),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(V6))))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8601,c_9040]) ).

cnf(c_9042,plain,
    multiply(multiply(multiply(multiply(D,A),C),B),inverse(multiply(inverse(multiply(F,multiply(inverse(inverse(V6)),inverse(B)))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9041]) ).

cnf(c_9043,plain,
    multiply(multiply(multiply(multiply(D,A),C),B),inverse(multiply(inverse(multiply(F,multiply(V6,inverse(B)))),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9042]) ).

cnf(c_9044,plain,
    multiply(multiply(multiply(multiply(D,A),C),B),inverse(multiply(multiply(inverse(multiply(V6,inverse(B))),inverse(F)),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9043]) ).

cnf(c_9045,plain,
    multiply(multiply(multiply(multiply(D,A),C),B),inverse(multiply(multiply(multiply(inverse(inverse(B)),inverse(V6)),inverse(F)),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9044]) ).

cnf(c_9046,plain,
    multiply(multiply(multiply(multiply(D,A),C),B),inverse(multiply(multiply(multiply(B,inverse(V6)),inverse(F)),multiply(F,V6)))) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9045]) ).

cnf(c_9047,plain,
    multiply(multiply(multiply(multiply(D,A),C),B),inverse(B)) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8615,c_9046]) ).

cnf(c_9048,plain,
    multiply(multiply(D,A),C) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8610,c_9047]) ).

cnf(c_9049,plain,
    multiply(multiply(D,A),C) = multiply(D,multiply(inverse(multiply(inverse(V7),inverse(inverse(V7)))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9048]) ).

cnf(c_9050,plain,
    multiply(multiply(D,A),C) = multiply(D,multiply(inverse(multiply(inverse(V7),V7)),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9049]) ).

cnf(c_9051,plain,
    multiply(multiply(D,A),C) = multiply(D,multiply(multiply(inverse(V7),inverse(inverse(V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8598,c_9050]) ).

cnf(c_9052,plain,
    multiply(multiply(D,A),C) = multiply(D,multiply(multiply(inverse(V7),V7),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8565,c_9051]) ).

cnf(c_8622,plain,
    multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
    inference(paramod,[status(thm)],[c_8473,c_9052]) ).

cnf(c_8623,plain,
    $false,
    inference(resolve,[status(thm)],[c_8622,c_2]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP423-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04  % Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36  % Computer : n014.cluster.edu
% 0.10/0.36  % Model    : x86_64 x86_64
% 0.10/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36  % Memory   : 8046.5625MB
% 0.10/0.36  % OS       : Linux 6.8.0-71-generic
% 0.10/0.37  % CPULimit : 300
% 0.10/0.37  % WCLimit  : 300
% 0.10/0.37  % DateTime : Fri Sep 25 14:53:17 UTC 2026
% 0.10/0.37  % CPUTime  : 
% 0.10/0.37  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37  % Process 501448 was started by sandbox on n014,
% 0.10/0.37  % Fri Sep 25 14:53:17 2026
% 0.10/0.37  % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37  
% 0.10/0.37  % From the command line: assign(max_seconds, 300).
% 47.95/7.32  
% 47.95/7.32  % SZS status Unsatisfiable for theBenchmark
% 47.95/7.32  
% 47.95/7.32  % Proof 1 at 5.78 (+ 1.06) seconds.
% 47.95/7.32  % Length of proof is 160.
% 47.95/7.32  % Level of proof is 41.
% 47.95/7.32  % Maximum clause weight is 100.000.
% 47.95/7.32  % Given clauses 100.
% 47.95/7.32  
% 47.95/7.32  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------