%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP057-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:53 AM UTC 2026
% Result : Unsatisfiable 3.02s 0.94s
% Output : CNFRefutation 3.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 80
% Number of leaves : 2
% Syntax : Number of formulae : 170 ( 164 unt; 0 def)
% Number of atoms : 181 ( 180 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 29 ( 18 ~; 11 |; 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 : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 530 ( 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,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_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_949,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_949]) ).
cnf(c_950,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_950]) ).
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_951,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_951]) ).
cnf(c_952,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_952]) ).
cnf(c_953,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_953]) ).
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_954,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_954]) ).
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_955,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_955]) ).
cnf(c_956,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_957,plain,
multiply(C,inverse(C)) = multiply(multiply(inverse(E),F),inverse(multiply(inverse(E),F))),
inference(paramod,[status(thm)],[c_6,c_956]) ).
cnf(c_227,plain,
multiply(multiply(inverse(A),B),inverse(multiply(inverse(A),B))) = multiply(C,inverse(C)),
inference(copy,[status(thm)],[c_957]) ).
cnf(c_958,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_958]) ).
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_959,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_959]) ).
cnf(c_960,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_961,plain,
multiply(A,multiply(B,inverse(B))) = multiply(inverse(C),multiply(C,A)),
inference(paramod,[status(thm)],[c_28,c_960]) ).
cnf(c_457,plain,
multiply(inverse(A),multiply(A,B)) = multiply(B,multiply(C,inverse(C))),
inference(copy,[status(thm)],[c_961]) ).
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_550,plain,
multiply(multiply(A,multiply(B,C)),inverse(multiply(C,multiply(D,inverse(D))))) = multiply(multiply(A,E),inverse(multiply(inverse(B),E))),
inference(paramod,[status(thm)],[c_457,c_146]) ).
cnf(c_962,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_962]) ).
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_963,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_963]) ).
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_964,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_964]) ).
cnf(c_965,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_966,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_965]) ).
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_966]) ).
cnf(c_967,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_968,plain,
multiply(inverse(inverse(A)),inverse(inverse(inverse(C)))) = multiply(multiply(A,E),inverse(multiply(C,E))),
inference(paramod,[status(thm)],[c_732,c_967]) ).
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_968]) ).
cnf(c_969,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_970,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_969]) ).
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_970]) ).
cnf(c_971,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_971]) ).
cnf(c_972,plain,
multiply(multiply(A,multiply(B,C)),inverse(inverse(inverse(C)))) = multiply(multiply(A,E),inverse(multiply(inverse(B),E))),
inference(paramod,[status(thm)],[c_732,c_550]) ).
cnf(c_832,plain,
multiply(multiply(A,multiply(B,C)),inverse(inverse(inverse(C)))) = multiply(inverse(inverse(A)),inverse(inverse(inverse(inverse(B))))),
inference(paramod,[status(thm)],[c_820,c_972]) ).
cnf(c_973,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_974,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_973]) ).
cnf(c_975,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_974]) ).
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_975]) ).
cnf(c_976,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_977,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_976]) ).
cnf(c_978,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_977]) ).
cnf(c_979,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_978]) ).
cnf(c_980,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_979]) ).
cnf(c_981,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_980]) ).
cnf(c_982,plain,
inverse(inverse(inverse(multiply(inverse(B),inverse(inverse(B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_816,c_981]) ).
cnf(c_983,plain,
inverse(multiply(inverse(inverse(inverse(B))),inverse(inverse(inverse(inverse(B)))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_827,c_982]) ).
cnf(c_839,plain,
multiply(A,inverse(A)) = inverse(multiply(inverse(inverse(inverse(B))),inverse(inverse(inverse(inverse(B)))))),
inference(copy,[status(thm)],[c_983]) ).
cnf(c_849,plain,
multiply(inverse(inverse(A)),inverse(multiply(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_805,c_291]) ).
cnf(c_984,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_984]) ).
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_985,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_985]) ).
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_986,plain,
multiply(inverse(A),B) = inverse(inverse(inverse(multiply(inverse(B),A)))),
inference(paramod,[status(thm)],[c_882,c_805]) ).
cnf(c_987,plain,
multiply(inverse(A),B) = inverse(multiply(inverse(inverse(inverse(B))),inverse(inverse(A)))),
inference(paramod,[status(thm)],[c_827,c_986]) ).
cnf(c_887,plain,
inverse(multiply(inverse(inverse(inverse(A))),inverse(inverse(B)))) = multiply(inverse(B),A),
inference(copy,[status(thm)],[c_987]) ).
cnf(c_888,plain,
multiply(multiply(A,B),inverse(inverse(inverse(B)))) = A,
inference(paramod,[status(thm)],[c_805,c_882]) ).
cnf(c_889,plain,
multiply(multiply(A,inverse(A)),inverse(inverse(inverse(inverse(B))))) = B,
inference(paramod,[status(thm)],[c_732,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_894,plain,
multiply(inverse(multiply(inverse(A),inverse(B))),inverse(A)) = B,
inference(paramod,[status(thm)],[c_882,c_882]) ).
cnf(c_988,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_988]) ).
cnf(c_989,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_989]) ).
cnf(c_990,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_990]) ).
cnf(c_991,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_991]) ).
cnf(c_992,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_993,plain,
inverse(inverse(multiply(inverse(B),inverse(inverse(inverse(A)))))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_896,c_992]) ).
cnf(c_994,plain,
inverse(multiply(inverse(inverse(A)),inverse(inverse(B)))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_902,c_993]) ).
cnf(c_995,plain,
multiply(inverse(B),inverse(inverse(inverse(A)))) = inverse(multiply(A,B)),
inference(paramod,[status(thm)],[c_902,c_994]) ).
cnf(c_903,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(inverse(inverse(A)))),
inference(copy,[status(thm)],[c_995]) ).
cnf(c_905,plain,
multiply(multiply(A,inverse(A)),B) = B,
inference(paramod,[status(thm)],[c_899,c_889]) ).
cnf(c_906,plain,
multiply(multiply(A,multiply(B,C)),inverse(inverse(inverse(C)))) = multiply(inverse(inverse(A)),B),
inference(paramod,[status(thm)],[c_899,c_832]) ).
cnf(c_996,plain,
multiply(multiply(inverse(inverse(B)),inverse(inverse(inverse(inverse(A))))),inverse(A)) = B,
inference(paramod,[status(thm)],[c_903,c_894]) ).
cnf(c_907,plain,
multiply(multiply(inverse(inverse(A)),B),inverse(B)) = A,
inference(paramod,[status(thm)],[c_899,c_996]) ).
cnf(c_997,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_997]) ).
cnf(c_998,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_999,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_998]) ).
cnf(c_1000,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_999]) ).
cnf(c_1001,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_1000]) ).
cnf(c_1002,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_1001]) ).
cnf(c_1003,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_1002]) ).
cnf(c_1004,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_1003]) ).
cnf(c_1005,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_1004]) ).
cnf(c_1006,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_1005]) ).
cnf(c_1007,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_1006]) ).
cnf(c_1008,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_1007]) ).
cnf(c_1009,plain,
multiply(inverse(inverse(A)),multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C))) = A,
inference(paramod,[status(thm)],[c_899,c_1008]) ).
cnf(c_1010,plain,
multiply(A,inverse(inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C))))) = A,
inference(paramod,[status(thm)],[c_910,c_1009]) ).
cnf(c_1011,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_1010]) ).
cnf(c_1012,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_1011]) ).
cnf(c_1013,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_1012]) ).
cnf(c_1014,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_1013]) ).
cnf(c_1015,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_1014]) ).
cnf(c_1016,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_1015]) ).
cnf(c_1017,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_1016]) ).
cnf(c_1018,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_1017]) ).
cnf(c_1019,plain,
multiply(A,inverse(multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C)))) = A,
inference(paramod,[status(thm)],[c_899,c_1018]) ).
cnf(c_1020,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_1019]) ).
cnf(c_1021,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_1020]) ).
cnf(c_1022,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_1021]) ).
cnf(c_1023,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_1022]) ).
cnf(c_1024,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),inverse(inverse(multiply(B,C))))) = A,
inference(paramod,[status(thm)],[c_899,c_1023]) ).
cnf(c_1025,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_1024]) ).
cnf(c_1026,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_1025]) ).
cnf(c_1027,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_1026]) ).
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_1027]) ).
cnf(c_1028,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_1029,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_1028]) ).
cnf(c_1030,plain,
multiply(A,multiply(multiply(inverse(C),inverse(inverse(inverse(B)))),multiply(B,C))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_899,c_1029]) ).
cnf(c_1031,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_914,c_1030]) ).
cnf(c_915,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_1031]) ).
cnf(c_921,plain,
multiply(multiply(A,B),inverse(B)) = A,
inference(paramod,[status(thm)],[c_915,c_907]) ).
cnf(c_1032,plain,
multiply(multiply(A,multiply(B,C)),inverse(C)) = multiply(inverse(inverse(A)),B),
inference(paramod,[status(thm)],[c_915,c_906]) ).
cnf(c_922,plain,
multiply(multiply(A,multiply(B,C)),inverse(C)) = multiply(A,B),
inference(paramod,[status(thm)],[c_915,c_1032]) ).
cnf(c_923,plain,
multiply(inverse(A),A) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_915,c_898]) ).
cnf(c_1033,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(A,inverse(A)),a2) != a2
| multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ),
inference(paramod,[status(thm)],[c_923,c_3]) ).
cnf(c_1034,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2
| multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ),
inference(paramod,[status(thm)],[c_905,c_1033]) ).
cnf(c_929,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ),
inference(copy,[status(thm)],[c_1034]) ).
cnf(c_930,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_923,c_923]) ).
cnf(c_931,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(resolve,[status(thm)],[c_930,c_929]) ).
cnf(c_1035,plain,
multiply(multiply(A,B),inverse(inverse(C))) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_922,c_921]) ).
cnf(c_947,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_915,c_1035]) ).
cnf(c_948,plain,
$false,
inference(resolve,[status(thm)],[c_947,c_931]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP057-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 14:21:18 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 3100512 was started by sandbox on n020,
% 0.09/0.36 % Fri Sep 25 14:21:18 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 3.02/0.94
% 3.02/0.94 % Assigning unary symbol inverse kb_weight 0 and highest precedence (10).
% 3.02/0.94
% 3.02/0.94 % SZS status Unsatisfiable for theBenchmark
% 3.02/0.94
% 3.02/0.94 % Proof 1 at 0.25 (+ 0.11) seconds.
% 3.02/0.94 % Length of proof is 81.
% 3.02/0.94 % Level of proof is 29.
% 3.02/0.94 % Maximum clause weight is 99.000.
% 3.02/0.94 % Given clauses 61.
% 3.02/0.94
% 3.02/0.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------