%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP427-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 1.41s 0.54s
% Output : CNFRefutation 1.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 2
% Syntax : Number of formulae : 153 ( 153 unt; 0 def)
% Number of atoms : 153 ( 152 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 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 : 490 ( 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_1,axiom,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file('theBenchmark.p',prove_these_axioms_1) ).
cnf(c_2,plain,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
inference(clausify,[status(thm)],[prove_these_axioms_1]) ).
cnf(c_3,plain,
multiply(inverse(b1),b1) != multiply(inverse(a1),a1),
inference(copy,[status(thm)],[c_2]) ).
cnf(c_4,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_5,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_4,c_1]) ).
cnf(c_6,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_4,c_1]) ).
cnf(c_8,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_6,c_1]) ).
cnf(c_12,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_8,c_1]) ).
cnf(c_14,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_8,c_6]) ).
cnf(c_930,plain,
multiply(inverse(A),multiply(A,B)) = multiply(inverse(inverse(C)),multiply(inverse(C),B)),
inference(paramod,[status(thm)],[c_1,c_14]) ).
cnf(c_21,plain,
multiply(inverse(inverse(A)),multiply(inverse(A),B)) = multiply(inverse(C),multiply(C,B)),
inference(copy,[status(thm)],[c_930]) ).
cnf(c_931,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_5,c_5]) ).
cnf(c_28,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_5,c_931]) ).
cnf(c_29,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_21,c_1]) ).
cnf(c_46,plain,
multiply(inverse(A),multiply(A,B)) = multiply(inverse(C),multiply(C,B)),
inference(paramod,[status(thm)],[c_21,c_21]) ).
cnf(c_90,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_14,c_28]) ).
cnf(c_932,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_90,c_14]) ).
cnf(c_105,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_14,c_932]) ).
cnf(c_933,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_28,c_90]) ).
cnf(c_112,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_28,c_933]) ).
cnf(c_934,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_28,c_105]) ).
cnf(c_124,plain,
multiply(multiply(inverse(A),B),inverse(multiply(C,B))) = multiply(multiply(inverse(A),D),inverse(multiply(C,D))),
inference(paramod,[status(thm)],[c_28,c_934]) ).
cnf(c_136,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_46,c_124]) ).
cnf(c_935,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_28,c_124]) ).
cnf(c_146,plain,
multiply(multiply(A,B),inverse(multiply(C,B))) = multiply(multiply(A,D),inverse(multiply(C,D))),
inference(paramod,[status(thm)],[c_28,c_935]) ).
cnf(c_165,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_146,c_46]) ).
cnf(c_936,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_28,c_112]) ).
cnf(c_188,plain,
inverse(multiply(multiply(A,B),inverse(multiply(C,B)))) = inverse(multiply(multiply(A,D),inverse(multiply(C,D)))),
inference(paramod,[status(thm)],[c_28,c_936]) ).
cnf(c_937,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_6,c_136]) ).
cnf(c_938,plain,
multiply(C,inverse(C)) = multiply(multiply(inverse(E),F),inverse(multiply(inverse(E),F))),
inference(paramod,[status(thm)],[c_6,c_937]) ).
cnf(c_227,plain,
multiply(multiply(inverse(A),B),inverse(multiply(inverse(A),B))) = multiply(C,inverse(C)),
inference(copy,[status(thm)],[c_938]) ).
cnf(c_939,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_227]) ).
cnf(c_252,plain,
multiply(A,inverse(A)) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_1,c_939]) ).
cnf(c_256,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_227,c_8]) ).
cnf(c_268,plain,
multiply(A,multiply(multiply(inverse(A),B),inverse(multiply(C,inverse(C))))) = B,
inference(paramod,[status(thm)],[c_227,c_12]) ).
cnf(c_291,plain,
multiply(multiply(inverse(A),multiply(A,B)),inverse(multiply(C,inverse(C)))) = B,
inference(paramod,[status(thm)],[c_227,c_29]) ).
cnf(c_326,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_165,c_227]) ).
cnf(c_362,plain,
multiply(inverse(A),multiply(B,inverse(B))) = multiply(inverse(C),multiply(C,inverse(A))),
inference(paramod,[status(thm)],[c_252,c_46]) ).
cnf(c_384,plain,
multiply(multiply(A,inverse(B)),inverse(multiply(C,inverse(C)))) = multiply(multiply(A,D),inverse(multiply(B,D))),
inference(paramod,[status(thm)],[c_252,c_146]) ).
cnf(c_940,plain,
inverse(multiply(A,inverse(A))) = inverse(multiply(multiply(B,C),inverse(multiply(B,C)))),
inference(paramod,[status(thm)],[c_252,c_188]) ).
cnf(c_387,plain,
inverse(multiply(multiply(A,B),inverse(multiply(A,B)))) = inverse(multiply(C,inverse(C))),
inference(copy,[status(thm)],[c_940]) ).
cnf(c_941,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_28,c_362]) ).
cnf(c_942,plain,
multiply(A,multiply(B,inverse(B))) = multiply(inverse(C),multiply(C,A)),
inference(paramod,[status(thm)],[c_28,c_941]) ).
cnf(c_457,plain,
multiply(inverse(A),multiply(A,B)) = multiply(B,multiply(C,inverse(C))),
inference(copy,[status(thm)],[c_942]) ).
cnf(c_543,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_457,c_28]) ).
cnf(c_943,plain,
multiply(inverse(inverse(A)),multiply(B,multiply(C,inverse(C)))) = multiply(multiply(A,B),multiply(D,inverse(D))),
inference(paramod,[status(thm)],[c_457,c_457]) ).
cnf(c_583,plain,
multiply(multiply(A,B),multiply(C,inverse(C))) = multiply(inverse(inverse(A)),multiply(B,multiply(D,inverse(D)))),
inference(copy,[status(thm)],[c_943]) ).
cnf(c_584,plain,
multiply(A,multiply(B,inverse(B))) = multiply(A,multiply(C,inverse(C))),
inference(paramod,[status(thm)],[c_457,c_457]) ).
cnf(c_599,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_584,c_29]) ).
cnf(c_603,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_584,c_146]) ).
cnf(c_607,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_584,c_165]) ).
cnf(c_944,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_387]) ).
cnf(c_613,plain,
inverse(multiply(A,inverse(A))) = inverse(multiply(B,inverse(B))),
inference(paramod,[status(thm)],[c_1,c_944]) ).
cnf(c_708,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_613,c_252]) ).
cnf(c_732,plain,
multiply(A,multiply(B,inverse(B))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_708,c_12]) ).
cnf(c_945,plain,
multiply(inverse(A),multiply(A,B)) = multiply(B,multiply(C,inverse(C))),
inference(paramod,[status(thm)],[c_708,c_457]) ).
cnf(c_805,plain,
multiply(inverse(A),multiply(A,B)) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_732,c_945]) ).
cnf(c_946,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_732,c_607]) ).
cnf(c_947,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_732,c_946]) ).
cnf(c_816,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_805,c_947]) ).
cnf(c_948,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_732,c_603]) ).
cnf(c_949,plain,
multiply(inverse(inverse(A)),inverse(inverse(inverse(C)))) = multiply(multiply(A,E),inverse(multiply(C,E))),
inference(paramod,[status(thm)],[c_732,c_948]) ).
cnf(c_820,plain,
multiply(multiply(A,B),inverse(multiply(C,B))) = multiply(inverse(inverse(A)),inverse(inverse(inverse(C)))),
inference(copy,[status(thm)],[c_949]) ).
cnf(c_950,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_805,c_599]) ).
cnf(c_951,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_732,c_950]) ).
cnf(c_822,plain,
multiply(A,inverse(multiply(inverse(inverse(inverse(inverse(inverse(B))))),inverse(inverse(inverse(inverse(A))))))) = B,
inference(paramod,[status(thm)],[c_732,c_951]) ).
cnf(c_952,plain,
inverse(inverse(multiply(A,B))) = multiply(inverse(inverse(A)),multiply(B,multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_732,c_583]) ).
cnf(c_827,plain,
inverse(inverse(multiply(A,B))) = multiply(inverse(inverse(A)),inverse(inverse(B))),
inference(paramod,[status(thm)],[c_732,c_952]) ).
cnf(c_953,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_805,c_543]) ).
cnf(c_954,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_732,c_953]) ).
cnf(c_955,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_827,c_954]) ).
cnf(c_833,plain,
inverse(multiply(inverse(multiply(inverse(inverse(inverse(A))),inverse(inverse(inverse(inverse(B)))))),inverse(inverse(inverse(A))))) = B,
inference(paramod,[status(thm)],[c_805,c_955]) ).
cnf(c_956,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_820,c_326]) ).
cnf(c_957,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_816,c_956]) ).
cnf(c_958,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_827,c_957]) ).
cnf(c_959,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_805,c_958]) ).
cnf(c_960,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_827,c_959]) ).
cnf(c_961,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_827,c_960]) ).
cnf(c_962,plain,
inverse(inverse(inverse(multiply(inverse(B),inverse(inverse(B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_816,c_961]) ).
cnf(c_963,plain,
inverse(multiply(inverse(inverse(inverse(B))),inverse(inverse(inverse(inverse(B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_827,c_962]) ).
cnf(c_839,plain,
multiply(A,inverse(A)) = inverse(multiply(inverse(inverse(inverse(B))),inverse(inverse(inverse(inverse(B)))))),
inference(copy,[status(thm)],[c_963]) ).
cnf(c_849,plain,
multiply(inverse(inverse(A)),inverse(multiply(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_805,c_291]) ).
cnf(c_964,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_820,c_256]) ).
cnf(c_862,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_827,c_964]) ).
cnf(c_869,plain,
multiply(multiply(A,inverse(B)),inverse(multiply(C,inverse(C)))) = multiply(inverse(inverse(A)),inverse(inverse(inverse(B)))),
inference(paramod,[status(thm)],[c_820,c_384]) ).
cnf(c_878,plain,
multiply(A,multiply(inverse(multiply(B,C)),multiply(inverse(inverse(B)),inverse(inverse(C))))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_827,c_732]) ).
cnf(c_879,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(inverse(B)))),inverse(multiply(C,inverse(C)))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_827,c_849]) ).
cnf(c_965,plain,
multiply(multiply(inverse(inverse(A)),inverse(inverse(B))),inverse(multiply(C,inverse(C)))) = multiply(A,B),
inference(paramod,[status(thm)],[c_827,c_849]) ).
cnf(c_880,plain,
multiply(inverse(inverse(inverse(inverse(A)))),inverse(inverse(inverse(inverse(B))))) = multiply(A,B),
inference(paramod,[status(thm)],[c_869,c_965]) ).
cnf(c_881,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(multiply(B,C)),multiply(inverse(inverse(B)),inverse(inverse(C)))))) = A,
inference(paramod,[status(thm)],[c_827,c_849]) ).
cnf(c_882,plain,
multiply(A,inverse(multiply(inverse(B),A))) = B,
inference(paramod,[status(thm)],[c_880,c_822]) ).
cnf(c_966,plain,
multiply(inverse(A),B) = inverse(inverse(inverse(multiply(inverse(B),A)))),
inference(paramod,[status(thm)],[c_882,c_805]) ).
cnf(c_967,plain,
multiply(inverse(A),B) = inverse(multiply(inverse(inverse(inverse(B))),inverse(inverse(A)))),
inference(paramod,[status(thm)],[c_827,c_966]) ).
cnf(c_887,plain,
inverse(multiply(inverse(inverse(inverse(A))),inverse(inverse(B)))) = multiply(inverse(B),A),
inference(copy,[status(thm)],[c_967]) ).
cnf(c_888,plain,
multiply(multiply(A,B),inverse(inverse(inverse(B)))) = A,
inference(paramod,[status(thm)],[c_805,c_882]) ).
cnf(c_892,plain,
multiply(A,multiply(B,inverse(multiply(C,inverse(C))))) = inverse(multiply(inverse(B),inverse(A))),
inference(paramod,[status(thm)],[c_882,c_268]) ).
cnf(c_968,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = inverse(multiply(multiply(inverse(A),C),inverse(inverse(inverse(C))))),
inference(paramod,[status(thm)],[c_887,c_862]) ).
cnf(c_896,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_888,c_968]) ).
cnf(c_969,plain,
multiply(A,inverse(A)) = multiply(inverse(inverse(inverse(B))),B),
inference(paramod,[status(thm)],[c_887,c_839]) ).
cnf(c_898,plain,
multiply(inverse(inverse(inverse(A))),A) = multiply(B,inverse(B)),
inference(copy,[status(thm)],[c_969]) ).
cnf(c_970,plain,
inverse(multiply(multiply(inverse(inverse(inverse(B))),A),inverse(inverse(inverse(A))))) = B,
inference(paramod,[status(thm)],[c_887,c_833]) ).
cnf(c_899,plain,
inverse(inverse(inverse(inverse(A)))) = A,
inference(paramod,[status(thm)],[c_888,c_970]) ).
cnf(c_971,plain,
multiply(A,inverse(inverse(B))) = inverse(multiply(inverse(B),inverse(A))),
inference(paramod,[status(thm)],[c_896,c_892]) ).
cnf(c_902,plain,
inverse(multiply(inverse(A),inverse(B))) = multiply(B,inverse(inverse(A))),
inference(copy,[status(thm)],[c_971]) ).
cnf(c_972,plain,
multiply(multiply(inverse(B),inverse(inverse(inverse(A)))),inverse(multiply(C,inverse(C)))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_902,c_879]) ).
cnf(c_973,plain,
inverse(inverse(multiply(inverse(B),inverse(inverse(inverse(A)))))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_896,c_972]) ).
cnf(c_974,plain,
inverse(multiply(inverse(inverse(A)),inverse(inverse(B)))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_902,c_973]) ).
cnf(c_975,plain,
multiply(inverse(B),inverse(inverse(inverse(A)))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_902,c_974]) ).
cnf(c_903,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(inverse(inverse(A)))),
inference(copy,[status(thm)],[c_975]) ).
cnf(c_976,plain,
multiply(inverse(inverse(B)),inverse(inverse(inverse(inverse(A))))) = multiply(B,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_903,c_902]) ).
cnf(c_910,plain,
multiply(inverse(inverse(A)),B) = multiply(A,inverse(inverse(B))),
inference(paramod,[status(thm)],[c_899,c_976]) ).
cnf(c_977,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_903,c_881]) ).
cnf(c_978,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_910,c_977]) ).
cnf(c_979,plain,
multiply(inverse(inverse(A)),inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C)))) = A,
inference(paramod,[status(thm)],[c_899,c_978]) ).
cnf(c_980,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_903,c_979]) ).
cnf(c_981,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_903,c_980]) ).
cnf(c_982,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_903,c_981]) ).
cnf(c_983,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_899,c_982]) ).
cnf(c_984,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(B,C))))) = A,
inference(paramod,[status(thm)],[c_899,c_983]) ).
cnf(c_985,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_903,c_984]) ).
cnf(c_986,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_903,c_985]) ).
cnf(c_987,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_899,c_986]) ).
cnf(c_988,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C))) = A,
inference(paramod,[status(thm)],[c_899,c_987]) ).
cnf(c_989,plain,
multiply(A,inverse(inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C))))) = A,
inference(paramod,[status(thm)],[c_910,c_988]) ).
cnf(c_990,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_903,c_989]) ).
cnf(c_991,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_903,c_990]) ).
cnf(c_992,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_903,c_991]) ).
cnf(c_993,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_899,c_992]) ).
cnf(c_994,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(B,C)))))) = A,
inference(paramod,[status(thm)],[c_899,c_993]) ).
cnf(c_995,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_903,c_994]) ).
cnf(c_996,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_903,c_995]) ).
cnf(c_997,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_899,c_996]) ).
cnf(c_998,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C)))) = A,
inference(paramod,[status(thm)],[c_899,c_997]) ).
cnf(c_999,plain,
multiply(A,multiply(inverse(multiply(B,C)),inverse(inverse(inverse(multiply(inverse(C),inverse(inverse(inverse(B))))))))) = A,
inference(paramod,[status(thm)],[c_903,c_998]) ).
cnf(c_1000,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_903,c_999]) ).
cnf(c_1001,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_903,c_1000]) ).
cnf(c_1002,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_899,c_1001]) ).
cnf(c_1003,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(B,C))))) = A,
inference(paramod,[status(thm)],[c_899,c_1002]) ).
cnf(c_1004,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_903,c_1003]) ).
cnf(c_1005,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_903,c_1004]) ).
cnf(c_1006,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,inverse(inverse(inverse(inverse(C))))))) = A,
inference(paramod,[status(thm)],[c_899,c_1005]) ).
cnf(c_914,plain,
multiply(A,multiply(multiply(inverse(B),inverse(inverse(inverse(C)))),multiply(C,B))) = A,
inference(paramod,[status(thm)],[c_899,c_1006]) ).
cnf(c_1007,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_903,c_878]) ).
cnf(c_1008,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_910,c_1007]) ).
cnf(c_1009,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_899,c_1008]) ).
cnf(c_1010,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_914,c_1009]) ).
cnf(c_915,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_1010]) ).
cnf(c_923,plain,
multiply(inverse(A),A) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_915,c_898]) ).
cnf(c_1011,plain,
multiply(A,inverse(A)) != multiply(inverse(a1),a1),
inference(paramod,[status(thm)],[c_923,c_3]) ).
cnf(c_1012,plain,
multiply(inverse(a1),a1) != multiply(A,inverse(A)),
inference(copy,[status(thm)],[c_1011]) ).
cnf(c_929,plain,
$false,
inference(resolve,[status(thm)],[c_923,c_1012]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP427-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Fri Sep 25 14:53:35 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.02/0.29 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/0.29 % Process 2364830 was started by sandbox2 on n012,
% 0.02/0.29 % Fri Sep 25 14:53:35 2026
% 0.02/0.29 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.02/0.30
% 0.02/0.30 % From the command line: assign(max_seconds, 300).
% 1.41/0.54
% 1.41/0.54 % Assigning unary symbol inverse kb_weight 0 and highest precedence (5).
% 1.41/0.54
% 1.41/0.54 % SZS status Unsatisfiable for theBenchmark
% 1.41/0.54
% 1.41/0.54 % Proof 1 at 0.17 (+ 0.05) seconds.
% 1.41/0.54 % Length of proof is 68.
% 1.41/0.54 % Level of proof is 27.
% 1.41/0.54 % Maximum clause weight is 99.000.
% 1.41/0.54 % Given clauses 47.
% 1.41/0.54
% 1.41/0.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------