%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP059-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 : n013.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:54 AM UTC 2026
% Result : Unsatisfiable 2.92s 1.41s
% Output : CNFRefutation 2.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 2
% Syntax : Number of formulae : 111 ( 103 unt; 0 def)
% Number of atoms : 123 ( 122 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 33 ( 21 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 15 ( 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 : 333 ( 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,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,
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_1268,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_13,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_1268]) ).
cnf(c_1269,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_7]) ).
cnf(c_15,plain,
inverse(multiply(A,inverse(A))) = inverse(multiply(B,inverse(B))),
inference(paramod,[status(thm)],[c_7,c_1269]) ).
cnf(c_18,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_15,c_5]) ).
cnf(c_22,plain,
inverse(multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B))))) = inverse(multiply(C,inverse(C))),
inference(paramod,[status(thm)],[c_15,c_15]) ).
cnf(c_23,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_18,c_1]) ).
cnf(c_1270,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_18,c_4]) ).
cnf(c_25,plain,
inverse(multiply(multiply(inverse(multiply(A,inverse(A))),B),inverse(B))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_7,c_1270]) ).
cnf(c_1271,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_18,c_7]) ).
cnf(c_26,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_1271]) ).
cnf(c_1272,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_18,c_7]) ).
cnf(c_27,plain,
inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),B)) = inverse(multiply(multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,inverse(D)))),B),multiply(E,inverse(E)))),
inference(copy,[status(thm)],[c_1272]) ).
cnf(c_33,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_15,c_18]) ).
cnf(c_49,plain,
inverse(multiply(multiply(A,inverse(A)),inverse(multiply(multiply(B,inverse(B)),inverse(multiply(multiply(C,inverse(C)),inverse(multiply(D,inverse(D))))))))) = inverse(multiply(E,inverse(E))),
inference(paramod,[status(thm)],[c_22,c_22]) ).
cnf(c_51,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_25,c_1]) ).
cnf(c_86,plain,
inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),B)) = inverse(B),
inference(paramod,[status(thm)],[c_51,c_27]) ).
cnf(c_88,plain,
inverse(inverse(multiply(A,inverse(A)))) = inverse(multiply(multiply(B,inverse(B)),multiply(C,inverse(C)))),
inference(paramod,[status(thm)],[c_86,c_26]) ).
cnf(c_1273,plain,
inverse(B) = inverse(multiply(multiply(multiply(C,inverse(C)),B),multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_86,c_13]) ).
cnf(c_89,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),multiply(C,inverse(C)))) = inverse(B),
inference(copy,[status(thm)],[c_1273]) ).
cnf(c_1274,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),inverse(inverse(inverse(multiply(multiply(B,inverse(B)),C))))),multiply(D,inverse(D)))) = C,
inference(paramod,[status(thm)],[c_5,c_6]) ).
cnf(c_92,plain,
inverse(inverse(inverse(inverse(multiply(multiply(A,inverse(A)),B))))) = B,
inference(paramod,[status(thm)],[c_89,c_1274]) ).
cnf(c_1275,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_33,c_7]) ).
cnf(c_1276,plain,
inverse(inverse(multiply(B,inverse(B)))) = inverse(multiply(inverse(inverse(multiply(D,inverse(D)))),inverse(multiply(E,inverse(E))))),
inference(paramod,[status(thm)],[c_89,c_1275]) ).
cnf(c_121,plain,
inverse(inverse(multiply(A,inverse(A)))) = inverse(inverse(multiply(B,inverse(B)))),
inference(paramod,[status(thm)],[c_86,c_1276]) ).
cnf(c_216,plain,
inverse(multiply(inverse(multiply(multiply(A,inverse(A)),multiply(B,inverse(B)))),C)) = inverse(C),
inference(paramod,[status(thm)],[c_88,c_86]) ).
cnf(c_1277,plain,
inverse(multiply(inverse(inverse(inverse(inverse(multiply(multiply(A,inverse(A)),multiply(B,inverse(B))))))),C)) = inverse(C),
inference(paramod,[status(thm)],[c_216,c_86]) ).
cnf(c_445,plain,
inverse(multiply(multiply(A,inverse(A)),B)) = inverse(B),
inference(paramod,[status(thm)],[c_92,c_1277]) ).
cnf(c_574,plain,
inverse(inverse(inverse(inverse(A)))) = A,
inference(paramod,[status(thm)],[c_445,c_92]) ).
cnf(c_1278,plain,
inverse(multiply(multiply(A,inverse(A)),inverse(multiply(multiply(B,inverse(B)),inverse(inverse(multiply(D,inverse(D)))))))) = inverse(multiply(E,inverse(E))),
inference(paramod,[status(thm)],[c_445,c_49]) ).
cnf(c_1279,plain,
inverse(multiply(multiply(A,inverse(A)),inverse(inverse(inverse(multiply(D,inverse(D))))))) = inverse(multiply(E,inverse(E))),
inference(paramod,[status(thm)],[c_445,c_1278]) ).
cnf(c_1280,plain,
inverse(inverse(inverse(inverse(multiply(D,inverse(D)))))) = inverse(multiply(E,inverse(E))),
inference(paramod,[status(thm)],[c_445,c_1279]) ).
cnf(c_1281,plain,
multiply(D,inverse(D)) = inverse(multiply(E,inverse(E))),
inference(paramod,[status(thm)],[c_574,c_1280]) ).
cnf(c_578,plain,
inverse(multiply(A,inverse(A))) = multiply(B,inverse(B)),
inference(copy,[status(thm)],[c_1281]) ).
cnf(c_580,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_445,c_23]) ).
cnf(c_583,plain,
inverse(multiply(multiply(multiply(inverse(A),B),inverse(B)),multiply(C,inverse(C)))) = A,
inference(paramod,[status(thm)],[c_445,c_6]) ).
cnf(c_614,plain,
inverse(multiply(multiply(multiply(multiply(A,inverse(A)),B),C),multiply(D,inverse(D)))) = inverse(multiply(B,C)),
inference(paramod,[status(thm)],[c_578,c_1]) ).
cnf(c_1282,plain,
inverse(multiply(multiply(inverse(multiply(A,inverse(A))),B),multiply(C,inverse(C)))) = inverse(multiply(inverse(inverse(multiply(D,inverse(D)))),B)),
inference(paramod,[status(thm)],[c_578,c_7]) ).
cnf(c_623,plain,
inverse(multiply(multiply(inverse(multiply(A,inverse(A))),B),multiply(C,inverse(C)))) = inverse(B),
inference(paramod,[status(thm)],[c_86,c_1282]) ).
cnf(c_638,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),inverse(multiply(C,inverse(C))))) = inverse(B),
inference(paramod,[status(thm)],[c_578,c_89]) ).
cnf(c_1283,plain,
inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(C,inverse(C))),A)),B),multiply(D,inverse(D)))),E)),F),inverse(F)),multiply(V6,inverse(V6)))) = E,
inference(paramod,[status(thm)],[c_10,c_1]) ).
cnf(c_649,plain,
multiply(inverse(multiply(multiply(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(C,inverse(C))),A)),B),multiply(D,inverse(D)))),E) = E,
inference(paramod,[status(thm)],[c_583,c_1283]) ).
cnf(c_1284,plain,
inverse(multiply(multiply(multiply(multiply(A,inverse(A)),multiply(inverse(multiply(B,inverse(B))),multiply(multiply(C,multiply(inverse(multiply(multiply(D,E),C)),D)),E))),multiply(F,inverse(F))),multiply(V6,inverse(V6)))) = multiply(V7,inverse(V7)),
inference(paramod,[status(thm)],[c_4,c_10]) ).
cnf(c_1285,plain,
inverse(multiply(multiply(inverse(multiply(B,inverse(B))),multiply(multiply(C,multiply(inverse(multiply(multiply(D,E),C)),D)),E)),multiply(F,inverse(F)))) = multiply(V7,inverse(V7)),
inference(paramod,[status(thm)],[c_614,c_1284]) ).
cnf(c_651,plain,
inverse(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C)) = multiply(D,inverse(D)),
inference(paramod,[status(thm)],[c_623,c_1285]) ).
cnf(c_1286,plain,
inverse(multiply(multiply(inverse(multiply(multiply(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(C,inverse(C))),A)),B),multiply(D,inverse(D)))),E),multiply(F,inverse(F)))) = inverse(multiply(inverse(inverse(multiply(V6,inverse(V6)))),E)),
inference(paramod,[status(thm)],[c_10,c_7]) ).
cnf(c_1287,plain,
inverse(multiply(E,multiply(F,inverse(F)))) = inverse(multiply(inverse(inverse(multiply(V6,inverse(V6)))),E)),
inference(paramod,[status(thm)],[c_649,c_1286]) ).
cnf(c_652,plain,
inverse(multiply(A,multiply(B,inverse(B)))) = inverse(A),
inference(paramod,[status(thm)],[c_86,c_1287]) ).
cnf(c_1288,plain,
inverse(inverse(multiply(multiply(multiply(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(C,inverse(C))),A)),B),multiply(D,inverse(D))),multiply(E,inverse(E))))) = inverse(inverse(multiply(F,inverse(F)))),
inference(paramod,[status(thm)],[c_10,c_121]) ).
cnf(c_1289,plain,
inverse(inverse(multiply(multiply(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(C,inverse(C))),A)),B),multiply(D,inverse(D))))) = inverse(inverse(multiply(F,inverse(F)))),
inference(paramod,[status(thm)],[c_652,c_1288]) ).
cnf(c_681,plain,
inverse(inverse(multiply(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(C,inverse(C))),A)),B))) = inverse(inverse(multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_652,c_1289]) ).
cnf(c_710,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),C)) = inverse(multiply(B,C)),
inference(paramod,[status(thm)],[c_652,c_614]) ).
cnf(c_711,plain,
inverse(multiply(multiply(inverse(A),B),inverse(B))) = A,
inference(paramod,[status(thm)],[c_652,c_583]) ).
cnf(c_714,plain,
inverse(multiply(multiply(inverse(A),multiply(B,inverse(B))),inverse(multiply(C,inverse(C))))) = A,
inference(paramod,[status(thm)],[c_652,c_580]) ).
cnf(c_722,plain,
inverse(multiply(A,inverse(multiply(B,inverse(B))))) = inverse(A),
inference(paramod,[status(thm)],[c_710,c_638]) ).
cnf(c_1290,plain,
inverse(multiply(inverse(A),multiply(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_722,c_714]) ).
cnf(c_734,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_652,c_1290]) ).
cnf(c_1291,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(C,inverse(C))),A)),B) = inverse(inverse(multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_734,c_681]) ).
cnf(c_748,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(C,inverse(C))),A)),B) = multiply(D,inverse(D)),
inference(paramod,[status(thm)],[c_734,c_1291]) ).
cnf(c_810,plain,
multiply(inverse(A),A) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_734,c_5]) ).
cnf(c_825,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_810,c_3]) ).
cnf(c_830,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_734,c_810]) ).
cnf(c_831,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(A,inverse(A)),a2) != a2 ),
inference(resolve,[status(thm)],[c_830,c_825]) ).
cnf(c_1292,plain,
inverse(inverse(A)) = multiply(multiply(B,inverse(B)),A),
inference(paramod,[status(thm)],[c_445,c_734]) ).
cnf(c_1293,plain,
A = multiply(multiply(B,inverse(B)),A),
inference(paramod,[status(thm)],[c_734,c_1292]) ).
cnf(c_992,plain,
multiply(multiply(A,inverse(A)),B) = B,
inference(copy,[status(thm)],[c_1293]) ).
cnf(c_1294,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(multiply(multiply(A,inverse(A)),B),inverse(B)),a2) != a2 ),
inference(paramod,[status(thm)],[c_445,c_831]) ).
cnf(c_1295,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(B,inverse(B)),a2) != a2 ),
inference(paramod,[status(thm)],[c_992,c_1294]) ).
cnf(c_1296,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_992,c_1295]) ).
cnf(c_999,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(copy,[status(thm)],[c_1296]) ).
cnf(c_1297,plain,
multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))),C) = C,
inference(paramod,[status(thm)],[c_15,c_992]) ).
cnf(c_1039,plain,
multiply(inverse(multiply(A,inverse(A))),B) = B,
inference(paramod,[status(thm)],[c_992,c_1297]) ).
cnf(c_1056,plain,
multiply(multiply(inverse(multiply(A,B)),A),B) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_1039,c_748]) ).
cnf(c_1298,plain,
inverse(A) = multiply(multiply(inverse(A),B),inverse(B)),
inference(paramod,[status(thm)],[c_711,c_734]) ).
cnf(c_1122,plain,
multiply(multiply(inverse(A),B),inverse(B)) = inverse(A),
inference(copy,[status(thm)],[c_1298]) ).
cnf(c_1299,plain,
multiply(multiply(A,B),inverse(B)) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_734,c_1122]) ).
cnf(c_1125,plain,
multiply(multiply(A,B),inverse(B)) = A,
inference(paramod,[status(thm)],[c_734,c_1299]) ).
cnf(c_1128,plain,
multiply(multiply(A,inverse(B)),B) = A,
inference(paramod,[status(thm)],[c_734,c_1125]) ).
cnf(c_1300,plain,
multiply(multiply(A,inverse(A)),inverse(B)) = multiply(inverse(multiply(C,B)),C),
inference(paramod,[status(thm)],[c_1056,c_1125]) ).
cnf(c_1301,plain,
inverse(B) = multiply(inverse(multiply(C,B)),C),
inference(paramod,[status(thm)],[c_992,c_1300]) ).
cnf(c_1141,plain,
multiply(inverse(multiply(A,B)),A) = inverse(B),
inference(copy,[status(thm)],[c_1301]) ).
cnf(c_1302,plain,
multiply(multiply(A,inverse(A)),multiply(B,multiply(inverse(multiply(multiply(C,D),B)),C))) = inverse(D),
inference(paramod,[status(thm)],[c_651,c_1141]) ).
cnf(c_1145,plain,
multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)) = inverse(C),
inference(paramod,[status(thm)],[c_992,c_1302]) ).
cnf(c_1303,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_1141,c_1125]) ).
cnf(c_1146,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_1303]) ).
cnf(c_1304,plain,
multiply(inverse(A),multiply(A,B)) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_1125,c_1141]) ).
cnf(c_1147,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(paramod,[status(thm)],[c_734,c_1304]) ).
cnf(c_1305,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(B,C))),B)) = inverse(C),
inference(paramod,[status(thm)],[c_1146,c_1145]) ).
cnf(c_1158,plain,
multiply(A,multiply(multiply(inverse(A),multiply(inverse(B),inverse(C))),C)) = inverse(B),
inference(paramod,[status(thm)],[c_1146,c_1305]) ).
cnf(c_1180,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_734,c_1147]) ).
cnf(c_1306,plain,
multiply(A,inverse(B)) = multiply(multiply(inverse(inverse(A)),multiply(inverse(B),inverse(C))),C),
inference(paramod,[status(thm)],[c_1158,c_1180]) ).
cnf(c_1307,plain,
multiply(A,inverse(B)) = multiply(multiply(A,multiply(inverse(B),inverse(C))),C),
inference(paramod,[status(thm)],[c_734,c_1306]) ).
cnf(c_1241,plain,
multiply(multiply(A,multiply(inverse(B),inverse(C))),C) = multiply(A,inverse(B)),
inference(copy,[status(thm)],[c_1307]) ).
cnf(c_1308,plain,
multiply(A,B) = multiply(multiply(A,inverse(multiply(inverse(C),inverse(B)))),inverse(C)),
inference(paramod,[status(thm)],[c_1128,c_1241]) ).
cnf(c_1309,plain,
multiply(A,B) = multiply(multiply(A,multiply(inverse(inverse(B)),inverse(inverse(C)))),inverse(C)),
inference(paramod,[status(thm)],[c_1146,c_1308]) ).
cnf(c_1310,plain,
multiply(A,B) = multiply(multiply(A,multiply(B,inverse(inverse(C)))),inverse(C)),
inference(paramod,[status(thm)],[c_734,c_1309]) ).
cnf(c_1311,plain,
multiply(A,B) = multiply(multiply(A,multiply(B,C)),inverse(C)),
inference(paramod,[status(thm)],[c_734,c_1310]) ).
cnf(c_1246,plain,
multiply(multiply(A,multiply(B,C)),inverse(C)) = multiply(A,B),
inference(copy,[status(thm)],[c_1311]) ).
cnf(c_1312,plain,
multiply(multiply(A,B),inverse(inverse(C))) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_1246,c_1125]) ).
cnf(c_1266,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_734,c_1312]) ).
cnf(c_1267,plain,
$false,
inference(resolve,[status(thm)],[c_1266,c_999]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP059-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.44 % Computer : n013.cluster.edu
% 0.09/0.44 % Model : x86_64 x86_64
% 0.09/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.44 % Memory : 8046.5625MB
% 0.09/0.44 % OS : Linux 6.8.0-71-generic
% 0.09/0.44 % CPULimit : 300
% 0.09/0.44 % WCLimit : 300
% 0.09/0.44 % DateTime : Fri Sep 25 14:19:51 UTC 2026
% 0.09/0.45 % CPUTime :
% 0.09/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.45 % Process 598641 was started by sandbox on n013,
% 0.09/0.45 % Fri Sep 25 14:19:51 2026
% 0.09/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.46
% 0.09/0.46 % From the command line: assign(max_seconds, 300).
% 2.92/1.41
% 2.92/1.41 % Assigning unary symbol inverse kb_weight 0 and highest precedence (10).
% 2.92/1.41
% 2.92/1.41 % SZS status Unsatisfiable for theBenchmark
% 2.92/1.41
% 2.92/1.41 % Proof 1 at 0.27 (+ 0.11) seconds.
% 2.92/1.41 % Length of proof is 64.
% 2.92/1.41 % Level of proof is 27.
% 2.92/1.41 % Maximum clause weight is 96.000.
% 2.92/1.41 % Given clauses 73.
% 2.92/1.41
% 2.92/1.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------