%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP049-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:26:23 AM UTC 2026
% Result : Unsatisfiable 30.27s 4.26s
% Output : CNFRefutation 30.27s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,inverse(multiply(inverse(multiply(inverse(multiply(VAR_0,VAR_1)),VAR_2)),inverse(multiply(VAR_1,multiply(inverse(VAR_1),VAR_1)))))) = VAR_2,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),inverse(multiply(B,multiply(inverse(B),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(inverse(multiply(inverse(B),C)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,D)),B)),inverse(multiply(D,multiply(inverse(D),D))))),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,D)),B)),inverse(multiply(D,multiply(inverse(D),D)))))),inverse(multiply(inverse(multiply(inverse(multiply(A,D)),B)),inverse(multiply(D,multiply(inverse(D),D))))))))))) = C,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_10536,plain,
multiply(A,inverse(multiply(inverse(B),inverse(multiply(C,multiply(inverse(C),C)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,C)),D)),B)),inverse(multiply(D,multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_5,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),D)),inverse(multiply(C,multiply(inverse(C),C))))) = multiply(A,inverse(multiply(inverse(D),inverse(multiply(B,multiply(inverse(B),B)))))),
inference(copy,[status(thm)],[c_10536]) ).
cnf(c_14,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(C),inverse(multiply(B,multiply(inverse(B),B))))))) = C,
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_10537,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),inverse(multiply(B,multiply(inverse(B),B))))))),D)),multiply(inverse(C),E))),inverse(multiply(D,multiply(inverse(D),D))))) = E,
inference(paramod,[status(thm)],[c_4,c_5]) ).
cnf(c_16,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(A),C))),inverse(multiply(B,multiply(inverse(B),B))))) = C,
inference(paramod,[status(thm)],[c_1,c_10537]) ).
cnf(c_10538,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(inverse(D),B)),multiply(inverse(D),C)),
inference(paramod,[status(thm)],[c_16,c_14]) ).
cnf(c_46,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(A),C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(copy,[status(thm)],[c_10538]) ).
cnf(c_10539,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(C),A))),inverse(multiply(D,multiply(inverse(D),D))))),E))),inverse(multiply(B,multiply(inverse(B),B))))) = E,
inference(paramod,[status(thm)],[c_16,c_16]) ).
cnf(c_47,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),inverse(multiply(B,multiply(inverse(B),B))))) = C,
inference(paramod,[status(thm)],[c_16,c_10539]) ).
cnf(c_55,plain,
multiply(inverse(multiply(inverse(A),B)),C) = multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),E)),C)),inverse(multiply(E,multiply(inverse(E),E))))))),
inference(paramod,[status(thm)],[c_1,c_46]) ).
cnf(c_10540,plain,
multiply(multiply(A,inverse(multiply(inverse(B),inverse(multiply(C,multiply(inverse(C),C)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_5,c_46]) ).
cnf(c_82,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,C)) = multiply(multiply(D,inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,F)),B)),E)),C)),
inference(copy,[status(thm)],[c_10540]) ).
cnf(c_10541,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),D)) = multiply(inverse(multiply(E,multiply(B,inverse(multiply(inverse(A),inverse(multiply(C,multiply(inverse(C),C)))))))),multiply(E,D)),
inference(paramod,[status(thm)],[c_14,c_46]) ).
cnf(c_87,plain,
multiply(inverse(multiply(A,multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))))),multiply(A,E)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),
inference(copy,[status(thm)],[c_10541]) ).
cnf(c_90,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_46,c_46]) ).
cnf(c_101,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),D)),inverse(multiply(multiply(B,C),multiply(inverse(multiply(E,C)),multiply(E,C))))))) = D,
inference(paramod,[status(thm)],[c_90,c_1]) ).
cnf(c_10542,plain,
multiply(inverse(A),multiply(B,C)) = multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(B,E)),A)),inverse(multiply(E,multiply(inverse(E),E))))))),multiply(D,C)),
inference(paramod,[status(thm)],[c_1,c_90]) ).
cnf(c_102,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,C)),D)),inverse(multiply(C,multiply(inverse(C),C))))))),multiply(A,E)) = multiply(inverse(D),multiply(B,E)),
inference(copy,[status(thm)],[c_10542]) ).
cnf(c_125,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_90,c_90]) ).
cnf(c_10543,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,A))),D)) = multiply(inverse(multiply(E,inverse(multiply(C,multiply(inverse(C),C))))),multiply(E,D)),
inference(paramod,[status(thm)],[c_47,c_90]) ).
cnf(c_142,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,C)) = multiply(D,multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),C)),
inference(copy,[status(thm)],[c_10543]) ).
cnf(c_10544,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,C)),V6)),A)),inverse(multiply(V6,multiply(inverse(V6),V6))))))),multiply(E,multiply(F,D))),
inference(paramod,[status(thm)],[c_1,c_125]) ).
cnf(c_10545,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(E,multiply(F,inverse(multiply(inverse(A),inverse(multiply(C,multiply(inverse(C),C)))))))),multiply(E,multiply(F,D))),
inference(paramod,[status(thm)],[c_5,c_10544]) ).
cnf(c_212,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_87,c_10545]) ).
cnf(c_10546,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,A))),inverse(multiply(F,multiply(inverse(F),F))))),multiply(inverse(multiply(V6,C)),multiply(V6,D))),
inference(paramod,[status(thm)],[c_47,c_212]) ).
cnf(c_355,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_47,c_10546]) ).
cnf(c_10547,plain,
multiply(inverse(multiply(A,B)),inverse(multiply(C,inverse(multiply(multiply(A,C),multiply(inverse(multiply(D,C)),multiply(D,C))))))) = inverse(multiply(B,multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_47,c_101]) ).
cnf(c_484,plain,
inverse(multiply(A,multiply(inverse(A),A))) = multiply(inverse(multiply(B,A)),inverse(multiply(C,inverse(multiply(multiply(B,C),multiply(inverse(multiply(D,C)),multiply(D,C))))))),
inference(copy,[status(thm)],[c_10547]) ).
cnf(c_746,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,A))),D)) = multiply(E,multiply(inverse(multiply(inverse(multiply(F,C)),multiply(F,E))),D)),
inference(paramod,[status(thm)],[c_47,c_142]) ).
cnf(c_10548,plain,
multiply(A,multiply(inverse(multiply(inverse(B),multiply(C,A))),D)) = multiply(E,multiply(inverse(multiply(inverse(multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(C,V6)),B)),inverse(multiply(V6,multiply(inverse(V6),V6))))))),multiply(F,E))),D)),
inference(paramod,[status(thm)],[c_1,c_746]) ).
cnf(c_865,plain,
multiply(A,multiply(inverse(multiply(inverse(B),multiply(C,A))),D)) = multiply(E,multiply(inverse(multiply(inverse(B),multiply(C,E))),D)),
inference(paramod,[status(thm)],[c_102,c_10548]) ).
cnf(c_879,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(C,multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,C))),F)))),inverse(multiply(B,multiply(inverse(B),B))))) = multiply(inverse(multiply(inverse(multiply(V6,E)),multiply(V6,A))),F),
inference(paramod,[status(thm)],[c_746,c_47]) ).
cnf(c_970,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(C,multiply(inverse(multiply(inverse(D),multiply(E,C))),F)))),inverse(multiply(B,multiply(inverse(B),B))))) = multiply(inverse(multiply(inverse(D),multiply(E,A))),F),
inference(paramod,[status(thm)],[c_865,c_47]) ).
cnf(c_1042,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_970,c_879]) ).
cnf(c_2470,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),inverse(multiply(B,multiply(inverse(B),B)))) = C,
inference(paramod,[status(thm)],[c_484,c_14]) ).
cnf(c_2772,plain,
multiply(inverse(A),A) = multiply(B,multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,B))),inverse(multiply(D,multiply(inverse(D),D))))),
inference(paramod,[status(thm)],[c_2470,c_746]) ).
cnf(c_10549,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(B),B))))) = multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,inverse(multiply(inverse(multiply(C,F)),B))))),inverse(multiply(E,multiply(inverse(E),E))))),inverse(multiply(F,multiply(inverse(F),F)))))),
inference(paramod,[status(thm)],[c_2772,c_5]) ).
cnf(c_10550,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(B),B))))) = multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(C,F)),B)),inverse(multiply(F,multiply(inverse(F),F)))))),
inference(paramod,[status(thm)],[c_2470,c_10549]) ).
cnf(c_2856,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(B),B))))) = B,
inference(paramod,[status(thm)],[c_1,c_10550]) ).
cnf(c_3155,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_2470,c_2772]) ).
cnf(c_3170,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2 ),
inference(resolve,[status(thm)],[c_3155,c_3]) ).
cnf(c_3172,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),inverse(multiply(B,multiply(inverse(D),D)))))) = C,
inference(paramod,[status(thm)],[c_3155,c_1]) ).
cnf(c_3188,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_3155,c_90]) ).
cnf(c_3189,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,A)),
inference(paramod,[status(thm)],[c_3155,c_90]) ).
cnf(c_10551,plain,
multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(inverse(multiply(C,D)),multiply(C,D))),
inference(paramod,[status(thm)],[c_3155,c_355]) ).
cnf(c_3215,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,C))) = multiply(A,multiply(inverse(D),D)),
inference(copy,[status(thm)],[c_10551]) ).
cnf(c_10552,plain,
multiply(inverse(multiply(inverse(A),A)),B) = multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,D))),B),
inference(paramod,[status(thm)],[c_3155,c_1042]) ).
cnf(c_3260,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,B))),C) = multiply(inverse(multiply(inverse(D),D)),C),
inference(copy,[status(thm)],[c_10552]) ).
cnf(c_3315,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),multiply(inverse(inverse(B)),inverse(B))))) = B,
inference(paramod,[status(thm)],[c_3155,c_2470]) ).
cnf(c_3343,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,D))),multiply(inverse(inverse(multiply(inverse(multiply(E,C)),multiply(E,D)))),inverse(multiply(inverse(multiply(E,C)),multiply(E,D)))))))) = inverse(multiply(inverse(multiply(E,C)),multiply(E,D))),
inference(paramod,[status(thm)],[c_1042,c_2856]) ).
cnf(c_3352,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_3155,c_2856]) ).
cnf(c_3355,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),
inference(paramod,[status(thm)],[c_3352,c_3343]) ).
cnf(c_3382,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_3155,c_3352]) ).
cnf(c_3443,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(A),A),a2) != a2 ),
inference(paramod,[status(thm)],[c_3155,c_3170]) ).
cnf(c_3541,plain,
multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_3155,c_3215]) ).
cnf(c_3590,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_3541,c_3155]) ).
cnf(c_10553,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))))) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_3590,c_3352]) ).
cnf(c_3695,plain,
inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(B),B)),
inference(paramod,[status(thm)],[c_3352,c_10553]) ).
cnf(c_3933,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),multiply(inverse(C),C)))) = B,
inference(paramod,[status(thm)],[c_3155,c_3315]) ).
cnf(c_3937,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_3590,c_3315]) ).
cnf(c_3940,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(C),C)))))) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_3695,c_3315]) ).
cnf(c_4568,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),D)))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_3188,c_3933]) ).
cnf(c_4586,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_4568,c_3940]) ).
cnf(c_5195,plain,
multiply(inverse(multiply(inverse(A),A)),B) = multiply(inverse(multiply(inverse(C),C)),B),
inference(paramod,[status(thm)],[c_3155,c_3260]) ).
cnf(c_5905,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),inverse(multiply(multiply(inverse(D),D),multiply(inverse(E),E)))))) = C,
inference(paramod,[status(thm)],[c_3590,c_3172]) ).
cnf(c_10554,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(B),B)),inverse(multiply(A,multiply(inverse(C),C)))))) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_3937,c_3172]) ).
cnf(c_10555,plain,
multiply(inverse(A),A) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_3352,c_10554]) ).
cnf(c_5911,plain,
inverse(multiply(inverse(A),A)) = multiply(inverse(B),B),
inference(copy,[status(thm)],[c_10555]) ).
cnf(c_10556,plain,
multiply(multiply(inverse(A),A),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_5911,c_3155]) ).
cnf(c_6008,plain,
multiply(inverse(A),A) = multiply(multiply(inverse(B),B),multiply(inverse(C),C)),
inference(copy,[status(thm)],[c_10556]) ).
cnf(c_6018,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(multiply(inverse(A),A)),a2) != a2 ),
inference(paramod,[status(thm)],[c_5911,c_3443]) ).
cnf(c_6066,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),multiply(inverse(C),C)))) = B,
inference(paramod,[status(thm)],[c_5911,c_3933]) ).
cnf(c_6070,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),inverse(multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_5911,c_3933]) ).
cnf(c_10557,plain,
multiply(multiply(inverse(A),A),B) = multiply(inverse(multiply(inverse(C),C)),B),
inference(paramod,[status(thm)],[c_5911,c_5195]) ).
cnf(c_6131,plain,
multiply(inverse(multiply(inverse(A),A)),B) = multiply(multiply(inverse(C),C),B),
inference(copy,[status(thm)],[c_10557]) ).
cnf(c_6170,plain,
inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_5911,c_5911]) ).
cnf(c_6719,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),a2) != a2 ),
inference(paramod,[status(thm)],[c_3541,c_6018]) ).
cnf(c_7498,plain,
multiply(inverse(multiply(inverse(A),inverse(multiply(B,multiply(inverse(C),C))))),D) = multiply(B,multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_3352,c_55]) ).
cnf(c_7857,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(B),B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_6008,c_3189]) ).
cnf(c_7869,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(multiply(inverse(B),B),C))) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),
inference(paramod,[status(thm)],[c_6008,c_3355]) ).
cnf(c_10558,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),C)),multiply(multiply(inverse(V6),V6),multiply(A,E))),
inference(paramod,[status(thm)],[c_6131,c_125]) ).
cnf(c_8009,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(multiply(inverse(C),C),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(D,F)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(copy,[status(thm)],[c_10558]) ).
cnf(c_8064,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(multiply(inverse(C),C),D))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_6131,c_3355]) ).
cnf(c_8071,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(B),B),C)),D)),inverse(multiply(C,multiply(inverse(E),E)))))) = D,
inference(paramod,[status(thm)],[c_6131,c_3172]) ).
cnf(c_8074,plain,
multiply(multiply(inverse(A),A),B) = multiply(multiply(inverse(C),C),B),
inference(paramod,[status(thm)],[c_5911,c_6131]) ).
cnf(c_10559,plain,
multiply(multiply(A,multiply(inverse(multiply(inverse(B),B)),inverse(multiply(A,multiply(inverse(C),C))))),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_3352,c_8074]) ).
cnf(c_8118,plain,
multiply(multiply(inverse(A),A),B) = multiply(multiply(C,multiply(inverse(multiply(inverse(D),D)),inverse(multiply(C,multiply(inverse(E),E))))),B),
inference(copy,[status(thm)],[c_10559]) ).
cnf(c_8126,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_3382,c_8074]) ).
cnf(c_8127,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(multiply(inverse(D),D),B)),multiply(multiply(inverse(E),E),C)),
inference(paramod,[status(thm)],[c_8074,c_3188]) ).
cnf(c_8349,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_82,c_3933]) ).
cnf(c_8361,plain,
multiply(inverse(multiply(inverse(A),inverse(multiply(B,multiply(inverse(B),B))))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_3937,c_82]) ).
cnf(c_8386,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_82,c_3188]) ).
cnf(c_8398,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,multiply(inverse(multiply(inverse(multiply(C,D)),B)),E))) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_3188,c_82]) ).
cnf(c_10560,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,C)) = multiply(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(multiply(inverse(F),F))),inverse(multiply(inverse(F),F)))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_4586,c_82]) ).
cnf(c_8402,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,C)) = multiply(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_4586,c_10560]) ).
cnf(c_10561,plain,
multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(B),B))))),multiply(A,C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_5911,c_82]) ).
cnf(c_8494,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),inverse(multiply(C,multiply(inverse(C),C)))))),C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(copy,[status(thm)],[c_10561]) ).
cnf(c_9505,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),multiply(inverse(multiply(C,D)),E))))) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(D),D)))))))),
inference(paramod,[status(thm)],[c_87,c_3352]) ).
cnf(c_9519,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C)))),multiply(A,D)) = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_3590,c_87]) ).
cnf(c_9526,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))))),E) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_3933,c_87]) ).
cnf(c_10562,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,C)) = multiply(inverse(inverse(multiply(D,multiply(inverse(D),D)))),multiply(inverse(multiply(inverse(multiply(inverse(E),E)),D)),C)),
inference(paramod,[status(thm)],[c_3937,c_87]) ).
cnf(c_9527,plain,
multiply(inverse(inverse(multiply(A,multiply(inverse(A),A)))),multiply(inverse(multiply(inverse(multiply(inverse(B),B)),A)),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
inference(copy,[status(thm)],[c_10562]) ).
cnf(c_10563,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D)))))))))),multiply(A,E)) = multiply(inverse(C),multiply(inverse(multiply(inverse(F),F)),E)),
inference(paramod,[status(thm)],[c_3937,c_87]) ).
cnf(c_10564,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(D),D)))))))),multiply(A,E)) = multiply(inverse(C),multiply(inverse(multiply(inverse(F),F)),E)),
inference(paramod,[status(thm)],[c_4586,c_10563]) ).
cnf(c_9529,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),multiply(inverse(multiply(inverse(D),D)),C)),
inference(paramod,[status(thm)],[c_6070,c_10564]) ).
cnf(c_9626,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))))),multiply(multiply(inverse(E),E),F)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),F)),
inference(paramod,[status(thm)],[c_6131,c_87]) ).
cnf(c_10011,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),D)))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_3188,c_6066]) ).
cnf(c_10123,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(multiply(inverse(C),C),multiply(multiply(inverse(D),D),multiply(inverse(E),E))))))) = B,
inference(paramod,[status(thm)],[c_6170,c_3352]) ).
cnf(c_10176,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),inverse(multiply(multiply(inverse(C),C),multiply(inverse(D),D)))))) = B,
inference(paramod,[status(thm)],[c_6170,c_3933]) ).
cnf(c_10266,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(multiply(multiply(inverse(B),B),C)),inverse(multiply(multiply(inverse(D),D),multiply(inverse(E),E)))))) = C,
inference(paramod,[status(thm)],[c_6170,c_3172]) ).
cnf(c_10324,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(multiply(inverse(B),B),multiply(multiply(inverse(C),C),multiply(inverse(D),D))))),a2) != a2 ),
inference(paramod,[status(thm)],[c_6170,c_6719]) ).
cnf(c_10382,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),inverse(multiply(multiply(inverse(C),C),multiply(inverse(D),D)))))) = B,
inference(paramod,[status(thm)],[c_6170,c_6066]) ).
cnf(c_10389,plain,
multiply(inverse(multiply(inverse(A),A)),B) = B,
inference(paramod,[status(thm)],[c_10176,c_5905]) ).
cnf(c_10393,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_10382,c_10266]) ).
cnf(c_10565,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(multiply(inverse(B),B),multiply(inverse(D),D)))),a2) != a2 ),
inference(paramod,[status(thm)],[c_10393,c_10324]) ).
cnf(c_10566,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(D),D))),a2) != a2 ),
inference(paramod,[status(thm)],[c_10393,c_10565]) ).
cnf(c_10567,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(multiply(inverse(D),D)),a2) != a2 ),
inference(paramod,[status(thm)],[c_10389,c_10566]) ).
cnf(c_10568,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_10389,c_10567]) ).
cnf(c_10396,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(copy,[status(thm)],[c_10568]) ).
cnf(c_10569,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(multiply(inverse(C),C),multiply(inverse(E),E)))))) = B,
inference(paramod,[status(thm)],[c_10393,c_10123]) ).
cnf(c_10570,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(B,multiply(inverse(E),E))))) = B,
inference(paramod,[status(thm)],[c_10393,c_10569]) ).
cnf(c_10405,plain,
inverse(inverse(multiply(A,multiply(inverse(B),B)))) = A,
inference(paramod,[status(thm)],[c_10389,c_10570]) ).
cnf(c_10571,plain,
multiply(multiply(inverse(A),A),inverse(multiply(inverse(C),D))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_10389,c_10011]) ).
cnf(c_10409,plain,
inverse(multiply(inverse(A),B)) = multiply(inverse(B),A),
inference(paramod,[status(thm)],[c_10393,c_10571]) ).
cnf(c_10572,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))))),multiply(multiply(inverse(E),E),F)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),F)),
inference(paramod,[status(thm)],[c_10409,c_9626]) ).
cnf(c_10573,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,multiply(inverse(inverse(multiply(D,multiply(inverse(D),D)))),C)))),multiply(multiply(inverse(E),E),F)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),F)),
inference(paramod,[status(thm)],[c_10409,c_10572]) ).
cnf(c_10574,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,multiply(D,C)))),multiply(multiply(inverse(E),E),F)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),F)),
inference(paramod,[status(thm)],[c_10405,c_10573]) ).
cnf(c_10575,plain,
multiply(inverse(multiply(B,multiply(D,C))),multiply(multiply(inverse(E),E),F)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),F)),
inference(paramod,[status(thm)],[c_10393,c_10574]) ).
cnf(c_10421,plain,
multiply(inverse(multiply(A,multiply(B,C))),D) = multiply(inverse(C),multiply(inverse(multiply(A,B)),D)),
inference(paramod,[status(thm)],[c_10393,c_10575]) ).
cnf(c_10576,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),multiply(multiply(inverse(D),D),C)),
inference(paramod,[status(thm)],[c_10409,c_9529]) ).
cnf(c_10437,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_10393,c_10576]) ).
cnf(c_10577,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(inverse(B),B)),A)),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
inference(paramod,[status(thm)],[c_10405,c_9527]) ).
cnf(c_10578,plain,
multiply(A,multiply(inverse(multiply(multiply(inverse(B),B),A)),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
inference(paramod,[status(thm)],[c_10409,c_10577]) ).
cnf(c_10579,plain,
multiply(A,multiply(inverse(A),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
inference(paramod,[status(thm)],[c_10393,c_10578]) ).
cnf(c_10580,plain,
multiply(A,multiply(inverse(A),C)) = multiply(inverse(multiply(inverse(E),E)),C),
inference(paramod,[status(thm)],[c_10437,c_10579]) ).
cnf(c_10581,plain,
multiply(A,multiply(inverse(A),C)) = multiply(multiply(inverse(E),E),C),
inference(paramod,[status(thm)],[c_10409,c_10580]) ).
cnf(c_10438,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_10393,c_10581]) ).
cnf(c_10582,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))))),E) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_10409,c_9526]) ).
cnf(c_10583,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,inverse(multiply(inverse(C),inverse(D)))))),E) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_10438,c_10582]) ).
cnf(c_10584,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,multiply(inverse(inverse(D)),C)))),E) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_10409,c_10583]) ).
cnf(c_10585,plain,
multiply(inverse(multiply(B,multiply(inverse(inverse(D)),C))),E) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_10393,c_10584]) ).
cnf(c_10586,plain,
multiply(inverse(C),multiply(inverse(multiply(B,inverse(inverse(D)))),E)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),inverse(multiply(inverse(E),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_10421,c_10585]) ).
cnf(c_10587,plain,
multiply(inverse(C),multiply(inverse(multiply(B,inverse(inverse(D)))),E)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),multiply(inverse(multiply(inverse(F),F)),E))),
inference(paramod,[status(thm)],[c_10409,c_10586]) ).
cnf(c_10588,plain,
multiply(inverse(C),multiply(inverse(multiply(B,inverse(inverse(D)))),E)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),multiply(multiply(inverse(F),F),E))),
inference(paramod,[status(thm)],[c_10409,c_10587]) ).
cnf(c_10439,plain,
multiply(inverse(A),multiply(inverse(multiply(B,inverse(inverse(C)))),D)) = multiply(inverse(A),multiply(inverse(multiply(B,C)),D)),
inference(paramod,[status(thm)],[c_10393,c_10588]) ).
cnf(c_10589,plain,
multiply(inverse(multiply(A,multiply(multiply(inverse(B),B),multiply(inverse(C),C)))),multiply(A,D)) = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_10409,c_9519]) ).
cnf(c_10590,plain,
multiply(inverse(multiply(A,multiply(inverse(C),C))),multiply(A,D)) = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_10393,c_10589]) ).
cnf(c_10591,plain,
multiply(inverse(multiply(inverse(C),C)),D) = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_10437,c_10590]) ).
cnf(c_10592,plain,
multiply(multiply(inverse(C),C),D) = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_10409,c_10591]) ).
cnf(c_10593,plain,
D = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(multiply(F,multiply(inverse(F),F)))))),F)),D)),
inference(paramod,[status(thm)],[c_10393,c_10592]) ).
cnf(c_10594,plain,
D = multiply(inverse(E),multiply(inverse(multiply(inverse(inverse(multiply(inverse(E),inverse(F)))),F)),D)),
inference(paramod,[status(thm)],[c_10438,c_10593]) ).
cnf(c_10595,plain,
D = multiply(inverse(E),multiply(inverse(multiply(inverse(multiply(inverse(inverse(F)),E)),F)),D)),
inference(paramod,[status(thm)],[c_10409,c_10594]) ).
cnf(c_10596,plain,
D = multiply(inverse(E),multiply(inverse(multiply(multiply(inverse(E),inverse(F)),F)),D)),
inference(paramod,[status(thm)],[c_10409,c_10595]) ).
cnf(c_10442,plain,
multiply(inverse(A),multiply(inverse(multiply(multiply(inverse(A),inverse(B)),B)),C)) = C,
inference(copy,[status(thm)],[c_10596]) ).
cnf(c_10597,plain,
inverse(multiply(multiply(inverse(A),A),inverse(multiply(inverse(B),multiply(inverse(multiply(C,D)),E))))) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(D),D)))))))),
inference(paramod,[status(thm)],[c_10409,c_9505]) ).
cnf(c_10598,plain,
inverse(multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(C,D)),E)),B))) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(D),D)))))))),
inference(paramod,[status(thm)],[c_10409,c_10597]) ).
cnf(c_10599,plain,
inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(E),multiply(C,D)),B))) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(D),D)))))))),
inference(paramod,[status(thm)],[c_10409,c_10598]) ).
cnf(c_10600,plain,
inverse(multiply(multiply(inverse(E),multiply(C,D)),B)) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(multiply(D,multiply(inverse(D),D)))))))),
inference(paramod,[status(thm)],[c_10393,c_10599]) ).
cnf(c_10601,plain,
inverse(multiply(multiply(inverse(E),multiply(C,D)),B)) = inverse(multiply(inverse(E),multiply(C,inverse(multiply(inverse(B),inverse(D)))))),
inference(paramod,[status(thm)],[c_10438,c_10600]) ).
cnf(c_10602,plain,
inverse(multiply(multiply(inverse(E),multiply(C,D)),B)) = inverse(multiply(inverse(E),multiply(C,multiply(inverse(inverse(D)),B)))),
inference(paramod,[status(thm)],[c_10409,c_10601]) ).
cnf(c_10603,plain,
inverse(multiply(multiply(inverse(E),multiply(C,D)),B)) = multiply(inverse(multiply(C,multiply(inverse(inverse(D)),B))),E),
inference(paramod,[status(thm)],[c_10409,c_10602]) ).
cnf(c_10604,plain,
inverse(multiply(multiply(inverse(E),multiply(C,D)),B)) = multiply(inverse(B),multiply(inverse(multiply(C,inverse(inverse(D)))),E)),
inference(paramod,[status(thm)],[c_10421,c_10603]) ).
cnf(c_10445,plain,
inverse(multiply(multiply(inverse(A),multiply(B,C)),D)) = multiply(inverse(D),multiply(inverse(multiply(B,C)),A)),
inference(paramod,[status(thm)],[c_10439,c_10604]) ).
cnf(c_10605,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),inverse(multiply(C,multiply(inverse(C),C)))))),C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_10409,c_8494]) ).
cnf(c_10606,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),inverse(C)))),C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_10438,c_10605]) ).
cnf(c_10607,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),B)),C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_10409,c_10606]) ).
cnf(c_10608,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(B),inverse(C)),C)),D)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_10409,c_10607]) ).
cnf(c_10609,plain,
multiply(multiply(inverse(A),A),multiply(inverse(multiply(multiply(inverse(D),multiply(multiply(inverse(B),inverse(C)),C)),B)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_10409,c_10608]) ).
cnf(c_10610,plain,
multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),multiply(inverse(multiply(multiply(inverse(B),inverse(C)),C)),D)),E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_10445,c_10609]) ).
cnf(c_10611,plain,
multiply(multiply(inverse(A),A),multiply(D,E)) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_10442,c_10610]) ).
cnf(c_10612,plain,
multiply(D,E) = multiply(inverse(multiply(F,inverse(multiply(D,multiply(inverse(D),D))))),multiply(F,E)),
inference(paramod,[status(thm)],[c_10393,c_10611]) ).
cnf(c_10613,plain,
multiply(D,E) = multiply(inverse(multiply(F,inverse(D))),multiply(F,E)),
inference(paramod,[status(thm)],[c_10438,c_10612]) ).
cnf(c_10614,plain,
multiply(D,E) = multiply(inverse(inverse(D)),E),
inference(paramod,[status(thm)],[c_10437,c_10613]) ).
cnf(c_10456,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(copy,[status(thm)],[c_10614]) ).
cnf(c_10615,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,C)) = multiply(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10438,c_8402]) ).
cnf(c_10616,plain,
multiply(inverse(inverse(B)),C) = multiply(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10437,c_10615]) ).
cnf(c_10617,plain,
multiply(B,C) = multiply(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10456,c_10616]) ).
cnf(c_10618,plain,
multiply(B,C) = multiply(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10409,c_10617]) ).
cnf(c_10619,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(E),inverse(multiply(inverse(multiply(inverse(F),F)),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10409,c_10618]) ).
cnf(c_10620,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(E),inverse(multiply(multiply(inverse(F),F),multiply(inverse(F),F)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10409,c_10619]) ).
cnf(c_10621,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(E),inverse(multiply(inverse(F),F))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10393,c_10620]) ).
cnf(c_10622,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),inverse(multiply(inverse(E),multiply(inverse(F),F)))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10409,c_10621]) ).
cnf(c_10623,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),multiply(inverse(multiply(inverse(F),F)),E)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10409,c_10622]) ).
cnf(c_10624,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),multiply(multiply(inverse(F),F),E)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10409,c_10623]) ).
cnf(c_10625,plain,
multiply(B,C) = multiply(multiply(multiply(inverse(D),D),E),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10393,c_10624]) ).
cnf(c_10626,plain,
multiply(B,C) = multiply(E,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(F),F)),B)),E)),C)),
inference(paramod,[status(thm)],[c_10393,c_10625]) ).
cnf(c_10627,plain,
multiply(B,C) = multiply(E,multiply(inverse(multiply(inverse(multiply(multiply(inverse(F),F),B)),E)),C)),
inference(paramod,[status(thm)],[c_10409,c_10626]) ).
cnf(c_10628,plain,
multiply(B,C) = multiply(E,multiply(inverse(multiply(inverse(B),E)),C)),
inference(paramod,[status(thm)],[c_10393,c_10627]) ).
cnf(c_10629,plain,
multiply(B,C) = multiply(E,multiply(multiply(inverse(E),B),C)),
inference(paramod,[status(thm)],[c_10409,c_10628]) ).
cnf(c_10463,plain,
multiply(A,multiply(multiply(inverse(A),B),C)) = multiply(B,C),
inference(copy,[status(thm)],[c_10629]) ).
cnf(c_10630,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(multiply(inverse(multiply(C,D)),B)),E))) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_10438,c_8398]) ).
cnf(c_10631,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(multiply(inverse(B),multiply(C,D)),E))) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_10409,c_10630]) ).
cnf(c_10632,plain,
multiply(inverse(inverse(B)),multiply(multiply(inverse(B),multiply(C,D)),E)) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_10437,c_10631]) ).
cnf(c_10633,plain,
multiply(B,multiply(multiply(inverse(B),multiply(C,D)),E)) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_10456,c_10632]) ).
cnf(c_10634,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_10463,c_10633]) ).
cnf(c_10635,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,inverse(multiply(inverse(F),inverse(D)))),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_10438,c_10634]) ).
cnf(c_10636,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,multiply(inverse(inverse(D)),F)),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_10409,c_10635]) ).
cnf(c_10637,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,multiply(D,F)),multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_10456,c_10636]) ).
cnf(c_10638,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,multiply(D,F)),multiply(multiply(inverse(V6),V6),multiply(inverse(F),E))),
inference(paramod,[status(thm)],[c_10409,c_10637]) ).
cnf(c_10639,plain,
multiply(multiply(C,D),E) = multiply(multiply(C,multiply(D,F)),multiply(inverse(F),E)),
inference(paramod,[status(thm)],[c_10393,c_10638]) ).
cnf(c_10464,plain,
multiply(multiply(A,multiply(B,C)),multiply(inverse(C),D)) = multiply(multiply(A,B),D),
inference(copy,[status(thm)],[c_10639]) ).
cnf(c_10640,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_10409,c_8386]) ).
cnf(c_10641,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,inverse(multiply(inverse(C),inverse(D)))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_10438,c_10640]) ).
cnf(c_10642,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,multiply(inverse(inverse(D)),C)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_10409,c_10641]) ).
cnf(c_10643,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,multiply(D,C)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_10456,c_10642]) ).
cnf(c_10644,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,multiply(D,C)),multiply(inverse(multiply(multiply(inverse(E),multiply(B,D)),C)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_10409,c_10643]) ).
cnf(c_10645,plain,
multiply(multiply(inverse(A),A),multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F))) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_10445,c_10644]) ).
cnf(c_10646,plain,
multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F)) = multiply(inverse(multiply(V6,multiply(V7,inverse(multiply(E,multiply(inverse(E),E)))))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_10393,c_10645]) ).
cnf(c_10647,plain,
multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F)) = multiply(inverse(multiply(V6,multiply(V7,inverse(E)))),multiply(V6,multiply(V7,F))),
inference(paramod,[status(thm)],[c_10438,c_10646]) ).
cnf(c_10648,plain,
multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F)) = multiply(inverse(multiply(V7,inverse(E))),multiply(V7,F)),
inference(paramod,[status(thm)],[c_10437,c_10647]) ).
cnf(c_10649,plain,
multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F)) = multiply(inverse(inverse(E)),F),
inference(paramod,[status(thm)],[c_10437,c_10648]) ).
cnf(c_10472,plain,
multiply(multiply(A,multiply(B,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(A,B)),D)),E)) = multiply(D,E),
inference(paramod,[status(thm)],[c_10456,c_10649]) ).
cnf(c_10650,plain,
multiply(inverse(multiply(inverse(A),inverse(B))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_10438,c_8361]) ).
cnf(c_10651,plain,
multiply(multiply(inverse(inverse(B)),A),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_10409,c_10650]) ).
cnf(c_10652,plain,
multiply(multiply(B,A),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_10456,c_10651]) ).
cnf(c_10653,plain,
multiply(multiply(B,A),multiply(multiply(inverse(C),C),inverse(multiply(inverse(D),D)))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_10409,c_10652]) ).
cnf(c_10654,plain,
multiply(multiply(B,A),multiply(multiply(inverse(C),C),multiply(inverse(D),D))) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_10409,c_10653]) ).
cnf(c_10655,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(multiply(V6,multiply(inverse(V6),V6)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_10393,c_10654]) ).
cnf(c_10656,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,inverse(multiply(inverse(F),inverse(V6)))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_10438,c_10655]) ).
cnf(c_10657,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,multiply(inverse(inverse(V6)),F)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_10409,c_10656]) ).
cnf(c_10658,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,multiply(V6,F)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,V6)),B)),F)),A)),
inference(paramod,[status(thm)],[c_10456,c_10657]) ).
cnf(c_10659,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,multiply(V6,F)),multiply(inverse(multiply(multiply(inverse(B),multiply(E,V6)),F)),A)),
inference(paramod,[status(thm)],[c_10409,c_10658]) ).
cnf(c_10660,plain,
multiply(multiply(B,A),multiply(inverse(D),D)) = multiply(multiply(E,multiply(V6,F)),multiply(multiply(inverse(F),multiply(inverse(multiply(E,V6)),B)),A)),
inference(paramod,[status(thm)],[c_10445,c_10659]) ).
cnf(c_10477,plain,
multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(A,B),
inference(paramod,[status(thm)],[c_10472,c_10660]) ).
cnf(c_10661,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,inverse(multiply(inverse(C),inverse(multiply(D,multiply(inverse(D),D)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_10409,c_8349]) ).
cnf(c_10662,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,inverse(multiply(inverse(C),inverse(D)))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_10438,c_10661]) ).
cnf(c_10663,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,multiply(inverse(inverse(D)),C)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_10409,c_10662]) ).
cnf(c_10664,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,multiply(D,C)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,D)),E)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_10456,c_10663]) ).
cnf(c_10665,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,multiply(D,C)),multiply(inverse(multiply(multiply(inverse(E),multiply(B,D)),C)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_10409,c_10664]) ).
cnf(c_10666,plain,
multiply(multiply(inverse(A),A),inverse(multiply(multiply(B,multiply(D,C)),multiply(multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),F)))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_10445,c_10665]) ).
cnf(c_10667,plain,
multiply(multiply(inverse(A),A),inverse(multiply(E,F))) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_10472,c_10666]) ).
cnf(c_10668,plain,
inverse(multiply(E,F)) = multiply(inverse(F),inverse(multiply(E,multiply(inverse(E),E)))),
inference(paramod,[status(thm)],[c_10393,c_10667]) ).
cnf(c_10479,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(paramod,[status(thm)],[c_10438,c_10668]) ).
cnf(c_10669,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(B),C)) = multiply(inverse(multiply(multiply(inverse(D),D),B)),multiply(multiply(inverse(E),E),C)),
inference(paramod,[status(thm)],[c_10479,c_8127]) ).
cnf(c_10670,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(B),C)) = multiply(inverse(B),multiply(multiply(inverse(E),E),C)),
inference(paramod,[status(thm)],[c_10393,c_10669]) ).
cnf(c_10506,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(B),C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_10393,c_10670]) ).
cnf(c_10671,plain,
multiply(multiply(inverse(multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(inverse(B),B)))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_10479,c_8126]) ).
cnf(c_10672,plain,
multiply(multiply(inverse(multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(B),inverse(inverse(B))))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_10479,c_10671]) ).
cnf(c_10673,plain,
multiply(multiply(inverse(multiply(inverse(B),inverse(inverse(B)))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_10506,c_10672]) ).
cnf(c_10674,plain,
multiply(multiply(multiply(inverse(inverse(inverse(B))),inverse(inverse(B))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_10479,c_10673]) ).
cnf(c_10675,plain,
multiply(multiply(multiply(inverse(B),inverse(inverse(B))),multiply(inverse(C),C)),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_10456,c_10674]) ).
cnf(c_10676,plain,
multiply(multiply(inverse(B),inverse(inverse(B))),D) = multiply(multiply(inverse(E),E),D),
inference(paramod,[status(thm)],[c_10477,c_10675]) ).
cnf(c_10507,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),B) = B,
inference(paramod,[status(thm)],[c_10393,c_10676]) ).
cnf(c_10677,plain,
B = multiply(multiply(C,multiply(inverse(multiply(inverse(D),D)),inverse(multiply(C,multiply(inverse(E),E))))),B),
inference(paramod,[status(thm)],[c_10393,c_8118]) ).
cnf(c_10678,plain,
B = multiply(multiply(C,multiply(multiply(inverse(D),inverse(inverse(D))),inverse(multiply(C,multiply(inverse(E),E))))),B),
inference(paramod,[status(thm)],[c_10479,c_10677]) ).
cnf(c_10679,plain,
B = multiply(multiply(C,multiply(multiply(inverse(D),inverse(inverse(D))),multiply(inverse(multiply(inverse(E),E)),inverse(C)))),B),
inference(paramod,[status(thm)],[c_10479,c_10678]) ).
cnf(c_10680,plain,
B = multiply(multiply(C,multiply(multiply(inverse(D),inverse(inverse(D))),multiply(multiply(inverse(E),inverse(inverse(E))),inverse(C)))),B),
inference(paramod,[status(thm)],[c_10479,c_10679]) ).
cnf(c_10681,plain,
B = multiply(multiply(C,multiply(multiply(inverse(D),inverse(inverse(D))),inverse(C))),B),
inference(paramod,[status(thm)],[c_10507,c_10680]) ).
cnf(c_10682,plain,
B = multiply(multiply(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_10507,c_10681]) ).
cnf(c_10508,plain,
multiply(multiply(A,inverse(A)),B) = B,
inference(copy,[status(thm)],[c_10682]) ).
cnf(c_10683,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(B),B),C)),D)),inverse(multiply(C,multiply(inverse(E),E)))))) = D,
inference(paramod,[status(thm)],[c_10479,c_8071]) ).
cnf(c_10684,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(inverse(multiply(inverse(C),D)),inverse(multiply(C,multiply(inverse(E),E)))))) = D,
inference(paramod,[status(thm)],[c_10393,c_10683]) ).
cnf(c_10685,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(multiply(inverse(D),inverse(inverse(C))),inverse(multiply(C,multiply(inverse(E),E)))))) = D,
inference(paramod,[status(thm)],[c_10479,c_10684]) ).
cnf(c_10686,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(multiply(inverse(D),inverse(inverse(C))),multiply(inverse(multiply(inverse(E),E)),inverse(C))))) = D,
inference(paramod,[status(thm)],[c_10479,c_10685]) ).
cnf(c_10687,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(multiply(inverse(D),inverse(inverse(C))),multiply(multiply(inverse(E),inverse(inverse(E))),inverse(C))))) = D,
inference(paramod,[status(thm)],[c_10479,c_10686]) ).
cnf(c_10688,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(multiply(multiply(inverse(D),inverse(inverse(C))),inverse(C)))) = D,
inference(paramod,[status(thm)],[c_10508,c_10687]) ).
cnf(c_10689,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(inverse(C)),inverse(multiply(inverse(D),inverse(inverse(C)))))) = D,
inference(paramod,[status(thm)],[c_10479,c_10688]) ).
cnf(c_10690,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(inverse(C)),multiply(inverse(inverse(inverse(C))),inverse(inverse(D))))) = D,
inference(paramod,[status(thm)],[c_10479,c_10689]) ).
cnf(c_10691,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(inverse(C)),multiply(inverse(C),inverse(inverse(D))))) = D,
inference(paramod,[status(thm)],[c_10456,c_10690]) ).
cnf(c_10692,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),multiply(C,multiply(inverse(C),inverse(inverse(D))))) = D,
inference(paramod,[status(thm)],[c_10456,c_10691]) ).
cnf(c_10693,plain,
multiply(multiply(inverse(A),inverse(inverse(A))),inverse(inverse(D))) = D,
inference(paramod,[status(thm)],[c_10438,c_10692]) ).
cnf(c_10509,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_10508,c_10693]) ).
cnf(c_10694,plain,
inverse(multiply(inverse(multiply(multiply(inverse(A),inverse(inverse(A))),B)),multiply(multiply(inverse(C),C),D))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_10479,c_8064]) ).
cnf(c_10695,plain,
inverse(multiply(inverse(multiply(multiply(inverse(A),A),B)),multiply(multiply(inverse(C),C),D))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_10509,c_10694]) ).
cnf(c_10696,plain,
inverse(multiply(inverse(B),multiply(multiply(inverse(C),C),D))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_10393,c_10695]) ).
cnf(c_10697,plain,
inverse(multiply(inverse(B),D)) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_10393,c_10696]) ).
cnf(c_10698,plain,
multiply(inverse(D),inverse(inverse(B))) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_10479,c_10697]) ).
cnf(c_10699,plain,
multiply(inverse(D),B) = inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),
inference(paramod,[status(thm)],[c_10509,c_10698]) ).
cnf(c_10700,plain,
multiply(inverse(D),B) = inverse(multiply(multiply(inverse(B),inverse(E)),multiply(E,D))),
inference(paramod,[status(thm)],[c_10479,c_10699]) ).
cnf(c_10701,plain,
multiply(inverse(D),B) = multiply(inverse(multiply(E,D)),inverse(multiply(inverse(B),inverse(E)))),
inference(paramod,[status(thm)],[c_10479,c_10700]) ).
cnf(c_10702,plain,
multiply(inverse(D),B) = multiply(multiply(inverse(D),inverse(E)),inverse(multiply(inverse(B),inverse(E)))),
inference(paramod,[status(thm)],[c_10479,c_10701]) ).
cnf(c_10703,plain,
multiply(inverse(D),B) = multiply(multiply(inverse(D),inverse(E)),multiply(inverse(inverse(E)),inverse(inverse(B)))),
inference(paramod,[status(thm)],[c_10479,c_10702]) ).
cnf(c_10704,plain,
multiply(inverse(D),B) = multiply(multiply(inverse(D),inverse(E)),multiply(E,inverse(inverse(B)))),
inference(paramod,[status(thm)],[c_10509,c_10703]) ).
cnf(c_10705,plain,
multiply(inverse(D),B) = multiply(multiply(inverse(D),inverse(E)),multiply(E,B)),
inference(paramod,[status(thm)],[c_10509,c_10704]) ).
cnf(c_10510,plain,
multiply(multiply(inverse(A),inverse(B)),multiply(B,C)) = multiply(inverse(A),C),
inference(copy,[status(thm)],[c_10705]) ).
cnf(c_10706,plain,
multiply(inverse(multiply(multiply(inverse(A),inverse(inverse(A))),B)),multiply(multiply(inverse(C),C),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(D,F)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_10479,c_8009]) ).
cnf(c_10707,plain,
multiply(inverse(multiply(multiply(inverse(A),A),B)),multiply(multiply(inverse(C),C),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(D,F)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_10509,c_10706]) ).
cnf(c_10708,plain,
multiply(inverse(B),multiply(multiply(inverse(C),C),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(D,F)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_10393,c_10707]) ).
cnf(c_10709,plain,
multiply(inverse(B),multiply(D,E)) = multiply(inverse(multiply(inverse(multiply(D,F)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_10393,c_10708]) ).
cnf(c_10710,plain,
multiply(inverse(B),multiply(D,E)) = multiply(inverse(multiply(multiply(inverse(F),inverse(D)),B)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_10479,c_10709]) ).
cnf(c_10711,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),inverse(multiply(inverse(F),inverse(D)))),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_10479,c_10710]) ).
cnf(c_10712,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),multiply(inverse(inverse(D)),inverse(inverse(F)))),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_10479,c_10711]) ).
cnf(c_10713,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),multiply(D,inverse(inverse(F)))),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_10509,c_10712]) ).
cnf(c_10714,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),multiply(D,F)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_10509,c_10713]) ).
cnf(c_10715,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),multiply(D,F)),multiply(multiply(inverse(F),inverse(V6)),multiply(V6,E))),
inference(paramod,[status(thm)],[c_10479,c_10714]) ).
cnf(c_10716,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),multiply(D,F)),multiply(inverse(F),E)),
inference(paramod,[status(thm)],[c_10510,c_10715]) ).
cnf(c_10717,plain,
multiply(inverse(B),multiply(D,E)) = multiply(multiply(inverse(B),D),E),
inference(paramod,[status(thm)],[c_10464,c_10716]) ).
cnf(c_10518,plain,
multiply(multiply(inverse(A),B),C) = multiply(inverse(A),multiply(B,C)),
inference(copy,[status(thm)],[c_10717]) ).
cnf(c_10718,plain,
inverse(multiply(multiply(inverse(A),inverse(inverse(A))),multiply(multiply(inverse(B),B),C))) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),
inference(paramod,[status(thm)],[c_10479,c_7869]) ).
cnf(c_10719,plain,
inverse(multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),C))) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),
inference(paramod,[status(thm)],[c_10509,c_10718]) ).
cnf(c_10720,plain,
inverse(multiply(multiply(inverse(A),A),C)) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),
inference(paramod,[status(thm)],[c_10393,c_10719]) ).
cnf(c_10721,plain,
inverse(C) = inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),
inference(paramod,[status(thm)],[c_10393,c_10720]) ).
cnf(c_10722,plain,
inverse(C) = inverse(multiply(multiply(inverse(multiply(inverse(E),E)),inverse(D)),multiply(D,C))),
inference(paramod,[status(thm)],[c_10479,c_10721]) ).
cnf(c_10723,plain,
inverse(C) = inverse(multiply(multiply(multiply(inverse(E),inverse(inverse(E))),inverse(D)),multiply(D,C))),
inference(paramod,[status(thm)],[c_10479,c_10722]) ).
cnf(c_10724,plain,
inverse(C) = inverse(multiply(multiply(multiply(inverse(E),E),inverse(D)),multiply(D,C))),
inference(paramod,[status(thm)],[c_10509,c_10723]) ).
cnf(c_10725,plain,
inverse(C) = inverse(multiply(inverse(D),multiply(D,C))),
inference(paramod,[status(thm)],[c_10393,c_10724]) ).
cnf(c_10726,plain,
inverse(C) = multiply(inverse(multiply(D,C)),inverse(inverse(D))),
inference(paramod,[status(thm)],[c_10479,c_10725]) ).
cnf(c_10727,plain,
inverse(C) = multiply(multiply(inverse(C),inverse(D)),inverse(inverse(D))),
inference(paramod,[status(thm)],[c_10479,c_10726]) ).
cnf(c_10728,plain,
inverse(C) = multiply(multiply(inverse(C),inverse(D)),D),
inference(paramod,[status(thm)],[c_10509,c_10727]) ).
cnf(c_10729,plain,
inverse(C) = multiply(inverse(C),multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_10518,c_10728]) ).
cnf(c_10525,plain,
multiply(inverse(A),multiply(inverse(B),B)) = inverse(A),
inference(copy,[status(thm)],[c_10729]) ).
cnf(c_10730,plain,
multiply(inverse(inverse(A)),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_10525,c_7857]) ).
cnf(c_10731,plain,
multiply(A,multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_10509,c_10730]) ).
cnf(c_10732,plain,
multiply(A,multiply(inverse(C),C)) = multiply(multiply(inverse(D),inverse(inverse(D))),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_10479,c_10731]) ).
cnf(c_10733,plain,
multiply(A,multiply(inverse(C),C)) = multiply(multiply(inverse(D),D),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_10509,c_10732]) ).
cnf(c_10734,plain,
multiply(A,multiply(inverse(C),C)) = multiply(multiply(inverse(D),D),A),
inference(paramod,[status(thm)],[c_10393,c_10733]) ).
cnf(c_10526,plain,
multiply(A,multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_10393,c_10734]) ).
cnf(c_10735,plain,
multiply(inverse(multiply(inverse(A),inverse(B))),D) = multiply(B,multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10526,c_7498]) ).
cnf(c_10736,plain,
multiply(multiply(inverse(inverse(B)),inverse(inverse(A))),D) = multiply(B,multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10479,c_10735]) ).
cnf(c_10737,plain,
multiply(multiply(B,inverse(inverse(A))),D) = multiply(B,multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10509,c_10736]) ).
cnf(c_10738,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10509,c_10737]) ).
cnf(c_10739,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),inverse(inverse(E))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10479,c_10738]) ).
cnf(c_10740,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),F)),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10509,c_10739]) ).
cnf(c_10741,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(multiply(inverse(F),inverse(inverse(A))),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10479,c_10740]) ).
cnf(c_10742,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(multiply(inverse(F),A),D)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10509,c_10741]) ).
cnf(c_10743,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(multiply(inverse(F),multiply(A,D))),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10518,c_10742]) ).
cnf(c_10744,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(multiply(inverse(multiply(A,D)),inverse(inverse(F))),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10479,c_10743]) ).
cnf(c_10745,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(multiply(multiply(inverse(D),inverse(A)),inverse(inverse(F))),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10479,c_10744]) ).
cnf(c_10746,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(multiply(multiply(inverse(D),inverse(A)),F),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10509,c_10745]) ).
cnf(c_10747,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(multiply(inverse(D),multiply(inverse(A),F)),inverse(multiply(F,multiply(inverse(F),F))))))),
inference(paramod,[status(thm)],[c_10518,c_10746]) ).
cnf(c_10748,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(multiply(inverse(D),multiply(inverse(A),F)),inverse(F))))),
inference(paramod,[status(thm)],[c_10438,c_10747]) ).
cnf(c_10749,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(D),multiply(multiply(inverse(A),F),inverse(F)))))),
inference(paramod,[status(thm)],[c_10518,c_10748]) ).
cnf(c_10750,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),inverse(multiply(inverse(D),multiply(inverse(A),multiply(F,inverse(F))))))),
inference(paramod,[status(thm)],[c_10518,c_10749]) ).
cnf(c_10751,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(inverse(multiply(inverse(A),multiply(F,inverse(F)))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_10479,c_10750]) ).
cnf(c_10752,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(multiply(inverse(multiply(F,inverse(F))),inverse(inverse(A))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_10479,c_10751]) ).
cnf(c_10753,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(multiply(multiply(inverse(inverse(F)),inverse(F)),inverse(inverse(A))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_10479,c_10752]) ).
cnf(c_10754,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(multiply(multiply(F,inverse(F)),inverse(inverse(A))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_10509,c_10753]) ).
cnf(c_10755,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(multiply(multiply(F,inverse(F)),A),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_10509,c_10754]) ).
cnf(c_10756,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(A,inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_10508,c_10755]) ).
cnf(c_10757,plain,
multiply(multiply(B,A),D) = multiply(B,multiply(multiply(inverse(E),E),multiply(A,D))),
inference(paramod,[status(thm)],[c_10509,c_10756]) ).
cnf(c_10534,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_10393,c_10757]) ).
cnf(c_10535,plain,
$false,
inference(resolve,[status(thm)],[c_10534,c_10396]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP049-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 14:15:17 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 2451899 was started by sandbox2 on n017,
% 0.10/0.36 % Fri Sep 25 14:15:17 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.36
% 0.10/0.36 % From the command line: assign(max_seconds, 300).
% 30.27/4.26
% 30.27/4.26 % SZS status Unsatisfiable for theBenchmark
% 30.27/4.26
% 30.27/4.26 % Proof 1 at 3.38 (+ 0.47) seconds.
% 30.27/4.26 % Length of proof is 114.
% 30.27/4.26 % Level of proof is 35.
% 30.27/4.26 % Maximum clause weight is 63.000.
% 30.27/4.26 % Given clauses 122.
% 30.27/4.26
% 30.27/4.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------