%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP050-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:33 AM UTC 2026
% Result : Unsatisfiable 8.72s 1.68s
% Output : CNFRefutation 8.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 95
% Number of leaves : 2
% Syntax : Number of formulae : 213 ( 201 unt; 0 def)
% Number of atoms : 228 ( 227 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 43 ( 28 ~; 15 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 876 ( 0 sgn 3 !; 0 ?)
% 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)),multiply(inverse(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)),multiply(inverse(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_773,plain,
multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(C),C))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,C)),D)),B)),multiply(inverse(D),multiply(inverse(D),D)))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_4,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(B),B))))),
inference(copy,[status(thm)],[c_773]) ).
cnf(c_5,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(C),multiply(inverse(B),multiply(inverse(B),B)))))) = C,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_6,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(A,B)),D))),multiply(inverse(C),multiply(inverse(C),C)))) = D,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_7,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(C,inverse(multiply(inverse(D),multiply(inverse(E),multiply(inverse(E),E))))))) = multiply(inverse(multiply(inverse(multiply(C,E)),B)),D),
inference(paramod,[status(thm)],[c_4,c_5]) ).
cnf(c_774,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(C,D)),A)),multiply(inverse(D),multiply(inverse(D),D)))))),E))),multiply(inverse(B),multiply(inverse(B),B)))) = E,
inference(paramod,[status(thm)],[c_1,c_6]) ).
cnf(c_8,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(A),C))),multiply(inverse(B),multiply(inverse(B),B)))) = C,
inference(paramod,[status(thm)],[c_1,c_774]) ).
cnf(c_775,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(inverse(multiply(D,E)),B)),multiply(inverse(multiply(D,E)),C)),
inference(paramod,[status(thm)],[c_6,c_5]) ).
cnf(c_9,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(A,B)),D)) = multiply(inverse(multiply(E,C)),multiply(E,D)),
inference(copy,[status(thm)],[c_775]) ).
cnf(c_776,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),E)),multiply(inverse(multiply(C,D)),A))),multiply(inverse(E),multiply(inverse(E),E)))),F))),multiply(inverse(B),multiply(inverse(B),B)))) = F,
inference(paramod,[status(thm)],[c_6,c_6]) ).
cnf(c_10,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(B),multiply(inverse(B),B)))) = C,
inference(paramod,[status(thm)],[c_8,c_776]) ).
cnf(c_16,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
inference(paramod,[status(thm)],[c_9,c_9]) ).
cnf(c_777,plain,
multiply(inverse(multiply(A,B)),C) = multiply(inverse(multiply(D,B)),multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(A,E)),C)),multiply(inverse(E),multiply(inverse(E),E)))))),
inference(paramod,[status(thm)],[c_1,c_16]) ).
cnf(c_22,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(C,D)),E)),multiply(inverse(D),multiply(inverse(D),D)))))) = multiply(inverse(multiply(C,B)),E),
inference(copy,[status(thm)],[c_777]) ).
cnf(c_23,plain,
multiply(inverse(multiply(A,multiply(B,C))),multiply(A,inverse(multiply(inverse(D),multiply(inverse(multiply(B,C)),multiply(inverse(multiply(E,C)),multiply(E,C))))))) = D,
inference(paramod,[status(thm)],[c_16,c_5]) ).
cnf(c_24,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,D)),multiply(C,multiply(inverse(B),B)))))) = multiply(inverse(B),D),
inference(paramod,[status(thm)],[c_16,c_5]) ).
cnf(c_25,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_16,c_16]) ).
cnf(c_26,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_16,c_16]) ).
cnf(c_28,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),multiply(inverse(B),B)))) = inverse(multiply(inverse(multiply(inverse(multiply(A,D)),C)),multiply(inverse(D),multiply(inverse(D),D)))),
inference(paramod,[status(thm)],[c_1,c_10]) ).
cnf(c_29,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E)))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,E),
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_778,plain,
multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,A))),D)) = multiply(inverse(multiply(E,multiply(inverse(C),multiply(inverse(C),C)))),multiply(E,D)),
inference(paramod,[status(thm)],[c_10,c_16]) ).
cnf(c_30,plain,
multiply(inverse(multiply(A,multiply(inverse(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_778]) ).
cnf(c_779,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),D) = multiply(inverse(multiply(E,multiply(F,C))),multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,B)),V6)),D)),multiply(inverse(V6),multiply(inverse(V6),V6)))))),
inference(paramod,[status(thm)],[c_1,c_25]) ).
cnf(c_32,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_22,c_779]) ).
cnf(c_780,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(inverse(multiply(C,D)),inverse(multiply(inverse(E),multiply(inverse(multiply(C,F)),multiply(inverse(multiply(C,F)),multiply(C,F)))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(V6,D)),multiply(V6,F))),B)),E),
inference(paramod,[status(thm)],[c_16,c_7]) ).
cnf(c_37,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),D)),E) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,B)),multiply(F,C))),D)),E),
inference(paramod,[status(thm)],[c_7,c_780]) ).
cnf(c_49,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_26,c_25]) ).
cnf(c_781,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),E)),multiply(inverse(D),multiply(inverse(D),D)))),multiply(inverse(B),multiply(inverse(B),B)))))) = multiply(inverse(multiply(inverse(multiply(C,F)),E)),multiply(inverse(F),multiply(inverse(F),F))),
inference(paramod,[status(thm)],[c_28,c_5]) ).
cnf(c_102,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(multiply(A,D)),C)),multiply(inverse(D),multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_5,c_781]) ).
cnf(c_782,plain,
multiply(inverse(multiply(A,multiply(inverse(multiply(B,C)),multiply(B,inverse(D))))),multiply(A,inverse(multiply(inverse(multiply(E,multiply(inverse(C),multiply(inverse(C),C)))),multiply(E,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(D)))),multiply(inverse(multiply(B,C)),multiply(B,inverse(D))))))))) = D,
inference(paramod,[status(thm)],[c_30,c_5]) ).
cnf(c_110,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),multiply(inverse(B),multiply(inverse(B),B))) = C,
inference(paramod,[status(thm)],[c_24,c_782]) ).
cnf(c_111,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_10,c_30]) ).
cnf(c_122,plain,
multiply(inverse(A),A) = multiply(B,multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,B))),multiply(inverse(D),multiply(inverse(D),D)))),
inference(paramod,[status(thm)],[c_110,c_111]) ).
cnf(c_783,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(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))))),multiply(inverse(E),multiply(inverse(E),E)))),multiply(inverse(F),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_122,c_4]) ).
cnf(c_784,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(B),B)))) = multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(C,F)),B)),multiply(inverse(F),multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_110,c_783]) ).
cnf(c_136,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(B),B)))) = B,
inference(paramod,[status(thm)],[c_1,c_784]) ).
cnf(c_785,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,inverse(B)))),multiply(inverse(E),multiply(inverse(E),E))))),multiply(C,multiply(inverse(B),B)))))) = multiply(inverse(F),F),
inference(paramod,[status(thm)],[c_122,c_24]) ).
cnf(c_786,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,B)),multiply(C,multiply(inverse(B),B)))))) = multiply(inverse(F),F),
inference(paramod,[status(thm)],[c_110,c_785]) ).
cnf(c_144,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_24,c_786]) ).
cnf(c_164,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2 ),
inference(resolve,[status(thm)],[c_144,c_3]) ).
cnf(c_169,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_144,c_4]) ).
cnf(c_176,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,A)),
inference(paramod,[status(thm)],[c_144,c_16]) ).
cnf(c_186,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(C,inverse(multiply(inverse(D),multiply(inverse(E),multiply(inverse(F),F))))))) = multiply(inverse(multiply(inverse(multiply(C,E)),B)),D),
inference(paramod,[status(thm)],[c_144,c_7]) ).
cnf(c_201,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),inverse(multiply(inverse(multiply(C,D)),multiply(C,multiply(inverse(B),B)))))) = multiply(inverse(B),D),
inference(paramod,[status(thm)],[c_144,c_24]) ).
cnf(c_202,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),multiply(inverse(B),B)))))) = multiply(inverse(B),D),
inference(paramod,[status(thm)],[c_144,c_24]) ).
cnf(c_203,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,D)),multiply(C,multiply(inverse(E),E)))))) = multiply(inverse(B),D),
inference(paramod,[status(thm)],[c_144,c_24]) ).
cnf(c_218,plain,
multiply(inverse(multiply(A,multiply(inverse(B),C))),multiply(A,multiply(inverse(D),D))) = multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,B))),
inference(paramod,[status(thm)],[c_144,c_49]) ).
cnf(c_242,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),C)),D)),multiply(inverse(E),multiply(inverse(E),E)))))) = multiply(inverse(multiply(inverse(E),B)),D),
inference(paramod,[status(thm)],[c_144,c_22]) ).
cnf(c_787,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),C)),D)),multiply(inverse(C),multiply(inverse(C),C)))))) = multiply(inverse(multiply(inverse(E),E)),D),
inference(paramod,[status(thm)],[c_144,c_22]) ).
cnf(c_244,plain,
multiply(inverse(multiply(inverse(A),A)),B) = multiply(inverse(multiply(inverse(C),C)),B),
inference(paramod,[status(thm)],[c_22,c_787]) ).
cnf(c_788,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(C),multiply(inverse(C),C))) = multiply(inverse(multiply(inverse(multiply(inverse(C),D)),B)),multiply(inverse(D),multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_144,c_102]) ).
cnf(c_253,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),B)),C)),multiply(inverse(B),multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(multiply(inverse(D),D)),C)),multiply(inverse(A),multiply(inverse(A),A))),
inference(copy,[status(thm)],[c_788]) ).
cnf(c_259,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,inverse(multiply(inverse(C),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(E,B)),multiply(E,B))))))) = C,
inference(paramod,[status(thm)],[c_144,c_23]) ).
cnf(c_268,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),B)),multiply(inverse(C),C))),multiply(inverse(B),multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_144,c_110]) ).
cnf(c_269,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),multiply(inverse(inverse(B)),inverse(B)))) = B,
inference(paramod,[status(thm)],[c_144,c_110]) ).
cnf(c_281,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E)))),multiply(inverse(C),multiply(inverse(F),F)))) = multiply(A,E),
inference(paramod,[status(thm)],[c_144,c_29]) ).
cnf(c_282,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(A),A),a2) != a2 ),
inference(paramod,[status(thm)],[c_144,c_164]) ).
cnf(c_304,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_244,c_144]) ).
cnf(c_789,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(A,E)),C)),multiply(inverse(multiply(inverse(F),F)),multiply(inverse(V6),V6))),
inference(paramod,[status(thm)],[c_304,c_26]) ).
cnf(c_371,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(V6,F)),multiply(V6,B))),
inference(copy,[status(thm)],[c_789]) ).
cnf(c_790,plain,
multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,F))),B)),multiply(inverse(multiply(inverse(multiply(V6,E)),multiply(V6,F))),A)),
inference(paramod,[status(thm)],[c_32,c_176]) ).
cnf(c_479,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),D)),multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),F)) = multiply(inverse(multiply(inverse(F),D)),multiply(inverse(V6),V6)),
inference(copy,[status(thm)],[c_790]) ).
cnf(c_480,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(V6),V6))),multiply(F,multiply(inverse(C),E))),
inference(paramod,[status(thm)],[c_176,c_26]) ).
cnf(c_483,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(V6,A))),multiply(F,multiply(V6,E))),
inference(paramod,[status(thm)],[c_176,c_26]) ).
cnf(c_791,plain,
multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D)))),E) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,D)),multiply(F,C))),multiply(inverse(V6),V6))),E),
inference(paramod,[status(thm)],[c_176,c_37]) ).
cnf(c_490,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(D),D))),E) = multiply(inverse(multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,B)))),E),
inference(copy,[status(thm)],[c_791]) ).
cnf(c_507,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(B),B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),E)),A)),
inference(paramod,[status(thm)],[c_304,c_176]) ).
cnf(c_526,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)),a2) != a2 ),
inference(paramod,[status(thm)],[c_244,c_282]) ).
cnf(c_527,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(C),C)),a2) != a2 ),
inference(paramod,[status(thm)],[c_244,c_526]) ).
cnf(c_792,plain,
multiply(A,multiply(inverse(multiply(B,A)),C)) = multiply(inverse(multiply(D,multiply(B,multiply(inverse(A),A)))),multiply(D,C)),
inference(paramod,[status(thm)],[c_136,c_25]) ).
cnf(c_533,plain,
multiply(inverse(multiply(A,multiply(B,multiply(inverse(C),C)))),multiply(A,D)) = multiply(C,multiply(inverse(multiply(B,C)),D)),
inference(copy,[status(thm)],[c_792]) ).
cnf(c_555,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(C),C)))) = B,
inference(paramod,[status(thm)],[c_144,c_136]) ).
cnf(c_574,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(B,C)),multiply(B,D)))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_176,c_136]) ).
cnf(c_587,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_555,c_202]) ).
cnf(c_793,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(D),multiply(inverse(E),E))))) = multiply(inverse(B),D),
inference(paramod,[status(thm)],[c_587,c_203]) ).
cnf(c_593,plain,
multiply(inverse(A),inverse(multiply(inverse(B),multiply(inverse(C),C)))) = multiply(inverse(A),B),
inference(paramod,[status(thm)],[c_587,c_793]) ).
cnf(c_794,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),inverse(multiply(inverse(D),multiply(inverse(B),B))))) = multiply(inverse(B),D),
inference(paramod,[status(thm)],[c_587,c_201]) ).
cnf(c_594,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_593,c_794]) ).
cnf(c_795,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(C),D))) = multiply(inverse(D),C),
inference(paramod,[status(thm)],[c_587,c_574]) ).
cnf(c_611,plain,
inverse(multiply(inverse(A),B)) = multiply(inverse(B),A),
inference(paramod,[status(thm)],[c_594,c_795]) ).
cnf(c_624,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),C) = multiply(B,multiply(inverse(multiply(A,B)),C)),
inference(paramod,[status(thm)],[c_587,c_533]) ).
cnf(c_796,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(D),D))),E) = multiply(inverse(multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,B)))),E),
inference(paramod,[status(thm)],[c_587,c_490]) ).
cnf(c_797,plain,
multiply(inverse(multiply(multiply(inverse(C),B),multiply(inverse(D),D))),E) = multiply(inverse(multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,B)))),E),
inference(paramod,[status(thm)],[c_611,c_796]) ).
cnf(c_798,plain,
multiply(D,multiply(inverse(multiply(multiply(inverse(C),B),D)),E)) = multiply(inverse(multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,B)))),E),
inference(paramod,[status(thm)],[c_624,c_797]) ).
cnf(c_799,plain,
multiply(D,multiply(inverse(multiply(multiply(inverse(C),B),D)),E)) = multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,B))),E),
inference(paramod,[status(thm)],[c_587,c_798]) ).
cnf(c_800,plain,
multiply(D,multiply(inverse(multiply(multiply(inverse(C),B),D)),E)) = multiply(inverse(multiply(inverse(C),B)),E),
inference(paramod,[status(thm)],[c_587,c_799]) ).
cnf(c_653,plain,
multiply(A,multiply(inverse(multiply(multiply(inverse(B),C),A)),D)) = multiply(multiply(inverse(C),B),D),
inference(paramod,[status(thm)],[c_611,c_800]) ).
cnf(c_801,plain,
multiply(inverse(multiply(multiply(inverse(B),A),multiply(inverse(C),C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(V6,A))),multiply(F,multiply(V6,E))),
inference(paramod,[status(thm)],[c_611,c_483]) ).
cnf(c_802,plain,
multiply(inverse(multiply(multiply(inverse(B),A),multiply(inverse(C),C))),multiply(inverse(B),E)) = multiply(inverse(multiply(F,multiply(V6,A))),multiply(F,multiply(V6,E))),
inference(paramod,[status(thm)],[c_587,c_801]) ).
cnf(c_803,plain,
multiply(C,multiply(inverse(multiply(multiply(inverse(B),A),C)),multiply(inverse(B),E))) = multiply(inverse(multiply(F,multiply(V6,A))),multiply(F,multiply(V6,E))),
inference(paramod,[status(thm)],[c_624,c_802]) ).
cnf(c_804,plain,
multiply(multiply(inverse(A),B),multiply(inverse(B),E)) = multiply(inverse(multiply(F,multiply(V6,A))),multiply(F,multiply(V6,E))),
inference(paramod,[status(thm)],[c_653,c_803]) ).
cnf(c_805,plain,
multiply(multiply(inverse(A),B),multiply(inverse(B),E)) = multiply(inverse(multiply(V6,A)),multiply(V6,E)),
inference(paramod,[status(thm)],[c_587,c_804]) ).
cnf(c_658,plain,
multiply(multiply(inverse(A),B),multiply(inverse(B),C)) = multiply(inverse(A),C),
inference(paramod,[status(thm)],[c_587,c_805]) ).
cnf(c_806,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
inference(paramod,[status(thm)],[c_587,c_480]) ).
cnf(c_807,plain,
multiply(multiply(inverse(C),B),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
inference(paramod,[status(thm)],[c_611,c_806]) ).
cnf(c_808,plain,
multiply(multiply(inverse(C),B),multiply(inverse(B),E)) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
inference(paramod,[status(thm)],[c_587,c_807]) ).
cnf(c_809,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
inference(paramod,[status(thm)],[c_658,c_808]) ).
cnf(c_810,plain,
multiply(inverse(C),E) = multiply(inverse(multiply(inverse(V6),V6)),multiply(inverse(C),E)),
inference(paramod,[status(thm)],[c_587,c_809]) ).
cnf(c_811,plain,
multiply(inverse(C),E) = multiply(multiply(inverse(V6),V6),multiply(inverse(C),E)),
inference(paramod,[status(thm)],[c_611,c_810]) ).
cnf(c_661,plain,
multiply(multiply(inverse(A),A),multiply(inverse(B),C)) = multiply(inverse(B),C),
inference(copy,[status(thm)],[c_811]) ).
cnf(c_812,plain,
multiply(inverse(multiply(inverse(multiply(inverse(B),C)),D)),multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),F)) = multiply(inverse(multiply(inverse(F),D)),multiply(inverse(V6),V6)),
inference(paramod,[status(thm)],[c_587,c_479]) ).
cnf(c_813,plain,
multiply(inverse(multiply(multiply(inverse(C),B),D)),multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,C))),F)) = multiply(inverse(multiply(inverse(F),D)),multiply(inverse(V6),V6)),
inference(paramod,[status(thm)],[c_611,c_812]) ).
cnf(c_814,plain,
multiply(inverse(multiply(multiply(inverse(C),B),D)),multiply(inverse(multiply(inverse(B),C)),F)) = multiply(inverse(multiply(inverse(F),D)),multiply(inverse(V6),V6)),
inference(paramod,[status(thm)],[c_587,c_813]) ).
cnf(c_815,plain,
multiply(inverse(multiply(multiply(inverse(C),B),D)),multiply(multiply(inverse(C),B),F)) = multiply(inverse(multiply(inverse(F),D)),multiply(inverse(V6),V6)),
inference(paramod,[status(thm)],[c_611,c_814]) ).
cnf(c_816,plain,
multiply(inverse(D),F) = multiply(inverse(multiply(inverse(F),D)),multiply(inverse(V6),V6)),
inference(paramod,[status(thm)],[c_587,c_815]) ).
cnf(c_817,plain,
multiply(inverse(D),F) = multiply(multiply(inverse(D),F),multiply(inverse(V6),V6)),
inference(paramod,[status(thm)],[c_611,c_816]) ).
cnf(c_662,plain,
multiply(multiply(inverse(A),B),multiply(inverse(C),C)) = multiply(inverse(A),B),
inference(copy,[status(thm)],[c_817]) ).
cnf(c_818,plain,
multiply(multiply(inverse(C),multiply(A,B)),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(V6,F)),multiply(V6,B))),
inference(paramod,[status(thm)],[c_611,c_371]) ).
cnf(c_819,plain,
multiply(multiply(inverse(C),multiply(A,B)),multiply(multiply(inverse(D),D),multiply(inverse(E),E))) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(V6,F)),multiply(V6,B))),
inference(paramod,[status(thm)],[c_611,c_818]) ).
cnf(c_820,plain,
multiply(multiply(inverse(C),multiply(A,B)),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(V6,F)),multiply(V6,B))),
inference(paramod,[status(thm)],[c_661,c_819]) ).
cnf(c_821,plain,
multiply(inverse(C),multiply(A,B)) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(V6,F)),multiply(V6,B))),
inference(paramod,[status(thm)],[c_662,c_820]) ).
cnf(c_822,plain,
multiply(inverse(C),multiply(A,B)) = multiply(multiply(inverse(C),multiply(A,F)),multiply(inverse(multiply(V6,F)),multiply(V6,B))),
inference(paramod,[status(thm)],[c_611,c_821]) ).
cnf(c_823,plain,
multiply(inverse(C),multiply(A,B)) = multiply(multiply(inverse(C),multiply(A,F)),multiply(inverse(F),B)),
inference(paramod,[status(thm)],[c_587,c_822]) ).
cnf(c_693,plain,
multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(C),D)) = multiply(inverse(A),multiply(B,D)),
inference(copy,[status(thm)],[c_823]) ).
cnf(c_824,plain,
inverse(multiply(inverse(multiply(multiply(inverse(C),multiply(A,B)),multiply(inverse(multiply(D,B)),multiply(D,E)))),multiply(inverse(C),multiply(inverse(F),F)))) = multiply(A,E),
inference(paramod,[status(thm)],[c_611,c_281]) ).
cnf(c_825,plain,
inverse(multiply(inverse(multiply(multiply(inverse(C),multiply(A,B)),multiply(inverse(B),E))),multiply(inverse(C),multiply(inverse(F),F)))) = multiply(A,E),
inference(paramod,[status(thm)],[c_587,c_824]) ).
cnf(c_826,plain,
inverse(multiply(inverse(multiply(inverse(C),multiply(A,E))),multiply(inverse(C),multiply(inverse(F),F)))) = multiply(A,E),
inference(paramod,[status(thm)],[c_693,c_825]) ).
cnf(c_827,plain,
inverse(multiply(multiply(inverse(multiply(A,E)),C),multiply(inverse(C),multiply(inverse(F),F)))) = multiply(A,E),
inference(paramod,[status(thm)],[c_611,c_826]) ).
cnf(c_828,plain,
inverse(multiply(inverse(multiply(A,E)),multiply(inverse(F),F))) = multiply(A,E),
inference(paramod,[status(thm)],[c_658,c_827]) ).
cnf(c_829,plain,
multiply(inverse(multiply(inverse(F),F)),multiply(A,E)) = multiply(A,E),
inference(paramod,[status(thm)],[c_611,c_828]) ).
cnf(c_715,plain,
multiply(multiply(inverse(A),A),multiply(B,C)) = multiply(B,C),
inference(paramod,[status(thm)],[c_611,c_829]) ).
cnf(c_830,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,inverse(multiply(inverse(C),multiply(multiply(inverse(D),D),multiply(inverse(multiply(E,B)),multiply(E,B))))))) = C,
inference(paramod,[status(thm)],[c_611,c_259]) ).
cnf(c_831,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,inverse(multiply(inverse(C),multiply(multiply(inverse(D),D),multiply(inverse(B),B)))))) = C,
inference(paramod,[status(thm)],[c_587,c_830]) ).
cnf(c_832,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,inverse(multiply(inverse(C),multiply(inverse(B),B))))) = C,
inference(paramod,[status(thm)],[c_715,c_831]) ).
cnf(c_833,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,multiply(inverse(multiply(inverse(B),B)),C))) = C,
inference(paramod,[status(thm)],[c_611,c_832]) ).
cnf(c_834,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,multiply(multiply(inverse(B),B),C))) = C,
inference(paramod,[status(thm)],[c_611,c_833]) ).
cnf(c_835,plain,
multiply(inverse(multiply(inverse(B),B)),multiply(multiply(inverse(B),B),C)) = C,
inference(paramod,[status(thm)],[c_587,c_834]) ).
cnf(c_836,plain,
multiply(multiply(inverse(B),B),multiply(multiply(inverse(B),B),C)) = C,
inference(paramod,[status(thm)],[c_611,c_835]) ).
cnf(c_720,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_715,c_836]) ).
cnf(c_837,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(C),C),D)),multiply(inverse(E),multiply(inverse(E),E)))))) = multiply(inverse(multiply(inverse(E),B)),D),
inference(paramod,[status(thm)],[c_611,c_242]) ).
cnf(c_838,plain,
multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(D),multiply(inverse(E),multiply(inverse(E),E)))))) = multiply(inverse(multiply(inverse(E),B)),D),
inference(paramod,[status(thm)],[c_720,c_837]) ).
cnf(c_839,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(inverse(multiply(inverse(E),multiply(inverse(E),E))),D))) = multiply(inverse(multiply(inverse(E),B)),D),
inference(paramod,[status(thm)],[c_611,c_838]) ).
cnf(c_840,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(multiply(inverse(multiply(inverse(E),E)),E),D))) = multiply(inverse(multiply(inverse(E),B)),D),
inference(paramod,[status(thm)],[c_611,c_839]) ).
cnf(c_841,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(multiply(multiply(inverse(E),E),E),D))) = multiply(inverse(multiply(inverse(E),B)),D),
inference(paramod,[status(thm)],[c_611,c_840]) ).
cnf(c_842,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(E,D))) = multiply(inverse(multiply(inverse(E),B)),D),
inference(paramod,[status(thm)],[c_720,c_841]) ).
cnf(c_843,plain,
multiply(inverse(B),multiply(E,D)) = multiply(inverse(multiply(inverse(E),B)),D),
inference(paramod,[status(thm)],[c_587,c_842]) ).
cnf(c_844,plain,
multiply(inverse(B),multiply(E,D)) = multiply(multiply(inverse(B),E),D),
inference(paramod,[status(thm)],[c_611,c_843]) ).
cnf(c_723,plain,
multiply(multiply(inverse(A),B),C) = multiply(inverse(A),multiply(B,C)),
inference(copy,[status(thm)],[c_844]) ).
cnf(c_845,plain,
multiply(inverse(multiply(inverse(B),C)),multiply(inverse(D),D)) = multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,B))),
inference(paramod,[status(thm)],[c_587,c_218]) ).
cnf(c_846,plain,
multiply(multiply(inverse(C),B),multiply(inverse(D),D)) = multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,B))),
inference(paramod,[status(thm)],[c_611,c_845]) ).
cnf(c_847,plain,
multiply(inverse(C),multiply(B,multiply(inverse(D),D))) = multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,B))),
inference(paramod,[status(thm)],[c_723,c_846]) ).
cnf(c_848,plain,
multiply(inverse(C),multiply(B,multiply(inverse(D),D))) = multiply(inverse(multiply(F,C)),multiply(F,B)),
inference(paramod,[status(thm)],[c_587,c_847]) ).
cnf(c_732,plain,
multiply(inverse(A),multiply(B,multiply(inverse(C),C))) = multiply(inverse(A),B),
inference(paramod,[status(thm)],[c_587,c_848]) ).
cnf(c_849,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(C,inverse(multiply(inverse(D),inverse(E)))))) = multiply(inverse(multiply(inverse(multiply(C,E)),B)),D),
inference(paramod,[status(thm)],[c_732,c_186]) ).
cnf(c_850,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(C,multiply(inverse(inverse(E)),D)))) = multiply(inverse(multiply(inverse(multiply(C,E)),B)),D),
inference(paramod,[status(thm)],[c_611,c_849]) ).
cnf(c_851,plain,
multiply(inverse(B),multiply(C,multiply(inverse(inverse(E)),D))) = multiply(inverse(multiply(inverse(multiply(C,E)),B)),D),
inference(paramod,[status(thm)],[c_587,c_850]) ).
cnf(c_852,plain,
multiply(inverse(B),multiply(C,multiply(inverse(inverse(E)),D))) = multiply(multiply(inverse(B),multiply(C,E)),D),
inference(paramod,[status(thm)],[c_611,c_851]) ).
cnf(c_853,plain,
multiply(inverse(B),multiply(C,multiply(inverse(inverse(E)),D))) = multiply(inverse(B),multiply(multiply(C,E),D)),
inference(paramod,[status(thm)],[c_723,c_852]) ).
cnf(c_737,plain,
multiply(inverse(A),multiply(multiply(B,C),D)) = multiply(inverse(A),multiply(B,multiply(inverse(inverse(C)),D))),
inference(copy,[status(thm)],[c_853]) ).
cnf(c_854,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),multiply(inverse(C),C)),a2) != a2 ),
inference(paramod,[status(thm)],[c_611,c_527]) ).
cnf(c_855,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C)),a2) != a2 ),
inference(paramod,[status(thm)],[c_720,c_854]) ).
cnf(c_856,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(multiply(inverse(B),B),multiply(inverse(C),C)),a2) != a2 ),
inference(paramod,[status(thm)],[c_611,c_855]) ).
cnf(c_857,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(C),C),a2) != a2 ),
inference(paramod,[status(thm)],[c_720,c_856]) ).
cnf(c_858,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_720,c_857]) ).
cnf(c_750,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(copy,[status(thm)],[c_858]) ).
cnf(c_859,plain,
multiply(multiply(inverse(multiply(inverse(B),B)),A),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),E)),A)),
inference(paramod,[status(thm)],[c_611,c_507]) ).
cnf(c_860,plain,
multiply(multiply(multiply(inverse(B),B),A),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),E)),A)),
inference(paramod,[status(thm)],[c_611,c_859]) ).
cnf(c_861,plain,
multiply(A,multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),E)),A)),
inference(paramod,[status(thm)],[c_720,c_860]) ).
cnf(c_862,plain,
multiply(A,multiply(inverse(C),C)) = multiply(multiply(inverse(D),D),multiply(inverse(multiply(inverse(E),E)),A)),
inference(paramod,[status(thm)],[c_611,c_861]) ).
cnf(c_863,plain,
multiply(A,multiply(inverse(C),C)) = multiply(multiply(inverse(D),D),multiply(multiply(inverse(E),E),A)),
inference(paramod,[status(thm)],[c_611,c_862]) ).
cnf(c_864,plain,
multiply(A,multiply(inverse(C),C)) = multiply(multiply(inverse(D),D),A),
inference(paramod,[status(thm)],[c_720,c_863]) ).
cnf(c_753,plain,
multiply(A,multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_720,c_864]) ).
cnf(c_865,plain,
multiply(multiply(inverse(A),A),multiply(inverse(inverse(B)),multiply(inverse(inverse(B)),inverse(B)))) = B,
inference(paramod,[status(thm)],[c_611,c_269]) ).
cnf(c_866,plain,
multiply(multiply(inverse(A),A),inverse(inverse(B))) = B,
inference(paramod,[status(thm)],[c_753,c_865]) ).
cnf(c_758,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_720,c_866]) ).
cnf(c_867,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(inverse(C),C))),multiply(inverse(B),multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_758,c_268]) ).
cnf(c_868,plain,
multiply(inverse(inverse(multiply(A,B))),multiply(inverse(B),multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_753,c_867]) ).
cnf(c_869,plain,
multiply(multiply(A,B),multiply(inverse(B),multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_758,c_868]) ).
cnf(c_765,plain,
multiply(multiply(A,B),inverse(B)) = A,
inference(paramod,[status(thm)],[c_753,c_869]) ).
cnf(c_870,plain,
multiply(inverse(multiply(multiply(inverse(B),A),C)),multiply(inverse(B),multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(multiply(inverse(D),D)),C)),multiply(inverse(A),multiply(inverse(A),A))),
inference(paramod,[status(thm)],[c_611,c_253]) ).
cnf(c_871,plain,
multiply(inverse(multiply(inverse(B),multiply(A,C))),multiply(inverse(B),multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(multiply(inverse(D),D)),C)),multiply(inverse(A),multiply(inverse(A),A))),
inference(paramod,[status(thm)],[c_723,c_870]) ).
cnf(c_872,plain,
multiply(multiply(inverse(multiply(A,C)),B),multiply(inverse(B),multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(multiply(inverse(D),D)),C)),multiply(inverse(A),multiply(inverse(A),A))),
inference(paramod,[status(thm)],[c_611,c_871]) ).
cnf(c_873,plain,
multiply(multiply(inverse(multiply(A,C)),B),inverse(B)) = multiply(inverse(multiply(inverse(multiply(inverse(D),D)),C)),multiply(inverse(A),multiply(inverse(A),A))),
inference(paramod,[status(thm)],[c_753,c_872]) ).
cnf(c_874,plain,
inverse(multiply(A,C)) = multiply(inverse(multiply(inverse(multiply(inverse(D),D)),C)),multiply(inverse(A),multiply(inverse(A),A))),
inference(paramod,[status(thm)],[c_765,c_873]) ).
cnf(c_875,plain,
inverse(multiply(A,C)) = multiply(inverse(multiply(multiply(inverse(D),D),C)),multiply(inverse(A),multiply(inverse(A),A))),
inference(paramod,[status(thm)],[c_611,c_874]) ).
cnf(c_876,plain,
inverse(multiply(A,C)) = multiply(inverse(C),multiply(inverse(A),multiply(inverse(A),A))),
inference(paramod,[status(thm)],[c_720,c_875]) ).
cnf(c_770,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(paramod,[status(thm)],[c_753,c_876]) ).
cnf(c_877,plain,
inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(B),inverse(A)),C)),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_770,c_169]) ).
cnf(c_878,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(A),C))),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_723,c_877]) ).
cnf(c_879,plain,
inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(A),C)),inverse(inverse(B))),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_770,c_878]) ).
cnf(c_880,plain,
inverse(multiply(inverse(multiply(multiply(multiply(inverse(C),inverse(inverse(A))),inverse(inverse(B))),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_770,c_879]) ).
cnf(c_881,plain,
inverse(multiply(inverse(multiply(multiply(multiply(inverse(C),A),inverse(inverse(B))),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_758,c_880]) ).
cnf(c_882,plain,
inverse(multiply(inverse(multiply(multiply(multiply(inverse(C),A),B),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_758,c_881]) ).
cnf(c_883,plain,
inverse(multiply(inverse(multiply(multiply(inverse(C),multiply(A,B)),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_723,c_882]) ).
cnf(c_884,plain,
inverse(multiply(inverse(multiply(inverse(C),multiply(multiply(A,B),D))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_723,c_883]) ).
cnf(c_885,plain,
inverse(multiply(inverse(multiply(inverse(C),multiply(A,multiply(inverse(inverse(B)),D)))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_737,c_884]) ).
cnf(c_886,plain,
inverse(multiply(inverse(multiply(inverse(C),multiply(A,multiply(B,D)))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_758,c_885]) ).
cnf(c_887,plain,
inverse(multiply(multiply(inverse(multiply(A,multiply(B,D))),inverse(inverse(C))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_770,c_886]) ).
cnf(c_888,plain,
inverse(multiply(multiply(multiply(inverse(multiply(B,D)),inverse(A)),inverse(inverse(C))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_770,c_887]) ).
cnf(c_889,plain,
inverse(multiply(multiply(multiply(multiply(inverse(D),inverse(B)),inverse(A)),inverse(inverse(C))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_770,c_888]) ).
cnf(c_890,plain,
inverse(multiply(multiply(multiply(inverse(D),multiply(inverse(B),inverse(A))),inverse(inverse(C))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_723,c_889]) ).
cnf(c_891,plain,
inverse(multiply(multiply(multiply(inverse(D),multiply(inverse(B),inverse(A))),C),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_758,c_890]) ).
cnf(c_892,plain,
inverse(multiply(multiply(inverse(D),multiply(multiply(inverse(B),inverse(A)),C)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_723,c_891]) ).
cnf(c_893,plain,
inverse(multiply(multiply(inverse(D),multiply(inverse(B),multiply(inverse(A),C))),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_723,c_892]) ).
cnf(c_894,plain,
inverse(multiply(multiply(inverse(D),multiply(inverse(B),multiply(inverse(A),C))),inverse(C))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_753,c_893]) ).
cnf(c_895,plain,
inverse(multiply(inverse(D),multiply(multiply(inverse(B),multiply(inverse(A),C)),inverse(C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_723,c_894]) ).
cnf(c_896,plain,
inverse(multiply(inverse(D),multiply(inverse(B),multiply(multiply(inverse(A),C),inverse(C))))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_723,c_895]) ).
cnf(c_897,plain,
inverse(multiply(inverse(D),multiply(inverse(B),inverse(A)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_765,c_896]) ).
cnf(c_898,plain,
multiply(inverse(multiply(inverse(B),inverse(A))),inverse(inverse(D))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_770,c_897]) ).
cnf(c_899,plain,
multiply(multiply(inverse(inverse(A)),inverse(inverse(B))),inverse(inverse(D))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_770,c_898]) ).
cnf(c_900,plain,
multiply(multiply(A,inverse(inverse(B))),inverse(inverse(D))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_758,c_899]) ).
cnf(c_901,plain,
multiply(multiply(A,B),inverse(inverse(D))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_758,c_900]) ).
cnf(c_902,plain,
multiply(multiply(A,B),D) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(E),E))))),
inference(paramod,[status(thm)],[c_758,c_901]) ).
cnf(c_903,plain,
multiply(multiply(A,B),D) = multiply(A,inverse(multiply(inverse(D),inverse(B)))),
inference(paramod,[status(thm)],[c_753,c_902]) ).
cnf(c_904,plain,
multiply(multiply(A,B),D) = multiply(A,multiply(inverse(inverse(B)),inverse(inverse(D)))),
inference(paramod,[status(thm)],[c_770,c_903]) ).
cnf(c_905,plain,
multiply(multiply(A,B),D) = multiply(A,multiply(B,inverse(inverse(D)))),
inference(paramod,[status(thm)],[c_758,c_904]) ).
cnf(c_771,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_758,c_905]) ).
cnf(c_772,plain,
$false,
inference(resolve,[status(thm)],[c_771,c_750]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP050-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n020.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Fri Sep 25 14:21:03 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.44 % Process 3099757 was started by sandbox on n020,
% 0.17/0.44 % Fri Sep 25 14:21:03 2026
% 0.17/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.17/0.45
% 0.17/0.45 % From the command line: assign(max_seconds, 300).
% 8.72/1.68
% 8.72/1.68 % Assigning unary symbol inverse kb_weight 0 and highest precedence (10).
% 8.72/1.68
% 8.72/1.68 % SZS status Unsatisfiable for theBenchmark
% 8.72/1.68
% 8.72/1.68 % Proof 1 at 0.90 (+ 0.28) seconds.
% 8.72/1.68 % Length of proof is 78.
% 8.72/1.68 % Level of proof is 25.
% 8.72/1.68 % Maximum clause weight is 100.000.
% 8.72/1.68 % Given clauses 58.
% 8.72/1.68
% 8.72/1.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------