%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP407-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:28:58 AM UTC 2026
% Result : Unsatisfiable 4.47s 1.29s
% Output : CNFRefutation 4.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 93
% Number of leaves : 2
% Syntax : Number of formulae : 268 ( 268 unt; 0 def)
% Number of atoms : 268 ( 267 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 11 ( 11 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 1439 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,inverse(multiply(inverse(multiply(inverse(multiply(VAR_0,VAR_1)),VAR_2)),multiply(inverse(VAR_1),multiply(inverse(VAR_1),VAR_1))))) = VAR_2,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),multiply(inverse(B),B))))) = C,
inference(clausify,[status(thm)],[single_axiom]) ).
fof(prove_these_axioms_2,axiom,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('theBenchmark.p',prove_these_axioms_2) ).
cnf(c_2,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(clausify,[status(thm)],[prove_these_axioms_2]) ).
cnf(c_2727,plain,
multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(C),C))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,C)),D)),B)),multiply(inverse(D),multiply(inverse(D),D)))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_3,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(B),B))))),
inference(copy,[status(thm)],[c_2727]) ).
cnf(c_5,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(C),multiply(inverse(B),multiply(inverse(B),B)))))) = C,
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_6,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(A,B)),D))),multiply(inverse(C),multiply(inverse(C),C)))) = D,
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_2728,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(C,D)),A)),multiply(inverse(D),multiply(inverse(D),D)))))),E))),multiply(inverse(B),multiply(inverse(B),B)))) = E,
inference(paramod,[status(thm)],[c_1,c_6]) ).
cnf(c_13,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(A),C))),multiply(inverse(B),multiply(inverse(B),B)))) = C,
inference(paramod,[status(thm)],[c_1,c_2728]) ).
cnf(c_2729,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(inverse(multiply(D,E)),B)),multiply(inverse(multiply(D,E)),C)),
inference(paramod,[status(thm)],[c_6,c_5]) ).
cnf(c_17,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(A,B)),D)) = multiply(inverse(multiply(E,C)),multiply(E,D)),
inference(copy,[status(thm)],[c_2729]) ).
cnf(c_2730,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),E)),multiply(inverse(multiply(C,D)),A))),multiply(inverse(E),multiply(inverse(E),E)))),F))),multiply(inverse(B),multiply(inverse(B),B)))) = F,
inference(paramod,[status(thm)],[c_6,c_6]) ).
cnf(c_18,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(B),multiply(inverse(B),B)))) = C,
inference(paramod,[status(thm)],[c_13,c_2730]) ).
cnf(c_2731,plain,
multiply(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(C),C))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,C)),D)),B)),E)) = multiply(inverse(multiply(F,multiply(inverse(D),multiply(inverse(D),D)))),multiply(F,E)),
inference(paramod,[status(thm)],[c_3,c_17]) ).
cnf(c_34,plain,
multiply(inverse(multiply(A,multiply(inverse(B),multiply(inverse(B),B)))),multiply(A,C)) = multiply(multiply(D,inverse(multiply(inverse(E),multiply(inverse(F),multiply(inverse(F),F))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,F)),B)),E)),C)),
inference(copy,[status(thm)],[c_2731]) ).
cnf(c_2732,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),D)) = multiply(inverse(multiply(E,multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),multiply(inverse(C),C))))))),multiply(E,D)),
inference(paramod,[status(thm)],[c_5,c_17]) ).
cnf(c_41,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(inverse(C),multiply(inverse(D),multiply(inverse(D),D))))))),multiply(A,E)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),
inference(copy,[status(thm)],[c_2732]) ).
cnf(c_46,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_17,c_17]) ).
cnf(c_51,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),D)),multiply(inverse(multiply(B,C)),multiply(inverse(multiply(E,C)),multiply(E,C)))))) = D,
inference(paramod,[status(thm)],[c_46,c_1]) ).
cnf(c_2733,plain,
multiply(inverse(A),multiply(B,C)) = multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(B,E)),A)),multiply(inverse(E),multiply(inverse(E),E)))))),multiply(D,C)),
inference(paramod,[status(thm)],[c_1,c_46]) ).
cnf(c_52,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(C),multiply(inverse(C),C)))))),multiply(A,E)) = multiply(inverse(D),multiply(B,E)),
inference(copy,[status(thm)],[c_2733]) ).
cnf(c_57,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),D))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(multiply(E,D)),multiply(E,multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_46,c_3]) ).
cnf(c_66,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,D)),multiply(C,multiply(inverse(B),B)))))) = multiply(inverse(B),D),
inference(paramod,[status(thm)],[c_46,c_5]) ).
cnf(c_67,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(F,multiply(D,C))),multiply(F,E)),
inference(paramod,[status(thm)],[c_46,c_46]) ).
cnf(c_68,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,C)),multiply(F,multiply(A,E))),
inference(paramod,[status(thm)],[c_46,c_46]) ).
cnf(c_2734,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,A))),D)) = multiply(inverse(multiply(E,multiply(inverse(C),multiply(inverse(C),C)))),multiply(E,D)),
inference(paramod,[status(thm)],[c_18,c_46]) ).
cnf(c_79,plain,
multiply(inverse(multiply(A,multiply(inverse(B),multiply(inverse(B),B)))),multiply(A,C)) = multiply(D,multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),C)),
inference(copy,[status(thm)],[c_2734]) ).
cnf(c_2735,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(F,multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(V6),multiply(inverse(V6),V6))))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_1,c_67]) ).
cnf(c_86,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(D,F)),E)),
inference(paramod,[status(thm)],[c_41,c_2735]) ).
cnf(c_106,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,E))),
inference(paramod,[status(thm)],[c_46,c_67]) ).
cnf(c_2736,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,C)),V6)),A)),multiply(inverse(V6),multiply(inverse(V6),V6)))))),multiply(E,multiply(F,D))),
inference(paramod,[status(thm)],[c_1,c_68]) ).
cnf(c_189,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(A),multiply(inverse(multiply(E,C)),multiply(E,D))),
inference(paramod,[status(thm)],[c_52,c_2736]) ).
cnf(c_219,plain,
multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D))) = multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D))),
inference(paramod,[status(thm)],[c_68,c_67]) ).
cnf(c_2737,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,A))),multiply(inverse(F),multiply(inverse(F),F)))),multiply(inverse(multiply(V6,C)),multiply(V6,D))),
inference(paramod,[status(thm)],[c_18,c_189]) ).
cnf(c_276,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(A,multiply(inverse(multiply(E,C)),multiply(E,D))),
inference(paramod,[status(thm)],[c_18,c_2737]) ).
cnf(c_305,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(inverse(multiply(C,D)),multiply(C,E)))) = multiply(inverse(multiply(F,B)),multiply(F,multiply(inverse(multiply(V6,D)),multiply(V6,E)))),
inference(paramod,[status(thm)],[c_276,c_46]) ).
cnf(c_333,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),multiply(inverse(B),D)))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(multiply(E,multiply(F,D))),multiply(E,multiply(F,B))))),
inference(paramod,[status(thm)],[c_219,c_3]) ).
cnf(c_376,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),D)),E))),multiply(A,multiply(inverse(multiply(F,D)),multiply(F,multiply(B,V6))))) = multiply(inverse(multiply(V7,multiply(V8,E))),multiply(V7,multiply(V8,multiply(inverse(multiply(V9,C)),multiply(V9,V6))))),
inference(paramod,[status(thm)],[c_68,c_219]) ).
cnf(c_382,plain,
multiply(A,multiply(inverse(multiply(B,multiply(C,D))),multiply(B,multiply(C,E)))) = multiply(A,multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E)))),
inference(paramod,[status(thm)],[c_219,c_276]) ).
cnf(c_443,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(multiply(E,C)),F)))),multiply(A,multiply(inverse(multiply(inverse(multiply(B,V6)),D)),V7))) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_86,c_219]) ).
cnf(c_445,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),D)),E))),multiply(A,multiply(inverse(multiply(inverse(multiply(B,F)),D)),multiply(inverse(multiply(V6,F)),V7)))) = multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,multiply(inverse(multiply(V6,C)),V7)))),
inference(paramod,[status(thm)],[c_86,c_219]) ).
cnf(c_455,plain,
multiply(A,multiply(inverse(multiply(B,multiply(inverse(multiply(C,D)),E))),multiply(B,F))) = multiply(A,multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,multiply(C,inverse(multiply(inverse(F),multiply(inverse(D),multiply(inverse(D),D))))))))),
inference(paramod,[status(thm)],[c_5,c_382]) ).
cnf(c_512,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(B,C)),multiply(inverse(multiply(B,C)),multiply(B,C))))),multiply(A,D)) = multiply(multiply(B,inverse(multiply(inverse(multiply(inverse(E),multiply(inverse(E),E))),multiply(inverse(E),multiply(inverse(E),E))))),multiply(C,D)),
inference(paramod,[status(thm)],[c_18,c_34]) ).
cnf(c_675,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(multiply(B,multiply(B,C))),multiply(B,C)))),multiply(A,D))),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,multiply(B,C)))))) = D,
inference(paramod,[status(thm)],[c_106,c_18]) ).
cnf(c_767,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),D)),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,V6)))) = multiply(inverse(multiply(inverse(multiply(A,V7)),D)),multiply(inverse(multiply(inverse(multiply(B,V8)),V7)),multiply(inverse(multiply(V9,V8)),multiply(V9,V6)))),
inference(paramod,[status(thm)],[c_106,c_86]) ).
cnf(c_808,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,multiply(F,V6))))) = multiply(inverse(multiply(V7,multiply(inverse(multiply(E,multiply(F,V8))),C))),multiply(V7,multiply(inverse(multiply(inverse(multiply(V9,V10)),multiply(V9,V8))),multiply(inverse(multiply(V11,V10)),multiply(V11,V6))))),
inference(paramod,[status(thm)],[c_106,c_106]) ).
cnf(c_821,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,V7)),multiply(V6,V8)))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(B,F)),D))),multiply(V9,multiply(inverse(multiply(V10,V7)),multiply(V10,V8)))),
inference(paramod,[status(thm)],[c_67,c_305]) ).
cnf(c_869,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,multiply(inverse(multiply(F,V6)),multiply(F,V7)))))) = multiply(inverse(multiply(V8,multiply(inverse(multiply(E,V9)),C))),multiply(V8,multiply(inverse(multiply(V10,V9)),multiply(V10,multiply(inverse(multiply(V11,V6)),multiply(V11,V7)))))),
inference(paramod,[status(thm)],[c_305,c_106]) ).
cnf(c_2738,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(B,C)),multiply(B,inverse(D))))),multiply(A,inverse(multiply(inverse(multiply(E,multiply(inverse(C),multiply(inverse(C),C)))),multiply(E,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(D)))),multiply(inverse(multiply(B,C)),multiply(B,inverse(D))))))))) = D,
inference(paramod,[status(thm)],[c_79,c_5]) ).
cnf(c_929,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),multiply(inverse(B),multiply(inverse(B),B))) = C,
inference(paramod,[status(thm)],[c_66,c_2738]) ).
cnf(c_988,plain,
multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(inverse(multiply(D,multiply(inverse(E),multiply(inverse(E),E)))),multiply(D,F)))) = multiply(inverse(multiply(V6,multiply(V7,C))),multiply(V6,multiply(V7,multiply(inverse(multiply(inverse(multiply(V8,E)),multiply(V8,B))),F)))),
inference(paramod,[status(thm)],[c_79,c_219]) ).
cnf(c_1052,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),inverse(multiply(inverse(multiply(C,D)),multiply(inverse(multiply(inverse(B),multiply(inverse(B),B))),multiply(inverse(multiply(E,multiply(inverse(B),B))),multiply(E,multiply(inverse(B),B))))))) = D,
inference(paramod,[status(thm)],[c_18,c_51]) ).
cnf(c_2739,plain,
multiply(inverse(multiply(A,multiply(inverse(B),multiply(inverse(B),B)))),multiply(A,multiply(inverse(B),multiply(inverse(B),B)))) = multiply(multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(C,D)),inverse(E))),multiply(inverse(D),multiply(inverse(D),D))))),E),
inference(paramod,[status(thm)],[c_929,c_34]) ).
cnf(c_1126,plain,
multiply(inverse(multiply(A,multiply(inverse(B),multiply(inverse(B),B)))),multiply(A,multiply(inverse(B),multiply(inverse(B),B)))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_1,c_2739]) ).
cnf(c_2740,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),multiply(inverse(E),E))))) = multiply(inverse(multiply(inverse(multiply(F,multiply(inverse(E),multiply(inverse(E),E)))),multiply(F,C))),multiply(inverse(V6),V6)),
inference(paramod,[status(thm)],[c_1126,c_106]) ).
cnf(c_1266,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),multiply(inverse(B),B)))),multiply(A,C))),multiply(inverse(D),D)) = multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,multiply(inverse(B),multiply(inverse(B),B))))),
inference(copy,[status(thm)],[c_2740]) ).
cnf(c_2741,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(A)))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_929,c_1126]) ).
cnf(c_1311,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_929,c_2741]) ).
cnf(c_1316,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(A),multiply(inverse(A),A))))) = C,
inference(paramod,[status(thm)],[c_1311,c_1]) ).
cnf(c_1319,plain,
multiply(multiply(inverse(A),A),a2) != a2,
inference(paramod,[status(thm)],[c_1311,c_2]) ).
cnf(c_1321,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(multiply(C,D)),multiply(inverse(multiply(C,D)),multiply(C,D))))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_1311,c_3]) ).
cnf(c_2742,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(B),B)))) = multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(C,D)),B)),multiply(inverse(D),multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_1311,c_3]) ).
cnf(c_1322,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(B),B)))) = B,
inference(paramod,[status(thm)],[c_1,c_2742]) ).
cnf(c_1337,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_1311,c_46]) ).
cnf(c_1338,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,A)),
inference(paramod,[status(thm)],[c_1311,c_46]) ).
cnf(c_1420,plain,
multiply(inverse(multiply(A,multiply(inverse(B),multiply(inverse(B),B)))),multiply(A,multiply(inverse(multiply(C,B)),multiply(C,D)))) = multiply(D,multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_1311,c_79]) ).
cnf(c_2743,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),C)),D)),multiply(inverse(C),multiply(inverse(C),C)))))),multiply(A,B)) = multiply(inverse(D),multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_1311,c_52]) ).
cnf(c_1431,plain,
multiply(inverse(A),multiply(inverse(B),B)) = multiply(inverse(A),multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_52,c_2743]) ).
cnf(c_1481,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_1431,c_1311]) ).
cnf(c_1483,plain,
multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,C))),a2) != a2,
inference(paramod,[status(thm)],[c_67,c_1319]) ).
cnf(c_1533,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,multiply(inverse(multiply(inverse(C),C)),D))) = multiply(inverse(multiply(E,multiply(F,multiply(inverse(V6),V6)))),multiply(E,multiply(F,D))),
inference(paramod,[status(thm)],[c_1481,c_219]) ).
cnf(c_1697,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),D))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(D),multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_1311,c_57]) ).
cnf(c_1698,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),D))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(multiply(E,D)),multiply(E,multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_1311,c_57]) ).
cnf(c_2744,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C))),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(D),D))))) = multiply(inverse(B),inverse(multiply(inverse(multiply(E,C)),multiply(E,multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_1481,c_57]) ).
cnf(c_1708,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(A),multiply(inverse(A),A))))) = multiply(inverse(B),inverse(multiply(inverse(multiply(D,C)),multiply(D,multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_1321,c_2744]) ).
cnf(c_1994,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(multiply(E,C)),multiply(E,F)))) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,F)))),
inference(paramod,[status(thm)],[c_68,c_1337]) ).
cnf(c_2131,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,multiply(C,D)))),multiply(inverse(E),E)) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,V7)),multiply(V6,D)))),multiply(F,multiply(inverse(multiply(C,V7)),B))),
inference(paramod,[status(thm)],[c_68,c_1338]) ).
cnf(c_2192,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,F)))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,V7)),C))),multiply(V6,multiply(inverse(multiply(inverse(F),V7)),multiply(inverse(V8),V8)))),
inference(paramod,[status(thm)],[c_1338,c_106]) ).
cnf(c_2197,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,E)))),multiply(inverse(F),F)) = multiply(inverse(multiply(V6,multiply(V7,multiply(V8,E)))),multiply(V6,multiply(V7,multiply(V8,C)))),
inference(paramod,[status(thm)],[c_106,c_1338]) ).
cnf(c_2745,plain,
multiply(A,multiply(inverse(multiply(B,A)),C)) = multiply(inverse(multiply(D,multiply(B,multiply(inverse(A),A)))),multiply(D,C)),
inference(paramod,[status(thm)],[c_1322,c_67]) ).
cnf(c_2246,plain,
multiply(inverse(multiply(A,multiply(B,multiply(inverse(C),C)))),multiply(A,D)) = multiply(C,multiply(inverse(multiply(B,C)),D)),
inference(copy,[status(thm)],[c_2745]) ).
cnf(c_2278,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(C),C)))) = B,
inference(paramod,[status(thm)],[c_1311,c_1322]) ).
cnf(c_2294,plain,
multiply(multiply(A,multiply(inverse(multiply(B,A)),multiply(B,multiply(inverse(A),A)))),a2) != a2,
inference(paramod,[status(thm)],[c_1322,c_1483]) ).
cnf(c_2331,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,multiply(inverse(multiply(inverse(C),C)),D))) = multiply(E,multiply(inverse(multiply(F,E)),multiply(F,D))),
inference(paramod,[status(thm)],[c_2246,c_1533]) ).
cnf(c_2334,plain,
multiply(A,multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(B,A)),multiply(B,C)))) = multiply(C,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2246,c_1420]) ).
cnf(c_2746,plain,
multiply(inverse(multiply(B,multiply(inverse(multiply(inverse(B),B)),C))),multiply(inverse(D),D)) = multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,F)),multiply(V6,multiply(inverse(B),multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_2246,c_1266]) ).
cnf(c_2351,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),multiply(inverse(E),E))))) = multiply(inverse(multiply(E,multiply(inverse(multiply(inverse(E),E)),C))),multiply(inverse(F),F)),
inference(copy,[status(thm)],[c_2746]) ).
cnf(c_2384,plain,
multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(D,multiply(inverse(multiply(inverse(D),D)),E)))) = multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,multiply(inverse(multiply(inverse(multiply(V7,D)),multiply(V7,B))),E)))),
inference(paramod,[status(thm)],[c_2246,c_988]) ).
cnf(c_2747,plain,
multiply(multiply(B,C),multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,C))),D)) = multiply(multiply(B,inverse(multiply(inverse(multiply(inverse(E),multiply(inverse(E),E))),multiply(inverse(E),multiply(inverse(E),E))))),multiply(C,D)),
inference(paramod,[status(thm)],[c_2246,c_512]) ).
cnf(c_2438,plain,
multiply(multiply(A,inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(B),B))),multiply(inverse(B),multiply(inverse(B),B))))),multiply(C,D)) = multiply(multiply(A,C),multiply(inverse(multiply(inverse(multiply(A,C)),multiply(A,C))),D)),
inference(copy,[status(thm)],[c_2747]) ).
cnf(c_2462,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),D))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,D),
inference(paramod,[status(thm)],[c_2278,c_1697]) ).
cnf(c_2748,plain,
multiply(A,D) = multiply(A,inverse(multiply(inverse(multiply(E,D)),multiply(E,multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_2462,c_1698]) ).
cnf(c_2470,plain,
multiply(A,inverse(multiply(inverse(multiply(B,C)),multiply(B,multiply(inverse(D),D))))) = multiply(A,C),
inference(copy,[status(thm)],[c_2748]) ).
cnf(c_2749,plain,
multiply(A,multiply(inverse(B),D)) = multiply(A,inverse(multiply(inverse(multiply(E,multiply(F,D))),multiply(E,multiply(F,B))))),
inference(paramod,[status(thm)],[c_2462,c_333]) ).
cnf(c_2476,plain,
multiply(A,inverse(multiply(inverse(multiply(B,multiply(C,D))),multiply(B,multiply(C,E))))) = multiply(A,multiply(inverse(E),D)),
inference(copy,[status(thm)],[c_2749]) ).
cnf(c_2481,plain,
multiply(multiply(A,multiply(inverse(B),B)),multiply(C,D)) = multiply(multiply(A,C),multiply(inverse(multiply(inverse(multiply(A,C)),multiply(A,C))),D)),
inference(paramod,[status(thm)],[c_2470,c_2438]) ).
cnf(c_2488,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(A),multiply(inverse(A),A))))) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_2470,c_1708]) ).
cnf(c_2514,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_2470,c_66]) ).
cnf(c_2528,plain,
multiply(inverse(multiply(inverse(A),A)),B) = B,
inference(paramod,[status(thm)],[c_2488,c_1316]) ).
cnf(c_2750,plain,
multiply(A,inverse(multiply(inverse(multiply(C,D)),multiply(C,E)))) = multiply(A,multiply(inverse(E),D)),
inference(paramod,[status(thm)],[c_2514,c_2476]) ).
cnf(c_2531,plain,
multiply(A,inverse(multiply(inverse(B),C))) = multiply(A,multiply(inverse(C),B)),
inference(paramod,[status(thm)],[c_2514,c_2750]) ).
cnf(c_2751,plain,
multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(D,E))) = multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,multiply(inverse(multiply(inverse(multiply(V7,D)),multiply(V7,B))),E)))),
inference(paramod,[status(thm)],[c_2528,c_2384]) ).
cnf(c_2752,plain,
multiply(inverse(multiply(B,C)),multiply(D,E)) = multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,multiply(inverse(multiply(inverse(multiply(V7,D)),multiply(V7,B))),E)))),
inference(paramod,[status(thm)],[c_2514,c_2751]) ).
cnf(c_2753,plain,
multiply(inverse(multiply(B,C)),multiply(D,E)) = multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,multiply(inverse(multiply(inverse(D),B)),E)))),
inference(paramod,[status(thm)],[c_2514,c_2752]) ).
cnf(c_2754,plain,
multiply(inverse(multiply(B,C)),multiply(D,E)) = multiply(inverse(multiply(V6,C)),multiply(V6,multiply(inverse(multiply(inverse(D),B)),E))),
inference(paramod,[status(thm)],[c_2514,c_2753]) ).
cnf(c_2546,plain,
multiply(inverse(multiply(A,B)),multiply(C,D)) = multiply(inverse(B),multiply(inverse(multiply(inverse(C),A)),D)),
inference(paramod,[status(thm)],[c_2514,c_2754]) ).
cnf(c_2755,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,D)) = multiply(E,multiply(inverse(multiply(F,E)),multiply(F,D))),
inference(paramod,[status(thm)],[c_2528,c_2331]) ).
cnf(c_2756,plain,
multiply(inverse(multiply(inverse(B),B)),D) = multiply(E,multiply(inverse(multiply(F,E)),multiply(F,D))),
inference(paramod,[status(thm)],[c_2514,c_2755]) ).
cnf(c_2757,plain,
D = multiply(E,multiply(inverse(multiply(F,E)),multiply(F,D))),
inference(paramod,[status(thm)],[c_2528,c_2756]) ).
cnf(c_2758,plain,
D = multiply(E,multiply(inverse(E),D)),
inference(paramod,[status(thm)],[c_2514,c_2757]) ).
cnf(c_2555,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(copy,[status(thm)],[c_2758]) ).
cnf(c_2759,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,E)))),multiply(inverse(F),F)) = multiply(inverse(multiply(V6,multiply(V7,multiply(V8,E)))),multiply(V6,multiply(V7,multiply(V8,C)))),
inference(paramod,[status(thm)],[c_2514,c_2197]) ).
cnf(c_2760,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),E))),multiply(inverse(F),F)) = multiply(inverse(multiply(V6,multiply(V7,multiply(V8,E)))),multiply(V6,multiply(V7,multiply(V8,C)))),
inference(paramod,[status(thm)],[c_2514,c_2759]) ).
cnf(c_2761,plain,
multiply(inverse(multiply(inverse(C),E)),multiply(inverse(F),F)) = multiply(inverse(multiply(V6,multiply(V7,multiply(V8,E)))),multiply(V6,multiply(V7,multiply(V8,C)))),
inference(paramod,[status(thm)],[c_2514,c_2760]) ).
cnf(c_2762,plain,
multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(F)),inverse(C))),F)) = multiply(inverse(multiply(V6,multiply(V7,multiply(V8,E)))),multiply(V6,multiply(V7,multiply(V8,C)))),
inference(paramod,[status(thm)],[c_2546,c_2761]) ).
cnf(c_2763,plain,
multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(F)),inverse(C))),F)) = multiply(inverse(multiply(V7,multiply(V8,E))),multiply(V7,multiply(V8,C))),
inference(paramod,[status(thm)],[c_2514,c_2762]) ).
cnf(c_2764,plain,
multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(F)),inverse(C))),F)) = multiply(inverse(multiply(V8,E)),multiply(V8,C)),
inference(paramod,[status(thm)],[c_2514,c_2763]) ).
cnf(c_2574,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),B)) = multiply(inverse(A),C),
inference(paramod,[status(thm)],[c_2514,c_2764]) ).
cnf(c_2765,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,F)))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,V7)),C))),multiply(V6,multiply(inverse(multiply(inverse(F),V7)),multiply(inverse(V8),V8)))),
inference(paramod,[status(thm)],[c_2514,c_2192]) ).
cnf(c_2766,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,V7)),C))),multiply(V6,multiply(inverse(multiply(inverse(F),V7)),multiply(inverse(V8),V8)))),
inference(paramod,[status(thm)],[c_2514,c_2765]) ).
cnf(c_2767,plain,
multiply(inverse(C),multiply(E,F)) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,V7)),C))),multiply(V6,multiply(inverse(multiply(inverse(F),V7)),multiply(inverse(V8),V8)))),
inference(paramod,[status(thm)],[c_2514,c_2766]) ).
cnf(c_2768,plain,
multiply(inverse(C),multiply(E,F)) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,V7)),C))),multiply(V6,multiply(inverse(V7),multiply(inverse(multiply(inverse(inverse(V8)),inverse(F))),V8)))),
inference(paramod,[status(thm)],[c_2546,c_2767]) ).
cnf(c_2769,plain,
multiply(inverse(C),multiply(E,F)) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,V7)),C))),multiply(V6,multiply(inverse(V7),F))),
inference(paramod,[status(thm)],[c_2574,c_2768]) ).
cnf(c_2770,plain,
multiply(inverse(C),multiply(E,F)) = multiply(inverse(multiply(inverse(multiply(E,V7)),C)),multiply(inverse(V7),F)),
inference(paramod,[status(thm)],[c_2514,c_2769]) ).
cnf(c_2771,plain,
multiply(inverse(C),multiply(E,F)) = multiply(inverse(C),multiply(inverse(multiply(inverse(inverse(V7)),inverse(multiply(E,V7)))),F)),
inference(paramod,[status(thm)],[c_2546,c_2770]) ).
cnf(c_2576,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(inverse(B)),inverse(multiply(C,B)))),D)) = multiply(inverse(A),multiply(C,D)),
inference(copy,[status(thm)],[c_2771]) ).
cnf(c_2772,plain,
multiply(inverse(multiply(inverse(B),multiply(C,D))),multiply(inverse(E),E)) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,V7)),multiply(V6,D)))),multiply(F,multiply(inverse(multiply(C,V7)),B))),
inference(paramod,[status(thm)],[c_2514,c_2131]) ).
cnf(c_2773,plain,
multiply(inverse(multiply(C,D)),multiply(inverse(multiply(inverse(inverse(E)),inverse(B))),E)) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,V7)),multiply(V6,D)))),multiply(F,multiply(inverse(multiply(C,V7)),B))),
inference(paramod,[status(thm)],[c_2546,c_2772]) ).
cnf(c_2774,plain,
multiply(inverse(multiply(C,D)),B) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,V7)),multiply(V6,D)))),multiply(F,multiply(inverse(multiply(C,V7)),B))),
inference(paramod,[status(thm)],[c_2574,c_2773]) ).
cnf(c_2775,plain,
multiply(inverse(multiply(C,D)),B) = multiply(inverse(multiply(F,multiply(inverse(V7),D))),multiply(F,multiply(inverse(multiply(C,V7)),B))),
inference(paramod,[status(thm)],[c_2514,c_2774]) ).
cnf(c_2776,plain,
multiply(inverse(multiply(C,D)),B) = multiply(inverse(multiply(inverse(V7),D)),multiply(inverse(multiply(C,V7)),B)),
inference(paramod,[status(thm)],[c_2514,c_2775]) ).
cnf(c_2777,plain,
multiply(inverse(multiply(C,D)),B) = multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(multiply(C,V7))),inverse(V7))),B)),
inference(paramod,[status(thm)],[c_2546,c_2776]) ).
cnf(c_2586,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(inverse(multiply(B,C))),inverse(C))),D)) = multiply(inverse(multiply(B,A)),D),
inference(copy,[status(thm)],[c_2777]) ).
cnf(c_2778,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(C),F))) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,F)))),
inference(paramod,[status(thm)],[c_2514,c_1994]) ).
cnf(c_2779,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(B,C)))),F))) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,F)))),
inference(paramod,[status(thm)],[c_2546,c_2778]) ).
cnf(c_2780,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(D),multiply(B,F))) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,F)))),
inference(paramod,[status(thm)],[c_2576,c_2779]) ).
cnf(c_2781,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(inverse(D)),inverse(A))),multiply(B,F))) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,F)))),
inference(paramod,[status(thm)],[c_2546,c_2780]) ).
cnf(c_2782,plain,
multiply(inverse(A),multiply(inverse(inverse(A)),multiply(inverse(multiply(inverse(B),inverse(inverse(D)))),F))) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,F)))),
inference(paramod,[status(thm)],[c_2546,c_2781]) ).
cnf(c_2783,plain,
multiply(inverse(multiply(inverse(B),inverse(inverse(D)))),F) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,F)))),
inference(paramod,[status(thm)],[c_2555,c_2782]) ).
cnf(c_2784,plain,
multiply(inverse(multiply(inverse(B),inverse(inverse(D)))),F) = multiply(inverse(multiply(V7,D)),multiply(V7,multiply(B,F))),
inference(paramod,[status(thm)],[c_2514,c_2783]) ).
cnf(c_2592,plain,
multiply(inverse(multiply(inverse(A),inverse(inverse(B)))),C) = multiply(inverse(B),multiply(A,C)),
inference(paramod,[status(thm)],[c_2514,c_2784]) ).
cnf(c_2785,plain,
multiply(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(multiply(C,D)),multiply(inverse(multiply(inverse(B),multiply(inverse(B),B))),multiply(inverse(multiply(E,multiply(inverse(B),B))),multiply(E,multiply(inverse(B),B))))))) = D,
inference(paramod,[status(thm)],[c_2514,c_1052]) ).
cnf(c_2786,plain,
multiply(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(multiply(C,D)),multiply(inverse(multiply(inverse(B),multiply(inverse(B),B))),multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))))) = D,
inference(paramod,[status(thm)],[c_2514,c_2785]) ).
cnf(c_2787,plain,
multiply(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(multiply(C,D)),multiply(inverse(multiply(inverse(B),multiply(inverse(B),B))),multiply(inverse(B),B))))) = D,
inference(paramod,[status(thm)],[c_2514,c_2786]) ).
cnf(c_2788,plain,
multiply(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(multiply(C,D)),multiply(inverse(multiply(inverse(B),B)),B)))) = D,
inference(paramod,[status(thm)],[c_2514,c_2787]) ).
cnf(c_2789,plain,
multiply(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(multiply(C,D)),B))) = D,
inference(paramod,[status(thm)],[c_2528,c_2788]) ).
cnf(c_2790,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),multiply(C,D))) = D,
inference(paramod,[status(thm)],[c_2531,c_2789]) ).
cnf(c_2618,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(paramod,[status(thm)],[c_2514,c_2790]) ).
cnf(c_2791,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,multiply(inverse(multiply(F,V6)),multiply(F,V7)))))) = multiply(inverse(multiply(V8,multiply(inverse(multiply(E,V9)),C))),multiply(V8,multiply(inverse(multiply(V10,V9)),multiply(V10,multiply(inverse(multiply(V11,V6)),multiply(V11,V7)))))),
inference(paramod,[status(thm)],[c_2514,c_869]) ).
cnf(c_2792,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,multiply(inverse(V6),V7))))) = multiply(inverse(multiply(V8,multiply(inverse(multiply(E,V9)),C))),multiply(V8,multiply(inverse(multiply(V10,V9)),multiply(V10,multiply(inverse(multiply(V11,V6)),multiply(V11,V7)))))),
inference(paramod,[status(thm)],[c_2514,c_2791]) ).
cnf(c_2793,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),multiply(E,multiply(inverse(V6),V7)))) = multiply(inverse(multiply(V8,multiply(inverse(multiply(E,V9)),C))),multiply(V8,multiply(inverse(multiply(V10,V9)),multiply(V10,multiply(inverse(multiply(V11,V6)),multiply(V11,V7)))))),
inference(paramod,[status(thm)],[c_2514,c_2792]) ).
cnf(c_2794,plain,
multiply(inverse(C),multiply(E,multiply(inverse(V6),V7))) = multiply(inverse(multiply(V8,multiply(inverse(multiply(E,V9)),C))),multiply(V8,multiply(inverse(multiply(V10,V9)),multiply(V10,multiply(inverse(multiply(V11,V6)),multiply(V11,V7)))))),
inference(paramod,[status(thm)],[c_2514,c_2793]) ).
cnf(c_2795,plain,
multiply(inverse(C),multiply(E,multiply(inverse(V6),V7))) = multiply(inverse(multiply(V8,multiply(inverse(multiply(E,V9)),C))),multiply(V8,multiply(inverse(multiply(V10,V9)),multiply(V10,multiply(inverse(V6),V7))))),
inference(paramod,[status(thm)],[c_2514,c_2794]) ).
cnf(c_2796,plain,
multiply(inverse(C),multiply(E,multiply(inverse(V6),V7))) = multiply(inverse(multiply(V8,multiply(inverse(multiply(E,V9)),C))),multiply(V8,multiply(inverse(V9),multiply(inverse(V6),V7)))),
inference(paramod,[status(thm)],[c_2514,c_2795]) ).
cnf(c_2797,plain,
multiply(inverse(C),multiply(E,multiply(inverse(V6),V7))) = multiply(inverse(multiply(inverse(multiply(E,V9)),C)),multiply(inverse(V9),multiply(inverse(V6),V7))),
inference(paramod,[status(thm)],[c_2514,c_2796]) ).
cnf(c_2798,plain,
multiply(inverse(C),multiply(E,multiply(inverse(V6),V7))) = multiply(inverse(C),multiply(inverse(multiply(inverse(inverse(V9)),inverse(multiply(E,V9)))),multiply(inverse(V6),V7))),
inference(paramod,[status(thm)],[c_2546,c_2797]) ).
cnf(c_2799,plain,
multiply(inverse(C),multiply(E,multiply(inverse(V6),V7))) = multiply(inverse(C),multiply(inverse(inverse(multiply(E,V9))),multiply(inverse(multiply(inverse(inverse(V6)),inverse(inverse(V9)))),V7))),
inference(paramod,[status(thm)],[c_2546,c_2798]) ).
cnf(c_2800,plain,
multiply(inverse(C),multiply(E,multiply(inverse(V6),V7))) = multiply(inverse(C),multiply(inverse(inverse(multiply(E,V9))),multiply(inverse(V9),multiply(inverse(V6),V7)))),
inference(paramod,[status(thm)],[c_2592,c_2799]) ).
cnf(c_2631,plain,
multiply(inverse(A),multiply(inverse(inverse(multiply(B,C))),multiply(inverse(C),multiply(inverse(D),E)))) = multiply(inverse(A),multiply(B,multiply(inverse(D),E))),
inference(copy,[status(thm)],[c_2800]) ).
cnf(c_2801,plain,
multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(V6,V7)),multiply(V6,V8)))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(B,F)),D))),multiply(V9,multiply(inverse(multiply(V10,V7)),multiply(V10,V8)))),
inference(paramod,[status(thm)],[c_2514,c_821]) ).
cnf(c_2802,plain,
multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(multiply(inverse(F),C)),multiply(inverse(multiply(V6,V7)),multiply(V6,V8)))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(B,F)),D))),multiply(V9,multiply(inverse(multiply(V10,V7)),multiply(V10,V8)))),
inference(paramod,[status(thm)],[c_2514,c_2801]) ).
cnf(c_2803,plain,
multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(multiply(inverse(F),C)),multiply(inverse(V7),V8))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(B,F)),D))),multiply(V9,multiply(inverse(multiply(V10,V7)),multiply(V10,V8)))),
inference(paramod,[status(thm)],[c_2514,c_2802]) ).
cnf(c_2804,plain,
multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(C),multiply(inverse(multiply(inverse(inverse(V7)),inverse(F))),V8))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(B,F)),D))),multiply(V9,multiply(inverse(multiply(V10,V7)),multiply(V10,V8)))),
inference(paramod,[status(thm)],[c_2546,c_2803]) ).
cnf(c_2805,plain,
multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(B,C)))),multiply(inverse(multiply(inverse(inverse(V7)),inverse(F))),V8))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(B,F)),D))),multiply(V9,multiply(inverse(multiply(V10,V7)),multiply(V10,V8)))),
inference(paramod,[status(thm)],[c_2546,c_2804]) ).
cnf(c_2806,plain,
multiply(inverse(D),multiply(inverse(inverse(multiply(B,C))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(V7)),inverse(F)))),inverse(inverse(C)))),V8))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(B,F)),D))),multiply(V9,multiply(inverse(multiply(V10,V7)),multiply(V10,V8)))),
inference(paramod,[status(thm)],[c_2546,c_2805]) ).
cnf(c_2807,plain,
multiply(inverse(D),multiply(inverse(inverse(multiply(B,C))),multiply(inverse(C),multiply(inverse(multiply(inverse(inverse(V7)),inverse(F))),V8)))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(B,F)),D))),multiply(V9,multiply(inverse(multiply(V10,V7)),multiply(V10,V8)))),
inference(paramod,[status(thm)],[c_2592,c_2806]) ).
cnf(c_2808,plain,
multiply(inverse(D),multiply(B,multiply(inverse(multiply(inverse(inverse(V7)),inverse(F))),V8))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(B,F)),D))),multiply(V9,multiply(inverse(multiply(V10,V7)),multiply(V10,V8)))),
inference(paramod,[status(thm)],[c_2631,c_2807]) ).
cnf(c_2809,plain,
multiply(inverse(D),multiply(B,multiply(inverse(multiply(inverse(inverse(V7)),inverse(F))),V8))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(B,F)),D))),multiply(V9,multiply(inverse(V7),V8))),
inference(paramod,[status(thm)],[c_2514,c_2808]) ).
cnf(c_2810,plain,
multiply(inverse(D),multiply(B,multiply(inverse(multiply(inverse(inverse(V7)),inverse(F))),V8))) = multiply(inverse(multiply(inverse(multiply(B,F)),D)),multiply(inverse(V7),V8)),
inference(paramod,[status(thm)],[c_2514,c_2809]) ).
cnf(c_2811,plain,
multiply(inverse(D),multiply(B,multiply(inverse(multiply(inverse(inverse(V7)),inverse(F))),V8))) = multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(V7)),inverse(multiply(B,F)))),V8)),
inference(paramod,[status(thm)],[c_2546,c_2810]) ).
cnf(c_2634,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(inverse(B)),inverse(multiply(C,D)))),E)) = multiply(inverse(A),multiply(C,multiply(inverse(multiply(inverse(inverse(B)),inverse(D))),E))),
inference(copy,[status(thm)],[c_2811]) ).
cnf(c_2812,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,multiply(F,V6))))) = multiply(inverse(multiply(V7,multiply(inverse(multiply(E,multiply(F,V8))),C))),multiply(V7,multiply(inverse(multiply(inverse(multiply(V9,V10)),multiply(V9,V8))),multiply(inverse(multiply(V11,V10)),multiply(V11,V6))))),
inference(paramod,[status(thm)],[c_2514,c_808]) ).
cnf(c_2813,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),multiply(E,multiply(F,V6)))) = multiply(inverse(multiply(V7,multiply(inverse(multiply(E,multiply(F,V8))),C))),multiply(V7,multiply(inverse(multiply(inverse(multiply(V9,V10)),multiply(V9,V8))),multiply(inverse(multiply(V11,V10)),multiply(V11,V6))))),
inference(paramod,[status(thm)],[c_2514,c_2812]) ).
cnf(c_2814,plain,
multiply(inverse(C),multiply(E,multiply(F,V6))) = multiply(inverse(multiply(V7,multiply(inverse(multiply(E,multiply(F,V8))),C))),multiply(V7,multiply(inverse(multiply(inverse(multiply(V9,V10)),multiply(V9,V8))),multiply(inverse(multiply(V11,V10)),multiply(V11,V6))))),
inference(paramod,[status(thm)],[c_2514,c_2813]) ).
cnf(c_2815,plain,
multiply(inverse(C),multiply(E,multiply(F,V6))) = multiply(inverse(multiply(V7,multiply(inverse(multiply(E,multiply(F,V8))),C))),multiply(V7,multiply(inverse(multiply(inverse(V10),V8)),multiply(inverse(multiply(V11,V10)),multiply(V11,V6))))),
inference(paramod,[status(thm)],[c_2514,c_2814]) ).
cnf(c_2816,plain,
multiply(inverse(C),multiply(E,multiply(F,V6))) = multiply(inverse(multiply(V7,multiply(inverse(multiply(E,multiply(F,V8))),C))),multiply(V7,multiply(inverse(multiply(inverse(V10),V8)),multiply(inverse(V10),V6)))),
inference(paramod,[status(thm)],[c_2514,c_2815]) ).
cnf(c_2817,plain,
multiply(inverse(C),multiply(E,multiply(F,V6))) = multiply(inverse(multiply(V7,multiply(inverse(multiply(E,multiply(F,V8))),C))),multiply(V7,multiply(inverse(V8),V6))),
inference(paramod,[status(thm)],[c_2514,c_2816]) ).
cnf(c_2818,plain,
multiply(inverse(C),multiply(E,multiply(F,V6))) = multiply(inverse(multiply(inverse(multiply(E,multiply(F,V8))),C)),multiply(inverse(V8),V6)),
inference(paramod,[status(thm)],[c_2514,c_2817]) ).
cnf(c_2819,plain,
multiply(inverse(C),multiply(E,multiply(F,V6))) = multiply(inverse(C),multiply(inverse(multiply(inverse(inverse(V8)),inverse(multiply(E,multiply(F,V8))))),V6)),
inference(paramod,[status(thm)],[c_2546,c_2818]) ).
cnf(c_2820,plain,
multiply(inverse(C),multiply(E,multiply(F,V6))) = multiply(inverse(C),multiply(E,multiply(inverse(multiply(inverse(inverse(V8)),inverse(multiply(F,V8)))),V6))),
inference(paramod,[status(thm)],[c_2634,c_2819]) ).
cnf(c_2635,plain,
multiply(inverse(A),multiply(B,multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(D,C)))),E))) = multiply(inverse(A),multiply(B,multiply(D,E))),
inference(copy,[status(thm)],[c_2820]) ).
cnf(c_2821,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),D)),multiply(inverse(multiply(F,C)),multiply(F,V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),D)),multiply(inverse(multiply(inverse(multiply(B,V8)),V7)),multiply(inverse(multiply(V9,V8)),multiply(V9,V6)))),
inference(paramod,[status(thm)],[c_2514,c_767]) ).
cnf(c_2822,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),D)),multiply(inverse(C),V6)) = multiply(inverse(multiply(inverse(multiply(A,V7)),D)),multiply(inverse(multiply(inverse(multiply(B,V8)),V7)),multiply(inverse(multiply(V9,V8)),multiply(V9,V6)))),
inference(paramod,[status(thm)],[c_2514,c_2821]) ).
cnf(c_2823,plain,
multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(A,multiply(B,C))))),V6)) = multiply(inverse(multiply(inverse(multiply(A,V7)),D)),multiply(inverse(multiply(inverse(multiply(B,V8)),V7)),multiply(inverse(multiply(V9,V8)),multiply(V9,V6)))),
inference(paramod,[status(thm)],[c_2546,c_2822]) ).
cnf(c_2824,plain,
multiply(inverse(D),multiply(A,multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(B,C)))),V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),D)),multiply(inverse(multiply(inverse(multiply(B,V8)),V7)),multiply(inverse(multiply(V9,V8)),multiply(V9,V6)))),
inference(paramod,[status(thm)],[c_2634,c_2823]) ).
cnf(c_2825,plain,
multiply(inverse(D),multiply(A,multiply(B,V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),D)),multiply(inverse(multiply(inverse(multiply(B,V8)),V7)),multiply(inverse(multiply(V9,V8)),multiply(V9,V6)))),
inference(paramod,[status(thm)],[c_2635,c_2824]) ).
cnf(c_2826,plain,
multiply(inverse(D),multiply(A,multiply(B,V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),D)),multiply(inverse(multiply(inverse(multiply(B,V8)),V7)),multiply(inverse(V8),V6))),
inference(paramod,[status(thm)],[c_2514,c_2825]) ).
cnf(c_2827,plain,
multiply(inverse(D),multiply(A,multiply(B,V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),D)),multiply(inverse(V7),multiply(inverse(multiply(inverse(inverse(V8)),inverse(multiply(B,V8)))),V6))),
inference(paramod,[status(thm)],[c_2546,c_2826]) ).
cnf(c_2828,plain,
multiply(inverse(D),multiply(A,multiply(B,V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),D)),multiply(inverse(V7),multiply(B,V6))),
inference(paramod,[status(thm)],[c_2576,c_2827]) ).
cnf(c_2829,plain,
multiply(inverse(D),multiply(A,multiply(B,V6))) = multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(V7)),inverse(multiply(A,V7)))),multiply(B,V6))),
inference(paramod,[status(thm)],[c_2546,c_2828]) ).
cnf(c_2830,plain,
multiply(inverse(D),multiply(A,multiply(B,V6))) = multiply(inverse(D),multiply(inverse(inverse(multiply(A,V7))),multiply(inverse(multiply(inverse(B),inverse(inverse(V7)))),V6))),
inference(paramod,[status(thm)],[c_2546,c_2829]) ).
cnf(c_2831,plain,
multiply(inverse(D),multiply(A,multiply(B,V6))) = multiply(inverse(D),multiply(inverse(inverse(multiply(A,V7))),multiply(inverse(V7),multiply(B,V6)))),
inference(paramod,[status(thm)],[c_2592,c_2830]) ).
cnf(c_2636,plain,
multiply(inverse(A),multiply(inverse(inverse(multiply(B,C))),multiply(inverse(C),multiply(D,E)))) = multiply(inverse(A),multiply(B,multiply(D,E))),
inference(copy,[status(thm)],[c_2831]) ).
cnf(c_2832,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(multiply(B,C)),C))),multiply(A,D))),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,multiply(B,C)))))) = D,
inference(paramod,[status(thm)],[c_2514,c_675]) ).
cnf(c_2833,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),C)),D)),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,multiply(B,C)))))) = D,
inference(paramod,[status(thm)],[c_2514,c_2832]) ).
cnf(c_2834,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),C)),D)),multiply(inverse(multiply(F,C)),multiply(F,multiply(B,C))))) = D,
inference(paramod,[status(thm)],[c_2514,c_2833]) ).
cnf(c_2835,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),C)),D)),multiply(inverse(C),multiply(B,C)))) = D,
inference(paramod,[status(thm)],[c_2514,c_2834]) ).
cnf(c_2836,plain,
inverse(multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(multiply(B,C)),C)))),multiply(B,C)))) = D,
inference(paramod,[status(thm)],[c_2546,c_2835]) ).
cnf(c_2837,plain,
inverse(multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(C)),multiply(inverse(C),multiply(B,C)))),multiply(B,C)))) = D,
inference(paramod,[status(thm)],[c_2531,c_2836]) ).
cnf(c_2838,plain,
inverse(multiply(inverse(D),multiply(inverse(multiply(B,C)),multiply(B,C)))) = D,
inference(paramod,[status(thm)],[c_2618,c_2837]) ).
cnf(c_2643,plain,
inverse(multiply(inverse(A),multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_2514,c_2838]) ).
cnf(c_2839,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(C,D)),E)),F)) = multiply(A,multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,multiply(C,inverse(multiply(inverse(F),multiply(inverse(D),multiply(inverse(D),D))))))))),
inference(paramod,[status(thm)],[c_2514,c_455]) ).
cnf(c_2840,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(C,D)),E)),F)) = multiply(A,multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,multiply(C,multiply(inverse(multiply(inverse(D),multiply(inverse(D),D))),F)))))),
inference(paramod,[status(thm)],[c_2531,c_2839]) ).
cnf(c_2841,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(C,D)),E)),F)) = multiply(A,multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,multiply(C,multiply(D,F)))))),
inference(paramod,[status(thm)],[c_2643,c_2840]) ).
cnf(c_2842,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(C,D)),E)),F)) = multiply(A,multiply(inverse(multiply(V7,E)),multiply(V7,multiply(C,multiply(D,F))))),
inference(paramod,[status(thm)],[c_2514,c_2841]) ).
cnf(c_2657,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),D)),E)) = multiply(A,multiply(inverse(D),multiply(B,multiply(C,E)))),
inference(paramod,[status(thm)],[c_2514,c_2842]) ).
cnf(c_2843,plain,
multiply(inverse(multiply(A,multiply(inverse(D),multiply(B,multiply(C,E))))),multiply(A,multiply(inverse(multiply(inverse(multiply(B,F)),D)),multiply(inverse(multiply(V6,F)),V7)))) = multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,multiply(inverse(multiply(V6,C)),V7)))),
inference(paramod,[status(thm)],[c_2657,c_445]) ).
cnf(c_2844,plain,
multiply(inverse(multiply(A,multiply(inverse(D),multiply(B,multiply(C,E))))),multiply(A,multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(multiply(V6,F))),inverse(multiply(B,F)))),V7)))) = multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,multiply(inverse(multiply(V6,C)),V7)))),
inference(paramod,[status(thm)],[c_2546,c_2843]) ).
cnf(c_2845,plain,
multiply(inverse(multiply(A,multiply(inverse(D),multiply(B,multiply(C,E))))),multiply(A,multiply(inverse(D),multiply(B,multiply(inverse(multiply(inverse(inverse(multiply(V6,F))),inverse(F))),V7))))) = multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,multiply(inverse(multiply(V6,C)),V7)))),
inference(paramod,[status(thm)],[c_2634,c_2844]) ).
cnf(c_2846,plain,
multiply(inverse(multiply(inverse(D),multiply(B,multiply(C,E)))),multiply(inverse(D),multiply(B,multiply(inverse(multiply(inverse(inverse(multiply(V6,F))),inverse(F))),V7)))) = multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,multiply(inverse(multiply(V6,C)),V7)))),
inference(paramod,[status(thm)],[c_2514,c_2845]) ).
cnf(c_2847,plain,
multiply(inverse(multiply(B,multiply(C,E))),multiply(B,multiply(inverse(multiply(inverse(inverse(multiply(V6,F))),inverse(F))),V7))) = multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,multiply(inverse(multiply(V6,C)),V7)))),
inference(paramod,[status(thm)],[c_2514,c_2846]) ).
cnf(c_2848,plain,
multiply(inverse(multiply(C,E)),multiply(inverse(multiply(inverse(inverse(multiply(V6,F))),inverse(F))),V7)) = multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,multiply(inverse(multiply(V6,C)),V7)))),
inference(paramod,[status(thm)],[c_2514,c_2847]) ).
cnf(c_2849,plain,
multiply(inverse(multiply(V6,multiply(C,E))),V7) = multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,multiply(inverse(multiply(V6,C)),V7)))),
inference(paramod,[status(thm)],[c_2586,c_2848]) ).
cnf(c_2850,plain,
multiply(inverse(multiply(V6,multiply(C,E))),V7) = multiply(inverse(multiply(V9,E)),multiply(V9,multiply(inverse(multiply(V6,C)),V7))),
inference(paramod,[status(thm)],[c_2514,c_2849]) ).
cnf(c_2661,plain,
multiply(inverse(multiply(A,multiply(B,C))),D) = multiply(inverse(C),multiply(inverse(multiply(A,B)),D)),
inference(paramod,[status(thm)],[c_2514,c_2850]) ).
cnf(c_2851,plain,
multiply(inverse(multiply(A,multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(multiply(E,C))),inverse(multiply(B,C)))),F)))),multiply(A,multiply(inverse(multiply(inverse(multiply(B,V6)),D)),V7))) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2546,c_443]) ).
cnf(c_2852,plain,
multiply(inverse(multiply(A,multiply(inverse(D),multiply(B,multiply(inverse(multiply(inverse(inverse(multiply(E,C))),inverse(C))),F))))),multiply(A,multiply(inverse(multiply(inverse(multiply(B,V6)),D)),V7))) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2634,c_2851]) ).
cnf(c_2853,plain,
multiply(inverse(multiply(A,multiply(inverse(D),multiply(B,multiply(inverse(multiply(inverse(inverse(multiply(E,C))),inverse(C))),F))))),multiply(A,multiply(inverse(D),multiply(B,multiply(V6,V7))))) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2657,c_2852]) ).
cnf(c_2854,plain,
multiply(inverse(multiply(inverse(D),multiply(B,multiply(inverse(multiply(inverse(inverse(multiply(E,C))),inverse(C))),F)))),multiply(inverse(D),multiply(B,multiply(V6,V7)))) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2514,c_2853]) ).
cnf(c_2855,plain,
multiply(inverse(multiply(B,multiply(inverse(multiply(inverse(inverse(multiply(E,C))),inverse(C))),F))),multiply(B,multiply(V6,V7))) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2514,c_2854]) ).
cnf(c_2856,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(E,C))),inverse(C))),F)),multiply(V6,V7)) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2514,c_2855]) ).
cnf(c_2857,plain,
multiply(inverse(F),multiply(inverse(multiply(inverse(V6),inverse(multiply(inverse(inverse(multiply(E,C))),inverse(C))))),V7)) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2546,c_2856]) ).
cnf(c_2858,plain,
multiply(inverse(F),multiply(inverse(multiply(inverse(V6),multiply(inverse(inverse(C)),inverse(multiply(E,C))))),V7)) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2531,c_2857]) ).
cnf(c_2859,plain,
multiply(inverse(F),multiply(inverse(inverse(multiply(E,C))),multiply(inverse(multiply(inverse(V6),inverse(inverse(C)))),V7))) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2661,c_2858]) ).
cnf(c_2860,plain,
multiply(inverse(F),multiply(inverse(inverse(multiply(E,C))),multiply(inverse(C),multiply(V6,V7)))) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2592,c_2859]) ).
cnf(c_2861,plain,
multiply(inverse(F),multiply(E,multiply(V6,V7))) = multiply(inverse(multiply(V8,multiply(V9,multiply(inverse(multiply(E,V6)),F)))),multiply(V8,multiply(V9,V7))),
inference(paramod,[status(thm)],[c_2636,c_2860]) ).
cnf(c_2862,plain,
multiply(inverse(F),multiply(E,multiply(V6,V7))) = multiply(inverse(multiply(V9,multiply(inverse(multiply(E,V6)),F))),multiply(V9,V7)),
inference(paramod,[status(thm)],[c_2514,c_2861]) ).
cnf(c_2863,plain,
multiply(inverse(F),multiply(E,multiply(V6,V7))) = multiply(inverse(multiply(inverse(multiply(E,V6)),F)),V7),
inference(paramod,[status(thm)],[c_2514,c_2862]) ).
cnf(c_2663,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),D) = multiply(inverse(C),multiply(A,multiply(B,D))),
inference(copy,[status(thm)],[c_2863]) ).
cnf(c_2864,plain,
multiply(inverse(multiply(A,multiply(inverse(D),multiply(B,multiply(C,E))))),multiply(A,multiply(inverse(multiply(F,D)),multiply(F,multiply(B,V6))))) = multiply(inverse(multiply(V7,multiply(V8,E))),multiply(V7,multiply(V8,multiply(inverse(multiply(V9,C)),multiply(V9,V6))))),
inference(paramod,[status(thm)],[c_2663,c_376]) ).
cnf(c_2865,plain,
multiply(inverse(multiply(A,multiply(inverse(D),multiply(B,multiply(C,E))))),multiply(A,multiply(inverse(D),multiply(B,V6)))) = multiply(inverse(multiply(V7,multiply(V8,E))),multiply(V7,multiply(V8,multiply(inverse(multiply(V9,C)),multiply(V9,V6))))),
inference(paramod,[status(thm)],[c_2514,c_2864]) ).
cnf(c_2866,plain,
multiply(inverse(multiply(inverse(D),multiply(B,multiply(C,E)))),multiply(inverse(D),multiply(B,V6))) = multiply(inverse(multiply(V7,multiply(V8,E))),multiply(V7,multiply(V8,multiply(inverse(multiply(V9,C)),multiply(V9,V6))))),
inference(paramod,[status(thm)],[c_2514,c_2865]) ).
cnf(c_2867,plain,
multiply(inverse(multiply(B,multiply(C,E))),multiply(B,V6)) = multiply(inverse(multiply(V7,multiply(V8,E))),multiply(V7,multiply(V8,multiply(inverse(multiply(V9,C)),multiply(V9,V6))))),
inference(paramod,[status(thm)],[c_2514,c_2866]) ).
cnf(c_2868,plain,
multiply(inverse(multiply(C,E)),V6) = multiply(inverse(multiply(V7,multiply(V8,E))),multiply(V7,multiply(V8,multiply(inverse(multiply(V9,C)),multiply(V9,V6))))),
inference(paramod,[status(thm)],[c_2514,c_2867]) ).
cnf(c_2869,plain,
multiply(inverse(multiply(C,E)),V6) = multiply(inverse(multiply(V7,multiply(V8,E))),multiply(V7,multiply(V8,multiply(inverse(C),V6)))),
inference(paramod,[status(thm)],[c_2514,c_2868]) ).
cnf(c_2870,plain,
multiply(inverse(multiply(C,E)),V6) = multiply(inverse(multiply(V8,E)),multiply(V8,multiply(inverse(C),V6))),
inference(paramod,[status(thm)],[c_2514,c_2869]) ).
cnf(c_2673,plain,
multiply(inverse(multiply(A,B)),C) = multiply(inverse(B),multiply(inverse(A),C)),
inference(paramod,[status(thm)],[c_2514,c_2870]) ).
cnf(c_2871,plain,
multiply(A,multiply(inverse(multiply(inverse(A),A)),multiply(inverse(A),multiply(inverse(B),multiply(B,C))))) = multiply(C,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2673,c_2334]) ).
cnf(c_2872,plain,
multiply(A,multiply(inverse(multiply(inverse(A),A)),multiply(inverse(A),C))) = multiply(C,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2618,c_2871]) ).
cnf(c_2873,plain,
multiply(A,multiply(inverse(A),multiply(inverse(inverse(A)),multiply(inverse(A),C)))) = multiply(C,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2673,c_2872]) ).
cnf(c_2874,plain,
multiply(A,multiply(inverse(A),C)) = multiply(C,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2618,c_2873]) ).
cnf(c_2875,plain,
C = multiply(C,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2555,c_2874]) ).
cnf(c_2704,plain,
multiply(A,multiply(inverse(B),B)) = A,
inference(copy,[status(thm)],[c_2875]) ).
cnf(c_2876,plain,
multiply(A,multiply(C,D)) = multiply(multiply(A,C),multiply(inverse(multiply(inverse(multiply(A,C)),multiply(A,C))),D)),
inference(paramod,[status(thm)],[c_2704,c_2481]) ).
cnf(c_2877,plain,
multiply(A,multiply(C,D)) = multiply(multiply(A,C),multiply(inverse(multiply(inverse(C),multiply(inverse(A),multiply(A,C)))),D)),
inference(paramod,[status(thm)],[c_2673,c_2876]) ).
cnf(c_2878,plain,
multiply(A,multiply(C,D)) = multiply(multiply(A,C),multiply(inverse(multiply(inverse(C),C)),D)),
inference(paramod,[status(thm)],[c_2618,c_2877]) ).
cnf(c_2879,plain,
multiply(A,multiply(C,D)) = multiply(multiply(A,C),multiply(inverse(C),multiply(inverse(inverse(C)),D))),
inference(paramod,[status(thm)],[c_2673,c_2878]) ).
cnf(c_2880,plain,
multiply(A,multiply(C,D)) = multiply(multiply(A,C),D),
inference(paramod,[status(thm)],[c_2555,c_2879]) ).
cnf(c_2718,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(copy,[status(thm)],[c_2880]) ).
cnf(c_2881,plain,
multiply(inverse(multiply(inverse(B),multiply(inverse(A),multiply(A,C)))),multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),multiply(inverse(E),E))))) = multiply(inverse(multiply(E,multiply(inverse(multiply(inverse(E),E)),C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_2673,c_2351]) ).
cnf(c_2882,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),multiply(inverse(E),E))))) = multiply(inverse(multiply(E,multiply(inverse(multiply(inverse(E),E)),C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_2618,c_2881]) ).
cnf(c_2883,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,inverse(E)))) = multiply(inverse(multiply(E,multiply(inverse(multiply(inverse(E),E)),C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_2704,c_2882]) ).
cnf(c_2884,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),multiply(inverse(D),multiply(D,inverse(E))))) = multiply(inverse(multiply(E,multiply(inverse(multiply(inverse(E),E)),C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_2673,c_2883]) ).
cnf(c_2885,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),inverse(E))) = multiply(inverse(multiply(E,multiply(inverse(multiply(inverse(E),E)),C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_2618,c_2884]) ).
cnf(c_2886,plain,
multiply(inverse(C),multiply(inverse(inverse(B)),multiply(inverse(B),inverse(E)))) = multiply(inverse(multiply(E,multiply(inverse(multiply(inverse(E),E)),C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_2673,c_2885]) ).
cnf(c_2887,plain,
multiply(inverse(C),inverse(E)) = multiply(inverse(multiply(E,multiply(inverse(multiply(inverse(E),E)),C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_2618,c_2886]) ).
cnf(c_2888,plain,
multiply(inverse(C),inverse(E)) = multiply(inverse(multiply(E,multiply(inverse(E),multiply(inverse(inverse(E)),C)))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_2673,c_2887]) ).
cnf(c_2889,plain,
multiply(inverse(C),inverse(E)) = multiply(inverse(multiply(E,C)),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_2555,c_2888]) ).
cnf(c_2890,plain,
multiply(inverse(C),inverse(E)) = inverse(multiply(E,C)),
inference(paramod,[status(thm)],[c_2704,c_2889]) ).
cnf(c_2723,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_2890]) ).
cnf(c_2891,plain,
multiply(multiply(A,multiply(multiply(inverse(A),inverse(B)),multiply(B,multiply(inverse(A),A)))),a2) != a2,
inference(paramod,[status(thm)],[c_2723,c_2294]) ).
cnf(c_2892,plain,
multiply(multiply(A,multiply(multiply(inverse(A),inverse(B)),B)),a2) != a2,
inference(paramod,[status(thm)],[c_2704,c_2891]) ).
cnf(c_2893,plain,
multiply(multiply(A,multiply(inverse(A),multiply(inverse(B),B))),a2) != a2,
inference(paramod,[status(thm)],[c_2718,c_2892]) ).
cnf(c_2894,plain,
multiply(multiply(A,inverse(A)),a2) != a2,
inference(paramod,[status(thm)],[c_2704,c_2893]) ).
cnf(c_2895,plain,
multiply(A,multiply(inverse(A),a2)) != a2,
inference(paramod,[status(thm)],[c_2718,c_2894]) ).
cnf(c_2896,plain,
a2 != a2,
inference(paramod,[status(thm)],[c_2555,c_2895]) ).
cnf(c_2726,plain,
$false,
inference(copy,[status(thm)],[c_2896]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP407-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.58 % Computer : n005.cluster.edu
% 0.10/0.58 % Model : x86_64 x86_64
% 0.10/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.58 % Memory : 8046.5625MB
% 0.10/0.58 % OS : Linux 6.8.0-71-generic
% 0.10/0.58 % CPULimit : 300
% 0.10/0.58 % WCLimit : 300
% 0.10/0.58 % DateTime : Fri Sep 25 14:52:32 UTC 2026
% 0.10/0.58 % CPUTime :
% 0.10/0.58 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.58 % Process 3754641 was started by sandbox on n005,
% 0.10/0.58 % Fri Sep 25 14:52:32 2026
% 0.10/0.58 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.58
% 0.10/0.58 % From the command line: assign(max_seconds, 300).
% 4.47/1.29
% 4.47/1.29 % Assigning unary symbol inverse kb_weight 0 and highest precedence (5).
% 4.47/1.29
% 4.47/1.29 % SZS status Unsatisfiable for theBenchmark
% 4.47/1.29
% 4.47/1.29 % Proof 1 at 0.58 (+ 0.11) seconds.
% 4.47/1.29 % Length of proof is 96.
% 4.47/1.29 % Level of proof is 27.
% 4.47/1.29 % Maximum clause weight is 97.000.
% 4.47/1.29 % Given clauses 51.
% 4.47/1.29
% 4.47/1.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------