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

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

% Computer : n026.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:26:42 AM UTC 2026

% Result   : Unsatisfiable 39.70s 5.47s
% Output   : CNFRefutation 39.70s
% 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,axiom,
    ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
    | multiply(multiply(inverse(b2),b2),a2) != a2
    | multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
    file('theBenchmark.p',prove_these_axioms) ).

cnf(c_2,plain,
    ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
    | multiply(multiply(inverse(b2),b2),a2) != a2
    | multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
    inference(clausify,[status(thm)],[prove_these_axioms]) ).

cnf(c_3,plain,
    ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
    | multiply(multiply(inverse(b2),b2),a2) != a2
    | multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ),
    inference(copy,[status(thm)],[c_2]) ).

cnf(c_8628,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_4,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_8628]) ).

cnf(c_8629,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_5,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_8629]) ).

cnf(c_7,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_4,c_1]) ).

cnf(c_8630,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_4,c_1]) ).

cnf(c_8,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_8630]) ).

cnf(c_9,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_4,c_1]) ).

cnf(c_12,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_5,c_1]) ).

cnf(c_14,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_5,c_1]) ).

cnf(c_15,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_5]) ).

cnf(c_16,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_5,c_4]) ).

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

cnf(c_8631,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_18,c_1]) ).

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

cnf(c_25,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_18,c_1]) ).

cnf(c_8632,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_18]) ).

cnf(c_26,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_8632]) ).

cnf(c_32,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_4,c_18]) ).

cnf(c_37,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_18,c_5]) ).

cnf(c_38,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_18,c_5]) ).

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

cnf(c_45,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_18,c_18]) ).

cnf(c_8633,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_21]) ).

cnf(c_47,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_8633]) ).

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

cnf(c_50,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_4,c_21]) ).

cnf(c_56,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_21,c_18]) ).

cnf(c_57,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_18,c_21]) ).

cnf(c_58,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_21,c_21]) ).

cnf(c_59,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_12]) ).

cnf(c_101,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_18,c_57]) ).

cnf(c_105,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_21,c_57]) ).

cnf(c_155,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_21,c_58]) ).

cnf(c_167,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_58,c_57]) ).

cnf(c_214,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_12,c_7]) ).

cnf(c_224,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_5,c_9]) ).

cnf(c_314,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_167,c_18]) ).

cnf(c_8634,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_14,c_21]) ).

cnf(c_490,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_8634]) ).

cnf(c_8635,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_14,c_58]) ).

cnf(c_495,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_490,c_8635]) ).

cnf(c_8636,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_14,c_56]) ).

cnf(c_498,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_490,c_8636]) ).

cnf(c_8637,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_495]) ).

cnf(c_500,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_8637]) ).

cnf(c_579,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_500,c_21]) ).

cnf(c_8638,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_498]) ).

cnf(c_615,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_8638]) ).

cnf(c_8639,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_16,c_224]) ).

cnf(c_730,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_8639]) ).

cnf(c_8640,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_18,c_25]) ).

cnf(c_755,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_25,c_8640]) ).

cnf(c_758,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_25,c_12]) ).

cnf(c_778,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_25,c_214]) ).

cnf(c_1076,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_101,c_314]) ).

cnf(c_1190,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_155,c_5]) ).

cnf(c_1376,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_9,c_105]) ).

cnf(c_1382,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_105,c_224]) ).

cnf(c_1833,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_26,c_12]) ).

cnf(c_1861,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,C)))) = inverse(multiply(inverse(D),D)),
    inference(paramod,[status(thm)],[c_9,c_26]) ).

cnf(c_1863,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_26,c_214]) ).

cnf(c_1873,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_26,c_45]) ).

cnf(c_8641,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_26,c_155]) ).

cnf(c_1927,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_8641]) ).

cnf(c_8642,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_9,c_1861]) ).

cnf(c_2084,plain,
    inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(B),B)),
    inference(paramod,[status(thm)],[c_9,c_8642]) ).

cnf(c_2093,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_1861,c_224]) ).

cnf(c_8643,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_1861,c_14]) ).

cnf(c_8644,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_1833,c_8643]) ).

cnf(c_2117,plain,
    multiply(inverse(A),A) = multiply(inverse(B),B),
    inference(paramod,[status(thm)],[c_9,c_8644]) ).

cnf(c_2232,plain,
    ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
    | multiply(multiply(inverse(b2),b2),a2) != a2 ),
    inference(resolve,[status(thm)],[c_2117,c_3]) ).

cnf(c_2254,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_2117,c_18]) ).

cnf(c_2255,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_2117,c_18]) ).

cnf(c_2257,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
    inference(paramod,[status(thm)],[c_2117,c_21]) ).

cnf(c_2258,plain,
    multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,A)),
    inference(paramod,[status(thm)],[c_2117,c_21]) ).

cnf(c_2261,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(B),B))))) = B,
    inference(paramod,[status(thm)],[c_2117,c_12]) ).

cnf(c_2289,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_2117,c_8]) ).

cnf(c_8645,plain,
    inverse(inverse(multiply(inverse(A),A))) = inverse(inverse(multiply(inverse(multiply(B,C)),multiply(B,C)))),
    inference(paramod,[status(thm)],[c_2117,c_214]) ).

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

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

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

cnf(c_8647,plain,
    inverse(multiply(A,multiply(inverse(B),B))) = inverse(multiply(A,multiply(inverse(multiply(C,D)),multiply(C,D)))),
    inference(paramod,[status(thm)],[c_2117,c_615]) ).

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

cnf(c_2354,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_2117,c_15]) ).

cnf(c_8648,plain,
    multiply(inverse(multiply(inverse(A),A)),B) = multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,D))),B),
    inference(paramod,[status(thm)],[c_2117,c_755]) ).

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

cnf(c_2424,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_2117,c_26]) ).

cnf(c_2426,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_2117,c_26]) ).

cnf(c_2456,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
    inference(paramod,[status(thm)],[c_2084,c_2117]) ).

cnf(c_2637,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_2084,c_2456]) ).

cnf(c_2792,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_2456,c_32]) ).

cnf(c_2876,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_2257,c_56]) ).

cnf(c_8649,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_2117,c_2257]) ).

cnf(c_2982,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_8649]) ).

cnf(c_3053,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_2258,c_45]) ).

cnf(c_3282,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))) = multiply(A,multiply(inverse(D),D)),
    inference(paramod,[status(thm)],[c_2117,c_2341]) ).

cnf(c_3283,plain,
    multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(inverse(C),C)),
    inference(paramod,[status(thm)],[c_2117,c_2341]) ).

cnf(c_3311,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_3283,c_45]) ).

cnf(c_3440,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_2117,c_2383]) ).

cnf(c_3581,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_3283,c_37]) ).

cnf(c_3600,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_2117,c_38]) ).

cnf(c_3601,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_2117,c_38]) ).

cnf(c_3619,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_2456,c_38]) ).

cnf(c_3649,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_3283,c_38]) ).

cnf(c_3713,plain,
    inverse(inverse(multiply(inverse(A),A))) = inverse(inverse(multiply(inverse(B),B))),
    inference(paramod,[status(thm)],[c_2117,c_2297]) ).

cnf(c_3751,plain,
    multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
    inference(paramod,[status(thm)],[c_3713,c_2117]) ).

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

cnf(c_4349,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_2982,c_314]) ).

cnf(c_4406,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_105,c_2982]) ).

cnf(c_4416,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_579,c_2982]) ).

cnf(c_4585,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_2117,c_2261]) ).

cnf(c_4615,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),B))) = inverse(multiply(inverse(C),C)),
    inference(paramod,[status(thm)],[c_3751,c_2261]) ).

cnf(c_4666,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_314,c_4585]) ).

cnf(c_4667,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_314,c_4585]) ).

cnf(c_4754,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_4615,c_45]) ).

cnf(c_8650,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_47,c_4585]) ).

cnf(c_5181,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_8650]) ).

cnf(c_8651,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_101,c_2254]) ).

cnf(c_5380,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_8651]) ).

cnf(c_5501,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_4615,c_2254]) ).

cnf(c_8652,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_101,c_2255]) ).

cnf(c_5552,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_8652]) ).

cnf(c_8653,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_155,c_2255]) ).

cnf(c_5555,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_8653]) ).

cnf(c_5610,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_3283,c_2255]) ).

cnf(c_5656,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_2255,c_4585]) ).

cnf(c_5718,plain,
    inverse(multiply(A,multiply(inverse(B),B))) = inverse(multiply(A,multiply(inverse(C),C))),
    inference(paramod,[status(thm)],[c_2117,c_2344]) ).

cnf(c_5831,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_5718,c_4585]) ).

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

cnf(c_5957,plain,
    multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_3751,c_50]) ).

cnf(c_5986,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_4585,c_50]) ).

cnf(c_6393,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_3282,c_45]) ).

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

cnf(c_7943,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_59,c_2258]) ).

cnf(c_7946,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_2258,c_59]) ).

cnf(c_7983,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_4585,c_59]) ).

cnf(c_8654,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_4615,c_59]) ).

cnf(c_7987,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_4585,c_8654]) ).

cnf(c_7993,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_4615,c_59]) ).

cnf(c_8012,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_2637,c_59]) ).

cnf(c_8655,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_3440,c_59]) ).

cnf(c_8016,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_4585,c_8655]) ).

cnf(c_8025,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_7987,c_7983]) ).

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

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

cnf(c_8657,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_8025,c_3649]) ).

cnf(c_8087,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_8657]) ).

cnf(c_8658,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_8025,c_3619]) ).

cnf(c_8115,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_8658]) ).

cnf(c_8659,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_8025,c_3601]) ).

cnf(c_8128,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_8659]) ).

cnf(c_8660,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_8025,c_3600]) ).

cnf(c_8129,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_8660]) ).

cnf(c_8661,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_8025,c_2354]) ).

cnf(c_8168,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_8661]) ).

cnf(c_8171,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_8025,c_1190]) ).

cnf(c_8186,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_8027,c_3581]) ).

cnf(c_8662,plain,
    multiply(inverse(F),multiply(D,C)) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
    inference(paramod,[status(thm)],[c_8087,c_3311]) ).

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

cnf(c_8663,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_8129,c_3053]) ).

cnf(c_8200,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_8197,c_8663]) ).

cnf(c_8664,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_8115,c_8016]) ).

cnf(c_8203,plain,
    multiply(inverse(inverse(multiply(inverse(A),A))),multiply(B,C)) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8197,c_8664]) ).

cnf(c_8240,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_8128,c_2876]) ).

cnf(c_8665,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_8240,c_5656]) ).

cnf(c_8251,plain,
    inverse(multiply(inverse(A),multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C)))) = A,
    inference(paramod,[status(thm)],[c_8203,c_8665]) ).

cnf(c_8666,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_8168,c_8012]) ).

cnf(c_8667,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_8251,c_8666]) ).

cnf(c_8291,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(B,C)) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8197,c_8667]) ).

cnf(c_8668,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_8168,c_7993]) ).

cnf(c_8669,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_8291,c_8668]) ).

cnf(c_8670,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_8203,c_8669]) ).

cnf(c_8297,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_8291,c_8670]) ).

cnf(c_8671,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_8168,c_7946]) ).

cnf(c_8672,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_8291,c_8671]) ).

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

cnf(c_8673,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_8168,c_7943]) ).

cnf(c_8674,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_8313,c_8673]) ).

cnf(c_8675,plain,
    multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(inverse(inverse(multiply(inverse(E),E))),multiply(A,B)),
    inference(paramod,[status(thm)],[c_8313,c_8674]) ).

cnf(c_8316,plain,
    multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(A,B),
    inference(paramod,[status(thm)],[c_8203,c_8675]) ).

cnf(c_8676,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_8313,c_2424]) ).

cnf(c_8347,plain,
    inverse(multiply(inverse(multiply(A,B)),C)) = multiply(inverse(C),multiply(A,B)),
    inference(paramod,[status(thm)],[c_8168,c_8676]) ).

cnf(c_8677,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_8313,c_1927]) ).

cnf(c_8678,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_8313,c_8677]) ).

cnf(c_8679,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_8313,c_8678]) ).

cnf(c_8680,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_8168,c_8679]) ).

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

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

cnf(c_8682,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_8313,c_1873]) ).

cnf(c_8683,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_8347,c_8682]) ).

cnf(c_8684,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_8347,c_8683]) ).

cnf(c_8685,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_8168,c_8684]) ).

cnf(c_8384,plain,
    multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(C),D)) = multiply(inverse(A),multiply(B,D)),
    inference(paramod,[status(thm)],[c_8200,c_8685]) ).

cnf(c_8686,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_8313,c_5552]) ).

cnf(c_8687,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_8347,c_8686]) ).

cnf(c_8688,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_8347,c_8687]) ).

cnf(c_8689,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_8384,c_8688]) ).

cnf(c_8690,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_8313,c_8689]) ).

cnf(c_8691,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_8347,c_8690]) ).

cnf(c_8413,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_8291,c_8691]) ).

cnf(c_8692,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_8313,c_5380]) ).

cnf(c_8693,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_8347,c_8692]) ).

cnf(c_8694,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_8347,c_8693]) ).

cnf(c_8695,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_8384,c_8694]) ).

cnf(c_8696,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_8313,c_8695]) ).

cnf(c_8697,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_8413,c_8696]) ).

cnf(c_8698,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_8347,c_8697]) ).

cnf(c_8699,plain,
    multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E)) = inverse(multiply(multiply(inverse(E),multiply(D,V6)),V7)),
    inference(paramod,[status(thm)],[c_8291,c_8698]) ).

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

cnf(c_8700,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_8313,c_1076]) ).

cnf(c_8701,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_8347,c_8700]) ).

cnf(c_8702,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_8347,c_8701]) ).

cnf(c_8703,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_8384,c_8702]) ).

cnf(c_8704,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_8313,c_8703]) ).

cnf(c_8705,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_8414,c_8704]) ).

cnf(c_8706,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_8347,c_8705]) ).

cnf(c_8707,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_8347,c_8706]) ).

cnf(c_8708,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_8384,c_8707]) ).

cnf(c_8709,plain,
    multiply(inverse(V7),E) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
    inference(paramod,[status(thm)],[c_8368,c_8708]) ).

cnf(c_8710,plain,
    multiply(inverse(V7),E) = inverse(multiply(inverse(multiply(V9,E)),multiply(V9,V7))),
    inference(paramod,[status(thm)],[c_8313,c_8709]) ).

cnf(c_8711,plain,
    multiply(inverse(V7),E) = inverse(multiply(inverse(E),V7)),
    inference(paramod,[status(thm)],[c_8313,c_8710]) ).

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

cnf(c_8712,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_8313,c_1863]) ).

cnf(c_8713,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_8423,c_8712]) ).

cnf(c_8714,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_8414,c_8713]) ).

cnf(c_8715,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_8423,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,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_8423,c_8715]) ).

cnf(c_8717,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_8423,c_8716]) ).

cnf(c_8718,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_8423,c_8717]) ).

cnf(c_8719,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_8423,c_8718]) ).

cnf(c_8720,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_8423,c_8719]) ).

cnf(c_8721,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_8313,c_8720]) ).

cnf(c_8722,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_8423,c_8721]) ).

cnf(c_8723,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_8414,c_8722]) ).

cnf(c_8724,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_8423,c_8723]) ).

cnf(c_8725,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_8423,c_8724]) ).

cnf(c_8448,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_8725]) ).

cnf(c_8726,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_8313,c_1376]) ).

cnf(c_8727,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_8423,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,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),C))),multiply(V6,V7)),
    inference(paramod,[status(thm)],[c_8313,c_8727]) ).

cnf(c_8729,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_8423,c_8728]) ).

cnf(c_8730,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_8423,c_8729]) ).

cnf(c_8731,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_8423,c_8730]) ).

cnf(c_8732,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_8423,c_8731]) ).

cnf(c_8733,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_8313,c_8732]) ).

cnf(c_8734,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_8423,c_8733]) ).

cnf(c_8735,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_8448,c_8734]) ).

cnf(c_8449,plain,
    multiply(multiply(inverse(A),B),multiply(inverse(B),multiply(C,D))) = multiply(inverse(A),multiply(C,D)),
    inference(paramod,[status(thm)],[c_8316,c_8735]) ).

cnf(c_8736,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_8423,c_778]) ).

cnf(c_8737,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_8313,c_8736]) ).

cnf(c_8738,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_8423,c_8737]) ).

cnf(c_8739,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_8423,c_8738]) ).

cnf(c_8740,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_8313,c_8739]) ).

cnf(c_8741,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_8423,c_8740]) ).

cnf(c_8461,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_8423,c_8741]) ).

cnf(c_8742,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_8423,c_758]) ).

cnf(c_8743,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_8313,c_8742]) ).

cnf(c_8744,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_8423,c_8743]) ).

cnf(c_8745,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_8423,c_8744]) ).

cnf(c_8746,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_8461,c_8745]) ).

cnf(c_8747,plain,
    inverse(multiply(multiply(inverse(multiply(C,A)),E),multiply(inverse(E),multiply(inverse(E),E)))) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8423,c_8746]) ).

cnf(c_8748,plain,
    inverse(multiply(inverse(multiply(C,A)),multiply(inverse(E),E))) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8449,c_8747]) ).

cnf(c_8749,plain,
    multiply(inverse(multiply(inverse(E),E)),multiply(C,A)) = multiply(C,A),
    inference(paramod,[status(thm)],[c_8423,c_8748]) ).

cnf(c_8462,plain,
    multiply(multiply(inverse(A),A),multiply(B,C)) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8423,c_8749]) ).

cnf(c_8750,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_8423,c_4667]) ).

cnf(c_8751,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_8423,c_8750]) ).

cnf(c_8752,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_8313,c_8751]) ).

cnf(c_8753,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_8313,c_8752]) ).

cnf(c_8754,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_8423,c_8753]) ).

cnf(c_8755,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_8313,c_8754]) ).

cnf(c_8756,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_8313,c_8755]) ).

cnf(c_8757,plain,
    inverse(multiply(inverse(B),inverse(multiply(multiply(inverse(F),E),multiply(inverse(E),F))))) = B,
    inference(paramod,[status(thm)],[c_8462,c_8756]) ).

cnf(c_8474,plain,
    multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(B),A)))),C) = C,
    inference(paramod,[status(thm)],[c_8423,c_8757]) ).

cnf(c_8758,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_8313,c_4666]) ).

cnf(c_8759,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_8313,c_8758]) ).

cnf(c_8760,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_8423,c_8759]) ).

cnf(c_8761,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_8313,c_8760]) ).

cnf(c_8762,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_8313,c_8761]) ).

cnf(c_8763,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_8423,c_8762]) ).

cnf(c_8764,plain,
    inverse(multiply(inverse(V6),multiply(inverse(V7),V7))) = V6,
    inference(paramod,[status(thm)],[c_8474,c_8763]) ).

cnf(c_8765,plain,
    multiply(inverse(multiply(inverse(V7),V7)),V6) = V6,
    inference(paramod,[status(thm)],[c_8423,c_8764]) ).

cnf(c_8475,plain,
    multiply(multiply(inverse(A),A),B) = B,
    inference(paramod,[status(thm)],[c_8423,c_8765]) ).

cnf(c_8766,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_8313,c_8171]) ).

cnf(c_8767,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_8423,c_8766]) ).

cnf(c_8768,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_8313,c_8767]) ).

cnf(c_8769,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_8384,c_8768]) ).

cnf(c_8770,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_8423,c_8769]) ).

cnf(c_8771,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_8423,c_8770]) ).

cnf(c_8495,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_8771]) ).

cnf(c_8772,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_8423,c_5555]) ).

cnf(c_8773,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_8313,c_8772]) ).

cnf(c_8774,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_8384,c_8773]) ).

cnf(c_8775,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_8423,c_8774]) ).

cnf(c_8776,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_8423,c_8775]) ).

cnf(c_8777,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_8495,c_8776]) ).

cnf(c_8778,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_8313,c_8777]) ).

cnf(c_8779,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_8423,c_8778]) ).

cnf(c_8780,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_8423,c_8779]) ).

cnf(c_8781,plain,
    multiply(inverse(V6),multiply(inverse(F),E)) = inverse(multiply(multiply(inverse(E),F),V6)),
    inference(paramod,[status(thm)],[c_8316,c_8780]) ).

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

cnf(c_8782,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_8423,c_8186]) ).

cnf(c_8783,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_8423,c_8782]) ).

cnf(c_8784,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_8316,c_8783]) ).

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

cnf(c_8786,plain,
    multiply(inverse(A),multiply(inverse(B),B)) = inverse(multiply(multiply(inverse(A),A),A)),
    inference(paramod,[status(thm)],[c_8423,c_8785]) ).

cnf(c_8533,plain,
    multiply(inverse(A),multiply(inverse(B),B)) = inverse(A),
    inference(paramod,[status(thm)],[c_8475,c_8786]) ).

cnf(c_8787,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(inverse(D),D)))) = multiply(B,C),
    inference(paramod,[status(thm)],[c_8423,c_8027]) ).

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

cnf(c_8539,plain,
    inverse(inverse(multiply(A,B))) = multiply(A,B),
    inference(paramod,[status(thm)],[c_8533,c_8788]) ).

cnf(c_8789,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_8313,c_6393]) ).

cnf(c_8790,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_8423,c_8789]) ).

cnf(c_8791,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_8423,c_8790]) ).

cnf(c_8792,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_8316,c_8791]) ).

cnf(c_8793,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_8533,c_8792]) ).

cnf(c_8794,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_8497,c_8793]) ).

cnf(c_8795,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_8539,c_8794]) ).

cnf(c_8796,plain,
    multiply(multiply(D,B),multiply(inverse(B),C)) = inverse(multiply(inverse(multiply(D,C)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_8313,c_8795]) ).

cnf(c_8797,plain,
    multiply(multiply(D,B),multiply(inverse(B),C)) = inverse(inverse(multiply(D,C))),
    inference(paramod,[status(thm)],[c_8533,c_8796]) ).

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

cnf(c_8798,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_8423,c_5831]) ).

cnf(c_8799,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_8423,c_8798]) ).

cnf(c_8800,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_8313,c_8799]) ).

cnf(c_8801,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_8423,c_8800]) ).

cnf(c_8802,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(inverse(D),D))))) = B,
    inference(paramod,[status(thm)],[c_8316,c_8801]) ).

cnf(c_8803,plain,
    inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),multiply(inverse(D),D)))) = B,
    inference(paramod,[status(thm)],[c_8423,c_8802]) ).

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

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

cnf(c_8805,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_8533,c_5610]) ).

cnf(c_8806,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_8567,c_8805]) ).

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

cnf(c_8808,plain,
    inverse(multiply(A,multiply(inverse(C),C))) = inverse(multiply(multiply(inverse(E),E),A)),
    inference(paramod,[status(thm)],[c_8423,c_8807]) ).

cnf(c_8569,plain,
    inverse(multiply(A,multiply(inverse(B),B))) = inverse(A),
    inference(paramod,[status(thm)],[c_8475,c_8808]) ).

cnf(c_8809,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_8423,c_5501]) ).

cnf(c_8810,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_8423,c_8809]) ).

cnf(c_8811,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_8423,c_8810]) ).

cnf(c_8812,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_8316,c_8811]) ).

cnf(c_8813,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_8423,c_8812]) ).

cnf(c_8814,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_8475,c_8813]) ).

cnf(c_8815,plain,
    inverse(D) = inverse(multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_8475,c_8814]) ).

cnf(c_8816,plain,
    inverse(D) = inverse(multiply(inverse(E),multiply(E,D))),
    inference(paramod,[status(thm)],[c_8569,c_8815]) ).

cnf(c_8817,plain,
    inverse(D) = multiply(inverse(multiply(E,D)),E),
    inference(paramod,[status(thm)],[c_8423,c_8816]) ).

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

cnf(c_8818,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_8423,c_4754]) ).

cnf(c_8819,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_8423,c_8818]) ).

cnf(c_8820,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_8423,c_8819]) ).

cnf(c_8821,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_8475,c_8820]) ).

cnf(c_8822,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_8475,c_8821]) ).

cnf(c_8823,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_8569,c_8822]) ).

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

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

cnf(c_8826,plain,
    multiply(multiply(inverse(F),D),C) = inverse(multiply(inverse(multiply(D,C)),F)),
    inference(paramod,[status(thm)],[c_8313,c_8825]) ).

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

cnf(c_8827,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_8313,c_4416]) ).

cnf(c_8828,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_8313,c_8827]) ).

cnf(c_8829,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_8423,c_8828]) ).

cnf(c_8830,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_8586,c_8829]) ).

cnf(c_8831,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_8423,c_8830]) ).

cnf(c_8832,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_8316,c_8831]) ).

cnf(c_8833,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_8423,c_8832]) ).

cnf(c_8834,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_8313,c_8833]) ).

cnf(c_8835,plain,
    multiply(inverse(multiply(C,E)),D) = multiply(multiply(inverse(V6),V6),multiply(inverse(E),multiply(inverse(C),D))),
    inference(paramod,[status(thm)],[c_8313,c_8834]) ).

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

cnf(c_8836,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_8588,c_4406]) ).

cnf(c_8837,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_8588,c_8836]) ).

cnf(c_8838,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_8423,c_8837]) ).

cnf(c_8839,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_8423,c_8838]) ).

cnf(c_8840,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_8423,c_8839]) ).

cnf(c_8841,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_8571,c_8840]) ).

cnf(c_8842,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_8571,c_8841]) ).

cnf(c_8843,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_8316,c_8842]) ).

cnf(c_8844,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_8423,c_8843]) ).

cnf(c_8845,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_8588,c_8844]) ).

cnf(c_8846,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_8423,c_8845]) ).

cnf(c_8847,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_8423,c_8846]) ).

cnf(c_8848,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_8571,c_8847]) ).

cnf(c_8849,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_8588,c_8848]) ).

cnf(c_8850,plain,
    multiply(inverse(D),C) = multiply(multiply(inverse(F),F),multiply(inverse(D),multiply(inverse(V8),multiply(V8,C)))),
    inference(paramod,[status(thm)],[c_8565,c_8849]) ).

cnf(c_8851,plain,
    multiply(inverse(D),C) = multiply(inverse(D),multiply(inverse(V8),multiply(V8,C))),
    inference(paramod,[status(thm)],[c_8475,c_8850]) ).

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

cnf(c_8852,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_8423,c_4349]) ).

cnf(c_8853,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_8586,c_8852]) ).

cnf(c_8854,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_8423,c_8853]) ).

cnf(c_8855,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_8588,c_8854]) ).

cnf(c_8856,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_8423,c_8855]) ).

cnf(c_8857,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_8586,c_8856]) ).

cnf(c_8858,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_8423,c_8857]) ).

cnf(c_8859,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_8475,c_8858]) ).

cnf(c_8860,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_8586,c_8859]) ).

cnf(c_8861,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_8423,c_8860]) ).

cnf(c_8862,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_8588,c_8861]) ).

cnf(c_8863,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_8423,c_8862]) ).

cnf(c_8864,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_8588,c_8863]) ).

cnf(c_8865,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_8423,c_8864]) ).

cnf(c_8866,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_8586,c_8865]) ).

cnf(c_8867,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_8565,c_8866]) ).

cnf(c_8868,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_8588,c_8867]) ).

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

cnf(c_8870,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_8588,c_8869]) ).

cnf(c_8871,plain,
    multiply(inverse(A),multiply(A,multiply(inverse(C),D))) = inverse(multiply(inverse(D),C)),
    inference(paramod,[status(thm)],[c_8589,c_8870]) ).

cnf(c_8590,plain,
    multiply(inverse(A),multiply(A,multiply(inverse(B),C))) = multiply(inverse(B),C),
    inference(paramod,[status(thm)],[c_8423,c_8871]) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(c_8883,plain,
    inverse(multiply(multiply(inverse(B),A),inverse(A))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(inverse(inverse(multiply(inverse(E),E))),inverse(multiply(inverse(F),F))))))),
    inference(paramod,[status(thm)],[c_8571,c_8882]) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(c_8895,plain,
    multiply(A,multiply(inverse(A),B)) = inverse(inverse(B)),
    inference(paramod,[status(thm)],[c_8533,c_8894]) ).

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

cnf(c_8896,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_8423,c_2792]) ).

cnf(c_8897,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_8533,c_8896]) ).

cnf(c_8898,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_8423,c_8897]) ).

cnf(c_8899,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_8567,c_8898]) ).

cnf(c_8900,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_8588,c_8899]) ).

cnf(c_8901,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_8589,c_8900]) ).

cnf(c_8902,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_8571,c_8901]) ).

cnf(c_8903,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_8533,c_8902]) ).

cnf(c_8904,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_8567,c_8903]) ).

cnf(c_8905,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_8423,c_8904]) ).

cnf(c_8906,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_8533,c_8905]) ).

cnf(c_8907,plain,
    B = inverse(multiply(inverse(multiply(E,multiply(multiply(B,inverse(F)),F))),multiply(E,multiply(inverse(V6),V6)))),
    inference(paramod,[status(thm)],[c_8567,c_8906]) ).

cnf(c_8908,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_8588,c_8907]) ).

cnf(c_8909,plain,
    B = inverse(multiply(inverse(multiply(multiply(B,inverse(F)),F)),multiply(inverse(V6),V6))),
    inference(paramod,[status(thm)],[c_8590,c_8908]) ).

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

cnf(c_8911,plain,
    B = multiply(multiply(B,inverse(F)),F),
    inference(paramod,[status(thm)],[c_8567,c_8910]) ).

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

cnf(c_8912,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_8423,c_2426]) ).

cnf(c_8913,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_8533,c_8912]) ).

cnf(c_8914,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_8423,c_8913]) ).

cnf(c_8915,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_8567,c_8914]) ).

cnf(c_8916,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_8571,c_8915]) ).

cnf(c_8917,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_8588,c_8916]) ).

cnf(c_8918,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_8567,c_8917]) ).

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

cnf(c_8599,plain,
    inverse(multiply(A,multiply(inverse(B),multiply(B,C)))) = inverse(multiply(A,C)),
    inference(paramod,[status(thm)],[c_8475,c_8919]) ).

cnf(c_8920,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_8423,c_2289]) ).

cnf(c_8921,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_8423,c_8920]) ).

cnf(c_8922,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_8423,c_8921]) ).

cnf(c_8923,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_8423,c_8922]) ).

cnf(c_8924,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_8423,c_8923]) ).

cnf(c_8925,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_8565,c_8924]) ).

cnf(c_8926,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_8423,c_8925]) ).

cnf(c_8927,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_8565,c_8926]) ).

cnf(c_8928,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_8569,c_8927]) ).

cnf(c_8929,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_8423,c_8928]) ).

cnf(c_8930,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_8423,c_8929]) ).

cnf(c_8931,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_8533,c_8930]) ).

cnf(c_8932,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_8423,c_8931]) ).

cnf(c_8933,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_8567,c_8932]) ).

cnf(c_8934,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_8571,c_8933]) ).

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

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

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

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

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

cnf(c_8939,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_8600,c_2093]) ).

cnf(c_8940,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_8567,c_8939]) ).

cnf(c_8941,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_8600,c_8940]) ).

cnf(c_8942,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_8600,c_8941]) ).

cnf(c_8943,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_8600,c_8942]) ).

cnf(c_8944,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_8567,c_8943]) ).

cnf(c_8945,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_8475,c_8944]) ).

cnf(c_8946,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_8600,c_8945]) ).

cnf(c_8947,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_8567,c_8946]) ).

cnf(c_8948,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_8600,c_8947]) ).

cnf(c_8949,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_8600,c_8948]) ).

cnf(c_8950,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_8567,c_8949]) ).

cnf(c_8951,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_8567,c_8950]) ).

cnf(c_8952,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_8597,c_8951]) ).

cnf(c_8953,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_8600,c_8952]) ).

cnf(c_8954,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_8567,c_8953]) ).

cnf(c_8955,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_8600,c_8954]) ).

cnf(c_8956,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_8600,c_8955]) ).

cnf(c_8957,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_8586,c_8956]) ).

cnf(c_8958,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_8586,c_8957]) ).

cnf(c_8959,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_8586,c_8958]) ).

cnf(c_8960,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_8589,c_8959]) ).

cnf(c_8961,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_8589,c_8960]) ).

cnf(c_8962,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_8600,c_8961]) ).

cnf(c_8963,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(multiply(inverse(F),F),multiply(inverse(C),C))))) = B,
    inference(paramod,[status(thm)],[c_8567,c_8962]) ).

cnf(c_8964,plain,
    multiply(B,multiply(multiply(inverse(C),C),inverse(multiply(inverse(F),F)))) = B,
    inference(paramod,[status(thm)],[c_8316,c_8963]) ).

cnf(c_8965,plain,
    multiply(B,multiply(multiply(inverse(C),C),multiply(inverse(F),inverse(inverse(F))))) = B,
    inference(paramod,[status(thm)],[c_8600,c_8964]) ).

cnf(c_8966,plain,
    multiply(B,multiply(multiply(inverse(C),C),multiply(inverse(F),F))) = B,
    inference(paramod,[status(thm)],[c_8567,c_8965]) ).

cnf(c_8603,plain,
    multiply(A,multiply(inverse(B),B)) = A,
    inference(paramod,[status(thm)],[c_8316,c_8966]) ).

cnf(c_8967,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_8600,c_1382]) ).

cnf(c_8968,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_8600,c_8967]) ).

cnf(c_8969,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_8586,c_8968]) ).

cnf(c_8970,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_8586,c_8969]) ).

cnf(c_8971,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_8586,c_8970]) ).

cnf(c_8972,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_8600,c_8971]) ).

cnf(c_8973,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_8600,c_8972]) ).

cnf(c_8974,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_8600,c_8973]) ).

cnf(c_8975,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_8567,c_8974]) ).

cnf(c_8976,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_8567,c_8975]) ).

cnf(c_8977,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_8567,c_8976]) ).

cnf(c_8978,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_8567,c_8977]) ).

cnf(c_8979,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_8600,c_8978]) ).

cnf(c_8980,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_8586,c_8979]) ).

cnf(c_8981,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_8589,c_8980]) ).

cnf(c_8982,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_8600,c_8981]) ).

cnf(c_8983,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_8567,c_8982]) ).

cnf(c_8984,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_8600,c_8983]) ).

cnf(c_8985,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_8586,c_8984]) ).

cnf(c_8986,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_8589,c_8985]) ).

cnf(c_8987,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_8565,c_8986]) ).

cnf(c_8988,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_8565,c_8987]) ).

cnf(c_8989,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_8600,c_8988]) ).

cnf(c_8990,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_8600,c_8989]) ).

cnf(c_8991,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_8600,c_8990]) ).

cnf(c_8992,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_8600,c_8991]) ).

cnf(c_8993,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_8600,c_8992]) ).

cnf(c_8994,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_8600,c_8993]) ).

cnf(c_8995,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_8567,c_8994]) ).

cnf(c_8996,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_8567,c_8995]) ).

cnf(c_8997,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_8567,c_8996]) ).

cnf(c_8998,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_8567,c_8997]) ).

cnf(c_8999,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_8600,c_8998]) ).

cnf(c_9000,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_8600,c_8999]) ).

cnf(c_9001,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_8586,c_9000]) ).

cnf(c_9002,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_8600,c_9001]) ).

cnf(c_9003,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_8600,c_9002]) ).

cnf(c_9004,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_8586,c_9003]) ).

cnf(c_9005,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_8586,c_9004]) ).

cnf(c_9006,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_8586,c_9005]) ).

cnf(c_9007,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_8589,c_9006]) ).

cnf(c_9008,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_8589,c_9007]) ).

cnf(c_9009,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_8600,c_9008]) ).

cnf(c_9010,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_8567,c_9009]) ).

cnf(c_9011,plain,
    multiply(multiply(multiply(multiply(D,A),B),V7),multiply(inverse(V7),multiply(inverse(B),inverse(A)))) = D,
    inference(paramod,[status(thm)],[c_8603,c_9010]) ).

cnf(c_9012,plain,
    multiply(multiply(multiply(D,A),B),multiply(inverse(B),inverse(A))) = D,
    inference(paramod,[status(thm)],[c_8565,c_9011]) ).

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

cnf(c_9013,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_8600,c_730]) ).

cnf(c_9014,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_8567,c_9013]) ).

cnf(c_9015,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_8603,c_9014]) ).

cnf(c_9016,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_8600,c_9015]) ).

cnf(c_9017,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_8567,c_9016]) ).

cnf(c_9018,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_8600,c_9017]) ).

cnf(c_9019,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_8600,c_9018]) ).

cnf(c_9020,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_8567,c_9019]) ).

cnf(c_9021,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_8600,c_9020]) ).

cnf(c_9022,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_8586,c_9021]) ).

cnf(c_9023,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_8589,c_9022]) ).

cnf(c_9024,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_8600,c_9023]) ).

cnf(c_9025,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_8567,c_9024]) ).

cnf(c_9026,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_8600,c_9025]) ).

cnf(c_9027,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_8567,c_9026]) ).

cnf(c_9028,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_8600,c_9027]) ).

cnf(c_9029,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_8567,c_9028]) ).

cnf(c_9030,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_8603,c_9029]) ).

cnf(c_9031,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_8612,c_9030]) ).

cnf(c_9032,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_8600,c_9031]) ).

cnf(c_9033,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_8567,c_9032]) ).

cnf(c_9034,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_8600,c_9033]) ).

cnf(c_9035,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_8600,c_9034]) ).

cnf(c_9036,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_8600,c_9035]) ).

cnf(c_9037,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_8567,c_9036]) ).

cnf(c_9038,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_8586,c_9037]) ).

cnf(c_9039,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_8589,c_9038]) ).

cnf(c_9040,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_8600,c_9039]) ).

cnf(c_9041,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_8567,c_9040]) ).

cnf(c_9042,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_8567,c_9041]) ).

cnf(c_9043,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_8600,c_9042]) ).

cnf(c_9044,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_8567,c_9043]) ).

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

cnf(c_8617,plain,
    multiply(multiply(multiply(A,inverse(B)),inverse(C)),multiply(C,B)) = A,
    inference(paramod,[status(thm)],[c_8612,c_9045]) ).

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

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

cnf(c_9048,plain,
    multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(D,multiply(inverse(inverse(multiply(inverse(E),E))),multiply(inverse(D),inverse(multiply(inverse(F),F)))))),
    inference(paramod,[status(thm)],[c_8603,c_9047]) ).

cnf(c_9049,plain,
    A = multiply(A,multiply(D,multiply(inverse(inverse(multiply(inverse(E),E))),multiply(inverse(D),inverse(multiply(inverse(F),F)))))),
    inference(paramod,[status(thm)],[c_8603,c_9048]) ).

cnf(c_9050,plain,
    A = multiply(A,multiply(D,multiply(inverse(multiply(inverse(E),inverse(inverse(E)))),multiply(inverse(D),inverse(multiply(inverse(F),F)))))),
    inference(paramod,[status(thm)],[c_8600,c_9049]) ).

cnf(c_9051,plain,
    A = multiply(A,multiply(D,multiply(inverse(multiply(inverse(E),E)),multiply(inverse(D),inverse(multiply(inverse(F),F)))))),
    inference(paramod,[status(thm)],[c_8567,c_9050]) ).

cnf(c_9052,plain,
    A = multiply(A,multiply(D,multiply(multiply(inverse(E),inverse(inverse(E))),multiply(inverse(D),inverse(multiply(inverse(F),F)))))),
    inference(paramod,[status(thm)],[c_8600,c_9051]) ).

cnf(c_9053,plain,
    A = multiply(A,multiply(D,multiply(multiply(inverse(E),E),multiply(inverse(D),inverse(multiply(inverse(F),F)))))),
    inference(paramod,[status(thm)],[c_8567,c_9052]) ).

cnf(c_9054,plain,
    A = multiply(A,multiply(D,multiply(multiply(inverse(E),E),multiply(inverse(D),multiply(inverse(F),inverse(inverse(F))))))),
    inference(paramod,[status(thm)],[c_8600,c_9053]) ).

cnf(c_9055,plain,
    A = multiply(A,multiply(D,multiply(multiply(inverse(E),E),multiply(inverse(D),multiply(inverse(F),F))))),
    inference(paramod,[status(thm)],[c_8567,c_9054]) ).

cnf(c_9056,plain,
    A = multiply(A,multiply(D,multiply(multiply(inverse(E),E),inverse(D)))),
    inference(paramod,[status(thm)],[c_8603,c_9055]) ).

cnf(c_9057,plain,
    A = multiply(A,multiply(D,inverse(D))),
    inference(paramod,[status(thm)],[c_8475,c_9056]) ).

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

cnf(c_9058,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_8600,c_5986]) ).

cnf(c_9059,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_8567,c_9058]) ).

cnf(c_9060,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_8603,c_9059]) ).

cnf(c_9061,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_8600,c_9060]) ).

cnf(c_9062,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_8567,c_9061]) ).

cnf(c_9063,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_8567,c_9062]) ).

cnf(c_9064,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_8600,c_9063]) ).

cnf(c_9065,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_8600,c_9064]) ).

cnf(c_9066,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_8586,c_9065]) ).

cnf(c_9067,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_8600,c_9066]) ).

cnf(c_9068,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_8567,c_9067]) ).

cnf(c_9069,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_8603,c_9068]) ).

cnf(c_9070,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_8586,c_9069]) ).

cnf(c_9071,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_8586,c_9070]) ).

cnf(c_9072,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_8600,c_9071]) ).

cnf(c_9073,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_8600,c_9072]) ).

cnf(c_9074,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_8600,c_9073]) ).

cnf(c_9075,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_8567,c_9074]) ).

cnf(c_9076,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_8567,c_9075]) ).

cnf(c_9077,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_8567,c_9076]) ).

cnf(c_9078,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_8567,c_9077]) ).

cnf(c_9079,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_8600,c_9078]) ).

cnf(c_9080,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_8567,c_9079]) ).

cnf(c_9081,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_8603,c_9080]) ).

cnf(c_9082,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_8600,c_9081]) ).

cnf(c_9083,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_8567,c_9082]) ).

cnf(c_9084,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_8600,c_9083]) ).

cnf(c_9085,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_8600,c_9084]) ).

cnf(c_9086,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_8567,c_9085]) ).

cnf(c_9087,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_8617,c_9086]) ).

cnf(c_9088,plain,
    multiply(multiply(D,A),C) = multiply(D,multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8612,c_9087]) ).

cnf(c_9089,plain,
    multiply(multiply(D,A),C) = multiply(D,multiply(inverse(multiply(inverse(V7),inverse(inverse(V7)))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9088]) ).

cnf(c_9090,plain,
    multiply(multiply(D,A),C) = multiply(D,multiply(inverse(multiply(inverse(V7),V7)),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9089]) ).

cnf(c_9091,plain,
    multiply(multiply(D,A),C) = multiply(D,multiply(multiply(inverse(V7),inverse(inverse(V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9090]) ).

cnf(c_9092,plain,
    multiply(multiply(D,A),C) = multiply(D,multiply(multiply(inverse(V7),V7),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9091]) ).

cnf(c_8624,plain,
    multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
    inference(paramod,[status(thm)],[c_8475,c_9092]) ).

cnf(c_9093,plain,
    multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(C),inverse(inverse(C)))))))),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_5957]) ).

cnf(c_9094,plain,
    multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(C),C)))))),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9093]) ).

cnf(c_9095,plain,
    multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),inverse(C))))),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8603,c_9094]) ).

cnf(c_9096,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(inverse(C)),inverse(inverse(B))))),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9095]) ).

cnf(c_9097,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(C,inverse(inverse(B))))),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9096]) ).

cnf(c_9098,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(C,B))),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9097]) ).

cnf(c_9099,plain,
    multiply(inverse(multiply(multiply(inverse(multiply(C,B)),inverse(A)),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9098]) ).

cnf(c_9100,plain,
    multiply(inverse(multiply(multiply(multiply(inverse(B),inverse(C)),inverse(A)),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9099]) ).

cnf(c_9101,plain,
    multiply(inverse(multiply(multiply(inverse(B),multiply(inverse(C),inverse(A))),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8624,c_9100]) ).

cnf(c_9102,plain,
    multiply(inverse(multiply(multiply(inverse(B),multiply(inverse(C),inverse(A))),multiply(inverse(D),inverse(inverse(D))))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9101]) ).

cnf(c_9103,plain,
    multiply(inverse(multiply(multiply(inverse(B),multiply(inverse(C),inverse(A))),multiply(inverse(D),D))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9102]) ).

cnf(c_9104,plain,
    multiply(inverse(multiply(inverse(B),multiply(inverse(C),inverse(A)))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8603,c_9103]) ).

cnf(c_9105,plain,
    multiply(multiply(inverse(multiply(inverse(C),inverse(A))),inverse(inverse(B))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9104]) ).

cnf(c_9106,plain,
    multiply(multiply(multiply(inverse(inverse(A)),inverse(inverse(C))),inverse(inverse(B))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9105]) ).

cnf(c_9107,plain,
    multiply(multiply(multiply(A,inverse(inverse(C))),inverse(inverse(B))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9106]) ).

cnf(c_9108,plain,
    multiply(multiply(multiply(A,C),inverse(inverse(B))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9107]) ).

cnf(c_9109,plain,
    multiply(multiply(multiply(A,C),B),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9108]) ).

cnf(c_9110,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8624,c_9109]) ).

cnf(c_9111,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),multiply(inverse(F),inverse(inverse(F)))))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9110]) ).

cnf(c_9112,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(inverse(multiply(E,inverse(multiply(B,multiply(inverse(F),multiply(inverse(F),F)))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9111]) ).

cnf(c_9113,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(inverse(multiply(E,inverse(multiply(B,inverse(F))))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8603,c_9112]) ).

cnf(c_9114,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(inverse(multiply(E,multiply(inverse(inverse(F)),inverse(B)))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9113]) ).

cnf(c_9115,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(inverse(multiply(E,multiply(F,inverse(B)))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9114]) ).

cnf(c_9116,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(multiply(inverse(multiply(F,inverse(B))),inverse(E)),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9115]) ).

cnf(c_9117,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(multiply(multiply(inverse(inverse(B)),inverse(F)),inverse(E)),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9116]) ).

cnf(c_9118,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(multiply(multiply(B,inverse(F)),inverse(E)),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9117]) ).

cnf(c_9119,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(multiply(B,multiply(inverse(F),inverse(E))),multiply(E,F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8624,c_9118]) ).

cnf(c_9120,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(B,multiply(multiply(inverse(F),inverse(E)),multiply(E,F))))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8624,c_9119]) ).

cnf(c_9121,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(B,multiply(inverse(F),multiply(inverse(E),multiply(E,F)))))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8624,c_9120]) ).

cnf(c_9122,plain,
    multiply(multiply(A,multiply(C,B)),inverse(multiply(B,multiply(inverse(F),F)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8589,c_9121]) ).

cnf(c_9123,plain,
    multiply(multiply(A,multiply(C,B)),inverse(B)) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8603,c_9122]) ).

cnf(c_9124,plain,
    multiply(A,multiply(multiply(C,B),inverse(B))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8624,c_9123]) ).

cnf(c_9125,plain,
    multiply(A,multiply(C,multiply(B,inverse(B)))) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8624,c_9124]) ).

cnf(c_9126,plain,
    multiply(A,C) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8622,c_9125]) ).

cnf(c_9127,plain,
    multiply(A,C) = multiply(multiply(inverse(V6),inverse(inverse(V6))),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9126]) ).

cnf(c_9128,plain,
    multiply(A,C) = multiply(multiply(inverse(V6),V6),multiply(inverse(inverse(multiply(inverse(V7),V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9127]) ).

cnf(c_9129,plain,
    multiply(A,C) = multiply(multiply(inverse(V6),V6),multiply(inverse(multiply(inverse(V7),inverse(inverse(V7)))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9128]) ).

cnf(c_9130,plain,
    multiply(A,C) = multiply(multiply(inverse(V6),V6),multiply(inverse(multiply(inverse(V7),V7)),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9129]) ).

cnf(c_9131,plain,
    multiply(A,C) = multiply(multiply(inverse(V6),V6),multiply(multiply(inverse(V7),inverse(inverse(V7))),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8600,c_9130]) ).

cnf(c_9132,plain,
    multiply(A,C) = multiply(multiply(inverse(V6),V6),multiply(multiply(inverse(V7),V7),multiply(A,C))),
    inference(paramod,[status(thm)],[c_8567,c_9131]) ).

cnf(c_9133,plain,
    multiply(A,C) = multiply(multiply(inverse(V6),V6),multiply(inverse(V7),multiply(V7,multiply(A,C)))),
    inference(paramod,[status(thm)],[c_8624,c_9132]) ).

cnf(c_9134,plain,
    multiply(A,C) = multiply(inverse(V6),multiply(V6,multiply(inverse(V7),multiply(V7,multiply(A,C))))),
    inference(paramod,[status(thm)],[c_8624,c_9133]) ).

cnf(c_9135,plain,
    multiply(A,C) = multiply(inverse(V7),multiply(V7,multiply(A,C))),
    inference(paramod,[status(thm)],[c_8590,c_9134]) ).

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

cnf(c_9136,plain,
    multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),inverse(inverse(B)))),multiply(inverse(C),C))))),multiply(A,D)) = inverse(multiply(inverse(multiply(inverse(multiply(E,F)),inverse(multiply(multiply(inverse(D),inverse(multiply(inverse(D),D))),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_5884]) ).

cnf(c_9137,plain,
    multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))))),multiply(A,D)) = inverse(multiply(inverse(multiply(inverse(multiply(E,F)),inverse(multiply(multiply(inverse(D),inverse(multiply(inverse(D),D))),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8567,c_9136]) ).

cnf(c_9138,plain,
    multiply(inverse(multiply(A,inverse(multiply(multiply(inverse(B),inverse(inverse(B))),multiply(inverse(C),C))))),multiply(A,D)) = inverse(multiply(inverse(multiply(inverse(multiply(E,F)),inverse(multiply(multiply(inverse(D),inverse(multiply(inverse(D),D))),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9137]) ).

cnf(c_9139,plain,
    multiply(inverse(multiply(A,inverse(multiply(multiply(inverse(B),B),multiply(inverse(C),C))))),multiply(A,D)) = inverse(multiply(inverse(multiply(inverse(multiply(E,F)),inverse(multiply(multiply(inverse(D),inverse(multiply(inverse(D),D))),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8567,c_9138]) ).

cnf(c_9140,plain,
    multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,D)) = inverse(multiply(inverse(multiply(inverse(multiply(E,F)),inverse(multiply(multiply(inverse(D),inverse(multiply(inverse(D),D))),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8603,c_9139]) ).

cnf(c_9141,plain,
    multiply(inverse(multiply(A,multiply(inverse(B),inverse(inverse(B))))),multiply(A,D)) = inverse(multiply(inverse(multiply(inverse(multiply(E,F)),inverse(multiply(multiply(inverse(D),inverse(multiply(inverse(D),D))),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9140]) ).

cnf(c_9142,plain,
    multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,D)) = inverse(multiply(inverse(multiply(inverse(multiply(E,F)),inverse(multiply(multiply(inverse(D),inverse(multiply(inverse(D),D))),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8567,c_9141]) ).

cnf(c_9143,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(inverse(multiply(E,F)),inverse(multiply(multiply(inverse(D),inverse(multiply(inverse(D),D))),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8603,c_9142]) ).

cnf(c_9144,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(multiply(inverse(D),inverse(multiply(inverse(D),D))),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9143]) ).

cnf(c_9145,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(multiply(inverse(D),multiply(inverse(D),inverse(inverse(D)))),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9144]) ).

cnf(c_9146,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(multiply(inverse(D),multiply(inverse(D),D)),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8567,c_9145]) ).

cnf(c_9147,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(inverse(D),multiply(inverse(multiply(E,V6)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8603,c_9146]) ).

cnf(c_9148,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(inverse(D),multiply(multiply(inverse(V6),inverse(E)),inverse(multiply(inverse(multiply(E,V6)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9147]) ).

cnf(c_9149,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(inverse(D),multiply(multiply(inverse(V6),inverse(E)),inverse(multiply(multiply(inverse(V6),inverse(E)),multiply(E,V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9148]) ).

cnf(c_9150,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(inverse(D),multiply(multiply(inverse(V6),inverse(E)),inverse(multiply(inverse(V6),multiply(inverse(E),multiply(E,V6))))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8624,c_9149]) ).

cnf(c_9151,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(inverse(D),multiply(multiply(inverse(V6),inverse(E)),inverse(multiply(inverse(V6),V6))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8589,c_9150]) ).

cnf(c_9152,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(inverse(D),multiply(multiply(inverse(V6),inverse(E)),multiply(inverse(V6),inverse(inverse(V6)))))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9151]) ).

cnf(c_9153,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(inverse(D),multiply(multiply(inverse(V6),inverse(E)),multiply(inverse(V6),V6)))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8567,c_9152]) ).

cnf(c_9154,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),inverse(multiply(inverse(D),multiply(inverse(V6),inverse(E)))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8603,c_9153]) ).

cnf(c_9155,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),multiply(inverse(multiply(inverse(V6),inverse(E))),inverse(inverse(D))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9154]) ).

cnf(c_9156,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),multiply(multiply(inverse(inverse(E)),inverse(inverse(V6))),inverse(inverse(D))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9155]) ).

cnf(c_9157,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),multiply(multiply(E,inverse(inverse(V6))),inverse(inverse(D))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8567,c_9156]) ).

cnf(c_9158,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),multiply(multiply(E,V6),inverse(inverse(D))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8567,c_9157]) ).

cnf(c_9159,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),multiply(multiply(E,V6),D))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8567,c_9158]) ).

cnf(c_9160,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(E)),multiply(E,multiply(V6,D)))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8624,c_9159]) ).

cnf(c_9161,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(inverse(F),multiply(inverse(E),multiply(E,multiply(V6,D))))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8624,c_9160]) ).

cnf(c_9162,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(multiply(inverse(F),multiply(V6,D))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8625,c_9161]) ).

cnf(c_9163,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(multiply(inverse(multiply(V6,D)),inverse(inverse(F))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9162]) ).

cnf(c_9164,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(multiply(multiply(inverse(D),inverse(V6)),inverse(inverse(F))),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9163]) ).

cnf(c_9165,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(multiply(multiply(inverse(D),inverse(V6)),F),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8567,c_9164]) ).

cnf(c_9166,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(multiply(inverse(D),multiply(inverse(V6),F)),multiply(inverse(multiply(V7,F)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8624,c_9165]) ).

cnf(c_9167,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(multiply(inverse(D),multiply(inverse(V6),F)),multiply(multiply(inverse(F),inverse(V7)),multiply(V7,V6)))),
    inference(paramod,[status(thm)],[c_8600,c_9166]) ).

cnf(c_9168,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(multiply(inverse(D),multiply(inverse(V6),F)),multiply(inverse(F),multiply(inverse(V7),multiply(V7,V6))))),
    inference(paramod,[status(thm)],[c_8624,c_9167]) ).

cnf(c_9169,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(multiply(inverse(D),multiply(inverse(V6),F)),multiply(inverse(F),V6))),
    inference(paramod,[status(thm)],[c_8589,c_9168]) ).

cnf(c_9170,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(D),multiply(multiply(inverse(V6),F),multiply(inverse(F),V6)))),
    inference(paramod,[status(thm)],[c_8624,c_9169]) ).

cnf(c_9171,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(D),multiply(inverse(V6),multiply(F,multiply(inverse(F),V6))))),
    inference(paramod,[status(thm)],[c_8624,c_9170]) ).

cnf(c_9172,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(multiply(inverse(D),multiply(inverse(V6),V6))),
    inference(paramod,[status(thm)],[c_8595,c_9171]) ).

cnf(c_9173,plain,
    multiply(inverse(A),multiply(A,D)) = inverse(inverse(D)),
    inference(paramod,[status(thm)],[c_8603,c_9172]) ).

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

cnf(c_9174,plain,
    ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
    | multiply(inverse(b2),multiply(b2,a2)) != a2 ),
    inference(paramod,[status(thm)],[c_8624,c_2232]) ).

cnf(c_9175,plain,
    ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
    | a2 != a2 ),
    inference(paramod,[status(thm)],[c_8626,c_9174]) ).

cnf(c_9176,plain,
    ( multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3))
    | a2 != a2 ),
    inference(paramod,[status(thm)],[c_8624,c_9175]) ).

cnf(c_9177,plain,
    multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
    inference(copy,[status(thm)],[c_9176]) ).

cnf(c_8627,plain,
    $false,
    inference(copy,[status(thm)],[c_9177]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP055-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04  % Command  : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36  % Computer : n026.cluster.edu
% 0.08/0.36  % Model    : x86_64 x86_64
% 0.08/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36  % Memory   : 8046.5625MB
% 0.08/0.36  % OS       : Linux 6.8.0-71-generic
% 0.08/0.36  % CPULimit : 300
% 0.08/0.36  % WCLimit  : 300
% 0.08/0.36  % DateTime : Fri Sep 25 14:22:40 UTC 2026
% 0.08/0.37  % CPUTime  : 
% 0.08/0.37  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37  % Process 2721382 was started by sandbox2 on n026,
% 0.08/0.37  % Fri Sep 25 14:22:40 2026
% 0.08/0.37  % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.38  
% 0.08/0.38  % From the command line: assign(max_seconds, 300).
% 39.70/5.47  
% 39.70/5.47  % SZS status Unsatisfiable for theBenchmark
% 39.70/5.47  
% 39.70/5.47  % Proof 1 at 4.20 (+ 0.74) seconds.
% 39.70/5.47  % Length of proof is 172.
% 39.70/5.47  % Level of proof is 43.
% 39.70/5.47  % Maximum clause weight is 100.000.
% 39.70/5.47  % Given clauses 101.
% 39.70/5.47  
% 39.70/5.47  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------