%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP062-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 : n006.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 7.01s 1.34s
% Output : CNFRefutation 7.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 2
% Syntax : Number of formulae : 139 ( 134 unt; 0 def)
% Number of atoms : 147 ( 146 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 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 : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 533 ( 0 sgn 4 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : inverse(multiply(VAR_0,multiply(VAR_1,multiply(multiply(VAR_2,inverse(VAR_2)),inverse(multiply(VAR_3,multiply(VAR_0,VAR_1))))))) = VAR_3,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B))))))) = D,
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(A,multiply(multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(D,A)))),multiply(multiply(E,inverse(E)),C)))) = D,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_5,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,multiply(C,D)))),multiply(multiply(multiply(E,inverse(E)),B),multiply(multiply(F,inverse(F)),C)))) = D,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_2850,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),B),multiply(multiply(multiply(C,inverse(C)),D),multiply(multiply(E,inverse(E)),F)))) = multiply(multiply(V6,inverse(V6)),inverse(multiply(B,multiply(D,F)))),
inference(paramod,[status(thm)],[c_4,c_4]) ).
cnf(c_6,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,multiply(C,D)))) = inverse(multiply(multiply(multiply(E,inverse(E)),B),multiply(multiply(multiply(F,inverse(F)),C),multiply(multiply(V6,inverse(V6)),D)))),
inference(copy,[status(thm)],[c_2850]) ).
cnf(c_7,plain,
inverse(multiply(A,multiply(B,inverse(multiply(multiply(multiply(C,inverse(C)),D),multiply(multiply(multiply(E,inverse(E)),A),multiply(multiply(F,inverse(F)),B))))))) = D,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_8,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,multiply(C,inverse(multiply(D,multiply(multiply(multiply(E,inverse(E)),B),multiply(multiply(F,inverse(F)),C)))))))) = D,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_10,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,multiply(C,D))),multiply(B,C)))) = D,
inference(paramod,[status(thm)],[c_6,c_5]) ).
cnf(c_11,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,multiply(C,D)))) = multiply(multiply(E,inverse(E)),inverse(multiply(B,multiply(C,D)))),
inference(paramod,[status(thm)],[c_6,c_6]) ).
cnf(c_2851,plain,
multiply(multiply(A,inverse(A)),B) = multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(E,multiply(multiply(F,inverse(F)),inverse(multiply(B,multiply(D,E)))))))),
inference(paramod,[status(thm)],[c_1,c_11]) ).
cnf(c_13,plain,
multiply(multiply(A,inverse(A)),B) = multiply(multiply(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_1,c_2851]) ).
cnf(c_2852,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(multiply(multiply(D,inverse(D)),inverse(multiply(E,multiply(multiply(F,inverse(F)),inverse(multiply(A,multiply(B,C))))))),multiply(multiply(V6,inverse(V6)),E)))) = multiply(V7,inverse(V7)),
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_14,plain,
multiply(A,inverse(A)) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_4,c_2852]) ).
cnf(c_16,plain,
inverse(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(D,inverse(D)))))))) = C,
inference(paramod,[status(thm)],[c_14,c_1]) ).
cnf(c_17,plain,
multiply(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B)))))),D) = multiply(E,inverse(E)),
inference(paramod,[status(thm)],[c_1,c_14]) ).
cnf(c_18,plain,
inverse(multiply(inverse(A),multiply(multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(D,inverse(D))))),multiply(multiply(E,inverse(E)),C)))) = A,
inference(paramod,[status(thm)],[c_14,c_4]) ).
cnf(c_21,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,multiply(C,inverse(C))))),multiply(multiply(multiply(D,inverse(D)),B),multiply(multiply(E,inverse(E)),F)))) = inverse(F),
inference(paramod,[status(thm)],[c_14,c_5]) ).
cnf(c_49,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_13,c_14]) ).
cnf(c_2853,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,multiply(C,inverse(C))))),multiply(multiply(multiply(D,inverse(D)),B),multiply(multiply(E,inverse(E)),multiply(F,inverse(F)))))) = inverse(multiply(V6,inverse(V6))),
inference(paramod,[status(thm)],[c_49,c_5]) ).
cnf(c_61,plain,
inverse(multiply(A,inverse(A))) = inverse(multiply(B,inverse(B))),
inference(paramod,[status(thm)],[c_21,c_2853]) ).
cnf(c_171,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,multiply(C,inverse(C)))),multiply(B,D)))) = inverse(D),
inference(paramod,[status(thm)],[c_14,c_10]) ).
cnf(c_904,plain,
multiply(multiply(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(D,inverse(D))))))),C),inverse(multiply(inverse(multiply(E,multiply(F,V6))),multiply(E,F)))) = V6,
inference(paramod,[status(thm)],[c_16,c_10]) ).
cnf(c_906,plain,
inverse(multiply(A,multiply(inverse(A),B))) = inverse(multiply(C,multiply(inverse(C),B))),
inference(paramod,[status(thm)],[c_10,c_16]) ).
cnf(c_910,plain,
inverse(multiply(A,multiply(inverse(A),inverse(inverse(B))))) = inverse(multiply(B,multiply(C,inverse(C)))),
inference(paramod,[status(thm)],[c_171,c_16]) ).
cnf(c_935,plain,
multiply(multiply(A,multiply(inverse(A),B)),inverse(multiply(C,multiply(inverse(C),B)))) = multiply(D,inverse(D)),
inference(paramod,[status(thm)],[c_906,c_14]) ).
cnf(c_1090,plain,
multiply(multiply(multiply(A,multiply(inverse(A),inverse(inverse(B)))),inverse(multiply(B,multiply(C,inverse(C))))),inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,E)))) = F,
inference(paramod,[status(thm)],[c_910,c_10]) ).
cnf(c_2854,plain,
inverse(multiply(inverse(multiply(A,multiply(inverse(A),B))),multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(E,inverse(E))))),multiply(multiply(F,inverse(F)),D)))) = multiply(V6,multiply(inverse(V6),B)),
inference(paramod,[status(thm)],[c_935,c_4]) ).
cnf(c_1216,plain,
multiply(A,multiply(inverse(A),B)) = multiply(C,multiply(inverse(C),B)),
inference(paramod,[status(thm)],[c_18,c_2854]) ).
cnf(c_2855,plain,
multiply(A,multiply(B,inverse(B))) = multiply(C,multiply(inverse(C),inverse(inverse(A)))),
inference(paramod,[status(thm)],[c_14,c_1216]) ).
cnf(c_1294,plain,
multiply(A,multiply(inverse(A),inverse(inverse(B)))) = multiply(B,multiply(C,inverse(C))),
inference(copy,[status(thm)],[c_2855]) ).
cnf(c_2856,plain,
multiply(A,multiply(inverse(A),inverse(inverse(B)))) = multiply(B,multiply(multiply(C,multiply(inverse(C),multiply(multiply(D,inverse(D)),inverse(multiply(E,multiply(F,inverse(F))))))),E)),
inference(paramod,[status(thm)],[c_16,c_1294]) ).
cnf(c_1385,plain,
multiply(A,multiply(multiply(B,multiply(inverse(B),multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(E,inverse(E))))))),D)) = multiply(F,multiply(inverse(F),inverse(inverse(A)))),
inference(copy,[status(thm)],[c_2856]) ).
cnf(c_2857,plain,
multiply(A,multiply(inverse(A),inverse(inverse(multiply(B,multiply(C,multiply(multiply(D,inverse(D)),inverse(multiply(multiply(E,inverse(E)),multiply(B,C)))))))))) = multiply(F,inverse(F)),
inference(paramod,[status(thm)],[c_17,c_1294]) ).
cnf(c_1489,plain,
multiply(A,multiply(inverse(A),inverse(multiply(B,inverse(B))))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_1,c_2857]) ).
cnf(c_1494,plain,
inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(B))),multiply(multiply(C,inverse(C)),inverse(multiply(D,inverse(D))))))) = A,
inference(paramod,[status(thm)],[c_1489,c_1]) ).
cnf(c_1501,plain,
inverse(multiply(inverse(multiply(A,inverse(A))),multiply(multiply(multiply(B,inverse(B)),inverse(multiply(C,inverse(C)))),multiply(multiply(D,inverse(D)),E)))) = inverse(E),
inference(paramod,[status(thm)],[c_1489,c_4]) ).
cnf(c_2858,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,multiply(C,inverse(C))))),multiply(multiply(multiply(D,inverse(D)),B),multiply(multiply(E,inverse(E)),F)))) = multiply(inverse(F),inverse(multiply(V6,inverse(V6)))),
inference(paramod,[status(thm)],[c_1489,c_5]) ).
cnf(c_2859,plain,
inverse(F) = multiply(inverse(F),inverse(multiply(V6,inverse(V6)))),
inference(paramod,[status(thm)],[c_21,c_2858]) ).
cnf(c_1508,plain,
multiply(inverse(A),inverse(multiply(B,inverse(B)))) = inverse(A),
inference(copy,[status(thm)],[c_2859]) ).
cnf(c_2860,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = inverse(multiply(C,multiply(D,multiply(multiply(E,inverse(E)),inverse(multiply(A,multiply(C,D))))))),
inference(paramod,[status(thm)],[c_1,c_1508]) ).
cnf(c_1533,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_1,c_2860]) ).
cnf(c_1559,plain,
inverse(multiply(inverse(multiply(A,inverse(A))),multiply(multiply(B,inverse(B)),multiply(multiply(C,inverse(C)),D)))) = inverse(D),
inference(paramod,[status(thm)],[c_1533,c_1501]) ).
cnf(c_1560,plain,
inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C))))) = A,
inference(paramod,[status(thm)],[c_1533,c_1494]) ).
cnf(c_1571,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,C)),multiply(B,C)))) = inverse(multiply(D,inverse(D))),
inference(paramod,[status(thm)],[c_1533,c_10]) ).
cnf(c_2861,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(B),multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(E,inverse(multiply(B,multiply(multiply(multiply(F,inverse(F)),D),multiply(multiply(V6,inverse(V6)),E))))))))))) = inverse(multiply(V7,inverse(V7))),
inference(paramod,[status(thm)],[c_8,c_1571]) ).
cnf(c_1605,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(B),B))) = inverse(multiply(C,inverse(C))),
inference(paramod,[status(thm)],[c_8,c_2861]) ).
cnf(c_1754,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(multiply(multiply(B,inverse(B)),inverse(multiply(inverse(C),C))),multiply(multiply(D,inverse(D)),inverse(multiply(E,multiply(F,inverse(F)))))))) = E,
inference(paramod,[status(thm)],[c_1605,c_16]) ).
cnf(c_1781,plain,
multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(inverse(C),C)))) = A,
inference(paramod,[status(thm)],[c_1605,c_1533]) ).
cnf(c_1783,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(B),B))) = multiply(multiply(C,inverse(C)),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_1605,c_1605]) ).
cnf(c_1808,plain,
multiply(A,multiply(multiply(multiply(B,multiply(inverse(B),multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(E,inverse(E))))))),D),inverse(multiply(inverse(F),F)))) = A,
inference(paramod,[status(thm)],[c_16,c_1781]) ).
cnf(c_1817,plain,
multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(multiply(multiply(C,inverse(C)),inverse(multiply(inverse(D),D))),multiply(E,inverse(E)))))) = A,
inference(paramod,[status(thm)],[c_1605,c_1781]) ).
cnf(c_1821,plain,
multiply(multiply(A,inverse(A)),multiply(multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(D,inverse(D))))),multiply(multiply(multiply(E,inverse(E)),C),F))) = F,
inference(paramod,[status(thm)],[c_18,c_10]) ).
cnf(c_1833,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(E,inverse(E))))),multiply(multiply(F,inverse(F)),D))),B))) = A,
inference(paramod,[status(thm)],[c_18,c_1533]) ).
cnf(c_1836,plain,
multiply(A,multiply(multiply(B,inverse(B)),multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(E,inverse(E))))),multiply(multiply(F,inverse(F)),D)))) = A,
inference(paramod,[status(thm)],[c_18,c_1781]) ).
cnf(c_2862,plain,
inverse(multiply(A,multiply(B,inverse(multiply(multiply(multiply(C,inverse(C)),inverse(multiply(inverse(D),D))),multiply(multiply(multiply(E,inverse(E)),A),multiply(multiply(F,inverse(F)),B))))))) = inverse(multiply(inverse(V6),V6)),
inference(paramod,[status(thm)],[c_1783,c_7]) ).
cnf(c_1842,plain,
inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(B),B)),
inference(paramod,[status(thm)],[c_7,c_2862]) ).
cnf(c_2863,plain,
inverse(multiply(inverse(multiply(inverse(A),A)),multiply(multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(D,inverse(D))))),multiply(multiply(E,inverse(E)),C)))) = multiply(inverse(F),F),
inference(paramod,[status(thm)],[c_1842,c_18]) ).
cnf(c_1942,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_18,c_2863]) ).
cnf(c_1951,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2 ),
inference(resolve,[status(thm)],[c_1942,c_3]) ).
cnf(c_1961,plain,
multiply(inverse(multiply(A,inverse(A))),multiply(B,inverse(B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_61,c_1942]) ).
cnf(c_1983,plain,
multiply(A,multiply(inverse(B),B)) = multiply(C,multiply(inverse(C),A)),
inference(paramod,[status(thm)],[c_1942,c_1216]) ).
cnf(c_2027,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,multiply(C,multiply(inverse(D),D)))),multiply(B,E)))) = multiply(inverse(E),C),
inference(paramod,[status(thm)],[c_1983,c_10]) ).
cnf(c_2028,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,multiply(inverse(C),C))),multiply(D,inverse(D))))) = B,
inference(paramod,[status(thm)],[c_1983,c_10]) ).
cnf(c_2864,plain,
inverse(multiply(inverse(multiply(A,inverse(A))),multiply(multiply(B,inverse(B)),multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(inverse(E),E))))))) = D,
inference(paramod,[status(thm)],[c_1961,c_1]) ).
cnf(c_2481,plain,
inverse(inverse(multiply(A,multiply(inverse(B),B)))) = A,
inference(paramod,[status(thm)],[c_1559,c_2864]) ).
cnf(c_2487,plain,
inverse(multiply(A,multiply(multiply(multiply(B,inverse(B)),inverse(multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D))))),multiply(multiply(E,inverse(E)),inverse(multiply(F,A)))))) = F,
inference(paramod,[status(thm)],[c_1961,c_4]) ).
cnf(c_2493,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C))))),multiply(multiply(multiply(D,inverse(D)),inverse(multiply(E,F))),multiply(multiply(V6,inverse(V6)),E)))) = F,
inference(paramod,[status(thm)],[c_1961,c_5]) ).
cnf(c_2865,plain,
inverse(multiply(inverse(inverse(A)),multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C))))) = inverse(multiply(A,multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_1961,c_910]) ).
cnf(c_2866,plain,
inverse(A) = inverse(multiply(A,multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_1560,c_2865]) ).
cnf(c_2535,plain,
inverse(multiply(A,multiply(B,inverse(B)))) = inverse(A),
inference(copy,[status(thm)],[c_2866]) ).
cnf(c_2593,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),inverse(inverse(multiply(B,inverse(B))))),multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,E))),multiply(multiply(F,inverse(F)),D)))) = E,
inference(paramod,[status(thm)],[c_2535,c_2493]) ).
cnf(c_2594,plain,
inverse(multiply(A,multiply(multiply(multiply(B,inverse(B)),inverse(inverse(multiply(C,inverse(C))))),multiply(multiply(D,inverse(D)),inverse(multiply(E,A)))))) = E,
inference(paramod,[status(thm)],[c_2535,c_2487]) ).
cnf(c_2867,plain,
multiply(multiply(A,inverse(A)),inverse(inverse(multiply(B,multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_2535,c_2028]) ).
cnf(c_2688,plain,
multiply(multiply(A,inverse(A)),B) = B,
inference(paramod,[status(thm)],[c_2481,c_2867]) ).
cnf(c_2868,plain,
multiply(A,multiply(multiply(B,inverse(B)),multiply(multiply(multiply(C,inverse(C)),inverse(D)),multiply(multiply(F,inverse(F)),D)))) = A,
inference(paramod,[status(thm)],[c_2535,c_1836]) ).
cnf(c_2869,plain,
multiply(A,multiply(multiply(B,inverse(B)),multiply(inverse(D),multiply(multiply(F,inverse(F)),D)))) = A,
inference(paramod,[status(thm)],[c_2688,c_2868]) ).
cnf(c_2870,plain,
multiply(A,multiply(multiply(B,inverse(B)),multiply(inverse(D),D))) = A,
inference(paramod,[status(thm)],[c_2688,c_2869]) ).
cnf(c_2716,plain,
multiply(A,multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_2688,c_2870]) ).
cnf(c_2871,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(multiply(multiply(C,inverse(C)),inverse(D)),multiply(multiply(F,inverse(F)),D))),B))) = A,
inference(paramod,[status(thm)],[c_2535,c_1833]) ).
cnf(c_2872,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(inverse(D),multiply(multiply(F,inverse(F)),D))),B))) = A,
inference(paramod,[status(thm)],[c_2688,c_2871]) ).
cnf(c_2873,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(inverse(D),D)),B))) = A,
inference(paramod,[status(thm)],[c_2688,c_2872]) ).
cnf(c_2718,plain,
multiply(A,inverse(multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_2716,c_2873]) ).
cnf(c_2874,plain,
multiply(multiply(A,inverse(A)),multiply(multiply(multiply(B,inverse(B)),inverse(C)),multiply(multiply(multiply(E,inverse(E)),C),F))) = F,
inference(paramod,[status(thm)],[c_2535,c_1821]) ).
cnf(c_2875,plain,
multiply(multiply(A,inverse(A)),multiply(inverse(C),multiply(multiply(multiply(E,inverse(E)),C),F))) = F,
inference(paramod,[status(thm)],[c_2688,c_2874]) ).
cnf(c_2876,plain,
multiply(multiply(A,inverse(A)),multiply(inverse(C),multiply(C,F))) = F,
inference(paramod,[status(thm)],[c_2688,c_2875]) ).
cnf(c_2730,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(paramod,[status(thm)],[c_2688,c_2876]) ).
cnf(c_2877,plain,
multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(multiply(C,inverse(C)),multiply(E,inverse(E)))))) = A,
inference(paramod,[status(thm)],[c_2718,c_1817]) ).
cnf(c_2878,plain,
multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(E,inverse(E))))) = A,
inference(paramod,[status(thm)],[c_2688,c_2877]) ).
cnf(c_2733,plain,
multiply(A,multiply(B,inverse(B))) = A,
inference(paramod,[status(thm)],[c_1533,c_2878]) ).
cnf(c_2879,plain,
multiply(A,multiply(multiply(multiply(B,multiply(inverse(B),multiply(multiply(C,inverse(C)),inverse(D)))),D),inverse(multiply(inverse(F),F)))) = A,
inference(paramod,[status(thm)],[c_2733,c_1808]) ).
cnf(c_2880,plain,
multiply(A,multiply(multiply(multiply(B,multiply(inverse(B),inverse(D))),D),inverse(multiply(inverse(F),F)))) = A,
inference(paramod,[status(thm)],[c_2688,c_2879]) ).
cnf(c_2735,plain,
multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(C))),C)) = A,
inference(paramod,[status(thm)],[c_2718,c_2880]) ).
cnf(c_2881,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(multiply(B,inverse(B)),multiply(multiply(D,inverse(D)),inverse(multiply(E,multiply(F,inverse(F)))))))) = E,
inference(paramod,[status(thm)],[c_2718,c_1754]) ).
cnf(c_2882,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(multiply(B,inverse(B)),multiply(multiply(D,inverse(D)),inverse(E))))) = E,
inference(paramod,[status(thm)],[c_2733,c_2881]) ).
cnf(c_2883,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(multiply(B,inverse(B)),inverse(E)))) = E,
inference(paramod,[status(thm)],[c_2688,c_2882]) ).
cnf(c_2884,plain,
inverse(multiply(multiply(A,inverse(A)),inverse(E))) = E,
inference(paramod,[status(thm)],[c_2688,c_2883]) ).
cnf(c_2742,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_2688,c_2884]) ).
cnf(c_2885,plain,
multiply(A,multiply(multiply(B,multiply(inverse(B),multiply(multiply(C,inverse(C)),inverse(D)))),D)) = multiply(F,multiply(inverse(F),inverse(inverse(A)))),
inference(paramod,[status(thm)],[c_2733,c_1385]) ).
cnf(c_2886,plain,
multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(D))),D)) = multiply(F,multiply(inverse(F),inverse(inverse(A)))),
inference(paramod,[status(thm)],[c_2688,c_2885]) ).
cnf(c_2887,plain,
A = multiply(F,multiply(inverse(F),inverse(inverse(A)))),
inference(paramod,[status(thm)],[c_2735,c_2886]) ).
cnf(c_2888,plain,
A = multiply(F,multiply(inverse(F),A)),
inference(paramod,[status(thm)],[c_2742,c_2887]) ).
cnf(c_2761,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(copy,[status(thm)],[c_2888]) ).
cnf(c_2889,plain,
multiply(multiply(multiply(A,multiply(inverse(A),B)),inverse(multiply(B,multiply(C,inverse(C))))),inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,E)))) = F,
inference(paramod,[status(thm)],[c_2742,c_1090]) ).
cnf(c_2890,plain,
multiply(multiply(B,inverse(multiply(B,multiply(C,inverse(C))))),inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,E)))) = F,
inference(paramod,[status(thm)],[c_2761,c_2889]) ).
cnf(c_2891,plain,
multiply(multiply(B,inverse(B)),inverse(multiply(inverse(multiply(D,multiply(E,F))),multiply(D,E)))) = F,
inference(paramod,[status(thm)],[c_2733,c_2890]) ).
cnf(c_2763,plain,
inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,B))) = C,
inference(paramod,[status(thm)],[c_2688,c_2891]) ).
cnf(c_2892,plain,
multiply(multiply(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),inverse(C)))),C),inverse(multiply(inverse(multiply(E,multiply(F,V6))),multiply(E,F)))) = V6,
inference(paramod,[status(thm)],[c_2733,c_904]) ).
cnf(c_2893,plain,
multiply(multiply(multiply(A,multiply(inverse(A),inverse(C))),C),inverse(multiply(inverse(multiply(E,multiply(F,V6))),multiply(E,F)))) = V6,
inference(paramod,[status(thm)],[c_2688,c_2892]) ).
cnf(c_2894,plain,
multiply(multiply(inverse(C),C),inverse(multiply(inverse(multiply(E,multiply(F,V6))),multiply(E,F)))) = V6,
inference(paramod,[status(thm)],[c_2761,c_2893]) ).
cnf(c_2768,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_2763,c_2894]) ).
cnf(c_2895,plain,
inverse(multiply(A,multiply(multiply(multiply(B,inverse(B)),multiply(C,inverse(C))),multiply(multiply(D,inverse(D)),inverse(multiply(E,A)))))) = E,
inference(paramod,[status(thm)],[c_2742,c_2594]) ).
cnf(c_2896,plain,
inverse(multiply(A,multiply(multiply(B,inverse(B)),multiply(multiply(D,inverse(D)),inverse(multiply(E,A)))))) = E,
inference(paramod,[status(thm)],[c_2733,c_2895]) ).
cnf(c_2897,plain,
inverse(multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(E,A))))) = E,
inference(paramod,[status(thm)],[c_2688,c_2896]) ).
cnf(c_2777,plain,
inverse(multiply(A,inverse(multiply(B,A)))) = B,
inference(paramod,[status(thm)],[c_2688,c_2897]) ).
cnf(c_2898,plain,
inverse(multiply(multiply(multiply(A,inverse(A)),multiply(B,inverse(B))),multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,E))),multiply(multiply(F,inverse(F)),D)))) = E,
inference(paramod,[status(thm)],[c_2742,c_2593]) ).
cnf(c_2899,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,E))),multiply(multiply(F,inverse(F)),D)))) = E,
inference(paramod,[status(thm)],[c_2733,c_2898]) ).
cnf(c_2900,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(inverse(multiply(D,E)),multiply(multiply(F,inverse(F)),D)))) = E,
inference(paramod,[status(thm)],[c_2688,c_2899]) ).
cnf(c_2901,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(inverse(multiply(D,E)),D))) = E,
inference(paramod,[status(thm)],[c_2688,c_2900]) ).
cnf(c_2778,plain,
inverse(multiply(inverse(multiply(A,B)),A)) = B,
inference(paramod,[status(thm)],[c_2688,c_2901]) ).
cnf(c_2902,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,C)),multiply(B,E)))) = multiply(inverse(E),C),
inference(paramod,[status(thm)],[c_2716,c_2027]) ).
cnf(c_2809,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = multiply(inverse(C),B),
inference(paramod,[status(thm)],[c_2688,c_2902]) ).
cnf(c_2903,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_2768,c_1951]) ).
cnf(c_2813,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(copy,[status(thm)],[c_2903]) ).
cnf(c_2904,plain,
inverse(A) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_2777,c_2742]) ).
cnf(c_2815,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_2904]) ).
cnf(c_2823,plain,
inverse(multiply(inverse(A),B)) = multiply(inverse(B),A),
inference(paramod,[status(thm)],[c_2761,c_2778]) ).
cnf(c_2824,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_2823,c_2809]) ).
cnf(c_2905,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_2815,c_2730]) ).
cnf(c_2826,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_2905]) ).
cnf(c_2829,plain,
multiply(multiply(inverse(A),inverse(B)),multiply(B,C)) = multiply(inverse(A),C),
inference(paramod,[status(thm)],[c_2826,c_2824]) ).
cnf(c_2906,plain,
multiply(multiply(A,inverse(B)),multiply(B,C)) = multiply(inverse(inverse(A)),C),
inference(paramod,[status(thm)],[c_2742,c_2829]) ).
cnf(c_2842,plain,
multiply(multiply(A,inverse(B)),multiply(B,C)) = multiply(A,C),
inference(paramod,[status(thm)],[c_2742,c_2906]) ).
cnf(c_2907,plain,
multiply(multiply(A,inverse(inverse(B))),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_2730,c_2842]) ).
cnf(c_2848,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_2742,c_2907]) ).
cnf(c_2849,plain,
$false,
inference(resolve,[status(thm)],[c_2848,c_2813]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP062-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 14:20:10 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 3089502 was started by sandbox on n006,
% 0.08/0.35 % Fri Sep 25 14:20:10 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.36
% 0.08/0.36 % From the command line: assign(max_seconds, 300).
% 7.01/1.34
% 7.01/1.34 % Assigning unary symbol inverse kb_weight 0 and highest precedence (10).
% 7.01/1.34
% 7.01/1.34 % SZS status Unsatisfiable for theBenchmark
% 7.01/1.34
% 7.01/1.34 % Proof 1 at 0.65 (+ 0.20) seconds.
% 7.01/1.34 % Length of proof is 79.
% 7.01/1.34 % Level of proof is 31.
% 7.01/1.34 % Maximum clause weight is 99.000.
% 7.01/1.34 % Given clauses 88.
% 7.01/1.34
% 7.01/1.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------