%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP428-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 : n018.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:26 AM UTC 2026
% Result : Unsatisfiable 2.98s 0.99s
% Output : CNFRefutation 2.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 2
% Syntax : Number of formulae : 154 ( 154 unt; 0 def)
% Number of atoms : 154 ( 153 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 16 ( 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 : 493 ( 0 sgn 4 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : multiply(VAR_0,inverse(multiply(multiply(inverse(multiply(inverse(VAR_1),multiply(inverse(VAR_0),VAR_2))),VAR_3),inverse(multiply(VAR_1,VAR_3))))) = VAR_2,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(A,inverse(multiply(multiply(inverse(multiply(inverse(B),multiply(inverse(A),C))),D),inverse(multiply(B,D))))) = C,
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,
multiply(A,inverse(multiply(multiply(inverse(multiply(inverse(B),C)),D),inverse(multiply(B,D))))) = inverse(multiply(multiply(inverse(multiply(inverse(E),multiply(inverse(inverse(A)),C))),F),inverse(multiply(E,F)))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_4,plain,
inverse(multiply(multiply(inverse(multiply(inverse(A),multiply(inverse(inverse(B)),multiply(inverse(B),C)))),D),inverse(multiply(A,D)))) = C,
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_5,plain,
multiply(inverse(A),multiply(A,inverse(multiply(multiply(inverse(multiply(inverse(B),C)),D),inverse(multiply(B,D)))))) = C,
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_7,plain,
multiply(A,inverse(multiply(multiply(inverse(B),C),inverse(multiply(inverse(A),C))))) = inverse(multiply(multiply(inverse(multiply(inverse(D),B)),E),inverse(multiply(D,E)))),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_11,plain,
multiply(A,multiply(B,inverse(multiply(multiply(inverse(multiply(inverse(A),C)),D),inverse(multiply(inverse(B),D)))))) = C,
inference(paramod,[status(thm)],[c_7,c_1]) ).
cnf(c_13,plain,
multiply(inverse(A),multiply(A,multiply(B,inverse(multiply(multiply(inverse(C),D),inverse(multiply(inverse(B),D))))))) = C,
inference(paramod,[status(thm)],[c_7,c_5]) ).
cnf(c_929,plain,
multiply(inverse(A),multiply(A,B)) = multiply(inverse(inverse(C)),multiply(inverse(C),B)),
inference(paramod,[status(thm)],[c_1,c_13]) ).
cnf(c_20,plain,
multiply(inverse(inverse(A)),multiply(inverse(A),B)) = multiply(inverse(C),multiply(C,B)),
inference(copy,[status(thm)],[c_929]) ).
cnf(c_930,plain,
inverse(multiply(multiply(inverse(multiply(inverse(A),multiply(inverse(B),multiply(inverse(multiply(multiply(inverse(multiply(inverse(C),multiply(inverse(inverse(D)),multiply(inverse(D),B)))),E),inverse(multiply(C,E)))),F)))),V6),inverse(multiply(A,V6)))) = F,
inference(paramod,[status(thm)],[c_4,c_4]) ).
cnf(c_27,plain,
inverse(multiply(multiply(inverse(multiply(inverse(A),multiply(inverse(B),multiply(B,C)))),D),inverse(multiply(A,D)))) = C,
inference(paramod,[status(thm)],[c_4,c_930]) ).
cnf(c_28,plain,
multiply(A,inverse(multiply(multiply(inverse(multiply(inverse(B),multiply(B,C))),D),inverse(multiply(inverse(A),D))))) = C,
inference(paramod,[status(thm)],[c_20,c_1]) ).
cnf(c_45,plain,
multiply(inverse(A),multiply(A,B)) = multiply(inverse(C),multiply(C,B)),
inference(paramod,[status(thm)],[c_20,c_20]) ).
cnf(c_89,plain,
inverse(multiply(multiply(inverse(A),B),inverse(multiply(inverse(C),B)))) = inverse(multiply(multiply(inverse(A),D),inverse(multiply(inverse(C),D)))),
inference(paramod,[status(thm)],[c_13,c_27]) ).
cnf(c_931,plain,
multiply(inverse(A),multiply(A,multiply(B,inverse(multiply(multiply(inverse(multiply(multiply(inverse(C),D),inverse(multiply(inverse(E),D)))),F),inverse(multiply(inverse(B),F))))))) = multiply(multiply(inverse(C),V6),inverse(multiply(inverse(E),V6))),
inference(paramod,[status(thm)],[c_89,c_13]) ).
cnf(c_104,plain,
multiply(multiply(inverse(A),B),inverse(multiply(inverse(C),B))) = multiply(multiply(inverse(A),D),inverse(multiply(inverse(C),D))),
inference(paramod,[status(thm)],[c_13,c_931]) ).
cnf(c_932,plain,
inverse(multiply(multiply(inverse(A),B),inverse(multiply(C,B)))) = inverse(multiply(multiply(inverse(A),D),inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(E),multiply(inverse(F),multiply(F,C)))),V6),inverse(multiply(E,V6)))),D)))),
inference(paramod,[status(thm)],[c_27,c_89]) ).
cnf(c_111,plain,
inverse(multiply(multiply(inverse(A),B),inverse(multiply(C,B)))) = inverse(multiply(multiply(inverse(A),D),inverse(multiply(C,D)))),
inference(paramod,[status(thm)],[c_27,c_932]) ).
cnf(c_933,plain,
multiply(multiply(inverse(A),B),inverse(multiply(C,B))) = multiply(multiply(inverse(A),D),inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(E),multiply(inverse(F),multiply(F,C)))),V6),inverse(multiply(E,V6)))),D))),
inference(paramod,[status(thm)],[c_27,c_104]) ).
cnf(c_123,plain,
multiply(multiply(inverse(A),B),inverse(multiply(C,B))) = multiply(multiply(inverse(A),D),inverse(multiply(C,D))),
inference(paramod,[status(thm)],[c_27,c_933]) ).
cnf(c_135,plain,
multiply(multiply(inverse(A),multiply(A,B)),inverse(multiply(C,multiply(D,B)))) = multiply(multiply(inverse(D),E),inverse(multiply(C,E))),
inference(paramod,[status(thm)],[c_45,c_123]) ).
cnf(c_934,plain,
multiply(multiply(A,B),inverse(multiply(C,B))) = multiply(multiply(inverse(multiply(multiply(inverse(multiply(inverse(D),multiply(inverse(E),multiply(E,A)))),F),inverse(multiply(D,F)))),V6),inverse(multiply(C,V6))),
inference(paramod,[status(thm)],[c_27,c_123]) ).
cnf(c_145,plain,
multiply(multiply(A,B),inverse(multiply(C,B))) = multiply(multiply(A,D),inverse(multiply(C,D))),
inference(paramod,[status(thm)],[c_27,c_934]) ).
cnf(c_164,plain,
multiply(inverse(multiply(A,B)),multiply(multiply(A,C),inverse(multiply(D,C)))) = multiply(inverse(E),multiply(E,inverse(multiply(D,B)))),
inference(paramod,[status(thm)],[c_145,c_45]) ).
cnf(c_935,plain,
inverse(multiply(multiply(A,B),inverse(multiply(C,B)))) = inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(inverse(D),multiply(inverse(E),multiply(E,A)))),F),inverse(multiply(D,F)))),V6),inverse(multiply(C,V6)))),
inference(paramod,[status(thm)],[c_27,c_111]) ).
cnf(c_187,plain,
inverse(multiply(multiply(A,B),inverse(multiply(C,B)))) = inverse(multiply(multiply(A,D),inverse(multiply(C,D)))),
inference(paramod,[status(thm)],[c_27,c_935]) ).
cnf(c_936,plain,
multiply(multiply(inverse(A),multiply(A,inverse(multiply(multiply(inverse(multiply(inverse(B),C)),D),inverse(multiply(B,D)))))),inverse(C)) = multiply(multiply(inverse(E),F),inverse(multiply(inverse(E),F))),
inference(paramod,[status(thm)],[c_5,c_135]) ).
cnf(c_937,plain,
multiply(C,inverse(C)) = multiply(multiply(inverse(E),F),inverse(multiply(inverse(E),F))),
inference(paramod,[status(thm)],[c_5,c_936]) ).
cnf(c_226,plain,
multiply(multiply(inverse(A),B),inverse(multiply(inverse(A),B))) = multiply(C,inverse(C)),
inference(copy,[status(thm)],[c_937]) ).
cnf(c_938,plain,
multiply(A,inverse(multiply(inverse(B),inverse(multiply(multiply(inverse(multiply(inverse(C),multiply(inverse(inverse(B)),A))),D),inverse(multiply(C,D))))))) = multiply(E,inverse(E)),
inference(paramod,[status(thm)],[c_1,c_226]) ).
cnf(c_251,plain,
multiply(A,inverse(A)) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_1,c_938]) ).
cnf(c_255,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = inverse(multiply(multiply(inverse(multiply(inverse(C),A)),D),inverse(multiply(C,D)))),
inference(paramod,[status(thm)],[c_226,c_7]) ).
cnf(c_267,plain,
multiply(A,multiply(multiply(inverse(A),B),inverse(multiply(C,inverse(C))))) = B,
inference(paramod,[status(thm)],[c_226,c_11]) ).
cnf(c_290,plain,
multiply(multiply(inverse(A),multiply(A,B)),inverse(multiply(C,inverse(C)))) = B,
inference(paramod,[status(thm)],[c_226,c_28]) ).
cnf(c_325,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(multiply(A,C),inverse(multiply(D,C)))),inverse(multiply(inverse(E),multiply(E,inverse(multiply(D,B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_164,c_226]) ).
cnf(c_361,plain,
multiply(inverse(A),multiply(B,inverse(B))) = multiply(inverse(C),multiply(C,inverse(A))),
inference(paramod,[status(thm)],[c_251,c_45]) ).
cnf(c_383,plain,
multiply(multiply(A,inverse(B)),inverse(multiply(C,inverse(C)))) = multiply(multiply(A,D),inverse(multiply(B,D))),
inference(paramod,[status(thm)],[c_251,c_145]) ).
cnf(c_939,plain,
inverse(multiply(A,inverse(A))) = inverse(multiply(multiply(B,C),inverse(multiply(B,C)))),
inference(paramod,[status(thm)],[c_251,c_187]) ).
cnf(c_386,plain,
inverse(multiply(multiply(A,B),inverse(multiply(A,B)))) = inverse(multiply(C,inverse(C))),
inference(copy,[status(thm)],[c_939]) ).
cnf(c_940,plain,
multiply(A,multiply(B,inverse(B))) = multiply(inverse(C),multiply(C,inverse(multiply(multiply(inverse(multiply(inverse(D),multiply(inverse(E),multiply(E,A)))),F),inverse(multiply(D,F)))))),
inference(paramod,[status(thm)],[c_27,c_361]) ).
cnf(c_941,plain,
multiply(A,multiply(B,inverse(B))) = multiply(inverse(C),multiply(C,A)),
inference(paramod,[status(thm)],[c_27,c_940]) ).
cnf(c_456,plain,
multiply(inverse(A),multiply(A,B)) = multiply(B,multiply(C,inverse(C))),
inference(copy,[status(thm)],[c_941]) ).
cnf(c_542,plain,
inverse(multiply(multiply(inverse(multiply(inverse(A),multiply(inverse(B),multiply(B,C)))),multiply(D,inverse(D))),inverse(multiply(inverse(E),multiply(E,A))))) = C,
inference(paramod,[status(thm)],[c_456,c_27]) ).
cnf(c_942,plain,
multiply(inverse(inverse(A)),multiply(B,multiply(C,inverse(C)))) = multiply(multiply(A,B),multiply(D,inverse(D))),
inference(paramod,[status(thm)],[c_456,c_456]) ).
cnf(c_582,plain,
multiply(multiply(A,B),multiply(C,inverse(C))) = multiply(inverse(inverse(A)),multiply(B,multiply(D,inverse(D)))),
inference(copy,[status(thm)],[c_942]) ).
cnf(c_583,plain,
multiply(A,multiply(B,inverse(B))) = multiply(A,multiply(C,inverse(C))),
inference(paramod,[status(thm)],[c_456,c_456]) ).
cnf(c_598,plain,
multiply(A,inverse(multiply(multiply(inverse(multiply(inverse(B),multiply(B,C))),multiply(D,inverse(D))),inverse(multiply(inverse(A),multiply(E,inverse(E))))))) = C,
inference(paramod,[status(thm)],[c_583,c_28]) ).
cnf(c_602,plain,
multiply(multiply(A,multiply(B,inverse(B))),inverse(multiply(C,multiply(D,inverse(D))))) = multiply(multiply(A,E),inverse(multiply(C,E))),
inference(paramod,[status(thm)],[c_583,c_145]) ).
cnf(c_606,plain,
multiply(inverse(multiply(A,B)),multiply(multiply(A,multiply(C,inverse(C))),inverse(multiply(D,multiply(E,inverse(E)))))) = multiply(inverse(F),multiply(F,inverse(multiply(D,B)))),
inference(paramod,[status(thm)],[c_583,c_164]) ).
cnf(c_943,plain,
inverse(multiply(A,inverse(multiply(B,inverse(multiply(multiply(inverse(multiply(inverse(C),multiply(inverse(B),A))),D),inverse(multiply(C,D)))))))) = inverse(multiply(E,inverse(E))),
inference(paramod,[status(thm)],[c_1,c_386]) ).
cnf(c_612,plain,
inverse(multiply(A,inverse(A))) = inverse(multiply(B,inverse(B))),
inference(paramod,[status(thm)],[c_1,c_943]) ).
cnf(c_707,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_612,c_251]) ).
cnf(c_731,plain,
multiply(A,multiply(B,inverse(B))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_707,c_11]) ).
cnf(c_944,plain,
multiply(inverse(A),multiply(A,B)) = multiply(B,multiply(C,inverse(C))),
inference(paramod,[status(thm)],[c_707,c_456]) ).
cnf(c_804,plain,
multiply(inverse(A),multiply(A,B)) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_731,c_944]) ).
cnf(c_945,plain,
multiply(inverse(multiply(A,B)),multiply(inverse(inverse(A)),inverse(multiply(D,multiply(E,inverse(E)))))) = multiply(inverse(F),multiply(F,inverse(multiply(D,B)))),
inference(paramod,[status(thm)],[c_731,c_606]) ).
cnf(c_946,plain,
multiply(inverse(multiply(A,B)),multiply(inverse(inverse(A)),inverse(inverse(inverse(D))))) = multiply(inverse(F),multiply(F,inverse(multiply(D,B)))),
inference(paramod,[status(thm)],[c_731,c_945]) ).
cnf(c_815,plain,
multiply(inverse(multiply(A,B)),multiply(inverse(inverse(A)),inverse(inverse(inverse(C))))) = inverse(inverse(inverse(multiply(C,B)))),
inference(paramod,[status(thm)],[c_804,c_946]) ).
cnf(c_947,plain,
multiply(inverse(inverse(A)),inverse(multiply(C,multiply(D,inverse(D))))) = multiply(multiply(A,E),inverse(multiply(C,E))),
inference(paramod,[status(thm)],[c_731,c_602]) ).
cnf(c_948,plain,
multiply(inverse(inverse(A)),inverse(inverse(inverse(C)))) = multiply(multiply(A,E),inverse(multiply(C,E))),
inference(paramod,[status(thm)],[c_731,c_947]) ).
cnf(c_819,plain,
multiply(multiply(A,B),inverse(multiply(C,B))) = multiply(inverse(inverse(A)),inverse(inverse(inverse(C)))),
inference(copy,[status(thm)],[c_948]) ).
cnf(c_949,plain,
multiply(A,inverse(multiply(multiply(inverse(inverse(inverse(C))),multiply(D,inverse(D))),inverse(multiply(inverse(A),multiply(E,inverse(E))))))) = C,
inference(paramod,[status(thm)],[c_804,c_598]) ).
cnf(c_950,plain,
multiply(A,inverse(multiply(inverse(inverse(inverse(inverse(inverse(C))))),inverse(multiply(inverse(A),multiply(E,inverse(E))))))) = C,
inference(paramod,[status(thm)],[c_731,c_949]) ).
cnf(c_821,plain,
multiply(A,inverse(multiply(inverse(inverse(inverse(inverse(inverse(B))))),inverse(inverse(inverse(inverse(A))))))) = B,
inference(paramod,[status(thm)],[c_731,c_950]) ).
cnf(c_951,plain,
inverse(inverse(multiply(A,B))) = multiply(inverse(inverse(A)),multiply(B,multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_731,c_582]) ).
cnf(c_826,plain,
inverse(inverse(multiply(A,B))) = multiply(inverse(inverse(A)),inverse(inverse(B))),
inference(paramod,[status(thm)],[c_731,c_951]) ).
cnf(c_952,plain,
inverse(multiply(multiply(inverse(multiply(inverse(A),inverse(inverse(C)))),multiply(D,inverse(D))),inverse(multiply(inverse(E),multiply(E,A))))) = C,
inference(paramod,[status(thm)],[c_804,c_542]) ).
cnf(c_953,plain,
inverse(multiply(inverse(inverse(inverse(multiply(inverse(A),inverse(inverse(C)))))),inverse(multiply(inverse(E),multiply(E,A))))) = C,
inference(paramod,[status(thm)],[c_731,c_952]) ).
cnf(c_954,plain,
inverse(multiply(inverse(multiply(inverse(inverse(inverse(A))),inverse(inverse(inverse(inverse(C)))))),inverse(multiply(inverse(E),multiply(E,A))))) = C,
inference(paramod,[status(thm)],[c_826,c_953]) ).
cnf(c_832,plain,
inverse(multiply(inverse(multiply(inverse(inverse(inverse(A))),inverse(inverse(inverse(inverse(B)))))),inverse(inverse(inverse(A))))) = B,
inference(paramod,[status(thm)],[c_804,c_954]) ).
cnf(c_955,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(inverse(inverse(A)),inverse(inverse(inverse(D))))),inverse(multiply(inverse(E),multiply(E,inverse(multiply(D,B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_819,c_325]) ).
cnf(c_956,plain,
multiply(inverse(inverse(inverse(multiply(D,B)))),inverse(multiply(inverse(E),multiply(E,inverse(multiply(D,B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_815,c_955]) ).
cnf(c_957,plain,
multiply(inverse(multiply(inverse(inverse(D)),inverse(inverse(B)))),inverse(multiply(inverse(E),multiply(E,inverse(multiply(D,B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_826,c_956]) ).
cnf(c_958,plain,
multiply(inverse(multiply(inverse(inverse(D)),inverse(inverse(B)))),inverse(inverse(inverse(inverse(multiply(D,B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_804,c_957]) ).
cnf(c_959,plain,
multiply(inverse(multiply(inverse(inverse(D)),inverse(inverse(B)))),inverse(inverse(multiply(inverse(inverse(D)),inverse(inverse(B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_826,c_958]) ).
cnf(c_960,plain,
multiply(inverse(multiply(inverse(inverse(D)),inverse(inverse(B)))),multiply(inverse(inverse(inverse(inverse(D)))),inverse(inverse(inverse(inverse(B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_826,c_959]) ).
cnf(c_961,plain,
inverse(inverse(inverse(multiply(inverse(B),inverse(inverse(B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_815,c_960]) ).
cnf(c_962,plain,
inverse(multiply(inverse(inverse(inverse(B))),inverse(inverse(inverse(inverse(B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_826,c_961]) ).
cnf(c_838,plain,
multiply(A,inverse(A)) = inverse(multiply(inverse(inverse(inverse(B))),inverse(inverse(inverse(inverse(B)))))),
inference(copy,[status(thm)],[c_962]) ).
cnf(c_848,plain,
multiply(inverse(inverse(A)),inverse(multiply(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_804,c_290]) ).
cnf(c_963,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = inverse(multiply(inverse(inverse(inverse(multiply(inverse(C),A)))),inverse(inverse(inverse(C))))),
inference(paramod,[status(thm)],[c_819,c_255]) ).
cnf(c_861,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = inverse(multiply(inverse(multiply(inverse(inverse(inverse(C))),inverse(inverse(A)))),inverse(inverse(inverse(C))))),
inference(paramod,[status(thm)],[c_826,c_963]) ).
cnf(c_868,plain,
multiply(multiply(A,inverse(B)),inverse(multiply(C,inverse(C)))) = multiply(inverse(inverse(A)),inverse(inverse(inverse(B)))),
inference(paramod,[status(thm)],[c_819,c_383]) ).
cnf(c_877,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(inverse(inverse(B)),inverse(inverse(C))))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_826,c_731]) ).
cnf(c_878,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(inverse(B)))),inverse(multiply(C,inverse(C)))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_826,c_848]) ).
cnf(c_964,plain,
multiply(multiply(inverse(inverse(A)),inverse(inverse(B))),inverse(multiply(C,inverse(C)))) = multiply(A,B),
inference(paramod,[status(thm)],[c_826,c_848]) ).
cnf(c_879,plain,
multiply(inverse(inverse(inverse(inverse(A)))),inverse(inverse(inverse(inverse(B))))) = multiply(A,B),
inference(paramod,[status(thm)],[c_868,c_964]) ).
cnf(c_880,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(B)),inverse(inverse(C)))))) = A,
inference(paramod,[status(thm)],[c_826,c_848]) ).
cnf(c_881,plain,
multiply(A,inverse(multiply(inverse(B),A))) = B,
inference(paramod,[status(thm)],[c_879,c_821]) ).
cnf(c_965,plain,
multiply(inverse(A),B) = inverse(inverse(inverse(multiply(inverse(B),A)))),
inference(paramod,[status(thm)],[c_881,c_804]) ).
cnf(c_966,plain,
multiply(inverse(A),B) = inverse(multiply(inverse(inverse(inverse(B))),inverse(inverse(A)))),
inference(paramod,[status(thm)],[c_826,c_965]) ).
cnf(c_886,plain,
inverse(multiply(inverse(inverse(inverse(A))),inverse(inverse(B)))) = multiply(inverse(B),A),
inference(copy,[status(thm)],[c_966]) ).
cnf(c_887,plain,
multiply(multiply(A,B),inverse(inverse(inverse(B)))) = A,
inference(paramod,[status(thm)],[c_804,c_881]) ).
cnf(c_888,plain,
multiply(multiply(A,inverse(A)),inverse(inverse(inverse(inverse(B))))) = B,
inference(paramod,[status(thm)],[c_731,c_881]) ).
cnf(c_891,plain,
multiply(A,multiply(B,inverse(multiply(C,inverse(C))))) = inverse(multiply(inverse(B),inverse(A))),
inference(paramod,[status(thm)],[c_881,c_267]) ).
cnf(c_967,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = inverse(multiply(multiply(inverse(A),C),inverse(inverse(inverse(C))))),
inference(paramod,[status(thm)],[c_886,c_861]) ).
cnf(c_895,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_887,c_967]) ).
cnf(c_968,plain,
multiply(A,inverse(A)) = multiply(inverse(inverse(inverse(B))),B),
inference(paramod,[status(thm)],[c_886,c_838]) ).
cnf(c_897,plain,
multiply(inverse(inverse(inverse(A))),A) = multiply(B,inverse(B)),
inference(copy,[status(thm)],[c_968]) ).
cnf(c_969,plain,
inverse(multiply(multiply(inverse(inverse(inverse(B))),A),inverse(inverse(inverse(A))))) = B,
inference(paramod,[status(thm)],[c_886,c_832]) ).
cnf(c_898,plain,
inverse(inverse(inverse(inverse(A)))) = A,
inference(paramod,[status(thm)],[c_887,c_969]) ).
cnf(c_970,plain,
multiply(A,inverse(inverse(B))) = inverse(multiply(inverse(B),inverse(A))),
inference(paramod,[status(thm)],[c_895,c_891]) ).
cnf(c_901,plain,
inverse(multiply(inverse(A),inverse(B))) = multiply(B,inverse(inverse(A))),
inference(copy,[status(thm)],[c_970]) ).
cnf(c_971,plain,
multiply(multiply(inverse(B),inverse(inverse(inverse(A)))),inverse(multiply(C,inverse(C)))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_901,c_878]) ).
cnf(c_972,plain,
inverse(inverse(multiply(inverse(B),inverse(inverse(inverse(A)))))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_895,c_971]) ).
cnf(c_973,plain,
inverse(multiply(inverse(inverse(A)),inverse(inverse(B)))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_901,c_972]) ).
cnf(c_974,plain,
multiply(inverse(B),inverse(inverse(inverse(A)))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_901,c_973]) ).
cnf(c_902,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(inverse(inverse(A)))),
inference(copy,[status(thm)],[c_974]) ).
cnf(c_904,plain,
multiply(multiply(A,inverse(A)),B) = B,
inference(paramod,[status(thm)],[c_898,c_888]) ).
cnf(c_975,plain,
multiply(inverse(inverse(B)),inverse(inverse(inverse(inverse(A))))) = multiply(B,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_902,c_901]) ).
cnf(c_909,plain,
multiply(inverse(inverse(A)),B) = multiply(A,inverse(inverse(B))),
inference(paramod,[status(thm)],[c_898,c_975]) ).
cnf(c_976,plain,
multiply(inverse(inverse(A)),inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(inverse(inverse(B)),inverse(inverse(C)))))) = A,
inference(paramod,[status(thm)],[c_902,c_880]) ).
cnf(c_977,plain,
multiply(inverse(inverse(A)),inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,inverse(inverse(inverse(inverse(C)))))))) = A,
inference(paramod,[status(thm)],[c_909,c_976]) ).
cnf(c_978,plain,
multiply(inverse(inverse(A)),inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C)))) = A,
inference(paramod,[status(thm)],[c_898,c_977]) ).
cnf(c_979,plain,
multiply(inverse(inverse(A)),multiply(inverse(multiply(B,C)),inverse(inverse(inverse(multiply(inverse(C),inverse(inverse(inverse(B))))))))) = A,
inference(paramod,[status(thm)],[c_902,c_978]) ).
cnf(c_980,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(inverse(multiply(inverse(C),inverse(inverse(inverse(B))))))))) = A,
inference(paramod,[status(thm)],[c_902,c_979]) ).
cnf(c_981,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(inverse(inverse(inverse(inverse(B)))),inverse(inverse(inverse(inverse(C))))))))) = A,
inference(paramod,[status(thm)],[c_902,c_980]) ).
cnf(c_982,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(B,inverse(inverse(inverse(inverse(C))))))))) = A,
inference(paramod,[status(thm)],[c_898,c_981]) ).
cnf(c_983,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(B,C))))) = A,
inference(paramod,[status(thm)],[c_898,c_982]) ).
cnf(c_984,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(multiply(inverse(C),inverse(inverse(inverse(B))))))) = A,
inference(paramod,[status(thm)],[c_902,c_983]) ).
cnf(c_985,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(inverse(inverse(inverse(inverse(B)))),inverse(inverse(inverse(inverse(C))))))) = A,
inference(paramod,[status(thm)],[c_902,c_984]) ).
cnf(c_986,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,inverse(inverse(inverse(inverse(C))))))) = A,
inference(paramod,[status(thm)],[c_898,c_985]) ).
cnf(c_987,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C))) = A,
inference(paramod,[status(thm)],[c_898,c_986]) ).
cnf(c_988,plain,
multiply(A,inverse(inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C))))) = A,
inference(paramod,[status(thm)],[c_909,c_987]) ).
cnf(c_989,plain,
multiply(A,inverse(multiply(inverse(multiply(B,C)),inverse(inverse(inverse(multiply(inverse(C),inverse(inverse(inverse(B)))))))))) = A,
inference(paramod,[status(thm)],[c_902,c_988]) ).
cnf(c_990,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(inverse(multiply(inverse(C),inverse(inverse(inverse(B)))))))))) = A,
inference(paramod,[status(thm)],[c_902,c_989]) ).
cnf(c_991,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(inverse(inverse(inverse(inverse(B)))),inverse(inverse(inverse(inverse(C)))))))))) = A,
inference(paramod,[status(thm)],[c_902,c_990]) ).
cnf(c_992,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(B,inverse(inverse(inverse(inverse(C)))))))))) = A,
inference(paramod,[status(thm)],[c_898,c_991]) ).
cnf(c_993,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(B,C)))))) = A,
inference(paramod,[status(thm)],[c_898,c_992]) ).
cnf(c_994,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(multiply(inverse(C),inverse(inverse(inverse(B)))))))) = A,
inference(paramod,[status(thm)],[c_902,c_993]) ).
cnf(c_995,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(inverse(inverse(inverse(inverse(B)))),inverse(inverse(inverse(inverse(C)))))))) = A,
inference(paramod,[status(thm)],[c_902,c_994]) ).
cnf(c_996,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,inverse(inverse(inverse(inverse(C)))))))) = A,
inference(paramod,[status(thm)],[c_898,c_995]) ).
cnf(c_997,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C)))) = A,
inference(paramod,[status(thm)],[c_898,c_996]) ).
cnf(c_998,plain,
multiply(A,multiply(inverse(multiply(B,C)),inverse(inverse(inverse(multiply(inverse(C),inverse(inverse(inverse(B))))))))) = A,
inference(paramod,[status(thm)],[c_902,c_997]) ).
cnf(c_999,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(inverse(multiply(inverse(C),inverse(inverse(inverse(B))))))))) = A,
inference(paramod,[status(thm)],[c_902,c_998]) ).
cnf(c_1000,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(inverse(inverse(inverse(inverse(B)))),inverse(inverse(inverse(inverse(C))))))))) = A,
inference(paramod,[status(thm)],[c_902,c_999]) ).
cnf(c_1001,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(B,inverse(inverse(inverse(inverse(C))))))))) = A,
inference(paramod,[status(thm)],[c_898,c_1000]) ).
cnf(c_1002,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(B,C))))) = A,
inference(paramod,[status(thm)],[c_898,c_1001]) ).
cnf(c_1003,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(multiply(inverse(C),inverse(inverse(inverse(B))))))) = A,
inference(paramod,[status(thm)],[c_902,c_1002]) ).
cnf(c_1004,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(inverse(inverse(inverse(inverse(B)))),inverse(inverse(inverse(inverse(C))))))) = A,
inference(paramod,[status(thm)],[c_902,c_1003]) ).
cnf(c_1005,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,inverse(inverse(inverse(inverse(C))))))) = A,
inference(paramod,[status(thm)],[c_898,c_1004]) ).
cnf(c_913,plain,
multiply(A,multiply(multiply(inverse(B),inverse(inverse(inverse(C)))),multiply(C,B))) = A,
inference(paramod,[status(thm)],[c_898,c_1005]) ).
cnf(c_1006,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(inverse(inverse(B)),inverse(inverse(C))))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_902,c_877]) ).
cnf(c_1007,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,inverse(inverse(inverse(inverse(C))))))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_909,c_1006]) ).
cnf(c_1008,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_898,c_1007]) ).
cnf(c_1009,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_913,c_1008]) ).
cnf(c_914,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_1009]) ).
cnf(c_922,plain,
multiply(inverse(A),A) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_914,c_897]) ).
cnf(c_1010,plain,
multiply(multiply(A,inverse(A)),a2) != a2,
inference(paramod,[status(thm)],[c_922,c_2]) ).
cnf(c_1011,plain,
a2 != a2,
inference(paramod,[status(thm)],[c_904,c_1010]) ).
cnf(c_928,plain,
$false,
inference(copy,[status(thm)],[c_1011]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP428-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.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 14:56:05 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 2233548 was started by sandbox on n018,
% 0.08/0.36 % Fri Sep 25 14:56:05 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.36
% 0.08/0.36 % From the command line: assign(max_seconds, 300).
% 2.98/0.99
% 2.98/0.99 % Assigning unary symbol inverse kb_weight 0 and highest precedence (5).
% 2.98/0.99
% 2.98/0.99 % SZS status Unsatisfiable for theBenchmark
% 2.98/0.99
% 2.98/0.99 % Proof 1 at 0.34 (+ 0.08) seconds.
% 2.98/0.99 % Length of proof is 69.
% 2.98/0.99 % Level of proof is 27.
% 2.98/0.99 % Maximum clause weight is 99.000.
% 2.98/0.99 % Given clauses 47.
% 2.98/0.99
% 2.98/0.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------