%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP433-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 : n026.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:32 AM UTC 2026
% Result : Unsatisfiable 1.68s 0.92s
% Output : CNFRefutation 1.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 2
% Syntax : Number of formulae : 69 ( 69 unt; 0 def)
% Number of atoms : 69 ( 68 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 : 14 ( 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 : 224 ( 0 sgn 4 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : inverse(multiply(multiply(multiply(inverse(multiply(multiply(VAR_0,VAR_1),VAR_2)),VAR_0),VAR_1),multiply(VAR_3,inverse(VAR_3)))) = VAR_2,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(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,
inverse(multiply(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C),multiply(D,inverse(D)))) = multiply(E,inverse(E)),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_5,plain,
multiply(A,inverse(A)) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_4,c_4]) ).
cnf(c_6,plain,
inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,inverse(A)),B)),C),inverse(C)),multiply(D,inverse(D)))) = B,
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_7,plain,
inverse(multiply(multiply(multiply(inverse(multiply(A,inverse(A))),B),C),multiply(D,inverse(D)))) = inverse(multiply(B,C)),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_10,plain,
inverse(multiply(multiply(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(C,inverse(C))),A)),B),multiply(D,inverse(D)))) = multiply(E,inverse(E)),
inference(paramod,[status(thm)],[c_5,c_4]) ).
cnf(c_1017,plain,
inverse(multiply(multiply(multiply(inverse(multiply(A,inverse(A))),B),inverse(B)),multiply(C,inverse(C)))) = inverse(multiply(D,inverse(D))),
inference(paramod,[status(thm)],[c_5,c_6]) ).
cnf(c_12,plain,
inverse(multiply(A,inverse(A))) = inverse(multiply(B,inverse(B))),
inference(paramod,[status(thm)],[c_7,c_1017]) ).
cnf(c_15,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_12,c_5]) ).
cnf(c_16,plain,
inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,inverse(A)),B)),multiply(C,inverse(C))),inverse(multiply(D,inverse(D)))),multiply(E,inverse(E)))) = B,
inference(paramod,[status(thm)],[c_12,c_6]) ).
cnf(c_1018,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))) = multiply(multiply(multiply(multiply(inverse(multiply(multiply(C,D),E)),C),D),multiply(F,inverse(F))),E),
inference(paramod,[status(thm)],[c_1,c_15]) ).
cnf(c_20,plain,
multiply(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(D))),C) = multiply(multiply(E,inverse(E)),inverse(multiply(F,inverse(F)))),
inference(copy,[status(thm)],[c_1018]) ).
cnf(c_1019,plain,
inverse(multiply(multiply(multiply(inverse(multiply(A,inverse(A))),multiply(inverse(multiply(B,inverse(B))),C)),inverse(C)),multiply(D,inverse(D)))) = multiply(E,inverse(E)),
inference(paramod,[status(thm)],[c_15,c_4]) ).
cnf(c_21,plain,
inverse(multiply(multiply(inverse(multiply(A,inverse(A))),B),inverse(B))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_7,c_1019]) ).
cnf(c_24,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))) = multiply(multiply(C,inverse(C)),inverse(multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_12,c_15]) ).
cnf(c_41,plain,
inverse(multiply(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))),C),multiply(D,inverse(D)))) = inverse(C),
inference(paramod,[status(thm)],[c_21,c_1]) ).
cnf(c_1020,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),multiply(C,inverse(C)))) = inverse(multiply(inverse(inverse(multiply(D,inverse(D)))),B)),
inference(paramod,[status(thm)],[c_5,c_7]) ).
cnf(c_96,plain,
inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),B)) = inverse(multiply(multiply(multiply(C,inverse(C)),B),multiply(D,inverse(D)))),
inference(copy,[status(thm)],[c_1020]) ).
cnf(c_1021,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(B,inverse(B)))) = inverse(multiply(inverse(inverse(multiply(C,inverse(C)))),inverse(multiply(D,inverse(D))))),
inference(paramod,[status(thm)],[c_15,c_7]) ).
cnf(c_102,plain,
inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),inverse(multiply(B,inverse(B))))) = inverse(multiply(multiply(C,inverse(C)),multiply(D,inverse(D)))),
inference(copy,[status(thm)],[c_1021]) ).
cnf(c_1022,plain,
inverse(multiply(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))),C),multiply(D,inverse(D)))) = inverse(multiply(inverse(inverse(multiply(E,inverse(E)))),C)),
inference(paramod,[status(thm)],[c_15,c_7]) ).
cnf(c_1023,plain,
inverse(C) = inverse(multiply(inverse(inverse(multiply(E,inverse(E)))),C)),
inference(paramod,[status(thm)],[c_41,c_1022]) ).
cnf(c_103,plain,
inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),B)) = inverse(B),
inference(copy,[status(thm)],[c_1023]) ).
cnf(c_1024,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))),multiply(C,inverse(C)))) = inverse(multiply(inverse(inverse(multiply(D,inverse(D)))),inverse(multiply(E,inverse(E))))),
inference(paramod,[status(thm)],[c_24,c_7]) ).
cnf(c_1025,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))),multiply(C,inverse(C)))) = inverse(inverse(multiply(E,inverse(E)))),
inference(paramod,[status(thm)],[c_103,c_1024]) ).
cnf(c_110,plain,
inverse(inverse(multiply(A,inverse(A)))) = inverse(multiply(multiply(multiply(B,inverse(B)),inverse(multiply(C,inverse(C)))),multiply(D,inverse(D)))),
inference(copy,[status(thm)],[c_1025]) ).
cnf(c_113,plain,
inverse(inverse(multiply(A,inverse(A)))) = inverse(multiply(multiply(B,inverse(B)),multiply(C,inverse(C)))),
inference(paramod,[status(thm)],[c_103,c_102]) ).
cnf(c_1026,plain,
inverse(B) = inverse(multiply(multiply(multiply(C,inverse(C)),B),multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_103,c_96]) ).
cnf(c_114,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),multiply(C,inverse(C)))) = inverse(B),
inference(copy,[status(thm)],[c_1026]) ).
cnf(c_115,plain,
inverse(inverse(multiply(A,inverse(A)))) = inverse(inverse(multiply(B,inverse(B)))),
inference(paramod,[status(thm)],[c_114,c_110]) ).
cnf(c_121,plain,
multiply(inverse(multiply(A,inverse(A))),inverse(inverse(multiply(B,inverse(B))))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_115,c_5]) ).
cnf(c_1027,plain,
inverse(multiply(multiply(multiply(inverse(multiply(A,inverse(A))),inverse(inverse(multiply(B,inverse(B))))),inverse(inverse(inverse(multiply(multiply(C,inverse(C)),D))))),multiply(E,inverse(E)))) = D,
inference(paramod,[status(thm)],[c_121,c_6]) ).
cnf(c_1028,plain,
inverse(multiply(inverse(inverse(multiply(B,inverse(B)))),inverse(inverse(inverse(multiply(multiply(C,inverse(C)),D)))))) = D,
inference(paramod,[status(thm)],[c_7,c_1027]) ).
cnf(c_187,plain,
inverse(inverse(inverse(inverse(multiply(multiply(A,inverse(A)),B))))) = B,
inference(paramod,[status(thm)],[c_103,c_1028]) ).
cnf(c_258,plain,
inverse(multiply(inverse(multiply(multiply(A,inverse(A)),multiply(B,inverse(B)))),C)) = inverse(C),
inference(paramod,[status(thm)],[c_113,c_103]) ).
cnf(c_1029,plain,
multiply(A,inverse(A)) = inverse(multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C)))),
inference(paramod,[status(thm)],[c_10,c_6]) ).
cnf(c_356,plain,
inverse(multiply(inverse(multiply(A,inverse(A))),multiply(B,inverse(B)))) = multiply(C,inverse(C)),
inference(copy,[status(thm)],[c_1029]) ).
cnf(c_455,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),inverse(multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D)))))) = inverse(B),
inference(paramod,[status(thm)],[c_356,c_114]) ).
cnf(c_1030,plain,
inverse(multiply(inverse(inverse(inverse(inverse(multiply(multiply(A,inverse(A)),multiply(B,inverse(B))))))),C)) = inverse(C),
inference(paramod,[status(thm)],[c_258,c_103]) ).
cnf(c_573,plain,
inverse(multiply(multiply(A,inverse(A)),B)) = inverse(B),
inference(paramod,[status(thm)],[c_187,c_1030]) ).
cnf(c_1031,plain,
inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),multiply(inverse(multiply(multiply(B,inverse(B)),multiply(C,inverse(C)))),D))) = inverse(D),
inference(paramod,[status(thm)],[c_258,c_103]) ).
cnf(c_1032,plain,
inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),multiply(inverse(multiply(C,inverse(C))),D))) = inverse(D),
inference(paramod,[status(thm)],[c_573,c_1031]) ).
cnf(c_574,plain,
inverse(multiply(inverse(multiply(A,inverse(A))),B)) = inverse(B),
inference(paramod,[status(thm)],[c_103,c_1032]) ).
cnf(c_1033,plain,
inverse(multiply(inverse(multiply(multiply(A,inverse(A)),multiply(inverse(multiply(B,inverse(B))),inverse(inverse(multiply(C,inverse(C))))))),D)) = inverse(D),
inference(paramod,[status(thm)],[c_121,c_258]) ).
cnf(c_1034,plain,
inverse(multiply(inverse(multiply(inverse(multiply(B,inverse(B))),inverse(inverse(multiply(C,inverse(C)))))),D)) = inverse(D),
inference(paramod,[status(thm)],[c_573,c_1033]) ).
cnf(c_582,plain,
inverse(multiply(inverse(inverse(inverse(multiply(A,inverse(A))))),B)) = inverse(B),
inference(paramod,[status(thm)],[c_574,c_1034]) ).
cnf(c_1035,plain,
inverse(multiply(inverse(inverse(inverse(multiply(multiply(A,inverse(A)),multiply(B,inverse(B)))))),multiply(C,inverse(C)))) = multiply(D,inverse(D)),
inference(paramod,[status(thm)],[c_258,c_356]) ).
cnf(c_1036,plain,
inverse(multiply(inverse(inverse(inverse(multiply(B,inverse(B))))),multiply(C,inverse(C)))) = multiply(D,inverse(D)),
inference(paramod,[status(thm)],[c_573,c_1035]) ).
cnf(c_605,plain,
inverse(multiply(A,inverse(A))) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_582,c_1036]) ).
cnf(c_716,plain,
inverse(multiply(multiply(multiply(inverse(A),multiply(B,inverse(B))),inverse(multiply(C,inverse(C)))),multiply(D,inverse(D)))) = A,
inference(paramod,[status(thm)],[c_573,c_16]) ).
cnf(c_730,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),inverse(multiply(C,inverse(C))))) = inverse(B),
inference(paramod,[status(thm)],[c_574,c_455]) ).
cnf(c_771,plain,
inverse(multiply(multiply(multiply(multiply(A,inverse(A)),B),C),multiply(D,inverse(D)))) = inverse(multiply(B,C)),
inference(paramod,[status(thm)],[c_605,c_1]) ).
cnf(c_1037,plain,
inverse(multiply(multiply(multiply(inverse(multiply(multiply(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(D))),C),E)),multiply(F,inverse(F))),inverse(multiply(V6,inverse(V6)))),multiply(V7,inverse(V7)))) = E,
inference(paramod,[status(thm)],[c_20,c_1]) ).
cnf(c_840,plain,
multiply(multiply(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(D))),C),E) = E,
inference(paramod,[status(thm)],[c_716,c_1037]) ).
cnf(c_1038,plain,
inverse(multiply(multiply(multiply(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(D))),C),E),multiply(F,inverse(F)))) = inverse(E),
inference(paramod,[status(thm)],[c_20,c_114]) ).
cnf(c_845,plain,
inverse(multiply(A,multiply(B,inverse(B)))) = inverse(A),
inference(paramod,[status(thm)],[c_840,c_1038]) ).
cnf(c_859,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),C)) = inverse(multiply(B,C)),
inference(paramod,[status(thm)],[c_845,c_771]) ).
cnf(c_863,plain,
inverse(multiply(multiply(inverse(A),multiply(B,inverse(B))),inverse(multiply(C,inverse(C))))) = A,
inference(paramod,[status(thm)],[c_845,c_716]) ).
cnf(c_874,plain,
inverse(multiply(A,inverse(multiply(B,inverse(B))))) = inverse(A),
inference(paramod,[status(thm)],[c_859,c_730]) ).
cnf(c_1039,plain,
inverse(multiply(inverse(A),multiply(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_874,c_863]) ).
cnf(c_885,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_845,c_1039]) ).
cnf(c_955,plain,
multiply(inverse(A),A) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_885,c_5]) ).
cnf(c_1040,plain,
multiply(A,inverse(A)) != multiply(inverse(a1),a1),
inference(paramod,[status(thm)],[c_955,c_3]) ).
cnf(c_1015,plain,
multiply(inverse(a1),a1) != multiply(A,inverse(A)),
inference(copy,[status(thm)],[c_1040]) ).
cnf(c_1016,plain,
$false,
inference(resolve,[status(thm)],[c_1015,c_955]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP433-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.40 % Computer : n026.cluster.edu
% 0.08/0.40 % Model : x86_64 x86_64
% 0.08/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.40 % Memory : 8046.5625MB
% 0.08/0.40 % OS : Linux 6.8.0-71-generic
% 0.08/0.40 % CPULimit : 300
% 0.08/0.40 % WCLimit : 300
% 0.08/0.40 % DateTime : Fri Sep 25 14:56:39 UTC 2026
% 0.08/0.40 % CPUTime :
% 0.08/0.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.41 % Process 2816725 was started by sandbox on n026,
% 0.08/0.41 % Fri Sep 25 14:56:39 2026
% 0.08/0.41 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.41
% 0.08/0.41 % From the command line: assign(max_seconds, 300).
% 1.68/0.92
% 1.68/0.92 % SZS status Unsatisfiable for theBenchmark
% 1.68/0.92
% 1.68/0.92 % Proof 1 at 0.17 (+ 0.05) seconds.
% 1.68/0.92 % Length of proof is 43.
% 1.68/0.92 % Level of proof is 23.
% 1.68/0.92 % Maximum clause weight is 98.000.
% 1.68/0.92 % Given clauses 34.
% 1.68/0.92
% 1.68/0.92 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------