%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP426-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:26 AM UTC 2026
% Result : Unsatisfiable 2.40s 0.79s
% Output : CNFRefutation 2.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 2
% Syntax : Number of formulae : 223 ( 223 unt; 0 def)
% Number of atoms : 223 ( 222 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 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 : 848 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(inverse(multiply(inverse(multiply(VAR_0,inverse(multiply(inverse(VAR_1),VAR_2)))),multiply(VAR_0,inverse(VAR_2)))),inverse(multiply(inverse(VAR_2),VAR_2))) = VAR_1,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),C)))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C))) = B,
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,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C))))) = multiply(inverse(multiply(D,inverse(multiply(inverse(B),C)))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_4,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(multiply(inverse(multiply(B,inverse(multiply(inverse(A),C)))),multiply(B,inverse(C)))),inverse(C)))),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_5,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(C),C)))),C)))),multiply(A,inverse(C))) = B,
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_6,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(C),C))) = B,
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_7,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(B),B)))))),inverse(multiply(inverse(inverse(multiply(inverse(B),B))),inverse(multiply(inverse(B),B))))) = multiply(inverse(C),multiply(inverse(multiply(inverse(multiply(D,inverse(multiply(inverse(C),B)))),multiply(D,inverse(B)))),inverse(B))),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_8,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),C)))),multiply(A,inverse(C))) = multiply(inverse(multiply(D,inverse(multiply(inverse(B),C)))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_3,c_3]) ).
cnf(c_9,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D)))))),inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(D))))) = multiply(C,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(D),D)))),D))),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_803,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D))))) = multiply(inverse(multiply(E,inverse(multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(D),D)))),D)))),multiply(C,inverse(D)))))),multiply(E,inverse(multiply(C,inverse(D))))),
inference(paramod,[status(thm)],[c_5,c_8]) ).
cnf(c_12,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(C,inverse(D))))) = multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(multiply(C,inverse(D))))),
inference(paramod,[status(thm)],[c_5,c_803]) ).
cnf(c_804,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(C,inverse(D)))))),multiply(A,inverse(multiply(C,inverse(D)))))),inverse(multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(D))))) = B,
inference(paramod,[status(thm)],[c_12,c_1]) ).
cnf(c_13,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),C))) = B,
inference(paramod,[status(thm)],[c_9,c_804]) ).
cnf(c_805,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(C),F)))),multiply(E,inverse(F)))),inverse(multiply(inverse(F),F)))))),
inference(paramod,[status(thm)],[c_1,c_12]) ).
cnf(c_15,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_1,c_805]) ).
cnf(c_806,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(D)))))),multiply(A,inverse(multiply(E,inverse(D)))))),inverse(multiply(inverse(multiply(E,inverse(D))),multiply(E,inverse(D))))) = multiply(E,inverse(C)),
inference(paramod,[status(thm)],[c_15,c_1]) ).
cnf(c_17,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,inverse(C))),multiply(B,inverse(D)))),inverse(multiply(inverse(D),D)))),D))) = multiply(A,inverse(C)),
inference(paramod,[status(thm)],[c_9,c_806]) ).
cnf(c_807,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(multiply(B,inverse(multiply(inverse(A),C)))),multiply(B,inverse(C)))),inverse(D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(C),C)))),multiply(E,inverse(D))),
inference(paramod,[status(thm)],[c_1,c_15]) ).
cnf(c_19,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(C))),
inference(copy,[status(thm)],[c_807]) ).
cnf(c_808,plain,
multiply(inverse(A),multiply(B,inverse(C))) = multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),multiply(B,inverse(E)))),inverse(multiply(inverse(E),E)))),E)))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_13,c_15]) ).
cnf(c_23,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),inverse(multiply(inverse(D),D)))),D)))),multiply(A,inverse(E))) = multiply(inverse(B),multiply(C,inverse(E))),
inference(copy,[status(thm)],[c_808]) ).
cnf(c_809,plain,
multiply(inverse(multiply(A,inverse(B))),C) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),multiply(A,inverse(E)))),inverse(multiply(inverse(E),E)))),E)))),
inference(paramod,[status(thm)],[c_13,c_15]) ).
cnf(c_24,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),multiply(D,inverse(E)))),inverse(multiply(inverse(E),E)))),E)))) = multiply(inverse(multiply(D,inverse(B))),C),
inference(copy,[status(thm)],[c_809]) ).
cnf(c_26,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C))) = multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_17,c_1]) ).
cnf(c_27,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(C)))),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_17,c_4]) ).
cnf(c_29,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),inverse(multiply(inverse(D),D)))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(E)))),inverse(multiply(inverse(E),E)))),E))),
inference(paramod,[status(thm)],[c_13,c_17]) ).
cnf(c_30,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(C),C)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_26,c_15]) ).
cnf(c_31,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(C)))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_26,c_15]) ).
cnf(c_810,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(inverse(multiply(inverse(C),C))),inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(C),C))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(E)))),inverse(multiply(inverse(E),E)))),E),
inference(paramod,[status(thm)],[c_17,c_6]) ).
cnf(c_811,plain,
B = multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(E)))),inverse(multiply(inverse(E),E)))),E),
inference(paramod,[status(thm)],[c_6,c_810]) ).
cnf(c_33,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),C) = B,
inference(copy,[status(thm)],[c_811]) ).
cnf(c_37,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(multiply(inverse(B),B)))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_1,c_19]) ).
cnf(c_812,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(multiply(B,inverse(multiply(inverse(A),C)))),multiply(B,inverse(C)))),inverse(multiply(inverse(C),C)))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_1,c_37]) ).
cnf(c_44,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_1,c_812]) ).
cnf(c_813,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))) = multiply(inverse(multiply(inverse(multiply(C,inverse(multiply(inverse(B),B)))),multiply(C,inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))),
inference(paramod,[status(thm)],[c_37,c_26]) ).
cnf(c_56,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))) = multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))),
inference(copy,[status(thm)],[c_813]) ).
cnf(c_67,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_44,c_1]) ).
cnf(c_68,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C)))),inverse(multiply(inverse(C),C))) = B,
inference(paramod,[status(thm)],[c_44,c_1]) ).
cnf(c_69,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),inverse(multiply(inverse(B),A)))),multiply(inverse(C),C))),inverse(multiply(inverse(A),A))) = B,
inference(paramod,[status(thm)],[c_44,c_1]) ).
cnf(c_77,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(C),C)))))),inverse(multiply(inverse(D),D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),C)))),multiply(E,inverse(C))),
inference(paramod,[status(thm)],[c_44,c_3]) ).
cnf(c_85,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),inverse(multiply(inverse(C),C)))),D)))),multiply(A,inverse(D))) = B,
inference(paramod,[status(thm)],[c_44,c_5]) ).
cnf(c_89,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C))),
inference(paramod,[status(thm)],[c_44,c_15]) ).
cnf(c_90,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(C),C)) = multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(A))),
inference(paramod,[status(thm)],[c_44,c_15]) ).
cnf(c_101,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(inverse(multiply(inverse(B),B)))))),inverse(multiply(inverse(C),C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(B))),
inference(paramod,[status(thm)],[c_44,c_7]) ).
cnf(c_108,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),B)))),multiply(A,inverse(C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(multiply(inverse(D),B)))),multiply(inverse(E),E))),inverse(C))),
inference(paramod,[status(thm)],[c_44,c_19]) ).
cnf(c_814,plain,
multiply(inverse(B),B) = multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))),
inference(paramod,[status(thm)],[c_67,c_56]) ).
cnf(c_109,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(B),B)))) = multiply(inverse(B),B),
inference(copy,[status(thm)],[c_814]) ).
cnf(c_110,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_89,c_44]) ).
cnf(c_815,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_44,c_89]) ).
cnf(c_113,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(B)),inverse(A))),
inference(copy,[status(thm)],[c_815]) ).
cnf(c_116,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_44,c_110]) ).
cnf(c_130,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(C),C)) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_116,c_116]) ).
cnf(c_159,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),inverse(multiply(inverse(D),D)))),D)))),multiply(A,inverse(E))) = multiply(inverse(B),multiply(inverse(inverse(D)),inverse(E))),
inference(paramod,[status(thm)],[c_44,c_23]) ).
cnf(c_816,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(inverse(C)),inverse(D)))),inverse(multiply(inverse(D),D)))),D)))),multiply(A,inverse(C))) = multiply(inverse(B),multiply(inverse(E),E)),
inference(paramod,[status(thm)],[c_44,c_23]) ).
cnf(c_163,plain,
multiply(inverse(A),multiply(inverse(inverse(B)),inverse(B))) = multiply(inverse(A),multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_23,c_816]) ).
cnf(c_166,plain,
multiply(inverse(A),multiply(inverse(B),B)) = multiply(inverse(A),multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_44,c_163]) ).
cnf(c_817,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),multiply(inverse(inverse(B)),inverse(D)))),inverse(multiply(inverse(D),D)))),D)))) = multiply(inverse(multiply(inverse(E),E)),C),
inference(paramod,[status(thm)],[c_44,c_24]) ).
cnf(c_213,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(A))),B) = multiply(inverse(multiply(inverse(C),C)),B),
inference(paramod,[status(thm)],[c_24,c_817]) ).
cnf(c_214,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),multiply(inverse(inverse(C)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),multiply(E,inverse(F)))),inverse(multiply(inverse(F),F)))),F)))) = multiply(inverse(multiply(E,inverse(C))),D),
inference(paramod,[status(thm)],[c_116,c_24]) ).
cnf(c_221,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(B)),inverse(C)))),inverse(C)))),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_44,c_27]) ).
cnf(c_818,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),inverse(multiply(inverse(D),D)))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(inverse(D)),inverse(E)))),inverse(multiply(inverse(E),E)))),E))),
inference(paramod,[status(thm)],[c_44,c_29]) ).
cnf(c_228,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(inverse(C)),inverse(D)))),inverse(multiply(inverse(D),D)))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))),C))),
inference(copy,[status(thm)],[c_818]) ).
cnf(c_237,plain,
multiply(inverse(multiply(inverse(A),A)),B) = multiply(inverse(multiply(inverse(C),C)),B),
inference(paramod,[status(thm)],[c_44,c_213]) ).
cnf(c_240,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),C) = multiply(inverse(multiply(inverse(D),D)),C),
inference(paramod,[status(thm)],[c_116,c_213]) ).
cnf(c_819,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))),inverse(B))),multiply(inverse(multiply(inverse(F),F)),inverse(C))),
inference(paramod,[status(thm)],[c_240,c_89]) ).
cnf(c_264,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),inverse(C))),multiply(inverse(multiply(inverse(D),D)),inverse(E))) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(C)),inverse(E))),
inference(copy,[status(thm)],[c_819]) ).
cnf(c_820,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E))),inverse(B))),multiply(inverse(multiply(inverse(F),F)),inverse(A))),
inference(paramod,[status(thm)],[c_240,c_90]) ).
cnf(c_275,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B))),inverse(C))),multiply(inverse(multiply(inverse(D),D)),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(C))),multiply(inverse(F),F)),
inference(copy,[status(thm)],[c_820]) ).
cnf(c_281,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B))) = multiply(inverse(C),C),
inference(paramod,[status(thm)],[c_44,c_109]) ).
cnf(c_297,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))),multiply(inverse(D),D))),multiply(inverse(E),E)))) = multiply(inverse(E),E),
inference(paramod,[status(thm)],[c_130,c_109]) ).
cnf(c_303,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(D),D))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(C),C)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_44,c_30]) ).
cnf(c_317,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(V6),V6)),inverse(E))),
inference(paramod,[status(thm)],[c_237,c_30]) ).
cnf(c_322,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(D))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_44,c_31]) ).
cnf(c_333,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C)))),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(C)))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),inverse(D))),multiply(inverse(multiply(inverse(V6),V6)),inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_237,c_31]) ).
cnf(c_374,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C)))) = multiply(inverse(D),D),
inference(paramod,[status(thm)],[c_281,c_116]) ).
cnf(c_379,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C)))) = multiply(inverse(A),multiply(inverse(D),D)),
inference(paramod,[status(thm)],[c_281,c_166]) ).
cnf(c_403,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B))) = multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D))),
inference(paramod,[status(thm)],[c_281,c_281]) ).
cnf(c_821,plain,
multiply(inverse(multiply(inverse(A),A)),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(D),D)),multiply(inverse(multiply(inverse(E),E)),inverse(multiply(inverse(F),F))))),
inference(paramod,[status(thm)],[c_374,c_89]) ).
cnf(c_437,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(multiply(inverse(C),C)),multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),E))))) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(B)),inverse(A))),
inference(copy,[status(thm)],[c_821]) ).
cnf(c_493,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(D),D)))),multiply(inverse(E),E))) = multiply(inverse(multiply(F,inverse(B))),multiply(F,inverse(A))),
inference(paramod,[status(thm)],[c_379,c_90]) ).
cnf(c_822,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),D)),inverse(multiply(inverse(E),E)))),multiply(inverse(F),F))),multiply(inverse(inverse(B)),inverse(A))),
inference(paramod,[status(thm)],[c_379,c_113]) ).
cnf(c_495,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),multiply(inverse(C),C))),multiply(inverse(inverse(D)),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(D))),multiply(inverse(F),F)),
inference(copy,[status(thm)],[c_822]) ).
cnf(c_576,plain,
multiply(inverse(multiply(inverse(A),A)),B) = B,
inference(paramod,[status(thm)],[c_281,c_33]) ).
cnf(c_823,plain,
multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(B),B)))),C) = C,
inference(paramod,[status(thm)],[c_403,c_33]) ).
cnf(c_585,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),B) = B,
inference(paramod,[status(thm)],[c_576,c_823]) ).
cnf(c_824,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),inverse(multiply(inverse(C),C))))),multiply(inverse(inverse(D)),inverse(E)))),inverse(multiply(inverse(E),E)))),E) = D,
inference(paramod,[status(thm)],[c_374,c_33]) ).
cnf(c_825,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(C),C)))),multiply(inverse(inverse(D)),inverse(E)))),inverse(multiply(inverse(E),E)))),E) = D,
inference(paramod,[status(thm)],[c_576,c_824]) ).
cnf(c_826,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(C),C))),multiply(inverse(inverse(D)),inverse(E)))),inverse(multiply(inverse(E),E)))),E) = D,
inference(paramod,[status(thm)],[c_576,c_825]) ).
cnf(c_586,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),inverse(multiply(inverse(B),B)))),B) = A,
inference(paramod,[status(thm)],[c_585,c_826]) ).
cnf(c_827,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),B))),multiply(inverse(C),C))),multiply(inverse(inverse(D)),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(D))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_576,c_495]) ).
cnf(c_828,plain,
multiply(inverse(multiply(inverse(C),C)),multiply(inverse(inverse(D)),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(D))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_585,c_827]) ).
cnf(c_829,plain,
multiply(inverse(inverse(D)),inverse(E)) = multiply(inverse(multiply(inverse(inverse(E)),inverse(D))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_576,c_828]) ).
cnf(c_597,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(C),C)) = multiply(inverse(inverse(B)),inverse(A)),
inference(copy,[status(thm)],[c_829]) ).
cnf(c_830,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(inverse(multiply(inverse(D),D))),multiply(inverse(E),E))) = multiply(inverse(multiply(F,inverse(B))),multiply(F,inverse(A))),
inference(paramod,[status(thm)],[c_576,c_493]) ).
cnf(c_831,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(E),E)) = multiply(inverse(multiply(F,inverse(B))),multiply(F,inverse(A))),
inference(paramod,[status(thm)],[c_585,c_830]) ).
cnf(c_832,plain,
multiply(inverse(inverse(B)),inverse(A)) = multiply(inverse(multiply(F,inverse(B))),multiply(F,inverse(A))),
inference(paramod,[status(thm)],[c_597,c_831]) ).
cnf(c_598,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(C))) = multiply(inverse(inverse(B)),inverse(C)),
inference(copy,[status(thm)],[c_832]) ).
cnf(c_833,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(multiply(inverse(C),C)),inverse(multiply(inverse(E),E)))) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(B)),inverse(A))),
inference(paramod,[status(thm)],[c_576,c_437]) ).
cnf(c_834,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),inverse(multiply(inverse(E),E))) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(B)),inverse(A))),
inference(paramod,[status(thm)],[c_576,c_833]) ).
cnf(c_601,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),inverse(multiply(inverse(C),C))) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_576,c_834]) ).
cnf(c_835,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(multiply(E,inverse(B))),multiply(E,inverse(C)))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),inverse(D))),multiply(inverse(multiply(inverse(V6),V6)),inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_598,c_333]) ).
cnf(c_836,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),inverse(D))),multiply(inverse(multiply(inverse(V6),V6)),inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_598,c_835]) ).
cnf(c_837,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(inverse(C)),inverse(B))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),inverse(D))),multiply(inverse(multiply(inverse(V6),V6)),inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_601,c_836]) ).
cnf(c_838,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(inverse(C)),inverse(B))) = multiply(inverse(inverse(D)),multiply(inverse(multiply(inverse(V6),V6)),inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_576,c_837]) ).
cnf(c_604,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),inverse(C))),multiply(inverse(inverse(B)),inverse(A))) = multiply(inverse(inverse(C)),inverse(multiply(inverse(B),B))),
inference(paramod,[status(thm)],[c_576,c_838]) ).
cnf(c_839,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(V6),V6)),inverse(E))),
inference(paramod,[status(thm)],[c_598,c_317]) ).
cnf(c_840,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(multiply(D,inverse(B))),multiply(D,inverse(C)))),inverse(E))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(V6),V6)),inverse(E))),
inference(paramod,[status(thm)],[c_601,c_839]) ).
cnf(c_841,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(E))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(V6),V6)),inverse(E))),
inference(paramod,[status(thm)],[c_598,c_840]) ).
cnf(c_842,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(E))) = multiply(inverse(inverse(multiply(inverse(C),C))),multiply(inverse(multiply(inverse(V6),V6)),inverse(E))),
inference(paramod,[status(thm)],[c_576,c_841]) ).
cnf(c_843,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(E))) = multiply(inverse(inverse(multiply(inverse(C),C))),inverse(E)),
inference(paramod,[status(thm)],[c_576,c_842]) ).
cnf(c_605,plain,
multiply(inverse(multiply(inverse(inverse(A)),inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(A))),inverse(C))) = inverse(C),
inference(paramod,[status(thm)],[c_585,c_843]) ).
cnf(c_844,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),D))),multiply(inverse(E),E)))) = multiply(inverse(E),E),
inference(paramod,[status(thm)],[c_576,c_297]) ).
cnf(c_845,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(E),E)))) = multiply(inverse(E),E),
inference(paramod,[status(thm)],[c_576,c_844]) ).
cnf(c_846,plain,
multiply(inverse(multiply(inverse(A),A)),inverse(multiply(inverse(E),E))) = multiply(inverse(E),E),
inference(paramod,[status(thm)],[c_576,c_845]) ).
cnf(c_606,plain,
inverse(multiply(inverse(A),A)) = multiply(inverse(A),A),
inference(paramod,[status(thm)],[c_576,c_846]) ).
cnf(c_847,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),inverse(C))),multiply(inverse(multiply(inverse(D),D)),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_606,c_275]) ).
cnf(c_848,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),inverse(C))),multiply(multiply(inverse(D),D),inverse(E))) = multiply(inverse(multiply(inverse(inverse(E)),inverse(C))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_606,c_847]) ).
cnf(c_613,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),inverse(C))),multiply(multiply(inverse(D),D),inverse(E))) = multiply(inverse(inverse(C)),inverse(E)),
inference(paramod,[status(thm)],[c_597,c_848]) ).
cnf(c_849,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),inverse(C))),multiply(inverse(multiply(inverse(D),D)),inverse(E))) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(C)),inverse(E))),
inference(paramod,[status(thm)],[c_606,c_264]) ).
cnf(c_850,plain,
multiply(inverse(multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),inverse(C))),multiply(multiply(inverse(D),D),inverse(E))) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(C)),inverse(E))),
inference(paramod,[status(thm)],[c_606,c_849]) ).
cnf(c_851,plain,
multiply(inverse(inverse(C)),inverse(E)) = multiply(inverse(multiply(inverse(F),F)),multiply(inverse(inverse(C)),inverse(E))),
inference(paramod,[status(thm)],[c_613,c_850]) ).
cnf(c_852,plain,
multiply(inverse(inverse(C)),inverse(E)) = multiply(multiply(inverse(F),F),multiply(inverse(inverse(C)),inverse(E))),
inference(paramod,[status(thm)],[c_606,c_851]) ).
cnf(c_623,plain,
multiply(multiply(inverse(A),A),multiply(inverse(inverse(B)),inverse(C))) = multiply(inverse(inverse(B)),inverse(C)),
inference(copy,[status(thm)],[c_852]) ).
cnf(c_853,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(B)),inverse(C)))),inverse(C)))),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_598,c_221]) ).
cnf(c_854,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),multiply(inverse(C),C))),multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(B)),inverse(C)))),inverse(C)))),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_606,c_853]) ).
cnf(c_855,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(multiply(inverse(D),D)),multiply(inverse(inverse(B)),inverse(C)))),inverse(C)))),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_597,c_854]) ).
cnf(c_856,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(multiply(inverse(D),D),multiply(inverse(inverse(B)),inverse(C)))),inverse(C)))),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_606,c_855]) ).
cnf(c_857,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(C)))),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_623,c_856]) ).
cnf(c_858,plain,
multiply(inverse(inverse(C)),inverse(multiply(inverse(C),C))) = C,
inference(paramod,[status(thm)],[c_605,c_857]) ).
cnf(c_643,plain,
multiply(inverse(inverse(A)),multiply(inverse(A),A)) = A,
inference(paramod,[status(thm)],[c_606,c_858]) ).
cnf(c_859,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),multiply(inverse(inverse(C)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),multiply(E,inverse(F)))),inverse(multiply(inverse(F),F)))),F)))) = multiply(inverse(multiply(E,inverse(C))),D),
inference(paramod,[status(thm)],[c_606,c_214]) ).
cnf(c_646,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(B),B))),multiply(inverse(inverse(C)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),multiply(E,inverse(F)))),multiply(inverse(F),F))),F)))) = multiply(inverse(multiply(E,inverse(C))),D),
inference(paramod,[status(thm)],[c_606,c_859]) ).
cnf(c_860,plain,
multiply(inverse(multiply(multiply(inverse(A),A),multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C)))),inverse(multiply(inverse(C),C))) = B,
inference(paramod,[status(thm)],[c_606,c_68]) ).
cnf(c_861,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C))),inverse(multiply(inverse(C),C))) = B,
inference(paramod,[status(thm)],[c_623,c_860]) ).
cnf(c_862,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C))),multiply(inverse(C),C)) = B,
inference(paramod,[status(thm)],[c_606,c_861]) ).
cnf(c_702,plain,
multiply(inverse(inverse(A)),inverse(multiply(inverse(B),A))) = B,
inference(paramod,[status(thm)],[c_597,c_862]) ).
cnf(c_863,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_598,c_322]) ).
cnf(c_864,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(inverse(C),C)))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_597,c_863]) ).
cnf(c_865,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),multiply(inverse(C),C))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_606,c_864]) ).
cnf(c_866,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(D))),multiply(inverse(inverse(C)),inverse(B))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_597,c_865]) ).
cnf(c_867,plain,
multiply(inverse(inverse(D)),inverse(multiply(inverse(C),C))) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_604,c_866]) ).
cnf(c_868,plain,
multiply(inverse(inverse(D)),multiply(inverse(C),C)) = multiply(inverse(multiply(F,inverse(D))),multiply(F,inverse(multiply(inverse(C),C)))),
inference(paramod,[status(thm)],[c_606,c_867]) ).
cnf(c_869,plain,
multiply(inverse(inverse(D)),multiply(inverse(C),C)) = multiply(inverse(multiply(F,inverse(D))),multiply(F,multiply(inverse(C),C))),
inference(paramod,[status(thm)],[c_606,c_868]) ).
cnf(c_721,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C))) = multiply(inverse(inverse(B)),multiply(inverse(C),C)),
inference(copy,[status(thm)],[c_869]) ).
cnf(c_870,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(multiply(inverse(C),C)))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(D),D))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(C),C)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_598,c_303]) ).
cnf(c_871,plain,
multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),multiply(inverse(C),C))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(D),D))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(C),C)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_606,c_870]) ).
cnf(c_872,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(D),D))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(C),C)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_597,c_871]) ).
cnf(c_873,plain,
multiply(inverse(multiply(inverse(inverse(C)),inverse(B))),multiply(inverse(multiply(inverse(inverse(B)),inverse(C))),inverse(E))) = multiply(inverse(multiply(F,inverse(multiply(inverse(C),C)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_597,c_872]) ).
cnf(c_874,plain,
inverse(E) = multiply(inverse(multiply(F,inverse(multiply(inverse(C),C)))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_605,c_873]) ).
cnf(c_875,plain,
inverse(E) = multiply(inverse(multiply(F,multiply(inverse(C),C))),multiply(F,inverse(E))),
inference(paramod,[status(thm)],[c_606,c_874]) ).
cnf(c_723,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,inverse(C))) = inverse(C),
inference(copy,[status(thm)],[c_875]) ).
cnf(c_876,plain,
multiply(inverse(multiply(A,multiply(inverse(B),B))),multiply(A,inverse(C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(multiply(inverse(D),B)))),multiply(inverse(E),E))),inverse(C))),
inference(paramod,[status(thm)],[c_606,c_108]) ).
cnf(c_877,plain,
inverse(C) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(multiply(inverse(D),B)))),multiply(inverse(E),E))),inverse(C))),
inference(paramod,[status(thm)],[c_723,c_876]) ).
cnf(c_878,plain,
inverse(C) = multiply(inverse(D),multiply(inverse(multiply(inverse(D),multiply(inverse(E),E))),inverse(C))),
inference(paramod,[status(thm)],[c_702,c_877]) ).
cnf(c_726,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(A),multiply(inverse(B),B))),inverse(C))) = inverse(C),
inference(copy,[status(thm)],[c_878]) ).
cnf(c_879,plain,
multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),inverse(multiply(inverse(A),A))) = B,
inference(paramod,[status(thm)],[c_702,c_69]) ).
cnf(c_729,plain,
multiply(inverse(multiply(inverse(A),multiply(inverse(B),B))),multiply(inverse(C),C)) = A,
inference(paramod,[status(thm)],[c_606,c_879]) ).
cnf(c_880,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),multiply(inverse(D),D))),D)))),multiply(A,inverse(E))) = multiply(inverse(B),multiply(inverse(inverse(D)),inverse(E))),
inference(paramod,[status(thm)],[c_606,c_159]) ).
cnf(c_881,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(B),D)))),multiply(A,inverse(E))) = multiply(inverse(B),multiply(inverse(inverse(D)),inverse(E))),
inference(paramod,[status(thm)],[c_729,c_880]) ).
cnf(c_735,plain,
multiply(inverse(inverse(multiply(inverse(A),B))),inverse(C)) = multiply(inverse(A),multiply(inverse(inverse(B)),inverse(C))),
inference(paramod,[status(thm)],[c_598,c_881]) ).
cnf(c_882,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(B),B))))),inverse(multiply(inverse(C),C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(B))),
inference(paramod,[status(thm)],[c_606,c_101]) ).
cnf(c_883,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(B),B)))),inverse(multiply(inverse(C),C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(B))),
inference(paramod,[status(thm)],[c_606,c_882]) ).
cnf(c_884,plain,
multiply(inverse(multiply(inverse(inverse(B)),multiply(inverse(B),B))),inverse(multiply(inverse(C),C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(B))),
inference(paramod,[status(thm)],[c_721,c_883]) ).
cnf(c_885,plain,
multiply(inverse(B),inverse(multiply(inverse(C),C))) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(B))),
inference(paramod,[status(thm)],[c_643,c_884]) ).
cnf(c_886,plain,
multiply(inverse(B),multiply(inverse(C),C)) = multiply(inverse(D),multiply(inverse(multiply(inverse(multiply(E,inverse(multiply(inverse(D),B)))),multiply(E,inverse(B)))),inverse(B))),
inference(paramod,[status(thm)],[c_606,c_885]) ).
cnf(c_887,plain,
multiply(inverse(B),multiply(inverse(C),C)) = multiply(inverse(D),multiply(inverse(multiply(inverse(inverse(multiply(inverse(D),B))),inverse(B))),inverse(B))),
inference(paramod,[status(thm)],[c_598,c_886]) ).
cnf(c_888,plain,
multiply(inverse(B),multiply(inverse(C),C)) = multiply(inverse(D),multiply(inverse(multiply(inverse(D),multiply(inverse(inverse(B)),inverse(B)))),inverse(B))),
inference(paramod,[status(thm)],[c_735,c_887]) ).
cnf(c_740,plain,
multiply(inverse(A),multiply(inverse(B),B)) = inverse(A),
inference(paramod,[status(thm)],[c_726,c_888]) ).
cnf(c_889,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(C),C))),D)))),multiply(A,inverse(D))) = B,
inference(paramod,[status(thm)],[c_606,c_85]) ).
cnf(c_890,plain,
multiply(inverse(multiply(A,inverse(multiply(inverse(inverse(B)),D)))),multiply(A,inverse(D))) = B,
inference(paramod,[status(thm)],[c_740,c_889]) ).
cnf(c_891,plain,
multiply(inverse(inverse(multiply(inverse(inverse(B)),D))),inverse(D)) = B,
inference(paramod,[status(thm)],[c_598,c_890]) ).
cnf(c_892,plain,
multiply(inverse(inverse(B)),multiply(inverse(inverse(D)),inverse(D))) = B,
inference(paramod,[status(thm)],[c_735,c_891]) ).
cnf(c_741,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_740,c_892]) ).
cnf(c_893,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,inverse(multiply(inverse(C),C))))),inverse(multiply(inverse(D),D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),C)))),multiply(E,inverse(C))),
inference(paramod,[status(thm)],[c_606,c_77]) ).
cnf(c_894,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(A,multiply(inverse(C),C)))),inverse(multiply(inverse(D),D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),C)))),multiply(E,inverse(C))),
inference(paramod,[status(thm)],[c_606,c_893]) ).
cnf(c_895,plain,
multiply(inverse(multiply(inverse(inverse(B)),multiply(inverse(C),C))),inverse(multiply(inverse(D),D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),C)))),multiply(E,inverse(C))),
inference(paramod,[status(thm)],[c_721,c_894]) ).
cnf(c_896,plain,
multiply(inverse(multiply(B,multiply(inverse(C),C))),inverse(multiply(inverse(D),D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),C)))),multiply(E,inverse(C))),
inference(paramod,[status(thm)],[c_741,c_895]) ).
cnf(c_897,plain,
multiply(inverse(multiply(B,multiply(inverse(C),C))),multiply(inverse(D),D)) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),C)))),multiply(E,inverse(C))),
inference(paramod,[status(thm)],[c_606,c_896]) ).
cnf(c_898,plain,
inverse(multiply(B,multiply(inverse(C),C))) = multiply(inverse(multiply(E,inverse(multiply(inverse(B),C)))),multiply(E,inverse(C))),
inference(paramod,[status(thm)],[c_740,c_897]) ).
cnf(c_899,plain,
inverse(multiply(B,multiply(inverse(C),C))) = multiply(inverse(inverse(multiply(inverse(B),C))),inverse(C)),
inference(paramod,[status(thm)],[c_598,c_898]) ).
cnf(c_744,plain,
inverse(multiply(A,multiply(inverse(B),B))) = multiply(multiply(inverse(A),B),inverse(B)),
inference(paramod,[status(thm)],[c_741,c_899]) ).
cnf(c_900,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),inverse(multiply(inverse(B),B)))),B) = A,
inference(paramod,[status(thm)],[c_741,c_586]) ).
cnf(c_901,plain,
multiply(inverse(multiply(inverse(multiply(A,inverse(B))),multiply(inverse(B),B))),B) = A,
inference(paramod,[status(thm)],[c_606,c_900]) ).
cnf(c_902,plain,
multiply(inverse(inverse(multiply(A,inverse(B)))),B) = A,
inference(paramod,[status(thm)],[c_740,c_901]) ).
cnf(c_751,plain,
multiply(multiply(A,inverse(B)),B) = A,
inference(paramod,[status(thm)],[c_741,c_902]) ).
cnf(c_903,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),inverse(multiply(inverse(D),D)))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))),C))),
inference(paramod,[status(thm)],[c_741,c_228]) ).
cnf(c_904,plain,
multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(C,inverse(D)))),multiply(inverse(D),D))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))),C))),
inference(paramod,[status(thm)],[c_606,c_903]) ).
cnf(c_905,plain,
multiply(A,inverse(multiply(inverse(inverse(multiply(inverse(B),multiply(C,inverse(D))))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))),C))),
inference(paramod,[status(thm)],[c_740,c_904]) ).
cnf(c_906,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(C,inverse(D))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),multiply(inverse(E),E))),inverse(multiply(inverse(C),C)))),C))),
inference(paramod,[status(thm)],[c_741,c_905]) ).
cnf(c_907,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(C,inverse(D))),D))) = multiply(A,inverse(multiply(inverse(multiply(inverse(inverse(B)),inverse(multiply(inverse(C),C)))),C))),
inference(paramod,[status(thm)],[c_740,c_906]) ).
cnf(c_908,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(C,inverse(D))),D))) = multiply(A,inverse(multiply(inverse(multiply(B,inverse(multiply(inverse(C),C)))),C))),
inference(paramod,[status(thm)],[c_741,c_907]) ).
cnf(c_909,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(C,inverse(D))),D))) = multiply(A,inverse(multiply(inverse(multiply(B,multiply(inverse(C),C))),C))),
inference(paramod,[status(thm)],[c_606,c_908]) ).
cnf(c_910,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(C,inverse(D))),D))) = multiply(A,inverse(multiply(multiply(multiply(inverse(B),C),inverse(C)),C))),
inference(paramod,[status(thm)],[c_744,c_909]) ).
cnf(c_755,plain,
multiply(A,inverse(multiply(multiply(inverse(B),multiply(C,inverse(D))),D))) = multiply(A,inverse(multiply(inverse(B),C))),
inference(paramod,[status(thm)],[c_751,c_910]) ).
cnf(c_911,plain,
multiply(inverse(multiply(A,inverse(B))),inverse(multiply(inverse(C),C))) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_741,c_601]) ).
cnf(c_912,plain,
multiply(inverse(multiply(A,inverse(B))),multiply(inverse(C),C)) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_606,c_911]) ).
cnf(c_913,plain,
inverse(multiply(A,inverse(B))) = multiply(inverse(inverse(B)),inverse(A)),
inference(paramod,[status(thm)],[c_740,c_912]) ).
cnf(c_760,plain,
inverse(multiply(A,inverse(B))) = multiply(B,inverse(A)),
inference(paramod,[status(thm)],[c_741,c_913]) ).
cnf(c_914,plain,
multiply(inverse(multiply(inverse(A),A)),B) = B,
inference(paramod,[status(thm)],[c_606,c_585]) ).
cnf(c_761,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_606,c_914]) ).
cnf(c_915,plain,
multiply(inverse(multiply(inverse(B),B)),multiply(inverse(inverse(C)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),multiply(E,inverse(F)))),multiply(inverse(F),F))),F)))) = multiply(inverse(multiply(E,inverse(C))),D),
inference(paramod,[status(thm)],[c_761,c_646]) ).
cnf(c_916,plain,
multiply(multiply(inverse(B),B),multiply(inverse(inverse(C)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),multiply(E,inverse(F)))),multiply(inverse(F),F))),F)))) = multiply(inverse(multiply(E,inverse(C))),D),
inference(paramod,[status(thm)],[c_606,c_915]) ).
cnf(c_917,plain,
multiply(multiply(inverse(B),B),multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(inverse(D),multiply(E,inverse(F)))),multiply(inverse(F),F))),F)))) = multiply(inverse(multiply(E,inverse(C))),D),
inference(paramod,[status(thm)],[c_741,c_916]) ).
cnf(c_918,plain,
multiply(multiply(inverse(B),B),multiply(C,inverse(multiply(inverse(inverse(multiply(inverse(D),multiply(E,inverse(F))))),F)))) = multiply(inverse(multiply(E,inverse(C))),D),
inference(paramod,[status(thm)],[c_740,c_917]) ).
cnf(c_919,plain,
multiply(multiply(inverse(B),B),multiply(C,inverse(multiply(multiply(inverse(D),multiply(E,inverse(F))),F)))) = multiply(inverse(multiply(E,inverse(C))),D),
inference(paramod,[status(thm)],[c_741,c_918]) ).
cnf(c_920,plain,
multiply(multiply(inverse(B),B),multiply(C,inverse(multiply(inverse(D),E)))) = multiply(inverse(multiply(E,inverse(C))),D),
inference(paramod,[status(thm)],[c_755,c_919]) ).
cnf(c_921,plain,
multiply(C,inverse(multiply(inverse(D),E))) = multiply(inverse(multiply(E,inverse(C))),D),
inference(paramod,[status(thm)],[c_761,c_920]) ).
cnf(c_922,plain,
multiply(C,inverse(multiply(inverse(D),E))) = multiply(multiply(C,inverse(E)),D),
inference(paramod,[status(thm)],[c_760,c_921]) ).
cnf(c_762,plain,
multiply(multiply(A,inverse(B)),C) = multiply(A,inverse(multiply(inverse(C),B))),
inference(copy,[status(thm)],[c_922]) ).
cnf(c_786,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(paramod,[status(thm)],[c_741,c_760]) ).
cnf(c_923,plain,
inverse(multiply(multiply(A,inverse(B)),inverse(C))) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_760,c_760]) ).
cnf(c_924,plain,
inverse(multiply(A,inverse(multiply(inverse(inverse(C)),B)))) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_762,c_923]) ).
cnf(c_925,plain,
inverse(multiply(A,inverse(multiply(C,B)))) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_741,c_924]) ).
cnf(c_926,plain,
inverse(multiply(A,multiply(inverse(B),inverse(C)))) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_786,c_925]) ).
cnf(c_927,plain,
multiply(inverse(multiply(inverse(B),inverse(C))),inverse(A)) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_786,c_926]) ).
cnf(c_928,plain,
multiply(multiply(inverse(inverse(C)),inverse(inverse(B))),inverse(A)) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_786,c_927]) ).
cnf(c_929,plain,
multiply(multiply(C,inverse(inverse(B))),inverse(A)) = multiply(C,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_741,c_928]) ).
cnf(c_790,plain,
multiply(multiply(A,B),inverse(C)) = multiply(A,multiply(B,inverse(C))),
inference(paramod,[status(thm)],[c_741,c_929]) ).
cnf(c_930,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,inverse(inverse(C)))),
inference(paramod,[status(thm)],[c_741,c_790]) ).
cnf(c_801,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_741,c_930]) ).
cnf(c_802,plain,
$false,
inference(resolve,[status(thm)],[c_801,c_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP426-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n004.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Fri Sep 25 14:53:22 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.38 % Process 3458529 was started by sandbox on n004,
% 0.11/0.38 % Fri Sep 25 14:53:22 2026
% 0.11/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.39
% 0.11/0.39 % From the command line: assign(max_seconds, 300).
% 2.40/0.79
% 2.40/0.79 % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 2.40/0.79
% 2.40/0.79 % SZS status Unsatisfiable for theBenchmark
% 2.40/0.79
% 2.40/0.79 % Proof 1 at 0.29 (+ 0.07) seconds.
% 2.40/0.79 % Length of proof is 93.
% 2.40/0.79 % Level of proof is 26.
% 2.40/0.79 % Maximum clause weight is 100.000.
% 2.40/0.79 % Given clauses 63.
% 2.40/0.79
% 2.40/0.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------