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

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

% Computer : n004.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Sun Sep 27 07:29:33 AM UTC 2026

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

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

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

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

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

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

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

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

cnf(c_13,plain,
    inverse(multiply(A,multiply(multiply(B,multiply(multiply(C,multiply(D,multiply(multiply(inverse(D),multiply(multiply(inverse(C),E),inverse(multiply(F,multiply(V6,E))))),F))),multiply(multiply(V6,V7),inverse(multiply(V8,multiply(B,V7)))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(A,V9))))))) = V10,
    inference(paramod,[status(thm)],[c_4,c_3]) ).

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

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

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

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

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

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

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

cnf(c_7751,plain,
    inverse(multiply(inverse(A),multiply(A,multiply(B,inverse(multiply(C,inverse(multiply(D,multiply(E,multiply(multiply(inverse(E),multiply(multiply(inverse(D),multiply(multiply(inverse(B),F),inverse(multiply(V6,multiply(V7,F))))),V6)),V7)))))))))) = C,
    inference(paramod,[status(thm)],[c_18,c_150]) ).

cnf(c_345,plain,
    inverse(multiply(inverse(A),multiply(A,multiply(B,inverse(multiply(C,B)))))) = C,
    inference(paramod,[status(thm)],[c_12,c_7751]) ).

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

cnf(c_421,plain,
    multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(C,inverse(multiply(D,C)))),D))) = A,
    inference(paramod,[status(thm)],[c_12,c_7752]) ).

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

cnf(c_439,plain,
    inverse(multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(C,A)))))) = C,
    inference(paramod,[status(thm)],[c_421,c_7753]) ).

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

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

cnf(c_512,plain,
    multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(inverse(A),inverse(multiply(C,inverse(D))))),C))) = D,
    inference(paramod,[status(thm)],[c_439,c_143]) ).

cnf(c_528,plain,
    inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(multiply(C,D)))),C)))) = D,
    inference(paramod,[status(thm)],[c_439,c_345]) ).

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

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

cnf(c_585,plain,
    multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(inverse(C),A))))) = C,
    inference(paramod,[status(thm)],[c_421,c_7754]) ).

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

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

cnf(c_678,plain,
    multiply(multiply(A,multiply(B,inverse(multiply(C,B)))),multiply(D,multiply(inverse(D),C))) = A,
    inference(paramod,[status(thm)],[c_345,c_585]) ).

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

cnf(c_681,plain,
    multiply(multiply(A,multiply(inverse(A),inverse(multiply(B,inverse(C))))),multiply(D,multiply(inverse(D),B))) = C,
    inference(paramod,[status(thm)],[c_439,c_585]) ).

cnf(c_802,plain,
    multiply(multiply(A,multiply(B,inverse(multiply(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C))),B)))),D) = A,
    inference(paramod,[status(thm)],[c_585,c_678]) ).

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

cnf(c_7757,plain,
    C = multiply(inverse(V6),multiply(V6,multiply(multiply(C,multiply(V7,inverse(multiply(V8,V7)))),V8))),
    inference(paramod,[status(thm)],[c_12,c_7756]) ).

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

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

cnf(c_1428,plain,
    inverse(multiply(multiply(A,multiply(inverse(A),inverse(multiply(multiply(inverse(inverse(B)),inverse(multiply(inverse(C),B))),D)))),C)) = D,
    inference(paramod,[status(thm)],[c_585,c_532]) ).

cnf(c_1538,plain,
    multiply(multiply(A,multiply(inverse(A),inverse(multiply(multiply(inverse(inverse(B)),inverse(multiply(inverse(C),B))),inverse(D))))),C) = D,
    inference(paramod,[status(thm)],[c_585,c_681]) ).

cnf(c_7758,plain,
    inverse(multiply(A,multiply(multiply(B,multiply(multiply(C,multiply(D,multiply(multiply(inverse(D),multiply(multiply(inverse(C),E),inverse(multiply(F,multiply(V6,E))))),F))),multiply(multiply(V6,V7),inverse(multiply(V8,multiply(B,V7)))))),multiply(multiply(V8,V9),inverse(V10))))) = multiply(V10,multiply(V11,inverse(multiply(multiply(inverse(inverse(V12)),inverse(multiply(inverse(multiply(A,V9)),V12))),V11)))),
    inference(paramod,[status(thm)],[c_802,c_13]) ).

cnf(c_1961,plain,
    multiply(A,multiply(B,inverse(multiply(multiply(inverse(inverse(C)),inverse(multiply(inverse(multiply(D,E)),C))),B)))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(copy,[status(thm)],[c_7758]) ).

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

cnf(c_2222,plain,
    multiply(inverse(A),multiply(A,multiply(B,inverse(multiply(inverse(C),B))))) = C,
    inference(paramod,[status(thm)],[c_678,c_7759]) ).

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

cnf(c_2334,plain,
    multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(multiply(C,inverse(D))))),C))) = D,
    inference(paramod,[status(thm)],[c_439,c_2222]) ).

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

cnf(c_2354,plain,
    inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(multiply(inverse(C),B))),D)))))),C)) = D,
    inference(paramod,[status(thm)],[c_2222,c_528]) ).

cnf(c_2674,plain,
    multiply(inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(multiply(inverse(C),B))),inverse(D))))))),C) = D,
    inference(paramod,[status(thm)],[c_2222,c_2334]) ).

cnf(c_7760,plain,
    inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),multiply(multiply(inverse(D),E),inverse(multiply(F,multiply(V6,E))))),F)),V6))),multiply(multiply(D,V7),V8)))) = multiply(V9,multiply(inverse(V9),inverse(multiply(multiply(inverse(inverse(V10)),inverse(multiply(inverse(multiply(A,V7)),V10))),V8)))),
    inference(paramod,[status(thm)],[c_1428,c_14]) ).

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

cnf(c_7761,plain,
    inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(A),multiply(B,multiply(C,multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(B,D)))))))))),F)) = multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(multiply(V7,inverse(multiply(inverse(F),V7)))),multiply(multiply(E,V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10)),
    inference(paramod,[status(thm)],[c_18,c_2354]) ).

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

cnf(c_3486,plain,
    multiply(multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(C))),inverse(D))),multiply(D,C)) = A,
    inference(paramod,[status(thm)],[c_678,c_2343]) ).

cnf(c_3833,plain,
    inverse(multiply(inverse(multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(inverse(multiply(C,D))))),inverse(D)))),A)) = C,
    inference(paramod,[status(thm)],[c_3486,c_345]) ).

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

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

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

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

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

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

cnf(c_4052,plain,
    inverse(multiply(inverse(multiply(A,multiply(B,multiply(inverse(B),C)))),A)) = C,
    inference(paramod,[status(thm)],[c_3946,c_7764]) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(c_4351,plain,
    multiply(A,multiply(B,inverse(multiply(inverse(multiply(inverse(A),C)),B)))) = C,
    inference(paramod,[status(thm)],[c_345,c_7770]) ).

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

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

cnf(c_7772,plain,
    inverse(multiply(inverse(multiply(A,B)),A)) = inverse(multiply(inverse(multiply(inverse(C),B)),inverse(C))),
    inference(paramod,[status(thm)],[c_4351,c_4052]) ).

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

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

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

cnf(c_4889,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),B)))) = C,
    inference(paramod,[status(thm)],[c_4595,c_4351]) ).

cnf(c_7774,plain,
    inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(inverse(multiply(C,D)),C)),E),inverse(multiply(F,multiply(V6,E))))),F)),V6)))) = multiply(inverse(multiply(V7,D)),V7),
    inference(paramod,[status(thm)],[c_4604,c_12]) ).

cnf(c_5057,plain,
    multiply(inverse(multiply(A,B)),A) = multiply(inverse(multiply(C,B)),C),
    inference(paramod,[status(thm)],[c_12,c_7774]) ).

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

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

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

cnf(c_5111,plain,
    inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(B),B)),
    inference(paramod,[status(thm)],[c_421,c_7776]) ).

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

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

cnf(c_7778,plain,
    inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(inverse(C),C)),D),inverse(multiply(E,multiply(F,D))))),E)),F)))) = multiply(inverse(V6),V6),
    inference(paramod,[status(thm)],[c_5111,c_12]) ).

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

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

cnf(c_5371,plain,
    multiply(A,multiply(B,inverse(multiply(inverse(multiply(inverse(C),C)),B)))) = A,
    inference(paramod,[status(thm)],[c_5111,c_4351]) ).

cnf(c_5372,plain,
    multiply(A,multiply(multiply(inverse(A),B),inverse(multiply(inverse(C),C)))) = B,
    inference(paramod,[status(thm)],[c_5111,c_4351]) ).

cnf(c_5466,plain,
    multiply(inverse(inverse(multiply(multiply(A,multiply(B,inverse(multiply(C,B)))),C))),multiply(inverse(D),D)) = A,
    inference(paramod,[status(thm)],[c_5216,c_828]) ).

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

cnf(c_5499,plain,
    multiply(inverse(inverse(multiply(multiply(A,multiply(inverse(A),inverse(multiply(B,inverse(C))))),B))),multiply(inverse(D),D)) = C,
    inference(paramod,[status(thm)],[c_5216,c_2334]) ).

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

cnf(c_5689,plain,
    multiply(inverse(multiply(inverse(A),A)),inverse(B)) = multiply(inverse(multiply(C,B)),C),
    inference(paramod,[status(thm)],[c_5111,c_5057]) ).

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

cnf(c_5842,plain,
    multiply(A,multiply(inverse(B),inverse(multiply(inverse(multiply(C,B)),C)))) = A,
    inference(paramod,[status(thm)],[c_5372,c_7779]) ).

cnf(c_7780,plain,
    inverse(multiply(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(B,D)))))),multiply(multiply(E,F),inverse(multiply(V6,multiply(A,F)))))),multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(V6,V8),inverse(multiply(V9,V10)))),V9)))) = multiply(V11,multiply(inverse(V11),inverse(multiply(multiply(inverse(inverse(V12)),inverse(multiply(inverse(V8),V12))),inverse(V10))))),
    inference(paramod,[status(thm)],[c_1538,c_17]) ).

cnf(c_6145,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(inverse(inverse(B)),inverse(multiply(inverse(C),B))),inverse(D))))) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),inverse(multiply(V8,multiply(F,V7)))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(copy,[status(thm)],[c_7780]) ).

cnf(c_6447,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),A)),multiply(inverse(C),C)) = B,
    inference(paramod,[status(thm)],[c_5216,c_4889]) ).

cnf(c_6450,plain,
    multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),inverse(multiply(inverse(multiply(C,D)),C))))) = multiply(inverse(D),B),
    inference(paramod,[status(thm)],[c_4889,c_5689]) ).

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

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

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

cnf(c_7782,plain,
    multiply(inverse(inverse(multiply(inverse(A),inverse(multiply(inverse(multiply(B,A)),B))))),inverse(C)) = multiply(inverse(multiply(D,C)),D),
    inference(paramod,[status(thm)],[c_5842,c_5689]) ).

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

cnf(c_6963,plain,
    multiply(inverse(multiply(A,inverse(B))),multiply(inverse(C),C)) = multiply(B,multiply(D,inverse(multiply(A,D)))),
    inference(paramod,[status(thm)],[c_345,c_6447]) ).

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

cnf(c_6983,plain,
    multiply(A,multiply(inverse(B),B)) = multiply(C,multiply(inverse(C),A)),
    inference(paramod,[status(thm)],[c_345,c_7783]) ).

cnf(c_7062,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),A)),inverse(multiply(C,B)))),multiply(inverse(D),D)) = C,
    inference(paramod,[status(thm)],[c_4604,c_6447]) ).

cnf(c_7075,plain,
    inverse(multiply(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(B,D)))))),multiply(multiply(E,F),inverse(multiply(V6,multiply(A,F)))))),multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(V6,multiply(inverse(V8),V8)),inverse(multiply(V9,V10)))),V9)))) = inverse(multiply(inverse(multiply(V11,V10)),V11)),
    inference(paramod,[status(thm)],[c_6447,c_17]) ).

cnf(c_7784,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),inverse(multiply(inverse(multiply(D,C)),D)))))) = A,
    inference(paramod,[status(thm)],[c_6447,c_5842]) ).

cnf(c_7084,plain,
    multiply(A,multiply(inverse(B),B)) = A,
    inference(paramod,[status(thm)],[c_6450,c_7784]) ).

cnf(c_7785,plain,
    inverse(multiply(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(B,D)))))),multiply(multiply(E,F),inverse(multiply(V6,multiply(A,F)))))),multiply(V7,multiply(multiply(inverse(V7),multiply(V6,inverse(multiply(V9,V10)))),V9)))) = inverse(multiply(inverse(multiply(V11,V10)),V11)),
    inference(paramod,[status(thm)],[c_7084,c_7075]) ).

cnf(c_7786,plain,
    V10 = inverse(multiply(inverse(multiply(V11,V10)),V11)),
    inference(paramod,[status(thm)],[c_954,c_7785]) ).

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

cnf(c_7787,plain,
    multiply(inverse(multiply(B,inverse(multiply(C,B)))),multiply(inverse(D),D)) = C,
    inference(paramod,[status(thm)],[c_7092,c_7062]) ).

cnf(c_7098,plain,
    inverse(multiply(A,inverse(multiply(B,A)))) = B,
    inference(paramod,[status(thm)],[c_7084,c_7787]) ).

cnf(c_7788,plain,
    A = multiply(C,multiply(inverse(C),A)),
    inference(paramod,[status(thm)],[c_7084,c_6983]) ).

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

cnf(c_7789,plain,
    inverse(multiply(A,inverse(B))) = multiply(B,multiply(D,inverse(multiply(A,D)))),
    inference(paramod,[status(thm)],[c_7084,c_6963]) ).

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

cnf(c_7790,plain,
    multiply(inverse(B),multiply(inverse(C),C)) = multiply(inverse(D),multiply(D,multiply(E,inverse(multiply(B,E))))),
    inference(paramod,[status(thm)],[c_7098,c_5510]) ).

cnf(c_7791,plain,
    inverse(B) = multiply(inverse(D),multiply(D,multiply(E,inverse(multiply(B,E))))),
    inference(paramod,[status(thm)],[c_7084,c_7790]) ).

cnf(c_7792,plain,
    inverse(B) = multiply(inverse(D),inverse(multiply(B,inverse(D)))),
    inference(paramod,[status(thm)],[c_7129,c_7791]) ).

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

cnf(c_7793,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(B,inverse(C))),B))),multiply(inverse(D),D)) = C,
    inference(paramod,[status(thm)],[c_7124,c_5499]) ).

cnf(c_7794,plain,
    multiply(inverse(inverse(C)),multiply(inverse(D),D)) = C,
    inference(paramod,[status(thm)],[c_7092,c_7793]) ).

cnf(c_7193,plain,
    inverse(inverse(A)) = A,
    inference(paramod,[status(thm)],[c_7084,c_7794]) ).

cnf(c_7795,plain,
    multiply(inverse(A),inverse(multiply(C,inverse(A)))) = multiply(D,multiply(inverse(multiply(C,D)),multiply(inverse(E),E))),
    inference(paramod,[status(thm)],[c_7129,c_5496]) ).

cnf(c_7796,plain,
    inverse(C) = multiply(D,multiply(inverse(multiply(C,D)),multiply(inverse(E),E))),
    inference(paramod,[status(thm)],[c_7187,c_7795]) ).

cnf(c_7797,plain,
    inverse(C) = multiply(D,inverse(multiply(C,D))),
    inference(paramod,[status(thm)],[c_7084,c_7796]) ).

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

cnf(c_7798,plain,
    multiply(inverse(inverse(multiply(multiply(A,inverse(C)),C))),multiply(inverse(D),D)) = A,
    inference(paramod,[status(thm)],[c_7195,c_5466]) ).

cnf(c_7799,plain,
    multiply(multiply(multiply(A,inverse(C)),C),multiply(inverse(D),D)) = A,
    inference(paramod,[status(thm)],[c_7193,c_7798]) ).

cnf(c_7203,plain,
    multiply(multiply(A,inverse(B)),B) = A,
    inference(paramod,[status(thm)],[c_7084,c_7799]) ).

cnf(c_7800,plain,
    inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),D)))))),multiply(inverse(E),E))) = D,
    inference(paramod,[status(thm)],[c_7195,c_5345]) ).

cnf(c_7801,plain,
    inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(multiply(inverse(C),C),D)))))),multiply(inverse(E),E))) = D,
    inference(paramod,[status(thm)],[c_7193,c_7800]) ).

cnf(c_7802,plain,
    inverse(multiply(inverse(inverse(inverse(multiply(multiply(inverse(C),C),D)))),multiply(inverse(E),E))) = D,
    inference(paramod,[status(thm)],[c_7124,c_7801]) ).

cnf(c_7803,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(C),C),D)),multiply(inverse(E),E))) = D,
    inference(paramod,[status(thm)],[c_7193,c_7802]) ).

cnf(c_7804,plain,
    inverse(inverse(multiply(multiply(inverse(C),C),D))) = D,
    inference(paramod,[status(thm)],[c_7084,c_7803]) ).

cnf(c_7227,plain,
    multiply(multiply(inverse(A),A),B) = B,
    inference(paramod,[status(thm)],[c_7193,c_7804]) ).

cnf(c_7805,plain,
    multiply(inverse(multiply(A,B)),A) = multiply(inverse(inverse(multiply(inverse(C),C))),inverse(B)),
    inference(paramod,[status(thm)],[c_7092,c_6857]) ).

cnf(c_7806,plain,
    multiply(inverse(multiply(A,B)),A) = multiply(multiply(inverse(C),C),inverse(B)),
    inference(paramod,[status(thm)],[c_7193,c_7805]) ).

cnf(c_7236,plain,
    multiply(inverse(multiply(A,B)),A) = inverse(B),
    inference(paramod,[status(thm)],[c_7227,c_7806]) ).

cnf(c_7807,plain,
    multiply(inverse(A),inverse(inverse(C))) = multiply(D,multiply(inverse(D),inverse(multiply(inverse(C),A)))),
    inference(paramod,[status(thm)],[c_7236,c_6466]) ).

cnf(c_7808,plain,
    multiply(inverse(A),C) = multiply(D,multiply(inverse(D),inverse(multiply(inverse(C),A)))),
    inference(paramod,[status(thm)],[c_7193,c_7807]) ).

cnf(c_7809,plain,
    multiply(inverse(A),C) = inverse(multiply(inverse(C),A)),
    inference(paramod,[status(thm)],[c_7124,c_7808]) ).

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

cnf(c_7810,plain,
    inverse(inverse(B)) = inverse(inverse(multiply(multiply(C,multiply(multiply(inverse(C),multiply(D,inverse(multiply(E,D)))),E)),B))),
    inference(paramod,[status(thm)],[c_7236,c_5112]) ).

cnf(c_7811,plain,
    B = inverse(inverse(multiply(multiply(C,multiply(multiply(inverse(C),multiply(D,inverse(multiply(E,D)))),E)),B))),
    inference(paramod,[status(thm)],[c_7193,c_7810]) ).

cnf(c_7812,plain,
    B = inverse(inverse(multiply(multiply(C,multiply(multiply(inverse(C),inverse(E)),E)),B))),
    inference(paramod,[status(thm)],[c_7195,c_7811]) ).

cnf(c_7813,plain,
    B = inverse(inverse(multiply(multiply(C,inverse(C)),B))),
    inference(paramod,[status(thm)],[c_7203,c_7812]) ).

cnf(c_7814,plain,
    B = multiply(multiply(C,inverse(C)),B),
    inference(paramod,[status(thm)],[c_7193,c_7813]) ).

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

cnf(c_7815,plain,
    multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(inverse(E))))) = multiply(multiply(A,C),E),
    inference(paramod,[status(thm)],[c_7236,c_5092]) ).

cnf(c_7424,plain,
    multiply(A,multiply(B,multiply(multiply(inverse(B),C),D))) = multiply(multiply(A,C),D),
    inference(paramod,[status(thm)],[c_7193,c_7815]) ).

cnf(c_7816,plain,
    inverse(multiply(B,inverse(C))) = inverse(multiply(inverse(multiply(D,multiply(C,multiply(E,multiply(F,multiply(inverse(F),inverse(multiply(B,E)))))))),D)),
    inference(paramod,[status(thm)],[c_7124,c_4345]) ).

cnf(c_7817,plain,
    inverse(multiply(B,inverse(C))) = inverse(multiply(inverse(multiply(D,multiply(C,multiply(E,inverse(multiply(B,E)))))),D)),
    inference(paramod,[status(thm)],[c_7124,c_7816]) ).

cnf(c_7818,plain,
    inverse(multiply(B,inverse(C))) = inverse(multiply(inverse(multiply(D,multiply(C,inverse(B)))),D)),
    inference(paramod,[status(thm)],[c_7195,c_7817]) ).

cnf(c_7819,plain,
    inverse(multiply(B,inverse(C))) = inverse(inverse(multiply(C,inverse(B)))),
    inference(paramod,[status(thm)],[c_7236,c_7818]) ).

cnf(c_7436,plain,
    inverse(multiply(A,inverse(B))) = multiply(B,inverse(A)),
    inference(paramod,[status(thm)],[c_7193,c_7819]) ).

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

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

cnf(c_7822,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(B,multiply(D,inverse(C)))),C)) = inverse(inverse(multiply(B,D))),
    inference(paramod,[status(thm)],[c_7236,c_7821]) ).

cnf(c_7437,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(B,multiply(C,inverse(D)))),D)) = multiply(B,C),
    inference(paramod,[status(thm)],[c_7193,c_7822]) ).

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

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

cnf(c_7825,plain,
    multiply(A,multiply(multiply(inverse(A),B),multiply(multiply(inverse(B),D),C))) = inverse(inverse(multiply(D,C))),
    inference(paramod,[status(thm)],[c_7236,c_7824]) ).

cnf(c_7441,plain,
    multiply(A,multiply(multiply(inverse(A),B),multiply(multiply(inverse(B),C),D))) = multiply(C,D),
    inference(paramod,[status(thm)],[c_7193,c_7825]) ).

cnf(c_7826,plain,
    multiply(A,multiply(inverse(C),inverse(D))) = inverse(multiply(inverse(multiply(E,multiply(multiply(F,multiply(inverse(F),inverse(inverse(A)))),inverse(multiply(D,C))))),E)),
    inference(paramod,[status(thm)],[c_7124,c_4153]) ).

cnf(c_7827,plain,
    multiply(A,multiply(inverse(C),inverse(D))) = inverse(multiply(inverse(multiply(E,multiply(multiply(F,multiply(inverse(F),A)),inverse(multiply(D,C))))),E)),
    inference(paramod,[status(thm)],[c_7193,c_7826]) ).

cnf(c_7828,plain,
    multiply(A,multiply(inverse(C),inverse(D))) = inverse(multiply(inverse(multiply(E,multiply(A,inverse(multiply(D,C))))),E)),
    inference(paramod,[status(thm)],[c_7124,c_7827]) ).

cnf(c_7829,plain,
    multiply(A,multiply(inverse(C),inverse(D))) = inverse(inverse(multiply(A,inverse(multiply(D,C))))),
    inference(paramod,[status(thm)],[c_7236,c_7828]) ).

cnf(c_7830,plain,
    multiply(A,multiply(inverse(C),inverse(D))) = inverse(multiply(multiply(D,C),inverse(A))),
    inference(paramod,[status(thm)],[c_7436,c_7829]) ).

cnf(c_7831,plain,
    multiply(A,multiply(inverse(C),inverse(D))) = multiply(A,inverse(multiply(D,C))),
    inference(paramod,[status(thm)],[c_7436,c_7830]) ).

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

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

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

cnf(c_7834,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(C,D)))) = inverse(multiply(inverse(multiply(E,multiply(multiply(F,multiply(inverse(F),inverse(D))),inverse(C)))),E)),
    inference(paramod,[status(thm)],[c_7124,c_7833]) ).

cnf(c_7835,plain,
    multiply(A,multiply(inverse(A),multiply(inverse(D),inverse(C)))) = inverse(multiply(inverse(multiply(E,multiply(multiply(F,multiply(inverse(F),inverse(D))),inverse(C)))),E)),
    inference(paramod,[status(thm)],[c_7443,c_7834]) ).

cnf(c_7836,plain,
    multiply(inverse(D),inverse(C)) = inverse(multiply(inverse(multiply(E,multiply(multiply(F,multiply(inverse(F),inverse(D))),inverse(C)))),E)),
    inference(paramod,[status(thm)],[c_7124,c_7835]) ).

cnf(c_7837,plain,
    multiply(inverse(D),inverse(C)) = inverse(multiply(inverse(multiply(E,multiply(inverse(D),inverse(C)))),E)),
    inference(paramod,[status(thm)],[c_7124,c_7836]) ).

cnf(c_7838,plain,
    multiply(inverse(D),inverse(C)) = inverse(inverse(multiply(inverse(D),inverse(C)))),
    inference(paramod,[status(thm)],[c_7236,c_7837]) ).

cnf(c_7839,plain,
    multiply(inverse(D),inverse(C)) = inverse(multiply(C,inverse(inverse(D)))),
    inference(paramod,[status(thm)],[c_7436,c_7838]) ).

cnf(c_7840,plain,
    multiply(inverse(D),inverse(C)) = inverse(multiply(C,D)),
    inference(paramod,[status(thm)],[c_7193,c_7839]) ).

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

cnf(c_7841,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(C),inverse(multiply(D,multiply(multiply(inverse(D),multiply(multiply(inverse(E),F),inverse(multiply(V6,multiply(C,F))))),V6)))))),A)) = E,
    inference(paramod,[status(thm)],[c_7124,c_3963]) ).

cnf(c_7842,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(C),inverse(multiply(D,multiply(multiply(inverse(D),multiply(multiply(inverse(E),F),multiply(inverse(multiply(C,F)),inverse(V6)))),V6)))))),A)) = E,
    inference(paramod,[status(thm)],[c_7451,c_7841]) ).

cnf(c_7843,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(C),inverse(multiply(D,multiply(multiply(inverse(D),multiply(multiply(inverse(E),F),multiply(multiply(inverse(F),inverse(C)),inverse(V6)))),V6)))))),A)) = E,
    inference(paramod,[status(thm)],[c_7451,c_7842]) ).

cnf(c_7844,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(C),inverse(multiply(multiply(inverse(E),F),multiply(inverse(F),inverse(C))))))),A)) = E,
    inference(paramod,[status(thm)],[c_7437,c_7843]) ).

cnf(c_7845,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(C),multiply(inverse(multiply(inverse(F),inverse(C))),inverse(multiply(inverse(E),F)))))),A)) = E,
    inference(paramod,[status(thm)],[c_7451,c_7844]) ).

cnf(c_7846,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(C),multiply(multiply(inverse(inverse(C)),inverse(inverse(F))),inverse(multiply(inverse(E),F)))))),A)) = E,
    inference(paramod,[status(thm)],[c_7451,c_7845]) ).

cnf(c_7847,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(C),multiply(multiply(C,inverse(inverse(F))),inverse(multiply(inverse(E),F)))))),A)) = E,
    inference(paramod,[status(thm)],[c_7193,c_7846]) ).

cnf(c_7848,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(C),multiply(multiply(C,F),inverse(multiply(inverse(E),F)))))),A)) = E,
    inference(paramod,[status(thm)],[c_7193,c_7847]) ).

cnf(c_7849,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(C),multiply(multiply(C,F),multiply(inverse(F),inverse(inverse(E))))))),A)) = E,
    inference(paramod,[status(thm)],[c_7451,c_7848]) ).

cnf(c_7850,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(C),multiply(multiply(C,F),multiply(inverse(F),E))))),A)) = E,
    inference(paramod,[status(thm)],[c_7193,c_7849]) ).

cnf(c_7851,plain,
    inverse(multiply(multiply(inverse(multiply(inverse(C),multiply(multiply(C,F),multiply(inverse(F),E)))),inverse(A)),A)) = E,
    inference(paramod,[status(thm)],[c_7451,c_7850]) ).

cnf(c_7852,plain,
    inverse(multiply(multiply(multiply(inverse(multiply(multiply(C,F),multiply(inverse(F),E))),inverse(inverse(C))),inverse(A)),A)) = E,
    inference(paramod,[status(thm)],[c_7451,c_7851]) ).

cnf(c_7853,plain,
    inverse(multiply(multiply(multiply(multiply(inverse(multiply(inverse(F),E)),inverse(multiply(C,F))),inverse(inverse(C))),inverse(A)),A)) = E,
    inference(paramod,[status(thm)],[c_7451,c_7852]) ).

cnf(c_7854,plain,
    inverse(multiply(multiply(multiply(multiply(multiply(inverse(E),inverse(inverse(F))),inverse(multiply(C,F))),inverse(inverse(C))),inverse(A)),A)) = E,
    inference(paramod,[status(thm)],[c_7451,c_7853]) ).

cnf(c_7855,plain,
    inverse(multiply(multiply(multiply(multiply(multiply(inverse(E),F),inverse(multiply(C,F))),inverse(inverse(C))),inverse(A)),A)) = E,
    inference(paramod,[status(thm)],[c_7193,c_7854]) ).

cnf(c_7856,plain,
    inverse(multiply(multiply(multiply(multiply(multiply(inverse(E),F),multiply(inverse(F),inverse(C))),inverse(inverse(C))),inverse(A)),A)) = E,
    inference(paramod,[status(thm)],[c_7451,c_7855]) ).

cnf(c_7857,plain,
    inverse(multiply(multiply(multiply(multiply(multiply(inverse(E),F),multiply(inverse(F),inverse(C))),C),inverse(A)),A)) = E,
    inference(paramod,[status(thm)],[c_7193,c_7856]) ).

cnf(c_7858,plain,
    inverse(multiply(multiply(multiply(inverse(E),F),multiply(inverse(F),inverse(C))),C)) = E,
    inference(paramod,[status(thm)],[c_7203,c_7857]) ).

cnf(c_7859,plain,
    multiply(inverse(C),inverse(multiply(multiply(inverse(E),F),multiply(inverse(F),inverse(C))))) = E,
    inference(paramod,[status(thm)],[c_7451,c_7858]) ).

cnf(c_7860,plain,
    multiply(inverse(C),multiply(inverse(multiply(inverse(F),inverse(C))),inverse(multiply(inverse(E),F)))) = E,
    inference(paramod,[status(thm)],[c_7451,c_7859]) ).

cnf(c_7861,plain,
    multiply(inverse(C),multiply(multiply(inverse(inverse(C)),inverse(inverse(F))),inverse(multiply(inverse(E),F)))) = E,
    inference(paramod,[status(thm)],[c_7451,c_7860]) ).

cnf(c_7862,plain,
    multiply(inverse(C),multiply(multiply(C,inverse(inverse(F))),inverse(multiply(inverse(E),F)))) = E,
    inference(paramod,[status(thm)],[c_7193,c_7861]) ).

cnf(c_7863,plain,
    multiply(inverse(C),multiply(multiply(C,F),inverse(multiply(inverse(E),F)))) = E,
    inference(paramod,[status(thm)],[c_7193,c_7862]) ).

cnf(c_7864,plain,
    multiply(inverse(C),multiply(multiply(C,F),multiply(inverse(F),inverse(inverse(E))))) = E,
    inference(paramod,[status(thm)],[c_7451,c_7863]) ).

cnf(c_7479,plain,
    multiply(inverse(A),multiply(multiply(A,B),multiply(inverse(B),C))) = C,
    inference(paramod,[status(thm)],[c_7193,c_7864]) ).

cnf(c_7865,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(B,multiply(inverse(B),inverse(inverse(C))))),multiply(multiply(D,E),inverse(multiply(F,multiply(V6,E))))),F)),V6)) = inverse(multiply(inverse(inverse(multiply(V7,multiply(inverse(V7),multiply(V8,multiply(V9,multiply(multiply(inverse(V9),V10),inverse(multiply(D,multiply(V8,V10)))))))))),C)),
    inference(paramod,[status(thm)],[c_7451,c_2916]) ).

cnf(c_7866,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(B,multiply(inverse(B),C))),multiply(multiply(D,E),inverse(multiply(F,multiply(V6,E))))),F)),V6)) = inverse(multiply(inverse(inverse(multiply(V7,multiply(inverse(V7),multiply(V8,multiply(V9,multiply(multiply(inverse(V9),V10),inverse(multiply(D,multiply(V8,V10)))))))))),C)),
    inference(paramod,[status(thm)],[c_7193,c_7865]) ).

cnf(c_7867,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(C),multiply(multiply(D,E),inverse(multiply(F,multiply(V6,E))))),F)),V6)) = inverse(multiply(inverse(inverse(multiply(V7,multiply(inverse(V7),multiply(V8,multiply(V9,multiply(multiply(inverse(V9),V10),inverse(multiply(D,multiply(V8,V10)))))))))),C)),
    inference(paramod,[status(thm)],[c_7124,c_7866]) ).

cnf(c_7868,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(C),multiply(multiply(D,E),multiply(inverse(multiply(V6,E)),inverse(F)))),F)),V6)) = inverse(multiply(inverse(inverse(multiply(V7,multiply(inverse(V7),multiply(V8,multiply(V9,multiply(multiply(inverse(V9),V10),inverse(multiply(D,multiply(V8,V10)))))))))),C)),
    inference(paramod,[status(thm)],[c_7451,c_7867]) ).

cnf(c_7869,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(C),multiply(multiply(D,E),multiply(multiply(inverse(E),inverse(V6)),inverse(F)))),F)),V6)) = inverse(multiply(inverse(inverse(multiply(V7,multiply(inverse(V7),multiply(V8,multiply(V9,multiply(multiply(inverse(V9),V10),inverse(multiply(D,multiply(V8,V10)))))))))),C)),
    inference(paramod,[status(thm)],[c_7451,c_7868]) ).

cnf(c_7870,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(C),multiply(multiply(D,E),multiply(multiply(inverse(E),inverse(V6)),inverse(F)))),F)),V6)) = inverse(multiply(inverse(inverse(multiply(V7,multiply(inverse(V7),multiply(V8,multiply(V9,multiply(multiply(inverse(V9),V10),multiply(inverse(multiply(V8,V10)),inverse(D))))))))),C)),
    inference(paramod,[status(thm)],[c_7451,c_7869]) ).

cnf(c_7871,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(C),multiply(multiply(D,E),multiply(multiply(inverse(E),inverse(V6)),inverse(F)))),F)),V6)) = inverse(multiply(inverse(inverse(multiply(V7,multiply(inverse(V7),multiply(V8,multiply(V9,multiply(multiply(inverse(V9),V10),multiply(multiply(inverse(V10),inverse(V8)),inverse(D))))))))),C)),
    inference(paramod,[status(thm)],[c_7451,c_7870]) ).

cnf(c_7872,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(C),multiply(multiply(D,E),multiply(multiply(inverse(E),inverse(V6)),inverse(F)))),F)),V6)) = inverse(multiply(inverse(inverse(multiply(V7,multiply(inverse(V7),multiply(V8,multiply(inverse(V8),inverse(D))))))),C)),
    inference(paramod,[status(thm)],[c_7441,c_7871]) ).

cnf(c_7873,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(C),multiply(multiply(D,E),multiply(multiply(inverse(E),inverse(V6)),inverse(F)))),F)),V6)) = inverse(multiply(inverse(inverse(multiply(V7,multiply(inverse(V7),inverse(D))))),C)),
    inference(paramod,[status(thm)],[c_7124,c_7872]) ).

cnf(c_7874,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(C),multiply(multiply(D,E),multiply(multiply(inverse(E),inverse(V6)),inverse(F)))),F)),V6)) = inverse(multiply(inverse(inverse(inverse(D))),C)),
    inference(paramod,[status(thm)],[c_7124,c_7873]) ).

cnf(c_7875,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(C),multiply(multiply(D,E),multiply(multiply(inverse(E),inverse(V6)),inverse(F)))),F)),V6)) = inverse(multiply(inverse(D),C)),
    inference(paramod,[status(thm)],[c_7193,c_7874]) ).

cnf(c_7876,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(multiply(inverse(C),multiply(multiply(D,E),multiply(multiply(inverse(E),inverse(V6)),inverse(F)))),F)),V6)) = multiply(inverse(C),inverse(inverse(D))),
    inference(paramod,[status(thm)],[c_7451,c_7875]) ).

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

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

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

cnf(c_7879,plain,
    multiply(A,multiply(B,multiply(inverse(B),multiply(multiply(inverse(A),C),inverse(multiply(multiply(D,inverse(D)),multiply(inverse(F),C))))))) = F,
    inference(paramod,[status(thm)],[c_7227,c_7878]) ).

cnf(c_7880,plain,
    multiply(A,multiply(B,multiply(inverse(B),multiply(multiply(inverse(A),C),inverse(multiply(inverse(F),C)))))) = F,
    inference(paramod,[status(thm)],[c_7412,c_7879]) ).

cnf(c_7881,plain,
    multiply(A,multiply(B,multiply(inverse(B),multiply(multiply(inverse(A),C),multiply(inverse(C),inverse(inverse(F))))))) = F,
    inference(paramod,[status(thm)],[c_7451,c_7880]) ).

cnf(c_7882,plain,
    multiply(A,multiply(B,multiply(inverse(B),multiply(multiply(inverse(A),C),multiply(inverse(C),F))))) = F,
    inference(paramod,[status(thm)],[c_7193,c_7881]) ).

cnf(c_7546,plain,
    multiply(A,multiply(multiply(inverse(A),B),multiply(inverse(B),C))) = C,
    inference(paramod,[status(thm)],[c_7124,c_7882]) ).

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

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

cnf(c_7885,plain,
    multiply(multiply(A,multiply(inverse(A),inverse(C))),multiply(multiply(C,V6),inverse(multiply(V7,multiply(inverse(V8),V6))))) = multiply(V8,multiply(V9,inverse(multiply(V7,V9)))),
    inference(paramod,[status(thm)],[c_7533,c_7884]) ).

cnf(c_7886,plain,
    multiply(inverse(C),multiply(multiply(C,V6),inverse(multiply(V7,multiply(inverse(V8),V6))))) = multiply(V8,multiply(V9,inverse(multiply(V7,V9)))),
    inference(paramod,[status(thm)],[c_7124,c_7885]) ).

cnf(c_7887,plain,
    multiply(inverse(C),multiply(multiply(C,V6),multiply(inverse(multiply(inverse(V8),V6)),inverse(V7)))) = multiply(V8,multiply(V9,inverse(multiply(V7,V9)))),
    inference(paramod,[status(thm)],[c_7451,c_7886]) ).

cnf(c_7888,plain,
    multiply(inverse(C),multiply(multiply(C,V6),multiply(multiply(inverse(V6),inverse(inverse(V8))),inverse(V7)))) = multiply(V8,multiply(V9,inverse(multiply(V7,V9)))),
    inference(paramod,[status(thm)],[c_7451,c_7887]) ).

cnf(c_7889,plain,
    multiply(inverse(C),multiply(multiply(C,V6),multiply(multiply(inverse(V6),V8),inverse(V7)))) = multiply(V8,multiply(V9,inverse(multiply(V7,V9)))),
    inference(paramod,[status(thm)],[c_7193,c_7888]) ).

cnf(c_7890,plain,
    multiply(inverse(C),multiply(multiply(C,V6),multiply(multiply(inverse(V6),V8),inverse(V7)))) = multiply(V8,multiply(V9,multiply(inverse(V9),inverse(V7)))),
    inference(paramod,[status(thm)],[c_7451,c_7889]) ).

cnf(c_7653,plain,
    multiply(inverse(A),multiply(multiply(A,B),multiply(multiply(inverse(B),C),inverse(D)))) = multiply(C,inverse(D)),
    inference(paramod,[status(thm)],[c_7124,c_7890]) ).

cnf(c_7891,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(multiply(inverse(C),B))),inverse(D))))) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),inverse(multiply(V8,multiply(F,V7)))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7193,c_6145]) ).

cnf(c_7892,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),inverse(inverse(C)))),inverse(D))))) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),inverse(multiply(V8,multiply(F,V7)))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7451,c_7891]) ).

cnf(c_7893,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),C)),inverse(D))))) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),inverse(multiply(V8,multiply(F,V7)))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7193,c_7892]) ).

cnf(c_7894,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(C,inverse(D))))) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),inverse(multiply(V8,multiply(F,V7)))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7124,c_7893]) ).

cnf(c_7895,plain,
    multiply(A,multiply(inverse(A),multiply(inverse(inverse(D)),inverse(C)))) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),inverse(multiply(V8,multiply(F,V7)))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7451,c_7894]) ).

cnf(c_7896,plain,
    multiply(A,multiply(inverse(A),multiply(D,inverse(C)))) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),inverse(multiply(V8,multiply(F,V7)))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7193,c_7895]) ).

cnf(c_7897,plain,
    multiply(D,inverse(C)) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),inverse(multiply(V8,multiply(F,V7)))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7124,c_7896]) ).

cnf(c_7898,plain,
    multiply(D,inverse(C)) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),multiply(inverse(multiply(F,V7)),inverse(V8))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7451,c_7897]) ).

cnf(c_7899,plain,
    multiply(D,inverse(C)) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),multiply(multiply(inverse(V7),inverse(F)),inverse(V8))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7451,c_7898]) ).

cnf(c_7900,plain,
    multiply(D,inverse(C)) = inverse(multiply(multiply(E,multiply(multiply(F,multiply(inverse(F),inverse(V8))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7441,c_7899]) ).

cnf(c_7901,plain,
    multiply(D,inverse(C)) = inverse(multiply(multiply(E,multiply(inverse(V8),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7124,c_7900]) ).

cnf(c_7902,plain,
    multiply(D,inverse(C)) = inverse(multiply(multiply(E,multiply(inverse(V8),multiply(multiply(V8,V9),multiply(inverse(multiply(E,V9)),inverse(V10))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7451,c_7901]) ).

cnf(c_7903,plain,
    multiply(D,inverse(C)) = inverse(multiply(multiply(E,multiply(inverse(V8),multiply(multiply(V8,V9),multiply(multiply(inverse(V9),inverse(E)),inverse(V10))))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7451,c_7902]) ).

cnf(c_7904,plain,
    multiply(D,inverse(C)) = inverse(multiply(multiply(E,multiply(inverse(E),inverse(V10))),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7653,c_7903]) ).

cnf(c_7905,plain,
    multiply(D,inverse(C)) = inverse(multiply(inverse(V10),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),inverse(multiply(V12,D)))),V12)))),
    inference(paramod,[status(thm)],[c_7124,c_7904]) ).

cnf(c_7906,plain,
    multiply(D,inverse(C)) = inverse(multiply(inverse(V10),multiply(V11,multiply(multiply(inverse(V11),multiply(multiply(V10,C),multiply(inverse(D),inverse(V12)))),V12)))),
    inference(paramod,[status(thm)],[c_7451,c_7905]) ).

cnf(c_7907,plain,
    multiply(D,inverse(C)) = inverse(multiply(inverse(V10),multiply(multiply(V10,C),inverse(D)))),
    inference(paramod,[status(thm)],[c_7437,c_7906]) ).

cnf(c_7908,plain,
    multiply(D,inverse(C)) = multiply(inverse(multiply(multiply(V10,C),inverse(D))),inverse(inverse(V10))),
    inference(paramod,[status(thm)],[c_7451,c_7907]) ).

cnf(c_7909,plain,
    multiply(D,inverse(C)) = multiply(multiply(inverse(inverse(D)),inverse(multiply(V10,C))),inverse(inverse(V10))),
    inference(paramod,[status(thm)],[c_7451,c_7908]) ).

cnf(c_7910,plain,
    multiply(D,inverse(C)) = multiply(multiply(D,inverse(multiply(V10,C))),inverse(inverse(V10))),
    inference(paramod,[status(thm)],[c_7193,c_7909]) ).

cnf(c_7911,plain,
    multiply(D,inverse(C)) = multiply(multiply(D,multiply(inverse(C),inverse(V10))),inverse(inverse(V10))),
    inference(paramod,[status(thm)],[c_7451,c_7910]) ).

cnf(c_7912,plain,
    multiply(D,inverse(C)) = multiply(multiply(D,multiply(inverse(C),inverse(V10))),V10),
    inference(paramod,[status(thm)],[c_7193,c_7911]) ).

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

cnf(c_7913,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(multiply(inverse(multiply(C,D)),B))),E)))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7193,c_2786]) ).

cnf(c_7914,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(D),inverse(C)),B))),E)))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7451,c_7913]) ).

cnf(c_7915,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),inverse(multiply(inverse(D),inverse(C))))),E)))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7451,c_7914]) ).

cnf(c_7916,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),multiply(inverse(inverse(C)),inverse(inverse(D))))),E)))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7451,c_7915]) ).

cnf(c_7917,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),multiply(C,inverse(inverse(D))))),E)))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7193,c_7916]) ).

cnf(c_7918,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),multiply(C,D))),E)))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7193,c_7917]) ).

cnf(c_7919,plain,
    multiply(A,multiply(inverse(A),inverse(multiply(multiply(C,D),E)))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7124,c_7918]) ).

cnf(c_7920,plain,
    multiply(A,multiply(inverse(A),multiply(inverse(E),inverse(multiply(C,D))))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7451,c_7919]) ).

cnf(c_7921,plain,
    multiply(A,multiply(inverse(A),multiply(inverse(E),multiply(inverse(D),inverse(C))))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7451,c_7920]) ).

cnf(c_7922,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7124,c_7921]) ).

cnf(c_7923,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),multiply(inverse(multiply(V10,V8)),inverse(V9)))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7451,c_7922]) ).

cnf(c_7924,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = inverse(multiply(C,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(V7),V8),multiply(multiply(inverse(V8),inverse(V10)),inverse(V9)))),V9)),V10))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7451,c_7923]) ).

cnf(c_7925,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = inverse(multiply(C,multiply(multiply(F,multiply(inverse(F),inverse(V7))),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7533,c_7924]) ).

cnf(c_7926,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = inverse(multiply(C,multiply(inverse(V7),multiply(multiply(V7,D),E)))),
    inference(paramod,[status(thm)],[c_7124,c_7925]) ).

cnf(c_7927,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = multiply(inverse(multiply(inverse(V7),multiply(multiply(V7,D),E))),inverse(C)),
    inference(paramod,[status(thm)],[c_7451,c_7926]) ).

cnf(c_7928,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = multiply(multiply(inverse(multiply(multiply(V7,D),E)),inverse(inverse(V7))),inverse(C)),
    inference(paramod,[status(thm)],[c_7451,c_7927]) ).

cnf(c_7929,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = multiply(multiply(multiply(inverse(E),inverse(multiply(V7,D))),inverse(inverse(V7))),inverse(C)),
    inference(paramod,[status(thm)],[c_7451,c_7928]) ).

cnf(c_7930,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = multiply(multiply(multiply(inverse(E),multiply(inverse(D),inverse(V7))),inverse(inverse(V7))),inverse(C)),
    inference(paramod,[status(thm)],[c_7451,c_7929]) ).

cnf(c_7931,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = multiply(multiply(multiply(inverse(E),multiply(inverse(D),inverse(V7))),V7),inverse(C)),
    inference(paramod,[status(thm)],[c_7193,c_7930]) ).

cnf(c_7932,plain,
    multiply(inverse(E),multiply(inverse(D),inverse(C))) = multiply(multiply(inverse(E),inverse(D)),inverse(C)),
    inference(paramod,[status(thm)],[c_7655,c_7931]) ).

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

cnf(c_7933,plain,
    multiply(A,multiply(B,inverse(multiply(multiply(C,inverse(multiply(inverse(multiply(D,E)),C))),B)))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7193,c_1961]) ).

cnf(c_7934,plain,
    multiply(A,multiply(B,inverse(multiply(multiply(C,inverse(multiply(multiply(inverse(E),inverse(D)),C))),B)))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7451,c_7933]) ).

cnf(c_7935,plain,
    multiply(A,multiply(B,inverse(multiply(multiply(C,multiply(inverse(C),inverse(multiply(inverse(E),inverse(D))))),B)))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7451,c_7934]) ).

cnf(c_7936,plain,
    multiply(A,multiply(B,inverse(multiply(multiply(C,multiply(inverse(C),multiply(inverse(inverse(D)),inverse(inverse(E))))),B)))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7451,c_7935]) ).

cnf(c_7937,plain,
    multiply(A,multiply(B,inverse(multiply(multiply(C,multiply(inverse(C),multiply(D,inverse(inverse(E))))),B)))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7193,c_7936]) ).

cnf(c_7938,plain,
    multiply(A,multiply(B,inverse(multiply(multiply(C,multiply(inverse(C),multiply(D,E))),B)))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7193,c_7937]) ).

cnf(c_7939,plain,
    multiply(A,multiply(B,inverse(multiply(multiply(D,E),B)))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7124,c_7938]) ).

cnf(c_7940,plain,
    multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(D,E))))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7451,c_7939]) ).

cnf(c_7941,plain,
    multiply(A,multiply(B,multiply(inverse(B),multiply(inverse(E),inverse(D))))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7451,c_7940]) ).

cnf(c_7942,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),inverse(multiply(V9,multiply(V10,V8))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7124,c_7941]) ).

cnf(c_7943,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),multiply(inverse(multiply(V10,V8)),inverse(V9)))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7451,c_7942]) ).

cnf(c_7944,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),multiply(multiply(inverse(V8),inverse(V10)),inverse(V9)))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7451,c_7943]) ).

cnf(c_7945,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(V6,multiply(V7,multiply(multiply(inverse(V7),multiply(multiply(inverse(V6),V8),multiply(inverse(V8),multiply(inverse(V10),inverse(V9))))),V9))),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7667,c_7944]) ).

cnf(c_7946,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(multiply(V6,multiply(multiply(inverse(V6),V8),multiply(inverse(V8),multiply(inverse(V10),inverse(V9))))),V9),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7424,c_7945]) ).

cnf(c_7947,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(multiply(multiply(inverse(V10),inverse(V9)),V9),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7546,c_7946]) ).

cnf(c_7948,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(inverse(V10),multiply(multiply(V10,V11),inverse(multiply(V12,multiply(F,V11)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7203,c_7947]) ).

cnf(c_7949,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(inverse(V10),multiply(multiply(V10,V11),multiply(inverse(multiply(F,V11)),inverse(V12))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7451,c_7948]) ).

cnf(c_7950,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(inverse(V10),multiply(multiply(V10,V11),multiply(multiply(inverse(V11),inverse(F)),inverse(V12))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7451,c_7949]) ).

cnf(c_7951,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(inverse(V10),multiply(multiply(V10,V11),multiply(inverse(V11),multiply(inverse(F),inverse(V12)))))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7667,c_7950]) ).

cnf(c_7952,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(multiply(F,multiply(inverse(F),inverse(V12))),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7479,c_7951]) ).

cnf(c_7953,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = inverse(multiply(D,multiply(inverse(V12),multiply(multiply(V12,E),inverse(A))))),
    inference(paramod,[status(thm)],[c_7124,c_7952]) ).

cnf(c_7954,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = multiply(inverse(multiply(inverse(V12),multiply(multiply(V12,E),inverse(A)))),inverse(D)),
    inference(paramod,[status(thm)],[c_7451,c_7953]) ).

cnf(c_7955,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = multiply(multiply(inverse(multiply(multiply(V12,E),inverse(A))),inverse(inverse(V12))),inverse(D)),
    inference(paramod,[status(thm)],[c_7451,c_7954]) ).

cnf(c_7956,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = multiply(multiply(multiply(inverse(inverse(A)),inverse(multiply(V12,E))),inverse(inverse(V12))),inverse(D)),
    inference(paramod,[status(thm)],[c_7451,c_7955]) ).

cnf(c_7957,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = multiply(multiply(multiply(A,inverse(multiply(V12,E))),inverse(inverse(V12))),inverse(D)),
    inference(paramod,[status(thm)],[c_7193,c_7956]) ).

cnf(c_7958,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = multiply(multiply(multiply(A,multiply(inverse(E),inverse(V12))),inverse(inverse(V12))),inverse(D)),
    inference(paramod,[status(thm)],[c_7451,c_7957]) ).

cnf(c_7959,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = multiply(multiply(multiply(A,multiply(inverse(E),inverse(V12))),V12),inverse(D)),
    inference(paramod,[status(thm)],[c_7193,c_7958]) ).

cnf(c_7960,plain,
    multiply(A,multiply(inverse(E),inverse(D))) = multiply(multiply(A,inverse(E)),inverse(D)),
    inference(paramod,[status(thm)],[c_7655,c_7959]) ).

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

cnf(c_7961,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(multiply(inverse(multiply(inverse(D),inverse(E))),B))),inverse(F))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7124,c_3925]) ).

cnf(c_7962,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(inverse(E)),inverse(inverse(D))),B))),inverse(F))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7451,c_7961]) ).

cnf(c_7963,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(multiply(multiply(E,inverse(inverse(D))),B))),inverse(F))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7193,c_7962]) ).

cnf(c_7964,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(multiply(multiply(E,D),B))),inverse(F))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7193,c_7963]) ).

cnf(c_7965,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),inverse(multiply(E,D)))),inverse(F))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7451,c_7964]) ).

cnf(c_7966,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),multiply(inverse(D),inverse(E)))),inverse(F))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7451,c_7965]) ).

cnf(c_7967,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(multiply(inverse(D),inverse(E)),inverse(F))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7124,c_7966]) ).

cnf(c_7968,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),inverse(multiply(inverse(D),multiply(inverse(E),inverse(F)))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7686,c_7967]) ).

cnf(c_7969,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),multiply(inverse(multiply(inverse(E),inverse(F))),inverse(inverse(D))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7451,c_7968]) ).

cnf(c_7970,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),multiply(multiply(inverse(inverse(F)),inverse(inverse(E))),inverse(inverse(D))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7451,c_7969]) ).

cnf(c_7971,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),multiply(multiply(F,inverse(inverse(E))),inverse(inverse(D))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7193,c_7970]) ).

cnf(c_7972,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),multiply(multiply(F,E),inverse(inverse(D))))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7193,c_7971]) ).

cnf(c_7973,plain,
    inverse(inverse(multiply(A,multiply(inverse(A),multiply(multiply(F,E),D))))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7193,c_7972]) ).

cnf(c_7974,plain,
    inverse(inverse(multiply(multiply(F,E),D))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7124,c_7973]) ).

cnf(c_7975,plain,
    inverse(multiply(inverse(D),inverse(multiply(F,E)))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7451,c_7974]) ).

cnf(c_7976,plain,
    inverse(multiply(inverse(D),multiply(inverse(E),inverse(F)))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7451,c_7975]) ).

cnf(c_7977,plain,
    multiply(inverse(multiply(inverse(E),inverse(F))),inverse(inverse(D))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7451,c_7976]) ).

cnf(c_7978,plain,
    multiply(multiply(inverse(inverse(F)),inverse(inverse(E))),inverse(inverse(D))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7451,c_7977]) ).

cnf(c_7979,plain,
    multiply(multiply(F,inverse(inverse(E))),inverse(inverse(D))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7193,c_7978]) ).

cnf(c_7980,plain,
    multiply(multiply(F,E),inverse(inverse(D))) = multiply(F,multiply(E,D)),
    inference(paramod,[status(thm)],[c_7193,c_7979]) ).

cnf(c_7748,plain,
    multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
    inference(paramod,[status(thm)],[c_7193,c_7980]) ).

cnf(c_7749,plain,
    $false,
    inference(resolve,[status(thm)],[c_7748,c_2]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP441-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04  % Command  : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36  % Computer : n004.cluster.edu
% 0.09/0.36  % Model    : x86_64 x86_64
% 0.09/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36  % Memory   : 8046.5625MB
% 0.09/0.36  % OS       : Linux 6.8.0-71-generic
% 0.09/0.36  % CPULimit : 300
% 0.09/0.36  % WCLimit  : 300
% 0.09/0.36  % DateTime : Fri Sep 25 14:54:21 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 0.09/0.36  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36  % Process 3464018 was started by sandbox2 on n004,
% 0.09/0.36  % Fri Sep 25 14:54:21 2026
% 0.09/0.36  % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.36  
% 0.09/0.36  % From the command line: assign(max_seconds, 300).
% 13.05/2.10  
% 13.05/2.10  % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 13.05/2.10  
% 13.05/2.10  % SZS status Unsatisfiable for theBenchmark
% 13.05/2.10  
% 13.05/2.10  % Proof 1 at 1.48 (+ 0.20) seconds.
% 13.05/2.10  % Length of proof is 107.
% 13.05/2.10  % Level of proof is 36.
% 13.05/2.10  % Maximum clause weight is 100.000.
% 13.05/2.10  % Given clauses 61.
% 13.05/2.10  
% 13.05/2.10  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------