%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP436-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 : n016.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.97s 0.83s
% Output : CNFRefutation 2.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 2
% Syntax : Number of formulae : 91 ( 91 unt; 0 def)
% Number of atoms : 91 ( 90 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 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 : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 373 ( 0 sgn 4 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : multiply(VAR_0,inverse(multiply(VAR_1,multiply(VAR_2,multiply(multiply(inverse(VAR_2),inverse(multiply(VAR_3,VAR_1))),VAR_0))))) = VAR_3,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(A,inverse(multiply(B,multiply(C,multiply(multiply(inverse(C),inverse(multiply(D,B))),A))))) = D,
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(B,multiply(multiply(inverse(B),inverse(multiply(C,D))),inverse(E))),multiply(E,multiply(C,A))))) = D,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_5,plain,
multiply(inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),inverse(multiply(C,A))),multiply(inverse(D),inverse(multiply(E,F))))))),inverse(multiply(F,multiply(D,C)))) = E,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_514,plain,
multiply(A,inverse(multiply(multiply(B,multiply(C,inverse(D))),multiply(D,multiply(E,A))))) = multiply(F,multiply(multiply(inverse(F),inverse(multiply(C,E))),inverse(B))),
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_6,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(B,C))),inverse(D))) = multiply(E,inverse(multiply(multiply(D,multiply(B,inverse(F))),multiply(F,multiply(C,E))))),
inference(copy,[status(thm)],[c_514]) ).
cnf(c_7,plain,
multiply(inverse(A),inverse(multiply(B,multiply(C,inverse(multiply(multiply(A,multiply(D,inverse(E))),multiply(E,multiply(B,C)))))))) = D,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_8,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,D))),C))),inverse(B))) = D,
inference(paramod,[status(thm)],[c_6,c_4]) ).
cnf(c_9,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(B,C))),inverse(D))) = multiply(E,multiply(multiply(inverse(E),inverse(multiply(B,C))),inverse(D))),
inference(paramod,[status(thm)],[c_6,c_6]) ).
cnf(c_515,plain,
multiply(A,multiply(multiply(inverse(A),inverse(B)),inverse(C))) = multiply(D,multiply(multiply(inverse(D),inverse(multiply(E,inverse(multiply(F,multiply(V6,multiply(multiply(inverse(V6),inverse(multiply(B,F))),E))))))),inverse(C))),
inference(paramod,[status(thm)],[c_1,c_9]) ).
cnf(c_10,plain,
multiply(A,multiply(multiply(inverse(A),inverse(B)),inverse(C))) = multiply(D,multiply(multiply(inverse(D),inverse(B)),inverse(C))),
inference(paramod,[status(thm)],[c_1,c_515]) ).
cnf(c_516,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(C)),D))),inverse(B))) = multiply(multiply(inverse(D),inverse(multiply(multiply(inverse(E),inverse(multiply(F,C))),F))),inverse(E)),
inference(paramod,[status(thm)],[c_8,c_8]) ).
cnf(c_12,plain,
multiply(multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,D))),C))),inverse(B)) = multiply(E,multiply(multiply(inverse(E),inverse(multiply(multiply(inverse(F),inverse(D)),A))),inverse(F))),
inference(copy,[status(thm)],[c_516]) ).
cnf(c_13,plain,
multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,multiply(A,multiply(D,inverse(B)))))),C))) = D,
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_517,plain,
multiply(inverse(A),inverse(multiply(B,multiply(C,inverse(multiply(D,multiply(E,multiply(B,C)))))))) = multiply(inverse(A),inverse(multiply(multiply(inverse(E),inverse(multiply(F,D))),F))),
inference(paramod,[status(thm)],[c_8,c_7]) ).
cnf(c_14,plain,
multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,D))),C))) = multiply(inverse(A),inverse(multiply(E,multiply(F,inverse(multiply(D,multiply(B,multiply(E,F)))))))),
inference(copy,[status(thm)],[c_517]) ).
cnf(c_16,plain,
multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,D))),C))) = multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(E,D))),E))),
inference(paramod,[status(thm)],[c_8,c_13]) ).
cnf(c_518,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),inverse(multiply(multiply(inverse(C),inverse(D)),A))),inverse(C)))) = multiply(E,inverse(multiply(multiply(F,multiply(multiply(inverse(F),inverse(multiply(V6,D))),inverse(V7))),multiply(V7,multiply(V6,E))))),
inference(paramod,[status(thm)],[c_12,c_6]) ).
cnf(c_17,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),inverse(multiply(multiply(inverse(C),inverse(D)),A))),inverse(C)))) = D,
inference(paramod,[status(thm)],[c_4,c_518]) ).
cnf(c_18,plain,
multiply(multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,multiply(A,D)))),C))),inverse(B)) = D,
inference(paramod,[status(thm)],[c_12,c_8]) ).
cnf(c_28,plain,
multiply(multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,D))),C))),inverse(B)) = inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),inverse(multiply(D,E))),A)))),
inference(paramod,[status(thm)],[c_1,c_18]) ).
cnf(c_519,plain,
multiply(multiply(inverse(A),inverse(multiply(B,C))),inverse(D)) = inverse(multiply(multiply(D,multiply(B,inverse(E))),multiply(E,multiply(C,A)))),
inference(paramod,[status(thm)],[c_7,c_18]) ).
cnf(c_30,plain,
inverse(multiply(multiply(A,multiply(B,inverse(C))),multiply(C,multiply(D,E)))) = multiply(multiply(inverse(E),inverse(multiply(B,D))),inverse(A)),
inference(copy,[status(thm)],[c_519]) ).
cnf(c_520,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),inverse(multiply(multiply(inverse(C),inverse(multiply(D,multiply(E,inverse(multiply(F,multiply(V6,multiply(D,E)))))))),A))),inverse(C)))) = multiply(multiply(inverse(V6),inverse(multiply(V7,F))),V7),
inference(paramod,[status(thm)],[c_14,c_17]) ).
cnf(c_521,plain,
multiply(D,multiply(E,inverse(multiply(F,multiply(V6,multiply(D,E)))))) = multiply(multiply(inverse(V6),inverse(multiply(V7,F))),V7),
inference(paramod,[status(thm)],[c_17,c_520]) ).
cnf(c_42,plain,
multiply(multiply(inverse(A),inverse(multiply(B,C))),B) = multiply(D,multiply(E,inverse(multiply(C,multiply(A,multiply(D,E)))))),
inference(copy,[status(thm)],[c_521]) ).
cnf(c_522,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),inverse(multiply(multiply(inverse(C),inverse(multiply(multiply(inverse(D),inverse(multiply(E,F))),E))),A))),inverse(C)))) = multiply(multiply(inverse(D),inverse(multiply(V6,F))),V6),
inference(paramod,[status(thm)],[c_16,c_17]) ).
cnf(c_44,plain,
multiply(multiply(inverse(A),inverse(multiply(B,C))),B) = multiply(multiply(inverse(A),inverse(multiply(D,C))),D),
inference(paramod,[status(thm)],[c_17,c_522]) ).
cnf(c_49,plain,
multiply(A,inverse(multiply(B,multiply(C,multiply(multiply(inverse(C),inverse(multiply(D,B))),D))))) = A,
inference(paramod,[status(thm)],[c_44,c_1]) ).
cnf(c_51,plain,
multiply(inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),inverse(multiply(C,A))),C)))),inverse(multiply(D,multiply(E,multiply(inverse(E),inverse(multiply(F,D))))))) = F,
inference(paramod,[status(thm)],[c_44,c_5]) ).
cnf(c_523,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(B,C))),B)) = multiply(D,multiply(multiply(inverse(D),inverse(multiply(inverse(E),C))),inverse(E))),
inference(paramod,[status(thm)],[c_44,c_10]) ).
cnf(c_52,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(inverse(B),C))),inverse(B))) = multiply(D,multiply(multiply(inverse(D),inverse(multiply(E,C))),E)),
inference(copy,[status(thm)],[c_523]) ).
cnf(c_524,plain,
multiply(A,multiply(inverse(A),inverse(B))) = multiply(C,multiply(multiply(inverse(C),inverse(multiply(D,multiply(E,multiply(multiply(inverse(E),inverse(multiply(F,D))),F))))),inverse(B))),
inference(paramod,[status(thm)],[c_49,c_10]) ).
cnf(c_63,plain,
multiply(A,multiply(inverse(A),inverse(B))) = multiply(C,multiply(inverse(C),inverse(B))),
inference(paramod,[status(thm)],[c_49,c_524]) ).
cnf(c_525,plain,
multiply(multiply(inverse(A),inverse(B)),B) = multiply(multiply(inverse(A),inverse(multiply(C,inverse(multiply(D,multiply(E,multiply(multiply(inverse(E),inverse(multiply(F,D))),F))))))),C),
inference(paramod,[status(thm)],[c_49,c_44]) ).
cnf(c_71,plain,
multiply(multiply(inverse(A),inverse(B)),B) = multiply(multiply(inverse(A),inverse(C)),C),
inference(paramod,[status(thm)],[c_49,c_525]) ).
cnf(c_526,plain,
multiply(A,inverse(A)) = multiply(B,multiply(inverse(B),inverse(multiply(C,multiply(D,multiply(multiply(inverse(D),inverse(multiply(E,C))),E)))))),
inference(paramod,[status(thm)],[c_49,c_63]) ).
cnf(c_97,plain,
multiply(A,inverse(A)) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_49,c_526]) ).
cnf(c_102,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,inverse(C)))),D))),inverse(B))) = inverse(D),
inference(paramod,[status(thm)],[c_97,c_8]) ).
cnf(c_123,plain,
multiply(multiply(inverse(A),inverse(multiply(B,inverse(B)))),C) = multiply(D,multiply(E,inverse(multiply(inverse(C),multiply(A,multiply(D,E)))))),
inference(paramod,[status(thm)],[c_97,c_42]) ).
cnf(c_527,plain,
multiply(multiply(A,inverse(A)),inverse(B)) = multiply(multiply(inverse(B),inverse(C)),C),
inference(paramod,[status(thm)],[c_97,c_71]) ).
cnf(c_155,plain,
multiply(multiply(inverse(A),inverse(B)),B) = multiply(multiply(C,inverse(C)),inverse(A)),
inference(copy,[status(thm)],[c_527]) ).
cnf(c_208,plain,
multiply(multiply(inverse(multiply(A,inverse(A))),inverse(B)),B) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_155,c_97]) ).
cnf(c_209,plain,
multiply(multiply(A,inverse(A)),inverse(B)) = multiply(multiply(C,inverse(C)),inverse(B)),
inference(paramod,[status(thm)],[c_97,c_155]) ).
cnf(c_223,plain,
multiply(multiply(inverse(A),inverse(multiply(multiply(B,inverse(B)),inverse(C)))),multiply(D,inverse(D))) = multiply(E,multiply(F,inverse(multiply(inverse(C),multiply(A,multiply(E,F)))))),
inference(paramod,[status(thm)],[c_209,c_42]) ).
cnf(c_225,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_209,c_97]) ).
cnf(c_528,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,inverse(C)))),multiply(D,inverse(D))))),inverse(B))) = inverse(multiply(E,inverse(E))),
inference(paramod,[status(thm)],[c_225,c_8]) ).
cnf(c_233,plain,
inverse(multiply(A,inverse(A))) = inverse(multiply(B,inverse(B))),
inference(paramod,[status(thm)],[c_102,c_528]) ).
cnf(c_245,plain,
inverse(multiply(multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(C,inverse(C))))),multiply(D,multiply(E,F)))) = multiply(multiply(inverse(F),inverse(multiply(D,E))),inverse(A)),
inference(paramod,[status(thm)],[c_225,c_30]) ).
cnf(c_254,plain,
multiply(A,inverse(multiply(inverse(multiply(B,inverse(B))),multiply(C,multiply(multiply(inverse(C),inverse(multiply(D,inverse(D)))),multiply(E,inverse(E))))))) = A,
inference(paramod,[status(thm)],[c_225,c_49]) ).
cnf(c_291,plain,
multiply(multiply(inverse(multiply(A,inverse(A))),inverse(B)),B) = multiply(multiply(inverse(multiply(C,inverse(C))),inverse(D)),D),
inference(paramod,[status(thm)],[c_233,c_71]) ).
cnf(c_293,plain,
multiply(multiply(inverse(A),inverse(multiply(B,inverse(B)))),multiply(C,inverse(C))) = multiply(multiply(D,inverse(D)),inverse(A)),
inference(paramod,[status(thm)],[c_233,c_155]) ).
cnf(c_529,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,inverse(C)))),multiply(inverse(multiply(D,inverse(D))),inverse(E))))),inverse(B))) = E,
inference(paramod,[status(thm)],[c_208,c_8]) ).
cnf(c_304,plain,
inverse(multiply(inverse(multiply(A,inverse(A))),inverse(B))) = B,
inference(paramod,[status(thm)],[c_102,c_529]) ).
cnf(c_530,plain,
multiply(multiply(inverse(multiply(inverse(multiply(A,inverse(A))),inverse(B))),inverse(multiply(multiply(inverse(C),inverse(multiply(D,multiply(E,inverse(E))))),D))),inverse(C)) = B,
inference(paramod,[status(thm)],[c_208,c_18]) ).
cnf(c_320,plain,
multiply(multiply(A,inverse(multiply(multiply(inverse(B),inverse(multiply(C,multiply(D,inverse(D))))),C))),inverse(B)) = A,
inference(paramod,[status(thm)],[c_304,c_530]) ).
cnf(c_327,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),inverse(multiply(C,inverse(C)))),inverse(multiply(D,inverse(D)))))) = A,
inference(paramod,[status(thm)],[c_208,c_17]) ).
cnf(c_531,plain,
inverse(A) = multiply(B,multiply(C,multiply(multiply(inverse(C),inverse(multiply(A,B))),inverse(multiply(D,inverse(D)))))),
inference(paramod,[status(thm)],[c_1,c_304]) ).
cnf(c_348,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),inverse(multiply(C,A))),inverse(multiply(D,inverse(D)))))) = inverse(C),
inference(copy,[status(thm)],[c_531]) ).
cnf(c_354,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(multiply(inverse(B),C),inverse(multiply(D,inverse(D)))))),inverse(B))) = inverse(C),
inference(paramod,[status(thm)],[c_304,c_8]) ).
cnf(c_532,plain,
multiply(multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(multiply(C,multiply(D,inverse(D))))),C))),inverse(B)) = inverse(multiply(inverse(multiply(E,inverse(E))),multiply(F,multiply(multiply(inverse(F),inverse(multiply(V6,inverse(V6)))),A)))),
inference(paramod,[status(thm)],[c_225,c_28]) ).
cnf(c_533,plain,
inverse(A) = inverse(multiply(inverse(multiply(E,inverse(E))),multiply(F,multiply(multiply(inverse(F),inverse(multiply(V6,inverse(V6)))),A)))),
inference(paramod,[status(thm)],[c_320,c_532]) ).
cnf(c_407,plain,
inverse(multiply(inverse(multiply(A,inverse(A))),multiply(B,multiply(multiply(inverse(B),inverse(multiply(C,inverse(C)))),D)))) = inverse(D),
inference(copy,[status(thm)],[c_533]) ).
cnf(c_411,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_407,c_254]) ).
cnf(c_420,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(inverse(B),C))),inverse(B))) = inverse(C),
inference(paramod,[status(thm)],[c_411,c_354]) ).
cnf(c_421,plain,
multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(C,A))))) = inverse(C),
inference(paramod,[status(thm)],[c_411,c_348]) ).
cnf(c_534,plain,
multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(D,inverse(D)))))) = A,
inference(paramod,[status(thm)],[c_411,c_327]) ).
cnf(c_428,plain,
multiply(A,multiply(B,inverse(B))) = A,
inference(paramod,[status(thm)],[c_411,c_534]) ).
cnf(c_535,plain,
multiply(inverse(A),multiply(C,inverse(C))) = multiply(multiply(D,inverse(D)),inverse(A)),
inference(paramod,[status(thm)],[c_411,c_293]) ).
cnf(c_536,plain,
inverse(A) = multiply(multiply(D,inverse(D)),inverse(A)),
inference(paramod,[status(thm)],[c_428,c_535]) ).
cnf(c_438,plain,
multiply(multiply(A,inverse(A)),inverse(B)) = inverse(B),
inference(copy,[status(thm)],[c_536]) ).
cnf(c_537,plain,
inverse(multiply(multiply(A,multiply(B,inverse(B))),multiply(D,multiply(E,F)))) = multiply(multiply(inverse(F),inverse(multiply(D,E))),inverse(A)),
inference(paramod,[status(thm)],[c_411,c_245]) ).
cnf(c_447,plain,
inverse(multiply(A,multiply(B,multiply(C,D)))) = multiply(multiply(inverse(D),inverse(multiply(B,C))),inverse(A)),
inference(paramod,[status(thm)],[c_428,c_537]) ).
cnf(c_538,plain,
multiply(inverse(A),C) = multiply(D,multiply(E,inverse(multiply(inverse(C),multiply(A,multiply(D,E)))))),
inference(paramod,[status(thm)],[c_411,c_123]) ).
cnf(c_539,plain,
multiply(inverse(A),C) = multiply(D,multiply(E,multiply(multiply(inverse(E),inverse(multiply(A,D))),inverse(inverse(C))))),
inference(paramod,[status(thm)],[c_447,c_538]) ).
cnf(c_452,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),inverse(multiply(C,A))),inverse(inverse(D))))) = multiply(inverse(C),D),
inference(copy,[status(thm)],[c_539]) ).
cnf(c_540,plain,
multiply(multiply(inverse(A),inverse(inverse(C))),multiply(D,inverse(D))) = multiply(E,multiply(F,inverse(multiply(inverse(C),multiply(A,multiply(E,F)))))),
inference(paramod,[status(thm)],[c_438,c_223]) ).
cnf(c_541,plain,
multiply(inverse(A),inverse(inverse(C))) = multiply(E,multiply(F,inverse(multiply(inverse(C),multiply(A,multiply(E,F)))))),
inference(paramod,[status(thm)],[c_428,c_540]) ).
cnf(c_542,plain,
multiply(inverse(A),inverse(inverse(C))) = multiply(E,multiply(F,multiply(multiply(inverse(F),inverse(multiply(A,E))),inverse(inverse(C))))),
inference(paramod,[status(thm)],[c_447,c_541]) ).
cnf(c_456,plain,
multiply(inverse(A),inverse(inverse(B))) = multiply(inverse(A),B),
inference(paramod,[status(thm)],[c_452,c_542]) ).
cnf(c_543,plain,
inverse(C) = multiply(D,multiply(multiply(inverse(D),inverse(multiply(E,C))),E)),
inference(paramod,[status(thm)],[c_420,c_52]) ).
cnf(c_458,plain,
multiply(A,multiply(multiply(inverse(A),inverse(multiply(B,C))),B)) = inverse(C),
inference(copy,[status(thm)],[c_543]) ).
cnf(c_544,plain,
multiply(inverse(multiply(A,inverse(A))),inverse(multiply(D,multiply(E,multiply(inverse(E),inverse(multiply(F,D))))))) = F,
inference(paramod,[status(thm)],[c_458,c_51]) ).
cnf(c_545,plain,
multiply(inverse(multiply(A,inverse(A))),inverse(inverse(F))) = F,
inference(paramod,[status(thm)],[c_421,c_544]) ).
cnf(c_459,plain,
multiply(inverse(multiply(A,inverse(A))),B) = B,
inference(paramod,[status(thm)],[c_456,c_545]) ).
cnf(c_546,plain,
multiply(inverse(B),B) = multiply(multiply(inverse(multiply(C,inverse(C))),inverse(D)),D),
inference(paramod,[status(thm)],[c_459,c_291]) ).
cnf(c_512,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_459,c_546]) ).
cnf(c_513,plain,
$false,
inference(resolve,[status(thm)],[c_512,c_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP436-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n016.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Fri Sep 25 14:59:13 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.44 % Process 2678556 was started by sandbox2 on n016,
% 0.17/0.44 % Fri Sep 25 14:59:13 2026
% 0.17/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.45
% 0.17/0.45 % From the command line: assign(max_seconds, 300).
% 2.97/0.83
% 2.97/0.83 % SZS status Unsatisfiable for theBenchmark
% 2.97/0.83
% 2.97/0.83 % Proof 1 at 0.28 (+ 0.09) seconds.
% 2.97/0.83 % Length of proof is 56.
% 2.97/0.83 % Level of proof is 22.
% 2.97/0.83 % Maximum clause weight is 100.000.
% 2.97/0.83 % Given clauses 39.
% 2.97/0.83
% 2.97/0.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------