%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP422-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:29:15 AM UTC 2026
% Result : Unsatisfiable 48.04s 6.68s
% Output : CNFRefutation 48.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 2
% Syntax : Number of formulae : 245 ( 245 unt; 0 def)
% Number of atoms : 245 ( 244 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 1240 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : inverse(multiply(inverse(multiply(VAR_0,inverse(multiply(inverse(VAR_1),multiply(inverse(VAR_2),inverse(multiply(inverse(VAR_2),VAR_2))))))),multiply(VAR_0,VAR_2))) = VAR_1,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C))) = B,
inference(clausify,[status(thm)],[single_axiom]) ).
fof(prove_these_axioms_2,axiom,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('theBenchmark.p',prove_these_axioms_2) ).
cnf(c_2,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(clausify,[status(thm)],[prove_these_axioms_2]) ).
cnf(c_10728,plain,
inverse(multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C))) = multiply(inverse(multiply(D,inverse(multiply(inverse(B),multiply(inverse(E),inverse(multiply(inverse(E),E))))))),multiply(D,E)),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_3,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C)) = inverse(multiply(inverse(multiply(D,inverse(multiply(B,multiply(inverse(E),inverse(multiply(inverse(E),E))))))),multiply(D,E))),
inference(copy,[status(thm)],[c_10728]) ).
cnf(c_10729,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = multiply(inverse(C),inverse(multiply(inverse(B),multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_4,plain,
multiply(inverse(A),inverse(multiply(inverse(B),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(C,B)),multiply(C,A))),
inference(copy,[status(thm)],[c_10729]) ).
cnf(c_6,plain,
inverse(inverse(multiply(inverse(multiply(A,inverse(multiply(B,multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C)))) = B,
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_8,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(B)),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C)) = B,
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_11,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))),multiply(inverse(C),inverse(multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_13,plain,
multiply(inverse(A),inverse(multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(A),inverse(multiply(inverse(A),A)))))),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = B,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_14,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(D,multiply(inverse(multiply(B,inverse(multiply(inverse(D),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),A))),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_17,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),
inference(paramod,[status(thm)],[c_4,c_4]) ).
cnf(c_10730,plain,
inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,D))),multiply(inverse(E),inverse(multiply(inverse(E),E))))))),multiply(A,E))) = multiply(inverse(multiply(F,C)),multiply(F,D)),
inference(paramod,[status(thm)],[c_17,c_1]) ).
cnf(c_20,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_1,c_10730]) ).
cnf(c_24,plain,
inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(multiply(inverse(D),D))))))),multiply(A,D))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_17,c_1]) ).
cnf(c_10731,plain,
inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))) = inverse(multiply(inverse(multiply(E,multiply(B,C))),multiply(E,D))),
inference(paramod,[status(thm)],[c_1,c_17]) ).
cnf(c_25,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))) = inverse(multiply(E,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),
inference(copy,[status(thm)],[c_10731]) ).
cnf(c_26,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,D))),multiply(inverse(E),inverse(multiply(inverse(E),E))))))),multiply(A,E)) = inverse(multiply(inverse(multiply(F,inverse(multiply(multiply(inverse(multiply(V6,C)),multiply(V6,D)),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),multiply(F,V7))),
inference(paramod,[status(thm)],[c_17,c_3]) ).
cnf(c_37,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,C))),multiply(inverse(multiply(B,E)),A))),
inference(paramod,[status(thm)],[c_17,c_4]) ).
cnf(c_44,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E))) = inverse(multiply(inverse(multiply(F,multiply(D,C))),multiply(F,E))),
inference(paramod,[status(thm)],[c_17,c_17]) ).
cnf(c_55,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E)))) = inverse(multiply(inverse(multiply(F,C)),multiply(F,multiply(A,E)))),
inference(paramod,[status(thm)],[c_20,c_17]) ).
cnf(c_56,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_17,c_20]) ).
cnf(c_57,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_20,c_20]) ).
cnf(c_58,plain,
inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D)))),multiply(inverse(D),inverse(multiply(inverse(D),D))))) = multiply(B,C),
inference(paramod,[status(thm)],[c_1,c_11]) ).
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_17,c_56]) ).
cnf(c_104,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_20,c_56]) ).
cnf(c_154,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_20,c_57]) ).
cnf(c_166,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_57,c_56]) ).
cnf(c_213,plain,
inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,C)))) = inverse(inverse(multiply(inverse(multiply(D,B)),multiply(D,C)))),
inference(paramod,[status(thm)],[c_11,c_6]) ).
cnf(c_313,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_166,c_17]) ).
cnf(c_10732,plain,
multiply(inverse(A),multiply(inverse(B),C)) = multiply(inverse(multiply(D,inverse(multiply(inverse(inverse(multiply(inverse(A),multiply(inverse(B),inverse(multiply(inverse(B),B)))))),multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))))))),multiply(D,C)),
inference(paramod,[status(thm)],[c_13,c_20]) ).
cnf(c_489,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C)))))),multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))))))),multiply(A,D)) = multiply(inverse(B),multiply(inverse(C),D)),
inference(copy,[status(thm)],[c_10732]) ).
cnf(c_10733,plain,
multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(multiply(inverse(A),multiply(inverse(multiply(F,C)),inverse(multiply(inverse(multiply(F,C)),multiply(F,C))))))),multiply(inverse(inverse(multiply(inverse(multiply(F,C)),multiply(F,C)))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(F,C)),multiply(F,C)))),inverse(multiply(inverse(multiply(F,C)),multiply(F,C)))))))))),multiply(E,multiply(F,D))),
inference(paramod,[status(thm)],[c_13,c_57]) ).
cnf(c_494,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_489,c_10733]) ).
cnf(c_10734,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(A),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),multiply(E,F))),multiply(inverse(multiply(V6,C)),multiply(V6,D))),
inference(paramod,[status(thm)],[c_1,c_494]) ).
cnf(c_499,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_1,c_10734]) ).
cnf(c_10735,plain,
inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,F))),multiply(inverse(multiply(D,E)),multiply(D,F))))))))),multiply(A,multiply(inverse(multiply(D,E)),multiply(D,F))))) = multiply(inverse(multiply(inverse(multiply(V6,E)),multiply(V6,F))),C),
inference(paramod,[status(thm)],[c_17,c_24]) ).
cnf(c_754,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_24,c_10735]) ).
cnf(c_757,plain,
inverse(multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(inverse(A),A))))))),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
inference(paramod,[status(thm)],[c_24,c_11]) ).
cnf(c_777,plain,
inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(inverse(A),A))))))),E)))) = inverse(inverse(multiply(inverse(multiply(F,multiply(C,A))),multiply(F,E)))),
inference(paramod,[status(thm)],[c_24,c_213]) ).
cnf(c_1075,plain,
inverse(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))),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_100,c_313]) ).
cnf(c_1375,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,F)))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),C))),multiply(V6,V7)),
inference(paramod,[status(thm)],[c_8,c_104]) ).
cnf(c_1832,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))),multiply(E,F)))),multiply(inverse(F),inverse(multiply(inverse(F),F))))) = multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D),
inference(paramod,[status(thm)],[c_25,c_11]) ).
cnf(c_1860,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,C)))) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_8,c_25]) ).
cnf(c_1862,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))),multiply(E,F)))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_25,c_213]) ).
cnf(c_1872,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E))) = inverse(multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(D,multiply(V6,V7))),E))),
inference(paramod,[status(thm)],[c_25,c_44]) ).
cnf(c_10736,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(inverse(multiply(E,multiply(B,C))),multiply(E,F))) = multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V6,D))),multiply(inverse(multiply(V8,V7)),multiply(V8,F))),
inference(paramod,[status(thm)],[c_25,c_154]) ).
cnf(c_1926,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(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(V8,multiply(V6,V7))),multiply(V8,E))),
inference(copy,[status(thm)],[c_10736]) ).
cnf(c_10737,plain,
multiply(inverse(inverse(multiply(inverse(multiply(A,inverse(multiply(multiply(inverse(multiply(B,C)),multiply(B,D)),multiply(inverse(E),inverse(multiply(inverse(E),E))))))),multiply(A,E)))),F) = multiply(inverse(multiply(inverse(multiply(V6,inverse(multiply(inverse(multiply(inverse(multiply(V7,C)),multiply(V7,D))),multiply(inverse(V8),inverse(multiply(inverse(V8),V8))))))),multiply(V6,V8))),F),
inference(paramod,[status(thm)],[c_26,c_754]) ).
cnf(c_10738,plain,
multiply(multiply(inverse(multiply(B,C)),multiply(B,D)),F) = multiply(inverse(multiply(inverse(multiply(V6,inverse(multiply(inverse(multiply(inverse(multiply(V7,C)),multiply(V7,D))),multiply(inverse(V8),inverse(multiply(inverse(V8),V8))))))),multiply(V6,V8))),F),
inference(paramod,[status(thm)],[c_6,c_10737]) ).
cnf(c_1979,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(A,C)),D) = multiply(multiply(inverse(multiply(E,B)),multiply(E,C)),D),
inference(paramod,[status(thm)],[c_1,c_10738]) ).
cnf(c_10739,plain,
inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(multiply(inverse(inverse(A)),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(B,C)))) = inverse(multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_8,c_1860]) ).
cnf(c_2083,plain,
inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(B),B)),
inference(paramod,[status(thm)],[c_8,c_10739]) ).
cnf(c_10740,plain,
multiply(inverse(A),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,multiply(C,D))),multiply(B,multiply(C,D)))),multiply(inverse(A),inverse(multiply(inverse(A),A)))))),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = multiply(inverse(E),E),
inference(paramod,[status(thm)],[c_1860,c_13]) ).
cnf(c_10741,plain,
multiply(inverse(A),multiply(inverse(multiply(C,inverse(multiply(inverse(inverse(A)),multiply(inverse(D),inverse(multiply(inverse(D),D))))))),multiply(C,D))) = multiply(inverse(E),E),
inference(paramod,[status(thm)],[c_1832,c_10740]) ).
cnf(c_2116,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_8,c_10741]) ).
cnf(c_2236,plain,
multiply(multiply(inverse(A),A),a2) != a2,
inference(paramod,[status(thm)],[c_2116,c_2]) ).
cnf(c_2253,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),
inference(paramod,[status(thm)],[c_2116,c_17]) ).
cnf(c_2254,plain,
inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))) = inverse(multiply(inverse(multiply(D,B)),multiply(D,A))),
inference(paramod,[status(thm)],[c_2116,c_17]) ).
cnf(c_2256,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_2116,c_20]) ).
cnf(c_2257,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,A)),
inference(paramod,[status(thm)],[c_2116,c_20]) ).
cnf(c_2260,plain,
inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(B),B))))) = B,
inference(paramod,[status(thm)],[c_2116,c_11]) ).
cnf(c_10742,plain,
inverse(inverse(multiply(inverse(A),A))) = inverse(inverse(multiply(inverse(multiply(B,C)),multiply(B,C)))),
inference(paramod,[status(thm)],[c_2116,c_213]) ).
cnf(c_2296,plain,
inverse(inverse(multiply(inverse(multiply(A,B)),multiply(A,B)))) = inverse(inverse(multiply(inverse(C),C))),
inference(copy,[status(thm)],[c_10742]) ).
cnf(c_10743,plain,
multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(inverse(multiply(C,D)),multiply(C,D))),
inference(paramod,[status(thm)],[c_2116,c_499]) ).
cnf(c_2340,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(B,C))) = multiply(A,multiply(inverse(D),D)),
inference(copy,[status(thm)],[c_10743]) ).
cnf(c_2353,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(D,multiply(inverse(multiply(B,inverse(multiply(inverse(D),multiply(inverse(C),inverse(multiply(inverse(E),E))))))),A))),
inference(paramod,[status(thm)],[c_2116,c_14]) ).
cnf(c_10744,plain,
multiply(inverse(multiply(inverse(A),A)),B) = multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,D))),B),
inference(paramod,[status(thm)],[c_2116,c_754]) ).
cnf(c_2382,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,B))),C) = multiply(inverse(multiply(inverse(D),D)),C),
inference(copy,[status(thm)],[c_10744]) ).
cnf(c_2423,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))) = inverse(multiply(E,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(F),F))))))),D))),
inference(paramod,[status(thm)],[c_2116,c_25]) ).
cnf(c_2455,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_2083,c_2116]) ).
cnf(c_2636,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_2083,c_2455]) ).
cnf(c_2646,plain,
multiply(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)),a2) != a2,
inference(paramod,[status(thm)],[c_2083,c_2236]) ).
cnf(c_3005,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(inverse(C),D))),multiply(inverse(multiply(E,B)),multiply(E,F)))) = inverse(multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,D))),multiply(inverse(multiply(inverse(V7),V7)),multiply(A,F)))),
inference(paramod,[status(thm)],[c_2256,c_55]) ).
cnf(c_3184,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(F,multiply(D,A))),V6))) = inverse(multiply(inverse(multiply(V7,multiply(F,E))),multiply(V7,V6))),
inference(paramod,[status(thm)],[c_2257,c_44]) ).
cnf(c_3414,plain,
multiply(A,multiply(inverse(B),B)) = multiply(A,multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_2116,c_2340]) ).
cnf(c_3442,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),F))) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
inference(paramod,[status(thm)],[c_3414,c_44]) ).
cnf(c_3628,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(E),E))),multiply(inverse(multiply(B,D)),A))),
inference(paramod,[status(thm)],[c_2116,c_37]) ).
cnf(c_3629,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),multiply(inverse(multiply(inverse(E),E)),A))),
inference(paramod,[status(thm)],[c_2116,c_37]) ).
cnf(c_3647,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))),multiply(inverse(multiply(B,C)),A))),
inference(paramod,[status(thm)],[c_2455,c_37]) ).
cnf(c_3679,plain,
multiply(inverse(A),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(A),A)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),multiply(inverse(multiply(B,multiply(inverse(F),F))),A))),
inference(paramod,[status(thm)],[c_3414,c_37]) ).
cnf(c_4091,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),C) = multiply(inverse(multiply(inverse(D),D)),C),
inference(paramod,[status(thm)],[c_2116,c_2382]) ).
cnf(c_4188,plain,
inverse(inverse(multiply(inverse(A),A))) = inverse(inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_2116,c_2296]) ).
cnf(c_4254,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_4188,c_2116]) ).
cnf(c_4261,plain,
multiply(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(C),C)))),a2) != a2,
inference(paramod,[status(thm)],[c_4188,c_2646]) ).
cnf(c_4701,plain,
multiply(multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(multiply(inverse(C),C)))),a2) != a2,
inference(paramod,[status(thm)],[c_20,c_4261]) ).
cnf(c_5342,plain,
inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_2116,c_2260]) ).
cnf(c_5394,plain,
inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),B))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_4254,c_2260]) ).
cnf(c_5455,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D)))),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D)))))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
inference(paramod,[status(thm)],[c_313,c_5342]) ).
cnf(c_5456,plain,
inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(multiply(C,multiply(D,E))),multiply(C,multiply(D,F)))),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
inference(paramod,[status(thm)],[c_313,c_5342]) ).
cnf(c_10745,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(multiply(B,C)),D)),E))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,V7))),multiply(inverse(multiply(B,V6)),D))),multiply(inverse(multiply(inverse(multiply(V8,C)),multiply(V8,V7))),E))),
inference(paramod,[status(thm)],[c_100,c_2253]) ).
cnf(c_6556,plain,
inverse(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))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
inference(copy,[status(thm)],[c_10745]) ).
cnf(c_10746,plain,
inverse(multiply(inverse(multiply(inverse(A),multiply(inverse(multiply(B,C)),D))),multiply(inverse(E),E))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,V7))),multiply(inverse(multiply(B,V6)),D))),multiply(inverse(multiply(inverse(multiply(V8,C)),multiply(V8,V7))),A))),
inference(paramod,[status(thm)],[c_100,c_2254]) ).
cnf(c_6798,plain,
inverse(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))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
inference(copy,[status(thm)],[c_10746]) ).
cnf(c_6950,plain,
inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(E),E))),multiply(inverse(multiply(F,D)),multiply(F,C))))))) = B,
inference(paramod,[status(thm)],[c_2254,c_5342]) ).
cnf(c_10747,plain,
multiply(multiply(inverse(A),A),B) = multiply(multiply(inverse(multiply(C,D)),multiply(C,D)),B),
inference(paramod,[status(thm)],[c_2116,c_1979]) ).
cnf(c_9652,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(A,B)),C) = multiply(multiply(inverse(D),D),C),
inference(copy,[status(thm)],[c_10747]) ).
cnf(c_9845,plain,
multiply(multiply(inverse(multiply(multiply(inverse(multiply(A,B)),multiply(A,B)),inverse(multiply(inverse(C),C)))),multiply(multiply(inverse(D),D),inverse(multiply(inverse(E),E)))),a2) != a2,
inference(paramod,[status(thm)],[c_9652,c_4701]) ).
cnf(c_10104,plain,
multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(inverse(multiply(D,multiply(inverse(E),inverse(multiply(inverse(E),E))))),multiply(D,inverse(multiply(F,multiply(inverse(multiply(A,inverse(multiply(inverse(F),multiply(inverse(B),inverse(multiply(inverse(B),B))))))),E))))),
inference(paramod,[status(thm)],[c_58,c_2257]) ).
cnf(c_10107,plain,
inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(B,D))))),multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(E),E)))))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_2257,c_58]) ).
cnf(c_10111,plain,
inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(inverse(D),D))))),multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(E),E)))))) = multiply(B,C),
inference(paramod,[status(thm)],[c_3414,c_58]) ).
cnf(c_10148,plain,
inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(inverse(multiply(inverse(D),D))),inverse(multiply(inverse(D),D))))))) = multiply(A,C),
inference(paramod,[status(thm)],[c_5342,c_58]) ).
cnf(c_10748,plain,
inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(multiply(B,inverse(multiply(inverse(inverse(inverse(multiply(inverse(C),C)))),multiply(inverse(D),inverse(multiply(inverse(D),D))))))),inverse(multiply(inverse(multiply(B,inverse(multiply(inverse(inverse(inverse(multiply(inverse(C),C)))),multiply(inverse(D),inverse(multiply(inverse(D),D))))))),multiply(B,inverse(multiply(inverse(inverse(inverse(multiply(inverse(C),C)))),multiply(inverse(D),inverse(multiply(inverse(D),D))))))))))) = multiply(B,D),
inference(paramod,[status(thm)],[c_5394,c_58]) ).
cnf(c_10152,plain,
multiply(A,inverse(multiply(inverse(inverse(inverse(multiply(inverse(B),B)))),multiply(inverse(C),inverse(multiply(inverse(C),C)))))) = multiply(A,C),
inference(paramod,[status(thm)],[c_5342,c_10748]) ).
cnf(c_10177,plain,
inverse(multiply(inverse(inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D)))),multiply(inverse(D),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(multiply(inverse(F),F)),multiply(inverse(V6),V6))))))) = multiply(B,C),
inference(paramod,[status(thm)],[c_2636,c_58]) ).
cnf(c_10749,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(multiply(C,inverse(multiply(inverse(inverse(multiply(inverse(D),D))),multiply(inverse(E),inverse(multiply(inverse(E),E))))))),F)))),multiply(inverse(F),inverse(multiply(inverse(F),F))))) = multiply(C,E),
inference(paramod,[status(thm)],[c_4091,c_58]) ).
cnf(c_10181,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(multiply(C,D)),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,D),
inference(paramod,[status(thm)],[c_5342,c_10749]) ).
cnf(c_10189,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))))) = multiply(A,B),
inference(paramod,[status(thm)],[c_10152,c_10148]) ).
cnf(c_10750,plain,
multiply(inverse(A),multiply(B,C)) = inverse(multiply(inverse(multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C))),multiply(inverse(multiply(B,multiply(inverse(F),F))),A))),
inference(paramod,[status(thm)],[c_10189,c_3679]) ).
cnf(c_10250,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,C))),multiply(inverse(multiply(D,multiply(inverse(E),E))),F))) = multiply(inverse(F),multiply(D,C)),
inference(copy,[status(thm)],[c_10750]) ).
cnf(c_10751,plain,
multiply(inverse(A),multiply(B,C)) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))),multiply(inverse(multiply(B,C)),A))),
inference(paramod,[status(thm)],[c_10189,c_3647]) ).
cnf(c_10280,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(multiply(C,D)),E))) = multiply(inverse(E),multiply(C,D)),
inference(copy,[status(thm)],[c_10751]) ).
cnf(c_10752,plain,
multiply(inverse(A),multiply(inverse(B),C)) = inverse(multiply(inverse(multiply(inverse(multiply(D,B)),multiply(D,C))),multiply(inverse(multiply(inverse(E),E)),A))),
inference(paramod,[status(thm)],[c_10189,c_3629]) ).
cnf(c_10293,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(inverse(D),D)),E))) = multiply(inverse(E),multiply(inverse(B),C)),
inference(copy,[status(thm)],[c_10752]) ).
cnf(c_10753,plain,
multiply(inverse(A),multiply(B,C)) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(E),E))),multiply(inverse(multiply(B,D)),A))),
inference(paramod,[status(thm)],[c_10189,c_3628]) ).
cnf(c_10294,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))),multiply(inverse(multiply(D,B)),E))) = multiply(inverse(E),multiply(D,A)),
inference(copy,[status(thm)],[c_10753]) ).
cnf(c_10754,plain,
multiply(inverse(A),multiply(B,C)) = inverse(multiply(D,multiply(inverse(multiply(B,inverse(multiply(inverse(D),multiply(inverse(C),inverse(multiply(inverse(E),E))))))),A))),
inference(paramod,[status(thm)],[c_10189,c_2353]) ).
cnf(c_10334,plain,
inverse(multiply(A,multiply(inverse(multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),inverse(multiply(inverse(D),D))))))),E))) = multiply(inverse(E),multiply(B,C)),
inference(copy,[status(thm)],[c_10754]) ).
cnf(c_10755,plain,
multiply(inverse(F),multiply(D,C)) = inverse(multiply(inverse(multiply(V6,multiply(D,C))),multiply(V6,F))),
inference(paramod,[status(thm)],[c_10250,c_3442]) ).
cnf(c_10366,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))) = multiply(inverse(D),multiply(B,C)),
inference(copy,[status(thm)],[c_10755]) ).
cnf(c_10756,plain,
inverse(multiply(multiply(inverse(E),multiply(D,A)),multiply(inverse(multiply(F,multiply(D,A))),V6))) = inverse(multiply(inverse(multiply(V7,multiply(F,E))),multiply(V7,V6))),
inference(paramod,[status(thm)],[c_10294,c_3184]) ).
cnf(c_10369,plain,
inverse(multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(multiply(D,multiply(B,C))),E))) = multiply(inverse(E),multiply(D,A)),
inference(paramod,[status(thm)],[c_10366,c_10756]) ).
cnf(c_10757,plain,
inverse(multiply(inverse(multiply(inverse(E),multiply(C,D))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,D),
inference(paramod,[status(thm)],[c_10280,c_10181]) ).
cnf(c_10372,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),multiply(B,C)) = multiply(B,C),
inference(paramod,[status(thm)],[c_10366,c_10757]) ).
cnf(c_10426,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(inverse(C),D))),multiply(inverse(multiply(E,B)),multiply(E,F)))) = multiply(inverse(multiply(A,F)),multiply(inverse(C),D)),
inference(paramod,[status(thm)],[c_10293,c_3005]) ).
cnf(c_10758,plain,
inverse(multiply(inverse(inverse(multiply(inverse(A),A))),multiply(inverse(B),multiply(inverse(multiply(inverse(C),C)),multiply(inverse(E),E))))) = B,
inference(paramod,[status(thm)],[c_10426,c_6950]) ).
cnf(c_10446,plain,
inverse(multiply(inverse(A),multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C)))) = A,
inference(paramod,[status(thm)],[c_10372,c_10758]) ).
cnf(c_10759,plain,
inverse(multiply(inverse(multiply(inverse(D),multiply(B,C))),multiply(inverse(D),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(multiply(inverse(F),F)),multiply(inverse(V6),V6))))))) = multiply(B,C),
inference(paramod,[status(thm)],[c_10334,c_10177]) ).
cnf(c_10760,plain,
inverse(multiply(inverse(multiply(inverse(D),multiply(B,C))),multiply(inverse(D),multiply(inverse(E),E)))) = multiply(B,C),
inference(paramod,[status(thm)],[c_10446,c_10759]) ).
cnf(c_10507,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(B,C)) = multiply(B,C),
inference(paramod,[status(thm)],[c_10366,c_10760]) ).
cnf(c_10761,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(B,C))),multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(E),E)))))) = multiply(B,C),
inference(paramod,[status(thm)],[c_10334,c_10111]) ).
cnf(c_10762,plain,
inverse(multiply(inverse(multiply(B,C)),multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(E),E)))))) = multiply(B,C),
inference(paramod,[status(thm)],[c_10507,c_10761]) ).
cnf(c_10530,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(C),C))))) = multiply(A,B),
inference(paramod,[status(thm)],[c_10507,c_10762]) ).
cnf(c_10763,plain,
inverse(multiply(inverse(multiply(inverse(multiply(B,D)),multiply(B,C))),multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(multiply(inverse(E),E)),multiply(inverse(E),E)))))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_10334,c_10107]) ).
cnf(c_10764,plain,
inverse(multiply(inverse(multiply(inverse(multiply(B,D)),multiply(B,C))),multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(E),E))))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_10507,c_10763]) ).
cnf(c_10533,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_10530,c_10764]) ).
cnf(c_10765,plain,
multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(inverse(multiply(D,multiply(inverse(E),inverse(multiply(inverse(E),E))))),multiply(D,multiply(inverse(E),multiply(A,B)))),
inference(paramod,[status(thm)],[c_10334,c_10104]) ).
cnf(c_10766,plain,
multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(E),inverse(multiply(inverse(E),E)))),multiply(inverse(E),multiply(A,B))),
inference(paramod,[status(thm)],[c_10533,c_10765]) ).
cnf(c_10767,plain,
multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(inverse(inverse(multiply(inverse(E),E))),multiply(A,B)),
inference(paramod,[status(thm)],[c_10533,c_10766]) ).
cnf(c_10536,plain,
multiply(multiply(A,B),multiply(inverse(C),C)) = multiply(A,B),
inference(paramod,[status(thm)],[c_10372,c_10767]) ).
cnf(c_10768,plain,
inverse(multiply(inverse(multiply(B,C)),D)) = inverse(multiply(E,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(F),F))))))),D))),
inference(paramod,[status(thm)],[c_10533,c_2423]) ).
cnf(c_10578,plain,
inverse(multiply(inverse(multiply(A,B)),C)) = multiply(inverse(C),multiply(A,B)),
inference(paramod,[status(thm)],[c_10334,c_10768]) ).
cnf(c_10769,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(V8,multiply(V6,V7))),multiply(V8,E))),
inference(paramod,[status(thm)],[c_10533,c_1926]) ).
cnf(c_10770,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),E)) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(V8,multiply(V6,V7))),multiply(V8,E))),
inference(paramod,[status(thm)],[c_10533,c_10769]) ).
cnf(c_10771,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(V8,multiply(V6,V7))),multiply(V8,E))),
inference(paramod,[status(thm)],[c_10533,c_10770]) ).
cnf(c_10772,plain,
multiply(inverse(C),E) = multiply(multiply(inverse(C),multiply(V6,V7)),multiply(inverse(multiply(V8,multiply(V6,V7))),multiply(V8,E))),
inference(paramod,[status(thm)],[c_10334,c_10771]) ).
cnf(c_10773,plain,
multiply(inverse(C),E) = multiply(multiply(inverse(C),multiply(V6,V7)),multiply(inverse(multiply(V6,V7)),E)),
inference(paramod,[status(thm)],[c_10533,c_10772]) ).
cnf(c_10599,plain,
multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(multiply(B,C)),D)) = multiply(inverse(A),D),
inference(copy,[status(thm)],[c_10773]) ).
cnf(c_10774,plain,
inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),E))) = inverse(multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(D,multiply(V6,V7))),E))),
inference(paramod,[status(thm)],[c_10533,c_1872]) ).
cnf(c_10775,plain,
multiply(inverse(multiply(inverse(multiply(D,B)),E)),multiply(inverse(B),C)) = inverse(multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(D,multiply(V6,V7))),E))),
inference(paramod,[status(thm)],[c_10578,c_10774]) ).
cnf(c_10776,plain,
multiply(multiply(inverse(E),multiply(D,B)),multiply(inverse(B),C)) = inverse(multiply(inverse(multiply(F,multiply(inverse(multiply(V6,inverse(multiply(inverse(F),multiply(inverse(V7),inverse(multiply(inverse(V7),V7))))))),C))),multiply(inverse(multiply(D,multiply(V6,V7))),E))),
inference(paramod,[status(thm)],[c_10578,c_10775]) ).
cnf(c_10777,plain,
multiply(multiply(inverse(E),multiply(D,B)),multiply(inverse(B),C)) = inverse(multiply(multiply(inverse(C),multiply(V6,V7)),multiply(inverse(multiply(D,multiply(V6,V7))),E))),
inference(paramod,[status(thm)],[c_10334,c_10776]) ).
cnf(c_10615,plain,
multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(C),D)) = multiply(inverse(A),multiply(B,D)),
inference(paramod,[status(thm)],[c_10369,c_10777]) ).
cnf(c_10778,plain,
inverse(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))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
inference(paramod,[status(thm)],[c_10533,c_6798]) ).
cnf(c_10779,plain,
inverse(multiply(multiply(inverse(multiply(inverse(multiply(D,B)),E)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
inference(paramod,[status(thm)],[c_10578,c_10778]) ).
cnf(c_10780,plain,
inverse(multiply(multiply(multiply(inverse(E),multiply(D,B)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
inference(paramod,[status(thm)],[c_10578,c_10779]) ).
cnf(c_10781,plain,
inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
inference(paramod,[status(thm)],[c_10615,c_10780]) ).
cnf(c_10782,plain,
inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(V6),C)),V7))) = inverse(multiply(inverse(multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),multiply(inverse(V8),V8))),
inference(paramod,[status(thm)],[c_10533,c_10781]) ).
cnf(c_10783,plain,
inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(V6),C)),V7))) = multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E))),
inference(paramod,[status(thm)],[c_10578,c_10782]) ).
cnf(c_10645,plain,
inverse(multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(multiply(inverse(D),C)),E))) = multiply(inverse(E),multiply(inverse(multiply(B,D)),A)),
inference(paramod,[status(thm)],[c_10507,c_10783]) ).
cnf(c_10784,plain,
inverse(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))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
inference(paramod,[status(thm)],[c_10533,c_6556]) ).
cnf(c_10785,plain,
inverse(multiply(multiply(inverse(multiply(inverse(multiply(D,B)),E)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
inference(paramod,[status(thm)],[c_10578,c_10784]) ).
cnf(c_10786,plain,
inverse(multiply(multiply(multiply(inverse(E),multiply(D,B)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
inference(paramod,[status(thm)],[c_10578,c_10785]) ).
cnf(c_10787,plain,
inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),V7))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
inference(paramod,[status(thm)],[c_10615,c_10786]) ).
cnf(c_10788,plain,
inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(V6),C)),V7))) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
inference(paramod,[status(thm)],[c_10533,c_10787]) ).
cnf(c_10789,plain,
multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E)) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(inverse(multiply(inverse(multiply(D,V6)),E)),V7))),
inference(paramod,[status(thm)],[c_10645,c_10788]) ).
cnf(c_10790,plain,
multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E)) = inverse(multiply(inverse(multiply(inverse(V8),V8)),multiply(multiply(inverse(E),multiply(D,V6)),V7))),
inference(paramod,[status(thm)],[c_10578,c_10789]) ).
cnf(c_10791,plain,
multiply(inverse(V7),multiply(inverse(multiply(D,V6)),E)) = inverse(multiply(multiply(inverse(E),multiply(D,V6)),V7)),
inference(paramod,[status(thm)],[c_10507,c_10790]) ).
cnf(c_10646,plain,
inverse(multiply(multiply(inverse(A),multiply(B,C)),D)) = multiply(inverse(D),multiply(inverse(multiply(B,C)),A)),
inference(copy,[status(thm)],[c_10791]) ).
cnf(c_10792,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),E))),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_10533,c_1075]) ).
cnf(c_10793,plain,
inverse(multiply(multiply(inverse(multiply(inverse(multiply(D,B)),E)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_10578,c_10792]) ).
cnf(c_10794,plain,
inverse(multiply(multiply(multiply(inverse(E),multiply(D,B)),multiply(inverse(B),C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_10578,c_10793]) ).
cnf(c_10795,plain,
inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,C))),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_10615,c_10794]) ).
cnf(c_10796,plain,
inverse(multiply(multiply(inverse(E),multiply(D,C)),multiply(inverse(multiply(inverse(V6),C)),multiply(inverse(multiply(D,V6)),V7)))) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_10533,c_10795]) ).
cnf(c_10797,plain,
multiply(inverse(multiply(inverse(multiply(inverse(V6),C)),multiply(inverse(multiply(D,V6)),V7))),multiply(inverse(multiply(D,C)),E)) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_10646,c_10796]) ).
cnf(c_10798,plain,
multiply(multiply(inverse(multiply(inverse(multiply(D,V6)),V7)),multiply(inverse(V6),C)),multiply(inverse(multiply(D,C)),E)) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_10578,c_10797]) ).
cnf(c_10799,plain,
multiply(multiply(multiply(inverse(V7),multiply(D,V6)),multiply(inverse(V6),C)),multiply(inverse(multiply(D,C)),E)) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_10578,c_10798]) ).
cnf(c_10800,plain,
multiply(multiply(inverse(V7),multiply(D,C)),multiply(inverse(multiply(D,C)),E)) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_10615,c_10799]) ).
cnf(c_10801,plain,
multiply(inverse(V7),E) = inverse(multiply(inverse(multiply(V8,multiply(V9,E))),multiply(V8,multiply(V9,V7)))),
inference(paramod,[status(thm)],[c_10599,c_10800]) ).
cnf(c_10802,plain,
multiply(inverse(V7),E) = inverse(multiply(inverse(multiply(V9,E)),multiply(V9,V7))),
inference(paramod,[status(thm)],[c_10533,c_10801]) ).
cnf(c_10803,plain,
multiply(inverse(V7),E) = inverse(multiply(inverse(E),V7)),
inference(paramod,[status(thm)],[c_10533,c_10802]) ).
cnf(c_10659,plain,
inverse(multiply(inverse(A),B)) = multiply(inverse(B),A),
inference(copy,[status(thm)],[c_10803]) ).
cnf(c_10804,plain,
inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(E,F)))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_10533,c_1862]) ).
cnf(c_10805,plain,
inverse(inverse(multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_10659,c_10804]) ).
cnf(c_10806,plain,
inverse(multiply(inverse(multiply(E,F)),multiply(inverse(multiply(B,C)),D))) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_10646,c_10805]) ).
cnf(c_10807,plain,
multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_10659,c_10806]) ).
cnf(c_10808,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_10659,c_10807]) ).
cnf(c_10809,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,inverse(multiply(inverse(E),multiply(inverse(C),multiply(inverse(C),C)))))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_10659,c_10808]) ).
cnf(c_10810,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,multiply(inverse(multiply(inverse(C),multiply(inverse(C),C))),E))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_10659,c_10809]) ).
cnf(c_10811,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,multiply(multiply(inverse(multiply(inverse(C),C)),C),E))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_10659,c_10810]) ).
cnf(c_10812,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(V6,multiply(inverse(multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),D))),multiply(V6,F)))),
inference(paramod,[status(thm)],[c_10659,c_10811]) ).
cnf(c_10813,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),D)),F))),
inference(paramod,[status(thm)],[c_10533,c_10812]) ).
cnf(c_10814,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(inverse(multiply(multiply(inverse(D),multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),F))),
inference(paramod,[status(thm)],[c_10659,c_10813]) ).
cnf(c_10815,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = inverse(multiply(inverse(F),multiply(inverse(multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),D))),
inference(paramod,[status(thm)],[c_10646,c_10814]) ).
cnf(c_10816,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = multiply(inverse(multiply(inverse(multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),D)),F),
inference(paramod,[status(thm)],[c_10659,c_10815]) ).
cnf(c_10817,plain,
multiply(multiply(inverse(D),multiply(B,C)),multiply(E,F)) = multiply(multiply(inverse(D),multiply(B,multiply(multiply(multiply(inverse(C),C),C),E))),F),
inference(paramod,[status(thm)],[c_10659,c_10816]) ).
cnf(c_10688,plain,
multiply(multiply(inverse(A),multiply(B,multiply(multiply(multiply(inverse(C),C),C),D))),E) = multiply(multiply(inverse(A),multiply(B,C)),multiply(D,E)),
inference(copy,[status(thm)],[c_10817]) ).
cnf(c_10818,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,F)))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),C))),multiply(V6,V7)),
inference(paramod,[status(thm)],[c_10533,c_1375]) ).
cnf(c_10819,plain,
multiply(multiply(inverse(C),B),multiply(inverse(multiply(D,B)),multiply(D,multiply(E,F)))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),C))),multiply(V6,V7)),
inference(paramod,[status(thm)],[c_10659,c_10818]) ).
cnf(c_10820,plain,
multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),inverse(multiply(inverse(F),F))))))),C))),multiply(V6,V7)),
inference(paramod,[status(thm)],[c_10533,c_10819]) ).
cnf(c_10821,plain,
multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,inverse(multiply(inverse(inverse(V7)),multiply(inverse(F),multiply(inverse(F),F)))))),C))),multiply(V6,V7)),
inference(paramod,[status(thm)],[c_10659,c_10820]) ).
cnf(c_10822,plain,
multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,multiply(inverse(multiply(inverse(F),multiply(inverse(F),F))),inverse(V7)))),C))),multiply(V6,V7)),
inference(paramod,[status(thm)],[c_10659,c_10821]) ).
cnf(c_10823,plain,
multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,multiply(multiply(inverse(multiply(inverse(F),F)),F),inverse(V7)))),C))),multiply(V6,V7)),
inference(paramod,[status(thm)],[c_10659,c_10822]) ).
cnf(c_10824,plain,
multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(V6,multiply(inverse(multiply(E,multiply(multiply(multiply(inverse(F),F),F),inverse(V7)))),C))),multiply(V6,V7)),
inference(paramod,[status(thm)],[c_10659,c_10823]) ).
cnf(c_10825,plain,
multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(inverse(multiply(inverse(multiply(E,multiply(multiply(multiply(inverse(F),F),F),inverse(V7)))),C)),V7),
inference(paramod,[status(thm)],[c_10533,c_10824]) ).
cnf(c_10826,plain,
multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(multiply(inverse(C),multiply(E,multiply(multiply(multiply(inverse(F),F),F),inverse(V7)))),V7),
inference(paramod,[status(thm)],[c_10659,c_10825]) ).
cnf(c_10827,plain,
multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(E,F))) = multiply(multiply(inverse(C),multiply(E,F)),multiply(inverse(V7),V7)),
inference(paramod,[status(thm)],[c_10688,c_10826]) ).
cnf(c_10689,plain,
multiply(multiply(inverse(A),B),multiply(inverse(B),multiply(C,D))) = multiply(inverse(A),multiply(C,D)),
inference(paramod,[status(thm)],[c_10536,c_10827]) ).
cnf(c_10828,plain,
inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(A),A)))))),E)))) = inverse(inverse(multiply(inverse(multiply(F,multiply(C,A))),multiply(F,E)))),
inference(paramod,[status(thm)],[c_10659,c_777]) ).
cnf(c_10829,plain,
inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(B),multiply(inverse(A),A))))),E)))) = inverse(inverse(multiply(inverse(multiply(F,multiply(C,A))),multiply(F,E)))),
inference(paramod,[status(thm)],[c_10533,c_10828]) ).
cnf(c_10830,plain,
inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(A),A)),B))),E)))) = inverse(inverse(multiply(inverse(multiply(F,multiply(C,A))),multiply(F,E)))),
inference(paramod,[status(thm)],[c_10659,c_10829]) ).
cnf(c_10831,plain,
inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),B))),E)))) = inverse(inverse(multiply(inverse(multiply(F,multiply(C,A))),multiply(F,E)))),
inference(paramod,[status(thm)],[c_10659,c_10830]) ).
cnf(c_10832,plain,
inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),B))),E)))) = inverse(inverse(multiply(inverse(multiply(C,A)),E))),
inference(paramod,[status(thm)],[c_10533,c_10831]) ).
cnf(c_10833,plain,
inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),B))),E)))) = inverse(multiply(inverse(E),multiply(C,A))),
inference(paramod,[status(thm)],[c_10659,c_10832]) ).
cnf(c_10701,plain,
inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),B))),D)))) = multiply(inverse(multiply(C,A)),D),
inference(paramod,[status(thm)],[c_10659,c_10833]) ).
cnf(c_10834,plain,
inverse(multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(D,B)),multiply(D,multiply(inverse(A),A)))))),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
inference(paramod,[status(thm)],[c_10659,c_757]) ).
cnf(c_10835,plain,
inverse(multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,inverse(multiply(inverse(B),multiply(inverse(A),A))))),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
inference(paramod,[status(thm)],[c_10533,c_10834]) ).
cnf(c_10836,plain,
inverse(multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(A),A)),B))),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
inference(paramod,[status(thm)],[c_10659,c_10835]) ).
cnf(c_10837,plain,
inverse(multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(multiply(C,multiply(multiply(inverse(A),A),B))),E)))),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
inference(paramod,[status(thm)],[c_10659,c_10836]) ).
cnf(c_10838,plain,
inverse(multiply(multiply(inverse(multiply(C,A)),E),multiply(inverse(E),inverse(multiply(inverse(E),E))))) = multiply(C,A),
inference(paramod,[status(thm)],[c_10701,c_10837]) ).
cnf(c_10839,plain,
inverse(multiply(multiply(inverse(multiply(C,A)),E),multiply(inverse(E),multiply(inverse(E),E)))) = multiply(C,A),
inference(paramod,[status(thm)],[c_10659,c_10838]) ).
cnf(c_10840,plain,
inverse(multiply(inverse(multiply(C,A)),multiply(inverse(E),E))) = multiply(C,A),
inference(paramod,[status(thm)],[c_10689,c_10839]) ).
cnf(c_10841,plain,
multiply(inverse(multiply(inverse(E),E)),multiply(C,A)) = multiply(C,A),
inference(paramod,[status(thm)],[c_10659,c_10840]) ).
cnf(c_10702,plain,
multiply(multiply(inverse(A),A),multiply(B,C)) = multiply(B,C),
inference(paramod,[status(thm)],[c_10659,c_10841]) ).
cnf(c_10842,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(multiply(C,multiply(D,E))),multiply(C,multiply(D,F)))),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
inference(paramod,[status(thm)],[c_10659,c_5456]) ).
cnf(c_10843,plain,
inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(multiply(C,multiply(D,E))),multiply(C,multiply(D,F)))),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
inference(paramod,[status(thm)],[c_10659,c_10842]) ).
cnf(c_10844,plain,
inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,F))),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
inference(paramod,[status(thm)],[c_10533,c_10843]) ).
cnf(c_10845,plain,
inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(inverse(multiply(inverse(E),F)),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
inference(paramod,[status(thm)],[c_10533,c_10844]) ).
cnf(c_10846,plain,
inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(multiply(inverse(F),E),multiply(inverse(multiply(V6,multiply(V7,E))),multiply(V6,multiply(V7,F)))))))) = B,
inference(paramod,[status(thm)],[c_10659,c_10845]) ).
cnf(c_10847,plain,
inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(multiply(inverse(F),E),multiply(inverse(multiply(V7,E)),multiply(V7,F))))))) = B,
inference(paramod,[status(thm)],[c_10533,c_10846]) ).
cnf(c_10848,plain,
inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),inverse(multiply(multiply(inverse(F),E),multiply(inverse(E),F)))))) = B,
inference(paramod,[status(thm)],[c_10533,c_10847]) ).
cnf(c_10849,plain,
inverse(multiply(inverse(B),inverse(multiply(multiply(inverse(F),E),multiply(inverse(E),F))))) = B,
inference(paramod,[status(thm)],[c_10702,c_10848]) ).
cnf(c_10725,plain,
multiply(inverse(inverse(multiply(multiply(inverse(A),B),multiply(inverse(B),A)))),C) = C,
inference(paramod,[status(thm)],[c_10659,c_10849]) ).
cnf(c_10850,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,D))),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D)))))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
inference(paramod,[status(thm)],[c_10533,c_5455]) ).
cnf(c_10851,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(C),D)),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D)))))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
inference(paramod,[status(thm)],[c_10533,c_10850]) ).
cnf(c_10852,plain,
inverse(multiply(inverse(inverse(multiply(multiply(inverse(D),C),multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D)))))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
inference(paramod,[status(thm)],[c_10659,c_10851]) ).
cnf(c_10853,plain,
inverse(multiply(inverse(inverse(multiply(multiply(inverse(D),C),multiply(inverse(multiply(F,C)),multiply(F,D))))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
inference(paramod,[status(thm)],[c_10533,c_10852]) ).
cnf(c_10854,plain,
inverse(multiply(inverse(inverse(multiply(multiply(inverse(D),C),multiply(inverse(C),D)))),multiply(inverse(V6),inverse(multiply(inverse(V7),V7))))) = V6,
inference(paramod,[status(thm)],[c_10533,c_10853]) ).
cnf(c_10855,plain,
inverse(multiply(inverse(inverse(multiply(multiply(inverse(D),C),multiply(inverse(C),D)))),multiply(inverse(V6),multiply(inverse(V7),V7)))) = V6,
inference(paramod,[status(thm)],[c_10659,c_10854]) ).
cnf(c_10856,plain,
inverse(multiply(inverse(V6),multiply(inverse(V7),V7))) = V6,
inference(paramod,[status(thm)],[c_10725,c_10855]) ).
cnf(c_10857,plain,
multiply(inverse(multiply(inverse(V7),V7)),V6) = V6,
inference(paramod,[status(thm)],[c_10659,c_10856]) ).
cnf(c_10726,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_10659,c_10857]) ).
cnf(c_10727,plain,
$false,
inference(resolve,[status(thm)],[c_10726,c_9845]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP422-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.52 % Computer : n026.cluster.edu
% 0.10/0.52 % Model : x86_64 x86_64
% 0.10/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.52 % Memory : 8046.5625MB
% 0.10/0.52 % OS : Linux 6.8.0-71-generic
% 0.10/0.52 % CPULimit : 300
% 0.10/0.52 % WCLimit : 300
% 0.10/0.52 % DateTime : Fri Sep 25 14:56:10 UTC 2026
% 0.10/0.53 % CPUTime :
% 0.10/0.53 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.53 % Process 2814576 was started by sandbox on n026,
% 0.10/0.53 % Fri Sep 25 14:56:10 2026
% 0.10/0.53 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.53
% 0.10/0.53 % From the command line: assign(max_seconds, 300).
% 48.04/6.68
% 48.04/6.68 % SZS status Unsatisfiable for theBenchmark
% 48.04/6.68
% 48.04/6.68 % Proof 1 at 5.12 (+ 0.94) seconds.
% 48.04/6.68 % Length of proof is 113.
% 48.04/6.68 % Level of proof is 29.
% 48.04/6.68 % Maximum clause weight is 92.000.
% 48.04/6.68 % Given clauses 124.
% 48.04/6.68
% 48.04/6.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------