%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP440-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 : n002.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:33 AM UTC 2026
% Result : Unsatisfiable 16.98s 2.66s
% Output : CNFRefutation 16.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 2
% Syntax : Number of formulae : 90 ( 90 unt; 0 def)
% Number of atoms : 90 ( 89 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 18 ( 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 : 428 ( 0 sgn 4 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : inverse(multiply(VAR_0,multiply(VAR_1,multiply(multiply(inverse(VAR_1),VAR_2),inverse(multiply(VAR_3,multiply(VAR_0,VAR_2))))))) = VAR_3,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C))))))) = D,
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_3,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(B,D)))))),multiply(multiply(E,F),inverse(multiply(V6,multiply(A,F))))))) = V6,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_4,plain,
inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),C),inverse(multiply(D,multiply(E,C))))),D)))) = E,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_12,plain,
inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(F,D))))),E)),F)))) = C,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_7347,plain,
inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(C,D),inverse(multiply(E,multiply(F,D))))),E)),F)))) = multiply(V6,multiply(V7,multiply(multiply(inverse(V7),V8),inverse(multiply(C,multiply(V6,V8)))))),
inference(paramod,[status(thm)],[c_3,c_4]) ).
cnf(c_18,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C)))))) = inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(multiply(D,V6),inverse(multiply(V7,multiply(V8,V6))))),V7)),V8)))),
inference(copy,[status(thm)],[c_7347]) ).
cnf(c_19,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),D),inverse(multiply(E,multiply(F,D))))),E))),multiply(multiply(F,multiply(multiply(inverse(A),V6),inverse(multiply(V7,multiply(V8,V6))))),V7)))) = V8,
inference(paramod,[status(thm)],[c_4,c_4]) ).
cnf(c_535,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(inverse(D),multiply(A,C)))))) = D,
inference(paramod,[status(thm)],[c_18,c_12]) ).
cnf(c_671,plain,
inverse(multiply(A,multiply(B,multiply(C,inverse(multiply(D,multiply(A,multiply(E,multiply(multiply(inverse(E),F),inverse(multiply(inverse(C),multiply(inverse(B),F)))))))))))) = D,
inference(paramod,[status(thm)],[c_535,c_1]) ).
cnf(c_7348,plain,
inverse(multiply(inverse(A),multiply(A,multiply(B,inverse(multiply(C,inverse(multiply(D,multiply(E,multiply(multiply(inverse(E),multiply(multiply(inverse(D),multiply(multiply(inverse(B),F),inverse(multiply(V6,multiply(V7,F))))),V6)),V7)))))))))) = C,
inference(paramod,[status(thm)],[c_18,c_671]) ).
cnf(c_1417,plain,
inverse(multiply(inverse(A),multiply(A,multiply(B,inverse(multiply(C,B)))))) = C,
inference(paramod,[status(thm)],[c_12,c_7348]) ).
cnf(c_7349,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(C,inverse(multiply(D,C)))),D))) = inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(multiply(inverse(A),V6),inverse(multiply(V7,multiply(V8,V6))))),V7)),V8)))),
inference(paramod,[status(thm)],[c_1417,c_18]) ).
cnf(c_1543,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(C,inverse(multiply(D,C)))),D))) = A,
inference(paramod,[status(thm)],[c_12,c_7349]) ).
cnf(c_7350,plain,
inverse(multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(C,multiply(A,multiply(D,multiply(multiply(inverse(D),multiply(E,inverse(multiply(F,E)))),F))))))))) = C,
inference(paramod,[status(thm)],[c_1417,c_671]) ).
cnf(c_1577,plain,
inverse(multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(C,A)))))) = C,
inference(paramod,[status(thm)],[c_1543,c_7350]) ).
cnf(c_1581,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(C,inverse(multiply(D,C)))),D)))) = inverse(B),
inference(paramod,[status(thm)],[c_1417,c_1417]) ).
cnf(c_1705,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(multiply(C,D)))),C)))) = D,
inference(paramod,[status(thm)],[c_1577,c_1417]) ).
cnf(c_1709,plain,
inverse(multiply(multiply(A,multiply(inverse(A),inverse(multiply(B,C)))),multiply(D,multiply(inverse(D),B)))) = C,
inference(paramod,[status(thm)],[c_1577,c_1577]) ).
cnf(c_7351,plain,
multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(inverse(C),multiply(A,multiply(D,multiply(multiply(inverse(D),multiply(E,inverse(multiply(F,E)))),F)))))))) = C,
inference(paramod,[status(thm)],[c_1543,c_535]) ).
cnf(c_1780,plain,
multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(inverse(C),A))))) = C,
inference(paramod,[status(thm)],[c_1543,c_7351]) ).
cnf(c_1810,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(C,multiply(D,inverse(multiply(E,D)))),E)),inverse(C)))) = A,
inference(paramod,[status(thm)],[c_1417,c_1543]) ).
cnf(c_1813,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(multiply(D,E)))),D)),E))) = A,
inference(paramod,[status(thm)],[c_1577,c_1543]) ).
cnf(c_1938,plain,
multiply(multiply(A,multiply(B,inverse(multiply(C,B)))),multiply(D,multiply(inverse(D),C))) = A,
inference(paramod,[status(thm)],[c_1417,c_1780]) ).
cnf(c_1941,plain,
multiply(multiply(A,multiply(inverse(A),inverse(multiply(B,inverse(C))))),multiply(D,multiply(inverse(D),B))) = C,
inference(paramod,[status(thm)],[c_1577,c_1780]) ).
cnf(c_2459,plain,
multiply(multiply(A,multiply(B,inverse(multiply(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C))),B)))),D) = A,
inference(paramod,[status(thm)],[c_1780,c_1938]) ).
cnf(c_7352,plain,
inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(F,D))))),E)),F)))) = multiply(inverse(V6),multiply(V6,multiply(multiply(C,multiply(V7,inverse(multiply(V8,V7)))),V8))),
inference(paramod,[status(thm)],[c_1581,c_12]) ).
cnf(c_7353,plain,
C = multiply(inverse(V6),multiply(V6,multiply(multiply(C,multiply(V7,inverse(multiply(V8,V7)))),V8))),
inference(paramod,[status(thm)],[c_12,c_7352]) ).
cnf(c_2495,plain,
multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(C,inverse(multiply(D,C)))),D))) = B,
inference(copy,[status(thm)],[c_7353]) ).
cnf(c_3606,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),D),inverse(multiply(E,multiply(F,D))))),E))),multiply(multiply(F,multiply(multiply(inverse(A),multiply(V6,multiply(multiply(V7,multiply(V8,inverse(multiply(V9,V8)))),V9))),inverse(multiply(V10,V7)))),V10)))) = inverse(V6),
inference(paramod,[status(thm)],[c_2495,c_19]) ).
cnf(c_4219,plain,
multiply(A,multiply(B,multiply(inverse(B),C))) = multiply(A,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(multiply(F,inverse(multiply(C,F)))),E))),D)))),
inference(paramod,[status(thm)],[c_2459,c_1938]) ).
cnf(c_4230,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(C))),multiply(C,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(F),E))),D)))))))) = F,
inference(paramod,[status(thm)],[c_2459,c_1705]) ).
cnf(c_7354,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),D),inverse(multiply(E,multiply(F,D))))),E))),multiply(multiply(F,multiply(multiply(inverse(A),V6),inverse(multiply(V7,V8)))),V7)))) = multiply(V8,multiply(V9,inverse(multiply(multiply(inverse(inverse(V10)),inverse(multiply(inverse(V6),V10))),V9)))),
inference(paramod,[status(thm)],[c_2459,c_19]) ).
cnf(c_4247,plain,
multiply(A,multiply(B,inverse(multiply(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C))),B)))) = inverse(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),V7),inverse(multiply(V8,multiply(V9,V7))))),V8))),multiply(multiply(V9,multiply(multiply(inverse(E),D),inverse(multiply(V10,A)))),V10)))),
inference(copy,[status(thm)],[c_7354]) ).
cnf(c_4257,plain,
multiply(multiply(A,multiply(inverse(A),inverse(B))),multiply(C,multiply(inverse(C),multiply(B,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(inverse(F)),E))),D))))))) = F,
inference(paramod,[status(thm)],[c_2459,c_1941]) ).
cnf(c_7355,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(D))),D)),multiply(E,multiply(multiply(inverse(E),multiply(F,inverse(multiply(V6,F)))),V6))))) = A,
inference(paramod,[status(thm)],[c_1543,c_1813]) ).
cnf(c_4544,plain,
multiply(A,multiply(B,multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(D))),D)))) = A,
inference(paramod,[status(thm)],[c_1543,c_7355]) ).
cnf(c_4727,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(D))),D))),inverse(E))))) = E,
inference(paramod,[status(thm)],[c_4544,c_1417]) ).
cnf(c_4756,plain,
multiply(A,multiply(B,inverse(multiply(multiply(multiply(C,multiply(inverse(C),inverse(D))),D),B)))) = A,
inference(paramod,[status(thm)],[c_4544,c_1938]) ).
cnf(c_4792,plain,
multiply(multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(D))),D))),inverse(E))))),multiply(F,inverse(F))) = E,
inference(paramod,[status(thm)],[c_4544,c_1941]) ).
cnf(c_7356,plain,
inverse(multiply(inverse(A),A)) = multiply(multiply(B,multiply(inverse(B),inverse(C))),C),
inference(paramod,[status(thm)],[c_4756,c_1]) ).
cnf(c_5358,plain,
multiply(multiply(A,multiply(inverse(A),inverse(B))),B) = inverse(multiply(inverse(C),C)),
inference(copy,[status(thm)],[c_7356]) ).
cnf(c_5524,plain,
multiply(multiply(A,multiply(B,inverse(multiply(multiply(C,inverse(multiply(multiply(multiply(D,multiply(inverse(D),inverse(E))),E),C))),B)))),multiply(F,inverse(F))) = A,
inference(paramod,[status(thm)],[c_4756,c_1938]) ).
cnf(c_5528,plain,
multiply(inverse(A),multiply(A,multiply(B,multiply(multiply(C,multiply(inverse(C),inverse(D))),D)))) = B,
inference(paramod,[status(thm)],[c_4756,c_2495]) ).
cnf(c_5529,plain,
multiply(inverse(A),multiply(A,multiply(B,multiply(C,inverse(multiply(multiply(D,inverse(multiply(multiply(multiply(E,multiply(inverse(E),inverse(F))),F),D))),C)))))) = B,
inference(paramod,[status(thm)],[c_4756,c_2495]) ).
cnf(c_7357,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),multiply(multiply(D,multiply(inverse(D),inverse(E))),E)))) = inverse(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(multiply(A,C)),V7),inverse(multiply(V8,multiply(V9,V7))))),V8)),V9)))),
inference(paramod,[status(thm)],[c_5358,c_18]) ).
cnf(c_5733,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),multiply(multiply(D,multiply(inverse(D),inverse(E))),E)))) = multiply(A,C),
inference(paramod,[status(thm)],[c_12,c_7357]) ).
cnf(c_7358,plain,
inverse(inverse(multiply(inverse(A),A))) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_5358,c_1709]) ).
cnf(c_5904,plain,
multiply(inverse(A),A) = inverse(inverse(multiply(inverse(B),B))),
inference(copy,[status(thm)],[c_7358]) ).
cnf(c_7359,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(multiply(inverse(C),C),multiply(D,inverse(multiply(E,D)))),E)),multiply(multiply(F,multiply(inverse(F),inverse(V6))),V6)))) = A,
inference(paramod,[status(thm)],[c_5358,c_1810]) ).
cnf(c_5922,plain,
multiply(A,multiply(multiply(multiply(inverse(B),B),multiply(C,inverse(multiply(D,C)))),D)) = A,
inference(paramod,[status(thm)],[c_5733,c_7359]) ).
cnf(c_5929,plain,
multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(inverse(C),C))))) = A,
inference(paramod,[status(thm)],[c_5358,c_4544]) ).
cnf(c_7360,plain,
multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(multiply(multiply(inverse(C),C),multiply(D,inverse(multiply(E,D)))),E))) = A,
inference(paramod,[status(thm)],[c_5904,c_1543]) ).
cnf(c_6189,plain,
multiply(A,inverse(multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_5922,c_7360]) ).
cnf(c_6222,plain,
multiply(inverse(A),multiply(A,multiply(inverse(inverse(multiply(inverse(B),B))),C))) = inverse(multiply(D,inverse(multiply(C,D)))),
inference(paramod,[status(thm)],[c_5904,c_2495]) ).
cnf(c_6350,plain,
multiply(A,multiply(B,inverse(B))) = A,
inference(paramod,[status(thm)],[c_6189,c_5929]) ).
cnf(c_6403,plain,
multiply(A,multiply(B,inverse(multiply(multiply(C,inverse(multiply(multiply(multiply(D,multiply(inverse(D),inverse(E))),E),C))),B)))) = A,
inference(paramod,[status(thm)],[c_6350,c_5524]) ).
cnf(c_6404,plain,
multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(D))),D))),inverse(E))))) = E,
inference(paramod,[status(thm)],[c_6350,c_4792]) ).
cnf(c_6417,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(paramod,[status(thm)],[c_6403,c_5529]) ).
cnf(c_6423,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),B) = inverse(multiply(C,inverse(multiply(B,C)))),
inference(paramod,[status(thm)],[c_6417,c_6222]) ).
cnf(c_6443,plain,
multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(C))),C)) = A,
inference(paramod,[status(thm)],[c_6417,c_5528]) ).
cnf(c_7361,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,inverse(B)),inverse(E))))) = E,
inference(paramod,[status(thm)],[c_6443,c_4727]) ).
cnf(c_6477,plain,
inverse(multiply(multiply(A,inverse(A)),inverse(B))) = B,
inference(paramod,[status(thm)],[c_6417,c_7361]) ).
cnf(c_6494,plain,
inverse(multiply(multiply(A,multiply(inverse(A),inverse(B))),multiply(B,multiply(C,inverse(multiply(multiply(inverse(inverse(D)),inverse(multiply(inverse(E),D))),C)))))) = E,
inference(paramod,[status(thm)],[c_6417,c_4230]) ).
cnf(c_6684,plain,
multiply(multiply(A,multiply(B,inverse(multiply(C,B)))),C) = A,
inference(paramod,[status(thm)],[c_6417,c_2495]) ).
cnf(c_6765,plain,
inverse(multiply(A,inverse(multiply(B,A)))) = B,
inference(paramod,[status(thm)],[c_6417,c_1417]) ).
cnf(c_7362,plain,
multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(B)),inverse(E))))) = E,
inference(paramod,[status(thm)],[c_6443,c_6404]) ).
cnf(c_6769,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_6477,c_7362]) ).
cnf(c_7363,plain,
multiply(A,C) = multiply(A,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(multiply(F,inverse(multiply(C,F)))),E))),D)))),
inference(paramod,[status(thm)],[c_6769,c_4219]) ).
cnf(c_7364,plain,
multiply(A,C) = multiply(A,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(C,E))),D)))),
inference(paramod,[status(thm)],[c_6765,c_7363]) ).
cnf(c_6946,plain,
multiply(A,multiply(B,inverse(multiply(multiply(inverse(inverse(C)),inverse(multiply(D,C))),B)))) = multiply(A,D),
inference(copy,[status(thm)],[c_7364]) ).
cnf(c_7365,plain,
inverse(multiply(inverse(B),multiply(B,multiply(C,inverse(multiply(multiply(inverse(inverse(D)),inverse(multiply(inverse(E),D))),C)))))) = E,
inference(paramod,[status(thm)],[c_6769,c_6494]) ).
cnf(c_7366,plain,
inverse(multiply(inverse(B),multiply(B,inverse(E)))) = E,
inference(paramod,[status(thm)],[c_6946,c_7365]) ).
cnf(c_6951,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_6417,c_7366]) ).
cnf(c_7367,plain,
multiply(inverse(B),multiply(C,multiply(inverse(C),multiply(B,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(inverse(F)),E))),D))))))) = F,
inference(paramod,[status(thm)],[c_6769,c_4257]) ).
cnf(c_7368,plain,
multiply(inverse(B),multiply(C,multiply(inverse(C),multiply(B,multiply(D,inverse(multiply(multiply(E,inverse(multiply(inverse(inverse(F)),E))),D))))))) = F,
inference(paramod,[status(thm)],[c_6951,c_7367]) ).
cnf(c_7369,plain,
multiply(inverse(B),multiply(C,multiply(inverse(C),multiply(B,multiply(D,inverse(multiply(multiply(E,inverse(multiply(F,E))),D))))))) = F,
inference(paramod,[status(thm)],[c_6951,c_7368]) ).
cnf(c_7370,plain,
multiply(inverse(B),multiply(B,multiply(D,inverse(multiply(multiply(E,inverse(multiply(F,E))),D))))) = F,
inference(paramod,[status(thm)],[c_6769,c_7369]) ).
cnf(c_6965,plain,
multiply(A,inverse(multiply(multiply(B,inverse(multiply(C,B))),A))) = C,
inference(paramod,[status(thm)],[c_6417,c_7370]) ).
cnf(c_7371,plain,
multiply(A,multiply(B,inverse(multiply(multiply(C,inverse(multiply(inverse(D),C))),B)))) = inverse(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),V7),inverse(multiply(V8,multiply(V9,V7))))),V8))),multiply(multiply(V9,multiply(multiply(inverse(E),D),inverse(multiply(V10,A)))),V10)))),
inference(paramod,[status(thm)],[c_6951,c_4247]) ).
cnf(c_7372,plain,
multiply(A,inverse(D)) = inverse(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),V7),inverse(multiply(V8,multiply(V9,V7))))),V8))),multiply(multiply(V9,multiply(multiply(inverse(E),D),inverse(multiply(V10,A)))),V10)))),
inference(paramod,[status(thm)],[c_6965,c_7371]) ).
cnf(c_6968,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),D),inverse(multiply(E,multiply(F,D))))),E))),multiply(multiply(F,multiply(multiply(inverse(A),V6),inverse(multiply(V7,V8)))),V7)))) = multiply(V8,inverse(V6)),
inference(copy,[status(thm)],[c_7372]) ).
cnf(c_7373,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),D),inverse(multiply(E,multiply(F,D))))),E))),multiply(multiply(F,multiply(multiply(inverse(A),multiply(V6,V7)),inverse(multiply(V10,V7)))),V10)))) = inverse(V6),
inference(paramod,[status(thm)],[c_6684,c_3606]) ).
cnf(c_7279,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(paramod,[status(thm)],[c_6968,c_7373]) ).
cnf(c_7374,plain,
multiply(multiply(inverse(A),A),B) = inverse(multiply(C,inverse(multiply(B,C)))),
inference(paramod,[status(thm)],[c_6951,c_6423]) ).
cnf(c_7375,plain,
multiply(multiply(inverse(A),A),B) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_7279,c_7374]) ).
cnf(c_7345,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_6951,c_7375]) ).
cnf(c_7346,plain,
$false,
inference(resolve,[status(thm)],[c_7345,c_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP440-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n002.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Fri Sep 25 14:57:04 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.42 % Process 3570681 was started by sandbox on n002,
% 0.15/0.42 % Fri Sep 25 14:57:04 2026
% 0.15/0.42 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/0.43
% 0.15/0.43 % From the command line: assign(max_seconds, 300).
% 16.98/2.66
% 16.98/2.66 % Assigning unary symbol inverse kb_weight 0 and highest precedence (5).
% 16.98/2.66
% 16.98/2.66 % SZS status Unsatisfiable for theBenchmark
% 16.98/2.66
% 16.98/2.66 % Proof 1 at 1.88 (+ 0.24) seconds.
% 16.98/2.66 % Length of proof is 59.
% 16.98/2.66 % Level of proof is 27.
% 16.98/2.66 % Maximum clause weight is 54.000.
% 16.98/2.66 % Given clauses 47.
% 16.98/2.66
% 16.98/2.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------