%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP056-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:26:53 AM UTC 2026
% Result : Unsatisfiable 3.98s 1.00s
% Output : CNFRefutation 3.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 2
% Syntax : Number of formulae : 308 ( 300 unt; 0 def)
% Number of atoms : 319 ( 318 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 31 ( 20 ~; 11 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 1140 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(inverse(multiply(inverse(multiply(VAR_0,inverse(multiply(inverse(VAR_1),VAR_2)))),multiply(VAR_0,inverse(VAR_2)))),inverse(multiply(inverse(VAR_2),VAR_2))) = VAR_1,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),C)))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C))) = B,
inference(clausify,[status(thm)],[single_axiom]) ).
fof(prove_these_axioms,axiom,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
file('theBenchmark.p',prove_these_axioms) ).
cnf(c_2,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(clausify,[status(thm)],[prove_these_axioms]) ).
cnf(c_3,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ),
inference(copy,[status(thm)],[c_2]) ).
cnf(c_4,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))) = multiply(inverse(multiply(D,inverse(multiply(inverse(B),C)))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_6,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(C),C)))),C)))),multiply(A,inverse(C))) = B,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_7,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(C),C))) = B,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_9,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),C)))),multiply(A,inverse(C))) = multiply(inverse(multiply(D,inverse(multiply(inverse(B),C)))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_4,c_4]) ).
cnf(c_10,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D)))))),inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(D))))) = multiply(C,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(D),D)))),D))),
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_840,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D))))) = multiply(inverse(multiply(E,inverse(multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(D),D)))),D)))),multiply(C,inverse(D)))))),multiply(E,inverse(multiply(C,inverse(D))))),
inference(paramod,[status(thm)],[c_6,c_9]) ).
cnf(c_13,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D))))) = multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(multiply(C,inverse(D))))),
inference(paramod,[status(thm)],[c_6,c_840]) ).
cnf(c_841,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(C,inverse(D)))))),multiply(A,inverse(multiply(C,inverse(D)))))),inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(D))))) = B,
inference(paramod,[status(thm)],[c_13,c_1]) ).
cnf(c_14,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),C))) = B,
inference(paramod,[status(thm)],[c_10,c_841]) ).
cnf(c_842,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(C),F)))),multiply(E,inverse(F)))),inverse(multiply(inverse(F),F)))))),
inference(paramod,[status(thm)],[c_1,c_13]) ).
cnf(c_16,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_1,c_842]) ).
cnf(c_843,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(D)))))),multiply(A,inverse(multiply(E,inverse(D)))))),inverse(multiply(inverse(multiply(E,inverse(D))),multiply(E,inverse(D))))) = multiply(E,inverse(C)),
inference(paramod,[status(thm)],[c_16,c_1]) ).
cnf(c_18,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(D)))),inverse(multiply(inverse(D),D)))),D))) = multiply(A,inverse(C)),
inference(paramod,[status(thm)],[c_10,c_843]) ).
cnf(c_844,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(multiply(B,inverse(multiply(inverse(A),C)))),multiply(B,inverse(C)))),inverse(D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(C),C)))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_1,c_16]) ).
cnf(c_20,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(C))),
inference(copy,[status(thm)],[c_844]) ).
cnf(c_21,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),C)))),multiply(A,inverse(C)))),inverse(D))),B) = multiply(inverse(multiply(E,inverse(D))),multiply(E,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_1,c_16]) ).
cnf(c_845,plain,
multiply(inverse(A),multiply(B,inverse(C))) = multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),multiply(B,inverse(E)))),inverse(multiply(inverse(E),E)))),E)))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_14,c_16]) ).
cnf(c_24,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),inverse(multiply(inverse(D),D)))),D)))),multiply(A,inverse(E))) = multiply(inverse(B),multiply(C,inverse(E))),
inference(copy,[status(thm)],[c_845]) ).
cnf(c_846,plain,
multiply(inverse(multiply(A,inverse(B))),C) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),multiply(A,inverse(E)))),inverse(multiply(inverse(E),E)))),E)))),
inference(paramod,[status(thm)],[c_14,c_16]) ).
cnf(c_25,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),multiply(D,inverse(E)))),inverse(multiply(inverse(E),E)))),E)))) = multiply(inverse(multiply(D,inverse(B))),C),
inference(copy,[status(thm)],[c_846]) ).
cnf(c_27,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C))) = multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_18,c_1]) ).
cnf(c_30,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),inverse(multiply(inverse(D),D)))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(E)))),inverse(multiply(inverse(E),E)))),E))),
inference(paramod,[status(thm)],[c_14,c_18]) ).
cnf(c_31,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(C),C)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_27,c_16]) ).
cnf(c_32,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(C)))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_27,c_16]) ).
cnf(c_847,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D)))))),inverse(multiply(inverse(multiply(E,inverse(D))),multiply(E,inverse(D))))) = multiply(inverse(multiply(inverse(multiply(F,inverse(B))),multiply(F,inverse(multiply(C,inverse(D)))))),inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(D))))),
inference(paramod,[status(thm)],[c_16,c_27]) ).
cnf(c_33,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D)))))),inverse(multiply(inverse(multiply(E,inverse(D))),multiply(E,inverse(D))))) = multiply(C,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(D),D)))),D))),
inference(paramod,[status(thm)],[c_10,c_847]) ).
cnf(c_848,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(C),C))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(E)))),inverse(multiply(inverse(E),E)))),E),
inference(paramod,[status(thm)],[c_18,c_7]) ).
cnf(c_849,plain,
B = multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(E)))),inverse(multiply(inverse(E),E)))),E),
inference(paramod,[status(thm)],[c_7,c_848]) ).
cnf(c_34,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),C) = B,
inference(copy,[status(thm)],[c_849]) ).
cnf(c_38,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(multiply(inverse(B),B)))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_1,c_20]) ).
cnf(c_850,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(multiply(B,inverse(multiply(inverse(A),C)))),multiply(B,inverse(C)))),inverse(multiply(inverse(C),C)))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_1,c_38]) ).
cnf(c_45,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_1,c_850]) ).
cnf(c_851,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))) = multiply(inverse(multiply(inverse(multiply(C,inverse(multiply(inverse(B),B)))),multiply(C,inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))),
inference(paramod,[status(thm)],[c_38,c_27]) ).
cnf(c_57,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))) = multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))),
inference(copy,[status(thm)],[c_851]) ).
cnf(c_68,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2 ),
inference(resolve,[status(thm)],[c_45,c_3]) ).
cnf(c_69,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_45,c_1]) ).
cnf(c_70,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C)))),inverse(multiply(inverse(C),C))) = B,
inference(paramod,[status(thm)],[c_45,c_1]) ).
cnf(c_71,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(inverse(B),A)))),multiply(inverse(C),C))),inverse(multiply(inverse(A),A))) = B,
inference(paramod,[status(thm)],[c_45,c_1]) ).
cnf(c_74,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D))))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),D)))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_45,c_4]) ).
cnf(c_88,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),B)),C)))),multiply(A,inverse(C))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_45,c_6]) ).
cnf(c_90,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(A),A)))),A)))),multiply(inverse(C),C)) = B,
inference(paramod,[status(thm)],[c_45,c_6]) ).
cnf(c_91,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_45,c_16]) ).
cnf(c_92,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(C),C)) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(A))),
inference(paramod,[status(thm)],[c_45,c_16]) ).
cnf(c_106,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(multiply(inverse(B),B))),inverse(C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(C))),
inference(paramod,[status(thm)],[c_45,c_20]) ).
cnf(c_852,plain,
multiply(inverse(B),B) = multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))),
inference(paramod,[status(thm)],[c_69,c_57]) ).
cnf(c_111,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))) = multiply(inverse(B),B),
inference(copy,[status(thm)],[c_852]) ).
cnf(c_112,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_91,c_45]) ).
cnf(c_853,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_45,c_91]) ).
cnf(c_115,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(B)),inverse(A))),
inference(copy,[status(thm)],[c_853]) ).
cnf(c_118,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_45,c_112]) ).
cnf(c_854,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_118,c_91]) ).
cnf(c_129,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),D))) = multiply(inverse(multiply(inverse(E),E)),multiply(inverse(inverse(B)),inverse(A))),
inference(copy,[status(thm)],[c_854]) ).
cnf(c_132,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(C),C)) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_118,c_118]) ).
cnf(c_138,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),C)))),multiply(A,inverse(C)))),inverse(D))),B) = multiply(inverse(multiply(inverse(E),E)),multiply(inverse(inverse(D)),inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_45,c_21]) ).
cnf(c_157,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),inverse(multiply(inverse(D),D)))),D)))),multiply(A,inverse(E))) = multiply(inverse(B),multiply(inverse(inverse(D)),inverse(E))),
inference(paramod,[status(thm)],[c_45,c_24]) ).
cnf(c_855,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(inverse(C)),inverse(D)))),inverse(multiply(inverse(D),D)))),D)))),multiply(A,inverse(C))) = multiply(inverse(B),multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_45,c_24]) ).
cnf(c_161,plain,
multiply(inverse(A),multiply(inverse(inverse(B)),inverse(B))) = multiply(inverse(A),multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_24,c_855]) ).
cnf(c_164,plain,
multiply(inverse(A),multiply(inverse(B),B)) = multiply(inverse(A),multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_45,c_161]) ).
cnf(c_165,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))) = multiply(inverse(A),multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_118,c_161]) ).
cnf(c_209,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),multiply(inverse(D),D))),inverse(multiply(inverse(E),E)))),E)))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(B))),C),
inference(paramod,[status(thm)],[c_45,c_25]) ).
cnf(c_856,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),multiply(inverse(inverse(B)),inverse(D)))),inverse(multiply(inverse(D),D)))),D)))) = multiply(inverse(multiply(inverse(E),E)),C),
inference(paramod,[status(thm)],[c_45,c_25]) ).
cnf(c_211,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(A))),B) = multiply(inverse(multiply(inverse(C),C)),B),
inference(paramod,[status(thm)],[c_25,c_856]) ).
cnf(c_213,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),multiply(D,inverse(E)))),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(V6),V6))))),E)))) = multiply(inverse(multiply(D,inverse(B))),C),
inference(paramod,[status(thm)],[c_118,c_25]) ).
cnf(c_857,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),inverse(multiply(inverse(D),D)))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(inverse(D)),inverse(E)))),inverse(multiply(inverse(E),E)))),E))),
inference(paramod,[status(thm)],[c_45,c_30]) ).
cnf(c_226,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(inverse(C)),inverse(D)))),inverse(multiply(inverse(D),D)))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))),C))),
inference(copy,[status(thm)],[c_857]) ).
cnf(c_237,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),C) = multiply(inverse(multiply(inverse(D),D)),C),
inference(paramod,[status(thm)],[c_118,c_211]) ).
cnf(c_858,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))),inverse(B))),multiply(inverse(multiply(inverse(F),F)),inverse(C))),
inference(paramod,[status(thm)],[c_237,c_91]) ).
cnf(c_263,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),inverse(C))),multiply(inverse(multiply(inverse(D),D)),inverse(E))) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(C)),inverse(E))),
inference(copy,[status(thm)],[c_858]) ).
cnf(c_859,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))),inverse(B))),multiply(inverse(multiply(inverse(F),F)),inverse(A))),
inference(paramod,[status(thm)],[c_237,c_92]) ).
cnf(c_274,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),inverse(C))),multiply(inverse(multiply(inverse(D),D)),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(C))),multiply(inverse(F),F)),
inference(copy,[status(thm)],[c_859]) ).
cnf(c_280,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(V6),V6)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_45,c_31]) ).
cnf(c_282,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(multiply(inverse(C),C)))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_45,c_31]) ).
cnf(c_298,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(D))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_45,c_32]) ).
cnf(c_304,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(C)))),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(V6),V6))))) = multiply(inverse(multiply(V7,inverse(D))),multiply(V7,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_118,c_32]) ).
cnf(c_312,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(A,inverse(B)))),inverse(C))),multiply(inverse(D),D))),inverse(multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(B))))) = multiply(A,inverse(multiply(inverse(multiply(inverse(C),inverse(multiply(inverse(B),B)))),B))),
inference(paramod,[status(thm)],[c_45,c_33]) ).
cnf(c_860,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D)))))),inverse(multiply(inverse(multiply(E,inverse(D))),multiply(E,inverse(D))))) = multiply(C,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(F),F)))),D))),
inference(paramod,[status(thm)],[c_45,c_33]) ).
cnf(c_861,plain,
multiply(C,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(D),D)))),D))) = multiply(C,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(F),F)))),D))),
inference(paramod,[status(thm)],[c_33,c_860]) ).
cnf(c_317,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(C),C)))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(D),D)))),D))),
inference(copy,[status(thm)],[c_861]) ).
cnf(c_343,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_45,c_111]) ).
cnf(c_359,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))),multiply(inverse(D),D))),multiply(inverse(E),E)))) = multiply(inverse(E),E),
inference(paramod,[status(thm)],[c_132,c_111]) ).
cnf(c_377,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C)))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_343,c_118]) ).
cnf(c_380,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C)))) = multiply(inverse(A),multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_343,c_164]) ).
cnf(c_406,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_343,c_343]) ).
cnf(c_496,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))),multiply(inverse(E),E))) = multiply(inverse(multiply(F,inverse(B))),multiply(F,inverse(A))),
inference(paramod,[status(thm)],[c_380,c_92]) ).
cnf(c_862,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),E)))),multiply(inverse(F),F))),multiply(inverse(inverse(B)),inverse(A))),
inference(paramod,[status(thm)],[c_380,c_115]) ).
cnf(c_498,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),multiply(inverse(C),C))),multiply(inverse(inverse(D)),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(D))),multiply(inverse(F),F)),
inference(copy,[status(thm)],[c_862]) ).
cnf(c_547,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(C),C))))),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))) = B,
inference(paramod,[status(thm)],[c_34,c_165]) ).
cnf(c_557,plain,
multiply(inverse(multiply(inverse(A),A)),B) = B,
inference(paramod,[status(thm)],[c_343,c_34]) ).
cnf(c_863,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),multiply(inverse(inverse(C)),inverse(D)))),inverse(multiply(inverse(D),D)))),D) = C,
inference(paramod,[status(thm)],[c_343,c_34]) ).
cnf(c_558,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(inverse(B)),inverse(C)))),inverse(multiply(inverse(C),C)))),C) = B,
inference(paramod,[status(thm)],[c_557,c_863]) ).
cnf(c_864,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(B))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D))))),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(E),E))))),multiply(inverse(E),E)) = B,
inference(paramod,[status(thm)],[c_406,c_34]) ).
cnf(c_865,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D))))),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(E),E))))),multiply(inverse(E),E)) = B,
inference(paramod,[status(thm)],[c_557,c_864]) ).
cnf(c_866,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(E),E))))),multiply(inverse(E),E)) = B,
inference(paramod,[status(thm)],[c_557,c_865]) ).
cnf(c_565,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(C),C)))),multiply(inverse(C),C)) = A,
inference(paramod,[status(thm)],[c_557,c_866]) ).
cnf(c_867,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),C) = C,
inference(paramod,[status(thm)],[c_406,c_34]) ).
cnf(c_566,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),B) = B,
inference(paramod,[status(thm)],[c_557,c_867]) ).
cnf(c_868,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C))))),multiply(inverse(inverse(D)),inverse(E)))),inverse(multiply(inverse(E),E)))),E) = D,
inference(paramod,[status(thm)],[c_377,c_34]) ).
cnf(c_869,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C)))),multiply(inverse(inverse(D)),inverse(E)))),inverse(multiply(inverse(E),E)))),E) = D,
inference(paramod,[status(thm)],[c_557,c_868]) ).
cnf(c_870,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(C),C))),multiply(inverse(inverse(D)),inverse(E)))),inverse(multiply(inverse(E),E)))),E) = D,
inference(paramod,[status(thm)],[c_557,c_869]) ).
cnf(c_567,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),inverse(multiply(inverse(B),B)))),B) = A,
inference(paramod,[status(thm)],[c_566,c_870]) ).
cnf(c_871,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))) = B,
inference(paramod,[status(thm)],[c_557,c_547]) ).
cnf(c_570,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(C),C)))),multiply(inverse(D),D)) = B,
inference(paramod,[status(thm)],[c_557,c_871]) ).
cnf(c_872,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),multiply(inverse(C),C))),multiply(inverse(inverse(D)),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(D))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_557,c_498]) ).
cnf(c_873,plain,
multiply(inverse(multiply(inverse(C),C)),multiply(inverse(inverse(D)),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(D))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_566,c_872]) ).
cnf(c_874,plain,
multiply(inverse(inverse(D)),inverse(E)) = multiply(inverse(multiply(inverse(inverse(E)),inverse(D))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_557,c_873]) ).
cnf(c_578,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(C),C)) = multiply(inverse(inverse(B)),inverse(A)),
inference(copy,[status(thm)],[c_874]) ).
cnf(c_875,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(inverse(multiply(inverse(D),D))),multiply(inverse(E),E))) = multiply(inverse(multiply(F,inverse(B))),multiply(F,inverse(A))),
inference(paramod,[status(thm)],[c_557,c_496]) ).
cnf(c_876,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(E),E)) = multiply(inverse(multiply(F,inverse(B))),multiply(F,inverse(A))),
inference(paramod,[status(thm)],[c_566,c_875]) ).
cnf(c_877,plain,
multiply(inverse(inverse(B)),inverse(A)) = multiply(inverse(multiply(F,inverse(B))),multiply(F,inverse(A))),
inference(paramod,[status(thm)],[c_578,c_876]) ).
cnf(c_579,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))) = multiply(inverse(inverse(B)),inverse(C)),
inference(copy,[status(thm)],[c_877]) ).
cnf(c_878,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),D))),multiply(inverse(E),E)))) = multiply(inverse(E),E),
inference(paramod,[status(thm)],[c_557,c_359]) ).
cnf(c_879,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E)))) = multiply(inverse(E),E),
inference(paramod,[status(thm)],[c_557,c_878]) ).
cnf(c_880,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(E),E))) = multiply(inverse(E),E),
inference(paramod,[status(thm)],[c_557,c_879]) ).
cnf(c_583,plain,
inverse(multiply(inverse(A),A)) = multiply(inverse(A),A),
inference(paramod,[status(thm)],[c_557,c_880]) ).
cnf(c_881,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(C)))),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(V6),V6))))) = multiply(inverse(multiply(V7,inverse(D))),multiply(V7,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_579,c_304]) ).
cnf(c_882,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(V6),V6))))) = multiply(inverse(multiply(V7,inverse(D))),multiply(V7,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_579,c_881]) ).
cnf(c_883,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(multiply(inverse(F),F),multiply(inverse(V6),V6))))) = multiply(inverse(multiply(V7,inverse(D))),multiply(V7,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_583,c_882]) ).
cnf(c_884,plain,
multiply(inverse(inverse(D)),inverse(multiply(multiply(inverse(F),F),multiply(inverse(V6),V6)))) = multiply(inverse(multiply(V7,inverse(D))),multiply(V7,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_579,c_883]) ).
cnf(c_885,plain,
multiply(inverse(inverse(D)),inverse(multiply(multiply(inverse(F),F),multiply(inverse(V6),V6)))) = multiply(inverse(multiply(V7,inverse(D))),multiply(V7,multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_583,c_884]) ).
cnf(c_611,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C))) = multiply(inverse(inverse(B)),inverse(multiply(multiply(inverse(D),D),multiply(inverse(E),E)))),
inference(copy,[status(thm)],[c_885]) ).
cnf(c_886,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),inverse(C))),multiply(inverse(multiply(inverse(D),D)),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_583,c_274]) ).
cnf(c_887,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),inverse(C))),multiply(multiply(inverse(D),D),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_583,c_886]) ).
cnf(c_628,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),inverse(C))),multiply(multiply(inverse(D),D),inverse(E))) = multiply(inverse(inverse(C)),inverse(E)),
inference(paramod,[status(thm)],[c_578,c_887]) ).
cnf(c_888,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),inverse(C))),multiply(inverse(multiply(inverse(D),D)),inverse(E))) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(C)),inverse(E))),
inference(paramod,[status(thm)],[c_583,c_263]) ).
cnf(c_889,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),inverse(C))),multiply(multiply(inverse(D),D),inverse(E))) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(C)),inverse(E))),
inference(paramod,[status(thm)],[c_583,c_888]) ).
cnf(c_890,plain,
multiply(inverse(inverse(C)),inverse(E)) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(C)),inverse(E))),
inference(paramod,[status(thm)],[c_628,c_889]) ).
cnf(c_891,plain,
multiply(inverse(inverse(C)),inverse(E)) = multiply(multiply(inverse(F),F),multiply(inverse(inverse(C)),inverse(E))),
inference(paramod,[status(thm)],[c_583,c_890]) ).
cnf(c_638,plain,
multiply(multiply(inverse(A),A),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(inverse(B)),inverse(C)),
inference(copy,[status(thm)],[c_891]) ).
cnf(c_892,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),multiply(D,inverse(E)))),inverse(multiply(multiply(inverse(F),F),multiply(inverse(V6),V6))))),E)))) = multiply(inverse(multiply(D,inverse(B))),C),
inference(paramod,[status(thm)],[c_583,c_213]) ).
cnf(c_663,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),inverse(multiply(multiply(inverse(E),E),multiply(inverse(F),F))))),D))) = multiply(inverse(multiply(C,inverse(A))),B),
inference(paramod,[status(thm)],[c_579,c_892]) ).
cnf(c_893,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C))),inverse(D))),B) = multiply(inverse(multiply(inverse(E),E)),multiply(inverse(inverse(D)),inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_579,c_138]) ).
cnf(c_894,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C))),inverse(D))),B) = multiply(multiply(inverse(E),E),multiply(inverse(inverse(D)),inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_583,c_893]) ).
cnf(c_895,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C))),inverse(D))),B) = multiply(multiply(inverse(E),E),multiply(inverse(inverse(D)),multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_583,c_894]) ).
cnf(c_705,plain,
multiply(multiply(inverse(A),A),multiply(inverse(inverse(B)),multiply(inverse(C),C))) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(D),C))),inverse(C))),inverse(B))),D),
inference(copy,[status(thm)],[c_895]) ).
cnf(c_896,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(multiply(inverse(C),C),multiply(inverse(D),D))) = multiply(inverse(multiply(inverse(E),E)),multiply(inverse(inverse(B)),inverse(A))),
inference(paramod,[status(thm)],[c_583,c_129]) ).
cnf(c_897,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(multiply(inverse(C),C),multiply(inverse(D),D))) = multiply(multiply(inverse(E),E),multiply(inverse(inverse(B)),inverse(A))),
inference(paramod,[status(thm)],[c_583,c_896]) ).
cnf(c_709,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(multiply(inverse(C),C),multiply(inverse(D),D))) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_638,c_897]) ).
cnf(c_898,plain,
multiply(multiply(inverse(A),A),multiply(inverse(inverse(multiply(inverse(B),B))),inverse(C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(C))),
inference(paramod,[status(thm)],[c_583,c_106]) ).
cnf(c_899,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(B),B)),inverse(C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(C))),
inference(paramod,[status(thm)],[c_583,c_898]) ).
cnf(c_900,plain,
multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),inverse(C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(C))),
inference(paramod,[status(thm)],[c_583,c_899]) ).
cnf(c_711,plain,
multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),inverse(C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(multiply(inverse(D),B))),inverse(B))),inverse(C))),
inference(paramod,[status(thm)],[c_579,c_900]) ).
cnf(c_901,plain,
multiply(inverse(multiply(A,inverse(multiply(multiply(inverse(B),B),C)))),multiply(A,inverse(C))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_583,c_88]) ).
cnf(c_902,plain,
multiply(inverse(inverse(multiply(multiply(inverse(B),B),C))),inverse(C)) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_579,c_901]) ).
cnf(c_713,plain,
multiply(inverse(inverse(multiply(multiply(inverse(A),A),B))),inverse(B)) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_583,c_902]) ).
cnf(c_903,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C)))),inverse(multiply(inverse(C),C))) = B,
inference(paramod,[status(thm)],[c_583,c_70]) ).
cnf(c_904,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C))),inverse(multiply(inverse(C),C))) = B,
inference(paramod,[status(thm)],[c_638,c_903]) ).
cnf(c_905,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C))),multiply(inverse(C),C)) = B,
inference(paramod,[status(thm)],[c_583,c_904]) ).
cnf(c_717,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(B),A))) = B,
inference(paramod,[status(thm)],[c_578,c_905]) ).
cnf(c_906,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C)))),inverse(multiply(inverse(C),C)))),C) = B,
inference(paramod,[status(thm)],[c_583,c_558]) ).
cnf(c_907,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(inverse(B)),inverse(C)))),inverse(multiply(inverse(C),C)))),C) = B,
inference(paramod,[status(thm)],[c_583,c_906]) ).
cnf(c_908,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(inverse(C),C)))),C) = B,
inference(paramod,[status(thm)],[c_638,c_907]) ).
cnf(c_909,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),multiply(inverse(C),C))),C) = B,
inference(paramod,[status(thm)],[c_583,c_908]) ).
cnf(c_720,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),A) = B,
inference(paramod,[status(thm)],[c_578,c_909]) ).
cnf(c_910,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D))))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),D)))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_583,c_74]) ).
cnf(c_911,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C)))),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D))))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),D)))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_583,c_910]) ).
cnf(c_912,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C)))),inverse(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(D),D))))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),D)))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_583,c_911]) ).
cnf(c_913,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C)))),inverse(multiply(multiply(inverse(D),D),inverse(multiply(inverse(D),D))))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),D)))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_583,c_912]) ).
cnf(c_914,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C)))),inverse(multiply(multiply(inverse(D),D),multiply(inverse(D),D)))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),D)))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_583,c_913]) ).
cnf(c_732,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C)))),inverse(multiply(multiply(inverse(D),D),multiply(inverse(D),D)))) = multiply(inverse(inverse(multiply(inverse(B),D))),inverse(D)),
inference(paramod,[status(thm)],[c_579,c_914]) ).
cnf(c_915,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(A,inverse(B))))),inverse(multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(B))))) = multiply(A,inverse(multiply(inverse(multiply(inverse(C),inverse(multiply(inverse(B),B)))),B))),
inference(paramod,[status(thm)],[c_578,c_312]) ).
cnf(c_916,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(A,inverse(B))))),inverse(multiply(inverse(inverse(B)),inverse(B)))) = multiply(A,inverse(multiply(inverse(multiply(inverse(C),inverse(multiply(inverse(B),B)))),B))),
inference(paramod,[status(thm)],[c_579,c_915]) ).
cnf(c_917,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(A,inverse(B))))),multiply(inverse(inverse(B)),inverse(B))) = multiply(A,inverse(multiply(inverse(multiply(inverse(C),inverse(multiply(inverse(B),B)))),B))),
inference(paramod,[status(thm)],[c_583,c_916]) ).
cnf(c_918,plain,
multiply(inverse(inverse(multiply(A,inverse(B)))),inverse(C)) = multiply(A,inverse(multiply(inverse(multiply(inverse(C),inverse(multiply(inverse(B),B)))),B))),
inference(paramod,[status(thm)],[c_578,c_917]) ).
cnf(c_919,plain,
multiply(inverse(inverse(multiply(A,inverse(B)))),inverse(C)) = multiply(A,inverse(multiply(inverse(multiply(inverse(C),multiply(inverse(B),B))),B))),
inference(paramod,[status(thm)],[c_583,c_918]) ).
cnf(c_735,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),C))) = multiply(inverse(inverse(multiply(A,inverse(C)))),inverse(B)),
inference(copy,[status(thm)],[c_919]) ).
cnf(c_920,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_579,c_298]) ).
cnf(c_921,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_578,c_920]) ).
cnf(c_922,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),multiply(inverse(C),C))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_583,c_921]) ).
cnf(c_923,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(inverse(C)),inverse(B))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_578,c_922]) ).
cnf(c_736,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),inverse(C))),multiply(inverse(inverse(B)),inverse(A))) = multiply(inverse(multiply(D,inverse(C))),multiply(D,multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_583,c_923]) ).
cnf(c_924,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(multiply(inverse(C),C)))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_579,c_282]) ).
cnf(c_925,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),multiply(inverse(C),C))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(multiply(inverse(C),C)))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_583,c_924]) ).
cnf(c_926,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(multiply(inverse(C),C)))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_578,c_925]) ).
cnf(c_927,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(multiply(inverse(C),C)))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_579,c_926]) ).
cnf(c_928,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),multiply(inverse(C),C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_583,c_927]) ).
cnf(c_737,plain,
multiply(inverse(multiply(inverse(inverse(A)),multiply(inverse(B),B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(inverse(B)),inverse(D))),multiply(inverse(multiply(inverse(inverse(D)),inverse(B))),inverse(A))),
inference(copy,[status(thm)],[c_928]) ).
cnf(c_929,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(A),A))),A)))),multiply(inverse(C),C)) = B,
inference(paramod,[status(thm)],[c_583,c_90]) ).
cnf(c_930,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(A)),inverse(A)))),inverse(B))),multiply(inverse(C),C)) = B,
inference(paramod,[status(thm)],[c_735,c_929]) ).
cnf(c_931,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),inverse(A))),inverse(B))),multiply(inverse(C),C)) = B,
inference(paramod,[status(thm)],[c_583,c_930]) ).
cnf(c_743,plain,
multiply(inverse(multiply(multiply(inverse(inverse(A)),inverse(A)),inverse(B))),multiply(inverse(C),C)) = B,
inference(paramod,[status(thm)],[c_583,c_931]) ).
cnf(c_932,plain,
multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),inverse(multiply(inverse(A),A))) = B,
inference(paramod,[status(thm)],[c_717,c_71]) ).
cnf(c_745,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(B),B))),multiply(inverse(C),C)) = A,
inference(paramod,[status(thm)],[c_583,c_932]) ).
cnf(c_933,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C)))),inverse(multiply(inverse(C),C)))),multiply(inverse(D),D)) = B,
inference(paramod,[status(thm)],[c_583,c_570]) ).
cnf(c_934,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C)))),multiply(inverse(C),C))),multiply(inverse(D),D)) = B,
inference(paramod,[status(thm)],[c_583,c_933]) ).
cnf(c_746,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C))) = B,
inference(paramod,[status(thm)],[c_745,c_934]) ).
cnf(c_935,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(V6),V6)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_579,c_280]) ).
cnf(c_936,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),multiply(inverse(C),C))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(V6),V6)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_583,c_935]) ).
cnf(c_937,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(V6),V6)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_578,c_936]) ).
cnf(c_938,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(V6),V6)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_579,c_937]) ).
cnf(c_749,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(A))),inverse(C))) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_583,c_938]) ).
cnf(c_939,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),multiply(inverse(D),D))),multiply(inverse(E),E))),E)))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(B))),C),
inference(paramod,[status(thm)],[c_583,c_209]) ).
cnf(c_940,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(C),E)))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(B))),C),
inference(paramod,[status(thm)],[c_745,c_939]) ).
cnf(c_941,plain,
multiply(inverse(inverse(B)),inverse(multiply(inverse(C),E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(B))),C),
inference(paramod,[status(thm)],[c_579,c_940]) ).
cnf(c_752,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),C) = multiply(inverse(inverse(B)),inverse(multiply(inverse(C),A))),
inference(copy,[status(thm)],[c_941]) ).
cnf(c_942,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),multiply(inverse(D),D))),D)))),multiply(A,inverse(E))) = multiply(inverse(B),multiply(inverse(inverse(D)),inverse(E))),
inference(paramod,[status(thm)],[c_583,c_157]) ).
cnf(c_943,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),D)))),multiply(A,inverse(E))) = multiply(inverse(B),multiply(inverse(inverse(D)),inverse(E))),
inference(paramod,[status(thm)],[c_745,c_942]) ).
cnf(c_754,plain,
multiply(inverse(inverse(multiply(inverse(A),B))),inverse(C)) = multiply(inverse(A),multiply(inverse(inverse(B)),inverse(C))),
inference(paramod,[status(thm)],[c_579,c_943]) ).
cnf(c_944,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(B),B))),B) = A,
inference(paramod,[status(thm)],[c_583,c_567]) ).
cnf(c_945,plain,
multiply(inverse(multiply(inverse(inverse(B)),inverse(multiply(inverse(multiply(inverse(B),B)),A)))),B) = A,
inference(paramod,[status(thm)],[c_752,c_944]) ).
cnf(c_946,plain,
multiply(inverse(multiply(inverse(inverse(B)),inverse(multiply(multiply(inverse(B),B),A)))),B) = A,
inference(paramod,[status(thm)],[c_583,c_945]) ).
cnf(c_768,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_720,c_946]) ).
cnf(c_947,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),multiply(inverse(B),B))),inverse(multiply(inverse(C),C)))),multiply(inverse(C),C)) = A,
inference(paramod,[status(thm)],[c_583,c_565]) ).
cnf(c_948,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),multiply(inverse(B),B))),multiply(inverse(C),C))),multiply(inverse(C),C)) = A,
inference(paramod,[status(thm)],[c_583,c_947]) ).
cnf(c_769,plain,
multiply(inverse(inverse(A)),multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_745,c_948]) ).
cnf(c_949,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(D),D)))),D))),
inference(paramod,[status(thm)],[c_583,c_317]) ).
cnf(c_950,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(D),D))),D))),
inference(paramod,[status(thm)],[c_583,c_949]) ).
cnf(c_770,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),D))) = multiply(inverse(inverse(multiply(A,inverse(D)))),inverse(B)),
inference(paramod,[status(thm)],[c_735,c_950]) ).
cnf(c_951,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(inverse(C)),inverse(D)))),multiply(inverse(D),D))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))),C))),
inference(paramod,[status(thm)],[c_583,c_226]) ).
cnf(c_952,plain,
multiply(inverse(inverse(multiply(A,inverse(D)))),inverse(multiply(inverse(B),multiply(inverse(inverse(C)),inverse(D))))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))),C))),
inference(paramod,[status(thm)],[c_735,c_951]) ).
cnf(c_953,plain,
multiply(inverse(inverse(multiply(A,inverse(D)))),inverse(multiply(inverse(B),multiply(inverse(inverse(C)),inverse(D))))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(E),E))),multiply(inverse(C),C))),C))),
inference(paramod,[status(thm)],[c_583,c_952]) ).
cnf(c_772,plain,
multiply(inverse(inverse(multiply(A,inverse(B)))),inverse(multiply(inverse(C),multiply(inverse(inverse(D)),inverse(B))))) = multiply(A,inverse(multiply(inverse(C),D))),
inference(paramod,[status(thm)],[c_745,c_953]) ).
cnf(c_954,plain,
multiply(inverse(A),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(inverse(B)),inverse(D))),multiply(inverse(multiply(inverse(inverse(D)),inverse(B))),inverse(A))),
inference(paramod,[status(thm)],[c_769,c_737]) ).
cnf(c_955,plain,
multiply(inverse(A),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(inverse(B)),inverse(D))),multiply(inverse(inverse(B)),inverse(multiply(inverse(inverse(A)),D)))),
inference(paramod,[status(thm)],[c_752,c_954]) ).
cnf(c_956,plain,
multiply(inverse(A),multiply(inverse(C),C)) = multiply(inverse(inverse(D)),inverse(multiply(inverse(inverse(A)),D))),
inference(paramod,[status(thm)],[c_579,c_955]) ).
cnf(c_778,plain,
multiply(inverse(A),multiply(inverse(B),B)) = inverse(A),
inference(paramod,[status(thm)],[c_717,c_956]) ).
cnf(c_957,plain,
multiply(inverse(multiply(inverse(inverse(B)),inverse(multiply(inverse(inverse(C)),A)))),multiply(inverse(inverse(B)),inverse(A))) = multiply(inverse(multiply(D,inverse(C))),multiply(D,multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_752,c_736]) ).
cnf(c_958,plain,
multiply(inverse(inverse(multiply(inverse(inverse(C)),A))),inverse(A)) = multiply(inverse(multiply(D,inverse(C))),multiply(D,multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_579,c_957]) ).
cnf(c_959,plain,
multiply(inverse(inverse(C)),multiply(inverse(inverse(A)),inverse(A))) = multiply(inverse(multiply(D,inverse(C))),multiply(D,multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_754,c_958]) ).
cnf(c_960,plain,
inverse(inverse(C)) = multiply(inverse(multiply(D,inverse(C))),multiply(D,multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_778,c_959]) ).
cnf(c_779,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_746,c_960]) ).
cnf(c_961,plain,
multiply(inverse(B),inverse(multiply(multiply(inverse(D),D),multiply(inverse(D),D)))) = multiply(inverse(inverse(multiply(inverse(B),D))),inverse(D)),
inference(paramod,[status(thm)],[c_746,c_732]) ).
cnf(c_962,plain,
multiply(inverse(B),inverse(multiply(inverse(D),D))) = multiply(inverse(inverse(multiply(inverse(B),D))),inverse(D)),
inference(paramod,[status(thm)],[c_768,c_961]) ).
cnf(c_963,plain,
multiply(inverse(B),multiply(inverse(D),D)) = multiply(inverse(inverse(multiply(inverse(B),D))),inverse(D)),
inference(paramod,[status(thm)],[c_583,c_962]) ).
cnf(c_964,plain,
inverse(B) = multiply(inverse(inverse(multiply(inverse(B),D))),inverse(D)),
inference(paramod,[status(thm)],[c_778,c_963]) ).
cnf(c_965,plain,
inverse(B) = multiply(multiply(inverse(B),D),inverse(D)),
inference(paramod,[status(thm)],[c_779,c_964]) ).
cnf(c_780,plain,
multiply(multiply(inverse(A),B),inverse(B)) = inverse(A),
inference(copy,[status(thm)],[c_965]) ).
cnf(c_966,plain,
B = multiply(inverse(inverse(B)),inverse(multiply(multiply(inverse(D),D),multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_746,c_611]) ).
cnf(c_967,plain,
B = multiply(B,inverse(multiply(multiply(inverse(D),D),multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_779,c_966]) ).
cnf(c_968,plain,
B = multiply(B,inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_768,c_967]) ).
cnf(c_969,plain,
B = multiply(B,multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_583,c_968]) ).
cnf(c_782,plain,
multiply(A,multiply(inverse(B),B)) = A,
inference(copy,[status(thm)],[c_969]) ).
cnf(c_970,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(A))),inverse(C))) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_779,c_749]) ).
cnf(c_971,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(inverse(multiply(B,inverse(A))),inverse(C))) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_779,c_970]) ).
cnf(c_786,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(inverse(multiply(B,inverse(A))),inverse(C))) = multiply(inverse(D),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_782,c_971]) ).
cnf(c_972,plain,
multiply(multiply(inverse(A),A),inverse(C)) = multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(multiply(inverse(D),B))),inverse(B))),inverse(C))),
inference(paramod,[status(thm)],[c_768,c_711]) ).
cnf(c_973,plain,
inverse(C) = multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(multiply(inverse(D),B))),inverse(B))),inverse(C))),
inference(paramod,[status(thm)],[c_768,c_972]) ).
cnf(c_974,plain,
inverse(C) = multiply(inverse(D),multiply(inverse(multiply(multiply(inverse(D),B),inverse(B))),inverse(C))),
inference(paramod,[status(thm)],[c_779,c_973]) ).
cnf(c_975,plain,
inverse(C) = multiply(inverse(D),multiply(inverse(inverse(D)),inverse(C))),
inference(paramod,[status(thm)],[c_780,c_974]) ).
cnf(c_976,plain,
inverse(C) = multiply(inverse(D),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_779,c_975]) ).
cnf(c_790,plain,
multiply(inverse(A),multiply(A,inverse(B))) = inverse(B),
inference(copy,[status(thm)],[c_976]) ).
cnf(c_977,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(multiply(inverse(C),C),multiply(inverse(D),D))) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_779,c_709]) ).
cnf(c_978,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(inverse(C),C)) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_782,c_977]) ).
cnf(c_979,plain,
inverse(multiply(A,inverse(B))) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_782,c_978]) ).
cnf(c_791,plain,
inverse(multiply(A,inverse(B))) = multiply(B,inverse(A)),
inference(paramod,[status(thm)],[c_779,c_979]) ).
cnf(c_980,plain,
multiply(multiply(inverse(A),A),multiply(B,multiply(inverse(C),C))) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(D),C))),inverse(C))),inverse(B))),D),
inference(paramod,[status(thm)],[c_779,c_705]) ).
cnf(c_981,plain,
multiply(multiply(inverse(A),A),B) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(D),C))),inverse(C))),inverse(B))),D),
inference(paramod,[status(thm)],[c_782,c_980]) ).
cnf(c_982,plain,
B = multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(D),C))),inverse(C))),inverse(B))),D),
inference(paramod,[status(thm)],[c_768,c_981]) ).
cnf(c_983,plain,
B = multiply(inverse(multiply(inverse(multiply(multiply(inverse(D),C),inverse(C))),inverse(B))),D),
inference(paramod,[status(thm)],[c_779,c_982]) ).
cnf(c_984,plain,
B = multiply(inverse(multiply(inverse(inverse(D)),inverse(B))),D),
inference(paramod,[status(thm)],[c_780,c_983]) ).
cnf(c_985,plain,
B = multiply(inverse(multiply(D,inverse(B))),D),
inference(paramod,[status(thm)],[c_779,c_984]) ).
cnf(c_986,plain,
B = multiply(multiply(B,inverse(D)),D),
inference(paramod,[status(thm)],[c_791,c_985]) ).
cnf(c_792,plain,
multiply(multiply(A,inverse(B)),B) = A,
inference(copy,[status(thm)],[c_986]) ).
cnf(c_987,plain,
multiply(inverse(multiply(multiply(A,inverse(A)),inverse(B))),multiply(inverse(C),C)) = B,
inference(paramod,[status(thm)],[c_779,c_743]) ).
cnf(c_988,plain,
multiply(multiply(B,inverse(multiply(A,inverse(A)))),multiply(inverse(C),C)) = B,
inference(paramod,[status(thm)],[c_791,c_987]) ).
cnf(c_989,plain,
multiply(multiply(B,multiply(A,inverse(A))),multiply(inverse(C),C)) = B,
inference(paramod,[status(thm)],[c_791,c_988]) ).
cnf(c_800,plain,
multiply(A,multiply(B,inverse(B))) = A,
inference(paramod,[status(thm)],[c_782,c_989]) ).
cnf(c_990,plain,
multiply(inverse(inverse(B)),inverse(B)) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_768,c_713]) ).
cnf(c_991,plain,
multiply(B,inverse(B)) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_779,c_990]) ).
cnf(c_801,plain,
multiply(inverse(A),A) = multiply(A,inverse(A)),
inference(copy,[status(thm)],[c_991]) ).
cnf(c_992,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),inverse(multiply(multiply(inverse(E),E),multiply(inverse(F),F))))),D))) = multiply(inverse(multiply(C,inverse(A))),B),
inference(paramod,[status(thm)],[c_779,c_663]) ).
cnf(c_993,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),inverse(multiply(multiply(E,inverse(E)),multiply(inverse(F),F))))),D))) = multiply(inverse(multiply(C,inverse(A))),B),
inference(paramod,[status(thm)],[c_801,c_992]) ).
cnf(c_994,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),inverse(multiply(multiply(E,inverse(E)),multiply(F,inverse(F)))))),D))) = multiply(inverse(multiply(C,inverse(A))),B),
inference(paramod,[status(thm)],[c_801,c_993]) ).
cnf(c_995,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),inverse(multiply(E,inverse(E))))),D))) = multiply(inverse(multiply(C,inverse(A))),B),
inference(paramod,[status(thm)],[c_800,c_994]) ).
cnf(c_996,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),multiply(E,inverse(E)))),D))) = multiply(inverse(multiply(C,inverse(A))),B),
inference(paramod,[status(thm)],[c_791,c_995]) ).
cnf(c_997,plain,
multiply(A,inverse(multiply(inverse(inverse(multiply(inverse(B),multiply(C,inverse(D))))),D))) = multiply(inverse(multiply(C,inverse(A))),B),
inference(paramod,[status(thm)],[c_800,c_996]) ).
cnf(c_998,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(C,inverse(D))),D))) = multiply(inverse(multiply(C,inverse(A))),B),
inference(paramod,[status(thm)],[c_779,c_997]) ).
cnf(c_803,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(C,inverse(D))),D))) = multiply(multiply(A,inverse(C)),B),
inference(paramod,[status(thm)],[c_791,c_998]) ).
cnf(c_810,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(b2,inverse(b2)),a2) != a2 ),
inference(paramod,[status(thm)],[c_801,c_68]) ).
cnf(c_999,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(C)))),D))) = multiply(inverse(inverse(multiply(A,inverse(D)))),inverse(B)),
inference(paramod,[status(thm)],[c_801,c_770]) ).
cnf(c_1000,plain,
multiply(A,inverse(multiply(inverse(inverse(B)),D))) = multiply(inverse(inverse(multiply(A,inverse(D)))),inverse(B)),
inference(paramod,[status(thm)],[c_800,c_999]) ).
cnf(c_1001,plain,
multiply(A,inverse(multiply(B,D))) = multiply(inverse(inverse(multiply(A,inverse(D)))),inverse(B)),
inference(paramod,[status(thm)],[c_779,c_1000]) ).
cnf(c_1002,plain,
multiply(A,inverse(multiply(B,D))) = multiply(inverse(multiply(D,inverse(A))),inverse(B)),
inference(paramod,[status(thm)],[c_791,c_1001]) ).
cnf(c_1003,plain,
multiply(A,inverse(multiply(B,D))) = multiply(multiply(A,inverse(D)),inverse(B)),
inference(paramod,[status(thm)],[c_791,c_1002]) ).
cnf(c_812,plain,
multiply(multiply(A,inverse(B)),inverse(C)) = multiply(A,inverse(multiply(C,B))),
inference(copy,[status(thm)],[c_1003]) ).
cnf(c_1004,plain,
multiply(inverse(multiply(B,inverse(A))),inverse(multiply(inverse(C),multiply(inverse(inverse(D)),inverse(B))))) = multiply(A,inverse(multiply(inverse(C),D))),
inference(paramod,[status(thm)],[c_791,c_772]) ).
cnf(c_1005,plain,
multiply(multiply(A,inverse(B)),inverse(multiply(inverse(C),multiply(inverse(inverse(D)),inverse(B))))) = multiply(A,inverse(multiply(inverse(C),D))),
inference(paramod,[status(thm)],[c_791,c_1004]) ).
cnf(c_1006,plain,
multiply(multiply(A,inverse(B)),inverse(multiply(inverse(C),multiply(D,inverse(B))))) = multiply(A,inverse(multiply(inverse(C),D))),
inference(paramod,[status(thm)],[c_779,c_1005]) ).
cnf(c_1007,plain,
multiply(A,inverse(multiply(multiply(inverse(C),multiply(D,inverse(B))),B))) = multiply(A,inverse(multiply(inverse(C),D))),
inference(paramod,[status(thm)],[c_812,c_1006]) ).
cnf(c_814,plain,
multiply(multiply(A,inverse(B)),C) = multiply(A,inverse(multiply(inverse(C),B))),
inference(paramod,[status(thm)],[c_803,c_1007]) ).
cnf(c_1008,plain,
multiply(multiply(B,inverse(A)),multiply(inverse(multiply(B,inverse(A))),inverse(C))) = multiply(inverse(D),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_791,c_786]) ).
cnf(c_1009,plain,
multiply(multiply(B,inverse(A)),multiply(multiply(A,inverse(B)),inverse(C))) = multiply(inverse(D),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_791,c_1008]) ).
cnf(c_1010,plain,
multiply(multiply(B,inverse(A)),multiply(A,inverse(multiply(inverse(inverse(C)),B)))) = multiply(inverse(D),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_814,c_1009]) ).
cnf(c_1011,plain,
multiply(multiply(B,inverse(A)),multiply(A,inverse(multiply(C,B)))) = multiply(inverse(D),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_779,c_1010]) ).
cnf(c_1012,plain,
multiply(B,inverse(multiply(inverse(multiply(A,inverse(multiply(C,B)))),A))) = multiply(inverse(D),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_814,c_1011]) ).
cnf(c_1013,plain,
multiply(B,inverse(multiply(multiply(multiply(C,B),inverse(A)),A))) = multiply(inverse(D),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_791,c_1012]) ).
cnf(c_1014,plain,
multiply(B,inverse(multiply(C,B))) = multiply(inverse(D),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_792,c_1013]) ).
cnf(c_816,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(paramod,[status(thm)],[c_790,c_1014]) ).
cnf(c_1015,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(b2,inverse(multiply(inverse(a2),b2))) != a2 ),
inference(paramod,[status(thm)],[c_814,c_810]) ).
cnf(c_1016,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| inverse(inverse(a2)) != a2 ),
inference(paramod,[status(thm)],[c_816,c_1015]) ).
cnf(c_1017,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_779,c_1016]) ).
cnf(c_820,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(copy,[status(thm)],[c_1017]) ).
cnf(c_827,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(paramod,[status(thm)],[c_779,c_791]) ).
cnf(c_1018,plain,
inverse(multiply(multiply(A,inverse(B)),inverse(C))) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_791,c_791]) ).
cnf(c_1019,plain,
inverse(multiply(A,inverse(multiply(inverse(inverse(C)),B)))) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_814,c_1018]) ).
cnf(c_1020,plain,
inverse(multiply(A,inverse(multiply(C,B)))) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_779,c_1019]) ).
cnf(c_1021,plain,
inverse(multiply(A,multiply(inverse(B),inverse(C)))) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_827,c_1020]) ).
cnf(c_1022,plain,
multiply(inverse(multiply(inverse(B),inverse(C))),inverse(A)) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_827,c_1021]) ).
cnf(c_1023,plain,
multiply(multiply(inverse(inverse(C)),inverse(inverse(B))),inverse(A)) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_827,c_1022]) ).
cnf(c_1024,plain,
multiply(multiply(C,inverse(inverse(B))),inverse(A)) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_779,c_1023]) ).
cnf(c_829,plain,
multiply(multiply(A,B),inverse(C)) = multiply(A,multiply(B,inverse(C))),
inference(paramod,[status(thm)],[c_779,c_1024]) ).
cnf(c_1025,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,inverse(inverse(C)))),
inference(paramod,[status(thm)],[c_779,c_829]) ).
cnf(c_838,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_779,c_1025]) ).
cnf(c_839,plain,
$false,
inference(resolve,[status(thm)],[c_838,c_820]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP056-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.42 % Computer : n002.cluster.edu
% 0.18/0.42 % Model : x86_64 x86_64
% 0.18/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.42 % Memory : 8046.5625MB
% 0.18/0.42 % OS : Linux 6.8.0-71-generic
% 0.18/0.42 % CPULimit : 300
% 0.18/0.42 % WCLimit : 300
% 0.18/0.42 % DateTime : Fri Sep 25 14:22:49 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.43 % Process 3478375 was started by sandbox2 on n002,
% 0.18/0.43 % Fri Sep 25 14:22:49 2026
% 0.18/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.43
% 0.18/0.43 % From the command line: assign(max_seconds, 300).
% 3.98/1.00
% 3.98/1.00 % Assigning unary symbol inverse kb_weight 0 and highest precedence (10).
% 3.98/1.00
% 3.98/1.00 % SZS status Unsatisfiable for theBenchmark
% 3.98/1.00
% 3.98/1.00 % Proof 1 at 0.40 (+ 0.12) seconds.
% 3.98/1.00 % Length of proof is 120.
% 3.98/1.00 % Level of proof is 28.
% 3.98/1.00 % Maximum clause weight is 100.000.
% 3.98/1.00 % Given clauses 61.
% 3.98/1.00
% 3.98/1.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------