%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP435-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 : n019.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 2.36s 0.75s
% Output : CNFRefutation 2.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 2
% Syntax : Number of formulae : 102 ( 102 unt; 0 def)
% Number of atoms : 102 ( 101 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 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 : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 324 ( 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_3,axiom,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('theBenchmark.p',prove_these_axioms_3) ).
cnf(c_2,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(clausify,[status(thm)],[prove_these_axioms_3]) ).
cnf(c_3,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_4,plain,
multiply(A,inverse(A)) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_3,c_3]) ).
cnf(c_5,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_4,c_1]) ).
cnf(c_6,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_4,c_1]) ).
cnf(c_9,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_4,c_3]) ).
cnf(c_1244,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_4,c_6]) ).
cnf(c_12,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_1244]) ).
cnf(c_1245,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_4,c_6]) ).
cnf(c_14,plain,
inverse(multiply(A,inverse(A))) = inverse(multiply(B,inverse(B))),
inference(paramod,[status(thm)],[c_6,c_1245]) ).
cnf(c_17,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_14,c_4]) ).
cnf(c_21,plain,
inverse(multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B))))) = inverse(multiply(C,inverse(C))),
inference(paramod,[status(thm)],[c_14,c_14]) ).
cnf(c_22,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_17,c_1]) ).
cnf(c_1246,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_17,c_3]) ).
cnf(c_24,plain,
inverse(multiply(multiply(inverse(multiply(A,inverse(A))),B),inverse(B))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_6,c_1246]) ).
cnf(c_1247,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_17,c_6]) ).
cnf(c_25,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_1247]) ).
cnf(c_1248,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_17,c_6]) ).
cnf(c_26,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_1248]) ).
cnf(c_32,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_14,c_17]) ).
cnf(c_48,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_21,c_21]) ).
cnf(c_50,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_24,c_1]) ).
cnf(c_85,plain,
inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),B)) = inverse(B),
inference(paramod,[status(thm)],[c_50,c_26]) ).
cnf(c_87,plain,
inverse(inverse(multiply(A,inverse(A)))) = inverse(multiply(multiply(B,inverse(B)),multiply(C,inverse(C)))),
inference(paramod,[status(thm)],[c_85,c_25]) ).
cnf(c_1249,plain,
inverse(B) = inverse(multiply(multiply(multiply(C,inverse(C)),B),multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_85,c_12]) ).
cnf(c_88,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),multiply(C,inverse(C)))) = inverse(B),
inference(copy,[status(thm)],[c_1249]) ).
cnf(c_1250,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_4,c_5]) ).
cnf(c_91,plain,
inverse(inverse(inverse(inverse(multiply(multiply(A,inverse(A)),B))))) = B,
inference(paramod,[status(thm)],[c_88,c_1250]) ).
cnf(c_1251,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_32,c_6]) ).
cnf(c_1252,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_88,c_1251]) ).
cnf(c_120,plain,
inverse(inverse(multiply(A,inverse(A)))) = inverse(inverse(multiply(B,inverse(B)))),
inference(paramod,[status(thm)],[c_85,c_1252]) ).
cnf(c_215,plain,
inverse(multiply(inverse(multiply(multiply(A,inverse(A)),multiply(B,inverse(B)))),C)) = inverse(C),
inference(paramod,[status(thm)],[c_87,c_85]) ).
cnf(c_1253,plain,
inverse(multiply(inverse(inverse(inverse(inverse(multiply(multiply(A,inverse(A)),multiply(B,inverse(B))))))),C)) = inverse(C),
inference(paramod,[status(thm)],[c_215,c_85]) ).
cnf(c_444,plain,
inverse(multiply(multiply(A,inverse(A)),B)) = inverse(B),
inference(paramod,[status(thm)],[c_91,c_1253]) ).
cnf(c_573,plain,
inverse(inverse(inverse(inverse(A)))) = A,
inference(paramod,[status(thm)],[c_444,c_91]) ).
cnf(c_1254,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_444,c_48]) ).
cnf(c_1255,plain,
inverse(multiply(multiply(A,inverse(A)),inverse(inverse(inverse(multiply(D,inverse(D))))))) = inverse(multiply(E,inverse(E))),
inference(paramod,[status(thm)],[c_444,c_1254]) ).
cnf(c_1256,plain,
inverse(inverse(inverse(inverse(multiply(D,inverse(D)))))) = inverse(multiply(E,inverse(E))),
inference(paramod,[status(thm)],[c_444,c_1255]) ).
cnf(c_1257,plain,
multiply(D,inverse(D)) = inverse(multiply(E,inverse(E))),
inference(paramod,[status(thm)],[c_573,c_1256]) ).
cnf(c_577,plain,
inverse(multiply(A,inverse(A))) = multiply(B,inverse(B)),
inference(copy,[status(thm)],[c_1257]) ).
cnf(c_579,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_444,c_22]) ).
cnf(c_582,plain,
inverse(multiply(multiply(multiply(inverse(A),B),inverse(B)),multiply(C,inverse(C)))) = A,
inference(paramod,[status(thm)],[c_444,c_5]) ).
cnf(c_613,plain,
inverse(multiply(multiply(multiply(multiply(A,inverse(A)),B),C),multiply(D,inverse(D)))) = inverse(multiply(B,C)),
inference(paramod,[status(thm)],[c_577,c_1]) ).
cnf(c_1258,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_577,c_6]) ).
cnf(c_622,plain,
inverse(multiply(multiply(inverse(multiply(A,inverse(A))),B),multiply(C,inverse(C)))) = inverse(B),
inference(paramod,[status(thm)],[c_85,c_1258]) ).
cnf(c_637,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),inverse(multiply(C,inverse(C))))) = inverse(B),
inference(paramod,[status(thm)],[c_577,c_88]) ).
cnf(c_1259,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_9,c_1]) ).
cnf(c_648,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_582,c_1259]) ).
cnf(c_1260,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_3,c_9]) ).
cnf(c_1261,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_613,c_1260]) ).
cnf(c_650,plain,
inverse(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C)) = multiply(D,inverse(D)),
inference(paramod,[status(thm)],[c_622,c_1261]) ).
cnf(c_1262,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_9,c_6]) ).
cnf(c_1263,plain,
inverse(multiply(E,multiply(F,inverse(F)))) = inverse(multiply(inverse(inverse(multiply(V6,inverse(V6)))),E)),
inference(paramod,[status(thm)],[c_648,c_1262]) ).
cnf(c_651,plain,
inverse(multiply(A,multiply(B,inverse(B)))) = inverse(A),
inference(paramod,[status(thm)],[c_85,c_1263]) ).
cnf(c_1264,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_9,c_120]) ).
cnf(c_1265,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_651,c_1264]) ).
cnf(c_680,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_651,c_1265]) ).
cnf(c_709,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),C)) = inverse(multiply(B,C)),
inference(paramod,[status(thm)],[c_651,c_613]) ).
cnf(c_710,plain,
inverse(multiply(multiply(inverse(A),B),inverse(B))) = A,
inference(paramod,[status(thm)],[c_651,c_582]) ).
cnf(c_713,plain,
inverse(multiply(multiply(inverse(A),multiply(B,inverse(B))),inverse(multiply(C,inverse(C))))) = A,
inference(paramod,[status(thm)],[c_651,c_579]) ).
cnf(c_721,plain,
inverse(multiply(A,inverse(multiply(B,inverse(B))))) = inverse(A),
inference(paramod,[status(thm)],[c_709,c_637]) ).
cnf(c_1266,plain,
inverse(multiply(inverse(A),multiply(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_721,c_713]) ).
cnf(c_733,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_651,c_1266]) ).
cnf(c_1267,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_733,c_680]) ).
cnf(c_747,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(C,inverse(C))),A)),B) = multiply(D,inverse(D)),
inference(paramod,[status(thm)],[c_733,c_1267]) ).
cnf(c_1268,plain,
inverse(inverse(A)) = multiply(multiply(B,inverse(B)),A),
inference(paramod,[status(thm)],[c_444,c_733]) ).
cnf(c_1269,plain,
A = multiply(multiply(B,inverse(B)),A),
inference(paramod,[status(thm)],[c_733,c_1268]) ).
cnf(c_969,plain,
multiply(multiply(A,inverse(A)),B) = B,
inference(copy,[status(thm)],[c_1269]) ).
cnf(c_1270,plain,
multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))),C) = C,
inference(paramod,[status(thm)],[c_14,c_969]) ).
cnf(c_1015,plain,
multiply(inverse(multiply(A,inverse(A))),B) = B,
inference(paramod,[status(thm)],[c_969,c_1270]) ).
cnf(c_1032,plain,
multiply(multiply(inverse(multiply(A,B)),A),B) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_1015,c_747]) ).
cnf(c_1271,plain,
inverse(A) = multiply(multiply(inverse(A),B),inverse(B)),
inference(paramod,[status(thm)],[c_710,c_733]) ).
cnf(c_1098,plain,
multiply(multiply(inverse(A),B),inverse(B)) = inverse(A),
inference(copy,[status(thm)],[c_1271]) ).
cnf(c_1272,plain,
multiply(multiply(A,B),inverse(B)) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_733,c_1098]) ).
cnf(c_1101,plain,
multiply(multiply(A,B),inverse(B)) = A,
inference(paramod,[status(thm)],[c_733,c_1272]) ).
cnf(c_1104,plain,
multiply(multiply(A,inverse(B)),B) = A,
inference(paramod,[status(thm)],[c_733,c_1101]) ).
cnf(c_1273,plain,
multiply(multiply(A,inverse(A)),inverse(B)) = multiply(inverse(multiply(C,B)),C),
inference(paramod,[status(thm)],[c_1032,c_1101]) ).
cnf(c_1274,plain,
inverse(B) = multiply(inverse(multiply(C,B)),C),
inference(paramod,[status(thm)],[c_969,c_1273]) ).
cnf(c_1117,plain,
multiply(inverse(multiply(A,B)),A) = inverse(B),
inference(copy,[status(thm)],[c_1274]) ).
cnf(c_1275,plain,
multiply(multiply(A,inverse(A)),multiply(B,multiply(inverse(multiply(multiply(C,D),B)),C))) = inverse(D),
inference(paramod,[status(thm)],[c_650,c_1117]) ).
cnf(c_1121,plain,
multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)) = inverse(C),
inference(paramod,[status(thm)],[c_969,c_1275]) ).
cnf(c_1276,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_1117,c_1101]) ).
cnf(c_1122,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_1276]) ).
cnf(c_1277,plain,
multiply(inverse(A),multiply(A,B)) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_1101,c_1117]) ).
cnf(c_1123,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(paramod,[status(thm)],[c_733,c_1277]) ).
cnf(c_1278,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(B,C))),B)) = inverse(C),
inference(paramod,[status(thm)],[c_1122,c_1121]) ).
cnf(c_1134,plain,
multiply(A,multiply(multiply(inverse(A),multiply(inverse(B),inverse(C))),C)) = inverse(B),
inference(paramod,[status(thm)],[c_1122,c_1278]) ).
cnf(c_1156,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_733,c_1123]) ).
cnf(c_1279,plain,
multiply(A,inverse(B)) = multiply(multiply(inverse(inverse(A)),multiply(inverse(B),inverse(C))),C),
inference(paramod,[status(thm)],[c_1134,c_1156]) ).
cnf(c_1280,plain,
multiply(A,inverse(B)) = multiply(multiply(A,multiply(inverse(B),inverse(C))),C),
inference(paramod,[status(thm)],[c_733,c_1279]) ).
cnf(c_1217,plain,
multiply(multiply(A,multiply(inverse(B),inverse(C))),C) = multiply(A,inverse(B)),
inference(copy,[status(thm)],[c_1280]) ).
cnf(c_1281,plain,
multiply(A,B) = multiply(multiply(A,inverse(multiply(inverse(C),inverse(B)))),inverse(C)),
inference(paramod,[status(thm)],[c_1104,c_1217]) ).
cnf(c_1282,plain,
multiply(A,B) = multiply(multiply(A,multiply(inverse(inverse(B)),inverse(inverse(C)))),inverse(C)),
inference(paramod,[status(thm)],[c_1122,c_1281]) ).
cnf(c_1283,plain,
multiply(A,B) = multiply(multiply(A,multiply(B,inverse(inverse(C)))),inverse(C)),
inference(paramod,[status(thm)],[c_733,c_1282]) ).
cnf(c_1284,plain,
multiply(A,B) = multiply(multiply(A,multiply(B,C)),inverse(C)),
inference(paramod,[status(thm)],[c_733,c_1283]) ).
cnf(c_1222,plain,
multiply(multiply(A,multiply(B,C)),inverse(C)) = multiply(A,B),
inference(copy,[status(thm)],[c_1284]) ).
cnf(c_1285,plain,
multiply(multiply(A,B),inverse(inverse(C))) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_1222,c_1101]) ).
cnf(c_1242,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_733,c_1285]) ).
cnf(c_1243,plain,
$false,
inference(resolve,[status(thm)],[c_1242,c_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP435-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n019.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Fri Sep 25 14:54:33 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.35 % Process 3033669 was started by sandbox2 on n019,
% 0.07/0.35 % Fri Sep 25 14:54:33 2026
% 0.07/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.07/0.35
% 0.07/0.35 % From the command line: assign(max_seconds, 300).
% 2.36/0.75
% 2.36/0.75 % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 2.36/0.75
% 2.36/0.75 % SZS status Unsatisfiable for theBenchmark
% 2.36/0.75
% 2.36/0.75 % Proof 1 at 0.27 (+ 0.10) seconds.
% 2.36/0.75 % Length of proof is 58.
% 2.36/0.75 % Level of proof is 27.
% 2.36/0.75 % Maximum clause weight is 96.000.
% 2.36/0.75 % Given clauses 68.
% 2.36/0.75
% 2.36/0.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------