%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP444-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 : n008.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:44 AM UTC 2026
% Result : Unsatisfiable 11.79s 2.11s
% Output : CNFRefutation 11.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 2
% Syntax : Number of formulae : 125 ( 125 unt; 0 def)
% Number of atoms : 125 ( 124 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 : 14 ( 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 : 485 ( 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_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(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_4,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_3,c_1]) ).
cnf(c_2847,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_3,c_3]) ).
cnf(c_5,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_2847]) ).
cnf(c_6,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_5,c_1]) ).
cnf(c_7,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_5,c_1]) ).
cnf(c_9,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,multiply(C,D))),multiply(B,C)))) = D,
inference(paramod,[status(thm)],[c_5,c_4]) ).
cnf(c_10,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_5,c_5]) ).
cnf(c_2848,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_10]) ).
cnf(c_12,plain,
multiply(multiply(A,inverse(A)),B) = multiply(multiply(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_1,c_2848]) ).
cnf(c_2849,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_10,c_3]) ).
cnf(c_13,plain,
multiply(A,inverse(A)) = multiply(B,inverse(B)),
inference(paramod,[status(thm)],[c_3,c_2849]) ).
cnf(c_15,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_13,c_1]) ).
cnf(c_16,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_13]) ).
cnf(c_17,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_13,c_3]) ).
cnf(c_20,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_13,c_4]) ).
cnf(c_48,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_12,c_13]) ).
cnf(c_2850,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_48,c_4]) ).
cnf(c_60,plain,
inverse(multiply(A,inverse(A))) = inverse(multiply(B,inverse(B))),
inference(paramod,[status(thm)],[c_20,c_2850]) ).
cnf(c_170,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_13,c_9]) ).
cnf(c_905,plain,
inverse(multiply(A,multiply(inverse(A),B))) = inverse(multiply(C,multiply(inverse(C),B))),
inference(paramod,[status(thm)],[c_9,c_15]) ).
cnf(c_909,plain,
inverse(multiply(A,multiply(inverse(A),inverse(inverse(B))))) = inverse(multiply(B,multiply(C,inverse(C)))),
inference(paramod,[status(thm)],[c_170,c_15]) ).
cnf(c_934,plain,
multiply(multiply(A,multiply(inverse(A),B)),inverse(multiply(C,multiply(inverse(C),B)))) = multiply(D,inverse(D)),
inference(paramod,[status(thm)],[c_905,c_13]) ).
cnf(c_2851,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_934,c_3]) ).
cnf(c_1215,plain,
multiply(A,multiply(inverse(A),B)) = multiply(C,multiply(inverse(C),B)),
inference(paramod,[status(thm)],[c_17,c_2851]) ).
cnf(c_2852,plain,
multiply(A,multiply(B,inverse(B))) = multiply(C,multiply(inverse(C),inverse(inverse(A)))),
inference(paramod,[status(thm)],[c_13,c_1215]) ).
cnf(c_1293,plain,
multiply(A,multiply(inverse(A),inverse(inverse(B)))) = multiply(B,multiply(C,inverse(C))),
inference(copy,[status(thm)],[c_2852]) ).
cnf(c_2853,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_15,c_1293]) ).
cnf(c_1384,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_2853]) ).
cnf(c_2854,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_16,c_1293]) ).
cnf(c_1488,plain,
multiply(A,multiply(inverse(A),inverse(multiply(B,inverse(B))))) = multiply(C,inverse(C)),
inference(paramod,[status(thm)],[c_1,c_2854]) ).
cnf(c_1493,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_1488,c_1]) ).
cnf(c_1500,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_1488,c_3]) ).
cnf(c_2855,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_1488,c_4]) ).
cnf(c_2856,plain,
inverse(F) = multiply(inverse(F),inverse(multiply(V6,inverse(V6)))),
inference(paramod,[status(thm)],[c_20,c_2855]) ).
cnf(c_1507,plain,
multiply(inverse(A),inverse(multiply(B,inverse(B)))) = inverse(A),
inference(copy,[status(thm)],[c_2856]) ).
cnf(c_2857,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_1507]) ).
cnf(c_1532,plain,
multiply(A,inverse(multiply(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_1,c_2857]) ).
cnf(c_1558,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_1532,c_1500]) ).
cnf(c_1559,plain,
inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C))))) = A,
inference(paramod,[status(thm)],[c_1532,c_1493]) ).
cnf(c_1570,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_1532,c_9]) ).
cnf(c_2858,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_7,c_1570]) ).
cnf(c_1604,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(B),B))) = inverse(multiply(C,inverse(C))),
inference(paramod,[status(thm)],[c_7,c_2858]) ).
cnf(c_1753,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_1604,c_15]) ).
cnf(c_1780,plain,
multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(inverse(C),C)))) = A,
inference(paramod,[status(thm)],[c_1604,c_1532]) ).
cnf(c_1782,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_1604,c_1604]) ).
cnf(c_1807,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_15,c_1780]) ).
cnf(c_1816,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_1604,c_1780]) ).
cnf(c_1820,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_17,c_9]) ).
cnf(c_1832,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_17,c_1532]) ).
cnf(c_1835,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_17,c_1780]) ).
cnf(c_2859,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_1782,c_6]) ).
cnf(c_1841,plain,
inverse(multiply(inverse(A),A)) = inverse(multiply(inverse(B),B)),
inference(paramod,[status(thm)],[c_6,c_2859]) ).
cnf(c_2860,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_1841,c_17]) ).
cnf(c_1941,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_17,c_2860]) ).
cnf(c_1959,plain,
multiply(inverse(multiply(A,inverse(A))),multiply(B,inverse(B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_60,c_1941]) ).
cnf(c_1981,plain,
multiply(A,multiply(inverse(B),B)) = multiply(C,multiply(inverse(C),A)),
inference(paramod,[status(thm)],[c_1941,c_1215]) ).
cnf(c_2025,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_1981,c_9]) ).
cnf(c_2026,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_1981,c_9]) ).
cnf(c_2861,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_1959,c_1]) ).
cnf(c_2479,plain,
inverse(inverse(multiply(A,multiply(inverse(B),B)))) = A,
inference(paramod,[status(thm)],[c_1558,c_2861]) ).
cnf(c_2485,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_1959,c_3]) ).
cnf(c_2491,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_1959,c_4]) ).
cnf(c_2862,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_1959,c_909]) ).
cnf(c_2863,plain,
inverse(A) = inverse(multiply(A,multiply(D,inverse(D)))),
inference(paramod,[status(thm)],[c_1559,c_2862]) ).
cnf(c_2533,plain,
inverse(multiply(A,multiply(B,inverse(B)))) = inverse(A),
inference(copy,[status(thm)],[c_2863]) ).
cnf(c_2591,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_2533,c_2491]) ).
cnf(c_2592,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_2533,c_2485]) ).
cnf(c_2864,plain,
multiply(multiply(A,inverse(A)),inverse(inverse(multiply(B,multiply(inverse(C),C))))) = B,
inference(paramod,[status(thm)],[c_2533,c_2026]) ).
cnf(c_2686,plain,
multiply(multiply(A,inverse(A)),B) = B,
inference(paramod,[status(thm)],[c_2479,c_2864]) ).
cnf(c_2865,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_2533,c_1835]) ).
cnf(c_2866,plain,
multiply(A,multiply(multiply(B,inverse(B)),multiply(inverse(D),multiply(multiply(F,inverse(F)),D)))) = A,
inference(paramod,[status(thm)],[c_2686,c_2865]) ).
cnf(c_2867,plain,
multiply(A,multiply(multiply(B,inverse(B)),multiply(inverse(D),D))) = A,
inference(paramod,[status(thm)],[c_2686,c_2866]) ).
cnf(c_2714,plain,
multiply(A,multiply(inverse(B),B)) = A,
inference(paramod,[status(thm)],[c_2686,c_2867]) ).
cnf(c_2868,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_2533,c_1832]) ).
cnf(c_2869,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(inverse(D),multiply(multiply(F,inverse(F)),D))),B))) = A,
inference(paramod,[status(thm)],[c_2686,c_2868]) ).
cnf(c_2870,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(inverse(D),D)),B))) = A,
inference(paramod,[status(thm)],[c_2686,c_2869]) ).
cnf(c_2716,plain,
multiply(A,inverse(multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_2714,c_2870]) ).
cnf(c_2871,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_2533,c_1820]) ).
cnf(c_2872,plain,
multiply(multiply(A,inverse(A)),multiply(inverse(C),multiply(multiply(multiply(E,inverse(E)),C),F))) = F,
inference(paramod,[status(thm)],[c_2686,c_2871]) ).
cnf(c_2873,plain,
multiply(multiply(A,inverse(A)),multiply(inverse(C),multiply(C,F))) = F,
inference(paramod,[status(thm)],[c_2686,c_2872]) ).
cnf(c_2728,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(paramod,[status(thm)],[c_2686,c_2873]) ).
cnf(c_2874,plain,
multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(multiply(C,inverse(C)),multiply(E,inverse(E)))))) = A,
inference(paramod,[status(thm)],[c_2716,c_1816]) ).
cnf(c_2875,plain,
multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(E,inverse(E))))) = A,
inference(paramod,[status(thm)],[c_2686,c_2874]) ).
cnf(c_2731,plain,
multiply(A,multiply(B,inverse(B))) = A,
inference(paramod,[status(thm)],[c_1532,c_2875]) ).
cnf(c_2876,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_2731,c_1807]) ).
cnf(c_2877,plain,
multiply(A,multiply(multiply(multiply(B,multiply(inverse(B),inverse(D))),D),inverse(multiply(inverse(F),F)))) = A,
inference(paramod,[status(thm)],[c_2686,c_2876]) ).
cnf(c_2733,plain,
multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(C))),C)) = A,
inference(paramod,[status(thm)],[c_2716,c_2877]) ).
cnf(c_2878,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_2716,c_1753]) ).
cnf(c_2879,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_2731,c_2878]) ).
cnf(c_2880,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(multiply(B,inverse(B)),inverse(E)))) = E,
inference(paramod,[status(thm)],[c_2686,c_2879]) ).
cnf(c_2881,plain,
inverse(multiply(multiply(A,inverse(A)),inverse(E))) = E,
inference(paramod,[status(thm)],[c_2686,c_2880]) ).
cnf(c_2740,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_2686,c_2881]) ).
cnf(c_2882,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_2731,c_1384]) ).
cnf(c_2883,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_2686,c_2882]) ).
cnf(c_2884,plain,
A = multiply(F,multiply(inverse(F),inverse(inverse(A)))),
inference(paramod,[status(thm)],[c_2733,c_2883]) ).
cnf(c_2885,plain,
A = multiply(F,multiply(inverse(F),A)),
inference(paramod,[status(thm)],[c_2740,c_2884]) ).
cnf(c_2759,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(copy,[status(thm)],[c_2885]) ).
cnf(c_2886,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_2740,c_2592]) ).
cnf(c_2887,plain,
inverse(multiply(A,multiply(multiply(B,inverse(B)),multiply(multiply(D,inverse(D)),inverse(multiply(E,A)))))) = E,
inference(paramod,[status(thm)],[c_2731,c_2886]) ).
cnf(c_2888,plain,
inverse(multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(E,A))))) = E,
inference(paramod,[status(thm)],[c_2686,c_2887]) ).
cnf(c_2775,plain,
inverse(multiply(A,inverse(multiply(B,A)))) = B,
inference(paramod,[status(thm)],[c_2686,c_2888]) ).
cnf(c_2889,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_2740,c_2591]) ).
cnf(c_2890,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_2731,c_2889]) ).
cnf(c_2891,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(inverse(multiply(D,E)),multiply(multiply(F,inverse(F)),D)))) = E,
inference(paramod,[status(thm)],[c_2686,c_2890]) ).
cnf(c_2892,plain,
inverse(multiply(multiply(A,inverse(A)),multiply(inverse(multiply(D,E)),D))) = E,
inference(paramod,[status(thm)],[c_2686,c_2891]) ).
cnf(c_2776,plain,
inverse(multiply(inverse(multiply(A,B)),A)) = B,
inference(paramod,[status(thm)],[c_2686,c_2892]) ).
cnf(c_2893,plain,
multiply(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,C)),multiply(B,E)))) = multiply(inverse(E),C),
inference(paramod,[status(thm)],[c_2714,c_2025]) ).
cnf(c_2807,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,C))) = multiply(inverse(C),B),
inference(paramod,[status(thm)],[c_2686,c_2893]) ).
cnf(c_2894,plain,
inverse(A) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_2775,c_2740]) ).
cnf(c_2812,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_2894]) ).
cnf(c_2820,plain,
inverse(multiply(inverse(A),B)) = multiply(inverse(B),A),
inference(paramod,[status(thm)],[c_2759,c_2776]) ).
cnf(c_2821,plain,
multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
inference(paramod,[status(thm)],[c_2820,c_2807]) ).
cnf(c_2895,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_2812,c_2728]) ).
cnf(c_2823,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_2895]) ).
cnf(c_2826,plain,
multiply(multiply(inverse(A),inverse(B)),multiply(B,C)) = multiply(inverse(A),C),
inference(paramod,[status(thm)],[c_2823,c_2821]) ).
cnf(c_2896,plain,
multiply(multiply(A,inverse(B)),multiply(B,C)) = multiply(inverse(inverse(A)),C),
inference(paramod,[status(thm)],[c_2740,c_2826]) ).
cnf(c_2839,plain,
multiply(multiply(A,inverse(B)),multiply(B,C)) = multiply(A,C),
inference(paramod,[status(thm)],[c_2740,c_2896]) ).
cnf(c_2897,plain,
multiply(multiply(A,inverse(inverse(B))),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_2728,c_2839]) ).
cnf(c_2845,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_2740,c_2897]) ).
cnf(c_2846,plain,
$false,
inference(resolve,[status(thm)],[c_2845,c_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP444-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.08/0.35 % Computer : n008.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:55:24 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 1332569 was started by sandbox2 on n008,
% 0.08/0.35 % Fri Sep 25 14:55:24 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.36
% 0.08/0.36 % From the command line: assign(max_seconds, 300).
% 11.79/2.11
% 11.79/2.11 % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 11.79/2.11
% 11.79/2.11 % SZS status Unsatisfiable for theBenchmark
% 11.79/2.11
% 11.79/2.11 % Proof 1 at 1.14 (+ 0.37) seconds.
% 11.79/2.11 % Length of proof is 72.
% 11.79/2.11 % Level of proof is 31.
% 11.79/2.11 % Maximum clause weight is 98.000.
% 11.79/2.11 % Given clauses 86.
% 11.79/2.11
% 11.79/2.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------