%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP411-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:08 AM UTC 2026
% Result : Unsatisfiable 19.14s 2.83s
% Output : CNFRefutation 19.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 2
% Syntax : Number of formulae : 261 ( 261 unt; 0 def)
% Number of atoms : 261 ( 260 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 : 16 ( 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 : 987 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(inverse(multiply(VAR_0,inverse(multiply(VAR_1,VAR_2)))),multiply(VAR_0,inverse(VAR_2))),inverse(multiply(inverse(VAR_2),VAR_2))) = VAR_1,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C))),inverse(multiply(inverse(C),C))) = B,
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_4074,plain,
multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))) = multiply(inverse(multiply(D,inverse(multiply(B,C)))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_3,plain,
multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C))) = multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),
inference(copy,[status(thm)],[c_4074]) ).
cnf(c_4,plain,
multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(B,inverse(multiply(A,C)))),multiply(B,inverse(C))),inverse(C))),inverse(multiply(inverse(C),C))) = inverse(C),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_5,plain,
multiply(multiply(inverse(multiply(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),B),inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(C),C)))) = D,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_4075,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(inverse(multiply(inverse(D),D))))),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D)))))))),multiply(A,inverse(multiply(E,inverse(D))))),inverse(multiply(inverse(multiply(E,inverse(D))),multiply(E,inverse(D))))) = inverse(multiply(E,inverse(multiply(C,D)))),
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_6,plain,
inverse(multiply(A,inverse(multiply(B,C)))) = multiply(multiply(inverse(multiply(D,inverse(multiply(multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))))),multiply(D,inverse(multiply(A,inverse(C))))),inverse(multiply(inverse(multiply(A,inverse(C))),multiply(A,inverse(C))))),
inference(copy,[status(thm)],[c_4075]) ).
cnf(c_7,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(C),C))) = B,
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_8,plain,
multiply(multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C)))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(C),C))))),inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))) = inverse(inverse(multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_9,plain,
multiply(inverse(multiply(A,inverse(multiply(multiply(B,inverse(multiply(inverse(C),C))),C)))),multiply(A,inverse(C))) = B,
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_10,plain,
multiply(inverse(A),multiply(multiply(inverse(multiply(B,inverse(multiply(A,C)))),multiply(B,inverse(C))),inverse(C))) = multiply(multiply(inverse(multiply(D,inverse(inverse(C)))),multiply(D,inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_13,plain,
multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C))) = multiply(inverse(multiply(D,inverse(multiply(B,C)))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_3,c_3]) ).
cnf(c_14,plain,
multiply(multiply(inverse(inverse(A)),multiply(multiply(inverse(B),multiply(multiply(inverse(multiply(C,inverse(multiply(B,A)))),multiply(C,inverse(A))),inverse(A))),inverse(A))),inverse(multiply(inverse(A),A))) = inverse(A),
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_15,plain,
multiply(multiply(inverse(multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(B,inverse(multiply(A,C)))),multiply(B,inverse(C))),inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),inverse(C)),inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(C),C)))) = D,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_18,plain,
multiply(multiply(inverse(A),multiply(multiply(multiply(inverse(multiply(B,inverse(A))),multiply(B,inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),inverse(C))),inverse(multiply(inverse(C),C))) = inverse(C),
inference(paramod,[status(thm)],[c_3,c_4]) ).
cnf(c_20,plain,
multiply(multiply(inverse(multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),inverse(multiply(D,multiply(inverse(C),C))))),B),inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(C),C)))) = D,
inference(paramod,[status(thm)],[c_3,c_5]) ).
cnf(c_4076,plain,
multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D))))),inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(D))))) = inverse(multiply(C,inverse(multiply(multiply(B,inverse(multiply(inverse(D),D))),D)))),
inference(paramod,[status(thm)],[c_9,c_1]) ).
cnf(c_33,plain,
inverse(multiply(A,inverse(multiply(multiply(B,inverse(multiply(inverse(C),C))),C)))) = multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(multiply(A,inverse(C))))),inverse(multiply(inverse(multiply(A,inverse(C))),multiply(A,inverse(C))))),
inference(copy,[status(thm)],[c_4076]) ).
cnf(c_4077,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D))))) = multiply(inverse(multiply(E,inverse(multiply(inverse(multiply(C,inverse(multiply(multiply(B,inverse(multiply(inverse(D),D))),D)))),multiply(C,inverse(D)))))),multiply(E,inverse(multiply(C,inverse(D))))),
inference(paramod,[status(thm)],[c_9,c_13]) ).
cnf(c_38,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D))))) = multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(multiply(C,inverse(D))))),
inference(paramod,[status(thm)],[c_9,c_4077]) ).
cnf(c_4078,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(multiply(multiply(inverse(multiply(E,inverse(multiply(C,F)))),multiply(E,inverse(F))),inverse(multiply(inverse(F),F)))))),
inference(paramod,[status(thm)],[c_1,c_38]) ).
cnf(c_42,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_1,c_4078]) ).
cnf(c_46,plain,
multiply(inverse(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C))))),inverse(D))),multiply(inverse(multiply(E,inverse(multiply(B,C)))),multiply(E,inverse(C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),
inference(paramod,[status(thm)],[c_3,c_38]) ).
cnf(c_4079,plain,
multiply(inverse(A),multiply(multiply(inverse(multiply(B,inverse(multiply(A,C)))),multiply(B,inverse(C))),inverse(D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(C),C)))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_1,c_42]) ).
cnf(c_55,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(C))) = multiply(inverse(D),multiply(multiply(inverse(multiply(E,inverse(multiply(D,B)))),multiply(E,inverse(B))),inverse(C))),
inference(copy,[status(thm)],[c_4079]) ).
cnf(c_57,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C)))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(C),C))))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_3,c_42]) ).
cnf(c_61,plain,
multiply(inverse(multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(B,inverse(multiply(A,C)))),multiply(B,inverse(C))),inverse(C))),inverse(D))),inverse(C)) = multiply(inverse(multiply(E,inverse(D))),multiply(E,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_4,c_42]) ).
cnf(c_65,plain,
multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),B),inverse(E))),D) = multiply(inverse(multiply(F,inverse(E))),multiply(F,inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_5,c_42]) ).
cnf(c_71,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(multiply(inverse(B),B)))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_1,c_55]) ).
cnf(c_4080,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(multiply(multiply(inverse(multiply(B,inverse(multiply(C,inverse(multiply(inverse(D),D)))))),multiply(B,inverse(inverse(multiply(inverse(D),D))))),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D)))))))),multiply(A,inverse(multiply(E,inverse(D))))),inverse(multiply(inverse(multiply(E,inverse(D))),multiply(E,inverse(D))))),multiply(E,inverse(D))) = C,
inference(paramod,[status(thm)],[c_6,c_9]) ).
cnf(c_88,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D))))),inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(D))))),multiply(C,inverse(D))) = B,
inference(paramod,[status(thm)],[c_1,c_4080]) ).
cnf(c_4081,plain,
multiply(inverse(A),multiply(multiply(inverse(multiply(B,inverse(multiply(A,C)))),multiply(B,inverse(C))),inverse(multiply(inverse(C),C)))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_1,c_71]) ).
cnf(c_109,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_1,c_4081]) ).
cnf(c_165,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C))),inverse(multiply(inverse(D),D))) = B,
inference(paramod,[status(thm)],[c_109,c_1]) ).
cnf(c_169,plain,
multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C))) = multiply(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_109,c_3]) ).
cnf(c_172,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),B)),B)))),multiply(A,inverse(B))) = multiply(multiply(inverse(C),C),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_109,c_3]) ).
cnf(c_191,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_109,c_42]) ).
cnf(c_206,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(D),D))) = B,
inference(paramod,[status(thm)],[c_109,c_7]) ).
cnf(c_216,plain,
multiply(multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C)))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(C),C))))),inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(E),E))) = inverse(inverse(multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_109,c_8]) ).
cnf(c_4082,plain,
multiply(multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C)))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(C),C))))),inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))) = inverse(inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_109,c_8]) ).
cnf(c_217,plain,
inverse(inverse(multiply(inverse(A),A))) = inverse(inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_216,c_4082]) ).
cnf(c_220,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_217,c_109]) ).
cnf(c_231,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(C))),inverse(multiply(inverse(D),D))) = inverse(C),
inference(paramod,[status(thm)],[c_109,c_165]) ).
cnf(c_242,plain,
multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(B,inverse(multiply(A,C)))),multiply(B,inverse(C))),inverse(D))),inverse(multiply(inverse(E),E))) = inverse(D),
inference(paramod,[status(thm)],[c_165,c_165]) ).
cnf(c_249,plain,
multiply(inverse(A),multiply(multiply(inverse(multiply(B,inverse(multiply(A,C)))),multiply(B,inverse(C))),inverse(C))) = multiply(multiply(inverse(multiply(D,inverse(inverse(C)))),multiply(D,inverse(inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_109,c_10]) ).
cnf(c_266,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(B),multiply(multiply(inverse(multiply(C,inverse(multiply(B,D)))),multiply(C,inverse(D))),inverse(A))),inverse(A))) = multiply(multiply(inverse(multiply(E,inverse(inverse(A)))),multiply(E,inverse(inverse(multiply(inverse(A),A))))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))),
inference(paramod,[status(thm)],[c_165,c_10]) ).
cnf(c_287,plain,
multiply(multiply(inverse(inverse(A)),multiply(multiply(inverse(B),multiply(multiply(inverse(multiply(C,inverse(multiply(B,A)))),multiply(C,inverse(A))),inverse(A))),inverse(A))),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),E))))) = inverse(A),
inference(paramod,[status(thm)],[c_220,c_14]) ).
cnf(c_292,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_191,c_109]) ).
cnf(c_4083,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_220,c_191]) ).
cnf(c_307,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(D),D)))) = multiply(inverse(multiply(inverse(E),E)),multiply(inverse(inverse(B)),inverse(A))),
inference(copy,[status(thm)],[c_4083]) ).
cnf(c_315,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_109,c_292]) ).
cnf(c_4084,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(multiply(inverse(inverse(C)),inverse(C))))),inverse(multiply(inverse(D),D))) = inverse(multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_292,c_165]) ).
cnf(c_319,plain,
inverse(multiply(inverse(inverse(A)),inverse(A))) = inverse(multiply(inverse(B),B)),
inference(paramod,[status(thm)],[c_231,c_4084]) ).
cnf(c_331,plain,
inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(B),B)),
inference(paramod,[status(thm)],[c_109,c_319]) ).
cnf(c_357,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_331,c_331]) ).
cnf(c_379,plain,
multiply(multiply(inverse(multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(B,inverse(multiply(A,C)))),multiply(B,inverse(C))),inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),inverse(C)),inverse(multiply(inverse(E),E))) = D,
inference(paramod,[status(thm)],[c_109,c_15]) ).
cnf(c_4085,plain,
multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(multiply(inverse(B),multiply(multiply(inverse(multiply(C,inverse(multiply(B,D)))),multiply(C,inverse(D))),inverse(D))),inverse(multiply(A,multiply(inverse(D),D))))),inverse(D)),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(E),E))) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_15,c_165]) ).
cnf(c_4086,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(E),E))) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_379,c_4085]) ).
cnf(c_391,plain,
inverse(multiply(inverse(A),A)) = multiply(multiply(inverse(B),B),inverse(multiply(inverse(C),C))),
inference(copy,[status(thm)],[c_4086]) ).
cnf(c_4087,plain,
multiply(multiply(inverse(A),multiply(multiply(multiply(inverse(multiply(B,inverse(A))),multiply(B,inverse(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(C))),multiply(inverse(inverse(C)),inverse(C))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(C))),multiply(inverse(inverse(C)),inverse(C))))),inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(C))),multiply(inverse(inverse(C)),inverse(C))))))),inverse(multiply(inverse(inverse(C)),inverse(C))))),inverse(multiply(inverse(multiply(D,inverse(C))),multiply(D,inverse(C))))) = inverse(multiply(inverse(inverse(C)),inverse(C))),
inference(paramod,[status(thm)],[c_191,c_18]) ).
cnf(c_430,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(C))))) = inverse(multiply(inverse(inverse(C)),inverse(C))),
inference(paramod,[status(thm)],[c_206,c_4087]) ).
cnf(c_4088,plain,
multiply(multiply(inverse(A),multiply(multiply(multiply(inverse(multiply(B,inverse(A))),multiply(B,inverse(inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(C),C)))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(C),C)))),inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(C),C)))))),inverse(multiply(inverse(C),C)))),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(C),C)))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_331,c_18]) ).
cnf(c_431,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C)))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_206,c_4088]) ).
cnf(c_441,plain,
multiply(multiply(inverse(multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D))))),inverse(multiply(E,multiply(inverse(D),D))))),B),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(D),D)))) = E,
inference(paramod,[status(thm)],[c_109,c_20]) ).
cnf(c_453,plain,
multiply(multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),inverse(multiply(D,multiply(inverse(C),C))))),inverse(multiply(inverse(C),C))),inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(C),C)))) = D,
inference(paramod,[status(thm)],[c_315,c_20]) ).
cnf(c_468,plain,
multiply(inverse(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(C),C))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_391,c_220]) ).
cnf(c_529,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))) = inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_331,c_357]) ).
cnf(c_777,plain,
inverse(multiply(A,inverse(multiply(multiply(B,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(D),D))))),E)))) = multiply(multiply(inverse(multiply(F,inverse(B))),multiply(F,inverse(multiply(A,inverse(E))))),inverse(multiply(inverse(multiply(A,inverse(E))),multiply(A,inverse(E))))),
inference(paramod,[status(thm)],[c_220,c_33]) ).
cnf(c_4089,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),B)),C)))) = multiply(multiply(inverse(multiply(D,inverse(multiply(inverse(E),E)))),multiply(D,inverse(multiply(A,inverse(C))))),inverse(multiply(inverse(multiply(A,inverse(C))),multiply(A,inverse(C))))),
inference(paramod,[status(thm)],[c_391,c_33]) ).
cnf(c_835,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),B)),C)))) = inverse(multiply(A,inverse(C))),
inference(paramod,[status(thm)],[c_231,c_4089]) ).
cnf(c_863,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(B))) = multiply(multiply(inverse(C),C),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_835,c_172]) ).
cnf(c_917,plain,
inverse(multiply(A,inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(D)))))) = inverse(multiply(A,inverse(multiply(inverse(inverse(C)),inverse(D))))),
inference(paramod,[status(thm)],[c_42,c_835]) ).
cnf(c_938,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(multiply(inverse(multiply(inverse(B),B)),C))),inverse(D))) = multiply(inverse(multiply(E,inverse(C))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_835,c_191]) ).
cnf(c_1209,plain,
multiply(inverse(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C))))),inverse(D))),multiply(inverse(multiply(E,inverse(multiply(B,C)))),multiply(E,inverse(C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7))))),
inference(paramod,[status(thm)],[c_315,c_46]) ).
cnf(c_1242,plain,
multiply(inverse(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C))))),inverse(D))),multiply(inverse(multiply(E,inverse(multiply(multiply(inverse(multiply(inverse(F),F)),B),C)))),multiply(E,inverse(C)))) = multiply(inverse(multiply(V6,inverse(D))),multiply(V6,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),
inference(paramod,[status(thm)],[c_835,c_46]) ).
cnf(c_1272,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C)))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(C),C))))),inverse(E))) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(multiply(inverse(V6),V6))),inverse(E))),
inference(paramod,[status(thm)],[c_220,c_57]) ).
cnf(c_1278,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C)))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(C),C))))),inverse(E))) = multiply(inverse(F),multiply(multiply(inverse(multiply(V6,inverse(multiply(F,V7)))),multiply(V6,inverse(V7))),inverse(E))),
inference(paramod,[status(thm)],[c_165,c_57]) ).
cnf(c_1289,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C)))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(F),F)))))),inverse(V6))) = multiply(inverse(multiply(V7,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),multiply(V7,inverse(V6))),
inference(paramod,[status(thm)],[c_315,c_57]) ).
cnf(c_4090,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),B)),B)))),multiply(A,inverse(B)))),multiply(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),D)),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_315,c_57]) ).
cnf(c_1290,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(B)))),multiply(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),D)),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_835,c_4090]) ).
cnf(c_1735,plain,
multiply(inverse(multiply(multiply(inverse(inverse(A)),multiply(multiply(inverse(B),multiply(multiply(inverse(multiply(C,inverse(multiply(B,D)))),multiply(C,inverse(D))),inverse(A))),inverse(A))),inverse(E))),inverse(A)) = multiply(inverse(multiply(F,inverse(E))),multiply(F,inverse(multiply(inverse(A),A)))),
inference(paramod,[status(thm)],[c_165,c_61]) ).
cnf(c_4091,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(D),D)))))))),multiply(A,inverse(E))),inverse(multiply(inverse(F),F))) = inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(V6,inverse(multiply(V7,D)))),multiply(V6,inverse(D))),inverse(multiply(E,multiply(inverse(D),D))))),V7),inverse(C))),
inference(paramod,[status(thm)],[c_65,c_165]) ).
cnf(c_4092,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(D),D))))))),multiply(A,inverse(E))),inverse(multiply(inverse(F),F))) = inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(V6,inverse(multiply(V7,D)))),multiply(V6,inverse(D))),inverse(multiply(E,multiply(inverse(D),D))))),V7),inverse(C))),
inference(paramod,[status(thm)],[c_917,c_4091]) ).
cnf(c_4093,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),D)))))),multiply(A,inverse(E))),inverse(multiply(inverse(F),F))) = inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(V6,inverse(multiply(V7,D)))),multiply(V6,inverse(D))),inverse(multiply(E,multiply(inverse(D),D))))),V7),inverse(C))),
inference(paramod,[status(thm)],[c_835,c_4092]) ).
cnf(c_1816,plain,
inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),B),inverse(E))) = multiply(multiply(inverse(multiply(F,inverse(multiply(inverse(inverse(E)),inverse(multiply(inverse(C),C)))))),multiply(F,inverse(D))),inverse(multiply(inverse(V6),V6))),
inference(copy,[status(thm)],[c_4093]) ).
cnf(c_1818,plain,
multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(A),multiply(multiply(inverse(multiply(B,inverse(multiply(A,C)))),multiply(B,inverse(C))),inverse(D))),inverse(multiply(E,multiply(inverse(D),D))))),inverse(D)),inverse(F))),E) = multiply(inverse(multiply(V6,inverse(F))),multiply(V6,inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_165,c_65]) ).
cnf(c_2873,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),D)))))),multiply(A,inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(F),F))))),inverse(multiply(inverse(V6),V6))) = B,
inference(paramod,[status(thm)],[c_529,c_165]) ).
cnf(c_4094,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(C))))),multiply(B,inverse(C))) = multiply(B,inverse(C)),
inference(paramod,[status(thm)],[c_109,c_88]) ).
cnf(c_2983,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(A))),multiply(B,inverse(A))) = multiply(B,inverse(A)),
inference(paramod,[status(thm)],[c_430,c_4094]) ).
cnf(c_4095,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))),inverse(multiply(inverse(multiply(multiply(inverse(multiply(D,inverse(multiply(C,E)))),multiply(D,inverse(E))),inverse(multiply(inverse(F),F)))),multiply(multiply(inverse(multiply(D,inverse(multiply(C,E)))),multiply(D,inverse(E))),inverse(multiply(inverse(F),F)))))),multiply(multiply(inverse(multiply(D,inverse(multiply(C,E)))),multiply(D,inverse(E))),inverse(multiply(inverse(F),F)))) = B,
inference(paramod,[status(thm)],[c_165,c_88]) ).
cnf(c_4096,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))),inverse(multiply(inverse(C),multiply(multiply(inverse(multiply(D,inverse(multiply(C,E)))),multiply(D,inverse(E))),inverse(multiply(inverse(F),F)))))),multiply(multiply(inverse(multiply(D,inverse(multiply(C,E)))),multiply(D,inverse(E))),inverse(multiply(inverse(F),F)))) = B,
inference(paramod,[status(thm)],[c_165,c_4095]) ).
cnf(c_4097,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))),inverse(multiply(inverse(C),C))),multiply(multiply(inverse(multiply(D,inverse(multiply(C,E)))),multiply(D,inverse(E))),inverse(multiply(inverse(F),F)))) = B,
inference(paramod,[status(thm)],[c_165,c_4096]) ).
cnf(c_3005,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))),inverse(multiply(inverse(C),C))),C) = B,
inference(paramod,[status(thm)],[c_165,c_4097]) ).
cnf(c_4098,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),D))))),inverse(multiply(inverse(multiply(inverse(inverse(E)),inverse(E))),multiply(inverse(inverse(E)),inverse(E))))),multiply(inverse(inverse(E)),inverse(E))) = B,
inference(paramod,[status(thm)],[c_315,c_88]) ).
cnf(c_3014,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),D))))),inverse(multiply(inverse(inverse(E)),inverse(E)))),multiply(inverse(inverse(E)),inverse(E))) = B,
inference(paramod,[status(thm)],[c_2983,c_4098]) ).
cnf(c_4099,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(inverse(C)),inverse(C))))),inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(C))),multiply(inverse(inverse(C)),inverse(C))))),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))) = B,
inference(paramod,[status(thm)],[c_315,c_88]) ).
cnf(c_3019,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(inverse(C)),inverse(C))))),inverse(multiply(inverse(inverse(C)),inverse(C)))),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))) = B,
inference(paramod,[status(thm)],[c_2983,c_4099]) ).
cnf(c_4100,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D))))),inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(D))))),multiply(C,inverse(D))) = multiply(inverse(multiply(inverse(E),E)),B),
inference(paramod,[status(thm)],[c_835,c_88]) ).
cnf(c_4101,plain,
B = multiply(inverse(multiply(inverse(E),E)),B),
inference(paramod,[status(thm)],[c_3005,c_4100]) ).
cnf(c_3050,plain,
multiply(inverse(multiply(inverse(A),A)),B) = B,
inference(copy,[status(thm)],[c_4101]) ).
cnf(c_4102,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(C),C),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(E),E)))))),inverse(multiply(inverse(multiply(inverse(inverse(F)),inverse(F))),multiply(inverse(inverse(F)),inverse(F))))),multiply(inverse(inverse(F)),inverse(F))) = B,
inference(paramod,[status(thm)],[c_468,c_88]) ).
cnf(c_3081,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(C),C),inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(E),E)))))),inverse(multiply(inverse(inverse(F)),inverse(F)))),multiply(inverse(inverse(F)),inverse(F))) = B,
inference(paramod,[status(thm)],[c_3050,c_4102]) ).
cnf(c_4103,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(B)))),multiply(multiply(inverse(D),D),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_3050,c_1290]) ).
cnf(c_4104,plain,
multiply(multiply(inverse(D),D),inverse(E)) = multiply(inverse(multiply(F,inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_3050,c_4103]) ).
cnf(c_3159,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))))),multiply(A,inverse(C))) = multiply(multiply(inverse(D),D),inverse(C)),
inference(copy,[status(thm)],[c_4104]) ).
cnf(c_4105,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C)))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(C),C))))),inverse(E))) = multiply(inverse(inverse(multiply(inverse(V6),V6))),inverse(E)),
inference(paramod,[status(thm)],[c_3050,c_1272]) ).
cnf(c_3161,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(B)) = multiply(inverse(multiply(inverse(multiply(C,inverse(multiply(D,E)))),multiply(C,inverse(E)))),multiply(multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(inverse(multiply(inverse(E),E))))),inverse(B))),
inference(copy,[status(thm)],[c_4105]) ).
cnf(c_4106,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(C)),inverse(D))) = multiply(inverse(multiply(E,inverse(C))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_3050,c_938]) ).
cnf(c_4107,plain,
multiply(inverse(inverse(C)),inverse(D)) = multiply(inverse(multiply(E,inverse(C))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_3050,c_4106]) ).
cnf(c_3183,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))) = multiply(inverse(inverse(B)),inverse(C)),
inference(copy,[status(thm)],[c_4107]) ).
cnf(c_3211,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(D),D)))) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_3050,c_307]) ).
cnf(c_4108,plain,
multiply(inverse(inverse(multiply(B,C))),inverse(C)) = multiply(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_3183,c_169]) ).
cnf(c_3224,plain,
multiply(inverse(inverse(multiply(A,B))),inverse(B)) = multiply(multiply(inverse(inverse(A)),inverse(inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_3050,c_4108]) ).
cnf(c_4109,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(D),D)))),inverse(multiply(inverse(inverse(E)),inverse(E)))),multiply(inverse(inverse(E)),inverse(E))) = B,
inference(paramod,[status(thm)],[c_3050,c_3014]) ).
cnf(c_3230,plain,
multiply(multiply(multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B))),inverse(multiply(inverse(inverse(C)),inverse(C)))),multiply(inverse(inverse(C)),inverse(C))) = A,
inference(paramod,[status(thm)],[c_3183,c_4109]) ).
cnf(c_4110,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(D),D))))),multiply(A,inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(F),F))))),inverse(multiply(inverse(V6),V6))) = B,
inference(paramod,[status(thm)],[c_3050,c_2873]) ).
cnf(c_4111,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(D),D))))),multiply(A,inverse(multiply(inverse(F),F)))),inverse(multiply(inverse(V6),V6))) = B,
inference(paramod,[status(thm)],[c_3050,c_4110]) ).
cnf(c_3231,plain,
multiply(multiply(inverse(inverse(multiply(A,multiply(inverse(B),B)))),inverse(multiply(inverse(C),C))),inverse(multiply(inverse(D),D))) = A,
inference(paramod,[status(thm)],[c_3183,c_4111]) ).
cnf(c_4112,plain,
multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(A),multiply(multiply(inverse(inverse(multiply(A,C))),inverse(C)),inverse(D))),inverse(multiply(E,multiply(inverse(D),D))))),inverse(D)),inverse(F))),E) = multiply(inverse(multiply(V6,inverse(F))),multiply(V6,inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_3183,c_1818]) ).
cnf(c_4113,plain,
multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(A),multiply(multiply(inverse(inverse(multiply(A,C))),inverse(C)),inverse(D))),inverse(multiply(E,multiply(inverse(D),D))))),inverse(D)),inverse(F))),E) = multiply(inverse(multiply(V6,inverse(F))),multiply(V6,inverse(multiply(inverse(D),D)))),
inference(paramod,[status(thm)],[c_3050,c_4112]) ).
cnf(c_3253,plain,
multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(A),multiply(multiply(inverse(inverse(multiply(A,B))),inverse(B)),inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),inverse(C)),inverse(E))),D) = multiply(inverse(inverse(E)),inverse(multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_3183,c_4113]) ).
cnf(c_4114,plain,
multiply(inverse(multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C)))),inverse(D))),multiply(inverse(multiply(E,inverse(multiply(B,C)))),multiply(E,inverse(C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7))))),
inference(paramod,[status(thm)],[c_3183,c_1209]) ).
cnf(c_4115,plain,
multiply(inverse(multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C)))),inverse(D))),multiply(inverse(inverse(multiply(B,C))),inverse(C))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7))))),
inference(paramod,[status(thm)],[c_3183,c_4114]) ).
cnf(c_4116,plain,
multiply(inverse(multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C)))),inverse(D))),multiply(inverse(inverse(multiply(B,C))),inverse(C))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(V7),V7)))),
inference(paramod,[status(thm)],[c_3050,c_4115]) ).
cnf(c_4117,plain,
multiply(inverse(multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C)))),inverse(D))),multiply(inverse(inverse(multiply(B,C))),inverse(C))) = multiply(inverse(inverse(D)),inverse(multiply(inverse(V7),V7))),
inference(paramod,[status(thm)],[c_3183,c_4116]) ).
cnf(c_3268,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B))) = multiply(inverse(multiply(multiply(inverse(inverse(C)),inverse(inverse(multiply(inverse(D),D)))),inverse(A))),multiply(inverse(inverse(multiply(C,D))),inverse(D))),
inference(copy,[status(thm)],[c_4117]) ).
cnf(c_4118,plain,
multiply(multiply(inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),inverse(multiply(D,multiply(inverse(C),C))))),inverse(multiply(inverse(C),C))),inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(C),C)))) = D,
inference(paramod,[status(thm)],[c_3050,c_453]) ).
cnf(c_3289,plain,
multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),inverse(multiply(C,multiply(inverse(B),B))))),inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))) = C,
inference(paramod,[status(thm)],[c_3050,c_4118]) ).
cnf(c_4119,plain,
multiply(multiply(inverse(multiply(multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C)))),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D))))),inverse(multiply(E,multiply(inverse(D),D))))),B),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(D),D)))) = E,
inference(paramod,[status(thm)],[c_3183,c_441]) ).
cnf(c_3292,plain,
multiply(multiply(inverse(multiply(multiply(multiply(inverse(inverse(A)),inverse(inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),inverse(multiply(D,multiply(inverse(C),C))))),A),inverse(multiply(inverse(C),C))) = D,
inference(paramod,[status(thm)],[c_3050,c_4119]) ).
cnf(c_3293,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))) = inverse(multiply(inverse(B),B)),
inference(paramod,[status(thm)],[c_3050,c_431]) ).
cnf(c_4120,plain,
multiply(multiply(multiply(inverse(inverse(B)),inverse(multiply(inverse(inverse(C)),inverse(C)))),inverse(multiply(inverse(inverse(C)),inverse(C)))),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))) = B,
inference(paramod,[status(thm)],[c_3183,c_3019]) ).
cnf(c_3302,plain,
multiply(multiply(multiply(inverse(inverse(A)),inverse(multiply(inverse(inverse(B)),inverse(B)))),inverse(multiply(inverse(inverse(B)),inverse(B)))),multiply(inverse(C),C)) = A,
inference(paramod,[status(thm)],[c_3050,c_4120]) ).
cnf(c_4121,plain,
multiply(inverse(multiply(inverse(inverse(multiply(B,C))),inverse(C))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(F),F)))))),inverse(V6))) = multiply(inverse(multiply(V7,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),multiply(V7,inverse(V6))),
inference(paramod,[status(thm)],[c_3183,c_1289]) ).
cnf(c_4122,plain,
multiply(inverse(multiply(inverse(inverse(multiply(B,C))),inverse(C))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(F),F))))),inverse(V6))) = multiply(inverse(multiply(V7,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),multiply(V7,inverse(V6))),
inference(paramod,[status(thm)],[c_3050,c_4121]) ).
cnf(c_4123,plain,
multiply(inverse(multiply(inverse(inverse(multiply(B,C))),inverse(C))),multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(F),F)))),inverse(V6))) = multiply(inverse(multiply(V7,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),multiply(V7,inverse(V6))),
inference(paramod,[status(thm)],[c_3183,c_4122]) ).
cnf(c_4124,plain,
multiply(inverse(multiply(inverse(inverse(multiply(B,C))),inverse(C))),multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(F),F)))),inverse(V6))) = multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),inverse(V6)),
inference(paramod,[status(thm)],[c_3183,c_4123]) ).
cnf(c_3331,plain,
multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))),inverse(B)) = multiply(inverse(multiply(inverse(inverse(multiply(C,A))),inverse(A))),multiply(multiply(inverse(inverse(C)),inverse(inverse(multiply(inverse(D),D)))),inverse(B))),
inference(copy,[status(thm)],[c_4124]) ).
cnf(c_4125,plain,
multiply(inverse(multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C)))),inverse(D))),multiply(inverse(multiply(E,inverse(multiply(multiply(inverse(multiply(inverse(F),F)),B),C)))),multiply(E,inverse(C)))) = multiply(inverse(multiply(V6,inverse(D))),multiply(V6,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),
inference(paramod,[status(thm)],[c_3183,c_1242]) ).
cnf(c_4126,plain,
multiply(inverse(multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C)))),inverse(D))),multiply(inverse(multiply(E,inverse(multiply(B,C)))),multiply(E,inverse(C)))) = multiply(inverse(multiply(V6,inverse(D))),multiply(V6,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),
inference(paramod,[status(thm)],[c_3050,c_4125]) ).
cnf(c_4127,plain,
multiply(inverse(multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C)))),inverse(D))),multiply(inverse(inverse(multiply(B,C))),inverse(C))) = multiply(inverse(multiply(V6,inverse(D))),multiply(V6,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),
inference(paramod,[status(thm)],[c_3183,c_4126]) ).
cnf(c_3333,plain,
multiply(inverse(multiply(multiply(inverse(inverse(A)),inverse(inverse(multiply(inverse(B),B)))),inverse(C))),multiply(inverse(inverse(multiply(A,B))),inverse(B))) = multiply(inverse(inverse(C)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_3183,c_4127]) ).
cnf(c_4128,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(B)) = multiply(inverse(multiply(inverse(inverse(multiply(D,E))),inverse(E))),multiply(multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(inverse(multiply(inverse(E),E))))),inverse(B))),
inference(paramod,[status(thm)],[c_3183,c_3161]) ).
cnf(c_3370,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(B)) = multiply(inverse(multiply(inverse(inverse(multiply(C,D))),inverse(D))),multiply(multiply(inverse(inverse(C)),inverse(inverse(multiply(inverse(D),D)))),inverse(B))),
inference(paramod,[status(thm)],[c_3183,c_4128]) ).
cnf(c_3372,plain,
multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))),inverse(B)) = multiply(multiply(inverse(C),C),inverse(B)),
inference(paramod,[status(thm)],[c_3183,c_3159]) ).
cnf(c_4129,plain,
multiply(multiply(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),E)))))),inverse(multiply(inverse(inverse(F)),inverse(F)))),multiply(inverse(inverse(F)),inverse(F))) = B,
inference(paramod,[status(thm)],[c_3293,c_3081]) ).
cnf(c_3389,plain,
multiply(multiply(multiply(inverse(inverse(A)),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(inverse(D)),inverse(D)))),multiply(inverse(inverse(D)),inverse(D))) = A,
inference(paramod,[status(thm)],[c_3183,c_4129]) ).
cnf(c_4130,plain,
inverse(multiply(multiply(inverse(multiply(multiply(inverse(inverse(multiply(B,C))),inverse(C)),inverse(multiply(D,multiply(inverse(C),C))))),B),inverse(E))) = multiply(multiply(inverse(multiply(F,inverse(multiply(inverse(inverse(E)),inverse(multiply(inverse(C),C)))))),multiply(F,inverse(D))),inverse(multiply(inverse(V6),V6))),
inference(paramod,[status(thm)],[c_3183,c_1816]) ).
cnf(c_3453,plain,
inverse(multiply(multiply(inverse(multiply(multiply(inverse(inverse(multiply(A,B))),inverse(B)),inverse(multiply(C,multiply(inverse(B),B))))),A),inverse(D))) = multiply(multiply(inverse(inverse(multiply(inverse(inverse(D)),inverse(multiply(inverse(B),B))))),inverse(C)),inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_3183,c_4130]) ).
cnf(c_4131,plain,
multiply(inverse(multiply(multiply(inverse(inverse(A)),multiply(multiply(inverse(B),multiply(multiply(inverse(inverse(multiply(B,D))),inverse(D)),inverse(A))),inverse(A))),inverse(E))),inverse(A)) = multiply(inverse(multiply(F,inverse(E))),multiply(F,inverse(multiply(inverse(A),A)))),
inference(paramod,[status(thm)],[c_3183,c_1735]) ).
cnf(c_3455,plain,
multiply(inverse(multiply(multiply(inverse(inverse(A)),multiply(multiply(inverse(B),multiply(multiply(inverse(inverse(multiply(B,C))),inverse(C)),inverse(A))),inverse(A))),inverse(D))),inverse(A)) = multiply(inverse(inverse(D)),inverse(multiply(inverse(A),A))),
inference(paramod,[status(thm)],[c_3183,c_4131]) ).
cnf(c_4132,plain,
multiply(inverse(multiply(inverse(inverse(multiply(B,C))),inverse(C))),multiply(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(inverse(multiply(inverse(C),C))))),inverse(E))) = multiply(inverse(F),multiply(multiply(inverse(multiply(V6,inverse(multiply(F,V7)))),multiply(V6,inverse(V7))),inverse(E))),
inference(paramod,[status(thm)],[c_3183,c_1278]) ).
cnf(c_4133,plain,
multiply(inverse(multiply(inverse(inverse(multiply(B,C))),inverse(C))),multiply(multiply(inverse(inverse(B)),inverse(inverse(multiply(inverse(C),C)))),inverse(E))) = multiply(inverse(F),multiply(multiply(inverse(multiply(V6,inverse(multiply(F,V7)))),multiply(V6,inverse(V7))),inverse(E))),
inference(paramod,[status(thm)],[c_3183,c_4132]) ).
cnf(c_3499,plain,
multiply(inverse(multiply(inverse(inverse(multiply(A,B))),inverse(B))),multiply(multiply(inverse(inverse(A)),inverse(inverse(multiply(inverse(B),B)))),inverse(C))) = multiply(inverse(D),multiply(multiply(inverse(inverse(multiply(D,E))),inverse(E)),inverse(C))),
inference(paramod,[status(thm)],[c_3183,c_4133]) ).
cnf(c_4134,plain,
multiply(inverse(inverse(B)),inverse(B)) = multiply(multiply(inverse(C),C),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))),
inference(paramod,[status(thm)],[c_3183,c_863]) ).
cnf(c_4135,plain,
multiply(inverse(inverse(B)),inverse(B)) = inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B)))),
inference(paramod,[status(thm)],[c_3293,c_4134]) ).
cnf(c_3552,plain,
inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))) = multiply(inverse(inverse(A)),inverse(A)),
inference(copy,[status(thm)],[c_4135]) ).
cnf(c_4136,plain,
inverse(multiply(A,inverse(multiply(multiply(B,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(D),D))))),E)))) = multiply(multiply(inverse(inverse(B)),inverse(multiply(A,inverse(E)))),inverse(multiply(inverse(multiply(A,inverse(E))),multiply(A,inverse(E))))),
inference(paramod,[status(thm)],[c_3183,c_777]) ).
cnf(c_3570,plain,
inverse(multiply(A,inverse(multiply(multiply(B,inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(D),D))))),E)))) = multiply(multiply(inverse(inverse(B)),inverse(multiply(A,inverse(E)))),inverse(multiply(inverse(inverse(E)),inverse(E)))),
inference(paramod,[status(thm)],[c_3183,c_4136]) ).
cnf(c_3592,plain,
multiply(multiply(inverse(inverse(A)),multiply(multiply(inverse(B),multiply(multiply(inverse(inverse(multiply(B,A))),inverse(A)),inverse(A))),inverse(A))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(D),D))))) = inverse(A),
inference(paramod,[status(thm)],[c_3183,c_287]) ).
cnf(c_4137,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(B),multiply(multiply(inverse(inverse(multiply(B,D))),inverse(D)),inverse(A))),inverse(A))) = multiply(multiply(inverse(multiply(E,inverse(inverse(A)))),multiply(E,inverse(inverse(multiply(inverse(A),A))))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))),
inference(paramod,[status(thm)],[c_3183,c_266]) ).
cnf(c_4138,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(B),multiply(multiply(inverse(inverse(multiply(B,D))),inverse(D)),inverse(A))),inverse(A))) = multiply(multiply(inverse(inverse(inverse(A))),inverse(inverse(multiply(inverse(A),A)))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A))))),
inference(paramod,[status(thm)],[c_3183,c_4137]) ).
cnf(c_3598,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(B),multiply(multiply(inverse(inverse(multiply(B,C))),inverse(C)),inverse(A))),inverse(A))) = multiply(multiply(inverse(inverse(inverse(A))),inverse(inverse(multiply(inverse(A),A)))),multiply(inverse(inverse(A)),inverse(A))),
inference(paramod,[status(thm)],[c_3552,c_4138]) ).
cnf(c_4139,plain,
multiply(inverse(A),multiply(multiply(inverse(inverse(multiply(A,C))),inverse(C)),inverse(C))) = multiply(multiply(inverse(multiply(D,inverse(inverse(C)))),multiply(D,inverse(inverse(multiply(inverse(E),E))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_3183,c_249]) ).
cnf(c_4140,plain,
multiply(inverse(A),multiply(multiply(inverse(inverse(multiply(A,C))),inverse(C)),inverse(C))) = multiply(multiply(inverse(inverse(inverse(C))),inverse(inverse(multiply(inverse(E),E)))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))),
inference(paramod,[status(thm)],[c_3183,c_4139]) ).
cnf(c_3606,plain,
multiply(inverse(A),multiply(multiply(inverse(inverse(multiply(A,B))),inverse(B)),inverse(B))) = multiply(multiply(inverse(inverse(inverse(B))),inverse(inverse(multiply(inverse(C),C)))),multiply(inverse(inverse(B)),inverse(B))),
inference(paramod,[status(thm)],[c_3552,c_4140]) ).
cnf(c_3609,plain,
multiply(multiply(inverse(A),multiply(multiply(inverse(inverse(multiply(A,B))),inverse(B)),inverse(C))),inverse(multiply(inverse(D),D))) = inverse(C),
inference(paramod,[status(thm)],[c_3183,c_242]) ).
cnf(c_3632,plain,
multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),A),multiply(inverse(inverse(B)),inverse(B))),inverse(multiply(C,multiply(inverse(B),B))))),inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))) = C,
inference(paramod,[status(thm)],[c_3552,c_3289]) ).
cnf(c_4141,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B))) = multiply(inverse(inverse(A)),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_3333,c_3268]) ).
cnf(c_3638,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B))) = multiply(inverse(inverse(A)),multiply(inverse(inverse(C)),inverse(C))),
inference(paramod,[status(thm)],[c_3552,c_4141]) ).
cnf(c_4142,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(A))),inverse(B)) = multiply(multiply(inverse(C),C),inverse(B)),
inference(paramod,[status(thm)],[c_3552,c_3372]) ).
cnf(c_4143,plain,
inverse(B) = multiply(multiply(inverse(C),C),inverse(B)),
inference(paramod,[status(thm)],[c_3050,c_4142]) ).
cnf(c_3699,plain,
multiply(multiply(inverse(A),A),inverse(B)) = inverse(B),
inference(copy,[status(thm)],[c_4143]) ).
cnf(c_4144,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(A))),inverse(B)) = multiply(inverse(multiply(inverse(inverse(multiply(C,A))),inverse(A))),multiply(multiply(inverse(inverse(C)),inverse(inverse(multiply(inverse(D),D)))),inverse(B))),
inference(paramod,[status(thm)],[c_3552,c_3331]) ).
cnf(c_4145,plain,
inverse(B) = multiply(inverse(multiply(inverse(inverse(multiply(C,A))),inverse(A))),multiply(multiply(inverse(inverse(C)),inverse(inverse(multiply(inverse(D),D)))),inverse(B))),
inference(paramod,[status(thm)],[c_3050,c_4144]) ).
cnf(c_3712,plain,
multiply(inverse(multiply(inverse(inverse(multiply(A,B))),inverse(B))),multiply(multiply(inverse(inverse(A)),inverse(inverse(multiply(inverse(C),C)))),inverse(D))) = inverse(D),
inference(copy,[status(thm)],[c_4145]) ).
cnf(c_3716,plain,
multiply(multiply(inverse(multiply(multiply(multiply(inverse(inverse(A)),inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(inverse(C)),inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),A),inverse(multiply(inverse(C),C))) = D,
inference(paramod,[status(thm)],[c_3552,c_3292]) ).
cnf(c_3719,plain,
multiply(inverse(inverse(multiply(A,B))),inverse(B)) = multiply(multiply(inverse(inverse(A)),inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(inverse(B)),inverse(B))),
inference(paramod,[status(thm)],[c_3552,c_3224]) ).
cnf(c_4146,plain,
inverse(C) = multiply(inverse(D),multiply(multiply(inverse(inverse(multiply(D,E))),inverse(E)),inverse(C))),
inference(paramod,[status(thm)],[c_3712,c_3499]) ).
cnf(c_3736,plain,
multiply(inverse(A),multiply(multiply(inverse(inverse(multiply(A,B))),inverse(B)),inverse(C))) = inverse(C),
inference(copy,[status(thm)],[c_4146]) ).
cnf(c_3737,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(B)) = inverse(B),
inference(paramod,[status(thm)],[c_3712,c_3370]) ).
cnf(c_4147,plain,
multiply(multiply(inverse(inverse(A)),multiply(inverse(A),inverse(A))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(D),D))))) = inverse(A),
inference(paramod,[status(thm)],[c_3736,c_3592]) ).
cnf(c_3758,plain,
multiply(multiply(inverse(inverse(A)),multiply(inverse(A),inverse(A))),inverse(inverse(multiply(inverse(B),B)))) = inverse(A),
inference(paramod,[status(thm)],[c_3737,c_4147]) ).
cnf(c_3763,plain,
inverse(multiply(A,inverse(multiply(multiply(B,inverse(inverse(multiply(inverse(C),C)))),D)))) = multiply(multiply(inverse(inverse(B)),inverse(multiply(A,inverse(D)))),inverse(multiply(inverse(inverse(D)),inverse(D)))),
inference(paramod,[status(thm)],[c_3737,c_3570]) ).
cnf(c_3791,plain,
multiply(multiply(multiply(inverse(inverse(A)),inverse(inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(inverse(C)),inverse(C)))),multiply(inverse(inverse(C)),inverse(C))) = A,
inference(paramod,[status(thm)],[c_3737,c_3389]) ).
cnf(c_3803,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),inverse(multiply(inverse(C),C))) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_3737,c_3211]) ).
cnf(c_3818,plain,
multiply(inverse(A),inverse(multiply(inverse(B),B))) = inverse(A),
inference(paramod,[status(thm)],[c_3736,c_3609]) ).
cnf(c_4148,plain,
inverse(B) = multiply(multiply(inverse(inverse(inverse(B))),inverse(inverse(multiply(inverse(C),C)))),multiply(inverse(inverse(B)),inverse(B))),
inference(paramod,[status(thm)],[c_3736,c_3606]) ).
cnf(c_3819,plain,
multiply(multiply(inverse(inverse(inverse(A))),inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(inverse(A)),inverse(A))) = inverse(A),
inference(copy,[status(thm)],[c_4148]) ).
cnf(c_4149,plain,
multiply(inverse(inverse(A)),multiply(inverse(A),inverse(A))) = multiply(multiply(inverse(inverse(inverse(A))),inverse(inverse(multiply(inverse(A),A)))),multiply(inverse(inverse(A)),inverse(A))),
inference(paramod,[status(thm)],[c_3736,c_3598]) ).
cnf(c_3821,plain,
multiply(inverse(inverse(A)),multiply(inverse(A),inverse(A))) = inverse(A),
inference(paramod,[status(thm)],[c_3819,c_4149]) ).
cnf(c_4150,plain,
multiply(inverse(multiply(multiply(inverse(inverse(A)),multiply(inverse(A),inverse(A))),inverse(D))),inverse(A)) = multiply(inverse(inverse(D)),inverse(multiply(inverse(A),A))),
inference(paramod,[status(thm)],[c_3736,c_3455]) ).
cnf(c_4151,plain,
multiply(inverse(multiply(inverse(A),inverse(D))),inverse(A)) = multiply(inverse(inverse(D)),inverse(multiply(inverse(A),A))),
inference(paramod,[status(thm)],[c_3821,c_4150]) ).
cnf(c_3826,plain,
multiply(inverse(multiply(inverse(A),inverse(B))),inverse(A)) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_3818,c_4151]) ).
cnf(c_4152,plain,
multiply(inverse(multiply(multiply(inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(C),C))))),inverse(C)),inverse(E))),D) = multiply(inverse(inverse(E)),inverse(multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_3736,c_3253]) ).
cnf(c_4153,plain,
multiply(inverse(multiply(inverse(inverse(multiply(D,multiply(inverse(C),C)))),inverse(E))),D) = multiply(inverse(inverse(E)),inverse(multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_3826,c_4152]) ).
cnf(c_3839,plain,
multiply(inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(B),B)))),inverse(C))),A) = inverse(inverse(C)),
inference(paramod,[status(thm)],[c_3818,c_4153]) ).
cnf(c_3873,plain,
inverse(multiply(inverse(inverse(A)),inverse(B))) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_3818,c_3803]) ).
cnf(c_4154,plain,
inverse(inverse(A)) = multiply(inverse(inverse(A)),multiply(inverse(inverse(C)),inverse(C))),
inference(paramod,[status(thm)],[c_3818,c_3638]) ).
cnf(c_3882,plain,
multiply(inverse(inverse(A)),multiply(inverse(inverse(B)),inverse(B))) = inverse(inverse(A)),
inference(copy,[status(thm)],[c_4154]) ).
cnf(c_4155,plain,
multiply(inverse(multiply(multiply(multiply(inverse(A),A),multiply(inverse(inverse(B)),inverse(B))),inverse(multiply(C,multiply(inverse(B),B))))),inverse(multiply(inverse(B),B))) = C,
inference(paramod,[status(thm)],[c_3818,c_3632]) ).
cnf(c_3883,plain,
inverse(multiply(multiply(multiply(inverse(A),A),multiply(inverse(inverse(B)),inverse(B))),inverse(multiply(C,multiply(inverse(B),B))))) = C,
inference(paramod,[status(thm)],[c_3818,c_4155]) ).
cnf(c_3890,plain,
inverse(multiply(multiply(inverse(multiply(multiply(inverse(inverse(multiply(A,B))),inverse(B)),inverse(multiply(C,multiply(inverse(B),B))))),A),inverse(D))) = multiply(multiply(inverse(inverse(inverse(inverse(D)))),inverse(C)),inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_3818,c_3453]) ).
cnf(c_4156,plain,
multiply(multiply(multiply(inverse(inverse(A)),multiply(inverse(inverse(B)),inverse(B))),inverse(multiply(inverse(inverse(B)),inverse(B)))),multiply(inverse(C),C)) = A,
inference(paramod,[status(thm)],[c_3873,c_3302]) ).
cnf(c_4157,plain,
multiply(multiply(inverse(inverse(A)),inverse(multiply(inverse(inverse(B)),inverse(B)))),multiply(inverse(C),C)) = A,
inference(paramod,[status(thm)],[c_3882,c_4156]) ).
cnf(c_4158,plain,
multiply(multiply(inverse(inverse(A)),multiply(inverse(inverse(B)),inverse(B))),multiply(inverse(C),C)) = A,
inference(paramod,[status(thm)],[c_3873,c_4157]) ).
cnf(c_3892,plain,
multiply(inverse(inverse(A)),multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_3882,c_4158]) ).
cnf(c_4159,plain,
multiply(inverse(inverse(multiply(A,multiply(inverse(B),B)))),inverse(multiply(inverse(D),D))) = A,
inference(paramod,[status(thm)],[c_3818,c_3231]) ).
cnf(c_3894,plain,
inverse(inverse(multiply(A,multiply(inverse(B),B)))) = A,
inference(paramod,[status(thm)],[c_3818,c_4159]) ).
cnf(c_4160,plain,
multiply(multiply(inverse(inverse(A)),inverse(multiply(inverse(inverse(C)),inverse(C)))),multiply(inverse(inverse(C)),inverse(C))) = A,
inference(paramod,[status(thm)],[c_3818,c_3230]) ).
cnf(c_4161,plain,
multiply(multiply(inverse(inverse(A)),multiply(inverse(inverse(C)),inverse(C))),multiply(inverse(inverse(C)),inverse(C))) = A,
inference(paramod,[status(thm)],[c_3873,c_4160]) ).
cnf(c_3895,plain,
multiply(A,multiply(inverse(inverse(B)),inverse(B))) = A,
inference(paramod,[status(thm)],[c_3892,c_4161]) ).
cnf(c_3898,plain,
multiply(inverse(A),inverse(inverse(multiply(inverse(B),B)))) = inverse(A),
inference(paramod,[status(thm)],[c_3821,c_3758]) ).
cnf(c_3913,plain,
multiply(inverse(multiply(A,inverse(B))),A) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_3894,c_3839]) ).
cnf(c_4162,plain,
multiply(multiply(inverse(inverse(A)),inverse(multiply(inverse(inverse(C)),inverse(C)))),multiply(inverse(inverse(C)),inverse(C))) = A,
inference(paramod,[status(thm)],[c_3898,c_3791]) ).
cnf(c_4163,plain,
multiply(multiply(inverse(inverse(A)),multiply(inverse(inverse(C)),inverse(C))),multiply(inverse(inverse(C)),inverse(C))) = A,
inference(paramod,[status(thm)],[c_3873,c_4162]) ).
cnf(c_4164,plain,
multiply(inverse(inverse(A)),multiply(inverse(inverse(C)),inverse(C))) = A,
inference(paramod,[status(thm)],[c_3895,c_4163]) ).
cnf(c_3916,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_3895,c_4164]) ).
cnf(c_4165,plain,
inverse(multiply(A,inverse(multiply(multiply(B,multiply(inverse(C),C)),D)))) = multiply(multiply(inverse(inverse(B)),inverse(multiply(A,inverse(D)))),inverse(multiply(inverse(inverse(D)),inverse(D)))),
inference(paramod,[status(thm)],[c_3916,c_3763]) ).
cnf(c_4166,plain,
inverse(multiply(A,inverse(multiply(multiply(B,multiply(inverse(C),C)),D)))) = multiply(multiply(B,inverse(multiply(A,inverse(D)))),inverse(multiply(inverse(inverse(D)),inverse(D)))),
inference(paramod,[status(thm)],[c_3916,c_4165]) ).
cnf(c_3920,plain,
inverse(multiply(A,inverse(multiply(multiply(B,multiply(inverse(C),C)),D)))) = multiply(multiply(B,inverse(multiply(A,inverse(D)))),inverse(multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_3916,c_4166]) ).
cnf(c_4167,plain,
multiply(A,multiply(inverse(inverse(B)),inverse(B))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_3916,c_3882]) ).
cnf(c_4168,plain,
multiply(A,multiply(B,inverse(B))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_3916,c_4167]) ).
cnf(c_3987,plain,
multiply(A,multiply(B,inverse(B))) = A,
inference(paramod,[status(thm)],[c_3916,c_4168]) ).
cnf(c_4169,plain,
inverse(multiply(multiply(multiply(inverse(A),A),multiply(B,inverse(B))),inverse(multiply(C,multiply(inverse(B),B))))) = C,
inference(paramod,[status(thm)],[c_3916,c_3883]) ).
cnf(c_4170,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(C,multiply(inverse(B),B))))) = C,
inference(paramod,[status(thm)],[c_3987,c_4169]) ).
cnf(c_4171,plain,
inverse(inverse(multiply(C,multiply(inverse(B),B)))) = C,
inference(paramod,[status(thm)],[c_3699,c_4170]) ).
cnf(c_3995,plain,
multiply(A,multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_3916,c_4171]) ).
cnf(c_4172,plain,
multiply(multiply(A,B),inverse(B)) = multiply(multiply(inverse(inverse(A)),inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(inverse(B)),inverse(B))),
inference(paramod,[status(thm)],[c_3916,c_3719]) ).
cnf(c_4173,plain,
multiply(multiply(A,B),inverse(B)) = multiply(multiply(A,inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(inverse(B)),inverse(B))),
inference(paramod,[status(thm)],[c_3916,c_4172]) ).
cnf(c_4174,plain,
multiply(multiply(A,B),inverse(B)) = multiply(multiply(A,multiply(inverse(B),B)),multiply(inverse(inverse(B)),inverse(B))),
inference(paramod,[status(thm)],[c_3916,c_4173]) ).
cnf(c_4175,plain,
multiply(multiply(A,B),inverse(B)) = multiply(A,multiply(inverse(inverse(B)),inverse(B))),
inference(paramod,[status(thm)],[c_3995,c_4174]) ).
cnf(c_4176,plain,
multiply(multiply(A,B),inverse(B)) = multiply(A,multiply(B,inverse(B))),
inference(paramod,[status(thm)],[c_3916,c_4175]) ).
cnf(c_4005,plain,
multiply(multiply(A,B),inverse(B)) = A,
inference(paramod,[status(thm)],[c_3987,c_4176]) ).
cnf(c_4177,plain,
multiply(multiply(inverse(multiply(multiply(multiply(A,inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(inverse(C)),inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),A),inverse(multiply(inverse(C),C))) = D,
inference(paramod,[status(thm)],[c_3916,c_3716]) ).
cnf(c_4178,plain,
multiply(multiply(inverse(multiply(multiply(multiply(A,multiply(inverse(B),B)),multiply(inverse(inverse(C)),inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),A),inverse(multiply(inverse(C),C))) = D,
inference(paramod,[status(thm)],[c_3916,c_4177]) ).
cnf(c_4179,plain,
multiply(multiply(inverse(multiply(multiply(A,multiply(inverse(inverse(C)),inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),A),inverse(multiply(inverse(C),C))) = D,
inference(paramod,[status(thm)],[c_3995,c_4178]) ).
cnf(c_4180,plain,
multiply(multiply(inverse(multiply(multiply(A,multiply(C,inverse(C))),inverse(multiply(D,multiply(inverse(C),C))))),A),inverse(multiply(inverse(C),C))) = D,
inference(paramod,[status(thm)],[c_3916,c_4179]) ).
cnf(c_4181,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(D,multiply(inverse(C),C))))),A),inverse(multiply(inverse(C),C))) = D,
inference(paramod,[status(thm)],[c_3987,c_4180]) ).
cnf(c_4182,plain,
multiply(multiply(inverse(multiply(A,inverse(D))),A),inverse(multiply(inverse(C),C))) = D,
inference(paramod,[status(thm)],[c_3995,c_4181]) ).
cnf(c_4183,plain,
multiply(inverse(inverse(D)),inverse(multiply(inverse(C),C))) = D,
inference(paramod,[status(thm)],[c_3913,c_4182]) ).
cnf(c_4007,plain,
multiply(A,inverse(multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_3916,c_4183]) ).
cnf(c_4184,plain,
inverse(multiply(multiply(inverse(multiply(multiply(multiply(A,B),inverse(B)),inverse(multiply(C,multiply(inverse(B),B))))),A),inverse(D))) = multiply(multiply(inverse(inverse(inverse(inverse(D)))),inverse(C)),inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_3916,c_3890]) ).
cnf(c_4185,plain,
inverse(multiply(multiply(inverse(multiply(A,inverse(multiply(C,multiply(inverse(B),B))))),A),inverse(D))) = multiply(multiply(inverse(inverse(inverse(inverse(D)))),inverse(C)),inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_4005,c_4184]) ).
cnf(c_4186,plain,
inverse(multiply(multiply(inverse(multiply(A,inverse(C))),A),inverse(D))) = multiply(multiply(inverse(inverse(inverse(inverse(D)))),inverse(C)),inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_3995,c_4185]) ).
cnf(c_4187,plain,
inverse(multiply(inverse(inverse(C)),inverse(D))) = multiply(multiply(inverse(inverse(inverse(inverse(D)))),inverse(C)),inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_3913,c_4186]) ).
cnf(c_4188,plain,
inverse(multiply(C,inverse(D))) = multiply(multiply(inverse(inverse(inverse(inverse(D)))),inverse(C)),inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_3916,c_4187]) ).
cnf(c_4189,plain,
inverse(multiply(C,inverse(D))) = multiply(multiply(inverse(inverse(D)),inverse(C)),inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_3916,c_4188]) ).
cnf(c_4190,plain,
inverse(multiply(C,inverse(D))) = multiply(multiply(D,inverse(C)),inverse(multiply(inverse(E),E))),
inference(paramod,[status(thm)],[c_3916,c_4189]) ).
cnf(c_4008,plain,
inverse(multiply(A,inverse(B))) = multiply(B,inverse(A)),
inference(paramod,[status(thm)],[c_4007,c_4190]) ).
cnf(c_4191,plain,
inverse(multiply(A,inverse(multiply(B,D)))) = multiply(multiply(B,inverse(multiply(A,inverse(D)))),inverse(multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_3995,c_3920]) ).
cnf(c_4192,plain,
multiply(multiply(B,D),inverse(A)) = multiply(multiply(B,inverse(multiply(A,inverse(D)))),inverse(multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_4008,c_4191]) ).
cnf(c_4193,plain,
multiply(multiply(B,D),inverse(A)) = multiply(multiply(B,multiply(D,inverse(A))),inverse(multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_4008,c_4192]) ).
cnf(c_4194,plain,
multiply(multiply(B,D),inverse(A)) = multiply(multiply(B,multiply(D,inverse(A))),multiply(D,inverse(D))),
inference(paramod,[status(thm)],[c_4008,c_4193]) ).
cnf(c_4030,plain,
multiply(multiply(A,B),inverse(C)) = multiply(A,multiply(B,inverse(C))),
inference(paramod,[status(thm)],[c_3987,c_4194]) ).
cnf(c_4195,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,inverse(inverse(C)))),
inference(paramod,[status(thm)],[c_3916,c_4030]) ).
cnf(c_4072,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_3916,c_4195]) ).
cnf(c_4073,plain,
$false,
inference(resolve,[status(thm)],[c_4072,c_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP411-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.36 % Computer : n010.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Fri Sep 25 14:53:30 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.37 % Process 1022278 was started by sandbox2 on n010,
% 0.12/0.37 % Fri Sep 25 14:53:30 2026
% 0.12/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/0.38
% 0.15/0.38 % From the command line: assign(max_seconds, 300).
% 19.14/2.83
% 19.14/2.83 % SZS status Unsatisfiable for theBenchmark
% 19.14/2.83
% 19.14/2.83 % Proof 1 at 1.99 (+ 0.39) seconds.
% 19.14/2.83 % Length of proof is 137.
% 19.14/2.83 % Level of proof is 28.
% 19.14/2.83 % Maximum clause weight is 100.000.
% 19.14/2.83 % Given clauses 84.
% 19.14/2.83
% 19.14/2.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------