↑ Up

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

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Prover9---2026-6A
% Problem  : GRP414-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 : n008.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:09 AM UTC 2026

% Result   : Unsatisfiable 15.34s 2.42s
% Output   : CNFRefutation 15.34s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   78
%            Number of leaves      :    2
% Syntax   : Number of formulae    :  346 ( 346 unt;   0 def)
%            Number of atoms       :  346 ( 345 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :    2 (   2   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    4 (   1 avg)
%            Maximal term depth    :   17 (   3 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :    5 (   5 usr;   3 con; 0-2 aty)
%            Number of variables   : 1561 (   0 sgn   3   !;   0   ?)

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

cnf(c_1,plain,
    multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(A,inverse(B))),C))),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(multiply(multiply(inverse(B),B),inverse(C)),B))) = inverse(multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),inverse(D))),C))),D)),
    inference(paramod,[status(thm)],[c_1,c_1]) ).

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

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

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

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

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

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

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

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

cnf(c_2119,plain,
    inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(multiply(E,D))))) = inverse(multiply(multiply(multiply(inverse(F),F),inverse(multiply(inverse(multiply(multiply(inverse(D),D),inverse(F))),E))),F)),
    inference(paramod,[status(thm)],[c_1,c_2118]) ).

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

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

cnf(c_2121,plain,
    multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(F))) = multiply(inverse(multiply(multiply(inverse(D),D),inverse(B))),multiply(multiply(inverse(D),D),inverse(F))),
    inference(paramod,[status(thm)],[c_1,c_2120]) ).

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

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

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

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

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

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

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

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

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

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

cnf(c_30,plain,
    inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(A))),multiply(B,C)))),A)) = C,
    inference(paramod,[status(thm)],[c_26,c_2126]) ).

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

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

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

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

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

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

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

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

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

cnf(c_66,plain,
    multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
    inference(paramod,[status(thm)],[c_30,c_2130]) ).

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

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

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

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

cnf(c_83,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_66,c_66]) ).

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

cnf(c_2133,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(inverse(multiply(A,inverse(V6))),C)),multiply(inverse(multiply(D,inverse(V6))),E)),
    inference(paramod,[status(thm)],[c_52,c_2132]) ).

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

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

cnf(c_86,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_70,c_2134]) ).

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

cnf(c_89,plain,
    inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),
    inference(paramod,[status(thm)],[c_75,c_2135]) ).

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

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

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

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

cnf(c_128,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_51,c_2136]) ).

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

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

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

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

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

cnf(c_162,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_30,c_2138]) ).

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

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

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

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

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

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

cnf(c_2141,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(F,inverse(E))),multiply(F,B)))),E)))),V6)) = multiply(inverse(multiply(inverse(multiply(A,V7)),C)),multiply(inverse(multiply(D,V7)),V6)),
    inference(paramod,[status(thm)],[c_30,c_85]) ).

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

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

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

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

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

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

cnf(c_500,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),D)),multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),inverse(multiply(inverse(multiply(F,inverse(V6))),multiply(F,inverse(multiply(V7,V6))))))) = multiply(inverse(multiply(multiply(inverse(V6),V6),D)),V7),
    inference(paramod,[status(thm)],[c_86,c_29]) ).

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

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

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

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

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

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

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

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

cnf(c_2148,plain,
    multiply(inverse(C),C) = multiply(inverse(multiply(D,E)),multiply(D,E)),
    inference(paramod,[status(thm)],[c_8,c_2147]) ).

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

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

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

cnf(c_622,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(multiply(inverse(C),C),inverse(B))),D))),B))) = D,
    inference(paramod,[status(thm)],[c_584,c_2149]) ).

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

cnf(c_2151,plain,
    E = multiply(multiply(inverse(F),F),inverse(multiply(inverse(multiply(V6,inverse(D))),multiply(V6,inverse(multiply(E,D)))))),
    inference(paramod,[status(thm)],[c_622,c_2150]) ).

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

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

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

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

cnf(c_706,plain,
    multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))),A) = A,
    inference(paramod,[status(thm)],[c_5,c_2153]) ).

cnf(c_813,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,B))),C)),multiply(inverse(multiply(D,E)),multiply(D,F))) = multiply(inverse(multiply(inverse(multiply(inverse(E),V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
    inference(paramod,[status(thm)],[c_581,c_136]) ).

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

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

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

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

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

cnf(c_916,plain,
    inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,D)))),C)) = D,
    inference(paramod,[status(thm)],[c_702,c_30]) ).

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

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

cnf(c_1059,plain,
    multiply(inverse(A),multiply(inverse(B),B)) = multiply(inverse(A),multiply(inverse(C),C)),
    inference(paramod,[status(thm)],[c_51,c_2154]) ).

cnf(c_1144,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
    inference(paramod,[status(thm)],[c_1059,c_702]) ).

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

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

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

cnf(c_1263,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),F)) = multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,C))),multiply(inverse(multiply(D,V7)),F)),
    inference(paramod,[status(thm)],[c_1144,c_99]) ).

cnf(c_2155,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(multiply(C,multiply(inverse(D),D))),multiply(C,E))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),V6)),B)),multiply(inverse(multiply(V7,V6)),multiply(V7,E))),
    inference(paramod,[status(thm)],[c_1144,c_136]) ).

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

cnf(c_1273,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),E)),F))) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
    inference(paramod,[status(thm)],[c_1144,c_136]) ).

cnf(c_1331,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,F))) = multiply(inverse(multiply(V6,multiply(V7,C))),multiply(V6,multiply(V7,F))),
    inference(paramod,[status(thm)],[c_1144,c_97]) ).

cnf(c_1343,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1144,c_97]) ).

cnf(c_1344,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(E),C))),multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1144,c_97]) ).

cnf(c_1376,plain,
    multiply(inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))),C)),A) = multiply(inverse(multiply(D,C)),multiply(D,A)),
    inference(paramod,[status(thm)],[c_706,c_66]) ).

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

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

cnf(c_1387,plain,
    inverse(multiply(inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))),C)),A)) = inverse(multiply(inverse(multiply(D,C)),multiply(D,A))),
    inference(paramod,[status(thm)],[c_706,c_89]) ).

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

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

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

cnf(c_1448,plain,
    multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))),C) = C,
    inference(paramod,[status(thm)],[c_702,c_706]) ).

cnf(c_2158,plain,
    multiply(A,multiply(inverse(D),B)) = multiply(A,multiply(inverse(multiply(E,D)),multiply(E,B))),
    inference(paramod,[status(thm)],[c_1448,c_1398]) ).

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

cnf(c_2159,plain,
    multiply(inverse(D),multiply(A,B)) = multiply(inverse(multiply(inverse(multiply(A,E)),D)),multiply(inverse(multiply(F,E)),multiply(F,B))),
    inference(paramod,[status(thm)],[c_1448,c_1395]) ).

cnf(c_2160,plain,
    multiply(inverse(D),multiply(A,B)) = multiply(inverse(multiply(inverse(multiply(A,E)),D)),multiply(inverse(E),B)),
    inference(paramod,[status(thm)],[c_1480,c_2159]) ).

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

cnf(c_2161,plain,
    inverse(multiply(inverse(C),A)) = inverse(multiply(inverse(multiply(D,C)),multiply(D,A))),
    inference(paramod,[status(thm)],[c_1448,c_1387]) ).

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

cnf(c_2162,plain,
    multiply(inverse(multiply(C,D)),A) = multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,D))),multiply(inverse(multiply(C,F)),A)),
    inference(paramod,[status(thm)],[c_1448,c_1383]) ).

cnf(c_2163,plain,
    multiply(inverse(multiply(C,D)),A) = multiply(inverse(multiply(inverse(F),D)),multiply(inverse(multiply(C,F)),A)),
    inference(paramod,[status(thm)],[c_1484,c_2162]) ).

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

cnf(c_2164,plain,
    multiply(inverse(C),A) = multiply(inverse(multiply(D,C)),multiply(D,A)),
    inference(paramod,[status(thm)],[c_1448,c_1376]) ).

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

cnf(c_2165,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),C)),D)),multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),inverse(multiply(inverse(multiply(F,inverse(V6))),multiply(F,inverse(multiply(V7,V6))))))) = multiply(inverse(multiply(multiply(inverse(V6),V6),D)),V7),
    inference(paramod,[status(thm)],[c_1487,c_500]) ).

cnf(c_2166,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),C)),D)),multiply(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(multiply(F,inverse(V6))),multiply(F,inverse(multiply(V7,V6))))))) = multiply(inverse(multiply(multiply(inverse(V6),V6),D)),V7),
    inference(paramod,[status(thm)],[c_1487,c_2165]) ).

cnf(c_2167,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),C)),D)),multiply(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(inverse(V6)),inverse(multiply(V7,V6)))))) = multiply(inverse(multiply(multiply(inverse(V6),V6),D)),V7),
    inference(paramod,[status(thm)],[c_1487,c_2166]) ).

cnf(c_2168,plain,
    multiply(inverse(D),inverse(multiply(inverse(inverse(V6)),inverse(multiply(V7,V6))))) = multiply(inverse(multiply(multiply(inverse(V6),V6),D)),V7),
    inference(paramod,[status(thm)],[c_1487,c_2167]) ).

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

cnf(c_2169,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(D),E))) = multiply(A,multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E)))),
    inference(paramod,[status(thm)],[c_1487,c_883]) ).

cnf(c_2170,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(D),E))) = multiply(A,multiply(inverse(multiply(V6,D)),multiply(V6,E))),
    inference(paramod,[status(thm)],[c_1487,c_2169]) ).

cnf(c_1514,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),D))) = multiply(A,multiply(inverse(C),D)),
    inference(paramod,[status(thm)],[c_1487,c_2170]) ).

cnf(c_2171,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7)) = multiply(inverse(multiply(V8,multiply(inverse(multiply(D,V6)),E))),multiply(V8,V7)),
    inference(paramod,[status(thm)],[c_1487,c_364]) ).

cnf(c_2172,plain,
    multiply(inverse(multiply(inverse(multiply(D,C)),E)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7)) = multiply(inverse(multiply(V8,multiply(inverse(multiply(D,V6)),E))),multiply(V8,V7)),
    inference(paramod,[status(thm)],[c_1485,c_2171]) ).

cnf(c_2173,plain,
    multiply(inverse(multiply(inverse(multiply(D,C)),E)),multiply(inverse(multiply(inverse(V6),C)),V7)) = multiply(inverse(multiply(V8,multiply(inverse(multiply(D,V6)),E))),multiply(V8,V7)),
    inference(paramod,[status(thm)],[c_1487,c_2172]) ).

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

cnf(c_2174,plain,
    inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E)))) = inverse(multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,B)))),
    inference(paramod,[status(thm)],[c_1487,c_1243]) ).

cnf(c_2175,plain,
    inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(E),E))) = inverse(multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,B)))),
    inference(paramod,[status(thm)],[c_1514,c_2174]) ).

cnf(c_2176,plain,
    inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(E),E))) = inverse(multiply(inverse(multiply(V6,C)),multiply(V6,B))),
    inference(paramod,[status(thm)],[c_1487,c_2175]) ).

cnf(c_1551,plain,
    inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))) = inverse(multiply(inverse(B),A)),
    inference(paramod,[status(thm)],[c_1487,c_2176]) ).

cnf(c_2177,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(multiply(D,E)),multiply(D,F))) = multiply(inverse(multiply(inverse(multiply(inverse(E),V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
    inference(paramod,[status(thm)],[c_1487,c_813]) ).

cnf(c_2178,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(E),F)) = multiply(inverse(multiply(inverse(multiply(inverse(E),V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
    inference(paramod,[status(thm)],[c_1487,c_2177]) ).

cnf(c_2179,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(E),F)) = multiply(inverse(multiply(inverse(multiply(inverse(E),V6)),C)),multiply(inverse(V6),F)),
    inference(paramod,[status(thm)],[c_1487,c_2178]) ).

cnf(c_1556,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(C),D)) = multiply(inverse(B),multiply(inverse(C),D)),
    inference(paramod,[status(thm)],[c_1481,c_2179]) ).

cnf(c_2180,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),C)),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),inverse(multiply(multiply(multiply(inverse(D),D),inverse(F)),D)))) = F,
    inference(paramod,[status(thm)],[c_1487,c_115]) ).

cnf(c_2181,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),C)),inverse(D))),multiply(inverse(multiply(inverse(B),C)),inverse(multiply(multiply(multiply(inverse(D),D),inverse(F)),D)))) = F,
    inference(paramod,[status(thm)],[c_1487,c_2180]) ).

cnf(c_1561,plain,
    multiply(inverse(inverse(A)),inverse(multiply(multiply(multiply(inverse(A),A),inverse(B)),A))) = B,
    inference(paramod,[status(thm)],[c_1487,c_2181]) ).

cnf(c_2182,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(C,D)),multiply(C,E)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E)))),
    inference(paramod,[status(thm)],[c_1551,c_1241]) ).

cnf(c_2183,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(D),E))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E)))),
    inference(paramod,[status(thm)],[c_1487,c_2182]) ).

cnf(c_2184,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(D),E))) = inverse(multiply(inverse(multiply(V6,D)),multiply(V6,E))),
    inference(paramod,[status(thm)],[c_1487,c_2183]) ).

cnf(c_1567,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C))) = inverse(multiply(inverse(B),C)),
    inference(paramod,[status(thm)],[c_1487,c_2184]) ).

cnf(c_2185,plain,
    multiply(A,inverse(multiply(inverse(C),C))) = multiply(A,inverse(multiply(inverse(multiply(D,E)),multiply(D,E)))),
    inference(paramod,[status(thm)],[c_1567,c_1232]) ).

cnf(c_1572,plain,
    multiply(A,inverse(multiply(inverse(B),B))) = multiply(A,inverse(multiply(inverse(C),C))),
    inference(paramod,[status(thm)],[c_1487,c_2185]) ).

cnf(c_1577,plain,
    inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(B)),C))),B)) = C,
    inference(paramod,[status(thm)],[c_1487,c_916]) ).

cnf(c_1578,plain,
    multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(B)),inverse(C)))),B) = C,
    inference(paramod,[status(thm)],[c_1487,c_913]) ).

cnf(c_1580,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(B)),inverse(multiply(C,B))))) = C,
    inference(paramod,[status(thm)],[c_1487,c_623]) ).

cnf(c_2186,plain,
    multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(C)),inverse(multiply(D,C)))))),multiply(A,E)) = multiply(inverse(D),multiply(multiply(inverse(C),C),E)),
    inference(paramod,[status(thm)],[c_1487,c_55]) ).

cnf(c_1595,plain,
    multiply(inverse(inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A))))),C) = multiply(inverse(B),multiply(multiply(inverse(A),A),C)),
    inference(paramod,[status(thm)],[c_1487,c_2186]) ).

cnf(c_2187,plain,
    multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(E),C))),multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1487,c_1344]) ).

cnf(c_2188,plain,
    multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),E)) = multiply(inverse(multiply(F,multiply(inverse(E),C))),multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1487,c_2187]) ).

cnf(c_2189,plain,
    multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(E),C))),multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1487,c_2188]) ).

cnf(c_2190,plain,
    multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(E),C))),multiply(F,multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1514,c_2189]) ).

cnf(c_2191,plain,
    multiply(inverse(C),E) = multiply(inverse(multiply(inverse(E),C)),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1487,c_2190]) ).

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

cnf(c_2192,plain,
    multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1487,c_1343]) ).

cnf(c_2193,plain,
    multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),E)) = multiply(inverse(multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1487,c_2192]) ).

cnf(c_2194,plain,
    multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1487,c_2193]) ).

cnf(c_2195,plain,
    multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1599,c_2194]) ).

cnf(c_2196,plain,
    multiply(inverse(C),E) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(C),E)),
    inference(paramod,[status(thm)],[c_1487,c_2195]) ).

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

cnf(c_2197,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,F))) = multiply(inverse(multiply(V6,multiply(V7,C))),multiply(V6,multiply(V7,F))),
    inference(paramod,[status(thm)],[c_1600,c_1331]) ).

cnf(c_2198,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(multiply(inverse(E),E)),F)) = multiply(inverse(multiply(V6,multiply(V7,C))),multiply(V6,multiply(V7,F))),
    inference(paramod,[status(thm)],[c_1487,c_2197]) ).

cnf(c_2199,plain,
    multiply(inverse(C),multiply(inverse(multiply(inverse(E),E)),F)) = multiply(inverse(multiply(V6,multiply(V7,C))),multiply(V6,multiply(V7,F))),
    inference(paramod,[status(thm)],[c_1556,c_2198]) ).

cnf(c_2200,plain,
    multiply(inverse(C),multiply(inverse(multiply(inverse(E),E)),F)) = multiply(inverse(multiply(V7,C)),multiply(V7,F)),
    inference(paramod,[status(thm)],[c_1487,c_2199]) ).

cnf(c_1602,plain,
    multiply(inverse(A),multiply(inverse(multiply(inverse(B),B)),C)) = multiply(inverse(A),C),
    inference(paramod,[status(thm)],[c_1487,c_2200]) ).

cnf(c_2201,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),multiply(inverse(multiply(inverse(D),D)),F)) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
    inference(paramod,[status(thm)],[c_1602,c_1273]) ).

cnf(c_2202,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),F) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
    inference(paramod,[status(thm)],[c_1602,c_2201]) ).

cnf(c_2203,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),F) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(V6),F)),
    inference(paramod,[status(thm)],[c_1487,c_2202]) ).

cnf(c_1603,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),D) = multiply(inverse(C),multiply(A,D)),
    inference(paramod,[status(thm)],[c_1481,c_2203]) ).

cnf(c_2204,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),C)),multiply(inverse(B),E)) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(inverse(multiply(V6,multiply(inverse(V7),V7))),multiply(V6,E))),
    inference(paramod,[status(thm)],[c_1487,c_1271]) ).

cnf(c_2205,plain,
    multiply(inverse(C),multiply(inverse(multiply(inverse(A),A)),E)) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(inverse(multiply(V6,multiply(inverse(V7),V7))),multiply(V6,E))),
    inference(paramod,[status(thm)],[c_1481,c_2204]) ).

cnf(c_2206,plain,
    multiply(inverse(C),E) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(inverse(multiply(V6,multiply(inverse(V7),V7))),multiply(V6,E))),
    inference(paramod,[status(thm)],[c_1602,c_2205]) ).

cnf(c_2207,plain,
    multiply(inverse(C),E) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(inverse(multiply(inverse(V7),V7)),E)),
    inference(paramod,[status(thm)],[c_1487,c_2206]) ).

cnf(c_2208,plain,
    multiply(inverse(C),E) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),E),
    inference(paramod,[status(thm)],[c_1602,c_2207]) ).

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

cnf(c_2209,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),inverse(multiply(multiply(multiply(inverse(E),E),inverse(F)),E)))) = multiply(inverse(multiply(inverse(multiply(A,inverse(E))),C)),F),
    inference(paramod,[status(thm)],[c_1487,c_129]) ).

cnf(c_1612,plain,
    multiply(inverse(A),multiply(B,inverse(multiply(multiply(multiply(inverse(C),C),inverse(D)),C)))) = multiply(inverse(multiply(inverse(multiply(B,inverse(C))),A)),D),
    inference(paramod,[status(thm)],[c_1481,c_2209]) ).

cnf(c_2210,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(A),A)),C)),multiply(inverse(multiply(D,multiply(inverse(E),E))),F)) = multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,C))),multiply(inverse(multiply(D,V7)),F)),
    inference(paramod,[status(thm)],[c_1602,c_1263]) ).

cnf(c_2211,plain,
    multiply(inverse(C),multiply(inverse(multiply(D,multiply(inverse(E),E))),F)) = multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,C))),multiply(inverse(multiply(D,V7)),F)),
    inference(paramod,[status(thm)],[c_1604,c_2210]) ).

cnf(c_2212,plain,
    multiply(inverse(C),multiply(inverse(multiply(D,multiply(inverse(E),E))),F)) = multiply(inverse(multiply(inverse(V7),C)),multiply(inverse(multiply(D,V7)),F)),
    inference(paramod,[status(thm)],[c_1487,c_2211]) ).

cnf(c_1614,plain,
    multiply(inverse(A),multiply(inverse(multiply(B,multiply(inverse(C),C))),D)) = multiply(inverse(multiply(B,A)),D),
    inference(paramod,[status(thm)],[c_1485,c_2212]) ).

cnf(c_2213,plain,
    multiply(inverse(multiply(inverse(B),inverse(multiply(multiply(multiply(inverse(C),C),D),C)))),multiply(inverse(multiply(E,B)),F)) = multiply(D,multiply(inverse(multiply(E,inverse(C))),F)),
    inference(paramod,[status(thm)],[c_1487,c_362]) ).

cnf(c_1617,plain,
    multiply(inverse(multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),C),B)))),D) = multiply(C,multiply(inverse(multiply(A,inverse(B))),D)),
    inference(paramod,[status(thm)],[c_1485,c_2213]) ).

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

cnf(c_2215,plain,
    inverse(multiply(inverse(inverse(B)),inverse(multiply(C,B)))) = inverse(multiply(inverse(multiply(D,inverse(E))),multiply(D,inverse(multiply(C,E))))),
    inference(paramod,[status(thm)],[c_1578,c_2214]) ).

cnf(c_1622,plain,
    inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A)))) = inverse(multiply(inverse(inverse(C)),inverse(multiply(B,C)))),
    inference(paramod,[status(thm)],[c_1487,c_2215]) ).

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

cnf(c_2217,plain,
    multiply(inverse(inverse(B)),inverse(multiply(C,B))) = multiply(inverse(multiply(D,inverse(E))),multiply(D,inverse(multiply(C,E)))),
    inference(paramod,[status(thm)],[c_1578,c_2216]) ).

cnf(c_1624,plain,
    multiply(inverse(inverse(A)),inverse(multiply(B,A))) = multiply(inverse(inverse(C)),inverse(multiply(B,C))),
    inference(paramod,[status(thm)],[c_1487,c_2217]) ).

cnf(c_1633,plain,
    multiply(inverse(multiply(inverse(A),A)),B) = B,
    inference(paramod,[status(thm)],[c_1561,c_905]) ).

cnf(c_1643,plain,
    multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
    inference(paramod,[status(thm)],[c_1572,c_702]) ).

cnf(c_2218,plain,
    multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(D),D))),C),
    inference(paramod,[status(thm)],[c_1572,c_1487]) ).

cnf(c_1648,plain,
    multiply(inverse(inverse(multiply(inverse(A),A))),B) = multiply(inverse(inverse(multiply(inverse(C),C))),B),
    inference(paramod,[status(thm)],[c_1487,c_2218]) ).

cnf(c_1654,plain,
    multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B))) = multiply(inverse(inverse(C)),inverse(multiply(inverse(A),C))),
    inference(paramod,[status(thm)],[c_702,c_1624]) ).

cnf(c_1657,plain,
    multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A)))),multiply(inverse(inverse(C)),D)) = multiply(inverse(inverse(multiply(B,C))),D),
    inference(paramod,[status(thm)],[c_1624,c_1487]) ).

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

cnf(c_2220,plain,
    multiply(inverse(C),multiply(A,multiply(inverse(multiply(inverse(D),E)),F))) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(multiply(inverse(multiply(inverse(E),D)),V6)),F)),
    inference(paramod,[status(thm)],[c_1603,c_2219]) ).

cnf(c_2221,plain,
    multiply(inverse(C),multiply(A,multiply(inverse(multiply(inverse(D),E)),F))) = multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(E),D))),C)),F),
    inference(paramod,[status(thm)],[c_1545,c_2220]) ).

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

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

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

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

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

cnf(c_2225,plain,
    multiply(inverse(multiply(A,B)),inverse(multiply(multiply(multiply(inverse(C),C),inverse(multiply(inverse(inverse(C)),multiply(A,multiply(inverse(multiply(inverse(E),F)),V6))))),C))) = multiply(inverse(multiply(inverse(multiply(inverse(F),E)),B)),V6),
    inference(paramod,[status(thm)],[c_1633,c_2224]) ).

cnf(c_2226,plain,
    multiply(inverse(multiply(A,B)),multiply(A,multiply(inverse(multiply(inverse(E),F)),V6))) = multiply(inverse(multiply(inverse(multiply(inverse(F),E)),B)),V6),
    inference(paramod,[status(thm)],[c_1577,c_2225]) ).

cnf(c_2227,plain,
    multiply(inverse(B),multiply(inverse(multiply(inverse(E),F)),V6)) = multiply(inverse(multiply(inverse(multiply(inverse(F),E)),B)),V6),
    inference(paramod,[status(thm)],[c_1487,c_2226]) ).

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

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

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

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

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

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

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

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

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

cnf(c_1743,plain,
    multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B)))),multiply(inverse(inverse(C)),D)) = multiply(inverse(inverse(multiply(inverse(A),C))),D),
    inference(paramod,[status(thm)],[c_1654,c_1487]) ).

cnf(c_1744,plain,
    multiply(inverse(multiply(inverse(inverse(A)),B)),multiply(inverse(inverse(C)),inverse(multiply(inverse(D),D)))) = multiply(inverse(B),inverse(multiply(inverse(C),A))),
    inference(paramod,[status(thm)],[c_1654,c_1487]) ).

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

cnf(c_1764,plain,
    multiply(inverse(inverse(inverse(multiply(A,B)))),inverse(multiply(inverse(C),C))) = multiply(inverse(inverse(inverse(B))),inverse(multiply(inverse(inverse(multiply(A,D))),inverse(D)))),
    inference(paramod,[status(thm)],[c_1666,c_1654]) ).

cnf(c_1798,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),inverse(multiply(C,inverse(multiply(inverse(D),D))))))) = C,
    inference(paramod,[status(thm)],[c_1572,c_1580]) ).

cnf(c_1801,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(C),D))))) = inverse(multiply(inverse(D),C)),
    inference(paramod,[status(thm)],[c_1599,c_1580]) ).

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

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

cnf(c_1808,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C))))))) = inverse(inverse(D)),
    inference(paramod,[status(thm)],[c_1654,c_1580]) ).

cnf(c_1811,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))) = inverse(multiply(inverse(C),C)),
    inference(paramod,[status(thm)],[c_1643,c_1580]) ).

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

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

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

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

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

cnf(c_1837,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C))),inverse(C))) = A,
    inference(paramod,[status(thm)],[c_1801,c_2236]) ).

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

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

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

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

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

cnf(c_1864,plain,
    multiply(inverse(multiply(inverse(inverse(multiply(inverse(A),A))),B)),multiply(inverse(inverse(multiply(inverse(C),C))),D)) = multiply(inverse(B),D),
    inference(paramod,[status(thm)],[c_1648,c_1487]) ).

cnf(c_2238,plain,
    multiply(inverse(B),D) = multiply(inverse(B),inverse(multiply(inverse(inverse(E)),inverse(multiply(D,E))))),
    inference(paramod,[status(thm)],[c_1864,c_1825]) ).

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

cnf(c_1874,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),inverse(C)))) = inverse(inverse(C)),
    inference(paramod,[status(thm)],[c_1873,c_1808]) ).

cnf(c_1885,plain,
    multiply(inverse(multiply(multiply(inverse(A),A),B)),C) = multiply(inverse(B),C),
    inference(paramod,[status(thm)],[c_1873,c_1490]) ).

cnf(c_1887,plain,
    inverse(inverse(multiply(A,inverse(multiply(inverse(B),B))))) = A,
    inference(paramod,[status(thm)],[c_1874,c_1798]) ).

cnf(c_2239,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(inverse(C)),D))),C))) = D,
    inference(paramod,[status(thm)],[c_1885,c_900]) ).

cnf(c_1899,plain,
    multiply(multiply(inverse(A),A),B) = B,
    inference(paramod,[status(thm)],[c_1577,c_2239]) ).

cnf(c_2240,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(inverse(E)),inverse(multiply(B,E)))))))) = D,
    inference(paramod,[status(thm)],[c_1899,c_1807]) ).

cnf(c_1904,plain,
    inverse(multiply(inverse(A),inverse(multiply(B,multiply(inverse(inverse(C)),inverse(multiply(A,C))))))) = B,
    inference(paramod,[status(thm)],[c_1899,c_2240]) ).

cnf(c_2241,plain,
    inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A)))) = inverse(multiply(inverse(C),inverse(multiply(B,multiply(inverse(inverse(E)),inverse(multiply(C,E))))))),
    inference(paramod,[status(thm)],[c_1899,c_1729]) ).

cnf(c_1907,plain,
    inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A)))) = B,
    inference(paramod,[status(thm)],[c_1904,c_2241]) ).

cnf(c_2242,plain,
    multiply(A,inverse(multiply(inverse(C),D))) = inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(D))),inverse(F))),C))),F)),
    inference(paramod,[status(thm)],[c_1899,c_1858]) ).

cnf(c_2243,plain,
    multiply(A,inverse(multiply(inverse(C),D))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(D))),inverse(F))),C)),F)),
    inference(paramod,[status(thm)],[c_1899,c_2242]) ).

cnf(c_2244,plain,
    multiply(A,inverse(multiply(inverse(C),D))) = inverse(multiply(inverse(C),multiply(inverse(multiply(inverse(inverse(F)),multiply(A,inverse(D)))),F))),
    inference(paramod,[status(thm)],[c_1679,c_2243]) ).

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

cnf(c_2245,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(C),C))),D)),multiply(inverse(E),E)))) = D,
    inference(paramod,[status(thm)],[c_1899,c_1856]) ).

cnf(c_2246,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(inverse(D),inverse(multiply(inverse(C),C))))) = D,
    inference(paramod,[status(thm)],[c_1599,c_2245]) ).

cnf(c_1918,plain,
    inverse(multiply(inverse(A),inverse(multiply(inverse(B),B)))) = A,
    inference(paramod,[status(thm)],[c_1899,c_2246]) ).

cnf(c_2247,plain,
    multiply(inverse(inverse(A)),inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(C),E))),multiply(inverse(C),A)))) = E,
    inference(paramod,[status(thm)],[c_1918,c_1853]) ).

cnf(c_2248,plain,
    multiply(inverse(inverse(A)),inverse(multiply(inverse(multiply(inverse(C),E)),multiply(inverse(C),A)))) = E,
    inference(paramod,[status(thm)],[c_1899,c_2247]) ).

cnf(c_1921,plain,
    multiply(inverse(inverse(A)),inverse(multiply(inverse(B),A))) = B,
    inference(paramod,[status(thm)],[c_1487,c_2248]) ).

cnf(c_1927,plain,
    multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(multiply(B,inverse(C))),D)),C))) = multiply(inverse(multiply(B,A)),D),
    inference(paramod,[status(thm)],[c_1899,c_1843]) ).

cnf(c_2249,plain,
    multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(C)),inverse(C)))) = multiply(inverse(D),D),
    inference(paramod,[status(thm)],[c_1907,c_1813]) ).

cnf(c_2250,plain,
    inverse(multiply(inverse(inverse(C)),inverse(C))) = multiply(inverse(D),D),
    inference(paramod,[status(thm)],[c_1899,c_2249]) ).

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

cnf(c_1943,plain,
    multiply(inverse(multiply(A,inverse(multiply(B,C)))),D) = multiply(B,multiply(inverse(multiply(A,inverse(C))),D)),
    inference(paramod,[status(thm)],[c_1899,c_1617]) ).

cnf(c_2251,plain,
    multiply(inverse(A),multiply(B,inverse(multiply(inverse(D),C)))) = multiply(inverse(multiply(inverse(multiply(B,inverse(C))),A)),D),
    inference(paramod,[status(thm)],[c_1899,c_1612]) ).

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

cnf(c_2252,plain,
    multiply(inverse(A),multiply(inverse(inverse(C)),D)) = multiply(inverse(inverse(multiply(inverse(A),C))),D),
    inference(paramod,[status(thm)],[c_1918,c_1743]) ).

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

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

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

cnf(c_2254,plain,
    multiply(B,multiply(inverse(inverse(C)),D)) = multiply(inverse(inverse(multiply(B,C))),D),
    inference(paramod,[status(thm)],[c_1907,c_1657]) ).

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

cnf(c_1976,plain,
    multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B))) = A,
    inference(paramod,[status(thm)],[c_1921,c_1654]) ).

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

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

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

cnf(c_1985,plain,
    multiply(inverse(A),inverse(multiply(inverse(B),multiply(C,inverse(multiply(inverse(D),D)))))) = multiply(inverse(multiply(C,A)),B),
    inference(paramod,[status(thm)],[c_1944,c_1927]) ).

cnf(c_1988,plain,
    multiply(inverse(multiply(inverse(inverse(A)),B)),C) = multiply(inverse(B),inverse(multiply(inverse(C),A))),
    inference(paramod,[status(thm)],[c_1976,c_1744]) ).

cnf(c_1995,plain,
    inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(inverse(inverse(C)),inverse(C)))) = A,
    inference(paramod,[status(thm)],[c_1965,c_1837]) ).

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

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

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

cnf(c_2260,plain,
    multiply(A,multiply(inverse(inverse(B)),multiply(inverse(inverse(inverse(B))),inverse(inverse(C))))) = multiply(inverse(inverse(multiply(A,multiply(inverse(inverse(C)),D)))),inverse(D)),
    inference(paramod,[status(thm)],[c_1965,c_2259]) ).

cnf(c_2261,plain,
    multiply(A,multiply(inverse(inverse(B)),multiply(inverse(inverse(inverse(B))),inverse(inverse(C))))) = multiply(A,multiply(inverse(inverse(multiply(inverse(inverse(C)),D))),inverse(D))),
    inference(paramod,[status(thm)],[c_1965,c_2260]) ).

cnf(c_1998,plain,
    multiply(A,multiply(inverse(inverse(B)),multiply(inverse(inverse(inverse(B))),inverse(inverse(C))))) = multiply(A,multiply(inverse(inverse(C)),multiply(inverse(inverse(D)),inverse(D)))),
    inference(paramod,[status(thm)],[c_1965,c_2261]) ).

cnf(c_2262,plain,
    inverse(multiply(A,B)) = multiply(inverse(inverse(inverse(B))),inverse(multiply(inverse(inverse(multiply(A,D))),inverse(D)))),
    inference(paramod,[status(thm)],[c_1976,c_1764]) ).

cnf(c_2263,plain,
    inverse(multiply(A,B)) = multiply(inverse(inverse(inverse(B))),inverse(multiply(A,multiply(inverse(inverse(D)),inverse(D))))),
    inference(paramod,[status(thm)],[c_1965,c_2262]) ).

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

cnf(c_2013,plain,
    multiply(inverse(multiply(inverse(A),multiply(inverse(inverse(A)),B))),multiply(inverse(C),D)) = multiply(inverse(B),inverse(multiply(inverse(D),C))),
    inference(paramod,[status(thm)],[c_1988,c_1958]) ).

cnf(c_2016,plain,
    inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(C))),inverse(multiply(inverse(D),D))))) = multiply(B,inverse(multiply(inverse(A),C))),
    inference(paramod,[status(thm)],[c_1988,c_1916]) ).

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

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

cnf(c_2266,plain,
    multiply(inverse(B),inverse(multiply(inverse(E),multiply(C,D)))) = multiply(inverse(multiply(inverse(multiply(inverse(D),F)),B)),multiply(inverse(multiply(C,F)),E)),
    inference(paramod,[status(thm)],[c_2013,c_2265]) ).

cnf(c_2267,plain,
    multiply(inverse(B),inverse(multiply(inverse(E),multiply(C,D)))) = multiply(inverse(B),multiply(inverse(multiply(inverse(F),D)),multiply(inverse(multiply(C,F)),E))),
    inference(paramod,[status(thm)],[c_1679,c_2266]) ).

cnf(c_2042,plain,
    multiply(inverse(A),inverse(multiply(inverse(B),multiply(C,D)))) = multiply(inverse(A),multiply(inverse(multiply(C,D)),B)),
    inference(paramod,[status(thm)],[c_1485,c_2267]) ).

cnf(c_2268,plain,
    multiply(inverse(inverse(multiply(inverse(inverse(A)),inverse(A)))),B) = B,
    inference(paramod,[status(thm)],[c_1929,c_1633]) ).

cnf(c_2048,plain,
    multiply(inverse(inverse(A)),multiply(inverse(inverse(inverse(A))),B)) = B,
    inference(paramod,[status(thm)],[c_1965,c_2268]) ).

cnf(c_2269,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(inverse(C)),inverse(C)))))) = B,
    inference(paramod,[status(thm)],[c_1929,c_1907]) ).

cnf(c_2061,plain,
    inverse(inverse(multiply(A,multiply(inverse(inverse(B)),inverse(B))))) = A,
    inference(paramod,[status(thm)],[c_1633,c_2269]) ).

cnf(c_2063,plain,
    multiply(inverse(inverse(A)),multiply(inverse(B),B)) = A,
    inference(paramod,[status(thm)],[c_1929,c_1976]) ).

cnf(c_2270,plain,
    multiply(inverse(A),multiply(inverse(multiply(C,inverse(multiply(inverse(D),D)))),B)) = multiply(inverse(multiply(C,A)),B),
    inference(paramod,[status(thm)],[c_2042,c_1985]) ).

cnf(c_2066,plain,
    multiply(inverse(A),multiply(inverse(B),multiply(inverse(multiply(C,inverse(B))),D))) = multiply(inverse(multiply(C,A)),D),
    inference(paramod,[status(thm)],[c_1943,c_2270]) ).

cnf(c_2271,plain,
    multiply(A,inverse(inverse(C))) = multiply(A,multiply(inverse(inverse(C)),multiply(inverse(inverse(D)),inverse(D)))),
    inference(paramod,[status(thm)],[c_2048,c_1998]) ).

cnf(c_2068,plain,
    multiply(A,inverse(inverse(B))) = multiply(A,B),
    inference(paramod,[status(thm)],[c_2063,c_2271]) ).

cnf(c_2069,plain,
    multiply(inverse(multiply(A,multiply(inverse(B),C))),D) = multiply(inverse(C),multiply(inverse(multiply(A,inverse(B))),D)),
    inference(paramod,[status(thm)],[c_2066,c_1980]) ).

cnf(c_2272,plain,
    multiply(inverse(B),multiply(inverse(multiply(inverse(A),inverse(inverse(A)))),multiply(inverse(C),D))) = multiply(inverse(B),inverse(multiply(inverse(D),C))),
    inference(paramod,[status(thm)],[c_2069,c_2013]) ).

cnf(c_2273,plain,
    multiply(inverse(B),multiply(inverse(multiply(inverse(A),A)),multiply(inverse(C),D))) = multiply(inverse(B),inverse(multiply(inverse(D),C))),
    inference(paramod,[status(thm)],[c_2068,c_2272]) ).

cnf(c_2274,plain,
    multiply(inverse(B),multiply(inverse(C),D)) = multiply(inverse(B),inverse(multiply(inverse(D),C))),
    inference(paramod,[status(thm)],[c_1633,c_2273]) ).

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

cnf(c_2075,plain,
    inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(A))),multiply(inverse(inverse(C)),inverse(C))))) = B,
    inference(paramod,[status(thm)],[c_2069,c_1995]) ).

cnf(c_2080,plain,
    inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(C))),multiply(inverse(D),D)))) = multiply(B,inverse(multiply(inverse(A),C))),
    inference(paramod,[status(thm)],[c_2073,c_2016]) ).

cnf(c_2089,plain,
    multiply(A,inverse(multiply(inverse(B),B))) = A,
    inference(paramod,[status(thm)],[c_2080,c_2075]) ).

cnf(c_2095,plain,
    inverse(inverse(A)) = A,
    inference(paramod,[status(thm)],[c_2089,c_1887]) ).

cnf(c_2275,plain,
    inverse(inverse(multiply(A,multiply(B,inverse(B))))) = A,
    inference(paramod,[status(thm)],[c_2095,c_2061]) ).

cnf(c_2104,plain,
    multiply(A,multiply(B,inverse(B))) = A,
    inference(paramod,[status(thm)],[c_2095,c_2275]) ).

cnf(c_2276,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(inverse(inverse(C)),inverse(C))))) = inverse(multiply(B,A)),
    inference(paramod,[status(thm)],[c_2095,c_2006]) ).

cnf(c_2277,plain,
    multiply(inverse(A),inverse(multiply(B,multiply(C,inverse(C))))) = inverse(multiply(B,A)),
    inference(paramod,[status(thm)],[c_2095,c_2276]) ).

cnf(c_2278,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
    inference(paramod,[status(thm)],[c_2104,c_2277]) ).

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

cnf(c_2279,plain,
    multiply(inverse(multiply(inverse(B),inverse(A))),C) = multiply(A,multiply(inverse(inverse(B)),C)),
    inference(paramod,[status(thm)],[c_2107,c_1965]) ).

cnf(c_2280,plain,
    multiply(multiply(inverse(inverse(A)),inverse(inverse(B))),C) = multiply(A,multiply(inverse(inverse(B)),C)),
    inference(paramod,[status(thm)],[c_2107,c_2279]) ).

cnf(c_2281,plain,
    multiply(multiply(A,inverse(inverse(B))),C) = multiply(A,multiply(inverse(inverse(B)),C)),
    inference(paramod,[status(thm)],[c_2095,c_2280]) ).

cnf(c_2282,plain,
    multiply(multiply(A,B),C) = multiply(A,multiply(inverse(inverse(B)),C)),
    inference(paramod,[status(thm)],[c_2095,c_2281]) ).

cnf(c_2115,plain,
    multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
    inference(paramod,[status(thm)],[c_2095,c_2282]) ).

cnf(c_2116,plain,
    $false,
    inference(resolve,[status(thm)],[c_2115,c_2]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : GRP414-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06  % Command  : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44  % Computer : n008.cluster.edu
% 0.17/0.44  % Model    : x86_64 x86_64
% 0.17/0.44  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44  % Memory   : 8046.5625MB
% 0.17/0.44  % OS       : Linux 6.8.0-71-generic
% 0.17/0.44  % CPULimit : 300
% 0.17/0.44  % WCLimit  : 300
% 0.17/0.44  % DateTime : Fri Sep 25 14:53:40 UTC 2026
% 0.17/0.45  % CPUTime  : 
% 0.17/0.45  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45  % Process 1326483 was started by sandbox2 on n008,
% 0.17/0.45  % Fri Sep 25 14:53:40 2026
% 0.17/0.45  % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.45  
% 0.17/0.45  % From the command line: assign(max_seconds, 300).
% 15.34/2.42  
% 15.34/2.42  % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 15.34/2.42  
% 15.34/2.42  % SZS status Unsatisfiable for theBenchmark
% 15.34/2.42  
% 15.34/2.42  % Proof 1 at 1.47 (+ 0.40) seconds.
% 15.34/2.42  % Length of proof is 178.
% 15.34/2.42  % Level of proof is 39.
% 15.34/2.42  % Maximum clause weight is 100.000.
% 15.34/2.42  % Given clauses 96.
% 15.34/2.42  
% 15.34/2.42  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------