%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP054-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 : 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:26:39 AM UTC 2026
% Result : Unsatisfiable 42.09s 6.54s
% Output : CNFRefutation 42.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 84
% Number of leaves : 2
% Syntax : Number of formulae : 251 ( 245 unt; 0 def)
% Number of atoms : 261 ( 260 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 28 ( 18 ~; 10 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 18 ( 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 : 955 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : inverse(multiply(inverse(multiply(VAR_0,inverse(multiply(inverse(VAR_1),inverse(multiply(VAR_2,inverse(multiply(inverse(VAR_2),VAR_2)))))))),multiply(VAR_0,VAR_2))) = VAR_1,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),multiply(A,C))) = B,
inference(clausify,[status(thm)],[single_axiom]) ).
fof(prove_these_axioms,axiom,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
file('theBenchmark.p',prove_these_axioms) ).
cnf(c_2,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(clausify,[status(thm)],[prove_these_axioms]) ).
cnf(c_8947,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_3,plain,
( multiply(a3,multiply(b3,c3)) != multiply(multiply(a3,b3),c3)
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ),
inference(copy,[status(thm)],[c_8947]) ).
cnf(c_8948,plain,
inverse(multiply(inverse(multiply(A,inverse(multiply(B,inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),multiply(A,C))) = multiply(inverse(multiply(D,inverse(multiply(inverse(B),inverse(multiply(E,inverse(multiply(inverse(E),E)))))))),multiply(D,E)),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_4,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),multiply(A,C)) = inverse(multiply(inverse(multiply(D,inverse(multiply(B,inverse(multiply(E,inverse(multiply(inverse(E),E)))))))),multiply(D,E))),
inference(copy,[status(thm)],[c_8948]) ).
cnf(c_6,plain,
inverse(inverse(multiply(inverse(multiply(A,inverse(multiply(B,inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),multiply(A,C)))) = B,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_8,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(B)),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),multiply(A,C)) = B,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_15,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),inverse(multiply(D,inverse(multiply(multiply(A,C),inverse(multiply(inverse(multiply(A,C)),multiply(A,C))))))))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(E,F)))))) = D,
inference(paramod,[status(thm)],[c_4,c_6]) ).
cnf(c_17,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(B)),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),inverse(multiply(inverse(D),inverse(multiply(multiply(A,C),inverse(multiply(inverse(multiply(A,C)),multiply(A,C))))))))),B)) = D,
inference(paramod,[status(thm)],[c_8,c_1]) ).
cnf(c_18,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(B)),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),inverse(multiply(inverse(D),inverse(multiply(multiply(A,C),inverse(multiply(inverse(multiply(A,C)),multiply(A,C))))))))),B) = inverse(multiply(inverse(multiply(E,inverse(multiply(D,inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(E,F))),
inference(paramod,[status(thm)],[c_8,c_4]) ).
cnf(c_20,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),inverse(multiply(inverse(inverse(D)),inverse(multiply(multiply(A,C),inverse(multiply(inverse(multiply(A,C)),multiply(A,C))))))))),inverse(multiply(inverse(multiply(E,inverse(multiply(B,inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(E,F)))) = D,
inference(paramod,[status(thm)],[c_4,c_8]) ).
cnf(c_8949,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = multiply(inverse(multiply(D,inverse(multiply(inverse(inverse(inverse(multiply(C,inverse(multiply(inverse(C),C)))))),inverse(multiply(E,inverse(multiply(inverse(E),E)))))))),inverse(multiply(inverse(B),inverse(multiply(multiply(D,E),inverse(multiply(inverse(multiply(D,E)),multiply(D,E)))))))),
inference(paramod,[status(thm)],[c_17,c_1]) ).
cnf(c_36,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(inverse(multiply(B,inverse(multiply(inverse(B),B)))))),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),inverse(multiply(inverse(D),inverse(multiply(multiply(A,C),inverse(multiply(inverse(multiply(A,C)),multiply(A,C)))))))) = inverse(multiply(inverse(multiply(E,D)),multiply(E,B))),
inference(copy,[status(thm)],[c_8949]) ).
cnf(c_8950,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))),multiply(inverse(multiply(D,inverse(multiply(inverse(inverse(inverse(multiply(C,inverse(multiply(inverse(C),C)))))),inverse(multiply(E,inverse(multiply(inverse(E),E)))))))),multiply(D,E)))) = B,
inference(paramod,[status(thm)],[c_36,c_1]) ).
cnf(c_58,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))),inverse(multiply(C,inverse(multiply(inverse(C),C)))))) = B,
inference(paramod,[status(thm)],[c_8,c_8950]) ).
cnf(c_8951,plain,
multiply(inverse(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,C)))),multiply(inverse(multiply(D,inverse(multiply(inverse(inverse(inverse(multiply(C,inverse(multiply(inverse(C),C)))))),inverse(multiply(E,inverse(multiply(inverse(E),E)))))))),multiply(D,E))) = B,
inference(paramod,[status(thm)],[c_36,c_8]) ).
cnf(c_63,plain,
multiply(inverse(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,C)))),inverse(multiply(C,inverse(multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_8,c_8951]) ).
cnf(c_76,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),
inference(paramod,[status(thm)],[c_36,c_36]) ).
cnf(c_8952,plain,
inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,D))),inverse(multiply(E,inverse(multiply(inverse(E),E)))))))),multiply(A,E))) = multiply(inverse(multiply(F,C)),multiply(F,D)),
inference(paramod,[status(thm)],[c_76,c_1]) ).
cnf(c_77,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_1,c_8952]) ).
cnf(c_8953,plain,
multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),D)) = multiply(inverse(multiply(E,multiply(B,C))),multiply(E,D)),
inference(paramod,[status(thm)],[c_1,c_77]) ).
cnf(c_132,plain,
multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D)) = multiply(E,multiply(inverse(multiply(B,inverse(multiply(inverse(E),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),D)),
inference(copy,[status(thm)],[c_8953]) ).
cnf(c_152,plain,
inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))) = inverse(inverse(multiply(inverse(multiply(D,B)),multiply(D,C)))),
inference(paramod,[status(thm)],[c_58,c_6]) ).
cnf(c_178,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,C)))),D)),B) = multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))),
inference(paramod,[status(thm)],[c_63,c_77]) ).
cnf(c_198,plain,
inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,C)))),D)),B))) = inverse(inverse(multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),
inference(paramod,[status(thm)],[c_63,c_152]) ).
cnf(c_214,plain,
multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,C))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_8,c_132]) ).
cnf(c_247,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))),multiply(E,F)))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_132,c_152]) ).
cnf(c_8954,plain,
multiply(inverse(A),multiply(inverse(multiply(B,inverse(multiply(inverse(inverse(A)),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),multiply(B,C))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_8,c_214]) ).
cnf(c_293,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_8,c_8954]) ).
cnf(c_364,plain,
( multiply(a3,multiply(b3,c3)) != multiply(multiply(a3,b3),c3)
| multiply(multiply(inverse(b2),b2),a2) != a2 ),
inference(resolve,[status(thm)],[c_293,c_3]) ).
cnf(c_8955,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,C)) = inverse(multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(C,inverse(multiply(inverse(C),C)))),inverse(multiply(E,inverse(multiply(inverse(E),E)))))))),multiply(D,E))),
inference(paramod,[status(thm)],[c_293,c_4]) ).
cnf(c_370,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,C)) = multiply(C,inverse(multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_1,c_8955]) ).
cnf(c_376,plain,
inverse(inverse(multiply(inverse(multiply(A,inverse(multiply(B,inverse(multiply(C,inverse(multiply(inverse(D),D)))))))),multiply(A,C)))) = B,
inference(paramod,[status(thm)],[c_293,c_6]) ).
cnf(c_380,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(B)),inverse(multiply(C,inverse(multiply(inverse(D),D)))))))),multiply(A,C)) = B,
inference(paramod,[status(thm)],[c_293,c_8]) ).
cnf(c_8956,plain,
inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(multiply(B,C)),multiply(B,C))),
inference(paramod,[status(thm)],[c_293,c_76]) ).
cnf(c_401,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,B))) = inverse(multiply(inverse(C),C)),
inference(copy,[status(thm)],[c_8956]) ).
cnf(c_406,plain,
inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(B,inverse(multiply(inverse(B),B)))))) = B,
inference(paramod,[status(thm)],[c_293,c_58]) ).
cnf(c_411,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),inverse(multiply(inverse(inverse(B)),inverse(B)))))) = B,
inference(paramod,[status(thm)],[c_293,c_63]) ).
cnf(c_429,plain,
inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(B),B)),
inference(paramod,[status(thm)],[c_293,c_401]) ).
cnf(c_431,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_429,c_293]) ).
cnf(c_499,plain,
inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(B,inverse(multiply(inverse(C),C)))))) = B,
inference(paramod,[status(thm)],[c_293,c_406]) ).
cnf(c_525,plain,
inverse(multiply(inverse(A),A)) = inverse(inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_293,c_499]) ).
cnf(c_555,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_525,c_293]) ).
cnf(c_578,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,inverse(multiply(inverse(C),C)))))) = B,
inference(paramod,[status(thm)],[c_525,c_499]) ).
cnf(c_582,plain,
inverse(multiply(inverse(A),A)) = inverse(inverse(inverse(multiply(inverse(B),B)))),
inference(paramod,[status(thm)],[c_499,c_525]) ).
cnf(c_586,plain,
inverse(multiply(inverse(A),A)) = inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_525,c_525]) ).
cnf(c_616,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_499,c_555]) ).
cnf(c_618,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(B),B)))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_499,c_555]) ).
cnf(c_623,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(C),C))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_525,c_555]) ).
cnf(c_624,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C))))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_525,c_555]) ).
cnf(c_653,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,inverse(inverse(multiply(inverse(C),C))))))) = B,
inference(paramod,[status(thm)],[c_499,c_578]) ).
cnf(c_8957,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),inverse(multiply(C,inverse(multiply(multiply(A,B),inverse(multiply(inverse(multiply(A,B)),multiply(A,B))))))))),inverse(multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(E),E)),inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(D,F)))))) = C,
inference(paramod,[status(thm)],[c_499,c_15]) ).
cnf(c_762,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),inverse(multiply(C,inverse(multiply(multiply(A,B),inverse(multiply(inverse(multiply(A,B)),multiply(A,B))))))))),inverse(multiply(inverse(multiply(D,E)),multiply(D,E)))))) = C,
inference(paramod,[status(thm)],[c_578,c_8957]) ).
cnf(c_8958,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))))))),inverse(multiply(D,inverse(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C))))))))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))))) = D,
inference(paramod,[status(thm)],[c_555,c_15]) ).
cnf(c_8959,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),inverse(inverse(multiply(inverse(C),C))))))),inverse(multiply(D,inverse(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C))))))))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))))) = D,
inference(paramod,[status(thm)],[c_578,c_8958]) ).
cnf(c_780,plain,
inverse(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(B,inverse(multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),E)))),multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),E))))))))))),inverse(multiply(inverse(multiply(F,inverse(multiply(A,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))))) = B,
inference(paramod,[status(thm)],[c_653,c_8959]) ).
cnf(c_8960,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(B)),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),multiply(A,C))),B) = inverse(multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(E),E)),inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(D,F))),
inference(paramod,[status(thm)],[c_499,c_18]) ).
cnf(c_8961,plain,
multiply(inverse(B),B) = inverse(multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(E),E)),inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(D,F))),
inference(paramod,[status(thm)],[c_380,c_8960]) ).
cnf(c_1889,plain,
multiply(inverse(A),A) = inverse(multiply(inverse(multiply(B,C)),multiply(B,C))),
inference(paramod,[status(thm)],[c_578,c_8961]) ).
cnf(c_2034,plain,
multiply(inverse(A),A) = inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_293,c_1889]) ).
cnf(c_2035,plain,
multiply(inverse(A),A) = inverse(multiply(inverse(B),B)),
inference(paramod,[status(thm)],[c_293,c_1889]) ).
cnf(c_2039,plain,
multiply(multiply(inverse(A),A),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_1889,c_431]) ).
cnf(c_2067,plain,
multiply(inverse(A),A) = inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_555,c_1889]) ).
cnf(c_2069,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(B,inverse(multiply(inverse(C),C)))))) = B,
inference(paramod,[status(thm)],[c_1889,c_578]) ).
cnf(c_2071,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_1889,c_578]) ).
cnf(c_2093,plain,
multiply(inverse(A),A) = inverse(multiply(inverse(multiply(inverse(B),B)),inverse(inverse(multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_618,c_1889]) ).
cnf(c_2096,plain,
multiply(inverse(A),A) = inverse(inverse(inverse(multiply(inverse(B),B)))),
inference(paramod,[status(thm)],[c_1889,c_582]) ).
cnf(c_2130,plain,
multiply(inverse(A),A) = inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_1889,c_586]) ).
cnf(c_2171,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_525,c_2035]) ).
cnf(c_2182,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_2035,c_616]) ).
cnf(c_2194,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(C),C))) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2035,c_623]) ).
cnf(c_2313,plain,
inverse(multiply(inverse(multiply(inverse(A),B)),inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,A))),
inference(paramod,[status(thm)],[c_2067,c_76]) ).
cnf(c_2900,plain,
inverse(inverse(multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(B),B)),C)))) = inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)))),
inference(paramod,[status(thm)],[c_2034,c_152]) ).
cnf(c_3191,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(B,multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_2035,c_2069]) ).
cnf(c_3206,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(B,multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D))))))) = B,
inference(paramod,[status(thm)],[c_2171,c_2069]) ).
cnf(c_3245,plain,
inverse(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(B,inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))))))),inverse(multiply(inverse(multiply(E,inverse(multiply(A,inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(E,F)))))) = B,
inference(paramod,[status(thm)],[c_3206,c_780]) ).
cnf(c_3249,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(B,C)),multiply(B,D))))) = inverse(multiply(inverse(D),C)),
inference(paramod,[status(thm)],[c_76,c_2071]) ).
cnf(c_8962,plain,
inverse(inverse(multiply(A,multiply(inverse(multiply(inverse(B),B)),C)))) = inverse(inverse(multiply(inverse(multiply(D,inverse(multiply(A,multiply(inverse(E),E))))),multiply(D,C)))),
inference(paramod,[status(thm)],[c_2071,c_152]) ).
cnf(c_3251,plain,
inverse(inverse(multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(C),C))))),multiply(A,D)))) = inverse(inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D)))),
inference(copy,[status(thm)],[c_8962]) ).
cnf(c_3252,plain,
inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))),inverse(multiply(inverse(multiply(D,B)),multiply(D,C))))),inverse(multiply(E,multiply(inverse(F),F))))) = E,
inference(paramod,[status(thm)],[c_152,c_2071]) ).
cnf(c_3253,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(inverse(multiply(inverse(multiply(C,D)),multiply(C,E)))),inverse(multiply(inverse(multiply(F,D)),multiply(F,E)))))))) = B,
inference(paramod,[status(thm)],[c_152,c_2071]) ).
cnf(c_8963,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))))))),inverse(multiply(inverse(inverse(D)),inverse(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C))))))))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))) = D,
inference(paramod,[status(thm)],[c_555,c_20]) ).
cnf(c_8964,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),inverse(inverse(multiply(inverse(C),C))))))),inverse(multiply(inverse(inverse(D)),inverse(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C))))))))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))) = D,
inference(paramod,[status(thm)],[c_578,c_8963]) ).
cnf(c_8965,plain,
multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(inverse(D)),inverse(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C))))))))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))) = D,
inference(paramod,[status(thm)],[c_653,c_8964]) ).
cnf(c_4008,plain,
multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(inverse(B)),inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))))))),inverse(multiply(inverse(multiply(E,inverse(multiply(A,inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(E,F)))) = B,
inference(paramod,[status(thm)],[c_3206,c_8965]) ).
cnf(c_8966,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(B),inverse(multiply(A,inverse(multiply(inverse(A),A)))))))),inverse(multiply(inverse(inverse(C)),inverse(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),E)))),multiply(inverse(A),A))))))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))) = C,
inference(paramod,[status(thm)],[c_555,c_20]) ).
cnf(c_4013,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(B),inverse(multiply(A,inverse(multiply(inverse(A),A)))))))),inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),E)))))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))) = C,
inference(paramod,[status(thm)],[c_3191,c_8966]) ).
cnf(c_8967,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),inverse(multiply(inverse(inverse(D)),inverse(multiply(multiply(A,C),inverse(multiply(inverse(multiply(A,C)),multiply(A,C))))))))),inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(F),F)))),multiply(E,inverse(multiply(inverse(V6),V6)))))) = D,
inference(paramod,[status(thm)],[c_624,c_20]) ).
cnf(c_4086,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),inverse(multiply(inverse(inverse(C)),inverse(multiply(multiply(A,B),inverse(multiply(inverse(multiply(A,B)),multiply(A,B))))))))),inverse(multiply(inverse(multiply(D,inverse(multiply(inverse(E),E)))),multiply(D,inverse(multiply(inverse(F),F)))))) = C,
inference(paramod,[status(thm)],[c_499,c_8967]) ).
cnf(c_8968,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(B),inverse(multiply(A,inverse(multiply(inverse(A),A)))))))),inverse(multiply(inverse(inverse(C)),inverse(multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),E))))),multiply(inverse(A),A))))))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))) = C,
inference(paramod,[status(thm)],[c_586,c_20]) ).
cnf(c_4104,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(B),inverse(multiply(A,inverse(multiply(inverse(A),A)))))))),inverse(multiply(inverse(inverse(C)),inverse(inverse(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),E))))))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))) = C,
inference(paramod,[status(thm)],[c_3191,c_8968]) ).
cnf(c_8969,plain,
inverse(inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(A),A))))),multiply(inverse(B),C)))) = inverse(inverse(multiply(inverse(multiply(D,B)),multiply(D,C)))),
inference(paramod,[status(thm)],[c_2096,c_152]) ).
cnf(c_4405,plain,
inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))) = inverse(inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(D),D))))),multiply(inverse(B),C)))),
inference(copy,[status(thm)],[c_8969]) ).
cnf(c_8970,plain,
inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(B),B)))))),multiply(inverse(C),D)))) = inverse(inverse(multiply(inverse(multiply(E,C)),multiply(E,D)))),
inference(paramod,[status(thm)],[c_2093,c_152]) ).
cnf(c_4840,plain,
inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(D),D)),inverse(inverse(multiply(inverse(E),E)))))),multiply(inverse(B),C)))),
inference(copy,[status(thm)],[c_8970]) ).
cnf(c_5099,plain,
inverse(multiply(inverse(multiply(inverse(A),B)),inverse(inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D))))))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,A))),
inference(paramod,[status(thm)],[c_2130,c_76]) ).
cnf(c_5285,plain,
inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(A),A))),B)),inverse(multiply(inverse(C),C)))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_2182,c_76]) ).
cnf(c_8971,plain,
inverse(inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(inverse(multiply(inverse(B),B))),C)))) = inverse(inverse(multiply(inverse(multiply(D,inverse(multiply(inverse(E),E)))),multiply(D,C)))),
inference(paramod,[status(thm)],[c_2182,c_152]) ).
cnf(c_5293,plain,
inverse(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,C)))) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(D),D))),multiply(inverse(inverse(multiply(inverse(E),E))),C)))),
inference(copy,[status(thm)],[c_8971]) ).
cnf(c_5295,plain,
inverse(inverse(multiply(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))),multiply(inverse(C),D)))) = inverse(inverse(multiply(inverse(multiply(E,C)),multiply(E,D)))),
inference(paramod,[status(thm)],[c_2182,c_152]) ).
cnf(c_6738,plain,
inverse(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(multiply(inverse(B),B),C)))) = inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)))),
inference(paramod,[status(thm)],[c_2039,c_152]) ).
cnf(c_6739,plain,
inverse(inverse(multiply(inverse(multiply(multiply(inverse(A),A),B)),multiply(inverse(C),C)))) = inverse(inverse(multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_2039,c_152]) ).
cnf(c_7313,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),C)),inverse(multiply(inverse(D),D))))) = inverse(inverse(multiply(inverse(multiply(E,C)),multiply(E,inverse(multiply(inverse(F),F)))))),
inference(paramod,[status(thm)],[c_2194,c_152]) ).
cnf(c_8972,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(B,inverse(multiply(inverse(C),C)))),multiply(B,D))))) = D,
inference(paramod,[status(thm)],[c_370,c_578]) ).
cnf(c_8343,plain,
inverse(multiply(inverse(A),inverse(multiply(inverse(B),B)))) = A,
inference(paramod,[status(thm)],[c_3249,c_8972]) ).
cnf(c_8973,plain,
inverse(inverse(multiply(inverse(multiply(multiply(inverse(A),A),C)),inverse(multiply(inverse(D),D))))) = inverse(inverse(multiply(inverse(multiply(E,C)),multiply(E,inverse(multiply(inverse(F),F)))))),
inference(paramod,[status(thm)],[c_8343,c_7313]) ).
cnf(c_8478,plain,
inverse(multiply(multiply(inverse(A),A),B)) = inverse(inverse(multiply(inverse(multiply(C,B)),multiply(C,inverse(multiply(inverse(D),D)))))),
inference(paramod,[status(thm)],[c_8343,c_8973]) ).
cnf(c_8538,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),B) = inverse(multiply(inverse(multiply(C,B)),multiply(C,inverse(multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_8343,c_5285]) ).
cnf(c_8974,plain,
inverse(multiply(inverse(multiply(inverse(A),B)),inverse(multiply(inverse(C),C)))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,A))),
inference(paramod,[status(thm)],[c_8343,c_5099]) ).
cnf(c_8975,plain,
multiply(inverse(A),B) = inverse(multiply(inverse(multiply(E,B)),multiply(E,A))),
inference(paramod,[status(thm)],[c_8343,c_8974]) ).
cnf(c_8541,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = multiply(inverse(C),B),
inference(copy,[status(thm)],[c_8975]) ).
cnf(c_8976,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(B),inverse(multiply(A,inverse(multiply(inverse(A),A)))))))),inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),D)))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))) = C,
inference(paramod,[status(thm)],[c_8343,c_4104]) ).
cnf(c_8977,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(B),inverse(multiply(A,inverse(multiply(inverse(A),A)))))))),inverse(C))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))) = C,
inference(paramod,[status(thm)],[c_8343,c_8976]) ).
cnf(c_8554,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(B),inverse(multiply(A,inverse(multiply(inverse(A),A)))))))),inverse(C))),multiply(inverse(D),inverse(multiply(B,inverse(multiply(D,inverse(multiply(inverse(D),D)))))))) = C,
inference(paramod,[status(thm)],[c_8541,c_8977]) ).
cnf(c_8978,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(B),inverse(multiply(A,inverse(multiply(inverse(A),A)))))))),inverse(multiply(inverse(inverse(C)),multiply(inverse(D),D))))),inverse(multiply(inverse(multiply(F,inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))),multiply(F,V6)))) = C,
inference(paramod,[status(thm)],[c_8343,c_4013]) ).
cnf(c_8979,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(B),inverse(multiply(A,inverse(multiply(inverse(A),A)))))))),inverse(multiply(inverse(inverse(C)),multiply(inverse(D),D))))),multiply(inverse(V6),inverse(multiply(B,inverse(multiply(V6,inverse(multiply(inverse(V6),V6)))))))) = C,
inference(paramod,[status(thm)],[c_8541,c_8978]) ).
cnf(c_8582,plain,
multiply(inverse(inverse(A)),multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_8554,c_8979]) ).
cnf(c_8980,plain,
multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(inverse(B)),multiply(inverse(C),C))))),inverse(multiply(inverse(multiply(E,inverse(multiply(A,inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(E,F)))) = B,
inference(paramod,[status(thm)],[c_8343,c_4008]) ).
cnf(c_8981,plain,
multiply(inverse(multiply(inverse(A),inverse(B))),inverse(multiply(inverse(multiply(E,inverse(multiply(A,inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(E,F)))) = B,
inference(paramod,[status(thm)],[c_8582,c_8980]) ).
cnf(c_8585,plain,
multiply(inverse(multiply(inverse(A),inverse(B))),multiply(inverse(C),inverse(multiply(A,inverse(multiply(C,inverse(multiply(inverse(C),C)))))))) = B,
inference(paramod,[status(thm)],[c_8541,c_8981]) ).
cnf(c_8982,plain,
inverse(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(B,multiply(inverse(C),C))))),inverse(multiply(inverse(multiply(E,inverse(multiply(A,inverse(multiply(F,inverse(multiply(inverse(F),F)))))))),multiply(E,F)))))) = B,
inference(paramod,[status(thm)],[c_8343,c_3245]) ).
cnf(c_8983,plain,
inverse(inverse(multiply(inverse(multiply(inverse(A),inverse(multiply(B,multiply(inverse(C),C))))),multiply(inverse(F),inverse(multiply(A,inverse(multiply(F,inverse(multiply(inverse(F),F)))))))))) = B,
inference(paramod,[status(thm)],[c_8541,c_8982]) ).
cnf(c_8592,plain,
inverse(inverse(multiply(A,multiply(inverse(B),B)))) = A,
inference(paramod,[status(thm)],[c_8585,c_8983]) ).
cnf(c_8984,plain,
inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,A))),
inference(paramod,[status(thm)],[c_8343,c_2313]) ).
cnf(c_8630,plain,
inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))) = multiply(inverse(A),B),
inference(paramod,[status(thm)],[c_8541,c_8984]) ).
cnf(c_8985,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),inverse(multiply(C,inverse(multiply(multiply(A,B),multiply(inverse(B),B))))))),inverse(multiply(inverse(multiply(D,E)),multiply(D,E)))))) = C,
inference(paramod,[status(thm)],[c_8541,c_762]) ).
cnf(c_8986,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),inverse(multiply(C,inverse(multiply(multiply(A,B),multiply(inverse(B),B))))))),multiply(inverse(E),E)))) = C,
inference(paramod,[status(thm)],[c_8541,c_8985]) ).
cnf(c_8727,plain,
inverse(multiply(inverse(multiply(A,B)),inverse(multiply(C,inverse(multiply(multiply(A,B),multiply(inverse(B),B))))))) = C,
inference(paramod,[status(thm)],[c_8630,c_8986]) ).
cnf(c_8734,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),B) = B,
inference(paramod,[status(thm)],[c_8343,c_411]) ).
cnf(c_8987,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),inverse(multiply(inverse(inverse(C)),inverse(multiply(multiply(A,B),multiply(inverse(B),B))))))),inverse(multiply(inverse(multiply(D,inverse(multiply(inverse(E),E)))),multiply(D,inverse(multiply(inverse(F),F)))))) = C,
inference(paramod,[status(thm)],[c_8541,c_4086]) ).
cnf(c_8988,plain,
multiply(inverse(inverse(C)),inverse(multiply(inverse(multiply(D,inverse(multiply(inverse(E),E)))),multiply(D,inverse(multiply(inverse(F),F)))))) = C,
inference(paramod,[status(thm)],[c_8727,c_8987]) ).
cnf(c_8989,plain,
multiply(inverse(inverse(C)),multiply(inverse(inverse(multiply(inverse(F),F))),inverse(multiply(inverse(E),E)))) = C,
inference(paramod,[status(thm)],[c_8541,c_8988]) ).
cnf(c_8752,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_8734,c_8989]) ).
cnf(c_8990,plain,
inverse(multiply(multiply(inverse(A),A),B)) = inverse(multiply(inverse(inverse(multiply(inverse(D),D))),B)),
inference(paramod,[status(thm)],[c_8541,c_8478]) ).
cnf(c_8769,plain,
inverse(multiply(multiply(inverse(A),A),B)) = inverse(B),
inference(paramod,[status(thm)],[c_8734,c_8990]) ).
cnf(c_8991,plain,
inverse(inverse(multiply(inverse(B),multiply(inverse(C),C)))) = inverse(inverse(multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_8769,c_6739]) ).
cnf(c_8992,plain,
inverse(B) = inverse(inverse(multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_8592,c_8991]) ).
cnf(c_8993,plain,
inverse(B) = inverse(multiply(inverse(multiply(inverse(E),E)),B)),
inference(paramod,[status(thm)],[c_8541,c_8992]) ).
cnf(c_8777,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),B)) = inverse(B),
inference(copy,[status(thm)],[c_8993]) ).
cnf(c_8994,plain,
inverse(inverse(multiply(multiply(inverse(B),B),C))) = inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)))),
inference(paramod,[status(thm)],[c_8777,c_6738]) ).
cnf(c_8995,plain,
inverse(inverse(C)) = inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)))),
inference(paramod,[status(thm)],[c_8769,c_8994]) ).
cnf(c_8996,plain,
inverse(inverse(C)) = inverse(multiply(inverse(C),multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_8541,c_8995]) ).
cnf(c_8778,plain,
inverse(multiply(inverse(A),multiply(inverse(B),B))) = inverse(inverse(A)),
inference(copy,[status(thm)],[c_8996]) ).
cnf(c_8997,plain,
inverse(inverse(multiply(multiply(inverse(A),A),multiply(inverse(C),D)))) = inverse(inverse(multiply(inverse(multiply(E,C)),multiply(E,D)))),
inference(paramod,[status(thm)],[c_8752,c_5295]) ).
cnf(c_8998,plain,
inverse(inverse(multiply(inverse(C),D))) = inverse(inverse(multiply(inverse(multiply(E,C)),multiply(E,D)))),
inference(paramod,[status(thm)],[c_8769,c_8997]) ).
cnf(c_8783,plain,
inverse(inverse(multiply(inverse(A),B))) = inverse(multiply(inverse(B),A)),
inference(paramod,[status(thm)],[c_8541,c_8998]) ).
cnf(c_8999,plain,
inverse(multiply(inverse(C),inverse(multiply(inverse(B),B)))) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(D),D))),multiply(inverse(inverse(multiply(inverse(E),E))),C)))),
inference(paramod,[status(thm)],[c_8541,c_5293]) ).
cnf(c_9000,plain,
C = inverse(inverse(multiply(inverse(inverse(multiply(inverse(D),D))),multiply(inverse(inverse(multiply(inverse(E),E))),C)))),
inference(paramod,[status(thm)],[c_8343,c_8999]) ).
cnf(c_9001,plain,
C = inverse(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(E),E))),C)))),
inference(paramod,[status(thm)],[c_8783,c_9000]) ).
cnf(c_9002,plain,
C = inverse(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),E)),C)))),
inference(paramod,[status(thm)],[c_8783,c_9001]) ).
cnf(c_9003,plain,
C = inverse(inverse(multiply(inverse(multiply(inverse(E),E)),C))),
inference(paramod,[status(thm)],[c_8777,c_9002]) ).
cnf(c_9004,plain,
C = inverse(inverse(C)),
inference(paramod,[status(thm)],[c_8777,c_9003]) ).
cnf(c_8784,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_9004]) ).
cnf(c_9005,plain,
inverse(multiply(inverse(C),B)) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(D),D)),inverse(inverse(multiply(inverse(E),E)))))),multiply(inverse(B),C)))),
inference(paramod,[status(thm)],[c_8541,c_4840]) ).
cnf(c_9006,plain,
inverse(multiply(inverse(C),B)) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E)))),multiply(inverse(B),C)))),
inference(paramod,[status(thm)],[c_8784,c_9005]) ).
cnf(c_9007,plain,
inverse(multiply(inverse(C),B)) = inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(D),D)))),multiply(inverse(B),C)))),
inference(paramod,[status(thm)],[c_8778,c_9006]) ).
cnf(c_9008,plain,
inverse(multiply(inverse(C),B)) = inverse(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(B),C)))),
inference(paramod,[status(thm)],[c_8784,c_9007]) ).
cnf(c_9009,plain,
inverse(multiply(inverse(C),B)) = inverse(inverse(multiply(inverse(B),C))),
inference(paramod,[status(thm)],[c_8777,c_9008]) ).
cnf(c_8785,plain,
inverse(multiply(inverse(A),B)) = multiply(inverse(B),A),
inference(paramod,[status(thm)],[c_8784,c_9009]) ).
cnf(c_9010,plain,
inverse(multiply(inverse(multiply(A,C)),multiply(A,B))) = inverse(inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(D),D))))),multiply(inverse(B),C)))),
inference(paramod,[status(thm)],[c_8785,c_4405]) ).
cnf(c_9011,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = inverse(inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(D),D))))),multiply(inverse(B),C)))),
inference(paramod,[status(thm)],[c_8785,c_9010]) ).
cnf(c_9012,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(D),D)))),multiply(inverse(B),C)))),
inference(paramod,[status(thm)],[c_8785,c_9011]) ).
cnf(c_9013,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(D),D))),multiply(inverse(B),C)))),
inference(paramod,[status(thm)],[c_8785,c_9012]) ).
cnf(c_9014,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = inverse(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(B),C)))),
inference(paramod,[status(thm)],[c_8785,c_9013]) ).
cnf(c_9015,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = inverse(inverse(multiply(multiply(inverse(D),D),multiply(inverse(B),C)))),
inference(paramod,[status(thm)],[c_8785,c_9014]) ).
cnf(c_9016,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = inverse(inverse(multiply(inverse(B),C))),
inference(paramod,[status(thm)],[c_8769,c_9015]) ).
cnf(c_9017,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = inverse(multiply(inverse(C),B)),
inference(paramod,[status(thm)],[c_8785,c_9016]) ).
cnf(c_8790,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_8785,c_9017]) ).
cnf(c_9018,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(B,multiply(inverse(inverse(multiply(inverse(multiply(C,D)),multiply(C,E)))),inverse(multiply(inverse(multiply(F,D)),multiply(F,E)))))))) = B,
inference(paramod,[status(thm)],[c_8785,c_3253]) ).
cnf(c_9019,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(B,multiply(inverse(inverse(multiply(inverse(D),E))),inverse(multiply(inverse(multiply(F,D)),multiply(F,E)))))))) = B,
inference(paramod,[status(thm)],[c_8790,c_9018]) ).
cnf(c_9020,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(B,multiply(inverse(multiply(inverse(E),D)),inverse(multiply(inverse(multiply(F,D)),multiply(F,E)))))))) = B,
inference(paramod,[status(thm)],[c_8785,c_9019]) ).
cnf(c_9021,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(B,multiply(multiply(inverse(D),E),inverse(multiply(inverse(multiply(F,D)),multiply(F,E)))))))) = B,
inference(paramod,[status(thm)],[c_8785,c_9020]) ).
cnf(c_9022,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(B,multiply(multiply(inverse(D),E),inverse(multiply(inverse(D),E))))))) = B,
inference(paramod,[status(thm)],[c_8790,c_9021]) ).
cnf(c_9023,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(B,multiply(multiply(inverse(D),E),multiply(inverse(E),D)))))) = B,
inference(paramod,[status(thm)],[c_8785,c_9022]) ).
cnf(c_9024,plain,
inverse(inverse(multiply(B,multiply(multiply(inverse(D),E),multiply(inverse(E),D))))) = B,
inference(paramod,[status(thm)],[c_8769,c_9023]) ).
cnf(c_8799,plain,
multiply(A,multiply(multiply(inverse(B),C),multiply(inverse(C),B))) = A,
inference(paramod,[status(thm)],[c_8784,c_9024]) ).
cnf(c_9025,plain,
inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),C))),inverse(multiply(inverse(multiply(D,B)),multiply(D,C))))),inverse(multiply(E,multiply(inverse(F),F))))) = E,
inference(paramod,[status(thm)],[c_8790,c_3252]) ).
cnf(c_9026,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),B)),inverse(multiply(inverse(multiply(D,B)),multiply(D,C))))),inverse(multiply(E,multiply(inverse(F),F))))) = E,
inference(paramod,[status(thm)],[c_8785,c_9025]) ).
cnf(c_9027,plain,
inverse(multiply(inverse(multiply(multiply(inverse(B),C),inverse(multiply(inverse(multiply(D,B)),multiply(D,C))))),inverse(multiply(E,multiply(inverse(F),F))))) = E,
inference(paramod,[status(thm)],[c_8785,c_9026]) ).
cnf(c_9028,plain,
inverse(multiply(inverse(multiply(multiply(inverse(B),C),inverse(multiply(inverse(B),C)))),inverse(multiply(E,multiply(inverse(F),F))))) = E,
inference(paramod,[status(thm)],[c_8790,c_9027]) ).
cnf(c_9029,plain,
inverse(multiply(inverse(multiply(multiply(inverse(B),C),multiply(inverse(C),B))),inverse(multiply(E,multiply(inverse(F),F))))) = E,
inference(paramod,[status(thm)],[c_8785,c_9028]) ).
cnf(c_9030,plain,
multiply(inverse(inverse(multiply(E,multiply(inverse(F),F)))),multiply(multiply(inverse(B),C),multiply(inverse(C),B))) = E,
inference(paramod,[status(thm)],[c_8785,c_9029]) ).
cnf(c_9031,plain,
multiply(multiply(E,multiply(inverse(F),F)),multiply(multiply(inverse(B),C),multiply(inverse(C),B))) = E,
inference(paramod,[status(thm)],[c_8784,c_9030]) ).
cnf(c_8800,plain,
multiply(A,multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_8799,c_9031]) ).
cnf(c_9032,plain,
inverse(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,D)))) = inverse(inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D)))),
inference(paramod,[status(thm)],[c_8800,c_3251]) ).
cnf(c_9033,plain,
inverse(inverse(multiply(inverse(inverse(B)),D))) = inverse(inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D)))),
inference(paramod,[status(thm)],[c_8790,c_9032]) ).
cnf(c_9034,plain,
inverse(inverse(multiply(B,D))) = inverse(inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D)))),
inference(paramod,[status(thm)],[c_8784,c_9033]) ).
cnf(c_9035,plain,
multiply(B,D) = inverse(inverse(multiply(B,multiply(inverse(multiply(inverse(E),E)),D)))),
inference(paramod,[status(thm)],[c_8784,c_9034]) ).
cnf(c_9036,plain,
multiply(B,D) = inverse(inverse(multiply(B,multiply(multiply(inverse(E),E),D)))),
inference(paramod,[status(thm)],[c_8785,c_9035]) ).
cnf(c_9037,plain,
multiply(B,D) = multiply(B,multiply(multiply(inverse(E),E),D)),
inference(paramod,[status(thm)],[c_8784,c_9036]) ).
cnf(c_8801,plain,
multiply(A,multiply(multiply(inverse(B),B),C)) = multiply(A,C),
inference(copy,[status(thm)],[c_9037]) ).
cnf(c_9038,plain,
inverse(inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),C)))) = inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)))),
inference(paramod,[status(thm)],[c_8785,c_2900]) ).
cnf(c_9039,plain,
inverse(inverse(multiply(multiply(inverse(A),A),C))) = inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)))),
inference(paramod,[status(thm)],[c_8801,c_9038]) ).
cnf(c_9040,plain,
inverse(inverse(C)) = inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)))),
inference(paramod,[status(thm)],[c_8769,c_9039]) ).
cnf(c_9041,plain,
C = inverse(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)))),
inference(paramod,[status(thm)],[c_8784,c_9040]) ).
cnf(c_9042,plain,
C = inverse(inverse(multiply(inverse(D),multiply(D,C)))),
inference(paramod,[status(thm)],[c_8800,c_9041]) ).
cnf(c_9043,plain,
C = inverse(multiply(inverse(multiply(D,C)),D)),
inference(paramod,[status(thm)],[c_8785,c_9042]) ).
cnf(c_9044,plain,
C = multiply(inverse(D),multiply(D,C)),
inference(paramod,[status(thm)],[c_8785,c_9043]) ).
cnf(c_8804,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_9044]) ).
cnf(c_9045,plain,
inverse(inverse(multiply(inverse(multiply(A,inverse(multiply(B,inverse(multiply(C,multiply(inverse(D),D))))))),multiply(A,C)))) = B,
inference(paramod,[status(thm)],[c_8785,c_376]) ).
cnf(c_9046,plain,
inverse(inverse(multiply(inverse(multiply(A,inverse(multiply(B,inverse(C))))),multiply(A,C)))) = B,
inference(paramod,[status(thm)],[c_8800,c_9045]) ).
cnf(c_9047,plain,
inverse(inverse(multiply(inverse(inverse(multiply(B,inverse(C)))),C))) = B,
inference(paramod,[status(thm)],[c_8790,c_9046]) ).
cnf(c_9048,plain,
inverse(inverse(multiply(multiply(B,inverse(C)),C))) = B,
inference(paramod,[status(thm)],[c_8784,c_9047]) ).
cnf(c_8810,plain,
multiply(multiply(A,inverse(B)),B) = A,
inference(paramod,[status(thm)],[c_8784,c_9048]) ).
cnf(c_9049,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(E,F)))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_8790,c_247]) ).
cnf(c_9050,plain,
inverse(inverse(multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_8785,c_9049]) ).
cnf(c_9051,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_8784,c_9050]) ).
cnf(c_9052,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),inverse(multiply(C,multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_8785,c_9051]) ).
cnf(c_9053,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),inverse(C))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_8800,c_9052]) ).
cnf(c_9054,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,multiply(inverse(inverse(C)),E))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_8785,c_9053]) ).
cnf(c_9055,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,multiply(C,E))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_8784,c_9054]) ).
cnf(c_9056,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,multiply(C,E))),D)),F))),
inference(paramod,[status(thm)],[c_8790,c_9055]) ).
cnf(c_9057,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(multiply(inverse(D),multiply(B,multiply(C,E))),F))),
inference(paramod,[status(thm)],[c_8785,c_9056]) ).
cnf(c_9058,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = multiply(multiply(inverse(D),multiply(B,multiply(C,E))),F),
inference(paramod,[status(thm)],[c_8784,c_9057]) ).
cnf(c_8813,plain,
multiply(multiply(inverse(A),multiply(B,multiply(C,D))),E) = multiply(multiply(inverse(A),multiply(B,C)),multiply(D,E)),
inference(copy,[status(thm)],[c_9058]) ).
cnf(c_9059,plain,
inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(B)),C))),D)),B))) = inverse(inverse(multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),
inference(paramod,[status(thm)],[c_8790,c_198]) ).
cnf(c_9060,plain,
inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(B,C))),D)),B))) = inverse(inverse(multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),
inference(paramod,[status(thm)],[c_8784,c_9059]) ).
cnf(c_9061,plain,
inverse(inverse(multiply(inverse(multiply(multiply(B,C),D)),B))) = inverse(inverse(multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),
inference(paramod,[status(thm)],[c_8784,c_9060]) ).
cnf(c_9062,plain,
inverse(multiply(inverse(B),multiply(multiply(B,C),D))) = inverse(inverse(multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),
inference(paramod,[status(thm)],[c_8785,c_9061]) ).
cnf(c_9063,plain,
multiply(inverse(multiply(multiply(B,C),D)),B) = inverse(inverse(multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),
inference(paramod,[status(thm)],[c_8785,c_9062]) ).
cnf(c_9064,plain,
multiply(inverse(multiply(multiply(B,C),D)),B) = inverse(inverse(multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,multiply(inverse(C),C))))))),
inference(paramod,[status(thm)],[c_8785,c_9063]) ).
cnf(c_9065,plain,
multiply(inverse(multiply(multiply(B,C),D)),B) = inverse(inverse(multiply(inverse(multiply(E,D)),multiply(E,inverse(C))))),
inference(paramod,[status(thm)],[c_8800,c_9064]) ).
cnf(c_9066,plain,
multiply(inverse(multiply(multiply(B,C),D)),B) = inverse(inverse(multiply(inverse(D),inverse(C)))),
inference(paramod,[status(thm)],[c_8790,c_9065]) ).
cnf(c_9067,plain,
multiply(inverse(multiply(multiply(B,C),D)),B) = inverse(multiply(inverse(inverse(C)),D)),
inference(paramod,[status(thm)],[c_8785,c_9066]) ).
cnf(c_8820,plain,
multiply(inverse(multiply(multiply(A,B),C)),A) = inverse(multiply(B,C)),
inference(paramod,[status(thm)],[c_8784,c_9067]) ).
cnf(c_9068,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(B)),C))),D)),B) = multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))),
inference(paramod,[status(thm)],[c_8790,c_178]) ).
cnf(c_9069,plain,
multiply(inverse(multiply(inverse(inverse(multiply(B,C))),D)),B) = multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))),
inference(paramod,[status(thm)],[c_8784,c_9068]) ).
cnf(c_9070,plain,
multiply(inverse(multiply(multiply(B,C),D)),B) = multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))),
inference(paramod,[status(thm)],[c_8784,c_9069]) ).
cnf(c_9071,plain,
inverse(multiply(C,D)) = multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,inverse(multiply(inverse(C),C)))))),
inference(paramod,[status(thm)],[c_8820,c_9070]) ).
cnf(c_9072,plain,
inverse(multiply(C,D)) = multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(C,multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_8785,c_9071]) ).
cnf(c_9073,plain,
inverse(multiply(C,D)) = multiply(inverse(multiply(E,D)),multiply(E,inverse(C))),
inference(paramod,[status(thm)],[c_8800,c_9072]) ).
cnf(c_8830,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(paramod,[status(thm)],[c_8790,c_9073]) ).
cnf(c_9074,plain,
multiply(inverse(multiply(inverse(A),inverse(inverse(A)))),B) = inverse(multiply(inverse(multiply(C,B)),multiply(C,inverse(multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_8830,c_8538]) ).
cnf(c_9075,plain,
multiply(inverse(multiply(inverse(A),A)),B) = inverse(multiply(inverse(multiply(C,B)),multiply(C,inverse(multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_8784,c_9074]) ).
cnf(c_9076,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),B) = inverse(multiply(inverse(multiply(C,B)),multiply(C,inverse(multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_8830,c_9075]) ).
cnf(c_9077,plain,
multiply(multiply(inverse(A),A),B) = inverse(multiply(inverse(multiply(C,B)),multiply(C,inverse(multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_8784,c_9076]) ).
cnf(c_9078,plain,
multiply(multiply(inverse(A),A),B) = inverse(multiply(multiply(inverse(B),inverse(C)),multiply(C,inverse(multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_8830,c_9077]) ).
cnf(c_9079,plain,
multiply(multiply(inverse(A),A),B) = inverse(multiply(multiply(inverse(B),inverse(C)),multiply(C,multiply(inverse(D),inverse(inverse(D)))))),
inference(paramod,[status(thm)],[c_8830,c_9078]) ).
cnf(c_9080,plain,
multiply(multiply(inverse(A),A),B) = inverse(multiply(multiply(inverse(B),inverse(C)),multiply(C,multiply(inverse(D),D)))),
inference(paramod,[status(thm)],[c_8784,c_9079]) ).
cnf(c_9081,plain,
multiply(multiply(inverse(A),A),B) = inverse(multiply(multiply(inverse(B),inverse(C)),C)),
inference(paramod,[status(thm)],[c_8800,c_9080]) ).
cnf(c_9082,plain,
multiply(multiply(inverse(A),A),B) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_8810,c_9081]) ).
cnf(c_8843,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_8784,c_9082]) ).
cnf(c_9083,plain,
( multiply(a3,multiply(b3,c3)) != multiply(multiply(a3,b3),c3)
| a2 != a2 ),
inference(paramod,[status(thm)],[c_8843,c_364]) ).
cnf(c_8926,plain,
multiply(a3,multiply(b3,c3)) != multiply(multiply(a3,b3),c3),
inference(copy,[status(thm)],[c_9083]) ).
cnf(c_9084,plain,
multiply(multiply(A,B),C) = multiply(multiply(inverse(D),multiply(D,A)),multiply(B,C)),
inference(paramod,[status(thm)],[c_8804,c_8813]) ).
cnf(c_8945,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_8804,c_9084]) ).
cnf(c_9085,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(copy,[status(thm)],[c_8926]) ).
cnf(c_8946,plain,
$false,
inference(resolve,[status(thm)],[c_8945,c_9085]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP054-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 14:20:40 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1238521 was started by sandbox2 on n008,
% 0.10/0.37 % Fri Sep 25 14:20:40 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 42.09/6.54
% 42.09/6.54 % SZS status Unsatisfiable for theBenchmark
% 42.09/6.54
% 42.09/6.54 % Proof 1 at 5.05 (+ 0.90) seconds.
% 42.09/6.54 % Length of proof is 110.
% 42.09/6.54 % Level of proof is 33.
% 42.09/6.54 % Maximum clause weight is 82.000.
% 42.09/6.54 % Given clauses 96.
% 42.09/6.54
% 42.09/6.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------