%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP417-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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:29:10 AM UTC 2026
% Result : Unsatisfiable 3.81s 1.05s
% Output : CNFRefutation 3.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 2
% Syntax : Number of formulae : 226 ( 226 unt; 0 def)
% Number of atoms : 226 ( 225 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 21 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 840 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : inverse(multiply(VAR_0,inverse(multiply(inverse(multiply(inverse(multiply(VAR_1,VAR_0)),multiply(VAR_1,inverse(VAR_2)))),inverse(multiply(inverse(VAR_0),VAR_0)))))) = VAR_2,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),multiply(B,inverse(C)))),inverse(multiply(inverse(A),A)))))) = C,
inference(clausify,[status(thm)],[single_axiom]) ).
fof(prove_these_axioms_3,axiom,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('theBenchmark.p',prove_these_axioms_3) ).
cnf(c_2,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(clausify,[status(thm)],[prove_these_axioms_3]) ).
cnf(c_3,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(multiply(C,multiply(B,inverse(D)))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(multiply(inverse(B),B)))))))))) = D,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_4,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),multiply(B,C))),inverse(multiply(inverse(A),A)))))) = multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(E,D)),multiply(E,inverse(C)))),inverse(multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_8,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(multiply(C,multiply(B,D))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(multiply(inverse(B),B)))))))))) = multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(F,E)),multiply(F,inverse(D)))),inverse(multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_11,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),multiply(B,inverse(inverse(C))))),inverse(multiply(inverse(A),A))))) = C,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_14,plain,
inverse(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),multiply(B,C))),inverse(multiply(inverse(A),A))))))) = C,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_24,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),C)),inverse(multiply(inverse(A),A)))))) = multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(inverse(C))))),inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_11,c_1]) ).
cnf(c_48,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(inverse(multiply(B,inverse(C))))))),inverse(multiply(inverse(B),B))) = C,
inference(paramod,[status(thm)],[c_24,c_1]) ).
cnf(c_2117,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),multiply(B,inverse(C)))),inverse(multiply(inverse(A),A)))))) = multiply(D,inverse(inverse(multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(D,E)),C)),inverse(multiply(inverse(E),E)))))))),
inference(paramod,[status(thm)],[c_24,c_4]) ).
cnf(c_2118,plain,
C = multiply(D,inverse(inverse(multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(D,E)),C)),inverse(multiply(inverse(E),E)))))))),
inference(paramod,[status(thm)],[c_1,c_2117]) ).
cnf(c_71,plain,
multiply(A,inverse(inverse(multiply(B,inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),inverse(multiply(inverse(B),B)))))))) = C,
inference(copy,[status(thm)],[c_2118]) ).
cnf(c_82,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(inverse(multiply(B,C)))))),inverse(multiply(inverse(B),B)))) = C,
inference(paramod,[status(thm)],[c_24,c_14]) ).
cnf(c_96,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),C)),inverse(multiply(inverse(A),A)))))) = inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(B,D)),C)),inverse(multiply(inverse(D),D)))))),
inference(paramod,[status(thm)],[c_24,c_24]) ).
cnf(c_104,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(inverse(multiply(C,inverse(D))))))),A)),D)),inverse(multiply(inverse(A),A)))))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_48,c_1]) ).
cnf(c_2119,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(D,C)),multiply(D,inverse(E)))),inverse(multiply(inverse(C),C))))))))),inverse(multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(multiply(F,B)),multiply(F,E))),inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_4,c_48]) ).
cnf(c_115,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),inverse(multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_1,c_2119]) ).
cnf(c_2120,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),multiply(B,inverse(multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(D,C)),E)),inverse(multiply(inverse(C),C))))))))),inverse(multiply(inverse(A),A)))))) = multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(D,F)),E)),inverse(multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_71,c_4]) ).
cnf(c_143,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),C)),inverse(multiply(inverse(A),A))))) = multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(B,D)),C)),inverse(multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_1,c_2120]) ).
cnf(c_2121,plain,
multiply(A,inverse(inverse(multiply(B,inverse(multiply(inverse(C),inverse(multiply(inverse(B),B)))))))) = inverse(inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),D)),C)),inverse(multiply(inverse(D),D))))))),
inference(paramod,[status(thm)],[c_71,c_71]) ).
cnf(c_166,plain,
inverse(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),A)),D)),inverse(multiply(inverse(A),A))))))) = multiply(B,inverse(inverse(multiply(C,inverse(multiply(inverse(D),inverse(multiply(inverse(C),C)))))))),
inference(copy,[status(thm)],[c_2121]) ).
cnf(c_204,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(inverse(multiply(B,C)))))),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(multiply(C,D)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))) = D,
inference(paramod,[status(thm)],[c_82,c_71]) ).
cnf(c_2122,plain,
inverse(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,A)),multiply(B,C))),inverse(multiply(inverse(A),A)))),multiply(inverse(multiply(inverse(multiply(D,A)),multiply(D,C))),E))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))))))) = E,
inference(paramod,[status(thm)],[c_115,c_14]) ).
cnf(c_220,plain,
multiply(inverse(multiply(A,B)),inverse(inverse(multiply(multiply(A,C),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),E)),inverse(multiply(inverse(multiply(A,C)),multiply(A,C))))))))) = E,
inference(paramod,[status(thm)],[c_166,c_2122]) ).
cnf(c_2123,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(B,C)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))))) = multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,A)),multiply(E,inverse(inverse(multiply(A,B)))))),D)),C)),inverse(multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_82,c_143]) ).
cnf(c_277,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(inverse(multiply(C,D)))))),A)),E)),inverse(multiply(inverse(A),A))))) = multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(D,E)),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))))),
inference(copy,[status(thm)],[c_2123]) ).
cnf(c_286,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = multiply(inverse(A),A),
inference(paramod,[status(thm)],[c_277,c_104]) ).
cnf(c_299,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),inverse(multiply(inverse(multiply(multiply(inverse(B),B),multiply(inverse(multiply(inverse(B),B)),C))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))))),inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))))))))))) = C,
inference(paramod,[status(thm)],[c_286,c_14]) ).
cnf(c_308,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))),inverse(C))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))))),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))))))) = C,
inference(paramod,[status(thm)],[c_286,c_48]) ).
cnf(c_376,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),inverse(multiply(inverse(multiply(multiply(inverse(B),B),C)),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))))),inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))))) = inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),D)),C)),inverse(multiply(inverse(D),D)))))),
inference(paramod,[status(thm)],[c_286,c_96]) ).
cnf(c_2124,plain,
inverse(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),A)),D)),inverse(multiply(inverse(A),A))))))) = inverse(inverse(multiply(multiply(B,E),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,C)),multiply(F,E))),D)),inverse(multiply(inverse(multiply(B,E)),multiply(B,E)))))))),
inference(paramod,[status(thm)],[c_220,c_14]) ).
cnf(c_2125,plain,
multiply(B,inverse(inverse(multiply(C,inverse(multiply(inverse(D),inverse(multiply(inverse(C),C)))))))) = inverse(inverse(multiply(multiply(B,E),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,C)),multiply(F,E))),D)),inverse(multiply(inverse(multiply(B,E)),multiply(B,E)))))))),
inference(paramod,[status(thm)],[c_166,c_2124]) ).
cnf(c_403,plain,
inverse(inverse(multiply(multiply(A,B),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,B))),E)),inverse(multiply(inverse(multiply(A,B)),multiply(A,B)))))))) = multiply(A,inverse(inverse(multiply(D,inverse(multiply(inverse(E),inverse(multiply(inverse(D),D)))))))),
inference(copy,[status(thm)],[c_2125]) ).
cnf(c_2126,plain,
multiply(inverse(multiply(A,B)),inverse(inverse(multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),D)),inverse(multiply(inverse(C),C)))))))) = D,
inference(paramod,[status(thm)],[c_143,c_220]) ).
cnf(c_451,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(inverse(multiply(B,inverse(multiply(inverse(C),inverse(multiply(inverse(B),B))))))))) = C,
inference(paramod,[status(thm)],[c_166,c_2126]) ).
cnf(c_2127,plain,
multiply(multiply(inverse(A),A),inverse(inverse(multiply(multiply(inverse(multiply(inverse(A),A)),B),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))),multiply(C,B))),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(multiply(inverse(A),A)),B))))))))) = E,
inference(paramod,[status(thm)],[c_286,c_220]) ).
cnf(c_452,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))),inverse(multiply(inverse(C),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))))),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))))))))))))) = C,
inference(paramod,[status(thm)],[c_403,c_2127]) ).
cnf(c_471,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(inverse(multiply(inverse(multiply(C,B)),multiply(C,D))),inverse(multiply(inverse(B),B))))))),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(inverse(multiply(inverse(multiply(C,B)),multiply(C,D))),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(E),inverse(multiply(multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(V6,F)),multiply(V6,inverse(D)))),inverse(multiply(inverse(F),F))))),multiply(B,inverse(multiply(inverse(multiply(inverse(multiply(C,B)),multiply(C,D))),inverse(multiply(inverse(B),B)))))))))))))) = E,
inference(paramod,[status(thm)],[c_4,c_451]) ).
cnf(c_2128,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(D,C)),multiply(D,inverse(E)))),inverse(multiply(inverse(C),C)))))))) = multiply(inverse(multiply(F,B)),multiply(F,E)),
inference(paramod,[status(thm)],[c_4,c_451]) ).
cnf(c_472,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_1,c_2128]) ).
cnf(c_2129,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(inverse(multiply(B,inverse(multiply(C,inverse(multiply(inverse(B),B))))))))) = multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,inverse(inverse(multiply(E,C)))))),inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_82,c_451]) ).
cnf(c_480,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(inverse(multiply(B,C)))))),inverse(multiply(inverse(B),B))) = multiply(inverse(multiply(D,E)),multiply(D,inverse(inverse(multiply(E,inverse(multiply(C,inverse(multiply(inverse(E),E))))))))),
inference(copy,[status(thm)],[c_2129]) ).
cnf(c_485,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(multiply(inverse(B),B)))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_286,c_451]) ).
cnf(c_2130,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(inverse(multiply(C,inverse(A))))))),inverse(multiply(inverse(C),C)))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_48,c_485]) ).
cnf(c_602,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_48,c_2130]) ).
cnf(c_2131,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(E,D)),multiply(E,inverse(F)))),inverse(multiply(inverse(D),D))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))) = inverse(multiply(inverse(multiply(C,multiply(B,F))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(multiply(inverse(B),B)))))))),
inference(paramod,[status(thm)],[c_8,c_71]) ).
cnf(c_676,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(A)))),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(A)))),inverse(multiply(inverse(B),B)))))))) = multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(A)))),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(F,E)),multiply(F,inverse(C)))),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))),
inference(copy,[status(thm)],[c_2131]) ).
cnf(c_688,plain,
inverse(multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(A)),inverse(A))))))) = A,
inference(paramod,[status(thm)],[c_602,c_1]) ).
cnf(c_706,plain,
inverse(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(A),A))))))) = A,
inference(paramod,[status(thm)],[c_602,c_14]) ).
cnf(c_713,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),C)),inverse(multiply(inverse(A),A)))))) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(inverse(C))),B)),multiply(inverse(D),D))),inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_602,c_24]) ).
cnf(c_728,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))),inverse(multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,A))),inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_602,c_115]) ).
cnf(c_751,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_602,c_472]) ).
cnf(c_752,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,A)),
inference(paramod,[status(thm)],[c_602,c_472]) ).
cnf(c_755,plain,
inverse(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C))))))) = A,
inference(paramod,[status(thm)],[c_602,c_706]) ).
cnf(c_769,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_751,c_602]) ).
cnf(c_834,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_769,c_472]) ).
cnf(c_871,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(B),B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),E)),A)),
inference(paramod,[status(thm)],[c_769,c_752]) ).
cnf(c_883,plain,
inverse(multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C)))))) = A,
inference(paramod,[status(thm)],[c_602,c_688]) ).
cnf(c_2132,plain,
multiply(inverse(multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(C)),inverse(C))))))),multiply(inverse(D),D)) = multiply(C,multiply(inverse(C),A)),
inference(paramod,[status(thm)],[c_688,c_752]) ).
cnf(c_900,plain,
multiply(A,multiply(inverse(B),B)) = multiply(C,multiply(inverse(C),A)),
inference(paramod,[status(thm)],[c_883,c_2132]) ).
cnf(c_2133,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))),inverse(multiply(inverse(C),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))))))))))) = C,
inference(paramod,[status(thm)],[c_883,c_452]) ).
cnf(c_903,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))),C))))) = C,
inference(paramod,[status(thm)],[c_883,c_2133]) ).
cnf(c_2134,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),inverse(multiply(inverse(multiply(multiply(inverse(B),B),C)),inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))) = inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),D)),C)),inverse(multiply(inverse(D),D)))))),
inference(paramod,[status(thm)],[c_883,c_376]) ).
cnf(c_904,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),multiply(multiply(inverse(B),B),C))) = inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),D)),C)),inverse(multiply(inverse(D),D)))))),
inference(paramod,[status(thm)],[c_883,c_2134]) ).
cnf(c_2135,plain,
multiply(inverse(inverse(C)),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))))),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))))))) = C,
inference(paramod,[status(thm)],[c_903,c_308]) ).
cnf(c_908,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))))) = A,
inference(paramod,[status(thm)],[c_883,c_2135]) ).
cnf(c_2136,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),inverse(multiply(inverse(multiply(multiply(inverse(B),B),multiply(inverse(multiply(inverse(B),B)),C))),inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))))))))) = C,
inference(paramod,[status(thm)],[c_908,c_299]) ).
cnf(c_910,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),multiply(multiply(inverse(B),B),multiply(inverse(multiply(inverse(B),B)),C))))) = C,
inference(paramod,[status(thm)],[c_883,c_2136]) ).
cnf(c_2137,plain,
multiply(A,multiply(inverse(A),inverse(multiply(inverse(B),B)))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_900,c_602]) ).
cnf(c_921,plain,
multiply(inverse(A),A) = multiply(B,multiply(inverse(B),inverse(multiply(inverse(C),C)))),
inference(copy,[status(thm)],[c_2137]) ).
cnf(c_2138,plain,
multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_769,c_900]) ).
cnf(c_943,plain,
multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))) = multiply(A,multiply(inverse(D),D)),
inference(copy,[status(thm)],[c_2138]) ).
cnf(c_954,plain,
multiply(A,multiply(inverse(A),B)) = multiply(C,multiply(inverse(C),B)),
inference(paramod,[status(thm)],[c_900,c_900]) ).
cnf(c_1054,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(D),D))))) = multiply(inverse(multiply(C,B)),multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_921,c_751]) ).
cnf(c_1058,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(B),inverse(multiply(inverse(C),C))))),multiply(inverse(D),D)) = multiply(inverse(multiply(inverse(E),E)),multiply(B,A)),
inference(paramod,[status(thm)],[c_921,c_752]) ).
cnf(c_2139,plain,
inverse(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D))))))))) = A,
inference(paramod,[status(thm)],[c_883,c_755]) ).
cnf(c_1069,plain,
inverse(inverse(multiply(A,multiply(inverse(B),B)))) = A,
inference(paramod,[status(thm)],[c_883,c_2139]) ).
cnf(c_2140,plain,
inverse(multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))))))) = A,
inference(paramod,[status(thm)],[c_883,c_883]) ).
cnf(c_1099,plain,
inverse(multiply(inverse(A),multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_883,c_2140]) ).
cnf(c_2141,plain,
multiply(A,multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),E)),A)),
inference(paramod,[status(thm)],[c_1099,c_871]) ).
cnf(c_1131,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),C)) = multiply(C,multiply(inverse(D),D)),
inference(copy,[status(thm)],[c_2141]) ).
cnf(c_2142,plain,
multiply(multiply(inverse(A),B),inverse(multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,A))),inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_1099,c_728]) ).
cnf(c_1145,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),inverse(multiply(inverse(B),B))) = multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B))),
inference(copy,[status(thm)],[c_2142]) ).
cnf(c_1148,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,A)),C)),inverse(multiply(inverse(A),A)))))) = multiply(multiply(inverse(inverse(inverse(C))),B),inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_1099,c_713]) ).
cnf(c_2143,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),inverse(multiply(inverse(inverse(multiply(multiply(inverse(inverse(A)),B),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(A)))),inverse(multiply(inverse(B),B)))))))) = multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(A)))),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(F,E)),multiply(F,inverse(C)))),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))),
inference(paramod,[status(thm)],[c_1145,c_676]) ).
cnf(c_2144,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),inverse(multiply(inverse(inverse(multiply(multiply(inverse(inverse(A)),B),inverse(multiply(inverse(B),B))))),inverse(multiply(multiply(inverse(inverse(A)),B),inverse(multiply(inverse(B),B)))))))) = multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(A)))),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(F,E)),multiply(F,inverse(C)))),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))),
inference(paramod,[status(thm)],[c_1145,c_2143]) ).
cnf(c_1258,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),inverse(multiply(inverse(inverse(multiply(multiply(inverse(inverse(A)),B),inverse(multiply(inverse(B),B))))),inverse(multiply(multiply(inverse(inverse(A)),B),inverse(multiply(inverse(B),B)))))))) = multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(A)))),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))),
inference(paramod,[status(thm)],[c_1145,c_2144]) ).
cnf(c_2145,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(multiply(inverse(D),B),inverse(multiply(inverse(B),B))))))),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(inverse(multiply(inverse(multiply(C,B)),multiply(C,D))),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(E),inverse(multiply(multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(V6,F)),multiply(V6,inverse(D)))),inverse(multiply(inverse(F),F))))),multiply(B,inverse(multiply(inverse(multiply(inverse(multiply(C,B)),multiply(C,D))),inverse(multiply(inverse(B),B)))))))))))))) = E,
inference(paramod,[status(thm)],[c_1145,c_471]) ).
cnf(c_2146,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(multiply(inverse(D),B),inverse(multiply(inverse(B),B))))))),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(D),B),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(E),inverse(multiply(multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(V6,F)),multiply(V6,inverse(D)))),inverse(multiply(inverse(F),F))))),multiply(B,inverse(multiply(inverse(multiply(inverse(multiply(C,B)),multiply(C,D))),inverse(multiply(inverse(B),B)))))))))))))) = E,
inference(paramod,[status(thm)],[c_1145,c_2145]) ).
cnf(c_2147,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(multiply(inverse(D),B),inverse(multiply(inverse(B),B))))))),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(D),B),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(E),inverse(multiply(multiply(F,inverse(multiply(multiply(inverse(inverse(D)),F),inverse(multiply(inverse(F),F))))),multiply(B,inverse(multiply(inverse(multiply(inverse(multiply(C,B)),multiply(C,D))),inverse(multiply(inverse(B),B)))))))))))))) = E,
inference(paramod,[status(thm)],[c_1145,c_2146]) ).
cnf(c_1279,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B))))))),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_1145,c_2147]) ).
cnf(c_2148,plain,
multiply(multiply(inverse(inverse(inverse(multiply(B,C)))),B),inverse(multiply(inverse(B),B))) = multiply(inverse(multiply(D,E)),multiply(D,inverse(inverse(multiply(E,inverse(multiply(C,inverse(multiply(inverse(E),E))))))))),
inference(paramod,[status(thm)],[c_1145,c_480]) ).
cnf(c_1413,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(inverse(multiply(B,inverse(multiply(C,inverse(multiply(inverse(B),B))))))))) = multiply(multiply(inverse(inverse(inverse(multiply(D,C)))),D),inverse(multiply(inverse(D),D))),
inference(copy,[status(thm)],[c_2148]) ).
cnf(c_1457,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),multiply(multiply(inverse(B),B),C))) = multiply(multiply(inverse(inverse(inverse(C))),inverse(multiply(inverse(B),B))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_1148,c_904]) ).
cnf(c_1486,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,B))),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))),E)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))) = E,
inference(paramod,[status(thm)],[c_755,c_204]) ).
cnf(c_1503,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(inverse(multiply(inverse(C),C)))))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(multiply(multiply(inverse(D),D),E)),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))))) = E,
inference(paramod,[status(thm)],[c_769,c_204]) ).
cnf(c_1566,plain,
inverse(inverse(multiply(A,multiply(inverse(A),B)))) = B,
inference(paramod,[status(thm)],[c_900,c_1069]) ).
cnf(c_1596,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = multiply(inverse(C),B),
inference(paramod,[status(thm)],[c_472,c_1099]) ).
cnf(c_1603,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),C)) = multiply(D,multiply(inverse(D),C)),
inference(paramod,[status(thm)],[c_1099,c_751]) ).
cnf(c_1605,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C))) = multiply(inverse(C),B),
inference(paramod,[status(thm)],[c_751,c_1099]) ).
cnf(c_1659,plain,
multiply(multiply(inverse(inverse(inverse(multiply(inverse(A),A)))),inverse(multiply(inverse(B),B))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(multiply(multiply(inverse(C),C),D)),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))))) = D,
inference(paramod,[status(thm)],[c_1596,c_1503]) ).
cnf(c_1664,plain,
multiply(multiply(inverse(A),A),inverse(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C)))),D)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))))) = D,
inference(paramod,[status(thm)],[c_1596,c_1486]) ).
cnf(c_1721,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),inverse(multiply(inverse(inverse(multiply(multiply(inverse(inverse(A)),B),inverse(multiply(inverse(B),B))))),inverse(multiply(multiply(inverse(inverse(A)),B),inverse(multiply(inverse(B),B)))))))) = multiply(multiply(inverse(inverse(A)),B),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(multiply(D,inverse(multiply(multiply(inverse(inverse(C)),D),inverse(multiply(inverse(D),D))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))),
inference(paramod,[status(thm)],[c_1596,c_1258]) ).
cnf(c_2149,plain,
inverse(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,C)))) = C,
inference(paramod,[status(thm)],[c_751,c_1566]) ).
cnf(c_1801,plain,
inverse(multiply(inverse(A),inverse(multiply(inverse(B),B)))) = A,
inference(paramod,[status(thm)],[c_1596,c_2149]) ).
cnf(c_1814,plain,
inverse(inverse(multiply(A,multiply(B,multiply(inverse(B),C))))) = multiply(inverse(inverse(A)),C),
inference(paramod,[status(thm)],[c_954,c_1566]) ).
cnf(c_2150,plain,
inverse(inverse(multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(inverse(C),C))))))) = A,
inference(paramod,[status(thm)],[c_921,c_1566]) ).
cnf(c_1818,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_1814,c_2150]) ).
cnf(c_2151,plain,
multiply(A,multiply(B,C)) = multiply(multiply(inverse(inverse(A)),B),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(multiply(D,inverse(multiply(multiply(inverse(inverse(C)),D),inverse(multiply(inverse(D),D))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))),
inference(paramod,[status(thm)],[c_1801,c_1721]) ).
cnf(c_2152,plain,
multiply(A,multiply(B,C)) = multiply(multiply(inverse(inverse(A)),B),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(multiply(D,inverse(multiply(multiply(inverse(inverse(C)),D),inverse(multiply(inverse(D),D))))),inverse(multiply(inverse(B),B)))))))),
inference(paramod,[status(thm)],[c_1818,c_2151]) ).
cnf(c_1852,plain,
multiply(multiply(inverse(inverse(A)),B),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(multiply(C,inverse(multiply(multiply(inverse(inverse(D)),C),inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(B),B)))))))) = multiply(A,multiply(B,D)),
inference(copy,[status(thm)],[c_2152]) ).
cnf(c_2153,plain,
multiply(multiply(inverse(A),A),inverse(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(multiply(inverse(B),B),D)),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))))) = D,
inference(paramod,[status(thm)],[c_1801,c_1664]) ).
cnf(c_2154,plain,
multiply(multiply(inverse(A),A),inverse(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(multiply(inverse(B),B),D)),inverse(multiply(inverse(A),A)))))))) = D,
inference(paramod,[status(thm)],[c_1818,c_2153]) ).
cnf(c_1871,plain,
multiply(multiply(inverse(A),A),inverse(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(multiply(inverse(B),B),C))))) = C,
inference(paramod,[status(thm)],[c_1801,c_2154]) ).
cnf(c_2155,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(multiply(multiply(inverse(C),C),D)),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))))) = D,
inference(paramod,[status(thm)],[c_1818,c_1659]) ).
cnf(c_2156,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(multiply(multiply(inverse(C),C),D)),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))))) = D,
inference(paramod,[status(thm)],[c_1818,c_2155]) ).
cnf(c_2157,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(multiply(multiply(inverse(C),C),D)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))))) = D,
inference(paramod,[status(thm)],[c_1818,c_2156]) ).
cnf(c_2158,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(multiply(multiply(inverse(C),C),D)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))))))) = D,
inference(paramod,[status(thm)],[c_1818,c_2157]) ).
cnf(c_2159,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(multiply(multiply(inverse(C),C),D)),inverse(multiply(inverse(B),B)))))))) = D,
inference(paramod,[status(thm)],[c_1818,c_2158]) ).
cnf(c_1874,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(inverse(multiply(inverse(B),B)),multiply(multiply(inverse(C),C),D))))) = D,
inference(paramod,[status(thm)],[c_1801,c_2159]) ).
cnf(c_2160,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),multiply(multiply(inverse(B),B),C))) = multiply(multiply(inverse(inverse(inverse(C))),inverse(multiply(inverse(B),B))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_1818,c_1457]) ).
cnf(c_2161,plain,
inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),C))) = multiply(multiply(inverse(inverse(inverse(C))),inverse(multiply(inverse(B),B))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_1801,c_2160]) ).
cnf(c_2162,plain,
inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),C))) = multiply(inverse(C),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_1818,c_2161]) ).
cnf(c_1893,plain,
inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),C))) = multiply(inverse(C),inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_1818,c_2162]) ).
cnf(c_2163,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),multiply(multiply(inverse(B),B),multiply(inverse(multiply(inverse(B),B)),C))))) = C,
inference(paramod,[status(thm)],[c_1818,c_910]) ).
cnf(c_2164,plain,
inverse(inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),multiply(inverse(multiply(inverse(B),B)),C))))) = C,
inference(paramod,[status(thm)],[c_1801,c_2163]) ).
cnf(c_2165,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),inverse(multiply(inverse(B),B)))) = C,
inference(paramod,[status(thm)],[c_1893,c_2164]) ).
cnf(c_1971,plain,
multiply(inverse(multiply(inverse(A),A)),B) = B,
inference(paramod,[status(thm)],[c_1801,c_2165]) ).
cnf(c_2000,plain,
multiply(multiply(inverse(inverse(A)),B),inverse(inverse(inverse(multiply(multiply(C,inverse(multiply(multiply(inverse(inverse(D)),C),inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(B),B))))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_1971,c_1852]) ).
cnf(c_2166,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(inverse(multiply(multiply(inverse(C),C),D)))) = D,
inference(paramod,[status(thm)],[c_1971,c_1874]) ).
cnf(c_2023,plain,
inverse(inverse(multiply(multiply(inverse(A),A),B))) = B,
inference(paramod,[status(thm)],[c_1971,c_2166]) ).
cnf(c_2167,plain,
multiply(multiply(inverse(A),A),inverse(inverse(multiply(multiply(inverse(B),B),C)))) = C,
inference(paramod,[status(thm)],[c_1971,c_1871]) ).
cnf(c_2026,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_2023,c_2167]) ).
cnf(c_2051,plain,
inverse(multiply(inverse(A),B)) = multiply(inverse(B),A),
inference(paramod,[status(thm)],[c_1971,c_1605]) ).
cnf(c_2168,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(B),B)),C)) = multiply(D,multiply(inverse(D),C)),
inference(paramod,[status(thm)],[c_2051,c_1603]) ).
cnf(c_2169,plain,
multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),C)) = multiply(D,multiply(inverse(D),C)),
inference(paramod,[status(thm)],[c_2051,c_2168]) ).
cnf(c_2170,plain,
multiply(multiply(inverse(A),A),C) = multiply(D,multiply(inverse(D),C)),
inference(paramod,[status(thm)],[c_2026,c_2169]) ).
cnf(c_2171,plain,
C = multiply(D,multiply(inverse(D),C)),
inference(paramod,[status(thm)],[c_2026,c_2170]) ).
cnf(c_2052,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(copy,[status(thm)],[c_2171]) ).
cnf(c_2172,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(B),B)),C)) = multiply(C,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2051,c_1131]) ).
cnf(c_2173,plain,
multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),C)) = multiply(C,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2051,c_2172]) ).
cnf(c_2174,plain,
multiply(multiply(inverse(A),A),C) = multiply(C,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2026,c_2173]) ).
cnf(c_2175,plain,
C = multiply(C,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2026,c_2174]) ).
cnf(c_2062,plain,
multiply(A,multiply(inverse(B),B)) = A,
inference(copy,[status(thm)],[c_2175]) ).
cnf(c_2176,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(B),multiply(inverse(C),C)))),multiply(inverse(D),D)) = multiply(inverse(multiply(inverse(E),E)),multiply(B,A)),
inference(paramod,[status(thm)],[c_2051,c_1058]) ).
cnf(c_2177,plain,
multiply(inverse(multiply(inverse(A),inverse(B))),multiply(inverse(D),D)) = multiply(inverse(multiply(inverse(E),E)),multiply(B,A)),
inference(paramod,[status(thm)],[c_2062,c_2176]) ).
cnf(c_2178,plain,
multiply(multiply(inverse(inverse(B)),A),multiply(inverse(D),D)) = multiply(inverse(multiply(inverse(E),E)),multiply(B,A)),
inference(paramod,[status(thm)],[c_2051,c_2177]) ).
cnf(c_2179,plain,
multiply(inverse(inverse(B)),A) = multiply(inverse(multiply(inverse(E),E)),multiply(B,A)),
inference(paramod,[status(thm)],[c_2062,c_2178]) ).
cnf(c_2180,plain,
multiply(inverse(inverse(B)),A) = multiply(multiply(inverse(E),E),multiply(B,A)),
inference(paramod,[status(thm)],[c_2051,c_2179]) ).
cnf(c_2063,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_2026,c_2180]) ).
cnf(c_2181,plain,
multiply(multiply(inverse(A),A),multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(D),D))))) = multiply(inverse(multiply(C,B)),multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_2051,c_1054]) ).
cnf(c_2182,plain,
multiply(multiply(inverse(A),A),multiply(inverse(B),multiply(inverse(C),multiply(inverse(D),D)))) = multiply(inverse(multiply(C,B)),multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_2051,c_2181]) ).
cnf(c_2183,plain,
multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(C))) = multiply(inverse(multiply(C,B)),multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_2062,c_2182]) ).
cnf(c_2184,plain,
multiply(inverse(B),inverse(C)) = multiply(inverse(multiply(C,B)),multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_2026,c_2183]) ).
cnf(c_2185,plain,
multiply(inverse(B),inverse(C)) = inverse(multiply(C,B)),
inference(paramod,[status(thm)],[c_2062,c_2184]) ).
cnf(c_2064,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_2185]) ).
cnf(c_2186,plain,
multiply(A,multiply(multiply(inverse(B),inverse(inverse(B))),multiply(inverse(C),C))) = multiply(A,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2064,c_943]) ).
cnf(c_2187,plain,
multiply(A,multiply(inverse(B),inverse(inverse(B)))) = multiply(A,multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_2062,c_2186]) ).
cnf(c_2073,plain,
multiply(A,multiply(inverse(B),inverse(inverse(B)))) = A,
inference(paramod,[status(thm)],[c_2062,c_2187]) ).
cnf(c_2188,plain,
multiply(inverse(multiply(multiply(inverse(A),inverse(inverse(A))),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_2064,c_834]) ).
cnf(c_2189,plain,
multiply(multiply(inverse(B),inverse(multiply(inverse(A),inverse(inverse(A))))),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_2064,c_2188]) ).
cnf(c_2190,plain,
multiply(multiply(inverse(B),multiply(inverse(inverse(inverse(A))),inverse(inverse(A)))),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_2064,c_2189]) ).
cnf(c_2191,plain,
multiply(multiply(inverse(B),multiply(inverse(A),inverse(inverse(A)))),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_2063,c_2190]) ).
cnf(c_2192,plain,
multiply(inverse(B),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_2073,c_2191]) ).
cnf(c_2193,plain,
inverse(B) = multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_2062,c_2192]) ).
cnf(c_2194,plain,
inverse(B) = multiply(multiply(inverse(B),inverse(D)),multiply(D,multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_2064,c_2193]) ).
cnf(c_2195,plain,
inverse(B) = multiply(multiply(inverse(B),inverse(D)),D),
inference(paramod,[status(thm)],[c_2062,c_2194]) ).
cnf(c_2087,plain,
multiply(multiply(inverse(A),inverse(B)),B) = inverse(A),
inference(copy,[status(thm)],[c_2195]) ).
cnf(c_2196,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,inverse(inverse(multiply(B,inverse(multiply(C,inverse(multiply(inverse(B),B))))))))) = multiply(multiply(inverse(inverse(inverse(multiply(D,C)))),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2064,c_1413]) ).
cnf(c_2197,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,inverse(inverse(multiply(B,inverse(multiply(C,multiply(inverse(B),inverse(inverse(B)))))))))) = multiply(multiply(inverse(inverse(inverse(multiply(D,C)))),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2064,c_2196]) ).
cnf(c_2198,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,inverse(inverse(multiply(B,inverse(C)))))) = multiply(multiply(inverse(inverse(inverse(multiply(D,C)))),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2073,c_2197]) ).
cnf(c_2199,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,inverse(multiply(inverse(inverse(C)),inverse(B))))) = multiply(multiply(inverse(inverse(inverse(multiply(D,C)))),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2064,c_2198]) ).
cnf(c_2200,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,inverse(multiply(C,inverse(B))))) = multiply(multiply(inverse(inverse(inverse(multiply(D,C)))),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2063,c_2199]) ).
cnf(c_2201,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,multiply(inverse(inverse(B)),inverse(C)))) = multiply(multiply(inverse(inverse(inverse(multiply(D,C)))),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2064,c_2200]) ).
cnf(c_2202,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,multiply(B,inverse(C)))) = multiply(multiply(inverse(inverse(inverse(multiply(D,C)))),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2063,c_2201]) ).
cnf(c_2203,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,multiply(B,inverse(C)))) = multiply(multiply(inverse(inverse(multiply(inverse(C),inverse(D)))),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2064,c_2202]) ).
cnf(c_2204,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,multiply(B,inverse(C)))) = multiply(multiply(inverse(multiply(inverse(inverse(D)),inverse(inverse(C)))),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2064,c_2203]) ).
cnf(c_2205,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,multiply(B,inverse(C)))) = multiply(multiply(inverse(multiply(D,inverse(inverse(C)))),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2063,c_2204]) ).
cnf(c_2206,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,multiply(B,inverse(C)))) = multiply(multiply(multiply(inverse(inverse(inverse(C))),inverse(D)),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2064,c_2205]) ).
cnf(c_2207,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,multiply(B,inverse(C)))) = multiply(multiply(multiply(inverse(C),inverse(D)),D),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2063,c_2206]) ).
cnf(c_2208,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,multiply(B,inverse(C)))) = multiply(inverse(C),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_2087,c_2207]) ).
cnf(c_2209,plain,
multiply(multiply(inverse(B),inverse(A)),multiply(A,multiply(B,inverse(C)))) = multiply(inverse(C),multiply(inverse(D),inverse(inverse(D)))),
inference(paramod,[status(thm)],[c_2064,c_2208]) ).
cnf(c_2101,plain,
multiply(multiply(inverse(A),inverse(B)),multiply(B,multiply(A,inverse(C)))) = inverse(C),
inference(paramod,[status(thm)],[c_2073,c_2209]) ).
cnf(c_2210,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(multiply(inverse(C),B),multiply(inverse(B),inverse(inverse(B)))))))),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2064,c_1279]) ).
cnf(c_2211,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(inverse(C),B))))),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2073,c_2210]) ).
cnf(c_2212,plain,
multiply(inverse(multiply(A,multiply(B,multiply(inverse(B),inverse(inverse(C)))))),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2211]) ).
cnf(c_2213,plain,
multiply(inverse(multiply(A,inverse(inverse(C)))),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2052,c_2212]) ).
cnf(c_2214,plain,
multiply(multiply(inverse(inverse(inverse(C))),inverse(A)),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2213]) ).
cnf(c_2215,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2063,c_2214]) ).
cnf(c_2216,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(multiply(inverse(C),B),multiply(inverse(B),inverse(inverse(B)))))),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2215]) ).
cnf(c_2217,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(multiply(B,inverse(multiply(inverse(C),B))),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2073,c_2216]) ).
cnf(c_2218,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(multiply(B,multiply(inverse(B),inverse(inverse(C)))),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2217]) ).
cnf(c_2219,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(inverse(inverse(C)),E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2052,c_2218]) ).
cnf(c_2220,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(C,E),inverse(multiply(inverse(E),E))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2063,c_2219]) ).
cnf(c_2221,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(multiply(C,E),multiply(inverse(E),inverse(inverse(E)))))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2220]) ).
cnf(c_2222,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(multiply(multiply(E,inverse(multiply(C,E))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2073,c_2221]) ).
cnf(c_2223,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(multiply(multiply(E,multiply(inverse(E),inverse(C))),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2222]) ).
cnf(c_2224,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(multiply(inverse(C),multiply(B,inverse(multiply(multiply(inverse(C),B),inverse(multiply(inverse(B),B)))))))))))))) = D,
inference(paramod,[status(thm)],[c_2052,c_2223]) ).
cnf(c_2225,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(multiply(inverse(C),multiply(B,inverse(multiply(multiply(inverse(C),B),multiply(inverse(B),inverse(inverse(B))))))))))))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2224]) ).
cnf(c_2226,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(multiply(inverse(C),multiply(B,inverse(multiply(inverse(C),B)))))))))))) = D,
inference(paramod,[status(thm)],[c_2073,c_2225]) ).
cnf(c_2227,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(multiply(inverse(C),multiply(B,multiply(inverse(B),inverse(inverse(C))))))))))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2226]) ).
cnf(c_2228,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(multiply(inverse(C),inverse(inverse(C))))))))))) = D,
inference(paramod,[status(thm)],[c_2052,c_2227]) ).
cnf(c_2229,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),multiply(inverse(inverse(inverse(C))),inverse(inverse(C)))))))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2228]) ).
cnf(c_2230,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),multiply(inverse(C),inverse(inverse(C)))))))))) = D,
inference(paramod,[status(thm)],[c_2063,c_2229]) ).
cnf(c_2231,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(inverse(inverse(C)),inverse(inverse(D))))))) = D,
inference(paramod,[status(thm)],[c_2073,c_2230]) ).
cnf(c_2232,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(inverse(multiply(C,inverse(inverse(D))))))) = D,
inference(paramod,[status(thm)],[c_2063,c_2231]) ).
cnf(c_2233,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(multiply(inverse(inverse(inverse(D))),inverse(C))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2232]) ).
cnf(c_2234,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,inverse(multiply(inverse(D),inverse(C))))) = D,
inference(paramod,[status(thm)],[c_2063,c_2233]) ).
cnf(c_2235,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,multiply(inverse(inverse(C)),inverse(inverse(D))))) = D,
inference(paramod,[status(thm)],[c_2064,c_2234]) ).
cnf(c_2236,plain,
multiply(multiply(inverse(C),inverse(A)),multiply(A,multiply(C,inverse(inverse(D))))) = D,
inference(paramod,[status(thm)],[c_2063,c_2235]) ).
cnf(c_2103,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_2101,c_2236]) ).
cnf(c_2237,plain,
multiply(multiply(A,B),inverse(inverse(inverse(multiply(multiply(C,inverse(multiply(multiply(inverse(inverse(D)),C),inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(B),B))))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2103,c_2000]) ).
cnf(c_2238,plain,
multiply(multiply(A,B),inverse(inverse(inverse(multiply(multiply(C,inverse(multiply(multiply(D,C),inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(B),B))))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2103,c_2237]) ).
cnf(c_2239,plain,
multiply(multiply(A,B),inverse(inverse(inverse(multiply(multiply(C,inverse(multiply(multiply(D,C),multiply(inverse(C),inverse(inverse(C)))))),inverse(multiply(inverse(B),B))))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2064,c_2238]) ).
cnf(c_2240,plain,
multiply(multiply(A,B),inverse(inverse(inverse(multiply(multiply(C,inverse(multiply(multiply(D,C),multiply(inverse(C),C)))),inverse(multiply(inverse(B),B))))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2103,c_2239]) ).
cnf(c_2241,plain,
multiply(multiply(A,B),inverse(inverse(inverse(multiply(multiply(C,inverse(multiply(D,C))),inverse(multiply(inverse(B),B))))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2062,c_2240]) ).
cnf(c_2242,plain,
multiply(multiply(A,B),inverse(inverse(inverse(multiply(multiply(C,multiply(inverse(C),inverse(D))),inverse(multiply(inverse(B),B))))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2064,c_2241]) ).
cnf(c_2243,plain,
multiply(multiply(A,B),inverse(inverse(inverse(multiply(inverse(D),inverse(multiply(inverse(B),B))))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2052,c_2242]) ).
cnf(c_2244,plain,
multiply(multiply(A,B),inverse(inverse(inverse(multiply(inverse(D),multiply(inverse(B),inverse(inverse(B)))))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2064,c_2243]) ).
cnf(c_2245,plain,
multiply(multiply(A,B),inverse(inverse(inverse(multiply(inverse(D),multiply(inverse(B),B)))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2103,c_2244]) ).
cnf(c_2246,plain,
multiply(multiply(A,B),inverse(inverse(inverse(inverse(D))))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2062,c_2245]) ).
cnf(c_2247,plain,
multiply(multiply(A,B),inverse(inverse(D))) = multiply(A,multiply(B,D)),
inference(paramod,[status(thm)],[c_2103,c_2246]) ).
cnf(c_2115,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_2103,c_2247]) ).
cnf(c_2116,plain,
$false,
inference(resolve,[status(thm)],[c_2115,c_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP417-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.54 % Computer : n017.cluster.edu
% 0.10/0.54 % Model : x86_64 x86_64
% 0.10/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.54 % Memory : 8046.5625MB
% 0.10/0.54 % OS : Linux 6.8.0-71-generic
% 0.10/0.54 % CPULimit : 300
% 0.10/0.54 % WCLimit : 300
% 0.10/0.54 % DateTime : Fri Sep 25 14:48:03 UTC 2026
% 0.10/0.54 % CPUTime :
% 0.10/0.55 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.55 % Process 2556664 was started by sandbox on n017,
% 0.10/0.55 % Fri Sep 25 14:48:03 2026
% 0.10/0.55 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.55
% 0.10/0.55 % From the command line: assign(max_seconds, 300).
% 3.81/1.05
% 3.81/1.05 % SZS status Unsatisfiable for theBenchmark
% 3.81/1.05
% 3.81/1.05 % Proof 1 at 0.44 (+ 0.06) seconds.
% 3.81/1.05 % Length of proof is 93.
% 3.81/1.05 % Level of proof is 27.
% 3.81/1.05 % Maximum clause weight is 99.000.
% 3.81/1.05 % Given clauses 41.
% 3.81/1.05
% 3.81/1.05 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------