%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP405-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:28:47 AM UTC 2026
% Result : Unsatisfiable 33.63s 5.31s
% Output : CNFRefutation 33.63s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,inverse(multiply(inverse(multiply(inverse(multiply(VAR_0,VAR_1)),VAR_2)),inverse(multiply(VAR_1,multiply(inverse(VAR_1),VAR_1)))))) = VAR_2,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),inverse(multiply(B,multiply(inverse(B),B)))))) = C,
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,
multiply(A,inverse(multiply(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,D)),B)),inverse(multiply(D,multiply(inverse(D),D))))),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,D)),B)),inverse(multiply(D,multiply(inverse(D),D)))))),inverse(multiply(inverse(multiply(inverse(multiply(A,D)),B)),inverse(multiply(D,multiply(inverse(D),D))))))))))) = C,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_8417,plain,
multiply(A,inverse(multiply(inverse(B),inverse(multiply(C,multiply(inverse(C),C)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,C)),D)),B)),inverse(multiply(D,multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_4,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),D)),inverse(multiply(C,multiply(inverse(C),C))))) = multiply(A,inverse(multiply(inverse(D),inverse(multiply(B,multiply(inverse(B),B)))))),
inference(copy,[status(thm)],[c_8417]) ).
cnf(c_13,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(C),inverse(multiply(B,multiply(inverse(B),B))))))) = C,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_8418,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),inverse(multiply(B,multiply(inverse(B),B))))))),D)),multiply(inverse(C),E))),inverse(multiply(D,multiply(inverse(D),D))))) = E,
inference(paramod,[status(thm)],[c_3,c_4]) ).
cnf(c_15,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(A),C))),inverse(multiply(B,multiply(inverse(B),B))))) = C,
inference(paramod,[status(thm)],[c_1,c_8418]) ).
cnf(c_8419,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(inverse(D),B)),multiply(inverse(D),C)),
inference(paramod,[status(thm)],[c_15,c_13]) ).
cnf(c_45,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(A),C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(copy,[status(thm)],[c_8419]) ).
cnf(c_8420,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(C),A))),inverse(multiply(D,multiply(inverse(D),D))))),E))),inverse(multiply(B,multiply(inverse(B),B))))) = E,
inference(paramod,[status(thm)],[c_15,c_15]) ).
cnf(c_46,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),inverse(multiply(B,multiply(inverse(B),B))))) = C,
inference(paramod,[status(thm)],[c_15,c_8420]) ).
cnf(c_54,plain,
multiply(inverse(multiply(inverse(A),B)),C) = multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),E)),C)),inverse(multiply(E,multiply(inverse(E),E))))))),
inference(paramod,[status(thm)],[c_1,c_45]) ).
cnf(c_8421,plain,
multiply(multiply(A,inverse(multiply(inverse(B),inverse(multiply(C,multiply(inverse(C),C)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_4,c_45]) ).
cnf(c_81,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,C)) = multiply(multiply(D,inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,F)),B)),E)),C)),
inference(copy,[status(thm)],[c_8421]) ).
cnf(c_8422,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),D)) = multiply(inverse(multiply(E,multiply(B,inverse(multiply(inverse(A),inverse(multiply(C,multiply(inverse(C),C)))))))),multiply(E,D)),
inference(paramod,[status(thm)],[c_13,c_45]) ).
cnf(c_86,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))))),multiply(A,E)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),
inference(copy,[status(thm)],[c_8422]) ).
cnf(c_89,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_45,c_45]) ).
cnf(c_100,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),D)),inverse(multiply(multiply(B,C),multiply(inverse(multiply(E,C)),multiply(E,C))))))) = D,
inference(paramod,[status(thm)],[c_89,c_1]) ).
cnf(c_8423,plain,
multiply(inverse(A),multiply(B,C)) = multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(B,E)),A)),inverse(multiply(E,multiply(inverse(E),E))))))),multiply(D,C)),
inference(paramod,[status(thm)],[c_1,c_89]) ).
cnf(c_101,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,C)),D)),inverse(multiply(C,multiply(inverse(C),C))))))),multiply(A,E)) = multiply(inverse(D),multiply(B,E)),
inference(copy,[status(thm)],[c_8423]) ).
cnf(c_124,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_89,c_89]) ).
cnf(c_8424,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,A))),D)) = multiply(inverse(multiply(E,inverse(multiply(C,multiply(inverse(C),C))))),multiply(E,D)),
inference(paramod,[status(thm)],[c_46,c_89]) ).
cnf(c_141,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,C)) = multiply(D,multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),C)),
inference(copy,[status(thm)],[c_8424]) ).
cnf(c_8425,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,C)),V6)),A)),inverse(multiply(V6,multiply(inverse(V6),V6))))))),multiply(E,multiply(F,D))),
inference(paramod,[status(thm)],[c_1,c_124]) ).
cnf(c_8426,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(E,multiply(F,inverse(multiply(inverse(A),inverse(multiply(C,multiply(inverse(C),C)))))))),multiply(E,multiply(F,D))),
inference(paramod,[status(thm)],[c_4,c_8425]) ).
cnf(c_211,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_86,c_8426]) ).
cnf(c_8427,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,A))),inverse(multiply(F,multiply(inverse(F),F))))),multiply(inverse(multiply(V6,C)),multiply(V6,D))),
inference(paramod,[status(thm)],[c_46,c_211]) ).
cnf(c_354,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_46,c_8427]) ).
cnf(c_8428,plain,
multiply(inverse(multiply(A,B)),inverse(multiply(C,inverse(multiply(multiply(A,C),multiply(inverse(multiply(D,C)),multiply(D,C))))))) = inverse(multiply(B,multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_46,c_100]) ).
cnf(c_483,plain,
inverse(multiply(A,multiply(inverse(A),A))) = multiply(inverse(multiply(B,A)),inverse(multiply(C,inverse(multiply(multiply(B,C),multiply(inverse(multiply(D,C)),multiply(D,C))))))),
inference(copy,[status(thm)],[c_8428]) ).
cnf(c_745,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,A))),D)) = multiply(E,multiply(inverse(multiply(inverse(multiply(F,C)),multiply(F,E))),D)),
inference(paramod,[status(thm)],[c_46,c_141]) ).
cnf(c_8429,plain,
multiply(A,multiply(inverse(multiply(inverse(B),multiply(C,A))),D)) = multiply(E,multiply(inverse(multiply(inverse(multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(C,V6)),B)),inverse(multiply(V6,multiply(inverse(V6),V6))))))),multiply(F,E))),D)),
inference(paramod,[status(thm)],[c_1,c_745]) ).
cnf(c_864,plain,
multiply(A,multiply(inverse(multiply(inverse(B),multiply(C,A))),D)) = multiply(E,multiply(inverse(multiply(inverse(B),multiply(C,E))),D)),
inference(paramod,[status(thm)],[c_101,c_8429]) ).
cnf(c_878,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(C,multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,C))),F)))),inverse(multiply(B,multiply(inverse(B),B))))) = multiply(inverse(multiply(inverse(multiply(V6,E)),multiply(V6,A))),F),
inference(paramod,[status(thm)],[c_745,c_46]) ).
cnf(c_969,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(C,multiply(inverse(multiply(inverse(D),multiply(E,C))),F)))),inverse(multiply(B,multiply(inverse(B),B))))) = multiply(inverse(multiply(inverse(D),multiply(E,A))),F),
inference(paramod,[status(thm)],[c_864,c_46]) ).
cnf(c_1041,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_969,c_878]) ).
cnf(c_2469,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(multiply(B,multiply(inverse(B),B)))) = C,
inference(paramod,[status(thm)],[c_483,c_13]) ).
cnf(c_2771,plain,
multiply(inverse(A),A) = multiply(B,multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,B))),inverse(multiply(D,multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_2469,c_745]) ).
cnf(c_8430,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(B),B))))) = multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,inverse(multiply(inverse(multiply(C,F)),B))))),inverse(multiply(E,multiply(inverse(E),E))))),inverse(multiply(F,multiply(inverse(F),F)))))),
inference(paramod,[status(thm)],[c_2771,c_4]) ).
cnf(c_8431,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(B),B))))) = multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(C,F)),B)),inverse(multiply(F,multiply(inverse(F),F)))))),
inference(paramod,[status(thm)],[c_2469,c_8430]) ).
cnf(c_2854,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(B),B))))) = B,
inference(paramod,[status(thm)],[c_1,c_8431]) ).
cnf(c_3153,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_2469,c_2771]) ).
cnf(c_3168,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),inverse(multiply(B,multiply(inverse(D),D)))))) = C,
inference(paramod,[status(thm)],[c_3153,c_1]) ).
cnf(c_3184,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_3153,c_89]) ).
cnf(c_3185,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,A)),
inference(paramod,[status(thm)],[c_3153,c_89]) ).
cnf(c_8432,plain,
multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(inverse(multiply(C,D)),multiply(C,D))),
inference(paramod,[status(thm)],[c_3153,c_354]) ).
cnf(c_3211,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,C))) = multiply(A,multiply(inverse(D),D)),
inference(copy,[status(thm)],[c_8432]) ).
cnf(c_8433,plain,
multiply(inverse(multiply(inverse(A),A)),B) = multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,D))),B),
inference(paramod,[status(thm)],[c_3153,c_1041]) ).
cnf(c_3256,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,B))),C) = multiply(inverse(multiply(inverse(D),D)),C),
inference(copy,[status(thm)],[c_8433]) ).
cnf(c_3311,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),multiply(inverse(inverse(B)),inverse(B))))) = B,
inference(paramod,[status(thm)],[c_3153,c_2469]) ).
cnf(c_3339,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,D))),multiply(inverse(inverse(multiply(inverse(multiply(E,C)),multiply(E,D)))),inverse(multiply(inverse(multiply(E,C)),multiply(E,D)))))))) = inverse(multiply(inverse(multiply(E,C)),multiply(E,D))),
inference(paramod,[status(thm)],[c_1041,c_2854]) ).
cnf(c_3348,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_3153,c_2854]) ).
cnf(c_3351,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),
inference(paramod,[status(thm)],[c_3348,c_3339]) ).
cnf(c_3378,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_3153,c_3348]) ).
cnf(c_3496,plain,
multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_3153,c_3211]) ).
cnf(c_3533,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_3496,c_3153]) ).
cnf(c_8434,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))))) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_3533,c_3348]) ).
cnf(c_3632,plain,
inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(B),B)),
inference(paramod,[status(thm)],[c_3348,c_8434]) ).
cnf(c_3770,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),multiply(inverse(C),C)))) = B,
inference(paramod,[status(thm)],[c_3153,c_3311]) ).
cnf(c_3774,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_3533,c_3311]) ).
cnf(c_3777,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(C),C)))))) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_3632,c_3311]) ).
cnf(c_4247,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),D)))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_3184,c_3770]) ).
cnf(c_4264,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_4247,c_3777]) ).
cnf(c_4696,plain,
multiply(inverse(multiply(inverse(A),A)),B) = multiply(inverse(multiply(inverse(C),C)),B),
inference(paramod,[status(thm)],[c_3153,c_3256]) ).
cnf(c_5198,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),inverse(multiply(multiply(inverse(D),D),multiply(inverse(E),E)))))) = C,
inference(paramod,[status(thm)],[c_3533,c_3168]) ).
cnf(c_8435,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(A,multiply(inverse(C),C)))))) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_3774,c_3168]) ).
cnf(c_8436,plain,
multiply(inverse(A),A) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_3348,c_8435]) ).
cnf(c_5204,plain,
inverse(multiply(inverse(A),A)) = multiply(inverse(B),B),
inference(copy,[status(thm)],[c_8436]) ).
cnf(c_8437,plain,
multiply(multiply(inverse(A),A),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_5204,c_3153]) ).
cnf(c_5296,plain,
multiply(inverse(A),A) = multiply(multiply(inverse(B),B),multiply(inverse(C),C)),
inference(copy,[status(thm)],[c_8437]) ).
cnf(c_5325,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),multiply(inverse(C),C)))) = B,
inference(paramod,[status(thm)],[c_5204,c_3770]) ).
cnf(c_5329,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),inverse(multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_5204,c_3770]) ).
cnf(c_8438,plain,
multiply(multiply(inverse(A),A),B) = multiply(inverse(multiply(inverse(C),C)),B),
inference(paramod,[status(thm)],[c_5204,c_4696]) ).
cnf(c_5358,plain,
multiply(inverse(multiply(inverse(A),A)),B) = multiply(multiply(inverse(C),C),B),
inference(copy,[status(thm)],[c_8438]) ).
cnf(c_5374,plain,
inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_5204,c_5204]) ).
cnf(c_6323,plain,
multiply(inverse(multiply(inverse(A),inverse(multiply(B,multiply(inverse(C),C))))),D) = multiply(B,multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_3348,c_54]) ).
cnf(c_6549,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(B),B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_5296,c_3185]) ).
cnf(c_6553,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(multiply(inverse(B),B),C))) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),
inference(paramod,[status(thm)],[c_5296,c_3351]) ).
cnf(c_8439,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(multiply(inverse(V6),V6),multiply(A,E))),
inference(paramod,[status(thm)],[c_5358,c_124]) ).
cnf(c_6673,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(multiply(inverse(C),C),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(D,F)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(copy,[status(thm)],[c_8439]) ).
cnf(c_6724,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(multiply(inverse(C),C),D))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_5358,c_3351]) ).
cnf(c_6726,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(B),B),C)),D)),inverse(multiply(C,multiply(inverse(E),E)))))) = D,
inference(paramod,[status(thm)],[c_5358,c_3168]) ).
cnf(c_6729,plain,
multiply(multiply(inverse(A),A),B) = multiply(multiply(inverse(C),C),B),
inference(paramod,[status(thm)],[c_5204,c_5358]) ).
cnf(c_8440,plain,
multiply(multiply(A,multiply(inverse(multiply(inverse(B),B)),inverse(multiply(A,multiply(inverse(C),C))))),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_3348,c_6729]) ).
cnf(c_6773,plain,
multiply(multiply(inverse(A),A),B) = multiply(multiply(C,multiply(inverse(multiply(inverse(D),D)),inverse(multiply(C,multiply(inverse(E),E))))),B),
inference(copy,[status(thm)],[c_8440]) ).
cnf(c_6779,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_3378,c_6729]) ).
cnf(c_6780,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(multiply(inverse(D),D),B)),multiply(multiply(inverse(E),E),C)),
inference(paramod,[status(thm)],[c_6729,c_3184]) ).
cnf(c_6975,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_81,c_3770]) ).
cnf(c_6987,plain,
multiply(inverse(multiply(inverse(A),inverse(multiply(B,multiply(inverse(B),B))))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_3774,c_81]) ).
cnf(c_7003,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_81,c_3184]) ).
cnf(c_7015,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,multiply(inverse(multiply(inverse(multiply(C,D)),B)),E))) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_3184,c_81]) ).
cnf(c_8441,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,C)) = multiply(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(multiply(inverse(F),F))),inverse(multiply(inverse(F),F)))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_4264,c_81]) ).
cnf(c_7019,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,C)) = multiply(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_4264,c_8441]) ).
cnf(c_8442,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_5204,c_81]) ).
cnf(c_7078,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),inverse(multiply(C,multiply(inverse(C),C)))))),C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(copy,[status(thm)],[c_8442]) ).
cnf(c_7698,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),multiply(inverse(multiply(C,D)),E))))) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(D),D)))))))),
inference(paramod,[status(thm)],[c_86,c_3348]) ).
cnf(c_7709,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C)))),multiply(A,D)) = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_3533,c_86]) ).
cnf(c_7715,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))))),E) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_3770,c_86]) ).
cnf(c_8443,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,C)) = multiply(inverse(inverse(multiply(D,multiply(inverse(D),D)))),multiply(inverse(multiply(inverse(multiply(inverse(E),E)),D)),C)),
inference(paramod,[status(thm)],[c_3774,c_86]) ).
cnf(c_7716,plain,
multiply(inverse(inverse(multiply(A,multiply(inverse(A),A)))),multiply(inverse(multiply(inverse(multiply(inverse(B),B)),A)),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
inference(copy,[status(thm)],[c_8443]) ).
cnf(c_8444,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D)))))))))),multiply(A,E)) = multiply(inverse(C),multiply(inverse(multiply(inverse(F),F)),E)),
inference(paramod,[status(thm)],[c_3774,c_86]) ).
cnf(c_8445,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(D),D)))))))),multiply(A,E)) = multiply(inverse(C),multiply(inverse(multiply(inverse(F),F)),E)),
inference(paramod,[status(thm)],[c_4264,c_8444]) ).
cnf(c_7718,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),multiply(inverse(multiply(inverse(D),D)),C)),
inference(paramod,[status(thm)],[c_5329,c_8445]) ).
cnf(c_7804,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))))),multiply(multiply(inverse(E),E),F)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),F)),
inference(paramod,[status(thm)],[c_5358,c_86]) ).
cnf(c_7998,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),D)))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_3184,c_5325]) ).
cnf(c_8106,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(multiply(inverse(C),C),multiply(multiply(inverse(D),D),multiply(inverse(E),E))))))) = B,
inference(paramod,[status(thm)],[c_5374,c_3348]) ).
cnf(c_8137,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),inverse(multiply(multiply(inverse(C),C),multiply(inverse(D),D)))))) = B,
inference(paramod,[status(thm)],[c_5374,c_3770]) ).
cnf(c_8178,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(multiply(inverse(B),B),C)),inverse(multiply(multiply(inverse(D),D),multiply(inverse(E),E)))))) = C,
inference(paramod,[status(thm)],[c_5374,c_3168]) ).
cnf(c_8262,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),inverse(multiply(multiply(inverse(C),C),multiply(inverse(D),D)))))) = B,
inference(paramod,[status(thm)],[c_5374,c_5325]) ).
cnf(c_8269,plain,
multiply(inverse(multiply(inverse(A),A)),B) = B,
inference(paramod,[status(thm)],[c_8137,c_5198]) ).
cnf(c_8273,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_8262,c_8178]) ).
cnf(c_8446,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(multiply(inverse(C),C),multiply(inverse(E),E)))))) = B,
inference(paramod,[status(thm)],[c_8273,c_8106]) ).
cnf(c_8447,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(E),E))))) = B,
inference(paramod,[status(thm)],[c_8273,c_8446]) ).
cnf(c_8284,plain,
inverse(inverse(multiply(A,multiply(inverse(B),B)))) = A,
inference(paramod,[status(thm)],[c_8269,c_8447]) ).
cnf(c_8448,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(C),D))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_8269,c_7998]) ).
cnf(c_8288,plain,
inverse(multiply(inverse(A),B)) = multiply(inverse(B),A),
inference(paramod,[status(thm)],[c_8273,c_8448]) ).
cnf(c_8449,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))))),multiply(multiply(inverse(E),E),F)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),F)),
inference(paramod,[status(thm)],[c_8288,c_7804]) ).
cnf(c_8450,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,multiply(inverse(inverse(multiply(D,multiply(inverse(D),D)))),C)))),multiply(multiply(inverse(E),E),F)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),F)),
inference(paramod,[status(thm)],[c_8288,c_8449]) ).
cnf(c_8451,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,multiply(D,C)))),multiply(multiply(inverse(E),E),F)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),F)),
inference(paramod,[status(thm)],[c_8284,c_8450]) ).
cnf(c_8452,plain,
multiply(inverse(multiply(B,multiply(D,C))),multiply(multiply(inverse(E),E),F)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),F)),
inference(paramod,[status(thm)],[c_8273,c_8451]) ).
cnf(c_8300,plain,
multiply(inverse(multiply(A,multiply(B,C))),D) = multiply(inverse(C),multiply(inverse(multiply(A,B)),D)),
inference(paramod,[status(thm)],[c_8273,c_8452]) ).
cnf(c_8453,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),multiply(multiply(inverse(D),D),C)),
inference(paramod,[status(thm)],[c_8288,c_7718]) ).
cnf(c_8316,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_8273,c_8453]) ).
cnf(c_8454,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(inverse(B),B)),A)),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
inference(paramod,[status(thm)],[c_8284,c_7716]) ).
cnf(c_8455,plain,
multiply(A,multiply(inverse(multiply(multiply(inverse(B),B),A)),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
inference(paramod,[status(thm)],[c_8288,c_8454]) ).
cnf(c_8456,plain,
multiply(A,multiply(inverse(A),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
inference(paramod,[status(thm)],[c_8273,c_8455]) ).
cnf(c_8457,plain,
multiply(A,multiply(inverse(A),C)) = multiply(inverse(multiply(inverse(E),E)),C),
inference(paramod,[status(thm)],[c_8316,c_8456]) ).
cnf(c_8458,plain,
multiply(A,multiply(inverse(A),C)) = multiply(multiply(inverse(E),E),C),
inference(paramod,[status(thm)],[c_8288,c_8457]) ).
cnf(c_8317,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_8273,c_8458]) ).
cnf(c_8459,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))))),E) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_8288,c_7715]) ).
cnf(c_8460,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,inverse(multiply(inverse(C),inverse(D)))))),E) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_8317,c_8459]) ).
cnf(c_8461,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,multiply(inverse(inverse(D)),C)))),E) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_8288,c_8460]) ).
cnf(c_8462,plain,
multiply(inverse(multiply(B,multiply(inverse(inverse(D)),C))),E) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_8273,c_8461]) ).
cnf(c_8463,plain,
multiply(inverse(C),multiply(inverse(multiply(B,inverse(inverse(D)))),E)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_8300,c_8462]) ).
cnf(c_8464,plain,
multiply(inverse(C),multiply(inverse(multiply(B,inverse(inverse(D)))),E)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),multiply(inverse(multiply(inverse(F),F)),E))),
inference(paramod,[status(thm)],[c_8288,c_8463]) ).
cnf(c_8465,plain,
multiply(inverse(C),multiply(inverse(multiply(B,inverse(inverse(D)))),E)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),multiply(multiply(inverse(F),F),E))),
inference(paramod,[status(thm)],[c_8288,c_8464]) ).
cnf(c_8318,plain,
multiply(inverse(A),multiply(inverse(multiply(B,inverse(inverse(C)))),D)) = multiply(inverse(A),multiply(inverse(multiply(B,C)),D)),
inference(paramod,[status(thm)],[c_8273,c_8465]) ).
cnf(c_8466,plain,
multiply(inverse(multiply(A,multiply(multiply(inverse(B),B),multiply(inverse(C),C)))),multiply(A,D)) = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_8288,c_7709]) ).
cnf(c_8467,plain,
multiply(inverse(multiply(A,multiply(inverse(C),C))),multiply(A,D)) = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_8273,c_8466]) ).
cnf(c_8468,plain,
multiply(inverse(multiply(inverse(C),C)),D) = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_8316,c_8467]) ).
cnf(c_8469,plain,
multiply(multiply(inverse(C),C),D) = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_8288,c_8468]) ).
cnf(c_8470,plain,
D = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_8273,c_8469]) ).
cnf(c_8471,plain,
D = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(F)))),F)),D)),
inference(paramod,[status(thm)],[c_8317,c_8470]) ).
cnf(c_8472,plain,
D = multiply(inverse(E),multiply(inverse(multiply(inverse(multiply(inverse(inverse(F)),E)),F)),D)),
inference(paramod,[status(thm)],[c_8288,c_8471]) ).
cnf(c_8473,plain,
D = multiply(inverse(E),multiply(inverse(multiply(multiply(inverse(E),inverse(F)),F)),D)),
inference(paramod,[status(thm)],[c_8288,c_8472]) ).
cnf(c_8321,plain,
multiply(inverse(A),multiply(inverse(multiply(multiply(inverse(A),inverse(B)),B)),C)) = C,
inference(copy,[status(thm)],[c_8473]) ).
cnf(c_8474,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),multiply(inverse(multiply(C,D)),E))))) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(D),D)))))))),
inference(paramod,[status(thm)],[c_8288,c_7698]) ).
cnf(c_8475,plain,
inverse(multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(C,D)),E)),B))) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(D),D)))))))),
inference(paramod,[status(thm)],[c_8288,c_8474]) ).
cnf(c_8476,plain,
inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(E),multiply(C,D)),B))) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(D),D)))))))),
inference(paramod,[status(thm)],[c_8288,c_8475]) ).
cnf(c_8477,plain,
inverse(multiply(multiply(inverse(E),multiply(C,D)),B)) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(D),D)))))))),
inference(paramod,[status(thm)],[c_8273,c_8476]) ).
cnf(c_8478,plain,
inverse(multiply(multiply(inverse(E),multiply(C,D)),B)) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(D)))))),
inference(paramod,[status(thm)],[c_8317,c_8477]) ).
cnf(c_8479,plain,
inverse(multiply(multiply(inverse(E),multiply(C,D)),B)) = inverse(multiply(inverse(E),multiply(C,multiply(inverse(inverse(D)),B)))),
inference(paramod,[status(thm)],[c_8288,c_8478]) ).
cnf(c_8480,plain,
inverse(multiply(multiply(inverse(E),multiply(C,D)),B)) = multiply(inverse(multiply(C,multiply(inverse(inverse(D)),B))),E),
inference(paramod,[status(thm)],[c_8288,c_8479]) ).
cnf(c_8481,plain,
inverse(multiply(multiply(inverse(E),multiply(C,D)),B)) = multiply(inverse(B),multiply(inverse(multiply(C,inverse(inverse(D)))),E)),
inference(paramod,[status(thm)],[c_8300,c_8480]) ).
cnf(c_8324,plain,
inverse(multiply(multiply(inverse(A),multiply(B,C)),D)) = multiply(inverse(D),multiply(inverse(multiply(B,C)),A)),
inference(paramod,[status(thm)],[c_8318,c_8481]) ).
cnf(c_8482,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),inverse(multiply(C,multiply(inverse(C),C)))))),C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_8288,c_7078]) ).
cnf(c_8483,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),inverse(C)))),C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_8317,c_8482]) ).
cnf(c_8484,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),B)),C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_8288,c_8483]) ).
cnf(c_8485,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(B),inverse(C)),C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_8288,c_8484]) ).
cnf(c_8486,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(multiply(inverse(D),multiply(multiply(inverse(B),inverse(C)),C)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_8288,c_8485]) ).
cnf(c_8487,plain,
multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),multiply(inverse(multiply(multiply(inverse(B),inverse(C)),C)),D)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_8324,c_8486]) ).
cnf(c_8488,plain,
multiply(multiply(inverse(A),A),multiply(D,E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_8321,c_8487]) ).
cnf(c_8489,plain,
multiply(D,E) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_8273,c_8488]) ).
cnf(c_8490,plain,
multiply(D,E) = multiply(inverse(multiply(F,inverse(D))),multiply(F,E)),
inference(paramod,[status(thm)],[c_8317,c_8489]) ).
cnf(c_8491,plain,
multiply(D,E) = multiply(inverse(inverse(D)),E),
inference(paramod,[status(thm)],[c_8316,c_8490]) ).
cnf(c_8335,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(copy,[status(thm)],[c_8491]) ).
cnf(c_8492,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,C)) = multiply(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8317,c_7019]) ).
cnf(c_8493,plain,
multiply(inverse(inverse(B)),C) = multiply(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8316,c_8492]) ).
cnf(c_8494,plain,
multiply(B,C) = multiply(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8335,c_8493]) ).
cnf(c_8495,plain,
multiply(B,C) = multiply(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8288,c_8494]) ).
cnf(c_8496,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8288,c_8495]) ).
cnf(c_8497,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(E),inverse(multiply(multiply(inverse(F),F),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8288,c_8496]) ).
cnf(c_8498,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(E),inverse(multiply(inverse(F),F))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8273,c_8497]) ).
cnf(c_8499,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(E),multiply(inverse(F),F)))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8288,c_8498]) ).
cnf(c_8500,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),multiply(inverse(multiply(inverse(F),F)),E)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8288,c_8499]) ).
cnf(c_8501,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),multiply(multiply(inverse(F),F),E)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8288,c_8500]) ).
cnf(c_8502,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),E),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8273,c_8501]) ).
cnf(c_8503,plain,
multiply(B,C) = multiply(E,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_8273,c_8502]) ).
cnf(c_8504,plain,
multiply(B,C) = multiply(E,multiply(inverse(multiply(inverse(multiply(multiply(inverse(F),F),B)),E)),C)),
inference(paramod,[status(thm)],[c_8288,c_8503]) ).
cnf(c_8505,plain,
multiply(B,C) = multiply(E,multiply(inverse(multiply(inverse(B),E)),C)),
inference(paramod,[status(thm)],[c_8273,c_8504]) ).
cnf(c_8506,plain,
multiply(B,C) = multiply(E,multiply(multiply(inverse(E),B),C)),
inference(paramod,[status(thm)],[c_8288,c_8505]) ).
cnf(c_8342,plain,
multiply(A,multiply(multiply(inverse(A),B),C)) = multiply(B,C),
inference(copy,[status(thm)],[c_8506]) ).
cnf(c_8507,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(multiply(inverse(multiply(C,D)),B)),E))) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_8317,c_7015]) ).
cnf(c_8508,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(multiply(inverse(B),multiply(C,D)),E))) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_8288,c_8507]) ).
cnf(c_8509,plain,
multiply(inverse(inverse(B)),multiply(multiply(inverse(B),multiply(C,D)),E)) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_8316,c_8508]) ).
cnf(c_8510,plain,
multiply(B,multiply(multiply(inverse(B),multiply(C,D)),E)) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_8335,c_8509]) ).
cnf(c_8511,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_8342,c_8510]) ).
cnf(c_8512,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(D)))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_8317,c_8511]) ).
cnf(c_8513,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,multiply(inverse(inverse(D)),F)),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_8288,c_8512]) ).
cnf(c_8514,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,multiply(D,F)),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_8335,c_8513]) ).
cnf(c_8515,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,multiply(D,F)),multiply(multiply(inverse(V6),V6),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_8288,c_8514]) ).
cnf(c_8516,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,multiply(D,F)),multiply(inverse(F),E)),
inference(paramod,[status(thm)],[c_8273,c_8515]) ).
cnf(c_8343,plain,
multiply(multiply(A,multiply(B,C)),multiply(inverse(C),D)) = multiply(multiply(A,B),D),
inference(copy,[status(thm)],[c_8516]) ).
cnf(c_8517,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_8288,c_7003]) ).
cnf(c_8518,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,inverse(multiply(inverse(C),inverse(D)))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_8317,c_8517]) ).
cnf(c_8519,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,multiply(inverse(inverse(D)),C)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_8288,c_8518]) ).
cnf(c_8520,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,multiply(D,C)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_8335,c_8519]) ).
cnf(c_8521,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,multiply(D,C)),multiply(inverse(multiply(multiply(inverse(E),multiply(B,D)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_8288,c_8520]) ).
cnf(c_8522,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_8324,c_8521]) ).
cnf(c_8523,plain,
multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F)) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_8273,c_8522]) ).
cnf(c_8524,plain,
multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F)) = multiply(inverse(multiply(V6,multiply(V7,inverse(E)))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_8317,c_8523]) ).
cnf(c_8525,plain,
multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F)) = multiply(inverse(multiply(V7,inverse(E))),multiply(V7,F)),
inference(paramod,[status(thm)],[c_8316,c_8524]) ).
cnf(c_8526,plain,
multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F)) = multiply(inverse(inverse(E)),F),
inference(paramod,[status(thm)],[c_8316,c_8525]) ).
cnf(c_8351,plain,
multiply(multiply(A,multiply(B,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(A,B)),D)),E)) = multiply(D,E),
inference(paramod,[status(thm)],[c_8335,c_8526]) ).
cnf(c_8527,plain,
multiply(inverse(multiply(inverse(A),inverse(B))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_8317,c_6987]) ).
cnf(c_8528,plain,
multiply(multiply(inverse(inverse(B)),A),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_8288,c_8527]) ).
cnf(c_8529,plain,
multiply(multiply(B,A),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_8335,c_8528]) ).
cnf(c_8530,plain,
multiply(multiply(B,A),multiply(multiply(inverse(C),C),inverse(multiply(inverse(D),D)))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_8288,c_8529]) ).
cnf(c_8531,plain,
multiply(multiply(B,A),multiply(multiply(inverse(C),C),multiply(inverse(D),D))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_8288,c_8530]) ).
cnf(c_8532,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_8273,c_8531]) ).
cnf(c_8533,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(V6)))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_8317,c_8532]) ).
cnf(c_8534,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,multiply(inverse(inverse(V6)),F)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_8288,c_8533]) ).
cnf(c_8535,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,multiply(V6,F)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_8335,c_8534]) ).
cnf(c_8536,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,multiply(V6,F)),multiply(inverse(multiply(multiply(inverse(B),multiply(E,V6)),F)),A)),
inference(paramod,[status(thm)],[c_8288,c_8535]) ).
cnf(c_8537,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,multiply(V6,F)),multiply(multiply(inverse(F),multiply(inverse(multiply(E,V6)),B)),A)),
inference(paramod,[status(thm)],[c_8324,c_8536]) ).
cnf(c_8356,plain,
multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(A,B),
inference(paramod,[status(thm)],[c_8351,c_8537]) ).
cnf(c_8538,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_8288,c_6975]) ).
cnf(c_8539,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,inverse(multiply(inverse(C),inverse(D)))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_8317,c_8538]) ).
cnf(c_8540,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,multiply(inverse(inverse(D)),C)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_8288,c_8539]) ).
cnf(c_8541,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,multiply(D,C)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_8335,c_8540]) ).
cnf(c_8542,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,multiply(D,C)),multiply(inverse(multiply(multiply(inverse(E),multiply(B,D)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_8288,c_8541]) ).
cnf(c_8543,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_8324,c_8542]) ).
cnf(c_8544,plain,
multiply(multiply(inverse(A),A),inverse(multiply(E,F))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_8351,c_8543]) ).
cnf(c_8545,plain,
inverse(multiply(E,F)) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_8273,c_8544]) ).
cnf(c_8358,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(paramod,[status(thm)],[c_8317,c_8545]) ).
cnf(c_8546,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(B),C)) = multiply(inverse(multiply(multiply(inverse(D),D),B)),multiply(multiply(inverse(E),E),C)),
inference(paramod,[status(thm)],[c_8358,c_6780]) ).
cnf(c_8547,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(B),C)) = multiply(inverse(B),multiply(multiply(inverse(E),E),C)),
inference(paramod,[status(thm)],[c_8273,c_8546]) ).
cnf(c_8387,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(B),C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_8273,c_8547]) ).
cnf(c_8548,plain,
multiply(multiply(inverse(multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(inverse(B),B)))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_8358,c_6779]) ).
cnf(c_8549,plain,
multiply(multiply(inverse(multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(B),inverse(inverse(B))))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_8358,c_8548]) ).
cnf(c_8550,plain,
multiply(multiply(inverse(multiply(inverse(B),inverse(inverse(B)))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_8387,c_8549]) ).
cnf(c_8551,plain,
multiply(multiply(multiply(inverse(inverse(inverse(B))),inverse(inverse(B))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_8358,c_8550]) ).
cnf(c_8552,plain,
multiply(multiply(multiply(inverse(B),inverse(inverse(B))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_8335,c_8551]) ).
cnf(c_8553,plain,
multiply(multiply(inverse(B),inverse(inverse(B))),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_8356,c_8552]) ).
cnf(c_8388,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),B) = B,
inference(paramod,[status(thm)],[c_8273,c_8553]) ).
cnf(c_8554,plain,
B = multiply(multiply(C,multiply(inverse(multiply(inverse(D),D)),inverse(multiply(C,multiply(inverse(E),E))))),B),
inference(paramod,[status(thm)],[c_8273,c_6773]) ).
cnf(c_8555,plain,
B = multiply(multiply(C,multiply(multiply(inverse(D),inverse(inverse(D))),inverse(multiply(C,multiply(inverse(E),E))))),B),
inference(paramod,[status(thm)],[c_8358,c_8554]) ).
cnf(c_8556,plain,
B = multiply(multiply(C,multiply(multiply(inverse(D),inverse(inverse(D))),multiply(inverse(multiply(inverse(E),E)),inverse(C)))),B),
inference(paramod,[status(thm)],[c_8358,c_8555]) ).
cnf(c_8557,plain,
B = multiply(multiply(C,multiply(multiply(inverse(D),inverse(inverse(D))),multiply(multiply(inverse(E),inverse(inverse(E))),inverse(C)))),B),
inference(paramod,[status(thm)],[c_8358,c_8556]) ).
cnf(c_8558,plain,
B = multiply(multiply(C,multiply(multiply(inverse(D),inverse(inverse(D))),inverse(C))),B),
inference(paramod,[status(thm)],[c_8388,c_8557]) ).
cnf(c_8559,plain,
B = multiply(multiply(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_8388,c_8558]) ).
cnf(c_8389,plain,
multiply(multiply(A,inverse(A)),B) = B,
inference(copy,[status(thm)],[c_8559]) ).
cnf(c_8560,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(B),B),C)),D)),inverse(multiply(C,multiply(inverse(E),E)))))) = D,
inference(paramod,[status(thm)],[c_8358,c_6726]) ).
cnf(c_8561,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(inverse(multiply(inverse(C),D)),inverse(multiply(C,multiply(inverse(E),E)))))) = D,
inference(paramod,[status(thm)],[c_8273,c_8560]) ).
cnf(c_8562,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(multiply(inverse(D),inverse(inverse(C))),inverse(multiply(C,multiply(inverse(E),E)))))) = D,
inference(paramod,[status(thm)],[c_8358,c_8561]) ).
cnf(c_8563,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(multiply(inverse(D),inverse(inverse(C))),multiply(inverse(multiply(inverse(E),E)),inverse(C))))) = D,
inference(paramod,[status(thm)],[c_8358,c_8562]) ).
cnf(c_8564,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(multiply(inverse(D),inverse(inverse(C))),multiply(multiply(inverse(E),inverse(inverse(E))),inverse(C))))) = D,
inference(paramod,[status(thm)],[c_8358,c_8563]) ).
cnf(c_8565,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(multiply(inverse(D),inverse(inverse(C))),inverse(C)))) = D,
inference(paramod,[status(thm)],[c_8389,c_8564]) ).
cnf(c_8566,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(inverse(C)))))) = D,
inference(paramod,[status(thm)],[c_8358,c_8565]) ).
cnf(c_8567,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(inverse(C)),multiply(inverse(inverse(inverse(C))),inverse(inverse(D))))) = D,
inference(paramod,[status(thm)],[c_8358,c_8566]) ).
cnf(c_8568,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(inverse(C)),multiply(inverse(C),inverse(inverse(D))))) = D,
inference(paramod,[status(thm)],[c_8335,c_8567]) ).
cnf(c_8569,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(C,multiply(inverse(C),inverse(inverse(D))))) = D,
inference(paramod,[status(thm)],[c_8335,c_8568]) ).
cnf(c_8570,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(inverse(D))) = D,
inference(paramod,[status(thm)],[c_8317,c_8569]) ).
cnf(c_8390,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_8389,c_8570]) ).
cnf(c_8571,plain,
inverse(multiply(inverse(multiply(multiply(inverse(A),inverse(inverse(A))),B)),multiply(multiply(inverse(C),C),D))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_8358,c_6724]) ).
cnf(c_8572,plain,
inverse(multiply(inverse(multiply(multiply(inverse(A),A),B)),multiply(multiply(inverse(C),C),D))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_8390,c_8571]) ).
cnf(c_8573,plain,
inverse(multiply(inverse(B),multiply(multiply(inverse(C),C),D))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_8273,c_8572]) ).
cnf(c_8574,plain,
inverse(multiply(inverse(B),D)) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_8273,c_8573]) ).
cnf(c_8575,plain,
multiply(inverse(D),inverse(inverse(B))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_8358,c_8574]) ).
cnf(c_8576,plain,
multiply(inverse(D),B) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_8390,c_8575]) ).
cnf(c_8577,plain,
multiply(inverse(D),B) = inverse(multiply(multiply(inverse(B),inverse(E)),multiply(E,D))),
inference(paramod,[status(thm)],[c_8358,c_8576]) ).
cnf(c_8578,plain,
multiply(inverse(D),B) = multiply(inverse(multiply(E,D)),inverse(multiply(inverse(B),inverse(E)))),
inference(paramod,[status(thm)],[c_8358,c_8577]) ).
cnf(c_8579,plain,
multiply(inverse(D),B) = multiply(multiply(inverse(D),inverse(E)),inverse(multiply(inverse(B),inverse(E)))),
inference(paramod,[status(thm)],[c_8358,c_8578]) ).
cnf(c_8580,plain,
multiply(inverse(D),B) = multiply(multiply(inverse(D),inverse(E)),multiply(inverse(inverse(E)),inverse(inverse(B)))),
inference(paramod,[status(thm)],[c_8358,c_8579]) ).
cnf(c_8581,plain,
multiply(inverse(D),B) = multiply(multiply(inverse(D),inverse(E)),multiply(E,inverse(inverse(B)))),
inference(paramod,[status(thm)],[c_8390,c_8580]) ).
cnf(c_8582,plain,
multiply(inverse(D),B) = multiply(multiply(inverse(D),inverse(E)),multiply(E,B)),
inference(paramod,[status(thm)],[c_8390,c_8581]) ).
cnf(c_8391,plain,
multiply(multiply(inverse(A),inverse(B)),multiply(B,C)) = multiply(inverse(A),C),
inference(copy,[status(thm)],[c_8582]) ).
cnf(c_8583,plain,
multiply(inverse(multiply(multiply(inverse(A),inverse(inverse(A))),B)),multiply(multiply(inverse(C),C),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(D,F)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_8358,c_6673]) ).
cnf(c_8584,plain,
multiply(inverse(multiply(multiply(inverse(A),A),B)),multiply(multiply(inverse(C),C),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(D,F)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_8390,c_8583]) ).
cnf(c_8585,plain,
multiply(inverse(B),multiply(multiply(inverse(C),C),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(D,F)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_8273,c_8584]) ).
cnf(c_8586,plain,
multiply(inverse(B),multiply(D,E)) = multiply(inverse(multiply(inverse(multiply(D,F)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_8273,c_8585]) ).
cnf(c_8587,plain,
multiply(inverse(B),multiply(D,E)) = multiply(inverse(multiply(multiply(inverse(F),inverse(D)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_8358,c_8586]) ).
cnf(c_8588,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),inverse(multiply(inverse(F),inverse(D)))),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_8358,c_8587]) ).
cnf(c_8589,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),multiply(inverse(inverse(D)),inverse(inverse(F)))),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_8358,c_8588]) ).
cnf(c_8590,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),multiply(D,inverse(inverse(F)))),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_8390,c_8589]) ).
cnf(c_8591,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),multiply(D,F)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_8390,c_8590]) ).
cnf(c_8592,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),multiply(D,F)),multiply(multiply(inverse(F),inverse(V6)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_8358,c_8591]) ).
cnf(c_8593,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),multiply(D,F)),multiply(inverse(F),E)),
inference(paramod,[status(thm)],[c_8391,c_8592]) ).
cnf(c_8594,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),D),E),
inference(paramod,[status(thm)],[c_8343,c_8593]) ).
cnf(c_8399,plain,
multiply(multiply(inverse(A),B),C) = multiply(inverse(A),multiply(B,C)),
inference(copy,[status(thm)],[c_8594]) ).
cnf(c_8595,plain,
inverse(multiply(multiply(inverse(A),inverse(inverse(A))),multiply(multiply(inverse(B),B),C))) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),
inference(paramod,[status(thm)],[c_8358,c_6553]) ).
cnf(c_8596,plain,
inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),C))) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),
inference(paramod,[status(thm)],[c_8390,c_8595]) ).
cnf(c_8597,plain,
inverse(multiply(multiply(inverse(A),A),C)) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),
inference(paramod,[status(thm)],[c_8273,c_8596]) ).
cnf(c_8598,plain,
inverse(C) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),
inference(paramod,[status(thm)],[c_8273,c_8597]) ).
cnf(c_8599,plain,
inverse(C) = inverse(multiply(multiply(inverse(multiply(inverse(E),E)),inverse(D)),multiply(D,C))),
inference(paramod,[status(thm)],[c_8358,c_8598]) ).
cnf(c_8600,plain,
inverse(C) = inverse(multiply(multiply(multiply(inverse(E),inverse(inverse(E))),inverse(D)),multiply(D,C))),
inference(paramod,[status(thm)],[c_8358,c_8599]) ).
cnf(c_8601,plain,
inverse(C) = inverse(multiply(multiply(multiply(inverse(E),E),inverse(D)),multiply(D,C))),
inference(paramod,[status(thm)],[c_8390,c_8600]) ).
cnf(c_8602,plain,
inverse(C) = inverse(multiply(inverse(D),multiply(D,C))),
inference(paramod,[status(thm)],[c_8273,c_8601]) ).
cnf(c_8603,plain,
inverse(C) = multiply(inverse(multiply(D,C)),inverse(inverse(D))),
inference(paramod,[status(thm)],[c_8358,c_8602]) ).
cnf(c_8604,plain,
inverse(C) = multiply(multiply(inverse(C),inverse(D)),inverse(inverse(D))),
inference(paramod,[status(thm)],[c_8358,c_8603]) ).
cnf(c_8605,plain,
inverse(C) = multiply(multiply(inverse(C),inverse(D)),D),
inference(paramod,[status(thm)],[c_8390,c_8604]) ).
cnf(c_8606,plain,
inverse(C) = multiply(inverse(C),multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_8399,c_8605]) ).
cnf(c_8406,plain,
multiply(inverse(A),multiply(inverse(B),B)) = inverse(A),
inference(copy,[status(thm)],[c_8606]) ).
cnf(c_8607,plain,
multiply(inverse(inverse(A)),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_8406,c_6549]) ).
cnf(c_8608,plain,
multiply(A,multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_8390,c_8607]) ).
cnf(c_8609,plain,
multiply(A,multiply(inverse(C),C)) = multiply(multiply(inverse(D),inverse(inverse(D))),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_8358,c_8608]) ).
cnf(c_8610,plain,
multiply(A,multiply(inverse(C),C)) = multiply(multiply(inverse(D),D),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_8390,c_8609]) ).
cnf(c_8611,plain,
multiply(A,multiply(inverse(C),C)) = multiply(multiply(inverse(D),D),A),
inference(paramod,[status(thm)],[c_8273,c_8610]) ).
cnf(c_8407,plain,
multiply(A,multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_8273,c_8611]) ).
cnf(c_8612,plain,
multiply(inverse(multiply(inverse(A),inverse(B))),D) = multiply(B,multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8407,c_6323]) ).
cnf(c_8613,plain,
multiply(multiply(inverse(inverse(B)),inverse(inverse(A))),D) = multiply(B,multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8358,c_8612]) ).
cnf(c_8614,plain,
multiply(multiply(B,inverse(inverse(A))),D) = multiply(B,multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8390,c_8613]) ).
cnf(c_8615,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8390,c_8614]) ).
cnf(c_8616,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),inverse(inverse(E))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8358,c_8615]) ).
cnf(c_8617,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8390,c_8616]) ).
cnf(c_8618,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(inverse(A))),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8358,c_8617]) ).
cnf(c_8619,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(multiply(inverse(F),A),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8390,c_8618]) ).
cnf(c_8620,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(F),multiply(A,D))),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8399,c_8619]) ).
cnf(c_8621,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(multiply(inverse(multiply(A,D)),inverse(inverse(F))),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8358,c_8620]) ).
cnf(c_8622,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(multiply(multiply(inverse(D),inverse(A)),inverse(inverse(F))),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8358,c_8621]) ).
cnf(c_8623,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(multiply(multiply(inverse(D),inverse(A)),F),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8390,c_8622]) ).
cnf(c_8624,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(multiply(inverse(D),multiply(inverse(A),F)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_8399,c_8623]) ).
cnf(c_8625,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(multiply(inverse(D),multiply(inverse(A),F)),inverse(F))))),
inference(paramod,[status(thm)],[c_8317,c_8624]) ).
cnf(c_8626,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(D),multiply(multiply(inverse(A),F),inverse(F)))))),
inference(paramod,[status(thm)],[c_8399,c_8625]) ).
cnf(c_8627,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(D),multiply(inverse(A),multiply(F,inverse(F))))))),
inference(paramod,[status(thm)],[c_8399,c_8626]) ).
cnf(c_8628,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(inverse(multiply(inverse(A),multiply(F,inverse(F)))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_8358,c_8627]) ).
cnf(c_8629,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(multiply(inverse(multiply(F,inverse(F))),inverse(inverse(A))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_8358,c_8628]) ).
cnf(c_8630,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(multiply(multiply(inverse(inverse(F)),inverse(F)),inverse(inverse(A))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_8358,c_8629]) ).
cnf(c_8631,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(multiply(multiply(F,inverse(F)),inverse(inverse(A))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_8390,c_8630]) ).
cnf(c_8632,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(multiply(multiply(F,inverse(F)),A),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_8390,c_8631]) ).
cnf(c_8633,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(A,inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_8389,c_8632]) ).
cnf(c_8634,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(A,D))),
inference(paramod,[status(thm)],[c_8390,c_8633]) ).
cnf(c_8415,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_8273,c_8634]) ).
cnf(c_8416,plain,
$false,
inference(resolve,[status(thm)],[c_8415,c_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP405-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n003.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Fri Sep 25 14:53:53 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 454025 was started by sandbox on n003,
% 0.18/0.45 % Fri Sep 25 14:53:53 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/0.46
% 0.18/0.46 % From the command line: assign(max_seconds, 300).
% 33.63/5.31
% 33.63/5.31 % SZS status Unsatisfiable for theBenchmark
% 33.63/5.31
% 33.63/5.31 % Proof 1 at 4.17 (+ 0.63) seconds.
% 33.63/5.31 % Length of proof is 107.
% 33.63/5.31 % Level of proof is 35.
% 33.63/5.31 % Maximum clause weight is 63.000.
% 33.63/5.31 % Given clauses 86.
% 33.63/5.31
% 33.63/5.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------