%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP052-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:26:35 AM UTC 2026
% Result : Unsatisfiable 10.66s 3.36s
% Output : CNFRefutation 10.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 2
% Syntax : Number of formulae : 350 ( 345 unt; 0 def)
% Number of atoms : 358 ( 357 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 17 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 1561 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,inverse(multiply(multiply(multiply(inverse(VAR_1),VAR_1),inverse(multiply(inverse(multiply(VAR_0,inverse(VAR_1))),VAR_2))),VAR_1))) = VAR_2,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(A,inverse(B))),C))),B))) = C,
inference(clausify,[status(thm)],[single_axiom]) ).
fof(prove_these_axioms,axiom,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
file('theBenchmark.p',prove_these_axioms) ).
cnf(c_2,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(clausify,[status(thm)],[prove_these_axioms]) ).
cnf(c_3,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ),
inference(copy,[status(thm)],[c_2]) ).
cnf(c_4,plain,
multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(C)),B))) = inverse(multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),inverse(D))),C))),D)),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_5,plain,
inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(inverse(multiply(B,inverse(C))),inverse(A))),multiply(inverse(multiply(B,inverse(C))),D)))),A)) = D,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_6,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(C)),B)))) = C,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_2120,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,B)))) = multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(multiply(multiply(inverse(B),B),inverse(D))),C))),D),
inference(paramod,[status(thm)],[c_1,c_6]) ).
cnf(c_7,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(multiply(inverse(B),B),inverse(A))),C))),A) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(multiply(C,B)))),
inference(copy,[status(thm)],[c_2120]) ).
cnf(c_9,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(A))),multiply(B,inverse(multiply(C,A)))))) = C,
inference(paramod,[status(thm)],[c_7,c_1]) ).
cnf(c_11,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(multiply(E,D))))))) = multiply(inverse(multiply(multiply(inverse(D),D),inverse(B))),E),
inference(paramod,[status(thm)],[c_7,c_6]) ).
cnf(c_15,plain,
multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(multiply(inverse(C),C),inverse(B))),D))),B))) = multiply(A,inverse(multiply(inverse(multiply(E,inverse(C))),multiply(E,inverse(multiply(D,C)))))),
inference(paramod,[status(thm)],[c_11,c_1]) ).
cnf(c_2121,plain,
multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(A,inverse(B))),inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(multiply(E,D)))))))),B))) = inverse(multiply(multiply(multiply(inverse(F),F),inverse(multiply(inverse(multiply(multiply(inverse(D),D),inverse(F))),E))),F)),
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_2122,plain,
inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(multiply(E,D))))) = inverse(multiply(multiply(multiply(inverse(F),F),inverse(multiply(inverse(multiply(multiply(inverse(D),D),inverse(F))),E))),F)),
inference(paramod,[status(thm)],[c_1,c_2121]) ).
cnf(c_17,plain,
inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(multiply(inverse(B),B),inverse(A))),C))),A)) = inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(multiply(C,B))))),
inference(copy,[status(thm)],[c_2122]) ).
cnf(c_2123,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(C,inverse(D))),inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(C,inverse(D))),inverse(E))),F))),E)))))) = multiply(inverse(multiply(multiply(inverse(D),D),inverse(B))),multiply(multiply(inverse(D),D),inverse(F))),
inference(paramod,[status(thm)],[c_4,c_11]) ).
cnf(c_2124,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(F))) = multiply(inverse(multiply(multiply(inverse(D),D),inverse(B))),multiply(multiply(inverse(D),D),inverse(F))),
inference(paramod,[status(thm)],[c_1,c_2123]) ).
cnf(c_18,plain,
multiply(inverse(multiply(multiply(inverse(A),A),inverse(B))),multiply(multiply(inverse(A),A),inverse(C))) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C))),
inference(copy,[status(thm)],[c_2124]) ).
cnf(c_2125,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(A))),multiply(B,inverse(C))))),A) = multiply(inverse(multiply(D,inverse(E))),multiply(D,inverse(multiply(multiply(multiply(inverse(E),E),inverse(C)),E)))),
inference(paramod,[status(thm)],[c_18,c_7]) ).
cnf(c_21,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(A))),multiply(B,inverse(C))))),A) = C,
inference(paramod,[status(thm)],[c_6,c_2125]) ).
cnf(c_2126,plain,
inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(inverse(B),inverse(A))),multiply(inverse(multiply(C,inverse(multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(multiply(C,inverse(D))),B))),D)))),E)))),A)) = E,
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_27,plain,
inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(inverse(B),inverse(A))),multiply(inverse(B),C)))),A)) = C,
inference(paramod,[status(thm)],[c_1,c_2126]) ).
cnf(c_2127,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,C)) = multiply(inverse(multiply(inverse(multiply(D,inverse(E))),inverse(B))),multiply(inverse(multiply(D,inverse(E))),C)),
inference(paramod,[status(thm)],[c_5,c_6]) ).
cnf(c_28,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),inverse(C))),multiply(inverse(multiply(A,inverse(B))),D)) = multiply(inverse(multiply(E,inverse(C))),multiply(E,D)),
inference(copy,[status(thm)],[c_2127]) ).
cnf(c_2128,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(multiply(E,D))))))) = multiply(inverse(multiply(multiply(inverse(D),D),inverse(multiply(multiply(multiply(inverse(F),F),inverse(multiply(inverse(multiply(inverse(multiply(V6,inverse(V7))),inverse(F))),multiply(inverse(multiply(V6,inverse(V7))),B)))),F)))),E),
inference(paramod,[status(thm)],[c_5,c_11]) ).
cnf(c_30,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(multiply(E,D))))))) = multiply(inverse(multiply(multiply(inverse(D),D),B)),E),
inference(paramod,[status(thm)],[c_27,c_2128]) ).
cnf(c_2129,plain,
inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(A))),multiply(inverse(multiply(multiply(multiply(inverse(inverse(C)),inverse(C)),inverse(multiply(inverse(multiply(inverse(multiply(D,inverse(E))),inverse(inverse(C)))),multiply(inverse(multiply(D,inverse(E))),B)))),inverse(C))),F)))),A)) = F,
inference(paramod,[status(thm)],[c_5,c_5]) ).
cnf(c_31,plain,
inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(A))),multiply(B,C)))),A)) = C,
inference(paramod,[status(thm)],[c_27,c_2129]) ).
cnf(c_50,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,C)) = multiply(inverse(multiply(D,inverse(B))),multiply(D,C)),
inference(paramod,[status(thm)],[c_28,c_28]) ).
cnf(c_2130,plain,
multiply(inverse(A),multiply(B,C)) = multiply(inverse(multiply(D,inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(B,inverse(E))),A))),E)))),multiply(D,C)),
inference(paramod,[status(thm)],[c_1,c_50]) ).
cnf(c_52,plain,
multiply(inverse(multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(C,inverse(B))),D))),B)))),multiply(A,E)) = multiply(inverse(D),multiply(C,E)),
inference(copy,[status(thm)],[c_2130]) ).
cnf(c_2131,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(multiply(multiply(inverse(C),C),inverse(D)),C))))),multiply(A,E)) = multiply(inverse(multiply(F,inverse(multiply(multiply(multiply(inverse(V6),V6),inverse(multiply(inverse(multiply(inverse(multiply(B,inverse(C))),inverse(V6))),D))),V6)))),multiply(F,E)),
inference(paramod,[status(thm)],[c_4,c_50]) ).
cnf(c_53,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(multiply(multiply(inverse(C),C),inverse(D)),C))))),multiply(A,E)) = multiply(inverse(D),multiply(inverse(multiply(B,inverse(C))),E)),
inference(paramod,[status(thm)],[c_52,c_2131]) ).
cnf(c_2132,plain,
multiply(inverse(A),multiply(multiply(inverse(B),B),C)) = multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(multiply(A,B))))))),multiply(D,C)),
inference(paramod,[status(thm)],[c_9,c_50]) ).
cnf(c_56,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(multiply(D,C))))))),multiply(A,E)) = multiply(inverse(D),multiply(multiply(inverse(C),C),E)),
inference(copy,[status(thm)],[c_2132]) ).
cnf(c_64,plain,
inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),C),B))))) = C,
inference(paramod,[status(thm)],[c_7,c_31]) ).
cnf(c_2133,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(F,inverse(E))),multiply(F,B)))),E)))),multiply(D,C)),
inference(paramod,[status(thm)],[c_31,c_50]) ).
cnf(c_67,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_31,c_2133]) ).
cnf(c_2134,plain,
multiply(inverse(multiply(A,B)),C) = multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(A,inverse(E))),C))),E)))),
inference(paramod,[status(thm)],[c_1,c_67]) ).
cnf(c_71,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(D,inverse(C))),E))),C)))) = multiply(inverse(multiply(D,B)),E),
inference(copy,[status(thm)],[c_2134]) ).
cnf(c_76,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(A,B)),inverse(multiply(inverse(multiply(C,inverse(multiply(A,B)))),multiply(C,inverse(multiply(inverse(multiply(D,E)),multiply(D,B))))))) = inverse(multiply(A,E)),
inference(paramod,[status(thm)],[c_67,c_9]) ).
cnf(c_83,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(F,multiply(D,C))),multiply(F,E)),
inference(paramod,[status(thm)],[c_67,c_67]) ).
cnf(c_84,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,C)),multiply(F,multiply(A,E))),
inference(paramod,[status(thm)],[c_67,c_67]) ).
cnf(c_2135,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(F,multiply(D,inverse(multiply(multiply(multiply(inverse(V6),V6),inverse(multiply(inverse(multiply(A,inverse(V6))),C))),V6))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_1,c_83]) ).
cnf(c_2136,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(inverse(multiply(A,inverse(V6))),C)),multiply(inverse(multiply(D,inverse(V6))),E)),
inference(paramod,[status(thm)],[c_53,c_2135]) ).
cnf(c_86,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),C)),multiply(inverse(multiply(D,inverse(B))),E)) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(D,F)),E)),
inference(copy,[status(thm)],[c_2136]) ).
cnf(c_2137,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),D) = multiply(inverse(multiply(E,multiply(F,C))),multiply(E,inverse(multiply(multiply(multiply(inverse(V6),V6),inverse(multiply(inverse(multiply(inverse(multiply(F,B)),inverse(V6))),D))),V6)))),
inference(paramod,[status(thm)],[c_1,c_83]) ).
cnf(c_87,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),D) = multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),D),
inference(paramod,[status(thm)],[c_71,c_2137]) ).
cnf(c_2138,plain,
multiply(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(A,B)),C)),inverse(multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(A,B)),C)))),multiply(D,inverse(multiply(inverse(multiply(E,multiply(A,F))),multiply(E,C))))))) = inverse(multiply(inverse(multiply(V6,B)),multiply(V6,F))),
inference(paramod,[status(thm)],[c_83,c_9]) ).
cnf(c_90,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),
inference(paramod,[status(thm)],[c_76,c_2138]) ).
cnf(c_98,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,E))),
inference(paramod,[status(thm)],[c_67,c_83]) ).
cnf(c_100,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),E)),
inference(paramod,[status(thm)],[c_67,c_83]) ).
cnf(c_116,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),inverse(multiply(multiply(multiply(inverse(D),D),inverse(F)),D)))) = F,
inference(paramod,[status(thm)],[c_87,c_6]) ).
cnf(c_2139,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(E,inverse(multiply(multiply(multiply(inverse(F),F),inverse(multiply(inverse(multiply(inverse(multiply(V6,C)),inverse(F))),A))),F)))),multiply(E,multiply(V6,D))),
inference(paramod,[status(thm)],[c_1,c_84]) ).
cnf(c_129,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(A),multiply(inverse(multiply(E,C)),multiply(E,D))),
inference(paramod,[status(thm)],[c_52,c_2139]) ).
cnf(c_2140,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(multiply(multiply(inverse(E),E),inverse(F)),E))))) = multiply(inverse(multiply(V6,C)),multiply(V6,inverse(multiply(multiply(multiply(inverse(V7),V7),inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(E))),inverse(V7))),F))),V7)))),
inference(paramod,[status(thm)],[c_4,c_84]) ).
cnf(c_130,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(multiply(multiply(inverse(E),E),inverse(F)),E))))) = multiply(inverse(multiply(inverse(multiply(A,inverse(E))),C)),F),
inference(paramod,[status(thm)],[c_71,c_2140]) ).
cnf(c_137,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_67,c_84]) ).
cnf(c_139,plain,
multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D))) = multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D))),
inference(paramod,[status(thm)],[c_84,c_83]) ).
cnf(c_2141,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(F,inverse(E))),multiply(F,A)))),E)),multiply(inverse(multiply(V6,C)),multiply(V6,D))),
inference(paramod,[status(thm)],[c_31,c_129]) ).
cnf(c_163,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(A,multiply(inverse(multiply(E,C)),multiply(E,D))),
inference(paramod,[status(thm)],[c_31,c_2141]) ).
cnf(c_2142,plain,
multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(multiply(inverse(C),C),inverse(B))),multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(D,inverse(C))),multiply(D,E))))))),B))) = multiply(A,inverse(multiply(inverse(multiply(F,inverse(C))),multiply(F,E)))),
inference(paramod,[status(thm)],[c_31,c_15]) ).
cnf(c_209,plain,
multiply(A,inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,D)))) = multiply(A,inverse(multiply(inverse(multiply(E,inverse(C))),multiply(E,D)))),
inference(paramod,[status(thm)],[c_21,c_2142]) ).
cnf(c_221,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D)))) = inverse(multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D)))),
inference(paramod,[status(thm)],[c_139,c_90]) ).
cnf(c_231,plain,
multiply(A,multiply(inverse(multiply(B,multiply(C,D))),multiply(B,multiply(C,E)))) = multiply(A,multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E)))),
inference(paramod,[status(thm)],[c_139,c_163]) ).
cnf(c_2143,plain,
multiply(A,inverse(multiply(inverse(multiply(B,C)),multiply(B,D)))) = multiply(A,inverse(multiply(inverse(multiply(E,inverse(multiply(multiply(multiply(inverse(F),F),inverse(multiply(inverse(multiply(V6,inverse(F))),multiply(V6,C)))),F)))),multiply(E,D)))),
inference(paramod,[status(thm)],[c_31,c_209]) ).
cnf(c_234,plain,
multiply(A,inverse(multiply(inverse(multiply(B,C)),multiply(B,D)))) = multiply(A,inverse(multiply(inverse(multiply(E,C)),multiply(E,D)))),
inference(paramod,[status(thm)],[c_31,c_2143]) ).
cnf(c_2144,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(F,inverse(E))),multiply(F,B)))),E)))),V6)) = multiply(inverse(multiply(inverse(multiply(A,V7)),C)),multiply(inverse(multiply(D,V7)),V6)),
inference(paramod,[status(thm)],[c_31,c_86]) ).
cnf(c_283,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(D,F)),E)),
inference(paramod,[status(thm)],[c_31,c_2144]) ).
cnf(c_312,plain,
multiply(inverse(multiply(A,B)),inverse(multiply(multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(inverse(multiply(A,D)),inverse(C))),multiply(inverse(multiply(E,D)),F)))),C))) = multiply(inverse(multiply(E,B)),F),
inference(paramod,[status(thm)],[c_283,c_1]) ).
cnf(c_363,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(multiply(multiply(inverse(C),C),D),C))))),multiply(inverse(multiply(E,B)),F)) = multiply(D,multiply(inverse(multiply(E,inverse(C))),F)),
inference(paramod,[status(thm)],[c_64,c_83]) ).
cnf(c_365,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7)) = multiply(inverse(multiply(V8,multiply(inverse(multiply(D,V6)),E))),multiply(V8,V7)),
inference(paramod,[status(thm)],[c_100,c_67]) ).
cnf(c_2145,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,inverse(multiply(D,E)))),multiply(C,inverse(multiply(F,multiply(D,E)))))))) = multiply(inverse(multiply(multiply(inverse(multiply(V6,E)),multiply(V6,E)),B)),F),
inference(paramod,[status(thm)],[c_67,c_30]) ).
cnf(c_500,plain,
multiply(inverse(multiply(multiply(inverse(multiply(A,B)),multiply(A,B)),C)),D) = multiply(inverse(multiply(multiply(inverse(multiply(E,B)),multiply(E,B)),C)),D),
inference(paramod,[status(thm)],[c_30,c_2145]) ).
cnf(c_501,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),D)),multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),inverse(multiply(inverse(multiply(F,inverse(V6))),multiply(F,inverse(multiply(V7,V6))))))) = multiply(inverse(multiply(multiply(inverse(V6),V6),D)),V7),
inference(paramod,[status(thm)],[c_87,c_30]) ).
cnf(c_2146,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(A))),multiply(B,inverse(multiply(inverse(multiply(multiply(inverse(multiply(C,D)),multiply(C,D)),E)),A)))))) = inverse(multiply(multiply(inverse(multiply(F,D)),multiply(F,D)),E)),
inference(paramod,[status(thm)],[c_500,c_9]) ).
cnf(c_510,plain,
inverse(multiply(multiply(inverse(multiply(A,B)),multiply(A,B)),C)) = inverse(multiply(multiply(inverse(multiply(D,B)),multiply(D,B)),C)),
inference(paramod,[status(thm)],[c_9,c_2146]) ).
cnf(c_2147,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(multiply(inverse(multiply(C,D)),multiply(C,D)),E))),B)))) = multiply(multiply(inverse(multiply(F,D)),multiply(F,D)),E),
inference(paramod,[status(thm)],[c_510,c_6]) ).
cnf(c_542,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(A,B)),C) = multiply(multiply(inverse(multiply(D,B)),multiply(D,B)),C),
inference(paramod,[status(thm)],[c_6,c_2147]) ).
cnf(c_2148,plain,
multiply(multiply(inverse(A),multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(C,inverse(B))),multiply(C,inverse(A))))),B)),D) = multiply(multiply(inverse(multiply(E,B)),multiply(E,B)),D),
inference(paramod,[status(thm)],[c_21,c_542]) ).
cnf(c_2149,plain,
multiply(multiply(inverse(A),A),D) = multiply(multiply(inverse(multiply(E,B)),multiply(E,B)),D),
inference(paramod,[status(thm)],[c_21,c_2148]) ).
cnf(c_551,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(A,B)),C) = multiply(multiply(inverse(D),D),C),
inference(copy,[status(thm)],[c_2149]) ).
cnf(c_2150,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(A))),multiply(B,inverse(multiply(multiply(inverse(C),C),A)))))) = multiply(inverse(multiply(D,E)),multiply(D,E)),
inference(paramod,[status(thm)],[c_551,c_9]) ).
cnf(c_2151,plain,
multiply(inverse(C),C) = multiply(inverse(multiply(D,E)),multiply(D,E)),
inference(paramod,[status(thm)],[c_9,c_2150]) ).
cnf(c_582,plain,
multiply(inverse(multiply(A,B)),multiply(A,B)) = multiply(inverse(C),C),
inference(copy,[status(thm)],[c_2151]) ).
cnf(c_585,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(A,B)),inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(multiply(E,D)))))) = E,
inference(paramod,[status(thm)],[c_551,c_9]) ).
cnf(c_2152,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(multiply(inverse(C),C),inverse(B))),D))),B))) = multiply(multiply(inverse(multiply(E,F)),multiply(E,F)),inverse(multiply(inverse(multiply(V6,inverse(C))),multiply(V6,inverse(multiply(D,C)))))),
inference(paramod,[status(thm)],[c_551,c_15]) ).
cnf(c_623,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(multiply(inverse(C),C),inverse(B))),D))),B))) = D,
inference(paramod,[status(thm)],[c_585,c_2152]) ).
cnf(c_2153,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(A,B)),inverse(multiply(multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(multiply(inverse(D),D),inverse(C))),E))),C))) = multiply(multiply(inverse(F),F),inverse(multiply(inverse(multiply(V6,inverse(D))),multiply(V6,inverse(multiply(E,D)))))),
inference(paramod,[status(thm)],[c_551,c_15]) ).
cnf(c_2154,plain,
E = multiply(multiply(inverse(F),F),inverse(multiply(inverse(multiply(V6,inverse(D))),multiply(V6,inverse(multiply(E,D)))))),
inference(paramod,[status(thm)],[c_623,c_2153]) ).
cnf(c_624,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(multiply(D,C)))))) = D,
inference(copy,[status(thm)],[c_2154]) ).
cnf(c_2155,plain,
multiply(inverse(A),multiply(B,inverse(multiply(multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(B,inverse(C))),A))),C)))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_1,c_582]) ).
cnf(c_703,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_1,c_2155]) ).
cnf(c_2156,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))),A) = multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(multiply(multiply(multiply(inverse(D),D),inverse(A)),D)))),
inference(paramod,[status(thm)],[c_582,c_7]) ).
cnf(c_707,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))),A) = A,
inference(paramod,[status(thm)],[c_6,c_2156]) ).
cnf(c_814,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,B))),C)),multiply(inverse(multiply(D,E)),multiply(D,F))) = multiply(inverse(multiply(inverse(multiply(inverse(E),V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
inference(paramod,[status(thm)],[c_582,c_137]) ).
cnf(c_884,plain,
multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(multiply(C,D)),multiply(C,E)))) = multiply(A,multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E)))),
inference(paramod,[status(thm)],[c_582,c_231]) ).
cnf(c_901,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2 ),
inference(resolve,[status(thm)],[c_703,c_3]) ).
cnf(c_902,plain,
multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(A,inverse(C))),D))),C))) = D,
inference(paramod,[status(thm)],[c_703,c_1]) ).
cnf(c_907,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(multiply(multiply(multiply(inverse(B),B),inverse(C)),B)))) = C,
inference(paramod,[status(thm)],[c_703,c_6]) ).
cnf(c_911,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(multiply(inverse(B),B),inverse(A))),C))),A) = multiply(inverse(multiply(D,inverse(E))),multiply(D,inverse(multiply(C,E)))),
inference(paramod,[status(thm)],[c_703,c_7]) ).
cnf(c_915,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(D))))),C) = D,
inference(paramod,[status(thm)],[c_703,c_21]) ).
cnf(c_918,plain,
inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,D)))),C)) = D,
inference(paramod,[status(thm)],[c_703,c_31]) ).
cnf(c_951,plain,
inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(multiply(inverse(B),B),inverse(A))),C))),A)) = inverse(multiply(inverse(multiply(D,inverse(E))),multiply(D,inverse(multiply(C,E))))),
inference(paramod,[status(thm)],[c_703,c_17]) ).
cnf(c_2157,plain,
multiply(inverse(multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(inverse(C),inverse(B))),D))),B)))),multiply(A,C)) = multiply(inverse(D),multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_703,c_52]) ).
cnf(c_1061,plain,
multiply(inverse(A),multiply(inverse(B),B)) = multiply(inverse(A),multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_52,c_2157]) ).
cnf(c_1146,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_1061,c_703]) ).
cnf(c_1234,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(multiply(D,E)),multiply(D,E)))),
inference(paramod,[status(thm)],[c_1146,c_234]) ).
cnf(c_1243,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(multiply(C,D)),multiply(C,E)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E)))),
inference(paramod,[status(thm)],[c_1146,c_221]) ).
cnf(c_1245,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E)))) = inverse(multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,B)))),
inference(paramod,[status(thm)],[c_1146,c_221]) ).
cnf(c_1265,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),F)) = multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,C))),multiply(inverse(multiply(D,V7)),F)),
inference(paramod,[status(thm)],[c_1146,c_100]) ).
cnf(c_2158,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(multiply(C,multiply(inverse(D),D))),multiply(C,E))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),V6)),B)),multiply(inverse(multiply(V7,V6)),multiply(V7,E))),
inference(paramod,[status(thm)],[c_1146,c_137]) ).
cnf(c_1273,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(inverse(multiply(V6,multiply(inverse(V7),V7))),multiply(V6,E))),
inference(copy,[status(thm)],[c_2158]) ).
cnf(c_1275,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),E)),F))) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
inference(paramod,[status(thm)],[c_1146,c_137]) ).
cnf(c_1333,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,F))) = multiply(inverse(multiply(V6,multiply(V7,C))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_1146,c_98]) ).
cnf(c_1345,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),multiply(F,multiply(inverse(C),E))),
inference(paramod,[status(thm)],[c_1146,c_98]) ).
cnf(c_1346,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(E),C))),multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),
inference(paramod,[status(thm)],[c_1146,c_98]) ).
cnf(c_1378,plain,
multiply(inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))),C)),A) = multiply(inverse(multiply(D,C)),multiply(D,A)),
inference(paramod,[status(thm)],[c_707,c_67]) ).
cnf(c_2159,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(F),F))),multiply(D,C))),E),
inference(paramod,[status(thm)],[c_707,c_83]) ).
cnf(c_1385,plain,
multiply(inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))),multiply(C,D))),A) = multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,D))),multiply(inverse(multiply(C,F)),A)),
inference(copy,[status(thm)],[c_2159]) ).
cnf(c_1389,plain,
inverse(multiply(inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))),C)),A)) = inverse(multiply(inverse(multiply(D,C)),multiply(D,A))),
inference(paramod,[status(thm)],[c_707,c_90]) ).
cnf(c_2160,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(multiply(multiply(inverse(multiply(A,E)),multiply(A,E)),inverse(multiply(inverse(F),F))),C)),multiply(A,E)),
inference(paramod,[status(thm)],[c_707,c_84]) ).
cnf(c_1397,plain,
multiply(inverse(multiply(multiply(multiply(inverse(multiply(A,B)),multiply(A,B)),inverse(multiply(inverse(C),C))),D)),multiply(A,B)) = multiply(inverse(multiply(inverse(multiply(A,E)),D)),multiply(inverse(multiply(F,E)),multiply(F,B))),
inference(copy,[status(thm)],[c_2160]) ).
cnf(c_1400,plain,
multiply(A,multiply(inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(C),C))),D)),B)) = multiply(A,multiply(inverse(multiply(E,D)),multiply(E,B))),
inference(paramod,[status(thm)],[c_707,c_163]) ).
cnf(c_1450,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))),C) = C,
inference(paramod,[status(thm)],[c_703,c_707]) ).
cnf(c_2161,plain,
multiply(A,multiply(inverse(D),B)) = multiply(A,multiply(inverse(multiply(E,D)),multiply(E,B))),
inference(paramod,[status(thm)],[c_1450,c_1400]) ).
cnf(c_1482,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(A,multiply(inverse(C),D)),
inference(copy,[status(thm)],[c_2161]) ).
cnf(c_2162,plain,
multiply(inverse(D),multiply(A,B)) = multiply(inverse(multiply(inverse(multiply(A,E)),D)),multiply(inverse(multiply(F,E)),multiply(F,B))),
inference(paramod,[status(thm)],[c_1450,c_1397]) ).
cnf(c_2163,plain,
multiply(inverse(D),multiply(A,B)) = multiply(inverse(multiply(inverse(multiply(A,E)),D)),multiply(inverse(E),B)),
inference(paramod,[status(thm)],[c_1482,c_2162]) ).
cnf(c_1483,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),D)) = multiply(inverse(C),multiply(A,D)),
inference(copy,[status(thm)],[c_2163]) ).
cnf(c_2164,plain,
inverse(multiply(inverse(C),A)) = inverse(multiply(inverse(multiply(D,C)),multiply(D,A))),
inference(paramod,[status(thm)],[c_1450,c_1389]) ).
cnf(c_1486,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = inverse(multiply(inverse(B),C)),
inference(copy,[status(thm)],[c_2164]) ).
cnf(c_2165,plain,
multiply(inverse(multiply(C,D)),A) = multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,D))),multiply(inverse(multiply(C,F)),A)),
inference(paramod,[status(thm)],[c_1450,c_1385]) ).
cnf(c_2166,plain,
multiply(inverse(multiply(C,D)),A) = multiply(inverse(multiply(inverse(F),D)),multiply(inverse(multiply(C,F)),A)),
inference(paramod,[status(thm)],[c_1486,c_2165]) ).
cnf(c_1487,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(multiply(C,A)),D)) = multiply(inverse(multiply(C,B)),D),
inference(copy,[status(thm)],[c_2166]) ).
cnf(c_2167,plain,
multiply(inverse(C),A) = multiply(inverse(multiply(D,C)),multiply(D,A)),
inference(paramod,[status(thm)],[c_1450,c_1378]) ).
cnf(c_1489,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
inference(copy,[status(thm)],[c_2167]) ).
cnf(c_2168,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),C)),D)),multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),inverse(multiply(inverse(multiply(F,inverse(V6))),multiply(F,inverse(multiply(V7,V6))))))) = multiply(inverse(multiply(multiply(inverse(V6),V6),D)),V7),
inference(paramod,[status(thm)],[c_1489,c_501]) ).
cnf(c_2169,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),C)),D)),multiply(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(multiply(F,inverse(V6))),multiply(F,inverse(multiply(V7,V6))))))) = multiply(inverse(multiply(multiply(inverse(V6),V6),D)),V7),
inference(paramod,[status(thm)],[c_1489,c_2168]) ).
cnf(c_2170,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),C)),D)),multiply(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(inverse(V6)),inverse(multiply(V7,V6)))))) = multiply(inverse(multiply(multiply(inverse(V6),V6),D)),V7),
inference(paramod,[status(thm)],[c_1489,c_2169]) ).
cnf(c_2171,plain,
multiply(inverse(D),inverse(multiply(inverse(inverse(V6)),inverse(multiply(V7,V6))))) = multiply(inverse(multiply(multiply(inverse(V6),V6),D)),V7),
inference(paramod,[status(thm)],[c_1489,c_2170]) ).
cnf(c_1492,plain,
multiply(inverse(multiply(multiply(inverse(A),A),B)),C) = multiply(inverse(B),inverse(multiply(inverse(inverse(A)),inverse(multiply(C,A))))),
inference(copy,[status(thm)],[c_2171]) ).
cnf(c_2172,plain,
multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(D),E))) = multiply(A,multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E)))),
inference(paramod,[status(thm)],[c_1489,c_884]) ).
cnf(c_2173,plain,
multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(D),E))) = multiply(A,multiply(inverse(multiply(V6,D)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_1489,c_2172]) ).
cnf(c_1516,plain,
multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),D))) = multiply(A,multiply(inverse(C),D)),
inference(paramod,[status(thm)],[c_1489,c_2173]) ).
cnf(c_2174,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7)) = multiply(inverse(multiply(V8,multiply(inverse(multiply(D,V6)),E))),multiply(V8,V7)),
inference(paramod,[status(thm)],[c_1489,c_365]) ).
cnf(c_2175,plain,
multiply(inverse(multiply(inverse(multiply(D,C)),E)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7)) = multiply(inverse(multiply(V8,multiply(inverse(multiply(D,V6)),E))),multiply(V8,V7)),
inference(paramod,[status(thm)],[c_1487,c_2174]) ).
cnf(c_2176,plain,
multiply(inverse(multiply(inverse(multiply(D,C)),E)),multiply(inverse(multiply(inverse(V6),C)),V7)) = multiply(inverse(multiply(V8,multiply(inverse(multiply(D,V6)),E))),multiply(V8,V7)),
inference(paramod,[status(thm)],[c_1489,c_2175]) ).
cnf(c_1547,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(inverse(D),B)),E)) = multiply(inverse(multiply(inverse(multiply(A,D)),C)),E),
inference(paramod,[status(thm)],[c_1489,c_2176]) ).
cnf(c_2177,plain,
inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E)))) = inverse(multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,B)))),
inference(paramod,[status(thm)],[c_1489,c_1245]) ).
cnf(c_2178,plain,
inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(E),E))) = inverse(multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,B)))),
inference(paramod,[status(thm)],[c_1516,c_2177]) ).
cnf(c_2179,plain,
inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(E),E))) = inverse(multiply(inverse(multiply(V6,C)),multiply(V6,B))),
inference(paramod,[status(thm)],[c_1489,c_2178]) ).
cnf(c_1553,plain,
inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))) = inverse(multiply(inverse(B),A)),
inference(paramod,[status(thm)],[c_1489,c_2179]) ).
cnf(c_2180,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(multiply(D,E)),multiply(D,F))) = multiply(inverse(multiply(inverse(multiply(inverse(E),V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
inference(paramod,[status(thm)],[c_1489,c_814]) ).
cnf(c_2181,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(E),F)) = multiply(inverse(multiply(inverse(multiply(inverse(E),V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
inference(paramod,[status(thm)],[c_1489,c_2180]) ).
cnf(c_2182,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(E),F)) = multiply(inverse(multiply(inverse(multiply(inverse(E),V6)),C)),multiply(inverse(V6),F)),
inference(paramod,[status(thm)],[c_1489,c_2181]) ).
cnf(c_1558,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(C),D)) = multiply(inverse(B),multiply(inverse(C),D)),
inference(paramod,[status(thm)],[c_1483,c_2182]) ).
cnf(c_2183,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),C)),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),inverse(multiply(multiply(multiply(inverse(D),D),inverse(F)),D)))) = F,
inference(paramod,[status(thm)],[c_1489,c_116]) ).
cnf(c_2184,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),C)),inverse(D))),multiply(inverse(multiply(inverse(B),C)),inverse(multiply(multiply(multiply(inverse(D),D),inverse(F)),D)))) = F,
inference(paramod,[status(thm)],[c_1489,c_2183]) ).
cnf(c_1563,plain,
multiply(inverse(inverse(A)),inverse(multiply(multiply(multiply(inverse(A),A),inverse(B)),A))) = B,
inference(paramod,[status(thm)],[c_1489,c_2184]) ).
cnf(c_2185,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(C,D)),multiply(C,E)))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E)))),
inference(paramod,[status(thm)],[c_1553,c_1243]) ).
cnf(c_2186,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(D),E))) = inverse(multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E)))),
inference(paramod,[status(thm)],[c_1489,c_2185]) ).
cnf(c_2187,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(D),E))) = inverse(multiply(inverse(multiply(V6,D)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_1489,c_2186]) ).
cnf(c_1569,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C))) = inverse(multiply(inverse(B),C)),
inference(paramod,[status(thm)],[c_1489,c_2187]) ).
cnf(c_2188,plain,
multiply(A,inverse(multiply(inverse(C),C))) = multiply(A,inverse(multiply(inverse(multiply(D,E)),multiply(D,E)))),
inference(paramod,[status(thm)],[c_1569,c_1234]) ).
cnf(c_1574,plain,
multiply(A,inverse(multiply(inverse(B),B))) = multiply(A,inverse(multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_1489,c_2188]) ).
cnf(c_1579,plain,
inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(B)),C))),B)) = C,
inference(paramod,[status(thm)],[c_1489,c_918]) ).
cnf(c_1580,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(B)),inverse(C)))),B) = C,
inference(paramod,[status(thm)],[c_1489,c_915]) ).
cnf(c_1582,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(B)),inverse(multiply(C,B))))) = C,
inference(paramod,[status(thm)],[c_1489,c_624]) ).
cnf(c_2189,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(C)),inverse(multiply(D,C)))))),multiply(A,E)) = multiply(inverse(D),multiply(multiply(inverse(C),C),E)),
inference(paramod,[status(thm)],[c_1489,c_56]) ).
cnf(c_1597,plain,
multiply(inverse(inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A))))),C) = multiply(inverse(B),multiply(multiply(inverse(A),A),C)),
inference(paramod,[status(thm)],[c_1489,c_2189]) ).
cnf(c_2190,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(E),C))),multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),
inference(paramod,[status(thm)],[c_1489,c_1346]) ).
cnf(c_2191,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),E)) = multiply(inverse(multiply(F,multiply(inverse(E),C))),multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),
inference(paramod,[status(thm)],[c_1489,c_2190]) ).
cnf(c_2192,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(E),C))),multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),
inference(paramod,[status(thm)],[c_1489,c_2191]) ).
cnf(c_2193,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(E),C))),multiply(F,multiply(inverse(V7),V7))),
inference(paramod,[status(thm)],[c_1516,c_2192]) ).
cnf(c_2194,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(inverse(E),C)),multiply(inverse(V7),V7)),
inference(paramod,[status(thm)],[c_1489,c_2193]) ).
cnf(c_1601,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(B),A),
inference(copy,[status(thm)],[c_2194]) ).
cnf(c_2195,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),multiply(F,multiply(inverse(C),E))),
inference(paramod,[status(thm)],[c_1489,c_1345]) ).
cnf(c_2196,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),E)) = multiply(inverse(multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),multiply(F,multiply(inverse(C),E))),
inference(paramod,[status(thm)],[c_1489,c_2195]) ).
cnf(c_2197,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(V7),V7)))),multiply(F,multiply(inverse(C),E))),
inference(paramod,[status(thm)],[c_1489,c_2196]) ).
cnf(c_2198,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
inference(paramod,[status(thm)],[c_1601,c_2197]) ).
cnf(c_2199,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(C),E)),
inference(paramod,[status(thm)],[c_1489,c_2198]) ).
cnf(c_1602,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(B),C),
inference(copy,[status(thm)],[c_2199]) ).
cnf(c_2200,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,F))) = multiply(inverse(multiply(V6,multiply(V7,C))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_1602,c_1333]) ).
cnf(c_2201,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(multiply(inverse(E),E)),F)) = multiply(inverse(multiply(V6,multiply(V7,C))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_1489,c_2200]) ).
cnf(c_2202,plain,
multiply(inverse(C),multiply(inverse(multiply(inverse(E),E)),F)) = multiply(inverse(multiply(V6,multiply(V7,C))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_1558,c_2201]) ).
cnf(c_2203,plain,
multiply(inverse(C),multiply(inverse(multiply(inverse(E),E)),F)) = multiply(inverse(multiply(V7,C)),multiply(V7,F)),
inference(paramod,[status(thm)],[c_1489,c_2202]) ).
cnf(c_1604,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(B),B)),C)) = multiply(inverse(A),C),
inference(paramod,[status(thm)],[c_1489,c_2203]) ).
cnf(c_2204,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),multiply(inverse(multiply(inverse(D),D)),F)) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
inference(paramod,[status(thm)],[c_1604,c_1275]) ).
cnf(c_2205,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),F) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
inference(paramod,[status(thm)],[c_1604,c_2204]) ).
cnf(c_2206,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),F) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(V6),F)),
inference(paramod,[status(thm)],[c_1489,c_2205]) ).
cnf(c_1605,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),D) = multiply(inverse(C),multiply(A,D)),
inference(paramod,[status(thm)],[c_1483,c_2206]) ).
cnf(c_2207,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),C)),multiply(inverse(B),E)) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(inverse(multiply(V6,multiply(inverse(V7),V7))),multiply(V6,E))),
inference(paramod,[status(thm)],[c_1489,c_1273]) ).
cnf(c_2208,plain,
multiply(inverse(C),multiply(inverse(multiply(inverse(A),A)),E)) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(inverse(multiply(V6,multiply(inverse(V7),V7))),multiply(V6,E))),
inference(paramod,[status(thm)],[c_1483,c_2207]) ).
cnf(c_2209,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(inverse(multiply(V6,multiply(inverse(V7),V7))),multiply(V6,E))),
inference(paramod,[status(thm)],[c_1604,c_2208]) ).
cnf(c_2210,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(inverse(multiply(inverse(V7),V7)),E)),
inference(paramod,[status(thm)],[c_1489,c_2209]) ).
cnf(c_2211,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),E),
inference(paramod,[status(thm)],[c_1604,c_2210]) ).
cnf(c_1606,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),C) = multiply(inverse(B),C),
inference(copy,[status(thm)],[c_2211]) ).
cnf(c_2212,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),inverse(multiply(multiply(multiply(inverse(E),E),inverse(F)),E)))) = multiply(inverse(multiply(inverse(multiply(A,inverse(E))),C)),F),
inference(paramod,[status(thm)],[c_1489,c_130]) ).
cnf(c_1614,plain,
multiply(inverse(A),multiply(B,inverse(multiply(multiply(multiply(inverse(C),C),inverse(D)),C)))) = multiply(inverse(multiply(inverse(multiply(B,inverse(C))),A)),D),
inference(paramod,[status(thm)],[c_1483,c_2212]) ).
cnf(c_2213,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),C)),multiply(inverse(multiply(D,multiply(inverse(E),E))),F)) = multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,C))),multiply(inverse(multiply(D,V7)),F)),
inference(paramod,[status(thm)],[c_1604,c_1265]) ).
cnf(c_2214,plain,
multiply(inverse(C),multiply(inverse(multiply(D,multiply(inverse(E),E))),F)) = multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,C))),multiply(inverse(multiply(D,V7)),F)),
inference(paramod,[status(thm)],[c_1606,c_2213]) ).
cnf(c_2215,plain,
multiply(inverse(C),multiply(inverse(multiply(D,multiply(inverse(E),E))),F)) = multiply(inverse(multiply(inverse(V7),C)),multiply(inverse(multiply(D,V7)),F)),
inference(paramod,[status(thm)],[c_1489,c_2214]) ).
cnf(c_1616,plain,
multiply(inverse(A),multiply(inverse(multiply(B,multiply(inverse(C),C))),D)) = multiply(inverse(multiply(B,A)),D),
inference(paramod,[status(thm)],[c_1487,c_2215]) ).
cnf(c_2216,plain,
multiply(inverse(multiply(inverse(B),inverse(multiply(multiply(multiply(inverse(C),C),D),C)))),multiply(inverse(multiply(E,B)),F)) = multiply(D,multiply(inverse(multiply(E,inverse(C))),F)),
inference(paramod,[status(thm)],[c_1489,c_363]) ).
cnf(c_1619,plain,
multiply(inverse(multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),C),B)))),D) = multiply(C,multiply(inverse(multiply(A,inverse(B))),D)),
inference(paramod,[status(thm)],[c_1487,c_2216]) ).
cnf(c_2217,plain,
inverse(multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(A)),inverse(multiply(inverse(inverse(B)),inverse(multiply(C,B))))))),A)) = inverse(multiply(inverse(multiply(D,inverse(E))),multiply(D,inverse(multiply(C,E))))),
inference(paramod,[status(thm)],[c_1492,c_951]) ).
cnf(c_2218,plain,
inverse(multiply(inverse(inverse(B)),inverse(multiply(C,B)))) = inverse(multiply(inverse(multiply(D,inverse(E))),multiply(D,inverse(multiply(C,E))))),
inference(paramod,[status(thm)],[c_1580,c_2217]) ).
cnf(c_1624,plain,
inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A)))) = inverse(multiply(inverse(inverse(C)),inverse(multiply(B,C)))),
inference(paramod,[status(thm)],[c_1489,c_2218]) ).
cnf(c_2219,plain,
multiply(multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(A)),inverse(multiply(inverse(inverse(B)),inverse(multiply(C,B))))))),A) = multiply(inverse(multiply(D,inverse(E))),multiply(D,inverse(multiply(C,E)))),
inference(paramod,[status(thm)],[c_1492,c_911]) ).
cnf(c_2220,plain,
multiply(inverse(inverse(B)),inverse(multiply(C,B))) = multiply(inverse(multiply(D,inverse(E))),multiply(D,inverse(multiply(C,E)))),
inference(paramod,[status(thm)],[c_1580,c_2219]) ).
cnf(c_1626,plain,
multiply(inverse(inverse(A)),inverse(multiply(B,A))) = multiply(inverse(inverse(C)),inverse(multiply(B,C))),
inference(paramod,[status(thm)],[c_1489,c_2220]) ).
cnf(c_1635,plain,
multiply(inverse(multiply(inverse(A),A)),B) = B,
inference(paramod,[status(thm)],[c_1563,c_907]) ).
cnf(c_1645,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_1574,c_703]) ).
cnf(c_2221,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,C)) = multiply(inverse(inverse(multiply(inverse(D),D))),C),
inference(paramod,[status(thm)],[c_1574,c_1489]) ).
cnf(c_1650,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),B) = multiply(inverse(inverse(multiply(inverse(C),C))),B),
inference(paramod,[status(thm)],[c_1489,c_2221]) ).
cnf(c_1656,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B))) = multiply(inverse(inverse(C)),inverse(multiply(inverse(A),C))),
inference(paramod,[status(thm)],[c_703,c_1626]) ).
cnf(c_1659,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A)))),multiply(inverse(inverse(C)),D)) = multiply(inverse(inverse(multiply(B,C))),D),
inference(paramod,[status(thm)],[c_1626,c_1489]) ).
cnf(c_2222,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),multiply(inverse(multiply(inverse(D),E)),F)) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(multiply(inverse(multiply(inverse(E),D)),V6)),F)),
inference(paramod,[status(thm)],[c_1601,c_283]) ).
cnf(c_2223,plain,
multiply(inverse(C),multiply(A,multiply(inverse(multiply(inverse(D),E)),F))) = multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(multiply(inverse(multiply(inverse(E),D)),V6)),F)),
inference(paramod,[status(thm)],[c_1605,c_2222]) ).
cnf(c_2224,plain,
multiply(inverse(C),multiply(A,multiply(inverse(multiply(inverse(D),E)),F))) = multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(E),D))),C)),F),
inference(paramod,[status(thm)],[c_1547,c_2223]) ).
cnf(c_1665,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),C))),D)),E) = multiply(inverse(D),multiply(A,multiply(inverse(multiply(inverse(C),B)),E))),
inference(copy,[status(thm)],[c_2224]) ).
cnf(c_2225,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A)))),multiply(inverse(C),C)) = multiply(inverse(inverse(multiply(B,D))),inverse(D)),
inference(paramod,[status(thm)],[c_1626,c_1601]) ).
cnf(c_1668,plain,
multiply(inverse(inverse(multiply(A,B))),inverse(B)) = multiply(inverse(inverse(multiply(A,C))),inverse(C)),
inference(paramod,[status(thm)],[c_1601,c_2225]) ).
cnf(c_2226,plain,
multiply(inverse(multiply(A,B)),inverse(multiply(multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(D),D))),inverse(C))),multiply(inverse(multiply(inverse(E),F)),V6)))),C))) = multiply(inverse(multiply(inverse(multiply(inverse(F),E)),B)),V6),
inference(paramod,[status(thm)],[c_1601,c_312]) ).
cnf(c_2227,plain,
multiply(inverse(multiply(A,B)),inverse(multiply(multiply(multiply(inverse(C),C),inverse(multiply(inverse(inverse(C)),multiply(A,multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),F)),V6)))))),C))) = multiply(inverse(multiply(inverse(multiply(inverse(F),E)),B)),V6),
inference(paramod,[status(thm)],[c_1665,c_2226]) ).
cnf(c_2228,plain,
multiply(inverse(multiply(A,B)),inverse(multiply(multiply(multiply(inverse(C),C),inverse(multiply(inverse(inverse(C)),multiply(A,multiply(inverse(multiply(inverse(E),F)),V6))))),C))) = multiply(inverse(multiply(inverse(multiply(inverse(F),E)),B)),V6),
inference(paramod,[status(thm)],[c_1635,c_2227]) ).
cnf(c_2229,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(inverse(multiply(inverse(E),F)),V6))) = multiply(inverse(multiply(inverse(multiply(inverse(F),E)),B)),V6),
inference(paramod,[status(thm)],[c_1579,c_2228]) ).
cnf(c_2230,plain,
multiply(inverse(B),multiply(inverse(multiply(inverse(E),F)),V6)) = multiply(inverse(multiply(inverse(multiply(inverse(F),E)),B)),V6),
inference(paramod,[status(thm)],[c_1489,c_2229]) ).
cnf(c_1681,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),B)),C)),D) = multiply(inverse(C),multiply(inverse(multiply(inverse(B),A)),D)),
inference(copy,[status(thm)],[c_2230]) ).
cnf(c_1707,plain,
multiply(inverse(inverse(multiply(inverse(inverse(multiply(A,B))),inverse(B)))),inverse(inverse(C))) = multiply(inverse(inverse(multiply(inverse(inverse(multiply(A,C))),D))),inverse(D)),
inference(paramod,[status(thm)],[c_1668,c_1668]) ).
cnf(c_2231,plain,
inverse(multiply(inverse(inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A))))),inverse(multiply(C,multiply(inverse(inverse(D)),inverse(multiply(B,D))))))) = inverse(multiply(inverse(inverse(E)),inverse(multiply(C,E)))),
inference(paramod,[status(thm)],[c_1624,c_1624]) ).
cnf(c_2232,plain,
inverse(multiply(inverse(B),multiply(multiply(inverse(A),A),inverse(multiply(C,multiply(inverse(inverse(D)),inverse(multiply(B,D)))))))) = inverse(multiply(inverse(inverse(E)),inverse(multiply(C,E)))),
inference(paramod,[status(thm)],[c_1597,c_2231]) ).
cnf(c_1731,plain,
inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A)))) = inverse(multiply(inverse(C),multiply(multiply(inverse(D),D),inverse(multiply(B,multiply(inverse(inverse(E)),inverse(multiply(C,E)))))))),
inference(copy,[status(thm)],[c_2232]) ).
cnf(c_2233,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(inverse(B),A)))),C)),multiply(inverse(multiply(D,inverse(multiply(inverse(E),E)))),F)) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),V6)),C)),multiply(inverse(multiply(D,V6)),F)),
inference(paramod,[status(thm)],[c_1656,c_283]) ).
cnf(c_2234,plain,
multiply(inverse(C),multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),A))),inverse(A))),multiply(inverse(multiply(D,inverse(multiply(inverse(E),E)))),F))) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),V6)),C)),multiply(inverse(multiply(D,V6)),F)),
inference(paramod,[status(thm)],[c_1681,c_2233]) ).
cnf(c_2235,plain,
multiply(inverse(C),multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),A))),inverse(A))),multiply(inverse(multiply(D,inverse(multiply(inverse(E),E)))),F))) = multiply(inverse(C),multiply(inverse(multiply(inverse(V6),inverse(B))),multiply(inverse(multiply(D,V6)),F))),
inference(paramod,[status(thm)],[c_1681,c_2234]) ).
cnf(c_1739,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C))),multiply(inverse(multiply(D,inverse(multiply(inverse(E),E)))),F))) = multiply(inverse(A),multiply(inverse(multiply(D,inverse(B))),F)),
inference(paramod,[status(thm)],[c_1487,c_2235]) ).
cnf(c_1745,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B)))),multiply(inverse(inverse(C)),D)) = multiply(inverse(inverse(multiply(inverse(A),C))),D),
inference(paramod,[status(thm)],[c_1656,c_1489]) ).
cnf(c_1746,plain,
multiply(inverse(multiply(inverse(inverse(A)),B)),multiply(inverse(inverse(C)),inverse(multiply(inverse(D),D)))) = multiply(inverse(B),inverse(multiply(inverse(C),A))),
inference(paramod,[status(thm)],[c_1656,c_1489]) ).
cnf(c_1758,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(A),A))),B)),multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C)))),E)) = multiply(inverse(multiply(inverse(inverse(D)),B)),E),
inference(paramod,[status(thm)],[c_1656,c_1487]) ).
cnf(c_1766,plain,
multiply(inverse(inverse(inverse(multiply(A,B)))),inverse(multiply(inverse(C),C))) = multiply(inverse(inverse(inverse(B))),inverse(multiply(inverse(inverse(multiply(A,D))),inverse(D)))),
inference(paramod,[status(thm)],[c_1668,c_1656]) ).
cnf(c_1800,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),inverse(multiply(C,inverse(multiply(inverse(D),D))))))) = C,
inference(paramod,[status(thm)],[c_1574,c_1582]) ).
cnf(c_1803,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(C),D))))) = inverse(multiply(inverse(D),C)),
inference(paramod,[status(thm)],[c_1601,c_1582]) ).
cnf(c_2236,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(multiply(inverse(inverse(B)),inverse(multiply(C,B))))),inverse(multiply(D,multiply(inverse(inverse(E)),inverse(multiply(C,E)))))))) = D,
inference(paramod,[status(thm)],[c_1624,c_1582]) ).
cnf(c_1809,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),multiply(multiply(inverse(C),C),inverse(multiply(D,multiply(inverse(inverse(E)),inverse(multiply(B,E))))))))) = D,
inference(paramod,[status(thm)],[c_1597,c_2236]) ).
cnf(c_1810,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C))))))) = inverse(inverse(D)),
inference(paramod,[status(thm)],[c_1656,c_1582]) ).
cnf(c_1813,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),B))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_1645,c_1582]) ).
cnf(c_1815,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(inverse(multiply(inverse(inverse(B)),inverse(multiply(C,B)))))),inverse(C)))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_1582,c_1582]) ).
cnf(c_2237,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(A),A))),B)),multiply(inverse(inverse(multiply(inverse(C),C))),D)) = multiply(inverse(multiply(multiply(inverse(E),E),B)),D),
inference(paramod,[status(thm)],[c_1813,c_1487]) ).
cnf(c_1827,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(A),A))),B)),multiply(inverse(inverse(multiply(inverse(C),C))),D)) = multiply(inverse(B),inverse(multiply(inverse(inverse(E)),inverse(multiply(D,E))))),
inference(paramod,[status(thm)],[c_1492,c_2237]) ).
cnf(c_2238,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(multiply(inverse(B),B),inverse(multiply(inverse(C),C)))),inverse(multiply(D,multiply(inverse(E),E)))))) = D,
inference(paramod,[status(thm)],[c_1813,c_1582]) ).
cnf(c_2239,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(inverse(B)),inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),B))))))) = D,
inference(paramod,[status(thm)],[c_1492,c_2238]) ).
cnf(c_1839,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C))),inverse(C))) = A,
inference(paramod,[status(thm)],[c_1803,c_2239]) ).
cnf(c_2240,plain,
multiply(inverse(multiply(A,B)),C) = multiply(inverse(B),inverse(multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(multiply(A,inverse(E))),C))),E))),
inference(paramod,[status(thm)],[c_902,c_1489]) ).
cnf(c_1845,plain,
multiply(inverse(A),inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(C,inverse(D))),E))),D))) = multiply(inverse(multiply(C,A)),E),
inference(copy,[status(thm)],[c_2240]) ).
cnf(c_1855,plain,
multiply(inverse(inverse(A)),inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),D)))),E))),multiply(inverse(C),A)))) = E,
inference(paramod,[status(thm)],[c_1656,c_902]) ).
cnf(c_1858,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),D))),multiply(inverse(E),E)))) = D,
inference(paramod,[status(thm)],[c_1813,c_902]) ).
cnf(c_1860,plain,
multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(C)),D))) = inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(D))),inverse(F))),C))),F)),
inference(paramod,[status(thm)],[c_902,c_902]) ).
cnf(c_1866,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(A),A))),B)),multiply(inverse(inverse(multiply(inverse(C),C))),D)) = multiply(inverse(B),D),
inference(paramod,[status(thm)],[c_1650,c_1489]) ).
cnf(c_2241,plain,
multiply(inverse(B),D) = multiply(inverse(B),inverse(multiply(inverse(inverse(E)),inverse(multiply(D,E))))),
inference(paramod,[status(thm)],[c_1866,c_1827]) ).
cnf(c_1875,plain,
multiply(inverse(A),inverse(multiply(inverse(inverse(B)),inverse(multiply(C,B))))) = multiply(inverse(A),C),
inference(copy,[status(thm)],[c_2241]) ).
cnf(c_1876,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),inverse(C)))) = inverse(inverse(C)),
inference(paramod,[status(thm)],[c_1875,c_1810]) ).
cnf(c_1887,plain,
multiply(inverse(multiply(multiply(inverse(A),A),B)),C) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_1875,c_1492]) ).
cnf(c_1889,plain,
inverse(inverse(multiply(A,inverse(multiply(inverse(B),B))))) = A,
inference(paramod,[status(thm)],[c_1876,c_1800]) ).
cnf(c_2242,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(inverse(C)),D))),C))) = D,
inference(paramod,[status(thm)],[c_1887,c_902]) ).
cnf(c_1901,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_1579,c_2242]) ).
cnf(c_2243,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(inverse(E)),inverse(multiply(B,E)))))))) = D,
inference(paramod,[status(thm)],[c_1901,c_1809]) ).
cnf(c_1906,plain,
inverse(multiply(inverse(A),inverse(multiply(B,multiply(inverse(inverse(C)),inverse(multiply(A,C))))))) = B,
inference(paramod,[status(thm)],[c_1901,c_2243]) ).
cnf(c_2244,plain,
inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A)))) = inverse(multiply(inverse(C),inverse(multiply(B,multiply(inverse(inverse(E)),inverse(multiply(C,E))))))),
inference(paramod,[status(thm)],[c_1901,c_1731]) ).
cnf(c_1909,plain,
inverse(multiply(inverse(inverse(A)),inverse(multiply(B,A)))) = B,
inference(paramod,[status(thm)],[c_1906,c_2244]) ).
cnf(c_2245,plain,
multiply(A,inverse(multiply(inverse(C),D))) = inverse(multiply(multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(D))),inverse(F))),C))),F)),
inference(paramod,[status(thm)],[c_1901,c_1860]) ).
cnf(c_2246,plain,
multiply(A,inverse(multiply(inverse(C),D))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(D))),inverse(F))),C)),F)),
inference(paramod,[status(thm)],[c_1901,c_2245]) ).
cnf(c_2247,plain,
multiply(A,inverse(multiply(inverse(C),D))) = inverse(multiply(inverse(C),multiply(inverse(multiply(inverse(inverse(F)),multiply(A,inverse(D)))),F))),
inference(paramod,[status(thm)],[c_1681,c_2246]) ).
cnf(c_1918,plain,
inverse(multiply(inverse(A),multiply(inverse(multiply(inverse(inverse(B)),multiply(C,inverse(D)))),B))) = multiply(C,inverse(multiply(inverse(A),D))),
inference(copy,[status(thm)],[c_2247]) ).
cnf(c_2248,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(C),C))),D)),multiply(inverse(E),E)))) = D,
inference(paramod,[status(thm)],[c_1901,c_1858]) ).
cnf(c_2249,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(D),inverse(multiply(inverse(C),C))))) = D,
inference(paramod,[status(thm)],[c_1601,c_2248]) ).
cnf(c_1920,plain,
inverse(multiply(inverse(A),inverse(multiply(inverse(B),B)))) = A,
inference(paramod,[status(thm)],[c_1901,c_2249]) ).
cnf(c_2250,plain,
multiply(inverse(inverse(A)),inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(C),E))),multiply(inverse(C),A)))) = E,
inference(paramod,[status(thm)],[c_1920,c_1855]) ).
cnf(c_2251,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(multiply(inverse(C),E)),multiply(inverse(C),A)))) = E,
inference(paramod,[status(thm)],[c_1901,c_2250]) ).
cnf(c_1923,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(B),A))) = B,
inference(paramod,[status(thm)],[c_1489,c_2251]) ).
cnf(c_1929,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(multiply(B,inverse(C))),D)),C))) = multiply(inverse(multiply(B,A)),D),
inference(paramod,[status(thm)],[c_1901,c_1845]) ).
cnf(c_2252,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(inverse(C)),inverse(C)))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_1909,c_1815]) ).
cnf(c_2253,plain,
inverse(multiply(inverse(inverse(C)),inverse(C))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_1901,c_2252]) ).
cnf(c_1931,plain,
multiply(inverse(A),A) = inverse(multiply(inverse(inverse(B)),inverse(B))),
inference(copy,[status(thm)],[c_2253]) ).
cnf(c_1945,plain,
multiply(inverse(multiply(A,inverse(multiply(B,C)))),D) = multiply(B,multiply(inverse(multiply(A,inverse(C))),D)),
inference(paramod,[status(thm)],[c_1901,c_1619]) ).
cnf(c_2254,plain,
multiply(inverse(A),multiply(B,inverse(multiply(inverse(D),C)))) = multiply(inverse(multiply(inverse(multiply(B,inverse(C))),A)),D),
inference(paramod,[status(thm)],[c_1901,c_1614]) ).
cnf(c_1946,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),C)),D) = multiply(inverse(C),multiply(A,inverse(multiply(inverse(D),B)))),
inference(copy,[status(thm)],[c_2254]) ).
cnf(c_2255,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_1901,c_901]) ).
cnf(c_1957,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(copy,[status(thm)],[c_2255]) ).
cnf(c_2256,plain,
multiply(inverse(A),multiply(inverse(inverse(C)),D)) = multiply(inverse(inverse(multiply(inverse(A),C))),D),
inference(paramod,[status(thm)],[c_1920,c_1745]) ).
cnf(c_1959,plain,
multiply(inverse(inverse(multiply(inverse(A),B))),C) = multiply(inverse(A),multiply(inverse(inverse(B)),C)),
inference(copy,[status(thm)],[c_2256]) ).
cnf(c_2257,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(inverse(A)),B))),multiply(inverse(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C)))),E)) = multiply(inverse(multiply(inverse(inverse(D)),B)),E),
inference(paramod,[status(thm)],[c_1959,c_1758]) ).
cnf(c_1961,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(inverse(A)),B))),multiply(inverse(C),D)) = multiply(inverse(multiply(inverse(inverse(C)),B)),D),
inference(paramod,[status(thm)],[c_1923,c_2257]) ).
cnf(c_2258,plain,
multiply(B,multiply(inverse(inverse(C)),D)) = multiply(inverse(inverse(multiply(B,C))),D),
inference(paramod,[status(thm)],[c_1909,c_1659]) ).
cnf(c_1968,plain,
multiply(inverse(inverse(multiply(A,B))),C) = multiply(A,multiply(inverse(inverse(B)),C)),
inference(copy,[status(thm)],[c_2258]) ).
cnf(c_1979,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_1923,c_1656]) ).
cnf(c_2259,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(B),multiply(inverse(inverse(C)),inverse(C)))),multiply(inverse(multiply(D,inverse(multiply(inverse(E),E)))),F))) = multiply(inverse(A),multiply(inverse(multiply(D,inverse(B))),F)),
inference(paramod,[status(thm)],[c_1968,c_1739]) ).
cnf(c_2260,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(B),multiply(inverse(inverse(C)),inverse(C)))),multiply(inverse(E),multiply(inverse(multiply(D,inverse(E))),F)))) = multiply(inverse(A),multiply(inverse(multiply(D,inverse(B))),F)),
inference(paramod,[status(thm)],[c_1945,c_2259]) ).
cnf(c_1983,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),multiply(inverse(multiply(D,inverse(C))),E))) = multiply(inverse(B),multiply(inverse(multiply(D,inverse(A))),E)),
inference(paramod,[status(thm)],[c_1616,c_2260]) ).
cnf(c_1988,plain,
multiply(inverse(A),inverse(multiply(inverse(B),multiply(C,inverse(multiply(inverse(D),D)))))) = multiply(inverse(multiply(C,A)),B),
inference(paramod,[status(thm)],[c_1946,c_1929]) ).
cnf(c_1991,plain,
multiply(inverse(multiply(inverse(inverse(A)),B)),C) = multiply(inverse(B),inverse(multiply(inverse(C),A))),
inference(paramod,[status(thm)],[c_1979,c_1746]) ).
cnf(c_1998,plain,
inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(inverse(inverse(C)),inverse(C)))) = A,
inference(paramod,[status(thm)],[c_1968,c_1839]) ).
cnf(c_2261,plain,
multiply(inverse(inverse(multiply(A,multiply(inverse(inverse(B)),inverse(B))))),inverse(inverse(C))) = multiply(inverse(inverse(multiply(inverse(inverse(multiply(A,C))),D))),inverse(D)),
inference(paramod,[status(thm)],[c_1968,c_1707]) ).
cnf(c_2262,plain,
multiply(A,multiply(inverse(inverse(multiply(inverse(inverse(B)),inverse(B)))),inverse(inverse(C)))) = multiply(inverse(inverse(multiply(inverse(inverse(multiply(A,C))),D))),inverse(D)),
inference(paramod,[status(thm)],[c_1968,c_2261]) ).
cnf(c_2263,plain,
multiply(A,multiply(inverse(inverse(B)),multiply(inverse(inverse(inverse(B))),inverse(inverse(C))))) = multiply(inverse(inverse(multiply(inverse(inverse(multiply(A,C))),D))),inverse(D)),
inference(paramod,[status(thm)],[c_1968,c_2262]) ).
cnf(c_2264,plain,
multiply(A,multiply(inverse(inverse(B)),multiply(inverse(inverse(inverse(B))),inverse(inverse(C))))) = multiply(inverse(inverse(multiply(A,multiply(inverse(inverse(C)),D)))),inverse(D)),
inference(paramod,[status(thm)],[c_1968,c_2263]) ).
cnf(c_2265,plain,
multiply(A,multiply(inverse(inverse(B)),multiply(inverse(inverse(inverse(B))),inverse(inverse(C))))) = multiply(A,multiply(inverse(inverse(multiply(inverse(inverse(C)),D))),inverse(D))),
inference(paramod,[status(thm)],[c_1968,c_2264]) ).
cnf(c_2001,plain,
multiply(A,multiply(inverse(inverse(B)),multiply(inverse(inverse(inverse(B))),inverse(inverse(C))))) = multiply(A,multiply(inverse(inverse(C)),multiply(inverse(inverse(D)),inverse(D)))),
inference(paramod,[status(thm)],[c_1968,c_2265]) ).
cnf(c_2266,plain,
inverse(multiply(A,B)) = multiply(inverse(inverse(inverse(B))),inverse(multiply(inverse(inverse(multiply(A,D))),inverse(D)))),
inference(paramod,[status(thm)],[c_1979,c_1766]) ).
cnf(c_2267,plain,
inverse(multiply(A,B)) = multiply(inverse(inverse(inverse(B))),inverse(multiply(A,multiply(inverse(inverse(D)),inverse(D))))),
inference(paramod,[status(thm)],[c_1968,c_2266]) ).
cnf(c_2009,plain,
multiply(inverse(inverse(inverse(A))),inverse(multiply(B,multiply(inverse(inverse(C)),inverse(C))))) = inverse(multiply(B,A)),
inference(copy,[status(thm)],[c_2267]) ).
cnf(c_2016,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(inverse(A)),B))),multiply(inverse(C),D)) = multiply(inverse(B),inverse(multiply(inverse(D),C))),
inference(paramod,[status(thm)],[c_1991,c_1961]) ).
cnf(c_2019,plain,
inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(C))),inverse(multiply(inverse(D),D))))) = multiply(B,inverse(multiply(inverse(A),C))),
inference(paramod,[status(thm)],[c_1991,c_1918]) ).
cnf(c_2268,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(A)),inverse(A)))),B)),multiply(inverse(multiply(C,D)),E)) = multiply(inverse(multiply(inverse(multiply(inverse(D),F)),B)),multiply(inverse(multiply(C,F)),E)),
inference(paramod,[status(thm)],[c_1931,c_283]) ).
cnf(c_2269,plain,
multiply(inverse(multiply(inverse(inverse(A)),multiply(inverse(inverse(inverse(A))),B))),multiply(inverse(multiply(C,D)),E)) = multiply(inverse(multiply(inverse(multiply(inverse(D),F)),B)),multiply(inverse(multiply(C,F)),E)),
inference(paramod,[status(thm)],[c_1968,c_2268]) ).
cnf(c_2270,plain,
multiply(inverse(B),inverse(multiply(inverse(E),multiply(C,D)))) = multiply(inverse(multiply(inverse(multiply(inverse(D),F)),B)),multiply(inverse(multiply(C,F)),E)),
inference(paramod,[status(thm)],[c_2016,c_2269]) ).
cnf(c_2271,plain,
multiply(inverse(B),inverse(multiply(inverse(E),multiply(C,D)))) = multiply(inverse(B),multiply(inverse(multiply(inverse(F),D)),multiply(inverse(multiply(C,F)),E))),
inference(paramod,[status(thm)],[c_1681,c_2270]) ).
cnf(c_2045,plain,
multiply(inverse(A),inverse(multiply(inverse(B),multiply(C,D)))) = multiply(inverse(A),multiply(inverse(multiply(C,D)),B)),
inference(paramod,[status(thm)],[c_1487,c_2271]) ).
cnf(c_2272,plain,
multiply(inverse(inverse(multiply(inverse(inverse(A)),inverse(A)))),B) = B,
inference(paramod,[status(thm)],[c_1931,c_1635]) ).
cnf(c_2051,plain,
multiply(inverse(inverse(A)),multiply(inverse(inverse(inverse(A))),B)) = B,
inference(paramod,[status(thm)],[c_1968,c_2272]) ).
cnf(c_2273,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(inverse(C)),inverse(C)))))) = B,
inference(paramod,[status(thm)],[c_1931,c_1909]) ).
cnf(c_2064,plain,
inverse(inverse(multiply(A,multiply(inverse(inverse(B)),inverse(B))))) = A,
inference(paramod,[status(thm)],[c_1635,c_2273]) ).
cnf(c_2066,plain,
multiply(inverse(inverse(A)),multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_1931,c_1979]) ).
cnf(c_2274,plain,
multiply(inverse(A),multiply(inverse(multiply(C,inverse(multiply(inverse(D),D)))),B)) = multiply(inverse(multiply(C,A)),B),
inference(paramod,[status(thm)],[c_2045,c_1988]) ).
cnf(c_2069,plain,
multiply(inverse(A),multiply(inverse(B),multiply(inverse(multiply(C,inverse(B))),D))) = multiply(inverse(multiply(C,A)),D),
inference(paramod,[status(thm)],[c_1945,c_2274]) ).
cnf(c_2275,plain,
multiply(A,inverse(inverse(C))) = multiply(A,multiply(inverse(inverse(C)),multiply(inverse(inverse(D)),inverse(D)))),
inference(paramod,[status(thm)],[c_2051,c_2001]) ).
cnf(c_2071,plain,
multiply(A,inverse(inverse(B))) = multiply(A,B),
inference(paramod,[status(thm)],[c_2066,c_2275]) ).
cnf(c_2072,plain,
multiply(inverse(multiply(A,multiply(inverse(B),C))),D) = multiply(inverse(C),multiply(inverse(multiply(A,inverse(B))),D)),
inference(paramod,[status(thm)],[c_2069,c_1983]) ).
cnf(c_2276,plain,
multiply(inverse(B),multiply(inverse(multiply(inverse(A),inverse(inverse(A)))),multiply(inverse(C),D))) = multiply(inverse(B),inverse(multiply(inverse(D),C))),
inference(paramod,[status(thm)],[c_2072,c_2016]) ).
cnf(c_2277,plain,
multiply(inverse(B),multiply(inverse(multiply(inverse(A),A)),multiply(inverse(C),D))) = multiply(inverse(B),inverse(multiply(inverse(D),C))),
inference(paramod,[status(thm)],[c_2071,c_2276]) ).
cnf(c_2278,plain,
multiply(inverse(B),multiply(inverse(C),D)) = multiply(inverse(B),inverse(multiply(inverse(D),C))),
inference(paramod,[status(thm)],[c_1635,c_2277]) ).
cnf(c_2076,plain,
multiply(inverse(A),inverse(multiply(inverse(B),C))) = multiply(inverse(A),multiply(inverse(C),B)),
inference(copy,[status(thm)],[c_2278]) ).
cnf(c_2078,plain,
inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(A))),multiply(inverse(inverse(C)),inverse(C))))) = B,
inference(paramod,[status(thm)],[c_2072,c_1998]) ).
cnf(c_2083,plain,
inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(C))),multiply(inverse(D),D)))) = multiply(B,inverse(multiply(inverse(A),C))),
inference(paramod,[status(thm)],[c_2076,c_2019]) ).
cnf(c_2092,plain,
multiply(A,inverse(multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_2083,c_2078]) ).
cnf(c_2098,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_2092,c_1889]) ).
cnf(c_2279,plain,
inverse(inverse(multiply(A,multiply(B,inverse(B))))) = A,
inference(paramod,[status(thm)],[c_2098,c_2064]) ).
cnf(c_2107,plain,
multiply(A,multiply(B,inverse(B))) = A,
inference(paramod,[status(thm)],[c_2098,c_2279]) ).
cnf(c_2280,plain,
multiply(inverse(A),inverse(multiply(B,multiply(inverse(inverse(C)),inverse(C))))) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_2098,c_2009]) ).
cnf(c_2281,plain,
multiply(inverse(A),inverse(multiply(B,multiply(C,inverse(C))))) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_2098,c_2280]) ).
cnf(c_2282,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_2107,c_2281]) ).
cnf(c_2110,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_2282]) ).
cnf(c_2283,plain,
multiply(inverse(multiply(inverse(B),inverse(A))),C) = multiply(A,multiply(inverse(inverse(B)),C)),
inference(paramod,[status(thm)],[c_2110,c_1968]) ).
cnf(c_2284,plain,
multiply(multiply(inverse(inverse(A)),inverse(inverse(B))),C) = multiply(A,multiply(inverse(inverse(B)),C)),
inference(paramod,[status(thm)],[c_2110,c_2283]) ).
cnf(c_2285,plain,
multiply(multiply(A,inverse(inverse(B))),C) = multiply(A,multiply(inverse(inverse(B)),C)),
inference(paramod,[status(thm)],[c_2098,c_2284]) ).
cnf(c_2286,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(inverse(inverse(B)),C)),
inference(paramod,[status(thm)],[c_2098,c_2285]) ).
cnf(c_2118,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_2098,c_2286]) ).
cnf(c_2119,plain,
$false,
inference(resolve,[status(thm)],[c_2118,c_1957]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP052-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n013.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Fri Sep 25 14:19:21 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.35 % Process 595923 was started by sandbox on n013,
% 0.07/0.35 % Fri Sep 25 14:19:21 2026
% 0.07/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/0.36
% 0.07/0.36 % From the command line: assign(max_seconds, 300).
% 10.66/3.36
% 10.66/3.36 % Assigning unary symbol inverse kb_weight 0 and highest precedence (10).
% 10.66/3.36
% 10.66/3.36 % SZS status Unsatisfiable for theBenchmark
% 10.66/3.36
% 10.66/3.36 % Proof 1 at 1.05 (+ 0.28) seconds.
% 10.66/3.36 % Length of proof is 181.
% 10.66/3.36 % Level of proof is 39.
% 10.66/3.36 % Maximum clause weight is 100.000.
% 10.66/3.36 % Given clauses 98.
% 10.66/3.36
% 10.66/3.36 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------